-- Mathlib/Topology/MetricSpace/Lipschitz.lean
theorem LipschitzOnWith.extend_pi [Fintype ι] {f : α → ι → ℝ} {s : Set α}
    {K : ℝ≥0} (hf : LipschitzOnWith K f s) : ∃ g : α → ι → ℝ, LipschitzWith K g ∧ EqOn f g s

Proof state:
α : Type u
ι : Type x
inst✝¹ : PseudoMetricSpace α
inst✝ : Fintype ι
f : α → ι → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
i : ι
this : LipschitzOnWith K (fun x => f x i) s
⊢ ∃ g, LipschitzWith K g ∧ EqOn (fun x => f x i) g s

Tactic:
exact this.extend_real

Result:
no goals

Proof state:
case refine_2
α : Type u
ι : Type x
inst✝¹ : PseudoMetricSpace α
inst✝ : Fintype ι
f : α → ι → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
g : ι → α → ℝ
hg : ∀ (i : ι), LipschitzWith K (g i) ∧ EqOn (fun x => f x i) (g i) s
x : α
hx : x ∈ s
⊢ f x = (fun x i => g i x) x

Tactic:
ext1 i

Result:
case refine_2.h
α : Type u
ι : Type x
inst✝¹ : PseudoMetricSpace α
inst✝ : Fintype ι
f : α → ι → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
g : ι → α → ℝ
hg : ∀ (i : ι), LipschitzWith K (g i) ∧ EqOn (fun x => f x i) (g i) s
x : α
hx : x ∈ s
i : ι
⊢ f x i = (fun x i => g i x) x i

Proof state:
case refine_1
α : Type u
ι : Type x
inst✝¹ : PseudoMetricSpace α
inst✝ : Fintype ι
f : α → ι → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
g : ι → α → ℝ
hg : ∀ (i : ι), LipschitzWith K (g i) ∧ EqOn (fun x => f x i) (g i) s
x y : α
⊢ (dist (fun i => g i x) fun i => g i y) ≤ ↑K * dist x y

Tactic:
exact (dist_pi_le_iff (mul_nonneg K.2 dist_nonneg)).2 fun i => (hg i).1.dist_le_mul x y

Result:
no goals

Proof state:
α : Type u
ι : Type x
inst✝¹ : PseudoMetricSpace α
inst✝ : Fintype ι
f : α → ι → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f 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 hg using this

Result:
α : Type u
ι : Type x
inst✝¹ : PseudoMetricSpace α
inst✝ : Fintype ι
f : α → ι → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
g : ι → α → ℝ
hg : ∀ (i : ι), LipschitzWith K (g i) ∧ EqOn (fun x => f x i) (g i) s
⊢ ∃ g, LipschitzWith K g ∧ EqOn f g s

Proof state:
α : Type u
ι : Type x
inst✝¹ : PseudoMetricSpace α
inst✝ : Fintype ι
f : α → ι → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
g : ι → α → ℝ
hg : ∀ (i : ι), LipschitzWith K (g i) ∧ EqOn (fun x => f x i) (g i) s
⊢ ∃ g, LipschitzWith K g ∧ EqOn f g s

Tactic:
refine ⟨fun x i => g i x, LipschitzWith.of_dist_le_mul fun x y => ?_, fun x hx ↦ ?_⟩

Result:
case refine_1
α : Type u
ι : Type x
inst✝¹ : PseudoMetricSpace α
inst✝ : Fintype ι
f : α → ι → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
g : ι → α → ℝ
hg : ∀ (i : ι), LipschitzWith K (g i) ∧ EqOn (fun x => f x i) (g i) s
x y : α
⊢ (dist (fun i => g i x) fun i => g i y) ≤ ↑K * dist x y

case refine_2
α : Type u
ι : Type x
inst✝¹ : PseudoMetricSpace α
inst✝ : Fintype ι
f : α → ι → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
g : ι → α → ℝ
hg : ∀ (i : ι), LipschitzWith K (g i) ∧ EqOn (fun x => f x i) (g i) s
x : α
hx : x ∈ s
⊢ f x = (fun x i => g i x) x

Proof state:
α : Type u
ι : Type x
inst✝¹ : PseudoMetricSpace α
inst✝ : Fintype ι
f : α → ι → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
⊢ ∃ g, LipschitzWith K g ∧ EqOn f g s

Tactic:
have : ∀ i, ∃ g : α → ℝ, LipschitzWith K g ∧ EqOn (fun x => f x i) g s := fun i => by
  have : LipschitzOnWith K (fun x : α => f x i) s :=
    LipschitzOnWith.of_dist_le_mul fun x hx y hy =>
      (dist_le_pi_dist _ _ i).trans (hf.dist_le_mul x hx y hy)
  exact this.extend_real

Result:
α : Type u
ι : Type x
inst✝¹ : PseudoMetricSpace α
inst✝ : Fintype ι
f : α → ι → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
this : ∀ (i : ι), ∃ g, LipschitzWith K g ∧ EqOn (fun x => f x i) g s
⊢ ∃ g, LipschitzWith K g ∧ EqOn f g s

Proof state:
α : Type u
ι : Type x
inst✝¹ : PseudoMetricSpace α
inst✝ : Fintype ι
f : α → ι → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
i : ι
⊢ ∃ g, LipschitzWith K g ∧ EqOn (fun x => f x i) g s

Tactic:
have : LipschitzOnWith K (fun x : α => f x i) s :=
  LipschitzOnWith.of_dist_le_mul fun x hx y hy =>
    (dist_le_pi_dist _ _ i).trans (hf.dist_le_mul x hx y hy)

Result:
α : Type u
ι : Type x
inst✝¹ : PseudoMetricSpace α
inst✝ : Fintype ι
f : α → ι → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
i : ι
this : LipschitzOnWith K (fun x => f x i) s
⊢ ∃ g, LipschitzWith K g ∧ EqOn (fun x => f x i) g s

Proof state:
case refine_2.h
α : Type u
ι : Type x
inst✝¹ : PseudoMetricSpace α
inst✝ : Fintype ι
f : α → ι → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
g : ι → α → ℝ
hg : ∀ (i : ι), LipschitzWith K (g i) ∧ EqOn (fun x => f x i) (g i) s
x : α
hx : x ∈ s
i : ι
⊢ f x i = (fun x i => g i x) x i

Tactic:
exact (hg i).2 hx

Result:
no goals