awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable (goal)
Goal:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup F
m m0 : MeasurableSpace α
one_le_p : Fact (1 ≤ p)
inst_1 : NormedSpace ℝ F
hm : m ≤ m0
s : Set α
μ : Measure α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : F
⊢ (↑(↑(↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F ℝ p μ hm) : (a : ↥(Lp F p (μ.trim hm))) → ↥(lpMeas F ℝ m p μ))
                  (indicatorConstLp (s := s) p hs hμs c)) :
              ↥(Lp F p μ)) :
          α →ₘ[μ] F) :
      α → F) =ᶠ[ae μ]
    (↑(↑(indicatorConstLp (s := s) p ⋯ ⋯ c) : α →ₘ[μ] F) : α → F)
have h : (↑(↑(↑(lpTrimToLpMeas F ℝ p μ hm (indicatorConstLp (s := s) p hs hμs c)) : ↥(Lp F p μ)) : α →ₘ[μ] F) : α → F) =ᶠ[ae μ]
  (↑(↑(indicatorConstLp (s := s) p sorry sorry c) : α →ₘ[μ] F) : α → F)
Tactic: change
    lpTrimToLpMeas F ℝ p μ hm (indicatorConstLp p hs hμs c) =ᵐ[μ]
      (indicatorConstLp p _ _ c : α → F)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable (goal)
Goal:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup F
m m0 : MeasurableSpace α
one_le_p : Fact (1 ≤ p)
inst_1 : NormedSpace ℝ F
hm : m ≤ m0
s : Set α
μ : Measure α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : F
⊢ (↑(↑(↑(lpTrimToLpMeas F ℝ p μ hm (indicatorConstLp (s := s) p hs hμs c)) : ↥(Lp F p μ)) : α →ₘ[μ] F) : α → F) =ᶠ[ae μ]
    (↑(↑(indicatorConstLp (s := s) p ⋯ ⋯ c) : α →ₘ[μ] F) : α → F)
have h : (↑(↑(indicatorConstLp (s := s) p hs hμs c) : α →ₘ[μ.trim hm] F) : α → F) =ᶠ[ae μ]
  (↑(↑(indicatorConstLp (s := s) p sorry sorry c) : α →ₘ[μ] F) : α → F)
Tactic: grw [lpTrimToLpMeas_ae_eq, ae_eq_of_ae_eq_trim indicatorConstLp_coeFn, indicatorConstLp_coeFn]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable (goal)
Goal:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup F
m m0 : MeasurableSpace α
one_le_p : Fact (1 ≤ p)
inst_1 : NormedSpace ℝ F
hm : m ≤ m0
s : Set α
μ : Measure α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : F
h :
  (↑(↑(indicatorConstLp (s := s) p hs hμs c) : α →ₘ[μ.trim hm] F) : α → F) =ᶠ[ae μ]
    (↑(↑(indicatorConstLp (s := s) p ⋯ ⋯ c) : α →ₘ[μ] F) : α → F)
⊢ (↑(↑(↑(lpTrimToLpMeas F ℝ p μ hm (indicatorConstLp (s := s) p hs hμs c)) : ↥(Lp F p μ)) : α →ₘ[μ] F) : α → F) =ᶠ[ae μ]
    (↑(↑(indicatorConstLp (s := s) p ⋯ ⋯ c) : α →ₘ[μ] F) : α → F)
have h₁ : (s.indicator fun (x : α) ↦ c) =ᶠ[ae μ] (↑(↑(indicatorConstLp (s := s) p sorry sorry c) : α →ₘ[μ] F) : α → F)
Tactic: grw [lpTrimToLpMeas_ae_eq, ae_eq_of_ae_eq_trim indicatorConstLp_coeFn, indicatorConstLp_coeFn]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable (goal)
Goal:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup F
m m0 : MeasurableSpace α
one_le_p : Fact (1 ≤ p)
inst_1 : NormedSpace ℝ F
hm : m ≤ m0
s : Set α
μ : Measure α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : F
h :
  (↑(↑(indicatorConstLp (s := s) p hs hμs c) : α →ₘ[μ.trim hm] F) : α → F) =ᶠ[ae μ]
    (↑(↑(indicatorConstLp (s := s) p ⋯ ⋯ c) : α →ₘ[μ] F) : α → F)
