-- Mathlib/Combinatorics/SimpleGraph/Triangle/Basic.lean
lemma EdgeDisjointTriangles.card_edgeFinset_le (hG : G.EdgeDisjointTriangles) :
    3 * #(G.cliqueFinset 3) ≤ #G.edgeFinset

Proof state:
case refine_1
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : 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 : #{s(a, b), s(a, c), s(b, c)} = 3
⊢ {s(a, b), s(a, c), s(b, c)} ≤ bipartiteAbove (fun s e => ∀ a ∈ e, a ∈ s) G.edgeFinset {a, b, c}

Tactic:
simp [insert_subset, *]

Result:
no goals

Proof state:
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : 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), s(b, c)} = 3

Tactic:
refine card_eq_three.2 ⟨_, _, _, ?_, ?_, ?_, rfl⟩ <;> simp [hab.ne, hac.ne, hbc.ne]

Result:
no goals

Proof state:
case refine_1
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : 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 : #{s(a, b), s(a, c), s(b, c)} = 3
⊢ #{s(a, b), s(a, c), s(b, c)} ≤ #(bipartiteAbove (fun s e => ∀ a ∈ e, a ∈ s) G.edgeFinset {a, b, c})

Tactic:
refine card_mono ?_

Result:
case refine_1
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : 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 : #{s(a, b), s(a, c), s(b, c)} = 3
⊢ {s(a, b), s(a, c), s(b, c)} ≤ bipartiteAbove (fun s e => ∀ a ∈ e, a ∈ s) G.edgeFinset {a, b, c}

Proof state:
case refine_1
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : 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 : #{s(a, b), s(a, c), s(b, c)} = 3
⊢ 3 ≤ #(bipartiteAbove (fun s e => ∀ a ∈ e, a ∈ s) G.edgeFinset {a, b, c})

Tactic:
rw [← this]

Result:
case refine_1
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : 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 : #{s(a, b), s(a, c), s(b, c)} = 3
⊢ #{s(a, b), s(a, c), s(b, c)} ≤ #(bipartiteAbove (fun s e => ∀ a ∈ e, a ∈ s) G.edgeFinset {a, b, c})

Proof state:
case refine_1
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
hG : G.EdgeDisjointTriangles
⊢ ∀ (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 e => ∀ a ∈ e, a ∈ s) G.edgeFinset a)

Tactic:
rintro _ a b c hab hac hbc rfl

Result:
case refine_1
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : 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 e => ∀ a ∈ e, a ∈ s) G.edgeFinset {a, b, c})

Proof state:
case refine_1
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
hG : G.EdgeDisjointTriangles
⊢ ∀ a ∈ G.cliqueFinset 3, 3 ≤ #(bipartiteAbove (fun s e => e ∈ s.sym2) G.edgeFinset a)

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

Result:
case refine_1
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
hG : G.EdgeDisjointTriangles
⊢ ∀ (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 e => ∀ a ∈ e, a ∈ s) G.edgeFinset a)

Proof state:
case refine_2
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
hG : G.EdgeDisjointTriangles
e : Sym2 α
he : e ∈ G.edgeFinset
⊢ #(bipartiteBelow (fun s e => 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)

Result:
no goals

Proof state:
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
hG : G.EdgeDisjointTriangles
⊢ 3 * #(G.cliqueFinset 3) ≤ #G.edgeFinset

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

Result:
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
hG : G.EdgeDisjointTriangles
⊢ #(G.cliqueFinset 3) * 3 ≤ #G.edgeFinset * 1

Proof state:
case refine_1
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : 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 e => ∀ a ∈ e, a ∈ s) G.edgeFinset {a, b, c})

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]

Result:
case refine_1
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : 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 : #{s(a, b), s(a, c), s(b, c)} = 3
⊢ 3 ≤ #(bipartiteAbove (fun s e => ∀ a ∈ e, a ∈ s) G.edgeFinset {a, b, c})

Proof state:
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
hG : G.EdgeDisjointTriangles
⊢ #(G.cliqueFinset 3) * 3 ≤ #G.edgeFinset * 1

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

Result:
case refine_1
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
hG : G.EdgeDisjointTriangles
⊢ ∀ a ∈ G.cliqueFinset 3, 3 ≤ #(bipartiteAbove (fun s e => e ∈ s.sym2) G.edgeFinset a)

case refine_2
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
hG : G.EdgeDisjointTriangles
e : Sym2 α
he : e ∈ G.edgeFinset
⊢ #(bipartiteBelow (fun s e => e ∈ s.sym2) (G.cliqueFinset 3) e) ≤ 1