-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Basic.lean
theorem mem_of_elem_eq_true [BEq α] [LawfulBEq α] {a : α} {as : List α} : elem a as = true → a ∈ as

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
as : List α
⊢ elem a nil = true → a ∈ nil

Tactic:
simp [elem]

Result:
no goals

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
as✝ : List α
a' : α
as : List α
x✝ : Bool
heq✝ : (a == a') = false
⊢ elem a as = true → a ∈ a' :: as

Tactic:
intro h

Result:
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
as✝ : List α
a' : α
as : List α
x✝ : Bool
heq✝ : (a == a') = false
h : elem a as = true
⊢ a ∈ a' :: as

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
as✝ : List α
a' : α
as : List α
x✝ : Bool
heq✝ : (a == a') = false
h : elem a as = true
⊢ a ∈ a' :: as

Tactic:
exact Mem.tail _ (mem_of_elem_eq_true h)

Result:
no goals

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
as✝ : List α
a' : α
as : List α
x✝ : Bool
a✝ : true = true
h : a = a'
⊢ a ∈ a' :: as

Tactic:
subst h

Result:
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
as✝ as : List α
x✝ : Bool
a✝ : true = true
⊢ a ∈ a :: as

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
as✝ : List α
a' : α
as : List α
x✝ : Bool
h : (a == a') = true
⊢ true = true → a ∈ a' :: as

Tactic:
intros

Result:
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
as✝ : List α
a' : α
as : List α
x✝ : Bool
h : (a == a') = true
a✝ : true = true
⊢ a ∈ a' :: as

Proof state:
case h_2
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
as✝ : List α
a' : α
as : List α
x✝ : Bool
heq✝ : (a == a') = false
⊢ elem a as = true → a ∈ a' :: as

Tactic:
next _ => intro h; exact Mem.tail _ (mem_of_elem_eq_true h)

Result:
no goals

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
as✝ : List α
a' : α
as : List α
⊢ (match a == a' with
      | true => true
      | false => elem a as) =
      true →
    a ∈ a' :: as

Tactic:
split

Result:
case h_1
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
as✝ : List α
a' : α
as : List α
x✝ : Bool
heq✝ : (a == a') = true
⊢ true = true → a ∈ a' :: as

case h_2
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
as✝ : List α
a' : α
as : List α
x✝ : Bool
heq✝ : (a == a') = false
⊢ elem a as = true → a ∈ a' :: as

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
as✝ : List α
a' : α
as : List α
⊢ elem a (a' :: as) = true → a ∈ a' :: as

Tactic:
simp [elem]

Result:
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
as✝ : List α
a' : α
as : List α
⊢ (match a == a' with
      | true => true
      | false => elem a as) =
      true →
    a ∈ a' :: as

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
as✝ as : List α
x✝ : Bool
a✝ : true = true
⊢ a ∈ a :: as

Tactic:
apply Mem.head

Result:
no goals

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
as✝ : List α
a' : α
as : List α
x✝ : Bool
h : (a == a') = true
a✝ : true = true
⊢ a ∈ a' :: as

Tactic:
simp [BEq.beq] at h

Result:
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
as✝ : List α
a' : α
as : List α
x✝ : Bool
a✝ : true = true
h : a = a'
⊢ a ∈ a' :: as

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
as : List α
⊢ elem a as = true → a ∈ as

Tactic:
match as with
| [] => simp [elem]
| a'::as =>
  simp [elem]
  split
  next h => intros; simp [BEq.beq] at h; subst h; apply Mem.head
  next _ => intro h; exact Mem.tail _ (mem_of_elem_eq_true h)

Result:
no goals

Proof state:
case h_1
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
as✝ : List α
a' : α
as : List α
x✝ : Bool
heq✝ : (a == a') = true
⊢ true = true → a ∈ a' :: as

case h_2
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
as✝ : List α
a' : α
as : List α
x✝ : Bool
heq✝ : (a == a') = false
⊢ elem a as = true → a ∈ a' :: as

Tactic:
next h => intros; simp [BEq.beq] at h; subst h; apply Mem.head

Result:
case h_2
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
as✝ : List α
a' : α
as : List α
x✝ : Bool
heq✝ : (a == a') = false
⊢ elem a as = true → a ∈ a' :: as