awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 α
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) : ℝ))
⊢ ∃ (P : Finpartition (α := Finset α) univ), P.IsEquipartition ∧ l ≤ #P.parts ∧ #P.parts ≤ bound ε l ∧ P.IsUniform 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
-- 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 α
⊢ ∃ (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) : ℝ))

Tactic:
⟨dum, hdum₁, hdum₂.ge, hdum₂.le, Or.inr ?_⟩

Premises used: Eq.ge, Eq.le, And.intro, Exists.intro, Or.inr
-- 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 α
inr : HPow.hPow (β := ℕ) ε 5 / 4 * (↑0 : ℝ) ≤ (↑(dum.energy G) : ℝ)
⊢ ∃ (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) : ℝ))

Tactic:
refine ⟨dum, hdum₁, hdum₂.ge, hdum₂.le, Or.inr ?_⟩
-- 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 α
inr : LE.le (α := ℝ) 0 (↑(dum.energy G) : ℝ)
⊢ HPow.hPow (β := ℕ) ε 5 / 4 * (↑0 : ℝ) ≤ (↑(dum.energy G) : ℝ)

Tactic:
rw [Nat.cast_zero, mul_zero]

Premises used: MulZeroClass.mul_zero, Nat.cast_zero
-- 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 α
⊢ LE.le (α := ℝ) 0 (↑(dum.energy G) : ℝ)

Tactic:
mod_cast dum.energy_nonneg G

Premises used: congrArg, cast, Finpartition.energy, Rat.cast, Rat.natCast_le_cast._simp_1, LE.le, congrFun', Finpartition.energy_nonneg, Nat.cast_zero, Eq.symm, Eq.trans
-- 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 α
⊢ LE.le (α := ℝ) 0 (↑(dum.energy G) : ℝ)

Tactic:
exact mod_cast dum.energy_nonneg G

Premises used: Finpartition.energy_nonneg
-- 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 : ℕ
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) : ℝ))
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) : ℝ))
⊢ ∃ (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
-- 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 : ℕ
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) : ℝ))
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) : ℝ))
⊢ ∃ (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 ε

Premises used: Finpartition.IsUniform
-- 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 : ℕ
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) : ℝ)
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:
⟨P, hP₁, hP₂, ?_, Or.inl huniform⟩

Premises used: And.intro, Exists.intro, Or.inl
-- 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 : ℕ
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) : ℝ)
huniform : P.IsUniform G ε
pos : #P.parts ≤ stepBound^[i + 1] t
⊢ ∃ (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:
refine ⟨P, hP₁, hP₂, ?_, Or.inl huniform⟩
-- 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 : ℕ
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) : ℝ)
huniform : P.IsUniform G ε
pos : #P.parts ≤ stepBound (stepBound^[i] t)
⊢ #P.parts ≤ stepBound^[i + 1] t

Tactic:
rw [iterate_succ_apply']

Premises used: Function.iterate_succ_apply'
-- 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 : ℕ
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) : ℝ)
huniform : P.IsUniform G ε
⊢ #P.parts ≤ stepBound (stepBound^[i] t)

Tactic:
hP₃.trans (le_stepBound _)

Premises used: SzemerediRegularity.le_stepBound, LE.le.trans
-- 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 : ℕ
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) : ℝ)
huniform : P.IsUniform G ε
⊢ #P.parts ≤ stepBound (stepBound^[i] t)

Tactic:
exact hP₃.trans (le_stepBound _)

Premises used: SzemerediRegularity.le_stepBound, LE.le.trans
-- 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 : ℕ
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) : ℝ)
huniform : ¬P.IsUniform G ε
⊢ HPow.hPow (β := ℕ) ε 5 / 4 * (↑i : ℝ) ≤ (↑(P.energy G) : ℝ)

Tactic:
replace hP₄ := hP₄.resolve_left huniform
-- 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 : ℕ
P : Finpartition (α := Finset α) univ
hP₁ : P.IsEquipartition
hP₂ : t ≤ #P.parts
hP₃ : #P.parts ≤ stepBound^[i] t
huniform : ¬P.IsUniform G ε
hP₄ : HPow.hPow (β := ℕ) ε 5 / 4 * (↑i : ℝ) ≤ (↑(P.energy G) : ℝ)
⊢ LE.le (α := ℝ) 1 4

