awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
⊢ (h.unit⁻¹ • p).Monic
have rw : (↑h.unit⁻¹ : R) • p.leadingCoeff = 1
Tactic: rw [Monic.def, leadingCoeff_smul_of_smul_regular _ (isSMulRegular_of_group _), Units.smul_def]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
⊢ p * q = 0 ↔ q = 0
have mp : p * q = 0 → q = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
mp : p * q = 0 → q = 0
⊢ p * q = 0 ↔ q = 0
have mpr : q = 0 → p * q = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (hypothesis)
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
hp : p * q = 0
⊢ q = 0
have hp₁ : h.unit⁻¹ • (p * q) = 0
Tactic: rw [← smul_eq_zero_iff_eq h.unit⁻¹] at hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
hp : h.unit⁻¹ • (p * q) = 0
⊢ h.unit⁻¹ • (p * q) = h.unit⁻¹ • p * q
have a : ∀ (n : ℕ), (h.unit⁻¹ • (p * q)).coeff n = (h.unit⁻¹ • p * q).coeff n
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
hp : h.unit⁻¹ • (p * q) = 0
n : ℕ
⊢ (h.unit⁻¹ • (p * q)).coeff n = (h.unit⁻¹ • p * q).coeff n
have a : Eq.{u + 1} (α := R) (∑ i ∈ @antidiagonal _ Nat.instAddMonoid _ n, (↑h.unit⁻¹ : R) * (p.coeff i.1 * q.coeff i.2))
  (∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n, (↑h.unit⁻¹ : R) * p.coeff x.1 * q.coeff x.2)
Tactic: simp only [Units.smul_def, coeff_smul, coeff_mul, smul_eq_mul, mul_sum]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
hp : h.unit⁻¹ • (p * q) = 0
n : ℕ
⊢ Eq.{u + 1} (α := R) (∑ i ∈ @antidiagonal _ Nat.instAddMonoid _ n, (↑h.unit⁻¹ : R) * (p.coeff i.1 * q.coeff i.2))
    (∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n, (↑h.unit⁻¹ : R) * p.coeff x.1 * q.coeff x.2)
have a : ∀ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
  (↑h.unit⁻¹ : R) * (p.coeff x.1 * q.coeff x.2) = (↑h.unit⁻¹ : R) * p.coeff x.1 * q.coeff x.2
