[GOAL]
R : Type
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : IsFractionRing R[X] K
f g₁ g₂ : R[X]
hg₁ : Monic g₁
hg₂ : Monic g₂
hcoprime : IsCoprime g₁ g₂
⊢ ∃ q r₁ r₂, degree r₁ < degree g₁ ∧ degree r₂ < degree g₂ ∧ ↑f / (↑g₁ * ↑g₂) = ↑q + ↑r₁ / ↑g₁ + ↑r₂ / ↑g₂
[PROOFSTEP]
rcases hcoprime with ⟨c, d, hcd⟩
[GOAL]
case intro.intro
R : Type
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : IsFractionRing R[X] K
f g₁ g₂ : R[X]
hg₁ : Monic g₁
hg₂ : Monic g₂
c d : R[X]
hcd : c * g₁ + d * g₂ = 1
⊢ ∃ q r₁ r₂, degree r₁ < degree g₁ ∧ degree r₂ < degree g₂ ∧ ↑f / (↑g₁ * ↑g₂) = ↑q + ↑r₁ / ↑g₁ + ↑r₂ / ↑g₂
[PROOFSTEP]
refine' ⟨f * d /ₘ g₁ + f * c /ₘ g₂, f * d %ₘ g₁, f * c %ₘ g₂, degree_modByMonic_lt _ hg₁, degree_modByMonic_lt _ hg₂, _⟩
[GOAL]
case intro.intro
R : Type
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : IsFractionRing R[X] K
f g₁ g₂ : R[X]
hg₁ : Monic g₁
hg₂ : Monic g₂
c d : R[X]
hcd : c * g₁ + d * g₂ = 1
⊢ ↑f / (↑g₁ * ↑g₂) = ↑(f * d /ₘ g₁ + f * c /ₘ g₂) + ↑(f * d %ₘ g₁) / ↑g₁ + ↑(f * c %ₘ g₂) / ↑g₂
[PROOFSTEP]
have hg₁' : (↑g₁ : K) ≠ 0 := by
  norm_cast
  exact hg₁.ne_zero_of_ne zero_ne_one
[GOAL]
R : Type
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : IsFractionRing R[X] K
f g₁ g₂ : R[X]
hg₁ : Monic g₁
hg₂ : Monic g₂
c d : R[X]
hcd : c * g₁ + d * g₂ = 1
⊢ ↑g₁ ≠ 0
[PROOFSTEP]
norm_cast
[GOAL]
R : Type
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : IsFractionRing R[X] K
f g₁ g₂ : R[X]
hg₁ : Monic g₁
hg₂ : Monic g₂
c d : R[X]
hcd : c * g₁ + d * g₂ = 1
⊢ ¬g₁ = 0
[PROOFSTEP]
exact hg₁.ne_zero_of_ne zero_ne_one
[GOAL]
case intro.intro
R : Type
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : IsFractionRing R[X] K
f g₁ g₂ : R[X]
hg₁ : Monic g₁
hg₂ : Monic g₂
c d : R[X]
hcd : c * g₁ + d * g₂ = 1
hg₁' : ↑g₁ ≠ 0
⊢ ↑f / (↑g₁ * ↑g₂) = ↑(f * d /ₘ g₁ + f * c /ₘ g₂) + ↑(f * d %ₘ g₁) / ↑g₁ + ↑(f * c %ₘ g₂) / ↑g₂
[PROOFSTEP]
have hg₂' : (↑g₂ : K) ≠ 0 := by
  norm_cast
  exact hg₂.ne_zero_of_ne zero_ne_one
