awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Maps.Proper.UniversallyClosed
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (X := X × Filter X) (Prod.map f id)
𝒰 : Ultrafilter X
F : Set (X × Filter X) := closure {xℱ : X × Filter X | xℱ.2 = pure xℱ.1}
this : IsClosed (Prod.map f id '' F)
x : X
hy : Tendsto f (↑𝒰 : Filter X) (nhds (f x))
hx :
  ∀ (t : Set (X × Filter X)),
    Membership.mem (γ := Filter (X × Filter X)) (nhds (x, 𝒰.1)) t →
      (t ∩ {xℱ : X × Filter X | xℱ.2 = pure xℱ.1}).Nonempty
U : Set X
hU : U ∈ nhds x
hUc : Uᶜ ∈ 𝒰
mpr : ∀ (z : X) (hz : z ∈ U) (hz' : Membership.mem (γ := Filter X) (pure z) Uᶜ), False
⊢ False

Tactic:
rcases hx (U ×ˢ {𝒢 | Uᶜ ∈ 𝒢}) (prod_mem_nhds hU (isOpen_setOf_mem.mem_nhds hUc)) with
      ⟨⟨z, 𝒢⟩, ⟨⟨hz : z ∈ U, hz' : Uᶜ ∈ 𝒢⟩, rfl : 𝒢 = pure z⟩⟩

Premises used: prod_mem_nhds, SProd.sprod, Compl.compl, setOf, Membership.mem, Filter.isOpen_setOf_mem, IsOpen.mem_nhds, rfl
-- Module: Mathlib.Topology.Maps.Proper.UniversallyClosed
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (X := X × Filter X) (Prod.map f id)
𝒰 : Ultrafilter X
F : Set (X × Filter X) := closure {xℱ : X × Filter X | xℱ.2 = pure xℱ.1}
this : IsClosed (Prod.map f id '' F)
x : X
hy : Tendsto f (↑𝒰 : Filter X) (nhds (f x))
hx :
  ∀ (t : Set (X × Filter X)),
    Membership.mem (γ := Filter (X × Filter X)) (nhds (x, 𝒰.1)) t →
      (t ∩ {xℱ : X × Filter X | xℱ.2 = pure xℱ.1}).Nonempty
U : Set X
hU : U ∈ nhds x
hUc : Uᶜ ∈ 𝒰
z : X
hz : z ∈ U
hz' : Membership.mem (γ := Filter X) (pure z) Uᶜ
⊢ False

Tactic:
hz' hz
-- Module: Mathlib.Topology.Maps.Proper.UniversallyClosed
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (X := X × Filter X) (Prod.map f id)
𝒰 : Ultrafilter X
F : Set (X × Filter X) := closure {xℱ : X × Filter X | xℱ.2 = pure xℱ.1}
this : IsClosed (Prod.map f id '' F)
x : X
hy : Tendsto f (↑𝒰 : Filter X) (nhds (f x))
hx :
  ∀ (t : Set (X × Filter X)),
    Membership.mem (γ := Filter (X × Filter X)) (nhds (x, 𝒰.1)) t →
      (t ∩ {xℱ : X × Filter X | xℱ.2 = pure xℱ.1}).Nonempty
U : Set X
hU : U ∈ nhds x
hUc : Uᶜ ∈ 𝒰
z : X
hz : z ∈ U
hz' : Membership.mem (γ := Filter X) (pure z) Uᶜ
⊢ False

Tactic:
exact hz' hz
-- Module: Mathlib.Topology.Maps.Proper.UniversallyClosed
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
mp : IsProperMap f → Continuous f ∧ IsClosedMap (X := X × Ultrafilter X) (Prod.map f id)
mpr : Continuous f ∧ IsClosedMap (X := X × Ultrafilter X) (Prod.map f id) → IsProperMap f
⊢ IsProperMap f ↔ Continuous f ∧ IsClosedMap (X := X × Ultrafilter X) (Prod.map f id)

Tactic:
constructor
-- Module: Mathlib.Topology.Maps.Proper.UniversallyClosed
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
H : IsProperMap f
⊢ Continuous f ∧ IsClosedMap (X := X × Ultrafilter X) (Prod.map f id)

Tactic:
⟨H.continuous, H.universally_closed _⟩

Premises used: IsProperMap.universally_closed, And.intro, IsProperMap.continuous
-- Module: Mathlib.Topology.Maps.Proper.UniversallyClosed
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
H : IsProperMap f
⊢ Continuous f ∧ IsClosedMap (X := X × Ultrafilter X) (Prod.map f id)

Tactic:
exact ⟨H.continuous, H.universally_closed _⟩
-- Module: Mathlib.Topology.Maps.Proper.UniversallyClosed
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (X := X × Ultrafilter X) (Prod.map f id)
mpr :
  Continuous f ∧
    ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰 : Filter X) (nhds y) → ∃ (x : X), f x = y ∧ (↑𝒰 : Filter X) ≤ nhds x
