awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.StateTransition
Goal:
σ : Type u_1
f : σ → Option σ
a b : σ
h : b ∈ eval f a
c : σ
left : Reaches f a b
b0 : f b = none
b' : σ
h' : b' ∈ f b
⊢ False

Tactic:
cases b0.symm.trans h'

Premises used: Eq.symm, Eq.trans
-- Module: Mathlib.Computability.StateTransition
Goal:
σ : Type u_1
f : σ → Option σ
a b : σ
ab : Reaches f a b
⊢ eval f a = eval f b

Tactic:
Part.ext fun _ ↦ ⟨fun h ↦ ?_, fun h ↦ ?_⟩

Premises used: Part.ext, Iff.intro
-- Module: Mathlib.Computability.StateTransition
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
refine_2 : ∀ (x : σ) (h : x ∈ eval f b), x ∈ eval f a
⊢ eval f a = eval f b

Tactic:
refine Part.ext fun _ ↦ ⟨fun h ↦ ?_, fun h ↦ ?_⟩

Premises used: Part.ext, Iff.intro
-- Module: Mathlib.Computability.StateTransition
Goal:
σ : Type u_1
f : σ → Option σ
a b : σ
ab : Reaches f a b
x : σ
h : x ∈ eval f a
⊢ Reaches f a x

Tactic:
have ⟨ac, c0⟩ := mem_eval.1 h
-- Module: Mathlib.Computability.StateTransition
Goal:
σ : Type u_1
f : σ → Option σ
a b : σ
ab : Reaches f a b
x : σ
h : x ∈ eval f a
ac : Reaches f a x
⊢ f x = none

Tactic:
have ⟨ac, c0⟩ := mem_eval.1 h
-- Module: Mathlib.Computability.StateTransition
Goal:
σ : Type u_1
f : σ → Option σ
a b : σ
ab : Reaches f a b
x : σ
h : x ∈ eval f a
ac : Reaches f a x
c0 : f x = none
⊢ x ∈ eval f b

Tactic:
mem_eval.2 ⟨(or_iff_left_of_imp fun cb ↦ (eval_maximal h).1 cb ▸ ReflTransGen.refl).1
      (reaches_total ab ac), c0⟩

Premises used: Iff.mpr, or_iff_left_of_imp, StateTransition.mem_eval, And.intro, Iff.mp, StateTransition.reaches_total
-- Module: Mathlib.Computability.StateTransition
Goal:
σ : Type u_1
f : σ → Option σ
a b : σ
ab : Reaches f a b
x : σ
h : x ∈ eval f a
ac : Reaches f a x
c0 : f x = none
⊢ x ∈ eval f b

Tactic:
exact mem_eval.2 ⟨(or_iff_left_of_imp fun cb ↦ (eval_maximal h).1 cb ▸ ReflTransGen.refl).1
      (reaches_total ab ac), c0⟩

Premises used: Iff.mpr, or_iff_left_of_imp, StateTransition.mem_eval, And.intro, Iff.mp, StateTransition.reaches_total
-- Module: Mathlib.Computability.StateTransition
Goal:
σ : Type u_1
f : σ → Option σ
a b : σ
ab : Reaches f a b
x : σ
h : x ∈ eval f b
⊢ Reaches f b x

Tactic:
have ⟨bc, c0⟩ := mem_eval.1 h
-- Module: Mathlib.Computability.StateTransition
Goal:
σ : Type u_1
f : σ → Option σ
a b : σ
ab : Reaches f a b
x : σ
h : x ∈ eval f b
bc : Reaches f b x
⊢ f x = none

Tactic:
have ⟨bc, c0⟩ := mem_eval.1 h
-- Module: Mathlib.Computability.StateTransition
Goal:
σ : Type u_1
f : σ → Option σ
a b : σ
ab : Reaches f a b
x : σ
h : x ∈ eval f b
bc : Reaches f b x
c0 : f x = none
⊢ x ∈ eval f a

Tactic:
mem_eval.2 ⟨ab.trans bc, c0⟩

Premises used: Iff.mpr, Relation.ReflTransGen.trans, StateTransition.mem_eval, And.intro
-- Module: Mathlib.Computability.StateTransition
Goal:
σ : Type u_1
f : σ → Option σ
a b : σ
ab : Reaches f a b
x : σ
h : x ∈ eval f b
bc : Reaches f b x
c0 : f x = none
⊢ x ∈ eval f a

