-- Mathlib/MeasureTheory/Measure/Tilted.lean
lemma integral_exp_tilted (f g : α → ℝ) :
    ∫ x, exp (g x) ∂(μ.tilted f) = (∫ x, exp ((f + g) x) ∂μ) / ∫ x, exp (f x) ∂μ

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ
h0 : NeZero μ
x : α
⊢ (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * rexp (g x) = rexp (f x) * rexp (g x) / ∫ (x : α), rexp (f x) ∂μ

Tactic:
ring

Result:
no goals

Proof state:
case inl
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ
h : μ = 0
⊢ ∫ (x : α), rexp (g x) ∂μ.tilted f = (∫ (x : α), rexp ((f + g) x) ∂μ) / ∫ (x : α), rexp (f x) ∂μ

Tactic:
rw [h]

Result:
case inl
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ
h : μ = 0
⊢ ∫ (x : α), rexp (g x) ∂Measure.tilted 0 f = (∫ (x : α), rexp ((f + g) x) ∂0) / ∫ (x : α), rexp (f x) ∂0

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ
h0 : NeZero μ
⊢ ∀ (x : α), (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * rexp (g x) = rexp ((f + g) x) / ∫ (x : α), rexp (f x) ∂μ

Tactic:
intro x

Result:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ
h0 : NeZero μ
x : α
⊢ (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * rexp (g x) = rexp ((f + g) x) / ∫ (x : α), rexp (f x) ∂μ

Proof state:
case inl
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ
h : μ = 0
⊢ ∫ (x : α), rexp (g x) ∂Measure.tilted 0 f = (∫ (x : α), rexp ((f + g) x) ∂0) / ∫ (x : α), rexp (f x) ∂0

Tactic:
simp

Result:
no goals

Proof state:
case inr
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ
h0 : NeZero μ
⊢ ∫ (x : α), rexp (g x) ∂μ.tilted f = (∫ (x : α), rexp ((f + g) x) ∂μ) / ∫ (x : α), rexp (f x) ∂μ

Tactic:
rw [integral_tilted f]

Result:
case inr
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ
h0 : NeZero μ
⊢ ∫ (x : α), (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) • rexp (g x) ∂μ =
    (∫ (x : α), rexp ((f + g) x) ∂μ) / ∫ (x : α), rexp (f x) ∂μ

Proof state:
case inr
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ
h0 : NeZero μ
⊢ ∫ (x : α), (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * rexp (g x) ∂μ =
    (∫ (x : α), rexp ((f + g) x) ∂μ) / ∫ (x : α), rexp (f x) ∂μ

Tactic:
have : ∀ x, (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * rexp (g x)
    = (rexp ((f + g) x) / ∫ (x : α), rexp (f x) ∂μ) := by
  intro x
  rw [Pi.add_apply, exp_add]
  ring

Result:
case inr
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ
h0 : NeZero μ
this : ∀ (x : α), (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * rexp (g x) = rexp ((f + g) x) / ∫ (x : α), rexp (f x) ∂μ
⊢ ∫ (x : α), (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * rexp (g x) ∂μ =
    (∫ (x : α), rexp ((f + g) x) ∂μ) / ∫ (x : α), rexp (f x) ∂μ

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ
h0 : NeZero μ
x : α
⊢ (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * rexp (g x) = rexp ((f + g) x) / ∫ (x : α), rexp (f x) ∂μ

Tactic:
rw [Pi.add_apply, exp_add]

Result:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ
h0 : NeZero μ
x : α
⊢ (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * rexp (g x) = rexp (f x) * rexp (g x) / ∫ (x : α), rexp (f x) ∂μ

Proof state:
case inr
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ
h0 : NeZero μ
this : ∀ (x : α), (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * rexp (g x) = rexp ((f + g) x) / ∫ (x : α), rexp (f x) ∂μ
⊢ ∫ (x : α), rexp ((f + g) x) * (∫ (x : α), rexp (f x) ∂μ)⁻¹ ∂μ =
    (∫ (x : α), rexp ((f + g) x) ∂μ) * (∫ (x : α), rexp (f x) ∂μ)⁻¹

Tactic:
rw [integral_mul_right]

Result:
no goals

Proof state:
case inr
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ
h0 : NeZero μ
⊢ ∫ (x : α), (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) • rexp (g x) ∂μ =
    (∫ (x : α), rexp ((f + g) x) ∂μ) / ∫ (x : α), rexp (f x) ∂μ

Tactic:
simp_rw [smul_eq_mul]

Result:
case inr
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ
h0 : NeZero μ
⊢ ∫ (x : α), (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * rexp (g x) ∂μ =
    (∫ (x : α), rexp ((f + g) x) ∂μ) / ∫ (x : α), rexp (f x) ∂μ

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ
⊢ ∫ (x : α), rexp (g x) ∂μ.tilted f = (∫ (x : α), rexp ((f + g) x) ∂μ) / ∫ (x : α), rexp (f x) ∂μ

Tactic:
cases eq_zero_or_neZero μ with
| inl h => rw [h]; simp
| inr h0 =>
  rw [integral_tilted f]
  simp_rw [smul_eq_mul]
  have : ∀ x, (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * rexp (g x)
      = (rexp ((f + g) x) / ∫ (x : α), rexp (f x) ∂μ) := by
    intro x
    rw [Pi.add_apply, exp_add]
    ring
  simp_rw [this, div_eq_mul_inv]
  rw [integral_mul_right]

Result:
no goals

Proof state:
case inr
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ
h0 : NeZero μ
this : ∀ (x : α), (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * rexp (g x) = rexp ((f + g) x) / ∫ (x : α), rexp (f x) ∂μ
⊢ ∫ (x : α), (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * rexp (g x) ∂μ =
    (∫ (x : α), rexp ((f + g) x) ∂μ) / ∫ (x : α), rexp (f x) ∂μ

Tactic:
simp_rw [this, div_eq_mul_inv]

Result:
case inr
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ
h0 : NeZero μ
this : ∀ (x : α), (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * rexp (g x) = rexp ((f + g) x) / ∫ (x : α), rexp (f x) ∂μ
⊢ ∫ (x : α), rexp ((f + g) x) * (∫ (x : α), rexp (f x) ∂μ)⁻¹ ∂μ =
    (∫ (x : α), rexp ((f + g) x) ∂μ) * (∫ (x : α), rexp (f x) ∂μ)⁻¹