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 : RelCWComplex C D
inst_1 : T2Space X
n : ℕ
j : @cell _ t C D _ n
hf : ContinuousOn (↑(map (C := C) (D := D) n j) : (Fin n → ℝ) → X) (closure (ball 0 1))
⊢ (↑(map (C := C) (D := D) n j) : (Fin n → ℝ) → X) '' closure (ball 0 1) ⊆ closure[t] (openCell (C := C) (D := D) n j)

Tactic:
apply ContinuousOn.image_closure

Premises used: ContinuousOn.image_closure
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
inst_1 : T2Space X
n : ℕ
j : @cell _ t C D _ n
hf : ContinuousOn (↑(map (C := C) (D := D) n j) : (Fin n → ℝ) → X) (closedBall 0 1)
⊢ ContinuousOn (↑(map (C := C) (D := D) n j) : (Fin n → ℝ) → X) (closure (ball 0 1))

Tactic:
rw [closure_ball 0 (by exact one_ne_zero)]

Premises used: closure_ball, OfNat.ofNat
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
inst_1 : T2Space X
n : ℕ
j : @cell _ t C D _ n
⊢ ContinuousOn (↑(map (C := C) (D := D) n j) : (Fin n → ℝ) → X) (closedBall 0 1)

Tactic:
continuousOn n j

Premises used: Topology.RelCWComplex.continuousOn
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
inst_1 : T2Space X
n : ℕ
j : @cell _ t C D _ n
⊢ ContinuousOn (↑(map (C := C) (D := D) n j) : (Fin n → ℝ) → X) (closedBall 0 1)

Tactic:
exact continuousOn n j

Premises used: Topology.RelCWComplex.continuousOn
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
inst_1 : T2Space X
A : Set X
asubc : A ⊆ C
⊢ IsClosed[t] A ↔
    (∀ (n : ℕ) (j : @cell _ t C D _ n), IsClosed[t] (A ∩ closedCell (C := C) (D := D) n j)) ∧ IsClosed[t] (A ∩ D)

Tactic:
⟨?_, closed' A asubc⟩

Premises used: Topology.RelCWComplex.closed', Iff.intro
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
inst_1 : T2Space X
A : Set X
asubc : A ⊆ C
refine :
  IsClosed[t] A →
    (∀ (n : ℕ) (j : @cell _ t C D _ n), IsClosed[t] (A ∩ closedCell (C := C) (D := D) n j)) ∧ IsClosed[t] (A ∩ D)
⊢ IsClosed[t] A ↔
    (∀ (n : ℕ) (j : @cell _ t C D _ n), IsClosed[t] (A ∩ closedCell (C := C) (D := D) n j)) ∧ IsClosed[t] (A ∩ D)

Tactic:
refine ⟨?_, closed' A asubc⟩
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
inst_1 : T2Space X
A : Set X
asubc : A ⊆ C
⊢ IsClosed[t] A →
    (∀ (n : ℕ) (j : @cell _ t C D _ n), IsClosed[t] (A ∩ closedCell (C := C) (D := D) n j)) ∧ IsClosed[t] (A ∩ D)

Tactic:
fun closedA ↦ ⟨fun _ _ ↦ closedA.inter isClosed_closedCell, closedA.inter (isClosedBase C)⟩

Premises used: Topology.RelCWComplex.isClosedBase, Topology.RelCWComplex.isClosed_closedCell, And.intro, IsClosed.inter
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
inst_1 : T2Space X
A : Set X
asubc : A ⊆ C
⊢ IsClosed[t] A →
    (∀ (n : ℕ) (j : @cell _ t C D _ n), IsClosed[t] (A ∩ closedCell (C := C) (D := D) n j)) ∧ IsClosed[t] (A ∩ D)

