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
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_2] D
union' : D ∪ ⋃ (n : ℕ), ⋃ (j : cell n), (↑(map n j) : (Fin n → ℝ) → X) '' closedBall 0 1 = C
n : ℕ
i : cell n
h :
  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)
⊢ MapsTo (↑(map n i) : (Fin n → ℝ) → X) (sphere 0 1)
    (D ∪
      ⋃ (m : ℕ),
        ⋃ (_ : m < n),
          ⋃ (j : cell m),
            ⋃ (_ :
              Membership.mem (γ := Finset (cell m))
                ((fun (m : ℕ) ↦ (Finite.toFinset (s := univ) ⋯ : Finset (cell m))) m) j),
              (↑(map m j) : (Fin m → ℝ) → X) '' closedBall 0 1)

Tactic:
simp only [Finite.mem_toFinset, mem_univ, iUnion_true]

Premises used: Set.Finite.mem_toFinset, Set.iUnion_true, Set.mem_univ
-- 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
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_2] D
union' : D ∪ ⋃ (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)
    (D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ (j : cell m), (↑(map m j) : (Fin m → ℝ) → X) '' closedBall 0 1)

Tactic:
mapsTo n 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
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_2] D
union' : D ∪ ⋃ (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)
    (D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ (j : cell m), (↑(map m j) : (Fin m → ℝ) → X) '' closedBall 0 1)

Tactic:
exact mapsTo n 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
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_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)
rw : IsClosed[inst_2] (A ∩ C)
⊢ IsClosed[inst_2] A

Tactic:
rw [← inter_eq_left.2 asubc]

Premises used: Set.inter_eq_left, Iff.mpr
-- 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
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_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)
⊢ ∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → IsEmpty.{u + 1} (cell b)

Tactic:
simp_rw [Filter.eventually_atTop, ge_iff_le] at eventually_isEmpty_cell

Premises used: ge_iff_le, Filter.eventually_atTop
-- 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)
eventually_isEmpty_cell : ∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → IsEmpty.{u + 1} (cell b)
obtain : ∀ (N : ℕ) (hN : ∀ (b : ℕ), N ≤ b → IsEmpty.{u + 1} (cell b)), IsClosed[inst_2] (A ∩ C)
⊢ IsClosed[inst_2] (A ∩ C)

Tactic:
obtain ⟨N, hN⟩ := eventually_isEmpty_cell
-- 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))
⊢ IsClosed[inst_2]
    (A ∩
      (D ∪
        ⋃ (n : { n : ℕ // n < N }),
          ⋃ (j : cell (↑n : ℕ)), (↑(map (↑n : ℕ) j) : (Fin (↑n : ℕ) → ℝ) → X) '' closedBall 0 1))

Tactic:
this
-- 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))
h₁ :
  C =
    D ∪
      ⋃ (n : { n : ℕ // n < N }), ⋃ (j : cell (↑n : ℕ)), (↑(map (↑n : ℕ) j) : (Fin (↑n : ℕ) → ℝ) → X) '' closedBall 0 1
⊢ IsClosed[inst_2] (A ∩ C)

Tactic:
convert! this using 2
-- 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))
h₁ :
  D ∪ ⋃ (n : ℕ), ⋃ (j : cell n), (↑(map n j) : (Fin n → ℝ) → X) '' closedBall 0 1 =
    D ∪
      ⋃ (x : ℕ),
        ⋃ (hx : x < N),
          ⋃ (j : cell (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < N) x hx) : ℕ)),
            (↑(map (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < N) x hx) : ℕ) j) : (Fin (↑⟨x, hx⟩ : ℕ) → ℝ) → X) ''
              closedBall 0 1
⊢ C =
    D ∪
      ⋃ (n : { n : ℕ // n < N }), ⋃ (j : cell (↑n : ℕ)), (↑(map (↑n : ℕ) j) : (Fin (↑n : ℕ) → ℝ) → X) '' closedBall 0 1

Tactic:
rw [← union', iUnion_subtype]

Premises used: Set.iUnion_subtype
-- 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))
h₁ :
  ∀ (n : ℕ),
    Eq.{u + 1} (α := 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)
⊢ D ∪ ⋃ (n : ℕ), ⋃ (j : cell n), (↑(map n j) : (Fin n → ℝ) → X) '' closedBall 0 1 =
    D ∪
      ⋃ (x : ℕ),
        ⋃ (hx : x < N),
          ⋃ (j : cell (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < N) x hx) : ℕ)),
            (↑(map (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < N) x hx) : ℕ) j) : (Fin (↑⟨x, hx⟩ : ℕ) → ℝ) → X) ''
              closedBall 0 1

Tactic:
congrm D ∪ ⋃ n, ?_
-- 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 : n < N
⊢ Subset.{u} (α := Set X)
    (⋃ (j : cell (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < N) n i) : ℕ)),
      (↑(map (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < N) n i) : ℕ) j) : (Fin (↑⟨n, i⟩ : ℕ) → ℝ) → X) '' closedBall 0 1)
    (⋃ (j : cell (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < N) n i) : ℕ)),
      (↑(map (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < N) n i) : ℕ) j) : (Fin (↑⟨n, i⟩ : ℕ) → ℝ) → X) '' closedBall 0 1)

Tactic:
rfl
-- 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₁ :
  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)
⊢ Eq.{u + 1} (α := 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:
refine subset_antisymm ?_ (iUnion_subset (fun i ↦ by rfl))

Premises used: Set.iUnion_subset, subset_antisymm