awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
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 ∈ 𝒜
⊢ m ≤ #s

Tactic:
mod_cast m_le_card_of_mem_chunk_parts (h𝒜 hs)

Premises used: SzemerediRegularity.stepBound, SzemerediRegularity.m_le_card_of_mem_chunk_parts, cast, Fintype.card, HDiv.hDiv, LE.le, Finpartition.parts, Finset.card, Eq.refl
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
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 ∈ 𝒜
⊢ m ≤ #s

Tactic:
exact mod_cast m_le_card_of_mem_chunk_parts (h𝒜 hs)

Premises used: SzemerediRegularity.m_le_card_of_mem_chunk_parts
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
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
rw₁ rw₂ : (↑m : ℝ) / HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 = (↑m : ℝ) / HAdd.hAdd (α := ℝ) (↑m : ℝ) 1
⊢ (↑m : ℝ) / HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 = 1 - 1 / HAdd.hAdd (α := ℝ) (↑m : ℝ) 1

Tactic:
rw [one_sub_div coe_m_add_one_pos.ne', add_sub_cancel_right]

Premises used: LT.lt.ne', SzemerediRegularity.coe_m_add_one_pos, add_sub_cancel_right, one_sub_div
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
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

Tactic:
have : (m : ℝ) / (m + 1) = 1 - 1 / (m + 1) := by
    rw [one_sub_div coe_m_add_one_pos.ne', add_sub_cancel_right]
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
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 :
  1 - HPow.hPow (β := ℕ) ε 5 / 50 ≤
    1 - 2 * (1 / HAdd.hAdd (α := ℝ) (↑m : ℝ) 1) + HPow.hPow (β := ℕ) (1 / HAdd.hAdd (α := ℝ) (↑m : ℝ) 1) 2
⊢ 1 - HPow.hPow (β := ℕ) ε 5 / 50 ≤ HPow.hPow (β := ℕ) ((↑m : ℝ) / HAdd.hAdd (α := ℝ) (↑m : ℝ) 1) 2

Tactic:
rw [this, sub_sq, one_pow, mul_one]

Premises used: one_pow, sub_sq, mul_one
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
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

Tactic:
le_trans ?_ (le_add_of_nonneg_right <| sq_nonneg _)

Premises used: le_add_of_nonneg_right, sq_nonneg, le_trans
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
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
refine : 1 - HPow.hPow (β := ℕ) ε 5 / 50 ≤ 1 - 2 * (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

Tactic:
refine le_trans ?_ (le_add_of_nonneg_right <| sq_nonneg _)

Premises used: le_add_of_nonneg_right, le_trans
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
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
⊢ LT.lt (α := ℝ) 0 2

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
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
rw₁ : 0 < HPow.hPow (β := ℕ) ε 5 / HMul.hMul (α := ℝ) 50 2
⊢ 1 - HPow.hPow (β := ℕ) ε 5 / 50 ≤ 1 - 2 * (1 / 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]

Premises used: le_div_iff₀', sub_le_sub_iff_left, one_div_le, SzemerediRegularity.coe_m_add_one_pos, div_div, one_div_div
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
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

Tactic:
le_trans ?_ (le_add_of_nonneg_right zero_le_one)

Premises used: zero_le_one, le_add_of_nonneg_right, le_trans
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
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
refine : HMul.hMul (α := ℝ) 50 2 / HPow.hPow (β := ℕ) ε 5 ≤ (↑m : ℝ)
⊢ HMul.hMul (α := ℝ) 50 2 / HPow.hPow (β := ℕ) ε 5 ≤ HAdd.hAdd (α := ℝ) (↑m : ℝ) 1

Tactic:
refine le_trans ?_ (le_add_of_nonneg_right zero_le_one)

Premises used: zero_le_one, le_add_of_nonneg_right, le_trans
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
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
norm_num : 100 / HPow.hPow (β := ℕ) ε 5 ≤ (↑m : ℝ)
⊢ HMul.hMul (α := ℝ) 50 2 / HPow.hPow (β := ℕ) ε 5 ≤ (↑m : ℝ)

Tactic:
norm_num
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
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
⊢ 100 / HPow.hPow (β := ℕ) ε 5 ≤ (↑m : ℝ)

Tactic:
apply hundred_div_ε_pow_five_le_m hPα hPε

Premises used: SzemerediRegularity.hundred_div_ε_pow_five_le_m
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
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
sz_positivity₄ sz_positivity₅ : 0 < m → 0 < ε → 0 < HPow.hPow (β := ℕ) ε 5 / HMul.hMul (α := ℝ) 50 2
⊢ 0 < HPow.hPow (β := ℕ) ε 5 / HMul.hMul (α := ℝ) 50 2

Tactic:
sz_positivity
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
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 ≤ ε
sz_positivity₄ sz_positivity₅ : 0 < m → 0 < ε → 0 ≤ ε
⊢ 0 ≤ ε

Tactic:
sz_positivity
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
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 ≤ ε

Tactic:
have : 0 ≤ ε := by sz_positivity
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
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
sz_positivity₄ sz_positivity₅ : 0 < m → 0 < ε → Ne (α := ℝ) (↑m : ℝ) 0
⊢ Ne (α := ℝ) (↑m : ℝ) 0

Tactic:
sz_positivity
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
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 ≤ ε
rw : HPow.hPow (β := ℕ) (1 + HDiv.hDiv (α := ℝ) 1 (↑m : ℝ)) 2 ≤ 1 + HPow.hPow (β := ℕ) ε 5 / 49
⊢ HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 / (↑m : ℝ)) 2 ≤ 1 + HPow.hPow (β := ℕ) ε 5 / 49

Tactic:
rw [same_add_div (by sz_positivity)]

Premises used: same_add_div
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
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 ≤ ε
hab : HDiv.hDiv (α := ℝ) 1 (↑m : ℝ) ≤ HPow.hPow (β := ℕ) ε 5 / 100
⊢ HPow.hPow (β := ℕ) (1 + HDiv.hDiv (α := ℝ) 1 (↑m : ℝ)) 2 ≤ HPow.hPow (β := ℕ) (1 + HPow.hPow (β := ℕ) ε 5 / 100) 2

Tactic:
gcongr (1 + ?_) ^ 2

Premises used: HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
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 ≤ ε
hab : HDiv.hDiv (α := ℝ) 1 (↑m : ℝ) ≤ 1 / (100 / HPow.hPow (β := ℕ) ε 5)
⊢ HDiv.hDiv (α := ℝ) 1 (↑m : ℝ) ≤ HPow.hPow (β := ℕ) ε 5 / 100

Tactic:
rw [← one_div_div (100 : ℝ)]

Premises used: OfNat.ofNat, one_div_div
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
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
sz_positivity₄ sz_positivity₅ : 0 < m → 0 < ε → 0 < 100 / HPow.hPow (β := ℕ) ε 5
⊢ 0 < 100 / HPow.hPow (β := ℕ) ε 5

Tactic:
sz_positivity
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
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 : ℝ) ≤ 1 / (100 / HPow.hPow (β := ℕ) ε 5)

Tactic:
exact one_div_le_one_div_of_le (by sz_positivity) (hundred_div_ε_pow_five_le_m hPα hPε)

Premises used: one_div_le_one_div_of_le, SzemerediRegularity.hundred_div_ε_pow_five_le_m
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
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 + HPow.hPow (β := ℕ) ε 5 / 100) 2 =
    1 + HPow.hPow (β := ℕ) ε 5 * (50⁻¹ + HPow.hPow (β := ℕ) ε 5 / 10000)

