awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.CWComplex.Classical.Finite
Goal:
X_1 : Type u_1
inst : TopologicalSpace X_1
C_1 D_1 : Set X_1
inst_1 : RelCWComplex C_1 D_1
X : Type u
inst_2 : TopologicalSpace X
C D : Set X
cell : (n : ℕ) → Type u
map : (n : ℕ) → (i : cell n) → PartialEquiv (Fin n → ℝ) X
finite_cell : ∀ (n : ℕ), _root_.Finite.{u + 1} (cell n)
source_eq : ∀ (n : ℕ) (i : cell n), (map n i).source = ball 0 1
continuousOn : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i) : (Fin n → ℝ) → X) (closedBall 0 1)
continuousOn_symm : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i).symm : X → Fin n → ℝ) (map n i).target
pairwiseDisjoint' :
  PairwiseDisjoint (α := Set X) univ fun (ni : (n : ℕ) × cell n) ↦
    (↑(map (ni.fst (β := fun (n : ℕ) ↦ cell n)) (ni.snd (β := fun (n : ℕ) ↦ cell n))) : (Fin ni.fst → ℝ) → X) ''
      ball 0 1
disjointBase' : ∀ (n : ℕ) (i : cell n), Disjoint ((↑(map n i) : (Fin n → ℝ) → X) '' ball 0 1) D
mapsTo :
  ∀ (n : ℕ) (i : cell n),
    MapsTo (↑(map n i) : (Fin n → ℝ) → X) (sphere 0 1)
      (D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ (j : cell m), (↑(map m j) : (Fin m → ℝ) → X) '' closedBall 0 1)
isClosedBase : IsClosed[inst_2] D
union' : D ∪ ⋃ (n : ℕ), ⋃ (j : cell n), (↑(map n j) : (Fin n → ℝ) → X) '' closedBall 0 1 = C
A : Set X
asubc : A ⊆ C
h :
  (∀ (n : ℕ) (j : cell n), IsClosed[inst_2] (A ∩ (↑(map n j) : (Fin n → ℝ) → X) '' closedBall 0 1)) ∧
    IsClosed[inst_2] (A ∩ D)
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → IsEmpty.{u + 1} (cell b)
this :
  IsClosed[inst_2]
    (A ∩
      (D ∪
        ⋃ (n : { n : ℕ // n < N }),
          ⋃ (j : cell (↑n : ℕ)), (↑(map (↑n : ℕ) j) : (Fin (↑n : ℕ) → ℝ) → X) '' closedBall 0 1))
n : ℕ
h₁ :
  ∀ (i : cell n),
    (↑(map n i) : (Fin n → ℝ) → X) '' closedBall 0 1 ⊆
      ⋃ (hx : n < N),
        ⋃ (j : cell (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < N) n hx) : ℕ)),
          (↑(map (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < N) n hx) : ℕ) j) : (Fin (↑⟨n, hx⟩ : ℕ) → ℝ) → X) ''
            closedBall 0 1
⊢ Subset.{u} (α := Set X) (⋃ (j : cell n), (↑(map n j) : (Fin n → ℝ) → X) '' closedBall 0 1)
    (⋃ (hx : n < N),
      ⋃ (j : cell (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < N) n hx) : ℕ)),
        (↑(map (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < N) n hx) : ℕ) j) : (Fin (↑⟨n, hx⟩ : ℕ) → ℝ) → X) '' closedBall 0 1)

Tactic:
apply iUnion_subset

Premises used: Set.iUnion_subset
-- Module: Mathlib.Topology.CWComplex.Classical.Finite
Goal:
X_1 : Type u_1
inst : TopologicalSpace X_1
C_1 D_1 : Set X_1
inst_1 : RelCWComplex C_1 D_1
X : Type u
inst_2 : TopologicalSpace X
C D : Set X
cell : (n : ℕ) → Type u
map : (n : ℕ) → (i : cell n) → PartialEquiv (Fin n → ℝ) X
finite_cell : ∀ (n : ℕ), _root_.Finite.{u + 1} (cell n)
source_eq : ∀ (n : ℕ) (i : cell n), (map n i).source = ball 0 1
continuousOn : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i) : (Fin n → ℝ) → X) (closedBall 0 1)
continuousOn_symm : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i).symm : X → Fin n → ℝ) (map n i).target
pairwiseDisjoint' :
  PairwiseDisjoint (α := Set X) univ fun (ni : (n : ℕ) × cell n) ↦
    (↑(map (ni.fst (β := fun (n : ℕ) ↦ cell n)) (ni.snd (β := fun (n : ℕ) ↦ cell n))) : (Fin ni.fst → ℝ) → X) ''
      ball 0 1
