Theorem: List.cons_sublist_cons_iff' (LeanCamCombi/Mathlib/Data/List/Basic.lean)

State before:
α : Type u_1
l l' l₀ l₁ l₂ : List α
a b : α
m n : ℕ
⊢ a :: l₁ <+ b :: l₂ ↔ a :: l₁ <+ l₂ ∨ a = b ∧ l₁ <+ l₂
Tactic:
constructor
State after:
case mp
α : Type u_1
l l' l₀ l₁ l₂ : List α
a b : α
m n : ℕ
⊢ a :: l₁ <+ b :: l₂ → a :: l₁ <+ l₂ ∨ a = b ∧ l₁ <+ l₂

case mpr
α : Type u_1
l l' l₀ l₁ l₂ : List α
a b : α
m n : ℕ
⊢ a :: l₁ <+ l₂ ∨ a = b ∧ l₁ <+ l₂ → a :: l₁ <+ b :: l₂

State before:
case mp
α : Type u_1
l l' l₀ l₁ l₂ : List α
a b : α
m n : ℕ
⊢ a :: l₁ <+ b :: l₂ → a :: l₁ <+ l₂ ∨ a = b ∧ l₁ <+ l₂
Tactic:
rintro (_ | _)
State after:
case mp.cons
α : Type u_1
l l' l₀ l₁ l₂ : List α
a b : α
m n : ℕ
a✝ : a :: l₁ <+ l₂
⊢ a :: l₁ <+ l₂ ∨ a = b ∧ l₁ <+ l₂

case mp.cons₂
α : Type u_1
l l' l₀ l₁ l₂ : List α
a : α
m n : ℕ
a✝ : l₁ <+ l₂
⊢ a :: l₁ <+ l₂ ∨ a = a ∧ l₁ <+ l₂

State before:
case mp.cons
α : Type u_1
l l' l₀ l₁ l₂ : List α
a b : α
m n : ℕ
a✝ : a :: l₁ <+ l₂
⊢ a :: l₁ <+ l₂ ∨ a = b ∧ l₁ <+ l₂
Tactic:
exact Or.inl ‹_›
State after:
no goals

State before:
case mp.cons₂
α : Type u_1
l l' l₀ l₁ l₂ : List α
a : α
m n : ℕ
a✝ : l₁ <+ l₂
⊢ a :: l₁ <+ l₂ ∨ a = a ∧ l₁ <+ l₂
Tactic:
exact Or.inr ⟨rfl, ‹_›⟩
State after:
no goals

State before:
case mpr
α : Type u_1
l l' l₀ l₁ l₂ : List α
a b : α
m n : ℕ
⊢ a :: l₁ <+ l₂ ∨ a = b ∧ l₁ <+ l₂ → a :: l₁ <+ b :: l₂
Tactic:
rintro (h | ⟨rfl, h⟩)
State after:
case mpr.inl
α : Type u_1
l l' l₀ l₁ l₂ : List α
a b : α
m n : ℕ
h : a :: l₁ <+ l₂
⊢ a :: l₁ <+ b :: l₂

case mpr.inr.intro
α : Type u_1
l l' l₀ l₁ l₂ : List α
a : α
m n : ℕ
h : l₁ <+ l₂
⊢ a :: l₁ <+ a :: l₂

State before:
case mpr.inl
α : Type u_1
l l' l₀ l₁ l₂ : List α
a b : α
m n : ℕ
h : a :: l₁ <+ l₂
⊢ a :: l₁ <+ b :: l₂
Tactic:
exact sublist_cons_of_sublist _ h
State after:
no goals

State before:
case mpr.inr.intro
α : Type u_1
l l' l₀ l₁ l₂ : List α
a : α
m n : ℕ
h : l₁ <+ l₂
⊢ a :: l₁ <+ a :: l₂
Tactic:
rwa [cons_sublist_cons]
State after:
no goals