awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 δ
inst_4 : IsFiniteMeasure μ
inst_5 : IsFiniteMeasure μ'
X : γ → α
X' : δ → α
Y : γ → β
Y' : δ → β
h_indep : X ⟂ᵢ[μ] Y
h_ident : IdentDistrib (γ := α × β) (fun (ω : γ) ↦ (X ω, Y ω)) (fun (ω : δ) ↦ (X' ω, Y' ω)) μ μ'
⊢ AEMeasurable X μ

Tactic:
measurable_fst.aemeasurable.comp_aemeasurable h_ident.aemeasurable_fst

Premises used: Measurable.aemeasurable, ProbabilityTheory.IdentDistrib.aemeasurable_fst, measurable_fst, 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 δ
inst_4 : IsFiniteMeasure μ
inst_5 : IsFiniteMeasure μ'
X : γ → α
X' : δ → α
Y : γ → β
Y' : δ → β
h_indep : X ⟂ᵢ[μ] Y
h_ident : IdentDistrib (γ := α × β) (fun (ω : γ) ↦ (X ω, Y ω)) (fun (ω : δ) ↦ (X' ω, Y' ω)) μ μ'
⊢ AEMeasurable X μ

Tactic:
exact measurable_fst.aemeasurable.comp_aemeasurable h_ident.aemeasurable_fst

Premises used: Measurable.aemeasurable, ProbabilityTheory.IdentDistrib.aemeasurable_fst, measurable_fst, 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 δ
inst_4 : IsFiniteMeasure μ
inst_5 : IsFiniteMeasure μ'
X : γ → α
X' : δ → α
Y : γ → β
Y' : δ → β
h_indep : X ⟂ᵢ[μ] Y
h_ident : IdentDistrib (γ := α × β) (fun (ω : γ) ↦ (X ω, Y ω)) (fun (ω : δ) ↦ (X' ω, Y' ω)) μ μ'
⊢ AEMeasurable Y μ

Tactic:
measurable_snd.aemeasurable.comp_aemeasurable h_ident.aemeasurable_fst

Premises used: Measurable.aemeasurable, ProbabilityTheory.IdentDistrib.aemeasurable_fst, measurable_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 δ
inst_4 : IsFiniteMeasure μ
inst_5 : IsFiniteMeasure μ'
X : γ → α
X' : δ → α
Y : γ → β
Y' : δ → β
h_indep : X ⟂ᵢ[μ] Y
h_ident : IdentDistrib (γ := α × β) (fun (ω : γ) ↦ (X ω, Y ω)) (fun (ω : δ) ↦ (X' ω, Y' ω)) μ μ'
⊢ AEMeasurable Y μ

Tactic:
exact measurable_snd.aemeasurable.comp_aemeasurable h_ident.aemeasurable_fst

Premises used: Measurable.aemeasurable, ProbabilityTheory.IdentDistrib.aemeasurable_fst, measurable_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 δ
inst_4 : IsFiniteMeasure μ
inst_5 : IsFiniteMeasure μ'
X : γ → α
X' : δ → α
Y : γ → β
Y' : δ → β
h_indep : X ⟂ᵢ[μ] Y
h_ident : IdentDistrib (γ := α × β) (fun (ω : γ) ↦ (X ω, Y ω)) (fun (ω : δ) ↦ (X' ω, Y' ω)) μ μ'
⊢ AEMeasurable X' μ'

Tactic:
measurable_fst.aemeasurable.comp_aemeasurable h_ident.aemeasurable_snd

Premises used: Measurable.aemeasurable, ProbabilityTheory.IdentDistrib.aemeasurable_snd, measurable_fst, 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 δ
inst_4 : IsFiniteMeasure μ
inst_5 : IsFiniteMeasure μ'
X : γ → α
X' : δ → α
Y : γ → β
Y' : δ → β
h_indep : X ⟂ᵢ[μ] Y
h_ident : IdentDistrib (γ := α × β) (fun (ω : γ) ↦ (X ω, Y ω)) (fun (ω : δ) ↦ (X' ω, Y' ω)) μ μ'
⊢ AEMeasurable X' μ'

Tactic:
exact measurable_fst.aemeasurable.comp_aemeasurable h_ident.aemeasurable_snd

