mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd

Goal state before:
pp: case pos.h_add
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝³ : NormedAddCommGroup E
a : α
κ : Kernel α β
inst✝² : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : NormedSpace ℝ E
f✝ : β × γ → E
hE : CompleteSpace E
f g : β × γ → E
a✝ : Disjoint (support f) (support g)
i_f : Integrable f ((κ ⊗ₖ η) a)
i_g : Integrable g ((κ ⊗ₖ η) a)
hf : ∫ (z : β × γ), f z ∂(κ ⊗ₖ η) a = ∫ (x : β), ∫ (y : γ), f (x, y) ∂η (a, x) ∂κ a
hg : ∫ (z : β × γ), g z ∂(κ ⊗ₖ η) a = ∫ (x : β), ∫ (y : γ), g (x, y) ∂η (a, x) ∂κ a
⊢ ∫ (z : β × γ), (f + g) z ∂(κ ⊗ₖ η) a = ∫ (x : β), ∫ (y : γ), (f + g) (x, y) ∂η (a, x) ∂κ a

Tactic:
integral_add' i_f i_g,

Goal state after:
case pos.h_add
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝³ : NormedAddCommGroup E
a : α
κ : Kernel α β
inst✝² : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : NormedSpace ℝ E
f✝ : β × γ → E
hE : CompleteSpace E
f g : β × γ → E
a✝ : Disjoint (support f) (support g)
i_f : Integrable f ((κ ⊗ₖ η) a)
i_g : Integrable g ((κ ⊗ₖ η) a)
hf : ∫ (z : β × γ), f z ∂(κ ⊗ₖ η) a = ∫ (x : β), ∫ (y : γ), f (x, y) ∂η (a, x) ∂κ a
hg : ∫ (z : β × γ), g z ∂(κ ⊗ₖ η) a = ∫ (x : β), ∫ (y : γ), g (x, y) ∂η (a, x) ∂κ a
⊢ ∫ (a : β × γ), f a ∂(κ ⊗ₖ η) a + ∫ (a : β × γ), g a ∂(κ ⊗ₖ η) a = ∫ (x : β), ∫ (y : γ), (f + g) (x, y) ∂η (a, x) ∂κ a
Module: Mathlib.MeasureTheory.Measure.Tilted

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ
g : α → E
s : Set α
hs : MeasurableSet s
hf : AEMeasurable f μ
⊢ AEMeasurable (fun x ↦ NNReal.mk (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) ⋯) (μ.restrict s)

Tactic:
suffices AEMeasurable (fun x ↦ exp (f x) / ∫ x, exp (f x) ∂μ) μ by
        rw [← aemeasurable_coe_nnreal_real_iff]
        refine AEMeasurable.restrict ?_
        simpa only [NNReal.coe_mk]
      exact (measurable_exp.comp_aemeasurable hf).div_const _

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Tilted

Goal state before:
pp: case pos.hf
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
f : α → ℝ
g : α → E
s : Set α
hf : AEMeasurable f μ
⊢ AEMeasurable (fun x ↦ NNReal.mk (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) ⋯) (μ.restrict s)

Tactic:
suffices AEMeasurable (fun x ↦ exp (f x) / ∫ x, exp (f x) ∂μ) μ by
        rw [← aemeasurable_coe_nnreal_real_iff]
        refine AEMeasurable.restrict ?_
        simpa only [NNReal.coe_mk]
      exact (measurable_exp.comp_aemeasurable hf).div_const _

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Tilted

Goal state before:
pp: case inr
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable (fun x ↦ rexp (f x)) μ
g : α → ℝ
h0 : NeZero μ
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : α) in s, ENNReal.ofReal (rexp (g a) / ∫ (x : α), rexp (g x) ∂μ.tilted f) ∂μ.tilted f =
    ∫⁻ (a : α) in s, ENNReal.ofReal (rexp ((f + g) a) / ∫ (x : α), rexp ((f + g) x) ∂μ) ∂μ

