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Ω
h_indep : iIndep m κ μ
S T : Set ι
hST : Disjoint S T
⊢ Indep (⨆ i ∈ S, m i) (⨆ i ∈ T, m i) κ μ
have inl : ∀ (h_indep : iIndep m κ 0), Indep (⨆ i ∈ S, m i) (⨆ i ∈ T, m i) κ 0
Tactic: classical
  rcases eq_or_ne μ 0 with rfl | hμ
  · simp
  obtain ⟨η, η_eq, hη⟩ : ∃ (η : Kernel α Ω), κ =ᵐ[μ] η ∧ IsMarkovKernel η :=
    exists_ae_eq_isMarkovKernel h_indep.ae_isProbabilityMeasure hμ
  apply Indep.congr (Filter.EventuallyEq.symm η_eq)
  refine
    IndepSets.indep (iSup₂_le fun i _ => h_le i) (iSup₂_le fun i _ => h_le i) ?_ ?_
      (generateFrom_piiUnionInter_measurableSet m S).symm
      (generateFrom_piiUnionInter_measurableSet m T).symm ?_
  · exact isPiSystem_piiUnionInter _ (fun n => @isPiSystem_measurableSet Ω (m n)) _
  · exact isPiSystem_piiUnionInter _ (fun n => @isPiSystem_measurableSet Ω (m n)) _
  · exact indepSets_piiUnionInter_of_disjoint (h_indep.congr η_eq) hST
Cleared hypotheses: μ, h_indep
-- 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Ω
h_indep : iIndep m κ μ
S T : Set ι
hST : Disjoint S T
inl : ∀ (h_indep : iIndep m κ 0), Indep (⨆ i ∈ S, m i) (⨆ i ∈ T, m i) κ 0
⊢ Indep (⨆ i ∈ S, m i) (⨆ i ∈ T, m i) κ μ
have inr : ∀ (hμ : μ ≠ 0), Indep (⨆ i ∈ S, m i) (⨆ i ∈ T, m i) κ μ
Tactic: classical
  rcases eq_or_ne μ 0 with rfl | hμ
  · simp
  obtain ⟨η, η_eq, hη⟩ : ∃ (η : Kernel α Ω), κ =ᵐ[μ] η ∧ IsMarkovKernel η :=
    exists_ae_eq_isMarkovKernel h_indep.ae_isProbabilityMeasure hμ
  apply Indep.congr (Filter.EventuallyEq.symm η_eq)
  refine
    IndepSets.indep (iSup₂_le fun i _ => h_le i) (iSup₂_le fun i _ => h_le i) ?_ ?_
      (generateFrom_piiUnionInter_measurableSet m S).symm
      (generateFrom_piiUnionInter_measurableSet m T).symm ?_
  · exact isPiSystem_piiUnionInter _ (fun n => @isPiSystem_measurableSet Ω (m n)) _
  · exact isPiSystem_piiUnionInter _ (fun n => @isPiSystem_measurableSet Ω (m n)) _
  · exact indepSets_piiUnionInter_of_disjoint (h_indep.congr η_eq) hST
-- 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Ω
h_indep : iIndep m κ μ
S T : Set ι
hST : Disjoint S T
inl : ∀ (h_indep : iIndep m κ 0), Indep (⨆ i ∈ S, m i) (⨆ i ∈ T, m i) κ 0
inr inr₁ : ∀ (hμ : μ ≠ 0), Indep (⨆ i ∈ S, m i) (⨆ i ∈ T, m i) κ μ
⊢ Indep (⨆ i ∈ S, m i) (⨆ i ∈ T, m i) κ μ
have inr₂ : ∀ (hμ : μ ≠ 0) (η : Kernel α Ω)
  (η_eq : Filter.EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μ) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω))
  (hη : IsMarkovKernel η), Indep (⨆ i ∈ S, m i) (⨆ i ∈ T, m i) κ μ
