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 Y
inst_1 : TopologicalSpace X
hf : IsInducing f
s : Set X
x : X
⊢ x ∈ closure[inst_1] s ↔ x ∈ f ⁻¹' closure[inst] (f '' s)
have h : x ∈ closure[inst_1] s ↔ f x ∈ closure[inst] (f '' s)
Tactic: rw [Set.mem_preimage, ← closure_induced, hf.eq_induced]
-- Lean 4 proof step from Mathlib.Topology.Maps.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace Y
inst_1 : TopologicalSpace X
hf : IsInducing f
s : Set X
x : X
h : x ∈ closure[inst_1] s ↔ f x ∈ closure[inst] (f '' s)
⊢ x ∈ closure[inst_1] s ↔ x ∈ f ⁻¹' closure[inst] (f '' s)
have h₁ : x ∈ closure[inst_1] s ↔ x ∈ closure[induced f inst] s
Tactic: rw [Set.mem_preimage, ← closure_induced, hf.eq_induced]
-- Lean 4 proof step from Mathlib.Topology.Maps.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace Y
inst_1 : TopologicalSpace X
hf : IsInducing f
s : Set X
x : X
h : x ∈ closure[inst_1] s ↔ f x ∈ closure[inst] (f '' s)
h₁ : x ∈ closure[inst_1] s ↔ x ∈ closure[induced f inst] s
⊢ x ∈ closure[inst_1] s ↔ x ∈ f ⁻¹' closure[inst] (f '' s)
have h₂ : x ∈ closure[induced f inst] s ↔ x ∈ closure[induced f inst] s
Tactic: rw [Set.mem_preimage, ← closure_induced, hf.eq_induced]
-- Lean 4 proof step from Mathlib.Topology.Maps.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace Y
inst_1 : TopologicalSpace X
hf : IsInducing f
s : Set X
⊢ IsClosed[inst_1] s ↔ ∃ (t : Set Y), IsClosed[inst] t ∧ f ⁻¹' t = s
have rw : IsClosed[induced f inst] s ↔ ∃ (t : Set Y), IsClosed[inst] t ∧ f ⁻¹' t = s
Tactic: rw [hf.eq_induced, isClosed_induced_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 Y
inst_1 : TopologicalSpace X
hf : IsInducing f
s : Set X
rw : IsClosed[induced f inst] s ↔ ∃ (t : Set Y), IsClosed[inst] t ∧ f ⁻¹' t = s
⊢ IsClosed[inst_1] s ↔ ∃ (t : Set Y), IsClosed[inst] t ∧ f ⁻¹' t = s
have rw₁ : (∃ (t : Set Y), IsClosed[inst] t ∧ f ⁻¹' t = s) ↔ ∃ (t : Set Y), IsClosed[inst] t ∧ f ⁻¹' t = s
Tactic: rw [hf.eq_induced, isClosed_induced_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 Y
inst_1 : TopologicalSpace X
hf : IsInducing f
s : Set X
hs : IsClosed[inst_1] s
⊢ ∃ (c : Set Y), IsClosed[inst] c ∧ f '' s = c ∩ range f
have obtain : ∀ (c : Set Y) (hc : IsClosed[inst] c) (hs : IsClosed[inst_1] (f ⁻¹' c)),
  ∃ (c_1 : Set Y), IsClosed[inst] c_1 ∧ f '' f ⁻¹' c = c_1 ∩ range f
Tactic: obtain ⟨c, hc, rfl⟩ := hf.isClosed_iff.1 hs
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 Y
inst_1 : TopologicalSpace X
hf : IsInducing f
s : Set X
⊢ IsClosed[inst_1] s ↔ ∀ (x : X), f x ∈ closure[inst] (f '' s) → x ∈ s
have rw : IsClosed[induced f inst] s ↔ ∀ (x : X), f x ∈ closure[inst] (f '' s) → x ∈ s
Tactic: rw [hf.eq_induced, isClosed_induced_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 Y
inst_1 : TopologicalSpace X
hf : IsInducing f
s : Set X
rw : IsClosed[induced f inst] s ↔ ∀ (x : X), f x ∈ closure[inst] (f '' s) → x ∈ s
⊢ IsClosed[inst_1] s ↔ ∀ (x : X), f x ∈ closure[inst] (f '' s) → x ∈ s
have rw₁ : (∀ (a : X), f a ∈ closure[inst] (f '' s) → a ∈ s) ↔ ∀ (x : X), f x ∈ closure[inst] (f '' s) → x ∈ s
Tactic: rw [hf.eq_induced, isClosed_induced_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 Y
inst_1 : TopologicalSpace X
hf : IsInducing f
s : Set X
⊢ IsOpen[inst_1] s ↔ ∃ (t : Set Y), IsOpen[inst] t ∧ f ⁻¹' t = s
have rw : IsOpen[induced f inst] s ↔ ∃ (t : Set Y), IsOpen[inst] t ∧ f ⁻¹' t = s
Tactic: rw [hf.eq_induced, isOpen_induced_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 Y
inst_1 : TopologicalSpace X
hf : IsInducing f
s : Set X
rw : IsOpen[induced f inst] s ↔ ∃ (t : Set Y), IsOpen[inst] t ∧ f ⁻¹' t = s
⊢ IsOpen[inst_1] s ↔ ∃ (t : Set Y), IsOpen[inst] t ∧ f ⁻¹' t = s
have rw₁ : (∃ (t : Set Y), IsOpen[inst] t ∧ f ⁻¹' t = s) ↔ ∃ (t : Set Y), IsOpen[inst] t ∧ f ⁻¹' t = s
Tactic: rw [hf.eq_induced, isOpen_induced_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 Y
inst_1 : TopologicalSpace X
hf : IsInducing f
s : Set X
hs : IsOpen[inst_1] s
⊢ ∃ (c : Set Y), IsOpen[inst] c ∧ f '' s = c ∩ range f
have obtain : ∀ (c : Set Y) (hc : IsOpen[inst] c) (hs : IsOpen[inst_1] (f ⁻¹' c)),
  ∃ (c_1 : Set Y), IsOpen[inst] c_1 ∧ f '' f ⁻¹' c = c_1 ∩ range f
Tactic: obtain ⟨c, hc, rfl⟩ := hf.isOpen_iff.1 hs
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Topology.Maps.Basic (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace Y
inst_1 : TopologicalSpace X
inst_2 : IndiscreteTopology Y
f : X → Y
hf : IsInducing f
⊢ inst_1 = ⊤
have inst : IndiscreteTopology Y
Tactic: cases IndiscreteTopology.eq_top Y
Cleared hypotheses: inst, inst_2, hf
-- Lean 4 proof step from Mathlib.Topology.Maps.Basic (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace X
inst_3 : IndiscreteTopology Y
f : X → Y
hf : IsInducing f
inst : IndiscreteTopology Y
⊢ inst_2 = ⊤
have hf₁ : IsInducing f
Tactic: cases IndiscreteTopology.eq_top Y
Cleared hypotheses: inst_1, inst_3, hf
-- Lean 4 proof step from Mathlib.Topology.Maps.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
inst_1 : IndiscreteTopology Y
hf : IsInducing f
this : TopologicalSpace Y := ⊤
⊢ inst = ⊤
have refl : induced f ⊤ = ⊤
Tactic: rw [hf.eq_induced, induced_top]
-- Lean 4 proof step from Mathlib.Topology.Maps.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
inst_1 : IndiscreteTopology Y
hf : IsInducing f
this : TopologicalSpace Y := ⊤
refl : induced f ⊤ = ⊤
⊢ inst = ⊤
have refl₁ : Eq.{u_1 + 1} (α := TopologicalSpace X) ⊤ ⊤
Tactic: rw [hf.eq_induced, induced_top]
-- 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
⊢ IsEmbedding (g ∘ f) ↔ IsEmbedding f
have simp_rw : IsInducing (g ∘ f) ∧ Injective (g ∘ f) ↔ IsInducing f ∧ Injective f
Tactic: simp_rw [isEmbedding_iff, hg.isInducing.of_comp_iff, hg.injective.of_comp_iff f]
-- 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
simp_rw : IsInducing (g ∘ f) ∧ Injective (g ∘ f) ↔ IsInducing f ∧ Injective f
⊢ IsEmbedding (g ∘ f) ↔ IsEmbedding f
have simp_rw₁ : IsInducing f ∧ Injective (g ∘ f) ↔ IsInducing f ∧ Injective f
Tactic: simp_rw [isEmbedding_iff, hg.isInducing.of_comp_iff, hg.injective.of_comp_iff f]
-- 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 : IsCoinducing g
hf : IsCoinducing f
⊢ inst_2 = coinduced (g ∘ f) inst
have rw : coinduced g inst_1 = coinduced (g ∘ f) inst
Tactic: rw [hg.eq_coinduced, hf.eq_coinduced, coinduced_compose]
-- 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 : IsCoinducing g
hf : IsCoinducing f
rw : coinduced g inst_1 = coinduced (g ∘ f) inst
⊢ inst_2 = coinduced (g ∘ f) inst
have rw₁ : coinduced g (coinduced f inst) = coinduced (g ∘ f) inst
Tactic: rw [hg.eq_coinduced, hf.eq_coinduced, coinduced_compose]
-- 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 : IsCoinducing g
hf : IsCoinducing f
rw : coinduced g inst_1 = coinduced (g ∘ f) inst
rw₁ : coinduced g (coinduced f inst) = coinduced (g ∘ f) inst
⊢ inst_2 = coinduced (g ∘ f) inst
have rw₂ : coinduced (g ∘ f) inst = coinduced (g ∘ f) inst
Tactic: rw [hg.eq_coinduced, hf.eq_coinduced, coinduced_compose]
-- 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 : IsCoinducing f
⊢ IsCoinducing (g ∘ f) ↔ IsCoinducing g
have refine : ∀ (hgf : IsCoinducing (g ∘ f)) (s : Set Z), IsOpen[inst_1] (g ⁻¹' s) ↔ IsOpen[inst_2] s
Tactic: refine ⟨fun hgf ↦ .of_isOpen_preimage_iff_isOpen fun s ↦ ?_, fun hg ↦ hg.comp hf⟩
-- 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 : IsCoinducing f
hgf : IsCoinducing (g ∘ f)
s : Set Z
⊢ IsOpen[inst_1] (g ⁻¹' s) ↔ IsOpen[inst_2] s
have rw : IsOpen[inst_1] (g ⁻¹' s) ↔ IsOpen[inst] (g ∘ f ⁻¹' s)
Tactic: rw [← hgf.isOpen_preimage, Set.preimage_comp, hf.isOpen_preimage]
-- 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 : IsCoinducing f
hgf : IsCoinducing (g ∘ f)
s : Set Z
rw : IsOpen[inst_1] (g ⁻¹' s) ↔ IsOpen[inst] (g ∘ f ⁻¹' s)
⊢ IsOpen[inst_1] (g ⁻¹' s) ↔ IsOpen[inst_2] s
have rw₁ : IsOpen[inst_1] (g ⁻¹' s) ↔ IsOpen[inst] (f ⁻¹' g ⁻¹' s)
Tactic: rw [← hgf.isOpen_preimage, Set.preimage_comp, hf.isOpen_preimage]
-- 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 : IsCoinducing f
hgf : IsCoinducing (g ∘ f)
s : Set Z
rw : IsOpen[inst_1] (g ⁻¹' s) ↔ IsOpen[inst] (g ∘ f ⁻¹' s)
rw₁ : IsOpen[inst_1] (g ⁻¹' s) ↔ IsOpen[inst] (f ⁻¹' g ⁻¹' s)
⊢ IsOpen[inst_1] (g ⁻¹' s) ↔ IsOpen[inst_2] s
have rw₂ : IsOpen[inst_1] (g ⁻¹' s) ↔ IsOpen[inst_1] (g ⁻¹' s)
Tactic: rw [← hgf.isOpen_preimage, Set.preimage_comp, hf.isOpen_preimage]
-- 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 : Continuous[inst, inst_1] f
hg : Continuous[inst_1, inst_2] g
hgf : IsCoinducing (g ∘ f)
⊢ inst_2 ≤ coinduced g inst_1
have grw : coinduced (g ∘ f) inst ≤ coinduced g inst_1
Tactic: grw [hgf.eq_coinduced, ← coinduced_compose, hf.coinduced_le]
-- 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 : Continuous[inst, inst_1] f
hg : Continuous[inst_1, inst_2] g
hgf : IsCoinducing (g ∘ f)
grw : coinduced (g ∘ f) inst ≤ coinduced g inst_1
⊢ inst_2 ≤ coinduced g inst_1
have grw₁ : coinduced g (coinduced f inst) ≤ coinduced g inst_1
Tactic: grw [hgf.eq_coinduced, ← coinduced_compose, hf.coinduced_le]
-- 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 : Continuous[inst, inst_1] f
hg : Continuous[inst_1, inst_2] g
hgf : IsCoinducing (g ∘ f)
grw : coinduced (g ∘ f) inst ≤ coinduced g inst_1
grw₁ : coinduced g (coinduced f inst) ≤ coinduced g inst_1
⊢ inst_2 ≤ coinduced g inst_1
have grw₂ : coinduced g inst_1 ≤ coinduced g inst_1
Tactic: grw [hgf.eq_coinduced, ← coinduced_compose, hf.coinduced_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
hf : IsCoinducing f
hf' : Injective f
s : Set X
hs : IsOpen[inst] s
⊢ IsOpen[inst_1] (f '' s)
have rwa : IsOpen[inst] (f ⁻¹' f '' s)
Tactic: rwa [← hf.isOpen_preimage, preimage_image_eq _ hf']
-- 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
⊢ IsQuotientMap f ↔ Surjective f ∧ ∀ (s : Set Y), IsClosed[inst_1] s ↔ IsClosed[inst] (f ⁻¹' s)
have simp_rw : IsCoinducing f ∧ Surjective f ↔ Surjective f ∧ ∀ (s : Set Y), IsClosed[inst_1] s ↔ IsClosed[inst] (f ⁻¹' s)
Tactic: simp_rw [isQuotientMap_iff, isCoinducing_iff_isClosed, and_comm, iff_comm]
-- 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
simp_rw : IsCoinducing f ∧ Surjective f ↔ Surjective f ∧ ∀ (s : Set Y), IsClosed[inst_1] s ↔ IsClosed[inst] (f ⁻¹' s)
⊢ IsQuotientMap f ↔ Surjective f ∧ ∀ (s : Set Y), IsClosed[inst_1] s ↔ IsClosed[inst] (f ⁻¹' s)
have simp_rw₁ : (∀ (s : Set Y), IsClosed[inst] (f ⁻¹' s) ↔ IsClosed[inst_1] s) ∧ Surjective f ↔
  Surjective f ∧ ∀ (s : Set Y), IsClosed[inst_1] s ↔ IsClosed[inst] (f ⁻¹' s)
Tactic: simp_rw [isQuotientMap_iff, isCoinducing_iff_isClosed, and_comm, iff_comm]
-- 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
simp_rw : IsCoinducing f ∧ Surjective f ↔ Surjective f ∧ ∀ (s : Set Y), IsClosed[inst_1] s ↔ IsClosed[inst] (f ⁻¹' s)
simp_rw₁ :
  (∀ (s : Set Y), IsClosed[inst] (f ⁻¹' s) ↔ IsClosed[inst_1] s) ∧ Surjective f ↔
    Surjective f ∧ ∀ (s : Set Y), IsClosed[inst_1] s ↔ IsClosed[inst] (f ⁻¹' s)
⊢ IsQuotientMap f ↔ Surjective f ∧ ∀ (s : Set Y), IsClosed[inst_1] s ↔ IsClosed[inst] (f ⁻¹' s)
have simp_rw₂ : (Surjective f ∧ ∀ (s : Set Y), IsClosed[inst] (f ⁻¹' s) ↔ IsClosed[inst_1] s) ↔
  Surjective f ∧ ∀ (s : Set Y), IsClosed[inst_1] s ↔ IsClosed[inst] (f ⁻¹' s)
Tactic: simp_rw [isQuotientMap_iff, isCoinducing_iff_isClosed, and_comm, iff_comm]
-- 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 : IsQuotientMap f
⊢ IsQuotientMap (g ∘ f) ↔ IsQuotientMap g
have rw : IsCoinducing (g ∘ f) ∧ Surjective (g ∘ f) ↔ IsQuotientMap g
Tactic: rw [isQuotientMap_iff, isQuotientMap_iff, hf.isCoinducing.of_comp_iff, hf.surjective.of_comp_iff]
-- 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 : IsQuotientMap f
rw : IsCoinducing (g ∘ f) ∧ Surjective (g ∘ f) ↔ IsQuotientMap g
⊢ IsQuotientMap (g ∘ f) ↔ IsQuotientMap g
have rw₁ : IsCoinducing (g ∘ f) ∧ Surjective (g ∘ f) ↔ IsCoinducing g ∧ Surjective g
Tactic: rw [isQuotientMap_iff, isQuotientMap_iff, hf.isCoinducing.of_comp_iff, hf.surjective.of_comp_iff]
-- 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 : IsQuotientMap f
rw : IsCoinducing (g ∘ f) ∧ Surjective (g ∘ f) ↔ IsQuotientMap g
rw₁ : IsCoinducing (g ∘ f) ∧ Surjective (g ∘ f) ↔ IsCoinducing g ∧ Surjective g
⊢ IsQuotientMap (g ∘ f) ↔ IsQuotientMap g
have rw₂ : IsCoinducing g ∧ Surjective (g ∘ f) ↔ IsCoinducing g ∧ Surjective g
Tactic: rw [isQuotientMap_iff, isQuotientMap_iff, hf.isCoinducing.of_comp_iff, hf.surjective.of_comp_iff]
-- 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 : IsQuotientMap f
rw : IsCoinducing (g ∘ f) ∧ Surjective (g ∘ f) ↔ IsQuotientMap g
rw₁ : IsCoinducing (g ∘ f) ∧ Surjective (g ∘ f) ↔ IsCoinducing g ∧ Surjective g
rw₂ : IsCoinducing g ∧ Surjective (g ∘ f) ↔ IsCoinducing g ∧ Surjective g
⊢ IsQuotientMap (g ∘ f) ↔ IsQuotientMap g
have rw₃ : IsCoinducing g ∧ Surjective g ↔ IsCoinducing g ∧ Surjective g
Tactic: rw [isQuotientMap_iff, isQuotientMap_iff, hf.isCoinducing.of_comp_iff, hf.surjective.of_comp_iff]
-- 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 : IsQuotientMap f
⊢ Continuous[inst_1, inst_2] g ↔ Continuous[inst, inst_2] (g ∘ f)
have rw : coinduced g inst_1 ≤ inst_2 ↔ Continuous[inst, inst_2] (g ∘ f)
Tactic: rw [continuous_iff_coinduced_le, continuous_iff_coinduced_le, hf.eq_coinduced, coinduced_compose]
-- 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 : IsQuotientMap f
rw : coinduced g inst_1 ≤ inst_2 ↔ Continuous[inst, inst_2] (g ∘ f)
⊢ Continuous[inst_1, inst_2] g ↔ Continuous[inst, inst_2] (g ∘ f)
have rw₁ : coinduced g inst_1 ≤ inst_2 ↔ coinduced (g ∘ f) inst ≤ inst_2
Tactic: rw [continuous_iff_coinduced_le, continuous_iff_coinduced_le, hf.eq_coinduced, coinduced_compose]
-- 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 : IsQuotientMap f
rw : coinduced g inst_1 ≤ inst_2 ↔ Continuous[inst, inst_2] (g ∘ f)
rw₁ : coinduced g inst_1 ≤ inst_2 ↔ coinduced (g ∘ f) inst ≤ inst_2
⊢ Continuous[inst_1, inst_2] g ↔ Continuous[inst, inst_2] (g ∘ f)
have rw₂ : coinduced g (coinduced f inst) ≤ inst_2 ↔ coinduced (g ∘ f) inst ≤ inst_2
Tactic: rw [continuous_iff_coinduced_le, continuous_iff_coinduced_le, hf.eq_coinduced, coinduced_compose]
-- 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 : IsQuotientMap f
rw : coinduced g inst_1 ≤ inst_2 ↔ Continuous[inst, inst_2] (g ∘ f)
rw₁ : coinduced g inst_1 ≤ inst_2 ↔ coinduced (g ∘ f) inst ≤ inst_2
rw₂ : coinduced g (coinduced f inst) ≤ inst_2 ↔ coinduced (g ∘ f) inst ≤ inst_2
⊢ Continuous[inst_1, inst_2] g ↔ Continuous[inst, inst_2] (g ∘ f)
have rw₃ : coinduced (g ∘ f) inst ≤ inst_2 ↔ coinduced (g ∘ f) inst ≤ inst_2
Tactic: rw [continuous_iff_coinduced_le, continuous_iff_coinduced_le, hf.eq_coinduced, coinduced_compose]
-- 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 : IsOpenMap g
hf : IsOpenMap f
s : Set X
hs : IsOpen[inst] s
⊢ IsOpen[inst_2] (g ∘ f '' s)
have rw : IsOpen[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
f : X → Y
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
hf : IsOpenMap f
⊢ IsOpen[inst_1] (range f)
have rw : IsOpen[inst_1] (f '' univ)
Tactic: rw [← image_univ]
-- 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
hf' : Continuous[inst, inst_1] f
s : Set X
⊢ map f (𝓝ˢ s) = 𝓝ˢ (f '' s)
have rw : map f (𝓝ˢ (⋃ x ∈ s, {x})) = 𝓝ˢ (f '' ⋃ x ∈ s, {x})
Tactic: rw [← 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
hf : IsOpenMap f
hf' : Continuous[inst, inst_1] f
s : Set X
⊢ map f (𝓝ˢ (⋃ x ∈ s, {x})) = 𝓝ˢ (f '' ⋃ x ∈ s, {x})
have simp_rw : map f (𝓝ˢ (⋃ x ∈ s, {x})) = 𝓝ˢ (⋃ i ∈ s, f '' {i})
Tactic: simp_rw [image_iUnion, nhdsSet_iUnion, map_iSup, image_singleton, nhdsSet_singleton,
    hf.map_nhds_eq hf'.continuousAt]
-- 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
hf' : Continuous[inst, inst_1] f
s : Set X
simp_rw : map f (𝓝ˢ (⋃ x ∈ s, {x})) = 𝓝ˢ (⋃ i ∈ s, f '' {i})
⊢ map f (𝓝ˢ (⋃ x ∈ s, {x})) = 𝓝ˢ (f '' ⋃ x ∈ s, {x})
have simp_rw₁ : map f (⨆ i ∈ s, 𝓝ˢ {i}) = ⨆ i ∈ s, 𝓝ˢ (f '' {i})
Tactic: simp_rw [image_iUnion, nhdsSet_iUnion, map_iSup, image_singleton, nhdsSet_singleton,
    hf.map_nhds_eq hf'.continuousAt]
-- 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
hf' : Continuous[inst, inst_1] f
s : Set X
simp_rw : map f (𝓝ˢ (⋃ x ∈ s, {x})) = 𝓝ˢ (⋃ i ∈ s, f '' {i})
simp_rw₁ : map f (⨆ i ∈ s, 𝓝ˢ {i}) = ⨆ i ∈ s, 𝓝ˢ (f '' {i})
⊢ map f (𝓝ˢ (⋃ x ∈ s, {x})) = 𝓝ˢ (f '' ⋃ x ∈ s, {x})
have simp_rw₂ : Eq.{u_2 + 1} (α := Filter Y) (⨆ i ∈ s, map f (𝓝ˢ {i})) (⨆ i ∈ s, 𝓝ˢ (f '' {i}))
Tactic: simp_rw [image_iUnion, nhdsSet_iUnion, map_iSup, image_singleton, nhdsSet_singleton,
    hf.map_nhds_eq hf'.continuousAt]
-- 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
hf' : Continuous[inst, inst_1] f
s : Set X
simp_rw : map f (𝓝ˢ (⋃ x ∈ s, {x})) = 𝓝ˢ (⋃ i ∈ s, f '' {i})
simp_rw₁ : map f (⨆ i ∈ s, 𝓝ˢ {i}) = ⨆ i ∈ s, 𝓝ˢ (f '' {i})
simp_rw₂ : Eq.{u_2 + 1} (α := Filter Y) (⨆ i ∈ s, map f (𝓝ˢ {i})) (⨆ i ∈ s, 𝓝ˢ (f '' {i}))
⊢ map f (𝓝ˢ (⋃ x ∈ s, {x})) = 𝓝ˢ (f '' ⋃ x ∈ s, {x})
have simp_rw₃ : Eq.{u_2 + 1} (α := Filter Y) (⨆ i ∈ s, map f (𝓝ˢ {i})) (⨆ i ∈ s, 𝓝ˢ {f i})
Tactic: simp_rw [image_iUnion, nhdsSet_iUnion, map_iSup, image_singleton, nhdsSet_singleton,
    hf.map_nhds_eq hf'.continuousAt]
-- 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
hf' : Continuous[inst, inst_1] f
s : Set X
simp_rw : map f (𝓝ˢ (⋃ x ∈ s, {x})) = 𝓝ˢ (⋃ i ∈ s, f '' {i})
simp_rw₁ : map f (⨆ i ∈ s, 𝓝ˢ {i}) = ⨆ i ∈ s, 𝓝ˢ (f '' {i})
simp_rw₂ : Eq.{u_2 + 1} (α := Filter Y) (⨆ i ∈ s, map f (𝓝ˢ {i})) (⨆ i ∈ s, 𝓝ˢ (f '' {i}))
simp_rw₃ : Eq.{u_2 + 1} (α := Filter Y) (⨆ i ∈ s, map f (𝓝ˢ {i})) (⨆ i ∈ s, 𝓝ˢ {f i})
⊢ map f (𝓝ˢ (⋃ x ∈ s, {x})) = 𝓝ˢ (f '' ⋃ x ∈ s, {x})
have simp_rw₄ : Eq.{u_2 + 1} (α := Filter Y) (⨆ i ∈ s, map f (𝓝 i)) (⨆ i ∈ s, 𝓝 (f i))
Tactic: simp_rw [image_iUnion, nhdsSet_iUnion, map_iSup, image_singleton, nhdsSet_singleton,
    hf.map_nhds_eq hf'.continuousAt]
-- 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
⊢ 𝓝 (f x) = map f (map g (𝓝 (f x)))
have rw : 𝓝 (f x) = map (f ∘ g) (𝓝 (f x))
Tactic: rw [map_map, hgf.comp_eq_id, map_id]
-- 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
rw : 𝓝 (f x) = map (f ∘ g) (𝓝 (f x))
⊢ 𝓝 (f x) = map f (map g (𝓝 (f x)))
have rw₁ : 𝓝 (f x) = map id (𝓝 (f x))
Tactic: rw [map_map, hgf.comp_eq_id, map_id]
-- 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
rw : 𝓝 (f x) = map (f ∘ g) (𝓝 (f x))
rw₁ : 𝓝 (f x) = map id (𝓝 (f x))
⊢ 𝓝 (f x) = map f (map g (𝓝 (f x)))
have rw₂ : 𝓝 (f x) = 𝓝 (f x)
Tactic: rw [map_map, hgf.comp_eq_id, map_id]