⊢ IsProperMap f

Tactic:
rw [isProperMap_iff_ultrafilter]

Premises used: isProperMap_iff_ultrafilter
-- Module: Mathlib.Topology.Maps.Proper.UniversallyClosed
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (X := X × Ultrafilter X) (Prod.map f id)
⊢ Continuous f ∧
    ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰 : Filter X) (nhds y) → ∃ (x : X), f x = y ∧ (↑𝒰 : Filter X) ≤ nhds x

Tactic:
⟨H.1, fun 𝒰 y hy ↦ ?_⟩

Premises used: And.left, And.intro
-- Module: Mathlib.Topology.Maps.Proper.UniversallyClosed
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (X := X × Ultrafilter X) (Prod.map f id)
mpr :
  ∀ (𝒰 : Ultrafilter X) (y : Y) (hy : Tendsto f (↑𝒰 : Filter X) (nhds y)), ∃ (x : X), f x = y ∧ (↑𝒰 : Filter X) ≤ nhds x
⊢ Continuous f ∧
    ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰 : Filter X) (nhds y) → ∃ (x : X), f x = y ∧ (↑𝒰 : Filter X) ≤ nhds x

Tactic:
refine ⟨H.1, fun 𝒰 y hy ↦ ?_⟩
-- Module: Mathlib.Topology.Maps.Proper.UniversallyClosed
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (X := X × Ultrafilter X) (Prod.map f id)
𝒰 : Ultrafilter X
y : Y
hy : Tendsto f (↑𝒰 : Filter X) (nhds y)
F : Set (X × Ultrafilter X) := closure {xℱ : X × Ultrafilter X | xℱ.2 = pure xℱ.1}
⊢ IsClosed (Prod.map f id '' F)

Tactic:
have := H.2 F isClosed_closure
-- Module: Mathlib.Topology.Maps.Proper.UniversallyClosed
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (X := X × Ultrafilter X) (Prod.map f id)
𝒰 : Ultrafilter X
y : Y
hy : Tendsto f (↑𝒰 : Filter X) (nhds y)
F : Set (X × Ultrafilter X) := closure {xℱ : X × Ultrafilter X | xℱ.2 = pure xℱ.1}
this : IsClosed (Prod.map f id '' F)
⊢ (y, 𝒰) ∈ Prod.map f id '' F

Tactic:
have : (y, 𝒰) ∈ Prod.map f id '' F :=
      this.mem_of_tendsto (hy.prodMk_nhds (Ultrafilter.tendsto_pure_self 𝒰))
        (Eventually.of_forall fun x ↦ ⟨⟨x, pure x⟩, subset_closure rfl, rfl⟩)
-- Module: Mathlib.Topology.Maps.Proper.UniversallyClosed
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (X := X × Ultrafilter X) (Prod.map f id)
𝒰 : Ultrafilter X
y : Y
hy : Tendsto f (↑𝒰 : Filter X) (nhds y)
F : Set (X × Ultrafilter X) := closure {xℱ : X × Ultrafilter X | xℱ.2 = pure xℱ.1}
this_1 : IsClosed (Prod.map f id '' F)
this : (y, 𝒰) ∈ Prod.map f id '' F
mpr :
  ∀ (x : X) (snd : Ultrafilter X) (hx : (x, snd) ∈ F) (hy : Tendsto f (↑(id snd) : Filter X) (nhds (f x))),
    ∃ (x_1 : X), f x_1 = f x ∧ (↑(id snd) : Filter X) ≤ nhds x_1
⊢ ∃ (x : X), f x = y ∧ (↑𝒰 : Filter X) ≤ nhds x

