awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (hypothesis)
Goal:
α : Type u_1
G : SimpleGraph α
⊢ G.EdgeDisjointTriangles ↔
    ∀ ⦃e : Sym2 α⦄, ¬e.IsDiag → Set.Subsingleton.{u_1} (α := Finset α) {s : Finset α | s ∈ G.cliqueSet 3 ∧ e ∈ s.sym2}
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}}
Tactic: 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 [*]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (goal)
Goal:
α : Type u_1
G : SimpleGraph α
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 mp : G.EdgeDisjointTriangles →
  ∀ ⦃e : Sym2 α⦄, ¬e.IsDiag → Set.Subsingleton.{u_1} (α := Finset α) {s : Finset α | s ∈ G.cliqueSet 3 ∧ e ∈ s.sym2}
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (goal)
Goal:
α : Type u_1
G : SimpleGraph α
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}}
mp :
  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 : (∀ ⦃e : Sym2 α⦄, ¬e.IsDiag → Set.Subsingleton.{u_1} (α := Finset α) {s : Finset α | s ∈ G.cliqueSet 3 ∧ e ∈ s.sym2}) →
  G.EdgeDisjointTriangles
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (goal)
Goal:
α : Type u_1
G : SimpleGraph α
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 mp : G.EdgeDisjointTriangles →
  ∀ (x y : α),
    ¬s(x, y).IsDiag → Set.Subsingleton.{u_1} (α := Finset α) {s : Finset α | s ∈ G.cliqueSet 3 ∧ s(x, y) ∈ s.sym2}
Tactic: rw [Sym2.forall]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (hypothesis)
Goal:
α : Type u_1
G : SimpleGraph α
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}}
hG : G.EdgeDisjointTriangles
a b : α
hab : ¬s(a, b).IsDiag
⊢ Set.Subsingleton.{u_1} (α := Finset α) {s : Finset α | s ∈ G.cliqueSet 3 ∧ s(a, b) ∈ s.sym2}
have hab₁ : ¬a = b
Tactic: simp only [Sym2.mk_isDiag_iff] at hab
Cleared hypotheses: hab
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (goal)
Goal:
α : Type u_1
G : SimpleGraph α
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}}
hG : G.EdgeDisjointTriangles
a b : α
hab : ¬a = b
⊢ Set.Subsingleton.{u_1} (α := Finset α) {s : Finset α | s ∈ G.cliqueSet 3 ∧ s(a, b) ∈ s.sym2}
have mp : Set.Subsingleton.{u_1} (α := Finset α)
  {s : Finset α |
    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}}
Tactic: rw [this _ _ (Sym2.mk_isDiag_iff.not.2 hab)]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (goal)
Goal:
α : Type u_1
G : SimpleGraph α
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}}
hG : G.EdgeDisjointTriangles
a b : α
hab_1 : ¬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
⊢ Eq (α := Finset α) {(a, b).1, (a, b).2, c} {(a, b).1, (a, b).2, d}
have mp : {(a, b).1, (a, b).2, c} ∈ G.cliqueSet 3
Tactic: refine hG.eq ?_ ?_ (Set.Nontrivial.not_subsingleton ⟨a, ?_, b, ?_, hab.ne⟩)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (goal)
Goal:
α : Type u_1
G : SimpleGraph α
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}}
hG : G.EdgeDisjointTriangles
a b : α
hab_1 : ¬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
mp : {(a, b).1, (a, b).2, c} ∈ G.cliqueSet 3
⊢ Eq (α := Finset α) {(a, b).1, (a, b).2, c} {(a, b).1, (a, b).2, d}
have mp₁ : {(a, b).1, (a, b).2, d} ∈ G.cliqueSet 3
Tactic: refine hG.eq ?_ ?_ (Set.Nontrivial.not_subsingleton ⟨a, ?_, b, ?_, hab.ne⟩)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (goal)
Goal:
α : Type u_1
G : SimpleGraph α
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}}
hG : G.EdgeDisjointTriangles
a b : α
hab_1 : ¬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
mp : {(a, b).1, (a, b).2, c} ∈ G.cliqueSet 3
mp₁ : {(a, b).1, (a, b).2, d} ∈ G.cliqueSet 3
⊢ Eq (α := Finset α) {(a, b).1, (a, b).2, c} {(a, b).1, (a, b).2, d}
have mp₂ : a ∈ (↑{(a, b).1, (a, b).2, c} : Set α) ∩ (↑{(a, b).1, (a, b).2, d} : Set α)
Tactic: refine hG.eq ?_ ?_ (Set.Nontrivial.not_subsingleton ⟨a, ?_, b, ?_, hab.ne⟩)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (goal)
Goal:
α : Type u_1
G : SimpleGraph α
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}}
hG : G.EdgeDisjointTriangles
a b : α
hab_1 : ¬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
mp : {(a, b).1, (a, b).2, c} ∈ G.cliqueSet 3
mp₁ : {(a, b).1, (a, b).2, d} ∈ G.cliqueSet 3
mp₂ : a ∈ (↑{(a, b).1, (a, b).2, c} : Set α) ∩ (↑{(a, b).1, (a, b).2, d} : Set α)
⊢ Eq (α := Finset α) {(a, b).1, (a, b).2, c} {(a, b).1, (a, b).2, d}
have mp₃ : b ∈ (↑{(a, b).1, (a, b).2, c} : Set α) ∩ (↑{(a, b).1, (a, b).2, d} : Set α)
Tactic: refine hG.eq ?_ ?_ (Set.Nontrivial.not_subsingleton ⟨a, ?_, b, ?_, hab.ne⟩)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (goal)
Goal:
α : Type u_1
G : SimpleGraph α
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
have mpr : (∀ ⦃e : Sym2 α⦄,
    ¬e.IsDiag →
      Set.Subsingleton.{u_1} (α := Finset α)
        {s : Finset α | (∃ (a : α) (b : α) (c : α), G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}) ∧ e ∈ s.sym2}) →
  ∀ ⦃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: 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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (goal)
