awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.CWComplex.Classical.Subcomplex
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : T2Space X
inst_1 : RelCWComplex C D
E : Subcomplex C (D := D)
n : ℕ
i : (↑(E.I (C := C) (D := D) n) : Type u_1)
h :
  Membership.mem (γ := Set ((n : ℕ) × (↑(E.I (C := C) (D := D) n) : Type u_1))) univ
    (Sigma.mk (β := fun (n : ℕ) ↦ (↑(E.I (C := C) (D := D) n) : Type u_1)) n i)
this :
  ∀ (m : ℕ) (j : (↑(E.I (C := C) (D := D) m) : Type u_1)),
    Membership.mem (γ := Set ((n : ℕ) × (↑(E.I (C := C) (D := D) n) : Type u_1))) univ
        (Sigma.mk (β := fun (n : ℕ) ↦ (↑(E.I (C := C) (D := D) n) : Type u_1)) m j) →
      Ne.{u_1 + 1} (α := (n : ℕ) × (↑(E.I (C := C) (D := D) n) : Type u_1))
          (Sigma.mk (β := fun (n : ℕ) ↦ (↑(E.I (C := C) (D := D) n) : Type u_1)) n i)
          (Sigma.mk (β := fun (n : ℕ) ↦ (↑(E.I (C := C) (D := D) n) : Type u_1)) m j) →
        Function.onFun (β := Set X) Disjoint
          (fun (ni : (n : ℕ) × (↑(E.I (C := C) (D := D) n) : Type u_1)) ↦
            (↑(map (C := C) (D := D) (ni.fst (β := fun (n : ℕ) ↦ (↑(E.I (C := C) (D := D) n) : Type u_1)))
                    (↑(ni.snd (β := fun (n : ℕ) ↦ (↑(E.I (C := C) (D := D) n) : Type u_1))) : cell C ni.fst)) :
                (Fin ni.fst → ℝ) → X) ''
              ball 0 1)
          (Sigma.mk (β := fun (n : ℕ) ↦ (↑(E.I (C := C) (D := D) n) : Type u_1)) n i)
          (Sigma.mk (β := fun (n : ℕ) ↦ (↑(E.I (C := C) (D := D) n) : Type u_1)) m j)
⊢ ∀ ⦃y : (n : ℕ) × (↑(E.I (C := C) (D := D) n) : Type u_1)⦄,
    Membership.mem (γ := Set ((n : ℕ) × (↑(E.I (C := C) (D := D) n) : Type u_1))) univ y →
      Sigma.mk (β := fun (n : ℕ) ↦ (↑(E.I (C := C) (D := D) n) : Type u_1)) n i ≠ y →
        Function.onFun (β := Set X) Disjoint
          (fun (ni : (n : ℕ) × (↑(E.I (C := C) (D := D) n) : Type u_1)) ↦
            (↑(map (C := C) (D := D) (ni.fst (β := fun (n : ℕ) ↦ (↑(E.I (C := C) (D := D) n) : Type u_1)))
                    (↑(ni.snd (β := fun (n : ℕ) ↦ (↑(E.I (C := C) (D := D) n) : Type u_1))) : cell C ni.fst)) :
                (Fin ni.fst → ℝ) → X) ''
              ball 0 1)
          (Sigma.mk (β := fun (n : ℕ) ↦ (↑(E.I (C := C) (D := D) n) : Type u_1)) n i) y

Tactic:
⟨m, j⟩
-- Module: Mathlib.Topology.CWComplex.Classical.Subcomplex
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : T2Space X
inst_1 : RelCWComplex C D
E : Subcomplex C (D := D)
n : ℕ
i : (↑(E.I (C := C) (D := D) n) : Type u_1)
h :
  Membership.mem (γ := Set ((n : ℕ) × (↑(E.I (C := C) (D := D) n) : Type u_1))) univ
    (Sigma.mk (β := fun (n : ℕ) ↦ (↑(E.I (C := C) (D := D) n) : Type u_1)) n i)