Tactic:
setLIntegral_tilted' f _ hs

Goal state after:
case inr
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable (fun x ↦ rexp (f x)) μ
g : α → ℝ
h0 : NeZero μ
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (x : α) in s,
      ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) *
        ENNReal.ofReal (rexp (g x) / ∫ (x : α), rexp (g x) ∂μ.tilted f) ∂μ =
    ∫⁻ (a : α) in s, ENNReal.ofReal (rexp ((f + g) a) / ∫ (x : α), rexp ((f + g) x) ∂μ) ∂μ
Module: Mathlib.MeasureTheory.Measure.Tilted

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable (fun x ↦ rexp (f x)) μ
⊢ μ ≪ μ.tilted f

Tactic:
by
  cases eq_zero_or_neZero μ with
  | inl h => simp only [h, tilted_zero_measure]; exact fun _ _ ↦ by simp
  | inr h0 =>
    refine withDensity_absolutelyContinuous' ?_ ?_
    · exact (hf.1.aemeasurable.div_const _).ennreal_ofReal
    · filter_upwards
      simp only [ne_eq, ENNReal.ofReal_eq_zero, not_le]
      exact fun _ ↦ div_pos (exp_pos _) (integral_exp_pos hf)

Goal state after:
Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd

Goal state before:
pp: case pos.h_add
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : NormedAddCommGroup E
a : α
κ : Kernel α β
η : Kernel β γ
inst✝ : NormedSpace ℝ E
f✝ : γ → E
hE : CompleteSpace E
f g : γ → E
i_f : Integrable f ((η ∘ₖ κ) a)
i_g : Integrable g ((η ∘ₖ κ) a)
hf : ∫ (z : γ), f z ∂(η ∘ₖ κ) a = ∫ (x : β), ∫ (y : γ), f y ∂η x ∂κ a
hg : ∫ (z : γ), g z ∂(η ∘ₖ κ) a = ∫ (x : β), ∫ (y : γ), g y ∂η x ∂κ a
⊢ ∫ (z : γ), (f + g) z ∂(η ∘ₖ κ) a = ∫ (x : β), ∫ (y : γ), (f + g) y ∂η x ∂κ a

Tactic:
integral_add' i_f i_g,

Goal state after:
case pos.h_add
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : NormedAddCommGroup E
a : α
κ : Kernel α β
η : Kernel β γ
inst✝ : NormedSpace ℝ E
f✝ : γ → E
hE : CompleteSpace E
f g : γ → E
i_f : Integrable f ((η ∘ₖ κ) a)
i_g : Integrable g ((η ∘ₖ κ) a)
hf : ∫ (z : γ), f z ∂(η ∘ₖ κ) a = ∫ (x : β), ∫ (y : γ), f y ∂η x ∂κ a
hg : ∫ (z : γ), g z ∂(η ∘ₖ κ) a = ∫ (x : β), ∫ (y : γ), g y ∂η x ∂κ a
⊢ ∫ (a : γ), f a ∂(η ∘ₖ κ) a + ∫ (a : γ), g a ∂(η ∘ₖ κ) a = ∫ (x : β), ∫ (z : γ), (f + g) z ∂η x ∂κ a
Module: Mathlib.InformationTheory.KullbackLeibler.Basic

Goal state before:
pp: case pos
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int_iff :
  ∫⁻ (a : α), ENNReal.ofReal (klFun (μ.rnDeriv ν a).toReal) ∂ν ≠ ∞ ↔ Integrable (fun x ↦ klFun (μ.rnDeriv ν x).toReal) ν
h_int : Integrable (llr μ ν) μ
⊢ ENNReal.ofReal (∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν) =
    ∫⁻ (x : α), ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal) ∂ν

Tactic:
ofReal_integral_eq_lintegral_ofReal

Goal state after:
case pos
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int_iff :
  ∫⁻ (a : α), ENNReal.ofReal (klFun (μ.rnDeriv ν a).toReal) ∂ν ≠ ∞ ↔ Integrable (fun x ↦ klFun (μ.rnDeriv ν x).toReal) ν
