awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
h :
  ∀ a ∈ e.source,
    (a ∈ s → a ∈ f ⁻¹' t) →
      ((↑e : X → Y) a ∈ (↑e.symm : Y → X) ⁻¹' s ↔ (↑e : X → Y) a ∈ e.target ∩ (↑e.symm : Y → X) ⁻¹' (s ∩ f ⁻¹' t))
⊢ ∀ᶠ (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)

Tactic:
filter_upwards [e.open_source.mem_nhds hxe,
    mem_nhdsWithin_iff_eventually.mp (hf.preimage_mem_nhdsWithin ht)]

Premises used: OpenPartialHomeomorph.open_source, mem_nhdsWithin_iff_eventually, ContinuousWithinAt.preimage_mem_nhdsWithin, IsOpen.mem_nhds, Iff.mp
-- 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)
y : X
hy : y ∈ e.source
hyu : y ∈ s → y ∈ f ⁻¹' t
h :
  (↑e : X → Y) y ∈ (↑e.symm : Y → X) ⁻¹' s ↔
    (↑e : X → Y) y ∈ e.target ∧ (↑e : X → Y) y ∈ (↑e.symm : Y → X) ⁻¹' (s ∩ f ⁻¹' t)
h₁ :
  (↑e.symm : Y → X) ((↑e : X → Y) y) ∈ s ↔ (↑e : X → Y) y ∈ e.target ∧ (↑e.symm : Y → X) ((↑e : X → Y) y) ∈ s ∩ f ⁻¹' t
h₂ :
  (↑e.symm : Y → X) ((↑e : X → Y) y) ∈ s ↔
    (↑e : X → Y) y ∈ e.target ∧ (↑e.symm : Y → X) ((↑e : X → Y) y) ∈ s ∧ (↑e.symm : Y → X) ((↑e : X → Y) y) ∈ f ⁻¹' t
h₃ :
  (↑e.symm : Y → X) ((↑e : X → Y) y) ∈ s ↔
    True ∧ (↑e.symm : Y → X) ((↑e : X → Y) y) ∈ s ∧ (↑e.symm : Y → X) ((↑e : X → Y) y) ∈ f ⁻¹' t
h₄ :
  (↑e.symm : Y → X) ((↑e : X → Y) y) ∈ s ↔
    (↑e.symm : Y → X) ((↑e : X → Y) y) ∈ s ∧ (↑e.symm : Y → X) ((↑e : X → Y) y) ∈ f ⁻¹' t
h₅ : (↑e.symm : Y → X) ((↑e : X → Y) y) ∈ s → (↑e.symm : Y → X) ((↑e : X → Y) y) ∈ f ⁻¹' t
h₆ : y ∈ s → y ∈ f ⁻¹' t
⊢ (↑e : X → Y) y ∈ (↑e.symm : Y → X) ⁻¹' s ↔ (↑e : X → Y) y ∈ e.target ∩ (↑e.symm : Y → X) ⁻¹' (s ∩ f ⁻¹' t)

Tactic:
simp_rw [mem_inter_iff, mem_preimage, mem_inter_iff, e.mapsTo hy, true_and, iff_self_and,
    e.left_inv hy, iff_true_intro hyu]

Premises used: Set.mem_inter_iff, iff_self_and, OpenPartialHomeomorph.left_inv, iff_true_intro, OpenPartialHomeomorph.mapsTo, Set.mem_preimage, true_and
-- 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
f : Y → Z
s : Set Y
x : Y
h : x ∈ e.target
simp_rw :
  Tendsto f (𝓝[s] x) (𝓝 (f x)) ↔
    Tendsto (f ∘ (↑e : X → Y)) (𝓝[(↑e : X → Y) ⁻¹' s] (↑e.symm : Y → X) x)
      (𝓝 ((f ∘ (↑e : X → Y)) ((↑e.symm : Y → X) x)))
simp_rw₁ :
  Tendsto f (𝓝[s] x) (𝓝 (f x)) ↔
    Tendsto f (map (↑e : X → Y) (𝓝[(↑e : X → Y) ⁻¹' s] (↑e.symm : Y → X) x))
      (𝓝 ((f ∘ (↑e : X → Y)) ((↑e.symm : Y → X) x)))
simp_rw₂ :
  Tendsto f (𝓝[s] x) (𝓝 (f x)) ↔
    Tendsto f (𝓝[s] (↑e : X → Y) ((↑e.symm : Y → X) x)) (𝓝 ((f ∘ (↑e : X → Y)) ((↑e.symm : Y → X) x)))
simp_rw₃ :
  Tendsto f (𝓝[s] x) (𝓝 (f x)) ↔
    Tendsto f (𝓝[s] (↑e : X → Y) ((↑e.symm : Y → X) x)) (𝓝 (f ((↑e : X → Y) ((↑e.symm : Y → X) x))))
⊢ ContinuousWithinAt f s x ↔ ContinuousWithinAt (f ∘ (↑e : X → Y)) ((↑e : X → Y) ⁻¹' s) ((↑e.symm : Y → X) x)

Tactic:
simp_rw [ContinuousWithinAt, ← @tendsto_map'_iff _ _ _ _ e,
    e.map_nhdsWithin_preimage_eq (e.map_target h), (· ∘ ·), e.right_inv h]

Premises used: ContinuousWithinAt, Filter.tendsto_map'_iff, Function.comp, OpenPartialHomeomorph.map_nhdsWithin_preimage_eq, OpenPartialHomeomorph.map_target, OpenPartialHomeomorph.right_inv
-- 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
f : Y → Z
x : Y
h : x ∈ e.target
rw : ContinuousWithinAt f univ x ↔ ContinuousAt (f ∘ (↑e : X → Y)) ((↑e.symm : Y → X) x)
rw₁ :
  ContinuousWithinAt (f ∘ (↑e : X → Y)) ((↑e : X → Y) ⁻¹' univ) ((↑e.symm : Y → X) x) ↔
    ContinuousAt (f ∘ (↑e : X → Y)) ((↑e.symm : Y → X) x)
rw₂ :
  ContinuousWithinAt (f ∘ (↑e : X → Y)) univ ((↑e.symm : Y → X) x) ↔
    ContinuousAt (f ∘ (↑e : X → Y)) ((↑e.symm : Y → X) x)
rw₃ rw₄ : ContinuousAt (f ∘ (↑e : X → Y)) ((↑e.symm : Y → X) x) ↔ ContinuousAt (f ∘ (↑e : X → Y)) ((↑e.symm : Y → X) x)
⊢ ContinuousAt f x ↔ ContinuousAt (f ∘ (↑e : X → Y)) ((↑e.symm : Y → X) x)

Tactic:
rw [← continuousWithinAt_univ, e.continuousWithinAt_iff_continuousWithinAt_comp_right h,
    preimage_univ, continuousWithinAt_univ]

Premises used: continuousWithinAt_univ, OpenPartialHomeomorph.continuousWithinAt_iff_continuousWithinAt_comp_right, Set.preimage_univ
-- 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
f : Y → Z
s : Set Y
h : s ⊆ e.target
simp :
  (∀ x ∈ s, ContinuousWithinAt f s x) ↔
    ∀ ⦃x : Y⦄, x ∈ s → ContinuousWithinAt (f ∘ (↑e : X → Y)) ((↑e.symm : Y → X) '' s) ((↑e.symm : Y → X) x)
⊢ ContinuousOn f s ↔ ContinuousOn (f ∘ (↑e : X → Y)) (e.source ∩ (↑e : X → Y) ⁻¹' s)

Tactic:
simp only [← e.symm_image_eq_source_inter_preimage h, ContinuousOn, forall_mem_image]

Premises used: OpenPartialHomeomorph.symm_image_eq_source_inter_preimage, ContinuousOn, Set.forall_mem_image
-- 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
f : Y → Z
s : Set Y
h : s ⊆ e.target
⊢ (∀ x ∈ s, ContinuousWithinAt f s x) ↔
    ∀ ⦃x : Y⦄, x ∈ s → ContinuousWithinAt (f ∘ (↑e : X → Y)) ((↑e.symm : Y → X) '' s) ((↑e.symm : Y → X) x)

Tactic:
forall₂_congr fun x hx => ?_

Premises used: forall₂_congr
-- 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
f : Y → Z
s : Set Y
h : s ⊆ e.target
refine :
  ∀ (x : Y) (hx : x ∈ s),
    ContinuousWithinAt f s x ↔ ContinuousWithinAt (f ∘ (↑e : X → Y)) ((↑e.symm : Y → X) '' s) ((↑e.symm : Y → X) x)
⊢ (∀ x ∈ s, ContinuousWithinAt f s x) ↔
    ∀ ⦃x : Y⦄, x ∈ s → ContinuousWithinAt (f ∘ (↑e : X → Y)) ((↑e.symm : Y → X) '' s) ((↑e.symm : Y → X) x)

Tactic:
refine forall₂_congr fun x hx => ?_

Premises used: forall₂_congr
-- 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
f : Y → Z
s : Set Y
h : s ⊆ e.target
x : Y
hx : x ∈ s
rw : e.source ∈ 𝓝 ((↑e.symm : Y → X) x)
⊢ ContinuousWithinAt f s x ↔ ContinuousWithinAt (f ∘ (↑e : X → Y)) ((↑e.symm : Y → X) '' s) ((↑e.symm : Y → X) x)

Tactic:
rw [e.continuousWithinAt_iff_continuousWithinAt_comp_right (h hx),
    e.symm_image_eq_source_inter_preimage h, inter_comm, continuousWithinAt_inter]

Premises used: OpenPartialHomeomorph.continuousWithinAt_iff_continuousWithinAt_comp_right, Set.inter_comm, OpenPartialHomeomorph.symm_image_eq_source_inter_preimage, continuousWithinAt_inter
-- 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
f : Y → Z
s : Set Y
h : s ⊆ e.target
x : Y
hx : x ∈ s
⊢ e.source ∈ 𝓝 ((↑e.symm : Y → X) x)

Tactic:
IsOpen.mem_nhds e.open_source (e.map_target (h hx))

Premises used: OpenPartialHomeomorph.open_source, OpenPartialHomeomorph.map_target, IsOpen.mem_nhds
-- 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
f : Y → Z
s : Set Y
h : s ⊆ e.target
x : Y
hx : x ∈ s
⊢ e.source ∈ 𝓝 ((↑e.symm : Y → X) x)

Tactic:
exact IsOpen.mem_nhds e.open_source (e.map_target (h hx))

Premises used: OpenPartialHomeomorph.open_source, OpenPartialHomeomorph.map_target, IsOpen.mem_nhds
-- 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
f : Z → X
s : Set Z
x : Z
hx : f x ∈ e.source
h : f ⁻¹' e.source ∈ 𝓝[s] x
⊢ ContinuousWithinAt f s x ↔ ContinuousWithinAt ((↑e : X → Y) ∘ f) s x

Tactic:
⟨(e.continuousAt hx).comp_continuousWithinAt, fun fe_cont => ?_⟩

Premises used: OpenPartialHomeomorph.continuousAt, Iff.intro, ContinuousAt.comp_continuousWithinAt
-- 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
f : Z → X
s : Set Z
x : Z
hx : f x ∈ e.source
h : f ⁻¹' e.source ∈ 𝓝[s] x
refine : ∀ (fe_cont : ContinuousWithinAt ((↑e : X → Y) ∘ f) s x), ContinuousWithinAt f s x
⊢ ContinuousWithinAt f s x ↔ ContinuousWithinAt ((↑e : X → Y) ∘ f) s x

Tactic:
refine ⟨(e.continuousAt hx).comp_continuousWithinAt, fun fe_cont => ?_⟩
-- 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
f : Z → X
s : Set Z
x : Z
hx : f x ∈ e.source
h : f ⁻¹' e.source ∈ 𝓝[s] x
fe_cont : ContinuousWithinAt ((↑e : X → Y) ∘ f) s x
rw :
  ∀ (fe_cont : ContinuousWithinAt ((↑e : X → Y) ∘ f) (s ∩ f ⁻¹' e.source) x),
    ContinuousWithinAt f (s ∩ f ⁻¹' e.source) x
⊢ ContinuousWithinAt f s x

Tactic:
rw [← continuousWithinAt_inter' h] at fe_cont ⊢

Premises used: continuousWithinAt_inter'
-- 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
f : Z → X
s : Set Z
x : Z
hx : f x ∈ e.source
h : f ⁻¹' e.source ∈ 𝓝[s] x
fe_cont : ContinuousWithinAt ((↑e : X → Y) ∘ f) (s ∩ f ⁻¹' e.source) x
⊢ ContinuousWithinAt ((↑e.symm : Y → X) ∘ (↑e : X → Y) ∘ f) (s ∩ f ⁻¹' e.source) x

Tactic:
have : ContinuousWithinAt (e.symm ∘ e ∘ f) (s ∩ f ⁻¹' e.source) x :=
    haveI : ContinuousWithinAt e.symm univ (e (f x)) :=
      (e.continuousAt_symm (e.map_source hx)).continuousWithinAt
    ContinuousWithinAt.comp this fe_cont (subset_univ _)
-- 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
f : Z → X
s : Set Z
x : Z
hx : f x ∈ e.source
h : f ⁻¹' e.source ∈ 𝓝[s] x
fe_cont : ContinuousWithinAt ((↑e : X → Y) ∘ f) (s ∩ f ⁻¹' e.source) x
this : ContinuousWithinAt ((↑e.symm : Y → X) ∘ (↑e : X → Y) ∘ f) (s ∩ f ⁻¹' e.source) x
y : Z
hy : y ∈ s ∩ f ⁻¹' e.source
⊢ f y = ((↑e.symm : Y → X) ∘ (↑e : X → Y) ∘ f) y

Tactic:
simp [e.left_inv hy.2]

Premises used: OpenPartialHomeomorph.left_inv, And.right
-- 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
f : Z → X
s : Set Z
x : Z
hx : f x ∈ e.source
h : f ⁻¹' e.source ∈ 𝓝[s] x
fe_cont : ContinuousWithinAt ((↑e : X → Y) ∘ f) (s ∩ f ⁻¹' e.source) x
this : ContinuousWithinAt ((↑e.symm : Y → X) ∘ (↑e : X → Y) ∘ f) (s ∩ f ⁻¹' e.source) x
⊢ f x = ((↑e.symm : Y → X) ∘ (↑e : X → Y) ∘ f) x

Tactic:
simp [e.left_inv hx]

Premises used: OpenPartialHomeomorph.left_inv
-- 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
f : Z → X
s : Set Z
x : Z
hx : f x ∈ e.source
h : f ⁻¹' e.source ∈ 𝓝[s] x
fe_cont : ContinuousWithinAt ((↑e : X → Y) ∘ f) (s ∩ f ⁻¹' e.source) x
this : ContinuousWithinAt ((↑e.symm : Y → X) ∘ (↑e : X → Y) ∘ f) (s ∩ f ⁻¹' e.source) x
⊢ ContinuousWithinAt f (s ∩ f ⁻¹' e.source) x

Tactic:
exact this.congr (fun y hy => by simp [e.left_inv hy.2]) (by simp [e.left_inv hx])

Premises used: ContinuousWithinAt.congr
-- 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
f : Z → X
x : Z
h : f ⁻¹' e.source ∈ 𝓝 x
⊢ f x ∈ e.source

Tactic:
have hx : f x ∈ e.source := (mem_of_mem_nhds h :)
-- 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
f : Z → X
x : Z
h : f ⁻¹' e.source ∈ 𝓝 x
hx : f x ∈ e.source
rwa rwa₁ rwa₂ rwa₃ : f ⁻¹' e.source ∈ 𝓝 x
⊢ f ⁻¹' e.source ∈ 𝓝[univ] x

Tactic:
rwa [nhdsWithin_univ]

Premises used: nhdsWithin_univ
-- 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
f : Z → X
x : Z
h : f ⁻¹' e.source ∈ 𝓝 x
hx : f x ∈ e.source
⊢ f ⁻¹' e.source ∈ 𝓝[univ] x

Tactic:
have h' : f ⁻¹' e.source ∈ 𝓝[univ] x := by rwa [nhdsWithin_univ]
-- 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
f : Z → X
x : Z
h : f ⁻¹' e.source ∈ 𝓝 x
hx : f x ∈ e.source
h' : f ⁻¹' e.source ∈ 𝓝[univ] x
rw : ContinuousWithinAt f univ x ↔ ContinuousAt ((↑e : X → Y) ∘ f) x
rw₁ : ContinuousWithinAt f univ x ↔ ContinuousWithinAt ((↑e : X → Y) ∘ f) univ x
rw₂ rw₃ : ContinuousWithinAt ((↑e : X → Y) ∘ f) univ x ↔ ContinuousWithinAt ((↑e : X → Y) ∘ f) univ x
⊢ ContinuousAt f x ↔ ContinuousAt ((↑e : X → Y) ∘ f) x

Tactic:
rw [← continuousWithinAt_univ, ← continuousWithinAt_univ,
    e.continuousWithinAt_iff_continuousWithinAt_comp_left hx h']

Premises used: continuousWithinAt_univ, OpenPartialHomeomorph.continuousWithinAt_iff_continuousWithinAt_comp_left
-- 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
f : Z → X
s : Set Z
h : s ⊆ f ⁻¹' e.source
⊢ ContinuousOn f s ↔ ContinuousOn ((↑e : X → Y) ∘ f) s

Tactic:
forall₂_congr fun _x hx =>
    e.continuousWithinAt_iff_continuousWithinAt_comp_left (h hx)
      (mem_of_superset self_mem_nhdsWithin h)

Premises used: forall₂_congr, self_mem_nhdsWithin, ContinuousOn, OpenPartialHomeomorph.continuousWithinAt_iff_continuousWithinAt_comp_left, Filter.mem_of_superset
-- 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
f : Z → X
h : f ⁻¹' e.source = univ
simp : ContinuousOn f univ ↔ ContinuousOn ((↑e : X → Y) ∘ f) univ
⊢ Continuous[inst_2, inst] f ↔ Continuous[inst_2, inst_1] ((↑e : X → Y) ∘ f)

Tactic:
simp only [← continuousOn_univ]

Premises used: continuousOn_univ
-- 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
f : Z → X
h : f ⁻¹' e.source = univ
⊢ ContinuousOn f univ ↔ ContinuousOn ((↑e : X → Y) ∘ f) univ

Tactic:
e.continuousOn_iff_continuousOn_comp_left (Eq.symm h).subset

Premises used: Eq.subset, Eq.symm, OpenPartialHomeomorph.continuousOn_iff_continuousOn_comp_left
-- 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
f : Z → X
h : f ⁻¹' e.source = univ
⊢ ContinuousOn f univ ↔ ContinuousOn ((↑e : X → Y) ∘ f) univ

Tactic:
exact e.continuousOn_iff_continuousOn_comp_left (Eq.symm h).subset

Premises used: Eq.subset, Eq.symm, OpenPartialHomeomorph.continuousOn_iff_continuousOn_comp_left
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Defs
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
⊢ ContinuousOn (↑e : X → Y) e.source

Tactic:
e.continuousOn_toFun

Premises used: OpenPartialHomeomorph.toFun', OpenPartialHomeomorph.continuousOn_toFun
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Defs
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
⊢ ContinuousOn (↑e.symm : Y → X) e.target

Tactic:
e.continuousOn_invFun

Premises used: OpenPartialHomeomorph.toFun', OpenPartialHomeomorph.continuousOn_invFun
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Defs
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : PartialEquiv X Y
a : IsOpen[inst] e.source
b : IsOpen[inst_1] e.target
c : ContinuousOn (↑e : X → Y) e.source
d : ContinuousOn e.invFun e.target
⊢ (↑{ toPartialEquiv := e, open_source := a, open_target := b, continuousOn_toFun := c, continuousOn_invFun := d :
          OpenPartialHomeomorph X Y } :
      X → Y) =
    (↑e : X → Y)

Tactic:
rfl

Premises used: OpenPartialHomeomorph.toFun', rfl
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Defs
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : PartialEquiv X Y
a : IsOpen[inst] e.source
b : IsOpen[inst_1] e.target
c : ContinuousOn (↑e : X → Y) e.source
d : ContinuousOn e.invFun e.target
⊢ (↑{ toPartialEquiv := e, open_source := a, open_target := b, continuousOn_toFun := c, continuousOn_invFun := d :
            OpenPartialHomeomorph X Y }.symm :
      Y → X) =
    (↑e.symm : Y → X)

Tactic:
rfl

Premises used: OpenPartialHomeomorph.toFun', rfl
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Defs
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
⊢ (↑e.toPartialEquiv : X → Y) = (↑e : X → Y)

Tactic:
rfl

Premises used: OpenPartialHomeomorph.toFun', rfl
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Defs
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
⊢ e.invFun = (↑e.symm : Y → X)

Tactic:
rfl

Premises used: OpenPartialHomeomorph.toFun', rfl
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Defs
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
⊢ (↑e.symm : Y → X) = (↑e.symm : Y → X)

Tactic:
rfl

Premises used: OpenPartialHomeomorph.toFun', rfl
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Defs
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
⊢ (↑e : X → Y) x ∈ e.target

Tactic:
e.map_source' h

Premises used: PartialEquiv.map_source', Set.Mem, OpenPartialHomeomorph.toFun', OpenPartialHomeomorph.toPartialEquiv
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Defs
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
⊢ (↑e : X → Y) '' e.source ⊆ e.target

Tactic:
fun _ ⟨_, hx, hex⟩ ↦ mem_of_eq_of_mem (id hex.symm) (e.map_source' hx)

Premises used: PartialEquiv.map_source', PartialEquiv.target, Membership.mem, id, Set.Subset, _private.0.OpenPartialHomeomorph.map_source''.match_1, Set.mem_of_eq_of_mem, OpenPartialHomeomorph.toPartialEquiv, Eq.symm
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Defs
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
⊢ (↑e.symm : Y → X) x ∈ e.source

Tactic:
e.map_target' h

Premises used: Set.Mem, OpenPartialHomeomorph.toFun', OpenPartialHomeomorph.toPartialEquiv, PartialEquiv.map_target'
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Defs
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
⊢ (↑e.symm : Y → X) ((↑e : X → Y) x) = x

Tactic:
e.left_inv' h

Premises used: OpenPartialHomeomorph.toFun', PartialEquiv.left_inv', OpenPartialHomeomorph.toPartialEquiv
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Defs
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
⊢ (↑e : X → Y) ((↑e.symm : Y → X) x) = x

Tactic:
e.right_inv' h

Premises used: PartialEquiv.right_inv', OpenPartialHomeomorph.toFun', OpenPartialHomeomorph.toPartialEquiv
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Defs
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
x : X
y : Y
hx : x ∈ e.source
hy : y ∈ e.target
⊢ x = (↑e.symm : Y → X) y ↔ (↑e : X → Y) x = y

Tactic:
e.toPartialEquiv.eq_symm_apply hx hy

Premises used: PartialEquiv.eq_symm_apply, OpenPartialHomeomorph.toFun', OpenPartialHomeomorph.toPartialEquiv
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Defs
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
⊢ MapsTo (↑e : X → Y) e.source e.target

Tactic:
fun _ => e.map_source

Premises used: OpenPartialHomeomorph.map_source, Set.MapsTo
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Defs
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
⊢ MapsTo (↑e.symm : Y → X) e.target e.source

Tactic:
e.symm.mapsTo

Premises used: OpenPartialHomeomorph.mapsTo, OpenPartialHomeomorph.symm
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Defs
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
⊢ LeftInvOn (↑e.symm : Y → X) (↑e : X → Y) e.source

Tactic:
fun _ => e.left_inv

Premises used: Set.LeftInvOn, OpenPartialHomeomorph.left_inv
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Defs
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
⊢ RightInvOn (↑e.symm : Y → X) (↑e : X → Y) e.target

Tactic:
fun _ => e.right_inv

Premises used: Set.LeftInvOn, OpenPartialHomeomorph.right_inv
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Defs
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
⊢ InvOn (↑e.symm : Y → X) (↑e : X → Y) e.source e.target

Tactic:
⟨e.leftInvOn, e.rightInvOn⟩

Premises used: Set.InvOn, OpenPartialHomeomorph.leftInvOn, And.intro, OpenPartialHomeomorph.rightInvOn
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Defs
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
⊢ InjOn (↑e : X → Y) e.source

Tactic:
e.leftInvOn.injOn

Premises used: OpenPartialHomeomorph.leftInvOn, Set.LeftInvOn.injOn
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Defs
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
⊢ BijOn (↑e : X → Y) e.source e.target

Tactic:
e.invOn.bijOn e.mapsTo e.symm_mapsTo

Premises used: OpenPartialHomeomorph.symm_mapsTo, OpenPartialHomeomorph.invOn, OpenPartialHomeomorph.mapsTo, Set.InvOn.bijOn
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Defs
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
⊢ SurjOn (↑e : X → Y) e.source e.target

Tactic:
e.bijOn.surjOn

Premises used: OpenPartialHomeomorph.bijOn, Set.BijOn.surjOn