case h
α : Type u_1
β : Type ?u.1594821
ι : Type ?u.1594824
E : Type u_2
F : Type ?u.1594830
𝕜 : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : BoundedSMul 𝕜 E
k : 𝕜
f : { x // x ∈ simpleFunc E p μ }
a✝ : α
⊢ ↑(toSimpleFunc (k • f)) a✝ = ↑↑↑(k • f) a✝ →
    ↑(toSimpleFunc f) a✝ = ↑↑↑f a✝ →
      ↑↑(k • ↑f) a✝ = (k • ↑↑↑f) a✝ → ↑(toSimpleFunc (k • f)) a✝ = (k • ↑(toSimpleFunc f)) a✝
α : Type u_1
β : Type ?u.1594821
ι : Type ?u.1594824
E : Type u_2
F : Type ?u.1594830
𝕜 : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : BoundedSMul 𝕜 E
k : 𝕜
f : { x // x ∈ simpleFunc E p μ }
⊢ ↑(toSimpleFunc (k • f)) =ᵐ[μ] k • ↑(toSimpleFunc f)
filter_upwards [toSimpleFunc_eq_toFun (k • f), toSimpleFunc_eq_toFun f,
  Lp.coeFn_smul k (f : Lp E p μ)] with _
case h
α : Type u_1
β : Type ?u.1594821
ι : Type ?u.1594824
E : Type u_2
F : Type ?u.1594830
𝕜 : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : BoundedSMul 𝕜 E
k : 𝕜
f : { x // x ∈ simpleFunc E p μ }
a✝ : α
⊢ ↑(toSimpleFunc (k • f)) a✝ = ↑↑(k • ↑f) a✝ →
    ↑(toSimpleFunc f) a✝ = ↑↑↑f a✝ → ↑↑(k • ↑f) a✝ = k • ↑↑↑f a✝ → ↑(toSimpleFunc (k • f)) a✝ = k • ↑(toSimpleFunc f) a✝
case h
α : Type u_1
β : Type ?u.1594821
ι : Type ?u.1594824
E : Type u_2
F : Type ?u.1594830
𝕜 : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : BoundedSMul 𝕜 E
k : 𝕜
f : { x // x ∈ simpleFunc E p μ }
a✝ : α
⊢ ↑(toSimpleFunc (k • f)) a✝ = ↑↑↑(k • f) a✝ →
    ↑(toSimpleFunc f) a✝ = ↑↑↑f a✝ →
      ↑↑(k • ↑f) a✝ = (k • ↑↑↑f) a✝ → ↑(toSimpleFunc (k • f)) a✝ = (k • ↑(toSimpleFunc f)) a✝
simp only [Pi.smul_apply, coe_smul]
no goals
case h
α : Type u_1
β : Type ?u.1594821
ι : Type ?u.1594824
E : Type u_2
F : Type ?u.1594830
𝕜 : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : BoundedSMul 𝕜 E
k : 𝕜
f : { x // x ∈ simpleFunc E p μ }
a✝ : α
⊢ ↑(toSimpleFunc (k • f)) a✝ = ↑↑(k • ↑f) a✝ →
    ↑(toSimpleFunc f) a✝ = ↑↑↑f a✝ → ↑↑(k • ↑f) a✝ = k • ↑↑↑f a✝ → ↑(toSimpleFunc (k • f)) a✝ = k • ↑(toSimpleFunc f) a✝
repeat intro h; rw [h]
no goals
case h
α : Type u_1
β : Type ?u.1594821
ι : Type ?u.1594824
E : Type u_2
F : Type ?u.1594830
𝕜 : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : BoundedSMul 𝕜 E
k : 𝕜
f : { x // x ∈ simpleFunc E p μ }
a✝ : α
h✝¹ : ↑(toSimpleFunc (k • f)) a✝ = ↑↑(k • ↑f) a✝
h✝ : ↑(toSimpleFunc f) a✝ = ↑↑↑f a✝
h : ↑↑(k • ↑f) a✝ = k • ↑↑↑f a✝
⊢ ↑↑(k • ↑f) a✝ = k • ↑↑↑f a✝
rw [h]