awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.StateTransition
Goal:
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ b₁ : σ₁
a₂ : σ₂
aa : tr a₁ a₂
ab_1 : b₁ ∈ eval f₁ a₁
ab_2 : Reaches f₁ a₁ b₁
b0 : f₁ b₁ = none
b₂ : σ₂
bb : tr b₁ b₂
ab : Reaches f₂ a₂ b₂
⊢ ∃ (b₂ : σ₂), tr b₁ b₂ ∧ b₂ ∈ eval f₂ a₂

Tactic:
⟨_, bb, mem_eval.2 ⟨ab, ?_⟩⟩

Premises used: Iff.mpr, StateTransition.mem_eval, And.intro, Exists.intro
-- Module: Mathlib.Computability.StateTransition
Goal:
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ b₁ : σ₁
a₂ : σ₂
aa : tr a₁ a₂
ab_1 : b₁ ∈ eval f₁ a₁
ab_2 : Reaches f₁ a₁ b₁
b0 : f₁ b₁ = none
b₂ : σ₂
bb : tr b₁ b₂
ab : Reaches f₂ a₂ b₂
refine : f₂ b₂ = none
⊢ ∃ (b₂ : σ₂), tr b₁ b₂ ∧ b₂ ∈ eval f₂ a₂

Tactic:
refine ⟨_, bb, mem_eval.2 ⟨ab, ?_⟩⟩
-- Module: Mathlib.Computability.StateTransition
Goal:
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ b₁ : σ₁
a₂ : σ₂
aa : tr a₁ a₂
ab_1 : b₁ ∈ eval f₁ a₁
ab_2 : Reaches f₁ a₁ b₁
b0 : f₁ b₁ = none
b₂ : σ₂
bb : tr b₁ b₂
ab : Reaches f₂ a₂ b₂
⊢ match (motive := Option σ₁ → Prop) f₁ b₁ with
  | some b₁ => ∃ (b₂_1 : σ₂), tr b₁ b₂_1 ∧ Reaches₁ f₂ b₂ b₂_1
  | none => f₂ b₂ = none

Tactic:
have := H bb
-- Module: Mathlib.Computability.StateTransition
Goal:
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ b₁ : σ₁
a₂ : σ₂
aa : tr a₁ a₂
ab_1 : b₁ ∈ eval f₁ a₁
ab_2 : Reaches f₁ a₁ b₁
b0 : f₁ b₁ = none
b₂ : σ₂
bb : tr b₁ b₂
ab : Reaches f₂ a₂ b₂
this :
  match (motive := Option σ₁ → Prop) f₁ b₁ with
  | some b₁ => ∃ (b₂_1 : σ₂), tr b₁ b₂_1 ∧ Reaches₁ f₂ b₂ b₂_1
  | none => f₂ b₂ = none
rwa rwa₁ rwa₂ rwa₃ :
  ∀
    (this :
      match (motive := Option σ₁ → Prop) none with
      | some b₁ => ∃ (b₂_1 : σ₂), tr b₁ b₂_1 ∧ Reaches₁ f₂ b₂ b₂_1
      | none => f₂ b₂ = none),
    f₂ b₂ = none
⊢ f₂ b₂ = none

Tactic:
rwa [b0] at this
-- Module: Mathlib.Computability.StateTransition
Goal:
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ : σ₁
b₂ a₂ : σ₂
aa : tr a₁ a₂
ab : b₂ ∈ eval f₂ a₂
⊢ Reaches f₂ a₂ b₂

Tactic:
obtain ⟨ab, b0⟩ := mem_eval.1 ab

Premises used: StateTransition.mem_eval, Iff.mp
-- Module: Mathlib.Computability.StateTransition
Goal:
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ : σ₁
b₂ a₂ : σ₂
aa : tr a₁ a₂
ab : b₂ ∈ eval f₂ a₂
ab₁ : Reaches f₂ a₂ b₂
⊢ f₂ b₂ = none

Tactic:
obtain ⟨ab, b0⟩ := mem_eval.1 ab

Premises used: StateTransition.mem_eval, Iff.mp
-- Module: Mathlib.Computability.StateTransition
Goal:
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ : σ₁
b₂ a₂ : σ₂
aa : tr a₁ a₂
ab_1 : b₂ ∈ eval f₂ a₂
ab : Reaches f₂ a₂ b₂
b0 : f₂ b₂ = none
rcases :
  ∀ (c₁ : σ₁) (c₂ : σ₂) (bc : Reaches f₂ b₂ c₂) (cc : tr c₁ c₂) (ac : Reaches f₁ a₁ c₁),
    ∃ (b₁ : σ₁), tr b₁ b₂ ∧ b₁ ∈ eval f₁ a₁
