mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case bit1.bit0.lt
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (Ordering.casesOn Ordering.lt Ordering.lt Ordering.gt Ordering.gt).swap =
    Ordering.casesOn Ordering.lt.swap Ordering.lt Ordering.lt Ordering.gt

pp: case bit1.bit0.eq
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (Ordering.casesOn Ordering.eq Ordering.lt Ordering.gt Ordering.gt).swap =
    Ordering.casesOn Ordering.eq.swap Ordering.lt Ordering.lt Ordering.gt

pp: case bit1.bit0.gt
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (Ordering.casesOn Ordering.gt Ordering.lt Ordering.gt Ordering.gt).swap =
    Ordering.casesOn Ordering.gt.swap Ordering.lt Ordering.lt Ordering.gt

pp: case bit0.bit1.lt
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (Ordering.casesOn Ordering.lt Ordering.lt Ordering.lt Ordering.gt).swap =
    Ordering.casesOn Ordering.lt.swap Ordering.lt Ordering.gt Ordering.gt

pp: case bit0.bit1.eq
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (Ordering.casesOn Ordering.eq Ordering.lt Ordering.lt Ordering.gt).swap =
    Ordering.casesOn Ordering.eq.swap Ordering.lt Ordering.gt Ordering.gt

pp: case bit0.bit1.gt
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (Ordering.casesOn Ordering.gt Ordering.lt Ordering.lt Ordering.gt).swap =
    Ordering.casesOn Ordering.gt.swap Ordering.lt Ordering.gt Ordering.gt

Tactic:
<;>

Goal state after:
case bit1.bit0.lt
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (Ordering.casesOn Ordering.lt Ordering.lt Ordering.gt Ordering.gt).swap =
    Ordering.casesOn Ordering.lt.swap Ordering.lt Ordering.lt Ordering.gt

case bit1.bit0.eq
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (Ordering.casesOn Ordering.eq Ordering.lt Ordering.gt Ordering.gt).swap =
    Ordering.casesOn Ordering.eq.swap Ordering.lt Ordering.lt Ordering.gt

case bit1.bit0.gt
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (Ordering.casesOn Ordering.gt Ordering.lt Ordering.gt Ordering.gt).swap =
    Ordering.casesOn Ordering.gt.swap Ordering.lt Ordering.lt Ordering.gt

case bit0.bit1.lt
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (Ordering.casesOn Ordering.lt Ordering.lt Ordering.lt Ordering.gt).swap =
    Ordering.casesOn Ordering.lt.swap Ordering.lt Ordering.gt Ordering.gt

case bit0.bit1.eq
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (Ordering.casesOn Ordering.eq Ordering.lt Ordering.lt Ordering.gt).swap =
    Ordering.casesOn Ordering.eq.swap Ordering.lt Ordering.gt Ordering.gt

case bit0.bit1.gt
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (Ordering.casesOn Ordering.gt Ordering.lt Ordering.lt Ordering.gt).swap =
    Ordering.casesOn Ordering.gt.swap Ordering.lt Ordering.gt Ordering.gt
Module: Mathlib.Computability.NFA

Goal state before:
pp: case mpr
α : Type u
σ : Type v
M : NFA α σ
S T : Set σ
x : List α
⊢ x ∈ M.acceptsFrom S ∪ M.acceptsFrom T → ∃ s ∈ M.accept, s ∈ M.evalFrom S x ∨ s ∈ M.evalFrom T x

Tactic:
rintro (⟨s, hs, h⟩ | ⟨s, hs, h⟩) <;> exists s

Goal state after:
case mpr.inl
α : Type u
σ : Type v
M : NFA α σ
S T : Set σ
x : List α
s : σ
hs : s ∈ M.accept
h : s ∈ M.evalFrom S x
⊢ s ∈ M.accept ∧ (s ∈ M.evalFrom S x ∨ s ∈ M.evalFrom T x)

case mpr.inr
α : Type u
σ : Type v
M : NFA α σ
S T : Set σ
x : List α
s : σ
hs : s ∈ M.accept
h : s ∈ M.evalFrom T x
⊢ s ∈ M.accept ∧ (s ∈ M.evalFrom S x ∨ s ∈ M.evalFrom T x)
Module: Mathlib.Computability.NFA

Goal state before:
pp: case mpr.inl
α : Type u
σ : Type v
M : NFA α σ
S T : Set σ
x : List α
s : σ
hs : s ∈ M.accept
h : s ∈ M.evalFrom S x
⊢ s ∈ M.accept ∧ (s ∈ M.evalFrom S x ∨ s ∈ M.evalFrom T x)

