awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Bornology.Constructions
Goal:
ι : Type u_3
X : ι → Type u_4
inst : (i : ι) → Bornology (X i)
⊢ Eq (α := Filter ((i : ι) → X i)) (cobounded ((i : ι) → X i)) (Filter.coprodᵢ (α := X) fun (i : ι) ↦ cobounded (X i))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Bornology.Constructions
Goal:
ι : Type u_3
X : ι → Type u_4
inst : (i : ι) → Bornology (X i)
s : Set ((i : ι) → X i)
⊢ (∀ (i : ι), IsBounded (eval (β := X) i '' s)) ↔ IsBounded s

Tactic:
compl_mem_coprodᵢ.symm

Premises used: Set.Mem, Filter.compl_mem_coprodᵢ, Bornology.IsBounded, Bornology.IsCobounded, Iff.symm
-- Module: Mathlib.Topology.Bornology.Constructions
Goal:
ι : Type u_3
X : ι → Type u_4
inst : (i : ι) → Bornology (X i)
s : Set ((i : ι) → X i)
hs : IsBounded s
i : ι
⊢ IsBounded (eval (β := X) i '' s)

Tactic:
forall_isBounded_image_eval_iff.2 hs i

Premises used: Iff.mpr, Bornology.forall_isBounded_image_eval_iff
-- Module: Mathlib.Topology.Bornology.Constructions
Goal:
ι : Type u_3
X : ι → Type u_4
inst : (i : ι) → Bornology (X i)
S : (i : ι) → Set (X i)
h : ∀ (i : ι), IsBounded (S i)
⊢ IsBounded (Set.pi (α := X) univ S)

Tactic:
forall_isBounded_image_eval_iff.1 fun i => (h i).subset eval_image_univ_pi_subset

Premises used: Set.eval_image_univ_pi_subset, Bornology.forall_isBounded_image_eval_iff, Bornology.IsBounded.subset, Iff.mp
-- Module: Mathlib.Topology.Bornology.Constructions
Goal:
ι : Type u_3
X : ι → Type u_4
inst : (i : ι) → Bornology (X i)
S : (i : ι) → Set (X i)
hne : (Set.pi (α := X) univ S).Nonempty
⊢ IsBounded (Set.pi (α := X) univ S) ↔ ∀ (i : ι), IsBounded (S i)

Tactic:
⟨fun H i => @eval_image_univ_pi _ _ _ i hne ▸ forall_isBounded_image_eval_iff.2 H i, IsBounded.pi⟩

Premises used: Iff.mpr, Eq.rec, Bornology.IsBounded.pi, Bornology.forall_isBounded_image_eval_iff, Set.eval_image_univ_pi, Iff.intro
-- Module: Mathlib.Topology.Bornology.Constructions
Goal:
ι : Type u_3
X : ι → Type u_4
inst : (i : ι) → Bornology (X i)
S : (i : ι) → Set (X i)
pos :
  ∀ (hne : ∃ (i : ι), S i = ∅), IsBounded (Set.pi (α := X) univ S) ↔ (∃ (i : ι), S i = ∅) ∨ ∀ (i : ι), IsBounded (S i)
neg :
  ∀ (hne : ¬∃ (i : ι), S i = ∅), IsBounded (Set.pi (α := X) univ S) ↔ (∃ (i : ι), S i = ∅) ∨ ∀ (i : ι), IsBounded (S i)
⊢ IsBounded (Set.pi (α := X) univ S) ↔ (∃ (i : ι), S i = ∅) ∨ ∀ (i : ι), IsBounded (S i)

Tactic:
by_cases hne : ∃ i, S i = ∅
-- Module: Mathlib.Topology.Bornology.Constructions
Goal:
ι : Type u_3
X : ι → Type u_4
inst : (i : ι) → Bornology (X i)
S : (i : ι) → Set (X i)
hne : ∃ (i : ι), S i = ∅
⊢ IsBounded (Set.pi (α := X) univ S) ↔ (∃ (i : ι), S i = ∅) ∨ ∀ (i : ι), IsBounded (S i)

