awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
c : ℝ≥0∞
hc : c ≠ 0
hc_ne_top : c ≠ ∞
hc' : c⁻¹ ≠ 0
hc_ne_top' : c⁻¹ ≠ ∞
h :
  ∀ (x : α) (hx_left : llr (c⁻¹ • μ) ν x = llr μ ν x + log c⁻¹.toReal)
    (hx_right : llr μ (c • ν) x = llr μ ν x - log c.toReal), llr (c⁻¹ • μ) ν x = llr μ (c • ν) x
⊢ llr (c⁻¹ • μ) ν =ᶠ[ae μ] llr μ (c • ν)

Tactic:
filter_upwards [llr_smul_left hμν c⁻¹ hc' hc_ne_top', llr_smul_right hμν c hc hc_ne_top] with
    x hx_left hx_right

Premises used: Inv.inv, MeasureTheory.llr_smul_right, MeasureTheory.llr_smul_left
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
c : ℝ≥0∞
hc : c ≠ 0
hc_ne_top : c ≠ ∞
hc' : c⁻¹ ≠ 0
hc_ne_top' : c⁻¹ ≠ ∞
x : α
hx_left : llr (c⁻¹ • μ) ν x = llr μ ν x + log c⁻¹.toReal
hx_right : llr μ (c • ν) x = llr μ ν x - log c.toReal
h : llr μ ν x + log c⁻¹.toReal = llr μ ν x - log c.toReal
⊢ llr (c⁻¹ • μ) ν x = llr μ (c • ν) x

Tactic:
rw [hx_left, hx_right]
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
c : ℝ≥0∞
hc : c ≠ 0
hc_ne_top : c ≠ ∞
hc' : c⁻¹ ≠ 0
hc_ne_top' : c⁻¹ ≠ ∞
x : α
hx_left : llr (c⁻¹ • μ) ν x = llr μ ν x + log c⁻¹.toReal
hx_right : llr μ (c • ν) x = llr μ ν x - log c.toReal
⊢ llr μ ν x + log c⁻¹.toReal = llr μ ν x - log c.toReal

Tactic:
simp [sub_eq_add_neg]

Premises used: sub_eq_add_neg
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
c : ℝ≥0∞
hc : c ≠ 0
hc_ne_top : c ≠ ∞
⊢ c ≠ ∞

Tactic:
hc_ne_top
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
c : ℝ≥0∞
hc : c ≠ 0
hc_ne_top : c ≠ ∞
lift :
  ∀ (c : ℝ≥0) (hc : (↑c : ℝ≥0∞) ≠ 0),
    (ae μ).EventuallyEq (β := ℝ) (fun (x : α) ↦ log (((↑c : ℝ≥0∞) • μ).rnDeriv ((↑c : ℝ≥0∞) • ν) x).toReal)
      fun (x : α) ↦ log (μ.rnDeriv ν x).toReal
⊢ (ae μ).EventuallyEq (β := ℝ) (fun (x : α) ↦ log ((c • μ).rnDeriv (c • ν) x).toReal) fun (x : α) ↦
    log (μ.rnDeriv ν x).toReal

Tactic:
lift c to ℝ≥0 using hc_ne_top
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
c : ℝ≥0
hc : (↑c : ℝ≥0∞) ≠ 0
⊢ ¬c = 0

Tactic:
norm_cast at hc
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
c : ℝ≥0
hc : ¬c = 0
x : α
hx : (c • μ).rnDeriv (c • ν) x = μ.rnDeriv ν x
⊢ log (((↑c : ℝ≥0∞) • μ).rnDeriv ((↑c : ℝ≥0∞) • ν) x).toReal = log (μ.rnDeriv ν x).toReal

Tactic:
simp [hx]
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
c : ℝ≥0
hc : ¬c = 0
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ (c • μ).rnDeriv (c • ν) x = μ.rnDeriv ν x) x} x →
          Membership.mem (γ := Set α)
            {x : α |
              (fun (x : α) ↦
                  Eq (α := ℝ) ((fun (x : α) ↦ log (((↑c : ℝ≥0∞) • μ).rnDeriv ((↑c : ℝ≥0∞) • ν) x).toReal) x)
                    ((fun (x : α) ↦ log (μ.rnDeriv ν x).toReal) x))
                x}
            x}
      a
