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 α
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)
⊢ 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) =
    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 : ι), g i) : ENNReal)
have e_a : Eq.{u_2 + 1} (α := Set Ω) ((⋂ (i : ι), Y i ⁻¹' t i) ∩ ⋂ i ∈ s, f i) (⋂ (i : ι), g i)
Tactic: congr 2
-- 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)
⊢ Eq.{u_2 + 1} (α := Set Ω) ((⋂ (i : ι), Y i ⁻¹' t i) ∩ ⋂ i ∈ s, f i)
    ((⋂ (i : ι), Y i ⁻¹' t i) ∩ ⋂ (i : ι), if i ∈ s then f i else univ)
have e_a : Eq.{u_2 + 1} (α := Set Ω) (⋂ i ∈ s, f i) (⋂ (i : ι), if i ∈ s then f i else univ)
Tactic: congr 1
-- 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)
⊢ Eq.{u_2 + 1} (α := Set Ω) ((⋂ (i : ι), Y i ⁻¹' t i) ∩ ⋂ (i : ι), if i ∈ s then f i else univ)
    (⋂ (i : ι), Y i ⁻¹' t i ∩ if i ∈ s then f i else univ)
have rw : Eq.{u_2 + 1} (α := Set Ω) ((⋂ (i : ι), Y i ⁻¹' t i) ∩ ⋂ (i : ι), if i ∈ s then f i else univ)
  ((⋂ (i : ι), Y i ⁻¹' t i) ∩ ⋂ (i : ι), if i ∈ s then f i else univ)
Tactic: rw [Set.iInter_inter_distrib]
-- 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)
i : ι
⊢ (Y i ⁻¹' t i ∩ if i ∈ s then f i else univ) = g i
have pos : ∀ (hi : i ∈ s), (Y i ⁻¹' t i ∩ if i ∈ s then f i else univ) = 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_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)
i : ι
pos : ∀ (hi : i ∈ s), (Y i ⁻¹' t i ∩ if i ∈ s then f i else univ) = g i
⊢ (Y i ⁻¹' t i ∩ if i ∈ s then f i else univ) = g i
have neg : ∀ (hi : i ∉ s), (Y i ⁻¹' t i ∩ if i ∈ s then f i else univ) = 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_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)
⊢ Eq.{u_2 + 1} (α := Set Ω) ((⋂ (i : ι), Y i ⁻¹' t i) ∩ ⋂ i ∈ s, f i) (⋂ (i : ι), g i)
have _ : Eq.{u_2 + 1} (α := Set Ω) ((⋂ (i : ι), Y i ⁻¹' t i) ∩ ⋂ i ∈ s, f i)
  ((⋂ (i : ι), Y i ⁻¹' t i) ∩ ⋂ (i : ι), if i ∈ s then f i else univ)
Tactic: calc
        _ = (⋂ i, Y i ⁻¹' t i) ∩ ⋂ i, if i ∈ s then f i else .univ := by
          congr 1
          simp only [Set.iInter_ite, Set.iInter_univ, Set.inter_univ]
        _ = ⋂ i, Y i ⁻¹' t i ∩ (if i ∈ s then f i else .univ) := by rw [Set.iInter_inter_distrib]
        _ = _ := Set.iInter_congr fun i ↦ by by_cases hi : i ∈ s <;> simp [hi, 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_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)
_ :
  Eq.{u_2 + 1} (α := Set Ω) ((⋂ (i : ι), Y i ⁻¹' t i) ∩ ⋂ i ∈ s, f i)
    ((⋂ (i : ι), Y i ⁻¹' t i) ∩ ⋂ (i : ι), if i ∈ s then f i else univ)
⊢ Eq.{u_2 + 1} (α := Set Ω) ((⋂ (i : ι), Y i ⁻¹' t i) ∩ ⋂ i ∈ s, f i) (⋂ (i : ι), g i)
have _₁ : Eq.{u_2 + 1} (α := Set Ω) ((⋂ (i : ι), Y i ⁻¹' t i) ∩ ⋂ (i : ι), if i ∈ s then f i else univ)
  (⋂ (i : ι), Y i ⁻¹' t i ∩ if i ∈ s then f i else univ)
Tactic: calc
        _ = (⋂ i, Y i ⁻¹' t i) ∩ ⋂ i, if i ∈ s then f i else .univ := by
          congr 1
          simp only [Set.iInter_ite, Set.iInter_univ, Set.inter_univ]
        _ = ⋂ i, Y i ⁻¹' t i ∩ (if i ∈ s then f i else .univ) := by rw [Set.iInter_inter_distrib]
        _ = _ := Set.iInter_congr fun i ↦ by by_cases hi : i ∈ s <;> simp [hi, 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_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)
⊢ 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 : ι), g i) : ENNReal) =
    HMul.hMul (α := ENNReal) (β := ENNReal)
      ((∏ i : ι, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (Y i ⁻¹' t i))⁻¹ : ENNReal)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ (i : ι), g i) : ENNReal)
have rw : HMul.hMul (α := ENNReal) (β := ENNReal)
    ((∏ i : ι, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (Y i ⁻¹' t i))⁻¹ : ENNReal)
    ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ (i : ι), g i) : ENNReal) =
  HMul.hMul (α := ENNReal) (β := ENNReal)
    ((∏ i : ι, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (Y i ⁻¹' t i))⁻¹ : ENNReal)
    ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ (i : ι), g i) : ENNReal)
Tactic: rw [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_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)
⊢ HMul.hMul (α := ENNReal) (β := ENNReal)
      ((∏ i : ι, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (Y i ⁻¹' t i))⁻¹ : ENNReal)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ (i : ι), g i) : ENNReal) =
    HMul.hMul (α := ENNReal)
      (∏ i : ι, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (Y i ⁻¹' t i))⁻¹
      (∏ i : ι, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (g i))
have rw : HMul.hMul (α := ENNReal) (∏ i : ι, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (Y i ⁻¹' t i))⁻¹
    (∏ i : ι, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (g i)) =
  HMul.hMul (α := ENNReal)
    (∏ i : ι, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (Y i ⁻¹' t i))⁻¹
    (∏ i : ι, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (g i))
Tactic: rw [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)
⊢ HMul.hMul (α := ENNReal)
      (∏ i : ι, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (Y i ⁻¹' t i))⁻¹
      (∏ i : ι, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (g i)) =
    ∏ i : ι,
      HMul.hMul (α := ENNReal) (β := ENNReal)
        (((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (Y i ⁻¹' t i))⁻¹ : ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (g i) : ENNReal)
have rw : (↑Finset.univ : Set ι).Pairwise fun (i j : ι) ↦
  Ne (α := ENNReal) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (Y i ⁻¹' t i) : ENNReal)
      (0 : ENNReal) ∨
    Ne (α := ENNReal) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (Y j ⁻¹' t j) : ENNReal)
      (⊤ : ENNReal)
Tactic: rw [Finset.prod_mul_distrib, ENNReal.prod_inv_distrib]
-- 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)
⊢ Eq (α := ENNReal)
    (∏ i : ι,
      HMul.hMul (α := ENNReal) (β := ENNReal)
        (((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (Y i ⁻¹' t i))⁻¹ : ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (g i) : ENNReal))
    (∏ i : ι, if i ∈ s then ((κ : (a : α) → Measure Ω) a)[f i | Y i ⁻¹' t i] else 1)
have refine : ∀ (i : ι),
  Membership.mem (γ := Finset ι) Finset.univ i →
    HMul.hMul (α := ENNReal) (β := ENNReal)
        (((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (Y i ⁻¹' t i))⁻¹ : ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (g i) : ENNReal) =
      if i ∈ s then ((κ : (a : α) → Measure Ω) a)[f i | Y i ⁻¹' t i] else 1
Tactic: refine Finset.prod_congr rfl fun i _ ↦ ?_