h₁ : (s.indicator fun (x : α) ↦ c) =ᶠ[ae μ] (↑(↑(indicatorConstLp (s := s) p ⋯ ⋯ c) : α →ₘ[μ] F) : α → F)
⊢ (↑(↑(↑(lpTrimToLpMeas F ℝ p μ hm (indicatorConstLp (s := s) p hs hμs c)) : ↥(Lp F p μ)) : α →ₘ[μ] F) : α → F) =ᶠ[ae μ]
    (↑(↑(indicatorConstLp (s := s) p ⋯ ⋯ c) : α →ₘ[μ] F) : α → F)
have h₂ : EventuallyEq.{u_1, u_2} (β := F) (ae μ) (s.indicator fun (x : α) ↦ c) (s.indicator fun (x : α) ↦ c)
Tactic: grw [lpTrimToLpMeas_ae_eq, ae_eq_of_ae_eq_trim indicatorConstLp_coeFn, indicatorConstLp_coeFn]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable (goal)
Goal:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
one_le_p : Fact (1 ≤ p)
inst_1 : NormedSpace ℝ F
hm : m ≤ m0
f : α → F
hf : MemLp f p (μ.trim hm)
⊢ (↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F ℝ p μ hm) : (a : ↥(Lp F p (μ.trim hm))) → ↥(lpMeas F ℝ m p μ))
          (MemLp.toLp f hf)) :
      ↥(Lp F p μ)) =
    MemLp.toLp f ⋯
have h : (↑(↑(↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F ℝ p μ hm) : (a : ↥(Lp F p (μ.trim hm))) → ↥(lpMeas F ℝ m p μ))
                (MemLp.toLp f hf)) :
            ↥(Lp F p μ)) :
        α →ₘ[μ] F) :
    α → F) =ᶠ[ae μ]
  (↑(↑(MemLp.toLp f sorry) : α →ₘ[μ] F) : α → F)
Tactic: ext1
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable (goal)
Goal:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
one_le_p : Fact (1 ≤ p)
inst_1 : NormedSpace ℝ F
hm : m ≤ m0
f : α → F
hf : MemLp f p (μ.trim hm)
⊢ (↑(↑(↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F ℝ p μ hm) : (a : ↥(Lp F p (μ.trim hm))) → ↥(lpMeas F ℝ m p μ))
                  (MemLp.toLp f hf)) :
              ↥(Lp F p μ)) :
          α →ₘ[μ] F) :
      α → F) =ᶠ[ae μ]
    (↑(↑(MemLp.toLp f ⋯) : α →ₘ[μ] F) : α → F)
have h : (↑(↑(↑(lpTrimToLpMeas F ℝ p μ hm (MemLp.toLp f hf)) : ↥(Lp F p μ)) : α →ₘ[μ] F) : α → F) =ᶠ[ae μ]
  (↑(↑(MemLp.toLp f sorry) : α →ₘ[μ] F) : α → F)
Tactic: change lpTrimToLpMeas F ℝ p μ hm (MemLp.toLp f hf) =ᵐ[μ] (MemLp.toLp f _ : α → F)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable (goal)
Goal:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
one_le_p : Fact (1 ≤ p)
inst_1 : NormedSpace ℝ F
hm : m ≤ m0
f : α → F
hf : MemLp f p (μ.trim hm)
⊢ (↑(↑(↑(lpTrimToLpMeas F ℝ p μ hm (MemLp.toLp f hf)) : ↥(Lp F p μ)) : α →ₘ[μ] F) : α → F) =ᶠ[ae μ]
    (↑(↑(MemLp.toLp f ⋯) : α →ₘ[μ] F) : α → F)
