awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
g : α → ℝ
h0 : NeZero μ
s : Set α
hs : MeasurableSet s
inr :
  ∫⁻ (x : α) in s,
      ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) *
        ENNReal.ofReal (rexp (g x) / ∫ (x : α), rexp (g x) ∂μ.tilted f) ∂μ =
    ∫⁻ (a : α) in s, ENNReal.ofReal (rexp ((f + g) a) / ∫ (x : α), rexp ((f + g) x) ∂μ) ∂μ
⊢ Eq (α := ℝ≥0∞) (((μ.tilted f).tilted g : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((μ.tilted (f + g) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [tilted_apply' _ _ hs, tilted_apply' _ _ hs, setLIntegral_tilted' f _ hs]

Premises used: MeasureTheory.setLIntegral_tilted', MeasureTheory.tilted_apply'
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
g : α → ℝ
h0 : NeZero μ
s : Set α
hs : MeasurableSet s
inr :
  ∀ (x : α),
    ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) *
        ENNReal.ofReal (rexp (g x) / ∫ (x : α), rexp (g x) ∂μ.tilted f) =
      ENNReal.ofReal (rexp ((f + g) x) / ∫ (x : α), rexp ((f + g) x) ∂μ)
⊢ ∫⁻ (x : α) in s,
      ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) *
        ENNReal.ofReal (rexp (g x) / ∫ (x : α), rexp (g x) ∂μ.tilted f) ∂μ =
    ∫⁻ (a : α) in s, ENNReal.ofReal (rexp ((f + g) a) / ∫ (x : α), rexp ((f + g) x) ∂μ) ∂μ

Tactic:
congr with x
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
g : α → ℝ
h0 : NeZero μ
s : Set α
hs : MeasurableSet s
x : α
⊢ 0 ≤ rexp (f x) / ∫ (x : α), rexp (f x) ∂μ

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
g : α → ℝ
h0 : NeZero μ
s : Set α
hs : MeasurableSet s
x : α
inr :
  ENNReal.ofReal
      ((rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) *
        (rexp (g x) / HDiv.hDiv (α := ℝ) (∫ (x : α), rexp ((f + g) x) ∂μ) (∫ (x : α), rexp (f x) ∂μ))) =
    ENNReal.ofReal (rexp (f x) * rexp (g x) / ∫ (x : α), rexp ((f + g) x) ∂μ)
⊢ ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) *
      ENNReal.ofReal (rexp (g x) / ∫ (x : α), rexp (g x) ∂μ.tilted f) =
    ENNReal.ofReal (rexp ((f + g) x) / ∫ (x : α), rexp ((f + g) x) ∂μ)

Tactic:
rw [← ENNReal.ofReal_mul (by positivity),
      integral_exp_tilted f, Pi.add_apply, exp_add]

Premises used: ENNReal.ofReal_mul, MeasureTheory.integral_exp_tilted, Pi.add_apply, Real.exp_add
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
g : α → ℝ
h0 : NeZero μ
s : Set α
hs : MeasurableSet s
x : α
inr :
  (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) *
      (rexp (g x) / HDiv.hDiv (α := ℝ) (∫ (x : α), rexp ((f + g) x) ∂μ) (∫ (x : α), rexp (f x) ∂μ)) =
    rexp (f x) * rexp (g x) / ∫ (x : α), rexp ((f + g) x) ∂μ
⊢ ENNReal.ofReal
      ((rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) *
        (rexp (g x) / HDiv.hDiv (α := ℝ) (∫ (x : α), rexp ((f + g) x) ∂μ) (∫ (x : α), rexp (f x) ∂μ))) =
    ENNReal.ofReal (rexp (f x) * rexp (g x) / ∫ (x : α), rexp ((f + g) x) ∂μ)

Tactic:
congr 1
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
g : α → ℝ
h0 : NeZero μ
s : Set α
hs : MeasurableSet s
x : α
⊢ Ne (α := ℝ) (∫ (x : α), rexp (f x) ∂μ) 0

Tactic:
have := (integral_exp_pos hf).ne'
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
g : α → ℝ
h0 : NeZero μ
s : Set α
hs : MeasurableSet s
x : α
this : Ne (α := ℝ) (∫ (x : α), rexp (f x) ∂μ) 0
⊢ (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) *
      (rexp (g x) / HDiv.hDiv (α := ℝ) (∫ (x : α), rexp (f x + g x) ∂μ) (∫ (x : α), rexp (f x) ∂μ)) =
    rexp (f x) * rexp (g x) / ∫ (x : α), rexp (f x + g x) ∂μ

Tactic:
simp [field]
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
g : α → ℝ
⊢ μ = 0 ∨ NeZero μ

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

Premises used: ENNReal.ofReal_mul, MeasureTheory.integral_exp_tilted, Pi.add_apply, eq_zero_or_neZero, Real.exp_add
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
g : α → ℝ
hg : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (g x)) μ
rw : μ.tilted (f + g) = (μ.tilted g).tilted f
rw₁ : μ.tilted (g + f) = (μ.tilted g).tilted f
rw₂ rw₃ : μ.tilted (g + f) = μ.tilted (g + f)
⊢ (μ.tilted f).tilted g = (μ.tilted g).tilted f

Tactic:
rw [tilted_tilted hf, add_comm, tilted_tilted hg]

Premises used: MeasureTheory.tilted_tilted, add_comm
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
rw : μ.tilted (f + -f) = HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) μ
⊢ (μ.tilted f).tilted (-f) = HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) μ

