awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.IndepFun (goal)
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : Type u_8
m : MeasurableSpace β
inst : CommMonoid β
inst_1 : MeasurableMul₂ β
f : ι → Ω → β
hf_Indep : iIndepFun (β := fun (x : ι) ↦ β) f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
s : Finset ι
i : ι
hi : i ∉ s
have have₁ have₂ :
  ∀
    (h_right :
      f i =
        (fun (p : ↥{i} → β) ↦ p (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯)) ∘
          fun (a : Ω) (j : ↥{i}) ↦ f (↑j : ι) a),
    IndepFun (β := β) (∏ j ∈ s, f j) (f i) κ μ
have₃ :
  ∀
    (h_right :
      f i =
        (fun (p : ↥{i} → β) ↦ p (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯)) ∘
          fun (a : Ω) (j : ↥{i}) ↦ f (↑j : ι) a)
    (h_meas_right :
      Measurable (β := β) fun (p : ↥{i} → β) ↦
        p (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯)),
    IndepFun (β := β) (∏ j ∈ s, f j) (f i) κ μ
have₄ :
  ∀
    (h_right :
      f i =
        (fun (p : ↥{i} → β) ↦ p (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯)) ∘
          fun (a : Ω) (j : ↥{i}) ↦ f (↑j : ι) a)
    (h_meas_right :
      Measurable (β := β) fun (p : ↥{i} → β) ↦
        p (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯))
    (h_left :
      Eq (α := Ω → β) (∏ j ∈ s, f j) ((fun (p : ↥s → β) ↦ ∏ j : ↥s, p j) ∘ fun (a : Ω) (j : ↥s) ↦ f (↑j : ι) a)),
    IndepFun (β := β) (∏ j ∈ s, f j) (f i) κ μ
⊢ IndepFun (β := β) (∏ j ∈ s, f j) (f i) κ μ
have have₅ : ∀
  (h_right :
    f i =
      (fun (p : ↥{i} → β) ↦ p (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i sorry)) ∘
        fun (a : Ω) (j : ↥{i}) ↦ f (↑j : ι) a)
  (h_meas_right :
    Measurable (β := β) fun (p : ↥{i} → β) ↦
      p (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i sorry))
  (h_left : Eq (α := Ω → β) (∏ j ∈ s, f j) ((fun (p : ↥s → β) ↦ ∏ j : ↥s, p j) ∘ fun (a : Ω) (j : ↥s) ↦ f (↑j : ι) a))
  (h_meas_left : Measurable (β := β) fun (p : ↥s → β) ↦ ∏ j : ↥s, p j), IndepFun (β := β) (∏ j ∈ s, f j) (f i) κ μ
