no goals
α : Type u_1
inst✝ : DecidableEq α
a b : α
l : List α
⊢ a ∈ List.insert b l ↔ a = b ∨ a ∈ l
if h : b ∈ l then
  rw [insert_of_mem h]
  constructor; {apply Or.inr}
  intro
  | Or.inl h' => rw [h']; exact h
  | Or.inr h' => exact h'
else rw [insert_of_not_mem h, mem_cons]
α : Type u_1
inst✝ : DecidableEq α
a b : α
l : List α
h : b ∈ l
⊢ a ∈ l ↔ a = b ∨ a ∈ l
α : Type u_1
inst✝ : DecidableEq α
a b : α
l : List α
h : b ∈ l
⊢ a ∈ List.insert b l ↔ a = b ∨ a ∈ l
rw [insert_of_mem h]
case mp
α : Type u_1
inst✝ : DecidableEq α
a b : α
l : List α
h : b ∈ l
⊢ a ∈ l → a = b ∨ a ∈ l

case mpr
α : Type u_1
inst✝ : DecidableEq α
a b : α
l : List α
h : b ∈ l
⊢ a = b ∨ a ∈ l → a ∈ l
α : Type u_1
inst✝ : DecidableEq α
a b : α
l : List α
h : b ∈ l
⊢ a ∈ l ↔ a = b ∨ a ∈ l
constructor
case mpr
α : Type u_1
inst✝ : DecidableEq α
a b : α
l : List α
h : b ∈ l
⊢ a = b ∨ a ∈ l → a ∈ l
case mp
α : Type u_1
inst✝ : DecidableEq α
a b : α
l : List α
h : b ∈ l
⊢ a ∈ l → a = b ∨ a ∈ l

case mpr
α : Type u_1
inst✝ : DecidableEq α
a b : α
l : List α
h : b ∈ l
⊢ a = b ∨ a ∈ l → a ∈ l
{apply Or.inr}
no goals
case mpr
α : Type u_1
inst✝ : DecidableEq α
a b : α
l : List α
h : b ∈ l
⊢ a = b ∨ a ∈ l → a ∈ l
intro
| Or.inl h' => rw [h']; exact h
| Or.inr h' => exact h'
α : Type u_1
inst✝ : DecidableEq α
a b : α
l : List α
h : b ∈ l
x✝ : a = b ∨ a ∈ l
h' : a = b
⊢ b ∈ l
α : Type u_1
inst✝ : DecidableEq α
a b : α
l : List α
h : b ∈ l
x✝ : a = b ∨ a ∈ l
h' : a = b
⊢ a ∈ l
rw [h']
no goals
α : Type u_1
inst✝ : DecidableEq α
a b : α
l : List α
h : b ∈ l
x✝ : a = b ∨ a ∈ l
h' : a = b
⊢ b ∈ l
exact h
no goals
α : Type u_1
inst✝ : DecidableEq α
a b : α
l : List α
h : b ∈ l
x✝ : a = b ∨ a ∈ l
h' : a ∈ l
⊢ a ∈ l
exact h'
no goals
α : Type u_1
inst✝ : DecidableEq α
a b : α
l : List α
h : ¬b ∈ l
⊢ a ∈ List.insert b l ↔ a = b ∨ a ∈ l
rw [insert_of_not_mem h, mem_cons]