internlm/Lean-Github huggingface dataset:
Theorem: Prod.fst.arg_self.broadcast_rule
Proof state before:
case h
R : Type u_5
inst✝²³ : Ring R
X : Type u_7
inst✝²² : AddCommGroup X
inst✝²¹ : Module R X
Y : Type u_1
inst✝²⁰ : AddCommGroup Y
inst✝¹⁹ : Module R Y
Z : Type u_2
inst✝¹⁸ : AddCommGroup Z
inst✝¹⁷ : Module R Z
ι : Type u_6
tag : Lean.Name
MR : Type ?u.166233
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_4
inst✝¹⁰ : AddCommGroup MY
inst✝⁹ : Module R MY
inst✝⁸ : BroadcastType tag R ι Y MY
MZ : Type u_8
inst✝⁷ : AddCommGroup MZ
inst✝⁶ : Module R MZ
inst✝⁵ : BroadcastType tag R ι Z MZ
κ : Type ?u.170173
E : κ → Type ?u.170178
ME : κ → Type ?u.170183
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 : X → Y × Z
mx : MX
⊢ broadcast tag R ι (fun x => (f x).1) mx = (broadcast tag R ι f mx).1
Tactic:
simp[broadcast, BroadcastType.equiv]
Proof state after:
no goals
Theorem: Prod.snd.arg_self.broadcast_rule
Proof state before:
R : Type u_5
inst✝²³ : Ring R
X : Type u_7
inst✝²² : AddCommGroup X
inst✝²¹ : Module R X
Y : Type u_1
inst✝²⁰ : AddCommGroup Y
inst✝¹⁹ : Module R Y
Z : Type u_2
inst✝¹⁸ : AddCommGroup Z
inst✝¹⁷ : Module R Z
ι : Type u_6
tag : Lean.Name
MR : Type ?u.192661
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_8
inst✝¹⁰ : AddCommGroup MY
inst✝⁹ : Module R MY
inst✝⁸ : BroadcastType tag R ι Y MY
MZ : Type u_4
inst✝⁷ : AddCommGroup MZ
inst✝⁶ : Module R MZ
inst✝⁵ : BroadcastType tag R ι Z MZ
κ : Type ?u.196601
E : κ → Type ?u.196606
ME : κ → Type ?u.196611
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 : X → Y × Z
⊢ (broadcast tag R ι fun x => (f x).2) = fun mx => (broadcast tag R ι f mx).2
Tactic:
funext mx
Proof state after:
case h
R : Type u_5
inst✝²³ : Ring R
X : Type u_7
inst✝²² : AddCommGroup X
inst✝²¹ : Module R X
Y : Type u_1
inst✝²⁰ : AddCommGroup Y
inst✝¹⁹ : Module R Y
Z : Type u_2
inst✝¹⁸ : AddCommGroup Z
inst✝¹⁷ : Module R Z
ι : Type u_6
tag : Lean.Name
MR : Type ?u.192661
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_8
inst✝¹⁰ : AddCommGroup MY
inst✝⁹ : Module R MY
inst✝⁸ : BroadcastType tag R ι Y MY
MZ : Type u_4
inst✝⁷ : AddCommGroup MZ
inst✝⁶ : Module R MZ
inst✝⁵ : BroadcastType tag R ι Z MZ
κ : Type ?u.196601
E : κ → Type ?u.196606
ME : κ → Type ?u.196611
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 : X → Y × Z
mx : MX
⊢ broadcast tag R ι (fun x => (f x).2) mx = (broadcast tag R ι f mx).2
Theorem: Prod.snd.arg_self.broadcast_rule
Proof state before:
case h
R : Type u_5
inst✝²³ : Ring R
X : Type u_7
inst✝²² : AddCommGroup X
inst✝²¹ : Module R X
Y : Type u_1
inst✝²⁰ : AddCommGroup Y
inst✝¹⁹ : Module R Y
Z : Type u_2
inst✝¹⁸ : AddCommGroup Z
inst✝¹⁷ : Module R Z
ι : Type u_6
tag : Lean.Name
MR : Type ?u.192661
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_8
inst✝¹⁰ : AddCommGroup MY
inst✝⁹ : Module R MY
inst✝⁸ : BroadcastType tag R ι Y MY
MZ : Type u_4
inst✝⁷ : AddCommGroup MZ
inst✝⁶ : Module R MZ
inst✝⁵ : BroadcastType tag R ι Z MZ
κ : Type ?u.196601
E : κ → Type ?u.196606
ME : κ → Type ?u.196611
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 : X → Y × Z
mx : MX
⊢ broadcast tag R ι (fun x => (f x).2) mx = (broadcast tag R ι f mx).2
Tactic:
simp[broadcast, BroadcastType.equiv]
Proof state after:
no goals
Theorem: HAdd.hAdd.arg_a0a1.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.218395
inst✝¹⁸ : AddCommGroup Z
inst✝¹⁷ : Module R Z
ι : Type u_4
tag : Lean.Name
MR : Type ?u.219134
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.222276
inst✝⁷ : AddCommGroup MZ
inst✝⁶ : Module R MZ
inst✝⁵ : BroadcastType tag R ι Z MZ
κ : Type ?u.223074
E : κ → Type ?u.223079
ME : κ → Type ?u.223084
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 g : X → Y
⊢ (broadcast tag R ι fun x => f x + g x) = fun mx => broadcast tag R ι f mx + broadcast tag R ι g 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.218395
inst✝¹⁸ : AddCommGroup Z
inst✝¹⁷ : Module R Z
ι : Type u_4
tag : Lean.Name
MR : Type ?u.219134
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.222276
inst✝⁷ : AddCommGroup MZ
inst✝⁶ : Module R MZ
inst✝⁵ : BroadcastType tag R ι Z MZ
κ : Type ?u.223074
E : κ → Type ?u.223079
ME : κ → Type ?u.223084
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 g : X → Y
mx : MX
⊢ broadcast tag R ι (fun x => f x + g x) mx = broadcast tag R ι f mx + broadcast tag R ι g mx
Theorem: HAdd.hAdd.arg_a0a1.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.218395
inst✝¹⁸ : AddCommGroup Z
inst✝¹⁷ : Module R Z
ι : Type u_4
tag : Lean.Name
MR : Type ?u.219134
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.222276
inst✝⁷ : AddCommGroup MZ
inst✝⁶ : Module R MZ
inst✝⁵ : BroadcastType tag R ι Z MZ
κ : Type ?u.223074
E : κ → Type ?u.223079
ME : κ → Type ?u.223084
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 g : X → Y
mx : MX
⊢ broadcast tag R ι (fun x => f x + g x) mx = broadcast tag R ι f mx + broadcast tag R ι g 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.218395
inst✝¹⁸ : AddCommGroup Z
inst✝¹⁷ : Module R Z
ι : Type u_4
tag : Lean.Name
MR : Type ?u.219134
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.222276
inst✝⁷ : AddCommGroup MZ
inst✝⁶ : Module R MZ
inst✝⁵ : BroadcastType tag R ι Z MZ
κ : Type ?u.223074
E : κ → Type ?u.223079
ME : κ → Type ?u.223084
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 g : X → Y
mx : MX
⊢ ((LinearEquiv.symm (BroadcastType.equiv tag)) fun i => (fun x => f x + g x) ((BroadcastType.equiv tag) mx i)) =
    ((LinearEquiv.symm (BroadcastType.equiv tag)) fun i => f ((BroadcastType.equiv tag) mx i)) +
      (LinearEquiv.symm (BroadcastType.equiv tag)) fun i => g ((BroadcastType.equiv tag) mx i)
