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

Goal state before:
pp: case hrf
a : Primrec fun a ↦ ofNat (ℕ × Code) a.length
k✝ : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.length).1
n✝ : Primrec Prod.snd
k : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.1.length).1
n : Primrec fun a ↦ a.1.2
k' : Primrec Prod.snd
c : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.1.length).2
⊢ Primrec fun a ↦
    have z := (unpair a.1.1.2).1;
    have m := (unpair a.1.1.2).2;
    do
    let x ← lup a.1.1.1 ((ofNat (ℕ × Code) a.1.1.1.length).1, a.2.1) (Nat.pair z m)
    Nat.casesOn x (some m) fun x ↦ lup a.1.1.1 (a.1.2, (ofNat (ℕ × Code) a.1.1.1.length).2) (Nat.pair z (m + 1))

Tactic:
· have L := (Primrec.fst.comp Primrec.fst).comp
      (Primrec.fst (α := (List (List (Option ℕ)) × ℕ) × ℕ)
        (β := Code × Option ℕ))
    have k := k.comp (Primrec.fst (β := Code × Option ℕ))
    have n := n.comp (Primrec.fst (β := Code × Option ℕ))
    have cf := Primrec.fst.comp (Primrec.snd (α := (List (List (Option ℕ)) × ℕ) × ℕ)
        (β := Code × Option ℕ))
    have z := Primrec.fst.comp (Primrec.unpair.comp n)
    have m := Primrec.snd.comp (Primrec.unpair.comp n)
    have h₁ := hlup.comp <| L.pair <| (k.pair cf).pair (Primrec₂.natPair.comp z m)
    refine Primrec.option_bind h₁ (?_ : Primrec _)
    have m := m.comp (Primrec.fst (β := ℕ))
    refine Primrec.nat_casesOn Primrec.snd (Primrec.option_some.comp m) ?_
    unfold Primrec₂
    exact (hlup.comp ((L.comp Primrec.fst).pair <|
      ((k'.pair c).comp <| Primrec.fst.comp Primrec.fst).pair
        (Primrec₂.natPair.comp (z.comp Primrec.fst) (_root_.Primrec.succ.comp m)))).comp
      Primrec.fst

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

Goal state before:
pp: case zero
n : ℕ
⊢ (n.bits.headI.toNat != 0) = n.bits.headI

Tactic:
cases List.headI (bits n)

Goal state after:
case zero.false
n : ℕ
⊢ (false.toNat != 0) = false

case zero.true
n : ℕ
⊢ (true.toNat != 0) = true
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: case inr.inl
a b c : ℕ
v : ℕ := ⋯
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
⊢ c ^^^ a < b

Tactic:
rw [hca]

Goal state after:
case inr.inl
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
⊢ b ^^^ v < b
Module: Mathlib.Computability.NFA

Goal state before:
pp: case nil
α : Type u
σ : Type v
M : NFA α σ
p : Prop
S : Set σ
⊢ [] ∈ M.acceptsFrom {s | s ∈ S ∧ p} ↔ [] ∈ M.acceptsFrom S ∧ p

Tactic:
simp only [nil_mem_acceptsFrom, mem_ofPred_eq]

Goal state after:
case nil
α : Type u
σ : Type v
M : NFA α σ
p : Prop
S : Set σ
⊢ (∃ s, (s ∈ S ∧ p) ∧ s ∈ M.accept) ↔ (∃ s ∈ S, s ∈ M.accept) ∧ p
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: α : Type u_1
x : Option α
⊢ [x].reduceOption = x.toList

Tactic:
by cases x <;> rfl

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
s : σ
⊢ (∃ t ∈ S, s ∈ M.εClosure {t}) → s ∈ M.εClosure S

Tactic:
intro ⟨t, _, h⟩
    induction h <;> subst_vars <;> solve_by_elim [εClosure.step]

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
s : σ
a : α
⊢ s ∈ M.stepSet S a ↔ ∃ t ∈ S, s ∈ M.εClosure (M.step t (some a))

Tactic:
simp_rw [stepSet, mem_iUnion₂, exists_prop]

Goal state after:
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:
· exact fun ⟨w, h2, h3⟩ => ⟨w, h3, h2⟩

Goal state after:
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:
· exact fun ⟨w, h2, h3⟩ => ⟨w, h3, h2⟩

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

Tactic:
cases hx

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

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

Goal state after:
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.Data.Num.Lemmas

Goal state before:
pp: x✝ : Num
⊢ ↑x✝ * 1 = ↑x✝

Tactic:
mul_one

Goal state after:
x✝ : Num
⊢ ↑x✝ = ↑x✝
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: x✝² x✝¹ x✝ : Num
⊢ x✝² * (x✝¹ + x✝) = x✝² * x✝¹ + x✝² * x✝

Tactic:
simp only [← to_nat_inj, mul_to_nat, add_to_nat, mul_add]

Goal state after:
Module: Mathlib.Computability.RE

Goal state before:
pp: case inr
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 : ℕ
this : ∀ x ∈ rfindOpt fun k ↦ Code.evaln k cf n <|> Code.evaln k cg n, x ∈ cf.eval n ∨ x ∈ cg.eval n
x k : ℕ
e : Code.evaln k cg n = Option.some x
⊢ ∃ n_1 a, a ∈ (Code.evaln n_1 cf n <|> Code.evaln n_1 cg n)

Tactic:
refine ⟨k, ?_⟩
    rcases cf.evaln k n with - | y
    · exact ⟨x, by simp [e]⟩
    · exact ⟨y, by simp⟩

Goal state after:
Module: Mathlib.Computability.PartrecBasis

Goal state before:
pp: case refine_2
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)
this : true ∈ ↑(some (ofNat (Option ℕ) (f (a ::ᵥ v))).isSome)
⊢ b = (f (a ::ᵥ v)).pred ↔ ofNat (Option ℕ) (f (a ::ᵥ v)) = some b

Tactic:
simp only [Part.coe_some, Part.mem_some_iff] at this

Goal state after:
case refine_2
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)
this : true = (ofNat (Option ℕ) (f (a ::ᵥ v))).isSome
⊢ b = (f (a ::ᵥ v)).pred ↔ ofNat (Option ℕ) (f (a ::ᵥ v)) = some b
Module: Mathlib.Computability.RE

