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
β : 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)
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 ∅)
⊢ 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)
  (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 ∅)
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)
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 ∅)
rw₆ :
  ∀ (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 ∅)
⊢ iIndepFun (β := fun (n : ι) ↦ β) (fun (n : ι) ↦ (s n).indicator fun (_ω : Ω) ↦ 1) κ μ
have refine_1 : ∀ (S : Finset ι) {π : (i : ι) → Set β} (_hπ : ∀ i ∈ S, MeasurableSet (π i)) (i : ι) (_hi : i ∈ S)
  (hsi : MeasurableSet (s i)), 1 ∉ π i → MeasurableSet.{u_2} (α := Ω) ∅
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)
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 ∅)
rw₆ :
  ∀ (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 ∅)
refine_1 :
  ∀ (S : Finset ι) {π : (i : ι) → Set β} (_hπ : ∀ i ∈ S, MeasurableSet (π i)) (i : ι) (_hi : i ∈ S)
    (hsi : MeasurableSet (s i)), 1 ∉ π i → MeasurableSet.{u_2} (α := Ω) ∅
⊢ iIndepFun (β := fun (n : ι) ↦ β) (fun (n : ι) ↦ (s n).indicator fun (_ω : Ω) ↦ 1) κ μ
have refine_2 : ∀ (S : Finset ι) {π : (i : ι) → Set β} (_hπ : ∀ i ∈ S, MeasurableSet (π i)) (i : ι) (_hi : i ∈ S)
  (hsi : MeasurableSet (s i)), 0 ∉ π i → MeasurableSet.{u_2} (α := Ω) ∅
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 α
mβ : MeasurableSpace β
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (β := fun (i : ι) ↦ α × β) (fun (i : ι) (ω : Ω) ↦ (X i ω, Y i ω)) κ μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy :
  ∀ᵐ (a : α) ∂μ,
    ∀ i ∉ s,
      Ne (α := ENNReal) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (Y i ⁻¹' t i) : ENNReal)
        (0 : ENNReal)
ht : ∀ (i : ι), MeasurableSet (t i)
⊢ ∀ᵐ (a : α) ∂μ,
    Eq (α := ENNReal) (((κ : (a : α) → Measure Ω) a)[⋂ i ∈ s, f i | ⋂ (i : ι), Y i ⁻¹' t i] : ENNReal)
      (∏ i ∈ s, ((κ : (a : α) → Measure Ω) a)[f i | Y i ⁻¹' t i] : ENNReal)
have intro : ∀ (val : Fintype ι),
  ∀ᵐ (a : α) ∂μ,
    Eq (α := ENNReal) (((κ : (a : α) → Measure Ω) a)[⋂ i ∈ s, f i | ⋂ (i : ι), Y i ⁻¹' t i] : ENNReal)
      (∏ i ∈ s, ((κ : (a : α) → Measure Ω) a)[f i | Y i ⁻¹' t i] : ENNReal)
Tactic: cases nonempty_fintype ι
-- 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 α
mβ : MeasurableSpace β
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (β := fun (i : ι) ↦ α × β) (fun (i : ι) (ω : Ω) ↦ (X i ω, Y i ω)) κ μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy :
  ∀ᵐ (a : α) ∂μ,
    ∀ i ∉ s,
      Ne (α := ENNReal) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (Y i ⁻¹' t i) : ENNReal)
        (0 : ENNReal)
ht : ∀ (i : ι), MeasurableSet (t i)
val : Fintype ι
g : (i' : ι) → Set Ω := fun (i' : ι) ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
i : ι
⊢ (fun (ω : Ω) ↦ (X i ω, Y i ω)) ⁻¹' SProd.sprod (α := Set α) univ (t i) = Y i ⁻¹' t i
have h : ∀ (x : Ω),
  Membership.mem (γ := Set Ω) ((fun (ω : Ω) ↦ (X i ω, Y i ω)) ⁻¹' SProd.sprod (α := Set α) univ (t i)) x ↔
    x ∈ Y i ⁻¹' t i
Tactic: ext
-- 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 α
mβ : MeasurableSpace β
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (β := fun (i : ι) ↦ α × β) (fun (i : ι) (ω : Ω) ↦ (X i ω, Y i ω)) κ μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy :
  ∀ᵐ (a : α) ∂μ,
    ∀ i ∉ s,
      Ne (α := ENNReal) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (Y i ⁻¹' t i) : ENNReal)
        (0 : ENNReal)
ht : ∀ (i : ι), MeasurableSet (t i)
val : Fintype ι
g : (i' : ι) → Set Ω := fun (i' : ι) ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
⊢ ∀ᵐ (a : α) ∂μ,
    Eq (α := ENNReal) (((κ : (a : α) → Measure Ω) a)[⋂ i ∈ s, f i | ⋂ (i : ι), Y i ⁻¹' t i] : ENNReal)
      (∏ i ∈ s, ((κ : (a : α) → Measure Ω) a)[f i | Y i ⁻¹' t i] : ENNReal)
have hYt : ∀ (i : ι), MeasurableSet (Y i ⁻¹' t i)
Tactic: have hYt i : MeasurableSet[(mα.prod mβ).comap fun ω ↦ (X i ω, Y i ω)] (Y i ⁻¹' t i) :=
    ⟨.univ ×ˢ t i, .prod .univ (ht _), by ext; simp⟩
-- 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 α
mβ : MeasurableSpace β
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (β := fun (i : ι) ↦ α × β) (fun (i : ι) (ω : Ω) ↦ (X i ω, Y i ω)) κ μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy :
  ∀ᵐ (a : α) ∂μ,
    ∀ i ∉ s,
      Ne (α := ENNReal) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (Y i ⁻¹' t i) : ENNReal)
        (0 : ENNReal)
ht : ∀ (i : ι), MeasurableSet (t i)
val : Fintype ι
g : (i' : ι) → Set Ω := fun (i' : ι) ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
hYt : ∀ (i : ι), MeasurableSet (Y i ⁻¹' t i)
i : ι
⊢ MeasurableSet (g i)
have pos : ∀ (hi : i ∈ s), MeasurableSet (g i)
Tactic: by_cases hi : i ∈ s
-- 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 α
mβ : MeasurableSpace β
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (β := fun (i : ι) ↦ α × β) (fun (i : ι) (ω : Ω) ↦ (X i ω, Y i ω)) κ μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy :
  ∀ᵐ (a : α) ∂μ,
    ∀ i ∉ s,
      Ne (α := ENNReal) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (Y i ⁻¹' t i) : ENNReal)
        (0 : ENNReal)
ht : ∀ (i : ι), MeasurableSet (t i)
val : Fintype ι
g : (i' : ι) → Set Ω := fun (i' : ι) ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
hYt : ∀ (i : ι), MeasurableSet (Y i ⁻¹' t i)
i : ι
pos : ∀ (hi : i ∈ s), MeasurableSet (g i)
⊢ MeasurableSet (g i)
have neg : ∀ (hi : i ∉ s), MeasurableSet (g i)
Tactic: by_cases hi : i ∈ s
-- 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 α
mβ : MeasurableSpace β
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (β := fun (i : ι) ↦ α × β) (fun (i : ι) (ω : Ω) ↦ (X i ω, Y i ω)) κ μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy :
  ∀ᵐ (a : α) ∂μ,
    ∀ i ∉ s,
      Ne (α := ENNReal) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (Y i ⁻¹' t i) : ENNReal)
        (0 : ENNReal)
ht : ∀ (i : ι), MeasurableSet (t i)
val : Fintype ι
g : (i' : ι) → Set Ω := fun (i' : ι) ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
hYt : ∀ (i : ι), MeasurableSet (Y i ⁻¹' t i)
i : ι
hi : i ∈ s
⊢ MeasurableSet (g i)
have pos : MeasurableSet (Y i ⁻¹' t i ∩ f i)
Tactic: simp only [hi, ↓reduceIte, g]
-- 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 α
mβ : MeasurableSpace β
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (β := fun (i : ι) ↦ α × β) (fun (i : ι) (ω : Ω) ↦ (X i ω, Y i ω)) κ μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy :
  ∀ᵐ (a : α) ∂μ,
    ∀ i ∉ s,
      Ne (α := ENNReal) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (Y i ⁻¹' t i) : ENNReal)
        (0 : ENNReal)
ht : ∀ (i : ι), MeasurableSet (t i)
val : Fintype ι
g : (i' : ι) → Set Ω := fun (i' : ι) ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
hYt : ∀ (i : ι), MeasurableSet (Y i ⁻¹' t i)
i : ι
hi : i ∉ s
⊢ MeasurableSet (g i)
have neg : MeasurableSet (Y i ⁻¹' t i)
Tactic: simp only [hi, ↓reduceIte, g]
-- 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 α
mβ : MeasurableSpace β
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (β := fun (i : ι) ↦ α × β) (fun (i : ι) (ω : Ω) ↦ (X i ω, Y i ω)) κ μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy :
  ∀ᵐ (a : α) ∂μ,
    ∀ i ∉ s,
      Ne (α := ENNReal) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (Y i ⁻¹' t i) : ENNReal)
        (0 : ENNReal)
ht : ∀ (i : ι), MeasurableSet (t i)
val : Fintype ι
g : (i' : ι) → Set Ω := fun (i' : ι) ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
hYt : ∀ (i : ι), MeasurableSet (Y i ⁻¹' t i)
i : ι
hi : i ∈ s
⊢ MeasurableSet (Y i ⁻¹' t i ∩ f i)
have pos : ∀ (A : Set α) (hA : MeasurableSet A) (hA' : X i ⁻¹' A = f i), MeasurableSet (Y i ⁻¹' t i ∩ f i)
Tactic: obtain ⟨A, hA, hA'⟩ := hf i hi
-- 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 α
mβ : MeasurableSpace β
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (β := fun (i : ι) ↦ α × β) (fun (i : ι) (ω : Ω) ↦ (X i ω, Y i ω)) κ μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy :
  ∀ᵐ (a : α) ∂μ,
    ∀ i ∉ s,
      Ne (α := ENNReal) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (Y i ⁻¹' t i) : ENNReal)
        (0 : ENNReal)
ht : ∀ (i : ι), MeasurableSet (t i)
val : Fintype ι
g : (i' : ι) → Set Ω := fun (i' : ι) ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
hYt : ∀ (i : ι), MeasurableSet (Y i ⁻¹' t i)
i : ι
hi : i ∈ s
A : Set α
hA : MeasurableSet A
hA' : X i ⁻¹' A = f i
⊢ (fun (ω : Ω) ↦ (X i ω, Y i ω)) ⁻¹' SProd.sprod (β := Set β) A univ = f i
have h : ∀ (x : Ω), Membership.mem (γ := Set Ω) ((fun (ω : Ω) ↦ (X i ω, Y i ω)) ⁻¹' SProd.sprod (β := Set β) A univ) x ↔ x ∈ f i
Tactic: ext
-- 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 α
mβ : MeasurableSpace β
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (β := fun (i : ι) ↦ α × β) (fun (i : ι) (ω : Ω) ↦ (X i ω, Y i ω)) κ μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy :
  ∀ᵐ (a : α) ∂μ,
    ∀ i ∉ s,
      Ne (α := ENNReal) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (Y i ⁻¹' t i) : ENNReal)
        (0 : ENNReal)
ht : ∀ (i : ι), MeasurableSet (t i)
val : Fintype ι
g : (i' : ι) → Set Ω := fun (i' : ι) ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
hYt : ∀ (i : ι), MeasurableSet (Y i ⁻¹' t i)
⊢ ∀ᵐ (a : α) ∂μ,
    Eq (α := ENNReal) (((κ : (a : α) → Measure Ω) a)[⋂ i ∈ s, f i | ⋂ (i : ι), Y i ⁻¹' t i] : ENNReal)
      (∏ i ∈ s, ((κ : (a : α) → Measure Ω) a)[f i | Y i ⁻¹' t i] : ENNReal)
have hg : ∀ (i : ι), MeasurableSet (g i)
Tactic: have hg i : MeasurableSet[(mα.prod mβ).comap fun ω ↦ (X i ω, Y i ω)] (g i) := by
    by_cases hi : i ∈ s <;> simp only [hi, ↓reduceIte, g]
    · obtain ⟨A, hA, hA'⟩ := hf i hi
      exact (hYt _).inter ⟨A ×ˢ .univ, hA.prod .univ, by ext; simp [← hA']⟩
    · exact hYt _
-- 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 α
mβ : MeasurableSpace β
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (β := fun (i : ι) ↦ α × β) (fun (i : ι) (ω : Ω) ↦ (X i ω, Y i ω)) κ μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy :
  ∀ᵐ (a : α) ∂μ,
    ∀ i ∉ s,
      Ne (α := ENNReal) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (Y i ⁻¹' t i) : ENNReal)
        (0 : ENNReal)
ht : ∀ (i : ι), MeasurableSet (t i)
val : Fintype ι
g : (i' : ι) → Set Ω := fun (i' : ι) ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
hYt : ∀ (i : ι), MeasurableSet (Y i ⁻¹' t i)
hg : ∀ (i : ι), MeasurableSet (g i)
⊢ ∀ᵐ (a : α) ∂μ,
    Eq (α := ENNReal) (((κ : (a : α) → Measure Ω) a)[⋂ i ∈ s, f i | ⋂ (i : ι), Y i ⁻¹' t i] : ENNReal)
      (∏ i ∈ s, ((κ : (a : α) → Measure Ω) a)[f i | Y i ⁻¹' t i] : ENNReal)
have h : ∀ (a : α)
  (hy :
    ∀ i ∉ s,
      Ne (α := ENNReal) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (Y i ⁻¹' t i) : ENNReal)
        (0 : ENNReal)),
  IsProbabilityMeasure.{u_2} (α := Ω) (m0 := mΩ) ((κ : (a : α) → Measure Ω) a) →
    ∀
      (hYt :
        Eq (α := ENNReal)
          ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ (i : ι), Y i ⁻¹' t i) : ENNReal)
          (∏ i : ι, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (Y i ⁻¹' t i) : ENNReal))
      (hg :
        Eq (α := ENNReal)
          ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ (i : ι), g i) : ENNReal)
          (∏ i : ι, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (g i) : ENNReal)),
      Eq (α := ENNReal) (((κ : (a : α) → Measure Ω) a)[⋂ i ∈ s, f i | ⋂ (i : ι), Y i ⁻¹' t i] : ENNReal)
        (∏ i ∈ s, ((κ : (a : α) → Measure Ω) a)[f i | Y i ⁻¹' t i] : ENNReal)
Tactic: filter_upwards [hy, hindep.ae_isProbabilityMeasure, hindep.meas_iInter hYt, hindep.meas_iInter hg]
    with a hy _ hYt hg
-- 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 α
mβ : MeasurableSpace β
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (β := fun (i : ι) ↦ α × β) (fun (i : ι) (ω : Ω) ↦ (X i ω, Y i ω)) κ μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy_1 :
  ∀ᵐ (a : α) ∂μ,
    ∀ i ∉ s,
      Ne (α := ENNReal) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (Y i ⁻¹' t i) : ENNReal)
        (0 : ENNReal)
ht : ∀ (i : ι), MeasurableSet (t i)
val : Fintype ι
g : (i' : ι) → Set Ω := fun (i' : ι) ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
hYt_1 : ∀ (i : ι), MeasurableSet (Y i ⁻¹' t i)
hg_1 : ∀ (i : ι), MeasurableSet (g i)
a : α
hy :
  ∀ i ∉ s,
    Ne (α := ENNReal) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (Y i ⁻¹' t i) : ENNReal)
      (0 : ENNReal)
h : IsProbabilityMeasure.{u_2} (α := Ω) (m0 := mΩ) ((κ : (a : α) → Measure Ω) a)
hYt :
  Eq (α := ENNReal)
    ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ (i : ι), Y i ⁻¹' t i) : ENNReal)
    (∏ i : ι, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (Y i ⁻¹' t i) : ENNReal)
hg :
  Eq (α := ENNReal) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ (i : ι), g i) : ENNReal)
    (∏ i : ι, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (g i) : ENNReal)
⊢ ((κ : (a : α) → Measure Ω) a)[⋂ i ∈ s, f i | ⋂ (i : ι), Y i ⁻¹' t i] =
    HMul.hMul (α := ENNReal) (β := ENNReal)
      (((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ (i : ι), Y i ⁻¹' t i))⁻¹ : ENNReal)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) ((⋂ (i : ι), Y i ⁻¹' t i) ∩ ⋂ i ∈ s, f i) :
        ENNReal)
have hms : MeasurableSet.{u_2} (α := Ω) (⋂ (i : ι), Y i ⁻¹' t i)
Tactic: rw [cond_apply]