-- Mathlib/Combinatorics/SimpleGraph/Triangle/Removal.lean
/-- **Triangle Removal Lemma**. If not all triangles can be removed by removing few edges (on the
order of `(card α)^2`), then there were many triangles to start with (on the order of
`(card α)^3`). -/
lemma FarFromTriangleFree.le_card_cliqueFinset (hG : G.FarFromTriangleFree ε) :
    triangleRemovalBound ε * card α ^ 3 ≤ #(G.cliqueFinset 3)

Proof state:
case inr.inr.inr.intro.intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
hG : G.FarFromTriangleFree ε
h✝ : Nonempty α
hε : 0 < ε
l : ℕ := ⌈4 / ε⌉₊
hl : 4 / ε ≤ ↑l
hl' : l ≤ Fintype.card α
P : Finpartition univ
hP₁ : P.IsEquipartition
hP₂ : l ≤ #P.parts
hP₃ : #P.parts ≤ bound (ε / 8) l
hP₄ : P.IsUniform G (ε / 8)
⊢ triangleRemovalBound ε * ↑(Fintype.card α) ^ 3 ≤ ↑(#(G.cliqueFinset 3))

Tactic:
have : 4/ε ≤ #P.parts := hl.trans (cast_le.2 hP₂)

Result:
case inr.inr.inr.intro.intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
hG : G.FarFromTriangleFree ε
h✝ : Nonempty α
hε : 0 < ε
l : ℕ := ⌈4 / ε⌉₊
hl : 4 / ε ≤ ↑l
hl' : l ≤ Fintype.card α
P : Finpartition univ
hP₁ : P.IsEquipartition
hP₂ : l ≤ #P.parts
hP₃ : #P.parts ≤ bound (ε / 8) l
hP₄ : P.IsUniform G (ε / 8)
this : 4 / ε ≤ ↑(#P.parts)
⊢ triangleRemovalBound ε * ↑(Fintype.card α) ^ 3 ≤ ↑(#(G.cliqueFinset 3))

Proof state:
case inr.inr.inr.intro.intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
hG : G.FarFromTriangleFree ε
h✝ : Nonempty α
hε : 0 < ε
l : ℕ := ⌈4 / ε⌉₊
hl : 4 / ε ≤ ↑l
hl' : l ≤ Fintype.card α
P : Finpartition univ
hP₁ : P.IsEquipartition
hP₂ : l ≤ #P.parts
hP₃ : #P.parts ≤ bound (ε / 8) l
hP₄ : P.IsUniform G (ε / 8)
this : 4 / ε ≤ ↑(#P.parts)
⊢ triangleRemovalBound ε * ↑(Fintype.card α) ^ 3 ≤ ↑(#(G.cliqueFinset 3))

Tactic:
have k := regularityReduced_edges_card_aux hε hP₁ hP₄ this

Result:
case inr.inr.inr.intro.intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
hG : G.FarFromTriangleFree ε
h✝ : Nonempty α
hε : 0 < ε
l : ℕ := ⌈4 / ε⌉₊
hl : 4 / ε ≤ ↑l
hl' : l ≤ Fintype.card α
P : Finpartition univ
hP₁ : P.IsEquipartition
hP₂ : l ≤ #P.parts
hP₃ : #P.parts ≤ bound (ε / 8) l
hP₄ : P.IsUniform G (ε / 8)
this : 4 / ε ≤ ↑(#P.parts)
k : 2 * (↑(#G.edgeFinset) - ↑(#(regularityReduced P G (ε / 8) (ε / 4)).edgeFinset)) < 2 * ε * ↑(Fintype.card α ^ 2)
⊢ triangleRemovalBound ε * ↑(Fintype.card α) ^ 3 ≤ ↑(#(G.cliqueFinset 3))

Proof state:
case inr.inr.inr.intro.intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
hG : G.FarFromTriangleFree ε
h✝ : Nonempty α
hε : 0 < ε
l : ℕ := ⌈4 / ε⌉₊
hl : 4 / ε ≤ ↑l
hl' : l ≤ Fintype.card α
P : Finpartition univ
hP₁ : P.IsEquipartition
hP₂ : l ≤ #P.parts
hP₃ : #P.parts ≤ bound (ε / 8) l
hP₄ : P.IsUniform G (ε / 8)
this : 4 / ε ≤ ↑(#P.parts)
k : 2 * (↑(#G.edgeFinset) - ↑(#(regularityReduced P G (ε / 8) (ε / 4)).edgeFinset)) < 2 * ε * ↑(Fintype.card α ^ 2)
⊢ triangleRemovalBound ε * ↑(Fintype.card α) ^ 3 ≤ ↑(#(G.cliqueFinset 3))

Tactic:
rw [mul_assoc] at k

Result:
case inr.inr.inr.intro.intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
hG : G.FarFromTriangleFree ε
h✝ : Nonempty α
hε : 0 < ε
l : ℕ := ⌈4 / ε⌉₊
hl : 4 / ε ≤ ↑l
hl' : l ≤ Fintype.card α
P : Finpartition univ
hP₁ : P.IsEquipartition
hP₂ : l ≤ #P.parts
hP₃ : #P.parts ≤ bound (ε / 8) l
hP₄ : P.IsUniform G (ε / 8)
this : 4 / ε ≤ ↑(#P.parts)
k : 2 * (↑(#G.edgeFinset) - ↑(#(regularityReduced P G (ε / 8) (ε / 4)).edgeFinset)) < 2 * (ε * ↑(Fintype.card α ^ 2))
⊢ triangleRemovalBound ε * ↑(Fintype.card α) ^ 3 ≤ ↑(#(G.cliqueFinset 3))

Proof state:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
hG : G.FarFromTriangleFree ε
⊢ triangleRemovalBound ε * ↑(Fintype.card α) ^ 3 ≤ ↑(#(G.cliqueFinset 3))

Tactic:
cases isEmpty_or_nonempty α

Result:
case inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
hG : G.FarFromTriangleFree ε
h✝ : IsEmpty α
⊢ triangleRemovalBound ε * ↑(Fintype.card α) ^ 3 ≤ ↑(#(G.cliqueFinset 3))

case inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
hG : G.FarFromTriangleFree ε
h✝ : Nonempty α
⊢ triangleRemovalBound ε * ↑(Fintype.card α) ^ 3 ≤ ↑(#(G.cliqueFinset 3))

Proof state:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
hG : G.FarFromTriangleFree ε
h✝ : Nonempty α
hε : 0 < ε
l : ℕ := ⌈4 / ε⌉₊
hl : 4 / ε ≤ ↑l
hl' : Fintype.card α ≤ l
⊢ triangleRemovalBound ε * ↑(Fintype.card α) ^ 3 ≤ triangleRemovalBound ε * ↑l ^ 3

Tactic:
gcongr

Result:
case a0
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
hG : G.FarFromTriangleFree ε
h✝ : Nonempty α
hε : 0 < ε
l : ℕ := ⌈4 / ε⌉₊
hl : 4 / ε ≤ ↑l
hl' : Fintype.card α ≤ l
⊢ 0 ≤ triangleRemovalBound ε

Proof state:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
hG : G.FarFromTriangleFree ε
h✝ : Nonempty α
hε : 0 < ε
l : ℕ := ⌈4 / ε⌉₊
hl : 4 / ε ≤ ↑l
hl' : l ≤ Fintype.card α
⊢ 0 < ε / 8

Tactic:
positivity

Result:
no goals

Proof state:
case inr.inr.inr.intro.intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
hG : G.FarFromTriangleFree ε
h✝ : Nonempty α
hε : 0 < ε
l : ℕ := ⌈4 / ε⌉₊
hl : 4 / ε ≤ ↑l
hl' : l ≤ Fintype.card α
P : Finpartition univ
hP₁ : P.IsEquipartition
hP₂ : l ≤ #P.parts
hP₃ : #P.parts ≤ bound (ε / 8) l
hP₄ : P.IsUniform G (ε / 8)
this : 4 / ε ≤ ↑(#P.parts)
k : 2 * (↑(#G.edgeFinset) - ↑(#(regularityReduced P G (ε / 8) (ε / 4)).edgeFinset)) < 2 * (ε * ↑(Fintype.card α ^ 2))
⊢ triangleRemovalBound ε * ↑(Fintype.card α) ^ 3 ≤ ↑(#(G.cliqueFinset 3))

Tactic:
replace k := lt_of_mul_lt_mul_left k zero_le_two

Result:
case inr.inr.inr.intro.intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
hG : G.FarFromTriangleFree ε
h✝ : Nonempty α
hε : 0 < ε
l : ℕ := ⌈4 / ε⌉₊
hl : 4 / ε ≤ ↑l
hl' : l ≤ Fintype.card α
P : Finpartition univ
hP₁ : P.IsEquipartition
hP₂ : l ≤ #P.parts
hP₃ : #P.parts ≤ bound (ε / 8) l
hP₄ : P.IsUniform G (ε / 8)
this : 4 / ε ≤ ↑(#P.parts)
k : ↑(#G.edgeFinset) - ↑(#(regularityReduced P G (ε / 8) (ε / 4)).edgeFinset) < ε * ↑(Fintype.card α ^ 2)
⊢ triangleRemovalBound ε * ↑(Fintype.card α) ^ 3 ≤ ↑(#(G.cliqueFinset 3))

Proof state:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
hG : G.FarFromTriangleFree ε
h✝ : Nonempty α
hε : 0 < ε
l : ℕ := ⌈4 / ε⌉₊
hl : 4 / ε ≤ ↑l
hl' : Fintype.card α ≤ l
⊢ 1 ≤ ↑(#(G.cliqueFinset 3))

Tactic:
simpa [one_le_iff_ne_zero] using (hG.cliqueFinset_nonempty hε).card_pos.ne'

Result:
no goals

Proof state:
case inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
hG : G.FarFromTriangleFree ε
h✝ : IsEmpty α
⊢ triangleRemovalBound ε * ↑(Fintype.card α) ^ 3 ≤ ↑(#(G.cliqueFinset 3))

Tactic:
simp [Fintype.card_eq_zero]

Result:
no goals