have h : (↑(↑(MemLp.toLp f hf) : α →ₘ[μ.trim hm] F) : α → F) =ᶠ[ae μ] (↑(↑(MemLp.toLp f sorry) : α →ₘ[μ] F) : α → F)
Tactic: grw [lpTrimToLpMeas_ae_eq, ae_eq_of_ae_eq_trim (MemLp.coeFn_toLp hf), MemLp.coeFn_toLp]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable (goal)
Goal:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
one_le_p : Fact (1 ≤ p)
inst_1 : NormedSpace ℝ F
hm : m ≤ m0
f : α → F
hf : MemLp f p (μ.trim hm)
h : (↑(↑(MemLp.toLp f hf) : α →ₘ[μ.trim hm] F) : α → F) =ᶠ[ae μ] (↑(↑(MemLp.toLp f ⋯) : α →ₘ[μ] F) : α → F)
⊢ (↑(↑(↑(lpTrimToLpMeas F ℝ p μ hm (MemLp.toLp f hf)) : ↥(Lp F p μ)) : α →ₘ[μ] F) : α → F) =ᶠ[ae μ]
    (↑(↑(MemLp.toLp f ⋯) : α →ₘ[μ] F) : α → F)
have h₁ : f =ᶠ[ae μ] (↑(↑(MemLp.toLp f sorry) : α →ₘ[μ] F) : α → F)
Tactic: grw [lpTrimToLpMeas_ae_eq, ae_eq_of_ae_eq_trim (MemLp.coeFn_toLp hf), MemLp.coeFn_toLp]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable (goal)
Goal:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
one_le_p : Fact (1 ≤ p)
inst_1 : NormedSpace ℝ F
hm : m ≤ m0
f : α → F
hf : MemLp f p (μ.trim hm)
h : (↑(↑(MemLp.toLp f hf) : α →ₘ[μ.trim hm] F) : α → F) =ᶠ[ae μ] (↑(↑(MemLp.toLp f ⋯) : α →ₘ[μ] F) : α → F)
h₁ : f =ᶠ[ae μ] (↑(↑(MemLp.toLp f ⋯) : α →ₘ[μ] F) : α → F)
⊢ (↑(↑(↑(lpTrimToLpMeas F ℝ p μ hm (MemLp.toLp f hf)) : ↥(Lp F p μ)) : α →ₘ[μ] F) : α → F) =ᶠ[ae μ]
    (↑(↑(MemLp.toLp f ⋯) : α →ₘ[μ] F) : α → F)
have h₂ : f =ᶠ[ae μ] f
Tactic: grw [lpTrimToLpMeas_ae_eq, ae_eq_of_ae_eq_trim (MemLp.coeFn_toLp hf), MemLp.coeFn_toLp]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable (hypothesis)
Goal:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
inst_1 : Fact (1 ≤ p)
inst_2 : NormedSpace ℝ F
hm : m ≤ m0
hp_ne_top : p ≠ ∞
P : ↥(Lp F p μ) → Prop
h_ind :
  ∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    P (↑(simpleFunc.indicatorConst p (s := s) ⋯ ⋯ c) : ↥(Lp F p μ))
h_add :
  ∀ ⦃f g : α → F⦄ (hf : MemLp f p μ) (hg : MemLp g p μ),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ →
        Disjoint (Function.support f) (Function.support g) →
          P (MemLp.toLp f hf) → P (MemLp.toLp g hg) → P (MemLp.toLp f hf + MemLp.toLp g hg)
h_closed : IsClosed (X := ↥(lpMeas F ℝ m p μ)) {f : ↥(lpMeas F ℝ m p μ) | P (↑f : ↥(Lp F p μ))}
f : ↥(Lp F p μ)
hf : AEStronglyMeasurable (↑(↑f : α →ₘ[μ] F) : α → F) μ
f' : ↥(lpMeas F ℝ m p μ) :=
  Subtype.mk (p := fun (x : ↥(Lp F p μ)) ↦ Membership.mem (γ := Submodule ℝ ↥(Lp F p μ)) (lpMeas F ℝ m p μ) x) f hf