disjointBase' : ∀ (n : ℕ) (i : cell n), Disjoint ((↑(map n i) : (Fin n → ℝ) → X) '' ball 0 1) D
mapsTo :
  ∀ (n : ℕ) (i : cell n),
    MapsTo (↑(map n i) : (Fin n → ℝ) → X) (sphere 0 1)
      (D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ (j : cell m), (↑(map m j) : (Fin m → ℝ) → X) '' closedBall 0 1)
isClosedBase : IsClosed[inst_2] D
union' : D ∪ ⋃ (n : ℕ), ⋃ (j : cell n), (↑(map n j) : (Fin n → ℝ) → X) '' closedBall 0 1 = C
A : Set X
asubc : A ⊆ C
h :
  (∀ (n : ℕ) (j : cell n), IsClosed[inst_2] (A ∩ (↑(map n j) : (Fin n → ℝ) → X) '' closedBall 0 1)) ∧
    IsClosed[inst_2] (A ∩ D)
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → IsEmpty.{u + 1} (cell b)
this :
  IsClosed[inst_2]
    (A ∩
      (D ∪
        ⋃ (n : { n : ℕ // n < N }),
          ⋃ (j : cell (↑n : ℕ)), (↑(map (↑n : ℕ) j) : (Fin (↑n : ℕ) → ℝ) → X) '' closedBall 0 1))
n : ℕ
i : cell n
⊢ n < N

Tactic:
have : n < N := Decidable.byContradiction fun h ↦ (hN n (Nat.ge_of_not_lt h)).false i
-- Module: Mathlib.Topology.CWComplex.Classical.Finite
Goal:
X_1 : Type u_1
inst : TopologicalSpace X_1
C_1 D_1 : Set X_1
inst_1 : RelCWComplex C_1 D_1
X : Type u
inst_2 : TopologicalSpace X
C D : Set X
cell : (n : ℕ) → Type u
map : (n : ℕ) → (i : cell n) → PartialEquiv (Fin n → ℝ) X
finite_cell : ∀ (n : ℕ), _root_.Finite.{u + 1} (cell n)
source_eq : ∀ (n : ℕ) (i : cell n), (map n i).source = ball 0 1
continuousOn : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i) : (Fin n → ℝ) → X) (closedBall 0 1)
continuousOn_symm : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i).symm : X → Fin n → ℝ) (map n i).target
pairwiseDisjoint' :
  PairwiseDisjoint (α := Set X) univ fun (ni : (n : ℕ) × cell n) ↦
    (↑(map (ni.fst (β := fun (n : ℕ) ↦ cell n)) (ni.snd (β := fun (n : ℕ) ↦ cell n))) : (Fin ni.fst → ℝ) → X) ''
      ball 0 1
disjointBase' : ∀ (n : ℕ) (i : cell n), Disjoint ((↑(map n i) : (Fin n → ℝ) → X) '' ball 0 1) D
mapsTo :
  ∀ (n : ℕ) (i : cell n),
    MapsTo (↑(map n i) : (Fin n → ℝ) → X) (sphere 0 1)
      (D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ (j : cell m), (↑(map m j) : (Fin m → ℝ) → X) '' closedBall 0 1)
isClosedBase : IsClosed[inst_2] D
union' : D ∪ ⋃ (n : ℕ), ⋃ (j : cell n), (↑(map n j) : (Fin n → ℝ) → X) '' closedBall 0 1 = C
A : Set X
asubc : A ⊆ C
h :
  (∀ (n : ℕ) (j : cell n), IsClosed[inst_2] (A ∩ (↑(map n j) : (Fin n → ℝ) → X) '' closedBall 0 1)) ∧
    IsClosed[inst_2] (A ∩ D)
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → IsEmpty.{u + 1} (cell b)
this_1 :
  IsClosed[inst_2]
    (A ∩
      (D ∪
        ⋃ (n : { n : ℕ // n < N }),
          ⋃ (j : cell (↑n : ℕ)), (↑(map (↑n : ℕ) j) : (Fin (↑n : ℕ) → ℝ) → X) '' closedBall 0 1))
n : ℕ
i : cell n
this : n < N
⊢ (↑(map n i) : (Fin n → ℝ) → X) '' closedBall 0 1 ⊆
    ⋃ (hx : n < N),
      ⋃ (j : cell (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < N) n hx) : ℕ)),
        (↑(map (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < N) n hx) : ℕ) j) : (Fin (↑⟨n, hx⟩ : ℕ) → ℝ) → X) '' closedBall 0 1

