awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : T2Space X
inst_1 : RelCWComplex C D
n : ℕ
j : @cell _ t C D _ n
by_contra! : ∀ (h : (interior D ∩ closedCell (C := C) (D := D) n j).Nonempty), False
⊢ interior D ∩ closedCell (C := C) (D := D) n j = ∅

Tactic:
by_contra! h
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : T2Space X
inst_1 : RelCWComplex C D
n : ℕ
j : @cell _ t C D _ n
h : (interior D ∩ closedCell (C := C) (D := D) n j).Nonempty
⊢ (openCell (C := C) (D := D) n j ∩ interior D).Nonempty

Tactic:
rw [← closure_openCell_eq_closedCell, inter_comm,
    closure_inter_open_nonempty_iff isOpen_interior] at h

Premises used: isOpen_interior, Set.inter_comm, Topology.RelCWComplex.closure_openCell_eq_closedCell, closure_inter_open_nonempty_iff
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : T2Space X
inst_1 : RelCWComplex C D
n : ℕ
j : @cell _ t C D _ n
h : (openCell (C := C) (D := D) n j ∩ interior D).Nonempty
rcases : ∀ (x : X) (xmemcell : x ∈ openCell (C := C) (D := D) n j) (xmemD : x ∈ interior D), False
⊢ False

Tactic:
rcases h with ⟨x, xmemcell, xmemD⟩
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : T2Space X
inst_1 : RelCWComplex C D
n : ℕ
j : @cell _ t C D _ n
x : X
xmemcell : x ∈ openCell (C := C) (D := D) n j
xmemD : x ∈ interior D
this : x ∈ (↑(skeletonLT C (D := D) 0) : Set X) ∩ openCell (C := C) (D := D) n j
rwa rwa₁ rwa₂ rwa₃ : ∀ (this : Membership.mem (γ := Set X) ∅ x), False
⊢ False

Tactic:
rwa [(disjoint_skeletonLT_openCell n.cast_nonneg').inter_eq] at this

Premises used: Nat.cast_nonneg', Topology.RelCWComplex.disjoint_skeletonLT_openCell, Disjoint.inter_eq
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : T2Space X
inst_1 : RelCWComplex C D
n : ℕ
j : @cell _ t C D _ n
x : X
xmemcell : x ∈ openCell (C := C) (D := D) n j
xmemD : x ∈ interior D
suffices : x ∈ (↑(skeletonLT C (D := D) 0) : Set X) ∩ openCell (C := C) (D := D) n j
⊢ False

Tactic:
suffices x ∈ (skeletonLT C 0 : Set X) ∩ openCell n j by
    rwa [(disjoint_skeletonLT_openCell n.cast_nonneg').inter_eq] at this
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : T2Space X
inst_1 : RelCWComplex C D
n : ℕ
j : @cell _ t C D _ n
x : X
xmemcell : x ∈ openCell (C := C) (D := D) n j
xmemD : x ∈ interior D
⊢ x ∈ (↑(skeletonLT C (D := D) 0) : Set X) ∩ openCell (C := C) (D := D) n j

Tactic:
⟨(skeletonLT C 0).base_subset (interior_subset xmemD), xmemcell⟩

Premises used: interior_subset, Set.Mem, setOf, Set.inter, Topology.RelCWComplex.Subcomplex.base_subset, And.intro, Topology.RelCWComplex.skeletonLT, OfNat.ofNat
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : T2Space X
inst_1 : RelCWComplex C D
n : ℕ
j : @cell _ t C D _ n
x : X
xmemcell : x ∈ openCell (C := C) (D := D) n j
xmemD : x ∈ interior D
⊢ x ∈ (↑(skeletonLT C (D := D) 0) : Set X) ∩ openCell (C := C) (D := D) n j

Tactic:
exact ⟨(skeletonLT C 0).base_subset (interior_subset xmemD), xmemcell⟩
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : T2Space X
inst_1 : RelCWComplex C D
simp_rw : interior D ∩ ⋃ (n : ℕ), ⋃ (j : @cell _ t C D _ n), closedCell (C := C) (D := D) n j = ∅
simp_rw₁ :
  Eq.{u_1 + 1} (α := Set X) (⋃ (i : ℕ), ⋃ (i_1 : @cell _ t C D _ i), interior D ∩ closedCell (C := C) (D := D) i i_1) ∅
simp_rw₂ : Eq.{u_1 + 1} (α := Set X) (⋃ (i : ℕ), ⋃ (i : @cell _ t C D _ i), ∅) ∅
⊢ Disjoint (interior D) (⋃ (n : ℕ), ⋃ (j : @cell _ t C D _ n), closedCell (C := C) (D := D) n j)

Tactic:
simp_rw [disjoint_iff_inter_eq_empty, inter_iUnion, disjoint_interior_base_closedCell.inter_eq,
    iUnion_empty]

Premises used: Set.disjoint_iff_inter_eq_empty, Topology.RelCWComplex.disjoint_interior_base_closedCell, Set.inter_iUnion, Set.iUnion_empty, Disjoint.inter_eq
-- 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)
closed' :
  ∀ A ⊆ C,
    (∀ (n : ℕ) (j : cell n), IsClosed[inst_2] (A ∩ (↑(map n j) : (Fin n → ℝ) → X) '' closedBall 0 1)) ∧
        IsClosed[inst_2] (A ∩ D) →
      IsClosed[inst_2] A
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),
            ⋃ (_ :
              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)
⊢ ∃ (I : (m : ℕ) → Finset (cell m)),
    MapsTo (↑(map n i) : (Fin n → ℝ) → X) (sphere 0 1)
      (D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, (↑(map m j) : (Fin m → ℝ) → X) '' closedBall 0 1)

Tactic:
use fun m ↦ finite_univ.toFinset (s := (univ : Set (cell m)))

Premises used: Set.finite_univ, Set.Finite.toFinset
-- 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)
closed' :
  ∀ A ⊆ C,
    (∀ (n : ℕ) (j : cell n), IsClosed[inst_2] (A ∩ (↑(map n j) : (Fin n → ℝ) → X) '' closedBall 0 1)) ∧
        IsClosed[inst_2] (A ∩ D) →
      IsClosed[inst_2] A
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
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)
closed' :
  ∀ A ⊆ C,
    (∀ (n : ℕ) (j : cell n), IsClosed[inst_2] (A ∩ (↑(map n j) : (Fin n → ℝ) → X) '' closedBall 0 1)) ∧
        IsClosed[inst_2] (A ∩ D) →
      IsClosed[inst_2] A
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
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)
closed' :
  ∀ A ⊆ C,
    (∀ (n : ℕ) (j : cell n), IsClosed[inst_2] (A ∩ (↑(map n j) : (Fin n → ℝ) → X) '' closedBall 0 1)) ∧
        IsClosed[inst_2] (A ∩ D) →
      IsClosed[inst_2] A
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 : Type u
inst : 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)
closed' :
  ∀ A ⊆ C,
    (∀ (n : ℕ) (j : cell n), IsClosed[inst] (A ∩ (↑(map n j) : (Fin n → ℝ) → X) '' closedBall 0 1)) ∧
        IsClosed[inst] (A ∩ D) →
      IsClosed[inst] A
