no goals
α : Type ?u.3131
β : Type ?u.3134
G : Type ?u.3137
M : Type u
inst✝ : MulOneClass M
a b : M
h : a * b = 1
⊢ a = 1 ↔ b = 1
constructor <;> (rintro rfl; simpa using h)
case mpr
α : Type ?u.3131
β : Type ?u.3134
G : Type ?u.3137
M : Type u
inst✝ : MulOneClass M
a : M
h : a * 1 = 1
⊢ a = 1
case mpr
α : Type ?u.3131
β : Type ?u.3134
G : Type ?u.3137
M : Type u
inst✝ : MulOneClass M
a b : M
h : a * b = 1
⊢ b = 1 → a = 1
rintro rfl
no goals
case mpr
α : Type ?u.3131
β : Type ?u.3134
G : Type ?u.3137
M : Type u
inst✝ : MulOneClass M
a : M
h : a * 1 = 1
⊢ a = 1
simpa using h