Event and complementary event marginal laws imply independent event indicator

import Mathlib.Probability.Independence.Basic
import Mathlib.MeasureTheory.Measure.Restrict

open MeasureTheory ProbabilityTheory Set

theorem AvramDividend.Classical.indicator_indepFun_of_both_event_marginals
    {Ω β : Type*} [MeasurableSpace Ω] [MeasurableSpace β]
    {P : Measure Ω} [IsProbabilityMeasure P]
    (A : Set Ω) (Y : Ω → β)
    (hA : MeasurableSet A) (hY : Measurable Y)
    (hFirst : ∀ B : Set β, MeasurableSet B →
      P (A ∩ Y ⁻¹' B) = P A * P (Y ⁻¹' B))
    (hSecond : ∀ B : Set β, MeasurableSet B →
      P (Aᶜ ∩ Y ⁻¹' B) = P Aᶜ * P (Y ⁻¹' B)) :
    IndepFun (Set.indicator A (fun _ : Ω => (1 : ℝ))) Y P := by
  sorry