g : ↥(Lp F p (μ.trim hm)) := (lpMeasToLpTrimLie F ℝ p μ hm : (a : ↥(lpMeas F ℝ m p μ)) → ↥(Lp F p (μ.trim hm))) f'
⊢ P f
have hfg : f' = (LinearIsometryEquiv.symm (lpMeasToLpTrimLie F ℝ p μ hm) : (a : ↥(Lp F p (μ.trim hm))) → ↥(lpMeas F ℝ m p μ)) g
Tactic: have hfg : f' = (lpMeasToLpTrimLie F ℝ p μ hm).symm g := by
    simp only [f', g, LinearIsometryEquiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable (goal)
Goal:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
inst_1 : Fact (1 ≤ p)
inst_2 : NormedSpace ℝ F
hm : m ≤ m0
hp_ne_top : p ≠ ∞
P : ↥(Lp F p μ) → Prop
h_ind :
  ∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    P (↑(simpleFunc.indicatorConst p (s := s) ⋯ ⋯ c) : ↥(Lp F p μ))
h_add :
  ∀ ⦃f g : α → F⦄ (hf : MemLp f p μ) (hg : MemLp g p μ),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ →
        Disjoint (Function.support f) (Function.support g) →
          P (MemLp.toLp f hf) → P (MemLp.toLp g hg) → P (MemLp.toLp f hf + MemLp.toLp g hg)
h_closed : IsClosed (X := ↥(lpMeas F ℝ m p μ)) {f : ↥(lpMeas F ℝ m p μ) | P (↑f : ↥(Lp F p μ))}
f : ↥(Lp F p μ)
hf : AEStronglyMeasurable (↑(↑f : α →ₘ[μ] F) : α → F) μ
f' : ↥(lpMeas F ℝ m p μ) :=
  Subtype.mk (p := fun (x : ↥(Lp F p μ)) ↦ Membership.mem (γ := Submodule ℝ ↥(Lp F p μ)) (lpMeas F ℝ m p μ) x) f hf
g : ↥(Lp F p (μ.trim hm)) := (lpMeasToLpTrimLie F ℝ p μ hm : (a : ↥(lpMeas F ℝ m p μ)) → ↥(Lp F p (μ.trim hm))) f'
hfg :
  f' = (LinearIsometryEquiv.symm (lpMeasToLpTrimLie F ℝ p μ hm) : (a : ↥(Lp F p (μ.trim hm))) → ↥(lpMeas F ℝ m p μ)) g
⊢ P f
have change : P (↑f' : ↥(Lp F p μ))
Tactic: change P ↑f'
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable (goal)
Goal:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
inst_1 : Fact (1 ≤ p)
inst_2 : NormedSpace ℝ F
hm : m ≤ m0
hp_ne_top : p ≠ ∞
P : ↥(Lp F p μ) → Prop
h_ind :
  ∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    P (↑(simpleFunc.indicatorConst p (s := s) ⋯ ⋯ c) : ↥(Lp F p μ))
h_add :
  ∀ ⦃f g : α → F⦄ (hf : MemLp f p μ) (hg : MemLp g p μ),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ →
        Disjoint (Function.support f) (Function.support g) →
          P (MemLp.toLp f hf) → P (MemLp.toLp g hg) → P (MemLp.toLp f hf + MemLp.toLp g hg)
h_closed : IsClosed (X := ↥(lpMeas F ℝ m p μ)) {f : ↥(lpMeas F ℝ m p μ) | P (↑f : ↥(Lp F p μ))}
f : ↥(Lp F p μ)
hf : AEStronglyMeasurable (↑(↑f : α →ₘ[μ] F) : α → F) μ
f' : ↥(lpMeas F ℝ m p μ) :=
  Subtype.mk (p := fun (x : ↥(Lp F p μ)) ↦ Membership.mem (γ := Submodule ℝ ↥(Lp F p μ)) (lpMeas F ℝ m p μ) x) f hf
g : ↥(Lp F p (μ.trim hm)) := (lpMeasToLpTrimLie F ℝ p μ hm : (a : ↥(lpMeas F ℝ m p μ)) → ↥(Lp F p (μ.trim hm))) f'
hfg :
  f' = (LinearIsometryEquiv.symm (lpMeasToLpTrimLie F ℝ p μ hm) : (a : ↥(Lp F p (μ.trim hm))) → ↥(lpMeas F ℝ m p μ)) g
⊢ P (↑f' : ↥(Lp F p μ))
have rw : P
  (↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F ℝ p μ hm) : (a : ↥(Lp F p (μ.trim hm))) → ↥(lpMeas F ℝ m p μ)) g) :
    ↥(Lp F p μ))
