internlm/Lean-Github huggingface dataset:
Theorem: elves_roundtrip
Proof state before:
case cons
hd : List ℤ
tail : List (List ℤ)
ih : stringToElves (elvesToString tail) = tail
⊢ stringToElves (elvesToString (hd :: tail)) = hd :: tail
Tactic:
unfold elvesToString stringToElves
Proof state after:
case cons
hd : List ℤ
tail : List (List ℤ)
ih : stringToElves (elvesToString tail) = tail
⊢ (if
        ((if (hd :: tail == []) = true then []
            else
              List.intercalate [Char.ofNat 10, Char.ofNat 10] (List.map elfToString (hd :: tail)) ++ [Char.ofNat 10]) ==
            []) =
          true then
      []
    else
      List.map stringToElf
        (List.splitOnList [Char.ofNat 10, Char.ofNat 10]
          (if (hd :: tail == []) = true then []
          else
            List.intercalate [Char.ofNat 10, Char.ofNat 10] (List.map elfToString (hd :: tail)) ++ [Char.ofNat 10]))) =
    hd :: tail
Theorem: elves_roundtrip
Proof state before:
case cons
hd : List ℤ
tail : List (List ℤ)
ih : stringToElves (elvesToString tail) = tail
⊢ (if
        ((if (hd :: tail == []) = true then []
            else
              List.intercalate [Char.ofNat 10, Char.ofNat 10] (List.map elfToString (hd :: tail)) ++ [Char.ofNat 10]) ==
            []) =
          true then
      []
    else
      List.map stringToElf
        (List.splitOnList [Char.ofNat 10, Char.ofNat 10]
          (if (hd :: tail == []) = true then []
          else
            List.intercalate [Char.ofNat 10, Char.ofNat 10] (List.map elfToString (hd :: tail)) ++ [Char.ofNat 10]))) =
    hd :: tail
Tactic:
cases tail with
| nil =>
  simp only [beq_iff_eq, List.map, List.intercalate_singleton, ite_false, List.append_eq_nil, and_false]
  rw [List.splitOnList_nonmatching, List.map_singleton, stringToElf_ignoresTrailing, elfToString_roundtrip]
  intro contr
  cases List.isInfix_append_split_left contr with
  | inl h₁ =>
    apply double_newline_not_isInfix_stringToElf hd h₁
  | inr h₂ =>
    simp only [List.length_cons, List.length_singleton, ge_iff_le, Nat.succ_sub_succ_eq_sub, tsub_zero] at h₂
    have newline_in_elf := List.isInfix_take_of_isInfix_append h₂
    simp only [List.take, List.length_nil, zero_add, ge_iff_le, List.lastN_one_eq_getLast,List.singleton_isInfix_iff_mem, Option.mem_toList, Option.mem_def] at newline_in_elf
    apply newline_not_last_elfToString _ newline_in_elf  
| cons mid tl =>
  simp only [beq_iff_eq, List.map, List.map_eq_nil, IsEmpty.forall_iff,
    List.join, ite_false, List.append_eq_nil, and_false, List.intercalate]
  rw [List.append_assoc, List.append_assoc, ← List.append_assoc, List.splitOnList_progress, List.map_append, 
    List.map_singleton, elfToString_roundtrip, List.singleton_append, ←ih, stringToElves, elvesToString, List.intercalate]
  . simp only [List.map_eq_nil, beq_iff_eq, List.map, ite_false, List.append_eq_nil, and_false]
  . simp only [List.dropLast]
    intro contr
    cases List.isInfix_append_split_left contr with
    | inl h₃ =>
      apply double_newline_not_isInfix_stringToElf hd
      apply h₃
    | inr h₄ =>
      simp only [List.length_cons, List.length_singleton, ge_iff_le, Nat.succ_sub_succ_eq_sub, tsub_zero, List.length_nil] at h₄
      have last_contains := List.isInfix_take_of_isInfix_append h₄
      simp only [List.take, ge_iff_le, List.lastN_one_eq_getLast, List.singleton_isInfix_iff_mem, Option.mem_toList, Option.mem_iff] at last_contains
      apply newline_not_last_elfToString _ last_contains
