awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Bound (goal)
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 +
      1 ≤
    HPow.hPow (α := ℕ) 4 #P.parts - 1 + 1
have 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
Tactic: rw [add_le_add_iff_right, tsub_le_iff_left, ← Nat.add_sub_assoc h]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Bound (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
P : Finpartition (α := Finset α) univ
u : Finset α
hucard : #u = m * HPow.hPow (α := ℕ) 4 #P.parts + a
⊢ (HPow.hPow (α := ℕ) 4 #P.parts - a) * m + a * (m + 1) = #u
have rw : (HPow.hPow (α := ℕ) 4 #P.parts - a) * m + a * (m + 1) = m * HPow.hPow (α := ℕ) 4 #P.parts + a
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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Bound (goal)
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
⊢ (HPow.hPow (α := ℕ) 4 #P.parts - a) * m + a * (m + 1) = #u
have rw₁ : (HPow.hPow (α := ℕ) 4 #P.parts - a) * m + (a * m + a * 1) = m * HPow.hPow (α := ℕ) 4 #P.parts + a
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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Bound (goal)
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
⊢ (HPow.hPow (α := ℕ) 4 #P.parts - a) * m + a * (m + 1) = #u
have rw₂ : (HPow.hPow (α := ℕ) 4 #P.parts - a) * m + (a * m + a) = m * HPow.hPow (α := ℕ) 4 #P.parts + a
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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Bound (goal)
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
⊢ (HPow.hPow (α := ℕ) 4 #P.parts - a) * m + a * (m + 1) = #u
have rw₃ : (HPow.hPow (α := ℕ) 4 #P.parts - a) * m + a * m + a = m * HPow.hPow (α := ℕ) 4 #P.parts + a
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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Bound (goal)
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
⊢ (HPow.hPow (α := ℕ) 4 #P.parts - a) * m + a * (m + 1) = #u
have rw₄ : (HPow.hPow (α := ℕ) 4 #P.parts - a + a) * m + a = m * HPow.hPow (α := ℕ) 4 #P.parts + a
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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Bound (goal)
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
⊢ (HPow.hPow (α := ℕ) 4 #P.parts - a) * m + a * (m + 1) = #u
have rw₅ : HPow.hPow (α := ℕ) 4 #P.parts * m + a = m * HPow.hPow (α := ℕ) 4 #P.parts + a
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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Bound (goal)
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
⊢ (HPow.hPow (α := ℕ) 4 #P.parts - a) * m + a * (m + 1) = #u
have rw₆ : m * HPow.hPow (α := ℕ) 4 #P.parts + a = m * HPow.hPow (α := ℕ) 4 #P.parts + a
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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Bound (goal)
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
have rw : Fintype.card α / #P.parts / HPow.hPow (α := ℕ) 4 #P.parts * HPow.hPow (α := ℕ) 4 #P.parts ≤ Fintype.card α / #P.parts
Tactic: rw [stepBound, ← Nat.div_div_eq_div_mul]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Bound (hypothesis)
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
⊢ (HPow.hPow (α := ℕ) 4 #P.parts - (a + 1)) * m + (a + 1) * (m + 1) = #u
have this : 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 _ _
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Bound (hypothesis)
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
⊢ (HPow.hPow (α := ℕ) 4 #P.parts - (a + 1)) * m + (a + 1) * (m + 1) = #u
have hucard₁ : #u ≠ Fintype.card α / #P.parts
Tactic: rw [Nat.add_sub_of_le this] at hucard
Cleared hypotheses: hucard, this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Bound (goal)
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
⊢ (HPow.hPow (α := ℕ) 4 #P.parts - (a + 1)) * m + (a + 1) * (m + 1) = #u
have rw : (HPow.hPow (α := ℕ) 4 #P.parts - (a + 1)) * m + (a + 1) * (m + 1) = Finset.card.{u_1} (α := α) univ / #P.parts + 1
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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Bound (goal)
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
⊢ (HPow.hPow (α := ℕ) 4 #P.parts - (a + 1)) * m + (a + 1) * (m + 1) = #u
have rw₁ : (HPow.hPow (α := ℕ) 4 #P.parts - (a + 1)) * m + ((a + 1) * m + (a + 1) * 1) =
  Finset.card.{u_1} (α := α) univ / #P.parts + 1
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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Bound (goal)
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
⊢ (HPow.hPow (α := ℕ) 4 #P.parts - (a + 1)) * m + (a + 1) * (m + 1) = #u
have rw₂ : (HPow.hPow (α := ℕ) 4 #P.parts - (a + 1)) * m + ((a + 1) * m + (a + 1)) = Finset.card.{u_1} (α := α) univ / #P.parts + 1
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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Bound (goal)
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
⊢ (HPow.hPow (α := ℕ) 4 #P.parts - (a + 1)) * m + (a + 1) * (m + 1) = #u
have rw₃ : (HPow.hPow (α := ℕ) 4 #P.parts - (a + 1)) * m + (a + 1) * m + (a + 1) = Finset.card.{u_1} (α := α) univ / #P.parts + 1
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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Bound (goal)
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
⊢ (HPow.hPow (α := ℕ) 4 #P.parts - (a + 1)) * m + (a + 1) * (m + 1) = #u
have rw₄ : (HPow.hPow (α := ℕ) 4 #P.parts - (a + 1) + (a + 1)) * m + (a + 1) = Finset.card.{u_1} (α := α) univ / #P.parts + 1
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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Bound (goal)
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
⊢ (HPow.hPow (α := ℕ) 4 #P.parts - (a + 1)) * m + (a + 1) * (m + 1) = #u
have rw₅ : HPow.hPow (α := ℕ) 4 #P.parts * m + (a + 1) = Finset.card.{u_1} (α := α) univ / #P.parts + 1
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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Bound (goal)
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
⊢ (HPow.hPow (α := ℕ) 4 #P.parts - (a + 1)) * m + (a + 1) * (m + 1) = #u
have rw₆ : HPow.hPow (α := ℕ) 4 #P.parts * m + a + 1 = Finset.card.{u_1} (α := α) univ / #P.parts + 1
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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Bound (goal)
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
⊢ (HPow.hPow (α := ℕ) 4 #P.parts - (a + 1)) * m + (a + 1) * (m + 1) = #u
have rw₇ : m * HPow.hPow (α := ℕ) 4 #P.parts + a + 1 = Finset.card.{u_1} (α := α) univ / #P.parts + 1
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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Bound (goal)
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
⊢ (HPow.hPow (α := ℕ) 4 #P.parts - (a + 1)) * m + (a + 1) * (m + 1) = #u
have rw₈ : Fintype.card α / #P.parts + 1 = Finset.card.{u_1} (α := α) univ / #P.parts + 1
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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Bound (goal)
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
⊢ (HPow.hPow (α := ℕ) 4 #P.parts - (a + 1)) * m + (a + 1) * (m + 1) = #u
have rw₉ : Fintype.card α / #P.parts + 1 = Fintype.card α / #P.parts + 1
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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Bound (goal)
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 * (↑m : ℝ) ≤ (↑(#u) : ℝ)
have norm_cast : HPow.hPow (α := ℕ) 4 #P.parts * m ≤ #u
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Bound (goal)
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 * m ≤ #u
have rw : HPow.hPow (α := ℕ) 4 #P.parts * (Fintype.card α / #P.parts / HPow.hPow (α := ℕ) 4 #P.parts) ≤ #u
Tactic: rw [stepBound, ← Nat.div_div_eq_div_mul]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Bound (goal)
Goal:
ε : ℝ
hε : 0 < ε
l : ℕ
⊢ 100 < HPow.hPow (α := ℝ) 4 (initialBound ε l) * HPow.hPow (β := ℕ) ε 5
have rw : log (100 / HPow.hPow (β := ℕ) ε 5) / log 4 <
  max (↑7 : ℝ) (max (↑l : ℝ) (↑(⌊log (100 / HPow.hPow (β := ℕ) ε 5) / log 4⌋₊ + 1) : ℝ))
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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Bound (goal)
Goal:
ε : ℝ
hε : 0 < ε
l : ℕ
rw :
  log (100 / HPow.hPow (β := ℕ) ε 5) / log 4 <
    max (↑7 : ℝ) (max (↑l : ℝ) (↑(⌊log (100 / HPow.hPow (β := ℕ) ε 5) / log 4⌋₊ + 1) : ℝ))
⊢ 100 < HPow.hPow (α := ℝ) 4 (initialBound ε l) * HPow.hPow (β := ℕ) ε 5
have rw₁ : 0 < log 4
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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Bound (goal)
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
⊢ 100 < HPow.hPow (α := ℝ) 4 (initialBound ε l) * HPow.hPow (β := ℕ) ε 5
have rw₂ : 0 < 100 / 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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Bound (goal)
Goal:
ε : ℝ
hε : 0 < ε
l : ℕ
⊢ log (100 / HPow.hPow (β := ℕ) ε 5) / log 4 <
    max (↑7 : ℝ) (max (↑l : ℝ) (↑(⌊log (100 / HPow.hPow (β := ℕ) ε 5) / log 4⌋₊ + 1) : ℝ))
have push_cast : log (100 / HPow.hPow (β := ℕ) ε 5) / log 4 <
  max 7 (max (↑l : ℝ) (HAdd.hAdd (α := ℝ) (↑⌊log (100 / HPow.hPow (β := ℕ) ε 5) / log 4⌋₊ : ℝ) 1))
Tactic: push_cast