awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Computability.StateTransition (goal)
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
⊢ ∃ (b₂ : σ₂), tr b₁ b₂ ∧ b₂ ∈ eval f₂ a₂
have rcases : ∀ (b₂ : σ₂) (bb : tr b₁ b₂) (ab : Reaches f₂ a₂ b₂), ∃ (b₂ : σ₂), tr b₁ b₂ ∧ b₂ ∈ eval f₂ a₂
Tactic: rcases tr_reaches H aa ab with ⟨b₂, bb, ab⟩
-- Lean 4 proof step from Mathlib.Computability.StateTransition (goal)
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₂
have refine : f₂ b₂ = none
Tactic: refine ⟨_, bb, mem_eval.2 ⟨ab, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Computability.StateTransition (hypothesis)
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₂
⊢ f₂ b₂ = none
have 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
Tactic: have := H bb
-- Lean 4 proof step from Mathlib.Computability.StateTransition (goal)
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
⊢ f₂ b₂ = none
have 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
Tactic: rwa [b0] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Computability.StateTransition (hypothesis)
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₂
⊢ ∃ (b₁ : σ₁), tr b₁ b₂ ∧ b₁ ∈ eval f₁ a₁
have ab₁ : Reaches f₂ a₂ b₂
Tactic: obtain ⟨ab, b0⟩ := mem_eval.1 ab
-- Lean 4 proof step from Mathlib.Computability.StateTransition (hypothesis)
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₂
⊢ ∃ (b₁ : σ₁), tr b₁ b₂ ∧ b₁ ∈ eval f₁ a₁
have b0 : f₂ b₂ = none
Tactic: obtain ⟨ab, b0⟩ := mem_eval.1 ab
-- Lean 4 proof step from Mathlib.Computability.StateTransition (goal)
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
⊢ ∃ (b₁ : σ₁), tr b₁ b₂ ∧ b₁ ∈ eval f₁ a₁
have 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₁
Tactic: rcases tr_reaches_rev H aa ab with ⟨c₁, c₂, bc, cc, ac⟩
-- Lean 4 proof step from Mathlib.Computability.StateTransition (hypothesis)
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₁
⊢ ∃ (b₁ : σ₁), tr b₁ b₂ ∧ b₁ ∈ eval f₁ a₁
have bc₁ : Reaches f₂ b₂ b₂
Tactic: cases (reflTransGen_iff_eq (Option.eq_none_iff_forall_not_mem.1 b0)).1 bc
Cleared hypotheses: c₂, bc, cc
-- Lean 4 proof step from Mathlib.Computability.StateTransition (hypothesis)
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₂
⊢ ∃ (b₁ : σ₁), tr b₁ b₂ ∧ b₁ ∈ eval f₁ a₁
have cc₁ : tr c₁ b₂
Tactic: cases (reflTransGen_iff_eq (Option.eq_none_iff_forall_not_mem.1 b0)).1 bc
Cleared hypotheses: c₂, bc, cc
-- Lean 4 proof step from Mathlib.Computability.StateTransition (goal)
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₁
have refl : f₁ c₁ = none
Tactic: refine ⟨_, cc, mem_eval.2 ⟨ac, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Computability.StateTransition (hypothesis)
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₂
⊢ f₁ c₁ = none
have 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
Tactic: have := H cc
-- Lean 4 proof step from Mathlib.Computability.StateTransition (goal)
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
⊢ f₁ c₁ = none
have refl : ∀ (hfc : f₁ c₁ = none), Eq.{u_1 + 1} (α := Option σ₁) none none
Tactic: rcases hfc : f₁ c₁ with - | d₁
-- Lean 4 proof step from Mathlib.Computability.StateTransition (goal)
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
⊢ f₁ c₁ = none
have refl₁ : ∀ (d₁ : σ₁) (hfc : f₁ c₁ = some d₁), some d₁ = none
Tactic: rcases hfc : f₁ c₁ with - | d₁
-- Lean 4 proof step from Mathlib.Computability.StateTransition (hypothesis)
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₁
⊢ some d₁ = none
have 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
Tactic: rw [hfc] at this
Cleared hypotheses: this, hfc
-- Lean 4 proof step from Mathlib.Computability.StateTransition (goal)
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₁
⊢ some d₁ = none
have refl : ∀ (d₂ : σ₂), tr d₁ d₂ → ∀ (bd : Reaches₁ f₂ b₂ d₂), some d₁ = none
Tactic: rcases this with ⟨d₂, _, bd⟩
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Computability.StateTransition (goal)
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₂
⊢ some d₁ = none
have refl : ∀ (e : σ₂) (h : e ∈ f₂ b₂), ReflTransGen (fun (a b : σ₂) ↦ b ∈ f₂ a) e d₂ → some d₁ = none
Tactic: rcases TransGen.head'_iff.1 bd with ⟨e, h, _⟩
-- Lean 4 proof step from Mathlib.Computability.StateTransition (goal)
Goal:
σ₁ : Type u_1
σ₂ : Type u_2
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂
a₂ b₂ : σ₂
h : f₂ a₂ = f₂ b₂
⊢ (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
have 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
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Computability.StateTransition (goal)
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) f₁ a₁ 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₁) (f₁ a₁)
have none : (∀ ⦃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: cases f₁ a₁
-- Lean 4 proof step from Mathlib.Computability.StateTransition (goal)
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
        | 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
⊢ (∀ ⦃a₂ : σ₂⦄,
      (fun (a : σ₁) (b : σ₂) ↦ tr a = b) a₁ a₂ →
        match (motive := Option σ₁ → Prop) f₁ a₁ with
        | 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₁)
have some : ∀ (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₂
        | Option.none => f₂ a₂ = Option.none) ↔
    FRespects f₂ tr (tr a₁) (some val)
Tactic: cases f₁ a₁
-- Lean 4 proof step from Mathlib.Computability.StateTransition (goal)
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₂ ∈ eval f₂ (tr a₁)
have rcases : ∀ (b₁ : σ₁) (ab : b₁ ∈ eval f₁ a₁) (bb : tr b₁ = b₂), b₂ ∈ eval f₂ (tr a₁)
Tactic: rcases (Part.mem_map_iff _).1 h with ⟨b₁, ab, bb⟩
-- Lean 4 proof step from Mathlib.Computability.StateTransition (hypothesis)
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₂
⊢ b₂ ∈ eval f₂ (tr a₁)
have h₁ : tr b₁ ∈ eval f₂ (tr a₁)
Tactic: rcases tr_eval H rfl ab with ⟨_, rfl, h⟩
-- Lean 4 proof step from Mathlib.Computability.StateTransition (goal)
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₁)
⊢ b₂ ∈ eval f₂ (tr a₁)
have rwa : ∀ (h : b₂ ∈ eval f₂ (tr a₁)), b₂ ∈ eval f₂ (tr a₁)
Tactic: rwa [bb] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Computability.StateTransition (goal)
Goal:
σ : Type u_1
f : σ → Option σ
a b : σ
c : Option σ
h₁ : EvalsTo f a (some b)
h₂ : EvalsTo f b c
⊢ (flip bind f)^[h₂.steps + h₁.steps] (some a) = c
have rw : (flip bind f)^[h₂.steps] ((flip bind f)^[h₁.steps] (some a)) = c
Tactic: rw [Function.iterate_add_apply, h₁.evals_in_steps, h₂.evals_in_steps]
-- Lean 4 proof step from Mathlib.Computability.StateTransition (goal)
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
⊢ (flip bind f)^[h₂.steps + h₁.steps] (some a) = c
have rw₁ : (flip bind f)^[h₂.steps] (some b) = c
Tactic: rw [Function.iterate_add_apply, h₁.evals_in_steps, h₂.evals_in_steps]
-- Lean 4 proof step from Mathlib.Computability.StateTransition (goal)
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
⊢ (flip bind f)^[h₂.steps + h₁.steps] (some a) = c
have rw₂ : c = c
Tactic: rw [Function.iterate_add_apply, h₁.evals_in_steps, h₂.evals_in_steps]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
v : List ℕ
⊢ pred.eval v = pure [v.headI.pred]
have 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]
Tactic: simp [pred]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
v : List ℕ
⊢ 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]
have 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]
Tactic: cases v.headI
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
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]
⊢ 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]
have 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]
Tactic: cases v.headI
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
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
⊢ ∃ (c : Code), ∀ (v : List.Vector ℕ m), c.eval (↑v : List ℕ) = pure <$> ((Vector.mOfFn fun (i : Fin n) ↦ g i v) >>= f)
have 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)
Tactic: rsuffices ⟨cg, hg⟩ :
    ∃ c : Code, ∀ v : List.Vector ℕ m,
      c.eval v.1 = Subtype.val <$> List.Vector.mOfFn fun i => g i v
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
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)
⊢ ∃ (c : Code), ∀ (v : List.Vector ℕ m), c.eval (↑v : List ℕ) = pure <$> ((Vector.mOfFn fun (i : Fin n) ↦ g i v) >>= f)
have 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)
Tactic: rsuffices ⟨cg, hg⟩ :
    ∃ c : Code, ∀ v : List.Vector ℕ m,
      c.eval v.1 = Subtype.val <$> List.Vector.mOfFn fun i => g i v
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
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)
⊢ ∃ (c : Code), ∀ (v : List.Vector ℕ m), c.eval (↑v : List ℕ) = pure <$> ((Vector.mOfFn fun (i : Fin n) ↦ g i v) >>= f)
have 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)
Tactic: obtain ⟨cf, hf⟩ := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
m n : ℕ
f : List.Vector ℕ n →. ℕ
g : Fin n → List.Vector ℕ m →. ℕ
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)
cf : Code
hf : ∀ (v : List.Vector ℕ n), cf.eval (↑v : List ℕ) = pure <$> f v
v : List.Vector ℕ m
⊢ (cf.comp cg).eval (↑v : List ℕ) = pure <$> ((Vector.mOfFn fun (i : Fin n) ↦ g i v) >>= f)
have simp : Eq (α := Part (List ℕ))
  (do
    let a ← Vector.mOfFn fun (i : Fin n) ↦ g i v
    pure <$> f a)
  do
  let a ← Vector.mOfFn fun (i : Fin n) ↦ g i v
  pure <$> f a
