α : Type ?u.225159
G : Type ?u.225162
M : Type ?u.225165
R : Type u_1
A : Type ?u.225171
inst✝² : Monoid M
inst✝¹ : AddMonoid A
inst✝ : AddMonoidWithOne R
⊢ AddMonoidHom.mrange (Nat.castAddMonoidHom R) = AddMonoidHom.mrange (↑(multiplesHom R) 1)
α : Type ?u.225159
G : Type ?u.225162
M : Type ?u.225165
R : Type u_1
A : Type ?u.225171
inst✝² : Monoid M
inst✝¹ : AddMonoid A
inst✝ : AddMonoidWithOne R
⊢ 1 = closure {1}
rw [closure_singleton_eq, one_eq_mrange]
case e_f
α : Type ?u.225159
G : Type ?u.225162
M : Type ?u.225165
R : Type u_1
A : Type ?u.225171
inst✝² : Monoid M
inst✝¹ : AddMonoid A
inst✝ : AddMonoidWithOne R
⊢ Nat.castAddMonoidHom R = ↑(multiplesHom R) 1
α : Type ?u.225159
G : Type ?u.225162
M : Type ?u.225165
R : Type u_1
A : Type ?u.225171
inst✝² : Monoid M
inst✝¹ : AddMonoid A
inst✝ : AddMonoidWithOne R
⊢ AddMonoidHom.mrange (Nat.castAddMonoidHom R) = AddMonoidHom.mrange (↑(multiplesHom R) 1)
congr 1
case e_f.a
α : Type ?u.225159
G : Type ?u.225162
M : Type ?u.225165
R : Type u_1
A : Type ?u.225171
inst✝² : Monoid M
inst✝¹ : AddMonoid A
inst✝ : AddMonoidWithOne R
⊢ ↑(Nat.castAddMonoidHom R) 1 = ↑(↑(multiplesHom R) 1) 1
case e_f
α : Type ?u.225159
G : Type ?u.225162
M : Type ?u.225165
R : Type u_1
A : Type ?u.225171
inst✝² : Monoid M
inst✝¹ : AddMonoid A
inst✝ : AddMonoidWithOne R
⊢ Nat.castAddMonoidHom R = ↑(multiplesHom R) 1
ext
no goals
case e_f.a
α : Type ?u.225159
G : Type ?u.225162
M : Type ?u.225165
R : Type u_1
A : Type ?u.225171
inst✝² : Monoid M
inst✝¹ : AddMonoid A
inst✝ : AddMonoidWithOne R
⊢ ↑(Nat.castAddMonoidHom R) 1 = ↑(↑(multiplesHom R) 1) 1
simp