mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.InformationTheory.Coding.KraftMcMillan

Goal state before:
pp: case calc.step.succ.zero
α : Type u_1
S : Finset (List α)
inst✝¹ : Fintype α
inst✝ : Nonempty α
h : UniquelyDecodable ↑S
maxLen : ℕ := S.sup List.length
D : ℝ := ↑(Fintype.card α)
hr : 0 + 1 ≥ 1
T : Finset (List α) := Finset.image concatFn Finset.univ
hlen_maps : ∀ x ∈ T, x.length ∈ Finset.Icc (0 + 1) ((0 + 1) * maxLen)
⊢ ∑ i ∈ Finset.Icc (0 + 1) ((0 + 1) * maxLen), ↑(Fintype.card α) ^ i * (1 / ↑(Fintype.card α)) ^ i ≤ ↑(0 + 1) * ↑maxLen

Tactic:
rcases maxLen with (_ | _ | maxLen)

Goal state after:
case calc.step.succ.zero.zero
α : Type u_1
S : Finset (List α)
inst✝¹ : Fintype α
inst✝ : Nonempty α
h : UniquelyDecodable ↑S
D : ℝ := ↑(Fintype.card α)
hr : 0 + 1 ≥ 1
T : Finset (List α) := Finset.image concatFn Finset.univ
hlen_maps : ∀ x ∈ T, x.length ∈ Finset.Icc (0 + 1) ((0 + 1) * 0)
⊢ ∑ i ∈ Finset.Icc (0 + 1) ((0 + 1) * 0), ↑(Fintype.card α) ^ i * (1 / ↑(Fintype.card α)) ^ i ≤ ↑(0 + 1) * ↑0

case calc.step.succ.zero.succ.zero
α : Type u_1
S : Finset (List α)
inst✝¹ : Fintype α
inst✝ : Nonempty α
h : UniquelyDecodable ↑S
D : ℝ := ↑(Fintype.card α)
hr : 0 + 1 ≥ 1
T : Finset (List α) := Finset.image concatFn Finset.univ
hlen_maps : ∀ x ∈ T, x.length ∈ Finset.Icc (0 + 1) ((0 + 1) * (0 + 1))
⊢ ∑ i ∈ Finset.Icc (0 + 1) ((0 + 1) * (0 + 1)), ↑(Fintype.card α) ^ i * (1 / ↑(Fintype.card α)) ^ i ≤
    ↑(0 + 1) * ↑(0 + 1)

case calc.step.succ.zero.succ.succ
α : Type u_1
S : Finset (List α)
inst✝¹ : Fintype α
inst✝ : Nonempty α
h : UniquelyDecodable ↑S
D : ℝ := ↑(Fintype.card α)
hr : 0 + 1 ≥ 1
T : Finset (List α) := Finset.image concatFn Finset.univ
maxLen : ℕ
hlen_maps : ∀ x ∈ T, x.length ∈ Finset.Icc (0 + 1) ((0 + 1) * (maxLen + 1 + 1))
⊢ ∑ i ∈ Finset.Icc (0 + 1) ((0 + 1) * (maxLen + 1 + 1)), ↑(Fintype.card α) ^ i * (1 / ↑(Fintype.card α)) ^ i ≤
    ↑(0 + 1) * ↑(maxLen + 1 + 1)
Module: Mathlib.InformationTheory.Coding.KraftMcMillan

Goal state before:
pp: case calc.step.succ.succ
α : Type u_1
S : Finset (List α)
inst✝¹ : Fintype α
inst✝ : Nonempty α
h : UniquelyDecodable ↑S
maxLen : ℕ := S.sup List.length
D : ℝ := ↑(Fintype.card α)
r : ℕ
hr : r + 1 + 1 ≥ 1
T : Finset (List α) := Finset.image concatFn Finset.univ
hlen_maps : ∀ x ∈ T, x.length ∈ Finset.Icc (r + 1 + 1) ((r + 1 + 1) * maxLen)
⊢ ∑ i ∈ Finset.Icc (r + 1 + 1) ((r + 1 + 1) * maxLen), ↑(Fintype.card α) ^ i * (1 / ↑(Fintype.card α)) ^ i ≤
    ↑(r + 1 + 1) * ↑maxLen

Tactic:
rcases maxLen with (_ | _ | maxLen)

