-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Increment (goal)
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₂ : ℕ
⊢ 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
have 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 α))) sorry)) =
      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)
Tactic: rw [sum_const_nat, sum_const_nat, univ_eq_attach, univ_eq_attach, card_attach, card_attach]