[GOAL]
R : Type
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : IsFractionRing R[X] K
f g₁ g₂ : R[X]
hg₁ : Monic g₁
hg₂ : Monic g₂
c d : R[X]
hcd : c * g₁ + d * g₂ = 1
hg₁' : ↑g₁ ≠ 0
⊢ ↑g₂ ≠ 0
[PROOFSTEP]
norm_cast
[GOAL]
R : Type
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : IsFractionRing R[X] K
f g₁ g₂ : R[X]
hg₁ : Monic g₁
hg₂ : Monic g₂
c d : R[X]
hcd : c * g₁ + d * g₂ = 1
hg₁' : ↑g₁ ≠ 0
⊢ ¬g₂ = 0
[PROOFSTEP]
exact hg₂.ne_zero_of_ne zero_ne_one
[GOAL]
case intro.intro
R : Type
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : IsFractionRing R[X] K
f g₁ g₂ : R[X]
hg₁ : Monic g₁
hg₂ : Monic g₂
c d : R[X]
hcd : c * g₁ + d * g₂ = 1
hg₁' : ↑g₁ ≠ 0
hg₂' : ↑g₂ ≠ 0
⊢ ↑f / (↑g₁ * ↑g₂) = ↑(f * d /ₘ g₁ + f * c /ₘ g₂) + ↑(f * d %ₘ g₁) / ↑g₁ + ↑(f * c %ₘ g₂) / ↑g₂
[PROOFSTEP]
have hfc := modByMonic_add_div (f * c) hg₂
[GOAL]
case intro.intro
R : Type
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : IsFractionRing R[X] K
f g₁ g₂ : R[X]
hg₁ : Monic g₁
hg₂ : Monic g₂
c d : R[X]
hcd : c * g₁ + d * g₂ = 1
hg₁' : ↑g₁ ≠ 0
hg₂' : ↑g₂ ≠ 0
hfc : f * c %ₘ g₂ + g₂ * (f * c /ₘ g₂) = f * c
⊢ ↑f / (↑g₁ * ↑g₂) = ↑(f * d /ₘ g₁ + f * c /ₘ g₂) + ↑(f * d %ₘ g₁) / ↑g₁ + ↑(f * c %ₘ g₂) / ↑g₂
[PROOFSTEP]
have hfd := modByMonic_add_div (f * d) hg₁
[GOAL]
case intro.intro
R : Type
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : IsFractionRing R[X] K
f g₁ g₂ : R[X]
hg₁ : Monic g₁
hg₂ : Monic g₂
c d : R[X]
hcd : c * g₁ + d * g₂ = 1
hg₁' : ↑g₁ ≠ 0
hg₂' : ↑g₂ ≠ 0
hfc : f * c %ₘ g₂ + g₂ * (f * c /ₘ g₂) = f * c
hfd : f * d %ₘ g₁ + g₁ * (f * d /ₘ g₁) = f * d
⊢ ↑f / (↑g₁ * ↑g₂) = ↑(f * d /ₘ g₁ + f * c /ₘ g₂) + ↑(f * d %ₘ g₁) / ↑g₁ + ↑(f * c %ₘ g₂) / ↑g₂
[PROOFSTEP]
field_simp
[GOAL]
case intro.intro
R : Type
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : IsFractionRing R[X] K
f g₁ g₂ : R[X]
hg₁ : Monic g₁
hg₂ : Monic g₂
c d : R[X]
hcd : c * g₁ + d * g₂ = 1
hg₁' : ↑g₁ ≠ 0
hg₂' : ↑g₂ ≠ 0
hfc : f * c %ₘ g₂ + g₂ * (f * c /ₘ g₂) = f * c
hfd : f * d %ₘ g₁ + g₁ * (f * d /ₘ g₁) = f * d
⊢ ↑f = (↑(f * d /ₘ g₁ + f * c /ₘ g₂) * ↑g₁ + ↑(f * d %ₘ g₁)) * ↑g₂ + ↑(f * c %ₘ g₂) * ↑g₁
[PROOFSTEP]
norm_cast
[GOAL]
case intro.intro
R : Type
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : IsFractionRing R[X] K
f g₁ g₂ : R[X]
hg₁ : Monic g₁
hg₂ : Monic g₂
c d : R[X]
hcd : c * g₁ + d * g₂ = 1
hg₁' : ↑g₁ ≠ 0
hg₂' : ↑g₂ ≠ 0
hfc : f * c %ₘ g₂ + g₂ * (f * c /ₘ g₂) = f * c
hfd : f * d %ₘ g₁ + g₁ * (f * d /ₘ g₁) = f * d
⊢ f = ((f * d /ₘ g₁ + f * c /ₘ g₂) * g₁ + f * d %ₘ g₁) * g₂ + f * c %ₘ g₂ * g₁
[PROOFSTEP]
linear_combination -1 * f * hcd + -1 * g₁ * hfc + -1 * g₂ * hfd
[GOAL]
R : Type
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : IsFractionRing R[X] K
f : R[X]
ι : Type u_1
g : ι → R[X]
s : Finset ι
hg : ∀ (i : ι), i ∈ s → Monic (g i)
hcop : Set.Pairwise ↑s fun i j => IsCoprime (g i) (g j)
⊢ ∃ q r, (∀ (i : ι), i ∈ s → degree (r i) < degree (g i)) ∧ ↑f / ∏ i in s, ↑(g i) = ↑q + ∑ i in s, ↑(r i) / ↑(g i)
[PROOFSTEP]
induction' s using Finset.induction_on with a b hab Hind f generalizing f
[GOAL]
case empty
R : Type
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : IsFractionRing R[X] K
f✝ : R[X]
ι : Type u_1
g : ι → R[X]
s : Finset ι
hg✝ : ∀ (i : ι), i ∈ s → Monic (g i)
hcop✝ : Set.Pairwise ↑s fun i j => IsCoprime (g i) (g j)
f : R[X]
hg : ∀ (i : ι), i ∈ ∅ → Monic (g i)
hcop : Set.Pairwise ↑∅ fun i j => IsCoprime (g i) (g j)
⊢ ∃ q r, (∀ (i : ι), i ∈ ∅ → degree (r i) < degree (g i)) ∧ ↑f / ∏ i in ∅, ↑(g i) = ↑q + ∑ i in ∅, ↑(r i) / ↑(g i)
[PROOFSTEP]
refine' ⟨f, fun _ : ι => (0 : R[X]), fun i => _, by simp⟩
[GOAL]
R : Type
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : IsFractionRing R[X] K
f✝ : R[X]
ι : Type u_1
g : ι → R[X]
s : Finset ι
hg✝ : ∀ (i : ι), i ∈ s → Monic (g i)
hcop✝ : Set.Pairwise ↑s fun i j => IsCoprime (g i) (g j)
f : R[X]
hg : ∀ (i : ι), i ∈ ∅ → Monic (g i)
hcop : Set.Pairwise ↑∅ fun i j => IsCoprime (g i) (g j)
⊢ ↑f / ∏ i in ∅, ↑(g i) = ↑f + ∑ i in ∅, ↑((fun x => 0) i) / ↑(g i)
[PROOFSTEP]
simp
[GOAL]
case empty
R : Type
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : IsFractionRing R[X] K
f✝ : R[X]
ι : Type u_1
g : ι → R[X]
s : Finset ι
hg✝ : ∀ (i : ι), i ∈ s → Monic (g i)
hcop✝ : Set.Pairwise ↑s fun i j => IsCoprime (g i) (g j)
f : R[X]
hg : ∀ (i : ι), i ∈ ∅ → Monic (g i)
hcop : Set.Pairwise ↑∅ fun i j => IsCoprime (g i) (g j)
i : ι
⊢ i ∈ ∅ → degree ((fun x => 0) i) < degree (g i)
[PROOFSTEP]
rintro ⟨⟩
[GOAL]
case insert
R : Type
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : IsFractionRing R[X] K
f✝ : R[X]
ι : Type u_1
g : ι → R[X]
s : Finset ι
hg✝ : ∀ (i : ι), i ∈ s → Monic (g i)
hcop✝ : Set.Pairwise ↑s fun i j => IsCoprime (g i) (g j)
a : ι
b : Finset ι
hab : ¬a ∈ b
Hind :
  ∀ (f : R[X]),
    (∀ (i : ι), i ∈ b → Monic (g i)) →
      (Set.Pairwise ↑b fun i j => IsCoprime (g i) (g j)) →
        ∃ q r, (∀ (i : ι), i ∈ b → degree (r i) < degree (g i)) ∧ ↑f / ∏ i in b, ↑(g i) = ↑q + ∑ i in b, ↑(r i) / ↑(g i)
f : R[X]
hg : ∀ (i : ι), i ∈ insert a b → Monic (g i)
hcop : Set.Pairwise ↑(insert a b) fun i j => IsCoprime (g i) (g j)
⊢ ∃ q r,
    (∀ (i : ι), i ∈ insert a b → degree (r i) < degree (g i)) ∧
      ↑f / ∏ i in insert a b, ↑(g i) = ↑q + ∑ i in insert a b, ↑(r i) / ↑(g i)
[PROOFSTEP]
obtain ⟨q₀, r₁, r₂, hdeg₁, _, hf : (↑f : K) / _ = _⟩ :=
  div_eq_quo_add_rem_div_add_rem_div R K f (hg a (b.mem_insert_self a) : Monic (g a))
    (monic_prod_of_monic _ _ fun i hi => hg i (Finset.mem_insert_of_mem hi) : Monic (∏ i : ι in b, g i))
    (IsCoprime.prod_right fun i hi =>
      hcop (Finset.mem_coe.2 (b.mem_insert_self a)) (Finset.mem_coe.2 (Finset.mem_insert_of_mem hi))
        (by rintro rfl; exact hab hi))
[GOAL]
R : Type
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : IsFractionRing R[X] K
f✝ : R[X]
ι : Type u_1
g : ι → R[X]
s : Finset ι
hg✝ : ∀ (i : ι), i ∈ s → Monic (g i)
hcop✝ : Set.Pairwise ↑s fun i j => IsCoprime (g i) (g j)
a : ι
b : Finset ι
hab : ¬a ∈ b
Hind :
  ∀ (f : R[X]),
    (∀ (i : ι), i ∈ b → Monic (g i)) →
      (Set.Pairwise ↑b fun i j => IsCoprime (g i) (g j)) →
        ∃ q r, (∀ (i : ι), i ∈ b → degree (r i) < degree (g i)) ∧ ↑f / ∏ i in b, ↑(g i) = ↑q + ∑ i in b, ↑(r i) / ↑(g i)
