-- Mathlib/Probability/Independence/Conditional.lean
theorem iCondIndepFun_iff_condExp_inter_preimage_eq_mul {β : ι → Type*}
    (m : ∀ x, MeasurableSpace (β x)) (f : ∀ i, Ω → β i) (hf : ∀ i, Measurable (f i)) :
    iCondIndepFun m' hm' m f μ ↔
      ∀ (S : Finset ι) {sets : ∀ i : ι, Set (β i)} (_H : ∀ i, i ∈ S → MeasurableSet[m i] (sets i)),
        (μ⟦⋂ i ∈ S, f i ⁻¹' sets i| m'⟧) =ᵐ[μ] ∏ i ∈ S, (μ⟦f i ⁻¹' sets i | m'⟧)

Proof state:
case refine_1
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
β : ι → Type u_5
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
hf : ∀ (i : ι), Measurable (f i)
h :
  ∀ (s : Finset ι) {g : ι → Set Ω},
    (∀ i ∈ s, MeasurableSet (g i)) →
      μ[(⋂ i ∈ s, g i).indicator fun ω => 1|m'] =ᶠ[ae μ] ∏ i ∈ s, μ[(g i).indicator fun ω => 1|m']
s : Finset ι
sets : (i : ι) → Set (β i)
h_sets : ∀ i ∈ s, MeasurableSet (sets i)
i : ι
hi : i ∈ s
⊢ MeasurableSet ((fun i => f i ⁻¹' sets i) i)

Tactic:
exact ⟨sets i, h_sets i hi, rfl⟩

Result:
no goals

Proof state:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
β : ι → Type u_5
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
hf : ∀ (i : ι), Measurable (f i)
s : Finset ι
sets : ι → Set Ω
h_sets : ∀ i ∈ s, MeasurableSet (sets i)
g : (i : ι) → Set (β i) := fun i => if hi : i ∈ s then Exists.choose ⋯ else Set.univ
h : μ[(⋂ i ∈ s, f i ⁻¹' g i).indicator fun ω => 1|m'] =ᶠ[ae μ] ∏ i ∈ s, μ[(f i ⁻¹' g i).indicator fun ω => 1|m']
i : ι
hi : i ∈ s
⊢ sets i = f i ⁻¹' g i

Tactic:
rw [(h_sets i hi).choose_spec.2.symm]

Result:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
β : ι → Type u_5
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
hf : ∀ (i : ι), Measurable (f i)
s : Finset ι
sets : ι → Set Ω
h_sets : ∀ i ∈ s, MeasurableSet (sets i)
g : (i : ι) → Set (β i) := fun i => if hi : i ∈ s then Exists.choose ⋯ else Set.univ
h : μ[(⋂ i ∈ s, f i ⁻¹' g i).indicator fun ω => 1|m'] =ᶠ[ae μ] ∏ i ∈ s, μ[(f i ⁻¹' g i).indicator fun ω => 1|m']
i : ι
hi : i ∈ s
⊢ f i ⁻¹' Exists.choose ⋯ = f i ⁻¹' g i

Proof state:
case refine_2
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
β : ι → Type u_5
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
hf : ∀ (i : ι), Measurable (f i)
h :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)},
    (∀ i ∈ S, MeasurableSet (sets i)) →
      μ[(⋂ i ∈ S, f i ⁻¹' sets i).indicator fun ω => 1|m'] =ᶠ[ae μ] ∏ i ∈ S, μ[(f i ⁻¹' sets i).indicator fun ω => 1|m']
s : Finset ι
sets : ι → Set Ω
h_sets : ∀ i ∈ s, MeasurableSet (sets i)
⊢ μ[(⋂ i ∈ s, sets i).indicator fun ω => 1|m'] =ᶠ[ae μ] ∏ i ∈ s, μ[(sets i).indicator fun ω => 1|m']

Tactic:
let g := fun i ↦ if hi : i ∈ s then (h_sets i hi).choose else Set.univ

Result:
case refine_2
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
β : ι → Type u_5
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
hf : ∀ (i : ι), Measurable (f i)
h :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)},
    (∀ i ∈ S, MeasurableSet (sets i)) →
      μ[(⋂ i ∈ S, f i ⁻¹' sets i).indicator fun ω => 1|m'] =ᶠ[ae μ] ∏ i ∈ S, μ[(f i ⁻¹' sets i).indicator fun ω => 1|m']
s : Finset ι
sets : ι → Set Ω
h_sets : ∀ i ∈ s, MeasurableSet (sets i)
g : (i : ι) → Set (β i) := fun i => if hi : i ∈ s then Exists.choose ⋯ else Set.univ
⊢ μ[(⋂ i ∈ s, sets i).indicator fun ω => 1|m'] =ᶠ[ae μ] ∏ i ∈ s, μ[(sets i).indicator fun ω => 1|m']

Proof state:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
β : ι → Type u_5
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
hf : ∀ (i : ι), Measurable (f i)
⊢ (∀ (s : Finset ι) {g : ι → Set Ω},
      (∀ i ∈ s, MeasurableSet (g i)) →
        μ[(⋂ i ∈ s, g i).indicator fun ω => 1|m'] =ᶠ[ae μ] ∏ i ∈ s, μ[(g i).indicator fun ω => 1|m']) ↔
    ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)},
      (∀ i ∈ S, MeasurableSet (sets i)) →
        μ[(⋂ i ∈ S, f i ⁻¹' sets i).indicator fun ω => 1|m'] =ᶠ[ae μ]
          ∏ i ∈ S, μ[(f i ⁻¹' sets i).indicator fun ω => 1|m']

Tactic:
refine ⟨fun h s sets h_sets ↦ ?_, fun h s sets h_sets ↦ ?_⟩

Result:
case refine_1
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
β : ι → Type u_5
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
hf : ∀ (i : ι), Measurable (f i)
h :
  ∀ (s : Finset ι) {g : ι → Set Ω},
    (∀ i ∈ s, MeasurableSet (g i)) →
      μ[(⋂ i ∈ s, g i).indicator fun ω => 1|m'] =ᶠ[ae μ] ∏ i ∈ s, μ[(g i).indicator fun ω => 1|m']
s : Finset ι
sets : (i : ι) → Set (β i)
h_sets : ∀ i ∈ s, MeasurableSet (sets i)
⊢ μ[(⋂ i ∈ s, f i ⁻¹' sets i).indicator fun ω => 1|m'] =ᶠ[ae μ] ∏ i ∈ s, μ[(f i ⁻¹' sets i).indicator fun ω => 1|m']

case refine_2
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
β : ι → Type u_5
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
hf : ∀ (i : ι), Measurable (f i)
h :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)},
    (∀ i ∈ S, MeasurableSet (sets i)) →
      μ[(⋂ i ∈ S, f i ⁻¹' sets i).indicator fun ω => 1|m'] =ᶠ[ae μ] ∏ i ∈ S, μ[(f i ⁻¹' sets i).indicator fun ω => 1|m']
s : Finset ι
sets : ι → Set Ω
h_sets : ∀ i ∈ s, MeasurableSet (sets i)
⊢ μ[(⋂ i ∈ s, sets i).indicator fun ω => 1|m'] =ᶠ[ae μ] ∏ i ∈ s, μ[(sets i).indicator fun ω => 1|m']

Proof state:
case refine_2
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
β : ι → Type u_5
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
hf : ∀ (i : ι), Measurable (f i)
h :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)},
    (∀ i ∈ S, MeasurableSet (sets i)) →
      μ[(⋂ i ∈ S, f i ⁻¹' sets i).indicator fun ω => 1|m'] =ᶠ[ae μ] ∏ i ∈ S, μ[(f i ⁻¹' sets i).indicator fun ω => 1|m']
s : Finset ι
sets : ι → Set Ω
h_sets : ∀ i ∈ s, MeasurableSet (sets i)
g : (i : ι) → Set (β i) := fun i => if hi : i ∈ s then Exists.choose ⋯ else Set.univ
⊢ μ[(⋂ i ∈ s, sets i).indicator fun ω => 1|m'] =ᶠ[ae μ] ∏ i ∈ s, μ[(sets i).indicator fun ω => 1|m']

Tactic:
specialize h s (sets := g) (fun i hi ↦ ?_)

Result:
case refine_2
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
β : ι → Type u_5
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
hf : ∀ (i : ι), Measurable (f i)
h :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)},
    (∀ i ∈ S, MeasurableSet (sets i)) →
      μ[(⋂ i ∈ S, f i ⁻¹' sets i).indicator fun ω => 1|m'] =ᶠ[ae μ] ∏ i ∈ S, μ[(f i ⁻¹' sets i).indicator fun ω => 1|m']
s : Finset ι
sets : ι → Set Ω
h_sets : ∀ i ∈ s, MeasurableSet (sets i)
g : (i : ι) → Set (β i) := fun i => if hi : i ∈ s then Exists.choose ⋯ else Set.univ
i : ι
hi : i ∈ s
⊢ MeasurableSet (g i)

case refine_2
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
β : ι → Type u_5
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
hf : ∀ (i : ι), Measurable (f i)
s : Finset ι
sets : ι → Set Ω
h_sets : ∀ i ∈ s, MeasurableSet (sets i)
g : (i : ι) → Set (β i) := fun i => if hi : i ∈ s then Exists.choose ⋯ else Set.univ
h : μ[(⋂ i ∈ s, f i ⁻¹' g i).indicator fun ω => 1|m'] =ᶠ[ae μ] ∏ i ∈ s, μ[(f i ⁻¹' g i).indicator fun ω => 1|m']
⊢ μ[(⋂ i ∈ s, sets i).indicator fun ω => 1|m'] =ᶠ[ae μ] ∏ i ∈ s, μ[(sets i).indicator fun ω => 1|m']