case h
α : Type u_1
β : Type ?u.1586018
ι : Type ?u.1586021
E : Type u_2
F : Type ?u.1586027
𝕜 : Type ?u.1586030
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
f : { x // x ∈ simpleFunc E p μ }
a✝ : α
⊢ ↑(toSimpleFunc (-f)) a✝ = ↑↑↑(-f) a✝ →
    ↑(toSimpleFunc f) a✝ = ↑↑↑f a✝ → ↑↑(-↑f) a✝ = (-↑↑↑f) a✝ → ↑(toSimpleFunc (-f)) a✝ = (-↑(toSimpleFunc f)) a✝
α : Type u_1
β : Type ?u.1586018
ι : Type ?u.1586021
E : Type u_2
F : Type ?u.1586027
𝕜 : Type ?u.1586030
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
f : { x // x ∈ simpleFunc E p μ }
⊢ ↑(toSimpleFunc (-f)) =ᵐ[μ] -↑(toSimpleFunc f)
filter_upwards [toSimpleFunc_eq_toFun (-f), toSimpleFunc_eq_toFun f,
  Lp.coeFn_neg (f : Lp E p μ)] with _
case h
α : Type u_1
β : Type ?u.1586018
ι : Type ?u.1586021
E : Type u_2
F : Type ?u.1586027
𝕜 : Type ?u.1586030
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
f : { x // x ∈ simpleFunc E p μ }
a✝ : α
⊢ ↑(toSimpleFunc (-f)) a✝ = ↑(-↑↑f) a✝ →
    ↑(toSimpleFunc f) a✝ = ↑↑↑f a✝ → ↑(-↑↑f) a✝ = -↑↑↑f a✝ → ↑(toSimpleFunc (-f)) a✝ = -↑(toSimpleFunc f) a✝
case h
α : Type u_1
β : Type ?u.1586018
ι : Type ?u.1586021
E : Type u_2
F : Type ?u.1586027
𝕜 : Type ?u.1586030
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
f : { x // x ∈ simpleFunc E p μ }
a✝ : α
⊢ ↑(toSimpleFunc (-f)) a✝ = ↑↑↑(-f) a✝ →
    ↑(toSimpleFunc f) a✝ = ↑↑↑f a✝ → ↑↑(-↑f) a✝ = (-↑↑↑f) a✝ → ↑(toSimpleFunc (-f)) a✝ = (-↑(toSimpleFunc f)) a✝
simp only [Pi.neg_apply, AddSubgroup.coe_neg]
no goals
case h
α : Type u_1
β : Type ?u.1586018
ι : Type ?u.1586021
E : Type u_2
F : Type ?u.1586027
𝕜 : Type ?u.1586030
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
f : { x // x ∈ simpleFunc E p μ }
a✝ : α
⊢ ↑(toSimpleFunc (-f)) a✝ = ↑(-↑↑f) a✝ →
    ↑(toSimpleFunc f) a✝ = ↑↑↑f a✝ → ↑(-↑↑f) a✝ = -↑↑↑f a✝ → ↑(toSimpleFunc (-f)) a✝ = -↑(toSimpleFunc f) a✝
repeat intro h; rw [h]
no goals
case h
α : Type u_1
β : Type ?u.1586018
ι : Type ?u.1586021
E : Type u_2
F : Type ?u.1586027
𝕜 : Type ?u.1586030
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
f : { x // x ∈ simpleFunc E p μ }
a✝ : α
h✝¹ : ↑(toSimpleFunc (-f)) a✝ = ↑(-↑↑f) a✝
h✝ : ↑(toSimpleFunc f) a✝ = ↑↑↑f a✝
h : ↑(-↑↑f) a✝ = -↑↑↑f a✝
⊢ ↑(-↑↑f) a✝ = -↑↑↑f a✝
rw [h]