internlm/Lean-Github huggingface dataset:
Theorem: HMul.hMul.arg_a0.broadcast_rule
Proof 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
Proof 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)
Theorem: HMul.hMul.arg_a0.broadcast_rule
Proof 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
Proof 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
Theorem: HMul.hMul.arg_a0.broadcast_rule
Proof 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]
Proof state after:
no goals
Theorem: HSMul.hSMul.arg_a1.broadcast_rule
Proof state before:
R : Type u_3
inst✝²³ : Ring R
X : Type u_5
inst✝²² : AddCommGroup X
inst✝²¹ : Module R X
Y : Type u_6
inst✝²⁰ : AddCommGroup Y
inst✝¹⁹ : Module R Y
Z : Type ?u.308523
inst✝¹⁸ : AddCommGroup Z
inst✝¹⁷ : Module R Z
ι : Type u_4
tag : Lean.Name
MR : Type ?u.309262
inst✝¹⁶ : AddCommGroup MR
inst✝¹⁵ : Module R MR
inst✝¹⁴ : BroadcastType tag R ι R MR
MX : Type u_1
inst✝¹³ : AddCommGroup MX
inst✝¹² : Module R MX
inst✝¹¹ : BroadcastType tag R ι X MX
MY : Type u_2
inst✝¹⁰ : AddCommGroup MY
inst✝⁹ : Module R MY
inst✝⁸ : BroadcastType tag R ι Y MY
MZ : Type ?u.312404
inst✝⁷ : AddCommGroup MZ
inst✝⁶ : Module R MZ
inst✝⁵ : BroadcastType tag R ι Z MZ
κ : Type ?u.313202
E : κ → Type ?u.313207
ME : κ → Type ?u.313212
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)
c : R
f : X → Y
⊢ (broadcast tag R ι fun x => c • f x) = fun mx => c • broadcast tag R ι f mx
Tactic:
funext mx
Proof state after:
case h
R : Type u_3
inst✝²³ : Ring R
X : Type u_5
inst✝²² : AddCommGroup X
inst✝²¹ : Module R X
Y : Type u_6
inst✝²⁰ : AddCommGroup Y
inst✝¹⁹ : Module R Y
Z : Type ?u.308523
inst✝¹⁸ : AddCommGroup Z
inst✝¹⁷ : Module R Z
ι : Type u_4
tag : Lean.Name
MR : Type ?u.309262
inst✝¹⁶ : AddCommGroup MR
inst✝¹⁵ : Module R MR
inst✝¹⁴ : BroadcastType tag R ι R MR
MX : Type u_1
inst✝¹³ : AddCommGroup MX
inst✝¹² : Module R MX
inst✝¹¹ : BroadcastType tag R ι X MX
MY : Type u_2
inst✝¹⁰ : AddCommGroup MY
inst✝⁹ : Module R MY
inst✝⁸ : BroadcastType tag R ι Y MY
MZ : Type ?u.312404
inst✝⁷ : AddCommGroup MZ
inst✝⁶ : Module R MZ
inst✝⁵ : BroadcastType tag R ι Z MZ
κ : Type ?u.313202
E : κ → Type ?u.313207
ME : κ → Type ?u.313212
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)
c : R
f : X → Y
mx : MX
⊢ broadcast tag R ι (fun x => c • f x) mx = c • broadcast tag R ι f mx
Theorem: HSMul.hSMul.arg_a1.broadcast_rule
Proof state before:
case h
R : Type u_3
inst✝²³ : Ring R
X : Type u_5
inst✝²² : AddCommGroup X
inst✝²¹ : Module R X
Y : Type u_6
inst✝²⁰ : AddCommGroup Y
inst✝¹⁹ : Module R Y
Z : Type ?u.308523
inst✝¹⁸ : AddCommGroup Z
inst✝¹⁷ : Module R Z
ι : Type u_4
tag : Lean.Name
MR : Type ?u.309262
inst✝¹⁶ : AddCommGroup MR
inst✝¹⁵ : Module R MR
inst✝¹⁴ : BroadcastType tag R ι R MR
MX : Type u_1
inst✝¹³ : AddCommGroup MX
inst✝¹² : Module R MX
inst✝¹¹ : BroadcastType tag R ι X MX
MY : Type u_2
inst✝¹⁰ : AddCommGroup MY
inst✝⁹ : Module R MY
inst✝⁸ : BroadcastType tag R ι Y MY
MZ : Type ?u.312404
inst✝⁷ : AddCommGroup MZ
inst✝⁶ : Module R MZ
inst✝⁵ : BroadcastType tag R ι Z MZ
κ : Type ?u.313202
E : κ → Type ?u.313207
ME : κ → Type ?u.313212
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)
c : R
f : X → Y
mx : MX
⊢ broadcast tag R ι (fun x => c • f x) mx = c • broadcast tag R ι f mx
Tactic:
unfold broadcast
Proof state after:
case h
R : Type u_3
inst✝²³ : Ring R
X : Type u_5
inst✝²² : AddCommGroup X
inst✝²¹ : Module R X
Y : Type u_6
inst✝²⁰ : AddCommGroup Y
inst✝¹⁹ : Module R Y
Z : Type ?u.308523
inst✝¹⁸ : AddCommGroup Z
inst✝¹⁷ : Module R Z
ι : Type u_4
tag : Lean.Name
MR : Type ?u.309262
inst✝¹⁶ : AddCommGroup MR
inst✝¹⁵ : Module R MR
inst✝¹⁴ : BroadcastType tag R ι R MR
MX : Type u_1
inst✝¹³ : AddCommGroup MX
inst✝¹² : Module R MX
inst✝¹¹ : BroadcastType tag R ι X MX
MY : Type u_2
inst✝¹⁰ : AddCommGroup MY
inst✝⁹ : Module R MY
inst✝⁸ : BroadcastType tag R ι Y MY
MZ : Type ?u.312404
inst✝⁷ : AddCommGroup MZ
inst✝⁶ : Module R MZ
inst✝⁵ : BroadcastType tag R ι Z MZ
κ : Type ?u.313202
E : κ → Type ?u.313207
ME : κ → Type ?u.313212
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)
c : R
f : X → Y
mx : MX
⊢ ((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)
Theorem: HSMul.hSMul.arg_a1.broadcast_rule
Proof state before:
case h
R : Type u_3
inst✝²³ : Ring R
X : Type u_5
inst✝²² : AddCommGroup X
inst✝²¹ : Module R X
Y : Type u_6
inst✝²⁰ : AddCommGroup Y
inst✝¹⁹ : Module R Y
Z : Type ?u.308523
inst✝¹⁸ : AddCommGroup Z
inst✝¹⁷ : Module R Z
ι : Type u_4
tag : Lean.Name
MR : Type ?u.309262
inst✝¹⁶ : AddCommGroup MR
inst✝¹⁵ : Module R MR
inst✝¹⁴ : BroadcastType tag R ι R MR
MX : Type u_1
inst✝¹³ : AddCommGroup MX
inst✝¹² : Module R MX
inst✝¹¹ : BroadcastType tag R ι X MX
MY : Type u_2
inst✝¹⁰ : AddCommGroup MY
inst✝⁹ : Module R MY
inst✝⁸ : BroadcastType tag R ι Y MY
MZ : Type ?u.312404
inst✝⁷ : AddCommGroup MZ
inst✝⁶ : Module R MZ
inst✝⁵ : BroadcastType tag R ι Z MZ
κ : Type ?u.313202
E : κ → Type ?u.313207
ME : κ → Type ?u.313212
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)
c : R
f : X → Y
mx : MX
⊢ ((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]
Proof state after:
case h
R : Type u_3
inst✝²³ : Ring R
X : Type u_5
inst✝²² : AddCommGroup X
inst✝²¹ : Module R X
Y : Type u_6
inst✝²⁰ : AddCommGroup Y
inst✝¹⁹ : Module R Y
Z : Type ?u.308523
inst✝¹⁸ : AddCommGroup Z
inst✝¹⁷ : Module R Z
ι : Type u_4
tag : Lean.Name
MR : Type ?u.309262
inst✝¹⁶ : AddCommGroup MR
inst✝¹⁵ : Module R MR
inst✝¹⁴ : BroadcastType tag R ι R MR
MX : Type u_1
inst✝¹³ : AddCommGroup MX
inst✝¹² : Module R MX
inst✝¹¹ : BroadcastType tag R ι X MX
MY : Type u_2
inst✝¹⁰ : AddCommGroup MY
inst✝⁹ : Module R MY
inst✝⁸ : BroadcastType tag R ι Y MY
MZ : Type ?u.312404
inst✝⁷ : AddCommGroup MZ
inst✝⁶ : Module R MZ
inst✝⁵ : BroadcastType tag R ι Z MZ
κ : Type ?u.313202
E : κ → Type ?u.313207
ME : κ → Type ?u.313212
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)
c : R
f : X → Y
mx : MX
⊢ ((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))
Theorem: HSMul.hSMul.arg_a1.broadcast_rule
Proof state before:
case h
R : Type u_3
inst✝²³ : Ring R
X : Type u_5
inst✝²² : AddCommGroup X
inst✝²¹ : Module R X
Y : Type u_6
inst✝²⁰ : AddCommGroup Y
inst✝¹⁹ : Module R Y
Z : Type ?u.308523
inst✝¹⁸ : AddCommGroup Z
inst✝¹⁷ : Module R Z
ι : Type u_4
tag : Lean.Name
MR : Type ?u.309262
inst✝¹⁶ : AddCommGroup MR
inst✝¹⁵ : Module R MR
inst✝¹⁴ : BroadcastType tag R ι R MR
MX : Type u_1
inst✝¹³ : AddCommGroup MX
inst✝¹² : Module R MX
inst✝¹¹ : BroadcastType tag R ι X MX
MY : Type u_2
inst✝¹⁰ : AddCommGroup MY
inst✝⁹ : Module R MY
inst✝⁸ : BroadcastType tag R ι Y MY
MZ : Type ?u.312404
inst✝⁷ : AddCommGroup MZ
inst✝⁶ : Module R MZ
inst✝⁵ : BroadcastType tag R ι Z MZ
κ : Type ?u.313202
E : κ → Type ?u.313207
ME : κ → Type ?u.313212
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)
c : R
f : X → Y
mx : MX
⊢ ((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
Proof state after:
no goals
Theorem: HSMul.hSMul.arg_a0.broadcast_rule
Proof state before:
R : Type u_1
inst✝²⁵ : Ring R
X : Type u_2
inst✝²⁴ : AddCommGroup X
inst✝²³ : Module R X
Y : Type u_4
inst✝²² : AddCommGroup Y
inst✝²¹ : Module R Y
Z : Type ?u.329177
inst✝²⁰ : AddCommGroup Z
inst✝¹⁹ : Module R Z
ι : Type ?u.329911
tag : Lean.Name
MR : Type ?u.329916
inst✝¹⁸ : AddCommGroup MR
inst✝¹⁷ : Module R MR
inst✝¹⁶ : BroadcastType tag R ι R MR
MX : Type u_3
inst✝¹⁵ : AddCommGroup MX
inst✝¹⁴ : Module R MX
inst✝¹³ : BroadcastType tag R ι X MX
MY : Type u_5
inst✝¹² : AddCommGroup MY
inst✝¹¹ : Module R MY
inst✝¹⁰ : BroadcastType tag R ι Y MY
MZ : Type ?u.333058
inst✝⁹ : AddCommGroup MZ
inst✝⁸ : Module R MZ
inst✝⁷ : BroadcastType tag R ι Z MZ
κ : Type ?u.333856
E : κ → Type ?u.333861
ME : κ → Type ?u.333866
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)
n : ℕ
f : X → R
y : Y
inst✝¹ : BroadcastType `Prod R (Fin n) X MX
inst✝ : BroadcastType `Prod R (Fin n) Y MY
⊢ (broadcast `Prod R (Fin (n + 1)) fun x => f x • y) = fun x =>
    match x with
    | (x, mx) => (f x • y, broadcast `Prod R (Fin n) (fun x => f x • y) mx)
Tactic:
funext mx
Proof state after:
case h
R : Type u_1
inst✝²⁵ : Ring R
X : Type u_2
inst✝²⁴ : AddCommGroup X
inst✝²³ : Module R X
Y : Type u_4
inst✝²² : AddCommGroup Y
inst✝²¹ : Module R Y
Z : Type ?u.329177
inst✝²⁰ : AddCommGroup Z
inst✝¹⁹ : Module R Z
ι : Type ?u.329911
tag : Lean.Name
MR : Type ?u.329916
inst✝¹⁸ : AddCommGroup MR
inst✝¹⁷ : Module R MR
inst✝¹⁶ : BroadcastType tag R ι R MR
MX : Type u_3
inst✝¹⁵ : AddCommGroup MX
inst✝¹⁴ : Module R MX
inst✝¹³ : BroadcastType tag R ι X MX
MY : Type u_5
inst✝¹² : AddCommGroup MY
inst✝¹¹ : Module R MY
inst✝¹⁰ : BroadcastType tag R ι Y MY
MZ : Type ?u.333058
inst✝⁹ : AddCommGroup MZ
inst✝⁸ : Module R MZ
inst✝⁷ : BroadcastType tag R ι Z MZ
κ : Type ?u.333856
E : κ → Type ?u.333861
ME : κ → Type ?u.333866
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)
n : ℕ
f : X → R
y : Y
inst✝¹ : BroadcastType `Prod R (Fin n) X MX
inst✝ : BroadcastType `Prod R (Fin n) Y MY
mx : X × MX
⊢ broadcast `Prod R (Fin (n + 1)) (fun x => f x • y) mx =
    match mx with
    | (x, mx) => (f x • y, broadcast `Prod R (Fin n) (fun x => f x • y) mx)
