awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
𝒜 : Finset (Finset α)
s : Finset α
h𝒜 : 𝒜 ⊆ (chunk hP G ε hU).parts
hs : s ∈ 𝒜
⊢ HMul.hMul (α := ℝ) (↑(#𝒜) : ℝ) (↑m : ℝ) ≤ (↑(#(𝒜.sup id)) : ℝ)
have h₁ : #𝒜 * m ≤ ∑ i ∈ 𝒜, #i
Tactic: rw [← (ofSubset _ h𝒜 rfl).sum_card_parts, ofSubset_parts, ← cast_mul, cast_le]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
𝒜 : Finset (Finset α)
s : Finset α
m_pos : LT.lt (α := ℝ) 0 (↑m : ℝ)
h𝒜 : 𝒜 ⊆ (chunk hP G ε hU).parts
hs : s ∈ 𝒜
⊢ (↑(#(𝒜.sup id)) : ℝ) ≤ HMul.hMul (α := ℝ) (↑(#𝒜) : ℝ) (↑(#s) : ℝ) * (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 / (↑m : ℝ))
have rw : HMul.hMul (α := ℝ) (↑(#(𝒜.biUnion id)) : ℝ) (↑m : ℝ) ≤ (↑(#𝒜) : ℝ) * HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 * (↑(#s) : ℝ)
Tactic: rw [sup_eq_biUnion, mul_div_assoc', le_div_iff₀ m_pos, mul_right_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
𝒜 : Finset (Finset α)
s : Finset α
m_pos : LT.lt (α := ℝ) 0 (↑m : ℝ)
h𝒜 : 𝒜 ⊆ (chunk hP G ε hU).parts
hs : s ∈ 𝒜
⊢ HMul.hMul (α := ℝ) (↑(#(𝒜.biUnion id)) : ℝ) (↑m : ℝ) ≤ (↑(#𝒜) : ℝ) * HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 * (↑(#s) : ℝ)
have h₁ : (↑(#(𝒜.biUnion id)) : ℝ) ≤ (↑(#𝒜) : ℝ) * HAdd.hAdd (α := ℝ) (↑m : ℝ) 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
𝒜 : Finset (Finset α)
s : Finset α
m_pos : LT.lt (α := ℝ) 0 (↑m : ℝ)
h𝒜 : 𝒜 ⊆ (chunk hP G ε hU).parts
hs : s ∈ 𝒜
h₁ : (↑(#(𝒜.biUnion id)) : ℝ) ≤ (↑(#𝒜) : ℝ) * HAdd.hAdd (α := ℝ) (↑m : ℝ) 1
⊢ HMul.hMul (α := ℝ) (↑(#(𝒜.biUnion id)) : ℝ) (↑m : ℝ) ≤ (↑(#𝒜) : ℝ) * HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 * (↑(#s) : ℝ)
have h₂ : m ≤ #s
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
𝒜 : Finset (Finset α)
s : Finset α
m_pos : LT.lt (α := ℝ) 0 (↑m : ℝ)
h𝒜 : 𝒜 ⊆ (chunk hP G ε hU).parts
hs : s ∈ 𝒜
⊢ (↑(#(𝒜.biUnion id)) : ℝ) ≤ (↑(#𝒜) : ℝ) * HAdd.hAdd (α := ℝ) (↑m : ℝ) 1
have h₁ : #(𝒜.biUnion id) ≤ #𝒜 * (m + 1)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
𝒜 : Finset (Finset α)
s : Finset α
m_pos : LT.lt (α := ℝ) 0 (↑m : ℝ)
h𝒜 : 𝒜 ⊆ (chunk hP G ε hU).parts
hs : s ∈ 𝒜
⊢ #(𝒜.biUnion id) ≤ #𝒜 * (m + 1)
have h₁ : ∀ (x : Finset α) (hx : x ∈ 𝒜), #(id x) ≤ m + 1
Tactic: refine card_biUnion_le_card_mul _ _ _ fun x hx => ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
ε : ℝ
inst_2 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
⊢ (↑m : ℝ) / HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 = 1 - 1 / HAdd.hAdd (α := ℝ) (↑m : ℝ) 1
have rw : (↑m : ℝ) / HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 = (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 - 1) / HAdd.hAdd (α := ℝ) (↑m : ℝ) 1
Tactic: rw [one_sub_div coe_m_add_one_pos.ne', add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
ε : ℝ
inst_2 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
rw : (↑m : ℝ) / HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 = (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 - 1) / HAdd.hAdd (α := ℝ) (↑m : ℝ) 1
⊢ (↑m : ℝ) / HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 = 1 - 1 / HAdd.hAdd (α := ℝ) (↑m : ℝ) 1
have rw₁ : (↑m : ℝ) / HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 = (↑m : ℝ) / HAdd.hAdd (α := ℝ) (↑m : ℝ) 1
Tactic: rw [one_sub_div coe_m_add_one_pos.ne', add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
ε : ℝ
inst_2 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
⊢ 1 - HPow.hPow (β := ℕ) ε 5 / 50 ≤ HPow.hPow (β := ℕ) ((↑m : ℝ) / HAdd.hAdd (α := ℝ) (↑m : ℝ) 1) 2
have this : (↑m : ℝ) / HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 = 1 - 1 / HAdd.hAdd (α := ℝ) (↑m : ℝ) 1
Tactic: have : (m : ℝ) / (m + 1) = 1 - 1 / (m + 1) := by
    rw [one_sub_div coe_m_add_one_pos.ne', add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
ε : ℝ
inst_2 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
this : (↑m : ℝ) / HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 = 1 - 1 / HAdd.hAdd (α := ℝ) (↑m : ℝ) 1
⊢ 1 - HPow.hPow (β := ℕ) ε 5 / 50 ≤ HPow.hPow (β := ℕ) ((↑m : ℝ) / HAdd.hAdd (α := ℝ) (↑m : ℝ) 1) 2
have rw : 1 - HPow.hPow (β := ℕ) ε 5 / 50 ≤
  1 - 2 * (1 / HAdd.hAdd (α := ℝ) (↑m : ℝ) 1) + HPow.hPow (β := ℕ) (1 / HAdd.hAdd (α := ℝ) (↑m : ℝ) 1) 2
Tactic: rw [this, sub_sq, one_pow, mul_one]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
ε : ℝ
inst_2 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
this : (↑m : ℝ) / HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 = 1 - 1 / HAdd.hAdd (α := ℝ) (↑m : ℝ) 1
⊢ 1 - HPow.hPow (β := ℕ) ε 5 / 50 ≤
    1 - 2 * (1 / HAdd.hAdd (α := ℝ) (↑m : ℝ) 1) + HPow.hPow (β := ℕ) (1 / HAdd.hAdd (α := ℝ) (↑m : ℝ) 1) 2
have refine : 1 - HPow.hPow (β := ℕ) ε 5 / 50 ≤ 1 - 2 * (1 / HAdd.hAdd (α := ℝ) (↑m : ℝ) 1)
Tactic: refine le_trans ?_ (le_add_of_nonneg_right <| sq_nonneg _)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
ε : ℝ
inst_2 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
this : (↑m : ℝ) / HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 = 1 - 1 / HAdd.hAdd (α := ℝ) (↑m : ℝ) 1
⊢ 1 - HPow.hPow (β := ℕ) ε 5 / 50 ≤ 1 - 2 * (1 / HAdd.hAdd (α := ℝ) (↑m : ℝ) 1)
have rw : HMul.hMul (α := ℝ) 50 2 / HPow.hPow (β := ℕ) ε 5 ≤ HAdd.hAdd (α := ℝ) (↑m : ℝ) 1
Tactic: rw [sub_le_sub_iff_left, ← le_div_iff₀' (show (0 : ℝ) < 2 by simp), div_div,
    one_div_le coe_m_add_one_pos, one_div_div]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
ε : ℝ
inst_2 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
this : (↑m : ℝ) / HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 = 1 - 1 / HAdd.hAdd (α := ℝ) (↑m : ℝ) 1
rw : HMul.hMul (α := ℝ) 50 2 / HPow.hPow (β := ℕ) ε 5 ≤ HAdd.hAdd (α := ℝ) (↑m : ℝ) 1
⊢ 1 - HPow.hPow (β := ℕ) ε 5 / 50 ≤ 1 - 2 * (1 / HAdd.hAdd (α := ℝ) (↑m : ℝ) 1)
have rw₁ : 0 < HPow.hPow (β := ℕ) ε 5 / HMul.hMul (α := ℝ) 50 2
Tactic: rw [sub_le_sub_iff_left, ← le_div_iff₀' (show (0 : ℝ) < 2 by simp), div_div,
    one_div_le coe_m_add_one_pos, one_div_div]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
ε : ℝ
inst_2 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
this : (↑m : ℝ) / HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 = 1 - 1 / HAdd.hAdd (α := ℝ) (↑m : ℝ) 1
⊢ HMul.hMul (α := ℝ) 50 2 / HPow.hPow (β := ℕ) ε 5 ≤ HAdd.hAdd (α := ℝ) (↑m : ℝ) 1
have refine : HMul.hMul (α := ℝ) 50 2 / HPow.hPow (β := ℕ) ε 5 ≤ (↑m : ℝ)
Tactic: refine le_trans ?_ (le_add_of_nonneg_right zero_le_one)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
ε : ℝ
inst_2 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
this : (↑m : ℝ) / HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 = 1 - 1 / HAdd.hAdd (α := ℝ) (↑m : ℝ) 1
⊢ HMul.hMul (α := ℝ) 50 2 / HPow.hPow (β := ℕ) ε 5 ≤ (↑m : ℝ)
have norm_num : 100 / HPow.hPow (β := ℕ) ε 5 ≤ (↑m : ℝ)
Tactic: norm_num
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
ε : ℝ
inst_2 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
this : (↑m : ℝ) / HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 = 1 - 1 / HAdd.hAdd (α := ℝ) (↑m : ℝ) 1
⊢ 0 < HPow.hPow (β := ℕ) ε 5 / HMul.hMul (α := ℝ) 50 2
have sz_positivity : 0 < m → 0 < HPow.hPow (β := ℕ) ε 5 / HMul.hMul (α := ℝ) 50 2
Tactic: sz_positivity
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
ε : ℝ
inst_2 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
this : (↑m : ℝ) / HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 = 1 - 1 / HAdd.hAdd (α := ℝ) (↑m : ℝ) 1
sz_positivity sz_positivity₁ sz_positivity₂ sz_positivity₃ :
  0 < m → 0 < HPow.hPow (β := ℕ) ε 5 / HMul.hMul (α := ℝ) 50 2
⊢ 0 < HPow.hPow (β := ℕ) ε 5 / HMul.hMul (α := ℝ) 50 2
have sz_positivity₄ : 0 < m → 0 < ε → 0 < HPow.hPow (β := ℕ) ε 5 / HMul.hMul (α := ℝ) 50 2
Tactic: sz_positivity
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
ε : ℝ
inst_2 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
⊢ 0 ≤ ε
have sz_positivity : 0 < m → 0 ≤ ε
Tactic: sz_positivity
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
ε : ℝ
inst_2 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
sz_positivity sz_positivity₁ sz_positivity₂ sz_positivity₃ : 0 < m → 0 ≤ ε
⊢ 0 ≤ ε
have sz_positivity₄ : 0 < m → 0 < ε → 0 ≤ ε
Tactic: sz_positivity
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
ε : ℝ
inst_2 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
⊢ HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 / (↑m : ℝ)) 2 ≤ 1 + HPow.hPow (β := ℕ) ε 5 / 49
have this : 0 ≤ ε
Tactic: have : 0 ≤ ε := by sz_positivity
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
ε : ℝ
inst_2 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
this : 0 ≤ ε
⊢ Ne (α := ℝ) (↑m : ℝ) 0
have sz_positivity : 0 < m → Ne (α := ℝ) (↑m : ℝ) 0
Tactic: sz_positivity
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
ε : ℝ
inst_2 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
this : 0 ≤ ε
sz_positivity sz_positivity₁ sz_positivity₂ sz_positivity₃ : 0 < m → Ne (α := ℝ) (↑m : ℝ) 0
⊢ Ne (α := ℝ) (↑m : ℝ) 0
have sz_positivity₄ : 0 < m → 0 < ε → Ne (α := ℝ) (↑m : ℝ) 0
Tactic: sz_positivity
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
ε : ℝ
inst_2 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
this : 0 ≤ ε
⊢ HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 / (↑m : ℝ)) 2 ≤ 1 + HPow.hPow (β := ℕ) ε 5 / 49
have rw : HPow.hPow (β := ℕ) (1 + HDiv.hDiv (α := ℝ) 1 (↑m : ℝ)) 2 ≤ 1 + HPow.hPow (β := ℕ) ε 5 / 49
Tactic: rw [same_add_div (by sz_positivity)]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
ε : ℝ
inst_2 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
this : 0 ≤ ε
⊢ HPow.hPow (β := ℕ) (1 + HDiv.hDiv (α := ℝ) 1 (↑m : ℝ)) 2 ≤ HPow.hPow (β := ℕ) (1 + HPow.hPow (β := ℕ) ε 5 / 100) 2
have hab : HDiv.hDiv (α := ℝ) 1 (↑m : ℝ) ≤ HPow.hPow (β := ℕ) ε 5 / 100
Tactic: gcongr (1 + ?_) ^ 2
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
ε : ℝ
inst_2 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
this : 0 ≤ ε
⊢ HDiv.hDiv (α := ℝ) 1 (↑m : ℝ) ≤ HPow.hPow (β := ℕ) ε 5 / 100
have hab : HDiv.hDiv (α := ℝ) 1 (↑m : ℝ) ≤ 1 / (100 / HPow.hPow (β := ℕ) ε 5)
Tactic: rw [← one_div_div (100 : ℝ)]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
ε : ℝ
inst_2 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
this : 0 ≤ ε
⊢ 0 < 100 / HPow.hPow (β := ℕ) ε 5
have sz_positivity : 0 < m → 0 < 100 / HPow.hPow (β := ℕ) ε 5
Tactic: sz_positivity
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
ε : ℝ
inst_2 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
this : 0 ≤ ε
sz_positivity sz_positivity₁ sz_positivity₂ sz_positivity₃ : 0 < m → 0 < 100 / HPow.hPow (β := ℕ) ε 5
⊢ 0 < 100 / HPow.hPow (β := ℕ) ε 5
have sz_positivity₄ : 0 < m → 0 < ε → 0 < 100 / HPow.hPow (β := ℕ) ε 5
Tactic: sz_positivity
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
ε : ℝ
inst_2 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
this : 0 ≤ ε
⊢ 1 + HPow.hPow (β := ℕ) ε 5 * (50⁻¹ + HPow.hPow (β := ℕ) ε 5 / 10000) ≤
    1 + HPow.hPow (β := ℕ) ε 5 * (50⁻¹ + HPow.hPow (α := ℝ) (β := ℕ) 1 5 / 10000)
have bc : 0 ≤ HPow.hPow (β := ℕ) ε 5
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
ε : ℝ
inst_2 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
this : 0 ≤ ε
bc : 0 ≤ HPow.hPow (β := ℕ) ε 5
⊢ 1 + HPow.hPow (β := ℕ) ε 5 * (50⁻¹ + HPow.hPow (β := ℕ) ε 5 / 10000) ≤
    1 + HPow.hPow (β := ℕ) ε 5 * (50⁻¹ + HPow.hPow (α := ℝ) (β := ℕ) 1 5 / 10000)
have bc₁ : LE.le (α := ℝ) 0 10000
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
ε : ℝ
inst_2 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
this : 0 ≤ ε
⊢ 1 + HPow.hPow (β := ℕ) ε 5 * (50⁻¹ + HPow.hPow (α := ℝ) (β := ℕ) 1 5 / 10000) ≤ 1 + HPow.hPow (β := ℕ) ε 5 * 49⁻¹
have bc : 50⁻¹ + HPow.hPow (α := ℝ) (β := ℕ) 1 5 / 10000 ≤ 49⁻¹
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
ε : ℝ
inst_2 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
this : 0 ≤ ε
⊢ 1 + HPow.hPow (β := ℕ) ε 5 * 49⁻¹ = 1 + HPow.hPow (β := ℕ) ε 5 / 49
have rw : 1 + HPow.hPow (β := ℕ) ε 5 * 49⁻¹ = 1 + HPow.hPow (β := ℕ) ε 5 * 49⁻¹
Tactic: rw [div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
ε : ℝ
inst_2 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
this : 0 ≤ ε
⊢ HPow.hPow (β := ℕ) (1 + HDiv.hDiv (α := ℝ) 1 (↑m : ℝ)) 2 ≤ 1 + HPow.hPow (β := ℕ) ε 5 / 49
have _ : HPow.hPow (β := ℕ) (1 + HDiv.hDiv (α := ℝ) 1 (↑m : ℝ)) 2 ≤ HPow.hPow (β := ℕ) (1 + HPow.hPow (β := ℕ) ε 5 / 100) 2
Tactic: calc
    _ ≤ (1 + ε ^ 5 / 100) ^ 2 := by
      gcongr (1 + ?_) ^ 2
      rw [← one_div_div (100 : ℝ)]
      exact one_div_le_one_div_of_le (by sz_positivity) (hundred_div_ε_pow_five_le_m hPα hPε)
    _ = 1 + ε ^ 5 * (50⁻¹ + ε ^ 5 / 10000) := by ring
    _ ≤ 1 + ε ^ 5 * (50⁻¹ + 1 ^ 5 / 10000) := by gcongr
    _ ≤ 1 + ε ^ 5 * 49⁻¹ := by gcongr; norm_num
    _ = 1 + ε ^ 5 / 49 := by rw [div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
ε : ℝ
inst_2 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
this : 0 ≤ ε
_ : HPow.hPow (β := ℕ) (1 + HDiv.hDiv (α := ℝ) 1 (↑m : ℝ)) 2 ≤ HPow.hPow (β := ℕ) (1 + HPow.hPow (β := ℕ) ε 5 / 100) 2
⊢ HPow.hPow (β := ℕ) (1 + HDiv.hDiv (α := ℝ) 1 (↑m : ℝ)) 2 ≤ 1 + HPow.hPow (β := ℕ) ε 5 / 49
have _₁ : HPow.hPow (β := ℕ) (1 + HPow.hPow (β := ℕ) ε 5 / 100) 2 =
  1 + HPow.hPow (β := ℕ) ε 5 * (50⁻¹ + HPow.hPow (β := ℕ) ε 5 / 10000)
Tactic: calc
    _ ≤ (1 + ε ^ 5 / 100) ^ 2 := by
      gcongr (1 + ?_) ^ 2
      rw [← one_div_div (100 : ℝ)]
      exact one_div_le_one_div_of_le (by sz_positivity) (hundred_div_ε_pow_five_le_m hPα hPε)
    _ = 1 + ε ^ 5 * (50⁻¹ + ε ^ 5 / 10000) := by ring
    _ ≤ 1 + ε ^ 5 * (50⁻¹ + 1 ^ 5 / 10000) := by gcongr
    _ ≤ 1 + ε ^ 5 * 49⁻¹ := by gcongr; norm_num
    _ = 1 + ε ^ 5 / 49 := by rw [div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
ε : ℝ
inst_2 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
this : 0 ≤ ε
_ : HPow.hPow (β := ℕ) (1 + HDiv.hDiv (α := ℝ) 1 (↑m : ℝ)) 2 ≤ HPow.hPow (β := ℕ) (1 + HPow.hPow (β := ℕ) ε 5 / 100) 2
_₁ :
  HPow.hPow (β := ℕ) (1 + HPow.hPow (β := ℕ) ε 5 / 100) 2 =
    1 + HPow.hPow (β := ℕ) ε 5 * (50⁻¹ + HPow.hPow (β := ℕ) ε 5 / 10000)
⊢ HPow.hPow (β := ℕ) (1 + HDiv.hDiv (α := ℝ) 1 (↑m : ℝ)) 2 ≤ 1 + HPow.hPow (β := ℕ) ε 5 / 49
have _₂ : 1 + HPow.hPow (β := ℕ) ε 5 * (50⁻¹ + HPow.hPow (β := ℕ) ε 5 / 10000) ≤
  1 + HPow.hPow (β := ℕ) ε 5 * (50⁻¹ + HPow.hPow (α := ℝ) (β := ℕ) 1 5 / 10000)
Tactic: calc
    _ ≤ (1 + ε ^ 5 / 100) ^ 2 := by
      gcongr (1 + ?_) ^ 2
      rw [← one_div_div (100 : ℝ)]
      exact one_div_le_one_div_of_le (by sz_positivity) (hundred_div_ε_pow_five_le_m hPα hPε)
    _ = 1 + ε ^ 5 * (50⁻¹ + ε ^ 5 / 10000) := by ring
    _ ≤ 1 + ε ^ 5 * (50⁻¹ + 1 ^ 5 / 10000) := by gcongr
    _ ≤ 1 + ε ^ 5 * 49⁻¹ := by gcongr; norm_num
    _ = 1 + ε ^ 5 / 49 := by rw [div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
ε : ℝ
inst_2 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
this : 0 ≤ ε
_ : HPow.hPow (β := ℕ) (1 + HDiv.hDiv (α := ℝ) 1 (↑m : ℝ)) 2 ≤ HPow.hPow (β := ℕ) (1 + HPow.hPow (β := ℕ) ε 5 / 100) 2
_₁ :
  HPow.hPow (β := ℕ) (1 + HPow.hPow (β := ℕ) ε 5 / 100) 2 =
    1 + HPow.hPow (β := ℕ) ε 5 * (50⁻¹ + HPow.hPow (β := ℕ) ε 5 / 10000)
_₂ :
  1 + HPow.hPow (β := ℕ) ε 5 * (50⁻¹ + HPow.hPow (β := ℕ) ε 5 / 10000) ≤
    1 + HPow.hPow (β := ℕ) ε 5 * (50⁻¹ + HPow.hPow (α := ℝ) (β := ℕ) 1 5 / 10000)
⊢ HPow.hPow (β := ℕ) (1 + HDiv.hDiv (α := ℝ) 1 (↑m : ℝ)) 2 ≤ 1 + HPow.hPow (β := ℕ) ε 5 / 49
have _₃ : 1 + HPow.hPow (β := ℕ) ε 5 * (50⁻¹ + HPow.hPow (α := ℝ) (β := ℕ) 1 5 / 10000) ≤ 1 + HPow.hPow (β := ℕ) ε 5 * 49⁻¹
Tactic: calc
    _ ≤ (1 + ε ^ 5 / 100) ^ 2 := by
      gcongr (1 + ?_) ^ 2
      rw [← one_div_div (100 : ℝ)]
      exact one_div_le_one_div_of_le (by sz_positivity) (hundred_div_ε_pow_five_le_m hPα hPε)
    _ = 1 + ε ^ 5 * (50⁻¹ + ε ^ 5 / 10000) := by ring
    _ ≤ 1 + ε ^ 5 * (50⁻¹ + 1 ^ 5 / 10000) := by gcongr
    _ ≤ 1 + ε ^ 5 * 49⁻¹ := by gcongr; norm_num
    _ = 1 + ε ^ 5 / 49 := by rw [div_eq_mul_inv]