Tactic:
exact mem_eval.2 ⟨ab.trans bc, c0⟩

Premises used: Iff.mpr, Relation.ReflTransGen.trans, StateTransition.mem_eval, And.intro
-- 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₂
b₁ b : σ₁
ac : b ∈ f₁ a₁
⊢ 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
-- 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₂
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
single single₁ single₂ 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₂
⊢ ∃ (b₂ : σ₂), tr b b₂ ∧ Reaches₁ f₂ a₂ b₂

Tactic:
rwa [show f₁ a₁ = _ from ac] 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₁ : σ₁
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₂
tail : ∀ (c₂ : σ₂) (cc : tr c₁ c₂) (ac₂ : Reaches₁ f₂ a₂ c₂), ∃ (b₂ : σ₂), tr d₁ b₂ ∧ Reaches₁ f₂ a₂ b₂
⊢ ∃ (b₂ : σ₂), tr d₁ b₂ ∧ Reaches₁ f₂ a₂ b₂

Tactic:
rcases IH with ⟨c₂, cc, ac₂⟩
-- 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₂
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₂
⊢ 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
-- 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₂
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
⊢ 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
-- 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₂
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
tail : ∀ (d₂ : σ₂) (dd : tr d₁ d₂) (cd₂ : Reaches₁ f₂ c₂ d₂), ∃ (b₂ : σ₂), tr d₁ b₂ ∧ Reaches₁ f₂ a₂ b₂
⊢ ∃ (b₂ : σ₂), tr d₁ b₂ ∧ Reaches₁ f₂ a₂ b₂

Tactic:
rcases this with ⟨d₂, dd, cd₂⟩
-- 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₂
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₂
d₂ : σ₂
dd : tr d₁ d₂
cd₂ : Reaches₁ f₂ c₂ d₂
⊢ ∃ (b₂ : σ₂), tr d₁ b₂ ∧ Reaches₁ f₂ a₂ b₂

Tactic:
⟨_, dd, ac₂.trans cd₂⟩

Premises used: Relation.TransGen.trans, 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₁ : σ₁
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₂
d₂ : σ₂
dd : tr d₁ d₂
cd₂ : Reaches₁ f₂ c₂ d₂
⊢ ∃ (b₂ : σ₂), tr d₁ b₂ ∧ Reaches₁ f₂ a₂ b₂

