Theorem: LeanColls.IndexType.get_toList_univ (LeanColls/Classes/IndexType/Basic.lean)

State before:
ι : Type ?u.1822
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
α : Type ?u.1841
inst✝¹ : IndexType α
inst✝ : LawfulIndexType α
i : Fin (toList (univ α)).length
⊢ (toList (univ α)).length = card α
Tactic:
simp
State after:
no goals

State before:
ι : Type ?u.1822
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
α : Type u_1
inst✝¹ : IndexType α
inst✝ : LawfulIndexType α
i : Fin (toList (univ α)).length
⊢ (toList (univ α)).get i = fromFin (Fin.cast ⋯ i)
Tactic:
suffices ∀ L i (hL : L = toList (univ α)), List.get L i = fromFin (i.cast (by simp [hL]))
  from this _ _ rfl
State after:
ι : Type ?u.1822
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
α : Type u_1
inst✝¹ : IndexType α
inst✝ : LawfulIndexType α
i : Fin (toList (univ α)).length
⊢ ∀ (L : List α) (i : Fin L.length) (hL : L = toList (univ α)), L.get i = fromFin (Fin.cast ⋯ i)

State before:
ι : Type ?u.1822
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
α : Type u_1
inst✝¹ : IndexType α
inst✝ : LawfulIndexType α
i : Fin (toList (univ α)).length
⊢ ∀ (L : List α) (i : Fin L.length) (hL : L = toList (univ α)), L.get i = fromFin (Fin.cast ⋯ i)
Tactic:
intro L i hL
State after:
ι : Type ?u.1822
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
α : Type u_1
inst✝¹ : IndexType α
inst✝ : LawfulIndexType α
i✝ : Fin (toList (univ α)).length
L : List α
i : Fin L.length
hL : L = toList (univ α)
⊢ L.get i = fromFin (Fin.cast ⋯ i)

State before:
ι : Type ?u.1822
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
α : Type u_1
inst✝¹ : IndexType α
inst✝ : LawfulIndexType α
i✝ : Fin (toList (univ α)).length
L : List α
i : Fin L.length
hL : L = toList (univ α)
⊢ L.get i = fromFin (Fin.cast ⋯ i)
Tactic:
rw [LawfulIndexType.toList_eq_ofFn] at hL
State after:
ι : Type ?u.1822
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
α : Type u_1
inst✝¹ : IndexType α
inst✝ : LawfulIndexType α
i✝ : Fin (toList (univ α)).length
L : List α
i : Fin L.length
hL✝ : L = toList (univ α)
hL : L = List.ofFn fromFin
⊢ L.get i = fromFin (Fin.cast ⋯ i)

State before:
ι : Type ?u.1822
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
α : Type u_1
inst✝¹ : IndexType α
inst✝ : LawfulIndexType α
i✝ : Fin (toList (univ α)).length
L : List α
i : Fin L.length
hL✝ : L = toList (univ α)
hL : L = List.ofFn fromFin
⊢ L.get i = fromFin (Fin.cast ⋯ i)
Tactic:
subst hL
State after:
ι : Type ?u.1822
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
α : Type u_1
inst✝¹ : IndexType α
inst✝ : LawfulIndexType α
i✝ : Fin (toList (univ α)).length
i : Fin (List.ofFn fromFin).length
hL : List.ofFn fromFin = toList (univ α)
⊢ (List.ofFn fromFin).get i = fromFin (Fin.cast ⋯ i)

State before:
ι : Type ?u.1822
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
α : Type u_1
inst✝¹ : IndexType α
inst✝ : LawfulIndexType α
i✝ : Fin (toList (univ α)).length
i : Fin (List.ofFn fromFin).length
hL : List.ofFn fromFin = toList (univ α)
⊢ (List.ofFn fromFin).get i = fromFin (Fin.cast ⋯ i)
Tactic:
simp
State after:
no goals

State before:
ι : Type ?u.1822
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
α : Type u_1
inst✝¹ : IndexType α
inst✝ : LawfulIndexType α
i✝ : Fin (toList (univ α)).length
L : List α
i : Fin L.length
hL : L = toList (univ α)
⊢ L.length = card α
Tactic:
simp [hL]
State after:
no goals