Goal state before:
pp: α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ x ∈ k a,
        (x ∈ (↑(decode₂ α a)).bind fun a ↦ Part.map encode (f a)) ∨
          x ∈ (↑(decode₂ α a)).bind fun a ↦ Part.map encode (g a)) ∧
      ((k a).Dom ↔
        ((↑(decode₂ α a)).bind fun a ↦ Part.map encode (f a)).Dom ∨
          ((↑(decode₂ α a)).bind fun a ↦ Part.map encode (g a)).Dom)
k' : α → Part σ := fun a ↦ (k (encode a)).bind fun n ↦ ↑(decode n)
a : α
this : ∀ x ∈ k' a, x ∈ f a ∨ x ∈ g a
h : (f a).Dom ∨ (g a).Dom
⊢ ((↑(decode₂ α (encode a))).bind fun a ↦ Part.map encode (f a)).Dom ∨
    ((↑(decode₂ α (encode a))).bind fun a ↦ Part.map encode (g a)).Dom

Tactic:
by simpa only [encodek₂, bind_some, coe_some] using! h

Goal state after:
Module: Mathlib.Computability.RE

Goal state before:
pp: case inl
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
H : ∀ (a : α), ∀ x ∈ f a, ∀ y ∈ g a, x = y
k : α →. σ
hk : Partrec k
K : ∀ (a : α), (∀ x ∈ k a, x ∈ f a ∨ x ∈ g a) ∧ ((k a).Dom ↔ (f a).Dom ∨ (g a).Dom)
a : α
x : σ
this : (k a).Dom
h : x ∈ f a
⊢ (k a).get this = x

Tactic:
rcases (K _).1 _ ⟨this, rfl⟩ with h' | h'

Goal state after:
case inl.inl
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
H : ∀ (a : α), ∀ x ∈ f a, ∀ y ∈ g a, x = y
k : α →. σ
hk : Partrec k
K : ∀ (a : α), (∀ x ∈ k a, x ∈ f a ∨ x ∈ g a) ∧ ((k a).Dom ↔ (f a).Dom ∨ (g a).Dom)
a : α
x : σ
this : (k a).Dom
h : x ∈ f a
h' : (k a).get this ∈ f a
⊢ (k a).get this = x

case inl.inr
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
H : ∀ (a : α), ∀ x ∈ f a, ∀ y ∈ g a, x = y
k : α →. σ
hk : Partrec k
K : ∀ (a : α), (∀ x ∈ k a, x ∈ f a ∨ x ∈ g a) ∧ ((k a).Dom ↔ (f a).Dom ∨ (g a).Dom)
a : α
x : σ
this : (k a).Dom
h : x ∈ f a
h' : (k a).get this ∈ g a
⊢ (k a).get this = x
Module: Mathlib.Computability.RE