Premises used: Measurable.aemeasurable, ProbabilityTheory.IdentDistrib.aemeasurable_snd, measurable_fst, 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 δ
inst_4 : IsFiniteMeasure μ
inst_5 : IsFiniteMeasure μ'
X : γ → α
X' : δ → α
Y : γ → β
Y' : δ → β
h_indep : X ⟂ᵢ[μ] Y
h_ident : IdentDistrib (γ := α × β) (fun (ω : γ) ↦ (X ω, Y ω)) (fun (ω : δ) ↦ (X' ω, Y' ω)) μ μ'
⊢ AEMeasurable Y' μ'

Tactic:
measurable_snd.aemeasurable.comp_aemeasurable h_ident.aemeasurable_snd

Premises used: Measurable.aemeasurable, measurable_snd, 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 δ
inst_4 : IsFiniteMeasure μ
inst_5 : IsFiniteMeasure μ'
X : γ → α
X' : δ → α
Y : γ → β
Y' : δ → β
h_indep : X ⟂ᵢ[μ] Y
h_ident : IdentDistrib (γ := α × β) (fun (ω : γ) ↦ (X ω, Y ω)) (fun (ω : δ) ↦ (X' ω, Y' ω)) μ μ'
⊢ AEMeasurable Y' μ'

Tactic:
exact measurable_snd.aemeasurable.comp_aemeasurable h_ident.aemeasurable_snd

Premises used: Measurable.aemeasurable, measurable_snd, ProbabilityTheory.IdentDistrib.aemeasurable_snd, AEMeasurable.comp_aemeasurable
-- Module: Mathlib.Probability.IdentDistribIndep
Goal:
Ω : Type u_1
Ω' : Type u_2
E : Type u_4
F : Type u_5
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
mE : MeasurableSpace E
mF : MeasurableSpace F
μ : Measure Ω
ν : Measure Ω'
inst : IsFiniteMeasure μ
X : Ω → E
Y : Ω → F
Z : Ω' → E
W : Ω' → F
hXZ : IdentDistrib X Z μ ν
hYW : IdentDistrib Y W μ ν
hXY : X ⟂ᵢ[μ] Y
hZW : Z ⟂ᵢ[ν] W
rw : IsFiniteMeasure (m0 := mE) (Measure.map X μ)
⊢ IsFiniteMeasure (m0 := mE) (Measure.map Z ν)

Tactic:
rw [← hXZ.map_eq]

Premises used: ProbabilityTheory.IdentDistrib.map_eq
-- Module: Mathlib.Probability.IdentDistribIndep
Goal:
Ω : Type u_1
Ω' : Type u_2
E : Type u_4
F : Type u_5
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
mE : MeasurableSpace E
mF : MeasurableSpace F
μ : Measure Ω
ν : Measure Ω'
inst : IsFiniteMeasure μ
X : Ω → E
Y : Ω → F
Z : Ω' → E
W : Ω' → F
hXZ : IdentDistrib X Z μ ν
hYW : IdentDistrib Y W μ ν
hXY : X ⟂ᵢ[μ] Y
hZW : Z ⟂ᵢ[ν] W
⊢ IsFiniteMeasure (m0 := mE) (Measure.map X μ)

Tactic:
infer_instance
-- Module: Mathlib.Probability.IdentDistribIndep
Goal:
Ω : Type u_1
Ω' : Type u_2
E : Type u_4
F : Type u_5
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
mE : MeasurableSpace E
mF : MeasurableSpace F
μ : Measure Ω
ν : Measure Ω'
inst : IsFiniteMeasure μ
X : Ω → E
Y : Ω → F
Z : Ω' → E
W : Ω' → F
hXZ : IdentDistrib X Z μ ν
hYW : IdentDistrib Y W μ ν
hXY : X ⟂ᵢ[μ] Y
hZW : Z ⟂ᵢ[ν] W
⊢ IsFiniteMeasure (m0 := mE) (Measure.map Z ν)

Tactic:
have : IsFiniteMeasure (ν.map Z) := by rw [← hXZ.map_eq]; infer_instance
-- Module: Mathlib.Probability.IdentDistribIndep
Goal:
Ω : Type u_1
Ω' : Type u_2
E : Type u_4
F : Type u_5
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
mE : MeasurableSpace E
mF : MeasurableSpace F
μ : Measure Ω
ν : Measure Ω'
inst : IsFiniteMeasure μ
X : Ω → E
Y : Ω → F
Z : Ω' → E
W : Ω' → F
hXZ : IdentDistrib X Z μ ν
hYW : IdentDistrib Y W μ ν
hXY : X ⟂ᵢ[μ] Y
hZW : Z ⟂ᵢ[ν] W
this : IsFiniteMeasure (m0 := mE) (Measure.map Z ν)
⊢ IsFiniteMeasure ν

