mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: case hx
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb₀ : 0 < b
h_tendsto : Tendsto (fun x ↦ 1 / 2 * log x) atTop atTop
x : ℝ
hx_pos : 1 < x
hx : ∀ (y : ℝ), b * id x ≤ y → -log b < 1 / 2 * log y
u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ 0 < u

pp: case hxy
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb₀ : 0 < b
h_tendsto : Tendsto (fun x ↦ 1 / 2 * log x) atTop atTop
x : ℝ
hx_pos : 1 < x
hx : ∀ (y : ℝ), b * id x ≤ y → -log b < 1 / 2 * log y
u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ u ≤ x

Tactic:
·

Goal state after:
case hx
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb₀ : 0 < b
h_tendsto : Tendsto (fun x ↦ 1 / 2 * log x) atTop atTop
x : ℝ
hx_pos : 1 < x
hx : ∀ (y : ℝ), b * id x ≤ y → -log b < 1 / 2 * log y
u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ 0 < u
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: case hxy
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb₀ : 0 < b
h_tendsto : Tendsto (fun x ↦ 1 / 2 * log x) atTop atTop
x : ℝ
hx_pos : 1 < x
hx : ∀ (y : ℝ), b * id x ≤ y → -log b < 1 / 2 * log y
u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ u ≤ x

Tactic:
·

Goal state after:
case hxy
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb₀ : 0 < b
h_tendsto : Tendsto (fun x ↦ 1 / 2 * log x) atTop atTop
x : ℝ
hx_pos : 1 < x
hx : ∀ (y : ℝ), b * id x ≤ y → -log b < 1 / 2 * log y
u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ u ≤ x
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: case inr.inl.refine_2
a b c : ℕ
v : ℕ := a ^^^ b ^^^ c
h✝ : v ≠ 0
hv : v = a ^^^ b ^^^ c
hab : a ^^^ b = c ^^^ v
hbc : b ^^^ c = a ^^^ v
hca : c ^^^ a = b ^^^ v
i : ℕ
hi : v.testBit i = true
hi' : ∀ (j : ℕ), i < j → v.testBit j = false
h : b.testBit i = true
j : ℕ
hj : i < j
⊢ (b ^^^ v).testBit j = b.testBit j

Tactic:
·

Goal state after:
case inr.inl.refine_2
a b c : ℕ
v : ℕ := a ^^^ b ^^^ c
h✝ : v ≠ 0
hv : v = a ^^^ b ^^^ c
hab : a ^^^ b = c ^^^ v
hbc : b ^^^ c = a ^^^ v
hca : c ^^^ a = b ^^^ v
i : ℕ
hi : v.testBit i = true
hi' : ∀ (j : ℕ), i < j → v.testBit j = false
h : b.testBit i = true
j : ℕ
hj : i < j
⊢ (b ^^^ v).testBit j = b.testBit j
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: case inr.inr.refine_1
a b c : ℕ
v : ℕ := a ^^^ b ^^^ c
h✝ : v ≠ 0
hv : v = a ^^^ b ^^^ c
hab : a ^^^ b = c ^^^ v
hbc : b ^^^ c = a ^^^ v
hca : c ^^^ a = b ^^^ v
i : ℕ
hi : v.testBit i = true
hi' : ∀ (j : ℕ), i < j → v.testBit j = false
h : c.testBit i = true
⊢ (c ^^^ v).testBit i = false

pp: case inr.inr.refine_2
a b c : ℕ
v : ℕ := a ^^^ b ^^^ c
h✝ : v ≠ 0
hv : v = a ^^^ b ^^^ c
hab : a ^^^ b = c ^^^ v
hbc : b ^^^ c = a ^^^ v
hca : c ^^^ a = b ^^^ v
i : ℕ
hi : v.testBit i = true
hi' : ∀ (j : ℕ), i < j → v.testBit j = false
h : c.testBit i = true
j : ℕ
hj : i < j
⊢ (c ^^^ v).testBit j = c.testBit j

Tactic:
·

Goal state after:
case inr.inr.refine_1
a b c : ℕ
v : ℕ := a ^^^ b ^^^ c
h✝ : v ≠ 0
hv : v = a ^^^ b ^^^ c
hab : a ^^^ b = c ^^^ v
hbc : b ^^^ c = a ^^^ v
hca : c ^^^ a = b ^^^ v
i : ℕ
hi : v.testBit i = true
hi' : ∀ (j : ℕ), i < j → v.testBit j = false
h : c.testBit i = true
⊢ (c ^^^ v).testBit i = false
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case succ.prec.succ.none
x✝ : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
cf cg : Code
hg :
  ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode (cf.prec cg)) →
      lup
          (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair k (encode (cf.prec cg)))))
          (k', c') n =
        evaln k' c' n
