case inl
α : Type u_1
inst✝ : LT α
s : Antisymm fun x x_1 => ¬x < x_1
as✝ bs✝ : List α
a : α
as : List α
b : α
bs : List α
h₁ : a :: as ≤ b :: bs
h₂ : b :: bs ≤ a :: as
hab : a < b
⊢ a :: as = b :: bs

case inr
α : Type u_1
inst✝ : LT α
s : Antisymm fun x x_1 => ¬x < x_1
as✝ bs✝ : List α
a : α
as : List α
b : α
bs : List α
h₁ : a :: as ≤ b :: bs
h₂ : b :: bs ≤ a :: as
hab : ¬a < b
⊢ a :: as = b :: bs
α : Type u_1
inst✝ : LT α
s : Antisymm fun x x_1 => ¬x < x_1
as✝ bs✝ : List α
a : α
as : List α
b : α
bs : List α
h₁ : a :: as ≤ b :: bs
h₂ : b :: bs ≤ a :: as
⊢ a :: as = b :: bs
by_cases hab : a < b
no goals
case inl
α : Type u_1
inst✝ : LT α
s : Antisymm fun x x_1 => ¬x < x_1
as✝ bs✝ : List α
a : α
as : List α
b : α
bs : List α
h₁ : a :: as ≤ b :: bs
h₂ : b :: bs ≤ a :: as
hab : a < b
⊢ a :: as = b :: bs
exact False.elim <| h₂ (List.lt.head _ _ hab)
case inr.inl
α : Type u_1
inst✝ : LT α
s : Antisymm fun x x_1 => ¬x < x_1
as✝ bs✝ : List α
a : α
as : List α
b : α
bs : List α
h₁ : a :: as ≤ b :: bs
h₂ : b :: bs ≤ a :: as
hab : ¬a < b
hba : b < a
⊢ a :: as = b :: bs

case inr.inr
α : Type u_1
inst✝ : LT α
s : Antisymm fun x x_1 => ¬x < x_1
as✝ bs✝ : List α
a : α
as : List α
b : α
bs : List α
h₁ : a :: as ≤ b :: bs
h₂ : b :: bs ≤ a :: as
hab : ¬a < b
hba : ¬b < a
⊢ a :: as = b :: bs
case inr
α : Type u_1
inst✝ : LT α
s : Antisymm fun x x_1 => ¬x < x_1
as✝ bs✝ : List α
a : α
as : List α
b : α
bs : List α
h₁ : a :: as ≤ b :: bs
h₂ : b :: bs ≤ a :: as
hab : ¬a < b
⊢ a :: as = b :: bs
by_cases hba : b < a
no goals
case inr.inl
α : Type u_1
inst✝ : LT α
s : Antisymm fun x x_1 => ¬x < x_1
as✝ bs✝ : List α
a : α
as : List α
b : α
bs : List α
h₁ : a :: as ≤ b :: bs
h₂ : b :: bs ≤ a :: as
hab : ¬a < b
hba : b < a
⊢ a :: as = b :: bs
exact False.elim <| h₁ (List.lt.head _ _ hba)
case inr.inr
α : Type u_1
inst✝ : LT α
s : Antisymm fun x x_1 => ¬x < x_1
as✝ bs✝ : List α
a : α
as : List α
b : α
bs : List α
h₁✝ : a :: as ≤ b :: bs
h₂ : b :: bs ≤ a :: as
hab : ¬a < b
hba : ¬b < a
h₁ : as ≤ bs
⊢ a :: as = b :: bs
case inr.inr
α : Type u_1
inst✝ : LT α
s : Antisymm fun x x_1 => ¬x < x_1
as✝ bs✝ : List α
a : α
as : List α
b : α
bs : List α
h₁ : a :: as ≤ b :: bs
h₂ : b :: bs ≤ a :: as
hab : ¬a < b
hba : ¬b < a
⊢ a :: as = b :: bs
have h₁ : as ≤ bs := fun h => h₁ (List.lt.tail hba hab h)
case inr.inr
α : Type u_1
inst✝ : LT α
s : Antisymm fun x x_1 => ¬x < x_1
as✝ bs✝ : List α
a : α
as : List α
b : α
bs : List α
h₁✝ : a :: as ≤ b :: bs
h₂✝ : b :: bs ≤ a :: as
hab : ¬a < b
hba : ¬b < a
h₁ : as ≤ bs
h₂ : bs ≤ as
⊢ a :: as = b :: bs
case inr.inr
α : Type u_1
inst✝ : LT α
s : Antisymm fun x x_1 => ¬x < x_1
as✝ bs✝ : List α
a : α
as : List α
b : α
bs : List α
h₁✝ : a :: as ≤ b :: bs
h₂ : b :: bs ≤ a :: as
hab : ¬a < b
hba : ¬b < a
h₁ : as ≤ bs
⊢ a :: as = b :: bs
have h₂ : bs ≤ as := fun h => h₂ (List.lt.tail hab hba h)
case inr.inr
α : Type u_1
inst✝ : LT α
s : Antisymm fun x x_1 => ¬x < x_1
as✝ bs✝ : List α
a : α
as : List α
b : α
bs : List α
h₁✝ : a :: as ≤ b :: bs
h₂✝ : b :: bs ≤ a :: as
hab : ¬a < b
hba : ¬b < a
h₁ : as ≤ bs
h₂ : bs ≤ as
ih : as = bs
⊢ a :: as = b :: bs
case inr.inr
α : Type u_1
inst✝ : LT α
s : Antisymm fun x x_1 => ¬x < x_1
as✝ bs✝ : List α
a : α
as : List α
b : α
bs : List α
h₁✝ : a :: as ≤ b :: bs
h₂✝ : b :: bs ≤ a :: as
hab : ¬a < b
hba : ¬b < a
h₁ : as ≤ bs
h₂ : bs ≤ as
⊢ a :: as = b :: bs
have ih : as = bs := le_antisymm h₁ h₂
case inr.inr
α : Type u_1
inst✝ : LT α
s : Antisymm fun x x_1 => ¬x < x_1
as✝ bs✝ : List α
a : α
as : List α
b : α
bs : List α
h₁✝ : a :: as ≤ b :: bs
h₂✝ : b :: bs ≤ a :: as
hab : ¬a < b
hba : ¬b < a
h₁ : as ≤ bs
h₂ : bs ≤ as
ih : as = bs
this : a = b
⊢ a :: as = b :: bs
case inr.inr
α : Type u_1
inst✝ : LT α
s : Antisymm fun x x_1 => ¬x < x_1
as✝ bs✝ : List α
a : α
as : List α
b : α
bs : List α
h₁✝ : a :: as ≤ b :: bs
h₂✝ : b :: bs ≤ a :: as
hab : ¬a < b
hba : ¬b < a
h₁ : as ≤ bs
h₂ : bs ≤ as
ih : as = bs
⊢ a :: as = b :: bs
have : a = b := s.antisymm hab hba
no goals
case inr.inr
α : Type u_1
inst✝ : LT α
s : Antisymm fun x x_1 => ¬x < x_1
as✝ bs✝ : List α
a : α
as : List α
b : α
bs : List α
h₁✝ : a :: as ≤ b :: bs
h₂✝ : b :: bs ≤ a :: as
hab : ¬a < b
hba : ¬b < a
h₁ : as ≤ bs
h₂ : bs ≤ as
ih : as = bs
this : a = b
⊢ a :: as = b :: bs
simp [this, ih]