-- Mathlib/Computability/PostTuringMachine.lean
theorem tr_respects : Respects (TM0.step M) (TM1.step (tr M)) fun a b ↦ trCfg M a = b :=
  fun_respects.2 fun ⟨q, T⟩ ↦ by
    rcases e : M q T.1 with - | val
    · simp only [TM0.step, trCfg, e]; exact Eq.refl none
    obtain ⟨q', s⟩ := val
    simp only [FRespects, TM0.step, trCfg, e, Option.isSome, cond, Option.map_some']
    revert e
    have : TM1.step (tr M) ⟨some (Λ'.act s q'), (), T⟩ = some ⟨some (Λ'.normal q'), (), match s with
        | TM0.Stmt.move d => T.move d
        | TM0.Stmt.write a => T.write a⟩

Proof state:
case some.mk
Γ : Type u_1
inst✝¹ : Inhabited Γ
Λ : Type u_2
inst✝ : Inhabited Λ
M : TM0.Machine Γ Λ
x✝ : TM0.Cfg Γ Λ
q : Λ
T : Tape Γ
q' : Λ
s : TM0.Stmt Γ
this :
  TM1.step (tr M) { l := some (Λ'.act s q'), var := (), Tape := T } =
    some
      { l := some (Λ'.normal q'), var := (),
        Tape :=
          match s with
          | TM0.Stmt.move d => Tape.move d T
          | TM0.Stmt.write a => Tape.write a T }
⊢ M q T.head = some (q', s) →
    Reaches₁ (TM1.step (tr M)) { l := some (Λ'.normal q), var := (), Tape := T }
      {
        l :=
          match
            match
              M q'
                (match s with
                  | TM0.Stmt.move d => Tape.move d T
                  | TM0.Stmt.write a => Tape.write a T).head with
            | some val => true
            | none => false with
          | true => some (Λ'.normal q')
          | false => none,
        var := (),
        Tape :=
          match s with
          | TM0.Stmt.move d => Tape.move d T
          | TM0.Stmt.write a => Tape.write a T }

Tactic:
intro e

Result:
case some.mk
Γ : Type u_1
inst✝¹ : Inhabited Γ
Λ : Type u_2
inst✝ : Inhabited Λ
M : TM0.Machine Γ Λ
x✝ : TM0.Cfg Γ Λ
q : Λ
T : Tape Γ
q' : Λ
s : TM0.Stmt Γ
this :
  TM1.step (tr M) { l := some (Λ'.act s q'), var := (), Tape := T } =
    some
      { l := some (Λ'.normal q'), var := (),
        Tape :=
          match s with
          | TM0.Stmt.move d => Tape.move d T
          | TM0.Stmt.write a => Tape.write a T }
e : M q T.head = some (q', s)
⊢ Reaches₁ (TM1.step (tr M)) { l := some (Λ'.normal q), var := (), Tape := T }
    {
      l :=
        match
          match
            M q'
              (match s with
                | TM0.Stmt.move d => Tape.move d T
                | TM0.Stmt.write a => Tape.write a T).head with
          | some val => true
          | none => false with
        | true => some (Λ'.normal q')
        | false => none,
      var := (),
      Tape :=
        match s with
        | TM0.Stmt.move d => Tape.move d T
        | TM0.Stmt.write a => Tape.write a T }

Proof state:
case none
Γ : Type u_1
inst✝¹ : Inhabited Γ
Λ : Type u_2
inst✝ : Inhabited Λ
M : TM0.Machine Γ Λ
x✝ : TM0.Cfg Γ Λ
q : Λ
T : Tape Γ
e : M q T.head = none
⊢ FRespects (TM1.step (tr M)) (trCfg M) { l := bif none.isSome then some (Λ'.normal q) else none, var := (), Tape := T }
    (Option.map
      (fun x =>
        { q := x.1,
          Tape :=
            match x.2 with
            | TM0.Stmt.move d => Tape.move d T
            | TM0.Stmt.write a => Tape.write a T })
      none)

Tactic:
exact Eq.refl none

Result:
no goals

Proof state:
case some.mk.refine_2
Γ : Type u_1
inst✝¹ : Inhabited Γ
Λ : Type u_2
inst✝ : Inhabited Λ
M : TM0.Machine Γ Λ
x✝ : TM0.Cfg Γ Λ
q : Λ
T : Tape Γ
q' : Λ
s : TM0.Stmt Γ
this :
  TM1.step (tr M) { l := some (Λ'.act s q'), var := (), Tape := T } =
    some
      { l := some (Λ'.normal q'), var := (),
        Tape :=
          match s with
          | TM0.Stmt.move d => Tape.move d T
          | TM0.Stmt.write a => Tape.write a T }
e : M q T.head = some (q', s)
⊢ ReflTransGen (fun a b => b ∈ TM1.step (tr M) a)
    { l := some (Λ'.normal q'), var := (),
      Tape :=
        match s with
        | TM0.Stmt.move d => Tape.move d T
        | TM0.Stmt.write a => Tape.write a T }
    {
      l :=
        match
          match
            M q'
              (match s with
                | TM0.Stmt.move d => Tape.move d T
                | TM0.Stmt.write a => Tape.write a T).head with
          | some val => true
          | none => false with
        | true => some (Λ'.normal q')
        | false => none,
      var := (),
      Tape :=
        match s with
        | TM0.Stmt.move d => Tape.move d T
        | TM0.Stmt.write a => Tape.write a T }

Tactic:
cases e' : M q' _

Result:
case some.mk.refine_2.none
Γ : Type u_1
inst✝¹ : Inhabited Γ
Λ : Type u_2
inst✝ : Inhabited Λ
M : TM0.Machine Γ Λ
x✝ : TM0.Cfg Γ Λ
q : Λ
T : Tape Γ
q' : Λ
s : TM0.Stmt Γ
this :
  TM1.step (tr M) { l := some (Λ'.act s q'), var := (), Tape := T } =
    some
      { l := some (Λ'.normal q'), var := (),
        Tape :=
          match s with
          | TM0.Stmt.move d => Tape.move d T
          | TM0.Stmt.write a => Tape.write a T }
e : M q T.head = some (q', s)
e' :
  M q'
      (match s with
        | TM0.Stmt.move d => Tape.move d T
        | TM0.Stmt.write a => Tape.write a T).head =
    none
⊢ ReflTransGen (fun a b => b ∈ TM1.step (tr M) a)
    { l := some (Λ'.normal q'), var := (),
      Tape :=
        match s with
        | TM0.Stmt.move d => Tape.move d T
        | TM0.Stmt.write a => Tape.write a T }
    {
      l :=
        match
          match none with
          | some val => true
          | none => false with
        | true => some (Λ'.normal q')
        | false => none,
      var := (),
      Tape :=
        match s with
        | TM0.Stmt.move d => Tape.move d T
        | TM0.Stmt.write a => Tape.write a T }

case some.mk.refine_2.some
Γ : Type u_1
inst✝¹ : Inhabited Γ
Λ : Type u_2
inst✝ : Inhabited Λ
M : TM0.Machine Γ Λ
x✝ : TM0.Cfg Γ Λ
q : Λ
T : Tape Γ
q' : Λ
s : TM0.Stmt Γ
this :
  TM1.step (tr M) { l := some (Λ'.act s q'), var := (), Tape := T } =
    some
      { l := some (Λ'.normal q'), var := (),
        Tape :=
          match s with
          | TM0.Stmt.move d => Tape.move d T
          | TM0.Stmt.write a => Tape.write a T }
e : M q T.head = some (q', s)
val✝ : Λ × TM0.Stmt Γ
e' :
  M q'
      (match s with
        | TM0.Stmt.move d => Tape.move d T
        | TM0.Stmt.write a => Tape.write a T).head =
    some val✝
⊢ ReflTransGen (fun a b => b ∈ TM1.step (tr M) a)
    { l := some (Λ'.normal q'), var := (),
      Tape :=
        match s with
        | TM0.Stmt.move d => Tape.move d T
        | TM0.Stmt.write a => Tape.write a T }
    {
      l :=
        match
          match some val✝ with
          | some val => true
          | none => false with
        | true => some (Λ'.normal q')
        | false => none,
      var := (),
      Tape :=
        match s with
        | TM0.Stmt.move d => Tape.move d T
        | TM0.Stmt.write a => Tape.write a T }