Theorem: SciLean.apply_rule (SciLean/Core/FunctionTransformations/Broadcast.lean)

State before:
tag : Lean.Name
R : Type u_3
inst✝²⁰ : Ring R
ι : Type u_4
X : Type ?u.90750
inst✝¹⁹ : AddCommGroup X
inst✝¹⁸ : Module R X
Y : Type ?u.91543
inst✝¹⁷ : AddCommGroup Y
inst✝¹⁶ : Module R Y
Z : Type ?u.92277
inst✝¹⁵ : AddCommGroup Z
inst✝¹⁴ : Module R Z
MX : Type ?u.93011
inst✝¹³ : AddCommGroup MX
inst✝¹² : Module R MX
inst✝¹¹ : BroadcastType tag R ι X MX
MY : Type ?u.93809
inst✝¹⁰ : AddCommGroup MY
inst✝⁹ : Module R MY
inst✝⁸ : BroadcastType tag R ι Y MY
MZ : Type ?u.94607
inst✝⁷ : AddCommGroup MZ
inst✝⁶ : Module R MZ
inst✝⁵ : BroadcastType tag R ι Z MZ
κ : Type u_1
E : κ → Type u_5
ME : κ → Type u_2
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)
j : κ
⊢ (broadcast tag R ι fun x => x j) = fun mx => mx j
Tactic:
unfold broadcast
State after:
tag : Lean.Name
R : Type u_3
inst✝²⁰ : Ring R
ι : Type u_4
X : Type ?u.90750
inst✝¹⁹ : AddCommGroup X
inst✝¹⁸ : Module R X
Y : Type ?u.91543
inst✝¹⁷ : AddCommGroup Y
inst✝¹⁶ : Module R Y
Z : Type ?u.92277
inst✝¹⁵ : AddCommGroup Z
inst✝¹⁴ : Module R Z
MX : Type ?u.93011
inst✝¹³ : AddCommGroup MX
inst✝¹² : Module R MX
inst✝¹¹ : BroadcastType tag R ι X MX
MY : Type ?u.93809
inst✝¹⁰ : AddCommGroup MY
inst✝⁹ : Module R MY
inst✝⁸ : BroadcastType tag R ι Y MY
MZ : Type ?u.94607
inst✝⁷ : AddCommGroup MZ
inst✝⁶ : Module R MZ
inst✝⁵ : BroadcastType tag R ι Z MZ
κ : Type u_1
E : κ → Type u_5
ME : κ → Type u_2
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)
j : κ
⊢ (fun mx => (LinearEquiv.symm (BroadcastType.equiv tag)) fun i => (fun x => x j) ((BroadcastType.equiv tag) mx i)) =
    fun mx => mx j

State before:
tag : Lean.Name
R : Type u_3
inst✝²⁰ : Ring R
ι : Type u_4
X : Type ?u.90750
inst✝¹⁹ : AddCommGroup X
inst✝¹⁸ : Module R X
Y : Type ?u.91543
inst✝¹⁷ : AddCommGroup Y
inst✝¹⁶ : Module R Y
Z : Type ?u.92277
inst✝¹⁵ : AddCommGroup Z
inst✝¹⁴ : Module R Z
MX : Type ?u.93011
inst✝¹³ : AddCommGroup MX
inst✝¹² : Module R MX
inst✝¹¹ : BroadcastType tag R ι X MX
MY : Type ?u.93809
inst✝¹⁰ : AddCommGroup MY
inst✝⁹ : Module R MY
inst✝⁸ : BroadcastType tag R ι Y MY
MZ : Type ?u.94607
inst✝⁷ : AddCommGroup MZ
inst✝⁶ : Module R MZ
inst✝⁵ : BroadcastType tag R ι Z MZ
κ : Type u_1
E : κ → Type u_5
ME : κ → Type u_2
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)
j : κ
⊢ (fun mx => (LinearEquiv.symm (BroadcastType.equiv tag)) fun i => (fun x => x j) ((BroadcastType.equiv tag) mx i)) =
    fun mx => mx j
Tactic:
simp[broadcastIntro, BroadcastType.equiv]
State after:
no goals