Tactic: rw [hfg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable (goal)
Goal:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
inst_1 : Fact (1 ≤ p)
inst_2 : NormedSpace ℝ F
hm : m ≤ m0
hp_ne_top : p ≠ ∞
P : ↥(Lp F p μ) → Prop
h_ind :
  ∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    P (↑(simpleFunc.indicatorConst p (s := s) ⋯ ⋯ c) : ↥(Lp F p μ))
h_add :
  ∀ ⦃f g : α → F⦄ (hf : MemLp f p μ) (hg : MemLp g p μ),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ →
        Disjoint (Function.support f) (Function.support g) →
          P (MemLp.toLp f hf) → P (MemLp.toLp g hg) → P (MemLp.toLp f hf + MemLp.toLp g hg)
h_closed : IsClosed (X := ↥(lpMeas F ℝ m p μ)) {f : ↥(lpMeas F ℝ m p μ) | P (↑f : ↥(Lp F p μ))}
f : ↥(Lp F p μ)
hf : AEStronglyMeasurable (↑(↑f : α →ₘ[μ] F) : α → F) μ
f' : ↥(lpMeas F ℝ m p μ) :=
  Subtype.mk (p := fun (x : ↥(Lp F p μ)) ↦ Membership.mem (γ := Submodule ℝ ↥(Lp F p μ)) (lpMeas F ℝ m p μ) x) f hf
g : ↥(Lp F p (μ.trim hm)) := (lpMeasToLpTrimLie F ℝ p μ hm : (a : ↥(lpMeas F ℝ m p μ)) → ↥(Lp F p (μ.trim hm))) f'
hfg :
  f' = (LinearIsometryEquiv.symm (lpMeasToLpTrimLie F ℝ p μ hm) : (a : ↥(Lp F p (μ.trim hm))) → ↥(lpMeas F ℝ m p μ)) g
⊢ P
    (↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F ℝ p μ hm) : (a : ↥(Lp F p (μ.trim hm))) → ↥(lpMeas F ℝ m p μ))
          g) :
      ↥(Lp F p μ))
have refine_1 : ∀ (c : F) {s : Set α} (hs : MeasurableSet s)
  (hμs : LT.lt (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
  (fun (g : ↥(Lp F p (μ.trim hm))) ↦
      P
        (↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F ℝ p μ hm) : (a : ↥(Lp F p (μ.trim hm))) → ↥(lpMeas F ℝ m p μ))
              g) :
          ↥(Lp F p μ)))
    (↑(simpleFunc.indicatorConst p (s := s) hs sorry c) : ↥(Lp F p (μ.trim hm)))
Tactic: refine
    @Lp.induction α F m _ p (μ.trim hm) _ hp_ne_top
      (fun g => P ((lpMeasToLpTrimLie F ℝ p μ hm).symm g)) ?_ ?_ ?_ g
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable (goal)
Goal:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
inst_1 : Fact (1 ≤ p)
inst_2 : NormedSpace ℝ F
hm : m ≤ m0
hp_ne_top : p ≠ ∞
P : ↥(Lp F p μ) → Prop
h_ind :
  ∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    P (↑(simpleFunc.indicatorConst p (s := s) ⋯ ⋯ c) : ↥(Lp F p μ))
h_add :
  ∀ ⦃f g : α → F⦄ (hf : MemLp f p μ) (hg : MemLp g p μ),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ →
        Disjoint (Function.support f) (Function.support g) →
          P (MemLp.toLp f hf) → P (MemLp.toLp g hg) → P (MemLp.toLp f hf + MemLp.toLp g hg)
