awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
k k' : Cont
v : List ℕ
cons₁ :
  ∀ (a : Code) (a_1 : List ℕ) (a_2 : Cont),
    (∀ {v : List ℕ}, stepRet (a_2.then k') v = (stepRet a_2 v).then k') →
      ∀ {v : List ℕ}, stepRet ((Cont.cons₁ a a_1 a_2).then k') v = (stepRet (Cont.cons₁ a a_1 a_2) v).then k'
cons₂ :
  ∀ (a : Code) (a_1 : List ℕ) (a_2 : Cont),
    (∀ {v : List ℕ}, stepRet (a_2.then k') v = (stepRet a_2 v).then k') →
      ∀ {v : List ℕ}, stepNormal a (Cont.cons₂ v (a_2.then k')) a_1 = (stepNormal a (Cont.cons₂ v a_2) a_1).then k'
comp :
  ∀ (a : Code) (a_1 : Cont),
    (∀ {v : List ℕ}, stepRet (a_1.then k') v = (stepRet a_1 v).then k') →
      ∀ {v : List ℕ}, stepRet ((Cont.comp a a_1).then k') v = (stepRet (Cont.comp a a_1) v).then k'
comp₁ :
  ∀ (a : Code) (a_1 : Cont),
    (∀ {v : List ℕ}, stepRet (a_1.then k') v = (stepRet a_1 v).then k') →
      ∀ {v : List ℕ}, stepNormal a (a_1.then k') v = (stepNormal a a_1 v).then k'
⊢ stepRet (k.then k') v = (stepRet k v).then k'
have fix : ∀ (a : Code) (a_1 : Cont) (k_ih : ∀ {v : List ℕ}, stepRet (a_1.then k') v = (stepRet a_1 v).then k') {v : List ℕ},
  stepRet ((Cont.fix a a_1).then k') v = (stepRet (Cont.fix a a_1) v).then k'
Tactic: induction k generalizing v with simp only [Cont.then, stepRet, *]
  | cons₁ =>
    rw [← stepNormal_then]
    rfl
  | comp =>
    rw [← stepNormal_then]
  | fix _ _ k_ih =>
    split_ifs
    · rw [← k_ih]
    · rw [← stepNormal_then]
      rfl
  | _ => simp only [Cfg.then]
Cleared hypotheses: k, v
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
k k' : Cont
v : List ℕ
cons₁ :
  ∀ (a : Code) (a_1 : List ℕ) (a_2 : Cont),
    (∀ {v : List ℕ}, stepRet (a_2.then k') v = (stepRet a_2 v).then k') →
      ∀ {v : List ℕ}, stepRet ((Cont.cons₁ a a_1 a_2).then k') v = (stepRet (Cont.cons₁ a a_1 a_2) v).then k'
cons₂ :
  ∀ (a : Code) (a_1 : List ℕ) (a_2 : Cont),
    (∀ {v : List ℕ}, stepRet (a_2.then k') v = (stepRet a_2 v).then k') →
      ∀ {v : List ℕ}, stepNormal a (Cont.cons₂ v (a_2.then k')) a_1 = (stepNormal a (Cont.cons₂ v a_2) a_1).then k'
comp :
  ∀ (a : Code) (a_1 : Cont),
    (∀ {v : List ℕ}, stepRet (a_1.then k') v = (stepRet a_1 v).then k') →
      ∀ {v : List ℕ}, stepRet ((Cont.comp a a_1).then k') v = (stepRet (Cont.comp a a_1) v).then k'
comp₁ :
  ∀ (a : Code) (a_1 : Cont),
    (∀ {v : List ℕ}, stepRet (a_1.then k') v = (stepRet a_1 v).then k') →
      ∀ {v : List ℕ}, stepNormal a (a_1.then k') v = (stepNormal a a_1 v).then k'
fix :
  ∀ (a : Code) (a_1 : Cont) (k_ih : ∀ {v : List ℕ}, stepRet (a_1.then k') v = (stepRet a_1 v).then k') {v : List ℕ},
    stepRet ((Cont.fix a a_1).then k') v = (stepRet (Cont.fix a a_1) v).then k'
⊢ stepRet (k.then k') v = (stepRet k v).then k'
have fix₁ : ∀ (a : Code) (a_1 : Cont) (k_ih : ∀ {v : List ℕ}, stepRet (a_1.then k') v = (stepRet a_1 v).then k') {v : List ℕ},
  (if v.headI = 0 then (stepRet a_1 v.tail).then k' else stepNormal a (Cont.fix a (a_1.then k')) v.tail) =
    (if v.headI = 0 then stepRet a_1 v.tail else stepNormal a (Cont.fix a a_1) v.tail).then k'
Tactic: induction k generalizing v with simp only [Cont.then, stepRet, *]
  | cons₁ =>
    rw [← stepNormal_then]
    rfl
  | comp =>
    rw [← stepNormal_then]
  | fix _ _ k_ih =>
    split_ifs
    · rw [← k_ih]
    · rw [← stepNormal_then]
      rfl
  | _ => simp only [Cfg.then]
Cleared hypotheses: k, v
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
k k' : Cont
v : List ℕ
cons₁ :
  ∀ (a : Code) (a_1 : List ℕ) (a_2 : Cont),
    (∀ {v : List ℕ}, stepRet (a_2.then k') v = (stepRet a_2 v).then k') →
      ∀ {v : List ℕ}, stepRet ((Cont.cons₁ a a_1 a_2).then k') v = (stepRet (Cont.cons₁ a a_1 a_2) v).then k'
cons₂ :
  ∀ (a : Code) (a_1 : List ℕ) (a_2 : Cont),
    (∀ {v : List ℕ}, stepRet (a_2.then k') v = (stepRet a_2 v).then k') →
      ∀ {v : List ℕ}, stepNormal a (Cont.cons₂ v (a_2.then k')) a_1 = (stepNormal a (Cont.cons₂ v a_2) a_1).then k'
comp :
  ∀ (a : Code) (a_1 : Cont),
    (∀ {v : List ℕ}, stepRet (a_1.then k') v = (stepRet a_1 v).then k') →
      ∀ {v : List ℕ}, stepRet ((Cont.comp a a_1).then k') v = (stepRet (Cont.comp a a_1) v).then k'
comp₁ :
  ∀ (a : Code) (a_1 : Cont),
    (∀ {v : List ℕ}, stepRet (a_1.then k') v = (stepRet a_1 v).then k') →
      ∀ {v : List ℕ}, stepNormal a (a_1.then k') v = (stepNormal a a_1 v).then k'
fix :
  ∀ (a : Code) (a_1 : Cont) (k_ih : ∀ {v : List ℕ}, stepRet (a_1.then k') v = (stepRet a_1 v).then k') {v : List ℕ},
    stepRet ((Cont.fix a a_1).then k') v = (stepRet (Cont.fix a a_1) v).then k'
fix₁ :
  ∀ (a : Code) (a_1 : Cont) (k_ih : ∀ {v : List ℕ}, stepRet (a_1.then k') v = (stepRet a_1 v).then k') {v : List ℕ},
    (if v.headI = 0 then (stepRet a_1 v.tail).then k' else stepNormal a (Cont.fix a (a_1.then k')) v.tail) =
      (if v.headI = 0 then stepRet a_1 v.tail else stepNormal a (Cont.fix a a_1) v.tail).then k'
⊢ stepRet (k.then k') v = (stepRet k v).then k'
have halt : ∀ {v : List ℕ}, stepRet (Cont.halt.then k') v = (stepRet Cont.halt v).then k'
Tactic: induction k generalizing v with simp only [Cont.then, stepRet, *]
  | cons₁ =>
    rw [← stepNormal_then]
    rfl
  | comp =>
    rw [← stepNormal_then]
  | fix _ _ k_ih =>
    split_ifs
    · rw [← k_ih]
    · rw [← stepNormal_then]
      rfl
  | _ => simp only [Cfg.then]
Cleared hypotheses: k, v
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
k k' : Cont
v : List ℕ
cons₁ :
  ∀ (a : Code) (a_1 : List ℕ) (a_2 : Cont),
    (∀ {v : List ℕ}, stepRet (a_2.then k') v = (stepRet a_2 v).then k') →
      ∀ {v : List ℕ}, stepRet ((Cont.cons₁ a a_1 a_2).then k') v = (stepRet (Cont.cons₁ a a_1 a_2) v).then k'
cons₂ :
  ∀ (a : Code) (a_1 : List ℕ) (a_2 : Cont),
    (∀ {v : List ℕ}, stepRet (a_2.then k') v = (stepRet a_2 v).then k') →
      ∀ {v : List ℕ}, stepNormal a (Cont.cons₂ v (a_2.then k')) a_1 = (stepNormal a (Cont.cons₂ v a_2) a_1).then k'
comp :
  ∀ (a : Code) (a_1 : Cont),
    (∀ {v : List ℕ}, stepRet (a_1.then k') v = (stepRet a_1 v).then k') →
      ∀ {v : List ℕ}, stepRet ((Cont.comp a a_1).then k') v = (stepRet (Cont.comp a a_1) v).then k'
comp₁ :
  ∀ (a : Code) (a_1 : Cont),
    (∀ {v : List ℕ}, stepRet (a_1.then k') v = (stepRet a_1 v).then k') →
      ∀ {v : List ℕ}, stepNormal a (a_1.then k') v = (stepNormal a a_1 v).then k'
fix :
  ∀ (a : Code) (a_1 : Cont) (k_ih : ∀ {v : List ℕ}, stepRet (a_1.then k') v = (stepRet a_1 v).then k') {v : List ℕ},
    stepRet ((Cont.fix a a_1).then k') v = (stepRet (Cont.fix a a_1) v).then k'
fix₁ :
  ∀ (a : Code) (a_1 : Cont) (k_ih : ∀ {v : List ℕ}, stepRet (a_1.then k') v = (stepRet a_1 v).then k') {v : List ℕ},
    (if v.headI = 0 then (stepRet a_1 v.tail).then k' else stepNormal a (Cont.fix a (a_1.then k')) v.tail) =
      (if v.headI = 0 then stepRet a_1 v.tail else stepNormal a (Cont.fix a a_1) v.tail).then k'
halt : ∀ {v : List ℕ}, stepRet (Cont.halt.then k') v = (stepRet Cont.halt v).then k'
⊢ stepRet (k.then k') v = (stepRet k v).then k'
have halt₁ : ∀ {v : List ℕ}, stepRet k' v = (Cfg.halt v).then k'
Tactic: induction k generalizing v with simp only [Cont.then, stepRet, *]
  | cons₁ =>
    rw [← stepNormal_then]
    rfl
  | comp =>
    rw [← stepNormal_then]
  | fix _ _ k_ih =>
    split_ifs
    · rw [← k_ih]
    · rw [← stepNormal_then]
      rfl
  | _ => simp only [Cfg.then]
Cleared hypotheses: k, v
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
k k' : Cont
v : List ℕ
cons₁ :
  ∀ (a : Code) (a_1 : List ℕ) (a_2 : Cont),
    (∀ {v : List ℕ}, stepRet (a_2.then k') v = (stepRet a_2 v).then k') →
      ∀ {v : List ℕ}, stepRet ((Cont.cons₁ a a_1 a_2).then k') v = (stepRet (Cont.cons₁ a a_1 a_2) v).then k'
cons₂ :
  ∀ (a : Code) (a_1 : List ℕ) (a_2 : Cont),
    (∀ {v : List ℕ}, stepRet (a_2.then k') v = (stepRet a_2 v).then k') →
      ∀ {v : List ℕ}, stepNormal a (Cont.cons₂ v (a_2.then k')) a_1 = (stepNormal a (Cont.cons₂ v a_2) a_1).then k'
comp :
  ∀ (a : Code) (a_1 : Cont),
    (∀ {v : List ℕ}, stepRet (a_1.then k') v = (stepRet a_1 v).then k') →
      ∀ {v : List ℕ}, stepRet ((Cont.comp a a_1).then k') v = (stepRet (Cont.comp a a_1) v).then k'
comp₁ :
  ∀ (a : Code) (a_1 : Cont),
    (∀ {v : List ℕ}, stepRet (a_1.then k') v = (stepRet a_1 v).then k') →
      ∀ {v : List ℕ}, stepNormal a (a_1.then k') v = (stepNormal a a_1 v).then k'
fix :
  ∀ (a : Code) (a_1 : Cont) (k_ih : ∀ {v : List ℕ}, stepRet (a_1.then k') v = (stepRet a_1 v).then k') {v : List ℕ},
    stepRet ((Cont.fix a a_1).then k') v = (stepRet (Cont.fix a a_1) v).then k'
fix₁ :
  ∀ (a : Code) (a_1 : Cont) (k_ih : ∀ {v : List ℕ}, stepRet (a_1.then k') v = (stepRet a_1 v).then k') {v : List ℕ},
    (if v.headI = 0 then (stepRet a_1 v.tail).then k' else stepNormal a (Cont.fix a (a_1.then k')) v.tail) =
      (if v.headI = 0 then stepRet a_1 v.tail else stepNormal a (Cont.fix a a_1) v.tail).then k'
halt : ∀ {v : List ℕ}, stepRet (Cont.halt.then k') v = (stepRet Cont.halt v).then k'
halt₁ : ∀ {v : List ℕ}, stepRet k' v = (Cfg.halt v).then k'
⊢ stepRet (k.then k') v = (stepRet k v).then k'
have cons₃ : ∀ (a : List ℕ) (a_1 : Cont),
  (∀ {v : List ℕ}, stepRet (a_1.then k') v = (stepRet a_1 v).then k') →
    ∀ {v : List ℕ}, stepRet ((Cont.cons₂ a a_1).then k') v = (stepRet (Cont.cons₂ a a_1) v).then k'
Tactic: induction k generalizing v with simp only [Cont.then, stepRet, *]
  | cons₁ =>
    rw [← stepNormal_then]
    rfl
  | comp =>
    rw [← stepNormal_then]
  | fix _ _ k_ih =>
    split_ifs
    · rw [← k_ih]
    · rw [← stepNormal_then]
      rfl
  | _ => simp only [Cfg.then]
Cleared hypotheses: k, v
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
c : Code
h : c.Ok
v : List ℕ
⊢ StateTransition.eval step (stepNormal c Cont.halt v) = Cfg.halt <$> c.eval v
have rw : Eq (α := Part Cfg)
  (do
    let v ← c.eval v
    StateTransition.eval step (Cfg.ret Cont.halt v))
  do
  let a ← c.eval v
  pure (Cfg.halt a)
Tactic: rw [h, ← bind_pure_comp]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
c : Code
h : c.Ok
v : List ℕ
⊢ Eq (α := Part Cfg)
    (do
      let v ← c.eval v
      StateTransition.eval step (Cfg.ret Cont.halt v))
    do
    let a ← c.eval v
    pure (Cfg.halt a)
have e_a : Eq (α := List ℕ → Part Cfg) (fun (v : List ℕ) ↦ StateTransition.eval step (Cfg.ret Cont.halt v)) fun (a : List ℕ) ↦
  pure (Cfg.halt a)
Tactic: congr
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
c : Code
h : c.Ok
v : List ℕ
⊢ Eq (α := List ℕ → Part Cfg) (fun (v : List ℕ) ↦ StateTransition.eval step (Cfg.ret Cont.halt v)) fun (a : List ℕ) ↦
    pure (Cfg.halt a)
have e_a : ∀ (v : List ℕ), StateTransition.eval step (Cfg.ret Cont.halt v) = pure (Cfg.halt v)
Tactic: funext v
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
f g : Code
IHf : ∀ (k : Cont) (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal f k v = Cfg.ret k' v'
IHg : ∀ (k : Cont) (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal g k v = Cfg.ret k' v'
k : Cont
v : List ℕ
⊢ ∃ (k' : Cont) (v' : List ℕ), stepNormal (f.case g) k v = Cfg.ret k' v'
have case : ∃ (k' : Cont) (v' : List ℕ),
  (fun (k : Cont) (v : List ℕ) ↦
        (Nat.rec (motive := fun (x : ℕ) ↦ Cfg) (stepNormal f k v.tail)
            (fun (y : ℕ) (x : Cfg) ↦ stepNormal g k (y :: v.tail)) v.headI :
          Cfg))
      k v =
    Cfg.ret k' v'
Tactic: rw [stepNormal]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
f g : Code
IHf : ∀ (k : Cont) (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal f k v = Cfg.ret k' v'
IHg : ∀ (k : Cont) (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal g k v = Cfg.ret k' v'
k : Cont
v : List ℕ
⊢ ∃ (k' : Cont) (v' : List ℕ),
    Nat.rec (motive := fun (x : ℕ) ↦ Cfg) (stepNormal f k v.tail) (fun (y : ℕ) (x : Cfg) ↦ stepNormal g k (y :: v.tail))
        v.headI =
      Cfg.ret k' v'
have case : ∃ (k' : Cont) (v' : List ℕ),
  Nat.rec (motive := fun (x : ℕ) ↦ Cfg) (stepNormal f k v.tail) (fun (y : ℕ) (x : Cfg) ↦ stepNormal g k (y :: v.tail))
      0 =
    Cfg.ret k' v'
Tactic: cases v.headI
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
f g : Code
IHf : ∀ (k : Cont) (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal f k v = Cfg.ret k' v'
IHg : ∀ (k : Cont) (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal g k v = Cfg.ret k' v'
k : Cont
v : List ℕ
case :
  ∃ (k' : Cont) (v' : List ℕ),
    Nat.rec (motive := fun (x : ℕ) ↦ Cfg) (stepNormal f k v.tail) (fun (y : ℕ) (x : Cfg) ↦ stepNormal g k (y :: v.tail))
        0 =
      Cfg.ret k' v'
⊢ ∃ (k' : Cont) (v' : List ℕ),
    Nat.rec (motive := fun (x : ℕ) ↦ Cfg) (stepNormal f k v.tail) (fun (y : ℕ) (x : Cfg) ↦ stepNormal g k (y :: v.tail))
        v.headI =
      Cfg.ret k' v'
have case₁ : ∀ (n : ℕ),
  ∃ (k' : Cont) (v' : List ℕ),
    Nat.rec (motive := fun (x : ℕ) ↦ Cfg) (stepNormal f k v.tail) (fun (y : ℕ) (x : Cfg) ↦ stepNormal g k (y :: v.tail))
        (n + 1) =
      Cfg.ret k' v'
Tactic: cases v.headI
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
f g : Code
IHf : ∀ (k : Cont) (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal f k v = Cfg.ret k' v'
IHg : ∀ (k : Cont) (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal g k v = Cfg.ret k' v'
k : Cont
v : List ℕ
⊢ ∃ (k' : Cont) (v' : List ℕ),
    Nat.rec (motive := fun (x : ℕ) ↦ Cfg) (stepNormal f k v.tail) (fun (y : ℕ) (x : Cfg) ↦ stepNormal g k (y :: v.tail))
        v.headI =
      Cfg.ret k' v'
have case : ∃ (k' : Cont) (v' : List ℕ),
  Nat.rec (motive := fun (x : ℕ) ↦ Cfg) (stepNormal f k v.tail) (fun (y : ℕ) (x : Cfg) ↦ stepNormal g k (y :: v.tail))
      0 =
    Cfg.ret k' v'
Tactic: cases v.headI <;> [apply IHf; apply IHg]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
f g : Code
IHf : ∀ (k : Cont) (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal f k v = Cfg.ret k' v'
IHg : ∀ (k : Cont) (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal g k v = Cfg.ret k' v'
k : Cont
v : List ℕ
case :
  ∃ (k' : Cont) (v' : List ℕ),
    Nat.rec (motive := fun (x : ℕ) ↦ Cfg) (stepNormal f k v.tail) (fun (y : ℕ) (x : Cfg) ↦ stepNormal g k (y :: v.tail))
        0 =
      Cfg.ret k' v'
⊢ ∃ (k' : Cont) (v' : List ℕ),
    Nat.rec (motive := fun (x : ℕ) ↦ Cfg) (stepNormal f k v.tail) (fun (y : ℕ) (x : Cfg) ↦ stepNormal g k (y :: v.tail))
        v.headI =
      Cfg.ret k' v'
have case₁ : ∀ (n : ℕ),
  ∃ (k' : Cont) (v' : List ℕ),
    Nat.rec (motive := fun (x : ℕ) ↦ Cfg) (stepNormal f k v.tail) (fun (y : ℕ) (x : Cfg) ↦ stepNormal g k (y :: v.tail))
        (n + 1) =
      Cfg.ret k' v'
Tactic: cases v.headI <;> [apply IHf; apply IHg]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
c : Code
k : Cont
v : List ℕ
⊢ ∃ (k' : Cont) (v' : List ℕ), stepNormal c k v = Cfg.ret k' v'
have cons : ∀ (_f fs : Code) (IHf : ∀ (k : Cont) (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal _f k v = Cfg.ret k' v')
  (_IHfs : ∀ (k : Cont) (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal fs k v = Cfg.ret k' v') (k : Cont)
  (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal (_f.cons fs) k v = Cfg.ret k' v'
Tactic: induction c generalizing k v with
  | cons _f fs IHf _IHfs => apply IHf
  | comp f _g _IHf IHg => apply IHg
  | case f g IHf IHg =>
    rw [stepNormal]
    simp only []
    cases v.headI <;> [apply IHf; apply IHg]
  | fix f IHf => apply IHf
  | _ => exact ⟨_, _, rfl⟩
Cleared hypotheses: c, k, v
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
c : Code
k : Cont
v : List ℕ
cons :
  ∀ (_f fs : Code) (IHf : ∀ (k : Cont) (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal _f k v = Cfg.ret k' v')
    (_IHfs : ∀ (k : Cont) (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal fs k v = Cfg.ret k' v') (k : Cont)
    (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal (_f.cons fs) k v = Cfg.ret k' v'
⊢ ∃ (k' : Cont) (v' : List ℕ), stepNormal c k v = Cfg.ret k' v'
have comp : ∀ (f _g : Code) (_IHf : ∀ (k : Cont) (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal f k v = Cfg.ret k' v')
  (IHg : ∀ (k : Cont) (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal _g k v = Cfg.ret k' v') (k : Cont)
  (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal (f.comp _g) k v = Cfg.ret k' v'
Tactic: induction c generalizing k v with
  | cons _f fs IHf _IHfs => apply IHf
  | comp f _g _IHf IHg => apply IHg
  | case f g IHf IHg =>
    rw [stepNormal]
    simp only []
    cases v.headI <;> [apply IHf; apply IHg]
  | fix f IHf => apply IHf
  | _ => exact ⟨_, _, rfl⟩
Cleared hypotheses: c, k, v
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
c : Code
k : Cont
v : List ℕ
cons :
  ∀ (_f fs : Code) (IHf : ∀ (k : Cont) (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal _f k v = Cfg.ret k' v')
    (_IHfs : ∀ (k : Cont) (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal fs k v = Cfg.ret k' v') (k : Cont)
    (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal (_f.cons fs) k v = Cfg.ret k' v'
comp :
  ∀ (f _g : Code) (_IHf : ∀ (k : Cont) (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal f k v = Cfg.ret k' v')
    (IHg : ∀ (k : Cont) (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal _g k v = Cfg.ret k' v') (k : Cont)
    (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal (f.comp _g) k v = Cfg.ret k' v'
⊢ ∃ (k' : Cont) (v' : List ℕ), stepNormal c k v = Cfg.ret k' v'
have case : ∀ (f g : Code) (IHf : ∀ (k : Cont) (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal f k v = Cfg.ret k' v')
  (IHg : ∀ (k : Cont) (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal g k v = Cfg.ret k' v') (k : Cont)
  (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal (f.case g) k v = Cfg.ret k' v'
Tactic: induction c generalizing k v with
  | cons _f fs IHf _IHfs => apply IHf
  | comp f _g _IHf IHg => apply IHg
  | case f g IHf IHg =>
    rw [stepNormal]
    simp only []
    cases v.headI <;> [apply IHf; apply IHg]
  | fix f IHf => apply IHf
  | _ => exact ⟨_, _, rfl⟩
Cleared hypotheses: c, k, v
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
c : Code
k : Cont
v : List ℕ
cons :
  ∀ (_f fs : Code) (IHf : ∀ (k : Cont) (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal _f k v = Cfg.ret k' v')
    (_IHfs : ∀ (k : Cont) (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal fs k v = Cfg.ret k' v') (k : Cont)
    (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal (_f.cons fs) k v = Cfg.ret k' v'
comp :
  ∀ (f _g : Code) (_IHf : ∀ (k : Cont) (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal f k v = Cfg.ret k' v')
    (IHg : ∀ (k : Cont) (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal _g k v = Cfg.ret k' v') (k : Cont)
    (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal (f.comp _g) k v = Cfg.ret k' v'
case :
  ∀ (f g : Code) (IHf : ∀ (k : Cont) (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal f k v = Cfg.ret k' v')
    (IHg : ∀ (k : Cont) (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal g k v = Cfg.ret k' v') (k : Cont)
    (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal (f.case g) k v = Cfg.ret k' v'
⊢ ∃ (k' : Cont) (v' : List ℕ), stepNormal c k v = Cfg.ret k' v'
have fix : ∀ (f : Code) (IHf : ∀ (k : Cont) (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal f k v = Cfg.ret k' v') (k : Cont)
  (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal f.fix k v = Cfg.ret k' v'
Tactic: induction c generalizing k v with
  | cons _f fs IHf _IHfs => apply IHf
  | comp f _g _IHf IHg => apply IHg
  | case f g IHf IHg =>
    rw [stepNormal]
    simp only []
    cases v.headI <;> [apply IHf; apply IHg]
  | fix f IHf => apply IHf
  | _ => exact ⟨_, _, rfl⟩
Cleared hypotheses: c, k, v
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
c : Code
k : Cont
v : List ℕ
cons :
  ∀ (_f fs : Code) (IHf : ∀ (k : Cont) (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal _f k v = Cfg.ret k' v')
    (_IHfs : ∀ (k : Cont) (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal fs k v = Cfg.ret k' v') (k : Cont)
    (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal (_f.cons fs) k v = Cfg.ret k' v'
comp :
  ∀ (f _g : Code) (_IHf : ∀ (k : Cont) (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal f k v = Cfg.ret k' v')
    (IHg : ∀ (k : Cont) (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal _g k v = Cfg.ret k' v') (k : Cont)
    (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal (f.comp _g) k v = Cfg.ret k' v'
case :
  ∀ (f g : Code) (IHf : ∀ (k : Cont) (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal f k v = Cfg.ret k' v')
    (IHg : ∀ (k : Cont) (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal g k v = Cfg.ret k' v') (k : Cont)
    (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal (f.case g) k v = Cfg.ret k' v'
fix :
  ∀ (f : Code) (IHf : ∀ (k : Cont) (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal f k v = Cfg.ret k' v')
    (k : Cont) (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal f.fix k v = Cfg.ret k' v'
⊢ ∃ (k' : Cont) (v' : List ℕ), stepNormal c k v = Cfg.ret k' v'
have zero' : ∀ (k : Cont) (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal Code.zero' k v = Cfg.ret k' v'
Tactic: induction c generalizing k v with
  | cons _f fs IHf _IHfs => apply IHf
  | comp f _g _IHf IHg => apply IHg
  | case f g IHf IHg =>
    rw [stepNormal]
    simp only []
    cases v.headI <;> [apply IHf; apply IHg]
  | fix f IHf => apply IHf
  | _ => exact ⟨_, _, rfl⟩
Cleared hypotheses: c, k, v
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
c : Code
k : Cont
v : List ℕ
cons :
  ∀ (_f fs : Code) (IHf : ∀ (k : Cont) (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal _f k v = Cfg.ret k' v')
    (_IHfs : ∀ (k : Cont) (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal fs k v = Cfg.ret k' v') (k : Cont)
    (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal (_f.cons fs) k v = Cfg.ret k' v'
comp :
  ∀ (f _g : Code) (_IHf : ∀ (k : Cont) (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal f k v = Cfg.ret k' v')
    (IHg : ∀ (k : Cont) (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal _g k v = Cfg.ret k' v') (k : Cont)
    (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal (f.comp _g) k v = Cfg.ret k' v'
case :
  ∀ (f g : Code) (IHf : ∀ (k : Cont) (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal f k v = Cfg.ret k' v')
    (IHg : ∀ (k : Cont) (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal g k v = Cfg.ret k' v') (k : Cont)
    (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal (f.case g) k v = Cfg.ret k' v'
fix :
  ∀ (f : Code) (IHf : ∀ (k : Cont) (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal f k v = Cfg.ret k' v')
    (k : Cont) (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal f.fix k v = Cfg.ret k' v'
zero' : ∀ (k : Cont) (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal Code.zero' k v = Cfg.ret k' v'
⊢ ∃ (k' : Cont) (v' : List ℕ), stepNormal c k v = Cfg.ret k' v'
have succ : ∀ (k : Cont) (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal Code.succ k v = Cfg.ret k' v'
Tactic: induction c generalizing k v with
  | cons _f fs IHf _IHfs => apply IHf
  | comp f _g _IHf IHg => apply IHg
  | case f g IHf IHg =>
    rw [stepNormal]
    simp only []
    cases v.headI <;> [apply IHf; apply IHg]
  | fix f IHf => apply IHf
  | _ => exact ⟨_, _, rfl⟩
Cleared hypotheses: c, k, v