awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (goal)
Goal:
Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
β : Type u_3
γ : Type u_4
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : Ω → β
g : Ω → γ
hf : Measurable f
hg : Measurable g
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
rw :
  CondIndep m' (MeasurableSpace.comap f mβ) (MeasurableSpace.comap g mγ) hm' μ ↔
    ∀ (t1 t2 : Set Ω),
      MeasurableSet t1 →
        MeasurableSet t2 →
          μ[(t1 ∩ t2).indicator fun (ω : Ω) ↦ 1 | m'] =ᶠ[ae μ]
            HMul.hMul (α := Ω → ℝ) μ[t1.indicator fun (ω : Ω) ↦ 1 | m'] μ[t2.indicator fun (ω : Ω) ↦ 1 | m']
⊢ CondIndepFun m' hm' f g μ ↔
    ∀ (t1 t2 : Set Ω),
      MeasurableSet t1 →
        MeasurableSet t2 →
          μ[(t1 ∩ t2).indicator fun (ω : Ω) ↦ 1 | m'] =ᶠ[ae μ]
            HMul.hMul (α := Ω → ℝ) μ[t1.indicator fun (ω : Ω) ↦ 1 | m'] μ[t2.indicator fun (ω : Ω) ↦ 1 | m']
have rw₁ : (∀ (t1 t2 : Set Ω),
    MeasurableSet t1 →
      MeasurableSet t2 →
        μ[(t1 ∩ t2).indicator fun (ω : Ω) ↦ 1 | m'] =ᶠ[ae μ]
          HMul.hMul (α := Ω → ℝ) μ[t1.indicator fun (ω : Ω) ↦ 1 | m'] μ[t2.indicator fun (ω : Ω) ↦ 1 | m']) ↔
  ∀ (t1 t2 : Set Ω),
    MeasurableSet t1 →
      MeasurableSet t2 →
        μ[(t1 ∩ t2).indicator fun (ω : Ω) ↦ 1 | m'] =ᶠ[ae μ]
          HMul.hMul (α := Ω → ℝ) μ[t1.indicator fun (ω : Ω) ↦ 1 | m'] μ[t2.indicator fun (ω : Ω) ↦ 1 | m']
Tactic: rw [condIndepFun_iff_condIndep, condIndep_iff _ _ _ _ hf.comap_le hg.comap_le]
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (goal)
Goal:
Ω : Type u_1
β : Type u_3
β' : Type u_4
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : 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 →
          (ae μ).EventuallyEq (β := ℝ) μ[(f ⁻¹' s ∩ g ⁻¹' t).indicator fun (ω : Ω) ↦ 1 | m'] fun (ω : Ω) ↦
            HMul.hMul (α := ℝ) (μ[(f ⁻¹' s).indicator fun (ω : Ω) ↦ 1 | m'] ω)
              (μ[(g ⁻¹' t).indicator fun (ω : Ω) ↦ 1 | m'] ω)
have rw : (∀ (t1 t2 : Set Ω),
    MeasurableSet t1 →
      MeasurableSet t2 →
        μ[(t1 ∩ t2).indicator fun (ω : Ω) ↦ 1 | m'] =ᶠ[ae μ]
          HMul.hMul (α := Ω → ℝ) μ[t1.indicator fun (ω : Ω) ↦ 1 | m'] μ[t2.indicator fun (ω : Ω) ↦ 1 | m']) ↔
  ∀ (s : Set β) (t : Set β'),
    MeasurableSet s →
      MeasurableSet t →
        (ae μ).EventuallyEq (β := ℝ) μ[(f ⁻¹' s ∩ g ⁻¹' t).indicator fun (ω : Ω) ↦ 1 | m'] fun (ω : Ω) ↦
          HMul.hMul (α := ℝ) (μ[(f ⁻¹' s).indicator fun (ω : Ω) ↦ 1 | m'] ω)
            (μ[(g ⁻¹' t).indicator fun (ω : Ω) ↦ 1 | m'] ω)
Tactic: rw [condIndepFun_iff _ _ _ _ hf hg]
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (goal)
Goal:
Ω : Type u_1
β : Type u_3
β' : Type u_4
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : 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 μ]
            HMul.hMul (α := Ω → ℝ) μ[t1.indicator fun (ω : Ω) ↦ 1 | m'] μ[t2.indicator fun (ω : Ω) ↦ 1 | m']) ↔
    ∀ (s : Set β) (t : Set β'),
      MeasurableSet s →
        MeasurableSet t →
          (ae μ).EventuallyEq (β := ℝ) μ[(f ⁻¹' s ∩ g ⁻¹' t).indicator fun (ω : Ω) ↦ 1 | m'] fun (ω : Ω) ↦
            HMul.hMul (α := ℝ) (μ[(f ⁻¹' s).indicator fun (ω : Ω) ↦ 1 | m'] ω)
              (μ[(g ⁻¹' t).indicator fun (ω : Ω) ↦ 1 | m'] ω)
have refine_1 : ∀
  (h :
    ∀ (t1 t2 : Set Ω),
      MeasurableSet t1 →
        MeasurableSet t2 →
          μ[(t1 ∩ t2).indicator fun (ω : Ω) ↦ 1 | m'] =ᶠ[ae μ]
            HMul.hMul (α := Ω → ℝ) μ[t1.indicator fun (ω : Ω) ↦ 1 | m'] μ[t2.indicator fun (ω : Ω) ↦ 1 | m'])
  (s : Set β) (t : Set β') (hs : MeasurableSet s) (ht : MeasurableSet t),
  (ae μ).EventuallyEq (β := ℝ) μ[(f ⁻¹' s ∩ g ⁻¹' t).indicator fun (ω : Ω) ↦ 1 | m'] fun (ω : Ω) ↦
    HMul.hMul (α := ℝ) (μ[(f ⁻¹' s).indicator fun (ω : Ω) ↦ 1 | m'] ω) (μ[(g ⁻¹' t).indicator fun (ω : Ω) ↦ 1 | m'] ω)
Tactic: refine ⟨fun h s t hs ht ↦ ?_, fun h s t ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (goal)
Goal:
Ω : Type u_1
β : Type u_3
β' : Type u_4
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
hf : Measurable f
hg : Measurable g
refine_1 :
  ∀
    (h :
      ∀ (t1 t2 : Set Ω),
        MeasurableSet t1 →
          MeasurableSet t2 →
            μ[(t1 ∩ t2).indicator fun (ω : Ω) ↦ 1 | m'] =ᶠ[ae μ]
              HMul.hMul (α := Ω → ℝ) μ[t1.indicator fun (ω : Ω) ↦ 1 | m'] μ[t2.indicator fun (ω : Ω) ↦ 1 | m'])
    (s : Set β) (t : Set β') (hs : MeasurableSet s) (ht : MeasurableSet t),
    (ae μ).EventuallyEq (β := ℝ) μ[(f ⁻¹' s ∩ g ⁻¹' t).indicator fun (ω : Ω) ↦ 1 | m'] fun (ω : Ω) ↦
      HMul.hMul (α := ℝ) (μ[(f ⁻¹' s).indicator fun (ω : Ω) ↦ 1 | m'] ω) (μ[(g ⁻¹' t).indicator fun (ω : Ω) ↦ 1 | m'] ω)
⊢ (∀ (t1 t2 : Set Ω),
      MeasurableSet t1 →
        MeasurableSet t2 →
          μ[(t1 ∩ t2).indicator fun (ω : Ω) ↦ 1 | m'] =ᶠ[ae μ]
            HMul.hMul (α := Ω → ℝ) μ[t1.indicator fun (ω : Ω) ↦ 1 | m'] μ[t2.indicator fun (ω : Ω) ↦ 1 | m']) ↔
    ∀ (s : Set β) (t : Set β'),
      MeasurableSet s →
        MeasurableSet t →
          (ae μ).EventuallyEq (β := ℝ) μ[(f ⁻¹' s ∩ g ⁻¹' t).indicator fun (ω : Ω) ↦ 1 | m'] fun (ω : Ω) ↦
            HMul.hMul (α := ℝ) (μ[(f ⁻¹' s).indicator fun (ω : Ω) ↦ 1 | m'] ω)
              (μ[(g ⁻¹' t).indicator fun (ω : Ω) ↦ 1 | m'] ω)
have refine_2 : ∀
  (h :
    ∀ (s : Set β) (t : Set β'),
      MeasurableSet s →
        MeasurableSet t →
          (ae μ).EventuallyEq (β := ℝ) μ[(f ⁻¹' s ∩ g ⁻¹' t).indicator fun (ω : Ω) ↦ 1 | m'] fun (ω : Ω) ↦
            HMul.hMul (α := ℝ) (μ[(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 μ]
        HMul.hMul (α := Ω → ℝ) μ[s.indicator fun (ω : Ω) ↦ 1 | m'] μ[t.indicator fun (ω : Ω) ↦ 1 | m']
Tactic: refine ⟨fun h s t hs ht ↦ ?_, fun h s t ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
β : ι → Type u_5
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
hf : ∀ (i : ι), Measurable (f i)
⊢ iCondIndepFun m' hm' (β := β) f μ ↔
    ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)} (_H : ∀ i ∈ S, MeasurableSet (sets i)),
      (ae μ).EventuallyEq (β := ℝ) μ[Set.indicator (⋂ i ∈ S, f i ⁻¹' sets i) fun (ω : Ω) ↦ 1 | m']
        (∏ i ∈ S, μ[(f i ⁻¹' sets i).indicator fun (ω : Ω) ↦ 1 | m'])
have rw : (∀ (s : Finset ι) {g : ι → Set Ω} (_H : ∀ i ∈ s, MeasurableSet (g i)),
    (ae μ).EventuallyEq (β := ℝ) μ[Set.indicator (⋂ i ∈ s, g i) fun (ω : Ω) ↦ 1 | m']
      (∏ i ∈ s, μ[(g i).indicator fun (ω : Ω) ↦ 1 | m'])) ↔
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)} (_H : ∀ i ∈ S, MeasurableSet (sets i)),
    (ae μ).EventuallyEq (β := ℝ) μ[Set.indicator (⋂ i ∈ S, f i ⁻¹' sets i) fun (ω : Ω) ↦ 1 | m']
      (∏ i ∈ S, μ[(f i ⁻¹' sets i).indicator fun (ω : Ω) ↦ 1 | m'])
Tactic: rw [iCondIndepFun_iff]
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
β : ι → Type u_5
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
hf : ∀ (i : ι), Measurable (f i)
⊢ (∀ (s : Finset ι) {g : ι → Set Ω} (_H : ∀ i ∈ s, MeasurableSet (g i)),
      (ae μ).EventuallyEq (β := ℝ) μ[Set.indicator (⋂ i ∈ s, g i) fun (ω : Ω) ↦ 1 | m']
        (∏ i ∈ s, μ[(g i).indicator fun (ω : Ω) ↦ 1 | m'])) ↔
    ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)} (_H : ∀ i ∈ S, MeasurableSet (sets i)),
      (ae μ).EventuallyEq (β := ℝ) μ[Set.indicator (⋂ i ∈ S, f i ⁻¹' sets i) fun (ω : Ω) ↦ 1 | m']
        (∏ i ∈ S, μ[(f i ⁻¹' sets i).indicator fun (ω : Ω) ↦ 1 | m'])
have refine_1 : ∀
  (h :
    ∀ (s : Finset ι) {g : ι → Set Ω} (_H : ∀ i ∈ s, MeasurableSet (g i)),
      (ae μ).EventuallyEq (β := ℝ) μ[Set.indicator (⋂ i ∈ s, g i) fun (ω : Ω) ↦ 1 | m']
        (∏ i ∈ s, μ[(g i).indicator fun (ω : Ω) ↦ 1 | m']))
  (s : Finset ι) (sets : (i : ι) → Set (β i)) (h_sets : ∀ i ∈ s, MeasurableSet (sets i)),
  (ae μ).EventuallyEq (β := ℝ) μ[Set.indicator (⋂ i ∈ s, f i ⁻¹' sets i) fun (ω : Ω) ↦ 1 | m']
    (∏ i ∈ s, μ[(f i ⁻¹' sets i).indicator fun (ω : Ω) ↦ 1 | m'])
Tactic: refine ⟨fun h s sets h_sets ↦ ?_, fun h s sets h_sets ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
β : ι → Type u_5
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
hf : ∀ (i : ι), Measurable (f i)
refine_1 :
  ∀
    (h :
      ∀ (s : Finset ι) {g : ι → Set Ω} (_H : ∀ i ∈ s, MeasurableSet (g i)),
        (ae μ).EventuallyEq (β := ℝ) μ[Set.indicator (⋂ i ∈ s, g i) fun (ω : Ω) ↦ 1 | m']
          (∏ i ∈ s, μ[(g i).indicator fun (ω : Ω) ↦ 1 | m']))
    (s : Finset ι) (sets : (i : ι) → Set (β i)) (h_sets : ∀ i ∈ s, MeasurableSet (sets i)),
    (ae μ).EventuallyEq (β := ℝ) μ[Set.indicator (⋂ i ∈ s, f i ⁻¹' sets i) fun (ω : Ω) ↦ 1 | m']
      (∏ i ∈ s, μ[(f i ⁻¹' sets i).indicator fun (ω : Ω) ↦ 1 | m'])
⊢ (∀ (s : Finset ι) {g : ι → Set Ω} (_H : ∀ i ∈ s, MeasurableSet (g i)),
      (ae μ).EventuallyEq (β := ℝ) μ[Set.indicator (⋂ i ∈ s, g i) fun (ω : Ω) ↦ 1 | m']
        (∏ i ∈ s, μ[(g i).indicator fun (ω : Ω) ↦ 1 | m'])) ↔
    ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)} (_H : ∀ i ∈ S, MeasurableSet (sets i)),
      (ae μ).EventuallyEq (β := ℝ) μ[Set.indicator (⋂ i ∈ S, f i ⁻¹' sets i) fun (ω : Ω) ↦ 1 | m']
        (∏ i ∈ S, μ[(f i ⁻¹' sets i).indicator fun (ω : Ω) ↦ 1 | m'])
have refine_2 : ∀
  (h :
    ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)} (_H : ∀ i ∈ S, MeasurableSet (sets i)),
      (ae μ).EventuallyEq (β := ℝ) μ[Set.indicator (⋂ i ∈ S, f i ⁻¹' sets i) fun (ω : Ω) ↦ 1 | m']
        (∏ i ∈ S, μ[(f i ⁻¹' sets i).indicator fun (ω : Ω) ↦ 1 | m']))
  (s : Finset ι) (sets : ι → Set Ω) (h_sets : ∀ i ∈ s, MeasurableSet (sets i)),
  (ae μ).EventuallyEq (β := ℝ) μ[Set.indicator (⋂ i ∈ s, sets i) fun (ω : Ω) ↦ 1 | m']
    (∏ i ∈ s, μ[(sets i).indicator fun (ω : Ω) ↦ 1 | m'])
Tactic: refine ⟨fun h s sets h_sets ↦ ?_, fun h s sets h_sets ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
β : ι → Type u_5
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
hf : ∀ (i : ι), Measurable (f i)
h :
  ∀ (s : Finset ι) {g : ι → Set Ω} (_H : ∀ i ∈ s, MeasurableSet (g i)),
    (ae μ).EventuallyEq (β := ℝ) μ[Set.indicator (⋂ i ∈ s, g i) fun (ω : Ω) ↦ 1 | m']
      (∏ i ∈ s, μ[(g i).indicator fun (ω : Ω) ↦ 1 | m'])
s : Finset ι
sets : (i : ι) → Set (β i)
h_sets : ∀ i ∈ s, MeasurableSet (sets i)
⊢ (ae μ).EventuallyEq (β := ℝ) μ[Set.indicator (⋂ i ∈ s, f i ⁻¹' sets i) fun (ω : Ω) ↦ 1 | m']
    (∏ i ∈ s, μ[(f i ⁻¹' sets i).indicator fun (ω : Ω) ↦ 1 | m'])
have refine_1 : ∀ (i : ι) (hi : i ∈ s), MeasurableSet.{u_1} (α := Ω) ((fun (i : ι) ↦ f i ⁻¹' sets i) i)
Tactic: refine h s (g := fun i ↦ f i ⁻¹' (sets i)) (fun i hi ↦ ?_)
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
β : ι → Type u_5
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
hf : ∀ (i : ι), Measurable (f i)
h :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)} (_H : ∀ i ∈ S, MeasurableSet (sets i)),
    (ae μ).EventuallyEq (β := ℝ) μ[Set.indicator (⋂ i ∈ S, f i ⁻¹' sets i) fun (ω : Ω) ↦ 1 | m']
      (∏ 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 (p := fun (s' : Set (β i)) ↦ MeasurableSet s' ∧ f i ⁻¹' s' = sets i) ⋯
    else Set.univ
⊢ (ae μ).EventuallyEq (β := ℝ) μ[Set.indicator (⋂ i ∈ s, sets i) fun (ω : Ω) ↦ 1 | m']
    (∏ i ∈ s, μ[(sets i).indicator fun (ω : Ω) ↦ 1 | m'])
have refine_2 : ∀ (i : ι) (hi : i ∈ s), MeasurableSet (g i)
Tactic: specialize h s (sets := g) (fun i hi ↦ ?_)
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
β : ι → Type u_5
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
hf : ∀ (i : ι), Measurable (f i)
h :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)} (_H : ∀ i ∈ S, MeasurableSet (sets i)),
    (ae μ).EventuallyEq (β := ℝ) μ[Set.indicator (⋂ i ∈ S, f i ⁻¹' sets i) fun (ω : Ω) ↦ 1 | m']
      (∏ 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 (p := fun (s' : Set (β i)) ↦ MeasurableSet s' ∧ f i ⁻¹' s' = sets i) ⋯
    else Set.univ
refine_2 : ∀ (i : ι) (hi : i ∈ s), MeasurableSet (g i)
⊢ (ae μ).EventuallyEq (β := ℝ) μ[Set.indicator (⋂ i ∈ s, sets i) fun (ω : Ω) ↦ 1 | m']
    (∏ i ∈ s, μ[(sets i).indicator fun (ω : Ω) ↦ 1 | m'])
have refine_2₁ : ∀
  (h :
    (ae μ).EventuallyEq (β := ℝ) μ[Set.indicator (⋂ i ∈ s, f i ⁻¹' g i) fun (ω : Ω) ↦ 1 | m']
      (∏ i ∈ s, μ[(f i ⁻¹' g i).indicator fun (ω : Ω) ↦ 1 | m'])),
  (ae μ).EventuallyEq (β := ℝ) μ[Set.indicator (⋂ i ∈ s, sets i) fun (ω : Ω) ↦ 1 | m']
    (∏ i ∈ s, μ[(sets i).indicator fun (ω : Ω) ↦ 1 | m'])
Tactic: specialize h s (sets := g) (fun i hi ↦ ?_)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
β : ι → Type u_5
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
hf : ∀ (i : ι), Measurable (f i)
h :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)} (_H : ∀ i ∈ S, MeasurableSet (sets i)),
    (ae μ).EventuallyEq (β := ℝ) μ[Set.indicator (⋂ i ∈ S, f i ⁻¹' sets i) fun (ω : Ω) ↦ 1 | m']
      (∏ 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 (p := fun (s' : Set (β i)) ↦ MeasurableSet s' ∧ f i ⁻¹' s' = sets i) ⋯
    else Set.univ
i : ι
hi : i ∈ s
⊢ MeasurableSet (g i)
have refine_2 : MeasurableSet (Exists.choose (p := fun (s' : Set (β i)) ↦ MeasurableSet s' ∧ f i ⁻¹' s' = sets i) sorry)
Tactic: simp only [g, dif_pos hi]
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : 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 (p := fun (s' : Set (β i)) ↦ MeasurableSet s' ∧ f i ⁻¹' s' = sets i) ⋯
    else Set.univ
h :
  (ae μ).EventuallyEq (β := ℝ) μ[Set.indicator (⋂ i ∈ s, f i ⁻¹' g i) fun (ω : Ω) ↦ 1 | m']
    (∏ i ∈ s, μ[(f i ⁻¹' g i).indicator fun (ω : Ω) ↦ 1 | m'])
i : ι
hi : i ∈ s
⊢ sets i = f i ⁻¹' g i
have rw : f i ⁻¹' Exists.choose (p := fun (s' : Set (β i)) ↦ MeasurableSet s' ∧ f i ⁻¹' s' = sets i) sorry = f i ⁻¹' g i
Tactic: rw [(h_sets i hi).choose_spec.2.symm]
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (hypothesis)
Goal:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : 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 (p := fun (s' : Set (β i)) ↦ MeasurableSet s' ∧ f i ⁻¹' s' = sets i) ⋯
    else Set.univ
h :
  (ae μ).EventuallyEq (β := ℝ) μ[Set.indicator (⋂ i ∈ s, f i ⁻¹' g i) fun (ω : Ω) ↦ 1 | m']
    (∏ i ∈ s, μ[(f i ⁻¹' g i).indicator fun (ω : Ω) ↦ 1 | m'])
⊢ (ae μ).EventuallyEq (β := ℝ) μ[Set.indicator (⋂ i ∈ s, sets i) fun (ω : Ω) ↦ 1 | m']
    (∏ i ∈ s, μ[(sets i).indicator fun (ω : Ω) ↦ 1 | m'])
have hg : ∀ i ∈ s, sets i = f i ⁻¹' g i
Tactic: have hg : ∀ i ∈ s, sets i = f i ⁻¹' g i := by
        intro i hi
        rw [(h_sets i hi).choose_spec.2.symm]
        simp only [g, dif_pos hi]
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
β : ι → Type u_5
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
hf : ∀ (i : ι), Measurable (f i)
h :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)} (_H : ∀ i ∈ S, MeasurableSet (sets i)),
    (ae μ).EventuallyEq (β := ℝ) μ[Set.indicator (⋂ i ∈ S, f i ⁻¹' sets i) fun (ω : Ω) ↦ 1 | m']
      (∏ i ∈ S, μ[(f i ⁻¹' sets i).indicator fun (ω : Ω) ↦ 1 | m'])
s : Finset ι
sets : ι → Set Ω
h_sets : ∀ i ∈ s, MeasurableSet (sets i)
refine_2 refine_2₁ refine_2₂ :
  (ae μ).EventuallyEq (β := ℝ) μ[Set.indicator (⋂ i ∈ s, sets i) fun (ω : Ω) ↦ 1 | m']
    (∏ i ∈ s, μ[(sets i).indicator fun (ω : Ω) ↦ 1 | m'])
⊢ (ae μ).EventuallyEq (β := ℝ) μ[Set.indicator (⋂ i ∈ s, sets i) fun (ω : Ω) ↦ 1 | m']
    (∏ i ∈ s, μ[(sets i).indicator fun (ω : Ω) ↦ 1 | m'])
have refine_2₃ : let g : (i : ι) → Set (β i) := fun (i : ι) ↦
  if hi : i ∈ s then Exists.choose (p := fun (s' : Set (β i)) ↦ MeasurableSet s' ∧ f i ⁻¹' s' = sets i) sorry else Set.univ;
∀ (i : ι) (hi : i ∈ s), MeasurableSet (g i)
Tactic: classical
    let g := fun i ↦ if hi : i ∈ s then (h_sets i hi).choose else Set.univ
    specialize h s (sets := g) (fun i hi ↦ ?_)
    · simp only [g, dif_pos hi]
      exact (h_sets i hi).choose_spec.1
    · have hg : ∀ i ∈ s, sets i = f i ⁻¹' g i := by
        intro i hi
        rw [(h_sets i hi).choose_spec.2.symm]
        simp only [g, dif_pos hi]
      convert! h with i hi i hi <;> exact hg i hi
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
β : ι → Type u_5
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
hf : ∀ (i : ι), Measurable (f i)
h :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)} (_H : ∀ i ∈ S, MeasurableSet (sets i)),
    (ae μ).EventuallyEq (β := ℝ) μ[Set.indicator (⋂ i ∈ S, f i ⁻¹' sets i) fun (ω : Ω) ↦ 1 | m']
      (∏ i ∈ S, μ[(f i ⁻¹' sets i).indicator fun (ω : Ω) ↦ 1 | m'])
s : Finset ι
sets : ι → Set Ω
h_sets : ∀ i ∈ s, MeasurableSet (sets i)
refine_2 refine_2₁ refine_2₂ :
  (ae μ).EventuallyEq (β := ℝ) μ[Set.indicator (⋂ i ∈ s, sets i) fun (ω : Ω) ↦ 1 | m']
    (∏ i ∈ s, μ[(sets i).indicator fun (ω : Ω) ↦ 1 | m'])
refine_2₃ :
  let g : (i : ι) → Set (β i) := fun (i : ι) ↦
    if hi : i ∈ s then Exists.choose (p := fun (s' : Set (β i)) ↦ MeasurableSet s' ∧ f i ⁻¹' s' = sets i) ⋯
    else Set.univ;
  ∀ (i : ι) (hi : i ∈ s), MeasurableSet (g i)
⊢ (ae μ).EventuallyEq (β := ℝ) μ[Set.indicator (⋂ i ∈ s, sets i) fun (ω : Ω) ↦ 1 | m']
    (∏ i ∈ s, μ[(sets i).indicator fun (ω : Ω) ↦ 1 | m'])
have refine_2₄ : let g : (i : ι) → Set (β i) := fun (i : ι) ↦
  if hi : i ∈ s then Exists.choose (p := fun (s' : Set (β i)) ↦ MeasurableSet s' ∧ f i ⁻¹' s' = sets i) sorry else Set.univ;
∀
  (h :
    (ae μ).EventuallyEq (β := ℝ) μ[Set.indicator (⋂ i ∈ s, f i ⁻¹' g i) fun (ω : Ω) ↦ 1 | m']
      (∏ i ∈ s, μ[(f i ⁻¹' g i).indicator fun (ω : Ω) ↦ 1 | m'])),
  (ae μ).EventuallyEq (β := ℝ) μ[Set.indicator (⋂ i ∈ s, sets i) fun (ω : Ω) ↦ 1 | m']
    (∏ i ∈ s, μ[(sets i).indicator fun (ω : Ω) ↦ 1 | m'])
Tactic: classical
    let g := fun i ↦ if hi : i ∈ s then (h_sets i hi).choose else Set.univ
    specialize h s (sets := g) (fun i hi ↦ ?_)
    · simp only [g, dif_pos hi]
      exact (h_sets i hi).choose_spec.1
    · have hg : ∀ i ∈ s, sets i = f i ⁻¹' g i := by
        intro i hi
        rw [(h_sets i hi).choose_spec.2.symm]
        simp only [g, dif_pos hi]
      convert! h with i hi i hi <;> exact hg i hi
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (goal)
Goal:
Ω : Type u_1
β : Type u_3
β' : Type u_4
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
X : Ω → β
Y : Ω → β'
hX : Measurable X
hY : Measurable Y
⊢ CondIndepFun m' hm' X Y μ
have rw : ∀ (t1 t2 : Set Ω),
  MeasurableSet t1 →
    MeasurableSet t2 →
      μ[(t1 ∩ t2).indicator fun (ω : Ω) ↦ 1 | m'] =ᶠ[ae μ]
        HMul.hMul (α := Ω → ℝ) μ[t1.indicator fun (ω : Ω) ↦ 1 | m'] μ[t2.indicator fun (ω : Ω) ↦ 1 | m']
Tactic: rw [condIndepFun_iff _ hm' _ _ (hX.mono hm' le_rfl) hY]
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (goal)
Goal:
Ω : Type u_1
β : Type u_3
β' : Type u_4
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
X : Ω → β
Y : Ω → β'
hX : Measurable X
hY : Measurable Y
s : Set β
hs : MeasurableSet s
t : Set β'
ht : MeasurableSet t
⊢ μ[(X ⁻¹' s ∩ Y ⁻¹' t).indicator fun (ω : Ω) ↦ 1 | m'] =ᶠ[ae μ]
    HMul.hMul (α := Ω → ℝ) μ[(X ⁻¹' s).indicator fun (ω : Ω) ↦ 1 | m'] μ[(Y ⁻¹' t).indicator fun (ω : Ω) ↦ 1 | m']
have rw : μ[HMul.hMul (α := (x : Ω) → ℝ) ((X ⁻¹' s).indicator 1) ((Y ⁻¹' t).indicator 1) | m'] =ᶠ[ae μ]
  HMul.hMul (α := Ω → ℝ) μ[(X ⁻¹' s).indicator 1 | m'] μ[(Y ⁻¹' t).indicator 1 | m']
Tactic: rw [show (fun ω : Ω ↦ (1 : ℝ)) = 1 from rfl, Set.inter_indicator_one]
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (goal)
Goal:
Ω : Type u_1
β : Type u_3
β' : Type u_4
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
X : Ω → β
Y : Ω → β'
hX : Measurable X
hY : Measurable Y
s : Set β
hs : MeasurableSet s
t : Set β'
ht : MeasurableSet t
⊢ μ[HMul.hMul (α := (x : Ω) → ℝ) ((X ⁻¹' s).indicator 1) ((Y ⁻¹' t).indicator 1) | m'] =ᶠ[ae μ]
    HMul.hMul (α := (x : Ω) → ℝ) ((X ⁻¹' s).indicator 1) μ[(Y ⁻¹' t).indicator 1 | m']
have refine : ∀ (ω : Ω), norm (E := ℝ) ((X ⁻¹' s).indicator 1 ω) ≤ 1
Tactic: refine condExp_stronglyMeasurable_mul_of_bound hm' (stronglyMeasurable_const.indicator (hX hs))
      ((integrable_indicator_iff (hY ht)).2 integrableOn_const) 1 (ae_of_all μ fun ω ↦ ?_)
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (goal)
Goal:
Ω : Type u_1
β : Type u_3
β' : Type u_4
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
X : Ω → β
Y : Ω → β'
hX : Measurable X
hY : Measurable Y
s : Set β
hs : MeasurableSet s
t : Set β'
ht : MeasurableSet t
ω : Ω
⊢ norm (E := ℝ) (if ω ∈ X ⁻¹' s then 1 ω else 0) ≤ 1
have pos : ∀ (h : ω ∈ X ⁻¹' s), norm (E := ℝ) (1 ω) ≤ 1
Tactic: split_ifs with h