Tactic:
subset_iUnion₂ (s := fun _ i ↦ (map n i) '' closedBall 0 1) this i

Premises used: Set.subset_iUnion₂
-- Module: Mathlib.Topology.CWComplex.Classical.Finite
Goal:
X_1 : Type u_1
inst : TopologicalSpace X_1
C_1 D_1 : Set X_1
inst_1 : RelCWComplex C_1 D_1
X : Type u
inst_2 : TopologicalSpace X
C D : Set X
cell : (n : ℕ) → Type u
map : (n : ℕ) → (i : cell n) → PartialEquiv (Fin n → ℝ) X
finite_cell : ∀ (n : ℕ), _root_.Finite.{u + 1} (cell n)
source_eq : ∀ (n : ℕ) (i : cell n), (map n i).source = ball 0 1
continuousOn : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i) : (Fin n → ℝ) → X) (closedBall 0 1)
continuousOn_symm : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i).symm : X → Fin n → ℝ) (map n i).target
pairwiseDisjoint' :
  PairwiseDisjoint (α := Set X) univ fun (ni : (n : ℕ) × cell n) ↦
    (↑(map (ni.fst (β := fun (n : ℕ) ↦ cell n)) (ni.snd (β := fun (n : ℕ) ↦ cell n))) : (Fin ni.fst → ℝ) → X) ''
      ball 0 1
disjointBase' : ∀ (n : ℕ) (i : cell n), Disjoint ((↑(map n i) : (Fin n → ℝ) → X) '' ball 0 1) D
mapsTo :
  ∀ (n : ℕ) (i : cell n),
    MapsTo (↑(map n i) : (Fin n → ℝ) → X) (sphere 0 1)
      (D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ (j : cell m), (↑(map m j) : (Fin m → ℝ) → X) '' closedBall 0 1)
isClosedBase : IsClosed[inst_2] D
union' : D ∪ ⋃ (n : ℕ), ⋃ (j : cell n), (↑(map n j) : (Fin n → ℝ) → X) '' closedBall 0 1 = C
A : Set X
asubc : A ⊆ C
h :
  (∀ (n : ℕ) (j : cell n), IsClosed[inst_2] (A ∩ (↑(map n j) : (Fin n → ℝ) → X) '' closedBall 0 1)) ∧
    IsClosed[inst_2] (A ∩ D)
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → IsEmpty.{u + 1} (cell b)
this_1 :
  IsClosed[inst_2]
    (A ∩
      (D ∪
        ⋃ (n : { n : ℕ // n < N }),
          ⋃ (j : cell (↑n : ℕ)), (↑(map (↑n : ℕ) j) : (Fin (↑n : ℕ) → ℝ) → X) '' closedBall 0 1))
n : ℕ
i : cell n
this : n < N
⊢ (↑(map n i) : (Fin n → ℝ) → X) '' closedBall 0 1 ⊆
    ⋃ (hx : n < N),
      ⋃ (j : cell (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < N) n hx) : ℕ)),
        (↑(map (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < N) n hx) : ℕ) j) : (Fin (↑⟨n, hx⟩ : ℕ) → ℝ) → X) '' closedBall 0 1

Tactic:
exact subset_iUnion₂ (s := fun _ i ↦ (map n i) '' closedBall 0 1) this i

Premises used: Set.subset_iUnion₂
-- Module: Mathlib.Topology.CWComplex.Classical.Finite
Goal:
X_1 : Type u_1
inst : TopologicalSpace X_1
C_1 D_1 : Set X_1
inst_1 : RelCWComplex C_1 D_1
X : Type u
inst_2 : TopologicalSpace X
C D : Set X
cell : (n : ℕ) → Type u
map : (n : ℕ) → (i : cell n) → PartialEquiv (Fin n → ℝ) X
finite_cell : ∀ (n : ℕ), _root_.Finite.{u + 1} (cell n)
source_eq : ∀ (n : ℕ) (i : cell n), (map n i).source = ball 0 1
continuousOn : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i) : (Fin n → ℝ) → X) (closedBall 0 1)
continuousOn_symm : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i).symm : X → Fin n → ℝ) (map n i).target
pairwiseDisjoint' :
  PairwiseDisjoint (α := Set X) univ fun (ni : (n : ℕ) × cell n) ↦
    (↑(map (ni.fst (β := fun (n : ℕ) ↦ cell n)) (ni.snd (β := fun (n : ℕ) ↦ cell n))) : (Fin ni.fst → ℝ) → X) ''
      ball 0 1