m : ℕ
j : (↑(E.I (C := C) (D := D) m) : Type u_1)
_ :
  Membership.mem (γ := Set ((n : ℕ) × (↑(E.I (C := C) (D := D) n) : Type u_1))) univ
      (Sigma.mk (β := fun (n : ℕ) ↦ (↑(E.I (C := C) (D := D) n) : Type u_1)) m j) →
    Ne.{u_1 + 1} (α := (n : ℕ) × (↑(E.I (C := C) (D := D) n) : Type u_1))
        (Sigma.mk (β := fun (n : ℕ) ↦ (↑(E.I (C := C) (D := D) n) : Type u_1)) n i)
        (Sigma.mk (β := fun (n : ℕ) ↦ (↑(E.I (C := C) (D := D) n) : Type u_1)) m j) →
      Function.onFun (β := Set X) Disjoint
        (fun (ni : (n : ℕ) × (↑(E.I (C := C) (D := D) n) : Type u_1)) ↦
          (↑(map (C := C) (D := D) (ni.fst (β := fun (n : ℕ) ↦ (↑(E.I (C := C) (D := D) n) : Type u_1)))
                  (↑(ni.snd (β := fun (n : ℕ) ↦ (↑(E.I (C := C) (D := D) n) : Type u_1))) : cell C ni.fst)) :
              (Fin ni.fst → ℝ) → X) ''
            ball 0 1)
        (Sigma.mk (β := fun (n : ℕ) ↦ (↑(E.I (C := C) (D := D) n) : Type u_1)) n i)
        (Sigma.mk (β := fun (n : ℕ) ↦ (↑(E.I (C := C) (D := D) n) : Type u_1)) m j)
⊢ Membership.mem (γ := Set ((n : ℕ) × (↑(E.I (C := C) (D := D) n) : Type u_1))) univ
      (Sigma.mk (β := fun (n : ℕ) ↦ (↑(E.I (C := C) (D := D) n) : Type u_1)) m j) →
    Ne.{u_1 + 1} (α := (n : ℕ) × (↑(E.I (C := C) (D := D) n) : Type u_1))
        (Sigma.mk (β := fun (n : ℕ) ↦ (↑(E.I (C := C) (D := D) n) : Type u_1)) n i)
        (Sigma.mk (β := fun (n : ℕ) ↦ (↑(E.I (C := C) (D := D) n) : Type u_1)) m j) →
      Function.onFun (β := Set X) Disjoint
        (fun (ni : (n : ℕ) × (↑(E.I (C := C) (D := D) n) : Type u_1)) ↦
          (↑(map (C := C) (D := D) (ni.fst (β := fun (n : ℕ) ↦ (↑(E.I (C := C) (D := D) n) : Type u_1)))
                  (↑(ni.snd (β := fun (n : ℕ) ↦ (↑(E.I (C := C) (D := D) n) : Type u_1))) : cell C ni.fst)) :
              (Fin ni.fst → ℝ) → X) ''
            ball 0 1)
        (Sigma.mk (β := fun (n : ℕ) ↦ (↑(E.I (C := C) (D := D) n) : Type u_1)) n i)
        (Sigma.mk (β := fun (n : ℕ) ↦ (↑(E.I (C := C) (D := D) n) : Type u_1)) m j)

Tactic:
_
-- Module: Mathlib.Topology.CWComplex.Classical.Subcomplex
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : T2Space X
inst_1 : RelCWComplex C D
E : Subcomplex C (D := D)
n : ℕ
i : (↑(E.I (C := C) (D := D) n) : Type u_1)
h :
  Membership.mem (γ := Set ((n : ℕ) × (↑(E.I (C := C) (D := D) n) : Type u_1))) univ
    (Sigma.mk (β := fun (n : ℕ) ↦ (↑(E.I (C := C) (D := D) n) : Type u_1)) n i)
m : ℕ
j : (↑(E.I (C := C) (D := D) m) : Type u_1)
h_1 :
  Membership.mem (γ := Set ((n : ℕ) × (↑(E.I (C := C) (D := D) n) : Type u_1))) univ
    (Sigma.mk (β := fun (n : ℕ) ↦ (↑(E.I (C := C) (D := D) n) : Type u_1)) m j)
hne :
  Ne.{u_1 + 1} (α := (n : ℕ) × (↑(E.I (C := C) (D := D) n) : Type u_1))
    (Sigma.mk (β := fun (n : ℕ) ↦ (↑(E.I (C := C) (D := D) n) : Type u_1)) n i)
    (Sigma.mk (β := fun (n : ℕ) ↦ (↑(E.I (C := C) (D := D) n) : Type u_1)) m j)
