-- Mathlib/Combinatorics/SimpleGraph/Triangle/Basic.lean
lemma LocallyLinear.card_edgeFinset (hG : G.LocallyLinear) :
    #G.edgeFinset = 3 * #(G.cliqueFinset 3)

Proof state:
case refine_2
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : 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 s => 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])

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

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

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

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

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

Tactic:
simp only [subset_iff, Sym2.forall, mem_sym2_iff, le_eq_subset, mem_bipartiteBelow, mem_insert,
  mem_edgeFinset, mem_singleton, and_imp, mem_edgeSet, Sym2.mem_iff, forall_eq_or_imp,
  forall_eq, Quotient.eq, Sym2.rel_iff]

Result:
case refine_2
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
hG : G.LocallyLinear
a b c : α
hab : G.Adj a b
hac : G.Adj a c
hbc : G.Adj b c
⊢ ∀ (x y : α),
    G.Adj x y →
      x = a ∨ x = b ∨ x = c → y = a ∨ y = b ∨ y = c → s(x, y) = s(a, b) ∨ s(x, y) = s(a, c) ∨ s(x, y) = s(b, c)

Proof state:
case refine_2
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
hG : G.LocallyLinear
a b c : α
hab : G.Adj a b
hac : G.Adj a c
hbc : G.Adj b c
⊢ ∀ (x y : α),
    G.Adj x y →
      x = a ∨ x = b ∨ x = c → y = a ∨ y = b ∨ y = c → s(x, y) = s(a, b) ∨ s(x, y) = s(a, c) ∨ s(x, y) = s(b, c)

Tactic:
rintro d e hde (rfl | rfl | rfl) (rfl | rfl | rfl) <;> simp [*] at *

Result:
no goals

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

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

Result:
case refine_2
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
hG : G.LocallyLinear
⊢ ∀ (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 s => e ∈ s.sym2) G.edgeFinset b) ≤ 3

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

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

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

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

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

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

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

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

Result:
no goals

Proof state:
case refine_2
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
hG : G.LocallyLinear
⊢ ∀ (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 s => e ∈ s.sym2) G.edgeFinset b) ≤ 3

Tactic:
rintro _ a b c hab hac hbc rfl

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

Proof state:
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
hG : G.LocallyLinear
a b c : α
hab : G.Adj a b
hac : G.Adj a c
hbc : G.Adj b c
⊢ #{s(b, c)} + 1 = 2

Tactic:
rw [card_singleton]

Result:
no goals