-- Mathlib/Combinatorics/SimpleGraph/Triangle/Counting.lean
private lemma good_vertices_triangle_card [DecidableEq α] (dst : 2 * ε ≤ G.edgeDensity s t)
    (dsu : 2 * ε ≤ G.edgeDensity s u) (dtu : 2 * ε ≤ G.edgeDensity t u) (utu : G.IsUniform ε t u)
    (x : α) (hx : x ∈ s \ (badVertices G ε s t ∪ badVertices G ε s u)) :
    ε ^ 3 * #t * #u ≤ #((({y ∈ t | G.Adj x y} ×ˢ {y ∈ u | G.Adj x y}).filter
        fun (y, z) ↦ G.Adj y z).image (x, ·))

Proof state:
α : Type u_1
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
inst✝ : DecidableEq α
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
dsu : 2 * ε ≤ ↑(G.edgeDensity s u)
dtu : 2 * ε ≤ ↑(G.edgeDensity t u)
utu : G.IsUniform ε t u
x : α
hxY : ↑(#t) * (↑(G.edgeDensity s t) - ε) ≤ ↑(#(filter (fun y => G.Adj x y) t))
hsu : ↑(#u) * (↑(G.edgeDensity s u) - ε) ≤ ↑(#(filter (fun y => G.Adj x y) u))
hY : ↑(#t) * ε ≤ ↑(#(filter (fun y => G.Adj x y) t))
⊢ ε ≤ ↑(G.edgeDensity s u) - ε

Tactic:
linarith

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
inst✝ : DecidableEq α
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
dsu : 2 * ε ≤ ↑(G.edgeDensity s u)
dtu : 2 * ε ≤ ↑(G.edgeDensity t u)
utu : G.IsUniform ε t u
x : α
hxY : ↑(#t) * (↑(G.edgeDensity s t) - ε) ≤ ↑(#(filter (fun y => G.Adj x y) t))
hsu : ↑(#u) * (↑(G.edgeDensity s u) - ε) ≤ ↑(#(filter (fun y => G.Adj x y) u))
hY : ↑(#t) * ε ≤ ↑(#(filter (fun y => G.Adj x y) t))
hZ : ↑(#u) * ε ≤ ↑(#(filter (fun y => G.Adj x y) u))
this✝ : |↑(G.edgeDensity (filter (G.Adj x) t) (filter (G.Adj x) u)) - ↑(G.edgeDensity t u)| < ε
this :
  ε ≤
    ↑(#(G.interedges (filter (fun y => G.Adj x y) t) (filter (fun y => G.Adj x y) u))) /
      (↑(#(filter (fun y => G.Adj x y) t)) * ↑(#(filter (fun y => G.Adj x y) u)))
⊢ ε ^ 3 * ↑(#t) * ↑(#u) ≤
    ↑(#(filter
          (fun x =>
            match x with
            | (y, z) => G.Adj y z)
          (filter (fun y => G.Adj x y) t ×ˢ filter (fun y => G.Adj x y) u)))

Tactic:
have hε := utu.pos.le

Result:
case intro.intro
α : Type u_1
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
inst✝ : DecidableEq α
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
dsu : 2 * ε ≤ ↑(G.edgeDensity s u)
dtu : 2 * ε ≤ ↑(G.edgeDensity t u)
utu : G.IsUniform ε t u
x : α
hxY : ↑(#t) * (↑(G.edgeDensity s t) - ε) ≤ ↑(#(filter (fun y => G.Adj x y) t))
hsu : ↑(#u) * (↑(G.edgeDensity s u) - ε) ≤ ↑(#(filter (fun y => G.Adj x y) u))
hY : ↑(#t) * ε ≤ ↑(#(filter (fun y => G.Adj x y) t))
hZ : ↑(#u) * ε ≤ ↑(#(filter (fun y => G.Adj x y) u))
this✝ : |↑(G.edgeDensity (filter (G.Adj x) t) (filter (G.Adj x) u)) - ↑(G.edgeDensity t u)| < ε
this :
  ε ≤
    ↑(#(G.interedges (filter (fun y => G.Adj x y) t) (filter (fun y => G.Adj x y) u))) /
      (↑(#(filter (fun y => G.Adj x y) t)) * ↑(#(filter (fun y => G.Adj x y) u)))
hε : 0 ≤ ε
⊢ ε ^ 3 * ↑(#t) * ↑(#u) ≤
    ↑(#(filter
          (fun x =>
            match x with
            | (y, z) => G.Adj y z)
          (filter (fun y => G.Adj x y) t ×ˢ filter (fun y => G.Adj x y) u)))

Proof state:
α : Type u_1
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
inst✝ : DecidableEq α
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
dsu : 2 * ε ≤ ↑(G.edgeDensity s u)
dtu : 2 * ε ≤ ↑(G.edgeDensity t u)
utu : G.IsUniform ε t u
x : α
hxY : ↑(#t) * (↑(G.edgeDensity s t) - ε) ≤ ↑(#(filter (fun y => G.Adj x y) t))
hsu : ↑(#u) * (↑(G.edgeDensity s u) - ε) ≤ ↑(#(filter (fun y => G.Adj x y) u))
hY : ↑(#t) * ε ≤ ↑(#(filter (fun y => G.Adj x y) t))
hZ : ↑(#u) * ε ≤ ↑(#(filter (fun y => G.Adj x y) u))
this :
  ↑(G.edgeDensity (filter (G.Adj x) t) (filter (G.Adj x) u)) - ↑(G.edgeDensity t u) < ε ∧
    ↑(G.edgeDensity t u) - ↑(G.edgeDensity (filter (G.Adj x) t) (filter (G.Adj x) u)) < ε
⊢ ε ≤ ↑(G.edgeDensity (filter (fun y => G.Adj x y) t) (filter (fun y => G.Adj x y) u))

Tactic:
linarith

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
inst✝ : DecidableEq α
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
dsu : 2 * ε ≤ ↑(G.edgeDensity s u)
dtu : 2 * ε ≤ ↑(G.edgeDensity t u)
utu : G.IsUniform ε t u
x : α
hxY : ↑(#t) * (↑(G.edgeDensity s t) - ε) ≤ ↑(#(filter (fun y => G.Adj x y) t))
hsu : ↑(#u) * (↑(G.edgeDensity s u) - ε) ≤ ↑(#(filter (fun y => G.Adj x y) u))
hY : ↑(#t) * ε ≤ ↑(#(filter (fun y => G.Adj x y) t))
hZ : ↑(#u) * ε ≤ ↑(#(filter (fun y => G.Adj x y) u))
this✝ : |↑(G.edgeDensity (filter (G.Adj x) t) (filter (G.Adj x) u)) - ↑(G.edgeDensity t u)| < ε
this :
  ε ≤
    ↑(#(G.interedges (filter (fun y => G.Adj x y) t) (filter (fun y => G.Adj x y) u))) /
      (↑(#(filter (fun y => G.Adj x y) t)) * ↑(#(filter (fun y => G.Adj x y) u)))
hε : 0 ≤ ε
⊢ ε ^ 3 * ↑(#t) * ↑(#u) ≤ ε * (↑(#(filter (fun y => G.Adj x y) t)) * ↑(#(filter (fun y => G.Adj x y) u)))

Tactic:
refine Eq.trans_le ?_
  (mul_le_mul_of_nonneg_left (mul_le_mul hY hZ (by positivity) (by positivity)) hε)

Result:
case intro.intro
α : Type u_1
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
inst✝ : DecidableEq α
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
dsu : 2 * ε ≤ ↑(G.edgeDensity s u)
dtu : 2 * ε ≤ ↑(G.edgeDensity t u)
utu : G.IsUniform ε t u
x : α
hxY : ↑(#t) * (↑(G.edgeDensity s t) - ε) ≤ ↑(#(filter (fun y => G.Adj x y) t))
hsu : ↑(#u) * (↑(G.edgeDensity s u) - ε) ≤ ↑(#(filter (fun y => G.Adj x y) u))
hY : ↑(#t) * ε ≤ ↑(#(filter (fun y => G.Adj x y) t))
hZ : ↑(#u) * ε ≤ ↑(#(filter (fun y => G.Adj x y) u))
this✝ : |↑(G.edgeDensity (filter (G.Adj x) t) (filter (G.Adj x) u)) - ↑(G.edgeDensity t u)| < ε
this :
  ε ≤
    ↑(#(G.interedges (filter (fun y => G.Adj x y) t) (filter (fun y => G.Adj x y) u))) /
      (↑(#(filter (fun y => G.Adj x y) t)) * ↑(#(filter (fun y => G.Adj x y) u)))
hε : 0 ≤ ε
⊢ ε ^ 3 * ↑(#t) * ↑(#u) = ε * (↑(#t) * ε * (↑(#u) * ε))

Proof state:
case intro.intro
α : Type u_1
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
inst✝ : DecidableEq α
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
dsu : 2 * ε ≤ ↑(G.edgeDensity s u)
dtu : 2 * ε ≤ ↑(G.edgeDensity t u)
utu : G.IsUniform ε t u
x : α
hxY : ↑(#t) * (↑(G.edgeDensity s t) - ε) ≤ ↑(#(filter (fun y => G.Adj x y) t))
hsu : ↑(#u) * (↑(G.edgeDensity s u) - ε) ≤ ↑(#(filter (fun y => G.Adj x y) u))
⊢ ε ^ 3 * ↑(#t) * ↑(#u) ≤
    ↑(#(image (fun x_1 => (x, x_1))
          (filter
            (fun x =>
              match x with
              | (y, z) => G.Adj y z)
            (filter (fun y => G.Adj x y) t ×ˢ filter (fun y => G.Adj x y) u))))

Tactic:
have hY : #t * ε ≤ #{y ∈ t | G.Adj x y} :=
  (mul_le_mul_of_nonneg_left (by linarith) (Nat.cast_nonneg _)).trans hxY

Result:
case intro.intro
α : Type u_1
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
inst✝ : DecidableEq α
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
dsu : 2 * ε ≤ ↑(G.edgeDensity s u)
dtu : 2 * ε ≤ ↑(G.edgeDensity t u)
utu : G.IsUniform ε t u
x : α
hxY : ↑(#t) * (↑(G.edgeDensity s t) - ε) ≤ ↑(#(filter (fun y => G.Adj x y) t))
hsu : ↑(#u) * (↑(G.edgeDensity s u) - ε) ≤ ↑(#(filter (fun y => G.Adj x y) u))
hY : ↑(#t) * ε ≤ ↑(#(filter (fun y => G.Adj x y) t))
⊢ ε ^ 3 * ↑(#t) * ↑(#u) ≤
    ↑(#(image (fun x_1 => (x, x_1))
          (filter
            (fun x =>
              match x with
              | (y, z) => G.Adj y z)
            (filter (fun y => G.Adj x y) t ×ˢ filter (fun y => G.Adj x y) u))))