⊢ ∃ (b₁ : σ₁), tr b₁ b₂ ∧ b₁ ∈ eval f₁ a₁

Tactic:
rcases tr_reaches_rev H aa ab with ⟨c₁, c₂, bc, cc, ac⟩

Premises used: StateTransition.tr_reaches_rev
-- Module: Mathlib.Computability.StateTransition
Goal:
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ : σ₁
b₂ a₂ : σ₂
aa : tr a₁ a₂
ab_1 : b₂ ∈ eval f₂ a₂
ab : Reaches f₂ a₂ b₂
b0 : f₂ b₂ = none
c₁ : σ₁
c₂ : σ₂
bc : Reaches f₂ b₂ c₂
cc : tr c₁ c₂
ac : Reaches f₁ a₁ c₁
⊢ Reaches f₂ b₂ b₂

Tactic:
cases (reflTransGen_iff_eq (Option.eq_none_iff_forall_not_mem.1 b0)).1 bc

Premises used: Iff.mp, Relation.reflTransGen_iff_eq
-- Module: Mathlib.Computability.StateTransition
Goal:
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ : σ₁
b₂ a₂ : σ₂
aa : tr a₁ a₂
ab_1 : b₂ ∈ eval f₂ a₂
ab : Reaches f₂ a₂ b₂
b0 : f₂ b₂ = none
c₁ : σ₁
c₂ : σ₂
bc : Reaches f₂ b₂ c₂
cc : tr c₁ c₂
ac : Reaches f₁ a₁ c₁
bc₁ : Reaches f₂ b₂ b₂
⊢ tr c₁ b₂

Tactic:
cases (reflTransGen_iff_eq (Option.eq_none_iff_forall_not_mem.1 b0)).1 bc

Premises used: Iff.mp, Relation.reflTransGen_iff_eq
-- Module: Mathlib.Computability.StateTransition
Goal:
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ : σ₁
b₂ a₂ : σ₂
aa : tr a₁ a₂
ab_1 : b₂ ∈ eval f₂ a₂
ab : Reaches f₂ a₂ b₂
b0 : f₂ b₂ = none
c₁ : σ₁
ac : Reaches f₁ a₁ c₁
bc : Reaches f₂ b₂ b₂
cc : tr c₁ b₂
⊢ ∃ (b₁ : σ₁), tr b₁ b₂ ∧ b₁ ∈ eval f₁ a₁

Tactic:
⟨_, cc, mem_eval.2 ⟨ac, ?_⟩⟩

Premises used: Iff.mpr, StateTransition.mem_eval, And.intro, Exists.intro
-- Module: Mathlib.Computability.StateTransition
Goal:
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ : σ₁
b₂ a₂ : σ₂
aa : tr a₁ a₂
ab_1 : b₂ ∈ eval f₂ a₂
ab : Reaches f₂ a₂ b₂
b0 : f₂ b₂ = none
c₁ : σ₁
ac : Reaches f₁ a₁ c₁
bc : Reaches f₂ b₂ b₂
cc : tr c₁ b₂
refl : f₁ c₁ = none
⊢ ∃ (b₁ : σ₁), tr b₁ b₂ ∧ b₁ ∈ eval f₁ a₁

Tactic:
refine ⟨_, cc, mem_eval.2 ⟨ac, ?_⟩⟩
-- Module: Mathlib.Computability.StateTransition
Goal:
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ : σ₁
b₂ a₂ : σ₂
aa : tr a₁ a₂
ab_1 : b₂ ∈ eval f₂ a₂
ab : Reaches f₂ a₂ b₂
b0 : f₂ b₂ = none
c₁ : σ₁
ac : Reaches f₁ a₁ c₁
bc : Reaches f₂ b₂ b₂
cc : tr c₁ b₂
⊢ match (motive := Option σ₁ → Prop) f₁ c₁ with
  | some b₁ => ∃ (b₂_1 : σ₂), tr b₁ b₂_1 ∧ Reaches₁ f₂ b₂ b₂_1
  | none => f₂ b₂ = none

