awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Independence.Conditional
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 ((γ × β') × β)))
⊢ Measurable (α := γ × β' × β) (β := (γ × β') × β) (⇑e : (a : γ × β' × β) → (γ × β') × β)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Independence.Conditional
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 ((γ × β') × β)))
⊢ Measurable (β := γ × β' × β) fun (a : Ω) ↦ (k a, g a, f a)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Independence.Conditional
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 ((γ × β') × β)))
rw :
  Eq (α := Measure ((γ × β') × β)) (Measure.map (fun (x : Ω) ↦ ((k x, g x), f x)) μ)
    (Measure.map (Function.comp (β := γ × β' × β) (⇑e : (a : γ × β' × β) → (γ × β') × β) fun (a : Ω) ↦ (k a, g a, f a))
      μ)
⊢ 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)) μ))

Tactic:
rw [Measure.map_map (by fun_prop) (by fun_prop)]

Premises used: MeasureTheory.Measure.map_map
-- Module: Mathlib.Probability.Independence.Conditional
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 ((γ × β') × β)))
⊢ Eq (α := Measure ((γ × β') × β)) (Measure.map (fun (x : Ω) ↦ ((k x, g x), f x)) μ)
    (Measure.map (Function.comp (β := γ × β' × β) (⇑e : (a : γ × β' × β) → (γ × β') × β) fun (a : Ω) ↦ (k a, g a, f a))
      μ)

Tactic:
rfl
-- Module: Mathlib.Probability.Independence.Conditional
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 ((γ × β') × β)))
⊢ 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)) μ))

Tactic:
have h1 : μ.map (fun x ↦ ((k x, g x), f x)) = (μ.map (fun a ↦ (k a, g a, f a))).map e := by
    rw [Measure.map_map (by fun_prop) (by fun_prop)]
    rfl
-- Module: Mathlib.Probability.Independence.Conditional
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)) μ))
⊢ Measurable (α := (γ × β') × β) (β := γ × β' × β) (⇑e.symm : (a : (γ × β') × β) → γ × β' × β)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Independence.Conditional
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)) μ))
⊢ Measurable (α := γ × β' × β) (β := (γ × β') × β) (⇑e : (a : γ × β' × β) → (γ × β') × β)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Independence.Conditional
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)) μ))
rw₃ rw₄ :
  Eq (α := Measure (γ × β' × β)) (Measure.map (fun (a : Ω) ↦ (k a, g a, f a)) μ)
    (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)) μ))

Tactic:
rw [h1, Measure.map_map (by fun_prop) (by fun_prop), MeasurableEquiv.symm_comp_self,
      Measure.map_id]

Premises used: MeasureTheory.Measure.map_id, MeasurableEquiv.symm_comp_self, MeasureTheory.Measure.map_map
-- Module: Mathlib.Probability.Independence.Conditional
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 (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]
-- Module: Mathlib.Probability.Independence.Conditional
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)) μ))
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 : γ × β' × β) → (γ × β') × β) ⋯ ∘ₖ
            (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 : (a : γ × β' × β) → (γ × β') × β)
      (Measure.bind (mα := mγ) (Measure.map k μ)
        (⇑(Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)) : (a : γ) → Measure (γ × β' × β))))

Tactic:
rw [← Measure.deterministic_comp_eq_map e.measurable, Measure.comp_assoc]

Premises used: MeasureTheory.Measure.deterministic_comp_eq_map, MeasureTheory.Measure.comp_assoc, MeasurableEquiv.measurable
-- Module: Mathlib.Probability.Independence.Conditional
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 :
  Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ =
    Kernel.deterministic (⇑e : (a : γ × β' × β) → (γ × β') × β) ⋯ ∘ₖ
      (Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ))
⊢ 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 ((γ × β') × β)))

Tactic:
congr 2
-- Module: Mathlib.Probability.Independence.Conditional
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.deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : γ × β' × β) → (γ × β') × β) ⋯ ∘ₖ
      (Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)))
⊢ Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ =
    Kernel.deterministic (⇑e : (a : γ × β' × β) → (γ × β') × β) ⋯ ∘ₖ
      (Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ))

Tactic:
unfold e
-- Module: Mathlib.Probability.Independence.Conditional
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 : γ × β' × β) → (γ × β') × β))
e_f₁ e_f₂ :
  Eq (α := Kernel γ ((γ × β') × β)) (Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ)
    (Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ)
⊢ 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 μ)))

Tactic:
rw [Kernel.deterministic_comp_eq_map, Kernel.prodAssoc_symm_prod]

Premises used: ProbabilityTheory.Kernel.deterministic_comp_eq_map, ProbabilityTheory.Kernel.prodAssoc_symm_prod
-- Module: Mathlib.Probability.Independence.Conditional
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 (γ × β' × β))))

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]