Tactic:
Measure.isFiniteMeasure_of_map hXZ.aemeasurable_snd

Premises used: MeasureTheory.Measure.isFiniteMeasure_of_map, ProbabilityTheory.IdentDistrib.aemeasurable_snd
-- Module: Mathlib.Probability.IdentDistribIndep
Goal:
Ω : Type u_1
Ω' : Type u_2
E : Type u_4
F : Type u_5
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
mE : MeasurableSpace E
mF : MeasurableSpace F
μ : Measure Ω
ν : Measure Ω'
inst : IsFiniteMeasure μ
X : Ω → E
Y : Ω → F
Z : Ω' → E
W : Ω' → F
hXZ : IdentDistrib X Z μ ν
hYW : IdentDistrib Y W μ ν
hXY : X ⟂ᵢ[μ] Y
hZW : Z ⟂ᵢ[ν] W
this : IsFiniteMeasure (m0 := mE) (Measure.map Z ν)
⊢ IsFiniteMeasure ν

Tactic:
exact Measure.isFiniteMeasure_of_map hXZ.aemeasurable_snd

Premises used: MeasureTheory.Measure.isFiniteMeasure_of_map, ProbabilityTheory.IdentDistrib.aemeasurable_snd
-- Module: Mathlib.Probability.IdentDistribIndep
Goal:
Ω : Type u_1
Ω' : Type u_2
E : Type u_4
F : Type u_5
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
mE : MeasurableSpace E
mF : MeasurableSpace F
μ : Measure Ω
ν : Measure Ω'
inst : IsFiniteMeasure μ
X : Ω → E
Y : Ω → F
Z : Ω' → E
W : Ω' → F
hXZ : IdentDistrib X Z μ ν
hYW : IdentDistrib Y W μ ν
hXY : X ⟂ᵢ[μ] Y
hZW : Z ⟂ᵢ[ν] W
⊢ IsFiniteMeasure ν

Tactic:
have : IsFiniteMeasure ν := by
      have : IsFiniteMeasure (ν.map Z) := by rw [← hXZ.map_eq]; infer_instance
      exact Measure.isFiniteMeasure_of_map hXZ.aemeasurable_snd
-- Module: Mathlib.Probability.IdentDistribIndep
Goal:
Ω : Type u_1
Ω' : Type u_2
E : Type u_4
F : Type u_5
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
mE : MeasurableSpace E
mF : MeasurableSpace F
μ : Measure Ω
ν : Measure Ω'
inst : IsFiniteMeasure μ
X : Ω → E
Y : Ω → F
Z : Ω' → E
W : Ω' → F
hXZ : IdentDistrib X Z μ ν
hYW : IdentDistrib Y W μ ν
hXY : X ⟂ᵢ[μ] Y
hZW : Z ⟂ᵢ[ν] W
this : IsFiniteMeasure ν
rw :
  Eq (α := Measure (E × F)) (Measure.prod (Measure.map X μ) (Measure.map Y μ))
    (Measure.map (fun (ω' : Ω') ↦ (Z ω', W ω')) ν)
rw₁ :
  Eq (α := Measure (E × F)) (Measure.prod (Measure.map X μ) (Measure.map Y μ))
    (Measure.prod (Measure.map Z ν) (Measure.map W ν))
rw₂ :
  Eq (α := Measure (E × F)) (Measure.prod (Measure.map Z ν) (Measure.map Y μ))
    (Measure.prod (Measure.map Z ν) (Measure.map W ν))
rw₃ rw₄ :
  Eq (α := Measure (E × F)) (Measure.prod (Measure.map Z ν) (Measure.map W ν))
    (Measure.prod (Measure.map Z ν) (Measure.map W ν))
⊢ Eq (α := Measure (E × F)) (Measure.map (fun (ω : Ω) ↦ (X ω, Y ω)) μ) (Measure.map (fun (ω' : Ω') ↦ (Z ω', W ω')) ν)

Tactic:
rw [hXY.map_prod_eq_prod_map_map hXZ.aemeasurable_fst hYW.aemeasurable_fst,
      hZW.map_prod_eq_prod_map_map hXZ.aemeasurable_snd hYW.aemeasurable_snd,
      hXZ.map_eq, hYW.map_eq]

