awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.ConditionalProbability (goal)
Goal:
Ω : Type u_1
Ω' : Type u_2
α : Type u_3
m : MeasurableSpace Ω
m' : MeasurableSpace Ω'
μ : Measure Ω
s t : Set Ω
measure_univ :
  ∀ (h : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) = 0 ∨
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) = 1
⊢ HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) = 0 ∨
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) = 1
have measure_univ₁ : ∀ (h : Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
  HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) = 0 ∨
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) = 1
Tactic: rcases eq_or_ne (μ s) 0 with h | h
-- Lean 4 proof step from Mathlib.Probability.ConditionalProbability (goal)
Goal:
Ω : Type u_1
Ω' : Type u_2
α : Type u_3
m : MeasurableSpace Ω
m' : MeasurableSpace Ω'
μ : Measure Ω
s t : Set Ω
h : Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) = 0 ∨
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) = 1
have measure_univ : ∀ (h' : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
  HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) = 0 ∨
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) = 1
Tactic: rcases eq_or_ne (μ s) ∞ with h' | h'
-- Lean 4 proof step from Mathlib.Probability.ConditionalProbability (goal)
Goal:
Ω : Type u_1
Ω' : Type u_2
α : Type u_3
m : MeasurableSpace Ω
m' : MeasurableSpace Ω'
μ : Measure Ω
s t : Set Ω
h : Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
measure_univ :
  ∀ (h' : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) = 0 ∨
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) = 1
⊢ HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) = 0 ∨
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) = 1
have measure_univ₁ : ∀ (h' : Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
  HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) = 0 ∨
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) = 1
Tactic: rcases eq_or_ne (μ s) ∞ with h' | h'
-- Lean 4 proof step from Mathlib.Probability.ConditionalProbability (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s : Set Ω
⊢ HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) (toMeasurable μ s))⁻¹ : ℝ≥0∞) (μ.restrict (toMeasurable μ s)) =
    HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) (μ.restrict s)
have pos : ∀ (hnt : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
  HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) (toMeasurable μ s))⁻¹ : ℝ≥0∞) (μ.restrict (toMeasurable μ s)) =
    HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) (μ.restrict s)
Tactic: by_cases hnt : μ s = ∞
-- Lean 4 proof step from Mathlib.Probability.ConditionalProbability (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s : Set Ω
pos :
  ∀ (hnt : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) (toMeasurable μ s))⁻¹ : ℝ≥0∞) (μ.restrict (toMeasurable μ s)) =
      HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) (μ.restrict s)
⊢ HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) (toMeasurable μ s))⁻¹ : ℝ≥0∞) (μ.restrict (toMeasurable μ s)) =
    HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) (μ.restrict s)
have neg : ∀ (hnt : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
  HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) (toMeasurable μ s))⁻¹ : ℝ≥0∞) (μ.restrict (toMeasurable μ s)) =
    HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) (μ.restrict s)
