awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (hypothesis)
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
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
hP₁ : 0 < #P.parts
this : HPow.hPow (α := ℝ) 2 #P.parts * (↑m : ℝ) / ((↑(#U) : ℝ) * ε) ≤ ε / 10
⊢ HPow.hPow (α := ℝ) 2 (#P.parts - 1) * (↑m : ℝ) ≤
    HPow.hPow (α := ℝ) 2 #P.parts * (↑m : ℝ) / ((↑(#U) : ℝ) * ε) * (↑(#(G.nonuniformWitness ε U V)) : ℝ)
have this₁ : HPow.hPow (α := ℝ) 2 #P.parts = HPow.hPow (α := ℝ) 2 (#P.parts - 1) * 2
Tactic: have : (2 : ℝ) ^ #P.parts = ↑2 ^ (#P.parts - 1) * 2 := by
        rw [← _root_.pow_succ, tsub_add_cancel_of_le (succ_le_iff.2 hP₁)]
-- 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
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
hP₁ : 0 < #P.parts
this_1 : HPow.hPow (α := ℝ) 2 #P.parts * (↑m : ℝ) / ((↑(#U) : ℝ) * ε) ≤ ε / 10
this : HPow.hPow (α := ℝ) 2 #P.parts = HPow.hPow (α := ℝ) 2 (#P.parts - 1) * 2
⊢ HPow.hPow (α := ℝ) 2 (#P.parts - 1) * (↑m : ℝ) ≤
    HPow.hPow (α := ℝ) 2 #P.parts * (↑m : ℝ) / ((↑(#U) : ℝ) * ε) * (↑(#(G.nonuniformWitness ε U V)) : ℝ)
have rw : HPow.hPow (α := ℝ) 2 (#P.parts - 1) * (↑m : ℝ) * ((↑(#U) : ℝ) * ε) ≤
  HPow.hPow (α := ℝ) 2 (#P.parts - 1) * (↑m : ℝ) * HMul.hMul (α := ℝ) 2 (↑(#(G.nonuniformWitness ε U V)) : ℝ)
Tactic: rw [← mul_div_right_comm, this, mul_right_comm _ (2 : ℝ), mul_assoc, le_div_iff₀]
-- 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
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
hP₁ : 0 < #P.parts
this_1 : HPow.hPow (α := ℝ) 2 #P.parts * (↑m : ℝ) / ((↑(#U) : ℝ) * ε) ≤ ε / 10
this : HPow.hPow (α := ℝ) 2 #P.parts = HPow.hPow (α := ℝ) 2 (#P.parts - 1) * 2
rw :
  HPow.hPow (α := ℝ) 2 (#P.parts - 1) * (↑m : ℝ) * ((↑(#U) : ℝ) * ε) ≤
    HPow.hPow (α := ℝ) 2 (#P.parts - 1) * (↑m : ℝ) * HMul.hMul (α := ℝ) 2 (↑(#(G.nonuniformWitness ε U V)) : ℝ)
⊢ HPow.hPow (α := ℝ) 2 (#P.parts - 1) * (↑m : ℝ) ≤
    HPow.hPow (α := ℝ) 2 #P.parts * (↑m : ℝ) / ((↑(#U) : ℝ) * ε) * (↑(#(G.nonuniformWitness ε U V)) : ℝ)
have rw₁ : 0 < (↑(#U) : ℝ) * ε
Tactic: rw [← mul_div_right_comm, this, mul_right_comm _ (2 : ℝ), mul_assoc, le_div_iff₀]
-- 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
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
hP₁ : 0 < #P.parts
this_1 : HPow.hPow (α := ℝ) 2 #P.parts * (↑m : ℝ) / ((↑(#U) : ℝ) * ε) ≤ ε / 10
this : HPow.hPow (α := ℝ) 2 #P.parts = HPow.hPow (α := ℝ) 2 (#P.parts - 1) * 2
⊢ HPow.hPow (α := ℝ) 2 (#P.parts - 1) * (↑m : ℝ) * ((↑(#U) : ℝ) * ε) ≤
    HPow.hPow (α := ℝ) 2 (#P.parts - 1) * (↑m : ℝ) * HMul.hMul (α := ℝ) 2 (↑(#(G.nonuniformWitness ε U V)) : ℝ)
have hbc : (↑(#U) : ℝ) * ε ≤ HMul.hMul (α := ℝ) 2 (↑(#(G.nonuniformWitness ε U V)) : ℝ)
Tactic: gcongr _ * ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (hypothesis)
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
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
hP₁ : 0 < #P.parts
this_1 : HPow.hPow (α := ℝ) 2 #P.parts * (↑m : ℝ) / ((↑(#U) : ℝ) * ε) ≤ ε / 10
this : HPow.hPow (α := ℝ) 2 #P.parts = HPow.hPow (α := ℝ) 2 (#P.parts - 1) * 2
⊢ 0 < (↑(#U) : ℝ) * ε
have this₁ : 0 < #U
Tactic: have := Finset.card_pos.mpr (P.nonempty_of_mem_parts hU)
-- 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
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
hP₁ : 0 < #P.parts
this_1 : HPow.hPow (α := ℝ) 2 #P.parts * (↑m : ℝ) / ((↑(#U) : ℝ) * ε) ≤ ε / 10
this_2 : HPow.hPow (α := ℝ) 2 #P.parts = HPow.hPow (α := ℝ) 2 (#P.parts - 1) * 2
this : 0 < #U
⊢ 0 < (↑(#U) : ℝ) * ε
have sz_positivity : 0 < ε → 0 < (↑(#U) : ℝ) * ε
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
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
hP₁ : 0 < #P.parts
this : HPow.hPow (α := ℝ) 2 #P.parts * (↑m : ℝ) / ((↑(#U) : ℝ) * ε) ≤ ε / 10
⊢ (↑(#(G.nonuniformWitness ε U V)) : ℝ) - HPow.hPow (α := ℝ) 2 (#P.parts - 1) * (↑m : ℝ) ≤
    (↑(#((star hP G ε hU V).biUnion id)) : ℝ)
have rw : (↑(#(G.nonuniformWitness ε U V \ (star hP G ε hU V).biUnion id)) : ℝ) ≤ HPow.hPow (α := ℝ) 2 (#P.parts - 1) * (↑m : ℝ)
Tactic: rw [sub_le_comm, ←
        cast_sub (card_le_card <| biUnion_star_subset_nonuniformWitness hP G ε hU V), ←
        card_sdiff_of_subset (biUnion_star_subset_nonuniformWitness hP G ε hU V)]
-- 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
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
hP₁ : 0 < #P.parts
this : HPow.hPow (α := ℝ) 2 #P.parts * (↑m : ℝ) / ((↑(#U) : ℝ) * ε) ≤ ε / 10
⊢ (1 - ε / 10) * (↑(#(G.nonuniformWitness ε U V)) : ℝ) ≤ (↑(#((star hP G ε hU V).biUnion id)) : ℝ)
have ε₁ : (1 - ε / 10) * (↑(#(G.nonuniformWitness ε U V)) : ℝ) ≤
  (1 - HPow.hPow (α := ℝ) 2 #P.parts * (↑m : ℝ) / ((↑(#U) : ℝ) * ε)) * (↑(#(G.nonuniformWitness ε U V)) : ℝ)
Tactic: calc
    (↑1 - ε / 10) * #(G.nonuniformWitness ε U V) ≤
        (↑1 - ↑2 ^ #P.parts * m / (#U * ε)) * #(G.nonuniformWitness ε U V) := by gcongr
    _ = #(G.nonuniformWitness ε U V) -
        ↑2 ^ #P.parts * m / (#U * ε) * #(G.nonuniformWitness ε U V) := by
      rw [sub_mul, one_mul]
    _ ≤ #(G.nonuniformWitness ε U V) - ↑2 ^ (#P.parts - 1) * m := by
      refine sub_le_sub_left ?_ _
      have : (2 : ℝ) ^ #P.parts = ↑2 ^ (#P.parts - 1) * 2 := by
        rw [← _root_.pow_succ, tsub_add_cancel_of_le (succ_le_iff.2 hP₁)]
      rw [← mul_div_right_comm, this, mul_right_comm _ (2 : ℝ), mul_assoc, le_div_iff₀]
      · gcongr _ * ?_
        exact (G.le_card_nonuniformWitness hunif).trans
          (le_mul_of_one_le_left (cast_nonneg _) one_le_two)
      have := Finset.card_pos.mpr (P.nonempty_of_mem_parts hU)
      sz_positivity
    _ ≤ #((star hP G ε hU V).biUnion id) := by
      rw [sub_le_comm, ←
        cast_sub (card_le_card <| biUnion_star_subset_nonuniformWitness hP G ε hU V), ←
        card_sdiff_of_subset (biUnion_star_subset_nonuniformWitness hP G ε hU V)]
      exact mod_cast card_nonuniformWitness_sdiff_biUnion_star hV hUV hunif
-- 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
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
hP₁ : 0 < #P.parts
this : HPow.hPow (α := ℝ) 2 #P.parts * (↑m : ℝ) / ((↑(#U) : ℝ) * ε) ≤ ε / 10
ε₁ :
  (1 - ε / 10) * (↑(#(G.nonuniformWitness ε U V)) : ℝ) ≤
    (1 - HPow.hPow (α := ℝ) 2 #P.parts * (↑m : ℝ) / ((↑(#U) : ℝ) * ε)) * (↑(#(G.nonuniformWitness ε U V)) : ℝ)
⊢ (1 - ε / 10) * (↑(#(G.nonuniformWitness ε U V)) : ℝ) ≤ (↑(#((star hP G ε hU V).biUnion id)) : ℝ)
have ε₂ : (1 - HPow.hPow (α := ℝ) 2 #P.parts * (↑m : ℝ) / ((↑(#U) : ℝ) * ε)) * (↑(#(G.nonuniformWitness ε U V)) : ℝ) =
  (↑(#(G.nonuniformWitness ε U V)) : ℝ) -
    HPow.hPow (α := ℝ) 2 #P.parts * (↑m : ℝ) / ((↑(#U) : ℝ) * ε) * (↑(#(G.nonuniformWitness ε U V)) : ℝ)
Tactic: calc
    (↑1 - ε / 10) * #(G.nonuniformWitness ε U V) ≤
        (↑1 - ↑2 ^ #P.parts * m / (#U * ε)) * #(G.nonuniformWitness ε U V) := by gcongr
    _ = #(G.nonuniformWitness ε U V) -
        ↑2 ^ #P.parts * m / (#U * ε) * #(G.nonuniformWitness ε U V) := by
      rw [sub_mul, one_mul]
    _ ≤ #(G.nonuniformWitness ε U V) - ↑2 ^ (#P.parts - 1) * m := by
      refine sub_le_sub_left ?_ _
      have : (2 : ℝ) ^ #P.parts = ↑2 ^ (#P.parts - 1) * 2 := by
        rw [← _root_.pow_succ, tsub_add_cancel_of_le (succ_le_iff.2 hP₁)]
      rw [← mul_div_right_comm, this, mul_right_comm _ (2 : ℝ), mul_assoc, le_div_iff₀]
      · gcongr _ * ?_
        exact (G.le_card_nonuniformWitness hunif).trans
          (le_mul_of_one_le_left (cast_nonneg _) one_le_two)
      have := Finset.card_pos.mpr (P.nonempty_of_mem_parts hU)
      sz_positivity
    _ ≤ #((star hP G ε hU V).biUnion id) := by
      rw [sub_le_comm, ←
        cast_sub (card_le_card <| biUnion_star_subset_nonuniformWitness hP G ε hU V), ←
        card_sdiff_of_subset (biUnion_star_subset_nonuniformWitness hP G ε hU V)]
      exact mod_cast card_nonuniformWitness_sdiff_biUnion_star hV hUV hunif
-- 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
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
hP₁ : 0 < #P.parts
this : HPow.hPow (α := ℝ) 2 #P.parts * (↑m : ℝ) / ((↑(#U) : ℝ) * ε) ≤ ε / 10
ε₁ :
  (1 - ε / 10) * (↑(#(G.nonuniformWitness ε U V)) : ℝ) ≤
    (1 - HPow.hPow (α := ℝ) 2 #P.parts * (↑m : ℝ) / ((↑(#U) : ℝ) * ε)) * (↑(#(G.nonuniformWitness ε U V)) : ℝ)
ε₂ :
  (1 - HPow.hPow (α := ℝ) 2 #P.parts * (↑m : ℝ) / ((↑(#U) : ℝ) * ε)) * (↑(#(G.nonuniformWitness ε U V)) : ℝ) =
    (↑(#(G.nonuniformWitness ε U V)) : ℝ) -
      HPow.hPow (α := ℝ) 2 #P.parts * (↑m : ℝ) / ((↑(#U) : ℝ) * ε) * (↑(#(G.nonuniformWitness ε U V)) : ℝ)
⊢ (1 - ε / 10) * (↑(#(G.nonuniformWitness ε U V)) : ℝ) ≤ (↑(#((star hP G ε hU V).biUnion id)) : ℝ)
have ε₃ : (↑(#(G.nonuniformWitness ε U V)) : ℝ) -
    HPow.hPow (α := ℝ) 2 #P.parts * (↑m : ℝ) / ((↑(#U) : ℝ) * ε) * (↑(#(G.nonuniformWitness ε U V)) : ℝ) ≤
  (↑(#(G.nonuniformWitness ε U V)) : ℝ) - HPow.hPow (α := ℝ) 2 (#P.parts - 1) * (↑m : ℝ)
Tactic: calc
    (↑1 - ε / 10) * #(G.nonuniformWitness ε U V) ≤
        (↑1 - ↑2 ^ #P.parts * m / (#U * ε)) * #(G.nonuniformWitness ε U V) := by gcongr
    _ = #(G.nonuniformWitness ε U V) -
        ↑2 ^ #P.parts * m / (#U * ε) * #(G.nonuniformWitness ε U V) := by
      rw [sub_mul, one_mul]
    _ ≤ #(G.nonuniformWitness ε U V) - ↑2 ^ (#P.parts - 1) * m := by
      refine sub_le_sub_left ?_ _
      have : (2 : ℝ) ^ #P.parts = ↑2 ^ (#P.parts - 1) * 2 := by
        rw [← _root_.pow_succ, tsub_add_cancel_of_le (succ_le_iff.2 hP₁)]
      rw [← mul_div_right_comm, this, mul_right_comm _ (2 : ℝ), mul_assoc, le_div_iff₀]
      · gcongr _ * ?_
        exact (G.le_card_nonuniformWitness hunif).trans
          (le_mul_of_one_le_left (cast_nonneg _) one_le_two)
      have := Finset.card_pos.mpr (P.nonempty_of_mem_parts hU)
      sz_positivity
    _ ≤ #((star hP G ε hU V).biUnion id) := by
      rw [sub_le_comm, ←
        cast_sub (card_le_card <| biUnion_star_subset_nonuniformWitness hP G ε hU V), ←
        card_sdiff_of_subset (biUnion_star_subset_nonuniformWitness hP G ε hU V)]
      exact mod_cast card_nonuniformWitness_sdiff_biUnion_star hV hUV hunif
-- 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
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
hP₁ : 0 < #P.parts
this : HPow.hPow (α := ℝ) 2 #P.parts * (↑m : ℝ) / ((↑(#U) : ℝ) * ε) ≤ ε / 10
ε₁ :
  (1 - ε / 10) * (↑(#(G.nonuniformWitness ε U V)) : ℝ) ≤
    (1 - HPow.hPow (α := ℝ) 2 #P.parts * (↑m : ℝ) / ((↑(#U) : ℝ) * ε)) * (↑(#(G.nonuniformWitness ε U V)) : ℝ)
ε₂ :
  (1 - HPow.hPow (α := ℝ) 2 #P.parts * (↑m : ℝ) / ((↑(#U) : ℝ) * ε)) * (↑(#(G.nonuniformWitness ε U V)) : ℝ) =
    (↑(#(G.nonuniformWitness ε U V)) : ℝ) -
      HPow.hPow (α := ℝ) 2 #P.parts * (↑m : ℝ) / ((↑(#U) : ℝ) * ε) * (↑(#(G.nonuniformWitness ε U V)) : ℝ)
ε₃ :
  (↑(#(G.nonuniformWitness ε U V)) : ℝ) -
      HPow.hPow (α := ℝ) 2 #P.parts * (↑m : ℝ) / ((↑(#U) : ℝ) * ε) * (↑(#(G.nonuniformWitness ε U V)) : ℝ) ≤
    (↑(#(G.nonuniformWitness ε U V)) : ℝ) - HPow.hPow (α := ℝ) 2 (#P.parts - 1) * (↑m : ℝ)
⊢ (1 - ε / 10) * (↑(#(G.nonuniformWitness ε U V)) : ℝ) ≤ (↑(#((star hP G ε hU V).biUnion id)) : ℝ)
have ε₄ : (↑(#(G.nonuniformWitness ε U V)) : ℝ) - HPow.hPow (α := ℝ) 2 (#P.parts - 1) * (↑m : ℝ) ≤
  (↑(#((star hP G ε hU V).biUnion id)) : ℝ)
Tactic: calc
    (↑1 - ε / 10) * #(G.nonuniformWitness ε U V) ≤
        (↑1 - ↑2 ^ #P.parts * m / (#U * ε)) * #(G.nonuniformWitness ε U V) := by gcongr
    _ = #(G.nonuniformWitness ε U V) -
        ↑2 ^ #P.parts * m / (#U * ε) * #(G.nonuniformWitness ε U V) := by
      rw [sub_mul, one_mul]
    _ ≤ #(G.nonuniformWitness ε U V) - ↑2 ^ (#P.parts - 1) * m := by
      refine sub_le_sub_left ?_ _
      have : (2 : ℝ) ^ #P.parts = ↑2 ^ (#P.parts - 1) * 2 := by
        rw [← _root_.pow_succ, tsub_add_cancel_of_le (succ_le_iff.2 hP₁)]
      rw [← mul_div_right_comm, this, mul_right_comm _ (2 : ℝ), mul_assoc, le_div_iff₀]
      · gcongr _ * ?_
        exact (G.le_card_nonuniformWitness hunif).trans
          (le_mul_of_one_le_left (cast_nonneg _) one_le_two)
      have := Finset.card_pos.mpr (P.nonempty_of_mem_parts hU)
      sz_positivity
    _ ≤ #((star hP G ε hU V).biUnion id) := by
      rw [sub_le_comm, ←
        cast_sub (card_le_card <| biUnion_star_subset_nonuniformWitness hP G ε hU V), ←
        card_sdiff_of_subset (biUnion_star_subset_nonuniformWitness hP G ε hU V)]
      exact mod_cast card_nonuniformWitness_sdiff_biUnion_star hV hUV hunif
-- 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
hm : m ≠ 0
⊢ Finset.card.{u_1} (α := Finset α)
      (parts (a := U)
        (if hUcard :
            #U =
              m * HPow.hPow (α := ℕ) 4 #P.parts + (Fintype.card α / #P.parts - m * HPow.hPow (α := ℕ) 4 #P.parts) then
          equitabilise (P := atomise U (P.nonuniformWitnesses G ε U)) ⋯
        else equitabilise (P := atomise U (P.nonuniformWitnesses G ε U)) ⋯)) =
    HPow.hPow (α := ℕ) 4 #P.parts
have pos : ∀ (h : #U = m * HPow.hPow (α := ℕ) 4 #P.parts + (Fintype.card α / #P.parts - m * HPow.hPow (α := ℕ) 4 #P.parts)),
  #(parts (equitabilise (P := atomise U (P.nonuniformWitnesses G ε U)) sorry)) = HPow.hPow (α := ℕ) 4 #P.parts
Tactic: split_ifs
-- 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
hm : m ≠ 0
pos :
  ∀ (h : #U = m * HPow.hPow (α := ℕ) 4 #P.parts + (Fintype.card α / #P.parts - m * HPow.hPow (α := ℕ) 4 #P.parts)),
    #(parts (equitabilise (P := atomise U (P.nonuniformWitnesses G ε U)) ⋯)) = HPow.hPow (α := ℕ) 4 #P.parts
⊢ Finset.card.{u_1} (α := Finset α)
      (parts (a := U)
        (if hUcard :
            #U =
              m * HPow.hPow (α := ℕ) 4 #P.parts + (Fintype.card α / #P.parts - m * HPow.hPow (α := ℕ) 4 #P.parts) then
          equitabilise (P := atomise U (P.nonuniformWitnesses G ε U)) ⋯
        else equitabilise (P := atomise U (P.nonuniformWitnesses G ε U)) ⋯)) =
    HPow.hPow (α := ℕ) 4 #P.parts
have neg : ∀ (h : ¬#U = m * HPow.hPow (α := ℕ) 4 #P.parts + (Fintype.card α / #P.parts - m * HPow.hPow (α := ℕ) 4 #P.parts)),
  #(parts (equitabilise (P := atomise U (P.nonuniformWitnesses G ε U)) sorry)) = HPow.hPow (α := ℕ) 4 #P.parts
Tactic: split_ifs
-- 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
hm : m ≠ 0
h : #U = m * HPow.hPow (α := ℕ) 4 #P.parts + (Fintype.card α / #P.parts - m * HPow.hPow (α := ℕ) 4 #P.parts)
⊢ #(parts (equitabilise (P := atomise U (P.nonuniformWitnesses G ε U)) ⋯)) = HPow.hPow (α := ℕ) 4 #P.parts
have pos : Fintype.card α / #P.parts - m * HPow.hPow (α := ℕ) 4 #P.parts ≤ HPow.hPow (α := ℕ) 4 #P.parts
Tactic: rw [card_parts_equitabilise _ _ hm, tsub_add_cancel_of_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
hm : m ≠ 0
h : ¬#U = m * HPow.hPow (α := ℕ) 4 #P.parts + (Fintype.card α / #P.parts - m * HPow.hPow (α := ℕ) 4 #P.parts)
⊢ #(parts (equitabilise (P := atomise U (P.nonuniformWitnesses G ε U)) ⋯)) = HPow.hPow (α := ℕ) 4 #P.parts
have neg : HPow.hPow (α := ℕ) 4 #P.parts - (Fintype.card α / #P.parts - m * HPow.hPow (α := ℕ) 4 #P.parts + 1) +
    (Fintype.card α / #P.parts - m * HPow.hPow (α := ℕ) 4 #P.parts + 1) =
  HPow.hPow (α := ℕ) 4 #P.parts
Tactic: rw [card_parts_equitabilise _ _ hm, tsub_add_cancel_of_le a_add_one_le_four_pow_parts_card]
-- 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
hm : m ≠ 0
h : ¬#U = m * HPow.hPow (α := ℕ) 4 #P.parts + (Fintype.card α / #P.parts - m * HPow.hPow (α := ℕ) 4 #P.parts)
neg :
  HPow.hPow (α := ℕ) 4 #P.parts - (Fintype.card α / #P.parts - m * HPow.hPow (α := ℕ) 4 #P.parts + 1) +
      (Fintype.card α / #P.parts - m * HPow.hPow (α := ℕ) 4 #P.parts + 1) =
    HPow.hPow (α := ℕ) 4 #P.parts
⊢ #(parts (equitabilise (P := atomise U (P.nonuniformWitnesses G ε U)) ⋯)) = HPow.hPow (α := ℕ) 4 #P.parts
have neg₁ : HPow.hPow (α := ℕ) 4 #P.parts = HPow.hPow (α := ℕ) 4 #P.parts
Tactic: rw [card_parts_equitabilise _ _ hm, tsub_add_cancel_of_le a_add_one_le_four_pow_parts_card]
-- 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
s : Finset α
hs :
  Membership.mem (γ := Finset (Finset α))
    (parts (a := U)
      (if hUcard :
          #U = m * HPow.hPow (α := ℕ) 4 #P.parts + (Fintype.card α / #P.parts - m * HPow.hPow (α := ℕ) 4 #P.parts) then
        equitabilise (P := atomise U (P.nonuniformWitnesses G ε U)) ⋯
      else equitabilise (P := atomise U (P.nonuniformWitnesses G ε U)) ⋯))
    s
⊢ #s = m ∨ #s = m + 1
have pos : ∀ (h : #U = m * HPow.hPow (α := ℕ) 4 #P.parts + (Fintype.card α / #P.parts - m * HPow.hPow (α := ℕ) 4 #P.parts))
  (hs : s ∈ parts (equitabilise (P := atomise U (P.nonuniformWitnesses G ε U)) sorry)), #s = m ∨ #s = m + 1
Tactic: split_ifs at hs
Cleared hypotheses: hs
-- 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
s : Finset α
hs :
  Membership.mem (γ := Finset (Finset α))
    (parts (a := U)
      (if hUcard :
          #U = m * HPow.hPow (α := ℕ) 4 #P.parts + (Fintype.card α / #P.parts - m * HPow.hPow (α := ℕ) 4 #P.parts) then
        equitabilise (P := atomise U (P.nonuniformWitnesses G ε U)) ⋯
      else equitabilise (P := atomise U (P.nonuniformWitnesses G ε U)) ⋯))
    s
pos :
  ∀ (h : #U = m * HPow.hPow (α := ℕ) 4 #P.parts + (Fintype.card α / #P.parts - m * HPow.hPow (α := ℕ) 4 #P.parts))
    (hs : s ∈ parts (equitabilise (P := atomise U (P.nonuniformWitnesses G ε U)) ⋯)), #s = m ∨ #s = m + 1
⊢ #s = m ∨ #s = m + 1
have neg : ∀ (h : ¬#U = m * HPow.hPow (α := ℕ) 4 #P.parts + (Fintype.card α / #P.parts - m * HPow.hPow (α := ℕ) 4 #P.parts))
  (hs : s ∈ parts (equitabilise (P := atomise U (P.nonuniformWitnesses G ε U)) sorry)), #s = m ∨ #s = m + 1
Tactic: split_ifs at hs
Cleared hypotheses: hs
-- 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 (α := ℝ) (↑(#𝒜) : ℝ) (↑(#s) : ℝ) * ((↑m : ℝ) / HAdd.hAdd (α := ℝ) (↑m : ℝ) 1) ≤ (↑(#(𝒜.sup id)) : ℝ)
have rw : HMul.hMul (α := ℝ) (↑(#𝒜) : ℝ) (↑m : ℝ) * (↑(#s) : ℝ) ≤ (↑(#(𝒜.sup id)) : ℝ) * HAdd.hAdd (α := ℝ) (↑m : ℝ) 1
Tactic: rw [mul_div_assoc', div_le_iff₀ coe_m_add_one_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 α
h𝒜 : 𝒜 ⊆ (chunk hP G ε hU).parts
hs : s ∈ 𝒜
⊢ HMul.hMul (α := ℝ) (↑(#𝒜) : ℝ) (↑m : ℝ) * (↑(#s) : ℝ) ≤ (↑(#(𝒜.sup id)) : ℝ) * HAdd.hAdd (α := ℝ) (↑m : ℝ) 1
have h₁ : HMul.hMul (α := ℝ) (↑(#𝒜) : ℝ) (↑m : ℝ) ≤ (↑(#(𝒜.sup id)) : ℝ)
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 α
h𝒜 : 𝒜 ⊆ (chunk hP G ε hU).parts
hs : s ∈ 𝒜
h₁ : HMul.hMul (α := ℝ) (↑(#𝒜) : ℝ) (↑m : ℝ) ≤ (↑(#(𝒜.sup id)) : ℝ)
⊢ HMul.hMul (α := ℝ) (↑(#𝒜) : ℝ) (↑m : ℝ) * (↑(#s) : ℝ) ≤ (↑(#(𝒜.sup id)) : ℝ) * HAdd.hAdd (α := ℝ) (↑m : ℝ) 1
have h₂ : (↑(#s) : ℝ) ≤ HAdd.hAdd (α := ℝ) (↑m : ℝ) 1
Tactic: gcongr