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 : ℕ
e_a :
  Eq.{u_1 + 1} (α := Set X)
    ((⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ (j : @cell _ t C D _ m), closedCell (C := C) (D := D) m j) ∪
      ⋃ (j : @cell _ t C D _ n), closedCell (C := C) (D := D) n j)
    (⋃ (m : ℕ), ⋃ (_ : m < n + 1), ⋃ (j : @cell _ t C D _ m), closedCell (C := C) (D := D) m j)
⊢ Eq.{u_1 + 1} (α := Set X)
    ((⋃ (m : ℕ),
        ⋃ (_ : LT.lt (α := ℕ∞) (↑m : ℕ∞) (↑n : ℕ∞)), ⋃ (j : @cell _ t C D _ m), closedCell (C := C) (D := D) m j) ∪
      ⋃ (j : @cell _ t C D _ n), closedCell (C := C) (D := D) n j)
    (⋃ (m : ℕ),
      ⋃ (_ : (↑m : ℕ∞) < HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1), ⋃ (j : @cell _ t C D _ m), closedCell (C := C) (D := D) m j)

Tactic:
norm_cast
-- 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 : ℕ
⊢ Eq.{u_1 + 1} (α := Set X)
    ((⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ (j : @cell _ t C D _ m), closedCell (C := C) (D := D) m j) ∪
      ⋃ (j : @cell _ t C D _ n), closedCell (C := C) (D := D) n j)
    (⋃ (m : ℕ), ⋃ (_ : m < n + 1), ⋃ (j : @cell _ t C D _ m), closedCell (C := C) (D := D) m j)

Tactic:
(biUnion_lt_succ _ _).symm

Premises used: Set.biUnion_lt_succ, Eq.symm
-- 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 : ℕ
⊢ Eq.{u_1 + 1} (α := Set X)
    ((⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ (j : @cell _ t C D _ m), closedCell (C := C) (D := D) m j) ∪
      ⋃ (j : @cell _ t C D _ n), closedCell (C := C) (D := D) n j)
    (⋃ (m : ℕ), ⋃ (_ : m < n + 1), ⋃ (j : @cell _ t C D _ m), closedCell (C := C) (D := D) m j)

Tactic:
exact (biUnion_lt_succ _ _).symm

Premises used: Set.biUnion_lt_succ, Eq.symm
-- 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 : ℕ
⊢ (↑(skeleton C (D := D) (↑n : ℕ∞)) : Set X) ∪ ⋃ (j : @cell _ t C D _ (n + 1)), closedCell (C := C) (D := D) (n + 1) j =
    (↑(skeleton C (D := D) (HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1)) : Set X)

Tactic:
skeletonLT_union_iUnion_closedCell_eq_skeletonLT_succ _

Premises used: Topology.RelCWComplex.skeletonLT_union_iUnion_closedCell_eq_skeletonLT_succ, WithTop.map₂, WithTop.some, Option.map₂
-- 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 : ℕ∞
⊢ D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j =
    (↑(skeletonLT C (D := D) n) : Set X)

Tactic:
(coe_skeletonLT C _).symm ▸ RelCWComplex.iUnion_openCell_eq_iUnion_closedCell n

Premises used: Topology.RelCWComplex.coe_skeletonLT, Eq.rec, _private.0.Topology.RelCWComplex.iUnion_openCell_eq_iUnion_closedCell, Eq.symm
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C : Set X
inst : T2Space X
inst_1 : CWComplex C
n : ℕ∞
rw :
  Eq.{u_1 + 1} (α := Set X)
    (⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C ∅ _ m), openCell (C := C) (D := ∅) m j)
    (∅ ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C ∅ _ m), openCell (C := C) (D := ∅) m j)
rw₁ rw₂ :
  Eq.{u_1 + 1} (α := Set X)
    (⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C ∅ _ m), openCell (C := C) (D := ∅) m j)
    (⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C ∅ _ m), openCell (C := C) (D := ∅) m j)
⊢ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C ∅ _ m), openCell (C := C) (D := ∅) m j =
    (↑(skeletonLT C (D := ∅) n) : Set X)

Tactic:
rw [← RelCWComplex.iUnion_openCell_eq_skeletonLT, empty_union]

Premises used: Set.empty_union, Topology.RelCWComplex.iUnion_openCell_eq_skeletonLT
-- 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 : ℕ∞
⊢ D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n + 1), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j =
    (↑(skeleton C (D := D) n) : Set X)

Tactic:
iUnion_openCell_eq_skeletonLT _

Premises used: Topology.RelCWComplex.iUnion_openCell_eq_skeletonLT
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C : Set X
inst : T2Space X
inst_1 : CWComplex C
n : ℕ∞
⊢ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n + 1), ⋃ (j : @cell _ t C ∅ _ m), openCell (C := C) (D := ∅) m j =
    (↑(skeleton C (D := ∅) n) : Set X)

Tactic:
iUnion_openCell_eq_skeletonLT _

Premises used: Topology.CWComplex.iUnion_openCell_eq_skeletonLT
-- 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
apply : C ⊆ ⋃ (i : ℕ), (↑(skeletonLT C (D := D) (↑i : ℕ∞)) : Set X)
⊢ ⋃ (n : ℕ), (↑(skeletonLT C (D := D) (↑n : ℕ∞)) : Set X) = C

Tactic:
apply subset_antisymm (iUnion_subset_iff.2 fun _ ↦ (skeletonLT C _).subset_complex)

Premises used: Iff.mpr, Set.iUnion_subset_iff, subset_antisymm, Topology.RelCWComplex.Subcomplex.subset_complex, Topology.RelCWComplex.skeletonLT
-- 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 :
  D ⊆ ⋃ (i : ℕ), (↑(skeletonLT C (D := D) (↑i : ℕ∞)) : Set X) ∧
    ∀ (i : ℕ) (j : @cell _ t C D _ i),
      openCell (C := C) (D := D) i j ⊆ ⋃ (i : ℕ), (↑(skeletonLT C (D := D) (↑i : ℕ∞)) : Set X)
⊢ C ⊆ ⋃ (i : ℕ), (↑(skeletonLT C (D := D) (↑i : ℕ∞)) : Set X)

Tactic:
simp_rw [← union_iUnion_openCell_eq_complex, union_subset_iff, iUnion₂_subset_iff]

Premises used: Topology.RelCWComplex.union_iUnion_openCell_eq_complex, Set.union_subset_iff, Set.iUnion₂_subset_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
⊢ D ⊆ ⋃ (i : ℕ), (↑(skeletonLT C (D := D) (↑i : ℕ∞)) : Set X) ∧
    ∀ (i : ℕ) (j : @cell _ t C D _ i),
      openCell (C := C) (D := D) i j ⊆ ⋃ (i : ℕ), (↑(skeletonLT C (D := D) (↑i : ℕ∞)) : Set X)

Tactic:
⟨subset_iUnion_of_subset 0 (skeletonLT C 0).base_subset,
    fun n i ↦ subset_iUnion_of_subset _ (openCell_subset_skeletonLT n i)⟩

Premises used: Set.subset_iUnion_of_subset, Topology.RelCWComplex.openCell_subset_skeletonLT, HAdd.hAdd, 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
⊢ D ⊆ ⋃ (i : ℕ), (↑(skeletonLT C (D := D) (↑i : ℕ∞)) : Set X) ∧
    ∀ (i : ℕ) (j : @cell _ t C D _ i),
      openCell (C := C) (D := D) i j ⊆ ⋃ (i : ℕ), (↑(skeletonLT C (D := D) (↑i : ℕ∞)) : Set X)

Tactic:
exact ⟨subset_iUnion_of_subset 0 (skeletonLT C 0).base_subset,
    fun n i ↦ subset_iUnion_of_subset _ (openCell_subset_skeletonLT n i)⟩
-- 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
apply : C ⊆ ⋃ (i : ℕ), (↑(skeleton C (D := D) (↑i : ℕ∞)) : Set X)
⊢ ⋃ (n : ℕ), (↑(skeleton C (D := D) (↑n : ℕ∞)) : Set X) = C

Tactic:
apply subset_antisymm (iUnion_subset_iff.2 fun _ ↦ (skeleton C _).subset_complex)

Premises used: Iff.mpr, Set.iUnion_subset_iff, subset_antisymm, Topology.RelCWComplex.Subcomplex.subset_complex, Topology.RelCWComplex.skeleton
-- 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 :
  D ⊆ ⋃ (i : ℕ), (↑(skeleton C (D := D) (↑i : ℕ∞)) : Set X) ∧
    ∀ (i : ℕ) (j : @cell _ t C D _ i),
      openCell (C := C) (D := D) i j ⊆ ⋃ (i : ℕ), (↑(skeleton C (D := D) (↑i : ℕ∞)) : Set X)
