awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.ConditionalProbability (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s : Set Ω
hms : MeasurableSet s
hcs' : Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
t : Set Ω
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (μ[t | s] : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) =
    (μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t)
have inl : ∀ (hcs : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (μ[t | s] : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) =
    (μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t)
Tactic: obtain hcs | hcs := eq_or_ne (μ s) 0
-- Lean 4 proof step from Mathlib.Probability.ConditionalProbability (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s : Set Ω
hms : MeasurableSet s
hcs' : Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
t : Set Ω
inl :
  ∀ (hcs : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (μ[t | s] : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) =
      (μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t)
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (μ[t | s] : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) =
    (μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t)
have inr : ∀ (hcs : Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (μ[t | s] : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) =
    (μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t)
Tactic: obtain hcs | hcs := eq_or_ne (μ s) 0
-- Lean 4 proof step from Mathlib.Probability.ConditionalProbability (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s : Set Ω
hms : MeasurableSet s
hcs' : Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
t : Set Ω
hcs : Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (μ[t | s] : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) =
    (μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t)
have inr : HMul.hMul (β := ℝ≥0∞)
    (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞)
      ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞))
    ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) =
  (μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t)
Tactic: rw [cond_apply hms, mul_comm, ← mul_assoc, ENNReal.mul_inv_cancel hcs hcs', one_mul]
-- Lean 4 proof step from Mathlib.Probability.ConditionalProbability (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s : Set Ω
hms : MeasurableSet s
hcs' : Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
t : Set Ω
hcs : Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
inr :
  HMul.hMul (β := ℝ≥0∞)
      (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞)
        ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞))
      ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) =
    (μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t)
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (μ[t | s] : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) =
    (μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t)
have inr₁ : HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
    (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞)
      ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)) =
  (μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t)
Tactic: rw [cond_apply hms, mul_comm, ← mul_assoc, ENNReal.mul_inv_cancel hcs hcs', one_mul]
-- Lean 4 proof step from Mathlib.Probability.ConditionalProbability (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s : Set Ω
hms : MeasurableSet s
hcs' : Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
t : Set Ω
hcs : Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
inr :
  HMul.hMul (β := ℝ≥0∞)
      (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞)
        ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞))
      ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) =
    (μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t)
inr₁ :
  HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
      (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞)
        ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)) =
    (μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t)
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (μ[t | s] : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) =
    (μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t)
have inr₂ : HMul.hMul (β := ℝ≥0∞)
    (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞))
    ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) =
  (μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t)
Tactic: rw [cond_apply hms, mul_comm, ← mul_assoc, ENNReal.mul_inv_cancel hcs hcs', one_mul]
-- Lean 4 proof step from Mathlib.Probability.ConditionalProbability (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s : Set Ω
hms : MeasurableSet s
hcs' : Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
t : Set Ω
hcs : Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
inr :
  HMul.hMul (β := ℝ≥0∞)
      (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞)
        ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞))
      ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) =
    (μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t)
inr₁ :
  HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
      (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞)
        ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)) =
    (μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t)
inr₂ :
  HMul.hMul (β := ℝ≥0∞)
      (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞))
      ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) =
    (μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t)
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (μ[t | s] : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) =
    (μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t)
have inr₃ : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) =
  (μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t)
Tactic: rw [cond_apply hms, mul_comm, ← mul_assoc, ENNReal.mul_inv_cancel hcs hcs', one_mul]
-- Lean 4 proof step from Mathlib.Probability.ConditionalProbability (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s : Set Ω
hms : MeasurableSet s
hcs' : Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
t : Set Ω
hcs : Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
inr :
  HMul.hMul (β := ℝ≥0∞)
      (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞)
        ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞))
      ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) =
    (μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t)
inr₁ :
  HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
      (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞)
        ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)) =
    (μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t)
inr₂ :
  HMul.hMul (β := ℝ≥0∞)
      (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞))
      ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) =
    (μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t)
