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
inr :
  ∀ (dum : Finpartition (α := Finset α) univ) (hdum₁ : dum.IsEquipartition) (hdum₂ : #dum.parts = initialBound ε l),
    ∃ (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 ε

Tactic:
obtain ⟨dum, hdum₁, hdum₂⟩ :=
    exists_equipartition_card_eq (univ : Finset α) (initialBound_pos _ _).ne' htα

Premises used: Finset.univ, Finpartition.exists_equipartition_card_eq, LT.lt.ne', SzemerediRegularity.initialBound_pos
-- 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
inr :
  ∀ (hε₁ : 1 ≤ ε),
    ∃ (P : Finpartition (α := Finset α) univ), P.IsEquipartition ∧ l ≤ #P.parts ∧ #P.parts ≤ bound ε l ∧ P.IsUniform G ε
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 ε

Tactic:
obtain hε₁ | hε₁ := le_total 1 ε

Premises used: le_total, OfNat.ofNat
-- 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 ≤ ε
⊢ ∃ (P : Finpartition (α := Finset α) univ), P.IsEquipartition ∧ l ≤ #P.parts ∧ #P.parts ≤ bound ε l ∧ P.IsUniform G ε

Tactic:
⟨dum, hdum₁, (le_initialBound ε l).trans hdum₂.ge,
      hdum₂.le.trans (initialBound_le_bound ε l), (dum.isUniform_one G).mono hε₁⟩

Premises used: SzemerediRegularity.initialBound_le_bound, Eq.ge, Finpartition.isUniform_one, Eq.le, And.intro, Exists.intro, LE.le.trans, Finpartition.IsUniform.mono, SzemerediRegularity.le_initialBound
-- 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 ≤ ε
⊢ ∃ (P : Finpartition (α := Finset α) univ), P.IsEquipartition ∧ l ≤ #P.parts ∧ #P.parts ≤ bound ε l ∧ P.IsUniform G ε

Tactic:
exact ⟨dum, hdum₁, (le_initialBound ε l).trans hdum₂.ge,
      hdum₂.le.trans (initialBound_le_bound ε l), (dum.isUniform_one G).mono 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
rw : 0 < Fintype.card α
⊢ Nonempty α

Tactic:
rw [← Fintype.card_pos_iff]

Premises used: Fintype.card_pos_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
⊢ 0 < Fintype.card α

Tactic:
(bound_pos _ _).trans_le hα

Premises used: SzemerediRegularity.bound_pos, LT.lt.trans_le
-- 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
⊢ 0 < Fintype.card α

Tactic:
exact (bound_pos _ _).trans_le hα

Premises used: SzemerediRegularity.bound_pos, LT.lt.trans_le
-- 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
⊢ Nonempty α

Tactic:
have : Nonempty α := by
    rw [← Fintype.card_pos_iff]
    exact (bound_pos _ _).trans_le 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 α
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) : ℝ))
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 ε
⊢ ∃ (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)

Premises used: HDiv.hDiv, HPow.hPow, HAdd.hAdd, Nat.floor, OfNat.ofNat
-- 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 α
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 ε

Tactic:
⟨P, hP₁, (le_initialBound _ _).trans hP₂, hP₃.trans ?_,
      hP₄.resolve_right fun hPenergy => lt_irrefl (1 : ℝ) ?_⟩

Premises used: lt_irrefl, And.intro, Exists.intro, Or.resolve_right, LE.le.trans, OfNat.ofNat, SzemerediRegularity.le_initialBound
-- 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 α
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
refine_2 :
  ∀ (hPenergy : HPow.hPow (β := ℕ) ε 5 / 4 * (↑(⌊4 / HPow.hPow (β := ℕ) ε 5⌋₊ + 1) : ℝ) ≤ (↑(P.energy G) : ℝ)),
    LT.lt (α := ℝ) 1 1
⊢ ∃ (P : Finpartition (α := Finset α) univ), P.IsEquipartition ∧ l ≤ #P.parts ∧ #P.parts ≤ bound ε l ∧ P.IsUniform G ε

Tactic:
refine ⟨P, hP₁, (le_initialBound _ _).trans hP₂, hP₃.trans ?_,
      hP₄.resolve_right fun hPenergy => lt_irrefl (1 : ℝ) ?_⟩