Tactic:
exact fun closedA ↦ ⟨fun _ _ ↦ closedA.inter isClosed_closedCell, closedA.inter (isClosedBase C)⟩
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C : Set X
inst : CWComplex C
inst_1 : T2Space X
A : Set X
asubc : A ⊆ C
⊢ IsClosed[t] A ↔
    (∀ (n : ℕ) (j : @cell _ t C ∅ _ n), IsClosed[t] (A ∩ closedCell (C := C) (D := ∅) n j)) ∧ IsClosed[t] (A ∩ ∅)

Tactic:
have := RelCWComplex.closed C A asubc
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C : Set X
inst : CWComplex C
inst_1 : T2Space X
A : Set X
asubc : A ⊆ C
this :
  IsClosed[t] A ↔
    (∀ (n : ℕ) (j : @cell _ t C ∅ _ n), IsClosed[t] (A ∩ closedCell (C := C) (D := ∅) n j)) ∧ IsClosed[t] (A ∩ ∅)
⊢ IsClosed[t] A ↔ ∀ (n : ℕ) (j : @cell _ t C ∅ _ n), IsClosed[t] (A ∩ closedCell (C := C) (D := ∅) n j)

Tactic:
simp_all
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
n : ℕ
j : @cell _ t C D _ n
simp_rw : closedCell (C := C) (D := D) n j ⊆ D ∪ ⋃ (n : ℕ), ⋃ (j : @cell _ t C D _ n), closedCell (C := C) (D := D) n j
⊢ closedCell (C := C) (D := D) n j ⊆ C

Tactic:
simp_rw [← union]

Premises used: Topology.RelCWComplex.union
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
n : ℕ
j : @cell _ t C D _ n
⊢ closedCell (C := C) (D := D) n j ⊆ D ∪ ⋃ (n : ℕ), ⋃ (j : @cell _ t C D _ n), closedCell (C := C) (D := D) n j

Tactic:
subset_union_of_subset_right (subset_iUnion₂ _ _) _

Premises used: Set.subset_iUnion₂, Set.subset_union_of_subset_right
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
n : ℕ
j : @cell _ t C D _ n
⊢ closedCell (C := C) (D := D) n j ⊆ D ∪ ⋃ (n : ℕ), ⋃ (j : @cell _ t C D _ n), closedCell (C := C) (D := D) n j

Tactic:
exact subset_union_of_subset_right (subset_iUnion₂ _ _) _

Premises used: Set.subset_iUnion₂, Set.subset_union_of_subset_right
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
n : ℕ
j : @cell _ t C D _ n
⊢ openCell (C := C) (D := D) n j ⊆ C

Tactic:
(openCell_subset_closedCell _ _).trans (closedCell_subset_complex _ _)

Premises used: HasSubset.Subset.trans, Topology.RelCWComplex.closedCell_subset_complex, Topology.RelCWComplex.openCell_subset_closedCell
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
n : ℕ
j : @cell _ t C D _ n
⊢ cellFrontier (C := C) (D := D) n j ⊆ C

Tactic:
(cellFrontier_subset_closedCell n j).trans (closedCell_subset_complex n j)

Premises used: HasSubset.Subset.trans, Topology.RelCWComplex.closedCell_subset_complex, Topology.RelCWComplex.cellFrontier_subset_closedCell
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
j : @cell _ t C D _ 0
⊢ closedCell (C := C) (D := D) 0 j = {(↑(map (C := C) (D := D) 0 j) : (Fin 0 → ℝ) → X) ![]}

Tactic:
simp [closedCell, Matrix.empty_eq]

Premises used: Matrix.empty_eq, Topology.RelCWComplex.closedCell
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
j : @cell _ t C D _ 0
⊢ openCell (C := C) (D := D) 0 j = {(↑(map (C := C) (D := D) 0 j) : (Fin 0 → ℝ) → X) ![]}

Tactic:
simp [openCell, Matrix.empty_eq]

Premises used: Topology.RelCWComplex.openCell, Matrix.empty_eq
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
j : @cell _ t C D _ 0
⊢ cellFrontier (C := C) (D := D) 0 j = ∅