Tactic:
simp [hne, univ_pi_eq_empty_iff.2 hne]

Premises used: Iff.mpr, Set.univ_pi_eq_empty_iff
-- Module: Mathlib.Topology.Bornology.Constructions
Goal:
ι : Type u_3
X : ι → Type u_4
inst : (i : ι) → Bornology (X i)
S : (i : ι) → Set (X i)
hne : ¬∃ (i : ι), S i = ∅
neg : IsBounded (Set.pi (α := X) univ S) ↔ ∀ (i : ι), IsBounded (S i)
⊢ IsBounded (Set.pi (α := X) univ S) ↔ (∃ (i : ι), S i = ∅) ∨ ∀ (i : ι), IsBounded (S i)

Tactic:
simp only [hne, false_or]

Premises used: false_or
-- Module: Mathlib.Topology.Bornology.Constructions
Goal:
ι : Type u_3
X : ι → Type u_4
inst : (i : ι) → Bornology (X i)
S : (i : ι) → Set (X i)
hne : ¬∃ (i : ι), S i = ∅
⊢ (Set.pi (α := X) univ S).Nonempty

Tactic:
simp only [not_exists, ← nonempty_iff_ne_empty, ← univ_pi_nonempty_iff] at hne

Premises used: not_exists, Set.univ_pi_nonempty_iff, Set.nonempty_iff_ne_empty
-- Module: Mathlib.Topology.Bornology.Constructions
Goal:
ι : Type u_3
X : ι → Type u_4
inst : (i : ι) → Bornology (X i)
S : (i : ι) → Set (X i)
hne : (Set.pi (α := X) univ S).Nonempty
⊢ IsBounded (Set.pi (α := X) univ S) ↔ ∀ (i : ι), IsBounded (S i)

Tactic:
isBounded_pi_of_nonempty hne

Premises used: Bornology.isBounded_pi_of_nonempty
-- Module: Mathlib.Topology.Bornology.Constructions
Goal:
ι : Type u_3
X : ι → Type u_4
inst : (i : ι) → Bornology (X i)
S : (i : ι) → Set (X i)
hne : (Set.pi (α := X) univ S).Nonempty
⊢ IsBounded (Set.pi (α := X) univ S) ↔ ∀ (i : ι), IsBounded (S i)

Tactic:
exact isBounded_pi_of_nonempty hne

Premises used: Bornology.isBounded_pi_of_nonempty
-- Module: Mathlib.Topology.Bornology.Constructions
Goal:
α : Type u_5
β : Type u_6
inst : Bornology β
f : α → β
s : Set α
⊢ IsBounded s ↔ IsBounded (f '' s)

Tactic:
compl_mem_comap

