ex_count_up_tomade with verso-snippets
View
def count_up_to := fun (n : Int) ↦
  (do
    let mut ans : List Int := []
    let mut isprime : List Bool := PastaLean.pyListRepeat [Bool.true] (n +ₚ (1 : Int))
    for i in (PastaLean.pyRange n (2 : Int))do
      let _ := Libraries.passta.pyPassInvariant (decide ((2 : Int) ≤ i))
      let _ := Libraries.passta.pyPassInvariant (decide (i ≤ n))
      let _ := Libraries.passta.pyPassInvariant (PastaLean.pyLen isprime == n +ₚ (1 : Int))
      -- At most one append per counter value.
      let _ := Libraries.passta.pyPassInvariant (decide (PastaLean.pyLen ans ≤ i))
      -- Everything appended so far was a counter value already passed.
      let _ :=
        Libraries.passta.pyPassInvariant (PastaLean.pyAll ((PastaLean.pyIter ans).map fun p => decide ((2 : Int) ≤ p)))
      let _ := Libraries.passta.pyPassInvariant (PastaLean.pyAll ((PastaLean.pyIter ans).map fun p => decide (p < i)))
      if h_1 : PastaLean.pyTruthy isprime⦋i⦌ then 
        ans := PastaLean.pyAppend ans i
        for j in (PastaLean.pyRange n (i +ₚ i) i)do
          -- Index bound for `isprime[j]`.
          let _ := Libraries.passta.pyPassInvariant (decide ((2 : Int) ≤ j))
          let _ := Libraries.passta.pyPassInvariant (decide (j < n))
          isprime := PastaLean.pySetItem isprime j Bool.false
      else
        let _ := ()
    return ans : Id _)

private theorem range_split_val {m : Nat} {pref suff : List Nat} {cur : Nat}
    (h : List.range m = pref ++ cur :: suff) : cur = pref.length := bym:ℕpref:List ℕsuff:List ℕcur:ℕh:List.range m = pref ++ cur :: suff⊢ cur = pref.length
  have h2 : (List.range m)[pref.length]? = some cur := by
    rw [h,m:ℕpref:List ℕsuff:List ℕcur:ℕh:List.range m = pref ++ cur :: suff⊢ (pref ++ cur :: suff)[pref.length]? = some cur List.getElem?_append_right (bym:ℕpref:List ℕsuff:List ℕcur:ℕh:List.range m = pref ++ cur :: suff⊢ pref.length ≤ pref.length omegaAll goals completed! 🐙)]m:ℕpref:List ℕsuff:List ℕcur:ℕh:List.range m = pref ++ cur :: suff⊢ (cur :: suff)[pref.length - pref.length]? = some cur; simpm:ℕpref:List ℕsuff:List ℕcur:ℕh:List.range m = pref ++ cur :: suffh2:(List.range m)[pref.length]? = some cur⊢ cur = pref.length
  have h3 : pref.length < m := by
    have := congrArg List.length hm:ℕpref:List ℕsuff:List ℕcur:ℕh:List.range m = pref ++ cur :: suffh2:(List.range m)[pref.length]? = some curthis:(List.range m).length = (pref ++ cur :: suff).length⊢ pref.length < m; simp at thism:ℕpref:List ℕsuff:List ℕcur:ℕh:List.range m = pref ++ cur :: suffh2:(List.range m)[pref.length]? = some curthis:m = pref.length + (suff.length + 1)⊢ pref.length < m; omegam:ℕpref:List ℕsuff:List ℕcur:ℕh:List.range m = pref ++ cur :: suffh2:(List.range m)[pref.length]? = some curh3:pref.length < m⊢ cur = pref.length
  rw [List.getElem?_range h3m:ℕpref:List ℕsuff:List ℕcur:ℕh:List.range m = pref ++ cur :: suffh2:some pref.length = some curh3:pref.length < m⊢ cur = pref.length] at h2m:ℕpref:List ℕsuff:List ℕcur:ℕh:List.range m = pref ++ cur :: suffh2:some pref.length = some curh3:pref.length < m⊢ cur = pref.length; simp at h2m:ℕpref:List ℕsuff:List ℕcur:ℕh:List.range m = pref ++ cur :: suffh3:pref.length < mh2:pref.length = cur⊢ cur = pref.length; omegaAll goals completed! 🐙

