awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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μ : μ = 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)) ν
h0 : NeZero ν
h :
  ∀ (x : α) (hx : (μ.rnDeriv (ν.tilted f) 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_right μ ν hf), Measure.rnDeriv_pos hμν,
      hμν.ae_le (Measure.rnDeriv_lt_top μ ν)] with x hx hx_pos hx_lt_top

Premises used: MeasureTheory.Measure.rnDeriv_lt_top, MeasureTheory.Measure.rnDeriv_pos, MeasureTheory.Measure.AbsolutelyContinuous.ae_le, MeasureTheory.toReal_rnDeriv_tilted_right
-- 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)) ν
h0 : NeZero ν
x : α
hx : (μ.rnDeriv (ν.tilted f) 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, log_mul (exp_pos _).ne', log_exp, llr]

Premises used: Real.log_exp, MeasureTheory.llr, LT.lt.ne', 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)) ν
h0 : NeZero ν
x : α
hx : (μ.rnDeriv (ν.tilted f) x).toReal = (rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν) * (μ.rnDeriv ν x).toReal
hx_pos : 0 < μ.rnDeriv ν x
hx_lt_top : μ.rnDeriv ν x < ∞
⊢ Ne (α := ℝ) (∫ (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)) ν
h0 : NeZero ν
x : α
hx : (μ.rnDeriv (ν.tilted f) x).toReal = (rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν) * (μ.rnDeriv ν x).toReal
hx_pos : 0 < μ.rnDeriv ν x
hx_lt_top : μ.rnDeriv ν x < ∞
⊢ Ne (α := ℝ) (∫ (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)) ν
h0 : NeZero ν
x : α
hx : (μ.rnDeriv (ν.tilted f) 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) * ∫ (x : α), rexp (f x) ∂ν ≠ 0

Tactic:
(mul_pos (exp_pos _) (integral_exp_pos hf)).ne'

Premises used: LT.lt.ne', mul_pos, 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)) ν
h0 : NeZero ν
x : α
hx : (μ.rnDeriv (ν.tilted f) 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) * ∫ (x : α), rexp (f x) ∂ν ≠ 0

Tactic:
refine (mul_pos (exp_pos _) (integral_exp_pos hf)).ne'

Premises used: LT.lt.ne', mul_pos, 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)) ν
h0 : NeZero ν
x : α
hx : (μ.rnDeriv (ν.tilted f) 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)) ν
⊢ ν = 0 ∨ NeZero ν

Tactic:
cases eq_zero_or_neZero ν with
  | inl h =>
    have hμ : μ = 0 := by ext s _; exact hμν (by simp [h])
    simp only [hμ, ae_zero, Filter.EventuallyEq, Filter.eventually_bot]
  | inr h0 =>
    filter_upwards [hμν.ae_le (toReal_rnDeriv_tilted_right μ ν 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, log_mul (exp_pos _).ne', log_exp, llr]
    · exact (integral_exp_pos hf).ne'
    · refine (mul_pos (exp_pos _) (integral_exp_pos hf)).ne'
    · simp [ENNReal.toReal_eq_zero_iff, hx_lt_top.ne, hx_pos.ne']

Premises used: Real.log_exp, MeasureTheory.ae_zero, MeasureTheory.Measure.rnDeriv_lt_top, MeasureTheory.llr, Filter.EventuallyEq, MeasureTheory.Measure.rnDeriv_pos, LT.lt.ne', MeasureTheory.Measure.AbsolutelyContinuous.ae_le, eq_zero_or_neZero, Real.log_mul, ENNReal.toReal_eq_zero_iff, MeasureTheory.toReal_rnDeriv_tilted_right, 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)) ν
rw : Integrable (ε := ℝ) (fun (x : α) ↦ -f x + log (∫ (z : α), rexp (f z) ∂ν) + llr μ ν x) μ
⊢ Integrable (llr μ (ν.tilted f)) μ

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

Premises used: MeasureTheory.integrable_congr, MeasureTheory.llr_tilted_right
-- 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)) ν
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ -f x + log (∫ (z : α), rexp (f z) ∂ν) + llr μ ν x) μ

