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 α
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: classical
  rcases eq_or_ne μ 0 with rfl | hμ
  · simp
  obtain ⟨η, η_eq, hη⟩ : ∃ (η : Kernel α Ω), κ =ᵐ[μ] η ∧ IsMarkovKernel η :=
    exists_ae_eq_isMarkovKernel h_ind.ae_isProbabilityMeasure hμ
  apply iIndep.congr (Filter.EventuallyEq.symm η_eq)
  intro s f
  refine Finset.induction ?_ ?_ s
  · simp
  · intro a S ha_notin_S h_rec hf_m
    have hf_m_S : ∀ x ∈ S, MeasurableSet[m x] (f x) := fun x hx => hf_m x (by simp [hx])
    let p := piiUnionInter π S
    set m_p := generateFrom p with hS_eq_generate
    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)
    have h := h_indep.symm (f a) (⋂ n ∈ S, f n) (hf_m a (Finset.mem_insert_self a S)) ?_
    · filter_upwards [h_rec hf_m_S, h] with a' ha' h'
      rwa [Finset.set_biInter_insert, Finset.prod_insert ha_notin_S, ← ha']
    · 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
      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)
      exact S.measurableSet_biInter h_S_f
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: classical
  rcases eq_or_ne μ 0 with rfl | hμ
  · simp
  obtain ⟨η, η_eq, hη⟩ : ∃ (η : Kernel α Ω), κ =ᵐ[μ] η ∧ IsMarkovKernel η :=
    exists_ae_eq_isMarkovKernel h_ind.ae_isProbabilityMeasure hμ
  apply iIndep.congr (Filter.EventuallyEq.symm η_eq)
  intro s f
  refine Finset.induction ?_ ?_ s
  · simp
  · intro a S ha_notin_S h_rec hf_m
    have hf_m_S : ∀ x ∈ S, MeasurableSet[m x] (f x) := fun x hx => hf_m x (by simp [hx])
    let p := piiUnionInter π S
    set m_p := generateFrom p with hS_eq_generate
    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)
    have h := h_indep.symm (f a) (⋂ n ∈ S, f n) (hf_m a (Finset.mem_insert_self a S)) ?_
    · filter_upwards [h_rec hf_m_S, h] with a' ha' h'
      rwa [Finset.set_biInter_insert, Finset.prod_insert ha_notin_S, ← ha']
    · 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
      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)
      exact S.measurableSet_biInter h_S_f
-- 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
inr inr₁ : ∀ (hμ : μ ≠ 0), Kernel.iIndep m κ μ
⊢ Kernel.iIndep m κ μ
have inr₂ : ∀ (hμ : μ ≠ 0) (η : Kernel α Ω)
  (η_eq : Filter.EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μ) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω))
  (hη : IsMarkovKernel η), Kernel.iIndep m κ μ
Tactic: classical
  rcases eq_or_ne μ 0 with rfl | hμ
  · simp
  obtain ⟨η, η_eq, hη⟩ : ∃ (η : Kernel α Ω), κ =ᵐ[μ] η ∧ IsMarkovKernel η :=
    exists_ae_eq_isMarkovKernel h_ind.ae_isProbabilityMeasure hμ
  apply iIndep.congr (Filter.EventuallyEq.symm η_eq)
  intro s f
  refine Finset.induction ?_ ?_ s
  · simp
  · intro a S ha_notin_S h_rec hf_m
    have hf_m_S : ∀ x ∈ S, MeasurableSet[m x] (f x) := fun x hx => hf_m x (by simp [hx])
    let p := piiUnionInter π S
    set m_p := generateFrom p with hS_eq_generate
    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)
    have h := h_indep.symm (f a) (⋂ n ∈ S, f n) (hf_m a (Finset.mem_insert_self a S)) ?_
    · filter_upwards [h_rec hf_m_S, h] with a' ha' h'
      rwa [Finset.set_biInter_insert, Finset.prod_insert ha_notin_S, ← ha']
    · 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
      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)
      exact S.measurableSet_biInter h_S_f
