-- 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)| < ε
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:
push_cast 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)))

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) ≤
    ↑(#(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:
rw [card_image_of_injective _ (Prod.mk.inj_left _)]

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