awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
γ : ι → Type u_9
mβ : (i : ι) → MeasurableSpace (β i)
mγ : (i : ι) → MeasurableSpace (γ i)
f : (i : ι) → Ω → β i
h :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)} (_H : ∀ i ∈ S, MeasurableSet (sets i)),
    ∀ᵐ (a : α) ∂μ,
      Eq (α := ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ i ∈ S, f i ⁻¹' sets i) : ENNReal)
        (∏ i ∈ S, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f i ⁻¹' sets i) : ENNReal)
g : (i : ι) → β i → γ i
hg : ∀ (i : ι), Measurable (g i)
refine :
  ∀ (t : Finset ι) (s : (i : ι) → Set (γ i)) (hs : ∀ i ∈ t, MeasurableSet (s i)),
    ∀ᵐ (a : α) ∂μ,
      Eq (α := ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ i ∈ t, g i ∘ f i ⁻¹' s i) : ENNReal)
        (∏ i ∈ t, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (g i ∘ f i ⁻¹' s i) : ENNReal)
⊢ ∀ (S : Finset ι) {sets : (i : ι) → Set (γ i)} (_H : ∀ i ∈ S, MeasurableSet (sets i)),
    ∀ᵐ (a : α) ∂μ,
      Eq (α := ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ i ∈ S, g i ∘ f i ⁻¹' sets i) : ENNReal)
        (∏ i ∈ S, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (g i ∘ f i ⁻¹' sets i) : ENNReal)

Tactic:
refine fun t s hs ↦ ?_
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
γ : ι → Type u_9
mβ : (i : ι) → MeasurableSpace (β i)
mγ : (i : ι) → MeasurableSpace (γ i)
f : (i : ι) → Ω → β i
h :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)} (_H : ∀ i ∈ S, MeasurableSet (sets i)),
    ∀ᵐ (a : α) ∂μ,
      Eq (α := ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ i ∈ S, f i ⁻¹' sets i) : ENNReal)
        (∏ i ∈ S, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f i ⁻¹' sets i) : ENNReal)
g : (i : ι) → β i → γ i
hg : ∀ (i : ι), Measurable (g i)
t : Finset ι
s : (i : ι) → Set (γ i)
hs : ∀ i ∈ t, MeasurableSet (s i)
⊢ ∀ᵐ (a : α) ∂μ,
    Eq (α := ENNReal)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
          (⋂ i ∈ t, f i ⁻¹' (fun (i : ι) ↦ g i ⁻¹' s i) i) :
        ENNReal)
      (∏ i ∈ t,
          (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f i ⁻¹' (fun (i : ι) ↦ g i ⁻¹' s i) i) :
        ENNReal)

Tactic:
have := h t (sets := fun i ↦ g i ⁻¹' (s i)) (fun i a ↦ hg i (hs i a))
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
γ : ι → Type u_9
mβ : (i : ι) → MeasurableSpace (β i)
mγ : (i : ι) → MeasurableSpace (γ i)
f : (i : ι) → Ω → β i
h :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)} (_H : ∀ i ∈ S, MeasurableSet (sets i)),
    ∀ᵐ (a : α) ∂μ,
      Eq (α := ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ i ∈ S, f i ⁻¹' sets i) : ENNReal)
        (∏ i ∈ S, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f i ⁻¹' sets i) : ENNReal)
g : (i : ι) → β i → γ i
hg : ∀ (i : ι), Measurable (g i)
t : Finset ι
s : (i : ι) → Set (γ i)
hs : ∀ i ∈ t, MeasurableSet (s i)
this :
  ∀ᵐ (a : α) ∂μ,
    Eq (α := ENNReal)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
          (⋂ i ∈ t, f i ⁻¹' (fun (i : ι) ↦ g i ⁻¹' s i) i) :
        ENNReal)
      (∏ i ∈ t,
          (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f i ⁻¹' (fun (i : ι) ↦ g i ⁻¹' s i) i) :
        ENNReal)
h₁ :
  ∀ (a : α)
    (ha :
      Eq (α := ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ i ∈ t, f i ⁻¹' g i ⁻¹' s i) : ENNReal)
        (∏ i ∈ t, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f i ⁻¹' g i ⁻¹' s i) : ENNReal)),
    Eq (α := ENNReal)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ i ∈ t, g i ∘ f i ⁻¹' s i) : ENNReal)
      (∏ i ∈ t, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (g i ∘ f i ⁻¹' s i) : ENNReal)
⊢ ∀ᵐ (a : α) ∂μ,
    Eq (α := ENNReal)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ i ∈ t, g i ∘ f i ⁻¹' s i) : ENNReal)
      (∏ i ∈ t, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (g i ∘ f i ⁻¹' s i) : ENNReal)

Tactic:
filter_upwards [this] with a ha
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
γ : ι → Type u_9
mβ : (i : ι) → MeasurableSpace (β i)
mγ : (i : ι) → MeasurableSpace (γ i)
f : (i : ι) → Ω → β i
h :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)} (_H : ∀ i ∈ S, MeasurableSet (sets i)),
    ∀ᵐ (a : α) ∂μ,
      Eq (α := ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ i ∈ S, f i ⁻¹' sets i) : ENNReal)
        (∏ i ∈ S, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f i ⁻¹' sets i) : ENNReal)
g : (i : ι) → β i → γ i
hg : ∀ (i : ι), Measurable (g i)
t : Finset ι
s : (i : ι) → Set (γ i)
hs : ∀ i ∈ t, MeasurableSet (s i)
this :
  ∀ᵐ (a : α) ∂μ,
    Eq (α := ENNReal)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
          (⋂ i ∈ t, f i ⁻¹' (fun (i : ι) ↦ g i ⁻¹' s i) i) :
        ENNReal)
      (∏ i ∈ t,
          (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f i ⁻¹' (fun (i : ι) ↦ g i ⁻¹' s i) i) :
        ENNReal)
a : α
ha h₁ :
  Eq (α := ENNReal)
    ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ i ∈ t, f i ⁻¹' g i ⁻¹' s i) : ENNReal)
    (∏ x ∈ t, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f x ⁻¹' g x ⁻¹' s x) : ENNReal)
