-- Mathlib/MeasureTheory/Function/ConditionalExpectation/AEMeasurable.lean
theorem MemLp.induction_stronglyMeasurable (hm : m ≤ m0) (hp_ne_top : p ≠ ∞) (P : (α → F) → Prop)
    (h_ind : ∀ (c : F) ⦃s⦄, MeasurableSet[m] s → μ s < ∞ → P (s.indicator fun _ => c))
    (h_add : ∀ ⦃f g : α → F⦄, Disjoint (Function.support f) (Function.support g) →
      MemLp f p μ → MemLp g p μ → StronglyMeasurable[m] f → StronglyMeasurable[m] g →
        P f → P g → P (f + g))
    (h_closed : IsClosed {f : lpMeas F ℝ m p μ | P f})
    (h_ae : ∀ ⦃f g⦄, f =ᵐ[μ] g → MemLp f p μ → P f → P g) :
    ∀ ⦃f : α → F⦄, MemLp f p μ → AEStronglyMeasurable[m] f μ → P f

Proof state:
case refine_2
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝² : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
inst✝¹ : Fact (1 ≤ p)
inst✝ : NormedSpace ℝ F
hm : m ≤ m0
hp_ne_top : p ≠ ⊤
P : (α → F) → Prop
h_ind : ∀ (c : F) ⦃s : Set α⦄, MeasurableSet s → μ s < ⊤ → P (s.indicator fun x => c)
h_closed : IsClosed {f | P ↑↑↑f}
h_ae : ∀ ⦃f g : α → F⦄, f =ᶠ[ae μ] g → MemLp f p μ → P f → P g
f✝ : α → F
hf : MemLp f✝ p μ
hfm✝ : AEStronglyMeasurable f✝ μ
f_Lp : ↥(Lp F p μ) := toLp f✝ hf
hfm_Lp : AEStronglyMeasurable (↑↑f_Lp) μ
f g : α → F
hf_mem : MemLp f p μ
hg_mem : MemLp g p μ
hfm : StronglyMeasurable f
hgm : StronglyMeasurable g
h_disj : Disjoint (Function.support f) (Function.support g)
hfP : P ↑↑(toLp f hf_mem)
hgP : P ↑↑(toLp g hg_mem)
hfP' : P f
hgP' : P g
h_add : P (f + g)
⊢ f + g =ᶠ[ae μ] ↑↑(toLp f hf_mem + toLp g hg_mem)

Tactic:
exact (hf_mem.coeFn_toLp.symm.add hg_mem.coeFn_toLp.symm).trans (Lp.coeFn_add _ _).symm

Result:
no goals

Proof state:
case refine_2
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝² : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
inst✝¹ : Fact (1 ≤ p)
inst✝ : NormedSpace ℝ F
hm : m ≤ m0
hp_ne_top : p ≠ ⊤
P : (α → F) → Prop
h_ind : ∀ (c : F) ⦃s : Set α⦄, MeasurableSet s → μ s < ⊤ → P (s.indicator fun x => c)
h_add :
  ∀ ⦃f g : α → F⦄,
    Disjoint (Function.support f) (Function.support g) →
      MemLp f p μ → MemLp g p μ → StronglyMeasurable f → StronglyMeasurable g → P f → P g → P (f + g)
h_closed : IsClosed {f | P ↑↑↑f}
h_ae : ∀ ⦃f g : α → F⦄, f =ᶠ[ae μ] g → MemLp f p μ → P f → P g
f✝ : α → F
hf : MemLp f✝ p μ
hfm✝ : AEStronglyMeasurable f✝ μ
f_Lp : ↥(Lp F p μ) := toLp f✝ hf
hfm_Lp : AEStronglyMeasurable (↑↑f_Lp) μ
f g : α → F
hf_mem : MemLp f p μ
hg_mem : MemLp g p μ
hfm : StronglyMeasurable f
hgm : StronglyMeasurable g
h_disj : Disjoint (Function.support f) (Function.support g)
hfP : P ↑↑(toLp f hf_mem)
hgP : P ↑↑(toLp g hg_mem)
hfP' : P f
hgP' : P g
⊢ P ↑↑(toLp f hf_mem + toLp g hg_mem)

