Theorem: SciLean.StructType.structProj_oneHot' (SciLean/Data/StructType/Basic.lean)

State before:
X : Sort u_3
I : Sort u_1
XI : I → Type u_2
inst✝² : StructType X I XI
inst✝¹ : DecidableEq I
inst✝ : (i : I) → Zero (XI i)
i j : I
xi : XI i
h : i ≠ j
⊢ structProj (oneHot i xi) j = 0
Tactic:
simp[oneHot]
State after:
X : Sort u_3
I : Sort u_1
XI : I → Type u_2
inst✝² : StructType X I XI
inst✝¹ : DecidableEq I
inst✝ : (i : I) → Zero (XI i)
i j : I
xi : XI i
h : i ≠ j
⊢ ∀ (h : i = j), h ▸ xi = 0

State before:
X : Sort u_3
I : Sort u_1
XI : I → Type u_2
inst✝² : StructType X I XI
inst✝¹ : DecidableEq I
inst✝ : (i : I) → Zero (XI i)
i j : I
xi : XI i
h : i ≠ j
⊢ ∀ (h : i = j), h ▸ xi = 0
Tactic:
if h':i=j then simp [h'] at h else simp[h']
State after:
no goals

State before:
X : Sort u_3
I : Sort u_1
XI : I → Type u_2
inst✝² : StructType X I XI
inst✝¹ : DecidableEq I
inst✝ : (i : I) → Zero (XI i)
i j : I
xi : XI i
h : i ≠ j
h' : i = j
⊢ ∀ (h : i = j), h ▸ xi = 0
Tactic:
simp [h'] at h
State after:
no goals

State before:
X : Sort u_3
I : Sort u_1
XI : I → Type u_2
inst✝² : StructType X I XI
inst✝¹ : DecidableEq I
inst✝ : (i : I) → Zero (XI i)
i j : I
xi : XI i
h : i ≠ j
h' : ¬i = j
⊢ ∀ (h : i = j), h ▸ xi = 0
Tactic:
simp[h']
State after:
no goals