lf : encode cf < encode (cf.prec cg)
lg : encode cg < encode (cf.prec cg)
n✝ : ℕ
⊢ (Option.none.bind fun i ↦
      lup
        (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
          (List.range (Nat.pair (k' + 1) (encode (cf.prec cg)))))
        (k' + 1, cg) (Nat.pair (unpair n).1 (Nat.pair n✝ i))) =
    Option.none.bind fun i ↦ evaln (k' + 1) cg (Nat.pair (unpair n).1 (Nat.pair n✝ i))

pp: case succ.prec.succ.some
x✝ : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
cf cg : Code
hg :
  ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode (cf.prec cg)) →
      lup
          (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair k (encode (cf.prec cg)))))
          (k', c') n =
        evaln k' c' n
lf : encode cf < encode (cf.prec cg)
lg : encode cg < encode (cf.prec cg)
n✝ val✝ : ℕ
⊢ ((some val✝).bind fun i ↦
      lup
        (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
          (List.range (Nat.pair (k' + 1) (encode (cf.prec cg)))))
        (k' + 1, cg) (Nat.pair (unpair n).1 (Nat.pair n✝ i))) =
    (some val✝).bind fun i ↦ evaln (k' + 1) cg (Nat.pair (unpair n).1 (Nat.pair n✝ i))

Tactic:
·

Goal state after:
case succ.prec.succ.none
x✝ : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
cf cg : Code
hg :
  ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode (cf.prec cg)) →
      lup
          (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair k (encode (cf.prec cg)))))
          (k', c') n =
        evaln k' c' n
lf : encode cf < encode (cf.prec cg)
lg : encode cg < encode (cf.prec cg)
n✝ : ℕ
⊢ (Option.none.bind fun i ↦
      lup
        (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
          (List.range (Nat.pair (k' + 1) (encode (cf.prec cg)))))
        (k' + 1, cg) (Nat.pair (unpair n).1 (Nat.pair n✝ i))) =
    Option.none.bind fun i ↦ evaln (k' + 1) cg (Nat.pair (unpair n).1 (Nat.pair n✝ i))
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case succ.rfind'
x✝ : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
cf : Code
hg :
  ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode cf.rfind') →
      lup
          (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair k (encode cf.rfind'))))
          (k', c') n =
        evaln k' c' n
⊢ ((lup
          (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair (k' + 1) (encode cf.rfind'))))
          (k' + 1, cf) n).bind
      fun x ↦
      Nat.rec (some (unpair n).2)
        (fun n_1 n_ih ↦
          lup
            (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
              (List.range (Nat.pair (k' + 1) (encode cf.rfind'))))
            (k', cf.rfind') (Nat.pair (unpair n).1 ((unpair n).2 + 1)))
        x) =
    (evaln (k' + 1) cf n).bind fun a ↦
      if a = 0 then some (unpair n).2 else evaln k' cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1))

Tactic:
·

Goal state after:
case succ.rfind'
x✝ : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
cf : Code
hg :
  ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode cf.rfind') →
      lup
          (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair k (encode cf.rfind'))))
          (k', c') n =
        evaln k' c' n
⊢ ((lup
          (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair (k' + 1) (encode cf.rfind'))))
          (k' + 1, cf) n).bind
      fun x ↦
      Nat.rec (some (unpair n).2)
        (fun n_1 n_ih ↦
          lup
            (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
              (List.range (Nat.pair (k' + 1) (encode cf.rfind'))))
            (k', cf.rfind') (Nat.pair (unpair n).1 ((unpair n).2 + 1)))
        x) =
    (evaln (k' + 1) cf n).bind fun a ↦
      if a = 0 then some (unpair n).2 else evaln k' cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1))
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: case inr.inr.refine_2
a b c : ℕ
v : ℕ := a ^^^ b ^^^ c
h✝ : v ≠ 0
hv : v = a ^^^ b ^^^ c
hab : a ^^^ b = c ^^^ v
hbc : b ^^^ c = a ^^^ v
hca : c ^^^ a = b ^^^ v
i : ℕ
hi : v.testBit i = true
hi' : ∀ (j : ℕ), i < j → v.testBit j = false
h : c.testBit i = true
j : ℕ
hj : i < j
⊢ (c ^^^ v).testBit j = c.testBit j

Tactic:
·

Goal state after:
case inr.inr.refine_2
a b c : ℕ
v : ℕ := a ^^^ b ^^^ c
h✝ : v ≠ 0
hv : v = a ^^^ b ^^^ c
hab : a ^^^ b = c ^^^ v
hbc : b ^^^ c = a ^^^ v
hca : c ^^^ a = b ^^^ v
i : ℕ
hi : v.testBit i = true
hi' : ∀ (j : ℕ), i < j → v.testBit j = false
h : c.testBit i = true
j : ℕ
hj : i < j
⊢ (c ^^^ v).testBit j = c.testBit j
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: case pos
m n : ℕ
h : (m + n) % 2 = 0
⊢ (m ^^^ n) % 2 = (m + n) % 2

pp: case neg
m n : ℕ
h : ¬(m + n) % 2 = 0
⊢ (m ^^^ n) % 2 = (m + n) % 2

Tactic:
·

Goal state after:
case pos
m n : ℕ
h : (m + n) % 2 = 0
⊢ (m ^^^ n) % 2 = (m + n) % 2
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: case neg
m n : ℕ
h : ¬(m + n) % 2 = 0
⊢ (m ^^^ n) % 2 = (m + n) % 2

Tactic:
·

Goal state after:
case neg
m n : ℕ
h : ¬(m + n) % 2 = 0
⊢ (m ^^^ n) % 2 = (m + n) % 2
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: case zero
h : Odd 0
⊢ 0 ^^^ 1 = 0 - 1

Tactic:
exact not_odd_zero h |>.elim

Goal state after:
Module: Mathlib.Computability.Encoding

Goal state before:
pp: case zero
⊢ (if
        (match Num.zero with
          | Num.zero => []
          | Num.pos n => encodePosNum n) =
          [] then
      Num.zero
    else
      ↑(decodePosNum
          (match Num.zero with
          | Num.zero => []
          | Num.pos n => encodePosNum n))) =
    Num.zero

pp: case pos
n : PosNum
⊢ (if
        (match Num.pos n with
          | Num.zero => []
          | Num.pos n => encodePosNum n) =
          [] then
      Num.zero
    else
      ↑(decodePosNum
          (match Num.pos n with
          | Num.zero => []
          | Num.pos n => encodePosNum n))) =
    Num.pos n

Tactic:
·

Goal state after:
case zero
⊢ (if
        (match Num.zero with
          | Num.zero => []
          | Num.pos n => encodePosNum n) =
          [] then
      Num.zero
    else
      ↑(decodePosNum
          (match Num.zero with
          | Num.zero => []
          | Num.pos n => encodePosNum n))) =
    Num.zero
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: case left
x y n m : ℕ
hx : x < 2 ^ n
hy : y < 2 ^ m
⊢ y <<< n < 2 ^ (n + m)

pp: case right
x y n m : ℕ
hx : x < 2 ^ n
hy : y < 2 ^ m
⊢ x < 2 ^ (n + m)

Tactic:
·

Goal state after:
case left
x y n m : ℕ
hx : x < 2 ^ n
hy : y < 2 ^ m
⊢ y <<< n < 2 ^ (n + m)
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: case right
x y n m : ℕ
hx : x < 2 ^ n
hy : y < 2 ^ m
⊢ x < 2 ^ (n + m)

Tactic:
·

Goal state after:
case right
x y n m : ℕ
hx : x < 2 ^ n
hy : y < 2 ^ m
⊢ x < 2 ^ (n + m)
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: case mp
α : Type u_1
l : List (Option α)
⊢ (∀ (a : Option α), a ∈ l → id a = none) → ∃ n, l = replicate n none

pp: case mpr
α : Type u_1
l : List (Option α)
⊢ (∃ n, l = replicate n none) → ∀ (a : Option α), a ∈ l → id a = none

Tactic:
·

Goal state after:
case mp
α : Type u_1
l : List (Option α)
⊢ (∀ (a : Option α), a ∈ l → id a = none) → ∃ n, l = replicate n none
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: case mpr
α : Type u_1
l : List (Option α)
⊢ (∃ n, l = replicate n none) → ∀ (a : Option α), a ∈ l → id a = none

Tactic:
·

Goal state after:
case mpr
α : Type u_1
l : List (Option α)
⊢ (∃ n, l = replicate n none) → ∀ (a : Option α), a ∈ l → id a = none
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: case mp
α : Type u_1
l : List (Option α)
a : α
⊢ filterMap id l = [a] → ∃ m n, l = replicate m none ++ some a :: replicate n none

pp: case mpr
α : Type u_1
l : List (Option α)
a : α
⊢ (∃ m n, l = replicate m none ++ some a :: replicate n none) → filterMap id l = [a]

Tactic:
·

Goal state after:
case mp
α : Type u_1
l : List (Option α)
a : α
⊢ filterMap id l = [a] → ∃ m n, l = replicate m none ++ some a :: replicate n none
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: case mpr
α : Type u_1
l : List (Option α)
a : α
⊢ (∃ m n, l = replicate m none ++ some a :: replicate n none) → filterMap id l = [a]

Tactic:
·

Goal state after:
case mpr
α : Type u_1
l : List (Option α)
a : α
⊢ (∃ m n, l = replicate m none ++ some a :: replicate n none) → filterMap id l = [a]
Module: Mathlib.Computability.NFA

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

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:
·

Goal state after:
case mp
α : Type u
σ : Type v
M : NFA α σ
S T : Set σ
x : List α
⊢ (∃ s ∈ M.accept, s ∈ M.evalFrom S x ∨ s ∈ M.evalFrom T x) → x ∈ M.acceptsFrom S ∪ M.acceptsFrom T
Module: Mathlib.Computability.NFA

Goal state before:
pp: case mp.inl
α : Type u
σ : Type v
M : NFA α σ
S T : Set σ
x : List α
s : σ
hs : s ∈ M.accept
h : s ∈ M.evalFrom S x
⊢ x ∈ M.acceptsFrom S ∪ M.acceptsFrom T

pp: case mp.inr
α : Type u
σ : Type v
M : NFA α σ
S T : Set σ
x : List α
s : σ
hs : s ∈ M.accept
h : s ∈ M.evalFrom T x
⊢ x ∈ M.acceptsFrom S ∪ M.acceptsFrom T

Tactic:
·

Goal state after:
case mp.inl
α : Type u
σ : Type v
M : NFA α σ
S T : Set σ
x : List α
s : σ
hs : s ∈ M.accept
h : s ∈ M.evalFrom S x
⊢ x ∈ M.acceptsFrom S ∪ M.acceptsFrom T
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: case mp
α : Type u_1
l : List (Option α)
l' : List α
a : α
⊢ l.reduceOption = l' ++ [a] → ∃ l₁ l₂, l = l₁ ++ some a :: l₂ ∧ l₁.reduceOption = l' ∧ l₂.reduceOption = []

pp: case mpr
α : Type u_1
l : List (Option α)
l' : List α
a : α
⊢ (∃ l₁ l₂, l = l₁ ++ some a :: l₂ ∧ l₁.reduceOption = l' ∧ l₂.reduceOption = []) → l.reduceOption = l' ++ [a]

Tactic:
·

Goal state after:
case mp
α : Type u_1
l : List (Option α)
l' : List α
a : α
⊢ l.reduceOption = l' ++ [a] → ∃ l₁ l₂, l = l₁ ++ some a :: l₂ ∧ l₁.reduceOption = l' ∧ l₂.reduceOption = []
Module: Mathlib.Computability.NFA

Goal state before:
pp: case mp.inr
α : Type u
σ : Type v
M : NFA α σ
S T : Set σ
x : List α
s : σ
hs : s ∈ M.accept
h : s ∈ M.evalFrom T x
⊢ x ∈ M.acceptsFrom S ∪ M.acceptsFrom T

Tactic:
·

Goal state after:
case mp.inr
α : Type u
σ : Type v
M : NFA α σ
S T : Set σ
x : List α
s : σ
hs : s ∈ M.accept
h : s ∈ M.evalFrom T x
⊢ x ∈ M.acceptsFrom S ∪ M.acceptsFrom T
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:
·

Goal state after:
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
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: case mpr
α : Type u_1
l : List (Option α)
l' : List α
a : α
⊢ (∃ l₁ l₂, l = l₁ ++ some a :: l₂ ∧ l₁.reduceOption = l' ∧ l₂.reduceOption = []) → l.reduceOption = l' ++ [a]

Tactic:
·

Goal state after:
case mpr
α : Type u_1
l : List (Option α)
l' : List α
a : α
⊢ (∃ l₁ l₂, l = l₁ ++ some a :: l₂ ∧ l₁.reduceOption = l' ∧ l₂.reduceOption = []) → l.reduceOption = l' ++ [a]
Module: Mathlib.Data.Num.Lemmas

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

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

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

Tactic:
·

Goal state after:
case lt
a b : PosNum
this : ↑a < ↑b
⊢ ↑a + ↑a < ↑b + ↑b
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case eq
a b : PosNum
this : a = b
⊢ a.bit0 = b.bit0

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

Tactic:
·

Goal state after:
case eq
a b : PosNum
this : a = b
⊢ a.bit0 = b.bit0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case gt
a b : PosNum
this : ↑b < ↑a
⊢ ↑b + ↑b < ↑a + ↑a

Tactic:
·

Goal state after:
case gt
a b : PosNum
this : ↑b < ↑a
⊢ ↑b + ↑b < ↑a + ↑a
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: case nil
α : Type u_1
⊢ [].reduceOption.length = (filter Option.isSome []).length

Tactic:
simp_rw [reduceOption_nil, filter_nil, length]

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

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

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

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

Tactic:
·

Goal state after:
case lt
a b : PosNum
this : ↑a < ↑b
⊢ ↑a + ↑a < ↑b + ↑b + 1
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: case nil
α : Type u_1
⊢ (¬∀ (x : Option α), x ∈ [] → x.isSome = true) ↔ none ∈ []

pp: case cons
α : Type u_1
head✝ : Option α
tail✝ : List (Option α)
tail_ih✝ : (¬∀ (x : Option α), x ∈ tail✝ → x.isSome = true) ↔ none ∈ tail✝
⊢ (¬∀ (x : Option α), x ∈ head✝ :: tail✝ → x.isSome = true) ↔ none ∈ head✝ :: tail✝

Tactic:
·

Goal state after:
case nil
α : Type u_1
⊢ (¬∀ (x : Option α), x ∈ [] → x.isSome = true) ↔ none ∈ []
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case eq
a b : PosNum
this : a = b
⊢ ↑a + ↑a < ↑b + ↑b + 1

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

Tactic:
·

Goal state after:
case eq
a b : PosNum
this : a = b
⊢ ↑a + ↑a < ↑b + ↑b + 1
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: case cons
α : Type u_1
head✝ : Option α
tail✝ : List (Option α)
tail_ih✝ : (¬∀ (x : Option α), x ∈ tail✝ → x.isSome = true) ↔ none ∈ tail✝
⊢ (¬∀ (x : Option α), x ∈ head✝ :: tail✝ → x.isSome = true) ↔ none ∈ head✝ :: tail✝

Tactic:
·

Goal state after:
case cons
α : Type u_1
head✝ : Option α
tail✝ : List (Option α)
tail_ih✝ : (¬∀ (x : Option α), x ∈ tail✝ → x.isSome = true) ↔ none ∈ tail✝
⊢ (¬∀ (x : Option α), x ∈ head✝ :: tail✝ → x.isSome = true) ↔ none ∈ head✝ :: tail✝
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case gt
a b : PosNum
this : ↑b < ↑a
⊢ ↑b + ↑b + 1 < ↑a + ↑a

Tactic:
·

Goal state after:
case gt
a b : PosNum
this : ↑b < ↑a
⊢ ↑b + ↑b + 1 < ↑a + ↑a
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

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
Module: Mathlib.Computability.NFA

Goal state before:
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 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
this : ↑a < ↑b
⊢ ↑a + ↑a + 1 < ↑b + ↑b

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

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

Tactic:
·

Goal state after:
case lt
a b : PosNum
this : ↑a < ↑b
⊢ ↑a + ↑a + 1 < ↑b + ↑b
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case eq
a b : PosNum
this : a = b
⊢ ↑b + ↑b < ↑a + ↑a + 1

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

Tactic:
·

Goal state after:
case eq
a b : PosNum
this : a = b
⊢ ↑b + ↑b < ↑a + ↑a + 1
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case gt
a b : PosNum
this : ↑b < ↑a
⊢ ↑b + ↑b < ↑a + ↑a + 1

Tactic:
·

Goal state after:
case gt
a b : PosNum
this : ↑b < ↑a
⊢ ↑b + ↑b < ↑a + ↑a + 1
Module: Mathlib.Computability.NFA

Goal state before:
pp: case mp
α : Type u
σ : Type v
M : DFA α σ
x : List α
⊢ (∃ S ∈ M.toNFA.accept, S ∈ {M.evalFrom M.start x}) → x ∈ M.accepts

pp: case mpr
α : Type u
σ : Type v
M : DFA α σ
x : List α
⊢ x ∈ M.accepts → ∃ S ∈ M.toNFA.accept, S ∈ {M.evalFrom M.start x}

Tactic:
·

Goal state after:
case mp
α : Type u
σ : Type v
M : DFA α σ
x : List α
⊢ (∃ S ∈ M.toNFA.accept, S ∈ {M.evalFrom M.start x}) → x ∈ M.accepts
Module: Mathlib.Computability.NFA

Goal state before:
pp: case mpr
α : Type u
σ : Type v
M : DFA α σ
x : List α
⊢ x ∈ M.accepts → ∃ S ∈ M.toNFA.accept, S ∈ {M.evalFrom M.start x}

Tactic:
·

Goal state after:
case mpr
α : Type u
σ : Type v
M : DFA α σ
x : List α
⊢ x ∈ M.accepts → ∃ S ∈ M.toNFA.accept, S ∈ {M.evalFrom M.start x}
Module: Mathlib.Data.Num.Lemmas

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

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

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

Tactic:
·

Goal state after:
case lt
a b : PosNum
this : ↑a < ↑b
⊢ ↑a + ↑a + 1 < ↑b + ↑b + 1
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case eq
a b : PosNum
this : a = b
⊢ a.bit1 = b.bit1

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

Tactic:
·

Goal state after:
case eq
a b : PosNum
this : a = b
⊢ a.bit1 = b.bit1
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case gt
a b : PosNum
this : ↑b < ↑a
⊢ ↑b + ↑b + 1 < ↑a + ↑a + 1

Tactic:
·

Goal state after:
case gt
a b : PosNum
this : ↑b < ↑a
⊢ ↑b + ↑b + 1 < ↑a + ↑a + 1
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case false
n : ℕ
ih : ofNat' (n + 1) = ofNat' n + 1
⊢ ofNat' (Nat.bit false n + 1) = ofNat' (Nat.bit false n) + 1

pp: case true
n : ℕ
ih : ofNat' (n + 1) = ofNat' n + 1
⊢ ofNat' (Nat.bit true n + 1) = ofNat' (Nat.bit true n) + 1

Tactic:
·

Goal state after:
case false
n : ℕ
ih : ofNat' (n + 1) = ofNat' n + 1
⊢ ofNat' (Nat.bit false n + 1) = ofNat' (Nat.bit false n) + 1
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case true
n : ℕ
ih : ofNat' (n + 1) = ofNat' n + 1
⊢ ofNat' (Nat.bit true n + 1) = ofNat' (Nat.bit true n) + 1

Tactic:
·

Goal state after:
case true
n : ℕ
ih : ofNat' (n + 1) = ofNat' n + 1
⊢ ofNat' (Nat.bit true n + 1) = ofNat' (Nat.bit true n) + 1
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case zero
m : ℕ
⊢ ofNat' (m + 0) = ofNat' m + ofNat' 0

pp: case succ
m n✝ : ℕ
a✝ : ofNat' (m + n✝) = ofNat' m + ofNat' n✝
⊢ ofNat' (m + (n✝ + 1)) = ofNat' m + ofNat' (n✝ + 1)

Tactic:
·

Goal state after:
case zero
m : ℕ
⊢ ofNat' (m + 0) = ofNat' m + ofNat' 0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case succ
m n✝ : ℕ
a✝ : ofNat' (m + n✝) = ofNat' m + ofNat' n✝
⊢ ofNat' (m + (n✝ + 1)) = ofNat' m + ofNat' (n✝ + 1)

Tactic:
·

Goal state after:
case succ
m n✝ : ℕ
a✝ : ofNat' (m + n✝) = ofNat' m + ofNat' n✝
⊢ ofNat' (m + (n✝ + 1)) = ofNat' m + ofNat' (n✝ + 1)
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: case zero
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ : σ
h : M.IsPath s₁ s₂ (List.replicate 0 none)
⊢ s₂ ∈ M.εClosure {s₁}

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:
·

Goal state after:
case zero
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ : σ
h : M.IsPath s₁ s₂ (List.replicate 0 none)
⊢ s₂ ∈ M.εClosure {s₁}
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:
·

Goal state after:
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₁}