awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : ℕ
h : ∀ (m : PosNum), m.testBit n = Nat.testBit (↑m : ℕ) n
m : PosNum
⊢ m.bit1.testBit (n + 1) = Nat.testBit (↑m.bit1 : ℕ) (n + 1)
have pos : m.testBit n = Nat.testBit (↑m.bit1 : ℕ) (n + 1)
Tactic: simp only [PosNum.testBit]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : ℕ
h : ∀ (m : PosNum), m.testBit n = Nat.testBit (↑m : ℕ) n
m : PosNum
⊢ m.bit0.testBit (n + 1) = Nat.testBit (↑m.bit0 : ℕ) (n + 1)
have pos : m.testBit n = Nat.testBit (↑m.bit0 : ℕ) (n + 1)
Tactic: simp only [PosNum.testBit]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
m : PosNum
⊢ true = Nat.testBit (↑m.bit1 : ℕ) 0
have pos : true = (HAdd.hAdd (α := ℕ) (↑m : ℕ) (↑m : ℕ) + 1).testBit 0
Tactic: rw [PosNum.cast_bit1, ← two_mul, ← congr_fun Nat.bit_true, Nat.testBit_bit_zero]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
m : PosNum
pos : true = (HAdd.hAdd (α := ℕ) (↑m : ℕ) (↑m : ℕ) + 1).testBit 0
⊢ true = Nat.testBit (↑m.bit1 : ℕ) 0
have pos₁ : true = (HMul.hMul (α := ℕ) 2 (↑m : ℕ) + 1).testBit 0
Tactic: rw [PosNum.cast_bit1, ← two_mul, ← congr_fun Nat.bit_true, Nat.testBit_bit_zero]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
m : PosNum
pos : true = (HAdd.hAdd (α := ℕ) (↑m : ℕ) (↑m : ℕ) + 1).testBit 0
pos₁ : true = (HMul.hMul (α := ℕ) 2 (↑m : ℕ) + 1).testBit 0
⊢ true = Nat.testBit (↑m.bit1 : ℕ) 0
have pos₂ : true = (Nat.bit true (↑m : ℕ)).testBit 0
Tactic: rw [PosNum.cast_bit1, ← two_mul, ← congr_fun Nat.bit_true, Nat.testBit_bit_zero]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
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
⊢ true = Nat.testBit (↑m.bit1 : ℕ) 0
have pos₃ : true = true
Tactic: rw [PosNum.cast_bit1, ← two_mul, ← congr_fun Nat.bit_true, Nat.testBit_bit_zero]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
m : PosNum
⊢ false = Nat.testBit (↑m.bit0 : ℕ) 0
have pos : false = (HAdd.hAdd (α := ℕ) (↑m : ℕ) (↑m : ℕ)).testBit 0
Tactic: rw [PosNum.cast_bit0, ← two_mul, ← congr_fun Nat.bit_false, Nat.testBit_bit_zero]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
m : PosNum
pos : false = (HAdd.hAdd (α := ℕ) (↑m : ℕ) (↑m : ℕ)).testBit 0
⊢ false = Nat.testBit (↑m.bit0 : ℕ) 0
have pos₁ : false = (HMul.hMul (α := ℕ) 2 (↑m : ℕ)).testBit 0
Tactic: rw [PosNum.cast_bit0, ← two_mul, ← congr_fun Nat.bit_false, Nat.testBit_bit_zero]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
m : PosNum
pos : false = (HAdd.hAdd (α := ℕ) (↑m : ℕ) (↑m : ℕ)).testBit 0
pos₁ : false = (HMul.hMul (α := ℕ) 2 (↑m : ℕ)).testBit 0
⊢ false = Nat.testBit (↑m.bit0 : ℕ) 0
have pos₂ : false = (Nat.bit false (↑m : ℕ)).testBit 0
Tactic: rw [PosNum.cast_bit0, ← two_mul, ← congr_fun Nat.bit_false, Nat.testBit_bit_zero]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
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
⊢ false = Nat.testBit (↑m.bit0 : ℕ) 0
have pos₃ : false = false
Tactic: rw [PosNum.cast_bit0, ← two_mul, ← congr_fun Nat.bit_false, Nat.testBit_bit_zero]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : ℕ
IH : ∀ (m : PosNum), m.testBit n = Nat.testBit (↑m : ℕ) n
m : PosNum
⊢ m.testBit n = Nat.testBit (↑m.bit1 : ℕ) (n + 1)
have rw : m.testBit n = (HAdd.hAdd (α := ℕ) (↑m : ℕ) (↑m : ℕ) + 1).testBit (n + 1)
Tactic: rw [PosNum.cast_bit1, ← two_mul, ← congr_fun Nat.bit_true, Nat.testBit_bit_succ, IH]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
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)
⊢ m.testBit n = Nat.testBit (↑m.bit1 : ℕ) (n + 1)
have rw₁ : m.testBit n = (HMul.hMul (α := ℕ) 2 (↑m : ℕ) + 1).testBit (n + 1)
Tactic: rw [PosNum.cast_bit1, ← two_mul, ← congr_fun Nat.bit_true, Nat.testBit_bit_succ, IH]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
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)
⊢ m.testBit n = Nat.testBit (↑m.bit1 : ℕ) (n + 1)
have rw₂ : m.testBit n = (Nat.bit true (↑m : ℕ)).testBit (n + 1)
Tactic: rw [PosNum.cast_bit1, ← two_mul, ← congr_fun Nat.bit_true, Nat.testBit_bit_succ, IH]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
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)
⊢ m.testBit n = Nat.testBit (↑m.bit1 : ℕ) (n + 1)
have rw₃ : m.testBit n = Nat.testBit (↑m : ℕ) n
Tactic: rw [PosNum.cast_bit1, ← two_mul, ← congr_fun Nat.bit_true, Nat.testBit_bit_succ, IH]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
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
⊢ m.testBit n = Nat.testBit (↑m.bit1 : ℕ) (n + 1)
have rw₄ : Nat.testBit (↑m : ℕ) n = Nat.testBit (↑m : ℕ) n
Tactic: rw [PosNum.cast_bit1, ← two_mul, ← congr_fun Nat.bit_true, Nat.testBit_bit_succ, IH]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : ℕ
IH : ∀ (m : PosNum), m.testBit n = Nat.testBit (↑m : ℕ) n
m : PosNum
⊢ m.testBit n = Nat.testBit (↑m.bit0 : ℕ) (n + 1)
have rw : m.testBit n = (HAdd.hAdd (α := ℕ) (↑m : ℕ) (↑m : ℕ)).testBit (n + 1)
Tactic: rw [PosNum.cast_bit0, ← two_mul, ← congr_fun Nat.bit_false, Nat.testBit_bit_succ, IH]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
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)
⊢ m.testBit n = Nat.testBit (↑m.bit0 : ℕ) (n + 1)
have rw₁ : m.testBit n = (HMul.hMul (α := ℕ) 2 (↑m : ℕ)).testBit (n + 1)
Tactic: rw [PosNum.cast_bit0, ← two_mul, ← congr_fun Nat.bit_false, Nat.testBit_bit_succ, IH]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
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)
⊢ m.testBit n = Nat.testBit (↑m.bit0 : ℕ) (n + 1)
have rw₂ : m.testBit n = (Nat.bit false (↑m : ℕ)).testBit (n + 1)
Tactic: rw [PosNum.cast_bit0, ← two_mul, ← congr_fun Nat.bit_false, Nat.testBit_bit_succ, IH]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
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)
⊢ m.testBit n = Nat.testBit (↑m.bit0 : ℕ) (n + 1)
have rw₃ : m.testBit n = Nat.testBit (↑m : ℕ) n
Tactic: rw [PosNum.cast_bit0, ← two_mul, ← congr_fun Nat.bit_false, Nat.testBit_bit_succ, IH]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
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
⊢ m.testBit n = Nat.testBit (↑m.bit0 : ℕ) (n + 1)
have rw₄ : Nat.testBit (↑m : ℕ) n = Nat.testBit (↑m : ℕ) n
Tactic: rw [PosNum.cast_bit0, ← two_mul, ← congr_fun Nat.bit_false, Nat.testBit_bit_succ, IH]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
m : Num
n : ℕ
⊢ m.testBit n = Nat.testBit (↑m : ℕ) n
have zero : zero.testBit n = Nat.testBit (↑zero : ℕ) 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]
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
m : Num
n : ℕ
zero : Num.zero.testBit n = Nat.testBit (↑Num.zero : ℕ) n
⊢ m.testBit n = Nat.testBit (↑m : ℕ) n
have zero₁ : false = Nat.testBit (↑Num.zero : ℕ) 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]
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
m : Num
n : ℕ
zero : Num.zero.testBit n = Nat.testBit (↑Num.zero : ℕ) n
zero₁ : false = Nat.testBit (↑Num.zero : ℕ) n
⊢ m.testBit n = Nat.testBit (↑m : ℕ) n
have pos : ∀ (m : PosNum), (pos m).testBit n = Nat.testBit (↑(pos 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]
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
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
⊢ m.testBit n = Nat.testBit (↑m : ℕ) n
have pos₁ : ∀ (m : PosNum), m.testBit n = Nat.testBit (↑(Num.pos 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]
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Num.Prime (goal)
Goal:
fuel : ℕ
n k : PosNum
h : Nat.sqrt (↑n : ℕ) < fuel + (↑k.bit1 : ℕ)
⊢ (↑(n.minFacAux fuel k) : ℕ) = Nat.minFacAux (↑n : ℕ) (↑k.bit1 : ℕ)
have zero : ∀ {k : PosNum} (h : Nat.sqrt (↑n : ℕ) < HAdd.hAdd (α := ℕ) 0 (↑k.bit1 : ℕ)),
  (↑(n.minFacAux 0 k) : ℕ) = Nat.minFacAux (↑n : ℕ) (↑k.bit1 : ℕ)
Tactic: induction fuel generalizing k
Cleared hypotheses: fuel, k, h
-- Lean 4 proof step from Mathlib.Data.Num.Prime (goal)
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 : ℕ)
⊢ (↑(n.minFacAux fuel k) : ℕ) = Nat.minFacAux (↑n : ℕ) (↑k.bit1 : ℕ)
have 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 : ℕ)
Tactic: induction fuel generalizing k
Cleared hypotheses: fuel, k, h
-- Lean 4 proof step from Mathlib.Data.Num.Prime (goal)
Goal:
n k : PosNum
h : Nat.sqrt (↑n : ℕ) < HAdd.hAdd (α := ℕ) 0 (↑k.bit1 : ℕ)
⊢ (↑(n.minFacAux 0 k) : ℕ) = Nat.minFacAux (↑n : ℕ) (↑k.bit1 : ℕ)
have 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)
Tactic: rw [minFacAux, Nat.minFacAux]
-- Lean 4 proof step from Mathlib.Data.Num.Prime (goal)
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 : ℕ)
⊢ (↑(n.minFacAux (n_1 + 1) k) : ℕ) = Nat.minFacAux (↑n : ℕ) (↑k.bit1 : ℕ)
have 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)
Tactic: rw [minFacAux, Nat.minFacAux]
-- Lean 4 proof step from Mathlib.Data.Num.Prime (hypothesis)
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)
have h₁ : (↑n : ℕ) < HMul.hMul (α := ℕ) (↑k.bit1 : ℕ) (↑k.bit1 : ℕ)
Tactic: rw [Nat.zero_add, Nat.sqrt_lt] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Num.Prime (goal)
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 : ℕ)
⊢ (↑(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)
have 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)
Tactic: simp_rw [← mul_to_nat]
-- Lean 4 proof step from Mathlib.Data.Num.Prime (goal)
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 : ℕ)
⊢ (↑(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)
have 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)
Tactic: simp only [cast_lt, dvd_to_nat]
-- Lean 4 proof step from Mathlib.Data.Num.Prime (goal)
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 : ℕ)
⊢ (↑(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)
have pos : n < k.bit1 * k.bit1 → Eq (α := ℕ) (↑n : ℕ) (↑n : ℕ)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Num.Prime (goal)
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 : ℕ)
⊢ (↑(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)
have pos₁ : ¬n < k.bit1 * k.bit1 → k.bit1 ∣ n → Eq (α := ℕ) (↑k.bit1 : ℕ) (↑k.bit1 : ℕ)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Num.Prime (goal)
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 : ℕ)
⊢ (↑(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)
have neg : ¬n < k.bit1 * k.bit1 →
  ¬k.bit1 ∣ n → (↑(n.minFacAux fuel k.succ) : ℕ) = Nat.minFacAux (↑n : ℕ) (HAdd.hAdd (α := ℕ) (↑k.bit1 : ℕ) 2)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Num.Prime (goal)
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
⊢ (↑(n.minFacAux fuel k.succ) : ℕ) = Nat.minFacAux (↑n : ℕ) (HAdd.hAdd (α := ℕ) (↑k.bit1 : ℕ) 2)
have neg : Nat.minFacAux (↑n : ℕ) (↑k.succ.bit1 : ℕ) = Nat.minFacAux (↑n : ℕ) (HAdd.hAdd (α := ℕ) (↑k.bit1 : ℕ) 2)
Tactic: rw [ih]
-- Lean 4 proof step from Mathlib.Data.Num.Prime (goal)
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)
⊢ (↑(n.minFacAux fuel k.succ) : ℕ) = Nat.minFacAux (↑n : ℕ) (HAdd.hAdd (α := ℕ) (↑k.bit1 : ℕ) 2)
have neg₁ : Nat.sqrt (↑n : ℕ) < fuel + (↑k.succ.bit1 : ℕ)
Tactic: rw [ih]
-- Lean 4 proof step from Mathlib.Data.Num.Prime (goal)
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.minFacAux (↑n : ℕ) (↑k.succ.bit1 : ℕ) = Nat.minFacAux (↑n : ℕ) (HAdd.hAdd (α := ℕ) (↑k.bit1 : ℕ) 2)
have neg : (↑k.succ.bit1 : ℕ) = HAdd.hAdd (α := ℕ) (↑k.bit1 : ℕ) 2
Tactic: congr
-- Lean 4 proof step from Mathlib.Data.Num.Prime (goal)
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 + (↑k.succ.bit1 : ℕ)
have h₁ : fuel + (↑k.succ.bit1 : ℕ) = (fuel + 1 + (↑k.bit1 : ℕ)).succ
Tactic: convert! Nat.lt_succ_of_lt h using 1
-- Lean 4 proof step from Mathlib.Data.Num.Prime (goal)
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
⊢ (↑(n.minFacAux fuel k.succ) : ℕ) = Nat.minFacAux (↑n : ℕ) (HAdd.hAdd (α := ℕ) (↑k.bit1 : ℕ) 2)
have neg : (↑k.succ.bit1 : ℕ) = HAdd.hAdd (α := ℕ) (↑k.bit1 : ℕ) 2
Tactic: rw [ih] <;> [congr; convert! Nat.lt_succ_of_lt h using 1]
-- Lean 4 proof step from Mathlib.Data.Num.Prime (goal)
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
⊢ (↑(n.minFacAux fuel k.succ) : ℕ) = Nat.minFacAux (↑n : ℕ) (HAdd.hAdd (α := ℕ) (↑k.bit1 : ℕ) 2)
have h₁ : fuel + (↑k.succ.bit1 : ℕ) = (fuel + 1 + (↑k.bit1 : ℕ)).succ
Tactic: rw [ih] <;> [congr; convert! Nat.lt_succ_of_lt h using 1]
-- Lean 4 proof step from Mathlib.Data.Num.Prime (goal)
Goal:
n : PosNum
⊢ (↑n.minFac : ℕ) = Nat.minFac (↑n : ℕ)
have one : (↑one.minFac : ℕ) = Nat.minFac (↑one : ℕ)
Tactic: obtain - | n := n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Num.Prime (goal)
Goal:
n : PosNum
one : (↑PosNum.one.minFac : ℕ) = Nat.minFac (↑PosNum.one : ℕ)
⊢ (↑n.minFac : ℕ) = Nat.minFac (↑n : ℕ)
have bit1 : ∀ (n : PosNum), (↑n.bit1.minFac : ℕ) = Nat.minFac (↑n.bit1 : ℕ)
Tactic: obtain - | n := n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Num.Prime (goal)
Goal:
n : PosNum
one : (↑PosNum.one.minFac : ℕ) = Nat.minFac (↑PosNum.one : ℕ)
bit1 : ∀ (n : PosNum), (↑n.bit1.minFac : ℕ) = Nat.minFac (↑n.bit1 : ℕ)
⊢ (↑n.minFac : ℕ) = Nat.minFac (↑n : ℕ)
have bit0 : ∀ (a : PosNum), (↑a.bit0.minFac : ℕ) = Nat.minFac (↑a.bit0 : ℕ)
Tactic: obtain - | n := n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Num.Prime (goal)
Goal:
n : PosNum
⊢ (↑n.bit1.minFac : ℕ) = Nat.minFac (↑n.bit1 : ℕ)
have bit1 : (↑(n.bit1.minFacAux (↑n : ℕ) 1) : ℕ) = Nat.minFacAux (↑n.bit1 : ℕ) 3
Tactic: rw [minFac, Nat.minFac_eq, if_neg]
-- Lean 4 proof step from Mathlib.Data.Num.Prime (goal)
Goal:
n : PosNum
bit1 : (↑(n.bit1.minFacAux (↑n : ℕ) 1) : ℕ) = Nat.minFacAux (↑n.bit1 : ℕ) 3
⊢ (↑n.bit1.minFac : ℕ) = Nat.minFac (↑n.bit1 : ℕ)
have bit1₁ : ¬Dvd.dvd (α := ℕ) 2 (↑n.bit1 : ℕ)
Tactic: rw [minFac, Nat.minFac_eq, if_neg]
-- Lean 4 proof step from Mathlib.Data.Num.Prime (goal)
Goal:
n : PosNum
⊢ (↑(n.bit1.minFacAux (↑n : ℕ) 1) : ℕ) = Nat.minFacAux (↑n.bit1 : ℕ) 3
have bit1 : Nat.minFacAux (↑n.bit1 : ℕ) (↑(bit1 1) : ℕ) = Nat.minFacAux (↑n.bit1 : ℕ) 3
Tactic: rw [minFacAux_to_nat]
-- Lean 4 proof step from Mathlib.Data.Num.Prime (goal)
Goal:
n : PosNum
bit1 : Nat.minFacAux (↑n.bit1 : ℕ) (↑(PosNum.bit1 1) : ℕ) = Nat.minFacAux (↑n.bit1 : ℕ) 3
⊢ (↑(n.bit1.minFacAux (↑n : ℕ) 1) : ℕ) = Nat.minFacAux (↑n.bit1 : ℕ) 3
have bit1₁ : Nat.sqrt (↑n.bit1 : ℕ) < HAdd.hAdd (α := ℕ) (↑n : ℕ) (↑(PosNum.bit1 1) : ℕ)
Tactic: rw [minFacAux_to_nat]