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

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

Tactic:
simp only [this]

Result:
no goals

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

Tactic:
simp only [Subtype.preimage_coe_eq_preimage_coe_iff, eq_comm, Set.inter_comm s]

Result:
no goals

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

Tactic:
rw [isClosed_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, IsClosed t_1 ∧ Subtype.val ⁻¹' t_1 = Subtype.val ⁻¹' (f ⁻¹' t)) ↔ ∃ u, IsClosed u ∧ f ⁻¹' t ∩ s = u ∩ s

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

Tactic:
have : ∀ t, IsClosed (s.restrict f ⁻¹' t) ↔ ∃ u : Set α, IsClosed u ∧ f ⁻¹' t ∩ s = u ∩ s := by
  intro t
  rw [isClosed_induced_iff, Set.restrict_eq, Set.preimage_comp]
  simp only [Subtype.preimage_coe_eq_preimage_coe_iff, eq_comm, Set.inter_comm s]

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

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

Tactic:
rw [continuousOn_iff_continuous_restrict, continuous_iff_isClosed]

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

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
⊢ ∀ (t : Set β), IsClosed (s.restrict f ⁻¹' t) ↔ ∃ u, IsClosed 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 β
⊢ IsClosed (s.restrict f ⁻¹' t) ↔ ∃ u, IsClosed u ∧ f ⁻¹' t ∩ s = u ∩ s