Tactic:
ring
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
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
bc₁ : LE.le (α := ℝ) 0 10000
bc₂ : 0 ≤ ε
⊢ 1 + HPow.hPow (β := ℕ) ε 5 * (50⁻¹ + HPow.hPow (β := ℕ) ε 5 / 10000) ≤
    1 + HPow.hPow (β := ℕ) ε 5 * (50⁻¹ + HPow.hPow (α := ℝ) (β := ℕ) 1 5 / 10000)

Tactic:
gcongr
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
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 : 50⁻¹ + HPow.hPow (α := ℝ) (β := ℕ) 1 5 / 10000 ≤ 49⁻¹
⊢ 1 + HPow.hPow (β := ℕ) ε 5 * (50⁻¹ + HPow.hPow (α := ℝ) (β := ℕ) 1 5 / 10000) ≤ 1 + HPow.hPow (β := ℕ) ε 5 * 49⁻¹

Tactic:
gcongr
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
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 ≤ ε
⊢ 50⁻¹ + HPow.hPow (α := ℝ) (β := ℕ) 1 5 / 10000 ≤ 49⁻¹

Tactic:
norm_num
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
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 ≤ ε
rw rw₁ : 1 + HPow.hPow (β := ℕ) ε 5 * 49⁻¹ = 1 + HPow.hPow (β := ℕ) ε 5 * 49⁻¹
⊢ 1 + HPow.hPow (β := ℕ) ε 5 * 49⁻¹ = 1 + HPow.hPow (β := ℕ) ε 5 / 49