h_int : Integrable (llr μ ν) μ
⊢ ∫⁻ (x : α), ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal) ∂ν =
    ∫⁻ (x : α), ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal) ∂ν

case pos.hfi
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int_iff :
  ∫⁻ (a : α), ENNReal.ofReal (klFun (μ.rnDeriv ν a).toReal) ∂ν ≠ ∞ ↔ Integrable (fun x ↦ klFun (μ.rnDeriv ν x).toReal) ν
h_int : Integrable (llr μ ν) μ
⊢ Integrable (fun x ↦ klFun (μ.rnDeriv ν x).toReal) ν

case pos.f_nn
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int_iff :
  ∫⁻ (a : α), ENNReal.ofReal (klFun (μ.rnDeriv ν a).toReal) ∂ν ≠ ∞ ↔ Integrable (fun x ↦ klFun (μ.rnDeriv ν x).toReal) ν
h_int : Integrable (llr μ ν) μ
⊢ 0 ≤ᵐ[ν] fun x ↦ klFun (μ.rnDeriv ν x).toReal
Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio

Goal state before:

Tactic:
∫ x, llr μ (ν.tilted f) x ∂μ
    = ∫ x, -f x + log (∫ x, exp (f x) ∂ν) + llr μ ν x ∂μ :=
        integral_congr_ae (llr_tilted_right hμν hfν)
  _ = -∫ x, f x ∂μ + log (∫ x, exp (f x) ∂ν) + ∫ x, llr μ ν x ∂μ := by
        rw [← integral_neg, integral_add ?_ h_int]
        swap; · exact hfμ.neg.add (integrable_const _)
        rw [integral_add ?_ (integrable_const _)]
        swap; · exact hfμ.neg
        simp only [integral_const, probReal_univ, smul_eq_mul, one_mul]
  _ = ∫ x, llr μ ν x ∂μ - ∫ x, f x ∂μ + log (∫ x, exp (f x) ∂ν) := by abel

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

