awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m : PosNum
pos : (↑(HShiftRight.hShiftRight (β := ℕ) one 0) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (β := ℕ) (↑(Num.pos one) : ℕ) 0
pos₁ :
  ∀ (a : PosNum),
    (↑(HShiftRight.hShiftRight (β := ℕ) a.bit1 0) : ℕ) =
      HShiftRight.hShiftRight (α := ℕ) (β := ℕ) (↑(Num.pos a.bit1) : ℕ) 0
pos₂ :
  ∀ (a : PosNum),
    (↑(HShiftRight.hShiftRight (β := ℕ) a.bit0 0) : ℕ) =
      HShiftRight.hShiftRight (α := ℕ) (β := ℕ) (↑(Num.pos a.bit0) : ℕ) 0
⊢ (↑(HShiftRight.hShiftRight (β := ℕ) m 0) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (β := ℕ) (↑(Num.pos m) : ℕ) 0

Tactic:
cases m
-- Module: Mathlib.Data.Num.Lemmas
Goal:
⊢ (↑(HShiftRight.hShiftRight (β := ℕ) one 0) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (β := ℕ) (↑(pos one) : ℕ) 0

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a : PosNum
⊢ (↑(HShiftRight.hShiftRight (β := ℕ) a.bit1 0) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (β := ℕ) (↑(pos a.bit1) : ℕ) 0

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a : PosNum
⊢ (↑(HShiftRight.hShiftRight (β := ℕ) a.bit0 0) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (β := ℕ) (↑(pos a.bit0) : ℕ) 0

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : ℕ
IH : ∀ (m : PosNum), (↑(m >>> n) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑(pos m) : ℕ) n
m : PosNum
⊢ (↑(m >>> (n + 1)) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑(pos m) : ℕ) (n + 1)

Tactic:
?_
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : ℕ
m : PosNum
pos :
  ∀ (n : ℕ) (IH : ∀ (m : PosNum), (↑(m >>> n) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑(Num.pos m) : ℕ) n)
    (m : PosNum), (↑(m >>> (n + 1)) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑(Num.pos m) : ℕ) (n + 1)
⊢ (↑(m >>> n) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑(Num.pos m) : ℕ) n

Tactic:
induction n generalizing m with
  | zero => cases m <;> rfl
  | succ n IH => ?_

Premises used: Num.succ, Num.zero
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : ℕ
IH : ∀ (m : PosNum), (↑(m >>> n) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑(pos m) : ℕ) n
m : PosNum
m_1 : ℕ
⊢ (m_1 + m_1) / 2 = m_1

Tactic:
lia
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : ℕ
IH : ∀ (m : PosNum), (↑(m >>> n) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑(pos m) : ℕ) n
m : PosNum
⊢ ∀ (m : ℕ), (m + m).div2 = m

Tactic:
have hdiv2 : ∀ m, Nat.div2 (m + m) = m := by intro; rw [Nat.div2_val]; lia
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : ℕ
IH : ∀ (m : PosNum), (↑(m >>> n) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑(Num.pos m) : ℕ) n
m : PosNum
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
pos : (↑(one >>> (n + 1)) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑(Num.pos one) : ℕ) (n + 1)
pos₁ : ∀ (m : PosNum), (↑(m.bit1 >>> (n + 1)) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑(Num.pos m.bit1) : ℕ) (n + 1)
pos₂ : ∀ (m : PosNum), (↑(m.bit0 >>> (n + 1)) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑(Num.pos m.bit0) : ℕ) (n + 1)
⊢ (↑(m >>> (n + 1)) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑(Num.pos m) : ℕ) (n + 1)

Tactic:
obtain - | m | m := m
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : ℕ
IH : ∀ (m : PosNum), (↑(m >>> n) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑(Num.pos m) : ℕ) n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
m : PosNum
pos : (↑(m.shiftr n) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑(Num.pos m.bit1) : ℕ) (n + 1)
⊢ (↑(m.bit1 >>> (n + 1)) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑(Num.pos m.bit1) : ℕ) (n + 1)

Tactic:
dsimp only [PosNum.shiftr, ← PosNum.shiftr_eq_shiftRight]

Premises used: PosNum.shiftr_eq_shiftRight, PosNum.shiftr
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : ℕ
IH : ∀ (m : PosNum), (↑(m >>> n) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑(Num.pos m) : ℕ) n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
m : PosNum
pos : (↑(m.shiftr n) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑(Num.pos m.bit0) : ℕ) (n + 1)
⊢ (↑(m.bit0 >>> (n + 1)) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑(Num.pos m.bit0) : ℕ) (n + 1)

Tactic:
dsimp only [PosNum.shiftr, ← PosNum.shiftr_eq_shiftRight]

Premises used: PosNum.shiftr_eq_shiftRight, PosNum.shiftr
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : ℕ
IH : ∀ (m : PosNum), (↑(m >>> n) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑(Num.pos m) : ℕ) n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
pos : (↑0 : ℕ) = (↑(Num.pos one) : ℕ) / HPow.hPow (α := ℕ) 2 (n + 1)
⊢ (↑0 : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑(Num.pos one) : ℕ) (n + 1)

Tactic:
rw [Nat.shiftRight_eq_div_pow]

Premises used: Nat.shiftRight_eq_div_pow
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : ℕ
IH : ∀ (m : PosNum), (↑(m >>> n) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑(Num.pos m) : ℕ) n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
pos : (↑(Num.pos one) : ℕ) / HPow.hPow (α := ℕ) 2 (n + 1) = (↑0 : ℕ)
⊢ (↑0 : ℕ) = (↑(Num.pos one) : ℕ) / HPow.hPow (α := ℕ) 2 (n + 1)

Tactic:
symm
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : ℕ
IH : ∀ (m : PosNum), (↑(m >>> n) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑(Num.pos m) : ℕ) n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
pos : (↑(Num.pos one) : ℕ) < HPow.hPow (α := ℕ) 2 (n + 1)
⊢ (↑(Num.pos one) : ℕ) / HPow.hPow (α := ℕ) 2 (n + 1) = (↑0 : ℕ)

Tactic:
apply Nat.div_eq_of_lt

Premises used: Nat.div_eq_of_lt
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : ℕ
IH : ∀ (m : PosNum), (↑(m >>> n) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑(pos m) : ℕ) n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
⊢ (↑(pos one) : ℕ) < HPow.hPow (α := ℕ) 2 (n + 1)

Tactic:
simp
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : ℕ
IH : ∀ (m : PosNum), (↑(m >>> n) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑(pos m) : ℕ) n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
m : PosNum
trans : (↑(m.shiftr n) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑(pos m) : ℕ) n
trans₁ :
  HShiftRight.hShiftRight (α := ℕ) (↑(pos m) : ℕ) n = HShiftRight.hShiftRight (α := ℕ) (↑(pos m.bit1) : ℕ) (n + 1)
trans₂ : ℕ
⊢ (↑(m.shiftr n) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑(pos m.bit1) : ℕ) (n + 1)

Tactic:
trans
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : ℕ
IH : ∀ (m : PosNum), (↑(m >>> n) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑(pos m) : ℕ) n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
m : PosNum
⊢ (↑(m.shiftr n) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑(pos m) : ℕ) n

Tactic:
apply IH
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : ℕ
IH : ∀ (m : PosNum), (↑(m >>> n) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑(pos m) : ℕ) n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
m : PosNum
rw : Nat.shiftRight (↑m : ℕ) n = HShiftRight.hShiftRight (β := ℕ) (HAdd.hAdd (α := ℕ) (↑m : ℕ) (↑m : ℕ) + 1) 1 >>> n
⊢ Nat.shiftRight (↑m : ℕ) n = (HAdd.hAdd (α := ℕ) (↑m : ℕ) (↑m : ℕ) + 1).shiftRight (n + 1)

Tactic:
rw [add_comm n 1, @Nat.shiftRight_eq _ (1 + n), Nat.shiftRight_add]

Premises used: Nat.shiftRight_add, Nat.shiftRight_eq, add_comm, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : ℕ
IH : ∀ (m : PosNum), (↑(m >>> n) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑(pos m) : ℕ) n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
m : PosNum
apply : (↑m : ℕ) = HShiftRight.hShiftRight (β := ℕ) (HAdd.hAdd (α := ℕ) (↑m : ℕ) (↑m : ℕ) + 1) 1
⊢ Nat.shiftRight (↑m : ℕ) n = HShiftRight.hShiftRight (β := ℕ) (HAdd.hAdd (α := ℕ) (↑m : ℕ) (↑m : ℕ) + 1) 1 >>> n

Tactic:
apply congr_arg fun x => Nat.shiftRight x n

Premises used: Nat.shiftRight, congr_arg
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : ℕ
IH : ∀ (m : PosNum), (↑(m >>> n) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑(pos m) : ℕ) n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
m : PosNum
⊢ (↑m : ℕ) = HShiftRight.hShiftRight (β := ℕ) (HAdd.hAdd (α := ℕ) (↑m : ℕ) (↑m : ℕ) + 1) 1

Tactic:
simp [-add_assoc, Nat.shiftRight_succ, Nat.shiftRight_zero, ← Nat.div2_val, hdiv2]

Premises used: add_assoc, Nat.shiftRight_succ, Nat.shiftRight_zero, Nat.div2_val
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : ℕ
IH : ∀ (m : PosNum), (↑(m >>> n) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑(pos m) : ℕ) n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
m : PosNum
trans : (↑(m.shiftr n) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑(pos m) : ℕ) n
trans₁ :
  HShiftRight.hShiftRight (α := ℕ) (↑(pos m) : ℕ) n = HShiftRight.hShiftRight (α := ℕ) (↑(pos m.bit0) : ℕ) (n + 1)
trans₂ : ℕ
⊢ (↑(m.shiftr n) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑(pos m.bit0) : ℕ) (n + 1)

Tactic:
trans
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : ℕ
IH : ∀ (m : PosNum), (↑(m >>> n) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑(pos m) : ℕ) n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
m : PosNum
rw : Nat.shiftRight (↑m : ℕ) n = HShiftRight.hShiftRight (β := ℕ) (HAdd.hAdd (α := ℕ) (↑m : ℕ) (↑m : ℕ)) 1 >>> n
⊢ Nat.shiftRight (↑m : ℕ) n = (HAdd.hAdd (α := ℕ) (↑m : ℕ) (↑m : ℕ)).shiftRight (n + 1)

Tactic:
rw [add_comm n 1, @Nat.shiftRight_eq _ (1 + n), Nat.shiftRight_add]

Premises used: Nat.shiftRight_add, Nat.shiftRight_eq, add_comm, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : ℕ
IH : ∀ (m : PosNum), (↑(m >>> n) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑(pos m) : ℕ) n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
m : PosNum
apply : (↑m : ℕ) = HShiftRight.hShiftRight (β := ℕ) (HAdd.hAdd (α := ℕ) (↑m : ℕ) (↑m : ℕ)) 1
⊢ Nat.shiftRight (↑m : ℕ) n = HShiftRight.hShiftRight (β := ℕ) (HAdd.hAdd (α := ℕ) (↑m : ℕ) (↑m : ℕ)) 1 >>> n

Tactic:
apply congr_arg fun x => Nat.shiftRight x n

Premises used: Nat.shiftRight, congr_arg
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : ℕ
IH : ∀ (m : PosNum), (↑(m >>> n) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑(pos m) : ℕ) n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
m : PosNum
⊢ (↑m : ℕ) = HShiftRight.hShiftRight (β := ℕ) (HAdd.hAdd (α := ℕ) (↑m : ℕ) (↑m : ℕ)) 1

Tactic:
simp [-add_assoc, Nat.shiftRight_succ, Nat.shiftRight_zero, ← Nat.div2_val, hdiv2]

Premises used: add_assoc, Nat.shiftRight_succ, Nat.shiftRight_zero, Nat.div2_val
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : ℕ
zero : false = Nat.testBit 0 n
zero₁ zero₂ : false = false
⊢ false = Nat.testBit (↑Num.zero : ℕ) n

Tactic:
rw [show (Num.zero : Nat) = 0 from rfl, Nat.zero_testBit]

Premises used: Nat.zero_testBit, rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : ℕ
m : PosNum
pos : ∀ (m : PosNum), m.testBit 0 = Nat.testBit (↑m : ℕ) 0
pos₁ :
  ∀ (n : ℕ),
    (∀ (m : PosNum), m.testBit n = Nat.testBit (↑m : ℕ) n) →
      ∀ (m : PosNum), m.testBit (n + 1) = Nat.testBit (↑m : ℕ) (n + 1)
⊢ m.testBit n = Nat.testBit (↑m : ℕ) n

Tactic:
induction n generalizing m
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m : PosNum
pos : one.testBit 0 = Nat.testBit (↑one : ℕ) 0
pos₁ : ∀ (m : PosNum), m.bit1.testBit 0 = Nat.testBit (↑m.bit1 : ℕ) 0
pos₂ : ∀ (m : PosNum), m.bit0.testBit 0 = Nat.testBit (↑m.bit0 : ℕ) 0
⊢ m.testBit 0 = Nat.testBit (↑m : ℕ) 0

Tactic:
obtain - | m | m := m
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : ℕ
h : ∀ (m : PosNum), m.testBit n = Nat.testBit (↑m : ℕ) n
m : PosNum
pos : one.testBit (n + 1) = Nat.testBit (↑one : ℕ) (n + 1)
pos₁ : ∀ (m : PosNum), m.bit1.testBit (n + 1) = Nat.testBit (↑m.bit1 : ℕ) (n + 1)
pos₂ : ∀ (m : PosNum), m.bit0.testBit (n + 1) = Nat.testBit (↑m.bit0 : ℕ) (n + 1)
⊢ m.testBit (n + 1) = Nat.testBit (↑m : ℕ) (n + 1)

Tactic:
obtain - | m | m := m
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : ℕ
h : ∀ (m : PosNum), m.testBit n = Nat.testBit (↑m : ℕ) n
m : PosNum
pos : m.testBit n = Nat.testBit (↑m.bit1 : ℕ) (n + 1)
⊢ m.bit1.testBit (n + 1) = Nat.testBit (↑m.bit1 : ℕ) (n + 1)

Tactic:
simp only [PosNum.testBit]

Premises used: PosNum.testBit
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : ℕ
h : ∀ (m : PosNum), m.testBit n = Nat.testBit (↑m : ℕ) n
m : PosNum
pos : m.testBit n = Nat.testBit (↑m.bit0 : ℕ) (n + 1)
⊢ m.bit0.testBit (n + 1) = Nat.testBit (↑m.bit0 : ℕ) (n + 1)

Tactic:
simp only [PosNum.testBit]

Premises used: PosNum.testBit
-- Module: Mathlib.Data.Num.Lemmas
Goal:
⊢ true = Nat.testBit (↑one : ℕ) 0

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m : PosNum
pos : true = (HAdd.hAdd (α := ℕ) (↑m : ℕ) (↑m : ℕ) + 1).testBit 0
pos₁ : true = (HMul.hMul (α := ℕ) 2 (↑m : ℕ) + 1).testBit 0
pos₂ : true = (Nat.bit true (↑m : ℕ)).testBit 0
pos₃ pos₄ : true = true
⊢ true = Nat.testBit (↑m.bit1 : ℕ) 0

Tactic:
rw [PosNum.cast_bit1, ← two_mul, ← congr_fun Nat.bit_true, Nat.testBit_bit_zero]

Premises used: PosNum.cast_bit1, Nat.bit_true, two_mul, Nat.testBit_bit_zero, congr_fun
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m : PosNum
pos : false = (HAdd.hAdd (α := ℕ) (↑m : ℕ) (↑m : ℕ)).testBit 0
pos₁ : false = (HMul.hMul (α := ℕ) 2 (↑m : ℕ)).testBit 0
pos₂ : false = (Nat.bit false (↑m : ℕ)).testBit 0
pos₃ pos₄ : false = false
⊢ false = Nat.testBit (↑m.bit0 : ℕ) 0

Tactic:
rw [PosNum.cast_bit0, ← two_mul, ← congr_fun Nat.bit_false, Nat.testBit_bit_zero]

Premises used: two_mul, Nat.bit_false, Nat.testBit_bit_zero, PosNum.cast_bit0, congr_fun
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : ℕ
h : ∀ (m : PosNum), m.testBit n = Nat.testBit (↑m : ℕ) n
⊢ false = Nat.testBit (↑one : ℕ) (n + 1)

Tactic:
simp [Nat.testBit_add_one]

Premises used: Nat.testBit_add_one
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : ℕ
IH : ∀ (m : PosNum), m.testBit n = Nat.testBit (↑m : ℕ) n
m : PosNum
rw : m.testBit n = (HAdd.hAdd (α := ℕ) (↑m : ℕ) (↑m : ℕ) + 1).testBit (n + 1)
rw₁ : m.testBit n = (HMul.hMul (α := ℕ) 2 (↑m : ℕ) + 1).testBit (n + 1)
rw₂ : m.testBit n = (Nat.bit true (↑m : ℕ)).testBit (n + 1)
rw₃ : m.testBit n = Nat.testBit (↑m : ℕ) n
rw₄ rw₅ : Nat.testBit (↑m : ℕ) n = Nat.testBit (↑m : ℕ) n
⊢ m.testBit n = Nat.testBit (↑m.bit1 : ℕ) (n + 1)

Tactic:
rw [PosNum.cast_bit1, ← two_mul, ← congr_fun Nat.bit_true, Nat.testBit_bit_succ, IH]

Premises used: PosNum.cast_bit1, Nat.bit_true, two_mul, Nat.testBit_bit_succ, congr_fun
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : ℕ
h : ∀ (m : PosNum), m.testBit n = Nat.testBit (↑m : ℕ) n
m : PosNum
⊢ m.testBit n = Nat.testBit (↑m.bit1 : ℕ) (n + 1)

Tactic:
case succ.bit1 n IH =>
      rw [PosNum.cast_bit1, ← two_mul, ← congr_fun Nat.bit_true, Nat.testBit_bit_succ, IH]

Premises used: PosNum.cast_bit1, Nat.bit_true, two_mul, Nat.testBit_bit_succ, congr_fun
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : ℕ
IH : ∀ (m : PosNum), m.testBit n = Nat.testBit (↑m : ℕ) n
m : PosNum
rw : m.testBit n = (HAdd.hAdd (α := ℕ) (↑m : ℕ) (↑m : ℕ)).testBit (n + 1)
rw₁ : m.testBit n = (HMul.hMul (α := ℕ) 2 (↑m : ℕ)).testBit (n + 1)
rw₂ : m.testBit n = (Nat.bit false (↑m : ℕ)).testBit (n + 1)
rw₃ : m.testBit n = Nat.testBit (↑m : ℕ) n
rw₄ rw₅ : Nat.testBit (↑m : ℕ) n = Nat.testBit (↑m : ℕ) n
⊢ m.testBit n = Nat.testBit (↑m.bit0 : ℕ) (n + 1)

Tactic:
rw [PosNum.cast_bit0, ← two_mul, ← congr_fun Nat.bit_false, Nat.testBit_bit_succ, IH]

Premises used: two_mul, Nat.bit_false, Nat.testBit_bit_succ, PosNum.cast_bit0, congr_fun
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m : Num
n : ℕ
zero : Num.zero.testBit n = Nat.testBit (↑Num.zero : ℕ) n
zero₁ : false = Nat.testBit (↑Num.zero : ℕ) n
pos : ∀ (m : PosNum), (Num.pos m).testBit n = Nat.testBit (↑(Num.pos m) : ℕ) n
pos₁ : ∀ (m : PosNum), m.testBit n = Nat.testBit (↑(Num.pos m) : ℕ) n
⊢ m.testBit n = Nat.testBit (↑m : ℕ) n

Tactic:
cases m with dsimp only [testBit]
  | zero =>
    rw [show (Num.zero : Nat) = 0 from rfl, Nat.zero_testBit]
  | pos m =>
    rw [cast_pos]
    induction n generalizing m <;> obtain - | m | m := m
        <;> simp only [PosNum.testBit]
    · rfl
    · rw [PosNum.cast_bit1, ← two_mul, ← congr_fun Nat.bit_true, Nat.testBit_bit_zero]
    · rw [PosNum.cast_bit0, ← two_mul, ← congr_fun Nat.bit_false, Nat.testBit_bit_zero]
    · simp [Nat.testBit_add_one]
    case succ.bit1 n IH =>
      rw [PosNum.cast_bit1, ← two_mul, ← congr_fun Nat.bit_true, Nat.testBit_bit_succ, IH]
    case succ.bit0 n IH =>
      rw [PosNum.cast_bit0, ← two_mul, ← congr_fun Nat.bit_false, Nat.testBit_bit_succ, IH]

Premises used: PosNum.cast_bit1, Nat.bit_true, Num.testBit, two_mul, Nat.bit_false, Nat.zero_testBit, Nat.testBit_bit_zero, Nat.testBit_bit_succ, Num.pos, PosNum.testBit, PosNum.cast_bit0, Nat.testBit_add_one, congr_fun, rfl, Num.zero, Num.cast_pos
-- Module: Mathlib.Data.Num.Prime
Goal:
fuel : ℕ
n k : PosNum
h : Nat.sqrt (↑n : ℕ) < fuel + (↑k.bit1 : ℕ)
zero :
  ∀ {k : PosNum} (h : Nat.sqrt (↑n : ℕ) < HAdd.hAdd (α := ℕ) 0 (↑k.bit1 : ℕ)),
    (↑(n.minFacAux 0 k) : ℕ) = Nat.minFacAux (↑n : ℕ) (↑k.bit1 : ℕ)
succ :
  ∀ (n_1 : ℕ),
    (∀ {k : PosNum} (h : Nat.sqrt (↑n : ℕ) < n_1 + (↑k.bit1 : ℕ)),
        (↑(n.minFacAux n_1 k) : ℕ) = Nat.minFacAux (↑n : ℕ) (↑k.bit1 : ℕ)) →
      ∀ {k : PosNum} (h : Nat.sqrt (↑n : ℕ) < n_1 + 1 + (↑k.bit1 : ℕ)),
        (↑(n.minFacAux (n_1 + 1) k) : ℕ) = Nat.minFacAux (↑n : ℕ) (↑k.bit1 : ℕ)
⊢ (↑(n.minFacAux fuel k) : ℕ) = Nat.minFacAux (↑n : ℕ) (↑k.bit1 : ℕ)

Tactic:
induction fuel generalizing k
-- Module: Mathlib.Data.Num.Prime
Goal:
n k : PosNum
h : Nat.sqrt (↑n : ℕ) < HAdd.hAdd (α := ℕ) 0 (↑k.bit1 : ℕ)
rw :
  (↑n : ℕ) =
    if (↑n : ℕ) < HMul.hMul (α := ℕ) (↑k.bit1 : ℕ) (↑k.bit1 : ℕ) then (↑n : ℕ)
    else
      if Dvd.dvd (α := ℕ) (↑k.bit1 : ℕ) (↑n : ℕ) then (↑k.bit1 : ℕ)
      else Nat.minFacAux (↑n : ℕ) (HAdd.hAdd (α := ℕ) (↑k.bit1 : ℕ) 2)
⊢ (↑(n.minFacAux 0 k) : ℕ) = Nat.minFacAux (↑n : ℕ) (↑k.bit1 : ℕ)

Tactic:
rw [minFacAux, Nat.minFacAux]

Premises used: PosNum.minFacAux, Nat.minFacAux
-- Module: Mathlib.Data.Num.Prime
Goal:
n : PosNum
n_1 : ℕ
h_1 :
  ∀ {k : PosNum} (h : Nat.sqrt (↑n : ℕ) < n_1 + (↑k.bit1 : ℕ)),
    (↑(n.minFacAux n_1 k) : ℕ) = Nat.minFacAux (↑n : ℕ) (↑k.bit1 : ℕ)
k : PosNum
h : Nat.sqrt (↑n : ℕ) < n_1 + 1 + (↑k.bit1 : ℕ)
succ :
  (↑(if n < k.bit1 * k.bit1 then n else if k.bit1 ∣ n then k.bit1 else n.minFacAux n_1 k.succ) : ℕ) =
    if (↑n : ℕ) < HMul.hMul (α := ℕ) (↑k.bit1 : ℕ) (↑k.bit1 : ℕ) then (↑n : ℕ)
    else
      if Dvd.dvd (α := ℕ) (↑k.bit1 : ℕ) (↑n : ℕ) then (↑k.bit1 : ℕ)
      else Nat.minFacAux (↑n : ℕ) (HAdd.hAdd (α := ℕ) (↑k.bit1 : ℕ) 2)
⊢ (↑(n.minFacAux (n_1 + 1) k) : ℕ) = Nat.minFacAux (↑n : ℕ) (↑k.bit1 : ℕ)

Tactic:
rw [minFacAux, Nat.minFacAux]

Premises used: PosNum.minFacAux, Nat.minFacAux
-- Module: Mathlib.Data.Num.Prime
Goal:
n k : PosNum
h : Nat.sqrt (↑n : ℕ) < HAdd.hAdd (α := ℕ) 0 (↑k.bit1 : ℕ)
⊢ (↑n : ℕ) < HMul.hMul (α := ℕ) (↑k.bit1 : ℕ) (↑k.bit1 : ℕ)

Tactic:
rw [Nat.zero_add, Nat.sqrt_lt] at h

Premises used: Nat.sqrt_lt, Nat.zero_add
-- Module: Mathlib.Data.Num.Prime
Goal:
n k : PosNum
h : (↑n : ℕ) < HMul.hMul (α := ℕ) (↑k.bit1 : ℕ) (↑k.bit1 : ℕ)
⊢ (↑n : ℕ) =
    if (↑n : ℕ) < HMul.hMul (α := ℕ) (↑k.bit1 : ℕ) (↑k.bit1 : ℕ) then (↑n : ℕ)
    else
      if Dvd.dvd (α := ℕ) (↑k.bit1 : ℕ) (↑n : ℕ) then (↑k.bit1 : ℕ)
      else Nat.minFacAux (↑n : ℕ) (HAdd.hAdd (α := ℕ) (↑k.bit1 : ℕ) 2)

Tactic:
simp only [h, ite_true]

Premises used: ite_true
-- Module: Mathlib.Data.Num.Prime
Goal:
n k : PosNum
h : Nat.sqrt (↑n : ℕ) < HAdd.hAdd (α := ℕ) 0 (↑k.bit1 : ℕ)
⊢ (↑n : ℕ) =
    if (↑n : ℕ) < HMul.hMul (α := ℕ) (↑k.bit1 : ℕ) (↑k.bit1 : ℕ) then (↑n : ℕ)
    else
      if Dvd.dvd (α := ℕ) (↑k.bit1 : ℕ) (↑n : ℕ) then (↑k.bit1 : ℕ)
      else Nat.minFacAux (↑n : ℕ) (HAdd.hAdd (α := ℕ) (↑k.bit1 : ℕ) 2)

Tactic:
case zero =>
    rw [Nat.zero_add, Nat.sqrt_lt] at h
    simp only [h, ite_true]

Premises used: Nat.sqrt_lt, ite_true, Nat.zero_add
-- Module: Mathlib.Data.Num.Prime
Goal:
n : PosNum
fuel : ℕ
ih :
  ∀ {k : PosNum} (h : Nat.sqrt (↑n : ℕ) < fuel + (↑k.bit1 : ℕ)),
    (↑(n.minFacAux fuel k) : ℕ) = Nat.minFacAux (↑n : ℕ) (↑k.bit1 : ℕ)
k : PosNum
h : Nat.sqrt (↑n : ℕ) < fuel + 1 + (↑k.bit1 : ℕ)
simp_rw :
  (↑(if n < k.bit1 * k.bit1 then n else if k.bit1 ∣ n then k.bit1 else n.minFacAux fuel k.succ) : ℕ) =
    if LT.lt (α := ℕ) (↑n : ℕ) (↑(k.bit1 * k.bit1) : ℕ) then (↑n : ℕ)
    else
      if Dvd.dvd (α := ℕ) (↑k.bit1 : ℕ) (↑n : ℕ) then (↑k.bit1 : ℕ)
      else Nat.minFacAux (↑n : ℕ) (HAdd.hAdd (α := ℕ) (↑k.bit1 : ℕ) 2)
⊢ (↑(if n < k.bit1 * k.bit1 then n else if k.bit1 ∣ n then k.bit1 else n.minFacAux fuel k.succ) : ℕ) =
    if (↑n : ℕ) < HMul.hMul (α := ℕ) (↑k.bit1 : ℕ) (↑k.bit1 : ℕ) then (↑n : ℕ)
    else
      if Dvd.dvd (α := ℕ) (↑k.bit1 : ℕ) (↑n : ℕ) then (↑k.bit1 : ℕ)
      else Nat.minFacAux (↑n : ℕ) (HAdd.hAdd (α := ℕ) (↑k.bit1 : ℕ) 2)

Tactic:
simp_rw [← mul_to_nat]

Premises used: PosNum.mul_to_nat
-- Module: Mathlib.Data.Num.Prime
Goal:
n : PosNum
fuel : ℕ
ih :
  ∀ {k : PosNum} (h : Nat.sqrt (↑n : ℕ) < fuel + (↑k.bit1 : ℕ)),
    (↑(n.minFacAux fuel k) : ℕ) = Nat.minFacAux (↑n : ℕ) (↑k.bit1 : ℕ)
k : PosNum
h : Nat.sqrt (↑n : ℕ) < fuel + 1 + (↑k.bit1 : ℕ)
simp :
  (↑(if n < k.bit1 * k.bit1 then n else if k.bit1 ∣ n then k.bit1 else n.minFacAux fuel k.succ) : ℕ) =
    if n < k.bit1 * k.bit1 then (↑n : ℕ)
    else if k.bit1 ∣ n then (↑k.bit1 : ℕ) else Nat.minFacAux (↑n : ℕ) (HAdd.hAdd (α := ℕ) (↑k.bit1 : ℕ) 2)
⊢ (↑(if n < k.bit1 * k.bit1 then n else if k.bit1 ∣ n then k.bit1 else n.minFacAux fuel k.succ) : ℕ) =
    if LT.lt (α := ℕ) (↑n : ℕ) (↑(k.bit1 * k.bit1) : ℕ) then (↑n : ℕ)
    else
      if Dvd.dvd (α := ℕ) (↑k.bit1 : ℕ) (↑n : ℕ) then (↑k.bit1 : ℕ)
      else Nat.minFacAux (↑n : ℕ) (HAdd.hAdd (α := ℕ) (↑k.bit1 : ℕ) 2)

Tactic:
simp only [cast_lt, dvd_to_nat]

Premises used: PosNum.dvd_to_nat, PosNum.cast_lt
-- Module: Mathlib.Data.Num.Prime
Goal:
n : PosNum
fuel : ℕ
ih :
  ∀ {k : PosNum} (h : Nat.sqrt (↑n : ℕ) < fuel + (↑k.bit1 : ℕ)),
    (↑(n.minFacAux fuel k) : ℕ) = Nat.minFacAux (↑n : ℕ) (↑k.bit1 : ℕ)
k : PosNum
h : Nat.sqrt (↑n : ℕ) < fuel + 1 + (↑k.bit1 : ℕ)
pos : n < k.bit1 * k.bit1 → Eq (α := ℕ) (↑n : ℕ) (↑n : ℕ)
pos₁ : ¬n < k.bit1 * k.bit1 → k.bit1 ∣ n → Eq (α := ℕ) (↑k.bit1 : ℕ) (↑k.bit1 : ℕ)
neg :
  ¬n < k.bit1 * k.bit1 →
    ¬k.bit1 ∣ n → (↑(n.minFacAux fuel k.succ) : ℕ) = Nat.minFacAux (↑n : ℕ) (HAdd.hAdd (α := ℕ) (↑k.bit1 : ℕ) 2)
⊢ (↑(if n < k.bit1 * k.bit1 then n else if k.bit1 ∣ n then k.bit1 else n.minFacAux fuel k.succ) : ℕ) =
    if n < k.bit1 * k.bit1 then (↑n : ℕ)
    else if k.bit1 ∣ n then (↑k.bit1 : ℕ) else Nat.minFacAux (↑n : ℕ) (HAdd.hAdd (α := ℕ) (↑k.bit1 : ℕ) 2)

Tactic:
split_ifs
-- Module: Mathlib.Data.Num.Prime
Goal:
n : PosNum
fuel : ℕ
ih :
  ∀ {k : PosNum} (h : Nat.sqrt (↑n : ℕ) < fuel + (↑k.bit1 : ℕ)),
    (↑(n.minFacAux fuel k) : ℕ) = Nat.minFacAux (↑n : ℕ) (↑k.bit1 : ℕ)
k : PosNum
h : Nat.sqrt (↑n : ℕ) < fuel + 1 + (↑k.bit1 : ℕ)
h_1 : n < k.bit1 * k.bit1
⊢ Eq (α := ℕ) (↑n : ℕ) (↑n : ℕ)

Tactic:
rfl
-- Module: Mathlib.Data.Num.Prime
Goal:
n : PosNum
fuel : ℕ
ih :
  ∀ {k : PosNum} (h : Nat.sqrt (↑n : ℕ) < fuel + (↑k.bit1 : ℕ)),
    (↑(n.minFacAux fuel k) : ℕ) = Nat.minFacAux (↑n : ℕ) (↑k.bit1 : ℕ)
k : PosNum
h : Nat.sqrt (↑n : ℕ) < fuel + 1 + (↑k.bit1 : ℕ)
h_1 : n < k.bit1 * k.bit1
⊢ Eq (α := ℕ) (↑n : ℕ) (↑n : ℕ)

Tactic:
try rfl
-- Module: Mathlib.Data.Num.Prime
Goal:
n : PosNum
fuel : ℕ
ih :
  ∀ {k : PosNum} (h : Nat.sqrt (↑n : ℕ) < fuel + (↑k.bit1 : ℕ)),
    (↑(n.minFacAux fuel k) : ℕ) = Nat.minFacAux (↑n : ℕ) (↑k.bit1 : ℕ)
k : PosNum
h : Nat.sqrt (↑n : ℕ) < fuel + 1 + (↑k.bit1 : ℕ)
h_1 : ¬n < k.bit1 * k.bit1
h_2 : k.bit1 ∣ n
⊢ Eq (α := ℕ) (↑k.bit1 : ℕ) (↑k.bit1 : ℕ)

Tactic:
rfl
-- Module: Mathlib.Data.Num.Prime
Goal:
n : PosNum
fuel : ℕ
ih :
  ∀ {k : PosNum} (h : Nat.sqrt (↑n : ℕ) < fuel + (↑k.bit1 : ℕ)),
    (↑(n.minFacAux fuel k) : ℕ) = Nat.minFacAux (↑n : ℕ) (↑k.bit1 : ℕ)
k : PosNum
h : Nat.sqrt (↑n : ℕ) < fuel + 1 + (↑k.bit1 : ℕ)
h_1 : ¬n < k.bit1 * k.bit1
h_2 : k.bit1 ∣ n
⊢ Eq (α := ℕ) (↑k.bit1 : ℕ) (↑k.bit1 : ℕ)

Tactic:
try rfl
-- Module: Mathlib.Data.Num.Prime
Goal:
n : PosNum
fuel : ℕ
ih :
  ∀ {k : PosNum} (h : Nat.sqrt (↑n : ℕ) < fuel + (↑k.bit1 : ℕ)),
    (↑(n.minFacAux fuel k) : ℕ) = Nat.minFacAux (↑n : ℕ) (↑k.bit1 : ℕ)
k : PosNum
h : Nat.sqrt (↑n : ℕ) < fuel + 1 + (↑k.bit1 : ℕ)
h_1 : ¬n < k.bit1 * k.bit1
h_2 : ¬k.bit1 ∣ n
neg : Nat.minFacAux (↑n : ℕ) (↑k.succ.bit1 : ℕ) = Nat.minFacAux (↑n : ℕ) (HAdd.hAdd (α := ℕ) (↑k.bit1 : ℕ) 2)
neg₁ : Nat.sqrt (↑n : ℕ) < fuel + (↑k.succ.bit1 : ℕ)
⊢ (↑(n.minFacAux fuel k.succ) : ℕ) = Nat.minFacAux (↑n : ℕ) (HAdd.hAdd (α := ℕ) (↑k.bit1 : ℕ) 2)

Tactic:
rw [ih]
-- Module: Mathlib.Data.Num.Prime
Goal:
n : PosNum
fuel : ℕ
ih :
  ∀ {k : PosNum} (h : Nat.sqrt (↑n : ℕ) < fuel + (↑k.bit1 : ℕ)),
    (↑(n.minFacAux fuel k) : ℕ) = Nat.minFacAux (↑n : ℕ) (↑k.bit1 : ℕ)
k : PosNum
h : Nat.sqrt (↑n : ℕ) < fuel + 1 + (↑k.bit1 : ℕ)
h_1 : ¬n < k.bit1 * k.bit1
h_2 : ¬k.bit1 ∣ n
neg : (↑k.succ.bit1 : ℕ) = HAdd.hAdd (α := ℕ) (↑k.bit1 : ℕ) 2
⊢ Nat.minFacAux (↑n : ℕ) (↑k.succ.bit1 : ℕ) = Nat.minFacAux (↑n : ℕ) (HAdd.hAdd (α := ℕ) (↑k.bit1 : ℕ) 2)

Tactic:
congr
-- Module: Mathlib.Data.Num.Prime
Goal:
n : PosNum
fuel : ℕ
ih :
  ∀ {k : PosNum} (h : Nat.sqrt (↑n : ℕ) < fuel + (↑k.bit1 : ℕ)),
    (↑(n.minFacAux fuel k) : ℕ) = Nat.minFacAux (↑n : ℕ) (↑k.bit1 : ℕ)
k : PosNum
h : Nat.sqrt (↑n : ℕ) < fuel + 1 + (↑k.bit1 : ℕ)
h_1 : ¬n < k.bit1 * k.bit1
h_2 : ¬k.bit1 ∣ n
⊢ Nat.sqrt (↑n : ℕ) < (fuel + 1 + (↑k.bit1 : ℕ)).succ

Tactic:
Nat.lt_succ_of_lt h

Premises used: Nat.lt_succ_of_lt