α : Type u_1
a : Lists α
l₁ l₂ : Lists' α true
h : cons a l₁ ⊆ l₂
⊢ a ∈ l₂ ∧ l₁ ⊆ l₂
α : Type u_1
a : Lists α
l₁ l₂ : Lists' α true
⊢ cons a l₁ ⊆ l₂ ↔ a ∈ l₂ ∧ l₁ ⊆ l₂
refine' ⟨fun h => _, fun ⟨⟨a', m, e⟩, s⟩ => Subset.cons e m s⟩
α : Type u_1
a : Lists α
l₁ l₂ l₁' : Lists' α true
h' : cons a l₁ = l₁'
h : l₁' ⊆ l₂
⊢ a ∈ l₂ ∧ l₁ ⊆ l₂
α : Type u_1
a : Lists α
l₁ l₂ : Lists' α true
h : cons a l₁ ⊆ l₂
⊢ a ∈ l₂ ∧ l₁ ⊆ l₂
generalize h' : Lists'.cons a l₁ = l₁' at h
case nil
α : Type u_1
a : Lists α
l₁ l₂ : Lists' α true
h' : cons a l₁ = nil
⊢ a ∈ l₂ ∧ l₁ ⊆ l₂

case cons
α : Type u_1
a : Lists α
l₁ l₂ : Lists' α true
a' a'' : Lists α
l : Lists' α true
e : a' ~ a''
h' : cons a l₁ = cons a' l
m : a'' ∈ toList l₂
s : Subset l l₂
⊢ a ∈ l₂ ∧ l₁ ⊆ l₂
α : Type u_1
a : Lists α
l₁ l₂ l₁' : Lists' α true
h' : cons a l₁ = l₁'
h : l₁' ⊆ l₂
⊢ a ∈ l₂ ∧ l₁ ⊆ l₂
cases' h with l a' a'' l l' e m s
case cons.mk
α : Type u_1
l₁ l₂ : Lists' α true
a' a'' : Lists α
l : Lists' α true
e : a' ~ a''
m : a'' ∈ toList l₂
s : Subset l l₂
fst✝ : Bool
snd✝ : Lists' α fst✝
h' : cons { fst := fst✝, snd := snd✝ } l₁ = cons a' l
⊢ { fst := fst✝, snd := snd✝ } ∈ l₂ ∧ l₁ ⊆ l₂
case cons
α : Type u_1
a : Lists α
l₁ l₂ : Lists' α true
a' a'' : Lists α
l : Lists' α true
e : a' ~ a''
h' : cons a l₁ = cons a' l
m : a'' ∈ toList l₂
s : Subset l l₂
⊢ a ∈ l₂ ∧ l₁ ⊆ l₂
cases a
case cons.mk.mk
α : Type u_1
l₁ l₂ : Lists' α true
a'' : Lists α
l : Lists' α true
m : a'' ∈ toList l₂
s : Subset l l₂
fst✝¹ : Bool
snd✝¹ : Lists' α fst✝¹
fst✝ : Bool
snd✝ : Lists' α fst✝
e : { fst := fst✝, snd := snd✝ } ~ a''
h' : cons { fst := fst✝¹, snd := snd✝¹ } l₁ = cons { fst := fst✝, snd := snd✝ } l
⊢ { fst := fst✝¹, snd := snd✝¹ } ∈ l₂ ∧ l₁ ⊆ l₂
case cons.mk
α : Type u_1
l₁ l₂ : Lists' α true
a' a'' : Lists α
l : Lists' α true
e : a' ~ a''
m : a'' ∈ toList l₂
s : Subset l l₂
fst✝ : Bool
snd✝ : Lists' α fst✝
h' : cons { fst := fst✝, snd := snd✝ } l₁ = cons a' l
⊢ { fst := fst✝, snd := snd✝ } ∈ l₂ ∧ l₁ ⊆ l₂
cases a'
case cons.mk.mk.refl
α : Type u_1
l₁ l₂ : Lists' α true
a'' : Lists α
m : a'' ∈ toList l₂
fst✝ : Bool
snd✝ : Lists' α fst✝
e : { fst := fst✝, snd := snd✝ } ~ a''
s : Subset l₁ l₂
⊢ { fst := fst✝, snd := snd✝ } ∈ l₂ ∧ l₁ ⊆ l₂
case cons.mk.mk
α : Type u_1
l₁ l₂ : Lists' α true
a'' : Lists α
l : Lists' α true
m : a'' ∈ toList l₂
s : Subset l l₂
fst✝¹ : Bool
snd✝¹ : Lists' α fst✝¹
fst✝ : Bool
snd✝ : Lists' α fst✝
e : { fst := fst✝, snd := snd✝ } ~ a''
h' : cons { fst := fst✝¹, snd := snd✝¹ } l₁ = cons { fst := fst✝, snd := snd✝ } l
⊢ { fst := fst✝¹, snd := snd✝¹ } ∈ l₂ ∧ l₁ ⊆ l₂
cases h'
no goals
case cons.mk.mk.refl
α : Type u_1
l₁ l₂ : Lists' α true
a'' : Lists α
m : a'' ∈ toList l₂
fst✝ : Bool
snd✝ : Lists' α fst✝
e : { fst := fst✝, snd := snd✝ } ~ a''
s : Subset l₁ l₂
⊢ { fst := fst✝, snd := snd✝ } ∈ l₂ ∧ l₁ ⊆ l₂
exact ⟨⟨_, m, e⟩, s⟩
case nil.mk
α : Type u_1
l₁ l₂ : Lists' α true
fst✝ : Bool
snd✝ : Lists' α fst✝
h' : cons { fst := fst✝, snd := snd✝ } l₁ = nil
⊢ { fst := fst✝, snd := snd✝ } ∈ l₂ ∧ l₁ ⊆ l₂
case nil
α : Type u_1
a : Lists α
l₁ l₂ : Lists' α true
h' : cons a l₁ = nil
⊢ a ∈ l₂ ∧ l₁ ⊆ l₂
cases a
no goals
case nil.mk
α : Type u_1
l₁ l₂ : Lists' α true
fst✝ : Bool
snd✝ : Lists' α fst✝
h' : cons { fst := fst✝, snd := snd✝ } l₁ = nil
⊢ { fst := fst✝, snd := snd✝ } ∈ l₂ ∧ l₁ ⊆ l₂
cases h'