Tactic: classical
  rcases eq_or_ne μ 0 with rfl | hμ
  · simp
  obtain ⟨η, η_eq, hη⟩ : ∃ (η : Kernel α Ω), κ =ᵐ[μ] η ∧ IsMarkovKernel η :=
    exists_ae_eq_isMarkovKernel h_indep.ae_isProbabilityMeasure hμ
  apply Indep.congr (Filter.EventuallyEq.symm η_eq)
  refine
    IndepSets.indep (iSup₂_le fun i _ => h_le i) (iSup₂_le fun i _ => h_le i) ?_ ?_
      (generateFrom_piiUnionInter_measurableSet m S).symm
      (generateFrom_piiUnionInter_measurableSet m T).symm ?_
  · exact isPiSystem_piiUnionInter _ (fun n => @isPiSystem_measurableSet Ω (m n)) _
  · exact isPiSystem_piiUnionInter _ (fun n => @isPiSystem_measurableSet Ω (m n)) _
  · exact indepSets_piiUnionInter_of_disjoint (h_indep.congr η_eq) hST
-- 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Ω
h_indep : iIndep m κ μ
S T : Set ι
hST : Disjoint S T
inl : ∀ (h_indep : iIndep m κ 0), Indep (⨆ i ∈ S, m i) (⨆ i ∈ T, m i) κ 0
inr inr₁ : ∀ (hμ : μ ≠ 0), Indep (⨆ i ∈ S, m i) (⨆ i ∈ T, m i) κ μ
inr₂ :
  ∀ (hμ : μ ≠ 0) (η : Kernel α Ω)
    (η_eq :
      Filter.EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μ) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω))
    (hη : IsMarkovKernel η), Indep (⨆ i ∈ S, m i) (⨆ i ∈ T, m i) κ μ
⊢ Indep (⨆ i ∈ S, m i) (⨆ i ∈ T, m i) κ μ
have inr₃ : ∀ (hμ : μ ≠ 0) (η : Kernel α Ω)
  (η_eq : Filter.EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μ) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω))
  (hη : IsMarkovKernel η), Indep (⨆ i ∈ S, m i) (⨆ i ∈ T, m i) η μ
Tactic: classical
  rcases eq_or_ne μ 0 with rfl | hμ
  · simp
  obtain ⟨η, η_eq, hη⟩ : ∃ (η : Kernel α Ω), κ =ᵐ[μ] η ∧ IsMarkovKernel η :=
    exists_ae_eq_isMarkovKernel h_indep.ae_isProbabilityMeasure hμ
  apply Indep.congr (Filter.EventuallyEq.symm η_eq)
  refine
    IndepSets.indep (iSup₂_le fun i _ => h_le i) (iSup₂_le fun i _ => h_le i) ?_ ?_
      (generateFrom_piiUnionInter_measurableSet m S).symm
      (generateFrom_piiUnionInter_measurableSet m T).symm ?_
  · exact isPiSystem_piiUnionInter _ (fun n => @isPiSystem_measurableSet Ω (m n)) _
  · exact isPiSystem_piiUnionInter _ (fun n => @isPiSystem_measurableSet Ω (m n)) _
  · exact indepSets_piiUnionInter_of_disjoint (h_indep.congr η_eq) hST
-- 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Ω
h_indep : iIndep m κ μ
S T : Set ι
hST : Disjoint S T
inl : ∀ (h_indep : iIndep m κ 0), Indep (⨆ i ∈ S, m i) (⨆ i ∈ T, m i) κ 0
inr inr₁ : ∀ (hμ : μ ≠ 0), Indep (⨆ i ∈ S, m i) (⨆ i ∈ T, m i) κ μ
inr₂ :
  ∀ (hμ : μ ≠ 0) (η : Kernel α Ω)
    (η_eq :
      Filter.EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μ) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω))
    (hη : IsMarkovKernel η), Indep (⨆ i ∈ S, m i) (⨆ i ∈ T, m i) κ μ
inr₃ :
  ∀ (hμ : μ ≠ 0) (η : Kernel α Ω)
    (η_eq :
      Filter.EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μ) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω))
    (hη : IsMarkovKernel η), Indep (⨆ i ∈ S, m i) (⨆ i ∈ T, m i) η μ
⊢ Indep (⨆ i ∈ S, m i) (⨆ i ∈ T, m i) κ μ
have inr₄ : ∀ (hμ : μ ≠ 0) (η : Kernel α Ω)
  (η_eq : Filter.EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μ) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω))
  (hη : IsMarkovKernel η), IsPiSystem.{u_2} (α := Ω) (piiUnionInter (fun (n : ι) ↦ {s : Set Ω | MeasurableSet s}) S)