f : R[X]
hg : ∀ (i : ι), i ∈ insert a b → Monic (g i)
hcop : Set.Pairwise ↑(insert a b) fun i j => IsCoprime (g i) (g j)
i : ι
hi : i ∈ b
⊢ a ≠ i
[PROOFSTEP]
rintro rfl
[GOAL]
R : Type
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : IsFractionRing R[X] K
f✝ : R[X]
ι : Type u_1
g : ι → R[X]
s : Finset ι
hg✝ : ∀ (i : ι), i ∈ s → Monic (g i)
hcop✝ : Set.Pairwise ↑s fun i j => IsCoprime (g i) (g j)
a : ι
b : Finset ι
hab : ¬a ∈ b
Hind :
  ∀ (f : R[X]),
    (∀ (i : ι), i ∈ b → Monic (g i)) →
      (Set.Pairwise ↑b fun i j => IsCoprime (g i) (g j)) →
        ∃ q r, (∀ (i : ι), i ∈ b → degree (r i) < degree (g i)) ∧ ↑f / ∏ i in b, ↑(g i) = ↑q + ∑ i in b, ↑(r i) / ↑(g i)
f : R[X]
hg : ∀ (i : ι), i ∈ insert a b → Monic (g i)
hcop : Set.Pairwise ↑(insert a b) fun i j => IsCoprime (g i) (g j)
hi : a ∈ b
⊢ False
[PROOFSTEP]
exact hab hi
[GOAL]
case insert.intro.intro.intro.intro.intro
R : Type
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : IsFractionRing R[X] K
f✝ : R[X]
ι : Type u_1
g : ι → R[X]
s : Finset ι
hg✝ : ∀ (i : ι), i ∈ s → Monic (g i)
hcop✝ : Set.Pairwise ↑s fun i j => IsCoprime (g i) (g j)
a : ι
b : Finset ι
hab : ¬a ∈ b
Hind :
  ∀ (f : R[X]),
    (∀ (i : ι), i ∈ b → Monic (g i)) →
      (Set.Pairwise ↑b fun i j => IsCoprime (g i) (g j)) →
        ∃ q r, (∀ (i : ι), i ∈ b → degree (r i) < degree (g i)) ∧ ↑f / ∏ i in b, ↑(g i) = ↑q + ∑ i in b, ↑(r i) / ↑(g i)
f : R[X]
hg : ∀ (i : ι), i ∈ insert a b → Monic (g i)
hcop : Set.Pairwise ↑(insert a b) fun i j => IsCoprime (g i) (g j)
q₀ r₁ r₂ : R[X]
hdeg₁ : degree r₁ < degree (g a)
left✝ : degree r₂ < degree (∏ i in b, g i)
hf : ↑f / (↑(g a) * ↑(∏ i in b, g i)) = ↑q₀ + ↑r₁ / ↑(g a) + ↑r₂ / ↑(∏ i in b, g i)
⊢ ∃ q r,
    (∀ (i : ι), i ∈ insert a b → degree (r i) < degree (g i)) ∧
      ↑f / ∏ i in insert a b, ↑(g i) = ↑q + ∑ i in insert a b, ↑(r i) / ↑(g i)
[PROOFSTEP]
obtain ⟨q, r, hrdeg, IH⟩ :=
  Hind _ (fun i hi => hg i (Finset.mem_insert_of_mem hi))
    (Set.Pairwise.mono (Finset.coe_subset.2 fun i hi => Finset.mem_insert_of_mem hi) hcop)
[GOAL]
case insert.intro.intro.intro.intro.intro.intro.intro.intro
R : Type
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : IsFractionRing R[X] K
f✝ : R[X]
ι : Type u_1
g : ι → R[X]
s : Finset ι
hg✝ : ∀ (i : ι), i ∈ s → Monic (g i)
hcop✝ : Set.Pairwise ↑s fun i j => IsCoprime (g i) (g j)
a : ι
b : Finset ι
hab : ¬a ∈ b
Hind :
  ∀ (f : R[X]),
    (∀ (i : ι), i ∈ b → Monic (g i)) →
      (Set.Pairwise ↑b fun i j => IsCoprime (g i) (g j)) →
        ∃ q r, (∀ (i : ι), i ∈ b → degree (r i) < degree (g i)) ∧ ↑f / ∏ i in b, ↑(g i) = ↑q + ∑ i in b, ↑(r i) / ↑(g i)
f : R[X]
hg : ∀ (i : ι), i ∈ insert a b → Monic (g i)
hcop : Set.Pairwise ↑(insert a b) fun i j => IsCoprime (g i) (g j)
q₀ r₁ r₂ : R[X]
hdeg₁ : degree r₁ < degree (g a)
left✝ : degree r₂ < degree (∏ i in b, g i)
hf : ↑f / (↑(g a) * ↑(∏ i in b, g i)) = ↑q₀ + ↑r₁ / ↑(g a) + ↑r₂ / ↑(∏ i in b, g i)
q : R[X]
r : ι → R[X]
hrdeg : ∀ (i : ι), i ∈ b → degree (r i) < degree (g i)
IH : ↑?m.70687 / ∏ i in b, ↑(g i) = ↑q + ∑ i in b, ↑(r i) / ↑(g i)
⊢ ∃ q r,
    (∀ (i : ι), i ∈ insert a b → degree (r i) < degree (g i)) ∧
      ↑f / ∏ i in insert a b, ↑(g i) = ↑q + ∑ i in insert a b, ↑(r i) / ↑(g i)
[PROOFSTEP]
refine ⟨q₀ + q, fun i => if i = a then r₁ else r i, ?_, ?_⟩
[GOAL]
case insert.intro.intro.intro.intro.intro.intro.intro.intro.refine_1
R : Type
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : IsFractionRing R[X] K
f✝ : R[X]
ι : Type u_1
g : ι → R[X]
s : Finset ι
hg✝ : ∀ (i : ι), i ∈ s → Monic (g i)
hcop✝ : Set.Pairwise ↑s fun i j => IsCoprime (g i) (g j)
a : ι
b : Finset ι
hab : ¬a ∈ b
Hind :
  ∀ (f : R[X]),
    (∀ (i : ι), i ∈ b → Monic (g i)) →
      (Set.Pairwise ↑b fun i j => IsCoprime (g i) (g j)) →
        ∃ q r, (∀ (i : ι), i ∈ b → degree (r i) < degree (g i)) ∧ ↑f / ∏ i in b, ↑(g i) = ↑q + ∑ i in b, ↑(r i) / ↑(g i)