pp: case mpr.inr
α : Type u
σ : Type v
M : NFA α σ
S T : Set σ
x : List α
s : σ
hs : s ∈ M.accept
h : s ∈ M.evalFrom T x
⊢ s ∈ M.accept ∧ (s ∈ M.evalFrom S x ∨ s ∈ M.evalFrom T x)

Tactic:
<;>

Goal state after:
case mpr.inl
α : Type u
σ : Type v
M : NFA α σ
S T : Set σ
x : List α
s : σ
hs : s ∈ M.accept
h : s ∈ M.evalFrom S x
⊢ s ∈ M.accept ∧ (s ∈ M.evalFrom S x ∨ s ∈ M.evalFrom T x)

case mpr.inr
α : Type u
σ : Type v
M : NFA α σ
S T : Set σ
x : List α
s : σ
hs : s ∈ M.accept
h : s ∈ M.evalFrom T x
⊢ s ∈ M.accept ∧ (s ∈ M.evalFrom S x ∨ s ∈ M.evalFrom T x)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case lt
a b : PosNum
⊢ Ordering.casesOn Ordering.lt (↑a < ↑b) (a = b) (↑b < ↑a) →
    Ordering.rec (↑a + ↑a < ↑b + ↑b) (a.bit0 = b.bit0) (↑b + ↑b < ↑a + ↑a) Ordering.lt

pp: case eq
a b : PosNum
⊢ Ordering.casesOn Ordering.eq (↑a < ↑b) (a = b) (↑b < ↑a) →
    Ordering.rec (↑a + ↑a < ↑b + ↑b) (a.bit0 = b.bit0) (↑b + ↑b < ↑a + ↑a) Ordering.eq

pp: case gt
a b : PosNum
⊢ Ordering.casesOn Ordering.gt (↑a < ↑b) (a = b) (↑b < ↑a) →
    Ordering.rec (↑a + ↑a < ↑b + ↑b) (a.bit0 = b.bit0) (↑b + ↑b < ↑a + ↑a) Ordering.gt

Tactic:
<;>

Goal state after:
case lt
a b : PosNum
⊢ Ordering.casesOn Ordering.lt (↑a < ↑b) (a = b) (↑b < ↑a) →
    Ordering.rec (↑a + ↑a < ↑b + ↑b) (a.bit0 = b.bit0) (↑b + ↑b < ↑a + ↑a) Ordering.lt

case eq
a b : PosNum
⊢ Ordering.casesOn Ordering.eq (↑a < ↑b) (a = b) (↑b < ↑a) →
    Ordering.rec (↑a + ↑a < ↑b + ↑b) (a.bit0 = b.bit0) (↑b + ↑b < ↑a + ↑a) Ordering.eq

case gt
a b : PosNum
⊢ Ordering.casesOn Ordering.gt (↑a < ↑b) (a = b) (↑b < ↑a) →
    Ordering.rec (↑a + ↑a < ↑b + ↑b) (a.bit0 = b.bit0) (↑b + ↑b < ↑a + ↑a) Ordering.gt
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case lt
a b : PosNum
⊢ ↑a < ↑b → ↑a + ↑a < ↑b + ↑b

pp: case eq
a b : PosNum
⊢ a = b → a.bit0 = b.bit0

pp: case gt
a b : PosNum
⊢ ↑b < ↑a → ↑b + ↑b < ↑a + ↑a

Tactic:
<;>

Goal state after:
case lt
a b : PosNum
⊢ ↑a < ↑b → ↑a + ↑a < ↑b + ↑b

case eq
a b : PosNum
⊢ a = b → a.bit0 = b.bit0

case gt
a b : PosNum
⊢ ↑b < ↑a → ↑b + ↑b < ↑a + ↑a
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: case cons.none
α : Type u_1
tl : List (Option α)
hl : tl.reduceOption.length = (filter Option.isSome tl).length
⊢ (none :: tl).reduceOption.length = (filter Option.isSome (none :: tl)).length

pp: case cons.some
α : Type u_1
tl : List (Option α)
hl : tl.reduceOption.length = (filter Option.isSome tl).length
val✝ : α
⊢ (some val✝ :: tl).reduceOption.length = (filter Option.isSome (some val✝ :: tl)).length

Tactic:
<;>

Goal state after:
case cons.none
α : Type u_1
tl : List (Option α)
hl : tl.reduceOption.length = (filter Option.isSome tl).length
⊢ (none :: tl).reduceOption.length = (filter Option.isSome (none :: tl)).length

