no goals
α : Type u
β : Type v
γ : Type w
a✝ : α
as as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a : α
h : a ∈ []
⊢ ∃ n, a = get n []
cases h
α : Type u
β : Type v
γ : Type w
a✝ : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a b : α
as : List α
h : a = b ∨ a ∈ as
⊢ ∃ n, a = get n (b :: as)
α : Type u
β : Type v
γ : Type w
a✝ : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a b : α
as : List α
h : a ∈ b :: as
⊢ ∃ n, a = get n (b :: as)
rw [mem_cons] at h
no goals
α : Type u
β : Type v
γ : Type w
a✝ : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a b : α
as : List α
h : a = b ∨ a ∈ as
⊢ ∃ n, a = get n (b :: as)
cases h with
| inl h => exact ⟨0, h⟩
| inr h =>
  rcases eq_get_of_mem h with ⟨n, h⟩
  exact ⟨n + 1, h⟩
no goals
case inl
α : Type u
β : Type v
γ : Type w
a✝ : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a b : α
as : List α
h : a = b
⊢ ∃ n, a = get n (b :: as)
exact ⟨0, h⟩
case inr.intro
α : Type u
β : Type v
γ : Type w
a✝ : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a b : α
as : List α
h✝ : a ∈ as
n : ℕ
h : a = get n as
⊢ ∃ n, a = get n (b :: as)
case inr
α : Type u
β : Type v
γ : Type w
a✝ : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a b : α
as : List α
h : a ∈ as
⊢ ∃ n, a = get n (b :: as)
rcases eq_get_of_mem h with ⟨n, h⟩
no goals
case inr.intro
α : Type u
β : Type v
γ : Type w
a✝ : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a b : α
as : List α
h✝ : a ∈ as
n : ℕ
h : a = get n as
⊢ ∃ n, a = get n (b :: as)
exact ⟨n + 1, h⟩