case mp
α : Type u_1
β : Type ?u.4752
γ : Type ?u.4755
a b c : α
h : Quotient.mk (Rel.setoid α) (b, a) = Quotient.mk (Rel.setoid α) (c, a)
⊢ b = c

case mpr
α : Type u_1
β : Type ?u.4752
γ : Type ?u.4755
a b c : α
h : b = c
⊢ Quotient.mk (Rel.setoid α) (b, a) = Quotient.mk (Rel.setoid α) (c, a)
α : Type u_1
β : Type ?u.4752
γ : Type ?u.4755
a b c : α
⊢ Quotient.mk (Rel.setoid α) (b, a) = Quotient.mk (Rel.setoid α) (c, a) ↔ b = c
constructor <;> intro h
no goals
case mpr
α : Type u_1
β : Type ?u.4752
γ : Type ?u.4755
a b c : α
h : b = c
⊢ Quotient.mk (Rel.setoid α) (b, a) = Quotient.mk (Rel.setoid α) (c, a)
rw [h]
case mp
α : Type u_1
β : Type ?u.4752
γ : Type ?u.4755
a b c : α
h : (b, a) ≈ (c, a)
⊢ b = c
case mp
α : Type u_1
β : Type ?u.4752
γ : Type ?u.4755
a b c : α
h : Quotient.mk (Rel.setoid α) (b, a) = Quotient.mk (Rel.setoid α) (c, a)
⊢ b = c
rw [Quotient.eq] at h
no goals
case mp
α : Type u_1
β : Type ?u.4752
γ : Type ?u.4755
a b c : α
h : (b, a) ≈ (c, a)
⊢ b = c
cases h <;> rfl