⊢ C ⊆ ⋃ (i : ℕ), (↑(skeleton C (D := D) (↑i : ℕ∞)) : Set X)

Tactic:
simp_rw [← union_iUnion_openCell_eq_complex, union_subset_iff, iUnion₂_subset_iff]

Premises used: Topology.RelCWComplex.union_iUnion_openCell_eq_complex, Set.union_subset_iff, Set.iUnion₂_subset_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
⊢ D ⊆ ⋃ (i : ℕ), (↑(skeleton C (D := D) (↑i : ℕ∞)) : Set X) ∧
    ∀ (i : ℕ) (j : @cell _ t C D _ i),
      openCell (C := C) (D := D) i j ⊆ ⋃ (i : ℕ), (↑(skeleton C (D := D) (↑i : ℕ∞)) : Set X)

Tactic:
⟨subset_iUnion_of_subset 0 (skeleton C 0).base_subset,
    fun n i ↦ subset_iUnion_of_subset _ (openCell_subset_skeleton n i)⟩

Premises used: Set.subset_iUnion_of_subset, Topology.RelCWComplex.openCell_subset_skeleton, Topology.RelCWComplex.Subcomplex.base_subset, And.intro, OfNat.ofNat, Topology.RelCWComplex.skeleton
-- 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
⊢ D ⊆ ⋃ (i : ℕ), (↑(skeleton C (D := D) (↑i : ℕ∞)) : Set X) ∧
    ∀ (i : ℕ) (j : @cell _ t C D _ i),
      openCell (C := C) (D := D) i j ⊆ ⋃ (i : ℕ), (↑(skeleton C (D := D) (↑i : ℕ∞)) : Set X)

Tactic:
exact ⟨subset_iUnion_of_subset 0 (skeleton C 0).base_subset,
    fun n i ↦ subset_iUnion_of_subset _ (openCell_subset_skeleton n i)⟩
-- 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 : ℕ∞
x : X
⊢ Membership.mem (γ := Subcomplex C (D := D)) (skeletonLT C (D := D) n) x ↔
    x ∈ D ∨ ∃ (m : ℕ) (_ : (↑m : ℕ∞) < n) (j : @cell _ t C D _ m), x ∈ openCell (C := C) (D := D) m j

Tactic:
simp [← SetLike.mem_coe, ← iUnion_openCell_eq_skeletonLT]

Premises used: Topology.RelCWComplex.iUnion_openCell_eq_skeletonLT, SetLike.mem_coe
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C : Set X
inst : T2Space X
inst_1 : CWComplex C
n : ℕ∞
x : X
⊢ Membership.mem (γ := Subcomplex C (D := ∅)) (skeletonLT C (D := ∅) n) x ↔
    ∃ (m : ℕ) (_ : (↑m : ℕ∞) < n) (j : @cell _ t C ∅ _ m), x ∈ openCell (C := C) (D := ∅) m j

Tactic:
simp [← SetLike.mem_coe, ← iUnion_openCell_eq_skeletonLT]

Premises used: Topology.CWComplex.iUnion_openCell_eq_skeletonLT, SetLike.mem_coe
-- 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 : ℕ∞
x : X
rw :
  (x ∈ D ∨ ∃ (m : ℕ) (_ : (↑m : ℕ∞) < n + 1) (j : @cell _ t C D _ m), x ∈ openCell (C := C) (D := D) m j) ↔
    x ∈ D ∨ ∃ (m : ℕ) (_ : (↑m : ℕ∞) ≤ n) (j : @cell _ t C D _ m), x ∈ openCell (C := C) (D := D) m j
⊢ Membership.mem (γ := Subcomplex C (D := D)) (skeleton C (D := D) n) x ↔
    x ∈ D ∨ ∃ (m : ℕ) (_ : (↑m : ℕ∞) ≤ n) (j : @cell _ t C D _ m), x ∈ openCell (C := C) (D := D) m j

Tactic:
rw [skeleton, mem_skeletonLT_iff]

