awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
hp : IsPiSystem p
⊢ Indep m_p (m a) η μ
have h_le' : ∀ (i : ι), generateFrom (π i) ≤ _mΩ
Tactic: have h_le' : ∀ i, generateFrom (π i) ≤ _mΩ := fun i ↦ (h_generate i).symm.trans_le (h_le i)
-- 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
hp : IsPiSystem p
h_le' : ∀ (i : ι), generateFrom (π i) ≤ _mΩ
⊢ Indep m_p (m a) η μ
have hm_p : m_p ≤ _mΩ
Tactic: have hm_p : m_p ≤ _mΩ := generateFrom_piiUnionInter_le π h_le' 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)
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
⊢ ∀ᵐ (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 h_indep : Indep m_p (m a) η μ
Tactic: have h_indep : Indep m_p (m a) η μ := by
      have hp : IsPiSystem p := isPiSystem_piiUnionInter π h_pi S
      have h_le' : ∀ i, generateFrom (π i) ≤ _mΩ := fun i ↦ (h_generate i).symm.trans_le (h_le i)
      have hm_p : m_p ≤ _mΩ := generateFrom_piiUnionInter_le π h_le' S
      exact IndepSets.indep hm_p (h_le a) hp (h_pi a) hS_eq_generate (h_generate a)
        (iIndepSets.piiUnionInter_of_notMem (h_ind.congr η_eq) ha_notin_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 Ω
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
h_indep : Indep m_p (m a) η μ
⊢ ∀ᵐ (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 inr : ∀
  (h :
    ∀ᵐ (a_1 : α) ∂μ,
      (((η : (a : α) → Measure Ω) a_1 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f a ∩ ⋂ n ∈ S, f n) =
        HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞)
          ((((η : (a : α) → Measure Ω) a_1 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f a) : ℝ≥0∞)
          ((((η : (a : α) → Measure Ω) a_1 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ n ∈ S, f n) : ℝ≥0∞)),
  ∀ᵐ (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∞)
Tactic: have h := h_indep.symm (f a) (⋂ n ∈ S, f n) (hf_m a (Finset.mem_insert_self a 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 Ω
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
h_indep : Indep m_p (m a) η μ
inr :
  ∀
    (h :
      ∀ᵐ (a_1 : α) ∂μ,
        (((η : (a : α) → Measure Ω) a_1 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f a ∩ ⋂ n ∈ S, f n) =
          HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞)
            ((((η : (a : α) → Measure Ω) a_1 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f a) : ℝ≥0∞)
            ((((η : (a : α) → Measure Ω) a_1 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ n ∈ S, f n) : ℝ≥0∞)),
    ∀ᵐ (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∞)
⊢ ∀ᵐ (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 inr₁ : Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} (⋂ n ∈ S, f n)
Tactic: have h := h_indep.symm (f a) (⋂ n ∈ S, f n) (hf_m a (Finset.mem_insert_self a 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 Ω
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
h_indep : Indep m_p (m a) η μ
h :
  ∀ᵐ (a_1 : α) ∂μ,
    (((η : (a : α) → Measure Ω) a_1 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f a ∩ ⋂ n ∈ S, f n) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞)
        ((((η : (a : α) → Measure Ω) a_1 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f a) : ℝ≥0∞)
        ((((η : (a : α) → Measure Ω) a_1 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ n ∈ S, f n) : ℝ≥0∞)
⊢ ∀ᵐ (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 h₁ : ∀ (a' : α)
  (ha' :
    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' :
    (((η : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f a ∩ ⋂ n ∈ S, f n) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((η : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f a) : ℝ≥0∞)
        ((((η : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ n ∈ S, f n) : ℝ≥0∞)),
  Eq (α := ℝ≥0∞) ((((η : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ insert a S, f i) : ℝ≥0∞)
    (∏ i ∈ insert a S, (((η : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i) : ℝ≥0∞)
Tactic: filter_upwards [h_rec hf_m_S, h] with a' ha' 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 η
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
h_indep : Indep m_p (m a) η μ
h :
  ∀ᵐ (a_1 : α) ∂μ,
    (((η : (a : α) → Measure Ω) a_1 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f a ∩ ⋂ n ∈ S, f n) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞)
        ((((η : (a : α) → Measure Ω) a_1 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f a) : ℝ≥0∞)
        ((((η : (a : α) → Measure Ω) a_1 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ n ∈ S, f n) : ℝ≥0∞)
a' : α
ha' :
  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' :
  (((η : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f a ∩ ⋂ n ∈ S, f n) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((η : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f a) : ℝ≥0∞)
      ((((η : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ n ∈ S, f n) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((((η : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ insert a S, f i) : ℝ≥0∞)
    (∏ i ∈ insert a S, (((η : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i) : ℝ≥0∞)
have h₁ : Eq (α := ℝ≥0∞) ((((η : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f a ∩ ⋂ x ∈ S, f x) : ℝ≥0∞)
  (∏ i ∈ insert a S, (((η : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i) : ℝ≥0∞)
Tactic: rwa [Finset.set_biInter_insert, Finset.prod_insert ha_notin_S, ← ha']
-- 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 Ω
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
h_indep : Indep m_p (m a) η μ
h :
  ∀ᵐ (a_1 : α) ∂μ,
    (((η : (a : α) → Measure Ω) a_1 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f a ∩ ⋂ n ∈ S, f n) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞)
        ((((η : (a : α) → Measure Ω) a_1 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f a) : ℝ≥0∞)
        ((((η : (a : α) → Measure Ω) a_1 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ n ∈ S, f n) : ℝ≥0∞)
a' : α
ha' :
  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' :
  (((η : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f a ∩ ⋂ n ∈ S, f n) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((η : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f a) : ℝ≥0∞)
      ((((η : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ n ∈ S, f n) : ℝ≥0∞)
h₁ :
  Eq (α := ℝ≥0∞) ((((η : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f a ∩ ⋂ x ∈ S, f x) : ℝ≥0∞)
    (∏ i ∈ insert a S, (((η : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((((η : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ insert a S, f i) : ℝ≥0∞)
    (∏ i ∈ insert a S, (((η : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i) : ℝ≥0∞)
have h₂ : (((η : (a : α) → Measure Ω) a' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f a ∩ ⋂ x ∈ S, f x) =
  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∞)
Tactic: rwa [Finset.set_biInter_insert, Finset.prod_insert ha_notin_S, ← ha']
-- 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 Ω
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
h_indep : Indep m_p (m a) η μ
n : ι
hn : n ∈ S
⊢ m n ≤ m_p
have rw : generateFrom (π n) ≤ generateFrom p
Tactic: rw [hS_eq_generate, h_generate n]
-- 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
h_indep : Indep m_p (m a) η μ
⊢ Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} (⋂ n ∈ S, f n)
have h_le_p : ∀ i ∈ S, m i ≤ m_p
Tactic: have h_le_p : ∀ i ∈ S, m i ≤ m_p := by
        intro n hn
        rw [hS_eq_generate, h_generate n]
        exact le_generateFrom_piiUnionInter (S : Set ι) hn
-- 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
h_indep : Indep m_p (m a) η μ
h_le_p : ∀ i ∈ S, m i ≤ m_p
⊢ Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} (⋂ n ∈ S, f n)
have h_S_f : ∀ i ∈ S, MeasurableSet (f i)
Tactic: have h_S_f : ∀ i ∈ S, MeasurableSet[m_p] (f i) :=
        fun i hi ↦ (h_le_p i hi) (f i) (hf_m_S i hi)