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
_mα : MeasurableSpace α
m1 m2 m : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst : IsZeroOrMarkovKernel κ
p1 p2 : Set (Set Ω)
h1 : m1 ≤ m
h2 : m2 ≤ m
hp1 : IsPiSystem p1
hp2 : IsPiSystem p2
hpm1 : m1 = generateFrom p1
hpm2 : m2 = generateFrom p2
hyp : IndepSets p1 p2 κ μ
h : IsMarkovKernel κ
t1 t2 : Set Ω
ht1 : Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} t1
ht2 : Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} t2
⊢ ∀ᵐ (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 inr : ∀ᵐ (a : α) ∂μ,
  (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (∅ ∩ t2) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) ∅ : ℝ≥0∞)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)
Tactic: induction t1, ht1 using induction_on_inter hpm1 hp1 with
  | empty =>
    simp only [Set.empty_inter, measure_empty, zero_mul, Filter.eventually_true]
  | basic t ht =>
    refine IndepSets.indep_aux h2 hp2 hpm2 hyp ht (h1 _ ?_) ht2
    rw [hpm1]
    exact measurableSet_generateFrom ht
  | compl t ht iht =>
    filter_upwards [iht] with a ha
    have : tᶜ ∩ t2 = t2 \ (t ∩ t2) := by
      rw [Set.inter_comm t, Set.diff_self_inter, Set.diff_eq_compl_inter]
    rw [this, Set.inter_comm t t2,
      measure_diff Set.inter_subset_left ((h2 _ ht2).inter (h1 _ ht)).nullMeasurableSet
        (measure_ne_top (κ a) _),
      Set.inter_comm, ha, measure_compl (h1 _ ht) (measure_ne_top (κ a) t), measure_univ,
      mul_comm (1 - κ a t), ENNReal.mul_sub (fun _ _ ↦ measure_ne_top (κ a) _), mul_one, mul_comm]
  | iUnion f hf_disj hf_meas h =>
    rw [← ae_all_iff] at h
    filter_upwards [h] with a ha
    rw [Set.inter_comm, Set.inter_iUnion, measure_iUnion]
    · rw [measure_iUnion hf_disj (fun i ↦ h1 _ (hf_meas i))]
      rw [← ENNReal.tsum_mul_right]
      congr 1 with i
      rw [Set.inter_comm t2, ha i]
    · intro i j hij
      rw [Function.onFun, Set.inter_comm t2, Set.inter_comm t2]
      exact Disjoint.inter_left _ (Disjoint.inter_right _ (hf_disj hij))
    · exact fun i ↦ (h2 _ ht2).inter (h1 _ (hf_meas i))
Cleared hypotheses: ht1
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.Indep (goal)
Goal:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m1 m2 m : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst : IsZeroOrMarkovKernel κ
p1 p2 : Set (Set Ω)
h1 : m1 ≤ m
h2 : m2 ≤ m
hp1 : IsPiSystem p1
hp2 : IsPiSystem p2
hpm1 : m1 = generateFrom p1
hpm2 : m2 = generateFrom p2
hyp : IndepSets p1 p2 κ μ
h : IsMarkovKernel κ
t1 t2 : Set Ω
ht1 : Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} t1
ht2 : Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} t2
inr :
  ∀ᵐ (a : α) ∂μ,
    (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (∅ ∩ t2) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) ∅ : ℝ≥0∞)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)
⊢ ∀ᵐ (a : α) ∂μ,
    (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)
have inr₁ : ∀ (t : Set Ω) (ht : t ∈ p1),
  ∀ᵐ (a : α) ∂μ,
    (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t ∩ t2) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)
