no goals
α : Type u
β : Type v
γ : Type w
a : α
as as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
f : α → β
x✝ : ℕ
h : x✝ < length []
⊢ get x✝ (map f []) = f (get x✝ [])
cases h
α : Type u
β : Type v
γ : Type w
a : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
f : α → β
n : ℕ
head✝ : α
as : List α
h1 : n + 1 < length (head✝ :: as)
h2 : n < length as
⊢ get (n + 1) (map f (head✝ :: as)) = f (get (n + 1) (head✝ :: as))
α : Type u
β : Type v
γ : Type w
a : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
f : α → β
n : ℕ
head✝ : α
as : List α
h1 : n + 1 < length (head✝ :: as)
⊢ get (n + 1) (map f (head✝ :: as)) = f (get (n + 1) (head✝ :: as))
have h2 : n < length as := by
  rw [← Nat.succ_le_iff, ← Nat.lt_succ_iff]
  apply h1
no goals
α : Type u
β : Type v
γ : Type w
a : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
f : α → β
n : ℕ
head✝ : α
as : List α
h1 : n + 1 < length (head✝ :: as)
h2 : n < length as
⊢ get (n + 1) (map f (head✝ :: as)) = f (get (n + 1) (head✝ :: as))
apply get_map h2
α : Type u
β : Type v
γ : Type w
a : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
f : α → β
n : ℕ
head✝ : α
as : List α
h1 : n + 1 < length (head✝ :: as)
⊢ Nat.succ n < Nat.succ (length as)
α : Type u
β : Type v
γ : Type w
a : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
f : α → β
n : ℕ
head✝ : α
as : List α
h1 : n + 1 < length (head✝ :: as)
⊢ n < length as
rw [← Nat.succ_le_iff, ← Nat.lt_succ_iff]
no goals
α : Type u
β : Type v
γ : Type w
a : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
f : α → β
n : ℕ
head✝ : α
as : List α
h1 : n + 1 < length (head✝ :: as)
⊢ Nat.succ n < Nat.succ (length as)
apply h1