Theorem: HSMul.hSMul.arg_a0.broadcast_rule (SciLean/Core/FunctionTransformations/Broadcast.lean)

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
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)

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
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))

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
State after:
no goals