⊢ Function.onFun (β := Set X) Disjoint
    (fun (ni : (n : ℕ) × (↑(E.I (C := C) (D := D) n) : Type u_1)) ↦
      (↑(map (C := C) (D := D) (ni.fst (β := fun (n : ℕ) ↦ (↑(E.I (C := C) (D := D) n) : Type u_1)))
              (↑(ni.snd (β := fun (n : ℕ) ↦ (↑(E.I (C := C) (D := D) n) : Type u_1))) : cell C ni.fst)) :
          (Fin ni.fst → ℝ) → X) ''
        ball 0 1)
    (Sigma.mk (β := fun (n : ℕ) ↦ (↑(E.I (C := C) (D := D) n) : Type u_1)) n i)
    (Sigma.mk (β := fun (n : ℕ) ↦ (↑(E.I (C := C) (D := D) n) : Type u_1)) m j)

Tactic:
@pairwiseDisjoint' _ _ C D _ ⟨n, i⟩ trivial ⟨m, j⟩ trivial ?_

Premises used: trivial, Topology.RelCWComplex.pairwiseDisjoint'
-- Module: Mathlib.Topology.CWComplex.Classical.Subcomplex
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : T2Space X
inst_1 : RelCWComplex C D
E : Subcomplex C (D := D)
n : ℕ
i : (↑(E.I (C := C) (D := D) n) : Type u_1)
h :
  Membership.mem (γ := Set ((n : ℕ) × (↑(E.I (C := C) (D := D) n) : Type u_1))) univ
    (Sigma.mk (β := fun (n : ℕ) ↦ (↑(E.I (C := C) (D := D) n) : Type u_1)) n i)
m : ℕ
j : (↑(E.I (C := C) (D := D) m) : Type u_1)
h_1 :
  Membership.mem (γ := Set ((n : ℕ) × (↑(E.I (C := C) (D := D) n) : Type u_1))) univ
    (Sigma.mk (β := fun (n : ℕ) ↦ (↑(E.I (C := C) (D := D) n) : Type u_1)) m j)
hne :
  Ne.{u_1 + 1} (α := (n : ℕ) × (↑(E.I (C := C) (D := D) n) : Type u_1))
    (Sigma.mk (β := fun (n : ℕ) ↦ (↑(E.I (C := C) (D := D) n) : Type u_1)) n i)
    (Sigma.mk (β := fun (n : ℕ) ↦ (↑(E.I (C := C) (D := D) n) : Type u_1)) m j)
refine :
  Sigma.mk (β := fun (n : ℕ) ↦ @cell _ t C D _ n) n (↑i : cell C n) ≠
    Sigma.mk (β := fun (n : ℕ) ↦ @cell _ t C D _ n) m (↑j : cell C m)
⊢ Function.onFun (β := Set X) Disjoint
    (fun (ni : (n : ℕ) × (↑(E.I (C := C) (D := D) n) : Type u_1)) ↦
      (↑(map (C := C) (D := D) (ni.fst (β := fun (n : ℕ) ↦ (↑(E.I (C := C) (D := D) n) : Type u_1)))
              (↑(ni.snd (β := fun (n : ℕ) ↦ (↑(E.I (C := C) (D := D) n) : Type u_1))) : cell C ni.fst)) :
          (Fin ni.fst → ℝ) → X) ''
        ball 0 1)
    (Sigma.mk (β := fun (n : ℕ) ↦ (↑(E.I (C := C) (D := D) n) : Type u_1)) n i)
    (Sigma.mk (β := fun (n : ℕ) ↦ (↑(E.I (C := C) (D := D) n) : Type u_1)) m j)

Tactic:
refine @pairwiseDisjoint' _ _ C D _ ⟨n, i⟩ trivial ⟨m, j⟩ trivial ?_

Premises used: trivial, Topology.RelCWComplex.pairwiseDisjoint'
-- Module: Mathlib.Topology.CWComplex.Classical.Subcomplex
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : T2Space X
inst_1 : RelCWComplex C D
E : Subcomplex C (D := D)
n : ℕ
i : (↑(E.I (C := C) (D := D) n) : Type u_1)
h :
  Membership.mem (γ := Set ((n : ℕ) × (↑(E.I (C := C) (D := D) n) : Type u_1))) univ
    (Sigma.mk (β := fun (n : ℕ) ↦ (↑(E.I (C := C) (D := D) n) : Type u_1)) n i)
m : ℕ
j : (↑(E.I (C := C) (D := D) m) : Type u_1)
h_1 :
  Membership.mem (γ := Set ((n : ℕ) × (↑(E.I (C := C) (D := D) n) : Type u_1))) univ
    (Sigma.mk (β := fun (n : ℕ) ↦ (↑(E.I (C := C) (D := D) n) : Type u_1)) m j)
