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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η η' : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : IsSFiniteKernel η'
h : ∀ (a : α), ∀ᵐ (b : β) ∂κ a, η (a, b) = η' (a, b)
hκ : IsSFiniteKernel κ
a : α
s : Set (β × γ)
hs : MeasurableSet s
⊢ ((κ ⊗ₖ η) a) s = ((κ ⊗ₖ η') a) s

Tactic:
rw [compProd_apply hs, compProd_apply hs]

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η η' : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : IsSFiniteKernel η'
h : ∀ (a : α), ∀ᵐ (b : β) ∂κ a, η (a, b) = η' (a, b)
hκ : IsSFiniteKernel κ
a : α
s : Set (β × γ)
hs : MeasurableSet s
⊢ ∫⁻ (b : β), (η (a, b)) (Prod.mk b ⁻¹' s) ∂κ a = ∫⁻ (b : β), (η' (a, b)) (Prod.mk b ⁻¹' s) ∂κ a
Module: Mathlib.Probability.Kernel.Composition.KernelLemmas

Goal state before:
pp: case pos
X : Type u_1
Y : Type u_2
Z : Type u_3
T : Type u_4
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
mT : MeasurableSpace T
κ : Kernel X Y
η : Kernel Z T
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
ac : X × Z
s : Set (T × Y)
hs : MeasurableSet s
⊢ ∫⁻ (a : Y × T), (Measure.dirac a.swap) s ∂(κ ac.1).prod (η ac.2) = ((η ∥ₖ κ) ac.swap) s

Tactic:
parallelComp_apply' hs,

Goal state after:
case pos
X : Type u_1
Y : Type u_2
Z : Type u_3
T : Type u_4
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
mT : MeasurableSpace T
κ : Kernel X Y
η : Kernel Z T
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
ac : X × Z
s : Set (T × Y)
hs : MeasurableSet s
⊢ ∫⁻ (a : Y × T), (Measure.dirac a.swap) s ∂(κ ac.1).prod (η ac.2) =
    ∫⁻ (b : T), (κ ac.swap.2) (Prod.mk b ⁻¹' s) ∂η ac.swap.1
Module: Mathlib.Probability.Kernel.Composition.KernelLemmas

Goal state before:
pp: case pos.e_f.e_f
X : Type u_1
Y : Type u_2
Z : Type u_3
T : Type u_4
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
mT : MeasurableSpace T
κ : Kernel X Y
X' : Type u_5
mX' : MeasurableSpace X'
η : Kernel X' Z
inst✝¹ : IsSFiniteKernel η
ξ : Kernel Z T
inst✝ : IsSFiniteKernel ξ
hκ : IsSFiniteKernel κ
a : X × X'
s : Set (Y × T)
hs : MeasurableSet s
x : Y
y : Z
⊢ ((Kernel.id ∥ₖ ξ) (x, y)) s = (ξ y) (Prod.mk x ⁻¹' s)

Tactic:
parallelComp_apply' hs,

Goal state after:
case pos.e_f.e_f
X : Type u_1
Y : Type u_2
Z : Type u_3
T : Type u_4
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
mT : MeasurableSpace T
κ : Kernel X Y
X' : Type u_5
mX' : MeasurableSpace X'
η : Kernel X' Z
inst✝¹ : IsSFiniteKernel η
ξ : Kernel Z T
inst✝ : IsSFiniteKernel ξ
hκ : IsSFiniteKernel κ
a : X × X'
s : Set (Y × T)
hs : MeasurableSet s
x : Y
y : Z
⊢ ∫⁻ (b : Y), (ξ (x, y).2) (Prod.mk b ⁻¹' s) ∂Kernel.id (x, y).1 = (ξ y) (Prod.mk x ⁻¹' s)
Module: Mathlib.Probability.Kernel.Composition.KernelLemmas

Goal state before:

Tactic:
ξ ∥ₖ Kernel.id ∘ₖ (η ∥ₖ κ)
    _ = swap Y T ∘ₖ (swap T Y ∘ₖ (ξ ∥ₖ Kernel.id) ∘ₖ (η ∥ₖ κ)) := by
      simp_rw [← comp_assoc, swap_swap, id_comp]
    _ = swap Y T ∘ₖ (swap T Y ∘ₖ ((ξ ∘ₖ η) ∥ₖ κ)) := by rw [this]
    _ = ξ ∘ₖ η ∥ₖ κ := by simp_rw [← comp_assoc, swap_swap, id_comp]

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)
F : ℕ → SimpleFunc (β × γ) ℝ≥0∞ := SimpleFunc.eapprox (Function.uncurry f)
⊢ ∫⁻ (bc : β × γ), f bc.1 bc.2 ∂(κ ⊗ₖ η) a = ∫⁻ (b : β), ∫⁻ (c : γ), f b c ∂η (a, b) ∂κ a

Tactic:
have h : ∀ a, ⨆ n, F n a = Function.uncurry f a := SimpleFunc.iSup_eapprox_apply hf

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)
h : ∀ (a : β × γ), ⨆ n, (F n) a = Function.uncurry f a
⊢ ∫⁻ (bc : β × γ), f bc.1 bc.2 ∂(κ ⊗ₖ η) a = ∫⁻ (b : β), ∫⁻ (c : γ), f b c ∂η (a, b) ∂κ a
Module: Mathlib.Probability.Kernel.Composition.MeasureComp

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
⊢ ⇑(κ + η) ∘ₘ μ = ⇑κ ∘ₘ μ + ⇑η ∘ₘ μ

Tactic:
simp_rw [comp_eq_comp_const_apply, Kernel.comp_add_left, _root_.add_apply]

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

Goal state before:
pp: α : 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 η
f : β × γ → E
h1f : AEStronglyMeasurable f ((κ ⊗ₖ η) a)
⊢ HasFiniteIntegral f ((κ ⊗ₖ η) a) ↔
    (∀ᵐ (x : β) ∂κ a, HasFiniteIntegral (fun y ↦ f (x, y)) (η (a, x))) ∧
      HasFiniteIntegral (fun x ↦ ∫ (y : γ), ‖f (x, y)‖ ∂η (a, x)) (κ a)

Tactic:
rw [hasFiniteIntegral_congr h1f.ae_eq_mk,
    hasFiniteIntegral_compProd_iff h1f.stronglyMeasurable_mk]
  apply and_congr
  · apply eventually_congr
    filter_upwards [ae_ae_of_ae_compProd h1f.ae_eq_mk.symm] with x hx using
      hasFiniteIntegral_congr hx
  · apply hasFiniteIntegral_congr
    filter_upwards [ae_ae_of_ae_compProd h1f.ae_eq_mk.symm] with _ hx using
      integral_congr_ae (EventuallyEq.fun_comp hx _)

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

Goal state before:
pp: α : 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
E' : Type u_5
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace ℝ E'
f g : β × γ → E
F : E → E'
hf : Integrable f ((κ ⊗ₖ η) a)
hg : Integrable g ((κ ⊗ₖ η) a)
⊢ ∫ (x : β), F (∫ (y : γ), f (x, y) - g (x, y) ∂η (a, x)) ∂κ a =
    ∫ (x : β), F (∫ (y : γ), f (x, y) ∂η (a, x) - ∫ (y : γ), g (x, y) ∂η (a, x)) ∂κ a

Tactic:
by
  refine integral_congr_ae ?_
  filter_upwards [hf.ae_of_compProd, hg.ae_of_compProd] with _ h2f h2g
  simp [integral_sub h2f h2g]

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

Goal state before:
pp: case refine_4
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ≪ ν
κ : Kernel α β
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsFiniteMeasure ν
inst✝ : IsFiniteKernel κ
s : Set (α × β)
hs : MeasurableSet s
x✝ : (ν ⊗ₘ κ) s < ∞
h_key :
  ∀ (t₁ : Set α) (t₂ : Set β),
    MeasurableSet t₁ →
      MeasurableSet t₂ →
        ∫⁻ (x : α × β) in t₁ ×ˢ t₂, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ =
          ∫⁻ (x : α × β) in t₁ ×ˢ t₂, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
⊢ ∀ (f : ℕ → Set (α × β)),
    Pairwise (Function.onFun Disjoint f) →
      (∀ (i : ℕ), MeasurableSet (f i)) →
        (∀ (i : ℕ),
            ∫⁻ (x : α × β) in f i, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ =
              ∫⁻ (x : α × β) in f i, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ) →
          ∫⁻ (x : α × β) in ⋃ i, f i, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ =
            ∫⁻ (x : α × β) in ⋃ i, f i, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ

Tactic:
intro f' hf_disj hf_meas hf_eq

Goal state after:
case refine_4
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ≪ ν
κ : Kernel α β
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsFiniteMeasure ν
inst✝ : IsFiniteKernel κ
s : Set (α × β)
hs : MeasurableSet s
x✝ : (ν ⊗ₘ κ) s < ∞
h_key :
  ∀ (t₁ : Set α) (t₂ : Set β),
    MeasurableSet t₁ →
      MeasurableSet t₂ →
        ∫⁻ (x : α × β) in t₁ ×ˢ t₂, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ =
          ∫⁻ (x : α × β) in t₁ ×ˢ t₂, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
f' : ℕ → Set (α × β)
hf_disj : Pairwise (Function.onFun Disjoint f')
hf_meas : ∀ (i : ℕ), MeasurableSet (f' i)
hf_eq :
  ∀ (i : ℕ),
    ∫⁻ (x : α × β) in f' i, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ = ∫⁻ (x : α × β) in f' i, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
⊢ ∫⁻ (x : α × β) in ⋃ i, f' i, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ =
    ∫⁻ (x : α × β) in ⋃ i, f' i, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
Module: Mathlib.MeasureTheory.Measure.Tilted

Goal state before:
pp: case e_f
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
x : α
⊢ ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) = ↑(NNReal.mk (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) ⋯)

Tactic:
rw [ENNReal.ofReal_eq_coe_nnreal]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv

Goal state before:
pp: case neg
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
f : ℝ → ℝ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (fun x ↦ f (μ.rnDeriv ν x).toReal) ν
hμν : μ ≪ ν
hν : ¬ν = 0
this✝ : NeZero ν
μ' : Measure 𝓧 := (ν univ)⁻¹ • μ
ν' : Measure 𝓧 := (ν univ)⁻¹ • ν
this : IsFiniteMeasure μ'
hμν' : μ' ≪ ν'
⊢ ν.real univ * f (μ.real univ / ν.real univ) ≤ ∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν

Tactic:
have h_rnDeriv_eq : μ'.rnDeriv ν' =ᵐ[ν] μ.rnDeriv ν := by
    have h1' : μ'.rnDeriv ν' =ᵐ[ν'] (ν univ)⁻¹ • μ.rnDeriv ν' :=
      Measure.rnDeriv_smul_left_of_ne_top' (μ := ν') (ν := μ) (by simp [hν])
    have h1 : μ'.rnDeriv ν' =ᵐ[ν] (ν univ)⁻¹ • μ.rnDeriv ν' := by
      rwa [Measure.ae_ennreal_smul_measure_eq] at h1'
      simp
    have h2 : μ.rnDeriv ν' =ᵐ[ν] (ν univ)⁻¹⁻¹ • μ.rnDeriv ν :=
      Measure.rnDeriv_smul_right_of_ne_top' (μ := ν) (ν := μ) (by simp) (by simp [hν])
    filter_upwards [h1, h2] with x h1 h2
    rw [h1, Pi.smul_apply, smul_eq_mul, h2]
    simp only [inv_inv, Pi.smul_apply, smul_eq_mul]
    rw [← mul_assoc, ENNReal.inv_mul_cancel, one_mul]
    · simp [hν]
    · simp

Goal state after:
case neg
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
f : ℝ → ℝ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (fun x ↦ f (μ.rnDeriv ν x).toReal) ν
hμν : μ ≪ ν
hν : ¬ν = 0
this✝ : NeZero ν
μ' : Measure 𝓧 := (ν univ)⁻¹ • μ
ν' : Measure 𝓧 := (ν univ)⁻¹ • ν
this : IsFiniteMeasure μ'
hμν' : μ' ≪ ν'
h_rnDeriv_eq : μ'.rnDeriv ν' =ᵐ[ν] μ.rnDeriv ν
⊢ ν.real univ * f (μ.real univ / ν.real univ) ≤ ∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν
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 α β
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
⊢ κ ⊗ₖ η = Kernel.sum fun n ↦ κ ⊗ₖ η.seq n

Tactic:
by
  simp_rw [compProd_def]
  rw [← comp_sum_left, ← comp_sum_left, ← comp_sum_left, ← comp_sum_left, ← comp_sum_right,
    ← parallelComp_sum_left, kernel_sum_seq]

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

Goal state before:
pp: case h0
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst✝ : NeZero μ
hf : Integrable (fun x ↦ rexp (f x)) μ
⊢ ENNReal.ofReal (∫ (x : α), rexp (f x) ∂μ) ≠ 0

Tactic:
simp only [ne_eq, ENNReal.ofReal_eq_zero, not_le]
    exact integral_exp_pos hf

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
a : α
ha : μ.rnDeriv μ a = 1
⊢ llr μ μ a = 0 a

Tactic:
simp [llr, ha]

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

Goal state before:
pp: α : 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
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun f ↦ ∫ (x : β), ∫ (y : γ), ↑↑f y ∂η x ∂κ a

Tactic:
by
  refine continuous_iff_continuousAt.2 fun g ↦ ?_
  refine tendsto_integral_of_L1 _ (L1.integrable_coeFn g).integral_comp.aestronglyMeasurable
      (Eventually.of_forall fun h ↦ (L1.integrable_coeFn h).integral_comp) ?_
  simp_rw [← lintegral_fn_integral_sub_comp (‖·‖ₑ) (L1.integrable_coeFn _) (L1.integrable_coeFn g)]
  refine tendsto_of_tendsto_of_tendsto_of_le_of_le
    (h := fun i ↦ ∫⁻ x, ∫⁻ y, ‖i y - g y‖ₑ ∂η x ∂κ a)
    tendsto_const_nhds ?_ (fun _ ↦ zero_le) ?_
  swap; · exact fun _ ↦ lintegral_mono fun _ ↦ enorm_integral_le_lintegral_enorm _
  have (i : γ →₁[(η ∘ₖ κ) a] E) : Measurable fun z ↦ ‖i z - g z‖ₑ :=
    ((Lp.stronglyMeasurable i).sub (Lp.stronglyMeasurable g)).enorm
  simp_rw [← lintegral_comp _ _ _ (this _), ← L1.ofReal_norm_sub_eq_lintegral, ← ofReal_zero]
  exact (continuous_ofReal.tendsto 0).comp (tendsto_iff_norm_sub_tendsto_zero.1 tendsto_id)

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst✝¹ : IsProbabilityMeasure μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable f μ
h_int : Integrable (llr μ ν) μ
hfμ : Integrable (fun x ↦ rexp (f x)) μ
hfν : AEMeasurable f ν
⊢ ∫ (x : α), f x ∂μ - log (∫ (x : α), rexp (f x) ∂μ) + ∫ (x : α), llr μ ν x ∂μ =
    ∫ (x : α), llr μ ν x ∂μ + ∫ (x : α), f x ∂μ - log (∫ (x : α), rexp (f x) ∂μ)

Tactic:
by abel

Goal state after:
Module: Mathlib.InformationTheory.KullbackLeibler.Basic

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : μ ≪ ν ∧ Integrable (llr μ ν) μ
⊢ ENNReal.ofReal (∫ (x : α), llr μ ν x ∂μ + ν.real univ - μ.real univ) =
    ENNReal.ofReal (∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν)

Tactic:
integral_klFun_rnDeriv h.1 h.2

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : μ ≪ ν ∧ Integrable (llr μ ν) μ
⊢ ENNReal.ofReal (∫ (x : α), llr μ ν x ∂μ + ν.real univ - μ.real univ) =
    ENNReal.ofReal (∫ (x : α), llr μ ν x ∂μ + ν.real univ - μ.real univ)
Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst✝¹ : IsProbabilityMeasure μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hfμ : Integrable f μ
hfν : Integrable (fun x ↦ rexp (f x)) ν
h_int : Integrable (llr μ ν) μ
⊢ -∫ (x : α), f x ∂μ + log (∫ (x : α), rexp (f x) ∂ν) + ∫ (x : α), llr μ ν x ∂μ =
    ∫ (x : α), llr μ ν x ∂μ - ∫ (x : α), f x ∂μ + log (∫ (x : α), rexp (f x) ∂ν)

Tactic:
by abel

Goal state after:
Module: Mathlib.InformationTheory.KullbackLeibler.Basic

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
⊢ ∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν = (klDiv μ ν).toReal

Tactic:
by rw [toReal_klDiv_eq_integral_klFun hμν]

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

Goal state before:
pp: case refine_1
α : Type u_1
E' : Type u_3
𝕜 : Type u_7
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace 𝕜 E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f : ↥(Lp E' 2 μ)
hs : MeasurableSet s
hμs : μ s ≠ ∞
⊢ Integrable (↑↑↑((condExpL2 E' 𝕜 hm) f) - ↑↑f) (μ.restrict s)

Tactic:
rw [integrable_congr (ae_restrict_of_ae (Lp.coeFn_sub (↑(condExpL2 E' 𝕜 hm f)) f).symm)]
    exact integrableOn_Lp_of_measure_ne_top _ fact_one_le_two_ennreal.elim hμs

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

Goal state before:
pp: α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
F : Type u_5
inst✝³ : NormedAddCommGroup F
inst✝² : CompleteSpace F
inst✝¹ : NormedSpace ℝ F
inst✝ : IsFiniteMeasure μ
hm : m ≤ m₀
hf_int : Integrable f μ
T : E →L[ℝ] F
a : F
hp : (fun x ↦ T (μ[f | m] x) + a) =ᵐ[μ] μ[⇑T ∘ f | m] + μ[fun y ↦ a | m]
⊢ (fun x ↦ T (μ[f | m] x) + a) =ᵐ[μ] μ[fun y ↦ T (f y) + a | m]

Tactic:
exact hp.trans (condExp_add (T.integrable_comp hf_int) (integrable_const a) m).symm

Goal state after:
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
⊢ μ[s.indicator f | m] =ᵐ[μ] s.indicator μ[f | m]

Tactic:
by
  by_cases hm : m ≤ m0
  swap; · simp_rw [condExp_of_not_le hm, Set.indicator_zero']; rfl
  by_cases hμm : SigmaFinite (μ.trim hm)
  swap; · simp_rw [condExp_of_not_sigmaFinite hm hμm, Set.indicator_zero']; rfl
  have : SigmaFinite (μ.trim hm) := hμm
  -- use `have` to perform what should be the first calc step because of an error I don't
  -- understand
  have : s.indicator (μ[f | m]) =ᵐ[μ] s.indicator (μ[s.indicator f + sᶜ.indicator f | m]) := by
    rw [Set.indicator_self_add_compl s f]
  refine (this.trans ?_).symm
  calc
    s.indicator (μ[s.indicator f + sᶜ.indicator f | m]) =ᵐ[μ]
        s.indicator (μ[s.indicator f | m] + μ[sᶜ.indicator f | m]) := by
      filter_upwards [condExp_add (hf_int.indicator (hm _ hs)) (hf_int.indicator (hm _ hs.compl)) m]
        with x hx
      classical rw [Set.indicator_apply, Set.indicator_apply, hx]
    _ = s.indicator (μ[s.indicator f | m]) + s.indicator (μ[sᶜ.indicator f | m]) :=
      (s.indicator_add' _ _)
    _ =ᵐ[μ] s.indicator (μ[s.indicator f | m]) +
        s.indicator (sᶜ.indicator (μ[sᶜ.indicator f | m])) := 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]
    _ =ᵐ[μ] s.indicator (μ[s.indicator f | m]) := by
      rw [Set.indicator_indicator, Set.inter_compl_self, Set.indicator_empty', add_zero]
    _ =ᵐ[μ] μ[s.indicator f | m] := by
      refine (condExp_indicator_aux hs ?_).symm.trans ?_
      · exact indicator_ae_eq_restrict_compl (hm _ hs)
      · rw [Set.indicator_indicator, Set.inter_self]

Goal state after:
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)
⊢ μ[f | m] =ᵐ[μ.restrict s] μ[f | m₂]

Tactic:
by
  rw [ae_eq_restrict_iff_indicator_ae_eq (hm _ hs_m)]
  have hs_m₂ : MeasurableSet[m₂] s := by rwa [← Set.inter_univ s, ← hs Set.univ, Set.inter_univ]
  by_cases hf_int : Integrable f μ
  swap; · simp_rw [condExp_of_not_integrable hf_int]; rfl
  refine ((condExp_indicator hf_int hs_m).symm.trans ?_).trans (condExp_indicator hf_int hs_m₂)
  refine ae_eq_of_forall_setIntegral_eq_of_sigmaFinite' hm₂
    (fun s _ _ => integrable_condExp.integrableOn)
    (fun s _ _ => integrable_condExp.integrableOn) ?_ ?_
    stronglyMeasurable_condExp.aestronglyMeasurable
  swap
  · have : StronglyMeasurable[m] (μ[s.indicator f | m]) := stronglyMeasurable_condExp
    refine this.aestronglyMeasurable.of_measurableSpace_le_on hm hs_m (fun t => (hs t).mp) ?_
    exact condExp_ae_eq_restrict_zero hs_m.compl (indicator_ae_eq_restrict_compl (hm _ hs_m))
  intro t ht _
  have : ∫ x in t, (μ[s.indicator f | m]) x ∂μ = ∫ x in s ∩ t, (μ[s.indicator f | m]) x ∂μ := by
    rw [← integral_add_compl (hm _ hs_m) integrable_condExp.integrableOn]
    suffices ∫ x in sᶜ, (μ[s.indicator f | m]) x ∂μ.restrict t = 0 by
      rw [this, add_zero, Measure.restrict_restrict (hm _ hs_m)]
    rw [Measure.restrict_restrict (MeasurableSet.compl (hm _ hs_m))]
    suffices μ[s.indicator f | m] =ᵐ[μ.restrict sᶜ] 0 by
      rw [Set.inter_comm, ← Measure.restrict_restrict (hm₂ _ ht)]
      calc
        ∫ x : α in t, (μ[s.indicator f | m]) x ∂μ.restrict sᶜ =
            ∫ x : α in t, 0 ∂μ.restrict sᶜ := by
          refine setIntegral_congr_ae (hm₂ _ ht) ?_
          filter_upwards [this] with x hx _ using hx
        _ = 0 := integral_zero _ _
    refine condExp_ae_eq_restrict_zero hs_m.compl ?_
    exact indicator_ae_eq_restrict_compl (hm _ hs_m)
  have hst_m : MeasurableSet[m] (s ∩ t) := (hs _).mpr (hs_m₂.inter ht)
  simp_rw [this, setIntegral_condExp hm₂ (hf_int.indicator (hm _ hs_m)) ht,
    setIntegral_condExp hm (hf_int.indicator (hm _ hs_m)) hst_m, integral_indicator (hm _ hs_m),
    Measure.restrict_restrict (hm _ hs_m), ← Set.inter_assoc, Set.inter_self]

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

Goal state before:
pp: 𝓧 : 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 ν
⊢ (fun a ↦ (Measure.map g μ).rnDeriv (Measure.map g ν) (g a)) =ᵐ[ν] ν⁻[μ.rnDeriv ν | MeasurableSpace.comap g m𝓨]

Tactic:
have h_ne_top1 : ∀ᵐ x ∂ν, (μ.map g).rnDeriv (ν.map g) (g x) ≠ ∞ :=
    ae_of_ae_map hg.aemeasurable (Measure.rnDeriv_ne_top (μ.map g) (ν.map g))

Goal state after:
𝓧 : 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 ν
h_ne_top1 : ∀ᵐ (x : 𝓧) ∂ν, (Measure.map g μ).rnDeriv (Measure.map g ν) (g x) ≠ ∞
⊢ (fun a ↦ (Measure.map g μ).rnDeriv (Measure.map g ν) (g a)) =ᵐ[ν] ν⁻[μ.rnDeriv ν | MeasurableSpace.comap g m𝓨]
Module: Mathlib.LinearAlgebra.FixedSubmodule

Goal state before:
pp: case refine_1
R : Type u_1
inst✝² : Semiring R
V : Type u_3
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
e : V ≃ₗ[R] V
W : Submodule R V
v : V
he : ∀ y ∈ W, e y = y
x✝ : v ∈ map (↑e) W
w : V
hv : w ∈ ↑W
hv' : ↑e w = v
⊢ v ∈ W

Tactic:
simp only [SetLike.mem_coe, coe_coe] at hv hv'
    rwa [← hv', he w hv]

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

Goal state before:
pp: case h
V : Type u_2
inst✝² : AddCommGroup V
K : Type u_3
inst✝¹ : DivisionRing K
inst✝ : Module K V
e : V ≃ₗ[K] V
u : V →ₗ[K] V := ↑e - LinearMap.id
hu : u + LinearMap.id = ↑e
hr : 1 ≤ Module.rank K ↥u.range
b : Basis Unit K ↥u.range
x : V
⊢ (LinearMap.id + u) x = x + (b.coord default ∘ₗ u.rangeRestrict) x • ↑(b default)

Tactic:
suffices u x = b.repr (u.rangeRestrict x) default • b default by
      simp [this]

Goal state after:
case h
V : Type u_2
inst✝² : AddCommGroup V
K : Type u_3
inst✝¹ : DivisionRing K
inst✝ : Module K V
e : V ≃ₗ[K] V
u : V →ₗ[K] V := ↑e - LinearMap.id
hu : u + LinearMap.id = ↑e
hr : 1 ≤ Module.rank K ↥u.range
b : Basis Unit K ↥u.range
x : V
⊢ u x = (b.repr (u.rangeRestrict x)) default • ↑(b default)
Module: Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X Y Z : QuadraticModuleCat R
i : X ≅ Y
x : ↑X.toModuleCat
⊢ (QuadraticModuleCat.Hom.toIsometry i.inv) ((QuadraticModuleCat.Hom.toIsometry i.hom) x) = x

Tactic:
by
    change (i.hom ≫ i.inv).toIsometry x = x
    simp

Goal state after:
Module: Mathlib.LinearAlgebra.QuadraticForm.TensorProduct

Goal state before:
pp: R : Type uR
A : Type uA
M₂ : Type uM₂
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : AddCommGroup M₂
inst✝³ : Algebra R A
inst✝² : Module R M₂
inst✝¹ : Invertible 2
inst✝ : Invertible 2
Q : QuadraticForm R M₂
⊢ associated (QuadraticForm.baseChange A Q) = BilinForm.baseChange A (associated Q)

Tactic:
dsimp only [QuadraticForm.baseChange, LinearMap.baseChange]
  rw [associated_tmul (QuadraticMap.sq (R := A)) Q, associated_sq]
  exact rfl

Goal state after: