awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma (goal)
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
inr :
  ∀ (hε₁ : 1 ≤ ε),
    ∃ (P : Finpartition (α := Finset α) univ), P.IsEquipartition ∧ l ≤ #P.parts ∧ #P.parts ≤ bound ε l ∧ P.IsUniform G ε
⊢ ∃ (P : Finpartition (α := Finset α) univ), P.IsEquipartition ∧ l ≤ #P.parts ∧ #P.parts ≤ bound ε l ∧ P.IsUniform G ε
have inr₁ : ∀ (hε₁ : ε ≤ 1),
  ∃ (P : Finpartition (α := Finset α) univ), P.IsEquipartition ∧ l ≤ #P.parts ∧ #P.parts ≤ bound ε l ∧ P.IsUniform G ε
Tactic: obtain hε₁ | hε₁ := le_total 1 ε
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma (goal)
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
⊢ Nonempty α
have rw : 0 < Fintype.card α
Tactic: rw [← Fintype.card_pos_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma (hypothesis)
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
⊢ ∃ (P : Finpartition (α := Finset α) univ), P.IsEquipartition ∧ l ≤ #P.parts ∧ #P.parts ≤ bound ε l ∧ P.IsUniform G ε
have this : Nonempty α
Tactic: have : Nonempty α := by
    rw [← Fintype.card_pos_iff]
    exact (bound_pos _ _).trans_le hα
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma (goal)
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 α
h :
  ∀ (i : ℕ),
    ∃ (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 ∧ l ≤ #P.parts ∧ #P.parts ≤ bound ε l ∧ P.IsUniform G ε
have obtain : ∀ (P : Finpartition (α := Finset α) univ) (hP₁ : P.IsEquipartition) (hP₂ : t ≤ #P.parts)
  (hP₃ : #P.parts ≤ stepBound^[⌊4 / HPow.hPow (β := ℕ) ε 5⌋₊ + 1] t)
  (hP₄ :
    P.IsUniform G ε ∨ HPow.hPow (β := ℕ) ε 5 / 4 * (↑(⌊4 / HPow.hPow (β := ℕ) ε 5⌋₊ + 1) : ℝ) ≤ (↑(P.energy G) : ℝ)),
  ∃ (P : Finpartition (α := Finset α) univ), P.IsEquipartition ∧ l ≤ #P.parts ∧ #P.parts ≤ bound ε l ∧ P.IsUniform G ε
Tactic: obtain ⟨P, hP₁, hP₂, hP₃, hP₄⟩ := h (⌊4 / ε ^ 5⌋₊ + 1)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma (goal)
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 α
h :
  ∀ (i : ℕ),
    ∃ (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
hP₁ : P.IsEquipartition
hP₂ : t ≤ #P.parts
hP₃ : #P.parts ≤ stepBound^[⌊4 / HPow.hPow (β := ℕ) ε 5⌋₊ + 1] t
hP₄ : P.IsUniform G ε ∨ HPow.hPow (β := ℕ) ε 5 / 4 * (↑(⌊4 / HPow.hPow (β := ℕ) ε 5⌋₊ + 1) : ℝ) ≤ (↑(P.energy G) : ℝ)
⊢ ∃ (P : Finpartition (α := Finset α) univ), P.IsEquipartition ∧ l ≤ #P.parts ∧ #P.parts ≤ bound ε l ∧ P.IsUniform G ε
have refine_1 : stepBound^[⌊4 / HPow.hPow (β := ℕ) ε 5⌋₊ + 1] t ≤ bound ε l
Tactic: refine ⟨P, hP₁, (le_initialBound _ _).trans hP₂, hP₃.trans ?_,
      hP₄.resolve_right fun hPenergy => lt_irrefl (1 : ℝ) ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma (goal)
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 α
h :
  ∀ (i : ℕ),
    ∃ (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
hP₁ : P.IsEquipartition
hP₂ : t ≤ #P.parts
hP₃ : #P.parts ≤ stepBound^[⌊4 / HPow.hPow (β := ℕ) ε 5⌋₊ + 1] t
hP₄ : P.IsUniform G ε ∨ HPow.hPow (β := ℕ) ε 5 / 4 * (↑(⌊4 / HPow.hPow (β := ℕ) ε 5⌋₊ + 1) : ℝ) ≤ (↑(P.energy G) : ℝ)
refine_1 : stepBound^[⌊4 / HPow.hPow (β := ℕ) ε 5⌋₊ + 1] t ≤ bound ε l
⊢ ∃ (P : Finpartition (α := Finset α) univ), P.IsEquipartition ∧ l ≤ #P.parts ∧ #P.parts ≤ bound ε l ∧ P.IsUniform G ε
have refine_2 : ∀ (hPenergy : HPow.hPow (β := ℕ) ε 5 / 4 * (↑(⌊4 / HPow.hPow (β := ℕ) ε 5⌋₊ + 1) : ℝ) ≤ (↑(P.energy G) : ℝ)),
  LT.lt (α := ℝ) 1 1
Tactic: refine ⟨P, hP₁, (le_initialBound _ _).trans hP₂, hP₃.trans ?_,
      hP₄.resolve_right fun hPenergy => lt_irrefl (1 : ℝ) ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma (goal)
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 α
h :
  ∀ (i : ℕ),
    ∃ (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
hP₁ : P.IsEquipartition
hP₂ : t ≤ #P.parts
hP₃ : #P.parts ≤ stepBound^[⌊4 / HPow.hPow (β := ℕ) ε 5⌋₊ + 1] t
hP₄ : P.IsUniform G ε ∨ HPow.hPow (β := ℕ) ε 5 / 4 * (↑(⌊4 / HPow.hPow (β := ℕ) ε 5⌋₊ + 1) : ℝ) ≤ (↑(P.energy G) : ℝ)
⊢ stepBound^[⌊4 / HPow.hPow (β := ℕ) ε 5⌋₊ + 1] t ≤ bound ε l
have refine_1 : stepBound^[⌊4 / HPow.hPow (β := ℕ) ε 5⌋₊] t * HPow.hPow (α := ℕ) 4 (stepBound^[⌊4 / HPow.hPow (β := ℕ) ε 5⌋₊] t) ≤
  stepBound^[⌊4 / HPow.hPow (β := ℕ) ε 5⌋₊] (initialBound ε l) *
    HPow.hPow (α := ℕ) 16 (stepBound^[⌊4 / HPow.hPow (β := ℕ) ε 5⌋₊] (initialBound ε l))
Tactic: rw [iterate_succ_apply', stepBound, bound]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma (goal)
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 α
h :
  ∀ (i : ℕ),
    ∃ (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
hP₁ : P.IsEquipartition
hP₂ : t ≤ #P.parts
hP₃ : #P.parts ≤ stepBound^[⌊4 / HPow.hPow (β := ℕ) ε 5⌋₊ + 1] t
hP₄ : P.IsUniform G ε ∨ HPow.hPow (β := ℕ) ε 5 / 4 * (↑(⌊4 / HPow.hPow (β := ℕ) ε 5⌋₊ + 1) : ℝ) ≤ (↑(P.energy G) : ℝ)
⊢ stepBound^[⌊4 / HPow.hPow (β := ℕ) ε 5⌋₊] t * HPow.hPow (α := ℕ) 4 (stepBound^[⌊4 / HPow.hPow (β := ℕ) ε 5⌋₊] t) ≤
    stepBound^[⌊4 / HPow.hPow (β := ℕ) ε 5⌋₊] (initialBound ε l) *
      HPow.hPow (α := ℕ) 16 (stepBound^[⌊4 / HPow.hPow (β := ℕ) ε 5⌋₊] (initialBound ε l))
have refine_1 : LE.le (α := ℕ) 4 16
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma (goal)
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 α
h :
  ∀ (i : ℕ),
    ∃ (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
hP₁ : P.IsEquipartition
hP₂ : t ≤ #P.parts
hP₃ : #P.parts ≤ stepBound^[⌊4 / HPow.hPow (β := ℕ) ε 5⌋₊ + 1] t
hP₄ : P.IsUniform G ε ∨ HPow.hPow (β := ℕ) ε 5 / 4 * (↑(⌊4 / HPow.hPow (β := ℕ) ε 5⌋₊ + 1) : ℝ) ≤ (↑(P.energy G) : ℝ)
hPenergy : HPow.hPow (β := ℕ) ε 5 / 4 * (↑(⌊4 / HPow.hPow (β := ℕ) ε 5⌋₊ + 1) : ℝ) ≤ (↑(P.energy G) : ℝ)
⊢ 1 = HPow.hPow (β := ℕ) ε 5 / 4 * (4 / HPow.hPow (β := ℕ) ε 5)
have rw : 1 = 4 / 4
Tactic: rw [mul_comm, div_mul_div_cancel₀ (pow_pos hε 5).ne']
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma (goal)
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 α
h :
  ∀ (i : ℕ),
    ∃ (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
hP₁ : P.IsEquipartition
hP₂ : t ≤ #P.parts
hP₃ : #P.parts ≤ stepBound^[⌊4 / HPow.hPow (β := ℕ) ε 5⌋₊ + 1] t
hP₄ : P.IsUniform G ε ∨ HPow.hPow (β := ℕ) ε 5 / 4 * (↑(⌊4 / HPow.hPow (β := ℕ) ε 5⌋₊ + 1) : ℝ) ≤ (↑(P.energy G) : ℝ)
hPenergy : HPow.hPow (β := ℕ) ε 5 / 4 * (↑(⌊4 / HPow.hPow (β := ℕ) ε 5⌋₊ + 1) : ℝ) ≤ (↑(P.energy G) : ℝ)
⊢ HPow.hPow (β := ℕ) ε 5 / 4 * (4 / HPow.hPow (β := ℕ) ε 5) <
    HPow.hPow (β := ℕ) ε 5 / 4 * HAdd.hAdd (α := ℝ) (↑⌊4 / HPow.hPow (β := ℕ) ε 5⌋₊ : ℝ) 1
have hbc : 4 / HPow.hPow (β := ℕ) ε 5 < HAdd.hAdd (α := ℝ) (↑⌊4 / HPow.hPow (β := ℕ) ε 5⌋₊ : ℝ) 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma (goal)
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 α
h :
  ∀ (i : ℕ),
    ∃ (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
hP₁ : P.IsEquipartition
hP₂ : t ≤ #P.parts
hP₃ : #P.parts ≤ stepBound^[⌊4 / HPow.hPow (β := ℕ) ε 5⌋₊ + 1] t
hP₄ : P.IsUniform G ε ∨ HPow.hPow (β := ℕ) ε 5 / 4 * (↑(⌊4 / HPow.hPow (β := ℕ) ε 5⌋₊ + 1) : ℝ) ≤ (↑(P.energy G) : ℝ)
hPenergy : HPow.hPow (β := ℕ) ε 5 / 4 * (↑(⌊4 / HPow.hPow (β := ℕ) ε 5⌋₊ + 1) : ℝ) ≤ (↑(P.energy G) : ℝ)
⊢ LT.lt (α := ℝ) 1 1
have ε₁ : 1 = HPow.hPow (β := ℕ) ε 5 / 4 * (4 / HPow.hPow (β := ℕ) ε 5)
Tactic: calc
      (1 : ℝ) = ε ^ 5 / ↑4 * (↑4 / ε ^ 5) := by
        rw [mul_comm, div_mul_div_cancel₀ (pow_pos hε 5).ne']; simp
      _ < ε ^ 5 / 4 * (⌊4 / ε ^ 5⌋₊ + 1) := by gcongr; exact Nat.lt_floor_add_one _
      _ ≤ (P.energy G : ℝ) := by rwa [← Nat.cast_add_one]
      _ ≤ 1 := mod_cast P.energy_le_one G
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma (goal)
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 α
h :
  ∀ (i : ℕ),
    ∃ (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
hP₁ : P.IsEquipartition
hP₂ : t ≤ #P.parts
hP₃ : #P.parts ≤ stepBound^[⌊4 / HPow.hPow (β := ℕ) ε 5⌋₊ + 1] t
hP₄ : P.IsUniform G ε ∨ HPow.hPow (β := ℕ) ε 5 / 4 * (↑(⌊4 / HPow.hPow (β := ℕ) ε 5⌋₊ + 1) : ℝ) ≤ (↑(P.energy G) : ℝ)
hPenergy : HPow.hPow (β := ℕ) ε 5 / 4 * (↑(⌊4 / HPow.hPow (β := ℕ) ε 5⌋₊ + 1) : ℝ) ≤ (↑(P.energy G) : ℝ)
ε₁ : 1 = HPow.hPow (β := ℕ) ε 5 / 4 * (4 / HPow.hPow (β := ℕ) ε 5)
⊢ LT.lt (α := ℝ) 1 1
have ε₂ : HPow.hPow (β := ℕ) ε 5 / 4 * (4 / HPow.hPow (β := ℕ) ε 5) <
  HPow.hPow (β := ℕ) ε 5 / 4 * HAdd.hAdd (α := ℝ) (↑⌊4 / HPow.hPow (β := ℕ) ε 5⌋₊ : ℝ) 1
Tactic: calc
      (1 : ℝ) = ε ^ 5 / ↑4 * (↑4 / ε ^ 5) := by
        rw [mul_comm, div_mul_div_cancel₀ (pow_pos hε 5).ne']; simp
      _ < ε ^ 5 / 4 * (⌊4 / ε ^ 5⌋₊ + 1) := by gcongr; exact Nat.lt_floor_add_one _
      _ ≤ (P.energy G : ℝ) := by rwa [← Nat.cast_add_one]
      _ ≤ 1 := mod_cast P.energy_le_one G
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma (goal)
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 α
h :
  ∀ (i : ℕ),
    ∃ (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
hP₁ : P.IsEquipartition
hP₂ : t ≤ #P.parts
hP₃ : #P.parts ≤ stepBound^[⌊4 / HPow.hPow (β := ℕ) ε 5⌋₊ + 1] t
hP₄ : P.IsUniform G ε ∨ HPow.hPow (β := ℕ) ε 5 / 4 * (↑(⌊4 / HPow.hPow (β := ℕ) ε 5⌋₊ + 1) : ℝ) ≤ (↑(P.energy G) : ℝ)
hPenergy : HPow.hPow (β := ℕ) ε 5 / 4 * (↑(⌊4 / HPow.hPow (β := ℕ) ε 5⌋₊ + 1) : ℝ) ≤ (↑(P.energy G) : ℝ)
ε₁ : 1 = HPow.hPow (β := ℕ) ε 5 / 4 * (4 / HPow.hPow (β := ℕ) ε 5)
ε₂ :
  HPow.hPow (β := ℕ) ε 5 / 4 * (4 / HPow.hPow (β := ℕ) ε 5) <
    HPow.hPow (β := ℕ) ε 5 / 4 * HAdd.hAdd (α := ℝ) (↑⌊4 / HPow.hPow (β := ℕ) ε 5⌋₊ : ℝ) 1
⊢ LT.lt (α := ℝ) 1 1
have ε₃ : HPow.hPow (β := ℕ) ε 5 / 4 * HAdd.hAdd (α := ℝ) (↑⌊4 / HPow.hPow (β := ℕ) ε 5⌋₊ : ℝ) 1 ≤ (↑(P.energy G) : ℝ)
Tactic: calc
      (1 : ℝ) = ε ^ 5 / ↑4 * (↑4 / ε ^ 5) := by
        rw [mul_comm, div_mul_div_cancel₀ (pow_pos hε 5).ne']; simp
      _ < ε ^ 5 / 4 * (⌊4 / ε ^ 5⌋₊ + 1) := by gcongr; exact Nat.lt_floor_add_one _
      _ ≤ (P.energy G : ℝ) := by rwa [← Nat.cast_add_one]
      _ ≤ 1 := mod_cast P.energy_le_one G
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma (goal)
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 α
⊢ ∃ (P : Finpartition (α := Finset α) univ), P.IsEquipartition ∧ l ≤ #P.parts ∧ #P.parts ≤ bound ε l ∧ P.IsUniform G ε
have inr : ∀ (i : ℕ),
  ∃ (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: suffices h : ∀ i, ∃ P : Finpartition (univ : Finset α), P.IsEquipartition ∧ t ≤ #P.parts ∧
    #P.parts ≤ stepBound^[i] t ∧ (P.IsUniform G ε ∨ ε ^ 5 / 4 * i ≤ P.energy G) by
  -- For `i > 4 / ε ^ 5` we know that the partition we get can't have energy `≥ ε ^ 5 / 4 * i > 1`,
  -- so it must instead be `ε`-uniform and we won.
    obtain ⟨P, hP₁, hP₂, hP₃, hP₄⟩ := h (⌊4 / ε ^ 5⌋₊ + 1)
    refine ⟨P, hP₁, (le_initialBound _ _).trans hP₂, hP₃.trans ?_,
      hP₄.resolve_right fun hPenergy => lt_irrefl (1 : ℝ) ?_⟩
    · rw [iterate_succ_apply', stepBound, bound]
      gcongr
      simp
    calc
      (1 : ℝ) = ε ^ 5 / ↑4 * (↑4 / ε ^ 5) := by
        rw [mul_comm, div_mul_div_cancel₀ (pow_pos hε 5).ne']; simp
      _ < ε ^ 5 / 4 * (⌊4 / ε ^ 5⌋₊ + 1) := by gcongr; exact Nat.lt_floor_add_one _
      _ ≤ (P.energy G : ℝ) := by rwa [← Nat.cast_add_one]
      _ ≤ 1 := mod_cast P.energy_le_one G
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma (goal)
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 α
⊢ ∃ (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) : ℝ))
have inr : HPow.hPow (β := ℕ) ε 5 / 4 * (↑0 : ℝ) ≤ (↑(dum.energy G) : ℝ)
Tactic: refine ⟨dum, hdum₁, hdum₂.ge, hdum₂.le, Or.inr ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma (goal)
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 α
⊢ HPow.hPow (β := ℕ) ε 5 / 4 * (↑0 : ℝ) ≤ (↑(dum.energy G) : ℝ)
have inr : LE.le (α := ℝ) 0 (↑(dum.energy G) : ℝ)
Tactic: rw [Nat.cast_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma (goal)
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 : ℕ
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) : ℝ))
have inr : ∀ (P : Finpartition (α := Finset α) univ) (hP₁ : P.IsEquipartition) (hP₂ : t ≤ #P.parts)
  (hP₃ : #P.parts ≤ stepBound^[i] t)
  (hP₄ : 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) : ℝ))
Tactic: obtain ⟨P, hP₁, hP₂, hP₃, hP₄⟩ := ih
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma (goal)
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 : ℕ
P : Finpartition (α := Finset α) univ
hP₁ : P.IsEquipartition
hP₂ : t ≤ #P.parts
hP₃ : #P.parts ≤ stepBound^[i] t
hP₄ : 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) : ℝ))
have pos : ∀ (huniform : P.IsUniform 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) : ℝ))
Tactic: by_cases huniform : P.IsUniform G ε
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma (goal)
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 : ℕ
P : Finpartition (α := Finset α) univ
hP₁ : P.IsEquipartition
hP₂ : t ≤ #P.parts
hP₃ : #P.parts ≤ stepBound^[i] t
hP₄ : P.IsUniform G ε ∨ HPow.hPow (β := ℕ) ε 5 / 4 * (↑i : ℝ) ≤ (↑(P.energy G) : ℝ)
pos :
  ∀ (huniform : P.IsUniform 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 + 1] t ∧
          (P.IsUniform G ε ∨ HPow.hPow (β := ℕ) ε 5 / 4 * (↑(i + 1) : ℝ) ≤ (↑(P.energy G) : ℝ))
have neg : ∀ (huniform : ¬P.IsUniform 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) : ℝ))
Tactic: by_cases huniform : P.IsUniform G ε