case h
α : Type u
m n o : ℕ
m' : Type ?u.75560
n' : Type ?u.75563
o' : Type ?u.75566
inst✝ : Zero α
i : Fin (Nat.succ n)
⊢ vecCons 0 0 i = OfNat.ofNat 0 i
α : Type u
m n o : ℕ
m' : Type ?u.75560
n' : Type ?u.75563
o' : Type ?u.75566
inst✝ : Zero α
⊢ vecCons 0 0 = 0
ext i
case h.refine'_1
α : Type u
m n o : ℕ
m' : Type ?u.75560
n' : Type ?u.75563
o' : Type ?u.75566
inst✝ : Zero α
i : Fin (Nat.succ n)
⊢ vecCons 0 0 0 = OfNat.ofNat 0 0

case h.refine'_2
α : Type u
m n o : ℕ
m' : Type ?u.75560
n' : Type ?u.75563
o' : Type ?u.75566
inst✝ : Zero α
i : Fin (Nat.succ n)
⊢ ∀ (i : Fin n), vecCons 0 0 (Fin.succ i) = OfNat.ofNat 0 (Fin.succ i)
case h
α : Type u
m n o : ℕ
m' : Type ?u.75560
n' : Type ?u.75563
o' : Type ?u.75566
inst✝ : Zero α
i : Fin (Nat.succ n)
⊢ vecCons 0 0 i = OfNat.ofNat 0 i
refine' Fin.cases _ _ i
no goals
case h.refine'_2
α : Type u
m n o : ℕ
m' : Type ?u.75560
n' : Type ?u.75563
o' : Type ?u.75566
inst✝ : Zero α
i : Fin (Nat.succ n)
⊢ ∀ (i : Fin n), vecCons 0 0 (Fin.succ i) = OfNat.ofNat 0 (Fin.succ i)
simp
no goals
case h.refine'_1
α : Type u
m n o : ℕ
m' : Type ?u.75560
n' : Type ?u.75563
o' : Type ?u.75566
inst✝ : Zero α
i : Fin (Nat.succ n)
⊢ vecCons 0 0 0 = OfNat.ofNat 0 0
rfl