[GOAL]
R : Type u
inst✝ : Ring R
ι : Type v
Z : ι → ModuleCatMax R
s : Cone (Discrete.functor Z)
j : Discrete ι
⊢ (fun s => LinearMap.pi fun j => NatTrans.app s.π { as := j }) s ≫ NatTrans.app (productCone Z).π j =
    NatTrans.app s.π j
[PROOFSTEP]
cases j
[GOAL]
case mk
R : Type u
inst✝ : Ring R
ι : Type v
Z : ι → ModuleCatMax R
s : Cone (Discrete.functor Z)
as✝ : ι
⊢ (fun s => LinearMap.pi fun j => NatTrans.app s.π { as := j }) s ≫ NatTrans.app (productCone Z).π { as := as✝ } =
    NatTrans.app s.π { as := as✝ }
[PROOFSTEP]
aesop
[GOAL]
R : Type u
inst✝ : Ring R
ι : Type v
Z : ι → ModuleCatMax R
s : Cone (Discrete.functor Z)
m : s.pt ⟶ (productCone Z).pt
w : ∀ (j : Discrete ι), m ≫ NatTrans.app (productCone Z).π j = NatTrans.app s.π j
⊢ m = (fun s => LinearMap.pi fun j => NatTrans.app s.π { as := j }) s
[PROOFSTEP]
ext x
[GOAL]
case h
R : Type u
inst✝ : Ring R
ι : Type v
Z : ι → ModuleCatMax R
s : Cone (Discrete.functor Z)
m : s.pt ⟶ (productCone Z).pt
w : ∀ (j : Discrete ι), m ≫ NatTrans.app (productCone Z).π j = NatTrans.app s.π j
x : ↑s.pt
⊢ ↑m x = ↑((fun s => LinearMap.pi fun j => NatTrans.app s.π { as := j }) s) x
[PROOFSTEP]
funext i
[GOAL]
case h.h
R : Type u
inst✝ : Ring R
ι : Type v
Z : ι → ModuleCatMax R
s : Cone (Discrete.functor Z)
m : s.pt ⟶ (productCone Z).pt
w : ∀ (j : Discrete ι), m ≫ NatTrans.app (productCone Z).π j = NatTrans.app s.π j
x : ↑s.pt
i : ι
⊢ ↑m x i = ↑((fun s => LinearMap.pi fun j => NatTrans.app s.π { as := j }) s) x i
[PROOFSTEP]
exact LinearMap.congr_fun (w ⟨i⟩) x
