-- 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:
case h.e'_1
α : 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 μ
hc : c = 0
⊢ toLp (SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) hf = indicatorConst p ⋯ ⋯ 0

Tactic:
ext1

Result:
case h.e'_1.a
α : 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 μ
hc : c = 0
⊢ ↑(toLp (SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) hf) = ↑(indicatorConst p ⋯ ⋯ 0)

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⦄,
    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)

Tactic:
intro f g hfg hf hg hfg'

Result:
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')

Proof state:
case pos
α : 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 μ
hc : c = 0
⊢ P (toLp (SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) hf)

Tactic:
convert h_ind 0 MeasurableSet.empty (by simp) using 1

Result:
case h.e'_1
α : 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 μ
hc : c = 0
⊢ toLp (SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) hf = indicatorConst p ⋯ ⋯ 0

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 (toLp (toSimpleFunc f) ⋯)

Tactic:
apply this

Result:
no goals

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 μ)
⊢ P f

Tactic:
suffices ∀ f : α →ₛ E, ∀ hf : MemLp f p μ, P (toLp f hf) by
  rw [← toLp_toSimpleFunc f]
  apply this

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 μ)
⊢ ∀ (f : α →ₛ E) (hf : MemLp (⇑f) p μ), P (toLp f hf)

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 μ)
⊢ ∀ (f : α →ₛ E) (hf : MemLp (⇑f) p μ), P (toLp f hf)

Tactic:
clear 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 : α →ₛ E) (hf : MemLp (⇑f) p μ), P (toLp f hf)