case cons.some
α : Type u_1
tl : List (Option α)
hl : tl.reduceOption.length = (filter Option.isSome tl).length
val✝ : α
⊢ (some val✝ :: tl).reduceOption.length = (filter Option.isSome (some val✝ :: tl)).length
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case lt
a b : PosNum
⊢ Ordering.casesOn Ordering.lt (↑a < ↑b) (a = b) (↑b < ↑a) →
    Ordering.rec (↑a + ↑a < ↑b + ↑b + 1) (a.bit0 = b.bit1) (↑b + ↑b + 1 < ↑a + ↑a)
      (Ordering.rec Ordering.lt Ordering.lt Ordering.gt Ordering.lt)

pp: case eq
a b : PosNum
⊢ Ordering.casesOn Ordering.eq (↑a < ↑b) (a = b) (↑b < ↑a) →
    Ordering.rec (↑a + ↑a < ↑b + ↑b + 1) (a.bit0 = b.bit1) (↑b + ↑b + 1 < ↑a + ↑a)
      (Ordering.rec Ordering.lt Ordering.lt Ordering.gt Ordering.eq)

pp: case gt
a b : PosNum
⊢ Ordering.casesOn Ordering.gt (↑a < ↑b) (a = b) (↑b < ↑a) →
    Ordering.rec (↑a + ↑a < ↑b + ↑b + 1) (a.bit0 = b.bit1) (↑b + ↑b + 1 < ↑a + ↑a)
      (Ordering.rec Ordering.lt Ordering.lt Ordering.gt Ordering.gt)

Tactic:
<;>

Goal state after:
case lt
a b : PosNum
⊢ Ordering.casesOn Ordering.lt (↑a < ↑b) (a = b) (↑b < ↑a) →
    Ordering.rec (↑a + ↑a < ↑b + ↑b + 1) (a.bit0 = b.bit1) (↑b + ↑b + 1 < ↑a + ↑a)
      (Ordering.rec Ordering.lt Ordering.lt Ordering.gt Ordering.lt)

case eq
a b : PosNum
⊢ Ordering.casesOn Ordering.eq (↑a < ↑b) (a = b) (↑b < ↑a) →
    Ordering.rec (↑a + ↑a < ↑b + ↑b + 1) (a.bit0 = b.bit1) (↑b + ↑b + 1 < ↑a + ↑a)
      (Ordering.rec Ordering.lt Ordering.lt Ordering.gt Ordering.eq)

case gt
a b : PosNum
⊢ Ordering.casesOn Ordering.gt (↑a < ↑b) (a = b) (↑b < ↑a) →
    Ordering.rec (↑a + ↑a < ↑b + ↑b + 1) (a.bit0 = b.bit1) (↑b + ↑b + 1 < ↑a + ↑a)
      (Ordering.rec Ordering.lt Ordering.lt Ordering.gt Ordering.gt)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case lt
a b : PosNum
⊢ ↑a < ↑b → ↑a + ↑a < ↑b + ↑b + 1

pp: case eq
a b : PosNum
⊢ a = b → ↑a + ↑a < ↑b + ↑b + 1

pp: case gt
a b : PosNum
⊢ ↑b < ↑a → ↑b + ↑b + 1 < ↑a + ↑a

Tactic:
<;>

Goal state after:
case lt
a b : PosNum
⊢ ↑a < ↑b → ↑a + ↑a < ↑b + ↑b + 1

case eq
a b : PosNum
⊢ a = b → ↑a + ↑a < ↑b + ↑b + 1

case gt
a b : PosNum
⊢ ↑b < ↑a → ↑b + ↑b + 1 < ↑a + ↑a
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
ι : Sort u_1
s : ι → Set σ
⊢ M.acceptsFrom (⋃ i, s i) = ⋃ i, M.acceptsFrom (s i)

Tactic:
ext x
  simp only [acceptsFrom, evalFrom_iUnion, mem_iUnion]
  simp_rw [↑mem_iUnion, ↑mem_ofPred_eq]; tauto

Goal state after:
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: case none
α : Type u_1
⊢ [none].reduceOption = none.toList

pp: case some
α : Type u_1
val✝ : α
⊢ [some val✝].reduceOption = (some val✝).toList

Tactic:
<;>

Goal state after:
case none
α : Type u_1
⊢ [none].reduceOption = none.toList

case some
α : Type u_1
val✝ : α
⊢ [some val✝].reduceOption = (some val✝).toList
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: case nil.none
α : Type u_1
⊢ ([].concat none).reduceOption = [].reduceOption ++ none.toList

pp: case nil.some
α : Type u_1
val✝ : α
⊢ ([].concat (some val✝)).reduceOption = [].reduceOption ++ (some val✝).toList

Tactic:
<;>

Goal state after:
case nil.none
α : Type u_1
⊢ ([].concat none).reduceOption = [].reduceOption ++ none.toList

