-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card.{u_1} (α := α) univ
dum : Finpartition (α := Finset α) univ
hdum₁ : dum.IsEquipartition
hdum₂ : #dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
inr :
  ∃ (P : Finpartition (α := Finset α) univ),
    P.IsEquipartition ∧
      t ≤ #P.parts ∧
        #P.parts ≤ stepBound^[0] t ∧ (P.IsUniform G ε ∨ HPow.hPow (β := ℕ) ε 5 / 4 * (↑0 : ℝ) ≤ (↑(P.energy G) : ℝ))
inr₁ :
  ∀ (i : ℕ)
    (ih :
      ∃ (P : Finpartition (α := Finset α) univ),
        P.IsEquipartition ∧
          t ≤ #P.parts ∧
            #P.parts ≤ stepBound^[i] t ∧
              (P.IsUniform G ε ∨ HPow.hPow (β := ℕ) ε 5 / 4 * (↑i : ℝ) ≤ (↑(P.energy G) : ℝ))),
    ∃ (P : Finpartition (α := Finset α) univ),
      P.IsEquipartition ∧
        t ≤ #P.parts ∧
          #P.parts ≤ stepBound^[i + 1] t ∧
            (P.IsUniform G ε ∨ HPow.hPow (β := ℕ) ε 5 / 4 * (↑(i + 1) : ℝ) ≤ (↑(P.energy G) : ℝ))
⊢ ∃ (P : Finpartition (α := Finset α) univ),
    P.IsEquipartition ∧
      t ≤ #P.parts ∧
        #P.parts ≤ stepBound^[i] t ∧ (P.IsUniform G ε ∨ HPow.hPow (β := ℕ) ε 5 / 4 * (↑i : ℝ) ≤ (↑(P.energy G) : ℝ))

Tactic:
induction i with
  -- For `i = 0`, the dummy equipartition is enough.
  | zero =>
    refine ⟨dum, hdum₁, hdum₂.ge, hdum₂.le, Or.inr ?_⟩
    rw [Nat.cast_zero, mul_zero]
    exact mod_cast dum.energy_nonneg G
  -- For the induction step at `i + 1`, find `P` the equipartition at `i`.
  | succ i ih =>
  obtain ⟨P, hP₁, hP₂, hP₃, hP₄⟩ := ih
  by_cases huniform : P.IsUniform G ε
  -- If `P` is already uniform, then no need to break it up further. We can just return `P` again.
  · refine ⟨P, hP₁, hP₂, ?_, Or.inl huniform⟩
    rw [iterate_succ_apply']
    exact hP₃.trans (le_stepBound _)
  -- Else, `P` must instead have energy at least `ε ^ 5 / 4 * i`.
  replace hP₄ := hP₄.resolve_left huniform
  -- We gather a few numerical facts.
  have hεl' : 100 ≤ 4 ^ #P.parts * ε ^ 5 :=
    (hundred_lt_pow_initialBound_mul hε l).le.trans
      (mul_le_mul_of_nonneg_right (pow_right_mono₀ (by simp) hP₂) <| by positivity)
  have hi : (i : ℝ) ≤ 4 / ε ^ 5 := by
    have hi : ε ^ 5 / 4 * ↑i ≤ 1 := hP₄.trans (mod_cast P.energy_le_one G)
    rw [div_mul_eq_mul_div, div_le_iff₀ (show (0 : ℝ) < 4 by simp)] at hi
    norm_num at hi
    rwa [le_div_iff₀' (pow_pos hε _)]
  have hsize : #P.parts ≤ stepBound^[⌊4 / ε ^ 5⌋₊] t :=
    hP₃.trans (monotone_iterate_of_id_le le_stepBound (Nat.le_floor hi) _)
  have hPα : #P.parts * 16 ^ #P.parts ≤ card α :=
    (Nat.mul_le_mul hsize (Nat.pow_le_pow_right (by simp) hsize)).trans hα
  -- We return the increment equipartition of `P`, which has energy `≥ ε ^ 5 / 4 * (i + 1)`.
  refine ⟨increment hP₁ G ε, increment_isEquipartition hP₁ G ε, ?_, ?_, Or.inr <| le_trans ?_ <|
    energy_increment hP₁ ((seven_le_initialBound ε l).trans hP₂) hεl' hPα huniform hε.le hε₁⟩
  · rw [card_increment hPα huniform]
    exact hP₂.trans (le_stepBound _)
  · rw [card_increment hPα huniform, iterate_succ_apply']
    exact stepBound_mono hP₃
  · rw [Nat.cast_succ, mul_add, mul_one]
    gcongr

Premises used: Function.iterate_succ_apply', Nat.cast_succ, MulZeroClass.mul_zero, mul_add, Finpartition.energy_nonneg, Nat.cast_zero, mul_one