Theorem: List.mem_singleton_iff (Table/BuiltinExtensions.lean)

State before:
α : Type u_1
x y : α
⊢ x ∈ [y] ↔ x = y
Tactic:
apply Iff.intro
State after:
case mp
α : Type u_1
x y : α
⊢ x ∈ [y] → x = y

case mpr
α : Type u_1
x y : α
⊢ x = y → x ∈ [y]

State before:
case mp
α : Type u_1
x y : α
⊢ x ∈ [y] → x = y

case mpr
α : Type u_1
x y : α
⊢ x = y → x ∈ [y]
Tactic:
. intro hmem
  cases hmem
  . rfl
  . contradiction
State after:
case mpr
α : Type u_1
x y : α
⊢ x = y → x ∈ [y]

State before:
case mpr
α : Type u_1
x y : α
⊢ x = y → x ∈ [y]
Tactic:
. intro heq
  rw [heq]
  constructor
State after:
no goals

State before:
case mp
α : Type u_1
x y : α
⊢ x ∈ [y] → x = y
Tactic:
intro hmem
State after:
case mp
α : Type u_1
x y : α
hmem : x ∈ [y]
⊢ x = y

State before:
case mp
α : Type u_1
x y : α
hmem : x ∈ [y]
⊢ x = y
Tactic:
cases hmem
State after:
case mp.head
α : Type u_1
x : α
⊢ x = x

case mp.tail
α : Type u_1
x y : α
a✝ : Mem x []
⊢ x = y

State before:
case mp.head
α : Type u_1
x : α
⊢ x = x

case mp.tail
α : Type u_1
x y : α
a✝ : Mem x []
⊢ x = y
Tactic:
. rfl
State after:
case mp.tail
α : Type u_1
x y : α
a✝ : Mem x []
⊢ x = y

State before:
case mp.tail
α : Type u_1
x y : α
a✝ : Mem x []
⊢ x = y
Tactic:
. contradiction
State after:
no goals

State before:
case mp.head
α : Type u_1
x : α
⊢ x = x
Tactic:
rfl
State after:
no goals

State before:
case mp.tail
α : Type u_1
x y : α
a✝ : Mem x []
⊢ x = y
Tactic:
contradiction
State after:
no goals

State before:
case mpr
α : Type u_1
x y : α
⊢ x = y → x ∈ [y]
Tactic:
intro heq
State after:
case mpr
α : Type u_1
x y : α
heq : x = y
⊢ x ∈ [y]

State before:
case mpr
α : Type u_1
x y : α
heq : x = y
⊢ x ∈ [y]
Tactic:
rw [heq]
State after:
case mpr
α : Type u_1
x y : α
heq : x = y
⊢ y ∈ [y]

State before:
case mpr
α : Type u_1
x y : α
heq : x = y
⊢ y ∈ [y]
Tactic:
constructor
State after:
no goals