awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions
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 : Z → X') = f ∘ (↑e.symm : Z → X)

Tactic:
rfl

Premises used: OpenPartialHomeomorph.toFun', rfl
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions
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.source = e.target

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions
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
rw₁ rw₂ : f '' e.source = f '' e.source
⊢ (e.lift_openEmbedding hf).symm.target = f '' e.source

Tactic:
rw [OpenPartialHomeomorph.symm_target, e.lift_openEmbedding_source]

Premises used: OpenPartialHomeomorph.lift_openEmbedding_source, OpenPartialHomeomorph.symm_target
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions
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
⊢ (↑((e.lift_openEmbedding hf).symm.trans (e'.lift_openEmbedding hf)) : Z → Z) z = (↑(e.symm.trans e') : Z → Z) z

Tactic:
simp [hf.injective.extend_apply e']

Premises used: Topology.IsOpenEmbedding.toIsEmbedding, OpenPartialHomeomorph.toFun', Function.Injective.extend_apply, Topology.IsEmbedding.injective
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions
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
hs :
  ∀ (z : Z), z ∈ ((e.lift_openEmbedding hf).symm.trans (e'.lift_openEmbedding hf)).source ↔ z ∈ (e.symm.trans e').source
⊢ (e.lift_openEmbedding hf).symm.trans (e'.lift_openEmbedding hf) = e.symm.trans e'

Tactic:
ext z
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions
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
⊢ (↑((e.lift_openEmbedding hf).symm.trans (e'.lift_openEmbedding hf)) : Z → Z) z = (↑(e.symm.trans e') : Z → Z) z

Tactic:
e.lift_openEmbedding_trans_apply e' hf z

Premises used: OpenPartialHomeomorph.lift_openEmbedding_trans_apply
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions
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
⊢ (↑((e.lift_openEmbedding hf).symm.trans (e'.lift_openEmbedding hf)) : Z → Z) z = (↑(e.symm.trans e') : Z → Z) z

Tactic:
exact e.lift_openEmbedding_trans_apply e' hf z

Premises used: OpenPartialHomeomorph.lift_openEmbedding_trans_apply
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions
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
⊢ (↑((e.lift_openEmbedding hf).symm.trans (e'.lift_openEmbedding hf)).symm : Z → Z) z =
    (↑(e.symm.trans e').symm : Z → Z) z

Tactic:
simp [hf.injective.extend_apply e]

Premises used: Topology.IsOpenEmbedding.toIsEmbedding, OpenPartialHomeomorph.toFun', Function.Injective.extend_apply, Topology.IsEmbedding.injective
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions
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
hs : z ∈ e.target ∩ f ∘ (↑e.symm : Z → X) ⁻¹' f '' e'.source ↔ z ∈ e.target ∩ (↑e.symm : Z → X) ⁻¹' e'.source
⊢ z ∈ ((e.lift_openEmbedding hf).symm.trans (e'.lift_openEmbedding hf)).source ↔ z ∈ (e.symm.trans e').source

Tactic:
simp_rw [OpenPartialHomeomorph.trans_source, e.lift_openEmbedding_symm_source, e.symm_source,
      e.lift_openEmbedding_symm, e'.lift_openEmbedding_source]

Premises used: OpenPartialHomeomorph.lift_openEmbedding_source, OpenPartialHomeomorph.lift_openEmbedding_symm, OpenPartialHomeomorph.trans_source, OpenPartialHomeomorph.symm_source, OpenPartialHomeomorph.lift_openEmbedding_symm_source
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions
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

Tactic:
⟨fun ⟨hx, ⟨y, hy, hxy⟩⟩ ↦ ⟨hx, ?_⟩, fun ⟨hx, hx'⟩ ↦ ⟨hx, mem_image_of_mem f hx'⟩⟩

Premises used: PartialEquiv.target, Function.comp, Membership.mem, OpenPartialHomeomorph.toFun', Inter.inter, Set.preimage, Set.mem_image_of_mem, And.intro, Iff.intro, _private.0.OpenPartialHomeomorph.lift_openEmbedding_trans.match_1, PartialEquiv.source, _private.0.OpenPartialHomeomorph.lift_openEmbedding_trans.match_2, Set.image, OpenPartialHomeomorph.toPartialEquiv, OpenPartialHomeomorph.symm
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions
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
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
⊢ z ∈ e.target ∩ f ∘ (↑e.symm : Z → X) ⁻¹' f '' e'.source ↔ z ∈ e.target ∩ (↑e.symm : Z → X) ⁻¹' e'.source

Tactic:
refine ⟨fun ⟨hx, ⟨y, hy, hxy⟩⟩ ↦ ⟨hx, ?_⟩, fun ⟨hx, hx'⟩ ↦ ⟨hx, mem_image_of_mem f hx'⟩⟩
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions
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
hs : (↑e.symm : Z → X) z ∈ e'.source
⊢ z ∈ (↑e.symm : Z → X) ⁻¹' e'.source

Tactic:
rw [mem_preimage]

Premises used: Set.mem_preimage
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions
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
⊢ f y = f ((↑e.symm : Z → X) z)

Tactic:
rw [comp_apply] at hxy

Premises used: Function.comp_apply
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions
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

Tactic:
(hf.injective hxy) ▸ hy

Premises used: Topology.IsOpenEmbedding.toIsEmbedding, Eq.rec, Topology.IsEmbedding.injective
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions
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

Tactic:
exact (hf.injective hxy) ▸ hy
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Continuity
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
⊢ ∀ᶠ (y : X) in 𝓝 x, (↑e.symm : Y → X) ((↑e : X → Y) y) = y

Tactic:
(e.open_source.eventually_mem hx).mono e.left_inv'

Premises used: OpenPartialHomeomorph.open_source, IsOpen.eventually_mem, Filter.Eventually.mono, PartialEquiv.left_inv', OpenPartialHomeomorph.toPartialEquiv
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Continuity
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
x : Y
hx : x ∈ e.target
⊢ ∀ᶠ (y : X) in 𝓝 ((↑e.symm : Y → X) x), (↑e.symm : Y → X) ((↑e : X → Y) y) = y

Tactic:
e.eventually_left_inverse (e.map_target hx)

Premises used: OpenPartialHomeomorph.eventually_left_inverse, OpenPartialHomeomorph.map_target
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Continuity
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
x : Y
hx : x ∈ e.target
⊢ ∀ᶠ (y : Y) in 𝓝 x, (↑e : X → Y) ((↑e.symm : Y → X) y) = y

Tactic:
(e.open_target.eventually_mem hx).mono e.right_inv'

Premises used: PartialEquiv.right_inv', IsOpen.eventually_mem, Filter.Eventually.mono, OpenPartialHomeomorph.open_target, OpenPartialHomeomorph.toPartialEquiv
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Continuity
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
⊢ ∀ᶠ (y : Y) in 𝓝 ((↑e : X → Y) x), (↑e : X → Y) ((↑e.symm : Y → X) y) = y

Tactic:
e.eventually_right_inverse (e.map_source hx)

Premises used: OpenPartialHomeomorph.eventually_right_inverse, OpenPartialHomeomorph.map_source
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Continuity
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')
rw₃ rw₄ : x' = x'
⊢ Membership.mem (γ := Set X) {x} x'

Tactic:
rw [mem_singleton_iff, ← e.left_inv hx, ← h, hx']

Premises used: OpenPartialHomeomorph.left_inv, Set.mem_singleton_iff
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Continuity
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 X
⊢ 𝓝[e.source ∩ s] x = 𝓝[s] x

Tactic:
nhdsWithin_inter_of_mem (mem_nhdsWithin_of_mem_nhds <| IsOpen.mem_nhds e.open_source hx)

Premises used: OpenPartialHomeomorph.open_source, nhdsWithin_inter_of_mem, mem_nhdsWithin_of_mem_nhds, IsOpen.mem_nhds
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Continuity
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
x : Y
hx : x ∈ e.target
s : Set Y
⊢ 𝓝[e.target ∩ s] x = 𝓝[s] x

Tactic:
e.symm.nhdsWithin_source_inter hx s

Premises used: OpenPartialHomeomorph.nhdsWithin_source_inter, OpenPartialHomeomorph.symm
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Continuity
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
x : X
h : x ∈ e.source
⊢ ContinuousAt (↑e : X → Y) x

Tactic:
(e.continuousOn x h).continuousAt (e.open_source.mem_nhds h)

Premises used: OpenPartialHomeomorph.open_source, OpenPartialHomeomorph.continuousOn, IsOpen.mem_nhds, ContinuousWithinAt.continuousAt
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Continuity
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
x : Y
h : x ∈ e.target
⊢ ContinuousAt (↑e.symm : Y → X) x

Tactic:
e.symm.continuousAt h

Premises used: OpenPartialHomeomorph.continuousAt, OpenPartialHomeomorph.symm
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Continuity
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
⊢ Tendsto (↑e.symm : Y → X) (𝓝 ((↑e : X → Y) x)) (𝓝 x)

Tactic:
simpa only [ContinuousAt, e.left_inv hx] using e.continuousAt_symm (e.map_source hx)

Premises used: ContinuousAt, OpenPartialHomeomorph.left_inv, OpenPartialHomeomorph.map_source, OpenPartialHomeomorph.continuousAt_symm
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Continuity
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
⊢ map (↑e : X → Y) (𝓝 x) = 𝓝 ((↑e : X → Y) x)

Tactic:
le_antisymm (e.continuousAt hx) <|
    le_map_of_right_inverse (e.eventually_right_inverse' hx) (e.tendsto_symm hx)

Premises used: Filter.le_map_of_right_inverse, OpenPartialHomeomorph.continuousAt, le_antisymm, OpenPartialHomeomorph.eventually_right_inverse', OpenPartialHomeomorph.tendsto_symm
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Continuity
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
rw rw₁ : 𝓝 x = 𝓝 x
⊢ 𝓝 ((↑e.symm : Y → X) ((↑e : X → Y) x)) = 𝓝 x

Tactic:
rw [e.left_inv hx]

Premises used: OpenPartialHomeomorph.left_inv
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Continuity
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 X
hs : s ∈ 𝓝 x
⊢ (↑e : X → Y) '' s ∈ 𝓝 ((↑e : X → Y) x)

Tactic:
e.map_nhds_eq hx ▸ Filter.image_mem_map hs

Premises used: Eq.rec, Filter.image_mem_map, OpenPartialHomeomorph.map_nhds_eq
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Continuity
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 X
⊢ map (↑e : X → Y) (𝓝[s] x) = 𝓝[(↑e : X → Y) '' (e.source ∩ s)] (↑e : X → Y) x

Tactic:
calc
    map e (𝓝[s] x) = map e (𝓝[e.source ∩ s] x) :=
      congr_arg (map e) (e.nhdsWithin_source_inter hx _).symm
    _ = 𝓝[e '' (e.source ∩ s)] e x :=
      (e.leftInvOn.mono inter_subset_left).map_nhdsWithin_eq (e.left_inv hx)
        (e.continuousAt_symm (e.map_source hx)).continuousWithinAt
        (e.continuousAt hx).continuousWithinAt

Premises used: OpenPartialHomeomorph.continuousAt, Trans.trans, Filter.map, ContinuousAt.continuousWithinAt, Set.LeftInvOn.map_nhdsWithin_eq, OpenPartialHomeomorph.leftInvOn, OpenPartialHomeomorph.left_inv, Set.inter_subset_left, OpenPartialHomeomorph.toFun', Set.LeftInvOn.mono, congr_arg, OpenPartialHomeomorph.map_source, OpenPartialHomeomorph.nhdsWithin_source_inter, OpenPartialHomeomorph.continuousAt_symm, Eq.symm
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Continuity
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
rw₃ rw₄ : 𝓝[s] (↑e : X → Y) x = 𝓝[s] (↑e : X → Y) x
⊢ map (↑e : X → Y) (𝓝[(↑e : X → Y) ⁻¹' s] 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)]

Premises used: OpenPartialHomeomorph.map_nhdsWithin_eq, OpenPartialHomeomorph.target_inter_inv_preimage_preimage, OpenPartialHomeomorph.nhdsWithin_target_inter, OpenPartialHomeomorph.image_source_inter_eq', OpenPartialHomeomorph.map_source
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Continuity
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
rw rw₁ : (∀ᶠ (y : Y) in 𝓝 ((↑e : X → Y) x), p y) ↔ ∀ᶠ (b : Y) in 𝓝 ((↑e : X → Y) x), p b
⊢ (∀ᶠ (y : Y) in 𝓝 ((↑e : X → Y) x), p y) ↔ ∀ᶠ (b : Y) in map (↑e : X → Y) (𝓝 x), p b

Tactic:
rw [e.map_nhds_eq hx]

Premises used: OpenPartialHomeomorph.map_nhds_eq
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Continuity
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
rw : (∀ᶠ (x : X) in 𝓝 x, p ((↑e.symm : Y → X) ((↑e : X → Y) x))) ↔ ∀ᶠ (x : X) in 𝓝 x, p x
⊢ (∀ᶠ (y : Y) in 𝓝 ((↑e : X → Y) x), p ((↑e.symm : Y → X) y)) ↔ ∀ᶠ (x : X) in 𝓝 x, p x

Tactic:
rw [e.eventually_nhds _ hx]

Premises used: OpenPartialHomeomorph.eventually_nhds
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Continuity
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

Tactic:
eventually_congr ((e.eventually_left_inverse hx).mono fun y hy => ?_)

Premises used: OpenPartialHomeomorph.eventually_left_inverse, Filter.Eventually.mono, Filter.eventually_congr
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Continuity
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
refine : ∀ (y : X) (hy : (↑e.symm : Y → X) ((↑e : X → Y) y) = y), p ((↑e.symm : Y → X) ((↑e : X → Y) y)) ↔ p y
⊢ (∀ᶠ (x : X) in 𝓝 x, p ((↑e.symm : Y → X) ((↑e : X → Y) x))) ↔ ∀ᶠ (x : X) in 𝓝 x, p x

Tactic:
refine eventually_congr ((e.eventually_left_inverse hx).mono fun y hy => ?_)

Premises used: OpenPartialHomeomorph.eventually_left_inverse, Filter.Eventually.mono, Filter.eventually_congr
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Continuity
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
rw rw₁ : p y ↔ p y
⊢ p ((↑e.symm : Y → X) ((↑e : X → Y) y)) ↔ p y

Tactic:
rw [hy]
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Continuity
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)

Tactic:
Iff.trans ?_ eventually_map

Premises used: Filter.eventually_map, Iff.trans
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Continuity
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
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
⊢ (∀ᶠ (y : Y) in 𝓝[(↑e.symm : Y → X) ⁻¹' s] (↑e : X → Y) x, p y) ↔ ∀ᶠ (x : X) in 𝓝[s] x, p ((↑e : X → Y) x)

Tactic:
refine Iff.trans ?_ eventually_map

Premises used: Filter.eventually_map, Iff.trans
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Continuity
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
rw₂ 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
⊢ (∀ᶠ (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:
rw [e.map_nhdsWithin_eq hx, e.image_source_inter_eq', e.nhdsWithin_target_inter (e.mapsTo hx)]

Premises used: OpenPartialHomeomorph.map_nhdsWithin_eq, OpenPartialHomeomorph.nhdsWithin_target_inter, OpenPartialHomeomorph.image_source_inter_eq', OpenPartialHomeomorph.mapsTo
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Continuity
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
rw : (∀ᶠ (x : X) in 𝓝[s] x, p ((↑e.symm : Y → X) ((↑e : X → Y) x))) ↔ ∀ᶠ (x : X) in 𝓝[s] x, p x
⊢ (∀ᶠ (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

Tactic:
rw [e.eventually_nhdsWithin _ hx]

Premises used: OpenPartialHomeomorph.eventually_nhdsWithin
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Continuity
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

Tactic:
eventually_congr <|
    (eventually_nhdsWithin_of_eventually_nhds <| e.eventually_left_inverse hx).mono fun y hy => ?_

Premises used: OpenPartialHomeomorph.eventually_left_inverse, eventually_nhdsWithin_of_eventually_nhds, Filter.Eventually.mono, Filter.eventually_congr
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Continuity
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
refine : ∀ (y : X) (hy : (↑e.symm : Y → X) ((↑e : X → Y) y) = y), p ((↑e.symm : Y → X) ((↑e : X → Y) y)) ↔ p y
⊢ (∀ᶠ (x : X) in 𝓝[s] x, p ((↑e.symm : Y → X) ((↑e : X → Y) x))) ↔ ∀ᶠ (x : X) in 𝓝[s] x, p x

Tactic:
refine eventually_congr <|
    (eventually_nhdsWithin_of_eventually_nhds <| e.eventually_left_inverse hx).mono fun y hy => ?_

Premises used: OpenPartialHomeomorph.eventually_left_inverse, eventually_nhdsWithin_of_eventually_nhds, Filter.Eventually.mono, Filter.eventually_congr
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Continuity
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
rw rw₁ : p y ↔ p y
⊢ p ((↑e.symm : Y → X) ((↑e : X → Y) y)) ↔ p y

Tactic:
rw [hy]
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Continuity
Goal:
X : Type u_1
Y : Type u_3
Z : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
e : OpenPartialHomeomorph X Y
s : Set X
t : Set Z
x : X
f : X → Z
hf : ContinuousWithinAt f s x
hxe : x ∈ e.source
ht : t ∈ 𝓝 (f x)
rw :
  ∀ᶠ (x : X) in 𝓝 x,
    (↑e : X → Y) x ∈ (↑e.symm : Y → X) ⁻¹' s ↔ (↑e : X → Y) x ∈ e.target ∩ (↑e.symm : Y → X) ⁻¹' (s ∩ f ⁻¹' t)
⊢ (↑e.symm : Y → X) ⁻¹' s =ᶠ[𝓝 ((↑e : X → Y) x)] e.target ∩ (↑e.symm : Y → X) ⁻¹' (s ∩ f ⁻¹' t)

Tactic:
rw [eventuallyEq_set, e.eventually_nhds _ hxe]

Premises used: Filter.eventuallyEq_set, OpenPartialHomeomorph.eventually_nhds