awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Distributions.Uniform (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : Nonempty α
s : Set α
inst_2 : Fintype (↑s : Type u_1)
rw :
  ((toOuterMeasure (uniformOfFinset Finset.univ ⋯) : MeasureTheory.OuterMeasure α) : (a : Set α) → ℝ≥0∞) s =
    HDiv.hDiv (α := ℝ≥0∞) (↑(Fintype.card.{u_1} (↑s : Type u_1)) : ℝ≥0∞) (↑(Fintype.card α) : ℝ≥0∞)
rw₁ :
  HDiv.hDiv (α := ℝ≥0∞) (↑(Finset.card.{u_1} (α := α) {x : α | x ∈ s}) : ℝ≥0∞)
      (↑(Finset.card.{u_1} (α := α) Finset.univ) : ℝ≥0∞) =
    HDiv.hDiv (α := ℝ≥0∞) (↑(Fintype.card.{u_1} (↑s : Type u_1)) : ℝ≥0∞) (↑(Fintype.card α) : ℝ≥0∞)
rw₂ :
  HDiv.hDiv (α := ℝ≥0∞) (↑(Finset.card.{u_1} (α := α) {x : α | x ∈ s}) : ℝ≥0∞)
      (↑(Finset.card.{u_1} (α := α) Finset.univ) : ℝ≥0∞) =
    HDiv.hDiv (α := ℝ≥0∞) (↑(Finset.card.{u_1} (α := α) {x : α | x ∈ s}) : ℝ≥0∞) (↑(Fintype.card α) : ℝ≥0∞)
⊢ ((uniformOfFintype α).toOuterMeasure : (a : Set α) → ℝ≥0∞) s =
    HDiv.hDiv (α := ℝ≥0∞) (↑(Fintype.card.{u_1} (↑s : Type u_1)) : ℝ≥0∞) (↑(Fintype.card α) : ℝ≥0∞)
have rw₃ : HDiv.hDiv (α := ℝ≥0∞) (↑(Finset.card.{u_1} (α := α) {x : α | x ∈ s}) : ℝ≥0∞) (↑(Fintype.card α) : ℝ≥0∞) =
  HDiv.hDiv (α := ℝ≥0∞) (↑(Finset.card.{u_1} (α := α) {x : α | x ∈ s}) : ℝ≥0∞) (↑(Fintype.card α) : ℝ≥0∞)
Tactic: rw [uniformOfFintype, toOuterMeasure_uniformOfFinset_apply, Fintype.card_subtype,
    Finset.card_univ]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Uniform (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : Nonempty α
s : Set α
inst_2 : Fintype (↑s : Type u_1)
⊢ ((uniformOfFintype α).toOuterMeasure : (a : Set α) → ℝ≥0∞) s =
    HDiv.hDiv (α := ℝ≥0∞) (↑(Fintype.card.{u_1} (↑s : Type u_1)) : ℝ≥0∞) (↑(Fintype.card α) : ℝ≥0∞)
have rw : ((toOuterMeasure (uniformOfFinset Finset.univ sorry) : MeasureTheory.OuterMeasure α) : (a : Set α) → ℝ≥0∞) s =
  HDiv.hDiv (α := ℝ≥0∞) (↑(Fintype.card.{u_1} (↑s : Type u_1)) : ℝ≥0∞) (↑(Fintype.card α) : ℝ≥0∞)
Tactic: classical
  rw [uniformOfFintype, toOuterMeasure_uniformOfFinset_apply, Fintype.card_subtype,
    Finset.card_univ]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Uniform (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : Nonempty α
s : Set α
inst_2 : Fintype (↑s : Type u_1)
rw :
  ((toOuterMeasure (uniformOfFinset Finset.univ ⋯) : MeasureTheory.OuterMeasure α) : (a : Set α) → ℝ≥0∞) s =
    HDiv.hDiv (α := ℝ≥0∞) (↑(Fintype.card.{u_1} (↑s : Type u_1)) : ℝ≥0∞) (↑(Fintype.card α) : ℝ≥0∞)
⊢ ((uniformOfFintype α).toOuterMeasure : (a : Set α) → ℝ≥0∞) s =
    HDiv.hDiv (α := ℝ≥0∞) (↑(Fintype.card.{u_1} (↑s : Type u_1)) : ℝ≥0∞) (↑(Fintype.card α) : ℝ≥0∞)
have rw₁ : HDiv.hDiv (α := ℝ≥0∞) (↑(Finset.card.{u_1} (α := α) {x : α | x ∈ s}) : ℝ≥0∞)
    (↑(Finset.card.{u_1} (α := α) Finset.univ) : ℝ≥0∞) =
  HDiv.hDiv (α := ℝ≥0∞) (↑(Fintype.card.{u_1} (↑s : Type u_1)) : ℝ≥0∞) (↑(Fintype.card α) : ℝ≥0∞)
Tactic: classical
  rw [uniformOfFintype, toOuterMeasure_uniformOfFinset_apply, Fintype.card_subtype,
    Finset.card_univ]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Uniform (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : Nonempty α
s : Set α
inst_2 : Fintype (↑s : Type u_1)
rw :
  ((toOuterMeasure (uniformOfFinset Finset.univ ⋯) : MeasureTheory.OuterMeasure α) : (a : Set α) → ℝ≥0∞) s =
    HDiv.hDiv (α := ℝ≥0∞) (↑(Fintype.card.{u_1} (↑s : Type u_1)) : ℝ≥0∞) (↑(Fintype.card α) : ℝ≥0∞)
rw₁ :
  HDiv.hDiv (α := ℝ≥0∞) (↑(Finset.card.{u_1} (α := α) {x : α | x ∈ s}) : ℝ≥0∞)
      (↑(Finset.card.{u_1} (α := α) Finset.univ) : ℝ≥0∞) =
    HDiv.hDiv (α := ℝ≥0∞) (↑(Fintype.card.{u_1} (↑s : Type u_1)) : ℝ≥0∞) (↑(Fintype.card α) : ℝ≥0∞)
⊢ ((uniformOfFintype α).toOuterMeasure : (a : Set α) → ℝ≥0∞) s =
    HDiv.hDiv (α := ℝ≥0∞) (↑(Fintype.card.{u_1} (↑s : Type u_1)) : ℝ≥0∞) (↑(Fintype.card α) : ℝ≥0∞)
have rw₂ : HDiv.hDiv (α := ℝ≥0∞) (↑(Finset.card.{u_1} (α := α) {x : α | x ∈ s}) : ℝ≥0∞)
    (↑(Finset.card.{u_1} (α := α) Finset.univ) : ℝ≥0∞) =
  HDiv.hDiv (α := ℝ≥0∞) (↑(Finset.card.{u_1} (α := α) {x : α | x ∈ s}) : ℝ≥0∞) (↑(Fintype.card α) : ℝ≥0∞)
Tactic: classical
  rw [uniformOfFintype, toOuterMeasure_uniformOfFinset_apply, Fintype.card_subtype,
    Finset.card_univ]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Uniform (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : Nonempty α
s : Set α
inst_2 : Fintype (↑s : Type u_1)
rw :
  ((toOuterMeasure (uniformOfFinset Finset.univ ⋯) : MeasureTheory.OuterMeasure α) : (a : Set α) → ℝ≥0∞) s =
    HDiv.hDiv (α := ℝ≥0∞) (↑(Fintype.card.{u_1} (↑s : Type u_1)) : ℝ≥0∞) (↑(Fintype.card α) : ℝ≥0∞)
rw₁ :
  HDiv.hDiv (α := ℝ≥0∞) (↑(Finset.card.{u_1} (α := α) {x : α | x ∈ s}) : ℝ≥0∞)
      (↑(Finset.card.{u_1} (α := α) Finset.univ) : ℝ≥0∞) =
    HDiv.hDiv (α := ℝ≥0∞) (↑(Fintype.card.{u_1} (↑s : Type u_1)) : ℝ≥0∞) (↑(Fintype.card α) : ℝ≥0∞)
rw₂ :
  HDiv.hDiv (α := ℝ≥0∞) (↑(Finset.card.{u_1} (α := α) {x : α | x ∈ s}) : ℝ≥0∞)
      (↑(Finset.card.{u_1} (α := α) Finset.univ) : ℝ≥0∞) =
    HDiv.hDiv (α := ℝ≥0∞) (↑(Finset.card.{u_1} (α := α) {x : α | x ∈ s}) : ℝ≥0∞) (↑(Fintype.card α) : ℝ≥0∞)
⊢ ((uniformOfFintype α).toOuterMeasure : (a : Set α) → ℝ≥0∞) s =
    HDiv.hDiv (α := ℝ≥0∞) (↑(Fintype.card.{u_1} (↑s : Type u_1)) : ℝ≥0∞) (↑(Fintype.card α) : ℝ≥0∞)
have rw₃ : HDiv.hDiv (α := ℝ≥0∞) (↑(Finset.card.{u_1} (α := α) {x : α | x ∈ s}) : ℝ≥0∞) (↑(Fintype.card α) : ℝ≥0∞) =
  HDiv.hDiv (α := ℝ≥0∞) (↑(Finset.card.{u_1} (α := α) {x : α | x ∈ s}) : ℝ≥0∞) (↑(Fintype.card α) : ℝ≥0∞)
Tactic: classical
  rw [uniformOfFintype, toOuterMeasure_uniformOfFinset_apply, Fintype.card_subtype,
    Finset.card_univ]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Uniform (goal)
Goal:
α : Type u_1
s : Multiset α
hs : s ≠ 0
⊢ ∑' (b : α), HDiv.hDiv (α := ℝ≥0∞) (↑(Multiset.count b s) : ℝ≥0∞) (↑s.card : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (↑s.card : ℝ≥0∞)⁻¹ (∑' (b : α), (↑(Multiset.count b s) : ℝ≥0∞))
have simp_rw : ∑' (b : α), HMul.hMul (α := ℝ≥0∞) (↑s.card : ℝ≥0∞)⁻¹ (↑(Multiset.count b s) : ℝ≥0∞) =
  HMul.hMul (α := ℝ≥0∞) (↑s.card : ℝ≥0∞)⁻¹ (∑' (b : α), (↑(Multiset.count b s) : ℝ≥0∞))
Tactic: simp_rw [ENNReal.div_eq_inv_mul, ENNReal.tsum_mul_left]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Uniform (goal)
Goal:
α : Type u_1
s : Multiset α
hs : s ≠ 0
a : α
ha : a ∉ s.toFinset
⊢ Multiset.count a s = 0
have rwa : a ∉ s
Tactic: rwa [Multiset.count_eq_zero, ← Multiset.mem_toFinset]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Uniform (goal)
Goal:
α : Type u_1
s : Multiset α
hs : s ≠ 0
⊢ HMul.hMul (α := ℝ≥0∞) (↑s.card : ℝ≥0∞)⁻¹ (∑ b ∈ s.toFinset, (↑(Multiset.count b s) : ℝ≥0∞)) = 1
have rw : HMul.hMul (α := ℝ≥0∞) (↑s.card : ℝ≥0∞)⁻¹ (↑(∑ x ∈ s.toFinset, Multiset.count x s) : ℝ≥0∞) = 1
Tactic: rw [← Nat.cast_sum, Multiset.toFinset_sum_count_eq s,
            ENNReal.inv_mul_cancel (Nat.cast_ne_zero.2 (hs ∘ Multiset.card_eq_zero.1))
              (ENNReal.natCast_ne_top _)]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Uniform (goal)
Goal:
α : Type u_1
s : Multiset α
hs : s ≠ 0
rw : HMul.hMul (α := ℝ≥0∞) (↑s.card : ℝ≥0∞)⁻¹ (↑(∑ x ∈ s.toFinset, Multiset.count x s) : ℝ≥0∞) = 1
⊢ HMul.hMul (α := ℝ≥0∞) (↑s.card : ℝ≥0∞)⁻¹ (∑ b ∈ s.toFinset, (↑(Multiset.count b s) : ℝ≥0∞)) = 1
have rw₁ : HMul.hMul (α := ℝ≥0∞) (↑s.card : ℝ≥0∞)⁻¹ (↑s.card : ℝ≥0∞) = 1
Tactic: rw [← Nat.cast_sum, Multiset.toFinset_sum_count_eq s,
            ENNReal.inv_mul_cancel (Nat.cast_ne_zero.2 (hs ∘ Multiset.card_eq_zero.1))
              (ENNReal.natCast_ne_top _)]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Uniform (goal)
Goal:
α : Type u_1
s : Multiset α
hs : s ≠ 0
rw : HMul.hMul (α := ℝ≥0∞) (↑s.card : ℝ≥0∞)⁻¹ (↑(∑ x ∈ s.toFinset, Multiset.count x s) : ℝ≥0∞) = 1
rw₁ : HMul.hMul (α := ℝ≥0∞) (↑s.card : ℝ≥0∞)⁻¹ (↑s.card : ℝ≥0∞) = 1
⊢ HMul.hMul (α := ℝ≥0∞) (↑s.card : ℝ≥0∞)⁻¹ (∑ b ∈ s.toFinset, (↑(Multiset.count b s) : ℝ≥0∞)) = 1
have rw₂ : Eq (α := ℝ≥0∞) 1 1
Tactic: rw [← Nat.cast_sum, Multiset.toFinset_sum_count_eq s,
            ENNReal.inv_mul_cancel (Nat.cast_ne_zero.2 (hs ∘ Multiset.card_eq_zero.1))
              (ENNReal.natCast_ne_top _)]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Uniform (goal)
Goal:
α : Type u_1
s : Multiset α
hs : s ≠ 0
t : Set α
⊢ ((ofMultiset s hs).toOuterMeasure : (a : Set α) → ℝ≥0∞) t =
    HDiv.hDiv (α := ℝ≥0∞) (∑' (x : α), (↑(Multiset.count x (Multiset.filter (fun (x : α) ↦ x ∈ t) s)) : ℝ≥0∞))
      (↑s.card : ℝ≥0∞)
have simp_rw : Eq (α := ℝ≥0∞) (∑' (x : α), t.indicator (⇑(ofMultiset s hs) : (a : α) → ℝ≥0∞) x)
  (∑' (i : α),
    HMul.hMul (α := ℝ≥0∞) (↑(Multiset.count i (Multiset.filter (fun (x : α) ↦ x ∈ t) s)) : ℝ≥0∞) (↑s.card : ℝ≥0∞)⁻¹)
Tactic: simp_rw [div_eq_mul_inv, ← ENNReal.tsum_mul_right, toOuterMeasure_apply]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Uniform (goal)
Goal:
α : Type u_1
s : Multiset α
hs : s ≠ 0
t : Set α
⊢ Eq (α := ℝ≥0∞) (∑' (x : α), t.indicator (⇑(ofMultiset s hs) : (a : α) → ℝ≥0∞) x)
    (∑' (i : α),
      HMul.hMul (α := ℝ≥0∞) (↑(Multiset.count i (Multiset.filter (fun (x : α) ↦ x ∈ t) s)) : ℝ≥0∞) (↑s.card : ℝ≥0∞)⁻¹)
have refine : ∀ (x : α),
  t.indicator (⇑(ofMultiset s hs) : (a : α) → ℝ≥0∞) x =
    HMul.hMul (α := ℝ≥0∞) (↑(Multiset.count x (Multiset.filter (fun (x : α) ↦ x ∈ t) s)) : ℝ≥0∞) (↑s.card : ℝ≥0∞)⁻¹
Tactic: refine tsum_congr fun x => ?_
-- Lean 4 proof step from Mathlib.Probability.Distributions.Uniform (goal)
Goal:
α : Type u_1
s : Multiset α
hs : s ≠ 0
t : Set α
x : α
⊢ t.indicator (⇑(ofMultiset s hs) : (a : α) → ℝ≥0∞) x =
    HMul.hMul (α := ℝ≥0∞) (↑(Multiset.count x (Multiset.filter (fun (x : α) ↦ x ∈ t) s)) : ℝ≥0∞) (↑s.card : ℝ≥0∞)⁻¹
have pos : ∀ (hx : x ∈ t),
  t.indicator (⇑(ofMultiset s hs) : (a : α) → ℝ≥0∞) x =
    HMul.hMul (α := ℝ≥0∞) (↑(Multiset.count x (Multiset.filter (fun (x : α) ↦ x ∈ t) s)) : ℝ≥0∞) (↑s.card : ℝ≥0∞)⁻¹
Tactic: by_cases hx : x ∈ t
-- Lean 4 proof step from Mathlib.Probability.Distributions.Uniform (goal)
Goal:
α : Type u_1
s : Multiset α
hs : s ≠ 0
t : Set α
x : α
pos :
  ∀ (hx : x ∈ t),
    t.indicator (⇑(ofMultiset s hs) : (a : α) → ℝ≥0∞) x =
      HMul.hMul (α := ℝ≥0∞) (↑(Multiset.count x (Multiset.filter (fun (x : α) ↦ x ∈ t) s)) : ℝ≥0∞) (↑s.card : ℝ≥0∞)⁻¹
⊢ t.indicator (⇑(ofMultiset s hs) : (a : α) → ℝ≥0∞) x =
    HMul.hMul (α := ℝ≥0∞) (↑(Multiset.count x (Multiset.filter (fun (x : α) ↦ x ∈ t) s)) : ℝ≥0∞) (↑s.card : ℝ≥0∞)⁻¹
have neg : ∀ (hx : x ∉ t),
  t.indicator (⇑(ofMultiset s hs) : (a : α) → ℝ≥0∞) x =
    HMul.hMul (α := ℝ≥0∞) (↑(Multiset.count x (Multiset.filter (fun (x : α) ↦ x ∈ t) s)) : ℝ≥0∞) (↑s.card : ℝ≥0∞)⁻¹
Tactic: by_cases hx : x ∈ t
-- Lean 4 proof step from Mathlib.Probability.HasLaw (goal)
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
hX : HasLaw X μ P
p : 𝓧 → Prop
hp : MeasurableSet.{u_2} (α := 𝓧) {x : 𝓧 | p x}
⊢ Eq (α := ℝ≥0∞) ((P : (a : Set Ω) → ℝ≥0∞) {ω : Ω | p (X ω)} : ℝ≥0∞) ((μ : (a : Set 𝓧) → ℝ≥0∞) {x : 𝓧 | p x} : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((P : (a : Set Ω) → ℝ≥0∞) {ω : Ω | p (X ω)} : ℝ≥0∞)
  ((P : (a : Set Ω) → ℝ≥0∞) (X ⁻¹' {x : 𝓧 | p x}) : ℝ≥0∞)
Tactic: rw [← hX.map_eq, map_apply_of_aemeasurable hX.aemeasurable hp]
-- Lean 4 proof step from Mathlib.Probability.HasLaw (goal)
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
hX : HasLaw X μ P
p : 𝓧 → Prop
hp : MeasurableSet.{u_2} (α := 𝓧) {x : 𝓧 | p x}
⊢ P.real {ω : Ω | p (X ω)} = μ.real {x : 𝓧 | p x}
have rw : P.real {ω : Ω | p (X ω)} = P.real (X ⁻¹' {x : 𝓧 | p x})
Tactic: rw [← hX.map_eq, map_measureReal_apply_of_aemeasurable hX.aemeasurable hp]
-- Lean 4 proof step from Mathlib.Probability.HasLaw (goal)
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
Ω' : Type u_3
𝓨 : Type u_4
m' : MeasurableSpace Ω'
m𝓨 : MeasurableSpace 𝓨
P' : Measure Ω'
ν : Measure 𝓨
f : 𝓧 → 𝓨
Y : Ω' → 𝓧
hf : AEMeasurable f μ
hX : HasLaw X μ P
hY : HasLaw Y μ P'
h : HasLaw (fun (ω : Ω) ↦ f (X ω)) ν P
⊢ map (fun (ω : Ω') ↦ f (Y ω)) P' = ν
have rw : map (f ∘ Y) P' = ν
Tactic: rw [← Function.comp_def,
      ← AEMeasurable.map_map_of_aemeasurable (hY.map_eq ▸ hf) hY.aemeasurable,
      hY.map_eq, ← hX.map_eq, AEMeasurable.map_map_of_aemeasurable (hX.map_eq ▸ hf) hX.aemeasurable,
      Function.comp_def, h.map_eq]
-- Lean 4 proof step from Mathlib.Probability.HasLaw (goal)
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
Ω' : Type u_3
𝓨 : Type u_4
m' : MeasurableSpace Ω'
m𝓨 : MeasurableSpace 𝓨
P' : Measure Ω'
ν : Measure 𝓨
f : 𝓧 → 𝓨
Y : Ω' → 𝓧
hf : AEMeasurable f μ
hX : HasLaw X μ P
hY : HasLaw Y μ P'
h : HasLaw (fun (ω : Ω) ↦ f (X ω)) ν P
rw : map (f ∘ Y) P' = ν
⊢ map (fun (ω : Ω') ↦ f (Y ω)) P' = ν
have rw₁ : map f (map Y P') = ν
Tactic: rw [← Function.comp_def,
      ← AEMeasurable.map_map_of_aemeasurable (hY.map_eq ▸ hf) hY.aemeasurable,
      hY.map_eq, ← hX.map_eq, AEMeasurable.map_map_of_aemeasurable (hX.map_eq ▸ hf) hX.aemeasurable,
      Function.comp_def, h.map_eq]
-- Lean 4 proof step from Mathlib.Probability.HasLaw (goal)
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
Ω' : Type u_3
𝓨 : Type u_4
m' : MeasurableSpace Ω'
m𝓨 : MeasurableSpace 𝓨
P' : Measure Ω'
ν : Measure 𝓨
f : 𝓧 → 𝓨
Y : Ω' → 𝓧
hf : AEMeasurable f μ
hX : HasLaw X μ P
hY : HasLaw Y μ P'
h : HasLaw (fun (ω : Ω) ↦ f (X ω)) ν P
rw : map (f ∘ Y) P' = ν
rw₁ : map f (map Y P') = ν
⊢ map (fun (ω : Ω') ↦ f (Y ω)) P' = ν
have rw₂ : map f μ = ν
Tactic: rw [← Function.comp_def,
      ← AEMeasurable.map_map_of_aemeasurable (hY.map_eq ▸ hf) hY.aemeasurable,
      hY.map_eq, ← hX.map_eq, AEMeasurable.map_map_of_aemeasurable (hX.map_eq ▸ hf) hX.aemeasurable,
      Function.comp_def, h.map_eq]
-- Lean 4 proof step from Mathlib.Probability.HasLaw (goal)
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
Ω' : Type u_3
𝓨 : Type u_4
m' : MeasurableSpace Ω'
m𝓨 : MeasurableSpace 𝓨
P' : Measure Ω'
ν : Measure 𝓨
f : 𝓧 → 𝓨
Y : Ω' → 𝓧
hf : AEMeasurable f μ
hX : HasLaw X μ P
hY : HasLaw Y μ P'
h : HasLaw (fun (ω : Ω) ↦ f (X ω)) ν P
rw : map (f ∘ Y) P' = ν
rw₁ : map f (map Y P') = ν
rw₂ : map f μ = ν
⊢ map (fun (ω : Ω') ↦ f (Y ω)) P' = ν
have rw₃ : map f (map X P) = ν
Tactic: rw [← Function.comp_def,
      ← AEMeasurable.map_map_of_aemeasurable (hY.map_eq ▸ hf) hY.aemeasurable,
      hY.map_eq, ← hX.map_eq, AEMeasurable.map_map_of_aemeasurable (hX.map_eq ▸ hf) hX.aemeasurable,
      Function.comp_def, h.map_eq]
-- Lean 4 proof step from Mathlib.Probability.HasLaw (goal)
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
Ω' : Type u_3
𝓨 : Type u_4
m' : MeasurableSpace Ω'
m𝓨 : MeasurableSpace 𝓨
P' : Measure Ω'
ν : Measure 𝓨
f : 𝓧 → 𝓨
Y : Ω' → 𝓧
hf : AEMeasurable f μ
hX : HasLaw X μ P
hY : HasLaw Y μ P'
h : HasLaw (fun (ω : Ω) ↦ f (X ω)) ν P
rw : map (f ∘ Y) P' = ν
rw₁ : map f (map Y P') = ν
rw₂ : map f μ = ν
rw₃ : map f (map X P) = ν
⊢ map (fun (ω : Ω') ↦ f (Y ω)) P' = ν
have rw₄ : map (f ∘ X) P = ν
Tactic: rw [← Function.comp_def,
      ← AEMeasurable.map_map_of_aemeasurable (hY.map_eq ▸ hf) hY.aemeasurable,
      hY.map_eq, ← hX.map_eq, AEMeasurable.map_map_of_aemeasurable (hX.map_eq ▸ hf) hX.aemeasurable,
      Function.comp_def, h.map_eq]
-- Lean 4 proof step from Mathlib.Probability.HasLaw (goal)
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
Ω' : Type u_3
𝓨 : Type u_4
m' : MeasurableSpace Ω'
m𝓨 : MeasurableSpace 𝓨
P' : Measure Ω'
ν : Measure 𝓨
f : 𝓧 → 𝓨
Y : Ω' → 𝓧
hf : AEMeasurable f μ
hX : HasLaw X μ P
hY : HasLaw Y μ P'
h : HasLaw (fun (ω : Ω) ↦ f (X ω)) ν P
rw : map (f ∘ Y) P' = ν
rw₁ : map f (map Y P') = ν
rw₂ : map f μ = ν
rw₃ : map f (map X P) = ν
rw₄ : map (f ∘ X) P = ν
⊢ map (fun (ω : Ω') ↦ f (Y ω)) P' = ν
have rw₅ : map (fun (x : Ω) ↦ f (X x)) P = ν
Tactic: rw [← Function.comp_def,
      ← AEMeasurable.map_map_of_aemeasurable (hY.map_eq ▸ hf) hY.aemeasurable,
      hY.map_eq, ← hX.map_eq, AEMeasurable.map_map_of_aemeasurable (hX.map_eq ▸ hf) hX.aemeasurable,
      Function.comp_def, h.map_eq]
-- Lean 4 proof step from Mathlib.Probability.HasLaw (goal)
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
Ω' : Type u_3
𝓨 : Type u_4
m' : MeasurableSpace Ω'
m𝓨 : MeasurableSpace 𝓨
P' : Measure Ω'
ν : Measure 𝓨
f : 𝓧 → 𝓨
Y : Ω' → 𝓧
hf : AEMeasurable f μ
hX : HasLaw X μ P
hY : HasLaw Y μ P'
h : HasLaw (fun (ω : Ω) ↦ f (X ω)) ν P
rw : map (f ∘ Y) P' = ν
rw₁ : map f (map Y P') = ν
rw₂ : map f μ = ν
rw₃ : map f (map X P) = ν
rw₄ : map (f ∘ X) P = ν
rw₅ : map (fun (x : Ω) ↦ f (X x)) P = ν
⊢ map (fun (ω : Ω') ↦ f (Y ω)) P' = ν
have rw₆ : ν = ν
Tactic: rw [← Function.comp_def,
      ← AEMeasurable.map_map_of_aemeasurable (hY.map_eq ▸ hf) hY.aemeasurable,
      hY.map_eq, ← hX.map_eq, AEMeasurable.map_map_of_aemeasurable (hX.map_eq ▸ hf) hX.aemeasurable,
      Function.comp_def, h.map_eq]
-- Lean 4 proof step from Mathlib.Probability.HasLaw (goal)
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X Y : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
hX : HasLaw X μ P
hY : Y =ᶠ[ae P] X
⊢ map Y P = μ
have rw : map X P = μ
Tactic: rw [map_congr hY, hX.map_eq]
-- Lean 4 proof step from Mathlib.Probability.HasLaw (goal)
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X Y : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
hX : HasLaw X μ P
hY : Y =ᶠ[ae P] X
rw : map X P = μ
⊢ map Y P = μ
have rw₁ : μ = μ
Tactic: rw [map_congr hY, hX.map_eq]
-- Lean 4 proof step from Mathlib.Probability.HasLaw (goal)
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
hX : HasLaw X μ P
p : 𝓧 → Prop
hp : Measurable p
⊢ (∀ᵐ (ω : Ω) ∂P, p (X ω)) ↔ ∀ᵐ (x : 𝓧) ∂μ, p x
have rw : (∀ᵐ (ω : Ω) ∂P, p (X ω)) ↔ ∀ᵐ (x : 𝓧) ∂map X P, p x
Tactic: rw [← hX.map_eq, ae_map_iff hX.aemeasurable (measurableSet_setOf.2 hp)]
-- Lean 4 proof step from Mathlib.Probability.HasLaw (goal)
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
hX : HasLaw X μ P
p : 𝓧 → Prop
hp : Measurable p
rw : (∀ᵐ (ω : Ω) ∂P, p (X ω)) ↔ ∀ᵐ (x : 𝓧) ∂map X P, p x
⊢ (∀ᵐ (ω : Ω) ∂P, p (X ω)) ↔ ∀ᵐ (x : 𝓧) ∂μ, p x
have rw₁ : (∀ᵐ (ω : Ω) ∂P, p (X ω)) ↔ ∀ᵐ (x : Ω) ∂P, p (X x)
Tactic: rw [← hX.map_eq, ae_map_iff hX.aemeasurable (measurableSet_setOf.2 hp)]
-- Lean 4 proof step from Mathlib.Probability.HasLaw (goal)
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
hX : HasLaw X μ P
⊢ IsFiniteMeasure P ↔ IsFiniteMeasure μ
have rw : IsFiniteMeasure P ↔ IsFiniteMeasure (m0 := m𝓧) (map X P)
Tactic: rw [← hX.map_eq, isFiniteMeasure_map_iff hX.aemeasurable]
-- Lean 4 proof step from Mathlib.Probability.HasLaw (goal)
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
hX : HasLaw X μ P
rw : IsFiniteMeasure P ↔ IsFiniteMeasure (m0 := m𝓧) (map X P)
⊢ IsFiniteMeasure P ↔ IsFiniteMeasure μ
have rw₁ : IsFiniteMeasure P ↔ IsFiniteMeasure P
Tactic: rw [← hX.map_eq, isFiniteMeasure_map_iff hX.aemeasurable]
-- Lean 4 proof step from Mathlib.Probability.HasLaw (goal)
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
hX : HasLaw X μ P
⊢ IsProbabilityMeasure P ↔ IsProbabilityMeasure μ
have rw : IsProbabilityMeasure P ↔ IsProbabilityMeasure (m0 := m𝓧) (map X P)
Tactic: rw [← hX.map_eq, isProbabilityMeasure_map_iff hX.aemeasurable]
-- Lean 4 proof step from Mathlib.Probability.HasLaw (goal)
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
hX : HasLaw X μ P
rw : IsProbabilityMeasure P ↔ IsProbabilityMeasure (m0 := m𝓧) (map X P)
⊢ IsProbabilityMeasure P ↔ IsProbabilityMeasure μ
have rw₁ : IsProbabilityMeasure P ↔ IsProbabilityMeasure P
Tactic: rw [← hX.map_eq, isProbabilityMeasure_map_iff hX.aemeasurable]
-- Lean 4 proof step from Mathlib.Probability.HasLaw (goal)
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
𝓨 : Type u_3
m𝓨 : MeasurableSpace 𝓨
ν : Measure 𝓨
Y : 𝓧 → 𝓨
hY : HasLaw Y ν μ
hX : HasLaw X μ P
⊢ map (Y ∘ X) P = ν
have rw : AEMeasurable (_m := m𝓧) Y (map X P)
Tactic: rw [← AEMeasurable.map_map_of_aemeasurable _ hX.aemeasurable, hX.map_eq, hY.map_eq]
-- Lean 4 proof step from Mathlib.Probability.HasLaw (goal)
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
𝓨 : Type u_3
m𝓨 : MeasurableSpace 𝓨
ν : Measure 𝓨
Y : 𝓧 → 𝓨
hY : HasLaw Y ν μ
hX : HasLaw X μ P
⊢ AEMeasurable (_m := m𝓧) Y (map X P)
have rw : AEMeasurable Y μ
Tactic: rw [hX.map_eq]
-- Lean 4 proof step from Mathlib.Probability.HasLaw (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
M : Type u_3
inst : Monoid M
mM : MeasurableSpace M
inst_1 : MeasurableMul₂ M
μ ν : Measure M
inst_2 : SigmaFinite μ
inst_3 : SigmaFinite ν
X Y : Ω → M
hX : HasLaw X μ P
hY : HasLaw Y ν P
hXY : X ⟂ᵢ[P] Y
⊢ map (X * Y) P = μ ∗ₘ ν
have σf : SigmaFinite (m0 := mM) (map X P)
Tactic: rw [hXY.map_mul_eq_map_mconv_map₀' hX.aemeasurable hY.aemeasurable, hX.map_eq, hY.map_eq]
-- Lean 4 proof step from Mathlib.Probability.HasLaw (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
M : Type u_3
inst : Monoid M
mM : MeasurableSpace M
inst_1 : MeasurableMul₂ M
μ ν : Measure M
inst_2 : SigmaFinite μ
inst_3 : SigmaFinite ν
X Y : Ω → M
hX : HasLaw X μ P
hY : HasLaw Y ν P
hXY : X ⟂ᵢ[P] Y
σf : SigmaFinite (m0 := mM) (map X P)
⊢ map (X * Y) P = μ ∗ₘ ν
have σg : SigmaFinite (m0 := mM) (map Y P)
Tactic: rw [hXY.map_mul_eq_map_mconv_map₀' hX.aemeasurable hY.aemeasurable, hX.map_eq, hY.map_eq]
-- Lean 4 proof step from Mathlib.Probability.HasLaw (goal)
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
P : Measure Ω
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
X : Ω → 𝓧
hX : HasLaw X μ P
f : 𝓧 → E
hf : AEStronglyMeasurable f μ
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : Ω), (f ∘ X) x ∂P) (∫ (x : 𝓧), f x ∂μ)
have rw : AEStronglyMeasurable (m₀ := m𝓧) f (map X P)
Tactic: rw [← hX.map_eq, integral_map hX.aemeasurable, Function.comp_def]
-- Lean 4 proof step from Mathlib.Probability.HasLaw (goal)
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
P : Measure Ω
X : Ω → 𝓧
hX : HasLaw X μ P
f : 𝓧 → ℝ≥0∞
hf : AEMeasurable f μ
⊢ ∫⁻ (ω : Ω), f (X ω) ∂P = ∫⁻ (x : 𝓧), f x ∂μ
have rw : AEMeasurable (_m := m𝓧) f (map X P)
Tactic: rw [← hX.map_eq, lintegral_map' _ hX.aemeasurable]
-- Lean 4 proof step from Mathlib.Probability.HasLaw (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SecondCountableTopology E
mE : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
μ : Measure E
X : Ω → E
hX : HasLaw X μ P
⊢ Eq (α := E) (∫ (x : Ω), X x ∂P) (∫ (x : E), x ∂μ)
have rw : Eq (α := E) (∫ (x : E), id x ∂μ) (∫ (x : E), x ∂μ)
Tactic: rw [← Function.id_comp X, hX.integral_comp aestronglyMeasurable_id]
-- Lean 4 proof step from Mathlib.Probability.HasLaw (goal)
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
hX : HasLaw X μ P
f g : 𝓧 → ℝ
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ cov[f ∘ X, g ∘ X; P] = cov[f, g; μ]
have hX₁ : AEStronglyMeasurable (m₀ := m𝓧) f (map X P)
Tactic: rw [← hX.map_eq, covariance_map]
-- Lean 4 proof step from Mathlib.Probability.HasLaw (goal)
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
hX : HasLaw X μ P
f g : 𝓧 → ℝ
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hX₁ : AEStronglyMeasurable (m₀ := m𝓧) f (map X P)
⊢ cov[f ∘ X, g ∘ X; P] = cov[f, g; μ]
have hY : AEStronglyMeasurable (m₀ := m𝓧) g (map X P)
Tactic: rw [← hX.map_eq, covariance_map]