internlm/Lean-Github huggingface dataset:
Theorem: HMem.Program.simpleLoopCost
Proof state before:
case hz.h₁.h₁
TracedProgram : Sort ?u.75510
α : Type u_1
inst✝² : Complexity.Coding α Memory
β : Type u_2
inst✝¹ : Complexity.Encoding β Memory
f : α → β
tp : TracedProgram
sz : α → ℕ
p : Program
inst✝ : Trace.HasCostedProgram p
h : sound p f sz
x : ℕ
hsi : subroutineTimeCost h + localTimeCost h ≤ fun x_1 => x
hr : maxRecurse p = 1
a : α
hsz : sz a = 0
⊢ (subroutineTimeCost h + recurseTimeCost h + localTimeCost h) a = ?hz.h₁.b

case hz.h₁.h₂
TracedProgram : Sort ?u.75510
α : Type u_1
inst✝² : Complexity.Coding α Memory
β : Type u_2
inst✝¹ : Complexity.Encoding β Memory
f : α → β
tp : TracedProgram
sz : α → ℕ
p : Program
inst✝ : Trace.HasCostedProgram p
h : sound p f sz
x : ℕ
hsi : subroutineTimeCost h + localTimeCost h ≤ fun x_1 => x
hr : maxRecurse p = 1
a : α
hsz : sz a = 0
⊢ ?hz.h₁.b = ?hz.b

case hz.h₁.b
TracedProgram : Sort ?u.75510
α : Type u_1
inst✝² : Complexity.Coding α Memory
β : Type u_2
inst✝¹ : Complexity.Encoding β Memory
f : α → β
tp : TracedProgram
sz : α → ℕ
p : Program
inst✝ : Trace.HasCostedProgram p
h : sound p f sz
x : ℕ
hsi : subroutineTimeCost h + localTimeCost h ≤ fun x_1 => x
hr : maxRecurse p = 1
a : α
hsz : sz a = 0
⊢ ℕ

case hz.h₂
TracedProgram : Sort ?u.75510
α : Type u_1
inst✝² : Complexity.Coding α Memory
β : Type u_2
inst✝¹ : Complexity.Encoding β Memory
f : α → β
tp : TracedProgram
sz : α → ℕ
p : Program
inst✝ : Trace.HasCostedProgram p
h : sound p f sz
x : ℕ
hsi : subroutineTimeCost h + localTimeCost h ≤ fun x_1 => x
hr : maxRecurse p = 1
a : α
hsz : sz a = 0
⊢ ?hz.b ≤ x * 0 + x

case hz.b
TracedProgram : Sort ?u.75510
α : Type u_1
inst✝² : Complexity.Coding α Memory
β : Type u_2
inst✝¹ : Complexity.Encoding β Memory
f : α → β
tp : TracedProgram
sz : α → ℕ
p : Program
inst✝ : Trace.HasCostedProgram p
h : sound p f sz
x : ℕ
hsi : subroutineTimeCost h + localTimeCost h ≤ fun x_1 => x
hr : maxRecurse p = 1
a : α
hsz : sz a = 0
⊢ ℕ
Tactic:
apply Nat.add_right_comm _ _ _
Proof state after:
case hz.h₁.h₂
TracedProgram : Sort ?u.75510
α : Type u_1
inst✝² : Complexity.Coding α Memory
β : Type u_2
inst✝¹ : Complexity.Encoding β Memory
f : α → β
tp : TracedProgram
sz : α → ℕ
p : Program
inst✝ : Trace.HasCostedProgram p
h : sound p f sz
x : ℕ
hsi : subroutineTimeCost h + localTimeCost h ≤ fun x_1 => x
hr : maxRecurse p = 1
a : α
hsz : sz a = 0
⊢ subroutineTimeCost h a + localTimeCost h a + recurseTimeCost h a = ?hz.b

case hz.h₂
TracedProgram : Sort ?u.75510
α : Type u_1
inst✝² : Complexity.Coding α Memory
β : Type u_2
inst✝¹ : Complexity.Encoding β Memory
f : α → β
tp : TracedProgram
sz : α → ℕ
p : Program
inst✝ : Trace.HasCostedProgram p
h : sound p f sz
x : ℕ
hsi : subroutineTimeCost h + localTimeCost h ≤ fun x_1 => x
hr : maxRecurse p = 1
a : α
hsz : sz a = 0
⊢ ?hz.b ≤ x * 0 + x