Theorem: HAdd.hAdd.arg_a0a1.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.218395
inst✝¹⁸ : AddCommGroup Z
inst✝¹⁷ : Module R Z
ι : Type u_4
tag : Lean.Name
MR : Type ?u.219134
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.222276
inst✝⁷ : AddCommGroup MZ
inst✝⁶ : Module R MZ
inst✝⁵ : BroadcastType tag R ι Z MZ
κ : Type ?u.223074
E : κ → Type ?u.223079
ME : κ → Type ?u.223084
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 g : X → Y
mx : MX
⊢ ((LinearEquiv.symm (BroadcastType.equiv tag)) fun i => (fun x => f x + g x) ((BroadcastType.equiv tag) mx i)) =
    ((LinearEquiv.symm (BroadcastType.equiv tag)) fun i => f ((BroadcastType.equiv tag) mx i)) +
      (LinearEquiv.symm (BroadcastType.equiv tag)) fun i => g ((BroadcastType.equiv tag) mx i)
Tactic:
rw[← map_add]
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.218395
inst✝¹⁸ : AddCommGroup Z
inst✝¹⁷ : Module R Z
ι : Type u_4
tag : Lean.Name
MR : Type ?u.219134
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.222276
inst✝⁷ : AddCommGroup MZ
inst✝⁶ : Module R MZ
inst✝⁵ : BroadcastType tag R ι Z MZ
κ : Type ?u.223074
E : κ → Type ?u.223079
ME : κ → Type ?u.223084
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 g : X → Y
mx : MX
⊢ ((LinearEquiv.symm (BroadcastType.equiv tag)) fun i => (fun x => f x + g x) ((BroadcastType.equiv tag) mx i)) =
    (LinearEquiv.symm (BroadcastType.equiv tag))
      ((fun i => f ((BroadcastType.equiv tag) mx i)) + fun i => g ((BroadcastType.equiv tag) mx i))