Tactic:
rw [tilted_tilted hf]

Premises used: MeasureTheory.tilted_tilted
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
⊢ μ.tilted (f + -f) = HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) μ

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst : IsProbabilityMeasure μ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
⊢ (μ.tilted f).tilted (-f) = μ

Tactic:
simp [hf]
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
⊢ μ.tilted f ≪ μ

Tactic:
withDensity_absolutelyContinuous _ _

Premises used: MeasureTheory.Measure.tilted, MeasureTheory.withDensity_absolutelyContinuous
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
h : μ = 0
inl : Measure.AbsolutelyContinuous.{u_1} (α := α) (_m0 := mα) 0 0
⊢ μ ≪ μ.tilted f

Tactic:
simp only [h, tilted_zero_measure]

Premises used: MeasureTheory.tilted_zero_measure
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
h : μ = 0
x : Set α
h_1 : Eq (α := ℝ≥0∞) (((0 : Measure α) : (a : Set α) → ℝ≥0∞) x : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((0 : Measure α) : (a : Set α) → ℝ≥0∞) x : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
h : μ = 0
⊢ Measure.AbsolutelyContinuous.{u_1} (α := α) (_m0 := mα) 0 0

Tactic:
exact fun _ _ ↦ by simp
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
h0 : NeZero μ
⊢ μ ≪ μ.tilted f

Tactic:
withDensity_absolutelyContinuous' ?_ ?_

Premises used: MeasureTheory.withDensity_absolutelyContinuous', MeasureTheory.Measure.tilted
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
h0 : NeZero μ
inr : AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)) μ
inr₁ : ∀ᵐ (x : α) ∂μ, ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) ≠ 0
⊢ μ ≪ μ.tilted f

Tactic:
refine withDensity_absolutelyContinuous' ?_ ?_

Premises used: MeasureTheory.withDensity_absolutelyContinuous'
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
h0 : NeZero μ
⊢ AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)) μ

Tactic:
(hf.1.aemeasurable.div_const _).ennreal_ofReal

Premises used: MeasureTheory.AEStronglyMeasurable.aemeasurable, AEMeasurable.div_const, And.left, AEMeasurable.ennreal_ofReal
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
h0 : NeZero μ
⊢ AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)) μ

Tactic:
exact (hf.1.aemeasurable.div_const _).ennreal_ofReal

Premises used: MeasureTheory.AEStronglyMeasurable.aemeasurable, AEMeasurable.div_const, And.left, AEMeasurable.ennreal_ofReal
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
h0 : NeZero μ
inr : ∀ (a : α), ENNReal.ofReal (rexp (f a) / ∫ (x : α), rexp (f x) ∂μ) ≠ 0
⊢ ∀ᵐ (x : α) ∂μ, ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) ≠ 0