case hz.b
TracedProgram : Sort ?u.75510
α : Type u_1
inst✝² : Complexity.Coding α Memory
β : Type u_2
inst✝¹ : Complexity.Encoding β Memory
f : α → β
tp : TracedProgram
sz : α → ℕ
p : Program
inst✝ : Trace.HasCostedProgram p
h : sound p f sz
x : ℕ
hsi : subroutineTimeCost h + localTimeCost h ≤ fun x_1 => x
hr : maxRecurse p = 1
a : α
hsz : sz a = 0
⊢ ℕ
Theorem: HMem.Program.simpleLoopCost
Proof state before:
case hz.h₁.h₂
TracedProgram : Sort ?u.75510
α : Type u_1
inst✝² : Complexity.Coding α Memory
β : Type u_2
inst✝¹ : Complexity.Encoding β Memory
f : α → β
tp : TracedProgram
sz : α → ℕ
p : Program
inst✝ : Trace.HasCostedProgram p
h : sound p f sz
x : ℕ
hsi : subroutineTimeCost h + localTimeCost h ≤ fun x_1 => x
hr : maxRecurse p = 1
a : α
hsz : sz a = 0
⊢ subroutineTimeCost h a + localTimeCost h a + recurseTimeCost h a = ?hz.b

case hz.h₂
TracedProgram : Sort ?u.75510
α : Type u_1
inst✝² : Complexity.Coding α Memory
β : Type u_2
inst✝¹ : Complexity.Encoding β Memory
f : α → β
tp : TracedProgram
sz : α → ℕ
p : Program
inst✝ : Trace.HasCostedProgram p
h : sound p f sz
x : ℕ
hsi : subroutineTimeCost h + localTimeCost h ≤ fun x_1 => x
hr : maxRecurse p = 1
a : α
hsz : sz a = 0
⊢ ?hz.b ≤ x * 0 + x

case hz.b
TracedProgram : Sort ?u.75510
α : Type u_1
inst✝² : Complexity.Coding α Memory
β : Type u_2
inst✝¹ : Complexity.Encoding β Memory
f : α → β
tp : TracedProgram
sz : α → ℕ
p : Program
inst✝ : Trace.HasCostedProgram p
h : sound p f sz
x : ℕ
hsi : subroutineTimeCost h + localTimeCost h ≤ fun x_1 => x
hr : maxRecurse p = 1
a : α
hsz : sz a = 0
⊢ ℕ
Tactic:
apply Nat.add_comm
Proof state after:
case hz.h₂
TracedProgram : Sort ?u.75510
α : Type u_1
inst✝² : Complexity.Coding α Memory
β : Type u_2
inst✝¹ : Complexity.Encoding β Memory
f : α → β
tp : TracedProgram
sz : α → ℕ
p : Program
inst✝ : Trace.HasCostedProgram p
h : sound p f sz
x : ℕ
hsi : subroutineTimeCost h + localTimeCost h ≤ fun x_1 => x
hr : maxRecurse p = 1
a : α
hsz : sz a = 0
⊢ recurseTimeCost h a + (subroutineTimeCost h a + localTimeCost h a) ≤ x * 0 + x
Theorem: HMem.Program.simpleLoopCost
Proof state before:
case hz.h₂
TracedProgram : Sort ?u.75510
α : Type u_1
inst✝² : Complexity.Coding α Memory
β : Type u_2
inst✝¹ : Complexity.Encoding β Memory
f : α → β
tp : TracedProgram
sz : α → ℕ
p : Program
inst✝ : Trace.HasCostedProgram p
h : sound p f sz
x : ℕ
hsi : subroutineTimeCost h + localTimeCost h ≤ fun x_1 => x
hr : maxRecurse p = 1
a : α
hsz : sz a = 0
⊢ recurseTimeCost h a + (subroutineTimeCost h a + localTimeCost h a) ≤ x * 0 + x
Tactic:
apply add_le_add _
Proof state after:
case hz.h₂
TracedProgram : Sort ?u.75510
α : Type u_1
inst✝² : Complexity.Coding α Memory
β : Type u_2
inst✝¹ : Complexity.Encoding β Memory
f : α → β
tp : TracedProgram
sz : α → ℕ
p : Program
inst✝ : Trace.HasCostedProgram p
h : sound p f sz
x : ℕ
hsi : subroutineTimeCost h + localTimeCost h ≤ fun x_1 => x
hr : maxRecurse p = 1
a : α
hsz : sz a = 0
⊢ subroutineTimeCost h a + localTimeCost h a ≤ x

