-- Mathlib/Analysis/Normed/Lp/lpSpace.lean
lemma LipschitzWith.uniformly_bounded [PseudoMetricSpace α] (g : α → ι → ℝ) {K : ℝ≥0}
    (hg : ∀ i, LipschitzWith K (g · i)) (a₀ : α) (hga₀b : Memℓp (g a₀) ∞) (a : α) :
    Memℓp (g a) ∞

Proof state:
α : Type u_3
ι : Type u_5
inst✝ : PseudoMetricSpace α
g : α → ι → ℝ
K : ℝ≥0
hg : ∀ (i : ι), LipschitzWith K fun x => g x i
a₀ : α
hga₀b : Memℓp (g a₀) ⊤
a : α
⊢ Memℓp (g a) ⊤

Tactic:
rcases hga₀b with ⟨M, hM⟩

Result:
case intro
α : Type u_3
ι : Type u_5
inst✝ : PseudoMetricSpace α
g : α → ι → ℝ
K : ℝ≥0
hg : ∀ (i : ι), LipschitzWith K fun x => g x i
a₀ a : α
M : ℝ
hM : M ∈ upperBounds (Set.range fun i => ‖g a₀ i‖)
⊢ Memℓp (g a) ⊤

Proof state:
α : Type u_3
ι : Type u_5
inst✝ : PseudoMetricSpace α
g : α → ι → ℝ
K : ℝ≥0
hg : ∀ (i : ι), LipschitzWith K fun x => g x i
a₀ a : α
M : ℝ
hM : M ∈ upperBounds (Set.range fun i => ‖g a₀ i‖)
i : ι
⊢ |g a i| = |g a i - g a₀ i + g a₀ i|

Tactic:
simp

Result:
no goals

Proof state:
case h
α : Type u_3
ι : Type u_5
inst✝ : PseudoMetricSpace α
g : α → ι → ℝ
K : ℝ≥0
hg : ∀ (i : ι), LipschitzWith K fun x => g x i
a₀ a : α
M : ℝ
hM : M ∈ upperBounds (Set.range fun i => ‖g a₀ i‖)
⊢ ↑K * dist a a₀ + M ∈ upperBounds (Set.range fun i => ‖g a i‖)

Tactic:
rintro - ⟨i, rfl⟩

Result:
case h.intro
α : Type u_3
ι : Type u_5
inst✝ : PseudoMetricSpace α
g : α → ι → ℝ
K : ℝ≥0
hg : ∀ (i : ι), LipschitzWith K fun x => g x i
a₀ a : α
M : ℝ
hM : M ∈ upperBounds (Set.range fun i => ‖g a₀ i‖)
i : ι
⊢ (fun i => ‖g a i‖) i ≤ ↑K * dist a a₀ + M

Proof state:
case h₂
α : Type u_3
ι : Type u_5
inst✝ : PseudoMetricSpace α
g : α → ι → ℝ
K : ℝ≥0
hg : ∀ (i : ι), LipschitzWith K fun x => g x i
a₀ a : α
M : ℝ
hM : M ∈ upperBounds (Set.range fun i => ‖g a₀ i‖)
i : ι
⊢ |g a₀ i| ≤ M

Tactic:
exact hM ⟨i, rfl⟩

Result:
no goals

Proof state:
α : Type u_3
ι : Type u_5
inst✝ : PseudoMetricSpace α
g : α → ι → ℝ
K : ℝ≥0
hg : ∀ (i : ι), LipschitzWith K fun x => g x i
a₀ a : α
M : ℝ
hM : M ∈ upperBounds (Set.range fun i => ‖g a₀ i‖)
i : ι
⊢ |g a i - g a₀ i| + |g a₀ i| ≤ ↑K * dist a a₀ + M

Tactic:
gcongr

Result:
case h₁
α : Type u_3
ι : Type u_5
inst✝ : PseudoMetricSpace α
g : α → ι → ℝ
K : ℝ≥0
hg : ∀ (i : ι), LipschitzWith K fun x => g x i
a₀ a : α
M : ℝ
hM : M ∈ upperBounds (Set.range fun i => ‖g a₀ i‖)
i : ι
⊢ |g a i - g a₀ i| ≤ ↑K * dist a a₀

case h₂
α : Type u_3
ι : Type u_5
inst✝ : PseudoMetricSpace α
g : α → ι → ℝ
K : ℝ≥0
hg : ∀ (i : ι), LipschitzWith K fun x => g x i
a₀ a : α
M : ℝ
hM : M ∈ upperBounds (Set.range fun i => ‖g a₀ i‖)
i : ι
⊢ |g a₀ i| ≤ M

Proof state:
case intro
α : Type u_3
ι : Type u_5
inst✝ : PseudoMetricSpace α
g : α → ι → ℝ
K : ℝ≥0
hg : ∀ (i : ι), LipschitzWith K fun x => g x i
a₀ a : α
M : ℝ
hM : M ∈ upperBounds (Set.range fun i => ‖g a₀ i‖)
⊢ Memℓp (g a) ⊤

Tactic:
use ↑K * dist a a₀ + M

Result:
case h
α : Type u_3
ι : Type u_5
inst✝ : PseudoMetricSpace α
g : α → ι → ℝ
K : ℝ≥0
hg : ∀ (i : ι), LipschitzWith K fun x => g x i
a₀ a : α
M : ℝ
hM : M ∈ upperBounds (Set.range fun i => ‖g a₀ i‖)
⊢ ↑K * dist a a₀ + M ∈ upperBounds (Set.range fun i => ‖g a i‖)

Proof state:
case h₁
α : Type u_3
ι : Type u_5
inst✝ : PseudoMetricSpace α
g : α → ι → ℝ
K : ℝ≥0
hg : ∀ (i : ι), LipschitzWith K fun x => g x i
a₀ a : α
M : ℝ
hM : M ∈ upperBounds (Set.range fun i => ‖g a₀ i‖)
i : ι
⊢ |g a i - g a₀ i| ≤ ↑K * dist a a₀

Tactic:
exact lipschitzWith_iff_dist_le_mul.1 (hg i) a a₀

Result:
no goals