awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (hypothesis)
Goal:
n_1 : ℕ
f_1 : List.Vector ℕ n_1 →. ℕ
n_2 : ℕ
f : List.Vector ℕ (n_2 + 1) → ℕ
h : Nat.Partrec' (↑f : List.Vector ℕ (n_2 + 1) →. ℕ)
cf : Code
v : List.Vector ℕ n_2
hf : ∀ (a : ℕ), cf.eval (a :: (↑v : List ℕ)) = Part.some [f (a ::ᵥ v)]
n : ℕ
hn : f (n ::ᵥ v) = 0
hm : ∀ {m : ℕ}, m < n → ¬f (m ::ᵥ v) = 0
⊢ Membership.mem (γ := Part (List ℕ))
    (PFun.fix
      (fun (v : List ℕ) ↦
        (cf.eval v).bind fun (y : List ℕ) ↦
          Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
      (0 :: (↑v : List ℕ)))
    (n.succ :: (↑v : List ℕ))
have this : Membership.mem (γ := Part (List ℕ))
  (PFun.fix
    (fun (v : List ℕ) ↦
      (cf.eval v).bind fun (y : List ℕ) ↦
        Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
    (n :: (↑v : List ℕ)))
  (n.succ :: (↑v : List ℕ))
Tactic: have : (n.succ::v.1 : List ℕ) ∈
        PFun.fix (fun v =>
          (cf.eval v).bind fun y =>
            Part.some <|
              if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail)
                else Sum.inr (v.headI.succ :: v.tail))
            (n::v.val) :=
        PFun.mem_fix_iff.2 (Or.inl (by simp [hf, hn]))
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
n_1 : ℕ
f_1 : List.Vector ℕ n_1 →. ℕ
n_2 : ℕ
f : List.Vector ℕ (n_2 + 1) → ℕ
h : Nat.Partrec' (↑f : List.Vector ℕ (n_2 + 1) →. ℕ)
cf : Code
v : List.Vector ℕ n_2
hf : ∀ (a : ℕ), cf.eval (a :: (↑v : List ℕ)) = Part.some [f (a ::ᵥ v)]
n : ℕ
hn : f (n ::ᵥ v) = 0
hm : ∀ {m : ℕ}, m < n → ¬f (m ::ᵥ v) = 0
this :
  Membership.mem (γ := Part (List ℕ))
    (PFun.fix
      (fun (v : List ℕ) ↦
        (cf.eval v).bind fun (y : List ℕ) ↦
          Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
      (n :: (↑v : List ℕ)))
    (n.succ :: (↑v : List ℕ))
⊢ Membership.mem (γ := Part (List ℕ))
    (PFun.fix
      (fun (v : List ℕ) ↦
        (cf.eval v).bind fun (y : List ℕ) ↦
          Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
      (0 :: (↑v : List ℕ)))
    (n.succ :: (↑v : List ℕ))
have rfind : ∀ (w : List ℕ)
  (this :
    Membership.mem (γ := Part (List ℕ))
      (PFun.fix
        (fun (v : List ℕ) ↦
          (cf.eval v).bind fun (y : List ℕ) ↦
            Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
        (n :: (↑v : List ℕ)))
      w),
  Membership.mem (γ := Part (List ℕ))
    (PFun.fix
      (fun (v : List ℕ) ↦
        (cf.eval v).bind fun (y : List ℕ) ↦
          Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
      (0 :: (↑v : List ℕ)))
    w
Tactic: generalize (n.succ :: v.1 : List ℕ) = w at this ⊢
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
n_1 : ℕ
f_1 : List.Vector ℕ n_1 →. ℕ
n_2 : ℕ
f : List.Vector ℕ (n_2 + 1) → ℕ
h : Nat.Partrec' (↑f : List.Vector ℕ (n_2 + 1) →. ℕ)
cf : Code
v : List.Vector ℕ n_2
hf : ∀ (a : ℕ), cf.eval (a :: (↑v : List ℕ)) = Part.some [f (a ::ᵥ v)]
w : List ℕ
n : ℕ
IH :
  ∀ (hm : ∀ {m : ℕ}, m < n → ¬f (m ::ᵥ v) = 0)
    (this :
      Membership.mem (γ := Part (List ℕ))
        (PFun.fix
          (fun (v : List ℕ) ↦
            (cf.eval v).bind fun (y : List ℕ) ↦
              Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
          (n :: (↑v : List ℕ)))
        w),
    Membership.mem (γ := Part (List ℕ))
      (PFun.fix
        (fun (v : List ℕ) ↦
          (cf.eval v).bind fun (y : List ℕ) ↦
            Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
        (0 :: (↑v : List ℕ)))
      w
hm : ∀ {m : ℕ}, m < n + 1 → ¬f (m ::ᵥ v) = 0
this :
  Membership.mem (γ := Part (List ℕ))
    (PFun.fix
      (fun (v : List ℕ) ↦
        (cf.eval v).bind fun (y : List ℕ) ↦
          Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
      ((n + 1) :: (↑v : List ℕ)))
    w
⊢ Membership.mem (γ := Part (List ℕ))
    (PFun.fix
      (fun (v : List ℕ) ↦
        (cf.eval v).bind fun (y : List ℕ) ↦
          Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
      (0 :: (↑v : List ℕ)))
    w
have rfind : Membership.mem (γ := Part (List ℕ ⊕ List ℕ))
  ((cf.eval (n :: (↑v : List ℕ))).bind fun (y : List ℕ) ↦
    Part.some
      (if y.headI = 0 then Sum.inl ((n :: (↑v : List ℕ)).headI.succ :: (n :: (↑v : List ℕ)).tail)
      else Sum.inr ((n :: (↑v : List ℕ)).headI.succ :: (n :: (↑v : List ℕ)).tail)))
  (Sum.inr ((n + 1) :: (↑v : List ℕ)))
Tactic: refine IH (fun {m} h' => hm (Nat.lt_succ_of_lt h'))
          (PFun.mem_fix_iff.2 (Or.inr ⟨_, ?_, this⟩))
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
n_1 : ℕ
f_1 : List.Vector ℕ n_1 →. ℕ
n_2 : ℕ
f : List.Vector ℕ (n_2 + 1) → ℕ
h : Nat.Partrec' (↑f : List.Vector ℕ (n_2 + 1) →. ℕ)
cf : Code
v : List.Vector ℕ n_2
hf : ∀ (a : ℕ), cf.eval (a :: (↑v : List ℕ)) = Part.some [f (a ::ᵥ v)]
n : ℕ
hm : ∀ {m : ℕ}, m < n → ¬f (m ::ᵥ v) = 0
w : List ℕ
this :
  Membership.mem (γ := Part (List ℕ))
    (PFun.fix
      (fun (v : List ℕ) ↦
        (cf.eval v).bind fun (y : List ℕ) ↦
          Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
      (n :: (↑v : List ℕ)))
    w
⊢ Membership.mem (γ := Part (List ℕ))
    (PFun.fix
      (fun (v : List ℕ) ↦
        (cf.eval v).bind fun (y : List ℕ) ↦
          Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
      (0 :: (↑v : List ℕ)))
    w
have rfind : ∀ (hm : ∀ {m : ℕ}, m < 0 → ¬f (m ::ᵥ v) = 0)
  (this :
    Membership.mem (γ := Part (List ℕ))
      (PFun.fix
        (fun (v : List ℕ) ↦
          (cf.eval v).bind fun (y : List ℕ) ↦
            Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
        (0 :: (↑v : List ℕ)))
      w),
  Membership.mem (γ := Part (List ℕ))
    (PFun.fix
      (fun (v : List ℕ) ↦
        (cf.eval v).bind fun (y : List ℕ) ↦
          Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
      (0 :: (↑v : List ℕ)))
    w
Tactic: induction n with
      | zero => exact this
      | succ n IH =>
        refine IH (fun {m} h' => hm (Nat.lt_succ_of_lt h'))
          (PFun.mem_fix_iff.2 (Or.inr ⟨_, ?_, this⟩))
        simp only [hf, hm n.lt_succ_self, Part.bind_some, List.headI, if_false,
          Part.mem_some_iff, List.tail_cons]
Cleared hypotheses: n, hm, this
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
k' : Cont
a : Code
a_1 : Cont
k_ih : ∀ {v : List ℕ}, (a_1.then k').eval v = a_1.eval v >>= k'.eval
v : List ℕ
⊢ ((fix a a_1).then k').eval v = (fix a a_1).eval v >>= k'.eval
have fix : (if v.headI = 0 then a_1.eval v.tail >>= k'.eval else a.fix.eval v.tail >>= (a_1.then k').eval) =
  (if v.headI = 0 then a_1.eval v.tail else a.fix.eval v.tail >>= a_1.eval) >>= k'.eval
Tactic: simp only [Cont.eval, Cont.then, *]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
k' : Cont
a : Code
a_1 : Cont
k_ih : ∀ {v : List ℕ}, (a_1.then k').eval v = a_1.eval v >>= k'.eval
v : List ℕ
⊢ (if v.headI = 0 then a_1.eval v.tail >>= k'.eval else a.fix.eval v.tail >>= (a_1.then k').eval) =
    (if v.headI = 0 then a_1.eval v.tail else a.fix.eval v.tail >>= a_1.eval) >>= k'.eval
have pos : v.headI = 0 → a_1.eval v.tail >>= k'.eval = a_1.eval v.tail >>= k'.eval
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
k' : Cont
a : Code
a_1 : Cont
k_ih : ∀ {v : List ℕ}, (a_1.then k').eval v = a_1.eval v >>= k'.eval
v : List ℕ
pos : v.headI = 0 → a_1.eval v.tail >>= k'.eval = a_1.eval v.tail >>= k'.eval
⊢ (if v.headI = 0 then a_1.eval v.tail >>= k'.eval else a.fix.eval v.tail >>= (a_1.then k').eval) =
    (if v.headI = 0 then a_1.eval v.tail else a.fix.eval v.tail >>= a_1.eval) >>= k'.eval
have neg : ¬v.headI = 0 → a.fix.eval v.tail >>= (a_1.then k').eval = a.fix.eval v.tail >>= a_1.eval >>= k'.eval
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
k' : Cont
a : Code
a_1 : Cont
k_ih : ∀ {v : List ℕ}, (a_1.then k').eval v = a_1.eval v >>= k'.eval
v : List ℕ
⊢ (if v.headI = 0 then a_1.eval v.tail >>= k'.eval else a.fix.eval v.tail >>= (a_1.then k').eval) =
    (if v.headI = 0 then a_1.eval v.tail else a.fix.eval v.tail >>= a_1.eval) >>= k'.eval
have pos : v.headI = 0 → a_1.eval v.tail >>= k'.eval = a_1.eval v.tail >>= k'.eval
Tactic: split_ifs <;> [rfl; simp only [← k_ih, bind_assoc]]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
k' : Cont
a : Code
a_1 : Cont
k_ih : ∀ {v : List ℕ}, (a_1.then k').eval v = a_1.eval v >>= k'.eval
v : List ℕ
pos : v.headI = 0 → a_1.eval v.tail >>= k'.eval = a_1.eval v.tail >>= k'.eval
⊢ (if v.headI = 0 then a_1.eval v.tail >>= k'.eval else a.fix.eval v.tail >>= (a_1.then k').eval) =
    (if v.headI = 0 then a_1.eval v.tail else a.fix.eval v.tail >>= a_1.eval) >>= k'.eval
have neg : ¬v.headI = 0 → a.fix.eval v.tail >>= (a_1.then k').eval = a.fix.eval v.tail >>= a_1.eval >>= k'.eval
Tactic: split_ifs <;> [rfl; simp only [← k_ih, bind_assoc]]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
k k' : Cont
v : List ℕ
⊢ (k.then k').eval v = k.eval v >>= k'.eval
have halt : ∀ {v : List ℕ}, (halt.then k').eval v = halt.eval v >>= k'.eval
Tactic: induction k generalizing v with
  | halt => simp only [Cont.eval, Cont.then, pure_bind]
  | cons₁ => simp only [Cont.eval, Cont.then, bind_assoc, *]
  | cons₂ => simp only [Cont.eval, Cont.then, *]
  | comp _ _ k_ih => simp only [Cont.eval, Cont.then, bind_assoc, ← k_ih]
  | fix _ _ k_ih =>
    simp only [Cont.eval, Cont.then, *]
    split_ifs <;> [rfl; simp only [← k_ih, bind_assoc]]
Cleared hypotheses: k, v
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
k k' : Cont
v : List ℕ
halt : ∀ {v : List ℕ}, (Cont.halt.then k').eval v = Cont.halt.eval v >>= k'.eval
⊢ (k.then k').eval v = k.eval v >>= k'.eval
have cons₁ : ∀ (a : Code) (a_1 : List ℕ) (a_2 : Cont),
  (∀ {v : List ℕ}, (a_2.then k').eval v = a_2.eval v >>= k'.eval) →
    ∀ {v : List ℕ}, ((cons₁ a a_1 a_2).then k').eval v = (cons₁ a a_1 a_2).eval v >>= k'.eval
Tactic: induction k generalizing v with
  | halt => simp only [Cont.eval, Cont.then, pure_bind]
  | cons₁ => simp only [Cont.eval, Cont.then, bind_assoc, *]
  | cons₂ => simp only [Cont.eval, Cont.then, *]
  | comp _ _ k_ih => simp only [Cont.eval, Cont.then, bind_assoc, ← k_ih]
  | fix _ _ k_ih =>
    simp only [Cont.eval, Cont.then, *]
    split_ifs <;> [rfl; simp only [← k_ih, bind_assoc]]
Cleared hypotheses: k, v
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
k k' : Cont
v : List ℕ
halt : ∀ {v : List ℕ}, (Cont.halt.then k').eval v = Cont.halt.eval v >>= k'.eval
cons₁ :
  ∀ (a : Code) (a_1 : List ℕ) (a_2 : Cont),
    (∀ {v : List ℕ}, (a_2.then k').eval v = a_2.eval v >>= k'.eval) →
      ∀ {v : List ℕ}, ((Cont.cons₁ a a_1 a_2).then k').eval v = (Cont.cons₁ a a_1 a_2).eval v >>= k'.eval
⊢ (k.then k').eval v = k.eval v >>= k'.eval
have cons₂ : ∀ (a : List ℕ) (a_1 : Cont),
  (∀ {v : List ℕ}, (a_1.then k').eval v = a_1.eval v >>= k'.eval) →
    ∀ {v : List ℕ}, ((cons₂ a a_1).then k').eval v = (cons₂ a a_1).eval v >>= k'.eval
Tactic: induction k generalizing v with
  | halt => simp only [Cont.eval, Cont.then, pure_bind]
  | cons₁ => simp only [Cont.eval, Cont.then, bind_assoc, *]
  | cons₂ => simp only [Cont.eval, Cont.then, *]
  | comp _ _ k_ih => simp only [Cont.eval, Cont.then, bind_assoc, ← k_ih]
  | fix _ _ k_ih =>
    simp only [Cont.eval, Cont.then, *]
    split_ifs <;> [rfl; simp only [← k_ih, bind_assoc]]
Cleared hypotheses: k, v
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
k k' : Cont
v : List ℕ
halt : ∀ {v : List ℕ}, (Cont.halt.then k').eval v = Cont.halt.eval v >>= k'.eval
cons₁ :
  ∀ (a : Code) (a_1 : List ℕ) (a_2 : Cont),
    (∀ {v : List ℕ}, (a_2.then k').eval v = a_2.eval v >>= k'.eval) →
      ∀ {v : List ℕ}, ((Cont.cons₁ a a_1 a_2).then k').eval v = (Cont.cons₁ a a_1 a_2).eval v >>= k'.eval
cons₂ :
  ∀ (a : List ℕ) (a_1 : Cont),
    (∀ {v : List ℕ}, (a_1.then k').eval v = a_1.eval v >>= k'.eval) →
      ∀ {v : List ℕ}, ((Cont.cons₂ a a_1).then k').eval v = (Cont.cons₂ a a_1).eval v >>= k'.eval
⊢ (k.then k').eval v = k.eval v >>= k'.eval
have comp : ∀ (a : Code) (a_1 : Cont) (k_ih : ∀ {v : List ℕ}, (a_1.then k').eval v = a_1.eval v >>= k'.eval) {v : List ℕ},
  ((comp a a_1).then k').eval v = (comp a a_1).eval v >>= k'.eval
Tactic: induction k generalizing v with
  | halt => simp only [Cont.eval, Cont.then, pure_bind]
  | cons₁ => simp only [Cont.eval, Cont.then, bind_assoc, *]
  | cons₂ => simp only [Cont.eval, Cont.then, *]
  | comp _ _ k_ih => simp only [Cont.eval, Cont.then, bind_assoc, ← k_ih]
  | fix _ _ k_ih =>
    simp only [Cont.eval, Cont.then, *]
    split_ifs <;> [rfl; simp only [← k_ih, bind_assoc]]
Cleared hypotheses: k, v
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
k k' : Cont
v : List ℕ
halt : ∀ {v : List ℕ}, (Cont.halt.then k').eval v = Cont.halt.eval v >>= k'.eval
cons₁ :
  ∀ (a : Code) (a_1 : List ℕ) (a_2 : Cont),
    (∀ {v : List ℕ}, (a_2.then k').eval v = a_2.eval v >>= k'.eval) →
      ∀ {v : List ℕ}, ((Cont.cons₁ a a_1 a_2).then k').eval v = (Cont.cons₁ a a_1 a_2).eval v >>= k'.eval
cons₂ :
  ∀ (a : List ℕ) (a_1 : Cont),
    (∀ {v : List ℕ}, (a_1.then k').eval v = a_1.eval v >>= k'.eval) →
      ∀ {v : List ℕ}, ((Cont.cons₂ a a_1).then k').eval v = (Cont.cons₂ a a_1).eval v >>= k'.eval
comp :
  ∀ (a : Code) (a_1 : Cont) (k_ih : ∀ {v : List ℕ}, (a_1.then k').eval v = a_1.eval v >>= k'.eval) {v : List ℕ},
    ((Cont.comp a a_1).then k').eval v = (Cont.comp a a_1).eval v >>= k'.eval
⊢ (k.then k').eval v = k.eval v >>= k'.eval
have fix : ∀ (a : Code) (a_1 : Cont) (k_ih : ∀ {v : List ℕ}, (a_1.then k').eval v = a_1.eval v >>= k'.eval) {v : List ℕ},
  ((fix a a_1).then k').eval v = (fix a a_1).eval v >>= k'.eval
Tactic: induction k generalizing v with
  | halt => simp only [Cont.eval, Cont.then, pure_bind]
  | cons₁ => simp only [Cont.eval, Cont.then, bind_assoc, *]
  | cons₂ => simp only [Cont.eval, Cont.then, *]
  | comp _ _ k_ih => simp only [Cont.eval, Cont.then, bind_assoc, ← k_ih]
  | fix _ _ k_ih =>
    simp only [Cont.eval, Cont.then, *]
    split_ifs <;> [rfl; simp only [← k_ih, bind_assoc]]
Cleared hypotheses: k, v
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
k' : Cont
c c' : Code
ih : ∀ (k : Cont) (v : List ℕ), stepNormal c (k.then k') v = (stepNormal c k v).then k'
a_ih : ∀ (k : Cont) (v : List ℕ), stepNormal c' (k.then k') v = (stepNormal c' k v).then k'
k : Cont
v : List ℕ
⊢ stepNormal (c.cons c') (k.then k') v = (stepNormal (c.cons c') k v).then k'
have cons : stepNormal c (Cont.cons₁ c' v (k.then k')) v = (stepNormal c (Cont.cons₁ c' v k) v).then k'
Tactic: simp only [stepNormal, *]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
k' : Cont
c c' : Code
ih : ∀ (k : Cont) (v : List ℕ), stepNormal c (k.then k') v = (stepNormal c k v).then k'
a_ih : ∀ (k : Cont) (v : List ℕ), stepNormal c' (k.then k') v = (stepNormal c' k v).then k'
k : Cont
v : List ℕ
⊢ stepNormal c (Cont.cons₁ c' v (k.then k')) v = (stepNormal c (Cont.cons₁ c' v k) v).then k'
have cons : stepNormal c (Cont.cons₁ c' v (k.then k')) v = stepNormal c ((Cont.cons₁ c' v k).then k') v
Tactic: rw [← ih, Cont.then]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
k' : Cont
c c' : Code
ih : ∀ (k : Cont) (v : List ℕ), stepNormal c (k.then k') v = (stepNormal c k v).then k'
a_ih : ∀ (k : Cont) (v : List ℕ), stepNormal c' (k.then k') v = (stepNormal c' k v).then k'
k : Cont
v : List ℕ
cons : stepNormal c (Cont.cons₁ c' v (k.then k')) v = stepNormal c ((Cont.cons₁ c' v k).then k') v
⊢ stepNormal c (Cont.cons₁ c' v (k.then k')) v = (stepNormal c (Cont.cons₁ c' v k) v).then k'
have cons₁ : stepNormal c (Cont.cons₁ c' v (k.then k')) v = stepNormal c ((fun (k' : Cont) ↦ Cont.cons₁ c' v (k.then k')) k') v
Tactic: rw [← ih, Cont.then]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
k' : Cont
c c' : Code
a_ih : ∀ (k : Cont) (v : List ℕ), stepNormal c (k.then k') v = (stepNormal c k v).then k'
ih' : ∀ (k : Cont) (v : List ℕ), stepNormal c' (k.then k') v = (stepNormal c' k v).then k'
k : Cont
v : List ℕ
⊢ stepNormal (c.comp c') (k.then k') v = (stepNormal (c.comp c') k v).then k'
have comp : stepNormal c' (Cont.comp c (k.then k')) v = (stepNormal c' (Cont.comp c k) v).then k'
Tactic: simp only [stepNormal, *]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
k' : Cont
c c' : Code
a_ih : ∀ (k : Cont) (v : List ℕ), stepNormal c (k.then k') v = (stepNormal c k v).then k'
ih' : ∀ (k : Cont) (v : List ℕ), stepNormal c' (k.then k') v = (stepNormal c' k v).then k'
k : Cont
v : List ℕ
⊢ stepNormal c' (Cont.comp c (k.then k')) v = (stepNormal c' (Cont.comp c k) v).then k'
have comp : stepNormal c' (Cont.comp c (k.then k')) v = stepNormal c' ((Cont.comp c k).then k') v
Tactic: rw [← ih', Cont.then]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
k' : Cont
c c' : Code
a_ih : ∀ (k : Cont) (v : List ℕ), stepNormal c (k.then k') v = (stepNormal c k v).then k'
ih' : ∀ (k : Cont) (v : List ℕ), stepNormal c' (k.then k') v = (stepNormal c' k v).then k'
k : Cont
v : List ℕ
comp : stepNormal c' (Cont.comp c (k.then k')) v = stepNormal c' ((Cont.comp c k).then k') v
⊢ stepNormal c' (Cont.comp c (k.then k')) v = (stepNormal c' (Cont.comp c k) v).then k'
have comp₁ : stepNormal c' (Cont.comp c (k.then k')) v = stepNormal c' ((fun (k' : Cont) ↦ Cont.comp c (k.then k')) k') v
Tactic: rw [← ih', Cont.then]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
k' : Cont
a a_1 : Code
a_ih : ∀ (k : Cont) (v : List ℕ), stepNormal a (k.then k') v = (stepNormal a k v).then k'
a_ih_1 : ∀ (k : Cont) (v : List ℕ), stepNormal a_1 (k.then k') v = (stepNormal a_1 k v).then k'
k : Cont
v : List ℕ
⊢ stepNormal (a.case a_1) (k.then k') v = (stepNormal (a.case a_1) k v).then k'
have case : Nat.rec (motive := fun (x : ℕ) ↦ Cfg) ((stepNormal a k v.tail).then k')
    (fun (y : ℕ) (x : Cfg) ↦ (stepNormal a_1 k (y :: v.tail)).then k') v.headI =
  Cfg.then
    (Nat.rec (motive := fun (x : ℕ) ↦ Cfg) (stepNormal a k v.tail)
      (fun (y : ℕ) (x : Cfg) ↦ stepNormal a_1 k (y :: v.tail)) v.headI)
    k'
Tactic: simp only [stepNormal, *]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
k' : Cont
a a_1 : Code
a_ih : ∀ (k : Cont) (v : List ℕ), stepNormal a (k.then k') v = (stepNormal a k v).then k'
a_ih_1 : ∀ (k : Cont) (v : List ℕ), stepNormal a_1 (k.then k') v = (stepNormal a_1 k v).then k'
k : Cont
v : List ℕ
⊢ Nat.rec (motive := fun (x : ℕ) ↦ Cfg) ((stepNormal a k v.tail).then k')
      (fun (y : ℕ) (x : Cfg) ↦ (stepNormal a_1 k (y :: v.tail)).then k') v.headI =
    Cfg.then
      (Nat.rec (motive := fun (x : ℕ) ↦ Cfg) (stepNormal a k v.tail)
        (fun (y : ℕ) (x : Cfg) ↦ stepNormal a_1 k (y :: v.tail)) v.headI)
      k'
have case : Nat.rec (motive := fun (x : ℕ) ↦ Cfg) ((stepNormal a k v.tail).then k')
    (fun (y : ℕ) (x : Cfg) ↦ (stepNormal a_1 k (y :: v.tail)).then k') 0 =
  Cfg.then
    (Nat.rec (motive := fun (x : ℕ) ↦ Cfg) (stepNormal a k v.tail)
      (fun (y : ℕ) (x : Cfg) ↦ stepNormal a_1 k (y :: v.tail)) 0)
    k'
Tactic: cases v.headI
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
k' : Cont
a a_1 : Code
a_ih : ∀ (k : Cont) (v : List ℕ), stepNormal a (k.then k') v = (stepNormal a k v).then k'
a_ih_1 : ∀ (k : Cont) (v : List ℕ), stepNormal a_1 (k.then k') v = (stepNormal a_1 k v).then k'
k : Cont
v : List ℕ
case :
  Nat.rec (motive := fun (x : ℕ) ↦ Cfg) ((stepNormal a k v.tail).then k')
      (fun (y : ℕ) (x : Cfg) ↦ (stepNormal a_1 k (y :: v.tail)).then k') 0 =
    Cfg.then
      (Nat.rec (motive := fun (x : ℕ) ↦ Cfg) (stepNormal a k v.tail)
        (fun (y : ℕ) (x : Cfg) ↦ stepNormal a_1 k (y :: v.tail)) 0)
      k'
⊢ Nat.rec (motive := fun (x : ℕ) ↦ Cfg) ((stepNormal a k v.tail).then k')
      (fun (y : ℕ) (x : Cfg) ↦ (stepNormal a_1 k (y :: v.tail)).then k') v.headI =
    Cfg.then
      (Nat.rec (motive := fun (x : ℕ) ↦ Cfg) (stepNormal a k v.tail)
        (fun (y : ℕ) (x : Cfg) ↦ stepNormal a_1 k (y :: v.tail)) v.headI)
      k'
have case₁ : ∀ (n : ℕ),
  Nat.rec (motive := fun (x : ℕ) ↦ Cfg) ((stepNormal a k v.tail).then k')
      (fun (y : ℕ) (x : Cfg) ↦ (stepNormal a_1 k (y :: v.tail)).then k') (n + 1) =
    Cfg.then
      (Nat.rec (motive := fun (x : ℕ) ↦ Cfg) (stepNormal a k v.tail)
        (fun (y : ℕ) (x : Cfg) ↦ stepNormal a_1 k (y :: v.tail)) (n + 1))
      k'
Tactic: cases v.headI
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
k' : Cont
c : Code
ih : ∀ (k : Cont) (v : List ℕ), stepNormal c (k.then k') v = (stepNormal c k v).then k'
k : Cont
v : List ℕ
⊢ stepNormal c.fix (k.then k') v = (stepNormal c.fix k v).then k'
have fix : stepNormal c (Cont.fix c (k.then k')) v = (stepNormal c (Cont.fix c k) v).then k'
Tactic: simp only [stepNormal, *]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
k' : Cont
c : Code
ih : ∀ (k : Cont) (v : List ℕ), stepNormal c (k.then k') v = (stepNormal c k v).then k'
k : Cont
v : List ℕ
⊢ stepNormal c (Cont.fix c (k.then k')) v = (stepNormal c (Cont.fix c k) v).then k'
have fix : stepNormal c (Cont.fix c (k.then k')) v = stepNormal c ((Cont.fix c k).then k') v
Tactic: rw [← ih, Cont.then]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
k' : Cont
c : Code
ih : ∀ (k : Cont) (v : List ℕ), stepNormal c (k.then k') v = (stepNormal c k v).then k'
k : Cont
v : List ℕ
fix : stepNormal c (Cont.fix c (k.then k')) v = stepNormal c ((Cont.fix c k).then k') v
⊢ stepNormal c (Cont.fix c (k.then k')) v = (stepNormal c (Cont.fix c k) v).then k'
have fix₁ : stepNormal c (Cont.fix c (k.then k')) v = stepNormal c ((fun (k' : Cont) ↦ Cont.fix c (k.then k')) k') v
Tactic: rw [← ih, Cont.then]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
c : Code
k k' : Cont
v : List ℕ
⊢ stepNormal c (k.then k') v = (stepNormal c k v).then k'
have cons : ∀ (c c' : Code) (ih : ∀ (k : Cont) (v : List ℕ), stepNormal c (k.then k') v = (stepNormal c k v).then k'),
  (∀ (k : Cont) (v : List ℕ), stepNormal c' (k.then k') v = (stepNormal c' k v).then k') →
    ∀ (k : Cont) (v : List ℕ), stepNormal (c.cons c') (k.then k') v = (stepNormal (c.cons c') k v).then k'
Tactic: induction c generalizing k v with simp only [stepNormal, *]
  | cons c c' ih _ => rw [← ih, Cont.then]
  | comp c c' _ ih' => rw [← ih', Cont.then]
  | case => cases v.headI <;> simp only [Nat.rec_zero]
  | fix c ih => rw [← ih, Cont.then]
  | _ => simp only [Cfg.then]
Cleared hypotheses: c, k, v