-- Mathlib/Topology/Algebra/Order/Field.lean
theorem bdd_le_mul_tendsto_zero {f g : α → 𝕜} {b B : 𝕜} (hb : ∀ᶠ x in l, b ≤ f x)
    (hB : ∀ᶠ x in l, f x ≤ B) (hg : Tendsto g l (𝓝 0)) :
    Tendsto (fun x ↦ f x * g x) l (𝓝 0)

Proof state:
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
b B : 𝕜
hb : ∀ᶠ (x : α) in l, b ≤ f x
hB : ∀ᶠ (x : α) in l, f x ≤ B
hg : Tendsto g l (𝓝 0)
C : 𝕜 := |b| ⊔ |B|
hbC : -C ≤ b
⊢ Tendsto (fun x => f x * g x) l (𝓝 0)

Tactic:
have hBC : B ≤ C := le_max_of_le_right (le_abs_self B)

Result:
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
b B : 𝕜
hb : ∀ᶠ (x : α) in l, b ≤ f x
hB : ∀ᶠ (x : α) in l, f x ≤ B
hg : Tendsto g l (𝓝 0)
C : 𝕜 := |b| ⊔ |B|
hbC : -C ≤ b
hBC : B ≤ C
⊢ Tendsto (fun x => f x * g x) l (𝓝 0)

Proof state:
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
b B : 𝕜
hb : ∀ᶠ (x : α) in l, b ≤ f x
hB : ∀ᶠ (x : α) in l, f x ≤ B
hg : Tendsto g l (𝓝 0)
C : 𝕜 := |b| ⊔ |B|
hbC : -C ≤ b
hBC : B ≤ C
⊢ Tendsto (fun x => f x * g x) l (𝓝 0)

Tactic:
apply bdd_le_mul_tendsto_zero' C _ hg

Result:
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
b B : 𝕜
hb : ∀ᶠ (x : α) in l, b ≤ f x
hB : ∀ᶠ (x : α) in l, f x ≤ B
hg : Tendsto g l (𝓝 0)
C : 𝕜 := |b| ⊔ |B|
hbC : -C ≤ b
hBC : B ≤ C
⊢ ∀ᶠ (x : α) in l, |f x| ≤ C

Proof state:
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
b B : 𝕜
hb : ∀ᶠ (x : α) in l, b ≤ f x
hB : ∀ᶠ (x : α) in l, f x ≤ B
hg : Tendsto g l (𝓝 0)
C : 𝕜 := |b| ⊔ |B|
⊢ Tendsto (fun x => f x * g x) l (𝓝 0)

Tactic:
have hbC : -C ≤ b := neg_le.mpr (le_max_of_le_left (neg_le_abs b))

Result:
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
b B : 𝕜
hb : ∀ᶠ (x : α) in l, b ≤ f x
hB : ∀ᶠ (x : α) in l, f x ≤ B
hg : Tendsto g l (𝓝 0)
C : 𝕜 := |b| ⊔ |B|
hbC : -C ≤ b
⊢ Tendsto (fun x => f x * g x) l (𝓝 0)

Proof state:
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
b B : 𝕜
hb : ∀ᶠ (x : α) in l, b ≤ f x
hB : ∀ᶠ (x : α) in l, f x ≤ B
hg : Tendsto g l (𝓝 0)
⊢ Tendsto (fun x => f x * g x) l (𝓝 0)

Tactic:
set C := max |b| |B|

Result:
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
b B : 𝕜
hb : ∀ᶠ (x : α) in l, b ≤ f x
hB : ∀ᶠ (x : α) in l, f x ≤ B
hg : Tendsto g l (𝓝 0)
C : 𝕜 := |b| ⊔ |B|
⊢ Tendsto (fun x => f x * g x) l (𝓝 0)

Proof state:
case h
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
b B : 𝕜
hb : ∀ᶠ (x : α) in l, b ≤ f x
hB : ∀ᶠ (x : α) in l, f x ≤ B
hg : Tendsto g l (𝓝 0)
C : 𝕜 := |b| ⊔ |B|
hbC : -C ≤ b
hBC : B ≤ C
⊢ ∀ (a : α), b ≤ f a → f a ≤ B → |f a| ≤ C

Tactic:
exact fun x hbx hBx ↦ abs_le.mpr ⟨hbC.trans hbx, hBx.trans hBC⟩

Result:
no goals

Proof state:
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
b B : 𝕜
hb : ∀ᶠ (x : α) in l, b ≤ f x
hB : ∀ᶠ (x : α) in l, f x ≤ B
hg : Tendsto g l (𝓝 0)
C : 𝕜 := |b| ⊔ |B|
hbC : -C ≤ b
hBC : B ≤ C
⊢ ∀ᶠ (x : α) in l, |f x| ≤ C

Tactic:
filter_upwards [hb, hB]

Result:
case h
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
b B : 𝕜
hb : ∀ᶠ (x : α) in l, b ≤ f x
hB : ∀ᶠ (x : α) in l, f x ≤ B
hg : Tendsto g l (𝓝 0)
C : 𝕜 := |b| ⊔ |B|
hbC : -C ≤ b
hBC : B ≤ C
⊢ ∀ (a : α), b ≤ f a → f a ≤ B → |f a| ≤ C