h₁ h₂ :
  ∀ (x : α) (hx : (c • μ).rnDeriv (c • ν) x = μ.rnDeriv ν x),
    log (((↑c : ℝ≥0∞) • μ).rnDeriv ((↑c : ℝ≥0∞) • ν) x).toReal = log (μ.rnDeriv ν x).toReal
⊢ (ae μ).EventuallyEq (β := ℝ) (fun (x : α) ↦ log (((↑c : ℝ≥0∞) • μ).rnDeriv ((↑c : ℝ≥0∞) • ν) x).toReal) fun (x : α) ↦
    log (μ.rnDeriv ν x).toReal

Tactic:
filter_upwards [hμν.ae_le (Measure.rnDeriv_smul_same μ ν hc)] with x hx using by simp [hx]

Premises used: MeasureTheory.Measure.rnDeriv_smul_same, MeasureTheory.Measure.AbsolutelyContinuous.ae_le
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
c : ℝ≥0
hc : c ≠ 0
h :
  ∀ (x : α) (hx : llr ((↑c : ℝ≥0∞) • μ) ((↑c : ℝ≥0∞) • ν) x = llr μ ν x),
    llr ((↑c : ℝ≥0∞) • μ) ((↑c : ℝ≥0∞) • ν) x = llr μ ν x
⊢ llr ((↑c : ℝ≥0∞) • μ) ((↑c : ℝ≥0∞) • ν) =ᶠ[ae μ] llr μ ν

Tactic:
filter_upwards [llr_smul_same hμν (c : ℝ≥0∞) (by simpa) (by simp)] with x hx

Premises used: ENNReal.ofNNReal, MeasureTheory.llr_smul_same
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
c : ℝ≥0
hc : c ≠ 0
x : α
hx : llr ((↑c : ℝ≥0∞) • μ) ((↑c : ℝ≥0∞) • ν) x = llr μ ν x
h h₁ : llr μ ν x = llr μ ν x
⊢ llr ((↑c : ℝ≥0∞) • μ) ((↑c : ℝ≥0∞) • ν) x = llr μ ν x

Tactic:
rw [hx]
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
⊢ Integrable (ε := ℝ) (fun (a : α) ↦ (μ.rnDeriv ν a).toReal * log (μ.rnDeriv ν a).toReal) ν ↔ Integrable (llr μ ν) μ

Tactic:
integrable_rnDeriv_smul_iff hμν

Premises used: MeasureTheory.llr, MeasureTheory.integrable_rnDeriv_smul_iff
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
simp_rw : Eq (α := ℝ) (∫ (a : α), (μ.rnDeriv ν a).toReal • log (μ.rnDeriv ν a).toReal ∂ν) (∫ (a : α), llr μ ν a ∂μ)
simp_rw₁ : Eq (α := ℝ) (∫ (x : α), log (μ.rnDeriv ν x).toReal ∂μ) (∫ (a : α), llr μ ν a ∂μ)
⊢ Eq (α := ℝ) (∫ (a : α), (μ.rnDeriv ν a).toReal * log (μ.rnDeriv ν a).toReal ∂ν) (∫ (a : α), llr μ ν a ∂μ)

Tactic:
simp_rw [← smul_eq_mul, integral_rnDeriv_smul hμν, llr]

Premises used: MeasureTheory.llr, MeasureTheory.integral_rnDeriv_smul, smul_eq_mul
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
hfν : AEMeasurable f ν
hμ : μ = 0
⊢ llr (μ.tilted f) ν =ᶠ[ae μ] fun (x : α) ↦ f x - log (∫ (z : α), rexp (f z) ∂μ) + llr μ ν x

Tactic:
simp only [hμ, ae_zero, Filter.EventuallyEq, Filter.eventually_bot]

