awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
ι : Type u_8
β : ι → Type u_9
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
refine :
  (∀ (S : Finset ι) {sets : (i : ι) → Set (β i)} (_H : ∀ i ∈ S, MeasurableSet (sets i)),
      ∀ᵐ (a : α) ∂μ,
        Eq (α := ENNReal)
          ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ i ∈ S, f i ⁻¹' sets i) : ENNReal)
          (∏ i ∈ S, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f i ⁻¹' sets i) : ENNReal)) →
    iIndepFun (β := β) f κ μ
⊢ iIndepFun (β := β) f κ μ ↔
    ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)} (_H : ∀ i ∈ S, MeasurableSet (sets i)),
      ∀ᵐ (a : α) ∂μ,
        Eq (α := ENNReal)
          ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ i ∈ S, f i ⁻¹' sets i) : ENNReal)
          (∏ i ∈ S, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f i ⁻¹' sets i) : ENNReal)

Tactic:
refine ⟨fun h S sets h_meas => h _ fun i hi_mem => ⟨sets i, h_meas i hi_mem, rfl⟩, ?_⟩
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
ι : Type u_8
β : ι → Type u_9
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
h :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)} (_H : ∀ i ∈ S, MeasurableSet (sets i)),
    ∀ᵐ (a : α) ∂μ,
      Eq (α := ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ i ∈ S, f i ⁻¹' sets i) : ENNReal)
        (∏ i ∈ S, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f i ⁻¹' sets i) : ENNReal)
S : Finset ι
setsΩ : ι → Set Ω
h_meas :
  ∀ i ∈ S, Membership.mem (γ := Set (Set Ω)) ((fun (x : ι) ↦ ({s : Set Ω | MeasurableSet s} : Set (Set Ω))) i) (setsΩ i)
setsβ : (i : ι) → Set (β i) :=
  fun (i : ι) ↦
    if hi_mem : i ∈ S then Exists.choose (p := fun (s' : Set (β i)) ↦ MeasurableSet s' ∧ f i ⁻¹' s' = setsΩ i) ⋯
    else univ
i : ι
hi_mem : i ∈ S
simp_rw : MeasurableSet (Exists.choose (p := fun (s' : Set (β i)) ↦ MeasurableSet s' ∧ f i ⁻¹' s' = setsΩ i) ⋯)
⊢ MeasurableSet (setsβ i)

Tactic:
simp_rw [setsβ, dif_pos hi_mem]

Premises used: dif_pos
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
ι : Type u_8
β : ι → Type u_9
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
h :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)} (_H : ∀ i ∈ S, MeasurableSet (sets i)),
    ∀ᵐ (a : α) ∂μ,
      Eq (α := ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ i ∈ S, f i ⁻¹' sets i) : ENNReal)
        (∏ i ∈ S, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f i ⁻¹' sets i) : ENNReal)
S : Finset ι
setsΩ : ι → Set Ω
h_meas :
  ∀ i ∈ S, Membership.mem (γ := Set (Set Ω)) ((fun (x : ι) ↦ ({s : Set Ω | MeasurableSet s} : Set (Set Ω))) i) (setsΩ i)
setsβ : (i : ι) → Set (β i) :=
  fun (i : ι) ↦
    if hi_mem : i ∈ S then Exists.choose (p := fun (s' : Set (β i)) ↦ MeasurableSet s' ∧ f i ⁻¹' s' = setsΩ i) ⋯
    else univ
i : ι
hi_mem : i ∈ S
⊢ MeasurableSet (Exists.choose (p := fun (s' : Set (β i)) ↦ MeasurableSet s' ∧ f i ⁻¹' s' = setsΩ i) ⋯)

Tactic:
(h_meas i hi_mem).choose_spec.1

Premises used: Exists.choose_spec, And.left
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
ι : Type u_8
β : ι → Type u_9
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
h :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)} (_H : ∀ i ∈ S, MeasurableSet (sets i)),
    ∀ᵐ (a : α) ∂μ,
      Eq (α := ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ i ∈ S, f i ⁻¹' sets i) : ENNReal)
        (∏ i ∈ S, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f i ⁻¹' sets i) : ENNReal)
S : Finset ι
setsΩ : ι → Set Ω
h_meas :
  ∀ i ∈ S, Membership.mem (γ := Set (Set Ω)) ((fun (x : ι) ↦ ({s : Set Ω | MeasurableSet s} : Set (Set Ω))) i) (setsΩ i)
setsβ : (i : ι) → Set (β i) :=
  fun (i : ι) ↦
    if hi_mem : i ∈ S then Exists.choose (p := fun (s' : Set (β i)) ↦ MeasurableSet s' ∧ f i ⁻¹' s' = setsΩ i) ⋯
    else univ
i : ι
hi_mem : i ∈ S
⊢ MeasurableSet (Exists.choose (p := fun (s' : Set (β i)) ↦ MeasurableSet s' ∧ f i ⁻¹' s' = setsΩ i) ⋯)

Tactic:
exact (h_meas i hi_mem).choose_spec.1

Premises used: Exists.choose_spec, And.left
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
ι : Type u_8
β : ι → Type u_9
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
h :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)} (_H : ∀ i ∈ S, MeasurableSet (sets i)),
    ∀ᵐ (a : α) ∂μ,
      Eq (α := ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ i ∈ S, f i ⁻¹' sets i) : ENNReal)
        (∏ i ∈ S, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f i ⁻¹' sets i) : ENNReal)
S : Finset ι
setsΩ : ι → Set Ω
h_meas :
  ∀ i ∈ S, Membership.mem (γ := Set (Set Ω)) ((fun (x : ι) ↦ ({s : Set Ω | MeasurableSet s} : Set (Set Ω))) i) (setsΩ i)
setsβ : (i : ι) → Set (β i) :=
  fun (i : ι) ↦
    if hi_mem : i ∈ S then Exists.choose (p := fun (s' : Set (β i)) ↦ MeasurableSet s' ∧ f i ⁻¹' s' = setsΩ i) ⋯
    else univ
⊢ ∀ i ∈ S, MeasurableSet (setsβ i)

Tactic:
have h_measβ : ∀ i ∈ S, MeasurableSet[m i] (setsβ i) := by
    intro i hi_mem
    simp_rw [setsβ, dif_pos hi_mem]
    exact (h_meas i hi_mem).choose_spec.1
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
ι : Type u_8
β : ι → Type u_9
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
h :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)} (_H : ∀ i ∈ S, MeasurableSet (sets i)),
    ∀ᵐ (a : α) ∂μ,
      Eq (α := ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ i ∈ S, f i ⁻¹' sets i) : ENNReal)
        (∏ i ∈ S, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f i ⁻¹' sets i) : ENNReal)
S : Finset ι
setsΩ : ι → Set Ω
h_meas :
  ∀ i ∈ S, Membership.mem (γ := Set (Set Ω)) ((fun (x : ι) ↦ ({s : Set Ω | MeasurableSet s} : Set (Set Ω))) i) (setsΩ i)
setsβ : (i : ι) → Set (β i) :=
  fun (i : ι) ↦
    if hi_mem : i ∈ S then Exists.choose (p := fun (s' : Set (β i)) ↦ MeasurableSet s' ∧ f i ⁻¹' s' = setsΩ i) ⋯
    else univ
h_measβ : ∀ i ∈ S, MeasurableSet (setsβ i)
i : ι
hi_mem : i ∈ S
simp_rw : setsΩ i = f i ⁻¹' Exists.choose (p := fun (s' : Set (β i)) ↦ MeasurableSet s' ∧ f i ⁻¹' s' = setsΩ i) ⋯
⊢ setsΩ i = f i ⁻¹' setsβ i

Tactic:
simp_rw [setsβ, dif_pos hi_mem]

Premises used: dif_pos
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
ι : Type u_8
β : ι → Type u_9
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
h :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)} (_H : ∀ i ∈ S, MeasurableSet (sets i)),
    ∀ᵐ (a : α) ∂μ,
      Eq (α := ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ i ∈ S, f i ⁻¹' sets i) : ENNReal)
        (∏ i ∈ S, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f i ⁻¹' sets i) : ENNReal)
S : Finset ι
setsΩ : ι → Set Ω
h_meas :
  ∀ i ∈ S, Membership.mem (γ := Set (Set Ω)) ((fun (x : ι) ↦ ({s : Set Ω | MeasurableSet s} : Set (Set Ω))) i) (setsΩ i)
setsβ : (i : ι) → Set (β i) :=
  fun (i : ι) ↦
    if hi_mem : i ∈ S then Exists.choose (p := fun (s' : Set (β i)) ↦ MeasurableSet s' ∧ f i ⁻¹' s' = setsΩ i) ⋯
    else univ
h_measβ : ∀ i ∈ S, MeasurableSet (setsβ i)
i : ι
hi_mem : i ∈ S
⊢ setsΩ i = f i ⁻¹' Exists.choose (p := fun (s' : Set (β i)) ↦ MeasurableSet s' ∧ f i ⁻¹' s' = setsΩ i) ⋯

Tactic:
(h_meas i hi_mem).choose_spec.2.symm

Premises used: Exists.choose_spec, And.right, Eq.symm
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
ι : Type u_8
β : ι → Type u_9
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
h :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)} (_H : ∀ i ∈ S, MeasurableSet (sets i)),
    ∀ᵐ (a : α) ∂μ,
      Eq (α := ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ i ∈ S, f i ⁻¹' sets i) : ENNReal)
        (∏ i ∈ S, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f i ⁻¹' sets i) : ENNReal)
S : Finset ι
setsΩ : ι → Set Ω
h_meas :
  ∀ i ∈ S, Membership.mem (γ := Set (Set Ω)) ((fun (x : ι) ↦ ({s : Set Ω | MeasurableSet s} : Set (Set Ω))) i) (setsΩ i)
setsβ : (i : ι) → Set (β i) :=
  fun (i : ι) ↦
    if hi_mem : i ∈ S then Exists.choose (p := fun (s' : Set (β i)) ↦ MeasurableSet s' ∧ f i ⁻¹' s' = setsΩ i) ⋯
    else univ
h_measβ : ∀ i ∈ S, MeasurableSet (setsβ i)
i : ι
hi_mem : i ∈ S
⊢ setsΩ i = f i ⁻¹' Exists.choose (p := fun (s' : Set (β i)) ↦ MeasurableSet s' ∧ f i ⁻¹' s' = setsΩ i) ⋯

Tactic:
exact (h_meas i hi_mem).choose_spec.2.symm

Premises used: Exists.choose_spec, And.right, Eq.symm
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
ι : Type u_8
β : ι → Type u_9
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
h :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)} (_H : ∀ i ∈ S, MeasurableSet (sets i)),
    ∀ᵐ (a : α) ∂μ,
      Eq (α := ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ i ∈ S, f i ⁻¹' sets i) : ENNReal)
        (∏ i ∈ S, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f i ⁻¹' sets i) : ENNReal)
S : Finset ι
setsΩ : ι → Set Ω
h_meas :
  ∀ i ∈ S, Membership.mem (γ := Set (Set Ω)) ((fun (x : ι) ↦ ({s : Set Ω | MeasurableSet s} : Set (Set Ω))) i) (setsΩ i)
setsβ : (i : ι) → Set (β i) :=
  fun (i : ι) ↦
    if hi_mem : i ∈ S then Exists.choose (p := fun (s' : Set (β i)) ↦ MeasurableSet s' ∧ f i ⁻¹' s' = setsΩ i) ⋯
    else univ
h_measβ : ∀ i ∈ S, MeasurableSet (setsβ i)
⊢ ∀ i ∈ S, setsΩ i = f i ⁻¹' setsβ i

Tactic:
have h_preim : ∀ i ∈ S, setsΩ i = f i ⁻¹' setsβ i := by
    intro i hi_mem
    simp_rw [setsβ, dif_pos hi_mem]
    exact (h_meas i hi_mem).choose_spec.2.symm
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
ι : Type u_8
β : ι → Type u_9
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
h :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)} (_H : ∀ i ∈ S, MeasurableSet (sets i)),
    ∀ᵐ (a : α) ∂μ,
      Eq (α := ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ i ∈ S, f i ⁻¹' sets i) : ENNReal)
        (∏ i ∈ S, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f i ⁻¹' sets i) : ENNReal)
S : Finset ι
setsΩ : ι → Set Ω
h_meas :
  ∀ i ∈ S, Membership.mem (γ := Set (Set Ω)) ((fun (x : ι) ↦ ({s : Set Ω | MeasurableSet s} : Set (Set Ω))) i) (setsΩ i)
setsβ : (i : ι) → Set (β i) :=
  fun (i : ι) ↦
    if hi_mem : i ∈ S then Exists.choose (p := fun (s' : Set (β i)) ↦ MeasurableSet s' ∧ f i ⁻¹' s' = setsΩ i) ⋯
    else univ
h_measβ : ∀ i ∈ S, MeasurableSet (setsβ i)
h_preim : ∀ i ∈ S, setsΩ i = f i ⁻¹' setsβ i
⊢ ∀ᵐ (a : α) ∂μ,
    Eq (α := ENNReal) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ i ∈ S, setsΩ i) : ENNReal)
      (∏ i ∈ S, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (setsΩ i) : ENNReal)

Tactic:
simp_all
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
ι : Type u_8
β : ι → Type u_9
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
h :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)} (_H : ∀ i ∈ S, MeasurableSet (sets i)),
    ∀ᵐ (a : α) ∂μ,
      Eq (α := ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ i ∈ S, f i ⁻¹' sets i) : ENNReal)
        (∏ i ∈ S, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f i ⁻¹' sets i) : ENNReal)
S : Finset ι
setsΩ : ι → Set Ω
h_meas :
  ∀ i ∈ S, Membership.mem (γ := Set (Set Ω)) ((fun (x : ι) ↦ ({s : Set Ω | MeasurableSet s} : Set (Set Ω))) i) (setsΩ i)
let let₁ let₂ :
  ∀ᵐ (a : α) ∂μ,
    Eq (α := ENNReal) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ i ∈ S, setsΩ i) : ENNReal)
      (∏ i ∈ S, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (setsΩ i) : ENNReal)
let₃ :
  let setsβ : (i : ι) → Set (β i) := fun (i : ι) ↦
    if hi_mem : i ∈ S then Exists.choose (p := fun (s' : Set (β i)) ↦ MeasurableSet s' ∧ f i ⁻¹' s' = setsΩ i) ⋯
    else univ;
  ∀ (h_measβ : ∀ i ∈ S, MeasurableSet (setsβ i)),
    ∀ᵐ (a : α) ∂μ,
      Eq (α := ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ i ∈ S, setsΩ i) : ENNReal)
        (∏ i ∈ S, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (setsΩ i) : ENNReal)
let₄ :
  let setsβ : (i : ι) → Set (β i) := fun (i : ι) ↦
    if hi_mem : i ∈ S then Exists.choose (p := fun (s' : Set (β i)) ↦ MeasurableSet s' ∧ f i ⁻¹' s' = setsΩ i) ⋯
    else univ;
  ∀ (h_measβ : ∀ i ∈ S, MeasurableSet (setsβ i)) (h_preim : ∀ i ∈ S, setsΩ i = f i ⁻¹' setsβ i),
    ∀ᵐ (a : α) ∂μ,
      Eq (α := ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ i ∈ S, setsΩ i) : ENNReal)
        (∏ i ∈ S, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (setsΩ i) : ENNReal)
⊢ ∀ᵐ (a : α) ∂μ,
    Eq (α := ENNReal) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ i ∈ S, setsΩ i) : ENNReal)
      (∏ i ∈ S, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (setsΩ i) : ENNReal)

Tactic:
classical
  let setsβ : ∀ i : ι, Set (β i) := fun i =>
    dite (i ∈ S) (fun hi_mem => (h_meas i hi_mem).choose) fun _ => Set.univ
  have h_measβ : ∀ i ∈ S, MeasurableSet[m i] (setsβ i) := by
    intro i hi_mem
    simp_rw [setsβ, dif_pos hi_mem]
    exact (h_meas i hi_mem).choose_spec.1
  have h_preim : ∀ i ∈ S, setsΩ i = f i ⁻¹' setsβ i := by
    intro i hi_mem
    simp_rw [setsβ, dif_pos hi_mem]
    exact (h_meas i hi_mem).choose_spec.2.symm
  simp_all
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
mβ : (i : ι) → MeasurableSpace (β i)
f g : (i : ι) → Ω → β i
hf : iIndepFun (β := β) f κ μ
h : ∀ (i : ι), ∀ᵐ (a : α) ∂μ, f i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] g i
rw :
  ∀
    (hf :
      ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)} (_H : ∀ i ∈ S, MeasurableSet (sets i)),
        ∀ᵐ (a : α) ∂μ,
          Eq (α := ENNReal)
            ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ i ∈ S, f i ⁻¹' sets i) : ENNReal)
            (∏ i ∈ S, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f i ⁻¹' sets i) : ENNReal))
    (h : ∀ (i : ι), ∀ᵐ (a : α) ∂μ, f i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] g i)
    (S : Finset ι) {sets : (i : ι) → Set (β i)} (_H : ∀ i ∈ S, MeasurableSet (sets i)),
    ∀ᵐ (a : α) ∂μ,
      Eq (α := ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ i ∈ S, g i ⁻¹' sets i) : ENNReal)
        (∏ i ∈ S, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (g i ⁻¹' sets i) : ENNReal)
⊢ iIndepFun (β := β) g κ μ

Tactic:
rw [iIndepFun_iff_measure_inter_preimage_eq_mul] at hf ⊢

Premises used: ProbabilityTheory.Kernel.iIndepFun_iff_measure_inter_preimage_eq_mul
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
mβ : (i : ι) → MeasurableSpace (β i)
f g : (i : ι) → Ω → β i
hf :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)} (_H : ∀ i ∈ S, MeasurableSet (sets i)),
    ∀ᵐ (a : α) ∂μ,
      Eq (α := ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ i ∈ S, f i ⁻¹' sets i) : ENNReal)
        (∏ i ∈ S, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f i ⁻¹' sets i) : ENNReal)
h : ∀ (i : ι), ∀ᵐ (a : α) ∂μ, f i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] g i
S : Finset ι
sets : (i : ι) → Set (β i)
hmeas : ∀ i ∈ S, MeasurableSet (sets i)
⊢ ∀ᵐ (a : α) ∂μ, ∀ i ∈ S, f i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] g i

Tactic:
have : ∀ᵐ a ∂μ, ∀ i ∈ S, f i =ᵐ[κ a] g i :=
    (ae_ball_iff (Finset.countable_toSet S)).2 (fun i hi ↦ h i)
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
mβ : (i : ι) → MeasurableSpace (β i)
f g : (i : ι) → Ω → β i
hf :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)} (_H : ∀ i ∈ S, MeasurableSet (sets i)),
    ∀ᵐ (a : α) ∂μ,
      Eq (α := ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ i ∈ S, f i ⁻¹' sets i) : ENNReal)
        (∏ i ∈ S, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f i ⁻¹' sets i) : ENNReal)
h : ∀ (i : ι), ∀ᵐ (a : α) ∂μ, f i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] g i
S : Finset ι
sets : (i : ι) → Set (β i)
hmeas : ∀ i ∈ S, MeasurableSet (sets i)
this : ∀ᵐ (a : α) ∂μ, ∀ i ∈ S, f i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] g i
h₁ :
  ∀ (a : α) (ha : ∀ i ∈ S, f i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] g i)
    (h'a :
      Eq (α := ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ i ∈ S, f i ⁻¹' sets i) : ENNReal)
        (∏ i ∈ S, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f i ⁻¹' sets i) : ENNReal)),
    Eq (α := ENNReal)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ i ∈ S, g i ⁻¹' sets i) : ENNReal)
      (∏ i ∈ S, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (g i ⁻¹' sets i) : ENNReal)
⊢ ∀ᵐ (a : α) ∂μ,
    Eq (α := ENNReal)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ i ∈ S, g i ⁻¹' sets i) : ENNReal)
      (∏ i ∈ S, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (g i ⁻¹' sets i) : ENNReal)

Tactic:
filter_upwards [this, hf S hmeas] with a ha h'a
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
mβ : (i : ι) → MeasurableSpace (β i)
f g : (i : ι) → Ω → β i
hf :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)} (_H : ∀ i ∈ S, MeasurableSet (sets i)),
    ∀ᵐ (a : α) ∂μ,
      Eq (α := ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ i ∈ S, f i ⁻¹' sets i) : ENNReal)
        (∏ i ∈ S, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f i ⁻¹' sets i) : ENNReal)
h : ∀ (i : ι), ∀ᵐ (a : α) ∂μ, f i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] g i
S : Finset ι
sets : (i : ι) → Set (β i)
hmeas : ∀ i ∈ S, MeasurableSet (sets i)
this : ∀ᵐ (a : α) ∂μ, ∀ i ∈ S, f i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] g i
a : α
ha : ∀ i ∈ S, f i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] g i
h'a :
  Eq (α := ENNReal)
    ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ i ∈ S, f i ⁻¹' sets i) : ENNReal)
    (∏ i ∈ S, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f i ⁻¹' sets i) : ENNReal)
i : ι
hi : i ∈ S
H : g i ⁻¹' sets i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] f i ⁻¹' sets i
⊢ Eq (α := ENNReal) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (g i ⁻¹' sets i) : ENNReal)
    ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f i ⁻¹' sets i) : ENNReal)

Tactic:
apply measure_congr

Premises used: MeasureTheory.measure_congr
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
mβ : (i : ι) → MeasurableSpace (β i)
f g : (i : ι) → Ω → β i
hf :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)} (_H : ∀ i ∈ S, MeasurableSet (sets i)),
    ∀ᵐ (a : α) ∂μ,
      Eq (α := ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ i ∈ S, f i ⁻¹' sets i) : ENNReal)
        (∏ i ∈ S, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f i ⁻¹' sets i) : ENNReal)
h : ∀ (i : ι), ∀ᵐ (a : α) ∂μ, f i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] g i
S : Finset ι
sets : (i : ι) → Set (β i)
hmeas : ∀ i ∈ S, MeasurableSet (sets i)
this : ∀ᵐ (a : α) ∂μ, ∀ i ∈ S, f i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] g i
a : α
ha : ∀ i ∈ S, f i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] g i
h'a :
  Eq (α := ENNReal)
    ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ i ∈ S, f i ⁻¹' sets i) : ENNReal)
    (∏ i ∈ S, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f i ⁻¹' sets i) : ENNReal)
i : ι
hi : i ∈ S
h₁ : ∀ (ω : Ω) (hω : f i ω = g i ω), (g i ⁻¹' sets i) ω = (f i ⁻¹' sets i) ω
⊢ g i ⁻¹' sets i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] f i ⁻¹' sets i

Tactic:
filter_upwards [ha i hi] with ω hω
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
mβ : (i : ι) → MeasurableSpace (β i)
f g : (i : ι) → Ω → β i
hf :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)} (_H : ∀ i ∈ S, MeasurableSet (sets i)),
    ∀ᵐ (a : α) ∂μ,
      Eq (α := ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ i ∈ S, f i ⁻¹' sets i) : ENNReal)
        (∏ i ∈ S, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f i ⁻¹' sets i) : ENNReal)
h : ∀ (i : ι), ∀ᵐ (a : α) ∂μ, f i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] g i
S : Finset ι
sets : (i : ι) → Set (β i)
hmeas : ∀ i ∈ S, MeasurableSet (sets i)
this : ∀ᵐ (a : α) ∂μ, ∀ i ∈ S, f i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] g i
a : α
ha : ∀ i ∈ S, f i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] g i
h'a :
  Eq (α := ENNReal)
    ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ i ∈ S, f i ⁻¹' sets i) : ENNReal)
    (∏ i ∈ S, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f i ⁻¹' sets i) : ENNReal)
i : ι
hi : i ∈ S
ω : Ω
hω : f i ω = g i ω
⊢ (g i ω ∈ sets i) = (f i ω ∈ sets i)

Tactic:
simp [hω]