hne :
  Ne.{u_1 + 1} (α := (n : ℕ) × (↑(E.I (C := C) (D := D) n) : Type u_1))
    (Sigma.mk (β := fun (n : ℕ) ↦ (↑(E.I (C := C) (D := D) n) : Type u_1)) n i)
    (Sigma.mk (β := fun (n : ℕ) ↦ (↑(E.I (C := C) (D := D) n) : Type u_1)) m j)
⊢ Sigma.mk (β := fun (n : ℕ) ↦ @cell _ t C D _ n) n (↑i : cell C n) ≠
    Sigma.mk (β := fun (n : ℕ) ↦ @cell _ t C D _ n) m (↑j : cell C m)

Tactic:
Function.injective_id.sigma_map (fun _ ↦ Subtype.val_injective) |>.ne hne

Premises used: Subtype.val_injective, Function.Injective.ne, Function.Injective.sigma_map, Function.injective_id, Sigma.map
-- Module: Mathlib.Topology.CWComplex.Classical.Subcomplex
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : T2Space X
inst_1 : RelCWComplex C D
E : Subcomplex C (D := D)
n : ℕ
i : (↑(E.I (C := C) (D := D) n) : Type u_1)
h :
  Membership.mem (γ := Set ((n : ℕ) × (↑(E.I (C := C) (D := D) n) : Type u_1))) univ
    (Sigma.mk (β := fun (n : ℕ) ↦ (↑(E.I (C := C) (D := D) n) : Type u_1)) n i)
m : ℕ
j : (↑(E.I (C := C) (D := D) m) : Type u_1)
h_1 :
  Membership.mem (γ := Set ((n : ℕ) × (↑(E.I (C := C) (D := D) n) : Type u_1))) univ
    (Sigma.mk (β := fun (n : ℕ) ↦ (↑(E.I (C := C) (D := D) n) : Type u_1)) m j)
hne :
  Ne.{u_1 + 1} (α := (n : ℕ) × (↑(E.I (C := C) (D := D) n) : Type u_1))
    (Sigma.mk (β := fun (n : ℕ) ↦ (↑(E.I (C := C) (D := D) n) : Type u_1)) n i)
    (Sigma.mk (β := fun (n : ℕ) ↦ (↑(E.I (C := C) (D := D) n) : Type u_1)) m j)
⊢ Sigma.mk (β := fun (n : ℕ) ↦ @cell _ t C D _ n) n (↑i : cell C n) ≠
    Sigma.mk (β := fun (n : ℕ) ↦ @cell _ t C D _ n) m (↑j : cell C m)

Tactic:
exact Function.injective_id.sigma_map (fun _ ↦ Subtype.val_injective) |>.ne hne

Premises used: Subtype.val_injective, Function.Injective.ne, Function.Injective.sigma_map, Function.injective_id
-- Module: Mathlib.Topology.CWComplex.Classical.Subcomplex
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : T2Space X
inst_1 : RelCWComplex C D
E : Subcomplex C (D := D)
n : ℕ
i : (↑(E.I (C := C) (D := D) n) : Type u_1)
rcases :
  ∀ (J : (m : ℕ) → Finset (@cell _ t C D _ m))
    (hJ :
      cellFrontier (C := C) (D := D) n (↑i : cell C n) ⊆
        D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ J m, openCell (C := C) (D := D) m j),
    ∃ (I : (m : ℕ) → Finset (↑(E.I (C := C) (D := D) m) : Type u_1)),
      MapsTo (↑(map (C := C) (D := D) n (↑i : cell C n)) : (Fin n → ℝ) → X) (sphere 0 1)
        (D ∪
          ⋃ (m : ℕ),
            ⋃ (_ : m < n), ⋃ j ∈ I m, (↑(map (C := C) (D := D) m (↑j : cell C m)) : (Fin m → ℝ) → X) '' closedBall 0 1)
⊢ ∃ (I : (m : ℕ) → Finset (↑(E.I (C := C) (D := D) m) : Type u_1)),
    MapsTo (↑(map (C := C) (D := D) n (↑i : cell C n)) : (Fin n → ℝ) → X) (sphere 0 1)
      (D ∪
        ⋃ (m : ℕ),
          ⋃ (_ : m < n), ⋃ j ∈ I m, (↑(map (C := C) (D := D) m (↑j : cell C m)) : (Fin m → ℝ) → X) '' closedBall 0 1)

Tactic:
rcases cellFrontier_subset_finite_openCell (C := C) n i with ⟨J, hJ⟩