⊢ Eq (α := ENNReal)
    ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ i ∈ t, g i ∘ f i ⁻¹' s i) : ENNReal)
    (∏ i ∈ t, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (g i ∘ f i ⁻¹' s i) : ENNReal)

Tactic:
simp_rw [Set.preimage_comp]

Premises used: Set.preimage_comp
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
γ : ι → Type u_9
mβ : (i : ι) → MeasurableSpace (β i)
mγ : (i : ι) → MeasurableSpace (γ i)
f : (i : ι) → Ω → β i
h :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)} (_H : ∀ i ∈ S, MeasurableSet (sets i)),
    ∀ᵐ (a : α) ∂μ,
      Eq (α := ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ i ∈ S, f i ⁻¹' sets i) : ENNReal)
        (∏ i ∈ S, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f i ⁻¹' sets i) : ENNReal)
g : (i : ι) → β i → γ i
hg : ∀ (i : ι), Measurable (g i)
t : Finset ι
s : (i : ι) → Set (γ i)
hs : ∀ i ∈ t, MeasurableSet (s i)
this :
  ∀ᵐ (a : α) ∂μ,
    Eq (α := ENNReal)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
          (⋂ i ∈ t, f i ⁻¹' (fun (i : ι) ↦ g i ⁻¹' s i) i) :
        ENNReal)
      (∏ i ∈ t,
          (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f i ⁻¹' (fun (i : ι) ↦ g i ⁻¹' s i) i) :
        ENNReal)
a : α
ha :
  Eq (α := ENNReal)
    ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ i ∈ t, f i ⁻¹' g i ⁻¹' s i) : ENNReal)
    (∏ i ∈ t, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f i ⁻¹' g i ⁻¹' s i) : ENNReal)