inr₃ :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) =
    (μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t)
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (μ[t | s] : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) =
    (μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t)
have inr₄ : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
Tactic: rw [cond_apply hms, mul_comm, ← mul_assoc, ENNReal.mul_inv_cancel hcs hcs', one_mul]
-- Lean 4 proof step from Mathlib.Probability.ConditionalProbability (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
s t : Set Ω
hms : MeasurableSet s
μ : Measure Ω
inst : IsFiniteMeasure μ
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (μ[t | s] : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) +
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (μ[t | sᶜ] : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) sᶜ : ℝ≥0∞) =
    (μ : (a : Set Ω) → ℝ≥0∞) t
have rw : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (t ∩ sᶜ) : ℝ≥0∞) =
  (μ : (a : Set Ω) → ℝ≥0∞) t
Tactic: rw [cond_mul_eq_inter hms, cond_mul_eq_inter hms.compl, Set.inter_comm _ t,
    Set.inter_comm _ t]
-- Lean 4 proof step from Mathlib.Probability.ConditionalProbability (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
s t : Set Ω
hms : MeasurableSet s
hmt : MeasurableSet t
μ : Measure Ω
inst : IsFiniteMeasure μ
⊢ μ[t | s] =
    HMul.hMul (β := ℝ≥0∞) (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) (μ[s | t] : ℝ≥0∞))
      ((μ : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
have rw : μ[t | s] =
  HMul.hMul (α := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞)
    (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (μ[s | t] : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞))
Tactic: rw [mul_assoc, cond_mul_eq_inter hmt s, Set.inter_comm, cond_apply hms]
-- Lean 4 proof step from Mathlib.Probability.ConditionalProbability (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
s t : Set Ω
hms : MeasurableSet s
hmt : MeasurableSet t
μ : Measure Ω
inst : IsFiniteMeasure μ
rw :
  μ[t | s] =
    HMul.hMul (α := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞)
      (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (μ[s | t] : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞))
⊢ μ[t | s] =
    HMul.hMul (β := ℝ≥0∞) (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) (μ[s | t] : ℝ≥0∞))
      ((μ : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
have rw₁ : μ[t | s] =
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
Tactic: rw [mul_assoc, cond_mul_eq_inter hmt s, Set.inter_comm, cond_apply hms]
-- Lean 4 proof step from Mathlib.Probability.ConditionalProbability (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
s t : Set Ω
hms : MeasurableSet s
hmt : MeasurableSet t
μ : Measure Ω
inst : IsFiniteMeasure μ
rw :
  μ[t | s] =
    HMul.hMul (α := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞)
      (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (μ[s | t] : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞))
rw₁ :
  μ[t | s] =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
⊢ μ[t | s] =
    HMul.hMul (β := ℝ≥0∞) (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) (μ[s | t] : ℝ≥0∞))
      ((μ : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
have rw₂ : μ[t | s] =
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
Tactic: rw [mul_assoc, cond_mul_eq_inter hmt s, Set.inter_comm, cond_apply hms]
-- Lean 4 proof step from Mathlib.Probability.ConditionalProbability (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
s t : Set Ω
hms : MeasurableSet s
hmt : MeasurableSet t
μ : Measure Ω
inst : IsFiniteMeasure μ
rw :
  μ[t | s] =
    HMul.hMul (α := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞)
      (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (μ[s | t] : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞))
rw₁ :
  μ[t | s] =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
rw₂ :
  μ[t | s] =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
⊢ μ[t | s] =
    HMul.hMul (β := ℝ≥0∞) (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) (μ[s | t] : ℝ≥0∞))
      ((μ : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
have rw₃ : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) =
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
Tactic: rw [mul_assoc, cond_mul_eq_inter hmt s, Set.inter_comm, cond_apply hms]
-- Lean 4 proof step from Mathlib.Probability.ConditionalProbability (goal)
Goal:
Ω : Type u_1
Ω' : Type u_2
m : MeasurableSpace Ω
m' : MeasurableSpace Ω'
μ : Measure Ω
s : Set Ω
i : Ω' → Ω
hi : MeasurableEmbedding i
hi' : ∀ᵐ (ω : Ω) ∂μ, ω ∈ range i
hs : MeasurableSet s
⊢ Eq (α := Measure Ω') (comap i μ[|s]) (comap i μ)[|i ⁻¹' s]
have h : ∀ (t : Set Ω') (ht : MeasurableSet t),
  Eq (α := ℝ≥0∞) (((comap i μ[|s] : Measure Ω') : (a : Set Ω') → ℝ≥0∞) t : ℝ≥0∞) ((comap i μ)[t | i ⁻¹' s] : ℝ≥0∞)
Tactic: ext t ht
-- Lean 4 proof step from Mathlib.Probability.ConditionalProbability (hypothesis)
Goal:
Ω : Type u_1
Ω' : Type u_2
m : MeasurableSpace Ω
m' : MeasurableSpace Ω'
μ : Measure Ω
s : Set Ω
i : Ω' → Ω
hi : MeasurableEmbedding i
hi' : ∀ᵐ (ω : Ω) ∂μ, ω ∈ range i
hs : MeasurableSet s
t : Set Ω'
ht : MeasurableSet t
⊢ Eq (α := ℝ≥0∞) (((comap i μ[|s] : Measure Ω') : (a : Set Ω') → ℝ≥0∞) t : ℝ≥0∞) ((comap i μ)[t | i ⁻¹' s] : ℝ≥0∞)
have hi'₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (range i)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: change μ (range i)ᶜ = 0 at hi'
Cleared hypotheses: hi'
-- Lean 4 proof step from Mathlib.Probability.ConditionalProbability (goal)
Goal:
Ω : Type u_1
Ω' : Type u_2
m : MeasurableSpace Ω
m' : MeasurableSpace Ω'
μ : Measure Ω
s : Set Ω
i : Ω' → Ω
hi : MeasurableEmbedding i
hs : MeasurableSet s
t : Set Ω'
ht : MeasurableSet t
hi' : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (range i)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((comap i μ[|s] : Measure Ω') : (a : Set Ω') → ℝ≥0∞) t : ℝ≥0∞) ((comap i μ)[t | i ⁻¹' s] : ℝ≥0∞)
have h : Function.Injective i
Tactic: rw [cond_apply, comap_apply, cond_apply, comap_apply, comap_apply, image_inter,
    image_preimage_eq_inter_range, inter_right_comm, measure_inter_conull hi',
    measure_inter_conull hi']
-- Lean 4 proof step from Mathlib.Probability.ConditionalProbability (goal)
Goal:
Ω : Type u_1
Ω' : Type u_2
m : MeasurableSpace Ω
m' : MeasurableSpace Ω'
μ : Measure Ω
s : Set Ω
i : Ω' → Ω
hi : MeasurableEmbedding i
hs : MeasurableSet s
t : Set Ω'
ht : MeasurableSet t
hi' : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (range i)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h h₁ : Function.Injective i
⊢ Eq (α := ℝ≥0∞) (((comap i μ[|s] : Measure Ω') : (a : Set Ω') → ℝ≥0∞) t : ℝ≥0∞) ((comap i μ)[t | i ⁻¹' s] : ℝ≥0∞)
have h₂ : ∀ (s : Set Ω'), MeasurableSet s → MeasurableSet (i '' s)
Tactic: rw [cond_apply, comap_apply, cond_apply, comap_apply, comap_apply, image_inter,
    image_preimage_eq_inter_range, inter_right_comm, measure_inter_conull hi',
    measure_inter_conull hi']
-- Lean 4 proof step from Mathlib.Probability.ConditionalProbability (goal)
Goal:
Ω : Type u_1
Ω' : Type u_2
m : MeasurableSpace Ω
m' : MeasurableSpace Ω'
μ : Measure Ω
s : Set Ω
i : Ω' → Ω
hi : MeasurableEmbedding i
hs : MeasurableSet s
t : Set Ω'
ht : MeasurableSet t
hi' : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (range i)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h h₁ : Function.Injective i
h₂ : ∀ (s : Set Ω'), MeasurableSet s → MeasurableSet (i '' s)
⊢ Eq (α := ℝ≥0∞) (((comap i μ[|s] : Measure Ω') : (a : Set Ω') → ℝ≥0∞) t : ℝ≥0∞) ((comap i μ)[t | i ⁻¹' s] : ℝ≥0∞)
have h₃ : MeasurableSet (i ⁻¹' s ∩ t)
Tactic: rw [cond_apply, comap_apply, cond_apply, comap_apply, comap_apply, image_inter,
    image_preimage_eq_inter_range, inter_right_comm, measure_inter_conull hi',
    measure_inter_conull hi']
-- Lean 4 proof step from Mathlib.Probability.ConditionalProbability (goal)
Goal:
Ω : Type u_1
Ω' : Type u_2
m : MeasurableSpace Ω
m' : MeasurableSpace Ω'
μ : Measure Ω
s : Set Ω
i : Ω' → Ω
hi : MeasurableEmbedding i
hs : MeasurableSet s
t : Set Ω'
ht : MeasurableSet t
hi' : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (range i)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h h₁ : Function.Injective i
h₂ : ∀ (s : Set Ω'), MeasurableSet s → MeasurableSet (i '' s)
h₃ : MeasurableSet (i ⁻¹' s ∩ t)
h₄ : Function.Injective i
h₅ : ∀ (s : Set Ω'), MeasurableSet s → MeasurableSet (i '' s)
⊢ Eq (α := ℝ≥0∞) (((comap i μ[|s] : Measure Ω') : (a : Set Ω') → ℝ≥0∞) t : ℝ≥0∞) ((comap i μ)[t | i ⁻¹' s] : ℝ≥0∞)
have h₆ : MeasurableSet (i ⁻¹' s)
Tactic: rw [cond_apply, comap_apply, cond_apply, comap_apply, comap_apply, image_inter,
    image_preimage_eq_inter_range, inter_right_comm, measure_inter_conull hi',
    measure_inter_conull hi']
-- Lean 4 proof step from Mathlib.Probability.ConditionalProbability (goal)
Goal:
Ω : Type u_1
α : Type u_3
m : MeasurableSpace Ω
inst : Fintype α
inst_1 : MeasurableSpace α
inst_2 : DiscreteMeasurableSpace α
X : Ω → α
hX : Measurable X
μ : Measure Ω
inst_3 : IsFiniteMeasure μ
⊢ ∑ x : α, HSMul.hSMul (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (X ⁻¹' {x}) : ℝ≥0∞) μ[|X ⁻¹' {x}] = μ
have h : ∀ (E : Set Ω) (hE : MeasurableSet E),
  Eq (α := ℝ≥0∞)
    (((∑ x : α, HSMul.hSMul (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (X ⁻¹' {x}) : ℝ≥0∞) μ[|X ⁻¹' {x}] : Measure Ω) :
          (a : Set Ω) → ℝ≥0∞)
        E :
      ℝ≥0∞)
    ((μ : (a : Set Ω) → ℝ≥0∞) E : ℝ≥0∞)
Tactic: ext E hE
-- Lean 4 proof step from Mathlib.Probability.ConditionalProbability (goal)
Goal:
Ω : Type u_1
α : Type u_3
m : MeasurableSpace Ω
inst : Fintype α
inst_1 : MeasurableSpace α
inst_2 : DiscreteMeasurableSpace α
X : Ω → α
hX : Measurable X
μ : Measure Ω
inst_3 : IsFiniteMeasure μ
E : Set Ω
hE : MeasurableSet E
⊢ Eq (α := ℝ≥0∞)
    (((∑ x : α, HSMul.hSMul (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (X ⁻¹' {x}) : ℝ≥0∞) μ[|X ⁻¹' {x}] : Measure Ω) :
          (a : Set Ω) → ℝ≥0∞)
        E :
      ℝ≥0∞)
    (∑ x : α, (μ : (a : Set Ω) → ℝ≥0∞) (X ⁻¹' {x} ∩ E) : ℝ≥0∞)
have simp : Eq (α := ℝ≥0∞)
  (∑ x : α, HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (X ⁻¹' {x}) : ℝ≥0∞) (μ[E | X ⁻¹' {x}] : ℝ≥0∞))
  (∑ x : α, (μ : (a : Set Ω) → ℝ≥0∞) (X ⁻¹' {x} ∩ E))
Tactic: simp only [Measure.coe_finsetSum, Measure.coe_smul, Finset.sum_apply,
        Pi.smul_apply, smul_eq_mul]
-- Lean 4 proof step from Mathlib.Probability.ConditionalProbability (goal)
Goal:
Ω : Type u_1
α : Type u_3
m : MeasurableSpace Ω
inst : Fintype α
inst_1 : MeasurableSpace α
inst_2 : DiscreteMeasurableSpace α
X : Ω → α
hX : Measurable X
μ : Measure Ω
inst_3 : IsFiniteMeasure μ
E : Set Ω
hE : MeasurableSet E
⊢ Eq (α := ℝ≥0∞)
    (∑ x : α, HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (X ⁻¹' {x}) : ℝ≥0∞) (μ[E | X ⁻¹' {x}] : ℝ≥0∞))
    (∑ x : α, (μ : (a : Set Ω) → ℝ≥0∞) (X ⁻¹' {x} ∩ E))
have simp_rw : Eq (α := ℝ≥0∞)
  (∑ x : α, HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (μ[E | X ⁻¹' {x}] : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (X ⁻¹' {x}) : ℝ≥0∞))
  (∑ x : α, (μ : (a : Set Ω) → ℝ≥0∞) (X ⁻¹' {x} ∩ E))
Tactic: simp_rw [mul_comm (μ _), cond_mul_eq_inter (hX (.singleton _))]
-- Lean 4 proof step from Mathlib.Probability.ConditionalProbability (goal)
Goal:
Ω : Type u_1
α : Type u_3
m : MeasurableSpace Ω
inst : Fintype α
inst_1 : MeasurableSpace α
inst_2 : DiscreteMeasurableSpace α
X : Ω → α
hX : Measurable X
μ : Measure Ω
inst_3 : IsFiniteMeasure μ
E : Set Ω
hE : MeasurableSet E
⊢ ⋃ (x : α), ⋃ (_ : Membership.mem (γ := Finset α) Finset.univ x), X ⁻¹' {x} ∩ E = E
have h : ∀ (x : Ω),
  Membership.mem (γ := Set Ω) (⋃ (x : α), ⋃ (_ : Membership.mem (γ := Finset α) Finset.univ x), X ⁻¹' {x} ∩ E) x ↔ x ∈ E
Tactic: ext
-- Lean 4 proof step from Mathlib.Probability.ConditionalProbability (hypothesis)
Goal:
Ω : Type u_1
α : Type u_3
m : MeasurableSpace Ω
inst : Fintype α
inst_1 : MeasurableSpace α
inst_2 : DiscreteMeasurableSpace α
X : Ω → α
hX : Measurable X
μ : Measure Ω
inst_3 : IsFiniteMeasure μ
E : Set Ω
hE : MeasurableSet E
⊢ Eq (α := ℝ≥0∞) (∑ x : α, (μ : (a : Set Ω) → ℝ≥0∞) (X ⁻¹' {x} ∩ E) : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) E : ℝ≥0∞)
have this : ⋃ (x : α), ⋃ (_ : Membership.mem (γ := Finset α) Finset.univ x), X ⁻¹' {x} ∩ E = E
Tactic: have : ⋃ x ∈ Finset.univ, X ⁻¹' {x} ∩ E = E := by ext; simp
-- Lean 4 proof step from Mathlib.Probability.ConditionalProbability (goal)
Goal:
Ω : Type u_1
α : Type u_3
m : MeasurableSpace Ω
inst : Fintype α
inst_1 : MeasurableSpace α
inst_2 : DiscreteMeasurableSpace α
X : Ω → α
hX : Measurable X
μ : Measure Ω
inst_3 : IsFiniteMeasure μ
E : Set Ω
hE : MeasurableSet E
this : ⋃ (x : α), ⋃ (_ : Membership.mem (γ := Finset α) Finset.univ x), X ⁻¹' {x} ∩ E = E
⊢ Eq (α := ℝ≥0∞) (∑ x : α, (μ : (a : Set Ω) → ℝ≥0∞) (X ⁻¹' {x} ∩ E) : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) E : ℝ≥0∞)
have rw : PairwiseDisjoint.{u_1, u_3} (α := Set Ω) (↑Finset.univ : Set α) fun (x : α) ↦ X ⁻¹' {x} ∩ E
Tactic: rw [← measure_biUnion_finset _ fun _ _ ↦ (hX (.singleton _)).inter hE, this]
-- Lean 4 proof step from Mathlib.Probability.ConditionalProbability (goal)
Goal:
Ω : Type u_1
α : Type u_3
m : MeasurableSpace Ω
inst : Fintype α
inst_1 : MeasurableSpace α
inst_2 : DiscreteMeasurableSpace α
X : Ω → α
hX : Measurable X
μ : Measure Ω
inst_3 : IsFiniteMeasure μ
E : Set Ω
hE : MeasurableSet E
⊢ Eq (α := ℝ≥0∞)
    (((∑ x : α, HSMul.hSMul (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (X ⁻¹' {x}) : ℝ≥0∞) μ[|X ⁻¹' {x}] : Measure Ω) :
          (a : Set Ω) → ℝ≥0∞)
        E :
      ℝ≥0∞)
    ((μ : (a : Set Ω) → ℝ≥0∞) E : ℝ≥0∞)
have _ : Eq (α := ℝ≥0∞)
  (((∑ x : α, HSMul.hSMul (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (X ⁻¹' {x}) : ℝ≥0∞) μ[|X ⁻¹' {x}] : Measure Ω) :
        (a : Set Ω) → ℝ≥0∞)
      E :
    ℝ≥0∞)
  (∑ x : α, (μ : (a : Set Ω) → ℝ≥0∞) (X ⁻¹' {x} ∩ E) : ℝ≥0∞)
Tactic: calc
    _ = ∑ x, μ (X ⁻¹' {x} ∩ E) := by
      simp only [Measure.coe_finsetSum, Measure.coe_smul, Finset.sum_apply,
        Pi.smul_apply, smul_eq_mul]
      simp_rw [mul_comm (μ _), cond_mul_eq_inter (hX (.singleton _))]
    _ = _ := by
      have : ⋃ x ∈ Finset.univ, X ⁻¹' {x} ∩ E = E := by ext; simp
      rw [← measure_biUnion_finset _ fun _ _ ↦ (hX (.singleton _)).inter hE, this]
      aesop (add simp [PairwiseDisjoint, Set.Pairwise, Function.onFun, disjoint_left])
-- Lean 4 proof step from Mathlib.Probability.ConditionalProbability (goal)
Goal:
Ω : Type u_1
α : Type u_3
m : MeasurableSpace Ω
inst : Fintype α
inst_1 : MeasurableSpace α
inst_2 : DiscreteMeasurableSpace α
X : Ω → α
hX : Measurable X
μ : Measure Ω
inst_3 : IsFiniteMeasure μ
E : Set Ω
hE : MeasurableSet E
_ :
  Eq (α := ℝ≥0∞)
    (((∑ x : α, HSMul.hSMul (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (X ⁻¹' {x}) : ℝ≥0∞) μ[|X ⁻¹' {x}] : Measure Ω) :
          (a : Set Ω) → ℝ≥0∞)
        E :
      ℝ≥0∞)
    (∑ x : α, (μ : (a : Set Ω) → ℝ≥0∞) (X ⁻¹' {x} ∩ E) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    (((∑ x : α, HSMul.hSMul (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (X ⁻¹' {x}) : ℝ≥0∞) μ[|X ⁻¹' {x}] : Measure Ω) :
          (a : Set Ω) → ℝ≥0∞)
        E :
      ℝ≥0∞)
    ((μ : (a : Set Ω) → ℝ≥0∞) E : ℝ≥0∞)
have _₁ : Eq (α := ℝ≥0∞) (∑ x : α, (μ : (a : Set Ω) → ℝ≥0∞) (X ⁻¹' {x} ∩ E) : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) E : ℝ≥0∞)
Tactic: calc
    _ = ∑ x, μ (X ⁻¹' {x} ∩ E) := by
      simp only [Measure.coe_finsetSum, Measure.coe_smul, Finset.sum_apply,
        Pi.smul_apply, smul_eq_mul]
      simp_rw [mul_comm (μ _), cond_mul_eq_inter (hX (.singleton _))]
    _ = _ := by
      have : ⋃ x ∈ Finset.univ, X ⁻¹' {x} ∩ E = E := by ext; simp
      rw [← measure_biUnion_finset _ fun _ _ ↦ (hX (.singleton _)).inter hE, this]
      aesop (add simp [PairwiseDisjoint, Set.Pairwise, Function.onFun, disjoint_left])
-- Lean 4 proof step from Mathlib.Probability.Decision.Risk.Basic (goal)
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
hl : Measurable (uncurry ℓ)
μ : Measure 𝓧
inst : SFinite μ
κ : Kernel 𝓧 𝓨
inst_1 : IsSFiniteKernel κ
π : Measure Θ
inst_2 : SFinite π
⊢ avgRisk ℓ (Kernel.const Θ μ) κ π = ∫⁻ (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y ∂π ∂(⇑κ : (a : 𝓧) → Measure 𝓨) ∘ₘ μ
have rw : ∫⁻ (θ : Θ), ∫⁻ (y : 𝓨), ℓ θ y ∂(⇑κ : (a : 𝓧) → Measure 𝓨) ∘ₘ μ ∂π =
  ∫⁻ (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y ∂π ∂(⇑κ : (a : 𝓧) → Measure 𝓨) ∘ₘ μ
Tactic: rw [avgRisk_const_left, lintegral_lintegral_swap (by fun_prop)]
-- Lean 4 proof step from Mathlib.Probability.Decision.Risk.Basic (goal)
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
hl : Measurable (uncurry ℓ)
μ : Measure 𝓧
inst : SFinite μ
κ : Kernel 𝓧 𝓨
inst_1 : IsSFiniteKernel κ
π : Measure Θ
inst_2 : SFinite π
rw :
  ∫⁻ (θ : Θ), ∫⁻ (y : 𝓨), ℓ θ y ∂(⇑κ : (a : 𝓧) → Measure 𝓨) ∘ₘ μ ∂π =
    ∫⁻ (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y ∂π ∂(⇑κ : (a : 𝓧) → Measure 𝓨) ∘ₘ μ
⊢ avgRisk ℓ (Kernel.const Θ μ) κ π = ∫⁻ (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y ∂π ∂(⇑κ : (a : 𝓧) → Measure 𝓨) ∘ₘ μ
have rw₁ : ∫⁻ (y : 𝓨), ∫⁻ (x : Θ), ℓ x y ∂π ∂(⇑κ : (a : 𝓧) → Measure 𝓨) ∘ₘ μ =
  ∫⁻ (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y ∂π ∂(⇑κ : (a : 𝓧) → Measure 𝓨) ∘ₘ μ
Tactic: rw [avgRisk_const_left, lintegral_lintegral_swap (by fun_prop)]