h_closed : IsClosed (X := ↥(lpMeas F ℝ m p μ)) {f : ↥(lpMeas F ℝ m p μ) | P (↑f : ↥(Lp F p μ))}
f : ↥(Lp F p μ)
hf : AEStronglyMeasurable (↑(↑f : α →ₘ[μ] F) : α → F) μ
f' : ↥(lpMeas F ℝ m p μ) :=
  Subtype.mk (p := fun (x : ↥(Lp F p μ)) ↦ Membership.mem (γ := Submodule ℝ ↥(Lp F p μ)) (lpMeas F ℝ m p μ) x) f hf
g : ↥(Lp F p (μ.trim hm)) := (lpMeasToLpTrimLie F ℝ p μ hm : (a : ↥(lpMeas F ℝ m p μ)) → ↥(Lp F p (μ.trim hm))) f'
hfg :
  f' = (LinearIsometryEquiv.symm (lpMeasToLpTrimLie F ℝ p μ hm) : (a : ↥(Lp F p (μ.trim hm))) → ↥(lpMeas F ℝ m p μ)) g
refine_1 :
  ∀ (c : F) {s : Set α} (hs : MeasurableSet s)
    (hμs : LT.lt (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    (fun (g : ↥(Lp F p (μ.trim hm))) ↦
        P
          (↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F ℝ p μ hm) :
                  (a : ↥(Lp F p (μ.trim hm))) → ↥(lpMeas F ℝ m p μ))
                g) :
            ↥(Lp F p μ)))
      (↑(simpleFunc.indicatorConst p (s := s) hs ⋯ c) : ↥(Lp F p (μ.trim hm)))
⊢ P
    (↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F ℝ p μ hm) : (a : ↥(Lp F p (μ.trim hm))) → ↥(lpMeas F ℝ m p μ))
          g) :
      ↥(Lp F p μ))
have refine_2 : ∀ ⦃f g : α → F⦄ (hf : MemLp f p (μ.trim hm)) (hg : MemLp g p (μ.trim hm)),
  Disjoint (Function.support f) (Function.support g) →
    (fun (g : ↥(Lp F p (μ.trim hm))) ↦
          P
            (↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F ℝ p μ hm) :
                    (a : ↥(Lp F p (μ.trim hm))) → ↥(lpMeas F ℝ m p μ))
                  g) :
              ↥(Lp F p μ)))
        (MemLp.toLp f hf) →
      (fun (g : ↥(Lp F p (μ.trim hm))) ↦
            P
              (↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F ℝ p μ hm) :
                      (a : ↥(Lp F p (μ.trim hm))) → ↥(lpMeas F ℝ m p μ))
                    g) :
                ↥(Lp F p μ)))
          (MemLp.toLp g hg) →
        (fun (g : ↥(Lp F p (μ.trim hm))) ↦
            P
              (↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F ℝ p μ hm) :
                      (a : ↥(Lp F p (μ.trim hm))) → ↥(lpMeas F ℝ m p μ))
                    g) :
                ↥(Lp F p μ)))
          (MemLp.toLp f hf + MemLp.toLp g hg)
Tactic: refine
    @Lp.induction α F m _ p (μ.trim hm) _ hp_ne_top
      (fun g => P ((lpMeasToLpTrimLie F ℝ p μ hm).symm g)) ?_ ?_ ?_ g
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable (goal)
Goal:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
inst_1 : Fact (1 ≤ p)
inst_2 : NormedSpace ℝ F
hm : m ≤ m0
hp_ne_top : p ≠ ∞
P : ↥(Lp F p μ) → Prop
h_ind :
  ∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    P (↑(simpleFunc.indicatorConst p (s := s) ⋯ ⋯ c) : ↥(Lp F p μ))
h_add :
  ∀ ⦃f g : α → F⦄ (hf : MemLp f p μ) (hg : MemLp g p μ),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ →
        Disjoint (Function.support f) (Function.support g) →
          P (MemLp.toLp f hf) → P (MemLp.toLp g hg) → P (MemLp.toLp f hf + MemLp.toLp g hg)
