mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
c : ℝ≥0∞
hc : c ≠ 0
hc_ne_top : c ≠ ∞
⊢ llr (c • μ) ν =ᵐ[μ] fun x ↦ llr μ ν x + log c.toReal

Tactic:
simp only [llr, llr_def]
  have h := Measure.rnDeriv_smul_left_of_ne_top μ ν hc_ne_top
  filter_upwards [hμν.ae_le h, Measure.rnDeriv_pos hμν, hμν.ae_le (Measure.rnDeriv_lt_top μ ν)]
    with x hx_eq hx_pos hx_ne_top
  rw [hx_eq]
  simp only [Pi.smul_apply, smul_eq_mul, ENNReal.toReal_mul]
  rw [log_mul]
  rotate_left
  · rw [ENNReal.toReal_ne_zero]
    simp [hc, hc_ne_top]
  · rw [ENNReal.toReal_ne_zero]
    simp [hx_pos.ne', hx_ne_top.ne]
  ring

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
f✝ : γ → E
hE : CompleteSpace E
f g : γ → E
hfg : f =ᵐ[(η ∘ₖ κ) a] g
hf : ∫ (z : γ), f z ∂(η ∘ₖ κ) a = ∫ (x : β), ∫ (y : γ), f y ∂η x ∂κ a
x : β
⊢ (∀ᵐ (z : γ) ∂η x, f z = g z) → ∫ (y : γ), g y ∂η x = ∫ (y : γ), f y ∂η x

Tactic:
hfgx

Goal state after:
α : 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
hfg : f =ᵐ[(η ∘ₖ κ) a] g
hf : ∫ (z : γ), f z ∂(η ∘ₖ κ) a = ∫ (x : β), ∫ (y : γ), f y ∂η x ∂κ a
x : β
hfgx : ∀ᵐ (z : γ) ∂η x, f z = g z
⊢ ∫ (y : γ), g y ∂η x = ∫ (y : γ), f y ∂η x
Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd

Goal state before:
pp: α : Type u_5
β : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ : Measure α
inst✝³ : SFinite μ
inst✝² : IsSFiniteKernel κ
E : Type u_8
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set α
hs : MeasurableSet s
t : Set β
ht : MeasurableSet t
f : α × β → E
hf : IntegrableOn f (s ×ˢ t) (μ ⊗ₘ κ)
⊢ ∫ (x : α × β) in s ×ˢ t, f x ∂(Kernel.const Unit μ ⊗ₖ prodMkLeft Unit κ) () =
    ∫ (a : α) in s, ∫ (b : β) in t, f (a, b) ∂κ a ∂μ

Tactic:
ProbabilityTheory.setIntegral_compProd hs ht hf

Goal state after:
α : Type u_5
β : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ : Measure α
inst✝³ : SFinite μ
inst✝² : IsSFiniteKernel κ
E : Type u_8
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set α
hs : MeasurableSet s
t : Set β
ht : MeasurableSet t
f : α × β → E
hf : IntegrableOn f (s ×ˢ t) (μ ⊗ₘ κ)
⊢ ∫ (x : α) in s, ∫ (y : β) in t, f (x, y) ∂(prodMkLeft Unit κ) ((), x) ∂(Kernel.const Unit μ) () =
    ∫ (a : α) in s, ∫ (b : β) in t, f (a, b) ∂κ a ∂μ
Module: Mathlib.InformationTheory.KullbackLeibler.KLFun

Goal state before:
pp: x : ℝ
hx : x ≠ 0
⊢ HasDerivAt klFun (log x) x

Tactic:
by
  convert! ((hasDerivAt_mul_log hx).add (hasDerivAt_const x 1)).sub (hasDerivAt_id x) using 1
  ring

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
h : llr μ μ =ᵐ[μ] 0
⊢ klDiv μ μ = 0

Tactic:
klDiv_def,

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
h : llr μ μ =ᵐ[μ] 0
⊢ (if μ ≪ μ ∧ Integrable (llr μ μ) μ then ENNReal.ofReal (∫ (x : α), llr μ μ x ∂μ + μ.real univ - μ.real univ) else ∞) =
    0
Module: Mathlib.InformationTheory.KullbackLeibler.KLFun

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

Tactic:
exact integral_rnDeriv_smul hμν

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
c : ℝ≥0
hc : c ≠ 0
hc' : ↑c ≠ 0
hμ_smul : μ = c • c⁻¹ • μ
⊢ ν = c⁻¹ • c • ν

Tactic:
rw [smul_smul, inv_mul_cancel₀ hc, one_smul]

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

Goal state before:
pp: α : Type u_1
F' : Type u_3
m m0 : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
f g : α → F'
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hg_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn g s μ
hfg_eq : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ
hfm : AEStronglyMeasurable f μ
hgm : AEStronglyMeasurable g μ
⊢ f =ᵐ[μ] g

Tactic:
by
  rw [← ae_eq_trim_iff_of_aestronglyMeasurable hm hfm hgm]
  have hf_mk_int_finite (s) :
      MeasurableSet[m] s → μ.trim hm s < ∞ → @IntegrableOn _ _ m _ _ (hfm.mk f) s (μ.trim hm) := by
    intro hs hμs
    rw [trim_measurableSet_eq hm hs] at hμs
    rw [IntegrableOn, restrict_trim hm _ hs]
    refine Integrable.trim hm ?_ hfm.stronglyMeasurable_mk
    exact Integrable.congr (hf_int_finite s hs hμs) (ae_restrict_of_ae hfm.ae_eq_mk)
  have hg_mk_int_finite (s) :
      MeasurableSet[m] s → μ.trim hm s < ∞ → @IntegrableOn _ _ m _ _ (hgm.mk g) s (μ.trim hm) := by
    intro hs hμs
    rw [trim_measurableSet_eq hm hs] at hμs
    rw [IntegrableOn, restrict_trim hm _ hs]
    refine Integrable.trim hm ?_ hgm.stronglyMeasurable_mk
    exact Integrable.congr (hg_int_finite s hs hμs) (ae_restrict_of_ae hgm.ae_eq_mk)
  have hfg_mk_eq :
    ∀ s : Set α,
      MeasurableSet[m] s →
        μ.trim hm s < ∞ → ∫ x in s, hfm.mk f x ∂μ.trim hm = ∫ x in s, hgm.mk g x ∂μ.trim hm := by
    intro s hs hμs
    rw [trim_measurableSet_eq hm hs] at hμs
    rw [restrict_trim hm _ hs, ← integral_trim hm hfm.stronglyMeasurable_mk, ←
      integral_trim hm hgm.stronglyMeasurable_mk,
      integral_congr_ae (ae_restrict_of_ae hfm.ae_eq_mk.symm),
      integral_congr_ae (ae_restrict_of_ae hgm.ae_eq_mk.symm)]
    exact hfg_eq s hs hμs
  exact ae_eq_of_forall_setIntegral_eq_of_sigmaFinite hf_mk_int_finite hg_mk_int_finite hfg_mk_eq

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ✝ ν : Measure α
inst✝¹ : IsFiniteMeasure μ✝
inst✝ : IsFiniteMeasure ν
c : ℝ≥0
hc : ¬c = 0
hc' : ↑c ≠ 0
μ : Measure α
⊢ μ = c⁻¹ • c • μ

Tactic:
rw [smul_smul, inv_mul_cancel₀ hc, one_smul]

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

Goal state before:
pp: α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f g : α → ℝ
hf : StronglyMeasurable f
hfi : IntegrableOn f s μ
hg : StronglyMeasurable g
hgi : IntegrableOn g s μ
hgf : ∀ (t : Set α), MeasurableSet t → μ t < ∞ → ∫ (x : α) in t, g x ∂μ = ∫ (x : α) in t, f x ∂μ
hs : MeasurableSet s
hμs : μ s ≠ ∞
⊢ ∫⁻ (x : α) in s, ‖g x‖ₑ ∂μ ≤ ∫⁻ (x : α) in s, ‖f x‖ₑ ∂μ

Tactic:
← ofReal_integral_norm_eq_lintegral_enorm hfi,

Goal state after:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f g : α → ℝ
hf : StronglyMeasurable f
hfi : IntegrableOn f s μ
hg : StronglyMeasurable g
hgi : IntegrableOn g s μ
hgf : ∀ (t : Set α), MeasurableSet t → μ t < ∞ → ∫ (x : α) in t, g x ∂μ = ∫ (x : α) in t, f x ∂μ
hs : MeasurableSet s
hμs : μ s ≠ ∞
⊢ ∫⁻ (x : α) in s, ‖g x‖ₑ ∂μ ≤ ENNReal.ofReal (∫ (x : α) in s, ‖f x‖ ∂μ)
Module: Mathlib.InformationTheory.KullbackLeibler.Basic

Goal state before:
pp: case pos
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
hμ : ¬μ = 0
hν : ν = 0
⊢ 0 ≤ ∫ (x : α), llr μ ν x ∂μ + μ.real univ * log (ν.real univ) + 1 - μ.real univ

pp: case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
hμ : ¬μ = 0
hν : ¬ν = 0
⊢ 0 ≤ ∫ (x : α), llr μ ν x ∂μ + μ.real univ * log (ν.real univ) + 1 - μ.real univ

Tactic:
· refine absurd ?_ hμ
    rw [hν] at hμν
    exact Measure.absolutelyContinuous_zero_iff.mp hμν

Goal state after:
case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
hμ : ¬μ = 0
hν : ¬ν = 0
⊢ 0 ≤ ∫ (x : α), llr μ ν x ∂μ + μ.real univ * log (ν.real univ) + 1 - μ.real univ
Module: Mathlib.InformationTheory.KullbackLeibler.Basic

Goal state before:
pp: case pos
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
hμ : ¬μ = 0
hν : ν = 0
⊢ μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ ≤ (klDiv μ ν).toReal

pp: case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
hμ : ¬μ = 0
hν : ¬ν = 0
⊢ μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ ≤ (klDiv μ ν).toReal

Tactic:
· refine absurd ?_ hμ
    rw [hν] at hμν
    exact Measure.absolutelyContinuous_zero_iff.mp hμν

Goal state after:
case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
hμ : ¬μ = 0
hν : ¬ν = 0
⊢ μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ ≤ (klDiv μ ν).toReal
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2

Goal state before:
pp: α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ∞
f : ↥(Lp ℝ 2 μ)
hf : ↑↑f =ᵐ[μ.restrict s] 0
h_nnnorm_eq_zero : ∫⁻ (x : α) in s, ↑‖↑↑↑((condExpL2 ℝ ℝ hm) f) x‖₊ ∂μ = 0
⊢ Measurable fun x ↦ ↑‖↑↑↑((condExpL2 ℝ ℝ hm) f) x‖₊

Tactic:
refine Measurable.coe_nnreal_ennreal (Measurable.nnnorm ?_)

Goal state after:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ∞
f : ↥(Lp ℝ 2 μ)
hf : ↑↑f =ᵐ[μ.restrict s] 0
h_nnnorm_eq_zero : ∫⁻ (x : α) in s, ↑‖↑↑↑((condExpL2 ℝ ℝ hm) f) x‖₊ ∂μ = 0
⊢ Measurable ↑↑↑((condExpL2 ℝ ℝ hm) f)
Module: Mathlib.MeasureTheory.Function.LpSpace.InfiniteSum

Goal state before:
pp: X : Type u_1
E : Type u_2
x✝ : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
p : ℝ≥0∞
hp : Fact (1 ≤ p)
inst✝ : CompleteSpace E
f : ℕ → ↥(Lp E p μ)
hf : ∑' (n : ℕ), ‖f n‖ₑ ≠ ∞
A : ∀ᵐ (a : X) ∂μ, Summable fun n ↦ ‖↑↑(f n) a‖
B : ∀ᵐ (x : X) ∂μ, ∀ (n : ℕ), ↑↑(∑ i ∈ range n, f i) x = ∑ i ∈ range n, ↑↑(f i) x
ns : ℕ → ℕ
hns : StrictMono ns
nslim : ∀ᵐ (x : X) ∂μ, Tendsto (fun i ↦ ↑↑(∑ j ∈ range (ns i), f j) x) atTop (𝓝 (↑↑(∑' (n : ℕ), f n) x))
x : X
S : Summable fun n ↦ ‖↑↑(f n) x‖
h'x : ∀ (n : ℕ), ↑↑(∑ i ∈ range n, f i) x = ∑ i ∈ range n, ↑↑(f i) x
h''x : Tendsto (fun i ↦ ↑↑(∑ j ∈ range (ns i), f j) x) atTop (𝓝 (↑↑(∑' (n : ℕ), f n) x))
⊢ HasSum (fun n ↦ ↑↑(f n) x) (↑↑(∑' (n : ℕ), f n) x)

Tactic:
apply hasSum_of_subseq_of_summable S (tendsto_finset_range.comp hns.tendsto_atTop)

Goal state after:
X : Type u_1
E : Type u_2
x✝ : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
p : ℝ≥0∞
hp : Fact (1 ≤ p)
inst✝ : CompleteSpace E
f : ℕ → ↥(Lp E p μ)
hf : ∑' (n : ℕ), ‖f n‖ₑ ≠ ∞
A : ∀ᵐ (a : X) ∂μ, Summable fun n ↦ ‖↑↑(f n) a‖
B : ∀ᵐ (x : X) ∂μ, ∀ (n : ℕ), ↑↑(∑ i ∈ range n, f i) x = ∑ i ∈ range n, ↑↑(f i) x
ns : ℕ → ℕ
hns : StrictMono ns
nslim : ∀ᵐ (x : X) ∂μ, Tendsto (fun i ↦ ↑↑(∑ j ∈ range (ns i), f j) x) atTop (𝓝 (↑↑(∑' (n : ℕ), f n) x))
x : X
S : Summable fun n ↦ ‖↑↑(f n) x‖
h'x : ∀ (n : ℕ), ↑↑(∑ i ∈ range n, f i) x = ∑ i ∈ range n, ↑↑(f i) x
h''x : Tendsto (fun i ↦ ↑↑(∑ j ∈ range (ns i), f j) x) atTop (𝓝 (↑↑(∑' (n : ℕ), f n) x))
⊢ Tendsto (fun b ↦ ∑ i ∈ (range ∘ ns) b, ↑↑(f i) x) atTop (𝓝 (↑↑(∑' (n : ℕ), f n) x))
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)
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))

Tactic:
hf_eq

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)
hf_eq :
  (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.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)
⊢ s.indicator μ[f | m] =ᵐ[μ] s.indicator μ[s.indicator f + sᶜ.indicator f | m]

Tactic:
rw [Set.indicator_self_add_compl s f]

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Ω₀
hσ : ¬SigmaFinite (P.trim hm)
⊢ Measurable P⁻[X | mΩ]

Tactic:
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 Y : Ω → ℝ≥0∞
hXY : X ≤ᵐ[P] Y
hm : mΩ ≤ mΩ₀
hσ : ¬SigmaFinite (P.trim hm)
⊢ P⁻[X | mΩ] ≤ᵐ[P] P⁻[Y | mΩ]

Tactic:
simp_rw [condLExp_of_not_sigmaFinite hm hσ, Filter.EventuallyLE.rfl]

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

Goal state before:
pp: 𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
hm : m ≤ m𝓧
inst✝ : IsFiniteMeasure μ
hsf : SigmaFinite (ν.trim hm)
hμν : μ ≪ ν
this : SigmaFinite (Measure.map id ν)
h :
  (fun a ↦ ((Measure.map id μ).rnDeriv (Measure.map id ν) a).toReal) =ᵐ[ν.trim ⋯] ν[fun a ↦ (μ.rnDeriv ν a).toReal | m]
⊢ (fun x ↦ ((Measure.map id μ).rnDeriv (Measure.map id ν) x).toReal) =ᵐ[Measure.map id ν]
    ν[fun x ↦ (μ.rnDeriv ν x).toReal | m]

Tactic:
trim_eq_map

Goal state after:
𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
hm : m ≤ m𝓧
inst✝ : IsFiniteMeasure μ
hsf : SigmaFinite (ν.trim hm)
hμν : μ ≪ ν
this : SigmaFinite (Measure.map id ν)
h :
  (fun a ↦ ((Measure.map id μ).rnDeriv (Measure.map id ν) a).toReal) =ᵐ[Measure.map id ν]
    ν[fun a ↦ (μ.rnDeriv ν a).toReal | m]
⊢ (fun x ↦ ((Measure.map id μ).rnDeriv (Measure.map id ν) x).toReal) =ᵐ[Measure.map id ν]
    ν[fun x ↦ (μ.rnDeriv ν x).toReal | m]
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen

Goal state before:
pp: case pos
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
α : Type u_2
m mα : MeasurableSpace α
μ : Measure α
f : α → E
hm : m ≤ mα
hμm : ¬SigmaFinite (μ.trim hm)
⊢ (fun x ↦ ‖μ[f | m] x‖) ≤ᵐ[μ] μ[fun x ↦ ‖f x‖ | m]

pp: case neg
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
α : Type u_2
m mα : MeasurableSpace α
μ : Measure α
f : α → E
hm : m ≤ mα
hμm : SigmaFinite (μ.trim hm)
⊢ (fun x ↦ ‖μ[f | m] x‖) ≤ᵐ[μ] μ[fun x ↦ ‖f x‖ | m]

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

Goal state after:
case neg
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
α : Type u_2
m mα : MeasurableSpace α
μ : Measure α
f : α → E
hm : m ≤ mα
hμm : SigmaFinite (μ.trim hm)
⊢ (fun x ↦ ‖μ[f | m] x‖) ≤ᵐ[μ] μ[fun x ↦ ‖f x‖ | m]
Module: Mathlib.InformationTheory.KullbackLeibler.DataProcessing

Goal state before:
pp: 𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hm : m ≤ m𝓧
⊢ klDiv (μ.trim hm) (ν.trim hm) ≤ klDiv μ ν

Tactic:
trim_eq_map

Goal state after:
𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hm : m ≤ m𝓧
⊢ klDiv (Measure.map id μ) (Measure.map id ν) ≤ klDiv μ ν
Module: Mathlib.LinearAlgebra.Dual.BaseChange

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommSemiring R
V : Type u_2
inst✝⁹ : AddCommMonoid V
inst✝⁸ : Module R V
W : Type u_3
inst✝⁷ : AddCommMonoid W
inst✝⁶ : Module R W
A : Type u_4
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : Module A W
inst✝² : IsScalarTower R A W
j : V →ₗ[R] W
ibc : IsBaseChange A j
inst✝¹ : Free R V
inst✝ : Module.Finite R V
⊢ A ⊗[R] Dual R V ≃ₗ[A] Dual A W

Tactic:
apply LinearEquiv.ofBijective ibc.toDualBaseChangeAux

Goal state after:
R : Type u_1
inst✝¹⁰ : CommSemiring R
V : Type u_2
inst✝⁹ : AddCommMonoid V
inst✝⁸ : Module R V
W : Type u_3
inst✝⁷ : AddCommMonoid W
inst✝⁶ : Module R W
A : Type u_4
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : Module A W
inst✝² : IsScalarTower R A W
j : V →ₗ[R] W
ibc : IsBaseChange A j
inst✝¹ : Free R V
inst✝ : Module.Finite R V
⊢ Function.Bijective ⇑ibc.toDualBaseChangeAux
Module: Mathlib.LinearAlgebra.Transvection.Basic

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
f : Dual R V
v : V
hf : f v = 0
hf' : (-f) v = 0
x✝ : V
⊢ (transvection hf).symm x✝ = (transvection hf') x✝

Tactic:
simp [symm_apply_eq, comp_of_right_eq_apply hf]

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

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
f : Dual R V
v : V
hfv : f v = 0
⊢ transvection hfv ∈ dilatransvections R V

Tactic:
exact ⟨f, v, by simp⟩

Goal state after:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction

Goal state before:
pp: case ι_mul
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d d' d₁ d₂ : Module.Dual R M
x✝ : CliffordAlgebra Q
m✝ : M
hx :
  (foldr' Q (contractLeftAux Q (d₁ + d₂)) ⋯ 0) x✝ =
    (foldr' Q (contractLeftAux Q d₁) ⋯ 0) x✝ + (foldr' Q (contractLeftAux Q d₂) ⋯ 0) x✝
⊢ ((contractLeftAux Q (d₁ + d₂)) m✝)
      (x✝, (foldr' Q (contractLeftAux Q d₁) ⋯ 0) x✝ + (foldr' Q (contractLeftAux Q d₂) ⋯ 0) x✝) =
    ((contractLeftAux Q d₁) m✝) (x✝, (foldr' Q (contractLeftAux Q d₁) ⋯ 0) x✝) +
      ((contractLeftAux Q d₂) m✝) (x✝, (foldr' Q (contractLeftAux Q d₂) ⋯ 0) x✝)

Tactic:
dsimp only [contractLeftAux_apply_apply]

Goal state after:
case ι_mul
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d d' d₁ d₂ : Module.Dual R M
x✝ : CliffordAlgebra Q
m✝ : M
hx :
  (foldr' Q (contractLeftAux Q (d₁ + d₂)) ⋯ 0) x✝ =
    (foldr' Q (contractLeftAux Q d₁) ⋯ 0) x✝ + (foldr' Q (contractLeftAux Q d₂) ⋯ 0) x✝
⊢ (d₁ + d₂) m✝ • x✝ - (ι Q) m✝ * ((foldr' Q (contractLeftAux Q d₁) ⋯ 0) x✝ + (foldr' Q (contractLeftAux Q d₂) ⋯ 0) x✝) =
    d₁ m✝ • x✝ - (ι Q) m✝ * (foldr' Q (contractLeftAux Q d₁) ⋯ 0) x✝ +
      (d₂ m✝ • x✝ - (ι Q) m✝ * (foldr' Q (contractLeftAux Q d₂) ⋯ 0) x✝)
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction

Goal state before:
pp: case ι_mul
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d✝ d' : Module.Dual R M
c : R
d : Module.Dual R M
x✝ : CliffordAlgebra Q
m✝ : M
hx : (foldr' Q (contractLeftAux Q (c • d)) ⋯ 0) x✝ = c • (foldr' Q (contractLeftAux Q d) ⋯ 0) x✝
⊢ ((contractLeftAux Q (c • d)) m✝) (x✝, c • (foldr' Q (contractLeftAux Q d) ⋯ 0) x✝) =
    c • ((contractLeftAux Q d) m✝) (x✝, (foldr' Q (contractLeftAux Q d) ⋯ 0) x✝)

Tactic:
dsimp only [contractLeftAux_apply_apply]

Goal state after:
case ι_mul
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d✝ d' : Module.Dual R M
c : R
d : Module.Dual R M
x✝ : CliffordAlgebra Q
m✝ : M
hx : (foldr' Q (contractLeftAux Q (c • d)) ⋯ 0) x✝ = c • (foldr' Q (contractLeftAux Q d) ⋯ 0) x✝
⊢ (c • d) m✝ • x✝ - (ι Q) m✝ * c • (foldr' Q (contractLeftAux Q d) ⋯ 0) x✝ =
    c • (d m✝ • x✝ - (ι Q) m✝ * (foldr' Q (contractLeftAux Q d) ⋯ 0) x✝)
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs

Goal state before:
pp: x y : CliffordAlgebra Q
⊢ CliffordAlgebraComplex.equiv (x * y) = CliffordAlgebraComplex.equiv (y * x)

Tactic:
rw [map_mul, mul_comm, map_mul]

Goal state after:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction

Goal state before:
pp: R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
B : BilinForm R M
v : M
x : CliffordAlgebra Q
⊢ ((changeFormAux Q B) v) (((changeFormAux Q B) v) x) = (Q v - (B v) v) • x

Tactic:
simp only [changeFormAux_apply_apply]
  rw [mul_sub, ← mul_assoc, ι_sq_scalar, map_sub, contractLeft_ι_mul, ← sub_add, sub_sub_sub_comm,
    ← Algebra.smul_def, sub_self, sub_zero, contractLeft_contractLeft, add_zero, sub_smul]

Goal state after:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
⊢ -(v Q) m * -1 = (v Q) m

Tactic:
mul_neg_one,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
⊢ - -(v Q) m = (v Q) m
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Even

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra R A
f g : ↥(even Q) →ₐ[R] A
h : (ι Q).compr₂ f = (ι Q).compr₂ g
⊢ f = g

Tactic:
EvenHom.ext_iff

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra R A
f g : ↥(even Q) →ₐ[R] A
h : ((ι Q).compr₂ f).bilin = ((ι Q).compr₂ g).bilin
⊢ f = g
Module: Mathlib.LinearAlgebra.Transvection.Basic

Goal state before:
pp: case neg
K : Type u_3
V : Type u_4
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : Dual K V
v : V
hfv : ¬f v = 0
ι : Set V
b : Basis (↑ι) K V
i : ↑ι
hv : v = b i
hf : f = f v • b.coord i
this : Fintype ↑ι
x y : ↑ι
hxy : ¬x = y
⊢ f v * ((Finsupp.single y 1) i * (Finsupp.single i 1) x) = 0

Tactic:
convert! mul_zero _

Goal state after:
case e'_2.e'_6
K : Type u_3
V : Type u_4
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : Dual K V
v : V
hfv : ¬f v = 0
ι : Set V
b : Basis (↑ι) K V
i : ↑ι
hv : v = b i
hf : f = f v • b.coord i
this : Fintype ↑ι
x y : ↑ι
hxy : ¬x = y
⊢ (Finsupp.single y 1) i * (Finsupp.single i 1) x = 0