Tactic: classical
  rcases eq_or_ne μ 0 with rfl | hμ
  · simp
  obtain ⟨η, η_eq, hη⟩ : ∃ (η : Kernel α Ω), κ =ᵐ[μ] η ∧ IsMarkovKernel η :=
    exists_ae_eq_isMarkovKernel h_indep.ae_isProbabilityMeasure hμ
  apply Indep.congr (Filter.EventuallyEq.symm η_eq)
  refine
    IndepSets.indep (iSup₂_le fun i _ => h_le i) (iSup₂_le fun i _ => h_le i) ?_ ?_
      (generateFrom_piiUnionInter_measurableSet m S).symm
      (generateFrom_piiUnionInter_measurableSet m T).symm ?_
  · exact isPiSystem_piiUnionInter _ (fun n => @isPiSystem_measurableSet Ω (m n)) _
  · exact isPiSystem_piiUnionInter _ (fun n => @isPiSystem_measurableSet Ω (m n)) _
  · exact indepSets_piiUnionInter_of_disjoint (h_indep.congr η_eq) hST
-- 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Ω
h_indep : iIndep m κ μ
S T : Set ι
hST : Disjoint S T
inl : ∀ (h_indep : iIndep m κ 0), Indep (⨆ i ∈ S, m i) (⨆ i ∈ T, m i) κ 0
inr inr₁ : ∀ (hμ : μ ≠ 0), Indep (⨆ i ∈ S, m i) (⨆ i ∈ T, m i) κ μ
inr₂ :
  ∀ (hμ : μ ≠ 0) (η : Kernel α Ω)
    (η_eq :
      Filter.EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μ) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω))
    (hη : IsMarkovKernel η), Indep (⨆ i ∈ S, m i) (⨆ i ∈ T, m i) κ μ
inr₃ :
  ∀ (hμ : μ ≠ 0) (η : Kernel α Ω)
    (η_eq :
      Filter.EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μ) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω))
    (hη : IsMarkovKernel η), Indep (⨆ i ∈ S, m i) (⨆ i ∈ T, m i) η μ
inr₄ :
  ∀ (hμ : μ ≠ 0) (η : Kernel α Ω)
    (η_eq :
      Filter.EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μ) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω))
    (hη : IsMarkovKernel η), IsPiSystem.{u_2} (α := Ω) (piiUnionInter (fun (n : ι) ↦ {s : Set Ω | MeasurableSet s}) S)
⊢ Indep (⨆ i ∈ S, m i) (⨆ i ∈ T, m i) κ μ
have inr₅ : ∀ (hμ : μ ≠ 0) (η : Kernel α Ω)
  (η_eq : Filter.EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μ) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω))
  (hη : IsMarkovKernel η), IsPiSystem.{u_2} (α := Ω) (piiUnionInter (fun (n : ι) ↦ {s : Set Ω | MeasurableSet s}) T)
Tactic: classical
  rcases eq_or_ne μ 0 with rfl | hμ
  · simp
  obtain ⟨η, η_eq, hη⟩ : ∃ (η : Kernel α Ω), κ =ᵐ[μ] η ∧ IsMarkovKernel η :=
    exists_ae_eq_isMarkovKernel h_indep.ae_isProbabilityMeasure hμ
  apply Indep.congr (Filter.EventuallyEq.symm η_eq)
  refine
    IndepSets.indep (iSup₂_le fun i _ => h_le i) (iSup₂_le fun i _ => h_le i) ?_ ?_
      (generateFrom_piiUnionInter_measurableSet m S).symm
      (generateFrom_piiUnionInter_measurableSet m T).symm ?_
  · exact isPiSystem_piiUnionInter _ (fun n => @isPiSystem_measurableSet Ω (m n)) _
  · exact isPiSystem_piiUnionInter _ (fun n => @isPiSystem_measurableSet Ω (m n)) _
  · exact indepSets_piiUnionInter_of_disjoint (h_indep.congr η_eq) hST
-- 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Ω
h_indep : iIndep m κ μ
S T : Set ι
hST : Disjoint S T
inl : ∀ (h_indep : iIndep m κ 0), Indep (⨆ i ∈ S, m i) (⨆ i ∈ T, m i) κ 0
inr inr₁ : ∀ (hμ : μ ≠ 0), Indep (⨆ i ∈ S, m i) (⨆ i ∈ T, m i) κ μ
inr₂ :
  ∀ (hμ : μ ≠ 0) (η : Kernel α Ω)
    (η_eq :
      Filter.EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μ) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω))
    (hη : IsMarkovKernel η), Indep (⨆ i ∈ S, m i) (⨆ i ∈ T, m i) κ μ