Tactic:
have := H cc
-- Module: Mathlib.Computability.StateTransition
Goal:
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ : σ₁
b₂ a₂ : σ₂
aa : tr a₁ a₂
ab_1 : b₂ ∈ eval f₂ a₂
ab : Reaches f₂ a₂ b₂
b0 : f₂ b₂ = none
c₁ : σ₁
ac : Reaches f₁ a₁ c₁
bc : Reaches f₂ b₂ b₂
cc : tr c₁ b₂
this :
  match (motive := Option σ₁ → Prop) f₁ c₁ with
  | some b₁ => ∃ (b₂_1 : σ₂), tr b₁ b₂_1 ∧ Reaches₁ f₂ b₂ b₂_1
  | none => f₂ b₂ = none
refl : ∀ (hfc : f₁ c₁ = none), Eq.{u_1 + 1} (α := Option σ₁) none none
refl₁ : ∀ (d₁ : σ₁) (hfc : f₁ c₁ = some d₁), some d₁ = none
⊢ f₁ c₁ = none

Tactic:
rcases hfc : f₁ c₁ with - | d₁
-- Module: Mathlib.Computability.StateTransition
Goal:
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ : σ₁
b₂ a₂ : σ₂
aa : tr a₁ a₂
ab_1 : b₂ ∈ eval f₂ a₂
ab : Reaches f₂ a₂ b₂
b0 : f₂ b₂ = none
c₁ : σ₁
ac : Reaches f₁ a₁ c₁
bc : Reaches f₂ b₂ b₂
cc : tr c₁ b₂
this :
  match (motive := Option σ₁ → Prop) f₁ c₁ with
  | some b₁ => ∃ (b₂_1 : σ₂), tr b₁ b₂_1 ∧ Reaches₁ f₂ b₂ b₂_1
  | none => f₂ b₂ = none
hfc : f₁ c₁ = none
⊢ Eq.{u_1 + 1} (α := Option σ₁) none none

Tactic:
rfl
-- Module: Mathlib.Computability.StateTransition
Goal:
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ : σ₁
b₂ a₂ : σ₂
aa : tr a₁ a₂
ab_1 : b₂ ∈ eval f₂ a₂
ab : Reaches f₂ a₂ b₂
b0 : f₂ b₂ = none
c₁ : σ₁
ac : Reaches f₁ a₁ c₁
bc : Reaches f₂ b₂ b₂
cc : tr c₁ b₂
this :
  match (motive := Option σ₁ → Prop) f₁ c₁ with
  | some b₁ => ∃ (b₂_1 : σ₂), tr b₁ b₂_1 ∧ Reaches₁ f₂ b₂ b₂_1
  | none => f₂ b₂ = none
d₁ : σ₁
hfc : f₁ c₁ = some d₁
⊢ match (motive := Option σ₁ → Prop) some d₁ with
  | some b₁ => ∃ (b₂_1 : σ₂), tr b₁ b₂_1 ∧ Reaches₁ f₂ b₂ b₂_1
  | none => f₂ b₂ = none

Tactic:
rw [hfc] at this
-- Module: Mathlib.Computability.StateTransition
Goal:
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ : σ₁
b₂ a₂ : σ₂
aa : tr a₁ a₂
ab_1 : b₂ ∈ eval f₂ a₂
ab : Reaches f₂ a₂ b₂
b0 : f₂ b₂ = none
c₁ : σ₁
ac : Reaches f₁ a₁ c₁
bc : Reaches f₂ b₂ b₂
cc : tr c₁ b₂
this :
  match (motive := Option σ₁ → Prop) f₁ c₁ with
  | some b₁ => ∃ (b₂_1 : σ₂), tr b₁ b₂_1 ∧ Reaches₁ f₂ b₂ b₂_1
  | none => f₂ b₂ = none
d₁ : σ₁
hfc : f₁ c₁ = some d₁
this₁ :
  match (motive := Option σ₁ → Prop) some d₁ with
  | some b₁ => ∃ (b₂_1 : σ₂), tr b₁ b₂_1 ∧ Reaches₁ f₂ b₂ b₂_1
  | none => f₂ b₂ = none
⊢ f₁ c₁ = some d₁

Tactic:
rw [hfc] at this
-- Module: Mathlib.Computability.StateTransition
Goal:
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ : σ₁
b₂ a₂ : σ₂
aa : tr a₁ a₂
ab_1 : b₂ ∈ eval f₂ a₂
ab : Reaches f₂ a₂ b₂
b0 : f₂ b₂ = none
c₁ : σ₁
ac : Reaches f₁ a₁ c₁
bc : Reaches f₂ b₂ b₂
cc : tr c₁ b₂
d₁ : σ₁
this :
  match (motive := Option σ₁ → Prop) some d₁ with
  | some b₁ => ∃ (b₂_1 : σ₂), tr b₁ b₂_1 ∧ Reaches₁ f₂ b₂ b₂_1
  | none => f₂ b₂ = none
