Theorem: Notes.totally_ordered_of_sorted (Notes4/IndPred2.lean)

State before:
α : Type
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Trans r r r
inst✝ : Transitive r
l : List α
h : Sorted r l
i✝ j✝ : ℕ
x✝¹ : i✝ < j✝
h' : i✝ < List.length []
x✝ : j✝ < List.length []
⊢ False
Tactic:
rw [List.length_nil] at h'
State after:
α : Type
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Trans r r r
inst✝ : Transitive r
l : List α
h : Sorted r l
i✝ j✝ : ℕ
x✝¹ : i✝ < j✝
h' : i✝ < 0
x✝ : j✝ < List.length []
⊢ False

State before:
α : Type
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Trans r r r
inst✝ : Transitive r
l : List α
h : Sorted r l
i✝ j✝ : ℕ
x✝¹ : i✝ < j✝
h' : i✝ < 0
x✝ : j✝ < List.length []
⊢ False
Tactic:
exact Nat.not_lt_zero _ h'
State after:
no goals

State before:
α : Type
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Trans r r r
inst✝ : Transitive r
l : List α
h✝ : Sorted r l
i✝ j✝ : ℕ
a✝ : α
h : i✝ < j✝
hi : i✝ < List.length [a✝]
hj : j✝ < List.length [a✝]
⊢ r [a✝][i✝] [a✝][j✝]
Tactic:
dsimp at hi hj
State after:
α : Type
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Trans r r r
inst✝ : Transitive r
l : List α
h✝ : Sorted r l
i✝ j✝ : ℕ
a✝ : α
h : i✝ < j✝
hi : i✝ < 1
hj : j✝ < 1
⊢ r [a✝][i✝] [a✝][j✝]

State before:
α : Type
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Trans r r r
inst✝ : Transitive r
l : List α
h✝ : Sorted r l
i✝ j✝ : ℕ
a✝ : α
h : i✝ < j✝
hi : i✝ < 1
hj : j✝ < 1
⊢ r [a✝][i✝] [a✝][j✝]
Tactic:
apply False.elim
State after:
case h
α : Type
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Trans r r r
inst✝ : Transitive r
l : List α
h✝ : Sorted r l
i✝ j✝ : ℕ
a✝ : α
h : i✝ < j✝
hi : i✝ < 1
hj : j✝ < 1
⊢ False

State before:
case h
α : Type
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Trans r r r
inst✝ : Transitive r
l : List α
h✝ : Sorted r l
i✝ j✝ : ℕ
a✝ : α
h : i✝ < j✝
hi : i✝ < 1
hj : j✝ < 1
⊢ False
Tactic:
linarith
State after:
no goals

State before:
α : Type
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Trans r r r
inst✝ : Transitive r
l : List α
h : Sorted r l
i✝ j✝ : ℕ
a₁✝ a₂✝ : α
as✝ : List α
h₁ : r a₁✝ a₂✝
h₂ : Sorted r (a₂✝ :: as✝)
⊢ i✝ < j✝ →
    ∀ (x : i✝ < List.length (a₁✝ :: a₂✝ :: as✝)) (x_1 : j✝ < List.length (a₁✝ :: a₂✝ :: as✝)),
      r (a₁✝ :: a₂✝ :: as✝)[i✝] (a₁✝ :: a₂✝ :: as✝)[j✝]
Tactic:
intro h' hi hj
State after:
α : Type
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Trans r r r
inst✝ : Transitive r
l : List α
h : Sorted r l
i✝ j✝ : ℕ
a₁✝ a₂✝ : α
as✝ : List α
h₁ : r a₁✝ a₂✝
h₂ : Sorted r (a₂✝ :: as✝)
h' : i✝ < j✝
hi : i✝ < List.length (a₁✝ :: a₂✝ :: as✝)
hj : j✝ < List.length (a₁✝ :: a₂✝ :: as✝)
⊢ r (a₁✝ :: a₂✝ :: as✝)[i✝] (a₁✝ :: a₂✝ :: as✝)[j✝]

State before:
α : Type
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Trans r r r
inst✝ : Transitive r
l : List α
h : Sorted r l
i✝ j✝ : ℕ
a₁✝ a₂✝ : α
as✝ : List α
h₁ : r a₁✝ a₂✝
h₂ : Sorted r (a₂✝ :: as✝)
h' : i✝ < j✝
hi : i✝ < List.length (a₁✝ :: a₂✝ :: as✝)
hj : j✝ < List.length (a₁✝ :: a₂✝ :: as✝)
⊢ r (a₁✝ :: a₂✝ :: as✝)[i✝] (a₁✝ :: a₂✝ :: as✝)[j✝]
Tactic:
rename_i i j a₁ a₂ as
State after:
α : Type
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Trans r r r
inst✝ : Transitive r
l : List α
h : Sorted r l
i j : ℕ
a₁ a₂ : α
as : List α
h₁ : r a₁ a₂
h₂ : Sorted r (a₂ :: as)
h' : i < j
hi : i < List.length (a₁ :: a₂ :: as)
hj : j < List.length (a₁ :: a₂ :: as)
⊢ r (a₁ :: a₂ :: as)[i] (a₁ :: a₂ :: as)[j]

State before:
α : Type
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Trans r r r
inst✝ : Transitive r
l : List α
h : Sorted r l
i j : ℕ
a₁ a₂ : α
as : List α
h₁ : r a₁ a₂
h₂ : Sorted r (a₂ :: as)
h' : i < j
hi : i < List.length (a₁ :: a₂ :: as)
hj : j < List.length (a₁ :: a₂ :: as)
⊢ r (a₁ :: a₂ :: as)[i] (a₁ :: a₂ :: as)[j]
Tactic:
have ⟨l,hl⟩ := Nat.succ_of_lt h'
State after:
α : Type
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Trans r r r
inst✝ : Transitive r
l✝ : List α
h : Sorted r l✝
i j : ℕ
a₁ a₂ : α
as : List α
h₁ : r a₁ a₂
h₂ : Sorted r (a₂ :: as)
h' : i < j
hi : i < List.length (a₁ :: a₂ :: as)
hj : j < List.length (a₁ :: a₂ :: as)
l : ℕ
hl : l + 1 = j
⊢ r (a₁ :: a₂ :: as)[i] (a₁ :: a₂ :: as)[j]

