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

Goal state before:
pp: case succ.rfind'.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 : 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
lf : encode cf < encode cf.rfind'
⊢ (Option.none.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) =
    Option.none.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:
rfl

Goal state after:
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: case zero
h : Even 0
⊢ 0 ^^^ 1 = 0 + 1

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: case succ
n : ℕ
h : Odd (n + 1)
⊢ (if n + 1 = 0 then if (false != true) = true then 1 else 0
    else
      if 1 = 0 then if (true != false) = true then n + 1 else 0
      else
        if (decide ((n + 1) % 2 = 1) != decide True) = true then
          ((if (true != false) = true then (n + 1) / 2 else 0) + if (true != false) = true then (n + 1) / 2 else 0) + 1
        else (if (true != false) = true then (n + 1) / 2 else 0) + if (true != false) = true then (n + 1) / 2 else 0) =
    n + 1 - 1

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: n : ℕ
ih :
  List.foldl (fun x1 x2 ↦ x1 ^^^ x2) 0 (List.range (n + 1)) =
    match Fin.ofNat 4 n with
    | 0 => n
    | 1 => 1
    | 2 => n + 1
    | 3 => 0
h : Fin.ofNat 4 n = 0
⊢ ↑0 % 2 = 0

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: n : ℕ
ih :
  List.foldl (fun x1 x2 ↦ x1 ^^^ x2) 0 (List.range (n + 1)) =
    match Fin.ofNat 4 n with
    | 0 => n
    | 1 => 1
    | 2 => n + 1
    | 3 => 0
h : Fin.ofNat 4 n = 1
⊢ (↑1 % 2 + 1 % 2) % 2 = 0

Tactic:
rfl

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

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

Tactic:
rfl

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

Goal state before:
pp: case bit1
a✝ : PosNum
⊢ 1 + a✝.bit1 = a✝.bit1.succ

Tactic:
rfl

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

Goal state before:
pp: case bit0
a✝ : PosNum
⊢ 1 + a✝.bit0 = a✝.bit0.succ

Tactic:
rfl

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

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

Tactic:
rfl

Goal state after:
Module: Mathlib.Computability.Encoding

Goal state before:
pp: case false
⊢ sectionΓ'Bool (inclusionBoolΓ' false) = false

Tactic:
rfl

Goal state after:
Module: Mathlib.Computability.Encoding

Goal state before:
pp: case true
⊢ sectionΓ'Bool (inclusionBoolΓ' true) = true

Tactic:
rfl

Goal state after:
Module: Mathlib.Computability.Encoding

Goal state before:
pp: case one
⊢ (if [] = [] then PosNum.one else (decodePosNum []).bit1) = PosNum.one

Tactic:
rfl

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

Tactic:
rfl

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

Goal state before:
pp: case bit1
a✝ : PosNum
⊢ a✝.bit1 + 1 = a✝.bit1.succ

Tactic:
rfl

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

Goal state before:
pp: case bit0
a✝ : PosNum
⊢ a✝.bit0 + 1 = a✝.bit0.succ

Tactic:
rfl

Goal state after:
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
S : Set σ
x : List α
⊢ x ∈ M.acceptsFrom S ↔ ∃ s ∈ M.accept, s ∈ M.evalFrom S x

Tactic:
rfl

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

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

Goal state before:
pp: case one.one
⊢ Ordering.eq.swap = Ordering.eq

Tactic:
rfl

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

Goal state before:
pp: case one.bit1
n : PosNum
⊢ Ordering.lt.swap = Ordering.gt

Tactic:
rfl

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

Goal state before:
pp: case one.bit0
n : PosNum
⊢ Ordering.lt.swap = Ordering.gt

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

Goal state after:
case bit1.bit1
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (m.cmp n).swap = n.cmp m
Module: Mathlib.Data.Num.Lemmas

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

Goal state after:
case bit0.bit0
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (m.cmp n).swap = n.cmp m
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

Tactic:
rfl

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

Goal state before:
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

Tactic:
rfl

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

Goal state before:
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

Tactic:
rfl

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

Goal state before:
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

Tactic:
rfl

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

Goal state before:
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

Tactic:
rfl

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

Goal state before:
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:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

Goal state after:
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
x : List α
⊢ x ∈ M.accepts ↔ ∃ S ∈ M.accept, S ∈ M.evalFrom M.start x