Premises used: Topology.RelCWComplex.cellFrontier_subset_finite_openCell
-- Module: Mathlib.Topology.CWComplex.Classical.Subcomplex
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : T2Space X
inst_1 : RelCWComplex C D
E : Subcomplex C (D := D)
n : ℕ
i : (↑(E.I (C := C) (D := D) n) : Type u_1)
J : (m : ℕ) → Finset (@cell _ t C D _ m)
hJ :
  cellFrontier (C := C) (D := D) n (↑i : cell C n) ⊆
    D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ J m, openCell (C := C) (D := D) m j
h :
  MapsTo (↑(map (C := C) (D := D) n (↑i : cell C n)) : (Fin n → ℝ) → X) (sphere 0 1)
    (D ∪
      ⋃ (m : ℕ),
        ⋃ (_ : m < n),
          ⋃ (j : (↑(E.I (C := C) (D := D) m) : Type u_1)),
            ⋃ (_ :
              Membership.mem (γ := Finset (↑(E.I (C := C) (D := D) m) : Type u_1))
                ((fun (m : ℕ) ↦
                    ((J m).preimage (Subtype.val (p := fun (x : @cell _ t C D _ m) ↦ x ∈ E.I (C := C) (D := D) m)) ⋯ :
                      Finset (↑(E.I (C := C) (D := D) m) : Type u_1)))
                  m)
                j),
              (↑(map (C := C) (D := D) m (↑j : cell C m)) : (Fin m → ℝ) → X) '' closedBall 0 1)
⊢ ∃ (I : (m : ℕ) → Finset (↑(E.I (C := C) (D := D) m) : Type u_1)),
    MapsTo (↑(map (C := C) (D := D) n (↑i : cell C n)) : (Fin n → ℝ) → X) (sphere 0 1)
      (D ∪
        ⋃ (m : ℕ),
          ⋃ (_ : m < n), ⋃ j ∈ I m, (↑(map (C := C) (D := D) m (↑j : cell C m)) : (Fin m → ℝ) → X) '' closedBall 0 1)

Tactic:
use fun m ↦ Finset.preimage (J m) Subtype.val Subtype.val_injective.injOn

Premises used: Subtype.val_injective, Function.Injective.injOn, Finset.preimage, Subtype.val
-- Module: Mathlib.Topology.CWComplex.Classical.Subcomplex
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : T2Space X
inst_1 : RelCWComplex C D
E : Subcomplex C (D := D)
n : ℕ
i : (↑(E.I (C := C) (D := D) n) : Type u_1)
J : (m : ℕ) → Finset (@cell _ t C D _ m)
hJ :
  cellFrontier (C := C) (D := D) n (↑i : cell C n) ⊆
    D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ J m, openCell (C := C) (D := D) m j
h :
  (↑(map (C := C) (D := D) n (↑i : cell C n)) : (Fin n → ℝ) → X) '' sphere 0 1 ⊆
    D ∪
      ⋃ (m : ℕ),
        ⋃ (_ : m < n),
          ⋃ (j : (↑(E.I (C := C) (D := D) m) : Type u_1)),
            ⋃ (_ :
              Membership.mem (γ := Finset (↑(E.I (C := C) (D := D) m) : Type u_1))
                ((fun (m : ℕ) ↦
                    ((J m).preimage (Subtype.val (p := fun (x : @cell _ t C D _ m) ↦ x ∈ E.I (C := C) (D := D) m)) ⋯ :
                      Finset (↑(E.I (C := C) (D := D) m) : Type u_1)))
                  m)
                j),
              (↑(map (C := C) (D := D) m (↑j : cell C m)) : (Fin m → ℝ) → X) '' closedBall 0 1
⊢ MapsTo (↑(map (C := C) (D := D) n (↑i : cell C n)) : (Fin n → ℝ) → X) (sphere 0 1)
    (D ∪
      ⋃ (m : ℕ),
        ⋃ (_ : m < n),
          ⋃ (j : (↑(E.I (C := C) (D := D) m) : Type u_1)),
            ⋃ (_ :
              Membership.mem (γ := Finset (↑(E.I (C := C) (D := D) m) : Type u_1))
                ((fun (m : ℕ) ↦
                    ((J m).preimage (Subtype.val (p := fun (x : @cell _ t C D _ m) ↦ x ∈ E.I (C := C) (D := D) m)) ⋯ :
                      Finset (↑(E.I (C := C) (D := D) m) : Type u_1)))
                  m)
                j),
              (↑(map (C := C) (D := D) m (↑j : cell C m)) : (Fin m → ℝ) → X) '' closedBall 0 1)

