awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.IndepFun (goal)
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
mβ : (i : ι) → MeasurableSpace (β i)
f g : (i : ι) → Ω → β i
hf :
  ∀ (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)
h : ∀ (i : ι), ∀ᵐ (a : α) ∂μ, f i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] g i
S : Finset ι
sets : (i : ι) → Set (β i)
hmeas : ∀ i ∈ S, MeasurableSet (sets i)
this : ∀ᵐ (a : α) ∂μ, ∀ i ∈ S, f i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] g i
a : α
ha : ∀ i ∈ S, f i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] g i
h'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)
A :
  ∀ (i : ι) (hi : i ∈ S),
    Eq (α := ENNReal) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (g i ⁻¹' sets i) : ENNReal)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f i ⁻¹' sets i) : ENNReal)
⊢ Eq (α := ENNReal)
    ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ i ∈ S, g i ⁻¹' sets i) : ENNReal)
    ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ i ∈ S, f i ⁻¹' sets i) : ENNReal)
have H : ⋂ i ∈ S, g i ⁻¹' sets i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] ⋂ i ∈ S, f i ⁻¹' sets i
Tactic: apply measure_congr
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.IndepFun (goal)
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
mβ : (i : ι) → MeasurableSpace (β i)
f g : (i : ι) → Ω → β i
hf :
  ∀ (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)
h : ∀ (i : ι), ∀ᵐ (a : α) ∂μ, f i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] g i
S : Finset ι
sets : (i : ι) → Set (β i)
hmeas : ∀ i ∈ S, MeasurableSet (sets i)
this : ∀ᵐ (a : α) ∂μ, ∀ i ∈ S, f i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] g i
a : α
ha : ∀ i ∈ S, f i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] g i
h'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)
A :
  ∀ (i : ι) (hi : i ∈ S),
    Eq (α := ENNReal) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (g i ⁻¹' sets i) : ENNReal)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f i ⁻¹' sets i) : ENNReal)
⊢ ⋂ i ∈ S, g i ⁻¹' sets i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] ⋂ i ∈ S, f i ⁻¹' sets i
have h₁ : ∀ (ω : Ω) (hω : ∀ (i : ι) (hi : i ∈ (↑S : Set ι)), f i ω = g i ω),
  (⋂ (i : ι) (_ : i ∈ S), g i ⁻¹' sets i) ω = (⋂ (i : ι) (_ : i ∈ S), f i ⁻¹' sets i) ω
Tactic: filter_upwards [(ae_ball_iff (Finset.countable_toSet S)).2 ha] with ω hω
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.IndepFun (hypothesis)
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
mβ : (i : ι) → MeasurableSpace (β i)
f g : (i : ι) → Ω → β i
hf :
  ∀ (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)
h : ∀ (i : ι), ∀ᵐ (a : α) ∂μ, f i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] g i
S : Finset ι
sets : (i : ι) → Set (β i)
hmeas : ∀ i ∈ S, MeasurableSet (sets i)
this : ∀ᵐ (a : α) ∂μ, ∀ i ∈ S, f i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] g i
a : α
ha : ∀ i ∈ S, f i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] g i
h'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)
A :
  ∀ (i : ι) (hi : i ∈ S),
    Eq (α := ENNReal) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (g i ⁻¹' sets i) : ENNReal)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f i ⁻¹' sets i) : ENNReal)
⊢ Eq (α := ENNReal)
    ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ i ∈ S, g i ⁻¹' sets i) : ENNReal)
    (∏ i ∈ S, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (g i ⁻¹' sets i) : ENNReal)
have B : Eq (α := ENNReal)
  ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ i ∈ S, g i ⁻¹' sets i) : ENNReal)
  ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ i ∈ S, f i ⁻¹' sets i) : ENNReal)
Tactic: have B : (κ a) (⋂ i ∈ S, g i ⁻¹' sets i) = (κ a) (⋂ i ∈ S, f i ⁻¹' sets i) := by
    apply measure_congr
    filter_upwards [(ae_ball_iff (Finset.countable_toSet S)).2 ha] with ω hω
    change (ω ∈ ⋂ i ∈ S, g i ⁻¹' sets i) = (ω ∈ ⋂ i ∈ S, f i ⁻¹' sets i)
    simp +contextual [hω]
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.IndepFun (goal)
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
mβ : (i : ι) → MeasurableSpace (β i)
f g : (i : ι) → Ω → β i
h : ∀ (i : ι), ∀ᵐ (a : α) ∂μ, f i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] g i
h' : iIndepFun (β := β) g κ μ
⊢ iIndepFun (β := β) f κ μ
have refine : ∀ (i : ι), ∀ᵐ (a : α) ∂μ, g i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] f i
Tactic: refine h'.congr' fun i ↦ ?_
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.IndepFun (goal)
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
mβ : (i : ι) → MeasurableSpace (β i)
f g : (i : ι) → Ω → β i
h : ∀ (i : ι), ∀ᵐ (a : α) ∂μ, f i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] g i
h' : iIndepFun (β := β) g κ μ
i : ι
⊢ ∀ᵐ (a : α) ∂μ, g i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] f i
have h₁ : ∀ (a : α),
  Membership.mem (γ := Set α)
    {x : α |
      Membership.mem (γ := Set α)
          {x : α | (fun (a : α) ↦ f i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] g i) x} x →
        Membership.mem (γ := Set α)
          {x : α | (fun (a : α) ↦ g i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] f i) x} x}
    a