Tactic:
exact ⟨_, dd, ac₂.trans cd₂⟩
-- 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₂
b₁ : σ₁
ab : Reaches₁ f₁ a₁ b₁
single : ∀ {b : σ₁} (ac : b ∈ f₁ a₁), ∃ (b₂ : σ₂), tr b b₂ ∧ Reaches₁ f₂ a₂ b₂
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₂
⊢ ∃ (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₂⟩
-- 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₂
b₁ : σ₁
ab : Reaches f₁ a₁ b₁
inl : ∀ (aa : tr b₁ a₂) (ab : Reaches f₁ b₁ b₁), ∃ (b₂ : σ₂), tr b₁ b₂ ∧ Reaches f₂ a₂ b₂
inr : ∀ (ab : TransGen (fun (a b : σ₁) ↦ b ∈ f₁ a) a₁ b₁), ∃ (b₂ : σ₂), tr b₁ b₂ ∧ Reaches f₂ a₂ b₂
⊢ ∃ (b₂ : σ₂), tr b₁ b₂ ∧ Reaches f₂ a₂ b₂

Tactic:
rcases reflTransGen_iff_eq_or_transGen.1 ab with (rfl | ab)

Premises used: Relation.reflTransGen_iff_eq_or_transGen, Iff.mp, 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₁ : σ₁
aa : tr b₁ a₂
ab : Reaches f₁ b₁ b₁
⊢ ∃ (b₂ : σ₂), tr b₁ b₂ ∧ Reaches f₂ a₂ b₂

Tactic:
⟨_, aa, ReflTransGen.refl⟩

Premises used: Relation.ReflTransGen.refl, 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₁ : σ₁
aa : tr b₁ a₂
ab : Reaches f₁ b₁ b₁
⊢ ∃ (b₂ : σ₂), tr b₁ b₂ ∧ Reaches f₂ a₂ b₂

Tactic:
exact ⟨_, aa, ReflTransGen.refl⟩
-- 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₂
b₁ : σ₁
ab_1 : Reaches f₁ a₁ b₁
ab : TransGen (fun (a b : σ₁) ↦ b ∈ f₁ a) a₁ b₁
inr : ∀ (b₂ : σ₂) (bb : tr b₁ b₂) (h : Reaches₁ f₂ a₂ b₂), ∃ (b₂ : σ₂), tr b₁ b₂ ∧ Reaches f₂ a₂ b₂
⊢ ∃ (b₂ : σ₂), tr b₁ b₂ ∧ Reaches f₂ a₂ b₂

Tactic:
have ⟨b₂, bb, h⟩ := tr_reaches₁ H aa ab
-- 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₂
b₁ : σ₁
ab_1 : Reaches f₁ a₁ b₁
ab : TransGen (fun (a b : σ₁) ↦ b ∈ f₁ a) a₁ b₁
b₂ : σ₂
bb : tr b₁ b₂
h : Reaches₁ f₂ a₂ b₂
⊢ ∃ (b₂ : σ₂), tr b₁ b₂ ∧ Reaches f₂ a₂ b₂

Tactic:
⟨b₂, bb, h.to_reflTransGen⟩

Premises used: And.intro, Exists.intro, Relation.TransGen.to_reflTransGen
-- 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₂
b₁ : σ₁
ab_1 : Reaches f₁ a₁ b₁
ab : TransGen (fun (a b : σ₁) ↦ b ∈ f₁ a) a₁ b₁
b₂ : σ₂
bb : tr b₁ b₂
h : Reaches₁ f₂ a₂ b₂
⊢ ∃ (b₂ : σ₂), tr b₁ b₂ ∧ Reaches f₂ a₂ b₂

Tactic:
exact ⟨b₂, bb, h.to_reflTransGen⟩
-- 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₂
b₂ : σ₂
⊢ ∃ (c₁ : σ₁) (c₂ : σ₂), Reaches f₂ a₂ c₂ ∧ tr c₁ c₂ ∧ Reaches f₁ a₁ c₁

Tactic:
⟨_, _, ReflTransGen.refl, aa, ReflTransGen.refl⟩

Premises used: Relation.ReflTransGen.refl, 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₁ : σ₁
a₂ : σ₂
aa : tr a₁ a₂
b₂ : σ₂
⊢ ∃ (c₁ : σ₁) (c₂ : σ₂), Reaches f₂ a₂ c₂ ∧ tr c₁ c₂ ∧ Reaches f₁ a₁ c₁

Tactic:
exact ⟨_, _, ReflTransGen.refl, aa, ReflTransGen.refl⟩
-- 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₂
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₁
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₁
⊢ ∃ (c₁ : σ₁) (c₂ : σ₂), Reaches f₂ c c₂ ∧ tr c₁ c₂ ∧ Reaches f₁ a₁ c₁

Tactic:
rcases IH with ⟨e₁, e₂, ce, ee, ae⟩
-- 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₂
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₁
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₁
⊢ ∃ (c₁ : σ₁) (c₂ : σ₂), Reaches f₂ c c₂ ∧ tr c₁ c₂ ∧ Reaches f₁ a₁ c₁

Tactic:
rcases ReflTransGen.cases_head ce with (rfl | ⟨d', cd', de⟩)

Premises used: Relation.ReflTransGen.cases_head, rfl
-- 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₂
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
⊢ 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
-- 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₂
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
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₁
⊢ ∃ (c₁ : σ₁) (c₂ : σ₂), Reaches f₂ c c₂ ∧ tr c₁ c₂ ∧ Reaches f₁ a₁ c₁

Tactic:
revert this
-- 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₂
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₁
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₁
⊢ ∀
    (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:
rcases eg : f₁ e₁ with - | g₁
-- 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₂
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₁
tail : ∀ (x : σ₂), tr g₁ x → Reaches₁ f₂ b x → ∃ (c₁ : σ₁) (c₂ : σ₂), Reaches f₂ c c₂ ∧ tr c₁ c₂ ∧ Reaches f₁ a₁ c₁
⊢ ∀
    (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:
simp only [and_imp, exists_imp]

Premises used: and_imp, exists_imp
-- 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₂
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
eg : f₁ e₁ = none
c0 : f₂ b = none
⊢ ∃ (c₁ : σ₁) (c₂ : σ₂), Reaches f₂ c c₂ ∧ tr c₁ c₂ ∧ Reaches f₁ a₁ c₁

Tactic:
cases cd.symm.trans c0

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₂
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₂
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₁
⊢ ∃ (c₁ : σ₁) (c₂ : σ₂), Reaches f₂ c c₂ ∧ tr c₁ c₂ ∧ Reaches f₁ a₁ c₁

Tactic:
rcases TransGen.head'_iff.1 cg with ⟨d', cd', dg⟩

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₁ : σ₁
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₂
⊢ c ∈ f₂ b

Tactic:
cases Option.mem_unique cd cd'

Premises used: Option.mem_unique
-- 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₂
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
⊢ ReflTransGen (fun (a b : σ₂) ↦ b ∈ f₂ a) c g₂

Tactic:
cases Option.mem_unique cd cd'

Premises used: Option.mem_unique
-- 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₂
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₂
cd' : c ∈ f₂ b
dg : ReflTransGen (fun (a b : σ₂) ↦ b ∈ f₂ a) c g₂
⊢ ∃ (c₁ : σ₁) (c₂ : σ₂), Reaches f₂ c c₂ ∧ tr c₁ c₂ ∧ Reaches f₁ a₁ c₁

Tactic:
⟨_, _, dg, gg, ae.tail eg⟩

Premises used: And.intro, Relation.ReflTransGen.tail, 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₁ : σ₁
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₂
cd' : c ∈ f₂ b
dg : ReflTransGen (fun (a b : σ₂) ↦ b ∈ f₂ a) c g₂
⊢ ∃ (c₁ : σ₁) (c₂ : σ₂), Reaches f₂ c c₂ ∧ tr c₁ c₂ ∧ Reaches f₁ a₁ c₁

Tactic:
exact ⟨_, _, dg, gg, ae.tail eg⟩
-- 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₂
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₂
⊢ c ∈ f₂ b

Tactic:
cases Option.mem_unique cd cd'

Premises used: Option.mem_unique
-- 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₂
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
⊢ ReflTransGen (fun (a b : σ₂) ↦ b ∈ f₂ a) c e₂

Tactic:
cases Option.mem_unique cd cd'

Premises used: Option.mem_unique
-- 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₂
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₁
cd' : c ∈ f₂ b
de : ReflTransGen (fun (a b : σ₂) ↦ b ∈ f₂ a) c e₂
⊢ ∃ (c₁ : σ₁) (c₂ : σ₂), Reaches f₂ c c₂ ∧ tr c₁ c₂ ∧ Reaches f₁ a₁ c₁

Tactic:
⟨_, _, de, ee, ae⟩

Premises used: 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₁ : σ₁
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₁
cd' : c ∈ f₂ b
de : ReflTransGen (fun (a b : σ₂) ↦ b ∈ f₂ a) c e₂
⊢ ∃ (c₁ : σ₁) (c₂ : σ₂), Reaches f₂ c c₂ ∧ tr c₁ c₂ ∧ Reaches f₁ a₁ c₁

Tactic:
exact ⟨_, _, de, ee, ae⟩
-- 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₂
b₂ : σ₂
ab : Reaches f₂ a₂ b₂
refl : ∃ (c₁ : σ₁) (c₂ : σ₂), Reaches f₂ a₂ c₂ ∧ tr c₁ c₂ ∧ Reaches f₁ a₁ c₁
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₁
⊢ ∃ (c₁ : σ₁) (c₂ : σ₂), Reaches f₂ b₂ 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⟩

Premises used: and_imp, exists_imp, refl, 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 : 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 : ∀ (b₂ : σ₂) (bb : tr b₁ b₂) (ab : Reaches f₂ a₂ b₂), ∃ (b₂ : σ₂), tr b₁ b₂ ∧ b₂ ∈ eval f₂ a₂
⊢ ∃ (b₂ : σ₂), tr b₁ b₂ ∧ b₂ ∈ eval f₂ a₂

Tactic:
rcases tr_reaches H aa ab with ⟨b₂, bb, ab⟩

Premises used: StateTransition.tr_reaches