Tactic: induction t1, ht1 using induction_on_inter hpm1 hp1 with
  | empty =>
    simp only [Set.empty_inter, measure_empty, zero_mul, Filter.eventually_true]
  | basic t ht =>
    refine IndepSets.indep_aux h2 hp2 hpm2 hyp ht (h1 _ ?_) ht2
    rw [hpm1]
    exact measurableSet_generateFrom ht
  | compl t ht iht =>
    filter_upwards [iht] with a ha
    have : tᶜ ∩ t2 = t2 \ (t ∩ t2) := by
      rw [Set.inter_comm t, Set.diff_self_inter, Set.diff_eq_compl_inter]
    rw [this, Set.inter_comm t t2,
      measure_diff Set.inter_subset_left ((h2 _ ht2).inter (h1 _ ht)).nullMeasurableSet
        (measure_ne_top (κ a) _),
      Set.inter_comm, ha, measure_compl (h1 _ ht) (measure_ne_top (κ a) t), measure_univ,
      mul_comm (1 - κ a t), ENNReal.mul_sub (fun _ _ ↦ measure_ne_top (κ a) _), mul_one, mul_comm]
  | iUnion f hf_disj hf_meas h =>
    rw [← ae_all_iff] at h
    filter_upwards [h] with a ha
    rw [Set.inter_comm, Set.inter_iUnion, measure_iUnion]
    · rw [measure_iUnion hf_disj (fun i ↦ h1 _ (hf_meas i))]
      rw [← ENNReal.tsum_mul_right]
      congr 1 with i
      rw [Set.inter_comm t2, ha i]
    · intro i j hij
      rw [Function.onFun, Set.inter_comm t2, Set.inter_comm t2]
      exact Disjoint.inter_left _ (Disjoint.inter_right _ (hf_disj hij))
    · exact fun i ↦ (h2 _ ht2).inter (h1 _ (hf_meas i))