Proof state after:
no goals
Theorem: elves_roundtrip
Proof state before:
case cons.nil
hd : List ℤ
ih : stringToElves (elvesToString []) = []
⊢ (if
        ((if ([hd] == []) = true then []
            else List.intercalate [Char.ofNat 10, Char.ofNat 10] (List.map elfToString [hd]) ++ [Char.ofNat 10]) ==
            []) =
          true then
      []
    else
      List.map stringToElf
        (List.splitOnList [Char.ofNat 10, Char.ofNat 10]
          (if ([hd] == []) = true then []
          else List.intercalate [Char.ofNat 10, Char.ofNat 10] (List.map elfToString [hd]) ++ [Char.ofNat 10]))) =
    [hd]
Tactic:
simp only [beq_iff_eq, List.map, List.intercalate_singleton, ite_false, List.append_eq_nil, and_false]
Proof state after:
case cons.nil
hd : List ℤ
ih : stringToElves (elvesToString []) = []
⊢ List.map stringToElf (List.splitOnList [Char.ofNat 10, Char.ofNat 10] (elfToString hd ++ [Char.ofNat 10])) = [hd]
Theorem: elves_roundtrip
Proof state before:
case cons.nil
hd : List ℤ
ih : stringToElves (elvesToString []) = []
⊢ List.map stringToElf (List.splitOnList [Char.ofNat 10, Char.ofNat 10] (elfToString hd ++ [Char.ofNat 10])) = [hd]
Tactic:
rw [List.splitOnList_nonmatching, List.map_singleton, stringToElf_ignoresTrailing, elfToString_roundtrip]
Proof state after:
case cons.nil.h₁
hd : List ℤ
ih : stringToElves (elvesToString []) = []
⊢ ¬[Char.ofNat 10, Char.ofNat 10] <:+: elfToString hd ++ [Char.ofNat 10]
Theorem: elves_roundtrip
Proof state before:
case cons.nil.h₁
hd : List ℤ
ih : stringToElves (elvesToString []) = []
⊢ ¬[Char.ofNat 10, Char.ofNat 10] <:+: elfToString hd ++ [Char.ofNat 10]
Tactic:
intro contr
Proof state after:
case cons.nil.h₁
hd : List ℤ
ih : stringToElves (elvesToString []) = []
contr : [Char.ofNat 10, Char.ofNat 10] <:+: elfToString hd ++ [Char.ofNat 10]
⊢ False
Theorem: elves_roundtrip
Proof state before:
case cons.nil.h₁
hd : List ℤ
ih : stringToElves (elvesToString []) = []
contr : [Char.ofNat 10, Char.ofNat 10] <:+: elfToString hd ++ [Char.ofNat 10]
⊢ False
Tactic:
cases List.isInfix_append_split_left contr with
| inl h₁ =>
  apply double_newline_not_isInfix_stringToElf hd h₁
| inr h₂ =>
  simp only [List.length_cons, List.length_singleton, ge_iff_le, Nat.succ_sub_succ_eq_sub, tsub_zero] at h₂
  have newline_in_elf := List.isInfix_take_of_isInfix_append h₂
  simp only [List.take, List.length_nil, zero_add, ge_iff_le, List.lastN_one_eq_getLast,List.singleton_isInfix_iff_mem, Option.mem_toList, Option.mem_def] at newline_in_elf
  apply newline_not_last_elfToString _ newline_in_elf
Proof state after:
no goals
Theorem: elves_roundtrip
Proof state before:
case cons.nil.h₁.inl
hd : List ℤ
ih : stringToElves (elvesToString []) = []
contr : [Char.ofNat 10, Char.ofNat 10] <:+: elfToString hd ++ [Char.ofNat 10]
h₁ : [Char.ofNat 10, Char.ofNat 10] <:+: elfToString hd
⊢ False
Tactic:
apply double_newline_not_isInfix_stringToElf hd h₁
Proof state after:
no goals
Theorem: elves_roundtrip
Proof state before:
case cons.nil.h₁.inr
hd : List ℤ
ih : stringToElves (elvesToString []) = []
contr : [Char.ofNat 10, Char.ofNat 10] <:+: elfToString hd ++ [Char.ofNat 10]
h₂ :
  [Char.ofNat 10, Char.ofNat 10] <:+:
    List.lastN (List.length [Char.ofNat 10, Char.ofNat 10] - 1) (elfToString hd) ++ [Char.ofNat 10]
