awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
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∞)
⊢ MeasurableSet (i ⁻¹' s ∩ t)

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∞)
⊢ MeasurableSet (i ⁻¹' s ∩ t)

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∞)
⊢ MeasurableSet (i ⁻¹' s ∩ t)

Tactic:
hs
-- 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∞)
⊢ MeasurableSet (i ⁻¹' s ∩ t)

Tactic:
ht
-- 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∞)
⊢ MeasurableSet (i ⁻¹' s ∩ t)

Tactic:
hi.measurable hs

Premises used: MeasurableEmbedding.measurable
-- 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∞)
⊢ MeasurableSet (i ⁻¹' s ∩ t)

Tactic:
(hi.measurable hs).inter ht

Premises used: 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∞)
⊢ MeasurableSet (i ⁻¹' s ∩ t)

Tactic:
exact (hi.measurable hs).inter ht

Premises used: 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∞)
⊢ MeasurableSet (i ⁻¹' s ∩ t)

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∞)
⊢ 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∞)
⊢ 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∞)
⊢ MeasurableSet (i ⁻¹' s)

Tactic:
hs
-- 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∞)
⊢ MeasurableSet (i ⁻¹' s)

Tactic:
ht
-- 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∞)
⊢ MeasurableSet (i ⁻¹' s)

Tactic:
hi.measurable hs

Premises used: MeasurableEmbedding.measurable
-- 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∞)
⊢ MeasurableSet (i ⁻¹' s)

Tactic:
exact hi.measurable hs

Premises used: MeasurableEmbedding.measurable
-- 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∞)
⊢ MeasurableSet (i ⁻¹' s)

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∞)
⊢ MeasurableSet 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∞)
⊢ MeasurableSet 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∞)
⊢ MeasurableSet s

Tactic:
hs
-- 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∞)
⊢ MeasurableSet s

Tactic:
exact hs
-- 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∞)
⊢ MeasurableSet s

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∞)
⊢ MeasurableSet t

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∞)
⊢ MeasurableSet t

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∞)
⊢ MeasurableSet t

Tactic:
hs
-- 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∞)
⊢ MeasurableSet t

Tactic:
ht
-- 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∞)
⊢ MeasurableSet t

Tactic:
exact ht
-- 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∞)
⊢ MeasurableSet t

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_3
m : MeasurableSpace Ω
inst : Fintype α
inst_1 : MeasurableSpace α
inst_2 : DiscreteMeasurableSpace α
X : Ω → α
hX : Measurable X
μ : Measure Ω
inst_3 : IsFiniteMeasure μ
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∞)
⊢ ∑ x : α, HSMul.hSMul (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (X ⁻¹' {x}) : ℝ≥0∞) μ[|X ⁻¹' {x}] = μ

Tactic:
ext E hE
-- Module: Mathlib.Probability.ConditionalProbability
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
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))
⊢ 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:
simp only [Measure.coe_finsetSum, Measure.coe_smul, Finset.sum_apply,
        Pi.smul_apply, smul_eq_mul]

Premises used: MeasureTheory.Measure.coe_finsetSum, Finset.sum_apply, MeasureTheory.Measure.coe_smul, smul_eq_mul, Pi.smul_apply
-- Module: Mathlib.Probability.ConditionalProbability
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
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))
⊢ 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_rw [mul_comm (μ _), cond_mul_eq_inter (hX (.singleton _))]

