internlm/Lean-Github huggingface dataset:
Theorem: Notes.totally_ordered_of_sorted
Proof 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'
Proof 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]
Theorem: Notes.totally_ordered_of_sorted
Proof 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]
Proof 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]
Theorem: Notes.totally_ordered_of_sorted
Proof 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
Proof 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]
Theorem: Notes.totally_ordered_of_sorted
Proof 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
Proof 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]
Theorem: Notes.totally_ordered_of_sorted
Proof 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
Proof 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]
Theorem: Notes.totally_ordered_of_sorted
Proof 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
Proof state after:
no goals
Theorem: Notes.totally_ordered_of_sorted
Proof 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 *
Proof 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)) })
Theorem: Notes.totally_ordered_of_sorted
Proof 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
Proof 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)) })
Theorem: Notes.totally_ordered_of_sorted
Proof 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₁]
Proof state after:
no goals
Theorem: Notes.totally_ordered_of_sorted
Proof 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'
Proof 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
⊢ α
Theorem: Notes.totally_ordered_of_sorted
Proof 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₁
Proof 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)) })
Theorem: Notes.totally_ordered_of_sorted
Proof 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₁
Proof state after:
no goals
Theorem: Notes.totally_ordered_of_sorted
Proof 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]
Proof 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]
Theorem: Notes.totally_ordered_of_sorted
Proof 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₂
Proof 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
Theorem: Notes.totally_ordered_of_sorted
Proof 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
Proof state after:
no goals
Theorem: Notes.totally_ordered_of_sorted
Proof 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
Proof 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]
Theorem: Notes.totally_ordered_of_sorted
Proof 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'
Proof 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]
Theorem: Notes.totally_ordered_of_sorted
Proof 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]
Proof 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]
Theorem: Notes.totally_ordered_of_sorted
Proof 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
Proof 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]
Theorem: Notes.totally_ordered_of_sorted
Proof 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
Proof 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]
Theorem: Notes.totally_ordered_of_sorted
Proof 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']
Proof 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]