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
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

Tactic:
have := Finset.card_pos.mpr (P.nonempty_of_mem_parts hU)
-- 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
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
sz_positivity sz_positivity₁ sz_positivity₂ sz_positivity₃ : 0 < ε → 0 < (↑(#U) : ℝ) * ε
⊢ 0 < (↑(#U) : ℝ) * ε

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 : 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
rw :
  (↑(#(G.nonuniformWitness ε U V \ (star hP G ε hU V).biUnion id)) : ℝ) ≤ HPow.hPow (α := ℝ) 2 (#P.parts - 1) * (↑m : ℝ)
⊢ (↑(#(G.nonuniformWitness ε U V)) : ℝ) - HPow.hPow (α := ℝ) 2 (#P.parts - 1) * (↑m : ℝ) ≤
    (↑(#((star hP G ε hU V).biUnion id)) : ℝ)

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)]

Premises used: Nat.cast_sub, Finset.card_le_card, Finset.card_sdiff_of_subset, SzemerediRegularity.biUnion_star_subset_nonuniformWitness, sub_le_comm
-- 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
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 \ (star hP G ε hU V).biUnion id)) : ℝ) ≤ HPow.hPow (α := ℝ) 2 (#P.parts - 1) * (↑m : ℝ)

Tactic:
mod_cast card_nonuniformWitness_sdiff_biUnion_star hV hUV hunif

Premises used: Nat.cast_mul._simp_1, SzemerediRegularity.stepBound, HMul.hMul, congrArg, HSub.hSub, cast, Fintype.card, id, HDiv.hDiv, Nat.cast_le._simp_1, LE.le, SzemerediRegularity.star, Finset.biUnion, Finpartition.parts, Nat.cast, SDiff.sdiff, HPow.hPow, _private.0.SzemerediRegularity.card_nonuniformWitness_sdiff_biUnion_star, Finset.card, congrFun', SimpleGraph.nonuniformWitness, OfNat.ofNat, Eq.symm, Eq.trans, Nat.cast_pow._simp_1
-- 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
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 \ (star hP G ε hU V).biUnion id)) : ℝ) ≤ HPow.hPow (α := ℝ) 2 (#P.parts - 1) * (↑m : ℝ)

Tactic:
exact mod_cast card_nonuniformWitness_sdiff_biUnion_star hV hUV hunif

Premises used: _private.0.SzemerediRegularity.card_nonuniformWitness_sdiff_biUnion_star
-- 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
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 : ℝ)
ε₄ :
  (↑(#(G.nonuniformWitness ε U V)) : ℝ) - HPow.hPow (α := ℝ) 2 (#P.parts - 1) * (↑m : ℝ) ≤
    (↑(#((star hP G ε hU V).biUnion id)) : ℝ)
⊢ (1 - ε / 10) * (↑(#(G.nonuniformWitness ε U V)) : ℝ) ≤ (↑(#((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

Premises used: HMul.hMul, HSub.hSub, id, HDiv.hDiv, SzemerediRegularity.star, Finset.biUnion, Finpartition.parts, Nat.cast, Finset.card, SimpleGraph.nonuniformWitness, 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 : 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
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)) ⋯)) = 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

Tactic:
split_ifs
-- 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
hm : m ≠ 0
h : #U = m * HPow.hPow (α := ℕ) 4 #P.parts + (Fintype.card α / #P.parts - m * HPow.hPow (α := ℕ) 4 #P.parts)
pos : Fintype.card α / #P.parts - m * HPow.hPow (α := ℕ) 4 #P.parts ≤ HPow.hPow (α := ℕ) 4 #P.parts
⊢ #(parts (equitabilise (P := atomise U (P.nonuniformWitnesses G ε U)) ⋯)) = HPow.hPow (α := ℕ) 4 #P.parts

Tactic:
rw [card_parts_equitabilise _ _ hm, tsub_add_cancel_of_le]

Premises used: tsub_add_cancel_of_le, Finpartition.card_parts_equitabilise
-- 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
hm : m ≠ 0
h : #U = m * HPow.hPow (α := ℕ) 4 #P.parts + (Fintype.card α / #P.parts - m * HPow.hPow (α := ℕ) 4 #P.parts)
⊢ Fintype.card α / #P.parts - m * HPow.hPow (α := ℕ) 4 #P.parts ≤ HPow.hPow (α := ℕ) 4 #P.parts

Tactic:
le_of_lt a_add_one_le_four_pow_parts_card

Premises used: SzemerediRegularity.a_add_one_le_four_pow_parts_card, le_of_lt
-- 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
hm : m ≠ 0
h : #U = m * HPow.hPow (α := ℕ) 4 #P.parts + (Fintype.card α / #P.parts - m * HPow.hPow (α := ℕ) 4 #P.parts)
⊢ Fintype.card α / #P.parts - m * HPow.hPow (α := ℕ) 4 #P.parts ≤ HPow.hPow (α := ℕ) 4 #P.parts

Tactic:
exact le_of_lt a_add_one_le_four_pow_parts_card

Premises used: le_of_lt
-- 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
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
neg₁ neg₂ : HPow.hPow (α := ℕ) 4 #P.parts = HPow.hPow (α := ℕ) 4 #P.parts
⊢ #(parts (equitabilise (P := atomise U (P.nonuniformWitnesses G ε U)) ⋯)) = HPow.hPow (α := ℕ) 4 #P.parts

Tactic:
rw [card_parts_equitabilise _ _ hm, tsub_add_cancel_of_le a_add_one_le_four_pow_parts_card]

Premises used: SzemerediRegularity.a_add_one_le_four_pow_parts_card, tsub_add_cancel_of_le, Finpartition.card_parts_equitabilise
-- 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
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
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)) ⋯)), #s = m ∨ #s = m + 1
⊢ #s = m ∨ #s = m + 1

Tactic:
split_ifs at hs
-- 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
s : Finset α
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

Tactic:
card_eq_of_mem_parts_equitabilise hs

Premises used: Finpartition.card_eq_of_mem_parts_equitabilise
-- 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
s : Finset α
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

Tactic:
exact card_eq_of_mem_parts_equitabilise hs

Premises used: Finpartition.card_eq_of_mem_parts_equitabilise
-- 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
s : Finset α
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

Tactic:
card_eq_of_mem_parts_equitabilise hs

Premises used: Finpartition.card_eq_of_mem_parts_equitabilise
-- 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
s : Finset α
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

Tactic:
exact card_eq_of_mem_parts_equitabilise hs

Premises used: Finpartition.card_eq_of_mem_parts_equitabilise
-- 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
s : Finset α
hs : s ∈ (chunk hP G ε hU).parts
i : #s = m + 1
⊢ m ≤ #s

Tactic:
simp [i]
-- 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
s : Finset α
hs : s ∈ (chunk hP G ε hU).parts
i : #s = m
⊢ #s ≤ m + 1

Tactic:
simp [i]
-- 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
V : Finset α
⊢ (↑(#((star hP G ε hU V).biUnion id)) : ℝ) ≤
    (↑(#(star hP G ε hU V)) : ℝ) * HAdd.hAdd (α := ℝ) (↑(Fintype.card α / stepBound #P.parts) : ℝ) 1

Tactic:
mod_cast card_biUnion_le_card_mul _ _ _ fun _ hs =>
    card_le_m_add_one_of_mem_chunk_parts <| star_subset_chunk hs

Premises used: Nat.cast_mul._simp_1, SzemerediRegularity.stepBound, HMul.hMul, congrArg, Nat.cast_add._simp_1, cast, Fintype.card, id, HDiv.hDiv, SzemerediRegularity.card_le_m_add_one_of_mem_chunk_parts, SzemerediRegularity.star_subset_chunk, Nat.cast_le._simp_1, LE.le, SzemerediRegularity.star, Finset.biUnion, Finpartition.parts, Nat.cast, HAdd.hAdd, Finset.card_biUnion_le_card_mul, Finset.card, OfNat.ofNat, 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 : Finset α
hU : U ∈ P.parts
𝒜 : Finset (Finset α)
s : Finset α
h𝒜 : 𝒜 ⊆ (chunk hP G ε hU).parts
hs : s ∈ 𝒜
rw : HMul.hMul (α := ℝ) (↑(#𝒜) : ℝ) (↑m : ℝ) * (↑(#s) : ℝ) ≤ (↑(#(𝒜.sup id)) : ℝ) * HAdd.hAdd (α := ℝ) (↑m : ℝ) 1
⊢ HMul.hMul (α := ℝ) (↑(#𝒜) : ℝ) (↑(#s) : ℝ) * ((↑m : ℝ) / HAdd.hAdd (α := ℝ) (↑m : ℝ) 1) ≤ (↑(#(𝒜.sup id)) : ℝ)

Tactic:
rw [mul_div_assoc', div_le_iff₀ coe_m_add_one_pos, mul_right_comm]

Premises used: div_le_iff₀, mul_div_assoc', mul_right_comm, SzemerediRegularity.coe_m_add_one_pos
-- 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 α
h𝒜 : 𝒜 ⊆ (chunk hP G ε hU).parts
hs : s ∈ 𝒜
h₁ : HMul.hMul (α := ℝ) (↑(#𝒜) : ℝ) (↑m : ℝ) ≤ (↑(#(𝒜.sup id)) : ℝ)
h₂ : (↑(#s) : ℝ) ≤ HAdd.hAdd (α := ℝ) (↑m : ℝ) 1
⊢ HMul.hMul (α := ℝ) (↑(#𝒜) : ℝ) (↑m : ℝ) * (↑(#s) : ℝ) ≤ (↑(#(𝒜.sup id)) : ℝ) * HAdd.hAdd (α := ℝ) (↑m : ℝ) 1

Tactic:
gcongr
-- 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 α
h𝒜 : 𝒜 ⊆ (chunk hP G ε hU).parts
hs : s ∈ 𝒜
h₁ : #𝒜 * m ≤ ∑ i ∈ 𝒜, #i
⊢ HMul.hMul (α := ℝ) (↑(#𝒜) : ℝ) (↑m : ℝ) ≤ (↑(#(𝒜.sup id)) : ℝ)

Tactic:
rw [← (ofSubset _ h𝒜 rfl).sum_card_parts, ofSubset_parts, ← cast_mul, cast_le]

Premises used: Finpartition.ofSubset_parts, Finpartition.ofSubset, Nat.cast_mul, Finpartition.sum_card_parts, Nat.cast_le, rfl
-- 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 α
h𝒜 : 𝒜 ⊆ (chunk hP G ε hU).parts
hs : s ∈ 𝒜
⊢ #𝒜 * m ≤ ∑ i ∈ 𝒜, #i

Tactic:
card_nsmul_le_sum _ _ _ fun x hx => m_le_card_of_mem_chunk_parts <| h𝒜 hx

Premises used: SzemerediRegularity.m_le_card_of_mem_chunk_parts, Finset.card_nsmul_le_sum
-- 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 α
h𝒜 : 𝒜 ⊆ (chunk hP G ε hU).parts
hs : s ∈ 𝒜
⊢ #𝒜 * m ≤ ∑ i ∈ 𝒜, #i

Tactic:
exact card_nsmul_le_sum _ _ _ fun x hx => m_le_card_of_mem_chunk_parts <| h𝒜 hx

Premises used: SzemerediRegularity.m_le_card_of_mem_chunk_parts, Finset.card_nsmul_le_sum
-- 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 α
h𝒜 : 𝒜 ⊆ (chunk hP G ε hU).parts
hs : s ∈ 𝒜
⊢ (↑(#s) : ℝ) ≤ HAdd.hAdd (α := ℝ) (↑m : ℝ) 1

Tactic:
mod_cast card_le_m_add_one_of_mem_chunk_parts (h𝒜 hs)

Premises used: SzemerediRegularity.stepBound, congrArg, Nat.cast_add._simp_1, cast, Fintype.card, HDiv.hDiv, SzemerediRegularity.card_le_m_add_one_of_mem_chunk_parts, Nat.cast_le._simp_1, LE.le, Finpartition.parts, Nat.cast, HAdd.hAdd, Finset.card, OfNat.ofNat, 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 : Finset α
hU : U ∈ P.parts
𝒜 : Finset (Finset α)
s : Finset α
h𝒜 : 𝒜 ⊆ (chunk hP G ε hU).parts
hs : s ∈ 𝒜
⊢ (↑(#s) : ℝ) ≤ HAdd.hAdd (α := ℝ) (↑m : ℝ) 1

Tactic:
exact mod_cast card_le_m_add_one_of_mem_chunk_parts (h𝒜 hs)

Premises used: SzemerediRegularity.card_le_m_add_one_of_mem_chunk_parts
-- 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 ∈ 𝒜
rw : HMul.hMul (α := ℝ) (↑(#(𝒜.biUnion id)) : ℝ) (↑m : ℝ) ≤ (↑(#𝒜) : ℝ) * HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 * (↑(#s) : ℝ)
⊢ (↑(#(𝒜.sup id)) : ℝ) ≤ HMul.hMul (α := ℝ) (↑(#𝒜) : ℝ) (↑(#s) : ℝ) * (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 / (↑m : ℝ))

Tactic:
rw [sup_eq_biUnion, mul_div_assoc', le_div_iff₀ m_pos, mul_right_comm]

Premises used: mul_div_assoc', Finset.sup_eq_biUnion, mul_right_comm, le_div_iff₀
-- 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 ∈ 𝒜
h₁ : (↑(#(𝒜.biUnion id)) : ℝ) ≤ (↑(#𝒜) : ℝ) * HAdd.hAdd (α := ℝ) (↑m : ℝ) 1
h₂ : m ≤ #s
⊢ HMul.hMul (α := ℝ) (↑(#(𝒜.biUnion id)) : ℝ) (↑m : ℝ) ≤ (↑(#𝒜) : ℝ) * HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 * (↑(#s) : ℝ)

Tactic:
gcongr
-- 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 ∈ 𝒜
h₁ : #(𝒜.biUnion id) ≤ #𝒜 * (m + 1)
⊢ (↑(#(𝒜.biUnion id)) : ℝ) ≤ (↑(#𝒜) : ℝ) * HAdd.hAdd (α := ℝ) (↑m : ℝ) 1

Tactic:
norm_cast
-- 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 ∈ 𝒜
⊢ #(𝒜.biUnion id) ≤ #𝒜 * (m + 1)

Tactic:
card_biUnion_le_card_mul _ _ _ fun x hx => ?_

Premises used: Finset.card_biUnion_le_card_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 : Finset α
hU : U ∈ P.parts
𝒜 : Finset (Finset α)
s : Finset α
m_pos : LT.lt (α := ℝ) 0 (↑m : ℝ)
h𝒜 : 𝒜 ⊆ (chunk hP G ε hU).parts
hs : s ∈ 𝒜
h₁ : ∀ (x : Finset α) (hx : x ∈ 𝒜), #(id x) ≤ m + 1
⊢ #(𝒜.biUnion id) ≤ #𝒜 * (m + 1)

Tactic:
refine card_biUnion_le_card_mul _ _ _ fun x hx => ?_

Premises used: Finset.card_biUnion_le_card_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 : Finset α
hU : U ∈ P.parts
𝒜 : Finset (Finset α)
s : Finset α
m_pos : LT.lt (α := ℝ) 0 (↑m : ℝ)
h𝒜 : 𝒜 ⊆ (chunk hP G ε hU).parts
hs : s ∈ 𝒜
x : Finset α
hx : x ∈ 𝒜
⊢ #(id x) ≤ m + 1

Tactic:
apply card_le_m_add_one_of_mem_chunk_parts (h𝒜 hx)

Premises used: SzemerediRegularity.card_le_m_add_one_of_mem_chunk_parts