awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.HasLaw
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)
σg : SigmaFinite (m0 := mM) (map Y P)
⊢ map (X * Y) P = μ ∗ₘ ν

Tactic:
rw [hXY.map_mul_eq_map_mconv_map₀' hX.aemeasurable hY.aemeasurable, hX.map_eq, hY.map_eq]

Premises used: ProbabilityTheory.HasLaw.aemeasurable, ProbabilityTheory.HasLaw.map_eq, ProbabilityTheory.IndepFun.map_mul_eq_map_mconv_map₀'
-- Module: Mathlib.Probability.HasLaw
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 σf₁ σf₂ σf₃ : SigmaFinite μ
⊢ SigmaFinite (m0 := mM) (map X P)

Tactic:
rwa [hX.map_eq]

Premises used: ProbabilityTheory.HasLaw.map_eq
-- Module: Mathlib.Probability.HasLaw
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
σg σg₁ σg₂ σg₃ : SigmaFinite ν
⊢ SigmaFinite (m0 := mM) (map Y P)

Tactic:
rwa [hY.map_eq]

Premises used: ProbabilityTheory.HasLaw.map_eq
-- Module: Mathlib.Probability.HasLaw
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
⊢ HasLaw (fun (ω : Ω) ↦ X ω * Y ω) (μ ∗ₘ ν) P

Tactic:
hXY.hasLaw_mul hX hY

Premises used: ProbabilityTheory.IndepFun.hasLaw_mul
-- Module: Mathlib.Probability.HasLaw
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 μ
rw : AEStronglyMeasurable (m₀ := m𝓧) f (map X P)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : Ω), (f ∘ X) x ∂P) (∫ (x : 𝓧), f x ∂μ)

Tactic:
rw [← hX.map_eq, integral_map hX.aemeasurable, Function.comp_def]

Premises used: MeasureTheory.integral_map, ProbabilityTheory.HasLaw.aemeasurable, ProbabilityTheory.HasLaw.map_eq, Function.comp_def
-- Module: Mathlib.Probability.HasLaw
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 rwa rwa₁ rwa₂ rwa₃ : AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable (m₀ := m𝓧) f (map X P)

Tactic:
rwa [hX.map_eq]

Premises used: ProbabilityTheory.HasLaw.map_eq
-- Module: Mathlib.Probability.HasLaw
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
P : Measure Ω
X : Ω → 𝓧
hX : HasLaw X μ P
f : 𝓧 → ℝ≥0∞
hf : AEMeasurable f μ
rw : AEMeasurable (_m := m𝓧) f (map X P)
⊢ ∫⁻ (ω : Ω), f (X ω) ∂P = ∫⁻ (x : 𝓧), f x ∂μ

Tactic:
rw [← hX.map_eq, lintegral_map' _ hX.aemeasurable]

Premises used: ProbabilityTheory.HasLaw.aemeasurable, ProbabilityTheory.HasLaw.map_eq, MeasureTheory.lintegral_map'
-- Module: Mathlib.Probability.HasLaw
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
P : Measure Ω
X : Ω → 𝓧
hX : HasLaw X μ P
f : 𝓧 → ℝ≥0∞
hf rwa rwa₁ rwa₂ rwa₃ : AEMeasurable f μ
⊢ AEMeasurable (_m := m𝓧) f (map X P)

Tactic:
rwa [hX.map_eq]

Premises used: ProbabilityTheory.HasLaw.map_eq
-- Module: Mathlib.Probability.HasLaw
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
rw : Eq (α := E) (∫ (x : E), id x ∂μ) (∫ (x : E), x ∂μ)
⊢ Eq (α := E) (∫ (x : Ω), X x ∂P) (∫ (x : E), x ∂μ)

Tactic:
rw [← Function.id_comp X, hX.integral_comp aestronglyMeasurable_id]

Premises used: ProbabilityTheory.HasLaw.integral_comp, aestronglyMeasurable_id, Function.id_comp
-- Module: Mathlib.Probability.HasLaw
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 : E), id x ∂μ) (∫ (x : E), x ∂μ)

