awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Continuity (goal)
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)
⊢ (↑e.symm : Y → X) ⁻¹' s =ᶠ[𝓝 ((↑e : X → Y) x)] e.target ∩ (↑e.symm : Y → X) ⁻¹' (s ∩ f ⁻¹' t)
have 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)
Tactic: rw [eventuallyEq_set, e.eventually_nhds _ hxe]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Continuity (goal)
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)
⊢ ∀ᶠ (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)
have 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))
Tactic: filter_upwards [e.open_source.mem_nhds hxe,
    mem_nhdsWithin_iff_eventually.mp (hf.preimage_mem_nhdsWithin ht)]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Continuity (goal)
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
⊢ (↑e : X → Y) y ∈ (↑e.symm : Y → X) ⁻¹' s ↔ (↑e : X → Y) y ∈ e.target ∩ (↑e.symm : Y → X) ⁻¹' (s ∩ f ⁻¹' t)
have 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)
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]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Continuity (goal)
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)
⊢ (↑e : X → Y) y ∈ (↑e.symm : Y → X) ⁻¹' s ↔ (↑e : X → Y) y ∈ e.target ∩ (↑e.symm : Y → X) ⁻¹' (s ∩ f ⁻¹' t)
have 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
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]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Continuity (goal)
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
⊢ (↑e : X → Y) y ∈ (↑e.symm : Y → X) ⁻¹' s ↔ (↑e : X → Y) y ∈ e.target ∩ (↑e.symm : Y → X) ⁻¹' (s ∩ f ⁻¹' t)
have 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
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]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Continuity (goal)
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
⊢ (↑e : X → Y) y ∈ (↑e.symm : Y → X) ⁻¹' s ↔ (↑e : X → Y) y ∈ e.target ∩ (↑e.symm : Y → X) ⁻¹' (s ∩ f ⁻¹' t)
have 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
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]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Continuity (goal)
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
⊢ (↑e : X → Y) y ∈ (↑e.symm : Y → X) ⁻¹' s ↔ (↑e : X → Y) y ∈ e.target ∩ (↑e.symm : Y → X) ⁻¹' (s ∩ f ⁻¹' t)
have 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
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]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Continuity (goal)
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
⊢ (↑e : X → Y) y ∈ (↑e.symm : Y → X) ⁻¹' s ↔ (↑e : X → Y) y ∈ e.target ∩ (↑e.symm : Y → X) ⁻¹' (s ∩ f ⁻¹' t)
have h₅ : (↑e.symm : Y → X) ((↑e : X → Y) y) ∈ s → (↑e.symm : Y → X) ((↑e : X → Y) y) ∈ 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]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Continuity (goal)
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
⊢ ContinuousWithinAt f s x ↔ ContinuousWithinAt (f ∘ (↑e : X → Y)) ((↑e : X → Y) ⁻¹' s) ((↑e.symm : Y → X) x)
have 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)))
Tactic: simp_rw [ContinuousWithinAt, ← @tendsto_map'_iff _ _ _ _ e,
    e.map_nhdsWithin_preimage_eq (e.map_target h), (· ∘ ·), e.right_inv h]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Continuity (goal)
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)))
⊢ ContinuousWithinAt f s x ↔ ContinuousWithinAt (f ∘ (↑e : X → Y)) ((↑e : X → Y) ⁻¹' s) ((↑e.symm : Y → X) x)
have 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)))
Tactic: simp_rw [ContinuousWithinAt, ← @tendsto_map'_iff _ _ _ _ e,
    e.map_nhdsWithin_preimage_eq (e.map_target h), (· ∘ ·), e.right_inv h]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Continuity (goal)
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)))
⊢ ContinuousWithinAt f s x ↔ ContinuousWithinAt (f ∘ (↑e : X → Y)) ((↑e : X → Y) ⁻¹' s) ((↑e.symm : Y → X) x)
have 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)))
Tactic: simp_rw [ContinuousWithinAt, ← @tendsto_map'_iff _ _ _ _ e,
    e.map_nhdsWithin_preimage_eq (e.map_target h), (· ∘ ·), e.right_inv h]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Continuity (goal)
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)))
⊢ ContinuousWithinAt f s x ↔ ContinuousWithinAt (f ∘ (↑e : X → Y)) ((↑e : X → Y) ⁻¹' s) ((↑e.symm : Y → X) x)
have 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))))
Tactic: simp_rw [ContinuousWithinAt, ← @tendsto_map'_iff _ _ _ _ e,
    e.map_nhdsWithin_preimage_eq (e.map_target h), (· ∘ ·), e.right_inv h]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Continuity (goal)
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
⊢ ContinuousAt f x ↔ ContinuousAt (f ∘ (↑e : X → Y)) ((↑e.symm : Y → X) x)
have rw : ContinuousWithinAt f univ 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]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Continuity (goal)
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)
⊢ ContinuousAt f x ↔ ContinuousAt (f ∘ (↑e : X → Y)) ((↑e.symm : Y → X) x)
have 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)
Tactic: rw [← continuousWithinAt_univ, e.continuousWithinAt_iff_continuousWithinAt_comp_right h,
    preimage_univ, continuousWithinAt_univ]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Continuity (goal)
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)
⊢ ContinuousAt f x ↔ ContinuousAt (f ∘ (↑e : X → Y)) ((↑e.symm : Y → X) x)
have rw₂ : ContinuousWithinAt (f ∘ (↑e : X → Y)) univ ((↑e.symm : Y → X) 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]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Continuity (goal)
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)
⊢ ContinuousAt f x ↔ ContinuousAt (f ∘ (↑e : X → Y)) ((↑e.symm : Y → X) x)
have rw₃ : ContinuousAt (f ∘ (↑e : X → Y)) ((↑e.symm : Y → X) 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]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Continuity (goal)
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
⊢ ContinuousOn f s ↔ ContinuousOn (f ∘ (↑e : X → Y)) (e.source ∩ (↑e : X → Y) ⁻¹' s)
have 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)
Tactic: simp only [← e.symm_image_eq_source_inter_preimage h, ContinuousOn, forall_mem_image]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Continuity (goal)
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)
have 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)
Tactic: refine forall₂_congr fun x hx => ?_
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Continuity (goal)
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
⊢ ContinuousWithinAt f s x ↔ ContinuousWithinAt (f ∘ (↑e : X → Y)) ((↑e.symm : Y → X) '' s) ((↑e.symm : Y → X) x)
have rw : e.source ∈ 𝓝 ((↑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]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Continuity (goal)
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
have refine : ∀ (fe_cont : ContinuousWithinAt ((↑e : X → Y) ∘ f) s x), ContinuousWithinAt f s x
Tactic: refine ⟨(e.continuousAt hx).comp_continuousWithinAt, fun fe_cont => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Continuity (goal)
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
⊢ ContinuousWithinAt f s x
have rw : ∀ (fe_cont : ContinuousWithinAt ((↑e : X → Y) ∘ f) (s ∩ f ⁻¹' e.source) x), ContinuousWithinAt f (s ∩ f ⁻¹' e.source) x
Tactic: rw [← continuousWithinAt_inter' h] at fe_cont ⊢
Cleared hypotheses: fe_cont
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Continuity (hypothesis)
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 f (s ∩ f ⁻¹' e.source) x
have this : 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 _)
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Continuity (hypothesis)
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
⊢ ContinuousAt f x ↔ ContinuousAt ((↑e : X → Y) ∘ f) x
have hx : f x ∈ e.source
Tactic: have hx : f x ∈ e.source := (mem_of_mem_nhds h :)
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Continuity (hypothesis)
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
⊢ ContinuousAt f x ↔ ContinuousAt ((↑e : X → Y) ∘ f) x
have h' : f ⁻¹' e.source ∈ 𝓝[univ] x
Tactic: have h' : f ⁻¹' e.source ∈ 𝓝[univ] x := by rwa [nhdsWithin_univ]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Continuity (goal)
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
⊢ ContinuousAt f x ↔ ContinuousAt ((↑e : X → Y) ∘ f) x
have rw : ContinuousWithinAt f univ x ↔ ContinuousAt ((↑e : X → Y) ∘ f) x
Tactic: rw [← continuousWithinAt_univ, ← continuousWithinAt_univ,
    e.continuousWithinAt_iff_continuousWithinAt_comp_left hx h']
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Continuity (goal)
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
⊢ ContinuousAt f x ↔ ContinuousAt ((↑e : X → Y) ∘ f) x
have rw₁ : ContinuousWithinAt f univ x ↔ ContinuousWithinAt ((↑e : X → Y) ∘ f) univ x
Tactic: rw [← continuousWithinAt_univ, ← continuousWithinAt_univ,
    e.continuousWithinAt_iff_continuousWithinAt_comp_left hx h']
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Continuity (goal)
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
⊢ ContinuousAt f x ↔ ContinuousAt ((↑e : X → Y) ∘ f) x
have rw₂ : ContinuousWithinAt ((↑e : X → Y) ∘ f) univ x ↔ ContinuousWithinAt ((↑e : X → Y) ∘ f) univ x
Tactic: rw [← continuousWithinAt_univ, ← continuousWithinAt_univ,
    e.continuousWithinAt_iff_continuousWithinAt_comp_left hx h']
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Continuity (goal)
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
⊢ Continuous[inst_2, inst] f ↔ Continuous[inst_2, inst_1] ((↑e : X → Y) ∘ f)
have simp : ContinuousOn f univ ↔ ContinuousOn ((↑e : X → Y) ∘ f) univ
Tactic: simp only [← continuousOn_univ]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Defs (goal)
Goal:
X : Type u_1
X' : Type u_2
Y : Type u_3
Y' : Type u_4
Z : Type u_5
Z' : Type u_6
inst : TopologicalSpace X
inst_1 : TopologicalSpace X'
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Y'
inst_4 : TopologicalSpace Z
inst_5 : TopologicalSpace Z'
e_1 : OpenPartialHomeomorph X Y
e : X ≃ₜ Y
⊢ Eq.{u_3 + 1} (α := Set Y) (image.{u_1, u_3} (α := X) (⇑e : (a : X) → Y) univ) univ
have rw : Eq.{u_3 + 1} (α := Set Y) (range.{u_3, u_1 + 1} (ι := X) (⇑e : (a : X) → Y)) univ
Tactic: rw [image_univ, e.surjective.range_eq]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Defs (goal)
Goal:
X : Type u_1
X' : Type u_2
Y : Type u_3
Y' : Type u_4
Z : Type u_5
Z' : Type u_6
inst : TopologicalSpace X
inst_1 : TopologicalSpace X'
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Y'
inst_4 : TopologicalSpace Z
inst_5 : TopologicalSpace Z'
e_1 : OpenPartialHomeomorph X Y
e : X ≃ₜ Y
rw : Eq.{u_3 + 1} (α := Set Y) (range.{u_3, u_1 + 1} (ι := X) (⇑e : (a : X) → Y)) univ
⊢ Eq.{u_3 + 1} (α := Set Y) (image.{u_1, u_3} (α := X) (⇑e : (a : X) → Y) univ) univ
have rw₁ : Eq.{u_3 + 1} (α := Set Y) univ univ
Tactic: rw [image_univ, e.surjective.range_eq]