case intro.intro
F : Type ?u.28464
α : Type u_1
β : Type ?u.28470
R : Type ?u.28473
inst✝ : CommSemigroup α
a b : α
⊢ IsSquare (a * a * (b * b))
F : Type ?u.28464
α : Type u_1
β : Type ?u.28470
R : Type ?u.28473
inst✝ : CommSemigroup α
a b : α
⊢ IsSquare a → IsSquare b → IsSquare (a * b)
rintro ⟨a, rfl⟩ ⟨b, rfl⟩
no goals
case intro.intro
F : Type ?u.28464
α : Type u_1
β : Type ?u.28470
R : Type ?u.28473
inst✝ : CommSemigroup α
a b : α
⊢ IsSquare (a * a * (b * b))
exact ⟨a * b, mul_mul_mul_comm _ _ _ _⟩