Premises used: ProbabilityTheory.IdentDistrib.aemeasurable_fst, ProbabilityTheory.IndepFun.map_prod_eq_prod_map_map, ProbabilityTheory.IdentDistrib.aemeasurable_snd, ProbabilityTheory.IdentDistrib.map_eq
-- Module: Mathlib.Probability.IdentDistribIndep
Goal:
Ω : Type u_1
Ω' : Type u_2
ι : Type u_3
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
μ : Measure Ω
ν : Measure Ω'
inst : Countable ι
E : ι → Type u_6
mE : (i : ι) → MeasurableSpace (E i)
X : (i : ι) → Ω → E i
Y : (i : ι) → Ω' → E i
h : ∀ (i : ι), IdentDistrib (X i) (Y i) μ ν
hX_ind : iIndepFun (β := E) X μ
hY_ind : iIndepFun (β := E) Y ν
⊢ IsProbabilityMeasure μ

Tactic:
have : IsProbabilityMeasure μ := hX_ind.isProbabilityMeasure
-- Module: Mathlib.Probability.IdentDistribIndep
Goal:
Ω : Type u_1
Ω' : Type u_2
ι : Type u_3
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
μ : Measure Ω
ν : Measure Ω'
inst : Countable ι
E : ι → Type u_6
mE : (i : ι) → MeasurableSpace (E i)
X : (i : ι) → Ω → E i
Y : (i : ι) → Ω' → E i
h : ∀ (i : ι), IdentDistrib (X i) (Y i) μ ν
hX_ind : iIndepFun (β := E) X μ
hY_ind : iIndepFun (β := E) Y ν
this : IsProbabilityMeasure μ
⊢ IsProbabilityMeasure ν

Tactic:
have : IsProbabilityMeasure ν := hY_ind.isProbabilityMeasure
-- Module: Mathlib.Probability.IdentDistribIndep
Goal:
Ω : Type u_1
Ω' : Type u_2
ι : Type u_3
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
μ : Measure Ω
ν : Measure Ω'
inst : Countable ι
E : ι → Type u_6
mE : (i : ι) → MeasurableSpace (E i)
X : (i : ι) → Ω → E i
Y : (i : ι) → Ω' → E i
h : ∀ (i : ι), IdentDistrib (X i) (Y i) μ ν
hX_ind : iIndepFun (β := E) X μ
hY_ind : iIndepFun (β := E) Y ν
this_1 : IsProbabilityMeasure μ
this : IsProbabilityMeasure ν
rw :
  Eq (α := Measure ((x : ι) → E x)) (Measure.infinitePi (X := E) fun (i : ι) ↦ Measure.map (X i) μ)
    (Measure.infinitePi (X := E) fun (i : ι) ↦ Measure.map (Y i) ν)
