case mp
α : Type u_1
β : Type ?u.35991
γ : Type ?u.35994
x y : α
z : Sym2 α
hne : x ≠ y
⊢ x ∈ z ∧ y ∈ z → z = Quotient.mk (Rel.setoid α) (x, y)

case mpr
α : Type u_1
β : Type ?u.35991
γ : Type ?u.35994
x y : α
z : Sym2 α
hne : x ≠ y
⊢ z = Quotient.mk (Rel.setoid α) (x, y) → x ∈ z ∧ y ∈ z
α : Type u_1
β : Type ?u.35991
γ : Type ?u.35994
x y : α
z : Sym2 α
hne : x ≠ y
⊢ x ∈ z ∧ y ∈ z ↔ z = Quotient.mk (Rel.setoid α) (x, y)
constructor
case mp.h
α : Type u_1
β : Type ?u.35991
γ : Type ?u.35994
x y : α
hne : x ≠ y
x' y' : α
⊢ x ∈ Quotient.mk (Rel.setoid α) (x', y') ∧ y ∈ Quotient.mk (Rel.setoid α) (x', y') →
    Quotient.mk (Rel.setoid α) (x', y') = Quotient.mk (Rel.setoid α) (x, y)
case mp
α : Type u_1
β : Type ?u.35991
γ : Type ?u.35994
x y : α
z : Sym2 α
hne : x ≠ y
⊢ x ∈ z ∧ y ∈ z → z = Quotient.mk (Rel.setoid α) (x, y)
induction' z using Sym2.ind with x' y'
case mp.h
α : Type u_1
β : Type ?u.35991
γ : Type ?u.35994
x y : α
hne : x ≠ y
x' y' : α
⊢ (x = x' ∨ x = y') ∧ (y = x' ∨ y = y') → Quotient.mk (Rel.setoid α) (x', y') = Quotient.mk (Rel.setoid α) (x, y)
case mp.h
α : Type u_1
β : Type ?u.35991
γ : Type ?u.35994
x y : α
hne : x ≠ y
x' y' : α
⊢ x ∈ Quotient.mk (Rel.setoid α) (x', y') ∧ y ∈ Quotient.mk (Rel.setoid α) (x', y') →
    Quotient.mk (Rel.setoid α) (x', y') = Quotient.mk (Rel.setoid α) (x, y)
rw [mem_iff, mem_iff]
no goals
case mp.h
α : Type u_1
β : Type ?u.35991
γ : Type ?u.35994
x y : α
hne : x ≠ y
x' y' : α
⊢ (x = x' ∨ x = y') ∧ (y = x' ∨ y = y') → Quotient.mk (Rel.setoid α) (x', y') = Quotient.mk (Rel.setoid α) (x, y)
aesop
case mpr
α : Type u_1
β : Type ?u.35991
γ : Type ?u.35994
x y : α
hne : x ≠ y
⊢ x ∈ Quotient.mk (Rel.setoid α) (x, y) ∧ y ∈ Quotient.mk (Rel.setoid α) (x, y)
case mpr
α : Type u_1
β : Type ?u.35991
γ : Type ?u.35994
x y : α
z : Sym2 α
hne : x ≠ y
⊢ z = Quotient.mk (Rel.setoid α) (x, y) → x ∈ z ∧ y ∈ z
rintro rfl
no goals
case mpr
α : Type u_1
β : Type ?u.35991
γ : Type ?u.35994
x y : α
hne : x ≠ y
⊢ x ∈ Quotient.mk (Rel.setoid α) (x, y) ∧ y ∈ Quotient.mk (Rel.setoid α) (x, y)
simp