Tactic:
filter_upwards
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
h0 : NeZero μ
inr : ∀ (a : α), 0 < rexp (f a) / ∫ (x : α), rexp (f x) ∂μ
⊢ ∀ (a : α), ENNReal.ofReal (rexp (f a) / ∫ (x : α), rexp (f x) ∂μ) ≠ 0

Tactic:
simp only [ne_eq, ENNReal.ofReal_eq_zero, not_le]

Premises used: not_le, ENNReal.ofReal_eq_zero, ne_eq
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
h0 : NeZero μ
⊢ ∀ (a : α), 0 < rexp (f a) / ∫ (x : α), rexp (f x) ∂μ

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

Premises used: div_pos, MeasureTheory.integral_exp_pos, Real.exp_pos
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
h0 : NeZero μ
⊢ ∀ (a : α), 0 < rexp (f a) / ∫ (x : α), rexp (f x) ∂μ

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

Premises used: div_pos, MeasureTheory.integral_exp_pos, Real.exp_pos
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
⊢ μ = 0 ∨ NeZero μ

Tactic:
cases eq_zero_or_neZero μ with
  | inl h => simp only [h, tilted_zero_measure]; exact fun _ _ ↦ by simp
  | inr h0 =>
    refine withDensity_absolutelyContinuous' ?_ ?_
    · exact (hf.1.aemeasurable.div_const _).ennreal_ofReal
    · filter_upwards
      simp only [ne_eq, ENNReal.ofReal_eq_zero, not_le]
      exact fun _ ↦ div_pos (exp_pos _) (integral_exp_pos hf)

Premises used: not_le, MeasureTheory.AEStronglyMeasurable.aemeasurable, MeasureTheory.withDensity_absolutelyContinuous', ENNReal.ofReal_eq_zero, AEMeasurable.div_const, ne_eq, And.left, MeasureTheory.tilted_zero_measure, AEMeasurable.ennreal_ofReal, eq_zero_or_neZero
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
g : α → E
pos : ∀ (hμ : μ = 0), Integrable g (μ.tilted f) ↔ Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ rexp (f x) • g x) μ
neg : ∀ (hμ : ¬μ = 0), Integrable g (μ.tilted f) ↔ Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ rexp (f x) • g x) μ
⊢ Integrable g (μ.tilted f) ↔ Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ rexp (f x) • g x) μ

Tactic:
by_cases hμ : μ = 0
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
g : α → E
hμ : μ = 0
⊢ Integrable g (μ.tilted f) ↔ Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ rexp (f x) • g x) μ

Tactic:
simp [hμ]
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
g : α → E
hμ : ¬μ = 0
⊢ AEMeasurable f μ

Tactic:
have hf_meas : AEMeasurable f μ := aemeasurable_of_aemeasurable_exp hf.1.aemeasurable
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
g : α → E
hμ : ¬μ = 0
hf_meas : AEMeasurable f μ
⊢ AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)) μ

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
g : α → E
hμ : ¬μ = 0
hf_meas : AEMeasurable f μ
⊢ ∀ᵐ (x : α) ∂μ, ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) < ∞

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
g : α → E
hμ : ¬μ = 0
hf_meas : AEMeasurable f μ
neg :
  Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ (ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)).toReal • g x)
      μ ↔
    Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ rexp (f x) • g x) μ
⊢ Integrable g (μ.tilted f) ↔ Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ rexp (f x) • g x) μ

Tactic:
rw [Measure.tilted, integrable_withDensity_iff_integrable_smul₀' (by fun_prop) (by simp)]

Premises used: MeasureTheory.integrable_withDensity_iff_integrable_smul₀', MeasureTheory.Measure.tilted
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
g : α → E
hμ : ¬μ = 0
hf_meas : AEMeasurable f μ
a : ∀ (a : α), (ENNReal.ofReal (rexp (f a) / ∫ (a : α), rexp (f a) ∂μ)).toReal = rexp (f a) / ∫ (a : α), rexp (f a) ∂μ
⊢ Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ (ENNReal.ofReal (rexp (f x) / ∫ (a : α), rexp (f a) ∂μ)).toReal • g x)
      μ ↔
    Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ (rexp (f x) / ∫ (a : α), rexp (f a) ∂μ) • g x) μ