Tactic: filter_upwards [h i] with a ha using ha.symm
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.IndepFun (goal)
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
mβ : (i : ι) → MeasurableSpace (β i)
f g : (i : ι) → Ω → β i
h : ∀ (i : ι), ∀ᵐ (a : α) ∂μ, f i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] g i
h' : iIndepFun (β := β) g κ μ
i : ι
h₁ :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α)
            {x : α | (fun (a : α) ↦ f i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] g i) x} x →
          Membership.mem (γ := Set α)
            {x : α | (fun (a : α) ↦ g i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] f i) x} x}
      a
⊢ ∀ᵐ (a : α) ∂μ, g i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] f i
have h₂ : ∀ (a : α),
  f i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] g i →
    g i =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] f i
Tactic: filter_upwards [h i] with a ha using ha.symm
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.IndepFun (goal)
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
hg : ∀ (i : ι), Measurable (g i)
⊢ iIndepFun (β := γ) (fun (i : ι) ↦ g i ∘ f i) κ μ
have rw : ∀
  (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)) (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: rw [iIndepFun_iff_measure_inter_preimage_eq_mul] at h ⊢
Cleared hypotheses: h, g, hg
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.IndepFun (hypothesis)
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, g i ∘ f i ⁻¹' s i) : ENNReal)
      (∏ i ∈ t, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (g i ∘ f i ⁻¹' s i) : ENNReal)
have 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)
Tactic: have := h t (sets := fun i ↦ g i ⁻¹' (s i)) (fun i a ↦ hg i (hs i a))
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.IndepFun (goal)
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 : α) ∂μ,
    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)
have 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)
Tactic: filter_upwards [this] with a ha
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.IndepFun (hypothesis)
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 : ι) ↦ g i ∘ f i) κ μ
have h₁ : iIndepFun (β := γ) (fun (i : ι) ↦ AEMeasurable.mk (g i) sorry ∘ 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
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.IndepFun (hypothesis)
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) κ μ
⊢ iIndepFun (β := γ) (fun (i : ι) ↦ g i ∘ f i) κ μ
have h_ae : ∀ (i : ι), ∀ᵐ (x : Ω) ∂(⇑κ : (a : α) → Measure Ω) ∘ₘ μ, AEMeasurable.mk (g i) sorry (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
-- 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 β'
inst : IsZeroOrMarkovKernel κ
hf : Measurable f
hg : Measurable g
⊢ IndepFun f g κ μ ↔ ∀ (s : Set β) (t : Set β'), MeasurableSet s → MeasurableSet t → IndepSet (f ⁻¹' s) (g ⁻¹' t) κ μ
have 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) κ μ
Tactic: refine indepFun_iff_measure_inter_preimage_eq_mul.trans ?_
-- 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 β'
inst : IsZeroOrMarkovKernel κ
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)) ↔
    ∀ (s : Set β) (t : Set β'), MeasurableSet s → MeasurableSet t → IndepSet (f ⁻¹' s) (g ⁻¹' t) κ μ
have 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) κ μ
Tactic: constructor
-- 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 β'
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) κ μ
⊢ (∀ (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) κ μ
have 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)
Tactic: constructor
-- 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 β'
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
⊢ IndepSet (f ⁻¹' s) (g ⁻¹' t) κ μ
have h₁ : ∀ᵐ (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
Cleared hypotheses: h
-- 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 β'
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
⊢ ∀ᵐ (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)
have h₁ : IndepSet (f ⁻¹' s) (g ⁻¹' t) κ μ
Tactic: specialize h s t hs ht
Cleared hypotheses: 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 α
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 : α) ∂μ,
    (((κ : (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 : α) (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)
Tactic: filter_upwards [hf, hg, hfg _ _ ⟨_, hA, rfl⟩ ⟨_, hB, rfl⟩] with a hf' hg' hfg'