Tactic: classical
  have h_right : f i =
    (fun p : ({i} : Finset ι) → β => p ⟨i, Finset.mem_singleton_self i⟩) ∘
    fun a (j : ({i} : Finset ι)) => f j a := rfl
  have h_meas_right : Measurable fun p : ({i} : Finset ι) → β =>
      p ⟨i, Finset.mem_singleton_self i⟩ := measurable_pi_apply _
  have h_left : ∏ j ∈ s, f j = (fun p : s → β => ∏ j, p j) ∘ fun a (j : s) => f j a := by
    ext1 a
    simp only [Function.comp_apply]
    have : (∏ j : ↥s, f (↑j) a) = (∏ j : ↥s, f ↑j) a := by rw [Finset.prod_apply]
    rw [this, Finset.prod_coe_sort]
  have h_meas_left : Measurable fun p : s → β => ∏ j, p j :=
    Finset.univ.measurable_fun_prod fun (j : ↥s) (_H : j ∈ Finset.univ) => measurable_pi_apply j
  rw [h_left, h_right]
  exact
    (hf_Indep.indepFun_finset s {i} (Finset.disjoint_singleton_left.mpr hi).symm hf_meas).comp
      h_meas_left h_meas_right
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.IndepFun (goal)
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : Type u_8
m : MeasurableSpace β
inst : CommMonoid β
inst_1 : MeasurableMul₂ β
f : ι → Ω → β
hf_Indep : iIndepFun (β := fun (x : ι) ↦ β) f κ μ
hf_meas : ∀ (i : ι), AEMeasurable (_m := mΩ) (f i) ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
s : Finset ι
i : ι
hi : i ∉ s
⊢ IndepFun (β := β) (∏ j ∈ s, AEMeasurable.mk (f j) ⋯) (AEMeasurable.mk (f i) ⋯) κ μ
have refine : iIndepFun (β := fun (x : ι) ↦ β) (fun (i : ι) ↦ AEMeasurable.mk (f i) sorry) κ μ
Tactic: refine iIndepFun.indepFun_finsetProd_of_notMem ?_ (fun i ↦ (hf_meas i).measurable_mk) hi
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.IndepFun (hypothesis)
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : Type u_8
m : MeasurableSpace β
inst : CommMonoid β
inst_1 : MeasurableMul₂ β
f : ι → Ω → β
hf_Indep : iIndepFun (β := fun (x : ι) ↦ β) f κ μ
hf_meas : ∀ (i : ι), AEMeasurable (_m := mΩ) (f i) ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
s : Finset ι
i : ι
hi : i ∉ s
⊢ IndepFun (β := β) (∏ j ∈ s, f j) (f i) κ μ
have h : IndepFun (β := β) (∏ j ∈ s, AEMeasurable.mk (f j) sorry) (AEMeasurable.mk (f i) sorry) κ μ
Tactic: have h : IndepFun (∏ j ∈ s, (hf_meas j).mk (f j)) ((hf_meas i).mk (f i)) κ μ := by
    refine iIndepFun.indepFun_finsetProd_of_notMem ?_ (fun i ↦ (hf_meas i).measurable_mk) hi
    exact iIndepFun.congr' hf_Indep fun i ↦ Measure.ae_ae_of_ae_comp (hf_meas i).ae_eq_mk
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.IndepFun (goal)
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : Type u_8
m : MeasurableSpace β
inst : CommMonoid β
inst_1 : MeasurableMul₂ β
f : ι → Ω → β
hf_Indep : iIndepFun (β := fun (x : ι) ↦ β) f κ μ
hf_meas : ∀ (i : ι), AEMeasurable (_m := mΩ) (f i) ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
s : Finset ι
i : ι
hi : i ∉ s
h : IndepFun (β := β) (∏ j ∈ s, AEMeasurable.mk (f j) ⋯) (AEMeasurable.mk (f i) ⋯) κ μ
⊢ IndepFun (β := β) (∏ j ∈ s, f j) (f i) κ μ
have refine_1 : ∀ᵐ (a : α) ∂μ,
  Filter.EventuallyEq.{u_2, u_8} (β := β) (ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω))
    (∏ j ∈ s, AEMeasurable.mk (f j) sorry) (∏ j ∈ s, f j)
Tactic: refine IndepFun.congr' h ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.IndepFun (goal)
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : Type u_8
m : MeasurableSpace β
inst : CommMonoid β
inst_1 : MeasurableMul₂ β
f : ι → Ω → β
hf_Indep : iIndepFun (β := fun (x : ι) ↦ β) f κ μ
hf_meas : ∀ (i : ι), AEMeasurable (_m := mΩ) (f i) ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
s : Finset ι
i : ι
hi : i ∉ s
h : IndepFun (β := β) (∏ j ∈ s, AEMeasurable.mk (f j) ⋯) (AEMeasurable.mk (f i) ⋯) κ μ
refine_1 :
  ∀ᵐ (a : α) ∂μ,
    Filter.EventuallyEq.{u_2, u_8} (β := β) (ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω))
      (∏ j ∈ s, AEMeasurable.mk (f j) ⋯) (∏ j ∈ s, f j)
⊢ IndepFun (β := β) (∏ j ∈ s, f j) (f i) κ μ
have refine_2 : ∀ᵐ (a : α) ∂μ, AEMeasurable.mk (f i) sorry =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] f i
Tactic: refine IndepFun.congr' h ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.IndepFun (goal)
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : Type u_8
m : MeasurableSpace β
inst : CommMonoid β
inst_1 : MeasurableMul₂ β
f : ι → Ω → β
hf_Indep : iIndepFun (β := fun (x : ι) ↦ β) f κ μ
hf_meas : ∀ (i : ι), AEMeasurable (_m := mΩ) (f i) ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
s : Finset ι
i : ι
hi : i ∉ s
h : IndepFun (β := β) (∏ j ∈ s, AEMeasurable.mk (f j) ⋯) (AEMeasurable.mk (f i) ⋯) κ μ
⊢ ∀ᵐ (a : α) ∂μ,
    ∀ (i : ↥s),
      f (↑i : ι) =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] AEMeasurable.mk (f (↑i : ι)) ⋯
have rw : ∀ (i : ↥s),
  ∀ᵐ (a : α) ∂μ,
    f (↑i : ι) =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] AEMeasurable.mk (f (↑i : ι)) sorry
Tactic: rw [ae_all_iff]
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.IndepFun (hypothesis)
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : Type u_8
m : MeasurableSpace β
inst : CommMonoid β
inst_1 : MeasurableMul₂ β
f : ι → Ω → β
hf_Indep : iIndepFun (β := fun (x : ι) ↦ β) f κ μ
hf_meas : ∀ (i : ι), AEMeasurable (_m := mΩ) (f i) ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
s : Finset ι
i : ι
hi : i ∉ s
h : IndepFun (β := β) (∏ j ∈ s, AEMeasurable.mk (f j) ⋯) (AEMeasurable.mk (f i) ⋯) κ μ
⊢ ∀ᵐ (a : α) ∂μ,
    Filter.EventuallyEq.{u_2, u_8} (β := β) (ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω))
      (∏ j ∈ s, AEMeasurable.mk (f j) ⋯) (∏ j ∈ s, f j)
have this : ∀ᵐ (a : α) ∂μ,
  ∀ (i : ↥s),
    f (↑i : ι) =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] AEMeasurable.mk (f (↑i : ι)) sorry
Tactic: have : ∀ᵐ a ∂μ, ∀ (i : s), f i =ᵐ[κ a] (hf_meas i).mk := by
      rw [ae_all_iff]
      exact fun i ↦ Measure.ae_ae_of_ae_comp (hf_meas i).ae_eq_mk
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.IndepFun (goal)
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : Type u_8
m : MeasurableSpace β
inst : CommMonoid β
inst_1 : MeasurableMul₂ β
f : ι → Ω → β
hf_Indep : iIndepFun (β := fun (x : ι) ↦ β) f κ μ
hf_meas : ∀ (i : ι), AEMeasurable (_m := mΩ) (f i) ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
s : Finset ι
i : ι
hi : i ∉ s
h : IndepFun (β := β) (∏ j ∈ s, AEMeasurable.mk (f j) ⋯) (AEMeasurable.mk (f i) ⋯) κ μ
this :
  ∀ᵐ (a : α) ∂μ,
    ∀ (i : ↥s),
      f (↑i : ι) =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] AEMeasurable.mk (f (↑i : ι)) ⋯
⊢ ∀ᵐ (a : α) ∂μ,
    Filter.EventuallyEq.{u_2, u_8} (β := β) (ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω))
      (∏ j ∈ s, AEMeasurable.mk (f j) ⋯) (∏ j ∈ s, f j)
have h₁ : ∀ (a : α)
  (ha :
    ∀ (i : ↥s),
      f (↑i : ι) =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] AEMeasurable.mk (f (↑i : ι)) sorry),
  Filter.EventuallyEq.{u_2, u_8} (β := β) (ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω))
    (∏ j ∈ s, AEMeasurable.mk (f j) sorry) (∏ j ∈ s, f j)
