case intro
α : Type u_1
β : Type ?u.95275
γ : Type ?u.95278
δ : Type ?u.95281
inst✝ : CommMonoid α
b : α
ha : Irreducible (b * b)
⊢ False
α : Type u_1
β : Type ?u.95275
γ : Type ?u.95278
δ : Type ?u.95281
inst✝ : CommMonoid α
a : α
ha : Irreducible a
⊢ ¬IsSquare a
rintro ⟨b, rfl⟩
case intro
α : Type u_1
β : Type ?u.95275
γ : Type ?u.95278
δ : Type ?u.95281
inst✝ : CommMonoid α
b : α
ha : Irreducible b ∧ IsUnit b
⊢ False
case intro
α : Type u_1
β : Type ?u.95275
γ : Type ?u.95278
δ : Type ?u.95281
inst✝ : CommMonoid α
b : α
ha : Irreducible (b * b)
⊢ False
simp only [irreducible_mul_iff, or_self_iff] at ha
no goals
case intro
α : Type u_1
β : Type ?u.95275
γ : Type ?u.95278
δ : Type ?u.95281
inst✝ : CommMonoid α
b : α
ha : Irreducible b ∧ IsUnit b
⊢ False
exact ha.1.not_unit ha.2