-- Mathlib/Algebra/MvPolynomial/Basic.lean
theorem ringHom_ext {A : Type*} [Semiring A] {f g : MvPolynomial σ R →+* A}
    (hC : ∀ r, f (C r) = g (C r)) (hX : ∀ i, f (X i) = g (X i)) : f = g

Proof state:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
A : Type u_2
inst✝ : Semiring A
f g : MvPolynomial σ R →+* A
hC : ∀ (r : R), f (C r) = g (C r)
hX : ∀ (i : σ), f (X i) = g (X i)
⊢ f = g

Tactic:
refine AddMonoidAlgebra.ringHom_ext' ?_ ?_

Result:
case refine_1
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
A : Type u_2
inst✝ : Semiring A
f g : MvPolynomial σ R →+* A
hC : ∀ (r : R), f (C r) = g (C r)
hX : ∀ (i : σ), f (X i) = g (X i)
⊢ f.comp singleZeroRingHom = g.comp singleZeroRingHom

case refine_2
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
A : Type u_2
inst✝ : Semiring A
f g : MvPolynomial σ R →+* A
hC : ∀ (r : R), f (C r) = g (C r)
hX : ∀ (i : σ), f (X i) = g (X i)
⊢ (↑f).comp (of R (σ →₀ ℕ)) = (↑g).comp (of R (σ →₀ ℕ))

Proof state:
case refine_2
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
A : Type u_2
inst✝ : Semiring A
f g : MvPolynomial σ R →+* A
hC : ∀ (r : R), f (C r) = g (C r)
hX : ∀ (i : σ), f (X i) = g (X i)
⊢ (↑f).comp (of R (σ →₀ ℕ)) = (↑g).comp (of R (σ →₀ ℕ))

Tactic:
apply Finsupp.mulHom_ext'

Result:
case refine_2.H
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
A : Type u_2
inst✝ : Semiring A
f g : MvPolynomial σ R →+* A
hC : ∀ (r : R), f (C r) = g (C r)
hX : ∀ (i : σ), f (X i) = g (X i)
⊢ ∀ (x : σ),
    ((↑f).comp (of R (σ →₀ ℕ))).comp (AddMonoidHom.toMultiplicative (Finsupp.singleAddHom x)) =
      ((↑g).comp (of R (σ →₀ ℕ))).comp (AddMonoidHom.toMultiplicative (Finsupp.singleAddHom x))

Proof state:
case refine_1.a
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
A : Type u_2
inst✝ : Semiring A
f g : MvPolynomial σ R →+* A
hC : ∀ (r : R), f (C r) = g (C r)
hX : ∀ (i : σ), f (X i) = g (X i)
x : R
⊢ (f.comp singleZeroRingHom) x = (g.comp singleZeroRingHom) x

Tactic:
exact hC _

Result:
no goals

Proof state:
case refine_2.H
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
A : Type u_2
inst✝ : Semiring A
f g : MvPolynomial σ R →+* A
hC : ∀ (r : R), f (C r) = g (C r)
hX : ∀ (i : σ), f (X i) = g (X i)
x : σ
⊢ ((↑f).comp (of R (σ →₀ ℕ))).comp (AddMonoidHom.toMultiplicative (Finsupp.singleAddHom x)) =
    ((↑g).comp (of R (σ →₀ ℕ))).comp (AddMonoidHom.toMultiplicative (Finsupp.singleAddHom x))

Tactic:
apply MonoidHom.ext_mnat

Result:
case refine_2.H.h
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
A : Type u_2
inst✝ : Semiring A
f g : MvPolynomial σ R →+* A
hC : ∀ (r : R), f (C r) = g (C r)
hX : ∀ (i : σ), f (X i) = g (X i)
x : σ
⊢ (((↑f).comp (of R (σ →₀ ℕ))).comp (AddMonoidHom.toMultiplicative (Finsupp.singleAddHom x))) (Multiplicative.ofAdd 1) =
    (((↑g).comp (of R (σ →₀ ℕ))).comp (AddMonoidHom.toMultiplicative (Finsupp.singleAddHom x))) (Multiplicative.ofAdd 1)

Proof state:
case refine_2.H.h
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
A : Type u_2
inst✝ : Semiring A
f g : MvPolynomial σ R →+* A
hC : ∀ (r : R), f (C r) = g (C r)
hX : ∀ (i : σ), f (X i) = g (X i)
x : σ
⊢ (((↑f).comp (of R (σ →₀ ℕ))).comp (AddMonoidHom.toMultiplicative (Finsupp.singleAddHom x))) (Multiplicative.ofAdd 1) =
    (((↑g).comp (of R (σ →₀ ℕ))).comp (AddMonoidHom.toMultiplicative (Finsupp.singleAddHom x))) (Multiplicative.ofAdd 1)

Tactic:
exact hX _

Result:
no goals

Proof state:
case refine_2.H
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
A : Type u_2
inst✝ : Semiring A
f g : MvPolynomial σ R →+* A
hC : ∀ (r : R), f (C r) = g (C r)
hX : ∀ (i : σ), f (X i) = g (X i)
⊢ ∀ (x : σ),
    ((↑f).comp (of R (σ →₀ ℕ))).comp (AddMonoidHom.toMultiplicative (Finsupp.singleAddHom x)) =
      ((↑g).comp (of R (σ →₀ ℕ))).comp (AddMonoidHom.toMultiplicative (Finsupp.singleAddHom x))

Tactic:
intros x

Result:
case refine_2.H
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
A : Type u_2
inst✝ : Semiring A
f g : MvPolynomial σ R →+* A
hC : ∀ (r : R), f (C r) = g (C r)
hX : ∀ (i : σ), f (X i) = g (X i)
x : σ
⊢ ((↑f).comp (of R (σ →₀ ℕ))).comp (AddMonoidHom.toMultiplicative (Finsupp.singleAddHom x)) =
    ((↑g).comp (of R (σ →₀ ℕ))).comp (AddMonoidHom.toMultiplicative (Finsupp.singleAddHom x))

Proof state:
case refine_1
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
A : Type u_2
inst✝ : Semiring A
f g : MvPolynomial σ R →+* A
hC : ∀ (r : R), f (C r) = g (C r)
hX : ∀ (i : σ), f (X i) = g (X i)
⊢ f.comp singleZeroRingHom = g.comp singleZeroRingHom

Tactic:
ext x

Result:
case refine_1.a
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
A : Type u_2
inst✝ : Semiring A
f g : MvPolynomial σ R →+* A
hC : ∀ (r : R), f (C r) = g (C r)
hX : ∀ (i : σ), f (X i) = g (X i)
x : R
⊢ (f.comp singleZeroRingHom) x = (g.comp singleZeroRingHom) x