Tactic: refine sum_congr rfl fun x _ => ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
hp : h.unit⁻¹ • (p * q) = 0
n : ℕ
x : ℕ × ℕ
h_1 : x ∈ @antidiagonal _ Nat.instAddMonoid _ n
⊢ (↑h.unit⁻¹ : R) * (p.coeff x.1 * q.coeff x.2) = (↑h.unit⁻¹ : R) * p.coeff x.1 * q.coeff x.2
have a : (↑h.unit⁻¹ : R) * p.coeff x.1 * q.coeff x.2 = (↑h.unit⁻¹ : R) * p.coeff x.1 * q.coeff x.2
Tactic: rw [← mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (hypothesis)
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
hp : h.unit⁻¹ • (p * q) = 0
⊢ q = 0
have this : h.unit⁻¹ • (p * q) = h.unit⁻¹ • p * q
Tactic: have : h.unit⁻¹ • (p * q) = h.unit⁻¹ • p * q := by
      ext
      simp only [Units.smul_def, coeff_smul, coeff_mul, smul_eq_mul, mul_sum]
      refine sum_congr rfl fun x _ => ?_
      rw [← mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
hp : h.unit⁻¹ • (p * q) = 0
this : h.unit⁻¹ • (p * q) = h.unit⁻¹ • p * q
⊢ q = 0
have mp : ∀ (hp : h.unit⁻¹ • p * q = 0) (this : h.unit⁻¹ • (p * q) = h.unit⁻¹ • p * q), (h.unit⁻¹ • p).Monic
Tactic: rwa [this, Monic.mul_right_eq_zero_iff] at hp
Cleared hypotheses: hp, this
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
⊢ q * p = 0 ↔ q = 0
have mp : q * p = 0 → q = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
mp : q * p = 0 → q = 0
⊢ q * p = 0 ↔ q = 0
have mpr : q = 0 → q * p = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (hypothesis)
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
hp : q * p = 0
⊢ q = 0
have hp₁ : Eq.{u + 1} (α := R[X])
  ((fun (x : R[X]) ↦ HMul.hMul (β := R[X]) x ((C : (a : R) → R[X]) (↑h.unit⁻¹ : R) : R[X])) (q * p))
  ((fun (x : R[X]) ↦ HMul.hMul (β := R[X]) x ((C : (a : R) → R[X]) (↑h.unit⁻¹ : R) : R[X])) 0)
Tactic: replace hp := congr_arg (· * C ↑h.unit⁻¹) hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (hypothesis)
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
hp :
  Eq.{u + 1} (α := R[X])
    ((fun (x : R[X]) ↦ HMul.hMul (β := R[X]) x ((C : (a : R) → R[X]) (↑h.unit⁻¹ : R) : R[X])) (q * p))
    ((fun (x : R[X]) ↦ HMul.hMul (β := R[X]) x ((C : (a : R) → R[X]) (↑h.unit⁻¹ : R) : R[X])) 0)
⊢ q = 0
have hp₁ : HMul.hMul (β := R[X]) (q * p) ((C : (a : R) → R[X]) (↑h.unit⁻¹ : R) : R[X]) = 0
Tactic: simp only [zero_mul] at hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
hp : HMul.hMul (β := R[X]) (q * p) ((C : (a : R) → R[X]) (↑h.unit⁻¹ : R) : R[X]) = 0
⊢ q = 0
have mp : ∀ (hp : q * HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) (↑h.unit⁻¹ : R) : R[X]) = 0),
  (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) (↑h.unit⁻¹ : R) : R[X])).Monic