Cleared hypotheses: ht1
-- 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 α
s : ι → Set (Set Ω)
S T : Set ι
h_indep : iIndepSets s κ μ
hST : Disjoint S T
t1 t2 : Set Ω
p1 : Finset ι
hp1 : (↑p1 : Set ι) ⊆ S
f1 : ι → Set Ω
ht1_m : ∀ x ∈ p1, f1 x ∈ s x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
p2 : Finset ι
hp2 : (↑p2 : Set ι) ⊆ T
f2 : ι → Set Ω
ht2_m : ∀ x ∈ p2, f2 x ∈ s x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
g : (i : ι) → Set Ω := fun (i : ι) ↦ (if i ∈ p1 then f1 i else univ) ∩ if i ∈ p2 then f2 i else univ
i : ι
hi_mem_union : i ∈ p1 ∪ p2
⊢ g i ∈ s i
have hi_mem_union₁ : i ∈ p1 ∨ i ∈ p2
Tactic: rw [Finset.mem_union] at hi_mem_union
Cleared hypotheses: hi_mem_union
-- 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 α
s : ι → Set (Set Ω)
S T : Set ι
h_indep : iIndepSets s κ μ
hST : Disjoint S T
t1 t2 : Set Ω
p1 : Finset ι
hp1 : (↑p1 : Set ι) ⊆ S
f1 : ι → Set Ω
ht1_m : ∀ x ∈ p1, f1 x ∈ s x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
p2 : Finset ι
hp2 : (↑p2 : Set ι) ⊆ T
f2 : ι → Set Ω
ht2_m : ∀ x ∈ p2, f2 x ∈ s x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
g : (i : ι) → Set Ω := fun (i : ι) ↦ (if i ∈ p1 then f1 i else univ) ∩ if i ∈ p2 then f2 i else univ
i : ι
hi_mem_union : i ∈ p1 ∨ i ∈ p2
⊢ g i ∈ s i
have inl : ∀ (hi1 : i ∈ p1), g i ∈ s i
Tactic: rcases hi_mem_union with hi1 | hi2
Cleared hypotheses: hi_mem_union
-- 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 α
s : ι → Set (Set Ω)
S T : Set ι
h_indep : iIndepSets s κ μ
hST : Disjoint S T
t1 t2 : Set Ω
p1 : Finset ι
hp1 : (↑p1 : Set ι) ⊆ S
f1 : ι → Set Ω
ht1_m : ∀ x ∈ p1, f1 x ∈ s x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
p2 : Finset ι
hp2 : (↑p2 : Set ι) ⊆ T
f2 : ι → Set Ω
ht2_m : ∀ x ∈ p2, f2 x ∈ s x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
g : (i : ι) → Set Ω := fun (i : ι) ↦ (if i ∈ p1 then f1 i else univ) ∩ if i ∈ p2 then f2 i else univ
i : ι
hi_mem_union : i ∈ p1 ∨ i ∈ p2
inl : ∀ (hi1 : i ∈ p1), g i ∈ s i
⊢ g i ∈ s i
have inr : ∀ (hi2 : i ∈ p2), g i ∈ s i
Tactic: rcases hi_mem_union with hi1 | hi2
Cleared hypotheses: hi_mem_union
-- 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 α
s : ι → Set (Set Ω)
S T : Set ι
h_indep : iIndepSets s κ μ
hST : Disjoint S T
t1 t2 : Set Ω
p1 : Finset ι
hp1 : (↑p1 : Set ι) ⊆ S
f1 : ι → Set Ω
ht1_m : ∀ x ∈ p1, f1 x ∈ s x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
p2 : Finset ι
hp2 : (↑p2 : Set ι) ⊆ T
f2 : ι → Set Ω
ht2_m : ∀ x ∈ p2, f2 x ∈ s x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
g : (i : ι) → Set Ω := fun (i : ι) ↦ (if i ∈ p1 then f1 i else univ) ∩ if i ∈ p2 then f2 i else univ
i : ι
hi1 : i ∈ p1
⊢ g i ∈ s i
have hi2 : i ∉ p2
Tactic: have hi2 : i ∉ p2 := fun hip2 => Set.disjoint_left.mp hST (hp1 hi1) (hp2 hip2)
-- 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 α
s : ι → Set (Set Ω)
S T : Set ι
h_indep : iIndepSets s κ μ
hST : Disjoint S T
t1 t2 : Set Ω
p1 : Finset ι
hp1 : (↑p1 : Set ι) ⊆ S
f1 : ι → Set Ω
ht1_m : ∀ x ∈ p1, f1 x ∈ s x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
p2 : Finset ι
hp2 : (↑p2 : Set ι) ⊆ T
f2 : ι → Set Ω
ht2_m : ∀ x ∈ p2, f2 x ∈ s x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
g : (i : ι) → Set Ω := fun (i : ι) ↦ (if i ∈ p1 then f1 i else univ) ∩ if i ∈ p2 then f2 i else univ
i : ι
hi1 : i ∈ p1
hi2 : i ∉ p2
⊢ g i ∈ s i
have inl : f1 i ∈ s i
Tactic: simp_rw [g, if_pos hi1, if_neg hi2, Set.inter_univ]
-- 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 α
s : ι → Set (Set Ω)
S T : Set ι
h_indep : iIndepSets s κ μ
hST : Disjoint S T
t1 t2 : Set Ω
p1 : Finset ι
hp1 : (↑p1 : Set ι) ⊆ S
f1 : ι → Set Ω
ht1_m : ∀ x ∈ p1, f1 x ∈ s x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
p2 : Finset ι
hp2 : (↑p2 : Set ι) ⊆ T
f2 : ι → Set Ω
ht2_m : ∀ x ∈ p2, f2 x ∈ s x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
g : (i : ι) → Set Ω := fun (i : ι) ↦ (if i ∈ p1 then f1 i else univ) ∩ if i ∈ p2 then f2 i else univ
i : ι
hi2 : i ∈ p2
⊢ g i ∈ s i
have hi1 : i ∉ p1
Tactic: have hi1 : i ∉ p1 := fun hip1 => Set.disjoint_right.mp hST (hp2 hi2) (hp1 hip1)
-- 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 α
s : ι → Set (Set Ω)
S T : Set ι
h_indep : iIndepSets s κ μ
hST : Disjoint S T
t1 t2 : Set Ω
p1 : Finset ι
hp1 : (↑p1 : Set ι) ⊆ S
f1 : ι → Set Ω
ht1_m : ∀ x ∈ p1, f1 x ∈ s x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
p2 : Finset ι
hp2 : (↑p2 : Set ι) ⊆ T
f2 : ι → Set Ω
ht2_m : ∀ x ∈ p2, f2 x ∈ s x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
g : (i : ι) → Set Ω := fun (i : ι) ↦ (if i ∈ p1 then f1 i else univ) ∩ if i ∈ p2 then f2 i else univ
i : ι
hi2 : i ∈ p2
hi1 : i ∉ p1
⊢ g i ∈ s i
have inr : f2 i ∈ s i
Tactic: simp_rw [g, if_neg hi1, if_pos hi2, Set.univ_inter]
-- 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 α
s : ι → Set (Set Ω)
S T : Set ι
h_indep : iIndepSets s κ μ
hST : Disjoint S T
t1 t2 : Set Ω
p1 : Finset ι
hp1 : (↑p1 : Set ι) ⊆ S
f1 : ι → Set Ω
ht1_m : ∀ x ∈ p1, f1 x ∈ s x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
p2 : Finset ι
hp2 : (↑p2 : Set ι) ⊆ T
f2 : ι → Set Ω
ht2_m : ∀ x ∈ p2, f2 x ∈ s x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
g : (i : ι) → Set Ω := fun (i : ι) ↦ (if i ∈ p1 then f1 i else univ) ∩ if i ∈ p2 then f2 i else univ
⊢ ∀ᵐ (a : α) ∂μ,
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) : ℝ≥0∞)
      (∏ n ∈ p1 ∪ p2, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (g n) : ℝ≥0∞)