Tactic:
simp [cellFrontier, sphere_eq_empty_of_subsingleton]

Premises used: Topology.RelCWComplex.cellFrontier, Metric.sphere_eq_empty_of_subsingleton
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C : Set X
inst : CWComplex C
n : ℕ
hn : n ≠ 0
j : @cell _ t C ∅ _ n
this : NeZero n := ⋯
h :
  (↑(map (C := C) (D := ∅) n j) : (Fin n → ℝ) → X) (Pi.single (M := fun (a : Fin n) ↦ ℝ) 0 1) ∈
    cellFrontier (C := C) (D := ∅) n j
⊢ (cellFrontier (C := C) (D := ∅) n j).Nonempty

Tactic:
use map n j (Pi.single 0 1)

Premises used: Topology.RelCWComplex.map, Pi.single, PartialEquiv.toFun, OfNat.ofNat
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C : Set X
inst : CWComplex C
n : ℕ
hn : n ≠ 0
j : @cell _ t C ∅ _ n
this : NeZero n := ⋯
h :
  ∃ (x : Fin n → ℝ),
    ‖x‖ = 1 ∧
      (↑(map (C := C) (D := ∅) n j) : (Fin n → ℝ) → X) x =
        (↑(map (C := C) (D := ∅) n j) : (Fin n → ℝ) → X) (Pi.single (M := fun (a : Fin n) ↦ ℝ) 0 1)
⊢ (↑(map (C := C) (D := ∅) n j) : (Fin n → ℝ) → X) (Pi.single (M := fun (a : Fin n) ↦ ℝ) 0 1) ∈
    cellFrontier (C := C) (D := ∅) n j

Tactic:
simp only [cellFrontier, mem_image, mem_sphere_iff_norm, sub_zero]

Premises used: sub_zero, Topology.RelCWComplex.cellFrontier, Set.mem_image, mem_sphere_iff_norm
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C : Set X
inst : CWComplex C
n : ℕ
hn : n ≠ 0
j : @cell _ t C ∅ _ n
this : NeZero n := ⋯
⊢ norm (E := Fin n → ℝ) (Pi.single (M := fun (a : Fin n) ↦ ℝ) 0 1) = 1

Tactic:
simp [Pi.norm_single]

Premises used: Pi.norm_single
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C : Set X
inst : CWComplex C
n : ℕ
hn : n ≠ 0
j : @cell _ t C ∅ _ n
this : NeZero n := ⋯
w : Fin n → ℝ
left : norm (E := Fin n → ℝ) (Pi.single (M := fun (a : Fin n) ↦ ℝ) 0 1) = 1
right :
  (↑(map (C := C) (D := ∅) n j) : (Fin n → ℝ) → X) (Pi.single (M := fun (a : Fin n) ↦ ℝ) 0 1) =
    (↑(map (C := C) (D := ∅) n j) : (Fin n → ℝ) → X) (Pi.single (M := fun (a : Fin n) ↦ ℝ) 0 1)
⊢ ∃ (x : Fin n → ℝ),
    ‖x‖ = 1 ∧
      (↑(map (C := C) (D := ∅) n j) : (Fin n → ℝ) → X) x =
        (↑(map (C := C) (D := ∅) n j) : (Fin n → ℝ) → X) (Pi.single (M := fun (a : Fin n) ↦ ℝ) 0 1)

Tactic:
use Pi.single 0 1, by simp [Pi.norm_single]

Premises used: Pi.single, OfNat.ofNat
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
D C : Set X
inst : RelCWComplex C D
x z : @cell _ t C D _ 0
h :
  Eq.{u_1 + 1} (α := X) ((fun (x : @cell _ t C D _ 0) ↦ (↑(map (C := C) (D := D) 0 x) : (Fin 0 → ℝ) → X) ![]) x)
    ((fun (x : @cell _ t C D _ 0) ↦ (↑(map (C := C) (D := D) 0 x) : (Fin 0 → ℝ) → X) ![]) z)
