awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
P : RegularExpression α
x : List α
zero :
  ∀ (x : List α),
    rmatch RegularExpression.zero x = true ↔ Membership.mem (γ := Language α) (matches' RegularExpression.zero) x
epsilon :
  ∀ (x : List α),
    rmatch RegularExpression.epsilon x = true ↔ Membership.mem (γ := Language α) (matches' RegularExpression.epsilon) x
char : ∀ (a : α) (x : List α), (RegularExpression.char a).rmatch x = true ↔ x ∈ (RegularExpression.char a).matches'
plus :
  ∀ (a a_1 : RegularExpression α) (ih₁ : ∀ (x : List α), a.rmatch x = true ↔ x ∈ a.matches')
    (ih₂ : ∀ (x : List α), a_1.rmatch x = true ↔ x ∈ a_1.matches') (x : List α),
    (a.plus a_1).rmatch x = true ↔ x ∈ (a.plus a_1).matches'
comp :
  ∀ (P Q : RegularExpression α) (ih₁ : ∀ (x : List α), P.rmatch x = true ↔ x ∈ P.matches')
    (ih₂ : ∀ (x : List α), Q.rmatch x = true ↔ x ∈ Q.matches') (x : List α),
    (P.comp Q).rmatch x = true ↔ x ∈ (P.comp Q).matches'
star :
  ∀ (a : RegularExpression α) (ih : ∀ (x : List α), a.rmatch x = true ↔ x ∈ a.matches') (x : List α),
    a.star.rmatch x = true ↔ x ∈ a.star.matches'
⊢ P.rmatch x = true ↔ x ∈ P.matches'

Tactic:
induction P generalizing x with
  | zero =>
    rw [zero_def, zero_rmatch]
    tauto
  | epsilon =>
    rw [one_def, one_rmatch_iff, matches'_epsilon, Language.mem_one]
  | char =>
    rw [char_rmatch_iff]
    rfl
  | plus _ _ ih₁ ih₂ =>
    rw [plus_def, add_rmatch_iff, ih₁, ih₂]
    rfl
  | comp P Q ih₁ ih₂ =>
    simp only [comp_def, mul_rmatch_iff, matches'_mul, Language.mem_mul, *]
    tauto
  | star _ ih =>
    simp only [star_rmatch_iff, matches'_star, ih, Language.mem_kstar_iff_exists_nonempty, and_comm]

Premises used: RegularExpression.matches'_mul, Language.mem_one, RegularExpression.char_rmatch_iff, RegularExpression.comp_def, RegularExpression.char, RegularExpression.comp, Language.mem_kstar_iff_exists_nonempty, and_comm, RegularExpression.matches'_star, RegularExpression.plus, RegularExpression.epsilon, RegularExpression.star_rmatch_iff, RegularExpression.plus_def, RegularExpression.star, Language.mem_mul, RegularExpression.add_rmatch_iff, RegularExpression.zero, RegularExpression.one_def, RegularExpression.mul_rmatch_iff, RegularExpression.one_rmatch_iff, RegularExpression.matches'_epsilon, RegularExpression.zero_rmatch, RegularExpression.zero_def
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
β : Type u_2
f : α → β
P : RegularExpression α
unfold :
  (match (motive := RegularExpression α → RegularExpression β) HPow.hPow (β := ℕ) P 0 with
    | zero => 0
    | epsilon => 1
    | char a => char (f a)
    | R.plus S => map f R + map f S
    | R.comp S => map f R * map f S
    | R.star => (map f R).star) =
    HPow.hPow (α := RegularExpression β) (β := ℕ)
      (match (motive := RegularExpression α → RegularExpression β) P with
        | zero => 0
        | epsilon => 1
        | char a => char (f a)
        | R.plus S => map f R + map f S
        | R.comp S => map f R * map f S
        | R.star => (map f R).star :
        RegularExpression β)
      0
⊢ map f (HPow.hPow (β := ℕ) P 0) = HPow.hPow (β := ℕ) (map f P) 0

Tactic:
unfold map

Premises used: RegularExpression.map
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
β : Type u_2
f : α → β
P : RegularExpression α
⊢ (match (motive := RegularExpression α → RegularExpression β) HPow.hPow (β := ℕ) P 0 with
    | zero => 0
    | epsilon => 1
    | char a => char (f a)
    | R.plus S => map f R + map f S
    | R.comp S => map f R * map f S
    | R.star => (map f R).star) =
    HPow.hPow (α := RegularExpression β) (β := ℕ)
      (match (motive := RegularExpression α → RegularExpression β) P with
        | zero => 0
        | epsilon => 1
        | char a => char (f a)
        | R.plus S => map f R + map f S
        | R.comp S => map f R * map f S
        | R.star => (map f R).star :
        RegularExpression β)
      0

Tactic:
rfl
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
g : β → γ
f : α → β
R S : RegularExpression α
⊢ map g (map f (R + S)) = map (g ∘ f) (R + S)

Tactic:
simp only [map, map_map]

Premises used: RegularExpression.map
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
g : β → γ
f : α → β
R S : RegularExpression α
⊢ map g (map f (R * S)) = map (g ∘ f) (R * S)

Tactic:
simp only [map, map_map]

Premises used: RegularExpression.map
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
g : β → γ
f : α → β
R : RegularExpression α
⊢ map g (map f R.star) = map (g ∘ f) R.star

Tactic:
simp only [map, map_map]

Premises used: RegularExpression.map
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
β : Type u_2
f : α → β
a : α
rw : (Language.map f : (a : Language α) → Language β) (char a).matches' = (map f (char a)).matches'
⊢ (map f (char a)).matches' = (Language.map f : (a : Language α) → Language β) (char a).matches'

Tactic:
rw [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
β : Type u_2
f : α → β
a : α
⊢ (Language.map f : (a : Language α) → Language β) (char a).matches' = (map f (char a)).matches'

Tactic:
image_singleton

Premises used: Set.image_singleton, Set.Mem, List.map, setOf, RegularExpression.matches', Set.image, Language
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
β : Type u_2
f : α → β
a : α
⊢ (Language.map f : (a : Language α) → Language β) (char a).matches' = (map f (char a)).matches'

Tactic:
exact image_singleton

Premises used: Set.image_singleton
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
β : Type u_2
f : α → β
R S : RegularExpression α
⊢ (map f (R + S)).matches' = (Language.map f : (a : Language α) → Language β) (R + S).matches'

Tactic:
simp only [matches'_map, map, matches'_add, map_add]

Premises used: RegularExpression.matches'_add, map_add, RegularExpression.map
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
β : Type u_2
f : α → β
R S : RegularExpression α
⊢ (map f (R * S)).matches' = (Language.map f : (a : Language α) → Language β) (R * S).matches'

Tactic:
simp [matches'_map]
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
β : Type u_2
f : α → β
R : RegularExpression α
⊢ (map f R.star).matches' = (Language.map f : (a : Language α) → Language β) R.star.matches'

Tactic:
simp [matches'_map]
-- Module: Mathlib.Computability.StateTransition
Goal:
σ : Type u_1
f : σ → Option σ
a b c : σ
h : f a = f b
rw rw₁ :
  (∃ b_1 ∈ f b, ReflTransGen (fun (a b : σ) ↦ b ∈ f a) b_1 c) ↔
    ∃ b_1 ∈ f b, ReflTransGen (fun (a b : σ) ↦ b ∈ f a) b_1 c
⊢ (∃ b_1 ∈ f b, ReflTransGen (fun (a b : σ) ↦ b ∈ f a) b_1 c) ↔ ∃ b ∈ f a, ReflTransGen (fun (a b : σ) ↦ b ∈ f a) b c

Tactic:
rw [h]
-- Module: Mathlib.Computability.StateTransition
Goal:
σ : Type u_1
f : σ → Option σ
a b c : σ
hab : Reaches f a b
hac : Reaches f a c
⊢ Reaches f b c ∨ Reaches f c b

Tactic:
ReflTransGen.total_of_right_unique (fun _ _ _ ↦ Option.mem_unique) hab hac

Premises used: Option.mem_unique, Relation.ReflTransGen.total_of_right_unique, StateTransition.Reaches
-- Module: Mathlib.Computability.StateTransition
Goal:
σ : Type u_1
f : σ → Option σ
a b c : σ
h₁ : Reaches₁ f a c
h₂ : b ∈ f a
rcases : ∀ (b' : σ) (hab : b' ∈ f a) (hbc : ReflTransGen (fun (a b : σ) ↦ b ∈ f a) b' c), Reaches f b c
⊢ Reaches f b c

Tactic:
rcases TransGen.head'_iff.1 h₁ with ⟨b', hab, hbc⟩

Premises used: Relation.TransGen.head'_iff, Iff.mp
-- Module: Mathlib.Computability.StateTransition
Goal:
σ : Type u_1
f : σ → Option σ
a b c : σ
h₁ : Reaches₁ f a c
h₂ : b ∈ f a
b' : σ
hab : b' ∈ f a
hbc : ReflTransGen (fun (a b : σ) ↦ b ∈ f a) b' c
⊢ b ∈ f a

Tactic:
cases Option.mem_unique hab h₂

Premises used: Option.mem_unique
-- Module: Mathlib.Computability.StateTransition
Goal:
σ : Type u_1
f : σ → Option σ
a b c : σ
h₁ : Reaches₁ f a c
h₂ : b ∈ f a
b' : σ
hab : b' ∈ f a
hbc : ReflTransGen (fun (a b : σ) ↦ b ∈ f a) b' c
hab₁ : b ∈ f a
⊢ ReflTransGen (fun (a b : σ) ↦ b ∈ f a) b c

Tactic:
cases Option.mem_unique hab h₂

Premises used: Option.mem_unique
-- Module: Mathlib.Computability.StateTransition
Goal:
σ : Type u_1
f : σ → Option σ
a b c : σ
h₁ : Reaches₁ f a c
h₂ hab : b ∈ f a
hbc : ReflTransGen (fun (a b : σ) ↦ b ∈ f a) b c
⊢ Reaches f b c

Tactic:
hbc

Premises used: StateTransition.Reaches
-- Module: Mathlib.Computability.StateTransition
Goal:
σ : Type u_1
f : σ → Option σ
a b c : σ
h₁ : Reaches₁ f a c
h₂ hab : b ∈ f a
hbc : ReflTransGen (fun (a b : σ) ↦ b ∈ f a) b c
⊢ Reaches f b c

Tactic:
exact hbc
-- Module: Mathlib.Computability.StateTransition
Goal:
σ : Type u_1
f : σ → Option σ
a b c : σ
h : b ∈ f a
h₂ : Reaches₀ f b c
⊢ Reaches₀ f a c

Tactic:
(Reaches₀.single h).trans h₂

Premises used: StateTransition.Reaches₀.trans, StateTransition.Reaches₀.single
-- Module: Mathlib.Computability.StateTransition
Goal:
σ : Type u_1
f : σ → Option σ
a b c : σ
h₁ : Reaches₀ f a b
h : c ∈ f b
⊢ Reaches₀ f a c

Tactic:
h₁.trans (Reaches₀.single h)

Premises used: StateTransition.Reaches₀.trans, StateTransition.Reaches₀.single
-- Module: Mathlib.Computability.StateTransition
Goal:
σ : Type u_1
f : σ → Option σ
a b c : σ
h : Reaches₀ f a b
h₂ : c ∈ f b
⊢ Reaches₁ f a c

Tactic:
h _ (TransGen.single h₂)

Premises used: Relation.TransGen.single
-- Module: Mathlib.Computability.StateTransition
Goal:
σ : Type u_2
f : σ → Option σ
b : σ
C : σ → Sort u_1
a : σ
h : b ∈ eval f a
H : (a : σ) → b ∈ eval f a → ((a' : σ) → f a = some a' → C a') → C a
a' : σ
ha' : Membership.mem (γ := Part σ) (PFun.fix (fun (s : σ) ↦ Part.some ((f s).elim (Sum.inl s) Sum.inr)) a') b
h' : (a'' : σ) → Sum.inr a'' ∈ Part.some ((f a').elim (Sum.inl a') Sum.inr) → C a''
b' : σ
e : f a' = some b'
rw : Sum.inr b' = (some b').elim (Sum.inl a') Sum.inr
⊢ Sum.inr b' = (f a').elim (Sum.inl a') Sum.inr

Tactic:
rw [e]
-- Module: Mathlib.Computability.StateTransition
Goal:
σ : Type u_2
f : σ → Option σ
b : σ
C : σ → Sort u_1
a : σ
h : b ∈ eval f a
H : (a : σ) → b ∈ eval f a → ((a' : σ) → f a = some a' → C a') → C a
a' : σ
ha' : Membership.mem (γ := Part σ) (PFun.fix (fun (s : σ) ↦ Part.some ((f s).elim (Sum.inl s) Sum.inr)) a') b
h' : (a'' : σ) → Sum.inr a'' ∈ Part.some ((f a').elim (Sum.inl a') Sum.inr) → C a''
b' : σ
e : f a' = some b'
⊢ Sum.inr b' = (some b').elim (Sum.inl a') Sum.inr

Tactic:
rfl
-- Module: Mathlib.Computability.StateTransition
Goal:
σ : Type u_1
f : σ → Option σ
a b : σ
⊢ b ∈ eval f a ↔ Reaches f a b ∧ f b = none

Tactic:
⟨fun h ↦ ?_, fun ⟨h₁, h₂⟩ ↦ ?_⟩

Premises used: Membership.mem, _private.0.StateTransition.mem_eval.match_1, Iff.intro, StateTransition.eval
-- Module: Mathlib.Computability.StateTransition
Goal:
σ : Type u_1
f : σ → Option σ
a b : σ
refine_1 : ∀ (h : b ∈ eval f a), Reaches f a b ∧ f b = none
refine_2 : Reaches f a b ∧ f b = none → ∀ (h₁ : Reaches f a b) (h₂ : f b = none), b ∈ eval f a
⊢ b ∈ eval f a ↔ Reaches f a b ∧ f b = none

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨h₁, h₂⟩ ↦ ?_⟩
-- Module: Mathlib.Computability.StateTransition
Goal:
σ : Type u_1
f : σ → Option σ
a b : σ
h : b ∈ eval f a
⊢ Reaches f a b ∧ f b = none

Tactic:
evalInduction h fun a h IH ↦ ?_

Premises used: StateTransition.evalInduction
-- Module: Mathlib.Computability.StateTransition
Goal:
σ : Type u_1
f : σ → Option σ
a b : σ
h : b ∈ eval f a
refine_1 :
  ∀ (a : σ) (h : b ∈ eval f a) (IH : ∀ (a' : σ), f a = some a' → Reaches f a' b ∧ f b = none),
    Reaches f a b ∧ f b = none
⊢ Reaches f a b ∧ f b = none

Tactic:
refine evalInduction h fun a h IH ↦ ?_
-- Module: Mathlib.Computability.StateTransition
Goal:
σ : Type u_1
f : σ → Option σ
a_1 b : σ
h_1 : b ∈ eval f a_1
a : σ
h : b ∈ eval f a
IH : ∀ (a' : σ), f a = some a' → Reaches f a' b ∧ f b = none
refine_1 : ∀ (e : f a = none), Reaches f a b ∧ f b = none
refine_1₁ : ∀ (a' : σ) (e : f a = some a'), Reaches f a b ∧ f b = none
⊢ Reaches f a b ∧ f b = none

Tactic:
rcases e : f a with - | a'
-- Module: Mathlib.Computability.StateTransition
Goal:
σ : Type u_1
f : σ → Option σ
a_1 b : σ
h_1 : b ∈ eval f a_1
a : σ
h : b ∈ eval f a
IH : ∀ (a' : σ), f a = some a' → Reaches f a' b ∧ f b = none
e : f a = none
rw : Eq (α := σ ⊕ σ) (Sum.inl a) (Option.elim none (Sum.inl a) Sum.inr)
⊢ Sum.inl a = (f a).elim (Sum.inl a) Sum.inr

Tactic:
rw [e]
-- Module: Mathlib.Computability.StateTransition
Goal:
σ : Type u_1
f : σ → Option σ
a_1 b : σ
h_1 : b ∈ eval f a_1
a : σ
h : b ∈ eval f a
IH : ∀ (a' : σ), f a = some a' → Reaches f a' b ∧ f b = none
e : f a = none
⊢ Eq (α := σ ⊕ σ) (Sum.inl a) (Option.elim none (Sum.inl a) Sum.inr)

Tactic:
rfl
-- Module: Mathlib.Computability.StateTransition
Goal:
σ : Type u_1
f : σ → Option σ
a_1 b : σ
h_1 : b ∈ eval f a_1
a : σ
h : b ∈ eval f a
IH : ∀ (a' : σ), f a = some a' → Reaches f a' b ∧ f b = none
e : f a = none
refine_1 : Reaches f a a ∧ f a = none
⊢ Reaches f a b ∧ f b = none

Tactic:
rw [Part.mem_unique h
          (PFun.mem_fix_iff.2 <| Or.inl <| Part.mem_some_iff.2 <| by rw [e]; rfl)]

Premises used: Iff.mpr, Part.mem_some_iff, Or.inl, PFun.mem_fix_iff, Part.mem_unique
-- Module: Mathlib.Computability.StateTransition
Goal:
σ : Type u_1
f : σ → Option σ
a_1 b : σ
h_1 : b ∈ eval f a_1
a : σ
h : b ∈ eval f a
IH : ∀ (a' : σ), f a = some a' → Reaches f a' b ∧ f b = none
e : f a = none
⊢ Reaches f a a ∧ f a = none

Tactic:
⟨ReflTransGen.refl, e⟩

Premises used: Relation.ReflTransGen.refl, And.intro
-- Module: Mathlib.Computability.StateTransition
Goal:
σ : Type u_1
f : σ → Option σ
a_1 b : σ
h_1 : b ∈ eval f a_1
a : σ
h : b ∈ eval f a
IH : ∀ (a' : σ), f a = some a' → Reaches f a' b ∧ f b = none
e : f a = none
⊢ Reaches f a a ∧ f a = none

Tactic:
exact ⟨ReflTransGen.refl, e⟩
-- Module: Mathlib.Computability.StateTransition
Goal:
σ : Type u_1
f : σ → Option σ
a_1 b : σ
h_1 : b ∈ eval f a_1
a : σ
h : b ∈ eval f a
IH : ∀ (a' : σ), f a = some a' → Reaches f a' b ∧ f b = none
a' : σ
e : f a = some a'
refine_1 : ∀ (h : Sum.inl b ∈ Part.some ((f a).elim (Sum.inl a) Sum.inr)), Reaches f a b ∧ f b = none
refine_1₁ :
  ∀ (w : σ) (h : Sum.inr w ∈ Part.some ((f a).elim (Sum.inl a) Sum.inr)),
    Membership.mem (γ := Part σ) (PFun.fix (fun (s : σ) ↦ Part.some ((f s).elim (Sum.inl s) Sum.inr)) w) b →
      Reaches f a b ∧ f b = none
⊢ Reaches f a b ∧ f b = none

Tactic:
rcases PFun.mem_fix_iff.1 h with (h | ⟨_, h, _⟩)

Premises used: Iff.mp, PFun.mem_fix_iff
-- Module: Mathlib.Computability.StateTransition
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.inl b ∈ Part.some ((f a).elim (Sum.inl a) Sum.inr)
⊢ Sum.inl b ∈ Part.some ((some a').elim (Sum.inl a) Sum.inr)

Tactic:
rw [e] at h
-- Module: Mathlib.Computability.StateTransition
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'
w : σ
h : Sum.inr w ∈ Part.some ((f 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)) w) b
⊢ Sum.inr w ∈ Part.some ((some a').elim (Sum.inl a) Sum.inr)

Tactic:
rw [e] at h
-- Module: Mathlib.Computability.StateTransition
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'
w : σ
h : Sum.inr w ∈ Part.some ((f 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)) w) b
h₁ : Sum.inr w ∈ Part.some ((some a').elim (Sum.inl a) Sum.inr)
⊢ Membership.mem (γ := Part σ) (PFun.fix (fun (s : σ) ↦ Part.some ((f s).elim (Sum.inl s) Sum.inr)) w) b

Tactic:
rw [e] at h
-- Module: Mathlib.Computability.StateTransition
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.inl b ∈ Part.some ((some a').elim (Sum.inl a) Sum.inr)
⊢ Reaches f a b ∧ f b = none

Tactic:
cases Part.mem_some_iff.1 h

Premises used: Part.mem_some_iff, Iff.mp
-- Module: Mathlib.Computability.StateTransition
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'
w : σ
h : Sum.inr w ∈ 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)) w) b
⊢ Sum.inr a' ∈ Part.some ((some a').elim (Sum.inl a) Sum.inr)

Tactic:
cases Part.mem_some_iff.1 h

Premises used: Part.mem_some_iff, Iff.mp
-- Module: Mathlib.Computability.StateTransition
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'
w : σ
h : Sum.inr w ∈ 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)) w) b
h₁ : Sum.inr a' ∈ Part.some ((some a').elim (Sum.inl a) Sum.inr)
⊢ Membership.mem (γ := Part σ) (PFun.fix (fun (s : σ) ↦ Part.some ((f s).elim (Sum.inl s) Sum.inr)) a') b

Tactic:
cases Part.mem_some_iff.1 h

Premises used: Part.mem_some_iff, Iff.mp
-- Module: Mathlib.Computability.StateTransition
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

Tactic:
obtain ⟨h₁, h₂⟩ := IH a' e
-- Module: Mathlib.Computability.StateTransition
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
⊢ f b = none

Tactic:
obtain ⟨h₁, h₂⟩ := IH a' e
-- Module: Mathlib.Computability.StateTransition
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
h₂ : f b = none
⊢ Reaches f a b ∧ f b = none

Tactic:
⟨ReflTransGen.head e h₁, h₂⟩

Premises used: Relation.ReflTransGen.head, And.intro
-- Module: Mathlib.Computability.StateTransition
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
h₂ : f b = none
⊢ Reaches f a b ∧ f b = none

Tactic:
exact ⟨ReflTransGen.head e h₁, h₂⟩
-- Module: Mathlib.Computability.StateTransition
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

Tactic:
ReflTransGen.head_induction_on h₁ ?_ fun h _ IH ↦ ?_

Premises used: Relation.ReflTransGen.head_induction_on
-- Module: Mathlib.Computability.StateTransition
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
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
⊢ b ∈ eval f a

Tactic:
refine ReflTransGen.head_induction_on h₁ ?_ fun h _ IH ↦ ?_
-- Module: Mathlib.Computability.StateTransition
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

Tactic:
PFun.mem_fix_iff.2 (Or.inl ?_)

Premises used: Iff.mpr, Or.inl, PFun.mem_fix_iff, StateTransition.eval
-- Module: Mathlib.Computability.StateTransition
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 : Sum.inl b ∈ Part.some ((f b).elim (Sum.inl b) Sum.inr)
⊢ b ∈ eval f b

Tactic:
refine PFun.mem_fix_iff.2 (Or.inl ?_)

Premises used: Iff.mpr, Or.inl, PFun.mem_fix_iff
-- Module: Mathlib.Computability.StateTransition
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 : Membership.mem (γ := Part (σ ⊕ σ)) (Part.some (Option.elim none (Sum.inl b) Sum.inr)) (Sum.inl b)
⊢ Sum.inl b ∈ Part.some ((f b).elim (Sum.inl b) Sum.inr)

Tactic:
rw [h₂]
-- Module: Mathlib.Computability.StateTransition
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
⊢ Membership.mem (γ := Part (σ ⊕ σ)) (Part.some (Option.elim none (Sum.inl b) Sum.inr)) (Sum.inl b)

Tactic:
apply Part.mem_some

Premises used: Part.mem_some
-- Module: Mathlib.Computability.StateTransition
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

Tactic:
PFun.mem_fix_iff.2 (Or.inr ⟨_, ?_, IH⟩)

Premises used: Iff.mpr, And.intro, Exists.intro, PFun.mem_fix_iff, StateTransition.eval, Or.inr
-- Module: Mathlib.Computability.StateTransition
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
refine_2 : Sum.inr c ∈ Part.some ((f a_1).elim (Sum.inl a_1) Sum.inr)
⊢ b ∈ eval f a_1

Tactic:
refine PFun.mem_fix_iff.2 (Or.inr ⟨_, ?_, IH⟩)

Premises used: Iff.mpr, And.intro, Exists.intro, PFun.mem_fix_iff, Or.inr
-- Module: Mathlib.Computability.StateTransition
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
refine_2 : Sum.inr c ∈ Part.some ((some c).elim (Sum.inl a_1) Sum.inr)
⊢ Sum.inr c ∈ Part.some ((f a_1).elim (Sum.inl a_1) Sum.inr)

Tactic:
rw [h]
-- Module: Mathlib.Computability.StateTransition
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 ((some c).elim (Sum.inl a_1) Sum.inr)

Tactic:
apply Part.mem_some

Premises used: Part.mem_some
-- Module: Mathlib.Computability.StateTransition
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
⊢ Reaches f a b

Tactic:
let ⟨_, b0⟩ := mem_eval.1 h
-- Module: Mathlib.Computability.StateTransition
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
⊢ f b = none

Tactic:
let ⟨_, b0⟩ := mem_eval.1 h
-- Module: Mathlib.Computability.StateTransition
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
let : ∀ (b' : σ) (h' : b' ∈ f b), ReflTransGen (fun (a b : σ) ↦ b ∈ f a) b' c → False
⊢ False

Tactic:
let ⟨b', h', _⟩ := TransGen.head'_iff.1 bc
-- Module: Mathlib.Computability.StateTransition
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
b' : σ
h' : b' ∈ f b
right : ReflTransGen (fun (a b : σ) ↦ b ∈ f a) b' c
⊢ False

Tactic:
cases b0.symm.trans h'

Premises used: Eq.symm, Eq.trans