case nil.some
α : Type u_1
val✝ : α
⊢ ([].concat (some val✝)).reduceOption = [].reduceOption ++ (some val✝).toList
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: case cons.none
α : Type u_1
tl : List (Option α)
x : Option α
hl : ∀ (x : Option α), tl.reduceOption ++ [x].reduceOption = tl.reduceOption ++ x.toList
⊢ ((none :: tl).concat x).reduceOption = (none :: tl).reduceOption ++ x.toList

pp: case cons.some
α : Type u_1
tl : List (Option α)
x : Option α
hl : ∀ (x : Option α), tl.reduceOption ++ [x].reduceOption = tl.reduceOption ++ x.toList
val✝ : α
⊢ ((some val✝ :: tl).concat x).reduceOption = (some val✝ :: tl).reduceOption ++ x.toList

Tactic:
<;>

Goal state after:
case cons.none
α : Type u_1
tl : List (Option α)
x : Option α
hl : ∀ (x : Option α), tl.reduceOption ++ [x].reduceOption = tl.reduceOption ++ x.toList
⊢ ((none :: tl).concat x).reduceOption = (none :: tl).reduceOption ++ x.toList

case cons.some
α : Type u_1
tl : List (Option α)
x : Option α
hl : ∀ (x : Option α), tl.reduceOption ++ [x].reduceOption = tl.reduceOption ++ x.toList
val✝ : α
⊢ ((some val✝ :: tl).concat x).reduceOption = (some val✝ :: tl).reduceOption ++ x.toList
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: case base
α : Type u
σ : Type v
M : εNFA α σ
s s✝ : σ
a✝ : s✝ ∈ ∅
⊢ False

pp: case step
α : Type u
σ : Type v
M : εNFA α σ
s s✝ t✝ : σ
a✝¹ : t✝ ∈ M.step s✝ none
a✝ : M.εClosure ∅ s✝
a_ih✝ : False
⊢ False

Tactic:
<;>

Goal state after:
case base
α : Type u
σ : Type v
M : εNFA α σ
s s✝ : σ
a✝ : s✝ ∈ ∅
⊢ False

case step
α : Type u
σ : Type v
M : εNFA α σ
s s✝ t✝ : σ
a✝¹ : t✝ ∈ M.step s✝ none
a✝ : M.εClosure ∅ s✝
a_ih✝ : False
⊢ False
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: case base
α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
s t : σ
left✝ : t ∈ S
s✝ : σ
a✝ : s✝ ∈ {t}
⊢ s✝ ∈ M.εClosure S

pp: case step
α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
s t : σ
left✝ : t ∈ S
s✝ t✝ : σ
a✝¹ : t✝ ∈ M.step s✝ none
a✝ : M.εClosure {t} s✝
a_ih✝ : s✝ ∈ M.εClosure S
⊢ t✝ ∈ M.εClosure S

Tactic:
<;>

Goal state after:
case base
α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
s t : σ
left✝ : t ∈ S
s✝ : σ
a✝ : s✝ ∈ {t}
⊢ s✝ ∈ M.εClosure S

case step
α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
s t : σ
left✝ : t ∈ S
s✝ t✝ : σ
a✝¹ : t✝ ∈ M.step s✝ none
a✝ : M.εClosure {t} s✝
a_ih✝ : s✝ ∈ M.εClosure S
⊢ t✝ ∈ M.εClosure S
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: case base
α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
s s✝ : σ
left✝ : s✝ ∈ S
⊢ s✝ ∈ M.εClosure S

pp: case step
α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
s t : σ
left✝ : t ∈ S
s✝ t✝ : σ
a✝¹ : t✝ ∈ M.step s✝ none
a✝ : M.εClosure {t} s✝
a_ih✝ : s✝ ∈ M.εClosure S
⊢ t✝ ∈ M.εClosure S

Tactic:
<;>

Goal state after:
case base
α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
s s✝ : σ
left✝ : s✝ ∈ S
⊢ s✝ ∈ M.εClosure S

case step
α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
s t : σ
left✝ : t ∈ S
s✝ t✝ : σ
a✝¹ : t✝ ∈ M.step s✝ none
a✝ : M.εClosure {t} s✝
a_ih✝ : s✝ ∈ M.εClosure S
⊢ t✝ ∈ M.εClosure S
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case lt
a b : PosNum
⊢ Ordering.casesOn Ordering.lt (↑a < ↑b) (a = b) (↑b < ↑a) →
    Ordering.rec (↑a + ↑a + 1 < ↑b + ↑b) (a.bit1 = b.bit0) (↑b + ↑b < ↑a + ↑a + 1)
      (Ordering.rec Ordering.lt Ordering.gt Ordering.gt Ordering.lt)

