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

State before:
α : Type u_1
inst✝ : Inhabited α
N : ℕ
hN : 0 < N
a : ℕ → α
ha : Function.Periodic a N
n : ℕ
⊢ NatSeq_ofList (List_ofNatSeq a N) n = a n
Tactic:
replace hN := List.length_pos.mp <| hN.trans_eq (List_ofNatSeq_length a N).symm
State after:
α : Type u_1
inst✝ : Inhabited α
N : ℕ
a : ℕ → α
ha : Function.Periodic a N
n : ℕ
hN : List_ofNatSeq a N ≠ []
⊢ NatSeq_ofList (List_ofNatSeq a N) n = a n

State before:
α : Type u_1
inst✝ : Inhabited α
N : ℕ
a : ℕ → α
ha : Function.Periodic a N
n : ℕ
hN : List_ofNatSeq a N ≠ []
⊢ NatSeq_ofList (List_ofNatSeq a N) n = a n
Tactic:
rw [NatSeq_nonempty_eq_get hN]
State after:
α : Type u_1
inst✝ : Inhabited α
N : ℕ
a : ℕ → α
ha : Function.Periodic a N
n : ℕ
hN : List_ofNatSeq a N ≠ []
⊢ (List_ofNatSeq a N).get ⟨n % (List_ofNatSeq a N).length, ⋯⟩ = a n

State before:
α : Type u_1
inst✝ : Inhabited α
N : ℕ
a : ℕ → α
ha : Function.Periodic a N
n : ℕ
hN : List_ofNatSeq a N ≠ []
⊢ (List_ofNatSeq a N).get ⟨n % (List_ofNatSeq a N).length, ⋯⟩ = a n
Tactic:
unfold List_ofNatSeq
State after:
α : Type u_1
inst✝ : Inhabited α
N : ℕ
a : ℕ → α
ha : Function.Periodic a N
n : ℕ
hN : List_ofNatSeq a N ≠ []
⊢ (List.map a (List.range N)).get ⟨n % (List.map a (List.range N)).length, ⋯⟩ = a n

State before:
α : Type u_1
inst✝ : Inhabited α
N : ℕ
a : ℕ → α
ha : Function.Periodic a N
n : ℕ
hN : List_ofNatSeq a N ≠ []
⊢ (List.map a (List.range N)).get ⟨n % (List.map a (List.range N)).length, ⋯⟩ = a n
Tactic:
rw [List.get_map, List.get_range, Fin.val_mk,
  List.length_map, List.length_range, ha.map_mod_nat]
State after:
no goals