mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1

Goal state before:
pp: case refine_2
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝¹ : SigmaFinite (μ.trim hm)
inst✝ : CompleteSpace F'
f✝ : ↥(Lp F' 1 μ)
f g : α → F'
hf : MemLp f 1 μ
hg : MemLp g 1 μ
⊢ Disjoint (Function.support f) (Function.support g) →
    AEStronglyMeasurable (↑↑((condExpL1CLM F' hm μ) (MemLp.toLp f hf))) μ →
      AEStronglyMeasurable (↑↑((condExpL1CLM F' hm μ) (MemLp.toLp g hg))) μ →
        AEStronglyMeasurable (↑↑((condExpL1CLM F' hm μ) (MemLp.toLp f hf + MemLp.toLp g hg))) μ

Tactic:
_

Goal state after:
case refine_2
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝¹ : SigmaFinite (μ.trim hm)
inst✝ : CompleteSpace F'
f✝ : ↥(Lp F' 1 μ)
f g : α → F'
hf : MemLp f 1 μ
hg : MemLp g 1 μ
a✝ : Disjoint (Function.support f) (Function.support g)
⊢ AEStronglyMeasurable (↑↑((condExpL1CLM F' hm μ) (MemLp.toLp f hf))) μ →
    AEStronglyMeasurable (↑↑((condExpL1CLM F' hm μ) (MemLp.toLp g hg))) μ →
      AEStronglyMeasurable (↑↑((condExpL1CLM F' hm μ) (MemLp.toLp f hf + MemLp.toLp g hg))) μ
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic

Goal state before:
pp: case neg
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hf : Integrable f μ
hg : Integrable g μ
m : MeasurableSpace α
hm : m ≤ m₀
hμm : ¬SigmaFinite (μ.trim hm)
⊢ μ[f + g | m] =ᵐ[μ] μ[f | m] + μ[g | m]

pp: case pos
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hf : Integrable f μ
hg : Integrable g μ
m : MeasurableSpace α
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
⊢ μ[f + g | m] =ᵐ[μ] μ[f | m] + μ[g | m]

Tactic:
· simp_rw [condExp_of_not_sigmaFinite hm hμm]; simp

Goal state after:
case pos
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hf : Integrable f μ
hg : Integrable g μ
m : MeasurableSpace α
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
⊢ μ[f + g | m] =ᵐ[μ] μ[f | m] + μ[g | m]
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1

Goal state before:
pp: case refine_2
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝¹ : SigmaFinite (μ.trim hm)
inst✝ : CompleteSpace F'
f✝ : ↥(lpMeas F' ℝ m 1 μ)
g✝ : ↥(Lp F' 1 (μ.trim hm)) := (lpMeasToLpTrimLie F' ℝ 1 μ hm) f✝
hfg : f✝ = (lpMeasToLpTrimLie F' ℝ 1 μ hm).symm g✝
f g : α → F'
hf : MemLp f 1 (μ.trim hm)
hg : MemLp g 1 (μ.trim hm)
⊢ Disjoint (Function.support f) (Function.support g) →
    (condExpL1CLM F' hm μ) ↑((lpMeasToLpTrimLie F' ℝ 1 μ hm).symm (MemLp.toLp f hf)) =
        ↑((lpMeasToLpTrimLie F' ℝ 1 μ hm).symm (MemLp.toLp f hf)) →
      (condExpL1CLM F' hm μ) ↑((lpMeasToLpTrimLie F' ℝ 1 μ hm).symm (MemLp.toLp g hg)) =
          ↑((lpMeasToLpTrimLie F' ℝ 1 μ hm).symm (MemLp.toLp g hg)) →
        (condExpL1CLM F' hm μ) ↑((lpMeasToLpTrimLie F' ℝ 1 μ hm).symm (MemLp.toLp f hf + MemLp.toLp g hg)) =
          ↑((lpMeasToLpTrimLie F' ℝ 1 μ hm).symm (MemLp.toLp f hf + MemLp.toLp g hg))

Tactic:
_

Goal state after:
case refine_2
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝¹ : SigmaFinite (μ.trim hm)
inst✝ : CompleteSpace F'
f✝ : ↥(lpMeas F' ℝ m 1 μ)
g✝ : ↥(Lp F' 1 (μ.trim hm)) := (lpMeasToLpTrimLie F' ℝ 1 μ hm) f✝
hfg : f✝ = (lpMeasToLpTrimLie F' ℝ 1 μ hm).symm g✝
f g : α → F'
hf : MemLp f 1 (μ.trim hm)
hg : MemLp g 1 (μ.trim hm)
a✝ : Disjoint (Function.support f) (Function.support g)
⊢ (condExpL1CLM F' hm μ) ↑((lpMeasToLpTrimLie F' ℝ 1 μ hm).symm (MemLp.toLp f hf)) =
      ↑((lpMeasToLpTrimLie F' ℝ 1 μ hm).symm (MemLp.toLp f hf)) →
    (condExpL1CLM F' hm μ) ↑((lpMeasToLpTrimLie F' ℝ 1 μ hm).symm (MemLp.toLp g hg)) =
        ↑((lpMeasToLpTrimLie F' ℝ 1 μ hm).symm (MemLp.toLp g hg)) →
      (condExpL1CLM F' hm μ) ↑((lpMeasToLpTrimLie F' ℝ 1 μ hm).symm (MemLp.toLp f hf + MemLp.toLp g hg)) =
        ↑((lpMeasToLpTrimLie F' ℝ 1 μ hm).symm (MemLp.toLp f hf + MemLp.toLp g hg))
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic

Goal state before:
pp: case neg
α : Type u_1
E : Type u_3
𝕜 : Type u_4
inst✝⁴ : RCLike 𝕜
m₀ : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
f : α → E
m : MeasurableSpace α
hm : m ≤ m₀
hμm : ¬SigmaFinite (μ.trim hm)
⊢ μ[c • f | m] =ᵐ[μ] c • μ[f | m]

pp: case pos
α : Type u_1
E : Type u_3
𝕜 : Type u_4
inst✝⁴ : RCLike 𝕜
m₀ : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
f : α → E
m : MeasurableSpace α
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
⊢ μ[c • f | m] =ᵐ[μ] c • μ[f | m]

Tactic:
· simp_rw [condExp_of_not_sigmaFinite hm hμm]; simp

Goal state after:
case pos
α : Type u_1
E : Type u_3
𝕜 : Type u_4
inst✝⁴ : RCLike 𝕜
m₀ : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
f : α → E
m : MeasurableSpace α
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
⊢ μ[c • f | m] =ᵐ[μ] c • μ[f | m]
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator

Goal state before:
pp: case pos.refine_3
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hs : MeasurableSet s
hf : f =ᵐ[μ.restrict s] 0
hm : m ≤ m0
hμm this✝ : SigmaFinite (μ.trim hm)
this : SigmaFinite ((μ.restrict s).trim hm)
hf_int : Integrable f μ
t : Set α
ht : MeasurableSet t
⊢ (μ.restrict s) t < ∞ → ∫ (x : α) in t, μ[f | m] x ∂μ.restrict s = ∫ (x : α) in t, 0 x ∂μ.restrict s

Tactic:
_

Goal state after:
case pos.refine_3
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hs : MeasurableSet s
hf : f =ᵐ[μ.restrict s] 0
hm : m ≤ m0
hμm this✝ : SigmaFinite (μ.trim hm)
this : SigmaFinite ((μ.restrict s).trim hm)
hf_int : Integrable f μ
t : Set α
ht : MeasurableSet t
a✝ : (μ.restrict s) t < ∞
⊢ ∫ (x : α) in t, μ[f | m] x ∂μ.restrict s = ∫ (x : α) in t, 0 x ∂μ.restrict s
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator

Goal state before:
pp: α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hs : MeasurableSet s
hf : f =ᵐ[μ.restrict s] 0
hm : m ≤ m0
hμm this✝ : SigmaFinite (μ.trim hm)
this : SigmaFinite ((μ.restrict s).trim hm)
hf_int : Integrable f μ
t : Set α
ht : MeasurableSet t
a✝ : (μ.restrict s) t < ∞
x : α
hx : f x = 0 x
⊢ x ∈ t → f x = 0 x

Tactic:
_

Goal state after:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hs : MeasurableSet s
hf : f =ᵐ[μ.restrict s] 0
hm : m ≤ m0
hμm this✝ : SigmaFinite (μ.trim hm)
this : SigmaFinite ((μ.restrict s).trim hm)
hf_int : Integrable f μ
t : Set α
ht : MeasurableSet t
a✝¹ : (μ.restrict s) t < ∞
x : α
hx : f x = 0 x
a✝ : x ∈ t
⊢ f x = 0 x
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic

Goal state before:
pp: case pos
α : Type u_1
E : Type u_3
f : α → E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
m₁ m₂ m₀ : MeasurableSpace α
μ : Measure α
hm₁₂ : m₁ ≤ m₂
hm₂ : m₂ ≤ m₀
inst✝ : SigmaFinite (μ.trim hm₂)
hμm₁ : SigmaFinite (μ.trim ⋯)
hf : Integrable f μ
s : Set α
hs : MeasurableSet s
⊢ μ s < ∞ → ∫ (x : α) in s, μ[μ[f | m₂] | m₁] x ∂μ = ∫ (x : α) in s, μ[f | m₁] x ∂μ

Tactic:
_

Goal state after:
case pos
α : Type u_1
E : Type u_3
f : α → E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
m₁ m₂ m₀ : MeasurableSpace α
μ : Measure α
hm₁₂ : m₁ ≤ m₂
hm₂ : m₂ ≤ m₀
inst✝ : SigmaFinite (μ.trim hm₂)
hμm₁ : SigmaFinite (μ.trim ⋯)
hf : Integrable f μ
s : Set α
hs : MeasurableSet s
a✝ : μ s < ∞
⊢ ∫ (x : α) in s, μ[μ[f | m₂] | m₁] x ∂μ = ∫ (x : α) in s, μ[f | m₁] x ∂μ
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator

Goal state before:
pp: α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f μ
hs : MeasurableSet s
hm : m ≤ m0
hμm this✝ : SigmaFinite (μ.trim hm)
this : s.indicator μ[f | m] =ᵐ[μ] s.indicator μ[s.indicator f + sᶜ.indicator f | m]
⊢ s.indicator μ[s.indicator f | m] + s.indicator μ[sᶜ.indicator f | m] =ᵐ[μ]
    s.indicator μ[s.indicator f | m] + s.indicator (sᶜ.indicator μ[sᶜ.indicator f | m])

Tactic:
by
      refine Filter.EventuallyEq.rfl.add ?_
      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]
      filter_upwards [this] with x hx
      by_cases hxs : x ∈ s
      · simp only [hx, hxs, Set.indicator_of_mem]
      · simp only [hxs, Set.indicator_of_notMem, not_false_iff]

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic

Goal state before:
pp: α : Type u_1
E : Type u_3
𝕜 : Type u_4
inst✝⁵ : RCLike 𝕜
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : InnerProductSpace 𝕜 E
hm : m ≤ m₀
hf1 : Integrable f μ
hf2 : MemLp f 2 μ
inst✝ : SigmaFinite (μ.trim hm)
s : Set α
hs : MeasurableSet s
htop : μ s < ∞
ω : α
⊢ ↑↑(toLp f hf2) ω = f ω → ω ∈ s → ↑↑(toLp f hf2) ω = f ω

Tactic:
hω

Goal state after:
α : Type u_1
E : Type u_3
𝕜 : Type u_4
inst✝⁵ : RCLike 𝕜
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : InnerProductSpace 𝕜 E
hm : m ≤ m₀
hf1 : Integrable f μ
hf2 : MemLp f 2 μ
inst✝ : SigmaFinite (μ.trim hm)
s : Set α
hs : MeasurableSet s
htop : μ s < ∞
ω : α
hω : ↑↑(toLp f hf2) ω = f ω
⊢ ω ∈ s → ↑↑(toLp f hf2) ω = f ω
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic

Goal state before:
pp: α : Type u_1
E : Type u_3
𝕜 : Type u_4
inst✝⁵ : RCLike 𝕜
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : InnerProductSpace 𝕜 E
hm : m ≤ m₀
hf1 : Integrable f μ
hf2 : MemLp f 2 μ
inst✝ : SigmaFinite (μ.trim hm)
s : Set α
hs : MeasurableSet s
htop : μ s < ∞
ω : α
hω : ↑↑(toLp f hf2) ω = f ω
⊢ ω ∈ s → ↑↑(toLp f hf2) ω = f ω

Tactic:
_

Goal state after:
α : Type u_1
E : Type u_3
𝕜 : Type u_4
inst✝⁵ : RCLike 𝕜
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : InnerProductSpace 𝕜 E
hm : m ≤ m₀
hf1 : Integrable f μ
hf2 : MemLp f 2 μ
inst✝ : SigmaFinite (μ.trim hm)
s : Set α
hs : MeasurableSet s
htop : μ s < ∞
ω : α
hω : ↑↑(toLp f hf2) ω = f ω
a✝ : ω ∈ s
⊢ ↑↑(toLp f hf2) ω = f ω
Module: Mathlib.InformationTheory.KullbackLeibler.ChainRule

Goal state before:
pp: 𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst✝³ : IsFiniteMeasure μ
inst✝² : IsFiniteMeasure ν
inst✝¹ : IsMarkovKernel κ
inst✝ : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ ν ⊗ₘ η
h_int : Integrable (llr (μ ⊗ₘ κ) (ν ⊗ₘ η)) (μ ⊗ₘ κ)
h_ac_μν : μ ≪ ν
h_ac_κη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
h_int_μν : Integrable (llr μ ν) μ
h_int_κη : Integrable (llr (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)
this :
  ∫ (p : 𝓧 × 𝓨), llr (μ ⊗ₘ κ) (ν ⊗ₘ η) p ∂μ ⊗ₘ κ =
    ∫ (a : 𝓧), llr μ ν a ∂μ + ∫ (p : 𝓧 × 𝓨), llr (μ ⊗ₘ κ) (μ ⊗ₘ η) p ∂μ ⊗ₘ κ
⊢ ENNReal.ofReal (∫ (x : 𝓧 × 𝓨), llr (μ ⊗ₘ κ) (ν ⊗ₘ η) x ∂μ ⊗ₘ κ + (ν univ).toReal - (μ univ).toReal) =
    ENNReal.ofReal
      (∫ (x : 𝓧), llr μ ν x ∂μ + (ν univ).toReal - (μ univ).toReal + ∫ (x : 𝓧 × 𝓨), llr (μ ⊗ₘ κ) (μ ⊗ₘ η) x ∂μ ⊗ₘ κ)

Tactic:
by rw [this]; ring_nf

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator

Goal state before:
pp: case refine_1
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs_m : MeasurableSet s
hf_int : Integrable f μ
this : SigmaFinite ((μ.restrict s).trim hm)
t : Set α
ht : MeasurableSet t
⊢ μ t < ∞ → IntegrableOn (s.indicator (μ.restrict s)[f | m]) t μ

Tactic:
_

Goal state after:
case refine_1
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs_m : MeasurableSet s
hf_int : Integrable f μ
this : SigmaFinite ((μ.restrict s).trim hm)
t : Set α
ht : MeasurableSet t
a✝ : μ t < ∞
⊢ IntegrableOn (s.indicator (μ.restrict s)[f | m]) t μ
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator

Goal state before:
pp: case refine_2
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs_m : MeasurableSet s
hf_int : Integrable f μ
this : SigmaFinite ((μ.restrict s).trim hm)
t : Set α
ht : MeasurableSet t
⊢ μ t < ∞ → ∫ (x : α) in t, s.indicator (μ.restrict s)[f | m] x ∂μ = ∫ (x : α) in t, s.indicator f x ∂μ

Tactic:
_

Goal state after:
case refine_2
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs_m : MeasurableSet s
hf_int : Integrable f μ
this : SigmaFinite ((μ.restrict s).trim hm)
t : Set α
ht : MeasurableSet t
a✝ : μ t < ∞
⊢ ∫ (x : α) in t, s.indicator (μ.restrict s)[f | m] x ∂μ = ∫ (x : α) in t, s.indicator f x ∂μ
Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation

Goal state before:
pp: case pos
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
hm : mΩ ≤ mΩ₀
⊢ Measurable P⁻[X | mΩ]

Tactic:
by_cases hσ : SigmaFinite (P.trim hm)
    · by_cases hX : Measurable[mΩ] X
      · simp [condLExp_eq_self hm, hX]
      simp [condLExp_of_not_sub_sigma_measurable hm _ hX, measurable_rnDeriv]
    simp [condLExp_of_not_sigmaFinite hm hσ, measurable_zero]

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation

Goal state before:
pp: case neg
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
hm : ¬mΩ ≤ mΩ₀
⊢ Measurable P⁻[X | mΩ]

Tactic:
simp [condLExp_of_not_le hm, measurable_zero]

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator

Goal state before:
pp: case pos.refine_1
α : Type u_1
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
f : α → E
s : Set α
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m0
inst✝¹ : SigmaFinite (μ.trim hm)
inst✝ : SigmaFinite (μ.trim hm₂)
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) ↔ MeasurableSet (s ∩ t)
hs_m₂ : MeasurableSet s
hf_int : Integrable f μ
t : Set α
ht : MeasurableSet t
⊢ μ t < ∞ → ∫ (x : α) in t, μ[s.indicator f | m] x ∂μ = ∫ (x : α) in t, μ[s.indicator f | m₂] x ∂μ

Tactic:
_

Goal state after:
case pos.refine_1
α : Type u_1
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
f : α → E
s : Set α
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m0
inst✝¹ : SigmaFinite (μ.trim hm)
inst✝ : SigmaFinite (μ.trim hm₂)
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) ↔ MeasurableSet (s ∩ t)
hs_m₂ : MeasurableSet s
hf_int : Integrable f μ
t : Set α
ht : MeasurableSet t
a✝ : μ t < ∞
⊢ ∫ (x : α) in t, μ[s.indicator f | m] x ∂μ = ∫ (x : α) in t, μ[s.indicator f | m₂] x ∂μ
Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation

Goal state before:
pp: case h12
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
Y : Ω → ℝ≥0∞
hm : mΩ ≤ mΩ₀
P : Measure Ω
hσ : SigmaFinite (P.trim hm)
X : Ω → ℝ≥0∞
hY : AEMeasurable Y (P.trim hm)
hXY : ∀ (s : Set Ω), MeasurableSet s → ∫⁻ (ω : Ω) in s, Y ω ∂P = ∫⁻ (ω : Ω) in s, X ω ∂P
s : Set Ω
hs : MeasurableSet s
⊢ (P.trim hm) s < ∞ → ∫⁻ (x : Ω) in s, Y x ∂P.trim hm = ∫⁻ (x : Ω) in s, P⁻[X | mΩ] x ∂P.trim hm

Tactic:
_

Goal state after:
case h12
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
Y : Ω → ℝ≥0∞
hm : mΩ ≤ mΩ₀
P : Measure Ω
hσ : SigmaFinite (P.trim hm)
X : Ω → ℝ≥0∞
hY : AEMeasurable Y (P.trim hm)
hXY : ∀ (s : Set Ω), MeasurableSet s → ∫⁻ (ω : Ω) in s, Y ω ∂P = ∫⁻ (ω : Ω) in s, X ω ∂P
s : Set Ω
hs : MeasurableSet s
a✝ : (P.trim hm) s < ∞
⊢ ∫⁻ (x : Ω) in s, Y x ∂P.trim hm = ∫⁻ (x : Ω) in s, P⁻[X | mΩ] x ∂P.trim hm
Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation

Goal state before:
pp: Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hXY : X =ᵐ[P] Y
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
s : Set Ω
hs : MeasurableSet s
a✝ : Ω
h : X a✝ = Y a✝
⊢ a✝ ∈ s → X a✝ = Y a✝

Tactic:
_

Goal state after:
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hXY : X =ᵐ[P] Y
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
s : Set Ω
hs : MeasurableSet s
a✝¹ : Ω
h : X a✝¹ = Y a✝¹
a✝ : a✝¹ ∈ s
⊢ X a✝¹ = Y a✝¹
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
f : α → E
s : Set α
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m0
inst✝¹ : SigmaFinite (μ.trim hm)
inst✝ : SigmaFinite (μ.trim hm₂)
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) ↔ MeasurableSet (s ∩ t)
hs_m₂ : MeasurableSet s
hf_int : Integrable f μ
t : Set α
ht : MeasurableSet t
a✝ : μ t < ∞
this : μ[s.indicator f | m] =ᵐ[μ.restrict sᶜ] 0
x : α
hx : μ[s.indicator f | m] x = 0 x
⊢ x ∈ t → μ[s.indicator f | m] x = 0

Tactic:
_

Goal state after:
α : Type u_1
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
f : α → E
s : Set α
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m0
inst✝¹ : SigmaFinite (μ.trim hm)
inst✝ : SigmaFinite (μ.trim hm₂)
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) ↔ MeasurableSet (s ∩ t)
hs_m₂ : MeasurableSet s
hf_int : Integrable f μ
t : Set α
ht : MeasurableSet t
a✝¹ : μ t < ∞
this : μ[s.indicator f | m] =ᵐ[μ.restrict sᶜ] 0
x : α
hx : μ[s.indicator f | m] x = 0 x
a✝ : x ∈ t
⊢ μ[s.indicator f | m] x = 0
Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation

Goal state before:
pp: case pos.h12
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hXY : X ≤ᵐ[P] Y
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
s : Set Ω
hs : MeasurableSet s
⊢ (P.trim hm) s < ∞ → ∫⁻ (x : Ω) in s, P⁻[X | mΩ] x ∂P.trim hm ≤ ∫⁻ (x : Ω) in s, P⁻[Y | mΩ] x ∂P.trim hm

Tactic:
_

Goal state after:
case pos.h12
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hXY : X ≤ᵐ[P] Y
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
s : Set Ω
hs : MeasurableSet s
a✝ : (P.trim hm) s < ∞
⊢ ∫⁻ (x : Ω) in s, P⁻[X | mΩ] x ∂P.trim hm ≤ ∫⁻ (x : Ω) in s, P⁻[Y | mΩ] x ∂P.trim hm
Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation

Goal state before:
pp: case pos.h12
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
s : Set Ω
hs : MeasurableSet s
⊢ (P.trim hm) s < ∞ →
    ∫⁻ (x : Ω) in s, (P⁻[X | mΩ] + P⁻[Y | mΩ]) x ∂P.trim hm ≤ ∫⁻ (x : Ω) in s, P⁻[X + Y | mΩ] x ∂P.trim hm

Tactic:
_

Goal state after:
case pos.h12
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
s : Set Ω
hs : MeasurableSet s
a✝ : (P.trim hm) s < ∞
⊢ ∫⁻ (x : Ω) in s, (P⁻[X | mΩ] + P⁻[Y | mΩ]) x ∂P.trim hm ≤ ∫⁻ (x : Ω) in s, P⁻[X + Y | mΩ] x ∂P.trim hm
Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation

Goal state before:
pp: case pos.h12
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
c : ℝ≥0∞
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
s : Set Ω
hs : MeasurableSet s
⊢ (P.trim hm) s < ∞ → ∫⁻ (x : Ω) in s, (c • P⁻[X | mΩ]) x ∂P.trim hm ≤ ∫⁻ (x : Ω) in s, P⁻[c • X | mΩ] x ∂P.trim hm

Tactic:
_

Goal state after:
case pos.h12
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
c : ℝ≥0∞
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
s : Set Ω
hs : MeasurableSet s
a✝ : (P.trim hm) s < ∞
⊢ ∫⁻ (x : Ω) in s, (c • P⁻[X | mΩ]) x ∂P.trim hm ≤ ∫⁻ (x : Ω) in s, P⁻[c • X | mΩ] x ∂P.trim hm
Module: Mathlib.LinearAlgebra.AffineSpace.Matrix

Goal state before:
pp: ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁵ : AddCommGroup V
inst✝⁴ : AffineSpace V P
inst✝³ : CommRing k
inst✝² : Module k V
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b b₂ : AffineBasis ι k P
x : P
hu : IsUnit (b.toMatrix ⇑b₂).det
⊢ b₂.coords x ᵥ* 1 = b₂.coords x

Tactic:
Matrix.vecMul_one

Goal state after:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁵ : AddCommGroup V
inst✝⁴ : AffineSpace V P
inst✝³ : CommRing k
inst✝² : Module k V
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b b₂ : AffineBasis ι k P
x : P
hu : IsUnit (b.toMatrix ⇑b₂).det
⊢ b₂.coords x = b₂.coords x
Module: Mathlib.LinearAlgebra.BilinearForm.IsometryEquiv

Goal state before:
pp: R : Type u_1
M : Type u_2
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
M₄ : Type u_6
N : Type u_7
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M₁
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommMonoid M₄
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R M
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module R M₄
inst✝ : Module R N
B₁ : LinearMap.BilinForm R M₁
B₂ : LinearMap.BilinForm R M₂
B₃ : LinearMap.BilinForm R M₃
f : B₁.IsometryEquiv B₂
n✝ : M₂
⊢ ∀ (m : M₂), (B₁ ((↑f.symm).toFun n✝)) ((↑f.symm).toFun m) = (B₂ n✝) m

Tactic:
_

Goal state after:
R : Type u_1
M : Type u_2
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
M₄ : Type u_6
N : Type u_7
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M₁
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommMonoid M₄
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R M
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module R M₄
inst✝ : Module R N
B₁ : LinearMap.BilinForm R M₁
B₂ : LinearMap.BilinForm R M₂
B₃ : LinearMap.BilinForm R M₃
f : B₁.IsometryEquiv B₂
n✝ m✝ : M₂
⊢ (B₁ ((↑f.symm).toFun n✝)) ((↑f.symm).toFun m✝) = (B₂ n✝) m✝
Module: Mathlib.LinearAlgebra.BilinearForm.IsometryEquiv

Goal state before:
pp: R : Type u_1
M : Type u_2
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
M₄ : Type u_6
N : Type u_7
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M₁
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommMonoid M₄
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R M
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module R M₄
inst✝ : Module R N
B : LinearMap.BilinForm R M
f : M₁ ≃ₗ[R] M
n✝ : M
⊢ ∀ (m : M), ((B.comp ↑f ↑f) ((↑f.symm).toFun n✝)) ((↑f.symm).toFun m) = (B n✝) m

Tactic:
_

Goal state after:
R : Type u_1
M : Type u_2
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
M₄ : Type u_6
N : Type u_7
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M₁
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommMonoid M₄
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R M
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module R M₄
inst✝ : Module R N
B : LinearMap.BilinForm R M
f : M₁ ≃ₗ[R] M
n✝ m✝ : M
⊢ ((B.comp ↑f ↑f) ((↑f.symm).toFun n✝)) ((↑f.symm).toFun m✝) = (B n✝) m✝