pp: case eq
a b : PosNum
⊢ Ordering.casesOn Ordering.eq (↑a < ↑b) (a = b) (↑b < ↑a) →
    Ordering.rec (↑a + ↑a + 1 < ↑b + ↑b) (a.bit1 = b.bit0) (↑b + ↑b < ↑a + ↑a + 1)
      (Ordering.rec Ordering.lt Ordering.gt Ordering.gt Ordering.eq)

pp: case gt
a b : PosNum
⊢ Ordering.casesOn Ordering.gt (↑a < ↑b) (a = b) (↑b < ↑a) →
    Ordering.rec (↑a + ↑a + 1 < ↑b + ↑b) (a.bit1 = b.bit0) (↑b + ↑b < ↑a + ↑a + 1)
      (Ordering.rec Ordering.lt Ordering.gt Ordering.gt Ordering.gt)

Tactic:
<;>

Goal state after:
case lt
a b : PosNum
⊢ Ordering.casesOn Ordering.lt (↑a < ↑b) (a = b) (↑b < ↑a) →
    Ordering.rec (↑a + ↑a + 1 < ↑b + ↑b) (a.bit1 = b.bit0) (↑b + ↑b < ↑a + ↑a + 1)
      (Ordering.rec Ordering.lt Ordering.gt Ordering.gt Ordering.lt)

case eq
a b : PosNum
⊢ Ordering.casesOn Ordering.eq (↑a < ↑b) (a = b) (↑b < ↑a) →
    Ordering.rec (↑a + ↑a + 1 < ↑b + ↑b) (a.bit1 = b.bit0) (↑b + ↑b < ↑a + ↑a + 1)
      (Ordering.rec Ordering.lt Ordering.gt Ordering.gt Ordering.eq)

case gt
a b : PosNum
⊢ Ordering.casesOn Ordering.gt (↑a < ↑b) (a = b) (↑b < ↑a) →
    Ordering.rec (↑a + ↑a + 1 < ↑b + ↑b) (a.bit1 = b.bit0) (↑b + ↑b < ↑a + ↑a + 1)
      (Ordering.rec Ordering.lt Ordering.gt Ordering.gt Ordering.gt)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case lt
a b : PosNum
⊢ ↑a < ↑b → ↑a + ↑a + 1 < ↑b + ↑b

pp: case eq
a b : PosNum
⊢ a = b → ↑b + ↑b < ↑a + ↑a + 1

pp: case gt
a b : PosNum
⊢ ↑b < ↑a → ↑b + ↑b < ↑a + ↑a + 1

Tactic:
<;>

Goal state after:
case lt
a b : PosNum
⊢ ↑a < ↑b → ↑a + ↑a + 1 < ↑b + ↑b

case eq
a b : PosNum
⊢ a = b → ↑b + ↑b < ↑a + ↑a + 1

case gt
a b : PosNum
⊢ ↑b < ↑a → ↑b + ↑b < ↑a + ↑a + 1
Module: Mathlib.Computability.NFA

Goal state before:
pp: case mp
α : Type u
σ : Type v
M : NFA α σ
x : List α
⊢ M.toDFA.eval x ∈ M.toDFA.accept → ∃ S ∈ M.accept, S ∈ M.evalFrom M.start x

pp: case mpr
α : Type u
σ : Type v
M : NFA α σ
x : List α
⊢ (∃ S ∈ M.accept, S ∈ M.evalFrom M.start x) → M.toDFA.eval x ∈ M.toDFA.accept

Tactic:
<;>

Goal state after:
case mp
α : Type u
σ : Type v
M : NFA α σ
x : List α
⊢ M.toDFA.eval x ∈ M.toDFA.accept → ∃ S ∈ M.accept, S ∈ M.evalFrom M.start x

case mpr
α : Type u
σ : Type v
M : NFA α σ
x : List α
⊢ (∃ S ∈ M.accept, S ∈ M.evalFrom M.start x) → M.toDFA.eval x ∈ M.toDFA.accept
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case lt
a b : PosNum
⊢ Ordering.casesOn Ordering.lt (↑a < ↑b) (a = b) (↑b < ↑a) →
    Ordering.rec (↑a + ↑a + 1 < ↑b + ↑b + 1) (a.bit1 = b.bit1) (↑b + ↑b + 1 < ↑a + ↑a + 1) Ordering.lt

