-- Mathlib/Combinatorics/SimpleGraph/Triangle/Counting.lean
private lemma card_badVertices_le (dst : 2 * ε ≤ G.edgeDensity s t) (hst : G.IsUniform ε s t) :
    #(badVertices G ε s t) ≤ #s * ε

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

Tactic:
have hε : ε ≤ 1 := (le_rfl.trans <| le_mul_of_one_le_left hst.pos.le (by norm_num)).trans
  (dst.trans <| by exact_mod_cast edgeDensity_le_one _ _ _)

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

Proof state:
α : Type u_1
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
s t : Finset α
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
hst : G.IsUniform ε s t
hε : ε ≤ 1
h : ↑(#s) * ε < ↑(#(SimpleGraph.badVertices G ε s t))
this : |↑(G.edgeDensity (SimpleGraph.badVertices G ε s t) t) - ↑(G.edgeDensity s t)| < ε
⊢ False

Tactic:
rw [abs_sub_lt_iff] at this

Result:
α : Type u_1
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
s t : Finset α
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
hst : G.IsUniform ε s t
hε : ε ≤ 1
h : ↑(#s) * ε < ↑(#(SimpleGraph.badVertices G ε s t))
this :
  ↑(G.edgeDensity (SimpleGraph.badVertices G ε s t) t) - ↑(G.edgeDensity s t) < ε ∧
    ↑(G.edgeDensity s t) - ↑(G.edgeDensity (SimpleGraph.badVertices G ε s t) t) < ε
⊢ False

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

Tactic:
have : |(G.edgeDensity (badVertices G ε s t) t - G.edgeDensity s t : ℝ)| < ε :=
  hst (filter_subset _ _) Subset.rfl h.le (mul_le_of_le_one_right (Nat.cast_nonneg _) hε)

Result:
α : Type u_1
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
s t : Finset α
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
hst : G.IsUniform ε s t
hε : ε ≤ 1
h : ↑(#s) * ε < ↑(#(SimpleGraph.badVertices G ε s t))
this : |↑(G.edgeDensity (SimpleGraph.badVertices G ε s t) t) - ↑(G.edgeDensity s t)| < ε
⊢ False

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

Tactic:
norm_num

Result:
no goals

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

Tactic:
exact_mod_cast edgeDensity_le_one _ _ _

Result:
no goals

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

Tactic:
by_contra! h

Result:
α : Type u_1
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
s t : Finset α
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
hst : G.IsUniform ε s t
hε : ε ≤ 1
h : ↑(#s) * ε < ↑(#(SimpleGraph.badVertices G ε s t))
⊢ False

Proof state:
α : Type u_1
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
s t : Finset α
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
hst : G.IsUniform ε s t
hε : ε ≤ 1
h : ↑(#s) * ε < ↑(#(SimpleGraph.badVertices G ε s t))
this :
  ↑(G.edgeDensity (SimpleGraph.badVertices G ε s t) t) - ↑(G.edgeDensity s t) < ε ∧
    ↑(G.edgeDensity s t) - ↑(G.edgeDensity (SimpleGraph.badVertices G ε s t) t) < ε
⊢ False

Tactic:
linarith [G.edgeDensity_badVertices_le hst.pos.le dst]

Result:
no goals