Goal state after:
case calc.step.succ.succ.zero
α : Type u_1
S : Finset (List α)
inst✝¹ : Fintype α
inst✝ : Nonempty α
h : UniquelyDecodable ↑S
D : ℝ := ↑(Fintype.card α)
r : ℕ
hr : r + 1 + 1 ≥ 1
T : Finset (List α) := Finset.image concatFn Finset.univ
hlen_maps : ∀ x ∈ T, x.length ∈ Finset.Icc (r + 1 + 1) ((r + 1 + 1) * 0)
⊢ ∑ i ∈ Finset.Icc (r + 1 + 1) ((r + 1 + 1) * 0), ↑(Fintype.card α) ^ i * (1 / ↑(Fintype.card α)) ^ i ≤
    ↑(r + 1 + 1) * ↑0

case calc.step.succ.succ.succ.zero
α : Type u_1
S : Finset (List α)
inst✝¹ : Fintype α
inst✝ : Nonempty α
h : UniquelyDecodable ↑S
D : ℝ := ↑(Fintype.card α)
r : ℕ
hr : r + 1 + 1 ≥ 1
T : Finset (List α) := Finset.image concatFn Finset.univ
hlen_maps : ∀ x ∈ T, x.length ∈ Finset.Icc (r + 1 + 1) ((r + 1 + 1) * (0 + 1))
⊢ ∑ i ∈ Finset.Icc (r + 1 + 1) ((r + 1 + 1) * (0 + 1)), ↑(Fintype.card α) ^ i * (1 / ↑(Fintype.card α)) ^ i ≤
    ↑(r + 1 + 1) * ↑(0 + 1)

case calc.step.succ.succ.succ.succ
α : Type u_1
S : Finset (List α)
inst✝¹ : Fintype α
inst✝ : Nonempty α
h : UniquelyDecodable ↑S
D : ℝ := ↑(Fintype.card α)
r : ℕ
hr : r + 1 + 1 ≥ 1
T : Finset (List α) := Finset.image concatFn Finset.univ
maxLen : ℕ
hlen_maps : ∀ x ∈ T, x.length ∈ Finset.Icc (r + 1 + 1) ((r + 1 + 1) * (maxLen + 1 + 1))
⊢ ∑ i ∈ Finset.Icc (r + 1 + 1) ((r + 1 + 1) * (maxLen + 1 + 1)), ↑(Fintype.card α) ^ i * (1 / ↑(Fintype.card α)) ^ i ≤
    ↑(r + 1 + 1) * ↑(maxLen + 1 + 1)
