-- Mathlib/Probability/Integration.lean
theorem indepFun_iff_integral_comp_mul [IsFiniteMeasure μ] {β β' : Type*} {mβ : MeasurableSpace β}
    {mβ' : MeasurableSpace β'} {f : Ω → β} {g : Ω → β'} {hfm : Measurable f} {hgm : Measurable g} :
    IndepFun f g μ ↔ ∀ {φ : β → ℝ} {ψ : β' → ℝ}, Measurable φ → Measurable ψ →
      Integrable (φ ∘ f) μ → Integrable (ψ ∘ g) μ →
        integral μ (φ ∘ f * ψ ∘ g) = integral μ (φ ∘ f) * integral μ (ψ ∘ g)

Proof state:
case intro.intro.intro.intro
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
β : Type u_2
β' : Type u_3
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
f : Ω → β
g : Ω → β'
hfm : Measurable f
hgm : Measurable g
A : Set β
hA : MeasurableSet A
B : Set β'
hB : MeasurableSet B
h : integral μ (A.indicator 1 ∘ f * B.indicator 1 ∘ g) = integral μ (A.indicator 1 ∘ f) * integral μ (B.indicator 1 ∘ g)
⊢ μ (f ⁻¹' A ∩ g ⁻¹' B) = μ (f ⁻¹' A) * μ (g ⁻¹' B)

Tactic:
rwa [← ENNReal.toReal_eq_toReal (measure_ne_top μ _), ENNReal.toReal_mul, ←
  integral_indicator_one ((hfm hA).inter (hgm hB)), ← integral_indicator_one (hfm hA), ←
  integral_indicator_one (hgm hB), Set.inter_indicator_one]

Result:
case intro.intro.intro.intro
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
β : Type u_2
β' : Type u_3
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
f : Ω → β
g : Ω → β'
hfm : Measurable f
hgm : Measurable g
A : Set β
hA : MeasurableSet A
B : Set β'
hB : MeasurableSet B
h : integral μ (A.indicator 1 ∘ f * B.indicator 1 ∘ g) = integral μ (A.indicator 1 ∘ f) * integral μ (B.indicator 1 ∘ g)
⊢ μ (f ⁻¹' A) * μ (g ⁻¹' B) ≠ ⊤

Proof state:
case intro.intro.intro.intro
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
β : Type u_2
β' : Type u_3
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
f : Ω → β
g : Ω → β'
hfm : Measurable f
hgm : Measurable g
h :
  ∀ {φ : β → ℝ} {ψ : β' → ℝ},
    Measurable φ →
      Measurable ψ →
        Integrable (φ ∘ f) μ →
          Integrable (ψ ∘ g) μ → integral μ (φ ∘ f * ψ ∘ g) = integral μ (φ ∘ f) * integral μ (ψ ∘ g)
A : Set β
hA : MeasurableSet A
B : Set β'
hB : MeasurableSet B
⊢ μ (f ⁻¹' A ∩ g ⁻¹' B) = μ (f ⁻¹' A) * μ (g ⁻¹' B)

Tactic:
specialize
  h (measurable_one.indicator hA) (measurable_one.indicator hB)
    ((integrable_const 1).indicator (hfm.comp measurable_id hA))
    ((integrable_const 1).indicator (hgm.comp measurable_id hB))

Result:
case intro.intro.intro.intro
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
β : Type u_2
β' : Type u_3
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
f : Ω → β
g : Ω → β'
hfm : Measurable f
hgm : Measurable g
A : Set β
hA : MeasurableSet A
B : Set β'
hB : MeasurableSet B
h : integral μ (A.indicator 1 ∘ f * B.indicator 1 ∘ g) = integral μ (A.indicator 1 ∘ f) * integral μ (B.indicator 1 ∘ g)
⊢ μ (f ⁻¹' A ∩ g ⁻¹' B) = μ (f ⁻¹' A) * μ (g ⁻¹' B)

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
β : Type u_2
β' : Type u_3
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
f : Ω → β
g : Ω → β'
hfm : Measurable f
hgm : Measurable g
⊢ (∀ {φ : β → ℝ} {ψ : β' → ℝ},
      Measurable φ →
        Measurable ψ →
          Integrable (φ ∘ f) μ →
            Integrable (ψ ∘ g) μ → integral μ (φ ∘ f * ψ ∘ g) = integral μ (φ ∘ f) * integral μ (ψ ∘ g)) →
    ∀ (t1 t2 : Set Ω), MeasurableSet t1 → MeasurableSet t2 → μ (t1 ∩ t2) = μ t1 * μ t2

Tactic:
rintro h _ _ ⟨A, hA, rfl⟩ ⟨B, hB, rfl⟩

Result:
case intro.intro.intro.intro
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
β : Type u_2
β' : Type u_3
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
f : Ω → β
g : Ω → β'
hfm : Measurable f
hgm : Measurable g
h :
  ∀ {φ : β → ℝ} {ψ : β' → ℝ},
    Measurable φ →
      Measurable ψ →
        Integrable (φ ∘ f) μ →
          Integrable (ψ ∘ g) μ → integral μ (φ ∘ f * ψ ∘ g) = integral μ (φ ∘ f) * integral μ (ψ ∘ g)
A : Set β
hA : MeasurableSet A
B : Set β'
hB : MeasurableSet B
⊢ μ (f ⁻¹' A ∩ g ⁻¹' B) = μ (f ⁻¹' A) * μ (g ⁻¹' B)

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
β : Type u_2
β' : Type u_3
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
f : Ω → β
g : Ω → β'
hfm : Measurable f
hgm : Measurable g
⊢ IndepFun f g μ ↔
    ∀ {φ : β → ℝ} {ψ : β' → ℝ},
      Measurable φ →
        Measurable ψ →
          Integrable (φ ∘ f) μ →
            Integrable (ψ ∘ g) μ → integral μ (φ ∘ f * ψ ∘ g) = integral μ (φ ∘ f) * integral μ (ψ ∘ g)

Tactic:
refine ⟨fun hfg _ _ hφ hψ => IndepFun.integral_mul_of_integrable (hfg.comp hφ hψ), ?_⟩

Result:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
β : Type u_2
β' : Type u_3
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
f : Ω → β
g : Ω → β'
hfm : Measurable f
hgm : Measurable g
⊢ (∀ {φ : β → ℝ} {ψ : β' → ℝ},
      Measurable φ →
        Measurable ψ →
          Integrable (φ ∘ f) μ →
            Integrable (ψ ∘ g) μ → integral μ (φ ∘ f * ψ ∘ g) = integral μ (φ ∘ f) * integral μ (ψ ∘ g)) →
    IndepFun f g μ

Proof state:
case intro.intro.intro.intro
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
β : Type u_2
β' : Type u_3
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
f : Ω → β
g : Ω → β'
hfm : Measurable f
hgm : Measurable g
A : Set β
hA : MeasurableSet A
B : Set β'
hB : MeasurableSet B
h : integral μ (A.indicator 1 ∘ f * B.indicator 1 ∘ g) = integral μ (A.indicator 1 ∘ f) * integral μ (B.indicator 1 ∘ g)
⊢ μ (f ⁻¹' A) * μ (g ⁻¹' B) ≠ ⊤

Tactic:
exact ENNReal.mul_ne_top (measure_ne_top μ _) (measure_ne_top μ _)

Result:
no goals

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
β : Type u_2
β' : Type u_3
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
f : Ω → β
g : Ω → β'
hfm : Measurable f
hgm : Measurable g
⊢ (∀ {φ : β → ℝ} {ψ : β' → ℝ},
      Measurable φ →
        Measurable ψ →
          Integrable (φ ∘ f) μ →
            Integrable (ψ ∘ g) μ → integral μ (φ ∘ f * ψ ∘ g) = integral μ (φ ∘ f) * integral μ (ψ ∘ g)) →
    IndepFun f g μ

Tactic:
rw [IndepFun_iff]

Result:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
β : Type u_2
β' : Type u_3
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
f : Ω → β
g : Ω → β'
hfm : Measurable f
hgm : Measurable g
⊢ (∀ {φ : β → ℝ} {ψ : β' → ℝ},
      Measurable φ →
        Measurable ψ →
          Integrable (φ ∘ f) μ →
            Integrable (ψ ∘ g) μ → integral μ (φ ∘ f * ψ ∘ g) = integral μ (φ ∘ f) * integral μ (ψ ∘ g)) →
    ∀ (t1 t2 : Set Ω), MeasurableSet t1 → MeasurableSet t2 → μ (t1 ∩ t2) = μ t1 * μ t2