-- Mathlib/Algebra/Polynomial/Monomial.lean
theorem ringHom_ext {S} [Semiring S] {f g : R[X] →+* S} (h₁ : ∀ a, f (C a) = g (C a))
    (h₂ : f X = g X) : f = g

Proof state:
case h₁.a
R : Type u
inst✝¹ : Semiring R
S : Type u_1
inst✝ : Semiring S
f g : R[X] →+* S
h₁ : ∀ (a : R), f (C a) = g (C a)
h₂ : f X = g X
f' : AddMonoidAlgebra R ℕ →+* S := f.comp (toFinsuppIso R).symm.toRingHom
hf' : f' = f.comp (toFinsuppIso R).symm.toRingHom
g' : AddMonoidAlgebra R ℕ →+* S := g.comp (toFinsuppIso R).symm.toRingHom
hg' : g' = g.comp (toFinsuppIso R).symm.toRingHom
x✝ : R
⊢ (f'.comp AddMonoidAlgebra.singleZeroRingHom) x✝ = (g'.comp AddMonoidAlgebra.singleZeroRingHom) x✝

case h_of.h
R : Type u
inst✝¹ : Semiring R
S : Type u_1
inst✝ : Semiring S
f g : R[X] →+* S
h₁ : ∀ (a : R), f (C a) = g (C a)
h₂ : f X = g X
f' : AddMonoidAlgebra R ℕ →+* S := f.comp (toFinsuppIso R).symm.toRingHom
hf' : f' = f.comp (toFinsuppIso R).symm.toRingHom
g' : AddMonoidAlgebra R ℕ →+* S := g.comp (toFinsuppIso R).symm.toRingHom
hg' : g' = g.comp (toFinsuppIso R).symm.toRingHom
⊢ ((↑f').comp (AddMonoidAlgebra.of R ℕ)) (Multiplicative.ofAdd 1) =
    ((↑g').comp (AddMonoidAlgebra.of R ℕ)) (Multiplicative.ofAdd 1)

Tactic:
simp [f', g', h₁, RingEquiv.toRingHom_eq_coe]

Result:
case h_of.h
R : Type u
inst✝¹ : Semiring R
S : Type u_1
inst✝ : Semiring S
f g : R[X] →+* S
h₁ : ∀ (a : R), f (C a) = g (C a)
h₂ : f X = g X
f' : AddMonoidAlgebra R ℕ →+* S := f.comp (toFinsuppIso R).symm.toRingHom
hf' : f' = f.comp (toFinsuppIso R).symm.toRingHom
g' : AddMonoidAlgebra R ℕ →+* S := g.comp (toFinsuppIso R).symm.toRingHom
hg' : g' = g.comp (toFinsuppIso R).symm.toRingHom
⊢ ((↑f').comp (AddMonoidAlgebra.of R ℕ)) (Multiplicative.ofAdd 1) =
    ((↑g').comp (AddMonoidAlgebra.of R ℕ)) (Multiplicative.ofAdd 1)

Proof state:
R : Type u
inst✝¹ : Semiring R
S : Type u_1
inst✝ : Semiring S
f g : R[X] →+* S
h₁ : ∀ (a : R), f (C a) = g (C a)
h₂ : f X = g X
f' : AddMonoidAlgebra R ℕ →+* S := f.comp (toFinsuppIso R).symm.toRingHom
hf' : f' = f.comp (toFinsuppIso R).symm.toRingHom
g' : AddMonoidAlgebra R ℕ →+* S := g.comp (toFinsuppIso R).symm.toRingHom
hg' : g' = g.comp (toFinsuppIso R).symm.toRingHom
A : f' = g'
B : f = f'.comp ↑(toFinsuppIso R)
⊢ g = g.comp ((toFinsuppIso R).symm.toRingHom.comp ↑(toFinsuppIso R))

Tactic:
ext x

Result:
case a
R : Type u
inst✝¹ : Semiring R
S : Type u_1
inst✝ : Semiring S
f g : R[X] →+* S
h₁ : ∀ (a : R), f (C a) = g (C a)
h₂ : f X = g X
f' : AddMonoidAlgebra R ℕ →+* S := f.comp (toFinsuppIso R).symm.toRingHom
hf' : f' = f.comp (toFinsuppIso R).symm.toRingHom
g' : AddMonoidAlgebra R ℕ →+* S := g.comp (toFinsuppIso R).symm.toRingHom
hg' : g' = g.comp (toFinsuppIso R).symm.toRingHom
A : f' = g'
B : f = f'.comp ↑(toFinsuppIso R)
x : R[X]
⊢ g x = (g.comp ((toFinsuppIso R).symm.toRingHom.comp ↑(toFinsuppIso R))) x

Proof state:
R : Type u
inst✝¹ : Semiring R
S : Type u_1
inst✝ : Semiring S
f g : R[X] →+* S
h₁ : ∀ (a : R), f (C a) = g (C a)
h₂ : f X = g X
f' : AddMonoidAlgebra R ℕ →+* S := f.comp (toFinsuppIso R).symm.toRingHom
hf' : f' = f.comp (toFinsuppIso R).symm.toRingHom
g' : AddMonoidAlgebra R ℕ →+* S := g.comp (toFinsuppIso R).symm.toRingHom
hg' : g' = g.comp (toFinsuppIso R).symm.toRingHom
⊢ f' = g'

Tactic:
ext

Result:
case h₁.a
R : Type u
inst✝¹ : Semiring R
S : Type u_1
inst✝ : Semiring S
f g : R[X] →+* S
h₁ : ∀ (a : R), f (C a) = g (C a)
h₂ : f X = g X
f' : AddMonoidAlgebra R ℕ →+* S := f.comp (toFinsuppIso R).symm.toRingHom
hf' : f' = f.comp (toFinsuppIso R).symm.toRingHom
g' : AddMonoidAlgebra R ℕ →+* S := g.comp (toFinsuppIso R).symm.toRingHom
hg' : g' = g.comp (toFinsuppIso R).symm.toRingHom
x✝ : R
⊢ (f'.comp AddMonoidAlgebra.singleZeroRingHom) x✝ = (g'.comp AddMonoidAlgebra.singleZeroRingHom) x✝

case h_of.h
R : Type u
inst✝¹ : Semiring R
S : Type u_1
inst✝ : Semiring S
f g : R[X] →+* S
h₁ : ∀ (a : R), f (C a) = g (C a)
h₂ : f X = g X
f' : AddMonoidAlgebra R ℕ →+* S := f.comp (toFinsuppIso R).symm.toRingHom
hf' : f' = f.comp (toFinsuppIso R).symm.toRingHom
g' : AddMonoidAlgebra R ℕ →+* S := g.comp (toFinsuppIso R).symm.toRingHom
hg' : g' = g.comp (toFinsuppIso R).symm.toRingHom
⊢ ((↑f').comp (AddMonoidAlgebra.of R ℕ)) (Multiplicative.ofAdd 1) =
    ((↑g').comp (AddMonoidAlgebra.of R ℕ)) (Multiplicative.ofAdd 1)

Proof state:
R : Type u
inst✝¹ : Semiring R
S : Type u_1
inst✝ : Semiring S
f g : R[X] →+* S
h₁ : ∀ (a : R), f (C a) = g (C a)
h₂ : f X = g X
⊢ f = g

Tactic:
set f' := f.comp (toFinsuppIso R).symm.toRingHom with hf'

Result:
R : Type u
inst✝¹ : Semiring R
S : Type u_1
inst✝ : Semiring S
f g : R[X] →+* S
h₁ : ∀ (a : R), f (C a) = g (C a)
h₂ : f X = g X
f' : AddMonoidAlgebra R ℕ →+* S := f.comp (toFinsuppIso R).symm.toRingHom
hf' : f' = f.comp (toFinsuppIso R).symm.toRingHom
⊢ f = g

Proof state:
R : Type u
inst✝¹ : Semiring R
S : Type u_1
inst✝ : Semiring S
f g : R[X] →+* S
h₁ : ∀ (a : R), f (C a) = g (C a)
h₂ : f X = g X
f' : AddMonoidAlgebra R ℕ →+* S := f.comp (toFinsuppIso R).symm.toRingHom
hf' : f' = f.comp (toFinsuppIso R).symm.toRingHom
g' : AddMonoidAlgebra R ℕ →+* S := g.comp (toFinsuppIso R).symm.toRingHom
hg' : g' = g.comp (toFinsuppIso R).symm.toRingHom
A : f' = g'
⊢ f = f.comp ((toFinsuppIso R).symm.toRingHom.comp ↑(toFinsuppIso R))

Tactic:
ext x

Result:
case a
R : Type u
inst✝¹ : Semiring R
S : Type u_1
inst✝ : Semiring S
f g : R[X] →+* S
h₁ : ∀ (a : R), f (C a) = g (C a)
h₂ : f X = g X
f' : AddMonoidAlgebra R ℕ →+* S := f.comp (toFinsuppIso R).symm.toRingHom
hf' : f' = f.comp (toFinsuppIso R).symm.toRingHom
g' : AddMonoidAlgebra R ℕ →+* S := g.comp (toFinsuppIso R).symm.toRingHom
hg' : g' = g.comp (toFinsuppIso R).symm.toRingHom
A : f' = g'
x : R[X]
⊢ f x = (f.comp ((toFinsuppIso R).symm.toRingHom.comp ↑(toFinsuppIso R))) x

Proof state:
R : Type u
inst✝¹ : Semiring R
S : Type u_1
inst✝ : Semiring S
f g : R[X] →+* S
h₁ : ∀ (a : R), f (C a) = g (C a)
h₂ : f X = g X
f' : AddMonoidAlgebra R ℕ →+* S := f.comp (toFinsuppIso R).symm.toRingHom
hf' : f' = f.comp (toFinsuppIso R).symm.toRingHom
g' : AddMonoidAlgebra R ℕ →+* S := g.comp (toFinsuppIso R).symm.toRingHom
hg' : g' = g.comp (toFinsuppIso R).symm.toRingHom
A : f' = g'
⊢ f = g

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]

Result:
R : Type u
inst✝¹ : Semiring R
S : Type u_1
inst✝ : Semiring S
f g : R[X] →+* S
h₁ : ∀ (a : R), f (C a) = g (C a)
h₂ : f X = g X
f' : AddMonoidAlgebra R ℕ →+* S := f.comp (toFinsuppIso R).symm.toRingHom
hf' : f' = f.comp (toFinsuppIso R).symm.toRingHom
g' : AddMonoidAlgebra R ℕ →+* S := g.comp (toFinsuppIso R).symm.toRingHom
hg' : g' = g.comp (toFinsuppIso R).symm.toRingHom
A : f' = g'
B : f = f'.comp ↑(toFinsuppIso R)
⊢ f = g

Proof state:
R : Type u
inst✝¹ : Semiring R
S : Type u_1
inst✝ : Semiring S
f g : R[X] →+* S
h₁ : ∀ (a : R), f (C a) = g (C a)
h₂ : f X = g X
f' : AddMonoidAlgebra R ℕ →+* S := f.comp (toFinsuppIso R).symm.toRingHom
hf' : f' = f.comp (toFinsuppIso R).symm.toRingHom
g' : AddMonoidAlgebra R ℕ →+* S := g.comp (toFinsuppIso R).symm.toRingHom
hg' : g' = g.comp (toFinsuppIso R).symm.toRingHom
A : f' = g'
⊢ f = f'.comp ↑(toFinsuppIso R)

Tactic:
rw [hf', RingHom.comp_assoc]

Result:
R : Type u
inst✝¹ : Semiring R
S : Type u_1
inst✝ : Semiring S
f g : R[X] →+* S
h₁ : ∀ (a : R), f (C a) = g (C a)
h₂ : f X = g X
f' : AddMonoidAlgebra R ℕ →+* S := f.comp (toFinsuppIso R).symm.toRingHom
hf' : f' = f.comp (toFinsuppIso R).symm.toRingHom
g' : AddMonoidAlgebra R ℕ →+* S := g.comp (toFinsuppIso R).symm.toRingHom
hg' : g' = g.comp (toFinsuppIso R).symm.toRingHom
A : f' = g'
⊢ f = f.comp ((toFinsuppIso R).symm.toRingHom.comp ↑(toFinsuppIso R))