disjointBase' : ∀ (n : ℕ) (i : cell n), Disjoint ((↑(map n i) : (Fin n → ℝ) → X) '' ball 0 1) D
mapsTo :
  ∀ (n : ℕ) (i : cell n),
    MapsTo (↑(map n i) : (Fin n → ℝ) → X) (sphere 0 1)
      (D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ (j : cell m), (↑(map m j) : (Fin m → ℝ) → X) '' closedBall 0 1)
isClosedBase : IsClosed[inst_2] D
union' : D ∪ ⋃ (n : ℕ), ⋃ (j : cell n), (↑(map n j) : (Fin n → ℝ) → X) '' closedBall 0 1 = C
A : Set X
asubc : A ⊆ C
h :
  (∀ (n : ℕ) (j : cell n), IsClosed[inst_2] (A ∩ (↑(map n j) : (Fin n → ℝ) → X) '' closedBall 0 1)) ∧
    IsClosed[inst_2] (A ∩ D)
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → IsEmpty.{u + 1} (cell b)
suffices :
  IsClosed[inst_2]
    (A ∩
      (D ∪
        ⋃ (n : { n : ℕ // n < N }),
          ⋃ (j : cell (↑n : ℕ)), (↑(map (↑n : ℕ) j) : (Fin (↑n : ℕ) → ℝ) → X) '' closedBall 0 1))
⊢ IsClosed[inst_2] (A ∩ C)

Tactic:
suffices IsClosed (A ∩ (D ∪ ⋃ (n : {n : ℕ // n < N}), ⋃ j, ↑(map n j) '' closedBall 0 1)) by
      convert! this using 2
      rw [← union', iUnion_subtype]
      congrm D ∪ ⋃ n, ?_
      refine subset_antisymm ?_ (iUnion_subset (fun i ↦ by rfl))
      apply iUnion_subset
      intro i
      have : n < N := Decidable.byContradiction fun h ↦ (hN n (Nat.ge_of_not_lt h)).false i
      exact subset_iUnion₂ (s := fun _ i ↦ (map n i) '' closedBall 0 1) this i
-- Module: Mathlib.Topology.CWComplex.Classical.Finite
Goal:
X_1 : Type u_1
inst : TopologicalSpace X_1
C_1 D_1 : Set X_1
inst_1 : RelCWComplex C_1 D_1
X : Type u
inst_2 : TopologicalSpace X
C D : Set X
cell : (n : ℕ) → Type u
map : (n : ℕ) → (i : cell n) → PartialEquiv (Fin n → ℝ) X
finite_cell : ∀ (n : ℕ), _root_.Finite.{u + 1} (cell n)
source_eq : ∀ (n : ℕ) (i : cell n), (map n i).source = ball 0 1
continuousOn : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i) : (Fin n → ℝ) → X) (closedBall 0 1)
continuousOn_symm : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i).symm : X → Fin n → ℝ) (map n i).target
pairwiseDisjoint' :
  PairwiseDisjoint (α := Set X) univ fun (ni : (n : ℕ) × cell n) ↦
    (↑(map (ni.fst (β := fun (n : ℕ) ↦ cell n)) (ni.snd (β := fun (n : ℕ) ↦ cell n))) : (Fin ni.fst → ℝ) → X) ''
      ball 0 1
disjointBase' : ∀ (n : ℕ) (i : cell n), Disjoint ((↑(map n i) : (Fin n → ℝ) → X) '' ball 0 1) D
mapsTo :
  ∀ (n : ℕ) (i : cell n),
    MapsTo (↑(map n i) : (Fin n → ℝ) → X) (sphere 0 1)
      (D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ (j : cell m), (↑(map m j) : (Fin m → ℝ) → X) '' closedBall 0 1)
isClosedBase : IsClosed[inst_2] D
union' : D ∪ ⋃ (n : ℕ), ⋃ (j : cell n), (↑(map n j) : (Fin n → ℝ) → X) '' closedBall 0 1 = C
A : Set X
asubc : A ⊆ C
h :
  (∀ (n : ℕ) (j : cell n), IsClosed[inst_2] (A ∩ (↑(map n j) : (Fin n → ℝ) → X) '' closedBall 0 1)) ∧
    IsClosed[inst_2] (A ∩ D)
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → IsEmpty.{u + 1} (cell b)
simp_rw :
  IsClosed[inst_2]
    (A ∩ D ∪
      ⋃ (i : { n : ℕ // n < N }),
        ⋃ (i_1 : cell (↑i : ℕ)), A ∩ (↑(map (↑i : ℕ) i_1) : (Fin (↑i : ℕ) → ℝ) → X) '' closedBall 0 1)
⊢ IsClosed[inst_2]
    (A ∩
      (D ∪
        ⋃ (n : { n : ℕ // n < N }),
          ⋃ (j : cell (↑n : ℕ)), (↑(map (↑n : ℕ) j) : (Fin (↑n : ℕ) → ℝ) → X) '' closedBall 0 1))

Tactic:
simp_rw [inter_union_distrib_left, inter_iUnion]

Premises used: Set.inter_iUnion, Set.inter_union_distrib_left
-- Module: Mathlib.Topology.CWComplex.Classical.Finite
Goal:
X_1 : Type u_1
inst : TopologicalSpace X_1
C_1 D_1 : Set X_1
inst_1 : RelCWComplex C_1 D_1
X : Type u
inst_2 : TopologicalSpace X
C D : Set X
cell : (n : ℕ) → Type u
map : (n : ℕ) → (i : cell n) → PartialEquiv (Fin n → ℝ) X
finite_cell : ∀ (n : ℕ), _root_.Finite.{u + 1} (cell n)
source_eq : ∀ (n : ℕ) (i : cell n), (map n i).source = ball 0 1
continuousOn : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i) : (Fin n → ℝ) → X) (closedBall 0 1)
continuousOn_symm : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i).symm : X → Fin n → ℝ) (map n i).target
pairwiseDisjoint' :
  PairwiseDisjoint (α := Set X) univ fun (ni : (n : ℕ) × cell n) ↦
    (↑(map (ni.fst (β := fun (n : ℕ) ↦ cell n)) (ni.snd (β := fun (n : ℕ) ↦ cell n))) : (Fin ni.fst → ℝ) → X) ''
      ball 0 1
disjointBase' : ∀ (n : ℕ) (i : cell n), Disjoint ((↑(map n i) : (Fin n → ℝ) → X) '' ball 0 1) D
mapsTo :
  ∀ (n : ℕ) (i : cell n),
    MapsTo (↑(map n i) : (Fin n → ℝ) → X) (sphere 0 1)
      (D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ (j : cell m), (↑(map m j) : (Fin m → ℝ) → X) '' closedBall 0 1)
isClosedBase : IsClosed[inst_2] D
union' : D ∪ ⋃ (n : ℕ), ⋃ (j : cell n), (↑(map n j) : (Fin n → ℝ) → X) '' closedBall 0 1 = C
A : Set X
asubc : A ⊆ C
h :
  (∀ (n : ℕ) (j : cell n), IsClosed[inst_2] (A ∩ (↑(map n j) : (Fin n → ℝ) → X) '' closedBall 0 1)) ∧
    IsClosed[inst_2] (A ∩ D)
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → IsEmpty.{u + 1} (cell b)
⊢ IsClosed[inst_2]
    (A ∩ D ∪
      ⋃ (i : { n : ℕ // n < N }),
        ⋃ (i_1 : cell (↑i : ℕ)), A ∩ (↑(map (↑i : ℕ) i_1) : (Fin (↑i : ℕ) → ℝ) → X) '' closedBall 0 1)

Tactic:
h.2.union (isClosed_iUnion_of_finite (fun n ↦ isClosed_iUnion_of_finite (h.1 n.1)))

Premises used: IsClosed.union, isClosed_iUnion_of_finite, And.right, And.left, Subtype.val
-- Module: Mathlib.Topology.CWComplex.Classical.Finite
Goal:
X_1 : Type u_1
inst : TopologicalSpace X_1
C_1 D_1 : Set X_1
inst_1 : RelCWComplex C_1 D_1
X : Type u
inst_2 : TopologicalSpace X
C D : Set X
cell : (n : ℕ) → Type u
map : (n : ℕ) → (i : cell n) → PartialEquiv (Fin n → ℝ) X
finite_cell : ∀ (n : ℕ), _root_.Finite.{u + 1} (cell n)
source_eq : ∀ (n : ℕ) (i : cell n), (map n i).source = ball 0 1
continuousOn : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i) : (Fin n → ℝ) → X) (closedBall 0 1)
continuousOn_symm : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i).symm : X → Fin n → ℝ) (map n i).target
pairwiseDisjoint' :
  PairwiseDisjoint (α := Set X) univ fun (ni : (n : ℕ) × cell n) ↦
    (↑(map (ni.fst (β := fun (n : ℕ) ↦ cell n)) (ni.snd (β := fun (n : ℕ) ↦ cell n))) : (Fin ni.fst → ℝ) → X) ''
      ball 0 1
disjointBase' : ∀ (n : ℕ) (i : cell n), Disjoint ((↑(map n i) : (Fin n → ℝ) → X) '' ball 0 1) D
mapsTo :
  ∀ (n : ℕ) (i : cell n),
    MapsTo (↑(map n i) : (Fin n → ℝ) → X) (sphere 0 1)
      (D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ (j : cell m), (↑(map m j) : (Fin m → ℝ) → X) '' closedBall 0 1)
isClosedBase : IsClosed[inst_2] D
union' : D ∪ ⋃ (n : ℕ), ⋃ (j : cell n), (↑(map n j) : (Fin n → ℝ) → X) '' closedBall 0 1 = C
A : Set X
asubc : A ⊆ C
h :
  (∀ (n : ℕ) (j : cell n), IsClosed[inst_2] (A ∩ (↑(map n j) : (Fin n → ℝ) → X) '' closedBall 0 1)) ∧
    IsClosed[inst_2] (A ∩ D)
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → IsEmpty.{u + 1} (cell b)
⊢ IsClosed[inst_2]
    (A ∩ D ∪
      ⋃ (i : { n : ℕ // n < N }),
        ⋃ (i_1 : cell (↑i : ℕ)), A ∩ (↑(map (↑i : ℕ) i_1) : (Fin (↑i : ℕ) → ℝ) → X) '' closedBall 0 1)

Tactic:
exact h.2.union (isClosed_iUnion_of_finite (fun n ↦ isClosed_iUnion_of_finite (h.1 n.1)))

Premises used: IsClosed.union, isClosed_iUnion_of_finite, And.right
-- Module: Mathlib.Topology.CWComplex.Classical.Finite
Goal:
X : Type u
inst : TopologicalSpace X
C D : Set X
cell : (n : ℕ) → Type u
map : (n : ℕ) → (i : cell n) → PartialEquiv (Fin n → ℝ) X
eventually_isEmpty_cell : ∀ᶠ (n : ℕ) in Filter.atTop, IsEmpty.{u + 1} (cell n)
finite_cell : ∀ (n : ℕ), _root_.Finite.{u + 1} (cell n)
source_eq : ∀ (n : ℕ) (i : cell n), (map n i).source = ball 0 1
continuousOn : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i) : (Fin n → ℝ) → X) (closedBall 0 1)
continuousOn_symm : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i).symm : X → Fin n → ℝ) (map n i).target
pairwiseDisjoint' :
  PairwiseDisjoint (α := Set X) univ fun (ni : (n : ℕ) × cell n) ↦
    (↑(map (ni.fst (β := fun (n : ℕ) ↦ cell n)) (ni.snd (β := fun (n : ℕ) ↦ cell n))) : (Fin ni.fst → ℝ) → X) ''
      ball 0 1
