-- Mathlib/Combinatorics/SimpleGraph/Triangle/Basic.lean
lemma edgeDisjointTriangles_iff_mem_sym2_subsingleton :
    G.EdgeDisjointTriangles ↔
      ∀ ⦃e : Sym2 α⦄, ¬ e.IsDiag → {s ∈ G.cliqueSet 3 | e ∈ (s : Finset α).sym2}.Subsingleton

Proof state:
case mp
α : Type u_1
G : SimpleGraph α
this :
  ∀ (a b : α),
    a ≠ b → {s | s ∈ G.cliqueSet 3 ∧ s(a, b) ∈ s.sym2} = {s | G.Adj a b ∧ ∃ c, G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}}
hG : G.EdgeDisjointTriangles
a b : α
hab : ¬a = b
⊢ {s | G.Adj (a, b).1 (a, b).2 ∧ ∃ c, G.Adj (a, b).1 c ∧ G.Adj (a, b).2 c ∧ s = {(a, b).1, (a, b).2, c}}.Subsingleton

Tactic:
rintro _ ⟨hab, c, hac, hbc, rfl⟩ _ ⟨-, d, had, hbd, rfl⟩

Result:
case mp.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
G : SimpleGraph α
this :
  ∀ (a b : α),
    a ≠ b → {s | s ∈ G.cliqueSet 3 ∧ s(a, b) ∈ s.sym2} = {s | G.Adj a b ∧ ∃ c, G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}}
hG : G.EdgeDisjointTriangles
a b : α
hab✝ : ¬a = b
hab : G.Adj (a, b).1 (a, b).2
c : α
hac : G.Adj (a, b).1 c
hbc : G.Adj (a, b).2 c
d : α
had : G.Adj (a, b).1 d
hbd : G.Adj (a, b).2 d
⊢ {(a, b).1, (a, b).2, c} = {(a, b).1, (a, b).2, d}

Proof state:
case h.mp.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
G : SimpleGraph α
a b : α
hab✝ : a ≠ b
c d e : α
hcd : G.Adj c d
hce : G.Adj c e
hde : G.Adj d e
hab : (a = c ∨ a = d ∨ a = e) ∧ (b = c ∨ b = d ∨ b = e)
⊢ G.Adj a b ∧ ∃ c_1, G.Adj a c_1 ∧ G.Adj b c_1 ∧ {c, d, e} = {a, b, c_1}

Tactic:
obtain ⟨rfl | rfl | rfl, rfl | rfl | rfl⟩ := hab

Result:
case h.mp.intro.intro.intro.intro.intro.intro.intro.intro.inl.inl
α : Type u_1
G : SimpleGraph α
b d e : α
hde : G.Adj d e
hab : b ≠ b
hcd : G.Adj b d
hce : G.Adj b e
⊢ G.Adj b b ∧ ∃ c, G.Adj b c ∧ G.Adj b c ∧ {b, d, e} = {b, b, c}

case h.mp.intro.intro.intro.intro.intro.intro.intro.intro.inl.inr.inl
α : Type u_1
G : SimpleGraph α
a b : α
hab : a ≠ b
e : α
hce : G.Adj a e
hde : G.Adj b e
hcd : G.Adj a b
⊢ G.Adj a b ∧ ∃ c, G.Adj a c ∧ G.Adj b c ∧ {a, b, e} = {a, b, c}

case h.mp.intro.intro.intro.intro.intro.intro.intro.intro.inl.inr.inr
α : Type u_1
G : SimpleGraph α
a b : α
hab : a ≠ b
d : α
hcd : G.Adj a d
hde : G.Adj d b
hce : G.Adj a b
⊢ G.Adj a b ∧ ∃ c, G.Adj a c ∧ G.Adj b c ∧ {a, d, b} = {a, b, c}

case h.mp.intro.intro.intro.intro.intro.intro.intro.intro.inr.inl.inl
α : Type u_1
G : SimpleGraph α
a b : α
hab : a ≠ b
e : α
hde : G.Adj a e
hce : G.Adj b e
hcd : G.Adj b a
⊢ G.Adj a b ∧ ∃ c, G.Adj a c ∧ G.Adj b c ∧ {b, a, e} = {a, b, c}

case h.mp.intro.intro.intro.intro.intro.intro.intro.intro.inr.inl.inr.inl
α : Type u_1
G : SimpleGraph α
b c e : α
hce : G.Adj c e
hab : b ≠ b
hcd : G.Adj c b
hde : G.Adj b e
⊢ G.Adj b b ∧ ∃ c_1, G.Adj b c_1 ∧ G.Adj b c_1 ∧ {c, b, e} = {b, b, c_1}