inr₃ :
  ∀ (hμ : μ ≠ 0) (η : Kernel α Ω)
    (η_eq :
      Filter.EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μ) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω))
    (hη : IsMarkovKernel η), Indep (⨆ i ∈ S, m i) (⨆ i ∈ T, m i) η μ
inr₄ :
  ∀ (hμ : μ ≠ 0) (η : Kernel α Ω)
    (η_eq :
      Filter.EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μ) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω))
    (hη : IsMarkovKernel η), IsPiSystem.{u_2} (α := Ω) (piiUnionInter (fun (n : ι) ↦ {s : Set Ω | MeasurableSet s}) S)
inr₅ :
  ∀ (hμ : μ ≠ 0) (η : Kernel α Ω)
    (η_eq :
      Filter.EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μ) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω))
    (hη : IsMarkovKernel η), IsPiSystem.{u_2} (α := Ω) (piiUnionInter (fun (n : ι) ↦ {s : Set Ω | MeasurableSet s}) T)
⊢ Indep (⨆ i ∈ S, m i) (⨆ i ∈ T, m i) κ μ
have inr₆ : ∀ (hμ : μ ≠ 0) (η : Kernel α Ω)
  (η_eq : Filter.EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μ) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω))
  (hη : IsMarkovKernel η),
  IndepSets (piiUnionInter (fun (n : ι) ↦ {s : Set Ω | MeasurableSet s}) S)
    (piiUnionInter (fun (n : ι) ↦ {s : Set Ω | MeasurableSet s}) T) η μ