disjointBase' : ∀ (n : ℕ) (i : cell n), Disjoint ((↑(map n i) : (Fin n → ℝ) → X) '' ball 0 1) D
mapsTo :
  ∀ (n : ℕ) (i : cell n),
    MapsTo (↑(map n i) : (Fin n → ℝ) → X) (sphere 0 1)
      (D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ (j : cell m), (↑(map m j) : (Fin m → ℝ) → X) '' closedBall 0 1)
isClosedBase : IsClosed[inst] D
union' : D ∪ ⋃ (n : ℕ), ⋃ (j : cell n), (↑(map n j) : (Fin n → ℝ) → X) '' closedBall 0 1 = C
⊢ Finite C (D := D)

Tactic:
letI := mkFinite C D cell map eventually_isEmpty_cell finite_cell source_eq continuousOn
      continuousOn_symm pairwiseDisjoint' disjointBase' mapsTo isClosedBase union'
  { eventually_isEmpty_cell := eventually_isEmpty_cell
    finite_cell := finite_cell }

Premises used: Topology.RelCWComplex.Finite.mk
-- Module: Mathlib.Topology.CWComplex.Classical.Finite
Goal:
X_1 : Type u_1
inst : TopologicalSpace X_1
C_1 D : Set X_1
inst_1 : RelCWComplex C_1 D
X : Type u
inst_2 : TopologicalSpace X
C : Set X
cell : (n : ℕ) → Type u
map : (n : ℕ) → (i : cell n) → PartialEquiv (Fin n → ℝ) X
eventually_isEmpty_cell : ∀ᶠ (n : ℕ) in Filter.atTop, IsEmpty.{u + 1} (cell n)
finite_cell : ∀ (n : ℕ), _root_.Finite.{u + 1} (cell n)
source_eq : ∀ (n : ℕ) (i : cell n), (map n i).source = ball 0 1
continuousOn : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i) : (Fin n → ℝ) → X) (closedBall 0 1)
continuousOn_symm : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i).symm : X → Fin n → ℝ) (map n i).target
pairwiseDisjoint' :
  PairwiseDisjoint (α := Set X) univ fun (ni : (n : ℕ) × cell n) ↦
    (↑(map (ni.fst (β := fun (n : ℕ) ↦ cell n)) (ni.snd (β := fun (n : ℕ) ↦ cell n))) : (Fin ni.fst → ℝ) → X) ''
      ball 0 1