Theorem: HSMul.hSMul.arg_a0.broadcast_rule
Proof state before:
case h
R : Type u_1
inst✝²⁵ : Ring R
X : Type u_2
inst✝²⁴ : AddCommGroup X
inst✝²³ : Module R X
Y : Type u_4
inst✝²² : AddCommGroup Y
inst✝²¹ : Module R Y
Z : Type ?u.329177
inst✝²⁰ : AddCommGroup Z
inst✝¹⁹ : Module R Z
ι : Type ?u.329911
tag : Lean.Name
MR : Type ?u.329916
inst✝¹⁸ : AddCommGroup MR
inst✝¹⁷ : Module R MR
inst✝¹⁶ : BroadcastType tag R ι R MR
MX : Type u_3
inst✝¹⁵ : AddCommGroup MX
inst✝¹⁴ : Module R MX
inst✝¹³ : BroadcastType tag R ι X MX
MY : Type u_5
inst✝¹² : AddCommGroup MY
inst✝¹¹ : Module R MY
inst✝¹⁰ : BroadcastType tag R ι Y MY
MZ : Type ?u.333058
inst✝⁹ : AddCommGroup MZ
inst✝⁸ : Module R MZ
inst✝⁷ : BroadcastType tag R ι Z MZ
κ : Type ?u.333856
E : κ → Type ?u.333861
ME : κ → Type ?u.333866
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)
n : ℕ
f : X → R
y : Y
inst✝¹ : BroadcastType `Prod R (Fin n) X MX
inst✝ : BroadcastType `Prod R (Fin n) Y MY
mx : X × MX
⊢ broadcast `Prod R (Fin (n + 1)) (fun x => f x • y) mx =
    match mx with
    | (x, mx) => (f x • y, broadcast `Prod R (Fin n) (fun x => f x • y) mx)
