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
h : ∀ (x : X), ∃ (g : Y → X), ContinuousAt g (f x) ∧ g (f x) = x ∧ RightInverse g f
x : X
g : Y → X
hgc : ContinuousAt g (f x)
hgx : g (f x) = x
hgf : RightInverse g f
⊢ map f (𝓝 (g (f x))) = map f (𝓝 x)
have rw : map f (𝓝 x) = map f (𝓝 x)
Tactic: rw [hgx]
-- 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
open_map : IsOpenMap f
cont : Continuous[inst, inst_1] f
surj : Surjective f
⊢ IsQuotientMap f
have rw : IsCoinducing f ∧ Surjective f
Tactic: rw [isQuotientMap_iff]
-- 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
open_map : IsOpenMap f
cont : Continuous[inst, inst_1] f
surj : Surjective f
⊢ IsCoinducing f ∧ Surjective f
have refine : ∀ (s : Set Y), IsOpen[inst] (f ⁻¹' s) ↔ IsOpen[inst_1] s
Tactic: refine ⟨.of_isOpen_preimage_iff_isOpen fun s ↦ ?_, surj⟩
-- 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 : IsOpenMap f
s : Set Y
⊢ f ⁻¹' closure[inst_1] s ⊆ closure[inst] (f ⁻¹' s)
have rw : (closure[inst] (f ⁻¹' s))ᶜ ⊆ (f ⁻¹' closure[inst_1] s)ᶜ
Tactic: rw [← compl_subset_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₁ : IsOpenMap f
h₂ : Injective f
h₃ : Continuous[inst, inst_1] f
s : Set X
hs' : IsClosed[inst] s
⊢ f ⁻¹' closure[inst_1] (f '' s) = s
have rw : closure[inst] (f ⁻¹' f '' s) = s
Tactic: rw [h₁.preimage_closure_eq_closure_preimage h₃, Set.preimage_image_eq _ h₂, hs'.closure_eq]
-- 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₁ : IsOpenMap f
h₂ : Injective f
h₃ : Continuous[inst, inst_1] f
s : Set X
hs' : IsClosed[inst] s
rw : closure[inst] (f ⁻¹' f '' s) = s
⊢ f ⁻¹' closure[inst_1] (f '' s) = s
have rw₁ : closure[inst] s = s
Tactic: rw [h₁.preimage_closure_eq_closure_preimage h₃, Set.preimage_image_eq _ h₂, hs'.closure_eq]
-- 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₁ : IsOpenMap f
h₂ : Injective f
h₃ : Continuous[inst, inst_1] f
s : Set X
hs' : IsClosed[inst] s
rw : closure[inst] (f ⁻¹' f '' s) = s
rw₁ : closure[inst] s = s
⊢ f ⁻¹' closure[inst_1] (f '' s) = s
have rw₂ : s = s
Tactic: rw [h₁.preimage_closure_eq_closure_preimage h₃, Set.preimage_image_eq _ h₂, hs'.closure_eq]
-- 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 : IsOpenMap f
x : X
l : Filter Y
h : ClusterPt (f x) l
⊢ ClusterPt x (comap f l)
have rw : (map f (𝓝 x) ⊓ l).NeBot
Tactic: rw [ClusterPt, ← map_neBot_iff, Filter.push_pull]
-- 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 : IsOpenMap f
x : X
l : Filter Y
h : AccPt (f x) l
⊢ AccPt x (comap f l)
have rw : ∀ (h : ClusterPt (f x) (𝓟 {f x}ᶜ ⊓ l)), ClusterPt x (𝓟 {x}ᶜ ⊓ comap f l)
Tactic: rw [accPt_iff_clusterPt] at h ⊢
Cleared hypotheses: 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
hf : IsOpenMap f
x : X
l : Filter Y
h : ClusterPt (f x) (𝓟 {f x}ᶜ ⊓ l)
⊢ ClusterPt x (𝓟 {x}ᶜ ⊓ comap f l)
have apply : comap f (𝓟 {f x}ᶜ ⊓ l) ≤ 𝓟 {x}ᶜ ⊓ comap f l
Tactic: apply (hf.clusterPt_comap h).mono
-- 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 : IsOpenMap f
x : X
l : Filter Y
h : ClusterPt (f x) (𝓟 {f x}ᶜ ⊓ l)
⊢ comap f (𝓟 {f x}ᶜ ⊓ l) ≤ 𝓟 {x}ᶜ ⊓ comap f l
have rw : 𝓟 (f ⁻¹' {f x})ᶜ ⊓ comap f l ≤ 𝓟 {x}ᶜ ⊓ comap f l
Tactic: rw [comap_inf, comap_principal, preimage_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
⊢ IsOpenMap f ↔ ∀ {u : Set X}, IsClosed[inst] u → IsClosed[inst_1] (kernImage f u)
have rw : (∀ (x : Set X), IsOpen[inst] xᶜ → IsOpen[inst_1] (f '' xᶜ)) ↔
  ∀ {u : Set X}, IsClosed[inst] u → IsClosed[inst_1] (kernImage f u)
Tactic: rw [IsOpenMap, compl_surjective.forall]
-- 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
⊢ IsOpenMap f ↔ ∀ (x : X) (l : Filter Y), ClusterPt (f x) l → ClusterPt x (comap f l)
have refine : ∀ (h : ∀ (x : X) (l : Filter Y), ClusterPt (f x) l → ClusterPt x (comap f l)), IsOpenMap f
Tactic: refine ⟨fun hf _ _ ↦ hf.clusterPt_comap, fun 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 : ∀ (x : X) (l : Filter Y), ClusterPt (f x) l → ClusterPt x (comap f l)
⊢ IsOpenMap f
have simp : ∀ (x : X), ∀ s ∈ 𝓝 x, f '' s ∈ 𝓝 (f x)
Tactic: simp only [isOpenMap_iff_nhds_le, le_map_iff]
-- 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 : ∀ (x : X) (l : Filter Y), ClusterPt (f x) l → ClusterPt x (comap f l)
x : X
s : Set X
hs : s ∈ 𝓝 x
⊢ f '' s ∈ 𝓝 (f x)
have contrapose : ∀ (hs : f '' s ∉ 𝓝 (f x)), s ∉ 𝓝 x
Tactic: contrapose hs
Cleared hypotheses: 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 : ∀ (x : X) (l : Filter Y), ClusterPt (f x) l → ClusterPt x (comap f l)
x : X
s : Set X
hs : f '' s ∉ 𝓝 (f x)
⊢ s ∉ 𝓝 x
have rw : ∀ (hs : ClusterPt (f x) (𝓟 (f '' s)ᶜ)), ClusterPt x (𝓟 sᶜ)
Tactic: rw [← mem_interior_iff_mem_nhds, mem_interior_iff_not_clusterPt_compl, not_not] at hs ⊢
Cleared hypotheses: 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
⊢ IsOpenMap f ↔ ∀ {s : Set X}, closure[inst_1] (kernImage f s) ⊆ kernImage f (closure[inst] s)
have rw : (∀ (x : Set X), f '' interior xᶜ ⊆ interior (f '' xᶜ)) ↔
  ∀ {s : Set X}, closure[inst_1] (kernImage f s) ⊆ kernImage f (closure[inst] s)
Tactic: rw [isOpenMap_iff_image_interior, compl_surjective.forall]
-- 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 : IsClosedMap g
hf : IsClosedMap f
s : Set X
hs : IsClosed[inst] s
⊢ IsClosed[inst_2] (g ∘ f '' s)
have rw : IsClosed[inst_2] (g '' f '' s)
Tactic: rw [image_comp]
-- 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
hf : Surjective f
hf' : Continuous[inst, inst_1] f
hfg : IsClosedMap (g ∘ f)
K : Set Y
hK : IsClosed[inst_1] K
⊢ IsClosed[inst_2] (g '' K)
have rw : IsClosed[inst_2] (g ∘ f '' f ⁻¹' K)
Tactic: rw [← image_preimage_eq K hf, ← image_comp]
-- 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
f' : Y → X
h : Continuous[inst_1, inst] f'
l_inv : LeftInverse f f'
r_inv : RightInverse f f'
s : Set X
hs : IsClosed[inst] s
⊢ IsClosed[inst_1] (f '' s)
have rw : IsClosed[inst_1] (f' ⁻¹' s)
Tactic: rw [image_eq_preimage_of_inverse r_inv l_inv]
-- 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 : ∀ (s : Set X), IsClosed[inst] s → s.Nonempty → IsClosed[inst_1] (f '' s)
s : Set X
hs : IsClosed[inst] s
⊢ IsClosed[inst_1] (f '' s)
have inl : ∀ (h2s : s = ∅), IsClosed[inst_1] (f '' s)
Tactic: rcases eq_empty_or_nonempty s with h2s | h2s
-- 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 : ∀ (s : Set X), IsClosed[inst] s → s.Nonempty → IsClosed[inst_1] (f '' s)
s : Set X
hs : IsClosed[inst] s
inl : ∀ (h2s : s = ∅), IsClosed[inst_1] (f '' s)
⊢ IsClosed[inst_1] (f '' s)
have inr : ∀ (h2s : s.Nonempty), IsClosed[inst_1] (f '' s)
Tactic: rcases eq_empty_or_nonempty s with h2s | h2s
-- 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 : ∀ (s : Set X), IsClosed[inst] s → s.Nonempty → IsClosed[inst_1] (f '' s)
s : Set X
hs : IsClosed[inst] s
h2s : s = ∅
⊢ IsClosed[inst_1] (f '' s)
have inl : IsClosed[inst_1] (f '' ∅)
Tactic: simp_rw [h2s, image_empty, isClosed_empty]
-- 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 : ∀ (s : Set X), IsClosed[inst] s → s.Nonempty → IsClosed[inst_1] (f '' s)
s : Set X
hs : IsClosed[inst] s
h2s : s = ∅
inl : IsClosed[inst_1] (f '' ∅)
⊢ IsClosed[inst_1] (f '' s)
have inl₁ : IsClosed[inst_1] ∅
Tactic: simp_rw [h2s, image_empty, isClosed_empty]
-- 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
⊢ IsClosedMap f ↔ ∀ {u : Set X}, IsOpen[inst] u → IsOpen[inst_1] (kernImage f u)
have rw : (∀ (x : Set X), IsClosed[inst] xᶜ → IsClosed[inst_1] (f '' xᶜ)) ↔
  ∀ {u : Set X}, IsOpen[inst] u → IsOpen[inst_1] (kernImage f u)
Tactic: rw [IsClosedMap, compl_surjective.forall]
-- 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 : IsInducing f
h : IsClosed[inst_1] (range f)
s : Set X
hs : IsClosed[inst] s
⊢ IsClosed[inst_1] (f '' s)
have rcases : ∀ (t : Set Y) (ht : IsClosed[inst_1] t) (hs : IsClosed[inst] (f ⁻¹' t)), IsClosed[inst_1] (f '' f ⁻¹' t)
Tactic: rcases hf.isClosed_iff.1 hs with ⟨t, ht, rfl⟩
Cleared hypotheses: 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
hf : IsInducing f
h : IsClosed[inst_1] (range f)
t : Set Y
ht : IsClosed[inst_1] t
hs : IsClosed[inst] (f ⁻¹' t)
⊢ IsClosed[inst_1] (f '' f ⁻¹' t)
have rw : IsClosed[inst_1] (t ∩ range f)
Tactic: rw [image_preimage_eq_inter_range]
-- 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
hs : ∀ (s : Set X), closure[inst_1] (f '' s) ⊆ f '' closure[inst] s
c : Set X
hc : IsClosed[inst] c
⊢ f '' closure[inst] c = f '' c
have rw : f '' c = f '' c
Tactic: rw [hc.closure_eq]
-- 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
⊢ IsClosedMap f ↔ ∀ {s : Set X}, kernImage f (interior s) ⊆ interior (kernImage f s)
have rw : (∀ (x : Set X), closure[inst_1] (f '' xᶜ) ⊆ f '' closure[inst] xᶜ) ↔
  ∀ {s : Set X}, kernImage f (interior s) ⊆ interior (kernImage f s)
Tactic: rw [isClosedMap_iff_closure_image, compl_surjective.forall]
-- 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
⊢ IsClosedMap f ↔ ∀ {s : Set Y}, comap f (𝓝ˢ s) ≤ 𝓝ˢ (f ⁻¹' s)
have simp_rw : (∀ {s : Set X}, kernImage f (interior s) ⊆ interior (kernImage f s)) ↔
  ∀ {s : Set Y} (x : Set X), s ⊆ kernImage f (interior x) → s ⊆ interior (kernImage f x)
Tactic: simp_rw [Filter.le_def, mem_comap'', ← subset_interior_iff_mem_nhdsSet,
    ← subset_kernImage_iff, isClosedMap_iff_kernImage_interior]
-- 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
⊢ IsClosedMap f ↔ ∀ {y : Y}, comap f (𝓝 y) ≤ 𝓝ˢ (f ⁻¹' {y})
have rw : (∀ {s : Set Y}, comap f (𝓝ˢ s) ≤ 𝓝ˢ (f ⁻¹' s)) ↔ ∀ {y : Y}, comap f (𝓝 y) ≤ 𝓝ˢ (f ⁻¹' {y})
Tactic: rw [isClosedMap_iff_comap_nhdsSet_le]
-- 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
⊢ (∀ {s : Set Y}, comap f (𝓝ˢ s) ≤ 𝓝ˢ (f ⁻¹' s)) ↔ ∀ {y : Y}, comap f (𝓝 y) ≤ 𝓝ˢ (f ⁻¹' {y})
have mp : (∀ {s : Set Y}, comap f (𝓝ˢ s) ≤ 𝓝ˢ (f ⁻¹' s)) → ∀ {y : Y}, comap f (𝓝 y) ≤ 𝓝ˢ (f ⁻¹' {y})
Tactic: constructor
-- 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
mp : (∀ {s : Set Y}, comap f (𝓝ˢ s) ≤ 𝓝ˢ (f ⁻¹' s)) → ∀ {y : Y}, comap f (𝓝 y) ≤ 𝓝ˢ (f ⁻¹' {y})
⊢ (∀ {s : Set Y}, comap f (𝓝ˢ s) ≤ 𝓝ˢ (f ⁻¹' s)) ↔ ∀ {y : Y}, comap f (𝓝 y) ≤ 𝓝ˢ (f ⁻¹' {y})
have mpr : (∀ {y : Y}, comap f (𝓝 y) ≤ 𝓝ˢ (f ⁻¹' {y})) → ∀ {s : Set Y}, comap f (𝓝ˢ s) ≤ 𝓝ˢ (f ⁻¹' s)
Tactic: constructor
-- 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 : ∀ {y : Y}, comap f (𝓝 y) ≤ 𝓝ˢ (f ⁻¹' {y})
s : Set Y
⊢ comap f (𝓝ˢ s) ≤ 𝓝ˢ (f ⁻¹' s)
have mpr : comap f (𝓝ˢ (⋃ x ∈ s, {x})) ≤ 𝓝ˢ (f ⁻¹' ⋃ x ∈ s, {x})
Tactic: rw [← Set.biUnion_of_singleton s]
-- 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 : ∀ {y : Y}, comap f (𝓝 y) ≤ 𝓝ˢ (f ⁻¹' {y})
s : Set Y
⊢ comap f (𝓝ˢ (⋃ x ∈ s, {x})) ≤ 𝓝ˢ (f ⁻¹' ⋃ x ∈ s, {x})
have mpr : LE.le.{u_1} (α := Filter X) (⨆ i ∈ s, comap f (𝓝 i)) (⨆ i ∈ s, 𝓝ˢ (f ⁻¹' {i}))
Tactic: simp_rw [preimage_iUnion, nhdsSet_iUnion, comap_iSup, nhdsSet_singleton]
-- Lean 4 proof step from Mathlib.Topology.Maps.Basic (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
hf : IsClosedMap f
p : X → Prop
y₀ : Y
H : ∀ x₀ ∈ f ⁻¹' {y₀}, ∀ᶠ (x : X) in 𝓝 x₀, p x
⊢ ∀ᶠ (y : Y) in 𝓝 y₀, ∀ x ∈ f ⁻¹' {y}, p x
have H₁ : ∀ᶠ (x : X) in 𝓝ˢ (f ⁻¹' {y₀}), p x
Tactic: rw [← eventually_nhdsSet_iff_forall] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Topology.Maps.Basic (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
hf : IsClosedMap f
p : X → Prop
y₀ : Y
H : ∀ᶠ (x : X) in 𝓝ˢ (f ⁻¹' {y₀}), p x
⊢ ∀ᶠ (y : Y) in 𝓝 y₀, ∀ x ∈ f ⁻¹' {y}, p x
have H₁ : ∀ᶠ (x : X) in comap f (𝓝 y₀), p x
Tactic: replace H := H.filter_mono hf.comap_nhds_le
Cleared hypotheses: 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
hf : IsClosedMap f
p : X → Prop
y₀ : Y
H : ∀ᶠ (x : X) in comap f (𝓝 y₀), p x
⊢ ∀ᶠ (y : Y) in 𝓝 y₀, ∀ x ∈ f ⁻¹' {y}, p x
have rwa : ∀ (H : ∀ᶠ (b : Y) in 𝓝 y₀, ∀ (a : X), f a = b → p a), ∀ᶠ (y : Y) in 𝓝 y₀, ∀ x ∈ f ⁻¹' {y}, p x
Tactic: rwa [eventually_comap] at H
Cleared hypotheses: 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
hf : IsClosedMap f
p : X → Prop
y₀ : Y
H : ∃ᶠ (y : Y) in 𝓝 y₀, ∃ x ∈ f ⁻¹' {y}, p x
⊢ ∃ x₀ ∈ f ⁻¹' {y₀}, ∃ᶠ (x : X) in 𝓝 x₀, p x
have contrapose! : ∀ (H : ∀ (x₀ : X) (_ : x₀ ∈ f ⁻¹' {y₀}), ∀ᶠ (x : X) in 𝓝 x₀, ¬p x),
  ∀ᶠ (x : Y) in 𝓝 y₀, ∀ (x_1 : X) (_ : x_1 ∈ f ⁻¹' {x}), ¬p x_1
Tactic: contrapose! H
Cleared hypotheses: 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
f_closed : IsClosedMap f
f_cont : Continuous[inst, inst_1] f
F : Filter X
⊢ (map f F).lift' closure[inst_1] = map f (F.lift' closure[inst])
have rw : F.lift' (closure[inst_1] ∘ image f) = F.lift' (image f ∘ closure[inst])
Tactic: rw [map_lift'_eq2 (monotone_closure Y), map_lift'_eq (monotone_closure X)]
-- 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
f_closed : IsClosedMap f
f_cont : Continuous[inst, inst_1] f
F : Filter X
⊢ F.lift' (closure[inst_1] ∘ image f) = F.lift' (image f ∘ closure[inst])
have e_h : closure[inst_1] ∘ image f = image f ∘ closure[inst]
Tactic: congr 1
-- 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
f_closed : IsClosedMap f
f_cont : Continuous[inst, inst_1] f
F : Filter X
⊢ closure[inst_1] ∘ image f = image f ∘ closure[inst]
have e_h : ∀ (s : Set X), (closure[inst_1] ∘ image f) s = (image f ∘ closure[inst]) s
Tactic: ext s : 1
-- 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
F : Filter X
f_closed : IsClosedMap f
f_cont : Continuous[inst, inst_1] f
y : Y
⊢ MapClusterPt y F f ↔ (F.lift' closure[inst] ⊓ 𝓟 (f ⁻¹' {y})).NeBot
have rw : ClusterPt y (map f F) ↔ (F.lift' closure[inst] ⊓ 𝓟 (f ⁻¹' {y})).NeBot
Tactic: rw [MapClusterPt, clusterPt_iff_lift'_closure', f_closed.lift'_closure_map_eq f_cont,
      ← comap_principal, ← map_neBot_iff f, Filter.push_pull, principal_singleton]
-- 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
F : Filter X
f_closed : IsClosedMap f
f_cont : Continuous[inst, inst_1] f
y : Y
rw : ClusterPt y (map f F) ↔ (F.lift' closure[inst] ⊓ 𝓟 (f ⁻¹' {y})).NeBot
⊢ MapClusterPt y F f ↔ (F.lift' closure[inst] ⊓ 𝓟 (f ⁻¹' {y})).NeBot
have rw₁ : ((map f F).lift' closure[inst_1] ⊓ pure y).NeBot ↔ (F.lift' closure[inst] ⊓ 𝓟 (f ⁻¹' {y})).NeBot
Tactic: rw [MapClusterPt, clusterPt_iff_lift'_closure', f_closed.lift'_closure_map_eq f_cont,
      ← comap_principal, ← map_neBot_iff f, Filter.push_pull, principal_singleton]
-- 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
F : Filter X
f_closed : IsClosedMap f
f_cont : Continuous[inst, inst_1] f
y : Y
rw : ClusterPt y (map f F) ↔ (F.lift' closure[inst] ⊓ 𝓟 (f ⁻¹' {y})).NeBot
rw₁ : ((map f F).lift' closure[inst_1] ⊓ pure y).NeBot ↔ (F.lift' closure[inst] ⊓ 𝓟 (f ⁻¹' {y})).NeBot
⊢ MapClusterPt y F f ↔ (F.lift' closure[inst] ⊓ 𝓟 (f ⁻¹' {y})).NeBot
have rw₂ : (map f (F.lift' closure[inst]) ⊓ pure y).NeBot ↔ (F.lift' closure[inst] ⊓ 𝓟 (f ⁻¹' {y})).NeBot
Tactic: rw [MapClusterPt, clusterPt_iff_lift'_closure', f_closed.lift'_closure_map_eq f_cont,
      ← comap_principal, ← map_neBot_iff f, Filter.push_pull, principal_singleton]
-- 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
F : Filter X
f_closed : IsClosedMap f
f_cont : Continuous[inst, inst_1] f
y : Y
rw : ClusterPt y (map f F) ↔ (F.lift' closure[inst] ⊓ 𝓟 (f ⁻¹' {y})).NeBot
rw₁ : ((map f F).lift' closure[inst_1] ⊓ pure y).NeBot ↔ (F.lift' closure[inst] ⊓ 𝓟 (f ⁻¹' {y})).NeBot
rw₂ : (map f (F.lift' closure[inst]) ⊓ pure y).NeBot ↔ (F.lift' closure[inst] ⊓ 𝓟 (f ⁻¹' {y})).NeBot
⊢ MapClusterPt y F f ↔ (F.lift' closure[inst] ⊓ 𝓟 (f ⁻¹' {y})).NeBot
have rw₃ : (map f (F.lift' closure[inst]) ⊓ pure y).NeBot ↔ (F.lift' closure[inst] ⊓ comap f (𝓟 {y})).NeBot
Tactic: rw [MapClusterPt, clusterPt_iff_lift'_closure', f_closed.lift'_closure_map_eq f_cont,
      ← comap_principal, ← map_neBot_iff f, Filter.push_pull, principal_singleton]
-- 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
F : Filter X
f_closed : IsClosedMap f
f_cont : Continuous[inst, inst_1] f
y : Y
rw : ClusterPt y (map f F) ↔ (F.lift' closure[inst] ⊓ 𝓟 (f ⁻¹' {y})).NeBot
rw₁ : ((map f F).lift' closure[inst_1] ⊓ pure y).NeBot ↔ (F.lift' closure[inst] ⊓ 𝓟 (f ⁻¹' {y})).NeBot
rw₂ : (map f (F.lift' closure[inst]) ⊓ pure y).NeBot ↔ (F.lift' closure[inst] ⊓ 𝓟 (f ⁻¹' {y})).NeBot
rw₃ : (map f (F.lift' closure[inst]) ⊓ pure y).NeBot ↔ (F.lift' closure[inst] ⊓ comap f (𝓟 {y})).NeBot
⊢ MapClusterPt y F f ↔ (F.lift' closure[inst] ⊓ 𝓟 (f ⁻¹' {y})).NeBot
have rw₄ : (map f (F.lift' closure[inst]) ⊓ pure y).NeBot ↔ (map f (F.lift' closure[inst] ⊓ comap f (𝓟 {y}))).NeBot
Tactic: rw [MapClusterPt, clusterPt_iff_lift'_closure', f_closed.lift'_closure_map_eq f_cont,
      ← comap_principal, ← map_neBot_iff f, Filter.push_pull, principal_singleton]
-- 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
F : Filter X
f_closed : IsClosedMap f
f_cont : Continuous[inst, inst_1] f
y : Y
rw : ClusterPt y (map f F) ↔ (F.lift' closure[inst] ⊓ 𝓟 (f ⁻¹' {y})).NeBot
rw₁ : ((map f F).lift' closure[inst_1] ⊓ pure y).NeBot ↔ (F.lift' closure[inst] ⊓ 𝓟 (f ⁻¹' {y})).NeBot
rw₂ : (map f (F.lift' closure[inst]) ⊓ pure y).NeBot ↔ (F.lift' closure[inst] ⊓ 𝓟 (f ⁻¹' {y})).NeBot
rw₃ : (map f (F.lift' closure[inst]) ⊓ pure y).NeBot ↔ (F.lift' closure[inst] ⊓ comap f (𝓟 {y})).NeBot
rw₄ : (map f (F.lift' closure[inst]) ⊓ pure y).NeBot ↔ (map f (F.lift' closure[inst] ⊓ comap f (𝓟 {y}))).NeBot
⊢ MapClusterPt y F f ↔ (F.lift' closure[inst] ⊓ 𝓟 (f ⁻¹' {y})).NeBot
have rw₅ : (map f (F.lift' closure[inst]) ⊓ pure y).NeBot ↔ (map f (F.lift' closure[inst]) ⊓ 𝓟 {y}).NeBot
Tactic: rw [MapClusterPt, clusterPt_iff_lift'_closure', f_closed.lift'_closure_map_eq f_cont,
      ← comap_principal, ← map_neBot_iff f, Filter.push_pull, principal_singleton]
-- 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
F : Filter X
f_closed : IsClosedMap f
f_cont : Continuous[inst, inst_1] f
y : Y
rw : ClusterPt y (map f F) ↔ (F.lift' closure[inst] ⊓ 𝓟 (f ⁻¹' {y})).NeBot
rw₁ : ((map f F).lift' closure[inst_1] ⊓ pure y).NeBot ↔ (F.lift' closure[inst] ⊓ 𝓟 (f ⁻¹' {y})).NeBot
rw₂ : (map f (F.lift' closure[inst]) ⊓ pure y).NeBot ↔ (F.lift' closure[inst] ⊓ 𝓟 (f ⁻¹' {y})).NeBot
rw₃ : (map f (F.lift' closure[inst]) ⊓ pure y).NeBot ↔ (F.lift' closure[inst] ⊓ comap f (𝓟 {y})).NeBot
rw₄ : (map f (F.lift' closure[inst]) ⊓ pure y).NeBot ↔ (map f (F.lift' closure[inst] ⊓ comap f (𝓟 {y}))).NeBot
rw₅ : (map f (F.lift' closure[inst]) ⊓ pure y).NeBot ↔ (map f (F.lift' closure[inst]) ⊓ 𝓟 {y}).NeBot
⊢ MapClusterPt y F f ↔ (F.lift' closure[inst] ⊓ 𝓟 (f ⁻¹' {y})).NeBot
have rw₆ : (map f (F.lift' closure[inst]) ⊓ pure y).NeBot ↔ (map f (F.lift' closure[inst]) ⊓ pure y).NeBot
Tactic: rw [MapClusterPt, clusterPt_iff_lift'_closure', f_closed.lift'_closure_map_eq f_cont,
      ← comap_principal, ← map_neBot_iff f, Filter.push_pull, principal_singleton]
-- 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 X
h : IsOpen[inst_1] (f '' s)
⊢ IsOpen[inst] s
have h₁ : f ⁻¹' f '' s = s
Tactic: convert! ← h.preimage hf.isEmbedding.continuous
-- 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
hf : IsOpenEmbedding f
l : Filter Z
x : X
⊢ Tendsto (g ∘ f) (𝓝 x) l ↔ Tendsto g (𝓝 (f x)) l
have rw : map g (𝓝 (f x)) ≤ l ↔ Tendsto g (𝓝 (f x)) l
Tactic: rw [Tendsto, ← map_map, hf.map_nhds_eq]