Tactic:
rcases this with ⟨⟨x, _⟩, hx, ⟨_, _⟩⟩
-- Module: Mathlib.Topology.Maps.Proper.UniversallyClosed
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (X := X × Ultrafilter X) (Prod.map f id)
F : Set (X × Ultrafilter X) := closure {xℱ : X × Ultrafilter X | xℱ.2 = pure xℱ.1}
this : IsClosed (Prod.map f id '' F)
x : X
snd : Ultrafilter X
hx : (x, snd) ∈ F
hy : Tendsto f (↑(id snd) : Filter X) (nhds (f x))
⊢ ∃ (x_1 : X), f x_1 = f x ∧ (↑(id snd) : Filter X) ≤ nhds x_1

Tactic:
⟨x, rfl, fun U hU ↦ Ultrafilter.compl_notMem_iff.mp fun hUc ↦ ?_⟩

Premises used: Ultrafilter.compl_notMem_iff, And.intro, Exists.intro, Iff.mp, rfl
-- Module: Mathlib.Topology.Maps.Proper.UniversallyClosed
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (X := X × Ultrafilter X) (Prod.map f id)
F : Set (X × Ultrafilter X) := closure {xℱ : X × Ultrafilter X | xℱ.2 = pure xℱ.1}
this : IsClosed (Prod.map f id '' F)
x : X
snd : Ultrafilter X
hx : (x, snd) ∈ F
hy : Tendsto f (↑(id snd) : Filter X) (nhds (f x))
mpr : ∀ (U : Set X) (hU : U ∈ nhds x) (hUc : Uᶜ ∈ id snd), False
⊢ ∃ (x_1 : X), f x_1 = f x ∧ (↑(id snd) : Filter X) ≤ nhds x_1

Tactic:
refine ⟨x, rfl, fun U hU ↦ Ultrafilter.compl_notMem_iff.mp fun hUc ↦ ?_⟩
-- Module: Mathlib.Topology.Maps.Proper.UniversallyClosed
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (X := X × Ultrafilter X) (Prod.map f id)
F : Set (X × Ultrafilter X) := closure {xℱ : X × Ultrafilter X | xℱ.2 = pure xℱ.1}
this : IsClosed (Prod.map f id '' F)
x : X
snd : Ultrafilter X
hx : (x, snd) ∈ F
hy : Tendsto f (↑(id snd) : Filter X) (nhds (f x))
U : Set X
hU : U ∈ nhds x
hUc : Uᶜ ∈ id snd
mpr :
  ∀ (hx : ∀ t ∈ nhds (x, snd), (t ∩ {xℱ : X × Ultrafilter X | xℱ.2 = pure xℱ.1}).Nonempty)
    (hy : Tendsto f (↑(id snd) : Filter X) (nhds (f x))) (U : Set X) (hU : U ∈ nhds x) (hUc : Uᶜ ∈ id snd), False
⊢ False

Tactic:
rw [mem_closure_iff_nhds] at hx

