awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator (hypothesis)
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hs : MeasurableSet s
hf : f =ᶠ[ae (μ.restrict sᶜ)] 0
hm : m ≤ m0
⊢ μ[s.indicator f | m] =ᶠ[ae μ] s.indicator μ[f | m]
have hsf_zero : ∀ (g : α → E), g =ᶠ[ae (μ.restrict sᶜ)] 0 → s.indicator g =ᶠ[ae μ] g
Tactic: have hsf_zero : ∀ g : α → E, g =ᵐ[μ.restrict sᶜ] 0 → s.indicator g =ᵐ[μ] g := fun g =>
    indicator_ae_eq_of_restrict_compl_ae_eq_zero (hm _ hs)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hs : MeasurableSet s
hf : f =ᶠ[ae (μ.restrict sᶜ)] 0
hm : m ≤ m0
hsf_zero : ∀ (g : α → E), g =ᶠ[ae (μ.restrict sᶜ)] 0 → s.indicator g =ᶠ[ae μ] g
⊢ μ[s.indicator f | m] =ᶠ[ae μ] s.indicator μ[f | m]
have pos : μ[f | m] =ᶠ[ae μ] μ[s.indicator f | m]
Tactic: refine ((hsf_zero (μ[f | m]) (condExp_ae_eq_restrict_zero hs.compl hf)).trans ?_).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f μ
hs : MeasurableSet s
⊢ μ[s.indicator f | m] =ᶠ[ae μ] s.indicator μ[f | m]
have pos : ∀ (hm : m ≤ m0), μ[s.indicator f | m] =ᶠ[ae μ] s.indicator μ[f | m]
Tactic: by_cases hm : m ≤ m0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f μ
hs : MeasurableSet s
pos : ∀ (hm : m ≤ m0), μ[s.indicator f | m] =ᶠ[ae μ] s.indicator μ[f | m]
⊢ μ[s.indicator f | m] =ᶠ[ae μ] s.indicator μ[f | m]
have neg : ∀ (hm : ¬m ≤ m0), μ[s.indicator f | m] =ᶠ[ae μ] s.indicator μ[f | m]
Tactic: by_cases hm : m ≤ m0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f μ
hs : MeasurableSet s
hm : ¬m ≤ m0
⊢ μ[s.indicator f | m] =ᶠ[ae μ] s.indicator μ[f | m]
have neg : EventuallyEq.{u_1, u_2} (β := E) (ae μ) 0 0
Tactic: simp_rw [condExp_of_not_le hm, Set.indicator_zero']
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f μ
hs : MeasurableSet s
hm : m ≤ m0
⊢ μ[s.indicator f | m] =ᶠ[ae μ] s.indicator μ[f | m]
have pos : ∀ (hμm : SigmaFinite (μ.trim hm)), μ[s.indicator f | m] =ᶠ[ae μ] s.indicator μ[f | m]
Tactic: by_cases hμm : SigmaFinite (μ.trim hm)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f μ
hs : MeasurableSet s
hm : m ≤ m0
pos : ∀ (hμm : SigmaFinite (μ.trim hm)), μ[s.indicator f | m] =ᶠ[ae μ] s.indicator μ[f | m]
⊢ μ[s.indicator f | m] =ᶠ[ae μ] s.indicator μ[f | m]
have neg : ∀ (hμm : ¬SigmaFinite (μ.trim hm)), μ[s.indicator f | m] =ᶠ[ae μ] s.indicator μ[f | m]
Tactic: by_cases hμm : SigmaFinite (μ.trim hm)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f μ
hs : MeasurableSet s
hm : m ≤ m0
hμm : ¬SigmaFinite (μ.trim hm)
⊢ μ[s.indicator f | m] =ᶠ[ae μ] s.indicator μ[f | m]
have neg : EventuallyEq.{u_1, u_2} (β := E) (ae μ) 0 0
Tactic: simp_rw [condExp_of_not_sigmaFinite hm hμm, Set.indicator_zero']
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f μ
hs : MeasurableSet s
hm : m ≤ m0
hμm this : SigmaFinite (μ.trim hm)
⊢ s.indicator μ[f | m] =ᶠ[ae μ] s.indicator μ[s.indicator f + sᶜ.indicator f | m]
have rw : s.indicator μ[f | m] =ᶠ[ae μ] s.indicator μ[f | m]
Tactic: rw [Set.indicator_self_add_compl s f]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator (hypothesis)
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f μ
hs : MeasurableSet s
hm : m ≤ m0
hμm this : SigmaFinite (μ.trim hm)
⊢ μ[s.indicator f | m] =ᶠ[ae μ] s.indicator μ[f | m]
have this₁ : s.indicator μ[f | m] =ᶠ[ae μ] s.indicator μ[s.indicator f + sᶜ.indicator f | m]
Tactic: have : s.indicator (μ[f | m]) =ᵐ[μ] s.indicator (μ[s.indicator f + sᶜ.indicator f | m]) := by
    rw [Set.indicator_self_add_compl s f]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f μ
hs : MeasurableSet s
hm : m ≤ m0
hμm this_1 : SigmaFinite (μ.trim hm)
this : s.indicator μ[f | m] =ᶠ[ae μ] s.indicator μ[s.indicator f + sᶜ.indicator f | m]
⊢ μ[s.indicator f | m] =ᶠ[ae μ] s.indicator μ[f | m]
have pos : s.indicator μ[s.indicator f + sᶜ.indicator f | m] =ᶠ[ae μ] μ[s.indicator f | m]
Tactic: refine (this.trans ?_).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f μ
hs : MeasurableSet s
hm : m ≤ m0
hμm this_1 : SigmaFinite (μ.trim hm)
this : s.indicator μ[f | m] =ᶠ[ae μ] s.indicator μ[s.indicator f + sᶜ.indicator f | m]
⊢ s.indicator μ[s.indicator f + sᶜ.indicator f | m] =ᶠ[ae μ] s.indicator (μ[s.indicator f | m] + μ[sᶜ.indicator f | m])
have h : ∀ (x : α) (hx : μ[s.indicator f + sᶜ.indicator f | m] x = (μ[s.indicator f | m] + μ[sᶜ.indicator f | m]) x),
  s.indicator μ[s.indicator f + sᶜ.indicator f | m] x = s.indicator (μ[s.indicator f | m] + μ[sᶜ.indicator f | m]) x
Tactic: filter_upwards [condExp_add (hf_int.indicator (hm _ hs)) (hf_int.indicator (hm _ hs.compl)) m]
        with x hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f μ
hs : MeasurableSet s
hm : m ≤ m0
hμm this_1 : SigmaFinite (μ.trim hm)
this : s.indicator μ[f | m] =ᶠ[ae μ] s.indicator μ[s.indicator f + sᶜ.indicator f | m]
x : α
hx : μ[s.indicator f + sᶜ.indicator f | m] x = (μ[s.indicator f | m] + μ[sᶜ.indicator f | m]) x
⊢ s.indicator μ[s.indicator f + sᶜ.indicator f | m] x = s.indicator (μ[s.indicator f | m] + μ[sᶜ.indicator f | m]) x
have h : (if x ∈ s then μ[s.indicator f + sᶜ.indicator f | m] x else 0) =
  s.indicator (μ[s.indicator f | m] + μ[sᶜ.indicator f | m]) x
Tactic: rw [Set.indicator_apply, Set.indicator_apply, hx]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f μ
hs : MeasurableSet s
hm : m ≤ m0
hμm this_1 : SigmaFinite (μ.trim hm)
this : s.indicator μ[f | m] =ᶠ[ae μ] s.indicator μ[s.indicator f + sᶜ.indicator f | m]
x : α
hx : μ[s.indicator f + sᶜ.indicator f | m] x = (μ[s.indicator f | m] + μ[sᶜ.indicator f | m]) x
h :
  (if x ∈ s then μ[s.indicator f + sᶜ.indicator f | m] x else 0) =
    s.indicator (μ[s.indicator f | m] + μ[sᶜ.indicator f | m]) x
⊢ s.indicator μ[s.indicator f + sᶜ.indicator f | m] x = s.indicator (μ[s.indicator f | m] + μ[sᶜ.indicator f | m]) x
have h₁ : (if x ∈ s then μ[s.indicator f + sᶜ.indicator f | m] x else 0) =
  if x ∈ s then (μ[s.indicator f | m] + μ[sᶜ.indicator f | m]) x else 0
Tactic: rw [Set.indicator_apply, Set.indicator_apply, hx]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f μ
hs : MeasurableSet s
hm : m ≤ m0
hμm this_1 : SigmaFinite (μ.trim hm)
this : s.indicator μ[f | m] =ᶠ[ae μ] s.indicator μ[s.indicator f + sᶜ.indicator f | m]
x : α
hx : μ[s.indicator f + sᶜ.indicator f | m] x = (μ[s.indicator f | m] + μ[sᶜ.indicator f | m]) x
h :
  (if x ∈ s then μ[s.indicator f + sᶜ.indicator f | m] x else 0) =
    s.indicator (μ[s.indicator f | m] + μ[sᶜ.indicator f | m]) x
h₁ :
  (if x ∈ s then μ[s.indicator f + sᶜ.indicator f | m] x else 0) =
    if x ∈ s then (μ[s.indicator f | m] + μ[sᶜ.indicator f | m]) x else 0
⊢ s.indicator μ[s.indicator f + sᶜ.indicator f | m] x = s.indicator (μ[s.indicator f | m] + μ[sᶜ.indicator f | m]) x
have h₂ : (if x ∈ s then (μ[s.indicator f | m] + μ[sᶜ.indicator f | m]) x else 0) =
  if x ∈ s then (μ[s.indicator f | m] + μ[sᶜ.indicator f | m]) x else 0
Tactic: rw [Set.indicator_apply, Set.indicator_apply, hx]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f μ
hs : MeasurableSet s
hm : m ≤ m0
hμm this_1 : SigmaFinite (μ.trim hm)
this : s.indicator μ[f | m] =ᶠ[ae μ] s.indicator μ[s.indicator f + sᶜ.indicator f | m]
x : α
hx : μ[s.indicator f + sᶜ.indicator f | m] x = (μ[s.indicator f | m] + μ[sᶜ.indicator f | m]) x
⊢ s.indicator μ[s.indicator f + sᶜ.indicator f | m] x = s.indicator (μ[s.indicator f | m] + μ[sᶜ.indicator f | m]) x
have h : (if x ∈ s then μ[s.indicator f + sᶜ.indicator f | m] x else 0) =
  s.indicator (μ[s.indicator f | m] + μ[sᶜ.indicator f | m]) x
Tactic: classical rw [Set.indicator_apply, Set.indicator_apply, hx]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f μ
hs : MeasurableSet s
hm : m ≤ m0
hμm this_1 : SigmaFinite (μ.trim hm)
this : s.indicator μ[f | m] =ᶠ[ae μ] s.indicator μ[s.indicator f + sᶜ.indicator f | m]
x : α
hx : μ[s.indicator f + sᶜ.indicator f | m] x = (μ[s.indicator f | m] + μ[sᶜ.indicator f | m]) x
h :
  (if x ∈ s then μ[s.indicator f + sᶜ.indicator f | m] x else 0) =
    s.indicator (μ[s.indicator f | m] + μ[sᶜ.indicator f | m]) x
⊢ s.indicator μ[s.indicator f + sᶜ.indicator f | m] x = s.indicator (μ[s.indicator f | m] + μ[sᶜ.indicator f | m]) x
have h₁ : (if x ∈ s then μ[s.indicator f + sᶜ.indicator f | m] x else 0) =
  if x ∈ s then (μ[s.indicator f | m] + μ[sᶜ.indicator f | m]) x else 0
Tactic: classical rw [Set.indicator_apply, Set.indicator_apply, hx]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f μ
hs : MeasurableSet s
hm : m ≤ m0
hμm this_1 : SigmaFinite (μ.trim hm)
this : s.indicator μ[f | m] =ᶠ[ae μ] s.indicator μ[s.indicator f + sᶜ.indicator f | m]
x : α
hx : μ[s.indicator f + sᶜ.indicator f | m] x = (μ[s.indicator f | m] + μ[sᶜ.indicator f | m]) x
h :
  (if x ∈ s then μ[s.indicator f + sᶜ.indicator f | m] x else 0) =
    s.indicator (μ[s.indicator f | m] + μ[sᶜ.indicator f | m]) x
h₁ :
  (if x ∈ s then μ[s.indicator f + sᶜ.indicator f | m] x else 0) =
    if x ∈ s then (μ[s.indicator f | m] + μ[sᶜ.indicator f | m]) x else 0
⊢ s.indicator μ[s.indicator f + sᶜ.indicator f | m] x = s.indicator (μ[s.indicator f | m] + μ[sᶜ.indicator f | m]) x
have h₂ : (if x ∈ s then (μ[s.indicator f | m] + μ[sᶜ.indicator f | m]) x else 0) =
  if x ∈ s then (μ[s.indicator f | m] + μ[sᶜ.indicator f | m]) x else 0
Tactic: classical rw [Set.indicator_apply, Set.indicator_apply, hx]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f μ
hs : MeasurableSet s
hm : m ≤ m0
hμm this_1 : SigmaFinite (μ.trim hm)
this : s.indicator μ[f | m] =ᶠ[ae μ] s.indicator μ[s.indicator f + sᶜ.indicator f | m]
⊢ s.indicator μ[s.indicator f | m] + s.indicator μ[sᶜ.indicator f | m] =ᶠ[ae μ]
    s.indicator μ[s.indicator f | m] + s.indicator (sᶜ.indicator μ[sᶜ.indicator f | m])
have refine : s.indicator μ[sᶜ.indicator f | m] =ᶠ[ae μ] s.indicator (sᶜ.indicator μ[sᶜ.indicator f | m])
Tactic: refine Filter.EventuallyEq.rfl.add ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f μ
hs : MeasurableSet s
hm : m ≤ m0
hμm this_1 : SigmaFinite (μ.trim hm)
this : s.indicator μ[f | m] =ᶠ[ae μ] s.indicator μ[s.indicator f + sᶜ.indicator f | m]
⊢ sᶜ.indicator μ[sᶜ.indicator f | m] =ᶠ[ae μ] μ[sᶜ.indicator f | m]
have refine_1 : sᶜ.indicator f =ᶠ[ae (μ.restrict sᶜᶜ)] 0
Tactic: refine (condExp_indicator_aux hs.compl ?_).symm.trans ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f μ
hs : MeasurableSet s
hm : m ≤ m0
hμm this_1 : SigmaFinite (μ.trim hm)
this : s.indicator μ[f | m] =ᶠ[ae μ] s.indicator μ[s.indicator f + sᶜ.indicator f | m]
refine_1 : sᶜ.indicator f =ᶠ[ae (μ.restrict sᶜᶜ)] 0
⊢ sᶜ.indicator μ[sᶜ.indicator f | m] =ᶠ[ae μ] μ[sᶜ.indicator f | m]
have refine_2 : μ[sᶜ.indicator (sᶜ.indicator f) | m] =ᶠ[ae μ] μ[sᶜ.indicator f | m]
Tactic: refine (condExp_indicator_aux hs.compl ?_).symm.trans ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f μ
hs : MeasurableSet s
hm : m ≤ m0
hμm this_1 : SigmaFinite (μ.trim hm)
this : s.indicator μ[f | m] =ᶠ[ae μ] s.indicator μ[s.indicator f + sᶜ.indicator f | m]
⊢ μ[sᶜ.indicator (sᶜ.indicator f) | m] =ᶠ[ae μ] μ[sᶜ.indicator f | m]
have refine_2 : μ[(sᶜ ∩ sᶜ).indicator f | m] =ᶠ[ae μ] μ[sᶜ.indicator f | m]
Tactic: rw [Set.indicator_indicator, Set.inter_self]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f μ
hs : MeasurableSet s
hm : m ≤ m0
hμm this_1 : SigmaFinite (μ.trim hm)
this : s.indicator μ[f | m] =ᶠ[ae μ] s.indicator μ[s.indicator f + sᶜ.indicator f | m]
refine_2 : μ[(sᶜ ∩ sᶜ).indicator f | m] =ᶠ[ae μ] μ[sᶜ.indicator f | m]
⊢ μ[sᶜ.indicator (sᶜ.indicator f) | m] =ᶠ[ae μ] μ[sᶜ.indicator f | m]
have refine_2₁ : μ[sᶜ.indicator f | m] =ᶠ[ae μ] μ[sᶜ.indicator f | m]
Tactic: rw [Set.indicator_indicator, Set.inter_self]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator (hypothesis)
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f μ
hs : MeasurableSet s
hm : m ≤ m0
hμm this_1 : SigmaFinite (μ.trim hm)
this : s.indicator μ[f | m] =ᶠ[ae μ] s.indicator μ[s.indicator f + sᶜ.indicator f | m]
⊢ s.indicator μ[sᶜ.indicator f | m] =ᶠ[ae μ] s.indicator (sᶜ.indicator μ[sᶜ.indicator f | m])
have this₁ : sᶜ.indicator μ[sᶜ.indicator f | m] =ᶠ[ae μ] μ[sᶜ.indicator f | m]
Tactic: have : sᶜ.indicator (μ[sᶜ.indicator f | m]) =ᵐ[μ] μ[sᶜ.indicator f | m] := by
        refine (condExp_indicator_aux hs.compl ?_).symm.trans ?_
        · exact indicator_ae_eq_restrict_compl (hm _ hs.compl)
        · rw [Set.indicator_indicator, Set.inter_self]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f μ
hs : MeasurableSet s
hm : m ≤ m0
hμm this_1 : SigmaFinite (μ.trim hm)
this_2 : s.indicator μ[f | m] =ᶠ[ae μ] s.indicator μ[s.indicator f + sᶜ.indicator f | m]
this : sᶜ.indicator μ[sᶜ.indicator f | m] =ᶠ[ae μ] μ[sᶜ.indicator f | m]
⊢ s.indicator μ[sᶜ.indicator f | m] =ᶠ[ae μ] s.indicator (sᶜ.indicator μ[sᶜ.indicator f | m])
have h : ∀ (x : α) (hx : sᶜ.indicator μ[sᶜ.indicator f | m] x = μ[sᶜ.indicator f | m] x),
  s.indicator μ[sᶜ.indicator f | m] x = s.indicator (sᶜ.indicator μ[sᶜ.indicator f | m]) x
Tactic: filter_upwards [this] with x hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f μ
hs : MeasurableSet s
hm : m ≤ m0
hμm this_1 : SigmaFinite (μ.trim hm)
this_2 : s.indicator μ[f | m] =ᶠ[ae μ] s.indicator μ[s.indicator f + sᶜ.indicator f | m]
this : sᶜ.indicator μ[sᶜ.indicator f | m] =ᶠ[ae μ] μ[sᶜ.indicator f | m]
x : α
hx : sᶜ.indicator μ[sᶜ.indicator f | m] x = μ[sᶜ.indicator f | m] x
⊢ s.indicator μ[sᶜ.indicator f | m] x = s.indicator (sᶜ.indicator μ[sᶜ.indicator f | m]) x
have pos : ∀ (hxs : x ∈ s), s.indicator μ[sᶜ.indicator f | m] x = s.indicator (sᶜ.indicator μ[sᶜ.indicator f | m]) x
Tactic: by_cases hxs : x ∈ s
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f μ
hs : MeasurableSet s
hm : m ≤ m0
hμm this_1 : SigmaFinite (μ.trim hm)
this_2 : s.indicator μ[f | m] =ᶠ[ae μ] s.indicator μ[s.indicator f + sᶜ.indicator f | m]
this : sᶜ.indicator μ[sᶜ.indicator f | m] =ᶠ[ae μ] μ[sᶜ.indicator f | m]
x : α
hx : sᶜ.indicator μ[sᶜ.indicator f | m] x = μ[sᶜ.indicator f | m] x
pos : ∀ (hxs : x ∈ s), s.indicator μ[sᶜ.indicator f | m] x = s.indicator (sᶜ.indicator μ[sᶜ.indicator f | m]) x
⊢ s.indicator μ[sᶜ.indicator f | m] x = s.indicator (sᶜ.indicator μ[sᶜ.indicator f | m]) x
have neg : ∀ (hxs : x ∉ s), s.indicator μ[sᶜ.indicator f | m] x = s.indicator (sᶜ.indicator μ[sᶜ.indicator f | m]) x
Tactic: by_cases hxs : x ∈ s
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f μ
hs : MeasurableSet s
hm : m ≤ m0
hμm this_1 : SigmaFinite (μ.trim hm)
this : s.indicator μ[f | m] =ᶠ[ae μ] s.indicator μ[s.indicator f + sᶜ.indicator f | m]
⊢ s.indicator μ[s.indicator f | m] + s.indicator (sᶜ.indicator μ[sᶜ.indicator f | m]) =ᶠ[ae μ]
    s.indicator μ[s.indicator f | m]
have rw : s.indicator μ[s.indicator f | m] + (s ∩ sᶜ).indicator μ[sᶜ.indicator f | m] =ᶠ[ae μ] s.indicator μ[s.indicator f | m]
Tactic: rw [Set.indicator_indicator, Set.inter_compl_self, Set.indicator_empty', add_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f μ
hs : MeasurableSet s
hm : m ≤ m0
hμm this_1 : SigmaFinite (μ.trim hm)
this : s.indicator μ[f | m] =ᶠ[ae μ] s.indicator μ[s.indicator f + sᶜ.indicator f | m]
rw :
  s.indicator μ[s.indicator f | m] + (s ∩ sᶜ).indicator μ[sᶜ.indicator f | m] =ᶠ[ae μ] s.indicator μ[s.indicator f | m]
⊢ s.indicator μ[s.indicator f | m] + s.indicator (sᶜ.indicator μ[sᶜ.indicator f | m]) =ᶠ[ae μ]
    s.indicator μ[s.indicator f | m]
have rw₁ : s.indicator μ[s.indicator f | m] + Set.indicator ∅ μ[sᶜ.indicator f | m] =ᶠ[ae μ] s.indicator μ[s.indicator f | m]
Tactic: rw [Set.indicator_indicator, Set.inter_compl_self, Set.indicator_empty', add_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f μ
hs : MeasurableSet s
hm : m ≤ m0
hμm this_1 : SigmaFinite (μ.trim hm)
this : s.indicator μ[f | m] =ᶠ[ae μ] s.indicator μ[s.indicator f + sᶜ.indicator f | m]
rw :
  s.indicator μ[s.indicator f | m] + (s ∩ sᶜ).indicator μ[sᶜ.indicator f | m] =ᶠ[ae μ] s.indicator μ[s.indicator f | m]
rw₁ : s.indicator μ[s.indicator f | m] + Set.indicator ∅ μ[sᶜ.indicator f | m] =ᶠ[ae μ] s.indicator μ[s.indicator f | m]
⊢ s.indicator μ[s.indicator f | m] + s.indicator (sᶜ.indicator μ[sᶜ.indicator f | m]) =ᶠ[ae μ]
    s.indicator μ[s.indicator f | m]
have rw₂ : s.indicator μ[s.indicator f | m] + 0 =ᶠ[ae μ] s.indicator μ[s.indicator f | m]
Tactic: rw [Set.indicator_indicator, Set.inter_compl_self, Set.indicator_empty', add_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f μ
hs : MeasurableSet s
hm : m ≤ m0
hμm this_1 : SigmaFinite (μ.trim hm)
this : s.indicator μ[f | m] =ᶠ[ae μ] s.indicator μ[s.indicator f + sᶜ.indicator f | m]
rw :
  s.indicator μ[s.indicator f | m] + (s ∩ sᶜ).indicator μ[sᶜ.indicator f | m] =ᶠ[ae μ] s.indicator μ[s.indicator f | m]
rw₁ : s.indicator μ[s.indicator f | m] + Set.indicator ∅ μ[sᶜ.indicator f | m] =ᶠ[ae μ] s.indicator μ[s.indicator f | m]
rw₂ : s.indicator μ[s.indicator f | m] + 0 =ᶠ[ae μ] s.indicator μ[s.indicator f | m]
⊢ s.indicator μ[s.indicator f | m] + s.indicator (sᶜ.indicator μ[sᶜ.indicator f | m]) =ᶠ[ae μ]
    s.indicator μ[s.indicator f | m]
have rw₃ : s.indicator μ[s.indicator f | m] =ᶠ[ae μ] s.indicator μ[s.indicator f | m]
Tactic: rw [Set.indicator_indicator, Set.inter_compl_self, Set.indicator_empty', add_zero]