mapsTo_iff_image_subset :
  ∀ (n : ℕ) (i : cell n),
    MapsTo (↑(map n i) : (Fin n → ℝ) → X) (sphere 0 1)
      (⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ (j : cell m), (↑(map m j) : (Fin m → ℝ) → X) '' closedBall 0 1)
union' : ⋃ (n : ℕ), ⋃ (j : cell n), (↑(map n j) : (Fin n → ℝ) → X) '' closedBall 0 1 = C
⊢ ∀ (n : ℕ) (i : cell n), Disjoint ((↑(map n i) : (Fin n → ℝ) → X) '' ball 0 1) ∅

Tactic:
simp only [disjoint_empty, implies_true]

Premises used: Set.disjoint_empty, implies_true
-- Module: Mathlib.Topology.CWComplex.Classical.Finite
Goal:
X_1 : Type u_1
inst : TopologicalSpace X_1
C_1 D : Set X_1
inst_1 : RelCWComplex C_1 D
X : Type u
inst_2 : TopologicalSpace X
C : Set X
cell : (n : ℕ) → Type u
map : (n : ℕ) → (i : cell n) → PartialEquiv (Fin n → ℝ) X
eventually_isEmpty_cell : ∀ᶠ (n : ℕ) in Filter.atTop, IsEmpty.{u + 1} (cell n)
finite_cell : ∀ (n : ℕ), _root_.Finite.{u + 1} (cell n)
source_eq : ∀ (n : ℕ) (i : cell n), (map n i).source = ball 0 1
continuousOn : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i) : (Fin n → ℝ) → X) (closedBall 0 1)
continuousOn_symm : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i).symm : X → Fin n → ℝ) (map n i).target
pairwiseDisjoint' :
  PairwiseDisjoint (α := Set X) univ fun (ni : (n : ℕ) × cell n) ↦
    (↑(map (ni.fst (β := fun (n : ℕ) ↦ cell n)) (ni.snd (β := fun (n : ℕ) ↦ cell n))) : (Fin ni.fst → ℝ) → X) ''
      ball 0 1