Tactic:
unfold broadcast
Proof state after:
case h
R : Type u_1
inst✝²⁵ : Ring R
X : Type u_2
inst✝²⁴ : AddCommGroup X
inst✝²³ : Module R X
Y : Type u_4
inst✝²² : AddCommGroup Y
inst✝²¹ : Module R Y
Z : Type ?u.329177
inst✝²⁰ : AddCommGroup Z
inst✝¹⁹ : Module R Z
ι : Type ?u.329911
tag : Lean.Name
MR : Type ?u.329916
inst✝¹⁸ : AddCommGroup MR
inst✝¹⁷ : Module R MR
inst✝¹⁶ : BroadcastType tag R ι R MR
MX : Type u_3
inst✝¹⁵ : AddCommGroup MX
inst✝¹⁴ : Module R MX
inst✝¹³ : BroadcastType tag R ι X MX
MY : Type u_5
inst✝¹² : AddCommGroup MY
inst✝¹¹ : Module R MY
inst✝¹⁰ : BroadcastType tag R ι Y MY
MZ : Type ?u.333058
inst✝⁹ : AddCommGroup MZ
inst✝⁸ : Module R MZ
inst✝⁷ : BroadcastType tag R ι Z MZ
κ : Type ?u.333856
E : κ → Type ?u.333861
ME : κ → Type ?u.333866
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)
n : ℕ
f : X → R
y : Y
inst✝¹ : BroadcastType `Prod R (Fin n) X MX
inst✝ : BroadcastType `Prod R (Fin n) Y MY
mx : X × MX
⊢ ((LinearEquiv.symm (BroadcastType.equiv `Prod)) fun i => (fun x => f x • y) ((BroadcastType.equiv `Prod) mx i)) =
    match mx with
    | (x, mx) =>
      (f x • y,
        (LinearEquiv.symm (BroadcastType.equiv `Prod)) fun i => (fun x => f x • y) ((BroadcastType.equiv `Prod) mx i))
