Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case some.branch.false
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Inhabited Γ
x✝ : TM1.Cfg Γ Λ σ
l₁ : Λ
p : Γ → σ → Bool
a✝¹ a✝ : TM1.Stmt Γ Λ σ
IH₁ :
  ∀ (v : σ) (T : Tape Γ),
    Reaches₁ (TM0.step (tr M)) { q := (some a✝¹, v), Tape := T }
      {
        q :=
          (match (TM1.stepAux a✝¹ v T).l with
            | some x => some (M x)
            | none => none,
            (TM1.stepAux a✝¹ v T).var),
        Tape := (TM1.stepAux a✝¹ v T).Tape }
IH₂ :
  ∀ (v : σ) (T : Tape Γ),
    Reaches₁ (TM0.step (tr M)) { q := (some a✝, v), Tape := T }
      {
        q :=
          (match (TM1.stepAux a✝ v T).l with
            | some x => some (M x)
            | none => none,
            (TM1.stepAux a✝ v T).var),
        Tape := (TM1.stepAux a✝ v T).Tape }
v : σ
T : Tape Γ
e : p T.head v = false
⊢ Reaches₁ (TM0.step (tr M)) { q := (some (TM1.Stmt.branch p a✝¹ a✝), v), Tape := T }
    {
      q :=
        (match (bif false then TM1.stepAux a✝¹ v T else TM1.stepAux a✝ v T).l with
          | some x => some (M x)
          | none => none,
          (bif false then TM1.stepAux a✝¹ v T else TM1.stepAux a✝ v T).var),
      Tape := (bif false then TM1.stepAux a✝¹ v T else TM1.stepAux a✝ v T).Tape }

pp: case some.branch.true
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Inhabited Γ
x✝ : TM1.Cfg Γ Λ σ
l₁ : Λ
p : Γ → σ → Bool
a✝¹ a✝ : TM1.Stmt Γ Λ σ
IH₁ :
  ∀ (v : σ) (T : Tape Γ),
    Reaches₁ (TM0.step (tr M)) { q := (some a✝¹, v), Tape := T }
      {
        q :=
          (match (TM1.stepAux a✝¹ v T).l with
            | some x => some (M x)
            | none => none,
            (TM1.stepAux a✝¹ v T).var),
        Tape := (TM1.stepAux a✝¹ v T).Tape }
IH₂ :
  ∀ (v : σ) (T : Tape Γ),
    Reaches₁ (TM0.step (tr M)) { q := (some a✝, v), Tape := T }
      {
        q :=
          (match (TM1.stepAux a✝ v T).l with
            | some x => some (M x)
            | none => none,
            (TM1.stepAux a✝ v T).var),
        Tape := (TM1.stepAux a✝ v T).Tape }
v : σ
T : Tape Γ
e : p T.head v = true
⊢ Reaches₁ (TM0.step (tr M)) { q := (some (TM1.Stmt.branch p a✝¹ a✝), v), Tape := T }
    {
      q :=
        (match (bif true then TM1.stepAux a✝¹ v T else TM1.stepAux a✝ v T).l with
          | some x => some (M x)
          | none => none,
          (bif true then TM1.stepAux a✝¹ v T else TM1.stepAux a✝ v T).var),
      Tape := (bif true then TM1.stepAux a✝¹ v T else TM1.stepAux a✝ v T).Tape }

Tactic:
· exact (reaches₁_eq (by simp only [TM0.step, tr, trAux, e]; rfl)).2 (IH₂ _ _)

Goal state after:
case some.branch.true
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Inhabited Γ
x✝ : TM1.Cfg Γ Λ σ
l₁ : Λ
p : Γ → σ → Bool
a✝¹ a✝ : TM1.Stmt Γ Λ σ
IH₁ :
  ∀ (v : σ) (T : Tape Γ),
    Reaches₁ (TM0.step (tr M)) { q := (some a✝¹, v), Tape := T }
      {
        q :=
          (match (TM1.stepAux a✝¹ v T).l with
            | some x => some (M x)
            | none => none,
            (TM1.stepAux a✝¹ v T).var),
        Tape := (TM1.stepAux a✝¹ v T).Tape }
IH₂ :
  ∀ (v : σ) (T : Tape Γ),
    Reaches₁ (TM0.step (tr M)) { q := (some a✝, v), Tape := T }
      {
        q :=
          (match (TM1.stepAux a✝ v T).l with
            | some x => some (M x)
            | none => none,
            (TM1.stepAux a✝ v T).var),
        Tape := (TM1.stepAux a✝ v T).Tape }
v : σ
T : Tape Γ
e : p T.head v = true
⊢ Reaches₁ (TM0.step (tr M)) { q := (some (TM1.Stmt.branch p a✝¹ a✝), v), Tape := T }
    {
      q :=
        (match (bif true then TM1.stepAux a✝¹ v T else TM1.stepAux a✝ v T).l with
          | some x => some (M x)
          | none => none,
          (bif true then TM1.stepAux a✝¹ v T else TM1.stepAux a✝ v T).var),
      Tape := (bif true then TM1.stepAux a✝¹ v T else TM1.stepAux a✝ v T).Tape }