Premises used: MeasurableSet.singleton, mul_comm, ProbabilityTheory.cond_mul_eq_inter, DFunLike.coe
-- Module: Mathlib.Probability.ConditionalProbability
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
h :
  ∀ (x : Ω),
    Membership.mem (γ := Set Ω) (⋃ (x : α), ⋃ (_ : Membership.mem (γ := Finset α) Finset.univ x), X ⁻¹' {x} ∩ E) x ↔
      x ∈ E
⊢ ⋃ (x : α), ⋃ (_ : Membership.mem (γ := Finset α) Finset.univ x), X ⁻¹' {x} ∩ E = E

Tactic:
ext
-- Module: Mathlib.Probability.ConditionalProbability
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 (γ := Set Ω) (⋃ (x : α), ⋃ (_ : Membership.mem (γ := Finset α) Finset.univ x), X ⁻¹' {x} ∩ E) x ↔ x ∈ E

Tactic:
simp
-- Module: Mathlib.Probability.ConditionalProbability
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

Tactic:
have : ⋃ x ∈ Finset.univ, X ⁻¹' {x} ∩ E = E := by ext; simp
-- Module: Mathlib.Probability.ConditionalProbability
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
rw : PairwiseDisjoint.{u_1, u_3} (α := Set Ω) (↑Finset.univ : Set α) fun (x : α) ↦ X ⁻¹' {x} ∩ E
⊢ Eq (α := ℝ≥0∞) (∑ x : α, (μ : (a : Set Ω) → ℝ≥0∞) (X ⁻¹' {x} ∩ E) : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) E : ℝ≥0∞)

Tactic:
rw [← measure_biUnion_finset _ fun _ _ ↦ (hX (.singleton _)).inter hE, this]

Premises used: MeasurableSet.singleton, MeasureTheory.measure_biUnion_finset, MeasurableSet.inter
-- Module: Mathlib.Probability.ConditionalProbability
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
⊢ PairwiseDisjoint.{u_1, u_3} (α := Set Ω) (↑Finset.univ : Set α) fun (x : α) ↦ X ⁻¹' {x} ∩ E

Tactic:
aesop (add simp [PairwiseDisjoint, Set.Pairwise, Function.onFun, disjoint_left])

Premises used: Function.onFun, Set.disjoint_left, Set.PairwiseDisjoint, Set.Pairwise
-- Module: Mathlib.Probability.ConditionalProbability
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 : α, (μ : (a : Set Ω) → ℝ≥0∞) (X ⁻¹' {x} ∩ E) : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) 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∞)

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])
-- Module: Mathlib.Probability.Decision.Risk.Basic
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
κ : Kernel 𝓧 𝓨
π : Measure Θ
inst : IsProbabilityMeasure π
⊢ avgRisk ℓ P κ π ≤ ⨆ (θ : Θ), ∫⁻ (y : 𝓨), ℓ θ y ∂(κ ∘ₖ P : (a : Θ) → Measure 𝓨) θ

Tactic:
lintegral_le_iSup _

Premises used: ProbabilityTheory.avgRisk, MeasureTheory.lintegral_le_iSup
-- Module: Mathlib.Probability.Decision.Risk.Basic
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
κ : Kernel 𝓧 𝓨
π : Measure Θ
hκ : IsMarkovKernel κ
⊢ bayesRisk ℓ P π ≤ avgRisk ℓ P κ π

Tactic:
iInf₂_le κ hκ

Premises used: ProbabilityTheory.bayesRisk, iInf₂_le
-- Module: Mathlib.Probability.Decision.Risk.Basic
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
π : Measure Θ
inst : IsProbabilityMeasure π
⊢ bayesRisk ℓ P π ≤ minimaxRisk ℓ P

Tactic:
iInf₂_mono fun _ _ ↦ avgRisk_le_iSup_risk _ _ _ _

Premises used: ProbabilityTheory.bayesRisk, ProbabilityTheory.minimaxRisk, ProbabilityTheory.avgRisk_le_iSup_risk, iInf₂_mono
-- Module: Mathlib.Probability.Decision.Risk.Basic
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
⊢ ⨆ (π : Measure Θ), ⨆ (_ : IsProbabilityMeasure π), bayesRisk ℓ P π ≤ minimaxRisk ℓ P

Tactic:
iSup₂_le fun _ _ ↦ bayesRisk_le_minimaxRisk _ _ _

Premises used: iSup₂_le, ProbabilityTheory.bayesRisk_le_minimaxRisk
-- Module: Mathlib.Probability.Decision.Risk.Basic
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
μ : Measure 𝓧
κ : Kernel 𝓧 𝓨
π : Measure Θ
⊢ avgRisk ℓ (Kernel.const Θ μ) κ π = ∫⁻ (θ : Θ), ∫⁻ (y : 𝓨), ℓ θ y ∂(⇑κ : (a : 𝓧) → Measure 𝓨) ∘ₘ μ ∂π

Tactic:
simp [avgRisk]

Premises used: ProbabilityTheory.avgRisk
-- Module: Mathlib.Probability.Decision.Risk.Basic
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 π
⊢ AEMeasurable (_m := Prod.instMeasurableSpace) (uncurry ℓ) (π.prod ((⇑κ : (a : 𝓧) → Measure 𝓨) ∘ₘ μ))

Tactic:
fun_prop
-- Module: Mathlib.Probability.Decision.Risk.Basic
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 𝓨) ∘ₘ μ
rw₁ rw₂ :
  ∫⁻ (y : 𝓨), ∫⁻ (x : Θ), ℓ x y ∂π ∂(⇑κ : (a : 𝓧) → Measure 𝓨) ∘ₘ μ =
    ∫⁻ (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y ∂π ∂(⇑κ : (a : 𝓧) → Measure 𝓨) ∘ₘ μ
⊢ avgRisk ℓ (Kernel.const Θ μ) κ π = ∫⁻ (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y ∂π ∂(⇑κ : (a : 𝓧) → Measure 𝓨) ∘ₘ μ

Tactic:
rw [avgRisk_const_left, lintegral_lintegral_swap (by fun_prop)]

Premises used: ProbabilityTheory.avgRisk_const_left, MeasureTheory.lintegral_lintegral_swap
-- Module: Mathlib.Probability.Decision.Risk.Basic
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
ν : Measure 𝓨
π : Measure Θ
⊢ avgRisk ℓ P (Kernel.const 𝓧 ν) π =
    ∫⁻ (θ : Θ),
      HMul.hMul (α := ℝ≥0∞) ((((P : (a : Θ) → Measure 𝓧) θ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞)
        (∫⁻ (y : 𝓨), ℓ θ y ∂ν) ∂π

Tactic:
simp [avgRisk, Kernel.const_comp]

Premises used: ProbabilityTheory.avgRisk, ProbabilityTheory.Kernel.const_comp
-- Module: Mathlib.Probability.Decision.Risk.Basic
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
inst : IsMarkovKernel P
ν : Measure 𝓨
π : Measure Θ
⊢ avgRisk ℓ P (Kernel.const 𝓧 ν) π = ∫⁻ (θ : Θ), ∫⁻ (y : 𝓨), ℓ θ y ∂ν ∂π

Tactic:
simp [avgRisk_const_right']

Premises used: ProbabilityTheory.avgRisk_const_right'
-- Module: Mathlib.Probability.Decision.Risk.Basic
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
hl : Measurable (uncurry ℓ)
P : Kernel Θ 𝓧
π : Measure Θ
simp_rw :
  ∀ (i : 𝓨),
    ⨅ (κ : Kernel 𝓧 𝓨), ⨅ (_ : IsMarkovKernel κ), avgRisk ℓ P κ π ≤
      ∫⁻ (θ : Θ),
        HMul.hMul (β := ℝ≥0∞) (ℓ θ i)
          ((((P : (a : Θ) → Measure 𝓧) θ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) ∂π
⊢ bayesRisk ℓ P π ≤
    ⨅ (y : 𝓨),
      ∫⁻ (θ : Θ),
        HMul.hMul (β := ℝ≥0∞) (ℓ θ y)
          ((((P : (a : Θ) → Measure 𝓧) θ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) ∂π

Tactic:
simp_rw [le_iInf_iff, bayesRisk]

Premises used: ProbabilityTheory.bayesRisk, le_iInf_iff