case intro
α : Type u_1
β : Type ?u.17778
γ : Type ?u.17781
a b c w✝ : α
h : Quotient.mk (Rel.setoid α) (b, c) = Quotient.mk (Rel.setoid α) (a, w✝)
⊢ a = b ∨ a = c
α : Type u_1
β : Type ?u.17778
γ : Type ?u.17781
a b c : α
⊢ Sym2.Mem a (Quotient.mk (Rel.setoid α) (b, c)) → a = b ∨ a = c
rintro ⟨_, h⟩
case intro
α : Type u_1
β : Type ?u.17778
γ : Type ?u.17781
a b c w✝ : α
h : b = a ∧ c = w✝ ∨ b = w✝ ∧ c = a
⊢ a = b ∨ a = c
case intro
α : Type u_1
β : Type ?u.17778
γ : Type ?u.17781
a b c w✝ : α
h : Quotient.mk (Rel.setoid α) (b, c) = Quotient.mk (Rel.setoid α) (a, w✝)
⊢ a = b ∨ a = c
rw [eq_iff] at h
no goals
case intro
α : Type u_1
β : Type ?u.17778
γ : Type ?u.17781
a b c w✝ : α
h : b = a ∧ c = w✝ ∨ b = w✝ ∧ c = a
⊢ a = b ∨ a = c
aesop
case inl
α : Type u_1
β : Type ?u.17778
γ : Type ?u.17781
a c : α
⊢ Sym2.Mem a (Quotient.mk (Rel.setoid α) (a, c))

case inr
α : Type u_1
β : Type ?u.17778
γ : Type ?u.17781
a b : α
⊢ Sym2.Mem a (Quotient.mk (Rel.setoid α) (b, a))
α : Type u_1
β : Type ?u.17778
γ : Type ?u.17781
a b c : α
⊢ a = b ∨ a = c → Sym2.Mem a (Quotient.mk (Rel.setoid α) (b, c))
rintro (rfl | rfl)
case inr
α : Type u_1
β : Type ?u.17778
γ : Type ?u.17781
a b : α
⊢ Sym2.Mem a (Quotient.mk (Rel.setoid α) (a, b))
case inr
α : Type u_1
β : Type ?u.17778
γ : Type ?u.17781
a b : α
⊢ Sym2.Mem a (Quotient.mk (Rel.setoid α) (b, a))
rw [eq_swap]
no goals
case inr
α : Type u_1
β : Type ?u.17778
γ : Type ?u.17781
a b : α
⊢ Sym2.Mem a (Quotient.mk (Rel.setoid α) (a, b))
exact ⟨_, rfl⟩
no goals
case inl
α : Type u_1
β : Type ?u.17778
γ : Type ?u.17781
a c : α
⊢ Sym2.Mem a (Quotient.mk (Rel.setoid α) (a, c))
exact ⟨_, rfl⟩