mapsTo_iff_image_subset :
  ∀ (n : ℕ) (i : cell n),
    MapsTo (↑(map n i) : (Fin n → ℝ) → X) (sphere 0 1)
      (⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ (j : cell m), (↑(map m j) : (Fin m → ℝ) → X) '' closedBall 0 1)
union' : ⋃ (n : ℕ), ⋃ (j : cell n), (↑(map n j) : (Fin n → ℝ) → X) '' closedBall 0 1 = C
⊢ ∀ (n : ℕ) (i : cell n),
    MapsTo (↑(map n i) : (Fin n → ℝ) → X) (sphere 0 1)
      (∅ ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ (j : cell m), (↑(map m j) : (Fin m → ℝ) → X) '' closedBall 0 1)

Tactic:
simpa only [empty_union]

Premises used: Set.empty_union
-- Module: Mathlib.Topology.CWComplex.Classical.Finite
Goal:
X_1 : Type u_1
inst : TopologicalSpace X_1
C_1 D : Set X_1
inst_1 : RelCWComplex C_1 D
X : Type u
inst_2 : TopologicalSpace X
C : Set X
cell : (n : ℕ) → Type u
map : (n : ℕ) → (i : cell n) → PartialEquiv (Fin n → ℝ) X
eventually_isEmpty_cell : ∀ᶠ (n : ℕ) in Filter.atTop, IsEmpty.{u + 1} (cell n)
finite_cell : ∀ (n : ℕ), _root_.Finite.{u + 1} (cell n)
source_eq : ∀ (n : ℕ) (i : cell n), (map n i).source = ball 0 1
continuousOn : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i) : (Fin n → ℝ) → X) (closedBall 0 1)
continuousOn_symm : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i).symm : X → Fin n → ℝ) (map n i).target
pairwiseDisjoint' :
  PairwiseDisjoint (α := Set X) univ fun (ni : (n : ℕ) × cell n) ↦
    (↑(map (ni.fst (β := fun (n : ℕ) ↦ cell n)) (ni.snd (β := fun (n : ℕ) ↦ cell n))) : (Fin ni.fst → ℝ) → X) ''
      ball 0 1
