-- Mathlib/Topology/EMetricSpace/Lipschitz.lean
lemma locallyLipschitzOn_iff_restrict :
    LocallyLipschitzOn s f ↔ LocallyLipschitz (s.restrict f)

Proof state:
case a.h.h.e'_2.h.a.mpr
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
s : Set α
f : α → β
x : ↑s
K : ℝ≥0
⊢ (∃ t, (∃ t_1 ∈ 𝓝[s] ↑x, Subtype.val ⁻¹' t_1 ⊆ t) ∧ LipschitzOnWith K f (s ∩ Subtype.val '' t)) →
    ∃ t ∈ 𝓝[s] ↑x, LipschitzOnWith K f t

Tactic:
rintro ⟨t, ⟨u, hu, hut⟩, hft⟩

Result:
case a.h.h.e'_2.h.a.mpr.intro.intro.intro.intro
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
s : Set α
f : α → β
x : ↑s
K : ℝ≥0
t : Set ↑s
hft : LipschitzOnWith K f (s ∩ Subtype.val '' t)
u : Set α
hu : u ∈ 𝓝[s] ↑x
hut : Subtype.val ⁻¹' u ⊆ t
⊢ ∃ t ∈ 𝓝[s] ↑x, LipschitzOnWith K f t

Proof state:
case a.h.h.e'_2.h.a.mp
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
s : Set α
f : α → β
x : ↑s
K : ℝ≥0
⊢ (∃ t ∈ 𝓝[s] ↑x, LipschitzOnWith K f t) →
    ∃ t, (∃ t_1 ∈ 𝓝[s] ↑x, Subtype.val ⁻¹' t_1 ⊆ t) ∧ LipschitzOnWith K f (s ∩ Subtype.val '' t)

Tactic:
rintro ⟨t, ht, hft⟩

Result:
case a.h.h.e'_2.h.a.mp.intro.intro
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
s : Set α
f : α → β
x : ↑s
K : ℝ≥0
t : Set α
ht : t ∈ 𝓝[s] ↑x
hft : LipschitzOnWith K f t
⊢ ∃ t, (∃ t_1 ∈ 𝓝[s] ↑x, Subtype.val ⁻¹' t_1 ⊆ t) ∧ LipschitzOnWith K f (s ∩ Subtype.val '' t)

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
s : Set α
f : α → β
⊢ LocallyLipschitzOn s f ↔ LocallyLipschitz (s.restrict f)

Tactic:
simp only [LocallyLipschitzOn, LocallyLipschitz, SetCoe.forall', restrict_apply,
  Subtype.edist_mk_mk, ← lipschitzOnWith_iff_restrict, lipschitzOnWith_restrict,
  nhds_subtype_eq_comap_nhdsWithin, mem_comap]

Result:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
s : Set α
f : α → β
⊢ (∀ (x : ↑s), ∃ K, ∃ t ∈ 𝓝[s] ↑x, LipschitzOnWith K f t) ↔
    ∀ (x : ↑s), ∃ K t, (∃ t_1 ∈ 𝓝[s] ↑x, Subtype.val ⁻¹' t_1 ⊆ t) ∧ LipschitzOnWith K f (s ∩ Subtype.val '' t)

Proof state:
case a.h.h.e'_2.h.a.mp.intro.intro
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
s : Set α
f : α → β
x : ↑s
K : ℝ≥0
t : Set α
ht : t ∈ 𝓝[s] ↑x
hft : LipschitzOnWith K f t
⊢ ∃ t, (∃ t_1 ∈ 𝓝[s] ↑x, Subtype.val ⁻¹' t_1 ⊆ t) ∧ LipschitzOnWith K f (s ∩ Subtype.val '' t)

Tactic:
exact ⟨_, ⟨t, ht, Subset.rfl⟩, hft.mono <| inter_subset_right.trans <| image_preimage_subset ..⟩

Result:
no goals

Proof state:
case a.h.h.e'_2.h.a
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
s : Set α
f : α → β
x : ↑s
K : ℝ≥0
⊢ (∃ t ∈ 𝓝[s] ↑x, LipschitzOnWith K f t) ↔
    ∃ t, (∃ t_1 ∈ 𝓝[s] ↑x, Subtype.val ⁻¹' t_1 ⊆ t) ∧ LipschitzOnWith K f (s ∩ Subtype.val '' t)

Tactic:
constructor

Result:
case a.h.h.e'_2.h.a.mp
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
s : Set α
f : α → β
x : ↑s
K : ℝ≥0
⊢ (∃ t ∈ 𝓝[s] ↑x, LipschitzOnWith K f t) →
    ∃ t, (∃ t_1 ∈ 𝓝[s] ↑x, Subtype.val ⁻¹' t_1 ⊆ t) ∧ LipschitzOnWith K f (s ∩ Subtype.val '' t)

case a.h.h.e'_2.h.a.mpr
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
s : Set α
f : α → β
x : ↑s
K : ℝ≥0
⊢ (∃ t, (∃ t_1 ∈ 𝓝[s] ↑x, Subtype.val ⁻¹' t_1 ⊆ t) ∧ LipschitzOnWith K f (s ∩ Subtype.val '' t)) →
    ∃ t ∈ 𝓝[s] ↑x, LipschitzOnWith K f t

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
s : Set α
f : α → β
⊢ (∀ (x : ↑s), ∃ K, ∃ t ∈ 𝓝[s] ↑x, LipschitzOnWith K f t) ↔
    ∀ (x : ↑s), ∃ K t, (∃ t_1 ∈ 𝓝[s] ↑x, Subtype.val ⁻¹' t_1 ⊆ t) ∧ LipschitzOnWith K f (s ∩ Subtype.val '' t)

Tactic:
congr! with x K

Result:
case a.h.h.e'_2.h.a
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
s : Set α
f : α → β
x : ↑s
K : ℝ≥0
⊢ (∃ t ∈ 𝓝[s] ↑x, LipschitzOnWith K f t) ↔
    ∃ t, (∃ t_1 ∈ 𝓝[s] ↑x, Subtype.val ⁻¹' t_1 ⊆ t) ∧ LipschitzOnWith K f (s ∩ Subtype.val '' t)

Proof state:
case a.h.h.e'_2.h.a.mpr.intro.intro.intro.intro
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
s : Set α
f : α → β
x : ↑s
K : ℝ≥0
t : Set ↑s
hft : LipschitzOnWith K f (s ∩ Subtype.val '' t)
u : Set α
hu : u ∈ 𝓝[s] ↑x
hut : Subtype.val ⁻¹' u ⊆ t
⊢ ∃ t ∈ 𝓝[s] ↑x, LipschitzOnWith K f t

Tactic:
exact ⟨s ∩ u, Filter.inter_mem self_mem_nhdsWithin hu,
  hft.mono fun x hx ↦ ⟨hx.1, ⟨x, hx.1⟩, hut hx.2, rfl⟩⟩

Result:
no goals