Tactic:
simp
-- Module: Mathlib.Probability.HasLaw
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)
hY : AEStronglyMeasurable (m₀ := m𝓧) g (map X P)
hZ : AEMeasurable X P
⊢ cov[f ∘ X, g ∘ X; P] = cov[f, g; μ]

Tactic:
rw [← hX.map_eq, covariance_map]

Premises used: ProbabilityTheory.HasLaw.map_eq, ProbabilityTheory.covariance_map
-- Module: Mathlib.Probability.HasLaw
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 f μ
⊢ AEStronglyMeasurable (m₀ := m𝓧) f (map X P)

Tactic:
rw [hX.map_eq]

Premises used: ProbabilityTheory.HasLaw.map_eq
-- Module: Mathlib.Probability.HasLaw
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 μ
⊢ AEStronglyMeasurable f μ

Tactic:
hf.aestronglyMeasurable

Premises used: AEMeasurable.aestronglyMeasurable
-- Module: Mathlib.Probability.HasLaw
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 μ
⊢ AEStronglyMeasurable f μ

Tactic:
exact hf.aestronglyMeasurable

Premises used: AEMeasurable.aestronglyMeasurable
-- Module: Mathlib.Probability.HasLaw
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 μ
hY : AEStronglyMeasurable g μ
⊢ AEStronglyMeasurable (m₀ := m𝓧) g (map X P)

Tactic:
rw [hX.map_eq]

Premises used: ProbabilityTheory.HasLaw.map_eq
-- Module: Mathlib.Probability.HasLaw
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 μ
⊢ AEStronglyMeasurable g μ

Tactic:
hg.aestronglyMeasurable

Premises used: AEMeasurable.aestronglyMeasurable
-- Module: Mathlib.Probability.HasLaw
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 μ
⊢ AEStronglyMeasurable g μ

Tactic:
exact hg.aestronglyMeasurable

Premises used: AEMeasurable.aestronglyMeasurable
-- Module: Mathlib.Probability.HasLaw
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 μ
⊢ AEMeasurable X P

Tactic:
hX.aemeasurable

Premises used: ProbabilityTheory.HasLaw.aemeasurable
-- Module: Mathlib.Probability.HasLaw
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 μ
⊢ AEMeasurable X P

Tactic:
exact hX.aemeasurable

Premises used: ProbabilityTheory.HasLaw.aemeasurable
-- Module: Mathlib.Probability.HasLaw
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[fun (ω : Ω) ↦ f (X ω), fun (ω : Ω) ↦ g (X ω); P] = cov[f, g; μ]

Tactic:
hX.covariance_comp hf hg

Premises used: ProbabilityTheory.HasLaw.covariance_comp
-- Module: Mathlib.Probability.HasLaw
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
μ : Measure ℝ
X : Ω → ℝ
hX : HasLaw X μ P
rw : Var[X; P] = variance (mΩ := Real.measurableSpace) id (map X P)
rw₁ : Var[X; P] = Var[id ∘ X; P]
rw₂ rw₃ : Var[X; P] = Var[X; P]
⊢ Var[X; P] = Var[id; μ]

Tactic:
rw [← hX.map_eq, variance_map aemeasurable_id hX.aemeasurable, Function.id_comp]

Premises used: ProbabilityTheory.HasLaw.aemeasurable, ProbabilityTheory.HasLaw.map_eq, ProbabilityTheory.variance_map, aemeasurable_id, Function.id_comp
-- Module: Mathlib.Probability.HasLaw
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
inst : IsFiniteMeasure P
𝓨 : Type u_3
m𝓨 : MeasurableSpace 𝓨
ν : Measure 𝓨
Y : Ω → 𝓨
hX : HasLaw X μ P
hY : HasLaw Y ν P
h : X ⟂ᵢ[P] Y
⊢ AEMeasurable X P

