awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.CWComplex.Classical.Graph
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) (y : @cell _ inst C ∅ _ 0),
    cellFrontier (C := C) (D := ∅) 1 e = closedCell (C := C) (D := ∅) 0 x ∪ closedCell (C := C) (D := ∅) 0 y

Tactic:
exists_cellFrontier_one_eq e

Premises used: Topology.CWComplex.exists_cellFrontier_one_eq
-- Module: Mathlib.Topology.CWComplex.Classical.Graph
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) (y : @cell _ inst C ∅ _ 0),
    cellFrontier (C := C) (D := ∅) 1 e = closedCell (C := C) (D := ∅) 0 x ∪ closedCell (C := C) (D := ∅) 0 y

Tactic:
exact exists_cellFrontier_one_eq e

Premises used: Topology.CWComplex.exists_cellFrontier_one_eq
-- Module: Mathlib.Topology.CWComplex.Classical.Graph
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) ![]}
rw₃ 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) ![]}

Tactic:
rw [OneSkeletonGraph_isLink, closedCell_zero_eq_singleton, closedCell_zero_eq_singleton,
    singleton_union]

Premises used: Topology.CWComplex.OneSkeletonGraph_isLink, Set.singleton_union, Topology.RelCWComplex.closedCell_zero_eq_singleton
-- Module: Mathlib.Topology.CWComplex.Classical.Graph
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

Tactic:
exists_congr fun x ↦ ?_

Premises used: exists_congr
-- Module: Mathlib.Topology.CWComplex.Classical.Graph
Goal:
X : Type u_1
inst : TopologicalSpace X
C : Set X
inst_1 : CWComplex C
e : @cell _ inst C ∅ _ 1
refine :
  ∀ (x : @cell _ inst C ∅ _ 0),
    IsLoopAt (OneSkeletonGraph C) e x ↔ cellFrontier (C := C) (D := ∅) 1 e = closedCell (C := C) (D := ∅) 0 x
⊢ (∃ (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

Tactic:
refine exists_congr fun x ↦ ?_

Premises used: exists_congr
-- Module: Mathlib.Topology.CWComplex.Classical.Graph
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
rw 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
⊢ 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

Tactic:
rw [union_self]

Premises used: Set.union_self
-- Module: Mathlib.Topology.CWComplex.Classical.Graph
Goal:
X : Type u_1
inst : TopologicalSpace X
C : Set X
inst_1 : CWComplex C
e : @cell _ inst C ∅ _ 1
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
⊢ (∃ (x : @cell _ inst C ∅ _ 0), IsLoopAt (OneSkeletonGraph C) e x) ↔ (cellFrontier (C := C) (D := ∅) 1 e).Subsingleton

Tactic:
rw [exists_isLoopAt_iff]

Premises used: Topology.CWComplex.OneSkeletonGraph.exists_isLoopAt_iff
-- Module: Mathlib.Topology.CWComplex.Classical.Graph
Goal:
X : Type u_1
inst : TopologicalSpace X
C : Set X
inst_1 : CWComplex C
e : @cell _ inst C ∅ _ 1
h : ∃ (x : @cell _ inst C ∅ _ 0), cellFrontier (C := C) (D := ∅) 1 e = closedCell (C := C) (D := ∅) 0 x
x : @cell _ inst C ∅ _ 0
hx : cellFrontier (C := C) (D := ∅) 1 e = closedCell (C := C) (D := ∅) 0 x
⊢ (cellFrontier (C := C) (D := ∅) 1 e).Subsingleton

Tactic:
simp [closedCell_zero_eq_singleton, hx]

Premises used: Topology.RelCWComplex.closedCell_zero_eq_singleton
-- Module: Mathlib.Topology.CWComplex.Classical.Graph
Goal:
X : Type u_1
inst : TopologicalSpace X
C : Set X
inst_1 : CWComplex C
e : @cell _ inst C ∅ _ 1
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
⊢ (∃ (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:
refine ⟨fun ⟨x, hx⟩ => by simp [closedCell_zero_eq_singleton, hx], fun h => ?_⟩
-- Module: Mathlib.Topology.CWComplex.Classical.Graph
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
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
⊢ ∃ (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

Premises used: Topology.CWComplex.exists_cellFrontier_one_eq
-- Module: Mathlib.Topology.CWComplex.Classical.Graph
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
⊢ 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

Premises used: Topology.RelCWComplex.closedCell_zero_eq_singleton, Set.union_singleton
-- Module: Mathlib.Topology.CWComplex.Classical.Graph
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) ![]}
⊢ Membership.mem (γ := Set X)
    {(↑(map (C := C) (D := ∅) 0 y) : (Fin 0 → ℝ) → X) ![], (↑(map (C := C) (D := ∅) 0 x) : (Fin 0 → ℝ) → X) ![]}
    ((fun (x : @cell _ inst C ∅ _ 0) ↦ (↑(map (C := C) (D := ∅) 0 x) : (Fin 0 → ℝ) → X) ![]) x)

Tactic:
simp
-- Module: Mathlib.Topology.CWComplex.Classical.Graph
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) ![]}
⊢ Membership.mem (γ := Set X)
    {(↑(map (C := C) (D := ∅) 0 y) : (Fin 0 → ℝ) → X) ![], (↑(map (C := C) (D := ∅) 0 x) : (Fin 0 → ℝ) → X) ![]}
    ((fun (x : @cell _ inst C ∅ _ 0) ↦ (↑(map (C := C) (D := ∅) 0 x) : (Fin 0 → ℝ) → X) ![]) y)

Tactic:
simp
-- Module: Mathlib.Topology.CWComplex.Classical.Graph
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) ![]}
⊢ 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)

