awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
s : Set (CofiniteTopology X)
simp_rw :
  IsOpen[TopologicalSpace.cofinite] (WithTopology.toTopology TopologicalSpace.cofinite ⁻¹' s) ↔ s.Nonempty → sᶜ.Finite
simp_rw₁ :
  IsOpen[TopologicalSpace.cofinite]
      (WithTopology.toTopology
          { IsOpen := fun (s : Set X) ↦ s.Nonempty → sᶜ.Finite, isOpen_univ := ⋯, isOpen_inter := ⋯,
            isOpen_sUnion := ⋯ : TopologicalSpace X } ⁻¹'
        s) ↔
    s.Nonempty → sᶜ.Finite
simp_rw₂ :
  (WithTopology.toTopology
            { IsOpen := fun (s : Set X) ↦ s.Nonempty → sᶜ.Finite, isOpen_univ := ⋯, isOpen_inter := ⋯,
              isOpen_sUnion := ⋯ : TopologicalSpace X } ⁻¹'
          s).Nonempty →
      (WithTopology.toTopology
              { IsOpen := fun (s : Set X) ↦ s.Nonempty → sᶜ.Finite, isOpen_univ := ⋯, isOpen_inter := ⋯,
                isOpen_sUnion := ⋯ : TopologicalSpace X } ⁻¹'
            s)ᶜ.Finite ↔
    s.Nonempty → sᶜ.Finite
simp_rw₃ :
  (WithTopology.toTopology
            { IsOpen := fun (s : Set X) ↦ s.Nonempty → sᶜ.Finite, isOpen_univ := ⋯, isOpen_inter := ⋯,
              isOpen_sUnion := ⋯ : TopologicalSpace X } ⁻¹'
          s).Nonempty →
      (WithTopology.toTopology
            { IsOpen := fun (s : Set X) ↦ s.Nonempty → sᶜ.Finite, isOpen_univ := ⋯, isOpen_inter := ⋯,
              isOpen_sUnion := ⋯ : TopologicalSpace X } ⁻¹'
          sᶜ).Finite ↔
    s.Nonempty → sᶜ.Finite
simp_rw₄ : (WithTopology.ofTopology '' s).Nonempty → (WithTopology.ofTopology '' sᶜ).Finite ↔ s.Nonempty → sᶜ.Finite
simp_rw₅ : s.Nonempty → (WithTopology.ofTopology '' sᶜ).Finite ↔ s.Nonempty → sᶜ.Finite
⊢ IsOpen s ↔ s.Nonempty → sᶜ.Finite

Tactic:
simp_rw [isOpen_coinduced, TopologicalSpace.cofinite, isOpen_mk, ← Set.preimage_compl,
    WithTopology.preimage_toTopology, image_nonempty,
    finite_image_iff (WithTopology.ofTopology_injective _).injOn]

Premises used: Set.image_nonempty, TopologicalSpace.cofinite, Function.Injective.injOn, WithTopology.ofTopology_injective, isOpen_coinduced, Set.finite_image_iff, Set.preimage_compl, WithTopology.preimage_toTopology, isOpen_mk
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
s : Set (CofiniteTopology X)
⊢ IsOpen s ↔ s = ∅ ∨ sᶜ.Finite

Tactic:
simp only [isOpen_iff, nonempty_iff_ne_empty, or_iff_not_imp_left]

Premises used: Classical.or_iff_not_imp_left, Set.nonempty_iff_ne_empty, CofiniteTopology.isOpen_iff
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
s : Set (CofiniteTopology X)
⊢ IsClosed s ↔ s = univ ∨ s.Finite

Tactic:
simp only [← isOpen_compl_iff, isOpen_iff', compl_compl, compl_empty_iff]

Premises used: compl_compl, Set.compl_empty_iff, CofiniteTopology.isOpen_iff', isOpen_compl_iff
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
x : CofiniteTopology X
h : ∀ (U : Set (CofiniteTopology X)), U ∈ 𝓝 x ↔ U ∈ pure x ⊔ cofinite
⊢ 𝓝 x = pure x ⊔ cofinite

Tactic:
ext U
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
x : CofiniteTopology X
U : Set (CofiniteTopology X)
h : (∃ t ⊆ U, (t.Nonempty → tᶜ.Finite) ∧ x ∈ t) ↔ U ∈ pure x ⊔ cofinite
⊢ U ∈ 𝓝 x ↔ U ∈ pure x ⊔ cofinite

Tactic:
simp_rw [mem_nhds_iff, isOpen_iff]

Premises used: mem_nhds_iff, CofiniteTopology.isOpen_iff
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
x : CofiniteTopology X
U : Set (CofiniteTopology X)
h : (∃ t ⊆ U, (t.Nonempty → tᶜ.Finite) ∧ x ∈ t) → U ∈ pure x ⊔ cofinite
h₁ : U ∈ pure x ⊔ cofinite → ∃ t ⊆ U, (t.Nonempty → tᶜ.Finite) ∧ x ∈ t
⊢ (∃ t ⊆ U, (t.Nonempty → tᶜ.Finite) ∧ x ∈ t) ↔ U ∈ pure x ⊔ cofinite

Tactic:
constructor
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
x : CofiniteTopology X
U V : Set (CofiniteTopology X)
hVU : V ⊆ U
V_op : V.Nonempty → Vᶜ.Finite
haV : x ∈ V
⊢ U ∈ pure x ⊔ cofinite

Tactic:
mem_sup.mpr ⟨hVU haV, mem_of_superset (V_op ⟨_, haV⟩) hVU⟩

Premises used: Iff.mpr, Filter.mem_sup, And.intro, Exists.intro, Filter.mem_of_superset
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
x : CofiniteTopology X
U V : Set (CofiniteTopology X)
hVU : V ⊆ U
V_op : V.Nonempty → Vᶜ.Finite
haV : x ∈ V
⊢ U ∈ pure x ⊔ cofinite

Tactic:
exact mem_sup.mpr ⟨hVU haV, mem_of_superset (V_op ⟨_, haV⟩) hVU⟩

Premises used: Iff.mpr, Filter.mem_sup, And.intro, Filter.mem_of_superset
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
x : CofiniteTopology X
U : Set (CofiniteTopology X)
hU : x ∈ U
hU' : Uᶜ.Finite
⊢ ∃ t ⊆ U, (t.Nonempty → tᶜ.Finite) ∧ x ∈ t

Tactic:
⟨U, Subset.rfl, fun _ => hU', hU⟩

Premises used: Set.Subset.rfl, And.intro, Exists.intro
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
x : CofiniteTopology X
U : Set (CofiniteTopology X)
hU : x ∈ U
hU' : Uᶜ.Finite
⊢ ∃ t ⊆ U, (t.Nonempty → tᶜ.Finite) ∧ x ∈ t

Tactic:
exact ⟨U, Subset.rfl, fun _ => hU', hU⟩
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
x : CofiniteTopology X
s : Set (CofiniteTopology X)
⊢ s ∈ 𝓝 x ↔ x ∈ s ∧ sᶜ.Finite

Tactic:
simp [nhds_eq]

Premises used: CofiniteTopology.nhds_eq
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
α : Type u_5
β : Type u_6
f : α → X
g : β → Y
la : Filter α
lb : Filter β
x : X
y : Y
hf : MapClusterPt x la f
hg : MapClusterPt y lb g
⊢ ∀ s ∈ 𝓝 x, ∃ᶠ (a : α) in la, f a ∈ s

Tactic:
rw [mapClusterPt_iff_frequently] at hf hg

Premises used: mapClusterPt_iff_frequently
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
α : Type u_5
β : Type u_6
f : α → X
g : β → Y
la : Filter α
lb : Filter β
x : X
y : Y
hf : MapClusterPt x la f
hg : MapClusterPt y lb g
hf₁ : ∀ s ∈ 𝓝 x, ∃ᶠ (a : α) in la, f a ∈ s
⊢ ∀ s ∈ 𝓝 y, ∃ᶠ (a : β) in lb, g a ∈ s

Tactic:
rw [mapClusterPt_iff_frequently] at hf hg

Premises used: mapClusterPt_iff_frequently
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
α : Type u_5
β : Type u_6
f : α → X
g : β → Y
la : Filter α
lb : Filter β
x : X
y : Y
hf : ∀ s ∈ 𝓝 x, ∃ᶠ (a : α) in la, f a ∈ s
hg : ∀ s ∈ 𝓝 y, ∃ᶠ (a : β) in lb, g a ∈ s
rw :
  ∀ (i : Prod.{u, v} (Set X) (Set Y)),
    i.1 ∈ 𝓝 x ∧ i.2 ∈ 𝓝 y → ∃ᶠ (a : α × β) in la.curry lb, Prod.map f g a ∈ id i.1 ×ˢ id i.2
⊢ MapClusterPt (x, y) (la.curry lb) (Prod.map f g)

Tactic:
rw [((𝓝 x).basis_sets.prod_nhds (𝓝 y).basis_sets).mapClusterPt_iff_frequently]

Premises used: nhds, Filter.basis_sets, Filter.HasBasis.prod_nhds, Filter.HasBasis.mapClusterPt_iff_frequently
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
α : Type u_5
β : Type u_6
f : α → X
g : β → Y
la : Filter α
lb : Filter β
x : X
y : Y
hf : ∀ s ∈ 𝓝 x, ∃ᶠ (a : α) in la, f a ∈ s
hg : ∀ s ∈ 𝓝 y, ∃ᶠ (a : β) in lb, g a ∈ s
s : Set X
t : Set Y
hs : (s, t).1 ∈ 𝓝 x
ht : (s, t).2 ∈ 𝓝 y
rw : ∃ᶠ (x : α) in la, ∃ᶠ (y : β) in lb, Prod.map f g (x, y) ∈ id (s, t).1 ×ˢ id (s, t).2
⊢ ∃ᶠ (a : α × β) in la.curry lb, Prod.map f g a ∈ id (s, t).1 ×ˢ id (s, t).2

Tactic:
rw [frequently_curry_iff]

Premises used: Filter.frequently_curry_iff
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
α : Type u_5
β : Type u_6
f : α → X
g : β → Y
la : Filter α
lb : Filter β
x : X
y : Y
hf : ∀ s ∈ 𝓝 x, ∃ᶠ (a : α) in la, f a ∈ s
hg : ∀ s ∈ 𝓝 y, ∃ᶠ (a : β) in lb, g a ∈ s
s : Set X
t : Set Y
hs : (s, t).1 ∈ 𝓝 x
ht : (s, t).2 ∈ 𝓝 y
⊢ ∃ᶠ (x : α) in la, ∃ᶠ (y : β) in lb, Prod.map f g (x, y) ∈ id (s, t).1 ×ˢ id (s, t).2

Tactic:
(hf s hs).mono fun x hx ↦ (hg t ht).mono fun y hy ↦ ⟨hx, hy⟩

Premises used: Filter.Frequently.mono, And.intro
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
α : Type u_5
β : Type u_6
f : α → X
g : β → Y
la : Filter α
lb : Filter β
x : X
y : Y
hf : ∀ s ∈ 𝓝 x, ∃ᶠ (a : α) in la, f a ∈ s
hg : ∀ s ∈ 𝓝 y, ∃ᶠ (a : β) in lb, g a ∈ s
s : Set X
t : Set Y
hs : (s, t).1 ∈ 𝓝 x
ht : (s, t).2 ∈ 𝓝 y
⊢ ∃ᶠ (x : α) in la, ∃ᶠ (y : β) in lb, Prod.map f g (x, y) ∈ id (s, t).1 ×ˢ id (s, t).2

Tactic:
exact (hf s hs).mono fun x hx ↦ (hg t ht).mono fun y hy ↦ ⟨hx, hy⟩

Premises used: Filter.Frequently.mono
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
α : Type u_5
β : Type u_6
f : α → X
g : β → Y
la : Filter α
lb : Filter β
x : X
y : Y
hf : MapClusterPt x la f
hg : MapClusterPt y lb g
⊢ MapClusterPt (x, y) (la ×ˢ lb) (Prod.map f g)

Tactic:
(hf.curry_prodMap hg).mono <| map_mono curry_le_prod

Premises used: Filter.map_mono, Filter.curry_le_prod, MapClusterPt.mono, MapClusterPt.curry_prodMap
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
f : X → Bool
b : Bool
rw : (∀ (b : Bool), IsOpen[inst] (f ⁻¹' {b})) ↔ IsClopen (f ⁻¹' {b})
rw₁ : IsOpen[inst] (f ⁻¹' {b}) ∧ IsOpen[inst] (f ⁻¹' {!b}) ↔ IsClopen (f ⁻¹' {b})
rw₂ : IsOpen[inst] (f ⁻¹' {b}) ∧ IsOpen[inst] (f ⁻¹' {!b}) ↔ IsClosed[inst] (f ⁻¹' {b}) ∧ IsOpen[inst] (f ⁻¹' {b})
rw₃ : IsOpen[inst] (f ⁻¹' {b}) ∧ IsOpen[inst] (f ⁻¹' {!b}) ↔ IsOpen[inst] (f ⁻¹' {b})ᶜ ∧ IsOpen[inst] (f ⁻¹' {b})
rw₄ : IsOpen[inst] (f ⁻¹' {b}) ∧ IsOpen[inst] (f ⁻¹' {!b}) ↔ IsOpen[inst] (f ⁻¹' {b}ᶜ) ∧ IsOpen[inst] (f ⁻¹' {b})
rw₅ : IsOpen[inst] (f ⁻¹' {b}) ∧ IsOpen[inst] (f ⁻¹' {!b}) ↔ IsOpen[inst] (f ⁻¹' {!b}) ∧ IsOpen[inst] (f ⁻¹' {b})
rw₆ rw₇ : IsOpen[inst] (f ⁻¹' {!b}) ∧ IsOpen[inst] (f ⁻¹' {b}) ↔ IsOpen[inst] (f ⁻¹' {!b}) ∧ IsOpen[inst] (f ⁻¹' {b})
⊢ Continuous[inst, _] f ↔ IsClopen (f ⁻¹' {b})

Tactic:
rw [continuous_discrete_rng, Bool.forall_bool' b, IsClopen, ← isOpen_compl_iff, ← preimage_compl,
    Bool.compl_singleton, and_comm]

Premises used: Bool.forall_bool', Bool.compl_singleton, and_comm, Set.preimage_compl, IsClopen, isOpen_compl_iff, continuous_discrete_rng
-- Module: Mathlib.Topology.Constructions
Goal:
Y : Type v
inst : TopologicalSpace Y
t : Set Y
⊢ IsInducing.{v, v} (X := { x : Y // x ∈ t }) (Subtype.val (p := fun (x : Y) ↦ x ∈ t))

Tactic:
⟨rfl⟩

Premises used: Topology.IsInducing.mk, rfl
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
t : Set Y
ht : ∀ (x : X), f x ∈ t
h : IsInducing (codRestrict f t ht)
⊢ IsInducing f

Tactic:
subtypeVal.comp h

Premises used: Topology.IsInducing.comp, Topology.IsInducing.subtypeVal
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
p : X → Prop
⊢ IsEmbedding.{u, u} (X := Subtype p) (Subtype.val (p := p))

Tactic:
⟨.subtypeVal, Subtype.coe_injective⟩

Premises used: Subtype.coe_injective, Topology.IsInducing.subtypeVal, Topology.IsEmbedding.mk
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
p : X → Prop
h rwa rwa₁ rwa₂ rwa₃ : IsClosed[inst] {x : X | p x}
⊢ IsClosed[inst] (range (ι := Subtype p) (Subtype.val (p := p)))

Tactic:
rwa [Subtype.range_coe_subtype]

Premises used: Subtype.range_coe_subtype
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
p : X → Prop
⊢ Continuous[instTopologicalSpaceSubtype, inst] (Subtype.val (p := p))

Tactic:
continuous_induced_dom

Premises used: continuous_induced_dom
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
p : X → Prop
f : Y → Subtype p
hf : Continuous[inst_1, instTopologicalSpaceSubtype] f
⊢ Continuous[inst_1, inst] fun (x : Y) ↦ (↑(f x) : X)

Tactic:
continuous_subtype_val.comp hf

Premises used: continuous_subtype_val, Continuous.comp
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsOpen[inst] s
⊢ IsOpenEmbedding.{u, u} (X := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s))

Tactic:
⟨.subtypeVal, (@Subtype.range_coe _ s).symm ▸ hs⟩

Premises used: Eq.rec, Subtype.range_coe, Topology.IsEmbedding.subtypeVal, Eq.symm, Topology.IsOpenEmbedding.mk
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsOpen[inst] s
⊢ IsOpenMap.{u, u} (X := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s))

Tactic:
hs.isOpenEmbedding_subtypeVal.isOpenMap

Premises used: IsOpen.isOpenEmbedding_subtypeVal, Topology.IsOpenEmbedding.isOpenMap
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsOpenMap f
s : Set X
hs : IsOpen[inst] s
⊢ IsOpenMap (s.restrict (π := fun (a : X) ↦ Y) f)

Tactic:
hf.comp hs.isOpenMap_subtype_val

Premises used: IsOpenMap.comp, Set.restrict, IsOpen.isOpenMap_subtype_val
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsClosed[inst] s
⊢ IsClosedEmbedding.{u, u} (X := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s))

Tactic:
.subtypeVal hs

Premises used: Topology.IsClosedEmbedding.subtypeVal
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsClosed[inst] s
⊢ IsClosedMap.{u, u} (X := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s))

Tactic:
hs.isClosedEmbedding_subtypeVal.isClosedMap

Premises used: Topology.IsClosedEmbedding.isClosedMap, IsClosed.isClosedEmbedding_subtypeVal
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsClosedMap f
s : Set X
hs : IsClosed[inst] s
⊢ IsClosedMap (s.restrict (π := fun (a : X) ↦ Y) f)

Tactic:
hf.comp hs.isClosedMap_subtype_val

Premises used: IsClosed.isClosedMap_subtype_val, IsClosedMap.comp, Set.restrict
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
p : X → Prop
f : Y → X
h : Continuous[inst_1, inst] f
hp : ∀ (x : Y), p (f x)
⊢ Continuous[inst_1, instTopologicalSpaceSubtype] fun (x : Y) ↦ Subtype.mk (p := p) (f x) ⋯

Tactic:
continuous_induced_rng.2 h

Premises used: Iff.mpr, continuous_induced_rng
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
p : X → Prop
f : Y → X
hf : IsOpenMap f
hp : ∀ (x : Y), p (f x)
u : Set Y
hu : IsOpen[inst_1] u
⊢ IsOpen[instTopologicalSpaceSubtype] (Subtype.val (p := p) ⁻¹' f '' u)

Tactic:
(hf u hu).preimage continuous_subtype_val

Premises used: continuous_subtype_val, IsOpen.preimage
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
p : X → Prop
f : Y → X
hf : IsOpenMap f
hp : ∀ (x : Y), p (f x)
u : Set Y
hu : IsOpen[inst_1] u
h : Eq (α := Set (Subtype p)) ((fun (x : Y) ↦ Subtype.mk (p := p) (f x) ⋯) '' u) (Subtype.val (p := p) ⁻¹' f '' u)
⊢ IsOpen[instTopologicalSpaceSubtype] ((fun (x : Y) ↦ Subtype.mk (p := p) (f x) ⋯) '' u)

Tactic:
convert! (hf u hu).preimage continuous_subtype_val

Premises used: continuous_subtype_val, IsOpen.preimage
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
p : X → Prop
f : Y → X
hf : IsOpenMap f
hp : ∀ (x : Y), p (f x)
u : Set Y
hu : IsOpen[inst_1] u
⊢ Eq (α := Set (Subtype p)) ((fun (x : Y) ↦ Subtype.mk (p := p) (f x) ⋯) '' u) (Subtype.val (p := p) ⁻¹' f '' u)

Tactic:
Set.ext fun _ ↦ exists_congr fun _ ↦ and_congr_right' Subtype.ext_iff

Premises used: Set.ext, and_congr_right', Subtype.ext_iff, exists_congr
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
p : X → Prop
f : Y → X
hf : IsOpenMap f
hp : ∀ (x : Y), p (f x)
u : Set Y
hu : IsOpen[inst_1] u
⊢ Eq (α := Set (Subtype p)) ((fun (x : Y) ↦ Subtype.mk (p := p) (f x) ⋯) '' u) (Subtype.val (p := p) ⁻¹' f '' u)

Tactic:
exact Set.ext fun _ ↦ exists_congr fun _ ↦ and_congr_right' Subtype.ext_iff

Premises used: Set.ext, and_congr_right', Subtype.ext_iff, exists_congr
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
p : X → Prop
f : Y → X
hf : IsClosedMap f
hp : ∀ (x : Y), p (f x)
u : Set Y
hu : IsClosed[inst_1] u
⊢ IsClosed[instTopologicalSpaceSubtype] (Subtype.val (p := p) ⁻¹' f '' u)

Tactic:
(hf u hu).preimage continuous_subtype_val

Premises used: continuous_subtype_val, IsClosed.preimage
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
p : X → Prop
f : Y → X
hf : IsClosedMap f
hp : ∀ (x : Y), p (f x)
u : Set Y
hu : IsClosed[inst_1] u
h : Eq (α := Set (Subtype p)) ((fun (x : Y) ↦ Subtype.mk (p := p) (f x) ⋯) '' u) (Subtype.val (p := p) ⁻¹' f '' u)
⊢ IsClosed[instTopologicalSpaceSubtype] ((fun (x : Y) ↦ Subtype.mk (p := p) (f x) ⋯) '' u)

Tactic:
convert! (hf u hu).preimage continuous_subtype_val

Premises used: continuous_subtype_val, IsClosed.preimage
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
p : X → Prop
f : Y → X
hf : IsClosedMap f
hp : ∀ (x : Y), p (f x)
u : Set Y
hu : IsClosed[inst_1] u
⊢ Eq (α := Set (Subtype p)) ((fun (x : Y) ↦ Subtype.mk (p := p) (f x) ⋯) '' u) (Subtype.val (p := p) ⁻¹' f '' u)

Tactic:
Set.ext fun _ ↦ exists_congr fun _ ↦ and_congr_right' Subtype.ext_iff

Premises used: Set.ext, and_congr_right', Subtype.ext_iff, exists_congr
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
p : X → Prop
f : Y → X
hf : IsClosedMap f
hp : ∀ (x : Y), p (f x)
u : Set Y
hu : IsClosed[inst_1] u
⊢ Eq (α := Set (Subtype p)) ((fun (x : Y) ↦ Subtype.mk (p := p) (f x) ⋯) '' u) (Subtype.val (p := p) ⁻¹' f '' u)

Tactic:
exact Set.ext fun _ ↦ exists_congr fun _ ↦ and_congr_right' Subtype.ext_iff

Premises used: Set.ext, and_congr_right', Subtype.ext_iff, exists_congr
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
p : X → Prop
f : Y → X
hf : Continuous[inst_1, inst] f
hp : ∀ (x : Y), p (f x)
⊢ Continuous[inst_1, instTopologicalSpaceSubtype] (Subtype.coind f (p := p) hp)

Tactic:
hf.subtype_mk hp

Premises used: Continuous.subtype_mk, Subtype.coind
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
p : X → Prop
f : Y → X
hf : IsOpenMap f
hp : ∀ (x : Y), p (f x)
⊢ IsOpenMap (Subtype.coind f (p := p) hp)

Tactic:
hf.subtype_mk hp

Premises used: IsOpenMap.subtype_mk, Subtype.coind
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
p : X → Prop
f : Y → X
hf : IsClosedMap f
hp : ∀ (x : Y), p (f x)
⊢ IsClosedMap (Subtype.coind f (p := p) hp)

Tactic:
hf.subtype_mk hp

Premises used: IsClosedMap.subtype_mk, Subtype.coind
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
p : X → Prop
f : X → Y
h : Continuous[inst, inst_1] f
q : Y → Prop
hpq : ∀ (x : X), p x → q (f x)
⊢ Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (Subtype.map (p := p) (q := q) f hpq)

Tactic:
(h.comp continuous_subtype_val).subtype_mk _

Premises used: Subtype.map, continuous_subtype_val, Continuous.comp, Continuous.subtype_mk
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsOpenMap f
s : Set X
t : Set Y
hs : IsOpen[inst] s
hst : ∀ x ∈ s, f x ∈ t
⊢ IsOpenMap (Subtype.map (p := Membership.mem s) (q := Membership.mem t) f hst)

Tactic:
(hf.comp hs.isOpenMap_subtype_val).subtype_mk _

Premises used: Subtype.map, IsOpenMap.comp, IsOpenMap.subtype_mk, IsOpen.isOpenMap_subtype_val
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsClosedMap f
s : Set X
t : Set Y
hs : IsClosed[inst] s
hst : ∀ x ∈ s, f x ∈ t
⊢ IsClosedMap (Subtype.map (p := Membership.mem s) (q := Membership.mem t) f hst)

Tactic:
(hf.comp hs.isClosedMap_subtype_val).subtype_mk _

Premises used: Subtype.map, IsClosedMap.subtype_mk, IsClosed.isClosedMap_subtype_val, IsClosedMap.comp
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
h : s ⊆ t
⊢ Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (inclusion (s := s) (t := t) h)

Tactic:
continuous_id.subtype_map h

Premises used: Subtype.map, continuous_id, Continuous.subtype_map
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
hs : IsOpen[inst] s
h : s ⊆ t
⊢ IsOpenMap (inclusion (s := s) (t := t) h)

Tactic:
IsOpenMap.id.subtype_map hs h

Premises used: Subtype.map, IsOpenMap.subtype_map, IsOpenMap.id
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
hs : IsClosed[inst] s
h : s ⊆ t
⊢ IsClosedMap (inclusion (s := s) (t := t) h)

Tactic:
IsClosedMap.id.subtype_map hs h

Premises used: Subtype.map, IsClosedMap.subtype_map, IsClosedMap.id
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
⊢ Continuous[inst, instTopologicalSpaceSubtype] (rangeFactorization f) ↔ Continuous[inst, inst_1] f

Tactic:
IsInducing.subtypeVal.continuous_iff

Premises used: Topology.IsInducing.continuous_iff, Topology.IsInducing.subtypeVal
-- 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[inst, instTopologicalSpaceSubtype] (Set.rangeFactorization f)

Tactic:
continuous_rangeFactorization_iff.mpr hf

Premises used: Iff.mpr, continuous_rangeFactorization_iff
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
p : X → Prop
x : Subtype p
⊢ ContinuousAt (Subtype.val (p := p)) x

Tactic:
continuous_subtype_val.continuousAt

Premises used: continuous_subtype_val, Continuous.continuousAt
-- 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 : TopologicalSpace Y
p_1 p q : X → Prop
hpq : p = q
x : X
⊢ p x → q (id x)

Tactic:
simp [hpq]
-- 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 : TopologicalSpace Y
p_1 p q : X → Prop
hpq : p = q
x : X
⊢ q x → p (id x)

Tactic:
simp [hpq]
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
p q : X → Prop
hpq : p = q
⊢ toEquiv (ofEqSubtypes (p := p) (q := q) hpq) = Equiv.subtypeEquivProp (p := p) (q := q) hpq

Tactic:
rfl

Premises used: Equiv.subtypeEquiv, Equiv.subtypeEquivProp, rfl
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
t : Set (↑s : Type u)
rw :
  (∀ (x : X) (h : x ∈ s),
      (↑(mk (p := fun (x : X) ↦ x ∈ s) x h) : X) ∈ closure[inst] (val (p := fun (x : X) ↦ x ∈ s) '' t)) ↔
    s ⊆ closure[inst] ↑t
⊢ Dense t ↔ s ⊆ closure[inst] ↑t

Tactic:
rw [IsInducing.subtypeVal.dense_iff, SetCoe.forall]

Premises used: Topology.IsInducing.dense_iff, SetCoe.forall, Topology.IsInducing.subtypeVal
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
t : Set (↑s : Type u)
⊢ (∀ (x : X) (h : x ∈ s),
      (↑(mk (p := fun (x : X) ↦ x ∈ s) x h) : X) ∈ closure[inst] (val (p := fun (x : X) ↦ x ∈ s) '' t)) ↔
    s ⊆ closure[inst] ↑t

Tactic:
rfl