Goal state before:
pp: case inr
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
H : ∀ (a : α), ∀ x ∈ f a, ∀ y ∈ g a, x = y
k : α →. σ
hk : Partrec k
K : ∀ (a : α), (∀ x ∈ k a, x ∈ f a ∨ x ∈ g a) ∧ ((k a).Dom ↔ (f a).Dom ∨ (g a).Dom)
a : α
x : σ
this : (k a).Dom
h : x ∈ g a
⊢ (k a).get this = x

Tactic:
rcases (K _).1 _ ⟨this, rfl⟩ with h' | h'

Goal state after:
case inr.inl
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
H : ∀ (a : α), ∀ x ∈ f a, ∀ y ∈ g a, x = y
k : α →. σ
hk : Partrec k
K : ∀ (a : α), (∀ x ∈ k a, x ∈ f a ∨ x ∈ g a) ∧ ((k a).Dom ↔ (f a).Dom ∨ (g a).Dom)
a : α
x : σ
this : (k a).Dom
h : x ∈ g a
h' : (k a).get this ∈ f a
⊢ (k a).get this = x

case inr.inr
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
H : ∀ (a : α), ∀ x ∈ f a, ∀ y ∈ g a, x = y
k : α →. σ
hk : Partrec k
K : ∀ (a : α), (∀ x ∈ k a, x ∈ f a ∨ x ∈ g a) ∧ ((k a).Dom ↔ (f a).Dom ∨ (g a).Dom)
a : α
x : σ
this : (k a).Dom
h : x ∈ g a
h' : (k a).get this ∈ g a
⊢ (k a).get this = x
Module: Mathlib.Computability.RE

Goal state before:
pp: α : Type u_1
inst✝¹ : Primcodable α
P : α → ℕ → Prop
inst✝ : DecidableRel P
hP_comp : ComputablePred fun p ↦ P p.1 p.2
hP_ex : ∀ (x : α), ∃ n, P x n
h : Partrec fun x ↦ Nat.rfind fun n ↦ Part.some (decide (P x n))
⊢ Computable fun x ↦ Nat.find ⋯

Tactic:
refine h.of_eq_tot fun x ↦ ?_

Goal state after:
α : Type u_1
inst✝¹ : Primcodable α
P : α → ℕ → Prop
inst✝ : DecidableRel P
hP_comp : ComputablePred fun p ↦ P p.1 p.2
hP_ex : ∀ (x : α), ∃ n, P x n
h : Partrec fun x ↦ Nat.rfind fun n ↦ Part.some (decide (P x n))
x : α
⊢ Nat.find ⋯ ∈ Nat.rfind fun n ↦ Part.some (decide (P x n))
Module: Mathlib.Computability.RecursiveIn

Goal state before:
pp: case prec
f : ℕ →. ℕ
O : Set (ℕ →. ℕ)
hO : ∀ g ∈ O, Nat.Partrec g
f✝ h✝ : ℕ →. ℕ
hf✝ : Nat.RecursiveIn O f✝
hh✝ : Nat.RecursiveIn O h✝
ih₁ : Nat.Partrec f✝
ih₂ : Nat.Partrec h✝
⊢ Nat.Partrec fun p ↦
    match unpair p with
    | (a, n) =>
      Nat.rec (f✝ a)
        (fun y IH ↦ do
          let i ← IH
          h✝ (Nat.pair a (Nat.pair y i)))
        n

Tactic:
| prec _ _ ih₁ ih₂ =>

Goal state after:
Module: Mathlib.Computability.RecursiveIn

Goal state before:
pp: case prec
f : ℕ →. ℕ
O : Set (ℕ →. ℕ)
f✝ g✝ : ℕ →. ℕ
a✝¹ : Nat.Partrec f✝
a✝ : Nat.Partrec g✝
ih₁ : Nat.RecursiveIn O f✝
ih₂ : Nat.RecursiveIn O g✝
⊢ Nat.RecursiveIn O
    (unpaired fun a n ↦
      Nat.rec (f✝ a)
        (fun y IH ↦ do
          let i ← IH
          g✝ (Nat.pair a (Nat.pair y i)))
        n)

