-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/BasicAux.lean
theorem not_lex_antisymm [DecidableEq α] {r : α → α → Prop} [DecidableRel r]
    (antisymm : ∀ x y : α, ¬ r x y → ¬ r y x → x = y)
    {as bs : List α} (h₁ : ¬ Lex r bs as) (h₂ : ¬ Lex r as bs) : as = bs :=
  match as, bs with
  | [],    []    => rfl
  | [],    _::_ => False.elim <| h₂ (List.Lex.nil ..)
  | _::_, []    => False.elim <| h₁ (List.Lex.nil ..)
  | a::as, b::bs => by
    by_cases hab : r a b
    · exact False.elim <| h₂ (List.Lex.rel hab)
    · by_cases eq : a = b
      · subst eq
        have h₁ : ¬ Lex r bs as := fun h => h₁ (List.Lex.cons h)
        have h₂ : ¬ Lex r as bs := fun h => h₂ (List.Lex.cons h)
        simp [not_lex_antisymm antisymm h₁ h₂]
      · exfalso
        by_cases hba : r b a
        · exact h₁ (Lex.rel hba)
        · exact eq (antisymm _ _ hab hba)

Proof state:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : DecidableRel r
antisymm : ∀ (x y : α), ¬r x y → ¬r y x → x = y
as✝ bs✝ : List α
a : α
as bs : List α
h₁✝ : ¬Lex r (a :: bs) (a :: as)
h₂ : ¬Lex r (a :: as) (a :: bs)
hab : ¬r a a
h₁ : ¬Lex r bs as
⊢ a :: as = a :: bs

Tactic:
have h₂ : ¬ Lex r as bs := fun h => h₂ (List.Lex.cons h)

Result:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : DecidableRel r
antisymm : ∀ (x y : α), ¬r x y → ¬r y x → x = y
as✝ bs✝ : List α
a : α
as bs : List α
h₁✝ : ¬Lex r (a :: bs) (a :: as)
h₂✝ : ¬Lex r (a :: as) (a :: bs)
hab : ¬r a a
h₁ : ¬Lex r bs as
h₂ : ¬Lex r as bs
⊢ a :: as = a :: bs

Proof state:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : DecidableRel r
antisymm : ∀ (x y : α), ¬r x y → ¬r y x → x = y
as✝ bs✝ : List α
a : α
as : List α
b : α
bs : List α
h₁ : ¬Lex r (b :: bs) (a :: as)
h₂ : ¬Lex r (a :: as) (b :: bs)
hab : ¬r a b
eq : ¬a = b
⊢ a :: as = b :: bs

Tactic:
exfalso

Result:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : DecidableRel r
antisymm : ∀ (x y : α), ¬r x y → ¬r y x → x = y
as✝ bs✝ : List α
a : α
as : List α
b : α
bs : List α
h₁ : ¬Lex r (b :: bs) (a :: as)
h₂ : ¬Lex r (a :: as) (b :: bs)
hab : ¬r a b
eq : ¬a = b
⊢ False

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : DecidableRel r
antisymm : ∀ (x y : α), ¬r x y → ¬r y x → x = y
as✝ bs✝ : List α
a : α
as : List α
b : α
bs : List α
h₁ : ¬Lex r (b :: bs) (a :: as)
h₂ : ¬Lex r (a :: as) (b :: bs)
⊢ a :: as = b :: bs

Tactic:
by_cases hab : r a b

Result:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : DecidableRel r
antisymm : ∀ (x y : α), ¬r x y → ¬r y x → x = y
as✝ bs✝ : List α
a : α
as : List α
b : α
bs : List α
h₁ : ¬Lex r (b :: bs) (a :: as)
h₂ : ¬Lex r (a :: as) (b :: bs)
hab : r a b
⊢ a :: as = b :: bs

case neg
α : Type u_1
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : DecidableRel r
antisymm : ∀ (x y : α), ¬r x y → ¬r y x → x = y
as✝ bs✝ : List α
a : α
as : List α
b : α
bs : List α
h₁ : ¬Lex r (b :: bs) (a :: as)
h₂ : ¬Lex r (a :: as) (b :: bs)
hab : ¬r a b
⊢ a :: as = b :: bs

Proof state:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : DecidableRel r
antisymm : ∀ (x y : α), ¬r x y → ¬r y x → x = y
as✝ bs✝ : List α
a : α
as : List α
b : α
bs : List α
h₁ : ¬Lex r (b :: bs) (a :: as)
h₂ : ¬Lex r (a :: as) (b :: bs)
hab : ¬r a b
⊢ a :: as = b :: bs

Tactic:
by_cases eq : a = b

Result:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : DecidableRel r
antisymm : ∀ (x y : α), ¬r x y → ¬r y x → x = y
as✝ bs✝ : List α
a : α
as : List α
b : α
bs : List α
h₁ : ¬Lex r (b :: bs) (a :: as)
h₂ : ¬Lex r (a :: as) (b :: bs)
hab : ¬r a b
eq : a = b
⊢ a :: as = b :: bs

