awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
k : Cont
v : List ℕ
⊢ eval step (stepRet k v) = Cfg.halt <$> k.eval v
have halt : ∀ {v : List ℕ}, eval step (stepRet Cont.halt v) = Cfg.halt <$> Cont.halt.eval v
Tactic: induction k generalizing v with
  | halt =>
    simp only [Cont.eval, map_pure]
    exact Part.eq_some_iff.2 (mem_eval.2 ⟨ReflTransGen.refl, rfl⟩)
  | cons₁ fs as k IH =>
    rw [Cont.eval, stepRet, code_is_ok]
    simp only [← bind_pure_comp, bind_assoc]; congr; funext v'
    rw [reaches_eval]; swap
    · exact ReflTransGen.single rfl
    rw [stepRet, IH, bind_pure_comp]
  | cons₂ ns k IH => rw [Cont.eval, stepRet]; exact IH
  | comp f k IH =>
    rw [Cont.eval, stepRet, code_is_ok]
    simp only [← bind_pure_comp, bind_assoc]; congr; funext v'
    rw [reaches_eval]; swap
    · exact ReflTransGen.single rfl
    rw [IH, bind_pure_comp]
  | fix f k IH =>
    rw [Cont.eval, stepRet]; simp only
    split_ifs; · exact IH
    simp only [← bind_pure_comp, bind_assoc, cont_eval_fix (code_is_ok _)]
    congr; funext; rw [bind_pure_comp, ← IH]
    exact reaches_eval (ReflTransGen.single rfl)
Cleared hypotheses: k, v
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
k : Cont
v : List ℕ
halt : ∀ {v : List ℕ}, eval step (stepRet Cont.halt v) = Cfg.halt <$> Cont.halt.eval v
⊢ eval step (stepRet k v) = Cfg.halt <$> k.eval v
have cons₁ : ∀ (fs : Code) (as : List ℕ) (k : Cont) (IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v)
  {v : List ℕ}, eval step (stepRet (Cont.cons₁ fs as k) v) = Cfg.halt <$> (Cont.cons₁ fs as k).eval v
Tactic: induction k generalizing v with
  | halt =>
    simp only [Cont.eval, map_pure]
    exact Part.eq_some_iff.2 (mem_eval.2 ⟨ReflTransGen.refl, rfl⟩)
  | cons₁ fs as k IH =>
    rw [Cont.eval, stepRet, code_is_ok]
    simp only [← bind_pure_comp, bind_assoc]; congr; funext v'
    rw [reaches_eval]; swap
    · exact ReflTransGen.single rfl
    rw [stepRet, IH, bind_pure_comp]
  | cons₂ ns k IH => rw [Cont.eval, stepRet]; exact IH
  | comp f k IH =>
    rw [Cont.eval, stepRet, code_is_ok]
    simp only [← bind_pure_comp, bind_assoc]; congr; funext v'
    rw [reaches_eval]; swap
    · exact ReflTransGen.single rfl
    rw [IH, bind_pure_comp]
  | fix f k IH =>
    rw [Cont.eval, stepRet]; simp only
    split_ifs; · exact IH
    simp only [← bind_pure_comp, bind_assoc, cont_eval_fix (code_is_ok _)]
    congr; funext; rw [bind_pure_comp, ← IH]
    exact reaches_eval (ReflTransGen.single rfl)
Cleared hypotheses: k, v
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
k : Cont
v : List ℕ
halt : ∀ {v : List ℕ}, eval step (stepRet Cont.halt v) = Cfg.halt <$> Cont.halt.eval v
cons₁ :
  ∀ (fs : Code) (as : List ℕ) (k : Cont) (IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v)
    {v : List ℕ}, eval step (stepRet (Cont.cons₁ fs as k) v) = Cfg.halt <$> (Cont.cons₁ fs as k).eval v
⊢ eval step (stepRet k v) = Cfg.halt <$> k.eval v
have cons₂ : ∀ (ns : List ℕ) (k : Cont) (IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v) {v : List ℕ},
  eval step (stepRet (Cont.cons₂ ns k) v) = Cfg.halt <$> (Cont.cons₂ ns k).eval v
