awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
h1 : f ⁻¹' A =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] f' ⁻¹' A
⊢ g ⁻¹' B =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] g' ⁻¹' B

Tactic:
have h2 : g ⁻¹' B =ᵐ[κ a] g' ⁻¹' B := hg'.fun_comp B
-- 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)
h1 : f ⁻¹' A =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] f' ⁻¹' A
h2 : g ⁻¹' B =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] g' ⁻¹' B
h :
  (((κ : (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)
h₁ :
  (((κ : (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)
h₂ h₃ h₄ h₅ :
  (((κ : (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)

Tactic:
rwa [← measure_congr h1, ← measure_congr h2, ← measure_congr (h1.inter h2)]

Premises used: MeasureTheory.measure_congr, Filter.EventuallyEq.inter
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
mγ : MeasurableSpace γ
mγ' : MeasurableSpace γ'
φ : β → γ
ψ : β' → γ'
hfg : IndepFun f g κ μ
hφ : Measurable φ
hψ : Measurable ψ
A : Set γ
hA : MeasurableSet A
B : Set γ'
hB : MeasurableSet B
a : Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} (φ ∘ f ⁻¹' A)
a₁ : Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} (ψ ∘ g ⁻¹' B)
⊢ ∀ᵐ (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:
apply hfg
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
mγ : MeasurableSpace γ
mγ' : MeasurableSpace γ'
φ : β → γ
ψ : β' → γ'
hfg : IndepFun f g κ μ
hφ : Measurable φ
hψ : Measurable ψ
A : Set γ
hA : MeasurableSet A
B : Set γ'
hB : MeasurableSet B
⊢ Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} (φ ∘ f ⁻¹' A)

Tactic:
⟨φ ⁻¹' A, hφ hA, Set.preimage_comp.symm⟩

Premises used: MeasurableSet, Set.Mem, setOf, Set.preimage_comp, Set.preimage, And.intro, Exists.intro, Eq.symm
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
mγ : MeasurableSpace γ
mγ' : MeasurableSpace γ'
φ : β → γ
ψ : β' → γ'
hfg : IndepFun f g κ μ
hφ : Measurable φ
hψ : Measurable ψ
A : Set γ
hA : MeasurableSet A
B : Set γ'
hB : MeasurableSet B
⊢ Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} (φ ∘ f ⁻¹' A)

Tactic:
exact ⟨φ ⁻¹' A, hφ hA, Set.preimage_comp.symm⟩
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
mγ : MeasurableSpace γ
mγ' : MeasurableSpace γ'
φ : β → γ
ψ : β' → γ'
hfg : IndepFun f g κ μ
hφ : Measurable φ
hψ : Measurable ψ
A : Set γ
hA : MeasurableSet A
B : Set γ'
hB : MeasurableSet B
⊢ Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} (ψ ∘ g ⁻¹' B)

Tactic:
⟨ψ ⁻¹' B, hψ hB, Set.preimage_comp.symm⟩

Premises used: MeasurableSet, Set.Mem, setOf, Set.preimage_comp, Set.preimage, And.intro, Exists.intro, Eq.symm
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
mγ : MeasurableSpace γ
mγ' : MeasurableSpace γ'
φ : β → γ
ψ : β' → γ'
hfg : IndepFun f g κ μ
hφ : Measurable φ
hψ : Measurable ψ
A : Set γ
hA : MeasurableSet A
B : Set γ'
hB : MeasurableSet B
⊢ Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} (ψ ∘ g ⁻¹' B)

Tactic:
exact ⟨ψ ⁻¹' B, hψ hB, Set.preimage_comp.symm⟩
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
mγ : MeasurableSpace γ
mγ' : MeasurableSpace γ'
φ : β → γ
ψ : β' → γ'
hfg : IndepFun f g κ μ
hf : AEMeasurable (_m := mΩ) f ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
hg : AEMeasurable (_m := mΩ) g ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
hφ : AEMeasurable (_m := mβ) φ (Measure.map f ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ))
hψ : AEMeasurable (_m := mβ') ψ (Measure.map g ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ))
⊢ IndepFun (AEMeasurable.mk φ hφ ∘ f) (AEMeasurable.mk ψ hψ ∘ g) κ μ

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

Premises used: ProbabilityTheory.Kernel.IndepFun.comp, AEMeasurable.measurable_mk
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
mγ : MeasurableSpace γ
mγ' : MeasurableSpace γ'
φ : β → γ
ψ : β' → γ'
hfg : IndepFun f g κ μ
hf : AEMeasurable (_m := mΩ) f ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
hg : AEMeasurable (_m := mΩ) g ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
hφ : AEMeasurable (_m := mβ) φ (Measure.map f ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ))
hψ : AEMeasurable (_m := mβ') ψ (Measure.map g ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ))
⊢ IndepFun (AEMeasurable.mk φ hφ ∘ f) (AEMeasurable.mk ψ hψ ∘ g) κ μ

Tactic:
refine IndepFun.comp hfg hφ.measurable_mk hψ.measurable_mk

Premises used: ProbabilityTheory.Kernel.IndepFun.comp, AEMeasurable.measurable_mk
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
mγ : MeasurableSpace γ
mγ' : MeasurableSpace γ'
φ : β → γ
ψ : β' → γ'
hfg : IndepFun f g κ μ
hf : AEMeasurable (_m := mΩ) f ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
hg : AEMeasurable (_m := mΩ) g ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
hφ : AEMeasurable (_m := mβ) φ (Measure.map f ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ))
hψ : AEMeasurable (_m := mβ') ψ (Measure.map g ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ))
⊢ IndepFun (AEMeasurable.mk φ hφ ∘ f) (AEMeasurable.mk ψ hψ ∘ g) κ μ

Tactic:
have h : IndepFun ((hφ.mk φ) ∘ f) ((hψ.mk ψ) ∘ g) κ μ := by
    refine IndepFun.comp hfg hφ.measurable_mk hψ.measurable_mk
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
mγ : MeasurableSpace γ
mγ' : MeasurableSpace γ'
φ : β → γ
ψ : β' → γ'
hfg : IndepFun f g κ μ
hf : AEMeasurable (_m := mΩ) f ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
hg : AEMeasurable (_m := mΩ) g ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
hφ : AEMeasurable (_m := mβ) φ (Measure.map f ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ))
hψ : AEMeasurable (_m := mβ') ψ (Measure.map g ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ))
h : IndepFun (AEMeasurable.mk φ hφ ∘ f) (AEMeasurable.mk ψ hψ ∘ g) κ μ
⊢ ∀ᵐ (x : Ω) ∂(⇑κ : (a : α) → Measure Ω) ∘ₘ μ, φ (f x) = AEMeasurable.mk φ hφ (f x)

Tactic:
have hφ_ae := ae_of_ae_map hf hφ.ae_eq_mk
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
mγ : MeasurableSpace γ
mγ' : MeasurableSpace γ'
φ : β → γ
ψ : β' → γ'
hfg : IndepFun f g κ μ
hf : AEMeasurable (_m := mΩ) f ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
hg : AEMeasurable (_m := mΩ) g ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
hφ : AEMeasurable (_m := mβ) φ (Measure.map f ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ))
hψ : AEMeasurable (_m := mβ') ψ (Measure.map g ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ))
h : IndepFun (AEMeasurable.mk φ hφ ∘ f) (AEMeasurable.mk ψ hψ ∘ g) κ μ
hφ_ae : ∀ᵐ (x : Ω) ∂(⇑κ : (a : α) → Measure Ω) ∘ₘ μ, φ (f x) = AEMeasurable.mk φ hφ (f x)
⊢ ∀ᵐ (x : Ω) ∂(⇑κ : (a : α) → Measure Ω) ∘ₘ μ, ψ (g x) = AEMeasurable.mk ψ hψ (g x)

Tactic:
have hψ_ae := ae_of_ae_map hg hψ.ae_eq_mk
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
mγ : MeasurableSpace γ
mγ' : MeasurableSpace γ'
φ : β → γ
ψ : β' → γ'
hfg : IndepFun f g κ μ
hf : AEMeasurable (_m := mΩ) f ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
hg : AEMeasurable (_m := mΩ) g ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
hφ : AEMeasurable (_m := mβ) φ (Measure.map f ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ))
hψ : AEMeasurable (_m := mβ') ψ (Measure.map g ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ))
h : IndepFun (AEMeasurable.mk φ hφ ∘ f) (AEMeasurable.mk ψ hψ ∘ g) κ μ
hφ_ae : ∀ᵐ (x : Ω) ∂(⇑κ : (a : α) → Measure Ω) ∘ₘ μ, φ (f x) = AEMeasurable.mk φ hφ (f x)
hψ_ae : ∀ᵐ (x : Ω) ∂(⇑κ : (a : α) → Measure Ω) ∘ₘ μ, ψ (g x) = AEMeasurable.mk ψ hψ (g x)
⊢ IndepFun (φ ∘ f) (ψ ∘ g) κ μ

Tactic:
IndepFun.congr' h ?_ ?_

Premises used: ProbabilityTheory.Kernel.IndepFun.congr'
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
mγ : MeasurableSpace γ
mγ' : MeasurableSpace γ'
φ : β → γ
ψ : β' → γ'
hfg : IndepFun f g κ μ
hf : AEMeasurable (_m := mΩ) f ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
hg : AEMeasurable (_m := mΩ) g ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
hφ : AEMeasurable (_m := mβ) φ (Measure.map f ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ))
hψ : AEMeasurable (_m := mβ') ψ (Measure.map g ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ))
h : IndepFun (AEMeasurable.mk φ hφ ∘ f) (AEMeasurable.mk ψ hψ ∘ g) κ μ
hφ_ae : ∀ᵐ (x : Ω) ∂(⇑κ : (a : α) → Measure Ω) ∘ₘ μ, φ (f x) = AEMeasurable.mk φ hφ (f x)
hψ_ae : ∀ᵐ (x : Ω) ∂(⇑κ : (a : α) → Measure Ω) ∘ₘ μ, ψ (g x) = AEMeasurable.mk ψ hψ (g x)
refine_1 :
  ∀ᵐ (a : α) ∂μ, AEMeasurable.mk φ hφ ∘ f =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] φ ∘ f
refine_2 :
  ∀ᵐ (a : α) ∂μ, AEMeasurable.mk ψ hψ ∘ g =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] ψ ∘ g
⊢ IndepFun (φ ∘ f) (ψ ∘ g) κ μ

Tactic:
refine IndepFun.congr' h ?_ ?_

Premises used: ProbabilityTheory.Kernel.IndepFun.congr'
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
mγ : MeasurableSpace γ
mγ' : MeasurableSpace γ'
φ : β → γ
ψ : β' → γ'
hfg : IndepFun f g κ μ
hf : AEMeasurable (_m := mΩ) f ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
hg : AEMeasurable (_m := mΩ) g ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
hφ : AEMeasurable (_m := mβ) φ (Measure.map f ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ))
hψ : AEMeasurable (_m := mβ') ψ (Measure.map g ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ))
h : IndepFun (AEMeasurable.mk φ hφ ∘ f) (AEMeasurable.mk ψ hψ ∘ g) κ μ
hφ_ae : ∀ᵐ (x : Ω) ∂(⇑κ : (a : α) → Measure Ω) ∘ₘ μ, φ (f x) = AEMeasurable.mk φ hφ (f x)
hψ_ae : ∀ᵐ (x : Ω) ∂(⇑κ : (a : α) → Measure Ω) ∘ₘ μ, ψ (g x) = AEMeasurable.mk ψ hψ (g x)
h₁ :
  ∀ (a : α) (haφ : ∀ᵐ (ω : Ω) ∂((κ : (a : α) → Measure Ω) a : Measure Ω), φ (f ω) = AEMeasurable.mk φ hφ (f ω)),
    AEMeasurable.mk φ hφ ∘ f =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] φ ∘ f
⊢ ∀ᵐ (a : α) ∂μ, AEMeasurable.mk φ hφ ∘ f =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] φ ∘ f

Tactic:
filter_upwards [Measure.ae_ae_of_ae_comp (hφ_ae)] with a haφ

Premises used: 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
γ : Type u_6
γ' : Type u_7
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
mγ : MeasurableSpace γ
mγ' : MeasurableSpace γ'
φ : β → γ
ψ : β' → γ'
hfg : IndepFun f g κ μ
hf : AEMeasurable (_m := mΩ) f ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
hg : AEMeasurable (_m := mΩ) g ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
hφ : AEMeasurable (_m := mβ) φ (Measure.map f ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ))
hψ : AEMeasurable (_m := mβ') ψ (Measure.map g ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ))
h : IndepFun (AEMeasurable.mk φ hφ ∘ f) (AEMeasurable.mk ψ hψ ∘ g) κ μ
hφ_ae : ∀ᵐ (x : Ω) ∂(⇑κ : (a : α) → Measure Ω) ∘ₘ μ, φ (f x) = AEMeasurable.mk φ hφ (f x)
hψ_ae : ∀ᵐ (x : Ω) ∂(⇑κ : (a : α) → Measure Ω) ∘ₘ μ, ψ (g x) = AEMeasurable.mk ψ hψ (g x)
a : α
haφ : ∀ᵐ (ω : Ω) ∂((κ : (a : α) → Measure Ω) a : Measure Ω), φ (f ω) = AEMeasurable.mk φ hφ (f ω)
h₁ : ∀ (ω : Ω) (hωφ : φ (f ω) = AEMeasurable.mk φ hφ (f ω)), (AEMeasurable.mk φ hφ ∘ f) ω = (φ ∘ f) ω
⊢ AEMeasurable.mk φ hφ ∘ f =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] φ ∘ f

Tactic:
filter_upwards [haφ] with ω hωφ
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
mγ : MeasurableSpace γ
mγ' : MeasurableSpace γ'
φ : β → γ
ψ : β' → γ'
hfg : IndepFun f g κ μ
hf : AEMeasurable (_m := mΩ) f ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
hg : AEMeasurable (_m := mΩ) g ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
hφ : AEMeasurable (_m := mβ) φ (Measure.map f ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ))
hψ : AEMeasurable (_m := mβ') ψ (Measure.map g ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ))
h : IndepFun (AEMeasurable.mk φ hφ ∘ f) (AEMeasurable.mk ψ hψ ∘ g) κ μ
hφ_ae : ∀ᵐ (x : Ω) ∂(⇑κ : (a : α) → Measure Ω) ∘ₘ μ, φ (f x) = AEMeasurable.mk φ hφ (f x)
hψ_ae : ∀ᵐ (x : Ω) ∂(⇑κ : (a : α) → Measure Ω) ∘ₘ μ, ψ (g x) = AEMeasurable.mk ψ hψ (g x)
a : α
haφ : ∀ᵐ (ω : Ω) ∂((κ : (a : α) → Measure Ω) a : Measure Ω), φ (f ω) = AEMeasurable.mk φ hφ (f ω)
ω : Ω
hωφ : φ (f ω) = AEMeasurable.mk φ hφ (f ω)
⊢ (AEMeasurable.mk φ hφ ∘ f) ω = (φ ∘ f) ω

Tactic:
simp [hωφ]
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
mγ : MeasurableSpace γ
mγ' : MeasurableSpace γ'
φ : β → γ
ψ : β' → γ'
hfg : IndepFun f g κ μ
hf : AEMeasurable (_m := mΩ) f ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
hg : AEMeasurable (_m := mΩ) g ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
hφ : AEMeasurable (_m := mβ) φ (Measure.map f ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ))
hψ : AEMeasurable (_m := mβ') ψ (Measure.map g ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ))
h : IndepFun (AEMeasurable.mk φ hφ ∘ f) (AEMeasurable.mk ψ hψ ∘ g) κ μ
hφ_ae : ∀ᵐ (x : Ω) ∂(⇑κ : (a : α) → Measure Ω) ∘ₘ μ, φ (f x) = AEMeasurable.mk φ hφ (f x)
hψ_ae : ∀ᵐ (x : Ω) ∂(⇑κ : (a : α) → Measure Ω) ∘ₘ μ, ψ (g x) = AEMeasurable.mk ψ hψ (g x)
h₁ :
  ∀ (a : α) (haψ : ∀ᵐ (ω : Ω) ∂((κ : (a : α) → Measure Ω) a : Measure Ω), ψ (g ω) = AEMeasurable.mk ψ hψ (g ω)),
    AEMeasurable.mk ψ hψ ∘ g =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] ψ ∘ g
⊢ ∀ᵐ (a : α) ∂μ, AEMeasurable.mk ψ hψ ∘ g =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] ψ ∘ g

Tactic:
filter_upwards [Measure.ae_ae_of_ae_comp (hψ_ae)] with a haψ

Premises used: 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
γ : Type u_6
γ' : Type u_7
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
mγ : MeasurableSpace γ
mγ' : MeasurableSpace γ'
φ : β → γ
ψ : β' → γ'
hfg : IndepFun f g κ μ
hf : AEMeasurable (_m := mΩ) f ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
hg : AEMeasurable (_m := mΩ) g ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
hφ : AEMeasurable (_m := mβ) φ (Measure.map f ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ))
hψ : AEMeasurable (_m := mβ') ψ (Measure.map g ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ))
h : IndepFun (AEMeasurable.mk φ hφ ∘ f) (AEMeasurable.mk ψ hψ ∘ g) κ μ
hφ_ae : ∀ᵐ (x : Ω) ∂(⇑κ : (a : α) → Measure Ω) ∘ₘ μ, φ (f x) = AEMeasurable.mk φ hφ (f x)
hψ_ae : ∀ᵐ (x : Ω) ∂(⇑κ : (a : α) → Measure Ω) ∘ₘ μ, ψ (g x) = AEMeasurable.mk ψ hψ (g x)
a : α
haψ : ∀ᵐ (ω : Ω) ∂((κ : (a : α) → Measure Ω) a : Measure Ω), ψ (g ω) = AEMeasurable.mk ψ hψ (g ω)
h₁ : ∀ (ω : Ω) (hωψ : ψ (g ω) = AEMeasurable.mk ψ hψ (g ω)), (AEMeasurable.mk ψ hψ ∘ g) ω = (ψ ∘ g) ω
⊢ AEMeasurable.mk ψ hψ ∘ g =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] ψ ∘ g

Tactic:
filter_upwards [haψ] with ω hωψ
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
mγ : MeasurableSpace γ
mγ' : MeasurableSpace γ'
φ : β → γ
ψ : β' → γ'
hfg : IndepFun f g κ μ
hf : AEMeasurable (_m := mΩ) f ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
hg : AEMeasurable (_m := mΩ) g ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
hφ : AEMeasurable (_m := mβ) φ (Measure.map f ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ))
hψ : AEMeasurable (_m := mβ') ψ (Measure.map g ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ))
h : IndepFun (AEMeasurable.mk φ hφ ∘ f) (AEMeasurable.mk ψ hψ ∘ g) κ μ
hφ_ae : ∀ᵐ (x : Ω) ∂(⇑κ : (a : α) → Measure Ω) ∘ₘ μ, φ (f x) = AEMeasurable.mk φ hφ (f x)
hψ_ae : ∀ᵐ (x : Ω) ∂(⇑κ : (a : α) → Measure Ω) ∘ₘ μ, ψ (g x) = AEMeasurable.mk ψ hψ (g x)
a : α
haψ : ∀ᵐ (ω : Ω) ∂((κ : (a : α) → Measure Ω) a : Measure Ω), ψ (g ω) = AEMeasurable.mk ψ hψ (g ω)
ω : Ω
hωψ : ψ (g ω) = AEMeasurable.mk ψ hψ (g ω)
⊢ (AEMeasurable.mk ψ hψ ∘ g) ω = (ψ ∘ g) ω

Tactic:
simp [hωψ]
-- 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 α
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst : IsZeroOrMarkovKernel κ
c : β'
X : Ω → β
rw : Indep ⊥ (MeasurableSpace.comap X mβ) κ μ
⊢ IndepFun.{u_1, u_2, u_5, u_4} (β := β') (fun (x : Ω) ↦ c) X κ μ

Tactic:
rw [IndepFun, MeasurableSpace.comap_const]

Premises used: MeasurableSpace.comap_const, 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 α
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst : IsZeroOrMarkovKernel κ
c : β'
X : Ω → β
⊢ Indep ⊥ (MeasurableSpace.comap X mβ) κ μ

Tactic:
indep_bot_left _

Premises used: ProbabilityTheory.Kernel.indep_bot_left
-- 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 α
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst : IsZeroOrMarkovKernel κ
c : β'
X : Ω → β
⊢ Indep ⊥ (MeasurableSpace.comap X mβ) κ μ

Tactic:
exact indep_bot_left _

Premises used: ProbabilityTheory.Kernel.indep_bot_left
-- 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 α
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst : IsZeroOrMarkovKernel κ
X : Ω → β
c : β'
⊢ IndepFun.{u_1, u_2, u_4, u_5} (γ := β') X (fun (x : Ω) ↦ c) κ μ

Tactic:
(indepFun_const_left c X).symm

Premises used: ProbabilityTheory.Kernel.indepFun_const_left, ProbabilityTheory.Kernel.IndepFun.symm