Tactic: by_cases hnt : μ s = ∞
-- Lean 4 proof step from Mathlib.Probability.ConditionalProbability (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
inst : IsFiniteMeasure μ
⊢ μ ≪ μ[|univ]
have rw : μ ≪ HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ
Tactic: rw [cond, restrict_univ]
-- Lean 4 proof step from Mathlib.Probability.ConditionalProbability (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
inst : IsFiniteMeasure μ
⊢ μ ≪ HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ
have refine : Ne (α := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: refine absolutelyContinuous_smul ?_
-- Lean 4 proof step from Mathlib.Probability.ConditionalProbability (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
s : Set Ω
hms : MeasurableSet s
μ : Measure Ω
t : Set Ω
⊢ μ[t | s] =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
have rw : (HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) (μ.restrict s) : (a : Set Ω) → ℝ≥0∞) t =
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
Tactic: rw [cond, Measure.smul_apply, Measure.restrict_apply' hms, Set.inter_comm, smul_eq_mul]
-- Lean 4 proof step from Mathlib.Probability.ConditionalProbability (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
s : Set Ω
hms : MeasurableSet s
μ : Measure Ω
t : Set Ω
rw :
  (HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) (μ.restrict s) : (a : Set Ω) → ℝ≥0∞) t =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
⊢ μ[t | s] =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
have rw₁ : HSMul.hSMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞)
    ((μ.restrict s : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) =
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
Tactic: rw [cond, Measure.smul_apply, Measure.restrict_apply' hms, Set.inter_comm, smul_eq_mul]
-- Lean 4 proof step from Mathlib.Probability.ConditionalProbability (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
s : Set Ω
hms : MeasurableSet s
μ : Measure Ω
t : Set Ω
rw :
  (HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) (μ.restrict s) : (a : Set Ω) → ℝ≥0∞) t =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
rw₁ :
  HSMul.hSMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞)
      ((μ.restrict s : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
⊢ μ[t | s] =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
have rw₂ : HSMul.hSMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞) =
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
Tactic: rw [cond, Measure.smul_apply, Measure.restrict_apply' hms, Set.inter_comm, smul_eq_mul]
-- Lean 4 proof step from Mathlib.Probability.ConditionalProbability (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
s : Set Ω
hms : MeasurableSet s
μ : Measure Ω
t : Set Ω
rw :
  (HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) (μ.restrict s) : (a : Set Ω) → ℝ≥0∞) t =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
rw₁ :
  HSMul.hSMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞)
      ((μ.restrict s : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
rw₂ :
  HSMul.hSMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞)
      ((μ : (a : Set Ω) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
⊢ μ[t | s] =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
have rw₃ : HSMul.hSMul (α := ℝ≥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 [cond, Measure.smul_apply, Measure.restrict_apply' hms, Set.inter_comm, smul_eq_mul]
-- Lean 4 proof step from Mathlib.Probability.ConditionalProbability (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
s : Set Ω
hms : MeasurableSet s
μ : Measure Ω
t : Set Ω
rw :
  (HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) (μ.restrict s) : (a : Set Ω) → ℝ≥0∞) t =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
rw₁ :
  HSMul.hSMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞)
      ((μ.restrict s : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
rw₂ :
  HSMul.hSMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞)
      ((μ : (a : Set Ω) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
rw₃ :
  HSMul.hSMul (α := ℝ≥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∞)
⊢ μ[t | s] =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ 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 [cond, Measure.smul_apply, Measure.restrict_apply' hms, Set.inter_comm, smul_eq_mul]
-- Lean 4 proof step from Mathlib.Probability.ConditionalProbability (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
s t : Set Ω
ht : MeasurableSet t
μ : Measure Ω
⊢ μ[t | s] =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
have rw : (HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) (μ.restrict s) : (a : Set Ω) → ℝ≥0∞) t =
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
Tactic: rw [cond, Measure.smul_apply, Measure.restrict_apply ht, Set.inter_comm, smul_eq_mul]
-- Lean 4 proof step from Mathlib.Probability.ConditionalProbability (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
s t : Set Ω
ht : MeasurableSet t
μ : Measure Ω
rw :
  (HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) (μ.restrict s) : (a : Set Ω) → ℝ≥0∞) t =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
⊢ μ[t | s] =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
have rw₁ : HSMul.hSMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞)
    ((μ.restrict s : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) =
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
Tactic: rw [cond, Measure.smul_apply, Measure.restrict_apply ht, Set.inter_comm, smul_eq_mul]
-- Lean 4 proof step from Mathlib.Probability.ConditionalProbability (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
s t : Set Ω
ht : MeasurableSet t
μ : Measure Ω
rw :
  (HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) (μ.restrict s) : (a : Set Ω) → ℝ≥0∞) t =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
rw₁ :
  HSMul.hSMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞)
      ((μ.restrict s : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
⊢ μ[t | s] =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
have rw₂ : HSMul.hSMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞) =
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
Tactic: rw [cond, Measure.smul_apply, Measure.restrict_apply ht, Set.inter_comm, smul_eq_mul]
-- Lean 4 proof step from Mathlib.Probability.ConditionalProbability (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
s t : Set Ω
ht : MeasurableSet t
μ : Measure Ω
rw :
  (HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) (μ.restrict s) : (a : Set Ω) → ℝ≥0∞) t =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
rw₁ :
  HSMul.hSMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞)
      ((μ.restrict s : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
rw₂ :
  HSMul.hSMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞)
      ((μ : (a : Set Ω) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
⊢ μ[t | s] =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
have rw₃ : HSMul.hSMul (α := ℝ≥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 [cond, Measure.smul_apply, Measure.restrict_apply ht, Set.inter_comm, smul_eq_mul]
-- Lean 4 proof step from Mathlib.Probability.ConditionalProbability (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
s t : Set Ω
ht : MeasurableSet t
μ : Measure Ω
rw :
  (HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) (μ.restrict s) : (a : Set Ω) → ℝ≥0∞) t =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
rw₁ :
  HSMul.hSMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞)
      ((μ.restrict s : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
rw₂ :
  HSMul.hSMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞)
      ((μ : (a : Set Ω) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
rw₃ :
  HSMul.hSMul (α := ℝ≥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∞)
⊢ μ[t | s] =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ 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 [cond, Measure.smul_apply, Measure.restrict_apply ht, Set.inter_comm, smul_eq_mul]
-- Lean 4 proof step from Mathlib.Probability.ConditionalProbability (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
s : Set Ω
hms : MeasurableSet s
t : Set Ω
μ : Measure Ω
⊢ Eq (α := ℝ≥0∞) (μ[s ∩ t | s] : ℝ≥0∞) (μ[t | s] : ℝ≥0∞)
have rw : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞)
    ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ (s ∩ t)) : ℝ≥0∞) =
  μ[t | s]
Tactic: rw [cond_apply hms, ← Set.inter_assoc, Set.inter_self, ← cond_apply hms]
-- Lean 4 proof step from Mathlib.Probability.ConditionalProbability (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
s : Set Ω
hms : MeasurableSet s
t : Set Ω
μ : Measure Ω
rw :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞)
      ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ (s ∩ t)) : ℝ≥0∞) =
    μ[t | s]
⊢ Eq (α := ℝ≥0∞) (μ[s ∩ t | s] : ℝ≥0∞) (μ[t | s] : ℝ≥0∞)
have rw₁ : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞)
    ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ s ∩ t) : ℝ≥0∞) =
  μ[t | s]
Tactic: rw [cond_apply hms, ← Set.inter_assoc, Set.inter_self, ← cond_apply hms]
-- Lean 4 proof step from Mathlib.Probability.ConditionalProbability (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
s : Set Ω
hms : MeasurableSet s
t : Set Ω
μ : Measure Ω
rw :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞)
      ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ (s ∩ t)) : ℝ≥0∞) =
    μ[t | s]
rw₁ :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞)
      ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ s ∩ t) : ℝ≥0∞) =
    μ[t | s]
⊢ Eq (α := ℝ≥0∞) (μ[s ∩ t | s] : ℝ≥0∞) (μ[t | s] : ℝ≥0∞)
have rw₂ : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) =
  μ[t | s]
Tactic: rw [cond_apply hms, ← Set.inter_assoc, Set.inter_self, ← cond_apply hms]
-- Lean 4 proof step from Mathlib.Probability.ConditionalProbability (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
s : Set Ω
hms : MeasurableSet s
t : Set Ω
μ : Measure Ω
rw :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞)
      ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ (s ∩ t)) : ℝ≥0∞) =
    μ[t | s]
rw₁ :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞)
      ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ s ∩ t) : ℝ≥0∞) =
    μ[t | s]
