awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (hypothesis)
Goal:
ι : Type u_6
Ω : Type u_7
α : Type u_8
β : Type u_9
mΩ : MeasurableSpace Ω
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure Ω
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (β := fun (i : ι) ↦ α × β) (fun (i : ι) (ω : Ω) ↦ (X i ω, Y i ω)) μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy : ∀ i ∉ s, Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (Y i ⁻¹' t i) : ℝ≥0∞) (0 : ℝ≥0∞)
ht : ∀ (i : ι), MeasurableSet (t i)
⊢ Eq (α := ℝ≥0∞) (μ[⋂ i ∈ s, f i | ⋂ (i : ι), Y i ⁻¹' t i] : ℝ≥0∞) (∏ i ∈ s, μ[f i | Y i ⁻¹' t i] : ℝ≥0∞)
have this : IsProbabilityMeasure μ
Tactic: have : IsProbabilityMeasure (μ : Measure Ω) := hindep.isProbabilityMeasure
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
Goal:
ι : Type u_6
Ω : Type u_7
α : Type u_8
β : Type u_9
mΩ : MeasurableSpace Ω
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure Ω
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (β := fun (i : ι) ↦ α × β) (fun (i : ι) (ω : Ω) ↦ (X i ω, Y i ω)) μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy : ∀ i ∉ s, Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (Y i ⁻¹' t i) : ℝ≥0∞) (0 : ℝ≥0∞)
ht : ∀ (i : ι), MeasurableSet (t i)
this : IsProbabilityMeasure μ
⊢ Eq (α := ℝ≥0∞) (μ[⋂ i ∈ s, f i | ⋂ (i : ι), Y i ⁻¹' t i] : ℝ≥0∞) (∏ i ∈ s, μ[f i | Y i ⁻¹' t i] : ℝ≥0∞)
have intro : ∀ (val : Fintype ι),
  Eq (α := ℝ≥0∞) (μ[⋂ i ∈ s, f i | ⋂ (i : ι), Y i ⁻¹' t i] : ℝ≥0∞) (∏ i ∈ s, μ[f i | Y i ⁻¹' t i] : ℝ≥0∞)
Tactic: cases nonempty_fintype ι
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
Goal:
ι : Type u_6
Ω : Type u_7
α : Type u_8
β : Type u_9
mΩ : MeasurableSpace Ω
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure Ω
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (β := fun (i : ι) ↦ α × β) (fun (i : ι) (ω : Ω) ↦ (X i ω, Y i ω)) μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy : ∀ i ∉ s, Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (Y i ⁻¹' t i) : ℝ≥0∞) (0 : ℝ≥0∞)
ht : ∀ (i : ι), MeasurableSet (t i)
this : IsProbabilityMeasure μ
val : Fintype ι
g : (i' : ι) → Set Ω := fun (i' : ι) ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
⊢ μ[⋂ i ∈ s, f i | ⋂ (i : ι), Y i ⁻¹' t i] =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) (⋂ (i : ι), Y i ⁻¹' t i))⁻¹ : ℝ≥0∞)
      ((μ : (a : Set Ω) → ℝ≥0∞) ((⋂ (i : ι), Y i ⁻¹' t i) ∩ ⋂ i ∈ s, f i) : ℝ≥0∞)
have hms : MeasurableSet.{u_7} (α := Ω) (⋂ (i : ι), Y i ⁻¹' t i)
Tactic: rw [cond_apply]
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
Goal:
ι : Type u_6
Ω : Type u_7
α : Type u_8
β : Type u_9
mΩ : MeasurableSpace Ω
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure Ω
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (β := fun (i : ι) ↦ α × β) (fun (i : ι) (ω : Ω) ↦ (X i ω, Y i ω)) μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy : ∀ i ∉ s, Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (Y i ⁻¹' t i) : ℝ≥0∞) (0 : ℝ≥0∞)
ht : ∀ (i : ι), MeasurableSet (t i)
this : IsProbabilityMeasure μ
val : Fintype ι
g : (i' : ι) → Set Ω := fun (i' : ι) ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) (⋂ (i : ι), Y i ⁻¹' t i))⁻¹ : ℝ≥0∞)
      ((μ : (a : Set Ω) → ℝ≥0∞) ((⋂ (i : ι), Y i ⁻¹' t i) ∩ ⋂ i ∈ s, f i) : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) (⋂ (i : ι), Y i ⁻¹' t i))⁻¹ : ℝ≥0∞)
      ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ (i : ι), g i) : ℝ≥0∞)
have e_a : Eq.{u_7 + 1} (α := Set Ω) ((⋂ (i : ι), Y i ⁻¹' t i) ∩ ⋂ i ∈ s, f i) (⋂ (i : ι), g i)
Tactic: congr
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
Goal:
ι : Type u_6
Ω : Type u_7
α : Type u_8
β : Type u_9
mΩ : MeasurableSpace Ω
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure Ω
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (β := fun (i : ι) ↦ α × β) (fun (i : ι) (ω : Ω) ↦ (X i ω, Y i ω)) μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy : ∀ i ∉ s, Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (Y i ⁻¹' t i) : ℝ≥0∞) (0 : ℝ≥0∞)
ht : ∀ (i : ι), MeasurableSet (t i)
this : IsProbabilityMeasure μ
val : Fintype ι
g : (i' : ι) → Set Ω := fun (i' : ι) ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
⊢ Eq.{u_7 + 1} (α := Set Ω) ((⋂ (i : ι), Y i ⁻¹' t i) ∩ ⋂ (i : ι), if i ∈ s then f i else univ)
    (⋂ (i : ι), Y i ⁻¹' t i ∩ if i ∈ s then f i else univ)
have rw : Eq.{u_7 + 1} (α := Set Ω) ((⋂ (i : ι), Y i ⁻¹' t i) ∩ ⋂ (i : ι), if i ∈ s then f i else univ)
  ((⋂ (i : ι), Y i ⁻¹' t i) ∩ ⋂ (i : ι), if i ∈ s then f i else univ)
Tactic: rw [Set.iInter_inter_distrib]
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
Goal:
ι : Type u_6
Ω : Type u_7
α : Type u_8
β : Type u_9
mΩ : MeasurableSpace Ω
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure Ω
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (β := fun (i : ι) ↦ α × β) (fun (i : ι) (ω : Ω) ↦ (X i ω, Y i ω)) μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy : ∀ i ∉ s, Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (Y i ⁻¹' t i) : ℝ≥0∞) (0 : ℝ≥0∞)
ht : ∀ (i : ι), MeasurableSet (t i)
this : IsProbabilityMeasure μ
val : Fintype ι
g : (i' : ι) → Set Ω := fun (i' : ι) ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
i : ι
⊢ (Y i ⁻¹' t i ∩ if i ∈ s then f i else univ) = g i
have pos : ∀ (hi : i ∈ s), (Y i ⁻¹' t i ∩ if i ∈ s then f i else univ) = g i
Tactic: by_cases hi : i ∈ s
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
Goal:
ι : Type u_6
Ω : Type u_7
α : Type u_8
β : Type u_9
mΩ : MeasurableSpace Ω
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure Ω
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (β := fun (i : ι) ↦ α × β) (fun (i : ι) (ω : Ω) ↦ (X i ω, Y i ω)) μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy : ∀ i ∉ s, Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (Y i ⁻¹' t i) : ℝ≥0∞) (0 : ℝ≥0∞)
ht : ∀ (i : ι), MeasurableSet (t i)
this : IsProbabilityMeasure μ
val : Fintype ι
g : (i' : ι) → Set Ω := fun (i' : ι) ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
i : ι
pos : ∀ (hi : i ∈ s), (Y i ⁻¹' t i ∩ if i ∈ s then f i else univ) = g i
⊢ (Y i ⁻¹' t i ∩ if i ∈ s then f i else univ) = g i
have neg : ∀ (hi : i ∉ s), (Y i ⁻¹' t i ∩ if i ∈ s then f i else univ) = g i
Tactic: by_cases hi : i ∈ s
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
Goal:
ι : Type u_6
Ω : Type u_7
α : Type u_8
β : Type u_9
mΩ : MeasurableSpace Ω
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure Ω
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (β := fun (i : ι) ↦ α × β) (fun (i : ι) (ω : Ω) ↦ (X i ω, Y i ω)) μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy : ∀ i ∉ s, Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (Y i ⁻¹' t i) : ℝ≥0∞) (0 : ℝ≥0∞)
ht : ∀ (i : ι), MeasurableSet (t i)
this : IsProbabilityMeasure μ
val : Fintype ι
g : (i' : ι) → Set Ω := fun (i' : ι) ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
⊢ Eq.{u_7 + 1} (α := Set Ω) ((⋂ (i : ι), Y i ⁻¹' t i) ∩ ⋂ i ∈ s, f i) (⋂ (i : ι), g i)
have _ : Eq.{u_7 + 1} (α := Set Ω) ((⋂ (i : ι), Y i ⁻¹' t i) ∩ ⋂ i ∈ s, f i)
  ((⋂ (i : ι), Y i ⁻¹' t i) ∩ ⋂ (i : ι), if i ∈ s then f i else univ)
Tactic: calc
        _ = (⋂ i, Y i ⁻¹' t i) ∩ ⋂ i, if i ∈ s then f i else .univ := by
          simp only [Set.iInter_ite, Set.iInter_univ, Set.inter_univ]
        _ = ⋂ i, Y i ⁻¹' t i ∩ (if i ∈ s then f i else .univ) := by rw [Set.iInter_inter_distrib]
        _ = _ := Set.iInter_congr fun i ↦ by by_cases hi : i ∈ s <;> simp [hi, g]
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
Goal:
ι : Type u_6
Ω : Type u_7
α : Type u_8
β : Type u_9
mΩ : MeasurableSpace Ω
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure Ω
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (β := fun (i : ι) ↦ α × β) (fun (i : ι) (ω : Ω) ↦ (X i ω, Y i ω)) μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy : ∀ i ∉ s, Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (Y i ⁻¹' t i) : ℝ≥0∞) (0 : ℝ≥0∞)
ht : ∀ (i : ι), MeasurableSet (t i)
this : IsProbabilityMeasure μ
val : Fintype ι
g : (i' : ι) → Set Ω := fun (i' : ι) ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
_ :
  Eq.{u_7 + 1} (α := Set Ω) ((⋂ (i : ι), Y i ⁻¹' t i) ∩ ⋂ i ∈ s, f i)
    ((⋂ (i : ι), Y i ⁻¹' t i) ∩ ⋂ (i : ι), if i ∈ s then f i else univ)
⊢ Eq.{u_7 + 1} (α := Set Ω) ((⋂ (i : ι), Y i ⁻¹' t i) ∩ ⋂ i ∈ s, f i) (⋂ (i : ι), g i)
have _₁ : Eq.{u_7 + 1} (α := Set Ω) ((⋂ (i : ι), Y i ⁻¹' t i) ∩ ⋂ (i : ι), if i ∈ s then f i else univ)
  (⋂ (i : ι), Y i ⁻¹' t i ∩ if i ∈ s then f i else univ)
Tactic: calc
        _ = (⋂ i, Y i ⁻¹' t i) ∩ ⋂ i, if i ∈ s then f i else .univ := by
          simp only [Set.iInter_ite, Set.iInter_univ, Set.inter_univ]
        _ = ⋂ i, Y i ⁻¹' t i ∩ (if i ∈ s then f i else .univ) := by rw [Set.iInter_inter_distrib]
        _ = _ := Set.iInter_congr fun i ↦ by by_cases hi : i ∈ s <;> simp [hi, g]
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
Goal:
ι : Type u_6
Ω : Type u_7
α : Type u_8
β : Type u_9
mΩ : MeasurableSpace Ω
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure Ω
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (β := fun (i : ι) ↦ α × β) (fun (i : ι) (ω : Ω) ↦ (X i ω, Y i ω)) μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy : ∀ i ∉ s, Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (Y i ⁻¹' t i) : ℝ≥0∞) (0 : ℝ≥0∞)
ht : ∀ (i : ι), MeasurableSet (t i)
this : IsProbabilityMeasure μ
val : Fintype ι
g : (i' : ι) → Set Ω := fun (i' : ι) ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) (⋂ (i : ι), Y i ⁻¹' t i))⁻¹ : ℝ≥0∞)
      ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ (i : ι), g i) : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((∏ i : ι, (μ : (a : Set Ω) → ℝ≥0∞) (Y i ⁻¹' t i))⁻¹ : ℝ≥0∞)
      ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ (i : ι), g i) : ℝ≥0∞)
have rw : ∀ (i : ι), MeasurableSet (Y i ⁻¹' t i)
Tactic: rw [hindep.meas_iInter]
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
Goal:
ι : Type u_6
Ω : Type u_7
α : Type u_8
β : Type u_9
mΩ : MeasurableSpace Ω
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure Ω
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (β := fun (i : ι) ↦ α × β) (fun (i : ι) (ω : Ω) ↦ (X i ω, Y i ω)) μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy : ∀ i ∉ s, Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (Y i ⁻¹' t i) : ℝ≥0∞) (0 : ℝ≥0∞)
ht : ∀ (i : ι), MeasurableSet (t i)
this : IsProbabilityMeasure μ
val : Fintype ι
g : (i' : ι) → Set Ω := fun (i' : ι) ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
i : ι
⊢ (fun (ω : Ω) ↦ (X i ω, Y i ω)) ⁻¹' SProd.sprod (α := Set α) univ (t i) = Y i ⁻¹' t i
have h : ∀ (x : Ω),
  Membership.mem (γ := Set Ω) ((fun (ω : Ω) ↦ (X i ω, Y i ω)) ⁻¹' SProd.sprod (α := Set α) univ (t i)) x ↔
    x ∈ Y i ⁻¹' t i
Tactic: ext
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
Goal:
ι : Type u_6
Ω : Type u_7
α : Type u_8
β : Type u_9
mΩ : MeasurableSpace Ω
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure Ω
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (β := fun (i : ι) ↦ α × β) (fun (i : ι) (ω : Ω) ↦ (X i ω, Y i ω)) μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy : ∀ i ∉ s, Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (Y i ⁻¹' t i) : ℝ≥0∞) (0 : ℝ≥0∞)
ht : ∀ (i : ι), MeasurableSet (t i)
this : IsProbabilityMeasure μ
val : Fintype ι
g : (i' : ι) → Set Ω := fun (i' : ι) ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((∏ i : ι, (μ : (a : Set Ω) → ℝ≥0∞) (Y i ⁻¹' t i))⁻¹ : ℝ≥0∞)
      ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ (i : ι), g i) : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (∏ i : ι, (μ : (a : Set Ω) → ℝ≥0∞) (Y i ⁻¹' t i))⁻¹ (∏ i : ι, (μ : (a : Set Ω) → ℝ≥0∞) (g i))
have rw : ∀ (i : ι), MeasurableSet (g i)
Tactic: rw [hindep.meas_iInter]
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
Goal:
ι : Type u_6
Ω : Type u_7
α : Type u_8
β : Type u_9
mΩ : MeasurableSpace Ω
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure Ω
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (β := fun (i : ι) ↦ α × β) (fun (i : ι) (ω : Ω) ↦ (X i ω, Y i ω)) μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy : ∀ i ∉ s, Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (Y i ⁻¹' t i) : ℝ≥0∞) (0 : ℝ≥0∞)
ht : ∀ (i : ι), MeasurableSet (t i)
this : IsProbabilityMeasure μ
val : Fintype ι
g : (i' : ι) → Set Ω := fun (i' : ι) ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
i : ι
⊢ MeasurableSet (g i)
have pos : ∀ (hi : i ∈ s), MeasurableSet (g i)
Tactic: by_cases hi : i ∈ s
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
Goal:
ι : Type u_6
Ω : Type u_7
α : Type u_8
β : Type u_9
mΩ : MeasurableSpace Ω
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure Ω
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (β := fun (i : ι) ↦ α × β) (fun (i : ι) (ω : Ω) ↦ (X i ω, Y i ω)) μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy : ∀ i ∉ s, Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (Y i ⁻¹' t i) : ℝ≥0∞) (0 : ℝ≥0∞)
ht : ∀ (i : ι), MeasurableSet (t i)
this : IsProbabilityMeasure μ
val : Fintype ι
g : (i' : ι) → Set Ω := fun (i' : ι) ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
i : ι
pos : ∀ (hi : i ∈ s), MeasurableSet (g i)
⊢ MeasurableSet (g i)
have neg : ∀ (hi : i ∉ s), MeasurableSet (g i)
Tactic: by_cases hi : i ∈ s
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
Goal:
ι : Type u_6
Ω : Type u_7
α : Type u_8
β : Type u_9
mΩ : MeasurableSpace Ω
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure Ω
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (β := fun (i : ι) ↦ α × β) (fun (i : ι) (ω : Ω) ↦ (X i ω, Y i ω)) μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy : ∀ i ∉ s, Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (Y i ⁻¹' t i) : ℝ≥0∞) (0 : ℝ≥0∞)
ht : ∀ (i : ι), MeasurableSet (t i)
this : IsProbabilityMeasure μ
val : Fintype ι
g : (i' : ι) → Set Ω := fun (i' : ι) ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
i : ι
hi : i ∈ s
⊢ MeasurableSet (g i)
have pos : MeasurableSet (Y i ⁻¹' t i ∩ f i)
Tactic: simp only [hi, ↓reduceIte, g]
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
Goal:
ι : Type u_6
Ω : Type u_7
α : Type u_8
β : Type u_9
mΩ : MeasurableSpace Ω
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure Ω
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (β := fun (i : ι) ↦ α × β) (fun (i : ι) (ω : Ω) ↦ (X i ω, Y i ω)) μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy : ∀ i ∉ s, Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (Y i ⁻¹' t i) : ℝ≥0∞) (0 : ℝ≥0∞)
ht : ∀ (i : ι), MeasurableSet (t i)
this : IsProbabilityMeasure μ
val : Fintype ι
g : (i' : ι) → Set Ω := fun (i' : ι) ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
i : ι
hi : i ∉ s
⊢ MeasurableSet (g i)
have neg : MeasurableSet (Y i ⁻¹' t i)
Tactic: simp only [hi, ↓reduceIte, g]
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
Goal:
ι : Type u_6
Ω : Type u_7
α : Type u_8
β : Type u_9
mΩ : MeasurableSpace Ω
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure Ω
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (β := fun (i : ι) ↦ α × β) (fun (i : ι) (ω : Ω) ↦ (X i ω, Y i ω)) μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy : ∀ i ∉ s, Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (Y i ⁻¹' t i) : ℝ≥0∞) (0 : ℝ≥0∞)
ht : ∀ (i : ι), MeasurableSet (t i)
this : IsProbabilityMeasure μ
val : Fintype ι
g : (i' : ι) → Set Ω := fun (i' : ι) ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
i : ι
hi : i ∈ s
⊢ MeasurableSet (Y i ⁻¹' t i ∩ f i)
have pos : ∀ (A : Set α) (hA : MeasurableSet A) (hA' : X i ⁻¹' A = f i), MeasurableSet (Y i ⁻¹' t i ∩ f i)
Tactic: obtain ⟨A, hA, hA'⟩ := hf i hi
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
Goal:
ι : Type u_6
Ω : Type u_7
α : Type u_8
β : Type u_9
mΩ : MeasurableSpace Ω
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure Ω
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (β := fun (i : ι) ↦ α × β) (fun (i : ι) (ω : Ω) ↦ (X i ω, Y i ω)) μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy : ∀ i ∉ s, Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (Y i ⁻¹' t i) : ℝ≥0∞) (0 : ℝ≥0∞)
ht : ∀ (i : ι), MeasurableSet (t i)
this : IsProbabilityMeasure μ
val : Fintype ι
g : (i' : ι) → Set Ω := fun (i' : ι) ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
i : ι
hi : i ∈ s
A : Set α
hA : MeasurableSet A
hA' : X i ⁻¹' A = f i
⊢ (fun (ω : Ω) ↦ (X i ω, Y i ω)) ⁻¹' SProd.sprod (α := Set α) univ (t i) = Y i ⁻¹' t i
have h : ∀ (x : Ω),
  Membership.mem (γ := Set Ω) ((fun (ω : Ω) ↦ (X i ω, Y i ω)) ⁻¹' SProd.sprod (α := Set α) univ (t i)) x ↔
    x ∈ Y i ⁻¹' t i
Tactic: ext
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
Goal:
ι : Type u_6
Ω : Type u_7
α : Type u_8
β : Type u_9
mΩ : MeasurableSpace Ω
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure Ω
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (β := fun (i : ι) ↦ α × β) (fun (i : ι) (ω : Ω) ↦ (X i ω, Y i ω)) μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy : ∀ i ∉ s, Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (Y i ⁻¹' t i) : ℝ≥0∞) (0 : ℝ≥0∞)
ht : ∀ (i : ι), MeasurableSet (t i)
this : IsProbabilityMeasure μ
val : Fintype ι
g : (i' : ι) → Set Ω := fun (i' : ι) ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
i : ι
hi : i ∈ s
A : Set α
hA : MeasurableSet A
hA' : X i ⁻¹' A = f i
⊢ (fun (ω : Ω) ↦ (X i ω, Y i ω)) ⁻¹' SProd.sprod (β := Set β) A univ = f i
have h : ∀ (x : Ω), Membership.mem (γ := Set Ω) ((fun (ω : Ω) ↦ (X i ω, Y i ω)) ⁻¹' SProd.sprod (β := Set β) A univ) x ↔ x ∈ f i
Tactic: ext
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
Goal:
ι : Type u_6
Ω : Type u_7
α : Type u_8
β : Type u_9
mΩ : MeasurableSpace Ω
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure Ω
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (β := fun (i : ι) ↦ α × β) (fun (i : ι) (ω : Ω) ↦ (X i ω, Y i ω)) μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy : ∀ i ∉ s, Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (Y i ⁻¹' t i) : ℝ≥0∞) (0 : ℝ≥0∞)
ht : ∀ (i : ι), MeasurableSet (t i)
this : IsProbabilityMeasure μ
val : Fintype ι
g : (i' : ι) → Set Ω := fun (i' : ι) ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
i : ι
hi : i ∉ s
⊢ (fun (ω : Ω) ↦ (X i ω, Y i ω)) ⁻¹' SProd.sprod (α := Set α) univ (t i) = Y i ⁻¹' t i
have h : ∀ (x : Ω),
  Membership.mem (γ := Set Ω) ((fun (ω : Ω) ↦ (X i ω, Y i ω)) ⁻¹' SProd.sprod (α := Set α) univ (t i)) x ↔
    x ∈ Y i ⁻¹' t i
Tactic: ext
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
Goal:
ι : Type u_6
Ω : Type u_7
α : Type u_8
β : Type u_9
mΩ : MeasurableSpace Ω
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure Ω
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (β := fun (i : ι) ↦ α × β) (fun (i : ι) (ω : Ω) ↦ (X i ω, Y i ω)) μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy : ∀ i ∉ s, Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (Y i ⁻¹' t i) : ℝ≥0∞) (0 : ℝ≥0∞)
ht : ∀ (i : ι), MeasurableSet (t i)
this : IsProbabilityMeasure μ
val : Fintype ι
g : (i' : ι) → Set Ω := fun (i' : ι) ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
⊢ HMul.hMul (α := ℝ≥0∞) (∏ i : ι, (μ : (a : Set Ω) → ℝ≥0∞) (Y i ⁻¹' t i))⁻¹ (∏ i : ι, (μ : (a : Set Ω) → ℝ≥0∞) (g i)) =
    ∏ i : ι,
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) (Y i ⁻¹' t i))⁻¹ : ℝ≥0∞)
        ((μ : (a : Set Ω) → ℝ≥0∞) (g i) : ℝ≥0∞)
have rw : (↑Finset.univ : Set ι).Pairwise fun (i j : ι) ↦
  Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (Y i ⁻¹' t i) : ℝ≥0∞) (0 : ℝ≥0∞) ∨
    Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (Y j ⁻¹' t j) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [Finset.prod_mul_distrib, ENNReal.prod_inv_distrib]
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
Goal:
ι : Type u_6
Ω : Type u_7
α : Type u_8
β : Type u_9
mΩ : MeasurableSpace Ω
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure Ω
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (β := fun (i : ι) ↦ α × β) (fun (i : ι) (ω : Ω) ↦ (X i ω, Y i ω)) μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy : ∀ i ∉ s, Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (Y i ⁻¹' t i) : ℝ≥0∞) (0 : ℝ≥0∞)
ht : ∀ (i : ι), MeasurableSet (t i)
this : IsProbabilityMeasure μ
val : Fintype ι
g : (i' : ι) → Set Ω := fun (i' : ι) ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
⊢ Eq (α := ℝ≥0∞)
    (∏ i : ι,
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) (Y i ⁻¹' t i))⁻¹ : ℝ≥0∞)
        ((μ : (a : Set Ω) → ℝ≥0∞) (g i) : ℝ≥0∞))
    (∏ i : ι, if i ∈ s then μ[f i | Y i ⁻¹' t i] else 1)
have refine : ∀ (i : ι),
  Membership.mem (γ := Finset ι) Finset.univ i →
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) (Y i ⁻¹' t i))⁻¹ : ℝ≥0∞)
        ((μ : (a : Set Ω) → ℝ≥0∞) (g i) : ℝ≥0∞) =
      if i ∈ s then μ[f i | Y i ⁻¹' t i] else 1
Tactic: refine Finset.prod_congr rfl fun i _ ↦ ?_
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
Goal:
ι : Type u_6
Ω : Type u_7
α : Type u_8
β : Type u_9
mΩ : MeasurableSpace Ω
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure Ω
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (β := fun (i : ι) ↦ α × β) (fun (i : ι) (ω : Ω) ↦ (X i ω, Y i ω)) μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy : ∀ i ∉ s, Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (Y i ⁻¹' t i) : ℝ≥0∞) (0 : ℝ≥0∞)
ht : ∀ (i : ι), MeasurableSet (t i)
this : IsProbabilityMeasure μ
val : Fintype ι
g : (i' : ι) → Set Ω := fun (i' : ι) ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
i : ι
h : Membership.mem (γ := Finset ι) Finset.univ i
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) (Y i ⁻¹' t i))⁻¹ : ℝ≥0∞)
      ((μ : (a : Set Ω) → ℝ≥0∞) (g i) : ℝ≥0∞) =
    if i ∈ s then μ[f i | Y i ⁻¹' t i] else 1
have pos : ∀ (hi : i ∈ s),
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) (Y i ⁻¹' t i))⁻¹ : ℝ≥0∞)
      ((μ : (a : Set Ω) → ℝ≥0∞) (g i) : ℝ≥0∞) =
    if i ∈ s then μ[f i | Y i ⁻¹' t i] else 1
Tactic: by_cases hi : i ∈ s