hfc : f₁ c₁ = some d₁
refl : ∀ (d₂ : σ₂), tr d₁ d₂ → ∀ (bd : Reaches₁ f₂ b₂ d₂), some d₁ = none
⊢ some d₁ = none

Tactic:
rcases this with ⟨d₂, _, bd⟩
-- Module: Mathlib.Computability.StateTransition
Goal:
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ : σ₁
b₂ a₂ : σ₂
aa : tr a₁ a₂
ab_1 : b₂ ∈ eval f₂ a₂
ab : Reaches f₂ a₂ b₂
b0 : f₂ b₂ = none
c₁ : σ₁
ac : Reaches f₁ a₁ c₁
bc : Reaches f₂ b₂ b₂
cc : tr c₁ b₂
d₁ : σ₁
hfc : f₁ c₁ = some d₁
d₂ : σ₂
left : tr d₁ d₂
bd : Reaches₁ f₂ b₂ d₂
refl : ∀ (e : σ₂) (h : e ∈ f₂ b₂), ReflTransGen (fun (a b : σ₂) ↦ b ∈ f₂ a) e d₂ → some d₁ = none
⊢ some d₁ = none

Tactic:
rcases TransGen.head'_iff.1 bd with ⟨e, h, _⟩

Premises used: Relation.TransGen.head'_iff, Iff.mp
-- Module: Mathlib.Computability.StateTransition
Goal:
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ : σ₁
b₂ a₂ : σ₂
aa : tr a₁ a₂
ab_1 : b₂ ∈ eval f₂ a₂
ab : Reaches f₂ a₂ b₂
b0 : f₂ b₂ = none
c₁ : σ₁
ac : Reaches f₁ a₁ c₁
bc : Reaches f₂ b₂ b₂
cc : tr c₁ b₂
d₁ : σ₁
hfc : f₁ c₁ = some d₁
d₂ : σ₂
left : tr d₁ d₂
bd : Reaches₁ f₂ b₂ d₂
e : σ₂
h : e ∈ f₂ b₂
right : ReflTransGen (fun (a b : σ₂) ↦ b ∈ f₂ a) e d₂
⊢ some d₁ = none

Tactic:
cases b0.symm.trans h

Premises used: Eq.symm, Eq.trans
-- Module: Mathlib.Computability.StateTransition
Goal:
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ : σ₁
a₂ : σ₂
aa : tr a₁ a₂
⊢ (eval f₂ a₂).Dom ↔ (eval f₁ a₁).Dom

Tactic:
⟨fun h ↦
    let ⟨_, _, h, _⟩ := tr_eval_rev H aa ⟨h, rfl⟩
    h,
    fun h ↦
    let ⟨_, _, h, _⟩ := tr_eval H aa ⟨h, rfl⟩
    h⟩

Premises used: StateTransition.tr_eval, _private.0.StateTransition.tr_eval_dom.match_1, Iff.intro, Exists.intro, Part.Dom, _private.0.StateTransition.tr_eval_dom.match_2, StateTransition.eval, StateTransition.tr_eval_rev, rfl
-- Module: Mathlib.Computability.StateTransition
Goal:
σ₁ : Type u_1
σ₂ : Type u_2
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂
a₂ b₂ : σ₂
h : f₂ a₂ = f₂ b₂
rw rw₁ :
  (match (motive := Option σ₁ → Prop) none with
    | some b₁ => Reaches₁ f₂ a₂ (tr b₁)
    | none => f₂ b₂ = none) ↔
    match (motive := Option σ₁ → Prop) none with
    | some b₁ => Reaches₁ f₂ b₂ (tr b₁)
    | none => f₂ b₂ = none
⊢ (match (motive := Option σ₁ → Prop) none with
    | some b₁ => Reaches₁ f₂ a₂ (tr b₁)
    | none => f₂ a₂ = none) ↔
    match (motive := Option σ₁ → Prop) none with
    | some b₁ => Reaches₁ f₂ b₂ (tr b₁)
    | none => f₂ b₂ = none

Tactic:
rw [h]
-- Module: Mathlib.Computability.StateTransition
Goal:
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂
a₁ : σ₁
none :
  (∀ ⦃a₂ : σ₂⦄,
      (fun (a : σ₁) (b : σ₂) ↦ tr a = b) a₁ a₂ →
        match (motive := Option σ₁ → Prop) Option.none with
        | Option.some b₁ => ∃ (b₂ : σ₂), (fun (a : σ₁) (b : σ₂) ↦ tr a = b) b₁ b₂ ∧ Reaches₁ f₂ a₂ b₂
        | Option.none => f₂ a₂ = Option.none) ↔
    FRespects f₂ tr (tr a₁) Option.none
