awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
f : Code
k : Cont
IH :
  ∀ (v : List ℕ) (s : Option Γ'),
    ∃ (b₂ : Cfg'),
      TrCfg (stepRet k v) b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.ret (trCont k))) s (elim (trList v) [] [] (trContStack k))) b₂
v : List ℕ
s : Option Γ'
h : ¬v.headI = 0
this :
  natEnd ((trList v).head?.getD default) = false ∧ (trList v).tail = (trNat v.headI).tail ++ Γ'.cons :: trList v.tail
s' : Cfg'
h₁ : TrCfg (stepNormal f (Cont.fix f k) v.tail) s'
h₂ :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont (Cont.fix f k)))) (some Γ'.cons)
      (elim (trList v.tail) [] [] (trContStack (Cont.fix f k))))
    s'
⊢ elim (trList v.tail) [] [] (trContStack (Cont.fix f k)) = elim (trList v.tail) [] [] (trContStack (Cont.fix f k))

Tactic:
convert! rfl

Premises used: rfl
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
f : Code
k : Cont
IH :
  ∀ (v : List ℕ) (s : Option Γ'),
    ∃ (b₂ : Cfg'),
      TrCfg (stepRet k v) b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.ret (trCont k))) s (elim (trList v) [] [] (trContStack k))) b₂
v : List ℕ
s : Option Γ'
h : ¬v.headI = 0
this :
  natEnd ((trList v).head?.getD default) = false ∧ (trList v).tail = (trNat v.headI).tail ++ Γ'.cons :: trList v.tail
s' : Cfg'
h₁ : TrCfg (stepNormal f (Cont.fix f k) v.tail) s'
h₂ :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont (Cont.fix f k)))) (some Γ'.cons)
      (elim (trList v.tail) [] [] (trContStack (Cont.fix f k))))
    s'
⊢ ∀ x ∈ (trNat v.headI).tail, natEnd x = false

Tactic:
fun x h => trNat_natEnd _ _ (List.tail_subset _ h)

Premises used: List.headI, Turing.PartrecToTM2.trNat, List.tail_subset, Turing.PartrecToTM2.trNat_natEnd
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
f : Code
k : Cont
IH :
  ∀ (v : List ℕ) (s : Option Γ'),
    ∃ (b₂ : Cfg'),
      TrCfg (stepRet k v) b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.ret (trCont k))) s (elim (trList v) [] [] (trContStack k))) b₂
v : List ℕ
s : Option Γ'
h : ¬v.headI = 0
this :
  natEnd ((trList v).head?.getD default) = false ∧ (trList v).tail = (trNat v.headI).tail ++ Γ'.cons :: trList v.tail
s' : Cfg'
h₁ : TrCfg (stepNormal f (Cont.fix f k) v.tail) s'
h₂ :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont (Cont.fix f k)))) (some Γ'.cons)
      (elim (trList v.tail) [] [] (trContStack (Cont.fix f k))))
    s'
⊢ ∀ x ∈ (trNat v.headI).tail, natEnd x = false

Tactic:
exact fun x h => trNat_natEnd _ _ (List.tail_subset _ h)

Premises used: Turing.PartrecToTM2.trNat, List.tail_subset, Turing.PartrecToTM2.trNat_natEnd
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
f : Code
k : Cont
IH :
  ∀ (v : List ℕ) (s : Option Γ'),
    ∃ (b₂ : Cfg'),
      TrCfg (stepRet k v) b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.ret (trCont k))) s (elim (trList v) [] [] (trContStack k))) b₂
v : List ℕ
s : Option Γ'
h : ¬v.headI = 0
this :
  natEnd ((trList v).head?.getD default) = false ∧ (trList v).tail = (trNat v.headI).tail ++ Γ'.cons :: trList v.tail
s' : Cfg'
h₁ : TrCfg (stepNormal f (Cont.fix f k) v.tail) s'
h₂ :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont (Cont.fix f k)))) (some Γ'.cons)
      (elim (trList v.tail) [] [] (trContStack (Cont.fix f k))))
    s'