f : R[X]
hg : ∀ (i : ι), i ∈ insert a b → Monic (g i)
hcop : Set.Pairwise ↑(insert a b) fun i j => IsCoprime (g i) (g j)
q₀ r₁ r₂ : R[X]
hdeg₁ : degree r₁ < degree (g a)
left✝ : degree r₂ < degree (∏ i in b, g i)
hf : ↑f / (↑(g a) * ↑(∏ i in b, g i)) = ↑q₀ + ↑r₁ / ↑(g a) + ↑r₂ / ↑(∏ i in b, g i)
q : R[X]
r : ι → R[X]
hrdeg : ∀ (i : ι), i ∈ b → degree (r i) < degree (g i)
IH : ↑?m.70687 / ∏ i in b, ↑(g i) = ↑q + ∑ i in b, ↑(r i) / ↑(g i)
⊢ ∀ (i : ι), i ∈ insert a b → degree ((fun i => if i = a then r₁ else r i) i) < degree (g i)
[PROOFSTEP]
intro i
[GOAL]
case insert.intro.intro.intro.intro.intro.intro.intro.intro.refine_1
R : Type
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : IsFractionRing R[X] K
f✝ : R[X]
ι : Type u_1
g : ι → R[X]
s : Finset ι
hg✝ : ∀ (i : ι), i ∈ s → Monic (g i)
hcop✝ : Set.Pairwise ↑s fun i j => IsCoprime (g i) (g j)
a : ι
b : Finset ι
hab : ¬a ∈ b
Hind :
  ∀ (f : R[X]),
    (∀ (i : ι), i ∈ b → Monic (g i)) →
      (Set.Pairwise ↑b fun i j => IsCoprime (g i) (g j)) →
        ∃ q r, (∀ (i : ι), i ∈ b → degree (r i) < degree (g i)) ∧ ↑f / ∏ i in b, ↑(g i) = ↑q + ∑ i in b, ↑(r i) / ↑(g i)
f : R[X]
hg : ∀ (i : ι), i ∈ insert a b → Monic (g i)
hcop : Set.Pairwise ↑(insert a b) fun i j => IsCoprime (g i) (g j)
q₀ r₁ r₂ : R[X]
hdeg₁ : degree r₁ < degree (g a)
left✝ : degree r₂ < degree (∏ i in b, g i)
hf : ↑f / (↑(g a) * ↑(∏ i in b, g i)) = ↑q₀ + ↑r₁ / ↑(g a) + ↑r₂ / ↑(∏ i in b, g i)
q : R[X]
r : ι → R[X]
hrdeg : ∀ (i : ι), i ∈ b → degree (r i) < degree (g i)
IH : ↑?m.70687 / ∏ i in b, ↑(g i) = ↑q + ∑ i in b, ↑(r i) / ↑(g i)
i : ι
⊢ i ∈ insert a b → degree ((fun i => if i = a then r₁ else r i) i) < degree (g i)
[PROOFSTEP]
dsimp only
[GOAL]
case insert.intro.intro.intro.intro.intro.intro.intro.intro.refine_1
R : Type
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : IsFractionRing R[X] K
f✝ : R[X]
ι : Type u_1
g : ι → R[X]
s : Finset ι
hg✝ : ∀ (i : ι), i ∈ s → Monic (g i)
hcop✝ : Set.Pairwise ↑s fun i j => IsCoprime (g i) (g j)
a : ι
b : Finset ι
hab : ¬a ∈ b
Hind :
  ∀ (f : R[X]),
    (∀ (i : ι), i ∈ b → Monic (g i)) →
      (Set.Pairwise ↑b fun i j => IsCoprime (g i) (g j)) →
        ∃ q r, (∀ (i : ι), i ∈ b → degree (r i) < degree (g i)) ∧ ↑f / ∏ i in b, ↑(g i) = ↑q + ∑ i in b, ↑(r i) / ↑(g i)
f : R[X]
hg : ∀ (i : ι), i ∈ insert a b → Monic (g i)
hcop : Set.Pairwise ↑(insert a b) fun i j => IsCoprime (g i) (g j)
q₀ r₁ r₂ : R[X]
hdeg₁ : degree r₁ < degree (g a)
left✝ : degree r₂ < degree (∏ i in b, g i)
hf : ↑f / (↑(g a) * ↑(∏ i in b, g i)) = ↑q₀ + ↑r₁ / ↑(g a) + ↑r₂ / ↑(∏ i in b, g i)
q : R[X]
r : ι → R[X]
hrdeg : ∀ (i : ι), i ∈ b → degree (r i) < degree (g i)
IH : ↑?m.70687 / ∏ i in b, ↑(g i) = ↑q + ∑ i in b, ↑(r i) / ↑(g i)
i : ι
⊢ i ∈ insert a b → degree (if i = a then r₁ else r i) < degree (g i)
[PROOFSTEP]
split_ifs with h1
[GOAL]
case pos
R : Type
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : IsFractionRing R[X] K
f✝ : R[X]
ι : Type u_1
g : ι → R[X]
s : Finset ι
hg✝ : ∀ (i : ι), i ∈ s → Monic (g i)
hcop✝ : Set.Pairwise ↑s fun i j => IsCoprime (g i) (g j)
a : ι
b : Finset ι
hab : ¬a ∈ b
Hind :
  ∀ (f : R[X]),
    (∀ (i : ι), i ∈ b → Monic (g i)) →
      (Set.Pairwise ↑b fun i j => IsCoprime (g i) (g j)) →
        ∃ q r, (∀ (i : ι), i ∈ b → degree (r i) < degree (g i)) ∧ ↑f / ∏ i in b, ↑(g i) = ↑q + ∑ i in b, ↑(r i) / ↑(g i)
f : R[X]
hg : ∀ (i : ι), i ∈ insert a b → Monic (g i)
hcop : Set.Pairwise ↑(insert a b) fun i j => IsCoprime (g i) (g j)
q₀ r₁ r₂ : R[X]
hdeg₁ : degree r₁ < degree (g a)
left✝ : degree r₂ < degree (∏ i in b, g i)
hf : ↑f / (↑(g a) * ↑(∏ i in b, g i)) = ↑q₀ + ↑r₁ / ↑(g a) + ↑r₂ / ↑(∏ i in b, g i)
q : R[X]
r : ι → R[X]
hrdeg : ∀ (i : ι), i ∈ b → degree (r i) < degree (g i)
IH : ↑?m.70687 / ∏ i in b, ↑(g i) = ↑q + ∑ i in b, ↑(r i) / ↑(g i)
i : ι
h1 : i = a
⊢ i ∈ insert a b → degree r₁ < degree (g i)
[PROOFSTEP]
cases h1
[GOAL]
case pos.refl
R : Type
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : IsFractionRing R[X] K
f✝ : R[X]
ι : Type u_1
g : ι → R[X]
s : Finset ι
hg✝ : ∀ (i : ι), i ∈ s → Monic (g i)
hcop✝ : Set.Pairwise ↑s fun i j => IsCoprime (g i) (g j)
a : ι
b : Finset ι
hab : ¬a ∈ b
Hind :
  ∀ (f : R[X]),
    (∀ (i : ι), i ∈ b → Monic (g i)) →
      (Set.Pairwise ↑b fun i j => IsCoprime (g i) (g j)) →
        ∃ q r, (∀ (i : ι), i ∈ b → degree (r i) < degree (g i)) ∧ ↑f / ∏ i in b, ↑(g i) = ↑q + ∑ i in b, ↑(r i) / ↑(g i)