some :
  ∀ (val : σ₁),
    (∀ ⦃a₂ : σ₂⦄,
        (fun (a : σ₁) (b : σ₂) ↦ tr a = b) a₁ a₂ →
          match (motive := Option σ₁ → Prop) Option.some val with
          | Option.some b₁ => ∃ (b₂ : σ₂), (fun (a : σ₁) (b : σ₂) ↦ tr a = b) b₁ b₂ ∧ Reaches₁ f₂ a₂ b₂
          | Option.none => f₂ a₂ = Option.none) ↔
      FRespects f₂ tr (tr a₁) (Option.some val)
⊢ (∀ ⦃a₂ : σ₂⦄,
      (fun (a : σ₁) (b : σ₂) ↦ tr a = b) a₁ a₂ →
        match (motive := Option σ₁ → Prop) f₁ a₁ with
        | Option.some b₁ => ∃ (b₂ : σ₂), (fun (a : σ₁) (b : σ₂) ↦ tr a = b) b₁ b₂ ∧ Reaches₁ f₂ a₂ b₂
        | Option.none => f₂ a₂ = Option.none) ↔
    FRespects f₂ tr (tr a₁) (f₁ a₁)

Tactic:
cases f₁ a₁
-- Module: Mathlib.Computability.StateTransition
Goal:
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂
a₁ : σ₁
⊢ (∀ ⦃a₂ : σ₂⦄,
      (fun (a : σ₁) (b : σ₂) ↦ tr a = b) a₁ a₂ →
        match (motive := Option σ₁ → Prop) none with
        | some b₁ => ∃ (b₂ : σ₂), (fun (a : σ₁) (b : σ₂) ↦ tr a = b) b₁ b₂ ∧ Reaches₁ f₂ a₂ b₂
        | none => f₂ a₂ = none) ↔
    FRespects f₂ tr (tr a₁) none

Tactic:
simp only [FRespects, exists_eq_left', forall_eq']

Premises used: exists_eq_left', forall_eq', StateTransition.FRespects
-- Module: Mathlib.Computability.StateTransition
Goal:
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂
a₁ val : σ₁
⊢ (∀ ⦃a₂ : σ₂⦄,
      (fun (a : σ₁) (b : σ₂) ↦ tr a = b) a₁ a₂ →
        match (motive := Option σ₁ → Prop) some val with
        | some b₁ => ∃ (b₂ : σ₂), (fun (a : σ₁) (b : σ₂) ↦ tr a = b) b₁ b₂ ∧ Reaches₁ f₂ a₂ b₂
        | none => f₂ a₂ = none) ↔
    FRespects f₂ tr (tr a₁) (some val)

Tactic:
simp only [FRespects, exists_eq_left', forall_eq']

Premises used: exists_eq_left', forall_eq', StateTransition.FRespects
-- Module: Mathlib.Computability.StateTransition
Goal:
σ₁ σ₂ : Type u_1
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂
H : Respects f₁ f₂ fun (a : σ₁) (b : σ₂) ↦ tr a = b
a₁ : σ₁
b₂ : σ₂
h : b₂ ∈ tr <$> eval f₁ a₁
rcases : ∀ (b₁ : σ₁) (ab : b₁ ∈ eval f₁ a₁) (bb : tr b₁ = b₂), b₂ ∈ eval f₂ (tr a₁)
⊢ b₂ ∈ eval f₂ (tr a₁)

Tactic:
rcases (Part.mem_map_iff _).1 h with ⟨b₁, ab, bb⟩

Premises used: Iff.mp, Part.mem_map_iff
-- Module: Mathlib.Computability.StateTransition
Goal:
σ₁ σ₂ : Type u_1
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂
H : Respects f₁ f₂ fun (a : σ₁) (b : σ₂) ↦ tr a = b
a₁ : σ₁
b₂ : σ₂
h : b₂ ∈ tr <$> eval f₁ a₁
b₁ : σ₁
ab : b₁ ∈ eval f₁ a₁
bb : tr b₁ = b₂
⊢ tr b₁ ∈ eval f₂ (tr a₁)

Tactic:
rcases tr_eval H rfl ab with ⟨_, rfl, h⟩

