Theorem: insert_mem (Dictionary.lean)

State before:
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a : α
l : List α
⊢ x ∈ insert' a l ↔ x = a ∨ x ∈ l
Tactic:
constructor
State after:
case mp
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a : α
l : List α
⊢ x ∈ insert' a l → x = a ∨ x ∈ l

case mpr
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a : α
l : List α
⊢ x = a ∨ x ∈ l → x ∈ insert' a l

State before:
case mp
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a : α
l : List α
⊢ x ∈ insert' a l → x = a ∨ x ∈ l
Tactic:
intro hel
State after:
case mp
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a : α
l : List α
hel : x ∈ insert' a l
⊢ x = a ∨ x ∈ l

State before:
case mp
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a : α
l : List α
hel : x ∈ insert' a l
⊢ x = a ∨ x ∈ l
Tactic:
induction' l with y ys ih
State after:
case mp.nil
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a : α
hel : x ∈ insert' a []
⊢ x = a ∨ x ∈ []

case mp.cons
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x ∈ insert' a ys → x = a ∨ x ∈ ys
hel : x ∈ insert' a (y :: ys)
⊢ x = a ∨ x ∈ y :: ys

State before:
case mp.nil
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a : α
hel : x ∈ insert' a []
⊢ x = a ∨ x ∈ []
Tactic:
rw [insert', List.mem_singleton] at hel
State after:
case mp.nil
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a : α
hel : x = a
⊢ x = a ∨ x ∈ []

State before:
case mp.nil
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a : α
hel : x = a
⊢ x = a ∨ x ∈ []
Tactic:
left
State after:
case mp.nil.h
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a : α
hel : x = a
⊢ x = a

State before:
case mp.nil.h
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a : α
hel : x = a
⊢ x = a
Tactic:
exact hel
State after:
no goals

State before:
case mp.cons
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x ∈ insert' a ys → x = a ∨ x ∈ ys
hel : x ∈ insert' a (y :: ys)
⊢ x = a ∨ x ∈ y :: ys
Tactic:
rw [insert'] at hel
State after:
case mp.cons
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x ∈ insert' a ys → x = a ∨ x ∈ ys
hel : x ∈ if a ≤ y then a :: y :: ys else y :: insert' a ys
⊢ x = a ∨ x ∈ y :: ys

State before:
case mp.cons
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x ∈ insert' a ys → x = a ∨ x ∈ ys
hel : x ∈ if a ≤ y then a :: y :: ys else y :: insert' a ys
⊢ x = a ∨ x ∈ y :: ys
Tactic:
split_ifs at hel
State after:
case pos
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x ∈ insert' a ys → x = a ∨ x ∈ ys
h✝ : a ≤ y
hel : x ∈ a :: y :: ys
⊢ x = a ∨ x ∈ y :: ys

case neg
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x ∈ insert' a ys → x = a ∨ x ∈ ys
h✝ : ¬a ≤ y
hel : x ∈ y :: insert' a ys
⊢ x = a ∨ x ∈ y :: ys

State before:
case pos
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x ∈ insert' a ys → x = a ∨ x ∈ ys
h✝ : a ≤ y
hel : x ∈ a :: y :: ys
⊢ x = a ∨ x ∈ y :: ys
Tactic:
simp only [List.mem_cons] at hel
State after:
case pos
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x ∈ insert' a ys → x = a ∨ x ∈ ys
h✝ : a ≤ y
hel : x = a ∨ x = y ∨ x ∈ ys
⊢ x = a ∨ x ∈ y :: ys

State before:
case pos
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x ∈ insert' a ys → x = a ∨ x ∈ ys
h✝ : a ≤ y
hel : x = a ∨ x = y ∨ x ∈ ys
⊢ x = a ∨ x ∈ y :: ys
Tactic:
simp only [List.mem_cons]
State after:
case pos
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x ∈ insert' a ys → x = a ∨ x ∈ ys
h✝ : a ≤ y
hel : x = a ∨ x = y ∨ x ∈ ys
⊢ x = a ∨ x = y ∨ x ∈ ys

State before:
case pos
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x ∈ insert' a ys → x = a ∨ x ∈ ys
h✝ : a ≤ y
hel : x = a ∨ x = y ∨ x ∈ ys
⊢ x = a ∨ x = y ∨ x ∈ ys
Tactic:
exact hel
State after:
no goals

State before:
case neg
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x ∈ insert' a ys → x = a ∨ x ∈ ys
h✝ : ¬a ≤ y
hel : x ∈ y :: insert' a ys
⊢ x = a ∨ x ∈ y :: ys
Tactic:
simp only [List.mem_cons] at hel
State after:
case neg
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x ∈ insert' a ys → x = a ∨ x ∈ ys
h✝ : ¬a ≤ y
hel : x = y ∨ x ∈ insert' a ys
⊢ x = a ∨ x ∈ y :: ys

State before:
case neg
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x ∈ insert' a ys → x = a ∨ x ∈ ys
h✝ : ¬a ≤ y
hel : x = y ∨ x ∈ insert' a ys
⊢ x = a ∨ x ∈ y :: ys
Tactic:
simp only [List.mem_cons]
State after:
case neg
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x ∈ insert' a ys → x = a ∨ x ∈ ys
h✝ : ¬a ≤ y
hel : x = y ∨ x ∈ insert' a ys
⊢ x = a ∨ x = y ∨ x ∈ ys

State before:
case neg
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x ∈ insert' a ys → x = a ∨ x ∈ ys
h✝ : ¬a ≤ y
hel : x = y ∨ x ∈ insert' a ys
⊢ x = a ∨ x = y ∨ x ∈ ys
Tactic:
rcases hel with (heq | hmem)
State after:
case neg.inl
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x ∈ insert' a ys → x = a ∨ x ∈ ys
h✝ : ¬a ≤ y
heq : x = y
⊢ x = a ∨ x = y ∨ x ∈ ys

case neg.inr
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x ∈ insert' a ys → x = a ∨ x ∈ ys
h✝ : ¬a ≤ y
hmem : x ∈ insert' a ys
⊢ x = a ∨ x = y ∨ x ∈ ys

State before:
case neg.inl
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x ∈ insert' a ys → x = a ∨ x ∈ ys
h✝ : ¬a ≤ y
heq : x = y
⊢ x = a ∨ x = y ∨ x ∈ ys
Tactic:
right
State after:
case neg.inl.h
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x ∈ insert' a ys → x = a ∨ x ∈ ys
h✝ : ¬a ≤ y
heq : x = y
⊢ x = y ∨ x ∈ ys

State before:
case neg.inl.h
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x ∈ insert' a ys → x = a ∨ x ∈ ys
h✝ : ¬a ≤ y
heq : x = y
⊢ x = y ∨ x ∈ ys
Tactic:
left
State after:
case neg.inl.h.h
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x ∈ insert' a ys → x = a ∨ x ∈ ys
h✝ : ¬a ≤ y
heq : x = y
⊢ x = y

State before:
case neg.inl.h.h
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x ∈ insert' a ys → x = a ∨ x ∈ ys
h✝ : ¬a ≤ y
heq : x = y
⊢ x = y
Tactic:
exact heq
State after:
no goals

State before:
case neg.inr
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x ∈ insert' a ys → x = a ∨ x ∈ ys
h✝ : ¬a ≤ y
hmem : x ∈ insert' a ys
⊢ x = a ∨ x = y ∨ x ∈ ys
Tactic:
rcases ih hmem with (heq' | hmem')
State after:
case neg.inr.inl
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x ∈ insert' a ys → x = a ∨ x ∈ ys
h✝ : ¬a ≤ y
hmem : x ∈ insert' a ys
heq' : x = a
⊢ x = a ∨ x = y ∨ x ∈ ys

case neg.inr.inr
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x ∈ insert' a ys → x = a ∨ x ∈ ys
h✝ : ¬a ≤ y
hmem : x ∈ insert' a ys
hmem' : x ∈ ys
⊢ x = a ∨ x = y ∨ x ∈ ys

State before:
case neg.inr.inl
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x ∈ insert' a ys → x = a ∨ x ∈ ys
h✝ : ¬a ≤ y
hmem : x ∈ insert' a ys
heq' : x = a
⊢ x = a ∨ x = y ∨ x ∈ ys
Tactic:
left
State after:
case neg.inr.inl.h
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x ∈ insert' a ys → x = a ∨ x ∈ ys
h✝ : ¬a ≤ y
hmem : x ∈ insert' a ys
heq' : x = a
⊢ x = a

State before:
case neg.inr.inl.h
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x ∈ insert' a ys → x = a ∨ x ∈ ys
h✝ : ¬a ≤ y
hmem : x ∈ insert' a ys
heq' : x = a
⊢ x = a
Tactic:
exact heq'
State after:
no goals

State before:
case neg.inr.inr
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x ∈ insert' a ys → x = a ∨ x ∈ ys
h✝ : ¬a ≤ y
hmem : x ∈ insert' a ys
hmem' : x ∈ ys
⊢ x = a ∨ x = y ∨ x ∈ ys
Tactic:
right
State after:
case neg.inr.inr.h
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x ∈ insert' a ys → x = a ∨ x ∈ ys
h✝ : ¬a ≤ y
hmem : x ∈ insert' a ys
hmem' : x ∈ ys
⊢ x = y ∨ x ∈ ys

State before:
case neg.inr.inr.h
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x ∈ insert' a ys → x = a ∨ x ∈ ys
h✝ : ¬a ≤ y
hmem : x ∈ insert' a ys
hmem' : x ∈ ys
⊢ x = y ∨ x ∈ ys
Tactic:
right
State after:
case neg.inr.inr.h.h
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x ∈ insert' a ys → x = a ∨ x ∈ ys
h✝ : ¬a ≤ y
hmem : x ∈ insert' a ys
hmem' : x ∈ ys
⊢ x ∈ ys

State before:
case neg.inr.inr.h.h
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x ∈ insert' a ys → x = a ∨ x ∈ ys
h✝ : ¬a ≤ y
hmem : x ∈ insert' a ys
hmem' : x ∈ ys
⊢ x ∈ ys
Tactic:
exact hmem'
State after:
no goals

State before:
case mpr
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a : α
l : List α
⊢ x = a ∨ x ∈ l → x ∈ insert' a l
Tactic:
intro hor
State after:
case mpr
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a : α
l : List α
hor : x = a ∨ x ∈ l
⊢ x ∈ insert' a l

State before:
case mpr
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a : α
l : List α
hor : x = a ∨ x ∈ l
⊢ x ∈ insert' a l
Tactic:
induction' l with y ys ih
State after:
case mpr.nil
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a : α
hor : x = a ∨ x ∈ []
⊢ x ∈ insert' a []

case mpr.cons
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x = a ∨ x ∈ ys → x ∈ insert' a ys
hor : x = a ∨ x ∈ y :: ys
⊢ x ∈ insert' a (y :: ys)

State before:
case mpr.nil
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a : α
hor : x = a ∨ x ∈ []
⊢ x ∈ insert' a []
Tactic:
rw [insert', List.mem_singleton]
State after:
case mpr.nil
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a : α
hor : x = a ∨ x ∈ []
⊢ x = a

State before:
case mpr.nil
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a : α
hor : x = a ∨ x ∈ []
⊢ x = a
Tactic:
rcases hor with (heq | hmem)
State after:
case mpr.nil.inl
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a : α
heq : x = a
⊢ x = a

case mpr.nil.inr
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a : α
hmem : x ∈ []
⊢ x = a

State before:
case mpr.nil.inl
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a : α
heq : x = a
⊢ x = a
Tactic:
exact heq
State after:
no goals

State before:
case mpr.nil.inr
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a : α
hmem : x ∈ []
⊢ x = a
Tactic:
simp only [List.not_mem_nil] at hmem
State after:
no goals

State before:
case mpr.cons
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x = a ∨ x ∈ ys → x ∈ insert' a ys
hor : x = a ∨ x ∈ y :: ys
⊢ x ∈ insert' a (y :: ys)
Tactic:
rw [insert']
State after:
case mpr.cons
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x = a ∨ x ∈ ys → x ∈ insert' a ys
hor : x = a ∨ x ∈ y :: ys
⊢ x ∈ if a ≤ y then a :: y :: ys else y :: insert' a ys

State before:
case mpr.cons
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x = a ∨ x ∈ ys → x ∈ insert' a ys
hor : x = a ∨ x ∈ y :: ys
⊢ x ∈ if a ≤ y then a :: y :: ys else y :: insert' a ys
Tactic:
split_ifs
State after:
case pos
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x = a ∨ x ∈ ys → x ∈ insert' a ys
hor : x = a ∨ x ∈ y :: ys
h✝ : a ≤ y
⊢ x ∈ a :: y :: ys

case neg
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x = a ∨ x ∈ ys → x ∈ insert' a ys
hor : x = a ∨ x ∈ y :: ys
h✝ : ¬a ≤ y
⊢ x ∈ y :: insert' a ys

State before:
case pos
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x = a ∨ x ∈ ys → x ∈ insert' a ys
hor : x = a ∨ x ∈ y :: ys
h✝ : a ≤ y
⊢ x ∈ a :: y :: ys
Tactic:
simp only [List.mem_cons]
State after:
case pos
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x = a ∨ x ∈ ys → x ∈ insert' a ys
hor : x = a ∨ x ∈ y :: ys
h✝ : a ≤ y
⊢ x = a ∨ x = y ∨ x ∈ ys

State before:
case pos
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x = a ∨ x ∈ ys → x ∈ insert' a ys
hor : x = a ∨ x ∈ y :: ys
h✝ : a ≤ y
⊢ x = a ∨ x = y ∨ x ∈ ys
Tactic:
rcases hor with (heq | hmem)
State after:
case pos.inl
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x = a ∨ x ∈ ys → x ∈ insert' a ys
h✝ : a ≤ y
heq : x = a
⊢ x = a ∨ x = y ∨ x ∈ ys

case pos.inr
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x = a ∨ x ∈ ys → x ∈ insert' a ys
h✝ : a ≤ y
hmem : x ∈ y :: ys
⊢ x = a ∨ x = y ∨ x ∈ ys

State before:
case pos.inl
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x = a ∨ x ∈ ys → x ∈ insert' a ys
h✝ : a ≤ y
heq : x = a
⊢ x = a ∨ x = y ∨ x ∈ ys
Tactic:
left
State after:
case pos.inl.h
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x = a ∨ x ∈ ys → x ∈ insert' a ys
h✝ : a ≤ y
heq : x = a
⊢ x = a

State before:
case pos.inl.h
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x = a ∨ x ∈ ys → x ∈ insert' a ys
h✝ : a ≤ y
heq : x = a
⊢ x = a
Tactic:
exact heq
State after:
no goals

State before:
case pos.inr
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x = a ∨ x ∈ ys → x ∈ insert' a ys
h✝ : a ≤ y
hmem : x ∈ y :: ys
⊢ x = a ∨ x = y ∨ x ∈ ys
Tactic:
right
State after:
case pos.inr.h
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x = a ∨ x ∈ ys → x ∈ insert' a ys
h✝ : a ≤ y
hmem : x ∈ y :: ys
⊢ x = y ∨ x ∈ ys

State before:
case pos.inr.h
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x = a ∨ x ∈ ys → x ∈ insert' a ys
h✝ : a ≤ y
hmem : x ∈ y :: ys
⊢ x = y ∨ x ∈ ys
Tactic:
simp only [List.mem_cons] at hmem
State after:
case pos.inr.h
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x = a ∨ x ∈ ys → x ∈ insert' a ys
h✝ : a ≤ y
hmem : x = y ∨ x ∈ ys
⊢ x = y ∨ x ∈ ys

State before:
case pos.inr.h
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x = a ∨ x ∈ ys → x ∈ insert' a ys
h✝ : a ≤ y
hmem : x = y ∨ x ∈ ys
⊢ x = y ∨ x ∈ ys
Tactic:
exact hmem
State after:
no goals

State before:
case neg
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x = a ∨ x ∈ ys → x ∈ insert' a ys
hor : x = a ∨ x ∈ y :: ys
h✝ : ¬a ≤ y
⊢ x ∈ y :: insert' a ys
Tactic:
simp only [List.mem_cons]
State after:
case neg
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x = a ∨ x ∈ ys → x ∈ insert' a ys
hor : x = a ∨ x ∈ y :: ys
h✝ : ¬a ≤ y
⊢ x = y ∨ x ∈ insert' a ys

State before:
case neg
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x = a ∨ x ∈ ys → x ∈ insert' a ys
hor : x = a ∨ x ∈ y :: ys
h✝ : ¬a ≤ y
⊢ x = y ∨ x ∈ insert' a ys
Tactic:
rcases hor with (heq | hmem)
State after:
case neg.inl
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x = a ∨ x ∈ ys → x ∈ insert' a ys
h✝ : ¬a ≤ y
heq : x = a
⊢ x = y ∨ x ∈ insert' a ys

case neg.inr
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x = a ∨ x ∈ ys → x ∈ insert' a ys
h✝ : ¬a ≤ y
hmem : x ∈ y :: ys
⊢ x = y ∨ x ∈ insert' a ys

State before:
case neg.inl
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x = a ∨ x ∈ ys → x ∈ insert' a ys
h✝ : ¬a ≤ y
heq : x = a
⊢ x = y ∨ x ∈ insert' a ys
Tactic:
right
State after:
case neg.inl.h
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x = a ∨ x ∈ ys → x ∈ insert' a ys
h✝ : ¬a ≤ y
heq : x = a
⊢ x ∈ insert' a ys

State before:
case neg.inl.h
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x = a ∨ x ∈ ys → x ∈ insert' a ys
h✝ : ¬a ≤ y
heq : x = a
⊢ x ∈ insert' a ys
Tactic:
exact ih (Or.inl heq)
State after:
no goals

State before:
case neg.inr
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x = a ∨ x ∈ ys → x ∈ insert' a ys
h✝ : ¬a ≤ y
hmem : x ∈ y :: ys
⊢ x = y ∨ x ∈ insert' a ys
Tactic:
simp only [List.mem_cons] at hmem
State after:
case neg.inr
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x = a ∨ x ∈ ys → x ∈ insert' a ys
h✝ : ¬a ≤ y
hmem : x = y ∨ x ∈ ys
⊢ x = y ∨ x ∈ insert' a ys

State before:
case neg.inr
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x = a ∨ x ∈ ys → x ∈ insert' a ys
h✝ : ¬a ≤ y
hmem : x = y ∨ x ∈ ys
⊢ x = y ∨ x ∈ insert' a ys
Tactic:
rcases hmem with (heq' | hmem')
State after:
case neg.inr.inl
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x = a ∨ x ∈ ys → x ∈ insert' a ys
h✝ : ¬a ≤ y
heq' : x = y
⊢ x = y ∨ x ∈ insert' a ys

case neg.inr.inr
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x = a ∨ x ∈ ys → x ∈ insert' a ys
h✝ : ¬a ≤ y
hmem' : x ∈ ys
⊢ x = y ∨ x ∈ insert' a ys

State before:
case neg.inr.inl
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x = a ∨ x ∈ ys → x ∈ insert' a ys
h✝ : ¬a ≤ y
heq' : x = y
⊢ x = y ∨ x ∈ insert' a ys
Tactic:
left
State after:
case neg.inr.inl.h
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x = a ∨ x ∈ ys → x ∈ insert' a ys
h✝ : ¬a ≤ y
heq' : x = y
⊢ x = y

State before:
case neg.inr.inl.h
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x = a ∨ x ∈ ys → x ∈ insert' a ys
h✝ : ¬a ≤ y
heq' : x = y
⊢ x = y
Tactic:
exact heq'
State after:
no goals

State before:
case neg.inr.inr
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x = a ∨ x ∈ ys → x ∈ insert' a ys
h✝ : ¬a ≤ y
hmem' : x ∈ ys
⊢ x = y ∨ x ∈ insert' a ys
Tactic:
right
State after:
case neg.inr.inr.h
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x = a ∨ x ∈ ys → x ∈ insert' a ys
h✝ : ¬a ≤ y
hmem' : x ∈ ys
⊢ x ∈ insert' a ys

State before:
case neg.inr.inr.h
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x = a ∨ x ∈ ys → x ∈ insert' a ys
h✝ : ¬a ≤ y
hmem' : x ∈ ys
⊢ x ∈ insert' a ys
Tactic:
exact ih (Or.inr hmem')
State after:
no goals