awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.IndepFun (hypothesis)
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)
⊢ (((κ : (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)
have h1 : f ⁻¹' A =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] f' ⁻¹' A
Tactic: have h1 : f ⁻¹' A =ᵐ[κ a] f' ⁻¹' A := hf'.fun_comp A
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.IndepFun (hypothesis)
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
⊢ (((κ : (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)
have h2 : g ⁻¹' B =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] g' ⁻¹' B
Tactic: have h2 : g ⁻¹' B =ᵐ[κ a] g' ⁻¹' B := hg'.fun_comp B
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.IndepFun (goal)
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
⊢ (((κ : (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)
have 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)
Tactic: rwa [← measure_congr h1, ← measure_congr h2, ← measure_congr (h1.inter h2)]
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.IndepFun (goal)
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)
⊢ (((κ : (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)
have 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)
Tactic: rwa [← measure_congr h1, ← measure_congr h2, ← measure_congr (h1.inter h2)]
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.IndepFun (goal)
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 : α) ∂μ,
    (((κ : (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)
have a : Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} (φ ∘ f ⁻¹' A)
Tactic: apply hfg
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.IndepFun (goal)
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 : α) ∂μ,
    (((κ : (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)
have a₁ : Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} (ψ ∘ g ⁻¹' B)
Tactic: apply hfg
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.IndepFun (hypothesis)
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 (φ ∘ f) (ψ ∘ g) κ μ
have h : 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
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.IndepFun (hypothesis)
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) κ μ
⊢ IndepFun (φ ∘ f) (ψ ∘ g) κ μ
have hφ_ae : ∀ᵐ (x : Ω) ∂(⇑κ : (a : α) → Measure Ω) ∘ₘ μ, φ (f x) = AEMeasurable.mk φ hφ (f x)
Tactic: have hφ_ae := ae_of_ae_map hf hφ.ae_eq_mk
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.IndepFun (hypothesis)
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)
⊢ IndepFun (φ ∘ f) (ψ ∘ g) κ μ
have hψ_ae : ∀ᵐ (x : Ω) ∂(⇑κ : (a : α) → Measure Ω) ∘ₘ μ, ψ (g x) = AEMeasurable.mk ψ hψ (g x)
Tactic: have hψ_ae := ae_of_ae_map hg hψ.ae_eq_mk
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.IndepFun (goal)
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) κ μ
have refine_1 : ∀ᵐ (a : α) ∂μ, AEMeasurable.mk φ hφ ∘ f =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] φ ∘ f
Tactic: refine IndepFun.congr' h ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.IndepFun (goal)
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
⊢ IndepFun (φ ∘ f) (ψ ∘ g) κ μ
have refine_2 : ∀ᵐ (a : α) ∂μ, AEMeasurable.mk ψ hψ ∘ g =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] ψ ∘ g
Tactic: refine IndepFun.congr' h ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.IndepFun (goal)
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 : α) ∂μ, AEMeasurable.mk φ hφ ∘ f =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] φ ∘ f
have h₁ : ∀ (a : α) (haφ : ∀ᵐ (ω : Ω) ∂((κ : (a : α) → Measure Ω) a : Measure Ω), φ (f ω) = AEMeasurable.mk φ hφ (f ω)),
  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φ
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.IndepFun (goal)
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 ω)
⊢ AEMeasurable.mk φ hφ ∘ f =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] φ ∘ f
have h₁ : ∀ (ω : Ω) (hωφ : φ (f ω) = AEMeasurable.mk φ hφ (f ω)), (AEMeasurable.mk φ hφ ∘ f) ω = (φ ∘ f) ω
Tactic: filter_upwards [haφ] with ω hωφ
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.IndepFun (goal)
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 : α) ∂μ, AEMeasurable.mk ψ hψ ∘ g =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] ψ ∘ g
have h₁ : ∀ (a : α) (haψ : ∀ᵐ (ω : Ω) ∂((κ : (a : α) → Measure Ω) a : Measure Ω), ψ (g ω) = AEMeasurable.mk ψ hψ (g ω)),
  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ψ
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.IndepFun (goal)
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 ω)
⊢ AEMeasurable.mk ψ hψ ∘ g =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] ψ ∘ g
have h₁ : ∀ (ω : Ω) (hωψ : ψ (g ω) = AEMeasurable.mk ψ hψ (g ω)), (AEMeasurable.mk ψ hψ ∘ g) ω = (ψ ∘ g) ω
Tactic: filter_upwards [haψ] with ω hωψ
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.IndepFun (goal)
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 : Ω → β
⊢ IndepFun.{u_1, u_2, u_5, u_4} (β := β') (fun (x : Ω) ↦ c) X κ μ
have rw : Indep ⊥ (MeasurableSpace.comap X mβ) κ μ
Tactic: rw [IndepFun, MeasurableSpace.comap_const]
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.IndepFun (goal)
Goal:
α : Type u_1
Ω : Type u_2
β : Type u_4
γ : Type u_6
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : IsFiniteMeasure μ
inst_1 : IsFiniteKernel κ
f : Ω → β
g : Ω → γ
hf : Measurable f
hg : Measurable g
⊢ IndepFun f g κ μ ↔ Eq (α := Measure (α × β × γ)) (μ ⊗ₘ κ.map fun (ω : Ω) ↦ (f ω, g ω)) (μ ⊗ₘ (κ.map f ×ₖ κ.map g))
have rw : (∀ (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)) ↔
  Eq (α := Measure (α × β × γ)) (μ ⊗ₘ κ.map fun (ω : Ω) ↦ (f ω, g ω)) (μ ⊗ₘ (κ.map f ×ₖ κ.map g))
Tactic: rw [indepFun_iff_measure_inter_preimage_eq_mul]
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.IndepFun (goal)
Goal:
α : Type u_1
Ω : Type u_2
β : Type u_4
γ : Type u_6
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : IsFiniteMeasure μ
inst_1 : IsFiniteKernel κ
f : Ω → β
g : Ω → γ
hf : Measurable f
hg : Measurable g
⊢ (∀ (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)) ↔
    Eq (α := Measure (α × β × γ)) (μ ⊗ₘ κ.map fun (ω : Ω) ↦ (f ω, g ω)) (μ ⊗ₘ (κ.map f ×ₖ κ.map g))
have refine_1 : ∀
  (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)),
  Eq (α := Measure (α × β × γ)) (μ ⊗ₘ κ.map fun (ω : Ω) ↦ (f ω, g ω)) (μ ⊗ₘ (κ.map f ×ₖ κ.map g))
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