Theorem: HSMul.hSMul.arg_a0.broadcast_rule
Proof state before:
case h
R : Type u_1
inst✝²⁵ : Ring R
X : Type u_2
inst✝²⁴ : AddCommGroup X
inst✝²³ : Module R X
Y : Type u_4
inst✝²² : AddCommGroup Y
inst✝²¹ : Module R Y
Z : Type ?u.329177
inst✝²⁰ : AddCommGroup Z
inst✝¹⁹ : Module R Z
ι : Type ?u.329911
tag : Lean.Name
MR : Type ?u.329916
inst✝¹⁸ : AddCommGroup MR
inst✝¹⁷ : Module R MR
inst✝¹⁶ : BroadcastType tag R ι R MR
MX : Type u_3
inst✝¹⁵ : AddCommGroup MX
inst✝¹⁴ : Module R MX
inst✝¹³ : BroadcastType tag R ι X MX
MY : Type u_5
inst✝¹² : AddCommGroup MY
inst✝¹¹ : Module R MY
inst✝¹⁰ : BroadcastType tag R ι Y MY
MZ : Type ?u.333058
inst✝⁹ : AddCommGroup MZ
inst✝⁸ : Module R MZ
inst✝⁷ : BroadcastType tag R ι Z MZ
κ : Type ?u.333856
E : κ → Type ?u.333861
ME : κ → Type ?u.333866
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)
n : ℕ
f : X → R
y : Y
inst✝¹ : BroadcastType `Prod R (Fin n) X MX
inst✝ : BroadcastType `Prod R (Fin n) Y MY
mx : X × MX
⊢ ((LinearEquiv.symm (BroadcastType.equiv `Prod)) fun i => (fun x => f x • y) ((BroadcastType.equiv `Prod) mx i)) =
    match mx with
    | (x, mx) =>
      (f x • y,
        (LinearEquiv.symm (BroadcastType.equiv `Prod)) fun i => (fun x => f x • y) ((BroadcastType.equiv `Prod) mx i))
