-- Mathlib/Topology/Algebra/Order/Field.lean
theorem bdd_le_mul_tendsto_zero' {f g : α → 𝕜} (C : 𝕜) (hf : ∀ᶠ x in l, |f x| ≤ C)
    (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 : α → 𝕜
C : 𝕜
hf : ∀ᶠ (x : α) in l, |f x| ≤ C
hg : Tendsto g l (𝓝 0)
hC : Tendsto (fun x => |C * g x|) l (𝓝 0)
⊢ Tendsto (abs ∘ fun x => f x * g x) l (𝓝 0)

Tactic:
apply tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds hC

Result:
case hgf
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hf : ∀ᶠ (x : α) in l, |f x| ≤ C
hg : Tendsto g l (𝓝 0)
hC : Tendsto (fun x => |C * g x|) l (𝓝 0)
⊢ ∀ᶠ (b : α) in l, 0 ≤ (abs ∘ fun x => f x * g x) b

case hfh
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hf : ∀ᶠ (x : α) in l, |f x| ≤ C
hg : Tendsto g l (𝓝 0)
hC : Tendsto (fun x => |C * g x|) l (𝓝 0)
⊢ ∀ᶠ (b : α) in l, (abs ∘ fun x => f x * g x) b ≤ |C * g b|

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

Tactic:
filter_upwards [hf] with x hx

Result:
case h
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hf : ∀ᶠ (x : α) in l, |f x| ≤ C
hg : Tendsto g l (𝓝 0)
hC : Tendsto (fun x => |C * g x|) l (𝓝 0)
x : α
hx : |f x| ≤ C
⊢ (abs ∘ fun x => f x * g x) x ≤ |C * g x|

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

Tactic:
convert (hg.const_mul C).abs

Result:
case h.e'_5.h.e'_3
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hf : ∀ᶠ (x : α) in l, |f x| ≤ C
hg : Tendsto g l (𝓝 0)
⊢ 0 = |C * 0|

Proof state:
case h
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hf : ∀ᶠ (x : α) in l, |f x| ≤ C
hg : Tendsto g l (𝓝 0)
hC : Tendsto (fun x => |C * g x|) l (𝓝 0)
x : α
hx : |f x| ≤ C
⊢ |f x| * |g x| ≤ |C| * |g x|

Tactic:
exact mul_le_mul_of_nonneg_right (hx.trans (le_abs_self C)) (abs_nonneg _)

Result:
no goals

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

Tactic:
have hC : Tendsto (fun x ↦ |C * g x|) l (𝓝 0) := by
  convert (hg.const_mul C).abs
  simp_rw [mul_zero, abs_zero]

Result:
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hf : ∀ᶠ (x : α) in l, |f x| ≤ C
hg : Tendsto g l (𝓝 0)
hC : Tendsto (fun x => |C * g x|) l (𝓝 0)
⊢ Tendsto (abs ∘ 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 : α → 𝕜
C : 𝕜
hf : ∀ᶠ (x : α) in l, |f x| ≤ C
hg : Tendsto g l (𝓝 0)
⊢ Tendsto (fun x => f x * g x) l (𝓝 0)

Tactic:
rw [tendsto_zero_iff_abs_tendsto_zero]

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

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

Tactic:
filter_upwards [hf] with x _ using abs_nonneg _

Result:
no goals

Proof state:
case h
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hf : ∀ᶠ (x : α) in l, |f x| ≤ C
hg : Tendsto g l (𝓝 0)
hC : Tendsto (fun x => |C * g x|) l (𝓝 0)
x : α
hx : |f x| ≤ C
⊢ (abs ∘ fun x => f x * g x) x ≤ |C * g x|

Tactic:
simp only [comp_apply, abs_mul]

Result:
case h
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hf : ∀ᶠ (x : α) in l, |f x| ≤ C
hg : Tendsto g l (𝓝 0)
hC : Tendsto (fun x => |C * g x|) l (𝓝 0)
x : α
hx : |f x| ≤ C
⊢ |f x| * |g x| ≤ |C| * |g x|

Proof state:
case h.e'_5.h.e'_3
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hf : ∀ᶠ (x : α) in l, |f x| ≤ C
hg : Tendsto g l (𝓝 0)
⊢ 0 = |C * 0|

Tactic:
simp_rw [mul_zero, abs_zero]

Result:
no goals