Theorem: cancel_aux (PrimeNumberTheoremAnd/Wiener.lean)

State before:
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 : ℕ
⊢ ∑ 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)))
Tactic:
have l1 (n : ℕ) : (g n - g (n + 1)) * ∑ i in Finset.range (n + 1), f i ≤ (g n - g (n + 1)) * (C * (n + 1)) := by
  apply mul_le_mul le_rfl (by simpa using hf' (n + 1)) (Finset.sum_nonneg' hf) ?_
  simp ; apply hg' ; simp
State after:
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))
⊢ ∑ 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)))

State before:
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))
⊢ ∑ 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)))
Tactic:
have l2 (x : ℕ) : C * (↑(x + 1) + 1) - C * (↑x + 1) = C := by simp ; ring
State after:
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
⊢ ∑ 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)))

State before:
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
⊢ ∑ 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)))
Tactic:
have l3 (n : ℕ) : 0 ≤ cumsum f n := Finset.sum_nonneg' hf
State after:
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)))

State before:
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)))
Tactic:
convert_to ∑ i in Finset.range n, (g i) • (f i) ≤ _
State after:
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)))

State before:
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)))
Tactic:
simp [mul_comm]
State after:
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)))

State before:
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)))
Tactic:
rw [Finset.sum_range_by_parts, sub_eq_add_neg, ← Finset.sum_neg_distrib]
State after:
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
⊢ g (n - 1) • ∑ i ∈ Finset.range n, f i +
      ∑ x ∈ Finset.range (n - 1), -((g (x + 1) - g x) • ∑ i ∈ Finset.range (x + 1), 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)))

State before:
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
⊢ g (n - 1) • ∑ i ∈ Finset.range n, f i +
      ∑ x ∈ Finset.range (n - 1), -((g (x + 1) - g x) • ∑ i ∈ Finset.range (x + 1), 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)))
Tactic:
simp_rw [← neg_smul, neg_sub, smul_eq_mul]
State after:
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
⊢ g (n - 1) * ∑ i ∈ Finset.range n, f i +
      ∑ x ∈ Finset.range (n - 1), (g x - g (x + 1)) * ∑ i ∈ Finset.range (x + 1), 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)))

State before:
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
⊢ g (n - 1) * ∑ i ∈ Finset.range n, f i +
      ∑ x ∈ Finset.range (n - 1), (g x - g (x + 1)) * ∑ i ∈ Finset.range (x + 1), 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)))
Tactic:
apply _root_.add_le_add
State after:
case convert_2.h₁
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
⊢ g (n - 1) * ∑ i ∈ Finset.range n, f i ≤ g (n - 1) * (C * ↑n)

case convert_2.h₂
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
⊢ ∑ x ∈ Finset.range (n - 1), (g x - g (x + 1)) * ∑ i ∈ Finset.range (x + 1), f i ≤
    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))

State before:
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✝ n : ℕ
⊢ (g n - g (n + 1)) * ∑ i ∈ Finset.range (n + 1), f i ≤ (g n - g (n + 1)) * (C * (↑n + 1))
Tactic:
apply mul_le_mul le_rfl (by simpa using hf' (n + 1)) (Finset.sum_nonneg' hf) ?_
State after:
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✝ n : ℕ
⊢ 0 ≤ g n - g (n + 1)

State before:
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✝ n : ℕ
⊢ 0 ≤ g n - g (n + 1)
Tactic:
simp
State after:
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✝ n : ℕ
⊢ g (n + 1) ≤ g n

State before:
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✝ n : ℕ
⊢ g (n + 1) ≤ g n
Tactic:
apply hg'
State after:
case a
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✝ n : ℕ
⊢ n ≤ n + 1

State before:
case a
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✝ n : ℕ
⊢ n ≤ n + 1
Tactic:
simp
State after:
no goals

State before:
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✝ n : ℕ
⊢ ∑ i ∈ Finset.range (n + 1), f i ≤ C * (↑n + 1)
Tactic:
simpa using hf' (n + 1)
State after:
no goals

State before:
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))
x : ℕ
⊢ C * (↑(x + 1) + 1) - C * (↑x + 1) = C
Tactic:
simp
State after:
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))
x : ℕ
⊢ C * (↑x + 1 + 1) - C * (↑x + 1) = C

State before:
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))
x : ℕ
⊢ C * (↑x + 1 + 1) - C * (↑x + 1) = C
Tactic:
ring
State after:
no goals

