Theorem: IMOSL.Extra.NatSeq_of_singleton (IMOSLLean4/Extra/NatSequence/OfList.lean)

State before:
α : Type u_1
inst✝ : Inhabited α
c : α
n : ℕ
⊢ NatSeq_ofList [c] n = c
Tactic:
rw [NatSeq_ofList, List.length_singleton, Nat.mod_one]
State after:
α : Type u_1
inst✝ : Inhabited α
c : α
n : ℕ
⊢ [c].getI 0 = c

State before:
α : Type u_1
inst✝ : Inhabited α
c : α
n : ℕ
⊢ [c].getI 0 = c
Tactic:
rfl
State after:
no goals