Tactic: rwa [mul_assoc, Monic.mul_left_eq_zero_iff] at hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
hp : q * HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) (↑h.unit⁻¹ : R) : R[X]) = 0
⊢ (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) (↑h.unit⁻¹ : R) : R[X])).Monic
have mp : p.leadingCoeff * (↑h.unit⁻¹ : R) = 1
Tactic: refine monic_mul_C_of_leadingCoeff_mul_eq_one ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
⊢ 0 * p = 0
have mpr : Eq.{u + 1} (α := R[X]) 0 0
Tactic: rw [zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monomial (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
i j : ℕ
⊢ Eq.{u + 1} (α := R[X]) ((monomial i : (a : R) → R[X]) 1) ((monomial j : (a : R) → R[X]) 1) ↔ i = j
have simp_rw : Eq.{u + 1} (α := AddMonoidAlgebra R ℕ) (AddMonoidAlgebra.single i 1) (AddMonoidAlgebra.single j 1) ↔ i = j
Tactic: simp_rw [← ofFinsupp_single, ofFinsupp.injEq]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monomial (goal)
Goal:
R : Type u
inst : Semiring R
f : R[X]
⊢ f.support.card ≤ 1 ↔ ∃ (n : ℕ) (a : R), f = (monomial n : (a : R) → R[X]) a
have mp : f.support.card ≤ 1 → ∃ (n : ℕ) (a : R), f = (monomial n : (a : R) → R[X]) a
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monomial (goal)
Goal:
R : Type u
inst : Semiring R
f : R[X]
mp : f.support.card ≤ 1 → ∃ (n : ℕ) (a : R), f = (monomial n : (a : R) → R[X]) a
⊢ f.support.card ≤ 1 ↔ ∃ (n : ℕ) (a : R), f = (monomial n : (a : R) → R[X]) a
have mpr : (∃ (n : ℕ) (a : R), f = (monomial n : (a : R) → R[X]) a) → f.support.card ≤ 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monomial (hypothesis)
Goal:
R : Type u
inst : Semiring R
f : R[X]
H : f.support.card ≤ 1
⊢ ∃ (n : ℕ) (a : R), f = (monomial n : (a : R) → R[X]) a
have H₁ : ∃ (x : ℕ), f.support ⊆ {x}
Tactic: rw [Finset.card_le_one_iff_subset_singleton] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monomial (goal)
Goal:
R : Type u
inst : Semiring R
f : R[X]
H : ∃ (x : ℕ), f.support ⊆ {x}
⊢ ∃ (n : ℕ) (a : R), f = (monomial n : (a : R) → R[X]) a
have mp : ∀ (n : ℕ) (hn : f.support ⊆ {n}), ∃ (n : ℕ) (a : R), f = (monomial n : (a : R) → R[X]) a
Tactic: rcases H with ⟨n, hn⟩
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monomial (goal)
Goal:
R : Type u
inst : Semiring R
f : R[X]
n : ℕ
hn : f.support ⊆ {n}
⊢ ∃ (n : ℕ) (a : R), f = (monomial n : (a : R) → R[X]) a
have mp : f = (monomial n : (a : R) → R[X]) (f.coeff n)
Tactic: refine ⟨n, f.coeff n, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monomial (goal)
Goal:
R : Type u
inst : Semiring R
f : R[X]
n : ℕ
hn : f.support ⊆ {n}
⊢ f = (monomial n : (a : R) → R[X]) (f.coeff n)
have mp : ∀ (i : ℕ), f.coeff i = coeff ((monomial n : (a : R) → R[X]) (f.coeff n)) i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monomial (goal)
Goal:
R : Type u
inst : Semiring R
f : R[X]
n : ℕ
hn : f.support ⊆ {n}
i : ℕ
⊢ f.coeff i = coeff ((monomial n : (a : R) → R[X]) (f.coeff n)) i
have pos : ∀ (hi : i = n), f.coeff i = coeff ((monomial n : (a : R) → R[X]) (f.coeff n)) i
Tactic: by_cases hi : i = n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monomial (goal)
Goal:
R : Type u
inst : Semiring R
f : R[X]
n : ℕ
hn : f.support ⊆ {n}
i : ℕ
pos : ∀ (hi : i = n), f.coeff i = coeff ((monomial n : (a : R) → R[X]) (f.coeff n)) i
⊢ f.coeff i = coeff ((monomial n : (a : R) → R[X]) (f.coeff n)) i
have neg : ∀ (hi : ¬i = n), f.coeff i = coeff ((monomial n : (a : R) → R[X]) (f.coeff n)) i
Tactic: by_cases hi : i = n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monomial (goal)
Goal:
R : Type u
inst : Semiring R
f : R[X]
n : ℕ
hn : f.support ⊆ {n}
i : ℕ
hi : ¬i = n
⊢ f.coeff i = 0
have rw : i ∉ f.support
Tactic: rw [← notMem_support_iff]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monomial (hypothesis)
Goal:
R : Type u
inst : Semiring R
f : R[X]
n : ℕ
hn : f.support ⊆ {n}
i : ℕ
hi : ¬i = n
⊢ f.coeff i = coeff ((monomial n : (a : R) → R[X]) (f.coeff n)) i
have this : f.coeff i = 0
Tactic: have : f.coeff i = 0 := by
        rw [← notMem_support_iff]
        exact fun hi' => hi (Finset.mem_singleton.1 (hn hi'))
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monomial (goal)
Goal:
R : Type u
inst : Semiring R
n : ℕ
a : R
⊢ (support.{u} (R := R) ((monomial n : (a : R) → R[X]) a)).card ≤ Finset.card (α := ℕ) {n}
have mpr : support.{u} (R := R) ((monomial n : (a : R) → R[X]) a) ⊆ {n}
Tactic: apply Finset.card_le_card
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monomial (hypothesis)
Goal:
R : Type u
inst : Semiring R
S : Type u_1
inst_1 : Semiring S
f g : RingHom.{u, u_1} R[X] S
h₁ :
  ∀ (a : R),
    Eq.{u_1 + 1} (α := S) ((f : (a : R[X]) → S) ((C : (a : R) → R[X]) a : R[X]) : S)
      ((g : (a : R[X]) → S) ((C : (a : R) → R[X]) a : R[X]) : S)
