Theorem: SciLean.revDerivProj.apply_rule (SciLean/Core/FunctionTransformations/RevDeriv.lean)

State before:
K : Type u_5
I : Type u_1
inst✝²⁵ : RCLike K
X : Type ?u.116532
inst✝²⁴ : SemiInnerProductSpace K X
Y : Type ?u.116545
inst✝²³ : SemiInnerProductSpace K Y
Z : Type ?u.116556
inst✝²² : SemiInnerProductSpace K Z
W : Type ?u.116567
inst✝²¹ : SemiInnerProductSpace K W
ι : Type u_2
inst✝²⁰ : IndexType ι
inst✝¹⁹ : LawfulIndexType ι
inst✝¹⁸ : DecidableEq ι
κ : Type ?u.116603
inst✝¹⁷ : IndexType κ
inst✝¹⁶ : LawfulIndexType κ
inst✝¹⁵ : DecidableEq κ
E : Type u_3
EI : I → Type u_4
inst✝¹⁴ : StructType E I EI
inst✝¹³ : IndexType I
inst✝¹² : LawfulIndexType I
inst✝¹¹ : DecidableEq I
inst✝¹⁰ : SemiInnerProductSpace K E
inst✝⁹ : (i : I) → SemiInnerProductSpace K (EI i)
inst✝⁸ : SemiInnerProductSpaceStruct K E I EI
F : Type ?u.116767
J : Type ?u.116770
FJ : J → Type ?u.116775
inst✝⁷ : StructType F J FJ
inst✝⁶ : IndexType J
inst✝⁵ : LawfulIndexType J
inst✝⁴ : DecidableEq J
inst✝³ : SemiInnerProductSpace K F
inst✝² : (j : J) → SemiInnerProductSpace K (FJ j)
inst✝¹ : SemiInnerProductSpaceStruct K F J FJ
inst✝ : DecidableEq I
i : ι
⊢ (revDerivProj K I fun f => f i) = fun f => (f i, fun j dxj => oneHot (i, j) dxj)
Tactic:
unfold revDerivProj
State after:
K : Type u_5
I : Type u_1
inst✝²⁵ : RCLike K
X : Type ?u.116532
inst✝²⁴ : SemiInnerProductSpace K X
Y : Type ?u.116545
inst✝²³ : SemiInnerProductSpace K Y
Z : Type ?u.116556
inst✝²² : SemiInnerProductSpace K Z
W : Type ?u.116567
inst✝²¹ : SemiInnerProductSpace K W
ι : Type u_2
inst✝²⁰ : IndexType ι
inst✝¹⁹ : LawfulIndexType ι
inst✝¹⁸ : DecidableEq ι
κ : Type ?u.116603
inst✝¹⁷ : IndexType κ
inst✝¹⁶ : LawfulIndexType κ
inst✝¹⁵ : DecidableEq κ
E : Type u_3
EI : I → Type u_4
inst✝¹⁴ : StructType E I EI
inst✝¹³ : IndexType I
inst✝¹² : LawfulIndexType I
inst✝¹¹ : DecidableEq I
inst✝¹⁰ : SemiInnerProductSpace K E
inst✝⁹ : (i : I) → SemiInnerProductSpace K (EI i)
inst✝⁸ : SemiInnerProductSpaceStruct K E I EI
F : Type ?u.116767
J : Type ?u.116770
FJ : J → Type ?u.116775
inst✝⁷ : StructType F J FJ
inst✝⁶ : IndexType J
inst✝⁵ : LawfulIndexType J
inst✝⁴ : DecidableEq J
inst✝³ : SemiInnerProductSpace K F
inst✝² : (j : J) → SemiInnerProductSpace K (FJ j)
inst✝¹ : SemiInnerProductSpaceStruct K F J FJ
inst✝ : DecidableEq I
i : ι
⊢ (fun x =>
      let ydf' := revDeriv K (fun f => f i) x;
      (ydf'.1, fun i de => ydf'.2 (oneHot i de))) =
    fun f => (f i, fun j dxj => oneHot (i, j) dxj)

State before:
K : Type u_5
I : Type u_1
inst✝²⁵ : RCLike K
X : Type ?u.116532
inst✝²⁴ : SemiInnerProductSpace K X
Y : Type ?u.116545
inst✝²³ : SemiInnerProductSpace K Y
Z : Type ?u.116556
inst✝²² : SemiInnerProductSpace K Z
W : Type ?u.116567
inst✝²¹ : SemiInnerProductSpace K W
ι : Type u_2
inst✝²⁰ : IndexType ι
inst✝¹⁹ : LawfulIndexType ι
inst✝¹⁸ : DecidableEq ι
κ : Type ?u.116603
inst✝¹⁷ : IndexType κ
inst✝¹⁶ : LawfulIndexType κ
inst✝¹⁵ : DecidableEq κ
E : Type u_3
EI : I → Type u_4
inst✝¹⁴ : StructType E I EI
inst✝¹³ : IndexType I
inst✝¹² : LawfulIndexType I
inst✝¹¹ : DecidableEq I
inst✝¹⁰ : SemiInnerProductSpace K E
inst✝⁹ : (i : I) → SemiInnerProductSpace K (EI i)
inst✝⁸ : SemiInnerProductSpaceStruct K E I EI
F : Type ?u.116767
J : Type ?u.116770
FJ : J → Type ?u.116775
inst✝⁷ : StructType F J FJ
inst✝⁶ : IndexType J
inst✝⁵ : LawfulIndexType J
inst✝⁴ : DecidableEq J
inst✝³ : SemiInnerProductSpace K F
inst✝² : (j : J) → SemiInnerProductSpace K (FJ j)
inst✝¹ : SemiInnerProductSpaceStruct K F J FJ
inst✝ : DecidableEq I
i : ι
⊢ (fun x =>
      let ydf' := revDeriv K (fun f => f i) x;
      (ydf'.1, fun i de => ydf'.2 (oneHot i de))) =
    fun f => (f i, fun j dxj => oneHot (i, j) dxj)
