awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Independence.Kernel.Indep
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∞)
inr₁ : Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} (⋂ n ∈ S, f n)
⊢ ∀ᵐ (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)) ?_
-- Module: Mathlib.Probability.Independence.Kernel.Indep
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∞)
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∞)
⊢ ∀ᵐ (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:
filter_upwards [h_rec hf_m_S, h] with a' ha' h'
-- Module: Mathlib.Probability.Independence.Kernel.Indep
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
rw : generateFrom (π n) ≤ generateFrom p
⊢ m n ≤ m_p

Tactic:
rw [hS_eq_generate, h_generate n]
-- Module: Mathlib.Probability.Independence.Kernel.Indep
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
⊢ generateFrom (π n) ≤ generateFrom p

Tactic:
le_generateFrom_piiUnionInter (S : Set ι) hn

Premises used: le_generateFrom_piiUnionInter, SetLike.coe
-- Module: Mathlib.Probability.Independence.Kernel.Indep
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
⊢ generateFrom (π n) ≤ generateFrom p

Tactic:
exact le_generateFrom_piiUnionInter (S : Set ι) hn

Premises used: le_generateFrom_piiUnionInter, SetLike.coe
-- Module: Mathlib.Probability.Independence.Kernel.Indep
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) η μ
⊢ ∀ 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
-- Module: Mathlib.Probability.Independence.Kernel.Indep
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
⊢ ∀ 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)
-- Module: Mathlib.Probability.Independence.Kernel.Indep
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
h_S_f : ∀ i ∈ S, MeasurableSet (f i)
⊢ Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} (⋂ n ∈ S, f n)

Tactic:
S.measurableSet_biInter h_S_f

Premises used: MeasurableSet, Set.Mem, setOf, Finset.measurableSet_biInter
-- Module: Mathlib.Probability.Independence.Kernel.Indep
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
h_S_f : ∀ i ∈ S, MeasurableSet (f i)
⊢ Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} (⋂ n ∈ S, f n)

Tactic:
exact S.measurableSet_biInter h_S_f

Premises used: Finset.measurableSet_biInter
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
f : ι → Set Ω
hf : ∀ (i : ι), MeasurableSet (f i)
i : ι
⊢ MeasurableSet (f i)

Tactic:
hf _
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
f : ι → Set Ω
hf : ∀ (i : ι), MeasurableSet (f i)
i : ι
⊢ MeasurableSet (f i)

Tactic:
exact hf _
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
f : ι → Set Ω
h : iIndepSet f κ μ
s : Finset ι
⊢ ∀ i ∈ s, Membership.mem (γ := Set (Set Ω)) {f i} (f i)

Tactic:
simp
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
f : ι → Set Ω
hf : ∀ (i : ι), MeasurableSet (f i)
⊢ iIndepSet f κ μ ↔
    ∀ (s : Finset ι),
      ∀ᵐ (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∞)

Tactic:
(iIndepSet_iff_iIndepSets_singleton hf).trans iIndepSets_singleton_iff

Premises used: Iff.trans, ProbabilityTheory.Kernel.iIndepSets_singleton_iff, ProbabilityTheory.Kernel.iIndepSet_iff_iIndepSets_singleton
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
f : ι → Set Ω
hfπ : ∀ (i : ι), f i ∈ π i
hf : ∀ (i : ι), MeasurableSet (f i)
hπ : iIndepSets π κ μ
⊢ iIndepSet f κ μ

Tactic:
(iIndepSet_iff_meas_biInter hf).2 fun _t ↦ hπ.meas_biInter _ fun _i _ ↦ hfπ _

Premises used: Iff.mpr, ProbabilityTheory.Kernel.iIndepSet_iff_meas_biInter, ProbabilityTheory.Kernel.iIndepSets.meas_biInter
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
s t : Set Ω
m0 : MeasurableSpace Ω
hs_meas : MeasurableSet s
ht_meas : MeasurableSet t
κ : Kernel α Ω
μ : Measure α
inst : IsZeroOrMarkovKernel κ
h : IndepSets {s} {t} κ μ
u : Set Ω
hu : Membership.mem (γ := Set (Set Ω)) {s} u
rwa rwa₁ rwa₂ rwa₃ : MeasurableSet s
⊢ MeasurableSet u

Tactic:
rwa [Set.mem_singleton_iff.mp hu]

Premises used: Set.mem_singleton_iff, Iff.mp
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
s t : Set Ω
m0 : MeasurableSpace Ω
hs_meas : MeasurableSet s
ht_meas : MeasurableSet t
κ : Kernel α Ω
μ : Measure α
inst : IsZeroOrMarkovKernel κ
h : IndepSets {s} {t} κ μ
u : Set Ω
hu : Membership.mem (γ := Set (Set Ω)) {t} u
rwa rwa₁ rwa₂ rwa₃ : MeasurableSet t
⊢ MeasurableSet u