⊢ Eq (α := Measure ((x : ι) → E x)) (Measure.map (fun (ω : Ω) (x : ι) ↦ X x ω) μ)
    (Measure.map (fun (ω : Ω') (x : ι) ↦ Y x ω) ν)

Tactic:
rw [(iIndepFun_iff_map_fun_eq_infinitePi_map₀' (fun i ↦ (h i).aemeasurable_fst)).mp hX_ind,
      (iIndepFun_iff_map_fun_eq_infinitePi_map₀' (fun i ↦ (h i).aemeasurable_snd)).mp hY_ind]

Premises used: ProbabilityTheory.IdentDistrib.aemeasurable_fst, ProbabilityTheory.iIndepFun_iff_map_fun_eq_infinitePi_map₀', Iff.mp, ProbabilityTheory.IdentDistrib.aemeasurable_snd
-- Module: Mathlib.Probability.IdentDistribIndep
Goal:
Ω : Type u_1
Ω' : Type u_2
ι : Type u_3
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
μ : Measure Ω
ν : Measure Ω'
inst : Countable ι
E : ι → Type u_6
mE : (i : ι) → MeasurableSpace (E i)
X : (i : ι) → Ω → E i
Y : (i : ι) → Ω' → E i
h : ∀ (i : ι), IdentDistrib (X i) (Y i) μ ν
hX_ind : iIndepFun (β := E) X μ
hY_ind : iIndepFun (β := E) Y ν
this_1 : IsProbabilityMeasure μ
this : IsProbabilityMeasure ν
e_μ :
  ∀ (i : ι) (s : Set (E i)),
    MeasurableSet s →
      Eq (α := ENNReal) (((Measure.map (X i) μ : Measure (E i)) : (a : Set (E i)) → ENNReal) s : ENNReal)
        (((Measure.map (Y i) ν : Measure (E i)) : (a : Set (E i)) → ENNReal) s : ENNReal)
⊢ Eq (α := Measure ((x : ι) → E x)) (Measure.infinitePi (X := E) fun (i : ι) ↦ Measure.map (X i) μ)
    (Measure.infinitePi (X := E) fun (i : ι) ↦ Measure.map (Y i) ν)

Tactic:
congr with i
-- Module: Mathlib.Probability.IdentDistribIndep
Goal:
Ω : Type u_1
Ω' : Type u_2
ι : Type u_3
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
μ : Measure Ω
ν : Measure Ω'
inst : Countable ι
E : ι → Type u_6
mE : (i : ι) → MeasurableSpace (E i)
X : (i : ι) → Ω → E i
Y : (i : ι) → Ω' → E i
h : ∀ (i : ι), IdentDistrib (X i) (Y i) μ ν
hX_ind : iIndepFun (β := E) X μ
hY_ind : iIndepFun (β := E) Y ν
this_1 : IsProbabilityMeasure μ
this : IsProbabilityMeasure ν
i : ι
s : Set (E i)
h_1 : MeasurableSet s
e_μ e_μ₁ :
  Eq (α := ENNReal) (((Measure.map (Y i) ν : Measure (E i)) : (a : Set (E i)) → ENNReal) s : ENNReal)
    (((Measure.map (Y i) ν : Measure (E i)) : (a : Set (E i)) → ENNReal) s : ENNReal)
⊢ Eq (α := ENNReal) (((Measure.map (X i) μ : Measure (E i)) : (a : Set (E i)) → ENNReal) s : ENNReal)
    (((Measure.map (Y i) ν : Measure (E i)) : (a : Set (E i)) → ENNReal) s : ENNReal)

Tactic:
rw [(h i).map_eq]

Premises used: ProbabilityTheory.IdentDistrib.map_eq
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
x : MeasurableSpace Ω
π : ι → Set (Set Ω)
μ : Measure Ω
⊢ iIndepSets π μ ↔
    ∀ (s : Finset ι) {f : ι → Set Ω} (_H : ∀ i ∈ s, f i ∈ π i),
      Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ s, f i) : ℝ≥0∞) (∏ i ∈ s, (μ : (a : Set Ω) → ℝ≥0∞) (f i) : ℝ≥0∞)

Tactic:
simp only [iIndepSets, Kernel.iIndepSets, ae_dirac_eq, Filter.eventually_pure, Kernel.const_apply]

Premises used: MeasureTheory.ae_dirac_eq, Filter.eventually_pure, ProbabilityTheory.iIndepSets, ProbabilityTheory.Kernel.const_apply, ProbabilityTheory.Kernel.iIndepSets
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
π : ι → Set (Set Ω)
x : MeasurableSpace Ω
μ : Measure Ω
h : iIndepSets π μ
s : Finset ι
f : ι → Set Ω
hf : ∀ i ∈ s, f i ∈ π i
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ s, f i) : ℝ≥0∞) (∏ i ∈ s, (μ : (a : Set Ω) → ℝ≥0∞) (f i) : ℝ≥0∞)

Tactic:
(iIndepSets_iff _ _).1 h s hf

Premises used: ProbabilityTheory.iIndepSets_iff, Iff.mp
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
π : ι → Set (Set Ω)
x : MeasurableSpace Ω
μ : Measure Ω
h : iIndepSets π μ
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
simpa using h ∅ (f := fun _ ↦ univ)

Premises used: EmptyCollection.emptyCollection
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
π : ι → Set (Set Ω)
x : MeasurableSpace Ω
μ : Measure Ω
s : ι → Set Ω
inst : Fintype ι
h : iIndepSets π μ
hs : ∀ (i : ι), s i ∈ π i
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ (i : ι), s i) : ℝ≥0∞) (∏ i : ι, (μ : (a : Set Ω) → ℝ≥0∞) (s i) : ℝ≥0∞)

Tactic:
simp [← h.meas_biInter _ fun _i _ ↦ hs _]