h_closed : IsClosed (X := ↥(lpMeas F ℝ m p μ)) {f : ↥(lpMeas F ℝ m p μ) | P (↑f : ↥(Lp F p μ))}
f : ↥(Lp F p μ)
hf : AEStronglyMeasurable (↑(↑f : α →ₘ[μ] F) : α → F) μ
f' : ↥(lpMeas F ℝ m p μ) :=
  Subtype.mk (p := fun (x : ↥(Lp F p μ)) ↦ Membership.mem (γ := Submodule ℝ ↥(Lp F p μ)) (lpMeas F ℝ m p μ) x) f hf
g : ↥(Lp F p (μ.trim hm)) := (lpMeasToLpTrimLie F ℝ p μ hm : (a : ↥(lpMeas F ℝ m p μ)) → ↥(Lp F p (μ.trim hm))) f'
hfg :
  f' = (LinearIsometryEquiv.symm (lpMeasToLpTrimLie F ℝ p μ hm) : (a : ↥(Lp F p (μ.trim hm))) → ↥(lpMeas F ℝ m p μ)) g
b : F
t : Set α
ht : MeasurableSet t
hμt : LT.lt (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ P
    (↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F ℝ p μ hm) : (a : ↥(Lp F p (μ.trim hm))) → ↥(lpMeas F ℝ m p μ))
          (↑(simpleFunc.indicatorConst p (s := t) ht ⋯ b) : ↥(Lp F p (μ.trim hm)))) :
      ↥(Lp F p μ))
have refine_1 : P (indicatorConstLp (s := t) p sorry sorry b)
Tactic: rw [@Lp.simpleFunc.coe_indicatorConst _ _ m, lpMeasToLpTrimLie_symm_indicator ht hμt.ne b]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable (goal)
Goal:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
inst_1 : Fact (1 ≤ p)
inst_2 : NormedSpace ℝ F
hm : m ≤ m0
hp_ne_top : p ≠ ∞
P : ↥(Lp F p μ) → Prop
h_ind :
  ∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    P (↑(simpleFunc.indicatorConst p (s := s) ⋯ ⋯ c) : ↥(Lp F p μ))
h_add :
  ∀ ⦃f g : α → F⦄ (hf : MemLp f p μ) (hg : MemLp g p μ),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ →
        Disjoint (Function.support f) (Function.support g) →
          P (MemLp.toLp f hf) → P (MemLp.toLp g hg) → P (MemLp.toLp f hf + MemLp.toLp g hg)
h_closed : IsClosed (X := ↥(lpMeas F ℝ m p μ)) {f : ↥(lpMeas F ℝ m p μ) | P (↑f : ↥(Lp F p μ))}
f : ↥(Lp F p μ)
hf : AEStronglyMeasurable (↑(↑f : α →ₘ[μ] F) : α → F) μ
f' : ↥(lpMeas F ℝ m p μ) :=
  Subtype.mk (p := fun (x : ↥(Lp F p μ)) ↦ Membership.mem (γ := Submodule ℝ ↥(Lp F p μ)) (lpMeas F ℝ m p μ) x) f hf
g : ↥(Lp F p (μ.trim hm)) := (lpMeasToLpTrimLie F ℝ p μ hm : (a : ↥(lpMeas F ℝ m p μ)) → ↥(Lp F p (μ.trim hm))) f'
hfg :
  f' = (LinearIsometryEquiv.symm (lpMeasToLpTrimLie F ℝ p μ hm) : (a : ↥(Lp F p (μ.trim hm))) → ↥(lpMeas F ℝ m p μ)) g