by_contra : ∀ (hne : ¬x = z), False
⊢ x = z

Tactic:
by_contra hne
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
D C : Set X
inst : RelCWComplex C D
x z : @cell _ t C D _ 0
h :
  Eq.{u_1 + 1} (α := X) ((fun (x : @cell _ t C D _ 0) ↦ (↑(map (C := C) (D := D) 0 x) : (Fin 0 → ℝ) → X) ![]) x)
    ((fun (x : @cell _ t C D _ 0) ↦ (↑(map (C := C) (D := D) 0 x) : (Fin 0 → ℝ) → X) ![]) z)
hne : ¬x = z
⊢ (↑(map (C := C) (D := D) 0 x) : (Fin 0 → ℝ) → X) ![] ∈ openCell (C := C) (D := D) 0 x ∧
    (↑(map (C := C) (D := D) 0 x) : (Fin 0 → ℝ) → X) ![] ∈ openCell (C := C) (D := D) 0 z

Tactic:
simp [openCell_zero_eq_singleton, h]

Premises used: Topology.RelCWComplex.openCell_zero_eq_singleton
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
D C : Set X
inst : RelCWComplex C D
x z : @cell _ t C D _ 0
h :
  Eq.{u_1 + 1} (α := X) ((fun (x : @cell _ t C D _ 0) ↦ (↑(map (C := C) (D := D) 0 x) : (Fin 0 → ℝ) → X) ![]) x)
    ((fun (x : @cell _ t C D _ 0) ↦ (↑(map (C := C) (D := D) 0 x) : (Fin 0 → ℝ) → X) ![]) z)
hne : ¬x = z
⊢ Sigma.mk (β := fun (n : ℕ) ↦ @cell _ t C D _ n) 0 x ≠ Sigma.mk (β := fun (n : ℕ) ↦ @cell _ t C D _ n) 0 z

Tactic:
grind
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
D C : Set X
inst : RelCWComplex C D
x z : @cell _ t C D _ 0
h :
  Eq.{u_1 + 1} (α := X) ((fun (x : @cell _ t C D _ 0) ↦ (↑(map (C := C) (D := D) 0 x) : (Fin 0 → ℝ) → X) ![]) x)
    ((fun (x : @cell _ t C D _ 0) ↦ (↑(map (C := C) (D := D) 0 x) : (Fin 0 → ℝ) → X) ![]) z)
hne : ¬x = z
⊢ False

Tactic:
exact not_disjoint_iff.mpr ⟨map 0 x ![], by simp [openCell_zero_eq_singleton, h]⟩
    <| disjoint_openCell_of_ne (by grind : (⟨0, x⟩ : Σ n, cell C n) ≠ ⟨0, z⟩)

Premises used: Iff.mpr, Topology.RelCWComplex.disjoint_openCell_of_ne, Topology.RelCWComplex.map, Set.not_disjoint_iff, Exists.intro, Matrix.vecEmpty, PartialEquiv.toFun, OfNat.ofNat
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
D C : Set X
inst : RelCWComplex C D
x z : @cell _ t C D _ 0
⊢ (↑(map (C := C) (D := D) 0 x) : (Fin 0 → ℝ) → X) ![] = (↑(map (C := C) (D := D) 0 z) : (Fin 0 → ℝ) → X) ![] ↔ x = z

Tactic:
⟨fun h ↦ injective_map_zero C h, fun h ↦ h ▸ rfl⟩

Premises used: Eq.rec, Topology.RelCWComplex.injective_map_zero, Iff.intro, rfl
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
D C : Set X
inst : RelCWComplex C D
x y : @cell _ t C D _ 0
h : closedCell (C := C) (D := D) 0 x = closedCell (C := C) (D := D) 0 y
⊢ (↑(map (C := C) (D := D) 0 x) : (Fin 0 → ℝ) → X) ![] = (↑(map (C := C) (D := D) 0 y) : (Fin 0 → ℝ) → X) ![]

