case refl
α : Type ?u.10869
β : Type ?u.10872
γ : Type ?u.10875
n : ℕ
h : Fin n = Fin n
⊢ _root_.cast h = ↑(cast (_ : n = n))
α : Type ?u.10869
β : Type ?u.10872
γ : Type ?u.10875
n m : ℕ
h : Fin n = Fin m
⊢ _root_.cast h = ↑(cast (_ : n = m))
cases fin_injective h
no goals
case refl
α : Type ?u.10869
β : Type ?u.10872
γ : Type ?u.10875
n : ℕ
h : Fin n = Fin n
⊢ _root_.cast h = ↑(cast (_ : n = n))
rfl