Premises used: mem_closure_iff_nhds
-- Module: Mathlib.Topology.Maps.Proper.UniversallyClosed
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (X := X × Ultrafilter X) (Prod.map f id)
F : Set (X × Ultrafilter X) := closure {xℱ : X × Ultrafilter X | xℱ.2 = pure xℱ.1}
this : IsClosed (Prod.map f id '' F)
x : X
snd : Ultrafilter X
hx : ∀ t ∈ nhds (x, snd), (t ∩ {xℱ : X × Ultrafilter X | xℱ.2 = pure xℱ.1}).Nonempty
hy : Tendsto f (↑(id snd) : Filter X) (nhds (f x))
U : Set X
hU : U ∈ nhds x
hUc : Uᶜ ∈ id snd
mpr : ∀ (y : X) (hy : y ∈ U) (hy' : Membership.mem (γ := Ultrafilter X) (pure y) Uᶜ), False
⊢ False

Tactic:
rcases hx (U ×ˢ {𝒢 | Uᶜ ∈ 𝒢}) (prod_mem_nhds hU ((ultrafilter_isOpen_basic _).mem_nhds hUc))
      with ⟨⟨y, 𝒢⟩, ⟨⟨hy : y ∈ U, hy' : Uᶜ ∈ 𝒢⟩, rfl : 𝒢 = pure y⟩⟩

Premises used: prod_mem_nhds, SProd.sprod, Compl.compl, setOf, Membership.mem, ultrafilter_isOpen_basic, IsOpen.mem_nhds, rfl
-- Module: Mathlib.Topology.Maps.Proper.UniversallyClosed
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (X := X × Ultrafilter X) (Prod.map f id)
F : Set (X × Ultrafilter X) := closure {xℱ : X × Ultrafilter X | xℱ.2 = pure xℱ.1}
this : IsClosed (Prod.map f id '' F)
x : X
snd : Ultrafilter X
hx : ∀ t ∈ nhds (x, snd), (t ∩ {xℱ : X × Ultrafilter X | xℱ.2 = pure xℱ.1}).Nonempty
hy_1 : Tendsto f (↑(id snd) : Filter X) (nhds (f x))
U : Set X
hU : U ∈ nhds x
hUc : Uᶜ ∈ id snd
y : X
hy : y ∈ U
hy' : Membership.mem (γ := Ultrafilter X) (pure y) Uᶜ
⊢ False

Tactic:
hy' hy
-- Module: Mathlib.Topology.Maps.Proper.UniversallyClosed
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (X := X × Ultrafilter X) (Prod.map f id)
F : Set (X × Ultrafilter X) := closure {xℱ : X × Ultrafilter X | xℱ.2 = pure xℱ.1}
this : IsClosed (Prod.map f id '' F)
x : X
snd : Ultrafilter X
hx : ∀ t ∈ nhds (x, snd), (t ∩ {xℱ : X × Ultrafilter X | xℱ.2 = pure xℱ.1}).Nonempty
hy_1 : Tendsto f (↑(id snd) : Filter X) (nhds (f x))
U : Set X
hU : U ∈ nhds x
hUc : Uᶜ ∈ id snd
y : X
hy : y ∈ U
hy' : Membership.mem (γ := Ultrafilter X) (pure y) Uᶜ
⊢ False

Tactic:
exact hy' hy
-- Module: Mathlib.Topology.Maps.Proper.UniversallyClosed
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
mp :
  IsProperMap f → Continuous f ∧ ∀ (Z : Type u) [inst_2 : TopologicalSpace Z], IsClosedMap (X := X × Z) (Prod.map f id)
mpr :
  (Continuous f ∧ ∀ (Z : Type u) [inst_2 : TopologicalSpace Z], IsClosedMap (X := X × Z) (Prod.map f id)) →
    IsProperMap f
⊢ IsProperMap f ↔ Continuous f ∧ ∀ (Z : Type u) [inst_2 : TopologicalSpace Z], IsClosedMap (X := X × Z) (Prod.map f id)

Tactic:
constructor
-- Module: Mathlib.Topology.Maps.Proper.UniversallyClosed
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
H : IsProperMap f
⊢ Continuous f ∧ ∀ (Z : Type u) [inst_2 : TopologicalSpace Z], IsClosedMap (X := X × Z) (Prod.map f id)

Tactic:
⟨H.continuous, fun Z ↦ H.universally_closed _⟩

Premises used: IsProperMap.universally_closed, And.intro, IsProperMap.continuous
-- Module: Mathlib.Topology.Maps.Proper.UniversallyClosed
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
H : IsProperMap f
⊢ Continuous f ∧ ∀ (Z : Type u) [inst_2 : TopologicalSpace Z], IsClosedMap (X := X × Z) (Prod.map f id)

Tactic:
exact ⟨H.continuous, fun Z ↦ H.universally_closed _⟩
-- Module: Mathlib.Topology.Maps.Proper.UniversallyClosed
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ ∀ (Z : Type u) [inst_2 : TopologicalSpace Z], IsClosedMap (X := X × Z) (Prod.map f id)
mpr : Continuous f ∧ IsClosedMap (X := X × Ultrafilter X) (Prod.map f id)
⊢ IsProperMap f

Tactic:
rw [isProperMap_iff_isClosedMap_ultrafilter]

Premises used: isProperMap_iff_isClosedMap_ultrafilter
-- Module: Mathlib.Topology.Maps.Proper.UniversallyClosed
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ ∀ (Z : Type u) [inst_2 : TopologicalSpace Z], IsClosedMap (X := X × Z) (Prod.map f id)
⊢ Continuous f ∧ IsClosedMap (X := X × Ultrafilter X) (Prod.map f id)

Tactic:
⟨H.1, H.2 _⟩

Premises used: And.right, And.left, And.intro
-- Module: Mathlib.Topology.Maps.Proper.UniversallyClosed
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ ∀ (Z : Type u) [inst_2 : TopologicalSpace Z], IsClosedMap (X := X × Z) (Prod.map f id)
⊢ Continuous f ∧ IsClosedMap (X := X × Ultrafilter X) (Prod.map f id)

Tactic:
exact ⟨H.1, H.2 _⟩
-- Module: Mathlib.Topology.Maps.Strict.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
⊢ IsStrictMap f ↔ IsQuotientMap (rangeFactorization f)

Tactic:
Iff.rfl

Premises used: Iff.rfl, Topology.IsStrictMap
-- Module: Mathlib.Topology.Maps.Strict.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
simp :
  IsQuotientMap (rangeFactorization f) ↔
    IsQuotientMap.{u_1, u_2} (X := Quotient (ker f)) (Y := (↑(range f) : Type u_2))
      (⇑(quotientKerEquivRange f) : (a : Quotient (ker f)) → (↑(range f) : Type u_2))
⊢ IsStrictMap f ↔
    IsHomeomorph.{u_1, u_2} (X := Quotient (ker f)) (Y := (↑(range f) : Type u_2))
      (⇑(quotientKerEquivRange f) : (a : Quotient (ker f)) → (↑(range f) : Type u_2))

Tactic:
simp only [IsStrictMap, isHomeomorph_iff_isQuotientMap_injective, Equiv.injective, and_true]

Premises used: isHomeomorph_iff_isQuotientMap_injective, and_true, Topology.IsStrictMap, Equiv.injective
-- Module: Mathlib.Topology.Maps.Strict.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
⊢ IsQuotientMap (rangeFactorization f) ↔
    IsQuotientMap.{u_1, u_2} (X := Quotient (ker f)) (Y := (↑(range f) : Type u_2))
      (⇑(quotientKerEquivRange f) : (a : Quotient (ker f)) → (↑(range f) : Type u_2))

Tactic:
⟨fun h => IsQuotientMap.of_comp_isQuotientMap isQuotientMap_quotient_mk' h,
         fun h ↦ h.comp isQuotientMap_quotient_mk'⟩

Premises used: isQuotientMap_quotient_mk', Topology.IsQuotientMap.comp, Iff.intro, Topology.IsQuotientMap.of_comp_isQuotientMap
-- Module: Mathlib.Topology.Maps.Strict.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
⊢ IsQuotientMap (rangeFactorization f) ↔
    IsQuotientMap.{u_1, u_2} (X := Quotient (ker f)) (Y := (↑(range f) : Type u_2))
      (⇑(quotientKerEquivRange f) : (a : Quotient (ker f)) → (↑(range f) : Type u_2))

Tactic:
exact ⟨fun h => IsQuotientMap.of_comp_isQuotientMap isQuotientMap_quotient_mk' h,
         fun h ↦ h.comp isQuotientMap_quotient_mk'⟩
-- Module: Mathlib.Topology.Maps.Strict.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
simp :
  IsEmbedding.{u_1, u_2} (X := Quotient (ker f)) (Y := (↑(range f) : Type u_2))
      (⇑(quotientKerEquivRange f) : (a : Quotient (ker f)) → (↑(range f) : Type u_2)) ↔
    IsEmbedding (kerLift f)
⊢ IsStrictMap f ↔ IsEmbedding (kerLift f)

Tactic:
simp only [isStrictMap_iff_isHomeomorph_quotientKerEquivRange,
    isHomeomorph_iff_isEmbedding_surjective, Equiv.surjective, and_true]

Premises used: Topology.isStrictMap_iff_isHomeomorph_quotientKerEquivRange, and_true, isHomeomorph_iff_isEmbedding_surjective, Equiv.surjective
-- Module: Mathlib.Topology.Maps.Strict.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
⊢ IsEmbedding.{u_1, u_2} (X := Quotient (ker f)) (Y := (↑(range f) : Type u_2))
      (⇑(quotientKerEquivRange f) : (a : Quotient (ker f)) → (↑(range f) : Type u_2)) ↔
    IsEmbedding (kerLift f)

Tactic:
(IsEmbedding.of_comp_iff .subtypeVal).symm

Premises used: Setoid.kerLift, Quotient, Topology.IsEmbedding.of_comp_iff, Topology.IsEmbedding.subtypeVal, Iff.symm
-- Module: Mathlib.Topology.Maps.Strict.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
⊢ IsEmbedding.{u_1, u_2} (X := Quotient (ker f)) (Y := (↑(range f) : Type u_2))
      (⇑(quotientKerEquivRange f) : (a : Quotient (ker f)) → (↑(range f) : Type u_2)) ↔
    IsEmbedding (kerLift f)

Tactic:
exact (IsEmbedding.of_comp_iff .subtypeVal).symm

Premises used: Topology.IsEmbedding.of_comp_iff, Topology.IsEmbedding.subtypeVal, Iff.symm
-- Module: Mathlib.Topology.Maps.Strict.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsStrictMap f
⊢ IsQuotientMap (rangeFactorization f)

Tactic:
rw [isStrictMap_iff_isQuotientMap_rangeFactorization] at hf

Premises used: Topology.isStrictMap_iff_isQuotientMap_rangeFactorization
-- Module: Mathlib.Topology.Maps.Strict.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsQuotientMap (rangeFactorization f)
⊢ Continuous[inst, inst_1] f

Tactic:
continuous_rangeFactorization_iff.mp hf.continuous

Premises used: continuous_rangeFactorization_iff, Topology.IsQuotientMap.continuous, Iff.mp
-- Module: Mathlib.Topology.Maps.Strict.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsQuotientMap (rangeFactorization f)
⊢ Continuous[inst, inst_1] f

Tactic:
exact continuous_rangeFactorization_iff.mp hf.continuous

Premises used: continuous_rangeFactorization_iff, Topology.IsQuotientMap.continuous, Iff.mp
-- Module: Mathlib.Topology.Maps.Strict.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
ho : IsOpenMap f
h_cont : Continuous[inst, inst_1] f
⊢ IsQuotientMap (rangeFactorization f)

Tactic:
(ho.subtype_mk fun x => ⟨x, rfl⟩).isQuotientMap
    h_cont.rangeFactorization Set.rangeFactorization_surjective

Premises used: IsOpenMap.isQuotientMap, Continuous.rangeFactorization, IsOpenMap.subtype_mk, Set.rangeFactorization_surjective, Set.rangeFactorization
-- Module: Mathlib.Topology.Maps.Strict.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
ho : IsOpenMap f
h_cont : Continuous[inst, inst_1] f
⊢ IsQuotientMap (rangeFactorization f)

Tactic:
exact (ho.subtype_mk fun x => ⟨x, rfl⟩).isQuotientMap
    h_cont.rangeFactorization Set.rangeFactorization_surjective

Premises used: IsOpenMap.isQuotientMap, Continuous.rangeFactorization, IsOpenMap.subtype_mk, Set.rangeFactorization_surjective
-- Module: Mathlib.Topology.Maps.Strict.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hc : IsClosedMap f
h_cont : Continuous[inst, inst_1] f
⊢ IsQuotientMap (rangeFactorization f)

Tactic:
(hc.subtype_mk fun x => ⟨x, rfl⟩).isQuotientMap
    h_cont.rangeFactorization Set.rangeFactorization_surjective

Premises used: IsClosedMap.subtype_mk, Continuous.rangeFactorization, Set.rangeFactorization_surjective, IsClosedMap.isQuotientMap, Set.rangeFactorization
-- Module: Mathlib.Topology.Maps.Strict.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hc : IsClosedMap f
h_cont : Continuous[inst, inst_1] f
⊢ IsQuotientMap (rangeFactorization f)

Tactic:
exact (hc.subtype_mk fun x => ⟨x, rfl⟩).isQuotientMap
    h_cont.rangeFactorization Set.rangeFactorization_surjective

Premises used: IsClosedMap.subtype_mk, Continuous.rangeFactorization, Set.rangeFactorization_surjective, IsClosedMap.isQuotientMap
-- Module: Mathlib.Topology.Maps.Strict.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
f_homeo : IsHomeomorph f
⊢ IsStrictMap f

Tactic:
f_homeo.isOpenMap.isStrictMap f_homeo.continuous

Premises used: IsHomeomorph.isOpenMap, IsHomeomorph.continuous, Topology.IsOpenMap.isStrictMap
-- Module: Mathlib.Topology.Maps.Strict.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ IsStrictMap.{u_1, u_1} (X := X) _root_.id

Tactic:
IsHomeomorph.id.isStrictMap

Premises used: IsHomeomorph.id, Topology.IsHomeomorph.isStrictMap
-- Module: Mathlib.Topology.Maps.Strict.Basic
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : X → Y
g : Y → Z
f_quot : IsQuotientMap f
Φ : (↑(range (g ∘ f)) : Type u_3) ≃ₜ (↑(range g) : Type u_3) :=
  Homeomorph.setCongr (s := range (g ∘ f)) (t := range g) ⋯
⊢ rangeFactorization g ∘ f =
    (⇑Φ : (a : (↑(range (g ∘ f)) : Type u_3)) → (↑(range g) : Type u_3)) ∘ rangeFactorization (g ∘ f)

Tactic:
have key : rangeFactorization g ∘ f = Φ ∘ rangeFactorization (g ∘ f) := rfl
-- Module: Mathlib.Topology.Maps.Strict.Basic
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : X → Y
g : Y → Z
f_quot : IsQuotientMap f
Φ : (↑(range (g ∘ f)) : Type u_3) ≃ₜ (↑(range g) : Type u_3) :=
  Homeomorph.setCongr (s := range (g ∘ f)) (t := range g) ⋯
key :
  rangeFactorization g ∘ f =
    (⇑Φ : (a : (↑(range (g ∘ f)) : Type u_3)) → (↑(range g) : Type u_3)) ∘ rangeFactorization (g ∘ f)
simp_rw :
  IsQuotientMap (Y := (↑(range g) : Type u_3))
      ((⇑Φ : (a : (↑(range (g ∘ f)) : Type u_3)) → (↑(range g) : Type u_3)) ∘ rangeFactorization (g ∘ f)) ↔
    IsQuotientMap (rangeFactorization (g ∘ f))
⊢ IsStrictMap g ↔ IsStrictMap (g ∘ f)

Tactic:
simp_rw [isStrictMap_iff_isQuotientMap_rangeFactorization, ← f_quot.of_comp_iff, key]

Premises used: Topology.IsQuotientMap.of_comp_iff, Topology.isStrictMap_iff_isQuotientMap_rangeFactorization
-- Module: Mathlib.Topology.Maps.Strict.Basic
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : X → Y
g : Y → Z
f_quot : IsQuotientMap f
Φ : (↑(range (g ∘ f)) : Type u_3) ≃ₜ (↑(range g) : Type u_3) :=
  Homeomorph.setCongr (s := range (g ∘ f)) (t := range g) ⋯
key :
  rangeFactorization g ∘ f =
    (⇑Φ : (a : (↑(range (g ∘ f)) : Type u_3)) → (↑(range g) : Type u_3)) ∘ rangeFactorization (g ∘ f)
H :
  IsQuotientMap (Y := (↑(range g) : Type u_3))
    ((⇑Φ : (a : (↑(range (g ∘ f)) : Type u_3)) → (↑(range g) : Type u_3)) ∘ rangeFactorization (g ∘ f))
⊢ IsQuotientMap (rangeFactorization (g ∘ f))

Tactic:
simpa using Φ.symm.isQuotientMap.comp H

Premises used: Topology.IsQuotientMap.comp, Homeomorph.symm, Homeomorph.isQuotientMap
-- Module: Mathlib.Topology.Maps.Strict.Basic
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : X → Y
g : Y → Z
f_quot : IsQuotientMap f
Φ : (↑(range (g ∘ f)) : Type u_3) ≃ₜ (↑(range g) : Type u_3) :=
  Homeomorph.setCongr (s := range (g ∘ f)) (t := range g) ⋯
key :
  rangeFactorization g ∘ f =
    (⇑Φ : (a : (↑(range (g ∘ f)) : Type u_3)) → (↑(range g) : Type u_3)) ∘ rangeFactorization (g ∘ f)
⊢ IsQuotientMap (Y := (↑(range g) : Type u_3))
      ((⇑Φ : (a : (↑(range (g ∘ f)) : Type u_3)) → (↑(range g) : Type u_3)) ∘ rangeFactorization (g ∘ f)) ↔
    IsQuotientMap (rangeFactorization (g ∘ f))

Tactic:
exact ⟨fun H ↦ by simpa using Φ.symm.isQuotientMap.comp H, fun H ↦ Φ.isQuotientMap.comp H⟩
-- Module: Mathlib.Topology.Maps.Strict.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
f_quot : IsQuotientMap f
⊢ IsStrictMap f

Tactic:
f_quot.isStrictMap_iff.mp .id

Premises used: Topology.IsStrictMap.id, Topology.IsQuotientMap.isStrictMap_iff, Iff.mp