Theorem: SciLean.StructType.structMake_zero (SciLean/Data/StructType/Algebra.lean)

State before:
K : Type u_4
inst✝¹⁴ : RCLike K
ι : Type ?u.168462
κ : Type ?u.168465
inst✝¹³ : IndexType ι
inst✝¹² : LawfulIndexType ι
inst✝¹¹ : DecidableEq ι
inst✝¹⁰ : IndexType κ
inst✝⁹ : LawfulIndexType κ
inst✝⁸ : DecidableEq κ
E : Type ?u.168512
I : Type u_2
EI : I → Type ?u.168520
inst✝⁷ : StructType E I EI
F : Type ?u.168531
J : Type ?u.168534
FJ : J → Type ?u.168539
inst✝⁶ : StructType F J FJ
X : Type u_1
XI : I → Type u_3
inst✝⁵ : StructType X I XI
inst✝⁴ : DecidableEq I
inst✝³ : (i : I) → Vec K (XI i)
inst✝² : Vec K X
inst✝¹ : VecStruct K X I XI
W : Type ?u.168663
inst✝ : Vec K W
⊢ (structMake fun x => 0) = 0
Tactic:
apply structExt (I:=I)
State after:
case a
K : Type u_4
inst✝¹⁴ : RCLike K
ι : Type ?u.168462
κ : Type ?u.168465
inst✝¹³ : IndexType ι
inst✝¹² : LawfulIndexType ι
inst✝¹¹ : DecidableEq ι
inst✝¹⁰ : IndexType κ
inst✝⁹ : LawfulIndexType κ
inst✝⁸ : DecidableEq κ
E : Type ?u.168512
I : Type u_2
EI : I → Type ?u.168520
inst✝⁷ : StructType E I EI
F : Type ?u.168531
J : Type ?u.168534
FJ : J → Type ?u.168539
inst✝⁶ : StructType F J FJ
X : Type u_1
XI : I → Type u_3
inst✝⁵ : StructType X I XI
inst✝⁴ : DecidableEq I
inst✝³ : (i : I) → Vec K (XI i)
inst✝² : Vec K X
inst✝¹ : VecStruct K X I XI
W : Type ?u.168663
inst✝ : Vec K W
⊢ ∀ (i : I), structProj (structMake fun x => 0) i = structProj 0 i

State before:
case a
K : Type u_4
inst✝¹⁴ : RCLike K
ι : Type ?u.168462
κ : Type ?u.168465
inst✝¹³ : IndexType ι
inst✝¹² : LawfulIndexType ι
inst✝¹¹ : DecidableEq ι
inst✝¹⁰ : IndexType κ
inst✝⁹ : LawfulIndexType κ
inst✝⁸ : DecidableEq κ
E : Type ?u.168512
I : Type u_2
EI : I → Type ?u.168520
inst✝⁷ : StructType E I EI
F : Type ?u.168531
J : Type ?u.168534
FJ : J → Type ?u.168539
inst✝⁶ : StructType F J FJ
X : Type u_1
XI : I → Type u_3
inst✝⁵ : StructType X I XI
inst✝⁴ : DecidableEq I
inst✝³ : (i : I) → Vec K (XI i)
inst✝² : Vec K X
inst✝¹ : VecStruct K X I XI
W : Type ?u.168663
inst✝ : Vec K W
⊢ ∀ (i : I), structProj (structMake fun x => 0) i = structProj 0 i
Tactic:
simp
State after:
no goals