awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
x : Cfg Γ Λ σ
f : Γ → σ → Γ
q : Stmt Γ Λ σ
IH :
  ∀ (v : σ) (L R : ListBlank Γ),
    Reaches (step (tr enc dec M)) (stepAux (trNormal dec q) v (trTape' enc0 L R))
      (trCfg enc enc0 (stepAux q v (Tape.mk' L R)))
v : σ
L : ListBlank Γ
a : Γ
R : ListBlank Γ
⊢ ReflTransGen (fun (a b : Cfg Bool (Λ' Γ Λ σ) σ) ↦ b ∈ step (tr enc dec M) a)
    (stepAux (tr enc dec M (Λ'.write (f (ListBlank.cons a R).head v) q)) v (trTape' enc0 L (ListBlank.cons a R)))
    (trCfg enc enc0
      (stepAux q v (Tape.write (f (Tape.mk' L (ListBlank.cons a R)).head v) (Tape.mk' L (ListBlank.cons a R)))))
have some : ReflTransGen (fun (a b : Cfg Bool (Λ' Γ Λ σ) σ) ↦ b ∈ step (tr enc dec M) a)
  (stepAux (trNormal dec q) v
    (trTape' enc0 (ListBlank.cons (f a v) L).tail (ListBlank.cons (ListBlank.cons (f a v) L).head R)))
  (trCfg enc enc0 (stepAux q v (Tape.write (f a v) (Tape.mk' L (ListBlank.cons a R)))))
Tactic: rw [tr, Tape.mk'_head, stepAux_write, ListBlank.head_cons, stepAux_move,
        trTape'_move_left enc0]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
x : Cfg Γ Λ σ
a : Γ → σ → σ
q : Stmt Γ Λ σ
IH :
  ∀ (v : σ) (L R : ListBlank Γ),
    Reaches (step (tr enc dec M)) (stepAux (trNormal dec q) v (trTape' enc0 L R))
      (trCfg enc enc0 (stepAux q v (Tape.mk' L R)))
v : σ
L R : ListBlank Γ
⊢ Reaches (step (tr enc dec M)) (stepAux (trNormal dec (Stmt.load a q)) v (trTape' enc0 L R))
    (trCfg enc enc0 (stepAux (Stmt.load a q) v (Tape.mk' L R)))
have some : Reaches (step (tr enc dec M))
  (stepAux (Stmt.load (fun (x : Bool) (s : σ) ↦ a R.head s) (trNormal dec q)) v (trTape' enc0 L R))
  (trCfg enc enc0 (stepAux (Stmt.load a q) v (Tape.mk' L R)))
Tactic: simp only [trNormal, stepAux_read dec enc0 encdec]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
x : Cfg Γ Λ σ
p : Γ → σ → Bool
q₁ q₂ : Stmt Γ Λ σ
IH₁ :
  ∀ (v : σ) (L R : ListBlank Γ),
    Reaches (step (tr enc dec M)) (stepAux (trNormal dec q₁) v (trTape' enc0 L R))
      (trCfg enc enc0 (stepAux q₁ v (Tape.mk' L R)))
IH₂ :
  ∀ (v : σ) (L R : ListBlank Γ),
    Reaches (step (tr enc dec M)) (stepAux (trNormal dec q₂) v (trTape' enc0 L R))
      (trCfg enc enc0 (stepAux q₂ v (Tape.mk' L R)))
v : σ
L R : ListBlank Γ
⊢ Reaches (step (tr enc dec M)) (stepAux (trNormal dec (Stmt.branch p q₁ q₂)) v (trTape' enc0 L R))
    (trCfg enc enc0 (stepAux (Stmt.branch p q₁ q₂) v (Tape.mk' L R)))
have some : Reaches (step (tr enc dec M))
  (bif p R.head v then stepAux (trNormal dec q₁) v (trTape' enc0 L R)
  else stepAux (trNormal dec q₂) v (trTape' enc0 L R))
  (trCfg enc enc0 (bif p R.head v then stepAux q₁ v (Tape.mk' L R) else stepAux q₂ v (Tape.mk' L R)))
Tactic: simp only [trNormal, stepAux_read dec enc0 encdec, stepAux, Tape.mk'_head]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
x : Cfg Γ Λ σ
l : Γ → σ → Λ
v : σ
L R : ListBlank Γ
⊢ Reaches (step (tr enc dec M)) (stepAux (trNormal dec (Stmt.goto l)) v (trTape' enc0 L R))
    (trCfg enc enc0 (stepAux (Stmt.goto l) v (Tape.mk' L R)))
have some : Reaches (step (tr enc dec M))
  { l := some (Λ'.normal (l R.head v)), var := v, Tape := trTape' enc0 L R : Cfg Bool (Λ' Γ Λ σ) σ }
  { l := Option.map Λ'.normal (some (l (Tape.mk' L R).head v)), var := v, Tape := trTape' enc0 L R }
Tactic: simp only [trNormal, stepAux_read dec enc0 encdec, stepAux, trCfg, trTape_mk']
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
x : Cfg Γ Λ σ
v : σ
L R : ListBlank Γ
⊢ Reaches (step (tr enc dec M)) (stepAux (trNormal dec Stmt.halt) v (trTape' enc0 L R))
    (trCfg enc enc0 (stepAux Stmt.halt v (Tape.mk' L R)))
have some : Reaches (step (tr enc dec M)) { l := none, var := v, Tape := trTape' enc0 L R : Cfg Bool (Λ' Γ Λ σ) σ }
  { l := Option.map Λ'.normal none, var := v, Tape := trTape' enc0 L R }
Tactic: simp only [trNormal, stepAux, trCfg,
        trTape_mk']
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
x : Cfg Γ Λ σ
v : σ
L : ListBlank Γ
q : Stmt Γ Λ σ
R : ListBlank Γ
⊢ Reaches (step (tr enc dec M)) (stepAux (trNormal dec q) v (trTape' enc0 L R))
    (trCfg enc enc0 (stepAux q v (Tape.mk' L R)))
have some : ∀ (d : Dir) (q : Stmt Γ Λ σ)
  (IH :
    ∀ (v : σ) (L R : ListBlank Γ),
      Reaches (step (tr enc dec M)) (stepAux (trNormal dec q) v (trTape' enc0 L R))
        (trCfg enc enc0 (stepAux q v (Tape.mk' L R))))
  (v : σ) (L R : ListBlank Γ),
  Reaches (step (tr enc dec M)) (stepAux (trNormal dec (Stmt.move d q)) v (trTape' enc0 L R))
    (trCfg enc enc0 (stepAux (Stmt.move d q) v (Tape.mk' L R)))
Tactic: induction q generalizing v L R with
    | move d q IH =>
      cases d <;>
          simp only [trNormal, stepAux_move, stepAux,
            Tape.move_left_mk',
            trTape'_move_left enc0, trTape'_move_right enc0] <;>
        apply IH
    | write f q IH =>
      simp only [trNormal, stepAux_read dec enc0 encdec, stepAux]
      refine ReflTransGen.head rfl ?_
      obtain ⟨a, R, rfl⟩ := R.exists_cons
      rw [tr, Tape.mk'_head, stepAux_write, ListBlank.head_cons, stepAux_move,
        trTape'_move_left enc0]
      simpa using IH ..
    | load a q IH =>
      simp only [trNormal, stepAux_read dec enc0 encdec]
      apply IH
    | branch p q₁ q₂ IH₁ IH₂ =>
      simp only [trNormal, stepAux_read dec enc0 encdec, stepAux, Tape.mk'_head]
      grind
    | goto l =>
      simp only [trNormal, stepAux_read dec enc0 encdec, stepAux, trCfg, trTape_mk']
      apply ReflTransGen.refl
    | halt =>
      simp only [trNormal, stepAux, trCfg,
        trTape_mk']
      apply ReflTransGen.refl
Cleared hypotheses: v, L, q, R
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
x : Cfg Γ Λ σ
v : σ
L : ListBlank Γ
q : Stmt Γ Λ σ
R : ListBlank Γ
some :
  ∀ (d : Dir) (q : Stmt Γ Λ σ)
    (IH :
      ∀ (v : σ) (L R : ListBlank Γ),
        Reaches (step (tr enc dec M)) (stepAux (trNormal dec q) v (trTape' enc0 L R))
          (trCfg enc enc0 (stepAux q v (Tape.mk' L R))))
    (v : σ) (L R : ListBlank Γ),
    Reaches (step (tr enc dec M)) (stepAux (trNormal dec (Stmt.move d q)) v (trTape' enc0 L R))
      (trCfg enc enc0 (stepAux (Stmt.move d q) v (Tape.mk' L R)))
⊢ Reaches (step (tr enc dec M)) (stepAux (trNormal dec q) v (trTape' enc0 L R))
    (trCfg enc enc0 (stepAux q v (Tape.mk' L R)))
have some₁ : ∀ (f : Γ → σ → Γ) (q : Stmt Γ Λ σ)
  (IH :
    ∀ (v : σ) (L R : ListBlank Γ),
      Reaches (step (tr enc dec M)) (stepAux (trNormal dec q) v (trTape' enc0 L R))
        (trCfg enc enc0 (stepAux q v (Tape.mk' L R))))
  (v : σ) (L R : ListBlank Γ),
  Reaches (step (tr enc dec M)) (stepAux (trNormal dec (Stmt.write f q)) v (trTape' enc0 L R))
    (trCfg enc enc0 (stepAux (Stmt.write f q) v (Tape.mk' L R)))
Tactic: induction q generalizing v L R with
    | move d q IH =>
      cases d <;>
          simp only [trNormal, stepAux_move, stepAux,
            Tape.move_left_mk',
            trTape'_move_left enc0, trTape'_move_right enc0] <;>
        apply IH
    | write f q IH =>
      simp only [trNormal, stepAux_read dec enc0 encdec, stepAux]
      refine ReflTransGen.head rfl ?_
      obtain ⟨a, R, rfl⟩ := R.exists_cons
      rw [tr, Tape.mk'_head, stepAux_write, ListBlank.head_cons, stepAux_move,
        trTape'_move_left enc0]
      simpa using IH ..
    | load a q IH =>
      simp only [trNormal, stepAux_read dec enc0 encdec]
      apply IH
    | branch p q₁ q₂ IH₁ IH₂ =>
      simp only [trNormal, stepAux_read dec enc0 encdec, stepAux, Tape.mk'_head]
      grind
    | goto l =>
      simp only [trNormal, stepAux_read dec enc0 encdec, stepAux, trCfg, trTape_mk']
      apply ReflTransGen.refl
    | halt =>
      simp only [trNormal, stepAux, trCfg,
        trTape_mk']
      apply ReflTransGen.refl
Cleared hypotheses: v, L, q, R
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
x : Cfg Γ Λ σ
v : σ
L : ListBlank Γ
q : Stmt Γ Λ σ
R : ListBlank Γ
some :
  ∀ (d : Dir) (q : Stmt Γ Λ σ)
    (IH :
      ∀ (v : σ) (L R : ListBlank Γ),
        Reaches (step (tr enc dec M)) (stepAux (trNormal dec q) v (trTape' enc0 L R))
          (trCfg enc enc0 (stepAux q v (Tape.mk' L R))))
    (v : σ) (L R : ListBlank Γ),
    Reaches (step (tr enc dec M)) (stepAux (trNormal dec (Stmt.move d q)) v (trTape' enc0 L R))
      (trCfg enc enc0 (stepAux (Stmt.move d q) v (Tape.mk' L R)))
some₁ :
  ∀ (f : Γ → σ → Γ) (q : Stmt Γ Λ σ)
    (IH :
      ∀ (v : σ) (L R : ListBlank Γ),
        Reaches (step (tr enc dec M)) (stepAux (trNormal dec q) v (trTape' enc0 L R))
          (trCfg enc enc0 (stepAux q v (Tape.mk' L R))))
    (v : σ) (L R : ListBlank Γ),
    Reaches (step (tr enc dec M)) (stepAux (trNormal dec (Stmt.write f q)) v (trTape' enc0 L R))
      (trCfg enc enc0 (stepAux (Stmt.write f q) v (Tape.mk' L R)))
⊢ Reaches (step (tr enc dec M)) (stepAux (trNormal dec q) v (trTape' enc0 L R))
    (trCfg enc enc0 (stepAux q v (Tape.mk' L R)))
have some₂ : ∀ (a : Γ → σ → σ) (q : Stmt Γ Λ σ)
  (IH :
    ∀ (v : σ) (L R : ListBlank Γ),
      Reaches (step (tr enc dec M)) (stepAux (trNormal dec q) v (trTape' enc0 L R))
        (trCfg enc enc0 (stepAux q v (Tape.mk' L R))))
  (v : σ) (L R : ListBlank Γ),
  Reaches (step (tr enc dec M)) (stepAux (trNormal dec (Stmt.load a q)) v (trTape' enc0 L R))
    (trCfg enc enc0 (stepAux (Stmt.load a q) v (Tape.mk' L R)))
Tactic: induction q generalizing v L R with
    | move d q IH =>
      cases d <;>
          simp only [trNormal, stepAux_move, stepAux,
            Tape.move_left_mk',
            trTape'_move_left enc0, trTape'_move_right enc0] <;>
        apply IH
    | write f q IH =>
      simp only [trNormal, stepAux_read dec enc0 encdec, stepAux]
      refine ReflTransGen.head rfl ?_
      obtain ⟨a, R, rfl⟩ := R.exists_cons
      rw [tr, Tape.mk'_head, stepAux_write, ListBlank.head_cons, stepAux_move,
        trTape'_move_left enc0]
      simpa using IH ..
    | load a q IH =>
      simp only [trNormal, stepAux_read dec enc0 encdec]
      apply IH
    | branch p q₁ q₂ IH₁ IH₂ =>
      simp only [trNormal, stepAux_read dec enc0 encdec, stepAux, Tape.mk'_head]
      grind
    | goto l =>
      simp only [trNormal, stepAux_read dec enc0 encdec, stepAux, trCfg, trTape_mk']
      apply ReflTransGen.refl
    | halt =>
      simp only [trNormal, stepAux, trCfg,
        trTape_mk']
      apply ReflTransGen.refl
Cleared hypotheses: v, L, q, R
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst : Fintype Γ
inst_1 : Inhabited Λ
S : Finset Λ
ss : Supports M S
q : Λ' Γ Λ σ
h : q ∈ trSupp M S
this :
  ∀ (q : Stmt Γ Λ σ),
    SupportsStmt S q →
      (∀ q' ∈ writes q, q' ∈ trSupp M S) →
        SupportsStmt (trSupp M S) (trNormal dec q) ∧ ∀ q' ∈ writes q, SupportsStmt (trSupp M S) (tr enc dec M q')
⊢ SupportsStmt (trSupp M S) (tr enc dec M q)
have rcases : ∀ (l : Λ) (hl : l ∈ S) (h : q ∈ insert (Λ'.normal l) (writes (M l))), SupportsStmt (trSupp M S) (tr enc dec M q)
Tactic: rcases Finset.mem_biUnion.1 h with ⟨l, hl, h⟩
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (hypothesis)
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst : Fintype Γ
inst_1 : Inhabited Λ
S : Finset Λ
ss : Supports M S
q : Λ' Γ Λ σ
h_1 : q ∈ trSupp M S
this :
  ∀ (q : Stmt Γ Λ σ),
    SupportsStmt S q →
      (∀ q' ∈ writes q, q' ∈ trSupp M S) →
        SupportsStmt (trSupp M S) (trNormal dec q) ∧ ∀ q' ∈ writes q, SupportsStmt (trSupp M S) (tr enc dec M q')
l : Λ
hl : l ∈ S
h : q ∈ insert (Λ'.normal l) (writes (M l))
⊢ SupportsStmt (trSupp M S) (tr enc dec M q)
have this₁ : SupportsStmt (trSupp M S) (trNormal dec (M l)) ∧ ∀ q' ∈ writes (M l), SupportsStmt (trSupp M S) (tr enc dec M q')
Tactic: have :=
        this _ (ss.2 _ hl) fun q' hq ↦ Finset.mem_biUnion.2 ⟨_, hl, Finset.mem_insert_of_mem hq⟩
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst : Fintype Γ
inst_1 : Inhabited Λ
S : Finset Λ
ss : Supports M S
q : Λ' Γ Λ σ
h_1 : q ∈ trSupp M S
this_1 :
  ∀ (q : Stmt Γ Λ σ),
    SupportsStmt S q →
      (∀ q' ∈ writes q, q' ∈ trSupp M S) →
        SupportsStmt (trSupp M S) (trNormal dec q) ∧ ∀ q' ∈ writes q, SupportsStmt (trSupp M S) (tr enc dec M q')
l : Λ
hl : l ∈ S
h : q ∈ insert (Λ'.normal l) (writes (M l))
this : SupportsStmt (trSupp M S) (trNormal dec (M l)) ∧ ∀ q' ∈ writes (M l), SupportsStmt (trSupp M S) (tr enc dec M q')
⊢ SupportsStmt (trSupp M S) (tr enc dec M q)
have inl : ∀ (h : Λ'.normal l ∈ trSupp M S) (h : Λ'.normal l ∈ insert (Λ'.normal l) (writes (M l))),
  SupportsStmt (trSupp M S) (tr enc dec M (Λ'.normal l))
Tactic: rcases Finset.mem_insert.1 h with (rfl | h)
Cleared hypotheses: q, h_1, h
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst : Fintype Γ
inst_1 : Inhabited Λ
S : Finset Λ
ss : Supports M S
q : Λ' Γ Λ σ
h_1 : q ∈ trSupp M S
this_1 :
  ∀ (q : Stmt Γ Λ σ),
    SupportsStmt S q →
      (∀ q' ∈ writes q, q' ∈ trSupp M S) →
        SupportsStmt (trSupp M S) (trNormal dec q) ∧ ∀ q' ∈ writes q, SupportsStmt (trSupp M S) (tr enc dec M q')
l : Λ
hl : l ∈ S
h : q ∈ insert (Λ'.normal l) (writes (M l))
this : SupportsStmt (trSupp M S) (trNormal dec (M l)) ∧ ∀ q' ∈ writes (M l), SupportsStmt (trSupp M S) (tr enc dec M q')
inl :
  ∀ (h : Λ'.normal l ∈ trSupp M S) (h : Λ'.normal l ∈ insert (Λ'.normal l) (writes (M l))),
    SupportsStmt (trSupp M S) (tr enc dec M (Λ'.normal l))
⊢ SupportsStmt (trSupp M S) (tr enc dec M q)
have inr : ∀ (h : q ∈ writes (M l)), SupportsStmt (trSupp M S) (tr enc dec M q)
Tactic: rcases Finset.mem_insert.1 h with (rfl | h)
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst : Fintype Γ
inst_1 : Inhabited Λ
S : Finset Λ
ss : Supports M S
q : Λ' Γ Λ σ
h : q ∈ trSupp M S
⊢ SupportsStmt (trSupp M S) (tr enc dec M q)
have suffices : ∀ (q : Stmt Γ Λ σ),
  SupportsStmt S q →
    (∀ q' ∈ writes q, q' ∈ trSupp M S) →
      SupportsStmt (trSupp M S) (trNormal dec q) ∧ ∀ q' ∈ writes q, SupportsStmt (trSupp M S) (tr enc dec M q')
Tactic: suffices ∀ q, SupportsStmt S q → (∀ q' ∈ writes q, q' ∈ trSupp M S) →
        SupportsStmt (trSupp M S) (trNormal dec q) ∧
        ∀ q' ∈ writes q, SupportsStmt (trSupp M S) (tr enc dec M q') by
      rcases Finset.mem_biUnion.1 h with ⟨l, hl, h⟩
      have :=
        this _ (ss.2 _ hl) fun q' hq ↦ Finset.mem_biUnion.2 ⟨_, hl, Finset.mem_insert_of_mem hq⟩
      rcases Finset.mem_insert.1 h with (rfl | h)
      exacts [this.1, this.2 _ h]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst : Fintype Γ
inst_1 : Inhabited Λ
S : Finset Λ
ss : Supports M S
q_1 : Λ' Γ Λ σ
h : q_1 ∈ trSupp M S
d : Dir
q : Stmt Γ Λ σ
IH :
  ∀ (hs : SupportsStmt S q) (hw : ∀ q' ∈ writes q, q' ∈ trSupp M S),
    SupportsStmt (trSupp M S) (trNormal dec q) ∧ ∀ q' ∈ writes q, SupportsStmt (trSupp M S) (tr enc dec M q')
hs : SupportsStmt S (Stmt.move d q)
hw : ∀ q' ∈ writes (Stmt.move d q), q' ∈ trSupp M S
⊢ SupportsStmt (trSupp M S) (trNormal dec (Stmt.move d q)) ∧
    ∀ q' ∈ writes (Stmt.move d q), SupportsStmt (trSupp M S) (tr enc dec M q')
have move : ∀ (hw : ∀ q' ∈ writes q, q' ∈ trSupp M S),
  SupportsStmt (trSupp M S) (trNormal dec (Stmt.move d q)) ∧
    ∀ q' ∈ writes q, SupportsStmt (trSupp M S) (tr enc dec M q')
Tactic: unfold writes at hw ⊢
Cleared hypotheses: hw
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (hypothesis)
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst : Fintype Γ
inst_1 : Inhabited Λ
S : Finset Λ
ss : Supports M S
q_1 : Λ' Γ Λ σ
h : q_1 ∈ trSupp M S
d : Dir
q : Stmt Γ Λ σ
IH :
  ∀ (hs : SupportsStmt S q) (hw : ∀ q' ∈ writes q, q' ∈ trSupp M S),
    SupportsStmt (trSupp M S) (trNormal dec q) ∧ ∀ q' ∈ writes q, SupportsStmt (trSupp M S) (tr enc dec M q')
hs : SupportsStmt S (Stmt.move d q)
hw : ∀ q' ∈ writes q, q' ∈ trSupp M S
⊢ SupportsStmt (trSupp M S) (trNormal dec (Stmt.move d q)) ∧
    ∀ q' ∈ writes q, SupportsStmt (trSupp M S) (tr enc dec M q')
have IH₁ : SupportsStmt (trSupp M S) (trNormal dec q) ∧ ∀ q' ∈ writes q, SupportsStmt (trSupp M S) (tr enc dec M q')
Tactic: replace IH := IH hs hw
Cleared hypotheses: IH
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst : Fintype Γ
inst_1 : Inhabited Λ
S : Finset Λ
ss : Supports M S
q_1 : Λ' Γ Λ σ
h : q_1 ∈ trSupp M S
d : Dir
q : Stmt Γ Λ σ
hs : SupportsStmt S (Stmt.move d q)
hw : ∀ q' ∈ writes q, q' ∈ trSupp M S
IH : SupportsStmt (trSupp M S) (trNormal dec q) ∧ ∀ q' ∈ writes q, SupportsStmt (trSupp M S) (tr enc dec M q')
⊢ SupportsStmt (trSupp M S) (trNormal dec (Stmt.move d q)) ∧
    ∀ q' ∈ writes q, SupportsStmt (trSupp M S) (tr enc dec M q')
have move : SupportsStmt (trSupp M S) (trNormal dec (Stmt.move d q))
Tactic: refine ⟨?_, IH.2⟩
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst : Fintype Γ
inst_1 : Inhabited Λ
S : Finset Λ
ss : Supports M S
q_1 : Λ' Γ Λ σ
h : q_1 ∈ trSupp M S
d : Dir
q : Stmt Γ Λ σ
hs : SupportsStmt S (Stmt.move d q)
hw : ∀ q' ∈ writes q, q' ∈ trSupp M S
IH : SupportsStmt (trSupp M S) (trNormal dec q) ∧ ∀ q' ∈ writes q, SupportsStmt (trSupp M S) (tr enc dec M q')
⊢ SupportsStmt (trSupp M S) (trNormal dec (Stmt.move d q))
have move : ∀ (hs : SupportsStmt S (Stmt.move Dir.left q)), SupportsStmt (trSupp M S) (trNormal dec (Stmt.move Dir.left q))
Tactic: cases d
Cleared hypotheses: d, hs
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst : Fintype Γ
inst_1 : Inhabited Λ
S : Finset Λ
ss : Supports M S
q_1 : Λ' Γ Λ σ
h : q_1 ∈ trSupp M S
d : Dir
q : Stmt Γ Λ σ
hs : SupportsStmt S (Stmt.move d q)
hw : ∀ q' ∈ writes q, q' ∈ trSupp M S
IH : SupportsStmt (trSupp M S) (trNormal dec q) ∧ ∀ q' ∈ writes q, SupportsStmt (trSupp M S) (tr enc dec M q')
move : ∀ (hs : SupportsStmt S (Stmt.move Dir.left q)), SupportsStmt (trSupp M S) (trNormal dec (Stmt.move Dir.left q))
⊢ SupportsStmt (trSupp M S) (trNormal dec (Stmt.move d q))
have move₁ : ∀ (hs : SupportsStmt S (Stmt.move Dir.right q)), SupportsStmt (trSupp M S) (trNormal dec (Stmt.move Dir.right q))
Tactic: cases d
Cleared hypotheses: d, hs
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (hypothesis)
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst : Fintype Γ
inst_1 : Inhabited Λ
S : Finset Λ
ss : Supports M S
q_1 : Λ' Γ Λ σ
h : q_1 ∈ trSupp M S
f : Γ → σ → Γ
q : Stmt Γ Λ σ
IH :
  ∀ (hs : SupportsStmt S q) (hw : ∀ q' ∈ writes q, q' ∈ trSupp M S),
    SupportsStmt (trSupp M S) (trNormal dec q) ∧ ∀ q' ∈ writes q, SupportsStmt (trSupp M S) (tr enc dec M q')
hs : SupportsStmt S (Stmt.write f q)
hw : ∀ q' ∈ writes (Stmt.write f q), q' ∈ trSupp M S
⊢ SupportsStmt (trSupp M S) (trNormal dec (Stmt.write f q)) ∧
    ∀ q' ∈ writes (Stmt.write f q), SupportsStmt (trSupp M S) (tr enc dec M q')
have hw₁ : ∀ q' ∈ Finset.image (fun (a : Γ) ↦ Λ'.write a q) Finset.univ ∪ writes q, q' ∈ trSupp M S
Tactic: unfold writes at hw ⊢
Cleared hypotheses: hw
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst : Fintype Γ
inst_1 : Inhabited Λ
S : Finset Λ
ss : Supports M S
q_1 : Λ' Γ Λ σ
h : q_1 ∈ trSupp M S
f : Γ → σ → Γ
q : Stmt Γ Λ σ
IH :
  ∀ (hs : SupportsStmt S q) (hw : ∀ q' ∈ writes q, q' ∈ trSupp M S),
    SupportsStmt (trSupp M S) (trNormal dec q) ∧ ∀ q' ∈ writes q, SupportsStmt (trSupp M S) (tr enc dec M q')
hs : SupportsStmt S (Stmt.write f q)
hw : ∀ q' ∈ Finset.image (fun (a : Γ) ↦ Λ'.write a q) Finset.univ ∪ writes q, q' ∈ trSupp M S
⊢ SupportsStmt (trSupp M S) (trNormal dec (Stmt.write f q)) ∧
    ∀ q' ∈ Finset.image (fun (a : Γ) ↦ Λ'.write a q) Finset.univ ∪ writes q, SupportsStmt (trSupp M S) (tr enc dec M q')
have write : ∀ (hw : ∀ (q' : Λ' Γ Λ σ), (∃ (a : Γ), Λ'.write a q = q') ∨ q' ∈ writes q → q' ∈ trSupp M S),
  SupportsStmt (trSupp M S) (trNormal dec (Stmt.write f q)) ∧
    ∀ (q' : Λ' Γ Λ σ), (∃ (a : Γ), Λ'.write a q = q') ∨ q' ∈ writes q → SupportsStmt (trSupp M S) (tr enc dec M q')
Tactic: simp only [Finset.mem_image, Finset.mem_union, Finset.mem_univ, true_and]
        at hw ⊢
Cleared hypotheses: hw