Tactic: induction k generalizing v with
  | halt =>
    simp only [Cont.eval, map_pure]
    exact Part.eq_some_iff.2 (mem_eval.2 ⟨ReflTransGen.refl, rfl⟩)
  | cons₁ fs as k IH =>
    rw [Cont.eval, stepRet, code_is_ok]
    simp only [← bind_pure_comp, bind_assoc]; congr; funext v'
    rw [reaches_eval]; swap
    · exact ReflTransGen.single rfl
    rw [stepRet, IH, bind_pure_comp]
  | cons₂ ns k IH => rw [Cont.eval, stepRet]; exact IH
  | comp f k IH =>
    rw [Cont.eval, stepRet, code_is_ok]
    simp only [← bind_pure_comp, bind_assoc]; congr; funext v'
    rw [reaches_eval]; swap
    · exact ReflTransGen.single rfl
    rw [IH, bind_pure_comp]
  | fix f k IH =>
    rw [Cont.eval, stepRet]; simp only
    split_ifs; · exact IH
    simp only [← bind_pure_comp, bind_assoc, cont_eval_fix (code_is_ok _)]
    congr; funext; rw [bind_pure_comp, ← IH]
    exact reaches_eval (ReflTransGen.single rfl)
Cleared hypotheses: k, v
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
k : Cont
v : List ℕ
halt : ∀ {v : List ℕ}, eval step (stepRet Cont.halt v) = Cfg.halt <$> Cont.halt.eval v
cons₁ :
  ∀ (fs : Code) (as : List ℕ) (k : Cont) (IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v)
    {v : List ℕ}, eval step (stepRet (Cont.cons₁ fs as k) v) = Cfg.halt <$> (Cont.cons₁ fs as k).eval v
cons₂ :
  ∀ (ns : List ℕ) (k : Cont) (IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v) {v : List ℕ},
    eval step (stepRet (Cont.cons₂ ns k) v) = Cfg.halt <$> (Cont.cons₂ ns k).eval v
⊢ eval step (stepRet k v) = Cfg.halt <$> k.eval v
have comp : ∀ (f : Code) (k : Cont) (IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v) {v : List ℕ},
  eval step (stepRet (Cont.comp f k) v) = Cfg.halt <$> (Cont.comp f k).eval v
Tactic: induction k generalizing v with
  | halt =>
    simp only [Cont.eval, map_pure]
    exact Part.eq_some_iff.2 (mem_eval.2 ⟨ReflTransGen.refl, rfl⟩)
  | cons₁ fs as k IH =>
    rw [Cont.eval, stepRet, code_is_ok]
    simp only [← bind_pure_comp, bind_assoc]; congr; funext v'
    rw [reaches_eval]; swap
    · exact ReflTransGen.single rfl
    rw [stepRet, IH, bind_pure_comp]
  | cons₂ ns k IH => rw [Cont.eval, stepRet]; exact IH
  | comp f k IH =>
    rw [Cont.eval, stepRet, code_is_ok]
    simp only [← bind_pure_comp, bind_assoc]; congr; funext v'
    rw [reaches_eval]; swap
    · exact ReflTransGen.single rfl
    rw [IH, bind_pure_comp]
  | fix f k IH =>
    rw [Cont.eval, stepRet]; simp only
    split_ifs; · exact IH
    simp only [← bind_pure_comp, bind_assoc, cont_eval_fix (code_is_ok _)]
    congr; funext; rw [bind_pure_comp, ← IH]
    exact reaches_eval (ReflTransGen.single rfl)
Cleared hypotheses: k, v
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
k : Cont
v : List ℕ
halt : ∀ {v : List ℕ}, eval step (stepRet Cont.halt v) = Cfg.halt <$> Cont.halt.eval v
cons₁ :
  ∀ (fs : Code) (as : List ℕ) (k : Cont) (IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v)
    {v : List ℕ}, eval step (stepRet (Cont.cons₁ fs as k) v) = Cfg.halt <$> (Cont.cons₁ fs as k).eval v
cons₂ :
  ∀ (ns : List ℕ) (k : Cont) (IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v) {v : List ℕ},
    eval step (stepRet (Cont.cons₂ ns k) v) = Cfg.halt <$> (Cont.cons₂ ns k).eval v
comp :
  ∀ (f : Code) (k : Cont) (IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v) {v : List ℕ},
    eval step (stepRet (Cont.comp f k) v) = Cfg.halt <$> (Cont.comp f k).eval v
⊢ eval step (stepRet k v) = Cfg.halt <$> k.eval v
have fix : ∀ (f : Code) (k : Cont) (IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v) {v : List ℕ},
  eval step (stepRet (Cont.fix f k) v) = Cfg.halt <$> (Cont.fix f k).eval v
