case mp
α : Type u_2
β : Type ?u.315708
E : Type ?u.315711
F : Type ?u.315714
G : Type ?u.315717
E' : Type u_3
F' : Type ?u.315723
G' : Type ?u.315726
E'' : Type u_1
F'' : Type ?u.315732
G'' : Type ?u.315735
R : Type ?u.315738
R' : Type ?u.315741
𝕜 : Type ?u.315744
𝕜' : Type ?u.315747
inst✝¹² : Norm E
inst✝¹¹ : Norm F
inst✝¹⁰ : Norm G
inst✝⁹ : SeminormedAddCommGroup E'
inst✝⁸ : SeminormedAddCommGroup F'
inst✝⁷ : SeminormedAddCommGroup G'
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedAddCommGroup F''
inst✝⁴ : NormedAddCommGroup G''
inst✝³ : SeminormedRing R
inst✝² : SeminormedRing R'
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
c✝ c' c₁ c₂ : ℝ
f : α → E
g : α → F
k : α → G
f' : α → E'
g' : α → F'
k' : α → G'
f'' : α → E''
g'' : α → F''
k'' : α → G''
l l' : Filter α
c : E''
hc : c ≠ 0
⊢ (fun _x => c) =O[l] f' → ∃ b, 0 < b ∧ ∀ᶠ (x : α) in l, b ≤ ‖f' x‖

