no goals
ι : Type ?u.488600
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ L : List α
i : Fin (length (attach L))
⊢ ↑i < length (map Subtype.val (attach L))
simpa using i.2
no goals
ι : Type ?u.488600
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ L : List α
i : Fin (length (attach L))
⊢ ↑(get (attach L) i) =
    get (map Subtype.val (attach L)) { val := ↑i, isLt := (_ : ↑i < length (map Subtype.val (attach L))) }
rw [get_map]
no goals
ι : Type ?u.488600
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ L : List α
i : Fin (length (attach L))
⊢ get (map Subtype.val (attach L)) { val := ↑i, isLt := (_ : ↑i < length (map Subtype.val (attach L))) } =
    get L { val := ↑i, isLt := (_ : ↑i < length L) }
congr 2 <;> simp