-- Mathlib/Topology/Partial.lean
theorem pcontinuous_iff' {f : X →. Y} :
    PContinuous f ↔ ∀ {x y} (_ : y ∈ f x), PTendsto' f (𝓝 x) (𝓝 y)

Proof state:
case mpr.intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X →. Y
hf : ∀ {x : X} {y : Y}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
s : Set Y
os : IsOpen s
x : X
y : Y
ys : y ∈ s
fxy : y ∈ f x
t : Set X
h : f.preimage s ⊆ t
⊢ t ∈ 𝓝 x

Tactic:
apply mem_of_superset _ h

Result:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X →. Y
hf : ∀ {x : X} {y : Y}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
s : Set Y
os : IsOpen s
x : X
y : Y
ys : y ∈ s
fxy : y ∈ f x
t : Set X
h : f.preimage s ⊆ t
⊢ f.preimage s ∈ 𝓝 x

Proof state:
case mp.intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X →. Y
h : PContinuous f
x : X
y : Y
h' : y ∈ f x
s t : Set Y
tsubs : t ⊆ s
opent : IsOpen t
yt : y ∈ t
⊢ ∃ t ⊆ f.preimage s, IsOpen t ∧ x ∈ t

Tactic:
exact ⟨f.preimage t, PFun.preimage_mono _ tsubs, h _ opent, ⟨y, yt, h'⟩⟩

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X →. Y
hf : ∀ {x : X} {y : Y}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
s : Set Y
os : IsOpen s
x : X
y : Y
ys : y ∈ s
fxy : y ∈ f x
t : Set X
h : f.preimage s ⊆ t
⊢ f.preimage s ∈ 𝓝 x