pp: case eq
a b : PosNum
⊢ Ordering.casesOn Ordering.eq (↑a < ↑b) (a = b) (↑b < ↑a) →
    Ordering.rec (↑a + ↑a + 1 < ↑b + ↑b + 1) (a.bit1 = b.bit1) (↑b + ↑b + 1 < ↑a + ↑a + 1) Ordering.eq

pp: case gt
a b : PosNum
⊢ Ordering.casesOn Ordering.gt (↑a < ↑b) (a = b) (↑b < ↑a) →
    Ordering.rec (↑a + ↑a + 1 < ↑b + ↑b + 1) (a.bit1 = b.bit1) (↑b + ↑b + 1 < ↑a + ↑a + 1) Ordering.gt

Tactic:
<;>

Goal state after:
case lt
a b : PosNum
⊢ Ordering.casesOn Ordering.lt (↑a < ↑b) (a = b) (↑b < ↑a) →
    Ordering.rec (↑a + ↑a + 1 < ↑b + ↑b + 1) (a.bit1 = b.bit1) (↑b + ↑b + 1 < ↑a + ↑a + 1) Ordering.lt

case eq
a b : PosNum
⊢ Ordering.casesOn Ordering.eq (↑a < ↑b) (a = b) (↑b < ↑a) →
    Ordering.rec (↑a + ↑a + 1 < ↑b + ↑b + 1) (a.bit1 = b.bit1) (↑b + ↑b + 1 < ↑a + ↑a + 1) Ordering.eq

case gt
a b : PosNum
⊢ Ordering.casesOn Ordering.gt (↑a < ↑b) (a = b) (↑b < ↑a) →
    Ordering.rec (↑a + ↑a + 1 < ↑b + ↑b + 1) (a.bit1 = b.bit1) (↑b + ↑b + 1 < ↑a + ↑a + 1) Ordering.gt
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case lt
a b : PosNum
⊢ ↑a < ↑b → ↑a + ↑a + 1 < ↑b + ↑b + 1

pp: case eq
a b : PosNum
⊢ a = b → a.bit1 = b.bit1

pp: case gt
a b : PosNum
⊢ ↑b < ↑a → ↑b + ↑b + 1 < ↑a + ↑a + 1

Tactic:
<;>

Goal state after:
case lt
a b : PosNum
⊢ ↑a < ↑b → ↑a + ↑a + 1 < ↑b + ↑b + 1

case eq
a b : PosNum
⊢ a = b → a.bit1 = b.bit1

case gt
a b : PosNum
⊢ ↑b < ↑a → ↑b + ↑b + 1 < ↑a + ↑a + 1
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case zero
⊢ zero + 0 = zero

pp: case pos
a✝ : PosNum
⊢ pos a✝ + 0 = pos a✝

Tactic:
<;>

Goal state after:
case zero
⊢ zero + 0 = zero

case pos
a✝ : PosNum
⊢ pos a✝ + 0 = pos a✝
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case zero
⊢ 0 + zero = zero

pp: case pos
a✝ : PosNum
⊢ 0 + pos a✝ = pos a✝

Tactic:
<;>

Goal state after:
case zero
⊢ 0 + zero = zero

case pos
a✝ : PosNum
⊢ 0 + pos a✝ = pos a✝
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: case nil
α : Type u
σ : Type v
M : εNFA α σ
u : σ
y : List (Option α)
t : σ
right✝ : M.IsPath t u y
s : σ
hx : M.IsPath s t []
⊢ M.IsPath s u ([] ++ y)

pp: case cons
α : Type u
σ : Type v
M : εNFA α σ
u : σ
y : List (Option α)
t : σ
right✝ : M.IsPath t u y
head✝ : Option α
tail✝ : List (Option α)
tail_ih✝ : ∀ {s : σ}, M.IsPath s t tail✝ → M.IsPath s u (tail✝ ++ y)
s : σ
hx : M.IsPath s t (head✝ :: tail✝)
⊢ M.IsPath s u (head✝ :: tail✝ ++ y)

Tactic:
<;>

Goal state after:
case nil
α : Type u
σ : Type v
M : εNFA α σ
u : σ
y : List (Option α)
t : σ
right✝ : M.IsPath t u y
s : σ
hx : M.IsPath s t []
⊢ M.IsPath s u ([] ++ y)

case cons
α : Type u
σ : Type v
M : εNFA α σ
u : σ
y : List (Option α)
t : σ
right✝ : M.IsPath t u y
head✝ : Option α
tail✝ : List (Option α)
tail_ih✝ : ∀ {s : σ}, M.IsPath s t tail✝ → M.IsPath s u (tail✝ ++ y)
s : σ
hx : M.IsPath s t (head✝ :: tail✝)
⊢ M.IsPath s u (head✝ :: tail✝ ++ y)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case one
⊢ pos one + 1 = (pos one).succ