⊢ False
Tactic:
simp only [List.length_cons, List.length_singleton, ge_iff_le, Nat.succ_sub_succ_eq_sub, tsub_zero] at h₂
Proof state after:
case cons.nil.h₁.inr
hd : List ℤ
ih : stringToElves (elvesToString []) = []
contr : [Char.ofNat 10, Char.ofNat 10] <:+: elfToString hd ++ [Char.ofNat 10]
h₂ : [Char.ofNat 10, Char.ofNat 10] <:+: List.lastN (List.length [] + 1) (elfToString hd) ++ [Char.ofNat 10]
⊢ False
Theorem: elves_roundtrip
Proof state before:
case cons.nil.h₁.inr
hd : List ℤ
ih : stringToElves (elvesToString []) = []
contr : [Char.ofNat 10, Char.ofNat 10] <:+: elfToString hd ++ [Char.ofNat 10]
h₂ : [Char.ofNat 10, Char.ofNat 10] <:+: List.lastN (List.length [] + 1) (elfToString hd) ++ [Char.ofNat 10]
⊢ False
Tactic:
have newline_in_elf := List.isInfix_take_of_isInfix_append h₂
Proof state after:
case cons.nil.h₁.inr
hd : List ℤ
ih : stringToElves (elvesToString []) = []
contr : [Char.ofNat 10, Char.ofNat 10] <:+: elfToString hd ++ [Char.ofNat 10]
h₂ : [Char.ofNat 10, Char.ofNat 10] <:+: List.lastN (List.length [] + 1) (elfToString hd) ++ [Char.ofNat 10]
newline_in_elf :
  List.take (List.length [Char.ofNat 10, Char.ofNat 10] - List.length [Char.ofNat 10])
      [Char.ofNat 10, Char.ofNat 10] <:+:
    List.lastN (List.length [] + 1) (elfToString hd)
⊢ False
Theorem: elves_roundtrip
Proof state before:
case cons.nil.h₁.inr
hd : List ℤ
ih : stringToElves (elvesToString []) = []
contr : [Char.ofNat 10, Char.ofNat 10] <:+: elfToString hd ++ [Char.ofNat 10]
h₂ : [Char.ofNat 10, Char.ofNat 10] <:+: List.lastN (List.length [] + 1) (elfToString hd) ++ [Char.ofNat 10]
newline_in_elf :
  List.take (List.length [Char.ofNat 10, Char.ofNat 10] - List.length [Char.ofNat 10])
      [Char.ofNat 10, Char.ofNat 10] <:+:
    List.lastN (List.length [] + 1) (elfToString hd)
