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

State before:
R✝ : Type ?u.285283
inst✝²⁷ : Ring R✝
X : Type ?u.285289
inst✝²⁶ : AddCommGroup X
inst✝²⁵ : Module R✝ X
Y : Type ?u.286082
inst✝²⁴ : AddCommGroup Y
inst✝²³ : Module R✝ Y
Z : Type ?u.286816
inst✝²² : AddCommGroup Z
inst✝²¹ : Module R✝ Z
ι✝ : Type ?u.287550
tag✝ : Lean.Name
MR✝ : Type ?u.287555
inst✝²⁰ : AddCommGroup MR✝
inst✝¹⁹ : Module R✝ MR✝
inst✝¹⁸ : BroadcastType tag✝ R✝ ι✝ R✝ MR✝
MX : Type ?u.289101
inst✝¹⁷ : AddCommGroup MX
inst✝¹⁶ : Module R✝ MX
inst✝¹⁵ : BroadcastType tag✝ R✝ ι✝ X MX
MY : Type ?u.289899
inst✝¹⁴ : AddCommGroup MY
inst✝¹³ : Module R✝ MY
inst✝¹² : BroadcastType tag✝ R✝ ι✝ Y MY
MZ : Type ?u.290697
inst✝¹¹ : AddCommGroup MZ
inst✝¹⁰ : Module R✝ MZ
inst✝⁹ : BroadcastType tag✝ R✝ ι✝ Z MZ
κ : Type ?u.291495
E : κ → Type ?u.291500
ME : κ → Type ?u.291505
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)
R : Type u_1
inst✝³ : CommRing R
ι : Type u_2
tag : Lean.Name
MR : Type u_3
inst✝² : AddCommGroup MR
inst✝¹ : Module R MR
inst✝ : BroadcastType tag R ι R MR
f : R → R
c : R
⊢ (broadcast tag R ι fun x => f x * c) = fun mx => c • broadcast tag R ι f mx
Tactic:
funext mx
State after:
case h
R✝ : Type ?u.285283
inst✝²⁷ : Ring R✝
X : Type ?u.285289
inst✝²⁶ : AddCommGroup X
inst✝²⁵ : Module R✝ X
Y : Type ?u.286082
inst✝²⁴ : AddCommGroup Y
inst✝²³ : Module R✝ Y
Z : Type ?u.286816
inst✝²² : AddCommGroup Z
inst✝²¹ : Module R✝ Z
ι✝ : Type ?u.287550
tag✝ : Lean.Name
MR✝ : Type ?u.287555
inst✝²⁰ : AddCommGroup MR✝
inst✝¹⁹ : Module R✝ MR✝
inst✝¹⁸ : BroadcastType tag✝ R✝ ι✝ R✝ MR✝
MX : Type ?u.289101
inst✝¹⁷ : AddCommGroup MX
inst✝¹⁶ : Module R✝ MX
inst✝¹⁵ : BroadcastType tag✝ R✝ ι✝ X MX
MY : Type ?u.289899
inst✝¹⁴ : AddCommGroup MY
inst✝¹³ : Module R✝ MY
inst✝¹² : BroadcastType tag✝ R✝ ι✝ Y MY
MZ : Type ?u.290697
inst✝¹¹ : AddCommGroup MZ
inst✝¹⁰ : Module R✝ MZ
inst✝⁹ : BroadcastType tag✝ R✝ ι✝ Z MZ
κ : Type ?u.291495
E : κ → Type ?u.291500
ME : κ → Type ?u.291505
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)
R : Type u_1
inst✝³ : CommRing R
ι : Type u_2
tag : Lean.Name
MR : Type u_3
inst✝² : AddCommGroup MR
inst✝¹ : Module R MR
inst✝ : BroadcastType tag R ι R MR
f : R → R
c : R
mx : MR
⊢ broadcast tag R ι (fun x => f x * c) mx = c • broadcast tag R ι f mx

