-- Mathlib/Combinatorics/SimpleGraph/Regularity/Chunk.lean
theorem card_nonuniformWitness_sdiff_biUnion_star (hV : V ∈ P.parts) (hUV : U ≠ V)
    (h₂ : ¬G.IsUniform ε U V) :
    #(G.nonuniformWitness ε U V \ (star hP G ε hU V).biUnion id) ≤ 2 ^ (#P.parts - 1) * m

Proof state:
case pos
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
h₂ : ¬G.IsUniform ε U V
hX : G.nonuniformWitness ε U V ∈ P.nonuniformWitnesses G ε U
q :
  G.nonuniformWitness ε U V \ (star hP G ε hU V).biUnion id ⊆
    (filter (fun B => B ⊆ G.nonuniformWitness ε U V ∧ B.Nonempty)
          (atomise U (P.nonuniformWitnesses G ε U)).parts).biUnion
      fun B => B \ (filter (fun A => A ⊆ B) (chunk hP G ε hU).parts).biUnion id
B : Finset α
hB : B ∈ (atomise U (P.nonuniformWitnesses G ε U)).parts
h₁ : #U = m * 4 ^ #P.parts + (Fintype.card α / #P.parts - m * 4 ^ #P.parts)
⊢ #(B \ (filter (fun A => A ⊆ B) (equitabilise ⋯).parts).biUnion id) ≤ m

Tactic:
convert card_parts_equitabilise_subset_le _ (card_aux₁ h₁) hB

Result:
no goals

Proof state:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
h₂ : ¬G.IsUniform ε U V
hX : G.nonuniformWitness ε U V ∈ P.nonuniformWitnesses G ε U
q :
  G.nonuniformWitness ε U V \ (star hP G ε hU V).biUnion id ⊆
    (filter (fun B => B ⊆ G.nonuniformWitness ε U V ∧ B.Nonempty)
          (atomise U (P.nonuniformWitnesses G ε U)).parts).biUnion
      fun B => B \ (filter (fun A => A ⊆ B) (chunk hP G ε hU).parts).biUnion id
⊢ ∀ B ∈ (atomise U (P.nonuniformWitnesses G ε U)).parts,
    #(B \ (filter (fun A => A ⊆ B) (chunk hP G ε hU).parts).biUnion id) ≤ m

Tactic:
intro B hB

Result:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
h₂ : ¬G.IsUniform ε U V
hX : G.nonuniformWitness ε U V ∈ P.nonuniformWitnesses G ε U
q :
  G.nonuniformWitness ε U V \ (star hP G ε hU V).biUnion id ⊆
    (filter (fun B => B ⊆ G.nonuniformWitness ε U V ∧ B.Nonempty)
          (atomise U (P.nonuniformWitnesses G ε U)).parts).biUnion
      fun B => B \ (filter (fun A => A ⊆ B) (chunk hP G ε hU).parts).biUnion id
B : Finset α
hB : B ∈ (atomise U (P.nonuniformWitnesses G ε U)).parts
⊢ #(B \ (filter (fun A => A ⊆ B) (chunk hP G ε hU).parts).biUnion id) ≤ m

Proof state:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
h₂ : ¬G.IsUniform ε U V
hX : G.nonuniformWitness ε U V ∈ P.nonuniformWitnesses G ε U
q :
  G.nonuniformWitness ε U V \ (star hP G ε hU V).biUnion id ⊆
    (filter (fun B => B ⊆ G.nonuniformWitness ε U V ∧ B.Nonempty)
          (atomise U (P.nonuniformWitnesses G ε U)).parts).biUnion
      fun B => B \ (filter (fun A => A ⊆ B) (chunk hP G ε hU).parts).biUnion id
⊢ #(G.nonuniformWitness ε U V \ (star hP G ε hU V).biUnion id) ≤ 2 ^ (#P.parts - 1) * m

Tactic:
apply (card_le_card q).trans (card_biUnion_le.trans _)

Result:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
h₂ : ¬G.IsUniform ε U V
hX : G.nonuniformWitness ε U V ∈ P.nonuniformWitnesses G ε U
q :
  G.nonuniformWitness ε U V \ (star hP G ε hU V).biUnion id ⊆
    (filter (fun B => B ⊆ G.nonuniformWitness ε U V ∧ B.Nonempty)
          (atomise U (P.nonuniformWitnesses G ε U)).parts).biUnion
      fun B => B \ (filter (fun A => A ⊆ B) (chunk hP G ε hU).parts).biUnion id
⊢ ∑ a ∈ filter (fun B => B ⊆ G.nonuniformWitness ε U V ∧ B.Nonempty) (atomise U (P.nonuniformWitnesses G ε U)).parts,
      #(a \ (filter (fun A => A ⊆ a) (chunk hP G ε hU).parts).biUnion id) ≤
    2 ^ (#P.parts - 1) * m

Proof state:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
h₂ : ¬G.IsUniform ε U V
hX : G.nonuniformWitness ε U V ∈ P.nonuniformWitnesses G ε U
x : α
hx :
  (∃ a, (a ∈ (atomise U (P.nonuniformWitnesses G ε U)).parts ∧ a ⊆ G.nonuniformWitness ε U V ∧ a.Nonempty) ∧ x ∈ a) ∧
    ∀ x_1 ∈ (chunk hP G ε hU).parts, x_1 ⊆ G.nonuniformWitness ε U V → x ∉ x_1
⊢ ∃ a,
    (a ∈ (atomise U (P.nonuniformWitnesses G ε U)).parts ∧ a ⊆ G.nonuniformWitness ε U V ∧ a.Nonempty) ∧
      x ∈ a ∧ ∀ x_1 ∈ (chunk hP G ε hU).parts, x_1 ⊆ a → x ∉ x_1

Tactic:
obtain ⟨⟨B, hB₁, hB₂⟩, hx⟩ := hx

Result:
case intro.intro.intro
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
h₂ : ¬G.IsUniform ε U V
hX : G.nonuniformWitness ε U V ∈ P.nonuniformWitnesses G ε U
x : α
hx : ∀ x_1 ∈ (chunk hP G ε hU).parts, x_1 ⊆ G.nonuniformWitness ε U V → x ∉ x_1
B : Finset α
hB₁ : B ∈ (atomise U (P.nonuniformWitnesses G ε U)).parts ∧ B ⊆ G.nonuniformWitness ε U V ∧ B.Nonempty
hB₂ : x ∈ B
⊢ ∃ a,
    (a ∈ (atomise U (P.nonuniformWitnesses G ε U)).parts ∧ a ⊆ G.nonuniformWitness ε U V ∧ a.Nonempty) ∧
      x ∈ a ∧ ∀ x_1 ∈ (chunk hP G ε hU).parts, x_1 ⊆ a → x ∉ x_1