⊢ False
Tactic:
simp only [List.take, List.length_nil, zero_add, ge_iff_le, List.lastN_one_eq_getLast,List.singleton_isInfix_iff_mem, Option.mem_toList, Option.mem_def] at newline_in_elf
Proof state after:
case cons.nil.h₁.inr
hd : List ℤ
ih : stringToElves (elvesToString []) = []
contr : [Char.ofNat 10, Char.ofNat 10] <:+: elfToString hd ++ [Char.ofNat 10]
h₂ : [Char.ofNat 10, Char.ofNat 10] <:+: List.lastN (List.length [] + 1) (elfToString hd) ++ [Char.ofNat 10]
newline_in_elf : List.getLast? (elfToString hd) = some (Char.ofNat 10)
⊢ False
Theorem: elves_roundtrip
Proof state before:
case cons.nil.h₁.inr
hd : List ℤ
ih : stringToElves (elvesToString []) = []
contr : [Char.ofNat 10, Char.ofNat 10] <:+: elfToString hd ++ [Char.ofNat 10]
h₂ : [Char.ofNat 10, Char.ofNat 10] <:+: List.lastN (List.length [] + 1) (elfToString hd) ++ [Char.ofNat 10]
newline_in_elf : List.getLast? (elfToString hd) = some (Char.ofNat 10)
⊢ False
Tactic:
apply newline_not_last_elfToString _ newline_in_elf
Proof state after:
no goals
Theorem: elves_roundtrip
Proof state before:
case cons.cons
hd mid : List ℤ
tl : List (List ℤ)
ih : stringToElves (elvesToString (mid :: tl)) = mid :: tl
⊢ (if
        ((if (hd :: mid :: tl == []) = true then []
            else
              List.intercalate [Char.ofNat 10, Char.ofNat 10] (List.map elfToString (hd :: mid :: tl)) ++
                [Char.ofNat 10]) ==
            []) =
          true then
      []
    else
      List.map stringToElf
        (List.splitOnList [Char.ofNat 10, Char.ofNat 10]
          (if (hd :: mid :: tl == []) = true then []
          else
            List.intercalate [Char.ofNat 10, Char.ofNat 10] (List.map elfToString (hd :: mid :: tl)) ++
              [Char.ofNat 10]))) =
    hd :: mid :: tl
Tactic:
simp only [beq_iff_eq, List.map, List.map_eq_nil, IsEmpty.forall_iff,
  List.join, ite_false, List.append_eq_nil, and_false, List.intercalate]
Proof state after:
case cons.cons
hd mid : List ℤ
tl : List (List ℤ)
ih : stringToElves (elvesToString (mid :: tl)) = mid :: tl
⊢ List.map stringToElf
      (List.splitOnList [Char.ofNat 10, Char.ofNat 10]
        (elfToString hd ++
            ([Char.ofNat 10, Char.ofNat 10] ++
              List.join
                (List.intersperse [Char.ofNat 10, Char.ofNat 10] (elfToString mid :: List.map elfToString tl))) ++
          [Char.ofNat 10])) =
    hd :: mid :: tl
Theorem: elves_roundtrip
Proof state before:
case cons.cons
hd mid : List ℤ
tl : List (List ℤ)
ih : stringToElves (elvesToString (mid :: tl)) = mid :: tl
⊢ List.map stringToElf
      (List.splitOnList [Char.ofNat 10, Char.ofNat 10]
        (elfToString hd ++
            ([Char.ofNat 10, Char.ofNat 10] ++
              List.join
                (List.intersperse [Char.ofNat 10, Char.ofNat 10] (elfToString mid :: List.map elfToString tl))) ++
          [Char.ofNat 10])) =
    hd :: mid :: tl
Tactic:
rw [List.append_assoc, List.append_assoc, ← List.append_assoc, List.splitOnList_progress, List.map_append, 
  List.map_singleton, elfToString_roundtrip, List.singleton_append, ←ih, stringToElves, elvesToString, List.intercalate]
Proof state after:
case cons.cons
hd mid : List ℤ
tl : List (List ℤ)
ih : stringToElves (elvesToString (mid :: tl)) = mid :: tl
⊢ hd ::
      List.map stringToElf
        (List.splitOnList [Char.ofNat 10, Char.ofNat 10]
          (List.join (List.intersperse [Char.ofNat 10, Char.ofNat 10] (elfToString mid :: List.map elfToString tl)) ++
            [Char.ofNat 10])) =
    hd ::
      if
          ((if (mid :: tl == []) = true then []
              else
                List.join (List.intersperse [Char.ofNat 10, Char.ofNat 10] (List.map elfToString (mid :: tl))) ++
                  [Char.ofNat 10]) ==
              []) =
            true then
        []
      else
        List.map stringToElf
          (List.splitOnList [Char.ofNat 10, Char.ofNat 10]
            (if (mid :: tl == []) = true then []
            else
              List.join (List.intersperse [Char.ofNat 10, Char.ofNat 10] (List.map elfToString (mid :: tl))) ++
                [Char.ofNat 10]))

