case h.e'_5
M : Type ?u.1462833
inst✝³ : MeasurableSpace M
α : Type u_2
m : MeasurableSpace α
μ : MeasureTheory.Measure α
f✝ g : α → M
δ : Type u_1
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
M : Type ?u.1462833
inst✝³ : MeasurableSpace M
α : Type u_2
m : MeasurableSpace α
μ : MeasureTheory.Measure α
f✝ g : α → M
δ : Type u_1
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
convert Finset.measurable_range_sup' hf using 1
case h.e'_5.h
M : Type ?u.1462833
inst✝³ : MeasurableSpace M
α : Type u_2
m : MeasurableSpace α
μ : MeasureTheory.Measure α
f✝ g : α → M
δ : Type u_1
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
case h.e'_5
M : Type ?u.1462833
inst✝³ : MeasurableSpace M
α : Type u_2
m : MeasurableSpace α
μ : MeasureTheory.Measure α
f✝ g : α → M
δ : Type u_1
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
ext x
no goals
case h.e'_5.h
M : Type ?u.1462833
inst✝³ : MeasurableSpace M
α : Type u_2
m : MeasurableSpace α
μ : MeasureTheory.Measure α
f✝ g : α → M
δ : Type u_1
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
simp