TracedProgram : Sort ?u.75510
α : Type u_1
inst✝² : Complexity.Coding α Memory
β : Type u_2
inst✝¹ : Complexity.Encoding β Memory
f : α → β
tp : TracedProgram
sz : α → ℕ
p : Program
inst✝ : Trace.HasCostedProgram p
h : sound p f sz
x : ℕ
hsi : subroutineTimeCost h + localTimeCost h ≤ fun x_1 => x
hr : maxRecurse p = 1
a : α
hsz : sz a = 0
⊢ recurseTimeCost h a ≤ x * 0
Theorem: HMem.Program.simpleLoopCost
Proof state before:
case hz.h₂
TracedProgram : Sort ?u.75510
α : Type u_1
inst✝² : Complexity.Coding α Memory
β : Type u_2
inst✝¹ : Complexity.Encoding β Memory
f : α → β
tp : TracedProgram
sz : α → ℕ
p : Program
inst✝ : Trace.HasCostedProgram p
h : sound p f sz
x : ℕ
hsi : subroutineTimeCost h + localTimeCost h ≤ fun x_1 => x
hr : maxRecurse p = 1
a : α
hsz : sz a = 0
⊢ subroutineTimeCost h a + localTimeCost h a ≤ x

TracedProgram : Sort ?u.75510
α : Type u_1
inst✝² : Complexity.Coding α Memory
β : Type u_2
inst✝¹ : Complexity.Encoding β Memory
f : α → β
tp : TracedProgram
sz : α → ℕ
p : Program
inst✝ : Trace.HasCostedProgram p
h : sound p f sz
x : ℕ
hsi : subroutineTimeCost h + localTimeCost h ≤ fun x_1 => x
hr : maxRecurse p = 1
a : α
hsz : sz a = 0
⊢ recurseTimeCost h a ≤ x * 0
Tactic:
apply hsi
Proof state after:
TracedProgram : Sort ?u.75510
α : Type u_1
inst✝² : Complexity.Coding α Memory
β : Type u_2
inst✝¹ : Complexity.Encoding β Memory
f : α → β
tp : TracedProgram
sz : α → ℕ
p : Program
inst✝ : Trace.HasCostedProgram p
h : sound p f sz
x : ℕ
hsi : subroutineTimeCost h + localTimeCost h ≤ fun x_1 => x
hr : maxRecurse p = 1
a : α
hsz : sz a = 0
⊢ recurseTimeCost h a ≤ x * 0
Theorem: HMem.Program.simpleLoopCost
Proof state before:
TracedProgram : Sort ?u.75510
α : Type u_1
inst✝² : Complexity.Coding α Memory
β : Type u_2
inst✝¹ : Complexity.Encoding β Memory
f : α → β
tp : TracedProgram
sz : α → ℕ
p : Program
inst✝ : Trace.HasCostedProgram p
h : sound p f sz
x : ℕ
hsi : subroutineTimeCost h + localTimeCost h ≤ fun x_1 => x
hr : maxRecurse p = 1
a : α
hsz : sz a = 0
⊢ recurseTimeCost h a ≤ x * 0
Tactic:
apply le_of_eq_of_le _ (zero_le _)
Proof state after:
TracedProgram : Sort ?u.75510
α : Type u_1
inst✝² : Complexity.Coding α Memory
β : Type u_2
inst✝¹ : Complexity.Encoding β Memory
f : α → β
tp : TracedProgram
sz : α → ℕ
p : Program
inst✝ : Trace.HasCostedProgram p
h : sound p f sz
x : ℕ
hsi : subroutineTimeCost h + localTimeCost h ≤ fun x_1 => x
hr : maxRecurse p = 1
a : α
hsz : sz a = 0
⊢ recurseTimeCost h a = 0
Theorem: HMem.Program.simpleLoopCost
Proof state before:
TracedProgram : Sort ?u.75510
α : Type u_1
inst✝² : Complexity.Coding α Memory
β : Type u_2
inst✝¹ : Complexity.Encoding β Memory
f : α → β
tp : TracedProgram
sz : α → ℕ
p : Program
inst✝ : Trace.HasCostedProgram p
h : sound p f sz
x : ℕ
hsi : subroutineTimeCost h + localTimeCost h ≤ fun x_1 => x
hr : maxRecurse p = 1
a : α
hsz : sz a = 0
⊢ recurseTimeCost h a = 0
Tactic:
apply Trace.CostedProgram.recurseTimeCost_leaf (costed_sound h) _ hsz
Proof state after:
no goals
Theorem: mul_of_mul_base_exp
Proof state before:
a b c : ℕ
⊢ exp (a * b) c = exp a c * exp b c
Tactic:
match c with 
| 0 => simp only [exp] 
| z+1 => 
  simp only [exp,Nat.add]
  rw [mul_of_mul_base_exp a b z]
  ac_rfl