Tactic: filter_upwards [this] with a ha
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.IndepFun (goal)
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : Type u_8
m : MeasurableSpace β
inst : CommMonoid β
inst_1 : MeasurableMul₂ β
f : ι → Ω → β
hf_Indep : iIndepFun (β := fun (x : ι) ↦ β) f κ μ
hf_meas : ∀ (i : ι), AEMeasurable (_m := mΩ) (f i) ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
s : Finset ι
i : ι
hi : i ∉ s
h : IndepFun (β := β) (∏ j ∈ s, AEMeasurable.mk (f j) ⋯) (AEMeasurable.mk (f i) ⋯) κ μ
this :
  ∀ᵐ (a : α) ∂μ,
    ∀ (i : ↥s),
      f (↑i : ι) =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] AEMeasurable.mk (f (↑i : ι)) ⋯
a : α
ha :
  ∀ (i : ↥s),
    f (↑i : ι) =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] AEMeasurable.mk (f (↑i : ι)) ⋯
⊢ Filter.EventuallyEq.{u_2, u_8} (β := β) (ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω))
    (∏ j ∈ s, AEMeasurable.mk (f j) ⋯) (∏ j ∈ s, f j)
have h₁ : ∀ (ω : Ω) (hω : ∀ (i : ↥s), f (↑i : ι) ω = AEMeasurable.mk (f (↑i : ι)) sorry ω),
  Eq.{u_8 + 1} (α := β) ((∏ j ∈ s, AEMeasurable.mk (f j) sorry) ω) ((∏ j ∈ s, f j) ω)
Tactic: filter_upwards [ae_all_iff.2 ha] with ω hω
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.IndepFun (goal)
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : Type u_8
m : MeasurableSpace β
inst : CommMonoid β
inst_1 : MeasurableMul₂ β
f : ι → Ω → β
hf_Indep : iIndepFun (β := fun (x : ι) ↦ β) f κ μ
hf_meas : ∀ (i : ι), AEMeasurable (_m := mΩ) (f i) ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
s : Finset ι
i : ι
hi : i ∉ s
h : IndepFun (β := β) (∏ j ∈ s, AEMeasurable.mk (f j) ⋯) (AEMeasurable.mk (f i) ⋯) κ μ
this :
  ∀ᵐ (a : α) ∂μ,
    ∀ (i : ↥s),
      f (↑i : ι) =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] AEMeasurable.mk (f (↑i : ι)) ⋯
a : α
ha :
  ∀ (i : ↥s),
    f (↑i : ι) =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] AEMeasurable.mk (f (↑i : ι)) ⋯