Premises used: ProbabilityTheory.iIndepSets.meas_biInter
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
x : MeasurableSpace Ω
s1 s2 : Set (Set Ω)
μ : Measure Ω
⊢ IndepSets s1 s2 μ ↔
    ∀ (t1 t2 : Set Ω),
      t1 ∈ s1 →
        t2 ∈ s2 →
          (μ : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) =
            HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)

Tactic:
simp only [IndepSets, Kernel.IndepSets, ae_dirac_eq, Filter.eventually_pure, Kernel.const_apply]

Premises used: ProbabilityTheory.Kernel.IndepSets, MeasureTheory.ae_dirac_eq, ProbabilityTheory.IndepSets, Filter.eventually_pure, ProbabilityTheory.Kernel.const_apply
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
m : ι → MeasurableSpace Ω
_mΩ : MeasurableSpace Ω
μ : Measure Ω
⊢ iIndep m μ ↔ iIndepSets (fun (x : ι) ↦ {s : Set Ω | MeasurableSet s}) μ

Tactic:
simp only [iIndep, iIndepSets, Kernel.iIndep]

Premises used: ProbabilityTheory.Kernel.iIndep, ProbabilityTheory.iIndepSets, ProbabilityTheory.iIndep
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
m : ι → MeasurableSpace Ω
x : MeasurableSpace Ω
μ : Measure Ω
hμ : iIndep m μ
⊢ iIndepSets (fun (x : ι) ↦ {s : Set Ω | MeasurableSet s}) μ

Tactic:
(iIndep_iff_iIndepSets _ _).1 hμ

Premises used: ProbabilityTheory.iIndep_iff_iIndepSets, Iff.mp
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
m : ι → MeasurableSpace Ω
x : MeasurableSpace Ω
μ : Measure Ω
h : iIndep m μ
⊢ IsProbabilityMeasure μ

Tactic:
h.iIndepSets'.isProbabilityMeasure

Premises used: ProbabilityTheory.iIndepSets.isProbabilityMeasure, ProbabilityTheory.iIndep.iIndepSets'
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
m : ι → MeasurableSpace Ω
_mΩ : MeasurableSpace Ω
μ : Measure Ω
simp :
  (∀ (s : Finset ι) {f : ι → Set Ω}
      (_H : ∀ i ∈ s, Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} (f i)),
      Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ s, f i) : ℝ≥0∞)
        (∏ i ∈ s, (μ : (a : Set Ω) → ℝ≥0∞) (f i) : ℝ≥0∞)) ↔
    ∀ (s : Finset ι) {f : ι → Set Ω} (_H : ∀ i ∈ s, MeasurableSet (f i)),
      Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ s, f i) : ℝ≥0∞) (∏ i ∈ s, (μ : (a : Set Ω) → ℝ≥0∞) (f i) : ℝ≥0∞)
⊢ iIndep m μ ↔
    ∀ (s : Finset ι) {f : ι → Set Ω} (_H : ∀ i ∈ s, MeasurableSet (f i)),
      Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ s, f i) : ℝ≥0∞) (∏ i ∈ s, (μ : (a : Set Ω) → ℝ≥0∞) (f i) : ℝ≥0∞)

Tactic:
simp only [iIndep_iff_iIndepSets, iIndepSets_iff]

Premises used: ProbabilityTheory.iIndep_iff_iIndepSets, ProbabilityTheory.iIndepSets_iff
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
m : ι → MeasurableSpace Ω
_mΩ : MeasurableSpace Ω
μ : Measure Ω
⊢ (∀ (s : Finset ι) {f : ι → Set Ω}
      (_H : ∀ i ∈ s, Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} (f i)),
      Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ s, f i) : ℝ≥0∞)
        (∏ i ∈ s, (μ : (a : Set Ω) → ℝ≥0∞) (f i) : ℝ≥0∞)) ↔
    ∀ (s : Finset ι) {f : ι → Set Ω} (_H : ∀ i ∈ s, MeasurableSet (f i)),
      Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ s, f i) : ℝ≥0∞) (∏ i ∈ s, (μ : (a : Set Ω) → ℝ≥0∞) (f i) : ℝ≥0∞)

Tactic:
rfl
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
m : ι → MeasurableSpace Ω
x : MeasurableSpace Ω
μ : Measure Ω
S : Finset ι
s : ι → Set Ω
hμ : iIndep m μ
hs : ∀ i ∈ S, MeasurableSet (s i)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ S, s i) : ℝ≥0∞) (∏ i ∈ S, (μ : (a : Set Ω) → ℝ≥0∞) (s i) : ℝ≥0∞)