Premises used: StateTransition.tr_eval, rfl
-- Module: Mathlib.Computability.StateTransition
Goal:
σ₁ σ₂ : Type u_1
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂
H : Respects f₁ f₂ fun (a : σ₁) (b : σ₂) ↦ tr a = b
a₁ : σ₁
b₂ : σ₂
h_1 : b₂ ∈ tr <$> eval f₁ a₁
b₁ : σ₁
ab : b₁ ∈ eval f₁ a₁
bb : tr b₁ = b₂
h : tr b₁ ∈ eval f₂ (tr a₁)
rwa rwa₁ rwa₂ rwa₃ : ∀ (h : b₂ ∈ eval f₂ (tr a₁)), b₂ ∈ eval f₂ (tr a₁)
⊢ b₂ ∈ eval f₂ (tr a₁)

Tactic:
rwa [bb] at h
-- Module: Mathlib.Computability.StateTransition
Goal:
σ : Type u_1
f : σ → Option σ
a b : σ
c : Option σ
h₁ : EvalsTo f a (some b)
h₂ : EvalsTo f b c
rw : (flip bind f)^[h₂.steps] ((flip bind f)^[h₁.steps] (some a)) = c
rw₁ : (flip bind f)^[h₂.steps] (some b) = c
rw₂ rw₃ : c = c
⊢ (flip bind f)^[h₂.steps + h₁.steps] (some a) = c

Tactic:
rw [Function.iterate_add_apply, h₁.evals_in_steps, h₂.evals_in_steps]

Premises used: Function.iterate_add_apply, StateTransition.EvalsTo.evals_in_steps
-- Module: Mathlib.Computability.TuringDegree
Goal:
f g : ℕ →. ℕ
pF : Partrec f
⊢ f ≤ᵀ g

Tactic:
pF.recursiveIn

Premises used: Partrec.recursiveIn
-- Module: Mathlib.Computability.TuringDegree
Goal:
f : ℕ →. ℕ
s : Part ℕ
hf : f ≤ᵀ fun (x : ℕ) ↦ s
⊢ Partrec f

Tactic:
RecursiveIn.partrec_of_const hf

Premises used: RecursiveIn.partrec_of_const
-- Module: Mathlib.Computability.TuringDegree
Goal:
f : ℕ →. ℕ
⊢ Partrec f ↔ ∀ (g : ℕ →. ℕ), f ≤ᵀ g

Tactic:
⟨fun hf _ => hf.turingReducible, fun hf => hf (fun _ => .none) |>.partrec_of_const⟩

Premises used: Part.none, Iff.intro, Partrec.turingReducible, TuringReducible.partrec_of_const
-- Module: Mathlib.Computability.TuringDegree
Goal:
f : ℕ →. ℕ
⊢ Membership.mem (γ := Set (ℕ →. ℕ)) {f} f

Tactic:
simp
-- Module: Mathlib.Computability.TuringDegree
Goal:
f : ℕ →. ℕ
⊢ f ≤ᵀ f

Tactic:
.refl _

Premises used: TuringReducible.refl
-- Module: Mathlib.Computability.TuringDegree
Goal:
f g h : ℕ →. ℕ
hg : f ≤ᵀ g
hh : g ≤ᵀ h
⊢ ∀ (g_1 : ℕ →. ℕ), Membership.mem (γ := Set (ℕ →. ℕ)) {g} g_1 → RecursiveIn {h} g_1

Tactic:
simpa using hh
-- Module: Mathlib.Computability.TuringDegree
Goal:
⊢ Equivalence TuringEquivalent

Tactic:
(AntisymmRel.setoid _ _).iseqv

Premises used: Setoid.iseqv
-- Module: Mathlib.Computability.TuringDegree
Goal:
f : ℕ →. ℕ
⊢ f ≡ᵀ f

Tactic:
Equivalence.refl equivalence f

Premises used: Equivalence.refl, TuringEquivalent.equivalence
-- Module: Mathlib.Computability.TuringDegree
Goal:
f g : ℕ →. ℕ
h : f ≡ᵀ g
⊢ g ≡ᵀ f

Tactic:
Equivalence.symm equivalence h

Premises used: Equivalence.symm, TuringEquivalent.equivalence
-- Module: Mathlib.Computability.TuringDegree
Goal:
f g h : ℕ →. ℕ
h₁ : f ≡ᵀ g
h₂ : g ≡ᵀ h
⊢ f ≡ᵀ h

Tactic:
Equivalence.trans equivalence h₁ h₂