Goal state before:
pp: α : Type u_1
E' : Type u_2
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace 𝕜 E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
hm : m ≤ m0
f : ↥(Lp E' p μ)
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn (↑↑f) s μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, ↑↑f x ∂μ = 0
hf_meas : AEStronglyMeasurable (↑↑f) μ
f_meas : ↥(lpMeas E' 𝕜 m p μ) := ⟨f, hf_meas⟩
hf_f_meas : ↑↑f =ᵐ[μ] ↑↑↑f_meas
⊢ ↑↑↑f_meas =ᵐ[μ] 0

Tactic:
exact lpMeas.ae_eq_zero_of_forall_setIntegral_eq_zero
    hm f_meas hp_ne_zero hp_ne_top hf_int_finite hf_zero

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

Goal state before:
pp: α : Type u_1
E' : Type u_2
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace 𝕜 E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
hm : m ≤ m0
f g : ↥(Lp E' p μ)
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn (↑↑f) s μ
hg_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn (↑↑g) s μ
hfg : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, ↑↑f x ∂μ = ∫ (x : α) in s, ↑↑g x ∂μ
hf_meas : AEStronglyMeasurable (↑↑f) μ
hg_meas : AEStronglyMeasurable (↑↑g) μ
h_sub : ↑↑(f - g) =ᵐ[μ] 0
⊢ ↑↑f =ᵐ[μ] ↑↑g

Tactic:
← sub_ae_eq_zero

Goal state after:
α : Type u_1
E' : Type u_2
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace 𝕜 E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
hm : m ≤ m0
f g : ↥(Lp E' p μ)
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn (↑↑f) s μ
hg_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn (↑↑g) s μ
hfg : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, ↑↑f x ∂μ = ∫ (x : α) in s, ↑↑g x ∂μ
hf_meas : AEStronglyMeasurable (↑↑f) μ
hg_meas : AEStronglyMeasurable (↑↑g) μ
h_sub : ↑↑(f - g) =ᵐ[μ] 0
⊢ ↑↑f - ↑↑g =ᵐ[μ] 0
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1

Goal state before:
pp: α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : μ s ≠ ∞
x y : G
⊢ ↑↑(MemLp.toLp ↑↑(condExpIndSMul hm hs hμs (x + y)) ⋯) =ᵐ[μ]
    ↑↑(MemLp.toLp ↑↑(condExpIndSMul hm hs hμs x) ⋯) + ↑↑(MemLp.toLp ↑↑(condExpIndSMul hm hs hμs y) ⋯)

Tactic:
MemLp.coeFn_toLp,

Goal state after:
α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : μ s ≠ ∞
x y : G
⊢ ↑↑(condExpIndSMul hm hs hμs (x + y)) =ᵐ[μ]
    ↑↑(MemLp.toLp ↑↑(condExpIndSMul hm hs hμs x) ⋯) + ↑↑(MemLp.toLp ↑↑(condExpIndSMul hm hs hμs y) ⋯)
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1

Goal state before:
pp: α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : μ s ≠ ∞
x y : G
⊢ ↑↑(condExpIndSMul hm hs hμs (x + y)) =ᵐ[μ]
    ↑↑(MemLp.toLp ↑↑(condExpIndSMul hm hs hμs x) ⋯) + ↑↑(MemLp.toLp ↑↑(condExpIndSMul hm hs hμs y) ⋯)

Tactic:
MemLp.coeFn_toLp,

Goal state after:
α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : μ s ≠ ∞
x y : G
⊢ ↑↑(condExpIndSMul hm hs hμs (x + y)) =ᵐ[μ]
    ↑↑(condExpIndSMul hm hs hμs x) + ↑↑(MemLp.toLp ↑↑(condExpIndSMul hm hs hμs y) ⋯)
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1

Goal state before:
pp: α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : μ s ≠ ∞
x y : G
⊢ ↑↑(condExpIndSMul hm hs hμs (x + y)) =ᵐ[μ]
    ↑↑(condExpIndSMul hm hs hμs x) + ↑↑(MemLp.toLp ↑↑(condExpIndSMul hm hs hμs y) ⋯)

Tactic:
MemLp.coeFn_toLp,

Goal state after:
α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : μ s ≠ ∞
x y : G
⊢ ↑↑(condExpIndSMul hm hs hμs (x + y)) =ᵐ[μ] ↑↑(condExpIndSMul hm hs hμs x) + ↑↑(condExpIndSMul hm hs hμs y)
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2

Goal state before:
pp: case refine_2
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ∞
inst✝ : SigmaFinite (μ.trim hm)
h : AEStronglyMeasurable (↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1))) μ
t : Set α
ht : MeasurableSet t
hμt : (μ.trim hm) t < ∞
⊢ 0 ≤ ∫ (x : α) in t, AEStronglyMeasurable.mk (↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1))) h x ∂μ.trim hm

Tactic:
← setIntegral_trim hm h.stronglyMeasurable_mk ht

Goal state after:
case refine_2
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ∞
inst✝ : SigmaFinite (μ.trim hm)
h : AEStronglyMeasurable (↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1))) μ
t : Set α
ht : MeasurableSet t
hμt : (μ.trim hm) t < ∞
⊢ 0 ≤ ∫ (x : α) in t, AEStronglyMeasurable.mk (↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1))) h x ∂μ
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic

Goal state before:
pp: case empty
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
ι : Type u_5
f : ι → α → E
m : MeasurableSpace α
hf : ∀ i ∈ ∅, Integrable (f i) μ
⊢ μ[∑ i ∈ ∅, f i | m] =ᵐ[μ] ∑ i ∈ ∅, μ[f i | m]

Tactic:
Finset.sum_empty,

