[GOAL]
M : Type u_1
inst✝³ : MeasurableSpace M
α : Type u_2
m : MeasurableSpace α
μ : Measure α
f✝ g : α → M
δ : Type u_3
inst✝² : MeasurableSpace δ
inst✝¹ : SemilatticeSup α
inst✝ : MeasurableSup₂ α
f : ℕ → δ → α
n : ℕ
hf : ∀ (k : ℕ), k ≤ n → Measurable (f k)
⊢ Measurable (sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) f)
[PROOFSTEP]
simp_rw [← Nat.lt_succ_iff] at hf 
[GOAL]
M : Type u_1
inst✝³ : MeasurableSpace M
α : Type u_2
m : MeasurableSpace α
μ : Measure α
f✝ g : α → M
δ : Type u_3
inst✝² : MeasurableSpace δ
inst✝¹ : SemilatticeSup α
inst✝ : MeasurableSup₂ α
f : ℕ → δ → α
n : ℕ
hf : ∀ (k : ℕ), k < Nat.succ n → Measurable (f k)
⊢ Measurable (sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) f)
[PROOFSTEP]
refine' Finset.measurable_sup' _ _
[GOAL]
M : Type u_1
inst✝³ : MeasurableSpace M
α : Type u_2
m : MeasurableSpace α
μ : Measure α
f✝ g : α → M
δ : Type u_3
inst✝² : MeasurableSpace δ
inst✝¹ : SemilatticeSup α
inst✝ : MeasurableSup₂ α
f : ℕ → δ → α
n : ℕ
hf : ∀ (k : ℕ), k < Nat.succ n → Measurable (f k)
⊢ ∀ (n_1 : ℕ), n_1 ∈ range (n + 1) → Measurable (f n_1)
[PROOFSTEP]
simpa [Finset.mem_range]
[GOAL]
M : Type u_1
inst✝³ : MeasurableSpace M
α : Type u_2
m : MeasurableSpace α
μ : Measure α
f✝ g : α → M
δ : Type u_3
inst✝² : MeasurableSpace δ
inst✝¹ : SemilatticeSup α
inst✝ : MeasurableSup₂ α
f : ℕ → δ → α
n : ℕ
hf : ∀ (k : ℕ), k ≤ n → Measurable (f k)
⊢ Measurable fun x => sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k x
[PROOFSTEP]
convert Finset.measurable_range_sup' hf using 1
[GOAL]
case h.e'_5
M : Type u_1
inst✝³ : MeasurableSpace M
α : Type u_2
m : MeasurableSpace α
μ : Measure α
f✝ g : α → M
δ : Type u_3
inst✝² : MeasurableSpace δ
inst✝¹ : SemilatticeSup α
inst✝ : MeasurableSup₂ α
f : ℕ → δ → α
n : ℕ
hf : ∀ (k : ℕ), k ≤ n → Measurable (f k)
⊢ (fun x => sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k x) =
    sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k
[PROOFSTEP]
ext x
[GOAL]
case h.e'_5.h
M : Type u_1
inst✝³ : MeasurableSpace M
α : Type u_2
m : MeasurableSpace α
μ : Measure α
f✝ g : α → M
δ : Type u_3
inst✝² : MeasurableSpace δ
inst✝¹ : SemilatticeSup α
inst✝ : MeasurableSup₂ α
f : ℕ → δ → α
n : ℕ
hf : ∀ (k : ℕ), k ≤ n → Measurable (f k)
x : δ
⊢ (sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k x) =
    sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) (fun k => f k) x
[PROOFSTEP]
simp