Tactic:
fun_trans
State after:
K : Type u_5
I : Type u_1
inst✝²⁵ : RCLike K
X : Type ?u.116532
inst✝²⁴ : SemiInnerProductSpace K X
Y : Type ?u.116545
inst✝²³ : SemiInnerProductSpace K Y
Z : Type ?u.116556
inst✝²² : SemiInnerProductSpace K Z
W : Type ?u.116567
inst✝²¹ : SemiInnerProductSpace K W
ι : Type u_2
inst✝²⁰ : IndexType ι
inst✝¹⁹ : LawfulIndexType ι
inst✝¹⁸ : DecidableEq ι
κ : Type ?u.116603
inst✝¹⁷ : IndexType κ
inst✝¹⁶ : LawfulIndexType κ
inst✝¹⁵ : DecidableEq κ
E : Type u_3
EI : I → Type u_4
inst✝¹⁴ : StructType E I EI
inst✝¹³ : IndexType I
inst✝¹² : LawfulIndexType I
inst✝¹¹ : DecidableEq I
inst✝¹⁰ : SemiInnerProductSpace K E
inst✝⁹ : (i : I) → SemiInnerProductSpace K (EI i)
inst✝⁸ : SemiInnerProductSpaceStruct K E I EI
F : Type ?u.116767
J : Type ?u.116770
FJ : J → Type ?u.116775
inst✝⁷ : StructType F J FJ
inst✝⁶ : IndexType J
inst✝⁵ : LawfulIndexType J
inst✝⁴ : DecidableEq J
inst✝³ : SemiInnerProductSpace K F
inst✝² : (j : J) → SemiInnerProductSpace K (FJ j)
inst✝¹ : SemiInnerProductSpaceStruct K F J FJ
inst✝ : DecidableEq I
i : ι
⊢ (fun x => (x i, fun i_1 de => oneHot i (oneHot i_1 de))) = fun f => (f i, fun j dxj => oneHot (i, j) dxj)

State before:
K : Type u_5
I : Type u_1
inst✝²⁵ : RCLike K
X : Type ?u.116532
inst✝²⁴ : SemiInnerProductSpace K X
Y : Type ?u.116545
inst✝²³ : SemiInnerProductSpace K Y
Z : Type ?u.116556
inst✝²² : SemiInnerProductSpace K Z
W : Type ?u.116567
inst✝²¹ : SemiInnerProductSpace K W
ι : Type u_2
inst✝²⁰ : IndexType ι
inst✝¹⁹ : LawfulIndexType ι
inst✝¹⁸ : DecidableEq ι
κ : Type ?u.116603
inst✝¹⁷ : IndexType κ
inst✝¹⁶ : LawfulIndexType κ
inst✝¹⁵ : DecidableEq κ
E : Type u_3
EI : I → Type u_4
inst✝¹⁴ : StructType E I EI
inst✝¹³ : IndexType I
inst✝¹² : LawfulIndexType I
inst✝¹¹ : DecidableEq I
inst✝¹⁰ : SemiInnerProductSpace K E
inst✝⁹ : (i : I) → SemiInnerProductSpace K (EI i)
inst✝⁸ : SemiInnerProductSpaceStruct K E I EI
F : Type ?u.116767
J : Type ?u.116770
FJ : J → Type ?u.116775
inst✝⁷ : StructType F J FJ
inst✝⁶ : IndexType J
inst✝⁵ : LawfulIndexType J
inst✝⁴ : DecidableEq J
inst✝³ : SemiInnerProductSpace K F
inst✝² : (j : J) → SemiInnerProductSpace K (FJ j)
inst✝¹ : SemiInnerProductSpaceStruct K F J FJ
inst✝ : DecidableEq I
i : ι
⊢ (fun x => (x i, fun i_1 de => oneHot i (oneHot i_1 de))) = fun f => (f i, fun j dxj => oneHot (i, j) dxj)
Tactic:
simp[oneHot]
State after:
K : Type u_5
I : Type u_1
inst✝²⁵ : RCLike K
X : Type ?u.116532
inst✝²⁴ : SemiInnerProductSpace K X
Y : Type ?u.116545
inst✝²³ : SemiInnerProductSpace K Y
Z : Type ?u.116556
inst✝²² : SemiInnerProductSpace K Z
W : Type ?u.116567
inst✝²¹ : SemiInnerProductSpace K W
ι : Type u_2
inst✝²⁰ : IndexType ι
inst✝¹⁹ : LawfulIndexType ι
inst✝¹⁸ : DecidableEq ι
κ : Type ?u.116603
inst✝¹⁷ : IndexType κ
inst✝¹⁶ : LawfulIndexType κ
inst✝¹⁵ : DecidableEq κ
E : Type u_3
EI : I → Type u_4
inst✝¹⁴ : StructType E I EI
inst✝¹³ : IndexType I
inst✝¹² : LawfulIndexType I
inst✝¹¹ : DecidableEq I
inst✝¹⁰ : SemiInnerProductSpace K E
inst✝⁹ : (i : I) → SemiInnerProductSpace K (EI i)
inst✝⁸ : SemiInnerProductSpaceStruct K E I EI
F : Type ?u.116767
J : Type ?u.116770
FJ : J → Type ?u.116775
inst✝⁷ : StructType F J FJ
inst✝⁶ : IndexType J
inst✝⁵ : LawfulIndexType J
inst✝⁴ : DecidableEq J
inst✝³ : SemiInnerProductSpace K F
inst✝² : (j : J) → SemiInnerProductSpace K (FJ j)
inst✝¹ : SemiInnerProductSpaceStruct K F J FJ
inst✝ : DecidableEq I
i : ι
⊢ (fun x => (x i, fun i_1 de i_2 => if i = i_2 then structMake fun i' => if h : i_1 = i' then h ▸ de else 0 else 0)) =
    fun f => (f i, fun j dxj j_1 => structMake fun i_1 => if h : i = j_1 ∧ j = i_1 then ⋯ ▸ dxj else 0)

State before:
K : Type u_5
I : Type u_1
inst✝²⁵ : RCLike K
X : Type ?u.116532
inst✝²⁴ : SemiInnerProductSpace K X
Y : Type ?u.116545
inst✝²³ : SemiInnerProductSpace K Y
Z : Type ?u.116556
inst✝²² : SemiInnerProductSpace K Z
W : Type ?u.116567
inst✝²¹ : SemiInnerProductSpace K W
ι : Type u_2
inst✝²⁰ : IndexType ι
inst✝¹⁹ : LawfulIndexType ι
inst✝¹⁸ : DecidableEq ι
κ : Type ?u.116603
inst✝¹⁷ : IndexType κ
inst✝¹⁶ : LawfulIndexType κ
inst✝¹⁵ : DecidableEq κ
E : Type u_3
EI : I → Type u_4
inst✝¹⁴ : StructType E I EI
inst✝¹³ : IndexType I
inst✝¹² : LawfulIndexType I
inst✝¹¹ : DecidableEq I
inst✝¹⁰ : SemiInnerProductSpace K E
inst✝⁹ : (i : I) → SemiInnerProductSpace K (EI i)
inst✝⁸ : SemiInnerProductSpaceStruct K E I EI
F : Type ?u.116767
J : Type ?u.116770
FJ : J → Type ?u.116775
inst✝⁷ : StructType F J FJ
inst✝⁶ : IndexType J
inst✝⁵ : LawfulIndexType J
inst✝⁴ : DecidableEq J
inst✝³ : SemiInnerProductSpace K F
inst✝² : (j : J) → SemiInnerProductSpace K (FJ j)
inst✝¹ : SemiInnerProductSpaceStruct K F J FJ
inst✝ : DecidableEq I
i : ι
⊢ (fun x => (x i, fun i_1 de i_2 => if i = i_2 then structMake fun i' => if h : i_1 = i' then h ▸ de else 0 else 0)) =
    fun f => (f i, fun j dxj j_1 => structMake fun i_1 => if h : i = j_1 ∧ j = i_1 then ⋯ ▸ dxj else 0)