Tactic: induction k generalizing v with
  | halt =>
    simp only [Cont.eval, map_pure]
    exact Part.eq_some_iff.2 (mem_eval.2 ⟨ReflTransGen.refl, rfl⟩)
  | cons₁ fs as k IH =>
    rw [Cont.eval, stepRet, code_is_ok]
    simp only [← bind_pure_comp, bind_assoc]; congr; funext v'
    rw [reaches_eval]; swap
    · exact ReflTransGen.single rfl
    rw [stepRet, IH, bind_pure_comp]
  | cons₂ ns k IH => rw [Cont.eval, stepRet]; exact IH
  | comp f k IH =>
    rw [Cont.eval, stepRet, code_is_ok]
    simp only [← bind_pure_comp, bind_assoc]; congr; funext v'
    rw [reaches_eval]; swap
    · exact ReflTransGen.single rfl
    rw [IH, bind_pure_comp]
  | fix f k IH =>
    rw [Cont.eval, stepRet]; simp only
    split_ifs; · exact IH
    simp only [← bind_pure_comp, bind_assoc, cont_eval_fix (code_is_ok _)]
    congr; funext; rw [bind_pure_comp, ← IH]
    exact reaches_eval (ReflTransGen.single rfl)
Cleared hypotheses: k, v
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
Λ : Type u_2
inst : Inhabited Λ
inst_1 : Inhabited Γ
M : Machine Γ Λ
S : Set Λ
ss : Supports M S
q : Λ
T : Tape Γ
c' : Cfg Γ Λ
h₁ : c' ∈ step M { q := q, Tape := T : Cfg Γ Λ }
h₂ : { q := q, Tape := T : Cfg Γ Λ }.q ∈ S
⊢ c'.q ∈ S
have rcases : ∀ (q' : Λ) (a : Stmt Γ) (h : M q T.head = some (q', a))
  (h₁ :
    Membership.mem (α := Cfg Γ Λ) (step M { q := q, Tape := T : Cfg Γ Λ })
      (match (motive := Prod.{u_2, u_1} Λ (Stmt Γ) → Cfg Γ Λ) (q', a) with
        | (q', a) =>
          { q := q',
            Tape :=
              match (motive := Stmt Γ → Tape Γ) a with
              | Stmt.move d => Tape.move d T
              | Stmt.write a => Tape.write a T } :
        Cfg Γ Λ)),
  Cfg.q.{u_1, u_2} (Γ := Γ)
      (match (motive := Prod.{u_2, u_1} Λ (Stmt Γ) → Cfg Γ Λ) (q', a) with
      | (q', a) =>
        { q := q',
          Tape :=
            match (motive := Stmt Γ → Tape Γ) a with
            | Stmt.move d => Tape.move d T
            | Stmt.write a => Tape.write a T }) ∈
    S
Tactic: rcases Option.map_eq_some_iff.1 h₁ with ⟨⟨q', a⟩, h, rfl⟩
Cleared hypotheses: c', h₁
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
Λ : Type u_2
inst : Inhabited Λ
M : Machine Γ Λ
⊢ Supports M Set.univ
have left : Membership.mem (γ := Set Λ) Set.univ default
Tactic: constructor
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
Λ : Type u_2
inst : Inhabited Λ
M : Machine Γ Λ
left : Membership.mem (γ := Set Λ) Set.univ default
⊢ Supports M Set.univ
have right : ∀ {q : Λ} {a : Γ} {q' : Λ} {s : Stmt Γ},
  (q', s) ∈ M q a → Membership.mem (γ := Set Λ) Set.univ q → Membership.mem (γ := Set Λ) Set.univ q'
Tactic: constructor
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
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
⊢ Eq (α := Option (Cfg Γ' Λ'))
    (Option.map
      (fun (x : Cfg Γ Λ) ↦
        match (motive := Cfg Γ Λ → Cfg Γ' Λ') x with
        | { q := q, Tape := T } => { q := g₁ q, Tape := Tape.map f₁ T })
      (match (motive := Cfg Γ Λ → Option (Cfg Γ Λ)) { q := q, Tape := T : Cfg Γ Λ } with
      | { q := q, Tape := T } =>
        Option.map
          (fun (x : Prod.{u_3, u_1} Λ (Stmt Γ)) ↦
            match (motive := Prod.{u_3, u_1} Λ (Stmt Γ) → Cfg Γ Λ) x with
            | (q', a) =>
              { q := q',
                Tape :=
                  match (motive := Stmt Γ → Tape Γ) a with
                  | Stmt.move d => Tape.move d T
                  | Stmt.write a => Tape.write a T })
          (M q T.head)))
    (match (motive := Cfg Γ' Λ' → Option (Cfg Γ' Λ'))
      match (motive := Cfg Γ Λ → Cfg Γ' Λ') { q := q, Tape := T : Cfg Γ Λ } with
      | { q := q, Tape := T } => { q := g₁ q, Tape := Tape.map f₁ T } with
    | { q := q, Tape := T } =>
      Option.map
        (fun (x : Prod.{u_4, u_2} Λ' (Stmt Γ')) ↦
          match (motive := Prod.{u_4, u_2} Λ' (Stmt Γ') → Cfg Γ' Λ') x with
          | (q', a) =>
            { q := q',
              Tape :=
                match (motive := Stmt Γ' → Tape Γ') a with
                | Stmt.move d => Tape.move d T
                | Stmt.write a => Tape.write a T })
        (match (motive := Λ' → Γ' → Option (Prod.{u_4, u_2} Λ' (Stmt Γ'))) q, T.head with
        | q, l => Option.map (Prod.map g₁ (Stmt.map f₁)) (M (g₂ q) (f₂.f l))))
have simp : 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: simp only [Turing.Tape.map_fst, g₂₁ q h, f₂₁ _]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
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
⊢ 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)))
have 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 })
      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₁)) none))