Tactic:
rw [closedCell_zero_eq_singleton, closedCell_zero_eq_singleton, singleton_eq_singleton_iff] at h

Premises used: Set.singleton_eq_singleton_iff, Topology.RelCWComplex.closedCell_zero_eq_singleton
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
D C : Set X
inst : RelCWComplex C D
x y : @cell _ t C D _ 0
h : (↑(map (C := C) (D := D) 0 x) : (Fin 0 → ℝ) → X) ![] = (↑(map (C := C) (D := D) 0 y) : (Fin 0 → ℝ) → X) ![]
⊢ x = y

Tactic:
injective_map_zero C h

Premises used: Topology.RelCWComplex.injective_map_zero
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
D C : Set X
inst : RelCWComplex C D
x y : @cell _ t C D _ 0
h : (↑(map (C := C) (D := D) 0 x) : (Fin 0 → ℝ) → X) ![] = (↑(map (C := C) (D := D) 0 y) : (Fin 0 → ℝ) → X) ![]
⊢ x = y

Tactic:
exact injective_map_zero C h

Premises used: Topology.RelCWComplex.injective_map_zero
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
D C : Set X
inst : RelCWComplex C D
x y : @cell _ t C D _ 0
h : openCell (C := C) (D := D) 0 x = openCell (C := C) (D := D) 0 y
⊢ (↑(map (C := C) (D := D) 0 x) : (Fin 0 → ℝ) → X) ![] = (↑(map (C := C) (D := D) 0 y) : (Fin 0 → ℝ) → X) ![]

Tactic:
rw [openCell_zero_eq_singleton, openCell_zero_eq_singleton, singleton_eq_singleton_iff] at h

Premises used: Set.singleton_eq_singleton_iff, Topology.RelCWComplex.openCell_zero_eq_singleton
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
e : @cell _ t C D _ 1
e_s : Eq (α := Set (Fin 1 → ℝ)) (sphere 0 1) {-1, 1}
⊢ (↑(map (C := C) (D := D) 1 e) : (Fin 1 → ℝ) → X) '' sphere 0 1 =
    (↑(map (C := C) (D := D) 1 e) : (Fin 1 → ℝ) → X) '' {-1, 1}

Tactic:
congr 1
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
e : @cell _ t C D _ 1
e_s :
  ∀ (f : Fin 1 → ℝ),
    Membership.mem (γ := Set (Fin 1 → ℝ)) (sphere 0 1) f ↔ Membership.mem (γ := Set (Fin 1 → ℝ)) {-1, 1} f
⊢ Eq (α := Set (Fin 1 → ℝ)) (sphere 0 1) {-1, 1}

Tactic:
ext f
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
e : @cell _ t C D _ 1
f : Fin 1 → ℝ
e_s : f 0 = 1 ∨ f 0 = -1 ↔ f = -1 ∨ f = 1
⊢ Membership.mem (γ := Set (Fin 1 → ℝ)) (sphere 0 1) f ↔ Membership.mem (γ := Set (Fin 1 → ℝ)) {-1, 1} f

