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

Goal state before:
pp: case pos.pos.bit0.one
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)
this : ∀ (b : Bool) (n : PosNum), (bif b then ↑n else 0) = ↑(bif b then pos n else 0)
this' : ∀ (b : Bool) (n : PosNum), ↑(pos (PosNum.bit b n)) = Nat.bit b ↑n
m : PosNum
IH : ∀ (n : PosNum), ↑(p m n) = Nat.bitwise g ↑(pos m) ↑(pos n)
⊢ ↑(p (PosNum.bit false m) 1) = Nat.bitwise g (Nat.bit false ↑m) (Nat.bit true 0)

Tactic:
this'

Goal state after:
case pos.pos.bit0.one
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)
this : ∀ (b : Bool) (n : PosNum), (bif b then ↑n else 0) = ↑(bif b then pos n else 0)
this' : ∀ (b : Bool) (n : PosNum), ↑(pos (PosNum.bit b n)) = Nat.bit b ↑n
m : PosNum
IH : ∀ (n : PosNum), ↑(p m n) = Nat.bitwise g ↑(pos m) ↑(pos n)
⊢ ↑(p (PosNum.bit false m) 1) = Nat.bitwise g (Nat.bit false ↑m) (Nat.bit true 0)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pos.pos.bit0.bit1
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)
this : ∀ (b : Bool) (n : PosNum), (bif b then ↑n else 0) = ↑(bif b then pos n else 0)
this' : ∀ (b : Bool) (n : PosNum), ↑(pos (PosNum.bit b n)) = Nat.bit b ↑n
m : PosNum
IH : ∀ (n : PosNum), ↑(p m n) = Nat.bitwise g ↑(pos m) ↑(pos n)
n : PosNum
⊢ ↑(p (PosNum.bit false m) (PosNum.bit true n)) = Nat.bitwise g ↑(pos (PosNum.bit false m)) ↑(pos (PosNum.bit true n))

Tactic:
this'

Goal state after:
case pos.pos.bit0.bit1
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)
this : ∀ (b : Bool) (n : PosNum), (bif b then ↑n else 0) = ↑(bif b then pos n else 0)
this' : ∀ (b : Bool) (n : PosNum), ↑(pos (PosNum.bit b n)) = Nat.bit b ↑n
m : PosNum
IH : ∀ (n : PosNum), ↑(p m n) = Nat.bitwise g ↑(pos m) ↑(pos n)
n : PosNum
⊢ ↑(p (PosNum.bit false m) (PosNum.bit true n)) = Nat.bitwise g (Nat.bit false ↑m) ↑(pos (PosNum.bit true n))
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pos.pos.bit0.bit1
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)
this : ∀ (b : Bool) (n : PosNum), (bif b then ↑n else 0) = ↑(bif b then pos n else 0)
this' : ∀ (b : Bool) (n : PosNum), ↑(pos (PosNum.bit b n)) = Nat.bit b ↑n
m : PosNum
IH : ∀ (n : PosNum), ↑(p m n) = Nat.bitwise g ↑(pos m) ↑(pos n)
n : PosNum
⊢ ↑(p (PosNum.bit false m) (PosNum.bit true n)) = Nat.bitwise g (Nat.bit false ↑m) ↑(pos (PosNum.bit true n))

Tactic:
this'

Goal state after:
case pos.pos.bit0.bit1
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)
this : ∀ (b : Bool) (n : PosNum), (bif b then ↑n else 0) = ↑(bif b then pos n else 0)
this' : ∀ (b : Bool) (n : PosNum), ↑(pos (PosNum.bit b n)) = Nat.bit b ↑n
m : PosNum
IH : ∀ (n : PosNum), ↑(p m n) = Nat.bitwise g ↑(pos m) ↑(pos n)
n : PosNum
⊢ ↑(p (PosNum.bit false m) (PosNum.bit true n)) = Nat.bitwise g (Nat.bit false ↑m) (Nat.bit true ↑n)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pos.pos.bit0.bit1
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)
this : ∀ (b : Bool) (n : PosNum), (bif b then ↑n else 0) = ↑(bif b then pos n else 0)
this' : ∀ (b : Bool) (n : PosNum), ↑(pos (PosNum.bit b n)) = Nat.bit b ↑n
m : PosNum
IH : ∀ (n : PosNum), ↑(p m n) = Nat.bitwise g ↑(pos m) ↑(pos n)
n : PosNum
⊢ ↑(p (PosNum.bit false m) (PosNum.bit true n)) = Nat.bitwise g (Nat.bit false ↑m) (Nat.bit true ↑n)

Tactic:
this'

Goal state after:
case pos.pos.bit0.bit1
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)
this : ∀ (b : Bool) (n : PosNum), (bif b then ↑n else 0) = ↑(bif b then pos n else 0)
this' : ∀ (b : Bool) (n : PosNum), ↑(pos (PosNum.bit b n)) = Nat.bit b ↑n
m : PosNum
IH : ∀ (n : PosNum), ↑(p m n) = Nat.bitwise g ↑(pos m) ↑(pos n)
n : PosNum
⊢ ↑(p (PosNum.bit false m) (PosNum.bit true n)) = Nat.bitwise g (Nat.bit false ↑m) (Nat.bit true ↑n)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pos.pos.bit0.bit0
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)
this : ∀ (b : Bool) (n : PosNum), (bif b then ↑n else 0) = ↑(bif b then pos n else 0)
this' : ∀ (b : Bool) (n : PosNum), ↑(pos (PosNum.bit b n)) = Nat.bit b ↑n
m : PosNum
IH : ∀ (n : PosNum), ↑(p m n) = Nat.bitwise g ↑(pos m) ↑(pos n)
n : PosNum
⊢ ↑(p (PosNum.bit false m) (PosNum.bit false n)) = Nat.bitwise g ↑(pos (PosNum.bit false m)) ↑(pos (PosNum.bit false n))

Tactic:
this'

Goal state after:
case pos.pos.bit0.bit0
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)
this : ∀ (b : Bool) (n : PosNum), (bif b then ↑n else 0) = ↑(bif b then pos n else 0)
this' : ∀ (b : Bool) (n : PosNum), ↑(pos (PosNum.bit b n)) = Nat.bit b ↑n
m : PosNum
IH : ∀ (n : PosNum), ↑(p m n) = Nat.bitwise g ↑(pos m) ↑(pos n)
n : PosNum
⊢ ↑(p (PosNum.bit false m) (PosNum.bit false n)) = Nat.bitwise g (Nat.bit false ↑m) ↑(pos (PosNum.bit false n))
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pos.pos.bit0.bit0
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)
this : ∀ (b : Bool) (n : PosNum), (bif b then ↑n else 0) = ↑(bif b then pos n else 0)
this' : ∀ (b : Bool) (n : PosNum), ↑(pos (PosNum.bit b n)) = Nat.bit b ↑n
m : PosNum
IH : ∀ (n : PosNum), ↑(p m n) = Nat.bitwise g ↑(pos m) ↑(pos n)
n : PosNum
⊢ ↑(p (PosNum.bit false m) (PosNum.bit false n)) = Nat.bitwise g (Nat.bit false ↑m) ↑(pos (PosNum.bit false n))

Tactic:
this'

Goal state after:
case pos.pos.bit0.bit0
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)
this : ∀ (b : Bool) (n : PosNum), (bif b then ↑n else 0) = ↑(bif b then pos n else 0)
this' : ∀ (b : Bool) (n : PosNum), ↑(pos (PosNum.bit b n)) = Nat.bit b ↑n
m : PosNum
IH : ∀ (n : PosNum), ↑(p m n) = Nat.bitwise g ↑(pos m) ↑(pos n)
n : PosNum
⊢ ↑(p (PosNum.bit false m) (PosNum.bit false n)) = Nat.bitwise g (Nat.bit false ↑m) (Nat.bit false ↑n)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pos.pos.bit0.bit0
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)
this : ∀ (b : Bool) (n : PosNum), (bif b then ↑n else 0) = ↑(bif b then pos n else 0)
this' : ∀ (b : Bool) (n : PosNum), ↑(pos (PosNum.bit b n)) = Nat.bit b ↑n
m : PosNum
IH : ∀ (n : PosNum), ↑(p m n) = Nat.bitwise g ↑(pos m) ↑(pos n)
n : PosNum
⊢ ↑(p (PosNum.bit false m) (PosNum.bit false n)) = Nat.bitwise g (Nat.bit false ↑m) (Nat.bit false ↑n)

Tactic:
this'

Goal state after:
case pos.pos.bit0.bit0
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)
this : ∀ (b : Bool) (n : PosNum), (bif b then ↑n else 0) = ↑(bif b then pos n else 0)
this' : ∀ (b : Bool) (n : PosNum), ↑(pos (PosNum.bit b n)) = Nat.bit b ↑n
m : PosNum
IH : ∀ (n : PosNum), ↑(p m n) = Nat.bitwise g ↑(pos m) ↑(pos n)
n : PosNum
⊢ ↑(p (PosNum.bit false m) (PosNum.bit false n)) = Nat.bitwise g (Nat.bit false ↑m) (Nat.bit false ↑n)
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: Γ : Type u_1
inst✝¹ : Inhabited Γ
inst✝ : Finite Γ
n : ℕ
e : Γ ≃ Fin n
this : DecidableEq Γ := e.decidableEq
G : Fin n ↪ Fin n → Bool := { toFun := fun a b ↦ decide (a = b), inj' := ⋯ }
⊢ ∃ n enc dec, enc default = List.Vector.replicate n false ∧ ∀ (a : Γ), dec (enc a) = a

Tactic:
let H := (e.toEmbedding.trans G).trans (Equiv.vectorEquivFin _ _).symm.toEmbedding

Goal state after:
Γ : Type u_1
inst✝¹ : Inhabited Γ
inst✝ : Finite Γ
n : ℕ
e : Γ ≃ Fin n
this : DecidableEq Γ := e.decidableEq
G : Fin n ↪ Fin n → Bool := { toFun := fun a b ↦ decide (a = b), inj' := ⋯ }
H : Γ ↪ List.Vector Bool n := (e.toEmbedding.trans G).trans (Equiv.vectorEquivFin Bool n).symm.toEmbedding
⊢ ∃ n enc dec, enc default = List.Vector.replicate n false ∧ ∀ (a : Γ), dec (enc a) = a
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)