-- Mathlib/Probability/Independence/Conditional.lean
theorem condIndepFun_iff_condExp_inter_preimage_eq_mul {mβ : MeasurableSpace β}
    {mβ' : MeasurableSpace β'} (hf : Measurable f) (hg : Measurable g) :
    CondIndepFun m' hm' f g μ ↔
      ∀ s t, MeasurableSet s → MeasurableSet t
        → (μ⟦f ⁻¹' s ∩ g ⁻¹' t | m'⟧) =ᵐ[μ] fun ω ↦ (μ⟦f ⁻¹' s | m'⟧) ω * (μ⟦g ⁻¹' t | m'⟧) ω

Proof state:
case refine_2
Ω : Type u_1
β : Type u_3
β' : Type u_4
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
hf : Measurable f
hg : Measurable g
h :
  ∀ (s : Set β) (t : Set β'),
    MeasurableSet s →
      MeasurableSet t →
        μ[(f ⁻¹' s ∩ g ⁻¹' t).indicator fun ω => 1|m'] =ᶠ[ae μ] fun ω =>
          (μ[(f ⁻¹' s).indicator fun ω => 1|m']) ω * (μ[(g ⁻¹' t).indicator fun ω => 1|m']) ω
s t : Set Ω
⊢ MeasurableSet s →
    MeasurableSet t →
      μ[(s ∩ t).indicator fun ω => 1|m'] =ᶠ[ae μ] μ[s.indicator fun ω => 1|m'] * μ[t.indicator fun ω => 1|m']

Tactic:
rintro ⟨s, hs, rfl⟩ ⟨t, ht, rfl⟩

Result:
case refine_2.intro.intro.intro.intro
Ω : Type u_1
β : Type u_3
β' : Type u_4
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
hf : Measurable f
hg : Measurable g
h :
  ∀ (s : Set β) (t : Set β'),
    MeasurableSet s →
      MeasurableSet t →
        μ[(f ⁻¹' s ∩ g ⁻¹' t).indicator fun ω => 1|m'] =ᶠ[ae μ] fun ω =>
          (μ[(f ⁻¹' s).indicator fun ω => 1|m']) ω * (μ[(g ⁻¹' t).indicator fun ω => 1|m']) ω
s : Set β
hs : MeasurableSet s
t : Set β'
ht : MeasurableSet t
⊢ μ[(f ⁻¹' s ∩ g ⁻¹' t).indicator fun ω => 1|m'] =ᶠ[ae μ]
    μ[(f ⁻¹' s).indicator fun ω => 1|m'] * μ[(g ⁻¹' t).indicator fun ω => 1|m']

Proof state:
case refine_2.intro.intro.intro.intro
Ω : Type u_1
β : Type u_3
β' : Type u_4
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
hf : Measurable f
hg : Measurable g
h :
  ∀ (s : Set β) (t : Set β'),
    MeasurableSet s →
      MeasurableSet t →
        μ[(f ⁻¹' s ∩ g ⁻¹' t).indicator fun ω => 1|m'] =ᶠ[ae μ] fun ω =>
          (μ[(f ⁻¹' s).indicator fun ω => 1|m']) ω * (μ[(g ⁻¹' t).indicator fun ω => 1|m']) ω
s : Set β
hs : MeasurableSet s
t : Set β'
ht : MeasurableSet t
⊢ μ[(f ⁻¹' s ∩ g ⁻¹' t).indicator fun ω => 1|m'] =ᶠ[ae μ]
    μ[(f ⁻¹' s).indicator fun ω => 1|m'] * μ[(g ⁻¹' t).indicator fun ω => 1|m']

Tactic:
exact h s t hs ht

Result:
no goals

Proof state:
case refine_1
Ω : Type u_1
β : Type u_3
β' : Type u_4
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
hf : Measurable f
hg : Measurable g
h :
  ∀ (t1 t2 : Set Ω),
    MeasurableSet t1 →
      MeasurableSet t2 →
        μ[(t1 ∩ t2).indicator fun ω => 1|m'] =ᶠ[ae μ] μ[t1.indicator fun ω => 1|m'] * μ[t2.indicator fun ω => 1|m']
s : Set β
t : Set β'
hs : MeasurableSet s
ht : MeasurableSet t
⊢ μ[(f ⁻¹' s ∩ g ⁻¹' t).indicator fun ω => 1|m'] =ᶠ[ae μ] fun ω =>
    (μ[(f ⁻¹' s).indicator fun ω => 1|m']) ω * (μ[(g ⁻¹' t).indicator fun ω => 1|m']) ω

Tactic:
exact h (f ⁻¹' s) (g ⁻¹' t) ⟨s, hs, rfl⟩ ⟨t, ht, rfl⟩

Result:
no goals

Proof state:
Ω : Type u_1
β : Type u_3
β' : Type u_4
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
hf : Measurable f
hg : Measurable g
⊢ (∀ (t1 t2 : Set Ω),
      MeasurableSet t1 →
        MeasurableSet t2 →
          μ[(t1 ∩ t2).indicator fun ω => 1|m'] =ᶠ[ae μ] μ[t1.indicator fun ω => 1|m'] * μ[t2.indicator fun ω => 1|m']) ↔
    ∀ (s : Set β) (t : Set β'),
      MeasurableSet s →
        MeasurableSet t →
          μ[(f ⁻¹' s ∩ g ⁻¹' t).indicator fun ω => 1|m'] =ᶠ[ae μ] fun ω =>
            (μ[(f ⁻¹' s).indicator fun ω => 1|m']) ω * (μ[(g ⁻¹' t).indicator fun ω => 1|m']) ω

Tactic:
refine ⟨fun h s t hs ht ↦ ?_, fun h s t ↦ ?_⟩

Result:
case refine_1
Ω : Type u_1
β : Type u_3
β' : Type u_4
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
hf : Measurable f
hg : Measurable g
h :
  ∀ (t1 t2 : Set Ω),
    MeasurableSet t1 →
      MeasurableSet t2 →
        μ[(t1 ∩ t2).indicator fun ω => 1|m'] =ᶠ[ae μ] μ[t1.indicator fun ω => 1|m'] * μ[t2.indicator fun ω => 1|m']
s : Set β
t : Set β'
hs : MeasurableSet s
ht : MeasurableSet t
⊢ μ[(f ⁻¹' s ∩ g ⁻¹' t).indicator fun ω => 1|m'] =ᶠ[ae μ] fun ω =>
    (μ[(f ⁻¹' s).indicator fun ω => 1|m']) ω * (μ[(g ⁻¹' t).indicator fun ω => 1|m']) ω

case refine_2
Ω : Type u_1
β : Type u_3
β' : Type u_4
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
hf : Measurable f
hg : Measurable g
h :
  ∀ (s : Set β) (t : Set β'),
    MeasurableSet s →
      MeasurableSet t →
        μ[(f ⁻¹' s ∩ g ⁻¹' t).indicator fun ω => 1|m'] =ᶠ[ae μ] fun ω =>
          (μ[(f ⁻¹' s).indicator fun ω => 1|m']) ω * (μ[(g ⁻¹' t).indicator fun ω => 1|m']) ω
s t : Set Ω
⊢ MeasurableSet s →
    MeasurableSet t →
      μ[(s ∩ t).indicator fun ω => 1|m'] =ᶠ[ae μ] μ[s.indicator fun ω => 1|m'] * μ[t.indicator fun ω => 1|m']

Proof state:
Ω : Type u_1
β : Type u_3
β' : Type u_4
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
hf : Measurable f
hg : Measurable g
⊢ CondIndepFun m' hm' f g μ ↔
    ∀ (s : Set β) (t : Set β'),
      MeasurableSet s →
        MeasurableSet t →
          μ[(f ⁻¹' s ∩ g ⁻¹' t).indicator fun ω => 1|m'] =ᶠ[ae μ] fun ω =>
            (μ[(f ⁻¹' s).indicator fun ω => 1|m']) ω * (μ[(g ⁻¹' t).indicator fun ω => 1|m']) ω

Tactic:
rw [condIndepFun_iff _ _ _ _ hf hg]

Result:
Ω : Type u_1
β : Type u_3
β' : Type u_4
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
hf : Measurable f
hg : Measurable g
⊢ (∀ (t1 t2 : Set Ω),
      MeasurableSet t1 →
        MeasurableSet t2 →
          μ[(t1 ∩ t2).indicator fun ω => 1|m'] =ᶠ[ae μ] μ[t1.indicator fun ω => 1|m'] * μ[t2.indicator fun ω => 1|m']) ↔
    ∀ (s : Set β) (t : Set β'),
      MeasurableSet s →
        MeasurableSet t →
          μ[(f ⁻¹' s ∩ g ⁻¹' t).indicator fun ω => 1|m'] =ᶠ[ae μ] fun ω =>
            (μ[(f ⁻¹' s).indicator fun ω => 1|m']) ω * (μ[(g ⁻¹' t).indicator fun ω => 1|m']) ω