-- 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}}
⊢ G.EdgeDisjointTriangles → ∀ (x y : α), ¬s(x, y).IsDiag → {s | s ∈ G.cliqueSet 3 ∧ s(x, y) ∈ s.sym2}.Subsingleton

Tactic:
rintro hG a b 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 : ¬s(a, b).IsDiag
⊢ {s | s ∈ G.cliqueSet 3 ∧ s(a, b) ∈ s.sym2}.Subsingleton

Proof state:
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 | (∃ a b c, G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}) ∧ e ∈ s.sym2}.Subsingleton) →
    ∀ ⦃x : Finset α⦄ (x_1 x_2 x_3 : α),
      G.Adj x_1 x_2 →
        G.Adj x_1 x_3 →
          G.Adj x_2 x_3 →
            x = {x_1, x_2, x_3} →
              ∀ ⦃y : Finset α⦄ (x_4 x_5 x_6 : α),
                G.Adj x_4 x_5 →
                  G.Adj x_4 x_6 →
                    G.Adj x_5 x_6 → y = {x_4, x_5, x_6} → ∀ x_7 ∈ x, x_7 ∈ y → ∀ x_8 ∈ x, x_8 ∈ y → ¬x_7 = x_8 → x = y

Tactic:
rintro hG _ a b c hab hac hbc rfl _ d e f hde hdf hef rfl g hg₁ hg₂ h hh₁ hh₂ hgh

Result:
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}}
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
⊢ {a, b, c} = {d, e, f}

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

Tactic:
simp only [EdgeDisjointTriangles, is3Clique_iff, Set.Pairwise, mem_cliqueSet_iff, Ne,
  forall_exists_index, and_imp, ← Set.not_nontrivial_iff (s := _ ∩ _), not_imp_not,
  Set.Nontrivial, Set.mem_inter_iff, mem_coe]

Result:
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 | (∃ a b c, G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}) ∧ e ∈ s.sym2}.Subsingleton) →
    ∀ ⦃x : Finset α⦄ (x_1 x_2 x_3 : α),
      G.Adj x_1 x_2 →
        G.Adj x_1 x_3 →
          G.Adj x_2 x_3 →
            x = {x_1, x_2, x_3} →
              ∀ ⦃y : Finset α⦄ (x_4 x_5 x_6 : α),
                G.Adj x_4 x_5 →
                  G.Adj x_4 x_6 →
                    G.Adj x_5 x_6 → y = {x_4, x_5, x_6} → ∀ x_7 ∈ x, x_7 ∈ y → ∀ x_8 ∈ x, x_8 ∈ y → ¬x_7 = x_8 → x = y

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

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

Tactic:
aesop

Result:
no goals

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}

Tactic:
exact ⟨e, by aesop⟩

Result:
no goals

Proof state:
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:
simp only [*, adj_comm, true_and, Ne, eq_self_iff_true, not_true] at *

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}}
⊢ G.EdgeDisjointTriangles → ∀ ⦃e : Sym2 α⦄, ¬e.IsDiag → {s | s ∈ G.cliqueSet 3 ∧ e ∈ s.sym2}.Subsingleton

Tactic:
rw [Sym2.forall]

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 → ∀ (x y : α), ¬s(x, y).IsDiag → {s | s ∈ G.cliqueSet 3 ∧ s(x, y) ∈ s.sym2}.Subsingleton

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

Tactic:
aesop

Result:
no goals

Proof state:
case h.mp
α : 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}

Tactic:
rintro ⟨⟨c, d, e, hcd, hce, hde, rfl⟩, 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, 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}

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

Tactic:
aesop

Result:
no goals