have hgm : ∀ i ∈ p1 ∪ p2, g i ∈ s i
Tactic: have hgm : ∀ i ∈ p1 ∪ p2, g i ∈ s i := by
      intro i hi_mem_union
      rw [Finset.mem_union] at hi_mem_union
      rcases hi_mem_union with hi1 | hi2
      · have hi2 : i ∉ p2 := fun hip2 => Set.disjoint_left.mp hST (hp1 hi1) (hp2 hip2)
        simp_rw [g, if_pos hi1, if_neg hi2, Set.inter_univ]
        exact ht1_m i hi1
      · have hi1 : i ∉ p1 := fun hip1 => Set.disjoint_right.mp hST (hp2 hi2) (hp1 hip1)
        simp_rw [g, if_neg hi1, if_pos hi2, Set.univ_inter]
        exact ht2_m i hi2
-- 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 α
s : ι → Set (Set Ω)
S T : Set ι
h_indep : iIndepSets s κ μ
hST : Disjoint S T
t1 t2 : Set Ω
p1 : Finset ι
hp1 : (↑p1 : Set ι) ⊆ S
f1 : ι → Set Ω
ht1_m : ∀ x ∈ p1, f1 x ∈ s x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
p2 : Finset ι
hp2 : (↑p2 : Set ι) ⊆ T
f2 : ι → Set Ω
ht2_m : ∀ x ∈ p2, f2 x ∈ s x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
g : (i : ι) → Set Ω := fun (i : ι) ↦ (if i ∈ p1 then f1 i else univ) ∩ if i ∈ p2 then f2 i else univ
hgm : ∀ i ∈ p1 ∪ p2, g i ∈ s i
⊢ Eq.{u_2 + 1} (α := Set Ω) ((⋂ x ∈ p1, f1 x) ∩ ⋂ x ∈ p2, f2 x)
    (⋂ i ∈ p1 ∪ p2, (if i ∈ p1 then f1 i else univ) ∩ if i ∈ p2 then f2 i else univ)
have h : ∀ (x : Ω),
  Membership.mem (γ := Set Ω) ((⋂ x ∈ p1, f1 x) ∩ ⋂ x ∈ p2, f2 x) x ↔
    Membership.mem (γ := Set Ω) (⋂ i ∈ p1 ∪ p2, (if i ∈ p1 then f1 i else univ) ∩ if i ∈ p2 then f2 i else univ) x