case h.mp.intro.intro.intro.intro.intro.intro.intro.intro.inr.inl.inr.inr
α : Type u_1
G : SimpleGraph α
a b : α
hab : a ≠ b
c : α
hcd : G.Adj c a
hce : G.Adj c b
hde : G.Adj a b
⊢ G.Adj a b ∧ ∃ c_1, G.Adj a c_1 ∧ G.Adj b c_1 ∧ {c, a, b} = {a, b, c_1}

case h.mp.intro.intro.intro.intro.intro.intro.intro.intro.inr.inr.inl
α : Type u_1
G : SimpleGraph α
a b : α
hab : a ≠ b
d : α
hde : G.Adj d a
hcd : G.Adj b d
hce : G.Adj b a
⊢ G.Adj a b ∧ ∃ c, G.Adj a c ∧ G.Adj b c ∧ {b, d, a} = {a, b, c}

case h.mp.intro.intro.intro.intro.intro.intro.intro.intro.inr.inr.inr.inl
α : Type u_1
G : SimpleGraph α
a b : α
hab : a ≠ b
c : α
hce : G.Adj c a
hcd : G.Adj c b
hde : G.Adj b a
⊢ G.Adj a b ∧ ∃ c_1, G.Adj a c_1 ∧ G.Adj b c_1 ∧ {c, b, a} = {a, b, c_1}

case h.mp.intro.intro.intro.intro.intro.intro.intro.intro.inr.inr.inr.inr
α : Type u_1
G : SimpleGraph α
b c d : α
hcd : G.Adj c d
hab : b ≠ b
hce : G.Adj c b
hde : G.Adj d b
⊢ G.Adj b b ∧ ∃ c_1, G.Adj b c_1 ∧ G.Adj b c_1 ∧ {c, d, b} = {b, b, c_1}

Proof state:
case h.mp.intro.intro.intro.intro.intro.intro.intro.intro.inr.inr.inr.inl
α : Type u_1
G : SimpleGraph α
a b : α
hab : ¬a = b
c : α
hce : G.Adj a c
hcd : G.Adj b c
hde : G.Adj a b
⊢ ∃ c_1, G.Adj a c_1 ∧ G.Adj b c_1 ∧ {c, b, a} = {a, b, c_1}

Tactic:
exact ⟨c, by aesop⟩

Result:
no goals

Proof state:
α : Type u_1
G : SimpleGraph α
a b : α
hab : a ≠ b
⊢ {s | s ∈ G.cliqueSet 3 ∧ s(a, b) ∈ s.sym2} = {s | G.Adj a b ∧ ∃ c, G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}}

Tactic:
ext s

Result:
case h
α : Type u_1
G : SimpleGraph α
a b : α
hab : a ≠ b
s : Finset α
⊢ s ∈ {s | s ∈ G.cliqueSet 3 ∧ s(a, b) ∈ s.sym2} ↔ s ∈ {s | G.Adj a b ∧ ∃ c, G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}}

Proof state:
α : Type u_1
G : SimpleGraph α
this :
  ∀ (a b : α),
    a ≠ b → {s | s ∈ G.cliqueSet 3 ∧ s(a, b) ∈ s.sym2} = {s | G.Adj a b ∧ ∃ c, G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}}
hG :
  ∀ ⦃e : Sym2 α⦄,
    ¬e.IsDiag → {s | (∃ a b c, G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}) ∧ e ∈ s.sym2}.Subsingleton
a b c : α
hab : G.Adj a b
hac : G.Adj a c
hbc : G.Adj b c
d e f : α
hde : G.Adj d e
hdf : G.Adj d f
hef : G.Adj e f
g : α
hg₁ : g ∈ {a, b, c}
hg₂ : g ∈ {d, e, f}
h : α
hh₁ : h ∈ {a, b, c}
hh₂ : h ∈ {d, e, f}
hgh : ¬g = h
⊢ s(g, h) ∈ {a, b, c}.sym2

Tactic:
simpa using And.intro hg₁ hh₁

Result:
no goals

Proof state:
α : Type u_1
G : SimpleGraph α
this :
  ∀ (a b : α),
    a ≠ b → {s | s ∈ G.cliqueSet 3 ∧ s(a, b) ∈ s.sym2} = {s | G.Adj a b ∧ ∃ c, G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}}
