awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.Indep (goal)
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
a : ι
S : Finset ι
hp_ind : iIndepSets π κ μ
haS : a ∉ S
t1 t2 : Set Ω
s : Finset ι
hs_mem : s ⊆ S
ft1 : ι → Set Ω
hft1_mem : ∀ x ∈ s, ft1 x ∈ π x
ht1_eq : t1 = ⋂ x ∈ s, ft1 x
ht2_mem_pia : t2 ∈ π a
f : (n : ι) → Set Ω := fun (n : ι) ↦ if n = a then t2 else if n ∈ s then ft1 n else univ
h_f_mem : ∀ n ∈ insert a s, f n ∈ π n
h_f_mem_pi : ∀ n ∈ s, f n ∈ π n
h_t1 : t1 = ⋂ n ∈ s, f n
h_μ_t1 :
  ∀ᵐ (a' : α) ∂μ,
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞)
      (∏ n ∈ s, (((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f n) : ℝ≥0∞)
h_t2 : t2 = f a
h_μ_inter :
  ∀ᵐ (a' : α) ∂μ,
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) : ℝ≥0∞)
      (∏ n ∈ insert a s, (((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f n) : ℝ≥0∞)
has : a ∉ s
⊢ ∀ᵐ (a : α) ∂μ,
    (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)
have h : ∀ (a' : α)
  (ha1 :
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞)
      (∏ n ∈ s, (((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f n) : ℝ≥0∞))
  (ha2 :
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) : ℝ≥0∞)
      (∏ n ∈ insert a s, (((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f n) : ℝ≥0∞)),
  (((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞)
      ((((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)
Tactic: filter_upwards [h_μ_t1, h_μ_inter] with a' ha1 ha2
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.Indep (goal)
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
a : ι
S : Finset ι
hp_ind : iIndepSets π κ μ
haS : a ∉ S
t1 t2 : Set Ω
s : Finset ι
hs_mem : s ⊆ S
ft1 : ι → Set Ω
hft1_mem : ∀ x ∈ s, ft1 x ∈ π x
ht1_eq : t1 = ⋂ x ∈ s, ft1 x
ht2_mem_pia : t2 ∈ π a
f : (n : ι) → Set Ω := fun (n : ι) ↦ if n = a then t2 else if n ∈ s then ft1 n else univ
h_f_mem : ∀ n ∈ insert a s, f n ∈ π n
h_f_mem_pi : ∀ n ∈ s, f n ∈ π n
h_t1 : t1 = ⋂ n ∈ s, f n
h_μ_t1 :
  ∀ᵐ (a' : α) ∂μ,
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞)
      (∏ n ∈ s, (((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f n) : ℝ≥0∞)
h_t2 : t2 = f a
h_μ_inter :
  ∀ᵐ (a' : α) ∂μ,
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) : ℝ≥0∞)
      (∏ n ∈ insert a s, (((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f n) : ℝ≥0∞)
has : a ∉ s
a' : α
ha1 :
  Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞)
    (∏ n ∈ s, (((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f n) : ℝ≥0∞)
ha2 :
  Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) : ℝ≥0∞)
    (∏ n ∈ insert a s, (((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f n) : ℝ≥0∞)
⊢ (((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞)
      ((((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)
have h : ∏ n ∈ insert a s, (((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f n) =
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞)
    ((((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)
Tactic: rw [ha2, Finset.prod_insert has, h_t2, mul_comm, ha1]
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.Indep (goal)
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
a : ι
S : Finset ι
hp_ind : iIndepSets π κ μ
haS : a ∉ S
t1 t2 : Set Ω
s : Finset ι
hs_mem : s ⊆ S
ft1 : ι → Set Ω
hft1_mem : ∀ x ∈ s, ft1 x ∈ π x
ht1_eq : t1 = ⋂ x ∈ s, ft1 x
ht2_mem_pia : t2 ∈ π a
f : (n : ι) → Set Ω := fun (n : ι) ↦ if n = a then t2 else if n ∈ s then ft1 n else univ
h_f_mem : ∀ n ∈ insert a s, f n ∈ π n
h_f_mem_pi : ∀ n ∈ s, f n ∈ π n
h_t1 : t1 = ⋂ n ∈ s, f n
h_μ_t1 :
  ∀ᵐ (a' : α) ∂μ,
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞)
      (∏ n ∈ s, (((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f n) : ℝ≥0∞)
h_t2 : t2 = f a
h_μ_inter :
  ∀ᵐ (a' : α) ∂μ,
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) : ℝ≥0∞)
      (∏ n ∈ insert a s, (((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f n) : ℝ≥0∞)
has : a ∉ s
a' : α
ha1 :
  Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞)
    (∏ n ∈ s, (((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f n) : ℝ≥0∞)
ha2 :
  Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) : ℝ≥0∞)
    (∏ n ∈ insert a s, (((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f n) : ℝ≥0∞)
h :
  ∏ n ∈ insert a s, (((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f n) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞)
      ((((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)
⊢ (((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞)
      ((((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)
have h₁ : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f a) : ℝ≥0∞)
    (∏ x ∈ s, (((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f x) : ℝ≥0∞) =
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞)
    ((((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)
Tactic: rw [ha2, Finset.prod_insert has, h_t2, mul_comm, ha1]
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.Indep (goal)
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
a : ι
S : Finset ι
hp_ind : iIndepSets π κ μ
haS : a ∉ S
t1 t2 : Set Ω
s : Finset ι
hs_mem : s ⊆ S
ft1 : ι → Set Ω
hft1_mem : ∀ x ∈ s, ft1 x ∈ π x
ht1_eq : t1 = ⋂ x ∈ s, ft1 x
ht2_mem_pia : t2 ∈ π a
f : (n : ι) → Set Ω := fun (n : ι) ↦ if n = a then t2 else if n ∈ s then ft1 n else univ
h_f_mem : ∀ n ∈ insert a s, f n ∈ π n
h_f_mem_pi : ∀ n ∈ s, f n ∈ π n
h_t1 : t1 = ⋂ n ∈ s, f n
h_μ_t1 :
  ∀ᵐ (a' : α) ∂μ,
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞)
      (∏ n ∈ s, (((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f n) : ℝ≥0∞)
h_t2 : t2 = f a
h_μ_inter :
  ∀ᵐ (a' : α) ∂μ,
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) : ℝ≥0∞)
      (∏ n ∈ insert a s, (((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f n) : ℝ≥0∞)
has : a ∉ s
a' : α
ha1 :
  Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞)
    (∏ n ∈ s, (((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f n) : ℝ≥0∞)
ha2 :
  Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) : ℝ≥0∞)
    (∏ n ∈ insert a s, (((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f n) : ℝ≥0∞)
h :
  ∏ n ∈ insert a s, (((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f n) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞)
      ((((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)
h₁ :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f a) : ℝ≥0∞)
      (∏ x ∈ s, (((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f x) : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞)
      ((((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)
⊢ (((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞)
      ((((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)
have h₂ : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f a) : ℝ≥0∞)
    (∏ x ∈ s, (((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f x) : ℝ≥0∞) =
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞)
    ((((κ : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f a) : ℝ≥0∞)
Tactic: rw [ha2, Finset.prod_insert has, h_t2, mul_comm, ha1]
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.Indep (goal)
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
a : ι
S : Finset ι
hp_ind : iIndepSets π κ μ
haS : a ∉ S
t1 t2 : Set Ω
s : Finset ι
hs_mem : s ⊆ S
ft1 : ι → Set Ω
hft1_mem : ∀ x ∈ s, ft1 x ∈ π x
ht1_eq : t1 = ⋂ x ∈ s, ft1 x
ht2_mem_pia : t2 ∈ π a
let let₁ let₂ :
  ∀ᵐ (a : α) ∂μ,
    (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)
⊢ ∀ᵐ (a : α) ∂μ,
    (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)
have let₃ : let f : (n : ι) → Set Ω := fun (n : ι) ↦ if n = a then t2 else if n ∈ s then ft1 n else univ;
∀ (h_f_mem : ∀ n ∈ insert a s, f n ∈ π n),
  ∀ᵐ (a : α) ∂μ,
    (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)
Tactic: classical
  let f := fun n => ite (n = a) t2 (ite (n ∈ s) (ft1 n) Set.univ)
  have h_f_mem : ∀ n ∈ insert a s, f n ∈ π n := by
    intro n hn_mem_insert
    dsimp only [f]
    rcases Finset.mem_insert.mp hn_mem_insert with hn_mem | hn_mem
    · simp [hn_mem, ht2_mem_pia]
    · grind
  have h_f_mem_pi : ∀ n ∈ s, f n ∈ π n := fun x hxS => h_f_mem x (by simp [hxS])
  have h_t1 : t1 = ⋂ n ∈ s, f n := by
    suffices h_forall : ∀ n ∈ s, f n = ft1 n by grind
    intro n hnS
    have hn_ne_a : n ≠ a := by rintro rfl; exact haS (hs_mem hnS)
    simp_rw [f, if_pos hnS, if_neg hn_ne_a]
  have h_μ_t1 : ∀ᵐ a' ∂μ, κ a' t1 = ∏ n ∈ s, κ a' (f n) := by
    filter_upwards [hp_ind s h_f_mem_pi] with a' ha'
    rw [h_t1, ← ha']
  have h_t2 : t2 = f a := by simp [f]
  have h_μ_inter : ∀ᵐ a' ∂μ, κ a' (t1 ∩ t2) = ∏ n ∈ insert a s, κ a' (f n) := by
    have h_t1_inter_t2 : t1 ∩ t2 = ⋂ n ∈ insert a s, f n := by
      rw [h_t1, h_t2, Finset.set_biInter_insert, Set.inter_comm]
    filter_upwards [hp_ind (insert a s) h_f_mem] with a' ha'
    rw [h_t1_inter_t2, ← ha']
  have has : a ∉ s := fun has_mem => haS (hs_mem has_mem)
  filter_upwards [h_μ_t1, h_μ_inter] with a' ha1 ha2
  rw [ha2, Finset.prod_insert has, h_t2, mul_comm, ha1]
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.Indep (goal)
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
m : ι → MeasurableSpace Ω
h_le : ∀ (i : ι), m i ≤ _mΩ
π : ι → Set (Set Ω)
h_pi : ∀ (n : ι), IsPiSystem (π n)
h_generate : ∀ (i : ι), m i = generateFrom (π i)
h_ind : iIndepSets π κ μ
⊢ Kernel.iIndep m κ μ
have inl : ∀ (h_ind : iIndepSets π κ 0), Kernel.iIndep m κ 0
Tactic: rcases eq_or_ne μ 0 with rfl | hμ
Cleared hypotheses: μ, h_ind
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.Indep (goal)
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
m : ι → MeasurableSpace Ω
h_le : ∀ (i : ι), m i ≤ _mΩ
π : ι → Set (Set Ω)
h_pi : ∀ (n : ι), IsPiSystem (π n)
h_generate : ∀ (i : ι), m i = generateFrom (π i)
h_ind : iIndepSets π κ μ
inl : ∀ (h_ind : iIndepSets π κ 0), Kernel.iIndep m κ 0
⊢ Kernel.iIndep m κ μ
have inr : ∀ (hμ : μ ≠ 0), Kernel.iIndep m κ μ
Tactic: rcases eq_or_ne μ 0 with rfl | hμ
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.Indep (goal)
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
m : ι → MeasurableSpace Ω
h_le : ∀ (i : ι), m i ≤ _mΩ
π : ι → Set (Set Ω)
h_pi : ∀ (n : ι), IsPiSystem (π n)
h_generate : ∀ (i : ι), m i = generateFrom (π i)
h_ind : iIndepSets π κ μ
hμ : μ ≠ 0
⊢ Kernel.iIndep m κ μ
have inr : ∀ (η : Kernel α Ω)
  (η_eq : Filter.EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μ) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω))
  (hη : IsMarkovKernel η), Kernel.iIndep m κ μ
Tactic: obtain ⟨η, η_eq, hη⟩ : ∃ (η : Kernel α Ω), κ =ᵐ[μ] η ∧ IsMarkovKernel η :=
    exists_ae_eq_isMarkovKernel h_ind.ae_isProbabilityMeasure hμ
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.Indep (goal)
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
m : ι → MeasurableSpace Ω
h_le : ∀ (i : ι), m i ≤ _mΩ
π : ι → Set (Set Ω)
h_pi : ∀ (n : ι), IsPiSystem (π n)
h_generate : ∀ (i : ι), m i = generateFrom (π i)
h_ind : iIndepSets π κ μ
hμ : μ ≠ 0
η : Kernel α Ω
η_eq : Filter.EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μ) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω)
hη : IsMarkovKernel η
⊢ Kernel.iIndep m κ μ
have inr : Kernel.iIndep m η μ
Tactic: apply iIndep.congr (Filter.EventuallyEq.symm η_eq)
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.Indep (goal)
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
m : ι → MeasurableSpace Ω
h_le : ∀ (i : ι), m i ≤ _mΩ
π : ι → Set (Set Ω)
h_pi : ∀ (n : ι), IsPiSystem (π n)
h_generate : ∀ (i : ι), m i = generateFrom (π i)
h_ind : iIndepSets π κ μ
hμ : μ ≠ 0
η : Kernel α Ω
η_eq : Filter.EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μ) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω)
hη : IsMarkovKernel η
s : Finset ι
f : ι → Set Ω
⊢ ∀
    (_H :
      ∀ i ∈ s,
        Membership.mem (γ := Set (Set Ω)) ((fun (x : ι) ↦ ({s : Set Ω | MeasurableSet s} : Set (Set Ω))) i) (f i)),
    ∀ᵐ (a : α) ∂μ,
      Eq (α := ℝ≥0∞) ((((η : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ s, f i) : ℝ≥0∞)
        (∏ i ∈ s, (((η : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i) : ℝ≥0∞)
have inr : ∀
  (_H :
    ∀ (i : ι),
      Membership.mem (γ := Finset ι) ∅ i →
        Membership.mem (γ := Set (Set Ω)) ((fun (x : ι) ↦ ({s : Set Ω | MeasurableSet s} : Set (Set Ω))) i) (f i)),
  ∀ᵐ (a : α) ∂μ,
    Eq (α := ℝ≥0∞)
      ((((η : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
          (⋂ (i : ι), ⋂ (_ : Membership.mem (γ := Finset ι) ∅ i), f i) :
        ℝ≥0∞)
      (∏ i ∈ ∅, (((η : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i) : ℝ≥0∞)
Tactic: refine Finset.induction ?_ ?_ s
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.Indep (goal)
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
m : ι → MeasurableSpace Ω
h_le : ∀ (i : ι), m i ≤ _mΩ
π : ι → Set (Set Ω)
h_pi : ∀ (n : ι), IsPiSystem (π n)
h_generate : ∀ (i : ι), m i = generateFrom (π i)
h_ind : iIndepSets π κ μ
hμ : μ ≠ 0
η : Kernel α Ω
η_eq : Filter.EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μ) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω)
hη : IsMarkovKernel η
s : Finset ι
f : ι → Set Ω
inr :
  ∀
    (_H :
      ∀ (i : ι),
        Membership.mem (γ := Finset ι) ∅ i →
          Membership.mem (γ := Set (Set Ω)) ((fun (x : ι) ↦ ({s : Set Ω | MeasurableSet s} : Set (Set Ω))) i) (f i)),
    ∀ᵐ (a : α) ∂μ,
      Eq (α := ℝ≥0∞)
        ((((η : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
            (⋂ (i : ι), ⋂ (_ : Membership.mem (γ := Finset ι) ∅ i), f i) :
          ℝ≥0∞)
        (∏ i ∈ ∅, (((η : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i) : ℝ≥0∞)
⊢ ∀
    (_H :
      ∀ i ∈ s,
        Membership.mem (γ := Set (Set Ω)) ((fun (x : ι) ↦ ({s : Set Ω | MeasurableSet s} : Set (Set Ω))) i) (f i)),
    ∀ᵐ (a : α) ∂μ,
      Eq (α := ℝ≥0∞) ((((η : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ s, f i) : ℝ≥0∞)
        (∏ i ∈ s, (((η : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i) : ℝ≥0∞)
have inr₁ : ∀ (a : ι) (s : Finset ι),
  a ∉ s →
    (∀
        (_H :
          ∀ i ∈ s,
            Membership.mem (γ := Set (Set Ω)) ((fun (x : ι) ↦ ({s : Set Ω | MeasurableSet s} : Set (Set Ω))) i) (f i)),
        ∀ᵐ (a : α) ∂μ,
          Eq (α := ℝ≥0∞) ((((η : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ s, f i) : ℝ≥0∞)
            (∏ i ∈ s, (((η : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i) : ℝ≥0∞)) →
      ∀
        (_H :
          ∀ i ∈ insert a s,
            Membership.mem (γ := Set (Set Ω)) ((fun (x : ι) ↦ ({s : Set Ω | MeasurableSet s} : Set (Set Ω))) i) (f i)),
        ∀ᵐ (a_3 : α) ∂μ,
          Eq (α := ℝ≥0∞)
            ((((η : (a : α) → Measure Ω) a_3 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ insert a s, f i) : ℝ≥0∞)
            (∏ i ∈ insert a s, (((η : (a : α) → Measure Ω) a_3 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i) : ℝ≥0∞)
Tactic: refine Finset.induction ?_ ?_ s
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.Indep (hypothesis)
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
m : ι → MeasurableSpace Ω
h_le : ∀ (i : ι), m i ≤ _mΩ
π : ι → Set (Set Ω)
h_pi : ∀ (n : ι), IsPiSystem (π n)
h_generate : ∀ (i : ι), m i = generateFrom (π i)
h_ind : iIndepSets π κ μ
hμ : μ ≠ 0
η : Kernel α Ω
η_eq : Filter.EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μ) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω)
hη : IsMarkovKernel η
s : Finset ι
f : ι → Set Ω
a : ι
S : Finset ι
ha_notin_S : a ∉ S
h_rec :
  ∀
    (_H :
      ∀ i ∈ S,
        Membership.mem (γ := Set (Set Ω)) ((fun (x : ι) ↦ ({s : Set Ω | MeasurableSet s} : Set (Set Ω))) i) (f i)),
    ∀ᵐ (a : α) ∂μ,
      Eq (α := ℝ≥0∞) ((((η : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ S, f i) : ℝ≥0∞)
        (∏ i ∈ S, (((η : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i) : ℝ≥0∞)
hf_m :
  ∀ i ∈ insert a S,
    Membership.mem (γ := Set (Set Ω)) ((fun (x : ι) ↦ ({s : Set Ω | MeasurableSet s} : Set (Set Ω))) i) (f i)
⊢ ∀ᵐ (a_1 : α) ∂μ,
    Eq (α := ℝ≥0∞) ((((η : (a : α) → Measure Ω) a_1 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ insert a S, f i) : ℝ≥0∞)
      (∏ i ∈ insert a S, (((η : (a : α) → Measure Ω) a_1 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i) : ℝ≥0∞)
have hf_m_S : ∀ x ∈ S, MeasurableSet (f x)
Tactic: have hf_m_S : ∀ x ∈ S, MeasurableSet[m x] (f x) := fun x hx => hf_m x (by simp [hx])
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.Indep (hypothesis)
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
m : ι → MeasurableSpace Ω
h_le : ∀ (i : ι), m i ≤ _mΩ
π : ι → Set (Set Ω)
h_pi : ∀ (n : ι), IsPiSystem (π n)
h_generate : ∀ (i : ι), m i = generateFrom (π i)
h_ind : iIndepSets π κ μ
hμ : μ ≠ 0
η : Kernel α Ω
η_eq : Filter.EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μ) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω)
hη : IsMarkovKernel η
s : Finset ι
f : ι → Set Ω
a : ι
S : Finset ι
ha_notin_S : a ∉ S
h_rec :
  ∀
    (_H :
      ∀ i ∈ S,
        Membership.mem (γ := Set (Set Ω)) ((fun (x : ι) ↦ ({s : Set Ω | MeasurableSet s} : Set (Set Ω))) i) (f i)),
    ∀ᵐ (a : α) ∂μ,
      Eq (α := ℝ≥0∞) ((((η : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ S, f i) : ℝ≥0∞)
        (∏ i ∈ S, (((η : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i) : ℝ≥0∞)
hf_m :
  ∀ i ∈ insert a S,
    Membership.mem (γ := Set (Set Ω)) ((fun (x : ι) ↦ ({s : Set Ω | MeasurableSet s} : Set (Set Ω))) i) (f i)
hf_m_S : ∀ x ∈ S, MeasurableSet (f x)
p : Set (Set Ω) := piiUnionInter π (↑S : Set ι)
⊢ ∀ᵐ (a_1 : α) ∂μ,
    Eq (α := ℝ≥0∞) ((((η : (a : α) → Measure Ω) a_1 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ insert a S, f i) : ℝ≥0∞)
      (∏ i ∈ insert a S, (((η : (a : α) → Measure Ω) a_1 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i) : ℝ≥0∞)
have hS_eq_generate : let m_p := generateFrom p;
m_p = generateFrom p
Tactic: set m_p := generateFrom p with hS_eq_generate
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.Indep (hypothesis)
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
m : ι → MeasurableSpace Ω
h_le : ∀ (i : ι), m i ≤ _mΩ
π : ι → Set (Set Ω)
h_pi : ∀ (n : ι), IsPiSystem (π n)
h_generate : ∀ (i : ι), m i = generateFrom (π i)
h_ind : iIndepSets π κ μ
hμ : μ ≠ 0
η : Kernel α Ω
η_eq : Filter.EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μ) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω)
hη : IsMarkovKernel η
s : Finset ι
f : ι → Set Ω
a : ι
S : Finset ι
ha_notin_S : a ∉ S
h_rec :
  ∀
    (_H :
      ∀ i ∈ S,
        Membership.mem (γ := Set (Set Ω)) ((fun (x : ι) ↦ ({s : Set Ω | MeasurableSet s} : Set (Set Ω))) i) (f i)),
    ∀ᵐ (a : α) ∂μ,
      Eq (α := ℝ≥0∞) ((((η : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ S, f i) : ℝ≥0∞)
        (∏ i ∈ S, (((η : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i) : ℝ≥0∞)
hf_m :
  ∀ i ∈ insert a S,
    Membership.mem (γ := Set (Set Ω)) ((fun (x : ι) ↦ ({s : Set Ω | MeasurableSet s} : Set (Set Ω))) i) (f i)
hf_m_S : ∀ x ∈ S, MeasurableSet (f x)
p : Set (Set Ω) := piiUnionInter π (↑S : Set ι)
m_p : MeasurableSpace Ω := generateFrom p
hS_eq_generate : m_p = generateFrom p
⊢ Indep m_p (m a) η μ
have hp : IsPiSystem p
Tactic: have hp : IsPiSystem p := isPiSystem_piiUnionInter π h_pi S