awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
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
h :
  ∀ (x : Ω),
    Membership.mem (γ := Set Ω) ((fun (ω : Ω) ↦ (X i ω, Y i ω)) ⁻¹' SProd.sprod (β := Set β) A univ) x ↔ x ∈ f i
⊢ (fun (ω : Ω) ↦ (X i ω, Y i ω)) ⁻¹' SProd.sprod (β := Set β) A univ = f i

Tactic:
ext
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
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
x : Ω
⊢ Membership.mem (γ := Set Ω) ((fun (ω : Ω) ↦ (X i ω, Y i ω)) ⁻¹' SProd.sprod (β := Set β) A univ) x ↔ x ∈ f i

Tactic:
simp [← hA']
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
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
⊢ MeasurableSet (Y i ⁻¹' t i ∩ f i)

Tactic:
exact (hYt _).inter ⟨A ×ˢ .univ, hA.prod .univ, by ext; simp [← hA']⟩

Premises used: SProd.sprod, MeasurableSet.prod, And.intro, Exists.intro, MeasurableSet.inter
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
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)

Tactic:
hYt _
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
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)

Tactic:
exact hYt _
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
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)

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 _
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
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 : ∀ (i : ι), MeasurableSet (Y i ⁻¹' t i)
hg : ∀ (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) →
    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) →
      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)
⊢ IsProbabilityMeasure.{u_2} (α := Ω) (m0 := mΩ) ((κ : (a : α) → Measure Ω) a) →
    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) →
      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:
_
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
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)
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)
⊢ ∀ᵐ (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:
filter_upwards [hy, hindep.ae_isProbabilityMeasure, hindep.meas_iInter hYt, hindep.meas_iInter hg]
    with a hy _ hYt hg

Premises used: ProbabilityTheory.Kernel.iIndepFun.meas_iInter, ProbabilityTheory.Kernel.iIndepFun.ae_isProbabilityMeasure
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
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)
hms : MeasurableSet.{u_2} (α := Ω) (⋂ (i : ι), Y i ⁻¹' t i)
⊢ ((κ : (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)

Tactic:
rw [cond_apply]

Premises used: ProbabilityTheory.cond_apply
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
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)
⊢ MeasurableSet.{u_2} (α := Ω) (⋂ (i : ι), Y i ⁻¹' t i)

Tactic:
.iInter fun i ↦ hY i (ht i)

Premises used: MeasurableSet.iInter
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
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)
⊢ MeasurableSet.{u_2} (α := Ω) (⋂ (i : ι), Y i ⁻¹' t i)

Tactic:
exact .iInter fun i ↦ hY i (ht i)
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
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)
e_a : Eq.{u_2 + 1} (α := Set Ω) ((⋂ (i : ι), Y i ⁻¹' t i) ∩ ⋂ i ∈ s, f i) (⋂ (i : ι), g 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) =
    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)

Tactic:
congr 2
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
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)
e_a : Eq.{u_2 + 1} (α := Set Ω) (⋂ i ∈ s, f 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 : ι), Y i ⁻¹' t i) ∩ ⋂ (i : ι), if i ∈ s then f i else univ)

Tactic:
congr 1
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
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 ∈ s, f i) (⋂ (i : ι), if i ∈ s then f i else univ)

Tactic:
simp only [Set.iInter_ite, Set.iInter_univ, Set.inter_univ]

Premises used: Set.inter_univ, Set.iInter_univ, Set.iInter_ite
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
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)
rw 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)
⊢ 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:
rw [Set.iInter_inter_distrib]

Premises used: Set.iInter_inter_distrib