-- Mathlib/Combinatorics/SimpleGraph/Triangle/Counting.lean
private lemma edgeDensity_badVertices_le (hε : 0 ≤ ε) (dst : 2 * ε ≤ G.edgeDensity s t) :
    G.edgeDensity (badVertices G ε s t) t ≤ G.edgeDensity s t - ε

Proof state:
α : Type u_1
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
s t : Finset α
hε : 0 ≤ ε
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
⊢ ↑(#(G.interedges (SimpleGraph.badVertices G ε s t) t)) ≤
    ↑(#(SimpleGraph.badVertices G ε s t)) * ↑(#t) * (↑(G.edgeDensity s t) - ε)

Tactic:
exact G.card_interedges_badVertices_le

Result:
no goals

Proof state:
α : Type u_1
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
s t : Finset α
hε : 0 ≤ ε
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
⊢ ε ≤ ↑(G.edgeDensity s t)

Tactic:
linarith

Result:
no goals

Proof state:
α : Type u_1
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
s t : Finset α
hε : 0 ≤ ε
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
⊢ 0 ≤ ↑(#(SimpleGraph.badVertices G ε s t)) * ↑(#t)

Tactic:
positivity

Result:
no goals

Proof state:
α : Type u_1
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
s t : Finset α
hε : 0 ≤ ε
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
⊢ ↑(↑(#(G.interedges (SimpleGraph.badVertices G ε s t) t)) / (↑(#(SimpleGraph.badVertices G ε s t)) * ↑(#t))) ≤
    ↑(G.edgeDensity s t) - ε

Tactic:
push_cast

Result:
α : Type u_1
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
s t : Finset α
hε : 0 ≤ ε
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
⊢ ↑(#(G.interedges (SimpleGraph.badVertices G ε s t) t)) / (↑(#(SimpleGraph.badVertices G ε s t)) * ↑(#t)) ≤
    ↑(G.edgeDensity s t) - ε

Proof state:
α : Type u_1
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
s t : Finset α
hε : 0 ≤ ε
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
⊢ ↑(#(G.interedges (SimpleGraph.badVertices G ε s t) t)) / (↑(#(SimpleGraph.badVertices G ε s t)) * ↑(#t)) ≤
    ↑(G.edgeDensity s t) - ε

Tactic:
refine div_le_of_le_mul₀ (by positivity) (sub_nonneg_of_le <| by linarith) ?_

Result:
α : Type u_1
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
s t : Finset α
hε : 0 ≤ ε
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
⊢ ↑(#(G.interedges (SimpleGraph.badVertices G ε s t) t)) ≤
    (↑(G.edgeDensity s t) - ε) * (↑(#(SimpleGraph.badVertices G ε s t)) * ↑(#t))

Proof state:
α : Type u_1
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
s t : Finset α
hε : 0 ≤ ε
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
⊢ ↑(#(G.interedges (SimpleGraph.badVertices G ε s t) t)) ≤
    (↑(G.edgeDensity s t) - ε) * (↑(#(SimpleGraph.badVertices G ε s t)) * ↑(#t))

Tactic:
rw [mul_comm]

Result:
α : Type u_1
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
s t : Finset α
hε : 0 ≤ ε
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
⊢ ↑(#(G.interedges (SimpleGraph.badVertices G ε s t) t)) ≤
    ↑(#(SimpleGraph.badVertices G ε s t)) * ↑(#t) * (↑(G.edgeDensity s t) - ε)

Proof state:
α : Type u_1
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
s t : Finset α
hε : 0 ≤ ε
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
⊢ ↑(G.edgeDensity (SimpleGraph.badVertices G ε s t) t) ≤ ↑(G.edgeDensity s t) - ε

Tactic:
rw [edgeDensity_def]

Result:
α : Type u_1
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
s t : Finset α
hε : 0 ≤ ε
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
⊢ ↑(↑(#(G.interedges (SimpleGraph.badVertices G ε s t) t)) / (↑(#(SimpleGraph.badVertices G ε s t)) * ↑(#t))) ≤
    ↑(G.edgeDensity s t) - ε