Premises used: Topology.RelCWComplex.mem_skeletonLT_iff, Topology.RelCWComplex.skeleton
-- 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 : ℕ∞
x : X
this : ∀ (m : ℕ), (↑m : ℕ∞) < n + 1 ↔ (↑m : ℕ∞) ≤ n
⊢ (x ∈ D ∨ ∃ (m : ℕ) (_ : (↑m : ℕ∞) < n + 1) (j : @cell _ t C D _ m), x ∈ openCell (C := C) (D := D) m j) ↔
    x ∈ D ∨ ∃ (m : ℕ) (_ : (↑m : ℕ∞) ≤ n) (j : @cell _ t C D _ m), x ∈ openCell (C := C) (D := D) m j

Tactic:
simp_rw [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 : ℕ∞
x : X
suffices : ∀ (m : ℕ), (↑m : ℕ∞) < n + 1 ↔ (↑m : ℕ∞) ≤ n
⊢ (x ∈ D ∨ ∃ (m : ℕ) (_ : (↑m : ℕ∞) < n + 1) (j : @cell _ t C D _ m), x ∈ openCell (C := C) (D := D) m j) ↔
    x ∈ D ∨ ∃ (m : ℕ) (_ : (↑m : ℕ∞) ≤ n) (j : @cell _ t C D _ m), x ∈ openCell (C := C) (D := D) m j

Tactic:
suffices ∀ (m : ℕ), m < n + 1 ↔ m ≤ n by simp_rw [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 : ℕ∞
x : X
m : ℕ
top : (↑m : ℕ∞) < HAdd.hAdd (α := ℕ∞) ⊤ 1 ↔ LE.le (α := ℕ∞) (↑m : ℕ∞) ⊤
coe : ∀ (a : ℕ), (↑m : ℕ∞) < HAdd.hAdd (α := ℕ∞) (↑a : ℕ∞) 1 ↔ LE.le (α := ℕ∞) (↑m : ℕ∞) (↑a : ℕ∞)
⊢ (↑m : ℕ∞) < n + 1 ↔ (↑m : ℕ∞) ≤ n

Tactic:
cases n
-- 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
x : X
m : ℕ
⊢ (↑m : ℕ∞) < HAdd.hAdd (α := ℕ∞) ⊤ 1 ↔ LE.le (α := ℕ∞) (↑m : ℕ∞) ⊤

Tactic:
simp
-- 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
x : X
m a : ℕ
coe : (↑m : ℕ∞) < HAdd.hAdd (α := ℕ∞) (↑a : ℕ∞) (↑1 : ℕ∞) ↔ LE.le (α := ℕ∞) (↑m : ℕ∞) (↑a : ℕ∞)
coe₁ : LT.lt (α := ℕ∞) (↑m : ℕ∞) (↑(a + 1) : ℕ∞) ↔ LE.le (α := ℕ∞) (↑m : ℕ∞) (↑a : ℕ∞)
coe₂ : m < a + 1 ↔ LE.le (α := ℕ∞) (↑m : ℕ∞) (↑a : ℕ∞)
coe₃ : m < a + 1 ↔ m ≤ a
coe₄ coe₅ : m ≤ a ↔ m ≤ a
⊢ (↑m : ℕ∞) < HAdd.hAdd (α := ℕ∞) (↑a : ℕ∞) 1 ↔ LE.le (α := ℕ∞) (↑m : ℕ∞) (↑a : ℕ∞)

Tactic:
rw [← Nat.cast_one, ← Nat.cast_add, Nat.cast_lt, Nat.cast_le, Order.lt_add_one_iff]

Premises used: Nat.cast_add, Order.lt_add_one_iff, Nat.cast_le, Nat.cast_lt, Nat.cast_one
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C : Set X
inst : T2Space X
inst_1 : CWComplex C
n : ℕ∞
x : X
rw :
  (Membership.mem (γ := Set X) ∅ x ∨
      ∃ (m : ℕ) (_ : (↑m : ℕ∞) ≤ n) (j : @cell _ t C ∅ _ m), x ∈ openCell (C := C) (D := ∅) m j) ↔
    ∃ (m : ℕ) (_ : (↑m : ℕ∞) ≤ n) (j : @cell _ t C ∅ _ m), x ∈ openCell (C := C) (D := ∅) m j
rw₁ :
  (False ∨ ∃ (m : ℕ) (_ : (↑m : ℕ∞) ≤ n) (j : @cell _ t C ∅ _ m), x ∈ openCell (C := C) (D := ∅) m j) ↔
    ∃ (m : ℕ) (_ : (↑m : ℕ∞) ≤ n) (j : @cell _ t C ∅ _ m), x ∈ openCell (C := C) (D := ∅) m j
rw₂ rw₃ :
  (∃ (m : ℕ) (_ : (↑m : ℕ∞) ≤ n) (j : @cell _ t C ∅ _ m), x ∈ openCell (C := C) (D := ∅) m j) ↔
    ∃ (m : ℕ) (_ : (↑m : ℕ∞) ≤ n) (j : @cell _ t C ∅ _ m), x ∈ openCell (C := C) (D := ∅) m j
⊢ Membership.mem (γ := Subcomplex C (D := ∅)) (skeleton C (D := ∅) n) x ↔
    ∃ (m : ℕ) (_ : (↑m : ℕ∞) ≤ n) (j : @cell _ t C ∅ _ m), x ∈ openCell (C := C) (D := ∅) m j

Tactic:
rw [RelCWComplex.mem_skeleton_iff, mem_empty_iff_false, false_or]

Premises used: Topology.RelCWComplex.mem_skeleton_iff, false_or, Set.mem_empty_iff_false
-- 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 : ℕ∞
m : ℕ
j : @cell _ t C D _ m
hnm : n ≤ (↑m : ℕ∞)
simp_rw :
  Disjoint D (openCell (C := C) (D := D) m j) ∧
    ∀ (i : ℕ) (i_1 : (↑i : ℕ∞) < n) (i_2 : @cell _ t C D _ i),
      Disjoint (openCell (C := C) (D := D) i i_2) (openCell (C := C) (D := D) m j)
⊢ Disjoint (↑(skeletonLT C (D := D) n) : Set X) (openCell (C := C) (D := D) m j)

Tactic:
simp_rw [← iUnion_openCell_eq_skeletonLT, disjoint_union_left, disjoint_iUnion_left]

Premises used: Set.disjoint_iUnion_left, Topology.RelCWComplex.iUnion_openCell_eq_skeletonLT, Set.disjoint_union_left
-- 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 : ℕ∞
m : ℕ
j : @cell _ t C D _ m
hnm : n ≤ (↑m : ℕ∞)
⊢ Disjoint D (openCell (C := C) (D := D) m j) ∧
    ∀ (i : ℕ) (i_1 : (↑i : ℕ∞) < n) (i_2 : @cell _ t C D _ i),
      Disjoint (openCell (C := C) (D := D) i i_2) (openCell (C := C) (D := D) m j)

Tactic:
⟨(disjointBase m j).symm, ?_⟩

Premises used: Disjoint.symm, Topology.RelCWComplex.disjointBase, And.intro
-- 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 : ℕ∞
m : ℕ
j : @cell _ t C D _ m
hnm : n ≤ (↑m : ℕ∞)
refine :
  ∀ (i : ℕ) (i_1 : (↑i : ℕ∞) < n) (i_2 : @cell _ t C D _ i),
    Disjoint (openCell (C := C) (D := D) i i_2) (openCell (C := C) (D := D) m j)
⊢ Disjoint D (openCell (C := C) (D := D) m j) ∧
    ∀ (i : ℕ) (i_1 : (↑i : ℕ∞) < n) (i_2 : @cell _ t C D _ i),
      Disjoint (openCell (C := C) (D := D) i i_2) (openCell (C := C) (D := D) m j)

Tactic:
refine ⟨(disjointBase m j).symm, ?_⟩
-- 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 : ℕ∞
m : ℕ
j : @cell _ t C D _ m
hnm : n ≤ (↑m : ℕ∞)
l : ℕ
hln : (↑l : ℕ∞) < n
i : @cell _ t C D _ l
ne : Sigma.mk (β := fun (n : ℕ) ↦ @cell _ t C D _ n) l i ≠ Sigma.mk (β := fun (n : ℕ) ↦ @cell _ t C D _ n) m j
⊢ Disjoint (openCell (C := C) (D := D) l i) (openCell (C := C) (D := D) m j)

Tactic:
apply disjoint_openCell_of_ne

Premises used: Topology.RelCWComplex.disjoint_openCell_of_ne
-- 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 : ℕ∞
m : ℕ
j : @cell _ t C D _ m
hnm : n ≤ (↑m : ℕ∞)
l : ℕ
hln : (↑l : ℕ∞) < n
i : @cell _ t C D _ l
h : Sigma.mk (β := fun (n : ℕ) ↦ @cell _ t C D _ n) l i = Sigma.mk (β := fun (n : ℕ) ↦ @cell _ t C D _ n) m j
⊢ (↑m : ℕ∞) < n

Tactic:
simp_all only [Sigma.mk.inj_iff]

Premises used: Sigma.mk.inj_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 : ℕ∞
m : ℕ
j : @cell _ t C D _ m
hnm : n ≤ (↑m : ℕ∞)
l : ℕ
hln : (↑l : ℕ∞) < n
i : @cell _ t C D _ l
h : Sigma.mk (β := fun (n : ℕ) ↦ @cell _ t C D _ n) l i = Sigma.mk (β := fun (n : ℕ) ↦ @cell _ t C D _ n) m j
hln₁ : (↑m : ℕ∞) < n
⊢ l = m ∧ i ≍ j

Tactic:
simp_all only [Sigma.mk.inj_iff]

Premises used: Sigma.mk.inj_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 : ℕ∞
m : ℕ
j : @cell _ t C D _ m
hnm : n ≤ (↑m : ℕ∞)
l : ℕ
i : @cell _ t C D _ l
hln : (↑m : ℕ∞) < n
h : l = m ∧ i ≍ j
⊢ False

Tactic:
(lt_self_iff_false m).mp (ENat.coe_lt_coe.1 (hln.trans_le hnm))

Premises used: LT.lt.trans_le, ENat.coe_lt_coe, lt_self_iff_false, Iff.mp
-- 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 : ℕ∞
m : ℕ
j : @cell _ t C D _ m
hnm : n ≤ (↑m : ℕ∞)
l : ℕ
i : @cell _ t C D _ l
hln : (↑m : ℕ∞) < n
h : l = m ∧ i ≍ j
⊢ False

Tactic:
exact (lt_self_iff_false m).mp (ENat.coe_lt_coe.1 (hln.trans_le hnm))

Premises used: LT.lt.trans_le, ENat.coe_lt_coe, lt_self_iff_false, Iff.mp
-- 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 : ℕ∞
m : ℕ
j : @cell _ t C D _ m
nlem : n < (↑m : ℕ∞)
⊢ Disjoint (↑(skeleton C (D := D) n) : Set X) (openCell (C := C) (D := D) m j)

Tactic:
disjoint_skeletonLT_openCell (Order.add_one_le_of_lt nlem)

Premises used: Topology.RelCWComplex.disjoint_skeletonLT_openCell, Order.add_one_le_of_lt
-- 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 : ℕ∞
m : ℕ
j : @cell _ t C D _ m
hnm : n ≤ (↑m : ℕ∞)
⊢ (↑(skeletonLT C (D := D) n) : Set X) ∩ closedCell (C := C) (D := D) m j =
    (↑(skeletonLT C (D := D) n) : Set X) ∩ cellFrontier (C := C) (D := D) m j

Tactic:
subset_antisymm ?_ (inter_subset_inter_right _ (cellFrontier_subset_closedCell _ _))

Premises used: Set.inter_subset_inter_right, subset_antisymm, Topology.RelCWComplex.cellFrontier_subset_closedCell
-- 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 : ℕ∞
m : ℕ
j : @cell _ t C D _ m
hnm : n ≤ (↑m : ℕ∞)
refine :
  (↑(skeletonLT C (D := D) n) : Set X) ∩ closedCell (C := C) (D := D) m j ⊆
    (↑(skeletonLT C (D := D) n) : Set X) ∩ cellFrontier (C := C) (D := D) m j
⊢ (↑(skeletonLT C (D := D) n) : Set X) ∩ closedCell (C := C) (D := D) m j =
    (↑(skeletonLT C (D := D) n) : Set X) ∩ cellFrontier (C := C) (D := D) m j

Tactic:
refine subset_antisymm ?_ (inter_subset_inter_right _ (cellFrontier_subset_closedCell _ _))

Premises used: Set.inter_subset_inter_right, subset_antisymm, Topology.RelCWComplex.cellFrontier_subset_closedCell
-- 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 : ℕ∞
m : ℕ
j : @cell _ t C D _ m
hnm : n ≤ (↑m : ℕ∞)
rw :
  (↑(skeletonLT C (D := D) n) : Set X) ∩ cellFrontier (C := C) (D := D) m j ∪
      (↑(skeletonLT C (D := D) n) : Set X) ∩ openCell (C := C) (D := D) m j ⊆
    (↑(skeletonLT C (D := D) n) : Set X) ∩ cellFrontier (C := C) (D := D) m j
⊢ (↑(skeletonLT C (D := D) n) : Set X) ∩ closedCell (C := C) (D := D) m j ⊆
    (↑(skeletonLT C (D := D) n) : Set X) ∩ cellFrontier (C := C) (D := D) m j

Tactic:
rw [← cellFrontier_union_openCell_eq_closedCell, inter_union_distrib_left]

Premises used: Topology.RelCWComplex.cellFrontier_union_openCell_eq_closedCell, Set.inter_union_distrib_left
-- 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 : ℕ∞
m : ℕ
j : @cell _ t C D _ m
hnm : n ≤ (↑m : ℕ∞)
⊢ (↑(skeletonLT C (D := D) n) : Set X) ∩ cellFrontier (C := C) (D := D) m j ⊆
    (↑(skeletonLT C (D := D) n) : Set X) ∩ cellFrontier (C := C) (D := D) m j

Tactic:
rfl
-- 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 : ℕ∞
m : ℕ
j : @cell _ t C D _ m
hnm : n ≤ (↑m : ℕ∞)
apply :
  (↑(skeletonLT C (D := D) n) : Set X) ∩ openCell (C := C) (D := D) m j ⊆
    (↑(skeletonLT C (D := D) n) : Set X) ∩ cellFrontier (C := C) (D := D) m j
⊢ (↑(skeletonLT C (D := D) n) : Set X) ∩ cellFrontier (C := C) (D := D) m j ∪
      (↑(skeletonLT C (D := D) n) : Set X) ∩ openCell (C := C) (D := D) m j ⊆
    (↑(skeletonLT C (D := D) n) : Set X) ∩ cellFrontier (C := C) (D := D) m j

Tactic:
apply union_subset (by rfl)

Premises used: Set.union_subset
-- 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 : ℕ∞
m : ℕ
j : @cell _ t C D _ m
hnm : n ≤ (↑m : ℕ∞)
rw : ∅ ⊆ (↑(skeletonLT C (D := D) n) : Set X) ∩ cellFrontier (C := C) (D := D) m j
⊢ (↑(skeletonLT C (D := D) n) : Set X) ∩ openCell (C := C) (D := D) m j ⊆
    (↑(skeletonLT C (D := D) n) : Set X) ∩ cellFrontier (C := C) (D := D) m j

Tactic:
rw [(disjoint_skeletonLT_openCell hnm).inter_eq]

Premises used: 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 : ℕ∞
m : ℕ
j : @cell _ t C D _ m
hnm : n ≤ (↑m : ℕ∞)
⊢ ∅ ⊆ (↑(skeletonLT C (D := D) n) : Set X) ∩ cellFrontier (C := C) (D := D) m j

Tactic:
empty_subset _

Premises used: Set.empty_subset
-- 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 : ℕ∞
m : ℕ
j : @cell _ t C D _ m
hnm : n ≤ (↑m : ℕ∞)
⊢ ∅ ⊆ (↑(skeletonLT C (D := D) n) : Set X) ∩ cellFrontier (C := C) (D := D) m j

Tactic:
exact empty_subset _

Premises used: Set.empty_subset
-- 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 : ℕ∞
m : ℕ
j : @cell _ t C D _ m
hnm : n < (↑m : ℕ∞)
⊢ (↑(skeleton C (D := D) n) : Set X) ∩ closedCell (C := C) (D := D) m j =
    (↑(skeleton C (D := D) n) : Set X) ∩ cellFrontier (C := C) (D := D) m j

Tactic:
skeletonLT_inter_closedCell_eq_skeletonLT_inter_cellFrontier (Order.add_one_le_of_lt hnm)

Premises used: Topology.RelCWComplex.skeletonLT_inter_closedCell_eq_skeletonLT_inter_cellFrontier, Order.add_one_le_of_lt
-- 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
rw : interior D ∩ closedCell (C := C) (D := D) n j = ∅
⊢ Disjoint (interior D) (closedCell (C := C) (D := D) n j)

Tactic:
rw [disjoint_iff_inter_eq_empty]

Premises used: Set.disjoint_iff_inter_eq_empty