Proof state after:
no goals
Theorem: mul_of_mul_base_exp
Proof state before:
a b c : ℕ
⊢ exp (a * b) 0 = exp a 0 * exp b 0
Tactic:
simp only [exp]
Proof state after:
no goals
Theorem: mul_of_mul_base_exp
Proof state before:
a b c z : ℕ
⊢ exp (a * b) (z + 1) = exp a (z + 1) * exp b (z + 1)
Tactic:
simp only [exp,Nat.add]
Proof state after:
a b c z : ℕ
⊢ exp (a * b) z * (a * b) = exp a z * a * (exp b z * b)
Theorem: mul_of_mul_base_exp
Proof state before:
a b c z : ℕ
⊢ exp (a * b) z * (a * b) = exp a z * a * (exp b z * b)
Tactic:
rw [mul_of_mul_base_exp a b z]
Proof state after:
a b c z : ℕ
⊢ exp a z * exp b z * (a * b) = exp a z * a * (exp b z * b)
Theorem: mul_of_mul_base_exp
Proof state before:
a b c z : ℕ
⊢ exp a z * exp b z * (a * b) = exp a z * a * (exp b z * b)
Tactic:
ac_rfl
Proof state after:
no goals
Theorem: zero_times
Proof state before:
α : Type
n : ℕ
⊢ times 0 n = 0
Tactic:
match n with 
| 0 => simp 
| n'+1 => 
  simp [times]
  exact zero_times