Module: Mathlib.Probability.Kernel.Composition.MapComap

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : β → γ
hf : Measurable f
a : α
s : Set γ
hs : MeasurableSet s
⊢ ∑' (i : ℕ), (((κ.seq i).map f) a) s = ∑' (i : ℕ), ((κ.seq i) a) (f ⁻¹' s)

Tactic:
map_apply' _ hf _ hs

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel β γ
f : α → β
g : γ → δ
hf : Measurable f
hg : Measurable g
⊢ (κ.map g).comap f hf = (κ.comap f hf).map g

Tactic:
by
  ext x s _
  rw [comap_apply, map_apply _ hg, map_apply _ hg, comap_apply]

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel β γ
f : γ → δ
hf : Measurable f
a : α
s : Set δ
hs : MeasurableSet s
⊢ ∫⁻ (b : β), (η b) (f ⁻¹' s) ∂κ a = ∫⁻ (b : β), ((η.map f) b) s ∂κ a

Tactic:
map_apply' _ hf _ hs

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
f : β → γ
g : β → δ
hg : Measurable g
hf : Measurable f
x : α
s : Set γ
hs : MeasurableSet s
⊢ (κ x) ((fun x ↦ (f x, g x)) ⁻¹' {p | p.1 ∈ s}) = ((κ.map f) x) s

pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
f : β → γ
g : β → δ
hg : Measurable g
hf : Measurable f
x : α
s : Set γ
hs : MeasurableSet s
⊢ MeasurableSet {p | p.1 ∈ s}

Tactic:
map_apply' _ hf _ hs

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
f : β → γ
g : β → δ
hg : Measurable g
hf : Measurable f
x : α
s : Set γ
hs : MeasurableSet s
⊢ (κ x) ((fun x ↦ (f x, g x)) ⁻¹' {p | p.1 ∈ s}) = (κ x) (f ⁻¹' s)

case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
f : β → γ
g : β → δ
hg : Measurable g
hf : Measurable f
x : α
s : Set γ
hs : MeasurableSet s
⊢ MeasurableSet {p | p.1 ∈ s}
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
γ : Type u_3
mγ : MeasurableSpace γ
η : Kernel (α × β) γ
⊢ map (⇑MeasurableEquiv.prodAssoc.symm) (μ ⊗ₘ (κ ⊗ₖ η)) = μ ⊗ₘ κ ⊗ₘ η

Tactic:
by
  by_cases hμ : SFinite μ
  swap; · simp [hμ]
  by_cases hκ : IsSFiniteKernel κ
  swap; · simp [hκ]
  by_cases hη : IsSFiniteKernel η
  swap; · simp [hη]
  ext s hs
  rw [Measure.compProd_apply hs, Measure.map_apply (by fun_prop) hs,
    Measure.compProd_apply (hs.preimage (by fun_prop)), Measure.lintegral_compProd]
  swap; · exact Kernel.measurable_kernel_prodMk_left hs
  congr with a
  rw [Kernel.compProd_apply]
  · congr
  · exact hs.preimage (by fun_prop)

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

Goal state before:
pp: case pos.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
η : Kernel Z T
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
ac : X × Z
s : Set (T × Y)
hs : MeasurableSet s
d : T
⊢ ∫⁻ (x : Y), (Measure.dirac (d, x)) s ∂κ ac.1 = (κ ac.1) (Prod.mk d ⁻¹' s)

Tactic:
Measure.dirac_apply' _ hs,

Goal state after:
case pos.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
η : Kernel Z T
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
ac : X × Z
s : Set (T × Y)
hs : MeasurableSet s
d : T
⊢ ∫⁻ (x : Y), s.indicator 1 (d, x) ∂κ ac.1 = (κ ac.1) (Prod.mk d ⁻¹' s)
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
h : μ ⊗ₘ κ ⟂ₘ μ ⊗ₘ η
⊢ μ.withDensity (ν.rnDeriv μ) ⊗ₘ η ≪ μ ⊗ₘ η

Tactic:
· exact (withDensity_absolutelyContinuous μ (ν.rnDeriv μ)).compProd_left _

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
⊢ SFinite (⇑κ ∘ₘ μ)

Tactic:
← snd_compProd

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
⊢ SFinite (μ ⊗ₘ κ).snd
Module: Mathlib.Probability.Kernel.Composition.MeasureComp

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteKernel κ
⊢ IsFiniteMeasure (⇑κ ∘ₘ μ)

Tactic:
← snd_compProd

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteKernel κ
⊢ IsFiniteMeasure (μ ⊗ₘ κ).snd
Module: Mathlib.Probability.Kernel.Composition.MeasureComp

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsMarkovKernel κ
⊢ IsProbabilityMeasure (⇑κ ∘ₘ μ)

Tactic:
← snd_compProd

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsMarkovKernel κ
⊢ IsProbabilityMeasure (μ ⊗ₘ κ).snd
Module: Mathlib.Probability.Kernel.Composition.MeasureComp

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : IsZeroOrProbabilityMeasure μ
inst✝ : IsZeroOrMarkovKernel κ
⊢ IsZeroOrProbabilityMeasure (⇑κ ∘ₘ μ)

Tactic:
← snd_compProd

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : IsZeroOrProbabilityMeasure μ
inst✝ : IsZeroOrMarkovKernel κ
⊢ IsZeroOrProbabilityMeasure (μ ⊗ₘ κ).snd
Module: Mathlib.Probability.Kernel.Composition.MeasureComp

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
⊢ ⇑(Kernel.discard α) ∘ₘ μ = μ Set.univ • dirac ()

Tactic:
by
  ext s hs; simp [Measure.bind_apply hs (Kernel.aemeasurable _), mul_comm]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst✝³ : IsFiniteMeasure μ
inst✝² : IsFiniteKernel κ
inst✝¹ : IsFiniteKernel η
h_ac : μ ⊗ₘ κ ≪ μ ⊗ₘ η
ν : Measure α
inst✝ : IsFiniteMeasure ν
⊢ (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) * (μ ⊗ₘ η).rnDeriv (ν ⊗ₘ η) =ᵐ[ν ⊗ₘ η] fun p ↦ μ.rnDeriv ν p.1 * (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) p

Tactic:
filter_upwards [rnDeriv_measure_compProd_left μ ν η] with p hp

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst✝³ : IsFiniteMeasure μ
inst✝² : IsFiniteKernel κ
inst✝¹ : IsFiniteKernel η
h_ac : μ ⊗ₘ κ ≪ μ ⊗ₘ η
ν : Measure α
inst✝ : IsFiniteMeasure ν
p : α × β
hp : (μ ⊗ₘ η).rnDeriv (ν ⊗ₘ η) p = μ.rnDeriv ν p.1
⊢ ((μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) * (μ ⊗ₘ η).rnDeriv (ν ⊗ₘ η)) p = μ.rnDeriv ν p.1 * (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) p
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 (β × γ)
κ : Kernel α β
inst✝¹ : IsMarkovKernel κ
η : Kernel (α × β) γ
inst✝ : IsMarkovKernel η
a : α
⊢ ((κ ⊗ₖ η) a) Set.univ = 1

Tactic:
by simp [compProd_apply]

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel (α × β) γ
ξ : Kernel (α × β × γ) δ
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
hξ : ¬IsSFiniteKernel ξ
⊢ (κ ⊗ₖ (η ⊗ₖ ξ.comap ⇑MeasurableEquiv.prodAssoc ⋯)).map ⇑MeasurableEquiv.prodAssoc.symm = κ ⊗ₖ η ⊗ₖ ξ

Tactic:
have : ¬ IsSFiniteKernel
        (ξ.comap MeasurableEquiv.prodAssoc (MeasurableEquiv.measurable _)) := by
      refine fun h_sfin ↦ hξ ?_
      have : ξ = (ξ.comap MeasurableEquiv.prodAssoc (MeasurableEquiv.measurable _)).comap
          MeasurableEquiv.prodAssoc.symm (MeasurableEquiv.measurable _) := by
        simp [← comap_comp_right]
      rw [this]
      infer_instance
    simp [hξ, this]

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 γ
ι : Type u_4
inst✝¹ : Countable ι
κ : ι → Kernel α β
η : Kernel (α × β) γ
inst✝ : ∀ (i : ι), IsSFiniteKernel (κ i)
⊢ Kernel.sum κ ⊗ₖ η = Kernel.sum fun i ↦ κ i ⊗ₖ η

Tactic:
by
  by_cases hη : IsSFiniteKernel η
  · ext a s hs
    simp_rw [sum_apply, compProd_apply hs, sum_apply, lintegral_sum_measure, Measure.sum_apply _ hs,
    compProd_apply hs]
  · simp [hη]

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

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

Tactic:
cases eq_zero_or_neZero μ with
  | inl h => simp [h]
  | inr h0 =>
    ext1 s hs
    rw [tilted_apply' _ _ hs, tilted_apply' _ _ hs, setLIntegral_tilted' f _ hs]
    congr with x
    rw [← ENNReal.ofReal_mul (by positivity),
      integral_exp_tilted f, Pi.add_apply, exp_add]
    congr 1
    simp only [Pi.add_apply]
    have := (integral_exp_pos hf).ne'
    simp [field]

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

Goal state before:
pp: case hy
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
c : ℝ≥0∞
hc : c ≠ 0
hc_ne_top : c ≠ ∞
h : (c • μ).rnDeriv ν =ᵐ[ν] c • μ.rnDeriv ν
x : α
hx_eq : (c • μ).rnDeriv ν x = (c • μ.rnDeriv ν) x
hx_pos : 0 < μ.rnDeriv ν x
hx_ne_top : μ.rnDeriv ν x < ∞
⊢ (μ.rnDeriv ν x).toReal ≠ 0

pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
c : ℝ≥0∞
hc : c ≠ 0
hc_ne_top : c ≠ ∞
h : (c • μ).rnDeriv ν =ᵐ[ν] c • μ.rnDeriv ν
x : α
hx_eq : (c • μ).rnDeriv ν x = (c • μ.rnDeriv ν) x
hx_pos : 0 < μ.rnDeriv ν x
hx_ne_top : μ.rnDeriv ν x < ∞
⊢ log c.toReal + log (μ.rnDeriv ν x).toReal = log (μ.rnDeriv ν x).toReal + log c.toReal

Tactic:
· rw [ENNReal.toReal_ne_zero]
    simp [hx_pos.ne', hx_ne_top.ne]

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
c : ℝ≥0∞
hc : c ≠ 0
hc_ne_top : c ≠ ∞
h : (c • μ).rnDeriv ν =ᵐ[ν] c • μ.rnDeriv ν
x : α
hx_eq : (c • μ).rnDeriv ν x = (c • μ.rnDeriv ν) x
hx_pos : 0 < μ.rnDeriv ν x
hx_ne_top : μ.rnDeriv ν x < ∞
⊢ log c.toReal + log (μ.rnDeriv ν x).toReal = log (μ.rnDeriv ν x).toReal + log c.toReal
Module: Mathlib.MeasureTheory.Measure.Tilted

Goal state before:
pp: case inr.refine_2
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable (fun x ↦ rexp (f x)) μ
h0 : NeZero μ
⊢ ∀ (a : α), 0 < rexp (f a) / ∫ (x : α), rexp (f x) ∂μ

Tactic:
exact fun _ ↦ div_pos (exp_pos _) (integral_exp_pos hf)

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

Goal state before:
pp: case hy
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
c : ℝ≥0∞
hc : c ≠ 0
hc_ne_top : c ≠ ∞
h : μ.rnDeriv (c • ν) =ᵐ[ν] c⁻¹ • μ.rnDeriv ν
x : α
hx_eq : μ.rnDeriv (c • ν) x = (c⁻¹ • μ.rnDeriv ν) x
hx_pos : 0 < μ.rnDeriv ν x
hx_ne_top : μ.rnDeriv ν x < ∞
⊢ (μ.rnDeriv ν x).toReal ≠ 0

pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
c : ℝ≥0∞
hc : c ≠ 0
hc_ne_top : c ≠ ∞
h : μ.rnDeriv (c • ν) =ᵐ[ν] c⁻¹ • μ.rnDeriv ν
x : α
hx_eq : μ.rnDeriv (c • ν) x = (c⁻¹ • μ.rnDeriv ν) x
hx_pos : 0 < μ.rnDeriv ν x
hx_ne_top : μ.rnDeriv ν x < ∞
⊢ log c⁻¹.toReal + log (μ.rnDeriv ν x).toReal = log (μ.rnDeriv ν x).toReal - log c.toReal

Tactic:
· rw [ENNReal.toReal_ne_zero]
    simp [hx_pos.ne', hx_ne_top.ne]

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
c : ℝ≥0∞
hc : c ≠ 0
hc_ne_top : c ≠ ∞
h : μ.rnDeriv (c • ν) =ᵐ[ν] c⁻¹ • μ.rnDeriv ν
x : α
hx_eq : μ.rnDeriv (c • ν) x = (c⁻¹ • μ.rnDeriv ν) x
hx_pos : 0 < μ.rnDeriv ν x
hx_ne_top : μ.rnDeriv ν x < ∞
⊢ log c⁻¹.toReal + log (μ.rnDeriv ν x).toReal = log (μ.rnDeriv ν x).toReal - log c.toReal
Module: Mathlib.MeasureTheory.Measure.Tilted

Goal state before:
pp: case inr.refine_2
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hf : Integrable (fun x ↦ rexp (f x)) ν
h0 : NeZero ν
⊢ ∀ (a : α), 0 < rexp (f a) / ∫ (x : α), rexp (f x) ∂ν

Tactic:
exact fun _ ↦ div_pos (exp_pos _) (integral_exp_pos hf)

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

Goal state before:
pp: α : Type u_5
β : Type u_6
E : Type u_7
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : NormedAddCommGroup E
κ : Kernel α β
μ : Measure α
f : β → E
h_int :
  (∀ᵐ (y : α) ∂(Kernel.const Unit μ) (), Integrable f (κ y)) ∧
    Integrable (fun y ↦ ∫ (z : β), ‖f z‖ ∂κ y) ((Kernel.const Unit μ) ())
⊢ ∀ᵐ (x : α) ∂μ, Integrable f (κ x)

Tactic:
exact h_int.1

Goal state after:
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
⊢ Integrable (llr (c • μ) ν) μ

Tactic:
integrable_congr h_llr

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
⊢ Integrable (fun x ↦ llr μ ν x + log ↑c) μ
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 α
hp : Fact (1 ≤ p)
inst✝ : CompleteSpace F
hm : m ≤ m0
⊢ IsComplete {f | AEStronglyMeasurable (↑↑f) μ}

Tactic:
rw [← completeSpace_coe_iff_isComplete]

Goal state after:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝¹ : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hp : Fact (1 ≤ p)
inst✝ : CompleteSpace F
hm : m ≤ m0
⊢ CompleteSpace ↑{f | AEStronglyMeasurable (↑↑f) μ}
Module: Mathlib.InformationTheory.KullbackLeibler.Basic

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : (fun x ↦ ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal)) =ᵐ[ν] 0
h_ne : μ ≪ ν ∧ Integrable (llr μ ν) μ
x : α
hx : ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal) = 0 x
⊢ μ.rnDeriv ν x = 1 x

Tactic:
simp only [Pi.zero_apply, ENNReal.ofReal_eq_zero] at hx

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : (fun x ↦ ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal)) =ᵐ[ν] 0
h_ne : μ ≪ ν ∧ Integrable (llr μ ν) μ
x : α
hx : klFun (μ.rnDeriv ν x).toReal ≤ 0
⊢ μ.rnDeriv ν x = 1 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 : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
c : ℝ
x : G
⊢ condExpIndL1 hm μ s (c • x) = c • condExpIndL1 hm μ s x

Tactic:
by
  by_cases hs : MeasurableSet s
  swap; · simp_rw [condExpIndL1_of_not_measurableSet hs]; rw [smul_zero]
  by_cases hμs : μ s = ∞
  · simp_rw [condExpIndL1_of_measure_eq_top hμs]; rw [smul_zero]
  · simp_rw [condExpIndL1_of_measurableSet_of_measure_ne_top hs hμs]
    exact condExpIndL1Fin_smul hs hμs c x

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
hμs : μ s ≠ ∞
ht : MeasurableSet t
hμt : μ t ≠ ∞
⊢ ∀ᵐ (x : α) ∂μ, (fun x ↦ ↑‖↑↑(indicatorConstLp 2 hs hμs 1) x‖₊) x = s.indicator (fun x ↦ 1) x

Tactic:
refine (@indicatorConstLp_coeFn _ _ _ 2 _ _ _ hs hμs (1 : ℝ)).mono fun x hx => ?_

Goal state after:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ∞
ht : MeasurableSet t
hμt : μ t ≠ ∞
x : α
hx : ↑↑(indicatorConstLp 2 hs hμs 1) x = s.indicator (fun x ↦ 1) x
⊢ (fun x ↦ ↑‖↑↑(indicatorConstLp 2 hs hμs 1) x‖₊) x = s.indicator (fun x ↦ 1) x
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2

Goal state before:
pp: case refine_3
α : 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 α
E'' : Type u_8
𝕜' : Type u_9
inst✝⁴ : RCLike 𝕜'
inst✝³ : NormedAddCommGroup E''
inst✝² : InnerProductSpace 𝕜' E''
inst✝¹ : CompleteSpace E''
inst✝ : NormedSpace ℝ E''
hm : m ≤ m0
T : E' →L[ℝ] E''
f : ↥(Lp E' 2 μ)
⊢ AEStronglyMeasurable (↑↑(T.compLp ↑((condExpL2 E' 𝕜 hm) f))) μ

Tactic:
· have h_coe := T.coeFn_compLp (condExpL2 E' 𝕜 hm f : α →₂[μ] E')
    rw [← EventuallyEq] at h_coe
    refine AEStronglyMeasurable.congr ?_ h_coe.symm
    exact T.continuous.comp_aestronglyMeasurable (lpMeas.aestronglyMeasurable (condExpL2 E' 𝕜 hm f))

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
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
hf : Integrable f μ
this : ∫ (x : α) in Set.univ, μ[f | m] x ∂μ = ∫ (x : α) in Set.univ, f x ∂μ
⊢ ∫ (x : α), μ[f | m] x ∂μ = ∫ (x : α), f x ∂μ

Tactic:
simp_rw [setIntegral_univ] at this; exact this

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

Goal state before:
pp: α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedSpace ℝ G
hm : m ≤ m0
x : G
⊢ condExpIndSMul hm ⋯ ⋯ x = 0

Tactic:
rw [condExpIndSMul, indicatorConstLp_empty]
  simp only [Submodule.coe_zero, map_zero]

Goal state after: