case h
n m n' : ℕ
h : n + 1 = n' + 1
i : Fin n
⊢ ↑(↑(cast h) (↑castSucc i)) = ↑(↑castSucc (↑(cast (_ : n = n')) i))
n m n' : ℕ
h : n + 1 = n' + 1
i : Fin n
⊢ ↑(cast h) (↑castSucc i) = ↑castSucc (↑(cast (_ : n = n')) i)
ext
no goals
case h
n m n' : ℕ
h : n + 1 = n' + 1
i : Fin n
⊢ ↑(↑(cast h) (↑castSucc i)) = ↑(↑castSucc (↑(cast (_ : n = n')) i))
simp only [coe_cast, coe_castSucc]