h₂ : Eq.{u_1 + 1} (α := S) ((f : (a : R[X]) → S) X : S) ((g : (a : R[X]) → S) X : S)
⊢ f = g
have hf' : let f' := f.comp (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)));
f' = f.comp (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
Tactic: set f' := f.comp (toFinsuppIso R).symm.toRingHom with hf'
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monomial (hypothesis)
Goal:
R : Type u
inst : Semiring R
S : Type u_1
inst_1 : Semiring S
f g : RingHom.{u, u_1} R[X] S
h₁ :
  ∀ (a : R),
    Eq.{u_1 + 1} (α := S) ((f : (a : R[X]) → S) ((C : (a : R) → R[X]) a : R[X]) : S)
      ((g : (a : R[X]) → S) ((C : (a : R) → R[X]) a : R[X]) : S)
h₂ : Eq.{u_1 + 1} (α := S) ((f : (a : R[X]) → S) X : S) ((g : (a : R[X]) → S) X : S)
f' : RingHom.{u, u_1} (AddMonoidAlgebra R ℕ) S := f.comp (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hf' : f' = f.comp (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
⊢ f = g
have hg' : let g' := g.comp (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)));
g' = g.comp (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
Tactic: set g' := g.comp (toFinsuppIso R).symm.toRingHom with hg'
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monomial (goal)
Goal:
R : Type u
inst : Semiring R
S : Type u_1
inst_1 : Semiring S
f g : RingHom.{u, u_1} R[X] S
h₁ :
  ∀ (a : R),
    Eq.{u_1 + 1} (α := S) ((f : (a : R[X]) → S) ((C : (a : R) → R[X]) a : R[X]) : S)
      ((g : (a : R[X]) → S) ((C : (a : R) → R[X]) a : R[X]) : S)