case cons.cons
hd mid : List ℤ
tl : List (List ℤ)
ih : stringToElves (elvesToString (mid :: tl)) = mid :: tl
⊢ ¬[Char.ofNat 10, Char.ofNat 10] <:+: elfToString hd ++ List.dropLast [Char.ofNat 10, Char.ofNat 10]
Theorem: elves_roundtrip
Proof state before:
case cons.cons
hd mid : List ℤ
tl : List (List ℤ)
ih : stringToElves (elvesToString (mid :: tl)) = mid :: tl
⊢ hd ::
      List.map stringToElf
        (List.splitOnList [Char.ofNat 10, Char.ofNat 10]
          (List.join (List.intersperse [Char.ofNat 10, Char.ofNat 10] (elfToString mid :: List.map elfToString tl)) ++
            [Char.ofNat 10])) =
    hd ::
      if
          ((if (mid :: tl == []) = true then []
              else
                List.join (List.intersperse [Char.ofNat 10, Char.ofNat 10] (List.map elfToString (mid :: tl))) ++
                  [Char.ofNat 10]) ==
              []) =
            true then
        []
      else
        List.map stringToElf
          (List.splitOnList [Char.ofNat 10, Char.ofNat 10]
            (if (mid :: tl == []) = true then []
            else
              List.join (List.intersperse [Char.ofNat 10, Char.ofNat 10] (List.map elfToString (mid :: tl))) ++
                [Char.ofNat 10]))

case cons.cons
hd mid : List ℤ
tl : List (List ℤ)
ih : stringToElves (elvesToString (mid :: tl)) = mid :: tl
⊢ ¬[Char.ofNat 10, Char.ofNat 10] <:+: elfToString hd ++ List.dropLast [Char.ofNat 10, Char.ofNat 10]
Tactic:
. simp only [List.map_eq_nil, beq_iff_eq, List.map, ite_false, List.append_eq_nil, and_false]
Proof state after:
case cons.cons
hd mid : List ℤ
tl : List (List ℤ)
ih : stringToElves (elvesToString (mid :: tl)) = mid :: tl
⊢ ¬[Char.ofNat 10, Char.ofNat 10] <:+: elfToString hd ++ List.dropLast [Char.ofNat 10, Char.ofNat 10]
Theorem: elves_roundtrip
Proof state before:
case cons.cons
hd mid : List ℤ
tl : List (List ℤ)
ih : stringToElves (elvesToString (mid :: tl)) = mid :: tl
⊢ ¬[Char.ofNat 10, Char.ofNat 10] <:+: elfToString hd ++ List.dropLast [Char.ofNat 10, Char.ofNat 10]
Tactic:
. simp only [List.dropLast]
  intro contr
  cases List.isInfix_append_split_left contr with
  | inl h₃ =>
    apply double_newline_not_isInfix_stringToElf hd
    apply h₃
  | inr h₄ =>
    simp only [List.length_cons, List.length_singleton, ge_iff_le, Nat.succ_sub_succ_eq_sub, tsub_zero, List.length_nil] at h₄
    have last_contains := List.isInfix_take_of_isInfix_append h₄
    simp only [List.take, ge_iff_le, List.lastN_one_eq_getLast, List.singleton_isInfix_iff_mem, Option.mem_toList, Option.mem_iff] at last_contains
    apply newline_not_last_elfToString _ last_contains
