awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Monic
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)
⊢ HMul.hMul (β := R[X]) (q * p) ((C : (a : R) → R[X]) (↑h.unit⁻¹ : R) : R[X]) = 0

Tactic:
simp only [zero_mul] at hp

Premises used: MulZeroClass.zero_mul
-- Module: Mathlib.Algebra.Polynomial.Monic
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
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
⊢ q = 0

Tactic:
rwa [mul_assoc, Monic.mul_left_eq_zero_iff] at hp

Premises used: mul_assoc, Polynomial.Monic.mul_left_eq_zero_iff
-- Module: Mathlib.Algebra.Polynomial.Monic
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

Tactic:
monic_mul_C_of_leadingCoeff_mul_eq_one ?_

Premises used: Polynomial.monic_mul_C_of_leadingCoeff_mul_eq_one
-- Module: Mathlib.Algebra.Polynomial.Monic
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
mp : p.leadingCoeff * (↑h.unit⁻¹ : R) = 1
⊢ (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) (↑h.unit⁻¹ : R) : R[X])).Monic

Tactic:
refine monic_mul_C_of_leadingCoeff_mul_eq_one ?_

Premises used: Polynomial.monic_mul_C_of_leadingCoeff_mul_eq_one
-- Module: Mathlib.Algebra.Polynomial.Monic
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
⊢ p.leadingCoeff * (↑h.unit⁻¹ : R) = 1

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
mpr mpr₁ : Eq.{u + 1} (α := R[X]) 0 0
⊢ 0 * p = 0

Tactic:
rw [zero_mul]

Premises used: MulZeroClass.zero_mul
-- Module: Mathlib.Algebra.Polynomial.Monomial
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
i j : ℕ
simp_rw : Eq.{u + 1} (α := AddMonoidAlgebra R ℕ) (AddMonoidAlgebra.single i 1) (AddMonoidAlgebra.single j 1) ↔ i = j
⊢ Eq.{u + 1} (α := R[X]) ((monomial i : (a : R) → R[X]) 1) ((monomial j : (a : R) → R[X]) 1) ↔ i = j

Tactic:
simp_rw [← ofFinsupp_single, ofFinsupp.injEq]

Premises used: Polynomial.ofFinsupp_single, Polynomial.ofFinsupp.injEq
-- Module: Mathlib.Algebra.Polynomial.Monomial
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
i j : ℕ
⊢ Eq.{u + 1} (α := AddMonoidAlgebra R ℕ) (AddMonoidAlgebra.single i 1) (AddMonoidAlgebra.single j 1) ↔ i = j

Tactic:
AddMonoidAlgebra.of_injective.eq_iff

Premises used: Function.Injective.eq_iff, Multiplicative, AddMonoidAlgebra.of_injective, Finsupp.single
-- Module: Mathlib.Algebra.Polynomial.Monomial
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
i j : ℕ
⊢ Eq.{u + 1} (α := AddMonoidAlgebra R ℕ) (AddMonoidAlgebra.single i 1) (AddMonoidAlgebra.single j 1) ↔ i = j

Tactic:
exact AddMonoidAlgebra.of_injective.eq_iff

Premises used: Function.Injective.eq_iff, AddMonoidAlgebra.of_injective
-- Module: Mathlib.Algebra.Polynomial.Monomial
Goal:
R : Type u
a b : R
m_1 n_1 : ℕ
inst : Semiring R
p q r : R[X]
inst_1 : Nontrivial R
m n : ℕ
h :
  Eq.{u + 1} (α := R[X]) ((fun (i : ℕ) ↦ ((monomial i : (a : R) → R[X]) 1 : R[X])) m)
    ((fun (i : ℕ) ↦ ((monomial i : (a : R) → R[X]) 1 : R[X])) n)
⊢ m = n

Tactic:
simpa [monomial_one_eq_iff] using h

Premises used: Polynomial.monomial_one_eq_iff
-- Module: Mathlib.Algebra.Polynomial.Monomial
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
mpr : (∃ (n : ℕ) (a : R), f = (monomial n : (a : R) → R[X]) a) → f.support.card ≤ 1
⊢ f.support.card ≤ 1 ↔ ∃ (n : ℕ) (a : R), f = (monomial n : (a : R) → R[X]) a

Tactic:
constructor
-- Module: Mathlib.Algebra.Polynomial.Monomial
Goal:
R : Type u
inst : Semiring R
f : R[X]
H : f.support.card ≤ 1
⊢ ∃ (x : ℕ), f.support ⊆ {x}

Tactic:
rw [Finset.card_le_one_iff_subset_singleton] at H

Premises used: Finset.card_le_one_iff_subset_singleton
-- Module: Mathlib.Algebra.Polynomial.Monomial
Goal:
R : Type u
inst : Semiring R
f : R[X]
H : ∃ (x : ℕ), f.support ⊆ {x}
mp : ∀ (n : ℕ) (hn : f.support ⊆ {n}), ∃ (n : ℕ) (a : R), f = (monomial n : (a : R) → R[X]) a
⊢ ∃ (n : ℕ) (a : R), f = (monomial n : (a : R) → R[X]) a

Tactic:
rcases H with ⟨n, hn⟩
-- Module: Mathlib.Algebra.Polynomial.Monomial
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

Tactic:
⟨n, f.coeff n, ?_⟩

Premises used: Polynomial.coeff, Exists.intro
-- Module: Mathlib.Algebra.Polynomial.Monomial
Goal:
R : Type u
inst : Semiring R
f : R[X]
n : ℕ
hn : f.support ⊆ {n}
mp : f = (monomial n : (a : R) → R[X]) (f.coeff n)
⊢ ∃ (n : ℕ) (a : R), f = (monomial n : (a : R) → R[X]) a

Tactic:
refine ⟨n, f.coeff n, ?_⟩
-- Module: Mathlib.Algebra.Polynomial.Monomial
Goal:
R : Type u
inst : Semiring R
f : R[X]
n : ℕ
hn : f.support ⊆ {n}
mp : ∀ (i : ℕ), f.coeff i = coeff ((monomial n : (a : R) → R[X]) (f.coeff n)) i
⊢ f = (monomial n : (a : R) → R[X]) (f.coeff n)

Tactic:
ext i
-- Module: Mathlib.Algebra.Polynomial.Monomial
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
neg : ∀ (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

Tactic:
by_cases hi : i = n
-- Module: Mathlib.Algebra.Polynomial.Monomial
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

Tactic:
simp [hi]
-- Module: Mathlib.Algebra.Polynomial.Monomial
Goal:
R : Type u
inst : Semiring R
f : R[X]
n : ℕ
hn : f.support ⊆ {n}
i : ℕ
hi : ¬i = n
rw : i ∉ f.support
⊢ f.coeff i = 0

Tactic:
rw [← notMem_support_iff]

Premises used: Polynomial.notMem_support_iff
-- Module: Mathlib.Algebra.Polynomial.Monomial
Goal:
R : Type u
inst : Semiring R
f : R[X]
n : ℕ
hn : f.support ⊆ {n}
i : ℕ
hi : ¬i = n
⊢ i ∉ f.support

Tactic:
fun hi' => hi (Finset.mem_singleton.1 (hn hi'))

Premises used: Finset.mem_singleton, Iff.mp, Not
-- Module: Mathlib.Algebra.Polynomial.Monomial
Goal:
R : Type u
inst : Semiring R
f : R[X]
n : ℕ
hn : f.support ⊆ {n}
i : ℕ
hi : ¬i = n
⊢ i ∉ f.support

Tactic:
exact fun hi' => hi (Finset.mem_singleton.1 (hn hi'))

Premises used: Finset.mem_singleton, Iff.mp
-- Module: Mathlib.Algebra.Polynomial.Monomial
Goal:
R : Type u
inst : Semiring R
f : R[X]
n : ℕ
hn : f.support ⊆ {n}
i : ℕ
hi : ¬i = n
⊢ 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'))
-- Module: Mathlib.Algebra.Polynomial.Monomial
Goal:
R : Type u
inst : Semiring R
f : R[X]
n : ℕ
hn : f.support ⊆ {n}
i : ℕ
hi : ¬i = n
this : f.coeff i = 0
⊢ f.coeff i = coeff ((monomial n : (a : R) → R[X]) (f.coeff n)) i

Tactic:
simp [this, Ne.symm hi, coeff_monomial]

Premises used: Ne.symm, Polynomial.coeff_monomial
-- Module: Mathlib.Algebra.Polynomial.Monomial
Goal:
R : Type u
inst : Semiring R
n : ℕ
a : R
mpr : support.{u} (R := R) ((monomial n : (a : R) → R[X]) a) ⊆ {n}
⊢ (support.{u} (R := R) ((monomial n : (a : R) → R[X]) a)).card ≤ Finset.card (α := ℕ) {n}

Tactic:
apply Finset.card_le_card

Premises used: Finset.card_le_card
-- Module: Mathlib.Algebra.Polynomial.Monomial
Goal:
R : Type u
inst : Semiring R
n : ℕ
a : R
⊢ support.{u} (R := R) ((monomial n : (a : R) → R[X]) a) ⊆ {n}

Tactic:
support_monomial' _ _

Premises used: Polynomial.support_monomial'
-- Module: Mathlib.Algebra.Polynomial.Monomial
Goal:
R : Type u
inst : Semiring R
n : ℕ
a : R
⊢ support.{u} (R := R) ((monomial n : (a : R) → R[X]) a) ⊆ {n}

Tactic:
exact support_monomial' _ _

Premises used: Polynomial.support_monomial'
-- Module: Mathlib.Algebra.Polynomial.Monomial
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)
⊢ 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'

Premises used: RingHom.comp, Polynomial.toFinsuppIso, RingEquiv.toRingHom, RingEquiv.symm
-- Module: Mathlib.Algebra.Polynomial.Monomial
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)))
⊢ 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'

Premises used: RingHom.comp, Polynomial.toFinsuppIso, RingEquiv.toRingHom, RingEquiv.symm
-- Module: Mathlib.Algebra.Polynomial.Monomial
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)
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)
⊢ f' = g'

Tactic:
ext
-- Module: Mathlib.Algebra.Polynomial.Monomial
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)))
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:
simp [f', g', h₁, RingEquiv.toRingHom_eq_coe]

Premises used: RingEquiv.toRingHom_eq_coe
-- Module: Mathlib.Algebra.Polynomial.Monomial
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)))
⊢ 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:
simpa using h₂
-- Module: Mathlib.Algebra.Polynomial.Monomial
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'

Tactic:
have A : f' = g' := by
    ext
    · simp [f', g', h₁, RingEquiv.toRingHom_eq_coe]
    simpa using h₂
-- Module: Mathlib.Algebra.Polynomial.Monomial
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'
rw :
  f =
    f.comp
      (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
        (↑(toFinsuppIso R) : R[X] →+* AddMonoidAlgebra R ℕ))
⊢ f = f'.comp (↑(toFinsuppIso R) : R[X] →+* AddMonoidAlgebra R ℕ)

Tactic:
rw [hf', RingHom.comp_assoc]

Premises used: RingHom.comp_assoc
-- Module: Mathlib.Algebra.Polynomial.Monomial
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'
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)
⊢ f =
    f.comp
      (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
        (↑(toFinsuppIso R) : R[X] →+* AddMonoidAlgebra R ℕ))

Tactic:
ext x
-- Module: Mathlib.Algebra.Polynomial.Monomial
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'
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:
simp only [RingEquiv.toRingHom_eq_coe, RingEquiv.symm_apply_apply, Function.comp_apply,
      RingHom.coe_comp, RingEquiv.coe_toRingHom]

Premises used: RingEquiv.symm_apply_apply, RingHom.coe_comp, RingEquiv.toRingHom_eq_coe, Function.comp_apply, RingEquiv.coe_toRingHom
-- Module: Mathlib.Algebra.Polynomial.Monomial
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 ℕ)

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]
-- Module: Mathlib.Algebra.Polynomial.Monomial
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 ℕ)
rw :
  g =
    g.comp
      (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
        (↑(toFinsuppIso R) : R[X] →+* AddMonoidAlgebra R ℕ))
⊢ g = g'.comp (↑(toFinsuppIso R) : R[X] →+* AddMonoidAlgebra R ℕ)

Tactic:
rw [hg', RingHom.comp_assoc]

Premises used: RingHom.comp_assoc
-- Module: Mathlib.Algebra.Polynomial.Monomial
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 ℕ)
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)
⊢ g =
    g.comp
      (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
        (↑(toFinsuppIso R) : R[X] →+* AddMonoidAlgebra R ℕ))

Tactic:
ext x
-- Module: Mathlib.Algebra.Polynomial.Monomial
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 ℕ)
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:
simp only [RingEquiv.toRingHom_eq_coe, RingEquiv.symm_apply_apply, Function.comp_apply,
      RingHom.coe_comp, RingEquiv.coe_toRingHom]

Premises used: RingEquiv.symm_apply_apply, RingHom.coe_comp, RingEquiv.toRingHom_eq_coe, Function.comp_apply, RingEquiv.coe_toRingHom
-- Module: Mathlib.Algebra.Polynomial.Monomial
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 ℕ)

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]