no goals
α : Type u
β : Type v
γ : Type w
a : α
as as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
x✝ : ℕ
h1 : x✝ < length []
⊢ get x✝ [] ∈ []
cases h1
α : Type u
β : Type v
γ : Type w
a✝ : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a : α
as : List α
x✝ : 0 < length (a :: as)
⊢ get 0 (a :: as) = a ∨ get 0 (a :: as) ∈ as
α : Type u
β : Type v
γ : Type w
a✝ : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a : α
as : List α
x✝ : 0 < length (a :: as)
⊢ get 0 (a :: as) ∈ a :: as
rw [mem_cons]
no goals
α : Type u
β : Type v
γ : Type w
a✝ : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a : α
as : List α
x✝ : 0 < length (a :: as)
⊢ get 0 (a :: as) = a ∨ get 0 (a :: as) ∈ as
exact Or.inl rfl
α : Type u
β : Type v
γ : Type w
a✝ : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
n : ℕ
a : α
as : List α
h1 : n + 1 < length (a :: as)
⊢ get (n + 1) (a :: as) = a ∨ get (n + 1) (a :: as) ∈ as
α : Type u
β : Type v
γ : Type w
a✝ : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
n : ℕ
a : α
as : List α
h1 : n + 1 < length (a :: as)
⊢ get (n + 1) (a :: as) ∈ a :: as
rw [mem_cons]
case h
α : Type u
β : Type v
γ : Type w
a✝ : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
n : ℕ
a : α
as : List α
h1 : n + 1 < length (a :: as)
⊢ get (n + 1) (a :: as) ∈ as
α : Type u
β : Type v
γ : Type w
a✝ : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
n : ℕ
a : α
as : List α
h1 : n + 1 < length (a :: as)
⊢ get (n + 1) (a :: as) = a ∨ get (n + 1) (a :: as) ∈ as
apply Or.inr
case h
α : Type u
β : Type v
γ : Type w
a✝ : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
n : ℕ
a : α
as : List α
h1 : n + 1 < length (a :: as)
⊢ get (Nat.add n 0) as ∈ as
case h
α : Type u
β : Type v
γ : Type w
a✝ : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
n : ℕ
a : α
as : List α
h1 : n + 1 < length (a :: as)
⊢ get (n + 1) (a :: as) ∈ as
unfold get
case h.a
α : Type u
β : Type v
γ : Type w
a✝ : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
n : ℕ
a : α
as : List α
h1 : n + 1 < length (a :: as)
⊢ Nat.add n 0 < length as
case h
α : Type u
β : Type v
γ : Type w
a✝ : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
n : ℕ
a : α
as : List α
h1 : n + 1 < length (a :: as)
⊢ get (Nat.add n 0) as ∈ as
apply mem_get_of_le
no goals
case h.a
α : Type u
β : Type v
γ : Type w
a✝ : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
n : ℕ
a : α
as : List α
h1 : n + 1 < length (a :: as)
⊢ Nat.add n 0 < length as
apply Nat.lt_of_succ_lt_succ h1