-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Increment (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
inst_3 : Nonempty α
hP : P.IsEquipartition
hP₇ : 7 ≤ #P.parts
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPG : (↑(#P.parts.offDiag) : ℝ) * ε < (↑(#(P.nonUniforms G ε)) : ℝ)
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
rw :
  ∑ x ∈ P.parts.offDiag, HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity x.1 x.2) : ℝ) 2 +
      ((↑(#(P.nonUniforms G ε)) : ℝ) * (HPow.hPow (β := ℕ) ε 4 / 3) -
        (↑(#P.parts.offDiag) : ℝ) * (HPow.hPow (β := ℕ) ε 5 / 25)) =
    HAdd.hAdd (α := ℝ) (∑ x ∈ P.parts.offDiag, HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity x.1 x.2) : ℝ) 2)
      (∑ x ∈ P.parts.offDiag,
        ((if G.IsUniform ε x.1 x.2 then 0 else HPow.hPow (β := ℕ) ε 4 / 3) - HPow.hPow (β := ℕ) ε 5 / 25))
rw₁ :
  ∑ x ∈ P.parts.offDiag, HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity x.1 x.2) : ℝ) 2 +
      ((↑(#(P.nonUniforms G ε)) : ℝ) * (HPow.hPow (β := ℕ) ε 4 / 3) -
        (↑(#P.parts.offDiag) : ℝ) * (HPow.hPow (β := ℕ) ε 5 / 25)) =
    ∑ x ∈ P.parts.offDiag, HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity x.1 x.2) : ℝ) 2 +
      HSub.hSub (α := ℝ) (∑ x ∈ P.parts.offDiag, if G.IsUniform ε x.1 x.2 then 0 else HPow.hPow (β := ℕ) ε 4 / 3)
        (∑ x ∈ P.parts.offDiag, HPow.hPow (β := ℕ) ε 5 / 25)
rw₂ :
  ∑ x ∈ P.parts.offDiag, HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity x.1 x.2) : ℝ) 2 +
      ((↑(#(P.nonUniforms G ε)) : ℝ) * (HPow.hPow (β := ℕ) ε 4 / 3) -
        (↑(#P.parts.offDiag) : ℝ) * (HPow.hPow (β := ℕ) ε 5 / 25)) =
    ∑ x ∈ P.parts.offDiag, HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity x.1 x.2) : ℝ) 2 +
      ((∑ x ∈ P.parts.offDiag, if G.IsUniform ε x.1 x.2 then 0 else HPow.hPow (β := ℕ) ε 4 / 3) -
        #P.parts.offDiag • (HPow.hPow (β := ℕ) ε 5 / 25))
rw₃ :
  ∑ x ∈ P.parts.offDiag, HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity x.1 x.2) : ℝ) 2 +
      ((↑(#(P.nonUniforms G ε)) : ℝ) * (HPow.hPow (β := ℕ) ε 4 / 3) -
        (↑(#P.parts.offDiag) : ℝ) * (HPow.hPow (β := ℕ) ε 5 / 25)) =
    ∑ x ∈ P.parts.offDiag, HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity x.1 x.2) : ℝ) 2 +
      ((∑ x ∈ P.parts.offDiag, if G.IsUniform ε x.1 x.2 then 0 else HPow.hPow (β := ℕ) ε 4 / 3) -
        (↑(#P.parts.offDiag) : ℝ) * (HPow.hPow (β := ℕ) ε 5 / 25))
⊢ ∑ x ∈ P.parts.offDiag, HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity x.1 x.2) : ℝ) 2 +
      ((↑(#(P.nonUniforms G ε)) : ℝ) * (HPow.hPow (β := ℕ) ε 4 / 3) -
        (↑(#P.parts.offDiag) : ℝ) * (HPow.hPow (β := ℕ) ε 5 / 25)) =
    ∑ x ∈ P.parts.offDiag,
      (HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity x.1 x.2) : ℝ) 2 +
        ((if G.IsUniform ε x.1 x.2 then 0 else HPow.hPow (β := ℕ) ε 4 / 3) - HPow.hPow (β := ℕ) ε 5 / 25))
have rw₄ : ∑ x ∈ P.parts.offDiag, HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity x.1 x.2) : ℝ) 2 +
    ((↑(#(P.nonUniforms G ε)) : ℝ) * (HPow.hPow (β := ℕ) ε 4 / 3) -
      (↑(#P.parts.offDiag) : ℝ) * (HPow.hPow (β := ℕ) ε 5 / 25)) =
  ∑ x ∈ P.parts.offDiag, HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity x.1 x.2) : ℝ) 2 +
    (HAdd.hAdd (α := ℝ) (∑ x ∈ P.parts.offDiag with G.IsUniform ε x.1 x.2, 0)
        (∑ x ∈ P.parts.offDiag with ¬G.IsUniform ε x.1 x.2, HPow.hPow (β := ℕ) ε 4 / 3) -
      (↑(#P.parts.offDiag) : ℝ) * (HPow.hPow (β := ℕ) ε 5 / 25))
Tactic: rw [sum_add_distrib, sum_sub_distrib, sum_const, nsmul_eq_mul, sum_ite, sum_const_zero,
          zero_add, sum_const, nsmul_eq_mul, ← Finpartition.nonUniforms, ← add_sub_assoc,
          add_sub_right_comm]