-- Mathlib/Topology/Bornology/BoundedOperation.lean
lemma add_bounded_of_bounded_of_bounded {X : Type*} [PseudoMetricSpace R] [Add R] [BoundedAdd R]
    {f g : X → R} (f_bdd : ∃ C, ∀ x y, dist (f x) (f y) ≤ C)
    (g_bdd : ∃ C, ∀ x y, dist (g x) (g y) ≤ C) :
    ∃ C, ∀ x y, dist ((f + g) x) ((f + g) y) ≤ C

Proof state:
R : Type u_1
X : Type u_2
inst✝² : PseudoMetricSpace R
inst✝¹ : Add R
inst✝ : BoundedAdd R
f g : X → R
f_bdd : ∃ C, ∀ (x y : X), dist (f x) (f y) ≤ C
g_bdd : ∃ C, ∀ (x y : X), dist (g x) (g y) ≤ C
⊢ ∃ C, ∀ (x y : X), dist ((f + g) x) ((f + g) y) ≤ C

Tactic:
obtain ⟨C, hC⟩ := Metric.isBounded_iff.mp <|
  isBounded_add (Metric.isBounded_range_iff.mpr f_bdd) (Metric.isBounded_range_iff.mpr g_bdd)

Result:
case intro
R : Type u_1
X : Type u_2
inst✝² : PseudoMetricSpace R
inst✝¹ : Add R
inst✝ : BoundedAdd R
f g : X → R
f_bdd : ∃ C, ∀ (x y : X), dist (f x) (f y) ≤ C
g_bdd : ∃ C, ∀ (x y : X), dist (g x) (g y) ≤ C
C : ℝ
hC : ∀ ⦃x : R⦄, x ∈ Set.range f + Set.range g → ∀ ⦃y : R⦄, y ∈ Set.range f + Set.range g → dist x y ≤ C
⊢ ∃ C, ∀ (x y : X), dist ((f + g) x) ((f + g) y) ≤ C

Proof state:
case h
R : Type u_1
X : Type u_2
inst✝² : PseudoMetricSpace R
inst✝¹ : Add R
inst✝ : BoundedAdd R
f g : X → R
f_bdd : ∃ C, ∀ (x y : X), dist (f x) (f y) ≤ C
g_bdd : ∃ C, ∀ (x y : X), dist (g x) (g y) ≤ C
C : ℝ
hC : ∀ ⦃x : R⦄, x ∈ Set.range f + Set.range g → ∀ ⦃y : R⦄, y ∈ Set.range f + Set.range g → dist x y ≤ C
⊢ ∀ (x y : X), dist ((f + g) x) ((f + g) y) ≤ C

Tactic:
intro x y

Result:
case h
R : Type u_1
X : Type u_2
inst✝² : PseudoMetricSpace R
inst✝¹ : Add R
inst✝ : BoundedAdd R
f g : X → R
f_bdd : ∃ C, ∀ (x y : X), dist (f x) (f y) ≤ C
g_bdd : ∃ C, ∀ (x y : X), dist (g x) (g y) ≤ C
C : ℝ
hC : ∀ ⦃x : R⦄, x ∈ Set.range f + Set.range g → ∀ ⦃y : R⦄, y ∈ Set.range f + Set.range g → dist x y ≤ C
x y : X
⊢ dist ((f + g) x) ((f + g) y) ≤ C

Proof state:
case intro
R : Type u_1
X : Type u_2
inst✝² : PseudoMetricSpace R
inst✝¹ : Add R
inst✝ : BoundedAdd R
f g : X → R
f_bdd : ∃ C, ∀ (x y : X), dist (f x) (f y) ≤ C
g_bdd : ∃ C, ∀ (x y : X), dist (g x) (g y) ≤ C
C : ℝ
hC : ∀ ⦃x : R⦄, x ∈ Set.range f + Set.range g → ∀ ⦃y : R⦄, y ∈ Set.range f + Set.range g → dist x y ≤ C
⊢ ∃ C, ∀ (x y : X), dist ((f + g) x) ((f + g) y) ≤ C

Tactic:
use C

Result:
case h
R : Type u_1
X : Type u_2
inst✝² : PseudoMetricSpace R
inst✝¹ : Add R
inst✝ : BoundedAdd R
f g : X → R
f_bdd : ∃ C, ∀ (x y : X), dist (f x) (f y) ≤ C
g_bdd : ∃ C, ∀ (x y : X), dist (g x) (g y) ≤ C
C : ℝ
hC : ∀ ⦃x : R⦄, x ∈ Set.range f + Set.range g → ∀ ⦃y : R⦄, y ∈ Set.range f + Set.range g → dist x y ≤ C
⊢ ∀ (x y : X), dist ((f + g) x) ((f + g) y) ≤ C

Proof state:
case h
R : Type u_1
X : Type u_2
inst✝² : PseudoMetricSpace R
inst✝¹ : Add R
inst✝ : BoundedAdd R
f g : X → R
f_bdd : ∃ C, ∀ (x y : X), dist (f x) (f y) ≤ C
g_bdd : ∃ C, ∀ (x y : X), dist (g x) (g y) ≤ C
C : ℝ
hC : ∀ ⦃x : R⦄, x ∈ Set.range f + Set.range g → ∀ ⦃y : R⦄, y ∈ Set.range f + Set.range g → dist x y ≤ C
x y : X
⊢ dist ((f + g) x) ((f + g) y) ≤ C

Tactic:
exact hC (Set.add_mem_add (Set.mem_range_self (f := f) x) (Set.mem_range_self (f := g) x))
         (Set.add_mem_add (Set.mem_range_self (f := f) y) (Set.mem_range_self (f := g) y))

Result:
no goals