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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
f : α × β → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : Set β
ht : MeasurableSet t
⊢ ∫⁻ (x : α × β) in s ×ˢ t, f x ∂μ ⊗ₘ κ = ∫⁻ (a : α) in s, ∫⁻ (b : β) in t, f (a, b) ∂κ a ∂μ

Tactic:
rw [compProd, Kernel.setLIntegral_compProd _ _ _ hf hs ht]

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
f : α × β → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : Set β
ht : MeasurableSet t
⊢ ∫⁻ (x : α) in s, ∫⁻ (y : β) in t, f (x, y) ∂(Kernel.prodMkLeft Unit κ) ((), x) ∂(Kernel.const Unit μ) () =
    ∫⁻ (a : α) in s, ∫⁻ (b : β) in t, f (a, b) ∂κ a ∂μ
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
γ : Type u_3
mγ : MeasurableSpace γ
η : Kernel (α × β) γ
hμ : SFinite μ
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
s : Set ((α × β) × γ)
hs : MeasurableSet s
⊢ (map (⇑MeasurableEquiv.prodAssoc.symm) (μ ⊗ₘ (κ ⊗ₖ η))) s = (μ ⊗ₘ κ ⊗ₘ η) s

Tactic:
rw [Measure.compProd_apply hs, Measure.map_apply (by fun_prop) hs,
    Measure.compProd_apply (hs.preimage (by fun_prop)), Measure.lintegral_compProd]

Goal state after:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
γ : Type u_3
mγ : MeasurableSpace γ
η : Kernel (α × β) γ
hμ : SFinite μ
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
s : Set ((α × β) × γ)
hs : MeasurableSet s
⊢ ∫⁻ (a : α), ((κ ⊗ₖ η) a) (Prod.mk a ⁻¹' ⇑MeasurableEquiv.prodAssoc.symm ⁻¹' s) ∂μ =
    ∫⁻ (a : α), ∫⁻ (b : β), (η (a, b)) (Prod.mk (a, b) ⁻¹' s) ∂κ a ∂μ

case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
γ : Type u_3
mγ : MeasurableSpace γ
η : Kernel (α × β) γ
hμ : SFinite μ
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
s : Set ((α × β) × γ)
hs : MeasurableSet s
⊢ Measurable fun a ↦ (η a) (Prod.mk a ⁻¹' s)
Module: Mathlib.Probability.Kernel.Composition.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
μ : Measure β
inst✝¹ : SFinite μ
ν : Measure γ
inst✝ : SFinite ν
⊢ const α μ ×ₖ const α ν = const α (μ.prod ν)

Tactic:
ext x

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
μ : Measure β
inst✝¹ : SFinite μ
ν : Measure γ
inst✝ : SFinite ν
x : α
s✝ : Set (β × γ)
a✝ : MeasurableSet s✝
⊢ ((const α μ ×ₖ const α ν) x) s✝ = ((const α (μ.prod ν)) x) s✝
Module: Mathlib.Probability.Kernel.Composition.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
μ : Measure β
inst✝¹ : SFinite μ
ν : Measure γ
inst✝ : SFinite ν
x : α
s✝ : Set (β × γ)
a✝ : MeasurableSet s✝
⊢ ((const α μ ×ₖ const α ν) x) s✝ = ((const α (μ.prod ν)) x) s✝

Tactic:
rw [const_apply, prod_apply, const_apply, const_apply]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ✝ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ✝ : MeasurableSpace γ✝
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel (α × β) γ
a : α
b : β
inst✝ : NeZero (κ (a, b))
⊢ NeZero ((κ.sectL b) a)

Tactic:
by
  rw [sectL_apply]; infer_instance

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α × β → ℝ≥0∞
hf : Measurable f
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
a : α
⊢ ∫⁻ (p : α × β), f p ∂(deterministic id ⋯ ×ₖ κ) a = ∫⁻ (b : β), f (a, b) ∂κ a

Tactic:
lintegral_deterministic_prod _ _ _ hf,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α × β → ℝ≥0∞
hf : Measurable f
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
a : α
⊢ ∫⁻ (c : β), f (id a, c) ∂κ a = ∫⁻ (b : β), f (a, b) ∂κ a
Module: Mathlib.Probability.Kernel.Composition.CompProd

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
hs : MeasurableSet s
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
⊢ ((κ ⊗ₖ η) a) s = ∫⁻ (b : β), (η (a, b)) (Prod.mk b ⁻¹' s) ∂κ a

Tactic:
rw [compProd, comp_apply, copy_apply, Measure.dirac_bind (by fun_prop), comp_apply,
    parallelComp_apply, Kernel.id_apply, Measure.bind_apply hs (by fun_prop),
    lintegral_prod _ (Kernel.measurable_coe _ hs).aemeasurable, lintegral_dirac']
  swap
  · suffices Measurable fun p : α × β ↦
      (swap γ β ∘ₖ (η ∥ₖ Kernel.id)
        ∘ₖ deterministic MeasurableEquiv.prodAssoc.symm (MeasurableEquiv.measurable _)
        ∘ₖ (Kernel.id ∥ₖ copy β)) p s by fun_prop
    exact Kernel.measurable_coe _ hs
  congr with b
  rw [comp_apply, parallelComp_apply, Kernel.id_apply, copy_apply, Measure.dirac_prod_dirac,
    Measure.dirac_bind (by fun_prop), comp_apply, deterministic_apply (by fun_prop),
    Measure.dirac_bind (by fun_prop), comp_apply]
  simp only [MeasurableEquiv.prodAssoc, MeasurableEquiv.symm_mk, MeasurableEquiv.coe_mk,
    Equiv.prodAssoc_symm_apply]
  rw [parallelComp_apply, Kernel.id_apply, Measure.bind_apply hs (by fun_prop),
    lintegral_prod _ (Kernel.measurable_coe _ hs).aemeasurable]
  classical
  have h_int x : ∫⁻ y, swap γ β (x, y) s ∂Measure.dirac b = (Prod.mk b ⁻¹' s).indicator 1 x := by
    rw [lintegral_dirac']
    · simp [swap_apply' _ hs, Set.indicator_apply]
    · simpa [swap_apply' _ hs, Prod.swap_prod_mk] using!
        measurable_const.indicator (measurable_prodMk_right hs)
  simp_rw [h_int]
  rw [lintegral_indicator_one]
  exact measurable_prodMk_left hs

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsMarkovKernel κ
η : Kernel α γ
inst✝ : IsSFiniteKernel η
⊢ (κ ×ₖ η).snd = η

Tactic:
ext x

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsMarkovKernel κ
η : Kernel α γ
inst✝ : IsSFiniteKernel η
x : α
s✝ : Set γ
a✝ : MeasurableSet s✝
⊢ ((κ ×ₖ η).snd x) s✝ = (η x) s✝
Module: Mathlib.Probability.Kernel.Composition.MeasureComp

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
inst✝¹ : SFinite μ
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
⊢ (μ ⊗ₘ κ).snd = ⇑κ ∘ₘ μ

Tactic:
ext s hs
  rw [bind_apply hs κ.aemeasurable, snd_apply hs, compProd_apply]
  · rfl
  · exact measurable_snd hs

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
f : β → γ → ℝ≥0∞
hf : Measurable (Function.uncurry f)
⊢ ∫⁻ (bc : β × γ), f bc.1 bc.2 ∂(κ ⊗ₖ η) a = ∫⁻ (b : β), ∫⁻ (c : γ), f b c ∂η (a, b) ∂κ a

Tactic:
let F : ℕ → SimpleFunc (β × γ) ℝ≥0∞ := SimpleFunc.eapprox (Function.uncurry f)

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
f : β → γ → ℝ≥0∞
hf : Measurable (Function.uncurry f)
F : ℕ → SimpleFunc (β × γ) ℝ≥0∞ := SimpleFunc.eapprox (Function.uncurry f)
⊢ ∫⁻ (bc : β × γ), f bc.1 bc.2 ∂(κ ⊗ₖ η) a = ∫⁻ (b : β), ∫⁻ (c : γ), f b c ∂η (a, b) ∂κ a
Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
s : Set (β × γ)
h2s : ((κ ⊗ₖ η) a) s ≠ ∞
t : Set (β × γ) := toMeasurable ((κ ⊗ₖ η) a) s
b : β
hb : (η (a, b)) (Prod.mk b ⁻¹' s) < ∞
⊢ ENNReal.ofReal ((η (a, b)) (Prod.mk b ⁻¹' s)).toReal ≤ (η (a, b)) (Prod.mk b ⁻¹' t)

Tactic:
rw [ofReal_toReal hb.ne]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
s : Set (β × γ)
h2s : ((κ ⊗ₖ η) a) s ≠ ∞
t : Set (β × γ) := toMeasurable ((κ ⊗ₖ η) a) s
b : β
hb : (η (a, b)) (Prod.mk b ⁻¹' s) < ∞
⊢ (η (a, b)) (Prod.mk b ⁻¹' s) ≤ (η (a, b)) (Prod.mk b ⁻¹' t)
Module: Mathlib.Probability.Kernel.Composition.CompProd

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
f : β → γ → ℝ≥0∞
hf : Measurable (Function.uncurry f)
⊢ ∫⁻ (bc : β × γ), f bc.1 bc.2 ∂(κ ⊗ₖ η) a = ∫⁻ (b : β), ∫⁻ (c : γ), f b c ∂η (a, b) ∂κ a

Tactic:
by
  let F : ℕ → SimpleFunc (β × γ) ℝ≥0∞ := SimpleFunc.eapprox (Function.uncurry f)
  have h : ∀ a, ⨆ n, F n a = Function.uncurry f a := SimpleFunc.iSup_eapprox_apply hf
  simp only [Prod.forall, Function.uncurry_apply_pair] at h
  simp_rw [← h]
  have h_mono : Monotone F := fun i j hij b =>
    SimpleFunc.monotone_eapprox (Function.uncurry f) hij _
  rw [lintegral_iSup (fun n => (F n).measurable) h_mono]
  have : ∀ b, ∫⁻ c, ⨆ n, F n (b, c) ∂η (a, b) = ⨆ n, ∫⁻ c, F n (b, c) ∂η (a, b) := by
    intro a
    rw [lintegral_iSup]
    · exact fun n => (F n).measurable.comp measurable_prodMk_left
    · exact fun i j hij b => h_mono hij _
  simp_rw [this]
  have h_some_meas_integral :
    ∀ f' : SimpleFunc (β × γ) ℝ≥0∞, Measurable fun b => ∫⁻ c, f' (b, c) ∂η (a, b) := by
    intro f'
    have :
      (fun b => ∫⁻ c, f' (b, c) ∂η (a, b)) =
        (fun ab => ∫⁻ c, f' (ab.2, c) ∂η ab) ∘ fun b => (a, b) := by
      ext1 ab; rfl
    rw [this]
    fun_prop
  rw [lintegral_iSup]
  rotate_left
  · exact fun n => h_some_meas_integral (F n)
  · exact fun i j hij b => lintegral_mono fun c => h_mono hij _
  congr
  ext1 n
  refine SimpleFunc.induction ?_ ?_ (F n)
  · intro c s hs
    simp +unfoldPartialApp only [SimpleFunc.const_zero,
      SimpleFunc.coe_piecewise, SimpleFunc.coe_const, SimpleFunc.coe_zero,
      Set.piecewise_eq_indicator, Function.const, lintegral_indicator_const hs]
    rw [compProd_apply hs, ← lintegral_const_mul c _]
    swap
    · exact (measurable_kernel_prodMk_left ((measurable_fst.snd.prodMk measurable_snd) hs)).comp
        measurable_prodMk_left
    congr
    ext1 b
    rw [lintegral_indicator_const_comp measurable_prodMk_left hs]
  · intro f f' _ hf_eq hf'_eq
    simp_rw [SimpleFunc.coe_add, Pi.add_apply]
    change
      ∫⁻ x, (f : β × γ → ℝ≥0∞) x + f' x ∂(κ ⊗ₖ η) a =
        ∫⁻ b, ∫⁻ c : γ, f (b, c) + f' (b, c) ∂η (a, b) ∂κ a
    rw [lintegral_add_left (SimpleFunc.measurable _), hf_eq, hf'_eq, ← lintegral_add_left]
    swap
    · exact h_some_meas_integral f
    congr with b
    rw [lintegral_add_left]
    exact (SimpleFunc.measurable _).comp measurable_prodMk_left

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

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

Tactic:
integral_exp_tilted f,

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

Goal state before:
pp: case inr
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hf : Integrable (fun x ↦ rexp (f x)) ν
h0 : NeZero ν
⊢ μ.rnDeriv (ν.tilted f) =ᵐ[ν] fun x ↦ ENNReal.ofReal (rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν) * μ.rnDeriv ν x

Tactic:
refine (Measure.rnDeriv_withDensity_right μ ν ?_ ?_ ?_).trans ?_

Goal state after:
case inr.refine_1
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hf : Integrable (fun x ↦ rexp (f x)) ν
h0 : NeZero ν
⊢ AEMeasurable (fun x ↦ ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂ν)) ν

case inr.refine_2
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hf : Integrable (fun x ↦ rexp (f x)) ν
h0 : NeZero ν
⊢ ∀ᵐ (x : α) ∂ν, ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂ν) ≠ 0

case inr.refine_3
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hf : Integrable (fun x ↦ rexp (f x)) ν
h0 : NeZero ν
⊢ ∀ᵐ (x : α) ∂ν, ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂ν) ≠ ∞

case inr.refine_4
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hf : Integrable (fun x ↦ rexp (f x)) ν
h0 : NeZero ν
⊢ (fun x ↦ (ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂ν))⁻¹ * μ.rnDeriv ν x) =ᵐ[ν] fun x ↦
    ENNReal.ofReal (rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν) * μ.rnDeriv ν x
Module: Mathlib.InformationTheory.KullbackLeibler.KLFun

Goal state before:
pp: ⊢ deriv klFun = log

Tactic:
ext x

Goal state after:
x : ℝ
⊢ deriv klFun x = log x
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Trim

Goal state before:
pp: α : Type u_1
ε : Type u_3
m m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
hm : m ≤ m0
f : α → ε
hf : StronglyMeasurable f
⊢ eLpNorm f p (μ.trim hm) = eLpNorm f p μ

Tactic:
by_cases h0 : p = 0
  · simp [h0]
  by_cases h_top : p = ∞
  · simpa only [h_top, eLpNorm_exponent_top] using eLpNormEssSup_trim hm hf
  simpa only [eLpNorm_eq_eLpNorm' h0 h_top] using eLpNorm'_trim hm hf

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
mα : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedSpace ℝ E
hp : Fact (1 ≤ p)
inst✝¹ : CompleteSpace ↥(Lp E p μ)
inst✝ : Nontrivial ↥(Lp E p μ)
f : ↥(Lp ℝ p μ)
hf : f ≠ 0
m : E →L[ℝ] ↥(Lp E p μ) := (compLpL₂ p μ (lsmul ℝ ℝ).flip).flip f
u : ℕ → E
hu : CauchySeq u
g : ↥(Lp E p μ)
hg : Tendsto (⇑m ∘ u) atTop (𝓝 g)
f' : ℕ → α → E := fun n ↦ ↑↑((⇑m ∘ u) n)
⊢ ∃ a, Tendsto u atTop (𝓝 a)

Tactic:
obtain ⟨ns, hns, nslim⟩ : ∃ ns : ℕ → ℕ, StrictMono ns ∧
      ∀ᵐ x ∂μ, Tendsto (fun i ↦ f' (ns i) x) atTop (𝓝 (g x)) :=
    (tendstoInMeasure_of_tendsto_Lp hg).exists_seq_tendsto_ae

Goal state after:
α : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
mα : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedSpace ℝ E
hp : Fact (1 ≤ p)
inst✝¹ : CompleteSpace ↥(Lp E p μ)
inst✝ : Nontrivial ↥(Lp E p μ)
f : ↥(Lp ℝ p μ)
hf : f ≠ 0
m : E →L[ℝ] ↥(Lp E p μ) := (compLpL₂ p μ (lsmul ℝ ℝ).flip).flip f
u : ℕ → E
hu : CauchySeq u
g : ↥(Lp E p μ)
hg : Tendsto (⇑m ∘ u) atTop (𝓝 g)
f' : ℕ → α → E := fun n ↦ ↑↑((⇑m ∘ u) n)
ns : ℕ → ℕ
hns : StrictMono ns
nslim : ∀ᵐ (x : α) ∂μ, Tendsto (fun i ↦ f' (ns i) x) atTop (𝓝 (↑↑g x))
⊢ ∃ a, Tendsto u atTop (𝓝 a)
Module: Mathlib.InformationTheory.KullbackLeibler.Basic

Goal state before:
pp: case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
c : ℝ≥0
hc : ¬c = 0
h_llr : llr (c • μ) ν =ᵐ[μ] fun x ↦ llr μ ν x + log ↑c
⊢ (klDiv (c • μ) ν).toReal = ↑c * (klDiv μ ν).toReal + (1 - ↑c) * ν.real univ + ↑c * log ↑c * μ.real univ

Tactic:
rw [toReal_klDiv hμν h_int, toReal_klDiv (hμν.smul_left c)]

Goal state after:
case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
c : ℝ≥0
hc : ¬c = 0
h_llr : llr (c • μ) ν =ᵐ[μ] fun x ↦ llr μ ν x + log ↑c
⊢ ∫ (a : α), llr (c • μ) ν a ∂c • μ + ν.real univ - (c • μ).real univ =
    ↑c * (∫ (a : α), llr μ ν a ∂μ + ν.real univ - μ.real univ) + (1 - ↑c) * ν.real univ + ↑c * log ↑c * μ.real univ

case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
c : ℝ≥0
hc : ¬c = 0
h_llr : llr (c • μ) ν =ᵐ[μ] fun x ↦ llr μ ν x + log ↑c
⊢ Integrable (llr (c • μ) ν) (c • μ)
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1

Goal state before:
pp: α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
⊢ condExpInd G hm μ ∅ = 0

Tactic:
ext x

Goal state after:
α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
x : G
⊢ ↑↑((condExpInd G hm μ ∅) x) =ᵐ[μ] ↑↑(0 x)
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 t : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
ht : MeasurableSet t
hμs : μ s ≠ ∞
hμt : μ t ≠ ∞
hst : Disjoint s t
⊢ condExpInd G hm μ (s ∪ t) = condExpInd G hm μ s + condExpInd G hm μ t

Tactic:
ext1 x; push_cast; exact condExpInd_disjoint_union_apply hs ht hμs hμt hst x

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

Goal state before:
pp: α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝² : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
inst✝¹ : Fact (1 ≤ p)
inst✝ : NormedSpace ℝ F
hm : m ≤ m0
hp_ne_top : p ≠ ∞
P : (α → F) → Prop
h_ind : ∀ (c : F) ⦃s : Set α⦄, MeasurableSet s → μ s < ∞ → P (s.indicator fun x ↦ c)
h_add :
  ∀ ⦃f g : α → F⦄,
    Disjoint (Function.support f) (Function.support g) →
      MemLp f p μ → MemLp g p μ → StronglyMeasurable f → StronglyMeasurable g → P f → P g → P (f + g)
h_closed : IsClosed {f | P ↑↑↑f}
h_ae : ∀ ⦃f g : α → F⦄, f =ᵐ[μ] g → MemLp f p μ → P f → P g
⊢ ∀ ⦃f : α → F⦄, MemLp f p μ → AEStronglyMeasurable f μ → P f

Tactic:
by
  intro f hf hfm
  let f_Lp := hf.toLp f
  have hfm_Lp : AEStronglyMeasurable[m] f_Lp μ := hfm.congr hf.coeFn_toLp.symm
  refine h_ae hf.coeFn_toLp (Lp.memLp _) ?_
  change P f_Lp
  refine Lp.induction_stronglyMeasurable hm hp_ne_top (fun f => P f) ?_ ?_ h_closed f_Lp hfm_Lp
  · intro c s hs hμs
    rw [Lp.simpleFunc.coe_indicatorConst]
    refine h_ae indicatorConstLp_coeFn.symm ?_ (h_ind c hs hμs)
    exact memLp_indicator_const p (hm s hs) c (Or.inr hμs.ne)
  · intro f g hf_mem hg_mem hfm hgm h_disj hfP hgP
    have hfP' : P f := h_ae hf_mem.coeFn_toLp (Lp.memLp _) hfP
    have hgP' : P g := h_ae hg_mem.coeFn_toLp (Lp.memLp _) hgP
    specialize h_add h_disj hf_mem hg_mem hfm hgm hfP' hgP'
    refine h_ae ?_ (hf_mem.add hg_mem) h_add
    exact (hf_mem.coeFn_toLp.symm.add hg_mem.coeFn_toLp.symm).trans (Lp.coeFn_add _ _).symm

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

Goal state before:
pp: α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hm : m ≤ m0
hs : MeasurableSet s
ht : MeasurableSet t
hμs : μ s ≠ ∞
hμt : μ t ≠ ∞
⊢ μ.real (t ∩ s) • 1 = μ.real (t ∩ s)

Tactic:
by rw [smul_eq_mul, mul_one]

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

Goal state before:
pp: 𝓧 : 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)
x : 𝓧
hx : 0 x ≤ f x
⊢ g x = ‖f x‖ₑ

Tactic:
by simp [g, Real.enorm_eq_ofReal hx]

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

Goal state before:
pp: case neg
Ω : 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:
simp_rw [condLExp_of_not_sigmaFinite hm hσ]; filter_upwards; simp

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

Goal state before:
pp: case neg
Ω : 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:
simp_rw [condLExp_of_not_sigmaFinite hm hσ]; filter_upwards; simp

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

Goal state before:
pp: case neg
Ω : Type u_1
mΩ₀ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
mΩ : MeasurableSpace Ω
inst✝ : Countable ι
X : ι → Ω → ℝ≥0∞
hX : ∀ (i : ι), AEMeasurable (X i) P
hm : mΩ ≤ mΩ₀
hσ : ¬SigmaFinite (P.trim hm)
⊢ P⁻[∑' (i : ι), X i | mΩ] =ᵐ[P] ∑' (i : ι), P⁻[X i | mΩ]

Tactic:
simp_rw [condLExp_of_not_sigmaFinite hm hσ]; filter_upwards; simp

Goal state after:
Module: Mathlib.Lean.Thunk

Goal state before:
pp: α : Type u
β : Type v
inst✝ : DecidableEq α
⊢ DecidableEq (Thunk α)

Tactic:
by
  intro a b
  have : a = b ↔ a.get = b.get := ⟨by intro x; rw [x], by intro; ext; assumption⟩
  rw [this]
  infer_instance

Goal state after:
Module: Mathlib.LinearAlgebra.Alternating.DomCoprod

Goal state before:
pp: case h
ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
a : Mᵢ [⋀^ιa]→ₗ[R'] N₁
b : Mᵢ [⋀^ιb]→ₗ[R'] N₂
v : ιa ⊕ ιb → Mᵢ
i j : ιa ⊕ ιb
hv : v i = v j
hij : i ≠ j
a✝ : Perm (ιa ⊕ ιb)
⊢ (summand a b (Quotient.mk'' a✝)) v + (summand a b (swap i j • Quotient.mk'' a✝)) v = 0

Tactic:
dsimp only [Quotient.liftOn'_mk'', Quotient.map'_mk'', MulAction.Quotient.smul_mk,
    domCoprod.summand]

Goal state after:
case h
ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
a : Mᵢ [⋀^ιa]→ₗ[R'] N₁
b : Mᵢ [⋀^ιb]→ₗ[R'] N₂
v : ιa ⊕ ιb → Mᵢ
i j : ιa ⊕ ιb
hv : v i = v j
hij : i ≠ j
a✝ : Perm (ιa ⊕ ιb)
⊢ (Perm.sign a✝ • MultilinearMap.domDomCongr a✝ ((↑a).domCoprod ↑b)) v +
      (Perm.sign (swap i j • a✝) • MultilinearMap.domDomCongr (swap i j • a✝) ((↑a).domCoprod ↑b)) v =
    0