Tactic:
rfl

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

Goal state before:
pp: m n : PosNum
⊢ ↑m ≤ ↑n ↔ m ≤ n

Tactic:
rw [← not_lt]; exact not_congr lt_to_nat

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

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

Tactic:
rfl

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

Goal state before:
pp: case pos
a✝ : PosNum
⊢ pos a✝ + 0 = pos a✝

Tactic:
rfl

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

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

Tactic:
rfl

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

Goal state before:
pp: case pos
a✝ : PosNum
⊢ 0 + pos a✝ = pos a✝

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

Goal state before:
pp: m n : Num
⊢ ↑m ≤ ↑n ↔ m ≤ n

Tactic:
rw [← not_lt]; exact not_congr lt_to_nat

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

Goal state before:
pp: n : PosNum
this : (↑n.pred').succ = ↑n
h : ↑1 = ↑n
⊢ ↑(Num.casesOn 0 1 bit1) = (↑1 + ↑1).pred

Tactic:
rfl

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
start S : Set σ
s : α
x✝ a✝¹ : σ
a✝ : a✝¹ ∈ S
⊢ x✝ ∈ M.toεNFA.step a✝¹ (some s) ↔ x✝ ∈ M.step a✝¹ s

Tactic:
rfl

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
⊢ {x | ∃ S ∈ M.toεNFA.accept, S ∈ M.evalFrom M.toεNFA.start x} = M.accepts

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

Goal state before:
pp: case true.zero
⊢ ↑zero.bit1 = 1

Tactic:
rfl

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

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

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
inst✝ : NonAssocSemiring α
n : Num
⊢ 2 * ↑n + ↑1 = 2 * ↑n + 1

Tactic:
rfl

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

Goal state before:
pp: case zero
⊢ -zero.toZNum = zero.toZNumNeg

Tactic:
rfl

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

Goal state before:
pp: case pos
a✝ : PosNum
⊢ -(pos a✝).toZNum = (pos a✝).toZNumNeg

Tactic:
rfl

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

Goal state before:
pp: case zero
⊢ -zero.toZNumNeg = zero.toZNum

Tactic:
rfl

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

Goal state before:
pp: case pos
a✝ : PosNum
⊢ -(pos a✝).toZNumNeg = (pos a✝).toZNum

Tactic:
rfl

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

Goal state before:
pp: case zero.zero.refl
⊢ zero = zero

Tactic:
rfl

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

Goal state before:
pp: case pos.pos.refl
a✝ : PosNum
⊢ pos a✝ = pos a✝

Tactic:
rfl

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

Goal state before:
pp: case zero.zero
⊢ (zero + zero).toZNum = zero.toZNum + zero.toZNum

Tactic:
rfl

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

Goal state before:
pp: case zero.pos
a✝ : PosNum
⊢ (zero + pos a✝).toZNum = zero.toZNum + (pos a✝).toZNum

Tactic:
rfl

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

Goal state before:
pp: case pos.zero
a✝ : PosNum
⊢ (pos a✝ + zero).toZNum = (pos a✝).toZNum + zero.toZNum

Tactic:
rfl

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

Goal state before:
pp: case pos.pos
a✝¹ a✝ : PosNum
⊢ (pos a✝¹ + pos a✝).toZNum = (pos a✝¹).toZNum + (pos a✝).toZNum

Tactic:
rfl

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

Goal state before:
pp: case pos
n : PosNum
h : 1 < n
a✝ : PosNum
e : n.pred' = pos a✝
⊢ ↑(Num.casesOn (pos a✝) 1 id) = ↑(pos a✝)

Tactic:
rfl

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

Goal state before:
pp: case one
⊢ one.sub' 1 = one.pred'.toZNum

Tactic:
rfl

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

Goal state before:
pp: case bit1
a✝ : PosNum
⊢ a✝.bit1.sub' 1 = a✝.bit1.pred'.toZNum

Tactic:
rfl

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

Goal state before:
pp: case bit0
a✝ : PosNum
⊢ a✝.bit0.sub' 1 = a✝.bit0.pred'.toZNum

Tactic:
rfl

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

Goal state before:
pp: case one
⊢ sub' 1 one = one.pred'.toZNumNeg

Tactic:
rfl

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

Goal state before:
pp: case bit1
a✝ : PosNum
⊢ sub' 1 a✝.bit1 = a✝.bit1.pred'.toZNumNeg

Tactic:
rfl

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

Goal state before:
pp: case bit0
a✝ : PosNum
⊢ sub' 1 a✝.bit0 = a✝.bit0.pred'.toZNumNeg

Tactic:
rfl

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

Goal state before:
pp: p : PosNum
⊢ ↑(pos p).pred = (↑(pos p)).pred

Tactic:
rw [pred, PosNum.pred'_to_nat]

Goal state after:
p : PosNum
⊢ (↑p).pred = (↑(pos p)).pred
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: p : PosNum
⊢ (↑p).pred = (↑(pos p)).pred

Tactic:
rfl

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

Goal state before:
pp: p : PosNum
⊢ ↑p = ↑(pos p)

Tactic:
rfl

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

Goal state before:
pp: case zero.zero
⊢ (zero.cmp zero).swap = zero.cmp zero

Tactic:
rfl

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

Goal state before:
pp: case zero.pos
a✝ : PosNum
⊢ (zero.cmp (pos a✝)).swap = (pos a✝).cmp zero

Tactic:
rfl

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

Goal state before:
pp: case pos.zero
a✝ : PosNum
⊢ ((pos a✝).cmp zero).swap = zero.cmp (pos a✝)

Tactic:
rfl

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

Goal state before:
pp: case pos.pos
a✝¹ a✝ : PosNum
⊢ ((pos a✝¹).cmp (pos a✝)).swap = (pos a✝).cmp (pos a✝¹)

Tactic:
rfl

Goal state after:
case pos.pos
a✝¹ a✝ : PosNum
⊢ ((pos a✝¹).cmp (pos a✝)).swap = (pos a✝).cmp (pos a✝¹)
Module: Mathlib.Computability.RE

Goal state before:
pp: cf : Code
hf : Nat.Partrec cf.eval
cg : Code
hg : Nat.Partrec cg.eval
this : Nat.Partrec fun n ↦ rfindOpt fun k ↦ Code.evaln k cf n <|> Code.evaln k cg n
n x : ℕ
h : x ∈ rfindOpt fun k ↦ Code.evaln k cf n <|> Code.evaln k cg n
k : ℕ
e : Code.evaln k cf n = Option.some x ∨ Code.evaln k cf n = Option.none ∧ Code.evaln k cg n = Option.some x
⊢ x ∈ cf.eval n ∨ x ∈ cg.eval n

Tactic:
← Option.mem_def,

Goal state after:
cf : Code
hf : Nat.Partrec cf.eval
cg : Code
hg : Nat.Partrec cg.eval
this : Nat.Partrec fun n ↦ rfindOpt fun k ↦ Code.evaln k cf n <|> Code.evaln k cg n
n x : ℕ
h : x ∈ rfindOpt fun k ↦ Code.evaln k cf n <|> Code.evaln k cg n
k : ℕ
e : x ∈ Code.evaln k cf n ∨ Code.evaln k cf n = Option.none ∧ Code.evaln k cg n = Option.some x
⊢ x ∈ cf.eval n ∨ x ∈ cg.eval n
Module: Mathlib.Computability.PartrecBasis

Goal state before:
pp: case refine_1.e_a.zero
n✝ : ℕ
f : List.Vector ℕ (n✝ + 1) → ℕ
hf : Partrec' ↑f
v : List.Vector ℕ n✝
b a n : ℕ
⊢ ofNat (Option ℕ) 0 = none

Tactic:
rfl

Goal state after:
Module: Mathlib.Computability.PartrecBasis

Goal state before:
pp: case refine_1.e_a.succ
n✝¹ : ℕ
f : List.Vector ℕ (n✝¹ + 1) → ℕ
hf : Partrec' ↑f
v : List.Vector ℕ n✝¹
b a n n✝ : ℕ
⊢ (ofNat (Option ℕ) (n✝ + 1)).isSome = true

Tactic:
rfl

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

Goal state before:
pp: case zero.zero
f : Num → Num → Num
g : Bool → Bool → Bool
p : PosNum → PosNum → Num
gff : g false false = false
f00 : f 0 0 = 0
f0n : ∀ (n : PosNum), f 0 (pos n) = bif g false true then pos n else 0
fn0 : ∀ (n : PosNum), f (pos n) 0 = bif g true false then pos n else 0
fnn : ∀ (m n : PosNum), f (pos m) (pos n) = p m n
p11 : p 1 1 = bif g true true then 1 else 0
p1b : ∀ (b : Bool) (n : PosNum), p 1 (PosNum.bit b n) = bit (g true b) (bif g false true then pos n else 0)
pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = bit (g a true) (bif g true false then pos m else 0)
pbb : ∀ (a b : Bool) (m n : PosNum), p (PosNum.bit a m) (PosNum.bit b n) = bit (g a b) (p m n)
⊢ ↑0 = 0

Tactic:
rfl

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

Goal state before:
pp: case zero.pos.false
f : Num → Num → Num
g : Bool → Bool → Bool
p : PosNum → PosNum → Num
gff : g false false = false
f00 : f 0 0 = 0
f0n : ∀ (n : PosNum), f 0 (pos n) = bif g false true then pos n else 0
fn0 : ∀ (n : PosNum), f (pos n) 0 = bif g true false then pos n else 0
fnn : ∀ (m n : PosNum), f (pos m) (pos n) = p m n
p11 : p 1 1 = bif g true true then 1 else 0
p1b : ∀ (b : Bool) (n : PosNum), p 1 (PosNum.bit b n) = bit (g true b) (bif g false true then pos n else 0)
pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = bit (g a true) (bif g true false then pos m else 0)
pbb : ∀ (a b : Bool) (m n : PosNum), p (PosNum.bit a m) (PosNum.bit b n) = bit (g a b) (p m n)
n : PosNum
⊢ ↑(bif false then pos n else 0) = if false = true then ↑(pos n) else 0

Tactic:
rfl

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

Goal state before:
pp: case zero.pos.true
f : Num → Num → Num
g : Bool → Bool → Bool
p : PosNum → PosNum → Num
gff : g false false = false
f00 : f 0 0 = 0
f0n : ∀ (n : PosNum), f 0 (pos n) = bif g false true then pos n else 0
fn0 : ∀ (n : PosNum), f (pos n) 0 = bif g true false then pos n else 0
fnn : ∀ (m n : PosNum), f (pos m) (pos n) = p m n
p11 : p 1 1 = bif g true true then 1 else 0
p1b : ∀ (b : Bool) (n : PosNum), p 1 (PosNum.bit b n) = bit (g true b) (bif g false true then pos n else 0)
pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = bit (g a true) (bif g true false then pos m else 0)
pbb : ∀ (a b : Bool) (m n : PosNum), p (PosNum.bit a m) (PosNum.bit b n) = bit (g a b) (p m n)
n : PosNum
⊢ ↑(bif true then pos n else 0) = if true = true then ↑(pos n) else 0

Tactic:
rfl

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

Goal state before:
pp: case pos.zero.false
f : Num → Num → Num
g : Bool → Bool → Bool
p : PosNum → PosNum → Num
gff : g false false = false
f00 : f 0 0 = 0
f0n : ∀ (n : PosNum), f 0 (pos n) = bif g false true then pos n else 0
fn0 : ∀ (n : PosNum), f (pos n) 0 = bif g true false then pos n else 0
fnn : ∀ (m n : PosNum), f (pos m) (pos n) = p m n
p11 : p 1 1 = bif g true true then 1 else 0
p1b : ∀ (b : Bool) (n : PosNum), p 1 (PosNum.bit b n) = bit (g true b) (bif g false true then pos n else 0)
pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = bit (g a true) (bif g true false then pos m else 0)
pbb : ∀ (a b : Bool) (m n : PosNum), p (PosNum.bit a m) (PosNum.bit b n) = bit (g a b) (p m n)
m : PosNum
⊢ ↑(bif false then pos m else 0) = if false = true then ↑(pos m) else 0

Tactic:
rfl

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

Goal state before:
pp: case pos.zero.true
f : Num → Num → Num
g : Bool → Bool → Bool
p : PosNum → PosNum → Num
gff : g false false = false
f00 : f 0 0 = 0
f0n : ∀ (n : PosNum), f 0 (pos n) = bif g false true then pos n else 0
fn0 : ∀ (n : PosNum), f (pos n) 0 = bif g true false then pos n else 0
fnn : ∀ (m n : PosNum), f (pos m) (pos n) = p m n
p11 : p 1 1 = bif g true true then 1 else 0
p1b : ∀ (b : Bool) (n : PosNum), p 1 (PosNum.bit b n) = bit (g true b) (bif g false true then pos n else 0)
pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = bit (g a true) (bif g true false then pos m else 0)
pbb : ∀ (a b : Bool) (m n : PosNum), p (PosNum.bit a m) (PosNum.bit b n) = bit (g a b) (p m n)
m : PosNum
⊢ ↑(bif true then pos m else 0) = if true = true then ↑(pos m) else 0

Tactic:
rfl

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

Goal state before:
pp: case false
f : Num → Num → Num
g : Bool → Bool → Bool
p : PosNum → PosNum → Num
gff : g false false = false
f00 : f 0 0 = 0
f0n : ∀ (n : PosNum), f 0 (pos n) = bif g false true then pos n else 0
fn0 : ∀ (n : PosNum), f (pos n) 0 = bif g true false then pos n else 0
fnn : ∀ (m n : PosNum), f (pos m) (pos n) = p m n
p11 : p 1 1 = bif g true true then 1 else 0
p1b : ∀ (b : Bool) (n : PosNum), p 1 (PosNum.bit b n) = bit (g true b) (bif g false true then pos n else 0)
pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = bit (g a true) (bif g true false then pos m else 0)
pbb : ∀ (a b : Bool) (m n : PosNum), p (PosNum.bit a m) (PosNum.bit b n) = bit (g a b) (p m n)
m n✝ n : PosNum
⊢ (bif false then ↑n else 0) = ↑(bif false then pos n else 0)

Tactic:
rfl

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

Goal state before:
pp: case true
f : Num → Num → Num
g : Bool → Bool → Bool
p : PosNum → PosNum → Num
gff : g false false = false
f00 : f 0 0 = 0
f0n : ∀ (n : PosNum), f 0 (pos n) = bif g false true then pos n else 0
fn0 : ∀ (n : PosNum), f (pos n) 0 = bif g true false then pos n else 0
fnn : ∀ (m n : PosNum), f (pos m) (pos n) = p m n
p11 : p 1 1 = bif g true true then 1 else 0
p1b : ∀ (b : Bool) (n : PosNum), p 1 (PosNum.bit b n) = bit (g true b) (bif g false true then pos n else 0)
pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = bit (g a true) (bif g true false then pos m else 0)
pbb : ∀ (a b : Bool) (m n : PosNum), p (PosNum.bit a m) (PosNum.bit b n) = bit (g a b) (p m n)
m n✝ n : PosNum
⊢ (bif true then ↑n else 0) = ↑(bif true then pos n else 0)

Tactic:
rfl

Goal state after:
Module: Mathlib.Computability.PartrecBasis

Goal state before:
pp: case refine_2.succ
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
hf : Partrec' ↑f
v : List.Vector ℕ n
b a : ℕ
h : a ∈ Nat.rfind fun n_1 ↦ ↑(some (ofNat (Option ℕ) (f (n_1 ::ᵥ v))).isSome)
c : ℕ
this : true = (ofNat (Option ℕ) (c + 1)).isSome
⊢ some (c + 1).pred = some b ↔ ofNat (Option ℕ) (c + 1) = some b

Tactic:
rfl

Goal state after:
Module: Mathlib.Computability.StateTransition

Goal state before:
pp: σ : Type u_1
f : σ → Option σ
a b c : σ
h₁ : Reaches₁ f a c
h₂ : b ∈ f a
⊢ Reaches f b c

Tactic:
rcases TransGen.head'_iff.1 h₁ with ⟨b', hab, hbc⟩
  cases Option.mem_unique hab h₂; exact hbc

Goal state after:
Module: Mathlib.Computability.StateTransition

Goal state before:
pp: σ : Type ?u.5
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' : b ∈ PFun.fix (fun s ↦ Part.some ((f s).elim (Sum.inl s) Sum.inr)) a'
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

Goal state after:
Module: Mathlib.Computability.StateTransition

Goal state before:
pp: σ : Type u_1
f : σ → Option σ
a✝ b : σ
h✝ : b ∈ eval f a✝
a : σ
h : b ∈ eval f a
IH : ∀ (a' : σ), f a = some a' → Reaches f a' b ∧ f b = none
e : f a = none
⊢ Sum.inl ?m.69 = none.elim (Sum.inl a) Sum.inr

Tactic:
rfl

Goal state after: