-- Mathlib/Probability/Independence/Kernel.lean
theorem iIndepFun_iff_measure_inter_preimage_eq_mul {ι : Type*} {β : ι → Type*}
    (m : ∀ x, MeasurableSpace (β x)) (f : ∀ i, Ω → β i) :
    iIndepFun m f κ μ ↔
      ∀ (S : Finset ι) {sets : ∀ i : ι, Set (β i)} (_H : ∀ i, i ∈ S → MeasurableSet[m i] (sets i)),
        ∀ᵐ a ∂μ, κ a (⋂ i ∈ S, (f i) ⁻¹' (sets i)) = ∏ i ∈ S, κ a ((f i) ⁻¹' (sets i))

Proof state:
α : 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)},
    (∀ i ∈ S, MeasurableSet (sets i)) → ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ S, f i ⁻¹' sets i) = ∏ i ∈ S, (κ a) (f i ⁻¹' sets i)
S : Finset ι
setsΩ : ι → Set Ω
h_meas : ∀ i ∈ S, setsΩ i ∈ (fun x => {s | MeasurableSet s}) i
setsβ : (i : ι) → Set (β i) := fun i => if hi_mem : i ∈ S then Exists.choose ⋯ else univ
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ S, setsΩ i) = ∏ i ∈ S, (κ a) (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

Result:
α : 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)},
    (∀ i ∈ S, MeasurableSet (sets i)) → ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ S, f i ⁻¹' sets i) = ∏ i ∈ S, (κ a) (f i ⁻¹' sets i)
S : Finset ι
setsΩ : ι → Set Ω
h_meas : ∀ i ∈ S, setsΩ i ∈ (fun x => {s | MeasurableSet s}) i
setsβ : (i : ι) → Set (β i) := fun i => if hi_mem : i ∈ S then Exists.choose ⋯ else univ
h_measβ : ∀ i ∈ S, MeasurableSet (setsβ i)
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ S, setsΩ i) = ∏ i ∈ S, (κ a) (setsΩ i)

Proof state:
α : 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
⊢ (∀ (S : Finset ι) {sets : (i : ι) → Set (β i)},
      (∀ i ∈ S, MeasurableSet (sets i)) →
        ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ S, f i ⁻¹' sets i) = ∏ i ∈ S, (κ a) (f i ⁻¹' sets i)) →
    iIndepFun m f κ μ

Tactic:
intro h S setsΩ h_meas

Result:
α : 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)},
    (∀ i ∈ S, MeasurableSet (sets i)) → ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ S, f i ⁻¹' sets i) = ∏ i ∈ S, (κ a) (f i ⁻¹' sets i)
S : Finset ι
setsΩ : ι → Set Ω
h_meas : ∀ i ∈ S, setsΩ i ∈ (fun x => {s | MeasurableSet s}) i
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ S, setsΩ i) = ∏ i ∈ S, (κ a) (setsΩ i)

Proof state:
α : 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)},
    (∀ i ∈ S, MeasurableSet (sets i)) → ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ S, f i ⁻¹' sets i) = ∏ i ∈ S, (κ a) (f i ⁻¹' sets i)
S : Finset ι
setsΩ : ι → Set Ω
h_meas : ∀ i ∈ S, setsΩ i ∈ (fun x => {s | MeasurableSet s}) i
setsβ : (i : ι) → Set (β i) := fun i => if hi_mem : i ∈ S then Exists.choose ⋯ else univ
h_measβ : ∀ i ∈ S, MeasurableSet (setsβ i)
i : ι
hi_mem : i ∈ S
⊢ setsΩ i = f i ⁻¹' setsβ i

Tactic:
simp_rw [setsβ, dif_pos hi_mem]

Result:
α : 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)},
    (∀ i ∈ S, MeasurableSet (sets i)) → ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ S, f i ⁻¹' sets i) = ∏ i ∈ S, (κ a) (f i ⁻¹' sets i)