⊢ Eq (α := ENNReal)
    ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ i ∈ t, f i ⁻¹' g i ⁻¹' s i) : ENNReal)
    (∏ x ∈ t, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f x ⁻¹' g x ⁻¹' s x) : ENNReal)

Tactic:
ha
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
γ : ι → Type u_9
mβ : (i : ι) → MeasurableSpace (β i)
mγ : (i : ι) → MeasurableSpace (γ i)
f : (i : ι) → Ω → β i
h :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)} (_H : ∀ i ∈ S, MeasurableSet (sets i)),
    ∀ᵐ (a : α) ∂μ,
      Eq (α := ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ i ∈ S, f i ⁻¹' sets i) : ENNReal)
        (∏ i ∈ S, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f i ⁻¹' sets i) : ENNReal)
g : (i : ι) → β i → γ i
hg : ∀ (i : ι), Measurable (g i)
t : Finset ι
s : (i : ι) → Set (γ i)
hs : ∀ i ∈ t, MeasurableSet (s i)
this :
  ∀ᵐ (a : α) ∂μ,
    Eq (α := ENNReal)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
          (⋂ i ∈ t, f i ⁻¹' (fun (i : ι) ↦ g i ⁻¹' s i) i) :
        ENNReal)
      (∏ i ∈ t,
          (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f i ⁻¹' (fun (i : ι) ↦ g i ⁻¹' s i) i) :
        ENNReal)
a : α
ha :
  Eq (α := ENNReal)
    ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ i ∈ t, f i ⁻¹' g i ⁻¹' s i) : ENNReal)
    (∏ i ∈ t, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f i ⁻¹' g i ⁻¹' s i) : ENNReal)
⊢ Eq (α := ENNReal)
    ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ i ∈ t, f i ⁻¹' g i ⁻¹' s i) : ENNReal)
    (∏ x ∈ t, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f x ⁻¹' g x ⁻¹' s x) : ENNReal)

Tactic:
exact ha
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
γ : ι → Type u_9
mβ : (i : ι) → MeasurableSpace (β i)
mγ : (i : ι) → MeasurableSpace (γ i)
f : (i : ι) → Ω → β i
h : iIndepFun (β := β) f κ μ
g : (i : ι) → β i → γ i
hf : ∀ (i : ι), AEMeasurable (_m := mΩ) (f i) ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
hg : ∀ (i : ι), AEMeasurable (_m := mβ i) (g i) (Measure.map (f i) ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ))
⊢ iIndepFun (β := γ) (fun (i : ι) ↦ AEMeasurable.mk (g i) ⋯ ∘ f i) κ μ

Tactic:
have h : iIndepFun (fun i ↦ ((hg i).mk (g i)) ∘ f i) κ μ :=
    iIndepFun.comp h (fun i ↦ (hg i).mk (g i)) fun i ↦ (hg i).measurable_mk
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
γ : ι → Type u_9
mβ : (i : ι) → MeasurableSpace (β i)
mγ : (i : ι) → MeasurableSpace (γ i)
f : (i : ι) → Ω → β i
h_1 : iIndepFun (β := β) f κ μ
g : (i : ι) → β i → γ i
hf : ∀ (i : ι), AEMeasurable (_m := mΩ) (f i) ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
hg : ∀ (i : ι), AEMeasurable (_m := mβ i) (g i) (Measure.map (f i) ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ))
h : iIndepFun (β := γ) (fun (i : ι) ↦ AEMeasurable.mk (g i) ⋯ ∘ f i) κ μ
⊢ ∀ (i : ι), ∀ᵐ (x : Ω) ∂(⇑κ : (a : α) → Measure Ω) ∘ₘ μ, AEMeasurable.mk (g i) ⋯ (f i x) = g i (f i x)

