Theorem: HMul.hMul.arg_a1.broadcast_rule (SciLean/Core/FunctionTransformations/Broadcast.lean)

State before:
R : Type u_2
inst✝²³ : Ring R
X : Type ?u.266497
inst✝²² : AddCommGroup X
inst✝²¹ : Module R X
Y : Type ?u.267290
inst✝²⁰ : AddCommGroup Y
inst✝¹⁹ : Module R Y
Z : Type ?u.268024
inst✝¹⁸ : AddCommGroup Z
inst✝¹⁷ : Module R Z
ι : Type u_3
tag : Lean.Name
MR : Type u_1
inst✝¹⁶ : AddCommGroup MR
inst✝¹⁵ : Module R MR
inst✝¹⁴ : BroadcastType tag R ι R MR
MX : Type ?u.270309
inst✝¹³ : AddCommGroup MX
inst✝¹² : Module R MX
inst✝¹¹ : BroadcastType tag R ι X MX
MY : Type ?u.271107
inst✝¹⁰ : AddCommGroup MY
inst✝⁹ : Module R MY
inst✝⁸ : BroadcastType tag R ι Y MY
MZ : Type ?u.271905
inst✝⁷ : AddCommGroup MZ
inst✝⁶ : Module R MZ
inst✝⁵ : BroadcastType tag R ι Z MZ
κ : Type ?u.272703
E : κ → Type ?u.272708
ME : κ → Type ?u.272713
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)
f : R → R
c : R
⊢ (broadcast tag R ι fun x => c * f x) = fun mx => c • broadcast tag R ι f mx
Tactic:
funext mx
State after:
case h
R : Type u_2
inst✝²³ : Ring R
X : Type ?u.266497
inst✝²² : AddCommGroup X
inst✝²¹ : Module R X
Y : Type ?u.267290
inst✝²⁰ : AddCommGroup Y
inst✝¹⁹ : Module R Y
Z : Type ?u.268024
inst✝¹⁸ : AddCommGroup Z
inst✝¹⁷ : Module R Z
ι : Type u_3
tag : Lean.Name
MR : Type u_1
inst✝¹⁶ : AddCommGroup MR
inst✝¹⁵ : Module R MR
inst✝¹⁴ : BroadcastType tag R ι R MR
MX : Type ?u.270309
inst✝¹³ : AddCommGroup MX
inst✝¹² : Module R MX
inst✝¹¹ : BroadcastType tag R ι X MX
MY : Type ?u.271107
inst✝¹⁰ : AddCommGroup MY
inst✝⁹ : Module R MY
inst✝⁸ : BroadcastType tag R ι Y MY
MZ : Type ?u.271905
inst✝⁷ : AddCommGroup MZ
inst✝⁶ : Module R MZ
inst✝⁵ : BroadcastType tag R ι Z MZ
κ : Type ?u.272703
E : κ → Type ?u.272708
ME : κ → Type ?u.272713
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)
f : R → R
c : R
mx : MR
⊢ broadcast tag R ι (fun x => c * f x) mx = c • broadcast tag R ι f mx

State before:
case h
R : Type u_2
inst✝²³ : Ring R
X : Type ?u.266497
inst✝²² : AddCommGroup X
inst✝²¹ : Module R X
Y : Type ?u.267290
inst✝²⁰ : AddCommGroup Y
inst✝¹⁹ : Module R Y
Z : Type ?u.268024
inst✝¹⁸ : AddCommGroup Z
inst✝¹⁷ : Module R Z
ι : Type u_3
tag : Lean.Name
MR : Type u_1
inst✝¹⁶ : AddCommGroup MR
inst✝¹⁵ : Module R MR
inst✝¹⁴ : BroadcastType tag R ι R MR
MX : Type ?u.270309
inst✝¹³ : AddCommGroup MX
inst✝¹² : Module R MX
inst✝¹¹ : BroadcastType tag R ι X MX
MY : Type ?u.271107
inst✝¹⁰ : AddCommGroup MY
inst✝⁹ : Module R MY
inst✝⁸ : BroadcastType tag R ι Y MY
MZ : Type ?u.271905
inst✝⁷ : AddCommGroup MZ
inst✝⁶ : Module R MZ
inst✝⁵ : BroadcastType tag R ι Z MZ
κ : Type ?u.272703
E : κ → Type ?u.272708
ME : κ → Type ?u.272713
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)
f : R → R
c : R
mx : MR
⊢ broadcast tag R ι (fun x => c * f x) mx = c • broadcast tag R ι f mx
Tactic:
unfold broadcast
State after:
case h
R : Type u_2
inst✝²³ : Ring R
X : Type ?u.266497
inst✝²² : AddCommGroup X
inst✝²¹ : Module R X
Y : Type ?u.267290
inst✝²⁰ : AddCommGroup Y
inst✝¹⁹ : Module R Y
Z : Type ?u.268024
inst✝¹⁸ : AddCommGroup Z
inst✝¹⁷ : Module R Z
ι : Type u_3
tag : Lean.Name
MR : Type u_1
inst✝¹⁶ : AddCommGroup MR
inst✝¹⁵ : Module R MR
inst✝¹⁴ : BroadcastType tag R ι R MR
MX : Type ?u.270309
inst✝¹³ : AddCommGroup MX
inst✝¹² : Module R MX
inst✝¹¹ : BroadcastType tag R ι X MX
MY : Type ?u.271107
inst✝¹⁰ : AddCommGroup MY
inst✝⁹ : Module R MY
inst✝⁸ : BroadcastType tag R ι Y MY
MZ : Type ?u.271905
inst✝⁷ : AddCommGroup MZ
inst✝⁶ : Module R MZ
inst✝⁵ : BroadcastType tag R ι Z MZ
κ : Type ?u.272703
E : κ → Type ?u.272708
ME : κ → Type ?u.272713
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)
f : R → R
c : R
mx : MR
⊢ ((LinearEquiv.symm (BroadcastType.equiv tag)) fun i => (fun x => c * f x) ((BroadcastType.equiv tag) mx i)) =
    c • (LinearEquiv.symm (BroadcastType.equiv tag)) fun i => f ((BroadcastType.equiv tag) mx i)