Goal:
α : Type u_1
G : SimpleGraph α
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}}
hG :
  ∀ ⦃e : Sym2 α⦄,
    ¬e.IsDiag →
      Set.Subsingleton.{u_1} (α := Finset α)
        {s : Finset α | (∃ (a : α) (b : α) (c : α), G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}) ∧ e ∈ s.sym2}
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₁ : Membership.mem (γ := Finset α) {a, b, c} g
hg₂ : Membership.mem (γ := Finset α) {d, e, f} g
h : α
hh₁ : Membership.mem (γ := Finset α) {a, b, c} h
hh₂ : Membership.mem (γ := Finset α) {d, e, f} h
hgh : ¬g = h
⊢ Eq (α := Finset α) {a, b, c} {d, e, f}
have mpr : G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ Eq (α := Finset α) {a, b, c} {a, b, c}
Tactic: 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₂⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (goal)
Goal:
α : Type u_1
G : SimpleGraph α
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}}
hG :
  ∀ ⦃e : Sym2 α⦄,
    ¬e.IsDiag →
      Set.Subsingleton.{u_1} (α := Finset α)
        {s : Finset α | (∃ (a : α) (b : α) (c : α), G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}) ∧ e ∈ s.sym2}
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₁ : Membership.mem (γ := Finset α) {a, b, c} g
hg₂ : Membership.mem (γ := Finset α) {d, e, f} g
h : α
hh₁ : Membership.mem (γ := Finset α) {a, b, c} h
hh₂ : Membership.mem (γ := Finset α) {d, e, f} h
hgh : ¬g = h
mpr : G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ Eq (α := Finset α) {a, b, c} {a, b, c}
⊢ Eq (α := Finset α) {a, b, c} {d, e, f}
have mpr₁ : G.Adj d e ∧ G.Adj d f ∧ G.Adj e f ∧ Eq (α := Finset α) {d, e, f} {d, e, f}
Tactic: 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₂⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (goal)
Goal:
α : Type u_1
G : SimpleGraph α
⊢ G.EdgeDisjointTriangles ↔
    ∀ ⦃e : Sym2 α⦄, ¬e.IsDiag → Set.Subsingleton.{u_1} (α := Finset α) {s : Finset α | s ∈ G.cliqueSet 3 ∧ e ∈ s.sym2}