Premises used: TuringEquivalent.equivalence, Equivalence.trans
-- Module: Mathlib.Computability.TuringMachine.Computable
Goal:
tm : FinTM2
s : List (tm.Γ tm.k₀)
k : tm.K
h : k = tm.k₀
rw : List (tm.Γ tm.k₀)
⊢ List (tm.Γ k)

Tactic:
rw [h]
-- Module: Mathlib.Computability.TuringMachine.Computable
Goal:
tm : FinTM2
s : List (tm.Γ tm.k₀)
k : tm.K
h : k = tm.k₀
⊢ List (tm.Γ tm.k₀)

Tactic:
exact s
-- Module: Mathlib.Computability.TuringMachine.Computable
Goal:
tm : FinTM2
s : List (tm.Γ tm.k₁)
k : tm.K
h : k = tm.k₁
rw : List (tm.Γ tm.k₁)
⊢ List (tm.Γ k)

Tactic:
rw [h]
-- Module: Mathlib.Computability.TuringMachine.Computable
Goal:
tm : FinTM2
s : List (tm.Γ tm.k₁)
k : tm.K
h : k = tm.k₁
⊢ List (tm.Γ tm.k₁)

Tactic:
exact s
-- Module: Mathlib.Computability.TuringMachine.Computable
Goal:
α αΓ : Type
inst : Fintype αΓ
ea : α → List αΓ
x : α
⊢ 1 ≤ Polynomial.eval (ea x).length 1

Tactic:
simp only [Polynomial.eval_one, le_refl]

Premises used: le_refl, Polynomial.eval_one
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
⊢ zero'.eval = fun (v : List ℕ) ↦ pure (0 :: v)

Tactic:
simp [eval]

Premises used: Turing.ToPartrec.Code.eval
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
⊢ succ.eval = fun (v : List ℕ) ↦ pure [v.headI.succ]

Tactic:
simp [eval]

Premises used: Turing.ToPartrec.Code.eval
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
⊢ tail.eval = fun (v : List ℕ) ↦ pure v.tail

Tactic:
simp [eval]

Premises used: Turing.ToPartrec.Code.eval
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f fs : Code
⊢ (f.cons fs).eval = fun (v : List ℕ) ↦ do
    let n ← f.eval v
    let ns ← fs.eval v
    pure (n.headI :: ns)

Tactic:
simp [eval]

Premises used: Turing.ToPartrec.Code.eval
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f g : Code
⊢ (f.comp g).eval = fun (v : List ℕ) ↦ g.eval v >>= f.eval

Tactic:
simp [eval]

Premises used: Turing.ToPartrec.Code.eval
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f g : Code
⊢ (f.case g).eval = fun (v : List ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ Part (List ℕ)) (f.eval v.tail)
      (fun (y : ℕ) (x : Part (List ℕ)) ↦ g.eval (y :: v.tail)) v.headI

Tactic:
simp [eval]

Premises used: Turing.ToPartrec.Code.eval
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f : Code
⊢ f.fix.eval =
    PFun.fix fun (v : List ℕ) ↦
      Part.map (fun (v : List ℕ) ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v)

Tactic:
simp [eval]

Premises used: Turing.ToPartrec.Code.eval
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
v : List ℕ
⊢ nil.eval v = pure []

Tactic:
simp [nil]

Premises used: Turing.ToPartrec.Code.nil
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
v : List ℕ
⊢ id.eval v = pure v

Tactic:
simp [id]

Premises used: Turing.ToPartrec.Code.id
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
v : List ℕ
⊢ head.eval v = pure [v.headI]

Tactic:
simp [head]

Premises used: Turing.ToPartrec.Code.head
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
v : List ℕ
⊢ zero.eval v = pure [0]

Tactic:
simp [zero]

Premises used: Turing.ToPartrec.Code.zero
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
v : List ℕ
simp :
  Nat.rec (motive := fun (x : ℕ) ↦ Part (List ℕ)) (Part.some [0]) (fun (y : ℕ) (x : Part (List ℕ)) ↦ Part.some [y])
      v.headI =
    Part.some [v.headI - 1]
⊢ pred.eval v = pure [v.headI.pred]

Tactic:
simp [pred]

Premises used: Turing.ToPartrec.Code.pred
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
v : List ℕ
zero :
  Nat.rec (motive := fun (x : ℕ) ↦ Part (List ℕ)) (Part.some [0]) (fun (y : ℕ) (x : Part (List ℕ)) ↦ Part.some [y]) 0 =
    Part.some [HSub.hSub (α := ℕ) 0 1]
