-- Mathlib/Topology/ContinuousOn.lean
theorem continuousOn_iff' :
    ContinuousOn f s ↔ ∀ t : Set β, IsOpen t → ∃ u, IsOpen u ∧ f ⁻¹' t ∩ s = u ∩ s

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

Tactic:
rw [isOpen_induced_iff, Set.restrict_eq, Set.preimage_comp]

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

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

Tactic:
intro t

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

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

Tactic:
rw [continuousOn_iff_continuous_restrict, continuous_def]

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

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

Tactic:
simp only [Subtype.preimage_coe_eq_preimage_coe_iff]

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

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
t : Set β
u : Set α
ou : IsOpen u
useq : f ⁻¹' t ∩ s = u ∩ s
⊢ s ∩ u = s ∩ f ⁻¹' t

Tactic:
simpa only [Set.inter_comm, eq_comm] using useq

Result:
no goals

Proof state:
case mpr.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
t : Set β
u : Set α
ou : IsOpen u
useq : f ⁻¹' t ∩ s = u ∩ s
⊢ ∃ t_1, IsOpen t_1 ∧ s ∩ t_1 = s ∩ f ⁻¹' t

Tactic:
exact ⟨u, ou, by simpa only [Set.inter_comm, eq_comm] using useq⟩

Result:
no goals

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

Tactic:
simp only [this]

Result:
no goals

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

Tactic:
rintro ⟨u, ou, useq⟩

Result:
case mpr.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
t : Set β
u : Set α
ou : IsOpen u
useq : f ⁻¹' t ∩ s = u ∩ s
⊢ ∃ t_1, IsOpen t_1 ∧ s ∩ t_1 = s ∩ f ⁻¹' t