⊢ Option.elim'
    (update (β := fun (k : K') ↦ List Γ') (elim (trList v) [] [] (trContStack (Cont.fix f k))) main (trList v).tail
          main =
        (trNat v.headI).tail ∧
      trList v.tail = [])
    (fun (a : Γ') ↦
      natEnd a = true ∧
        update (β := fun (k : K') ↦ List Γ') (elim (trList v) [] [] (trContStack (Cont.fix f k))) main (trList v).tail
            main =
          (trNat v.headI).tail ++ a :: trList v.tail)
    (some Γ'.cons)

Tactic:
⟨rfl, this.2⟩

Premises used: Option.elim', And.right, And.intro, rfl
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
f : Code
k : Cont
IH :
  ∀ (v : List ℕ) (s : Option Γ'),
    ∃ (b₂ : Cfg'),
      TrCfg (stepRet k v) b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.ret (trCont k))) s (elim (trList v) [] [] (trContStack k))) b₂
v : List ℕ
s : Option Γ'
h : ¬v.headI = 0
this :
  natEnd ((trList v).head?.getD default) = false ∧ (trList v).tail = (trNat v.headI).tail ++ Γ'.cons :: trList v.tail
s' : Cfg'
h₁ : TrCfg (stepNormal f (Cont.fix f k) v.tail) s'
h₂ :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont (Cont.fix f k)))) (some Γ'.cons)
      (elim (trList v.tail) [] [] (trContStack (Cont.fix f k))))
    s'
