awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Maps.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
hf : IsOpenEmbedding f
s : Set Y
hs : s ⊆ range f
⊢ IsOpen[inst_1] s ↔ IsOpen[inst] (f ⁻¹' s)
have rw : IsOpen[inst_1] s ↔ IsOpen[inst_1] (f '' f ⁻¹' s)
Tactic: rw [hf.isOpen_iff_image_isOpen, image_preimage_eq_inter_range, inter_eq_self_of_subset_left hs]
-- Lean 4 proof step from Mathlib.Topology.Maps.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
hf : IsOpenEmbedding f
s : Set Y
hs : s ⊆ range f
rw : IsOpen[inst_1] s ↔ IsOpen[inst_1] (f '' f ⁻¹' s)
⊢ IsOpen[inst_1] s ↔ IsOpen[inst] (f ⁻¹' s)
have rw₁ : IsOpen[inst_1] s ↔ IsOpen[inst_1] (s ∩ range f)
Tactic: rw [hf.isOpen_iff_image_isOpen, image_preimage_eq_inter_range, inter_eq_self_of_subset_left hs]
-- Lean 4 proof step from Mathlib.Topology.Maps.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
hf : IsOpenEmbedding f
s : Set Y
hs : s ⊆ range f
rw : IsOpen[inst_1] s ↔ IsOpen[inst_1] (f '' f ⁻¹' s)
rw₁ : IsOpen[inst_1] s ↔ IsOpen[inst_1] (s ∩ range f)
⊢ IsOpen[inst_1] s ↔ IsOpen[inst] (f ⁻¹' s)
have rw₂ : IsOpen[inst_1] s ↔ IsOpen[inst_1] s
Tactic: rw [hf.isOpen_iff_image_isOpen, image_preimage_eq_inter_range, inter_eq_self_of_subset_left hs]
-- Lean 4 proof step from Mathlib.Topology.Maps.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h₁ : Continuous[inst, inst_1] f
h₂ : Injective f
h₃ : IsOpenMap f
⊢ IsOpenEmbedding f
have simp : ∀ (x : X), 𝓝 x = comap f (𝓝 (f x))
Tactic: simp only [isOpenEmbedding_iff_isEmbedding_isOpenMap, isEmbedding_iff, isInducing_iff_nhds, *,
    and_true]
-- Lean 4 proof step from Mathlib.Topology.Maps.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
hg : IsOpenEmbedding g
⊢ IsOpenMap f ↔ IsOpenMap (g ∘ f)
have simp_rw : (∀ (x : X), 𝓝 (f x) ≤ map f (𝓝 x)) ↔ ∀ (x : X), 𝓝 ((g ∘ f) x) ≤ map (g ∘ f) (𝓝 x)
Tactic: simp_rw [isOpenMap_iff_nhds_le, ← map_map, comp, ← hg.map_nhds_eq, map_le_map_iff hg.injective]
-- Lean 4 proof step from Mathlib.Topology.Maps.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
hg : IsOpenEmbedding g
simp_rw : (∀ (x : X), 𝓝 (f x) ≤ map f (𝓝 x)) ↔ ∀ (x : X), 𝓝 ((g ∘ f) x) ≤ map (g ∘ f) (𝓝 x)
⊢ IsOpenMap f ↔ IsOpenMap (g ∘ f)
have simp_rw₁ : (∀ (x : X), 𝓝 (f x) ≤ map f (𝓝 x)) ↔ ∀ (x : X), 𝓝 ((g ∘ f) x) ≤ map g (map f (𝓝 x))
Tactic: simp_rw [isOpenMap_iff_nhds_le, ← map_map, comp, ← hg.map_nhds_eq, map_le_map_iff hg.injective]
-- Lean 4 proof step from Mathlib.Topology.Maps.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
hg : IsOpenEmbedding g
simp_rw : (∀ (x : X), 𝓝 (f x) ≤ map f (𝓝 x)) ↔ ∀ (x : X), 𝓝 ((g ∘ f) x) ≤ map (g ∘ f) (𝓝 x)
simp_rw₁ : (∀ (x : X), 𝓝 (f x) ≤ map f (𝓝 x)) ↔ ∀ (x : X), 𝓝 ((g ∘ f) x) ≤ map g (map f (𝓝 x))
⊢ IsOpenMap f ↔ IsOpenMap (g ∘ f)
have simp_rw₂ : (∀ (x : X), 𝓝 (f x) ≤ map f (𝓝 x)) ↔ ∀ (x : X), 𝓝 (g (f x)) ≤ map g (map f (𝓝 x))
Tactic: simp_rw [isOpenMap_iff_nhds_le, ← map_map, comp, ← hg.map_nhds_eq, map_le_map_iff hg.injective]
-- Lean 4 proof step from Mathlib.Topology.Maps.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
hg : IsOpenEmbedding g
simp_rw : (∀ (x : X), 𝓝 (f x) ≤ map f (𝓝 x)) ↔ ∀ (x : X), 𝓝 ((g ∘ f) x) ≤ map (g ∘ f) (𝓝 x)
simp_rw₁ : (∀ (x : X), 𝓝 (f x) ≤ map f (𝓝 x)) ↔ ∀ (x : X), 𝓝 ((g ∘ f) x) ≤ map g (map f (𝓝 x))
simp_rw₂ : (∀ (x : X), 𝓝 (f x) ≤ map f (𝓝 x)) ↔ ∀ (x : X), 𝓝 (g (f x)) ≤ map g (map f (𝓝 x))
⊢ IsOpenMap f ↔ IsOpenMap (g ∘ f)
have simp_rw₃ : (∀ (x : X), 𝓝 (f x) ≤ map f (𝓝 x)) ↔ ∀ (x : X), map g (𝓝 (f x)) ≤ map g (map f (𝓝 x))
Tactic: simp_rw [isOpenMap_iff_nhds_le, ← map_map, comp, ← hg.map_nhds_eq, map_le_map_iff hg.injective]
-- Lean 4 proof step from Mathlib.Topology.Maps.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsOpenEmbedding f
s : Set X
x : X
⊢ f '' s ∈ 𝓝 (f x) ↔ s ∈ 𝓝 x
have rw : f '' s ∈ map f (𝓝 x) ↔ s ∈ 𝓝 x
Tactic: rw [← hf.map_nhds_eq, mem_map, preimage_image_eq _ hf.injective]
-- Lean 4 proof step from Mathlib.Topology.Maps.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsOpenEmbedding f
s : Set X
x : X
rw : f '' s ∈ map f (𝓝 x) ↔ s ∈ 𝓝 x
⊢ f '' s ∈ 𝓝 (f x) ↔ s ∈ 𝓝 x
have rw₁ : f ⁻¹' f '' s ∈ 𝓝 x ↔ s ∈ 𝓝 x
Tactic: rw [← hf.map_nhds_eq, mem_map, preimage_image_eq _ hf.injective]
-- Lean 4 proof step from Mathlib.Topology.Maps.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsOpenEmbedding f
s : Set X
x : X
rw : f '' s ∈ map f (𝓝 x) ↔ s ∈ 𝓝 x
rw₁ : f ⁻¹' f '' s ∈ 𝓝 x ↔ s ∈ 𝓝 x
⊢ f '' s ∈ 𝓝 (f x) ↔ s ∈ 𝓝 x
have rw₂ : s ∈ 𝓝 x ↔ s ∈ 𝓝 x
Tactic: rw [← hf.map_nhds_eq, mem_map, preimage_image_eq _ hf.injective]
-- Lean 4 proof step from Mathlib.Topology.Maps.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
hf : IsOpenEmbedding f
x : X
l : Filter Y
⊢ AccPt x (comap f l) ↔ AccPt (f x) l
have rw : ClusterPt x (𝓟 {x}ᶜ ⊓ comap f l) ↔ AccPt (f x) l
Tactic: rw [accPt_iff_clusterPt, accPt_iff_clusterPt, ← hf.injective.preimage_image {x}, image_singleton,
    ← preimage_compl, ← comap_principal, ← comap_inf,
    hf.isOpenMap.clusterPt_comap_iff hf.continuous]
-- Lean 4 proof step from Mathlib.Topology.Maps.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
hf : IsOpenEmbedding f
x : X
l : Filter Y
rw : ClusterPt x (𝓟 {x}ᶜ ⊓ comap f l) ↔ AccPt (f x) l
⊢ AccPt x (comap f l) ↔ AccPt (f x) l
have rw₁ : ClusterPt x (𝓟 {x}ᶜ ⊓ comap f l) ↔ ClusterPt (f x) (𝓟 {f x}ᶜ ⊓ l)
Tactic: rw [accPt_iff_clusterPt, accPt_iff_clusterPt, ← hf.injective.preimage_image {x}, image_singleton,
    ← preimage_compl, ← comap_principal, ← comap_inf,
    hf.isOpenMap.clusterPt_comap_iff hf.continuous]
-- Lean 4 proof step from Mathlib.Topology.Maps.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
hf : IsOpenEmbedding f
x : X
l : Filter Y
rw : ClusterPt x (𝓟 {x}ᶜ ⊓ comap f l) ↔ AccPt (f x) l
rw₁ : ClusterPt x (𝓟 {x}ᶜ ⊓ comap f l) ↔ ClusterPt (f x) (𝓟 {f x}ᶜ ⊓ l)
⊢ AccPt x (comap f l) ↔ AccPt (f x) l
have rw₂ : ClusterPt x (𝓟 (f ⁻¹' f '' {x})ᶜ ⊓ comap f l) ↔ ClusterPt (f x) (𝓟 {f x}ᶜ ⊓ l)
Tactic: rw [accPt_iff_clusterPt, accPt_iff_clusterPt, ← hf.injective.preimage_image {x}, image_singleton,
    ← preimage_compl, ← comap_principal, ← comap_inf,
    hf.isOpenMap.clusterPt_comap_iff hf.continuous]
-- Lean 4 proof step from Mathlib.Topology.Maps.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
hf : IsOpenEmbedding f
x : X
l : Filter Y
rw : ClusterPt x (𝓟 {x}ᶜ ⊓ comap f l) ↔ AccPt (f x) l
rw₁ : ClusterPt x (𝓟 {x}ᶜ ⊓ comap f l) ↔ ClusterPt (f x) (𝓟 {f x}ᶜ ⊓ l)
rw₂ : ClusterPt x (𝓟 (f ⁻¹' f '' {x})ᶜ ⊓ comap f l) ↔ ClusterPt (f x) (𝓟 {f x}ᶜ ⊓ l)
⊢ AccPt x (comap f l) ↔ AccPt (f x) l
have rw₃ : ClusterPt x (𝓟 (f ⁻¹' {f x})ᶜ ⊓ comap f l) ↔ ClusterPt (f x) (𝓟 {f x}ᶜ ⊓ l)
Tactic: rw [accPt_iff_clusterPt, accPt_iff_clusterPt, ← hf.injective.preimage_image {x}, image_singleton,
    ← preimage_compl, ← comap_principal, ← comap_inf,
    hf.isOpenMap.clusterPt_comap_iff hf.continuous]
-- Lean 4 proof step from Mathlib.Topology.Maps.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
hf : IsOpenEmbedding f
x : X
l : Filter Y
rw : ClusterPt x (𝓟 {x}ᶜ ⊓ comap f l) ↔ AccPt (f x) l
rw₁ : ClusterPt x (𝓟 {x}ᶜ ⊓ comap f l) ↔ ClusterPt (f x) (𝓟 {f x}ᶜ ⊓ l)
rw₂ : ClusterPt x (𝓟 (f ⁻¹' f '' {x})ᶜ ⊓ comap f l) ↔ ClusterPt (f x) (𝓟 {f x}ᶜ ⊓ l)
rw₃ : ClusterPt x (𝓟 (f ⁻¹' {f x})ᶜ ⊓ comap f l) ↔ ClusterPt (f x) (𝓟 {f x}ᶜ ⊓ l)
⊢ AccPt x (comap f l) ↔ AccPt (f x) l
have rw₄ : ClusterPt x (𝓟 (f ⁻¹' {f x}ᶜ) ⊓ comap f l) ↔ ClusterPt (f x) (𝓟 {f x}ᶜ ⊓ l)
Tactic: rw [accPt_iff_clusterPt, accPt_iff_clusterPt, ← hf.injective.preimage_image {x}, image_singleton,
    ← preimage_compl, ← comap_principal, ← comap_inf,
    hf.isOpenMap.clusterPt_comap_iff hf.continuous]
-- Lean 4 proof step from Mathlib.Topology.Maps.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
hf : IsOpenEmbedding f
x : X
l : Filter Y
rw : ClusterPt x (𝓟 {x}ᶜ ⊓ comap f l) ↔ AccPt (f x) l
rw₁ : ClusterPt x (𝓟 {x}ᶜ ⊓ comap f l) ↔ ClusterPt (f x) (𝓟 {f x}ᶜ ⊓ l)
rw₂ : ClusterPt x (𝓟 (f ⁻¹' f '' {x})ᶜ ⊓ comap f l) ↔ ClusterPt (f x) (𝓟 {f x}ᶜ ⊓ l)
rw₃ : ClusterPt x (𝓟 (f ⁻¹' {f x})ᶜ ⊓ comap f l) ↔ ClusterPt (f x) (𝓟 {f x}ᶜ ⊓ l)
rw₄ : ClusterPt x (𝓟 (f ⁻¹' {f x}ᶜ) ⊓ comap f l) ↔ ClusterPt (f x) (𝓟 {f x}ᶜ ⊓ l)
⊢ AccPt x (comap f l) ↔ AccPt (f x) l
have rw₅ : ClusterPt x (comap f (𝓟 {f x}ᶜ) ⊓ comap f l) ↔ ClusterPt (f x) (𝓟 {f x}ᶜ ⊓ l)
Tactic: rw [accPt_iff_clusterPt, accPt_iff_clusterPt, ← hf.injective.preimage_image {x}, image_singleton,
    ← preimage_compl, ← comap_principal, ← comap_inf,
    hf.isOpenMap.clusterPt_comap_iff hf.continuous]
-- Lean 4 proof step from Mathlib.Topology.Maps.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
hf : IsOpenEmbedding f
x : X
l : Filter Y
rw : ClusterPt x (𝓟 {x}ᶜ ⊓ comap f l) ↔ AccPt (f x) l
rw₁ : ClusterPt x (𝓟 {x}ᶜ ⊓ comap f l) ↔ ClusterPt (f x) (𝓟 {f x}ᶜ ⊓ l)
rw₂ : ClusterPt x (𝓟 (f ⁻¹' f '' {x})ᶜ ⊓ comap f l) ↔ ClusterPt (f x) (𝓟 {f x}ᶜ ⊓ l)
rw₃ : ClusterPt x (𝓟 (f ⁻¹' {f x})ᶜ ⊓ comap f l) ↔ ClusterPt (f x) (𝓟 {f x}ᶜ ⊓ l)
rw₄ : ClusterPt x (𝓟 (f ⁻¹' {f x}ᶜ) ⊓ comap f l) ↔ ClusterPt (f x) (𝓟 {f x}ᶜ ⊓ l)
rw₅ : ClusterPt x (comap f (𝓟 {f x}ᶜ) ⊓ comap f l) ↔ ClusterPt (f x) (𝓟 {f x}ᶜ ⊓ l)
⊢ AccPt x (comap f l) ↔ AccPt (f x) l
have rw₆ : ClusterPt x (comap f (𝓟 {f x}ᶜ ⊓ l)) ↔ ClusterPt (f x) (𝓟 {f x}ᶜ ⊓ l)
Tactic: rw [accPt_iff_clusterPt, accPt_iff_clusterPt, ← hf.injective.preimage_image {x}, image_singleton,
    ← preimage_compl, ← comap_principal, ← comap_inf,
    hf.isOpenMap.clusterPt_comap_iff hf.continuous]
-- Lean 4 proof step from Mathlib.Topology.Maps.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
hf : IsOpenEmbedding f
x : X
l : Filter Y
rw : ClusterPt x (𝓟 {x}ᶜ ⊓ comap f l) ↔ AccPt (f x) l
rw₁ : ClusterPt x (𝓟 {x}ᶜ ⊓ comap f l) ↔ ClusterPt (f x) (𝓟 {f x}ᶜ ⊓ l)
rw₂ : ClusterPt x (𝓟 (f ⁻¹' f '' {x})ᶜ ⊓ comap f l) ↔ ClusterPt (f x) (𝓟 {f x}ᶜ ⊓ l)
rw₃ : ClusterPt x (𝓟 (f ⁻¹' {f x})ᶜ ⊓ comap f l) ↔ ClusterPt (f x) (𝓟 {f x}ᶜ ⊓ l)
rw₄ : ClusterPt x (𝓟 (f ⁻¹' {f x}ᶜ) ⊓ comap f l) ↔ ClusterPt (f x) (𝓟 {f x}ᶜ ⊓ l)
rw₅ : ClusterPt x (comap f (𝓟 {f x}ᶜ) ⊓ comap f l) ↔ ClusterPt (f x) (𝓟 {f x}ᶜ ⊓ l)
rw₆ : ClusterPt x (comap f (𝓟 {f x}ᶜ ⊓ l)) ↔ ClusterPt (f x) (𝓟 {f x}ᶜ ⊓ l)
⊢ AccPt x (comap f l) ↔ AccPt (f x) l
have rw₇ : ClusterPt (f x) (𝓟 {f x}ᶜ ⊓ l) ↔ ClusterPt (f x) (𝓟 {f x}ᶜ ⊓ l)
Tactic: rw [accPt_iff_clusterPt, accPt_iff_clusterPt, ← hf.injective.preimage_image {x}, image_singleton,
    ← preimage_compl, ← comap_principal, ← comap_inf,
    hf.isOpenMap.clusterPt_comap_iff hf.continuous]
-- Lean 4 proof step from Mathlib.Topology.Maps.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
hf : IsClosedEmbedding f
s : Set X
h : IsClosed[inst_1] (f '' s)
⊢ IsClosed[inst] s
have rw : IsClosed[inst] (f ⁻¹' f '' s)
Tactic: rw [← preimage_image_eq s hf.injective]
-- Lean 4 proof step from Mathlib.Topology.Maps.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
hf : IsClosedEmbedding f
s : Set Y
hs : s ⊆ range f
⊢ IsClosed[inst_1] s ↔ IsClosed[inst] (f ⁻¹' s)
have rw : IsClosed[inst_1] s ↔ IsClosed[inst_1] (f '' f ⁻¹' s)
Tactic: rw [hf.isClosed_iff_image_isClosed, image_preimage_eq_of_subset hs]
-- Lean 4 proof step from Mathlib.Topology.Maps.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
hf : IsClosedEmbedding f
s : Set Y
hs : s ⊆ range f
rw : IsClosed[inst_1] s ↔ IsClosed[inst_1] (f '' f ⁻¹' s)
⊢ IsClosed[inst_1] s ↔ IsClosed[inst] (f ⁻¹' s)
have rw₁ : IsClosed[inst_1] s ↔ IsClosed[inst_1] s
Tactic: rw [hf.isClosed_iff_image_isClosed, image_preimage_eq_of_subset hs]
-- Lean 4 proof step from Mathlib.Topology.Maps.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h₁ : Continuous[inst, inst_1] f
h₂ : Injective f
h₃ : IsClosedMap f
⊢ IsClosedEmbedding f
have refine : inst = induced f inst_1
Tactic: refine .of_isEmbedding_isClosedMap ⟨⟨?_⟩, h₂⟩ h₃
-- Lean 4 proof step from Mathlib.Topology.Maps.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h₁ : Continuous[inst, inst_1] f
h₂ : Injective f
h₃ : IsClosedMap f
⊢ inst = induced f inst_1
have refine : ∀ (s : Set X) (hs : IsOpen[inst] s), IsOpen[induced f inst_1] s
Tactic: refine h₁.le_induced.antisymm fun s hs => ?_
-- Lean 4 proof step from Mathlib.Topology.Maps.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h₁ : Continuous[inst, inst_1] f
h₂ : Injective f
h₃ : IsClosedMap f
s : Set X
hs : IsOpen[inst] s
⊢ IsOpen[induced f inst_1] s
have refine : f ⁻¹' (f '' sᶜ)ᶜ = s
Tactic: refine ⟨(f '' sᶜ)ᶜ, (h₃ _ hs.isClosed_compl).isOpen_compl, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Maps.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h₁ : Continuous[inst, inst_1] f
h₂ : Injective f
h₃ : IsClosedMap f
s : Set X
hs : IsOpen[inst] s
⊢ f ⁻¹' (f '' sᶜ)ᶜ = s
have rw : (f ⁻¹' f '' sᶜ)ᶜ = s
Tactic: rw [preimage_compl, preimage_image_eq _ h₂, compl_compl]
-- Lean 4 proof step from Mathlib.Topology.Maps.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h₁ : Continuous[inst, inst_1] f
h₂ : Injective f
h₃ : IsClosedMap f
s : Set X
hs : IsOpen[inst] s
rw : (f ⁻¹' f '' sᶜ)ᶜ = s
⊢ f ⁻¹' (f '' sᶜ)ᶜ = s
have rw₁ : sᶜᶜ = s
Tactic: rw [preimage_compl, preimage_image_eq _ h₂, compl_compl]
-- Lean 4 proof step from Mathlib.Topology.Maps.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h₁ : Continuous[inst, inst_1] f
h₂ : Injective f
h₃ : IsClosedMap f
s : Set X
hs : IsOpen[inst] s
rw : (f ⁻¹' f '' sᶜ)ᶜ = s
rw₁ : sᶜᶜ = s
⊢ f ⁻¹' (f '' sᶜ)ᶜ = s
have rw₂ : s = s
Tactic: rw [preimage_compl, preimage_image_eq _ h₂, compl_compl]
-- Lean 4 proof step from Mathlib.Topology.Maps.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
hg : IsClosedEmbedding g
⊢ IsClosedEmbedding (g ∘ f) ↔ IsClosedEmbedding f
have simp_rw : IsEmbedding (g ∘ f) ∧ IsClosed[inst_2] (range (g ∘ f)) ↔ IsEmbedding f ∧ IsClosed[inst_1] (range f)
Tactic: simp_rw [isClosedEmbedding_iff, hg.isEmbedding.of_comp_iff, Set.range_comp,
    ← hg.isClosed_iff_image_isClosed]
-- Lean 4 proof step from Mathlib.Topology.Maps.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
hg : IsClosedEmbedding g
simp_rw : IsEmbedding (g ∘ f) ∧ IsClosed[inst_2] (range (g ∘ f)) ↔ IsEmbedding f ∧ IsClosed[inst_1] (range f)
⊢ IsClosedEmbedding (g ∘ f) ↔ IsClosedEmbedding f
have simp_rw₁ : IsEmbedding f ∧ IsClosed[inst_2] (range (g ∘ f)) ↔ IsEmbedding f ∧ IsClosed[inst_1] (range f)
Tactic: simp_rw [isClosedEmbedding_iff, hg.isEmbedding.of_comp_iff, Set.range_comp,
    ← hg.isClosed_iff_image_isClosed]
-- Lean 4 proof step from Mathlib.Topology.Maps.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
hg : IsClosedEmbedding g
simp_rw : IsEmbedding (g ∘ f) ∧ IsClosed[inst_2] (range (g ∘ f)) ↔ IsEmbedding f ∧ IsClosed[inst_1] (range f)
simp_rw₁ : IsEmbedding f ∧ IsClosed[inst_2] (range (g ∘ f)) ↔ IsEmbedding f ∧ IsClosed[inst_1] (range f)
⊢ IsClosedEmbedding (g ∘ f) ↔ IsClosedEmbedding f
have simp_rw₂ : IsEmbedding f ∧ IsClosed[inst_2] (g '' range f) ↔ IsEmbedding f ∧ IsClosed[inst_1] (range f)
Tactic: simp_rw [isClosedEmbedding_iff, hg.isEmbedding.of_comp_iff, Set.range_comp,
    ← hg.isClosed_iff_image_isClosed]
-- Lean 4 proof step from Mathlib.Topology.Maps.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
hg : IsEmbedding g
hgf : IsClosedEmbedding (g ∘ f)
⊢ IsClosed[inst_1] (range f)
have h : range f = g ⁻¹' range (g ∘ f)
Tactic: convert! hg.isClosed_preimage _ hgf.isClosed_range
-- Lean 4 proof step from Mathlib.Topology.Maps.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
hg : IsEmbedding g
hgf : IsClosedEmbedding (g ∘ f)
⊢ range f = g ⁻¹' range (g ∘ f)
have h : range f = g ⁻¹' g '' range f
Tactic: rw [range_comp, hg.injective.preimage_image]
-- Lean 4 proof step from Mathlib.Topology.Maps.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
hg : IsEmbedding g
hgf : IsClosedEmbedding (g ∘ f)
h : range f = g ⁻¹' g '' range f
⊢ range f = g ⁻¹' range (g ∘ f)
have h₁ : range f = range f
Tactic: rw [range_comp, hg.injective.preimage_image]
-- Lean 4 proof step from Mathlib.Topology.Maps.OpenQuotient (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
inst_2 : BaireSpace X
hf : IsOpenQuotientMap f
⊢ BaireSpace Y
have baire_property : ∀ (f : ℕ → Set Y), (∀ (n : ℕ), IsOpen[inst_1] (f n)) → (∀ (n : ℕ), Dense (f n)) → Dense.{u_2} (X := Y) (⋂ (n : ℕ), f n)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Maps.OpenQuotient (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
inst_2 : BaireSpace X
hf : IsOpenQuotientMap f
u : ℕ → Set Y
hou : ∀ (n : ℕ), IsOpen[inst_1] (u n)
hdu : ∀ (n : ℕ), Dense (u n)
⊢ Dense.{u_2} (X := Y) (⋂ (n : ℕ), u n)
have this : Dense.{u_1} (X := X) (⋂ (n : ℕ), f ⁻¹' u n)
Tactic: have := dense_iInter_of_isOpen_nat (fun n => hf.continuous.isOpen_preimage (u n) (hou n))
    (fun n => (IsOpenQuotientMap.dense_preimage_iff hf).mpr (hdu n))
-- Lean 4 proof step from Mathlib.Topology.Maps.OpenQuotient (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
ind : IsInducing f
surj : Surjective f
U : Set X
U_open : IsOpen[inst] U
⊢ IsOpen[inst_1] (f '' U)
have obtain : ∀ (V : Set Y) (hV : IsOpen[inst_1] V) (U_open : IsOpen[inst] (f ⁻¹' V)), IsOpen[inst_1] (f '' f ⁻¹' V)
Tactic: obtain ⟨V, hV, rfl⟩ := ind.isOpen_iff.mp U_open
Cleared hypotheses: U, U_open
-- Lean 4 proof step from Mathlib.Topology.Maps.OpenQuotient (goal)
Goal:
A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst : TopologicalSpace A
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace D
f : A → B
g : C → D
p : A → C
q : B → D
h : g ∘ p = q ∘ f
hf : IsInducing f
hp : Surjective p
hq : IsOpenQuotientMap q
hg : Injective g
H : q ⁻¹' q '' range f ⊆ range f
⊢ TopologicalSpace.coinduced p inst = TopologicalSpace.induced g inst_2
have a : ∀ (U : Set C), IsOpen[TopologicalSpace.coinduced p inst] U ↔ IsOpen[TopologicalSpace.induced g inst_2] U
Tactic: ext U
-- Lean 4 proof step from Mathlib.Topology.Maps.OpenQuotient (goal)
Goal:
A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst : TopologicalSpace A
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace D
f : A → B
g : C → D
p : A → C
q : B → D
h : g ∘ p = q ∘ f
hf : IsInducing f
hp : Surjective p
hq : IsOpenQuotientMap q
hg : Injective g
H : q ⁻¹' q '' range f ⊆ range f
U : Set C
⊢ IsOpen[TopologicalSpace.coinduced p inst] U ↔ IsOpen[TopologicalSpace.induced g inst_2] U
have a : IsOpen[inst] (p ⁻¹' U) ↔ ∃ (V : Set D), IsOpen[inst_2] V ∧ g ⁻¹' V = U
Tactic: change IsOpen (p ⁻¹' U) ↔ ∃ V, _
-- Lean 4 proof step from Mathlib.Topology.Maps.OpenQuotient (goal)
Goal:
A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst : TopologicalSpace A
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace D
f : A → B
g : C → D
p : A → C
q : B → D
h : g ∘ p = q ∘ f
hf : IsInducing f
hp : Surjective p
hq : IsOpenQuotientMap q
hg : Injective g
H : q ⁻¹' q '' range f ⊆ range f
U : Set C
⊢ IsOpen[inst] (p ⁻¹' U) ↔ ∃ (V : Set D), IsOpen[inst_2] V ∧ g ⁻¹' V = U
have a : (∃ (t : Set B), IsOpen[inst_1] t ∧ f ⁻¹' t = p ⁻¹' U) ↔ ∃ (x : Set B), IsOpen[inst_1] (q ⁻¹' q '' x) ∧ g ⁻¹' q '' x = U
Tactic: simp_rw [hf.isOpen_iff,
    (Set.image_surjective.mpr hq.surjective).exists,
    ← hq.isQuotientMap.isOpen_preimage]
-- Lean 4 proof step from Mathlib.Topology.Maps.OpenQuotient (goal)
Goal:
A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst : TopologicalSpace A
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace D
f : A → B
g : C → D
p : A → C
q : B → D
h : g ∘ p = q ∘ f
hf : IsInducing f
hp : Surjective p
hq : IsOpenQuotientMap q
hg : Injective g
H : q ⁻¹' q '' range f ⊆ range f
U : Set C
⊢ (∃ (t : Set B), IsOpen[inst_1] t ∧ f ⁻¹' t = p ⁻¹' U) ↔
    ∃ (x : Set B), IsOpen[inst_1] (q ⁻¹' q '' x) ∧ g ⁻¹' q '' x = U
have a : (∃ (t : Set B), IsOpen[inst_1] t ∧ f ⁻¹' t = p ⁻¹' U) → ∃ (x : Set B), IsOpen[inst_1] (q ⁻¹' q '' x) ∧ g ⁻¹' q '' x = U
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Maps.OpenQuotient (goal)
Goal:
A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst : TopologicalSpace A
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace D
f : A → B
g : C → D
p : A → C
q : B → D
h : g ∘ p = q ∘ f
hf : IsInducing f
hp : Surjective p
hq : IsOpenQuotientMap q
hg : Injective g
H : q ⁻¹' q '' range f ⊆ range f
U : Set C
a :
  (∃ (t : Set B), IsOpen[inst_1] t ∧ f ⁻¹' t = p ⁻¹' U) →
    ∃ (x : Set B), IsOpen[inst_1] (q ⁻¹' q '' x) ∧ g ⁻¹' q '' x = U
⊢ (∃ (t : Set B), IsOpen[inst_1] t ∧ f ⁻¹' t = p ⁻¹' U) ↔
    ∃ (x : Set B), IsOpen[inst_1] (q ⁻¹' q '' x) ∧ g ⁻¹' q '' x = U
have a₁ : (∃ (x : Set B), IsOpen[inst_1] (q ⁻¹' q '' x) ∧ g ⁻¹' q '' x = U) → ∃ (t : Set B), IsOpen[inst_1] t ∧ f ⁻¹' t = p ⁻¹' U
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Maps.OpenQuotient (goal)
Goal:
A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst : TopologicalSpace A
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace D
f : A → B
g : C → D
p : A → C
q : B → D
h : g ∘ p = q ∘ f
hf : IsInducing f
hp : Surjective p
hq : IsOpenQuotientMap q
hg : Injective g
H : q ⁻¹' q '' range f ⊆ range f
U : Set C
V : Set B
hV : IsOpen[inst_1] V
e : f ⁻¹' V = p ⁻¹' U
⊢ ∃ (x : Set B), IsOpen[inst_1] (q ⁻¹' q '' x) ∧ g ⁻¹' q '' x = U
have a : g ⁻¹' q '' V = U
Tactic: refine ⟨V, hq.continuous.1 _ (hq.isOpenMap _ hV), ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Maps.OpenQuotient (goal)
Goal:
A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst : TopologicalSpace A
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace D
f : A → B
g : C → D
p : A → C
q : B → D
h : g ∘ p = q ∘ f
hf : IsInducing f
hp : Surjective p
hq : IsOpenQuotientMap q
hg : Injective g
H : q ⁻¹' q '' range f ⊆ range f
U : Set C
V : Set B
hV : IsOpen[inst_1] V
e : f ⁻¹' V = p ⁻¹' U
⊢ g ⁻¹' q '' V = U
have a : ∀ (x : C), x ∈ g ⁻¹' q '' V ↔ x ∈ U
Tactic: ext x