-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Increment
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPG : ¬P.IsUniform G ε
hPα' : stepBound #P.parts ≤ Fintype.card α
hPpos : 0 < stepBound #P.parts
rw :
  #({x ∈ P.parts.attach |
            #(↑x : Finset α) =
              m * HPow.hPow (α := ℕ) 4 #P.parts + (Fintype.card α / #P.parts - m * HPow.hPow (α := ℕ) 4 #P.parts)}) *
        (HPow.hPow (α := ℕ) 4 #P.parts - (Fintype.card α / #P.parts - m * HPow.hPow (α := ℕ) 4 #P.parts) +
          (Fintype.card α / #P.parts - m * HPow.hPow (α := ℕ) 4 #P.parts)) +
      #({x ∈ P.parts.attach |
            ¬#(↑x : Finset α) =
                m * HPow.hPow (α := ℕ) 4 #P.parts + (Fintype.card α / #P.parts - m * HPow.hPow (α := ℕ) 4 #P.parts)}) *
        (HPow.hPow (α := ℕ) 4 #P.parts - (Fintype.card α / #P.parts - m * HPow.hPow (α := ℕ) 4 #P.parts + 1) +
          (Fintype.card α / #P.parts - m * HPow.hPow (α := ℕ) 4 #P.parts + 1)) =
    stepBound #P.parts
rw₁ :
  ∀
    (x :
      ↥({x ∈ P.parts.attach |
          ¬#(↑x : Finset α) =
              m * HPow.hPow (α := ℕ) 4 #P.parts + (Fintype.card α / #P.parts - m * HPow.hPow (α := ℕ) 4 #P.parts)})),
    Membership.mem (γ :=
        Finset
          ↥({x ∈ P.parts.attach |
              ¬#(↑x : Finset α) =
                  m * HPow.hPow (α := ℕ) 4 #P.parts + (Fintype.card α / #P.parts - m * HPow.hPow (α := ℕ) 4 #P.parts)}))
        univ x →
      #(parts
            (equitabilise (P :=
              atomise (↑(↑x : ↥P.parts) : Finset α) (P.nonuniformWitnesses G ε (↑(↑x : ↥P.parts) : Finset α))) ⋯)) =
        HPow.hPow (α := ℕ) 4 #P.parts - (Fintype.card α / #P.parts - m * HPow.hPow (α := ℕ) 4 #P.parts + 1) +
          (Fintype.card α / #P.parts - m * HPow.hPow (α := ℕ) 4 #P.parts + 1)
rw₂ : ℕ
rw₃ :
  ∀
    (x :
      ↥({x ∈ P.parts.attach |
          #(↑x : Finset α) =
            m * HPow.hPow (α := ℕ) 4 #P.parts + (Fintype.card α / #P.parts - m * HPow.hPow (α := ℕ) 4 #P.parts)})),
    Membership.mem (γ :=
        Finset
          ↥({x ∈ P.parts.attach |
              #(↑x : Finset α) =
                m * HPow.hPow (α := ℕ) 4 #P.parts + (Fintype.card α / #P.parts - m * HPow.hPow (α := ℕ) 4 #P.parts)}))
        univ x →
      #(parts
            (equitabilise (P :=
              atomise (↑(↑x : ↥P.parts) : Finset α) (P.nonuniformWitnesses G ε (↑(↑x : ↥P.parts) : Finset α))) ⋯)) =
        HPow.hPow (α := ℕ) 4 #P.parts - (Fintype.card α / #P.parts - m * HPow.hPow (α := ℕ) 4 #P.parts) +
          (Fintype.card α / #P.parts - m * HPow.hPow (α := ℕ) 4 #P.parts)
rw₄ : ℕ
⊢ HAdd.hAdd (α := ℕ)
      (∑ x :
        ↥({x ∈ P.parts.attach | #(↑x : Finset α) = m * 4 ^ #P.parts + (Fintype.card α / #P.parts - m * 4 ^ #P.parts)}),
        #(parts
            (equitabilise (P :=
              atomise (↑(↑x : ↥P.parts) : Finset α) (P.nonuniformWitnesses G ε (↑(↑x : ↥P.parts) : Finset α))) ⋯)))
      (∑ x :
        ↥({x ∈ P.parts.attach | ¬#(↑x : Finset α) = m * 4 ^ #P.parts + (Fintype.card α / #P.parts - m * 4 ^ #P.parts)}),
        #(parts
            (equitabilise (P :=
              atomise (↑(↑x : ↥P.parts) : Finset α) (P.nonuniformWitnesses G ε (↑(↑x : ↥P.parts) : Finset α))) ⋯))) =
    stepBound #P.parts

Tactic:
rw [sum_const_nat, sum_const_nat, univ_eq_attach, univ_eq_attach, card_attach, card_attach]

Premises used: Finset.sum_const_nat, Finset.card_attach, Finset.univ_eq_attach