f : R[X]
hg : ∀ (i : ι), i ∈ insert a b → Monic (g i)
hcop : Set.Pairwise ↑(insert a b) fun i j => IsCoprime (g i) (g j)
q₀ r₁ r₂ : R[X]
hdeg₁ : degree r₁ < degree (g a)
left✝ : degree r₂ < degree (∏ i in b, g i)
hf : ↑f / (↑(g a) * ↑(∏ i in b, g i)) = ↑q₀ + ↑r₁ / ↑(g a) + ↑r₂ / ↑(∏ i in b, g i)
q : R[X]
r : ι → R[X]
hrdeg : ∀ (i : ι), i ∈ b → degree (r i) < degree (g i)
IH : ↑?m.70687 / ∏ i in b, ↑(g i) = ↑q + ∑ i in b, ↑(r i) / ↑(g i)
⊢ a ∈ insert a b → degree r₁ < degree (g a)
[PROOFSTEP]
intro
[GOAL]
case pos.refl
R : Type
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : IsFractionRing R[X] K
f✝ : R[X]
ι : Type u_1
g : ι → R[X]
s : Finset ι
hg✝ : ∀ (i : ι), i ∈ s → Monic (g i)
hcop✝ : Set.Pairwise ↑s fun i j => IsCoprime (g i) (g j)
a : ι
b : Finset ι
hab : ¬a ∈ b
Hind :
  ∀ (f : R[X]),
    (∀ (i : ι), i ∈ b → Monic (g i)) →
      (Set.Pairwise ↑b fun i j => IsCoprime (g i) (g j)) →
        ∃ q r, (∀ (i : ι), i ∈ b → degree (r i) < degree (g i)) ∧ ↑f / ∏ i in b, ↑(g i) = ↑q + ∑ i in b, ↑(r i) / ↑(g i)
f : R[X]
hg : ∀ (i : ι), i ∈ insert a b → Monic (g i)
hcop : Set.Pairwise ↑(insert a b) fun i j => IsCoprime (g i) (g j)
q₀ r₁ r₂ : R[X]
hdeg₁ : degree r₁ < degree (g a)
left✝ : degree r₂ < degree (∏ i in b, g i)
hf : ↑f / (↑(g a) * ↑(∏ i in b, g i)) = ↑q₀ + ↑r₁ / ↑(g a) + ↑r₂ / ↑(∏ i in b, g i)
q : R[X]
r : ι → R[X]
hrdeg : ∀ (i : ι), i ∈ b → degree (r i) < degree (g i)
IH : ↑?m.70687 / ∏ i in b, ↑(g i) = ↑q + ∑ i in b, ↑(r i) / ↑(g i)
a✝ : a ∈ insert a b
⊢ degree r₁ < degree (g a)
[PROOFSTEP]
exact hdeg₁
[GOAL]
case neg
R : Type
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : IsFractionRing R[X] K
f✝ : R[X]
ι : Type u_1
g : ι → R[X]
s : Finset ι
hg✝ : ∀ (i : ι), i ∈ s → Monic (g i)
hcop✝ : Set.Pairwise ↑s fun i j => IsCoprime (g i) (g j)
a : ι
b : Finset ι
hab : ¬a ∈ b
Hind :
  ∀ (f : R[X]),
    (∀ (i : ι), i ∈ b → Monic (g i)) →
      (Set.Pairwise ↑b fun i j => IsCoprime (g i) (g j)) →
        ∃ q r, (∀ (i : ι), i ∈ b → degree (r i) < degree (g i)) ∧ ↑f / ∏ i in b, ↑(g i) = ↑q + ∑ i in b, ↑(r i) / ↑(g i)
f : R[X]
hg : ∀ (i : ι), i ∈ insert a b → Monic (g i)
hcop : Set.Pairwise ↑(insert a b) fun i j => IsCoprime (g i) (g j)
q₀ r₁ r₂ : R[X]
hdeg₁ : degree r₁ < degree (g a)
left✝ : degree r₂ < degree (∏ i in b, g i)
hf : ↑f / (↑(g a) * ↑(∏ i in b, g i)) = ↑q₀ + ↑r₁ / ↑(g a) + ↑r₂ / ↑(∏ i in b, g i)
q : R[X]
r : ι → R[X]
hrdeg : ∀ (i : ι), i ∈ b → degree (r i) < degree (g i)
IH : ↑?m.70687 / ∏ i in b, ↑(g i) = ↑q + ∑ i in b, ↑(r i) / ↑(g i)
i : ι
h1 : ¬i = a
⊢ i ∈ insert a b → degree (r i) < degree (g i)
[PROOFSTEP]
intro hi
[GOAL]
case neg
R : Type
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : IsFractionRing R[X] K
f✝ : R[X]
ι : Type u_1
g : ι → R[X]
s : Finset ι
hg✝ : ∀ (i : ι), i ∈ s → Monic (g i)
hcop✝ : Set.Pairwise ↑s fun i j => IsCoprime (g i) (g j)
a : ι
b : Finset ι
hab : ¬a ∈ b
Hind :
  ∀ (f : R[X]),
    (∀ (i : ι), i ∈ b → Monic (g i)) →
      (Set.Pairwise ↑b fun i j => IsCoprime (g i) (g j)) →
        ∃ q r, (∀ (i : ι), i ∈ b → degree (r i) < degree (g i)) ∧ ↑f / ∏ i in b, ↑(g i) = ↑q + ∑ i in b, ↑(r i) / ↑(g i)
f : R[X]
hg : ∀ (i : ι), i ∈ insert a b → Monic (g i)
hcop : Set.Pairwise ↑(insert a b) fun i j => IsCoprime (g i) (g j)
q₀ r₁ r₂ : R[X]
hdeg₁ : degree r₁ < degree (g a)
left✝ : degree r₂ < degree (∏ i in b, g i)
hf : ↑f / (↑(g a) * ↑(∏ i in b, g i)) = ↑q₀ + ↑r₁ / ↑(g a) + ↑r₂ / ↑(∏ i in b, g i)
q : R[X]
r : ι → R[X]
hrdeg : ∀ (i : ι), i ∈ b → degree (r i) < degree (g i)
IH : ↑?m.70687 / ∏ i in b, ↑(g i) = ↑q + ∑ i in b, ↑(r i) / ↑(g i)
i : ι
h1 : ¬i = a
hi : i ∈ insert a b
⊢ degree (r i) < degree (g i)
[PROOFSTEP]
exact hrdeg i (Finset.mem_of_mem_insert_of_ne hi h1)
[GOAL]
case insert.intro.intro.intro.intro.intro.intro.intro.intro.refine_2
R : Type
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : IsFractionRing R[X] K
f✝ : R[X]
ι : Type u_1
g : ι → R[X]
s : Finset ι
hg✝ : ∀ (i : ι), i ∈ s → Monic (g i)
hcop✝ : Set.Pairwise ↑s fun i j => IsCoprime (g i) (g j)
a : ι
b : Finset ι
hab : ¬a ∈ b
Hind :
  ∀ (f : R[X]),
    (∀ (i : ι), i ∈ b → Monic (g i)) →
      (Set.Pairwise ↑b fun i j => IsCoprime (g i) (g j)) →
        ∃ q r, (∀ (i : ι), i ∈ b → degree (r i) < degree (g i)) ∧ ↑f / ∏ i in b, ↑(g i) = ↑q + ∑ i in b, ↑(r i) / ↑(g i)
