awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Constructions (hypothesis)
Goal:
X_1 : Type u_1
X'_1 : Type u_2
Y : Type u_3
Y' : Type u_4
Z_1 : Type u_5
Z' : Type u_6
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace X'_1
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Y'
inst_4 : TopologicalSpace Z_1
inst_5 : TopologicalSpace Z'
e_1 : OpenPartialHomeomorph X_1 Y
X : Type u_7
X' : Type u_8
Z : Type u_9
inst_6 : TopologicalSpace X
inst_7 : TopologicalSpace X'
inst_8 : TopologicalSpace Z
inst_9 : Nonempty Z
f : X → X'
e : OpenPartialHomeomorph X Z
hf : IsOpenEmbedding f
h : Nonempty X
F : X' → Z := extend f (↑e : X → Z) fun (x : X') ↦ Classical.arbitrary Z
F_eq : F = extend f (↑e : X → Z) fun (x : X') ↦ Classical.arbitrary Z
⊢ ContinuousOn F (f '' e.source)
have heq : EqOn F ((↑e : X → Z) ∘ (↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm : X' → X)) (f '' e.source)
Tactic: have heq : EqOn F (e ∘ (hf.toOpenPartialHomeomorph).symm) (f '' e.source) := by
      intro x ⟨x₀, hx₀, hxx₀⟩
      rw [← hxx₀, F_eq, hf.injective.extend_apply e, comp_apply,
        hf.toOpenPartialHomeomorph_left_inv]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Constructions (goal)
Goal:
X_1 : Type u_1
X'_1 : Type u_2
Y : Type u_3
Y' : Type u_4
Z_1 : Type u_5
Z' : Type u_6
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace X'_1
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Y'
inst_4 : TopologicalSpace Z_1
inst_5 : TopologicalSpace Z'
e_1 : OpenPartialHomeomorph X_1 Y
X : Type u_7
X' : Type u_8
Z : Type u_9
inst_6 : TopologicalSpace X
inst_7 : TopologicalSpace X'
inst_8 : TopologicalSpace Z
inst_9 : Nonempty Z
f : X → X'
e : OpenPartialHomeomorph X Z
hf : IsOpenEmbedding f
h : Nonempty X
F : X' → Z := extend f (↑e : X → Z) fun (x : X') ↦ Classical.arbitrary Z
F_eq : F = extend f (↑e : X → Z) fun (x : X') ↦ Classical.arbitrary Z
heq : EqOn F ((↑e : X → Z) ∘ (↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm : X' → X)) (f '' e.source)
⊢ ContinuousOn ((↑e : X → Z) ∘ (↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm : X' → X)) (f '' e.source)
have hf₁ : ContinuousOn (↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm : X' → X) (f '' e.source)
Tactic: apply e.continuousOn_toFun.comp
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Constructions (goal)
Goal:
X_1 : Type u_1
X'_1 : Type u_2
Y : Type u_3
Y' : Type u_4
Z_1 : Type u_5
Z' : Type u_6
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace X'_1
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Y'
inst_4 : TopologicalSpace Z_1
inst_5 : TopologicalSpace Z'
e_1 : OpenPartialHomeomorph X_1 Y
X : Type u_7
X' : Type u_8
Z : Type u_9
inst_6 : TopologicalSpace X
inst_7 : TopologicalSpace X'
inst_8 : TopologicalSpace Z
inst_9 : Nonempty Z
f : X → X'
e : OpenPartialHomeomorph X Z
hf : IsOpenEmbedding f
h : Nonempty X
F : X' → Z := extend f (↑e : X → Z) fun (x : X') ↦ Classical.arbitrary Z
F_eq : F = extend f (↑e : X → Z) fun (x : X') ↦ Classical.arbitrary Z
heq : EqOn F ((↑e : X → Z) ∘ (↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm : X' → X)) (f '' e.source)
hf₁ : ContinuousOn (↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm : X' → X) (f '' e.source)
⊢ ContinuousOn ((↑e : X → Z) ∘ (↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm : X' → X)) (f '' e.source)
have h : MapsTo (↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm : X' → X) (f '' e.source) e.source
Tactic: apply e.continuousOn_toFun.comp
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Constructions (goal)
Goal:
X_1 : Type u_1
X'_1 : Type u_2
Y : Type u_3
Y' : Type u_4
Z_1 : Type u_5
Z' : Type u_6
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace X'_1
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Y'
inst_4 : TopologicalSpace Z_1
inst_5 : TopologicalSpace Z'
e_1 : OpenPartialHomeomorph X_1 Y
X : Type u_7
X' : Type u_8
Z : Type u_9
inst_6 : TopologicalSpace X
inst_7 : TopologicalSpace X'
inst_8 : TopologicalSpace Z
inst_9 : Nonempty Z
f : X → X'
e : OpenPartialHomeomorph X Z
hf : IsOpenEmbedding f
h : Nonempty X
F : X' → Z := extend f (↑e : X → Z) fun (x : X') ↦ Classical.arbitrary Z
F_eq : F = extend f (↑e : X → Z) fun (x : X') ↦ Classical.arbitrary Z
heq : EqOn F ((↑e : X → Z) ∘ (↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm : X' → X)) (f '' e.source)
x' : X'
⊢ x' ∈ f '' e.source → (↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm : X' → X) x' ∈ e.source
have h : ∀ (x : X) (hx : x ∈ e.source) (hx'x : f x = x'),
  (↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm : X' → X) x' ∈ e.source
Tactic: ⟨x, hx, hx'x⟩
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Constructions (hypothesis)
Goal:
X_1 : Type u_1
X'_1 : Type u_2
Y : Type u_3
Y' : Type u_4
Z_1 : Type u_5
Z' : Type u_6
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace X'_1
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Y'
inst_4 : TopologicalSpace Z_1
inst_5 : TopologicalSpace Z'
e_1 : OpenPartialHomeomorph X_1 Y
X : Type u_7
X' : Type u_8
Z : Type u_9
inst_6 : TopologicalSpace X
inst_7 : TopologicalSpace X'
inst_8 : TopologicalSpace Z
inst_9 : Nonempty Z
f : X → X'
e : OpenPartialHomeomorph X Z
hf : IsOpenEmbedding f
h : Nonempty X
F : X' → Z := extend f (↑e : X → Z) fun (x : X') ↦ Classical.arbitrary Z
F_eq : F = extend f (↑e : X → Z) fun (x : X') ↦ Classical.arbitrary Z
heq : EqOn F ((↑e : X → Z) ∘ (↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm : X' → X)) (f '' e.source)
⊢ ContinuousOn (↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm : X' → X) (f '' e.source)
have this : ContinuousOn (↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm : X' → X) (f '' univ)
Tactic: have : ContinuousOn (hf.toOpenPartialHomeomorph).symm (f '' univ) :=
        (hf.toOpenPartialHomeomorph).continuousOn_invFun
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Constructions (hypothesis)
Goal:
X_1 : Type u_1
X'_1 : Type u_2
Y : Type u_3
Y' : Type u_4
Z_1 : Type u_5
Z' : Type u_6
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace X'_1
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Y'
inst_4 : TopologicalSpace Z_1
inst_5 : TopologicalSpace Z'
e_1 : OpenPartialHomeomorph X_1 Y
X : Type u_7
X' : Type u_8
Z : Type u_9
inst_6 : TopologicalSpace X
inst_7 : TopologicalSpace X'
inst_8 : TopologicalSpace Z
inst_9 : Nonempty Z
f : X → X'
e : OpenPartialHomeomorph X Z
hf : IsOpenEmbedding f
h : Nonempty X
F : X' → Z := extend f (↑e : X → Z) fun (x : X') ↦ Classical.arbitrary Z
F_eq : F = extend f (↑e : X → Z) fun (x : X') ↦ Classical.arbitrary Z
heq : EqOn F ((↑e : X → Z) ∘ (↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm : X' → X)) (f '' e.source)
⊢ ContinuousOn F (f '' e.source)
have this : ContinuousOn ((↑e : X → Z) ∘ (↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm : X' → X)) (f '' e.source)
Tactic: have : ContinuousOn (e ∘ (hf.toOpenPartialHomeomorph).symm) (f '' e.source) := by
      apply e.continuousOn_toFun.comp; swap
      · intro x' ⟨x, hx, hx'x⟩
        rw [← hx'x, hf.toOpenPartialHomeomorph_left_inv]; exact hx
      have : ContinuousOn (hf.toOpenPartialHomeomorph).symm (f '' univ) :=
        (hf.toOpenPartialHomeomorph).continuousOn_invFun
      exact this.mono <| image_mono <| subset_univ _
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Constructions (goal)
Goal:
X : Type u_7
X' : Type u_8
Z : Type u_9
inst : TopologicalSpace X
inst_1 : TopologicalSpace X'
inst_2 : TopologicalSpace Z
inst_3 : Nonempty Z
f : X → X'
e : OpenPartialHomeomorph X Z
hf : IsOpenEmbedding f
x : X
⊢ (↑(e.lift_openEmbedding hf) : X' → Z) (f x) = (↑e : X → Z) x
have simp_rw : extend f (↑e : X → Z) (fun (x : X') ↦ Classical.arbitrary Z) (f x) = (↑e : X → Z) x
Tactic: simp_rw [e.lift_openEmbedding_toFun]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Constructions (goal)
Goal:
X : Type u_7
X' : Type u_8
Z : Type u_9
inst : TopologicalSpace X
inst_1 : TopologicalSpace X'
inst_2 : TopologicalSpace Z
inst_3 : Nonempty Z
f : X → X'
e : OpenPartialHomeomorph X Z
hf : IsOpenEmbedding f
⊢ (e.lift_openEmbedding hf).symm.target = f '' e.source
have rw : (e.lift_openEmbedding hf).source = f '' e.source
Tactic: rw [OpenPartialHomeomorph.symm_target, e.lift_openEmbedding_source]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Constructions (goal)
Goal:
X : Type u_7
X' : Type u_8
Z : Type u_9
inst : TopologicalSpace X
inst_1 : TopologicalSpace X'
inst_2 : TopologicalSpace Z
inst_3 : Nonempty Z
f : X → X'
e : OpenPartialHomeomorph X Z
hf : IsOpenEmbedding f
rw : (e.lift_openEmbedding hf).source = f '' e.source
⊢ (e.lift_openEmbedding hf).symm.target = f '' e.source
have rw₁ : f '' e.source = f '' e.source
Tactic: rw [OpenPartialHomeomorph.symm_target, e.lift_openEmbedding_source]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Constructions (goal)
Goal:
X : Type u_7
X' : Type u_8
Z : Type u_9
inst : TopologicalSpace X
inst_1 : TopologicalSpace X'
inst_2 : TopologicalSpace Z
inst_3 : Nonempty Z
f : X → X'
e e' : OpenPartialHomeomorph X Z
hf : IsOpenEmbedding f
⊢ (e.lift_openEmbedding hf).symm.trans (e'.lift_openEmbedding hf) = e.symm.trans e'
have h : ∀ (z : Z),
  (↑((e.lift_openEmbedding hf).symm.trans (e'.lift_openEmbedding hf)) : Z → Z) z = (↑(e.symm.trans e') : Z → Z) z
Tactic: ext z
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Constructions (goal)
Goal:
X : Type u_7
X' : Type u_8
Z : Type u_9
inst : TopologicalSpace X
inst_1 : TopologicalSpace X'
inst_2 : TopologicalSpace Z
inst_3 : Nonempty Z
f : X → X'
e e' : OpenPartialHomeomorph X Z
hf : IsOpenEmbedding f
h :
  ∀ (z : Z),
    (↑((e.lift_openEmbedding hf).symm.trans (e'.lift_openEmbedding hf)) : Z → Z) z = (↑(e.symm.trans e') : Z → Z) z
⊢ (e.lift_openEmbedding hf).symm.trans (e'.lift_openEmbedding hf) = e.symm.trans e'
have hinv : ∀ (z : Z),
  (↑((e.lift_openEmbedding hf).symm.trans (e'.lift_openEmbedding hf)).symm : Z → Z) z =
    (↑(e.symm.trans e').symm : Z → Z) z
Tactic: ext z
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Constructions (goal)
Goal:
X : Type u_7
X' : Type u_8
Z : Type u_9
inst : TopologicalSpace X
inst_1 : TopologicalSpace X'
inst_2 : TopologicalSpace Z
inst_3 : Nonempty Z
f : X → X'
e e' : OpenPartialHomeomorph X Z
hf : IsOpenEmbedding f
h :
  ∀ (z : Z),
    (↑((e.lift_openEmbedding hf).symm.trans (e'.lift_openEmbedding hf)) : Z → Z) z = (↑(e.symm.trans e') : Z → Z) z
hinv :
  ∀ (z : Z),
    (↑((e.lift_openEmbedding hf).symm.trans (e'.lift_openEmbedding hf)).symm : Z → Z) z =
      (↑(e.symm.trans e').symm : Z → Z) z
⊢ (e.lift_openEmbedding hf).symm.trans (e'.lift_openEmbedding hf) = e.symm.trans e'
have hs : ∀ (z : Z), z ∈ ((e.lift_openEmbedding hf).symm.trans (e'.lift_openEmbedding hf)).source ↔ z ∈ (e.symm.trans e').source
Tactic: ext z
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Constructions (goal)
Goal:
X : Type u_7
X' : Type u_8
Z : Type u_9
inst : TopologicalSpace X
inst_1 : TopologicalSpace X'
inst_2 : TopologicalSpace Z
inst_3 : Nonempty Z
f : X → X'
e e' : OpenPartialHomeomorph X Z
hf : IsOpenEmbedding f
z : Z
⊢ z ∈ ((e.lift_openEmbedding hf).symm.trans (e'.lift_openEmbedding hf)).source ↔ z ∈ (e.symm.trans e').source
have hs : z ∈ e.target ∩ f ∘ (↑e.symm : Z → X) ⁻¹' f '' e'.source ↔ z ∈ e.target ∩ (↑e.symm : Z → X) ⁻¹' e'.source
Tactic: simp_rw [OpenPartialHomeomorph.trans_source, e.lift_openEmbedding_symm_source, e.symm_source,
      e.lift_openEmbedding_symm, e'.lift_openEmbedding_source]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Constructions (goal)
Goal:
X : Type u_7
X' : Type u_8
Z : Type u_9
inst : TopologicalSpace X
inst_1 : TopologicalSpace X'
inst_2 : TopologicalSpace Z
inst_3 : Nonempty Z
f : X → X'
e e' : OpenPartialHomeomorph X Z
hf : IsOpenEmbedding f
z : Z
⊢ z ∈ e.target ∩ f ∘ (↑e.symm : Z → X) ⁻¹' f '' e'.source ↔ z ∈ e.target ∩ (↑e.symm : Z → X) ⁻¹' e'.source
have hs : z ∈ e.target ∩ f ∘ (↑e.symm : Z → X) ⁻¹' f '' e'.source →
  ∀ (hx : z ∈ e.target) (y : X) (hy : y ∈ e'.source) (hxy : f y = (f ∘ (↑e.symm : Z → X)) z),
    z ∈ (↑e.symm : Z → X) ⁻¹' e'.source
Tactic: refine ⟨fun ⟨hx, ⟨y, hy, hxy⟩⟩ ↦ ⟨hx, ?_⟩, fun ⟨hx, hx'⟩ ↦ ⟨hx, mem_image_of_mem f hx'⟩⟩
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Constructions (goal)
Goal:
X : Type u_7
X' : Type u_8
Z : Type u_9
inst : TopologicalSpace X
inst_1 : TopologicalSpace X'
inst_2 : TopologicalSpace Z
inst_3 : Nonempty Z
f : X → X'
e e' : OpenPartialHomeomorph X Z
hf : IsOpenEmbedding f
z : Z
h : z ∈ e.target ∩ f ∘ (↑e.symm : Z → X) ⁻¹' f '' e'.source
hx : z ∈ e.target
y : X
hy : y ∈ e'.source
hxy : f y = (f ∘ (↑e.symm : Z → X)) z
⊢ z ∈ (↑e.symm : Z → X) ⁻¹' e'.source
have hs : (↑e.symm : Z → X) z ∈ e'.source
Tactic: rw [mem_preimage]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Constructions (hypothesis)
Goal:
X : Type u_7
X' : Type u_8
Z : Type u_9
inst : TopologicalSpace X
inst_1 : TopologicalSpace X'
inst_2 : TopologicalSpace Z
inst_3 : Nonempty Z
f : X → X'
e e' : OpenPartialHomeomorph X Z
hf : IsOpenEmbedding f
z : Z
h : z ∈ e.target ∩ f ∘ (↑e.symm : Z → X) ⁻¹' f '' e'.source
hx : z ∈ e.target
y : X
hy : y ∈ e'.source
hxy : f y = (f ∘ (↑e.symm : Z → X)) z
⊢ (↑e.symm : Z → X) z ∈ e'.source
have hxy₁ : f y = f ((↑e.symm : Z → X) z)
Tactic: rw [comp_apply] at hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Continuity (goal)
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
x : X
hx : x ∈ e.source
x' : X
hx' : (↑e.symm : Y → X) ((↑e : X → Y) x') = x'
h : (↑e : X → Y) x' = (↑e : X → Y) x
⊢ Membership.mem (γ := Set X) {x} x'
have rw : x' = x
Tactic: rw [mem_singleton_iff, ← e.left_inv hx, ← h, hx']
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Continuity (goal)
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
x : X
hx : x ∈ e.source
x' : X
hx' : (↑e.symm : Y → X) ((↑e : X → Y) x') = x'
h : (↑e : X → Y) x' = (↑e : X → Y) x
rw : x' = x
⊢ Membership.mem (γ := Set X) {x} x'
have rw₁ : x' = (↑e.symm : Y → X) ((↑e : X → Y) x)
Tactic: rw [mem_singleton_iff, ← e.left_inv hx, ← h, hx']
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Continuity (goal)
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
x : X
hx : x ∈ e.source
x' : X
hx' : (↑e.symm : Y → X) ((↑e : X → Y) x') = x'
h : (↑e : X → Y) x' = (↑e : X → Y) x
rw : x' = x
rw₁ : x' = (↑e.symm : Y → X) ((↑e : X → Y) x)
⊢ Membership.mem (γ := Set X) {x} x'
have rw₂ : x' = (↑e.symm : Y → X) ((↑e : X → Y) x')
Tactic: rw [mem_singleton_iff, ← e.left_inv hx, ← h, hx']
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Continuity (goal)
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
x : X
hx : x ∈ e.source
x' : X
hx' : (↑e.symm : Y → X) ((↑e : X → Y) x') = x'
h : (↑e : X → Y) x' = (↑e : X → Y) x
rw : x' = x
rw₁ : x' = (↑e.symm : Y → X) ((↑e : X → Y) x)
rw₂ : x' = (↑e.symm : Y → X) ((↑e : X → Y) x')
⊢ Membership.mem (γ := Set X) {x} x'
have rw₃ : x' = x'
Tactic: rw [mem_singleton_iff, ← e.left_inv hx, ← h, hx']
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Continuity (goal)
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
x : X
hx : x ∈ e.source
⊢ 𝓝 ((↑e.symm : Y → X) ((↑e : X → Y) x)) = 𝓝 x
have rw : 𝓝 x = 𝓝 x
Tactic: rw [e.left_inv hx]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Continuity (goal)
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
x : X
hx : x ∈ e.source
s : Set Y
⊢ map (↑e : X → Y) (𝓝[(↑e : X → Y) ⁻¹' s] x) = 𝓝[s] (↑e : X → Y) x
have rw : 𝓝[(↑e : X → Y) '' (e.source ∩ (↑e : X → Y) ⁻¹' s)] (↑e : X → Y) x = 𝓝[s] (↑e : X → Y) x
Tactic: rw [e.map_nhdsWithin_eq hx, e.image_source_inter_eq', e.target_inter_inv_preimage_preimage,
    e.nhdsWithin_target_inter (e.map_source hx)]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Continuity (goal)
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
x : X
hx : x ∈ e.source
s : Set Y
rw : 𝓝[(↑e : X → Y) '' (e.source ∩ (↑e : X → Y) ⁻¹' s)] (↑e : X → Y) x = 𝓝[s] (↑e : X → Y) x
⊢ map (↑e : X → Y) (𝓝[(↑e : X → Y) ⁻¹' s] x) = 𝓝[s] (↑e : X → Y) x
have rw₁ : 𝓝[e.target ∩ (↑e.symm : Y → X) ⁻¹' (↑e : X → Y) ⁻¹' s] (↑e : X → Y) x = 𝓝[s] (↑e : X → Y) x
Tactic: rw [e.map_nhdsWithin_eq hx, e.image_source_inter_eq', e.target_inter_inv_preimage_preimage,
    e.nhdsWithin_target_inter (e.map_source hx)]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Continuity (goal)
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
x : X
hx : x ∈ e.source
s : Set Y
rw : 𝓝[(↑e : X → Y) '' (e.source ∩ (↑e : X → Y) ⁻¹' s)] (↑e : X → Y) x = 𝓝[s] (↑e : X → Y) x
rw₁ : 𝓝[e.target ∩ (↑e.symm : Y → X) ⁻¹' (↑e : X → Y) ⁻¹' s] (↑e : X → Y) x = 𝓝[s] (↑e : X → Y) x
⊢ map (↑e : X → Y) (𝓝[(↑e : X → Y) ⁻¹' s] x) = 𝓝[s] (↑e : X → Y) x
have rw₂ : 𝓝[e.target ∩ s] (↑e : X → Y) x = 𝓝[s] (↑e : X → Y) x
Tactic: rw [e.map_nhdsWithin_eq hx, e.image_source_inter_eq', e.target_inter_inv_preimage_preimage,
    e.nhdsWithin_target_inter (e.map_source hx)]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Continuity (goal)
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
x : X
hx : x ∈ e.source
s : Set Y
rw : 𝓝[(↑e : X → Y) '' (e.source ∩ (↑e : X → Y) ⁻¹' s)] (↑e : X → Y) x = 𝓝[s] (↑e : X → Y) x
rw₁ : 𝓝[e.target ∩ (↑e.symm : Y → X) ⁻¹' (↑e : X → Y) ⁻¹' s] (↑e : X → Y) x = 𝓝[s] (↑e : X → Y) x
rw₂ : 𝓝[e.target ∩ s] (↑e : X → Y) x = 𝓝[s] (↑e : X → Y) x
⊢ map (↑e : X → Y) (𝓝[(↑e : X → Y) ⁻¹' s] x) = 𝓝[s] (↑e : X → Y) x
have rw₃ : 𝓝[s] (↑e : X → Y) x = 𝓝[s] (↑e : X → Y) x
Tactic: rw [e.map_nhdsWithin_eq hx, e.image_source_inter_eq', e.target_inter_inv_preimage_preimage,
    e.nhdsWithin_target_inter (e.map_source hx)]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Continuity (goal)
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
x : X
p : Y → Prop
hx : x ∈ e.source
⊢ (∀ᶠ (y : Y) in 𝓝 ((↑e : X → Y) x), p y) ↔ ∀ᶠ (b : Y) in map (↑e : X → Y) (𝓝 x), p b
have rw : (∀ᶠ (y : Y) in 𝓝 ((↑e : X → Y) x), p y) ↔ ∀ᶠ (b : Y) in 𝓝 ((↑e : X → Y) x), p b
Tactic: rw [e.map_nhds_eq hx]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Continuity (goal)
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
x : X
p : X → Prop
hx : x ∈ e.source
⊢ (∀ᶠ (y : Y) in 𝓝 ((↑e : X → Y) x), p ((↑e.symm : Y → X) y)) ↔ ∀ᶠ (x : X) in 𝓝 x, p x
have rw : (∀ᶠ (x : X) in 𝓝 x, p ((↑e.symm : Y → X) ((↑e : X → Y) x))) ↔ ∀ᶠ (x : X) in 𝓝 x, p x
Tactic: rw [e.eventually_nhds _ hx]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Continuity (goal)
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
x : X
p : X → Prop
hx : x ∈ e.source
⊢ (∀ᶠ (x : X) in 𝓝 x, p ((↑e.symm : Y → X) ((↑e : X → Y) x))) ↔ ∀ᶠ (x : X) in 𝓝 x, p x
have refine : ∀ (y : X) (hy : (↑e.symm : Y → X) ((↑e : X → Y) y) = y), p ((↑e.symm : Y → X) ((↑e : X → Y) y)) ↔ p y
Tactic: refine eventually_congr ((e.eventually_left_inverse hx).mono fun y hy => ?_)
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Continuity (goal)
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
x : X
p : X → Prop
hx : x ∈ e.source
y : X
hy : (↑e.symm : Y → X) ((↑e : X → Y) y) = y
⊢ p ((↑e.symm : Y → X) ((↑e : X → Y) y)) ↔ p y
have rw : p y ↔ p y
Tactic: rw [hy]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Continuity (goal)
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
x : X
p : Y → Prop
s : Set X
hx : x ∈ e.source
⊢ (∀ᶠ (y : Y) in 𝓝[(↑e.symm : Y → X) ⁻¹' s] (↑e : X → Y) x, p y) ↔ ∀ᶠ (x : X) in 𝓝[s] x, p ((↑e : X → Y) x)
have refine : (∀ᶠ (y : Y) in 𝓝[(↑e.symm : Y → X) ⁻¹' s] (↑e : X → Y) x, p y) ↔ ∀ᶠ (b : Y) in map (↑e : X → Y) (𝓝[s] x), p b
Tactic: refine Iff.trans ?_ eventually_map
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Continuity (goal)
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
x : X
p : Y → Prop
s : Set X
hx : x ∈ e.source
⊢ (∀ᶠ (y : Y) in 𝓝[(↑e.symm : Y → X) ⁻¹' s] (↑e : X → Y) x, p y) ↔ ∀ᶠ (b : Y) in map (↑e : X → Y) (𝓝[s] x), p b
have rw : (∀ᶠ (y : Y) in 𝓝[(↑e.symm : Y → X) ⁻¹' s] (↑e : X → Y) x, p y) ↔
  ∀ᶠ (b : Y) in 𝓝[(↑e : X → Y) '' (e.source ∩ s)] (↑e : X → Y) x, p b
Tactic: rw [e.map_nhdsWithin_eq hx, e.image_source_inter_eq', e.nhdsWithin_target_inter (e.mapsTo hx)]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Continuity (goal)
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
x : X
p : Y → Prop
s : Set X
hx : x ∈ e.source
rw :
  (∀ᶠ (y : Y) in 𝓝[(↑e.symm : Y → X) ⁻¹' s] (↑e : X → Y) x, p y) ↔
    ∀ᶠ (b : Y) in 𝓝[(↑e : X → Y) '' (e.source ∩ s)] (↑e : X → Y) x, p b
⊢ (∀ᶠ (y : Y) in 𝓝[(↑e.symm : Y → X) ⁻¹' s] (↑e : X → Y) x, p y) ↔ ∀ᶠ (b : Y) in map (↑e : X → Y) (𝓝[s] x), p b
have rw₁ : (∀ᶠ (y : Y) in 𝓝[(↑e.symm : Y → X) ⁻¹' s] (↑e : X → Y) x, p y) ↔
  ∀ᶠ (b : Y) in 𝓝[e.target ∩ (↑e.symm : Y → X) ⁻¹' s] (↑e : X → Y) x, p b
Tactic: rw [e.map_nhdsWithin_eq hx, e.image_source_inter_eq', e.nhdsWithin_target_inter (e.mapsTo hx)]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Continuity (goal)
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
x : X
p : Y → Prop
s : Set X
hx : x ∈ e.source
rw :
  (∀ᶠ (y : Y) in 𝓝[(↑e.symm : Y → X) ⁻¹' s] (↑e : X → Y) x, p y) ↔
    ∀ᶠ (b : Y) in 𝓝[(↑e : X → Y) '' (e.source ∩ s)] (↑e : X → Y) x, p b
rw₁ :
  (∀ᶠ (y : Y) in 𝓝[(↑e.symm : Y → X) ⁻¹' s] (↑e : X → Y) x, p y) ↔
    ∀ᶠ (b : Y) in 𝓝[e.target ∩ (↑e.symm : Y → X) ⁻¹' s] (↑e : X → Y) x, p b
⊢ (∀ᶠ (y : Y) in 𝓝[(↑e.symm : Y → X) ⁻¹' s] (↑e : X → Y) x, p y) ↔ ∀ᶠ (b : Y) in map (↑e : X → Y) (𝓝[s] x), p b
have rw₂ : (∀ᶠ (y : Y) in 𝓝[(↑e.symm : Y → X) ⁻¹' s] (↑e : X → Y) x, p y) ↔
  ∀ᶠ (b : Y) in 𝓝[(↑e.symm : Y → X) ⁻¹' s] (↑e : X → Y) x, p b
Tactic: rw [e.map_nhdsWithin_eq hx, e.image_source_inter_eq', e.nhdsWithin_target_inter (e.mapsTo hx)]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Continuity (goal)
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
x : X
p : X → Prop
s : Set X
hx : x ∈ e.source
⊢ (∀ᶠ (y : Y) in 𝓝[(↑e.symm : Y → X) ⁻¹' s] (↑e : X → Y) x, p ((↑e.symm : Y → X) y)) ↔ ∀ᶠ (x : X) in 𝓝[s] x, p x
have rw : (∀ᶠ (x : X) in 𝓝[s] x, p ((↑e.symm : Y → X) ((↑e : X → Y) x))) ↔ ∀ᶠ (x : X) in 𝓝[s] x, p x
Tactic: rw [e.eventually_nhdsWithin _ hx]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Continuity (goal)
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
x : X
p : X → Prop
s : Set X
hx : x ∈ e.source
⊢ (∀ᶠ (x : X) in 𝓝[s] x, p ((↑e.symm : Y → X) ((↑e : X → Y) x))) ↔ ∀ᶠ (x : X) in 𝓝[s] x, p x
have refine : ∀ (y : X) (hy : (↑e.symm : Y → X) ((↑e : X → Y) y) = y), p ((↑e.symm : Y → X) ((↑e : X → Y) y)) ↔ p y
Tactic: refine eventually_congr <|
    (eventually_nhdsWithin_of_eventually_nhds <| e.eventually_left_inverse hx).mono fun y hy => ?_
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Continuity (goal)
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
x : X
p : X → Prop
s : Set X
hx : x ∈ e.source
y : X
hy : (↑e.symm : Y → X) ((↑e : X → Y) y) = y
⊢ p ((↑e.symm : Y → X) ((↑e : X → Y) y)) ↔ p y
have rw : p y ↔ p y
Tactic: rw [hy]