awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
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 α)
mp₃ : b ∈ (↑{(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}

Tactic:
refine hG.eq ?_ ?_ (Set.Nontrivial.not_subsingleton ⟨a, ?_, b, ?_, hab.ne⟩)

Premises used: SimpleGraph.Adj.ne, Set.Nontrivial.not_subsingleton, And.intro, Exists.intro, Set.Pairwise.eq
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
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
⊢ {(a, b).1, (a, b).2, c} ∈ G.cliqueSet 3

Tactic:
simp [is3Clique_triple_iff, *]

Premises used: SimpleGraph.is3Clique_triple_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
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
⊢ {(a, b).1, (a, b).2, d} ∈ G.cliqueSet 3

Tactic:
simp [is3Clique_triple_iff, *]

Premises used: SimpleGraph.is3Clique_triple_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
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
⊢ a ∈ (↑{(a, b).1, (a, b).2, c} : Set α) ∩ (↑{(a, b).1, (a, b).2, d} : Set α)

Tactic:
simp [is3Clique_triple_iff, *]

Premises used: SimpleGraph.is3Clique_triple_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
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
⊢ b ∈ (↑{(a, b).1, (a, b).2, c} : Set α) ∩ (↑{(a, b).1, (a, b).2, d} : Set α)

Tactic:
simp [is3Clique_triple_iff, *]

Premises used: SimpleGraph.is3Clique_triple_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
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}}
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
⊢ (∀ ⦃e : Sym2 α⦄, ¬e.IsDiag → Set.Subsingleton.{u_1} (α := Finset α) {s : Finset α | s ∈ G.cliqueSet 3 ∧ e ∈ s.sym2}) →
    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]

Premises used: and_imp, Set.mem_inter_iff, forall_exists_index, SimpleGraph.EdgeDisjointTriangles, Ne, Set.Pairwise, SimpleGraph.is3Clique_iff, Set.not_nontrivial_iff, Set.Nontrivial, Finset.mem_coe, not_imp_not, SimpleGraph.mem_cliqueSet_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
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
⊢ Membership.mem (γ := Finset (Sym2 α)) (Finset.sym2 {a, b, c}) s(g, h)

Tactic:
simpa using And.intro hg₁ hh₁

Premises used: And.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
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
⊢ Membership.mem (γ := Finset (Sym2 α)) (Finset.sym2 {d, e, f}) s(g, h)

Tactic:
simpa using And.intro hg₂ hh₂

Premises used: And.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
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}
mpr₁ : G.Adj d e ∧ G.Adj d f ∧ G.Adj e f ∧ Eq (α := Finset α) {d, e, f} {d, e, f}
⊢ Eq (α := Finset α) {a, b, c} {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₂⟩

Premises used: Iff.mpr, Iff.not, And.intro, Sym2.mk_isDiag_iff, Exists.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
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
⊢ G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ Eq (α := Finset α) {a, b, c} {a, b, c}

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
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
⊢ G.Adj d e ∧ G.Adj d f ∧ G.Adj e f ∧ Eq (α := Finset α) {d, e, f} {d, e, f}

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
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
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
⊢ ((↑(G.cliqueFinset 3) : Set (Finset α)).Pairwise fun (x y : Finset α) ↦ #(x ∩ y) ≤ 1) ↔ G.EdgeDisjointTriangles

Tactic:
simp only [coe_cliqueFinset, EdgeDisjointTriangles, Finset.card_le_one, ← coe_inter]

Premises used: SimpleGraph.coe_cliqueFinset, SimpleGraph.EdgeDisjointTriangles, Finset.card_le_one, Finset.coe_inter
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
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.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:
rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableEq α
inst_1 : Fintype α
inst_2 : DecidableRel G.Adj
hG : G.EdgeDisjointTriangles
rw : #(G.cliqueFinset 3) * 3 ≤ #G.edgeFinset * 1
⊢ 3 * #(G.cliqueFinset 3) ≤ #G.edgeFinset

Tactic:
rw [mul_comm, ← mul_one #G.edgeFinset]

Premises used: SimpleGraph.edgeFinset, mul_comm, Finset.card, mul_one
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
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

Tactic:
card_mul_le_card_mul (fun s e ↦ e ∈ s.sym2) ?_ (fun e he ↦ ?_)

Premises used: Membership.mem, Finset.card_mul_le_card_mul
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
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)
refine_2 :
  ∀ (e : Sym2 α) (he : e ∈ G.edgeFinset),
    #(bipartiteBelow (fun (s : Finset α) (e : Sym2 α) ↦ e ∈ s.sym2) (G.cliqueFinset 3) e) ≤ 1
⊢ #(G.cliqueFinset 3) * 3 ≤ #G.edgeFinset * 1

Tactic:
refine card_mul_le_card_mul (fun s e ↦ e ∈ s.sym2) ?_ (fun e he ↦ ?_)

Premises used: Membership.mem, Finset.card_mul_le_card_mul
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableEq α
inst_1 : Fintype α
inst_2 : DecidableRel G.Adj
hG : G.EdgeDisjointTriangles
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)
⊢ ∀ a ∈ G.cliqueFinset 3, 3 ≤ #(bipartiteAbove (fun (s : Finset α) (e : Sym2 α) ↦ e ∈ s.sym2) G.edgeFinset a)

Tactic:
simp only [is3Clique_iff, mem_cliqueFinset_iff, mem_sym2_iff, forall_exists_index, and_imp]

Premises used: and_imp, forall_exists_index, Finset.mem_sym2_iff, SimpleGraph.is3Clique_iff, SimpleGraph.mem_cliqueFinset_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
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

Tactic:
card_eq_three.2 ⟨_, _, _, ?_, ?_, ?_, rfl⟩

Premises used: Iff.mpr, And.intro, Exists.intro, Finset.card_eq_three, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
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)
refine_3 : s(a, c) ≠ s(b, c)
⊢ Finset.card (α := Sym2 α) {s(a, b), s(a, c), s(b, c)} = 3

