-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst_3 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
hUVne : U ≠ V
hUV : ¬G.IsUniform ε U V
t : (star hP G ε hU V).product (star hP G ε hV U) ⊆ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts
hε : 0 ≤ ε
sp : ∀ (a b : Finset (Finset α)), a.product b = a ×ˢ b
refine_3 :
  ∀
    (this :
      HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity U V) : ℝ) 2 - HPow.hPow (β := ℕ) ε 5 / 25 +
          HDiv.hDiv (α := ℝ) (↑(#((star hP G ε hU V).product (star hP G ε hV U))) : ℝ)
              (↑(#((chunk hP G ε hU).parts.product (chunk hP G ε hV).parts)) : ℝ) *
            HPow.hPow (β := ℕ) (3 / 4 * ε) 2 ≤
        HDiv.hDiv (α := ℝ)
          (∑ i ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts,
            HPow.hPow (α := ℝ) (β := ℕ) ((fun (x : Finset α × Finset α) ↦ ((↑(G.edgeDensity x.1 x.2) : ℝ) : ℝ)) i) 2)
          (↑(#((chunk hP G ε hU).parts.product (chunk hP G ε hV).parts)) : ℝ)),
    HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity U V) : ℝ) 2 - HPow.hPow (β := ℕ) ε 5 / 25 +
        HMul.hMul (α := ℝ) (↑(#(star hP G ε hU V)) : ℝ) (↑(#(star hP G ε hV U)) : ℝ) / HPow.hPow (α := ℝ) 16 #P.parts *
            (9 / 16) *
          HPow.hPow (β := ℕ) ε 2 ≤
      (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts,
          HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity ab.1 ab.2) : ℝ) 2) /
        HPow.hPow (α := ℝ) 16 #P.parts
refine_1 :
  3 / 4 * ε ≤
    |HDiv.hDiv (α := ℝ)
          (∑ i ∈ (star hP G ε hU V).product (star hP G ε hV U),
            (fun (x : Finset α × Finset α) ↦ ((↑(G.edgeDensity x.1 x.2) : ℝ) : ℝ)) i)
          (↑(#((star hP G ε hU V).product (star hP G ε hV U))) : ℝ) -
        HDiv.hDiv (α := ℝ)
          (∑ i ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts,
            (fun (x : Finset α × Finset α) ↦ ((↑(G.edgeDensity x.1 x.2) : ℝ) : ℝ)) i)
          (↑(#((chunk hP G ε hU).parts.product (chunk hP G ε hV).parts)) : ℝ)|
refine_2 :
  HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity U V) : ℝ) 2 - HPow.hPow (β := ℕ) ε 5 / 25 ≤
    HPow.hPow (β := ℕ)
      (HDiv.hDiv (α := ℝ)
        (∑ i ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts,
          (fun (x : Finset α × Finset α) ↦ ((↑(G.edgeDensity x.1 x.2) : ℝ) : ℝ)) i)
        (↑(#((chunk hP G ε hU).parts.product (chunk hP G ε hV).parts)) : ℝ))
      2
⊢ HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity U V) : ℝ) 2 - HPow.hPow (β := ℕ) ε 5 / 25 +
      HMul.hMul (α := ℝ) (↑(#(star hP G ε hU V)) : ℝ) (↑(#(star hP G ε hV U)) : ℝ) / HPow.hPow (α := ℝ) 16 #P.parts *
          (9 / 16) *
        HPow.hPow (β := ℕ) ε 2 ≤
    (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts,
        HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity ab.1 ab.2) : ℝ) 2) /
      HPow.hPow (α := ℝ) 16 #P.parts

Tactic:
have := add_div_le_sum_sq_div_card t (fun x => (G.edgeDensity x.1 x.2 : ℝ))
        ((G.edgeDensity U V : ℝ) ^ 2 - ε ^ 5 / ↑25) (show 0 ≤ 3 / 4 * ε by linarith) ?_ ?_