Tactic:
simp
-- 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 : ℕ
P : Finpartition (α := Finset α) univ
hP₁ : P.IsEquipartition
hP₂ : t ≤ #P.parts
hP₃ : #P.parts ≤ stepBound^[i] t
huniform : ¬P.IsUniform G ε
hP₄ : HPow.hPow (β := ℕ) ε 5 / 4 * (↑i : ℝ) ≤ (↑(P.energy G) : ℝ)
⊢ 0 ≤ HPow.hPow (β := ℕ) ε 5

Tactic:
positivity
-- 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 : ℕ
P : Finpartition (α := Finset α) univ
hP₁ : P.IsEquipartition
hP₂ : t ≤ #P.parts
hP₃ : #P.parts ≤ stepBound^[i] t
huniform : ¬P.IsUniform G ε
hP₄ : HPow.hPow (β := ℕ) ε 5 / 4 * (↑i : ℝ) ≤ (↑(P.energy G) : ℝ)
⊢ 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5

Tactic:
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)
-- 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 : ℕ
P : Finpartition (α := Finset α) univ
hP₁ : P.IsEquipartition
hP₂ : t ≤ #P.parts
hP₃ : #P.parts ≤ stepBound^[i] t
huniform : ¬P.IsUniform G ε
hP₄ : HPow.hPow (β := ℕ) ε 5 / 4 * (↑i : ℝ) ≤ (↑(P.energy G) : ℝ)
hεl' : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
⊢ HPow.hPow (β := ℕ) ε 5 / 4 * (↑i : ℝ) ≤ 1

Tactic:
have hi : ε ^ 5 / 4 * ↑i ≤ 1 := hP₄.trans (mod_cast P.energy_le_one G)
-- 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 : ℕ
P : Finpartition (α := Finset α) univ
hP₁ : P.IsEquipartition
hP₂ : t ≤ #P.parts
hP₃ : #P.parts ≤ stepBound^[i] t
huniform : ¬P.IsUniform G ε
hP₄ : HPow.hPow (β := ℕ) ε 5 / 4 * (↑i : ℝ) ≤ (↑(P.energy G) : ℝ)
hεl' : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hi : HPow.hPow (β := ℕ) ε 5 * (↑i : ℝ) / 4 ≤ 1
⊢ LT.lt (α := ℝ) 0 4

Tactic:
simp
-- 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 : ℕ
P : Finpartition (α := Finset α) univ
hP₁ : P.IsEquipartition
hP₂ : t ≤ #P.parts
hP₃ : #P.parts ≤ stepBound^[i] t
huniform : ¬P.IsUniform G ε
hP₄ : HPow.hPow (β := ℕ) ε 5 / 4 * (↑i : ℝ) ≤ (↑(P.energy G) : ℝ)
hεl' : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hi : HPow.hPow (β := ℕ) ε 5 / 4 * (↑i : ℝ) ≤ 1
⊢ HPow.hPow (β := ℕ) ε 5 * (↑i : ℝ) ≤ HMul.hMul (α := ℝ) 1 4

Tactic:
rw [div_mul_eq_mul_div, div_le_iff₀ (show (0 : ℝ) < 4 by simp)] at hi

Premises used: div_le_iff₀, div_mul_eq_mul_div
-- 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 : ℕ
P : Finpartition (α := Finset α) univ
hP₁ : P.IsEquipartition
hP₂ : t ≤ #P.parts
hP₃ : #P.parts ≤ stepBound^[i] t
huniform : ¬P.IsUniform G ε
hP₄ : HPow.hPow (β := ℕ) ε 5 / 4 * (↑i : ℝ) ≤ (↑(P.energy G) : ℝ)
hεl' : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hi : HPow.hPow (β := ℕ) ε 5 * (↑i : ℝ) ≤ HMul.hMul (α := ℝ) 1 4
⊢ HPow.hPow (β := ℕ) ε 5 * (↑i : ℝ) ≤ 4