f : R[X]
hg : ∀ (i : ι), i ∈ insert a b → Monic (g i)
hcop : Set.Pairwise ↑(insert a b) fun i j => IsCoprime (g i) (g j)
q₀ r₁ r₂ : R[X]
hdeg₁ : degree r₁ < degree (g a)
left✝ : degree r₂ < degree (∏ i in b, g i)
hf : ↑f / (↑(g a) * ↑(∏ i in b, g i)) = ↑q₀ + ↑r₁ / ↑(g a) + ↑r₂ / ↑(∏ i in b, g i)
q : R[X]
r : ι → R[X]
hrdeg : ∀ (i : ι), i ∈ b → degree (r i) < degree (g i)
IH : ↑?m.70687 / ∏ i in b, ↑(g i) = ↑q + ∑ i in b, ↑(r i) / ↑(g i)
⊢ ↑f / ∏ i in insert a b, ↑(g i) = ↑(q₀ + q) + ∑ i in insert a b, ↑((fun i => if i = a then r₁ else r i) i) / ↑(g i)
[PROOFSTEP]
norm_cast at hf IH ⊢
[GOAL]
case insert.intro.intro.intro.intro.intro.intro.intro.intro.refine_2
R : Type
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : IsFractionRing R[X] K
f✝ : R[X]
ι : Type u_1
g : ι → R[X]
s : Finset ι
hg✝ : ∀ (i : ι), i ∈ s → Monic (g i)
hcop✝ : Set.Pairwise ↑s fun i j => IsCoprime (g i) (g j)
a : ι
b : Finset ι
hab : ¬a ∈ b
Hind :
  ∀ (f : R[X]),
    (∀ (i : ι), i ∈ b → Monic (g i)) →
      (Set.Pairwise ↑b fun i j => IsCoprime (g i) (g j)) →
        ∃ q r, (∀ (i : ι), i ∈ b → degree (r i) < degree (g i)) ∧ ↑f / ∏ i in b, ↑(g i) = ↑q + ∑ i in b, ↑(r i) / ↑(g i)
f : R[X]
hg : ∀ (i : ι), i ∈ insert a b → Monic (g i)
hcop : Set.Pairwise ↑(insert a b) fun i j => IsCoprime (g i) (g j)
q₀ r₁ r₂ : R[X]
hdeg₁ : degree r₁ < degree (g a)
left✝ : degree r₂ < degree (∏ i in b, g i)
hf✝ : ↑f / (↑(g a) * ↑(∏ i in b, g i)) = ↑q₀ + ↑r₁ / ↑(g a) + ↑r₂ / ↑(∏ i in b, g i)
q : R[X]
r : ι → R[X]
hrdeg : ∀ (i : ι), i ∈ b → degree (r i) < degree (g i)
hf : ↑f / ↑(g a * ∏ i in b, g i) = ↑q₀ + ↑r₁ / ↑(g a) + ↑r₂ / ↑(∏ i in b, g i)
IH : ↑?m.70687 / ↑(∏ i in b, g i) = ↑q + ∑ i in b, ↑(r i) / ↑(g i)
⊢ ↑f / ↑(∏ i in insert a b, g i) = ↑(q₀ + q) + ∑ x in insert a b, ↑(if x = a then r₁ else r x) / ↑(g x)
[PROOFSTEP]
rw [Finset.prod_insert hab, hf, IH, Finset.sum_insert hab, if_pos rfl]
[GOAL]
case insert.intro.intro.intro.intro.intro.intro.intro.intro.refine_2
R : Type
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : IsFractionRing R[X] K
f✝ : R[X]
ι : Type u_1
g : ι → R[X]
s : Finset ι
hg✝ : ∀ (i : ι), i ∈ s → Monic (g i)
hcop✝ : Set.Pairwise ↑s fun i j => IsCoprime (g i) (g j)
a : ι
b : Finset ι
hab : ¬a ∈ b
Hind :
  ∀ (f : R[X]),
    (∀ (i : ι), i ∈ b → Monic (g i)) →
      (Set.Pairwise ↑b fun i j => IsCoprime (g i) (g j)) →
        ∃ q r, (∀ (i : ι), i ∈ b → degree (r i) < degree (g i)) ∧ ↑f / ∏ i in b, ↑(g i) = ↑q + ∑ i in b, ↑(r i) / ↑(g i)
f : R[X]
hg : ∀ (i : ι), i ∈ insert a b → Monic (g i)
hcop : Set.Pairwise ↑(insert a b) fun i j => IsCoprime (g i) (g j)
q₀ r₁ r₂ : R[X]
hdeg₁ : degree r₁ < degree (g a)
left✝ : degree r₂ < degree (∏ i in b, g i)
hf✝ : ↑f / (↑(g a) * ↑(∏ i in b, g i)) = ↑q₀ + ↑r₁ / ↑(g a) + ↑r₂ / ↑(∏ i in b, g i)
q : R[X]
r : ι → R[X]
hrdeg : ∀ (i : ι), i ∈ b → degree (r i) < degree (g i)
hf : ↑f / ↑(g a * ∏ i in b, g i) = ↑q₀ + ↑r₁ / ↑(g a) + ↑r₂ / ↑(∏ i in b, g i)
IH : ↑r₂ / ↑(∏ i in b, g i) = ↑q + ∑ i in b, ↑(r i) / ↑(g i)
⊢ ↑q₀ + ↑r₁ / ↑(g a) + (↑q + ∑ i in b, ↑(r i) / ↑(g i)) =
    ↑(q₀ + q) + (↑r₁ / ↑(g a) + ∑ x in b, ↑(if x = a then r₁ else r x) / ↑(g x))
[PROOFSTEP]
trans (↑(q₀ + q : R[X]) : K) + (↑r₁ / ↑(g a) + ∑ i : ι in b, (r i : K) / (g i : K))
[GOAL]
R : Type
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : IsFractionRing R[X] K
f✝ : R[X]
ι : Type u_1
g : ι → R[X]
s : Finset ι
hg✝ : ∀ (i : ι), i ∈ s → Monic (g i)
hcop✝ : Set.Pairwise ↑s fun i j => IsCoprime (g i) (g j)
a : ι
b : Finset ι
hab : ¬a ∈ b
Hind :
  ∀ (f : R[X]),
    (∀ (i : ι), i ∈ b → Monic (g i)) →
      (Set.Pairwise ↑b fun i j => IsCoprime (g i) (g j)) →
        ∃ q r, (∀ (i : ι), i ∈ b → degree (r i) < degree (g i)) ∧ ↑f / ∏ i in b, ↑(g i) = ↑q + ∑ i in b, ↑(r i) / ↑(g i)
