awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LogLikelihoodRatio (goal)
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 ν
⊢ HAdd.hAdd (α := ℝ) (∫ (a : α), f a - log (∫ (x : α), rexp (f x) ∂μ) ∂μ) (∫ (a : α), llr μ ν a ∂μ) =
    ∫ (x : α), f x ∂μ - log (∫ (x : α), rexp (f x) ∂μ) + ∫ (x : α), llr μ ν x ∂μ
have 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 ∂μ
Tactic: rw [integral_sub hf (integrable_const _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LogLikelihoodRatio (goal)
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 : α), llr (μ.tilted f) ν x ∂μ =
    HAdd.hAdd (α := ℝ) (∫ (x : α), llr μ ν x ∂μ) (∫ (x : α), f x ∂μ) - log (∫ (x : α), rexp (f x) ∂μ)
have calc : ∫ (x : α), f x - log (∫ (x : α), rexp (f x) ∂μ) + llr μ ν x ∂μ =
  ∫ (x : α), f x ∂μ - log (∫ (x : α), rexp (f x) ∂μ) + ∫ (x : α), llr μ ν 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LogLikelihoodRatio (goal)
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 ∂μ
⊢ ∫ (x : α), llr (μ.tilted f) ν x ∂μ =
    HAdd.hAdd (α := ℝ) (∫ (x : α), llr μ ν x ∂μ) (∫ (x : α), f x ∂μ) - log (∫ (x : α), rexp (f x) ∂μ)
have 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) ∂μ)
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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LogLikelihoodRatio (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) ν
h : ν = 0
⊢ μ = 0
have h₁ : ∀ (s : Set α),
  MeasurableSet s → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (((0 : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext s _
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LogLikelihoodRatio (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) ν
h : ν = 0
⊢ llr μ (ν.tilted f) =ᶠ[ae μ] fun (x : α) ↦ -f x + log (∫ (z : α), rexp (f z) ∂ν) + llr μ ν x
have hμ : μ = 0
Tactic: have hμ : μ = 0 := by ext s _; exact hμν (by simp [h])
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LogLikelihoodRatio (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) ν
h0 : NeZero ν
⊢ llr μ (ν.tilted f) =ᶠ[ae μ] fun (x : α) ↦ -f x + log (∫ (z : α), rexp (f z) ∂ν) + llr μ ν x
have 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
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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LogLikelihoodRatio (goal)
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 < ∞
⊢ llr μ (ν.tilted f) x = -f x + log (∫ (z : α), rexp (f z) ∂ν) + llr μ ν x
have h : Ne (α := ℝ) (∫ (x : α), rexp (f x) ∂ν) 0
Tactic: rw [llr, hx, log_mul, log_mul (exp_pos _).ne', log_exp, llr]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LogLikelihoodRatio (goal)
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
⊢ llr μ (ν.tilted f) x = -f x + log (∫ (z : α), rexp (f z) ∂ν) + llr μ ν x
have h₁ : rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν ≠ 0
Tactic: rw [llr, hx, log_mul, log_mul (exp_pos _).ne', log_exp, llr]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LogLikelihoodRatio (goal)
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
⊢ llr μ (ν.tilted f) x = -f x + log (∫ (z : α), rexp (f z) ∂ν) + llr μ ν x
have h₂ : (μ.rnDeriv ν x).toReal ≠ 0
Tactic: rw [llr, hx, log_mul, log_mul (exp_pos _).ne', log_exp, llr]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LogLikelihoodRatio (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) ν
⊢ llr μ (ν.tilted f) =ᶠ[ae μ] fun (x : α) ↦ -f x + log (∫ (z : α), rexp (f z) ∂ν) + llr μ ν x
have 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']
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LogLikelihoodRatio (goal)
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 (llr μ (ν.tilted f)) μ
have rw : Integrable (ε := ℝ) (fun (x : α) ↦ -f x + log (∫ (z : α), rexp (f z) ∂ν) + llr μ ν x) μ
Tactic: rw [integrable_congr (llr_tilted_right hμν hfν)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LogLikelihoodRatio (goal)
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) ∂ν) + llr μ ν x ∂μ =
    -∫ (x : α), f x ∂μ + log (∫ (x : α), rexp (f x) ∂ν) + ∫ (x : α), llr μ ν x ∂μ
have 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 ∂μ
Tactic: rw [← integral_neg, integral_add ?_ h_int]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LogLikelihoodRatio (goal)
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 ∂μ
⊢ ∫ (x : α), -f x + log (∫ (x : α), rexp (f x) ∂ν) + llr μ ν x ∂μ =
    -∫ (x : α), f x ∂μ + log (∫ (x : α), rexp (f x) ∂ν) + ∫ (x : α), llr μ ν x ∂μ
have rw₁ : Integrable (ε := ℝ) (fun (x : α) ↦ -f x + log (∫ (x : α), rexp (f x) ∂ν)) μ
Tactic: rw [← integral_neg, integral_add ?_ h_int]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LogLikelihoodRatio (goal)
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 + log (∫ (x : α), rexp (f x) ∂ν) ∂μ) (∫ (a : α), llr μ ν a ∂μ) =
    ∫ (a : α), -f a ∂μ + log (∫ (x : α), rexp (f x) ∂ν) + ∫ (x : α), llr μ ν x ∂μ
have 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 ∂μ
Tactic: rw [integral_add ?_ (integrable_const _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LogLikelihoodRatio (goal)
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 ∂μ
⊢ HAdd.hAdd (α := ℝ) (∫ (a : α), -f a + log (∫ (x : α), rexp (f x) ∂ν) ∂μ) (∫ (a : α), llr μ ν a ∂μ) =
    ∫ (a : α), -f a ∂μ + log (∫ (x : α), rexp (f x) ∂ν) + ∫ (x : α), llr μ ν x ∂μ
have rw₁ : Integrable (ε := ℝ) (fun (a : α) ↦ -f a) μ
Tactic: rw [integral_add ?_ (integrable_const _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LogLikelihoodRatio (goal)
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 : α), llr μ (ν.tilted f) x ∂μ =
    HSub.hSub (α := ℝ) (∫ (x : α), llr μ ν x ∂μ) (∫ (x : α), f x ∂μ) + log (∫ (x : α), rexp (f x) ∂ν)
have calc : ∫ (x : α), -f x + log (∫ (x : α), rexp (f x) ∂ν) + llr μ ν x ∂μ =
  -∫ (x : α), f x ∂μ + log (∫ (x : α), rexp (f x) ∂ν) + ∫ (x : α), llr μ ν 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LogLikelihoodRatio (goal)
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 ∂μ
⊢ ∫ (x : α), llr μ (ν.tilted f) x ∂μ =
    HSub.hSub (α := ℝ) (∫ (x : α), llr μ ν x ∂μ) (∫ (x : α), f x ∂μ) + log (∫ (x : α), rexp (f x) ∂ν)
have 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) ∂ν)
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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Map (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f g : α → β
hf : Measurable f
hg : Measurable g
h : f =ᶠ[ae μ] g
⊢ 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 β)
have 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∞)
Tactic: ext1 s hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Map (goal)
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 f μ : Measure β)
have 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 sorry) : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ≥0∞) (Measure α) (Measure β)) :
        (a : Measure α) → Measure β)
      μ :
    Measure β)
