awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.IsLocalHomeomorph (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
h : IsLocalHomeomorphOn f s
hs : IsOpen[inst] s
hX : ∀ (a : (↑s : Type u_1)), IsOpen[instTopologicalSpaceSubtype] {a}
x : X
hx : x ∈ s
⊢ IsOpen[instTopologicalSpaceSubtype] {Subtype.mk (p := fun (x : Y) ↦ x ∈ f '' s) (f x) ⋯}
have obtain : ∀ (e : OpenPartialHomeomorph X Y) (hxe : x ∈ e.source) (h : IsLocalHomeomorphOn (↑e : X → Y) s),
  IsOpen[instTopologicalSpaceSubtype] {Subtype.mk (p := fun (x : Y) ↦ x ∈ (↑e : X → Y) '' s) ((↑e : X → Y) x) sorry}
Tactic: obtain ⟨e, hxe, rfl⟩ := h x hx
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.Topology.IsLocalHomeomorph (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
hs : IsOpen[inst] s
hX : ∀ (a : (↑s : Type u_1)), IsOpen[instTopologicalSpaceSubtype] {a}
x : X
hx : x ∈ s
e : OpenPartialHomeomorph X Y
hxe : x ∈ e.source
h : IsLocalHomeomorphOn (↑e : X → Y) s
⊢ IsOpen[instTopologicalSpaceSubtype] {Subtype.mk (p := fun (x : Y) ↦ x ∈ (↑e : X → Y) '' s) ((↑e : X → Y) x) ⋯}
have refine_1 : IsOpen[inst] {x}
Tactic: refine ⟨e '' {x}, e.isOpen_image_of_subset_source ?_ (Set.singleton_subset_iff.mpr hxe), ?_⟩
-- Lean 4 proof step from Mathlib.Topology.IsLocalHomeomorph (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
hs : IsOpen[inst] s
hX : ∀ (a : (↑s : Type u_1)), IsOpen[instTopologicalSpaceSubtype] {a}
x : X
hx : x ∈ s
e : OpenPartialHomeomorph X Y
hxe : x ∈ e.source
h : IsLocalHomeomorphOn (↑e : X → Y) s
refine_1 : IsOpen[inst] {x}
⊢ IsOpen[instTopologicalSpaceSubtype] {Subtype.mk (p := fun (x : Y) ↦ x ∈ (↑e : X → Y) '' s) ((↑e : X → Y) x) ⋯}
have refine_2 : Eq (α := Set { x : Y // x ∈ (↑e : X → Y) '' s })
  (Subtype.val (p := fun (x : Y) ↦ x ∈ (↑e : X → Y) '' s) ⁻¹' (↑e : X → Y) '' {x})
  {Subtype.mk (p := fun (x : Y) ↦ x ∈ (↑e : X → Y) '' s) ((↑e : X → Y) x) sorry}
Tactic: refine ⟨e '' {x}, e.isOpen_image_of_subset_source ?_ (Set.singleton_subset_iff.mpr hxe), ?_⟩
-- Lean 4 proof step from Mathlib.Topology.IsLocalHomeomorph (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
hs : IsOpen[inst] s
hX : ∀ (a : (↑s : Type u_1)), IsOpen[instTopologicalSpaceSubtype] {a}
x : X
hx : x ∈ s
e : OpenPartialHomeomorph X Y
hxe : x ∈ e.source
h : IsLocalHomeomorphOn (↑e : X → Y) s
⊢ Eq (α := Set { x : Y // x ∈ (↑e : X → Y) '' s })
    (Subtype.val (p := fun (x : Y) ↦ x ∈ (↑e : X → Y) '' s) ⁻¹' (↑e : X → Y) '' {x})
    {Subtype.mk (p := fun (x : Y) ↦ x ∈ (↑e : X → Y) '' s) ((↑e : X → Y) x) ⋯}
have refine_2 : ∀ (x_1 : { x : Y // x ∈ (↑e : X → Y) '' s }),
  Membership.mem (γ := Set { x : Y // x ∈ (↑e : X → Y) '' s })
      (Subtype.val (p := fun (x : Y) ↦ x ∈ (↑e : X → Y) '' s) ⁻¹' (↑e : X → Y) '' {x}) x_1 ↔
    Membership.mem (γ := Set { x : Y // x ∈ (↑e : X → Y) '' s })
      {Subtype.mk (p := fun (x : Y) ↦ x ∈ (↑e : X → Y) '' s) ((↑e : X → Y) x) sorry} x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.IsLocalHomeomorph (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
h : ∀ x ∈ s, ∃ (e : OpenPartialHomeomorph X Y), x ∈ e.source ∧ Set.EqOn f (↑e : X → Y) e.source
x : X
hx : x ∈ s
⊢ ∃ (e : OpenPartialHomeomorph X Y), x ∈ e.source ∧ f = (↑e : X → Y)
have obtain : ∀ (e : OpenPartialHomeomorph X Y) (hx : x ∈ e.source) (he : Set.EqOn f (↑e : X → Y) e.source),
  ∃ (e : OpenPartialHomeomorph X Y), x ∈ e.source ∧ f = (↑e : X → Y)
Tactic: obtain ⟨e, hx, he⟩ := h x hx
-- Lean 4 proof step from Mathlib.Topology.IsLocalHomeomorph (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
h : ∀ x ∈ s, ∃ (e : OpenPartialHomeomorph X Y), x ∈ e.source ∧ Set.EqOn f (↑e : X → Y) e.source
x : X
hx_1 : x ∈ s
e : OpenPartialHomeomorph X Y
hx_2 : x ∈ e.source
he : Set.EqOn f (↑e : X → Y) e.source
_x : X
hx : _x ∈ e.source
⊢ f _x ∈ e.target
have rw : (↑e : X → Y) _x ∈ e.target
Tactic: rw [he hx]
-- Lean 4 proof step from Mathlib.Topology.IsLocalHomeomorph (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
h : ∀ x ∈ s, ∃ (e : OpenPartialHomeomorph X Y), x ∈ e.source ∧ Set.EqOn f (↑e : X → Y) e.source
x : X
hx_1 : x ∈ s
e : OpenPartialHomeomorph X Y
hx_2 : x ∈ e.source
he : Set.EqOn f (↑e : X → Y) e.source
_x : X
hx : _x ∈ e.source
⊢ e.invFun (f _x) = _x
have rw : e.invFun ((↑e : X → Y) _x) = _x
Tactic: rw [he hx]
-- Lean 4 proof step from Mathlib.Topology.IsLocalHomeomorph (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
h : ∀ x ∈ s, ∃ (e : OpenPartialHomeomorph X Y), x ∈ e.source ∧ Set.EqOn f (↑e : X → Y) e.source
x : X
hx_1 : x ∈ s
e : OpenPartialHomeomorph X Y
hx : x ∈ e.source
he : Set.EqOn f (↑e : X → Y) e.source
_y : Y
hy : _y ∈ e.target
⊢ f (e.invFun _y) = _y
have rw : (↑e : X → Y) (e.invFun _y) = _y
Tactic: rw [he (e.map_target' hy)]
-- Lean 4 proof step from Mathlib.Topology.IsLocalHomeomorph (goal)
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
g : Y → Z
f : X → Y
s : Set X
hgf : IsLocalHomeomorphOn (g ∘ f) s
hg : IsLocalHomeomorphOn g (f '' s)
cont : ∀ x ∈ s, ContinuousAt f x
x : X
hx : x ∈ s
⊢ ∃ (e : OpenPartialHomeomorph X Y), x ∈ e.source ∧ Set.EqOn f (↑e : X → Y) e.source
have obtain : ∀ (g : OpenPartialHomeomorph Y Z) (hxg : f x ∈ g.source) (hgf : IsLocalHomeomorphOn ((↑g : Y → Z) ∘ f) s)
  (hg : IsLocalHomeomorphOn (↑g : Y → Z) (f '' s)),
  ∃ (e : OpenPartialHomeomorph X Y), x ∈ e.source ∧ Set.EqOn f (↑e : X → Y) e.source
Tactic: obtain ⟨g, hxg, rfl⟩ := hg (f x) ⟨x, hx, rfl⟩
Cleared hypotheses: g, hgf, hg
-- Lean 4 proof step from Mathlib.Topology.IsLocalHomeomorph (goal)
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
s : Set X
cont : ∀ x ∈ s, ContinuousAt f x
x : X
hx : x ∈ s
g : OpenPartialHomeomorph Y Z
hxg : f x ∈ g.source
hgf : IsLocalHomeomorphOn ((↑g : Y → Z) ∘ f) s
hg : IsLocalHomeomorphOn (↑g : Y → Z) (f '' s)
⊢ ∃ (e : OpenPartialHomeomorph X Y), x ∈ e.source ∧ Set.EqOn f (↑e : X → Y) e.source
have obtain : ∀ (gf : OpenPartialHomeomorph X Z) (hgf : x ∈ gf.source) (he : (↑g : Y → Z) ∘ f = (↑gf : X → Z)),
  ∃ (e : OpenPartialHomeomorph X Y), x ∈ e.source ∧ Set.EqOn f (↑e : X → Y) e.source
Tactic: obtain ⟨gf, hgf, he⟩ := hgf x hx
-- Lean 4 proof step from Mathlib.Topology.IsLocalHomeomorph (goal)
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
s : Set X
cont : ∀ x ∈ s, ContinuousAt f x
x : X
hx : x ∈ s
g : OpenPartialHomeomorph Y Z
hxg : f x ∈ g.source
hgf_1 : IsLocalHomeomorphOn ((↑g : Y → Z) ∘ f) s
hg : IsLocalHomeomorphOn (↑g : Y → Z) (f '' s)
gf : OpenPartialHomeomorph X Z
hgf : x ∈ gf.source
he : (↑g : Y → Z) ∘ f = (↑gf : X → Z)
⊢ ∃ (e : OpenPartialHomeomorph X Y), x ∈ e.source ∧ Set.EqOn f (↑e : X → Y) e.source
have refine : ∀ (y : X) (hy : y ∈ ((gf.restr (f ⁻¹' g.source)).trans g.symm).source),
  f y = (↑((gf.restr (f ⁻¹' g.source)).trans g.symm) : X → Y) y
Tactic: refine ⟨(gf.restr <| f ⁻¹' g.source).trans g.symm, ⟨⟨hgf, mem_interior_iff_mem_nhds.mpr
    ((cont x hx).preimage_mem_nhds <| g.open_source.mem_nhds hxg)⟩, he ▸ g.map_source hxg⟩,
    fun y hy ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.IsLocalHomeomorph (goal)
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
s : Set X
cont : ∀ x ∈ s, ContinuousAt f x
x : X
hx : x ∈ s
g : OpenPartialHomeomorph Y Z
hxg : f x ∈ g.source
hgf_1 : IsLocalHomeomorphOn ((↑g : Y → Z) ∘ f) s
hg : IsLocalHomeomorphOn (↑g : Y → Z) (f '' s)
gf : OpenPartialHomeomorph X Z
hgf : x ∈ gf.source
he : (↑g : Y → Z) ∘ f = (↑gf : X → Z)
y : X
hy : y ∈ ((gf.restr (f ⁻¹' g.source)).trans g.symm).source
⊢ f y = (↑((gf.restr (f ⁻¹' g.source)).trans g.symm) : X → Y) y
have change : f y = (↑g.symm : Z → Y) ((↑gf : X → Z) y)
Tactic: change f y = g.symm (gf y)
-- Lean 4 proof step from Mathlib.Topology.IsLocalHomeomorph (hypothesis)
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
s : Set X
cont : ∀ x ∈ s, ContinuousAt f x
x : X
hx : x ∈ s
g : OpenPartialHomeomorph Y Z
hxg : f x ∈ g.source
hgf_1 : IsLocalHomeomorphOn ((↑g : Y → Z) ∘ f) s
hg : IsLocalHomeomorphOn (↑g : Y → Z) (f '' s)
gf : OpenPartialHomeomorph X Z
hgf : x ∈ gf.source
he : (↑g : Y → Z) ∘ f = (↑gf : X → Z)
y : X
hy : y ∈ ((gf.restr (f ⁻¹' g.source)).trans g.symm).source
⊢ f y = (↑g.symm : Z → Y) ((↑gf : X → Z) y)
have this : f y ∈ g.source
Tactic: have : f y ∈ g.source := by apply interior_subset hy.1.2
-- Lean 4 proof step from Mathlib.Topology.IsLocalHomeomorph (goal)
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
s : Set X
cont : ∀ x ∈ s, ContinuousAt f x
x : X
hx : x ∈ s
g : OpenPartialHomeomorph Y Z
hxg : f x ∈ g.source
hgf_1 : IsLocalHomeomorphOn ((↑g : Y → Z) ∘ f) s
hg : IsLocalHomeomorphOn (↑g : Y → Z) (f '' s)
gf : OpenPartialHomeomorph X Z
hgf : x ∈ gf.source
he : (↑g : Y → Z) ∘ f = (↑gf : X → Z)
y : X
hy : y ∈ ((gf.restr (f ⁻¹' g.source)).trans g.symm).source
this : f y ∈ g.source
⊢ f y = (↑g.symm : Z → Y) ((↑gf : X → Z) y)
have rw : f y = (↑g.symm : Z → Y) (((↑g : Y → Z) ∘ f) y)
Tactic: rw [← he, g.eq_symm_apply this (by apply g.map_source this), Function.comp_apply]
-- Lean 4 proof step from Mathlib.Topology.IsLocalHomeomorph (goal)
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
s : Set X
cont : ∀ x ∈ s, ContinuousAt f x
x : X
hx : x ∈ s
g : OpenPartialHomeomorph Y Z
hxg : f x ∈ g.source
hgf_1 : IsLocalHomeomorphOn ((↑g : Y → Z) ∘ f) s
hg : IsLocalHomeomorphOn (↑g : Y → Z) (f '' s)
gf : OpenPartialHomeomorph X Z
hgf : x ∈ gf.source
he : (↑g : Y → Z) ∘ f = (↑gf : X → Z)
y : X
hy : y ∈ ((gf.restr (f ⁻¹' g.source)).trans g.symm).source
this : f y ∈ g.source
rw : f y = (↑g.symm : Z → Y) (((↑g : Y → Z) ∘ f) y)
⊢ f y = (↑g.symm : Z → Y) ((↑gf : X → Z) y)
have rw₁ : (↑g : Y → Z) (f y) = ((↑g : Y → Z) ∘ f) y
Tactic: rw [← he, g.eq_symm_apply this (by apply g.map_source this), Function.comp_apply]
-- Lean 4 proof step from Mathlib.Topology.IsLocalHomeomorph (goal)
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
s : Set X
cont : ∀ x ∈ s, ContinuousAt f x
x : X
hx : x ∈ s
g : OpenPartialHomeomorph Y Z
hxg : f x ∈ g.source
hgf_1 : IsLocalHomeomorphOn ((↑g : Y → Z) ∘ f) s
hg : IsLocalHomeomorphOn (↑g : Y → Z) (f '' s)
gf : OpenPartialHomeomorph X Z
hgf : x ∈ gf.source
he : (↑g : Y → Z) ∘ f = (↑gf : X → Z)
y : X
hy : y ∈ ((gf.restr (f ⁻¹' g.source)).trans g.symm).source
this : f y ∈ g.source
rw : f y = (↑g.symm : Z → Y) (((↑g : Y → Z) ∘ f) y)
rw₁ : (↑g : Y → Z) (f y) = ((↑g : Y → Z) ∘ f) y
⊢ f y = (↑g.symm : Z → Y) ((↑gf : X → Z) y)
have rw₂ : (↑g : Y → Z) (f y) = (↑g : Y → Z) (f y)
Tactic: rw [← he, g.eq_symm_apply this (by apply g.map_source this), Function.comp_apply]
-- Lean 4 proof step from Mathlib.Topology.IsLocalHomeomorph (goal)
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
g : Y → Z
f : X → Y
s : Set X
hgf : IsLocalHomeomorphOn (g ∘ f) s
hf : IsLocalHomeomorphOn f s
x : X
hx : x ∈ s
⊢ ∃ (e : OpenPartialHomeomorph Y Z), f x ∈ e.source ∧ Set.EqOn g (↑e : Y → Z) e.source
have obtain : ∀ (f : OpenPartialHomeomorph X Y) (hxf : x ∈ f.source) (hgf : IsLocalHomeomorphOn (g ∘ (↑f : X → Y)) s)
  (hf : IsLocalHomeomorphOn (↑f : X → Y) s),
  ∃ (e : OpenPartialHomeomorph Y Z), (↑f : X → Y) x ∈ e.source ∧ Set.EqOn g (↑e : Y → Z) e.source
Tactic: obtain ⟨f, hxf, rfl⟩ := hf x hx
Cleared hypotheses: f, hgf, hf
-- Lean 4 proof step from Mathlib.Topology.IsLocalHomeomorph (goal)
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
g : Y → Z
s : Set X
x : X
hx : x ∈ s
f : OpenPartialHomeomorph X Y
hxf : x ∈ f.source
hgf : IsLocalHomeomorphOn (g ∘ (↑f : X → Y)) s
hf : IsLocalHomeomorphOn (↑f : X → Y) s
⊢ ∃ (e : OpenPartialHomeomorph Y Z), (↑f : X → Y) x ∈ e.source ∧ Set.EqOn g (↑e : Y → Z) e.source
have obtain : ∀ (gf : OpenPartialHomeomorph X Z) (hgf : x ∈ gf.source) (he : g ∘ (↑f : X → Y) = (↑gf : X → Z)),
  ∃ (e : OpenPartialHomeomorph Y Z), (↑f : X → Y) x ∈ e.source ∧ Set.EqOn g (↑e : Y → Z) e.source
Tactic: obtain ⟨gf, hgf, he⟩ := hgf x hx
-- Lean 4 proof step from Mathlib.Topology.IsLocalHomeomorph (goal)
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
g : Y → Z
s : Set X
x : X
hx : x ∈ s
f : OpenPartialHomeomorph X Y
hxf : x ∈ f.source
hgf_1 : IsLocalHomeomorphOn (g ∘ (↑f : X → Y)) s
hf : IsLocalHomeomorphOn (↑f : X → Y) s
gf : OpenPartialHomeomorph X Z
hgf : x ∈ gf.source
he : g ∘ (↑f : X → Y) = (↑gf : X → Z)
⊢ ∃ (e : OpenPartialHomeomorph Y Z), (↑f : X → Y) x ∈ e.source ∧ Set.EqOn g (↑e : Y → Z) e.source
have refine_1 : (↑f : X → Y) x ∈ (↑f.symm.symm.symm : Y → X) ⁻¹' gf.source
Tactic: refine ⟨f.symm.trans gf, ⟨f.map_source hxf, ?_⟩, fun y hy ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.IsLocalHomeomorph (goal)
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
g : Y → Z
s : Set X
x : X
hx : x ∈ s
f : OpenPartialHomeomorph X Y
hxf : x ∈ f.source
hgf_1 : IsLocalHomeomorphOn (g ∘ (↑f : X → Y)) s
hf : IsLocalHomeomorphOn (↑f : X → Y) s
gf : OpenPartialHomeomorph X Z
hgf : x ∈ gf.source
he : g ∘ (↑f : X → Y) = (↑gf : X → Z)
refine_1 : (↑f : X → Y) x ∈ (↑f.symm.symm.symm : Y → X) ⁻¹' gf.source
⊢ ∃ (e : OpenPartialHomeomorph Y Z), (↑f : X → Y) x ∈ e.source ∧ Set.EqOn g (↑e : Y → Z) e.source
have refine_2 : ∀ (y : Y) (hy : y ∈ (f.symm.trans gf).source), g y = (↑(f.symm.trans gf) : Y → Z) y
Tactic: refine ⟨f.symm.trans gf, ⟨f.map_source hxf, ?_⟩, fun y hy ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.IsLocalHomeomorph (goal)
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
g : Y → Z
s : Set X
x : X
hx : x ∈ s
f : OpenPartialHomeomorph X Y
hxf : x ∈ f.source
hgf_1 : IsLocalHomeomorphOn (g ∘ (↑f : X → Y)) s
hf : IsLocalHomeomorphOn (↑f : X → Y) s
gf : OpenPartialHomeomorph X Z
hgf : x ∈ gf.source
he : g ∘ (↑f : X → Y) = (↑gf : X → Z)
y : Y
hy : y ∈ (f.symm.trans gf).source
⊢ g y = (↑(f.symm.trans gf) : Y → Z) y
have refine_2 : g y = (↑gf : X → Z) ((↑f.symm : Y → X) y)
Tactic: change g y = gf (f.symm y)
-- Lean 4 proof step from Mathlib.Topology.IsLocalHomeomorph (goal)
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
g : Y → Z
s : Set X
x : X
hx : x ∈ s
f : OpenPartialHomeomorph X Y
hxf : x ∈ f.source
hgf_1 : IsLocalHomeomorphOn (g ∘ (↑f : X → Y)) s
hf : IsLocalHomeomorphOn (↑f : X → Y) s
gf : OpenPartialHomeomorph X Z
hgf : x ∈ gf.source
he : g ∘ (↑f : X → Y) = (↑gf : X → Z)
y : Y
hy : y ∈ (f.symm.trans gf).source
⊢ g y = (↑gf : X → Z) ((↑f.symm : Y → X) y)
have refine_2 : g y = (g ∘ (↑f : X → Y)) ((↑f.symm : Y → X) y)
Tactic: rw [← he, Function.comp_apply, f.right_inv hy.1]
-- Lean 4 proof step from Mathlib.Topology.IsLocalHomeomorph (goal)
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
g : Y → Z
s : Set X
x : X
hx : x ∈ s
f : OpenPartialHomeomorph X Y
hxf : x ∈ f.source
hgf_1 : IsLocalHomeomorphOn (g ∘ (↑f : X → Y)) s
hf : IsLocalHomeomorphOn (↑f : X → Y) s
gf : OpenPartialHomeomorph X Z
hgf : x ∈ gf.source
he : g ∘ (↑f : X → Y) = (↑gf : X → Z)
y : Y
hy : y ∈ (f.symm.trans gf).source
refine_2 : g y = (g ∘ (↑f : X → Y)) ((↑f.symm : Y → X) y)
⊢ g y = (↑gf : X → Z) ((↑f.symm : Y → X) y)
have refine_2₁ : g y = g ((↑f : X → Y) ((↑f.symm : Y → X) y))
Tactic: rw [← he, Function.comp_apply, f.right_inv hy.1]
-- Lean 4 proof step from Mathlib.Topology.IsLocalHomeomorph (goal)
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
g : Y → Z
s : Set X
x : X
hx : x ∈ s
f : OpenPartialHomeomorph X Y
hxf : x ∈ f.source
hgf_1 : IsLocalHomeomorphOn (g ∘ (↑f : X → Y)) s
hf : IsLocalHomeomorphOn (↑f : X → Y) s
gf : OpenPartialHomeomorph X Z
hgf : x ∈ gf.source
he : g ∘ (↑f : X → Y) = (↑gf : X → Z)
y : Y
hy : y ∈ (f.symm.trans gf).source
refine_2 : g y = (g ∘ (↑f : X → Y)) ((↑f.symm : Y → X) y)
refine_2₁ : g y = g ((↑f : X → Y) ((↑f.symm : Y → X) y))
⊢ g y = (↑gf : X → Z) ((↑f.symm : Y → X) y)
have refine_2₂ : g y = g y
Tactic: rw [← he, Function.comp_apply, f.right_inv hy.1]
-- Lean 4 proof step from Mathlib.Topology.IsLocalHomeomorph (goal)
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
g : Y → Z
f : X → Y
s : Set X
t : Set Y
hg : IsLocalHomeomorphOn g t
hf : IsLocalHomeomorphOn f s
h : Set.MapsTo f s t
x : X
hx : x ∈ s
⊢ ∃ (e : OpenPartialHomeomorph X Z), x ∈ e.source ∧ g ∘ f = (↑e : X → Z)
have obtain : ∀ (eg : OpenPartialHomeomorph Y Z) (hxg : f x ∈ eg.source) (hg : IsLocalHomeomorphOn (↑eg : Y → Z) t),
  ∃ (e : OpenPartialHomeomorph X Z), x ∈ e.source ∧ (↑eg : Y → Z) ∘ f = (↑e : X → Z)
Tactic: obtain ⟨eg, hxg, rfl⟩ := hg (f x) (h hx)
Cleared hypotheses: g, hg
-- Lean 4 proof step from Mathlib.Topology.IsLocalHomeomorph (goal)
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
s : Set X
t : Set Y
hf : IsLocalHomeomorphOn f s
h : Set.MapsTo f s t
x : X
hx : x ∈ s
eg : OpenPartialHomeomorph Y Z
hxg : f x ∈ eg.source
hg : IsLocalHomeomorphOn (↑eg : Y → Z) t
⊢ ∃ (e : OpenPartialHomeomorph X Z), x ∈ e.source ∧ (↑eg : Y → Z) ∘ f = (↑e : X → Z)
have obtain : ∀ (ef : OpenPartialHomeomorph X Y) (hxf : x ∈ ef.source) (hf : IsLocalHomeomorphOn (↑ef : X → Y) s)
  (h : Set.MapsTo (↑ef : X → Y) s t) (hxg : (↑ef : X → Y) x ∈ eg.source),
  ∃ (e : OpenPartialHomeomorph X Z), x ∈ e.source ∧ (↑eg : Y → Z) ∘ (↑ef : X → Y) = (↑e : X → Z)
Tactic: obtain ⟨ef, hxf, rfl⟩ := hf x hx
Cleared hypotheses: f, hf, h, hxg
-- Lean 4 proof step from Mathlib.Topology.IsLocalHomeomorph (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
⊢ IsLocalHomeomorph f ↔ ∀ (x : X), ∃ U ∈ 𝓝 x, IsOpenEmbedding (U.restrict (π := fun (a : X) ↦ Y) f)
have simp_rw : IsLocalHomeomorphOn f Set.univ ↔ ∀ (x : X), ∃ U ∈ 𝓝 x, IsOpenEmbedding (U.restrict (π := fun (a : X) ↦ Y) f)
Tactic: simp_rw [isLocalHomeomorph_iff_isLocalHomeomorphOn_univ,
    isLocalHomeomorphOn_iff_isOpenEmbedding_restrict, imp_iff_right (Set.mem_univ _)]
-- Lean 4 proof step from Mathlib.Topology.IsLocalHomeomorph (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
simp_rw : IsLocalHomeomorphOn f Set.univ ↔ ∀ (x : X), ∃ U ∈ 𝓝 x, IsOpenEmbedding (U.restrict (π := fun (a : X) ↦ Y) f)
⊢ IsLocalHomeomorph f ↔ ∀ (x : X), ∃ U ∈ 𝓝 x, IsOpenEmbedding (U.restrict (π := fun (a : X) ↦ Y) f)
have simp_rw₁ : (∀ (x : X), Membership.mem (γ := Set X) Set.univ x → ∃ U ∈ 𝓝 x, IsOpenEmbedding (U.restrict (π := fun (a : X) ↦ Y) f)) ↔
  ∀ (x : X), ∃ U ∈ 𝓝 x, IsOpenEmbedding (U.restrict (π := fun (a : X) ↦ Y) f)
Tactic: simp_rw [isLocalHomeomorph_iff_isLocalHomeomorphOn_univ,
    isLocalHomeomorphOn_iff_isOpenEmbedding_restrict, imp_iff_right (Set.mem_univ _)]
-- Lean 4 proof step from Mathlib.Topology.IsLocalHomeomorph (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
h : IsLocalHomeomorph f
⊢ DiscreteTopology.{u_2} (↑(Set.range f) : Type u_2) ↔ DiscreteTopology X
have rw : DiscreteTopology.{u_2} (↑(f '' Set.univ) : Type u_2) ↔ DiscreteTopology.{u_1} (↑Set.univ : Type u_1)
Tactic: rw [← Set.image_univ, ← (Homeomorph.Set.univ X).discreteTopology_iff]
-- Lean 4 proof step from Mathlib.Topology.IsLocalHomeomorph (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
h : IsLocalHomeomorph f
hs : Function.Surjective f
⊢ DiscreteTopology X ↔ DiscreteTopology Y
have rw : DiscreteTopology X ↔ DiscreteTopology.{u_2} (↑Set.univ : Type u_2)
Tactic: rw [← (Homeomorph.Set.univ Y).discreteTopology_iff, ← hs.range_eq, h.discreteTopology_range_iff]
-- Lean 4 proof step from Mathlib.Topology.IsLocalHomeomorph (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
h : IsLocalHomeomorph f
hs : Function.Surjective f
rw : DiscreteTopology X ↔ DiscreteTopology.{u_2} (↑Set.univ : Type u_2)
⊢ DiscreteTopology X ↔ DiscreteTopology Y
have rw₁ : DiscreteTopology X ↔ DiscreteTopology.{u_2} (↑(Set.range f) : Type u_2)
Tactic: rw [← (Homeomorph.Set.univ Y).discreteTopology_iff, ← hs.range_eq, h.discreteTopology_range_iff]
-- Lean 4 proof step from Mathlib.Topology.IsLocalHomeomorph (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
h : IsLocalHomeomorph f
hs : Function.Surjective f
rw : DiscreteTopology X ↔ DiscreteTopology.{u_2} (↑Set.univ : Type u_2)
rw₁ : DiscreteTopology X ↔ DiscreteTopology.{u_2} (↑(Set.range f) : Type u_2)
⊢ DiscreteTopology X ↔ DiscreteTopology Y
have rw₂ : DiscreteTopology X ↔ DiscreteTopology X
Tactic: rw [← (Homeomorph.Set.univ Y).discreteTopology_iff, ← hs.range_eq, h.discreteTopology_range_iff]
-- Lean 4 proof step from Mathlib.Topology.IsLocalHomeomorph (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsLocalHomeomorph f
x : X
⊢ ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ Set.InjOn f U
have obtain : ∀ (f : OpenPartialHomeomorph X Y) (hx : x ∈ f.source) (hf : IsLocalHomeomorph (↑f : X → Y)),
  ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ Set.InjOn (↑f : X → Y) U
Tactic: obtain ⟨f, hx, rfl⟩ := hf x
Cleared hypotheses: f, hf
-- Lean 4 proof step from Mathlib.Topology.IsLocalHomeomorph (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsLocalHomeomorph f
⊢ IsTopologicalBasis.{u_1} (α := X)
    {U : Set X |
      ∃ (V : Set Y),
        IsOpen[inst_1] V ∧
          ∃ (s : ContinuousMap.{u_2, u_1} (↑V : Type u_2) X),
            Eq (α := (↑V : Type u_2) → Y) (f ∘ (⇑s : (a : (↑V : Type u_2)) → X))
                (Subtype.val (p := fun (x : Y) ↦ x ∈ V)) ∧
              Set.range.{u_1, u_2 + 1} (ι := (↑V : Type u_2)) (⇑s : (a : (↑V : Type u_2)) → X) = U}
have refine_1 : ∀ (u : Set X),
  Membership.mem (γ := Set (Set X))
      {U : Set X |
        ∃ (V : Set Y),
          IsOpen[inst_1] V ∧
            ∃ (s : ContinuousMap.{u_2, u_1} (↑V : Type u_2) X),
              Eq (α := (↑V : Type u_2) → Y) (f ∘ (⇑s : (a : (↑V : Type u_2)) → X))
                  (Subtype.val (p := fun (x : Y) ↦ x ∈ V)) ∧
                Set.range.{u_1, u_2 + 1} (ι := (↑V : Type u_2)) (⇑s : (a : (↑V : Type u_2)) → X) = U}
      u →
    IsOpen[inst] u
Tactic: refine isTopologicalBasis_of_isOpen_of_nhds ?_ fun x U hx hU ↦ ?_