Tactic:
funext x
State after:
case h
K : Type u_5
I : Type u_1
inst✝²⁵ : RCLike K
X : Type ?u.116532
inst✝²⁴ : SemiInnerProductSpace K X
Y : Type ?u.116545
inst✝²³ : SemiInnerProductSpace K Y
Z : Type ?u.116556
inst✝²² : SemiInnerProductSpace K Z
W : Type ?u.116567
inst✝²¹ : SemiInnerProductSpace K W
ι : Type u_2
inst✝²⁰ : IndexType ι
inst✝¹⁹ : LawfulIndexType ι
inst✝¹⁸ : DecidableEq ι
κ : Type ?u.116603
inst✝¹⁷ : IndexType κ
inst✝¹⁶ : LawfulIndexType κ
inst✝¹⁵ : DecidableEq κ
E : Type u_3
EI : I → Type u_4
inst✝¹⁴ : StructType E I EI
inst✝¹³ : IndexType I
inst✝¹² : LawfulIndexType I
inst✝¹¹ : DecidableEq I
inst✝¹⁰ : SemiInnerProductSpace K E
inst✝⁹ : (i : I) → SemiInnerProductSpace K (EI i)
inst✝⁸ : SemiInnerProductSpaceStruct K E I EI
F : Type ?u.116767
J : Type ?u.116770
FJ : J → Type ?u.116775
inst✝⁷ : StructType F J FJ
inst✝⁶ : IndexType J
inst✝⁵ : LawfulIndexType J
inst✝⁴ : DecidableEq J
inst✝³ : SemiInnerProductSpace K F
inst✝² : (j : J) → SemiInnerProductSpace K (FJ j)
inst✝¹ : SemiInnerProductSpaceStruct K F J FJ
inst✝ : DecidableEq I
i : ι
x : ι → E
⊢ (x i, fun i_1 de i_2 => if i = i_2 then structMake fun i' => if h : i_1 = i' then h ▸ de else 0 else 0) =
    (x i, fun j dxj j_1 => structMake fun i_1 => if h : i = j_1 ∧ j = i_1 then ⋯ ▸ dxj else 0)

State before:
case h
K : Type u_5
I : Type u_1
inst✝²⁵ : RCLike K
X : Type ?u.116532
inst✝²⁴ : SemiInnerProductSpace K X
Y : Type ?u.116545
inst✝²³ : SemiInnerProductSpace K Y
Z : Type ?u.116556
inst✝²² : SemiInnerProductSpace K Z
W : Type ?u.116567
inst✝²¹ : SemiInnerProductSpace K W
ι : Type u_2
inst✝²⁰ : IndexType ι
inst✝¹⁹ : LawfulIndexType ι
inst✝¹⁸ : DecidableEq ι
κ : Type ?u.116603
inst✝¹⁷ : IndexType κ
inst✝¹⁶ : LawfulIndexType κ
inst✝¹⁵ : DecidableEq κ
E : Type u_3
EI : I → Type u_4
inst✝¹⁴ : StructType E I EI
inst✝¹³ : IndexType I
inst✝¹² : LawfulIndexType I
inst✝¹¹ : DecidableEq I
inst✝¹⁰ : SemiInnerProductSpace K E
inst✝⁹ : (i : I) → SemiInnerProductSpace K (EI i)
inst✝⁸ : SemiInnerProductSpaceStruct K E I EI
F : Type ?u.116767
J : Type ?u.116770
FJ : J → Type ?u.116775
inst✝⁷ : StructType F J FJ
inst✝⁶ : IndexType J
inst✝⁵ : LawfulIndexType J
inst✝⁴ : DecidableEq J
inst✝³ : SemiInnerProductSpace K F
inst✝² : (j : J) → SemiInnerProductSpace K (FJ j)
inst✝¹ : SemiInnerProductSpaceStruct K F J FJ
inst✝ : DecidableEq I
i : ι
x : ι → E
⊢ (x i, fun i_1 de i_2 => if i = i_2 then structMake fun i' => if h : i_1 = i' then h ▸ de else 0 else 0) =
    (x i, fun j dxj j_1 => structMake fun i_1 => if h : i = j_1 ∧ j = i_1 then ⋯ ▸ dxj else 0)
Tactic:
simp
State after:
case h
K : Type u_5
I : Type u_1
inst✝²⁵ : RCLike K
X : Type ?u.116532
inst✝²⁴ : SemiInnerProductSpace K X
Y : Type ?u.116545
inst✝²³ : SemiInnerProductSpace K Y
Z : Type ?u.116556
inst✝²² : SemiInnerProductSpace K Z
W : Type ?u.116567
inst✝²¹ : SemiInnerProductSpace K W
ι : Type u_2
inst✝²⁰ : IndexType ι
inst✝¹⁹ : LawfulIndexType ι
inst✝¹⁸ : DecidableEq ι
κ : Type ?u.116603
inst✝¹⁷ : IndexType κ
inst✝¹⁶ : LawfulIndexType κ
inst✝¹⁵ : DecidableEq κ
E : Type u_3
EI : I → Type u_4
inst✝¹⁴ : StructType E I EI
inst✝¹³ : IndexType I
inst✝¹² : LawfulIndexType I
inst✝¹¹ : DecidableEq I
inst✝¹⁰ : SemiInnerProductSpace K E
inst✝⁹ : (i : I) → SemiInnerProductSpace K (EI i)
inst✝⁸ : SemiInnerProductSpaceStruct K E I EI
F : Type ?u.116767
J : Type ?u.116770
FJ : J → Type ?u.116775
inst✝⁷ : StructType F J FJ
inst✝⁶ : IndexType J
inst✝⁵ : LawfulIndexType J
inst✝⁴ : DecidableEq J
inst✝³ : SemiInnerProductSpace K F
inst✝² : (j : J) → SemiInnerProductSpace K (FJ j)
inst✝¹ : SemiInnerProductSpaceStruct K F J FJ
inst✝ : DecidableEq I
i : ι
x : ι → E
⊢ (fun i_1 de i_2 => if i = i_2 then structMake fun i' => if h : i_1 = i' then h ▸ de else 0 else 0) = fun j dxj j_1 =>
    structMake fun i_1 => if h : i = j_1 ∧ j = i_1 then ⋯ ▸ dxj else 0

State before:
case h
K : Type u_5
I : Type u_1
inst✝²⁵ : RCLike K
X : Type ?u.116532
inst✝²⁴ : SemiInnerProductSpace K X
Y : Type ?u.116545
inst✝²³ : SemiInnerProductSpace K Y
Z : Type ?u.116556
inst✝²² : SemiInnerProductSpace K Z
W : Type ?u.116567
inst✝²¹ : SemiInnerProductSpace K W
ι : Type u_2
inst✝²⁰ : IndexType ι
inst✝¹⁹ : LawfulIndexType ι
inst✝¹⁸ : DecidableEq ι
κ : Type ?u.116603
inst✝¹⁷ : IndexType κ
inst✝¹⁶ : LawfulIndexType κ
inst✝¹⁵ : DecidableEq κ
E : Type u_3
EI : I → Type u_4
inst✝¹⁴ : StructType E I EI
inst✝¹³ : IndexType I
inst✝¹² : LawfulIndexType I
inst✝¹¹ : DecidableEq I
inst✝¹⁰ : SemiInnerProductSpace K E
inst✝⁹ : (i : I) → SemiInnerProductSpace K (EI i)
inst✝⁸ : SemiInnerProductSpaceStruct K E I EI
F : Type ?u.116767
J : Type ?u.116770
FJ : J → Type ?u.116775
inst✝⁷ : StructType F J FJ
inst✝⁶ : IndexType J
inst✝⁵ : LawfulIndexType J
inst✝⁴ : DecidableEq J
inst✝³ : SemiInnerProductSpace K F
inst✝² : (j : J) → SemiInnerProductSpace K (FJ j)
inst✝¹ : SemiInnerProductSpaceStruct K F J FJ
inst✝ : DecidableEq I
i : ι
x : ι → E
⊢ (fun i_1 de i_2 => if i = i_2 then structMake fun i' => if h : i_1 = i' then h ▸ de else 0 else 0) = fun j dxj j_1 =>
    structMake fun i_1 => if h : i = j_1 ∧ j = i_1 then ⋯ ▸ dxj else 0