rw₂ :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) =
    μ[t | s]
⊢ Eq (α := ℝ≥0∞) (μ[s ∩ t | s] : ℝ≥0∞) (μ[t | s] : ℝ≥0∞)
have rw₃ : Eq (α := ℝ≥0∞) (μ[t | s] : ℝ≥0∞) (μ[t | s] : ℝ≥0∞)
Tactic: rw [cond_apply hms, ← Set.inter_assoc, Set.inter_self, ← cond_apply hms]
-- Lean 4 proof step from Mathlib.Probability.ConditionalProbability (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s t : Set Ω
hms : MeasurableSet s
hcst : Ne (α := ℝ≥0∞) (μ[t | s] : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
have refine : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) ≠ 0
Tactic: refine pos_iff_ne_zero.mpr (right_ne_zero_of_mul (a := (μ s)⁻¹) ?_)
-- Lean 4 proof step from Mathlib.Probability.ConditionalProbability (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s t : Set Ω
hms : MeasurableSet s
hcst : Ne (α := ℝ≥0∞) (μ[t | s] : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) ≠
    0
have h : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) =
  μ[t | s]
Tactic: convert! hcst
-- Lean 4 proof step from Mathlib.Probability.ConditionalProbability (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s t : Set Ω
inst : IsFiniteMeasure μ
hms : MeasurableSet s
hci : Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) (μ[t | s] : ℝ≥0∞)
have rw : 0 < HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
Tactic: rw [cond_apply hms]
-- Lean 4 proof step from Mathlib.Probability.ConditionalProbability (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s t : Set Ω
inst : IsFiniteMeasure μ
hms : MeasurableSet s
hci : Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ 0 <
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
have refine : Ne (α := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: refine ENNReal.mul_pos ?_ hci
-- Lean 4 proof step from Mathlib.Probability.ConditionalProbability (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s t : Set Ω
hms : MeasurableSet s
hmt : MeasurableSet t
hcs : Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ μ[|s][|t] = μ[|s ∩ t]
have h : ∀ (u : Set Ω), MeasurableSet u → Eq (α := ℝ≥0∞) (μ[|s][u | t] : ℝ≥0∞) (μ[u | s ∩ t] : ℝ≥0∞)
Tactic: ext u
-- Lean 4 proof step from Mathlib.Probability.ConditionalProbability (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s t : Set Ω
hms : MeasurableSet s
hmt : MeasurableSet t
hcs : Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
u : Set Ω
h : MeasurableSet u
⊢ Eq (α := ℝ≥0∞) (μ[|s][u | t] : ℝ≥0∞) (μ[u | s ∩ t] : ℝ≥0∞)
have h : ∀ (hst : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (0 : ℝ≥0∞)),
  Eq (α := ℝ≥0∞) (μ[|s][u | t] : ℝ≥0∞) (μ[u | s ∩ t] : ℝ≥0∞)
Tactic: obtain hst | hst := eq_or_ne (μ (s ∩ t)) 0
-- Lean 4 proof step from Mathlib.Probability.ConditionalProbability (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s t : Set Ω
hms : MeasurableSet s
hmt : MeasurableSet t
hcs : Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
u : Set Ω
h_1 : MeasurableSet u
h :
  ∀ (hst : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (0 : ℝ≥0∞)),
    Eq (α := ℝ≥0∞) (μ[|s][u | t] : ℝ≥0∞) (μ[u | s ∩ t] : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (μ[|s][u | t] : ℝ≥0∞) (μ[u | s ∩ t] : ℝ≥0∞)
have h₁ : ∀ (hst : Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (0 : ℝ≥0∞)),
  Eq (α := ℝ≥0∞) (μ[|s][u | t] : ℝ≥0∞) (μ[u | s ∩ t] : ℝ≥0∞)
Tactic: obtain hst | hst := eq_or_ne (μ (s ∩ t)) 0
-- Lean 4 proof step from Mathlib.Probability.ConditionalProbability (hypothesis)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s t : Set Ω
hms : MeasurableSet s
hmt : MeasurableSet t
hcs : Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
u : Set Ω
h : MeasurableSet u
hst : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (μ[|s][u | t] : ℝ≥0∞) (μ[u | s ∩ t] : ℝ≥0∞)
have this : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t ∩ u) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: have : μ (s ∩ t ∩ u) = 0 := measure_mono_null Set.inter_subset_left hst
-- Lean 4 proof step from Mathlib.Probability.ConditionalProbability (hypothesis)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s t : Set Ω
hms : MeasurableSet s
hmt : MeasurableSet t
hcs : Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
u : Set Ω
h : MeasurableSet u
hst : Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (μ[|s][u | t] : ℝ≥0∞) (μ[u | s ∩ t] : ℝ≥0∞)
have hs : Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: have hs : μ s ≠ 0 := (measure_pos_of_superset Set.inter_subset_left hst).ne'