-- Mathlib/Computability/TMConfig.lean
theorem stepRet_then {k k' : Cont} {v} : stepRet (k.then k') v = (stepRet k v).then k'

Proof state:
case pos
k' : Cont
a✝¹ : Code
a✝ : Cont
k_ih : ∀ {v : List ℕ}, stepRet (a✝.then k') v = (stepRet a✝ v).then k'
v : List ℕ
h✝ : v.headI = 0
⊢ (stepRet a✝ v.tail).then k' = (stepRet a✝ v.tail).then k'

Tactic:
rw [← k_ih]

Result:
no goals

Proof state:
case fix
k' : Cont
a✝¹ : Code
a✝ : Cont
k_ih : ∀ {v : List ℕ}, stepRet (a✝.then k') v = (stepRet a✝ v).then k'
v : List ℕ
⊢ (if v.headI = 0 then (stepRet a✝ v.tail).then k' else stepNormal a✝¹ (Cont.fix a✝¹ (a✝.then k')) v.tail) =
    (if v.headI = 0 then stepRet a✝ v.tail else stepNormal a✝¹ (Cont.fix a✝¹ a✝) v.tail).then k'

Tactic:
split_ifs

Result:
case pos
k' : Cont
a✝¹ : Code
a✝ : Cont
k_ih : ∀ {v : List ℕ}, stepRet (a✝.then k') v = (stepRet a✝ v).then k'
v : List ℕ
h✝ : v.headI = 0
⊢ (stepRet a✝ v.tail).then k' = (stepRet a✝ v.tail).then k'

case neg
k' : Cont
a✝¹ : Code
a✝ : Cont
k_ih : ∀ {v : List ℕ}, stepRet (a✝.then k') v = (stepRet a✝ v).then k'
v : List ℕ
h✝ : ¬v.headI = 0
⊢ stepNormal a✝¹ (Cont.fix a✝¹ (a✝.then k')) v.tail = (stepNormal a✝¹ (Cont.fix a✝¹ a✝) v.tail).then k'

Proof state:
case neg
k' : Cont
a✝¹ : Code
a✝ : Cont
k_ih : ∀ {v : List ℕ}, stepRet (a✝.then k') v = (stepRet a✝ v).then k'
v : List ℕ
h✝ : ¬v.headI = 0
⊢ stepNormal a✝¹ (Cont.fix a✝¹ (a✝.then k')) v.tail = (stepNormal a✝¹ (Cont.fix a✝¹ a✝) v.tail).then k'

Tactic:
rw [← stepNormal_then]

Result:
case neg
k' : Cont
a✝¹ : Code
a✝ : Cont
k_ih : ∀ {v : List ℕ}, stepRet (a✝.then k') v = (stepRet a✝ v).then k'
v : List ℕ
h✝ : ¬v.headI = 0
⊢ stepNormal a✝¹ (Cont.fix a✝¹ (a✝.then k')) v.tail = stepNormal a✝¹ ((Cont.fix a✝¹ a✝).then k') v.tail

Proof state:
case neg
k' : Cont
a✝¹ : Code
a✝ : Cont
k_ih : ∀ {v : List ℕ}, stepRet (a✝.then k') v = (stepRet a✝ v).then k'
v : List ℕ
h✝ : ¬v.headI = 0
⊢ stepNormal a✝¹ (Cont.fix a✝¹ (a✝.then k')) v.tail = stepNormal a✝¹ ((Cont.fix a✝¹ a✝).then k') v.tail

Tactic:
rfl

Result:
no goals

Proof state:
case cons₁
k' : Cont
a✝² : Code
a✝¹ : List ℕ
a✝ : Cont
a_ih✝ : ∀ {v : List ℕ}, stepRet (a✝.then k') v = (stepRet a✝ v).then k'
v : List ℕ
⊢ stepNormal a✝² (Cont.cons₂ v (a✝.then k')) a✝¹ = stepNormal a✝² ((Cont.cons₂ v a✝).then k') a✝¹

Tactic:
rfl

Result:
no goals

Proof state:
case halt
k' : Cont
v : List ℕ
⊢ stepRet k' v = (Cfg.halt v).then k'

Tactic:
simp only [Cfg.then]

Result:
no goals

Proof state:
case cons₁
k' : Cont
a✝² : Code
a✝¹ : List ℕ
a✝ : Cont
a_ih✝ : ∀ {v : List ℕ}, stepRet (a✝.then k') v = (stepRet a✝ v).then k'
v : List ℕ
⊢ stepNormal a✝² (Cont.cons₂ v (a✝.then k')) a✝¹ = (stepNormal a✝² (Cont.cons₂ v a✝) a✝¹).then k'

Tactic:
rw [← stepNormal_then]

Result:
case cons₁
k' : Cont
a✝² : Code
a✝¹ : List ℕ
a✝ : Cont
a_ih✝ : ∀ {v : List ℕ}, stepRet (a✝.then k') v = (stepRet a✝ v).then k'
v : List ℕ
⊢ stepNormal a✝² (Cont.cons₂ v (a✝.then k')) a✝¹ = stepNormal a✝² ((Cont.cons₂ v a✝).then k') a✝¹

Proof state:
case comp
k' : Cont
a✝¹ : Code
a✝ : Cont
a_ih✝ : ∀ {v : List ℕ}, stepRet (a✝.then k') v = (stepRet a✝ v).then k'
v : List ℕ
⊢ stepNormal a✝¹ (a✝.then k') v = (stepNormal a✝¹ a✝ v).then k'

Tactic:
rw [← stepNormal_then]

Result:
no goals