case intro
F : Type u_3
α : Type u_1
β : Type u_2
R : Type ?u.2218
inst✝² : MulOneClass α
inst✝¹ : MulOneClass β
inst✝ : MonoidHomClass F α β
f : F
m : α
⊢ IsSquare (↑f (m * m))
F : Type u_3
α : Type u_1
β : Type u_2
R : Type ?u.2218
inst✝² : MulOneClass α
inst✝¹ : MulOneClass β
inst✝ : MonoidHomClass F α β
m : α
f : F
⊢ IsSquare m → IsSquare (↑f m)
rintro ⟨m, rfl⟩
no goals
case intro
F : Type u_3
α : Type u_1
β : Type u_2
R : Type ?u.2218
inst✝² : MulOneClass α
inst✝¹ : MulOneClass β
inst✝ : MonoidHomClass F α β
f : F
m : α
⊢ IsSquare (↑f (m * m))
exact ⟨f m, by simp⟩
no goals
F : Type u_3
α : Type u_1
β : Type u_2
R : Type ?u.2218
inst✝² : MulOneClass α
inst✝¹ : MulOneClass β
inst✝ : MonoidHomClass F α β
f : F
m : α
⊢ ↑f (m * m) = ↑f m * ↑f m
simp