Tactic:
(iIndep_iff _ _).1 hμ _ hs

Premises used: ProbabilityTheory.iIndep_iff, Iff.mp
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
m : ι → MeasurableSpace Ω
x : MeasurableSpace Ω
μ : Measure Ω
s : ι → Set Ω
inst : Fintype ι
hμ : iIndep m μ
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ (i : ι), s i) : ℝ≥0∞) (∏ i : ι, (μ : (a : Set Ω) → ℝ≥0∞) (s i) : ℝ≥0∞)

Tactic:
simp [← hμ.meas_biInter fun _ _ ↦ hs _]

Premises used: ProbabilityTheory.iIndep.meas_biInter
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
m₁ m₂ _mΩ : MeasurableSpace Ω
μ : Measure Ω
⊢ Indep m₁ m₂ μ ↔ IndepSets {s : Set Ω | MeasurableSet s} {s : Set Ω | MeasurableSet s} μ

Tactic:
simp only [Indep, IndepSets, Kernel.Indep]

Premises used: ProbabilityTheory.Kernel.Indep, ProbabilityTheory.Indep, ProbabilityTheory.IndepSets
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
m₁ m₂ _mΩ : MeasurableSpace Ω
μ : Measure Ω
rw :
  (∀ (t1 t2 : Set Ω),
      Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} t1 →
        Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} t2 →
          (μ : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) =
            HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞)
              ((μ : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)) ↔
    ∀ (t1 t2 : Set Ω),
      MeasurableSet t1 →
        MeasurableSet t2 →
          (μ : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) =
            HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)
⊢ Indep m₁ m₂ μ ↔
    ∀ (t1 t2 : Set Ω),
      MeasurableSet t1 →
        MeasurableSet t2 →
          (μ : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) =
            HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)

Tactic:
rw [Indep_iff_IndepSets, IndepSets_iff]

Premises used: ProbabilityTheory.Indep_iff_IndepSets, ProbabilityTheory.IndepSets_iff
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
m₁ m₂ _mΩ : MeasurableSpace Ω
μ : Measure Ω
⊢ (∀ (t1 t2 : Set Ω),
      Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} t1 →
        Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} t2 →
          (μ : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) =
            HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞)
              ((μ : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)) ↔
    ∀ (t1 t2 : Set Ω),
      MeasurableSet t1 →
        MeasurableSet t2 →
          (μ : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) =
            HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)

Tactic:
rfl
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
x : MeasurableSpace Ω
s : ι → Set Ω
μ : Measure Ω
⊢ iIndepSet s μ ↔ iIndep (fun (i : ι) ↦ generateFrom {s i}) μ

Tactic:
simp only [iIndepSet, iIndep, Kernel.iIndepSet]

Premises used: ProbabilityTheory.iIndepSet, ProbabilityTheory.Kernel.iIndepSet, ProbabilityTheory.iIndep
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
x : MeasurableSpace Ω
μ : Measure Ω
s : ι → Set Ω
h : iIndepSet s μ
⊢ IsProbabilityMeasure μ

Tactic:
((iIndepSet_iff_iIndep _ _).1 h).isProbabilityMeasure

Premises used: Iff.mp, ProbabilityTheory.iIndepSet_iff_iIndep, ProbabilityTheory.iIndep.isProbabilityMeasure
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
x : MeasurableSpace Ω
s : ι → Set Ω
μ : Measure Ω
⊢ iIndepSet s μ ↔
    ∀ (s' : Finset ι) {f : ι → Set Ω} (_H : ∀ i ∈ s', MeasurableSet (f i)),
      Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ s', f i) : ℝ≥0∞) (∏ i ∈ s', (μ : (a : Set Ω) → ℝ≥0∞) (f i) : ℝ≥0∞)

Tactic:
simp only [iIndepSet_iff_iIndep, iIndep_iff]

Premises used: ProbabilityTheory.iIndep_iff, ProbabilityTheory.iIndepSet_iff_iIndep
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
x : MeasurableSpace Ω
s t : Set Ω
μ : Measure Ω
⊢ IndepSet s t μ ↔ Indep (generateFrom {s}) (generateFrom {t}) μ

Tactic:
simp only [IndepSet, Indep, Kernel.IndepSet]

Premises used: ProbabilityTheory.IndepSet, ProbabilityTheory.Indep, ProbabilityTheory.Kernel.IndepSet