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

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

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

Goal state after:
case calc.step.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
T : Finset (List α) := Finset.image concatFn Finset.univ
hlen_maps : ∀ x ∈ T, x.length ∈ Finset.Icc 0 (0 * maxLen)
⊢ ∑ i ∈ Finset.Icc 0 (0 * maxLen), ↑(Fintype.card α) ^ i * (1 / ↑(Fintype.card α)) ^ i ≤ ↑0 * ↑maxLen

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

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
Module: Mathlib.Probability.Kernel.MeasurableLIntegral

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
t : Set (α × β)
ht : MeasurableSet t
c : ℝ≥0∞
⊢ Measurable fun a ↦ ∫⁻ (b : β), t.indicator (fun x ↦ c) (a, b) ∂κ a

Tactic:
lintegral_indicator_const_comp measurable_prodMk_left ht _

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
t : Set (α × β)
ht : MeasurableSet t
c : ℝ≥0∞
⊢ Measurable fun a ↦ c * (κ a) (Prod.mk a ⁻¹' t)
Module: Mathlib.Probability.Kernel.Basic

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
κ : Kernel Bool α
⊢ κ = boolKernel (κ false) (κ true)

Tactic:
ext (_ | _) <;> simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
η : Kernel β γ
inst✝¹ : IsFiniteKernel η
κ : Kernel α β
inst✝ : IsFiniteKernel κ
a : α
⊢ (κ a) Set.univ * η.bound ≤ κ.bound * η.bound

Tactic:
gcongr; exact measure_le_bound κ a Set.univ

Goal state after:
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
⊢ (Kernel.sum fun n ↦ (κ.seq n).map f) = κ.map f

Tactic:
ext a s hs
    rw [Kernel.sum_apply, map_apply' κ hf a hs, Measure.sum_apply _ hs, ← measure_sum_seq κ,
      Measure.sum_apply _ (hf hs)]
    simp_rw [map_apply' _ hf _ hs]

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 δ
f : β → γ
g : γ → α
κ : Kernel α β
inst✝ : IsFiniteKernel κ
hg : Measurable g
a : γ
⊢ (κ (g a)) Set.univ ≤ κ.bound

Tactic:
exact measure_le_bound κ _ _

Goal state after:
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 δ
γ : Type u_5
inst✝ : MeasurableSpace γ
κ : Kernel α β
f : β → δ
hf : Measurable f
⊢ (prodMkLeft γ κ).map f = prodMkLeft γ (κ.map f)

pp: case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
δ : Type u_4
mδ : MeasurableSpace δ
γ : Type u_5
inst✝ : MeasurableSpace γ
κ : Kernel α β
f : β → δ
hf : ¬Measurable f
⊢ (prodMkLeft γ κ).map f = prodMkLeft γ (κ.map f)

Tactic:
· simp only [map, hf, ↓reduceDIte]
    rfl

Goal state after:
case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
δ : Type u_4
mδ : MeasurableSpace δ
γ : Type u_5
inst✝ : MeasurableSpace γ
κ : Kernel α β
f : β → δ
hf : ¬Measurable f
⊢ (prodMkLeft γ κ).map f = prodMkLeft γ (κ.map f)
Module: Mathlib.Probability.Kernel.Composition.CompNotation

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
⊢ ⇑Kernel.id ∘ₘ μ = μ

Tactic:
rw [Kernel.id, deterministic_comp_eq_map, Measure.map_id]

Goal state after:
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 α β
γ : Type u_5
mγ : MeasurableSpace γ
f : β → δ
hf : Measurable f
⊢ (prodMkRight γ κ).map f = prodMkRight γ (κ.map f)

pp: case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
γ : Type u_5
mγ : MeasurableSpace γ
f : β → δ
hf : ¬Measurable f
⊢ (prodMkRight γ κ).map f = prodMkRight γ (κ.map f)

Tactic:
· simp only [map, hf, ↓reduceDIte]
    rfl

Goal state after:
case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
γ : Type u_5
mγ : MeasurableSpace γ
f : β → δ
hf : ¬Measurable f
⊢ (prodMkRight γ κ).map f = prodMkRight γ (κ.map f)
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 α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsMarkovKernel η
x : α
⊢ ∀ (b : β), (η (x, b)) {_c | b ∈ s} = s.indicator (fun x ↦ 1) b

Tactic:
intro b

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set β
hs : MeasurableSet s
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsMarkovKernel η
x : α
b : β
⊢ (η (x, b)) {_c | b ∈ s} = s.indicator (fun x ↦ 1) b
Module: Mathlib.Probability.Kernel.Composition.CompProd

Goal state before:
pp: case e'_2.e'_6
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : MeasurableSingletonClass γ
f : α × β → γ
hf : Measurable f
s : Set (β × γ)
hs : MeasurableSet s
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
x : α
t : Set β := {b | (b, f (x, b)) ∈ s}
ht : MeasurableSet t
⊢ ∀ b ∈ tᶜ, (if f (x, b) ∈ Prod.mk b ⁻¹' s then 1 else 0) = 0

Tactic:
intro b

Goal state after:
case e'_2.e'_6
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : MeasurableSingletonClass γ
f : α × β → γ
hf : Measurable f
s : Set (β × γ)
hs : MeasurableSet s
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
x : α
t : Set β := {b | (b, f (x, b)) ∈ s}
ht : MeasurableSet t
b : β
⊢ b ∈ tᶜ → (if f (x, b) ∈ Prod.mk b ⁻¹' s then 1 else 0) = 0
Module: Mathlib.Probability.Kernel.Composition.CompProd

Goal state before:
pp: case e'_3
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : MeasurableSingletonClass γ
f : α × β → γ
hf : Measurable f
s : Set (β × γ)
hs : MeasurableSet s
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
x : α
t : Set β := {b | (b, f (x, b)) ∈ s}
ht : MeasurableSet t
⊢ ∀ b ∈ t, (if f (x, b) ∈ Prod.mk b ⁻¹' s then 1 else 0) = 1

Tactic:
intro b

Goal state after:
case e'_3
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : MeasurableSingletonClass γ
f : α × β → γ
hf : Measurable f
s : Set (β × γ)
hs : MeasurableSet s
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
x : α
t : Set β := {b | (b, f (x, b)) ∈ s}
ht : MeasurableSet t
b : β
⊢ b ∈ t → (if f (x, b) ∈ Prod.mk b ⁻¹' s then 1 else 0) = 1
Module: Mathlib.Probability.Kernel.Composition.Prod

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 α β
inst✝² : IsSFiniteKernel κ
η : Kernel α γ
inst✝¹ : IsSFiniteKernel η
ξ : Kernel α δ
inst✝ : IsSFiniteKernel ξ
⊢ (κ ×ₖ ξ ×ₖ η).map ⇑MeasurableEquiv.prodAssoc = κ ×ₖ (ξ ×ₖ η)

Tactic:
ext1 a
  rw [map_apply _ (by fun_prop), prod_apply, prod_apply, Measure.prodAssoc_prod, prod_apply,
    prod_apply]

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

Goal state before:
pp: α : 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 < ∞
t₁ : Set α
t₂ : Set β
ht₁ : MeasurableSet t₁
ht₂ : MeasurableSet t₂
⊢ ∫⁻ (x : α × β) in t₁ ×ˢ t₂, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ = ∫⁻ (x : α × β) in t₁ ×ˢ t₂, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ

Tactic:
Measure.setLIntegral_rnDeriv (hμν.compProd_left _),

Goal state after:
α : 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 < ∞
t₁ : Set α
t₂ : Set β
ht₁ : MeasurableSet t₁
ht₂ : MeasurableSet t₂
⊢ (μ ⊗ₘ κ) (t₁ ×ˢ t₂) = ∫⁻ (x : α × β) in t₁ ×ˢ t₂, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
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:
hf_disj

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')
⊢ (∀ (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 ∂ν ⊗ₘ κ
Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv

Goal state before:
pp: 𝓧 : 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μν' : μ' ≪ ν'
h1' : μ'.rnDeriv ν' =ᵐ[ν'] (ν univ)⁻¹ • μ.rnDeriv ν'
h1 : μ'.rnDeriv ν' =ᵐ[ν] (ν univ)⁻¹ • μ.rnDeriv ν'
⊢ μ'.rnDeriv ν' =ᵐ[ν] μ.rnDeriv ν

Tactic:
have h2 : μ.rnDeriv ν' =ᵐ[ν] (ν univ)⁻¹⁻¹ • μ.rnDeriv ν :=
      Measure.rnDeriv_smul_right_of_ne_top' (μ := ν) (ν := μ) (by simp) (by simp [hν])

Goal state after:
𝓧 : 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μν' : μ' ≪ ν'
h1' : μ'.rnDeriv ν' =ᵐ[ν'] (ν univ)⁻¹ • μ.rnDeriv ν'
h1 : μ'.rnDeriv ν' =ᵐ[ν] (ν univ)⁻¹ • μ.rnDeriv ν'
h2 : μ.rnDeriv ν' =ᵐ[ν] (ν univ)⁻¹⁻¹ • μ.rnDeriv ν
⊢ μ'.rnDeriv ν' =ᵐ[ν] μ.rnDeriv ν
Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv

Goal state before:
pp: case neg.refine_1
𝓧 : 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 ν
h_eq : ∫ (x : 𝓧), f (μ'.rnDeriv ν' x).toReal ∂ν' = (ν.real univ)⁻¹ * ∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν
⊢ Integrable (fun x ↦ f (μ'.rnDeriv ν' x).toReal) ν'

Tactic:
refine Integrable.smul_measure ?_ (by simp [hν])
    refine (integrable_congr ?_).mpr hf_int
    filter_upwards [h_rnDeriv_eq] with x hx
    rw [hx]

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

Goal state before:
pp: 𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
𝓨 : Type u_2
m𝓨 : MeasurableSpace 𝓨
κ η : Kernel 𝓧 𝓨
f : ℝ → ℝ
inst✝³ : IsFiniteMeasure μ
inst✝² : IsFiniteMeasure ν
inst✝¹ : IsMarkovKernel κ
inst✝ : IsMarkovKernel η
hf : StronglyMeasurable f
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont_at : ContinuousWithinAt f (Ici 0) 0
h_int✝ :
  (∀ᵐ (x : 𝓧) ∂ν, Integrable (fun y ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal) (η x)) ∧
    Integrable (fun x ↦ ∫ (y : 𝓨), ‖f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal‖ ∂η x) ν
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
hf_cont : ContinuousOn f (Ici 0)
h_lt_top✝ : ∀ᵐ (a : 𝓧) ∂ν, ∀ᵐ (b : 𝓨) ∂η a, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b) < ∞
h_integrable :
  (∀ᵐ (x : 𝓧) ∂ν, Integrable (fun y ↦ ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal) (η x)) ∧
    Integrable (fun x ↦ ∫ (y : 𝓨), ‖((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal‖ ∂η x) ν
h_ae1 : ∀ᵐ (a : 𝓧) ∂ν, μ.rnDeriv ν a * ∫⁻ (b : 𝓨), (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) ∂η a = μ.rnDeriv ν a
h_ae2 :
  ∀ᵐ (a : 𝓧) ∂ν, ∀ᵐ (b : 𝓨) ∂η a, μ.rnDeriv ν a * (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) = (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b)
a : 𝓧
h_eq_one : μ.rnDeriv ν a * ∫⁻ (b : 𝓨), (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) ∂η a = μ.rnDeriv ν a
h_mul_eq : ∀ᵐ (b : 𝓨) ∂η a, μ.rnDeriv ν a * (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) = (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b)
h_lt_top : ∀ᵐ (b : 𝓨) ∂η a, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b) < ∞
h_int' : Integrable (fun y ↦ ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, y)).toReal) (η a)
h_int : Integrable (fun y ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, y)).toReal) (η a)
⊢ f (∫⁻ (b : 𝓨), μ.rnDeriv ν a * (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) ∂η a).toReal =
    f (∫⁻ (b : 𝓨), (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b) ∂η a).toReal

Tactic:
by
    congr 2
    refine lintegral_congr_ae ?_
    filter_upwards [h_mul_eq] with b hb using hb

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

Goal state before:
pp: ⊢ ¬DifferentiableWithinAt ℝ klFun (Ioi 0) 0

Tactic:
refine not_differentiableWithinAt_of_deriv_tendsto_atBot_Ioi _ ?_

Goal state after:
⊢ Tendsto (deriv klFun) (nhdsWithin 0 (Ioi 0)) atBot
Module: Mathlib.InformationTheory.KullbackLeibler.Basic

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
⊢ klDiv μ ν = if μ ≪ ν ∧ Integrable (llr μ ν) μ then ENNReal.ofReal (∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν) else ∞

Tactic:
rw [klDiv_def]
  exact if_ctx_congr Iff.rfl (fun h ↦ by rw [integral_klFun_rnDeriv h.1 h.2]) fun _ ↦ rfl

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

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

Tactic:
exact hμν.smul_left _

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

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

Tactic:
rw [memLp_one_iff_integrable]; apply integrable_condExpIndSMul

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

Goal state before:
pp: case refine_1
α : 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 : ↥(Lp F p μ) → Prop
h_ind : ∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ∞), P ↑(simpleFunc.indicatorConst p ⋯ ⋯ c)
h_add :
  ∀ ⦃f g : α → F⦄ (hf : MemLp f p μ) (hg : MemLp g p μ),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ →
        Disjoint (Function.support f) (Function.support g) →
          P (MemLp.toLp f hf) → P (MemLp.toLp g hg) → P (MemLp.toLp f hf + MemLp.toLp g hg)
h_closed : IsClosed {f | P ↑f}
f : ↥(Lp F p μ)
hf : AEStronglyMeasurable (↑↑f) μ
f' : ↥(lpMeas F ℝ m p μ) := ⟨f, hf⟩
g : ↥(Lp F p (μ.trim hm)) := (lpMeasToLpTrimLie F ℝ p μ hm) f'
hfg : f' = (lpMeasToLpTrimLie F ℝ p μ hm).symm g
⊢ ∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : (μ.trim hm) s < ∞),
    P ↑((lpMeasToLpTrimLie F ℝ p μ hm).symm ↑(simpleFunc.indicatorConst p hs ⋯ c))

Tactic:
intro b

Goal state after:
case refine_1
α : 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 : ↥(Lp F p μ) → Prop
h_ind : ∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ∞), P ↑(simpleFunc.indicatorConst p ⋯ ⋯ c)
h_add :
  ∀ ⦃f g : α → F⦄ (hf : MemLp f p μ) (hg : MemLp g p μ),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ →
        Disjoint (Function.support f) (Function.support g) →
          P (MemLp.toLp f hf) → P (MemLp.toLp g hg) → P (MemLp.toLp f hf + MemLp.toLp g hg)
h_closed : IsClosed {f | P ↑f}
f : ↥(Lp F p μ)
hf : AEStronglyMeasurable (↑↑f) μ
f' : ↥(lpMeas F ℝ m p μ) := ⟨f, hf⟩
g : ↥(Lp F p (μ.trim hm)) := (lpMeasToLpTrimLie F ℝ p μ hm) f'
hfg : f' = (lpMeasToLpTrimLie F ℝ p μ hm).symm g
b : F
⊢ ∀ {s : Set α} (hs : MeasurableSet s) (hμs : (μ.trim hm) s < ∞),
    P ↑((lpMeasToLpTrimLie F ℝ p μ hm).symm ↑(simpleFunc.indicatorConst p hs ⋯ b))
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable

Goal state before:
pp: case refine_3
α : 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 : ↥(Lp F p μ) → Prop
h_ind : ∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ∞), P ↑(simpleFunc.indicatorConst p ⋯ ⋯ c)
h_add :
  ∀ ⦃f g : α → F⦄ (hf : MemLp f p μ) (hg : MemLp g p μ),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ →
        Disjoint (Function.support f) (Function.support g) →
          P (MemLp.toLp f hf) → P (MemLp.toLp g hg) → P (MemLp.toLp f hf + MemLp.toLp g hg)
