-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (goal)
Goal:
α : Type u_1
G : SimpleGraph α
have :
  ∀ (a b : α) (hab : a ≠ b),
    Eq.{u_1 + 1} (α := Set (Finset α)) {s : Finset α | s ∈ G.cliqueSet 3 ∧ s(a, b) ∈ s.sym2}
      {s : Finset α | G.Adj a b ∧ ∃ (c : α), G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}}
have₁ :
  ∀
    (this :
      ∀ (a b : α) (hab : a ≠ b),
        Eq.{u_1 + 1} (α := Set (Finset α)) {s : Finset α | s ∈ G.cliqueSet 3 ∧ s(a, b) ∈ s.sym2}
          {s : Finset α | G.Adj a b ∧ ∃ (c : α), G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}}),
    G.EdgeDisjointTriangles ↔
      ∀ ⦃e : Sym2 α⦄, ¬e.IsDiag → Set.Subsingleton.{u_1} (α := Finset α) {s : Finset α | s ∈ G.cliqueSet 3 ∧ e ∈ s.sym2}
have₂ :
  ∀ (a b : α) (hab : a ≠ b),
    Eq.{u_1 + 1} (α := Set (Finset α)) {s : Finset α | s ∈ G.cliqueSet 3 ∧ s(a, b) ∈ s.sym2}
      {s : Finset α | G.Adj a b ∧ ∃ (c : α), G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}}
have₃ have₄ :
  ∀
    (this :
      ∀ (a b : α) (hab : a ≠ b),
        Eq.{u_1 + 1} (α := Set (Finset α)) {s : Finset α | s ∈ G.cliqueSet 3 ∧ s(a, b) ∈ s.sym2}
          {s : Finset α | G.Adj a b ∧ ∃ (c : α), G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}}),
    G.EdgeDisjointTriangles ↔
      ∀ ⦃e : Sym2 α⦄, ¬e.IsDiag → Set.Subsingleton.{u_1} (α := Finset α) {s : Finset α | s ∈ G.cliqueSet 3 ∧ e ∈ s.sym2}
mp :
  ∀
    (this :
      ∀ (a b : α) (hab : a ≠ b),
        Eq.{u_1 + 1} (α := Set (Finset α)) {s : Finset α | s ∈ G.cliqueSet 3 ∧ s(a, b) ∈ s.sym2}
          {s : Finset α | G.Adj a b ∧ ∃ (c : α), G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}}),
    G.EdgeDisjointTriangles →
      ∀ ⦃e : Sym2 α⦄, ¬e.IsDiag → Set.Subsingleton.{u_1} (α := Finset α) {s : Finset α | s ∈ G.cliqueSet 3 ∧ e ∈ s.sym2}
⊢ G.EdgeDisjointTriangles ↔
    ∀ ⦃e : Sym2 α⦄, ¬e.IsDiag → Set.Subsingleton.{u_1} (α := Finset α) {s : Finset α | s ∈ G.cliqueSet 3 ∧ e ∈ s.sym2}
have mpr : ∀
  (this :
    ∀ (a b : α) (hab : a ≠ b),
      Eq.{u_1 + 1} (α := Set (Finset α)) {s : Finset α | s ∈ G.cliqueSet 3 ∧ s(a, b) ∈ s.sym2}
        {s : Finset α | G.Adj a b ∧ ∃ (c : α), G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}}),
  (∀ ⦃e : Sym2 α⦄, ¬e.IsDiag → Set.Subsingleton.{u_1} (α := Finset α) {s : Finset α | s ∈ G.cliqueSet 3 ∧ e ∈ s.sym2}) →
    G.EdgeDisjointTriangles
Tactic: classical
  have (a b) (hab : a ≠ b) : {s ∈ (G.cliqueSet 3 : Set (Finset α)) | s(a, b) ∈ (s : Finset α).sym2}
    = {s | G.Adj a b ∧ ∃ c, G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}} := by
    ext s
    simp only [mem_sym2_iff, Sym2.mem_iff, forall_eq_or_imp, forall_eq,
      mem_cliqueSet_iff, Set.mem_setOf_eq,
      is3Clique_iff]
    constructor
    · rintro ⟨⟨c, d, e, hcd, hce, hde, rfl⟩, hab⟩
      simp only [mem_insert, mem_singleton] at hab
      obtain ⟨rfl | rfl | rfl, rfl | rfl | rfl⟩ := hab
      any_goals
        simp only [*, adj_comm, true_and, Ne, not_true] at *
      any_goals
        first
        | exact ⟨c, by aesop⟩
        | exact ⟨d, by aesop⟩
        | exact ⟨e, by aesop⟩
        | simp only [*, true_and] at *
          exact ⟨c, by aesop⟩
        | simp only [*, true_and] at *
          exact ⟨d, by aesop⟩
        | simp only [*, true_and] at *
          exact ⟨e, by aesop⟩
    · rintro ⟨hab, c, hac, hbc, rfl⟩
      refine ⟨⟨a, b, c, ?_⟩, ?_⟩ <;> simp [*]
  constructor
  · rw [Sym2.forall]
    rintro hG a b hab
    simp only [Sym2.mk_isDiag_iff] at hab
    rw [this _ _ (Sym2.mk_isDiag_iff.not.2 hab)]
    rintro _ ⟨hab, c, hac, hbc, rfl⟩ _ ⟨-, d, had, hbd, rfl⟩
    refine hG.eq ?_ ?_ (Set.Nontrivial.not_subsingleton ⟨a, ?_, b, ?_, hab.ne⟩) <;>
      simp [is3Clique_triple_iff, *]
  · 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]
    rintro hG _ a b c hab hac hbc rfl _ d e f hde hdf hef rfl g hg₁ hg₂ h hh₁ hh₂ hgh
    refine hG (Sym2.mk_isDiag_iff.not.2 hgh) ⟨⟨a, b, c, ?_⟩, by simpa using And.intro hg₁ hh₁⟩
      ⟨⟨d, e, f, ?_⟩, by simpa using And.intro hg₂ hh₂⟩ <;> simp [*]