pp: case bit1
a✝ : PosNum
⊢ pos a✝.bit1 + 1 = (pos a✝.bit1).succ

pp: case bit0
a✝ : PosNum
⊢ pos a✝.bit0 + 1 = (pos a✝.bit0).succ

Tactic:
<;>

Goal state after:
case one
⊢ pos one + 1 = (pos one).succ

case bit1
a✝ : PosNum
⊢ pos a✝.bit1 + 1 = (pos a✝.bit1).succ

case bit0
a✝ : PosNum
⊢ pos a✝.bit0 + 1 = (pos a✝.bit0).succ
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: case nil.nil
α : Type u
σ : Type v
M : εNFA α σ
u : σ
y : List (Option α)
t : σ
right✝ : M.IsPath t u y
⊢ M.IsPath t u ([] ++ y)

pp: case cons.cons
α : Type u
σ : Type v
M : εNFA α σ
u : σ
y : List (Option α)
t : σ
right✝ : M.IsPath t u y
head✝ : Option α
tail✝ : List (Option α)
tail_ih✝ : ∀ {s : σ}, M.IsPath s t tail✝ → M.IsPath s u (tail✝ ++ y)
s t✝ : σ
a✝¹ : t✝ ∈ M.step s head✝
a✝ : M.IsPath t✝ t tail✝
⊢ M.IsPath s u (head✝ :: tail✝ ++ y)

Tactic:
<;>

Goal state after:
case nil.nil
α : Type u
σ : Type v
M : εNFA α σ
u : σ
y : List (Option α)
t : σ
right✝ : M.IsPath t u y
⊢ M.IsPath t u ([] ++ y)

case cons.cons
α : Type u
σ : Type v
M : εNFA α σ
u : σ
y : List (Option α)
t : σ
right✝ : M.IsPath t u y
head✝ : Option α
tail✝ : List (Option α)
tail_ih✝ : ∀ {s : σ}, M.IsPath s t tail✝ → M.IsPath s u (tail✝ ++ y)
s t✝ : σ
a✝¹ : t✝ ∈ M.step s head✝
a✝ : M.IsPath t✝ t tail✝
⊢ M.IsPath s u (head✝ :: tail✝ ++ y)
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: case succ
α : Type u
σ : Type v
M : εNFA α σ
s₁ : σ
n✝ : ℕ
a✝ : ∀ {s₂ : σ}, M.IsPath s₁ s₂ (List.replicate n✝ none) → s₂ ∈ M.εClosure {s₁}
s₂ : σ
h : M.IsPath s₁ s₂ (List.replicate (n✝ + 1) none)
⊢ s₂ ∈ M.εClosure {s₁}

Tactic:
· simp_rw [List.replicate_add, isPath_append, List.replicate_one, isPath_singleton] at h
      obtain ⟨t, _, _⟩ := h
      solve_by_elim [εClosure.step]

Goal state after:
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case one
⊢ 0 < one.natSize

pp: case bit1
a✝ : PosNum
⊢ 0 < a✝.bit1.natSize

pp: case bit0
a✝ : PosNum
⊢ 0 < a✝.bit0.natSize

Tactic:
<;>

Goal state after:
case one
⊢ 0 < one.natSize

case bit1
a✝ : PosNum
⊢ 0 < a✝.bit1.natSize

case bit0
a✝ : PosNum
⊢ 0 < a✝.bit0.natSize
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case false
n : PosNum
⊢ ↑(bit false n) = Nat.bit false ↑n

pp: case true
n : PosNum
⊢ ↑(bit true n) = Nat.bit true ↑n

Tactic:
<;>

Goal state after:
case false
n : PosNum
⊢ ↑(bit false n) = Nat.bit false ↑n

case true
n : PosNum
⊢ ↑(bit true n) = Nat.bit true ↑n
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case lt
m n : PosNum
⊢ Ordering.casesOn Ordering.lt (m < n) (m = n) (n < m) → (Ordering.lt = Ordering.eq ↔ m = n)

pp: case eq
m n : PosNum
⊢ Ordering.casesOn Ordering.eq (m < n) (m = n) (n < m) → (Ordering.eq = Ordering.eq ↔ m = n)

pp: case gt
m n : PosNum
⊢ Ordering.casesOn Ordering.gt (m < n) (m = n) (n < m) → (Ordering.gt = Ordering.eq ↔ m = n)

Tactic:
<;>

Goal state after:
case lt
m n : PosNum
⊢ Ordering.casesOn Ordering.lt (m < n) (m = n) (n < m) → (Ordering.lt = Ordering.eq ↔ m = n)

