by_cases hi : i = 0 <;> simp [hi]
case a
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x₀ : ℝ
f : ℝ → ℝ
n : ℕ
hfi : IntegrableOn f (Icc x₀ (x₀ + ↑(n + 1))) volume
hf : AntitoneOn f (Ioc x₀ (x₀ + (↑n + 1)))
i : ℕ
⊢ i ∈ Finset.range (n + 1) ↔ i ∈ {0} ∪ Finset.Ico 1 (n + 1)
case neg
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x₀ : ℝ
f : ℝ → ℝ
n : ℕ
hfi : IntegrableOn f (Icc x₀ (x₀ + ↑(n + 1))) volume
hf : AntitoneOn f (Ioc x₀ (x₀ + (↑n + 1)))
i : ℕ
hi : ¬i = 0
⊢ i < n + 1 → 1 ≤ i