simp[broadcast, BroadcastType.equiv]
case h
tag : Lean.Name
R : Type u_3
inst✝²⁰ : Ring R
ι : Type u_4
X : Type u_5
inst✝¹⁹ : AddCommGroup X
inst✝¹⁸ : Module R X
Y : Type u_7
inst✝¹⁷ : AddCommGroup Y
inst✝¹⁶ : Module R Y
Z : Type u_6
inst✝¹⁵ : AddCommGroup Z
inst✝¹⁴ : Module R Z
MX : Type u_1
inst✝¹³ : AddCommGroup MX
inst✝¹² : Module R MX
inst✝¹¹ : BroadcastType tag R ι X MX
MY : Type u_8
inst✝¹⁰ : AddCommGroup MY
inst✝⁹ : Module R MY
inst✝⁸ : BroadcastType tag R ι Y MY
MZ : Type u_2
inst✝⁷ : AddCommGroup MZ
inst✝⁶ : Module R MZ
inst✝⁵ : BroadcastType tag R ι Z MZ
κ : Type ?u.63075
E : κ → Type ?u.63080
ME : κ → Type ?u.63085
inst✝⁴ : (j : κ) → AddCommGroup (E j)
inst✝³ : (j : κ) → Module R (E j)
inst✝² : (j : κ) → AddCommGroup (ME j)
inst✝¹ : (j : κ) → Module R (ME j)
inst✝ : (j : κ) → BroadcastType tag R ι (E j) (ME j)
g : X → Y
f : X → Y → Z
mx : MX
⊢ broadcast tag R ι (fun x => (fun xy => f xy.1 xy.2) ((fun x' => (x', g x')) x)) mx =
    let my := (fun mx => broadcast tag R ι g (broadcast tag R ι (fun x => x) mx)) mx;
    let mz := broadcast tag R ι (fun xy => f xy.1 xy.2) (mx, my);
    mz
no goals