Tactic:
specialize h_add h_disj hf_mem hg_mem hfm hgm hfP' hgP'

Result:
case refine_2
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝² : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
inst✝¹ : Fact (1 ≤ p)
inst✝ : NormedSpace ℝ F
hm : m ≤ m0
hp_ne_top : p ≠ ⊤
P : (α → F) → Prop
h_ind : ∀ (c : F) ⦃s : Set α⦄, MeasurableSet s → μ s < ⊤ → P (s.indicator fun x => c)
h_closed : IsClosed {f | P ↑↑↑f}
h_ae : ∀ ⦃f g : α → F⦄, f =ᶠ[ae μ] g → MemLp f p μ → P f → P g
f✝ : α → F
hf : MemLp f✝ p μ
hfm✝ : AEStronglyMeasurable f✝ μ
f_Lp : ↥(Lp F p μ) := toLp f✝ hf
hfm_Lp : AEStronglyMeasurable (↑↑f_Lp) μ
f g : α → F
hf_mem : MemLp f p μ
hg_mem : MemLp g p μ
hfm : StronglyMeasurable f
hgm : StronglyMeasurable g
h_disj : Disjoint (Function.support f) (Function.support g)
hfP : P ↑↑(toLp f hf_mem)
hgP : P ↑↑(toLp g hg_mem)
hfP' : P f
hgP' : P g
h_add : P (f + g)
⊢ P ↑↑(toLp f hf_mem + toLp g hg_mem)

Proof state:
case refine_2
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝² : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
inst✝¹ : Fact (1 ≤ p)
inst✝ : NormedSpace ℝ F
hm : m ≤ m0
hp_ne_top : p ≠ ⊤
P : (α → F) → Prop
h_ind : ∀ (c : F) ⦃s : Set α⦄, MeasurableSet s → μ s < ⊤ → P (s.indicator fun x => c)
h_closed : IsClosed {f | P ↑↑↑f}
h_ae : ∀ ⦃f g : α → F⦄, f =ᶠ[ae μ] g → MemLp f p μ → P f → P g
f✝ : α → F
hf : MemLp f✝ p μ
hfm✝ : AEStronglyMeasurable f✝ μ
f_Lp : ↥(Lp F p μ) := toLp f✝ hf
hfm_Lp : AEStronglyMeasurable (↑↑f_Lp) μ
f g : α → F
hf_mem : MemLp f p μ
hg_mem : MemLp g p μ
hfm : StronglyMeasurable f
hgm : StronglyMeasurable g
h_disj : Disjoint (Function.support f) (Function.support g)
hfP : P ↑↑(toLp f hf_mem)
hgP : P ↑↑(toLp g hg_mem)
hfP' : P f
hgP' : P g
h_add : P (f + g)
⊢ P ↑↑(toLp f hf_mem + toLp g hg_mem)

Tactic:
refine h_ae ?_ (hf_mem.add hg_mem) h_add

Result:
case refine_2
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝² : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
inst✝¹ : Fact (1 ≤ p)
inst✝ : NormedSpace ℝ F
hm : m ≤ m0
hp_ne_top : p ≠ ⊤
P : (α → F) → Prop
h_ind : ∀ (c : F) ⦃s : Set α⦄, MeasurableSet s → μ s < ⊤ → P (s.indicator fun x => c)
h_closed : IsClosed {f | P ↑↑↑f}
h_ae : ∀ ⦃f g : α → F⦄, f =ᶠ[ae μ] g → MemLp f p μ → P f → P g
f✝ : α → F
hf : MemLp f✝ p μ
hfm✝ : AEStronglyMeasurable f✝ μ
f_Lp : ↥(Lp F p μ) := toLp f✝ hf
hfm_Lp : AEStronglyMeasurable (↑↑f_Lp) μ
f g : α → F
hf_mem : MemLp f p μ
hg_mem : MemLp g p μ
hfm : StronglyMeasurable f
hgm : StronglyMeasurable g
h_disj : Disjoint (Function.support f) (Function.support g)
hfP : P ↑↑(toLp f hf_mem)
hgP : P ↑↑(toLp g hg_mem)
hfP' : P f
hgP' : P g
h_add : P (f + g)
⊢ f + g =ᶠ[ae μ] ↑↑(toLp f hf_mem + toLp g hg_mem)

