-- Mathlib/Combinatorics/SimpleGraph/Triangle/Removal.lean
/-- **Triangle Removal Lemma**. If there are not too many triangles (on the order of `(card α)^3`)
then they can all be removed by removing a few edges (on the order of `(card α)^2`). -/
lemma triangle_removal (hG : #(G.cliqueFinset 3) < triangleRemovalBound ε * card α ^ 3) :
    ∃ G' ≤ G, ∃ _ : DecidableRel G'.Adj,
      (#G.edgeFinset - #G'.edgeFinset : ℝ) < ε * (card α^2 : ℕ) ∧ G'.CliqueFree 3

Proof state:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
hG : ↑(#(G.cliqueFinset 3)) < triangleRemovalBound ε * ↑(Fintype.card α) ^ 3
⊢ ∃ G' ≤ G, ∃ x, ↑(#G.edgeFinset) - ↑(#G'.edgeFinset) < ε * ↑(Fintype.card α ^ 2) ∧ G'.CliqueFree 3

Tactic:
by_contra! h

Result:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
hG : ↑(#(G.cliqueFinset 3)) < triangleRemovalBound ε * ↑(Fintype.card α) ^ 3
h :
  ∀ G' ≤ G,
    ∀ (x : DecidableRel G'.Adj), ↑(#G.edgeFinset) - ↑(#G'.edgeFinset) < ε * ↑(Fintype.card α ^ 2) → ¬G'.CliqueFree 3
⊢ False

Proof state:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
hG : ↑(#(G.cliqueFinset 3)) < triangleRemovalBound ε * ↑(Fintype.card α) ^ 3
h :
  ∀ G' ≤ G,
    ∀ (x : DecidableRel G'.Adj), ↑(#G.edgeFinset) - ↑(#G'.edgeFinset) < ε * ↑(Fintype.card α ^ 2) → ¬G'.CliqueFree 3
⊢ ∀ ⦃H : SimpleGraph α⦄ [inst : DecidableRel H.Adj],
    H ≤ G → H.CliqueFree 3 → ε * ↑(Fintype.card α ^ 2) ≤ ↑(#G.edgeFinset) - ↑(#H.edgeFinset)

Tactic:
intros G' _ hG hG'

Result:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Fintype α
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
hG✝ : ↑(#(G.cliqueFinset 3)) < triangleRemovalBound ε * ↑(Fintype.card α) ^ 3
h :
  ∀ G' ≤ G,
    ∀ (x : DecidableRel G'.Adj), ↑(#G.edgeFinset) - ↑(#G'.edgeFinset) < ε * ↑(Fintype.card α ^ 2) → ¬G'.CliqueFree 3
G' : SimpleGraph α
inst✝ : DecidableRel G'.Adj
hG : G' ≤ G
hG' : G'.CliqueFree 3
⊢ ε * ↑(Fintype.card α ^ 2) ≤ ↑(#G.edgeFinset) - ↑(#G'.edgeFinset)

Proof state:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
hG : ↑(#(G.cliqueFinset 3)) < triangleRemovalBound ε * ↑(Fintype.card α) ^ 3
h :
  ∀ G' ≤ G,
    ∀ (x : DecidableRel G'.Adj), ↑(#G.edgeFinset) - ↑(#G'.edgeFinset) < ε * ↑(Fintype.card α ^ 2) → ¬G'.CliqueFree 3
⊢ False

Tactic:
refine hG.not_le (farFromTriangleFree_iff.2 ?_).le_card_cliqueFinset

Result:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
hG : ↑(#(G.cliqueFinset 3)) < triangleRemovalBound ε * ↑(Fintype.card α) ^ 3
h :
  ∀ G' ≤ G,
    ∀ (x : DecidableRel G'.Adj), ↑(#G.edgeFinset) - ↑(#G'.edgeFinset) < ε * ↑(Fintype.card α ^ 2) → ¬G'.CliqueFree 3
⊢ ∀ ⦃H : SimpleGraph α⦄ [inst : DecidableRel H.Adj],
    H ≤ G → H.CliqueFree 3 → ε * ↑(Fintype.card α ^ 2) ≤ ↑(#G.edgeFinset) - ↑(#H.edgeFinset)

Proof state:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Fintype α
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
hG✝ : ↑(#(G.cliqueFinset 3)) < triangleRemovalBound ε * ↑(Fintype.card α) ^ 3
h :
  ∀ G' ≤ G,
    ∀ (x : DecidableRel G'.Adj), ↑(#G.edgeFinset) - ↑(#G'.edgeFinset) < ε * ↑(Fintype.card α ^ 2) → ¬G'.CliqueFree 3
G' : SimpleGraph α
inst✝ : DecidableRel G'.Adj
hG : G' ≤ G
hG' : G'.CliqueFree 3
⊢ ε * ↑(Fintype.card α ^ 2) ≤ ↑(#G.edgeFinset) - ↑(#G'.edgeFinset)

Tactic:
exact le_of_not_lt fun i ↦ h G' hG _ i hG'

Result:
no goals