Tactic: simp [hg, hf, map_bind]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
m : ℕ
g : Fin 0 → List.Vector ℕ m →. ℕ
hg : ∀ (i : Fin 0), ∃ (c : Code), ∀ (v : List.Vector ℕ m), c.eval (↑v : List ℕ) = pure <$> g i v
v : List.Vector ℕ m
⊢ nil.eval (↑v : List ℕ) =
    Functor.map (α := { l : List ℕ // l.length = 0 }) (Subtype.val (p := fun (l : List ℕ) ↦ l.length = 0))
      (Vector.mOfFn fun (i : Fin 0) ↦ g i v)
have simp : Eq (α := Part (List ℕ)) (Part.some []) (Subtype.val (p := fun (l : List ℕ) ↦ l.length = 0) <$> Part.some Vector.nil)
Tactic: simp [Vector.mOfFn]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
m n : ℕ
IH :
  ∀ {g : Fin n → List.Vector ℕ m →. ℕ}
    (hg : ∀ (i : Fin n), ∃ (c : Code), ∀ (v : List.Vector ℕ m), c.eval (↑v : List ℕ) = pure <$> g i v),
    ∃ (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)
g : Fin (n + 1) → List.Vector ℕ m →. ℕ
hg : ∀ (i : Fin (n + 1)), ∃ (c : Code), ∀ (v : List.Vector ℕ m), c.eval (↑v : List ℕ) = pure <$> g i v
⊢ ∃ (c : Code),
    ∀ (v : List.Vector ℕ m),
      c.eval (↑v : List ℕ) =
        Functor.map (α := { l : List ℕ // l.length = n + 1 }) (Subtype.val (p := fun (l : List ℕ) ↦ l.length = n + 1))
          (Vector.mOfFn fun (i : Fin (n + 1)) ↦ g i v)
have succ : ∀ (cg : Code) (hg₁ : ∀ (v : List.Vector ℕ m), cg.eval (↑v : List ℕ) = pure <$> g 0 v),
  ∃ (c : Code),
    ∀ (v : List.Vector ℕ m),
      c.eval (↑v : List ℕ) =
        Functor.map (α := { l : List ℕ // l.length = n + 1 }) (Subtype.val (p := fun (l : List ℕ) ↦ l.length = n + 1))
          (Vector.mOfFn fun (i : Fin (n + 1)) ↦ g i v)
Tactic: obtain ⟨cg, hg₁⟩ := hg 0
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
m n : ℕ
IH :
  ∀ {g : Fin n → List.Vector ℕ m →. ℕ}
    (hg : ∀ (i : Fin n), ∃ (c : Code), ∀ (v : List.Vector ℕ m), c.eval (↑v : List ℕ) = pure <$> g i v),
    ∃ (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)
g : Fin (n + 1) → List.Vector ℕ m →. ℕ
hg : ∀ (i : Fin (n + 1)), ∃ (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 ℕ) = pure <$> g 0 v
⊢ ∃ (c : Code),
    ∀ (v : List.Vector ℕ m),
      c.eval (↑v : List ℕ) =
        Functor.map (α := { l : List ℕ // l.length = n + 1 }) (Subtype.val (p := fun (l : List ℕ) ↦ l.length = n + 1))
          (Vector.mOfFn fun (i : Fin (n + 1)) ↦ g i v)
have succ : ∀ (cl : Code)
  (hl :
    ∀ (v : List.Vector ℕ m),
      cl.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.succ v)),
  ∃ (c : Code),
    ∀ (v : List.Vector ℕ m),
      c.eval (↑v : List ℕ) =
        Functor.map (α := { l : List ℕ // l.length = n + 1 }) (Subtype.val (p := fun (l : List ℕ) ↦ l.length = n + 1))
          (Vector.mOfFn fun (i : Fin (n + 1)) ↦ g i v)
Tactic: obtain ⟨cl, hl⟩ := IH fun i => hg i.succ
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
m n : ℕ
IH :
  ∀ {g : Fin n → List.Vector ℕ m →. ℕ}
    (hg : ∀ (i : Fin n), ∃ (c : Code), ∀ (v : List.Vector ℕ m), c.eval (↑v : List ℕ) = pure <$> g i v),
    ∃ (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)
g : Fin (n + 1) → List.Vector ℕ m →. ℕ
hg : ∀ (i : Fin (n + 1)), ∃ (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 ℕ) = pure <$> g 0 v
cl : Code
hl :
  ∀ (v : List.Vector ℕ m),
    cl.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.succ v)
v : List.Vector ℕ m
⊢ (cg.cons cl).eval (↑v : List ℕ) =
    Functor.map (α := { l : List ℕ // l.length = n + 1 }) (Subtype.val (p := fun (l : List ℕ) ↦ l.length = n + 1))
      (Vector.mOfFn fun (i : Fin (n + 1)) ↦ g i v)
have simp : Eq (α := Part (List ℕ))
  (do
    let a ← g 0 v
    let a_1 ← Vector.mOfFn fun (i : Fin n) ↦ g i.succ v
    Part.some (a :: (↑a_1 : List ℕ)))
  (Functor.map (α := { l : List ℕ // l.length = n + 1 }) (Subtype.val (p := fun (l : List ℕ) ↦ l.length = n + 1)) do
    let a ← g 0 v
    let v ← Vector.mOfFn fun (i : Fin n) ↦ g i.succ v
    Part.some (a ::ᵥ v))
Tactic: simp [Vector.mOfFn, hg₁, hl]