-- Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean
theorem sub_toSimpleFunc (f g : Lp.simpleFunc E p μ) :
    toSimpleFunc (f - g) =ᵐ[μ] toSimpleFunc f - toSimpleFunc g

Proof state:
case h
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f g : ↥(simpleFunc E p μ)
a✝ : α
⊢ (toSimpleFunc (f - g)) a✝ = ↑(↑↑f - ↑↑g) a✝ →
    (toSimpleFunc f) a✝ = ↑↑↑f a✝ →
      (toSimpleFunc g) a✝ = ↑↑↑g a✝ →
        ↑(↑↑f - ↑↑g) a✝ = ↑↑↑f a✝ - ↑↑↑g a✝ → (toSimpleFunc (f - g)) a✝ = (toSimpleFunc f) a✝ - (toSimpleFunc g) a✝

Tactic:
repeat' intro h; rw [h]

Result:
no goals

Proof state:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f g : ↥(simpleFunc E p μ)
⊢ ⇑(toSimpleFunc (f - g)) =ᶠ[ae μ] ⇑(toSimpleFunc f) - ⇑(toSimpleFunc g)

Tactic:
filter_upwards [toSimpleFunc_eq_toFun (f - g), toSimpleFunc_eq_toFun f,
  toSimpleFunc_eq_toFun g, Lp.coeFn_sub (f : Lp E p μ) g] with _

Result:
case h
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f g : ↥(simpleFunc E p μ)
a✝ : α
⊢ (toSimpleFunc (f - g)) a✝ = ↑↑↑(f - g) a✝ →
    (toSimpleFunc f) a✝ = ↑↑↑f a✝ →
      (toSimpleFunc g) a✝ = ↑↑↑g a✝ →
        ↑↑(↑f - ↑g) a✝ = (↑↑↑f - ↑↑↑g) a✝ → (toSimpleFunc (f - g)) a✝ = (⇑(toSimpleFunc f) - ⇑(toSimpleFunc g)) a✝

Proof state:
case h
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f g : ↥(simpleFunc E p μ)
a✝ : α
⊢ (toSimpleFunc (f - g)) a✝ = ↑↑↑(f - g) a✝ →
    (toSimpleFunc f) a✝ = ↑↑↑f a✝ →
      (toSimpleFunc g) a✝ = ↑↑↑g a✝ →
        ↑↑(↑f - ↑g) a✝ = (↑↑↑f - ↑↑↑g) a✝ → (toSimpleFunc (f - g)) a✝ = (⇑(toSimpleFunc f) - ⇑(toSimpleFunc g)) a✝

Tactic:
simp only [AddSubgroup.coe_sub, Pi.sub_apply]

Result:
case h
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f g : ↥(simpleFunc E p μ)
a✝ : α
⊢ (toSimpleFunc (f - g)) a✝ = ↑(↑↑f - ↑↑g) a✝ →
    (toSimpleFunc f) a✝ = ↑↑↑f a✝ →
      (toSimpleFunc g) a✝ = ↑↑↑g a✝ →
        ↑(↑↑f - ↑↑g) a✝ = ↑↑↑f a✝ - ↑↑↑g a✝ → (toSimpleFunc (f - g)) a✝ = (toSimpleFunc f) a✝ - (toSimpleFunc g) a✝

Proof state:
case h
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f g : ↥(simpleFunc E p μ)
a✝ : α
h✝² : (toSimpleFunc (f - g)) a✝ = ↑(↑↑f - ↑↑g) a✝
h✝¹ : (toSimpleFunc f) a✝ = ↑↑↑f a✝
h✝ : (toSimpleFunc g) a✝ = ↑↑↑g a✝
h : ↑(↑↑f - ↑↑g) a✝ = ↑↑↑f a✝ - ↑↑↑g a✝
⊢ ↑(↑↑f - ↑↑g) a✝ = ↑↑↑f a✝ - ↑↑↑g a✝

Tactic:
rw [h]

Result:
no goals

Proof state:
case h
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f g : ↥(simpleFunc E p μ)
a✝ : α
h✝¹ : (toSimpleFunc (f - g)) a✝ = ↑(↑↑f - ↑↑g) a✝
h✝ : (toSimpleFunc f) a✝ = ↑↑↑f a✝
h : (toSimpleFunc g) a✝ = ↑↑↑g a✝
⊢ ↑(↑↑f - ↑↑g) a✝ = ↑↑↑f a✝ - ↑↑↑g a✝ → ↑(↑↑f - ↑↑g) a✝ = ↑↑↑f a✝ - ↑↑↑g a✝

Tactic:
intro h

Result:
case h
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f g : ↥(simpleFunc E p μ)
a✝ : α
h✝² : (toSimpleFunc (f - g)) a✝ = ↑(↑↑f - ↑↑g) a✝
h✝¹ : (toSimpleFunc f) a✝ = ↑↑↑f a✝
h✝ : (toSimpleFunc g) a✝ = ↑↑↑g a✝
h : ↑(↑↑f - ↑↑g) a✝ = ↑↑↑f a✝ - ↑↑↑g a✝
⊢ ↑(↑↑f - ↑↑g) a✝ = ↑↑↑f a✝ - ↑↑↑g a✝