Tactic:
congr! with a
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
g : α → E
hμ : ¬μ = 0
hf_meas : AEMeasurable f μ
a : α
a₁ : 0 ≤ rexp (f a) / ∫ (a : α), rexp (f a) ∂μ
⊢ (ENNReal.ofReal (rexp (f a) / ∫ (a : α), rexp (f a) ∂μ)).toReal = rexp (f a) / ∫ (a : α), rexp (f a) ∂μ

Tactic:
rw [ENNReal.toReal_ofReal]

Premises used: ENNReal.toReal_ofReal
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
g : α → E
hμ : ¬μ = 0
hf_meas : AEMeasurable f μ
a : α
⊢ 0 ≤ rexp (f a) / ∫ (a : α), rexp (f a) ∂μ

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
g : α → E
hμ : ¬μ = 0
hf_meas : AEMeasurable f μ
a :
  ∀ (a : α),
    (rexp (f a) / ∫ (a : α), rexp (f a) ∂μ) • g a = HSMul.hSMul (α := ℝ) (∫ (a : α), rexp (f a) ∂μ)⁻¹ (rexp (f a) • g a)
⊢ Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ (rexp (f x) / ∫ (a : α), rexp (f a) ∂μ) • g x) μ ↔
    Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ HSMul.hSMul (α := ℝ) (∫ (a : α), rexp (f a) ∂μ)⁻¹ (rexp (f x) • g x))
      μ

Tactic:
congr! 2 with a
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
g : α → E
hμ : ¬μ = 0
hf_meas : AEMeasurable f μ
a : α
a₁ : (rexp (f a) / ∫ (a : α), rexp (f a) ∂μ) • g a = ((∫ (a : α), rexp (f a) ∂μ)⁻¹ * rexp (f a)) • g a
a₂ a₃ : ((∫ (a : α), rexp (f a) ∂μ)⁻¹ * rexp (f a)) • g a = ((∫ (a : α), rexp (f a) ∂μ)⁻¹ * rexp (f a)) • g a
⊢ (rexp (f a) / ∫ (a : α), rexp (f a) ∂μ) • g a = HSMul.hSMul (α := ℝ) (∫ (a : α), rexp (f a) ∂μ)⁻¹ (rexp (f a) • g a)

Tactic:
rw [smul_smul, div_eq_inv_mul]

Premises used: smul_smul, div_eq_inv_mul
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
g : α → E
hμ : ¬μ = 0
hf_meas : AEMeasurable f μ
hc : Ne (α := ℝ) (∫ (a : α), rexp (f a) ∂μ)⁻¹ 0
⊢ Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ HSMul.hSMul (α := ℝ) (∫ (a : α), rexp (f a) ∂μ)⁻¹ (rexp (f x) • g x))
      μ ↔
    Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ rexp (f x) • g x) μ

Tactic:
rw [integrable_fun_smul_iff]

Premises used: MeasureTheory.integrable_fun_smul_iff
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
g : α → E
hμ : ¬μ = 0
hf_meas : AEMeasurable f μ
hc : ¬Eq (α := ℝ) (∫ (a : α), rexp (f a) ∂μ) 0
⊢ Ne (α := ℝ) (∫ (a : α), rexp (f a) ∂μ)⁻¹ 0

Tactic:
simp only [ne_eq, inv_eq_zero]

Premises used: inv_eq_zero, ne_eq
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
g : α → E
hμ : ¬μ = 0
hf_meas : AEMeasurable f μ
⊢ NeZero μ

Tactic:
have : NeZero μ := ⟨hμ⟩
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
g : α → E
hμ : ¬μ = 0
hf_meas : AEMeasurable f μ
this : NeZero μ
⊢ ¬Eq (α := ℝ) (∫ (a : α), rexp (f a) ∂μ) 0

Tactic:
(integral_exp_pos hf).ne'

Premises used: LT.lt.ne', MeasureTheory.integral_exp_pos
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
g : α → E
hμ : ¬μ = 0
hf_meas : AEMeasurable f μ
this : NeZero μ
⊢ ¬Eq (α := ℝ) (∫ (a : α), rexp (f a) ∂μ) 0

Tactic:
exact (integral_exp_pos hf).ne'