have 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}}
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 [*]
-- 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}}
⊢ G.EdgeDisjointTriangles ↔
    ∀ ⦃e : Sym2 α⦄, ¬e.IsDiag → Set.Subsingleton.{u_1} (α := Finset α) {s : Finset α | s ∈ G.cliqueSet 3 ∧ e ∈ s.sym2}
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}
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 [*]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
G H : SimpleGraph α
ε δ : 𝕜
inst_3 : DecidableEq α
inst_4 : Fintype α
inst_5 : DecidableRel G.Adj
⊢ ((↑(G.cliqueFinset 3) : Set (Finset α)).Pairwise fun (x y : Finset α) ↦ #(x ∩ y) ≤ 1) ↔ G.EdgeDisjointTriangles
have simp : ((G.cliqueSet 3).Pairwise fun (x y : Finset α) ↦ ∀ a ∈ x ∩ y, ∀ b ∈ x ∩ y, a = b) ↔
  (G.cliqueSet 3).Pairwise fun (x y : Finset α) ↦ (↑(x ∩ y) : Set α).Subsingleton
Tactic: simp only [coe_cliqueFinset, EdgeDisjointTriangles, Finset.card_le_one, ← coe_inter]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (goal)
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableEq α
inst_1 : Fintype α
inst_2 : DecidableRel G.Adj
hG : G.EdgeDisjointTriangles
⊢ 3 * #(G.cliqueFinset 3) ≤ #G.edgeFinset
have rw : #(G.cliqueFinset 3) * 3 ≤ #G.edgeFinset * 1
Tactic: rw [mul_comm, ← mul_one #G.edgeFinset]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (goal)
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableEq α
inst_1 : Fintype α
inst_2 : DecidableRel G.Adj
hG : G.EdgeDisjointTriangles
⊢ #(G.cliqueFinset 3) * 3 ≤ #G.edgeFinset * 1
have refine_1 : ∀ a ∈ G.cliqueFinset 3, 3 ≤ #(bipartiteAbove (fun (s : Finset α) (e : Sym2 α) ↦ e ∈ s.sym2) G.edgeFinset a)
Tactic: refine card_mul_le_card_mul (fun s e ↦ e ∈ s.sym2) ?_ (fun e he ↦ ?_)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (goal)
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableEq α
inst_1 : Fintype α
inst_2 : DecidableRel G.Adj
hG : G.EdgeDisjointTriangles
refine_1 : ∀ a ∈ G.cliqueFinset 3, 3 ≤ #(bipartiteAbove (fun (s : Finset α) (e : Sym2 α) ↦ e ∈ s.sym2) G.edgeFinset a)
⊢ #(G.cliqueFinset 3) * 3 ≤ #G.edgeFinset * 1
have refine_2 : ∀ (e : Sym2 α) (he : e ∈ G.edgeFinset),
  #(bipartiteBelow (fun (s : Finset α) (e : Sym2 α) ↦ e ∈ s.sym2) (G.cliqueFinset 3) e) ≤ 1
Tactic: refine card_mul_le_card_mul (fun s e ↦ e ∈ s.sym2) ?_ (fun e he ↦ ?_)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (goal)
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableEq α
inst_1 : Fintype α
inst_2 : DecidableRel G.Adj
hG : G.EdgeDisjointTriangles
⊢ ∀ a ∈ G.cliqueFinset 3, 3 ≤ #(bipartiteAbove (fun (s : Finset α) (e : Sym2 α) ↦ e ∈ s.sym2) G.edgeFinset a)
have refine_1 : ∀ (a : Finset α) (x x_1 x_2 : α),
  G.Adj x x_1 →
    G.Adj x x_2 →
      G.Adj x_1 x_2 →
        a = {x, x_1, x_2} → 3 ≤ #(bipartiteAbove (fun (s : Finset α) (e : Sym2 α) ↦ ∀ a ∈ e, a ∈ s) G.edgeFinset a)
Tactic: simp only [is3Clique_iff, mem_cliqueFinset_iff, mem_sym2_iff, forall_exists_index, and_imp]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (goal)
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableEq α
inst_1 : Fintype α
inst_2 : DecidableRel G.Adj
hG : G.EdgeDisjointTriangles
a b c : α
hab : G.Adj a b
hac : G.Adj a c
hbc : G.Adj b c
⊢ Finset.card (α := Sym2 α) {s(a, b), s(a, c), s(b, c)} = 3
have refine_1 : s(a, b) ≠ s(a, c)
Tactic: refine card_eq_three.2 ⟨_, _, _, ?_, ?_, ?_, rfl⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (goal)
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableEq α
inst_1 : Fintype α
inst_2 : DecidableRel G.Adj
hG : G.EdgeDisjointTriangles
a b c : α
hab : G.Adj a b
hac : G.Adj a c
hbc : G.Adj b c
refine_1 : s(a, b) ≠ s(a, c)
⊢ Finset.card (α := Sym2 α) {s(a, b), s(a, c), s(b, c)} = 3
have refine_2 : s(a, b) ≠ s(b, c)
Tactic: refine card_eq_three.2 ⟨_, _, _, ?_, ?_, ?_, rfl⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (goal)
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableEq α
inst_1 : Fintype α
inst_2 : DecidableRel G.Adj
hG : G.EdgeDisjointTriangles
a b c : α
hab : G.Adj a b
hac : G.Adj a c
hbc : G.Adj b c
refine_1 : s(a, b) ≠ s(a, c)
refine_2 : s(a, b) ≠ s(b, c)
⊢ Finset.card (α := Sym2 α) {s(a, b), s(a, c), s(b, c)} = 3
have refine_3 : s(a, c) ≠ s(b, c)
Tactic: refine card_eq_three.2 ⟨_, _, _, ?_, ?_, ?_, rfl⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (hypothesis)
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableEq α
inst_1 : Fintype α
inst_2 : DecidableRel G.Adj
hG : G.EdgeDisjointTriangles
a b c : α
hab : G.Adj a b
hac : G.Adj a c
hbc : G.Adj b c
⊢ 3 ≤ #(bipartiteAbove (fun (s : Finset α) (e : Sym2 α) ↦ ∀ a ∈ e, a ∈ s) G.edgeFinset {a, b, c})
have this : Finset.card (α := Sym2 α) {s(a, b), s(a, c), s(b, c)} = 3
Tactic: have : #{s(a, b), s(a, c), s(b, c)} = 3 := by
      refine card_eq_three.2 ⟨_, _, _, ?_, ?_, ?_, rfl⟩ <;> simp [hab.ne, hac.ne, hbc.ne]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (goal)
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableEq α
inst_1 : Fintype α
inst_2 : DecidableRel G.Adj
hG : G.EdgeDisjointTriangles
a b c : α
hab : G.Adj a b
hac : G.Adj a c
hbc : G.Adj b c
this : Finset.card (α := Sym2 α) {s(a, b), s(a, c), s(b, c)} = 3
⊢ 3 ≤ #(bipartiteAbove (fun (s : Finset α) (e : Sym2 α) ↦ ∀ a ∈ e, a ∈ s) G.edgeFinset {a, b, c})
have refine_1 : Finset.card (α := Sym2 α) {s(a, b), s(a, c), s(b, c)} ≤
  #(bipartiteAbove (fun (s : Finset α) (e : Sym2 α) ↦ ∀ a ∈ e, a ∈ s) G.edgeFinset {a, b, c})
Tactic: rw [← this]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (goal)
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableEq α
inst_1 : Fintype α
inst_2 : DecidableRel G.Adj
hG : G.EdgeDisjointTriangles
a b c : α
hab : G.Adj a b
hac : G.Adj a c
hbc : G.Adj b c
this : Finset.card (α := Sym2 α) {s(a, b), s(a, c), s(b, c)} = 3
⊢ Finset.card (α := Sym2 α) {s(a, b), s(a, c), s(b, c)} ≤
    #(bipartiteAbove (fun (s : Finset α) (e : Sym2 α) ↦ ∀ a ∈ e, a ∈ s) G.edgeFinset {a, b, c})
have refine_1 : {s(a, b), s(a, c), s(b, c)} ≤ bipartiteAbove (fun (s : Finset α) (e : Sym2 α) ↦ ∀ a ∈ e, a ∈ s) G.edgeFinset {a, b, c}
Tactic: refine card_mono ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (goal)
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableEq α
inst_1 : Fintype α
inst_2 : DecidableRel G.Adj
hG : G.LocallyLinear
⊢ #G.edgeFinset = 3 * #(G.cliqueFinset 3)
have refine : #G.edgeFinset ≤ 3 * #(G.cliqueFinset 3)
Tactic: refine hG.edgeDisjointTriangles.card_edgeFinset_le.antisymm' ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (goal)
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableEq α
inst_1 : Fintype α
inst_2 : DecidableRel G.Adj
hG : G.LocallyLinear
⊢ #G.edgeFinset ≤ 3 * #(G.cliqueFinset 3)
have rw : #G.edgeFinset * 1 ≤ #(G.cliqueFinset 3) * 3
Tactic: rw [← mul_comm, ← mul_one #_]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (goal)
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableEq α
inst_1 : Fintype α
inst_2 : DecidableRel G.Adj
hG : G.LocallyLinear
⊢ #G.edgeFinset * 1 ≤ #(G.cliqueFinset 3) * 3
have refine_1 : ∀ a ∈ G.edgeFinset, 1 ≤ #(bipartiteAbove (fun (e : Sym2 α) (s : Finset α) ↦ e ∈ s.sym2) (G.cliqueFinset 3) a)
Tactic: refine card_mul_le_card_mul (fun e s ↦ e ∈ s.sym2) ?_ ?_