S : Finset ι
setsΩ : ι → Set Ω
h_meas : ∀ i ∈ S, setsΩ i ∈ (fun x => {s | MeasurableSet s}) i
setsβ : (i : ι) → Set (β i) := fun i => if hi_mem : i ∈ S then Exists.choose ⋯ else univ
h_measβ : ∀ i ∈ S, MeasurableSet (setsβ i)
i : ι
hi_mem : i ∈ S
⊢ setsΩ i = f i ⁻¹' Exists.choose ⋯

Proof state:
α : 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)},
    (∀ i ∈ S, MeasurableSet (sets i)) → ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ S, f i ⁻¹' sets i) = ∏ i ∈ S, (κ a) (f i ⁻¹' sets i)
S : Finset ι
setsΩ : ι → Set Ω
h_meas : ∀ i ∈ S, setsΩ i ∈ (fun x => {s | MeasurableSet s}) i
setsβ : (i : ι) → Set (β i) := fun i => if hi_mem : i ∈ S then Exists.choose ⋯ else univ
h_measβ : ∀ i ∈ S, MeasurableSet (setsβ i)
h_preim : ∀ i ∈ S, setsΩ i = f i ⁻¹' setsβ i
h_left_eq : ∀ (a : α), (κ a) (⋂ i ∈ S, setsΩ i) = (κ a) (⋂ i ∈ S, f i ⁻¹' setsβ i)
h_right_eq : ∀ (a : α), ∏ i ∈ S, (κ a) (setsΩ i) = ∏ i ∈ S, (κ a) (f i ⁻¹' setsβ i)
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ S, setsΩ i) = ∏ i ∈ S, (κ a) (setsΩ i)

Tactic:
filter_upwards [h S h_measβ] with a ha

Result:
case h
α : 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)},
    (∀ i ∈ S, MeasurableSet (sets i)) → ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ S, f i ⁻¹' sets i) = ∏ i ∈ S, (κ a) (f i ⁻¹' sets i)
S : Finset ι
setsΩ : ι → Set Ω
h_meas : ∀ i ∈ S, setsΩ i ∈ (fun x => {s | MeasurableSet s}) i
setsβ : (i : ι) → Set (β i) := fun i => if hi_mem : i ∈ S then Exists.choose ⋯ else univ
h_measβ : ∀ i ∈ S, MeasurableSet (setsβ i)
h_preim : ∀ i ∈ S, setsΩ i = f i ⁻¹' setsβ i
h_left_eq : ∀ (a : α), (κ a) (⋂ i ∈ S, setsΩ i) = (κ a) (⋂ i ∈ S, f i ⁻¹' setsβ i)
h_right_eq : ∀ (a : α), ∏ i ∈ S, (κ a) (setsΩ i) = ∏ i ∈ S, (κ a) (f i ⁻¹' setsβ i)
a : α
ha : (κ a) (⋂ i ∈ S, f i ⁻¹' setsβ i) = ∏ i ∈ S, (κ a) (f i ⁻¹' setsβ i)
⊢ (κ a) (⋂ i ∈ S, setsΩ i) = ∏ i ∈ S, (κ a) (setsΩ i)

Proof state:
α : 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)},
    (∀ i ∈ S, MeasurableSet (sets i)) → ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ S, f i ⁻¹' sets i) = ∏ i ∈ S, (κ a) (f i ⁻¹' sets i)
S : Finset ι
setsΩ : ι → Set Ω
h_meas : ∀ i ∈ S, setsΩ i ∈ (fun x => {s | MeasurableSet s}) i
setsβ : (i : ι) → Set (β i) := fun i => if hi_mem : i ∈ S then Exists.choose ⋯ else univ
⊢ ∀ i ∈ S, MeasurableSet (setsβ i)

Tactic:
intro i hi_mem

Result:
α : 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)},
    (∀ i ∈ S, MeasurableSet (sets i)) → ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ S, f i ⁻¹' sets i) = ∏ i ∈ S, (κ a) (f i ⁻¹' sets i)
S : Finset ι
setsΩ : ι → Set Ω
h_meas : ∀ i ∈ S, setsΩ i ∈ (fun x => {s | MeasurableSet s}) i
setsβ : (i : ι) → Set (β i) := fun i => if hi_mem : i ∈ S then Exists.choose ⋯ else univ
i : ι
hi_mem : i ∈ S
⊢ MeasurableSet (setsβ i)