-- Mathlib/Analysis/Normed/Group/Uniform.lean
@[to_additive CauchySeq.norm_bddAbove]
lemma CauchySeq.mul_norm_bddAbove {G : Type*} [SeminormedGroup G] {u : ℕ → G}
    (hu : CauchySeq u) : BddAbove (Set.range (fun n ↦ ‖u n‖))

Proof state:
G : Type u_4
inst✝ : SeminormedGroup G
u : ℕ → G
hu : CauchySeq u
C : ℝ
hC : ∀ (m n : ℕ), ‖u m / u n‖ < C
n : ℕ
⊢ ‖u n‖ ≤ C + ‖u 0‖

Tactic:
rw [add_comm]

Result:
G : Type u_4
inst✝ : SeminormedGroup G
u : ℕ → G
hu : CauchySeq u
C : ℝ
hC : ∀ (m n : ℕ), ‖u m / u n‖ < C
n : ℕ
⊢ ‖u n‖ ≤ ‖u 0‖ + C

Proof state:
G : Type u_4
inst✝ : SeminormedGroup G
u : ℕ → G
hu : CauchySeq u
⊢ BddAbove (Set.range fun n => ‖u n‖)

Tactic:
obtain ⟨C, -, hC⟩ := cauchySeq_bdd hu

Result:
case intro.intro
G : Type u_4
inst✝ : SeminormedGroup G
u : ℕ → G
hu : CauchySeq u
C : ℝ
hC : ∀ (m n : ℕ), dist (u m) (u n) < C
⊢ BddAbove (Set.range fun n => ‖u n‖)

Proof state:
case intro.intro
G : Type u_4
inst✝ : SeminormedGroup G
u : ℕ → G
hu : CauchySeq u
C : ℝ
hC : ∀ (m n : ℕ), ‖u m / u n‖ < C
this : ∀ (n : ℕ), ‖u n‖ ≤ C + ‖u 0‖
⊢ ∃ x, ∀ y ∈ Set.range fun n => ‖u n‖, y ≤ x

Tactic:
exact ⟨C + ‖u 0‖, by simpa using this⟩

Result:
no goals

Proof state:
case intro.intro
G : Type u_4
inst✝ : SeminormedGroup G
u : ℕ → G
hu : CauchySeq u
C : ℝ
hC : ∀ (m n : ℕ), ‖u m / u n‖ < C
this : ∀ (n : ℕ), ‖u n‖ ≤ C + ‖u 0‖
⊢ BddAbove (Set.range fun n => ‖u n‖)

Tactic:
rw [bddAbove_def]

Result:
case intro.intro
G : Type u_4
inst✝ : SeminormedGroup G
u : ℕ → G
hu : CauchySeq u
C : ℝ
hC : ∀ (m n : ℕ), ‖u m / u n‖ < C
this : ∀ (n : ℕ), ‖u n‖ ≤ C + ‖u 0‖
⊢ ∃ x, ∀ y ∈ Set.range fun n => ‖u n‖, y ≤ x

Proof state:
case intro.intro
G : Type u_4
inst✝ : SeminormedGroup G
u : ℕ → G
hu : CauchySeq u
C : ℝ
hC : ∀ (m n : ℕ), dist (u m) (u n) < C
⊢ BddAbove (Set.range fun n => ‖u n‖)

Tactic:
simp_rw [SeminormedGroup.dist_eq] at hC

Result:
case intro.intro
G : Type u_4
inst✝ : SeminormedGroup G
u : ℕ → G
hu : CauchySeq u
C : ℝ
hC : ∀ (m n : ℕ), ‖u m / u n‖ < C
⊢ BddAbove (Set.range fun n => ‖u n‖)

Proof state:
case intro.intro
G : Type u_4
inst✝ : SeminormedGroup G
u : ℕ → G
hu : CauchySeq u
C : ℝ
hC : ∀ (m n : ℕ), ‖u m / u n‖ < C
⊢ BddAbove (Set.range fun n => ‖u n‖)

Tactic:
have : ∀ n, ‖u n‖ ≤ C + ‖u 0‖ := by
  intro n
  rw [add_comm]
  refine (norm_le_norm_add_norm_div' (u n) (u 0)).trans ?_
  simp [(hC _ _).le]

Result:
case intro.intro
G : Type u_4
inst✝ : SeminormedGroup G
u : ℕ → G
hu : CauchySeq u
C : ℝ
hC : ∀ (m n : ℕ), ‖u m / u n‖ < C
this : ∀ (n : ℕ), ‖u n‖ ≤ C + ‖u 0‖
⊢ BddAbove (Set.range fun n => ‖u n‖)

Proof state:
G : Type u_4
inst✝ : SeminormedGroup G
u : ℕ → G
hu : CauchySeq u
C : ℝ
hC : ∀ (m n : ℕ), ‖u m / u n‖ < C
n : ℕ
⊢ ‖u 0‖ + ‖u n / u 0‖ ≤ ‖u 0‖ + C

Tactic:
simp [(hC _ _).le]

Result:
no goals

Proof state:
G : Type u_4
inst✝ : SeminormedGroup G
u : ℕ → G
hu : CauchySeq u
C : ℝ
hC : ∀ (m n : ℕ), ‖u m / u n‖ < C
this : ∀ (n : ℕ), ‖u n‖ ≤ C + ‖u 0‖
⊢ ∀ y ∈ Set.range fun n => ‖u n‖, y ≤ C + ‖u 0‖

Tactic:
simpa using this

Result:
no goals

Proof state:
G : Type u_4
inst✝ : SeminormedGroup G
u : ℕ → G
hu : CauchySeq u
C : ℝ
hC : ∀ (m n : ℕ), ‖u m / u n‖ < C
⊢ ∀ (n : ℕ), ‖u n‖ ≤ C + ‖u 0‖

Tactic:
intro n

Result:
G : Type u_4
inst✝ : SeminormedGroup G
u : ℕ → G
hu : CauchySeq u
C : ℝ
hC : ∀ (m n : ℕ), ‖u m / u n‖ < C
n : ℕ
⊢ ‖u n‖ ≤ C + ‖u 0‖

Proof state:
G : Type u_4
inst✝ : SeminormedGroup G
u : ℕ → G
hu : CauchySeq u
C : ℝ
hC : ∀ (m n : ℕ), ‖u m / u n‖ < C
n : ℕ
⊢ ‖u n‖ ≤ ‖u 0‖ + C

Tactic:
refine (norm_le_norm_add_norm_div' (u n) (u 0)).trans ?_

Result:
G : Type u_4
inst✝ : SeminormedGroup G
u : ℕ → G
hu : CauchySeq u
C : ℝ
hC : ∀ (m n : ℕ), ‖u m / u n‖ < C
n : ℕ
⊢ ‖u 0‖ + ‖u n / u 0‖ ≤ ‖u 0‖ + C