State before:
case h
R : Type u_2
inst✝²³ : Ring R
X : Type ?u.266497
inst✝²² : AddCommGroup X
inst✝²¹ : Module R X
Y : Type ?u.267290
inst✝²⁰ : AddCommGroup Y
inst✝¹⁹ : Module R Y
Z : Type ?u.268024
inst✝¹⁸ : AddCommGroup Z
inst✝¹⁷ : Module R Z
ι : Type u_3
tag : Lean.Name
MR : Type u_1
inst✝¹⁶ : AddCommGroup MR
inst✝¹⁵ : Module R MR
inst✝¹⁴ : BroadcastType tag R ι R MR
MX : Type ?u.270309
inst✝¹³ : AddCommGroup MX
inst✝¹² : Module R MX
inst✝¹¹ : BroadcastType tag R ι X MX
MY : Type ?u.271107
inst✝¹⁰ : AddCommGroup MY
inst✝⁹ : Module R MY
inst✝⁸ : BroadcastType tag R ι Y MY
MZ : Type ?u.271905
inst✝⁷ : AddCommGroup MZ
inst✝⁶ : Module R MZ
inst✝⁵ : BroadcastType tag R ι Z MZ
κ : Type ?u.272703
E : κ → Type ?u.272708
ME : κ → Type ?u.272713
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)
f : R → R
c : R
mx : MR
⊢ ((LinearEquiv.symm (BroadcastType.equiv tag)) fun i => (fun x => c * f x) ((BroadcastType.equiv tag) mx i)) =
    c • (LinearEquiv.symm (BroadcastType.equiv tag)) fun i => f ((BroadcastType.equiv tag) mx i)
Tactic:
rw[← map_smul]
State after:
case h
R : Type u_2
inst✝²³ : Ring R
X : Type ?u.266497
inst✝²² : AddCommGroup X
inst✝²¹ : Module R X
Y : Type ?u.267290
inst✝²⁰ : AddCommGroup Y
inst✝¹⁹ : Module R Y
Z : Type ?u.268024
inst✝¹⁸ : AddCommGroup Z
inst✝¹⁷ : Module R Z
ι : Type u_3
tag : Lean.Name
MR : Type u_1
inst✝¹⁶ : AddCommGroup MR
inst✝¹⁵ : Module R MR
inst✝¹⁴ : BroadcastType tag R ι R MR
MX : Type ?u.270309
inst✝¹³ : AddCommGroup MX
inst✝¹² : Module R MX
inst✝¹¹ : BroadcastType tag R ι X MX
MY : Type ?u.271107
inst✝¹⁰ : AddCommGroup MY
inst✝⁹ : Module R MY
inst✝⁸ : BroadcastType tag R ι Y MY
MZ : Type ?u.271905
inst✝⁷ : AddCommGroup MZ
inst✝⁶ : Module R MZ
inst✝⁵ : BroadcastType tag R ι Z MZ
κ : Type ?u.272703
E : κ → Type ?u.272708
ME : κ → Type ?u.272713
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)
f : R → R
c : R
mx : MR
⊢ ((LinearEquiv.symm (BroadcastType.equiv tag)) fun i => (fun x => c * f x) ((BroadcastType.equiv tag) mx i)) =
    (LinearEquiv.symm (BroadcastType.equiv tag)) (c • fun i => f ((BroadcastType.equiv tag) mx i))

State before:
case h
R : Type u_2
inst✝²³ : Ring R
X : Type ?u.266497
inst✝²² : AddCommGroup X
inst✝²¹ : Module R X
Y : Type ?u.267290
inst✝²⁰ : AddCommGroup Y
inst✝¹⁹ : Module R Y
Z : Type ?u.268024
inst✝¹⁸ : AddCommGroup Z
inst✝¹⁷ : Module R Z
ι : Type u_3
tag : Lean.Name
MR : Type u_1
inst✝¹⁶ : AddCommGroup MR
inst✝¹⁵ : Module R MR
inst✝¹⁴ : BroadcastType tag R ι R MR
MX : Type ?u.270309
inst✝¹³ : AddCommGroup MX
inst✝¹² : Module R MX
inst✝¹¹ : BroadcastType tag R ι X MX
MY : Type ?u.271107
inst✝¹⁰ : AddCommGroup MY
inst✝⁹ : Module R MY
inst✝⁸ : BroadcastType tag R ι Y MY
MZ : Type ?u.271905
inst✝⁷ : AddCommGroup MZ
inst✝⁶ : Module R MZ
inst✝⁵ : BroadcastType tag R ι Z MZ
κ : Type ?u.272703
E : κ → Type ?u.272708
ME : κ → Type ?u.272713
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)
f : R → R
c : R
mx : MR
⊢ ((LinearEquiv.symm (BroadcastType.equiv tag)) fun i => (fun x => c * f x) ((BroadcastType.equiv tag) mx i)) =
    (LinearEquiv.symm (BroadcastType.equiv tag)) (c • fun i => f ((BroadcastType.equiv tag) mx i))
Tactic:
rfl
State after:
no goals