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
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) : ℝ))
have pos : #P.parts ≤ stepBound^[i + 1] t
Tactic: refine ⟨P, hP₁, hP₂, ?_, Or.inl huniform⟩
-- 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) : ℝ)
huniform : P.IsUniform G ε
⊢ #P.parts ≤ stepBound^[i + 1] t
have pos : #P.parts ≤ stepBound (stepBound^[i] t)
Tactic: rw [iterate_succ_apply']
-- 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
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) : ℝ))
have hP₅ : HPow.hPow (β := ℕ) ε 5 / 4 * (↑i : ℝ) ≤ (↑(P.energy G) : ℝ)
Tactic: replace hP₄ := hP₄.resolve_left huniform
Cleared hypotheses: hP₄
-- 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
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) : ℝ)
⊢ ∃ (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 hεl' : 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)
-- 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
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
have hi : HPow.hPow (β := ℕ) ε 5 / 4 * (↑i : ℝ) ≤ 1
Tactic: have hi : ε ^ 5 / 4 * ↑i ≤ 1 := hP₄.trans (mod_cast P.energy_le_one G)
-- 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
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
⊢ (↑i : ℝ) ≤ 4 / HPow.hPow (β := ℕ) ε 5
have hi₁ : 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
Cleared hypotheses: hi
-- 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
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
⊢ (↑i : ℝ) ≤ 4 / HPow.hPow (β := ℕ) ε 5
have hi₁ : HPow.hPow (β := ℕ) ε 5 * (↑i : ℝ) ≤ 4
Tactic: norm_num at hi
Cleared hypotheses: hi
-- 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
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
⊢ ∃ (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 hi : (↑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ε _)]
-- 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
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 : 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 hsize : #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) _)
-- 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
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 : 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 hPα : #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α
-- 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
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
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
⊢ ∃ (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 : t ≤ #(increment hP₁ G ε).parts
Tactic: 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ε₁⟩
-- 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
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
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
neg : t ≤ #(increment hP₁ G ε).parts
⊢ ∃ (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₁ : #(increment hP₁ G ε).parts ≤ stepBound^[i + 1] t
Tactic: 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ε₁⟩
-- 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
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
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
neg : t ≤ #(increment hP₁ G ε).parts
neg₁ : #(increment hP₁ G ε).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) : ℝ))
have neg₂ : HPow.hPow (β := ℕ) ε 5 / 4 * (↑(i + 1) : ℝ) ≤ (↑(P.energy G) : ℝ) + HPow.hPow (β := ℕ) ε 5 / 4
Tactic: 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ε₁⟩
-- 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
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
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
⊢ t ≤ #(increment hP₁ G ε).parts
have neg : t ≤ stepBound #P.parts
Tactic: rw [card_increment hPα huniform]
-- 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
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
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
⊢ #(increment hP₁ G ε).parts ≤ stepBound^[i + 1] t
have neg : stepBound #P.parts ≤ stepBound (stepBound^[i] t)
Tactic: rw [card_increment hPα huniform, iterate_succ_apply']
-- 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
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
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
⊢ HPow.hPow (β := ℕ) ε 5 / 4 * (↑(i + 1) : ℝ) ≤ (↑(P.energy G) : ℝ) + HPow.hPow (β := ℕ) ε 5 / 4
have neg : HPow.hPow (β := ℕ) ε 5 / 4 * (↑i : ℝ) + HPow.hPow (β := ℕ) ε 5 / 4 ≤ (↑(P.energy G) : ℝ) + HPow.hPow (β := ℕ) ε 5 / 4
Tactic: rw [Nat.cast_succ, mul_add, mul_one]
-- 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),
    P.IsEquipartition ∧
      t ≤ #P.parts ∧
        #P.parts ≤ stepBound^[i] t ∧ (P.IsUniform G ε ∨ HPow.hPow (β := ℕ) ε 5 / 4 * (↑i : ℝ) ≤ (↑(P.energy G) : ℝ))
have 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) : ℝ))
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
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
G : SimpleGraph α
inst_3 : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
ε' : 𝕜
h : ε ≤ ε'
hε : G.IsUniform ε s t
s' : Finset α
hs' : s' ⊆ s
t' : Finset α
ht' : t' ⊆ t
hs : (↑(#s) : 𝕜) * ε' ≤ (↑(#s') : 𝕜)
ht : (↑(#t) : 𝕜) * ε' ≤ (↑(#t') : 𝕜)
⊢ |HSub.hSub (α := 𝕜) (↑(G.edgeDensity s' t') : 𝕜) (↑(G.edgeDensity s t) : 𝕜)| < ε'
have refine_1 : (↑(#s) : 𝕜) * ε ≤ (↑(#s) : 𝕜) * ε'
Tactic: refine (hε hs' ht' (le_trans ?_ hs) (le_trans ?_ ht)).trans_le h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
G : SimpleGraph α
inst_3 : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
ε' : 𝕜
h : ε ≤ ε'
hε : G.IsUniform ε s t
s' : Finset α
hs' : s' ⊆ s
t' : Finset α
ht' : t' ⊆ t
hs : (↑(#s) : 𝕜) * ε' ≤ (↑(#s') : 𝕜)
ht : (↑(#t) : 𝕜) * ε' ≤ (↑(#t') : 𝕜)
refine_1 : (↑(#s) : 𝕜) * ε ≤ (↑(#s) : 𝕜) * ε'
⊢ |HSub.hSub (α := 𝕜) (↑(G.edgeDensity s' t') : 𝕜) (↑(G.edgeDensity s t) : 𝕜)| < ε'
have refine_2 : (↑(#t) : 𝕜) * ε ≤ (↑(#t) : 𝕜) * ε'
Tactic: refine (hε hs' ht' (le_trans ?_ hs) (le_trans ?_ ht)).trans_le h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
G : SimpleGraph α
inst_3 : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
ε' : 𝕜
h : ε ≤ ε'
hε : G.IsUniform ε s t
s' : Finset α
hs' : s' ⊆ s
t' : Finset α
ht' : t' ⊆ t
hs : (↑(#s) : 𝕜) * ε' ≤ (↑(#s') : 𝕜)
ht : (↑(#t) : 𝕜) * ε' ≤ (↑(#t') : 𝕜)
⊢ (↑(#s) : 𝕜) * ε ≤ (↑(#s) : 𝕜) * ε'
have refine_1 : LE.le.{u_2} (α := 𝕜) 0 (↑(#s) : 𝕜)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
G : SimpleGraph α
inst_3 : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
ε' : 𝕜
h : ε ≤ ε'
hε : G.IsUniform ε s t
s' : Finset α
hs' : s' ⊆ s
t' : Finset α
ht' : t' ⊆ t
hs : (↑(#s) : 𝕜) * ε' ≤ (↑(#s') : 𝕜)
ht : (↑(#t) : 𝕜) * ε' ≤ (↑(#t') : 𝕜)
⊢ (↑(#t) : 𝕜) * ε ≤ (↑(#t) : 𝕜) * ε'
have refine_2 : LE.le.{u_2} (α := 𝕜) 0 (↑(#t) : 𝕜)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
h : G.IsUniform ε s t
t' : Finset α
ht' : t' ⊆ t
s' : Finset α
hs' : s' ⊆ s
ht : (↑(#t) : 𝕜) * ε ≤ (↑(#t') : 𝕜)
hs : (↑(#s) : 𝕜) * ε ≤ (↑(#s') : 𝕜)
⊢ |HSub.hSub (α := 𝕜) (↑(G.edgeDensity t' s') : 𝕜) (↑(G.edgeDensity t s) : 𝕜)| < ε
have rw : |HSub.hSub (α := 𝕜) (↑(G.edgeDensity s' t') : 𝕜) (↑(G.edgeDensity s t) : 𝕜)| < ε
Tactic: rw [edgeDensity_comm _ t', edgeDensity_comm _ t]