h₂ : Eq.{u_1 + 1} (α := S) ((f : (a : R[X]) → S) X : S) ((g : (a : R[X]) → S) X : S)
f' : RingHom.{u, u_1} (AddMonoidAlgebra R ℕ) S := f.comp (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hf' : f' = f.comp (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
g' : RingHom.{u, u_1} (AddMonoidAlgebra R ℕ) S := g.comp (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hg' : g' = g.comp (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
⊢ f' = g'
have h₃ : ∀ (x : R),
  Eq.{u_1 + 1} (α := S) ((f'.comp AddMonoidAlgebra.singleZeroRingHom : (a : R) → S) x : S)
    ((g'.comp AddMonoidAlgebra.singleZeroRingHom : (a : R) → S) x : S)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monomial (goal)
Goal:
R : Type u
inst : Semiring R
S : Type u_1
inst_1 : Semiring S
f g : RingHom.{u, u_1} R[X] S
h₁ :
  ∀ (a : R),
    Eq.{u_1 + 1} (α := S) ((f : (a : R[X]) → S) ((C : (a : R) → R[X]) a : R[X]) : S)
      ((g : (a : R[X]) → S) ((C : (a : R) → R[X]) a : R[X]) : S)
h₂ : Eq.{u_1 + 1} (α := S) ((f : (a : R[X]) → S) X : S) ((g : (a : R[X]) → S) X : S)
f' : RingHom.{u, u_1} (AddMonoidAlgebra R ℕ) S := f.comp (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hf' : f' = f.comp (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
g' : RingHom.{u, u_1} (AddMonoidAlgebra R ℕ) S := g.comp (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hg' : g' = g.comp (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
h₃ :
  ∀ (x : R),
    Eq.{u_1 + 1} (α := S) ((f'.comp AddMonoidAlgebra.singleZeroRingHom : (a : R) → S) x : S)
      ((g'.comp AddMonoidAlgebra.singleZeroRingHom : (a : R) → S) x : S)
⊢ f' = g'
have h_of : Eq (α := S)
  ((MonoidHom.comp (↑f' : AddMonoidAlgebra R ℕ →* S) (AddMonoidAlgebra.of R ℕ) : (a : Multiplicative ℕ) → S)
      ((Multiplicative.ofAdd : (a : ℕ) → Multiplicative ℕ) 1 : Multiplicative ℕ) :
    S)
  ((MonoidHom.comp (↑g' : AddMonoidAlgebra R ℕ →* S) (AddMonoidAlgebra.of R ℕ) : (a : Multiplicative ℕ) → S)
      ((Multiplicative.ofAdd : (a : ℕ) → Multiplicative ℕ) 1 : Multiplicative ℕ) :
    S)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monomial (hypothesis)
Goal:
R : Type u
inst : Semiring R
S : Type u_1
inst_1 : Semiring S
f g : RingHom.{u, u_1} R[X] S
h₁ :
  ∀ (a : R),
    Eq.{u_1 + 1} (α := S) ((f : (a : R[X]) → S) ((C : (a : R) → R[X]) a : R[X]) : S)
      ((g : (a : R[X]) → S) ((C : (a : R) → R[X]) a : R[X]) : S)
h₂ : Eq.{u_1 + 1} (α := S) ((f : (a : R[X]) → S) X : S) ((g : (a : R[X]) → S) X : S)
f' : RingHom.{u, u_1} (AddMonoidAlgebra R ℕ) S := f.comp (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hf' : f' = f.comp (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
g' : RingHom.{u, u_1} (AddMonoidAlgebra R ℕ) S := g.comp (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hg' : g' = g.comp (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
⊢ f = g
have A : f' = g'
Tactic: have A : f' = g' := by
    ext
    · simp [f', g', h₁, RingEquiv.toRingHom_eq_coe]
    simpa using h₂
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monomial (goal)
Goal:
R : Type u
inst : Semiring R
S : Type u_1
inst_1 : Semiring S
f g : RingHom.{u, u_1} R[X] S
h₁ :
  ∀ (a : R),
    Eq.{u_1 + 1} (α := S) ((f : (a : R[X]) → S) ((C : (a : R) → R[X]) a : R[X]) : S)
      ((g : (a : R[X]) → S) ((C : (a : R) → R[X]) a : R[X]) : S)
h₂ : Eq.{u_1 + 1} (α := S) ((f : (a : R[X]) → S) X : S) ((g : (a : R[X]) → S) X : S)
f' : RingHom.{u, u_1} (AddMonoidAlgebra R ℕ) S := f.comp (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hf' : f' = f.comp (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
g' : RingHom.{u, u_1} (AddMonoidAlgebra R ℕ) S := g.comp (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hg' : g' = g.comp (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
A : f' = g'
⊢ f = f'.comp (↑(toFinsuppIso R) : R[X] →+* AddMonoidAlgebra R ℕ)
have rw : f =
  f.comp
    (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
      (↑(toFinsuppIso R) : R[X] →+* AddMonoidAlgebra R ℕ))
Tactic: rw [hf', RingHom.comp_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monomial (goal)
Goal:
R : Type u
inst : Semiring R
S : Type u_1
inst_1 : Semiring S
f g : RingHom.{u, u_1} R[X] S
h₁ :
  ∀ (a : R),
    Eq.{u_1 + 1} (α := S) ((f : (a : R[X]) → S) ((C : (a : R) → R[X]) a : R[X]) : S)
      ((g : (a : R[X]) → S) ((C : (a : R) → R[X]) a : R[X]) : S)
h₂ : Eq.{u_1 + 1} (α := S) ((f : (a : R[X]) → S) X : S) ((g : (a : R[X]) → S) X : S)
f' : RingHom.{u, u_1} (AddMonoidAlgebra R ℕ) S := f.comp (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hf' : f' = f.comp (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
g' : RingHom.{u, u_1} (AddMonoidAlgebra R ℕ) S := g.comp (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hg' : g' = g.comp (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
A : f' = g'
⊢ f =
    f.comp
      (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
        (↑(toFinsuppIso R) : R[X] →+* AddMonoidAlgebra R ℕ))
have a : ∀ (x : R[X]),
  Eq.{u_1 + 1} (α := S) ((f : (a : R[X]) → S) x : S)
    ((f.comp
            (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
              (↑(toFinsuppIso R) : R[X] →+* AddMonoidAlgebra R ℕ)) :
          (a : R[X]) → S)
        x :
      S)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monomial (hypothesis)
Goal:
R : Type u
inst : Semiring R
S : Type u_1
inst_1 : Semiring S
f g : RingHom.{u, u_1} R[X] S
h₁ :
  ∀ (a : R),
    Eq.{u_1 + 1} (α := S) ((f : (a : R[X]) → S) ((C : (a : R) → R[X]) a : R[X]) : S)
      ((g : (a : R[X]) → S) ((C : (a : R) → R[X]) a : R[X]) : S)
h₂ : Eq.{u_1 + 1} (α := S) ((f : (a : R[X]) → S) X : S) ((g : (a : R[X]) → S) X : S)
f' : RingHom.{u, u_1} (AddMonoidAlgebra R ℕ) S := f.comp (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hf' : f' = f.comp (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
g' : RingHom.{u, u_1} (AddMonoidAlgebra R ℕ) S := g.comp (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hg' : g' = g.comp (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
A : f' = g'
⊢ f = g
have B : f = f'.comp (↑(toFinsuppIso R) : R[X] →+* AddMonoidAlgebra R ℕ)
Tactic: have B : f = f'.comp (toFinsuppIso R) := by
    rw [hf', RingHom.comp_assoc]
    ext x
    simp only [RingEquiv.toRingHom_eq_coe, RingEquiv.symm_apply_apply, Function.comp_apply,
      RingHom.coe_comp, RingEquiv.coe_toRingHom]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monomial (goal)
Goal:
R : Type u
inst : Semiring R
S : Type u_1
inst_1 : Semiring S
f g : RingHom.{u, u_1} R[X] S
h₁ :
  ∀ (a : R),
    Eq.{u_1 + 1} (α := S) ((f : (a : R[X]) → S) ((C : (a : R) → R[X]) a : R[X]) : S)
      ((g : (a : R[X]) → S) ((C : (a : R) → R[X]) a : R[X]) : S)
h₂ : Eq.{u_1 + 1} (α := S) ((f : (a : R[X]) → S) X : S) ((g : (a : R[X]) → S) X : S)
f' : RingHom.{u, u_1} (AddMonoidAlgebra R ℕ) S := f.comp (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hf' : f' = f.comp (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
g' : RingHom.{u, u_1} (AddMonoidAlgebra R ℕ) S := g.comp (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hg' : g' = g.comp (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
A : f' = g'
B : f = f'.comp (↑(toFinsuppIso R) : R[X] →+* AddMonoidAlgebra R ℕ)
⊢ g = g'.comp (↑(toFinsuppIso R) : R[X] →+* AddMonoidAlgebra R ℕ)
have rw : g =
  g.comp
    (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
      (↑(toFinsuppIso R) : R[X] →+* AddMonoidAlgebra R ℕ))
Tactic: rw [hg', RingHom.comp_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monomial (goal)
Goal:
R : Type u
inst : Semiring R
S : Type u_1
inst_1 : Semiring S
f g : RingHom.{u, u_1} R[X] S
h₁ :
  ∀ (a : R),
    Eq.{u_1 + 1} (α := S) ((f : (a : R[X]) → S) ((C : (a : R) → R[X]) a : R[X]) : S)
      ((g : (a : R[X]) → S) ((C : (a : R) → R[X]) a : R[X]) : S)
h₂ : Eq.{u_1 + 1} (α := S) ((f : (a : R[X]) → S) X : S) ((g : (a : R[X]) → S) X : S)
f' : RingHom.{u, u_1} (AddMonoidAlgebra R ℕ) S := f.comp (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hf' : f' = f.comp (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
g' : RingHom.{u, u_1} (AddMonoidAlgebra R ℕ) S := g.comp (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hg' : g' = g.comp (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
A : f' = g'
B : f = f'.comp (↑(toFinsuppIso R) : R[X] →+* AddMonoidAlgebra R ℕ)
⊢ g =
    g.comp
      (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
        (↑(toFinsuppIso R) : R[X] →+* AddMonoidAlgebra R ℕ))
have a : ∀ (x : R[X]),
  Eq.{u_1 + 1} (α := S) ((g : (a : R[X]) → S) x : S)
    ((g.comp
            (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
              (↑(toFinsuppIso R) : R[X] →+* AddMonoidAlgebra R ℕ)) :
          (a : R[X]) → S)
        x :
      S)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monomial (hypothesis)
Goal:
R : Type u
inst : Semiring R
S : Type u_1
inst_1 : Semiring S
f g : RingHom.{u, u_1} R[X] S
h₁ :
  ∀ (a : R),
    Eq.{u_1 + 1} (α := S) ((f : (a : R[X]) → S) ((C : (a : R) → R[X]) a : R[X]) : S)
      ((g : (a : R[X]) → S) ((C : (a : R) → R[X]) a : R[X]) : S)
h₂ : Eq.{u_1 + 1} (α := S) ((f : (a : R[X]) → S) X : S) ((g : (a : R[X]) → S) X : S)
f' : RingHom.{u, u_1} (AddMonoidAlgebra R ℕ) S := f.comp (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hf' : f' = f.comp (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
g' : RingHom.{u, u_1} (AddMonoidAlgebra R ℕ) S := g.comp (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hg' : g' = g.comp (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
A : f' = g'
B : f = f'.comp (↑(toFinsuppIso R) : R[X] →+* AddMonoidAlgebra R ℕ)
⊢ f = g
have C' : g = g'.comp (↑(toFinsuppIso R) : R[X] →+* AddMonoidAlgebra R ℕ)
Tactic: have C' : g = g'.comp (toFinsuppIso R) := by
    rw [hg', RingHom.comp_assoc]
    ext x
    simp only [RingEquiv.toRingHom_eq_coe, RingEquiv.symm_apply_apply, Function.comp_apply,
      RingHom.coe_comp, RingEquiv.coe_toRingHom]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monomial (goal)
Goal:
R : Type u
inst : Semiring R
S : Type u_1
inst_1 : Semiring S
f g : RingHom.{u, u_1} R[X] S
h₁ :
  ∀ (a : R),
    Eq.{u_1 + 1} (α := S) ((f : (a : R[X]) → S) ((C : (a : R) → R[X]) a : R[X]) : S)
      ((g : (a : R[X]) → S) ((C : (a : R) → R[X]) a : R[X]) : S)
h₂ : Eq.{u_1 + 1} (α := S) ((f : (a : R[X]) → S) X : S) ((g : (a : R[X]) → S) X : S)
f' : RingHom.{u, u_1} (AddMonoidAlgebra R ℕ) S := f.comp (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hf' : f' = f.comp (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
g' : RingHom.{u, u_1} (AddMonoidAlgebra R ℕ) S := g.comp (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hg' : g' = g.comp (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
A : f' = g'
B : f = f'.comp (↑(toFinsuppIso R) : R[X] →+* AddMonoidAlgebra R ℕ)
C' : g = g'.comp (↑(toFinsuppIso R) : R[X] →+* AddMonoidAlgebra R ℕ)
⊢ f = g
have rw : f'.comp (↑(toFinsuppIso R) : R[X] →+* AddMonoidAlgebra R ℕ) = g
Tactic: rw [B, C', A]