-- Mathlib/MeasureTheory/Integral/Average.lean
theorem laverage_add_measure :
    ⨍⁻ x, f x ∂(μ + ν) =
      μ univ / (μ univ + ν univ) * ⨍⁻ x, f x ∂μ + ν univ / (μ univ + ν univ) * ⨍⁻ x, f x ∂ν

Proof state:
case pos
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hμ : IsFiniteMeasure μ
hν : IsFiniteMeasure ν
this : IsFiniteMeasure μ
⊢ ⨍⁻ (x : α), f x ∂(μ + ν) =
    μ univ / (μ univ + ν univ) * ⨍⁻ (x : α), f x ∂μ + ν univ / (μ univ + ν univ) * ⨍⁻ (x : α), f x ∂ν

Tactic:
haveI := hν

Result:
case pos
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hμ : IsFiniteMeasure μ
hν : IsFiniteMeasure ν
this✝ : IsFiniteMeasure μ
this : IsFiniteMeasure ν
⊢ ⨍⁻ (x : α), f x ∂(μ + ν) =
    μ univ / (μ univ + ν univ) * ⨍⁻ (x : α), f x ∂μ + ν univ / (μ univ + ν univ) * ⨍⁻ (x : α), f x ∂ν

Proof state:
case pos
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hμ : IsFiniteMeasure μ
hν : IsFiniteMeasure ν
this✝ : IsFiniteMeasure μ
this : IsFiniteMeasure ν
⊢ ⨍⁻ (x : α), f x ∂(μ + ν) =
    μ univ / (μ univ + ν univ) * ⨍⁻ (x : α), f x ∂μ + ν univ / (μ univ + ν univ) * ⨍⁻ (x : α), f x ∂ν

Tactic:
simp only [← ENNReal.mul_div_right_comm, measure_mul_laverage, ← ENNReal.add_div,
  ← lintegral_add_measure, ← Measure.add_apply, ← laverage_eq]

Result:
no goals

Proof state:
case pos
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hμ : IsFiniteMeasure μ
hν : IsFiniteMeasure ν
⊢ ⨍⁻ (x : α), f x ∂(μ + ν) =
    μ univ / (μ univ + ν univ) * ⨍⁻ (x : α), f x ∂μ + ν univ / (μ univ + ν univ) * ⨍⁻ (x : α), f x ∂ν

Tactic:
haveI := hμ

Result:
case pos
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hμ : IsFiniteMeasure μ
hν : IsFiniteMeasure ν
this : IsFiniteMeasure μ
⊢ ⨍⁻ (x : α), f x ∂(μ + ν) =
    μ univ / (μ univ + ν univ) * ⨍⁻ (x : α), f x ∂μ + ν univ / (μ univ + ν univ) * ⨍⁻ (x : α), f x ∂ν

Proof state:
case neg
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hμ : IsFiniteMeasure μ
hν : ¬IsFiniteMeasure ν
⊢ ⨍⁻ (x : α), f x ∂(μ + ν) =
    μ univ / (μ univ + ν univ) * ⨍⁻ (x : α), f x ∂μ + ν univ / (μ univ + ν univ) * ⨍⁻ (x : α), f x ∂ν

Tactic:
rw [not_isFiniteMeasure_iff] at hν

Result:
case neg
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hμ : IsFiniteMeasure μ
hν : ν univ = ⊤
⊢ ⨍⁻ (x : α), f x ∂(μ + ν) =
    μ univ / (μ univ + ν univ) * ⨍⁻ (x : α), f x ∂μ + ν univ / (μ univ + ν univ) * ⨍⁻ (x : α), f x ∂ν

Proof state:
case neg
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hμ : IsFiniteMeasure μ
hν : ν univ = ⊤
⊢ ⨍⁻ (x : α), f x ∂(μ + ν) =
    μ univ / (μ univ + ν univ) * ⨍⁻ (x : α), f x ∂μ + ν univ / (μ univ + ν univ) * ⨍⁻ (x : α), f x ∂ν

Tactic:
simp [laverage_eq, hν]

Result:
no goals

Proof state:
case neg
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hμ : μ univ = ⊤
⊢ ⨍⁻ (x : α), f x ∂(μ + ν) =
    μ univ / (μ univ + ν univ) * ⨍⁻ (x : α), f x ∂μ + ν univ / (μ univ + ν univ) * ⨍⁻ (x : α), f x ∂ν

Tactic:
simp [laverage_eq, hμ]

Result:
no goals

Proof state:
case pos
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hμ : IsFiniteMeasure μ
hν : IsFiniteMeasure ν
⊢ ⨍⁻ (x : α), f x ∂(μ + ν) =
    μ univ / (μ univ + ν univ) * ⨍⁻ (x : α), f x ∂μ + ν univ / (μ univ + ν univ) * ⨍⁻ (x : α), f x ∂ν

case neg
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hμ : IsFiniteMeasure μ
hν : ¬IsFiniteMeasure ν
⊢ ⨍⁻ (x : α), f x ∂(μ + ν) =
    μ univ / (μ univ + ν univ) * ⨍⁻ (x : α), f x ∂μ + ν univ / (μ univ + ν univ) * ⨍⁻ (x : α), f x ∂ν