-- 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
inr inr₁ : ∀ (hμ : μ ≠ 0), Kernel.iIndep m κ μ
inr₂ :
  ∀ (hμ : μ ≠ 0) (η : Kernel α Ω)
    (η_eq :
      Filter.EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μ) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω))
    (hη : IsMarkovKernel η), Kernel.iIndep m κ μ
⊢ Kernel.iIndep m κ μ
have inr₃ : ∀ (hμ : μ ≠ 0) (η : Kernel α Ω)
  (η_eq : Filter.EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μ) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω))
  (hη : IsMarkovKernel η), Kernel.iIndep m η μ
Tactic: classical
  rcases eq_or_ne μ 0 with rfl | hμ
  · simp
  obtain ⟨η, η_eq, hη⟩ : ∃ (η : Kernel α Ω), κ =ᵐ[μ] η ∧ IsMarkovKernel η :=
    exists_ae_eq_isMarkovKernel h_ind.ae_isProbabilityMeasure hμ
  apply iIndep.congr (Filter.EventuallyEq.symm η_eq)
  intro s f
  refine Finset.induction ?_ ?_ s
  · simp
  · intro a S ha_notin_S h_rec hf_m
    have hf_m_S : ∀ x ∈ S, MeasurableSet[m x] (f x) := fun x hx => hf_m x (by simp [hx])
    let p := piiUnionInter π S
    set m_p := generateFrom p with hS_eq_generate
    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)
    have h := h_indep.symm (f a) (⋂ n ∈ S, f n) (hf_m a (Finset.mem_insert_self a S)) ?_
    · filter_upwards [h_rec hf_m_S, h] with a' ha' h'
      rwa [Finset.set_biInter_insert, Finset.prod_insert ha_notin_S, ← ha']
    · 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
      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)
      exact S.measurableSet_biInter h_S_f
-- 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
inr inr₁ : ∀ (hμ : μ ≠ 0), Kernel.iIndep m κ μ
inr₂ :
  ∀ (hμ : μ ≠ 0) (η : Kernel α Ω)
    (η_eq :
      Filter.EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μ) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω))
    (hη : IsMarkovKernel η), Kernel.iIndep m κ μ
inr₃ :
  ∀ (hμ : μ ≠ 0) (η : Kernel α Ω)
    (η_eq :
      Filter.EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μ) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω))
    (hη : IsMarkovKernel η), Kernel.iIndep m η μ
⊢ Kernel.iIndep m κ μ
have inr₄ : ∀ (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∞)
Tactic: classical
  rcases eq_or_ne μ 0 with rfl | hμ
  · simp
  obtain ⟨η, η_eq, hη⟩ : ∃ (η : Kernel α Ω), κ =ᵐ[μ] η ∧ IsMarkovKernel η :=
    exists_ae_eq_isMarkovKernel h_ind.ae_isProbabilityMeasure hμ
  apply iIndep.congr (Filter.EventuallyEq.symm η_eq)
  intro s f
  refine Finset.induction ?_ ?_ s
  · simp
  · intro a S ha_notin_S h_rec hf_m
    have hf_m_S : ∀ x ∈ S, MeasurableSet[m x] (f x) := fun x hx => hf_m x (by simp [hx])
    let p := piiUnionInter π S
    set m_p := generateFrom p with hS_eq_generate
    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)
    have h := h_indep.symm (f a) (⋂ n ∈ S, f n) (hf_m a (Finset.mem_insert_self a S)) ?_
    · filter_upwards [h_rec hf_m_S, h] with a' ha' h'
      rwa [Finset.set_biInter_insert, Finset.prod_insert ha_notin_S, ← ha']
    · 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
      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)
      exact S.measurableSet_biInter h_S_f
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.Indep (goal)
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 κ μ
have 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'
Tactic: refine fun s' t' hs' ht' => h_indep s' t' ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.Indep (goal)
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'
⊢ IndepSet s t κ μ
have 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'
Tactic: refine fun s' t' hs' ht' => h_indep s' t' ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.Indep (goal)
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 Ω
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'
have refine_1 : ∀ (t : Set Ω) (ht : Membership.mem (γ := Set (Set Ω)) {s} t),
  MeasurableSet t → Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} t
