awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.ConditionalProbability
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∞)
rw₄ 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∞)
⊢ μ[t | s] =
    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]

Premises used: Set.inter_comm, MeasureTheory.Measure.smul_apply, smul_eq_mul, ProbabilityTheory.cond, MeasureTheory.Measure.restrict_apply'
-- Module: Mathlib.Probability.ConditionalProbability
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∞)
rw₄ 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∞)
⊢ μ[t | s] =
    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]

Premises used: MeasureTheory.Measure.restrict_apply, Set.inter_comm, MeasureTheory.Measure.smul_apply, smul_eq_mul, ProbabilityTheory.cond
-- Module: Mathlib.Probability.ConditionalProbability
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s : Set Ω
hs₀ : Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (μ[s | s] : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
simpa [cond] using ENNReal.inv_mul_cancel hs₀ hs

Premises used: ENNReal.inv_mul_cancel, ProbabilityTheory.cond
-- Module: Mathlib.Probability.ConditionalProbability
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]
rw₃ rw₄ : Eq (α := ℝ≥0∞) (μ[t | s] : ℝ≥0∞) (μ[t | s] : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (μ[s ∩ t | s] : ℝ≥0∞) (μ[t | s] : ℝ≥0∞)

Tactic:
rw [cond_apply hms, ← Set.inter_assoc, Set.inter_self, ← cond_apply hms]

Premises used: ProbabilityTheory.cond_apply, Set.inter_self, Set.inter_assoc
-- Module: Mathlib.Probability.ConditionalProbability
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∞)

Tactic:
pos_iff_ne_zero.mpr (right_ne_zero_of_mul (a := (μ s)⁻¹) ?_)

Premises used: Iff.mpr, right_ne_zero_of_mul, pos_iff_ne_zero
-- Module: Mathlib.Probability.ConditionalProbability
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s t : Set Ω
hms : MeasurableSet s
hcst : Ne (α := ℝ≥0∞) (μ[t | s] : ℝ≥0∞) (0 : ℝ≥0∞)
refine :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) ≠
    0
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)

Tactic:
refine pos_iff_ne_zero.mpr (right_ne_zero_of_mul (a := (μ s)⁻¹) ?_)

Premises used: Iff.mpr, right_ne_zero_of_mul, pos_iff_ne_zero
-- Module: Mathlib.Probability.ConditionalProbability
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s t : Set Ω
hms : MeasurableSet s
hcst : Ne (α := ℝ≥0∞) (μ[t | s] : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) (μ[t | s] : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
hcst
-- Module: Mathlib.Probability.ConditionalProbability
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s t : Set Ω
hms : MeasurableSet s
hcst : Ne (α := ℝ≥0∞) (μ[t | s] : ℝ≥0∞) (0 : ℝ≥0∞)
h :
  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∞) ≠
    0

Tactic:
convert! hcst
-- Module: Mathlib.Probability.ConditionalProbability
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∞) =
    μ[t | s]

Tactic:
simp [hms, Set.inter_comm, cond]

Premises used: Set.inter_comm, ProbabilityTheory.cond
-- Module: Mathlib.Probability.ConditionalProbability
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∞)
rw :
  0 <
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) (μ[t | s] : ℝ≥0∞)

Tactic:
rw [cond_apply hms]

Premises used: ProbabilityTheory.cond_apply
-- Module: Mathlib.Probability.ConditionalProbability
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∞)

Tactic:
ENNReal.mul_pos ?_ hci

Premises used: ENNReal.mul_pos
-- Module: Mathlib.Probability.ConditionalProbability
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∞)
refine : Ne (α := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ 0 <
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)

Tactic:
refine ENNReal.mul_pos ?_ hci

Premises used: ENNReal.mul_pos
-- Module: Mathlib.Probability.ConditionalProbability
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∞)
⊢ Ne (α := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
ENNReal.inv_ne_zero.mpr (measure_ne_top _ _)

Premises used: Iff.mpr, MeasureTheory.measure_ne_top, ENNReal.inv_ne_zero
-- Module: Mathlib.Probability.ConditionalProbability
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∞)
⊢ Ne (α := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
exact ENNReal.inv_ne_zero.mpr (measure_ne_top _ _)

Premises used: Iff.mpr, MeasureTheory.measure_ne_top, ENNReal.inv_ne_zero
-- Module: Mathlib.Probability.ConditionalProbability
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∞)
h : ∀ (u : Set Ω), MeasurableSet u → Eq (α := ℝ≥0∞) (μ[|s][u | t] : ℝ≥0∞) (μ[u | s ∩ t] : ℝ≥0∞)
⊢ μ[|s][|t] = μ[|s ∩ t]