State before:
case h
R✝ : Type ?u.285283
inst✝²⁷ : Ring R✝
X : Type ?u.285289
inst✝²⁶ : AddCommGroup X
inst✝²⁵ : Module R✝ X
Y : Type ?u.286082
inst✝²⁴ : AddCommGroup Y
inst✝²³ : Module R✝ Y
Z : Type ?u.286816
inst✝²² : AddCommGroup Z
inst✝²¹ : Module R✝ Z
ι✝ : Type ?u.287550
tag✝ : Lean.Name
MR✝ : Type ?u.287555
inst✝²⁰ : AddCommGroup MR✝
inst✝¹⁹ : Module R✝ MR✝
inst✝¹⁸ : BroadcastType tag✝ R✝ ι✝ R✝ MR✝
MX : Type ?u.289101
inst✝¹⁷ : AddCommGroup MX
inst✝¹⁶ : Module R✝ MX
inst✝¹⁵ : BroadcastType tag✝ R✝ ι✝ X MX
MY : Type ?u.289899
inst✝¹⁴ : AddCommGroup MY
inst✝¹³ : Module R✝ MY
inst✝¹² : BroadcastType tag✝ R✝ ι✝ Y MY
MZ : Type ?u.290697
inst✝¹¹ : AddCommGroup MZ
inst✝¹⁰ : Module R✝ MZ
inst✝⁹ : BroadcastType tag✝ R✝ ι✝ Z MZ
κ : Type ?u.291495
E : κ → Type ?u.291500
ME : κ → Type ?u.291505
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)
R : Type u_1
inst✝³ : CommRing R
ι : Type u_2
tag : Lean.Name
MR : Type u_3
inst✝² : AddCommGroup MR
inst✝¹ : Module R MR
inst✝ : BroadcastType tag R ι R MR
f : R → R
c : R
mx : MR
⊢ broadcast tag R ι (fun x => f x * c) mx = c • broadcast tag R ι f mx
Tactic:
unfold broadcast
State after:
case h
R✝ : Type ?u.285283
inst✝²⁷ : Ring R✝
X : Type ?u.285289
inst✝²⁶ : AddCommGroup X
inst✝²⁵ : Module R✝ X
Y : Type ?u.286082
inst✝²⁴ : AddCommGroup Y
inst✝²³ : Module R✝ Y
Z : Type ?u.286816
inst✝²² : AddCommGroup Z
inst✝²¹ : Module R✝ Z
ι✝ : Type ?u.287550
tag✝ : Lean.Name
MR✝ : Type ?u.287555
inst✝²⁰ : AddCommGroup MR✝
inst✝¹⁹ : Module R✝ MR✝
inst✝¹⁸ : BroadcastType tag✝ R✝ ι✝ R✝ MR✝
MX : Type ?u.289101
inst✝¹⁷ : AddCommGroup MX
inst✝¹⁶ : Module R✝ MX
inst✝¹⁵ : BroadcastType tag✝ R✝ ι✝ X MX
MY : Type ?u.289899
inst✝¹⁴ : AddCommGroup MY
inst✝¹³ : Module R✝ MY
inst✝¹² : BroadcastType tag✝ R✝ ι✝ Y MY
MZ : Type ?u.290697
inst✝¹¹ : AddCommGroup MZ
inst✝¹⁰ : Module R✝ MZ
inst✝⁹ : BroadcastType tag✝ R✝ ι✝ Z MZ
κ : Type ?u.291495
E : κ → Type ?u.291500
ME : κ → Type ?u.291505
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)
R : Type u_1
inst✝³ : CommRing R
ι : Type u_2
tag : Lean.Name
MR : Type u_3
inst✝² : AddCommGroup MR
inst✝¹ : Module R MR
inst✝ : BroadcastType tag R ι R MR
f : R → R
c : R
mx : MR
⊢ ((LinearEquiv.symm (BroadcastType.equiv tag)) fun i => (fun x => f x * c) ((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.285283
inst✝²⁷ : Ring R✝
X : Type ?u.285289
inst✝²⁶ : AddCommGroup X
inst✝²⁵ : Module R✝ X
Y : Type ?u.286082
inst✝²⁴ : AddCommGroup Y
inst✝²³ : Module R✝ Y
Z : Type ?u.286816
inst✝²² : AddCommGroup Z
inst✝²¹ : Module R✝ Z
ι✝ : Type ?u.287550
tag✝ : Lean.Name
MR✝ : Type ?u.287555
inst✝²⁰ : AddCommGroup MR✝
inst✝¹⁹ : Module R✝ MR✝
inst✝¹⁸ : BroadcastType tag✝ R✝ ι✝ R✝ MR✝
MX : Type ?u.289101
inst✝¹⁷ : AddCommGroup MX
inst✝¹⁶ : Module R✝ MX
inst✝¹⁵ : BroadcastType tag✝ R✝ ι✝ X MX
MY : Type ?u.289899
inst✝¹⁴ : AddCommGroup MY
inst✝¹³ : Module R✝ MY
inst✝¹² : BroadcastType tag✝ R✝ ι✝ Y MY
MZ : Type ?u.290697
inst✝¹¹ : AddCommGroup MZ
inst✝¹⁰ : Module R✝ MZ
inst✝⁹ : BroadcastType tag✝ R✝ ι✝ Z MZ
κ : Type ?u.291495
E : κ → Type ?u.291500
ME : κ → Type ?u.291505
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)
R : Type u_1
inst✝³ : CommRing R
ι : Type u_2
tag : Lean.Name
MR : Type u_3
inst✝² : AddCommGroup MR
inst✝¹ : Module R MR
inst✝ : BroadcastType tag R ι R MR
f : R → R
c : R
mx : MR
⊢ ((LinearEquiv.symm (BroadcastType.equiv tag)) fun i => (fun x => f x * c) ((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.285283
inst✝²⁷ : Ring R✝
X : Type ?u.285289
inst✝²⁶ : AddCommGroup X
inst✝²⁵ : Module R✝ X
Y : Type ?u.286082
inst✝²⁴ : AddCommGroup Y
inst✝²³ : Module R✝ Y
Z : Type ?u.286816
inst✝²² : AddCommGroup Z
inst✝²¹ : Module R✝ Z
ι✝ : Type ?u.287550
tag✝ : Lean.Name
MR✝ : Type ?u.287555
inst✝²⁰ : AddCommGroup MR✝
inst✝¹⁹ : Module R✝ MR✝
inst✝¹⁸ : BroadcastType tag✝ R✝ ι✝ R✝ MR✝
MX : Type ?u.289101
inst✝¹⁷ : AddCommGroup MX
inst✝¹⁶ : Module R✝ MX
inst✝¹⁵ : BroadcastType tag✝ R✝ ι✝ X MX
MY : Type ?u.289899
inst✝¹⁴ : AddCommGroup MY
inst✝¹³ : Module R✝ MY
inst✝¹² : BroadcastType tag✝ R✝ ι✝ Y MY
MZ : Type ?u.290697
inst✝¹¹ : AddCommGroup MZ
inst✝¹⁰ : Module R✝ MZ
inst✝⁹ : BroadcastType tag✝ R✝ ι✝ Z MZ
κ : Type ?u.291495
E : κ → Type ?u.291500
ME : κ → Type ?u.291505
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)
R : Type u_1
inst✝³ : CommRing R
ι : Type u_2
tag : Lean.Name
MR : Type u_3
inst✝² : AddCommGroup MR
inst✝¹ : Module R MR
inst✝ : BroadcastType tag R ι R MR
f : R → R
c : R
mx : MR
⊢ ((LinearEquiv.symm (BroadcastType.equiv tag)) fun i => (fun x => f x * c) ((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.285283
inst✝²⁷ : Ring R✝
X : Type ?u.285289
inst✝²⁶ : AddCommGroup X
inst✝²⁵ : Module R✝ X
Y : Type ?u.286082
inst✝²⁴ : AddCommGroup Y
inst✝²³ : Module R✝ Y
Z : Type ?u.286816
inst✝²² : AddCommGroup Z
inst✝²¹ : Module R✝ Z
ι✝ : Type ?u.287550
tag✝ : Lean.Name
MR✝ : Type ?u.287555
inst✝²⁰ : AddCommGroup MR✝
inst✝¹⁹ : Module R✝ MR✝
inst✝¹⁸ : BroadcastType tag✝ R✝ ι✝ R✝ MR✝
MX : Type ?u.289101
inst✝¹⁷ : AddCommGroup MX
inst✝¹⁶ : Module R✝ MX
inst✝¹⁵ : BroadcastType tag✝ R✝ ι✝ X MX
MY : Type ?u.289899
inst✝¹⁴ : AddCommGroup MY
inst✝¹³ : Module R✝ MY
inst✝¹² : BroadcastType tag✝ R✝ ι✝ Y MY
MZ : Type ?u.290697
inst✝¹¹ : AddCommGroup MZ
inst✝¹⁰ : Module R✝ MZ
inst✝⁹ : BroadcastType tag✝ R✝ ι✝ Z MZ
κ : Type ?u.291495
E : κ → Type ?u.291500
ME : κ → Type ?u.291505
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)
R : Type u_1
inst✝³ : CommRing R
ι : Type u_2
tag : Lean.Name
MR : Type u_3
inst✝² : AddCommGroup MR
inst✝¹ : Module R MR
inst✝ : BroadcastType tag R ι R MR
f : R → R
c : R
mx : MR
⊢ ((LinearEquiv.symm (BroadcastType.equiv tag)) fun i => (fun x => f x * c) ((BroadcastType.equiv tag) mx i)) =
    (LinearEquiv.symm (BroadcastType.equiv tag)) (c • fun i => f ((BroadcastType.equiv tag) mx i))
Tactic:
congr
State after:
case h.h.e_6.h
R✝ : Type ?u.285283
inst✝²⁷ : Ring R✝
X : Type ?u.285289
inst✝²⁶ : AddCommGroup X
inst✝²⁵ : Module R✝ X
Y : Type ?u.286082
inst✝²⁴ : AddCommGroup Y
inst✝²³ : Module R✝ Y
Z : Type ?u.286816
inst✝²² : AddCommGroup Z
inst✝²¹ : Module R✝ Z
ι✝ : Type ?u.287550
tag✝ : Lean.Name
MR✝ : Type ?u.287555
inst✝²⁰ : AddCommGroup MR✝
inst✝¹⁹ : Module R✝ MR✝
inst✝¹⁸ : BroadcastType tag✝ R✝ ι✝ R✝ MR✝
MX : Type ?u.289101
inst✝¹⁷ : AddCommGroup MX
inst✝¹⁶ : Module R✝ MX
inst✝¹⁵ : BroadcastType tag✝ R✝ ι✝ X MX
MY : Type ?u.289899
inst✝¹⁴ : AddCommGroup MY
inst✝¹³ : Module R✝ MY
inst✝¹² : BroadcastType tag✝ R✝ ι✝ Y MY
MZ : Type ?u.290697
inst✝¹¹ : AddCommGroup MZ
inst✝¹⁰ : Module R✝ MZ
inst✝⁹ : BroadcastType tag✝ R✝ ι✝ Z MZ
κ : Type ?u.291495
E : κ → Type ?u.291500
ME : κ → Type ?u.291505
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)
R : Type u_1
inst✝³ : CommRing R
ι : Type u_2
tag : Lean.Name
MR : Type u_3
inst✝² : AddCommGroup MR
inst✝¹ : Module R MR
inst✝ : BroadcastType tag R ι R MR
f : R → R
c : R
mx : MR
⊢ (fun i => (fun x => f x * c) ((BroadcastType.equiv tag) mx i)) = c • fun i => f ((BroadcastType.equiv tag) mx i)

State before:
case h.h.e_6.h
R✝ : Type ?u.285283
inst✝²⁷ : Ring R✝
X : Type ?u.285289
inst✝²⁶ : AddCommGroup X
inst✝²⁵ : Module R✝ X
Y : Type ?u.286082
inst✝²⁴ : AddCommGroup Y
inst✝²³ : Module R✝ Y
Z : Type ?u.286816
inst✝²² : AddCommGroup Z
inst✝²¹ : Module R✝ Z
ι✝ : Type ?u.287550
tag✝ : Lean.Name
MR✝ : Type ?u.287555
inst✝²⁰ : AddCommGroup MR✝
inst✝¹⁹ : Module R✝ MR✝
inst✝¹⁸ : BroadcastType tag✝ R✝ ι✝ R✝ MR✝
MX : Type ?u.289101
inst✝¹⁷ : AddCommGroup MX
inst✝¹⁶ : Module R✝ MX
inst✝¹⁵ : BroadcastType tag✝ R✝ ι✝ X MX
MY : Type ?u.289899
inst✝¹⁴ : AddCommGroup MY
inst✝¹³ : Module R✝ MY
inst✝¹² : BroadcastType tag✝ R✝ ι✝ Y MY
MZ : Type ?u.290697
inst✝¹¹ : AddCommGroup MZ
inst✝¹⁰ : Module R✝ MZ
inst✝⁹ : BroadcastType tag✝ R✝ ι✝ Z MZ
κ : Type ?u.291495
E : κ → Type ?u.291500
ME : κ → Type ?u.291505
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)
R : Type u_1
inst✝³ : CommRing R
ι : Type u_2
tag : Lean.Name
MR : Type u_3
inst✝² : AddCommGroup MR
inst✝¹ : Module R MR
inst✝ : BroadcastType tag R ι R MR
f : R → R
c : R
mx : MR
⊢ (fun i => (fun x => f x * c) ((BroadcastType.equiv tag) mx i)) = c • fun i => f ((BroadcastType.equiv tag) mx i)
Tactic:
funext i
State after:
case h.h.e_6.h.h
R✝ : Type ?u.285283
inst✝²⁷ : Ring R✝
X : Type ?u.285289
inst✝²⁶ : AddCommGroup X
inst✝²⁵ : Module R✝ X
Y : Type ?u.286082
inst✝²⁴ : AddCommGroup Y
inst✝²³ : Module R✝ Y
Z : Type ?u.286816
inst✝²² : AddCommGroup Z
inst✝²¹ : Module R✝ Z
ι✝ : Type ?u.287550
tag✝ : Lean.Name
MR✝ : Type ?u.287555
inst✝²⁰ : AddCommGroup MR✝
inst✝¹⁹ : Module R✝ MR✝
inst✝¹⁸ : BroadcastType tag✝ R✝ ι✝ R✝ MR✝
MX : Type ?u.289101
inst✝¹⁷ : AddCommGroup MX
inst✝¹⁶ : Module R✝ MX
inst✝¹⁵ : BroadcastType tag✝ R✝ ι✝ X MX
MY : Type ?u.289899
inst✝¹⁴ : AddCommGroup MY
inst✝¹³ : Module R✝ MY
inst✝¹² : BroadcastType tag✝ R✝ ι✝ Y MY
MZ : Type ?u.290697
inst✝¹¹ : AddCommGroup MZ
inst✝¹⁰ : Module R✝ MZ
inst✝⁹ : BroadcastType tag✝ R✝ ι✝ Z MZ
κ : Type ?u.291495
E : κ → Type ?u.291500
ME : κ → Type ?u.291505
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)
R : Type u_1
inst✝³ : CommRing R
ι : Type u_2
tag : Lean.Name
MR : Type u_3
inst✝² : AddCommGroup MR
inst✝¹ : Module R MR
inst✝ : BroadcastType tag R ι R MR
f : R → R
c : R
mx : MR
i : ι
⊢ (fun x => f x * c) ((BroadcastType.equiv tag) mx i) = (c • fun i => f ((BroadcastType.equiv tag) mx i)) i

State before:
case h.h.e_6.h.h
R✝ : Type ?u.285283
inst✝²⁷ : Ring R✝
X : Type ?u.285289
inst✝²⁶ : AddCommGroup X
inst✝²⁵ : Module R✝ X
Y : Type ?u.286082
inst✝²⁴ : AddCommGroup Y
inst✝²³ : Module R✝ Y
Z : Type ?u.286816
inst✝²² : AddCommGroup Z
inst✝²¹ : Module R✝ Z
ι✝ : Type ?u.287550
tag✝ : Lean.Name
MR✝ : Type ?u.287555
inst✝²⁰ : AddCommGroup MR✝
inst✝¹⁹ : Module R✝ MR✝
inst✝¹⁸ : BroadcastType tag✝ R✝ ι✝ R✝ MR✝
MX : Type ?u.289101
inst✝¹⁷ : AddCommGroup MX
inst✝¹⁶ : Module R✝ MX
inst✝¹⁵ : BroadcastType tag✝ R✝ ι✝ X MX
MY : Type ?u.289899
inst✝¹⁴ : AddCommGroup MY
inst✝¹³ : Module R✝ MY
inst✝¹² : BroadcastType tag✝ R✝ ι✝ Y MY
MZ : Type ?u.290697
inst✝¹¹ : AddCommGroup MZ
inst✝¹⁰ : Module R✝ MZ
inst✝⁹ : BroadcastType tag✝ R✝ ι✝ Z MZ
κ : Type ?u.291495
E : κ → Type ?u.291500
ME : κ → Type ?u.291505
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)
R : Type u_1
inst✝³ : CommRing R
ι : Type u_2
tag : Lean.Name
MR : Type u_3
inst✝² : AddCommGroup MR
inst✝¹ : Module R MR
inst✝ : BroadcastType tag R ι R MR
f : R → R
c : R
mx : MR
i : ι
⊢ (fun x => f x * c) ((BroadcastType.equiv tag) mx i) = (c • fun i => f ((BroadcastType.equiv tag) mx i)) i
Tactic:
simp[mul_comm]
State after:
no goals