Tactic:
rw [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
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)
_₃ : 1 + HPow.hPow (β := ℕ) ε 5 * (50⁻¹ + HPow.hPow (α := ℝ) (β := ℕ) 1 5 / 10000) ≤ 1 + HPow.hPow (β := ℕ) ε 5 * 49⁻¹
_₄ : 1 + HPow.hPow (β := ℕ) ε 5 * 49⁻¹ = 1 + HPow.hPow (β := ℕ) ε 5 / 49
⊢ HPow.hPow (β := ℕ) (1 + HDiv.hDiv (α := ℝ) 1 (↑m : ℝ)) 2 ≤ 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]

Premises used: HDiv.hDiv, Inv.inv, HPow.hPow, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst_3 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hU : U ∈ P.parts
hV : V ∈ P.parts
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
rw : HPow.hPow (β := ℕ) ε 5 / 50 * (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ) ≤ HPow.hPow (β := ℕ) ε 5 / 50
⊢ (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ) - HPow.hPow (β := ℕ) ε 5 / 50 ≤
    (1 - HPow.hPow (β := ℕ) ε 5 / 50) * (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ)

Tactic:
rw [sub_mul, one_mul, sub_le_sub_iff_left]

Premises used: sub_le_sub_iff_left, sub_mul, one_mul
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst_3 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hU : U ∈ P.parts
hV : V ∈ P.parts
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
sz_positivity sz_positivity₁ sz_positivity₂ sz_positivity₃ : 0 < m → 0 ≤ HPow.hPow (β := ℕ) ε 5 / 50
sz_positivity₄ sz_positivity₅ : 0 < m → 0 < ε → 0 ≤ HPow.hPow (β := ℕ) ε 5 / 50
⊢ 0 ≤ HPow.hPow (β := ℕ) ε 5 / 50

Tactic:
sz_positivity
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst_3 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hU : U ∈ P.parts
hV : V ∈ P.parts
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
refine : LE.le (α := ℝ) (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ) 1
⊢ HPow.hPow (β := ℕ) ε 5 / 50 * (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ) ≤ HPow.hPow (β := ℕ) ε 5 / 50

Tactic:
refine mul_le_of_le_one_right (by sz_positivity) ?_

Premises used: mul_le_of_le_one_right
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst_3 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hU : U ∈ P.parts
hV : V ∈ P.parts
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
⊢ LE.le (α := ℝ) (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ) 1

Tactic:
mod_cast G.edgeDensity_le_one _ _

Premises used: SimpleGraph.edgeDensity_le_one, congrArg, SimpleGraph.edgeDensity, cast, id, Rat.cast, LE.le, Finset.biUnion, Rat.cast_le_natCast._simp_1, Eq.symm, Nat.cast_one, Eq.trans
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst_3 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hU : U ∈ P.parts
hV : V ∈ P.parts
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
⊢ LE.le (α := ℝ) (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ) 1

Tactic:
exact mod_cast G.edgeDensity_le_one _ _

Premises used: SimpleGraph.edgeDensity_le_one
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst_3 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hU : U ∈ P.parts
hV : V ∈ P.parts
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
⊢ (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ) - HPow.hPow (β := ℕ) ε 5 / 50 ≤
    (1 - HPow.hPow (β := ℕ) ε 5 / 50) * (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ)

Tactic:
have : ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) - ε ^ 5 / ↑50 ≤
      (↑1 - ε ^ 5 / 50) * G.edgeDensity (A.biUnion id) (B.biUnion id) := by
    rw [sub_mul, one_mul, sub_le_sub_iff_left]
    refine mul_le_of_le_one_right (by sz_positivity) ?_
    exact mod_cast G.edgeDensity_le_one _ _
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst_3 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hU : U ∈ P.parts
hV : V ∈ P.parts
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
this :
  (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ) - HPow.hPow (β := ℕ) ε 5 / 50 ≤
    (1 - HPow.hPow (β := ℕ) ε 5 / 50) * (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ)
⊢ (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ) - HPow.hPow (β := ℕ) ε 5 / 50 ≤
    (∑ ab ∈ A.product B, (↑(G.edgeDensity ab.1 ab.2) : ℝ)) / HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#B) : ℝ)

Tactic:
this.trans ?_

Premises used: LE.le.trans