Premises used: LT.lt.ne', MeasureTheory.integral_exp_pos
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
g : α → E
hμ : ¬μ = 0
hf_meas : AEMeasurable f μ
calc :
  Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ (ENNReal.ofReal (rexp (f x) / ∫ (a : α), rexp (f a) ∂μ)).toReal • g x)
      μ ↔
    Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ (rexp (f x) / ∫ (a : α), rexp (f a) ∂μ) • g x) μ
calc₁ :
  Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ (rexp (f x) / ∫ (a : α), rexp (f a) ∂μ) • g x) μ ↔
    Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ HSMul.hSMul (α := ℝ) (∫ (a : α), rexp (f a) ∂μ)⁻¹ (rexp (f x) • g x))
      μ
calc₂ :
  Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ HSMul.hSMul (α := ℝ) (∫ (a : α), rexp (f a) ∂μ)⁻¹ (rexp (f x) • g x))
      μ ↔
    Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ rexp (f x) • g x) μ
⊢ Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ (ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)).toReal • g x)
      μ ↔
    Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ rexp (f x) • g x) μ

Tactic:
calc Integrable (fun x ↦ (ENNReal.ofReal (exp (f x) / ∫ a, exp (f a) ∂μ)).toReal • g x) μ
  _ ↔ Integrable (fun x ↦ (exp (f x) / ∫ a, exp (f a) ∂μ) • g x) μ := by
    congr! with a
    rw [ENNReal.toReal_ofReal]
    positivity
  _ ↔ Integrable (fun x ↦ (∫ a, exp (f a) ∂μ)⁻¹ • exp (f x) • g x) μ := by
    congr! 2 with a
    rw [smul_smul, div_eq_inv_mul]
  _ ↔ Integrable (fun x ↦ exp (f x) • g x) μ := by
    rw [integrable_fun_smul_iff]
    simp only [ne_eq, inv_eq_zero]
    have : NeZero μ := ⟨hμ⟩
    exact (integral_exp_pos hf).ne'

Premises used: ENNReal.ofReal, MeasureTheory.Integrable, HDiv.hDiv, Real.exp, ENNReal.toReal, Inv.inv, MeasureTheory.integral, HSMul.hSMul
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) ν
h : ν = 0
inl :
  ∀ᶠ (x : α) in ⊥,
    μ.rnDeriv (Measure.tilted 0 f) x =
      ENNReal.ofReal (rexp (-f x) * @integral _ _ _ _ mα 0 fun (x : α) ↦ rexp (f x)) * μ.rnDeriv 0 x
⊢ μ.rnDeriv (ν.tilted f) =ᶠ[ae ν] fun (x : α) ↦ ENNReal.ofReal (rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν) * μ.rnDeriv ν x

Tactic:
simp_rw [h, ae_zero, Filter.EventuallyEq]

Premises used: MeasureTheory.ae_zero, Filter.EventuallyEq
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) ν
h : ν = 0
⊢ ∀ᶠ (x : α) in ⊥,
    μ.rnDeriv (Measure.tilted 0 f) x =
      ENNReal.ofReal (rexp (-f x) * @integral _ _ _ _ mα 0 fun (x : α) ↦ rexp (f x)) * μ.rnDeriv 0 x

Tactic:
Filter.eventually_bot

Premises used: Filter.eventually_bot
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) ν
h : ν = 0
⊢ ∀ᶠ (x : α) in ⊥,
    μ.rnDeriv (Measure.tilted 0 f) x =
      ENNReal.ofReal (rexp (-f x) * @integral _ _ _ _ mα 0 fun (x : α) ↦ rexp (f x)) * μ.rnDeriv 0 x

Tactic:
exact Filter.eventually_bot

Premises used: Filter.eventually_bot
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) ν
h0 : NeZero ν
⊢ μ.rnDeriv (ν.tilted f) =ᶠ[ae ν] fun (x : α) ↦ ENNReal.ofReal (rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν) * μ.rnDeriv ν x

Tactic:
(Measure.rnDeriv_withDensity_right μ ν ?_ ?_ ?_).trans ?_

Premises used: Filter.EventuallyEq.trans, MeasureTheory.Measure.rnDeriv_withDensity_right, MeasureTheory.Measure.tilted