-- Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean
theorem induction (hp_pos : p ≠ 0) (hp_ne_top : p ≠ ∞) {P : Lp.simpleFunc E p μ → Prop}
    (h_ind :
      ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ∞),
        P (Lp.simpleFunc.indicatorConst p hs hμs.ne c))
    (h_add :
      ∀ ⦃f g : α →ₛ E⦄,
        ∀ hf : MemLp f p μ,
          ∀ hg : MemLp g p μ,
            Disjoint (support f) (support g) →
              P (Lp.simpleFunc.toLp f hf) →
                P (Lp.simpleFunc.toLp g hg) → P (Lp.simpleFunc.toLp f hf + Lp.simpleFunc.toLp g hg))
    (f : Lp.simpleFunc E p μ) : P f

Proof state:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
P : ↥(simpleFunc E p μ) → Prop
h_ind : ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ⊤), P (indicatorConst p hs ⋯ c)
h_add :
  ∀ ⦃f g : α →ₛ E⦄ (hf : MemLp (⇑f) p μ) (hg : MemLp (⇑g) p μ),
    Disjoint (support ⇑f) (support ⇑g) → P (toLp f hf) → P (toLp g hg) → P (toLp f hf + toLp g hg)
f : ↥(simpleFunc E p μ)
this : ∀ (f : α →ₛ E) (hf : MemLp (⇑f) p μ), P (toLp f hf)
⊢ P f

Tactic:
rw [← toLp_toSimpleFunc f]

Result:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
P : ↥(simpleFunc E p μ) → Prop
h_ind : ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ⊤), P (indicatorConst p hs ⋯ c)
h_add :
  ∀ ⦃f g : α →ₛ E⦄ (hf : MemLp (⇑f) p μ) (hg : MemLp (⇑g) p μ),
    Disjoint (support ⇑f) (support ⇑g) → P (toLp f hf) → P (toLp g hg) → P (toLp f hf + toLp g hg)
f : ↥(simpleFunc E p μ)
this : ∀ (f : α →ₛ E) (hf : MemLp (⇑f) p μ), P (toLp f hf)
⊢ P (toLp (toSimpleFunc f) ⋯)

Proof state:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
P : ↥(simpleFunc E p μ) → Prop
h_ind : ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ⊤), P (indicatorConst p hs ⋯ c)
h_add :
  ∀ ⦃f g : α →ₛ E⦄ (hf : MemLp (⇑f) p μ) (hg : MemLp (⇑g) p μ),
    Disjoint (support ⇑f) (support ⇑g) → P (toLp f hf) → P (toLp g hg) → P (toLp f hf + toLp g hg)
⊢ ∀ (f : α →ₛ E) (hf : MemLp (⇑f) p μ), P (toLp f hf)

Tactic:
apply SimpleFunc.induction

Result:
case h_ind
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
P : ↥(simpleFunc E p μ) → Prop
h_ind : ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ⊤), P (indicatorConst p hs ⋯ c)
h_add :
  ∀ ⦃f g : α →ₛ E⦄ (hf : MemLp (⇑f) p μ) (hg : MemLp (⇑g) p μ),
    Disjoint (support ⇑f) (support ⇑g) → P (toLp f hf) → P (toLp g hg) → P (toLp f hf + toLp g hg)
⊢ ∀ (c : E) {s : Set α} (hs : MeasurableSet s)
    (hf : MemLp (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))) p μ),
    P (toLp (SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) hf)

case h_add
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
P : ↥(simpleFunc E p μ) → Prop
h_ind : ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ⊤), P (indicatorConst p hs ⋯ c)
h_add :
  ∀ ⦃f g : α →ₛ E⦄ (hf : MemLp (⇑f) p μ) (hg : MemLp (⇑g) p μ),
    Disjoint (support ⇑f) (support ⇑g) → P (toLp f hf) → P (toLp g hg) → P (toLp f hf + toLp g hg)
⊢ ∀ ⦃f g : α →ₛ E⦄,
    Disjoint (support ⇑f) (support ⇑g) →
      (∀ (hf : MemLp (⇑f) p μ), P (toLp f hf)) →
        (∀ (hf : MemLp (⇑g) p μ), P (toLp g hf)) → ∀ (hf : MemLp (⇑(f + g)) p μ), P (toLp (f + g) hf)

Proof state:
case h_add
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
P : ↥(simpleFunc E p μ) → Prop
h_ind : ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ⊤), P (indicatorConst p hs ⋯ c)
h_add :
  ∀ ⦃f g : α →ₛ E⦄ (hf : MemLp (⇑f) p μ) (hg : MemLp (⇑g) p μ),
    Disjoint (support ⇑f) (support ⇑g) → P (toLp f hf) → P (toLp g hg) → P (toLp f hf + toLp g hg)
f g : α →ₛ E
hfg : Disjoint (support ⇑f) (support ⇑g)
hf : ∀ (hf : MemLp (⇑f) p μ), P (toLp f hf)
hg : ∀ (hf : MemLp (⇑g) p μ), P (toLp g hf)
hfg' : MemLp (⇑(f + g)) p μ
⊢ P (toLp (f + g) hfg')

Tactic:
obtain ⟨hf', hg'⟩ : MemLp f p μ ∧ MemLp g p μ :=
  (memLp_add_of_disjoint hfg f.stronglyMeasurable g.stronglyMeasurable).mp hfg'

Result:
case h_add.intro
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
P : ↥(simpleFunc E p μ) → Prop
h_ind : ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ⊤), P (indicatorConst p hs ⋯ c)
h_add :
  ∀ ⦃f g : α →ₛ E⦄ (hf : MemLp (⇑f) p μ) (hg : MemLp (⇑g) p μ),
    Disjoint (support ⇑f) (support ⇑g) → P (toLp f hf) → P (toLp g hg) → P (toLp f hf + toLp g hg)
f g : α →ₛ E
hfg : Disjoint (support ⇑f) (support ⇑g)
hf : ∀ (hf : MemLp (⇑f) p μ), P (toLp f hf)
hg : ∀ (hf : MemLp (⇑g) p μ), P (toLp g hf)
hfg' : MemLp (⇑(f + g)) p μ
hf' : MemLp (⇑f) p μ
hg' : MemLp (⇑g) p μ
⊢ P (toLp (f + g) hfg')