awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Graph (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
C : Set X
inst_1 : CWComplex C
e : @cell _ inst C ∅ _ 1
x y : @cell _ inst C ∅ _ 0
rw :
  cellFrontier (C := C) (D := ∅) 1 e = closedCell (C := C) (D := ∅) 0 x ∪ closedCell (C := C) (D := ∅) 0 y ↔
    cellFrontier (C := C) (D := ∅) 1 e =
      {(↑(map (C := C) (D := ∅) 0 x) : (Fin 0 → ℝ) → X) ![], (↑(map (C := C) (D := ∅) 0 y) : (Fin 0 → ℝ) → X) ![]}
⊢ IsLink (OneSkeletonGraph C) e x y ↔
    cellFrontier (C := C) (D := ∅) 1 e =
      {(↑(map (C := C) (D := ∅) 0 x) : (Fin 0 → ℝ) → X) ![], (↑(map (C := C) (D := ∅) 0 y) : (Fin 0 → ℝ) → X) ![]}
have rw₁ : cellFrontier (C := C) (D := ∅) 1 e =
    {(↑(map (C := C) (D := ∅) 0 x) : (Fin 0 → ℝ) → X) ![]} ∪ closedCell (C := C) (D := ∅) 0 y ↔
  cellFrontier (C := C) (D := ∅) 1 e =
    {(↑(map (C := C) (D := ∅) 0 x) : (Fin 0 → ℝ) → X) ![], (↑(map (C := C) (D := ∅) 0 y) : (Fin 0 → ℝ) → X) ![]}
Tactic: rw [OneSkeletonGraph_isLink, closedCell_zero_eq_singleton, closedCell_zero_eq_singleton,
    singleton_union]
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Graph (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
C : Set X
inst_1 : CWComplex C
e : @cell _ inst C ∅ _ 1
x y : @cell _ inst C ∅ _ 0
rw :
  cellFrontier (C := C) (D := ∅) 1 e = closedCell (C := C) (D := ∅) 0 x ∪ closedCell (C := C) (D := ∅) 0 y ↔
    cellFrontier (C := C) (D := ∅) 1 e =
      {(↑(map (C := C) (D := ∅) 0 x) : (Fin 0 → ℝ) → X) ![], (↑(map (C := C) (D := ∅) 0 y) : (Fin 0 → ℝ) → X) ![]}
rw₁ :
  cellFrontier (C := C) (D := ∅) 1 e =
      {(↑(map (C := C) (D := ∅) 0 x) : (Fin 0 → ℝ) → X) ![]} ∪ closedCell (C := C) (D := ∅) 0 y ↔
    cellFrontier (C := C) (D := ∅) 1 e =
      {(↑(map (C := C) (D := ∅) 0 x) : (Fin 0 → ℝ) → X) ![], (↑(map (C := C) (D := ∅) 0 y) : (Fin 0 → ℝ) → X) ![]}
⊢ IsLink (OneSkeletonGraph C) e x y ↔
    cellFrontier (C := C) (D := ∅) 1 e =
      {(↑(map (C := C) (D := ∅) 0 x) : (Fin 0 → ℝ) → X) ![], (↑(map (C := C) (D := ∅) 0 y) : (Fin 0 → ℝ) → X) ![]}
have rw₂ : cellFrontier (C := C) (D := ∅) 1 e =
    {(↑(map (C := C) (D := ∅) 0 x) : (Fin 0 → ℝ) → X) ![]} ∪ {(↑(map (C := C) (D := ∅) 0 y) : (Fin 0 → ℝ) → X) ![]} ↔
  cellFrontier (C := C) (D := ∅) 1 e =
    {(↑(map (C := C) (D := ∅) 0 x) : (Fin 0 → ℝ) → X) ![], (↑(map (C := C) (D := ∅) 0 y) : (Fin 0 → ℝ) → X) ![]}
Tactic: rw [OneSkeletonGraph_isLink, closedCell_zero_eq_singleton, closedCell_zero_eq_singleton,
    singleton_union]
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Graph (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
C : Set X
inst_1 : CWComplex C
e : @cell _ inst C ∅ _ 1
x y : @cell _ inst C ∅ _ 0
rw :
  cellFrontier (C := C) (D := ∅) 1 e = closedCell (C := C) (D := ∅) 0 x ∪ closedCell (C := C) (D := ∅) 0 y ↔
    cellFrontier (C := C) (D := ∅) 1 e =
      {(↑(map (C := C) (D := ∅) 0 x) : (Fin 0 → ℝ) → X) ![], (↑(map (C := C) (D := ∅) 0 y) : (Fin 0 → ℝ) → X) ![]}
rw₁ :
  cellFrontier (C := C) (D := ∅) 1 e =
      {(↑(map (C := C) (D := ∅) 0 x) : (Fin 0 → ℝ) → X) ![]} ∪ closedCell (C := C) (D := ∅) 0 y ↔
    cellFrontier (C := C) (D := ∅) 1 e =
      {(↑(map (C := C) (D := ∅) 0 x) : (Fin 0 → ℝ) → X) ![], (↑(map (C := C) (D := ∅) 0 y) : (Fin 0 → ℝ) → X) ![]}
rw₂ :
  cellFrontier (C := C) (D := ∅) 1 e =
      {(↑(map (C := C) (D := ∅) 0 x) : (Fin 0 → ℝ) → X) ![]} ∪ {(↑(map (C := C) (D := ∅) 0 y) : (Fin 0 → ℝ) → X) ![]} ↔
    cellFrontier (C := C) (D := ∅) 1 e =
      {(↑(map (C := C) (D := ∅) 0 x) : (Fin 0 → ℝ) → X) ![], (↑(map (C := C) (D := ∅) 0 y) : (Fin 0 → ℝ) → X) ![]}
⊢ IsLink (OneSkeletonGraph C) e x y ↔
    cellFrontier (C := C) (D := ∅) 1 e =
      {(↑(map (C := C) (D := ∅) 0 x) : (Fin 0 → ℝ) → X) ![], (↑(map (C := C) (D := ∅) 0 y) : (Fin 0 → ℝ) → X) ![]}
have rw₃ : cellFrontier (C := C) (D := ∅) 1 e =
    {(↑(map (C := C) (D := ∅) 0 x) : (Fin 0 → ℝ) → X) ![], (↑(map (C := C) (D := ∅) 0 y) : (Fin 0 → ℝ) → X) ![]} ↔
  cellFrontier (C := C) (D := ∅) 1 e =
    {(↑(map (C := C) (D := ∅) 0 x) : (Fin 0 → ℝ) → X) ![], (↑(map (C := C) (D := ∅) 0 y) : (Fin 0 → ℝ) → X) ![]}
Tactic: rw [OneSkeletonGraph_isLink, closedCell_zero_eq_singleton, closedCell_zero_eq_singleton,
    singleton_union]
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Graph (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
C : Set X
inst_1 : CWComplex C
e : @cell _ inst C ∅ _ 1
⊢ (∃ (x : @cell _ inst C ∅ _ 0), IsLoopAt (OneSkeletonGraph C) e x) ↔
    ∃ (x : @cell _ inst C ∅ _ 0), cellFrontier (C := C) (D := ∅) 1 e = closedCell (C := C) (D := ∅) 0 x
have refine : ∀ (x : @cell _ inst C ∅ _ 0),
  IsLoopAt (OneSkeletonGraph C) e x ↔ cellFrontier (C := C) (D := ∅) 1 e = closedCell (C := C) (D := ∅) 0 x
Tactic: refine exists_congr fun x ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Graph (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
C : Set X
inst_1 : CWComplex C
e : @cell _ inst C ∅ _ 1
x : @cell _ inst C ∅ _ 0
⊢ cellFrontier (C := C) (D := ∅) 1 e = closedCell (C := C) (D := ∅) 0 x ∪ closedCell (C := C) (D := ∅) 0 x ↔
    cellFrontier (C := C) (D := ∅) 1 e = closedCell (C := C) (D := ∅) 0 x
have rw : cellFrontier (C := C) (D := ∅) 1 e = closedCell (C := C) (D := ∅) 0 x ↔
  cellFrontier (C := C) (D := ∅) 1 e = closedCell (C := C) (D := ∅) 0 x
Tactic: rw [union_self]
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Graph (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
C : Set X
inst_1 : CWComplex C
e : @cell _ inst C ∅ _ 1
⊢ (∃ (x : @cell _ inst C ∅ _ 0), IsLoopAt (OneSkeletonGraph C) e x) ↔ (cellFrontier (C := C) (D := ∅) 1 e).Subsingleton
have rw : (∃ (x : @cell _ inst C ∅ _ 0), cellFrontier (C := C) (D := ∅) 1 e = closedCell (C := C) (D := ∅) 0 x) ↔
  (cellFrontier (C := C) (D := ∅) 1 e).Subsingleton
Tactic: rw [exists_isLoopAt_iff]
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Graph (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
C : Set X
inst_1 : CWComplex C
e : @cell _ inst C ∅ _ 1
⊢ (∃ (x : @cell _ inst C ∅ _ 0), cellFrontier (C := C) (D := ∅) 1 e = closedCell (C := C) (D := ∅) 0 x) ↔
    (cellFrontier (C := C) (D := ∅) 1 e).Subsingleton
have refine : ∀ (h : (cellFrontier (C := C) (D := ∅) 1 e).Subsingleton),
  ∃ (x : @cell _ inst C ∅ _ 0), cellFrontier (C := C) (D := ∅) 1 e = closedCell (C := C) (D := ∅) 0 x
Tactic: refine ⟨fun ⟨x, hx⟩ => by simp [closedCell_zero_eq_singleton, hx], fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Graph (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
C : Set X
inst_1 : CWComplex C
e : @cell _ inst C ∅ _ 1
h : (cellFrontier (C := C) (D := ∅) 1 e).Subsingleton
⊢ ∃ (x : @cell _ inst C ∅ _ 0), cellFrontier (C := C) (D := ∅) 1 e = closedCell (C := C) (D := ∅) 0 x
have obtain : ∀ (x y : @cell _ inst C ∅ _ 0)
  (hxy : cellFrontier (C := C) (D := ∅) 1 e = closedCell (C := C) (D := ∅) 0 x ∪ closedCell (C := C) (D := ∅) 0 y),
  ∃ (x : @cell _ inst C ∅ _ 0), cellFrontier (C := C) (D := ∅) 1 e = closedCell (C := C) (D := ∅) 0 x
Tactic: obtain ⟨x, y, hxy⟩ := exists_cellFrontier_one_eq e
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Graph (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
C : Set X
inst_1 : CWComplex C
e : @cell _ inst C ∅ _ 1
h : (cellFrontier (C := C) (D := ∅) 1 e).Subsingleton
x y : @cell _ inst C ∅ _ 0
hxy : cellFrontier (C := C) (D := ∅) 1 e = closedCell (C := C) (D := ∅) 0 x ∪ closedCell (C := C) (D := ∅) 0 y
⊢ ∃ (x : @cell _ inst C ∅ _ 0), cellFrontier (C := C) (D := ∅) 1 e = closedCell (C := C) (D := ∅) 0 x
have hxy₁ : cellFrontier (C := C) (D := ∅) 1 e =
  {(↑(map (C := C) (D := ∅) 0 y) : (Fin 0 → ℝ) → X) ![], (↑(map (C := C) (D := ∅) 0 x) : (Fin 0 → ℝ) → X) ![]}
Tactic: simp only [closedCell_zero_eq_singleton, union_singleton] at hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Graph (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
C : Set X
inst_1 : CWComplex C
e : @cell _ inst C ∅ _ 1
h : (cellFrontier (C := C) (D := ∅) 1 e).Subsingleton
x y : @cell _ inst C ∅ _ 0
hxy :
  cellFrontier (C := C) (D := ∅) 1 e =
    {(↑(map (C := C) (D := ∅) 0 y) : (Fin 0 → ℝ) → X) ![], (↑(map (C := C) (D := ∅) 0 x) : (Fin 0 → ℝ) → X) ![]}
⊢ ∃ (x : @cell _ inst C ∅ _ 0), cellFrontier (C := C) (D := ∅) 1 e = closedCell (C := C) (D := ∅) 0 x
have hxy₁ : cellFrontier (C := C) (D := ∅) 1 e =
  {(↑(map (C := C) (D := ∅) 0 x) : (Fin 0 → ℝ) → X) ![], (↑(map (C := C) (D := ∅) 0 x) : (Fin 0 → ℝ) → X) ![]}
Tactic: obtain rfl : x = y := RelCWComplex.injective_map_zero C <| (hxy ▸ h) (by simp) (by simp)
Cleared hypotheses: y, hxy
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Subcomplex (goal)
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 : @cell _ t C D _ n
hi : i ∈ E.I (C := C) (D := D) n
⊢ closedCell (C := C) (D := D) n i ⊆ (↑E : Set X)
have rw : openCell (C := C) (D := D) n i ⊆
  D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(E.I (C := C) (D := D) n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n)
Tactic: rw [← closure_openCell_eq_closedCell, E.closed.closure_subset_iff, ← E.union]
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Subcomplex (goal)
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 : @cell _ t C D _ n
hi : i ∈ E.I (C := C) (D := D) n
⊢ openCell (C := C) (D := D) n i ⊆
    D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(E.I (C := C) (D := D) n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n)
have h : openCell (C := C) (D := D) n i ⊆
  ⋃ (n : ℕ), ⋃ (j : (↑(E.I (C := C) (D := D) n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n)
Tactic: apply subset_union_of_subset_right
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Subcomplex (goal)
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)
⊢ D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(E.I (C := C) (D := D) n) : Type u_1)), closedCell (C := C) (D := D) n (↑j : cell C n) =
    (↑E : Set X)
have a : D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(E.I (C := C) (D := D) n) : Type u_1)), closedCell (C := C) (D := D) n (↑j : cell C n) ⊆
  (↑E : Set X)
Tactic: apply subset_antisymm
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Subcomplex (goal)
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 :
  D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(E.I (C := C) (D := D) n) : Type u_1)), closedCell (C := C) (D := D) n (↑j : cell C n) ⊆
    (↑E : Set X)
⊢ D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(E.I (C := C) (D := D) n) : Type u_1)), closedCell (C := C) (D := D) n (↑j : cell C n) =
    (↑E : Set X)
have a₁ : (↑E : Set X) ⊆
  D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(E.I (C := C) (D := D) n) : Type u_1)), closedCell (C := C) (D := D) n (↑j : cell C n)
Tactic: apply subset_antisymm
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Subcomplex (goal)
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)
⊢ D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(E.I (C := C) (D := D) n) : Type u_1)), closedCell (C := C) (D := D) n (↑j : cell C n) ⊆
    (↑E : Set X)
have a : ⋃ (n : ℕ), ⋃ (j : (↑(E.I (C := C) (D := D) n) : Type u_1)), closedCell (C := C) (D := D) n (↑j : cell C n) ⊆
  (↑E : Set X)
Tactic: apply union_subset E.base_subset
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Subcomplex (goal)
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)
⊢ (↑E : Set X) ⊆
    D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(E.I (C := C) (D := D) n) : Type u_1)), closedCell (C := C) (D := D) n (↑j : cell C n)
have a : D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(E.I (C := C) (D := D) n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n) ⊆
  D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(E.I (C := C) (D := D) n) : Type u_1)), closedCell (C := C) (D := D) n (↑j : cell C n)
Tactic: rw [← E.union]
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Subcomplex (goal)
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)
⊢ D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(E.I (C := C) (D := D) n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n) ⊆
    D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(E.I (C := C) (D := D) n) : Type u_1)), closedCell (C := C) (D := D) n (↑j : cell C n)
have a : Subset.{u_1} (α := Set X)
  (⋃ (n : ℕ), ⋃ (j : (↑(E.I (C := C) (D := D) n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n))
  (⋃ (n : ℕ), ⋃ (j : (↑(E.I (C := C) (D := D) n) : Type u_1)), closedCell (C := C) (D := D) n (↑j : cell C n))
Tactic: apply union_subset_union_right
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Subcomplex (goal)
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)
⊢ Subset.{u_1} (α := Set X)
    (⋃ (n : ℕ), ⋃ (j : (↑(E.I (C := C) (D := D) n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n))
    (⋃ (n : ℕ), ⋃ (j : (↑(E.I (C := C) (D := D) n) : Type u_1)), closedCell (C := C) (D := D) n (↑j : cell C n))
have apply : ∀ (n : ℕ) (i : (↑(E.I (C := C) (D := D) n) : Type u_1)),
  openCell (C := C) (D := D) n (↑i : cell C n) ⊆ closedCell (C := C) (D := D) n (↑i : cell C n)
Tactic: apply iUnion₂_mono fun n i ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Subcomplex (goal)
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
E : Subcomplex C (D := D)
n : ℕ
i : @cell _ t C D _ n
h : i ∉ E.I (C := C) (D := D) n
⊢ Disjoint (openCell (C := C) (D := D) n i) (↑E : Set X)
have simp_rw : Disjoint (openCell (C := C) (D := D) n i) D ∧
  ∀ (i_1 : ℕ) (i_2 : (↑(E.I (C := C) (D := D) i_1) : Type u_1)),
    Disjoint (openCell (C := C) (D := D) n i) (openCell (C := C) (D := D) i_1 (↑i_2 : cell C i_1))
Tactic: simp_rw [← union, disjoint_union_right, disjoint_iUnion_right]
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Subcomplex (goal)
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)
⊢ ∀ ⦃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
have 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)
Tactic: ⟨m, j⟩
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Subcomplex (goal)
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)
have 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)
Tactic: refine @pairwiseDisjoint' _ _ C D _ ⟨n, i⟩ trivial ⟨m, j⟩ trivial ?_
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Subcomplex (goal)
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)
⊢ ∃ (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)
have 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)
Tactic: rcases cellFrontier_subset_finite_openCell (C := C) n i with ⟨J, hJ⟩
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Subcomplex (goal)
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
⊢ ∃ (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)
have 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)) sorry :
                    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: use fun m ↦ Finset.preimage (J m) Subtype.val Subtype.val_injective.injOn
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Subcomplex (goal)
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
⊢ 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)
have 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)) sorry :
                    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]
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Subcomplex (hypothesis)
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 : (↑(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
have hJ₁ : x ∈ D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ J m, openCell (C := C) (D := D) m j
Tactic: specialize hJ hx
Cleared hypotheses: hJ