Tactic:
ext u
-- Module: Mathlib.Probability.ConditionalProbability
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∞)
h₁ :
  ∀ (hst : Ne (α := ℝ≥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∞)

Tactic:
obtain hst | hst := eq_or_ne (μ (s ∩ t)) 0

Premises used: Inter.inter, eq_or_ne, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Probability.ConditionalProbability
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∞) ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t ∩ u) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
have : μ (s ∩ t ∩ u) = 0 := measure_mono_null Set.inter_subset_left hst
-- Module: Mathlib.Probability.ConditionalProbability
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∞)
this : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t ∩ u) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (μ[|s][u | t] : ℝ≥0∞) (μ[u | s ∩ t] : ℝ≥0∞)

Tactic:
simp [cond_apply, *, ← Set.inter_assoc]

Premises used: ProbabilityTheory.cond_apply, Set.inter_assoc
-- Module: Mathlib.Probability.ConditionalProbability
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∞)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
have hs : μ s ≠ 0 := (measure_pos_of_superset Set.inter_subset_left hst).ne'
-- Module: Mathlib.Probability.ConditionalProbability
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∞)
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (μ[|s][u | t] : ℝ≥0∞) (μ[u | s ∩ t] : ℝ≥0∞)

Tactic:
simp [*, hms.inter hmt, cond_apply, ← Set.inter_assoc, ENNReal.mul_inv, ← mul_assoc,
      mul_comm _ (μ s)⁻¹, ENNReal.inv_mul_cancel]

Premises used: ProbabilityTheory.cond_apply, mul_assoc, Inv.inv, mul_comm, ENNReal.inv_mul_cancel, ENNReal.mul_inv, DFunLike.coe, Set.inter_assoc, MeasurableSet.inter
-- Module: Mathlib.Probability.ConditionalProbability
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
s t : Set Ω
hms : MeasurableSet s
hmt : MeasurableSet t
μ : Measure Ω
inst : IsFiniteMeasure μ
⊢ μ[|s][|t] = μ[|s ∩ t]

Tactic:
cond_cond_eq_cond_inter' hms hmt (measure_ne_top μ s)

Premises used: MeasureTheory.measure_ne_top, ProbabilityTheory.cond_cond_eq_cond_inter'
-- Module: Mathlib.Probability.ConditionalProbability
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)
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)
⊢ 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

Premises used: eq_or_ne, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Probability.ConditionalProbability
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s : Set Ω
hms : MeasurableSet s
hcs' : Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
t : Set Ω
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:
simp [hcs, measure_inter_null_of_null_left]

Premises used: MeasureTheory.measure_inter_null_of_null_left
-- Module: Mathlib.Probability.ConditionalProbability
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)
inr₄ inr₅ : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (μ[t | s] : ℝ≥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]

Premises used: ProbabilityTheory.cond_apply, mul_assoc, ENNReal.mul_inv_cancel, mul_comm, one_mul
-- Module: Mathlib.Probability.ConditionalProbability
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
s : Set Ω
hms : MeasurableSet s
t : Set Ω
μ : Measure Ω
inst : IsFiniteMeasure μ
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (μ[t | s] : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) =
    (μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t)

Tactic:
cond_mul_eq_inter' hms (measure_ne_top _ s) t

Premises used: MeasureTheory.measure_ne_top, ProbabilityTheory.cond_mul_eq_inter'
-- Module: Mathlib.Probability.ConditionalProbability
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
s t : Set Ω
hms : MeasurableSet s
μ : Measure Ω
inst : IsFiniteMeasure μ
rw :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
      ((μ : (a : Set Ω) → ℝ≥0∞) (t ∩ sᶜ) : ℝ≥0∞) =
    (μ : (a : Set Ω) → ℝ≥0∞) t
⊢ 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

Tactic:
rw [cond_mul_eq_inter hms, cond_mul_eq_inter hms.compl, Set.inter_comm _ t,
    Set.inter_comm _ t]

Premises used: MeasurableSet.compl, Set.inter_comm, ProbabilityTheory.cond_mul_eq_inter
-- Module: Mathlib.Probability.ConditionalProbability
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
s t : Set Ω
hms : MeasurableSet s
μ : Measure Ω
inst : IsFiniteMeasure μ
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
      ((μ : (a : Set Ω) → ℝ≥0∞) (t ∩ sᶜ) : ℝ≥0∞) =
    (μ : (a : Set Ω) → ℝ≥0∞) t

Tactic:
measure_inter_add_diff t hms