Tactic: simp only [← mapₗ_mk_apply_of_aemeasurable hf.aemeasurable]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Map (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
⊢ Eq (α := Measure β) (map f 0) 0
have pos : ∀ (hf : AEMeasurable (_m := mα) f 0), Eq (α := Measure β) (map f 0) 0
Tactic: by_cases hf : AEMeasurable f (0 : Measure α)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Map (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
pos : ∀ (hf : AEMeasurable (_m := mα) f 0), Eq (α := Measure β) (map f 0) 0
⊢ Eq (α := Measure β) (map f 0) 0
have neg : ∀ (hf : ¬AEMeasurable (_m := mα) f 0), Eq (α := Measure β) (map f 0) 0
Tactic: by_cases hf : AEMeasurable f (0 : Measure α)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Map (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f g : α → β
h : f =ᶠ[ae μ] g
⊢ Eq (α := Measure β) (map f μ) (map g μ)
have pos : ∀ (hf : AEMeasurable f μ), Eq (α := Measure β) (map f μ) (map g μ)
Tactic: by_cases hf : AEMeasurable f μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Map (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f g : α → β
h : f =ᶠ[ae μ] g
pos : ∀ (hf : AEMeasurable f μ), Eq (α := Measure β) (map f μ) (map g μ)
⊢ Eq (α := Measure β) (map f μ) (map g μ)
have neg : ∀ (hf : ¬AEMeasurable f μ), Eq (α := Measure β) (map f μ) (map g μ)
Tactic: by_cases hf : AEMeasurable f μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Map (hypothesis)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f g : α → β
h : f =ᶠ[ae μ] g
hf : AEMeasurable f μ
⊢ Eq (α := Measure β) (map f μ) (map g μ)
have hg : AEMeasurable g μ
Tactic: have hg : AEMeasurable g μ := hf.congr h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Map (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f g : α → β
h : f =ᶠ[ae μ] g
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ Eq (α := Measure β) (map f μ) (map g μ)
have pos : 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ₗ (AEMeasurable.mk g hg) : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ≥0∞) (Measure α) (Measure β)) :
        (a : Measure α) → Measure β)
      μ :
    Measure β)
Tactic: simp only [← mapₗ_mk_apply_of_aemeasurable hf, ← mapₗ_mk_apply_of_aemeasurable hg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Map (hypothesis)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f g : α → β
h : f =ᶠ[ae μ] g
hf : ¬AEMeasurable f μ
⊢ Eq (α := Measure β) (map f μ) (map g μ)
have hg : ¬AEMeasurable g μ
Tactic: have hg : ¬AEMeasurable g μ := by simpa [← aemeasurable_congr h] using hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Map (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
R : Type u_4
inst : SMul R ℝ≥0∞
inst_1 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
c : R
μ : Measure α
f : α → β
⊢ map f (c • μ) = HSMul.hSMul (β := Measure β) c (map f μ)
have suffices : ∀ (c : ℝ≥0∞), map f (c • μ) = HSMul.hSMul (β := Measure β) c (map f μ)
Tactic: suffices ∀ c : ℝ≥0∞, (c • μ).map f = c • μ.map f by simpa using this (c • 1)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Map (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
R : Type u_4
inst : SMul R ℝ≥0∞
inst_1 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
μ : Measure α
f : α → β
c : ℝ≥0∞
⊢ map f (c • μ) = HSMul.hSMul (β := Measure β) c (map f μ)
have inl : map f (HSMul.hSMul (α := ℝ≥0∞) 0 μ) = HSMul.hSMul (α := ℝ≥0∞) (β := Measure β) 0 (map f μ)
Tactic: rcases eq_or_ne c 0 with (rfl | hc)
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Map (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
R : Type u_4
inst : SMul R ℝ≥0∞
inst_1 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
μ : Measure α
f : α → β
c : ℝ≥0∞
inl : map f (HSMul.hSMul (α := ℝ≥0∞) 0 μ) = HSMul.hSMul (α := ℝ≥0∞) (β := Measure β) 0 (map f μ)
⊢ map f (c • μ) = HSMul.hSMul (β := Measure β) c (map f μ)
have inr : ∀ (hc : c ≠ 0), map f (c • μ) = HSMul.hSMul (β := Measure β) c (map f μ)
Tactic: rcases eq_or_ne c 0 with (rfl | hc)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Map (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
R : Type u_4
inst : SMul R ℝ≥0∞
inst_1 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
μ : Measure α
f : α → β
c : ℝ≥0∞
hc : c ≠ 0
⊢ map f (c • μ) = HSMul.hSMul (β := Measure β) c (map f μ)
have pos : ∀ (hf : AEMeasurable f μ), map f (c • μ) = HSMul.hSMul (β := Measure β) c (map f μ)
Tactic: by_cases hf : AEMeasurable f μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Map (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
R : Type u_4
inst : SMul R ℝ≥0∞
inst_1 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
μ : Measure α
f : α → β
c : ℝ≥0∞
hc : c ≠ 0
pos : ∀ (hf : AEMeasurable f μ), map f (c • μ) = HSMul.hSMul (β := Measure β) c (map f μ)
⊢ map f (c • μ) = HSMul.hSMul (β := Measure β) c (map f μ)
have neg : ∀ (hf : ¬AEMeasurable f μ), map f (c • μ) = HSMul.hSMul (β := Measure β) c (map f μ)
Tactic: by_cases hf : AEMeasurable f μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Map (hypothesis)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
R : Type u_4
inst : SMul R ℝ≥0∞
inst_1 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
μ : Measure α
f : α → β
c : ℝ≥0∞
hc : c ≠ 0
hf : AEMeasurable f μ
⊢ map f (c • μ) = HSMul.hSMul (β := Measure β) c (map f μ)
have hfc : AEMeasurable f (c • μ)
Tactic: have hfc : AEMeasurable f (c • μ) :=
      ⟨hf.mk f, hf.measurable_mk, (ae_ennreal_smul_measure_iff hc).2 hf.ae_eq_mk⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Map (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
R : Type u_4
inst : SMul R ℝ≥0∞
inst_1 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
μ : Measure α
f : α → β
c : ℝ≥0∞
hc : c ≠ 0
hf : AEMeasurable f μ
hfc : AEMeasurable f (c • μ)
⊢ map f (c • μ) = HSMul.hSMul (β := Measure β) c (map f μ)
have pos : HSMul.hSMul (β := Measure β) c
    (((mapₗ (AEMeasurable.mk f hfc) : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ≥0∞) (Measure α) (Measure β)) :
          (a : Measure α) → Measure β)
        μ :
      Measure β) =
  HSMul.hSMul (β := Measure β) c
    (((mapₗ (AEMeasurable.mk f hf) : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ≥0∞) (Measure α) (Measure β)) :
          (a : Measure α) → Measure β)
        μ :
      Measure β)
Tactic: simp only [← mapₗ_mk_apply_of_aemeasurable hf, ← mapₗ_mk_apply_of_aemeasurable hfc, map_smulₛₗ,
      RingHom.id_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Map (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
R : Type u_4
inst : SMul R ℝ≥0∞
inst_1 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
μ : Measure α
f : α → β
c : ℝ≥0∞
hc : c ≠ 0
hf : AEMeasurable f μ
hfc : AEMeasurable f (c • μ)
⊢ HSMul.hSMul (β := Measure β) c
      (((mapₗ (AEMeasurable.mk f hfc) : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ≥0∞) (Measure α) (Measure β)) :
            (a : Measure α) → Measure β)
          μ :
        Measure β) =
    HSMul.hSMul (β := Measure β) c
      (((mapₗ (AEMeasurable.mk f hf) : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ≥0∞) (Measure α) (Measure β)) :
            (a : Measure α) → Measure β)
          μ :
        Measure β)
have pos : Eq.{u_2 + 1} (α := Measure β)
  (((mapₗ (AEMeasurable.mk f hfc) : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ≥0∞) (Measure α) (Measure β)) :
        (a : Measure α) → Measure β)
      μ :
    Measure β)
  (((mapₗ (AEMeasurable.mk f hf) : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ≥0∞) (Measure α) (Measure β)) :
        (a : Measure α) → Measure β)
      μ :
    Measure β)
Tactic: congr 1