Tactic: rcases M q T.1 with (_ | ⟨q', d | a⟩)
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
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))
⊢ 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)))
have 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 })
        (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₁)) (some (q', Stmt.move d))))
Tactic: rcases M q T.1 with (_ | ⟨q', d | a⟩)
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
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
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 })
        (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₁)) (some (q', Stmt.move d))))
have some : some { q := g₁ q', Tape := Tape.move d (Tape.map f₁ T) : Cfg Γ' Λ' } =
  some
    { q := (Prod.map g₁ (Stmt.map f₁) (q', Stmt.move d)).1,
      Tape :=
        match (motive := Stmt Γ' → Tape Γ') (Prod.map g₁ (Stmt.map f₁) (q', Stmt.move d)).2 with
        | Stmt.move d => Tape.move d (Tape.map f₁ T)
        | Stmt.write a => Tape.write a (Tape.map f₁ T) }
Tactic: simp only [Option.map_some, Tape.map_move f₁]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
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
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 })
        (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₁)) (some (q', Stmt.write a))))
have some : some { q := g₁ q', Tape := Tape.write (f₁.f a) (Tape.map f₁ T) : Cfg Γ' Λ' } =
  some
    { q := (Prod.map g₁ (Stmt.map f₁) (q', Stmt.write a)).1,
      Tape :=
        match (motive := Stmt Γ' → Tape Γ') (Prod.map g₁ (Stmt.map f₁) (q', Stmt.write a)).2 with
        | Stmt.move d => Tape.move d (Tape.map f₁ T)
        | Stmt.write a => Tape.write a (Tape.map f₁ T) }
Tactic: simp only [Option.map_some, Tape.map_write]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
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₁ : PointedMap Λ Λ'
g₂ : Λ' → Λ
S : Set Λ
ss : Supports M S
f₂₁ : Function.RightInverse f₁.f f₂.f
g₂₁ : ∀ q ∈ S, g₂ (g₁.f q) = q
c : Cfg Γ Λ
a₂ : Cfg Γ' Λ'
⊢ (fun (a : Cfg Γ Λ) (b : Cfg Γ' Λ') ↦ a.q ∈ S ∧ Cfg.map f₁ g₁.f a = b) c a₂ →
    match (motive := Option (Cfg Γ Λ) → Prop) step M c with
    | some b₁ =>
      ∃ (b₂ : Cfg Γ' Λ'),
        (fun (a : Cfg Γ Λ) (b : Cfg Γ' Λ') ↦ a.q ∈ S ∧ Cfg.map f₁ g₁.f a = b) b₁ b₂ ∧
          Reaches₁ (step (M.map f₁ f₂ g₁.f g₂)) a₂ b₂
    | none => step (M.map f₁ f₂ g₁.f g₂) a₂ = none
have this : ∀ (cs : c.q ∈ S),
  match (motive := Option (Cfg Γ Λ) → Prop) step M c with
  | some b₁ =>
    ∃ (b₂ : Cfg Γ' Λ'),
      (fun (a : Cfg Γ Λ) (b : Cfg Γ' Λ') ↦ a.q ∈ S ∧ Cfg.map f₁ g₁.f a = b) b₁ b₂ ∧
        Reaches₁ (step (M.map f₁ f₂ g₁.f g₂)) (Cfg.map f₁ g₁.f c) b₂
  | none => step (M.map f₁ f₂ g₁.f g₂) (Cfg.map f₁ g₁.f c) = none
Tactic: ⟨cs, rfl⟩
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
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₁ : PointedMap Λ Λ'
g₂ : Λ' → Λ
S : Set Λ
ss : Supports M S
f₂₁ : Function.RightInverse f₁.f f₂.f
g₂₁ : ∀ q ∈ S, g₂ (g₁.f q) = q
c : Cfg Γ Λ
a₂ : Cfg Γ' Λ'
cs : c.q ∈ S
⊢ match (motive := Option (Cfg Γ Λ) → Prop) step M c with
  | some b₁ =>
    ∃ (b₂ : Cfg Γ' Λ'),
      (fun (a : Cfg Γ Λ) (b : Cfg Γ' Λ') ↦ a.q ∈ S ∧ Cfg.map f₁ g₁.f a = b) b₁ b₂ ∧
        Reaches₁ (step (M.map f₁ f₂ g₁.f g₂)) (Cfg.map f₁ g₁.f c) b₂
  | none => step (M.map f₁ f₂ g₁.f g₂) (Cfg.map f₁ g₁.f c) = none
have none : ∀ (e : step M c = none),
  match (motive := Option (Cfg Γ Λ) → Prop) none with
  | some b₁ =>
    ∃ (b₂ : Cfg Γ' Λ'),
      (fun (a : Cfg Γ Λ) (b : Cfg Γ' Λ') ↦ a.q ∈ S ∧ Cfg.map f₁ g₁.f a = b) b₁ b₂ ∧
        Reaches₁ (step (M.map f₁ f₂ g₁.f g₂)) (Cfg.map f₁ g₁.f c) b₂
  | none => step (M.map f₁ f₂ g₁.f g₂) (Cfg.map f₁ g₁.f c) = none
Tactic: cases e : step M c
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
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₁ : PointedMap Λ Λ'
g₂ : Λ' → Λ
S : Set Λ
ss : Supports M S
f₂₁ : Function.RightInverse f₁.f f₂.f
g₂₁ : ∀ q ∈ S, g₂ (g₁.f q) = q
c : Cfg Γ Λ
a₂ : Cfg Γ' Λ'
cs : c.q ∈ S
none :
  ∀ (e : step M c = Option.none),
    match (motive := Option (Cfg Γ Λ) → Prop) Option.none with
    | some b₁ =>
      ∃ (b₂ : Cfg Γ' Λ'),
        (fun (a : Cfg Γ Λ) (b : Cfg Γ' Λ') ↦ a.q ∈ S ∧ Cfg.map f₁ g₁.f a = b) b₁ b₂ ∧
          Reaches₁ (step (M.map f₁ f₂ g₁.f g₂)) (Cfg.map f₁ g₁.f c) b₂
    | Option.none => step (M.map f₁ f₂ g₁.f g₂) (Cfg.map f₁ g₁.f c) = Option.none
⊢ match (motive := Option (Cfg Γ Λ) → Prop) step M c with
  | some b₁ =>
    ∃ (b₂ : Cfg Γ' Λ'),
      (fun (a : Cfg Γ Λ) (b : Cfg Γ' Λ') ↦ a.q ∈ S ∧ Cfg.map f₁ g₁.f a = b) b₁ b₂ ∧
        Reaches₁ (step (M.map f₁ f₂ g₁.f g₂)) (Cfg.map f₁ g₁.f c) b₂
  | Option.none => step (M.map f₁ f₂ g₁.f g₂) (Cfg.map f₁ g₁.f c) = Option.none
have some : ∀ (val : Cfg Γ Λ) (e : step M c = some val),
  match (motive := Option (Cfg Γ Λ) → Prop) some val with
  | some b₁ =>
    ∃ (b₂ : Cfg Γ' Λ'),
      (fun (a : Cfg Γ Λ) (b : Cfg Γ' Λ') ↦ a.q ∈ S ∧ Cfg.map f₁ g₁.f a = b) b₁ b₂ ∧
        Reaches₁ (step (M.map f₁ f₂ g₁.f g₂)) (Cfg.map f₁ g₁.f c) b₂
  | Option.none => step (M.map f₁ f₂ g₁.f g₂) (Cfg.map f₁ g₁.f c) = Option.none
Tactic: cases e : step M c