-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Counting (goal)
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
dst : 2 * ε ≤ (↑(G.edgeDensity s t) : ℝ)
hst : G.IsUniform ε s t
dsu : 2 * ε ≤ (↑(G.edgeDensity s u) : ℝ)
usu : G.IsUniform ε s u
dtu : 2 * ε ≤ (↑(G.edgeDensity t u) : ℝ)
utu : G.IsUniform ε t u
have have₁ have₂ :
  ∀ (h₁ : (↑(#(G.badVertices ε s t)) : ℝ) ≤ (↑(#s) : ℝ) * ε),
    (1 - 2 * ε) * HPow.hPow (β := ℕ) ε 3 * (↑(#s) : ℝ) * (↑(#t) : ℝ) * (↑(#u) : ℝ) ≤
      (↑(#({x ∈ s ×ˢ t ×ˢ u |
              match (motive := α × α × α → Prop) x with
              | (a, b, c) => G.Adj a b ∧ G.Adj a c ∧ G.Adj b c})) :
        ℝ)
have₃ have₄ :
  ∀ (h₁ : (↑(#(G.badVertices ε s t)) : ℝ) ≤ (↑(#s) : ℝ) * ε) (h₂ : (↑(#(G.badVertices ε s u)) : ℝ) ≤ (↑(#s) : ℝ) * ε),
    (1 - 2 * ε) * HPow.hPow (β := ℕ) ε 3 * (↑(#s) : ℝ) * (↑(#t) : ℝ) * (↑(#u) : ℝ) ≤
      (↑(#({x ∈ s ×ˢ t ×ˢ u |
              match (motive := α × α × α → Prop) x with
              | (a, b, c) => G.Adj a b ∧ G.Adj a c ∧ G.Adj b c})) :
        ℝ)
⊢ (1 - 2 * ε) * HPow.hPow (β := ℕ) ε 3 * (↑(#s) : ℝ) * (↑(#t) : ℝ) * (↑(#u) : ℝ) ≤
    (↑(#({x ∈ s ×ˢ t ×ˢ u |
            match (motive := α × α × α → Prop) x with
            | (a, b, c) => G.Adj a b ∧ G.Adj a c ∧ G.Adj b c})) :
      ℝ)
have have₅ : ∀ (h₁ : (↑(#(G.badVertices ε s t)) : ℝ) ≤ (↑(#s) : ℝ) * ε) (h₂ : (↑(#(G.badVertices ε s u)) : ℝ) ≤ (↑(#s) : ℝ) * ε),
  let X' := s \ (G.badVertices ε s t ∪ G.badVertices ε s u);
  ∀
    (this :
      (X'.biUnion fun (x : α) ↦
          image (fun (x_1 : α × α) ↦ (x, x_1)) (G.interedges ({y ∈ t | G.Adj x y}) ({y ∈ u | G.Adj x y}))) ⊆
        {x ∈ s ×ˢ t ×ˢ u |
          match (motive := α × α × α → Prop) x with
          | (a, b, c) => G.Adj a b ∧ G.Adj a c ∧ G.Adj b c}),
    (1 - 2 * ε) * HPow.hPow (β := ℕ) ε 3 * (↑(#s) : ℝ) * (↑(#t) : ℝ) * (↑(#u) : ℝ) ≤
      (↑(#({x ∈ s ×ˢ t ×ˢ u |
              match (motive := α × α × α → Prop) x with
              | (a, b, c) => G.Adj a b ∧ G.Adj a c ∧ G.Adj b c})) :
        ℝ)
Tactic: classical
  have h₁ : #(badVertices G ε s t) ≤ #s * ε := G.card_badVertices_le dst hst
  have h₂ : #(badVertices G ε s u) ≤ #s * ε := G.card_badVertices_le dsu usu
  let X' := s \ (badVertices G ε s t ∪ badVertices G ε s u)
  have : X'.biUnion _ ⊆ (s ×ˢ t ×ˢ u).filter fun (a, b, c) ↦ G.Adj a b ∧ G.Adj a c ∧ G.Adj b c :=
    triangle_split_helper _
  refine le_trans ?_ (Nat.cast_le.2 <| card_le_card this)
  rw [card_biUnion, Nat.cast_sum]
  · apply le_trans _ (card_nsmul_le_sum X' _ _ <| G.good_vertices_triangle_card dst dsu dtu utu)
    rw [nsmul_eq_mul]
    have := hst.pos.le
    suffices hX' : (1 - 2 * ε) * #s ≤ #X' by
      exact Eq.trans_le (by ring) (mul_le_mul_of_nonneg_right hX' <| by positivity)
    have i : badVertices G ε s t ∪ badVertices G ε s u ⊆ s :=
      union_subset (filter_subset _ _) (filter_subset _ _)
    rw [sub_mul, one_mul, card_sdiff_of_subset i, Nat.cast_sub (card_le_card i),
      sub_le_sub_iff_left, mul_assoc, mul_comm ε, two_mul]
    refine (Nat.cast_le.2 <| card_union_le _ _).trans ?_
    rw [Nat.cast_add]
    gcongr
  rintro a _ b _ t
  rw [Function.onFun, Finset.disjoint_left]
  simp only [Prod.forall, mem_image, not_exists, Prod.mk_inj,
    exists_imp, and_imp, not_and]
  aesop