Theorem: HAdd.hAdd.arg_a0a1.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.218395
inst✝¹⁸ : AddCommGroup Z
inst✝¹⁷ : Module R Z
ι : Type u_4
tag : Lean.Name
MR : Type ?u.219134
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.222276
inst✝⁷ : AddCommGroup MZ
inst✝⁶ : Module R MZ
inst✝⁵ : BroadcastType tag R ι Z MZ
κ : Type ?u.223074
E : κ → Type ?u.223079
ME : κ → Type ?u.223084
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 g : X → Y
mx : MX
⊢ ((LinearEquiv.symm (BroadcastType.equiv tag)) fun i => (fun x => f x + g x) ((BroadcastType.equiv tag) mx i)) =
    (LinearEquiv.symm (BroadcastType.equiv tag))
      ((fun i => f ((BroadcastType.equiv tag) mx i)) + fun i => g ((BroadcastType.equiv tag) mx i))
Tactic:
rfl
Proof state after:
no goals
Theorem: HSub.hSub.arg_a0a1.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.236266
inst✝¹⁸ : AddCommGroup Z
inst✝¹⁷ : Module R Z
ι : Type u_4
tag : Lean.Name
MR : Type ?u.237005
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.240147
inst✝⁷ : AddCommGroup MZ
inst✝⁶ : Module R MZ
inst✝⁵ : BroadcastType tag R ι Z MZ
κ : Type ?u.240945
E : κ → Type ?u.240950
ME : κ → Type ?u.240955
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 g : X → Y
⊢ (broadcast tag R ι fun x => f x - g x) = fun mx => broadcast tag R ι f mx - broadcast tag R ι g 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.236266
inst✝¹⁸ : AddCommGroup Z
inst✝¹⁷ : Module R Z
ι : Type u_4
tag : Lean.Name
MR : Type ?u.237005
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.240147
inst✝⁷ : AddCommGroup MZ
inst✝⁶ : Module R MZ
inst✝⁵ : BroadcastType tag R ι Z MZ
κ : Type ?u.240945
E : κ → Type ?u.240950
ME : κ → Type ?u.240955
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 g : X → Y
mx : MX
⊢ broadcast tag R ι (fun x => f x - g x) mx = broadcast tag R ι f mx - broadcast tag R ι g mx
Theorem: HSub.hSub.arg_a0a1.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.236266
inst✝¹⁸ : AddCommGroup Z
inst✝¹⁷ : Module R Z
ι : Type u_4
tag : Lean.Name
MR : Type ?u.237005
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.240147
inst✝⁷ : AddCommGroup MZ
inst✝⁶ : Module R MZ
inst✝⁵ : BroadcastType tag R ι Z MZ
κ : Type ?u.240945
E : κ → Type ?u.240950
ME : κ → Type ?u.240955
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 g : X → Y
mx : MX
⊢ broadcast tag R ι (fun x => f x - g x) mx = broadcast tag R ι f mx - broadcast tag R ι g 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.236266
inst✝¹⁸ : AddCommGroup Z
inst✝¹⁷ : Module R Z
ι : Type u_4
tag : Lean.Name
MR : Type ?u.237005
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.240147
inst✝⁷ : AddCommGroup MZ
inst✝⁶ : Module R MZ
inst✝⁵ : BroadcastType tag R ι Z MZ
κ : Type ?u.240945
E : κ → Type ?u.240950
ME : κ → Type ?u.240955
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 g : X → Y
mx : MX
⊢ ((LinearEquiv.symm (BroadcastType.equiv tag)) fun i => (fun x => f x - g x) ((BroadcastType.equiv tag) mx i)) =
    ((LinearEquiv.symm (BroadcastType.equiv tag)) fun i => f ((BroadcastType.equiv tag) mx i)) -
      (LinearEquiv.symm (BroadcastType.equiv tag)) fun i => g ((BroadcastType.equiv tag) mx i)