Goal state after:
case empty
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
ι : Type u_5
f : ι → α → E
m : MeasurableSpace α
hf : ∀ i ∈ ∅, Integrable (f i) μ
⊢ μ[0 | m] =ᵐ[μ] ∑ i ∈ ∅, μ[f i | m]
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic

Goal state before:
pp: case empty
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
ι : Type u_5
f : ι → α → E
m : MeasurableSpace α
hf : ∀ i ∈ ∅, Integrable (f i) μ
⊢ μ[0 | m] =ᵐ[μ] ∑ i ∈ ∅, μ[f i | m]

Tactic:
Finset.sum_empty,

Goal state after:
case empty
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
ι : Type u_5
f : ι → α → E
m : MeasurableSpace α
hf : ∀ i ∈ ∅, Integrable (f i) μ
⊢ μ[0 | m] =ᵐ[μ] 0
Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation

Goal state before:
pp: case pos
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hXY : X ≤ᵐ[P] Y
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
⊢ P⁻[X | mΩ] ≤ᵐ[P] P⁻[Y | mΩ]

Tactic:
apply ae_le_of_ae_le_trim

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)
⊢ P⁻[X | mΩ] ≤ᵐ[P.trim ?pos.hm✝] P⁻[Y | mΩ]

case pos.m
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hXY : X ≤ᵐ[P] Y
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
⊢ MeasurableSpace Ω

case pos.hm
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hXY : X ≤ᵐ[P] Y
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
⊢ ?pos.m✝ ≤ mΩ₀
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.LebesgueBochner

Goal state before:
pp: case pos
𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
f : 𝓧 → ℝ
hf : Integrable f μ
h'f : 0 ≤ᵐ[μ] f
hm : m ≤ m𝓧
hμ : SigmaFinite (μ.trim hm)
A : μ[fun x ↦ (ENNReal.ofReal (f x)).toReal | m] =ᵐ[μ] μ[f | m]
B : 0 ≤ᵐ[μ] μ[f | m]
⊢ μ⁻[fun x ↦ ENNReal.ofReal (f x) | m] =ᵐ[μ] fun x ↦ ENNReal.ofReal (μ[f | m] x)

Tactic:
let g x := ENNReal.ofReal (f x)

Goal state after:
case pos
𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
f : 𝓧 → ℝ
hf : Integrable f μ
h'f : 0 ≤ᵐ[μ] f
hm : m ≤ m𝓧
hμ : SigmaFinite (μ.trim hm)
A : μ[fun x ↦ (ENNReal.ofReal (f x)).toReal | m] =ᵐ[μ] μ[f | m]
B : 0 ≤ᵐ[μ] μ[f | m]
g : 𝓧 → ℝ≥0∞ := fun x ↦ ENNReal.ofReal (f x)
⊢ μ⁻[fun x ↦ ENNReal.ofReal (f x) | m] =ᵐ[μ] fun x ↦ ENNReal.ofReal (μ[f | m] x)
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym

Goal state before:
pp: case refine_1
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst✝ : IsFiniteMeasure μ
hμν : μ ≪ ν
g : 𝓧 → 𝓨
hg : Measurable g
hσ : SigmaFinite (Measure.map g ν)
this✝ : SigmaFinite (ν.trim ⋯)
this : SigmaFinite ν
t : Set 𝓨
left✝ : MeasurableSet t
a✝ : ν (g ⁻¹' t) < ∞
⊢ IntegrableOn (fun a ↦ ((Measure.map g μ).rnDeriv (Measure.map g ν) (g a)).toReal) (g ⁻¹' t) ν

Tactic:
exact Integrable.integrableOn (Measure.integrable_toReal_rnDeriv.comp_measurable hg)

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

Goal state before:
pp: case pos
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
⊢ P⁻[X | mΩ] + P⁻[Y | mΩ] ≤ᵐ[P] P⁻[X + Y | mΩ]

Tactic:
apply ae_le_of_ae_le_trim

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)
⊢ P⁻[X | mΩ] + P⁻[Y | mΩ] ≤ᵐ[P.trim ?pos.hm✝] P⁻[X + Y | mΩ]

case pos.m
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
⊢ MeasurableSpace Ω

case pos.hm
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
⊢ ?pos.m✝ ≤ mΩ₀
Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation

Goal state before:
pp: case pos
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
c : ℝ≥0∞
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
⊢ c • P⁻[X | mΩ] ≤ᵐ[P] P⁻[c • X | mΩ]

Tactic:
apply ae_le_of_ae_le_trim

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)
⊢ c • P⁻[X | mΩ] ≤ᵐ[P.trim ?pos.hm✝] P⁻[c • X | mΩ]