Tactic:
rw [mapsTo_iff_image_subset]

Premises used: Set.mapsTo_iff_image_subset
-- Module: Mathlib.Topology.CWComplex.Classical.Subcomplex
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : T2Space X
inst_1 : RelCWComplex C D
E : Subcomplex C (D := D)
n : ℕ
i : (↑(E.I (C := C) (D := D) n) : Type u_1)
J : (m : ℕ) → Finset (@cell _ t C D _ m)
hJ :
  cellFrontier (C := C) (D := D) n (↑i : cell C n) ⊆
    D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ J m, openCell (C := C) (D := D) m j
x : X
hx : x ∈ (↑(map (C := C) (D := D) n (↑i : cell C n)) : (Fin n → ℝ) → X) '' sphere 0 1
⊢ x ∈ D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ J m, openCell (C := C) (D := D) m j

Tactic:
specialize hJ hx
-- Module: Mathlib.Topology.CWComplex.Classical.Subcomplex
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : T2Space X
inst_1 : RelCWComplex C D
E : Subcomplex C (D := D)
n : ℕ
i : (↑(E.I (C := C) (D := D) n) : Type u_1)
J : (m : ℕ) → Finset (@cell _ t C D _ m)
x : X
hx : x ∈ (↑(map (C := C) (D := D) n (↑i : cell C n)) : (Fin n → ℝ) → X) '' sphere 0 1
hJ : x ∈ D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ J m, openCell (C := C) (D := D) m j
h :
  ∀ (hJ : x ∉ D → ∃ i < n, ∃ i_1 ∈ J i, x ∈ openCell (C := C) (D := D) i i_1),
    x ∉ D →
      ∃ i < n,
        ∃ i_1 ∈ E.I (C := C) (D := D) i,
          i_1 ∈ J i ∧
            Membership.mem (γ := Set X)
              ((fun (a : Fin i → ℝ) ↦ (↑(map (C := C) (D := D) i i_1) : (Fin i → ℝ) → X) a) '' closedBall 0 1) x
⊢ x ∈
    D ∪
      ⋃ (m : ℕ),
        ⋃ (_ : m < n),
          ⋃ (j : (↑(E.I (C := C) (D := D) m) : Type u_1)),
            ⋃ (_ :
              Membership.mem (γ := Finset (↑(E.I (C := C) (D := D) m) : Type u_1))
                ((fun (m : ℕ) ↦
                    ((J m).preimage (Subtype.val (p := fun (x : @cell _ t C D _ m) ↦ x ∈ E.I (C := C) (D := D) m)) ⋯ :
                      Finset (↑(E.I (C := C) (D := D) m) : Type u_1)))
                  m)
                j),
              (↑(map (C := C) (D := D) m (↑j : cell C m)) : (Fin m → ℝ) → X) '' closedBall 0 1

Tactic:
simp_rw [iUnion_coe_set, mem_union, mem_iUnion, Finset.mem_preimage, exists_prop,
      Decidable.or_iff_not_imp_left] at hJ ⊢

Premises used: Set.mem_union, Decidable.or_iff_not_imp_left, Set.mem_iUnion, Set.iUnion_coe_set, exists_prop, Finset.mem_preimage
-- Module: Mathlib.Topology.CWComplex.Classical.Subcomplex
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : T2Space X
inst_1 : RelCWComplex C D
E : Subcomplex C (D := D)
n : ℕ
i : (↑(E.I (C := C) (D := D) n) : Type u_1)
J : (m : ℕ) → Finset (@cell _ t C D _ m)
x : X
hx : x ∈ (↑(map (C := C) (D := D) n (↑i : cell C n)) : (Fin n → ℝ) → X) '' sphere 0 1
hJ : x ∉ D → ∃ i < n, ∃ i_1 ∈ J i, x ∈ openCell (C := C) (D := D) i i_1
h : x ∉ D
⊢ ∃ i < n, ∃ i_1 ∈ J i, x ∈ openCell (C := C) (D := D) i i_1