Tactic:
| prec _ _ ih₁ ih₂ =>

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

Goal state before:
pp: case gff
⊢ (false || false) = false

Tactic:
try rintro (_ | _)

Goal state after:
case gff
⊢ (false || false) = false
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case f00
⊢ 0 ||| 0 = 0

Tactic:
try rintro (_ | _)

Goal state after:
case f00
⊢ 0 ||| 0 = 0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case f0n
⊢ ∀ (n : PosNum), 0 ||| pos n = bif false || true then pos n else 0

Tactic:
try rintro (_ | _)

Goal state after:
case f0n.one
⊢ 0 ||| pos one = bif false || true then pos one else 0

case f0n.bit1
a✝ : PosNum
⊢ 0 ||| pos a✝.bit1 = bif false || true then pos a✝.bit1 else 0

case f0n.bit0
a✝ : PosNum
⊢ 0 ||| pos a✝.bit0 = bif false || true then pos a✝.bit0 else 0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case fn0
⊢ ∀ (n : PosNum), pos n ||| 0 = bif true || false then pos n else 0

Tactic:
try rintro (_ | _)

Goal state after:
case fn0.one
⊢ pos one ||| 0 = bif true || false then pos one else 0

case fn0.bit1
a✝ : PosNum
⊢ pos a✝.bit1 ||| 0 = bif true || false then pos a✝.bit1 else 0

case fn0.bit0
a✝ : PosNum
⊢ pos a✝.bit0 ||| 0 = bif true || false then pos a✝.bit0 else 0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case fnn
⊢ ∀ (m n : PosNum), pos m ||| pos n = pos (m.lor n)

Tactic:
try rintro (_ | _)

Goal state after:
case fnn.one
⊢ ∀ (n : PosNum), pos one ||| pos n = pos (one.lor n)

case fnn.bit1
a✝ : PosNum
⊢ ∀ (n : PosNum), pos a✝.bit1 ||| pos n = pos (a✝.bit1.lor n)

case fnn.bit0
a✝ : PosNum
⊢ ∀ (n : PosNum), pos a✝.bit0 ||| pos n = pos (a✝.bit0.lor n)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case p11
⊢ pos (lor 1 1) = bif true || true then 1 else 0

Tactic:
try rintro (_ | _)

Goal state after:
case p11
⊢ pos (lor 1 1) = bif true || true then 1 else 0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case p1b
⊢ ∀ (b : Bool) (n : PosNum), pos (lor 1 (PosNum.bit b n)) = bit (true || b) (bif false || true then pos n else 0)

Tactic:
try rintro (_ | _)

Goal state after:
case p1b.false
⊢ ∀ (n : PosNum), pos (lor 1 (PosNum.bit false n)) = bit (true || false) (bif false || true then pos n else 0)

case p1b.true
⊢ ∀ (n : PosNum), pos (lor 1 (PosNum.bit true n)) = bit (true || true) (bif false || true then pos n else 0)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pb1
⊢ ∀ (a : Bool) (m : PosNum), pos ((PosNum.bit a m).lor 1) = bit (a || true) (bif true || false then pos m else 0)

Tactic:
try rintro (_ | _)

Goal state after:
case pb1.false
⊢ ∀ (m : PosNum), pos ((PosNum.bit false m).lor 1) = bit (false || true) (bif true || false then pos m else 0)

case pb1.true
⊢ ∀ (m : PosNum), pos ((PosNum.bit true m).lor 1) = bit (true || true) (bif true || false then pos m else 0)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pbb
⊢ ∀ (a b : Bool) (m n : PosNum), pos ((PosNum.bit a m).lor (PosNum.bit b n)) = bit (a || b) (pos (m.lor n))

Tactic:
try rintro (_ | _)

Goal state after:
case pbb.false
⊢ ∀ (b : Bool) (m n : PosNum), pos ((PosNum.bit false m).lor (PosNum.bit b n)) = bit (false || b) (pos (m.lor n))

case pbb.true
⊢ ∀ (b : Bool) (m n : PosNum), pos ((PosNum.bit true m).lor (PosNum.bit b n)) = bit (true || b) (pos (m.lor n))
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case f0n.one
⊢ 0 ||| pos one = bif false || true then pos one else 0

Tactic:
try rintro (_ | _)

Goal state after:
case f0n.one
⊢ 0 ||| pos one = bif false || true then pos one else 0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case f0n.bit1
a✝ : PosNum
⊢ 0 ||| pos a✝.bit1 = bif false || true then pos a✝.bit1 else 0