Tactic:
fun_prop
-- Module: Mathlib.Probability.HasLaw
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
inst : IsFiniteMeasure P
𝓨 : Type u_3
m𝓨 : MeasurableSpace 𝓨
ν : Measure 𝓨
Y : Ω → 𝓨
hX : HasLaw X μ P
hY : HasLaw Y ν P
h : X ⟂ᵢ[P] Y
⊢ AEMeasurable Y P

Tactic:
fun_prop
-- Module: Mathlib.Probability.HasLaw
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
inst : IsFiniteMeasure P
𝓨 : Type u_3
m𝓨 : MeasurableSpace 𝓨
ν : Measure 𝓨
Y : Ω → 𝓨
hX : HasLaw X μ P
hY : HasLaw Y ν P
h : X ⟂ᵢ[P] Y
rw : Measure.prod (map X P) (map Y P) = μ.prod ν
rw₁ : μ.prod (map Y P) = μ.prod ν
rw₂ rw₃ : μ.prod ν = μ.prod ν
⊢ map (fun (ω : Ω) ↦ (X ω, Y ω)) P = μ.prod ν

Tactic:
rw [h.map_prod_eq_prod_map_map (by fun_prop) (by fun_prop), hX.map_eq,
          hY.map_eq]

Premises used: ProbabilityTheory.HasLaw.map_eq, ProbabilityTheory.IndepFun.map_prod_eq_prod_map_map
-- Module: Mathlib.Probability.HasLaw
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
inst : IsFiniteMeasure P
𝓨 : Type u_3
m𝓨 : MeasurableSpace 𝓨
ν : Measure 𝓨
Y : Ω → 𝓨
hX : HasLaw X μ P
hY : HasLaw Y ν P
h : HasLaw (fun (ω : Ω) ↦ (X ω, Y ω)) (μ.prod ν) P
⊢ AEMeasurable X P

Tactic:
fun_prop
-- Module: Mathlib.Probability.HasLaw
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
inst : IsFiniteMeasure P
𝓨 : Type u_3
m𝓨 : MeasurableSpace 𝓨
ν : Measure 𝓨
Y : Ω → 𝓨
hX : HasLaw X μ P
hY : HasLaw Y ν P
h : HasLaw (fun (ω : Ω) ↦ (X ω, Y ω)) (μ.prod ν) P
⊢ AEMeasurable Y P

Tactic:
fun_prop
-- Module: Mathlib.Probability.HasLaw
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
inst : IsFiniteMeasure P
𝓨 : Type u_3
m𝓨 : MeasurableSpace 𝓨
ν : Measure 𝓨
Y : Ω → 𝓨
hX : HasLaw X μ P
hY : HasLaw Y ν P
h : HasLaw (fun (ω : Ω) ↦ (X ω, Y ω)) (μ.prod ν) P
rw : Eq (α := Measure (𝓧 × 𝓨)) (map (fun (ω : Ω) ↦ (X ω, Y ω)) P) (Measure.prod (map X P) (map Y P))
rw₁ : μ.prod ν = Measure.prod (map X P) (map Y P)
rw₂ : μ.prod ν = μ.prod (map Y P)
rw₃ rw₄ : μ.prod ν = μ.prod ν
⊢ X ⟂ᵢ[P] Y

Tactic:
rw [indepFun_iff_map_prod_eq_prod_map_map (by fun_prop) (by fun_prop),
      h.map_eq, hX.map_eq, hY.map_eq]