h_closed : IsClosed {f | P ↑f}
f : ↥(Lp F p μ)
hf : AEStronglyMeasurable (↑↑f) μ
f' : ↥(lpMeas F ℝ m p μ) := ⟨f, hf⟩
g : ↥(Lp F p (μ.trim hm)) := (lpMeasToLpTrimLie F ℝ p μ hm) f'
hfg : f' = (lpMeasToLpTrimLie F ℝ p μ hm).symm g
⊢ IsClosed {f | P ↑((lpMeasToLpTrimLie F ℝ p μ hm).symm f)}

Tactic:
· change IsClosed ((lpMeasToLpTrimLie F ℝ p μ hm).symm ⁻¹' {g : lpMeas F ℝ m p μ | P ↑g})
    exact IsClosed.preimage (LinearIsometryEquiv.continuous _) h_closed

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

Goal state before:
pp: case refine_1
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝¹ : SigmaFinite (μ.trim hm)
s : Set α
inst✝ : CompleteSpace F'
f : ↥(Lp F' 1 μ)
hs : MeasurableSet s
hμs : μ s ≠ ∞
⊢ ∀ (c : F') {s_1 : Set α} (hs : MeasurableSet s_1) (hμs : μ s_1 < ∞),
    ∫ (x : α) in s, ↑↑((condExpL1CLM F' hm μ) ↑(simpleFunc.indicatorConst 1 hs ⋯ c)) x ∂μ =
      ∫ (x : α) in s, ↑↑↑(simpleFunc.indicatorConst 1 hs ⋯ c) x ∂μ

Tactic:
intro x t ht hμt

Goal state after:
case refine_1
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝¹ : SigmaFinite (μ.trim hm)
s : Set α
inst✝ : CompleteSpace F'
f : ↥(Lp F' 1 μ)
hs : MeasurableSet s
hμs : μ s ≠ ∞
x : F'
t : Set α
ht : MeasurableSet t
hμt : μ t < ∞
⊢ ∫ (x_1 : α) in s, ↑↑((condExpL1CLM F' hm μ) ↑(simpleFunc.indicatorConst 1 ht ⋯ x)) x_1 ∂μ =
    ∫ (x_1 : α) in s, ↑↑↑(simpleFunc.indicatorConst 1 ht ⋯ x) x_1 ∂μ
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2

Goal state before:
pp: case refine_2
α : Type u_1
E : Type u_2
𝕜 : Type u_7
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp E 2 μ)
c : E
h_mem_Lp : MemLp (fun a ↦ ⟪c, ↑↑↑((condExpL2 E 𝕜 hm) f) a⟫) 2 μ
h_eq : ↑↑(MemLp.toLp (fun a ↦ ⟪c, ↑↑↑((condExpL2 E 𝕜 hm) f) a⟫) h_mem_Lp) =ᵐ[μ] fun a ↦ ⟪c, ↑↑↑((condExpL2 E 𝕜 hm) f) a⟫
s : Set α
hs : MeasurableSet s
hμs : μ s < ∞
⊢ ∫ (x : α) in s, ↑↑↑((condExpL2 𝕜 𝕜 hm) (MemLp.toLp (fun a ↦ ⟪c, ↑↑f a⟫) ⋯)) x ∂μ =
    ∫ (x : α) in s, ↑↑(MemLp.toLp (fun a ↦ ⟪c, ↑↑↑((condExpL2 E 𝕜 hm) f) a⟫) h_mem_Lp) x ∂μ

Tactic:
integral_condExpL2_eq_of_fin_meas_real _ hs hμs.ne,

Goal state after:
case refine_2
α : Type u_1
E : Type u_2
𝕜 : Type u_7
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp E 2 μ)
c : E
h_mem_Lp : MemLp (fun a ↦ ⟪c, ↑↑↑((condExpL2 E 𝕜 hm) f) a⟫) 2 μ
h_eq : ↑↑(MemLp.toLp (fun a ↦ ⟪c, ↑↑↑((condExpL2 E 𝕜 hm) f) a⟫) h_mem_Lp) =ᵐ[μ] fun a ↦ ⟪c, ↑↑↑((condExpL2 E 𝕜 hm) f) a⟫
s : Set α
hs : MeasurableSet s
hμs : μ s < ∞
⊢ ∫ (x : α) in s, ↑↑(MemLp.toLp (fun a ↦ ⟪c, ↑↑f a⟫) ⋯) x ∂μ =
    ∫ (x : α) in s, ↑↑(MemLp.toLp (fun a ↦ ⟪c, ↑↑↑((condExpL2 E 𝕜 hm) f) a⟫) h_mem_Lp) x ∂μ
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2

Goal state before:
pp: case refine_2
α : 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
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : μ s ≠ ∞
x : E'
⊢ ∀ (s_1 : Set α),
    MeasurableSet s_1 →
      μ s_1 ≠ ∞ → ∫⁻ (x_1 : α) in s_1, ‖↑↑↑((condExpL2 E' 𝕜 hm) (indicatorConstLp 2 hs hμs x)) x_1‖ₑ ∂μ ≤ μ s * ↑‖x‖₊

Tactic:
· refine fun t ht hμt =>
      (setLIntegral_nnnorm_condExpL2_indicator_le hm hs hμs x ht hμt).trans ?_
    gcongr
    apply Set.inter_subset_left

Goal state after: