awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Content (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
S : Type u_2
inst_2 : Ring S
inst_3 : IsDomain S
inst_4 : Algebra R S
inst_5 : Module.IsTorsionFree R S
p : R[X]
s : S
hpzero : p ≠ 0
hp :
  HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) p.content : S)
      ((aeval s : (a : R[X]) → S) p.primPart : S) =
    0
inst_6 : Nontrivial S
⊢ Ne.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) p.content : S) (0 : S)
have this : IsDomain R
Tactic: have : IsDomain R := { Module.nontrivial R S with }
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Content (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
S : Type u_2
inst_2 : Ring S
inst_3 : IsDomain S
inst_4 : Algebra R S
inst_5 : Module.IsTorsionFree R S
p : R[X]
s : S
hpzero : p ≠ 0
hp :
  HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) p.content : S)
      ((aeval s : (a : R[X]) → S) p.primPart : S) =
    0
inst_6 : Nontrivial S
this : IsDomain R
⊢ Ne.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) p.content : S) (0 : S)
have rwa : p.content ≠ 0
Tactic: rwa [(FaithfulSMul.algebraMap_injective R S).ne_iff' (map_zero _), Ne, content_eq_zero_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Content (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
S : Type u_2
inst_2 : Ring S
inst_3 : IsDomain S
inst_4 : Algebra R S
inst_5 : Module.IsTorsionFree R S
p : R[X]
s : S
hpzero : p ≠ 0
hp :
  HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) p.content : S)
      ((aeval s : (a : R[X]) → S) p.primPart : S) =
    0
inst_6 : Nontrivial S
this : IsDomain R
rwa : p.content ≠ 0
⊢ Ne.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) p.content : S) (0 : S)
have rwa₁ : ¬p.content = 0
Tactic: rwa [(FaithfulSMul.algebraMap_injective R S).ne_iff' (map_zero _), Ne, content_eq_zero_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Content (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
S : Type u_2
inst_2 : Ring S
inst_3 : IsDomain S
inst_4 : Algebra R S
inst_5 : Module.IsTorsionFree R S
p : R[X]
s : S
hpzero : p ≠ 0
hp :
  HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) p.content : S)
      ((aeval s : (a : R[X]) → S) p.primPart : S) =
    0
