-- 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:
α : 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)
              (if hUcard : #U = m * 4 ^ #P.parts + (Fintype.card α / #P.parts - m * 4 ^ #P.parts) then equitabilise ⋯
                else equitabilise ⋯).parts).biUnion
          id) ≤
    m

Tactic:
split_ifs with h₁

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

case neg
α : 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

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
⊢ ∑ 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) ≤
    ∑ B ∈ filter (fun B => B ⊆ G.nonuniformWitness ε U V ∧ B.Nonempty) (atomise U (P.nonuniformWitnesses G ε U)).parts,
      m

Tactic:
suffices ∀ B ∈ (atomise U <| P.nonuniformWitnesses G ε U).parts,
    #(B \ {A ∈ (chunk hP G ε hU).parts | A ⊆ B}.biUnion id) ≤ m by
  exact sum_le_sum fun B hB => this B <| filter_subset _ _ 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 ∈ (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
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

Tactic:
unfold chunk

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)
              (if hUcard : #U = m * 4 ^ #P.parts + (Fintype.card α / #P.parts - m * 4 ^ #P.parts) then equitabilise ⋯
                else equitabilise ⋯).parts).biUnion
          id) ≤
    m