Tactic:
try rintro (_ | _)

Goal state after:
case f0n.bit1
a✝ : PosNum
⊢ 0 ||| pos a✝.bit1 = bif false || true then pos a✝.bit1 else 0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case f0n.bit0
a✝ : PosNum
⊢ 0 ||| pos a✝.bit0 = bif false || true then pos a✝.bit0 else 0

Tactic:
try rintro (_ | _)

Goal state after:
case f0n.bit0
a✝ : PosNum
⊢ 0 ||| pos a✝.bit0 = bif false || true then pos a✝.bit0 else 0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case fn0.one
⊢ pos one ||| 0 = bif true || false then pos one else 0

Tactic:
try rintro (_ | _)

Goal state after:
case fn0.one
⊢ pos one ||| 0 = bif true || false then pos one else 0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case fn0.bit1
a✝ : PosNum
⊢ pos a✝.bit1 ||| 0 = bif true || false then pos a✝.bit1 else 0

Tactic:
try rintro (_ | _)

Goal state after:
case fn0.bit1
a✝ : PosNum
⊢ pos a✝.bit1 ||| 0 = bif true || false then pos a✝.bit1 else 0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case fn0.bit0
a✝ : PosNum
⊢ pos a✝.bit0 ||| 0 = bif true || false then pos a✝.bit0 else 0

Tactic:
try rintro (_ | _)

Goal state after:
case fn0.bit0
a✝ : PosNum
⊢ pos a✝.bit0 ||| 0 = bif true || false then pos a✝.bit0 else 0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case fnn.one
⊢ ∀ (n : PosNum), pos one ||| pos n = pos (one.lor n)

Tactic:
try rintro (_ | _)

Goal state after:
case fnn.one.one
⊢ pos one ||| pos one = pos (one.lor one)

case fnn.one.bit1
a✝ : PosNum
⊢ pos one ||| pos a✝.bit1 = pos (one.lor a✝.bit1)

case fnn.one.bit0
a✝ : PosNum
⊢ pos one ||| pos a✝.bit0 = pos (one.lor a✝.bit0)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case fnn.bit1
a✝ : PosNum
⊢ ∀ (n : PosNum), pos a✝.bit1 ||| pos n = pos (a✝.bit1.lor n)

Tactic:
try rintro (_ | _)

Goal state after:
case fnn.bit1.one
a✝ : PosNum
⊢ pos a✝.bit1 ||| pos one = pos (a✝.bit1.lor one)

case fnn.bit1.bit1
a✝¹ a✝ : PosNum
⊢ pos a✝¹.bit1 ||| pos a✝.bit1 = pos (a✝¹.bit1.lor a✝.bit1)

case fnn.bit1.bit0
a✝¹ a✝ : PosNum
⊢ pos a✝¹.bit1 ||| pos a✝.bit0 = pos (a✝¹.bit1.lor a✝.bit0)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case fnn.bit0
a✝ : PosNum
⊢ ∀ (n : PosNum), pos a✝.bit0 ||| pos n = pos (a✝.bit0.lor n)

Tactic:
try rintro (_ | _)

Goal state after:
case fnn.bit0.one
a✝ : PosNum
⊢ pos a✝.bit0 ||| pos one = pos (a✝.bit0.lor one)

case fnn.bit0.bit1
a✝¹ a✝ : PosNum
⊢ pos a✝¹.bit0 ||| pos a✝.bit1 = pos (a✝¹.bit0.lor a✝.bit1)

case fnn.bit0.bit0
a✝¹ a✝ : PosNum
⊢ pos a✝¹.bit0 ||| pos a✝.bit0 = pos (a✝¹.bit0.lor a✝.bit0)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case p1b.false
⊢ ∀ (n : PosNum), pos (lor 1 (PosNum.bit false n)) = bit (true || false) (bif false || true then pos n else 0)

Tactic:
try rintro (_ | _)

Goal state after:
case p1b.false.one
⊢ pos (lor 1 (PosNum.bit false one)) = bit (true || false) (bif false || true then pos one else 0)

case p1b.false.bit1
a✝ : PosNum
⊢ pos (lor 1 (PosNum.bit false a✝.bit1)) = bit (true || false) (bif false || true then pos a✝.bit1 else 0)