Tactic:
have h_ae i := ae_of_ae_map (hf i) (hg i).ae_eq_mk.symm
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
γ : ι → Type u_9
mβ : (i : ι) → MeasurableSpace (β i)
mγ : (i : ι) → MeasurableSpace (γ i)
f : (i : ι) → Ω → β i
h_1 : iIndepFun (β := β) f κ μ
g : (i : ι) → β i → γ i
hf : ∀ (i : ι), AEMeasurable (_m := mΩ) (f i) ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
hg : ∀ (i : ι), AEMeasurable (_m := mβ i) (g i) (Measure.map (f i) ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ))
h : iIndepFun (β := γ) (fun (i : ι) ↦ AEMeasurable.mk (g i) ⋯ ∘ f i) κ μ
h_ae : ∀ (i : ι), ∀ᵐ (x : Ω) ∂(⇑κ : (a : α) → Measure Ω) ∘ₘ μ, AEMeasurable.mk (g i) ⋯ (f i x) = g i (f i x)
⊢ iIndepFun (β := γ) (fun (i : ι) ↦ g i ∘ f i) κ μ

Tactic:
iIndepFun.congr' h fun i ↦ Measure.ae_ae_of_ae_comp (h_ae i)

Premises used: ProbabilityTheory.Kernel.iIndepFun.congr', MeasureTheory.Measure.ae_ae_of_ae_comp
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
γ : ι → Type u_9
mβ : (i : ι) → MeasurableSpace (β i)
mγ : (i : ι) → MeasurableSpace (γ i)
f : (i : ι) → Ω → β i
h_1 : iIndepFun (β := β) f κ μ
g : (i : ι) → β i → γ i
hf : ∀ (i : ι), AEMeasurable (_m := mΩ) (f i) ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
hg : ∀ (i : ι), AEMeasurable (_m := mβ i) (g i) (Measure.map (f i) ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ))
h : iIndepFun (β := γ) (fun (i : ι) ↦ AEMeasurable.mk (g i) ⋯ ∘ f i) κ μ
h_ae : ∀ (i : ι), ∀ᵐ (x : Ω) ∂(⇑κ : (a : α) → Measure Ω) ∘ₘ μ, AEMeasurable.mk (g i) ⋯ (f i x) = g i (f i x)
⊢ iIndepFun (β := γ) (fun (i : ι) ↦ g i ∘ f i) κ μ

Tactic:
exact iIndepFun.congr' h fun i ↦ Measure.ae_ae_of_ae_comp (h_ae i)

