case zero
α : Type u_1
β : Type ?u.843173
γ : Type ?u.843176
δ : Type ?u.843179
inst✝ : MeasurableSpace α
K : Type ?u.843185
f : α → ℝ≥0∞
a : α
⊢ ∑ k in Finset.range (Nat.zero + 1), ↑(↑(eapproxDiff f k) a) = ↑(eapprox f Nat.zero) a

case succ
α : Type u_1
β : Type ?u.843173
γ : Type ?u.843176
δ : Type ?u.843179
inst✝ : MeasurableSpace α
K : Type ?u.843185
f : α → ℝ≥0∞
a : α
n : ℕ
IH : ∑ k in Finset.range (n + 1), ↑(↑(eapproxDiff f k) a) = ↑(eapprox f n) a
⊢ ∑ k in Finset.range (Nat.succ n + 1), ↑(↑(eapproxDiff f k) a) = ↑(eapprox f (Nat.succ n)) a
α : Type u_1
β : Type ?u.843173
γ : Type ?u.843176
δ : Type ?u.843179
inst✝ : MeasurableSpace α
K : Type ?u.843185
f : α → ℝ≥0∞
n : ℕ
a : α
⊢ ∑ k in Finset.range (n + 1), ↑(↑(eapproxDiff f k) a) = ↑(eapprox f n) a
induction' n with n IH
case zero
α : Type u_1
β : Type ?u.843173
γ : Type ?u.843176
δ : Type ?u.843179
inst✝ : MeasurableSpace α
K : Type ?u.843185
f : α → ℝ≥0∞
a : α
⊢ ↑(↑(eapproxDiff f 0) a) = ↑(eapprox f 0) a
case zero
α : Type u_1
β : Type ?u.843173
γ : Type ?u.843176
δ : Type ?u.843179
inst✝ : MeasurableSpace α
K : Type ?u.843185
f : α → ℝ≥0∞
a : α
⊢ ∑ k in Finset.range (Nat.zero + 1), ↑(↑(eapproxDiff f k) a) = ↑(eapprox f Nat.zero) a
simp only [Nat.zero_eq, Nat.zero_add, Finset.sum_singleton, Finset.range_one]
no goals
case zero
α : Type u_1
β : Type ?u.843173
γ : Type ?u.843176
δ : Type ?u.843179
inst✝ : MeasurableSpace α
K : Type ?u.843185
f : α → ℝ≥0∞
a : α
⊢ ↑(↑(eapproxDiff f 0) a) = ↑(eapprox f 0) a
rfl
case succ
α : Type u_1
β : Type ?u.843173
γ : Type ?u.843176
δ : Type ?u.843179
inst✝ : MeasurableSpace α
K : Type ?u.843185
f : α → ℝ≥0∞
a : α
n : ℕ
IH : ∑ k in Finset.range (n + 1), ↑(↑(eapproxDiff f k) a) = ↑(eapprox f n) a
⊢ ↑(eapprox f (Nat.add n 0 + 1)) a - ↑(eapprox f (Nat.add n 0)) a ≠ ⊤
case succ
α : Type u_1
β : Type ?u.843173
γ : Type ?u.843176
δ : Type ?u.843179
inst✝ : MeasurableSpace α
K : Type ?u.843185
f : α → ℝ≥0∞
a : α
n : ℕ
IH : ∑ k in Finset.range (n + 1), ↑(↑(eapproxDiff f k) a) = ↑(eapprox f n) a
⊢ ∑ k in Finset.range (Nat.succ n + 1), ↑(↑(eapproxDiff f k) a) = ↑(eapprox f (Nat.succ n)) a
erw [Finset.sum_range_succ, Nat.succ_eq_add_one, IH, eapproxDiff, coe_map, Function.comp_apply,
  coe_sub, Pi.sub_apply, ENNReal.coe_toNNReal,
  add_tsub_cancel_of_le (monotone_eapprox f (Nat.le_succ _) _)]
α : Type u_1
β : Type ?u.843173
γ : Type ?u.843176
δ : Type ?u.843179
inst✝ : MeasurableSpace α
K : Type ?u.843185
f : α → ℝ≥0∞
a : α
n : ℕ
IH : ∑ k in Finset.range (n + 1), ↑(↑(eapproxDiff f k) a) = ↑(eapprox f n) a
⊢ ↑(eapprox f (Nat.add n 0 + 1)) a - ↑(eapprox f (Nat.add n 0)) a ≤ ↑(eapprox f (n + 1)) a
case succ
α : Type u_1
β : Type ?u.843173
γ : Type ?u.843176
δ : Type ?u.843179
inst✝ : MeasurableSpace α
K : Type ?u.843185
f : α → ℝ≥0∞
a : α
n : ℕ
IH : ∑ k in Finset.range (n + 1), ↑(↑(eapproxDiff f k) a) = ↑(eapprox f n) a
⊢ ↑(eapprox f (Nat.add n 0 + 1)) a - ↑(eapprox f (Nat.add n 0)) a ≠ ⊤
apply (lt_of_le_of_lt _ (eapprox_lt_top f (n + 1) a)).ne
α : Type u_1
β : Type ?u.843173
γ : Type ?u.843176
δ : Type ?u.843179
inst✝ : MeasurableSpace α
K : Type ?u.843185
f : α → ℝ≥0∞
a : α
n : ℕ
IH : ∑ k in Finset.range (n + 1), ↑(↑(eapproxDiff f k) a) = ↑(eapprox f n) a
⊢ ↑(eapprox f (Nat.add n 0 + 1)) a ≤ ↑(eapprox f (n + 1)) a + ↑(eapprox f (Nat.add n 0)) a
α : Type u_1
β : Type ?u.843173
γ : Type ?u.843176
δ : Type ?u.843179
inst✝ : MeasurableSpace α
K : Type ?u.843185
f : α → ℝ≥0∞
a : α
n : ℕ
IH : ∑ k in Finset.range (n + 1), ↑(↑(eapproxDiff f k) a) = ↑(eapprox f n) a
⊢ ↑(eapprox f (Nat.add n 0 + 1)) a - ↑(eapprox f (Nat.add n 0)) a ≤ ↑(eapprox f (n + 1)) a
rw [tsub_le_iff_right]
no goals
α : Type u_1
β : Type ?u.843173
γ : Type ?u.843176
δ : Type ?u.843179
inst✝ : MeasurableSpace α
K : Type ?u.843185
f : α → ℝ≥0∞
a : α
n : ℕ
IH : ∑ k in Finset.range (n + 1), ↑(↑(eapproxDiff f k) a) = ↑(eapprox f n) a
⊢ ↑(eapprox f (Nat.add n 0 + 1)) a ≤ ↑(eapprox f (n + 1)) a + ↑(eapprox f (Nat.add n 0)) a
exact le_self_add