awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
σ : ι → Type u_7
inst : (i : ι) → TopologicalSpace (σ i)
i : ι
s : Set (σ i)
hs : IsOpen[inst i] s
j : ι
hne : j ≠ i
⊢ IsOpen[inst j] ∅

Tactic:
isOpen_empty

Premises used: isOpen_empty
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
σ : ι → Type u_7
inst : (i : ι) → TopologicalSpace (σ i)
i : ι
s : Set (σ i)
hs : IsOpen[inst i] s
j : ι
hne : j ≠ i
⊢ IsOpen[inst j] ∅

Tactic:
exact isOpen_empty

Premises used: isOpen_empty
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
σ : ι → Type u_7
inst : (i : ι) → TopologicalSpace (σ i)
i : ι
⊢ IsOpen[instTopologicalSpaceSigma] (range (Sigma.mk (β := σ) i))

Tactic:
isOpenMap_sigmaMk.isOpen_range

Premises used: isOpenMap_sigmaMk, IsOpenMap.isOpen_range
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
σ : ι → Type u_7
inst : (i : ι) → TopologicalSpace (σ i)
i : ι
s : Set (σ i)
hs : IsClosed[inst i] s
rw : ∀ (i_1 : ι), IsClosed[inst i_1] (Sigma.mk (β := σ) i_1 ⁻¹' Sigma.mk (β := σ) i '' s)
⊢ IsClosed[instTopologicalSpaceSigma] (Sigma.mk (β := σ) i '' s)

Tactic:
rw [isClosed_sigma_iff]

Premises used: isClosed_sigma_iff
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
σ : ι → Type u_7
inst : (i : ι) → TopologicalSpace (σ i)
i : ι
s : Set (σ i)
hs : IsClosed[inst i] s
j : ι
inl : ∀ (s : Set (σ j)) (hs : IsClosed[inst j] s), IsClosed[inst j] (Sigma.mk (β := σ) j ⁻¹' Sigma.mk (β := σ) j '' s)
inr : ∀ (hne : j ≠ i), IsClosed[inst j] (Sigma.mk (β := σ) j ⁻¹' Sigma.mk (β := σ) i '' s)
⊢ IsClosed[inst j] (Sigma.mk (β := σ) j ⁻¹' Sigma.mk (β := σ) i '' s)

Tactic:
rcases eq_or_ne j i with (rfl | hne)

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
σ : ι → Type u_7
inst : (i : ι) → TopologicalSpace (σ i)
j : ι
s : Set (σ j)
hs inl inl₁ inl₂ inl₃ : IsClosed[inst j] s
⊢ IsClosed[inst j] (Sigma.mk (β := σ) j ⁻¹' Sigma.mk (β := σ) j '' s)

Tactic:
rwa [preimage_image_eq _ sigma_mk_injective]

Premises used: Set.preimage_image_eq, sigma_mk_injective
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
σ : ι → Type u_7
inst : (i : ι) → TopologicalSpace (σ i)
i : ι
s : Set (σ i)
hs : IsClosed[inst i] s
j : ι
hne : j ≠ i
inr : IsClosed[inst j] ∅
⊢ IsClosed[inst j] (Sigma.mk (β := σ) j ⁻¹' Sigma.mk (β := σ) i '' s)

Tactic:
rw [preimage_image_sigmaMk_of_ne hne]

Premises used: Set.preimage_image_sigmaMk_of_ne
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
σ : ι → Type u_7
inst : (i : ι) → TopologicalSpace (σ i)
i : ι
s : Set (σ i)
hs : IsClosed[inst i] s
j : ι
hne : j ≠ i
⊢ IsClosed[inst j] ∅

Tactic:
isClosed_empty

Premises used: isClosed_empty
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
σ : ι → Type u_7
inst : (i : ι) → TopologicalSpace (σ i)
i : ι
s : Set (σ i)
hs : IsClosed[inst i] s
j : ι
hne : j ≠ i
⊢ IsClosed[inst j] ∅

Tactic:
exact isClosed_empty

Premises used: isClosed_empty
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
σ : ι → Type u_7
inst : (i : ι) → TopologicalSpace (σ i)
i : ι
⊢ IsClosed[instTopologicalSpaceSigma] (range (Sigma.mk (β := σ) i))

Tactic:
isClosedMap_sigmaMk.isClosed_range

Premises used: isClosedMap_sigmaMk, IsClosedMap.isClosed_range
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
σ : ι → Type u_7
inst : (i : ι) → TopologicalSpace (σ i)
i : ι
⊢ IsOpenEmbedding (X := σ i) (Sigma.mk (β := σ) i)

Tactic:
.of_continuous_injective_isOpenMap continuous_sigmaMk sigma_mk_injective isOpenMap_sigmaMk

Premises used: continuous_sigmaMk, Topology.IsOpenEmbedding.of_continuous_injective_isOpenMap, isOpenMap_sigmaMk, sigma_mk_injective
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
σ : ι → Type u_7
inst : (i : ι) → TopologicalSpace (σ i)
i : ι
⊢ IsClosedEmbedding (X := σ i) (Sigma.mk (β := σ) i)

Tactic:
.of_continuous_injective_isClosedMap continuous_sigmaMk sigma_mk_injective isClosedMap_sigmaMk

Premises used: isClosedMap_sigmaMk, continuous_sigmaMk, Topology.IsClosedEmbedding.of_continuous_injective_isClosedMap, sigma_mk_injective
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
σ : ι → Type u_7
inst : (i : ι) → TopologicalSpace (σ i)
i : ι
⊢ IsEmbedding (X := σ i) (Sigma.mk (β := σ) i)

Tactic:
IsClosedEmbedding.sigmaMk.1

Premises used: Topology.IsClosedEmbedding.sigmaMk, Topology.IsClosedEmbedding.toIsEmbedding
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
σ : ι → Type u_7
inst : (i : ι) → TopologicalSpace (σ i)
i : ι
x : σ i
⊢ 𝓝 (mk (β := σ) i x) = Filter.map (mk (β := σ) i) (𝓝 x)

Tactic:
(IsOpenEmbedding.sigmaMk.map_nhds_eq x).symm

Premises used: Topology.IsOpenEmbedding.map_nhds_eq, Topology.IsOpenEmbedding.sigmaMk, Eq.symm
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
σ : ι → Type u_7
inst : (i : ι) → TopologicalSpace (σ i)
x : Sigma σ
mk :
  ∀ (fst : ι) (snd : σ fst),
    𝓝 (Sigma.mk (β := σ) fst snd) =
      Filter.map (Sigma.mk (β := σ) ((Sigma.mk (β := σ) fst snd).fst (β := σ)))
        (𝓝 ((Sigma.mk (β := σ) fst snd).snd (β := σ)))
⊢ 𝓝 x = Filter.map (Sigma.mk (β := σ) (x.fst (β := σ))) (𝓝 (x.snd (β := σ)))

Tactic:
cases x
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
σ : ι → Type u_7
inst : (i : ι) → TopologicalSpace (σ i)
fst : ι
snd : σ fst
⊢ 𝓝 (mk (β := σ) fst snd) =
    Filter.map (mk (β := σ) ((mk (β := σ) fst snd).fst (β := σ))) (𝓝 ((mk (β := σ) fst snd).snd (β := σ)))

Tactic:
apply Sigma.nhds_mk

Premises used: Sigma.nhds_mk
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
σ : ι → Type u_7
inst : (i : ι) → TopologicalSpace (σ i)
i : ι
x : σ i
⊢ comap (Sigma.mk (β := σ) i) (𝓝 (Sigma.mk (β := σ) i x)) = 𝓝 x

Tactic:
(IsEmbedding.sigmaMk.nhds_eq_comap _).symm

Premises used: Topology.IsInducing.nhds_eq_comap, Topology.IsEmbedding.sigmaMk, Topology.IsEmbedding.toIsInducing, Eq.symm
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
σ : ι → Type u_7
inst : (i : ι) → TopologicalSpace (σ i)
s : Set ι
rw : IsOpen[instTopologicalSpaceSigma] (⋃ i ∈ s, Sigma.fst (β := fun (a : ι) ↦ σ a) ⁻¹' {i})
⊢ IsOpen[instTopologicalSpaceSigma] (Sigma.fst (β := fun (a : ι) ↦ σ a) ⁻¹' s)

Tactic:
rw [← biUnion_of_singleton s, preimage_iUnion₂]

Premises used: Set.biUnion_of_singleton, Set.preimage_iUnion₂
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
σ : ι → Type u_7
inst : (i : ι) → TopologicalSpace (σ i)
s : Set ι
simp : IsOpen[instTopologicalSpaceSigma] (⋃ i ∈ s, range (Sigma.mk (β := fun (a : ι) ↦ σ a) i))
⊢ IsOpen[instTopologicalSpaceSigma] (⋃ i ∈ s, Sigma.fst (β := fun (a : ι) ↦ σ a) ⁻¹' {i})

Tactic:
simp only [← range_sigmaMk]

Premises used: Set.range_sigmaMk
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
σ : ι → Type u_7
inst : (i : ι) → TopologicalSpace (σ i)
s : Set ι
⊢ IsOpen[instTopologicalSpaceSigma] (⋃ i ∈ s, range (Sigma.mk (β := fun (a : ι) ↦ σ a) i))

Tactic:
isOpen_biUnion fun _ _ => isOpen_range_sigmaMk

Premises used: isOpen_range_sigmaMk, isOpen_biUnion
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
σ : ι → Type u_7
inst : (i : ι) → TopologicalSpace (σ i)
s : Set ι
⊢ IsOpen[instTopologicalSpaceSigma] (⋃ i ∈ s, range (Sigma.mk (β := fun (a : ι) ↦ σ a) i))

Tactic:
exact isOpen_biUnion fun _ _ => isOpen_range_sigmaMk

Premises used: isOpen_range_sigmaMk, isOpen_biUnion
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
ι : Type u_5
σ : ι → Type u_7
inst : (i : ι) → TopologicalSpace (σ i)
inst_1 : TopologicalSpace X
f : Sigma σ → X
rw :
  (∀ (i : ι), Continuous[coinduced (Sigma.mk i) (inst i), inst_1] f) ↔
    ∀ (i : ι), Continuous[inst i, inst_1] fun (a : σ i) ↦ f (Sigma.mk (β := σ) i a)
⊢ Continuous[⨆ (i : ι), coinduced (Sigma.mk i) (inst i), inst_1] f ↔
    ∀ (i : ι), Continuous[inst i, inst_1] fun (a : σ i) ↦ f (Sigma.mk (β := σ) i a)

Tactic:
rw [continuous_iSup_dom]

Premises used: continuous_iSup_dom
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
ι : Type u_5
σ : ι → Type u_7
inst : (i : ι) → TopologicalSpace (σ i)
inst_1 : TopologicalSpace X
f : Sigma σ → X
⊢ (∀ (i : ι), Continuous[coinduced (Sigma.mk i) (inst i), inst_1] f) ↔
    ∀ (i : ι), Continuous[inst i, inst_1] fun (a : σ i) ↦ f (Sigma.mk (β := σ) i a)

Tactic:
forall_congr' fun _ => continuous_coinduced_dom

Premises used: continuous_coinduced_dom, forall_congr'
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
ι : Type u_5
σ : ι → Type u_7
inst : (i : ι) → TopologicalSpace (σ i)
inst_1 : TopologicalSpace X
f : Sigma σ → X
⊢ (∀ (i : ι), Continuous[coinduced (Sigma.mk i) (inst i), inst_1] f) ↔
    ∀ (i : ι), Continuous[inst i, inst_1] fun (a : σ i) ↦ f (Sigma.mk (β := σ) i a)

Tactic:
exact forall_congr' fun _ => continuous_coinduced_dom

Premises used: continuous_coinduced_dom, forall_congr'
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
ι : Type u_5
σ : ι → Type u_7
inst : (i : ι) → TopologicalSpace (σ i)
inst_1 : TopologicalSpace X
f : Sigma σ → X
hf : ∀ (i : ι), Continuous[inst i, inst_1] fun (a : σ i) ↦ f (Sigma.mk (β := σ) i a)
⊢ Continuous[instTopologicalSpaceSigma, inst_1] f

Tactic:
continuous_sigma_iff.2 hf

Premises used: Iff.mpr, continuous_sigma_iff
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
ι : Type u_5
σ : ι → Type u_7
inst : (i : ι) → TopologicalSpace (σ i)
inst_1 : TopologicalSpace X
f : Sigma σ → X
⊢ IsInducing f ↔
    (∀ (i : ι), IsInducing (f ∘ Sigma.mk (β := σ) i)) ∧
      ∀ (i : ι), ∃ (U : Set X), IsOpen[inst_1] U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst (β := σ) = i

Tactic:
⟨fun h ↦ ⟨fun i ↦ h.comp IsEmbedding.sigmaMk.1, fun i ↦ ?_⟩, ?_⟩

Premises used: Topology.IsInducing.comp, Topology.IsEmbedding.sigmaMk, And.intro, Iff.intro, Topology.IsEmbedding.toIsInducing
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
ι : Type u_5
σ : ι → Type u_7
inst : (i : ι) → TopologicalSpace (σ i)
inst_1 : TopologicalSpace X
f : Sigma σ → X
refine_1 : ∀ (h : IsInducing f) (i : ι), ∃ (U : Set X), IsOpen[inst_1] U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst (β := σ) = i
refine_2 :
  ((∀ (i : ι), IsInducing (f ∘ Sigma.mk (β := σ) i)) ∧
      ∀ (i : ι), ∃ (U : Set X), IsOpen[inst_1] U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst (β := σ) = i) →
    IsInducing f
⊢ IsInducing f ↔
    (∀ (i : ι), IsInducing (f ∘ Sigma.mk (β := σ) i)) ∧
      ∀ (i : ι), ∃ (U : Set X), IsOpen[inst_1] U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst (β := σ) = i

Tactic:
refine ⟨fun h ↦ ⟨fun i ↦ h.comp IsEmbedding.sigmaMk.1, fun i ↦ ?_⟩, ?_⟩
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
ι : Type u_5
σ : ι → Type u_7
inst : (i : ι) → TopologicalSpace (σ i)
inst_1 : TopologicalSpace X
f : Sigma σ → X
h : IsInducing f
i : ι
refine_1 :
  ∀ (U : Set X) (hUo : IsOpen[inst_1] U) (hU : f ⁻¹' U = range (Sigma.mk (β := σ) i)),
    ∃ (U : Set X), IsOpen[inst_1] U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst (β := σ) = i
⊢ ∃ (U : Set X), IsOpen[inst_1] U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst (β := σ) = i

Tactic:
rcases h.isOpen_iff.1 (isOpen_range_sigmaMk (i := i)) with ⟨U, hUo, hU⟩

Premises used: Topology.IsInducing.isOpen_iff, Iff.mp, isOpen_range_sigmaMk
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
ι : Type u_5
σ : ι → Type u_7
inst : (i : ι) → TopologicalSpace (σ i)
inst_1 : TopologicalSpace X
f : Sigma σ → X
h : IsInducing f
i : ι
U : Set X
hUo : IsOpen[inst_1] U
hU : f ⁻¹' U = range (Sigma.mk (β := σ) i)
⊢ ∃ (U : Set X), IsOpen[inst_1] U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst (β := σ) = i

Tactic:
⟨U, hUo, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
ι : Type u_5
σ : ι → Type u_7
inst : (i : ι) → TopologicalSpace (σ i)
inst_1 : TopologicalSpace X
f : Sigma σ → X
h : IsInducing f
i : ι
U : Set X
hUo : IsOpen[inst_1] U
hU : f ⁻¹' U = range (Sigma.mk (β := σ) i)
refine_1 : ∀ (x : Sigma σ), f x ∈ U ↔ x.fst (β := σ) = i
⊢ ∃ (U : Set X), IsOpen[inst_1] U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst (β := σ) = i

Tactic:
refine ⟨U, hUo, ?_⟩
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
ι : Type u_5
σ : ι → Type u_7
inst : (i : ι) → TopologicalSpace (σ i)
inst_1 : TopologicalSpace X
f : Sigma σ → X
h : IsInducing f
i : ι
U : Set X
hUo : IsOpen[inst_1] U
hU : f ⁻¹' U = range (Sigma.mk (β := σ) i)
⊢ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst (β := σ) = i

Tactic:
simpa [Set.ext_iff] using hU

Premises used: Set.ext_iff
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
ι : Type u_5
σ : ι → Type u_7
inst : (i : ι) → TopologicalSpace (σ i)
inst_1 : TopologicalSpace X
f : Sigma σ → X
⊢ ((∀ (i : ι), IsInducing (f ∘ Sigma.mk (β := σ) i)) ∧
      ∀ (i : ι), ∃ (U : Set X), IsOpen[inst_1] U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst (β := σ) = i) →
    IsInducing f

Tactic:
fun ⟨h₁, h₂⟩ ↦ isInducing_iff_nhds.2 fun ⟨i, x⟩ ↦ ?_

Premises used: Iff.mpr, nhds, Topology.IsInducing, Topology.isInducing_iff_nhds, _private.0.inducing_sigma.match_1, Eq, _private.0.inducing_sigma.match_2, Filter.comap
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
ι : Type u_5
σ : ι → Type u_7
inst : (i : ι) → TopologicalSpace (σ i)
inst_1 : TopologicalSpace X
f : Sigma σ → X
refine_2 :
  ((∀ (i : ι), IsInducing (f ∘ Sigma.mk (β := σ) i)) ∧
      ∀ (i : ι), ∃ (U : Set X), IsOpen[inst_1] U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst (β := σ) = i) →
    ∀ (h₁ : ∀ (i : ι), IsInducing (f ∘ Sigma.mk (β := σ) i))
      (h₂ : ∀ (i : ι), ∃ (U : Set X), IsOpen[inst_1] U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst (β := σ) = i) (x : Sigma σ)
      (i : ι) (x : σ i), 𝓝 (Sigma.mk (β := σ) i x) = comap f (𝓝 (f (Sigma.mk (β := σ) i x)))
⊢ ((∀ (i : ι), IsInducing (f ∘ Sigma.mk (β := σ) i)) ∧
      ∀ (i : ι), ∃ (U : Set X), IsOpen[inst_1] U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst (β := σ) = i) →
    IsInducing f

Tactic:
refine fun ⟨h₁, h₂⟩ ↦ isInducing_iff_nhds.2 fun ⟨i, x⟩ ↦ ?_
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
ι : Type u_5
σ : ι → Type u_7
inst : (i : ι) → TopologicalSpace (σ i)
inst_1 : TopologicalSpace X
f : Sigma σ → X
h :
  (∀ (i : ι), IsInducing (f ∘ Sigma.mk (β := σ) i)) ∧
    ∀ (i : ι), ∃ (U : Set X), IsOpen[inst_1] U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst (β := σ) = i
h₁ : ∀ (i : ι), IsInducing (f ∘ Sigma.mk (β := σ) i)
h₂ : ∀ (i : ι), ∃ (U : Set X), IsOpen[inst_1] U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst (β := σ) = i
x_1 : Sigma σ
i : ι
x : σ i
refine_2 : range (Sigma.mk (β := σ) i) ∈ comap f (𝓝 (f (Sigma.mk (β := σ) i x)))
⊢ 𝓝 (Sigma.mk (β := σ) i x) = comap f (𝓝 (f (Sigma.mk (β := σ) i x)))

Tactic:
rw [Sigma.nhds_mk, (h₁ i).nhds_eq_comap, comp_apply, ← comap_comap, map_comap_of_mem]

Premises used: Topology.IsInducing.nhds_eq_comap, Filter.map_comap_of_mem, Sigma.nhds_mk, Filter.comap_comap, Function.comp_apply
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
ι : Type u_5
σ : ι → Type u_7
inst : (i : ι) → TopologicalSpace (σ i)
inst_1 : TopologicalSpace X
f : Sigma σ → X
h :
  (∀ (i : ι), IsInducing (f ∘ Sigma.mk (β := σ) i)) ∧
    ∀ (i : ι), ∃ (U : Set X), IsOpen[inst_1] U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst (β := σ) = i
h₁ : ∀ (i : ι), IsInducing (f ∘ Sigma.mk (β := σ) i)
h₂ : ∀ (i : ι), ∃ (U : Set X), IsOpen[inst_1] U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst (β := σ) = i
x_1 : Sigma σ
i : ι
x : σ i
refine_2 :
  ∀ (U : Set X) (hUo : IsOpen[inst_1] U) (hU : ∀ (x : Sigma σ), f x ∈ U ↔ x.fst (β := σ) = i),
    range (Sigma.mk (β := σ) i) ∈ comap f (𝓝 (f (Sigma.mk (β := σ) i x)))
⊢ range (Sigma.mk (β := σ) i) ∈ comap f (𝓝 (f (Sigma.mk (β := σ) i x)))

Tactic:
rcases h₂ i with ⟨U, hUo, hU⟩
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
ι : Type u_5
σ : ι → Type u_7
inst : (i : ι) → TopologicalSpace (σ i)
inst_1 : TopologicalSpace X
f : Sigma σ → X
h_1 :
  (∀ (i : ι), IsInducing (f ∘ Sigma.mk (β := σ) i)) ∧
    ∀ (i : ι), ∃ (U : Set X), IsOpen[inst_1] U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst (β := σ) = i
h₁ : ∀ (i : ι), IsInducing (f ∘ Sigma.mk (β := σ) i)
h₂ : ∀ (i : ι), ∃ (U : Set X), IsOpen[inst_1] U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst (β := σ) = i
x_1 : Sigma σ
i : ι
x : σ i
U : Set X
hUo : IsOpen[inst_1] U
hU : ∀ (x : Sigma σ), f x ∈ U ↔ x.fst (β := σ) = i
h : ∀ (y : Sigma σ) (hy : y ∈ f ⁻¹' U), Membership.mem (γ := Set (Sigma σ)) (range (Sigma.mk (β := σ) i)) y
⊢ range (Sigma.mk (β := σ) i) ∈ comap f (𝓝 (f (Sigma.mk (β := σ) i x)))

Tactic:
filter_upwards [preimage_mem_comap <| hUo.mem_nhds <| (hU _).2 rfl] with y hy

Premises used: Iff.mpr, IsOpen.mem_nhds, Filter.preimage_mem_comap
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
ι : Type u_5
σ : ι → Type u_7
inst : (i : ι) → TopologicalSpace (σ i)
inst_1 : TopologicalSpace X
f : Sigma σ → X
h :
  (∀ (i : ι), IsInducing (f ∘ Sigma.mk (β := σ) i)) ∧
    ∀ (i : ι), ∃ (U : Set X), IsOpen[inst_1] U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst (β := σ) = i
h₁ : ∀ (i : ι), IsInducing (f ∘ Sigma.mk (β := σ) i)
h₂ : ∀ (i : ι), ∃ (U : Set X), IsOpen[inst_1] U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst (β := σ) = i
x_1 : Sigma σ
i : ι
x : σ i
U : Set X
hUo : IsOpen[inst_1] U
hU : ∀ (x : Sigma σ), f x ∈ U ↔ x.fst (β := σ) = i
y : Sigma σ
hy : y ∈ f ⁻¹' U
⊢ Membership.mem (γ := Set (Sigma σ)) (range (Sigma.mk (β := σ) i)) y

Tactic:
simpa [hU] using hy
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
κ : Type u_6
σ : ι → Type u_7
τ : κ → Type u_8
inst : (i : ι) → TopologicalSpace (σ i)
inst_1 : (k : κ) → TopologicalSpace (τ k)
f₁ : ι → κ
f₂ : (i : ι) → σ i → τ (f₁ i)
⊢ (∀ (i : ι),
      Continuous[inst i, instTopologicalSpaceSigma] fun (a : σ i) ↦
        Sigma.map (β₁ := σ) (β₂ := τ) f₁ f₂ (Sigma.mk (β := σ) i a)) ↔
    ∀ (i : ι), Continuous[inst i, inst_1 (f₁ i)] (f₂ i)

Tactic:
simp only [Sigma.map, IsEmbedding.sigmaMk.continuous_iff, comp_def]

Premises used: Topology.IsEmbedding.sigmaMk, Function.comp_def, Sigma.map, Topology.IsEmbedding.continuous_iff
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
κ : Type u_6
σ : ι → Type u_7
τ : κ → Type u_8
inst : (i : ι) → TopologicalSpace (σ i)
inst_1 : (k : κ) → TopologicalSpace (τ k)
f₁ : ι → κ
f₂ : (i : ι) → σ i → τ (f₁ i)
hf : ∀ (i : ι), Continuous[inst i, inst_1 (f₁ i)] (f₂ i)
⊢ Continuous[instTopologicalSpaceSigma, instTopologicalSpaceSigma] (Sigma.map (β₁ := σ) (β₂ := τ) f₁ f₂)

Tactic:
continuous_sigma_map.2 hf

Premises used: Iff.mpr, continuous_sigma_map
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
ι : Type u_5
σ : ι → Type u_7
inst : (i : ι) → TopologicalSpace (σ i)
inst_1 : TopologicalSpace X
f : Sigma σ → X
⊢ IsOpenMap f ↔ ∀ (i : ι), IsOpenMap.{u_7, u} (Y := X) fun (a : σ i) ↦ f (Sigma.mk (β := σ) i a)

Tactic:
simp only [isOpenMap_iff_nhds_le, Sigma.forall, Sigma.nhds_eq, map_map, comp_def]

Premises used: isOpenMap_iff_nhds_le, Filter.map_map, Sigma.forall, Function.comp_def, Sigma.nhds_eq
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
κ : Type u_6
σ : ι → Type u_7
τ : κ → Type u_8
inst : (i : ι) → TopologicalSpace (σ i)
inst_1 : (k : κ) → TopologicalSpace (τ k)
f₁ : ι → κ
f₂ : (i : ι) → σ i → τ (f₁ i)
⊢ IsOpenMap (Sigma.map (β₁ := σ) (β₂ := τ) f₁ f₂) ↔ ∀ (i : ι), IsOpenMap (f₂ i)

Tactic:
isOpenMap_sigma.trans <|
    forall_congr' fun i => (@IsOpenEmbedding.sigmaMk _ _ _ (f₁ i)).isOpenMap_iff.symm

Premises used: Topology.IsOpenEmbedding.isOpenMap_iff, forall_congr', Topology.IsOpenEmbedding.sigmaMk, Iff.trans, isOpenMap_sigma, Iff.symm
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
κ : Type u_6
σ : ι → Type u_7
τ : κ → Type u_8
inst : (i : ι) → TopologicalSpace (σ i)
inst_1 : (k : κ) → TopologicalSpace (τ k)
f₁ : ι → κ
f₂ : (i : ι) → σ i → τ (f₁ i)
h₁ : Injective f₁
⊢ IsInducing (Sigma.map (β₁ := σ) (β₂ := τ) f₁ f₂) ↔ ∀ (i : ι), IsInducing (f₂ i)

Tactic:
simp only [isInducing_iff_nhds, Sigma.forall, Sigma.nhds_mk, Sigma.map_mk,
    ← map_sigma_mk_comap h₁, map_inj sigma_mk_injective]

Premises used: Sigma.forall, Filter.map_sigma_mk_comap, Topology.isInducing_iff_nhds, Sigma.nhds_mk, Sigma.map_mk, Filter.map_inj, sigma_mk_injective
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
κ : Type u_6
σ : ι → Type u_7
τ : κ → Type u_8
inst : (i : ι) → TopologicalSpace (σ i)
inst_1 : (k : κ) → TopologicalSpace (τ k)
f₁ : ι → κ
f₂ : (i : ι) → σ i → τ (f₁ i)
h : Injective f₁
⊢ IsEmbedding (Sigma.map (β₁ := σ) (β₂ := τ) f₁ f₂) ↔ ∀ (i : ι), IsEmbedding (f₂ i)

Tactic:
simp only [isEmbedding_iff, isInducing_sigmaMap h, forall_and,
    h.sigma_map_iff]

Premises used: Function.Injective.sigma_map_iff, Topology.isEmbedding_iff, Topology.isInducing_sigmaMap, forall_and
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
κ : Type u_6
σ : ι → Type u_7
τ : κ → Type u_8
inst : (i : ι) → TopologicalSpace (σ i)
inst_1 : (k : κ) → TopologicalSpace (τ k)
f₁ : ι → κ
f₂ : (i : ι) → σ i → τ (f₁ i)
h : Injective f₁
⊢ IsOpenEmbedding (Sigma.map (β₁ := σ) (β₂ := τ) f₁ f₂) ↔ ∀ (i : ι), IsOpenEmbedding (f₂ i)

Tactic:
simp only [isOpenEmbedding_iff_isEmbedding_isOpenMap, isOpenMap_sigma_map, isEmbedding_sigmaMap h,
    forall_and]

Premises used: isOpenMap_sigma_map, Topology.isEmbedding_sigmaMap, Topology.isOpenEmbedding_iff_isEmbedding_isOpenMap, forall_and
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
s : Set (ULift.{v, u} X)
rw : IsOpen[induced down inst] s ↔ IsOpen[inst] (up ⁻¹' s)
rw₁ : IsOpen[induced (⇑Equiv.ulift : (a : ULift.{v, u} X) → X) inst] s ↔ IsOpen[inst] (up ⁻¹' s)
rw₂ : IsOpen[coinduced (⇑Equiv.ulift.symm : (a : X) → ULift.{v, u} X) inst] s ↔ IsOpen[inst] (up ⁻¹' s)
rw₃ rw₄ : IsOpen[coinduced (⇑Equiv.ulift.symm : (a : X) → ULift.{v, u} X) inst] s ↔ IsOpen[coinduced up inst] s
⊢ IsOpen[topologicalSpace] s ↔ IsOpen[inst] (up ⁻¹' s)

Tactic:
rw [ULift.topologicalSpace, ← Equiv.ulift_apply, ← Equiv.ulift.coinduced_symm, ← isOpen_coinduced]

Premises used: ULift.topologicalSpace, Equiv.ulift_apply, Equiv.ulift, isOpen_coinduced, Equiv.coinduced_symm
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
s : Set (ULift.{v, u} X)
rw : IsOpen[topologicalSpace] sᶜ ↔ IsClosed[inst] (up ⁻¹' s)
rw₁ : IsOpen[topologicalSpace] sᶜ ↔ IsOpen[inst] (up ⁻¹' s)ᶜ
rw₂ : IsOpen[inst] (up ⁻¹' sᶜ) ↔ IsOpen[inst] (up ⁻¹' s)ᶜ
rw₃ rw₄ : IsOpen[inst] (up ⁻¹' s)ᶜ ↔ IsOpen[inst] (up ⁻¹' s)ᶜ
⊢ IsClosed[topologicalSpace] s ↔ IsClosed[inst] (up ⁻¹' s)

Tactic:
rw [← isOpen_compl_iff, ← isOpen_compl_iff, isOpen_iff, preimage_compl]

Premises used: Set.preimage_compl, isOpen_compl_iff, ULift.isOpen_iff
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
⊢ Continuous[ULift.topologicalSpace, inst] ULift.down

Tactic:
continuous_induced_dom

Premises used: continuous_induced_dom
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
⊢ Continuous[inst, ULift.topologicalSpace] ULift.up

Tactic:
continuous_induced_rng.2 continuous_id

Premises used: Iff.mpr, continuous_id, continuous_induced_rng
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : Continuous[inst, inst_1] f
change : Continuous[ULift.topologicalSpace, ULift.topologicalSpace] (ULift.up ∘ f ∘ ULift.down)
⊢ Continuous[ULift.topologicalSpace, ULift.topologicalSpace] (ULift.map f)

Tactic:
change Continuous (ULift.up ∘ f ∘ ULift.down)

Premises used: Continuous, Function.comp, ULift.up, ULift.down
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : Continuous[inst, inst_1] f
⊢ Continuous[ULift.topologicalSpace, ULift.topologicalSpace] (ULift.up ∘ f ∘ ULift.down)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
⊢ IsEmbedding (X := ULift.{v, u} X) ULift.down

Tactic:
⟨⟨rfl⟩, ULift.down_injective⟩

Premises used: Topology.IsInducing.mk, ULift.down_injective, rfl, Topology.IsEmbedding.mk
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
⊢ IsClosed[inst] (range ULift.down)

Tactic:
simp only [ULift.down_surjective.range_eq, isClosed_univ]

Premises used: isClosed_univ, ULift.down_surjective, Function.Surjective.range_eq
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
Y : Type v
Z : Type u_1
W : Type u_2
ε : Type u_3
ζ : Type u_4
inst : TopologicalSpace X
inst_1 : DiscreteTopology X
⊢ DiscreteTopology (ULift.{u_5, u} X)

Tactic:
IsEmbedding.uliftDown.discreteTopology

Premises used: Topology.IsEmbedding.uliftDown, Topology.IsEmbedding.discreteTopology