State before:
α : Type
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Trans r r r
inst✝ : Transitive r
l✝ : List α
h : Sorted r l✝
i j : ℕ
a₁ a₂ : α
as : List α
h₁ : r a₁ a₂
h₂ : Sorted r (a₂ :: as)
h' : i < j
hi : i < List.length (a₁ :: a₂ :: as)
hj : j < List.length (a₁ :: a₂ :: as)
l : ℕ
hl : l + 1 = j
⊢ r (a₁ :: a₂ :: as)[i] (a₁ :: a₂ :: as)[j]
Tactic:
rw [←hl] at hj h'
State after:
α : Type
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Trans r r r
inst✝ : Transitive r
l✝ : List α
h : Sorted r l✝
i j : ℕ
a₁ a₂ : α
as : List α
h₁ : r a₁ a₂
h₂ : Sorted r (a₂ :: as)
hi : i < List.length (a₁ :: a₂ :: as)
hj✝ : j < List.length (a₁ :: a₂ :: as)
l : ℕ
h' : i < l + 1
hj : l + 1 < List.length (a₁ :: a₂ :: as)
hl : l + 1 = j
⊢ r (a₁ :: a₂ :: as)[i] (a₁ :: a₂ :: as)[j]

State before:
α : Type
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Trans r r r
inst✝ : Transitive r
l✝ : List α
h : Sorted r l✝
i j : ℕ
a₁ a₂ : α
as : List α
h₁ : r a₁ a₂
h₂ : Sorted r (a₂ :: as)
hi : i < List.length (a₁ :: a₂ :: as)
hj✝ : j < List.length (a₁ :: a₂ :: as)
l : ℕ
h' : i < l + 1
hj : l + 1 < List.length (a₁ :: a₂ :: as)
hl : l + 1 = j
⊢ r (a₁ :: a₂ :: as)[i] (a₁ :: a₂ :: as)[j]
Tactic:
simp only [←hl]
State after:
α : Type
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Trans r r r
inst✝ : Transitive r
l✝ : List α
h : Sorted r l✝
i j : ℕ
a₁ a₂ : α
as : List α
h₁ : r a₁ a₂
h₂ : Sorted r (a₂ :: as)
hi : i < List.length (a₁ :: a₂ :: as)
hj✝ : j < List.length (a₁ :: a₂ :: as)
l : ℕ
h' : i < l + 1
hj : l + 1 < List.length (a₁ :: a₂ :: as)
hl : l + 1 = j
⊢ r (a₁ :: a₂ :: as)[i] (a₁ :: a₂ :: as)[l + 1]

State before:
α : Type
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Trans r r r
inst✝ : Transitive r
l✝ : List α
h : Sorted r l✝
i j : ℕ
a₁ a₂ : α
as : List α
h₁ : r a₁ a₂
h₂ : Sorted r (a₂ :: as)
hi : i < List.length (a₁ :: a₂ :: as)
hj✝ : j < List.length (a₁ :: a₂ :: as)
l : ℕ
h' : i < l + 1
hj : l + 1 < List.length (a₁ :: a₂ :: as)
hl : l + 1 = j
⊢ r (a₁ :: a₂ :: as)[i] (a₁ :: a₂ :: as)[l + 1]
Tactic:
have : l < (a₂ :: as).length := 
  Nat.pred_lt_pred (by simp) hj
State after:
α : Type
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Trans r r r
inst✝ : Transitive r
l✝ : List α
h : Sorted r l✝
i j : ℕ
a₁ a₂ : α
as : List α
h₁ : r a₁ a₂
h₂ : Sorted r (a₂ :: as)
hi : i < List.length (a₁ :: a₂ :: as)
hj✝ : j < List.length (a₁ :: a₂ :: as)
l : ℕ
h' : i < l + 1
hj : l + 1 < List.length (a₁ :: a₂ :: as)
hl : l + 1 = j
this : l < List.length (a₂ :: as)
⊢ r (a₁ :: a₂ :: as)[i] (a₁ :: a₂ :: as)[l + 1]

State before:
α : Type
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Trans r r r
inst✝ : Transitive r
l✝ : List α
h : Sorted r l✝
i j : ℕ
a₁ a₂ : α
as : List α
h₁ : r a₁ a₂
h₂ : Sorted r (a₂ :: as)
hi : i < List.length (a₁ :: a₂ :: as)
hj✝ : j < List.length (a₁ :: a₂ :: as)
l : ℕ
h' : i < l + 1
hj : l + 1 < List.length (a₁ :: a₂ :: as)
hl : l + 1 = j
this : l < List.length (a₂ :: as)
⊢ r (a₁ :: a₂ :: as)[i] (a₁ :: a₂ :: as)[l + 1]
Tactic:
have hl' : (a₁::a₂::as)[l+1] = (a₂::as)[l] := rfl
State after:
α : Type
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Trans r r r
inst✝ : Transitive r
l✝ : List α
h : Sorted r l✝
i j : ℕ
a₁ a₂ : α
as : List α
h₁ : r a₁ a₂
h₂ : Sorted r (a₂ :: as)
hi : i < List.length (a₁ :: a₂ :: as)
hj✝ : j < List.length (a₁ :: a₂ :: as)
l : ℕ
h' : i < l + 1
hj : l + 1 < List.length (a₁ :: a₂ :: as)
hl : l + 1 = j
this : l < List.length (a₂ :: as)
hl' : (a₁ :: a₂ :: as)[l + 1] = (a₂ :: as)[l]
⊢ r (a₁ :: a₂ :: as)[i] (a₁ :: a₂ :: as)[l + 1]