f : R[X]
hg : ∀ (i : ι), i ∈ insert a b → Monic (g i)
hcop : Set.Pairwise ↑(insert a b) fun i j => IsCoprime (g i) (g j)
q₀ r₁ r₂ : R[X]
hdeg₁ : degree r₁ < degree (g a)
left✝ : degree r₂ < degree (∏ i in b, g i)
hf✝ : ↑f / (↑(g a) * ↑(∏ i in b, g i)) = ↑q₀ + ↑r₁ / ↑(g a) + ↑r₂ / ↑(∏ i in b, g i)
q : R[X]
r : ι → R[X]
hrdeg : ∀ (i : ι), i ∈ b → degree (r i) < degree (g i)
hf : ↑f / ↑(g a * ∏ i in b, g i) = ↑q₀ + ↑r₁ / ↑(g a) + ↑r₂ / ↑(∏ i in b, g i)
IH : ↑r₂ / ↑(∏ i in b, g i) = ↑q + ∑ i in b, ↑(r i) / ↑(g i)
⊢ ↑q₀ + ↑r₁ / ↑(g a) + (↑q + ∑ i in b, ↑(r i) / ↑(g i)) = ↑(q₀ + q) + (↑r₁ / ↑(g a) + ∑ i in b, ↑(r i) / ↑(g i))
[PROOFSTEP]
push_cast
[GOAL]
R : Type
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : IsFractionRing R[X] K
f✝ : R[X]
ι : Type u_1
g : ι → R[X]
s : Finset ι
hg✝ : ∀ (i : ι), i ∈ s → Monic (g i)
hcop✝ : Set.Pairwise ↑s fun i j => IsCoprime (g i) (g j)
a : ι
b : Finset ι
hab : ¬a ∈ b
Hind :
  ∀ (f : R[X]),
    (∀ (i : ι), i ∈ b → Monic (g i)) →
      (Set.Pairwise ↑b fun i j => IsCoprime (g i) (g j)) →
        ∃ q r, (∀ (i : ι), i ∈ b → degree (r i) < degree (g i)) ∧ ↑f / ∏ i in b, ↑(g i) = ↑q + ∑ i in b, ↑(r i) / ↑(g i)
f : R[X]
hg : ∀ (i : ι), i ∈ insert a b → Monic (g i)
hcop : Set.Pairwise ↑(insert a b) fun i j => IsCoprime (g i) (g j)
q₀ r₁ r₂ : R[X]
hdeg₁ : degree r₁ < degree (g a)
left✝ : degree r₂ < degree (∏ i in b, g i)
hf✝ : ↑f / (↑(g a) * ↑(∏ i in b, g i)) = ↑q₀ + ↑r₁ / ↑(g a) + ↑r₂ / ↑(∏ i in b, g i)
q : R[X]
r : ι → R[X]
hrdeg : ∀ (i : ι), i ∈ b → degree (r i) < degree (g i)
hf : ↑f / ↑(g a * ∏ i in b, g i) = ↑q₀ + ↑r₁ / ↑(g a) + ↑r₂ / ↑(∏ i in b, g i)
IH : ↑r₂ / ↑(∏ i in b, g i) = ↑q + ∑ i in b, ↑(r i) / ↑(g i)
⊢ ↑q₀ + ↑r₁ / ↑(g a) + (↑q + ∑ i in b, ↑(r i) / ↑(g i)) = ↑q₀ + ↑q + (↑r₁ / ↑(g a) + ∑ i in b, ↑(r i) / ↑(g i))
[PROOFSTEP]
ring
[GOAL]
R : Type
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : IsFractionRing R[X] K
f✝ : R[X]
ι : Type u_1
g : ι → R[X]
s : Finset ι
hg✝ : ∀ (i : ι), i ∈ s → Monic (g i)
hcop✝ : Set.Pairwise ↑s fun i j => IsCoprime (g i) (g j)
a : ι
b : Finset ι
hab : ¬a ∈ b
Hind :
  ∀ (f : R[X]),
    (∀ (i : ι), i ∈ b → Monic (g i)) →
      (Set.Pairwise ↑b fun i j => IsCoprime (g i) (g j)) →
        ∃ q r, (∀ (i : ι), i ∈ b → degree (r i) < degree (g i)) ∧ ↑f / ∏ i in b, ↑(g i) = ↑q + ∑ i in b, ↑(r i) / ↑(g i)
f : R[X]
hg : ∀ (i : ι), i ∈ insert a b → Monic (g i)
hcop : Set.Pairwise ↑(insert a b) fun i j => IsCoprime (g i) (g j)
q₀ r₁ r₂ : R[X]
hdeg₁ : degree r₁ < degree (g a)
left✝ : degree r₂ < degree (∏ i in b, g i)
hf✝ : ↑f / (↑(g a) * ↑(∏ i in b, g i)) = ↑q₀ + ↑r₁ / ↑(g a) + ↑r₂ / ↑(∏ i in b, g i)
q : R[X]
r : ι → R[X]
hrdeg : ∀ (i : ι), i ∈ b → degree (r i) < degree (g i)
hf : ↑f / ↑(g a * ∏ i in b, g i) = ↑q₀ + ↑r₁ / ↑(g a) + ↑r₂ / ↑(∏ i in b, g i)
IH : ↑r₂ / ↑(∏ i in b, g i) = ↑q + ∑ i in b, ↑(r i) / ↑(g i)
⊢ ↑(q₀ + q) + (↑r₁ / ↑(g a) + ∑ i in b, ↑(r i) / ↑(g i)) =
    ↑(q₀ + q) + (↑r₁ / ↑(g a) + ∑ x in b, ↑(if x = a then r₁ else r x) / ↑(g x))
[PROOFSTEP]
congr 2
[GOAL]
case e_a.e_a
R : Type
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : IsFractionRing R[X] K
f✝ : R[X]
ι : Type u_1
g : ι → R[X]
s : Finset ι
hg✝ : ∀ (i : ι), i ∈ s → Monic (g i)
hcop✝ : Set.Pairwise ↑s fun i j => IsCoprime (g i) (g j)
a : ι
b : Finset ι
hab : ¬a ∈ b
Hind :
  ∀ (f : R[X]),
    (∀ (i : ι), i ∈ b → Monic (g i)) →
      (Set.Pairwise ↑b fun i j => IsCoprime (g i) (g j)) →
        ∃ q r, (∀ (i : ι), i ∈ b → degree (r i) < degree (g i)) ∧ ↑f / ∏ i in b, ↑(g i) = ↑q + ∑ i in b, ↑(r i) / ↑(g i)