Tactic:
funext j de i'
State after:
case h.h.h.h
K : Type u_5
I : Type u_1
inst✝²⁵ : RCLike K
X : Type ?u.116532
inst✝²⁴ : SemiInnerProductSpace K X
Y : Type ?u.116545
inst✝²³ : SemiInnerProductSpace K Y
Z : Type ?u.116556
inst✝²² : SemiInnerProductSpace K Z
W : Type ?u.116567
inst✝²¹ : SemiInnerProductSpace K W
ι : Type u_2
inst✝²⁰ : IndexType ι
inst✝¹⁹ : LawfulIndexType ι
inst✝¹⁸ : DecidableEq ι
κ : Type ?u.116603
inst✝¹⁷ : IndexType κ
inst✝¹⁶ : LawfulIndexType κ
inst✝¹⁵ : DecidableEq κ
E : Type u_3
EI : I → Type u_4
inst✝¹⁴ : StructType E I EI
inst✝¹³ : IndexType I
inst✝¹² : LawfulIndexType I
inst✝¹¹ : DecidableEq I
inst✝¹⁰ : SemiInnerProductSpace K E
inst✝⁹ : (i : I) → SemiInnerProductSpace K (EI i)
inst✝⁸ : SemiInnerProductSpaceStruct K E I EI
F : Type ?u.116767
J : Type ?u.116770
FJ : J → Type ?u.116775
inst✝⁷ : StructType F J FJ
inst✝⁶ : IndexType J
inst✝⁵ : LawfulIndexType J
inst✝⁴ : DecidableEq J
inst✝³ : SemiInnerProductSpace K F
inst✝² : (j : J) → SemiInnerProductSpace K (FJ j)
inst✝¹ : SemiInnerProductSpaceStruct K F J FJ
inst✝ : DecidableEq I
i : ι
x : ι → E
j : I
de : EI j
i' : ι
⊢ (if i = i' then structMake fun i' => if h : j = i' then h ▸ de else 0 else 0) =
    structMake fun i_1 => if h : i = i' ∧ j = i_1 then ⋯ ▸ de else 0

State before:
case h.h.h.h
K : Type u_5
I : Type u_1
inst✝²⁵ : RCLike K
X : Type ?u.116532
inst✝²⁴ : SemiInnerProductSpace K X
Y : Type ?u.116545
inst✝²³ : SemiInnerProductSpace K Y
Z : Type ?u.116556
inst✝²² : SemiInnerProductSpace K Z
W : Type ?u.116567
inst✝²¹ : SemiInnerProductSpace K W
ι : Type u_2
inst✝²⁰ : IndexType ι
inst✝¹⁹ : LawfulIndexType ι
inst✝¹⁸ : DecidableEq ι
κ : Type ?u.116603
inst✝¹⁷ : IndexType κ
inst✝¹⁶ : LawfulIndexType κ
inst✝¹⁵ : DecidableEq κ
E : Type u_3
EI : I → Type u_4
inst✝¹⁴ : StructType E I EI
inst✝¹³ : IndexType I
inst✝¹² : LawfulIndexType I
inst✝¹¹ : DecidableEq I
inst✝¹⁰ : SemiInnerProductSpace K E
inst✝⁹ : (i : I) → SemiInnerProductSpace K (EI i)
inst✝⁸ : SemiInnerProductSpaceStruct K E I EI
F : Type ?u.116767
J : Type ?u.116770
FJ : J → Type ?u.116775
inst✝⁷ : StructType F J FJ
inst✝⁶ : IndexType J
inst✝⁵ : LawfulIndexType J
inst✝⁴ : DecidableEq J
inst✝³ : SemiInnerProductSpace K F
inst✝² : (j : J) → SemiInnerProductSpace K (FJ j)
inst✝¹ : SemiInnerProductSpaceStruct K F J FJ
inst✝ : DecidableEq I
i : ι
x : ι → E
j : I
de : EI j
i' : ι
⊢ (if i = i' then structMake fun i' => if h : j = i' then h ▸ de else 0 else 0) =
    structMake fun i_1 => if h : i = i' ∧ j = i_1 then ⋯ ▸ de else 0
Tactic:
if h:i=i' then
  subst h
  simp; congr; funext j'
  if h':j=j' then
    subst h'
    simp
  else
    simp[h']
else
  simp[h]
State after:
no goals

State before:
K : Type u_5
I : Type u_1
inst✝²⁵ : RCLike K
X : Type ?u.116532
inst✝²⁴ : SemiInnerProductSpace K X
Y : Type ?u.116545
inst✝²³ : SemiInnerProductSpace K Y
Z : Type ?u.116556
inst✝²² : SemiInnerProductSpace K Z
W : Type ?u.116567
inst✝²¹ : SemiInnerProductSpace K W
ι : Type u_2
inst✝²⁰ : IndexType ι
inst✝¹⁹ : LawfulIndexType ι
inst✝¹⁸ : DecidableEq ι
κ : Type ?u.116603
inst✝¹⁷ : IndexType κ
inst✝¹⁶ : LawfulIndexType κ
inst✝¹⁵ : DecidableEq κ
E : Type u_3
EI : I → Type u_4
inst✝¹⁴ : StructType E I EI
inst✝¹³ : IndexType I
inst✝¹² : LawfulIndexType I
inst✝¹¹ : DecidableEq I
inst✝¹⁰ : SemiInnerProductSpace K E
inst✝⁹ : (i : I) → SemiInnerProductSpace K (EI i)
inst✝⁸ : SemiInnerProductSpaceStruct K E I EI
F : Type ?u.116767
J : Type ?u.116770
FJ : J → Type ?u.116775
inst✝⁷ : StructType F J FJ
inst✝⁶ : IndexType J
inst✝⁵ : LawfulIndexType J
inst✝⁴ : DecidableEq J
inst✝³ : SemiInnerProductSpace K F
inst✝² : (j : J) → SemiInnerProductSpace K (FJ j)
inst✝¹ : SemiInnerProductSpaceStruct K F J FJ
inst✝ : DecidableEq I
i : ι
x : ι → E
j : I
de : EI j
i' : ι
h : i = i'
⊢ (if i = i' then structMake fun i' => if h : j = i' then h ▸ de else 0 else 0) =
    structMake fun i_1 => if h : i = i' ∧ j = i_1 then ⋯ ▸ de else 0
Tactic:
subst h
State after:
K : Type u_5
I : Type u_1
inst✝²⁵ : RCLike K
X : Type ?u.116532
inst✝²⁴ : SemiInnerProductSpace K X
Y : Type ?u.116545
inst✝²³ : SemiInnerProductSpace K Y
Z : Type ?u.116556
inst✝²² : SemiInnerProductSpace K Z
W : Type ?u.116567
inst✝²¹ : SemiInnerProductSpace K W
ι : Type u_2
inst✝²⁰ : IndexType ι
inst✝¹⁹ : LawfulIndexType ι
inst✝¹⁸ : DecidableEq ι
κ : Type ?u.116603
inst✝¹⁷ : IndexType κ
inst✝¹⁶ : LawfulIndexType κ
inst✝¹⁵ : DecidableEq κ
E : Type u_3
EI : I → Type u_4
inst✝¹⁴ : StructType E I EI
inst✝¹³ : IndexType I
inst✝¹² : LawfulIndexType I
inst✝¹¹ : DecidableEq I
inst✝¹⁰ : SemiInnerProductSpace K E
inst✝⁹ : (i : I) → SemiInnerProductSpace K (EI i)
inst✝⁸ : SemiInnerProductSpaceStruct K E I EI
F : Type ?u.116767
J : Type ?u.116770
FJ : J → Type ?u.116775
inst✝⁷ : StructType F J FJ
inst✝⁶ : IndexType J
inst✝⁵ : LawfulIndexType J
inst✝⁴ : DecidableEq J
inst✝³ : SemiInnerProductSpace K F
inst✝² : (j : J) → SemiInnerProductSpace K (FJ j)
inst✝¹ : SemiInnerProductSpaceStruct K F J FJ
inst✝ : DecidableEq I
i : ι
x : ι → E
j : I
de : EI j
⊢ (if i = i then structMake fun i' => if h : j = i' then h ▸ de else 0 else 0) =
    structMake fun i_1 => if h : i = i ∧ j = i_1 then ⋯ ▸ de else 0

State before:
K : Type u_5
I : Type u_1
inst✝²⁵ : RCLike K
X : Type ?u.116532
inst✝²⁴ : SemiInnerProductSpace K X
Y : Type ?u.116545
inst✝²³ : SemiInnerProductSpace K Y
Z : Type ?u.116556
inst✝²² : SemiInnerProductSpace K Z
W : Type ?u.116567
inst✝²¹ : SemiInnerProductSpace K W
ι : Type u_2
inst✝²⁰ : IndexType ι
inst✝¹⁹ : LawfulIndexType ι
inst✝¹⁸ : DecidableEq ι
κ : Type ?u.116603
inst✝¹⁷ : IndexType κ
inst✝¹⁶ : LawfulIndexType κ
inst✝¹⁵ : DecidableEq κ
E : Type u_3
EI : I → Type u_4
inst✝¹⁴ : StructType E I EI
inst✝¹³ : IndexType I
inst✝¹² : LawfulIndexType I
inst✝¹¹ : DecidableEq I
inst✝¹⁰ : SemiInnerProductSpace K E
inst✝⁹ : (i : I) → SemiInnerProductSpace K (EI i)
inst✝⁸ : SemiInnerProductSpaceStruct K E I EI
F : Type ?u.116767
J : Type ?u.116770
FJ : J → Type ?u.116775
inst✝⁷ : StructType F J FJ
inst✝⁶ : IndexType J
inst✝⁵ : LawfulIndexType J
inst✝⁴ : DecidableEq J
inst✝³ : SemiInnerProductSpace K F
inst✝² : (j : J) → SemiInnerProductSpace K (FJ j)
inst✝¹ : SemiInnerProductSpaceStruct K F J FJ
inst✝ : DecidableEq I
i : ι
x : ι → E
j : I
de : EI j
⊢ (if i = i then structMake fun i' => if h : j = i' then h ▸ de else 0 else 0) =
    structMake fun i_1 => if h : i = i ∧ j = i_1 then ⋯ ▸ de else 0
Tactic:
simp
State after:
K : Type u_5
I : Type u_1
inst✝²⁵ : RCLike K
X : Type ?u.116532
inst✝²⁴ : SemiInnerProductSpace K X
Y : Type ?u.116545
inst✝²³ : SemiInnerProductSpace K Y
Z : Type ?u.116556
inst✝²² : SemiInnerProductSpace K Z
W : Type ?u.116567
inst✝²¹ : SemiInnerProductSpace K W
ι : Type u_2
inst✝²⁰ : IndexType ι
inst✝¹⁹ : LawfulIndexType ι
inst✝¹⁸ : DecidableEq ι
κ : Type ?u.116603
inst✝¹⁷ : IndexType κ
inst✝¹⁶ : LawfulIndexType κ
inst✝¹⁵ : DecidableEq κ
E : Type u_3
EI : I → Type u_4
inst✝¹⁴ : StructType E I EI
inst✝¹³ : IndexType I
inst✝¹² : LawfulIndexType I
inst✝¹¹ : DecidableEq I
inst✝¹⁰ : SemiInnerProductSpace K E
inst✝⁹ : (i : I) → SemiInnerProductSpace K (EI i)
inst✝⁸ : SemiInnerProductSpaceStruct K E I EI
F : Type ?u.116767
J : Type ?u.116770
FJ : J → Type ?u.116775
inst✝⁷ : StructType F J FJ
inst✝⁶ : IndexType J
inst✝⁵ : LawfulIndexType J
inst✝⁴ : DecidableEq J
inst✝³ : SemiInnerProductSpace K F
inst✝² : (j : J) → SemiInnerProductSpace K (FJ j)
inst✝¹ : SemiInnerProductSpaceStruct K F J FJ
inst✝ : DecidableEq I
i : ι
x : ι → E
j : I
de : EI j
⊢ (structMake fun i' => if h : j = i' then h ▸ de else 0) = structMake fun i_1 => if h : j = i_1 then ⋯ ▸ de else 0

State before:
K : Type u_5
I : Type u_1
inst✝²⁵ : RCLike K
X : Type ?u.116532
inst✝²⁴ : SemiInnerProductSpace K X
Y : Type ?u.116545
inst✝²³ : SemiInnerProductSpace K Y
Z : Type ?u.116556
inst✝²² : SemiInnerProductSpace K Z
W : Type ?u.116567
inst✝²¹ : SemiInnerProductSpace K W
ι : Type u_2
inst✝²⁰ : IndexType ι
inst✝¹⁹ : LawfulIndexType ι
inst✝¹⁸ : DecidableEq ι
κ : Type ?u.116603
inst✝¹⁷ : IndexType κ
inst✝¹⁶ : LawfulIndexType κ
inst✝¹⁵ : DecidableEq κ
E : Type u_3
EI : I → Type u_4
inst✝¹⁴ : StructType E I EI
inst✝¹³ : IndexType I
inst✝¹² : LawfulIndexType I
inst✝¹¹ : DecidableEq I
inst✝¹⁰ : SemiInnerProductSpace K E
inst✝⁹ : (i : I) → SemiInnerProductSpace K (EI i)
inst✝⁸ : SemiInnerProductSpaceStruct K E I EI
F : Type ?u.116767
J : Type ?u.116770
FJ : J → Type ?u.116775
inst✝⁷ : StructType F J FJ
inst✝⁶ : IndexType J
inst✝⁵ : LawfulIndexType J
inst✝⁴ : DecidableEq J
inst✝³ : SemiInnerProductSpace K F
inst✝² : (j : J) → SemiInnerProductSpace K (FJ j)
inst✝¹ : SemiInnerProductSpaceStruct K F J FJ
inst✝ : DecidableEq I
i : ι
x : ι → E
j : I
de : EI j
⊢ (structMake fun i' => if h : j = i' then h ▸ de else 0) = structMake fun i_1 => if h : j = i_1 then ⋯ ▸ de else 0
Tactic:
congr
State after:
case e_f
K : Type u_5
I : Type u_1
inst✝²⁵ : RCLike K
X : Type ?u.116532
inst✝²⁴ : SemiInnerProductSpace K X
Y : Type ?u.116545
inst✝²³ : SemiInnerProductSpace K Y
Z : Type ?u.116556
inst✝²² : SemiInnerProductSpace K Z
W : Type ?u.116567
inst✝²¹ : SemiInnerProductSpace K W
ι : Type u_2
inst✝²⁰ : IndexType ι
inst✝¹⁹ : LawfulIndexType ι
inst✝¹⁸ : DecidableEq ι
κ : Type ?u.116603
inst✝¹⁷ : IndexType κ
inst✝¹⁶ : LawfulIndexType κ
inst✝¹⁵ : DecidableEq κ
E : Type u_3
EI : I → Type u_4
inst✝¹⁴ : StructType E I EI
inst✝¹³ : IndexType I
inst✝¹² : LawfulIndexType I
inst✝¹¹ : DecidableEq I
inst✝¹⁰ : SemiInnerProductSpace K E
inst✝⁹ : (i : I) → SemiInnerProductSpace K (EI i)
inst✝⁸ : SemiInnerProductSpaceStruct K E I EI
F : Type ?u.116767
J : Type ?u.116770
FJ : J → Type ?u.116775
inst✝⁷ : StructType F J FJ
inst✝⁶ : IndexType J
inst✝⁵ : LawfulIndexType J
inst✝⁴ : DecidableEq J
inst✝³ : SemiInnerProductSpace K F
inst✝² : (j : J) → SemiInnerProductSpace K (FJ j)
inst✝¹ : SemiInnerProductSpaceStruct K F J FJ
inst✝ : DecidableEq I
i : ι
x : ι → E
j : I
de : EI j
⊢ (fun i' => if h : j = i' then h ▸ de else 0) = fun i_1 => if h : j = i_1 then ⋯ ▸ de else 0

State before:
case e_f
K : Type u_5
I : Type u_1
inst✝²⁵ : RCLike K
X : Type ?u.116532
inst✝²⁴ : SemiInnerProductSpace K X
Y : Type ?u.116545
inst✝²³ : SemiInnerProductSpace K Y
Z : Type ?u.116556
inst✝²² : SemiInnerProductSpace K Z
W : Type ?u.116567
inst✝²¹ : SemiInnerProductSpace K W
ι : Type u_2
inst✝²⁰ : IndexType ι
inst✝¹⁹ : LawfulIndexType ι
inst✝¹⁸ : DecidableEq ι
κ : Type ?u.116603
inst✝¹⁷ : IndexType κ
inst✝¹⁶ : LawfulIndexType κ
inst✝¹⁵ : DecidableEq κ
E : Type u_3
EI : I → Type u_4
inst✝¹⁴ : StructType E I EI
inst✝¹³ : IndexType I
inst✝¹² : LawfulIndexType I
inst✝¹¹ : DecidableEq I
inst✝¹⁰ : SemiInnerProductSpace K E
inst✝⁹ : (i : I) → SemiInnerProductSpace K (EI i)
inst✝⁸ : SemiInnerProductSpaceStruct K E I EI
F : Type ?u.116767
J : Type ?u.116770
FJ : J → Type ?u.116775
inst✝⁷ : StructType F J FJ
inst✝⁶ : IndexType J
inst✝⁵ : LawfulIndexType J
inst✝⁴ : DecidableEq J
inst✝³ : SemiInnerProductSpace K F
inst✝² : (j : J) → SemiInnerProductSpace K (FJ j)
inst✝¹ : SemiInnerProductSpaceStruct K F J FJ
inst✝ : DecidableEq I
i : ι
x : ι → E
j : I
de : EI j
⊢ (fun i' => if h : j = i' then h ▸ de else 0) = fun i_1 => if h : j = i_1 then ⋯ ▸ de else 0
Tactic:
funext j'
State after:
case e_f.h
K : Type u_5
I : Type u_1
inst✝²⁵ : RCLike K
X : Type ?u.116532
inst✝²⁴ : SemiInnerProductSpace K X
Y : Type ?u.116545
inst✝²³ : SemiInnerProductSpace K Y
Z : Type ?u.116556
inst✝²² : SemiInnerProductSpace K Z
W : Type ?u.116567
inst✝²¹ : SemiInnerProductSpace K W
ι : Type u_2
inst✝²⁰ : IndexType ι
inst✝¹⁹ : LawfulIndexType ι
inst✝¹⁸ : DecidableEq ι
κ : Type ?u.116603
inst✝¹⁷ : IndexType κ
inst✝¹⁶ : LawfulIndexType κ
inst✝¹⁵ : DecidableEq κ
E : Type u_3
EI : I → Type u_4
inst✝¹⁴ : StructType E I EI
inst✝¹³ : IndexType I
inst✝¹² : LawfulIndexType I
inst✝¹¹ : DecidableEq I
inst✝¹⁰ : SemiInnerProductSpace K E
inst✝⁹ : (i : I) → SemiInnerProductSpace K (EI i)
inst✝⁸ : SemiInnerProductSpaceStruct K E I EI
F : Type ?u.116767
J : Type ?u.116770
FJ : J → Type ?u.116775
inst✝⁷ : StructType F J FJ
inst✝⁶ : IndexType J
inst✝⁵ : LawfulIndexType J
inst✝⁴ : DecidableEq J
inst✝³ : SemiInnerProductSpace K F
inst✝² : (j : J) → SemiInnerProductSpace K (FJ j)
inst✝¹ : SemiInnerProductSpaceStruct K F J FJ
inst✝ : DecidableEq I
i : ι
x : ι → E
j : I
de : EI j
j' : I
⊢ (if h : j = j' then h ▸ de else 0) = if h : j = j' then ⋯ ▸ de else 0

State before:
case e_f.h
K : Type u_5
I : Type u_1
inst✝²⁵ : RCLike K
X : Type ?u.116532
inst✝²⁴ : SemiInnerProductSpace K X
Y : Type ?u.116545
inst✝²³ : SemiInnerProductSpace K Y
Z : Type ?u.116556
inst✝²² : SemiInnerProductSpace K Z
W : Type ?u.116567
inst✝²¹ : SemiInnerProductSpace K W
ι : Type u_2
inst✝²⁰ : IndexType ι
inst✝¹⁹ : LawfulIndexType ι
inst✝¹⁸ : DecidableEq ι
κ : Type ?u.116603
inst✝¹⁷ : IndexType κ
inst✝¹⁶ : LawfulIndexType κ
inst✝¹⁵ : DecidableEq κ
E : Type u_3
EI : I → Type u_4
inst✝¹⁴ : StructType E I EI
inst✝¹³ : IndexType I
inst✝¹² : LawfulIndexType I
inst✝¹¹ : DecidableEq I
inst✝¹⁰ : SemiInnerProductSpace K E
inst✝⁹ : (i : I) → SemiInnerProductSpace K (EI i)
inst✝⁸ : SemiInnerProductSpaceStruct K E I EI
F : Type ?u.116767
J : Type ?u.116770
FJ : J → Type ?u.116775
inst✝⁷ : StructType F J FJ
inst✝⁶ : IndexType J
inst✝⁵ : LawfulIndexType J
inst✝⁴ : DecidableEq J
inst✝³ : SemiInnerProductSpace K F
inst✝² : (j : J) → SemiInnerProductSpace K (FJ j)
inst✝¹ : SemiInnerProductSpaceStruct K F J FJ
inst✝ : DecidableEq I
i : ι
x : ι → E
j : I
de : EI j
j' : I
⊢ (if h : j = j' then h ▸ de else 0) = if h : j = j' then ⋯ ▸ de else 0
Tactic:
if h':j=j' then
  subst h'
  simp
else
  simp[h']
State after:
no goals

State before:
K : Type u_5
I : Type u_1
inst✝²⁵ : RCLike K
X : Type ?u.116532
inst✝²⁴ : SemiInnerProductSpace K X
Y : Type ?u.116545
inst✝²³ : SemiInnerProductSpace K Y
Z : Type ?u.116556
inst✝²² : SemiInnerProductSpace K Z
W : Type ?u.116567
inst✝²¹ : SemiInnerProductSpace K W
ι : Type u_2
inst✝²⁰ : IndexType ι
inst✝¹⁹ : LawfulIndexType ι
inst✝¹⁸ : DecidableEq ι
κ : Type ?u.116603
inst✝¹⁷ : IndexType κ
inst✝¹⁶ : LawfulIndexType κ
inst✝¹⁵ : DecidableEq κ
E : Type u_3
EI : I → Type u_4
inst✝¹⁴ : StructType E I EI
inst✝¹³ : IndexType I
inst✝¹² : LawfulIndexType I
inst✝¹¹ : DecidableEq I
inst✝¹⁰ : SemiInnerProductSpace K E
inst✝⁹ : (i : I) → SemiInnerProductSpace K (EI i)
inst✝⁸ : SemiInnerProductSpaceStruct K E I EI
F : Type ?u.116767
J : Type ?u.116770
FJ : J → Type ?u.116775
inst✝⁷ : StructType F J FJ
inst✝⁶ : IndexType J
inst✝⁵ : LawfulIndexType J
inst✝⁴ : DecidableEq J
inst✝³ : SemiInnerProductSpace K F
inst✝² : (j : J) → SemiInnerProductSpace K (FJ j)
inst✝¹ : SemiInnerProductSpaceStruct K F J FJ
inst✝ : DecidableEq I
i : ι
x : ι → E
j : I
de : EI j
j' : I
h' : j = j'
⊢ (if h : j = j' then h ▸ de else 0) = if h : j = j' then ⋯ ▸ de else 0
Tactic:
subst h'
State after:
K : Type u_5
I : Type u_1
inst✝²⁵ : RCLike K
X : Type ?u.116532
inst✝²⁴ : SemiInnerProductSpace K X
Y : Type ?u.116545
inst✝²³ : SemiInnerProductSpace K Y
Z : Type ?u.116556
inst✝²² : SemiInnerProductSpace K Z
W : Type ?u.116567
inst✝²¹ : SemiInnerProductSpace K W
ι : Type u_2
inst✝²⁰ : IndexType ι
inst✝¹⁹ : LawfulIndexType ι
inst✝¹⁸ : DecidableEq ι
κ : Type ?u.116603
inst✝¹⁷ : IndexType κ
inst✝¹⁶ : LawfulIndexType κ
inst✝¹⁵ : DecidableEq κ
E : Type u_3
EI : I → Type u_4
inst✝¹⁴ : StructType E I EI
inst✝¹³ : IndexType I
inst✝¹² : LawfulIndexType I
inst✝¹¹ : DecidableEq I
inst✝¹⁰ : SemiInnerProductSpace K E
inst✝⁹ : (i : I) → SemiInnerProductSpace K (EI i)
inst✝⁸ : SemiInnerProductSpaceStruct K E I EI
F : Type ?u.116767
J : Type ?u.116770
FJ : J → Type ?u.116775
inst✝⁷ : StructType F J FJ
inst✝⁶ : IndexType J
inst✝⁵ : LawfulIndexType J
inst✝⁴ : DecidableEq J
inst✝³ : SemiInnerProductSpace K F
inst✝² : (j : J) → SemiInnerProductSpace K (FJ j)
inst✝¹ : SemiInnerProductSpaceStruct K F J FJ
inst✝ : DecidableEq I
i : ι
x : ι → E
j : I
de : EI j
⊢ (if h : j = j then h ▸ de else 0) = if h : j = j then ⋯ ▸ de else 0

State before:
K : Type u_5
I : Type u_1
inst✝²⁵ : RCLike K
X : Type ?u.116532
inst✝²⁴ : SemiInnerProductSpace K X
Y : Type ?u.116545
inst✝²³ : SemiInnerProductSpace K Y
Z : Type ?u.116556
inst✝²² : SemiInnerProductSpace K Z
W : Type ?u.116567
inst✝²¹ : SemiInnerProductSpace K W
ι : Type u_2
inst✝²⁰ : IndexType ι
inst✝¹⁹ : LawfulIndexType ι
inst✝¹⁸ : DecidableEq ι
κ : Type ?u.116603
inst✝¹⁷ : IndexType κ
inst✝¹⁶ : LawfulIndexType κ
inst✝¹⁵ : DecidableEq κ
E : Type u_3
EI : I → Type u_4
inst✝¹⁴ : StructType E I EI
inst✝¹³ : IndexType I
inst✝¹² : LawfulIndexType I
inst✝¹¹ : DecidableEq I
inst✝¹⁰ : SemiInnerProductSpace K E
inst✝⁹ : (i : I) → SemiInnerProductSpace K (EI i)
inst✝⁸ : SemiInnerProductSpaceStruct K E I EI
F : Type ?u.116767
J : Type ?u.116770
FJ : J → Type ?u.116775
inst✝⁷ : StructType F J FJ
inst✝⁶ : IndexType J
inst✝⁵ : LawfulIndexType J
inst✝⁴ : DecidableEq J
inst✝³ : SemiInnerProductSpace K F
inst✝² : (j : J) → SemiInnerProductSpace K (FJ j)
inst✝¹ : SemiInnerProductSpaceStruct K F J FJ
inst✝ : DecidableEq I
i : ι
x : ι → E
j : I
de : EI j
⊢ (if h : j = j then h ▸ de else 0) = if h : j = j then ⋯ ▸ de else 0
Tactic:
simp
State after:
no goals

State before:
K : Type u_5
I : Type u_1
inst✝²⁵ : RCLike K
X : Type ?u.116532
inst✝²⁴ : SemiInnerProductSpace K X
Y : Type ?u.116545
inst✝²³ : SemiInnerProductSpace K Y
Z : Type ?u.116556
inst✝²² : SemiInnerProductSpace K Z
W : Type ?u.116567
inst✝²¹ : SemiInnerProductSpace K W
ι : Type u_2
inst✝²⁰ : IndexType ι
inst✝¹⁹ : LawfulIndexType ι
inst✝¹⁸ : DecidableEq ι
κ : Type ?u.116603
inst✝¹⁷ : IndexType κ
inst✝¹⁶ : LawfulIndexType κ
inst✝¹⁵ : DecidableEq κ
E : Type u_3
EI : I → Type u_4
inst✝¹⁴ : StructType E I EI
inst✝¹³ : IndexType I
inst✝¹² : LawfulIndexType I
inst✝¹¹ : DecidableEq I
inst✝¹⁰ : SemiInnerProductSpace K E
inst✝⁹ : (i : I) → SemiInnerProductSpace K (EI i)
inst✝⁸ : SemiInnerProductSpaceStruct K E I EI
F : Type ?u.116767
J : Type ?u.116770
FJ : J → Type ?u.116775
inst✝⁷ : StructType F J FJ
inst✝⁶ : IndexType J
inst✝⁵ : LawfulIndexType J
inst✝⁴ : DecidableEq J
inst✝³ : SemiInnerProductSpace K F
inst✝² : (j : J) → SemiInnerProductSpace K (FJ j)
inst✝¹ : SemiInnerProductSpaceStruct K F J FJ
inst✝ : DecidableEq I
i : ι
x : ι → E
j : I
de : EI j
j' : I
h' : ¬j = j'
⊢ (if h : j = j' then h ▸ de else 0) = if h : j = j' then ⋯ ▸ de else 0
Tactic:
simp[h']
State after:
no goals

State before:
K : Type u_5
I : Type u_1
inst✝²⁵ : RCLike K
X : Type ?u.116532
inst✝²⁴ : SemiInnerProductSpace K X
Y : Type ?u.116545
inst✝²³ : SemiInnerProductSpace K Y
Z : Type ?u.116556
inst✝²² : SemiInnerProductSpace K Z
W : Type ?u.116567
inst✝²¹ : SemiInnerProductSpace K W
ι : Type u_2
inst✝²⁰ : IndexType ι
inst✝¹⁹ : LawfulIndexType ι
inst✝¹⁸ : DecidableEq ι
κ : Type ?u.116603
inst✝¹⁷ : IndexType κ
inst✝¹⁶ : LawfulIndexType κ
inst✝¹⁵ : DecidableEq κ
E : Type u_3
EI : I → Type u_4
inst✝¹⁴ : StructType E I EI
inst✝¹³ : IndexType I
inst✝¹² : LawfulIndexType I
inst✝¹¹ : DecidableEq I
inst✝¹⁰ : SemiInnerProductSpace K E
inst✝⁹ : (i : I) → SemiInnerProductSpace K (EI i)
inst✝⁸ : SemiInnerProductSpaceStruct K E I EI
F : Type ?u.116767
J : Type ?u.116770
FJ : J → Type ?u.116775
inst✝⁷ : StructType F J FJ
inst✝⁶ : IndexType J
inst✝⁵ : LawfulIndexType J
inst✝⁴ : DecidableEq J
inst✝³ : SemiInnerProductSpace K F
inst✝² : (j : J) → SemiInnerProductSpace K (FJ j)
inst✝¹ : SemiInnerProductSpaceStruct K F J FJ
inst✝ : DecidableEq I
i : ι
x : ι → E
j : I
de : EI j
i' : ι
h : ¬i = i'
⊢ (if i = i' then structMake fun i' => if h : j = i' then h ▸ de else 0 else 0) =
    structMake fun i_1 => if h : i = i' ∧ j = i_1 then ⋯ ▸ de else 0
Tactic:
simp[h]
State after:
no goals