case zero
α : Type u_1
β : Type ?u.989121
γ : Type ?u.989124
δ : Type ?u.989127
m : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
h_meas : ∀ (n : ℕ), Measurable (f n)
h_mono✝ : ∀ (n : ℕ), f (Nat.succ n) ≤ᵐ[μ] f n
h_fin : (∫⁻ (a : α), f 0 a ∂μ) ≠ ⊤
fn_le_f0 : (∫⁻ (a : α), ⨅ (n : ℕ), f n a ∂μ) ≤ ∫⁻ (a : α), f 0 a ∂μ
fn_le_f0' : (⨅ (n : ℕ), ∫⁻ (a : α), f n a ∂μ) ≤ ∫⁻ (a : α), f 0 a ∂μ
h_mono : ∀ᵐ (a : α) ∂μ, ∀ (n : ℕ), f (Nat.succ n) a ≤ f n a
a : α
h : ∀ (n : ℕ), f (Nat.succ n) a ≤ f n a
⊢ f Nat.zero a ≤ f 0 a

case succ
α : Type u_1
β : Type ?u.989121
γ : Type ?u.989124
δ : Type ?u.989127
m : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
h_meas : ∀ (n : ℕ), Measurable (f n)
h_mono✝ : ∀ (n : ℕ), f (Nat.succ n) ≤ᵐ[μ] f n
h_fin : (∫⁻ (a : α), f 0 a ∂μ) ≠ ⊤
fn_le_f0 : (∫⁻ (a : α), ⨅ (n : ℕ), f n a ∂μ) ≤ ∫⁻ (a : α), f 0 a ∂μ
fn_le_f0' : (⨅ (n : ℕ), ∫⁻ (a : α), f n a ∂μ) ≤ ∫⁻ (a : α), f 0 a ∂μ
h_mono : ∀ᵐ (a : α) ∂μ, ∀ (n : ℕ), f (Nat.succ n) a ≤ f n a
a : α
h : ∀ (n : ℕ), f (Nat.succ n) a ≤ f n a
n : ℕ
ih : f n a ≤ f 0 a
⊢ f (Nat.succ n) a ≤ f 0 a
α : Type u_1
β : Type ?u.989121
γ : Type ?u.989124
δ : Type ?u.989127
m : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
h_meas : ∀ (n : ℕ), Measurable (f n)
h_mono✝ : ∀ (n : ℕ), f (Nat.succ n) ≤ᵐ[μ] f n
h_fin : (∫⁻ (a : α), f 0 a ∂μ) ≠ ⊤
fn_le_f0 : (∫⁻ (a : α), ⨅ (n : ℕ), f n a ∂μ) ≤ ∫⁻ (a : α), f 0 a ∂μ
fn_le_f0' : (⨅ (n : ℕ), ∫⁻ (a : α), f n a ∂μ) ≤ ∫⁻ (a : α), f 0 a ∂μ
h_mono : ∀ᵐ (a : α) ∂μ, ∀ (n : ℕ), f (Nat.succ n) a ≤ f n a
n : ℕ
a : α
h : ∀ (n : ℕ), f (Nat.succ n) a ≤ f n a
⊢ f n a ≤ f 0 a
induction' n with n ih