-- Mathlib/Data/List/Sublists.lean
theorem mem_sublists' {s t : List α} : s ∈ sublists' t ↔ s <+ t

Proof state:
case cons
α : Type u
a : α
t : List α
IH : ∀ {s : List α}, s ∈ t.sublists' ↔ s <+ t
s : List α
⊢ (s <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = s) ↔ s <+ a :: t

Tactic:
constructor <;> intro h

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

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

Proof state:
case cons.mpr
α : Type u
a : α
t : List α
IH : ∀ {s : List α}, s ∈ t.sublists' ↔ s <+ t
s : List α
h : s <+ a :: t
⊢ s <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = s

Tactic:
obtain - | ⟨-, h⟩ | ⟨-, h⟩ := h

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

case cons.mpr.cons₂
α : Type u
a : α
t : List α
IH : ∀ {s : List α}, s ∈ t.sublists' ↔ s <+ t
l₁✝ : List α
h : l₁✝ <+ t
⊢ a :: l₁✝ <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = a :: l₁✝

Proof state:
case cons.mpr.cons
α : Type u
a : α
t : List α
IH : ∀ {s : List α}, s ∈ t.sublists' ↔ s <+ t
s : List α
h : s <+ t
⊢ s <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = s

Tactic:
exact Or.inl h

Result:
no goals

Proof state:
α : Type u
s : List α
h : s = []
⊢ s <+ []

Tactic:
rw [h]

Result:
no goals

Proof state:
case cons.mp.inl
α : Type u
a : α
t : List α
IH : ∀ {s : List α}, s ∈ t.sublists' ↔ s <+ t
s : List α
h : s <+ t
⊢ s <+ a :: t

Tactic:
exact sublist_cons_of_sublist _ h

Result:
no goals

Proof state:
case nil
α : Type u
s : List α
⊢ s = [] ↔ s <+ []

Tactic:
exact ⟨fun h => by rw [h], eq_nil_of_sublist_nil⟩

Result:
no goals

Proof state:
case nil
α : Type u
s : List α
⊢ s ∈ [].sublists' ↔ s <+ []

Tactic:
simp only [sublists'_nil, mem_singleton]

Result:
case nil
α : Type u
s : List α
⊢ s = [] ↔ s <+ []

Proof state:
case cons.mp.inr.intro.intro
α : Type u
a : α
t : List α
IH : ∀ {s : List α}, s ∈ t.sublists' ↔ s <+ t
s : List α
h : s <+ t
⊢ a :: s <+ a :: t

Tactic:
exact h.cons_cons _

Result:
no goals

Proof state:
case cons
α : Type u
a : α
t : List α
IH : ∀ {s : List α}, s ∈ t.sublists' ↔ s <+ t
s : List α
⊢ s ∈ (a :: t).sublists' ↔ s <+ a :: t

Tactic:
simp only [sublists'_cons, mem_append, IH, mem_map]

Result:
case cons
α : Type u
a : α
t : List α
IH : ∀ {s : List α}, s ∈ t.sublists' ↔ s <+ t
s : List α
⊢ (s <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = s) ↔ s <+ a :: t

Proof state:
case cons.mpr.cons₂
α : Type u
a : α
t : List α
IH : ∀ {s : List α}, s ∈ t.sublists' ↔ s <+ t
l₁✝ : List α
h : l₁✝ <+ t
⊢ a :: l₁✝ <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = a :: l₁✝

Tactic:
exact Or.inr ⟨_, h, rfl⟩

Result:
no goals

Proof state:
case cons.mp
α : Type u
a : α
t : List α
IH : ∀ {s : List α}, s ∈ t.sublists' ↔ s <+ t
s : List α
h : s <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = s
⊢ s <+ a :: t

Tactic:
rcases h with (h | ⟨s, h, rfl⟩)

Result:
case cons.mp.inl
α : Type u
a : α
t : List α
IH : ∀ {s : List α}, s ∈ t.sublists' ↔ s <+ t
s : List α
h : s <+ t
⊢ s <+ a :: t

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

Proof state:
α : Type u
s t : List α
⊢ s ∈ t.sublists' ↔ s <+ t

Tactic:
induction' t with a t IH generalizing s

Result:
case nil
α : Type u
s : List α
⊢ s ∈ [].sublists' ↔ s <+ []

case cons
α : Type u
a : α
t : List α
IH : ∀ {s : List α}, s ∈ t.sublists' ↔ s <+ t
s : List α
⊢ s ∈ (a :: t).sublists' ↔ s <+ a :: t