α : Type u_3
β : Type ?u.347410
γ : Type ?u.347413
ι : Type ?u.347416
M : Type u_2
M' : Type ?u.347422
N : Type u_1
P : Type ?u.347428
G : Type ?u.347431
H✝ : Type ?u.347434
R : Type ?u.347437
S : Type ?u.347440
inst✝¹ : AddZeroClass M
inst✝ : MulOneClass N
f g : Multiplicative (α →₀ M) →* N
H : ∀ (x : α) (y : M), ↑f (↑Multiplicative.ofAdd (single x y)) = ↑g (↑Multiplicative.ofAdd (single x y))
this : ↑MonoidHom.toAdditive'' f = ↑MonoidHom.toAdditive'' g
⊢ f = g
α : Type u_3
β : Type ?u.347410
γ : Type ?u.347413
ι : Type ?u.347416
M : Type u_2
M' : Type ?u.347422
N : Type u_1
P : Type ?u.347428
G : Type ?u.347431
H✝ : Type ?u.347434
R : Type ?u.347437
S : Type ?u.347440
inst✝¹ : AddZeroClass M
inst✝ : MulOneClass N
f g : Multiplicative (α →₀ M) →* N
H : ∀ (x : α) (y : M), ↑f (↑Multiplicative.ofAdd (single x y)) = ↑g (↑Multiplicative.ofAdd (single x y))
⊢ f = g
have := @addHom_ext α M (Additive N) _ _
  (MonoidHom.toAdditive'' f) (MonoidHom.toAdditive'' g) H
case h
α : Type u_3
β : Type ?u.347410
γ : Type ?u.347413
ι : Type ?u.347416
M : Type u_2
M' : Type ?u.347422
N : Type u_1
P : Type ?u.347428
G : Type ?u.347431
H✝ : Type ?u.347434
R : Type ?u.347437
S : Type ?u.347440
inst✝¹ : AddZeroClass M
inst✝ : MulOneClass N
f g : Multiplicative (α →₀ M) →* N
H : ∀ (x : α) (y : M), ↑f (↑Multiplicative.ofAdd (single x y)) = ↑g (↑Multiplicative.ofAdd (single x y))
this : ↑MonoidHom.toAdditive'' f = ↑MonoidHom.toAdditive'' g
x✝ : Multiplicative (α →₀ M)
⊢ ↑f x✝ = ↑g x✝
α : Type u_3
β : Type ?u.347410
γ : Type ?u.347413
ι : Type ?u.347416
M : Type u_2
M' : Type ?u.347422
N : Type u_1
P : Type ?u.347428
G : Type ?u.347431
H✝ : Type ?u.347434
R : Type ?u.347437
S : Type ?u.347440
inst✝¹ : AddZeroClass M
inst✝ : MulOneClass N
f g : Multiplicative (α →₀ M) →* N
H : ∀ (x : α) (y : M), ↑f (↑Multiplicative.ofAdd (single x y)) = ↑g (↑Multiplicative.ofAdd (single x y))
this : ↑MonoidHom.toAdditive'' f = ↑MonoidHom.toAdditive'' g
⊢ f = g
ext
case h
α : Type u_3
β : Type ?u.347410
γ : Type ?u.347413
ι : Type ?u.347416
M : Type u_2
M' : Type ?u.347422
N : Type u_1
P : Type ?u.347428
G : Type ?u.347431
H✝ : Type ?u.347434
R : Type ?u.347437
S : Type ?u.347440
inst✝¹ : AddZeroClass M
inst✝ : MulOneClass N
f g : Multiplicative (α →₀ M) →* N
H : ∀ (x : α) (y : M), ↑f (↑Multiplicative.ofAdd (single x y)) = ↑g (↑Multiplicative.ofAdd (single x y))
this✝ : ↑MonoidHom.toAdditive'' f = ↑MonoidHom.toAdditive'' g
this : ∀ (x : α →₀ M), ↑(↑MonoidHom.toAdditive'' f) x = ↑(↑MonoidHom.toAdditive'' g) x
x✝ : Multiplicative (α →₀ M)
⊢ ↑f x✝ = ↑g x✝
case h
α : Type u_3
β : Type ?u.347410
γ : Type ?u.347413
ι : Type ?u.347416
M : Type u_2
M' : Type ?u.347422
N : Type u_1
P : Type ?u.347428
G : Type ?u.347431
H✝ : Type ?u.347434
R : Type ?u.347437
S : Type ?u.347440
inst✝¹ : AddZeroClass M
inst✝ : MulOneClass N
f g : Multiplicative (α →₀ M) →* N
H : ∀ (x : α) (y : M), ↑f (↑Multiplicative.ofAdd (single x y)) = ↑g (↑Multiplicative.ofAdd (single x y))
this : ↑MonoidHom.toAdditive'' f = ↑MonoidHom.toAdditive'' g
x✝ : Multiplicative (α →₀ M)
⊢ ↑f x✝ = ↑g x✝
rw [FunLike.ext_iff] at this
no goals
case h
α : Type u_3
β : Type ?u.347410
γ : Type ?u.347413
ι : Type ?u.347416
M : Type u_2
M' : Type ?u.347422
N : Type u_1
P : Type ?u.347428
G : Type ?u.347431
H✝ : Type ?u.347434
R : Type ?u.347437
S : Type ?u.347440
inst✝¹ : AddZeroClass M
inst✝ : MulOneClass N
f g : Multiplicative (α →₀ M) →* N
H : ∀ (x : α) (y : M), ↑f (↑Multiplicative.ofAdd (single x y)) = ↑g (↑Multiplicative.ofAdd (single x y))
this✝ : ↑MonoidHom.toAdditive'' f = ↑MonoidHom.toAdditive'' g
this : ∀ (x : α →₀ M), ↑(↑MonoidHom.toAdditive'' f) x = ↑(↑MonoidHom.toAdditive'' g) x
x✝ : Multiplicative (α →₀ M)
⊢ ↑f x✝ = ↑g x✝
apply this