-- Mathlib/Computability/TMToPartrec.lean
theorem copy_ok (q s a b c d) :
    Reaches₁ (TM2.step tr) ⟨some (Λ'.copy q), s, K'.elim a b c d⟩
      ⟨some q, none, K'.elim (List.reverseAux b a) [] c (List.reverseAux b d)⟩

Proof state:
case cons
q : Λ'
c : List Γ'
x : Γ'
b : List Γ'
IH :
  ∀ (s : Option Γ') (a d : List Γ'),
    Reaches₁ (TM2.step tr) { l := some q.copy, var := s, stk := elim a b c d }
      { l := some q, var := none, stk := elim (b.reverseAux a) [] c (b.reverseAux d) }
s : Option Γ'
a d : List Γ'
⊢ TransGen
    (fun a b =>
      (match a with
        | { l := none, var := var, stk := stk } => none
        | { l := some l, var := v, stk := S } => some (TM2.stepAux (tr l) v S)) =
        some b)
    { l := some q.copy, var := some x, stk := elim ((some x).iget :: a) b c ((some x).iget :: d) }
    { l := some q, var := none, stk := elim (b.reverseAux (x :: a)) [] c (b.reverseAux (x :: d)) }

Tactic:
exact IH _ _ _

Result:
no goals

Proof state:
q : Λ'
s : Option Γ'
a b c d : List Γ'
⊢ Reaches₁ (TM2.step tr) { l := some q.copy, var := s, stk := elim a b c d }
    { l := some q, var := none, stk := elim (b.reverseAux a) [] c (b.reverseAux d) }

Tactic:
induction' b with x b IH generalizing a d s

Result:
case nil
q : Λ'
c : List Γ'
s : Option Γ'
a d : List Γ'
⊢ Reaches₁ (TM2.step tr) { l := some q.copy, var := s, stk := elim a [] c d }
    { l := some q, var := none, stk := elim ([].reverseAux a) [] c ([].reverseAux d) }

case cons
q : Λ'
c : List Γ'
x : Γ'
b : List Γ'
IH :
  ∀ (s : Option Γ') (a d : List Γ'),
    Reaches₁ (TM2.step tr) { l := some q.copy, var := s, stk := elim a b c d }
      { l := some q, var := none, stk := elim (b.reverseAux a) [] c (b.reverseAux d) }
s : Option Γ'
a d : List Γ'
⊢ Reaches₁ (TM2.step tr) { l := some q.copy, var := s, stk := elim a (x :: b) c d }
    { l := some q, var := none, stk := elim ((x :: b).reverseAux a) [] c ((x :: b).reverseAux d) }

Proof state:
case cons
q : Λ'
c : List Γ'
x : Γ'
b : List Γ'
IH :
  ∀ (s : Option Γ') (a d : List Γ'),
    Reaches₁ (TM2.step tr) { l := some q.copy, var := s, stk := elim a b c d }
      { l := some q, var := none, stk := elim (b.reverseAux a) [] c (b.reverseAux d) }
s : Option Γ'
a d : List Γ'
⊢ TransGen (fun a b => b ∈ TM2.step tr a) (TM2.stepAux (tr q.copy) s (elim a (x :: b) c d))
    { l := some q, var := none, stk := elim ((x :: b).reverseAux a) [] c ((x :: b).reverseAux d) }

Tactic:
rw [tr]

Result:
case cons
q : Λ'
c : List Γ'
x : Γ'
b : List Γ'
IH :
  ∀ (s : Option Γ') (a d : List Γ'),
    Reaches₁ (TM2.step tr) { l := some q.copy, var := s, stk := elim a b c d }
      { l := some q, var := none, stk := elim (b.reverseAux a) [] c (b.reverseAux d) }
s : Option Γ'
a d : List Γ'
⊢ TransGen (fun a b => b ∈ TM2.step tr a)
    (TM2.stepAux (pop' rev (branch Option.isSome (push' main (push' stack (goto fun x => q.copy))) (goto fun x => q))) s
      (elim a (x :: b) c d))
    { l := some q, var := none, stk := elim ((x :: b).reverseAux a) [] c ((x :: b).reverseAux d) }

Proof state:
case cons
q : Λ'
c : List Γ'
x : Γ'
b : List Γ'
IH :
  ∀ (s : Option Γ') (a d : List Γ'),
    Reaches₁ (TM2.step tr) { l := some q.copy, var := s, stk := elim a b c d }
      { l := some q, var := none, stk := elim (b.reverseAux a) [] c (b.reverseAux d) }
s : Option Γ'
a d : List Γ'
⊢ TransGen (fun a b => b ∈ TM2.step tr a)
    (TM2.stepAux (pop' rev (branch Option.isSome (push' main (push' stack (goto fun x => q.copy))) (goto fun x => q))) s
      (elim a (x :: b) c d))
    { l := some q, var := none, stk := elim ((x :: b).reverseAux a) [] c ((x :: b).reverseAux d) }

Tactic:
simp only [TM2.step, Option.mem_def, TM2.stepAux, elim_rev, List.head?_cons, Option.isSome_some,
  List.tail_cons, elim_update_rev, ne_eq, Function.update_of_ne, elim_main, elim_update_main,
  elim_stack, elim_update_stack, cond_true, List.reverseAux_cons, pop', push']

Result:
case cons
q : Λ'
c : List Γ'
x : Γ'
b : List Γ'
IH :
  ∀ (s : Option Γ') (a d : List Γ'),
    Reaches₁ (TM2.step tr) { l := some q.copy, var := s, stk := elim a b c d }
      { l := some q, var := none, stk := elim (b.reverseAux a) [] c (b.reverseAux d) }
s : Option Γ'
a d : List Γ'
⊢ TransGen
    (fun a b =>
      (match a with
        | { l := none, var := var, stk := stk } => none
        | { l := some l, var := v, stk := S } => some (TM2.stepAux (tr l) v S)) =
        some b)
    { l := some q.copy, var := some x, stk := elim ((some x).iget :: a) b c ((some x).iget :: d) }
    { l := some q, var := none, stk := elim (b.reverseAux (x :: a)) [] c (b.reverseAux (x :: d)) }

Proof state:
case nil
q : Λ'
c : List Γ'
s : Option Γ'
a d : List Γ'
⊢ Reaches₁ (TM2.step tr) { l := some q.copy, var := s, stk := elim a [] c d }
    { l := some q, var := none, stk := elim ([].reverseAux a) [] c ([].reverseAux d) }

Tactic:
refine TransGen.single ?_

Result:
case nil
q : Λ'
c : List Γ'
s : Option Γ'
a d : List Γ'
⊢ { l := some q, var := none, stk := elim ([].reverseAux a) [] c ([].reverseAux d) } ∈
    TM2.step tr { l := some q.copy, var := s, stk := elim a [] c d }

Proof state:
case nil
q : Λ'
c : List Γ'
s : Option Γ'
a d : List Γ'
⊢ { l := some q, var := none, stk := elim ([].reverseAux a) [] c ([].reverseAux d) } ∈
    TM2.step tr { l := some q.copy, var := s, stk := elim a [] c d }

Tactic:
simp

Result:
no goals

Proof state:
case cons
q : Λ'
c : List Γ'
x : Γ'
b : List Γ'
IH :
  ∀ (s : Option Γ') (a d : List Γ'),
    Reaches₁ (TM2.step tr) { l := some q.copy, var := s, stk := elim a b c d }
      { l := some q, var := none, stk := elim (b.reverseAux a) [] c (b.reverseAux d) }
s : Option Γ'
a d : List Γ'
⊢ Reaches₁ (TM2.step tr) { l := some q.copy, var := s, stk := elim a (x :: b) c d }
    { l := some q, var := none, stk := elim ((x :: b).reverseAux a) [] c ((x :: b).reverseAux d) }

Tactic:
refine TransGen.head rfl ?_

Result:
case cons
q : Λ'
c : List Γ'
x : Γ'
b : List Γ'
IH :
  ∀ (s : Option Γ') (a d : List Γ'),
    Reaches₁ (TM2.step tr) { l := some q.copy, var := s, stk := elim a b c d }
      { l := some q, var := none, stk := elim (b.reverseAux a) [] c (b.reverseAux d) }
s : Option Γ'
a d : List Γ'
⊢ TransGen (fun a b => b ∈ TM2.step tr a) (TM2.stepAux (tr q.copy) s (elim a (x :: b) c d))
    { l := some q, var := none, stk := elim ((x :: b).reverseAux a) [] c ((x :: b).reverseAux d) }