-- Mathlib/Topology/MetricSpace/Kuratowski.lean
theorem LipschitzOnWith.extend_lp_infty [PseudoMetricSpace α] {s : Set α} {ι : Type*}
    {f : α → ℓ^∞(ι)} {K : ℝ≥0} (hfl : LipschitzOnWith K f s) :
    ∃ g : α → ℓ^∞(ι), LipschitzWith K g ∧ EqOn f g s

Proof state:
case inr.intro.refine_2
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
ι : Type u_1
f : α → ↥(lp (fun i => ℝ) ⊤)
K : ℝ≥0
hfl : ∀ (i : ι), LipschitzOnWith K (fun a => ↑(f a) i) s
g : ι → α → ℝ
hgl : ∀ (i : ι), LipschitzWith K (g i)
hgeq : ∀ (i : ι), EqOn (fun x => ↑(f x) i) (g i) s
a₀ : α
ha₀_in_s : a₀ ∈ s
hf_extb : ∀ (a : α), Memℓp (swap g a) ⊤
f_ext' : α → ↥(lp (fun i => ℝ) ⊤) := fun i => ⟨swap g i, ⋯⟩
a : α
hyp : a ∈ s
⊢ f a = f_ext' a

Tactic:
ext i

Result:
case inr.intro.refine_2.h.h
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
ι : Type u_1
f : α → ↥(lp (fun i => ℝ) ⊤)
K : ℝ≥0
hfl : ∀ (i : ι), LipschitzOnWith K (fun a => ↑(f a) i) s
g : ι → α → ℝ
hgl : ∀ (i : ι), LipschitzWith K (g i)
hgeq : ∀ (i : ι), EqOn (fun x => ↑(f x) i) (g i) s
a₀ : α
ha₀_in_s : a₀ ∈ s
hf_extb : ∀ (a : α), Memℓp (swap g a) ⊤
f_ext' : α → ↥(lp (fun i => ℝ) ⊤) := fun i => ⟨swap g i, ⋯⟩
a : α
hyp : a ∈ s
i : ι
⊢ ↑(f a) i = ↑(f_ext' a) i

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
ι : Type u_1
f : α → ↥(lp (fun i => ℝ) ⊤)
K : ℝ≥0
g : ι → α → ℝ
hgl : ∀ (i : ι), LipschitzWith K (g i)
hfl : ∀ (i : ι), LipschitzOnWith K (fun a => ↑(f a) i) ∅
hgeq : ∀ (i : ι), EqOn (fun x => ↑(f x) i) (g i) ∅
⊢ EqOn f 0 ∅

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
ι : Type u_1
f : α → ↥(lp (fun i => ℝ) ⊤)
K : ℝ≥0
hfl : ∀ (i : ι), LipschitzOnWith K (fun a => ↑(f a) i) s
g : ι → α → ℝ
hgl : ∀ (i : ι), LipschitzWith K (g i)
hgeq : ∀ (i : ι), EqOn (fun x => ↑(f x) i) (g i) s
⊢ ∃ g, LipschitzWith K g ∧ EqOn f g s

Tactic:
rcases s.eq_empty_or_nonempty with rfl | ⟨a₀, ha₀_in_s⟩

Result:
case inl
α : Type u
inst✝ : PseudoMetricSpace α
ι : Type u_1
f : α → ↥(lp (fun i => ℝ) ⊤)
K : ℝ≥0
g : ι → α → ℝ
hgl : ∀ (i : ι), LipschitzWith K (g i)
hfl : ∀ (i : ι), LipschitzOnWith K (fun a => ↑(f a) i) ∅
hgeq : ∀ (i : ι), EqOn (fun x => ↑(f x) i) (g i) ∅
⊢ ∃ g, LipschitzWith K g ∧ EqOn f g ∅

case inr.intro
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
ι : Type u_1
f : α → ↥(lp (fun i => ℝ) ⊤)
K : ℝ≥0
hfl : ∀ (i : ι), LipschitzOnWith K (fun a => ↑(f a) i) s
g : ι → α → ℝ
hgl : ∀ (i : ι), LipschitzWith K (g i)
hgeq : ∀ (i : ι), EqOn (fun x => ↑(f x) i) (g i) s
a₀ : α
ha₀_in_s : a₀ ∈ s
⊢ ∃ g, LipschitzWith K g ∧ EqOn f g s

Proof state:
case inr.intro.refine_1
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
ι : Type u_1
f : α → ↥(lp (fun i => ℝ) ⊤)
K : ℝ≥0
hfl : ∀ (i : ι), LipschitzOnWith K (fun a => ↑(f a) i) s
g : ι → α → ℝ
hgl : ∀ (i : ι), LipschitzWith K (g i)
hgeq : ∀ (i : ι), EqOn (fun x => ↑(f x) i) (g i) s
a₀ : α
ha₀_in_s : a₀ ∈ s
hf_extb : ∀ (a : α), Memℓp (swap g a) ⊤
f_ext' : α → ↥(lp (fun i => ℝ) ⊤) := fun i => ⟨swap g i, ⋯⟩
⊢ LipschitzWith K f_ext'

Tactic:
rw [LipschitzWith.coordinate]

Result:
case inr.intro.refine_1
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
ι : Type u_1
f : α → ↥(lp (fun i => ℝ) ⊤)
K : ℝ≥0
hfl : ∀ (i : ι), LipschitzOnWith K (fun a => ↑(f a) i) s
g : ι → α → ℝ
hgl : ∀ (i : ι), LipschitzWith K (g i)
hgeq : ∀ (i : ι), EqOn (fun x => ↑(f x) i) (g i) s
a₀ : α
ha₀_in_s : a₀ ∈ s
hf_extb : ∀ (a : α), Memℓp (swap g a) ⊤
f_ext' : α → ↥(lp (fun i => ℝ) ⊤) := fun i => ⟨swap g i, ⋯⟩
⊢ ∀ (i : ι), LipschitzWith K fun a => ↑(f_ext' a) i

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
ι : Type u_1
f : α → ↥(lp (fun i => ℝ) ⊤)
K : ℝ≥0
hfl : LipschitzOnWith K f s
⊢ ∃ g, LipschitzWith K g ∧ EqOn f g s

Tactic:
rw [LipschitzOnWith.coordinate] at hfl

Result:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
ι : Type u_1
f : α → ↥(lp (fun i => ℝ) ⊤)
K : ℝ≥0
hfl : ∀ (i : ι), LipschitzOnWith K (fun a => ↑(f a) i) s
⊢ ∃ g, LipschitzWith K g ∧ EqOn f g s

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
ι : Type u_1
f : α → ↥(lp (fun i => ℝ) ⊤)
K : ℝ≥0
hfl : ∀ (i : ι), LipschitzOnWith K (fun a => ↑(f a) i) s
this : ∀ (i : ι), ∃ g, LipschitzWith K g ∧ EqOn (fun x => ↑(f x) i) g s
⊢ ∃ g, LipschitzWith K g ∧ EqOn f g s

Tactic:
choose g hgl hgeq using this

Result:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
ι : Type u_1
f : α → ↥(lp (fun i => ℝ) ⊤)
K : ℝ≥0
hfl : ∀ (i : ι), LipschitzOnWith K (fun a => ↑(f a) i) s
g : ι → α → ℝ
hgl : ∀ (i : ι), LipschitzWith K (g i)
hgeq : ∀ (i : ι), EqOn (fun x => ↑(f x) i) (g i) s
⊢ ∃ g, LipschitzWith K g ∧ EqOn f g s

Proof state:
case inr.intro.refine_2
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
ι : Type u_1
f : α → ↥(lp (fun i => ℝ) ⊤)
K : ℝ≥0
hfl : ∀ (i : ι), LipschitzOnWith K (fun a => ↑(f a) i) s
g : ι → α → ℝ
hgl : ∀ (i : ι), LipschitzWith K (g i)
hgeq : ∀ (i : ι), EqOn (fun x => ↑(f x) i) (g i) s
a₀ : α
ha₀_in_s : a₀ ∈ s
hf_extb : ∀ (a : α), Memℓp (swap g a) ⊤
f_ext' : α → ↥(lp (fun i => ℝ) ⊤) := fun i => ⟨swap g i, ⋯⟩
⊢ EqOn f f_ext' s

Tactic:
intro a hyp

Result:
case inr.intro.refine_2
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
ι : Type u_1
f : α → ↥(lp (fun i => ℝ) ⊤)
K : ℝ≥0
hfl : ∀ (i : ι), LipschitzOnWith K (fun a => ↑(f a) i) s
g : ι → α → ℝ
hgl : ∀ (i : ι), LipschitzWith K (g i)
hgeq : ∀ (i : ι), EqOn (fun x => ↑(f x) i) (g i) s
a₀ : α
ha₀_in_s : a₀ ∈ s
hf_extb : ∀ (a : α), Memℓp (swap g a) ⊤
f_ext' : α → ↥(lp (fun i => ℝ) ⊤) := fun i => ⟨swap g i, ⋯⟩
a : α
hyp : a ∈ s
⊢ f a = f_ext' a

Proof state:
case inr.intro
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
ι : Type u_1
f : α → ↥(lp (fun i => ℝ) ⊤)
K : ℝ≥0
hfl : ∀ (i : ι), LipschitzOnWith K (fun a => ↑(f a) i) s
g : ι → α → ℝ
hgl : ∀ (i : ι), LipschitzWith K (g i)
hgeq : ∀ (i : ι), EqOn (fun x => ↑(f x) i) (g i) s
a₀ : α
ha₀_in_s : a₀ ∈ s
hf_extb : ∀ (a : α), Memℓp (swap g a) ⊤
⊢ ∃ g, LipschitzWith K g ∧ EqOn f g s

Tactic:
let f_ext' : α → ℓ^∞(ι) := fun i ↦ ⟨swap g i, hf_extb i⟩

Result:
case inr.intro
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
ι : Type u_1
f : α → ↥(lp (fun i => ℝ) ⊤)
K : ℝ≥0
hfl : ∀ (i : ι), LipschitzOnWith K (fun a => ↑(f a) i) s
g : ι → α → ℝ
hgl : ∀ (i : ι), LipschitzWith K (g i)
hgeq : ∀ (i : ι), EqOn (fun x => ↑(f x) i) (g i) s
a₀ : α
ha₀_in_s : a₀ ∈ s
hf_extb : ∀ (a : α), Memℓp (swap g a) ⊤
f_ext' : α → ↥(lp (fun i => ℝ) ⊤) := fun i => ⟨swap g i, ⋯⟩
⊢ ∃ g, LipschitzWith K g ∧ EqOn f g s

Proof state:
case h.intro
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
ι : Type u_1
f : α → ↥(lp (fun i => ℝ) ⊤)
K : ℝ≥0
hfl : ∀ (i : ι), LipschitzOnWith K (fun a => ↑(f a) i) s
g : ι → α → ℝ
hgl : ∀ (i : ι), LipschitzWith K (g i)
hgeq : ∀ (i : ι), EqOn (fun x => ↑(f x) i) (g i) s
a₀ : α
ha₀_in_s : a₀ ∈ s
i : ι
⊢ ‖↑(f a₀) i‖ ≤ ‖f a₀‖

Tactic:
exact lp.norm_apply_le_norm top_ne_zero (f a₀) i

Result:
no goals