-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
inst : Inhabited Γ
Γ' : Type u_2
inst_1 : Inhabited Γ'
Λ : Type u_3
inst_2 : Inhabited Λ
Λ' : Type u_4
inst_3 : Inhabited Λ'
M : Machine Γ Λ
f₁ : PointedMap Γ Γ'
f₂ : PointedMap Γ' Γ
g₁ : Λ → Λ'
g₂ : Λ' → Λ
S : Set Λ
f₂₁ : Function.RightInverse f₁.f f₂.f
g₂₁ : ∀ q ∈ S, g₂ (g₁ q) = q
q : Λ
T : Tape Γ
h : { q := q, Tape := T : Cfg Γ Λ }.q ∈ S
none :
  Eq (α := Option (Cfg Γ' Λ'))
    (Option.map (fun (x : Cfg Γ Λ) ↦ { q := g₁ x.q, Tape := Tape.map f₁ x.Tape })
      (Option.map
        (fun (x : Prod.{u_3, u_1} Λ (Stmt Γ)) ↦
          { q := x.1,
            Tape :=
              match (motive := Stmt Γ → Tape Γ) x.2 with
              | Stmt.move d => Tape.move d T
              | Stmt.write a => Tape.write a T })
        Option.none))
    (Option.map
      (fun (x : Prod.{u_4, u_2} Λ' (Stmt Γ')) ↦
        { q := x.1,
          Tape :=
            match (motive := Stmt Γ' → Tape Γ') x.2 with
            | Stmt.move d => Tape.move d (Tape.map f₁ T)
            | Stmt.write a => Tape.write a (Tape.map f₁ T) })
      (Option.map (Prod.map g₁ (Stmt.map f₁)) Option.none))
some :
  ∀ (q' : Λ) (d : Dir),
    Eq (α := Option (Cfg Γ' Λ'))
      (Option.map (fun (x : Cfg Γ Λ) ↦ { q := g₁ x.q, Tape := Tape.map f₁ x.Tape })
        (Option.map
          (fun (x : Prod.{u_3, u_1} Λ (Stmt Γ)) ↦
            { q := x.1,
              Tape :=
                match (motive := Stmt Γ → Tape Γ) x.2 with
                | Stmt.move d => Tape.move d T
                | Stmt.write a => Tape.write a T })
          (Option.some (q', Stmt.move d))))
      (Option.map
        (fun (x : Prod.{u_4, u_2} Λ' (Stmt Γ')) ↦
          { q := x.1,
            Tape :=
              match (motive := Stmt Γ' → Tape Γ') x.2 with
              | Stmt.move d => Tape.move d (Tape.map f₁ T)
              | Stmt.write a => Tape.write a (Tape.map f₁ T) })
        (Option.map (Prod.map g₁ (Stmt.map f₁)) (Option.some (q', Stmt.move d))))
some₁ :
  ∀ (q' : Λ) (a : Γ),
    Eq (α := Option (Cfg Γ' Λ'))
      (Option.map (fun (x : Cfg Γ Λ) ↦ { q := g₁ x.q, Tape := Tape.map f₁ x.Tape })
        (Option.map
          (fun (x : Prod.{u_3, u_1} Λ (Stmt Γ)) ↦
            { q := x.1,
              Tape :=
                match (motive := Stmt Γ → Tape Γ) x.2 with
                | Stmt.move d => Tape.move d T
                | Stmt.write a => Tape.write a T })
          (Option.some (q', Stmt.write a))))
      (Option.map
        (fun (x : Prod.{u_4, u_2} Λ' (Stmt Γ')) ↦
          { q := x.1,
            Tape :=
              match (motive := Stmt Γ' → Tape Γ') x.2 with
              | Stmt.move d => Tape.move d (Tape.map f₁ T)
              | Stmt.write a => Tape.write a (Tape.map f₁ T) })
        (Option.map (Prod.map g₁ (Stmt.map f₁)) (Option.some (q', Stmt.write a))))
⊢ Eq (α := Option (Cfg Γ' Λ'))
    (Option.map (fun (x : Cfg Γ Λ) ↦ { q := g₁ x.q, Tape := Tape.map f₁ x.Tape })
      (Option.map
        (fun (x : Prod.{u_3, u_1} Λ (Stmt Γ)) ↦
          { q := x.1,
            Tape :=
              match (motive := Stmt Γ → Tape Γ) x.2 with
              | Stmt.move d => Tape.move d T
              | Stmt.write a => Tape.write a T })
        (M q T.head)))
    (Option.map
      (fun (x : Prod.{u_4, u_2} Λ' (Stmt Γ')) ↦
        { q := x.1,
          Tape :=
            match (motive := Stmt Γ' → Tape Γ') x.2 with
            | Stmt.move d => Tape.move d (Tape.map f₁ T)
            | Stmt.write a => Tape.write a (Tape.map f₁ T) })
      (Option.map (Prod.map g₁ (Stmt.map f₁)) (M q T.head)))

Tactic:
rcases M q T.1 with (_ | ⟨q', d | a⟩)

Premises used: Turing.Tape.head