Premises used: Topology.RelCWComplex.injective_map_zero, rfl
-- Module: Mathlib.Topology.CWComplex.Classical.Graph
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
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) ![]}
⊢ cellFrontier (C := C) (D := ∅) 1 e = closedCell (C := C) (D := ∅) 0 x

Tactic:
simp [hxy, closedCell_zero_eq_singleton]

Premises used: Topology.RelCWComplex.closedCell_zero_eq_singleton
-- Module: Mathlib.Topology.CWComplex.Classical.Graph
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
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) ![]}
⊢ ∃ (x : @cell _ inst C ∅ _ 0), cellFrontier (C := C) (D := ∅) 1 e = closedCell (C := C) (D := ∅) 0 x

Tactic:
exact ⟨x, by simp [hxy, closedCell_zero_eq_singleton]⟩
-- Module: Mathlib.Topology.CWComplex.Classical.Graph
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).Nontrivial

Tactic:
(exists_isLoopAt_iff_subsingleton e).not.trans not_subsingleton_iff

Premises used: Set.not_subsingleton_iff, Iff.not, Topology.CWComplex.OneSkeletonGraph.exists_isLoopAt_iff_subsingleton, Iff.trans
-- Module: Mathlib.Topology.CWComplex.Classical.Graph
Goal:
X : Type u_1
inst : TopologicalSpace X
C : Set X
inst_1 : CWComplex C
x y : @cell _ inst C ∅ _ 0
⊢ Adj (OneSkeletonGraph C) x y ↔
    ∃ (e : @cell _ inst C ∅ _ 1),
      cellFrontier (C := C) (D := ∅) 1 e = closedCell (C := C) (D := ∅) 0 x ∪ closedCell (C := C) (D := ∅) 0 y

Tactic:
Iff.rfl

Premises used: Iff.rfl, Graph.Adj
-- 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 : @cell _ t C D _ n
hi : i ∈ E.I (C := C) (D := D) n
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)
⊢ closedCell (C := C) (D := D) n i ⊆ (↑E : Set X)

Tactic:
rw [← closure_openCell_eq_closedCell, E.closed.closure_subset_iff, ← E.union]

Premises used: Topology.RelCWComplex.Subcomplex.union, IsClosed.closure_subset_iff, Topology.RelCWComplex.Subcomplex.closed, Topology.RelCWComplex.closure_openCell_eq_closedCell
-- 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 : @cell _ t C D _ n
hi : i ∈ E.I (C := C) (D := D) n
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)
⊢ 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:
apply subset_union_of_subset_right

Premises used: Set.subset_union_of_subset_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)
n : ℕ
i : @cell _ t C D _ n
hi : i ∈ E.I (C := C) (D := D) n
⊢ 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:
subset_iUnion_of_subset n
    (subset_iUnion (fun (j : ↑(E.I n)) ↦ openCell (C := C) n j) ⟨i, hi⟩)

Premises used: Set.subset_iUnion_of_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 : @cell _ t C D _ n
hi : i ∈ E.I (C := C) (D := D) n
⊢ 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:
exact subset_iUnion_of_subset n
    (subset_iUnion (fun (j : ↑(E.I n)) ↦ openCell (C := C) n j) ⟨i, hi⟩)

Premises used: Set.subset_iUnion_of_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 : @cell _ t C D _ n
hi : i ∈ E.I (C := C) (D := D) n
⊢ openCell (C := C) (D := D) n i ⊆ (↑E : Set X)