case eq
m n : PosNum
⊢ Ordering.casesOn Ordering.eq (m < n) (m = n) (n < m) → (Ordering.eq = Ordering.eq ↔ m = n)

case gt
m n : PosNum
⊢ Ordering.casesOn Ordering.gt (m < n) (m = n) (n < m) → (Ordering.gt = Ordering.eq ↔ m = n)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case false
n : Num
⊢ ↑(bit false n) = Nat.bit false ↑n

pp: case true
n : Num
⊢ ↑(bit true n) = Nat.bit true ↑n

Tactic:
<;>

Goal state after:
case false
n : Num
⊢ ↑(bit false n) = Nat.bit false ↑n

case true
n : Num
⊢ ↑(bit true n) = Nat.bit true ↑n
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case false.zero
⊢ ↑(bit false zero) = Nat.bit false ↑zero

pp: case false.pos
a✝ : PosNum
⊢ ↑(bit false (pos a✝)) = Nat.bit false ↑(pos a✝)

pp: case true.zero
⊢ ↑(bit true zero) = Nat.bit true ↑zero

pp: case true.pos
a✝ : PosNum
⊢ ↑(bit true (pos a✝)) = Nat.bit true ↑(pos a✝)

Tactic:
<;>

Goal state after:
case false.zero
⊢ ↑(bit false zero) = Nat.bit false ↑zero

case false.pos
a✝ : PosNum
⊢ ↑(bit false (pos a✝)) = Nat.bit false ↑(pos a✝)

case true.zero
⊢ ↑(bit true zero) = Nat.bit true ↑zero

case true.pos
a✝ : PosNum
⊢ ↑(bit true (pos a✝)) = Nat.bit true ↑(pos a✝)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case false.zero
⊢ ↑zero.bit0 = 0

pp: case false.pos
a✝ : PosNum
⊢ ↑(pos a✝).bit0 = ↑a✝ + ↑a✝

pp: case true.zero
⊢ ↑zero.bit1 = 1

pp: case true.pos
a✝ : PosNum
⊢ ↑(pos a✝).bit1 = ↑a✝ + (↑a✝ + 1)

Tactic:
<;>

Goal state after:
case false.zero
⊢ ↑zero.bit0 = 0

case false.pos
a✝ : PosNum
⊢ ↑(pos a✝).bit0 = ↑a✝ + ↑a✝

case true.zero
⊢ ↑zero.bit1 = 1

case true.pos
a✝ : PosNum
⊢ ↑(pos a✝).bit1 = ↑a✝ + (↑a✝ + 1)
Module: Mathlib.Computability.Halting

Goal state before:
pp: case pos
C : Set (ℕ →. ℕ)
f g : ℕ →. ℕ
hf : Nat.Partrec f
hg : Nat.Partrec g
fC : f ∈ C
w✝ : DecidablePred fun c ↦ c.eval ∈ C
h : Computable fun a ↦ decide ((fun c ↦ c.eval ∈ C) a)
c : Code
e : c.eval = fun b ↦ if c.eval ∈ C then g b else f b
H : c.eval ∈ C
⊢ g ∈ C

pp: case neg
C : Set (ℕ →. ℕ)
f g : ℕ →. ℕ
hf : Nat.Partrec f
hg : Nat.Partrec g
fC : f ∈ C
w✝ : DecidablePred fun c ↦ c.eval ∈ C
h : Computable fun a ↦ decide ((fun c ↦ c.eval ∈ C) a)
c : Code
e : c.eval = fun b ↦ if c.eval ∈ C then g b else f b
H : c.eval ∉ C
⊢ g ∈ C

Tactic:
<;>

Goal state after:
case pos
C : Set (ℕ →. ℕ)
f g : ℕ →. ℕ
hf : Nat.Partrec f
hg : Nat.Partrec g
fC : f ∈ C
w✝ : DecidablePred fun c ↦ c.eval ∈ C
h : Computable fun a ↦ decide ((fun c ↦ c.eval ∈ C) a)
c : Code
e : c.eval = fun b ↦ if c.eval ∈ C then g b else f b
H : c.eval ∈ C
⊢ g ∈ C

case neg
C : Set (ℕ →. ℕ)
f g : ℕ →. ℕ
hf : Nat.Partrec f
hg : Nat.Partrec g
fC : f ∈ C
w✝ : DecidablePred fun c ↦ c.eval ∈ C
h : Computable fun a ↦ decide ((fun c ↦ c.eval ∈ C) a)
c : Code
e : c.eval = fun b ↦ if c.eval ∈ C then g b else f b
H : c.eval ∉ C
⊢ g ∈ C