case neg
α : Type u_1
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : DecidableRel r
antisymm : ∀ (x y : α), ¬r x y → ¬r y x → x = y
as✝ bs✝ : List α
a : α
as : List α
b : α
bs : List α
h₁ : ¬Lex r (b :: bs) (a :: as)
h₂ : ¬Lex r (a :: as) (b :: bs)
hab : ¬r a b
eq : ¬a = b
⊢ a :: as = b :: bs

Proof state:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : DecidableRel r
antisymm : ∀ (x y : α), ¬r x y → ¬r y x → x = y
as✝ bs✝ : List α
a : α
as : List α
b : α
bs : List α
h₁ : ¬Lex r (b :: bs) (a :: as)
h₂ : ¬Lex r (a :: as) (b :: bs)
hab : ¬r a b
eq : a = b
⊢ a :: as = b :: bs

Tactic:
subst eq

Result:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : DecidableRel r
antisymm : ∀ (x y : α), ¬r x y → ¬r y x → x = y
as✝ bs✝ : List α
a : α
as bs : List α
h₁ : ¬Lex r (a :: bs) (a :: as)
h₂ : ¬Lex r (a :: as) (a :: bs)
hab : ¬r a a
⊢ a :: as = a :: bs

Proof state:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : DecidableRel r
antisymm : ∀ (x y : α), ¬r x y → ¬r y x → x = y
as✝ bs✝ : List α
a : α
as : List α
b : α
bs : List α
h₁ : ¬Lex r (b :: bs) (a :: as)
h₂ : ¬Lex r (a :: as) (b :: bs)
hab : ¬r a b
eq : ¬a = b
⊢ False

Tactic:
by_cases hba : r b a

Result:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : DecidableRel r
antisymm : ∀ (x y : α), ¬r x y → ¬r y x → x = y
as✝ bs✝ : List α
a : α
as : List α
b : α
bs : List α
h₁ : ¬Lex r (b :: bs) (a :: as)
h₂ : ¬Lex r (a :: as) (b :: bs)
hab : ¬r a b
eq : ¬a = b
hba : r b a
⊢ False

case neg
α : Type u_1
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : DecidableRel r
antisymm : ∀ (x y : α), ¬r x y → ¬r y x → x = y
as✝ bs✝ : List α
a : α
as : List α
b : α
bs : List α
h₁ : ¬Lex r (b :: bs) (a :: as)
h₂ : ¬Lex r (a :: as) (b :: bs)
hab : ¬r a b
eq : ¬a = b
hba : ¬r b a
⊢ False

Proof state:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : DecidableRel r
antisymm : ∀ (x y : α), ¬r x y → ¬r y x → x = y
as✝ bs✝ : List α
a : α
as bs : List α
h₁✝ : ¬Lex r (a :: bs) (a :: as)
h₂✝ : ¬Lex r (a :: as) (a :: bs)
hab : ¬r a a
h₁ : ¬Lex r bs as
h₂ : ¬Lex r as bs
⊢ a :: as = a :: bs

Tactic:
simp [not_lex_antisymm antisymm h₁ h₂]

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : DecidableRel r
antisymm : ∀ (x y : α), ¬r x y → ¬r y x → x = y
as✝ bs✝ : List α
a : α
as : List α
b : α
bs : List α
h₁ : ¬Lex r (b :: bs) (a :: as)
h₂ : ¬Lex r (a :: as) (b :: bs)
hab : ¬r a b
eq : ¬a = b
hba : ¬r b a
⊢ False

Tactic:
exact eq (antisymm _ _ hab hba)

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : DecidableRel r
antisymm : ∀ (x y : α), ¬r x y → ¬r y x → x = y
as✝ bs✝ : List α
a : α
as bs : List α
h₁ : ¬Lex r (a :: bs) (a :: as)
h₂ : ¬Lex r (a :: as) (a :: bs)
hab : ¬r a a
⊢ a :: as = a :: bs

Tactic:
have h₁ : ¬ Lex r bs as := fun h => h₁ (List.Lex.cons h)

Result:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : DecidableRel r
antisymm : ∀ (x y : α), ¬r x y → ¬r y x → x = y
as✝ bs✝ : List α
a : α
as bs : List α
h₁✝ : ¬Lex r (a :: bs) (a :: as)
h₂ : ¬Lex r (a :: as) (a :: bs)
hab : ¬r a a
h₁ : ¬Lex r bs as
⊢ a :: as = a :: bs

Proof state:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : DecidableRel r
antisymm : ∀ (x y : α), ¬r x y → ¬r y x → x = y
as✝ bs✝ : List α
a : α
as : List α
b : α
bs : List α
h₁ : ¬Lex r (b :: bs) (a :: as)
h₂ : ¬Lex r (a :: as) (b :: bs)
hab : r a b
⊢ a :: as = b :: bs

Tactic:
exact False.elim <| h₂ (List.Lex.rel hab)

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : DecidableRel r
antisymm : ∀ (x y : α), ¬r x y → ¬r y x → x = y
as✝ bs✝ : List α
a : α
as : List α
b : α
bs : List α
h₁ : ¬Lex r (b :: bs) (a :: as)
h₂ : ¬Lex r (a :: as) (b :: bs)
hab : ¬r a b
eq : ¬a = b
hba : r b a
⊢ False

Tactic:
exact h₁ (Lex.rel hba)

Result:
no goals