Tactic: ext1 x
-- 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 α
s : ι → Set (Set Ω)
S T : Set ι
h_indep : iIndepSets s κ μ
hST : Disjoint S T
t1 t2 : Set Ω
p1 : Finset ι
hp1 : (↑p1 : Set ι) ⊆ S
f1 : ι → Set Ω
ht1_m : ∀ x ∈ p1, f1 x ∈ s x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
p2 : Finset ι
hp2 : (↑p2 : Set ι) ⊆ T
f2 : ι → Set Ω
ht2_m : ∀ x ∈ p2, f2 x ∈ s x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
g : (i : ι) → Set Ω := fun (i : ι) ↦ (if i ∈ p1 then f1 i else univ) ∩ if i ∈ p2 then f2 i else univ
hgm : ∀ i ∈ p1 ∪ p2, g i ∈ s i
x : Ω
⊢ Membership.mem (γ := Set Ω) ((⋂ x ∈ p1, f1 x) ∩ ⋂ x ∈ p2, f2 x) x ↔
    Membership.mem (γ := Set Ω) (⋂ i ∈ p1 ∪ p2, (if i ∈ p1 then f1 i else univ) ∩ if i ∈ p2 then f2 i else univ) x
have h : ((∀ (i : ι) (i_1 : i ∈ p1), x ∈ f1 i) ∧ ∀ (i : ι) (i_1 : i ∈ p2), x ∈ f2 i) ↔
  ∀ (i : ι) (i_1 : i ∈ p1 ∨ i ∈ p2), (i ∈ p1 → x ∈ f1 i) ∧ (i ∈ p2 → x ∈ f2 i)
Tactic: simp only [Set.mem_ite_univ_right, Set.mem_inter_iff, Set.mem_iInter, Finset.mem_union]
-- 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 α
s : ι → Set (Set Ω)
S T : Set ι
h_indep : iIndepSets s κ μ
hST : Disjoint S T
t1 t2 : Set Ω
p1 : Finset ι
hp1 : (↑p1 : Set ι) ⊆ S
f1 : ι → Set Ω
ht1_m : ∀ x ∈ p1, f1 x ∈ s x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
p2 : Finset ι
hp2 : (↑p2 : Set ι) ⊆ T
f2 : ι → Set Ω
ht2_m : ∀ x ∈ p2, f2 x ∈ s x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
g : (i : ι) → Set Ω := fun (i : ι) ↦ (if i ∈ p1 then f1 i else univ) ∩ if i ∈ p2 then f2 i else univ
hgm : ∀ i ∈ p1 ∪ p2, g i ∈ s i
⊢ ∀ᵐ (a : α) ∂μ,
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) : ℝ≥0∞)
      (∏ n ∈ p1 ∪ p2, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (g n) : ℝ≥0∞)
have h_p1_inter_p2 : Eq.{u_2 + 1} (α := Set Ω) ((⋂ x ∈ p1, f1 x) ∩ ⋂ x ∈ p2, f2 x)
  (⋂ i ∈ p1 ∪ p2, (if i ∈ p1 then f1 i else univ) ∩ if i ∈ p2 then f2 i else univ)
Tactic: have h_p1_inter_p2 :
      ((⋂ x ∈ p1, f1 x) ∩ ⋂ x ∈ p2, f2 x) =
        ⋂ i ∈ p1 ∪ p2, ite (i ∈ p1) (f1 i) Set.univ ∩ ite (i ∈ p2) (f2 i) Set.univ := by
      ext1 x
      simp only [Set.mem_ite_univ_right, Set.mem_inter_iff, Set.mem_iInter, Finset.mem_union]
      exact
        ⟨fun h i _ => ⟨h.1 i, h.2 i⟩, fun h =>
          ⟨fun i hi => (h i (Or.inl hi)).1 hi, fun i hi => (h i (Or.inr hi)).2 hi⟩⟩
