-- 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
x : α
hx :
  (∃ a ∈ filter (fun u => u ⊆ G.nonuniformWitness ε U V ∧ u.Nonempty) (atomise U (P.nonuniformWitnesses G ε U)).parts,
      x ∈ id a) ∧
    x ∉ (filter (fun A => A ⊆ G.nonuniformWitness ε U V) (chunk hP G ε hU).parts).biUnion id
⊢ x ∈
    (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

Tactic:
simp only [not_exists, mem_biUnion, and_imp, exists_prop, mem_filter,
  not_and, mem_sdiff, id, mem_sdiff] at hx ⊢

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

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 : x ∈ G.nonuniformWitness ε U V \ (star hP G ε hU V).biUnion id
⊢ x ∈
    (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

Tactic:
rw [← biUnion_filter_atomise hX (G.nonuniformWitness_subset h₂), star, mem_sdiff,
  mem_biUnion] at hx

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
x : α
hx :
  (∃ a ∈ filter (fun u => u ⊆ G.nonuniformWitness ε U V ∧ u.Nonempty) (atomise U (P.nonuniformWitnesses G ε U)).parts,
      x ∈ id a) ∧
    x ∉ (filter (fun A => A ⊆ G.nonuniformWitness ε U V) (chunk hP G ε hU).parts).biUnion id
⊢ x ∈
    (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

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

Tactic:
rw [sum_const]

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
⊢ #(filter (fun B => B ⊆ G.nonuniformWitness ε U V ∧ B.Nonempty) (atomise U (P.nonuniformWitnesses G ε U)).parts) • m ≤
    2 ^ (#P.parts - 1) * m

Proof state:
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

Tactic:
exact ⟨B, hB₁, hB₂, fun A hA AB => hx A hA <| AB.trans hB₁.2.1⟩

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

Tactic:
intro x hx

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
x : α
hx : x ∈ G.nonuniformWitness ε U V \ (star hP G ε hU V).biUnion id
⊢ x ∈
    (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