[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


[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
a b : α
src✝ : αᵒᵈ ≃ α := ofDual
⊢ ∀ {a b : αᵒᵈ},
    Adj (hasse α)
        (↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
              right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
          a)
        (↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
              right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
          b) ↔
      Adj (hasse αᵒᵈ) a b
[PROOFSTEP]
simp [or_comm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
⊢ hasse (α × β) = hasse α □ hasse β
[PROOFSTEP]
ext x y
[GOAL]
case Adj.h.h.a
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
x y : α × β
⊢ Adj (hasse (α × β)) x y ↔ Adj (hasse α □ hasse β) x y
[PROOFSTEP]
simp_rw [boxProd_adj, hasse_adj, Prod.covby_iff, or_and_right, @eq_comm _ y.1, @eq_comm _ y.2, or_or_or_comm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
a b : α
⊢ Reachable (hasse α) a b
[PROOFSTEP]
rw [reachable_iff_reflTransGen]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
a b : α
⊢ ReflTransGen (hasse α).Adj a b
[PROOFSTEP]
exact
  reflTransGen_of_succ _ (fun c hc => Or.inl <| covby_succ_of_not_isMax hc.2.not_isMax) fun c hc =>
    Or.inr <| covby_succ_of_not_isMax hc.2.not_isMax
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
a b : α
⊢ Reachable (hasse α) a b
[PROOFSTEP]
rw [reachable_iff_reflTransGen, ← reflTransGen_swap]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
a b : α
⊢ ReflTransGen (Function.swap (hasse α).Adj) b a
[PROOFSTEP]
exact
  reflTransGen_of_pred _ (fun c hc => Or.inl <| pred_covby_of_not_isMin hc.1.not_isMin) fun c hc =>
    Or.inr <| pred_covby_of_not_isMin hc.1.not_isMin


[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasShift C ℤ
X : C
X✝ Y✝ : Triangle C
f : X✝ ⟶ Y✝
⊢ (Triangle.rotate X✝).mor₃ ≫ (shiftFunctor C 1).map f.hom₂ = (shiftFunctor C 1).map f.hom₁ ≫ (Triangle.rotate Y✝).mor₃
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasShift C ℤ
X : C
X✝ Y✝ : Triangle C
f : X✝ ⟶ Y✝
⊢ (-(shiftFunctor C 1).map X✝.mor₁) ≫ (shiftFunctor C 1).map f.hom₂ =
    (shiftFunctor C 1).map f.hom₁ ≫ (-(shiftFunctor C 1).map Y✝.mor₁)
[PROOFSTEP]
simp only [comp_neg, neg_comp, ← Functor.map_comp, f.comm₁]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasShift C ℤ
X : C
X✝ Y✝ : Triangle C
f : X✝ ⟶ Y✝
⊢ (Triangle.invRotate X✝).mor₁ ≫ f.hom₁ = (shiftFunctor C (-1)).map f.hom₃ ≫ (Triangle.invRotate Y✝).mor₁
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasShift C ℤ
X : C
X✝ Y✝ : Triangle C
f : X✝ ⟶ Y✝
⊢ (-(shiftFunctor C (-1)).map X✝.mor₃ ≫ NatTrans.app (shiftFunctorCompIsoId C 1 (-1) (_ : 1 + -1 = 0)).hom X✝.obj₁) ≫
      f.hom₁ =
    (shiftFunctor C (-1)).map f.hom₃ ≫
      (-(shiftFunctor C (-1)).map Y✝.mor₃ ≫ NatTrans.app (shiftFunctorCompIsoId C 1 (-1) (_ : 1 + -1 = 0)).hom Y✝.obj₁)
[PROOFSTEP]
simp only [neg_comp, assoc, comp_neg, neg_inj, ← Functor.map_comp_assoc, ← f.comm₃]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasShift C ℤ
X : C
X✝ Y✝ : Triangle C
f : X✝ ⟶ Y✝
⊢ (shiftFunctor C (-1)).map X✝.mor₃ ≫
      NatTrans.app (shiftFunctorCompIsoId C 1 (-1) (_ : 1 + -1 = 0)).hom X✝.obj₁ ≫ f.hom₁ =
    (shiftFunctor C (-1)).map (X✝.mor₃ ≫ (shiftFunctor C 1).map f.hom₁) ≫
      NatTrans.app (shiftFunctorCompIsoId C 1 (-1) (_ : 1 + -1 = 0)).hom Y✝.obj₁
[PROOFSTEP]
rw [Functor.map_comp, assoc]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasShift C ℤ
X : C
X✝ Y✝ : Triangle C
f : X✝ ⟶ Y✝
⊢ (shiftFunctor C (-1)).map X✝.mor₃ ≫
      NatTrans.app (shiftFunctorCompIsoId C 1 (-1) (_ : 1 + -1 = 0)).hom X✝.obj₁ ≫ f.hom₁ =
    (shiftFunctor C (-1)).map X✝.mor₃ ≫
      (shiftFunctor C (-1)).map ((shiftFunctor C 1).map f.hom₁) ≫
        NatTrans.app (shiftFunctorCompIsoId C 1 (-1) (_ : 1 + -1 = 0)).hom Y✝.obj₁
[PROOFSTEP]
erw [← NatTrans.naturality]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasShift C ℤ
X : C
X✝ Y✝ : Triangle C
f : X✝ ⟶ Y✝
⊢ (shiftFunctor C (-1)).map X✝.mor₃ ≫
      (shiftFunctor C 1 ⋙ shiftFunctor C (-1)).map f.1 ≫
        NatTrans.app (shiftFunctorCompIsoId C 1 (-1) (_ : 1 + -1 = 0)).hom Y✝.obj₁ =
    (shiftFunctor C (-1)).map X✝.mor₃ ≫
      (shiftFunctor C (-1)).map ((shiftFunctor C 1).map f.hom₁) ≫
        NatTrans.app (shiftFunctorCompIsoId C 1 (-1) (_ : 1 + -1 = 0)).hom Y✝.obj₁
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasShift C ℤ
X : C
X✝ Y✝ : Triangle C
f : X✝ ⟶ Y✝
⊢ (Triangle.invRotate X✝).mor₃ ≫ (shiftFunctor C 1).map ((shiftFunctor C (-1)).map f.hom₃) =
    f.hom₂ ≫ (Triangle.invRotate Y✝).mor₃
[PROOFSTEP]
erw [← reassoc_of% f.comm₂, Category.assoc, ← NatTrans.naturality]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasShift C ℤ
X : C
X✝ Y✝ : Triangle C
f : X✝ ⟶ Y✝
⊢ X✝.mor₂ ≫ (𝟭 C).map f.hom₃ ≫ NatTrans.app (shiftEquiv C 1).counitIso.inv Y✝.obj₃ =
    X✝.mor₂ ≫ f.hom₃ ≫ NatTrans.app (shiftEquiv C 1).counitIso.inv Y✝.3
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
X : C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
⊢ IsEquivalence (rotate C)
[PROOFSTEP]
change IsEquivalence (triangleRotation C).functor
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
X : C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
⊢ IsEquivalence (triangleRotation C).functor
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
X : C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
⊢ IsEquivalence (invRotate C)
[PROOFSTEP]
change IsEquivalence (triangleRotation C).inverse
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
X : C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
⊢ IsEquivalence (triangleRotation C).inverse
[PROOFSTEP]
infer_instance