α : Type u_1
E : Type ?u.94507
F : Type ?u.94510
𝕜 : Type ?u.94513
inst✝² : LinearOrder E
inst✝¹ : Zero E
inst✝ : MeasurableSpace α
f : α →ₛ ℝ
⊢ map (fun b => max b 0) f - map (fun b => max b 0) (-f) = f
α : Type u_1
E : Type ?u.94507
F : Type ?u.94510
𝕜 : Type ?u.94513
inst✝² : LinearOrder E
inst✝¹ : Zero E
inst✝ : MeasurableSpace α
f : α →ₛ ℝ
⊢ posPart f - negPart f = f
simp only [posPart, negPart]
case H
α : Type u_1
E : Type ?u.94507
F : Type ?u.94510
𝕜 : Type ?u.94513
inst✝² : LinearOrder E
inst✝¹ : Zero E
inst✝ : MeasurableSpace α
f : α →ₛ ℝ
a : α
⊢ ↑(map (fun b => max b 0) f - map (fun b => max b 0) (-f)) a = ↑f a
α : Type u_1
E : Type ?u.94507
F : Type ?u.94510
𝕜 : Type ?u.94513
inst✝² : LinearOrder E
inst✝¹ : Zero E
inst✝ : MeasurableSpace α
f : α →ₛ ℝ
⊢ map (fun b => max b 0) f - map (fun b => max b 0) (-f) = f
ext a
case H
α : Type u_1
E : Type ?u.94507
F : Type ?u.94510
𝕜 : Type ?u.94513
inst✝² : LinearOrder E
inst✝¹ : Zero E
inst✝ : MeasurableSpace α
f : α →ₛ ℝ
a : α
⊢ (↑(map (fun b => max b 0) f) - ↑(map (fun b => max b 0) (-f))) a = ↑f a
case H
α : Type u_1
E : Type ?u.94507
F : Type ?u.94510
𝕜 : Type ?u.94513
inst✝² : LinearOrder E
inst✝¹ : Zero E
inst✝ : MeasurableSpace α
f : α →ₛ ℝ
a : α
⊢ ↑(map (fun b => max b 0) f - map (fun b => max b 0) (-f)) a = ↑f a
rw [coe_sub]
no goals
case H
α : Type u_1
E : Type ?u.94507
F : Type ?u.94510
𝕜 : Type ?u.94513
inst✝² : LinearOrder E
inst✝¹ : Zero E
inst✝ : MeasurableSpace α
f : α →ₛ ℝ
a : α
⊢ (↑(map (fun b => max b 0) f) - ↑(map (fun b => max b 0) (-f))) a = ↑f a
exact max_zero_sub_eq_self (f a)