case h.ofNat
F : Type ?u.48754
ι : Type ?u.48757
α : Type ?u.48760
β : Type ?u.48763
M : Type u_1
inst✝ : Monoid M
f g : ℤ →* M
h_neg_one : ↑f (-1) = ↑g (-1)
h_nat : comp f ↑ofNatHom = comp g ↑ofNatHom
x : ℕ
⊢ ↑f (ofNat x) = ↑g (ofNat x)

case h.negSucc
F : Type ?u.48754
ι : Type ?u.48757
α : Type ?u.48760
β : Type ?u.48763
M : Type u_1
inst✝ : Monoid M
f g : ℤ →* M
h_neg_one : ↑f (-1) = ↑g (-1)
h_nat : comp f ↑ofNatHom = comp g ↑ofNatHom
x : ℕ
⊢ ↑f -[x+1] = ↑g -[x+1]
F : Type ?u.48754
ι : Type ?u.48757
α : Type ?u.48760
β : Type ?u.48763
M : Type u_1
inst✝ : Monoid M
f g : ℤ →* M
h_neg_one : ↑f (-1) = ↑g (-1)
h_nat : comp f ↑ofNatHom = comp g ↑ofNatHom
⊢ f = g
ext (x | x)
no goals
case h.ofNat
F : Type ?u.48754
ι : Type ?u.48757
α : Type ?u.48760
β : Type ?u.48763
M : Type u_1
inst✝ : Monoid M
f g : ℤ →* M
h_neg_one : ↑f (-1) = ↑g (-1)
h_nat : comp f ↑ofNatHom = comp g ↑ofNatHom
x : ℕ
⊢ ↑f (ofNat x) = ↑g (ofNat x)
exact (FunLike.congr_fun h_nat x : _)
case h.negSucc
F : Type ?u.48754
ι : Type ?u.48757
α : Type ?u.48760
β : Type ?u.48763
M : Type u_1
inst✝ : Monoid M
f g : ℤ →* M
h_neg_one : ↑f (-1) = ↑g (-1)
h_nat : comp f ↑ofNatHom = comp g ↑ofNatHom
x : ℕ
⊢ ↑f (-1) * ↑f (↑x + 1) = ↑g (-1) * ↑g (↑x + 1)
case h.negSucc
F : Type ?u.48754
ι : Type ?u.48757
α : Type ?u.48760
β : Type ?u.48763
M : Type u_1
inst✝ : Monoid M
f g : ℤ →* M
h_neg_one : ↑f (-1) = ↑g (-1)
h_nat : comp f ↑ofNatHom = comp g ↑ofNatHom
x : ℕ
⊢ ↑f -[x+1] = ↑g -[x+1]
rw [Int.negSucc_eq, ← neg_one_mul, f.map_mul, g.map_mul]
case h.negSucc.e_a
F : Type ?u.48754
ι : Type ?u.48757
α : Type ?u.48760
β : Type ?u.48763
M : Type u_1
inst✝ : Monoid M
f g : ℤ →* M
h_neg_one : ↑f (-1) = ↑g (-1)
h_nat : comp f ↑ofNatHom = comp g ↑ofNatHom
x : ℕ
⊢ ↑f (↑x + 1) = ↑g (↑x + 1)
case h.negSucc
F : Type ?u.48754
ι : Type ?u.48757
α : Type ?u.48760
β : Type ?u.48763
M : Type u_1
inst✝ : Monoid M
f g : ℤ →* M
h_neg_one : ↑f (-1) = ↑g (-1)
h_nat : comp f ↑ofNatHom = comp g ↑ofNatHom
x : ℕ
⊢ ↑f (-1) * ↑f (↑x + 1) = ↑g (-1) * ↑g (↑x + 1)
congr 1
no goals
case h.negSucc.e_a
F : Type ?u.48754
ι : Type ?u.48757
α : Type ?u.48760
β : Type ?u.48763
M : Type u_1
inst✝ : Monoid M
f g : ℤ →* M
h_neg_one : ↑f (-1) = ↑g (-1)
h_nat : comp f ↑ofNatHom = comp g ↑ofNatHom
x : ℕ
⊢ ↑f (↑x + 1) = ↑g (↑x + 1)
exact_mod_cast (FunLike.congr_fun h_nat (x + 1) : _)