Tactic:
rfl
Proof state after:
no goals
Theorem: SciLean.inner_proj_dualProj
Proof state before:
ι : Type u_1
K X : Type u_2
x✝ : IndexType ι
inst✝³ : LawfulIndexType ι
inst✝² : DecidableEq ι
inst✝¹ : RCLike K
inst✝ : FinVec ι K X
x y : X
⊢ ⟪x, y⟫_K = ∑ i, ℼ i x * ℼ' i y
Tactic:
calc
  ⟪x, y⟫[K] = ∑ i, ∑ j, ⟪(ℼ i x) • ⅇ[X] i, (ℼ' j y) • ⅇ' j⟫[K] := by sorry_proof _ = ∑ i, ∑ j, (ℼ i x * ℼ' j y) * ⟪ⅇ[X] i, ⅇ' j⟫[K] := by sorry_proof _ = ∑ i, ∑ j, (ℼ i x * ℼ' j y) * if i=j then 1 else 0 := by simp [FinVec.duality]
       _ = ∑ i, ℼ i x * ℼ' i y := sorry_proof
Proof state after:
no goals
Theorem: SciLean.inner_proj_dualProj
Proof state before:
ι : Type u_1
K X : Type u_2
x✝ : IndexType ι
inst✝³ : LawfulIndexType ι
inst✝² : DecidableEq ι
inst✝¹ : RCLike K
inst✝ : FinVec ι K X
x y : X
⊢ ⟪x, y⟫_K = ∑ i, ∑ j, ⟪ℼ i x • ⅇ i, ℼ' j y • ⅇ' j⟫_K
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.inner_proj_dualProj
Proof state before:
ι : Type u_1
K X : Type u_2
x✝ : IndexType ι
inst✝³ : LawfulIndexType ι
inst✝² : DecidableEq ι
inst✝¹ : RCLike K
inst✝ : FinVec ι K X
x y : X
⊢  ∑ i, ∑ j, ⟪ℼ i x • ⅇ i, ℼ' j y • ⅇ' j⟫_K = ∑ i, ∑ j, ℼ i x * ℼ' j y * ⟪ⅇ i, ⅇ' j⟫_K
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.inner_proj_dualProj
Proof state before:
ι : Type u_1
K X : Type u_2
x✝ : IndexType ι
inst✝³ : LawfulIndexType ι
inst✝² : DecidableEq ι
inst✝¹ : RCLike K
inst✝ : FinVec ι K X
x y : X
⊢  ∑ i, ∑ j, ℼ i x * ℼ' j y * ⟪ⅇ i, ⅇ' j⟫_K = ∑ i, ∑ j, ℼ i x * ℼ' j y * if i = j then 1 else 0
Tactic:
simp [FinVec.duality]
Proof state after:
no goals
Theorem: SciLean.inner_basis_dualBasis
Proof state before:
ι : Type u_3
K : Type u_1
X : Type u_2
inst✝⁴ : IndexType ι
inst✝³ : LawfulIndexType ι
inst✝² : DecidableEq ι
inst✝¹ : RCLike K
inst✝ : FinVec ι K X
i j : ι
⊢ ⟪ⅇ i, ⅇ' j⟫_K = if i = j then 1 else 0
Tactic:
apply FinVec.duality
Proof state after:
no goals
Theorem: SciLean.inner_dualBasis_basis
Proof state before:
ι : Type u_3
K : Type u_1
X : Type u_2
inst✝⁴ : IndexType ι
inst✝³ : LawfulIndexType ι
inst✝² : DecidableEq ι
inst✝¹ : RCLike K
inst✝ : FinVec ι K X
i j : ι
⊢ ⟪ⅇ' i, ⅇ j⟫_K = if i = j then 1 else 0
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.inner_dualBasis_proj
Proof state before:
ι : Type u_3
K : Type u_1
X : Type u_2
inst✝⁴ : IndexType ι
inst✝³ : LawfulIndexType ι
inst✝² : DecidableEq ι
inst✝¹ : RCLike K
inst✝ : FinVec ι K X
i : ι
x : X
⊢ ⟪x, ⅇ' i⟫_K = ℼ i x
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.inner_basis_dualProj
Proof state before:
ι : Type u_3
K : Type u_1
X : Type u_2
inst✝⁴ : IndexType ι
inst✝³ : LawfulIndexType ι
inst✝² : DecidableEq ι
inst✝¹ : RCLike K
inst✝ : FinVec ι K X
i : ι
x : X
⊢ ⟪x, ⅇ i⟫_K = ℼ' i x
Tactic:
sorry_proof
Proof state after:
no goals