-- Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean
theorem MemLp.induction [_i : Fact (1 ≤ p)] (hp_ne_top : p ≠ ∞) (P : (α → E) → Prop)
    (h_ind : ∀ (c : E) ⦃s⦄, MeasurableSet s → μ s < ∞ → P (s.indicator fun _ => c))
    (h_add : ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → MemLp f p μ → MemLp g p μ →
      P f → P g → P (f + g))
    (h_closed : IsClosed { f : Lp E p μ | P f })
    (h_ae : ∀ ⦃f g⦄, f =ᵐ[μ] g → MemLp f p μ → P f → P g) :
    ∀ ⦃f : α → E⦄, MemLp f p μ → P f

Proof state:
case h_add
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
_i : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
P : (α → E) → Prop
h_ind : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → μ s < ⊤ → P (s.indicator fun x => c)
h_add : ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → MemLp f p μ → MemLp g p μ → P f → P g → P (f + g)
h_closed : IsClosed {f | P ↑↑f}
h_ae : ∀ ⦃f g : α → E⦄, f =ᶠ[ae μ] g → MemLp f p μ → P f → P g
⊢ ∀ ⦃f g : α →ₛ E⦄,
    Disjoint (support ⇑f) (support ⇑g) →
      (MemLp (⇑f) p μ → P ⇑f) → (MemLp (⇑g) p μ → P ⇑g) → MemLp (⇑(f + g)) p μ → P ⇑(f + g)

Tactic:
intro f g hfg hf hg int_fg

Result:
case h_add
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
_i : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
P : (α → E) → Prop
h_ind : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → μ s < ⊤ → P (s.indicator fun x => c)
h_add : ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → MemLp f p μ → MemLp g p μ → P f → P g → P (f + g)
h_closed : IsClosed {f | P ↑↑f}
h_ae : ∀ ⦃f g : α → E⦄, f =ᶠ[ae μ] g → MemLp f p μ → P f → P g
f g : α →ₛ E
hfg : Disjoint (support ⇑f) (support ⇑g)
hf : MemLp (⇑f) p μ → P ⇑f
hg : MemLp (⇑g) p μ → P ⇑g
int_fg : MemLp (⇑(f + g)) p μ
⊢ P ⇑(f + g)

Proof state:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
_i : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
P : (α → E) → Prop
h_ind : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → μ s < ⊤ → P (s.indicator fun x => c)
h_add : ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → MemLp f p μ → MemLp g p μ → P f → P g → P (f + g)
h_closed : IsClosed {f | P ↑↑f}
h_ae : ∀ ⦃f g : α → E⦄, f =ᶠ[ae μ] g → MemLp f p μ → P f → P g
this : ∀ (f : α →ₛ E), MemLp (⇑f) p μ → P ⇑f
⊢ ∀ (f : ↥(Lp.simpleFunc E p μ)), P ↑↑↑f

Tactic:
intro f

Result:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
_i : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
P : (α → E) → Prop
h_ind : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → μ s < ⊤ → P (s.indicator fun x => c)
h_add : ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → MemLp f p μ → MemLp g p μ → P f → P g → P (f + g)
h_closed : IsClosed {f | P ↑↑f}
h_ae : ∀ ⦃f g : α → E⦄, f =ᶠ[ae μ] g → MemLp f p μ → P f → P g
this : ∀ (f : α →ₛ E), MemLp (⇑f) p μ → P ⇑f
f : ↥(Lp.simpleFunc E p μ)
⊢ P ↑↑↑f

Proof state:
case h_add
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
_i : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
P : (α → E) → Prop
h_ind : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → μ s < ⊤ → P (s.indicator fun x => c)
h_add : ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → MemLp f p μ → MemLp g p μ → P f → P g → P (f + g)
h_closed : IsClosed {f | P ↑↑f}
h_ae : ∀ ⦃f g : α → E⦄, f =ᶠ[ae μ] g → MemLp f p μ → P f → P g
f g : α →ₛ E
hfg : Disjoint (support ⇑f) (support ⇑g)
hf : MemLp (⇑f) p μ → P ⇑f
hg : MemLp (⇑g) p μ → P ⇑g
int_fg : MemLp (⇑(f + g)) p μ
⊢ P ⇑(f + g)

Tactic:
rw [SimpleFunc.coe_add,
  memLp_add_of_disjoint hfg f.stronglyMeasurable g.stronglyMeasurable] at int_fg

Result:
case h_add
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
_i : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
P : (α → E) → Prop
h_ind : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → μ s < ⊤ → P (s.indicator fun x => c)
h_add : ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → MemLp f p μ → MemLp g p μ → P f → P g → P (f + g)
h_closed : IsClosed {f | P ↑↑f}
h_ae : ∀ ⦃f g : α → E⦄, f =ᶠ[ae μ] g → MemLp f p μ → P f → P g
f g : α →ₛ E
hfg : Disjoint (support ⇑f) (support ⇑g)
hf : MemLp (⇑f) p μ → P ⇑f
hg : MemLp (⇑g) p μ → P ⇑g
int_fg : MemLp (⇑f) p μ ∧ MemLp (⇑g) p μ
⊢ P ⇑(f + g)

Proof state:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
_i : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
P : (α → E) → Prop
h_ind : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → μ s < ⊤ → P (s.indicator fun x => c)
h_add : ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → MemLp f p μ → MemLp g p μ → P f → P g → P (f + g)
h_closed : IsClosed {f | P ↑↑f}
h_ae : ∀ ⦃f g : α → E⦄, f =ᶠ[ae μ] g → MemLp f p μ → P f → P g
this✝ : ∀ (f : α →ₛ E), MemLp (⇑f) p μ → P ⇑f
this : ∀ (f : ↥(Lp.simpleFunc E p μ)), P ↑↑↑f
⊢ ∀ ⦃f : α → E⦄, MemLp f p μ → P f

Tactic:
have : ∀ f : Lp E p μ, P f := fun f =>
  (Lp.simpleFunc.denseRange hp_ne_top).induction_on f h_closed this

Result:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
_i : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
P : (α → E) → Prop
h_ind : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → μ s < ⊤ → P (s.indicator fun x => c)
h_add : ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → MemLp f p μ → MemLp g p μ → P f → P g → P (f + g)
h_closed : IsClosed {f | P ↑↑f}
h_ae : ∀ ⦃f g : α → E⦄, f =ᶠ[ae μ] g → MemLp f p μ → P f → P g
this✝¹ : ∀ (f : α →ₛ E), MemLp (⇑f) p μ → P ⇑f
this✝ : ∀ (f : ↥(Lp.simpleFunc E p μ)), P ↑↑↑f
this : ∀ (f : ↥(Lp E p μ)), P ↑↑f
⊢ ∀ ⦃f : α → E⦄, MemLp f p μ → P f

Proof state:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
_i : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
P : (α → E) → Prop
h_ind : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → μ s < ⊤ → P (s.indicator fun x => c)
h_add : ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → MemLp f p μ → MemLp g p μ → P f → P g → P (f + g)
h_closed : IsClosed {f | P ↑↑f}
h_ae : ∀ ⦃f g : α → E⦄, f =ᶠ[ae μ] g → MemLp f p μ → P f → P g
s : Set α
hs : MeasurableSet s
h : MemLp (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α 0) (SimpleFunc.const α 0))) p μ
⊢ μ ∅ < ⊤

Tactic:
simp

Result:
no goals