⊢ Option.elim'
    (update (β := fun (k : K') ↦ List Γ') (elim (trList v) [] [] (trContStack (Cont.fix f k))) main (trList v).tail
          main =
        (trNat v.headI).tail ∧
      trList v.tail = [])
    (fun (a : Γ') ↦
      natEnd a = true ∧
        update (β := fun (k : K') ↦ List Γ') (elim (trList v) [] [] (trContStack (Cont.fix f k))) main (trList v).tail
            main =
          (trNat v.headI).tail ++ a :: trList v.tail)
    (some Γ'.cons)

Tactic:
exact ⟨rfl, this.2⟩
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
c : Code
v : List ℕ
⊢ ∃ (b : Cfg'), TrCfg (stepNormal c Cont.halt v) b ∧ Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr) (init c v) b

Tactic:
trNormal_respects _ _ _ _

Premises used: Turing.PartrecToTM2.trContStack, Turing.PartrecToTM2.trLList, Turing.PartrecToTM2.trNormal_respects, Turing.PartrecToTM2.init, Turing.PartrecToTM2.trCont
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
c : Code
v : List ℕ
obtain :
  ∀ (i : Cfg') (h₁ : TrCfg (stepNormal c Cont.halt v) i)
    (h₂ : Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr) (init c v) i),
    eval (TM2.step (Γ := fun (x : K') ↦ Γ') tr) (init c v) = halt <$> c.eval v
⊢ eval (TM2.step (Γ := fun (x : K') ↦ Γ') tr) (init c v) = halt <$> c.eval v

Tactic:
obtain ⟨i, h₁, h₂⟩ := tr_init c v

Premises used: Turing.PartrecToTM2.tr_init
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
c : Code
v : List ℕ
i : Cfg'
h₁ : TrCfg (stepNormal c Cont.halt v) i
h₂ : Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr) (init c v) i
⊢ eval (TM2.step (Γ := fun (x : K') ↦ Γ') tr) (init c v) = halt <$> c.eval v

Tactic:
Part.ext fun x => ?_

Premises used: Part.ext
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
c : Code
v : List ℕ
i : Cfg'
h₁ : TrCfg (stepNormal c Cont.halt v) i
h₂ : Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr) (init c v) i
refine :
  ∀ (x : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')),
    x ∈ eval (TM2.step (Γ := fun (x : K') ↦ Γ') tr) (init c v) ↔ x ∈ halt <$> c.eval v
⊢ eval (TM2.step (Γ := fun (x : K') ↦ Γ') tr) (init c v) = halt <$> c.eval v

Tactic:
refine Part.ext fun x => ?_

Premises used: Part.ext
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
c : Code
v : List ℕ
i : Cfg'
h₁ : TrCfg (stepNormal c Cont.halt v) i
h₂ : Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr) (init c v) i
x : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')
rw : x ∈ eval (TM2.step (Γ := fun (x : K') ↦ Γ') tr) i ↔ x ∈ halt <$> c.eval v
⊢ x ∈ eval (TM2.step (Γ := fun (x : K') ↦ Γ') tr) (init c v) ↔ x ∈ halt <$> c.eval v

Tactic:
rw [reaches_eval h₂.to_reflTransGen]

Premises used: StateTransition.reaches_eval, Relation.TransGen.to_reflTransGen
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
c : Code
v : List ℕ
i : Cfg'
h₁ : TrCfg (stepNormal c Cont.halt v) i
h₂ : Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr) (init c v) i
x : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')
simp : x ∈ eval (TM2.step (Γ := fun (x : K') ↦ Γ') tr) i ↔ ∃ a ∈ c.eval v, halt a = x
⊢ x ∈ eval (TM2.step (Γ := fun (x : K') ↦ Γ') tr) i ↔ x ∈ halt <$> c.eval v

Tactic:
simp only [Part.map_eq_map, Part.mem_map_iff]

Premises used: Part.map_eq_map, Part.mem_map_iff
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
c : Code
v : List ℕ
i : Cfg'
h₁ : TrCfg (stepNormal c Cont.halt v) i
h₂ : Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr) (init c v) i
x : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')
⊢ x ∈ eval (TM2.step (Γ := fun (x : K') ↦ Γ') tr) i ↔ ∃ a ∈ c.eval v, halt a = x

Tactic:
⟨fun h => ?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
c : Code
v : List ℕ
i : Cfg'
h₁ : TrCfg (stepNormal c Cont.halt v) i
h₂ : Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr) (init c v) i
x : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')
refine_1 : ∀ (h : x ∈ eval (TM2.step (Γ := fun (x : K') ↦ Γ') tr) i), ∃ a ∈ c.eval v, halt a = x
refine_2 : (∃ a ∈ c.eval v, halt a = x) → x ∈ eval (TM2.step (Γ := fun (x : K') ↦ Γ') tr) i
⊢ x ∈ eval (TM2.step (Γ := fun (x : K') ↦ Γ') tr) i ↔ ∃ a ∈ c.eval v, halt a = x

Tactic:
refine ⟨fun h => ?_, ?_⟩
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
c : Code
v : List ℕ
i : Cfg'
h₁ : TrCfg (stepNormal c Cont.halt v) i
h₂ : Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr) (init c v) i
x : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')
h : x ∈ eval (TM2.step (Γ := fun (x : K') ↦ Γ') tr) i
refine_1 :
  ∀ (c_1 : Cfg) (hc₁ : TrCfg c_1 x) (hc₂ : c_1 ∈ eval step (stepNormal c Cont.halt v)), ∃ a ∈ c.eval v, halt a = x
⊢ ∃ a ∈ c.eval v, halt a = x

Tactic:
obtain ⟨c, hc₁, hc₂⟩ := tr_eval_rev tr_respects h₁ h

Premises used: Turing.PartrecToTM2.tr_respects, StateTransition.tr_eval_rev
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
c_1 : Code
v : List ℕ
i : Cfg'
h₁ : TrCfg (stepNormal c_1 Cont.halt v) i
h₂ : Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr) (init c_1 v) i
x : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')
h : x ∈ eval (TM2.step (Γ := fun (x : K') ↦ Γ') tr) i
c : Cfg
hc₁ : TrCfg c x
hc₂ : c ∈ eval step (stepNormal c_1 Cont.halt v)
⊢ ∃ a ∈ c_1.eval v, Cfg.halt a = c

Tactic:
simp only [stepNormal_eval, Part.map_eq_map, Part.mem_map_iff] at hc₂

Premises used: Turing.ToPartrec.stepNormal_eval, Part.map_eq_map, Part.mem_map_iff
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
c_1 : Code
v : List ℕ
i : Cfg'
h₁ : TrCfg (stepNormal c_1 Cont.halt v) i
h₂ : Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr) (init c_1 v) i
x : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')
h : x ∈ eval (TM2.step (Γ := fun (x : K') ↦ Γ') tr) i
c : Cfg
hc₁ : TrCfg c x
hc₂ : ∃ a ∈ c_1.eval v, Cfg.halt a = c
refine_1 : ∀ (v' : List ℕ) (hv : v' ∈ c_1.eval v) (hc₁ : TrCfg (Cfg.halt v') x), ∃ a ∈ c_1.eval v, halt a = x
⊢ ∃ a ∈ c_1.eval v, halt a = x

Tactic:
obtain ⟨v', hv, rfl⟩ := hc₂

Premises used: rfl
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
c : Code
v : List ℕ
i : Cfg'
h₁ : TrCfg (stepNormal c Cont.halt v) i
h₂ : Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr) (init c v) i
x : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')
h : x ∈ eval (TM2.step (Γ := fun (x : K') ↦ Γ') tr) i
v' : List ℕ
hv : v' ∈ c.eval v
hc₁ : TrCfg (Cfg.halt v') x
⊢ ∃ a ∈ c.eval v, halt a = x

Tactic:
⟨_, hv, hc₁.symm⟩

Premises used: And.intro, Exists.intro, Eq.symm
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
c : Code
v : List ℕ
i : Cfg'
h₁ : TrCfg (stepNormal c Cont.halt v) i
h₂ : Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr) (init c v) i
x : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')
h : x ∈ eval (TM2.step (Γ := fun (x : K') ↦ Γ') tr) i
v' : List ℕ
hv : v' ∈ c.eval v
hc₁ : TrCfg (Cfg.halt v') x
⊢ ∃ a ∈ c.eval v, halt a = x

Tactic:
exact ⟨_, hv, hc₁.symm⟩
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
c : Code
v : List ℕ
i : Cfg'
h₁ : TrCfg (stepNormal c Cont.halt v) i
h₂ : Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr) (init c v) i
v' : List ℕ
hv : v' ∈ c.eval v
⊢ ∀ (ab : Cfg.halt v' ∈ eval step (stepNormal c Cont.halt v)),
    ∃ (b₂ : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')),
      TrCfg (Cfg.halt v') b₂ ∧ b₂ ∈ eval (TM2.step (Γ := fun (x : K') ↦ Γ') tr) i

Tactic:
have := StateTransition.tr_eval (b₁ := Cfg.halt v') tr_respects h₁
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
c : Code
v : List ℕ
i : Cfg'
h₁ : TrCfg (stepNormal c Cont.halt v) i
h₂ : Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr) (init c v) i
v' : List ℕ
hv : v' ∈ c.eval v
this :
  ∀ (ab : Cfg.halt v' ∈ eval step (stepNormal c Cont.halt v)),
    ∃ (b₂ : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')),
      TrCfg (Cfg.halt v') b₂ ∧ b₂ ∈ eval (TM2.step (Γ := fun (x : K') ↦ Γ') tr) i
⊢ ∀ (ab : v' ∈ c.eval v),
    ∃ (b₂ : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')),
      TrCfg (Cfg.halt v') b₂ ∧ b₂ ∈ eval (TM2.step (Γ := fun (x : K') ↦ Γ') tr) i

Tactic:
simp only [stepNormal_eval, Part.map_eq_map, Part.mem_map_iff, Cfg.halt.injEq,
      exists_eq_right] at this

Premises used: Turing.ToPartrec.stepNormal_eval, exists_eq_right, Part.map_eq_map, Turing.ToPartrec.Cfg.halt.injEq, Part.mem_map_iff
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
c : Code
v : List ℕ
i : Cfg'
h₁ : TrCfg (stepNormal c Cont.halt v) i
h₂ : Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr) (init c v) i
v' : List ℕ
hv : v' ∈ c.eval v
this :
  ∀ (ab : v' ∈ c.eval v),
    ∃ (b₂ : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')),
      TrCfg (Cfg.halt v') b₂ ∧ b₂ ∈ eval (TM2.step (Γ := fun (x : K') ↦ Γ') tr) i
⊢ halt v' ∈ eval (TM2.step (Γ := fun (x : K') ↦ Γ') tr) i

Tactic:
obtain ⟨_, ⟨⟩, h⟩ := this hv
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
c : Code
v : List ℕ
i : Cfg'
h₁ : TrCfg (stepNormal c Cont.halt v) i
h₂ : Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr) (init c v) i
v' : List ℕ
hv : v' ∈ c.eval v
this :
  ∀ (ab : v' ∈ c.eval v),
    ∃ (b₂ : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')),
      TrCfg (Cfg.halt v') b₂ ∧ b₂ ∈ eval (TM2.step (Γ := fun (x : K') ↦ Γ') tr) i
h : halt v' ∈ eval (TM2.step (Γ := fun (x : K') ↦ Γ') tr) i
⊢ halt v' ∈ eval (TM2.step (Γ := fun (x : K') ↦ Γ') tr) i

Tactic:
h
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
c : Code
v : List ℕ
i : Cfg'
h₁ : TrCfg (stepNormal c Cont.halt v) i
h₂ : Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr) (init c v) i
v' : List ℕ
hv : v' ∈ c.eval v
this :
  ∀ (ab : v' ∈ c.eval v),
    ∃ (b₂ : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')),
      TrCfg (Cfg.halt v') b₂ ∧ b₂ ∈ eval (TM2.step (Γ := fun (x : K') ↦ Γ') tr) i
h : halt v' ∈ eval (TM2.step (Γ := fun (x : K') ↦ Γ') tr) i
⊢ halt v' ∈ eval (TM2.step (Γ := fun (x : K') ↦ Γ') tr) i

Tactic:
exact h
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q' : Λ'
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q
⊢ q' ∈ trStmts₁ (Λ'.move p k₁ k₂ q) → trStmts₁ q' ⊆ trStmts₁ (Λ'.move p k₁ k₂ q)

Tactic:
_
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q' : Λ'
p : Γ' → Bool
k : K'
q : Λ'
q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q
⊢ q' ∈ trStmts₁ (Λ'.clear p k q) → trStmts₁ q' ⊆ trStmts₁ (Λ'.clear p k q)

Tactic:
_
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q' q : Λ'
q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q
⊢ q' ∈ trStmts₁ q.copy → trStmts₁ q' ⊆ trStmts₁ q.copy

Tactic:
_
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q' : Λ'
k : K'
s : Option Γ' → Option Γ'
q : Λ'
q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q
⊢ q' ∈ trStmts₁ (Λ'.push k s q) → trStmts₁ q' ⊆ trStmts₁ (Λ'.push k s q)

Tactic:
_
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q' : Λ'
q : Option Γ' → Λ'
q_ih : ∀ (a : Option Γ'), q' ∈ trStmts₁ (q a) → trStmts₁ q' ⊆ trStmts₁ (q a)
⊢ q' ∈ trStmts₁ (Λ'.read q) → trStmts₁ q' ⊆ trStmts₁ (Λ'.read q)

Tactic:
_
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q' q : Λ'
q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q
⊢ q' ∈ trStmts₁ q.succ → trStmts₁ q' ⊆ trStmts₁ q.succ

Tactic:
_
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q' q₁ q₂ : Λ'
q₁_ih : q' ∈ trStmts₁ q₁ → trStmts₁ q' ⊆ trStmts₁ q₁
q₂_ih : q' ∈ trStmts₁ q₂ → trStmts₁ q' ⊆ trStmts₁ q₂
⊢ q' ∈ trStmts₁ (q₁.pred q₂) → trStmts₁ q' ⊆ trStmts₁ (q₁.pred q₂)

Tactic:
_
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q' : Λ'
k : Cont'
⊢ q' ∈ trStmts₁ (Λ'.ret k) → trStmts₁ q' ⊆ trStmts₁ (Λ'.ret k)

Tactic:
_
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q q' : Λ'
move :
  ∀ (p : Γ' → Bool) (k₁ k₂ : K') (q : Λ') (q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q),
    q' ∈ trStmts₁ (Λ'.move p k₁ k₂ q) → trStmts₁ q' ⊆ trStmts₁ (Λ'.move p k₁ k₂ q)
clear :
  ∀ (p : Γ' → Bool) (k : K') (q : Λ') (q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q),
    q' ∈ trStmts₁ (Λ'.clear p k q) → trStmts₁ q' ⊆ trStmts₁ (Λ'.clear p k q)
copy :
  ∀ (q : Λ') (q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q), q' ∈ trStmts₁ q.copy → trStmts₁ q' ⊆ trStmts₁ q.copy
push :
  ∀ (k : K') (s : Option Γ' → Option Γ') (q : Λ') (q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q),
    q' ∈ trStmts₁ (Λ'.push k s q) → trStmts₁ q' ⊆ trStmts₁ (Λ'.push k s q)
read :
  ∀ (q : Option Γ' → Λ') (q_ih : ∀ (a : Option Γ'), q' ∈ trStmts₁ (q a) → trStmts₁ q' ⊆ trStmts₁ (q a)),
    q' ∈ trStmts₁ (Λ'.read q) → trStmts₁ q' ⊆ trStmts₁ (Λ'.read q)
succ :
  ∀ (q : Λ') (q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q), q' ∈ trStmts₁ q.succ → trStmts₁ q' ⊆ trStmts₁ q.succ
pred :
  ∀ (q₁ q₂ : Λ') (q₁_ih : q' ∈ trStmts₁ q₁ → trStmts₁ q' ⊆ trStmts₁ q₁)
    (q₂_ih : q' ∈ trStmts₁ q₂ → trStmts₁ q' ⊆ trStmts₁ q₂),
    q' ∈ trStmts₁ (q₁.pred q₂) → trStmts₁ q' ⊆ trStmts₁ (q₁.pred q₂)
ret : ∀ (k : Cont'), q' ∈ trStmts₁ (Λ'.ret k) → trStmts₁ q' ⊆ trStmts₁ (Λ'.ret k)
⊢ q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q

Tactic:
induction q with
  | move _ _ _ q q_ih => _ | clear _ _ q q_ih => _ | copy q q_ih => _ | push _ _ q q_ih => _
  | read q q_ih => _ | succ q q_ih => _ | pred q₁ q₂ q₁_ih q₂_ih => _ | ret => _

Premises used: MonadReader.read, Turing.TM2.Stmt.push
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q' : Λ'
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q
move : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ insert (Λ'.move p k₁ k₂ q) (trStmts₁ q)
⊢ q' ∈ trStmts₁ (Λ'.move p k₁ k₂ q) → trStmts₁ q' ⊆ trStmts₁ (Λ'.move p k₁ k₂ q)

Tactic:
simp +contextual only [trStmts₁, Finset.mem_insert, Finset.mem_union,
      or_imp, Finset.mem_singleton, Finset.Subset.refl, imp_true_iff, true_and]

Premises used: Turing.PartrecToTM2.trStmts₁, Finset.mem_singleton, Finset.Subset.refl, or_imp, Finset.mem_insert, imp_true_iff, Finset.mem_union, true_and
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q' : Λ'
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q
⊢ q' ∈ trStmts₁ q → trStmts₁ q' ⊆ insert (Λ'.move p k₁ k₂ q) (trStmts₁ q)

Tactic:
fun h => Finset.Subset.trans (q_ih h) (Finset.subset_insert _ _)

Premises used: Turing.PartrecToTM2.trStmts₁, Finset.Subset.trans, Turing.PartrecToTM2.Λ'.move, Finset.subset_insert
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q' : Λ'
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q
⊢ q' ∈ trStmts₁ q → trStmts₁ q' ⊆ insert (Λ'.move p k₁ k₂ q) (trStmts₁ q)

Tactic:
exact fun h => Finset.Subset.trans (q_ih h) (Finset.subset_insert _ _)

Premises used: Turing.PartrecToTM2.trStmts₁, Finset.Subset.trans, Finset.subset_insert
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q' : Λ'
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q
⊢ q' ∈ trStmts₁ q → trStmts₁ q' ⊆ insert (Λ'.move p k₁ k₂ q) (trStmts₁ q)

Tactic:
repeat exact fun h => Finset.Subset.trans (q_ih h) (Finset.subset_insert _ _)

Premises used: Turing.PartrecToTM2.trStmts₁, Finset.Subset.trans, Finset.subset_insert
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q' : Λ'
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q
move : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ insert (Λ'.move p k₁ k₂ q) (trStmts₁ q)
⊢ q' ∈ trStmts₁ (Λ'.move p k₁ k₂ q) → trStmts₁ q' ⊆ trStmts₁ (Λ'.move p k₁ k₂ q)

Tactic:
all_goals
    simp +contextual only [trStmts₁, Finset.mem_insert, Finset.mem_union,
      or_imp, Finset.mem_singleton, Finset.Subset.refl, imp_true_iff, true_and]
    repeat exact fun h => Finset.Subset.trans (q_ih h) (Finset.subset_insert _ _)

Premises used: Turing.PartrecToTM2.trStmts₁, Finset.mem_singleton, Finset.Subset.trans, Finset.Subset.refl, or_imp, Finset.mem_insert, imp_true_iff, Finset.subset_insert, Finset.mem_union, true_and
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q' : Λ'
p : Γ' → Bool
k : K'
q : Λ'
q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q
clear : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ insert (Λ'.clear p k q) (trStmts₁ q)
⊢ q' ∈ trStmts₁ (Λ'.clear p k q) → trStmts₁ q' ⊆ trStmts₁ (Λ'.clear p k q)

Tactic:
simp +contextual only [trStmts₁, Finset.mem_insert, Finset.mem_union,
      or_imp, Finset.mem_singleton, Finset.Subset.refl, imp_true_iff, true_and]

Premises used: Turing.PartrecToTM2.trStmts₁, Finset.mem_singleton, Finset.Subset.refl, or_imp, Finset.mem_insert, imp_true_iff, Finset.mem_union, true_and
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q' : Λ'
p : Γ' → Bool
k : K'
q : Λ'
q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q
⊢ q' ∈ trStmts₁ q → trStmts₁ q' ⊆ insert (Λ'.clear p k q) (trStmts₁ q)

Tactic:
fun h => Finset.Subset.trans (q_ih h) (Finset.subset_insert _ _)

Premises used: Turing.PartrecToTM2.trStmts₁, Finset.Subset.trans, Turing.PartrecToTM2.Λ'.clear, Finset.subset_insert
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q' : Λ'
p : Γ' → Bool
k : K'
q : Λ'
q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q
⊢ q' ∈ trStmts₁ q → trStmts₁ q' ⊆ insert (Λ'.clear p k q) (trStmts₁ q)

Tactic:
exact fun h => Finset.Subset.trans (q_ih h) (Finset.subset_insert _ _)

Premises used: Turing.PartrecToTM2.trStmts₁, Finset.Subset.trans, Finset.subset_insert
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q' : Λ'
p : Γ' → Bool
k : K'
q : Λ'
q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q
⊢ q' ∈ trStmts₁ q → trStmts₁ q' ⊆ insert (Λ'.clear p k q) (trStmts₁ q)

Tactic:
repeat exact fun h => Finset.Subset.trans (q_ih h) (Finset.subset_insert _ _)

Premises used: Turing.PartrecToTM2.trStmts₁, Finset.Subset.trans, Finset.subset_insert
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q' : Λ'
p : Γ' → Bool
k : K'
q : Λ'
q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q
clear : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ insert (Λ'.clear p k q) (trStmts₁ q)
⊢ q' ∈ trStmts₁ (Λ'.clear p k q) → trStmts₁ q' ⊆ trStmts₁ (Λ'.clear p k q)

Tactic:
all_goals
    simp +contextual only [trStmts₁, Finset.mem_insert, Finset.mem_union,
      or_imp, Finset.mem_singleton, Finset.Subset.refl, imp_true_iff, true_and]
    repeat exact fun h => Finset.Subset.trans (q_ih h) (Finset.subset_insert _ _)

Premises used: Turing.PartrecToTM2.trStmts₁, Finset.mem_singleton, Finset.Subset.trans, Finset.Subset.refl, or_imp, Finset.mem_insert, imp_true_iff, Finset.subset_insert, Finset.mem_union, true_and
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q' q : Λ'
q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q
copy : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ insert q.copy (trStmts₁ q)
⊢ q' ∈ trStmts₁ q.copy → trStmts₁ q' ⊆ trStmts₁ q.copy

Tactic:
simp +contextual only [trStmts₁, Finset.mem_insert, Finset.mem_union,
      or_imp, Finset.mem_singleton, Finset.Subset.refl, imp_true_iff, true_and]

Premises used: Turing.PartrecToTM2.trStmts₁, Finset.mem_singleton, Finset.Subset.refl, or_imp, Finset.mem_insert, imp_true_iff, Finset.mem_union, true_and
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q' q : Λ'
q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q
⊢ q' ∈ trStmts₁ q → trStmts₁ q' ⊆ insert q.copy (trStmts₁ q)

Tactic:
fun h => Finset.Subset.trans (q_ih h) (Finset.subset_insert _ _)

Premises used: Turing.PartrecToTM2.trStmts₁, Finset.Subset.trans, Turing.PartrecToTM2.Λ'.copy, Finset.subset_insert