case pos.m
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
c : ℝ≥0∞
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
⊢ MeasurableSpace Ω

case pos.hm
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
c : ℝ≥0∞
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
⊢ ?pos.m✝ ≤ mΩ₀
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Shift

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Ring k
inst✝⁴ : AddCommGroup V
inst✝³ : AddTorsor V P
inst✝² : Module k V
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : Nontrivial ι
p : ι → P
i : ι
w : ι → k
hw : ∑ i, w i = 1
⊢ (affineCombination k univ p) w ∈ (affineSpan k (p '' {i}ᶜ)).shift (p i) (1 - w i)

Tactic:
by
  cases subsingleton_or_nontrivial k
  · suffices (affineSpan k <| p '' {i}ᶜ) = ⊤ by simp [this]
    have : Subsingleton P := (AddTorsor.subsingleton_iff V P).mp <| Module.subsingleton k V
    simp
  classical
  obtain ⟨j, hj⟩ := exists_ne i
  rw [shift_eq ⟨p j, mem_affineSpan k <| Set.mem_image_of_mem _ hj⟩]
  suffices ∃ q ∈ affineSpan k (p '' {i}ᶜ), w i • (p i -ᵥ p j) +ᵥ q = affineCombination k univ p w by
    simpa
  refine ⟨-(w i • (p i -ᵥ p j)) +ᵥ affineCombination k univ p w, ?_, by simp⟩
  rw [← affineCombination_piSingle k _ p (mem_univ i),
    ← affineCombination_piSingle k _ p (mem_univ j), affineCombination_vsub, ← map_smul, ← map_neg,
    weightedVSub_vadd_affineCombination]
  refine affineCombination_mem_affineSpan_image ?_ (fun i' _ hi ↦ by aesop) _
  simp [sum_add_distrib, ← mul_sum, hw]

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeHom

Goal state before:
pp: R : Type u_1
inst✝¹⁴ : CommSemiring R
S : Type u_2
inst✝¹³ : CommSemiring S
inst✝¹² : Algebra R S
M : Type u_3
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
N : Type u_4
inst✝⁹ : AddCommMonoid N
inst✝⁸ : Module R N
P : Type u_5
inst✝⁷ : AddCommMonoid P
inst✝⁶ : Module R P
Q : Type u_6
inst✝⁵ : AddCommMonoid Q
inst✝⁴ : Module R Q
inst✝³ : Module S P
inst✝² : IsScalarTower R S P
inst✝¹ : Module S Q
inst✝ : IsScalarTower R S Q
α : M →ₗ[R] P
j : IsBaseChange S α
β : N →ₗ[R] Q
f : M →ₗ[R] N
m : M
⊢ ((j.linearMapLeftRightHom β) f) (α m) = β (f m)

Tactic:
simp [linearMapLeftRightHom_apply, IsBaseChange.equiv_symm_apply]

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Shift

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁶ : Field k
inst✝⁵ : LinearOrder k
inst✝⁴ : IsOrderedRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
n : ℕ
inst✝ : NeZero n
s : Simplex k P n
i : Fin (n + 1)
x : k
hx : x ∈ Set.Icc 0 1
hxpos : 0 < x
w : Fin (n + 1) → k
hw : ∑ i, w i = 1
hp : (affineCombination k univ s.points) w ∈ affineSpan k (Set.range s.points)
j : Fin (n + 1)
hj : j ≠ i
⊢ x⁻¹ * w j ∈ Set.Icc 0 1 ↔ (lineMap (Pi.single i 1) w) x⁻¹ j ∈ Set.Icc 0 1

Tactic:
by simp [lineMap_apply, hj]

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Shift

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁶ : Field k
inst✝⁵ : LinearOrder k
inst✝⁴ : IsOrderedRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
n : ℕ
inst✝ : NeZero n
s : Simplex k P n
i : Fin (n + 1)
x : k
hx : x ∈ Set.Icc 0 1
hxpos : 0 < x
w : Fin (n + 1) → k
hw : ∑ i, w i = 1
hp : (affineCombination k univ s.points) w ∈ affineSpan k (Set.range s.points)
j : Fin (n + 1)
hj : ¬j = i
⊢ x⁻¹ * w j ∈ Set.Icc 0 1 ↔ (lineMap (Pi.single i 1) w) x⁻¹ j ∈ Set.Icc 0 1

Tactic:
by simp [lineMap_apply, hj]

Goal state after:
Module: Mathlib.LinearAlgebra.Center

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝⁴ : Ring R
inst✝³ : IsDomain R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
f : V →ₗ[R] V
ι : Type u_3
inst✝ : Nontrivial ι
b : Basis ι R V
i j : ι
h : ∀ (v : V), ∃ x x_1, ∃ (_ : x • v + x_1 • f v = 0), ¬(x = 0 ∧ x_1 = 0)
⊢ (b.repr (f (b i))) j = (b.repr ((b.coord i) (f (b i)) • b i)) j

Tactic:
obtain ⟨s, t, ⟨h, h'⟩⟩ := h (b i)

Goal state after:
R : Type u_1
V : Type u_2
inst✝⁴ : Ring R
inst✝³ : IsDomain R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
f : V →ₗ[R] V
ι : Type u_3
inst✝ : Nontrivial ι
b : Basis ι R V
i j : ι
h✝ : ∀ (v : V), ∃ x x_1, ∃ (_ : x • v + x_1 • f v = 0), ¬(x = 0 ∧ x_1 = 0)
s t : R
h : s • b i + t • f (b i) = 0
h' : ¬(s = 0 ∧ t = 0)
⊢ (b.repr (f (b i))) j = (b.repr ((b.coord i) (f (b i)) • b i)) j
Module: Mathlib.LinearAlgebra.Transvection.Basic

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
f : Dual R V
v w : V
hw : f w = 0
⊢ transvection f v ∘ₗ transvection f w = transvection f (v + w)

Tactic:
by
  ext; simp [comp_of_left_eq_apply hw]

Goal state after:
Module: Mathlib.LinearAlgebra.Transvection.Basic

Goal state before:
pp: case «1»
R : Type u_3
V : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid V
inst✝³ : Module R V
inst✝² : Free R V
inst✝¹ : Module.Finite R V
inst✝ : StrongRankCondition R
f : Dual R V
v : V
hfv : f v = 0
h : finrank R V = 1
h1 : 1 ≤ 1
b : Basis (Fin (finrank R V)) R V := finBasis R V
x✝ : V
i : Fin (finrank R V) := ⟨0, ⋯⟩
x : V
⊢ x = (b.repr x) i • b i

Tactic:
have : x = ∑ i, b.repr x i • b i := (b.sum_equivFun x).symm

Goal state after:
case «1»
R : Type u_3
V : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid V
inst✝³ : Module R V
inst✝² : Free R V
inst✝¹ : Module.Finite R V
inst✝ : StrongRankCondition R
f : Dual R V
v : V
hfv : f v = 0
h : finrank R V = 1
h1 : 1 ≤ 1
b : Basis (Fin (finrank R V)) R V := finBasis R V
x✝ : V
i : Fin (finrank R V) := ⟨0, ⋯⟩
x : V
this : x = ∑ i, (b.repr x) i • b i
⊢ x = (b.repr x) i • b i