Proof state after:
no goals
Theorem: zero_times
Proof state before:
α : Type
n : ℕ
⊢ times 0 0 = 0
Tactic:
simp
Proof state after:
no goals
Theorem: zero_times
Proof state before:
α : Type
n n' : ℕ
⊢ times 0 (n' + 1) = 0
Tactic:
simp [times]
Proof state after:
α : Type
n n' : ℕ
⊢ times 0 n' = 0
Theorem: zero_times
Proof state before:
α : Type
n n' : ℕ
⊢ times 0 n' = 0
Tactic:
exact zero_times
Proof state after:
no goals
Theorem: succ_times
Proof state before:
α : Type
n m : ℕ
⊢ times (n + 1) m = times n m + m
Tactic:
match m with 
| 0 =>
  simp [times]
| m'+1 => 
  simp [times]
  rw [@succ_times n m']
  ac_rfl
Proof state after:
no goals
Theorem: succ_times
Proof state before:
α : Type
n m : ℕ
⊢ times (n + 1) 0 = times n 0 + 0
Tactic:
simp [times]
Proof state after:
no goals
Theorem: succ_times
Proof state before:
α : Type
n m m' : ℕ
⊢ times (n + 1) (m' + 1) = times n (m' + 1) + (m' + 1)
Tactic:
simp [times]
Proof state after:
α : Type
n m m' : ℕ
⊢ times (n + 1) m' + (n + 1) = times n m' + n + (m' + 1)
Theorem: succ_times
Proof state before:
α : Type
n m m' : ℕ
⊢ times (n + 1) m' + (n + 1) = times n m' + n + (m' + 1)
Tactic:
rw [@succ_times n m']
Proof state after:
α : Type
n m m' : ℕ
⊢ times n m' + m' + (n + 1) = times n m' + n + (m' + 1)
Theorem: succ_times
Proof state before:
α : Type
n m m' : ℕ
⊢ times n m' + m' + (n + 1) = times n m' + n + (m' + 1)
Tactic:
ac_rfl
Proof state after:
no goals
Theorem: times_comm
Proof state before:
α : Type
n m : ℕ
⊢ times n m = times m n
Tactic:
match n,m with 
| n, 0 => 
  simp [times]
  | n, m'+1 => 
  simp [times]
  rw [times_comm n m']
Proof state after:
no goals
Theorem: times_comm
Proof state before:
α : Type
n✝ m n : ℕ
⊢ times n 0 = times 0 n
Tactic:
simp [times]
Proof state after:
no goals
Theorem: times_comm
Proof state before:
α : Type
n✝ m n m' : ℕ
⊢ times n (m' + 1) = times (m' + 1) n
Tactic:
simp [times]
Proof state after:
α : Type
n✝ m n m' : ℕ
⊢ times n m' + n = times m' n + n
Theorem: times_comm
Proof state before:
α : Type
n✝ m n m' : ℕ
⊢ times n m' + n = times m' n + n
Tactic:
rw [times_comm n m']
Proof state after:
no goals
Theorem: Notes.sorted_tail_of_sorted
Proof state before:
α : Type
r : α → α → Prop
inst✝ : DecidableRel r
a : α
as : List α
h : Sorted r (a :: as)
⊢ Sorted r as
Tactic:
match h with 
| single => apply nil  
| longer _ h'' => exact h''
Proof state after:
no goals
Theorem: Notes.sorted_tail_of_sorted
Proof state before:
α : Type
r : α → α → Prop
inst✝ : DecidableRel r
a : α
as : List α
h : Sorted r (a :: as)
⊢ Sorted r []
Tactic:
apply nil
Proof state after:
no goals
Theorem: Notes.sorted_tail_of_sorted
Proof state before:
α : Type
r : α → α → Prop
inst✝ : DecidableRel r
a : α
as : List α
h : Sorted r (a :: as)
a₂✝ : α
as✝ : List α
h✝ : r a a₂✝
h'' : Sorted r (a₂✝ :: as✝)
⊢ Sorted r (a₂✝ :: as✝)
Tactic:
exact h''
Proof state after:
no goals
Theorem: Notes.len_insert_eq_succ_len
Proof state before:
α : Type
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l : List α
⊢ List.length (insert r a []) = List.length [] + 1
Tactic:
simp [insert]
Proof state after:
no goals
Theorem: Notes.len_insert_eq_succ_len
Proof state before:
α : Type
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l : List α
a' : α
as : List α
h : r a a'
⊢ List.length (insert r a (a' :: as)) = List.length (a' :: as) + 1
Tactic:
simp [insert, h]
Proof state after:
no goals
Theorem: Notes.len_insert_eq_succ_len
Proof state before:
α : Type
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l : List α
a' : α
as : List α
h : ¬r a a'
⊢ List.length (insert r a (a' :: as)) = List.length (a' :: as) + 1
Tactic:
simp [insert, h]
Proof state after:
α : Type
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l : List α
a' : α
as : List α
h : ¬r a a'
⊢ List.length (insert r a as) = List.length as + 1
Theorem: Notes.len_insert_eq_succ_len
Proof state before:
α : Type
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l : List α
a' : α
as : List α
h : ¬r a a'
⊢ List.length (insert r a as) = List.length as + 1
Tactic:
apply len_insert_eq_succ_len
Proof state after:
no goals
Theorem: Notes.ordered_cons_insert_of_unordered
Proof state before:
α : Type
r : α → α → Prop
inst✝ : DecidableRel r
a a' : α
as : List α
h' : r a' a
h : Sorted r [a']
⊢ r a' (insert r a [])[0]
Tactic:
simp [insert]
Proof state after:
α : Type
r : α → α → Prop
inst✝ : DecidableRel r
a a' : α
as : List α
h' : r a' a
h : Sorted r [a']
⊢ r a' a
Theorem: Notes.ordered_cons_insert_of_unordered
Proof state before:
α : Type
r : α → α → Prop
inst✝ : DecidableRel r
a a' : α
as : List α
h' : r a' a
h : Sorted r [a']
⊢ r a' a
Tactic:
assumption
Proof state after:
no goals
Theorem: Notes.ordered_cons_insert_of_unordered
Proof state before:
α : Type
r : α → α → Prop
inst✝ : DecidableRel r
a a' : α
as : List α
h' : r a' a
a'' : α
as' : List α
h : Sorted r (a' :: a'' :: as')
h'' : r a a''
⊢ r a' (insert r a (a'' :: as'))[0]
Tactic:
simpa [insert, h'']
Proof state after:
no goals
Theorem: Notes.ordered_cons_insert_of_unordered
Proof state before:
α : Type
r : α → α → Prop
inst✝ : DecidableRel r
a a' : α
as : List α
h' : r a' a
a'' : α
as' : List α
h : Sorted r (a' :: a'' :: as')
h'' : ¬r a a''
⊢ r a' (insert r a (a'' :: as'))[0]
Tactic:
simp [insert, h'']
Proof state after:
α : Type
r : α → α → Prop
inst✝ : DecidableRel r
a a' : α
as : List α
h' : r a' a
a'' : α
as' : List α
h : Sorted r (a' :: a'' :: as')
h'' : ¬r a a''
⊢ r a' a''
Theorem: Notes.ordered_cons_insert_of_unordered
Proof state before:
α : Type
r : α → α → Prop
inst✝ : DecidableRel r
a a' : α
as : List α
h' : r a' a
a'' : α
as' : List α
h : Sorted r (a' :: a'' :: as')
h'' : ¬r a a''
⊢ r a' a''
Tactic:
apply ordered_of_sorted r h
Proof state after:
no goals
Theorem: Notes.insert_sorted_of_sorted
Proof state before:
α : Type
r : α → α → Prop
inst✝¹ : DecidableRel r
a : α
l : List α
inst✝ : Asymmetric r
a' : α
as : List α
h : Sorted r (a' :: as)
h' : r a a'
⊢ Sorted r (insert r a (a' :: as))
Tactic:
simp [insert, h']
Proof state after:
α : Type
r : α → α → Prop
inst✝¹ : DecidableRel r
a : α
l : List α
inst✝ : Asymmetric r
a' : α
as : List α
h : Sorted r (a' :: as)
h' : r a a'
⊢ Sorted r (a :: a' :: as)
Theorem: Notes.insert_sorted_of_sorted
Proof state before:
α : Type
r : α → α → Prop
inst✝¹ : DecidableRel r
a : α
l : List α
inst✝ : Asymmetric r
a' : α
as : List α
h : Sorted r (a' :: as)
h' : r a a'
⊢ Sorted r (a :: a' :: as)
Tactic:
apply longer h' h
Proof state after:
no goals
Theorem: Notes.insert_sorted_of_sorted
Proof state before:
α : Type
r : α → α → Prop
inst✝¹ : DecidableRel r
a : α
l : List α
inst✝ : Asymmetric r
a' : α
as : List α
h : Sorted r (a' :: as)
h' : ¬r a a'
⊢ Sorted r (insert r a (a' :: as))
Tactic:
simp [insert, h']
Proof state after:
α : Type
r : α → α → Prop
inst✝¹ : DecidableRel r
a : α
l : List α
inst✝ : Asymmetric r
a' : α
as : List α
h : Sorted r (a' :: as)
h' : ¬r a a'
⊢ Sorted r (a' :: insert r a as)
Theorem: Notes.insert_sorted_of_sorted
Proof state before:
α : Type
r : α → α → Prop
inst✝¹ : DecidableRel r
a : α
l : List α
inst✝ : Asymmetric r
a' : α
as : List α
h : Sorted r (a' :: as)
h' : ¬r a a'
⊢ Sorted r (a' :: insert r a as)
Tactic:
apply cons r
Proof state after:
case h₁
α : Type
r : α → α → Prop
inst✝¹ : DecidableRel r
a : α
l : List α
inst✝ : Asymmetric r
a' : α
as : List α
h : Sorted r (a' :: as)
h' : ¬r a a'
⊢ Sorted r (insert r a as)

case h₃
α : Type
r : α → α → Prop
inst✝¹ : DecidableRel r
a : α
l : List α
inst✝ : Asymmetric r
a' : α
as : List α
h : Sorted r (a' :: as)
h' : ¬r a a'
⊢ r a' (insert r a as)[0]

case h₂
α : Type
r : α → α → Prop
inst✝¹ : DecidableRel r
a : α
l : List α
inst✝ : Asymmetric r
a' : α
as : List α
h : Sorted r (a' :: as)
h' : ¬r a a'
⊢ List.length (insert r a as) > 0
Theorem: Notes.insert_sorted_of_sorted
Proof state before:
case h₁
α : Type
r : α → α → Prop
inst✝¹ : DecidableRel r
a : α
l : List α
inst✝ : Asymmetric r
a' : α
as : List α
h : Sorted r (a' :: as)
h' : ¬r a a'
⊢ Sorted r (insert r a as)
Tactic:
apply insert_sorted_of_sorted <| sorted_tail_of_sorted r a' as h
Proof state after:
no goals
Theorem: Notes.insert_sorted_of_sorted
Proof state before:
case h₃
α : Type
r : α → α → Prop
inst✝¹ : DecidableRel r
a : α
l : List α
inst✝ : Asymmetric r
a' : α
as : List α
h : Sorted r (a' :: as)
h' : ¬r a a'
⊢ r a' (insert r a as)[0]
Tactic:
apply ordered_cons_insert_of_unordered r h
Proof state after:
case h₃
α : Type
r : α → α → Prop
inst✝¹ : DecidableRel r
a : α
l : List α
inst✝ : Asymmetric r
a' : α
as : List α
h : Sorted r (a' :: as)
h' : ¬r a a'
⊢ r a' a
Theorem: Notes.insert_sorted_of_sorted
Proof state before:
case h₃
α : Type
r : α → α → Prop
inst✝¹ : DecidableRel r
a : α
l : List α
inst✝ : Asymmetric r
a' : α
as : List α
h : Sorted r (a' :: as)
h' : ¬r a a'
⊢ r a' a
Tactic:
apply asym
Proof state after:
case h₃.a
α : Type
r : α → α → Prop
inst✝¹ : DecidableRel r
a : α
l : List α
inst✝ : Asymmetric r
a' : α
as : List α
h : Sorted r (a' :: as)
h' : ¬r a a'
⊢ ¬r a a'
Theorem: Notes.insert_sorted_of_sorted
Proof state before:
case h₃.a
α : Type
r : α → α → Prop
inst✝¹ : DecidableRel r
a : α
l : List α
inst✝ : Asymmetric r
a' : α
as : List α
h : Sorted r (a' :: as)
h' : ¬r a a'
⊢ ¬r a a'
Tactic:
assumption
Proof state after:
no goals
Theorem: Notes.sorted_of_insertSort
Proof state before:
α : Type
r : α → α → Prop
inst✝¹ : DecidableRel r
l : List α
inst✝ : Asymmetric r
a : α
as : List α
⊢ Sorted r (insertSort r (a :: as))
Tactic:
dsimp [insertSort]
Proof state after:
α : Type
r : α → α → Prop
inst✝¹ : DecidableRel r
l : List α
inst✝ : Asymmetric r
a : α
as : List α
⊢ Sorted r (insert r a (insertSort r as))
Theorem: Notes.sorted_of_insertSort
Proof state before:
α : Type
r : α → α → Prop
inst✝¹ : DecidableRel r
l : List α
inst✝ : Asymmetric r
a : α
as : List α
⊢ Sorted r (insert r a (insertSort r as))
Tactic:
apply insert_sorted_of_sorted r <| sorted_of_insertSort as
Proof state after:
no goals
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✝ : ℕ
x✝¹ : i✝ < j✝
h' : i✝ < List.length []
x✝ : j✝ < List.length []
⊢ False
Tactic:
rw [List.length_nil] at 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✝ : ℕ
x✝¹ : i✝ < j✝
h' : i✝ < 0
x✝ : j✝ < List.length []
⊢ False
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✝ : ℕ
x✝¹ : i✝ < j✝
h' : i✝ < 0
x✝ : j✝ < List.length []
⊢ False
Tactic:
exact Nat.not_lt_zero _ h'
Proof state after:
no goals
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✝ : α
h : i✝ < j✝
hi : i✝ < List.length [a✝]
hj : j✝ < List.length [a✝]
⊢ r [a✝][i✝] [a✝][j✝]
Tactic:
dsimp at hi 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✝ : α
h : i✝ < j✝
hi : i✝ < 1
hj : j✝ < 1
⊢ r [a✝][i✝] [a✝][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✝ : α
h : i✝ < j✝
hi : i✝ < 1
hj : j✝ < 1
⊢ r [a✝][i✝] [a✝][j✝]
Tactic:
apply False.elim
Proof 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
Theorem: Notes.totally_ordered_of_sorted
Proof 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
Proof state after:
no goals
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✝)
⊢ 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
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✝)
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✝]
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✝)
⊢ r (a₁✝ :: a₂✝ :: as✝)[i✝] (a₁✝ :: a₂✝ :: as✝)[j✝]
Tactic:
rename_i i j a₁ a₂ as
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)
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]
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)
⊢ r (a₁ :: a₂ :: as)[i] (a₁ :: a₂ :: as)[j]
Tactic:
have ⟨l,hl⟩ := Nat.succ_of_lt 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)
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]