Tactic: induction s', hs' using generateFrom_induction with
    | hC t ht => exact ht ▸ hs
    | empty => exact @MeasurableSet.empty _ m₁
    | compl u _ hu => exact hu.compl
    | iUnion f _ hf => exact .iUnion hf
Cleared hypotheses: hs'
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.Indep (goal)
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 Ω
hs' : Membership.mem (γ := Set (Set Ω)) {s_1 : Set Ω | MeasurableSet s_1} s'
ht' : Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} t'
refine_1 :
  ∀ (t : Set Ω) (ht : Membership.mem (γ := Set (Set Ω)) {s} t),
    MeasurableSet t → Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} t
⊢ Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} s'
have refine_1₁ : Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} ∅
Tactic: induction s', hs' using generateFrom_induction with
    | hC t ht => exact ht ▸ hs
    | empty => exact @MeasurableSet.empty _ m₁
    | compl u _ hu => exact hu.compl
    | iUnion f _ hf => exact .iUnion hf
Cleared hypotheses: hs'
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.Indep (goal)
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 Ω
hs' : Membership.mem (γ := Set (Set Ω)) {s_1 : Set Ω | MeasurableSet s_1} s'
ht' : Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} t'
refine_1 :
  ∀ (t : Set Ω) (ht : Membership.mem (γ := Set (Set Ω)) {s} t),
    MeasurableSet t → Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} t
refine_1₁ : Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} ∅
⊢ Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} s'
have refine_1₂ : ∀ (u : Set Ω),
  MeasurableSet u →
    ∀ (hu : Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} u),
      Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} uᶜ
Tactic: induction s', hs' using generateFrom_induction with
    | hC t ht => exact ht ▸ hs
    | empty => exact @MeasurableSet.empty _ m₁
    | compl u _ hu => exact hu.compl
    | iUnion f _ hf => exact .iUnion hf
Cleared hypotheses: hs'
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.Indep (goal)
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 Ω
hs' : Membership.mem (γ := Set (Set Ω)) {s_1 : Set Ω | MeasurableSet s_1} s'
ht' : Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} t'
refine_1 :
  ∀ (t : Set Ω) (ht : Membership.mem (γ := Set (Set Ω)) {s} t),
    MeasurableSet t → Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} t
refine_1₁ : Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} ∅
refine_1₂ :
  ∀ (u : Set Ω),
    MeasurableSet u →
      ∀ (hu : Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} u),
        Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} uᶜ
⊢ Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} s'
have refine_1₃ : ∀ (f : ℕ → Set Ω),
  (∀ (n : ℕ), MeasurableSet (f n)) →
    ∀ (hf : ∀ (n : ℕ), Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} (f n)),
      Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} (⋃ (i : ℕ), f i)
Tactic: induction s', hs' using generateFrom_induction with
    | hC t ht => exact ht ▸ hs
    | empty => exact @MeasurableSet.empty _ m₁
    | compl u _ hu => exact hu.compl
    | iUnion f _ hf => exact .iUnion hf
Cleared hypotheses: hs'
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.Indep (goal)
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 Ω
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'
have refine_2 : ∀ (s : Set Ω) (hs : Membership.mem (γ := Set (Set Ω)) {t} s),
  MeasurableSet s → Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} s
