-- 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 pos
α : 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 μ
⊢ P ⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α 0) (SimpleFunc.const α 0))

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 α
_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 μ
⊢ ⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α 0) (SimpleFunc.const α 0)) = ∅.indicator fun x => 0

Proof state:
case neg
α : 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
c : E
s : Set α
hs : MeasurableSet s
h : MemLp (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))) p μ
hc : ¬c = 0
hp_pos : p ≠ 0
⊢ P ⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))

Tactic:
exact h_ind c hs (SimpleFunc.measure_lt_top_of_memLp_indicator hp_pos hp_ne_top hc hs h)

Result:
no goals

Proof state:
case h_ind
α : 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
⊢ ∀ (c : E) {s : Set α} (hs : MeasurableSet s),
    MemLp (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))) p μ →
      P ⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))

Tactic:
intro c s hs h

Result:
case h_ind
α : 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
c : E
s : Set α
hs : MeasurableSet s
h : MemLp (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))) p μ
⊢ P ⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))

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) p μ ∧ MemLp (⇑g) p μ
⊢ P ⇑(f + g)

Tactic:
exact h_add hfg int_fg.1 int_fg.2 (hf int_fg.1) (hg int_fg.2)

Result:
no goals

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 : α → E⦄, MemLp f p μ → P f

Tactic:
have : ∀ f : Lp.simpleFunc E p μ, P f := by
  intro f
  exact
    h_ae (Lp.simpleFunc.toSimpleFunc_eq_toFun f) (Lp.simpleFunc.memLp f)
      (this (Lp.simpleFunc.toSimpleFunc f) (Lp.simpleFunc.memLp 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
this : ∀ (f : ↥(Lp.simpleFunc E p μ)), P ↑↑↑f
⊢ ∀ ⦃f : α → E⦄, MemLp f p μ → P f

Proof state:
case pos
α : 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
c : E
s : Set α
hs : MeasurableSet s
h : MemLp (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))) p μ
hc : c = 0
⊢ P ⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))

Tactic:
subst hc

Result:
case pos
α : 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 μ
⊢ P ⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α 0) (SimpleFunc.const α 0))