Premises used: MeasureTheory.ae_zero, Filter.EventuallyEq, Filter.eventually_bot
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
hfν : AEMeasurable f ν
h0 : NeZero μ
h :
  ∀ (x : α) (hx : ((μ.tilted f).rnDeriv ν x).toReal = (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * (μ.rnDeriv ν x).toReal)
    (hx_pos : 0 < μ.rnDeriv ν x) (hx_lt_top : μ.rnDeriv ν x < ∞),
    llr (μ.tilted f) ν x = f x - log (∫ (z : α), rexp (f z) ∂μ) + llr μ ν x
⊢ llr (μ.tilted f) ν =ᶠ[ae μ] fun (x : α) ↦ f x - log (∫ (z : α), rexp (f z) ∂μ) + llr μ ν x

Tactic:
filter_upwards [hμν.ae_le (toReal_rnDeriv_tilted_left μ hfν), Measure.rnDeriv_pos hμν,
      hμν.ae_le (Measure.rnDeriv_lt_top μ ν)] with x hx hx_pos hx_lt_top

Premises used: MeasureTheory.toReal_rnDeriv_tilted_left, MeasureTheory.Measure.rnDeriv_lt_top, MeasureTheory.Measure.rnDeriv_pos, MeasureTheory.Measure.AbsolutelyContinuous.ae_le
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
hfν : AEMeasurable f ν
h0 : NeZero μ
x : α
hx : ((μ.tilted f).rnDeriv ν x).toReal = (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * (μ.rnDeriv ν x).toReal
hx_pos : 0 < μ.rnDeriv ν x
hx_lt_top : μ.rnDeriv ν x < ∞
h : Ne (α := ℝ) (∫ (x : α), rexp (f x) ∂μ)⁻¹ 0
h₁ : rexp (f x) / ∫ (x : α), rexp (f x) ∂μ ≠ 0
h₂ : (μ.rnDeriv ν x).toReal ≠ 0
⊢ llr (μ.tilted f) ν x = f x - log (∫ (z : α), rexp (f z) ∂μ) + llr μ ν x

Tactic:
rw [llr, hx, log_mul, div_eq_mul_inv, log_mul (exp_pos _).ne', log_exp, log_inv, llr,
      ← sub_eq_add_neg]

Premises used: Real.log_exp, sub_eq_add_neg, MeasureTheory.llr, div_eq_mul_inv, LT.lt.ne', Real.log_inv, Real.log_mul, Real.exp_pos
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
hfν : AEMeasurable f ν
h0 : NeZero μ
x : α
hx : ((μ.tilted f).rnDeriv ν x).toReal = (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * (μ.rnDeriv ν x).toReal
hx_pos : 0 < μ.rnDeriv ν x
hx_lt_top : μ.rnDeriv ν x < ∞
h : ¬Eq (α := ℝ) (∫ (x : α), rexp (f x) ∂μ) 0
⊢ Ne (α := ℝ) (∫ (x : α), rexp (f x) ∂μ)⁻¹ 0

Tactic:
simp only [ne_eq, inv_eq_zero]

Premises used: inv_eq_zero, ne_eq
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
hfν : AEMeasurable f ν
h0 : NeZero μ
x : α
hx : ((μ.tilted f).rnDeriv ν x).toReal = (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * (μ.rnDeriv ν x).toReal
hx_pos : 0 < μ.rnDeriv ν x
hx_lt_top : μ.rnDeriv ν x < ∞
⊢ ¬Eq (α := ℝ) (∫ (x : α), rexp (f x) ∂μ) 0

Tactic:
(integral_exp_pos hf).ne'

Premises used: LT.lt.ne', MeasureTheory.integral_exp_pos
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
hfν : AEMeasurable f ν
h0 : NeZero μ
x : α
hx : ((μ.tilted f).rnDeriv ν x).toReal = (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * (μ.rnDeriv ν x).toReal
hx_pos : 0 < μ.rnDeriv ν x
hx_lt_top : μ.rnDeriv ν x < ∞
⊢ ¬Eq (α := ℝ) (∫ (x : α), rexp (f x) ∂μ) 0

Tactic:
exact (integral_exp_pos hf).ne'

Premises used: LT.lt.ne', MeasureTheory.integral_exp_pos
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
hfν : AEMeasurable f ν
h0 : NeZero μ
x : α
hx : ((μ.tilted f).rnDeriv ν x).toReal = (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * (μ.rnDeriv ν x).toReal
hx_pos : 0 < μ.rnDeriv ν x
hx_lt_top : μ.rnDeriv ν x < ∞
h : ¬(rexp (f x) = 0 ∨ Eq (α := ℝ) (∫ (x : α), rexp (f x) ∂μ) 0)
⊢ rexp (f x) / ∫ (x : α), rexp (f x) ∂μ ≠ 0

Tactic:
simp only [ne_eq, div_eq_zero_iff]

Premises used: ne_eq, div_eq_zero_iff
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
hfν : AEMeasurable f ν
h0 : NeZero μ
x : α
hx : ((μ.tilted f).rnDeriv ν x).toReal = (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * (μ.rnDeriv ν x).toReal
hx_pos : 0 < μ.rnDeriv ν x
hx_lt_top : μ.rnDeriv ν x < ∞
h : rexp (f x) ≠ 0 ∧ Ne (α := ℝ) (∫ (x : α), rexp (f x) ∂μ) 0
⊢ ¬(rexp (f x) = 0 ∨ Eq (α := ℝ) (∫ (x : α), rexp (f x) ∂μ) 0)

Tactic:
push Not

Premises used: Not
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
hfν : AEMeasurable f ν
h0 : NeZero μ
x : α
hx : ((μ.tilted f).rnDeriv ν x).toReal = (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * (μ.rnDeriv ν x).toReal
hx_pos : 0 < μ.rnDeriv ν x
hx_lt_top : μ.rnDeriv ν x < ∞
⊢ rexp (f x) ≠ 0 ∧ Ne (α := ℝ) (∫ (x : α), rexp (f x) ∂μ) 0

Tactic:
⟨(exp_pos _).ne', (integral_exp_pos hf).ne'⟩

Premises used: LT.lt.ne', And.intro, MeasureTheory.integral_exp_pos, Real.exp_pos
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
hfν : AEMeasurable f ν
h0 : NeZero μ
x : α
hx : ((μ.tilted f).rnDeriv ν x).toReal = (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * (μ.rnDeriv ν x).toReal
hx_pos : 0 < μ.rnDeriv ν x
hx_lt_top : μ.rnDeriv ν x < ∞
⊢ rexp (f x) ≠ 0 ∧ Ne (α := ℝ) (∫ (x : α), rexp (f x) ∂μ) 0

Tactic:
exact ⟨(exp_pos _).ne', (integral_exp_pos hf).ne'⟩
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
hfν : AEMeasurable f ν
h0 : NeZero μ
x : α
hx : ((μ.tilted f).rnDeriv ν x).toReal = (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * (μ.rnDeriv ν x).toReal
hx_pos : 0 < μ.rnDeriv ν x
hx_lt_top : μ.rnDeriv ν x < ∞
⊢ (μ.rnDeriv ν x).toReal ≠ 0

Tactic:
simp [ENNReal.toReal_eq_zero_iff, hx_lt_top.ne, hx_pos.ne']

Premises used: LT.lt.ne', ENNReal.toReal_eq_zero_iff, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
hfν : AEMeasurable f ν
⊢ μ = 0 ∨ NeZero μ

Tactic:
cases eq_zero_or_neZero μ with
  | inl hμ =>
    simp only [hμ, ae_zero, Filter.EventuallyEq, Filter.eventually_bot]
  | inr h0 =>
    filter_upwards [hμν.ae_le (toReal_rnDeriv_tilted_left μ hfν), Measure.rnDeriv_pos hμν,
      hμν.ae_le (Measure.rnDeriv_lt_top μ ν)] with x hx hx_pos hx_lt_top
    rw [llr, hx, log_mul, div_eq_mul_inv, log_mul (exp_pos _).ne', log_exp, log_inv, llr,
      ← sub_eq_add_neg]
    · simp only [ne_eq, inv_eq_zero]
      exact (integral_exp_pos hf).ne'
    · simp only [ne_eq, div_eq_zero_iff]
      push Not
      exact ⟨(exp_pos _).ne', (integral_exp_pos hf).ne'⟩
    · simp [ENNReal.toReal_eq_zero_iff, hx_lt_top.ne, hx_pos.ne']

Premises used: inv_eq_zero, MeasureTheory.toReal_rnDeriv_tilted_left, Real.log_exp, MeasureTheory.ae_zero, sub_eq_add_neg, MeasureTheory.Measure.rnDeriv_lt_top, MeasureTheory.llr, Filter.EventuallyEq, ne_eq, div_eq_mul_inv, MeasureTheory.Measure.rnDeriv_pos, LT.lt.ne', MeasureTheory.Measure.AbsolutelyContinuous.ae_le, Real.log_inv, div_eq_zero_iff, eq_zero_or_neZero, Not, Real.log_mul, ENNReal.toReal_eq_zero_iff, Real.exp_pos, Filter.eventually_bot
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst : IsFiniteMeasure μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable f μ
h_int : Integrable (llr μ ν) μ
hfμ : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
hfν : AEMeasurable f ν
rw : Integrable (ε := ℝ) (fun (x : α) ↦ f x - log (∫ (z : α), rexp (f z) ∂μ) + llr μ ν x) μ
⊢ Integrable (llr (μ.tilted f) ν) μ

Tactic:
rw [integrable_congr (llr_tilted_left hμν hfμ hfν)]

Premises used: MeasureTheory.integrable_congr, MeasureTheory.llr_tilted_left
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst : IsFiniteMeasure μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable f μ
h_int : Integrable (llr μ ν) μ
hfμ : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
hfν : AEMeasurable f ν
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ f x - log (∫ (z : α), rexp (f z) ∂μ) + llr μ ν x) μ

Tactic:
Integrable.add (hf.sub (integrable_const _)) h_int

Premises used: MeasureTheory.Integrable.sub, MeasureTheory.Integrable.add, MeasureTheory.integrable_const
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst : IsFiniteMeasure μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable f μ
h_int : Integrable (llr μ ν) μ
hfμ : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
hfν : AEMeasurable f ν
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ f x - log (∫ (z : α), rexp (f z) ∂μ) + llr μ ν x) μ

Tactic:
exact Integrable.add (hf.sub (integrable_const _)) h_int

Premises used: MeasureTheory.Integrable.sub, MeasureTheory.Integrable.add, MeasureTheory.integrable_const
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst : IsProbabilityMeasure μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable f μ
h_int : Integrable (llr μ ν) μ
hfμ : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
hfν : AEMeasurable f ν
⊢ Eq (α := ℝ) (∫ (x : α), llr (μ.tilted f) ν x ∂μ) (∫ (x : α), f x - log (∫ (x : α), rexp (f x) ∂μ) + llr μ ν x ∂μ)

Tactic:
integral_congr_ae (llr_tilted_left hμν hfμ hfν)

Premises used: MeasureTheory.integral_congr_ae, MeasureTheory.llr_tilted_left
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst : IsProbabilityMeasure μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable f μ
h_int : Integrable (llr μ ν) μ
hfμ : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
hfν : AEMeasurable f ν
rw :
  HAdd.hAdd (α := ℝ) (∫ (a : α), f a - log (∫ (x : α), rexp (f x) ∂μ) ∂μ) (∫ (a : α), llr μ ν a ∂μ) =
    ∫ (x : α), f x ∂μ - log (∫ (x : α), rexp (f x) ∂μ) + ∫ (x : α), llr μ ν x ∂μ
rw₁ : Integrable (ε := ℝ) (fun (x : α) ↦ f x - log (∫ (x : α), rexp (f x) ∂μ)) μ
⊢ ∫ (x : α), f x - log (∫ (x : α), rexp (f x) ∂μ) + llr μ ν x ∂μ =
    ∫ (x : α), f x ∂μ - log (∫ (x : α), rexp (f x) ∂μ) + ∫ (x : α), llr μ ν x ∂μ

Tactic:
rw [integral_add ?_ h_int]

Premises used: MeasureTheory.integral_add
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst : IsProbabilityMeasure μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable f μ
h_int : Integrable (llr μ ν) μ
hfμ : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
hfν : AEMeasurable f ν
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ f x - log (∫ (x : α), rexp (f x) ∂μ)) μ

Tactic:
hf.sub (integrable_const _)

Premises used: MeasureTheory.Integrable.sub, MeasureTheory.integrable_const
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst : IsProbabilityMeasure μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable f μ
h_int : Integrable (llr μ ν) μ
hfμ : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
hfν : AEMeasurable f ν
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ f x - log (∫ (x : α), rexp (f x) ∂μ)) μ

Tactic:
exact hf.sub (integrable_const _)

Premises used: MeasureTheory.Integrable.sub, MeasureTheory.integrable_const
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst : IsProbabilityMeasure μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable f μ
h_int : Integrable (llr μ ν) μ
hfμ : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
hfν : AEMeasurable f ν
rw :
  HSub.hSub (α := ℝ) (∫ (a : α), f a ∂μ) (∫ (a : α), log (∫ (x : α), rexp (f x) ∂μ) ∂μ) + ∫ (a : α), llr μ ν a ∂μ =
    ∫ (x : α), f x ∂μ - log (∫ (x : α), rexp (f x) ∂μ) + ∫ (x : α), llr μ ν x ∂μ
⊢ HAdd.hAdd (α := ℝ) (∫ (a : α), f a - log (∫ (x : α), rexp (f x) ∂μ) ∂μ) (∫ (a : α), llr μ ν a ∂μ) =
    ∫ (x : α), f x ∂μ - log (∫ (x : α), rexp (f x) ∂μ) + ∫ (x : α), llr μ ν x ∂μ

Tactic:
rw [integral_sub hf (integrable_const _)]

Premises used: MeasureTheory.integral_sub, MeasureTheory.integrable_const
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst : IsProbabilityMeasure μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable f μ
h_int : Integrable (llr μ ν) μ
hfμ : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
hfν : AEMeasurable f ν
⊢ HSub.hSub (α := ℝ) (∫ (a : α), f a ∂μ) (∫ (a : α), log (∫ (x : α), rexp (f x) ∂μ) ∂μ) + ∫ (a : α), llr μ ν a ∂μ =
    ∫ (x : α), f x ∂μ - log (∫ (x : α), rexp (f x) ∂μ) + ∫ (x : α), llr μ ν x ∂μ

Tactic:
simp only [integral_const, probReal_univ, smul_eq_mul, one_mul]

Premises used: MeasureTheory.integral_const, MeasureTheory.probReal_univ, smul_eq_mul, one_mul
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst : IsProbabilityMeasure μ
inst_1 : 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 ∂μ =
    HAdd.hAdd (α := ℝ) (∫ (x : α), llr μ ν x ∂μ) (∫ (x : α), f x ∂μ) - log (∫ (x : α), rexp (f x) ∂μ)

Tactic:
abel
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst : IsProbabilityMeasure μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable f μ
h_int : Integrable (llr μ ν) μ
hfμ : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
hfν : AEMeasurable f ν
calc :
  ∫ (x : α), f x - log (∫ (x : α), rexp (f x) ∂μ) + llr μ ν x ∂μ =
    ∫ (x : α), f x ∂μ - log (∫ (x : α), rexp (f x) ∂μ) + ∫ (x : α), llr μ ν x ∂μ
calc₁ :
  ∫ (x : α), f x ∂μ - log (∫ (x : α), rexp (f x) ∂μ) + ∫ (x : α), llr μ ν x ∂μ =
    HAdd.hAdd (α := ℝ) (∫ (x : α), llr μ ν x ∂μ) (∫ (x : α), f x ∂μ) - log (∫ (x : α), rexp (f x) ∂μ)
⊢ ∫ (x : α), llr (μ.tilted f) ν x ∂μ =
    HAdd.hAdd (α := ℝ) (∫ (x : α), llr μ ν x ∂μ) (∫ (x : α), f x ∂μ) - log (∫ (x : α), rexp (f x) ∂μ)

Tactic:
calc ∫ x, llr (μ.tilted f) ν x ∂μ
    = ∫ x, f x - log (∫ x, exp (f x) ∂μ) + llr μ ν x ∂μ :=
        integral_congr_ae (llr_tilted_left hμν hfμ hfν)
  _ = ∫ x, f x ∂μ - log (∫ x, exp (f x) ∂μ) + ∫ x, llr μ ν x ∂μ := by
        rw [integral_add ?_ h_int]
        swap; · exact hf.sub (integrable_const _)
        rw [integral_sub hf (integrable_const _)]
        simp only [integral_const, probReal_univ, smul_eq_mul, one_mul]
  _ = ∫ x, llr μ ν x ∂μ + ∫ x, f x ∂μ - log (∫ x, exp (f x) ∂μ) := by abel

Premises used: MeasureTheory.integral_congr_ae, Real.exp, Real.log, MeasureTheory.integral, MeasureTheory.llr_tilted_left
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) ν
h : ν = 0
h₁ :
  ∀ (s : Set α),
    MeasurableSet s →
      Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (((0 : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ μ = 0

Tactic:
ext s _
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) ν
h : ν = 0
s : Set α
h_1 : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp [h]
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) ν
h : ν = 0
s : Set α
h_1 : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (((0 : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
exact hμν (by simp [h])
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) ν
h : ν = 0
⊢ μ = 0

Tactic:
have hμ : μ = 0 := by ext s _; exact hμν (by simp [h])