awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m n : Num
lt :
  ∀ (this : Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) Ordering.lt (m < n) (m = n) (n < m)),
    Ordering.lt = Ordering.eq ↔ m = n
eq :
  ∀ (this : Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) Ordering.eq (m < n) (m = n) (n < m)),
    Ordering.eq = Ordering.eq ↔ m = n
gt :
  ∀ (this : Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) Ordering.gt (m < n) (m = n) (n < m)),
    Ordering.gt = Ordering.eq ↔ m = n
⊢ ∀ (this : Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) (m.cmp n) (m < n) (m = n) (n < m)),
    m.cmp n = Ordering.eq ↔ m = n

Tactic:
cases cmp m n

Premises used: Num.cmp
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m n : Num
⊢ ∀ (this : Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) Ordering.lt (m < n) (m = n) (n < m)),
    Ordering.lt = Ordering.eq ↔ m = n

Tactic:
simp_all [LT.lt.ne, LT.lt.ne']

Premises used: LT.lt.ne', LT.lt.ne
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m n : Num
⊢ ∀ (this : Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) Ordering.eq (m < n) (m = n) (n < m)),
    Ordering.eq = Ordering.eq ↔ m = n

Tactic:
simp_all [LT.lt.ne, LT.lt.ne']

Premises used: LT.lt.ne', LT.lt.ne
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m n : Num
⊢ ∀ (this : Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) Ordering.gt (m < n) (m = n) (n < m)),
    Ordering.gt = Ordering.eq ↔ m = n