Proof state:
case refine_2
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝² : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
inst✝¹ : Fact (1 ≤ p)
inst✝ : NormedSpace ℝ F
hm : m ≤ m0
hp_ne_top : p ≠ ⊤
P : (α → F) → Prop
h_ind : ∀ (c : F) ⦃s : Set α⦄, MeasurableSet s → μ s < ⊤ → P (s.indicator fun x => c)
h_add :
  ∀ ⦃f g : α → F⦄,
    Disjoint (Function.support f) (Function.support g) →
      MemLp f p μ → MemLp g p μ → StronglyMeasurable f → StronglyMeasurable g → P f → P g → P (f + g)
h_closed : IsClosed {f | P ↑↑↑f}
h_ae : ∀ ⦃f g : α → F⦄, f =ᶠ[ae μ] g → MemLp f p μ → P f → P g
f✝ : α → F
hf : MemLp f✝ p μ
hfm✝ : AEStronglyMeasurable f✝ μ
f_Lp : ↥(Lp F p μ) := toLp f✝ hf
hfm_Lp : AEStronglyMeasurable (↑↑f_Lp) μ
f g : α → F
hf_mem : MemLp f p μ
hg_mem : MemLp g p μ
hfm : StronglyMeasurable f
hgm : StronglyMeasurable g
h_disj : Disjoint (Function.support f) (Function.support g)
hfP : P ↑↑(toLp f hf_mem)
hgP : P ↑↑(toLp g hg_mem)
hfP' : P f
⊢ P ↑↑(toLp f hf_mem + toLp g hg_mem)

Tactic:
have hgP' : P g := h_ae hg_mem.coeFn_toLp (Lp.memLp _) hgP

Result:
case refine_2
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝² : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
inst✝¹ : Fact (1 ≤ p)
inst✝ : NormedSpace ℝ F
hm : m ≤ m0
hp_ne_top : p ≠ ⊤
P : (α → F) → Prop
h_ind : ∀ (c : F) ⦃s : Set α⦄, MeasurableSet s → μ s < ⊤ → P (s.indicator fun x => c)
h_add :
  ∀ ⦃f g : α → F⦄,
    Disjoint (Function.support f) (Function.support g) →
      MemLp f p μ → MemLp g p μ → StronglyMeasurable f → StronglyMeasurable g → P f → P g → P (f + g)
h_closed : IsClosed {f | P ↑↑↑f}
h_ae : ∀ ⦃f g : α → F⦄, f =ᶠ[ae μ] g → MemLp f p μ → P f → P g
f✝ : α → F
hf : MemLp f✝ p μ
hfm✝ : AEStronglyMeasurable f✝ μ
f_Lp : ↥(Lp F p μ) := toLp f✝ hf
hfm_Lp : AEStronglyMeasurable (↑↑f_Lp) μ
f g : α → F
hf_mem : MemLp f p μ
hg_mem : MemLp g p μ
hfm : StronglyMeasurable f
hgm : StronglyMeasurable g
h_disj : Disjoint (Function.support f) (Function.support g)
hfP : P ↑↑(toLp f hf_mem)
hgP : P ↑↑(toLp g hg_mem)
hfP' : P f
hgP' : P g
⊢ P ↑↑(toLp f hf_mem + toLp g hg_mem)