case slnil
α : Type u_1
l : List α
x : α
l' : List α
hx✝ : x ∈+ l
hx : x ∈+ []
⊢ x ∈+ []

case cons
α : Type u_1
l : List α
x : α
l' : List α
hx✝ : x ∈+ l
l₁ l₂ : List α
y : α
a✝ : l₁ <+ l₂
IH : x ∈+ l₁ → x ∈+ l₂
hx : x ∈+ l₁
⊢ x ∈+ y :: l₂

case cons₂
α : Type u_1
l : List α
x : α
l' : List α
hx✝ : x ∈+ l
l₁ l₂ : List α
y : α
h : l₁ <+ l₂
IH : x ∈+ l₁ → x ∈+ l₂
hx : x ∈+ y :: l₁
⊢ x ∈+ y :: l₂
α : Type u_1
l : List α
x : α
l' : List α
hx : x ∈+ l
h : l <+ l'
⊢ x ∈+ l'
induction' h with l₁ l₂ y _ IH l₁ l₂ y h IH
no goals
case slnil
α : Type u_1
l : List α
x : α
l' : List α
hx✝ : x ∈+ l
hx : x ∈+ []
⊢ x ∈+ []
exact hx
no goals
case cons
α : Type u_1
l : List α
x : α
l' : List α
hx✝ : x ∈+ l
l₁ l₂ : List α
y : α
a✝ : l₁ <+ l₂
IH : x ∈+ l₁ → x ∈+ l₂
hx : x ∈+ l₁
⊢ x ∈+ y :: l₂
exact (IH hx).duplicate_cons _
case cons₂
α : Type u_1
l : List α
x : α
l' : List α
hx✝ : x ∈+ l
l₁ l₂ : List α
y : α
h : l₁ <+ l₂
IH : x ∈+ l₁ → x ∈+ l₂
hx : y = x ∧ x ∈ l₁ ∨ x ∈+ l₁
⊢ y = x ∧ x ∈ l₂ ∨ x ∈+ l₂
case cons₂
α : Type u_1
l : List α
x : α
l' : List α
hx✝ : x ∈+ l
l₁ l₂ : List α
y : α
h : l₁ <+ l₂
IH : x ∈+ l₁ → x ∈+ l₂
hx : x ∈+ y :: l₁
⊢ x ∈+ y :: l₂
rw [duplicate_cons_iff] at hx⊢
case cons₂.inl.intro
α : Type u_1
l l' l₁ l₂ : List α
y : α
h : l₁ <+ l₂
hx✝ : y ∈+ l
IH : y ∈+ l₁ → y ∈+ l₂
hx : y ∈ l₁
⊢ y = y ∧ y ∈ l₂ ∨ y ∈+ l₂

case cons₂.inr
α : Type u_1
l : List α
x : α
l' : List α
hx✝ : x ∈+ l
l₁ l₂ : List α
y : α
h : l₁ <+ l₂
IH : x ∈+ l₁ → x ∈+ l₂
hx : x ∈+ l₁
⊢ y = x ∧ x ∈ l₂ ∨ x ∈+ l₂
case cons₂
α : Type u_1
l : List α
x : α
l' : List α
hx✝ : x ∈+ l
l₁ l₂ : List α
y : α
h : l₁ <+ l₂
IH : x ∈+ l₁ → x ∈+ l₂
hx : y = x ∧ x ∈ l₁ ∨ x ∈+ l₁
⊢ y = x ∧ x ∈ l₂ ∨ x ∈+ l₂
rcases hx with (⟨rfl, hx⟩ | hx)
no goals
case cons₂.inl.intro
α : Type u_1
l l' l₁ l₂ : List α
y : α
h : l₁ <+ l₂
hx✝ : y ∈+ l
IH : y ∈+ l₁ → y ∈+ l₂
hx : y ∈ l₁
⊢ y = y ∧ y ∈ l₂ ∨ y ∈+ l₂
simp [h.subset hx]
no goals
case cons₂.inr
α : Type u_1
l : List α
x : α
l' : List α
hx✝ : x ∈+ l
l₁ l₂ : List α
y : α
h : l₁ <+ l₂
IH : x ∈+ l₁ → x ∈+ l₂
hx : x ∈+ l₁
⊢ y = x ∧ x ∈ l₂ ∨ x ∈+ l₂
simp [IH hx]