Premises used: Set.Mem, setOf, Set.inter, MeasureTheory.measure_inter_add_diff, Not
-- Module: Mathlib.Probability.ConditionalProbability
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
s t : Set Ω
hms : MeasurableSet s
μ : Measure Ω
inst : IsFiniteMeasure μ
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
      ((μ : (a : Set Ω) → ℝ≥0∞) (t ∩ sᶜ) : ℝ≥0∞) =
    (μ : (a : Set Ω) → ℝ≥0∞) t

Tactic:
exact measure_inter_add_diff t hms

Premises used: MeasureTheory.measure_inter_add_diff
-- Module: Mathlib.Probability.ConditionalProbability
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∞)
rw₃ 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∞)
⊢ μ[t | s] =
    HMul.hMul (β := ℝ≥0∞) (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥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]

Premises used: ProbabilityTheory.cond_apply, mul_assoc, Set.inter_comm, ProbabilityTheory.cond_mul_eq_inter
-- Module: Mathlib.Probability.ConditionalProbability
Goal:
Ω : Type u_1
Ω' : Type u_2
m : MeasurableSpace Ω
m' : MeasurableSpace Ω'
μ : Measure Ω
s : Set Ω
i : Ω' → Ω
hi : MeasurableEmbedding i
hi' : ∀ᵐ (ω : Ω) ∂μ, ω ∈ range i
hs : MeasurableSet s
h :
  ∀ (t : Set Ω') (ht : MeasurableSet t),
    Eq (α := ℝ≥0∞) (((comap i μ[|s] : Measure Ω') : (a : Set Ω') → ℝ≥0∞) t : ℝ≥0∞) ((comap i μ)[t | i ⁻¹' s] : ℝ≥0∞)
⊢ Eq (α := Measure Ω') (comap i μ[|s]) (comap i μ)[|i ⁻¹' s]

Tactic:
ext t ht
-- Module: Mathlib.Probability.ConditionalProbability
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∞) ((μ : (a : Set Ω) → ℝ≥0∞) (range i)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
change μ (range i)ᶜ = 0 at hi'

Premises used: Compl.compl, Set.range, DFunLike.coe
-- Module: Mathlib.Probability.ConditionalProbability
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)
h₆ : MeasurableSet (i ⁻¹' s)
h₇ : MeasurableSet s
h₈ : Function.Injective i
h₉ : ∀ (s : Set Ω'), MeasurableSet s → MeasurableSet (i '' s)
h₁₀ : MeasurableSet t
h₁₁ : MeasurableSet (i ⁻¹' s)
⊢ Eq (α := ℝ≥0∞) (((comap i μ[|s] : Measure Ω') : (a : Set Ω') → ℝ≥0∞) t : ℝ≥0∞) ((comap i μ)[t | i ⁻¹' s] : ℝ≥0∞)

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']

Premises used: ProbabilityTheory.cond_apply, Set.image_inter, MeasureTheory.Measure.comap_apply, Set.image_preimage_eq_inter_range, Set.inter_right_comm, MeasureTheory.measure_inter_conull
-- Module: Mathlib.Probability.ConditionalProbability
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∞)
⊢ Function.Injective i

Tactic:
hi.injective

Premises used: MeasurableEmbedding.injective
-- Module: Mathlib.Probability.ConditionalProbability
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∞)
⊢ Function.Injective i

Tactic:
exact hi.injective

Premises used: MeasurableEmbedding.injective
-- Module: Mathlib.Probability.ConditionalProbability
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∞)
⊢ Function.Injective i

Tactic:
first
  | exact hi.injective
  | exact hi.measurableSet_image'
  | exact hs
  | exact ht
  | exact hi.measurable hs
  | exact (hi.measurable hs).inter ht

Premises used: MeasurableEmbedding.measurableSet_image', MeasurableEmbedding.injective, MeasurableEmbedding.measurable, MeasurableSet.inter
-- Module: Mathlib.Probability.ConditionalProbability
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∞)
⊢ ∀ (s : Set Ω'), MeasurableSet s → MeasurableSet (i '' s)

Tactic:
hi.injective

Premises used: MeasurableEmbedding.injective
-- Module: Mathlib.Probability.ConditionalProbability
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∞)
⊢ ∀ (s : Set Ω'), MeasurableSet s → MeasurableSet (i '' s)

Tactic:
hi.measurableSet_image'

Premises used: MeasurableEmbedding.measurableSet_image'
-- Module: Mathlib.Probability.ConditionalProbability
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∞)
⊢ ∀ (s : Set Ω'), MeasurableSet s → MeasurableSet (i '' s)

Tactic:
exact hi.measurableSet_image'

Premises used: MeasurableEmbedding.measurableSet_image'