inst_6 : Nontrivial S
this : IsDomain R
rwa : p.content ≠ 0
rwa₁ : ¬p.content = 0
⊢ Ne.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) p.content : S) (0 : S)
have rwa₂ : ¬p = 0
Tactic: rwa [(FaithfulSMul.algebraMap_injective R S).ne_iff' (map_zero _), Ne, content_eq_zero_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Content (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
S : Type u_2
inst_2 : CommSemiring S
inst_3 : IsDomain S
f : R →+* S
hinj : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
p : R[X]
s : S
hpzero : p ≠ 0
hp : eval₂ f s p = 0
⊢ eval₂ f s p.primPart = 0
have hp₁ : HMul.hMul (α := S) ((f : (a : R) → S) p.content : S) (eval₂ f s p.primPart) = 0
Tactic: rw [eq_C_content_mul_primPart p, eval₂_mul, eval₂_C] at hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Content (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
S : Type u_2
inst_2 : CommSemiring S
inst_3 : IsDomain S
f : R →+* S
hinj : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
p : R[X]
s : S
hpzero : p ≠ 0
hp : HMul.hMul (α := S) ((f : (a : R) → S) p.content : S) (eval₂ f s p.primPart) = 0
⊢ eval₂ f s p.primPart = 0
have refine : Ne.{u_2 + 1} (α := S) ((f : (a : R) → S) p.content : S) (0 : S)
Tactic: refine eq_zero_of_ne_zero_of_mul_left_eq_zero ?_ hp
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Content (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
S : Type u_2
inst_2 : CommSemiring S
inst_3 : IsDomain S
f : R →+* S
hinj : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
p : R[X]
s : S
hpzero : p ≠ 0
hp : HMul.hMul (α := S) ((f : (a : R) → S) p.content : S) (eval₂ f s p.primPart) = 0
⊢ Ne.{u_2 + 1} (α := S) ((f : (a : R) → S) p.content : S) (0 : S)
have rwa : p.content ≠ 0
Tactic: rwa [hinj.ne_iff' (map_zero _), Ne, content_eq_zero_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Content (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
S : Type u_2
inst_2 : CommSemiring S
inst_3 : IsDomain S
f : R →+* S
hinj : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
p : R[X]
s : S
hpzero : p ≠ 0
hp : HMul.hMul (α := S) ((f : (a : R) → S) p.content : S) (eval₂ f s p.primPart) = 0
rwa : p.content ≠ 0
⊢ Ne.{u_2 + 1} (α := S) ((f : (a : R) → S) p.content : S) (0 : S)
have rwa₁ : ¬p.content = 0
Tactic: rwa [hinj.ne_iff' (map_zero _), Ne, content_eq_zero_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Content (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
S : Type u_2
inst_2 : CommSemiring S
inst_3 : IsDomain S
f : R →+* S
hinj : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
p : R[X]
s : S
hpzero : p ≠ 0
hp : HMul.hMul (α := S) ((f : (a : R) → S) p.content : S) (eval₂ f s p.primPart) = 0
rwa : p.content ≠ 0
rwa₁ : ¬p.content = 0
⊢ Ne.{u_2 + 1} (α := S) ((f : (a : R) → S) p.content : S) (0 : S)
have rwa₂ : ¬p = 0
Tactic: rwa [hinj.ne_iff' (map_zero _), Ne, content_eq_zero_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Content (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
a : R
p q : R[X]
h : (C : (a : R) → R[X]) a ∣ p - q
⊢ @gcd _ CommSemiring.toCommMonoidWithZero _ a p.content = @gcd _ CommSemiring.toCommMonoidWithZero _ a q.content
have rw : @gcd _ CommSemiring.toCommMonoidWithZero _ a ((Finset.range (max p.natDegree q.natDegree).succ).gcd p.coeff) =
  @gcd _ CommSemiring.toCommMonoidWithZero _ a q.content
Tactic: rw [content_eq_gcd_range_of_lt p (max p.natDegree q.natDegree).succ
      (lt_of_le_of_lt (le_max_left _ _) (Nat.lt_succ_self _))]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Content (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
a : R
p q : R[X]
h : (C : (a : R) → R[X]) a ∣ p - q
⊢ @gcd _ CommSemiring.toCommMonoidWithZero _ a ((Finset.range (max p.natDegree q.natDegree).succ).gcd p.coeff) =
    @gcd _ CommSemiring.toCommMonoidWithZero _ a q.content
have rw : @gcd _ CommSemiring.toCommMonoidWithZero _ a ((Finset.range (max p.natDegree q.natDegree).succ).gcd p.coeff) =
  @gcd _ CommSemiring.toCommMonoidWithZero _ a ((Finset.range (max p.natDegree q.natDegree).succ).gcd q.coeff)
Tactic: rw [content_eq_gcd_range_of_lt q (max p.natDegree q.natDegree).succ
      (lt_of_le_of_lt (le_max_right _ _) (Nat.lt_succ_self _))]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Content (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
a : R
p q : R[X]
h : (C : (a : R) → R[X]) a ∣ p - q
⊢ @gcd _ CommSemiring.toCommMonoidWithZero _ a ((Finset.range (max p.natDegree q.natDegree).succ).gcd p.coeff) =
    @gcd _ CommSemiring.toCommMonoidWithZero _ a ((Finset.range (max p.natDegree q.natDegree).succ).gcd q.coeff)
have h₁ : ∀ x ∈ Finset.range (max p.natDegree q.natDegree).succ, a ∣ p.coeff x - q.coeff x
Tactic: apply Finset.gcd_eq_of_dvd_sub
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Content (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
a : R
p q : R[X]
h : (C : (a : R) → R[X]) a ∣ p - q
x : ℕ
h_1 : x ∈ Finset.range (max p.natDegree q.natDegree).succ
⊢ a ∣ p.coeff x - q.coeff x
have h₁ : ∀ (w : R[X]) (hw : p - q = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) w), a ∣ p.coeff x - q.coeff x
Tactic: obtain ⟨w, hw⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Content (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
a : R
p q : R[X]
x : ℕ
h : x ∈ Finset.range (max p.natDegree q.natDegree).succ
w : R[X]
hw : p - q = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) w
⊢ a ∣ p.coeff x - q.coeff x
have h : p.coeff x - q.coeff x = a * w.coeff x
Tactic: use w.coeff x
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Content (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
a : R
p q : R[X]
x : ℕ
h : x ∈ Finset.range (max p.natDegree q.natDegree).succ
w : R[X]
hw : p - q = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) w
⊢ p.coeff x - q.coeff x = a * w.coeff x
have h : (p - q).coeff x = a * w.coeff x
Tactic: rw [← coeff_sub, hw, coeff_C_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Content (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
a : R
p q : R[X]
x : ℕ
h_1 : x ∈ Finset.range (max p.natDegree q.natDegree).succ
w : R[X]
hw : p - q = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) w
h : (p - q).coeff x = a * w.coeff x
⊢ p.coeff x - q.coeff x = a * w.coeff x
have h₁ : (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) w).coeff x = a * w.coeff x
Tactic: rw [← coeff_sub, hw, coeff_C_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Content (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
a : R
p q : R[X]
x : ℕ
h_1 : x ∈ Finset.range (max p.natDegree q.natDegree).succ
w : R[X]
hw : p - q = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) w
h : (p - q).coeff x = a * w.coeff x
h₁ : (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) w).coeff x = a * w.coeff x
⊢ p.coeff x - q.coeff x = a * w.coeff x
have h₂ : a * w.coeff x = a * w.coeff x
Tactic: rw [← coeff_sub, hw, coeff_C_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Content (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p q : R[X]
⊢ @gcd _ CommSemiring.toCommMonoidWithZero _ (p * q).eraseLead.content p.leadingCoeff =
    @gcd _ CommSemiring.toCommMonoidWithZero _ (p.eraseLead * q).content p.leadingCoeff
have rw : @gcd _ CommSemiring.toCommMonoidWithZero _ p.leadingCoeff (p * q).eraseLead.content =
  @gcd _ CommSemiring.toCommMonoidWithZero _ p.leadingCoeff (p.eraseLead * q).content
Tactic: rw [gcd_comm (content _) _, gcd_comm (content _) _]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Content (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p q : R[X]
⊢ @gcd _ CommSemiring.toCommMonoidWithZero _ p.leadingCoeff (p * q).eraseLead.content =
    @gcd _ CommSemiring.toCommMonoidWithZero _ p.leadingCoeff (p.eraseLead * q).content
have h : (C : (a : R) → R[X]) p.leadingCoeff ∣ (p * q).eraseLead - p.eraseLead * q
Tactic: apply gcd_content_eq_of_dvd_sub
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Content (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p q : R[X]
⊢ (C : (a : R) → R[X]) p.leadingCoeff ∣ (p * q).eraseLead - p.eraseLead * q
have h : (C : (a : R) → R[X]) p.leadingCoeff ∣
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X p.natDegree * q) -
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X (p * q).natDegree))
Tactic: rw [← self_sub_C_mul_X_pow, ← self_sub_C_mul_X_pow, sub_mul, sub_sub, add_comm, sub_add,
    sub_sub_cancel, leadingCoeff_mul, map_mul, mul_assoc, mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Content (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p q : R[X]
⊢ (p * q).content = p.content * q.content
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Content (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p q : R[X]
h_1 : Nontrivial R
h : ∀ (n : ℕ) (p q : R[X]), (p * q).degree < (↑n : WithBot ℕ) → (p * q).content = p.content * q.content
⊢ (p * q).content = p.content * q.content
have a : (p * q).degree < (↑(Nat.succ (↑(p * q).natDegree : ℕ)) : WithBot ℕ)
Tactic: apply h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Content (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p q : R[X]
h_1 : Nontrivial R
h : ∀ (n : ℕ) (p q : R[X]), (p * q).degree < (↑n : WithBot ℕ) → (p * q).content = p.content * q.content
a : (p * q).degree < (↑(Nat.succ (↑(p * q).natDegree : ℕ)) : WithBot ℕ)
⊢ (p * q).content = p.content * q.content
have n : ℕ
Tactic: apply h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Content (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p q : R[X]
h : Nontrivial R
⊢ (p * q).content = p.content * q.content
have suffices : ∀ (n : ℕ) (p q : R[X]), (p * q).degree < (↑n : WithBot ℕ) → (p * q).content = p.content * q.content
Tactic: suffices h :
        ∀ (n : ℕ) (p q : R[X]), (p * q).degree < n → (p * q).content = p.content * q.content by
      apply h
      apply lt_of_le_of_lt degree_le_natDegree (WithBot.coe_lt_coe.2 (Nat.lt_succ_self _))
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Content (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p_1 q_1 : R[X]
h : Nontrivial R
p q : R[X]
hpq : (p * q).degree < (↑0 : WithBot ℕ)
⊢ (p * q).content = p.content * q.content
have hpq₁ : p = 0 ∨ q = 0
Tactic: rw [Nat.cast_zero, Nat.WithBot.lt_zero_iff, degree_eq_bot, mul_eq_zero] at hpq
Cleared hypotheses: hpq
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Content (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p_1 q_1 : R[X]
h : Nontrivial R
p q : R[X]
hpq : p = 0 ∨ q = 0
⊢ (p * q).content = p.content * q.content
have zero : (0 * q).content = content 0 * q.content
Tactic: rcases hpq with (rfl | rfl)
Cleared hypotheses: p, hpq
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Content (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p_1 q_1 : R[X]
h : Nontrivial R
p q : R[X]
hpq : p = 0 ∨ q = 0
zero : (0 * q).content = content 0 * q.content
⊢ (p * q).content = p.content * q.content
have zero₁ : (p * 0).content = p.content * content 0
Tactic: rcases hpq with (rfl | rfl)
Cleared hypotheses: q, hpq
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Content (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p_1 q_1 : R[X]
h : Nontrivial R
n : ℕ
p q : R[X]
hpq : (p * q).degree < (↑n : WithBot ℕ)
⊢ (p * q).content = p.content * q.content
have succ : ∀ (n : ℕ) (ih : ∀ (p q : R[X]) (hpq : (p * q).degree < (↑n : WithBot ℕ)), (p * q).content = p.content * q.content)
  (p q : R[X]) (hpq : (p * q).degree < (↑(n + 1) : WithBot ℕ)), (p * q).content = p.content * q.content
Tactic: induction n generalizing p q with
    | zero =>
      rw [Nat.cast_zero, Nat.WithBot.lt_zero_iff, degree_eq_bot, mul_eq_zero] at hpq
      rcases hpq with (rfl | rfl) <;> simp
    | succ n ih => ?_
Cleared hypotheses: n, p, q, hpq
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Content (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p_1 q_1 : R[X]
h : Nontrivial R
n : ℕ
ih : ∀ (p q : R[X]) (hpq : (p * q).degree < (↑n : WithBot ℕ)), (p * q).content = p.content * q.content
p q : R[X]
hpq : (p * q).degree < (↑(n + 1) : WithBot ℕ)
⊢ (p * q).content = p.content * q.content
have pos : ∀ (p0 : p = 0), (p * q).content = p.content * q.content
Tactic: by_cases p0 : p = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Content (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p_1 q_1 : R[X]
h : Nontrivial R
n : ℕ
ih : ∀ (p q : R[X]) (hpq : (p * q).degree < (↑n : WithBot ℕ)), (p * q).content = p.content * q.content
p q : R[X]
hpq : (p * q).degree < (↑(n + 1) : WithBot ℕ)
pos : ∀ (p0 : p = 0), (p * q).content = p.content * q.content
⊢ (p * q).content = p.content * q.content
have neg : ∀ (p0 : ¬p = 0), (p * q).content = p.content * q.content
Tactic: by_cases p0 : p = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Content (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p_1 q_1 : R[X]
h : Nontrivial R
n : ℕ
ih : ∀ (p q : R[X]) (hpq : (p * q).degree < (↑n : WithBot ℕ)), (p * q).content = p.content * q.content
p q : R[X]
hpq : (p * q).degree < (↑(n + 1) : WithBot ℕ)
p0 : ¬p = 0
⊢ (p * q).content = p.content * q.content
have pos : ∀ (q0 : q = 0), (p * q).content = p.content * q.content
Tactic: by_cases q0 : q = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Content (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p_1 q_1 : R[X]
h : Nontrivial R
n : ℕ
ih : ∀ (p q : R[X]) (hpq : (p * q).degree < (↑n : WithBot ℕ)), (p * q).content = p.content * q.content
p q : R[X]
hpq : (p * q).degree < (↑(n + 1) : WithBot ℕ)
p0 : ¬p = 0
pos : ∀ (q0 : q = 0), (p * q).content = p.content * q.content
⊢ (p * q).content = p.content * q.content
have neg : ∀ (q0 : ¬q = 0), (p * q).content = p.content * q.content
Tactic: by_cases q0 : q = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Content (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p_1 q_1 : R[X]
h : Nontrivial R
n : ℕ
ih : ∀ (p q : R[X]) (hpq : (p * q).degree < (↑n : WithBot ℕ)), (p * q).content = p.content * q.content
p q : R[X]
hpq : (p * q).degree < (↑(n + 1) : WithBot ℕ)
p0 : ¬p = 0
q0 : ¬q = 0
⊢ (p * q).content = p.content * q.content
have hpq₁ : (p * q).degree < (↑n : WithBot ℕ) ∨ p.natDegree + q.natDegree = n
Tactic: rw [degree_eq_natDegree (mul_ne_zero p0 q0), Nat.cast_lt,
      Nat.lt_succ_iff_lt_or_eq, ← Nat.cast_lt (α := WithBot ℕ),
      ← degree_eq_natDegree (mul_ne_zero p0 q0), natDegree_mul p0 q0] at hpq
Cleared hypotheses: hpq, p0, q0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Content (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p_1 q_1 : R[X]
h : Nontrivial R
n : ℕ
ih : ∀ (p q : R[X]) (hpq : (p * q).degree < (↑n : WithBot ℕ)), (p * q).content = p.content * q.content
p q : R[X]
hpq : (p * q).degree < (↑n : WithBot ℕ) ∨ p.natDegree + q.natDegree = n
p0 : ¬p = 0
q0 : ¬q = 0
⊢ (p * q).content = p.content * q.content
have neg : ∀ (hlt : (p * q).degree < (↑n : WithBot ℕ)), (p * q).content = p.content * q.content
Tactic: rcases hpq with (hlt | heq)
Cleared hypotheses: hpq
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Content (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p_1 q_1 : R[X]
h : Nontrivial R
n : ℕ
ih : ∀ (p q : R[X]) (hpq : (p * q).degree < (↑n : WithBot ℕ)), (p * q).content = p.content * q.content
p q : R[X]
hpq : (p * q).degree < (↑n : WithBot ℕ) ∨ p.natDegree + q.natDegree = n
p0 : ¬p = 0
q0 : ¬q = 0
neg : ∀ (hlt : (p * q).degree < (↑n : WithBot ℕ)), (p * q).content = p.content * q.content
⊢ (p * q).content = p.content * q.content
have neg₁ : ∀ (heq : p.natDegree + q.natDegree = n), (p * q).content = p.content * q.content
Tactic: rcases hpq with (hlt | heq)
Cleared hypotheses: hpq
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Content (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p_1 q_1 : R[X]
h : Nontrivial R
n : ℕ
ih : ∀ (p q : R[X]) (hpq : (p * q).degree < (↑n : WithBot ℕ)), (p * q).content = p.content * q.content
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : p.natDegree + q.natDegree = n
⊢ (p * q).content = p.content * q.content
have heq₁ : p.primPart.degree + q.primPart.degree = (↑n : WithBot ℕ)
Tactic: rw [← p.natDegree_primPart, ← q.natDegree_primPart, ← Nat.cast_inj (R := WithBot ℕ),
      Nat.cast_add, ← degree_eq_natDegree p.primPart_ne_zero,
      ← degree_eq_natDegree q.primPart_ne_zero] at heq
Cleared hypotheses: heq
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Content (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p_1 q_1 : R[X]
h : Nontrivial R
n : ℕ
ih : ∀ (p q : R[X]) (hpq : (p * q).degree < (↑n : WithBot ℕ)), (p * q).content = p.content * q.content
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : p.primPart.degree + q.primPart.degree = (↑n : WithBot ℕ)
⊢ (p * q).content = p.content * q.content
have neg : (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.content : R[X]) p.primPart *
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.content : R[X]) q.primPart).content =
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.content : R[X]) p.primPart).content *
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.content : R[X]) q.primPart).content
Tactic: rw [p.eq_C_content_mul_primPart, q.eq_C_content_mul_primPart]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Content (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p_1 q_1 : R[X]
h_1 : Nontrivial R
n : ℕ
ih : ∀ (p q : R[X]) (hpq : (p * q).degree < (↑n : WithBot ℕ)), (p * q).content = p.content * q.content
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : p.primPart.degree + q.primPart.degree = (↑n : WithBot ℕ)
h : (q.primPart * p.primPart).content = 1
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.content : R[X]) p.primPart *
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.content : R[X]) q.primPart).content =
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.content : R[X]) p.primPart).content *
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.content : R[X]) q.primPart).content
have rw : (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.content : R[X])
      (p.primPart * HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.content : R[X]) q.primPart)).content =
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.content : R[X]) p.primPart).content *
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.content : R[X]) q.primPart).content
Tactic: rw [mul_assoc, content_C_mul, content_C_mul, mul_comm p.primPart, mul_assoc, content_C_mul,
        content_C_mul, h, mul_one, content_primPart, content_primPart, mul_one, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Content (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p_1 q_1 : R[X]
h_1 : Nontrivial R
n : ℕ
ih : ∀ (p q : R[X]) (hpq : (p * q).degree < (↑n : WithBot ℕ)), (p * q).content = p.content * q.content
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : p.primPart.degree + q.primPart.degree = (↑n : WithBot ℕ)
h : (q.primPart * p.primPart).content = 1
rw :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.content : R[X])
        (p.primPart * HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.content : R[X]) q.primPart)).content =
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.content : R[X]) p.primPart).content *
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.content : R[X]) q.primPart).content
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.content : R[X]) p.primPart *
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.content : R[X]) q.primPart).content =
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.content : R[X]) p.primPart).content *
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.content : R[X]) q.primPart).content
have rw₁ : HMul.hMul (α := R) ((normalize : (a : R) → R) p.content : R)
    (p.primPart * HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.content : R[X]) q.primPart).content =
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.content : R[X]) p.primPart).content *
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.content : R[X]) q.primPart).content
Tactic: rw [mul_assoc, content_C_mul, content_C_mul, mul_comm p.primPart, mul_assoc, content_C_mul,
        content_C_mul, h, mul_one, content_primPart, content_primPart, mul_one, mul_one]