Tactic:
specialize hJ h
-- Module: Mathlib.Topology.CWComplex.Classical.Subcomplex
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : T2Space X
inst_1 : RelCWComplex C D
E : Subcomplex C (D := D)
n : ℕ
i : (↑(E.I (C := C) (D := D) n) : Type u_1)
J : (m : ℕ) → Finset (@cell _ t C D _ m)
x : X
hx : x ∈ (↑(map (C := C) (D := D) n (↑i : cell C n)) : (Fin n → ℝ) → X) '' sphere 0 1
h : x ∉ D
hJ : ∃ i < n, ∃ i_1 ∈ J i, x ∈ openCell (C := C) (D := D) i i_1
h₁ :
  ∀ (m : ℕ) (hmn : m < n) (j : @cell _ t C D _ m) (hj : j ∈ J m) (hxj : x ∈ openCell (C := C) (D := D) m j),
    ∃ i < n,
      ∃ i_1 ∈ E.I (C := C) (D := D) i,
        i_1 ∈ J i ∧
          Membership.mem (γ := Set X)
            ((fun (a : Fin i → ℝ) ↦ (↑(map (C := C) (D := D) i i_1) : (Fin i → ℝ) → X) a) '' closedBall 0 1) x
⊢ ∃ i < n,
    ∃ i_1 ∈ E.I (C := C) (D := D) i,
      i_1 ∈ J i ∧
        Membership.mem (γ := Set X)
          ((fun (a : Fin i → ℝ) ↦ (↑(map (C := C) (D := D) i i_1) : (Fin i → ℝ) → X) a) '' closedBall 0 1) x

Tactic:
obtain ⟨m, hmn, j, hj, hxj⟩ := hJ
-- Module: Mathlib.Topology.CWComplex.Classical.Subcomplex
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : T2Space X
inst_1 : RelCWComplex C D
E : Subcomplex C (D := D)
n : ℕ
i : (↑(E.I (C := C) (D := D) n) : Type u_1)
J : (m : ℕ) → Finset (@cell _ t C D _ m)
x : X
hx : x ∈ (↑(map (C := C) (D := D) n (↑i : cell C n)) : (Fin n → ℝ) → X) '' sphere 0 1
h : x ∉ D
m : ℕ
hmn : m < n
j : @cell _ t C D _ m
hj : j ∈ J m
hxj : x ∈ openCell (C := C) (D := D) m j
h₁ : j ∈ E.I (C := C) (D := D) m
⊢ ∃ i < n,
    ∃ i_1 ∈ E.I (C := C) (D := D) i,
      i_1 ∈ J i ∧
        Membership.mem (γ := Set X)
          ((fun (a : Fin i → ℝ) ↦ (↑(map (C := C) (D := D) i i_1) : (Fin i → ℝ) → X) a) '' closedBall 0 1) x

Tactic:
suffices j ∈ E.I m from ⟨m, hmn, j, this, hj, openCell_subset_closedCell _ _ hxj⟩
-- Module: Mathlib.Topology.CWComplex.Classical.Subcomplex
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : T2Space X
inst_1 : RelCWComplex C D
E : Subcomplex C (D := D)
n : ℕ
i : (↑(E.I (C := C) (D := D) n) : Type u_1)
J : (m : ℕ) → Finset (@cell _ t C D _ m)
x : X
hx : x ∈ (↑(map (C := C) (D := D) n (↑i : cell C n)) : (Fin n → ℝ) → X) '' sphere 0 1
h : x ∉ D
m : ℕ
hmn : m < n
j : @cell _ t C D _ m
hj : j ∈ J m
hxj : x ∈ openCell (C := C) (D := D) m j
⊢ x ∈ (↑E : Set X)

Tactic:
have : x ∈ (E : Set X) := E.cellFrontier_subset_of_mem i.2 hx
-- Module: Mathlib.Topology.CWComplex.Classical.Subcomplex
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : T2Space X
inst_1 : RelCWComplex C D
E : Subcomplex C (D := D)
n : ℕ
i : (↑(E.I (C := C) (D := D) n) : Type u_1)
J : (m : ℕ) → Finset (@cell _ t C D _ m)
x : X
hx : x ∈ (↑(map (C := C) (D := D) n (↑i : cell C n)) : (Fin n → ℝ) → X) '' sphere 0 1
h : x ∉ D
m : ℕ
hmn : m < n
j : @cell _ t C D _ m
hj : j ∈ J m
hxj : x ∈ openCell (C := C) (D := D) m j
this : x ∈ (↑E : Set X)
h₁ : ∀ (hj' : ¬j ∈ E.I (C := C) (D := D) m), False
⊢ j ∈ E.I (C := C) (D := D) m

Tactic:
by_contra hj'
-- Module: Mathlib.Topology.CWComplex.Classical.Subcomplex
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : T2Space X
inst_1 : RelCWComplex C D
E : Subcomplex C (D := D)
n : ℕ
i : (↑(E.I (C := C) (D := D) n) : Type u_1)
J : (m : ℕ) → Finset (@cell _ t C D _ m)
x : X
hx : x ∈ (↑(map (C := C) (D := D) n (↑i : cell C n)) : (Fin n → ℝ) → X) '' sphere 0 1
h : x ∉ D
m : ℕ
hmn : m < n
j : @cell _ t C D _ m
hj : j ∈ J m
hxj : x ∈ openCell (C := C) (D := D) m j
this : x ∈ (↑E : Set X)
hj' : ¬j ∈ E.I (C := C) (D := D) m
⊢ False

Tactic:
E.disjoint_openCell_subcomplex_of_not_mem hj' |>.notMem_of_mem_left hxj this

Premises used: Disjoint.notMem_of_mem_left, Topology.RelCWComplex.Subcomplex.disjoint_openCell_subcomplex_of_not_mem
-- Module: Mathlib.Topology.CWComplex.Classical.Subcomplex
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : T2Space X
inst_1 : RelCWComplex C D
E : Subcomplex C (D := D)
n : ℕ
i : (↑(E.I (C := C) (D := D) n) : Type u_1)
J : (m : ℕ) → Finset (@cell _ t C D _ m)
x : X
hx : x ∈ (↑(map (C := C) (D := D) n (↑i : cell C n)) : (Fin n → ℝ) → X) '' sphere 0 1
h : x ∉ D
m : ℕ
hmn : m < n
j : @cell _ t C D _ m
hj : j ∈ J m
hxj : x ∈ openCell (C := C) (D := D) m j
this : x ∈ (↑E : Set X)
hj' : ¬j ∈ E.I (C := C) (D := D) m
⊢ False

Tactic:
exact E.disjoint_openCell_subcomplex_of_not_mem hj' |>.notMem_of_mem_left hxj this

Premises used: Disjoint.notMem_of_mem_left, Topology.RelCWComplex.Subcomplex.disjoint_openCell_subcomplex_of_not_mem
-- Module: Mathlib.Topology.CWComplex.Classical.Subcomplex
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : T2Space X
inst_1 : RelCWComplex C D
E : Subcomplex C (D := D)
A : Set X
hA : A ⊆ (↑E : Set X)
h :
  (∀ (n : ℕ) (j : (↑(E.I (C := C) (D := D) n) : Type u_1)),
      IsClosed[t] (A ∩ (↑(map (C := C) (D := D) n (↑j : cell C n)) : (Fin n → ℝ) → X) '' closedBall 0 1)) ∧
    IsClosed[t] (A ∩ D)
apply :
  ∀ (n : ℕ),
    0 < n →
      ∀ (j : @cell _ t C D _ n),
        Disjoint A (openCell (C := C) (D := D) n j) ∨ IsClosed[t] (A ∩ closedCell (C := C) (D := D) n j)
⊢ IsClosed[t] A

Tactic:
apply isClosed_of_disjoint_openCell_or_isClosed_inter_closedCell
      (subset_trans hA (subset_complex (C := C) E)) h.2

Premises used: subset_trans, Topology.RelCWComplex.Subcomplex.subset_complex, Topology.RelCWComplex.isClosed_of_disjoint_openCell_or_isClosed_inter_closedCell, And.right
-- Module: Mathlib.Topology.CWComplex.Classical.Subcomplex
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : T2Space X
inst_1 : RelCWComplex C D
E : Subcomplex C (D := D)
A : Set X
hA : A ⊆ (↑E : Set X)
h :
  (∀ (n : ℕ) (j : (↑(E.I (C := C) (D := D) n) : Type u_1)),
      IsClosed[t] (A ∩ (↑(map (C := C) (D := D) n (↑j : cell C n)) : (Fin n → ℝ) → X) '' closedBall 0 1)) ∧
    IsClosed[t] (A ∩ D)
n : ℕ
_ :
  0 < n →
    ∀ (j : @cell _ t C D _ n),
      Disjoint A (openCell (C := C) (D := D) n j) ∨ IsClosed[t] (A ∩ closedCell (C := C) (D := D) n j)
⊢ 0 < n →
    ∀ (j : @cell _ t C D _ n),
      Disjoint A (openCell (C := C) (D := D) n j) ∨ IsClosed[t] (A ∩ closedCell (C := C) (D := D) n j)

Tactic:
_