succ :
  ∀ (n : ℕ),
    Nat.rec (motive := fun (x : ℕ) ↦ Part (List ℕ)) (Part.some [0]) (fun (y : ℕ) (x : Part (List ℕ)) ↦ Part.some [y])
        (n + 1) =
      Part.some [n + 1 - 1]
⊢ Nat.rec (motive := fun (x : ℕ) ↦ Part (List ℕ)) (Part.some [0]) (fun (y : ℕ) (x : Part (List ℕ)) ↦ Part.some [y])
      v.headI =
    Part.some [v.headI - 1]

Tactic:
cases v.headI

Premises used: List.headI
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
v : List ℕ
⊢ Nat.rec (motive := fun (x : ℕ) ↦ Part (List ℕ)) (Part.some [0]) (fun (y : ℕ) (x : Part (List ℕ)) ↦ Part.some [y]) 0 =
    Part.some [HSub.hSub (α := ℕ) 0 1]

Tactic:
simp
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
v : List ℕ
n : ℕ
⊢ Nat.rec (motive := fun (x : ℕ) ↦ Part (List ℕ)) (Part.some [0]) (fun (y : ℕ) (x : Part (List ℕ)) ↦ Part.some [y])
      (n + 1) =
    Part.some [n + 1 - 1]

Tactic:
simp
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
m n : ℕ
f : List.Vector ℕ n →. ℕ
g : Fin n → List.Vector ℕ m →. ℕ
hf : ∃ (c : Code), ∀ (v : List.Vector ℕ n), c.eval (↑v : List ℕ) = pure <$> f v
hg : ∀ (i : Fin n), ∃ (c : Code), ∀ (v : List.Vector ℕ m), c.eval (↑v : List ℕ) = pure <$> g i v
rsuffices :
  ∀ (cg : Code)
    (hg :
      ∀ (v : List.Vector ℕ m),
        cg.eval (↑v : List ℕ) =
          Functor.map (α := { l : List ℕ // l.length = n }) (Subtype.val (p := fun (l : List ℕ) ↦ l.length = n))
            (Vector.mOfFn fun (i : Fin n) ↦ g i v)),
    ∃ (c : Code),
      ∀ (v : List.Vector ℕ m), c.eval (↑v : List ℕ) = pure <$> ((Vector.mOfFn fun (i : Fin n) ↦ g i v) >>= f)
rsuffices₁ :
  ∃ (c : Code),
    ∀ (v : List.Vector ℕ m),
      c.eval (↑v : List ℕ) =
        Functor.map (α := { l : List ℕ // l.length = n }) (Subtype.val (p := fun (l : List ℕ) ↦ l.length = n))
          (Vector.mOfFn fun (i : Fin n) ↦ g i v)
⊢ ∃ (c : Code), ∀ (v : List.Vector ℕ m), c.eval (↑v : List ℕ) = pure <$> ((Vector.mOfFn fun (i : Fin n) ↦ g i v) >>= f)

Tactic:
rsuffices ⟨cg, hg⟩ :
    ∃ c : Code, ∀ v : List.Vector ℕ m,
      c.eval v.1 = Subtype.val <$> List.Vector.mOfFn fun i => g i v

Premises used: Turing.ToPartrec.Code
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
m n : ℕ
f : List.Vector ℕ n →. ℕ
g : Fin n → List.Vector ℕ m →. ℕ
hf : ∃ (c : Code), ∀ (v : List.Vector ℕ n), c.eval (↑v : List ℕ) = pure <$> f v
hg_1 : ∀ (i : Fin n), ∃ (c : Code), ∀ (v : List.Vector ℕ m), c.eval (↑v : List ℕ) = pure <$> g i v
cg : Code
hg :
  ∀ (v : List.Vector ℕ m),
    cg.eval (↑v : List ℕ) =
      Functor.map (α := { l : List ℕ // l.length = n }) (Subtype.val (p := fun (l : List ℕ) ↦ l.length = n))
        (Vector.mOfFn fun (i : Fin n) ↦ g i v)
obtain :
  ∀ (cf : Code) (hf : ∀ (v : List.Vector ℕ n), cf.eval (↑v : List ℕ) = pure <$> f v),
    ∃ (c : Code),
      ∀ (v : List.Vector ℕ m), c.eval (↑v : List ℕ) = pure <$> ((Vector.mOfFn fun (i : Fin n) ↦ g i v) >>= f)
⊢ ∃ (c : Code), ∀ (v : List.Vector ℕ m), c.eval (↑v : List ℕ) = pure <$> ((Vector.mOfFn fun (i : Fin n) ↦ g i v) >>= f)

Tactic:
obtain ⟨cf, hf⟩ := hf