f : R[X]
hg : ∀ (i : ι), i ∈ insert a b → Monic (g i)
hcop : Set.Pairwise ↑(insert a b) fun i j => IsCoprime (g i) (g j)
q₀ r₁ r₂ : R[X]
hdeg₁ : degree r₁ < degree (g a)
left✝ : degree r₂ < degree (∏ i in b, g i)
hf✝ : ↑f / (↑(g a) * ↑(∏ i in b, g i)) = ↑q₀ + ↑r₁ / ↑(g a) + ↑r₂ / ↑(∏ i in b, g i)
q : R[X]
r : ι → R[X]
hrdeg : ∀ (i : ι), i ∈ b → degree (r i) < degree (g i)
hf : ↑f / ↑(g a * ∏ i in b, g i) = ↑q₀ + ↑r₁ / ↑(g a) + ↑r₂ / ↑(∏ i in b, g i)
IH : ↑r₂ / ↑(∏ i in b, g i) = ↑q + ∑ i in b, ↑(r i) / ↑(g i)
⊢ ∑ i in b, ↑(r i) / ↑(g i) = ∑ x in b, ↑(if x = a then r₁ else r x) / ↑(g x)
[PROOFSTEP]
refine' Finset.sum_congr rfl fun x hxb => _
[GOAL]
case e_a.e_a
R : Type
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : IsFractionRing R[X] K
f✝ : R[X]
ι : Type u_1
g : ι → R[X]
s : Finset ι
hg✝ : ∀ (i : ι), i ∈ s → Monic (g i)
hcop✝ : Set.Pairwise ↑s fun i j => IsCoprime (g i) (g j)
a : ι
b : Finset ι
hab : ¬a ∈ b
Hind :
  ∀ (f : R[X]),
    (∀ (i : ι), i ∈ b → Monic (g i)) →
      (Set.Pairwise ↑b fun i j => IsCoprime (g i) (g j)) →
        ∃ q r, (∀ (i : ι), i ∈ b → degree (r i) < degree (g i)) ∧ ↑f / ∏ i in b, ↑(g i) = ↑q + ∑ i in b, ↑(r i) / ↑(g i)
f : R[X]
hg : ∀ (i : ι), i ∈ insert a b → Monic (g i)
hcop : Set.Pairwise ↑(insert a b) fun i j => IsCoprime (g i) (g j)
q₀ r₁ r₂ : R[X]
hdeg₁ : degree r₁ < degree (g a)
left✝ : degree r₂ < degree (∏ i in b, g i)
hf✝ : ↑f / (↑(g a) * ↑(∏ i in b, g i)) = ↑q₀ + ↑r₁ / ↑(g a) + ↑r₂ / ↑(∏ i in b, g i)
q : R[X]
r : ι → R[X]
hrdeg : ∀ (i : ι), i ∈ b → degree (r i) < degree (g i)
hf : ↑f / ↑(g a * ∏ i in b, g i) = ↑q₀ + ↑r₁ / ↑(g a) + ↑r₂ / ↑(∏ i in b, g i)
IH : ↑r₂ / ↑(∏ i in b, g i) = ↑q + ∑ i in b, ↑(r i) / ↑(g i)
x : ι
hxb : x ∈ b
⊢ ↑(r x) / ↑(g x) = ↑(if x = a then r₁ else r x) / ↑(g x)
[PROOFSTEP]
rw [if_neg]
[GOAL]
case e_a.e_a.hnc
R : Type
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : IsFractionRing R[X] K
f✝ : R[X]
ι : Type u_1
g : ι → R[X]
s : Finset ι
hg✝ : ∀ (i : ι), i ∈ s → Monic (g i)
hcop✝ : Set.Pairwise ↑s fun i j => IsCoprime (g i) (g j)
a : ι
b : Finset ι
hab : ¬a ∈ b
Hind :
  ∀ (f : R[X]),
    (∀ (i : ι), i ∈ b → Monic (g i)) →
      (Set.Pairwise ↑b fun i j => IsCoprime (g i) (g j)) →
        ∃ q r, (∀ (i : ι), i ∈ b → degree (r i) < degree (g i)) ∧ ↑f / ∏ i in b, ↑(g i) = ↑q + ∑ i in b, ↑(r i) / ↑(g i)
f : R[X]
hg : ∀ (i : ι), i ∈ insert a b → Monic (g i)
hcop : Set.Pairwise ↑(insert a b) fun i j => IsCoprime (g i) (g j)
q₀ r₁ r₂ : R[X]
hdeg₁ : degree r₁ < degree (g a)
left✝ : degree r₂ < degree (∏ i in b, g i)
hf✝ : ↑f / (↑(g a) * ↑(∏ i in b, g i)) = ↑q₀ + ↑r₁ / ↑(g a) + ↑r₂ / ↑(∏ i in b, g i)
q : R[X]
r : ι → R[X]
hrdeg : ∀ (i : ι), i ∈ b → degree (r i) < degree (g i)
hf : ↑f / ↑(g a * ∏ i in b, g i) = ↑q₀ + ↑r₁ / ↑(g a) + ↑r₂ / ↑(∏ i in b, g i)
IH : ↑r₂ / ↑(∏ i in b, g i) = ↑q + ∑ i in b, ↑(r i) / ↑(g i)
x : ι
hxb : x ∈ b
⊢ ¬x = a
[PROOFSTEP]
rintro rfl
[GOAL]
case e_a.e_a.hnc
R : Type
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : IsFractionRing R[X] K
f✝ : R[X]
ι : Type u_1
g : ι → R[X]
s : Finset ι
hg✝ : ∀ (i : ι), i ∈ s → Monic (g i)
hcop✝ : Set.Pairwise ↑s fun i j => IsCoprime (g i) (g j)
b : Finset ι
Hind :
  ∀ (f : R[X]),
    (∀ (i : ι), i ∈ b → Monic (g i)) →
      (Set.Pairwise ↑b fun i j => IsCoprime (g i) (g j)) →
        ∃ q r, (∀ (i : ι), i ∈ b → degree (r i) < degree (g i)) ∧ ↑f / ∏ i in b, ↑(g i) = ↑q + ∑ i in b, ↑(r i) / ↑(g i)
f q₀ r₁ r₂ : R[X]
left✝ : degree r₂ < degree (∏ i in b, g i)
q : R[X]
r : ι → R[X]
hrdeg : ∀ (i : ι), i ∈ b → degree (r i) < degree (g i)
IH : ↑r₂ / ↑(∏ i in b, g i) = ↑q + ∑ i in b, ↑(r i) / ↑(g i)
x : ι
hxb : x ∈ b
hab : ¬x ∈ b
hg : ∀ (i : ι), i ∈ insert x b → Monic (g i)
hcop : Set.Pairwise ↑(insert x b) fun i j => IsCoprime (g i) (g j)
hdeg₁ : degree r₁ < degree (g x)
hf✝ : ↑f / (↑(g x) * ↑(∏ i in b, g i)) = ↑q₀ + ↑r₁ / ↑(g x) + ↑r₂ / ↑(∏ i in b, g i)
hf : ↑f / ↑(g x * ∏ i in b, g i) = ↑q₀ + ↑r₁ / ↑(g x) + ↑r₂ / ↑(∏ i in b, g i)
⊢ False
[PROOFSTEP]
exact hab hxb
