awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Computability.StateTransition (hypothesis)
Goal:
σ : Type u_1
f : σ → Option σ
a_1 b : σ
h_1 : b ∈ eval f a_1
a : σ
h_2 : b ∈ eval f a
IH : ∀ (a' : σ), f a = some a' → Reaches f a' b ∧ f b = none
a' : σ
e : f a = some a'
h : Sum.inr a' ∈ Part.some ((some a').elim (Sum.inl a) Sum.inr)
right : Membership.mem (γ := Part σ) (PFun.fix (fun (s : σ) ↦ Part.some ((f s).elim (Sum.inl s) Sum.inr)) a') b
⊢ Reaches f a b ∧ f b = none
have h₁ : Reaches f a' b
Tactic: obtain ⟨h₁, h₂⟩ := IH a' e
-- Lean 4 proof step from Mathlib.Computability.StateTransition (hypothesis)
Goal:
σ : Type u_1
f : σ → Option σ
a_1 b : σ
h_1 : b ∈ eval f a_1
a : σ
h_2 : b ∈ eval f a
IH : ∀ (a' : σ), f a = some a' → Reaches f a' b ∧ f b = none
a' : σ
e : f a = some a'
h : Sum.inr a' ∈ Part.some ((some a').elim (Sum.inl a) Sum.inr)
right : Membership.mem (γ := Part σ) (PFun.fix (fun (s : σ) ↦ Part.some ((f s).elim (Sum.inl s) Sum.inr)) a') b
h₁ : Reaches f a' b
⊢ Reaches f a b ∧ f b = none
have h₂ : f b = none
Tactic: obtain ⟨h₁, h₂⟩ := IH a' e
-- Lean 4 proof step from Mathlib.Computability.StateTransition (goal)
Goal:
σ : Type u_1
f : σ → Option σ
a b : σ
h : Reaches f a b ∧ f b = none
h₁ : Reaches f a b
h₂ : f b = none
⊢ b ∈ eval f a
have refine_2 : b ∈ eval f b
Tactic: refine ReflTransGen.head_induction_on h₁ ?_ fun h _ IH ↦ ?_
-- Lean 4 proof step from Mathlib.Computability.StateTransition (goal)
Goal:
σ : Type u_1
f : σ → Option σ
a b : σ
h : Reaches f a b ∧ f b = none
h₁ : Reaches f a b
h₂ : f b = none
refine_2 : b ∈ eval f b
⊢ b ∈ eval f a
have refine_2₁ : ∀ {a c : σ} (h : c ∈ f a), ReflTransGen (fun (a b : σ) ↦ b ∈ f a) c b → ∀ (IH : b ∈ eval f c), b ∈ eval f a
Tactic: refine ReflTransGen.head_induction_on h₁ ?_ fun h _ IH ↦ ?_
-- Lean 4 proof step from Mathlib.Computability.StateTransition (goal)
Goal:
σ : Type u_1
f : σ → Option σ
a b : σ
h : Reaches f a b ∧ f b = none
h₁ : Reaches f a b
h₂ : f b = none
⊢ b ∈ eval f b
have refine_2 : Sum.inl b ∈ Part.some ((f b).elim (Sum.inl b) Sum.inr)
Tactic: refine PFun.mem_fix_iff.2 (Or.inl ?_)
-- Lean 4 proof step from Mathlib.Computability.StateTransition (goal)
Goal:
σ : Type u_1
f : σ → Option σ
a b : σ
h : Reaches f a b ∧ f b = none
h₁ : Reaches f a b
h₂ : f b = none
⊢ Sum.inl b ∈ Part.some ((f b).elim (Sum.inl b) Sum.inr)
have refine_2 : Membership.mem (γ := Part (σ ⊕ σ)) (Part.some (Option.elim none (Sum.inl b) Sum.inr)) (Sum.inl b)
Tactic: rw [h₂]
-- Lean 4 proof step from Mathlib.Computability.StateTransition (goal)
Goal:
σ : Type u_1
f : σ → Option σ
a b : σ
h_1 : Reaches f a b ∧ f b = none
h₁ : Reaches f a b
h₂ : f b = none
a_1 c : σ
h : c ∈ f a_1
h_2 : ReflTransGen (fun (a b : σ) ↦ b ∈ f a) c b
IH : b ∈ eval f c
⊢ b ∈ eval f a_1
have refine_2 : Sum.inr c ∈ Part.some ((f a_1).elim (Sum.inl a_1) Sum.inr)
Tactic: refine PFun.mem_fix_iff.2 (Or.inr ⟨_, ?_, IH⟩)
-- Lean 4 proof step from Mathlib.Computability.StateTransition (goal)
Goal:
σ : Type u_1
f : σ → Option σ
a b : σ
h_1 : Reaches f a b ∧ f b = none
h₁ : Reaches f a b
h₂ : f b = none
a_1 c : σ
h : c ∈ f a_1
h_2 : ReflTransGen (fun (a b : σ) ↦ b ∈ f a) c b
IH : b ∈ eval f c
⊢ Sum.inr c ∈ Part.some ((f a_1).elim (Sum.inl a_1) Sum.inr)
have refine_2 : Sum.inr c ∈ Part.some ((some c).elim (Sum.inl a_1) Sum.inr)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Computability.StateTransition (hypothesis)
Goal:
σ : Type u_1
f : σ → Option σ
a b : σ
h : b ∈ eval f a
c : σ
h_1 : Reaches₁ f b c
bc : Reaches₁ f b c := h_1
⊢ False
have left : Reaches f a b
Tactic: let ⟨_, b0⟩ := mem_eval.1 h
-- Lean 4 proof step from Mathlib.Computability.StateTransition (hypothesis)
Goal:
σ : Type u_1
f : σ → Option σ
a b : σ
h : b ∈ eval f a
c : σ
h_1 : Reaches₁ f b c
bc : Reaches₁ f b c := h_1
left : Reaches f a b
⊢ False
have b0 : f b = none
Tactic: let ⟨_, b0⟩ := mem_eval.1 h
-- Lean 4 proof step from Mathlib.Computability.StateTransition (goal)
Goal:
σ : Type u_1
f : σ → Option σ
a b : σ
h : b ∈ eval f a
c : σ
h_1 : Reaches₁ f b c
bc : Reaches₁ f b c := h_1
left : Reaches f a b
b0 : f b = none
⊢ False
have let : ∀ (b' : σ) (h' : b' ∈ f b), ReflTransGen (fun (a b : σ) ↦ b ∈ f a) b' c → False
Tactic: let ⟨b', h', _⟩ := TransGen.head'_iff.1 bc
-- Lean 4 proof step from Mathlib.Computability.StateTransition (goal)
Goal:
σ : Type u_1
f : σ → Option σ
a b : σ
ab : Reaches f a b
⊢ eval f a = eval f b
have refine_1 : ∀ (x : σ) (h : x ∈ eval f a), x ∈ eval f b
Tactic: refine Part.ext fun _ ↦ ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Computability.StateTransition (goal)
Goal:
σ : Type u_1
f : σ → Option σ
a b : σ
ab : Reaches f a b
refine_1 : ∀ (x : σ) (h : x ∈ eval f a), x ∈ eval f b
⊢ eval f a = eval f b
have refine_2 : ∀ (x : σ) (h : x ∈ eval f b), x ∈ eval f a
Tactic: refine Part.ext fun _ ↦ ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Computability.StateTransition (hypothesis)
Goal:
σ : Type u_1
f : σ → Option σ
a b : σ
ab : Reaches f a b
x : σ
h : x ∈ eval f a
⊢ x ∈ eval f b
have ac : Reaches f a x
Tactic: have ⟨ac, c0⟩ := mem_eval.1 h
-- Lean 4 proof step from Mathlib.Computability.StateTransition (hypothesis)
Goal:
σ : Type u_1
f : σ → Option σ
a b : σ
ab : Reaches f a b
x : σ
h : x ∈ eval f a
ac : Reaches f a x
⊢ x ∈ eval f b
have c0 : f x = none
Tactic: have ⟨ac, c0⟩ := mem_eval.1 h
-- Lean 4 proof step from Mathlib.Computability.StateTransition (hypothesis)
Goal:
σ : Type u_1
f : σ → Option σ
a b : σ
ab : Reaches f a b
x : σ
h : x ∈ eval f b
⊢ x ∈ eval f a
have bc : Reaches f b x
Tactic: have ⟨bc, c0⟩ := mem_eval.1 h
-- Lean 4 proof step from Mathlib.Computability.StateTransition (hypothesis)
Goal:
σ : Type u_1
f : σ → Option σ
a b : σ
ab : Reaches f a b
x : σ
h : x ∈ eval f b
bc : Reaches f b x
⊢ x ∈ eval f a
have c0 : f x = none
Tactic: have ⟨bc, c0⟩ := mem_eval.1 h
-- 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₁ : σ₁
a₂ : σ₂
aa : tr a₁ a₂
b₁ b : σ₁
ac : b ∈ f₁ a₁
⊢ ∃ (b₂ : σ₂), tr b b₂ ∧ Reaches₁ f₂ a₂ b₂
have this : match (motive := Option σ₁ → Prop) f₁ a₁ with
| some b₁ => ∃ (b₂ : σ₂), tr b₁ b₂ ∧ Reaches₁ f₂ a₂ b₂
| none => f₂ a₂ = none
Tactic: have := H aa
-- 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₁ : σ₁
a₂ : σ₂
aa : tr a₁ a₂
b₁ b : σ₁
ac : b ∈ f₁ a₁
this :
  match (motive := Option σ₁ → Prop) f₁ a₁ with
  | some b₁ => ∃ (b₂ : σ₂), tr b₁ b₂ ∧ Reaches₁ f₂ a₂ b₂
  | none => f₂ a₂ = none
⊢ ∃ (b₂ : σ₂), tr b b₂ ∧ Reaches₁ f₂ a₂ b₂
have single : ∀
  (this :
    match (motive := Option σ₁ → Prop) some b with
    | some b₁ => ∃ (b₂ : σ₂), tr b₁ b₂ ∧ Reaches₁ f₂ a₂ b₂
    | none => f₂ a₂ = none),
  ∃ (b₂ : σ₂), tr b b₂ ∧ Reaches₁ f₂ a₂ b₂
Tactic: rwa [show f₁ a₁ = _ from ac] at this
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₁ : σ₁
a₂ : σ₂
aa : tr a₁ a₂
b₁ c₁ d₁ : σ₁
h : TransGen (fun (a b : σ₁) ↦ b ∈ f₁ a) a₁ c₁
cd : d₁ ∈ f₁ c₁
IH : ∃ (b₂ : σ₂), tr c₁ b₂ ∧ Reaches₁ f₂ a₂ b₂
⊢ ∃ (b₂ : σ₂), tr d₁ b₂ ∧ Reaches₁ f₂ a₂ b₂
have tail : ∀ (c₂ : σ₂) (cc : tr c₁ c₂) (ac₂ : Reaches₁ f₂ a₂ c₂), ∃ (b₂ : σ₂), tr d₁ b₂ ∧ Reaches₁ f₂ a₂ b₂
Tactic: rcases IH with ⟨c₂, cc, ac₂⟩
Cleared hypotheses: IH
-- 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₁ : σ₁
a₂ : σ₂
aa : tr a₁ a₂
b₁ c₁ d₁ : σ₁
h : TransGen (fun (a b : σ₁) ↦ b ∈ f₁ a) a₁ c₁
cd : d₁ ∈ f₁ c₁
c₂ : σ₂
cc : tr c₁ c₂
ac₂ : Reaches₁ f₂ a₂ c₂
⊢ ∃ (b₂ : σ₂), tr d₁ b₂ ∧ Reaches₁ f₂ a₂ b₂
have this : match (motive := Option σ₁ → Prop) f₁ c₁ with
| some b₁ => ∃ (b₂ : σ₂), tr b₁ b₂ ∧ Reaches₁ f₂ c₂ b₂
| none => f₂ c₂ = none
Tactic: have := H 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₁ : σ₁
a₂ : σ₂
aa : tr a₁ a₂
b₁ c₁ d₁ : σ₁
h : TransGen (fun (a b : σ₁) ↦ b ∈ f₁ a) a₁ c₁
cd : d₁ ∈ f₁ c₁
c₂ : σ₂
cc : tr c₁ c₂
ac₂ : Reaches₁ f₂ a₂ c₂
this :
  match (motive := Option σ₁ → Prop) f₁ c₁ with
  | some b₁ => ∃ (b₂ : σ₂), tr b₁ b₂ ∧ Reaches₁ f₂ c₂ b₂
  | none => f₂ c₂ = none
⊢ ∃ (b₂ : σ₂), tr d₁ b₂ ∧ Reaches₁ f₂ a₂ b₂
have this₁ : match (motive := Option σ₁ → Prop) some d₁ with
| some b₁ => ∃ (b₂ : σ₂), tr b₁ b₂ ∧ Reaches₁ f₂ c₂ b₂
| none => f₂ c₂ = none
Tactic: rw [show f₁ c₁ = _ from cd] at this
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₁ : σ₁
a₂ : σ₂
aa : tr a₁ a₂
b₁ c₁ d₁ : σ₁
h : TransGen (fun (a b : σ₁) ↦ b ∈ f₁ a) a₁ c₁
cd : d₁ ∈ f₁ c₁
c₂ : σ₂
cc : tr c₁ c₂
ac₂ : Reaches₁ f₂ a₂ c₂
this :
  match (motive := Option σ₁ → Prop) some d₁ with
  | some b₁ => ∃ (b₂ : σ₂), tr b₁ b₂ ∧ Reaches₁ f₂ c₂ b₂
  | none => f₂ c₂ = none
⊢ ∃ (b₂ : σ₂), tr d₁ b₂ ∧ Reaches₁ f₂ a₂ b₂
have tail : ∀ (d₂ : σ₂) (dd : tr d₁ d₂) (cd₂ : Reaches₁ f₂ c₂ d₂), ∃ (b₂ : σ₂), tr d₁ b₂ ∧ Reaches₁ f₂ a₂ b₂
Tactic: rcases this with ⟨d₂, dd, cd₂⟩
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₁ : σ₁
a₂ : σ₂
aa : tr a₁ a₂
b₁ : σ₁
ab : Reaches₁ f₁ a₁ b₁
⊢ ∃ (b₂ : σ₂), tr b₁ b₂ ∧ Reaches₁ f₂ a₂ b₂
have single : ∀ {b : σ₁} (ac : b ∈ f₁ a₁), ∃ (b₂ : σ₂), tr b b₂ ∧ Reaches₁ f₂ a₂ b₂
Tactic: induction ab with
  | single ac =>
    have := H aa
    rwa [show f₁ a₁ = _ from ac] at this
  | @tail c₁ d₁ _ cd IH =>
    rcases IH with ⟨c₂, cc, ac₂⟩
    have := H cc
    rw [show f₁ c₁ = _ from cd] at this
    rcases this with ⟨d₂, dd, cd₂⟩
    exact ⟨_, dd, ac₂.trans cd₂⟩
Cleared hypotheses: 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₁ : σ₁
a₂ : σ₂
aa : tr a₁ a₂
b₁ : σ₁
ab : Reaches₁ f₁ a₁ b₁
single : ∀ {b : σ₁} (ac : b ∈ f₁ a₁), ∃ (b₂ : σ₂), tr b b₂ ∧ Reaches₁ f₂ a₂ b₂
⊢ ∃ (b₂ : σ₂), tr b₁ b₂ ∧ Reaches₁ f₂ a₂ b₂
have tail : ∀ {c₁ d₁ : σ₁},
  TransGen (fun (a b : σ₁) ↦ b ∈ f₁ a) a₁ c₁ →
    ∀ (cd : d₁ ∈ f₁ c₁) (IH : ∃ (b₂ : σ₂), tr c₁ b₂ ∧ Reaches₁ f₂ a₂ b₂), ∃ (b₂ : σ₂), tr d₁ b₂ ∧ Reaches₁ f₂ a₂ b₂
Tactic: induction ab with
  | single ac =>
    have := H aa
    rwa [show f₁ a₁ = _ from ac] at this
  | @tail c₁ d₁ _ cd IH =>
    rcases IH with ⟨c₂, cc, ac₂⟩
    have := H cc
    rw [show f₁ c₁ = _ from cd] at this
    rcases this with ⟨d₂, dd, cd₂⟩
    exact ⟨_, dd, ac₂.trans cd₂⟩
Cleared hypotheses: 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₁ : σ₁
a₂ : σ₂
aa : tr a₁ a₂
b₁ : σ₁
ab : Reaches f₁ a₁ b₁
⊢ ∃ (b₂ : σ₂), tr b₁ b₂ ∧ Reaches f₂ a₂ b₂
have inl : ∀ (aa : tr b₁ a₂) (ab : Reaches f₁ b₁ b₁), ∃ (b₂ : σ₂), tr b₁ b₂ ∧ Reaches f₂ a₂ b₂
Tactic: rcases reflTransGen_iff_eq_or_transGen.1 ab with (rfl | ab)
Cleared hypotheses: a₁, aa, 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₁ : σ₁
a₂ : σ₂
aa : tr a₁ a₂
b₁ : σ₁
ab : Reaches f₁ a₁ b₁
inl : ∀ (aa : tr b₁ a₂) (ab : Reaches f₁ b₁ b₁), ∃ (b₂ : σ₂), tr b₁ b₂ ∧ Reaches f₂ a₂ b₂
⊢ ∃ (b₂ : σ₂), tr b₁ b₂ ∧ Reaches f₂ a₂ b₂
have inr : ∀ (ab : TransGen (fun (a b : σ₁) ↦ b ∈ f₁ a) a₁ b₁), ∃ (b₂ : σ₂), tr b₁ b₂ ∧ Reaches f₂ a₂ b₂
Tactic: rcases reflTransGen_iff_eq_or_transGen.1 ab with (rfl | 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₁ : σ₁
a₂ : σ₂
aa : tr a₁ a₂
b₁ : σ₁
ab_1 : Reaches f₁ a₁ b₁
ab : TransGen (fun (a b : σ₁) ↦ b ∈ f₁ a) a₁ b₁
⊢ ∃ (b₂ : σ₂), tr b₁ b₂ ∧ Reaches f₂ a₂ b₂
have inr : ∀ (b₂ : σ₂) (bb : tr b₁ b₂) (h : Reaches₁ f₂ a₂ b₂), ∃ (b₂ : σ₂), tr b₁ b₂ ∧ Reaches f₂ a₂ b₂
Tactic: have ⟨b₂, bb, h⟩ := tr_reaches₁ H aa 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₁ : σ₁
a₂ : σ₂
aa : tr a₁ a₂
b₂ b c : σ₂
h : ReflTransGen (fun (a b : σ₂) ↦ b ∈ f₂ a) a₂ b
cd : c ∈ f₂ b
IH : ∃ (c₁ : σ₁) (c₂ : σ₂), Reaches f₂ b c₂ ∧ tr c₁ c₂ ∧ Reaches f₁ a₁ c₁
⊢ ∃ (c₁ : σ₁) (c₂ : σ₂), Reaches f₂ c c₂ ∧ tr c₁ c₂ ∧ Reaches f₁ a₁ c₁
have tail : ∀ (e₁ : σ₁) (e₂ : σ₂) (ce : Reaches f₂ b e₂) (ee : tr e₁ e₂) (ae : Reaches f₁ a₁ e₁),
  ∃ (c₁ : σ₁) (c₂ : σ₂), Reaches f₂ c c₂ ∧ tr c₁ c₂ ∧ Reaches f₁ a₁ c₁
Tactic: rcases IH with ⟨e₁, e₂, ce, ee, ae⟩
Cleared hypotheses: IH
-- 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₁ : σ₁
a₂ : σ₂
aa : tr a₁ a₂
b₂ b c : σ₂
h : ReflTransGen (fun (a b : σ₂) ↦ b ∈ f₂ a) a₂ b
cd : c ∈ f₂ b
e₁ : σ₁
e₂ : σ₂
ce : Reaches f₂ b e₂
ee : tr e₁ e₂
ae : Reaches f₁ a₁ e₁
⊢ ∃ (c₁ : σ₁) (c₂ : σ₂), Reaches f₂ c c₂ ∧ tr c₁ c₂ ∧ Reaches f₁ a₁ c₁
have tail : ∀ (ce : Reaches f₂ b b) (ee : tr e₁ b), ∃ (c₁ : σ₁) (c₂ : σ₂), Reaches f₂ c c₂ ∧ tr c₁ c₂ ∧ Reaches f₁ a₁ c₁
Tactic: rcases ReflTransGen.cases_head ce with (rfl | ⟨d', cd', de⟩)
Cleared hypotheses: e₂, ce, ee
-- 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₁ : σ₁
a₂ : σ₂
aa : tr a₁ a₂
b₂ b c : σ₂
h : ReflTransGen (fun (a b : σ₂) ↦ b ∈ f₂ a) a₂ b
cd : c ∈ f₂ b
e₁ : σ₁
e₂ : σ₂
ce : Reaches f₂ b e₂
ee : tr e₁ e₂
ae : Reaches f₁ a₁ e₁
tail : ∀ (ce : Reaches f₂ b b) (ee : tr e₁ b), ∃ (c₁ : σ₁) (c₂ : σ₂), Reaches f₂ c c₂ ∧ tr c₁ c₂ ∧ Reaches f₁ a₁ c₁
⊢ ∃ (c₁ : σ₁) (c₂ : σ₂), Reaches f₂ c c₂ ∧ tr c₁ c₂ ∧ Reaches f₁ a₁ c₁
have tail₁ : ∀ (d' : σ₂) (cd' : d' ∈ f₂ b) (de : ReflTransGen (fun (a b : σ₂) ↦ b ∈ f₂ a) d' e₂),
  ∃ (c₁ : σ₁) (c₂ : σ₂), Reaches f₂ c c₂ ∧ tr c₁ c₂ ∧ Reaches f₁ a₁ c₁
Tactic: rcases ReflTransGen.cases_head ce with (rfl | ⟨d', cd', de⟩)
-- 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₁ : σ₁
a₂ : σ₂
aa : tr a₁ a₂
b₂ b c : σ₂
h : ReflTransGen (fun (a b : σ₂) ↦ b ∈ f₂ a) a₂ b
cd : c ∈ f₂ b
e₁ : σ₁
ae : Reaches f₁ a₁ e₁
ce : Reaches f₂ b b
ee : tr e₁ b
⊢ ∃ (c₁ : σ₁) (c₂ : σ₂), Reaches f₂ c c₂ ∧ tr c₁ c₂ ∧ Reaches f₁ a₁ c₁
have this : match (motive := Option σ₁ → Prop) f₁ e₁ with
| some b₁ => ∃ (b₂ : σ₂), tr b₁ b₂ ∧ Reaches₁ f₂ b b₂
| none => f₂ b = none
Tactic: have := H ee
-- 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₁ : σ₁
a₂ : σ₂
aa : tr a₁ a₂
b₂ b c : σ₂
h : ReflTransGen (fun (a b : σ₂) ↦ b ∈ f₂ a) a₂ b
cd : c ∈ f₂ b
e₁ : σ₁
ae : Reaches f₁ a₁ e₁
ce : Reaches f₂ b b
ee : tr e₁ b
this :
  match (motive := Option σ₁ → Prop) f₁ e₁ with
  | some b₁ => ∃ (b₂ : σ₂), tr b₁ b₂ ∧ Reaches₁ f₂ b b₂
  | none => f₂ b = none
⊢ ∃ (c₁ : σ₁) (c₂ : σ₂), Reaches f₂ c c₂ ∧ tr c₁ c₂ ∧ Reaches f₁ a₁ c₁
have tail : ∀
  (this :
    match (motive := Option σ₁ → Prop) f₁ e₁ with
    | some b₁ => ∃ (b₂ : σ₂), tr b₁ b₂ ∧ Reaches₁ f₂ b b₂
    | none => f₂ b = none),
  ∃ (c₁ : σ₁) (c₂ : σ₂), Reaches f₂ c c₂ ∧ tr c₁ c₂ ∧ Reaches f₁ a₁ c₁
Tactic: revert this
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₁ : σ₁
a₂ : σ₂
aa : tr a₁ a₂
b₂ b c : σ₂
h : ReflTransGen (fun (a b : σ₂) ↦ b ∈ f₂ a) a₂ b
cd : c ∈ f₂ b
e₁ : σ₁
ae : Reaches f₁ a₁ e₁
ce : Reaches f₂ b b
ee : tr e₁ b
⊢ ∀
    (this :
      match (motive := Option σ₁ → Prop) f₁ e₁ with
      | some b₁ => ∃ (b₂ : σ₂), tr b₁ b₂ ∧ Reaches₁ f₂ b b₂
      | none => f₂ b = none),
    ∃ (c₁ : σ₁) (c₂ : σ₂), Reaches f₂ c c₂ ∧ tr c₁ c₂ ∧ Reaches f₁ a₁ c₁
have tail : ∀ (eg : f₁ e₁ = none)
  (this :
    match (motive := Option σ₁ → Prop) none with
    | some b₁ => ∃ (b₂ : σ₂), tr b₁ b₂ ∧ Reaches₁ f₂ b b₂
    | none => f₂ b = none),
  ∃ (c₁ : σ₁) (c₂ : σ₂), Reaches f₂ c c₂ ∧ tr c₁ c₂ ∧ Reaches f₁ a₁ c₁
Tactic: rcases eg : f₁ e₁ with - | g₁
-- 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₁ : σ₁
a₂ : σ₂
aa : tr a₁ a₂
b₂ b c : σ₂
h : ReflTransGen (fun (a b : σ₂) ↦ b ∈ f₂ a) a₂ b
cd : c ∈ f₂ b
e₁ : σ₁
ae : Reaches f₁ a₁ e₁
ce : Reaches f₂ b b
ee : tr e₁ b
tail :
  ∀ (eg : f₁ e₁ = none)
    (this :
      match (motive := Option σ₁ → Prop) none with
      | some b₁ => ∃ (b₂ : σ₂), tr b₁ b₂ ∧ Reaches₁ f₂ b b₂
      | none => f₂ b = none),
    ∃ (c₁ : σ₁) (c₂ : σ₂), Reaches f₂ c c₂ ∧ tr c₁ c₂ ∧ Reaches f₁ a₁ c₁
⊢ ∀
    (this :
      match (motive := Option σ₁ → Prop) f₁ e₁ with
      | some b₁ => ∃ (b₂ : σ₂), tr b₁ b₂ ∧ Reaches₁ f₂ b b₂
      | none => f₂ b = none),
    ∃ (c₁ : σ₁) (c₂ : σ₂), Reaches f₂ c c₂ ∧ tr c₁ c₂ ∧ Reaches f₁ a₁ c₁
have tail₁ : ∀ (g₁ : σ₁) (eg : f₁ e₁ = some g₁)
  (this :
    match (motive := Option σ₁ → Prop) some g₁ with
    | some b₁ => ∃ (b₂ : σ₂), tr b₁ b₂ ∧ Reaches₁ f₂ b b₂
    | none => f₂ b = none),
  ∃ (c₁ : σ₁) (c₂ : σ₂), Reaches f₂ c c₂ ∧ tr c₁ c₂ ∧ Reaches f₁ a₁ c₁
Tactic: rcases eg : f₁ e₁ with - | g₁
-- 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₁ : σ₁
a₂ : σ₂
aa : tr a₁ a₂
b₂ b c : σ₂
h : ReflTransGen (fun (a b : σ₂) ↦ b ∈ f₂ a) a₂ b
cd : c ∈ f₂ b
e₁ : σ₁
ae : Reaches f₁ a₁ e₁
ce : Reaches f₂ b b
ee : tr e₁ b
g₁ : σ₁
eg : f₁ e₁ = some g₁
⊢ ∀
    (this :
      match (motive := Option σ₁ → Prop) some g₁ with
      | some b₁ => ∃ (b₂ : σ₂), tr b₁ b₂ ∧ Reaches₁ f₂ b b₂
      | none => f₂ b = none),
    ∃ (c₁ : σ₁) (c₂ : σ₂), Reaches f₂ c c₂ ∧ tr c₁ c₂ ∧ Reaches f₁ a₁ c₁
have tail : ∀ (x : σ₂), tr g₁ x → Reaches₁ f₂ b x → ∃ (c₁ : σ₁) (c₂ : σ₂), Reaches f₂ c c₂ ∧ tr c₁ c₂ ∧ Reaches f₁ a₁ c₁
Tactic: simp only [and_imp, exists_imp]
-- 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₁ : σ₁
a₂ : σ₂
aa : tr a₁ a₂
b₂ b c : σ₂
h : ReflTransGen (fun (a b : σ₂) ↦ b ∈ f₂ a) a₂ b
cd : c ∈ f₂ b
e₁ : σ₁
ae : Reaches f₁ a₁ e₁
ce : Reaches f₂ b b
ee : tr e₁ b
g₁ : σ₁
eg : f₁ e₁ = some g₁
g₂ : σ₂
gg : tr g₁ g₂
cg : Reaches₁ f₂ b g₂
⊢ ∃ (c₁ : σ₁) (c₂ : σ₂), Reaches f₂ c c₂ ∧ tr c₁ c₂ ∧ Reaches f₁ a₁ c₁
have tail : ∀ (d' : σ₂) (cd' : d' ∈ f₂ b) (dg : ReflTransGen (fun (a b : σ₂) ↦ b ∈ f₂ a) d' g₂),
  ∃ (c₁ : σ₁) (c₂ : σ₂), Reaches f₂ c c₂ ∧ tr c₁ c₂ ∧ Reaches f₁ a₁ c₁
Tactic: rcases TransGen.head'_iff.1 cg with ⟨d', cd', dg⟩
-- 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₁ : σ₁
a₂ : σ₂
aa : tr a₁ a₂
b₂ b c : σ₂
h : ReflTransGen (fun (a b : σ₂) ↦ b ∈ f₂ a) a₂ b
cd : c ∈ f₂ b
e₁ : σ₁
ae : Reaches f₁ a₁ e₁
ce : Reaches f₂ b b
ee : tr e₁ b
g₁ : σ₁
eg : f₁ e₁ = some g₁
g₂ : σ₂
gg : tr g₁ g₂
cg : Reaches₁ f₂ b g₂
d' : σ₂
cd' : d' ∈ f₂ b
dg : ReflTransGen (fun (a b : σ₂) ↦ b ∈ f₂ a) d' g₂
cd'₁ : c ∈ f₂ b
⊢ ∃ (c₁ : σ₁) (c₂ : σ₂), Reaches f₂ c c₂ ∧ tr c₁ c₂ ∧ Reaches f₁ a₁ c₁
have dg₁ : ReflTransGen (fun (a b : σ₂) ↦ b ∈ f₂ a) c g₂
Tactic: cases Option.mem_unique cd cd'
Cleared hypotheses: d', cd', dg
-- 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₁ : σ₁
a₂ : σ₂
aa : tr a₁ a₂
b₂ b c : σ₂
h : ReflTransGen (fun (a b : σ₂) ↦ b ∈ f₂ a) a₂ b
cd : c ∈ f₂ b
e₁ : σ₁
e₂ : σ₂
ce : Reaches f₂ b e₂
ee : tr e₁ e₂
ae : Reaches f₁ a₁ e₁
d' : σ₂
cd' : d' ∈ f₂ b
de : ReflTransGen (fun (a b : σ₂) ↦ b ∈ f₂ a) d' e₂
cd'₁ : c ∈ f₂ b
⊢ ∃ (c₁ : σ₁) (c₂ : σ₂), Reaches f₂ c c₂ ∧ tr c₁ c₂ ∧ Reaches f₁ a₁ c₁
have de₁ : ReflTransGen (fun (a b : σ₂) ↦ b ∈ f₂ a) c e₂
Tactic: cases Option.mem_unique cd cd'
Cleared hypotheses: d', cd', de
-- 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₁ : σ₁
a₂ : σ₂
aa : tr a₁ a₂
b₂ : σ₂
ab : Reaches f₂ a₂ b₂
⊢ ∃ (c₁ : σ₁) (c₂ : σ₂), Reaches f₂ b₂ c₂ ∧ tr c₁ c₂ ∧ Reaches f₁ a₁ c₁
have refl : ∃ (c₁ : σ₁) (c₂ : σ₂), Reaches f₂ a₂ c₂ ∧ tr c₁ c₂ ∧ Reaches f₁ a₁ c₁
Tactic: induction ab with
  | refl => exact ⟨_, _, ReflTransGen.refl, aa, ReflTransGen.refl⟩
  | tail _ cd IH =>
    rcases IH with ⟨e₁, e₂, ce, ee, ae⟩
    rcases ReflTransGen.cases_head ce with (rfl | ⟨d', cd', de⟩)
    · have := H ee
      revert this
      rcases eg : f₁ e₁ with - | g₁ <;> simp only [and_imp, exists_imp]
      · intro c0
        cases cd.symm.trans c0
      · intro g₂ gg cg
        rcases TransGen.head'_iff.1 cg with ⟨d', cd', dg⟩
        cases Option.mem_unique cd cd'
        exact ⟨_, _, dg, gg, ae.tail eg⟩
    · cases Option.mem_unique cd cd'
      exact ⟨_, _, de, ee, ae⟩
Cleared hypotheses: 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₁ : σ₁
a₂ : σ₂
aa : tr a₁ a₂
b₂ : σ₂
ab : Reaches f₂ a₂ b₂
refl : ∃ (c₁ : σ₁) (c₂ : σ₂), Reaches f₂ a₂ c₂ ∧ tr c₁ c₂ ∧ Reaches f₁ a₁ c₁
⊢ ∃ (c₁ : σ₁) (c₂ : σ₂), Reaches f₂ b₂ c₂ ∧ tr c₁ c₂ ∧ Reaches f₁ a₁ c₁
have tail : ∀ {b c : σ₂},
  ReflTransGen (fun (a b : σ₂) ↦ b ∈ f₂ a) a₂ b →
    ∀ (cd : c ∈ f₂ b) (IH : ∃ (c₁ : σ₁) (c₂ : σ₂), Reaches f₂ b c₂ ∧ tr c₁ c₂ ∧ Reaches f₁ a₁ c₁),
      ∃ (c₁ : σ₁) (c₂ : σ₂), Reaches f₂ c c₂ ∧ tr c₁ c₂ ∧ Reaches f₁ a₁ c₁
Tactic: induction ab with
  | refl => exact ⟨_, _, ReflTransGen.refl, aa, ReflTransGen.refl⟩
  | tail _ cd IH =>
    rcases IH with ⟨e₁, e₂, ce, ee, ae⟩
    rcases ReflTransGen.cases_head ce with (rfl | ⟨d', cd', de⟩)
    · have := H ee
      revert this
      rcases eg : f₁ e₁ with - | g₁ <;> simp only [and_imp, exists_imp]
      · intro c0
        cases cd.symm.trans c0
      · intro g₂ gg cg
        rcases TransGen.head'_iff.1 cg with ⟨d', cd', dg⟩
        cases Option.mem_unique cd cd'
        exact ⟨_, _, dg, gg, ae.tail eg⟩
    · cases Option.mem_unique cd cd'
      exact ⟨_, _, de, ee, ae⟩
Cleared hypotheses: 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₁
⊢ ∃ (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