Tactic:
Integrable.add (hfμ.neg.add (integrable_const _)) h_int

Premises used: MeasureTheory.Integrable.neg, 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)) ν
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ -f x + log (∫ (z : α), rexp (f z) ∂ν) + llr μ ν x) μ

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

Premises used: MeasureTheory.Integrable.neg, 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 μ
hfν : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) ν
h_int : Integrable (llr μ ν) μ
⊢ Eq (α := ℝ) (∫ (x : α), llr μ (ν.tilted f) x ∂μ) (∫ (x : α), -f x + log (∫ (x : α), rexp (f x) ∂ν) + llr μ ν x ∂μ)

Tactic:
integral_congr_ae (llr_tilted_right hμν hfν)

Premises used: MeasureTheory.integral_congr_ae, MeasureTheory.llr_tilted_right
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst : IsProbabilityMeasure μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hfμ : Integrable f μ
hfν : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) ν
h_int : Integrable (llr μ ν) μ
rw :
  HAdd.hAdd (α := ℝ) (∫ (a : α), -f a + log (∫ (x : α), rexp (f x) ∂ν) ∂μ) (∫ (a : α), llr μ ν a ∂μ) =
    ∫ (a : α), -f a ∂μ + 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_neg, integral_add ?_ h_int]

Premises used: MeasureTheory.integral_neg, 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 μ
hfν : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) ν
h_int : Integrable (llr μ ν) μ
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ -f x + log (∫ (x : α), rexp (f x) ∂ν)) μ

Tactic:
hfμ.neg.add (integrable_const _)

Premises used: MeasureTheory.Integrable.neg, 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 μ
hfν : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) ν
h_int : Integrable (llr μ ν) μ
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ -f x + log (∫ (x : α), rexp (f x) ∂ν)) μ

Tactic:
exact hfμ.neg.add (integrable_const _)

Premises used: MeasureTheory.Integrable.neg, 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 μ
hfν : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) ν
h_int : Integrable (llr μ ν) μ
rw :
  HAdd.hAdd (α := ℝ) (∫ (a : α), -f a ∂μ) (∫ (a : α), log (∫ (x : α), rexp (f x) ∂ν) ∂μ) + ∫ (a : α), llr μ ν a ∂μ =
    ∫ (a : α), -f a ∂μ + log (∫ (x : α), rexp (f x) ∂ν) + ∫ (x : α), llr μ ν x ∂μ
rw₁ : Integrable (ε := ℝ) (fun (a : α) ↦ -f a) μ
⊢ HAdd.hAdd (α := ℝ) (∫ (a : α), -f a + log (∫ (x : α), rexp (f x) ∂ν) ∂μ) (∫ (a : α), llr μ ν a ∂μ) =
    ∫ (a : α), -f a ∂μ + log (∫ (x : α), rexp (f x) ∂ν) + ∫ (x : α), llr μ ν x ∂μ

Tactic:
rw [integral_add ?_ (integrable_const _)]

Premises used: MeasureTheory.integrable_const, 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 μ
hfν : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) ν
h_int : Integrable (llr μ ν) μ
⊢ Integrable (ε := ℝ) (fun (a : α) ↦ -f a) μ

Tactic:
hfμ.neg

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

Tactic:
exact hfμ.neg

Premises used: MeasureTheory.Integrable.neg
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst : IsProbabilityMeasure μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hfμ : Integrable f μ
hfν : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) ν
h_int : Integrable (llr μ ν) μ
⊢ HAdd.hAdd (α := ℝ) (∫ (a : α), -f a ∂μ) (∫ (a : α), log (∫ (x : α), rexp (f x) ∂ν) ∂μ) + ∫ (a : α), llr μ ν a ∂μ =
    ∫ (a : α), -f a ∂μ + 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 μ