Tactic:
(openCell_subset_closedCell n i).trans (closedCell_subset_of_mem E hi)

Premises used: Topology.RelCWComplex.Subcomplex.closedCell_subset_of_mem, HasSubset.Subset.trans, Topology.RelCWComplex.openCell_subset_closedCell
-- 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 : @cell _ t C D _ n
hi : i ∈ E.I (C := C) (D := D) n
⊢ cellFrontier (C := C) (D := D) n i ⊆ (↑E : Set X)

Tactic:
(cellFrontier_subset_closedCell n i).trans (closedCell_subset_of_mem E hi)

Premises used: Topology.RelCWComplex.Subcomplex.closedCell_subset_of_mem, HasSubset.Subset.trans, Topology.RelCWComplex.cellFrontier_subset_closedCell
-- 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 :
  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)
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)
⊢ 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

Premises used: subset_antisymm
-- 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 :
  ⋃ (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)

Tactic:
apply union_subset E.base_subset

Premises used: Set.union_subset, Topology.RelCWComplex.Subcomplex.base_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 : ℕ), ⋃ (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:
iUnion₂_subset fun n i ↦ closedCell_subset_of_mem E i.2

Premises used: Set.iUnion₂_subset, Topology.RelCWComplex.Subcomplex.closedCell_subset_of_mem, Subtype.property
-- 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 : ℕ), ⋃ (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:
exact iUnion₂_subset fun n i ↦ closedCell_subset_of_mem E i.2

Premises used: Set.iUnion₂_subset, Topology.RelCWComplex.Subcomplex.closedCell_subset_of_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 :
  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)
⊢ (↑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:
rw [← E.union]

Premises used: Topology.RelCWComplex.Subcomplex.union
-- 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 :
  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))
⊢ 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:
apply union_subset_union_right

Premises used: Set.union_subset_union_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)
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)
⊢ 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 iUnion₂_mono fun n i ↦ ?_

Premises used: Set.iUnion₂_mono
-- 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)
⊢ openCell (C := C) (D := D) n (↑i : cell C n) ⊆ closedCell (C := C) (D := D) n (↑i : cell C n)

Tactic:
openCell_subset_closedCell (C := C) n i

Premises used: Topology.RelCWComplex.openCell_subset_closedCell
-- 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)
⊢ openCell (C := C) (D := D) n (↑i : cell C n) ⊆ closedCell (C := C) (D := D) n (↑i : cell C n)

Tactic:
exact openCell_subset_closedCell (C := C) n i

Premises used: Topology.RelCWComplex.openCell_subset_closedCell
-- Module: Mathlib.Topology.CWComplex.Classical.Subcomplex
Goal:
X : Type u_1
t : TopologicalSpace X
C : Set X
inst : T2Space X
inst_1 : CWComplex C
E : Subcomplex C (D := ∅)
⊢ ⋃ (n : ℕ), ⋃ (j : (↑(E.I (C := C) (D := ∅) n) : Type u_1)), closedCell (C := C) (D := ∅) n (↑j : cell C n) =
    (↑E : Set X)

Tactic:
(empty_union _).symm.trans (RelCWComplex.Subcomplex.union_closedCell E)

Premises used: Topology.RelCWComplex.Subcomplex.union_closedCell, Set.empty_union, Eq.symm, Eq.trans
-- Module: Mathlib.Topology.CWComplex.Classical.Subcomplex
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
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))
⊢ Disjoint (openCell (C := C) (D := D) n i) (↑E : Set X)

Tactic:
simp_rw [← union, disjoint_union_right, disjoint_iUnion_right]

Premises used: Set.disjoint_union_right, Topology.RelCWComplex.Subcomplex.union, Set.disjoint_iUnion_right
-- Module: Mathlib.Topology.CWComplex.Classical.Subcomplex
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
x : ℕ
x_1 : (↑(E.I (C := C) (D := D) x) : Type u_1)
⊢ Sigma.mk (β := fun (n : ℕ) ↦ @cell _ t C D _ n) n i ≠
    Sigma.mk (β := fun (n : ℕ) ↦ @cell _ t C D _ n) x (↑x_1 : cell C x)

Tactic:
lia
-- Module: Mathlib.Topology.CWComplex.Classical.Subcomplex
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) 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:
exact ⟨disjointBase n i , fun _ _ ↦ disjoint_openCell_of_ne (by lia)⟩
-- 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)
_ :
  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
⊢ 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

Tactic:
_