Tactic:
rwa [Set.mem_singleton_iff.mp hu]

Premises used: Set.mem_singleton_iff, Iff.mp
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
s t : Set Ω
_m0 : MeasurableSpace Ω
hs_meas : MeasurableSet s
ht_meas : MeasurableSet t
κ : Kernel α Ω
μ : Measure α
inst : IsZeroOrMarkovKernel κ
⊢ IndepSet s t κ μ ↔
    ∀ᵐ (a : α) ∂μ,
      (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s ∩ t) =
        HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
          ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
(indepSet_iff_indepSets_singleton hs_meas ht_meas κ μ).trans indepSets_singleton_iff

Premises used: Iff.trans, ProbabilityTheory.Kernel.indepSet_iff_indepSets_singleton, ProbabilityTheory.Kernel.indepSets_singleton_iff
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
s t : Set Ω
_m0 : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h : IndepSet s t κ μ
⊢ Membership.mem (γ := Set (Set Ω)) {s} s

Tactic:
simp
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
s t : Set Ω
_m0 : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h : IndepSet s t κ μ
⊢ Membership.mem (γ := Set (Set Ω)) {t} t

Tactic:
simp
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
s t : Set Ω
S T : Set (Set Ω)
_m0 : MeasurableSpace Ω
hs : s ∈ S
ht : t ∈ T
hs_meas : MeasurableSet s
ht_meas : MeasurableSet t
κ : Kernel α Ω
μ : Measure α
inst : IsZeroOrMarkovKernel κ
h_indep : IndepSets S T κ μ
⊢ IndepSet s t κ μ

Tactic:
(indepSet_iff_measure_inter_eq_mul hs_meas ht_meas κ μ).mpr (h_indep s t hs ht)

Premises used: Iff.mpr, ProbabilityTheory.Kernel.indepSet_iff_measure_inter_eq_mul
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m₁ m₂ x : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h_indep : Indep m₁ m₂ κ μ
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
⊢ IndepSet s t κ μ

Tactic:
fun s' t' hs' ht' => h_indep s' t' ?_ ?_

Premises used: ProbabilityTheory.Kernel.Indep, ProbabilityTheory.Kernel.IndepSets, ProbabilityTheory.Kernel.IndepSet
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m₁ m₂ x : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h_indep : Indep m₁ m₂ κ μ
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
refine_1 :
  ∀ (s' t' : Set Ω) (hs' : Membership.mem (γ := Set (Set Ω)) {s_1 : Set Ω | MeasurableSet s_1} s')
    (ht' : Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} t'),
    Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} s'
refine_2 :
  ∀ (s' t' : Set Ω) (hs' : Membership.mem (γ := Set (Set Ω)) {s_1 : Set Ω | MeasurableSet s_1} s')
    (ht' : Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} t'),
    Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} t'
⊢ IndepSet s t κ μ

Tactic:
refine fun s' t' hs' ht' => h_indep s' t' ?_ ?_
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m₁ m₂ x : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h_indep : Indep m₁ m₂ κ μ
s t_1 : Set Ω
hs : MeasurableSet s
ht_1 : MeasurableSet t_1
s' t' : Set Ω
ht' : Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} t'
t : Set Ω
ht : Membership.mem (γ := Set (Set Ω)) {s} t
ht_2 : MeasurableSet t
⊢ Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} t

Tactic:
ht ▸ hs

Premises used: Eq.rec, Eq.symm
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m₁ m₂ x : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h_indep : Indep m₁ m₂ κ μ
s t_1 : Set Ω
hs : MeasurableSet s
ht_1 : MeasurableSet t_1
s' t' : Set Ω
ht' : Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} t'
t : Set Ω
ht : Membership.mem (γ := Set (Set Ω)) {s} t
ht_2 : MeasurableSet t
⊢ Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} t

Tactic:
exact ht ▸ hs
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m₁ m₂ x : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h_indep : Indep m₁ m₂ κ μ
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
s' t' : Set Ω
ht' : Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} t'
⊢ Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} ∅

Tactic:
@MeasurableSet.empty _ m₁

Premises used: MeasurableSet, MeasurableSet.empty, Set.Mem, setOf
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m₁ m₂ x : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h_indep : Indep m₁ m₂ κ μ
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
s' t' : Set Ω
ht' : Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} t'
⊢ Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} ∅

Tactic:
exact @MeasurableSet.empty _ m₁

Premises used: MeasurableSet.empty
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m₁ m₂ x : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h_indep : Indep m₁ m₂ κ μ
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
s' t' : Set Ω
ht' : Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} t'
u : Set Ω
ht_1 : MeasurableSet u
hu : Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} u
⊢ Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} uᶜ

Tactic:
hu.compl

Premises used: MeasurableSet, Set.Mem, setOf, MeasurableSet.compl