-- 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 α
s : ι → Set (Set Ω)
S T : Set ι
h_indep : iIndepSets s κ μ
hST : Disjoint S T
t1 t2 : Set Ω
p1 : Finset ι
hp1 : (↑p1 : Set ι) ⊆ S
f1 : ι → Set Ω
ht1_m : ∀ x ∈ p1, f1 x ∈ s x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
p2 : Finset ι
hp2 : (↑p2 : Set ι) ⊆ T
f2 : ι → Set Ω
ht2_m : ∀ x ∈ p2, f2 x ∈ s x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
g : (i : ι) → Set Ω := fun (i : ι) ↦ (if i ∈ p1 then f1 i else univ) ∩ if i ∈ p2 then f2 i else univ
hgm : ∀ i ∈ p1 ∪ p2, g i ∈ s i
h_p1_inter_p2 :
  Eq.{u_2 + 1} (α := Set Ω) ((⋂ x ∈ p1, f1 x) ∩ ⋂ x ∈ p2, f2 x)
    (⋂ i ∈ p1 ∪ p2, (if i ∈ p1 then f1 i else univ) ∩ if i ∈ p2 then f2 i else univ)
⊢ ∀ᵐ (a : α) ∂μ,
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) : ℝ≥0∞)
      (∏ n ∈ p1 ∪ p2, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (g n) : ℝ≥0∞)
have h : ∀ (a : α)
  (ha :
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ p1 ∪ p2, g i) : ℝ≥0∞)
      (∏ i ∈ p1 ∪ p2, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (g i) : ℝ≥0∞)),
  Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) : ℝ≥0∞)
    (∏ n ∈ p1 ∪ p2, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (g n) : ℝ≥0∞)
Tactic: filter_upwards [h_indep _ hgm] with a 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 α
s : ι → Set (Set Ω)
S T : Set ι
h_indep : iIndepSets s κ μ
hST : Disjoint S T
t1 t2 : Set Ω
p1 : Finset ι
hp1 : (↑p1 : Set ι) ⊆ S
f1 : ι → Set Ω
ht1_m : ∀ x ∈ p1, f1 x ∈ s x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
p2 : Finset ι
hp2 : (↑p2 : Set ι) ⊆ T
f2 : ι → Set Ω
ht2_m : ∀ x ∈ p2, f2 x ∈ s x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
g : (i : ι) → Set Ω := fun (i : ι) ↦ (if i ∈ p1 then f1 i else univ) ∩ if i ∈ p2 then f2 i else univ
hgm : ∀ i ∈ p1 ∪ p2, g i ∈ s i
h_p1_inter_p2 :
  Eq.{u_2 + 1} (α := Set Ω) ((⋂ x ∈ p1, f1 x) ∩ ⋂ x ∈ p2, f2 x)
    (⋂ i ∈ p1 ∪ p2, (if i ∈ p1 then f1 i else univ) ∩ if i ∈ p2 then f2 i else univ)
a : α
ha :
  Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ p1 ∪ p2, g i) : ℝ≥0∞)
    (∏ i ∈ p1 ∪ p2, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (g i) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) : ℝ≥0∞)
    (∏ n ∈ p1 ∪ p2, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (g n) : ℝ≥0∞)
have h : Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) ((⋂ x ∈ p1, f1 x) ∩ t2) : ℝ≥0∞)
  (∏ n ∈ p1 ∪ p2, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (g n) : ℝ≥0∞)
Tactic: rw [ht1_eq, ht2_eq, h_p1_inter_p2, ← 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 α
s : ι → Set (Set Ω)
S T : Set ι
h_indep : iIndepSets s κ μ
hST : Disjoint S T
t1 t2 : Set Ω
p1 : Finset ι
hp1 : (↑p1 : Set ι) ⊆ S
f1 : ι → Set Ω
ht1_m : ∀ x ∈ p1, f1 x ∈ s x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
p2 : Finset ι
hp2 : (↑p2 : Set ι) ⊆ T
f2 : ι → Set Ω
ht2_m : ∀ x ∈ p2, f2 x ∈ s x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
g : (i : ι) → Set Ω := fun (i : ι) ↦ (if i ∈ p1 then f1 i else univ) ∩ if i ∈ p2 then f2 i else univ
hgm : ∀ i ∈ p1 ∪ p2, g i ∈ s i
h_p1_inter_p2 :
  Eq.{u_2 + 1} (α := Set Ω) ((⋂ x ∈ p1, f1 x) ∩ ⋂ x ∈ p2, f2 x)
    (⋂ i ∈ p1 ∪ p2, (if i ∈ p1 then f1 i else univ) ∩ if i ∈ p2 then f2 i else univ)
a : α
ha :
  Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ p1 ∪ p2, g i) : ℝ≥0∞)
    (∏ i ∈ p1 ∪ p2, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (g i) : ℝ≥0∞)