Theorem: HSub.hSub.arg_a0a1.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.236266
inst✝¹⁸ : AddCommGroup Z
inst✝¹⁷ : Module R Z
ι : Type u_4
tag : Lean.Name
MR : Type ?u.237005
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.240147
inst✝⁷ : AddCommGroup MZ
inst✝⁶ : Module R MZ
inst✝⁵ : BroadcastType tag R ι Z MZ
κ : Type ?u.240945
E : κ → Type ?u.240950
ME : κ → Type ?u.240955
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 g : X → Y
mx : MX
⊢ ((LinearEquiv.symm (BroadcastType.equiv tag)) fun i => (fun x => f x - g x) ((BroadcastType.equiv tag) mx i)) =
    ((LinearEquiv.symm (BroadcastType.equiv tag)) fun i => f ((BroadcastType.equiv tag) mx i)) -
      (LinearEquiv.symm (BroadcastType.equiv tag)) fun i => g ((BroadcastType.equiv tag) mx i)
Tactic:
rw[← map_sub]
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.236266
inst✝¹⁸ : AddCommGroup Z
inst✝¹⁷ : Module R Z
ι : Type u_4
tag : Lean.Name
MR : Type ?u.237005
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.240147
inst✝⁷ : AddCommGroup MZ
inst✝⁶ : Module R MZ
inst✝⁵ : BroadcastType tag R ι Z MZ
κ : Type ?u.240945
E : κ → Type ?u.240950
ME : κ → Type ?u.240955
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 g : X → Y
mx : MX
⊢ ((LinearEquiv.symm (BroadcastType.equiv tag)) fun i => (fun x => f x - g x) ((BroadcastType.equiv tag) mx i)) =
    (LinearEquiv.symm (BroadcastType.equiv tag))
      ((fun i => f ((BroadcastType.equiv tag) mx i)) - fun i => g ((BroadcastType.equiv tag) mx i))
Theorem: HSub.hSub.arg_a0a1.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.236266
inst✝¹⁸ : AddCommGroup Z
inst✝¹⁷ : Module R Z
ι : Type u_4
tag : Lean.Name
MR : Type ?u.237005
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.240147
inst✝⁷ : AddCommGroup MZ
inst✝⁶ : Module R MZ
inst✝⁵ : BroadcastType tag R ι Z MZ
κ : Type ?u.240945
E : κ → Type ?u.240950
ME : κ → Type ?u.240955
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 g : X → Y
mx : MX
⊢ ((LinearEquiv.symm (BroadcastType.equiv tag)) fun i => (fun x => f x - g x) ((BroadcastType.equiv tag) mx i)) =
    (LinearEquiv.symm (BroadcastType.equiv tag))
      ((fun i => f ((BroadcastType.equiv tag) mx i)) - fun i => g ((BroadcastType.equiv tag) mx i))
Tactic:
rfl
Proof state after:
no goals
Theorem: Neg.neg.arg_a0.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.252585
inst✝¹⁸ : AddCommGroup Z
inst✝¹⁷ : Module R Z
ι : Type u_4
tag : Lean.Name
MR : Type ?u.253324
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.256466
inst✝⁷ : AddCommGroup MZ
inst✝⁶ : Module R MZ
inst✝⁵ : BroadcastType tag R ι Z MZ
κ : Type ?u.257264
E : κ → Type ?u.257269
ME : κ → Type ?u.257274
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 : X → Y
⊢ (broadcast tag R ι fun x => -f x) = fun mx => -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.252585
inst✝¹⁸ : AddCommGroup Z
inst✝¹⁷ : Module R Z
ι : Type u_4
tag : Lean.Name
MR : Type ?u.253324
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.256466
inst✝⁷ : AddCommGroup MZ
inst✝⁶ : Module R MZ
inst✝⁵ : BroadcastType tag R ι Z MZ
κ : Type ?u.257264
E : κ → Type ?u.257269
ME : κ → Type ?u.257274
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 : X → Y
mx : MX
⊢ broadcast tag R ι (fun x => -f x) mx = -broadcast tag R ι f mx