-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
P : Finpartition (α := Finset α) univ
ε : ℝ
inst_3 : Nonempty α
hε : 0 < ε
hP : P.IsEquipartition
hPε : P.IsUniform G (ε / 8)
hP' : 4 / ε ≤ (↑(#P.parts) : ℝ)
A : Finset (α × α) :=
  (P.nonUniforms G (ε / 8)).biUnion fun (x : Finset α × Finset α) ↦
    match (motive := Finset α × Finset α → Finset (α × α)) x with
    | (U, V) => U ×ˢ V
B : Finset (α × α) := P.parts.biUnion offDiag
C : Finset (α × α) :=
  (P.sparsePairs G (ε / 4)).biUnion fun (x : Finset α × Finset α) ↦
    match (motive := Finset α × Finset α → Finset (α × α)) x with
    | (U, V) => G.interedges U V
_ :
  2 * HSub.hSub (α := ℝ) (↑(#G.edgeFinset) : ℝ) (↑(#(regularityReduced P G (ε / 8) (ε / 4)).edgeFinset) : ℝ) =
    (↑(#({x ∈ SProd.sprod (α := Finset α) (β := Finset α) univ univ |
            match (motive := α × α → Prop) x with
            | (x, y) => G.Adj x y ∧ ¬(regularityReduced P G (ε / 8) (ε / 4)).Adj x y})) :
      ℝ)
_₁ :
  LE.le (α := ℝ)
    (↑(#({x ∈ SProd.sprod (α := Finset α) (β := Finset α) univ univ |
            match (motive := α × α → Prop) x with
            | (x, y) => G.Adj x y ∧ ¬(regularityReduced P G (ε / 8) (ε / 4)).Adj x y})) :
      ℝ)
    (↑(#(A ∪ B ∪ C)) : ℝ)
_₂ : HAdd.hAdd (α := ℝ) (↑(#(A ∪ B)) : ℝ) (↑(#C) : ℝ) ≤ HAdd.hAdd (α := ℝ) (↑(#A) : ℝ) (↑(#B) : ℝ) + (↑(#C) : ℝ)
_₃ :
  HAdd.hAdd (α := ℝ) (↑(#A) : ℝ) (↑(#B) : ℝ) + (↑(#C) : ℝ) <
    4 * (ε / 8) * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 2 + (↑(#B) : ℝ) + (↑(#C) : ℝ)
_₄ :
  4 * (ε / 8) * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 2 + (↑(#B) : ℝ) + (↑(#C) : ℝ) ≤
    4 * (ε / 8) * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 2 +
        ε / 2 * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 2 +
      4 * (ε / 4) * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 2
_₅ :
  4 * (ε / 8) * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 2 +
        ε / 2 * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 2 +
      4 * (ε / 4) * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 2 =
    2 * ε * (↑(HPow.hPow (β := ℕ) (Fintype.card α) 2) : ℝ)
⊢ 2 * HSub.hSub (α := ℝ) (↑(#G.edgeFinset) : ℝ) (↑(#(regularityReduced P G (ε / 8) (ε / 4)).edgeFinset) : ℝ) <
    2 * ε * (↑(HPow.hPow (β := ℕ) (Fintype.card α) 2) : ℝ)

Tactic:
calc
    _ = (#((univ ×ˢ univ).filter fun (x, y) ↦
          G.Adj x y ∧ ¬(G.regularityReduced P (ε / 8) (ε / 4)).Adj x y) : ℝ) := by
      rw [univ_product_univ, mul_sub, filter_and_not, cast_card_sdiff]
      · norm_cast
        rw [two_mul_card_edgeFinset, two_mul_card_edgeFinset]
      · gcongr with xy _
        exact fun hxy ↦ regularityReduced_le hxy
    _ ≤ #(A ∪ B ∪ C) := by gcongr; exact unreduced_edges_subset
    _ ≤ #(A ∪ B) + #C := mod_cast (card_union_le _ _)
    _ ≤ #A + #B + #C := by gcongr; exact mod_cast card_union_le _ _
    _ < 4 * (ε / 8) * card α ^ 2 + _ + _ := by
      gcongr; exact hP.sum_nonUniforms_lt univ_nonempty (by positivity) hPε
    _ ≤ _ + ε / 2 * card α ^ 2 + 4 * (ε / 4) * card α ^ 2 := by
      gcongr
      · exact hP.card_biUnion_offDiag_le hε hP'
      · exact hP.card_interedges_sparsePairs_le (G := G) (ε := ε / 4) (by positivity)
    _ = 2 * ε * (card α ^ 2 : ℕ) := by norm_cast; ring

Premises used: Finset.univ, SProd.sprod, Fintype.card, HDiv.hDiv, Finset.card_union_le, Nat.cast, HPow.hPow, Finset.card, Union.union, OfNat.ofNat, Finset.filter