case nil
α : Type u
β : Type v
γ : Type w
s✝ s : List α
⊢ s ∈ sublists' [] ↔ s <+ []

case cons
α : Type u
β : Type v
γ : Type w
s✝ : List α
a : α
t : List α
IH : ∀ {s : List α}, s ∈ sublists' t ↔ s <+ t
s : List α
⊢ s ∈ sublists' (a :: t) ↔ s <+ a :: t
α : Type u
β : Type v
γ : Type w
s t : List α
⊢ s ∈ sublists' t ↔ s <+ t
induction' t with a t IH generalizing s
case cons
α : Type u
β : Type v
γ : Type w
s✝ : List α
a : α
t : List α
IH : ∀ {s : List α}, s ∈ sublists' t ↔ s <+ t
s : List α
⊢ (s <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = s) ↔ s <+ a :: t
case cons
α : Type u
β : Type v
γ : Type w
s✝ : List α
a : α
t : List α
IH : ∀ {s : List α}, s ∈ sublists' t ↔ s <+ t
s : List α
⊢ s ∈ sublists' (a :: t) ↔ s <+ a :: t
simp only [sublists'_cons, mem_append, IH, mem_map]
case cons.mp
α : Type u
β : Type v
γ : Type w
s✝ : List α
a : α
t : List α
IH : ∀ {s : List α}, s ∈ sublists' t ↔ s <+ t
s : List α
h : s <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = s
⊢ s <+ a :: t

case cons.mpr
α : Type u
β : Type v
γ : Type w
s✝ : List α
a : α
t : List α
IH : ∀ {s : List α}, s ∈ sublists' t ↔ s <+ t
s : List α
h : s <+ a :: t
⊢ s <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = s
case cons
α : Type u
β : Type v
γ : Type w
s✝ : List α
a : α
t : List α
IH : ∀ {s : List α}, s ∈ sublists' t ↔ s <+ t
s : List α
⊢ (s <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = s) ↔ s <+ a :: t
constructor <;> intro h
case cons.mp.inl
α : Type u
β : Type v
γ : Type w
s✝ : List α
a : α
t : List α
IH : ∀ {s : List α}, s ∈ sublists' t ↔ s <+ t
s : List α
h : s <+ t
⊢ s <+ a :: t

case cons.mp.inr.intro.intro
α : Type u
β : Type v
γ : Type w
s✝ : List α
a : α
t : List α
IH : ∀ {s : List α}, s ∈ sublists' t ↔ s <+ t
s : List α
h : s <+ t
⊢ a :: s <+ a :: t

case cons.mpr
α : Type u
β : Type v
γ : Type w
s✝ : List α
a : α
t : List α
IH : ∀ {s : List α}, s ∈ sublists' t ↔ s <+ t
s : List α
h : s <+ a :: t
⊢ s <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = s
case cons.mp
α : Type u
β : Type v
γ : Type w
s✝ : List α
a : α
t : List α
IH : ∀ {s : List α}, s ∈ sublists' t ↔ s <+ t
s : List α
h : s <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = s
⊢ s <+ a :: t

case cons.mpr
α : Type u
β : Type v
γ : Type w
s✝ : List α
a : α
t : List α
IH : ∀ {s : List α}, s ∈ sublists' t ↔ s <+ t
s : List α
h : s <+ a :: t
⊢ s <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = s
rcases h with (h | ⟨s, h, rfl⟩)
case nil
α : Type u
β : Type v
γ : Type w
s✝ s : List α
⊢ s = [] ↔ s <+ []
case nil
α : Type u
β : Type v
γ : Type w
s✝ s : List α
⊢ s ∈ sublists' [] ↔ s <+ []
simp only [sublists'_nil, mem_singleton]
no goals
case nil
α : Type u
β : Type v
γ : Type w
s✝ s : List α
⊢ s = [] ↔ s <+ []
exact ⟨fun h => by rw [h], eq_nil_of_sublist_nil⟩
no goals
α : Type u
β : Type v
γ : Type w
s✝ s : List α
h : s = []
⊢ s <+ []
rw [h]
no goals
case cons.mp.inl
α : Type u
β : Type v
γ : Type w
s✝ : List α
a : α
t : List α
IH : ∀ {s : List α}, s ∈ sublists' t ↔ s <+ t
s : List α
h : s <+ t
⊢ s <+ a :: t
exact sublist_cons_of_sublist _ h
no goals
case cons.mp.inr.intro.intro
α : Type u
β : Type v
γ : Type w
s✝ : List α
a : α
t : List α
IH : ∀ {s : List α}, s ∈ sublists' t ↔ s <+ t
s : List α
h : s <+ t
⊢ a :: s <+ a :: t
exact h.cons_cons _
case cons.mpr.cons
α : Type u
β : Type v
γ : Type w
s✝ : List α
a : α
t : List α
IH : ∀ {s : List α}, s ∈ sublists' t ↔ s <+ t
s : List α
h : s <+ t
⊢ s <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = s

case cons.mpr.cons₂
α : Type u
β : Type v
γ : Type w
s✝ : List α
a : α
t : List α
IH : ∀ {s : List α}, s ∈ sublists' t ↔ s <+ t
s : List α
h : s <+ t
⊢ a :: s <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = a :: s
case cons.mpr
α : Type u
β : Type v
γ : Type w
s✝ : List α
a : α
t : List α
IH : ∀ {s : List α}, s ∈ sublists' t ↔ s <+ t
s : List α
h : s <+ a :: t
⊢ s <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = s
cases' h with _ _ _ h s _ _ h
no goals
case cons.mpr.cons
α : Type u
β : Type v
γ : Type w
s✝ : List α
a : α
t : List α
IH : ∀ {s : List α}, s ∈ sublists' t ↔ s <+ t
s : List α
h : s <+ t
⊢ s <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = s
exact Or.inl h
no goals
case cons.mpr.cons₂
α : Type u
β : Type v
γ : Type w
s✝ : List α
a : α
t : List α
IH : ∀ {s : List α}, s ∈ sublists' t ↔ s <+ t
s : List α
h : s <+ t
⊢ a :: s <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = a :: s
exact Or.inr ⟨s, h, rfl⟩