-- Mathlib/Topology/ContinuousOn.lean
theorem continuousOn_open_iff (hs : IsOpen s) :
    ContinuousOn f s ↔ ∀ t, IsOpen t → IsOpen (s ∩ f ⁻¹' t)

Proof state:
case mpr
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hs : IsOpen s
h : ∀ (t : Set β), IsOpen t → IsOpen (s ∩ f ⁻¹' t)
t : Set β
ht : IsOpen t
⊢ ∃ u, IsOpen u ∧ f ⁻¹' t ∩ s = u ∩ s

Tactic:
refine ⟨s ∩ f ⁻¹' t, h t ht, ?_⟩

Result:
case mpr
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hs : IsOpen s
h : ∀ (t : Set β), IsOpen t → IsOpen (s ∩ f ⁻¹' t)
t : Set β
ht : IsOpen t
⊢ f ⁻¹' t ∩ s = s ∩ f ⁻¹' t ∩ s

Proof state:
case mp.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hs : IsOpen s
h : ∀ (t : Set β), IsOpen t → ∃ u, IsOpen u ∧ f ⁻¹' t ∩ s = u ∩ s
t : Set β
ht : IsOpen t
u : Set α
u_open : IsOpen u
hu : f ⁻¹' t ∩ s = u ∩ s
⊢ IsOpen (s ∩ f ⁻¹' t)

Tactic:
rw [inter_comm, hu]

Result:
case mp.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hs : IsOpen s
h : ∀ (t : Set β), IsOpen t → ∃ u, IsOpen u ∧ f ⁻¹' t ∩ s = u ∩ s
t : Set β
ht : IsOpen t
u : Set α
u_open : IsOpen u
hu : f ⁻¹' t ∩ s = u ∩ s
⊢ IsOpen (u ∩ s)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hs : IsOpen s
⊢ ContinuousOn f s ↔ ∀ (t : Set β), IsOpen t → IsOpen (s ∩ f ⁻¹' t)

Tactic:
rw [continuousOn_iff']

Result:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hs : IsOpen s
⊢ (∀ (t : Set β), IsOpen t → ∃ u, IsOpen u ∧ f ⁻¹' t ∩ s = u ∩ s) ↔ ∀ (t : Set β), IsOpen t → IsOpen (s ∩ f ⁻¹' t)

Proof state:
case mpr
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hs : IsOpen s
⊢ (∀ (t : Set β), IsOpen t → IsOpen (s ∩ f ⁻¹' t)) → ∀ (t : Set β), IsOpen t → ∃ u, IsOpen u ∧ f ⁻¹' t ∩ s = u ∩ s

Tactic:
intro h t ht

Result:
case mpr
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hs : IsOpen s
h : ∀ (t : Set β), IsOpen t → IsOpen (s ∩ f ⁻¹' t)
t : Set β
ht : IsOpen t
⊢ ∃ u, IsOpen u ∧ f ⁻¹' t ∩ s = u ∩ s

Proof state:
case mp
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hs : IsOpen s
⊢ (∀ (t : Set β), IsOpen t → ∃ u, IsOpen u ∧ f ⁻¹' t ∩ s = u ∩ s) → ∀ (t : Set β), IsOpen t → IsOpen (s ∩ f ⁻¹' t)

Tactic:
intro h t ht

Result:
case mp
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hs : IsOpen s
h : ∀ (t : Set β), IsOpen t → ∃ u, IsOpen u ∧ f ⁻¹' t ∩ s = u ∩ s
t : Set β
ht : IsOpen t
⊢ IsOpen (s ∩ f ⁻¹' t)

Proof state:
case mp
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hs : IsOpen s
h : ∀ (t : Set β), IsOpen t → ∃ u, IsOpen u ∧ f ⁻¹' t ∩ s = u ∩ s
t : Set β
ht : IsOpen t
⊢ IsOpen (s ∩ f ⁻¹' t)

Tactic:
rcases h t ht with ⟨u, u_open, hu⟩

Result:
case mp.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hs : IsOpen s
h : ∀ (t : Set β), IsOpen t → ∃ u, IsOpen u ∧ f ⁻¹' t ∩ s = u ∩ s
t : Set β
ht : IsOpen t
u : Set α
u_open : IsOpen u
hu : f ⁻¹' t ∩ s = u ∩ s
⊢ IsOpen (s ∩ f ⁻¹' t)

Proof state:
case mp.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hs : IsOpen s
h : ∀ (t : Set β), IsOpen t → ∃ u, IsOpen u ∧ f ⁻¹' t ∩ s = u ∩ s
t : Set β
ht : IsOpen t
u : Set α
u_open : IsOpen u
hu : f ⁻¹' t ∩ s = u ∩ s
⊢ IsOpen (u ∩ s)

Tactic:
apply IsOpen.inter u_open hs

Result:
no goals

Proof state:
case mpr
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hs : IsOpen s
h : ∀ (t : Set β), IsOpen t → IsOpen (s ∩ f ⁻¹' t)
t : Set β
ht : IsOpen t
⊢ f ⁻¹' t ∩ s = s ∩ f ⁻¹' t ∩ s

Tactic:
rw [@inter_comm _ s (f ⁻¹' t), inter_assoc, inter_self]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hs : IsOpen s
⊢ (∀ (t : Set β), IsOpen t → ∃ u, IsOpen u ∧ f ⁻¹' t ∩ s = u ∩ s) ↔ ∀ (t : Set β), IsOpen t → IsOpen (s ∩ f ⁻¹' t)

Tactic:
constructor

Result:
case mp
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hs : IsOpen s
⊢ (∀ (t : Set β), IsOpen t → ∃ u, IsOpen u ∧ f ⁻¹' t ∩ s = u ∩ s) → ∀ (t : Set β), IsOpen t → IsOpen (s ∩ f ⁻¹' t)

case mpr
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hs : IsOpen s
⊢ (∀ (t : Set β), IsOpen t → IsOpen (s ∩ f ⁻¹' t)) → ∀ (t : Set β), IsOpen t → ∃ u, IsOpen u ∧ f ⁻¹' t ∩ s = u ∩ s