Tactic:
norm_num at hi
-- 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 : ℕ
P : Finpartition (α := Finset α) univ
hP₁ : P.IsEquipartition
hP₂ : t ≤ #P.parts
hP₃ : #P.parts ≤ stepBound^[i] t
huniform : ¬P.IsUniform G ε
hP₄ : HPow.hPow (β := ℕ) ε 5 / 4 * (↑i : ℝ) ≤ (↑(P.energy G) : ℝ)
hεl' : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hi : HPow.hPow (β := ℕ) ε 5 * (↑i : ℝ) ≤ 4
rwa rwa₁ rwa₂ rwa₃ : HPow.hPow (β := ℕ) ε 5 * (↑i : ℝ) ≤ 4
⊢ (↑i : ℝ) ≤ 4 / HPow.hPow (β := ℕ) ε 5

Tactic:
rwa [le_div_iff₀' (pow_pos hε _)]

Premises used: pow_pos, le_div_iff₀'
-- 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 : ℕ
P : Finpartition (α := Finset α) univ
hP₁ : P.IsEquipartition
hP₂ : t ≤ #P.parts
hP₃ : #P.parts ≤ stepBound^[i] t
huniform : ¬P.IsUniform G ε
hP₄ : HPow.hPow (β := ℕ) ε 5 / 4 * (↑i : ℝ) ≤ (↑(P.energy G) : ℝ)
hεl' : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
⊢ (↑i : ℝ) ≤ 4 / HPow.hPow (β := ℕ) ε 5

Tactic:
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ε _)]
-- 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 : ℕ
P : Finpartition (α := Finset α) univ
hP₁ : P.IsEquipartition
hP₂ : t ≤ #P.parts
hP₃ : #P.parts ≤ stepBound^[i] t
huniform : ¬P.IsUniform G ε
hP₄ : HPow.hPow (β := ℕ) ε 5 / 4 * (↑i : ℝ) ≤ (↑(P.energy G) : ℝ)
hεl' : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hi : (↑i : ℝ) ≤ 4 / HPow.hPow (β := ℕ) ε 5
⊢ #P.parts ≤ stepBound^[⌊4 / HPow.hPow (β := ℕ) ε 5⌋₊] t

Tactic:
have hsize : #P.parts ≤ stepBound^[⌊4 / ε ^ 5⌋₊] t :=
    hP₃.trans (monotone_iterate_of_id_le le_stepBound (Nat.le_floor hi) _)
-- 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 : ℕ
P : Finpartition (α := Finset α) univ
hP₁ : P.IsEquipartition
hP₂ : t ≤ #P.parts
hP₃ : #P.parts ≤ stepBound^[i] t
huniform : ¬P.IsUniform G ε
hP₄ : HPow.hPow (β := ℕ) ε 5 / 4 * (↑i : ℝ) ≤ (↑(P.energy G) : ℝ)
hεl' : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hi : (↑i : ℝ) ≤ 4 / HPow.hPow (β := ℕ) ε 5
hsize : #P.parts ≤ stepBound^[⌊4 / HPow.hPow (β := ℕ) ε 5⌋₊] t
⊢ GT.gt (α := ℕ) 16 0

Tactic:
simp
-- 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 : ℕ
P : Finpartition (α := Finset α) univ
hP₁ : P.IsEquipartition
hP₂ : t ≤ #P.parts
hP₃ : #P.parts ≤ stepBound^[i] t
huniform : ¬P.IsUniform G ε
hP₄ : HPow.hPow (β := ℕ) ε 5 / 4 * (↑i : ℝ) ≤ (↑(P.energy G) : ℝ)
hεl' : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hi : (↑i : ℝ) ≤ 4 / HPow.hPow (β := ℕ) ε 5
hsize : #P.parts ≤ stepBound^[⌊4 / HPow.hPow (β := ℕ) ε 5⌋₊] t
⊢ #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α

Tactic:
have hPα : #P.parts * 16 ^ #P.parts ≤ card α :=
    (Nat.mul_le_mul hsize (Nat.pow_le_pow_right (by simp) hsize)).trans hα