Premises used: ProbabilityTheory.HasLaw.map_eq, ProbabilityTheory.indepFun_iff_map_prod_eq_prod_map_map
-- Module: Mathlib.Probability.HasLaw
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_3
inst : Fintype ι
𝓧 : ι → Type u_4
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
μ : (i : ι) → Measure (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
hX : ∀ (i : ι), HasLaw (X i) (μ i) P
h : iIndepFun (β := 𝓧) X P
⊢ ∀ (i : ι), AEMeasurable (X i) P

Tactic:
fun_prop
-- Module: Mathlib.Probability.HasLaw
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_3
inst : Fintype ι
𝓧 : ι → Type u_4
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
μ : (i : ι) → Measure (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
hX : ∀ (i : ι), HasLaw (X i) (μ i) P
h : iIndepFun (β := 𝓧) X P
rw : (Measure.pi (α := 𝓧) fun (i : ι) ↦ map (X i) P) = Measure.pi (α := 𝓧) μ
⊢ map (fun (ω : Ω) (i : ι) ↦ X i ω) P = Measure.pi (α := 𝓧) μ

Tactic:
rw [h.map_fun_eq_pi_map (by fun_prop)]

Premises used: ProbabilityTheory.iIndepFun.map_fun_eq_pi_map
-- Module: Mathlib.Probability.HasLaw
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_3
inst : Fintype ι
𝓧 : ι → Type u_4
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
μ : (i : ι) → Measure (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
hX : ∀ (i : ι), HasLaw (X i) (μ i) P
h : iIndepFun (β := 𝓧) X P
⊢ (Measure.pi (α := 𝓧) fun (i : ι) ↦ map (X i) P) = Measure.pi (α := 𝓧) μ

Tactic:
simp_rw [fun i ↦ (hX i).map_eq]

Premises used: ProbabilityTheory.HasLaw.map_eq
-- Module: Mathlib.Probability.HasLaw
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : IsProbabilityMeasure P
ι : Type u_3
inst_1 : Fintype ι
𝓧 : ι → Type u_4
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
μ : (i : ι) → Measure (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
hX : ∀ (i : ι), HasLaw (X i) (μ i) P
h : HasLaw (fun (ω : Ω) (i : ι) ↦ X i ω) (Measure.pi (α := 𝓧) μ) P
⊢ ∀ (i : ι), AEMeasurable (X i) P

Tactic:
fun_prop
-- Module: Mathlib.Probability.HasLaw
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : IsProbabilityMeasure P
ι : Type u_3
inst_1 : Fintype ι
𝓧 : ι → Type u_4
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
μ : (i : ι) → Measure (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
hX : ∀ (i : ι), HasLaw (X i) (μ i) P
h : HasLaw (fun (ω : Ω) (i : ι) ↦ X i ω) (Measure.pi (α := 𝓧) μ) P
rw : Measure.pi (α := 𝓧) μ = Measure.pi (α := 𝓧) fun (i : ι) ↦ map (X i) P
⊢ iIndepFun (β := 𝓧) X P

Tactic:
rw [iIndepFun_iff_map_fun_eq_pi_map (by fun_prop), h.map_eq]

Premises used: ProbabilityTheory.HasLaw.map_eq, ProbabilityTheory.iIndepFun_iff_map_fun_eq_pi_map
-- Module: Mathlib.Probability.HasLaw
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : IsProbabilityMeasure P
ι : Type u_3
inst_1 : Fintype ι
𝓧 : ι → Type u_4
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
μ : (i : ι) → Measure (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
hX : ∀ (i : ι), HasLaw (X i) (μ i) P
h : HasLaw (fun (ω : Ω) (i : ι) ↦ X i ω) (Measure.pi (α := 𝓧) μ) P
⊢ Measure.pi (α := 𝓧) μ = Measure.pi (α := 𝓧) fun (i : ι) ↦ map (X i) P

Tactic:
simp_rw [fun i ↦ (hX i).map_eq]

Premises used: ProbabilityTheory.HasLaw.map_eq
-- Module: Mathlib.Probability.HasLawExists
Goal:
𝓧 : Type u
m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
⊢ ∃ (Ω : Type u) (x : MeasurableSpace Ω) (P : Measure Ω) (X : Ω → 𝓧), Measurable X ∧ HasLaw X μ P

Tactic:
⟨𝓧, m𝓧, μ, id, measurable_id, .id⟩

Premises used: ProbabilityTheory.HasLaw.id, measurable_id, id, And.intro, Exists.intro
-- Module: Mathlib.Probability.HasLawExists
Goal:
ι : Type v
𝓧 : ι → Type u
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
μ : (i : ι) → Measure (𝓧 i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
h :
  (∀ (i : ι),
      Measurable (α := (i : ι) → 𝓧 i) (β := 𝓧 i)
        ((fun (i : ι) ↦ (Function.eval (β := 𝓧) i : (f : (x : ι) → 𝓧 x) → 𝓧 i)) i)) ∧
    (∀ (i : ι),
        HasLaw ((fun (i : ι) ↦ (Function.eval (β := 𝓧) i : (f : (x : ι) → 𝓧 x) → 𝓧 i)) i) (μ i)
          (infinitePi (X := 𝓧) μ)) ∧
      iIndepFun (β := 𝓧) (fun (i : ι) ↦ Function.eval (β := 𝓧) i) (infinitePi (X := 𝓧) μ) ∧
        IsProbabilityMeasure (infinitePi (X := 𝓧) μ)
⊢ ∃ (Ω : Type (max u v)) (x : MeasurableSpace Ω) (P : Measure Ω) (X : (i : ι) → Ω → 𝓧 i),
    (∀ (i : ι), Measurable (X i)) ∧ (∀ (i : ι), HasLaw (X i) (μ i) P) ∧ iIndepFun (β := 𝓧) X P ∧ IsProbabilityMeasure P

Tactic:
use Π i, (𝓧 i), .pi, infinitePi μ, fun i ↦ Function.eval i

Premises used: Function.eval, MeasureTheory.Measure.infinitePi
-- Module: Mathlib.Probability.HasLawExists
Goal:
ι : Type v
𝓧 : ι → Type u
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
μ : (i : ι) → Measure (𝓧 i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
⊢ ∀ (i : ι),
    Measurable (α := (i : ι) → 𝓧 i) (β := 𝓧 i)
      ((fun (i : ι) ↦ (Function.eval (β := 𝓧) i : (f : (x : ι) → 𝓧 x) → 𝓧 i)) i)

Tactic:
fun_prop
-- Module: Mathlib.Probability.HasLawExists
Goal:
ι : Type v
𝓧 : ι → Type u
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
μ : (i : ι) → Measure (𝓧 i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
⊢ IsProbabilityMeasure (infinitePi (X := 𝓧) μ)

Tactic:
infer_instance
-- Module: Mathlib.Probability.HasLawExists
Goal:
ι : Type v
𝓧 : ι → Type u
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
μ : (i : ι) → Measure (𝓧 i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
h : iIndepFun (β := 𝓧) (fun (i : ι) ↦ Function.eval (β := 𝓧) i) (infinitePi (X := 𝓧) μ)
⊢ (∀ (i : ι),
      Measurable (α := (i : ι) → 𝓧 i) (β := 𝓧 i)
        ((fun (i : ι) ↦ (Function.eval (β := 𝓧) i : (f : (x : ι) → 𝓧 x) → 𝓧 i)) i)) ∧
    (∀ (i : ι),
        HasLaw ((fun (i : ι) ↦ (Function.eval (β := 𝓧) i : (f : (x : ι) → 𝓧 x) → 𝓧 i)) i) (μ i)
          (infinitePi (X := 𝓧) μ)) ∧
      iIndepFun (β := 𝓧) (fun (i : ι) ↦ Function.eval (β := 𝓧) i) (infinitePi (X := 𝓧) μ) ∧
        IsProbabilityMeasure (infinitePi (X := 𝓧) μ)

Tactic:
refine ⟨by fun_prop, fun i ↦ MeasurePreserving.hasLaw (measurePreserving_eval_infinitePi _ _),
    ?_, by infer_instance⟩
-- Module: Mathlib.Probability.HasLawExists
Goal:
ι : Type v
𝓧 : ι → Type u
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
μ : (i : ι) → Measure (𝓧 i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
⊢ ∀ (i : ι), Measurable (α := (i : ι) → 𝓧 i) (Function.eval (β := 𝓧) i)

Tactic:
fun_prop
-- Module: Mathlib.Probability.HasLawExists
Goal:
ι : Type v
𝓧 : ι → Type u
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
μ : (i : ι) → Measure (𝓧 i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
h : infinitePi (X := 𝓧) μ = infinitePi (X := 𝓧) fun (i : ι) ↦ map (Function.eval (β := 𝓧) i) (infinitePi (X := 𝓧) μ)
⊢ iIndepFun (β := 𝓧) (fun (i : ι) ↦ Function.eval (β := 𝓧) i) (infinitePi (X := 𝓧) μ)

Tactic:
rw [iIndepFun_iff_map_fun_eq_infinitePi_map (by fun_prop), map_id']

Premises used: MeasureTheory.Measure.map_id', ProbabilityTheory.iIndepFun_iff_map_fun_eq_infinitePi_map
-- Module: Mathlib.Probability.HasLawExists
Goal:
ι : Type v
𝓧 : ι → Type u
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
μ : (i : ι) → Measure (𝓧 i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
h : μ = fun (i : ι) ↦ map (Function.eval (β := 𝓧) i) (infinitePi (X := 𝓧) μ)
⊢ infinitePi (X := 𝓧) μ = infinitePi (X := 𝓧) fun (i : ι) ↦ map (Function.eval (β := 𝓧) i) (infinitePi (X := 𝓧) μ)

Tactic:
congr
-- Module: Mathlib.Probability.HasLawExists
Goal:
ι : Type v
𝓧 : ι → Type u
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
μ : (i : ι) → Measure (𝓧 i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
h : ∀ (i : ι), μ i = map (Function.eval (β := 𝓧) i) (infinitePi (X := 𝓧) μ)
⊢ μ = fun (i : ι) ↦ map (Function.eval (β := 𝓧) i) (infinitePi (X := 𝓧) μ)

Tactic:
funext i
-- Module: Mathlib.Probability.HasLawExists
Goal:
ι : Type v
𝓧 : ι → Type u
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
μ : (i : ι) → Measure (𝓧 i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
i : ι
⊢ μ i = map (Function.eval (β := 𝓧) i) (infinitePi (X := 𝓧) μ)

Tactic:
((measurePreserving_eval_infinitePi μ i).map_eq).symm

Premises used: MeasureTheory.MeasurePreserving.map_eq, measurePreserving_eval_infinitePi, Eq.symm
-- Module: Mathlib.Probability.HasLawExists
Goal:
ι : Type v
𝓧 : ι → Type u
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
μ : (i : ι) → Measure (𝓧 i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
i : ι
⊢ μ i = map (Function.eval (β := 𝓧) i) (infinitePi (X := 𝓧) μ)

Tactic:
exact ((measurePreserving_eval_infinitePi μ i).map_eq).symm

Premises used: MeasureTheory.MeasurePreserving.map_eq, measurePreserving_eval_infinitePi, Eq.symm
-- Module: Mathlib.Probability.HasLawExists
Goal:
ι : Type v
𝓧 : Type u
m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
inst : IsProbabilityMeasure μ
⊢ ∃ (Ω : Type (max u v)) (x : MeasurableSpace Ω) (P : Measure Ω) (X : ι → Ω → 𝓧),
    (∀ (i : ι), Measurable (X i)) ∧
      (∀ (i : ι), HasLaw (X i) μ P) ∧ iIndepFun (β := fun (x : ι) ↦ 𝓧) X P ∧ IsProbabilityMeasure P

Tactic:
exists_hasLaw_indepFun (fun _ ↦ 𝓧) (fun _ ↦ μ)

Premises used: ProbabilityTheory.exists_hasLaw_indepFun
-- Module: Mathlib.Probability.IdentDistrib
Goal:
α : Type u_1
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace γ
μ : Measure α
f : α → γ
hf : AEMeasurable f μ
⊢ IdentDistrib f f μ μ

Tactic:
{ aemeasurable_fst := hf
    aemeasurable_snd := hf
    map_eq := rfl }

Premises used: rfl, ProbabilityTheory.IdentDistrib.mk
-- Module: Mathlib.Probability.IdentDistrib
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
h : IdentDistrib f g μ ν
⊢ IdentDistrib g f ν μ

Tactic:
{ aemeasurable_fst := h.aemeasurable_snd
    aemeasurable_snd := h.aemeasurable_fst
    map_eq := h.map_eq.symm }

Premises used: ProbabilityTheory.IdentDistrib.aemeasurable_fst, ProbabilityTheory.IdentDistrib.aemeasurable_snd, ProbabilityTheory.IdentDistrib.map_eq, Eq.symm, ProbabilityTheory.IdentDistrib.mk
-- Module: Mathlib.Probability.IdentDistrib
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
inst_3 : MeasurableSpace δ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
ρ : Measure δ
h : δ → γ
h₁ : IdentDistrib f g μ ν
h₂ : IdentDistrib g h ν ρ
⊢ IdentDistrib f h μ ρ

Tactic:
{ aemeasurable_fst := h₁.aemeasurable_fst
    aemeasurable_snd := h₂.aemeasurable_snd
    map_eq := h₁.map_eq.trans h₂.map_eq }

Premises used: ProbabilityTheory.IdentDistrib.aemeasurable_fst, ProbabilityTheory.IdentDistrib.aemeasurable_snd, ProbabilityTheory.IdentDistrib.map_eq, Eq.trans, ProbabilityTheory.IdentDistrib.mk
-- Module: Mathlib.Probability.IdentDistrib
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
inst_3 : MeasurableSpace δ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
u : γ → δ
h : IdentDistrib f g μ ν
hu : AEMeasurable (_m := inst_2) u (Measure.map f μ)
⊢ AEMeasurable (_m := inst_2) u (Measure.map g ν)

Tactic:
rw [h.map_eq] at hu

Premises used: ProbabilityTheory.IdentDistrib.map_eq
-- Module: Mathlib.Probability.IdentDistrib
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
inst_3 : MeasurableSpace δ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
u : γ → δ
h : IdentDistrib f g μ ν
hu : AEMeasurable (_m := inst_2) u (Measure.map g ν)
⊢ AEMeasurable (u ∘ g) ν

Tactic:
hu.comp_aemeasurable h.aemeasurable_snd

Premises used: ProbabilityTheory.IdentDistrib.aemeasurable_snd, AEMeasurable.comp_aemeasurable
-- Module: Mathlib.Probability.IdentDistrib
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
inst_3 : MeasurableSpace δ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
u : γ → δ
h : IdentDistrib f g μ ν
hu : AEMeasurable (_m := inst_2) u (Measure.map g ν)
⊢ AEMeasurable (u ∘ g) ν

Tactic:
exact hu.comp_aemeasurable h.aemeasurable_snd

Premises used: ProbabilityTheory.IdentDistrib.aemeasurable_snd, AEMeasurable.comp_aemeasurable
-- Module: Mathlib.Probability.IdentDistrib
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
inst_3 : MeasurableSpace δ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
u : γ → δ
h : IdentDistrib f g μ ν
hu : AEMeasurable (_m := inst_2) u (Measure.map f μ)
rw : AEMeasurable (_m := inst_2) u (Measure.map g ν)
⊢ Eq (α := Measure δ) (Measure.map (u ∘ f) μ) (Measure.map (u ∘ g) ν)

Tactic:
rw [← AEMeasurable.map_map_of_aemeasurable hu h.aemeasurable_fst, ←
        AEMeasurable.map_map_of_aemeasurable _ h.aemeasurable_snd, h.map_eq]

Premises used: ProbabilityTheory.IdentDistrib.aemeasurable_fst, AEMeasurable.map_map_of_aemeasurable, ProbabilityTheory.IdentDistrib.aemeasurable_snd, ProbabilityTheory.IdentDistrib.map_eq