Tactic:
refine card_eq_three.2 ⟨_, _, _, ?_, ?_, ?_, rfl⟩

Premises used: Iff.mpr, And.intro, Exists.intro, Finset.card_eq_three, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
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
⊢ s(a, b) ≠ s(a, c)

Tactic:
simp [hab.ne, hac.ne, hbc.ne]

Premises used: SimpleGraph.Adj.ne
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
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
⊢ s(a, b) ≠ s(b, c)

Tactic:
simp [hab.ne, hac.ne, hbc.ne]

Premises used: SimpleGraph.Adj.ne
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
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
⊢ s(a, c) ≠ s(b, c)

Tactic:
simp [hab.ne, hac.ne, hbc.ne]

Premises used: SimpleGraph.Adj.ne
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
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

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]
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
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
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})
⊢ 3 ≤ #(bipartiteAbove (fun (s : Finset α) (e : Sym2 α) ↦ ∀ a ∈ e, a ∈ s) G.edgeFinset {a, b, c})

Tactic:
rw [← this]
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
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})

Tactic:
card_mono ?_

Premises used: Finset.card_mono
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
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
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}
⊢ 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:
refine card_mono ?_
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
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
⊢ {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:
simp [insert_subset, *]

Premises used: Finset.insert_subset
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableEq α
inst_1 : Fintype α
inst_2 : DecidableRel G.Adj
hG : G.EdgeDisjointTriangles
e : Sym2 α
he : e ∈ G.edgeFinset
⊢ #(bipartiteBelow (fun (s : Finset α) (e : Sym2 α) ↦ e ∈ s.sym2) (G.cliqueFinset 3) e) ≤ 1

Tactic:
simpa only [card_le_one, mem_bipartiteBelow, and_imp, Set.Subsingleton, Set.mem_setOf_eq,
      mem_cliqueFinset_iff, mem_cliqueSet_iff]
      using hG.mem_sym2_subsingleton (G.not_isDiag_of_mem_edgeSet <| mem_edgeFinset.1 he)

Premises used: and_imp, Finset.card_le_one, Set.mem_setOf_eq, SimpleGraph.mem_cliqueFinset_iff, SimpleGraph.EdgeDisjointTriangles.mem_sym2_subsingleton, Finset.mem_bipartiteBelow, SimpleGraph.mem_edgeFinset, Set.Subsingleton, Iff.mp, SimpleGraph.not_isDiag_of_mem_edgeSet, SimpleGraph.mem_cliqueSet_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
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)

Tactic:
hG.edgeDisjointTriangles.card_edgeFinset_le.antisymm' ?_

Premises used: SimpleGraph.EdgeDisjointTriangles.card_edgeFinset_le, SimpleGraph.LocallyLinear.edgeDisjointTriangles, LE.le.antisymm'
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableEq α
inst_1 : Fintype α
inst_2 : DecidableRel G.Adj
hG : G.LocallyLinear
refine : #G.edgeFinset ≤ 3 * #(G.cliqueFinset 3)
⊢ #G.edgeFinset = 3 * #(G.cliqueFinset 3)

Tactic:
refine hG.edgeDisjointTriangles.card_edgeFinset_le.antisymm' ?_

Premises used: SimpleGraph.EdgeDisjointTriangles.card_edgeFinset_le, SimpleGraph.LocallyLinear.edgeDisjointTriangles, LE.le.antisymm'
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableEq α
inst_1 : Fintype α
inst_2 : DecidableRel G.Adj
hG : G.LocallyLinear
rw : #G.edgeFinset * 1 ≤ #(G.cliqueFinset 3) * 3
⊢ #G.edgeFinset ≤ 3 * #(G.cliqueFinset 3)