Tactic:
have h' : ∀ s ∈ 𝓝 y, f.preimage s ∈ 𝓝 x := by
  intro s hs
  have : PTendsto' f (𝓝 x) (𝓝 y) := hf fxy
  rw [ptendsto'_def] at this
  exact this s hs

Result:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X →. Y
hf : ∀ {x : X} {y : Y}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
s : Set Y
os : IsOpen s
x : X
y : Y
ys : y ∈ s
fxy : y ∈ f x
t : Set X
h : f.preimage s ⊆ t
h' : ∀ s ∈ 𝓝 y, f.preimage s ∈ 𝓝 x
⊢ f.preimage s ∈ 𝓝 x

Proof state:
case mpr
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X →. Y
hf : ∀ {x : X} {y : Y}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
s : Set Y
os : IsOpen s
⊢ IsOpen (f.preimage s)

Tactic:
rw [isOpen_iff_nhds]

Result:
case mpr
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X →. Y
hf : ∀ {x : X} {y : Y}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
s : Set Y
os : IsOpen s
⊢ ∀ x ∈ f.preimage s, 𝓝 x ≤ 𝓟 (f.preimage s)

Proof state:
case mpr.intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X →. Y
hf : ∀ {x : X} {y : Y}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
s : Set Y
os : IsOpen s
x : X
y : Y
ys : y ∈ s
fxy : y ∈ f x
t : Set X
⊢ t ∈ 𝓟 (f.preimage s) → t ∈ 𝓝 x

Tactic:
rw [mem_principal]

Result:
case mpr.intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X →. Y
hf : ∀ {x : X} {y : Y}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
s : Set Y
os : IsOpen s
x : X
y : Y
ys : y ∈ s
fxy : y ∈ f x
t : Set X
⊢ f.preimage s ⊆ t → t ∈ 𝓝 x

Proof state:
case mp
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X →. Y
h : PContinuous f
x : X
y : Y
h' : y ∈ f x
⊢ PTendsto' f (𝓝 x) (𝓝 y)

Tactic:
simp only [ptendsto'_def, mem_nhds_iff]

Result:
case mp
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X →. Y
h : PContinuous f
x : X
y : Y
h' : y ∈ f x
⊢ ∀ (s : Set Y), (∃ t ⊆ s, IsOpen t ∧ y ∈ t) → ∃ t ⊆ f.preimage s, IsOpen t ∧ x ∈ t

Proof state:
case mpr
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X →. Y
⊢ (∀ {x : X} {y : Y}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)) → PContinuous f

Tactic:
intro hf s os

Result:
case mpr
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X →. Y
hf : ∀ {x : X} {y : Y}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
s : Set Y
os : IsOpen s
⊢ IsOpen (f.preimage s)

Proof state:
case mpr
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X →. Y
hf : ∀ {x : X} {y : Y}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
s : Set Y
os : IsOpen s
⊢ ∀ x ∈ f.preimage s, 𝓝 x ≤ 𝓟 (f.preimage s)

Tactic:
rintro x ⟨y, ys, fxy⟩ t

Result:
case mpr.intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X →. Y
hf : ∀ {x : X} {y : Y}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
s : Set Y
os : IsOpen s
x : X
y : Y
ys : y ∈ s
fxy : y ∈ f x
t : Set X
⊢ t ∈ 𝓟 (f.preimage s) → t ∈ 𝓝 x

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X →. Y
hf : ∀ {x : X} {y : Y}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
s : Set Y
os : IsOpen s
x : X
y : Y
ys : y ∈ s
fxy : y ∈ f x
t : Set X
h : f.preimage s ⊆ t
h' : ∀ s ∈ 𝓝 y, f.preimage s ∈ 𝓝 x
⊢ f.preimage s ∈ 𝓝 x

Tactic:
apply h'

Result:
case a
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X →. Y
hf : ∀ {x : X} {y : Y}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
s : Set Y
os : IsOpen s
x : X
y : Y
ys : y ∈ s
fxy : y ∈ f x
t : Set X
h : f.preimage s ⊆ t
h' : ∀ s ∈ 𝓝 y, f.preimage s ∈ 𝓝 x
⊢ s ∈ 𝓝 y

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X →. Y
hf : ∀ {x : X} {y : Y}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
s✝ : Set Y
os : IsOpen s✝
x : X
y : Y
ys : y ∈ s✝
fxy : y ∈ f x
t : Set X
h : f.preimage s✝ ⊆ t
s : Set Y
hs : s ∈ 𝓝 y
this : ∀ s ∈ 𝓝 y, f.preimage s ∈ 𝓝 x
⊢ f.preimage s ∈ 𝓝 x

Tactic:
exact this s hs

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X →. Y
hf : ∀ {x : X} {y : Y}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
s✝ : Set Y
os : IsOpen s✝
x : X
y : Y
ys : y ∈ s✝
fxy : y ∈ f x
t : Set X
h : f.preimage s✝ ⊆ t
s : Set Y
hs : s ∈ 𝓝 y
⊢ f.preimage s ∈ 𝓝 x

Tactic:
have : PTendsto' f (𝓝 x) (𝓝 y) := hf fxy

Result:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X →. Y
hf : ∀ {x : X} {y : Y}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
s✝ : Set Y
os : IsOpen s✝
x : X
y : Y
ys : y ∈ s✝
fxy : y ∈ f x
t : Set X
h : f.preimage s✝ ⊆ t
s : Set Y
hs : s ∈ 𝓝 y
this : PTendsto' f (𝓝 x) (𝓝 y)
⊢ f.preimage s ∈ 𝓝 x

Proof state:
case a
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X →. Y
hf : ∀ {x : X} {y : Y}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
s : Set Y
os : IsOpen s
x : X
y : Y
ys : y ∈ s
fxy : y ∈ f x
t : Set X
h : f.preimage s ⊆ t
h' : ∀ s ∈ 𝓝 y, f.preimage s ∈ 𝓝 x
⊢ s ∈ 𝓝 y

Tactic:
rw [mem_nhds_iff]

Result:
case a
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X →. Y
hf : ∀ {x : X} {y : Y}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
s : Set Y
os : IsOpen s
x : X
y : Y
ys : y ∈ s
fxy : y ∈ f x
t : Set X
h : f.preimage s ⊆ t
h' : ∀ s ∈ 𝓝 y, f.preimage s ∈ 𝓝 x
⊢ ∃ t ⊆ s, IsOpen t ∧ y ∈ t

Proof state:
case mpr.intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X →. Y
hf : ∀ {x : X} {y : Y}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
s : Set Y
os : IsOpen s
x : X
y : Y
ys : y ∈ s
fxy : y ∈ f x
t : Set X
⊢ f.preimage s ⊆ t → t ∈ 𝓝 x

Tactic:
intro (h : f.preimage s ⊆ t)

Result:
case mpr.intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X →. Y
hf : ∀ {x : X} {y : Y}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
s : Set Y
os : IsOpen s
x : X
y : Y
ys : y ∈ s
fxy : y ∈ f x
t : Set X
h : f.preimage s ⊆ t
⊢ t ∈ 𝓝 x

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X →. Y
hf : ∀ {x : X} {y : Y}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
s : Set Y
os : IsOpen s
x : X
y : Y
ys : y ∈ s
fxy : y ∈ f x
t : Set X
h : f.preimage s ⊆ t
⊢ ∀ s ∈ 𝓝 y, f.preimage s ∈ 𝓝 x

Tactic:
intro s hs

Result:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X →. Y
hf : ∀ {x : X} {y : Y}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
s✝ : Set Y
os : IsOpen s✝
x : X
y : Y
ys : y ∈ s✝
fxy : y ∈ f x
t : Set X
h : f.preimage s✝ ⊆ t
s : Set Y
hs : s ∈ 𝓝 y
⊢ f.preimage s ∈ 𝓝 x