Proof state after:
no goals
Theorem: elves_roundtrip
Proof state before:
case cons.cons.inl
hd mid : List ℤ
tl : List (List ℤ)
ih : stringToElves (elvesToString (mid :: tl)) = mid :: tl
contr : [Char.ofNat 10, Char.ofNat 10] <:+: elfToString hd ++ [Char.ofNat 10]
h₃ : [Char.ofNat 10, Char.ofNat 10] <:+: elfToString hd
⊢ False
Tactic:
apply double_newline_not_isInfix_stringToElf hd
Proof state after:
case cons.cons.inl
hd mid : List ℤ
tl : List (List ℤ)
ih : stringToElves (elvesToString (mid :: tl)) = mid :: tl
contr : [Char.ofNat 10, Char.ofNat 10] <:+: elfToString hd ++ [Char.ofNat 10]
h₃ : [Char.ofNat 10, Char.ofNat 10] <:+: elfToString hd
⊢ [Char.ofNat 10, Char.ofNat 10] <:+: elfToString hd
Theorem: elves_roundtrip
Proof state before:
case cons.cons.inl
hd mid : List ℤ
tl : List (List ℤ)
ih : stringToElves (elvesToString (mid :: tl)) = mid :: tl
contr : [Char.ofNat 10, Char.ofNat 10] <:+: elfToString hd ++ [Char.ofNat 10]
h₃ : [Char.ofNat 10, Char.ofNat 10] <:+: elfToString hd
⊢ [Char.ofNat 10, Char.ofNat 10] <:+: elfToString hd
Tactic:
apply h₃
Proof state after:
no goals
Theorem: elves_roundtrip
Proof state before:
case cons.cons.inr
hd mid : List ℤ
tl : List (List ℤ)
ih : stringToElves (elvesToString (mid :: tl)) = mid :: tl
contr : [Char.ofNat 10, Char.ofNat 10] <:+: elfToString hd ++ [Char.ofNat 10]
h₄ :
  [Char.ofNat 10, Char.ofNat 10] <:+:
    List.lastN (List.length [Char.ofNat 10, Char.ofNat 10] - 1) (elfToString hd) ++ [Char.ofNat 10]
⊢ False
Tactic:
simp only [List.length_cons, List.length_singleton, ge_iff_le, Nat.succ_sub_succ_eq_sub, tsub_zero, List.length_nil] at h₄
Proof state after:
case cons.cons.inr
hd mid : List ℤ
tl : List (List ℤ)
ih : stringToElves (elvesToString (mid :: tl)) = mid :: tl
contr : [Char.ofNat 10, Char.ofNat 10] <:+: elfToString hd ++ [Char.ofNat 10]
h₄ : [Char.ofNat 10, Char.ofNat 10] <:+: List.lastN 1 (elfToString hd) ++ [Char.ofNat 10]
⊢ False
Theorem: elves_roundtrip
Proof state before:
case cons.cons.inr
hd mid : List ℤ
tl : List (List ℤ)
ih : stringToElves (elvesToString (mid :: tl)) = mid :: tl
contr : [Char.ofNat 10, Char.ofNat 10] <:+: elfToString hd ++ [Char.ofNat 10]
h₄ : [Char.ofNat 10, Char.ofNat 10] <:+: List.lastN 1 (elfToString hd) ++ [Char.ofNat 10]
⊢ False
Tactic:
have last_contains := List.isInfix_take_of_isInfix_append h₄
Proof state after:
case cons.cons.inr
hd mid : List ℤ
tl : List (List ℤ)
ih : stringToElves (elvesToString (mid :: tl)) = mid :: tl
contr : [Char.ofNat 10, Char.ofNat 10] <:+: elfToString hd ++ [Char.ofNat 10]
h₄ : [Char.ofNat 10, Char.ofNat 10] <:+: List.lastN 1 (elfToString hd) ++ [Char.ofNat 10]
last_contains :
  List.take (List.length [Char.ofNat 10, Char.ofNat 10] - List.length [Char.ofNat 10])
      [Char.ofNat 10, Char.ofNat 10] <:+:
    List.lastN 1 (elfToString hd)
⊢ False
Theorem: elves_roundtrip
Proof state before:
case cons.cons.inr
hd mid : List ℤ
tl : List (List ℤ)
ih : stringToElves (elvesToString (mid :: tl)) = mid :: tl
contr : [Char.ofNat 10, Char.ofNat 10] <:+: elfToString hd ++ [Char.ofNat 10]
h₄ : [Char.ofNat 10, Char.ofNat 10] <:+: List.lastN 1 (elfToString hd) ++ [Char.ofNat 10]
last_contains :
  List.take (List.length [Char.ofNat 10, Char.ofNat 10] - List.length [Char.ofNat 10])
      [Char.ofNat 10, Char.ofNat 10] <:+:
    List.lastN 1 (elfToString hd)
⊢ False
Tactic:
simp only [List.take, ge_iff_le, List.lastN_one_eq_getLast, List.singleton_isInfix_iff_mem, Option.mem_toList, Option.mem_iff] at last_contains
Proof state after:
case cons.cons.inr
hd mid : List ℤ
tl : List (List ℤ)
ih : stringToElves (elvesToString (mid :: tl)) = mid :: tl
contr : [Char.ofNat 10, Char.ofNat 10] <:+: elfToString hd ++ [Char.ofNat 10]
h₄ : [Char.ofNat 10, Char.ofNat 10] <:+: List.lastN 1 (elfToString hd) ++ [Char.ofNat 10]
last_contains : List.getLast? (elfToString hd) = some (Char.ofNat 10)
⊢ False
Theorem: elves_roundtrip
Proof state before:
case cons.cons.inr
hd mid : List ℤ
tl : List (List ℤ)
ih : stringToElves (elvesToString (mid :: tl)) = mid :: tl
contr : [Char.ofNat 10, Char.ofNat 10] <:+: elfToString hd ++ [Char.ofNat 10]
h₄ : [Char.ofNat 10, Char.ofNat 10] <:+: List.lastN 1 (elfToString hd) ++ [Char.ofNat 10]
last_contains : List.getLast? (elfToString hd) = some (Char.ofNat 10)
⊢ False
Tactic:
apply newline_not_last_elfToString _ last_contains
Proof state after:
no goals
Theorem: isSolutionModel_solveOneModel
Proof state before:
⊢ isSolutionModel solveOneModel
Tactic:
unfold isSolutionModel
Proof state after:
⊢ ∀ (elves : List (List ℤ)) (elf : List ℤ), elf ∈ elves → solveOneModel elves ≥ List.sum elf
Theorem: isSolutionModel_solveOneModel
Proof state before:
⊢ ∀ (elves : List (List ℤ)) (elf : List ℤ), elf ∈ elves → solveOneModel elves ≥ List.sum elf
Tactic:
intro elves elf elfin
Proof state after:
elves : List (List ℤ)
elf : List ℤ
elfin : elf ∈ elves
⊢ solveOneModel elves ≥ List.sum elf
Theorem: isSolutionModel_solveOneModel
Proof state before:
elves : List (List ℤ)
elf : List ℤ
elfin : elf ∈ elves
⊢ solveOneModel elves ≥ List.sum elf
Tactic:
unfold solveOneModel
Proof state after:
elves : List (List ℤ)
elf : List ℤ
elfin : elf ∈ elves
⊢ WithBot.unbot' 0 (List.maximum (List.map List.sum elves)) ≥ List.sum elf
Theorem: isSolutionModel_solveOneModel
Proof state before:
elves : List (List ℤ)
elf : List ℤ
elfin : elf ∈ elves
⊢ WithBot.unbot' 0 (List.maximum (List.map List.sum elves)) ≥ List.sum elf
Tactic:
have hsumin: List.sum elf ∈ (List.map List.sum) elves := by apply List.mem_map'.2; exists elf
Proof state after:
elves : List (List ℤ)
elf : List ℤ
elfin : elf ∈ elves
hsumin : List.sum elf ∈ List.map List.sum elves
⊢ WithBot.unbot' 0 (List.maximum (List.map List.sum elves)) ≥ List.sum elf
Theorem: isSolutionModel_solveOneModel
Proof state before:
elves : List (List ℤ)
elf : List ℤ
elfin : elf ∈ elves
hsumin : List.sum elf ∈ List.map List.sum elves
⊢ WithBot.unbot' 0 (List.maximum (List.map List.sum elves)) ≥ List.sum elf
Tactic:
have z:=  List.le_maximum_of_mem' hsumin
Proof state after:
elves : List (List ℤ)
elf : List ℤ
elfin : elf ∈ elves
hsumin : List.sum elf ∈ List.map List.sum elves
z : ↑(List.sum elf) ≤ List.maximum (List.map List.sum elves)
⊢ WithBot.unbot' 0 (List.maximum (List.map List.sum elves)) ≥ List.sum elf
Theorem: isSolutionModel_solveOneModel
Proof state before:
elves : List (List ℤ)
elf : List ℤ
elfin : elf ∈ elves
hsumin : List.sum elf ∈ List.map List.sum elves
z : ↑(List.sum elf) ≤ List.maximum (List.map List.sum elves)
⊢ WithBot.unbot' 0 (List.maximum (List.map List.sum elves)) ≥ List.sum elf
Tactic:
apply WithBot.coe_le_coe.1
Proof state after:
elves : List (List ℤ)
elf : List ℤ
elfin : elf ∈ elves
hsumin : List.sum elf ∈ List.map List.sum elves
z : ↑(List.sum elf) ≤ List.maximum (List.map List.sum elves)
⊢ ↑(List.sum elf) ≤ ↑(WithBot.unbot' 0 (List.maximum (List.map List.sum elves)))
Theorem: isSolutionModel_solveOneModel
Proof state before:
elves : List (List ℤ)
elf : List ℤ
elfin : elf ∈ elves
hsumin : List.sum elf ∈ List.map List.sum elves
z : ↑(List.sum elf) ≤ List.maximum (List.map List.sum elves)
⊢ ↑(List.sum elf) ≤ ↑(WithBot.unbot' 0 (List.maximum (List.map List.sum elves)))
Tactic:
apply le_trans z
Proof state after:
elves : List (List ℤ)
elf : List ℤ
elfin : elf ∈ elves
hsumin : List.sum elf ∈ List.map List.sum elves
z : ↑(List.sum elf) ≤ List.maximum (List.map List.sum elves)
⊢ List.maximum (List.map List.sum elves) ≤ ↑(WithBot.unbot' 0 (List.maximum (List.map List.sum elves)))
Theorem: isSolutionModel_solveOneModel
Proof state before:
elves : List (List ℤ)
elf : List ℤ
elfin : elf ∈ elves
hsumin : List.sum elf ∈ List.map List.sum elves
z : ↑(List.sum elf) ≤ List.maximum (List.map List.sum elves)
⊢ List.maximum (List.map List.sum elves) ≤ ↑(WithBot.unbot' 0 (List.maximum (List.map List.sum elves)))
Tactic:
apply WithBot.le_coe_unbot'
Proof state after:
no goals
Theorem: isSolutionModel_solveOneModel
Proof state before:
elves : List (List ℤ)
elf : List ℤ
elfin : elf ∈ elves
⊢ List.sum elf ∈ List.map List.sum elves
Tactic:
apply List.mem_map'.2
Proof state after:
elves : List (List ℤ)
elf : List ℤ
elfin : elf ∈ elves
⊢ ∃ a, a ∈ elves ∧ List.sum a = List.sum elf
Theorem: isSolutionModel_solveOneModel
Proof state before:
elves : List (List ℤ)
elf : List ℤ
elfin : elf ∈ elves
⊢ ∃ a, a ∈ elves ∧ List.sum a = List.sum elf
Tactic:
exists elf
Proof state after:
no goals
Theorem: isSolution_solveOne
Proof state before:
⊢ isSolution solveOne
Tactic:
unfold isSolution solveOne
Proof state after:
⊢ isSolutionModel ((fun input => solveOneModel (stringToElves input)) ∘ elvesToString)
Theorem: isSolution_solveOne
Proof state before:
⊢ isSolutionModel ((fun input => solveOneModel (stringToElves input)) ∘ elvesToString)
Tactic:
simp [Function.comp, isSolutionModel_solveOneModel, elves_roundtrip]
Proof state after:
no goals
Theorem: divides_of_cong_four
Proof state before:
t : ℕ
⊢ 5 ∣ 4 * (65 * t + 4) ^ 2 + 1 ∧ 13 ∣ 4 * (65 * t + 4) ^ 2 + 1
Tactic:
refine ⟨?_, ?_⟩
Proof state after:
case refine_1
t : ℕ
⊢ 5 ∣ 4 * (65 * t + 4) ^ 2 + 1

case refine_2
t : ℕ
⊢ 13 ∣ 4 * (65 * t + 4) ^ 2 + 1