Tactic: classical
  rcases eq_or_ne μ 0 with rfl | hμ
  · simp
  obtain ⟨η, η_eq, hη⟩ : ∃ (η : Kernel α Ω), κ =ᵐ[μ] η ∧ IsMarkovKernel η :=
    exists_ae_eq_isMarkovKernel h_indep.ae_isProbabilityMeasure hμ
  apply Indep.congr (Filter.EventuallyEq.symm η_eq)
  refine
    IndepSets.indep (iSup₂_le fun i _ => h_le i) (iSup₂_le fun i _ => h_le i) ?_ ?_
      (generateFrom_piiUnionInter_measurableSet m S).symm
      (generateFrom_piiUnionInter_measurableSet m T).symm ?_
  · exact isPiSystem_piiUnionInter _ (fun n => @isPiSystem_measurableSet Ω (m n)) _
  · exact isPiSystem_piiUnionInter _ (fun n => @isPiSystem_measurableSet Ω (m n)) _
  · exact indepSets_piiUnionInter_of_disjoint (h_indep.congr η_eq) hST
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.Indep (hypothesis)
Goal:
α : Type u_1
ι : Type u_3
_mα : MeasurableSpace α
Ω : Type u_4
m : ι → MeasurableSpace Ω
m' m0 : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst : IsZeroOrMarkovKernel κ
h_indep : ∀ (i : ι), Indep (m i) m' κ μ
h_le : ∀ (i : ι), m i ≤ m0
h_le' : m' ≤ m0
hm : Directed (fun (x1 x2 : MeasurableSpace Ω) ↦ x1 ≤ x2) m
p : ι → Set (Set Ω) := fun (n : ι) ↦ {t : Set Ω | MeasurableSet t}
⊢ Indep (⨆ (i : ι), m i) m' κ μ
have hp : ∀ (n : ι), IsPiSystem (p n)
Tactic: have hp : ∀ n, IsPiSystem (p n) := fun n => @isPiSystem_measurableSet Ω (m n)
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.Indep (hypothesis)
Goal:
α : Type u_1
ι : Type u_3
_mα : MeasurableSpace α
Ω : Type u_4
m : ι → MeasurableSpace Ω
m' m0 : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst : IsZeroOrMarkovKernel κ
h_indep : ∀ (i : ι), Indep (m i) m' κ μ
h_le : ∀ (i : ι), m i ≤ m0
h_le' : m' ≤ m0
hm : Directed (fun (x1 x2 : MeasurableSpace Ω) ↦ x1 ≤ x2) m
p : ι → Set (Set Ω) := fun (n : ι) ↦ {t : Set Ω | MeasurableSet t}
hp : ∀ (n : ι), IsPiSystem (p n)
⊢ Indep (⨆ (i : ι), m i) m' κ μ
have h_gen_n : ∀ (n : ι), m n = generateFrom (p n)
Tactic: have h_gen_n : ∀ n, m n = generateFrom (p n) := fun n =>
    (@generateFrom_measurableSet Ω (m n)).symm
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.Indep (hypothesis)
Goal:
α : Type u_1
ι : Type u_3
_mα : MeasurableSpace α
Ω : Type u_4
m : ι → MeasurableSpace Ω
m' m0 : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst : IsZeroOrMarkovKernel κ
h_indep : ∀ (i : ι), Indep (m i) m' κ μ
h_le : ∀ (i : ι), m i ≤ m0
h_le' : m' ≤ m0
hm : Directed (fun (x1 x2 : MeasurableSpace Ω) ↦ x1 ≤ x2) m
p : ι → Set (Set Ω) := fun (n : ι) ↦ {t : Set Ω | MeasurableSet t}
hp : ∀ (n : ι), IsPiSystem (p n)
h_gen_n : ∀ (n : ι), m n = generateFrom (p n)
⊢ Indep (⨆ (i : ι), m i) m' κ μ
have hp_supr_pi : IsPiSystem.{u_4} (α := Ω) (⋃ (n : ι), p n)
Tactic: have hp_supr_pi : IsPiSystem (⋃ n, p n) := isPiSystem_iUnion_of_directed_le p hp hm
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.Indep (hypothesis)
Goal:
α : Type u_1
ι : Type u_3
_mα : MeasurableSpace α
Ω : Type u_4
m : ι → MeasurableSpace Ω
m' m0 : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst : IsZeroOrMarkovKernel κ
h_indep : ∀ (i : ι), Indep (m i) m' κ μ
h_le : ∀ (i : ι), m i ≤ m0
h_le' : m' ≤ m0
hm : Directed (fun (x1 x2 : MeasurableSpace Ω) ↦ x1 ≤ x2) m
p : ι → Set (Set Ω) := fun (n : ι) ↦ {t : Set Ω | MeasurableSet t}
hp : ∀ (n : ι), IsPiSystem (p n)
h_gen_n : ∀ (n : ι), m n = generateFrom (p n)
hp_supr_pi : IsPiSystem.{u_4} (α := Ω) (⋃ (n : ι), p n)
p' : Set (Set Ω) := {t : Set Ω | MeasurableSet t}
⊢ Indep (⨆ (i : ι), m i) m' κ μ
have hp'_pi : IsPiSystem p'
Tactic: have hp'_pi : IsPiSystem p' := @isPiSystem_measurableSet Ω m'
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.Indep (hypothesis)
Goal:
α : Type u_1
ι : Type u_3
_mα : MeasurableSpace α
Ω : Type u_4
m : ι → MeasurableSpace Ω
m' m0 : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst : IsZeroOrMarkovKernel κ
h_indep : ∀ (i : ι), Indep (m i) m' κ μ
h_le : ∀ (i : ι), m i ≤ m0
h_le' : m' ≤ m0
hm : Directed (fun (x1 x2 : MeasurableSpace Ω) ↦ x1 ≤ x2) m
p : ι → Set (Set Ω) := fun (n : ι) ↦ {t : Set Ω | MeasurableSet t}
hp : ∀ (n : ι), IsPiSystem (p n)
h_gen_n : ∀ (n : ι), m n = generateFrom (p n)
hp_supr_pi : IsPiSystem.{u_4} (α := Ω) (⋃ (n : ι), p n)
p' : Set (Set Ω) := {t : Set Ω | MeasurableSet t}
hp'_pi : IsPiSystem p'
⊢ Indep (⨆ (i : ι), m i) m' κ μ
have h_gen' : m' = generateFrom p'
Tactic: have h_gen' : m' = generateFrom p' := (@generateFrom_measurableSet Ω m').symm
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.Indep (goal)
Goal:
α : Type u_1
ι : Type u_3
_mα : MeasurableSpace α
Ω : Type u_4
m : ι → MeasurableSpace Ω
m' m0 : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst : IsZeroOrMarkovKernel κ
h_indep : ∀ (i : ι), Indep (m i) m' κ μ
h_le : ∀ (i : ι), m i ≤ m0
h_le' : m' ≤ m0
hm : Directed (fun (x1 x2 : MeasurableSpace Ω) ↦ x1 ≤ x2) m
p : ι → Set (Set Ω) := fun (n : ι) ↦ {t : Set Ω | MeasurableSet t}
hp : ∀ (n : ι), IsPiSystem (p n)
h_gen_n : ∀ (n : ι), m n = generateFrom (p n)
hp_supr_pi : IsPiSystem.{u_4} (α := Ω) (⋃ (n : ι), p n)
p' : Set (Set Ω) := {t : Set Ω | MeasurableSet t}
hp'_pi : IsPiSystem p'
h_gen' : m' = generateFrom p'
⊢ IndepSets (⋃ (n : ι), p n) p' κ μ
have refine : ∀ (n : ι), IndepSets (p n) p' κ μ
Tactic: refine IndepSets.iUnion ?_
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.Indep (goal)
Goal:
α : Type u_1
ι : Type u_3
_mα : MeasurableSpace α
Ω : Type u_4
m : ι → MeasurableSpace Ω
m' m0 : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst : IsZeroOrMarkovKernel κ
h_indep : ∀ (i : ι), Indep (m i) m' κ μ
h_le : ∀ (i : ι), m i ≤ m0
h_le' : m' ≤ m0
hm : Directed (fun (x1 x2 : MeasurableSpace Ω) ↦ x1 ≤ x2) m
p : ι → Set (Set Ω) := fun (n : ι) ↦ {t : Set Ω | MeasurableSet t}
hp : ∀ (n : ι), IsPiSystem (p n)
h_gen_n : ∀ (n : ι), m n = generateFrom (p n)
hp_supr_pi : IsPiSystem.{u_4} (α := Ω) (⋃ (n : ι), p n)
p' : Set (Set Ω) := {t : Set Ω | MeasurableSet t}
hp'_pi : IsPiSystem p'
h_gen' : m' = generateFrom p'
i : ι
| Indep (m i) m' κ μ
have rw : Indep (generateFrom (p i)) (generateFrom p') κ μ
Tactic: rw [h_gen_n i, h_gen']
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.Indep (hypothesis)
Goal:
α : Type u_1
ι : Type u_3
_mα : MeasurableSpace α
Ω : Type u_4
m : ι → MeasurableSpace Ω
m' m0 : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst : IsZeroOrMarkovKernel κ
h_indep : ∀ (i : ι), Indep (m i) m' κ μ
h_le : ∀ (i : ι), m i ≤ m0
h_le' : m' ≤ m0
hm : Directed (fun (x1 x2 : MeasurableSpace Ω) ↦ x1 ≤ x2) m
p : ι → Set (Set Ω) := fun (n : ι) ↦ {t : Set Ω | MeasurableSet t}
hp : ∀ (n : ι), IsPiSystem (p n)
h_gen_n : ∀ (n : ι), m n = generateFrom (p n)
hp_supr_pi : IsPiSystem.{u_4} (α := Ω) (⋃ (n : ι), p n)
p' : Set (Set Ω) := {t : Set Ω | MeasurableSet t}
hp'_pi : IsPiSystem p'
h_gen' : m' = generateFrom p'
⊢ ∀ (n : ι), IndepSets (p n) p' κ μ
have h_indep₁ : ∀ (i : ι), Indep (generateFrom (p i)) (generateFrom p') κ μ
Tactic: conv at h_indep =>
      intro i
      rw [h_gen_n i, h_gen']
Cleared hypotheses: h_indep, hp'_pi, h_gen'
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.Indep (hypothesis)
Goal:
α : Type u_1
ι : Type u_3
_mα : MeasurableSpace α
Ω : Type u_4
m : ι → MeasurableSpace Ω
m' m0 : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst : IsZeroOrMarkovKernel κ
h_indep : ∀ (i : ι), Indep (m i) m' κ μ
h_le : ∀ (i : ι), m i ≤ m0
h_le' : m' ≤ m0
hm : Directed (fun (x1 x2 : MeasurableSpace Ω) ↦ x1 ≤ x2) m
p : ι → Set (Set Ω) := fun (n : ι) ↦ {t : Set Ω | MeasurableSet t}
hp : ∀ (n : ι), IsPiSystem (p n)
h_gen_n : ∀ (n : ι), m n = generateFrom (p n)
hp_supr_pi : IsPiSystem.{u_4} (α := Ω) (⋃ (n : ι), p n)
p' : Set (Set Ω) := {t : Set Ω | MeasurableSet t}
hp'_pi : IsPiSystem p'
h_gen' : m' = generateFrom p'
⊢ Indep (⨆ (i : ι), m i) m' κ μ
have h_pi_system_indep : IndepSets (⋃ (n : ι), p n) p' κ μ
Tactic: have h_pi_system_indep : IndepSets (⋃ n, p n) p' κ μ := by
    refine IndepSets.iUnion ?_
    conv at h_indep =>
      intro i
      rw [h_gen_n i, h_gen']
    exact fun n => (h_indep n).indepSets
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.Indep (goal)
Goal:
α : Type u_1
ι : Type u_3
_mα : MeasurableSpace α
Ω : Type u_4
m : ι → MeasurableSpace Ω
m' m0 : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst : IsZeroOrMarkovKernel κ
h_indep : ∀ (i : ι), Indep (m i) m' κ μ
h_le : ∀ (i : ι), m i ≤ m0
h_le' : m' ≤ m0
hm : Directed (fun (x1 x2 : MeasurableSpace Ω) ↦ x1 ≤ x2) m
p : ι → Set (Set Ω) := fun (n : ι) ↦ {t : Set Ω | MeasurableSet t}
hp : ∀ (n : ι), IsPiSystem (p n)
h_gen_n : ∀ (n : ι), m n = generateFrom (p n)
hp_supr_pi : IsPiSystem.{u_4} (α := Ω) (⋃ (n : ι), p n)
p' : Set (Set Ω) := {t : Set Ω | MeasurableSet t}
hp'_pi : IsPiSystem p'
h_gen' : m' = generateFrom p'
h_pi_system_indep : IndepSets (⋃ (n : ι), p n) p' κ μ
⊢ Indep (⨆ (i : ι), m i) m' κ μ
have refine : Eq.{u_4 + 1} (α := MeasurableSpace Ω) (⨆ (i : ι), m i) (generateFrom (⋃ (n : ι), p n))
Tactic: refine IndepSets.indep (iSup_le h_le) h_le' hp_supr_pi hp'_pi ?_ h_gen' h_pi_system_indep
-- 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 α
inst : Preorder ι
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iIndepSet s κ μ
i : ι
⊢ Indep (generateFrom {s i}) (generateFrom {t : Set Ω | ∃ j < i, s j = t}) κ μ
have h : Eq (α := MeasurableSpace Ω) (generateFrom {s i})
  (generateFrom {t : Set Ω | ∃ (n : ι), Membership.mem (γ := Set ι) {i} n ∧ s n = t})
Tactic: convert!
    iIndepSet.indep_generateFrom_of_disjoint hsm hs { i } {j | j < i}
      (Set.disjoint_singleton_left.mpr (lt_irrefl _)) using 1
-- 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 α
inst : Preorder ι
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iIndepSet s κ μ
i k : ι
hk : i < k
⊢ Indep (generateFrom {s k}) (generateFrom {t : Set Ω | ∃ j ≤ i, s j = t}) κ μ
have h : Eq (α := MeasurableSpace Ω) (generateFrom {s k})
  (generateFrom {t : Set Ω | ∃ (n : ι), Membership.mem (γ := Set ι) {k} n ∧ s n = t})
Tactic: convert!
    iIndepSet.indep_generateFrom_of_disjoint hsm hs { k } {j | j ≤ i}
      (Set.disjoint_singleton_left.mpr hk.not_ge) using 1
-- 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 : Set ι) ⊆ (↑S : Set ι)
ft1 : ι → Set Ω
hft1_mem : ∀ x ∈ s, ft1 x ∈ π x
ht1_eq : t1 = ⋂ x ∈ s, ft1 x
ht2_mem_pia : t2 ∈ π a
⊢ ∀ᵐ (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 rw : ∀ (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),
  ∀ᵐ (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: rw [Finset.coe_subset] at hs_mem
Cleared hypotheses: hs_mem, ft1, hft1_mem, ht1_eq, ht2_mem_pia
-- 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
n : ι
hn_mem_insert : n ∈ insert a s
⊢ (if n = a then t2 else if n ∈ s then ft1 n else univ) ∈ π n
have inl : ∀ (hn_mem : n = a), (if n = a then t2 else if n ∈ s then ft1 n else univ) ∈ π n
Tactic: rcases Finset.mem_insert.mp hn_mem_insert with hn_mem | hn_mem