ω : Ω
hω : ∀ (i : ↥s), f (↑i : ι) ω = AEMeasurable.mk (f (↑i : ι)) ⋯ ω
⊢ Eq.{u_8 + 1} (α := β) ((∏ j ∈ s, AEMeasurable.mk (f j) ⋯) ω) ((∏ j ∈ s, f j) ω)
have h₁ : Eq.{u_8 + 1} (α := β) (∏ c ∈ s, AEMeasurable.mk (f c) sorry ω) (∏ c ∈ s, f c ω)
Tactic: simp only [Finset.prod_apply]
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.IndepFun (goal)
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
β : Type u_4
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst : Zero β
inst_1 : One β
m : MeasurableSpace β
s : ι → Set Ω
hs : iIndepSet s κ μ
⊢ iIndepFun (β := fun (n : ι) ↦ β) (fun (n : ι) ↦ (s n).indicator fun (_ω : Ω) ↦ 1) κ μ
have rw : ∀ (S : Finset ι) {sets : (i : ι) → Set β} (_H : ∀ i ∈ S, MeasurableSet (sets i)),
  ∀ᵐ (a : α) ∂μ,
    Eq (α := ENNReal)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
          (⋂ i ∈ S, ((s i).indicator fun (_ω : Ω) ↦ 1) ⁻¹' sets i) :
        ENNReal)
      (∏ i ∈ S,
          (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
            (((s i).indicator fun (_ω : Ω) ↦ 1) ⁻¹' sets i) :
        ENNReal)
Tactic: rw [iIndepFun_iff_measure_inter_preimage_eq_mul]
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.IndepFun (goal)
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
β : Type u_4
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst : Zero β
inst_1 : One β
m : MeasurableSpace β
s : ι → Set Ω
hs : iIndepSet s κ μ
S : Finset ι
π : (i : ι) → Set β
_hπ : ∀ i ∈ S, MeasurableSet (π i)
⊢ ∀ᵐ (a : α) ∂μ,
    Eq (α := ENNReal)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
          (⋂ i ∈ S, ((s i).indicator fun (_ω : Ω) ↦ 1) ⁻¹' π i) :
        ENNReal)
      (∏ i ∈ S,
          (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
            (((s i).indicator fun (_ω : Ω) ↦ 1) ⁻¹' π i) :
        ENNReal)
have simp_rw : ∀ᵐ (a : α) ∂μ,
  Eq (α := ENNReal)
    ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
        (⋂ i ∈ S, (if 1 ∈ π i then s i else ∅) ∪ if 0 ∈ π i then (s i)ᶜ else ∅) :
      ENNReal)
    (∏ x ∈ S,
        (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
          ((if 1 ∈ π x then s x else ∅) ∪ if 0 ∈ π x then (s x)ᶜ else ∅) :
      ENNReal)
Tactic: simp_rw [Set.indicator_const_preimage_eq_union]
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.IndepFun (goal)
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
β : Type u_4
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst : Zero β
inst_1 : One β
m : MeasurableSpace β
s : ι → Set Ω
hs : iIndepSet s κ μ
S : Finset ι
π : (i : ι) → Set β
_hπ : ∀ i ∈ S, MeasurableSet (π i)
⊢ ∀ᵐ (a : α) ∂μ,
    Eq (α := ENNReal)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
          (⋂ i ∈ S, (if 1 ∈ π i then s i else ∅) ∪ if 0 ∈ π i then (s i)ᶜ else ∅) :
        ENNReal)
      (∏ x ∈ S,
          (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
            ((if 1 ∈ π x then s x else ∅) ∪ if 0 ∈ π x then (s x)ᶜ else ∅) :
        ENNReal)
have apply : ∀ (i : ι) (_hi : i ∈ S),
  Membership.mem (γ := Set (Set Ω)) ((fun (x : ι) ↦ ({s_1 : Set Ω | MeasurableSet s_1} : Set (Set Ω))) i)
    ((if 1 ∈ π i then s i else ∅) ∪ if 0 ∈ π i then (s i)ᶜ else ∅)
Tactic: apply hs _ fun i _hi ↦ ?_
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.IndepFun (hypothesis)
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
β : Type u_4
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst : Zero β
inst_1 : One β
m : MeasurableSpace β
s : ι → Set Ω
hs : iIndepSet s κ μ
S : Finset ι
π : (i : ι) → Set β
_hπ : ∀ i ∈ S, MeasurableSet (π i)
i : ι
_hi : i ∈ S
⊢ Membership.mem (γ := Set (Set Ω)) ((fun (x : ι) ↦ ({s_1 : Set Ω | MeasurableSet s_1} : Set (Set Ω))) i)
    ((if 1 ∈ π i then s i else ∅) ∪ if 0 ∈ π i then (s i)ᶜ else ∅)
have hsi : MeasurableSet (s i)
Tactic: have hsi : MeasurableSet[generateFrom {s i}] (s i) :=
    measurableSet_generateFrom (Set.mem_singleton _)
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.IndepFun (goal)
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
β : Type u_4
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst : Zero β
inst_1 : One β
m : MeasurableSpace β
s : ι → Set Ω
hs : iIndepSet s κ μ
S : Finset ι
π : (i : ι) → Set β
_hπ : ∀ i ∈ S, MeasurableSet (π i)
i : ι
_hi : i ∈ S
hsi : MeasurableSet (s i)
⊢ Membership.mem (γ := Set (Set Ω)) ((fun (x : ι) ↦ ({s_1 : Set Ω | MeasurableSet s_1} : Set (Set Ω))) i)
    ((if 1 ∈ π i then s i else ∅) ∪ if 0 ∈ π i then (s i)ᶜ else ∅)
have refine_1 : 1 ∉ π i → MeasurableSet.{u_2} (α := Ω) ∅
Tactic: refine
    MeasurableSet.union (MeasurableSet.ite' (fun _ => hsi) fun _ => ?_)
      (MeasurableSet.ite' (fun _ => hsi.compl) fun _ => ?_)
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.IndepFun (goal)
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
β : Type u_4
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst : Zero β
inst_1 : One β
m : MeasurableSpace β
s : ι → Set Ω
hs : iIndepSet s κ μ
S : Finset ι
π : (i : ι) → Set β
_hπ : ∀ i ∈ S, MeasurableSet (π i)
i : ι
_hi : i ∈ S
hsi : MeasurableSet (s i)
refine_1 : 1 ∉ π i → MeasurableSet.{u_2} (α := Ω) ∅
⊢ Membership.mem (γ := Set (Set Ω)) ((fun (x : ι) ↦ ({s_1 : Set Ω | MeasurableSet s_1} : Set (Set Ω))) i)
    ((if 1 ∈ π i then s i else ∅) ∪ if 0 ∈ π i then (s i)ᶜ else ∅)
have refine_2 : 0 ∉ π i → MeasurableSet.{u_2} (α := Ω) ∅
Tactic: refine
    MeasurableSet.union (MeasurableSet.ite' (fun _ => hsi) fun _ => ?_)
      (MeasurableSet.ite' (fun _ => hsi.compl) fun _ => ?_)
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.IndepFun (goal)
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
β : Type u_4
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst : Zero β
inst_1 : One β
m : MeasurableSpace β
s : ι → Set Ω
hs : iIndepSet s κ μ
⊢ iIndepFun (β := fun (n : ι) ↦ β) (fun (n : ι) ↦ (s n).indicator fun (_ω : Ω) ↦ 1) κ μ
have rw : ∀ (S : Finset ι) {sets : (i : ι) → Set β} (_H : ∀ i ∈ S, MeasurableSet (sets i)),
  ∀ᵐ (a : α) ∂μ,
    Eq (α := ENNReal)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
          (⋂ i ∈ S, ((s i).indicator fun (_ω : Ω) ↦ 1) ⁻¹' sets i) :
        ENNReal)
      (∏ i ∈ S,
          (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
            (((s i).indicator fun (_ω : Ω) ↦ 1) ⁻¹' sets i) :
        ENNReal)
Tactic: classical
  rw [iIndepFun_iff_measure_inter_preimage_eq_mul]
  rintro S π _hπ
  simp_rw [Set.indicator_const_preimage_eq_union]
  apply hs _ fun i _hi ↦ ?_
  have hsi : MeasurableSet[generateFrom {s i}] (s i) :=
    measurableSet_generateFrom (Set.mem_singleton _)
  refine
    MeasurableSet.union (MeasurableSet.ite' (fun _ => hsi) fun _ => ?_)
      (MeasurableSet.ite' (fun _ => hsi.compl) fun _ => ?_)
  · exact @MeasurableSet.empty _ (generateFrom {s i})
  · exact @MeasurableSet.empty _ (generateFrom {s i})
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.IndepFun (goal)
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
β : Type u_4
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst : Zero β
inst_1 : One β
m : MeasurableSpace β
s : ι → Set Ω
hs : iIndepSet s κ μ
rw rw₁ rw₂ rw₃ :
  ∀ (S : Finset ι) {π : (i : ι) → Set β} (_hπ : ∀ i ∈ S, MeasurableSet (π i)),
    ∀ᵐ (a : α) ∂μ,
      Eq (α := ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
            (⋂ i ∈ S, ((s i).indicator fun (_ω : Ω) ↦ 1) ⁻¹' π i) :
          ENNReal)
        (∏ i ∈ S,
            (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
              (((s i).indicator fun (_ω : Ω) ↦ 1) ⁻¹' π i) :
          ENNReal)
⊢ iIndepFun (β := fun (n : ι) ↦ β) (fun (n : ι) ↦ (s n).indicator fun (_ω : Ω) ↦ 1) κ μ
have rw₄ : ∀ (S : Finset ι) {π : (i : ι) → Set β} (_hπ : ∀ i ∈ S, MeasurableSet (π i)),
  ∀ᵐ (a : α) ∂μ,
    Eq (α := ENNReal)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
          (⋂ i ∈ S, (if 1 ∈ π i then s i else ∅) ∪ if 0 ∈ π i then (s i)ᶜ else ∅) :
        ENNReal)
      (∏ x ∈ S,
          (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
            ((if 1 ∈ π x then s x else ∅) ∪ if 0 ∈ π x then (s x)ᶜ else ∅) :
        ENNReal)
Tactic: classical
  rw [iIndepFun_iff_measure_inter_preimage_eq_mul]
  rintro S π _hπ
  simp_rw [Set.indicator_const_preimage_eq_union]
  apply hs _ fun i _hi ↦ ?_
  have hsi : MeasurableSet[generateFrom {s i}] (s i) :=
    measurableSet_generateFrom (Set.mem_singleton _)
  refine
    MeasurableSet.union (MeasurableSet.ite' (fun _ => hsi) fun _ => ?_)
      (MeasurableSet.ite' (fun _ => hsi.compl) fun _ => ?_)
  · exact @MeasurableSet.empty _ (generateFrom {s i})
  · exact @MeasurableSet.empty _ (generateFrom {s i})
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.IndepFun (goal)
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
β : Type u_4
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst : Zero β
inst_1 : One β
m : MeasurableSpace β
s : ι → Set Ω
hs : iIndepSet s κ μ
rw rw₁ rw₂ rw₃ :
  ∀ (S : Finset ι) {π : (i : ι) → Set β} (_hπ : ∀ i ∈ S, MeasurableSet (π i)),
    ∀ᵐ (a : α) ∂μ,
      Eq (α := ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
            (⋂ i ∈ S, ((s i).indicator fun (_ω : Ω) ↦ 1) ⁻¹' π i) :
          ENNReal)
        (∏ i ∈ S,
            (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
              (((s i).indicator fun (_ω : Ω) ↦ 1) ⁻¹' π i) :
          ENNReal)
rw₄ :
  ∀ (S : Finset ι) {π : (i : ι) → Set β} (_hπ : ∀ i ∈ S, MeasurableSet (π i)),
    ∀ᵐ (a : α) ∂μ,
      Eq (α := ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
            (⋂ i ∈ S, (if 1 ∈ π i then s i else ∅) ∪ if 0 ∈ π i then (s i)ᶜ else ∅) :
          ENNReal)
        (∏ x ∈ S,
            (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
              ((if 1 ∈ π x then s x else ∅) ∪ if 0 ∈ π x then (s x)ᶜ else ∅) :
          ENNReal)
⊢ iIndepFun (β := fun (n : ι) ↦ β) (fun (n : ι) ↦ (s n).indicator fun (_ω : Ω) ↦ 1) κ μ
have rw₅ : ∀ (S : Finset ι) {π : (i : ι) → Set β} (_hπ : ∀ i ∈ S, MeasurableSet (π i)) (i : ι) (_hi : i ∈ S),
  Membership.mem (γ := Set (Set Ω)) ((fun (x : ι) ↦ ({s_1 : Set Ω | MeasurableSet s_1} : Set (Set Ω))) i)
    ((if 1 ∈ π i then s i else ∅) ∪ if 0 ∈ π i then (s i)ᶜ else ∅)
Tactic: classical
  rw [iIndepFun_iff_measure_inter_preimage_eq_mul]
  rintro S π _hπ
  simp_rw [Set.indicator_const_preimage_eq_union]
  apply hs _ fun i _hi ↦ ?_
  have hsi : MeasurableSet[generateFrom {s i}] (s i) :=
    measurableSet_generateFrom (Set.mem_singleton _)
  refine
    MeasurableSet.union (MeasurableSet.ite' (fun _ => hsi) fun _ => ?_)
      (MeasurableSet.ite' (fun _ => hsi.compl) fun _ => ?_)
  · exact @MeasurableSet.empty _ (generateFrom {s i})
  · exact @MeasurableSet.empty _ (generateFrom {s i})