State before:
case convert_2.h₁
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
⊢ g (n - 1) * ∑ i ∈ Finset.range n, f i ≤ g (n - 1) * (C * ↑n)
Tactic:
exact mul_le_mul le_rfl (hf' n) (l3 n) (hg _)
State after:
no goals

State before:
case convert_2.h₂
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
⊢ ∑ x ∈ Finset.range (n - 1), (g x - g (x + 1)) * ∑ i ∈ Finset.range (x + 1), f i ≤
    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))
Tactic:
apply Finset.sum_le_sum (fun n _ => l1 n) |>.trans
State after:
case convert_2.h₂
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 - 1), (g i - g (i + 1)) * (C * (↑i + 1)) ≤
    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))

State before:
case convert_2.h₂
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 - 1), (g i - g (i + 1)) * (C * (↑i + 1)) ≤
    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))
Tactic:
convert_to ∑ i in Finset.range (n - 1), (C * (↑i + 1)) • (g i - g (i + 1)) ≤ _
State after:
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 - 1), (g i - g (i + 1)) * (C * (↑i + 1)) =
    ∑ i ∈ Finset.range (n - 1), (C * (↑i + 1)) • (g i - g (i + 1))

case convert_2.h₂.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 - 1), (C * (↑i + 1)) • (g i - g (i + 1)) ≤
    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))

State before:
case convert_2.h₂.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 - 1), (C * (↑i + 1)) • (g i - g (i + 1)) ≤
    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))
Tactic:
rw [Finset.sum_range_by_parts]
State after:
case convert_2.h₂.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
⊢ (C * (↑(n - 1 - 1) + 1)) • ∑ i ∈ Finset.range (n - 1), (g i - g (i + 1)) -
      ∑ i ∈ Finset.range (n - 1 - 1),
        (C * (↑(i + 1) + 1) - C * (↑i + 1)) • ∑ i ∈ Finset.range (i + 1), (g i - g (i + 1)) ≤
    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))

State before:
case convert_2.h₂.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
⊢ (C * (↑(n - 1 - 1) + 1)) • ∑ i ∈ Finset.range (n - 1), (g i - g (i + 1)) -
      ∑ i ∈ Finset.range (n - 1 - 1),
        (C * (↑(i + 1) + 1) - C * (↑i + 1)) • ∑ i ∈ Finset.range (i + 1), (g i - g (i + 1)) ≤
    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))
Tactic:
simp_rw [Finset.sum_range_sub', l2, smul_sub, smul_eq_mul, Finset.sum_sub_distrib, Finset.sum_const, Finset.card_range]
State after:
case convert_2.h₂.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
⊢ 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)) ≤
    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))

State before:
case convert_2.h₂.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
⊢ 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)) ≤
    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))
Tactic:
apply le_of_eq
State after:
case convert_2.h₂.convert_2.a
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
⊢ 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)) =
    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))

State before:
case convert_2.h₂.convert_2.a
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
⊢ 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)) =
    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))
Tactic:
ring_nf
State after:
no goals

State before:
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 - 1), (g i - g (i + 1)) * (C * (↑i + 1)) =
    ∑ i ∈ Finset.range (n - 1), (C * (↑i + 1)) • (g i - g (i + 1))
Tactic:
congr
State after:
case h.e'_3.e_f
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
⊢ (fun i => (g i - g (i + 1)) * (C * (↑i + 1))) = fun i => (C * (↑i + 1)) • (g i - g (i + 1))

State before:
case h.e'_3.e_f
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
⊢ (fun i => (g i - g (i + 1)) * (C * (↑i + 1))) = fun i => (C * (↑i + 1)) • (g i - g (i + 1))
Tactic:
ext i
State after:
case h.e'_3.e_f.h
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 : ℕ
⊢ (g i - g (i + 1)) * (C * (↑i + 1)) = (C * (↑i + 1)) • (g i - g (i + 1))

State before:
case h.e'_3.e_f.h
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 : ℕ
⊢ (g i - g (i + 1)) * (C * (↑i + 1)) = (C * (↑i + 1)) • (g i - g (i + 1))
Tactic:
simp
State after:
case h.e'_3.e_f.h
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 : ℕ
⊢ (g i - g (i + 1)) * (C * (↑i + 1)) = C * (↑i + 1) * (g i - g (i + 1))

State before:
case h.e'_3.e_f.h
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 : ℕ
⊢ (g i - g (i + 1)) * (C * (↑i + 1)) = C * (↑i + 1) * (g i - g (i + 1))
Tactic:
ring
State after:
no goals