awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
The : (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤
The₁ :
  ∀ (top_case : (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤),
    (G □ H).edist x y = G.edist x.1 y.1 + H.edist x.2 y.2
The₂ : (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤
The₃ The₄ :
  ∀ (top_case : (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤),
    (G □ H).edist x y = G.edist x.1 y.1 + H.edist x.2 y.2
pos :
  ∀ (top_case : (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤) (h : (G □ H).edist x y = ⊤),
    (G □ H).edist x y = G.edist x.1 y.1 + H.edist x.2 y.2
neg neg₁ :
  ∀ (top_case : (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤) (h : ¬(G □ H).edist x y = ⊤),
    (G □ H).edist x y = G.edist x.1 y.1 + H.edist x.2 y.2
⊢ (G □ H).edist x y = G.edist x.1 y.1 + H.edist x.2 y.2

Tactic:
classical
  -- The case `(G □ H).edist x y = ⊤` is used twice, so better to factor it out.
  have top_case : (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤ := by
    simp_rw [← not_ne_iff, edist_ne_top_iff_reachable, reachable_boxProd, not_and_or]
  by_cases h : (G □ H).edist x y = ⊤
  · rw [top_case] at h
    aesop
  · have rGH : G.edist x.1 y.1 ≠ ⊤ ∧ H.edist x.2 y.2 ≠ ⊤ := by rw [top_case] at h; aesop
    have ⟨wG, hwG⟩ := exists_walk_of_edist_ne_top rGH.1
    have ⟨wH, hwH⟩ := exists_walk_of_edist_ne_top rGH.2
    let w_app := (wG.boxProdLeft _ _).append (wH.boxProdRight _ _)
    have w_len : w_app.length = wG.length + wH.length := by
      unfold w_app Walk.boxProdLeft Walk.boxProdRight; simp
    refine le_antisymm ?_ ?_
    · calc (G □ H).edist x y ≤ w_app.length := by exact edist_le _
          _ = wG.length + wH.length := by exact_mod_cast w_len
          _ = G.edist x.1 y.1 + H.edist x.2 y.2 := by simp only [hwG, hwH]
    · have ⟨w, hw⟩ := exists_walk_of_edist_ne_top h
      rw [← hw, Walk.length_boxProd]
      exact add_le_add (edist_le w.ofBoxProdLeft) (edist_le w.ofBoxProdRight)

Premises used: SimpleGraph.boxProd, Prod.fst, SimpleGraph.Walk.length_boxProd, le_antisymm, SimpleGraph.edist, Prod.snd
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
Goal:
n : ℕ
⊢ LT.lt (α := ℕ) 0 4

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
Goal:
x x_1 : ℕ
h : x ≤ x_1
h₂ : LE.le (α := ℕ) 1 4
⊢ x * HPow.hPow (α := ℕ) 4 x ≤ x_1 * HPow.hPow (α := ℕ) 4 x_1

Tactic:
gcongr
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
Goal:
x x_1 : ℕ
h : x ≤ x_1
⊢ LE.le (α := ℕ) 1 4

Tactic:
decide
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
Goal:
n : ℕ
⊢ 0 < HPow.hPow (α := ℕ) 4 n

Tactic:
positivity
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
Goal:
α : Type u_1
inst : Semiring α
n : ℕ
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ :
  Eq.{u_1 + 1} (α := α) (↑(n * HPow.hPow (α := ℕ) 4 n) : α) (↑(n * HPow.hPow (α := ℕ) 4 n) : α)
⊢ (↑(n * HPow.hPow (α := ℕ) 4 n) : α) = (↑n : α) * HPow.hPow (α := α) 4 n

Tactic:
norm_cast
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
Goal:
ε : ℝ
n : ℕ
h : 100 ≤ HPow.hPow (α := ℝ) 4 n * HPow.hPow (β := ℕ) ε 5
⊢ Odd (α := ℕ) 5

Tactic:
decide
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
Goal:
ε : ℝ
n : ℕ
h : 100 ≤ HPow.hPow (α := ℝ) 4 n * HPow.hPow (β := ℕ) ε 5
⊢ LT.lt (α := ℝ) 0 100

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
Goal:
ε : ℝ
n : ℕ
h : 100 ≤ HPow.hPow (α := ℝ) 4 n * HPow.hPow (β := ℕ) ε 5
⊢ 0 ≤ HPow.hPow (α := ℝ) 4 n

Tactic:
positivity
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
P : Finpartition (α := Finset α) univ
inst_2 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
bc : LE.le (α := ℕ) 4 16
⊢ #P.parts * HPow.hPow (α := ℕ) 4 #P.parts ≤ #P.parts * HPow.hPow (α := ℕ) 16 #P.parts

Tactic:
gcongr
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
P : Finpartition (α := Finset α) univ
inst_2 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
⊢ LE.le (α := ℕ) 4 16

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
P : Finpartition (α := Finset α) univ
inst_2 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
sz_positivity sz_positivity₁ sz_positivity₂ sz_positivity₃ sz_positivity₄ sz_positivity₅ : 0 < m → 0 < m
⊢ 0 < m

Tactic:
sz_positivity
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
P : Finpartition (α := Finset α) univ
⊢ 0 < HAdd.hAdd (α := ℝ) (↑m : ℝ) 1

Tactic:
positivity
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
P : Finpartition (α := Finset α) univ
inst_2 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
⊢ LE.le (α := ℝ) 1 (↑(Fintype.card α / stepBound #P.parts) : ℝ)

Tactic:
Nat.one_le_cast.2 <| m_pos hPα

Premises used: Iff.mpr, Nat.one_le_cast, SzemerediRegularity.m_pos
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
P : Finpartition (α := Finset α) univ
ε : ℝ
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
⊢ LT.lt (α := ℝ) 0 100

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
P : Finpartition (α := Finset α) univ
ε : ℝ
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
⊢ 0 ≤ HPow.hPow (α := ℝ) 4 #P.parts

Tactic:
positivity
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
P : Finpartition (α := Finset α) univ
ε : ℝ
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
⊢ Odd (α := ℕ) 5

Tactic:
decide
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
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
⊢ 0 ≤ HPow.hPow (α := ℝ) 4 #P.parts

Tactic:
positivity
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
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
norm_cast : HPow.hPow (α := ℕ) 4 #P.parts ≤ m
⊢ HPow.hPow (α := ℝ) 4 #P.parts ≤ (↑m : ℝ)

Tactic:
norm_cast
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
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
rwa : HPow.hPow (α := ℕ) 4 #P.parts * stepBound #P.parts ≤ Fintype.card α
rwa₁ : HPow.hPow (α := ℕ) 4 #P.parts * (#P.parts * HPow.hPow (α := ℕ) 4 #P.parts) ≤ Fintype.card α
rwa₂ : #P.parts * (HPow.hPow (α := ℕ) 4 #P.parts * HPow.hPow (α := ℕ) 4 #P.parts) ≤ Fintype.card α
rwa₃ rwa₄ rwa₅ rwa₆ : #P.parts * HMul.hMul (α := ℕ) 4 4 ^ #P.parts ≤ Fintype.card α
⊢ HPow.hPow (α := ℕ) 4 #P.parts ≤ m

Tactic:
rwa [Nat.le_div_iff_mul_le (stepBound_pos (P.parts_nonempty <|
      univ_nonempty.ne_empty).card_pos), stepBound, mul_left_comm, ← mul_pow]

Premises used: SzemerediRegularity.stepBound_pos, SzemerediRegularity.stepBound, Finset.univ_nonempty, Finset.Nonempty.card_pos, mul_left_comm, Finset.Nonempty.ne_empty, Nat.le_div_iff_mul_le, mul_pow, Finpartition.parts_nonempty
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
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
⊢ LE.le (α := ℝ) 0 100

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
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 < HPow.hPow (β := ℕ) ε 5
sz_positivity₄ sz_positivity₅ : 0 < m → 0 < ε → 0 < HPow.hPow (β := ℕ) ε 5
⊢ 0 < HPow.hPow (β := ℕ) ε 5

Tactic:
sz_positivity
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
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.Bound
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
P : Finpartition (α := Finset α) univ
⊢ LE.le (α := ℕ) 1 4

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
P : Finpartition (α := Finset α) univ
⊢ 1 ≤ HPow.hPow (α := ℕ) 4 #P.parts

Tactic:
have h : 1 ≤ 4 ^ #P.parts := one_le_pow₀ (by simp)
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
P : Finpartition (α := Finset α) univ
h : 1 ≤ HPow.hPow (α := ℕ) 4 #P.parts
rw :
  Fintype.card α / #P.parts -
        Fintype.card α / #P.parts / HPow.hPow (α := ℕ) 4 #P.parts * HPow.hPow (α := ℕ) 4 #P.parts +
      1 ≤
    HPow.hPow (α := ℕ) 4 #P.parts
⊢ a + 1 ≤ HPow.hPow (α := ℕ) 4 #P.parts

Tactic:
rw [stepBound, ← Nat.div_div_eq_div_mul]

Premises used: SzemerediRegularity.stepBound, Nat.div_div_eq_div_mul
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
P : Finpartition (α := Finset α) univ
h : 1 ≤ HPow.hPow (α := ℕ) 4 #P.parts
rw : HPow.hPow (α := ℕ) 4 #P.parts - 1 + 1
| HPow.hPow (α := ℕ) 4 #P.parts

Tactic:
rw [← Nat.sub_add_cancel h]

Premises used: Nat.sub_add_cancel
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
P : Finpartition (α := Finset α) univ
h : 1 ≤ HPow.hPow (α := ℕ) 4 #P.parts
conv_rhs :
  Fintype.card α / #P.parts -
        Fintype.card α / #P.parts / HPow.hPow (α := ℕ) 4 #P.parts * HPow.hPow (α := ℕ) 4 #P.parts +
      1 ≤
    HPow.hPow (α := ℕ) 4 #P.parts - 1 + 1
⊢ Fintype.card α / #P.parts -
        Fintype.card α / #P.parts / HPow.hPow (α := ℕ) 4 #P.parts * HPow.hPow (α := ℕ) 4 #P.parts +
      1 ≤
    HPow.hPow (α := ℕ) 4 #P.parts

Tactic:
conv_rhs => rw [← Nat.sub_add_cancel h]

Premises used: Nat.sub_add_cancel
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
P : Finpartition (α := Finset α) univ
h : 1 ≤ HPow.hPow (α := ℕ) 4 #P.parts
rw :
  Fintype.card α / #P.parts ≤
    Fintype.card α / #P.parts / HPow.hPow (α := ℕ) 4 #P.parts * HPow.hPow (α := ℕ) 4 #P.parts +
        HPow.hPow (α := ℕ) 4 #P.parts -
      1
⊢ Fintype.card α / #P.parts -
        Fintype.card α / #P.parts / HPow.hPow (α := ℕ) 4 #P.parts * HPow.hPow (α := ℕ) 4 #P.parts +
      1 ≤
    HPow.hPow (α := ℕ) 4 #P.parts - 1 + 1

Tactic:
rw [add_le_add_iff_right, tsub_le_iff_left, ← Nat.add_sub_assoc h]

Premises used: Nat.add_sub_assoc, tsub_le_iff_left, add_le_add_iff_right
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
P : Finpartition (α := Finset α) univ
h : 1 ≤ HPow.hPow (α := ℕ) 4 #P.parts
⊢ Fintype.card α / #P.parts ≤
    Fintype.card α / #P.parts / HPow.hPow (α := ℕ) 4 #P.parts * HPow.hPow (α := ℕ) 4 #P.parts +
        HPow.hPow (α := ℕ) 4 #P.parts -
      1

Tactic:
Nat.le_sub_one_of_lt (Nat.lt_div_mul_add h)

Premises used: Nat.lt_div_mul_add, Nat.le_sub_one_of_lt
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
P : Finpartition (α := Finset α) univ
h : 1 ≤ HPow.hPow (α := ℕ) 4 #P.parts
⊢ Fintype.card α / #P.parts ≤
    Fintype.card α / #P.parts / HPow.hPow (α := ℕ) 4 #P.parts * HPow.hPow (α := ℕ) 4 #P.parts +
        HPow.hPow (α := ℕ) 4 #P.parts -
      1

Tactic:
exact Nat.le_sub_one_of_lt (Nat.lt_div_mul_add h)

Premises used: Nat.lt_div_mul_add, Nat.le_sub_one_of_lt
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
P : Finpartition (α := Finset α) univ
u : Finset α
hucard : #u = m * HPow.hPow (α := ℕ) 4 #P.parts + a
rw : (HPow.hPow (α := ℕ) 4 #P.parts - a) * m + a * (m + 1) = m * HPow.hPow (α := ℕ) 4 #P.parts + a
rw₁ : (HPow.hPow (α := ℕ) 4 #P.parts - a) * m + (a * m + a * 1) = m * HPow.hPow (α := ℕ) 4 #P.parts + a
rw₂ : (HPow.hPow (α := ℕ) 4 #P.parts - a) * m + (a * m + a) = m * HPow.hPow (α := ℕ) 4 #P.parts + a
rw₃ : (HPow.hPow (α := ℕ) 4 #P.parts - a) * m + a * m + a = m * HPow.hPow (α := ℕ) 4 #P.parts + a
rw₄ : (HPow.hPow (α := ℕ) 4 #P.parts - a + a) * m + a = m * HPow.hPow (α := ℕ) 4 #P.parts + a
rw₅ : HPow.hPow (α := ℕ) 4 #P.parts * m + a = m * HPow.hPow (α := ℕ) 4 #P.parts + a
rw₆ rw₇ : m * HPow.hPow (α := ℕ) 4 #P.parts + a = m * HPow.hPow (α := ℕ) 4 #P.parts + a
⊢ (HPow.hPow (α := ℕ) 4 #P.parts - a) * m + a * (m + 1) = #u

Tactic:
rw [hucard, mul_add, mul_one, ← add_assoc, ← add_mul,
    Nat.sub_add_cancel ((Nat.le_succ _).trans a_add_one_le_four_pow_parts_card), mul_comm]

Premises used: add_mul, SzemerediRegularity.a_add_one_le_four_pow_parts_card, add_assoc, Nat.le_succ, Nat.sub_add_cancel, mul_comm, mul_add, LE.le.trans, mul_one
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
P : Finpartition (α := Finset α) univ
u : Finset α
hP : P.IsEquipartition
hu : u ∈ P.parts
hucard : #u ≠ m * HPow.hPow (α := ℕ) 4 #P.parts + a
rw :
  Fintype.card α / #P.parts / HPow.hPow (α := ℕ) 4 #P.parts * HPow.hPow (α := ℕ) 4 #P.parts ≤ Fintype.card α / #P.parts
⊢ m * HPow.hPow (α := ℕ) 4 #P.parts ≤ Fintype.card α / #P.parts

Tactic:
rw [stepBound, ← Nat.div_div_eq_div_mul]

Premises used: SzemerediRegularity.stepBound, Nat.div_div_eq_div_mul
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
P : Finpartition (α := Finset α) univ
u : Finset α
hP : P.IsEquipartition
hu : u ∈ P.parts
hucard : #u ≠ m * HPow.hPow (α := ℕ) 4 #P.parts + a
⊢ Fintype.card α / #P.parts / HPow.hPow (α := ℕ) 4 #P.parts * HPow.hPow (α := ℕ) 4 #P.parts ≤ Fintype.card α / #P.parts

Tactic:
Nat.div_mul_le_self _ _

Premises used: Nat.div_mul_le_self
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
P : Finpartition (α := Finset α) univ
u : Finset α
hP : P.IsEquipartition
hu : u ∈ P.parts
hucard : #u ≠ m * HPow.hPow (α := ℕ) 4 #P.parts + a
⊢ Fintype.card α / #P.parts / HPow.hPow (α := ℕ) 4 #P.parts * HPow.hPow (α := ℕ) 4 #P.parts ≤ Fintype.card α / #P.parts

Tactic:
exact Nat.div_mul_le_self _ _

Premises used: Nat.div_mul_le_self
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
P : Finpartition (α := Finset α) univ
u : Finset α
hP : P.IsEquipartition
hu : u ∈ P.parts
hucard : #u ≠ m * HPow.hPow (α := ℕ) 4 #P.parts + a
⊢ m * HPow.hPow (α := ℕ) 4 #P.parts ≤ Fintype.card α / #P.parts

Tactic:
have : m * 4 ^ #P.parts ≤ card α / #P.parts := by
    rw [stepBound, ← Nat.div_div_eq_div_mul]
    exact Nat.div_mul_le_self _ _
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
P : Finpartition (α := Finset α) univ
u : Finset α
hP : P.IsEquipartition
hu : u ∈ P.parts
hucard : #u ≠ m * HPow.hPow (α := ℕ) 4 #P.parts + a
this : m * HPow.hPow (α := ℕ) 4 #P.parts ≤ Fintype.card α / #P.parts
⊢ #u ≠ Fintype.card α / #P.parts

Tactic:
rw [Nat.add_sub_of_le this] at hucard

Premises used: Nat.add_sub_of_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
P : Finpartition (α := Finset α) univ
u : Finset α
hP : P.IsEquipartition
hu : u ∈ P.parts
hucard : #u ≠ m * HPow.hPow (α := ℕ) 4 #P.parts + a
this : m * HPow.hPow (α := ℕ) 4 #P.parts ≤ Fintype.card α / #P.parts
hucard₁ : #u ≠ Fintype.card α / #P.parts
⊢ m * HPow.hPow (α := ℕ) 4 #P.parts ≤ Fintype.card α / #P.parts

Tactic:
rw [Nat.add_sub_of_le this] at hucard

Premises used: Nat.add_sub_of_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
P : Finpartition (α := Finset α) univ
u : Finset α
hP : P.IsEquipartition
hu : u ∈ P.parts
hucard : #u ≠ Fintype.card α / #P.parts
this : m * HPow.hPow (α := ℕ) 4 #P.parts ≤ Fintype.card α / #P.parts
rw : (HPow.hPow (α := ℕ) 4 #P.parts - (a + 1)) * m + (a + 1) * (m + 1) = Finset.card.{u_1} (α := α) univ / #P.parts + 1
rw₁ :
  (HPow.hPow (α := ℕ) 4 #P.parts - (a + 1)) * m + ((a + 1) * m + (a + 1) * 1) =
    Finset.card.{u_1} (α := α) univ / #P.parts + 1
rw₂ :
  (HPow.hPow (α := ℕ) 4 #P.parts - (a + 1)) * m + ((a + 1) * m + (a + 1)) =
    Finset.card.{u_1} (α := α) univ / #P.parts + 1
rw₃ :
  (HPow.hPow (α := ℕ) 4 #P.parts - (a + 1)) * m + (a + 1) * m + (a + 1) = Finset.card.{u_1} (α := α) univ / #P.parts + 1
rw₄ : (HPow.hPow (α := ℕ) 4 #P.parts - (a + 1) + (a + 1)) * m + (a + 1) = Finset.card.{u_1} (α := α) univ / #P.parts + 1
rw₅ : HPow.hPow (α := ℕ) 4 #P.parts * m + (a + 1) = Finset.card.{u_1} (α := α) univ / #P.parts + 1
rw₆ : HPow.hPow (α := ℕ) 4 #P.parts * m + a + 1 = Finset.card.{u_1} (α := α) univ / #P.parts + 1
rw₇ : m * HPow.hPow (α := ℕ) 4 #P.parts + a + 1 = Finset.card.{u_1} (α := α) univ / #P.parts + 1
rw₈ : Fintype.card α / #P.parts + 1 = Finset.card.{u_1} (α := α) univ / #P.parts + 1
rw₉ rw₁₀ : Fintype.card α / #P.parts + 1 = Fintype.card α / #P.parts + 1
⊢ (HPow.hPow (α := ℕ) 4 #P.parts - (a + 1)) * m + (a + 1) * (m + 1) = #u

Tactic:
rw [(hP.card_parts_eq_average hu).resolve_left hucard, mul_add, mul_one, ← add_assoc, ← add_mul,
    Nat.sub_add_cancel a_add_one_le_four_pow_parts_card, ← add_assoc, mul_comm,
    Nat.add_sub_of_le this, card_univ]

Premises used: add_mul, Finset.card_univ, SzemerediRegularity.a_add_one_le_four_pow_parts_card, Finpartition.IsEquipartition.card_parts_eq_average, add_assoc, Nat.add_sub_of_le, Or.resolve_left, Nat.sub_add_cancel, mul_comm, mul_add, mul_one
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
P : Finpartition (α := Finset α) univ
u : Finset α
hP : P.IsEquipartition
hu : u ∈ P.parts
norm_cast : HPow.hPow (α := ℕ) 4 #P.parts * m ≤ #u
⊢ HPow.hPow (α := ℝ) 4 #P.parts * (↑m : ℝ) ≤ (↑(#u) : ℝ)

Tactic:
norm_cast
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
P : Finpartition (α := Finset α) univ
u : Finset α
hP : P.IsEquipartition
hu : u ∈ P.parts
rw : HPow.hPow (α := ℕ) 4 #P.parts * (Fintype.card α / #P.parts / HPow.hPow (α := ℕ) 4 #P.parts) ≤ #u
⊢ HPow.hPow (α := ℕ) 4 #P.parts * m ≤ #u

Tactic:
rw [stepBound, ← Nat.div_div_eq_div_mul]

Premises used: SzemerediRegularity.stepBound, Nat.div_div_eq_div_mul
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
P : Finpartition (α := Finset α) univ
u : Finset α
hP : P.IsEquipartition
hu : u ∈ P.parts
⊢ HPow.hPow (α := ℕ) 4 #P.parts * (Fintype.card α / #P.parts / HPow.hPow (α := ℕ) 4 #P.parts) ≤ #u

Tactic:
(Nat.mul_div_le _ _).trans (hP.average_le_card_part hu)

Premises used: Finpartition.IsEquipartition.average_le_card_part, Nat.mul_div_le, LE.le.trans
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
P : Finpartition (α := Finset α) univ
u : Finset α
hP : P.IsEquipartition
hu : u ∈ P.parts
⊢ HPow.hPow (α := ℕ) 4 #P.parts * (Fintype.card α / #P.parts / HPow.hPow (α := ℕ) 4 #P.parts) ≤ #u

Tactic:
exact (Nat.mul_div_le _ _).trans (hP.average_le_card_part hu)

Premises used: Finpartition.IsEquipartition.average_le_card_part, Nat.mul_div_le, LE.le.trans
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
Goal:
ε : ℝ
l : ℕ
⊢ l ≤ initialBound ε l

Tactic:
(le_max_left _ _).trans <| le_max_right _ _

Premises used: le_max_right, LE.le.trans, le_max_left
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
Goal:
ε : ℝ
l : ℕ
⊢ 7 ≤ initialBound ε l

Tactic:
le_max_left _ _

Premises used: SzemerediRegularity.initialBound, le_max_left
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
Goal:
ε : ℝ
l : ℕ
⊢ 0 < initialBound ε l

Tactic:
Nat.succ_pos'.trans_le <| seven_le_initialBound _ _

Premises used: Nat.succ_pos', SzemerediRegularity.seven_le_initialBound, LT.lt.trans_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
Goal:
ε : ℝ
hε : 0 < ε
l : ℕ
rw :
  log (100 / HPow.hPow (β := ℕ) ε 5) / log 4 <
    max (↑7 : ℝ) (max (↑l : ℝ) (↑(⌊log (100 / HPow.hPow (β := ℕ) ε 5) / log 4⌋₊ + 1) : ℝ))
rw₁ : 0 < log 4
rw₂ : 0 < 100 / HPow.hPow (β := ℕ) ε 5
⊢ 100 < HPow.hPow (α := ℝ) 4 (initialBound ε l) * HPow.hPow (β := ℕ) ε 5

Tactic:
rw [← rpow_natCast 4, ← div_lt_iff₀ (pow_pos hε 5), lt_rpow_iff_log_lt _ zero_lt_four, ←
    div_lt_iff₀, initialBound, Nat.cast_max, Nat.cast_max]

Premises used: pow_pos, Nat.cast_max, div_lt_iff₀, zero_lt_four, SzemerediRegularity.initialBound, OfNat.ofNat, Real.rpow_natCast, Real.lt_rpow_iff_log_lt
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
Goal:
ε : ℝ
hε : 0 < ε
l : ℕ
push_cast :
  log (100 / HPow.hPow (β := ℕ) ε 5) / log 4 <
    max 7 (max (↑l : ℝ) (HAdd.hAdd (α := ℝ) (↑⌊log (100 / HPow.hPow (β := ℕ) ε 5) / log 4⌋₊ : ℝ) 1))
⊢ log (100 / HPow.hPow (β := ℕ) ε 5) / log 4 <
    max (↑7 : ℝ) (max (↑l : ℝ) (↑(⌊log (100 / HPow.hPow (β := ℕ) ε 5) / log 4⌋₊ + 1) : ℝ))

Tactic:
push_cast
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
Goal:
ε : ℝ
hε : 0 < ε
l : ℕ
⊢ log (100 / HPow.hPow (β := ℕ) ε 5) / log 4 <
    max 7 (max (↑l : ℝ) (HAdd.hAdd (α := ℝ) (↑⌊log (100 / HPow.hPow (β := ℕ) ε 5) / log 4⌋₊ : ℝ) 1))

Tactic:
lt_max_of_lt_right (lt_max_of_lt_right <| Nat.lt_floor_add_one _)

Premises used: lt_max_of_lt_right, Nat.lt_floor_add_one
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
Goal:
ε : ℝ
hε : 0 < ε
l : ℕ
⊢ log (100 / HPow.hPow (β := ℕ) ε 5) / log 4 <
    max 7 (max (↑l : ℝ) (HAdd.hAdd (α := ℝ) (↑⌊log (100 / HPow.hPow (β := ℕ) ε 5) / log 4⌋₊ : ℝ) 1))

Tactic:
exact lt_max_of_lt_right (lt_max_of_lt_right <| Nat.lt_floor_add_one _)

Premises used: lt_max_of_lt_right, Nat.lt_floor_add_one
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
Goal:
ε : ℝ
hε : 0 < ε
l : ℕ
⊢ LT.lt (α := ℝ) 1 4

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
Goal:
ε : ℝ
hε : 0 < ε
l : ℕ
⊢ 0 < log 4

Tactic:
exact log_pos (by simp)

Premises used: Real.log_pos
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
Goal:
ε : ℝ
hε : 0 < ε
l : ℕ
⊢ LT.lt (α := ℝ) 0 100

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
Goal:
ε : ℝ
hε : 0 < ε
l : ℕ
⊢ 0 < 100 / HPow.hPow (β := ℕ) ε 5

Tactic:
exact div_pos (by simp) (pow_pos hε 5)

Premises used: pow_pos, div_pos, OfNat.ofNat
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
Goal:
ε : ℝ
l : ℕ
⊢ 0 < HPow.hPow (α := ℕ) 16 (stepBound^[⌊4 / HPow.hPow (β := ℕ) ε 5⌋₊] (initialBound ε l))

Tactic:
positivity