awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Independence.Conditional
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)
i : ι
hi : i ∈ s
⊢ MeasurableSet.{u_1} (α := Ω) ((fun (i : ι) ↦ f i ⁻¹' sets i) i)

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

Premises used: MeasurableSet, And.intro, Exists.intro, rfl
-- Module: Mathlib.Probability.Independence.Conditional
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)
i : ι
hi : i ∈ s
⊢ MeasurableSet.{u_1} (α := Ω) ((fun (i : ι) ↦ f i ⁻¹' sets i) i)

Tactic:
exact ⟨sets i, h_sets i hi, rfl⟩
-- Module: Mathlib.Probability.Independence.Conditional
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)
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'])
⊢ (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 ↦ ?_)
-- Module: Mathlib.Probability.Independence.Conditional
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
refine_2 : MeasurableSet (Exists.choose (p := fun (s' : Set (β i)) ↦ MeasurableSet s' ∧ f i ⁻¹' s' = sets i) ⋯)
⊢ MeasurableSet (g i)

Tactic:
simp only [g, dif_pos hi]

Premises used: dif_pos
-- Module: Mathlib.Probability.Independence.Conditional
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 (Exists.choose (p := fun (s' : Set (β i)) ↦ MeasurableSet s' ∧ f i ⁻¹' s' = sets i) ⋯)

Tactic:
(h_sets i hi).choose_spec.1

Premises used: Exists.choose_spec, And.left
-- Module: Mathlib.Probability.Independence.Conditional
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 (Exists.choose (p := fun (s' : Set (β i)) ↦ MeasurableSet s' ∧ f i ⁻¹' s' = sets i) ⋯)

Tactic:
exact (h_sets i hi).choose_spec.1

Premises used: Exists.choose_spec, And.left
-- Module: Mathlib.Probability.Independence.Conditional
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
rw : f i ⁻¹' Exists.choose (p := fun (s' : Set (β i)) ↦ MeasurableSet s' ∧ f i ⁻¹' s' = sets i) ⋯ = f i ⁻¹' g i
⊢ sets i = f i ⁻¹' g i

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

Premises used: Exists.choose_spec, And.right, Eq.symm
-- Module: Mathlib.Probability.Independence.Conditional
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
⊢ f i ⁻¹' Exists.choose (p := fun (s' : Set (β i)) ↦ MeasurableSet s' ∧ f i ⁻¹' s' = sets i) ⋯ = f i ⁻¹' g i

Tactic:
simp only [g, dif_pos hi]

Premises used: dif_pos
-- Module: Mathlib.Probability.Independence.Conditional
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 ∈ 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]
-- Module: Mathlib.Probability.Independence.Conditional
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'])
hg : ∀ i ∈ s, sets i = f i ⁻¹' g i
⊢ (ae μ).EventuallyEq (β := ℝ) μ[Set.indicator (⋂ i ∈ s, f i ⁻¹' g i) fun (ω : Ω) ↦ 1 | m']
    (∏ i ∈ s, μ[(f i ⁻¹' g i).indicator fun (ω : Ω) ↦ 1 | m'])

Tactic:
h
-- Module: Mathlib.Probability.Independence.Conditional
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'])
hg h₁ h₂ : ∀ (i : ι) (hi : i ∈ s), sets i = f i ⁻¹' g i
⊢ (ae μ).EventuallyEq (β := ℝ) μ[Set.indicator (⋂ i ∈ s, sets i) fun (ω : Ω) ↦ 1 | m']
    (∏ i ∈ s, μ[(sets i).indicator fun (ω : Ω) ↦ 1 | m'])

Tactic:
convert! h with i hi i hi
-- Module: Mathlib.Probability.Independence.Conditional
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'])
hg : ∀ i ∈ s, sets i = f i ⁻¹' g i
i : ι
hi : i ∈ s
⊢ sets i = f i ⁻¹' g i

Tactic:
hg i hi
-- Module: Mathlib.Probability.Independence.Conditional
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'])
hg : ∀ i ∈ s, sets i = f i ⁻¹' g i
i : ι
hi : i ∈ s
⊢ sets i = f i ⁻¹' g i

Tactic:
exact hg i hi
-- Module: Mathlib.Probability.Independence.Conditional
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)
refine_2₄ 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;
  ∀
    (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'])
⊢ (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
-- Module: Mathlib.Probability.Independence.Conditional
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 → CondIndepSet m' hm' (f ⁻¹' s) (g ⁻¹' t) μ

Tactic:
simp only [CondIndepFun, CondIndepSet, Kernel.indepFun_iff_indepSet_preimage hf hg]

Premises used: ProbabilityTheory.CondIndepSet, ProbabilityTheory.Kernel.indepFun_iff_indepSet_preimage, ProbabilityTheory.CondIndepFun
-- Module: Mathlib.Probability.Independence.Conditional
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 β'
f : Ω → β
g : Ω → β'
hfg : CondIndepFun m' hm' f g μ
⊢ CondIndepFun m' hm' g f μ

Tactic:
hfg.symm

Premises used: ProbabilityTheory.Kernel.IndepFun.symm, ProbabilityTheory.CondIndepFun
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
β : Type u_3
β' : Type u_4
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
γ : Type u_5
γ' : Type u_6
_mβ : MeasurableSpace β
_mβ' : MeasurableSpace β'
_mγ : MeasurableSpace γ
_mγ' : MeasurableSpace γ'
φ : β → γ
ψ : β' → γ'
hfg : CondIndepFun m' hm' f g μ
hφ : Measurable φ
hψ : Measurable ψ
⊢ CondIndepFun m' hm' (φ ∘ f) (ψ ∘ g) μ

Tactic:
Kernel.IndepFun.comp hfg hφ hψ

Premises used: ProbabilityTheory.Kernel.IndepFun.comp, ProbabilityTheory.CondIndepFun
-- Module: Mathlib.Probability.Independence.Conditional
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 β'
c : β
X : Ω → β'
⊢ CondIndepFun.{u_1, u_3, u_4} m' hm' (β := β) (fun (x : Ω) ↦ c) X μ

Tactic:
Kernel.indepFun_const_left c X

Premises used: ProbabilityTheory.Kernel.indepFun_const_left, ProbabilityTheory.CondIndepFun
-- Module: Mathlib.Probability.Independence.Conditional
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 : Ω → β
c : β'
⊢ CondIndepFun.{u_1, u_3, u_4} m' hm' (γ := β') X (fun (x : Ω) ↦ c) μ

Tactic:
Kernel.indepFun_const_right X c

Premises used: ProbabilityTheory.CondIndepFun, ProbabilityTheory.Kernel.indepFun_const_right
-- Module: Mathlib.Probability.Independence.Conditional
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 β'
inst_2 : Neg β'
inst_3 : MeasurableNeg β'
hfg : CondIndepFun m' hm' f g μ
⊢ CondIndepFun m' hm' f (-g) μ

Tactic:
hfg.comp measurable_id measurable_neg

Premises used: measurable_id, MeasurableNeg.measurable_neg, ProbabilityTheory.CondIndepFun.comp
-- Module: Mathlib.Probability.Independence.Conditional
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 β'
inst_2 : Neg β
inst_3 : MeasurableNeg β
hfg : CondIndepFun m' hm' f g μ
⊢ CondIndepFun m' hm' (-f) g μ

Tactic:
hfg.comp measurable_neg measurable_id

Premises used: measurable_id, MeasurableNeg.measurable_neg, ProbabilityTheory.CondIndepFun.comp
-- Module: Mathlib.Probability.Independence.Conditional
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
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']
⊢ CondIndepFun m' hm' X Y μ

Tactic:
rw [condIndepFun_iff _ hm' _ _ (hX.mono hm' le_rfl) hY]

Premises used: le_rfl, ProbabilityTheory.condIndepFun_iff, Measurable.mono
-- Module: Mathlib.Probability.Independence.Conditional
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
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']
⊢ μ[(X ⁻¹' s ∩ Y ⁻¹' t).indicator fun (ω : Ω) ↦ 1 | m'] =ᶠ[ae μ]
    HMul.hMul (α := Ω → ℝ) μ[(X ⁻¹' s).indicator fun (ω : Ω) ↦ 1 | m'] μ[(Y ⁻¹' t).indicator fun (ω : Ω) ↦ 1 | m']

Tactic:
rw [show (fun ω : Ω ↦ (1 : ℝ)) = 1 from rfl, Set.inter_indicator_one]

Premises used: Set.inter_indicator_one, rfl
-- Module: Mathlib.Probability.Independence.Conditional
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']

Tactic:
condExp_stronglyMeasurable_mul_of_bound hm' (stronglyMeasurable_const.indicator (hX hs))
      ((integrable_indicator_iff (hY ht)).2 integrableOn_const) 1 (ae_of_all μ fun ω ↦ ?_)

Premises used: MeasureTheory.stronglyMeasurable_const, Iff.mpr, MeasureTheory.condExp_stronglyMeasurable_mul_of_bound, MeasureTheory.integrableOn_const, MeasureTheory.StronglyMeasurable.indicator, MeasureTheory.ae_of_all, OfNat.ofNat, MeasureTheory.integrable_indicator_iff
-- Module: Mathlib.Probability.Independence.Conditional
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
refine : ∀ (ω : Ω), norm (E := ℝ) ((X ⁻¹' s).indicator 1 ω) ≤ 1
⊢ μ[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']

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 ω ↦ ?_)

Premises used: MeasureTheory.stronglyMeasurable_const, Iff.mpr, MeasureTheory.condExp_stronglyMeasurable_mul_of_bound, MeasureTheory.integrableOn_const, MeasureTheory.StronglyMeasurable.indicator, MeasureTheory.ae_of_all, OfNat.ofNat, MeasureTheory.integrable_indicator_iff
-- Module: Mathlib.Probability.Independence.Conditional
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
ω : Ω
pos : ∀ (h : ω ∈ X ⁻¹' s), norm (E := ℝ) (1 ω) ≤ 1
neg : ∀ (h : ω ∉ X ⁻¹' s), norm (E := ℝ) 0 ≤ 1
⊢ norm (E := ℝ) (if ω ∈ X ⁻¹' s then 1 ω else 0) ≤ 1

Tactic:
split_ifs with h
-- Module: Mathlib.Probability.Independence.Conditional
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
ω : Ω
h : ω ∈ X ⁻¹' s
⊢ norm (E := ℝ) (1 ω) ≤ 1

Tactic:
simp
-- Module: Mathlib.Probability.Independence.Conditional
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
ω : Ω
h : ω ∉ X ⁻¹' s
⊢ norm (E := ℝ) 0 ≤ 1

Tactic:
simp
-- Module: Mathlib.Probability.Independence.Conditional
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
hf : StronglyMeasurable (β := ℝ) ((X ⁻¹' s).indicator 1)
hfi : Integrable (ε := ℝ) ((X ⁻¹' s).indicator 1) μ
⊢ 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:
nth_rw 2 [condExp_of_stronglyMeasurable hm']

Premises used: MeasureTheory.condExp_of_stronglyMeasurable