case refine_1
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_2
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
p q : MvPolynomial σ R
A : Type u_1
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)
⊢ RingHom.comp f singleZeroRingHom = RingHom.comp g singleZeroRingHom

case refine_2
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_2
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
p q : MvPolynomial σ R
A : Type u_1
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)
⊢ MonoidHom.comp (↑f) (of R (σ →₀ ℕ)) = MonoidHom.comp (↑g) (of R (σ →₀ ℕ))
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_2
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
p q : MvPolynomial σ R
A : Type u_1
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
refine AddMonoidAlgebra.ringHom_ext' ?_ ?_
case refine_1.a
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_2
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
p q : MvPolynomial σ R
A : Type u_1
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
⊢ ↑(RingHom.comp f singleZeroRingHom) x = ↑(RingHom.comp g singleZeroRingHom) x
case refine_1
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_2
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
p q : MvPolynomial σ R
A : Type u_1
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)
⊢ RingHom.comp f singleZeroRingHom = RingHom.comp g singleZeroRingHom
ext x
no goals
case refine_1.a
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_2
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
p q : MvPolynomial σ R
A : Type u_1
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
⊢ ↑(RingHom.comp f singleZeroRingHom) x = ↑(RingHom.comp g singleZeroRingHom) x
exact hC _
case refine_2.H
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_2
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
p q : MvPolynomial σ R
A : Type u_1
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 : σ),
    MonoidHom.comp (MonoidHom.comp (↑f) (of R (σ →₀ ℕ))) (↑AddMonoidHom.toMultiplicative (singleAddHom x)) =
      MonoidHom.comp (MonoidHom.comp (↑g) (of R (σ →₀ ℕ))) (↑AddMonoidHom.toMultiplicative (singleAddHom x))
case refine_2
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_2
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
p q : MvPolynomial σ R
A : Type u_1
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)
⊢ MonoidHom.comp (↑f) (of R (σ →₀ ℕ)) = MonoidHom.comp (↑g) (of R (σ →₀ ℕ))
apply Finsupp.mulHom_ext'
case refine_2.H
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_2
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
p q : MvPolynomial σ R
A : Type u_1
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 : σ
⊢ MonoidHom.comp (MonoidHom.comp (↑f) (of R (σ →₀ ℕ))) (↑AddMonoidHom.toMultiplicative (singleAddHom x)) =
    MonoidHom.comp (MonoidHom.comp (↑g) (of R (σ →₀ ℕ))) (↑AddMonoidHom.toMultiplicative (singleAddHom x))
case refine_2.H
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_2
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
p q : MvPolynomial σ R
A : Type u_1
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 : σ),
    MonoidHom.comp (MonoidHom.comp (↑f) (of R (σ →₀ ℕ))) (↑AddMonoidHom.toMultiplicative (singleAddHom x)) =
      MonoidHom.comp (MonoidHom.comp (↑g) (of R (σ →₀ ℕ))) (↑AddMonoidHom.toMultiplicative (singleAddHom x))
intros x
case refine_2.H.h
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_2
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
p q : MvPolynomial σ R
A : Type u_1
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 : σ
⊢ ↑(MonoidHom.comp (MonoidHom.comp (↑f) (of R (σ →₀ ℕ))) (↑AddMonoidHom.toMultiplicative (singleAddHom x)))
      (↑Multiplicative.ofAdd 1) =
    ↑(MonoidHom.comp (MonoidHom.comp (↑g) (of R (σ →₀ ℕ))) (↑AddMonoidHom.toMultiplicative (singleAddHom x)))
      (↑Multiplicative.ofAdd 1)
case refine_2.H
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_2
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
p q : MvPolynomial σ R
A : Type u_1
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 : σ
⊢ MonoidHom.comp (MonoidHom.comp (↑f) (of R (σ →₀ ℕ))) (↑AddMonoidHom.toMultiplicative (singleAddHom x)) =
    MonoidHom.comp (MonoidHom.comp (↑g) (of R (σ →₀ ℕ))) (↑AddMonoidHom.toMultiplicative (singleAddHom x))
apply MonoidHom.ext_mnat
no goals
case refine_2.H.h
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_2
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
p q : MvPolynomial σ R
A : Type u_1
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 : σ
⊢ ↑(MonoidHom.comp (MonoidHom.comp (↑f) (of R (σ →₀ ℕ))) (↑AddMonoidHom.toMultiplicative (singleAddHom x)))
      (↑Multiplicative.ofAdd 1) =
    ↑(MonoidHom.comp (MonoidHom.comp (↑g) (of R (σ →₀ ℕ))) (↑AddMonoidHom.toMultiplicative (singleAddHom x)))
      (↑Multiplicative.ofAdd 1)
exact hX _