hG :
  ∀ ⦃e : Sym2 α⦄,
    ¬e.IsDiag → {s | (∃ a b c, G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}) ∧ e ∈ s.sym2}.Subsingleton
a b c : α
hab : G.Adj a b
hac : G.Adj a c
hbc : G.Adj b c
d e f : α
hde : G.Adj d e
hdf : G.Adj d f
hef : G.Adj e f
g : α
hg₁ : g ∈ {a, b, c}
hg₂ : g ∈ {d, e, f}
h : α
hh₁ : h ∈ {a, b, c}
hh₂ : h ∈ {d, e, f}
hgh : ¬g = h
⊢ s(g, h) ∈ {d, e, f}.sym2

Tactic:
simpa using And.intro hg₂ hh₂

Result:
no goals

Proof state:
case mp
α : Type u_1
G : SimpleGraph α
this :
  ∀ (a b : α),
    a ≠ b → {s | s ∈ G.cliqueSet 3 ∧ s(a, b) ∈ s.sym2} = {s | G.Adj a b ∧ ∃ c, G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}}
hG : G.EdgeDisjointTriangles
a b : α
hab : ¬s(a, b).IsDiag
⊢ {s | s ∈ G.cliqueSet 3 ∧ s(a, b) ∈ s.sym2}.Subsingleton

Tactic:
simp only [Sym2.isDiag_iff_proj_eq] at hab

Result:
case mp
α : Type u_1
G : SimpleGraph α
this :
  ∀ (a b : α),
    a ≠ b → {s | s ∈ G.cliqueSet 3 ∧ s(a, b) ∈ s.sym2} = {s | G.Adj a b ∧ ∃ c, G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}}
hG : G.EdgeDisjointTriangles
a b : α
hab : ¬a = b
⊢ {s | s ∈ G.cliqueSet 3 ∧ s(a, b) ∈ s.sym2}.Subsingleton

Proof state:
α : Type u_1
G : SimpleGraph α
this :
  ∀ (a b : α),
    a ≠ b → {s | s ∈ G.cliqueSet 3 ∧ s(a, b) ∈ s.sym2} = {s | G.Adj a b ∧ ∃ c, G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}}
⊢ G.EdgeDisjointTriangles ↔ ∀ ⦃e : Sym2 α⦄, ¬e.IsDiag → {s | s ∈ G.cliqueSet 3 ∧ e ∈ s.sym2}.Subsingleton

Tactic:
constructor

Result:
case mp
α : Type u_1
G : SimpleGraph α
this :
  ∀ (a b : α),
    a ≠ b → {s | s ∈ G.cliqueSet 3 ∧ s(a, b) ∈ s.sym2} = {s | G.Adj a b ∧ ∃ c, G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}}
⊢ G.EdgeDisjointTriangles → ∀ ⦃e : Sym2 α⦄, ¬e.IsDiag → {s | s ∈ G.cliqueSet 3 ∧ e ∈ s.sym2}.Subsingleton

case mpr
α : Type u_1
G : SimpleGraph α
this :
  ∀ (a b : α),
    a ≠ b → {s | s ∈ G.cliqueSet 3 ∧ s(a, b) ∈ s.sym2} = {s | G.Adj a b ∧ ∃ c, G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}}
⊢ (∀ ⦃e : Sym2 α⦄, ¬e.IsDiag → {s | s ∈ G.cliqueSet 3 ∧ e ∈ s.sym2}.Subsingleton) → G.EdgeDisjointTriangles

Proof state:
case h.mp.intro.intro.intro.intro.intro.intro.intro.intro.inr.inr.inl
α : Type u_1
G : SimpleGraph α
a b : α
hab : ¬a = b
d : α
hcd : G.Adj b d
hde : G.Adj a d
hce : G.Adj a b
⊢ G.Adj a b ∧ ∃ c, G.Adj a c ∧ G.Adj b c ∧ {b, d, a} = {a, b, c}

Tactic:
simp only [*, adj_comm, true_and, Ne, eq_self_iff_true, not_true] at *

Result:
case h.mp.intro.intro.intro.intro.intro.intro.intro.intro.inr.inr.inl
α : Type u_1
G : SimpleGraph α
a b : α
hab : ¬a = b
d : α
hcd : G.Adj b d
hde : G.Adj a d
hce : G.Adj a b
⊢ ∃ c, G.Adj a c ∧ G.Adj b c ∧ {b, d, a} = {a, b, c}