convert_to ∑ i in Finset.range n, (g i) • (f i) ≤ _
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
f g : ℕ → ℝ
hf : 0 ≤ f
hg : 0 ≤ g
hf' : ∀ (n : ℕ), cumsum f n ≤ C * ↑n
hg' : Antitone g
n : ℕ
l1 : ∀ (n : ℕ), (g n - g (n + 1)) * ∑ i ∈ Finset.range (n + 1), f i ≤ (g n - g (n + 1)) * (C * (↑n + 1))
l2 : ∀ (x : ℕ), C * (↑(x + 1) + 1) - C * (↑x + 1) = C
l3 : ∀ (n : ℕ), 0 ≤ cumsum f n
⊢ ∑ i ∈ Finset.range n, f i * g i ≤
    g (n - 1) * (C * ↑n) +
      (C * (↑(n - 1 - 1) + 1) * g 0 - C * (↑(n - 1 - 1) + 1) * g (n - 1) -
        ((n - 1 - 1) • (C * g 0) - ∑ x ∈ Finset.range (n - 1 - 1), C * g (x + 1)))
case h.e'_3
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
f g : ℕ → ℝ
hf : 0 ≤ f
hg : 0 ≤ g
hf' : ∀ (n : ℕ), cumsum f n ≤ C * ↑n
hg' : Antitone g
n : ℕ
l1 : ∀ (n : ℕ), (g n - g (n + 1)) * ∑ i ∈ Finset.range (n + 1), f i ≤ (g n - g (n + 1)) * (C * (↑n + 1))
l2 : ∀ (x : ℕ), C * (↑(x + 1) + 1) - C * (↑x + 1) = C
l3 : ∀ (n : ℕ), 0 ≤ cumsum f n
⊢ ∑ i ∈ Finset.range n, f i * g i = ∑ i ∈ Finset.range n, g i • f i

case convert_2
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
f g : ℕ → ℝ
hf : 0 ≤ f
hg : 0 ≤ g
hf' : ∀ (n : ℕ), cumsum f n ≤ C * ↑n
hg' : Antitone g
n : ℕ
l1 : ∀ (n : ℕ), (g n - g (n + 1)) * ∑ i ∈ Finset.range (n + 1), f i ≤ (g n - g (n + 1)) * (C * (↑n + 1))
l2 : ∀ (x : ℕ), C * (↑(x + 1) + 1) - C * (↑x + 1) = C
l3 : ∀ (n : ℕ), 0 ≤ cumsum f n
⊢ ∑ i ∈ Finset.range n, g i • f i ≤
    g (n - 1) * (C * ↑n) +
      (C * (↑(n - 1 - 1) + 1) * g 0 - C * (↑(n - 1 - 1) + 1) * g (n - 1) -
        ((n - 1 - 1) • (C * g 0) - ∑ x ∈ Finset.range (n - 1 - 1), C * g (x + 1)))