isClosedBase : IsClosed[inst] D
union' : D ∪ ⋃ (n : ℕ), ⋃ (j : cell n), (↑(map n j) : (Fin n → ℝ) → X) '' closedBall 0 1 = C
⊢ FiniteType C (D := D)

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

Premises used: Topology.RelCWComplex.FiniteType.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
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)
closed' :
  ∀ A ⊆ C,
    (∀ (n : ℕ) (j : cell n), IsClosed[inst_2] (A ∩ (↑(map n j) : (Fin n → ℝ) → X) '' closedBall 0 1)) →
      IsClosed[inst_2] A
union' : ⋃ (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)
    (⋃ (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)
⊢ ∃ (I : (m : ℕ) → Finset (cell m)),
    MapsTo (↑(map n i) : (Fin n → ℝ) → X) (sphere 0 1)
      (⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, (↑(map m j) : (Fin m → ℝ) → X) '' closedBall 0 1)

Tactic:
use fun m ↦ finite_univ.toFinset (s := (univ : Set (cell m)))

Premises used: Set.finite_univ, Set.Finite.toFinset
-- 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
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)
closed' :
  ∀ A ⊆ C,
    (∀ (n : ℕ) (j : cell n), IsClosed[inst_2] (A ∩ (↑(map n j) : (Fin n → ℝ) → X) '' closedBall 0 1)) →
      IsClosed[inst_2] A
union' : ⋃ (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)
    (⋃ (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)
    (⋃ (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 : 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
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)
closed' :
  ∀ A ⊆ C,
    (∀ (n : ℕ) (j : cell n), IsClosed[inst_2] (A ∩ (↑(map n j) : (Fin n → ℝ) → X) '' closedBall 0 1)) →
      IsClosed[inst_2] A
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:
mapsTo n i
-- 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
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)
closed' :
  ∀ A ⊆ C,
    (∀ (n : ℕ) (j : cell n), IsClosed[inst_2] (A ∩ (↑(map n j) : (Fin n → ℝ) → X) '' closedBall 0 1)) →
      IsClosed[inst_2] A
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:
exact mapsTo n i
-- 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
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)
closed' :
  ∀ A ⊆ C,
    (∀ (n : ℕ) (j : cell n), IsClosed[inst] (A ∩ (↑(map n j) : (Fin n → ℝ) → X) '' closedBall 0 1)) → IsClosed[inst] A
union' : ⋃ (n : ℕ), ⋃ (j : cell n), (↑(map n j) : (Fin n → ℝ) → X) '' closedBall 0 1 = C
⊢ FiniteType C (D := ∅)

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

Premises used: Topology.RelCWComplex.FiniteType.mk
-- 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),
            ⋃ (_ :
              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)
⊢ ∃ (I : (m : ℕ) → Finset (cell m)),
    MapsTo (↑(map n i) : (Fin n → ℝ) → X) (sphere 0 1)
      (D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, (↑(map m j) : (Fin m → ℝ) → X) '' closedBall 0 1)

Tactic:
use fun m ↦ finite_univ.toFinset (s := (univ : Set (cell m)))

Premises used: Set.finite_univ, Set.Finite.toFinset