-- 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 α
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⌋₊] 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))
⊢ stepBound^[⌊4 / HPow.hPow (β := ℕ) ε 5⌋₊ + 1] t ≤ bound ε l

Tactic:
rw [iterate_succ_apply', stepBound, bound]

Premises used: Function.iterate_succ_apply', SzemerediRegularity.bound, SzemerediRegularity.stepBound
-- 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 α
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 : LE.le (α := ℕ) 4 16
⊢ 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:
gcongr
-- 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 α
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) : ℝ)
⊢ LE.le (α := ℕ) 4 16

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 α
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) : ℝ)
rw : 1 = 4 / 4
⊢ 1 = HPow.hPow (β := ℕ) ε 5 / 4 * (4 / HPow.hPow (β := ℕ) ε 5)

Tactic:
rw [mul_comm, div_mul_div_cancel₀ (pow_pos hε 5).ne']

Premises used: pow_pos, LT.lt.ne', mul_comm, OfNat.ofNat, div_mul_div_cancel₀
-- 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 α
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 = 4 / 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 α
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) : ℝ)
hbc : 4 / HPow.hPow (β := ℕ) ε 5 < HAdd.hAdd (α := ℝ) (↑⌊4 / HPow.hPow (β := ℕ) ε 5⌋₊ : ℝ) 1
⊢ HPow.hPow (β := ℕ) ε 5 / 4 * (4 / HPow.hPow (β := ℕ) ε 5) <
    HPow.hPow (β := ℕ) ε 5 / 4 * HAdd.hAdd (α := ℝ) (↑⌊4 / HPow.hPow (β := ℕ) ε 5⌋₊ : ℝ) 1

Tactic:
gcongr
-- 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 α
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) : ℝ)
⊢ 4 / HPow.hPow (β := ℕ) ε 5 < HAdd.hAdd (α := ℝ) (↑⌊4 / HPow.hPow (β := ℕ) ε 5⌋₊ : ℝ) 1

Tactic:
Nat.lt_floor_add_one _

Premises used: Nat.lt_floor_add_one
-- 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 α
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) : ℝ)
⊢ 4 / HPow.hPow (β := ℕ) ε 5 < HAdd.hAdd (α := ℝ) (↑⌊4 / HPow.hPow (β := ℕ) ε 5⌋₊ : ℝ) 1

Tactic:
exact Nat.lt_floor_add_one _

Premises used: Nat.lt_floor_add_one
-- 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 α
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) : ℝ)
rwa rwa₁ rwa₂ rwa₃ : HPow.hPow (β := ℕ) ε 5 / 4 * (↑(⌊4 / HPow.hPow (β := ℕ) ε 5⌋₊ + 1) : ℝ) ≤ (↑(P.energy G) : ℝ)
⊢ HPow.hPow (β := ℕ) ε 5 / 4 * HAdd.hAdd (α := ℝ) (↑⌊4 / HPow.hPow (β := ℕ) ε 5⌋₊ : ℝ) 1 ≤ (↑(P.energy G) : ℝ)

Tactic:
rwa [← Nat.cast_add_one]

Premises used: Nat.cast_add_one
-- 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 α
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) : ℝ)
⊢ LE.le (α := ℝ) (↑(P.energy G) : ℝ) 1

Tactic:
mod_cast P.energy_le_one G

Premises used: congrArg, Finpartition.energy_le_one, cast, Finpartition.energy, Rat.cast, LE.le, Rat.cast_le_natCast._simp_1, Eq.symm, Nat.cast_one, 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 α
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
ε₃ : HPow.hPow (β := ℕ) ε 5 / 4 * HAdd.hAdd (α := ℝ) (↑⌊4 / HPow.hPow (β := ℕ) ε 5⌋₊ : ℝ) 1 ≤ (↑(P.energy G) : ℝ)
⊢ LT.lt (α := ℝ) 1 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

Premises used: Finpartition.energy_le_one, HDiv.hDiv, Finpartition.energy, Rat.cast, HPow.hPow, HAdd.hAdd, Nat.floor, OfNat.ofNat