case mpr
α : Type u_2
β : Type ?u.315708
E : Type ?u.315711
F : Type ?u.315714
G : Type ?u.315717
E' : Type u_3
F' : Type ?u.315723
G' : Type ?u.315726
E'' : Type u_1
F'' : Type ?u.315732
G'' : Type ?u.315735
R : Type ?u.315738
R' : Type ?u.315741
𝕜 : Type ?u.315744
𝕜' : Type ?u.315747
inst✝¹² : Norm E
inst✝¹¹ : Norm F
inst✝¹⁰ : Norm G
inst✝⁹ : SeminormedAddCommGroup E'
inst✝⁸ : SeminormedAddCommGroup F'
inst✝⁷ : SeminormedAddCommGroup G'
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedAddCommGroup F''
inst✝⁴ : NormedAddCommGroup G''
inst✝³ : SeminormedRing R
inst✝² : SeminormedRing R'
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
c✝ c' c₁ c₂ : ℝ
f : α → E
g : α → F
k : α → G
f' : α → E'
g' : α → F'
k' : α → G'
f'' : α → E''
g'' : α → F''
k'' : α → G''
l l' : Filter α
c : E''
hc : c ≠ 0
⊢ (∃ b, 0 < b ∧ ∀ᶠ (x : α) in l, b ≤ ‖f' x‖) → (fun _x => c) =O[l] f'
α : Type u_2
β : Type ?u.315708
E : Type ?u.315711
F : Type ?u.315714
G : Type ?u.315717
E' : Type u_3
F' : Type ?u.315723
G' : Type ?u.315726
E'' : Type u_1
F'' : Type ?u.315732
G'' : Type ?u.315735
R : Type ?u.315738
R' : Type ?u.315741
𝕜 : Type ?u.315744
𝕜' : Type ?u.315747
inst✝¹² : Norm E
inst✝¹¹ : Norm F
inst✝¹⁰ : Norm G
inst✝⁹ : SeminormedAddCommGroup E'
inst✝⁸ : SeminormedAddCommGroup F'
inst✝⁷ : SeminormedAddCommGroup G'
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedAddCommGroup F''
inst✝⁴ : NormedAddCommGroup G''
inst✝³ : SeminormedRing R
inst✝² : SeminormedRing R'
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
c✝ c' c₁ c₂ : ℝ
f : α → E
g : α → F
k : α → G
f' : α → E'
g' : α → F'
k' : α → G'
f'' : α → E''
g'' : α → F''
k'' : α → G''
l l' : Filter α
c : E''
hc : c ≠ 0
⊢ (fun _x => c) =O[l] f' ↔ ∃ b, 0 < b ∧ ∀ᶠ (x : α) in l, b ≤ ‖f' x‖
constructor
case mp
α : Type u_2
β : Type ?u.315708
E : Type ?u.315711
F : Type ?u.315714
G : Type ?u.315717
E' : Type u_3
F' : Type ?u.315723
G' : Type ?u.315726
E'' : Type u_1
F'' : Type ?u.315732
G'' : Type ?u.315735
R : Type ?u.315738
R' : Type ?u.315741
𝕜 : Type ?u.315744
𝕜' : Type ?u.315747
inst✝¹² : Norm E
inst✝¹¹ : Norm F
inst✝¹⁰ : Norm G
inst✝⁹ : SeminormedAddCommGroup E'
inst✝⁸ : SeminormedAddCommGroup F'
inst✝⁷ : SeminormedAddCommGroup G'
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedAddCommGroup F''
inst✝⁴ : NormedAddCommGroup G''
inst✝³ : SeminormedRing R
inst✝² : SeminormedRing R'
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
c✝ c' c₁ c₂ : ℝ
f : α → E
g : α → F
k : α → G
f' : α → E'
g' : α → F'
k' : α → G'
f'' : α → E''
g'' : α → F''
k'' : α → G''
l l' : Filter α
c : E''
hc : c ≠ 0
h : (fun _x => c) =O[l] f'
⊢ ∃ b, 0 < b ∧ ∀ᶠ (x : α) in l, b ≤ ‖f' x‖
case mp
α : Type u_2
β : Type ?u.315708
E : Type ?u.315711
F : Type ?u.315714
G : Type ?u.315717
E' : Type u_3
F' : Type ?u.315723
G' : Type ?u.315726
E'' : Type u_1
F'' : Type ?u.315732
G'' : Type ?u.315735
R : Type ?u.315738
R' : Type ?u.315741
𝕜 : Type ?u.315744
𝕜' : Type ?u.315747
inst✝¹² : Norm E
inst✝¹¹ : Norm F
inst✝¹⁰ : Norm G
inst✝⁹ : SeminormedAddCommGroup E'
inst✝⁸ : SeminormedAddCommGroup F'
inst✝⁷ : SeminormedAddCommGroup G'
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedAddCommGroup F''
inst✝⁴ : NormedAddCommGroup G''
inst✝³ : SeminormedRing R
inst✝² : SeminormedRing R'
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
c✝ c' c₁ c₂ : ℝ
f : α → E
g : α → F
k : α → G
f' : α → E'
g' : α → F'
k' : α → G'
f'' : α → E''
g'' : α → F''
k'' : α → G''
l l' : Filter α
c : E''
hc : c ≠ 0
⊢ (fun _x => c) =O[l] f' → ∃ b, 0 < b ∧ ∀ᶠ (x : α) in l, b ≤ ‖f' x‖
intro h
case mp.intro.intro
α : Type u_2
β : Type ?u.315708
E : Type ?u.315711
F : Type ?u.315714
G : Type ?u.315717
E' : Type u_3
F' : Type ?u.315723
G' : Type ?u.315726
E'' : Type u_1
F'' : Type ?u.315732
G'' : Type ?u.315735
R : Type ?u.315738
R' : Type ?u.315741
𝕜 : Type ?u.315744
𝕜' : Type ?u.315747
inst✝¹² : Norm E
inst✝¹¹ : Norm F
inst✝¹⁰ : Norm G
inst✝⁹ : SeminormedAddCommGroup E'
inst✝⁸ : SeminormedAddCommGroup F'
inst✝⁷ : SeminormedAddCommGroup G'
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedAddCommGroup F''
inst✝⁴ : NormedAddCommGroup G''
inst✝³ : SeminormedRing R
inst✝² : SeminormedRing R'
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
c✝ c' c₁ c₂ : ℝ
f : α → E
g : α → F
k : α → G
f' : α → E'
g' : α → F'
k' : α → G'
f'' : α → E''
g'' : α → F''
k'' : α → G''
l l' : Filter α
c : E''
hc : c ≠ 0
h : (fun _x => c) =O[l] f'
C : ℝ
hC₀ : 0 < C
hC : IsBigOWith C l (fun _x => c) f'
⊢ ∃ b, 0 < b ∧ ∀ᶠ (x : α) in l, b ≤ ‖f' x‖
case mp
α : Type u_2
β : Type ?u.315708
E : Type ?u.315711
F : Type ?u.315714
G : Type ?u.315717
E' : Type u_3
F' : Type ?u.315723
G' : Type ?u.315726
E'' : Type u_1
F'' : Type ?u.315732
G'' : Type ?u.315735
R : Type ?u.315738
R' : Type ?u.315741
𝕜 : Type ?u.315744
𝕜' : Type ?u.315747
inst✝¹² : Norm E
inst✝¹¹ : Norm F
inst✝¹⁰ : Norm G
inst✝⁹ : SeminormedAddCommGroup E'
inst✝⁸ : SeminormedAddCommGroup F'
inst✝⁷ : SeminormedAddCommGroup G'
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedAddCommGroup F''
inst✝⁴ : NormedAddCommGroup G''
inst✝³ : SeminormedRing R
inst✝² : SeminormedRing R'
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
c✝ c' c₁ c₂ : ℝ
f : α → E
g : α → F
k : α → G
f' : α → E'
g' : α → F'
k' : α → G'
f'' : α → E''
g'' : α → F''
k'' : α → G''
l l' : Filter α
c : E''
hc : c ≠ 0
h : (fun _x => c) =O[l] f'
⊢ ∃ b, 0 < b ∧ ∀ᶠ (x : α) in l, b ≤ ‖f' x‖
rcases h.exists_pos with ⟨C, hC₀, hC⟩
case mp.intro.intro
α : Type u_2
β : Type ?u.315708
E : Type ?u.315711
F : Type ?u.315714
G : Type ?u.315717
E' : Type u_3
F' : Type ?u.315723
G' : Type ?u.315726
E'' : Type u_1
F'' : Type ?u.315732
G'' : Type ?u.315735
R : Type ?u.315738
R' : Type ?u.315741
𝕜 : Type ?u.315744
𝕜' : Type ?u.315747
inst✝¹² : Norm E
inst✝¹¹ : Norm F
inst✝¹⁰ : Norm G
inst✝⁹ : SeminormedAddCommGroup E'
inst✝⁸ : SeminormedAddCommGroup F'
inst✝⁷ : SeminormedAddCommGroup G'
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedAddCommGroup F''
inst✝⁴ : NormedAddCommGroup G''
inst✝³ : SeminormedRing R
inst✝² : SeminormedRing R'
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
c✝ c' c₁ c₂ : ℝ
f : α → E
g : α → F
k : α → G
f' : α → E'
g' : α → F'
k' : α → G'
f'' : α → E''
g'' : α → F''
k'' : α → G''
l l' : Filter α
c : E''
hc : c ≠ 0
h : (fun _x => c) =O[l] f'
C : ℝ
hC₀ : 0 < C
hC : IsBigOWith C l (fun _x => c) f'
⊢ ∀ᶠ (x : α) in l, ‖c‖ / C ≤ ‖f' x‖
case mp.intro.intro
α : Type u_2
β : Type ?u.315708
E : Type ?u.315711
F : Type ?u.315714
G : Type ?u.315717
E' : Type u_3
F' : Type ?u.315723
G' : Type ?u.315726
E'' : Type u_1
F'' : Type ?u.315732
G'' : Type ?u.315735
R : Type ?u.315738
R' : Type ?u.315741
𝕜 : Type ?u.315744
𝕜' : Type ?u.315747
inst✝¹² : Norm E
inst✝¹¹ : Norm F
inst✝¹⁰ : Norm G
inst✝⁹ : SeminormedAddCommGroup E'
inst✝⁸ : SeminormedAddCommGroup F'
inst✝⁷ : SeminormedAddCommGroup G'
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedAddCommGroup F''
inst✝⁴ : NormedAddCommGroup G''
inst✝³ : SeminormedRing R
inst✝² : SeminormedRing R'
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
c✝ c' c₁ c₂ : ℝ
f : α → E
g : α → F
k : α → G
f' : α → E'
g' : α → F'
k' : α → G'
f'' : α → E''
g'' : α → F''
k'' : α → G''
l l' : Filter α
c : E''
hc : c ≠ 0
h : (fun _x => c) =O[l] f'
C : ℝ
hC₀ : 0 < C
hC : IsBigOWith C l (fun _x => c) f'
⊢ ∃ b, 0 < b ∧ ∀ᶠ (x : α) in l, b ≤ ‖f' x‖
refine' ⟨‖c‖ / C, div_pos (norm_pos_iff.2 hc) hC₀, _⟩
no goals
case mp.intro.intro
α : Type u_2
β : Type ?u.315708
E : Type ?u.315711
F : Type ?u.315714
G : Type ?u.315717
E' : Type u_3
F' : Type ?u.315723
G' : Type ?u.315726
E'' : Type u_1
F'' : Type ?u.315732
G'' : Type ?u.315735
R : Type ?u.315738
R' : Type ?u.315741
𝕜 : Type ?u.315744
𝕜' : Type ?u.315747
inst✝¹² : Norm E
inst✝¹¹ : Norm F
inst✝¹⁰ : Norm G
inst✝⁹ : SeminormedAddCommGroup E'
inst✝⁸ : SeminormedAddCommGroup F'
inst✝⁷ : SeminormedAddCommGroup G'
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedAddCommGroup F''
inst✝⁴ : NormedAddCommGroup G''
inst✝³ : SeminormedRing R
inst✝² : SeminormedRing R'
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
c✝ c' c₁ c₂ : ℝ
f : α → E
g : α → F
k : α → G
f' : α → E'
g' : α → F'
k' : α → G'
f'' : α → E''
g'' : α → F''
k'' : α → G''
l l' : Filter α
c : E''
hc : c ≠ 0
h : (fun _x => c) =O[l] f'
C : ℝ
hC₀ : 0 < C
hC : IsBigOWith C l (fun _x => c) f'
⊢ ∀ᶠ (x : α) in l, ‖c‖ / C ≤ ‖f' x‖
exact hC.bound.mono fun x => (div_le_iff' hC₀).2
case mpr.intro.intro
α : Type u_2
β : Type ?u.315708
E : Type ?u.315711
F : Type ?u.315714
G : Type ?u.315717
E' : Type u_3
F' : Type ?u.315723
G' : Type ?u.315726
E'' : Type u_1
F'' : Type ?u.315732
G'' : Type ?u.315735
R : Type ?u.315738
R' : Type ?u.315741
𝕜 : Type ?u.315744
𝕜' : Type ?u.315747
inst✝¹² : Norm E
inst✝¹¹ : Norm F
inst✝¹⁰ : Norm G
inst✝⁹ : SeminormedAddCommGroup E'
inst✝⁸ : SeminormedAddCommGroup F'
inst✝⁷ : SeminormedAddCommGroup G'
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedAddCommGroup F''
inst✝⁴ : NormedAddCommGroup G''
inst✝³ : SeminormedRing R
inst✝² : SeminormedRing R'
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
c✝ c' c₁ c₂ : ℝ
f : α → E
g : α → F
k : α → G
f' : α → E'
g' : α → F'
k' : α → G'
f'' : α → E''
g'' : α → F''
k'' : α → G''
l l' : Filter α
c : E''
hc : c ≠ 0
b : ℝ
hb₀ : 0 < b
hb : ∀ᶠ (x : α) in l, b ≤ ‖f' x‖
⊢ (fun _x => c) =O[l] f'
case mpr
α : Type u_2
β : Type ?u.315708
E : Type ?u.315711
F : Type ?u.315714
G : Type ?u.315717
E' : Type u_3
F' : Type ?u.315723
G' : Type ?u.315726
E'' : Type u_1
F'' : Type ?u.315732
G'' : Type ?u.315735
R : Type ?u.315738
R' : Type ?u.315741
𝕜 : Type ?u.315744
𝕜' : Type ?u.315747
inst✝¹² : Norm E
inst✝¹¹ : Norm F
inst✝¹⁰ : Norm G
inst✝⁹ : SeminormedAddCommGroup E'
inst✝⁸ : SeminormedAddCommGroup F'
inst✝⁷ : SeminormedAddCommGroup G'
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedAddCommGroup F''
inst✝⁴ : NormedAddCommGroup G''
inst✝³ : SeminormedRing R
inst✝² : SeminormedRing R'
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
c✝ c' c₁ c₂ : ℝ
f : α → E
g : α → F
k : α → G
f' : α → E'
g' : α → F'
k' : α → G'
f'' : α → E''
g'' : α → F''
k'' : α → G''
l l' : Filter α
c : E''
hc : c ≠ 0
⊢ (∃ b, 0 < b ∧ ∀ᶠ (x : α) in l, b ≤ ‖f' x‖) → (fun _x => c) =O[l] f'
rintro ⟨b, hb₀, hb⟩
case mpr.intro.intro
α : Type u_2
β : Type ?u.315708
E : Type ?u.315711
F : Type ?u.315714
G : Type ?u.315717
E' : Type u_3
F' : Type ?u.315723
G' : Type ?u.315726
E'' : Type u_1
F'' : Type ?u.315732
G'' : Type ?u.315735
R : Type ?u.315738
R' : Type ?u.315741
𝕜 : Type ?u.315744
𝕜' : Type ?u.315747
inst✝¹² : Norm E
inst✝¹¹ : Norm F
inst✝¹⁰ : Norm G
inst✝⁹ : SeminormedAddCommGroup E'
inst✝⁸ : SeminormedAddCommGroup F'
inst✝⁷ : SeminormedAddCommGroup G'
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedAddCommGroup F''
inst✝⁴ : NormedAddCommGroup G''
inst✝³ : SeminormedRing R
inst✝² : SeminormedRing R'
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
c✝ c' c₁ c₂ : ℝ
f : α → E
g : α → F
k : α → G
f' : α → E'
g' : α → F'
k' : α → G'
f'' : α → E''
g'' : α → F''
k'' : α → G''
l l' : Filter α
c : E''
hc : c ≠ 0
b : ℝ
hb₀ : 0 < b
hb : ∀ᶠ (x : α) in l, b ≤ ‖f' x‖
x : α
hx : b ≤ ‖f' x‖
⊢ ‖c‖ ≤ ‖c‖ / b * ‖f' x‖
case mpr.intro.intro
α : Type u_2
β : Type ?u.315708
E : Type ?u.315711
F : Type ?u.315714
G : Type ?u.315717
E' : Type u_3
F' : Type ?u.315723
G' : Type ?u.315726
E'' : Type u_1
F'' : Type ?u.315732
G'' : Type ?u.315735
R : Type ?u.315738
R' : Type ?u.315741
𝕜 : Type ?u.315744
𝕜' : Type ?u.315747
inst✝¹² : Norm E
inst✝¹¹ : Norm F
inst✝¹⁰ : Norm G
inst✝⁹ : SeminormedAddCommGroup E'
inst✝⁸ : SeminormedAddCommGroup F'
inst✝⁷ : SeminormedAddCommGroup G'
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedAddCommGroup F''
inst✝⁴ : NormedAddCommGroup G''
inst✝³ : SeminormedRing R
inst✝² : SeminormedRing R'
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
c✝ c' c₁ c₂ : ℝ
f : α → E
g : α → F
k : α → G
f' : α → E'
g' : α → F'
k' : α → G'
f'' : α → E''
g'' : α → F''
k'' : α → G''
l l' : Filter α
c : E''
hc : c ≠ 0
b : ℝ
hb₀ : 0 < b
hb : ∀ᶠ (x : α) in l, b ≤ ‖f' x‖
⊢ (fun _x => c) =O[l] f'
refine' IsBigO.of_bound (‖c‖ / b) (hb.mono fun x hx => _)
case mpr.intro.intro
α : Type u_2
β : Type ?u.315708
E : Type ?u.315711
F : Type ?u.315714
G : Type ?u.315717
E' : Type u_3
F' : Type ?u.315723
G' : Type ?u.315726
E'' : Type u_1
F'' : Type ?u.315732
G'' : Type ?u.315735
R : Type ?u.315738
R' : Type ?u.315741
𝕜 : Type ?u.315744
𝕜' : Type ?u.315747
inst✝¹² : Norm E
inst✝¹¹ : Norm F
inst✝¹⁰ : Norm G
inst✝⁹ : SeminormedAddCommGroup E'
inst✝⁸ : SeminormedAddCommGroup F'
inst✝⁷ : SeminormedAddCommGroup G'
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedAddCommGroup F''
inst✝⁴ : NormedAddCommGroup G''
inst✝³ : SeminormedRing R
inst✝² : SeminormedRing R'
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
c✝ c' c₁ c₂ : ℝ
f : α → E
g : α → F
k : α → G
f' : α → E'
g' : α → F'
k' : α → G'
f'' : α → E''
g'' : α → F''
k'' : α → G''
l l' : Filter α
c : E''
hc : c ≠ 0
b : ℝ
hb₀ : 0 < b
hb : ∀ᶠ (x : α) in l, b ≤ ‖f' x‖
x : α
hx : b ≤ ‖f' x‖
⊢ ‖c‖ ≤ ‖c‖ * (‖f' x‖ / b)
case mpr.intro.intro
α : Type u_2
β : Type ?u.315708
E : Type ?u.315711
F : Type ?u.315714
G : Type ?u.315717
E' : Type u_3
F' : Type ?u.315723
G' : Type ?u.315726
E'' : Type u_1
F'' : Type ?u.315732
G'' : Type ?u.315735
R : Type ?u.315738
R' : Type ?u.315741
𝕜 : Type ?u.315744
𝕜' : Type ?u.315747
inst✝¹² : Norm E
inst✝¹¹ : Norm F
inst✝¹⁰ : Norm G
inst✝⁹ : SeminormedAddCommGroup E'
inst✝⁸ : SeminormedAddCommGroup F'
inst✝⁷ : SeminormedAddCommGroup G'
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedAddCommGroup F''
inst✝⁴ : NormedAddCommGroup G''
inst✝³ : SeminormedRing R
inst✝² : SeminormedRing R'
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
c✝ c' c₁ c₂ : ℝ
f : α → E
g : α → F
k : α → G
f' : α → E'
g' : α → F'
k' : α → G'
f'' : α → E''
g'' : α → F''
k'' : α → G''
l l' : Filter α
c : E''
hc : c ≠ 0
b : ℝ
hb₀ : 0 < b
hb : ∀ᶠ (x : α) in l, b ≤ ‖f' x‖
x : α
hx : b ≤ ‖f' x‖
⊢ ‖c‖ ≤ ‖c‖ / b * ‖f' x‖
rw [div_mul_eq_mul_div, mul_div_assoc]
no goals
case mpr.intro.intro
α : Type u_2
β : Type ?u.315708
E : Type ?u.315711
F : Type ?u.315714
G : Type ?u.315717
E' : Type u_3
F' : Type ?u.315723
G' : Type ?u.315726
E'' : Type u_1
F'' : Type ?u.315732
G'' : Type ?u.315735
R : Type ?u.315738
R' : Type ?u.315741
𝕜 : Type ?u.315744
𝕜' : Type ?u.315747
inst✝¹² : Norm E
inst✝¹¹ : Norm F
inst✝¹⁰ : Norm G
inst✝⁹ : SeminormedAddCommGroup E'
inst✝⁸ : SeminormedAddCommGroup F'
inst✝⁷ : SeminormedAddCommGroup G'
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedAddCommGroup F''
inst✝⁴ : NormedAddCommGroup G''
inst✝³ : SeminormedRing R
inst✝² : SeminormedRing R'
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
c✝ c' c₁ c₂ : ℝ
f : α → E
g : α → F
k : α → G
f' : α → E'
g' : α → F'
k' : α → G'
f'' : α → E''
g'' : α → F''
k'' : α → G''
l l' : Filter α
c : E''
hc : c ≠ 0
b : ℝ
hb₀ : 0 < b
hb : ∀ᶠ (x : α) in l, b ≤ ‖f' x‖
x : α
hx : b ≤ ‖f' x‖
⊢ ‖c‖ ≤ ‖c‖ * (‖f' x‖ / b)
exact le_mul_of_one_le_right (norm_nonneg _) ((one_le_div hb₀).2 hx)