-- Mathlib/Analysis/Asymptotics/Lemmas.lean
theorem IsLittleO.smul_isBigO (h₁ : k₁ =o[l] k₂) (h₂ : f' =O[l] g') :
    (fun x => k₁ x • f' x) =o[l] fun x => k₂ x • g' x

Proof state:
α : Type u_1
E' : Type u_6
F' : Type u_7
R : Type u_13
𝕜' : Type u_16
inst✝⁷ : SeminormedAddCommGroup E'
inst✝⁶ : SeminormedAddCommGroup F'
inst✝⁵ : SeminormedRing R
inst✝⁴ : NormedDivisionRing 𝕜'
f' : α → E'
g' : α → F'
l : Filter α
inst✝³ : Module R E'
inst✝² : BoundedSMul R E'
inst✝¹ : Module 𝕜' F'
inst✝ : BoundedSMul 𝕜' F'
k₁ : α → R
k₂ : α → 𝕜'
h₂ : f' =O[l] g'
h₁ : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l k₁ k₂
c : ℝ
cpos : 0 < c
⊢ IsBigOWith c l (fun x => k₁ x • f' x) fun x => k₂ x • g' x

Tactic:
rcases h₂.exists_pos with ⟨c', c'pos, hc'⟩

Result:
case intro.intro
α : Type u_1
E' : Type u_6
F' : Type u_7
R : Type u_13
𝕜' : Type u_16
inst✝⁷ : SeminormedAddCommGroup E'
inst✝⁶ : SeminormedAddCommGroup F'
inst✝⁵ : SeminormedRing R
inst✝⁴ : NormedDivisionRing 𝕜'
f' : α → E'
g' : α → F'
l : Filter α
inst✝³ : Module R E'
inst✝² : BoundedSMul R E'
inst✝¹ : Module 𝕜' F'
inst✝ : BoundedSMul 𝕜' F'
k₁ : α → R
k₂ : α → 𝕜'
h₂ : f' =O[l] g'
h₁ : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l k₁ k₂
c : ℝ
cpos : 0 < c
c' : ℝ
c'pos : c' > 0
hc' : IsBigOWith c' l f' g'
⊢ IsBigOWith c l (fun x => k₁ x • f' x) fun x => k₂ x • g' x

Proof state:
α : Type u_1
E' : Type u_6
F' : Type u_7
R : Type u_13
𝕜' : Type u_16
inst✝⁷ : SeminormedAddCommGroup E'
inst✝⁶ : SeminormedAddCommGroup F'
inst✝⁵ : SeminormedRing R
inst✝⁴ : NormedDivisionRing 𝕜'
f' : α → E'
g' : α → F'
l : Filter α
inst✝³ : Module R E'
inst✝² : BoundedSMul R E'
inst✝¹ : Module 𝕜' F'
inst✝ : BoundedSMul 𝕜' F'
k₁ : α → R
k₂ : α → 𝕜'
h₂ : f' =O[l] g'
h₁ : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l k₁ k₂
⊢ ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l (fun x => k₁ x • f' x) fun x => k₂ x • g' x

Tactic:
intro c cpos

Result:
α : Type u_1
E' : Type u_6
F' : Type u_7
R : Type u_13
𝕜' : Type u_16
inst✝⁷ : SeminormedAddCommGroup E'
inst✝⁶ : SeminormedAddCommGroup F'
inst✝⁵ : SeminormedRing R
inst✝⁴ : NormedDivisionRing 𝕜'
f' : α → E'
g' : α → F'
l : Filter α
inst✝³ : Module R E'
inst✝² : BoundedSMul R E'
inst✝¹ : Module 𝕜' F'
inst✝ : BoundedSMul 𝕜' F'
k₁ : α → R
k₂ : α → 𝕜'
h₂ : f' =O[l] g'
h₁ : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l k₁ k₂
c : ℝ
cpos : 0 < c
⊢ IsBigOWith c l (fun x => k₁ x • f' x) fun x => k₂ x • g' x

Proof state:
case intro.intro
α : Type u_1
E' : Type u_6
F' : Type u_7
R : Type u_13
𝕜' : Type u_16
inst✝⁷ : SeminormedAddCommGroup E'
inst✝⁶ : SeminormedAddCommGroup F'
inst✝⁵ : SeminormedRing R
inst✝⁴ : NormedDivisionRing 𝕜'
f' : α → E'
g' : α → F'
l : Filter α
inst✝³ : Module R E'
inst✝² : BoundedSMul R E'
inst✝¹ : Module 𝕜' F'
inst✝ : BoundedSMul 𝕜' F'
k₁ : α → R
k₂ : α → 𝕜'
h₂ : f' =O[l] g'
h₁ : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l k₁ k₂
c : ℝ
cpos : 0 < c
c' : ℝ
c'pos : c' > 0
hc' : IsBigOWith c' l f' g'
⊢ IsBigOWith c l (fun x => k₁ x • f' x) fun x => k₂ x • g' x

Tactic:
exact ((h₁ (div_pos cpos c'pos)).smul hc').congr_const (div_mul_cancel₀ _ (ne_of_gt c'pos))

Result:
no goals

Proof state:
α : Type u_1
E' : Type u_6
F' : Type u_7
R : Type u_13
𝕜' : Type u_16
inst✝⁷ : SeminormedAddCommGroup E'
inst✝⁶ : SeminormedAddCommGroup F'
inst✝⁵ : SeminormedRing R
inst✝⁴ : NormedDivisionRing 𝕜'
f' : α → E'
g' : α → F'
l : Filter α
inst✝³ : Module R E'
inst✝² : BoundedSMul R E'
inst✝¹ : Module 𝕜' F'
inst✝ : BoundedSMul 𝕜' F'
k₁ : α → R
k₂ : α → 𝕜'
h₁ : k₁ =o[l] k₂
h₂ : f' =O[l] g'
⊢ (fun x => k₁ x • f' x) =o[l] fun x => k₂ x • g' x

Tactic:
simp only [IsLittleO_def] at *

Result:
α : Type u_1
E' : Type u_6
F' : Type u_7
R : Type u_13
𝕜' : Type u_16
inst✝⁷ : SeminormedAddCommGroup E'
inst✝⁶ : SeminormedAddCommGroup F'
inst✝⁵ : SeminormedRing R
inst✝⁴ : NormedDivisionRing 𝕜'
f' : α → E'
g' : α → F'
l : Filter α
inst✝³ : Module R E'
inst✝² : BoundedSMul R E'
inst✝¹ : Module 𝕜' F'
inst✝ : BoundedSMul 𝕜' F'
k₁ : α → R
k₂ : α → 𝕜'
h₂ : f' =O[l] g'
h₁ : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l k₁ k₂
⊢ ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l (fun x => k₁ x • f' x) fun x => k₂ x • g' x