case p1b.false.bit0
a✝ : PosNum
⊢ pos (lor 1 (PosNum.bit false a✝.bit0)) = bit (true || false) (bif false || true then pos a✝.bit0 else 0)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case p1b.true
⊢ ∀ (n : PosNum), pos (lor 1 (PosNum.bit true n)) = bit (true || true) (bif false || true then pos n else 0)

Tactic:
try rintro (_ | _)

Goal state after:
case p1b.true.one
⊢ pos (lor 1 (PosNum.bit true one)) = bit (true || true) (bif false || true then pos one else 0)

case p1b.true.bit1
a✝ : PosNum
⊢ pos (lor 1 (PosNum.bit true a✝.bit1)) = bit (true || true) (bif false || true then pos a✝.bit1 else 0)

case p1b.true.bit0
a✝ : PosNum
⊢ pos (lor 1 (PosNum.bit true a✝.bit0)) = bit (true || true) (bif false || true then pos a✝.bit0 else 0)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pb1.false
⊢ ∀ (m : PosNum), pos ((PosNum.bit false m).lor 1) = bit (false || true) (bif true || false then pos m else 0)

Tactic:
try rintro (_ | _)

Goal state after:
case pb1.false.one
⊢ pos ((PosNum.bit false one).lor 1) = bit (false || true) (bif true || false then pos one else 0)

case pb1.false.bit1
a✝ : PosNum
⊢ pos ((PosNum.bit false a✝.bit1).lor 1) = bit (false || true) (bif true || false then pos a✝.bit1 else 0)

case pb1.false.bit0
a✝ : PosNum
⊢ pos ((PosNum.bit false a✝.bit0).lor 1) = bit (false || true) (bif true || false then pos a✝.bit0 else 0)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pb1.true
⊢ ∀ (m : PosNum), pos ((PosNum.bit true m).lor 1) = bit (true || true) (bif true || false then pos m else 0)

Tactic:
try rintro (_ | _)

Goal state after:
case pb1.true.one
⊢ pos ((PosNum.bit true one).lor 1) = bit (true || true) (bif true || false then pos one else 0)

case pb1.true.bit1
a✝ : PosNum
⊢ pos ((PosNum.bit true a✝.bit1).lor 1) = bit (true || true) (bif true || false then pos a✝.bit1 else 0)

case pb1.true.bit0
a✝ : PosNum
⊢ pos ((PosNum.bit true a✝.bit0).lor 1) = bit (true || true) (bif true || false then pos a✝.bit0 else 0)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pbb.false
⊢ ∀ (b : Bool) (m n : PosNum), pos ((PosNum.bit false m).lor (PosNum.bit b n)) = bit (false || b) (pos (m.lor n))

Tactic:
try rintro (_ | _)

Goal state after:
case pbb.false.false
⊢ ∀ (m n : PosNum), pos ((PosNum.bit false m).lor (PosNum.bit false n)) = bit (false || false) (pos (m.lor n))

case pbb.false.true
⊢ ∀ (m n : PosNum), pos ((PosNum.bit false m).lor (PosNum.bit true n)) = bit (false || true) (pos (m.lor n))
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pbb.true
⊢ ∀ (b : Bool) (m n : PosNum), pos ((PosNum.bit true m).lor (PosNum.bit b n)) = bit (true || b) (pos (m.lor n))

Tactic:
try rintro (_ | _)

Goal state after:
case pbb.true.false
⊢ ∀ (m n : PosNum), pos ((PosNum.bit true m).lor (PosNum.bit false n)) = bit (true || false) (pos (m.lor n))

case pbb.true.true
⊢ ∀ (m n : PosNum), pos ((PosNum.bit true m).lor (PosNum.bit true n)) = bit (true || true) (pos (m.lor n))
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: case comp
α : Type u_1
inst✝ : DecidableEq α
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'

Tactic:
| comp P Q ih₁ ih₂ =>

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

Goal state before:
pp: case pos.succ.bit0
n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
m : PosNum
⊢ ↑(m.shiftr n) = ↑(pos m.bit0) >>> (n + 1)

Tactic:
trans
    · apply IH
    change Nat.shiftRight m n = Nat.shiftRight (m + m) (n + 1)
    rw [add_comm n 1, @Nat.shiftRight_eq _ (1 + n), Nat.shiftRight_add]
    apply congr_arg fun x => Nat.shiftRight x n
    simp [-add_assoc, Nat.shiftRight_succ, Nat.shiftRight_zero, ← Nat.div2_val, hdiv2]

Goal state after: