-- Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean
theorem smul_toSimpleFunc (k : 𝕜) (f : Lp.simpleFunc E p μ) :
    toSimpleFunc (k • f) =ᵐ[μ] k • ⇑(toSimpleFunc f)

Proof state:
case h
α : Type u_1
E : Type u_4
𝕜 : Type u_6
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : BoundedSMul 𝕜 E
k : 𝕜
f : ↥(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✝

Tactic:
rw [h]

Result:
no goals

Proof state:
α : Type u_1
E : Type u_4
𝕜 : Type u_6
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : BoundedSMul 𝕜 E
k : 𝕜
f : ↥(simpleFunc E p μ)
⊢ ⇑(toSimpleFunc (k • f)) =ᶠ[ae μ] k • ⇑(toSimpleFunc f)

Tactic:
filter_upwards [toSimpleFunc_eq_toFun (k • f), toSimpleFunc_eq_toFun f,
  Lp.coeFn_smul k (f : Lp E p μ)] with _

Result:
case h
α : Type u_1
E : Type u_4
𝕜 : Type u_6
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : BoundedSMul 𝕜 E
k : 𝕜
f : ↥(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✝

Proof state:
case h
α : Type u_1
E : Type u_4
𝕜 : Type u_6
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : BoundedSMul 𝕜 E
k : 𝕜
f : ↥(simpleFunc E p μ)
a✝ : α
h✝ : (toSimpleFunc (k • f)) a✝ = ↑↑(k • ↑f) a✝
h : (toSimpleFunc f) a✝ = ↑↑↑f a✝
⊢ ↑↑(k • ↑f) a✝ = k • ↑↑↑f a✝ → ↑↑(k • ↑f) a✝ = k • ↑↑↑f a✝

Tactic:
intro h

Result:
case h
α : Type u_1
E : Type u_4
𝕜 : Type u_6
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : BoundedSMul 𝕜 E
k : 𝕜
f : ↥(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✝

Proof state:
case h
α : Type u_1
E : Type u_4
𝕜 : Type u_6
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : BoundedSMul 𝕜 E
k : 𝕜
f : ↥(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✝

Tactic:
simp only [Pi.smul_apply, coe_smul]

Result:
case h
α : Type u_1
E : Type u_4
𝕜 : Type u_6
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : BoundedSMul 𝕜 E
k : 𝕜
f : ↥(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✝

Proof state:
case h
α : Type u_1
E : Type u_4
𝕜 : Type u_6
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : BoundedSMul 𝕜 E
k : 𝕜
f : ↥(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✝

Tactic:
repeat intro h; rw [h]

Result:
no goals