Premises used: ProbabilityTheory.Kernel.iIndepFun.congr', MeasureTheory.Measure.ae_ae_of_ae_comp
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
β : Type u_4
β' : Type u_5
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst : IsZeroOrMarkovKernel κ
hf : Measurable f
hg : Measurable g
⊢ IndepFun f g κ μ ↔ ∀ (s : Set β) (t : Set β'), MeasurableSet s → MeasurableSet t → IndepSet (f ⁻¹' s) (g ⁻¹' t) κ μ

Tactic:
indepFun_iff_measure_inter_preimage_eq_mul.trans ?_

Premises used: ProbabilityTheory.Kernel.indepFun_iff_measure_inter_preimage_eq_mul, Iff.trans
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
β : Type u_4
β' : Type u_5
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst : IsZeroOrMarkovKernel κ
hf : Measurable f
hg : Measurable g
refine :
  (∀ (s : Set β) (t : Set β'),
      MeasurableSet s →
        MeasurableSet t →
          ∀ᵐ (a : α) ∂μ,
            (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s ∩ g ⁻¹' t) =
              HMul.hMul (α := ENNReal) (β := ENNReal)
                ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s) : ENNReal)
                ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (g ⁻¹' t) : ENNReal)) ↔
    ∀ (s : Set β) (t : Set β'), MeasurableSet s → MeasurableSet t → IndepSet (f ⁻¹' s) (g ⁻¹' t) κ μ
⊢ IndepFun f g κ μ ↔ ∀ (s : Set β) (t : Set β'), MeasurableSet s → MeasurableSet t → IndepSet (f ⁻¹' s) (g ⁻¹' t) κ μ

Tactic:
refine indepFun_iff_measure_inter_preimage_eq_mul.trans ?_

Premises used: ProbabilityTheory.Kernel.indepFun_iff_measure_inter_preimage_eq_mul, Iff.trans
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
β : Type u_4
β' : Type u_5
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst : IsZeroOrMarkovKernel κ
hf : Measurable f
hg : Measurable g
mp :
  (∀ (s : Set β) (t : Set β'),
      MeasurableSet s →
        MeasurableSet t →
          ∀ᵐ (a : α) ∂μ,
            (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s ∩ g ⁻¹' t) =
              HMul.hMul (α := ENNReal) (β := ENNReal)
                ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s) : ENNReal)
                ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (g ⁻¹' t) : ENNReal)) →
    ∀ (s : Set β) (t : Set β'), MeasurableSet s → MeasurableSet t → IndepSet (f ⁻¹' s) (g ⁻¹' t) κ μ
mpr :
  (∀ (s : Set β) (t : Set β'), MeasurableSet s → MeasurableSet t → IndepSet (f ⁻¹' s) (g ⁻¹' t) κ μ) →
    ∀ (s : Set β) (t : Set β'),
      MeasurableSet s →
        MeasurableSet t →
          ∀ᵐ (a : α) ∂μ,
            (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s ∩ g ⁻¹' t) =
              HMul.hMul (α := ENNReal) (β := ENNReal)
                ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s) : ENNReal)
                ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (g ⁻¹' t) : ENNReal)
⊢ (∀ (s : Set β) (t : Set β'),
      MeasurableSet s →
        MeasurableSet t →
          ∀ᵐ (a : α) ∂μ,
            (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s ∩ g ⁻¹' t) =
              HMul.hMul (α := ENNReal) (β := ENNReal)
                ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s) : ENNReal)
                ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (g ⁻¹' t) : ENNReal)) ↔
    ∀ (s : Set β) (t : Set β'), MeasurableSet s → MeasurableSet t → IndepSet (f ⁻¹' s) (g ⁻¹' t) κ μ

Tactic:
constructor
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
β : Type u_4
β' : Type u_5
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst : IsZeroOrMarkovKernel κ
hf : Measurable f
hg : Measurable g
h :
  ∀ (s : Set β) (t : Set β'),
    MeasurableSet s →
      MeasurableSet t →
        ∀ᵐ (a : α) ∂μ,
          (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s ∩ g ⁻¹' t) =
            HMul.hMul (α := ENNReal) (β := ENNReal)
              ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s) : ENNReal)
              ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (g ⁻¹' t) : ENNReal)
s : Set β
t : Set β'
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ∀ᵐ (a : α) ∂μ,
    (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s ∩ g ⁻¹' t) =
      HMul.hMul (α := ENNReal) (β := ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s) : ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (g ⁻¹' t) : ENNReal)

Tactic:
specialize h s t hs ht
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
β : Type u_4
β' : Type u_5
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst : IsZeroOrMarkovKernel κ
hf : Measurable f
hg : Measurable g
h : ∀ (s : Set β) (t : Set β'), MeasurableSet s → MeasurableSet t → IndepSet (f ⁻¹' s) (g ⁻¹' t) κ μ
s : Set β
t : Set β'
hs : MeasurableSet s
ht : MeasurableSet t
⊢ IndepSet (f ⁻¹' s) (g ⁻¹' t) κ μ

Tactic:
specialize h s t hs ht
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
β : Type u_4
β' : Type u_5
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst : IsZeroOrMarkovKernel κ
hf : Measurable f
hg : Measurable g
s : Set β
t : Set β'
hs : MeasurableSet s
ht : MeasurableSet t
h mp mp₁ mp₂ mp₃ :
  ∀ᵐ (a : α) ∂μ,
    (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s ∩ g ⁻¹' t) =
      HMul.hMul (α := ENNReal) (β := ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s) : ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (g ⁻¹' t) : ENNReal)
⊢ IndepSet (f ⁻¹' s) (g ⁻¹' t) κ μ

Tactic:
rwa [indepSet_iff_measure_inter_eq_mul (hf hs) (hg ht) κ μ]

Premises used: ProbabilityTheory.Kernel.indepSet_iff_measure_inter_eq_mul
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
β : Type u_4
β' : Type u_5
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst : IsZeroOrMarkovKernel κ
hf : Measurable f
hg : Measurable g
s : Set β
t : Set β'
hs : MeasurableSet s
ht : MeasurableSet t
h mpr mpr₁ mpr₂ mpr₃ : IndepSet (f ⁻¹' s) (g ⁻¹' t) κ μ
⊢ ∀ᵐ (a : α) ∂μ,
    (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s ∩ g ⁻¹' t) =
      HMul.hMul (α := ENNReal) (β := ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s) : ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (g ⁻¹' t) : ENNReal)

Tactic:
rwa [← indepSet_iff_measure_inter_eq_mul (hf hs) (hg ht) κ μ]

Premises used: ProbabilityTheory.Kernel.indepSet_iff_measure_inter_eq_mul
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
β : Type u_4
β' : Type u_5
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
f : Ω → β
g : Ω → β'
x : MeasurableSpace β
x_1 : MeasurableSpace β'
hfg : IndepFun f g κ μ
⊢ IndepFun g f κ μ

Tactic:
hfg.symm

Premises used: ProbabilityTheory.Kernel.Indep.symm, ProbabilityTheory.Kernel.IndepFun
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
β : Type u_4
β' : Type u_5
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
f' : Ω → β
g' : Ω → β'
hfg : IndepFun f g κ μ
hf : ∀ᵐ (a : α) ∂μ, f =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] f'
hg : ∀ᵐ (a : α) ∂μ, g =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] g'
A : Set β
hA : MeasurableSet A
B : Set β'
hB : MeasurableSet B
h :
  ∀ (a : α) (hf' : f =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] f')
    (hg' : g =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] g')
    (hfg' :
      (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' A ∩ g ⁻¹' B) =
        HMul.hMul (α := ENNReal) (β := ENNReal)
          ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' A) : ENNReal)
          ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (g ⁻¹' B) : ENNReal)),
    (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f' ⁻¹' A ∩ g' ⁻¹' B) =
      HMul.hMul (α := ENNReal) (β := ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f' ⁻¹' A) : ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (g' ⁻¹' B) : ENNReal)
⊢ ∀ᵐ (a : α) ∂μ,
    (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f' ⁻¹' A ∩ g' ⁻¹' B) =
      HMul.hMul (α := ENNReal) (β := ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f' ⁻¹' A) : ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (g' ⁻¹' B) : ENNReal)

Tactic:
filter_upwards [hf, hg, hfg _ _ ⟨_, hA, rfl⟩ ⟨_, hB, rfl⟩] with a hf' hg' hfg'

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
β : Type u_4
β' : Type u_5
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
f' : Ω → β
g' : Ω → β'
hfg : IndepFun f g κ μ
hf : ∀ᵐ (a : α) ∂μ, f =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] f'
hg : ∀ᵐ (a : α) ∂μ, g =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] g'
A : Set β
hA : MeasurableSet A
B : Set β'
hB : MeasurableSet B
a : α
hf' : f =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] f'
hg' : g =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] g'
hfg' :
  (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' A ∩ g ⁻¹' B) =
    HMul.hMul (α := ENNReal) (β := ENNReal)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' A) : ENNReal)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (g ⁻¹' B) : ENNReal)
⊢ f ⁻¹' A =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] f' ⁻¹' A

Tactic:
have h1 : f ⁻¹' A =ᵐ[κ a] f' ⁻¹' A := hf'.fun_comp A