-- 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 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}

Tactic:
any_goals
  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.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
⊢ ∃ 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
hce : G.Adj a b
hde : G.Adj b d
⊢ ∃ 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 a b
⊢ 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.inr
α : Type u_1
G : SimpleGraph α
a b : α
hab : ¬a = b
c : α
hde : G.Adj a b
hcd : G.Adj a c
hce : G.Adj b c
⊢ ∃ 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 : α
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}

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
⊢ G.Adj a b ∧ ∃ c_1, G.Adj a c_1 ∧ G.Adj b c_1 ∧ {c, b, a} = {a, b, c_1}

Proof state:
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
⊢ ∃ 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
hce : G.Adj a b
hde : G.Adj b d
⊢ ∃ 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 a b
⊢ 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.inr
α : Type u_1
G : SimpleGraph α
a b : α
hab : ¬a = b
c : α
hde : G.Adj a b
hcd : G.Adj a c
hce : G.Adj b c
⊢ ∃ 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 : α
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}

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
⊢ G.Adj a b ∧ ∃ c_1, G.Adj a c_1 ∧ G.Adj b c_1 ∧ {c, b, a} = {a, b, c_1}

Tactic:
any_goals
  first
  | exact ⟨c, by aesop⟩
  | exact ⟨d, by aesop⟩
  | exact ⟨e, by aesop⟩
  | simp only [*, adj_comm, true_and, Ne, eq_self_iff_true, not_true] at *
    exact ⟨c, by aesop⟩
  | simp only [*, adj_comm, true_and, Ne, eq_self_iff_true, not_true] at *
    exact ⟨d, by aesop⟩
  | simp only [*, adj_comm, true_and, Ne, eq_self_iff_true, not_true] at *
    exact ⟨e, by aesop⟩

Result:
no goals

Proof state:
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 a b
⊢ ∃ c, G.Adj a c ∧ G.Adj b c ∧ {b, a, e} = {a, b, c}

Tactic:
exact ⟨e, by aesop⟩

Result:
no goals

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, d, e} ∧ b ∈ {c, d, 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:
simp only [mem_insert, mem_singleton] at hab

Result:
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}

Proof state:
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}}

Tactic:
simp only [mem_sym2_iff, Sym2.mem_iff, forall_eq_or_imp, forall_eq, Set.sep_and,
  Set.mem_inter_iff, Set.mem_sep_iff, mem_cliqueSet_iff, Set.mem_setOf_eq,
  and_and_and_comm (b := _ ∈ _), and_self, is3Clique_iff]

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