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

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