-- 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 (γ × β' × β))))
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 (γ × β' × β)))))
rw₁ :
  Eq (α := Measure (γ × β' × β))
    (Measure.bind (mα := mγ) (Measure.map k μ)
      (⇑(Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)) : (a : γ) → Measure (γ × β' × β)))
    (Measure.map (α := γ × β' × β)
      (Function.comp (β := (γ × β') × β) (⇑e.symm : (a : (γ × β') × β) → γ × β' × β)
        (⇑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 id
    (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]