-- Mathlib/Topology/EMetricSpace/Lipschitz.lean
theorem continuousOn_prod_of_subset_closure_continuousOn_lipschitzOnWith [PseudoEMetricSpace α]
    [TopologicalSpace β] [PseudoEMetricSpace γ] (f : α × β → γ) {s s' : Set α} {t : Set β}
    (hs' : s' ⊆ s) (hss' : s ⊆ closure s') (K : ℝ≥0)
    (ha : ∀ a ∈ s', ContinuousOn (fun y => f (a, y)) t)
    (hb : ∀ b ∈ t, LipschitzOnWith K (fun x => f (x, b)) s) : ContinuousOn f (s ×ˢ t)

Proof state:
case mk.intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoEMetricSpace γ
f : α × β → γ
s s' : Set α
t : Set β
hs' : s' ⊆ s
hss' : s ⊆ closure s'
K : ℝ≥0
ha : ∀ a ∈ s', ContinuousOn (fun y => f (a, y)) t
hb : ∀ b ∈ t, LipschitzOnWith K (fun x => f (x, b)) s
x : α
y : β
hx : x ∈ s
hy : y ∈ t
ε : ℝ≥0∞
ε0 : 0 < ε / 2
δ : ℝ≥0
δpos : 0 < ↑δ
hδ : ↑δ * ↑(3 * K) < ε / 2
x' : α
hx' : x' ∈ s'
hxx' : edist x x' < ↑δ
A : s ∩ EMetric.ball x ↑δ ∈ 𝓝[s] x
⊢ ∀ᶠ (x_1 : α × β) in 𝓝[s ×ˢ t] (x, y), f x_1 ∈ EMetric.closedBall (f (x, y)) ε

Tactic:
have B : t ∩ { b | edist (f (x', b)) (f (x', y)) ≤ ε / 2 } ∈ 𝓝[t] y :=
  inter_mem self_mem_nhdsWithin (ha x' hx' y hy (EMetric.closedBall_mem_nhds (f (x', y)) ε0))

Result:
case mk.intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoEMetricSpace γ
f : α × β → γ
s s' : Set α
t : Set β
hs' : s' ⊆ s
hss' : s ⊆ closure s'
K : ℝ≥0
ha : ∀ a ∈ s', ContinuousOn (fun y => f (a, y)) t
hb : ∀ b ∈ t, LipschitzOnWith K (fun x => f (x, b)) s
x : α
y : β
hx : x ∈ s
hy : y ∈ t
ε : ℝ≥0∞
ε0 : 0 < ε / 2
δ : ℝ≥0
δpos : 0 < ↑δ
hδ : ↑δ * ↑(3 * K) < ε / 2
x' : α
hx' : x' ∈ s'
hxx' : edist x x' < ↑δ
A : s ∩ EMetric.ball x ↑δ ∈ 𝓝[s] x
B : t ∩ {b | edist (f (x', b)) (f (x', y)) ≤ ε / 2} ∈ 𝓝[t] y
⊢ ∀ᶠ (x_1 : α × β) in 𝓝[s ×ˢ t] (x, y), f x_1 ∈ EMetric.closedBall (f (x, y)) ε

Proof state:
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoEMetricSpace γ
f : α × β → γ
s s' : Set α
t : Set β
hs' : s' ⊆ s
hss' : s ⊆ closure s'
K : ℝ≥0
ha : ∀ a ∈ s', ContinuousOn (fun y => f (a, y)) t
hb : ∀ b ∈ t, LipschitzOnWith K (fun x => f (x, b)) s
x : α
y : β
hx : x ∈ s
hy : y ∈ t
ε : ℝ≥0∞
ε0 : 0 < ε / 2
δ : ℝ≥0
δpos : 0 < ↑δ
hδ : ↑δ * ↑(3 * K) < ε / 2
x' : α
hx' : x' ∈ s'
hxx' : edist x x' < ↑δ
A : s ∩ EMetric.ball x ↑δ ∈ 𝓝[s] x
B : t ∩ {b | edist (f (x', b)) (f (x', y)) ≤ ε / 2} ∈ 𝓝[t] y
a : α
b : β
has : (a, b).1 ∈ s
hax : (a, b).1 ∈ EMetric.ball x ↑δ
hbt : (a, b).2 ∈ t
hby : (a, b).2 ∈ {b | edist (f (x', b)) (f (x', y)) ≤ ε / 2}
⊢ ↑K * (↑δ + ↑δ) + ε / 2 + ↑K * ↑δ = ↑δ * (3 * ↑K) + ε / 2

Tactic:
ring

Result:
no goals

Proof state:
case mk.intro
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoEMetricSpace γ
f : α × β → γ
s s' : Set α
t : Set β
hs' : s' ⊆ s
hss' : s ⊆ closure s'
K : ℝ≥0
ha : ∀ a ∈ s', ContinuousOn (fun y => f (a, y)) t
hb : ∀ b ∈ t, LipschitzOnWith K (fun x => f (x, b)) s
x : α
y : β
hx : x ∈ s
hy : y ∈ t
⊢ ContinuousWithinAt f (s ×ˢ t) (x, y)

Tactic:
refine EMetric.nhds_basis_closed_eball.tendsto_right_iff.2 fun ε (ε0 : 0 < ε) => ?_

Result:
case mk.intro
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoEMetricSpace γ
f : α × β → γ
s s' : Set α
t : Set β
hs' : s' ⊆ s
hss' : s ⊆ closure s'
K : ℝ≥0
ha : ∀ a ∈ s', ContinuousOn (fun y => f (a, y)) t
hb : ∀ b ∈ t, LipschitzOnWith K (fun x => f (x, b)) s
x : α
y : β
hx : x ∈ s
hy : y ∈ t
ε : ℝ≥0∞
ε0 : 0 < ε
⊢ ∀ᶠ (x_1 : α × β) in 𝓝[s ×ˢ t] (x, y), f x_1 ∈ EMetric.closedBall (f (x, y)) ε

Proof state:
case h₂
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoEMetricSpace γ
f : α × β → γ
s s' : Set α
t : Set β
hs' : s' ⊆ s
hss' : s ⊆ closure s'
K : ℝ≥0
ha : ∀ a ∈ s', ContinuousOn (fun y => f (a, y)) t
hb : ∀ b ∈ t, LipschitzOnWith K (fun x => f (x, b)) s
x : α
y : β
hx : x ∈ s
hy : y ∈ t
ε : ℝ≥0∞
ε0 : 0 < ε / 2
δ : ℝ≥0
δpos : 0 < ↑δ
hδ : ↑δ * ↑(3 * K) < ε / 2
x' : α
hx' : x' ∈ s'
hxx' : edist x x' < ↑δ
A : s ∩ EMetric.ball x ↑δ ∈ 𝓝[s] x
B : t ∩ {b | edist (f (x', b)) (f (x', y)) ≤ ε / 2} ∈ 𝓝[t] y
a : α
b : β
has : (a, b).1 ∈ s
hax : (a, b).1 ∈ EMetric.ball x ↑δ
hbt : (a, b).2 ∈ t
hby : (a, b).2 ∈ {b | edist (f (x', b)) (f (x', y)) ≤ ε / 2}
⊢ edist (f (x', y)) (f (x, y)) ≤ ↑K * ↑δ

Tactic:
exact (hb y hy).edist_le_mul_of_le (hs' hx') hx ((edist_comm _ _).trans_le hxx'.le)

Result:
no goals

Proof state:
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoEMetricSpace γ
f : α × β → γ
s s' : Set α
t : Set β
hs' : s' ⊆ s
hss' : s ⊆ closure s'
K : ℝ≥0
ha : ∀ a ∈ s', ContinuousOn (fun y => f (a, y)) t
hb : ∀ b ∈ t, LipschitzOnWith K (fun x => f (x, b)) s
x : α
y : β
hx : x ∈ s
hy : y ∈ t
ε : ℝ≥0∞
ε0 : 0 < ε / 2
δ : ℝ≥0
δpos : 0 < ↑δ
hδ : ↑δ * ↑(3 * K) < ε / 2
x' : α
hx' : x' ∈ s'
hxx' : edist x x' < ↑δ
A : s ∩ EMetric.ball x ↑δ ∈ 𝓝[s] x
B : t ∩ {b | edist (f (x', b)) (f (x', y)) ≤ ε / 2} ∈ 𝓝[t] y
a : α
b : β
has : (a, b).1 ∈ s
hax : (a, b).1 ∈ EMetric.ball x ↑δ
hbt : (a, b).2 ∈ t
hby : (a, b).2 ∈ {b | edist (f (x', b)) (f (x', y)) ≤ ε / 2}
⊢ ↑δ * ↑(3 * K) + ε / 2 ≤ ε / 2 + ε / 2

Tactic:
gcongr

Result:
no goals