Tactic: induction t', ht' using generateFrom_induction with
    | hC s hs => exact hs ▸ ht
    | empty => exact @MeasurableSet.empty _ m₂
    | compl u _ hu => exact hu.compl
    | iUnion f _ hf => exact .iUnion hf
Cleared hypotheses: ht'
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.Indep (goal)
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 Ω
hs' : Membership.mem (γ := Set (Set Ω)) {s_1 : Set Ω | MeasurableSet s_1} s'
ht' : Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} t'
refine_2 :
  ∀ (s : Set Ω) (hs : Membership.mem (γ := Set (Set Ω)) {t} s),
    MeasurableSet s → Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} s
⊢ Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} t'
have refine_2₁ : Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} ∅
Tactic: induction t', ht' using generateFrom_induction with
    | hC s hs => exact hs ▸ ht
    | empty => exact @MeasurableSet.empty _ m₂
    | compl u _ hu => exact hu.compl
    | iUnion f _ hf => exact .iUnion hf
Cleared hypotheses: ht'
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.Indep (goal)
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 Ω
hs' : Membership.mem (γ := Set (Set Ω)) {s_1 : Set Ω | MeasurableSet s_1} s'
ht' : Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} t'
refine_2 :
  ∀ (s : Set Ω) (hs : Membership.mem (γ := Set (Set Ω)) {t} s),
    MeasurableSet s → Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} s
refine_2₁ : Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} ∅
⊢ Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} t'
have refine_2₂ : ∀ (u : Set Ω),
  MeasurableSet u →
    ∀ (hu : Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} u),
      Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} uᶜ
Tactic: induction t', ht' using generateFrom_induction with
    | hC s hs => exact hs ▸ ht
    | empty => exact @MeasurableSet.empty _ m₂
    | compl u _ hu => exact hu.compl
    | iUnion f _ hf => exact .iUnion hf
Cleared hypotheses: ht'
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.Indep (goal)
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 Ω
hs' : Membership.mem (γ := Set (Set Ω)) {s_1 : Set Ω | MeasurableSet s_1} s'
ht' : Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} t'
refine_2 :
  ∀ (s : Set Ω) (hs : Membership.mem (γ := Set (Set Ω)) {t} s),
    MeasurableSet s → Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} s
refine_2₁ : Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} ∅
refine_2₂ :
  ∀ (u : Set Ω),
    MeasurableSet u →
      ∀ (hu : Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} u),
        Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} uᶜ
⊢ Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} t'
have refine_2₃ : ∀ (f : ℕ → Set Ω),
  (∀ (n : ℕ), MeasurableSet (f n)) →
    ∀ (hf : ∀ (n : ℕ), Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} (f n)),
      Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} (⋃ (i : ℕ), f i)
Tactic: induction t', ht' using generateFrom_induction with
    | hC s hs => exact hs ▸ ht
    | empty => exact @MeasurableSet.empty _ m₂
    | compl u _ hu => exact hu.compl
    | iUnion f _ hf => exact .iUnion hf
Cleared hypotheses: ht'
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.IndepFun (goal)
Goal:
α : Type u_1
Ω : Type u_2
β : Type u_4
β' : Type u_5
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
⊢ IndepFun f g κ μ ↔
    ∀ (s : Set β) (t : Set β'),
      MeasurableSet s →
        MeasurableSet t →
          ∀ᵐ (a : α) ∂μ,
            (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s ∩ g ⁻¹' t) =
              HMul.hMul (α := ENNReal) (β := ENNReal)
                ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s) : ENNReal)
                ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (g ⁻¹' t) : ENNReal)
have mp : IndepFun f g κ μ →
  ∀ (s : Set β) (t : Set β'),
    MeasurableSet s →
      MeasurableSet t →
        ∀ᵐ (a : α) ∂μ,
          (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s ∩ g ⁻¹' t) =
            HMul.hMul (α := ENNReal) (β := ENNReal)
              ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s) : ENNReal)
              ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (g ⁻¹' t) : ENNReal)
Tactic: constructor