Tactic:
swap

Result:
case neg
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hμ : IsFiniteMeasure μ
hν : ¬IsFiniteMeasure ν
⊢ ⨍⁻ (x : α), f x ∂(μ + ν) =
    μ univ / (μ univ + ν univ) * ⨍⁻ (x : α), f x ∂μ + ν univ / (μ univ + ν univ) * ⨍⁻ (x : α), f x ∂ν

case pos
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hμ : IsFiniteMeasure μ
hν : IsFiniteMeasure ν
⊢ ⨍⁻ (x : α), f x ∂(μ + ν) =
    μ univ / (μ univ + ν univ) * ⨍⁻ (x : α), f x ∂μ + ν univ / (μ univ + ν univ) * ⨍⁻ (x : α), f x ∂ν

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
⊢ ⨍⁻ (x : α), f x ∂(μ + ν) =
    μ univ / (μ univ + ν univ) * ⨍⁻ (x : α), f x ∂μ + ν univ / (μ univ + ν univ) * ⨍⁻ (x : α), f x ∂ν

Tactic:
by_cases hμ : IsFiniteMeasure μ

Result:
case pos
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hμ : IsFiniteMeasure μ
⊢ ⨍⁻ (x : α), f x ∂(μ + ν) =
    μ univ / (μ univ + ν univ) * ⨍⁻ (x : α), f x ∂μ + ν univ / (μ univ + ν univ) * ⨍⁻ (x : α), f x ∂ν

case neg
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hμ : ¬IsFiniteMeasure μ
⊢ ⨍⁻ (x : α), f x ∂(μ + ν) =
    μ univ / (μ univ + ν univ) * ⨍⁻ (x : α), f x ∂μ + ν univ / (μ univ + ν univ) * ⨍⁻ (x : α), f x ∂ν

Proof state:
case neg
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hμ : ¬IsFiniteMeasure μ
⊢ ⨍⁻ (x : α), f x ∂(μ + ν) =
    μ univ / (μ univ + ν univ) * ⨍⁻ (x : α), f x ∂μ + ν univ / (μ univ + ν univ) * ⨍⁻ (x : α), f x ∂ν

Tactic:
rw [not_isFiniteMeasure_iff] at hμ

Result:
case neg
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hμ : μ univ = ⊤
⊢ ⨍⁻ (x : α), f x ∂(μ + ν) =
    μ univ / (μ univ + ν univ) * ⨍⁻ (x : α), f x ∂μ + ν univ / (μ univ + ν univ) * ⨍⁻ (x : α), f x ∂ν

Proof state:
case pos
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hμ : IsFiniteMeasure μ
⊢ ⨍⁻ (x : α), f x ∂(μ + ν) =
    μ univ / (μ univ + ν univ) * ⨍⁻ (x : α), f x ∂μ + ν univ / (μ univ + ν univ) * ⨍⁻ (x : α), f x ∂ν

case neg
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hμ : ¬IsFiniteMeasure μ
⊢ ⨍⁻ (x : α), f x ∂(μ + ν) =
    μ univ / (μ univ + ν univ) * ⨍⁻ (x : α), f x ∂μ + ν univ / (μ univ + ν univ) * ⨍⁻ (x : α), f x ∂ν

Tactic:
swap

Result:
case neg
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hμ : ¬IsFiniteMeasure μ
⊢ ⨍⁻ (x : α), f x ∂(μ + ν) =
    μ univ / (μ univ + ν univ) * ⨍⁻ (x : α), f x ∂μ + ν univ / (μ univ + ν univ) * ⨍⁻ (x : α), f x ∂ν

case pos
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hμ : IsFiniteMeasure μ
⊢ ⨍⁻ (x : α), f x ∂(μ + ν) =
    μ univ / (μ univ + ν univ) * ⨍⁻ (x : α), f x ∂μ + ν univ / (μ univ + ν univ) * ⨍⁻ (x : α), f x ∂ν

Proof state:
case pos
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hμ : IsFiniteMeasure μ
⊢ ⨍⁻ (x : α), f x ∂(μ + ν) =
    μ univ / (μ univ + ν univ) * ⨍⁻ (x : α), f x ∂μ + ν univ / (μ univ + ν univ) * ⨍⁻ (x : α), f x ∂ν

Tactic:
by_cases hν : IsFiniteMeasure ν

Result:
case pos
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hμ : IsFiniteMeasure μ
hν : IsFiniteMeasure ν
⊢ ⨍⁻ (x : α), f x ∂(μ + ν) =
    μ univ / (μ univ + ν univ) * ⨍⁻ (x : α), f x ∂μ + ν univ / (μ univ + ν univ) * ⨍⁻ (x : α), f x ∂ν

case neg
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hμ : IsFiniteMeasure μ
hν : ¬IsFiniteMeasure ν
⊢ ⨍⁻ (x : α), f x ∂(μ + ν) =
    μ univ / (μ univ + ν univ) * ⨍⁻ (x : α), f x ∂μ + ν univ / (μ univ + ν univ) * ⨍⁻ (x : α), f x ∂ν