h :
  Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) ((⋂ x ∈ p1, f1 x) ∩ t2) : ℝ≥0∞)
    (∏ n ∈ p1 ∪ p2, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (g n) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) : ℝ≥0∞)
    (∏ n ∈ p1 ∪ p2, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (g n) : ℝ≥0∞)
have h₁ : Eq (α := ℝ≥0∞)
  ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) ((⋂ x ∈ p1, f1 x) ∩ ⋂ x ∈ p2, f2 x) : ℝ≥0∞)
  (∏ n ∈ p1 ∪ p2, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (g n) : ℝ≥0∞)
Tactic: rw [ht1_eq, ht2_eq, h_p1_inter_p2, ← 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 α
s : ι → Set (Set Ω)
S T : Set ι
h_indep : iIndepSets s κ μ
hST : Disjoint S T
t1 t2 : Set Ω
p1 : Finset ι
hp1 : (↑p1 : Set ι) ⊆ S
f1 : ι → Set Ω
ht1_m : ∀ x ∈ p1, f1 x ∈ s x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
p2 : Finset ι
hp2 : (↑p2 : Set ι) ⊆ T
f2 : ι → Set Ω
ht2_m : ∀ x ∈ p2, f2 x ∈ s x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
g : (i : ι) → Set Ω := fun (i : ι) ↦ (if i ∈ p1 then f1 i else univ) ∩ if i ∈ p2 then f2 i else univ
hgm : ∀ i ∈ p1 ∪ p2, g i ∈ s i
h_p1_inter_p2 :
  Eq.{u_2 + 1} (α := Set Ω) ((⋂ x ∈ p1, f1 x) ∩ ⋂ x ∈ p2, f2 x)
    (⋂ i ∈ p1 ∪ p2, (if i ∈ p1 then f1 i else univ) ∩ if i ∈ p2 then f2 i else univ)
a : α
ha :
  Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ p1 ∪ p2, g i) : ℝ≥0∞)
    (∏ i ∈ p1 ∪ p2, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (g i) : ℝ≥0∞)
h :
  Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) ((⋂ x ∈ p1, f1 x) ∩ t2) : ℝ≥0∞)
    (∏ n ∈ p1 ∪ p2, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (g n) : ℝ≥0∞)
h₁ :
  Eq (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) ((⋂ x ∈ p1, f1 x) ∩ ⋂ x ∈ p2, f2 x) : ℝ≥0∞)
    (∏ n ∈ p1 ∪ p2, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (g n) : ℝ≥0∞)
h₂ :
  Eq (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
        (⋂ i ∈ p1 ∪ p2, (if i ∈ p1 then f1 i else univ) ∩ if i ∈ p2 then f2 i else univ) :
      ℝ≥0∞)
    (∏ n ∈ p1 ∪ p2, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (g n) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) : ℝ≥0∞)
    (∏ n ∈ p1 ∪ p2, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (g n) : ℝ≥0∞)
have h₃ : Eq (α := ℝ≥0∞)
  ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
      (⋂ i ∈ p1 ∪ p2, (if i ∈ p1 then f1 i else univ) ∩ if i ∈ p2 then f2 i else univ) :
    ℝ≥0∞)
  ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ p1 ∪ p2, g i) : ℝ≥0∞)
Tactic: rw [ht1_eq, ht2_eq, h_p1_inter_p2, ← ha]