-- 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:
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)| < ε
⊢ ε ^ 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 : ε ≤ G.edgeDensity {y ∈ t | G.Adj x y} {y ∈ u | G.Adj x y} := by
  rw [abs_sub_lt_iff] at this; linarith

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.edgeDensity (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)))

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))
⊢ ε ≤ ↑(G.edgeDensity s t) - ε

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))
⊢ ε ^ 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 := utu (filter_subset (G.Adj x) _) (filter_subset (G.Adj x) _) hY hZ

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)| < ε
⊢ ε ^ 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 : α
hx :
  x ∈ s ∧ x ∉ s ∨
    x ∈ s ∧
      (↑(G.edgeDensity s t) - ε) * ↑(#t) ≤ ↑(#(filter (fun y => G.Adj x y) t)) ∧
        (↑(G.edgeDensity s u) - ε) * ↑(#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:
simp only [false_or, and_not_self, mul_comm (_ - _)] at hx

Result:
α : 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 : α
hx :
  x ∈ s ∧
    ↑(#t) * (↑(G.edgeDensity s t) - ε) ≤ ↑(#(filter (fun y => G.Adj x y) t)) ∧
      ↑(#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))))

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.edgeDensity (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:
rw [edgeDensity_def] at this

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))))
⊢ ε ^ 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)))