case mp
α✝ : Type u_1
l₁ : List α✝
a : α✝
l₂ : List α✝
⊢ l₁ <:+: a :: l₂ → l₁ <+: a :: l₂ ∨ l₁ <:+: l₂

case mpr
α✝ : Type u_1
l₁ : List α✝
a : α✝
l₂ : List α✝
⊢ l₁ <+: a :: l₂ ∨ l₁ <:+: l₂ → l₁ <:+: a :: l₂
α✝ : Type u_1
l₁ : List α✝
a : α✝
l₂ : List α✝
⊢ l₁ <:+: a :: l₂ ↔ l₁ <+: a :: l₂ ∨ l₁ <:+: l₂
constructor
case mp.intro.nil.intro
α✝ : Type u_1
l₁ : List α✝
a : α✝
l₂ t : List α✝
hl₃ : [] ++ l₁ ++ t = a :: l₂
⊢ l₁ <+: a :: l₂ ∨ l₁ <:+: l₂

case mp.intro.cons.intro
α✝ : Type u_1
l₁ : List α✝
a : α✝
l₂ : List α✝
head✝ : α✝
tail✝ t : List α✝
hl₃ : head✝ :: tail✝ ++ l₁ ++ t = a :: l₂
⊢ l₁ <+: a :: l₂ ∨ l₁ <:+: l₂
case mp
α✝ : Type u_1
l₁ : List α✝
a : α✝
l₂ : List α✝
⊢ l₁ <:+: a :: l₂ → l₁ <+: a :: l₂ ∨ l₁ <:+: l₂
rintro ⟨⟨hd, tl⟩, t, hl₃⟩
no goals
case mp.intro.nil.intro
α✝ : Type u_1
l₁ : List α✝
a : α✝
l₂ t : List α✝
hl₃ : [] ++ l₁ ++ t = a :: l₂
⊢ l₁ <+: a :: l₂ ∨ l₁ <:+: l₂
exact Or.inl ⟨t, hl₃⟩
case mp.intro.cons.intro
α✝ : Type u_1
l₁ : List α✝
a : α✝
l₂ : List α✝
head✝ : α✝
tail✝ t : List α✝
hl₃ : head✝ :: (tail✝ ++ l₁ ++ t) = a :: l₂
⊢ l₁ <+: a :: l₂ ∨ l₁ <:+: l₂
case mp.intro.cons.intro
α✝ : Type u_1
l₁ : List α✝
a : α✝
l₂ : List α✝
head✝ : α✝
tail✝ t : List α✝
hl₃ : head✝ :: tail✝ ++ l₁ ++ t = a :: l₂
⊢ l₁ <+: a :: l₂ ∨ l₁ <:+: l₂
simp only [cons_append] at hl₃
case mp.intro.cons.intro
α✝ : Type u_1
l₁ : List α✝
a : α✝
l₂ : List α✝
head✝ : α✝
tail✝ t : List α✝
head_eq✝ : head✝ = a
hl₄ : tail✝ ++ l₁ ++ t = l₂
⊢ l₁ <+: a :: l₂ ∨ l₁ <:+: l₂
case mp.intro.cons.intro
α✝ : Type u_1
l₁ : List α✝
a : α✝
l₂ : List α✝
head✝ : α✝
tail✝ t : List α✝
hl₃ : head✝ :: (tail✝ ++ l₁ ++ t) = a :: l₂
⊢ l₁ <+: a :: l₂ ∨ l₁ <:+: l₂
injection hl₃ with _ hl₄
no goals
case mp.intro.cons.intro
α✝ : Type u_1
l₁ : List α✝
a : α✝
l₂ : List α✝
head✝ : α✝
tail✝ t : List α✝
head_eq✝ : head✝ = a
hl₄ : tail✝ ++ l₁ ++ t = l₂
⊢ l₁ <+: a :: l₂ ∨ l₁ <:+: l₂
exact Or.inr ⟨_, t, hl₄⟩
case mpr.inl
α✝ : Type u_1
l₁ : List α✝
a : α✝
l₂ : List α✝
h : l₁ <+: a :: l₂
⊢ l₁ <:+: a :: l₂

case mpr.inr
α✝ : Type u_1
l₁ : List α✝
a : α✝
l₂ : List α✝
hl₁ : l₁ <:+: l₂
⊢ l₁ <:+: a :: l₂
case mpr
α✝ : Type u_1
l₁ : List α✝
a : α✝
l₂ : List α✝
⊢ l₁ <+: a :: l₂ ∨ l₁ <:+: l₂ → l₁ <:+: a :: l₂
rintro (h | hl₁)
no goals
case mpr.inl
α✝ : Type u_1
l₁ : List α✝
a : α✝
l₂ : List α✝
h : l₁ <+: a :: l₂
⊢ l₁ <:+: a :: l₂
exact h.isInfix
no goals
case mpr.inr
α✝ : Type u_1
l₁ : List α✝
a : α✝
l₂ : List α✝
hl₁ : l₁ <:+: l₂
⊢ l₁ <:+: a :: l₂
exact infix_cons hl₁