case mp
α : Type u_1
β : Type ?u.248864
γ : Type ?u.248867
δ : Type ?u.248870
inst✝¹ : Monoid α
inst✝ : Unique αˣ
x y : α
⊢ x ~ᵤ y → x = y

case mpr
α : Type u_1
β : Type ?u.248864
γ : Type ?u.248867
δ : Type ?u.248870
inst✝¹ : Monoid α
inst✝ : Unique αˣ
x y : α
⊢ x = y → x ~ᵤ y
α : Type u_1
β : Type ?u.248864
γ : Type ?u.248867
δ : Type ?u.248870
inst✝¹ : Monoid α
inst✝ : Unique αˣ
x y : α
⊢ x ~ᵤ y ↔ x = y
constructor
case mp.intro
α : Type u_1
β : Type ?u.248864
γ : Type ?u.248867
δ : Type ?u.248870
inst✝¹ : Monoid α
inst✝ : Unique αˣ
x : α
c : αˣ
⊢ x = x * ↑c
case mp
α : Type u_1
β : Type ?u.248864
γ : Type ?u.248867
δ : Type ?u.248870
inst✝¹ : Monoid α
inst✝ : Unique αˣ
x y : α
⊢ x ~ᵤ y → x = y
rintro ⟨c, rfl⟩
no goals
case mp.intro
α : Type u_1
β : Type ?u.248864
γ : Type ?u.248867
δ : Type ?u.248870
inst✝¹ : Monoid α
inst✝ : Unique αˣ
x : α
c : αˣ
⊢ x = x * ↑c
rw [units_eq_one c, Units.val_one, mul_one]
case mpr
α : Type u_1
β : Type ?u.248864
γ : Type ?u.248867
δ : Type ?u.248870
inst✝¹ : Monoid α
inst✝ : Unique αˣ
x : α
⊢ x ~ᵤ x
case mpr
α : Type u_1
β : Type ?u.248864
γ : Type ?u.248867
δ : Type ?u.248870
inst✝¹ : Monoid α
inst✝ : Unique αˣ
x y : α
⊢ x = y → x ~ᵤ y
rintro rfl
no goals
case mpr
α : Type u_1
β : Type ?u.248864
γ : Type ?u.248867
δ : Type ?u.248870
inst✝¹ : Monoid α
inst✝ : Unique αˣ
x : α
⊢ x ~ᵤ x
rfl