awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (goal)
Goal:
Ω : Type u_1
β : Type u_3
β' : Type u_4
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
γ : Type u_5
mγ : MeasurableSpace γ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst_2 : StandardBorelSpace β
inst_3 : Nonempty β
inst_4 : StandardBorelSpace β'
inst_5 : Nonempty β'
hf : Measurable f
hg : Measurable g
k : Ω → γ
hk : Measurable k
e : γ × β' × β ≃ᵐ (γ × β') × β := MeasurableEquiv.symm MeasurableEquiv.prodAssoc
h_eq :
  Eq (α := Measure ((γ × β') × β))
    (Measure.bind (mα := mγ) (Measure.map k μ)
      (⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) : (a : γ) → Measure ((γ × β') × β)))
    (Measure.bind (α := γ × β') (mα := Prod.instMeasurableSpace) (Measure.map (fun (a : Ω) ↦ (k a, g a)) μ)
      (⇑(Kernel.id ×ₖ Kernel.prodMkRight β' (condDistrib f k μ)) : (a : γ × β') → Measure ((γ × β') × β)))
h1 :
  Eq (α := Measure ((γ × β') × β)) (Measure.map (fun (x : Ω) ↦ ((k x, g x), f x)) μ)
    (Measure.map (α := γ × β' × β) (⇑e : (a : γ × β' × β) → (γ × β') × β)
      (Measure.map (fun (a : Ω) ↦ (k a, g a, f a)) μ))
rw :
  Eq (α := Measure (γ × β' × β)) (Measure.map (fun (a : Ω) ↦ (k a, g a, f a)) μ)
    (Measure.map (α := (γ × β') × β) (⇑e.symm : (a : (γ × β') × β) → γ × β' × β)
      (Measure.map (α := γ × β' × β) (⇑e : (a : γ × β' × β) → (γ × β') × β)
        (Measure.map (fun (a : Ω) ↦ (k a, g a, f a)) μ)))
rw₁ :
  Eq (α := Measure (γ × β' × β)) (Measure.map (fun (a : Ω) ↦ (k a, g a, f a)) μ)
    (Measure.map (α := γ × β' × β)
      (Function.comp (β := (γ × β') × β) (⇑e.symm : (a : (γ × β') × β) → γ × β' × β)
        (⇑e : (a : γ × β' × β) → (γ × β') × β))
      (Measure.map (fun (a : Ω) ↦ (k a, g a, f a)) μ))
rw₂ :
  Eq (α := Measure (γ × β' × β)) (Measure.map (fun (a : Ω) ↦ (k a, g a, f a)) μ)
    (Measure.map id (Measure.map (fun (a : Ω) ↦ (k a, g a, f a)) μ))
⊢ Eq (α := Measure (γ × β' × β)) (Measure.map (fun (a : Ω) ↦ (k a, g a, f a)) μ)
    (Measure.map (α := (γ × β') × β) (⇑e.symm : (a : (γ × β') × β) → γ × β' × β)
      (Measure.map (fun (x : Ω) ↦ ((k x, g x), f x)) μ))
have rw₃ : Eq (α := Measure (γ × β' × β)) (Measure.map (fun (a : Ω) ↦ (k a, g a, f a)) μ)
  (Measure.map (fun (a : Ω) ↦ (k a, g a, f a)) μ)
Tactic: rw [h1, Measure.map_map (by fun_prop) (by fun_prop), MeasurableEquiv.symm_comp_self,
      Measure.map_id]
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (hypothesis)
Goal:
Ω : Type u_1
β : Type u_3
β' : Type u_4
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
γ : Type u_5
mγ : MeasurableSpace γ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst_2 : StandardBorelSpace β
inst_3 : Nonempty β
inst_4 : StandardBorelSpace β'
inst_5 : Nonempty β'
hf : Measurable f
hg : Measurable g
k : Ω → γ
hk : Measurable k
e : γ × β' × β ≃ᵐ (γ × β') × β := MeasurableEquiv.symm MeasurableEquiv.prodAssoc
h_eq :
  Eq (α := Measure ((γ × β') × β))
    (Measure.bind (mα := mγ) (Measure.map k μ)
      (⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) : (a : γ) → Measure ((γ × β') × β)))
    (Measure.bind (α := γ × β') (mα := Prod.instMeasurableSpace) (Measure.map (fun (a : Ω) ↦ (k a, g a)) μ)
      (⇑(Kernel.id ×ₖ Kernel.prodMkRight β' (condDistrib f k μ)) : (a : γ × β') → Measure ((γ × β') × β)))
h1 :
  Eq (α := Measure ((γ × β') × β)) (Measure.map (fun (x : Ω) ↦ ((k x, g x), f x)) μ)
    (Measure.map (α := γ × β' × β) (⇑e : (a : γ × β' × β) → (γ × β') × β)
      (Measure.map (fun (a : Ω) ↦ (k a, g a, f a)) μ))
⊢ Eq (α := Measure (γ × β' × β)) (Measure.map (fun (ω : Ω) ↦ (k ω, g ω, f ω)) μ)
      (Measure.bind (mα := mγ) (Measure.map k μ)
        (⇑(Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)) : (a : γ) → Measure (γ × β' × β))) ↔
    Eq (α := Measure ((γ × β') × β)) (Measure.map (fun (x : Ω) ↦ ((k x, g x), f x)) μ)
      (Measure.bind (mα := mγ) (Measure.map k μ)
        (⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) : (a : γ) → Measure ((γ × β') × β)))
have h1_symm : Eq (α := Measure (γ × β' × β)) (Measure.map (fun (a : Ω) ↦ (k a, g a, f a)) μ)
  (Measure.map (α := (γ × β') × β) (⇑e.symm : (a : (γ × β') × β) → γ × β' × β)
    (Measure.map (fun (x : Ω) ↦ ((k x, g x), f x)) μ))
Tactic: have h1_symm : μ.map (fun a ↦ (k a, g a, f a)) =
      (μ.map (fun x ↦ ((k x, g x), f x))).map e.symm := by
    rw [h1, Measure.map_map (by fun_prop) (by fun_prop), MeasurableEquiv.symm_comp_self,
      Measure.map_id]
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (goal)
Goal:
Ω : Type u_1
β : Type u_3
β' : Type u_4
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
γ : Type u_5
mγ : MeasurableSpace γ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst_2 : StandardBorelSpace β
inst_3 : Nonempty β
inst_4 : StandardBorelSpace β'
inst_5 : Nonempty β'
hf : Measurable f
hg : Measurable g
k : Ω → γ
hk : Measurable k
e : γ × β' × β ≃ᵐ (γ × β') × β := MeasurableEquiv.symm MeasurableEquiv.prodAssoc
h_eq :
  Eq (α := Measure ((γ × β') × β))
    (Measure.bind (mα := mγ) (Measure.map k μ)
      (⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) : (a : γ) → Measure ((γ × β') × β)))
    (Measure.bind (α := γ × β') (mα := Prod.instMeasurableSpace) (Measure.map (fun (a : Ω) ↦ (k a, g a)) μ)
      (⇑(Kernel.id ×ₖ Kernel.prodMkRight β' (condDistrib f k μ)) : (a : γ × β') → Measure ((γ × β') × β)))
h1 :
  Eq (α := Measure ((γ × β') × β)) (Measure.map (fun (x : Ω) ↦ ((k x, g x), f x)) μ)
    (Measure.map (α := γ × β' × β) (⇑e : (a : γ × β' × β) → (γ × β') × β)
      (Measure.map (fun (a : Ω) ↦ (k a, g a, f a)) μ))
h1_symm :
  Eq (α := Measure (γ × β' × β)) (Measure.map (fun (a : Ω) ↦ (k a, g a, f a)) μ)
    (Measure.map (α := (γ × β') × β) (⇑e.symm : (a : (γ × β') × β) → γ × β' × β)
      (Measure.map (fun (x : Ω) ↦ ((k x, g x), f x)) μ))
⊢ Eq (α := Measure ((γ × β') × β))
    (Measure.bind (mα := mγ) (Measure.map k μ)
      (⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) : (a : γ) → Measure ((γ × β') × β)))
    (Measure.map (α := γ × β' × β) (⇑e : (a : γ × β' × β) → (γ × β') × β)
      (Measure.bind (mα := mγ) (Measure.map k μ)
        (⇑(Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)) : (a : γ) → Measure (γ × β' × β))))
have rw : Eq (α := Measure ((γ × β') × β))
  (Measure.bind (mα := mγ) (Measure.map k μ)
    (⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) : (a : γ) → Measure ((γ × β') × β)))
  (Measure.bind (mα := mγ) (Measure.map k μ)
    (⇑(Kernel.deterministic (⇑e : (a : γ × β' × β) → (γ × β') × β) sorry ∘ₖ
          (Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ))) :
      (a : γ) → Measure ((γ × β') × β)))
Tactic: rw [← Measure.deterministic_comp_eq_map e.measurable, Measure.comp_assoc]
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (goal)
Goal:
Ω : Type u_1
β : Type u_3
β' : Type u_4
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
γ : Type u_5
mγ : MeasurableSpace γ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst_2 : StandardBorelSpace β
inst_3 : Nonempty β
inst_4 : StandardBorelSpace β'
inst_5 : Nonempty β'
hf : Measurable f
hg : Measurable g
k : Ω → γ
hk : Measurable k
e : γ × β' × β ≃ᵐ (γ × β') × β := MeasurableEquiv.symm MeasurableEquiv.prodAssoc
h_eq :
  Eq (α := Measure ((γ × β') × β))
    (Measure.bind (mα := mγ) (Measure.map k μ)
      (⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) : (a : γ) → Measure ((γ × β') × β)))
    (Measure.bind (α := γ × β') (mα := Prod.instMeasurableSpace) (Measure.map (fun (a : Ω) ↦ (k a, g a)) μ)
      (⇑(Kernel.id ×ₖ Kernel.prodMkRight β' (condDistrib f k μ)) : (a : γ × β') → Measure ((γ × β') × β)))
h1 :
  Eq (α := Measure ((γ × β') × β)) (Measure.map (fun (x : Ω) ↦ ((k x, g x), f x)) μ)
    (Measure.map (α := γ × β' × β) (⇑e : (a : γ × β' × β) → (γ × β') × β)
      (Measure.map (fun (a : Ω) ↦ (k a, g a, f a)) μ))
h1_symm :
  Eq (α := Measure (γ × β' × β)) (Measure.map (fun (a : Ω) ↦ (k a, g a, f a)) μ)
    (Measure.map (α := (γ × β') × β) (⇑e.symm : (a : (γ × β') × β) → γ × β' × β)
      (Measure.map (fun (x : Ω) ↦ ((k x, g x), f x)) μ))
⊢ Eq (α := Measure ((γ × β') × β))
    (Measure.bind (mα := mγ) (Measure.map k μ)
      (⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) : (a : γ) → Measure ((γ × β') × β)))
    (Measure.bind (mα := mγ) (Measure.map k μ)
      (⇑(Kernel.deterministic (⇑e : (a : γ × β' × β) → (γ × β') × β) ⋯ ∘ₖ
            (Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ))) :
        (a : γ) → Measure ((γ × β') × β)))
have e_f : Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ =
  Kernel.deterministic (⇑e : (a : γ × β' × β) → (γ × β') × β) sorry ∘ₖ
    (Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ))
Tactic: congr 2
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (goal)
Goal:
Ω : Type u_1
β : Type u_3
β' : Type u_4
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
γ : Type u_5
mγ : MeasurableSpace γ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst_2 : StandardBorelSpace β
inst_3 : Nonempty β
inst_4 : StandardBorelSpace β'
inst_5 : Nonempty β'
hf : Measurable f
hg : Measurable g
k : Ω → γ
hk : Measurable k
e : γ × β' × β ≃ᵐ (γ × β') × β := MeasurableEquiv.symm MeasurableEquiv.prodAssoc
h_eq :
  Eq (α := Measure ((γ × β') × β))
    (Measure.bind (mα := mγ) (Measure.map k μ)
      (⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) : (a : γ) → Measure ((γ × β') × β)))
    (Measure.bind (α := γ × β') (mα := Prod.instMeasurableSpace) (Measure.map (fun (a : Ω) ↦ (k a, g a)) μ)
      (⇑(Kernel.id ×ₖ Kernel.prodMkRight β' (condDistrib f k μ)) : (a : γ × β') → Measure ((γ × β') × β)))
h1 :
  Eq (α := Measure ((γ × β') × β)) (Measure.map (fun (x : Ω) ↦ ((k x, g x), f x)) μ)
    (Measure.map (α := γ × β' × β) (⇑e : (a : γ × β' × β) → (γ × β') × β)
      (Measure.map (fun (a : Ω) ↦ (k a, g a, f a)) μ))
h1_symm :
  Eq (α := Measure (γ × β' × β)) (Measure.map (fun (a : Ω) ↦ (k a, g a, f a)) μ)
    (Measure.map (α := (γ × β') × β) (⇑e.symm : (a : (γ × β') × β) → γ × β' × β)
      (Measure.map (fun (x : Ω) ↦ ((k x, g x), f x)) μ))
⊢ Eq (α := Kernel γ ((γ × β') × β)) (Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ)
    (Kernel.deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : γ × β' × β) → (γ × β') × β) ⋯ ∘ₖ
      (Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)))
have e_f : Eq (α := Kernel γ ((γ × β') × β)) (Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ)
  (Kernel.map (mβ := Prod.instMeasurableSpace) (Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ))
    (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : γ × β' × β) → (γ × β') × β))
Tactic: rw [Kernel.deterministic_comp_eq_map, Kernel.prodAssoc_symm_prod]
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (goal)
Goal:
Ω : Type u_1
β : Type u_3
β' : Type u_4
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
γ : Type u_5
mγ : MeasurableSpace γ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst_2 : StandardBorelSpace β
inst_3 : Nonempty β
inst_4 : StandardBorelSpace β'
inst_5 : Nonempty β'
hf : Measurable f
hg : Measurable g
k : Ω → γ
hk : Measurable k
e : γ × β' × β ≃ᵐ (γ × β') × β := MeasurableEquiv.symm MeasurableEquiv.prodAssoc
h_eq :
  Eq (α := Measure ((γ × β') × β))
    (Measure.bind (mα := mγ) (Measure.map k μ)
      (⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) : (a : γ) → Measure ((γ × β') × β)))
    (Measure.bind (α := γ × β') (mα := Prod.instMeasurableSpace) (Measure.map (fun (a : Ω) ↦ (k a, g a)) μ)
      (⇑(Kernel.id ×ₖ Kernel.prodMkRight β' (condDistrib f k μ)) : (a : γ × β') → Measure ((γ × β') × β)))
h1 :
  Eq (α := Measure ((γ × β') × β)) (Measure.map (fun (x : Ω) ↦ ((k x, g x), f x)) μ)
    (Measure.map (α := γ × β' × β) (⇑e : (a : γ × β' × β) → (γ × β') × β)
      (Measure.map (fun (a : Ω) ↦ (k a, g a, f a)) μ))
h1_symm :
  Eq (α := Measure (γ × β' × β)) (Measure.map (fun (a : Ω) ↦ (k a, g a, f a)) μ)
    (Measure.map (α := (γ × β') × β) (⇑e.symm : (a : (γ × β') × β) → γ × β' × β)
      (Measure.map (fun (x : Ω) ↦ ((k x, g x), f x)) μ))
e_f :
  Eq (α := Kernel γ ((γ × β') × β)) (Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ)
    (Kernel.map (mβ := Prod.instMeasurableSpace) (Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ))
      (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : γ × β' × β) → (γ × β') × β))
⊢ Eq (α := Kernel γ ((γ × β') × β)) (Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ)
    (Kernel.deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : γ × β' × β) → (γ × β') × β) ⋯ ∘ₖ
      (Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)))
have e_f₁ : Eq (α := Kernel γ ((γ × β') × β)) (Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ)
  (Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ)
Tactic: rw [Kernel.deterministic_comp_eq_map, Kernel.prodAssoc_symm_prod]
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (hypothesis)
Goal:
Ω : Type u_1
β : Type u_3
β' : Type u_4
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
γ : Type u_5
mγ : MeasurableSpace γ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst_2 : StandardBorelSpace β
inst_3 : Nonempty β
inst_4 : StandardBorelSpace β'
inst_5 : Nonempty β'
hf : Measurable f
hg : Measurable g
k : Ω → γ
hk : Measurable k
e : γ × β' × β ≃ᵐ (γ × β') × β := MeasurableEquiv.symm MeasurableEquiv.prodAssoc
h_eq :
  Eq (α := Measure ((γ × β') × β))
    (Measure.bind (mα := mγ) (Measure.map k μ)
      (⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) : (a : γ) → Measure ((γ × β') × β)))
    (Measure.bind (α := γ × β') (mα := Prod.instMeasurableSpace) (Measure.map (fun (a : Ω) ↦ (k a, g a)) μ)
      (⇑(Kernel.id ×ₖ Kernel.prodMkRight β' (condDistrib f k μ)) : (a : γ × β') → Measure ((γ × β') × β)))
h1 :
  Eq (α := Measure ((γ × β') × β)) (Measure.map (fun (x : Ω) ↦ ((k x, g x), f x)) μ)
    (Measure.map (α := γ × β' × β) (⇑e : (a : γ × β' × β) → (γ × β') × β)
      (Measure.map (fun (a : Ω) ↦ (k a, g a, f a)) μ))
h1_symm :
  Eq (α := Measure (γ × β' × β)) (Measure.map (fun (a : Ω) ↦ (k a, g a, f a)) μ)
    (Measure.map (α := (γ × β') × β) (⇑e.symm : (a : (γ × β') × β) → γ × β' × β)
      (Measure.map (fun (x : Ω) ↦ ((k x, g x), f x)) μ))
⊢ Eq (α := Measure (γ × β' × β)) (Measure.map (fun (ω : Ω) ↦ (k ω, g ω, f ω)) μ)
      (Measure.bind (mα := mγ) (Measure.map k μ)
        (⇑(Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)) : (a : γ) → Measure (γ × β' × β))) ↔
    Eq (α := Measure ((γ × β') × β)) (Measure.map (fun (x : Ω) ↦ ((k x, g x), f x)) μ)
      (Measure.bind (mα := mγ) (Measure.map k μ)
        (⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) : (a : γ) → Measure ((γ × β') × β)))
have h2 : Eq (α := Measure ((γ × β') × β))
  (Measure.bind (mα := mγ) (Measure.map k μ)
    (⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) : (a : γ) → Measure ((γ × β') × β)))
  (Measure.map (α := γ × β' × β) (⇑e : (a : γ × β' × β) → (γ × β') × β)
    (Measure.bind (mα := mγ) (Measure.map k μ)
      (⇑(Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)) : (a : γ) → Measure (γ × β' × β))))
Tactic: have h2 : ((Kernel.id ×ₖ condDistrib g k μ) ×ₖ condDistrib f k μ) ∘ₘ μ.map k =
      ((Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)) ∘ₘ μ.map k).map e := by
    rw [← Measure.deterministic_comp_eq_map e.measurable, Measure.comp_assoc]
    congr 2
    unfold e
    rw [Kernel.deterministic_comp_eq_map, Kernel.prodAssoc_symm_prod]
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (goal)
Goal:
Ω : Type u_1
β : Type u_3
β' : Type u_4
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
γ : Type u_5
mγ : MeasurableSpace γ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst_2 : StandardBorelSpace β
inst_3 : Nonempty β
inst_4 : StandardBorelSpace β'
inst_5 : Nonempty β'
hf : Measurable f
hg : Measurable g
k : Ω → γ
hk : Measurable k
e : γ × β' × β ≃ᵐ (γ × β') × β := MeasurableEquiv.symm MeasurableEquiv.prodAssoc
h_eq :
  Eq (α := Measure ((γ × β') × β))
    (Measure.bind (mα := mγ) (Measure.map k μ)
      (⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) : (a : γ) → Measure ((γ × β') × β)))
    (Measure.bind (α := γ × β') (mα := Prod.instMeasurableSpace) (Measure.map (fun (a : Ω) ↦ (k a, g a)) μ)
      (⇑(Kernel.id ×ₖ Kernel.prodMkRight β' (condDistrib f k μ)) : (a : γ × β') → Measure ((γ × β') × β)))
h1 :
  Eq (α := Measure ((γ × β') × β)) (Measure.map (fun (x : Ω) ↦ ((k x, g x), f x)) μ)
    (Measure.map (α := γ × β' × β) (⇑e : (a : γ × β' × β) → (γ × β') × β)
      (Measure.map (fun (a : Ω) ↦ (k a, g a, f a)) μ))
h1_symm :
  Eq (α := Measure (γ × β' × β)) (Measure.map (fun (a : Ω) ↦ (k a, g a, f a)) μ)
    (Measure.map (α := (γ × β') × β) (⇑e.symm : (a : (γ × β') × β) → γ × β' × β)
      (Measure.map (fun (x : Ω) ↦ ((k x, g x), f x)) μ))
h2 :
  Eq (α := Measure ((γ × β') × β))
    (Measure.bind (mα := mγ) (Measure.map k μ)
      (⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) : (a : γ) → Measure ((γ × β') × β)))
    (Measure.map (α := γ × β' × β) (⇑e : (a : γ × β' × β) → (γ × β') × β)
      (Measure.bind (mα := mγ) (Measure.map k μ)
        (⇑(Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)) : (a : γ) → Measure (γ × β' × β))))
⊢ Eq (α := Measure (γ × β' × β))
    (Measure.bind (mα := mγ) (Measure.map k μ)
      (⇑(Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)) : (a : γ) → Measure (γ × β' × β)))
    (Measure.map (α := (γ × β') × β) (⇑e.symm : (a : (γ × β') × β) → γ × β' × β)
      (Measure.bind (mα := mγ) (Measure.map k μ)
        (⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) : (a : γ) → Measure ((γ × β') × β))))
have rw : Eq (α := Measure (γ × β' × β))
  (Measure.bind (mα := mγ) (Measure.map k μ)
    (⇑(Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)) : (a : γ) → Measure (γ × β' × β)))
  (Measure.map (α := (γ × β') × β) (⇑e.symm : (a : (γ × β') × β) → γ × β' × β)
    (Measure.map (α := γ × β' × β) (⇑e : (a : γ × β' × β) → (γ × β') × β)
      (Measure.bind (mα := mγ) (Measure.map k μ)
        (⇑(Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)) : (a : γ) → Measure (γ × β' × β)))))
Tactic: rw [h2, Measure.map_map (by fun_prop) (by fun_prop), MeasurableEquiv.symm_comp_self,
      Measure.map_id]
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (hypothesis)
Goal:
Ω : Type u_1
β : Type u_3
β' : Type u_4
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
γ : Type u_5
mγ : MeasurableSpace γ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst_2 : StandardBorelSpace β
inst_3 : Nonempty β
inst_4 : StandardBorelSpace β'
inst_5 : Nonempty β'
hf : Measurable f
hg : Measurable g
k : Ω → γ
hk : Measurable k
e : γ × β' × β ≃ᵐ (γ × β') × β := MeasurableEquiv.symm MeasurableEquiv.prodAssoc
h_eq :
  Eq (α := Measure ((γ × β') × β))
    (Measure.bind (mα := mγ) (Measure.map k μ)
      (⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) : (a : γ) → Measure ((γ × β') × β)))
    (Measure.bind (α := γ × β') (mα := Prod.instMeasurableSpace) (Measure.map (fun (a : Ω) ↦ (k a, g a)) μ)
      (⇑(Kernel.id ×ₖ Kernel.prodMkRight β' (condDistrib f k μ)) : (a : γ × β') → Measure ((γ × β') × β)))
h1 :
  Eq (α := Measure ((γ × β') × β)) (Measure.map (fun (x : Ω) ↦ ((k x, g x), f x)) μ)
    (Measure.map (α := γ × β' × β) (⇑e : (a : γ × β' × β) → (γ × β') × β)
      (Measure.map (fun (a : Ω) ↦ (k a, g a, f a)) μ))
h1_symm :
  Eq (α := Measure (γ × β' × β)) (Measure.map (fun (a : Ω) ↦ (k a, g a, f a)) μ)
    (Measure.map (α := (γ × β') × β) (⇑e.symm : (a : (γ × β') × β) → γ × β' × β)
      (Measure.map (fun (x : Ω) ↦ ((k x, g x), f x)) μ))
h2 :
  Eq (α := Measure ((γ × β') × β))
    (Measure.bind (mα := mγ) (Measure.map k μ)
      (⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) : (a : γ) → Measure ((γ × β') × β)))
    (Measure.map (α := γ × β' × β) (⇑e : (a : γ × β' × β) → (γ × β') × β)
      (Measure.bind (mα := mγ) (Measure.map k μ)
        (⇑(Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)) : (a : γ) → Measure (γ × β' × β))))
⊢ Eq (α := Measure (γ × β' × β)) (Measure.map (fun (ω : Ω) ↦ (k ω, g ω, f ω)) μ)
      (Measure.bind (mα := mγ) (Measure.map k μ)
        (⇑(Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)) : (a : γ) → Measure (γ × β' × β))) ↔
    Eq (α := Measure ((γ × β') × β)) (Measure.map (fun (x : Ω) ↦ ((k x, g x), f x)) μ)
      (Measure.bind (mα := mγ) (Measure.map k μ)
        (⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) : (a : γ) → Measure ((γ × β') × β)))
have h2_symm : Eq (α := Measure (γ × β' × β))
  (Measure.bind (mα := mγ) (Measure.map k μ)
    (⇑(Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)) : (a : γ) → Measure (γ × β' × β)))
  (Measure.map (α := (γ × β') × β) (⇑e.symm : (a : (γ × β') × β) → γ × β' × β)
    (Measure.bind (mα := mγ) (Measure.map k μ)
      (⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) : (a : γ) → Measure ((γ × β') × β))))
Tactic: have h2_symm : (Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)) ∘ₘ μ.map k =
      (((Kernel.id ×ₖ condDistrib g k μ) ×ₖ condDistrib f k μ) ∘ₘ μ.map k).map e.symm := by
    rw [h2, Measure.map_map (by fun_prop) (by fun_prop), MeasurableEquiv.symm_comp_self,
      Measure.map_id]
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (hypothesis)
Goal:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
β : ι → Type u_5
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
h_indep : iCondIndepFun m' hm' (β := β) f μ
hf : ∀ (i : ι), Measurable (f i)
i j k l : ι
hik : i ≠ k
hil : i ≠ l
hjk : j ≠ k
hjl : j ≠ l
g : (i j : ι) → (v : (x : ↥{i, j}) → β (↑x : ι)) → β i × β j :=
  fun (i j : ι) (v : (x : ↥{i, j}) → β (↑x : ι)) ↦
    (v (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i, j} x) i ⋯),
      v (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i, j} x) j ⋯))
⊢ CondIndepFun.{u_1, u_5, u_5} m' hm' (β := β i × β j) (γ := β k × β l) (fun (a : Ω) ↦ (f i a, f j a))
    (fun (a : Ω) ↦ (f k a, f l a)) μ
have hg : ∀ (i j : ι), Measurable (g i j)
Tactic: have hg (i j : ι) : Measurable (g i j) := by fun_prop
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
β : ι → Type u_5
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
h_indep : iCondIndepFun m' hm' (β := β) f μ
hf : ∀ (i : ι), Measurable (f i)
i j k l : ι
hik : i ≠ k
hil : i ≠ l
hjk : j ≠ k
hjl : j ≠ l
let let₁ let₂ :
  CondIndepFun.{u_1, u_5, u_5} m' hm' (β := β i × β j) (γ := β k × β l) (fun (a : Ω) ↦ (f i a, f j a))
    (fun (a : Ω) ↦ (f k a, f l a)) μ
⊢ CondIndepFun.{u_1, u_5, u_5} m' hm' (β := β i × β j) (γ := β k × β l) (fun (a : Ω) ↦ (f i a, f j a))
    (fun (a : Ω) ↦ (f k a, f l a)) μ
have let₃ : let g : (i j : ι) → (v : (x : ↥{i, j}) → β (↑x : ι)) → β i × β j := fun (i j : ι) (v : (x : ↥{i, j}) → β (↑x : ι)) ↦
  (v (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i, j} x) i sorry),
    v (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i, j} x) j sorry));
∀ (hg : ∀ (i j : ι), Measurable (g i j)),
  CondIndepFun.{u_1, u_5, u_5} m' hm' (β := β i × β j) (γ := β k × β l) (fun (a : Ω) ↦ (f i a, f j a))
    (fun (a : Ω) ↦ (f k a, f l a)) μ
Tactic: classical
  let g (i j : ι) (v : Π x : ({i, j} : Finset ι), β x) : β i × β j :=
    ⟨v ⟨i, mem_insert_self _ _⟩, v ⟨j, mem_insert_of_mem <| mem_singleton_self _⟩⟩
  have hg (i j : ι) : Measurable (g i j) := by fun_prop
  exact (h_indep.indepFun_finset {i, j} {k, l} (by aesop) hf).comp (hg i j) (hg k l)