mapsTo_iff_image_subset :
  ∀ (n : ℕ) (i : cell n),
    MapsTo (↑(map n i) : (Fin n → ℝ) → X) (sphere 0 1)
      (⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ (j : cell m), (↑(map m j) : (Fin m → ℝ) → X) '' closedBall 0 1)
union' : ⋃ (n : ℕ), ⋃ (j : cell n), (↑(map n j) : (Fin n → ℝ) → X) '' closedBall 0 1 = C
⊢ ∅ ∪ ⋃ (n : ℕ), ⋃ (j : cell n), (↑(map n j) : (Fin n → ℝ) → X) '' closedBall 0 1 = C

Tactic:
simpa only [empty_union]

Premises used: Set.empty_union
-- Module: Mathlib.Topology.CWComplex.Classical.Finite
Goal:
X : Type u
inst : TopologicalSpace X
C : Set X
cell : (n : ℕ) → Type u
map : (n : ℕ) → (i : cell n) → PartialEquiv (Fin n → ℝ) X
eventually_isEmpty_cell : ∀ᶠ (n : ℕ) in Filter.atTop, IsEmpty.{u + 1} (cell n)
finite_cell : ∀ (n : ℕ), _root_.Finite.{u + 1} (cell n)
source_eq : ∀ (n : ℕ) (i : cell n), (map n i).source = ball 0 1
continuousOn : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i) : (Fin n → ℝ) → X) (closedBall 0 1)
continuousOn_symm : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i).symm : X → Fin n → ℝ) (map n i).target
pairwiseDisjoint' :
  PairwiseDisjoint (α := Set X) univ fun (ni : (n : ℕ) × cell n) ↦
    (↑(map (ni.fst (β := fun (n : ℕ) ↦ cell n)) (ni.snd (β := fun (n : ℕ) ↦ cell n))) : (Fin ni.fst → ℝ) → X) ''
      ball 0 1
mapsTo :
  ∀ (n : ℕ) (i : cell n),
    MapsTo (↑(map n i) : (Fin n → ℝ) → X) (sphere 0 1)
      (⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ (j : cell m), (↑(map m j) : (Fin m → ℝ) → X) '' closedBall 0 1)
union' : ⋃ (n : ℕ), ⋃ (j : cell n), (↑(map n j) : (Fin n → ℝ) → X) '' closedBall 0 1 = C
⊢ Finite C (D := ∅)

Tactic:
letI := mkFinite C cell map eventually_isEmpty_cell finite_cell source_eq continuousOn
      continuousOn_symm pairwiseDisjoint' mapsTo union'
  { eventually_isEmpty_cell := eventually_isEmpty_cell
    finite_cell := finite_cell }

Premises used: Topology.RelCWComplex.Finite.mk
-- Module: Mathlib.Topology.CWComplex.Classical.Finite
Goal:
X : Type u_2
inst : TopologicalSpace X
C D : Set X
inst_1 : RelCWComplex C D
finite : _root_.Finite.{max (u_2 + 1) 1} ((n : ℕ) × @cell _ inst C D _ n)
simp : ∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → IsEmpty.{u_2 + 1} (@cell _ inst C D _ b)
⊢ ∀ᶠ (n : ℕ) in Filter.atTop, IsEmpty.{u_2 + 1} (@cell _ inst C D _ n)

Tactic:
simp only [Filter.eventually_atTop, ge_iff_le]

Premises used: ge_iff_le, Filter.eventually_atTop
-- Module: Mathlib.Topology.CWComplex.Classical.Finite
Goal:
X : Type u_2
inst : TopologicalSpace X
C D : Set X
inst_1 : RelCWComplex C D
finite : _root_.Finite.{max (u_2 + 1) 1} ((n : ℕ) × @cell _ inst C D _ n)
inl :
  IsEmpty.{max (u_2 + 1) 1} ((n : ℕ) × @cell _ inst C D _ n) →
    ∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → IsEmpty.{u_2 + 1} (@cell _ inst C D _ b)
inr :
  Nonempty.{max (u_2 + 1) 1} ((n : ℕ) × @cell _ inst C D _ n) →
    ∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → IsEmpty.{u_2 + 1} (@cell _ inst C D _ b)
⊢ ∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → IsEmpty.{u_2 + 1} (@cell _ inst C D _ b)

Tactic:
cases isEmpty_or_nonempty (Σ n, cell C n)

Premises used: isEmpty_or_nonempty, Topology.RelCWComplex.cell, Sigma