@[spec]
theorem count_up_to_spec :
    ⦃⌜n ≥ (0 : Int)⌝⦄ count_up_to n ⦃⇓ans =>
      ⌜(PastaLean.pyLen ans ≤ n ∧ ∀ p ∈ PastaLean.pyIter ans, (2 : Int) ≤ p) ∧ ∀ p ∈ PastaLean.pyIter ans, p < n⌝⦄ :=
  byn:ℤ⊢ ⦃⌜n ≥ 0⌝⦄
  count_up_to n ⦃PostCond.noThrow fun ans => ⌜(pyLen ans ≤ n ∧ ∀ p ∈ pyIter ans, 2 ≤ p) ∧ ∀ p ∈ pyIter ans, p < n⌝⦄
  mvcgen [count_up_to, PastaLean.pyRange_forIn, PastaLean.pyRange_forIn_start] invariants
  · ⇓⟨cur, ans, isprime⟩ =>
    ⌜(PastaLean.pyLen ans ≤ (cur.prefix.length : Int)) ∧
      (∀ p ∈ PastaLean.pyIter ans, (2 : Int) ≤ p) ∧
      (∀ p ∈ PastaLean.pyIter ans, p < (2 : Int) + (cur.prefix.length : Int))⌝
  · ⇓⟨cur, isprime⟩ => ⌜True⌝vc3.step.isTrue.post.successn:ℤans✝²:List ℤ := []isprime✝¹:List Bool := pyListRepeat [true] (n +ₚ 1)h✝⁴:n ≥ 0pref✝:List ℕcur✝:ℕsuff✝:List ℕh✝³:List.range (n - 2).toNat = pref✝ ++ cur✝ :: suff✝b✝:MProd (List ℤ) (List Bool)ans✝¹:List ℤ := b✝.fstisprime✝:List Bool := b✝.sndh✝²:pyTruthy isprime✝⦋2 + Int.ofNat cur✝⦌ = trueans✝:List ℤ := pyAppend ans✝¹ (2 + Int.ofNat cur✝)h✝¹:pyLen b✝.fst ≤ ↑pref✝.length ∧ (∀ p ∈ pyIter b✝.fst, 2 ≤ p) ∧ ∀ p ∈ pyIter b✝.fst, p < 2 + ↑pref✝.lengthr✝:List Boolh✝:True⊢ pyLen ans✝ ≤ ↑(pref✝ ++ [cur✝]).length ∧
  (∀ p ∈ pyIter ans✝, 2 ≤ p) ∧ ∀ p ∈ pyIter ans✝, p < 2 + ↑(pref✝ ++ [cur✝]).lengthvc4.step.isFalsen:ℤans✝¹:List ℤ := []isprime✝¹:List Bool := pyListRepeat [true] (n +ₚ 1)h✝³:n ≥ 0pref✝:List ℕcur✝:ℕsuff✝:List ℕh✝²:List.range (n - 2).toNat = pref✝ ++ cur✝ :: suff✝b✝:MProd (List ℤ) (List Bool)ans✝:List ℤ := b✝.fstisprime✝:List Bool := b✝.sndh✝¹:¬pyTruthy isprime✝⦋2 + Int.ofNat cur✝⦌ = trueh✝:pyLen b✝.fst ≤ ↑pref✝.length ∧ (∀ p ∈ pyIter b✝.fst, 2 ≤ p) ∧ ∀ p ∈ pyIter b✝.fst, p < 2 + ↑pref✝.length⊢ pyLen ans✝ ≤ ↑(pref✝ ++ [cur✝]).length ∧
  (∀ p ∈ pyIter ans✝, 2 ≤ p) ∧ ∀ p ∈ pyIter ans✝, p < 2 + ↑(pref✝ ++ [cur✝]).lengthvc5.pren:ℤans✝:List ℤ := []isprime✝:List Bool := pyListRepeat [true] (n +ₚ 1)h✝:n ≥ 0⊢ pyLen ans✝ ≤ ↑[].length ∧ (∀ p ∈ pyIter ans✝, 2 ≤ p) ∧ ∀ p ∈ pyIter ans✝, p < 2 + ↑[].lengthvc6.post.successn:ℤans✝:List ℤ := []isprime✝:List Bool := pyListRepeat [true] (n +ₚ 1)h✝¹:n ≥ 0r✝:MProd (List ℤ) (List Bool)h✝:pyLen r✝.fst ≤ ↑(List.range (n - 2).toNat).length ∧
  (∀ p ∈ pyIter r✝.fst, 2 ≤ p) ∧ ∀ p ∈ pyIter r✝.fst, p < 2 + ↑(List.range (n - 2).toNat).length⊢ (pyLen r✝.fst ≤ n ∧ ∀ p ∈ pyIter r✝.fst, 2 ≤ p) ∧ ∀ p ∈ pyIter r✝.fst, p < n
  all_goals (try (simp_all (config := { zetaDelta := true }) [taste_ingr, PastaLean.pyAppend, PastaLean.pyListAppend]vc6.post.successn:ℤans✝:List ℤ := []isprime✝:List Bool := pyListRepeat [true] (n +ₚ 1)r✝:MProd (List ℤ) (List Bool)h✝¹:0 ≤ nh✝:(pyLen r✝.fst ≤ n - 2 ∨ pyLen r✝.fst ≤ 0) ∧ (∀ p ∈ r✝.fst, 2 ≤ p) ∧ ∀ p ∈ r✝.fst, p < 2 + max (n - 2) 0⊢ pyLen r✝.fst ≤ n ∧ ∀ p ∈ r✝.fst, p < n))
  case vc3.step.isTrue.post.success =>n:ℤans✝²:List ℤ := []isprime✝¹:List Bool := pyListRepeat [true] (n +ₚ 1)pref✝:List ℕcur✝:ℕsuff✝:List ℕb✝:MProd (List ℤ) (List Bool)ans✝¹:List ℤ := b✝.fstisprime✝:List Bool := b✝.sndans✝:List ℤ := pyAppend ans✝¹ (2 + Int.ofNat cur✝)r✝:List Boolh✝³:0 ≤ nh✝²:List.range (n - 2).toNat = pref✝ ++ cur✝ :: suff✝h✝¹:b✝.snd⦋2 + ↑cur✝⦌ = trueh✝:pyLen b✝.fst ≤ ↑pref✝.length ∧ (∀ p ∈ b✝.fst, 2 ≤ p) ∧ ∀ p ∈ b✝.fst, p < 2 + ↑pref✝.length⊢ pyLen (b✝.fst ++ [2 + ↑cur✝]) ≤ ↑pref✝.length + 1 ∧
  (∀ (p : ℤ), p ∈ b✝.fst ∨ p = 2 + ↑cur✝ → 2 ≤ p) ∧ ∀ (p : ℤ), p ∈ b✝.fst ∨ p = 2 + ↑cur✝ → p < 2 + (↑pref✝.length + 1)
    have hcur := range_split_val ‹List.range _ = _ ++ _ :: _›n:ℤans✝²:List ℤ := []isprime✝¹:List Bool := pyListRepeat [true] (n +ₚ 1)pref✝:List ℕcur✝:ℕsuff✝:List ℕb✝:MProd (List ℤ) (List Bool)ans✝¹:List ℤ := b✝.fstisprime✝:List Bool := b✝.sndans✝:List ℤ := pyAppend ans✝¹ (2 + Int.ofNat cur✝)r✝:List Boolh✝³:0 ≤ nh✝²:List.range (n - 2).toNat = pref✝ ++ cur✝ :: suff✝h✝¹:b✝.snd⦋2 + ↑cur✝⦌ = trueh✝:pyLen b✝.fst ≤ ↑pref✝.length ∧ (∀ p ∈ b✝.fst, 2 ≤ p) ∧ ∀ p ∈ b✝.fst, p < 2 + ↑pref✝.lengthhcur:cur✝ = pref✝.length⊢ pyLen (b✝.fst ++ [2 + ↑cur✝]) ≤ ↑pref✝.length + 1 ∧
  (∀ (p : ℤ), p ∈ b✝.fst ∨ p = 2 + ↑cur✝ → 2 ≤ p) ∧ ∀ (p : ℤ), p ∈ b✝.fst ∨ p = 2 + ↑cur✝ → p < 2 + (↑pref✝.length + 1)
    obtain ⟨hlen, h2, h3⟩ := ‹PastaLean.pyLen _ ≤ _ ∧ _›n:ℤans✝²:List ℤ := []isprime✝¹:List Bool := pyListRepeat [true] (n +ₚ 1)pref✝:List ℕcur✝:ℕsuff✝:List ℕb✝:MProd (List ℤ) (List Bool)ans✝¹:List ℤ := b✝.fstisprime✝:List Bool := b✝.sndans✝:List ℤ := pyAppend ans✝¹ (2 + Int.ofNat cur✝)r✝:List Boolh✝³:0 ≤ nh✝²:List.range (n - 2).toNat = pref✝ ++ cur✝ :: suff✝h✝¹:b✝.snd⦋2 + ↑cur✝⦌ = trueh✝:pyLen b✝.fst ≤ ↑pref✝.length ∧ (∀ p ∈ b✝.fst, 2 ≤ p) ∧ ∀ p ∈ b✝.fst, p < 2 + ↑pref✝.lengthhcur:cur✝ = pref✝.lengthhlen:pyLen b✝.fst ≤ ↑pref✝.lengthh2:∀ p ∈ b✝.fst, 2 ≤ ph3:∀ p ∈ b✝.fst, p < 2 + ↑pref✝.length⊢ pyLen (b✝.fst ++ [2 + ↑cur✝]) ≤ ↑pref✝.length + 1 ∧
  (∀ (p : ℤ), p ∈ b✝.fst ∨ p = 2 + ↑cur✝ → 2 ≤ p) ∧ ∀ (p : ℤ), p ∈ b✝.fst ∨ p = 2 + ↑cur✝ → p < 2 + (↑pref✝.length + 1)
    simp only [PastaLean.pyLen, PastaLean.PyLen.pyLen, List.length_append,
      List.length_cons, List.length_nil] at hlen ⊢n:ℤans✝²:List ℤ := []isprime✝¹:List Bool := pyListRepeat [true] (n +ₚ 1)pref✝:List ℕcur✝:ℕsuff✝:List ℕb✝:MProd (List ℤ) (List Bool)ans✝¹:List ℤ := b✝.fstisprime✝:List Bool := b✝.sndans✝:List ℤ := pyAppend ans✝¹ (2 + Int.ofNat cur✝)r✝:List Boolh✝³:0 ≤ nh✝²:List.range (n - 2).toNat = pref✝ ++ cur✝ :: suff✝h✝¹:b✝.snd⦋2 + ↑cur✝⦌ = trueh✝:pyLen b✝.fst ≤ ↑pref✝.length ∧ (∀ p ∈ b✝.fst, 2 ≤ p) ∧ ∀ p ∈ b✝.fst, p < 2 + ↑pref✝.lengthhcur:cur✝ = pref✝.lengthhlen:↑b✝.fst.length ≤ ↑pref✝.lengthh2:∀ p ∈ b✝.fst, 2 ≤ ph3:∀ p ∈ b✝.fst, p < 2 + ↑pref✝.length⊢ ↑(b✝.fst.length + (0 + 1)) ≤ ↑pref✝.length + 1 ∧
  (∀ (p : ℤ), p ∈ b✝.fst ∨ p = 2 + ↑cur✝ → 2 ≤ p) ∧ ∀ (p : ℤ), p ∈ b✝.fst ∨ p = 2 + ↑cur✝ → p < 2 + (↑pref✝.length + 1)
    refine ⟨byn:ℤans✝²:List ℤ := []isprime✝¹:List Bool := pyListRepeat [true] (n +ₚ 1)pref✝:List ℕcur✝:ℕsuff✝:List ℕb✝:MProd (List ℤ) (List Bool)ans✝¹:List ℤ := b✝.fstisprime✝:List Bool := b✝.sndans✝:List ℤ := pyAppend ans✝¹ (2 + Int.ofNat cur✝)r✝:List Boolh✝³:0 ≤ nh✝²:List.range (n - 2).toNat = pref✝ ++ cur✝ :: suff✝h✝¹:b✝.snd⦋2 + ↑cur✝⦌ = trueh✝:pyLen b✝.fst ≤ ↑pref✝.length ∧ (∀ p ∈ b✝.fst, 2 ≤ p) ∧ ∀ p ∈ b✝.fst, p < 2 + ↑pref✝.lengthhcur:cur✝ = pref✝.lengthhlen:↑b✝.fst.length ≤ ↑pref✝.lengthh2:∀ p ∈ b✝.fst, 2 ≤ ph3:∀ p ∈ b✝.fst, p < 2 + ↑pref✝.length⊢ ↑(b✝.fst.length + (0 + 1)) ≤ ↑pref✝.length + 1 omegaAll goals completed! 🐙, ?_, ?_⟩
    ·refine_1n:ℤans✝²:List ℤ := []isprime✝¹:List Bool := pyListRepeat [true] (n +ₚ 1)pref✝:List ℕcur✝:ℕsuff✝:List ℕb✝:MProd (List ℤ) (List Bool)ans✝¹:List ℤ := b✝.fstisprime✝:List Bool := b✝.sndans✝:List ℤ := pyAppend ans✝¹ (2 + Int.ofNat cur✝)r✝:List Boolh✝³:0 ≤ nh✝²:List.range (n - 2).toNat = pref✝ ++ cur✝ :: suff✝h✝¹:b✝.snd⦋2 + ↑cur✝⦌ = trueh✝:pyLen b✝.fst ≤ ↑pref✝.length ∧ (∀ p ∈ b✝.fst, 2 ≤ p) ∧ ∀ p ∈ b✝.fst, p < 2 + ↑pref✝.lengthhcur:cur✝ = pref✝.lengthhlen:↑b✝.fst.length ≤ ↑pref✝.lengthh2:∀ p ∈ b✝.fst, 2 ≤ ph3:∀ p ∈ b✝.fst, p < 2 + ↑pref✝.length⊢ ∀ (p : ℤ), p ∈ b✝.fst ∨ p = 2 + ↑cur✝ → 2 ≤ p rintro p (hp | rfl)refine_1.inln:ℤans✝²:List ℤ := []isprime✝¹:List Bool := pyListRepeat [true] (n +ₚ 1)pref✝:List ℕcur✝:ℕsuff✝:List ℕb✝:MProd (List ℤ) (List Bool)ans✝¹:List ℤ := b✝.fstisprime✝:List Bool := b✝.sndans✝:List ℤ := pyAppend ans✝¹ (2 + Int.ofNat cur✝)r✝:List Boolh✝³:0 ≤ nh✝²:List.range (n - 2).toNat = pref✝ ++ cur✝ :: suff✝h✝¹:b✝.snd⦋2 + ↑cur✝⦌ = trueh✝:pyLen b✝.fst ≤ ↑pref✝.length ∧ (∀ p ∈ b✝.fst, 2 ≤ p) ∧ ∀ p ∈ b✝.fst, p < 2 + ↑pref✝.lengthhcur:cur✝ = pref✝.lengthhlen:↑b✝.fst.length ≤ ↑pref✝.lengthh2:∀ p ∈ b✝.fst, 2 ≤ ph3:∀ p ∈ b✝.fst, p < 2 + ↑pref✝.lengthp:ℤhp:p ∈ b✝.fst⊢ 2 ≤ prefine_1.inrn:ℤans✝²:List ℤ := []isprime✝¹:List Bool := pyListRepeat [true] (n +ₚ 1)pref✝:List ℕcur✝:ℕsuff✝:List ℕb✝:MProd (List ℤ) (List Bool)ans✝¹:List ℤ := b✝.fstisprime✝:List Bool := b✝.sndans✝:List ℤ := pyAppend ans✝¹ (2 + Int.ofNat cur✝)r✝:List Boolh✝³:0 ≤ nh✝²:List.range (n - 2).toNat = pref✝ ++ cur✝ :: suff✝h✝¹:b✝.snd⦋2 + ↑cur✝⦌ = trueh✝:pyLen b✝.fst ≤ ↑pref✝.length ∧ (∀ p ∈ b✝.fst, 2 ≤ p) ∧ ∀ p ∈ b✝.fst, p < 2 + ↑pref✝.lengthhcur:cur✝ = pref✝.lengthhlen:↑b✝.fst.length ≤ ↑pref✝.lengthh2:∀ p ∈ b✝.fst, 2 ≤ ph3:∀ p ∈ b✝.fst, p < 2 + ↑pref✝.length⊢ 2 ≤ 2 + ↑cur✝
      ·refine_1.inln:ℤans✝²:List ℤ := []isprime✝¹:List Bool := pyListRepeat [true] (n +ₚ 1)pref✝:List ℕcur✝:ℕsuff✝:List ℕb✝:MProd (List ℤ) (List Bool)ans✝¹:List ℤ := b✝.fstisprime✝:List Bool := b✝.sndans✝:List ℤ := pyAppend ans✝¹ (2 + Int.ofNat cur✝)r✝:List Boolh✝³:0 ≤ nh✝²:List.range (n - 2).toNat = pref✝ ++ cur✝ :: suff✝h✝¹:b✝.snd⦋2 + ↑cur✝⦌ = trueh✝:pyLen b✝.fst ≤ ↑pref✝.length ∧ (∀ p ∈ b✝.fst, 2 ≤ p) ∧ ∀ p ∈ b✝.fst, p < 2 + ↑pref✝.lengthhcur:cur✝ = pref✝.lengthhlen:↑b✝.fst.length ≤ ↑pref✝.lengthh2:∀ p ∈ b✝.fst, 2 ≤ ph3:∀ p ∈ b✝.fst, p < 2 + ↑pref✝.lengthp:ℤhp:p ∈ b✝.fst⊢ 2 ≤ p exact h2 p hpAll goals completed! 🐙
      ·refine_1.inrn:ℤans✝²:List ℤ := []isprime✝¹:List Bool := pyListRepeat [true] (n +ₚ 1)pref✝:List ℕcur✝:ℕsuff✝:List ℕb✝:MProd (List ℤ) (List Bool)ans✝¹:List ℤ := b✝.fstisprime✝:List Bool := b✝.sndans✝:List ℤ := pyAppend ans✝¹ (2 + Int.ofNat cur✝)r✝:List Boolh✝³:0 ≤ nh✝²:List.range (n - 2).toNat = pref✝ ++ cur✝ :: suff✝h✝¹:b✝.snd⦋2 + ↑cur✝⦌ = trueh✝:pyLen b✝.fst ≤ ↑pref✝.length ∧ (∀ p ∈ b✝.fst, 2 ≤ p) ∧ ∀ p ∈ b✝.fst, p < 2 + ↑pref✝.lengthhcur:cur✝ = pref✝.lengthhlen:↑b✝.fst.length ≤ ↑pref✝.lengthh2:∀ p ∈ b✝.fst, 2 ≤ ph3:∀ p ∈ b✝.fst, p < 2 + ↑pref✝.length⊢ 2 ≤ 2 + ↑cur✝ omegaAll goals completed! 🐙
    ·refine_2n:ℤans✝²:List ℤ := []isprime✝¹:List Bool := pyListRepeat [true] (n +ₚ 1)pref✝:List ℕcur✝:ℕsuff✝:List ℕb✝:MProd (List ℤ) (List Bool)ans✝¹:List ℤ := b✝.fstisprime✝:List Bool := b✝.sndans✝:List ℤ := pyAppend ans✝¹ (2 + Int.ofNat cur✝)r✝:List Boolh✝³:0 ≤ nh✝²:List.range (n - 2).toNat = pref✝ ++ cur✝ :: suff✝h✝¹:b✝.snd⦋2 + ↑cur✝⦌ = trueh✝:pyLen b✝.fst ≤ ↑pref✝.length ∧ (∀ p ∈ b✝.fst, 2 ≤ p) ∧ ∀ p ∈ b✝.fst, p < 2 + ↑pref✝.lengthhcur:cur✝ = pref✝.lengthhlen:↑b✝.fst.length ≤ ↑pref✝.lengthh2:∀ p ∈ b✝.fst, 2 ≤ ph3:∀ p ∈ b✝.fst, p < 2 + ↑pref✝.length⊢ ∀ (p : ℤ), p ∈ b✝.fst ∨ p = 2 + ↑cur✝ → p < 2 + (↑pref✝.length + 1) rintro p (hp | rfl)refine_2.inln:ℤans✝²:List ℤ := []isprime✝¹:List Bool := pyListRepeat [true] (n +ₚ 1)pref✝:List ℕcur✝:ℕsuff✝:List ℕb✝:MProd (List ℤ) (List Bool)ans✝¹:List ℤ := b✝.fstisprime✝:List Bool := b✝.sndans✝:List ℤ := pyAppend ans✝¹ (2 + Int.ofNat cur✝)r✝:List Boolh✝³:0 ≤ nh✝²:List.range (n - 2).toNat = pref✝ ++ cur✝ :: suff✝h✝¹:b✝.snd⦋2 + ↑cur✝⦌ = trueh✝:pyLen b✝.fst ≤ ↑pref✝.length ∧ (∀ p ∈ b✝.fst, 2 ≤ p) ∧ ∀ p ∈ b✝.fst, p < 2 + ↑pref✝.lengthhcur:cur✝ = pref✝.lengthhlen:↑b✝.fst.length ≤ ↑pref✝.lengthh2:∀ p ∈ b✝.fst, 2 ≤ ph3:∀ p ∈ b✝.fst, p < 2 + ↑pref✝.lengthp:ℤhp:p ∈ b✝.fst⊢ p < 2 + (↑pref✝.length + 1)refine_2.inrn:ℤans✝²:List ℤ := []isprime✝¹:List Bool := pyListRepeat [true] (n +ₚ 1)pref✝:List ℕcur✝:ℕsuff✝:List ℕb✝:MProd (List ℤ) (List Bool)ans✝¹:List ℤ := b✝.fstisprime✝:List Bool := b✝.sndans✝:List ℤ := pyAppend ans✝¹ (2 + Int.ofNat cur✝)r✝:List Boolh✝³:0 ≤ nh✝²:List.range (n - 2).toNat = pref✝ ++ cur✝ :: suff✝h✝¹:b✝.snd⦋2 + ↑cur✝⦌ = trueh✝:pyLen b✝.fst ≤ ↑pref✝.length ∧ (∀ p ∈ b✝.fst, 2 ≤ p) ∧ ∀ p ∈ b✝.fst, p < 2 + ↑pref✝.lengthhcur:cur✝ = pref✝.lengthhlen:↑b✝.fst.length ≤ ↑pref✝.lengthh2:∀ p ∈ b✝.fst, 2 ≤ ph3:∀ p ∈ b✝.fst, p < 2 + ↑pref✝.length⊢ 2 + ↑cur✝ < 2 + (↑pref✝.length + 1)
      ·refine_2.inln:ℤans✝²:List ℤ := []isprime✝¹:List Bool := pyListRepeat [true] (n +ₚ 1)pref✝:List ℕcur✝:ℕsuff✝:List ℕb✝:MProd (List ℤ) (List Bool)ans✝¹:List ℤ := b✝.fstisprime✝:List Bool := b✝.sndans✝:List ℤ := pyAppend ans✝¹ (2 + Int.ofNat cur✝)r✝:List Boolh✝³:0 ≤ nh✝²:List.range (n - 2).toNat = pref✝ ++ cur✝ :: suff✝h✝¹:b✝.snd⦋2 + ↑cur✝⦌ = trueh✝:pyLen b✝.fst ≤ ↑pref✝.length ∧ (∀ p ∈ b✝.fst, 2 ≤ p) ∧ ∀ p ∈ b✝.fst, p < 2 + ↑pref✝.lengthhcur:cur✝ = pref✝.lengthhlen:↑b✝.fst.length ≤ ↑pref✝.lengthh2:∀ p ∈ b✝.fst, 2 ≤ ph3:∀ p ∈ b✝.fst, p < 2 + ↑pref✝.lengthp:ℤhp:p ∈ b✝.fst⊢ p < 2 + (↑pref✝.length + 1) have := h3 p hprefine_2.inln:ℤans✝²:List ℤ := []isprime✝¹:List Bool := pyListRepeat [true] (n +ₚ 1)pref✝:List ℕcur✝:ℕsuff✝:List ℕb✝:MProd (List ℤ) (List Bool)ans✝¹:List ℤ := b✝.fstisprime✝:List Bool := b✝.sndans✝:List ℤ := pyAppend ans✝¹ (2 + Int.ofNat cur✝)r✝:List Boolh✝³:0 ≤ nh✝²:List.range (n - 2).toNat = pref✝ ++ cur✝ :: suff✝h✝¹:b✝.snd⦋2 + ↑cur✝⦌ = trueh✝:pyLen b✝.fst ≤ ↑pref✝.length ∧ (∀ p ∈ b✝.fst, 2 ≤ p) ∧ ∀ p ∈ b✝.fst, p < 2 + ↑pref✝.lengthhcur:cur✝ = pref✝.lengthhlen:↑b✝.fst.length ≤ ↑pref✝.lengthh2:∀ p ∈ b✝.fst, 2 ≤ ph3:∀ p ∈ b✝.fst, p < 2 + ↑pref✝.lengthp:ℤhp:p ∈ b✝.fstthis:p < 2 + ↑pref✝.length⊢ p < 2 + (↑pref✝.length + 1); omegaAll goals completed! 🐙
      ·refine_2.inrn:ℤans✝²:List ℤ := []isprime✝¹:List Bool := pyListRepeat [true] (n +ₚ 1)pref✝:List ℕcur✝:ℕsuff✝:List ℕb✝:MProd (List ℤ) (List Bool)ans✝¹:List ℤ := b✝.fstisprime✝:List Bool := b✝.sndans✝:List ℤ := pyAppend ans✝¹ (2 + Int.ofNat cur✝)r✝:List Boolh✝³:0 ≤ nh✝²:List.range (n - 2).toNat = pref✝ ++ cur✝ :: suff✝h✝¹:b✝.snd⦋2 + ↑cur✝⦌ = trueh✝:pyLen b✝.fst ≤ ↑pref✝.length ∧ (∀ p ∈ b✝.fst, 2 ≤ p) ∧ ∀ p ∈ b✝.fst, p < 2 + ↑pref✝.lengthhcur:cur✝ = pref✝.lengthhlen:↑b✝.fst.length ≤ ↑pref✝.lengthh2:∀ p ∈ b✝.fst, 2 ≤ ph3:∀ p ∈ b✝.fst, p < 2 + ↑pref✝.length⊢ 2 + ↑cur✝ < 2 + (↑pref✝.length + 1) omegaAll goals completed! 🐙
  case vc4.step.isFalse =>n:ℤans✝¹:List ℤ := []isprime✝¹:List Bool := pyListRepeat [true] (n +ₚ 1)pref✝:List ℕcur✝:ℕsuff✝:List ℕb✝:MProd (List ℤ) (List Bool)ans✝:List ℤ := b✝.fstisprime✝:List Bool := b✝.sndh✝³:0 ≤ nh✝²:List.range (n - 2).toNat = pref✝ ++ cur✝ :: suff✝h✝¹:b✝.snd⦋2 + ↑cur✝⦌ = falseh✝:pyLen b✝.fst ≤ ↑pref✝.length ∧ (∀ p ∈ b✝.fst, 2 ≤ p) ∧ ∀ p ∈ b✝.fst, p < 2 + ↑pref✝.length⊢ pyLen b✝.fst ≤ ↑pref✝.length + 1 ∧ ∀ p ∈ b✝.fst, p < 2 + (↑pref✝.length + 1)
    obtain ⟨hlen, h2, h3⟩ := ‹PastaLean.pyLen _ ≤ _ ∧ _›n:ℤans✝¹:List ℤ := []isprime✝¹:List Bool := pyListRepeat [true] (n +ₚ 1)pref✝:List ℕcur✝:ℕsuff✝:List ℕb✝:MProd (List ℤ) (List Bool)ans✝:List ℤ := b✝.fstisprime✝:List Bool := b✝.sndh✝³:0 ≤ nh✝²:List.range (n - 2).toNat = pref✝ ++ cur✝ :: suff✝h✝¹:b✝.snd⦋2 + ↑cur✝⦌ = falseh✝:pyLen b✝.fst ≤ ↑pref✝.length ∧ (∀ p ∈ b✝.fst, 2 ≤ p) ∧ ∀ p ∈ b✝.fst, p < 2 + ↑pref✝.lengthhlen:pyLen b✝.fst ≤ ↑pref✝.lengthh2:∀ p ∈ b✝.fst, 2 ≤ ph3:∀ p ∈ b✝.fst, p < 2 + ↑pref✝.length⊢ pyLen b✝.fst ≤ ↑pref✝.length + 1 ∧ ∀ p ∈ b✝.fst, p < 2 + (↑pref✝.length + 1)
    simp only [PastaLean.pyLen, PastaLean.PyLen.pyLen] at hlen ⊢n:ℤans✝¹:List ℤ := []isprime✝¹:List Bool := pyListRepeat [true] (n +ₚ 1)pref✝:List ℕcur✝:ℕsuff✝:List ℕb✝:MProd (List ℤ) (List Bool)ans✝:List ℤ := b✝.fstisprime✝:List Bool := b✝.sndh✝³:0 ≤ nh✝²:List.range (n - 2).toNat = pref✝ ++ cur✝ :: suff✝h✝¹:b✝.snd⦋2 + ↑cur✝⦌ = falseh✝:pyLen b✝.fst ≤ ↑pref✝.length ∧ (∀ p ∈ b✝.fst, 2 ≤ p) ∧ ∀ p ∈ b✝.fst, p < 2 + ↑pref✝.lengthhlen:↑b✝.fst.length ≤ ↑pref✝.lengthh2:∀ p ∈ b✝.fst, 2 ≤ ph3:∀ p ∈ b✝.fst, p < 2 + ↑pref✝.length⊢ ↑b✝.fst.length ≤ ↑pref✝.length + 1 ∧ ∀ p ∈ b✝.fst, p < 2 + (↑pref✝.length + 1)
    refine ⟨byn:ℤans✝¹:List ℤ := []isprime✝¹:List Bool := pyListRepeat [true] (n +ₚ 1)pref✝:List ℕcur✝:ℕsuff✝:List ℕb✝:MProd (List ℤ) (List Bool)ans✝:List ℤ := b✝.fstisprime✝:List Bool := b✝.sndh✝³:0 ≤ nh✝²:List.range (n - 2).toNat = pref✝ ++ cur✝ :: suff✝h✝¹:b✝.snd⦋2 + ↑cur✝⦌ = falseh✝:pyLen b✝.fst ≤ ↑pref✝.length ∧ (∀ p ∈ b✝.fst, 2 ≤ p) ∧ ∀ p ∈ b✝.fst, p < 2 + ↑pref✝.lengthhlen:↑b✝.fst.length ≤ ↑pref✝.lengthh2:∀ p ∈ b✝.fst, 2 ≤ ph3:∀ p ∈ b✝.fst, p < 2 + ↑pref✝.length⊢ ↑b✝.fst.length ≤ ↑pref✝.length + 1 omegaAll goals completed! 🐙, ?_⟩
    intro p hpn:ℤans✝¹:List ℤ := []isprime✝¹:List Bool := pyListRepeat [true] (n +ₚ 1)pref✝:List ℕcur✝:ℕsuff✝:List ℕb✝:MProd (List ℤ) (List Bool)ans✝:List ℤ := b✝.fstisprime✝:List Bool := b✝.sndh✝³:0 ≤ nh✝²:List.range (n - 2).toNat = pref✝ ++ cur✝ :: suff✝h✝¹:b✝.snd⦋2 + ↑cur✝⦌ = falseh✝:pyLen b✝.fst ≤ ↑pref✝.length ∧ (∀ p ∈ b✝.fst, 2 ≤ p) ∧ ∀ p ∈ b✝.fst, p < 2 + ↑pref✝.lengthhlen:↑b✝.fst.length ≤ ↑pref✝.lengthh2:∀ p ∈ b✝.fst, 2 ≤ ph3:∀ p ∈ b✝.fst, p < 2 + ↑pref✝.lengthp:ℤhp:p ∈ b✝.fst⊢ p < 2 + (↑pref✝.length + 1); have := h3 p hpn:ℤans✝¹:List ℤ := []isprime✝¹:List Bool := pyListRepeat [true] (n +ₚ 1)pref✝:List ℕcur✝:ℕsuff✝:List ℕb✝:MProd (List ℤ) (List Bool)ans✝:List ℤ := b✝.fstisprime✝:List Bool := b✝.sndh✝³:0 ≤ nh✝²:List.range (n - 2).toNat = pref✝ ++ cur✝ :: suff✝h✝¹:b✝.snd⦋2 + ↑cur✝⦌ = falseh✝:pyLen b✝.fst ≤ ↑pref✝.length ∧ (∀ p ∈ b✝.fst, 2 ≤ p) ∧ ∀ p ∈ b✝.fst, p < 2 + ↑pref✝.lengthhlen:↑b✝.fst.length ≤ ↑pref✝.lengthh2:∀ p ∈ b✝.fst, 2 ≤ ph3:∀ p ∈ b✝.fst, p < 2 + ↑pref✝.lengthp:ℤhp:p ∈ b✝.fstthis:p < 2 + ↑pref✝.length⊢ p < 2 + (↑pref✝.length + 1); omegaAll goals completed! 🐙
  case vc6.post.success =>n:ℤans✝:List ℤ := []isprime✝:List Bool := pyListRepeat [true] (n +ₚ 1)r✝:MProd (List ℤ) (List Bool)h✝¹:0 ≤ nh✝:(pyLen r✝.fst ≤ n - 2 ∨ pyLen r✝.fst ≤ 0) ∧ (∀ p ∈ r✝.fst, 2 ≤ p) ∧ ∀ p ∈ r✝.fst, p < 2 + max (n - 2) 0⊢ pyLen r✝.fst ≤ n ∧ ∀ p ∈ r✝.fst, p < n
    obtain ⟨hlen, h2, h3⟩ := ‹(PastaLean.pyLen _ ≤ _ ∨ _) ∧ _›n:ℤans✝:List ℤ := []isprime✝:List Bool := pyListRepeat [true] (n +ₚ 1)r✝:MProd (List ℤ) (List Bool)h✝¹:0 ≤ nh✝:(pyLen r✝.fst ≤ n - 2 ∨ pyLen r✝.fst ≤ 0) ∧ (∀ p ∈ r✝.fst, 2 ≤ p) ∧ ∀ p ∈ r✝.fst, p < 2 + max (n - 2) 0hlen:pyLen r✝.fst ≤ n - 2 ∨ pyLen r✝.fst ≤ 0h2:∀ p ∈ r✝.fst, 2 ≤ ph3:∀ p ∈ r✝.fst, p < 2 + max (n - 2) 0⊢ pyLen r✝.fst ≤ n ∧ ∀ p ∈ r✝.fst, p < n
    refine ⟨?_, ?_⟩refine_1n:ℤans✝:List ℤ := []isprime✝:List Bool := pyListRepeat [true] (n +ₚ 1)r✝:MProd (List ℤ) (List Bool)h✝¹:0 ≤ nh✝:(pyLen r✝.fst ≤ n - 2 ∨ pyLen r✝.fst ≤ 0) ∧ (∀ p ∈ r✝.fst, 2 ≤ p) ∧ ∀ p ∈ r✝.fst, p < 2 + max (n - 2) 0hlen:pyLen r✝.fst ≤ n - 2 ∨ pyLen r✝.fst ≤ 0h2:∀ p ∈ r✝.fst, 2 ≤ ph3:∀ p ∈ r✝.fst, p < 2 + max (n - 2) 0⊢ pyLen r✝.fst ≤ nrefine_2n:ℤans✝:List ℤ := []isprime✝:List Bool := pyListRepeat [true] (n +ₚ 1)r✝:MProd (List ℤ) (List Bool)h✝¹:0 ≤ nh✝:(pyLen r✝.fst ≤ n - 2 ∨ pyLen r✝.fst ≤ 0) ∧ (∀ p ∈ r✝.fst, 2 ≤ p) ∧ ∀ p ∈ r✝.fst, p < 2 + max (n - 2) 0hlen:pyLen r✝.fst ≤ n - 2 ∨ pyLen r✝.fst ≤ 0h2:∀ p ∈ r✝.fst, 2 ≤ ph3:∀ p ∈ r✝.fst, p < 2 + max (n - 2) 0⊢ ∀ p ∈ r✝.fst, p < n
    ·refine_1n:ℤans✝:List ℤ := []isprime✝:List Bool := pyListRepeat [true] (n +ₚ 1)r✝:MProd (List ℤ) (List Bool)h✝¹:0 ≤ nh✝:(pyLen r✝.fst ≤ n - 2 ∨ pyLen r✝.fst ≤ 0) ∧ (∀ p ∈ r✝.fst, 2 ≤ p) ∧ ∀ p ∈ r✝.fst, p < 2 + max (n - 2) 0hlen:pyLen r✝.fst ≤ n - 2 ∨ pyLen r✝.fst ≤ 0h2:∀ p ∈ r✝.fst, 2 ≤ ph3:∀ p ∈ r✝.fst, p < 2 + max (n - 2) 0⊢ pyLen r✝.fst ≤ n rcases hlen with h | hrefine_1.inln:ℤans✝:List ℤ := []isprime✝:List Bool := pyListRepeat [true] (n +ₚ 1)r✝:MProd (List ℤ) (List Bool)h✝¹:0 ≤ nh✝:(pyLen r✝.fst ≤ n - 2 ∨ pyLen r✝.fst ≤ 0) ∧ (∀ p ∈ r✝.fst, 2 ≤ p) ∧ ∀ p ∈ r✝.fst, p < 2 + max (n - 2) 0h2:∀ p ∈ r✝.fst, 2 ≤ ph3:∀ p ∈ r✝.fst, p < 2 + max (n - 2) 0h:pyLen r✝.fst ≤ n - 2⊢ pyLen r✝.fst ≤ nrefine_1.inrn:ℤans✝:List ℤ := []isprime✝:List Bool := pyListRepeat [true] (n +ₚ 1)r✝:MProd (List ℤ) (List Bool)h✝¹:0 ≤ nh✝:(pyLen r✝.fst ≤ n - 2 ∨ pyLen r✝.fst ≤ 0) ∧ (∀ p ∈ r✝.fst, 2 ≤ p) ∧ ∀ p ∈ r✝.fst, p < 2 + max (n - 2) 0h2:∀ p ∈ r✝.fst, 2 ≤ ph3:∀ p ∈ r✝.fst, p < 2 + max (n - 2) 0h:pyLen r✝.fst ≤ 0⊢ pyLen r✝.fst ≤ n <;>refine_1.inln:ℤans✝:List ℤ := []isprime✝:List Bool := pyListRepeat [true] (n +ₚ 1)r✝:MProd (List ℤ) (List Bool)h✝¹:0 ≤ nh✝:(pyLen r✝.fst ≤ n - 2 ∨ pyLen r✝.fst ≤ 0) ∧ (∀ p ∈ r✝.fst, 2 ≤ p) ∧ ∀ p ∈ r✝.fst, p < 2 + max (n - 2) 0h2:∀ p ∈ r✝.fst, 2 ≤ ph3:∀ p ∈ r✝.fst, p < 2 + max (n - 2) 0h:pyLen r✝.fst ≤ n - 2⊢ pyLen r✝.fst ≤ nrefine_1.inrn:ℤans✝:List ℤ := []isprime✝:List Bool := pyListRepeat [true] (n +ₚ 1)r✝:MProd (List ℤ) (List Bool)h✝¹:0 ≤ nh✝:(pyLen r✝.fst ≤ n - 2 ∨ pyLen r✝.fst ≤ 0) ∧ (∀ p ∈ r✝.fst, 2 ≤ p) ∧ ∀ p ∈ r✝.fst, p < 2 + max (n - 2) 0h2:∀ p ∈ r✝.fst, 2 ≤ ph3:∀ p ∈ r✝.fst, p < 2 + max (n - 2) 0h:pyLen r✝.fst ≤ 0⊢ pyLen r✝.fst ≤ n
        simp only [PastaLean.pyLen, PastaLean.PyLen.pyLen] at h ⊢refine_1.inrn:ℤans✝:List ℤ := []isprime✝:List Bool := pyListRepeat [true] (n +ₚ 1)r✝:MProd (List ℤ) (List Bool)h✝¹:0 ≤ nh✝:(pyLen r✝.fst ≤ n - 2 ∨ pyLen r✝.fst ≤ 0) ∧ (∀ p ∈ r✝.fst, 2 ≤ p) ∧ ∀ p ∈ r✝.fst, p < 2 + max (n - 2) 0h2:∀ p ∈ r✝.fst, 2 ≤ ph3:∀ p ∈ r✝.fst, p < 2 + max (n - 2) 0h:↑r✝.fst.length ≤ 0⊢ ↑r✝.fst.length ≤ n <;>refine_1.inln:ℤans✝:List ℤ := []isprime✝:List Bool := pyListRepeat [true] (n +ₚ 1)r✝:MProd (List ℤ) (List Bool)h✝¹:0 ≤ nh✝:(pyLen r✝.fst ≤ n - 2 ∨ pyLen r✝.fst ≤ 0) ∧ (∀ p ∈ r✝.fst, 2 ≤ p) ∧ ∀ p ∈ r✝.fst, p < 2 + max (n - 2) 0h2:∀ p ∈ r✝.fst, 2 ≤ ph3:∀ p ∈ r✝.fst, p < 2 + max (n - 2) 0h:↑r✝.fst.length ≤ n - 2⊢ ↑r✝.fst.length ≤ nrefine_1.inrn:ℤans✝:List ℤ := []isprime✝:List Bool := pyListRepeat [true] (n +ₚ 1)r✝:MProd (List ℤ) (List Bool)h✝¹:0 ≤ nh✝:(pyLen r✝.fst ≤ n - 2 ∨ pyLen r✝.fst ≤ 0) ∧ (∀ p ∈ r✝.fst, 2 ≤ p) ∧ ∀ p ∈ r✝.fst, p < 2 + max (n - 2) 0h2:∀ p ∈ r✝.fst, 2 ≤ ph3:∀ p ∈ r✝.fst, p < 2 + max (n - 2) 0h:↑r✝.fst.length ≤ 0⊢ ↑r✝.fst.length ≤ n omegaAll goals completed! 🐙
    ·refine_2n:ℤans✝:List ℤ := []isprime✝:List Bool := pyListRepeat [true] (n +ₚ 1)r✝:MProd (List ℤ) (List Bool)h✝¹:0 ≤ nh✝:(pyLen r✝.fst ≤ n - 2 ∨ pyLen r✝.fst ≤ 0) ∧ (∀ p ∈ r✝.fst, 2 ≤ p) ∧ ∀ p ∈ r✝.fst, p < 2 + max (n - 2) 0hlen:pyLen r✝.fst ≤ n - 2 ∨ pyLen r✝.fst ≤ 0h2:∀ p ∈ r✝.fst, 2 ≤ ph3:∀ p ∈ r✝.fst, p < 2 + max (n - 2) 0⊢ ∀ p ∈ r✝.fst, p < n intro p hprefine_2n:ℤans✝:List ℤ := []isprime✝:List Bool := pyListRepeat [true] (n +ₚ 1)r✝:MProd (List ℤ) (List Bool)h✝¹:0 ≤ nh✝:(pyLen r✝.fst ≤ n - 2 ∨ pyLen r✝.fst ≤ 0) ∧ (∀ p ∈ r✝.fst, 2 ≤ p) ∧ ∀ p ∈ r✝.fst, p < 2 + max (n - 2) 0hlen:pyLen r✝.fst ≤ n - 2 ∨ pyLen r✝.fst ≤ 0h2:∀ p ∈ r✝.fst, 2 ≤ ph3:∀ p ∈ r✝.fst, p < 2 + max (n - 2) 0p:ℤhp:p ∈ r✝.fst⊢ p < n
      have hp3 := h3 p hprefine_2n:ℤans✝:List ℤ := []isprime✝:List Bool := pyListRepeat [true] (n +ₚ 1)r✝:MProd (List ℤ) (List Bool)h✝¹:0 ≤ nh✝:(pyLen r✝.fst ≤ n - 2 ∨ pyLen r✝.fst ≤ 0) ∧ (∀ p ∈ r✝.fst, 2 ≤ p) ∧ ∀ p ∈ r✝.fst, p < 2 + max (n - 2) 0hlen:pyLen r✝.fst ≤ n - 2 ∨ pyLen r✝.fst ≤ 0h2:∀ p ∈ r✝.fst, 2 ≤ ph3:∀ p ∈ r✝.fst, p < 2 + max (n - 2) 0p:ℤhp:p ∈ r✝.fsthp3:p < 2 + max (n - 2) 0⊢ p < n
      have hpos := List.length_pos_of_mem hprefine_2n:ℤans✝:List ℤ := []isprime✝:List Bool := pyListRepeat [true] (n +ₚ 1)r✝:MProd (List ℤ) (List Bool)h✝¹:0 ≤ nh✝:(pyLen r✝.fst ≤ n - 2 ∨ pyLen r✝.fst ≤ 0) ∧ (∀ p ∈ r✝.fst, 2 ≤ p) ∧ ∀ p ∈ r✝.fst, p < 2 + max (n - 2) 0hlen:pyLen r✝.fst ≤ n - 2 ∨ pyLen r✝.fst ≤ 0h2:∀ p ∈ r✝.fst, 2 ≤ ph3:∀ p ∈ r✝.fst, p < 2 + max (n - 2) 0p:ℤhp:p ∈ r✝.fsthp3:p < 2 + max (n - 2) 0hpos:0 < r✝.fst.length⊢ p < n
      rcases hlen with h | hrefine_2.inln:ℤans✝:List ℤ := []isprime✝:List Bool := pyListRepeat [true] (n +ₚ 1)r✝:MProd (List ℤ) (List Bool)h✝¹:0 ≤ nh✝:(pyLen r✝.fst ≤ n - 2 ∨ pyLen r✝.fst ≤ 0) ∧ (∀ p ∈ r✝.fst, 2 ≤ p) ∧ ∀ p ∈ r✝.fst, p < 2 + max (n - 2) 0h2:∀ p ∈ r✝.fst, 2 ≤ ph3:∀ p ∈ r✝.fst, p < 2 + max (n - 2) 0p:ℤhp:p ∈ r✝.fsthp3:p < 2 + max (n - 2) 0hpos:0 < r✝.fst.lengthh:pyLen r✝.fst ≤ n - 2⊢ p < nrefine_2.inrn:ℤans✝:List ℤ := []isprime✝:List Bool := pyListRepeat [true] (n +ₚ 1)r✝:MProd (List ℤ) (List Bool)h✝¹:0 ≤ nh✝:(pyLen r✝.fst ≤ n - 2 ∨ pyLen r✝.fst ≤ 0) ∧ (∀ p ∈ r✝.fst, 2 ≤ p) ∧ ∀ p ∈ r✝.fst, p < 2 + max (n - 2) 0h2:∀ p ∈ r✝.fst, 2 ≤ ph3:∀ p ∈ r✝.fst, p < 2 + max (n - 2) 0p:ℤhp:p ∈ r✝.fsthp3:p < 2 + max (n - 2) 0hpos:0 < r✝.fst.lengthh:pyLen r✝.fst ≤ 0⊢ p < n <;>refine_2.inln:ℤans✝:List ℤ := []isprime✝:List Bool := pyListRepeat [true] (n +ₚ 1)r✝:MProd (List ℤ) (List Bool)h✝¹:0 ≤ nh✝:(pyLen r✝.fst ≤ n - 2 ∨ pyLen r✝.fst ≤ 0) ∧ (∀ p ∈ r✝.fst, 2 ≤ p) ∧ ∀ p ∈ r✝.fst, p < 2 + max (n - 2) 0h2:∀ p ∈ r✝.fst, 2 ≤ ph3:∀ p ∈ r✝.fst, p < 2 + max (n - 2) 0p:ℤhp:p ∈ r✝.fsthp3:p < 2 + max (n - 2) 0hpos:0 < r✝.fst.lengthh:pyLen r✝.fst ≤ n - 2⊢ p < nrefine_2.inrn:ℤans✝:List ℤ := []isprime✝:List Bool := pyListRepeat [true] (n +ₚ 1)r✝:MProd (List ℤ) (List Bool)h✝¹:0 ≤ nh✝:(pyLen r✝.fst ≤ n - 2 ∨ pyLen r✝.fst ≤ 0) ∧ (∀ p ∈ r✝.fst, 2 ≤ p) ∧ ∀ p ∈ r✝.fst, p < 2 + max (n - 2) 0h2:∀ p ∈ r✝.fst, 2 ≤ ph3:∀ p ∈ r✝.fst, p < 2 + max (n - 2) 0p:ℤhp:p ∈ r✝.fsthp3:p < 2 + max (n - 2) 0hpos:0 < r✝.fst.lengthh:pyLen r✝.fst ≤ 0⊢ p < n
        simp only [PastaLean.pyLen, PastaLean.PyLen.pyLen] at hrefine_2.inrn:ℤans✝:List ℤ := []isprime✝:List Bool := pyListRepeat [true] (n +ₚ 1)r✝:MProd (List ℤ) (List Bool)h✝¹:0 ≤ nh✝:(pyLen r✝.fst ≤ n - 2 ∨ pyLen r✝.fst ≤ 0) ∧ (∀ p ∈ r✝.fst, 2 ≤ p) ∧ ∀ p ∈ r✝.fst, p < 2 + max (n - 2) 0h2:∀ p ∈ r✝.fst, 2 ≤ ph3:∀ p ∈ r✝.fst, p < 2 + max (n - 2) 0p:ℤhp:p ∈ r✝.fsthp3:p < 2 + max (n - 2) 0hpos:0 < r✝.fst.lengthh:↑r✝.fst.length ≤ 0⊢ p < n <;>refine_2.inln:ℤans✝:List ℤ := []isprime✝:List Bool := pyListRepeat [true] (n +ₚ 1)r✝:MProd (List ℤ) (List Bool)h✝¹:0 ≤ nh✝:(pyLen r✝.fst ≤ n - 2 ∨ pyLen r✝.fst ≤ 0) ∧ (∀ p ∈ r✝.fst, 2 ≤ p) ∧ ∀ p ∈ r✝.fst, p < 2 + max (n - 2) 0h2:∀ p ∈ r✝.fst, 2 ≤ ph3:∀ p ∈ r✝.fst, p < 2 + max (n - 2) 0p:ℤhp:p ∈ r✝.fsthp3:p < 2 + max (n - 2) 0hpos:0 < r✝.fst.lengthh:↑r✝.fst.length ≤ n - 2⊢ p < nrefine_2.inrn:ℤans✝:List ℤ := []isprime✝:List Bool := pyListRepeat [true] (n +ₚ 1)r✝:MProd (List ℤ) (List Bool)h✝¹:0 ≤ nh✝:(pyLen r✝.fst ≤ n - 2 ∨ pyLen r✝.fst ≤ 0) ∧ (∀ p ∈ r✝.fst, 2 ≤ p) ∧ ∀ p ∈ r✝.fst, p < 2 + max (n - 2) 0h2:∀ p ∈ r✝.fst, 2 ≤ ph3:∀ p ∈ r✝.fst, p < 2 + max (n - 2) 0p:ℤhp:p ∈ r✝.fsthp3:p < 2 + max (n - 2) 0hpos:0 < r✝.fst.lengthh:↑r✝.fst.length ≤ 0⊢ p < n omegaAll goals completed! 🐙

theorem count_up_to_correct :
    ∀ (n : Int),
      n ≥ (0 : Int) →
        let ans := (count_up_to n).run;
        (PastaLean.pyLen ans ≤ n ∧ ∀ p ∈ PastaLean.pyIter ans, (2 : Int) ≤ p) ∧ ∀ p ∈ PastaLean.pyIter ans, p < n :=
  by⊢ ∀ n ≥ 0,
  let ans := (count_up_to n).run;
  (pyLen ans ≤ n ∧ ∀ p ∈ pyIter ans, 2 ≤ p) ∧ ∀ p ∈ pyIter ans, p < n
  intro n hpren:ℤhpre:n ≥ 0⊢ let ans := (count_up_to n).run;
(pyLen ans ≤ n ∧ ∀ p ∈ pyIter ans, 2 ≤ p) ∧ ∀ p ∈ pyIter ans, p < n
  exact count_up_to_spec hpreAll goals completed! 🐙