internlm/Lean-Github huggingface dataset:
Theorem: insert_sorted_size_eq'
Proof state before:
case succ
α : Type u_1
inst✝ : Ord α
len i' : Nat
ih :
  ∀ (arr : Array α) (isLt : i' < Array.size arr),
    Array.size arr = len → Array.size (insertSorted' arr { val := i', isLt := isLt }) = len
arr : Array α
isLt : Nat.succ i' < Array.size arr
hLen : Array.size arr = len
⊢ Array.size (insertSorted' arr { val := Nat.succ i', isLt := isLt }) = len
Tactic:
simp [insertSorted', dbgTraceIfShared]
Proof state after:
case succ
α : Type u_1
inst✝ : Ord α
len i' : Nat
ih :
  ∀ (arr : Array α) (isLt : i' < Array.size arr),
    Array.size arr = len → Array.size (insertSorted' arr { val := i', isLt := isLt }) = len
arr : Array α
isLt : Nat.succ i' < Array.size arr
hLen : Array.size arr = len
⊢ Array.size
      (match compare arr[i'] arr[{ val := Nat.succ i', isLt := isLt }] with
      | Ordering.lt => arr
      | Ordering.eq => arr
      | Ordering.gt =>
        insertSorted'
          (Array.swap arr { val := i', isLt := (_ : i' < Array.size arr) } { val := Nat.succ i', isLt := isLt })
          { val := i',
            isLt :=
              (_ :
                i' <
                  Array.size
                    (Array.swap arr { val := i', isLt := (_ : i' < Array.size arr) }
                      { val := Nat.succ i', isLt := isLt })) }) =
    len
Theorem: insert_sorted_size_eq'
Proof state before:
case succ
α : Type u_1
inst✝ : Ord α
len i' : Nat
ih :
  ∀ (arr : Array α) (isLt : i' < Array.size arr),
    Array.size arr = len → Array.size (insertSorted' arr { val := i', isLt := isLt }) = len
arr : Array α
isLt : Nat.succ i' < Array.size arr
hLen : Array.size arr = len
⊢ Array.size
      (match compare arr[i'] arr[{ val := Nat.succ i', isLt := isLt }] with
      | Ordering.lt => arr
      | Ordering.eq => arr
      | Ordering.gt =>
        insertSorted'
          (Array.swap arr { val := i', isLt := (_ : i' < Array.size arr) } { val := Nat.succ i', isLt := isLt })
          { val := i',
            isLt :=
              (_ :
                i' <
                  Array.size
                    (Array.swap arr { val := i', isLt := (_ : i' < Array.size arr) }
                      { val := Nat.succ i', isLt := isLt })) }) =
    len
Tactic:
split <;> simp [*]
Proof state after:
no goals
Theorem: onePlusOneIsTwo''
Proof state before:
⊢ 1 + 1 = 2
Tactic:
simp
Proof state after:
no goals
Theorem: addAndAppend
Proof state before:
⊢ 1 + 1 = 2 ∧ String.append "Str" "ing" = "String"
Tactic:
simp
Proof state after:
no goals
Theorem: onePlusOneAndLessThan
Proof state before:
⊢ 1 + 1 = 2 ∨ 3 < 5
Tactic:
simp
Proof state after:
no goals
Theorem: notTwoEqualFive
Proof state before:
⊢ ¬1 + 1 = 5
Tactic:
simp
Proof state after:
no goals
Theorem: trueOrFalse
Proof state before:
⊢ True ∨ False
Tactic:
simp
Proof state after:
no goals
Theorem: falseImpliesTrue
Proof state before:
⊢ False → True
Tactic:
simp
Proof state after:
no goals
Theorem: fairlyEasy
Proof state before:
⊢ EasyToProve
Tactic:
constructor
Proof state after:
no goals
Theorem: three_is_three
Proof state before:
⊢ IsThree 3
Tactic:
constructor
Proof state after:
no goals
Theorem: three_plus_two_five
Proof state before:
n : Nat
⊢ IsThree n → IsFive (n + 2)
Tactic:
intro three
Proof state after:
n : Nat
three : IsThree n
⊢ IsFive (n + 2)
Theorem: three_plus_two_five
Proof state before:
n : Nat
three : IsThree n
⊢ IsFive (n + 2)
Tactic:
cases three with
| isThree => constructor
Proof state after:
no goals
Theorem: three_plus_two_five
Proof state before:
case isThree

⊢ IsFive (3 + 2)
Tactic:
constructor
Proof state after:
no goals
Theorem: four_is_not_three
Proof state before:
⊢ ¬IsThree 4
Tactic:
simp [Not]
Proof state after:
⊢ IsThree 4 → False
Theorem: four_is_not_three
Proof state before:
⊢ IsThree 4 → False
Tactic:
intro h
Proof state after:
h : IsThree 4
⊢ False
Theorem: four_is_not_three
Proof state before:
h : IsThree 4
⊢ False
Tactic:
cases h
Proof state after:
no goals
Theorem: atLeastThreeSpiders
Proof state before:
⊢ NonEmptyList.inBounds idahoSpiders 2
Tactic:
simp
Proof state after:
no goals
Theorem: notSixSpiders
Proof state before:
⊢ ¬NonEmptyList.inBounds idahoSpiders 5
Tactic:
simp
Proof state after:
no goals
Theorem: Nat.succ_le_succ'
Proof state before:
n m : Nat
⊢ n ≤ m → succ n ≤ succ m
Tactic:
intro h
Proof state after:
n m : Nat
h : n ≤ m
⊢ succ n ≤ succ m
Theorem: Nat.succ_le_succ'
Proof state before:
n m : Nat
h : n ≤ m
⊢ succ n ≤ succ m
Tactic:
induction h with
| refl => constructor
| step _ ih =>
  constructor
  assumption
Proof state after:
no goals
Theorem: Nat.succ_le_succ'
Proof state before:
case refl
n m : Nat
⊢ succ n ≤ succ n
Tactic:
constructor
Proof state after:
no goals
Theorem: Nat.succ_le_succ'
Proof state before:
case step
n m m✝ : Nat
a✝ : Nat.le n m✝
ih : succ n ≤ succ m✝
⊢ succ n ≤ succ (succ m✝)
Tactic:
constructor
Proof state after:
case step.a
n m m✝ : Nat
a✝ : Nat.le n m✝
ih : succ n ≤ succ m✝
⊢ Nat.le (succ n) (m✝ + 1)
Theorem: Nat.succ_le_succ'
Proof state before:
case step.a
n m m✝ : Nat
a✝ : Nat.le n m✝
ih : succ n ≤ succ m✝
⊢ Nat.le (succ n) (m✝ + 1)
Tactic:
assumption
Proof state after:
no goals
Theorem: Nat.le_succ_of_le'
Proof state before:
n m : Nat
⊢ n ≤ m → n ≤ succ m
Tactic:
intro h
Proof state after:
n m : Nat
h : n ≤ m
⊢ n ≤ succ m
Theorem: Nat.le_succ_of_le'
Proof state before:
n m : Nat
h : n ≤ m
⊢ n ≤ succ m
Tactic:
induction h with
| refl => constructor ; constructor
| step => constructor ; assumption
Proof state after:
no goals
Theorem: Nat.le_succ_of_le'
Proof state before:
case refl
n m : Nat
⊢ n ≤ succ n
Tactic:
constructor
Proof state after:
case refl.a
n m : Nat
⊢ Nat.le n n
Theorem: Nat.le_succ_of_le'
Proof state before:
case refl.a
n m : Nat
⊢ Nat.le n n
Tactic:
constructor
Proof state after:
no goals
Theorem: Nat.le_succ_of_le'
Proof state before:
case step
n m m✝ : Nat
a✝ : Nat.le n m✝
a_ih✝ : n ≤ succ m✝
⊢ n ≤ succ (succ m✝)
Tactic:
constructor
Proof state after:
case step.a
n m m✝ : Nat
a✝ : Nat.le n m✝
a_ih✝ : n ≤ succ m✝
⊢ Nat.le n (m✝ + 1)
Theorem: Nat.le_succ_of_le'
Proof state before:
case step.a
n m m✝ : Nat
a✝ : Nat.le n m✝
a_ih✝ : n ≤ succ m✝
⊢ Nat.le n (m✝ + 1)
Tactic:
assumption
Proof state after:
no goals
Theorem: Nat.le_succ_of_le''
Proof state before:
n m : Nat
⊢ n ≤ m → n ≤ succ m
Tactic:
intro h
Proof state after:
n m : Nat
h : n ≤ m
⊢ n ≤ succ m
Theorem: Nat.le_succ_of_le''
Proof state before:
n m : Nat
h : n ≤ m
⊢ n ≤ succ m
Tactic:
induction h with
| refl => apply Nat.le.step; exact Nat.le.refl
| step _ ih => apply Nat.le.step; exact ih
Proof state after:
no goals
Theorem: Nat.le_succ_of_le''
Proof state before:
case refl
n m : Nat
⊢ n ≤ succ n
Tactic:
apply Nat.le.step
Proof state after:
case refl.a
n m : Nat
⊢ Nat.le n n
Theorem: Nat.le_succ_of_le''
Proof state before:
case refl.a
n m : Nat
⊢ Nat.le n n
Tactic:
exact Nat.le.refl
Proof state after:
no goals
Theorem: Nat.le_succ_of_le''
Proof state before:
case step
n m m✝ : Nat
a✝ : Nat.le n m✝
ih : n ≤ succ m✝
⊢ n ≤ succ (succ m✝)
Tactic:
apply Nat.le.step
Proof state after:
case step.a
n m m✝ : Nat
a✝ : Nat.le n m✝
ih : n ≤ succ m✝
⊢ Nat.le n (m✝ + 1)
Theorem: Nat.le_succ_of_le''
Proof state before:
case step.a
n m m✝ : Nat
a✝ : Nat.le n m✝
ih : n ≤ succ m✝
⊢ Nat.le n (m✝ + 1)
Tactic:
exact ih
Proof state after:
no goals
Theorem: Nat.le_succ_of_le'''
Proof state before:
n m : Nat
⊢ n ≤ m → n ≤ succ m
Tactic:
intro h
Proof state after:
n m : Nat
h : n ≤ m
⊢ n ≤ succ m
Theorem: Nat.le_succ_of_le'''
Proof state before:
n m : Nat
h : n ≤ m
⊢ n ≤ succ m
Tactic:
induction h <;> repeat (first | constructor | assumption)
Proof state after:
no goals
Theorem: Nat.le_succ_of_le'''
Proof state before:
case step.a.a
n m m✝ : Nat
a✝ : Nat.le n m✝
a_ih✝ : n ≤ succ m✝
⊢ Nat.le n m✝
Tactic:
(first | constructor | assumption)
Proof state after:
no goals
Theorem: Nat.le_succ_of_le'''
Proof state before:
case step.a.a
n m m✝ : Nat
a✝ : Nat.le n m✝
a_ih✝ : n ≤ succ m✝
⊢ Nat.le n m✝
Tactic:
first | constructor | assumption
Proof state after:
no goals
Theorem: Nat.le_succ_of_le'''
Proof state before:
case step.a
n m m✝ : Nat
a✝ : Nat.le n m✝
a_ih✝ : n ≤ succ m✝
⊢ Nat.le n (m✝ + 1)
Tactic:
constructor
Proof state after:
case step.a.a
n m m✝ : Nat
a✝ : Nat.le n m✝
a_ih✝ : n ≤ succ m✝
⊢ Nat.le n m✝
Theorem: Nat.le_succ_of_le'''
Proof state before:
case step.a.a
n m m✝ : Nat
a✝ : Nat.le n m✝
a_ih✝ : n ≤ succ m✝
⊢ Nat.le n m✝
Tactic:
assumption
Proof state after:
no goals
Theorem: splitList_shorter_le
Proof state before:
α : Type u_1
lst : List α
⊢ List.length (splitList lst).fst ≤ List.length lst ∧ List.length (splitList lst).snd ≤ List.length lst
Tactic:
induction lst with
| nil =>
  simp [splitList]
| cons x xs ih =>
  simp [splitList]
  cases ih
  constructor
  case left =>
    apply Nat.succ_le_succ
    assumption
  case right =>
    apply Nat.le_succ_of_le
    assumption
Proof state after:
no goals
Theorem: splitList_shorter_le
Proof state before:
case nil
α : Type u_1
⊢ List.length (splitList []).fst ≤ List.length [] ∧ List.length (splitList []).snd ≤ List.length []
Tactic:
simp [splitList]
Proof state after:
no goals
Theorem: splitList_shorter_le
Proof state before:
case cons
α : Type u_1
x : α
xs : List α
ih : List.length (splitList xs).fst ≤ List.length xs ∧ List.length (splitList xs).snd ≤ List.length xs
⊢ List.length (splitList (x :: xs)).fst ≤ List.length (x :: xs) ∧
    List.length (splitList (x :: xs)).snd ≤ List.length (x :: xs)
Tactic:
simp [splitList]
Proof state after:
case cons
α : Type u_1
x : α
xs : List α
ih : List.length (splitList xs).fst ≤ List.length xs ∧ List.length (splitList xs).snd ≤ List.length xs
⊢ Nat.succ (List.length (splitList xs).snd) ≤ Nat.succ (List.length xs) ∧
    List.length (splitList xs).fst ≤ Nat.succ (List.length xs)
Theorem: splitList_shorter_le
Proof state before:
case cons
α : Type u_1
x : α
xs : List α
ih : List.length (splitList xs).fst ≤ List.length xs ∧ List.length (splitList xs).snd ≤ List.length xs
⊢ Nat.succ (List.length (splitList xs).snd) ≤ Nat.succ (List.length xs) ∧
    List.length (splitList xs).fst ≤ Nat.succ (List.length xs)
Tactic:
cases ih
Proof state after:
case cons.intro
α : Type u_1
x : α
xs : List α
left✝ : List.length (splitList xs).fst ≤ List.length xs
right✝ : List.length (splitList xs).snd ≤ List.length xs
⊢ Nat.succ (List.length (splitList xs).snd) ≤ Nat.succ (List.length xs) ∧
    List.length (splitList xs).fst ≤ Nat.succ (List.length xs)
Theorem: splitList_shorter_le
Proof state before:
case cons.intro
α : Type u_1
x : α
xs : List α
left✝ : List.length (splitList xs).fst ≤ List.length xs
right✝ : List.length (splitList xs).snd ≤ List.length xs
⊢ Nat.succ (List.length (splitList xs).snd) ≤ Nat.succ (List.length xs) ∧
    List.length (splitList xs).fst ≤ Nat.succ (List.length xs)
Tactic:
constructor
Proof state after:
case cons.intro.left
α : Type u_1
x : α
xs : List α
left✝ : List.length (splitList xs).fst ≤ List.length xs
right✝ : List.length (splitList xs).snd ≤ List.length xs
⊢ Nat.succ (List.length (splitList xs).snd) ≤ Nat.succ (List.length xs)

case cons.intro.right
α : Type u_1
x : α
xs : List α
left✝ : List.length (splitList xs).fst ≤ List.length xs
right✝ : List.length (splitList xs).snd ≤ List.length xs
⊢ List.length (splitList xs).fst ≤ Nat.succ (List.length xs)
Theorem: splitList_shorter_le
Proof state before:
α : Type u_1
x : α
xs : List α
left✝ : List.length (splitList xs).fst ≤ List.length xs
right✝ : List.length (splitList xs).snd ≤ List.length xs
⊢ Nat.succ (List.length (splitList xs).snd) ≤ Nat.succ (List.length xs)
Tactic:
case left =>
  apply Nat.succ_le_succ
  assumption
Proof state after:
no goals
Theorem: splitList_shorter_le
Proof state before:
α : Type u_1
x : α
xs : List α
left✝ : List.length (splitList xs).fst ≤ List.length xs
right✝ : List.length (splitList xs).snd ≤ List.length xs
⊢ List.length (splitList xs).fst ≤ Nat.succ (List.length xs)
Tactic:
case right =>
  apply Nat.le_succ_of_le
  assumption
Proof state after:
no goals
Theorem: splitList_shorter_le
Proof state before:
α : Type u_1
x : α
xs : List α
left✝ : List.length (splitList xs).fst ≤ List.length xs
right✝ : List.length (splitList xs).snd ≤ List.length xs
⊢ Nat.succ (List.length (splitList xs).snd) ≤ Nat.succ (List.length xs)
Tactic:
apply Nat.succ_le_succ
Proof state after:
case a
α : Type u_1
x : α
xs : List α
left✝ : List.length (splitList xs).fst ≤ List.length xs
right✝ : List.length (splitList xs).snd ≤ List.length xs
⊢ List.length (splitList xs).snd ≤ List.length xs
Theorem: splitList_shorter_le
Proof state before:
case a
α : Type u_1
x : α
xs : List α
left✝ : List.length (splitList xs).fst ≤ List.length xs
right✝ : List.length (splitList xs).snd ≤ List.length xs
⊢ List.length (splitList xs).snd ≤ List.length xs
Tactic:
assumption
Proof state after:
no goals
Theorem: splitList_shorter_le
Proof state before:
α : Type u_1
x : α
xs : List α
left✝ : List.length (splitList xs).fst ≤ List.length xs
right✝ : List.length (splitList xs).snd ≤ List.length xs
⊢ List.length (splitList xs).fst ≤ Nat.succ (List.length xs)
Tactic:
apply Nat.le_succ_of_le
Proof state after:
case h
α : Type u_1
x : α
xs : List α
left✝ : List.length (splitList xs).fst ≤ List.length xs
right✝ : List.length (splitList xs).snd ≤ List.length xs
⊢ List.length (splitList xs).fst ≤ List.length xs
Theorem: splitList_shorter_le
Proof state before:
case h
α : Type u_1
x : α
xs : List α
left✝ : List.length (splitList xs).fst ≤ List.length xs
right✝ : List.length (splitList xs).snd ≤ List.length xs
⊢ List.length (splitList xs).fst ≤ List.length xs
Tactic:
assumption
Proof state after:
no goals
Theorem: splitList_shorter
Proof state before:
α : Type u_1
lst : List α
x✝ : List.length lst ≥ 2
⊢ List.length (splitList lst).fst < List.length lst ∧ List.length (splitList lst).snd < List.length lst
Tactic:
match lst with
| x :: y :: xs =>
  simp_arith [splitList]
  apply splitList_shorter_le
Proof state after:
no goals
Theorem: splitList_shorter
Proof state before:
α : Type u_1
lst : List α
x y : α
xs : List α
x✝ : List.length (x :: y :: xs) ≥ 2
⊢ List.length (splitList (x :: y :: xs)).fst < List.length (x :: y :: xs) ∧
    List.length (splitList (x :: y :: xs)).snd < List.length (x :: y :: xs)
Tactic:
simp_arith [splitList]
Proof state after:
α : Type u_1
lst : List α
x y : α
xs : List α
x✝ : List.length (x :: y :: xs) ≥ 2
⊢ List.length (splitList xs).fst ≤ List.length xs ∧ List.length (splitList xs).snd ≤ List.length xs
Theorem: splitList_shorter
Proof state before:
α : Type u_1
lst : List α
x y : α
xs : List α
x✝ : List.length (x :: y :: xs) ≥ 2
⊢ List.length (splitList xs).fst ≤ List.length xs ∧ List.length (splitList xs).snd ≤ List.length xs
Tactic:
apply splitList_shorter_le
Proof state after:
no goals
Theorem: plusR_zero_left
Proof state before:
k : Nat
⊢ k = Nat.plusR 0 k
Tactic:
induction k with
| zero => rfl
| succ n ih =>
  unfold Nat.plusR
  rw [←ih]
Proof state after:
no goals
Theorem: plusR_zero_left
Proof state before:
case zero

⊢ Nat.zero = Nat.plusR 0 Nat.zero
Tactic:
rfl
Proof state after:
no goals
Theorem: plusR_zero_left
Proof state before:
case succ
n : Nat
ih : n = Nat.plusR 0 n
⊢ Nat.succ n = Nat.plusR 0 (Nat.succ n)
Tactic:
unfold Nat.plusR
Proof state after:
case succ
n : Nat
ih : n = Nat.plusR 0 n
⊢ Nat.succ n = Nat.plusR 0 n + 1
Theorem: plusR_zero_left
Proof state before:
case succ
n : Nat
ih : n = Nat.plusR 0 n
⊢ Nat.succ n = Nat.plusR 0 n + 1
Tactic:
rw [←ih]
Proof state after:
no goals
Theorem: plusR_zero_left'
Proof state before:
k : Nat
⊢ k = Nat.plusR 0 k
Tactic:
induction k with
| zero => rfl
| succ n ih =>
  simp [Nat.plusR]
  assumption
Proof state after:
no goals
Theorem: plusR_zero_left'
Proof state before:
case zero

⊢ Nat.zero = Nat.plusR 0 Nat.zero
Tactic:
rfl
Proof state after:
no goals
Theorem: plusR_zero_left'
Proof state before:
case succ
n : Nat
ih : n = Nat.plusR 0 n
⊢ Nat.succ n = Nat.plusR 0 (Nat.succ n)
Tactic:
simp [Nat.plusR]
Proof state after:
case succ
n : Nat
ih : n = Nat.plusR 0 n
⊢ n = Nat.plusR 0 n
Theorem: plusR_zero_left'
Proof state before:
case succ
n : Nat
ih : n = Nat.plusR 0 n
⊢ n = Nat.plusR 0 n
Tactic:
assumption
Proof state after:
no goals
Theorem: plusR_zero_left''
Proof state before:
k : Nat
⊢ k = Nat.plusR 0 k
Tactic:
induction k
Proof state after:
case zero

⊢ Nat.zero = Nat.plusR 0 Nat.zero

case succ
n✝ : Nat
n_ih✝ : n✝ = Nat.plusR 0 n✝
⊢ Nat.succ n✝ = Nat.plusR 0 (Nat.succ n✝)
Theorem: plusR_zero_left''
Proof state before:
⊢ Nat.zero = Nat.plusR 0 Nat.zero
Tactic:
case zero => simp [Nat.plusR]
Proof state after:
no goals
Theorem: plusR_zero_left''
Proof state before:
n : Nat
ih : n = Nat.plusR 0 n
⊢ Nat.succ n = Nat.plusR 0 (Nat.succ n)
Tactic:
case succ n ih =>
  simp [Nat.plusR]
  assumption
Proof state after:
no goals
Theorem: plusR_zero_left''
Proof state before:
⊢ Nat.zero = Nat.plusR 0 Nat.zero
Tactic:
simp [Nat.plusR]
Proof state after:
no goals
Theorem: plusR_zero_left''
Proof state before:
n : Nat
ih : n = Nat.plusR 0 n
⊢ Nat.succ n = Nat.plusR 0 (Nat.succ n)
Tactic:
simp [Nat.plusR]
Proof state after:
n : Nat
ih : n = Nat.plusR 0 n
⊢ n = Nat.plusR 0 n
Theorem: plusR_zero_left''
Proof state before:
n : Nat
ih : n = Nat.plusR 0 n
⊢ n = Nat.plusR 0 n
Tactic:
assumption
Proof state after:
no goals
Theorem: plusR_zero_left'''
Proof state before:
k : Nat
⊢ k = Nat.plusR 0 k
Tactic:
induction k <;> simp [Nat.plusR] <;> assumption
Proof state after:
no goals
Theorem: non_tail_sum_eq_helper_acumm
Proof state before:
xs : List Nat
⊢ ∀ (n : Nat), n + NonTail.sum xs = Tail.sumHelper n xs
Tactic:
induction xs with
| nil =>
  intro n
  rfl
| cons y ys ih =>
  intro n
  simp [NonTail.sum, Tail.sumHelper]
  rw [← Nat.add_assoc, Nat.add_comm y n]
  exact ih (n + y)
Proof state after:
no goals
Theorem: non_tail_sum_eq_helper_acumm
Proof state before:
case nil

⊢ ∀ (n : Nat), n + NonTail.sum [] = Tail.sumHelper n []
Tactic:
intro n
Proof state after:
case nil
n : Nat
⊢ n + NonTail.sum [] = Tail.sumHelper n []
Theorem: non_tail_sum_eq_helper_acumm
Proof state before:
case nil
n : Nat
⊢ n + NonTail.sum [] = Tail.sumHelper n []
Tactic:
rfl
Proof state after:
no goals
Theorem: non_tail_sum_eq_helper_acumm
Proof state before:
case cons
y : Nat
ys : List Nat
ih : ∀ (n : Nat), n + NonTail.sum ys = Tail.sumHelper n ys
⊢ ∀ (n : Nat), n + NonTail.sum (y :: ys) = Tail.sumHelper n (y :: ys)
Tactic:
intro n
Proof state after:
case cons
y : Nat
ys : List Nat
ih : ∀ (n : Nat), n + NonTail.sum ys = Tail.sumHelper n ys
n : Nat
⊢ n + NonTail.sum (y :: ys) = Tail.sumHelper n (y :: ys)
Theorem: non_tail_sum_eq_helper_acumm
Proof state before:
case cons
y : Nat
ys : List Nat
ih : ∀ (n : Nat), n + NonTail.sum ys = Tail.sumHelper n ys
n : Nat
⊢ n + NonTail.sum (y :: ys) = Tail.sumHelper n (y :: ys)
Tactic:
simp [NonTail.sum, Tail.sumHelper]
Proof state after:
case cons
y : Nat
ys : List Nat
ih : ∀ (n : Nat), n + NonTail.sum ys = Tail.sumHelper n ys
n : Nat
⊢ n + (y + NonTail.sum ys) = Tail.sumHelper (y + n) ys
Theorem: non_tail_sum_eq_helper_acumm
Proof state before:
case cons
y : Nat
ys : List Nat
ih : ∀ (n : Nat), n + NonTail.sum ys = Tail.sumHelper n ys
n : Nat
⊢ n + (y + NonTail.sum ys) = Tail.sumHelper (y + n) ys
Tactic:
rw [← Nat.add_assoc, Nat.add_comm y n]
Proof state after:
case cons
y : Nat
ys : List Nat
ih : ∀ (n : Nat), n + NonTail.sum ys = Tail.sumHelper n ys
n : Nat
⊢ n + y + NonTail.sum ys = Tail.sumHelper (n + y) ys
Theorem: non_tail_sum_eq_helper_acumm
Proof state before:
case cons
y : Nat
ys : List Nat
ih : ∀ (n : Nat), n + NonTail.sum ys = Tail.sumHelper n ys
n : Nat
⊢ n + y + NonTail.sum ys = Tail.sumHelper (n + y) ys
Tactic:
exact ih (n + y)
Proof state after:
no goals
Theorem: non_tail_sum_eq_tail_sum
Proof state before:
⊢ NonTail.sum = Tail.sum
Tactic:
funext xs
Proof state after:
case h
xs : List Nat
⊢ NonTail.sum xs = Tail.sum xs
Theorem: non_tail_sum_eq_tail_sum
Proof state before:
case h
xs : List Nat
⊢ NonTail.sum xs = Tail.sum xs
Tactic:
simp [Tail.sum]
Proof state after:
case h
xs : List Nat
⊢ NonTail.sum xs = Tail.sumHelper 0 xs
Theorem: non_tail_sum_eq_tail_sum
Proof state before:
case h
xs : List Nat
⊢ NonTail.sum xs = Tail.sumHelper 0 xs
Tactic:
rw [← Nat.zero_add (NonTail.sum _)]
Proof state after:
case h
xs : List Nat
⊢ 0 + NonTail.sum xs = Tail.sumHelper 0 xs
Theorem: non_tail_sum_eq_tail_sum
Proof state before:
case h
xs : List Nat
⊢ 0 + NonTail.sum xs = Tail.sumHelper 0 xs
Tactic:
exact non_tail_sum_eq_helper_acumm xs 0
Proof state after:
no goals
Theorem: remove_mem_length
Proof state before:
case cons.inr.a
α : Type u
inst✝ : DecidableEq α
a h' : α
t : List α
ih : a ∈ t → List.length (List.remove a t) < List.length t
hyp : a ∈ h' :: t
h✝ : ¬a = h'
⊢ List.length (List.remove a t) < List.length t
Tactic:
have in_tail: a ∈ t := by 
  have : ¬ a = h' := by assumption
  simp [List.mem_cons, this] at hyp
  assumption
Proof state after:
case cons.inr.a
α : Type u
inst✝ : DecidableEq α
a h' : α
t : List α
ih : a ∈ t → List.length (List.remove a t) < List.length t
hyp : a ∈ h' :: t
h✝ : ¬a = h'
in_tail : a ∈ t
⊢ List.length (List.remove a t) < List.length t
Theorem: totient_of_prime
Proof state before:
p : ℕ
hp : Nat.Prime p
⊢ Nat.totient p = p - 1
Tactic:
rw [Nat.totient_prime hp]
Proof state after:
no goals
Theorem: totient_product_of_two_primes
Proof state before:
p q : ℕ
hp : Nat.Prime p
hq : Nat.Prime q
hr : Nat.coprime p q
⊢ Nat.totient (p * q) = (p - 1) * (q - 1)
Tactic:
have h1 : Nat.totient (p*q) = Nat.totient p * Nat.totient q := by
 rw [Nat.totient_mul hr]
Proof state after:
p q : ℕ
hp : Nat.Prime p
hq : Nat.Prime q
hr : Nat.coprime p q
h1 : Nat.totient (p * q) = Nat.totient p * Nat.totient q
⊢ Nat.totient (p * q) = (p - 1) * (q - 1)
Theorem: totient_product_of_two_primes
Proof state before:
p q : ℕ
hp : Nat.Prime p
hq : Nat.Prime q
hr : Nat.coprime p q
h1 : Nat.totient (p * q) = Nat.totient p * Nat.totient q
⊢ Nat.totient (p * q) = (p - 1) * (q - 1)
Tactic:
have h2 : Nat.totient p * Nat.totient q = (p - 1) * (q - 1) := by
 rw [totient_of_prime p hp, totient_of_prime q hq]
Proof state after:
p q : ℕ
hp : Nat.Prime p
hq : Nat.Prime q
hr : Nat.coprime p q
h1 : Nat.totient (p * q) = Nat.totient p * Nat.totient q
h2 : Nat.totient p * Nat.totient q = (p - 1) * (q - 1)
⊢ Nat.totient (p * q) = (p - 1) * (q - 1)
Theorem: totient_product_of_two_primes
Proof state before:
p q : ℕ
hp : Nat.Prime p
hq : Nat.Prime q
hr : Nat.coprime p q
h1 : Nat.totient (p * q) = Nat.totient p * Nat.totient q
h2 : Nat.totient p * Nat.totient q = (p - 1) * (q - 1)
⊢ Nat.totient (p * q) = (p - 1) * (q - 1)
Tactic:
have h3 : Nat.totient (p*q) = (p - 1) * (q - 1) := by
 rw [h1, h2]
Proof state after:
p q : ℕ
hp : Nat.Prime p
hq : Nat.Prime q
hr : Nat.coprime p q
h1 : Nat.totient (p * q) = Nat.totient p * Nat.totient q
h2 : Nat.totient p * Nat.totient q = (p - 1) * (q - 1)
h3 : Nat.totient (p * q) = (p - 1) * (q - 1)
⊢ Nat.totient (p * q) = (p - 1) * (q - 1)
Theorem: totient_product_of_two_primes
Proof state before:
p q : ℕ
hp : Nat.Prime p
hq : Nat.Prime q
hr : Nat.coprime p q
h1 : Nat.totient (p * q) = Nat.totient p * Nat.totient q
h2 : Nat.totient p * Nat.totient q = (p - 1) * (q - 1)
h3 : Nat.totient (p * q) = (p - 1) * (q - 1)
⊢ Nat.totient (p * q) = (p - 1) * (q - 1)
Tactic:
apply h3
Proof state after:
no goals
Theorem: totient_product_of_two_primes
Proof state before:
p q : ℕ
hp : Nat.Prime p
hq : Nat.Prime q
hr : Nat.coprime p q
⊢ Nat.totient (p * q) = Nat.totient p * Nat.totient q
Tactic:
rw [Nat.totient_mul hr]
Proof state after:
no goals
Theorem: totient_product_of_two_primes
Proof state before:
p q : ℕ
hp : Nat.Prime p
hq : Nat.Prime q
hr : Nat.coprime p q
h1 : Nat.totient (p * q) = Nat.totient p * Nat.totient q
⊢ Nat.totient p * Nat.totient q = (p - 1) * (q - 1)
Tactic:
rw [totient_of_prime p hp, totient_of_prime q hq]
Proof state after:
no goals
Theorem: totient_product_of_two_primes
Proof state before:
p q : ℕ
hp : Nat.Prime p
hq : Nat.Prime q
hr : Nat.coprime p q
h1 : Nat.totient (p * q) = Nat.totient p * Nat.totient q
h2 : Nat.totient p * Nat.totient q = (p - 1) * (q - 1)
⊢ Nat.totient (p * q) = (p - 1) * (q - 1)
Tactic:
rw [h1, h2]
Proof state after:
no goals
Theorem: coprime_product_comprime
Proof state before:
x z y : ℕ
hp : Nat.coprime x z
hq : Nat.coprime y z
⊢ Nat.coprime (x * y) z
Tactic:
apply Nat.coprime.mul hp hq
Proof state after:
no goals