Premises used: Set.Mem, Bornology.IsBounded, Filter.compl_mem_comap, Bornology.IsCobounded
-- Module: Mathlib.Topology.Bornology.Constructions
Goal:
α : Type u_1
inst : Bornology α
p : α → Prop
s : Set { x : α // p x }
⊢ IsBounded (Subtype.val (p := fun (x : α) ↦ p x) '' s) ↔ IsBounded s

Tactic:
isBounded_induced.symm

Premises used: Bornology.isBounded_induced, Iff.symm
-- Module: Mathlib.Topology.Bornology.Constructions
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
X : ι → Type u_4
inst : Bornology α
inst_1 : Bornology β
inst_2 : (i : ι) → Bornology (X i)
inst_3 : BoundedSpace α
inst_4 : BoundedSpace β
⊢ BoundedSpace (α × β)

Tactic:
simp [← cobounded_eq_bot_iff, cobounded_prod]

Premises used: Bornology.cobounded_eq_bot_iff, Bornology.cobounded_prod
-- Module: Mathlib.Topology.Bornology.Constructions
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
X : ι → Type u_4
inst : Bornology α
inst_1 : Bornology β
inst_2 : (i : ι) → Bornology (X i)
inst_3 : ∀ (i : ι), BoundedSpace.{u_4} (X i)
⊢ BoundedSpace ((i : ι) → X i)

Tactic:
simp [← cobounded_eq_bot_iff, cobounded_pi]

Premises used: Bornology.cobounded_eq_bot_iff, Bornology.cobounded_pi
-- Module: Mathlib.Topology.Bornology.Constructions
Goal:
α : Type u_5
β : Type u_6
inst : Bornology β
f : α → β
rw : Bornology.IsBounded.{u_5} (α := α) univ ↔ Bornology.IsBounded (range f)
rw₁ : Bornology.IsBounded (f '' univ) ↔ Bornology.IsBounded (range f)
rw₂ rw₃ : Bornology.IsBounded (range f) ↔ Bornology.IsBounded (range f)
⊢ BoundedSpace α ↔ Bornology.IsBounded (range f)

Tactic:
rw [← @isBounded_univ, isBounded_induced, image_univ]

Premises used: Set.image_univ, Bornology.isBounded_induced, Bornology.isBounded_univ
-- Module: Mathlib.Topology.Bornology.Constructions
Goal:
α : Type u_1
inst : Bornology α
p : α → Prop
rw :
  Bornology.IsBounded.{u_1} (α := α) (range (ι := Subtype p) (Subtype.val (p := p))) ↔
    Bornology.IsBounded.{u_1} (α := α) {x : α | p x}
rw₁ rw₂ : Bornology.IsBounded.{u_1} (α := α) {x : α | p x} ↔ Bornology.IsBounded.{u_1} (α := α) {x : α | p x}
⊢ BoundedSpace.{u_1} (Subtype p) ↔ Bornology.IsBounded.{u_1} (α := α) {x : α | p x}

Tactic:
rw [boundedSpace_induced_iff, Subtype.range_coe_subtype]

Premises used: Subtype.range_coe_subtype, boundedSpace_induced_iff
-- Module: Mathlib.Topology.Bornology.Constructions
Goal:
α : Type u_1
inst : Bornology α
s : Set α
⊢ BoundedSpace.{u_1} (↑s : Type u_1) ↔ Bornology.IsBounded s

Tactic:
boundedSpace_subtype_iff

Premises used: Set.Mem, setOf, boundedSpace_subtype_iff
-- Module: Mathlib.Topology.Bornology.Constructions
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
X : ι → Type u_4
inst : Bornology α
inst_1 : Bornology β
inst_2 : (i : ι) → Bornology (X i)
inst_3 : BoundedSpace α
p : α → Prop
⊢ BoundedSpace.{u_1} (Subtype p)

Tactic:
(IsBounded.all { x | p x }).boundedSpace_subtype

Premises used: Bornology.IsBounded.all, Bornology.IsBounded.boundedSpace_subtype, setOf
-- Module: Mathlib.Topology.Bornology.Hom
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : FunLike F α β
inst_1 : Bornology α
inst_2 : Bornology β
inst_3 : LocallyBoundedMapClass F α β
f : F
s : Set α
hs : IsBounded s
⊢ IsBounded.{u_3} (α := β) ((⇑f : (a : α) → β) '' s)

Tactic:
comap_cobounded_le_iff.1 (comap_cobounded_le f) hs

Premises used: LocallyBoundedMapClass.comap_cobounded_le, Iff.mp, Bornology.comap_cobounded_le_iff
-- Module: Mathlib.Topology.Bornology.Hom
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : Bornology α
inst_2 : Bornology β
inst_3 : Bornology γ
inst_4 : Bornology δ
f g : LocallyBoundedMap α β
h :
  Eq (α := (a : α) → β) ((fun (f : LocallyBoundedMap α β) ↦ f.toFun) f) ((fun (f : LocallyBoundedMap α β) ↦ f.toFun) g)
mk :
  ∀ (toFun : α → β) (comap_cobounded_le' : comap toFun (cobounded β) ≤ cobounded α)
    (h :
      Eq (α := (a : α) → β)
        ((fun (f : LocallyBoundedMap α β) ↦ f.toFun) { toFun := toFun, comap_cobounded_le' := comap_cobounded_le' })
        ((fun (f : LocallyBoundedMap α β) ↦ f.toFun) g)),
    { toFun := toFun, comap_cobounded_le' := comap_cobounded_le' : LocallyBoundedMap α β } = g
⊢ f = g

Tactic:
cases f
-- Module: Mathlib.Topology.Bornology.Hom
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : Bornology α
inst_2 : Bornology β
inst_3 : Bornology γ
inst_4 : Bornology δ
g : LocallyBoundedMap α β
toFun : α → β
comap_cobounded_le' : comap toFun (cobounded β) ≤ cobounded α
h :
  Eq (α := (a : α) → β)
    ((fun (f : LocallyBoundedMap α β) ↦ f.toFun) { toFun := toFun, comap_cobounded_le' := comap_cobounded_le' })
    ((fun (f : LocallyBoundedMap α β) ↦ f.toFun) g)
mk :
  ∀ (toFun_1 : α → β) (comap_cobounded_le'_1 : comap toFun_1 (cobounded β) ≤ cobounded α)
    (h :
      Eq (α := (a : α) → β)
        ((fun (f : LocallyBoundedMap α β) ↦ f.toFun) { toFun := toFun, comap_cobounded_le' := comap_cobounded_le' })
        ((fun (f : LocallyBoundedMap α β) ↦ f.toFun)
          { toFun := toFun_1, comap_cobounded_le' := comap_cobounded_le'_1 })),
    { toFun := toFun, comap_cobounded_le' := comap_cobounded_le' : LocallyBoundedMap α β } =
      { toFun := toFun_1, comap_cobounded_le' := comap_cobounded_le'_1 }
⊢ { toFun := toFun, comap_cobounded_le' := comap_cobounded_le' : LocallyBoundedMap α β } = g

Tactic:
cases g
-- Module: Mathlib.Topology.Bornology.Hom
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : Bornology α
inst_2 : Bornology β
inst_3 : Bornology γ
inst_4 : Bornology δ
toFun : α → β
comap_cobounded_le' : comap toFun (cobounded β) ≤ cobounded α
toFun_1 : α → β
comap_cobounded_le'_1 : comap toFun_1 (cobounded β) ≤ cobounded α
h :
  Eq (α := (a : α) → β)
    ((fun (f : LocallyBoundedMap α β) ↦ f.toFun) { toFun := toFun, comap_cobounded_le' := comap_cobounded_le' })
    ((fun (f : LocallyBoundedMap α β) ↦ f.toFun) { toFun := toFun_1, comap_cobounded_le' := comap_cobounded_le'_1 })
⊢ { toFun := toFun, comap_cobounded_le' := comap_cobounded_le' : LocallyBoundedMap α β } =
    { toFun := toFun_1, comap_cobounded_le' := comap_cobounded_le'_1 }

Tactic:
congr
-- Module: Mathlib.Topology.Bornology.Hom
Goal:
α : Type u_2
β : Type u_3
inst : Bornology α
inst_1 : Bornology β
f g : LocallyBoundedMap α β
h : ∀ (a : α), Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) a : β) ((g : (a : α) → β) a : β)
⊢ f = g

Tactic:
DFunLike.ext f g h

Premises used: DFunLike.ext
-- Module: Mathlib.Topology.Bornology.Hom
Goal:
α : Type u_2
β : Type u_3
inst : Bornology α
inst_1 : Bornology β
f : LocallyBoundedMap α β
f' : α → β
h : f' = (⇑f : (a : α) → β)
⊢ (⇑(f.copy f' h) : (a : α) → β) = f'

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Bornology.Hom
Goal:
α : Type u_2
β : Type u_3
inst : Bornology α
inst_1 : Bornology β
f : LocallyBoundedMap α β
f' : α → β
h : f' = (⇑f : (a : α) → β)
⊢ f.copy f' h = f

Tactic:
DFunLike.ext' h

Premises used: DFunLike.ext'
-- Module: Mathlib.Topology.Bornology.Hom
Goal:
α : Type u_2
β : Type u_3
inst : Bornology α
inst_1 : Bornology β
f : α → β
h : ∀ ⦃s : Set α⦄, Bornology.IsBounded s → Bornology.IsBounded (f '' s)
⊢ (⇑(ofMapBounded f h) : (a : α) → β) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Bornology.Hom
Goal:
α : Type u_2
β : Type u_3
inst : Bornology α
inst_1 : Bornology β
f : α → β
h : ∀ ⦃s : Set α⦄, Bornology.IsBounded s → Bornology.IsBounded (f '' s)
a : α
⊢ (ofMapBounded f h : (a : α) → β) a = f a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Bornology.Hom
Goal:
α : Type u_2
inst : Bornology α
⊢ Eq (α := (a : α) → α) (⇑(LocallyBoundedMap.id α) : (a : α) → α) id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Bornology.Hom
Goal:
α : Type u_2
inst : Bornology α
a : α
⊢ (LocallyBoundedMap.id α : (a : α) → α) a = a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Bornology.Hom
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Bornology α
inst_1 : Bornology β
inst_2 : Bornology γ
f : LocallyBoundedMap β γ
g : LocallyBoundedMap α β
⊢ Eq (α := (a : α) → γ) (⇑(f.comp g) : (a : α) → γ)
    (Function.comp.{u_2 + 1, u_3 + 1, u_4 + 1} (β := β) (⇑f : (a : β) → γ) (⇑g : (a : α) → β))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Bornology.Hom
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Bornology α
inst_1 : Bornology β
inst_2 : Bornology γ
f : LocallyBoundedMap β γ
g : LocallyBoundedMap α β
a : α
⊢ Eq.{u_4 + 1} (α := γ) ((f.comp g : (a : α) → γ) a : γ) ((f : (a : β) → γ) ((g : (a : α) → β) a : β) : γ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Bornology.Hom
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : Bornology α
inst_1 : Bornology β
inst_2 : Bornology γ
inst_3 : Bornology δ
f : LocallyBoundedMap γ δ
g : LocallyBoundedMap β γ
h : LocallyBoundedMap α β
⊢ (f.comp g).comp h = f.comp (g.comp h)

Tactic:
rfl

Premises used: LocallyBoundedMap.comp, rfl
-- Module: Mathlib.Topology.Bornology.Hom
Goal:
α : Type u_2
β : Type u_3
inst : Bornology α
inst_1 : Bornology β
f : LocallyBoundedMap α β
⊢ f.comp (LocallyBoundedMap.id α) = f

Tactic:
ext fun _ => rfl

Premises used: LocallyBoundedMap.ext, rfl
-- Module: Mathlib.Topology.Bornology.Hom
Goal:
α : Type u_2
β : Type u_3
inst : Bornology α
inst_1 : Bornology β
f : LocallyBoundedMap α β
⊢ comp (LocallyBoundedMap.id β) f = f

Tactic:
ext fun _ => rfl

Premises used: LocallyBoundedMap.ext, rfl
-- Module: Mathlib.Topology.Bornology.Hom
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Bornology α
inst_1 : Bornology β
inst_2 : Bornology γ
g₁ g₂ : LocallyBoundedMap β γ
f : LocallyBoundedMap α β
hf : Surjective.{u_2 + 1, u_3 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
⊢ g₁.comp f = g₂.comp f ↔ g₁ = g₂

Tactic:
⟨fun h => ext <| hf.forall.2 <| DFunLike.ext_iff.1 h, congrArg (comp · _)⟩

Premises used: Iff.mpr, Function.Surjective.forall, congrArg, LocallyBoundedMap.comp, DFunLike.ext_iff, Iff.intro, Iff.mp, LocallyBoundedMap.ext
-- Module: Mathlib.Topology.Bornology.Hom
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Bornology α
inst_1 : Bornology β
inst_2 : Bornology γ
g : LocallyBoundedMap β γ
f₁ f₂ : LocallyBoundedMap α β
hg : Injective.{u_3 + 1, u_4 + 1} (α := β) (β := γ) (⇑g : (a : β) → γ)
h : g.comp f₁ = g.comp f₂
a : α
rw : Eq.{u_4 + 1} (α := γ) ((g.comp f₁ : (a : α) → γ) a : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
rw₁ : Eq.{u_4 + 1} (α := γ) ((g.comp f₂ : (a : α) → γ) a : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
rw₂ rw₃ :
  Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
    ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
⊢ Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₁ : (a : α) → β) a : β) : γ)
    ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)

Tactic:
rw [← comp_apply, h, comp_apply]

Premises used: LocallyBoundedMap.comp_apply
-- Module: Mathlib.Topology.Bornology.Real
Goal:
⊢ ∀ (r : ℝ), BddBelow (α := ℝ) (closedBall 0 r)

Tactic:
simp [closedBall_eq_Icc]

Premises used: Real.closedBall_eq_Icc
-- Module: Mathlib.Topology.Bornology.Real
Goal:
⊢ ∀ (r : ℝ), BddAbove (α := ℝ) (closedBall 0 r)

Tactic:
simp [closedBall_eq_Icc]

Premises used: Real.closedBall_eq_Icc
-- Module: Mathlib.Topology.Bornology.Real
Goal:
⊢ OrderTopology ℝ≥0

Tactic:
orderTopology_of_ordConnected (t := Ici 0)

Premises used: Set.Ici, Set.Mem, NNReal, orderTopology_of_ordConnected
-- Module: Mathlib.Topology.Bornology.Real
Goal:
⊢ ∀ (r : ℝ), BddBelow (α := ℝ≥0) (closedBall 0 r)

Tactic:
simp
-- Module: Mathlib.Topology.Bornology.Real
Goal:
r : ℝ
inl : ∀ (hr : 0 ≤ r), BddAbove (α := ℝ≥0) (closedBall 0 r)
inr : ∀ (hr : r < 0), BddAbove (α := ℝ≥0) (closedBall 0 r)
⊢ BddAbove (α := ℝ≥0) (closedBall 0 r)

Tactic:
obtain hr | hr := le_or_gt 0 r

Premises used: le_or_gt, OfNat.ofNat
-- Module: Mathlib.Topology.Bornology.Real
Goal:
r : ℝ
hr : 0 ≤ r
⊢ BddAbove (α := ℝ≥0) (closedBall 0 r)

Tactic:
simp [closedBall_zero_eq_Icc, *]

Premises used: NNReal.closedBall_zero_eq_Icc
-- Module: Mathlib.Topology.Bornology.Real
Goal:
r : ℝ
hr : r < 0
⊢ BddAbove (α := ℝ≥0) (closedBall 0 r)

Tactic:
simp [closedBall_zero_eq_Icc, *]

Premises used: NNReal.closedBall_zero_eq_Icc
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
C : Set X
inst_1 : CWComplex C
⊢ ∀ (n : ℕ) (i : @CWComplex.cell _ inst C _ n),
    Disjoint ((↑(CWComplex.map (C := C) n i) : (Fin n → ℝ) → X) '' ball 0 1) ∅

Tactic:
simp [disjoint_empty]

Premises used: Set.disjoint_empty
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
C : Set X
inst_1 : CWComplex C
⊢ ∀ (n : ℕ) (i : @CWComplex.cell _ inst C _ n),
    ∃ (I : (m : ℕ) → Finset (@CWComplex.cell _ inst C _ m)),
      MapsTo (↑(CWComplex.map (C := C) n i) : (Fin n → ℝ) → X) (sphere 0 1)
        (∅ ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, (↑(CWComplex.map (C := C) m j) : (Fin m → ℝ) → X) '' closedBall 0 1)

Tactic:
simpa only [empty_union] using CWComplex.mapsTo'

Premises used: Set.empty_union, Topology.CWComplex.mapsTo'
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
C : Set X
inst_1 : CWComplex C
⊢ ∀ (A : Set X) (hAC : A ⊆ C),
    (∀ (n : ℕ) (j : @CWComplex.cell _ inst C _ n),
          IsClosed[inst] (A ∩ (↑(CWComplex.map (C := C) n j) : (Fin n → ℝ) → X) '' closedBall 0 1)) ∧
        IsClosed[inst] (A ∩ ∅) →
      IsClosed[inst] A

Tactic:
simpa only [inter_empty, isClosed_empty, and_true] using CWComplex.closed'

Premises used: and_true, isClosed_empty, Topology.CWComplex.closed', Set.inter_empty
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
C : Set X
inst_1 : CWComplex C
⊢ ∅ ∪
      ⋃ (n : ℕ),
        ⋃ (j : @CWComplex.cell _ inst C _ n), (↑(CWComplex.map (C := C) n j) : (Fin n → ℝ) → X) '' closedBall 0 1 =
    C

Tactic:
simpa only [empty_union] using CWComplex.union'

Premises used: Set.empty_union, Topology.CWComplex.union'
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
C : Set X
inst_1 : RelCWComplex C ∅
⊢ ∀ (n : ℕ) (i : @cell _ inst C ∅ _ n),
    ∃ (I : (m : ℕ) → Finset (@cell _ inst C ∅ _ m)),
      MapsTo (↑(map (C := C) (D := ∅) n i) : (Fin n → ℝ) → X) (sphere 0 1)
        (⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, (↑(map (C := C) (D := ∅) m j) : (Fin m → ℝ) → X) '' closedBall 0 1)

Tactic:
simpa using mapsTo (C := C)

Premises used: Topology.RelCWComplex.mapsTo
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
C : Set X
inst_1 : RelCWComplex C ∅
⊢ ∀ (A : Set X) (hAC : A ⊆ C),
    (∀ (n : ℕ) (j : @cell _ inst C ∅ _ n),
        IsClosed[inst] (A ∩ (↑(map (C := C) (D := ∅) n j) : (Fin n → ℝ) → X) '' closedBall 0 1)) →
      IsClosed[inst] A

Tactic:
simpa using closed' (C := C)

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

Tactic:
simpa using union' (C := C)

Premises used: Topology.RelCWComplex.union'
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
C : Set X
h : RelCWComplex C ∅
⊢ CWComplex.instRelCWComplex C = h

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C : Set X
inst : CWComplex C
n : ℕ
i : @cell _ t C ∅ _ n
⊢ ∃ (I : (m : ℕ) → Finset (@cell _ t C ∅ _ m)),
    MapsTo (↑(map (C := C) (D := ∅) n i) : (Fin n → ℝ) → X) (sphere 0 1)
      (∅ ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, (↑(map (C := C) (D := ∅) m j) : (Fin m → ℝ) → X) '' closedBall 0 1)

Tactic:
have := RelCWComplex.mapsTo n i
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C : Set X
inst : CWComplex C
n : ℕ
i : @cell _ t C ∅ _ n
this :
  ∃ (I : (m : ℕ) → Finset (@cell _ t C ∅ _ m)),
    MapsTo (↑(map (C := C) (D := ∅) n i) : (Fin n → ℝ) → X) (sphere 0 1)
      (∅ ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, (↑(map (C := C) (D := ∅) m j) : (Fin m → ℝ) → X) '' closedBall 0 1)
⊢ ∃ (I : (m : ℕ) → Finset (@cell _ t C ∅ _ m)),
    MapsTo (↑(map (C := C) (D := ∅) n i) : (Fin n → ℝ) → X) (sphere 0 1)
      (⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, (↑(map (C := C) (D := ∅) m j) : (Fin m → ℝ) → X) '' closedBall 0 1)

Tactic:
simp_rw [empty_union] at this

Premises used: Set.empty_union
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C : Set X
inst : CWComplex C
n : ℕ
i : @cell _ t C ∅ _ n
this :
  ∃ (I : (m : ℕ) → Finset (@cell _ t C ∅ _ m)),
    MapsTo (↑(map (C := C) (D := ∅) n i) : (Fin n → ℝ) → X) (sphere 0 1)
      (⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, (↑(map (C := C) (D := ∅) m j) : (Fin m → ℝ) → X) '' closedBall 0 1)
⊢ ∃ (I : (m : ℕ) → Finset (@cell _ t C ∅ _ m)),
    MapsTo (↑(map (C := C) (D := ∅) n i) : (Fin n → ℝ) → X) (sphere 0 1)
      (⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, (↑(map (C := C) (D := ∅) m j) : (Fin m → ℝ) → X) '' closedBall 0 1)

Tactic:
this
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C : Set X
inst : CWComplex C
n : ℕ
i : @cell _ t C ∅ _ n
this :
  ∃ (I : (m : ℕ) → Finset (@cell _ t C ∅ _ m)),
    MapsTo (↑(map (C := C) (D := ∅) n i) : (Fin n → ℝ) → X) (sphere 0 1)
      (⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, (↑(map (C := C) (D := ∅) m j) : (Fin m → ℝ) → X) '' closedBall 0 1)
⊢ ∃ (I : (m : ℕ) → Finset (@cell _ t C ∅ _ m)),
    MapsTo (↑(map (C := C) (D := ∅) n i) : (Fin n → ℝ) → X) (sphere 0 1)
      (⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, (↑(map (C := C) (D := ∅) m j) : (Fin m → ℝ) → X) '' closedBall 0 1)

Tactic:
exact this
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
⊢ PairwiseDisjoint (α := Set X) univ fun (ni : (n : ℕ) × @cell _ t C D _ n) ↦
    openCell (C := C) (D := D) (ni.fst (β := fun (n : ℕ) ↦ @cell _ t C D _ n))
      (ni.snd (β := fun (n : ℕ) ↦ @cell _ t C D _ n))

Tactic:
RelCWComplex.pairwiseDisjoint'

Premises used: Topology.RelCWComplex.pairwiseDisjoint', Topology.RelCWComplex.openCell
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
n : ℕ
i : @cell _ t C D _ n
⊢ Disjoint (openCell (C := C) (D := D) n i) D

Tactic:
RelCWComplex.disjointBase' n i

Premises used: Topology.RelCWComplex.openCell, Topology.RelCWComplex.disjointBase'
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
n m : ℕ
i : @cell _ t C D _ n
j : @cell _ t C D _ m
ne : Sigma.mk (β := fun (n : ℕ) ↦ @cell _ t C D _ n) n i ≠ Sigma.mk (β := fun (n : ℕ) ↦ @cell _ t C D _ n) m j
⊢ Disjoint (openCell (C := C) (D := D) n i) (openCell (C := C) (D := D) m j)

Tactic:
pairwiseDisjoint (mem_univ _) (mem_univ _) ne

Premises used: Set.mem_univ, Topology.RelCWComplex.pairwiseDisjoint
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
n : ℕ
i : @cell _ t C D _ n
rcases :
  ∀ (I : (m : ℕ) → Finset (@cell _ t C D _ m))
    (hI :
      MapsTo (↑(map (C := C) (D := D) n i) : (Fin n → ℝ) → X) (sphere 0 1)
        (D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, (↑(map (C := C) (D := D) m j) : (Fin m → ℝ) → X) '' closedBall 0 1)),
    ∃ (I : (m : ℕ) → Finset (@cell _ t C D _ m)),
      cellFrontier (C := C) (D := D) n i ⊆ D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell (C := C) (D := D) m j
⊢ ∃ (I : (m : ℕ) → Finset (@cell _ t C D _ m)),
    cellFrontier (C := C) (D := D) n i ⊆ D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell (C := C) (D := D) m j

Tactic:
rcases mapsTo n i with ⟨I, hI⟩

Premises used: Topology.RelCWComplex.mapsTo