Tactic:
rw [← mul_comm, ← mul_one #_]

Premises used: mul_comm, Finset.card, mul_one
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
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

Tactic:
card_mul_le_card_mul (fun e s ↦ e ∈ s.sym2) ?_ ?_

Premises used: Membership.mem, Finset.card_mul_le_card_mul
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableEq α
inst_1 : Fintype α
inst_2 : DecidableRel G.Adj
hG : G.LocallyLinear
refine_1 : ∀ a ∈ G.edgeFinset, 1 ≤ #(bipartiteAbove (fun (e : Sym2 α) (s : Finset α) ↦ e ∈ s.sym2) (G.cliqueFinset 3) a)
refine_2 : ∀ b ∈ G.cliqueFinset 3, #(bipartiteBelow (fun (e : Sym2 α) (s : Finset α) ↦ e ∈ s.sym2) G.edgeFinset b) ≤ 3
⊢ #G.edgeFinset * 1 ≤ #(G.cliqueFinset 3) * 3

Tactic:
refine card_mul_le_card_mul (fun e s ↦ e ∈ s.sym2) ?_ ?_

Premises used: Membership.mem, Finset.card_mul_le_card_mul
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableEq α
inst_1 : Fintype α
inst_2 : DecidableRel G.Adj
hG : G.LocallyLinear
⊢ ∀ a ∈ G.edgeFinset, 1 ≤ #(bipartiteAbove (fun (e : Sym2 α) (s : Finset α) ↦ e ∈ s.sym2) (G.cliqueFinset 3) a)

Tactic:
simpa [Sym2.forall, Nat.one_le_iff_ne_zero, -Finset.card_eq_zero, Finset.card_ne_zero,
        Finset.Nonempty]
      using hG.2

Premises used: Sym2.forall, And.right, Finset.card_eq_zero, Finset.Nonempty, Nat.one_le_iff_ne_zero, Finset.card_ne_zero
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableEq α
inst_1 : Fintype α
inst_2 : DecidableRel G.Adj
hG : G.LocallyLinear
refine_2 :
  ∀ (b : Finset α) (x x_1 x_2 : α),
    G.Adj x x_1 →
      G.Adj x x_2 →
        G.Adj x_1 x_2 →
          b = {x, x_1, x_2} → #(bipartiteBelow (fun (e : Sym2 α) (s : Finset α) ↦ e ∈ s.sym2) G.edgeFinset b) ≤ 3
⊢ ∀ b ∈ G.cliqueFinset 3, #(bipartiteBelow (fun (e : Sym2 α) (s : Finset α) ↦ e ∈ s.sym2) G.edgeFinset b) ≤ 3

Tactic:
simp only [mem_cliqueFinset_iff, is3Clique_iff, forall_exists_index, and_imp]

Premises used: and_imp, forall_exists_index, SimpleGraph.is3Clique_iff, SimpleGraph.mem_cliqueFinset_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableEq α
inst_1 : Fintype α
inst_2 : DecidableRel G.Adj
hG : G.LocallyLinear
a b c : α
hab : G.Adj a b
hac : G.Adj a c
hbc : G.Adj b c
⊢ #(bipartiteBelow (fun (e : Sym2 α) (s : Finset α) ↦ e ∈ s.sym2) G.edgeFinset {a, b, c}) ≤
    Finset.card (α := Sym2 α) {s(a, b), s(a, c), s(b, c)}

Tactic:
card_le_card ?_

Premises used: Finset.card_le_card
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableEq α
inst_1 : Fintype α
inst_2 : DecidableRel G.Adj
hG : G.LocallyLinear
a b c : α
hab : G.Adj a b
hac : G.Adj a c
hbc : G.Adj b c
rw rw₁ : HAdd.hAdd (α := ℕ) 1 1 = 2
⊢ Finset.card (α := Sym2 α) {s(b, c)} + 1 = 2

Tactic:
rw [card_singleton]

Premises used: Finset.card_singleton
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableEq α
inst_1 : Fintype α
inst_2 : DecidableRel G.Adj
hG : G.LocallyLinear
a b c : α
hab : G.Adj a b
hac : G.Adj a c
hbc : G.Adj b c
refine_2 :
  bipartiteBelow (fun (e : Sym2 α) (s : Finset α) ↦ e ∈ s.sym2) G.edgeFinset {a, b, c} ⊆ {s(a, b), s(a, c), s(b, c)}
⊢ #(bipartiteBelow (fun (e : Sym2 α) (s : Finset α) ↦ e ∈ s.sym2) G.edgeFinset {a, b, c}) ≤ 3

Tactic:
calc
    _ ≤ #{s(a, b), s(a, c), s(b, c)} := card_le_card ?_
    _ ≤ 3 := (card_insert_le _ _).trans (succ_le_succ <| (card_insert_le _ _).trans_eq <| by
      rw [card_singleton])

Premises used: LE.le.trans_eq, Finset.card_le_card, Finset.card_insert_le, LE.le.trans, Nat.succ_le_succ