Tactic:
simp only [mem_sphere_iff_norm, sub_zero, Pi.norm_def, Finset.univ_unique, Fin.default_eq_zero,
    Fin.isValue, Finset.sup_singleton, coe_nnnorm, Real.norm_eq_abs, abs_eq (zero_le_one' ℝ),
    mem_insert_iff, mem_singleton_iff]

Premises used: Real, Finset.sup_singleton, sub_zero, abs_eq, zero_le_one', Finset.univ_unique, Pi.norm_def, Set.mem_singleton_iff, mem_sphere_iff_norm, Fin.isValue, coe_nnnorm, Fin.default_eq_zero, Set.mem_insert_iff, Real.norm_eq_abs
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
e : @cell _ t C D _ 1
f : Fin 1 → ℝ
e_s :
  const (Fin 1) (f default) 0 = 1 ∨ const (Fin 1) (f default) 0 = -1 ↔
    const (Fin 1) (f default) 0 = (-1) 0 ∨ Eq (α := Fin 1 → ℝ) (const (Fin 1) (f default)) 1
⊢ f 0 = 1 ∨ f 0 = -1 ↔ f = -1 ∨ f = 1

Tactic:
rw [eq_const_of_unique (f := f), ← funext_iff_of_subsingleton (x := 0) (y := 0)]

Premises used: Function.funext_iff_of_subsingleton, OfNat.ofNat, eq_const_of_unique
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
e : @cell _ t C D _ 1
f : Fin 1 → ℝ
⊢ const (Fin 1) (f default) 0 = 1 ∨ const (Fin 1) (f default) 0 = -1 ↔
    const (Fin 1) (f default) 0 = (-1) 0 ∨ Eq (α := Fin 1 → ℝ) (const (Fin 1) (f default)) 1

Tactic:
simp [const_apply, or_comm]

Premises used: Function.const_apply, or_comm
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C : Set X
inst : CWComplex C
e : @cell _ t C ∅ _ 1
obtain :
  ∀ (f : (m : ℕ) → Finset (@cell _ t C ∅ _ m))
    (h : cellFrontier (C := C) (D := ∅) 1 e ⊆ ⋃ (m : ℕ), ⋃ (_ : m < 1), ⋃ j ∈ f m, closedCell (C := C) (D := ∅) m j),
    ∃ (x : @cell _ t C ∅ _ 0) (y : @cell _ t C ∅ _ 0),
      cellFrontier (C := C) (D := ∅) 1 e = closedCell (C := C) (D := ∅) 0 x ∪ closedCell (C := C) (D := ∅) 0 y
⊢ ∃ (x : @cell _ t C ∅ _ 0) (y : @cell _ t C ∅ _ 0),
    cellFrontier (C := C) (D := ∅) 1 e = closedCell (C := C) (D := ∅) 0 x ∪ closedCell (C := C) (D := ∅) 0 y

Tactic:
obtain ⟨f, h⟩ := cellFrontier_subset_finite_closedCell 1 e

Premises used: Topology.CWComplex.cellFrontier_subset_finite_closedCell, OfNat.ofNat
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C : Set X
inst : CWComplex C
e : @cell _ t C ∅ _ 1
f : (m : ℕ) → Finset (@cell _ t C ∅ _ m)
h : cellFrontier (C := C) (D := ∅) 1 e ⊆ ⋃ (m : ℕ), ⋃ (_ : m < 1), ⋃ j ∈ f m, closedCell (C := C) (D := ∅) m j
⊢ (∃ (i : @cell _ t C ∅ _ 0),
      Membership.mem (γ := Finset (@cell _ t C ∅ _ 0)) (f 0) i ∧
        (↑(map (C := C) (D := ∅) 1 e) : (Fin 1 → ℝ) → X) (-1) = (↑(map (C := C) (D := ∅) 0 i) : (Fin 0 → ℝ) → X) ![]) ∧
    ∃ (i : @cell _ t C ∅ _ 0),
      Membership.mem (γ := Finset (@cell _ t C ∅ _ 0)) (f 0) i ∧
        (↑(map (C := C) (D := ∅) 1 e) : (Fin 1 → ℝ) → X) 1 = (↑(map (C := C) (D := ∅) 0 i) : (Fin 0 → ℝ) → X) ![]

Tactic:
simp only [RelCWComplex.cellFrontier_one_eq, image_pair, Order.lt_one_iff, iUnion_iUnion_eq_left,
    RelCWComplex.closedCell_zero_eq_singleton, pair_subset_iff, mem_iUnion, mem_singleton_iff,
    exists_prop] at h

Premises used: Set.image_pair, Set.mem_iUnion, Set.pair_subset_iff, exists_prop, Topology.RelCWComplex.cellFrontier_one_eq, Set.iUnion_iUnion_eq_left, Set.mem_singleton_iff, Topology.RelCWComplex.closedCell_zero_eq_singleton, Order.lt_one_iff
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C : Set X
inst : CWComplex C
e : @cell _ t C ∅ _ 1
f : (m : ℕ) → Finset (@cell _ t C ∅ _ m)
h :
  (∃ (i : @cell _ t C ∅ _ 0),
      Membership.mem (γ := Finset (@cell _ t C ∅ _ 0)) (f 0) i ∧
        (↑(map (C := C) (D := ∅) 1 e) : (Fin 1 → ℝ) → X) (-1) = (↑(map (C := C) (D := ∅) 0 i) : (Fin 0 → ℝ) → X) ![]) ∧
    ∃ (i : @cell _ t C ∅ _ 0),
      Membership.mem (γ := Finset (@cell _ t C ∅ _ 0)) (f 0) i ∧
        (↑(map (C := C) (D := ∅) 1 e) : (Fin 1 → ℝ) → X) 1 = (↑(map (C := C) (D := ∅) 0 i) : (Fin 0 → ℝ) → X) ![]
obtain :
  ∀ (u : @cell _ t C ∅ _ 0) (hu : Membership.mem (γ := Finset (@cell _ t C ∅ _ 0)) (f 0) u)
    (hun1 :
      (↑(map (C := C) (D := ∅) 1 e) : (Fin 1 → ℝ) → X) (-1) = (↑(map (C := C) (D := ∅) 0 u) : (Fin 0 → ℝ) → X) ![])
    (v : @cell _ t C ∅ _ 0) (hv : Membership.mem (γ := Finset (@cell _ t C ∅ _ 0)) (f 0) v)
    (hv1 : (↑(map (C := C) (D := ∅) 1 e) : (Fin 1 → ℝ) → X) 1 = (↑(map (C := C) (D := ∅) 0 v) : (Fin 0 → ℝ) → X) ![]),
    ∃ (x : @cell _ t C ∅ _ 0) (y : @cell _ t C ∅ _ 0),
      cellFrontier (C := C) (D := ∅) 1 e = closedCell (C := C) (D := ∅) 0 x ∪ closedCell (C := C) (D := ∅) 0 y
⊢ ∃ (x : @cell _ t C ∅ _ 0) (y : @cell _ t C ∅ _ 0),
    cellFrontier (C := C) (D := ∅) 1 e = closedCell (C := C) (D := ∅) 0 x ∪ closedCell (C := C) (D := ∅) 0 y

Tactic:
obtain ⟨⟨u, hu, hun1⟩, v, hv, hv1⟩ := h
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C : Set X
inst : CWComplex C
e : @cell _ t C ∅ _ 1
f : (m : ℕ) → Finset (@cell _ t C ∅ _ m)
u : @cell _ t C ∅ _ 0
hu : Membership.mem (γ := Finset (@cell _ t C ∅ _ 0)) (f 0) u
hun1 : (↑(map (C := C) (D := ∅) 1 e) : (Fin 1 → ℝ) → X) (-1) = (↑(map (C := C) (D := ∅) 0 u) : (Fin 0 → ℝ) → X) ![]
v : @cell _ t C ∅ _ 0
hv : Membership.mem (γ := Finset (@cell _ t C ∅ _ 0)) (f 0) v
hv1 : (↑(map (C := C) (D := ∅) 1 e) : (Fin 1 → ℝ) → X) 1 = (↑(map (C := C) (D := ∅) 0 v) : (Fin 0 → ℝ) → X) ![]
h : cellFrontier (C := C) (D := ∅) 1 e = closedCell (C := C) (D := ∅) 0 u ∪ closedCell (C := C) (D := ∅) 0 v
⊢ ∃ (x : @cell _ t C ∅ _ 0) (y : @cell _ t C ∅ _ 0),
    cellFrontier (C := C) (D := ∅) 1 e = closedCell (C := C) (D := ∅) 0 x ∪ closedCell (C := C) (D := ∅) 0 y

Tactic:
use u, v
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C : Set X
inst : CWComplex C
e : @cell _ t C ∅ _ 1
f : (m : ℕ) → Finset (@cell _ t C ∅ _ m)
u : @cell _ t C ∅ _ 0
hu : Membership.mem (γ := Finset (@cell _ t C ∅ _ 0)) (f 0) u
hun1 : (↑(map (C := C) (D := ∅) 1 e) : (Fin 1 → ℝ) → X) (-1) = (↑(map (C := C) (D := ∅) 0 u) : (Fin 0 → ℝ) → X) ![]
v : @cell _ t C ∅ _ 0
hv : Membership.mem (γ := Finset (@cell _ t C ∅ _ 0)) (f 0) v
hv1 : (↑(map (C := C) (D := ∅) 1 e) : (Fin 1 → ℝ) → X) 1 = (↑(map (C := C) (D := ∅) 0 v) : (Fin 0 → ℝ) → X) ![]
⊢ cellFrontier (C := C) (D := ∅) 1 e = closedCell (C := C) (D := ∅) 0 u ∪ closedCell (C := C) (D := ∅) 0 v

Tactic:
simp [RelCWComplex.cellFrontier_one_eq, image_pair, RelCWComplex.closedCell_zero_eq_singleton,
    hun1, hv1, pair_comm]

Premises used: Set.image_pair, Topology.RelCWComplex.cellFrontier_one_eq, Topology.RelCWComplex.closedCell_zero_eq_singleton, Set.pair_comm
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
simp_rw : D ⊆ D ∪ ⋃ (n : ℕ), ⋃ (j : @cell _ t C D _ n), closedCell (C := C) (D := D) n j
⊢ D ⊆ C

Tactic:
simp_rw [← union]

Premises used: Topology.RelCWComplex.union
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
⊢ D ⊆ D ∪ ⋃ (n : ℕ), ⋃ (j : @cell _ t C D _ n), closedCell (C := C) (D := D) n j

Tactic:
subset_union_left

Premises used: Set.subset_union_left
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
⊢ D ⊆ D ∪ ⋃ (n : ℕ), ⋃ (j : @cell _ t C D _ n), closedCell (C := C) (D := D) n j

Tactic:
exact subset_union_left

Premises used: Set.subset_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
⊢ C ⊆ C

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
rw : (∀ (n : ℕ) (j : @cell _ t C D _ n), IsClosed[t] (C ∩ closedCell (C := C) (D := D) n j)) ∧ IsClosed[t] (C ∩ D)
⊢ IsClosed[t] C

Tactic:
rw [closed C C (by rfl)]

Premises used: Topology.RelCWComplex.closed
-- 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
left : ∀ (n : ℕ) (j : @cell _ t C D _ n), IsClosed[t] (C ∩ closedCell (C := C) (D := D) n j)
right : IsClosed[t] (C ∩ D)
⊢ (∀ (n : ℕ) (j : @cell _ t C D _ n), IsClosed[t] (C ∩ closedCell (C := C) (D := D) n j)) ∧ IsClosed[t] (C ∩ D)

Tactic:
constructor
-- 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
left : IsClosed[t] (closedCell (C := C) (D := D) n j)
⊢ IsClosed[t] (C ∩ closedCell (C := C) (D := D) n j)

Tactic:
rw [inter_eq_right.2 (closedCell_subset_complex _ _)]

Premises used: Iff.mpr, Set.inter_eq_right, Topology.RelCWComplex.closedCell_subset_complex
-- 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
⊢ IsClosed[t] (closedCell (C := C) (D := D) n j)

Tactic:
isClosed_closedCell

Premises used: Topology.RelCWComplex.isClosed_closedCell