b : F
t : Set α
ht : MeasurableSet t
hμt : LT.lt (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ P (indicatorConstLp (s := t) p ⋯ ⋯ b)
have refine_1 : ∀ (hμt' : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)), P (indicatorConstLp (s := t) p sorry sorry b)
Tactic: have hμt' : μ t < ∞ := (le_trim hm).trans_lt hμt
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable (hypothesis)
Goal:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
inst_1 : Fact (1 ≤ p)
inst_2 : NormedSpace ℝ F
hm : m ≤ m0
hp_ne_top : p ≠ ∞
P : ↥(Lp F p μ) → Prop
h_ind :
  ∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    P (↑(simpleFunc.indicatorConst p (s := s) ⋯ ⋯ c) : ↥(Lp F p μ))
h_add :
  ∀ ⦃f g : α → F⦄ (hf : MemLp f p μ) (hg : MemLp g p μ),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ →
        Disjoint (Function.support f) (Function.support g) →
          P (MemLp.toLp f hf) → P (MemLp.toLp g hg) → P (MemLp.toLp f hf + MemLp.toLp g hg)
h_closed : IsClosed (X := ↥(lpMeas F ℝ m p μ)) {f : ↥(lpMeas F ℝ m p μ) | P (↑f : ↥(Lp F p μ))}
f : ↥(Lp F p μ)
hf : AEStronglyMeasurable (↑(↑f : α →ₘ[μ] F) : α → F) μ
f' : ↥(lpMeas F ℝ m p μ) :=
  Subtype.mk (p := fun (x : ↥(Lp F p μ)) ↦ Membership.mem (γ := Submodule ℝ ↥(Lp F p μ)) (lpMeas F ℝ m p μ) x) f hf
g : ↥(Lp F p (μ.trim hm)) := (lpMeasToLpTrimLie F ℝ p μ hm : (a : ↥(lpMeas F ℝ m p μ)) → ↥(Lp F p (μ.trim hm))) f'
hfg :
  f' = (LinearIsometryEquiv.symm (lpMeasToLpTrimLie F ℝ p μ hm) : (a : ↥(Lp F p (μ.trim hm))) → ↥(lpMeas F ℝ m p μ)) g
b : F
t : Set α
ht : MeasurableSet t
hμt : LT.lt (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hμt' : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ P (indicatorConstLp (s := t) p ⋯ ⋯ b)
have h_ind₁ : P (↑(simpleFunc.indicatorConst p (s := t) sorry sorry b) : ↥(Lp F p μ))
Tactic: specialize h_ind b ht hμt'
Cleared hypotheses: h_ind
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable (goal)
Goal:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
inst_1 : Fact (1 ≤ p)
inst_2 : NormedSpace ℝ F
hm : m ≤ m0
hp_ne_top : p ≠ ∞
P : ↥(Lp F p μ) → Prop
h_add :
  ∀ ⦃f g : α → F⦄ (hf : MemLp f p μ) (hg : MemLp g p μ),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ →
        Disjoint (Function.support f) (Function.support g) →
          P (MemLp.toLp f hf) → P (MemLp.toLp g hg) → P (MemLp.toLp f hf + MemLp.toLp g hg)
h_closed : IsClosed (X := ↥(lpMeas F ℝ m p μ)) {f : ↥(lpMeas F ℝ m p μ) | P (↑f : ↥(Lp F p μ))}
f : ↥(Lp F p μ)
hf : AEStronglyMeasurable (↑(↑f : α →ₘ[μ] F) : α → F) μ
f' : ↥(lpMeas F ℝ m p μ) :=
  Subtype.mk (p := fun (x : ↥(Lp F p μ)) ↦ Membership.mem (γ := Submodule ℝ ↥(Lp F p μ)) (lpMeas F ℝ m p μ) x) f hf
g : ↥(Lp F p (μ.trim hm)) := (lpMeasToLpTrimLie F ℝ p μ hm : (a : ↥(lpMeas F ℝ m p μ)) → ↥(Lp F p (μ.trim hm))) f'
hfg :
  f' = (LinearIsometryEquiv.symm (lpMeasToLpTrimLie F ℝ p μ hm) : (a : ↥(Lp F p (μ.trim hm))) → ↥(lpMeas F ℝ m p μ)) g
b : F
t : Set α
ht : MeasurableSet t
hμt : LT.lt (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hμt' : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
h_ind : P (↑(simpleFunc.indicatorConst p (s := t) ⋯ ⋯ b) : ↥(Lp F p μ))
⊢ P (indicatorConstLp (s := t) p ⋯ ⋯ b)
have refine_1 : ∀ (h_ind : P (indicatorConstLp (s := t) p sorry sorry b)), P (indicatorConstLp (s := t) p sorry sorry b)
Tactic: rwa [Lp.simpleFunc.coe_indicatorConst] at h_ind
Cleared hypotheses: h_ind