State before:
α : Type
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Trans r r r
inst✝ : Transitive r
l✝ : List α
h : Sorted r l✝
i j : ℕ
a₁ a₂ : α
as : List α
h₁ : r a₁ a₂
h₂ : Sorted r (a₂ :: as)
hi : i < List.length (a₁ :: a₂ :: as)
hj✝ : j < List.length (a₁ :: a₂ :: as)
l : ℕ
h' : i < l + 1
hj : l + 1 < List.length (a₁ :: a₂ :: as)
hl : l + 1 = j
this : l < List.length (a₂ :: as)
hl' : (a₁ :: a₂ :: as)[l + 1] = (a₂ :: as)[l]
⊢ r (a₁ :: a₂ :: as)[i] (a₁ :: a₂ :: as)[l + 1]
Tactic:
by_cases i = 0
State after:
case pos
α : Type
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Trans r r r
inst✝ : Transitive r
l✝ : List α
h✝ : Sorted r l✝
i j : ℕ
a₁ a₂ : α
as : List α
h₁ : r a₁ a₂
h₂ : Sorted r (a₂ :: as)
hi : i < List.length (a₁ :: a₂ :: as)
hj✝ : j < List.length (a₁ :: a₂ :: as)
l : ℕ
h' : i < l + 1
hj : l + 1 < List.length (a₁ :: a₂ :: as)
hl : l + 1 = j
this : l < List.length (a₂ :: as)
hl' : (a₁ :: a₂ :: as)[l + 1] = (a₂ :: as)[l]
h : i = 0
⊢ r (a₁ :: a₂ :: as)[i] (a₁ :: a₂ :: as)[l + 1]

case neg
α : Type
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Trans r r r
inst✝ : Transitive r
l✝ : List α
h✝ : Sorted r l✝
i j : ℕ
a₁ a₂ : α
as : List α
h₁ : r a₁ a₂
h₂ : Sorted r (a₂ :: as)
hi : i < List.length (a₁ :: a₂ :: as)
hj✝ : j < List.length (a₁ :: a₂ :: as)
l : ℕ
h' : i < l + 1
hj : l + 1 < List.length (a₁ :: a₂ :: as)
hl : l + 1 = j
this : l < List.length (a₂ :: as)
hl' : (a₁ :: a₂ :: as)[l + 1] = (a₂ :: as)[l]
h : ¬i = 0
⊢ r (a₁ :: a₂ :: as)[i] (a₁ :: a₂ :: as)[l + 1]

State before:
α : Type
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Trans r r r
inst✝ : Transitive r
l✝ : List α
h : Sorted r l✝
i j : ℕ
a₁ a₂ : α
as : List α
h₁ : r a₁ a₂
h₂ : Sorted r (a₂ :: as)
hi : i < List.length (a₁ :: a₂ :: as)
hj✝ : j < List.length (a₁ :: a₂ :: as)
l : ℕ
h' : i < l + 1
hj : l + 1 < List.length (a₁ :: a₂ :: as)
hl : l + 1 = j
⊢ l + 1 ≠ 0
Tactic:
simp
State after:
no goals

