-- Mathlib/Computability/TMToPartrec.lean
theorem clear_ok {p k q s L₁ o L₂} {S : K' → List Γ'} (e : splitAtPred p (S k) = (L₁, o, L₂)) :
    Reaches₁ (TM2.step tr) ⟨some (Λ'.clear p k q), s, S⟩ ⟨some q, o, update S k L₂⟩

Proof state:
case cons
p : Γ' → Bool
k : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
a : Γ'
L₁ : List Γ'
IH :
  ∀ {s : Option Γ'} {S : K' → List Γ'},
    splitAtPred p (S k) = (L₁, o, L₂) →
      Reaches₁ (TM2.step tr) { l := some (Λ'.clear p k q), var := s, stk := S }
        { l := some q, var := o, stk := update S k L₂ }
s : Option Γ'
S : K' → List Γ'
e : splitAtPred p (S k) = (a :: L₁, o, L₂)
⊢ TransGen (fun a b => b ∈ TM2.step tr a)
    (TM2.stepAux (pop' k (branch (fun s => s.elim true p) (goto fun x => q) (goto fun x => Λ'.clear p k q))) s S)
    { l := some q, var := o, stk := update S k L₂ }

Tactic:
simp only [pop', TM2.step, Option.mem_def, TM2.stepAux, Option.elim]

Result:
case cons
p : Γ' → Bool
k : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
a : Γ'
L₁ : List Γ'
IH :
  ∀ {s : Option Γ'} {S : K' → List Γ'},
    splitAtPred p (S k) = (L₁, o, L₂) →
      Reaches₁ (TM2.step tr) { l := some (Λ'.clear p k q), var := s, stk := S }
        { l := some q, var := o, stk := update S k L₂ }
s : Option Γ'
S : K' → List Γ'
e : splitAtPred p (S k) = (a :: L₁, o, L₂)
⊢ 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)
    (bif
        match (S k).head?, true, p with
        | some x, x_1, f => f x
        | none, y, x => y then
      { l := some q, var := (S k).head?, stk := update S k (S k).tail }
    else { l := some (Λ'.clear p k q), var := (S k).head?, stk := update S k (S k).tail })
    { l := some q, var := o, stk := update S k L₂ }

Proof state:
case nil
p : Γ' → Bool
k : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
s : Option Γ'
S : K' → List Γ'
e : splitAtPred p (S k) = ([], o, L₂)
⊢ ReflTransGen (fun a b => b ∈ TM2.step tr a)
    (TM2.stepAux (pop' k (branch (fun s => s.elim true p) (goto fun x => q) (goto fun x => Λ'.clear p k q))) s S)
    { l := some q, var := o, stk := update S k L₂ }

Tactic:
simp only [pop', TM2.step, Option.mem_def, TM2.stepAux, Option.elim]

Result:
case nil
p : Γ' → Bool
k : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
s : Option Γ'
S : K' → List Γ'
e : splitAtPred p (S k) = ([], o, L₂)
⊢ ReflTransGen
    (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)
    (bif
        match (S k).head?, true, p with
        | some x, x_1, f => f x
        | none, y, x => y then
      { l := some q, var := (S k).head?, stk := update S k (S k).tail }
    else { l := some (Λ'.clear p k q), var := (S k).head?, stk := update S k (S k).tail })
    { l := some q, var := o, stk := update S k L₂ }

Proof state:
case cons
p : Γ' → Bool
k : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
a : Γ'
L₁ : List Γ'
IH :
  ∀ {s : Option Γ'} {S : K' → List Γ'},
    splitAtPred p (S k) = (L₁, o, L₂) →
      Reaches₁ (TM2.step tr) { l := some (Λ'.clear p k q), var := s, stk := S }
        { l := some q, var := o, stk := update S k L₂ }
s : Option Γ'
S : K' → List Γ'
e : splitAtPred p (S k) = (a :: L₁, o, L₂)
⊢ 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)
    (bif
        match (S k).head?, true, p with
        | some x, x_1, f => f x
        | none, y, x => y then
      { l := some q, var := (S k).head?, stk := update S k (S k).tail }
    else { l := some (Λ'.clear p k q), var := (S k).head?, stk := update S k (S k).tail })
    { l := some q, var := o, stk := update S k L₂ }

Tactic:
rcases e₁ : S k with - | ⟨a', Sk⟩ <;> rw [e₁, splitAtPred] at e

Result:
case cons.nil
p : Γ' → Bool
k : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
a : Γ'
L₁ : List Γ'
IH :
  ∀ {s : Option Γ'} {S : K' → List Γ'},
    splitAtPred p (S k) = (L₁, o, L₂) →
      Reaches₁ (TM2.step tr) { l := some (Λ'.clear p k q), var := s, stk := S }
        { l := some q, var := o, stk := update S k L₂ }
s : Option Γ'
S : K' → List Γ'
e : ([], none, []) = (a :: L₁, o, L₂)
e₁ : S k = []
⊢ 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)
    (bif
        match [].head?, true, p with
        | some x, x_1, f => f x
        | none, y, x => y then
      { l := some q, var := [].head?, stk := update S k [].tail }
    else { l := some (Λ'.clear p k q), var := [].head?, stk := update S k [].tail })
    { l := some q, var := o, stk := update S k L₂ }

case cons.cons
p : Γ' → Bool
k : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
a : Γ'
L₁ : List Γ'
IH :
  ∀ {s : Option Γ'} {S : K' → List Γ'},
    splitAtPred p (S k) = (L₁, o, L₂) →
      Reaches₁ (TM2.step tr) { l := some (Λ'.clear p k q), var := s, stk := S }
        { l := some q, var := o, stk := update S k L₂ }
s : Option Γ'
S : K' → List Γ'
a' : Γ'
Sk : List Γ'
e :
  (bif p a' then ([], some a', Sk)
    else
      match splitAtPred p Sk with
      | (l₁, o, l₂) => (a' :: l₁, o, l₂)) =
    (a :: L₁, o, L₂)
e₁ : S k = a' :: Sk
⊢ 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)
    (bif
        match (a' :: Sk).head?, true, p with
        | some x, x_1, f => f x
        | none, y, x => y then
      { l := some q, var := (a' :: Sk).head?, stk := update S k (a' :: Sk).tail }
    else { l := some (Λ'.clear p k q), var := (a' :: Sk).head?, stk := update S k (a' :: Sk).tail })
    { l := some q, var := o, stk := update S k L₂ }

Proof state:
case nil.nil
p : Γ' → Bool
k : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
s : Option Γ'
S : K' → List Γ'
e : splitAtPred p [] = ([], o, L₂)
⊢ ReflTransGen
    (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)
    (bif
        match [].head?, true, p with
        | some x, x_1, f => f x
        | none, y, x => y then
      { l := some q, var := [].head?, stk := update S k [].tail }
    else { l := some (Λ'.clear p k q), var := [].head?, stk := update S k [].tail })
    { l := some q, var := o, stk := update S k L₂ }

Tactic:
cases e

Result:
case nil.nil.refl
p : Γ' → Bool
k : K'
q : Λ'
s : Option Γ'
S : K' → List Γ'
⊢ ReflTransGen
    (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)
    (bif
        match [].head?, true, p with
        | some x, x_1, f => f x
        | none, y, x => y then
      { l := some q, var := [].head?, stk := update S k [].tail }
    else { l := some (Λ'.clear p k q), var := [].head?, stk := update S k [].tail })
    { l := some q, var := none, stk := update S k [] }

Proof state:
case nil.cons.true.intro
p : Γ' → Bool
k : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
s : Option Γ'
S : K' → List Γ'
a : Γ'
Sk : List Γ'
e₁ : some a = o
e₂ : Sk = L₂
⊢ ReflTransGen
    (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, var := some a, stk := update S k Sk } { l := some q, var := o, stk := update S k L₂ }

Tactic:
rw [e₁, e₂]

Result:
no goals