Tactic:
simp_all [LT.lt.ne, LT.lt.ne']

Premises used: LT.lt.ne', LT.lt.ne
-- Module: Mathlib.Data.Num.Lemmas
Goal:
α : Type u_1
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : IsStrictOrderedRing α
m n : Num
rw : LT.lt.{u_1} (α := α) (↑(↑m : ℕ) : α) (↑n : α) ↔ m < n
rw₁ : LT.lt.{u_1} (α := α) (↑(↑m : ℕ) : α) (↑(↑n : ℕ) : α) ↔ m < n
rw₂ : LT.lt (α := ℕ) (↑m : ℕ) (↑n : ℕ) ↔ m < n
rw₃ rw₄ : m < n ↔ m < n
⊢ LT.lt.{u_1} (α := α) (↑m : α) (↑n : α) ↔ m < n

Tactic:
rw [← cast_to_nat m, ← cast_to_nat n, Nat.cast_lt (α := α), lt_to_nat]

Premises used: Num.cast_to_nat, Num.lt_to_nat, Nat.cast_lt
-- Module: Mathlib.Data.Num.Lemmas
Goal:
α : Type u_1
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
m n : Num
rw : ¬LT.lt.{u_1} (α := α) (↑n : α) (↑m : α) ↔ m ≤ n
⊢ LE.le.{u_1} (α := α) (↑m : α) (↑n : α) ↔ m ≤ n

Tactic:
rw [← not_lt]

Premises used: not_lt
-- Module: Mathlib.Data.Num.Lemmas
Goal:
α : Type u_1
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
m n : Num
⊢ ¬LT.lt.{u_1} (α := α) (↑n : α) (↑m : α) ↔ m ≤ n

Tactic:
not_congr cast_lt

Premises used: Num.cast_lt, not_congr
-- Module: Mathlib.Data.Num.Lemmas
Goal:
α : Type u_1
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
m n : Num
⊢ ¬LT.lt.{u_1} (α := α) (↑n : α) (↑m : α) ↔ m ≤ n

Tactic:
exact not_congr cast_lt

Premises used: Num.cast_lt, not_congr
-- Module: Mathlib.Data.Num.Lemmas
Goal:
α : Type u_1
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : IsStrictOrderedRing α
m n : Num
rw : Eq.{u_1 + 1} (α := α) (↑(↑m : ℕ) : α) (↑n : α) ↔ m = n
rw₁ : Eq.{u_1 + 1} (α := α) (↑(↑m : ℕ) : α) (↑(↑n : ℕ) : α) ↔ m = n
rw₂ : Eq (α := ℕ) (↑m : ℕ) (↑n : ℕ) ↔ m = n
rw₃ rw₄ : m = n ↔ m = n
⊢ Eq.{u_1 + 1} (α := α) (↑m : α) (↑n : α) ↔ m = n

Tactic:
rw [← cast_to_nat m, ← cast_to_nat n, Nat.cast_inj, to_nat_inj]

Premises used: Num.cast_to_nat, Nat.cast_inj, Num.to_nat_inj
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m n : Num
⊢ m < n ↔ m.cmp n = Ordering.lt

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m n : Num
rw : (m.cmp n).swap = Ordering.lt ↔ m.cmp n = Ordering.gt
⊢ n.cmp m = Ordering.lt ↔ m.cmp n = Ordering.gt

Tactic:
rw [← cmp_swap]

Premises used: Num.cmp_swap
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m n : Num
lt : Ordering.lt.swap = Ordering.lt ↔ Ordering.lt = Ordering.gt
eq : Ordering.eq.swap = Ordering.lt ↔ Ordering.eq = Ordering.gt
gt : Ordering.gt.swap = Ordering.lt ↔ Ordering.gt = Ordering.gt
⊢ (m.cmp n).swap = Ordering.lt ↔ m.cmp n = Ordering.gt

Tactic:
cases cmp m n

Premises used: Num.cmp
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m n : Num
⊢ Ordering.lt.swap = Ordering.lt ↔ Ordering.lt = Ordering.gt

Tactic:
decide
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m n : Num
⊢ Ordering.eq.swap = Ordering.lt ↔ Ordering.eq = Ordering.gt

Tactic:
decide
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m n : Num
⊢ Ordering.gt.swap = Ordering.lt ↔ Ordering.gt = Ordering.gt

Tactic:
decide
-- Module: Mathlib.Data.Num.Lemmas
Goal:
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 (Num.pos n) = bif g false true then Num.pos n else 0
fn0 : ∀ (n : PosNum), f (Num.pos n) 0 = bif g true false then Num.pos n else 0
fnn : ∀ (m n : PosNum), f (Num.pos m) (Num.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 Num.pos n else 0)
pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = bit (g a true) (bif g true false then Num.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 : Num
zero : (↑(f Num.zero n) : ℕ) = Nat.bitwise g (↑Num.zero : ℕ) (↑n : ℕ)
pos : ∀ (m : PosNum), (↑(f (Num.pos m) n) : ℕ) = Nat.bitwise g (↑(Num.pos m) : ℕ) (↑n : ℕ)
⊢ (↑(f m n) : ℕ) = Nat.bitwise g (↑m : ℕ) (↑n : ℕ)

Tactic:
obtain - | m := m
-- Module: Mathlib.Data.Num.Lemmas
Goal:
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 : Num
zero : (↑(f Num.zero Num.zero) : ℕ) = Nat.bitwise g (↑Num.zero : ℕ) (↑Num.zero : ℕ)
zero₁ : ∀ (n : PosNum), (↑(f Num.zero (pos n)) : ℕ) = Nat.bitwise g (↑Num.zero : ℕ) (↑(pos n) : ℕ)
⊢ (↑(f Num.zero n) : ℕ) = Nat.bitwise g (↑Num.zero : ℕ) (↑n : ℕ)

Tactic:
obtain - | n := n
-- Module: Mathlib.Data.Num.Lemmas
Goal:
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 (Num.pos n) = bif g false true then Num.pos n else 0
fn0 : ∀ (n : PosNum), f (Num.pos n) 0 = bif g true false then Num.pos n else 0
fnn : ∀ (m n : PosNum), f (Num.pos m) (Num.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 Num.pos n else 0)
pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = bit (g a true) (bif g true false then Num.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 : Num
m : PosNum
pos : (↑(f (Num.pos m) zero) : ℕ) = Nat.bitwise g (↑(Num.pos m) : ℕ) (↑zero : ℕ)
pos₁ : ∀ (n : PosNum), (↑(f (Num.pos m) (Num.pos n)) : ℕ) = Nat.bitwise g (↑(Num.pos m) : ℕ) (↑(Num.pos n) : ℕ)
⊢ (↑(f (Num.pos m) n) : ℕ) = Nat.bitwise g (↑(Num.pos m) : ℕ) (↑n : ℕ)

Tactic:
obtain - | n := n
-- Module: Mathlib.Data.Num.Lemmas
Goal:
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)
zero : (↑(f 0 0) : ℕ) = Nat.bitwise g 0 0
⊢ (↑(f Num.zero Num.zero) : ℕ) = Nat.bitwise g (↑Num.zero : ℕ) (↑Num.zero : ℕ)

Tactic:
simp only [show zero = 0 from rfl, show ((0 : Num) : ℕ) = 0 from rfl]

Premises used: rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
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)
zero : (↑(f 0 0) : ℕ) = Nat.bitwise g 0 0
⊢ (↑(f Num.zero Num.zero) : ℕ) = Nat.bitwise g (↑Num.zero : ℕ) (↑Num.zero : ℕ)

Tactic:
try simp only [show zero = 0 from rfl, show ((0 : Num) : ℕ) = 0 from rfl]

Premises used: rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
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
zero : (↑(f 0 (pos n)) : ℕ) = Nat.bitwise g 0 (↑(pos n) : ℕ)
⊢ (↑(f Num.zero (pos n)) : ℕ) = Nat.bitwise g (↑Num.zero : ℕ) (↑(pos n) : ℕ)

Tactic:
simp only [show zero = 0 from rfl, show ((0 : Num) : ℕ) = 0 from rfl]

Premises used: rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
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
zero : (↑(f 0 (pos n)) : ℕ) = Nat.bitwise g 0 (↑(pos n) : ℕ)
⊢ (↑(f Num.zero (pos n)) : ℕ) = Nat.bitwise g (↑Num.zero : ℕ) (↑(pos n) : ℕ)

Tactic:
try simp only [show zero = 0 from rfl, show ((0 : Num) : ℕ) = 0 from rfl]

Premises used: rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
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 (Num.pos n) = bif g false true then Num.pos n else 0
fn0 : ∀ (n : PosNum), f (Num.pos n) 0 = bif g true false then Num.pos n else 0
fnn : ∀ (m n : PosNum), f (Num.pos m) (Num.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 Num.pos n else 0)
pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = bit (g a true) (bif g true false then Num.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
pos : (↑(f (Num.pos m) 0) : ℕ) = Nat.bitwise g (↑(Num.pos m) : ℕ) 0
⊢ (↑(f (Num.pos m) zero) : ℕ) = Nat.bitwise g (↑(Num.pos m) : ℕ) (↑zero : ℕ)

Tactic:
simp only [show zero = 0 from rfl, show ((0 : Num) : ℕ) = 0 from rfl]

Premises used: rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
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 (Num.pos n) = bif g false true then Num.pos n else 0
fn0 : ∀ (n : PosNum), f (Num.pos n) 0 = bif g true false then Num.pos n else 0
fnn : ∀ (m n : PosNum), f (Num.pos m) (Num.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 Num.pos n else 0)
pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = bit (g a true) (bif g true false then Num.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
pos : (↑(f (Num.pos m) 0) : ℕ) = Nat.bitwise g (↑(Num.pos m) : ℕ) 0
⊢ (↑(f (Num.pos m) zero) : ℕ) = Nat.bitwise g (↑(Num.pos m) : ℕ) (↑zero : ℕ)

Tactic:
try simp only [show zero = 0 from rfl, show ((0 : Num) : ℕ) = 0 from rfl]

Premises used: rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
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)
zero : Eq (α := ℕ) (↑0 : ℕ) 0
⊢ (↑(f 0 0) : ℕ) = Nat.bitwise g 0 0

Tactic:
rw [f00, Nat.bitwise_zero]

Premises used: Nat.bitwise_zero
-- Module: Mathlib.Data.Num.Lemmas
Goal:
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)
⊢ Eq (α := ℕ) (↑0 : ℕ) 0

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
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
zero : Eq (α := ℕ) (↑(bif g false true then pos n else 0) : ℕ) (if g false true = true then (↑(pos n) : ℕ) else 0)
⊢ (↑(f 0 (pos n)) : ℕ) = Nat.bitwise g 0 (↑(pos n) : ℕ)

Tactic:
rw [f0n, Nat.bitwise_zero_left]

Premises used: Nat.bitwise_zero_left
-- Module: Mathlib.Data.Num.Lemmas
Goal:
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
zero : Eq (α := ℕ) (↑(bif false then pos n else 0) : ℕ) (if false = true then (↑(pos n) : ℕ) else 0)
zero₁ : Eq (α := ℕ) (↑(bif true then pos n else 0) : ℕ) (if true = true then (↑(pos n) : ℕ) else 0)
⊢ Eq (α := ℕ) (↑(bif g false true then pos n else 0) : ℕ) (if g false true = true then (↑(pos n) : ℕ) else 0)

Tactic:
cases g false true

Premises used: Bool.true, Bool.false
-- Module: Mathlib.Data.Num.Lemmas
Goal:
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
⊢ Eq (α := ℕ) (↑(bif false then pos n else 0) : ℕ) (if false = true then (↑(pos n) : ℕ) else 0)

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
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
⊢ Eq (α := ℕ) (↑(bif true then pos n else 0) : ℕ) (if true = true then (↑(pos n) : ℕ) else 0)

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
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 (Num.pos n) = bif g false true then Num.pos n else 0
fn0 : ∀ (n : PosNum), f (Num.pos n) 0 = bif g true false then Num.pos n else 0
fnn : ∀ (m n : PosNum), f (Num.pos m) (Num.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 Num.pos n else 0)
pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = bit (g a true) (bif g true false then Num.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
pos :
  Eq (α := ℕ) (↑(bif g true false then Num.pos m else 0) : ℕ) (if g true false = true then (↑(Num.pos m) : ℕ) else 0)
⊢ (↑(f (Num.pos m) 0) : ℕ) = Nat.bitwise g (↑(Num.pos m) : ℕ) 0

Tactic:
rw [fn0, Nat.bitwise_zero_right]

Premises used: Nat.bitwise_zero_right
-- Module: Mathlib.Data.Num.Lemmas
Goal:
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 (Num.pos n) = bif g false true then Num.pos n else 0
fn0 : ∀ (n : PosNum), f (Num.pos n) 0 = bif g true false then Num.pos n else 0
fnn : ∀ (m n : PosNum), f (Num.pos m) (Num.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 Num.pos n else 0)
pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = bit (g a true) (bif g true false then Num.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
pos : Eq (α := ℕ) (↑(bif false then Num.pos m else 0) : ℕ) (if false = true then (↑(Num.pos m) : ℕ) else 0)
pos₁ : Eq (α := ℕ) (↑(bif true then Num.pos m else 0) : ℕ) (if true = true then (↑(Num.pos m) : ℕ) else 0)
⊢ Eq (α := ℕ) (↑(bif g true false then Num.pos m else 0) : ℕ) (if g true false = true then (↑(Num.pos m) : ℕ) else 0)

Tactic:
cases g true false

Premises used: Bool.true, Bool.false
-- Module: Mathlib.Data.Num.Lemmas
Goal:
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
⊢ Eq (α := ℕ) (↑(bif false then pos m else 0) : ℕ) (if false = true then (↑(pos m) : ℕ) else 0)

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
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
⊢ Eq (α := ℕ) (↑(bif true then pos m else 0) : ℕ) (if true = true then (↑(pos m) : ℕ) else 0)

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
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 (Num.pos n) = bif g false true then Num.pos n else 0
fn0 : ∀ (n : PosNum), f (Num.pos n) 0 = bif g true false then Num.pos n else 0
fnn : ∀ (m n : PosNum), f (Num.pos m) (Num.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 Num.pos n else 0)
pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = bit (g a true) (bif g true false then Num.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 : PosNum
pos : (↑(p m n) : ℕ) = Nat.bitwise g (↑(Num.pos m) : ℕ) (↑(Num.pos n) : ℕ)
⊢ (↑(f (Num.pos m) (Num.pos n)) : ℕ) = Nat.bitwise g (↑(Num.pos m) : ℕ) (↑(Num.pos n) : ℕ)

Tactic:
rw [fnn]
-- Module: Mathlib.Data.Num.Lemmas
Goal:
f : Num → Num → Num
g : Bool → Bool → Bool
p : PosNum → PosNum → Num
gff : g Bool.false Bool.false = Bool.false
f00 : f 0 0 = 0
f0n : ∀ (n : PosNum), f 0 (pos n) = bif g Bool.false Bool.true then pos n else 0
fn0 : ∀ (n : PosNum), f (pos n) 0 = bif g Bool.true Bool.false then pos n else 0
fnn : ∀ (m n : PosNum), f (pos m) (pos n) = p m n
p11 : p 1 1 = bif g Bool.true Bool.true then 1 else 0
p1b :
  ∀ (b : Bool) (n : PosNum), p 1 (PosNum.bit b n) = bit (g Bool.true b) (bif g Bool.false Bool.true then pos n else 0)
pb1 :
  ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = bit (g a Bool.true) (bif g Bool.true Bool.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_1 : PosNum
b : Bool
n : PosNum
false : Eq (α := ℕ) (bif Bool.false then (↑n : ℕ) else 0) (↑(bif Bool.false then pos n else 0) : ℕ)
true : Eq (α := ℕ) (bif Bool.true then (↑n : ℕ) else 0) (↑(bif Bool.true then pos n else 0) : ℕ)
⊢ Eq (α := ℕ) (bif b then (↑n : ℕ) else 0) (↑(bif b then pos n else 0) : ℕ)

Tactic:
cases b