hfν : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) ν
h_int : Integrable (llr μ ν) μ
⊢ -∫ (x : α), f x ∂μ + log (∫ (x : α), rexp (f x) ∂ν) + ∫ (x : α), llr μ ν x ∂μ =
    HSub.hSub (α := ℝ) (∫ (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 μ
hfν : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) ν
h_int : Integrable (llr μ ν) μ
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 ∂μ =
    HSub.hSub (α := ℝ) (∫ (x : α), llr μ ν x ∂μ) (∫ (x : α), f x ∂μ) + log (∫ (x : α), rexp (f x) ∂ν)
⊢ ∫ (x : α), llr μ (ν.tilted f) x ∂μ =
    HSub.hSub (α := ℝ) (∫ (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_right hμν hfν)
  _ = -∫ x, f x ∂μ + log (∫ x, exp (f x) ∂ν) + ∫ x, llr μ ν x ∂μ := by
        rw [← integral_neg, integral_add ?_ h_int]
        swap; · exact hfμ.neg.add (integrable_const _)
        rw [integral_add ?_ (integrable_const _)]
        swap; · exact hfμ.neg
        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, MeasureTheory.llr_tilted_right, Real.exp, Real.log, MeasureTheory.integral
-- Module: Mathlib.MeasureTheory.Measure.Map
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν : Measure α
s_1 : Set α
inst : MeasurableSpace β
f : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ≥0∞) (OuterMeasure α) (OuterMeasure β)
hf : ∀ (μ : Measure α), inst ≤ OuterMeasure.caratheodory ((f : (a : OuterMeasure α) → OuterMeasure β) μ.toOuterMeasure)
μ₁ μ₂ : Measure α
s : Set β
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞)
    ((OuterMeasure.toMeasure ((f : (a : OuterMeasure α) → OuterMeasure β) (μ₁ + μ₂).toOuterMeasure) ⋯ :
          (a : Set β) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((OuterMeasure.toMeasure ((f : (a : OuterMeasure α) → OuterMeasure β) μ₁.toOuterMeasure) ⋯ +
            OuterMeasure.toMeasure ((f : (a : OuterMeasure α) → OuterMeasure β) μ₂.toOuterMeasure) ⋯ :
          (a : Set β) → ℝ≥0∞)
        s :
      ℝ≥0∞)

Tactic:
simp only [map_add, coe_add, Pi.add_apply, toMeasure_apply, add_toOuterMeasure,
      OuterMeasure.coe_add, hs]

Premises used: MeasureTheory.OuterMeasure.coe_add, map_add, MeasureTheory.Measure.coe_add, Pi.add_apply, MeasureTheory.toMeasure_apply, MeasureTheory.Measure.add_toOuterMeasure
-- Module: Mathlib.MeasureTheory.Measure.Map
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ_1 ν : Measure α
s_1 : Set α
inst : MeasurableSpace β
f : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ≥0∞) (OuterMeasure α) (OuterMeasure β)
hf : ∀ (μ : Measure α), inst ≤ OuterMeasure.caratheodory ((f : (a : OuterMeasure α) → OuterMeasure β) μ.toOuterMeasure)
c : ℝ≥0∞
μ : Measure α
s : Set β
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞)
    ((OuterMeasure.toMeasure ((f : (a : OuterMeasure α) → OuterMeasure β) (c • μ).toOuterMeasure) ⋯ :
          (a : Set β) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((HSMul.hSMul (α := ℝ≥0∞) ((RingHom.id ℝ≥0∞ : (a : ℝ≥0∞) → ℝ≥0∞) c : ℝ≥0∞)
            (OuterMeasure.toMeasure ((f : (a : OuterMeasure α) → OuterMeasure β) μ.toOuterMeasure) ⋯) :
          (a : Set β) → ℝ≥0∞)
        s :
      ℝ≥0∞)

Tactic:
simp only [map_smulₛₗ, Pi.smul_apply, toMeasure_apply, smul_toOuterMeasure (R := ℝ≥0∞),
      OuterMeasure.coe_smul (R := ℝ≥0∞), smul_apply, hs]

Premises used: MeasureTheory.Measure.smul_toOuterMeasure, MulActionSemiHomClass.map_smulₛₗ, MeasureTheory.Measure.smul_apply, MeasureTheory.toMeasure_apply, MeasureTheory.OuterMeasure.coe_smul, Pi.smul_apply
-- Module: Mathlib.MeasureTheory.Measure.Map
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ≥0∞) (OuterMeasure α) (OuterMeasure β)
hf : ∀ (μ : Measure α), mβ ≤ OuterMeasure.caratheodory ((f : (a : OuterMeasure α) → OuterMeasure β) μ.toOuterMeasure)
s : Set β
hs : NullMeasurableSet s ((liftLinear f hf : (a : Measure α) → Measure β) μ)
⊢ Eq (α := ℝ≥0∞) ((((liftLinear f hf : (a : Measure α) → Measure β) μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((f : (a : OuterMeasure α) → OuterMeasure β) μ.toOuterMeasure : OuterMeasure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
toMeasure_apply₀ _ (hf μ) hs

Premises used: MeasureTheory.toMeasure_apply₀
-- Module: Mathlib.MeasureTheory.Measure.Map
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ≥0∞) (OuterMeasure α) (OuterMeasure β)
hf : ∀ (μ : Measure α), mβ ≤ OuterMeasure.caratheodory ((f : (a : OuterMeasure α) → OuterMeasure β) μ.toOuterMeasure)
s : Set β
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((((liftLinear f hf : (a : Measure α) → Measure β) μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((f : (a : OuterMeasure α) → OuterMeasure β) μ.toOuterMeasure : OuterMeasure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
toMeasure_apply _ (hf μ) hs

Premises used: MeasureTheory.toMeasure_apply
-- Module: Mathlib.MeasureTheory.Measure.Map
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ≥0∞) (OuterMeasure α) (OuterMeasure β)
hf : ∀ (μ : Measure α), mβ ≤ OuterMeasure.caratheodory ((f : (a : OuterMeasure α) → OuterMeasure β) μ.toOuterMeasure)
s : Set β
⊢ LE.le (α := ℝ≥0∞)
    ((((f : (a : OuterMeasure α) → OuterMeasure β) μ.toOuterMeasure : OuterMeasure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((liftLinear f hf : (a : Measure α) → Measure β) μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
le_toMeasure_apply _ (hf μ) s

Premises used: MeasureTheory.le_toMeasure_apply
-- Module: Mathlib.MeasureTheory.Measure.Map
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f g : α → β
hf : Measurable f
hg : Measurable g
h : f =ᶠ[ae μ] g
h₁ :
  ∀ (s : Set β) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞)
      (((((mapₗ f : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ≥0∞) (Measure α) (Measure β)) : (a : Measure α) → Measure β)
                μ :
              Measure β) :
            (a : Set β) → ℝ≥0∞)
          s :
        ℝ≥0∞)
      (((((mapₗ g : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ≥0∞) (Measure α) (Measure β)) : (a : Measure α) → Measure β)
                μ :
              Measure β) :
            (a : Set β) → ℝ≥0∞)
          s :
        ℝ≥0∞)
⊢ Eq.{u_2 + 1} (α := Measure β)
    (((mapₗ f : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ≥0∞) (Measure α) (Measure β)) : (a : Measure α) → Measure β) μ :
      Measure β)
    (((mapₗ g : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ≥0∞) (Measure α) (Measure β)) : (a : Measure α) → Measure β) μ :
      Measure β)

Tactic:
ext1 s hs
-- Module: Mathlib.MeasureTheory.Measure.Map
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f g : α → β
hf : Measurable f
hg : Measurable g
h : f =ᶠ[ae μ] g
s : Set β
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞)
    (((((mapₗ f : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ≥0∞) (Measure α) (Measure β)) : (a : Measure α) → Measure β)
              μ :
            Measure β) :
          (a : Set β) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    (((((mapₗ g : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ≥0∞) (Measure α) (Measure β)) : (a : Measure α) → Measure β)
              μ :
            Measure β) :
          (a : Set β) → ℝ≥0∞)
        s :
      ℝ≥0∞)

Tactic:
simpa only [mapₗ, hf, hg, hs, dif_pos, liftLinear_apply, OuterMeasure.map_apply]
    using measure_congr (h.preimage s)

Premises used: MeasureTheory.Measure.mapₗ, MeasureTheory.measure_congr, MeasureTheory.OuterMeasure.map_apply, dif_pos, Filter.EventuallyEq.preimage, MeasureTheory.Measure.liftLinear_apply
-- Module: Mathlib.MeasureTheory.Measure.Map
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : AEMeasurable f μ
⊢ Eq.{u_2 + 1} (α := Measure β)
    (((mapₗ (AEMeasurable.mk f hf) : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ≥0∞) (Measure α) (Measure β)) :
          (a : Measure α) → Measure β)
        μ :
      Measure β)
    (map f μ : Measure β)

Tactic:
simp [map, hf]

Premises used: MeasureTheory.Measure.map
-- Module: Mathlib.MeasureTheory.Measure.Map
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
μ : Measure α
simp :
  Eq.{u_2 + 1} (α := Measure β)
    (((mapₗ f : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ≥0∞) (Measure α) (Measure β)) : (a : Measure α) → Measure β) μ :
      Measure β)
    (((mapₗ (AEMeasurable.mk (μ := μ) f ⋯) : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ≥0∞) (Measure α) (Measure β)) :
          (a : Measure α) → Measure β)
        μ :
      Measure β)
⊢ Eq.{u_2 + 1} (α := Measure β)
    (((mapₗ f : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ≥0∞) (Measure α) (Measure β)) : (a : Measure α) → Measure β) μ :
      Measure β)
    (map f μ : Measure β)

Tactic:
simp only [← mapₗ_mk_apply_of_aemeasurable hf.aemeasurable]

Premises used: Measurable.aemeasurable, MeasureTheory.Measure.mapₗ_mk_apply_of_aemeasurable
-- Module: Mathlib.MeasureTheory.Measure.Map
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
μ : Measure α
⊢ Eq.{u_2 + 1} (α := Measure β)
    (((mapₗ f : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ≥0∞) (Measure α) (Measure β)) : (a : Measure α) → Measure β) μ :
      Measure β)
    (((mapₗ (AEMeasurable.mk (μ := μ) f ⋯) : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ≥0∞) (Measure α) (Measure β)) :
          (a : Measure α) → Measure β)
        μ :
      Measure β)

Tactic:
mapₗ_congr hf hf.aemeasurable.measurable_mk hf.aemeasurable.ae_eq_mk

Premises used: Measurable.aemeasurable, MeasureTheory.Measure.mapₗ_congr, AEMeasurable.ae_eq_mk, AEMeasurable.measurable_mk
-- Module: Mathlib.MeasureTheory.Measure.Map
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
μ : Measure α
⊢ Eq.{u_2 + 1} (α := Measure β)
    (((mapₗ f : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ≥0∞) (Measure α) (Measure β)) : (a : Measure α) → Measure β) μ :
      Measure β)
    (((mapₗ (AEMeasurable.mk (μ := μ) f ⋯) : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ≥0∞) (Measure α) (Measure β)) :
          (a : Measure α) → Measure β)
        μ :
      Measure β)

Tactic:
exact mapₗ_congr hf hf.aemeasurable.measurable_mk hf.aemeasurable.ae_eq_mk

Premises used: Measurable.aemeasurable, MeasureTheory.Measure.mapₗ_congr, AEMeasurable.ae_eq_mk, AEMeasurable.measurable_mk