State before:
case pos
α : Type
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Trans r r r
inst✝ : Transitive r
l✝ : List α
h✝ : Sorted r l✝
i j : ℕ
a₁ a₂ : α
as : List α
h₁ : r a₁ a₂
h₂ : Sorted r (a₂ :: as)
hi : i < List.length (a₁ :: a₂ :: as)
hj✝ : j < List.length (a₁ :: a₂ :: as)
l : ℕ
h' : i < l + 1
hj : l + 1 < List.length (a₁ :: a₂ :: as)
hl : l + 1 = j
this : l < List.length (a₂ :: as)
hl' : (a₁ :: a₂ :: as)[l + 1] = (a₂ :: as)[l]
h : i = 0
⊢ r (a₁ :: a₂ :: as)[i] (a₁ :: a₂ :: as)[l + 1]
Tactic:
simp [h,hl'] at *
State after:
case pos
α : Type
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Trans r r r
inst✝ : Transitive r
l✝ : List α
h✝ : Sorted r l✝
i j : ℕ
a₁ a₂ : α
as : List α
h₁ : r a₁ a₂
h₂ : Sorted r (a₂ :: as)
hi : i < List.length (a₁ :: a₂ :: as)
hj✝ : j < List.length (a₁ :: a₂ :: as)
l : ℕ
hj : l + 1 < List.length (a₁ :: a₂ :: as)
hl : l + 1 = j
this : l < List.length (a₂ :: as)
h' hl' h : True
⊢ r a₁ (List.get (a₂ :: as) { val := l, isLt := (_ : l < List.length (a₂ :: as)) })

State before:
case pos
α : Type
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Trans r r r
inst✝ : Transitive r
l✝ : List α
h✝ : Sorted r l✝
i j : ℕ
a₁ a₂ : α
as : List α
h₁ : r a₁ a₂
h₂ : Sorted r (a₂ :: as)
hi : i < List.length (a₁ :: a₂ :: as)
hj✝ : j < List.length (a₁ :: a₂ :: as)
l : ℕ
hj : l + 1 < List.length (a₁ :: a₂ :: as)
hl : l + 1 = j
this : l < List.length (a₂ :: as)
h' hl' h : True
⊢ r a₁ (List.get (a₂ :: as) { val := l, isLt := (_ : l < List.length (a₂ :: as)) })
Tactic:
by_cases l = 0
State after:
case pos
α : Type
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Trans r r r
inst✝ : Transitive r
l✝ : List α
h✝¹ : Sorted r l✝
i j : ℕ
a₁ a₂ : α
as : List α
h₁ : r a₁ a₂
h₂ : Sorted r (a₂ :: as)
hi : i < List.length (a₁ :: a₂ :: as)
hj✝ : j < List.length (a₁ :: a₂ :: as)
l : ℕ
hj : l + 1 < List.length (a₁ :: a₂ :: as)
hl : l + 1 = j
this : l < List.length (a₂ :: as)
h' hl' h✝ : True
h : l = 0
⊢ r a₁ (List.get (a₂ :: as) { val := l, isLt := (_ : l < List.length (a₂ :: as)) })

case neg
α : Type
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Trans r r r
inst✝ : Transitive r
l✝ : List α
h✝¹ : Sorted r l✝
i j : ℕ
a₁ a₂ : α
as : List α
h₁ : r a₁ a₂
h₂ : Sorted r (a₂ :: as)
hi : i < List.length (a₁ :: a₂ :: as)
hj✝ : j < List.length (a₁ :: a₂ :: as)
l : ℕ
hj : l + 1 < List.length (a₁ :: a₂ :: as)
hl : l + 1 = j
this : l < List.length (a₂ :: as)
h' hl' h✝ : True
h : ¬l = 0
⊢ r a₁ (List.get (a₂ :: as) { val := l, isLt := (_ : l < List.length (a₂ :: as)) })

State before:
case pos
α : Type
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Trans r r r
inst✝ : Transitive r
l✝ : List α
h✝¹ : Sorted r l✝
i j : ℕ
a₁ a₂ : α
as : List α
h₁ : r a₁ a₂
h₂ : Sorted r (a₂ :: as)
hi : i < List.length (a₁ :: a₂ :: as)
hj✝ : j < List.length (a₁ :: a₂ :: as)
l : ℕ
hj : l + 1 < List.length (a₁ :: a₂ :: as)
hl : l + 1 = j
this : l < List.length (a₂ :: as)
h' hl' h✝ : True
h : l = 0
⊢ r a₁ (List.get (a₂ :: as) { val := l, isLt := (_ : l < List.length (a₂ :: as)) })
Tactic:
simp [h,h₁]
State after:
no goals

State before:
case neg
α : Type
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Trans r r r
inst✝ : Transitive r
l✝ : List α
h✝¹ : Sorted r l✝
i j : ℕ
a₁ a₂ : α
as : List α
h₁ : r a₁ a₂
h₂ : Sorted r (a₂ :: as)
hi : i < List.length (a₁ :: a₂ :: as)
hj✝ : j < List.length (a₁ :: a₂ :: as)
l : ℕ
hj : l + 1 < List.length (a₁ :: a₂ :: as)
hl : l + 1 = j
this : l < List.length (a₂ :: as)
h' hl' h✝ : True
h : ¬l = 0
⊢ r a₁ (List.get (a₂ :: as) { val := l, isLt := (_ : l < List.length (a₂ :: as)) })
Tactic:
apply trans'
State after:
case neg.a
α : Type
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Trans r r r
inst✝ : Transitive r
l✝ : List α
h✝¹ : Sorted r l✝
i j : ℕ
a₁ a₂ : α
as : List α
h₁ : r a₁ a₂
h₂ : Sorted r (a₂ :: as)
hi : i < List.length (a₁ :: a₂ :: as)
hj✝ : j < List.length (a₁ :: a₂ :: as)
l : ℕ
hj : l + 1 < List.length (a₁ :: a₂ :: as)
hl : l + 1 = j
this : l < List.length (a₂ :: as)
h' hl' h✝ : True
h : ¬l = 0
⊢ r a₁ ?neg.a₂✝

case neg.a
α : Type
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Trans r r r
inst✝ : Transitive r
l✝ : List α
h✝¹ : Sorted r l✝
i j : ℕ
a₁ a₂ : α
as : List α
h₁ : r a₁ a₂
h₂ : Sorted r (a₂ :: as)
hi : i < List.length (a₁ :: a₂ :: as)
hj✝ : j < List.length (a₁ :: a₂ :: as)
l : ℕ
hj : l + 1 < List.length (a₁ :: a₂ :: as)
hl : l + 1 = j
this : l < List.length (a₂ :: as)
h' hl' h✝ : True
h : ¬l = 0
⊢ r ?neg.a₂✝ (List.get (a₂ :: as) { val := l, isLt := (_ : l < List.length (a₂ :: as)) })

case neg.a₂
α : Type
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Trans r r r
inst✝ : Transitive r
l✝ : List α
h✝¹ : Sorted r l✝
i j : ℕ
a₁ a₂ : α
as : List α
h₁ : r a₁ a₂
h₂ : Sorted r (a₂ :: as)
hi : i < List.length (a₁ :: a₂ :: as)
hj✝ : j < List.length (a₁ :: a₂ :: as)
l : ℕ
hj : l + 1 < List.length (a₁ :: a₂ :: as)
hl : l + 1 = j
this : l < List.length (a₂ :: as)
h' hl' h✝ : True
h : ¬l = 0
⊢ α

State before:
case neg.a
α : Type
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Trans r r r
inst✝ : Transitive r
l✝ : List α
h✝¹ : Sorted r l✝
i j : ℕ
a₁ a₂ : α
as : List α
h₁ : r a₁ a₂
h₂ : Sorted r (a₂ :: as)
hi : i < List.length (a₁ :: a₂ :: as)
hj✝ : j < List.length (a₁ :: a₂ :: as)
l : ℕ
hj : l + 1 < List.length (a₁ :: a₂ :: as)
hl : l + 1 = j
this : l < List.length (a₂ :: as)
h' hl' h✝ : True
h : ¬l = 0
⊢ r a₁ ?neg.a₂✝

case neg.a
α : Type
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Trans r r r
inst✝ : Transitive r
l✝ : List α
h✝¹ : Sorted r l✝
i j : ℕ
a₁ a₂ : α
as : List α
h₁ : r a₁ a₂
h₂ : Sorted r (a₂ :: as)
hi : i < List.length (a₁ :: a₂ :: as)
hj✝ : j < List.length (a₁ :: a₂ :: as)
l : ℕ
hj : l + 1 < List.length (a₁ :: a₂ :: as)
hl : l + 1 = j
this : l < List.length (a₂ :: as)
h' hl' h✝ : True
h : ¬l = 0
⊢ r ?neg.a₂✝ (List.get (a₂ :: as) { val := l, isLt := (_ : l < List.length (a₂ :: as)) })

case neg.a₂
α : Type
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Trans r r r
inst✝ : Transitive r
l✝ : List α
h✝¹ : Sorted r l✝
i j : ℕ
a₁ a₂ : α
as : List α
h₁ : r a₁ a₂
h₂ : Sorted r (a₂ :: as)
hi : i < List.length (a₁ :: a₂ :: as)
hj✝ : j < List.length (a₁ :: a₂ :: as)
l : ℕ
hj : l + 1 < List.length (a₁ :: a₂ :: as)
hl : l + 1 = j
this : l < List.length (a₂ :: as)
h' hl' h✝ : True
h : ¬l = 0
⊢ α
Tactic:
. exact h₁
State after:
case neg.a
α : Type
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Trans r r r
inst✝ : Transitive r
l✝ : List α
h✝¹ : Sorted r l✝
i j : ℕ
a₁ a₂ : α
as : List α
h₁ : r a₁ a₂
h₂ : Sorted r (a₂ :: as)
hi : i < List.length (a₁ :: a₂ :: as)
hj✝ : j < List.length (a₁ :: a₂ :: as)
l : ℕ
hj : l + 1 < List.length (a₁ :: a₂ :: as)
hl : l + 1 = j
this : l < List.length (a₂ :: as)
h' hl' h✝ : True
h : ¬l = 0
⊢ r a₂ (List.get (a₂ :: as) { val := l, isLt := (_ : l < List.length (a₂ :: as)) })

State before:
case neg.a
α : Type
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Trans r r r
inst✝ : Transitive r
l✝ : List α
h✝¹ : Sorted r l✝
i j : ℕ
a₁ a₂ : α
as : List α
h₁ : r a₁ a₂
h₂ : Sorted r (a₂ :: as)
hi : i < List.length (a₁ :: a₂ :: as)
hj✝ : j < List.length (a₁ :: a₂ :: as)
l : ℕ
hj : l + 1 < List.length (a₁ :: a₂ :: as)
hl : l + 1 = j
this : l < List.length (a₂ :: as)
h' hl' h✝ : True
h : ¬l = 0
⊢ r a₁ ?neg.a₂✝
Tactic:
exact h₁
State after:
no goals

State before:
case neg.a
α : Type
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Trans r r r
inst✝ : Transitive r
l✝ : List α
h✝¹ : Sorted r l✝
i j : ℕ
a₁ a₂ : α
as : List α
h₁ : r a₁ a₂
h₂ : Sorted r (a₂ :: as)
hi : i < List.length (a₁ :: a₂ :: as)
hj✝ : j < List.length (a₁ :: a₂ :: as)
l : ℕ
hj : l + 1 < List.length (a₁ :: a₂ :: as)
hl : l + 1 = j
this : l < List.length (a₂ :: as)
h' hl' h✝ : True
h : ¬l = 0
⊢ r a₂ (List.get (a₂ :: as) { val := l, isLt := (_ : l < List.length (a₂ :: as)) })
Tactic:
change r (a₂::as)[0] (a₂::as)[l]
State after:
case neg.a
α : Type
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Trans r r r
inst✝ : Transitive r
l✝ : List α
h✝¹ : Sorted r l✝
i j : ℕ
a₁ a₂ : α
as : List α
h₁ : r a₁ a₂
h₂ : Sorted r (a₂ :: as)
hi : i < List.length (a₁ :: a₂ :: as)
hj✝ : j < List.length (a₁ :: a₂ :: as)
l : ℕ
hj : l + 1 < List.length (a₁ :: a₂ :: as)
hl : l + 1 = j
this : l < List.length (a₂ :: as)
h' hl' h✝ : True
h : ¬l = 0
⊢ r (a₂ :: as)[0] (a₂ :: as)[l]

State before:
case neg.a
α : Type
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Trans r r r
inst✝ : Transitive r
l✝ : List α
h✝¹ : Sorted r l✝
i j : ℕ
a₁ a₂ : α
as : List α
h₁ : r a₁ a₂
h₂ : Sorted r (a₂ :: as)
hi : i < List.length (a₁ :: a₂ :: as)
hj✝ : j < List.length (a₁ :: a₂ :: as)
l : ℕ
hj : l + 1 < List.length (a₁ :: a₂ :: as)
hl : l + 1 = j
this : l < List.length (a₂ :: as)
h' hl' h✝ : True
h : ¬l = 0
⊢ r (a₂ :: as)[0] (a₂ :: as)[l]
Tactic:
apply totally_ordered_of_sorted h₂
State after:
case neg.a.a
α : Type
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Trans r r r
inst✝ : Transitive r
l✝ : List α
h✝¹ : Sorted r l✝
i j : ℕ
a₁ a₂ : α
as : List α
h₁ : r a₁ a₂
h₂ : Sorted r (a₂ :: as)
hi : i < List.length (a₁ :: a₂ :: as)
hj✝ : j < List.length (a₁ :: a₂ :: as)
l : ℕ
hj : l + 1 < List.length (a₁ :: a₂ :: as)
hl : l + 1 = j
this : l < List.length (a₂ :: as)
h' hl' h✝ : True
h : ¬l = 0
⊢ 0 < l

State before:
case neg.a.a
α : Type
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Trans r r r
inst✝ : Transitive r
l✝ : List α
h✝¹ : Sorted r l✝
i j : ℕ
a₁ a₂ : α
as : List α
h₁ : r a₁ a₂
h₂ : Sorted r (a₂ :: as)
hi : i < List.length (a₁ :: a₂ :: as)
hj✝ : j < List.length (a₁ :: a₂ :: as)
l : ℕ
hj : l + 1 < List.length (a₁ :: a₂ :: as)
hl : l + 1 = j
this : l < List.length (a₂ :: as)
h' hl' h✝ : True
h : ¬l = 0
⊢ 0 < l
Tactic:
apply Nat.one_le_iff_ne_zero.mpr h
State after:
no goals

State before:
case neg
α : Type
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Trans r r r
inst✝ : Transitive r
l✝ : List α
h✝ : Sorted r l✝
i j : ℕ
a₁ a₂ : α
as : List α
h₁ : r a₁ a₂
h₂ : Sorted r (a₂ :: as)
hi : i < List.length (a₁ :: a₂ :: as)
hj✝ : j < List.length (a₁ :: a₂ :: as)
l : ℕ
h' : i < l + 1
hj : l + 1 < List.length (a₁ :: a₂ :: as)
hl : l + 1 = j
this : l < List.length (a₂ :: as)
hl' : (a₁ :: a₂ :: as)[l + 1] = (a₂ :: as)[l]
h : ¬i = 0
⊢ r (a₁ :: a₂ :: as)[i] (a₁ :: a₂ :: as)[l + 1]
Tactic:
have ⟨k,hk⟩ := Nat.exists_eq_succ_of_ne_zero h
State after:
case neg
α : Type
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Trans r r r
inst✝ : Transitive r
l✝ : List α
h✝ : Sorted r l✝
i j : ℕ
a₁ a₂ : α
as : List α
h₁ : r a₁ a₂
h₂ : Sorted r (a₂ :: as)
hi : i < List.length (a₁ :: a₂ :: as)
hj✝ : j < List.length (a₁ :: a₂ :: as)
l : ℕ
h' : i < l + 1
hj : l + 1 < List.length (a₁ :: a₂ :: as)
hl : l + 1 = j
this : l < List.length (a₂ :: as)
hl' : (a₁ :: a₂ :: as)[l + 1] = (a₂ :: as)[l]
h : ¬i = 0
k : ℕ
hk : i = Nat.succ k
⊢ r (a₁ :: a₂ :: as)[i] (a₁ :: a₂ :: as)[l + 1]

State before:
case neg
α : Type
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Trans r r r
inst✝ : Transitive r
l✝ : List α
h✝ : Sorted r l✝
i j : ℕ
a₁ a₂ : α
as : List α
h₁ : r a₁ a₂
h₂ : Sorted r (a₂ :: as)
hi : i < List.length (a₁ :: a₂ :: as)
hj✝ : j < List.length (a₁ :: a₂ :: as)
l : ℕ
h' : i < l + 1
hj : l + 1 < List.length (a₁ :: a₂ :: as)
hl : l + 1 = j
this : l < List.length (a₂ :: as)
hl' : (a₁ :: a₂ :: as)[l + 1] = (a₂ :: as)[l]
h : ¬i = 0
k : ℕ
hk : i = Nat.succ k
⊢ r (a₁ :: a₂ :: as)[i] (a₁ :: a₂ :: as)[l + 1]
Tactic:
rw [hk] at hi h'
State after:
case neg
α : Type
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Trans r r r
inst✝ : Transitive r
l✝ : List α
h✝ : Sorted r l✝
i j : ℕ
a₁ a₂ : α
as : List α
h₁ : r a₁ a₂
h₂ : Sorted r (a₂ :: as)
hi✝ : i < List.length (a₁ :: a₂ :: as)
hj✝ : j < List.length (a₁ :: a₂ :: as)
l : ℕ
hj : l + 1 < List.length (a₁ :: a₂ :: as)
hl : l + 1 = j
this : l < List.length (a₂ :: as)
hl' : (a₁ :: a₂ :: as)[l + 1] = (a₂ :: as)[l]
h : ¬i = 0
k : ℕ
h' : Nat.succ k < l + 1
hi : Nat.succ k < List.length (a₁ :: a₂ :: as)
hk : i = Nat.succ k
⊢ r (a₁ :: a₂ :: as)[i] (a₁ :: a₂ :: as)[l + 1]

State before:
case neg
α : Type
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Trans r r r
inst✝ : Transitive r
l✝ : List α
h✝ : Sorted r l✝
i j : ℕ
a₁ a₂ : α
as : List α
h₁ : r a₁ a₂
h₂ : Sorted r (a₂ :: as)
hi✝ : i < List.length (a₁ :: a₂ :: as)
hj✝ : j < List.length (a₁ :: a₂ :: as)
l : ℕ
hj : l + 1 < List.length (a₁ :: a₂ :: as)
hl : l + 1 = j
this : l < List.length (a₂ :: as)
hl' : (a₁ :: a₂ :: as)[l + 1] = (a₂ :: as)[l]
h : ¬i = 0
k : ℕ
h' : Nat.succ k < l + 1
hi : Nat.succ k < List.length (a₁ :: a₂ :: as)
hk : i = Nat.succ k
⊢ r (a₁ :: a₂ :: as)[i] (a₁ :: a₂ :: as)[l + 1]
Tactic:
simp only [hk]
State after:
case neg
α : Type
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Trans r r r
inst✝ : Transitive r
l✝ : List α
h✝ : Sorted r l✝
i j : ℕ
a₁ a₂ : α
as : List α
h₁ : r a₁ a₂
h₂ : Sorted r (a₂ :: as)
hi✝ : i < List.length (a₁ :: a₂ :: as)
hj✝ : j < List.length (a₁ :: a₂ :: as)
l : ℕ
hj : l + 1 < List.length (a₁ :: a₂ :: as)
hl : l + 1 = j
this : l < List.length (a₂ :: as)
hl' : (a₁ :: a₂ :: as)[l + 1] = (a₂ :: as)[l]
h : ¬i = 0
k : ℕ
h' : Nat.succ k < l + 1
hi : Nat.succ k < List.length (a₁ :: a₂ :: as)
hk : i = Nat.succ k
⊢ r (a₁ :: a₂ :: as)[Nat.succ k] (a₁ :: a₂ :: as)[l + 1]

State before:
case neg
α : Type
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Trans r r r
inst✝ : Transitive r
l✝ : List α
h✝ : Sorted r l✝
i j : ℕ
a₁ a₂ : α
as : List α
h₁ : r a₁ a₂
h₂ : Sorted r (a₂ :: as)
hi✝ : i < List.length (a₁ :: a₂ :: as)
hj✝ : j < List.length (a₁ :: a₂ :: as)
l : ℕ
hj : l + 1 < List.length (a₁ :: a₂ :: as)
hl : l + 1 = j
this : l < List.length (a₂ :: as)
hl' : (a₁ :: a₂ :: as)[l + 1] = (a₂ :: as)[l]
h : ¬i = 0
k : ℕ
h' : Nat.succ k < l + 1
hi : Nat.succ k < List.length (a₁ :: a₂ :: as)
hk : i = Nat.succ k
⊢ r (a₁ :: a₂ :: as)[Nat.succ k] (a₁ :: a₂ :: as)[l + 1]
Tactic:
have : k < (a₂::as).length :=
  Nat.pred_lt_pred (by simp) hi
State after:
case neg
α : Type
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Trans r r r
inst✝ : Transitive r
l✝ : List α
h✝ : Sorted r l✝
i j : ℕ
a₁ a₂ : α
as : List α
h₁ : r a₁ a₂
h₂ : Sorted r (a₂ :: as)
hi✝ : i < List.length (a₁ :: a₂ :: as)
hj✝ : j < List.length (a₁ :: a₂ :: as)
l : ℕ
hj : l + 1 < List.length (a₁ :: a₂ :: as)
hl : l + 1 = j
this✝ : l < List.length (a₂ :: as)
hl' : (a₁ :: a₂ :: as)[l + 1] = (a₂ :: as)[l]
h : ¬i = 0
k : ℕ
h' : Nat.succ k < l + 1
hi : Nat.succ k < List.length (a₁ :: a₂ :: as)
hk : i = Nat.succ k
this : k < List.length (a₂ :: as)
⊢ r (a₁ :: a₂ :: as)[Nat.succ k] (a₁ :: a₂ :: as)[l + 1]

State before:
case neg
α : Type
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Trans r r r
inst✝ : Transitive r
l✝ : List α
h✝ : Sorted r l✝
i j : ℕ
a₁ a₂ : α
as : List α
h₁ : r a₁ a₂
h₂ : Sorted r (a₂ :: as)
hi✝ : i < List.length (a₁ :: a₂ :: as)
hj✝ : j < List.length (a₁ :: a₂ :: as)
l : ℕ
hj : l + 1 < List.length (a₁ :: a₂ :: as)
hl : l + 1 = j
this✝ : l < List.length (a₂ :: as)
hl' : (a₁ :: a₂ :: as)[l + 1] = (a₂ :: as)[l]
h : ¬i = 0
k : ℕ
h' : Nat.succ k < l + 1
hi : Nat.succ k < List.length (a₁ :: a₂ :: as)
hk : i = Nat.succ k
this : k < List.length (a₂ :: as)
⊢ r (a₁ :: a₂ :: as)[Nat.succ k] (a₁ :: a₂ :: as)[l + 1]
Tactic:
have hk' : (a₁::a₂::as)[k+1] = (a₂::as)[k] := rfl
State after:
case neg
α : Type
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Trans r r r
inst✝ : Transitive r
l✝ : List α
h✝ : Sorted r l✝
i j : ℕ
a₁ a₂ : α
as : List α
h₁ : r a₁ a₂
h₂ : Sorted r (a₂ :: as)
hi✝ : i < List.length (a₁ :: a₂ :: as)
hj✝ : j < List.length (a₁ :: a₂ :: as)
l : ℕ
hj : l + 1 < List.length (a₁ :: a₂ :: as)
hl : l + 1 = j
this✝ : l < List.length (a₂ :: as)
hl' : (a₁ :: a₂ :: as)[l + 1] = (a₂ :: as)[l]
h : ¬i = 0
k : ℕ
h' : Nat.succ k < l + 1
hi : Nat.succ k < List.length (a₁ :: a₂ :: as)
hk : i = Nat.succ k
this : k < List.length (a₂ :: as)
hk' : (a₁ :: a₂ :: as)[k + 1] = (a₂ :: as)[k]
⊢ r (a₁ :: a₂ :: as)[Nat.succ k] (a₁ :: a₂ :: as)[l + 1]

State before:
case neg
α : Type
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Trans r r r
inst✝ : Transitive r
l✝ : List α
h✝ : Sorted r l✝
i j : ℕ
a₁ a₂ : α
as : List α
h₁ : r a₁ a₂
h₂ : Sorted r (a₂ :: as)
hi✝ : i < List.length (a₁ :: a₂ :: as)
hj✝ : j < List.length (a₁ :: a₂ :: as)
l : ℕ
hj : l + 1 < List.length (a₁ :: a₂ :: as)
hl : l + 1 = j
this✝ : l < List.length (a₂ :: as)
hl' : (a₁ :: a₂ :: as)[l + 1] = (a₂ :: as)[l]
h : ¬i = 0
k : ℕ
h' : Nat.succ k < l + 1
hi : Nat.succ k < List.length (a₁ :: a₂ :: as)
hk : i = Nat.succ k
this : k < List.length (a₂ :: as)
hk' : (a₁ :: a₂ :: as)[k + 1] = (a₂ :: as)[k]
⊢ r (a₁ :: a₂ :: as)[Nat.succ k] (a₁ :: a₂ :: as)[l + 1]
Tactic:
rw [hk',hl']
State after:
case neg
α : Type
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Trans r r r
inst✝ : Transitive r
l✝ : List α
h✝ : Sorted r l✝
i j : ℕ
a₁ a₂ : α
as : List α
h₁ : r a₁ a₂
h₂ : Sorted r (a₂ :: as)
hi✝ : i < List.length (a₁ :: a₂ :: as)
hj✝ : j < List.length (a₁ :: a₂ :: as)
l : ℕ
hj : l + 1 < List.length (a₁ :: a₂ :: as)
hl : l + 1 = j
this✝ : l < List.length (a₂ :: as)
hl' : (a₁ :: a₂ :: as)[l + 1] = (a₂ :: as)[l]
h : ¬i = 0
k : ℕ
h' : Nat.succ k < l + 1
hi : Nat.succ k < List.length (a₁ :: a₂ :: as)
hk : i = Nat.succ k
this : k < List.length (a₂ :: as)
hk' : (a₁ :: a₂ :: as)[k + 1] = (a₂ :: as)[k]
⊢ r (a₂ :: as)[k] (a₂ :: as)[l]

State before:
case neg
α : Type
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Trans r r r
inst✝ : Transitive r
l✝ : List α
h✝ : Sorted r l✝
i j : ℕ
a₁ a₂ : α
as : List α
h₁ : r a₁ a₂
h₂ : Sorted r (a₂ :: as)
hi✝ : i < List.length (a₁ :: a₂ :: as)
hj✝ : j < List.length (a₁ :: a₂ :: as)
l : ℕ
hj : l + 1 < List.length (a₁ :: a₂ :: as)
hl : l + 1 = j
this✝ : l < List.length (a₂ :: as)
hl' : (a₁ :: a₂ :: as)[l + 1] = (a₂ :: as)[l]
h : ¬i = 0
k : ℕ
h' : Nat.succ k < l + 1
hi : Nat.succ k < List.length (a₁ :: a₂ :: as)
hk : i = Nat.succ k
this : k < List.length (a₂ :: as)
hk' : (a₁ :: a₂ :: as)[k + 1] = (a₂ :: as)[k]
⊢ r (a₂ :: as)[k] (a₂ :: as)[l]
Tactic:
apply totally_ordered_of_sorted h₂
State after:
case neg.a
α : Type
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Trans r r r
inst✝ : Transitive r
l✝ : List α
h✝ : Sorted r l✝
i j : ℕ
a₁ a₂ : α
as : List α
h₁ : r a₁ a₂
h₂ : Sorted r (a₂ :: as)
hi✝ : i < List.length (a₁ :: a₂ :: as)
hj✝ : j < List.length (a₁ :: a₂ :: as)
l : ℕ
hj : l + 1 < List.length (a₁ :: a₂ :: as)
hl : l + 1 = j
this✝ : l < List.length (a₂ :: as)
hl' : (a₁ :: a₂ :: as)[l + 1] = (a₂ :: as)[l]
h : ¬i = 0
k : ℕ
h' : Nat.succ k < l + 1
hi : Nat.succ k < List.length (a₁ :: a₂ :: as)
hk : i = Nat.succ k
this : k < List.length (a₂ :: as)
hk' : (a₁ :: a₂ :: as)[k + 1] = (a₂ :: as)[k]
⊢ k < l

State before:
case neg.a
α : Type
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Trans r r r
inst✝ : Transitive r
l✝ : List α
h✝ : Sorted r l✝
i j : ℕ
a₁ a₂ : α
as : List α
h₁ : r a₁ a₂
h₂ : Sorted r (a₂ :: as)
hi✝ : i < List.length (a₁ :: a₂ :: as)
hj✝ : j < List.length (a₁ :: a₂ :: as)
l : ℕ
hj : l + 1 < List.length (a₁ :: a₂ :: as)
hl : l + 1 = j
this✝ : l < List.length (a₂ :: as)
hl' : (a₁ :: a₂ :: as)[l + 1] = (a₂ :: as)[l]
h : ¬i = 0
k : ℕ
h' : Nat.succ k < l + 1
hi : Nat.succ k < List.length (a₁ :: a₂ :: as)
hk : i = Nat.succ k
this : k < List.length (a₂ :: as)
hk' : (a₁ :: a₂ :: as)[k + 1] = (a₂ :: as)[k]
⊢ k < l
Tactic:
apply Nat.pred_lt_pred (by simp) h'
State after:
no goals

State before:
α : Type
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Trans r r r
inst✝ : Transitive r
l✝ : List α
h✝ : Sorted r l✝
i j : ℕ
a₁ a₂ : α
as : List α
h₁ : r a₁ a₂
h₂ : Sorted r (a₂ :: as)
hi✝ : i < List.length (a₁ :: a₂ :: as)
hj✝ : j < List.length (a₁ :: a₂ :: as)
l : ℕ
hj : l + 1 < List.length (a₁ :: a₂ :: as)
hl : l + 1 = j
this : l < List.length (a₂ :: as)
hl' : (a₁ :: a₂ :: as)[l + 1] = (a₂ :: as)[l]
h : ¬i = 0
k : ℕ
h' : Nat.succ k < l + 1
hi : Nat.succ k < List.length (a₁ :: a₂ :: as)
hk : i = Nat.succ k
⊢ Nat.succ k ≠ 0
Tactic:
simp
State after:
no goals

State before:
α : Type
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Trans r r r
inst✝ : Transitive r
l✝ : List α
h✝ : Sorted r l✝
i j : ℕ
a₁ a₂ : α
as : List α
h₁ : r a₁ a₂
h₂ : Sorted r (a₂ :: as)
hi✝ : i < List.length (a₁ :: a₂ :: as)
hj✝ : j < List.length (a₁ :: a₂ :: as)
l : ℕ
hj : l + 1 < List.length (a₁ :: a₂ :: as)
hl : l + 1 = j
this✝ : l < List.length (a₂ :: as)
hl' : (a₁ :: a₂ :: as)[l + 1] = (a₂ :: as)[l]
h : ¬i = 0
k : ℕ
h' : Nat.succ k < l + 1
hi : Nat.succ k < List.length (a₁ :: a₂ :: as)
hk : i = Nat.succ k
this : k < List.length (a₂ :: as)
hk' : (a₁ :: a₂ :: as)[k + 1] = (a₂ :: as)[k]
⊢ Nat.succ k ≠ 0
Tactic:
simp
State after:
no goals