case h
n✝ m✝ m n : ℕ
h : m = n
h' : m ≤ n
x✝ : Fin m
⊢ ↑(↑(castLE h') x✝) = ↑(↑(cast h) x✝)
n✝ m✝ m n : ℕ
h : m = n
h' : m ≤ n
x✝ : Fin m
⊢ ↑(castLE h') x✝ = ↑(cast h) x✝
ext
no goals
case h
n✝ m✝ m n : ℕ
h : m = n
h' : m ≤ n
x✝ : Fin m
⊢ ↑(↑(castLE h') x✝) = ↑(↑(cast h) x✝)
simp