-- Mathlib/Topology/EMetricSpace/Lipschitz.lean
/-- If `f` and `g` are locally Lipschitz, so is the induced map `f × g` to the product type. -/
protected lemma prod {f : α → β} (hf : LocallyLipschitz f) {g : α → γ} (hg : LocallyLipschitz g) :
    LocallyLipschitz fun x => (f x, g x)

Proof state:
case intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
f : α → β
hf : LocallyLipschitz f
g : α → γ
hg : LocallyLipschitz g
x : α
Kf : ℝ≥0
t₁ : Set α
h₁t : t₁ ∈ 𝓝 x
hfL : LipschitzOnWith Kf f t₁
Kg : ℝ≥0
t₂ : Set α
h₂t : t₂ ∈ 𝓝 x
hgL : LipschitzOnWith Kg g t₂
⊢ ∃ K, ∃ t ∈ 𝓝 x, LipschitzOnWith K (fun x => (f x, g x)) t

Tactic:
refine ⟨max Kf Kg, t₁ ∩ t₂, Filter.inter_mem h₁t h₂t, ?_⟩

Result:
case intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
f : α → β
hf : LocallyLipschitz f
g : α → γ
hg : LocallyLipschitz g
x : α
Kf : ℝ≥0
t₁ : Set α
h₁t : t₁ ∈ 𝓝 x
hfL : LipschitzOnWith Kf f t₁
Kg : ℝ≥0
t₂ : Set α
h₂t : t₂ ∈ 𝓝 x
hgL : LipschitzOnWith Kg g t₂
⊢ LipschitzOnWith (Kf ⊔ Kg) (fun x => (f x, g x)) (t₁ ∩ t₂)

Proof state:
case intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
f : α → β
hf : LocallyLipschitz f
g : α → γ
hg : LocallyLipschitz g
x : α
Kf : ℝ≥0
t₁ : Set α
h₁t : t₁ ∈ 𝓝 x
hfL : LipschitzOnWith Kf f t₁
⊢ ∃ K, ∃ t ∈ 𝓝 x, LipschitzOnWith K (fun x => (f x, g x)) t

Tactic:
rcases hg x with ⟨Kg, t₂, h₂t, hgL⟩

Result:
case intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
f : α → β
hf : LocallyLipschitz f
g : α → γ
hg : LocallyLipschitz g
x : α
Kf : ℝ≥0
t₁ : Set α
h₁t : t₁ ∈ 𝓝 x
hfL : LipschitzOnWith Kf f t₁
Kg : ℝ≥0
t₂ : Set α
h₂t : t₂ ∈ 𝓝 x
hgL : LipschitzOnWith Kg g t₂
⊢ ∃ K, ∃ t ∈ 𝓝 x, LipschitzOnWith K (fun x => (f x, g x)) t

Proof state:
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
f : α → β
hf : LocallyLipschitz f
g : α → γ
hg : LocallyLipschitz g
x : α
⊢ ∃ K, ∃ t ∈ 𝓝 x, LipschitzOnWith K (fun x => (f x, g x)) t

Tactic:
rcases hf x with ⟨Kf, t₁, h₁t, hfL⟩

Result:
case intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
f : α → β
hf : LocallyLipschitz f
g : α → γ
hg : LocallyLipschitz g
x : α
Kf : ℝ≥0
t₁ : Set α
h₁t : t₁ ∈ 𝓝 x
hfL : LipschitzOnWith Kf f t₁
⊢ ∃ K, ∃ t ∈ 𝓝 x, LipschitzOnWith K (fun x => (f x, g x)) t

Proof state:
case intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
f : α → β
hf : LocallyLipschitz f
g : α → γ
hg : LocallyLipschitz g
x : α
Kf : ℝ≥0
t₁ : Set α
h₁t : t₁ ∈ 𝓝 x
hfL : LipschitzOnWith Kf f t₁
Kg : ℝ≥0
t₂ : Set α
h₂t : t₂ ∈ 𝓝 x
hgL : LipschitzOnWith Kg g t₂
⊢ LipschitzOnWith (Kf ⊔ Kg) (fun x => (f x, g x)) (t₁ ∩ t₂)

Tactic:
exact (hfL.mono inter_subset_left).prod (hgL.mono inter_subset_right)

Result:
no goals

Proof state:
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
f : α → β
hf : LocallyLipschitz f
g : α → γ
hg : LocallyLipschitz g
⊢ LocallyLipschitz fun x => (f x, g x)

Tactic:
intro x

Result:
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
f : α → β
hf : LocallyLipschitz f
g : α → γ
hg : LocallyLipschitz g
x : α
⊢ ∃ K, ∃ t ∈ 𝓝 x, LipschitzOnWith K (fun x => (f x, g x)) t