case mp
α : Type u_1
β : Type ?u.27592
l l₁ l₂ l₃ : List α
a b : α
m n : ℕ
⊢ a :: l₁ <+: b :: l₂ → a = b ∧ l₁ <+: l₂

case mpr
α : Type u_1
β : Type ?u.27592
l l₁ l₂ l₃ : List α
a b : α
m n : ℕ
⊢ a = b ∧ l₁ <+: l₂ → a :: l₁ <+: b :: l₂
α : Type u_1
β : Type ?u.27592
l l₁ l₂ l₃ : List α
a b : α
m n : ℕ
⊢ a :: l₁ <+: b :: l₂ ↔ a = b ∧ l₁ <+: l₂
constructor
case mp.intro
α : Type u_1
β : Type ?u.27592
l l₁ l₂ l₃ : List α
a b : α
m n : ℕ
L : List α
hL : a :: l₁ ++ L = b :: l₂
⊢ a = b ∧ l₁ <+: l₂
case mp
α : Type u_1
β : Type ?u.27592
l l₁ l₂ l₃ : List α
a b : α
m n : ℕ
⊢ a :: l₁ <+: b :: l₂ → a = b ∧ l₁ <+: l₂
rintro ⟨L, hL⟩
case mp.intro
α : Type u_1
β : Type ?u.27592
l l₁ l₂ l₃ : List α
a b : α
m n : ℕ
L : List α
hL : a :: (l₁ ++ L) = b :: l₂
⊢ a = b ∧ l₁ <+: l₂
case mp.intro
α : Type u_1
β : Type ?u.27592
l l₁ l₂ l₃ : List α
a b : α
m n : ℕ
L : List α
hL : a :: l₁ ++ L = b :: l₂
⊢ a = b ∧ l₁ <+: l₂
simp only [cons_append] at hL
case mp.intro
α : Type u_1
β : Type ?u.27592
l l₁ l₂ l₃ : List α
a b : α
m n : ℕ
L : List α
hLLeft : a = b
hLRight : l₁ ++ L = l₂
⊢ a = b ∧ l₁ <+: l₂
case mp.intro
α : Type u_1
β : Type ?u.27592
l l₁ l₂ l₃ : List α
a b : α
m n : ℕ
L : List α
hL : a :: (l₁ ++ L) = b :: l₂
⊢ a = b ∧ l₁ <+: l₂
injection hL with hLLeft hLRight
no goals
case mp.intro
α : Type u_1
β : Type ?u.27592
l l₁ l₂ l₃ : List α
a b : α
m n : ℕ
L : List α
hLLeft : a = b
hLRight : l₁ ++ L = l₂
⊢ a = b ∧ l₁ <+: l₂
exact ⟨hLLeft, ⟨L, hLRight⟩⟩
case mpr.intro
α : Type u_1
β : Type ?u.27592
l l₁ l₂ l₃ : List α
a : α
m n : ℕ
h : l₁ <+: l₂
⊢ a :: l₁ <+: a :: l₂
case mpr
α : Type u_1
β : Type ?u.27592
l l₁ l₂ l₃ : List α
a b : α
m n : ℕ
⊢ a = b ∧ l₁ <+: l₂ → a :: l₁ <+: b :: l₂
rintro ⟨rfl, h⟩
no goals
case mpr.intro
α : Type u_1
β : Type ?u.27592
l l₁ l₂ l₃ : List α
a : α
m n : ℕ
h : l₁ <+: l₂
⊢ a :: l₁ <+: a :: l₂
rwa [prefix_cons_inj]