awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Nat.Basic (goal)
Goal:
a : ℕ
ha : a ≠ 1
b : ℕ
zero : a * 0 ≤ HPow.hPow (β := ℕ) a 0
⊢ a * b ≤ a ^ b
have succ : ∀ (b : ℕ), a * (b + 1) ≤ a ^ (b + 1)
Tactic: cases b with
  | zero => exact Nat.zero_le _
  | succ b =>
      obtain rfl | ha0 : a = 0 ∨ a > 0 := a.eq_zero_or_pos
      · rw [Nat.zero_mul]; exact Nat.zero_le _
      · have ha1 : a > 1 := Nat.lt_of_le_of_ne ha0 ha.symm
        rw [Nat.pow_succ']; exact Nat.mul_le_mul_left a (Nat.lt_pow_self ha1)
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Nat.Basic (goal)
Goal:
k : ℕ
⊢ 2 * HPow.hPow (β := ℕ) k 2 + 1 ≤ HPow.hPow (α := ℕ) 2 (2 * k)
have inl : 2 * HPow.hPow (α := ℕ) (β := ℕ) 0 2 + 1 ≤ HPow.hPow (α := ℕ) 2 (HMul.hMul (α := ℕ) 2 0)
Tactic: obtain rfl | hk : k = 0 ∨ k > 0 := k.eq_zero_or_pos
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Data.Nat.Basic (goal)
Goal:
k : ℕ
inl : 2 * HPow.hPow (α := ℕ) (β := ℕ) 0 2 + 1 ≤ HPow.hPow (α := ℕ) 2 (HMul.hMul (α := ℕ) 2 0)
⊢ 2 * HPow.hPow (β := ℕ) k 2 + 1 ≤ HPow.hPow (α := ℕ) 2 (2 * k)
have inr : ∀ (hk : k > 0), 2 * HPow.hPow (β := ℕ) k 2 + 1 ≤ HPow.hPow (α := ℕ) 2 (2 * k)
Tactic: obtain rfl | hk : k = 0 ∨ k > 0 := k.eq_zero_or_pos
-- Lean 4 proof step from Mathlib.Data.Nat.Basic (hypothesis)
Goal:
k : ℕ
hk : k > 0
⊢ 2 * HPow.hPow (β := ℕ) k 2 + 1 ≤ HPow.hPow (α := ℕ) 2 (2 * k)
have hk0 : 0 < 2 * HPow.hPow (β := ℕ) k 2
Tactic: have hk0 : 0 < 2 * k ^ 2 := Nat.mul_pos Nat.two_pos (Nat.pow_pos hk)
-- Lean 4 proof step from Mathlib.Data.Nat.Basic (goal)
Goal:
k : ℕ
hk : k > 0
hk0 : 0 < 2 * HPow.hPow (β := ℕ) k 2
⊢ 2 * HPow.hPow (β := ℕ) k 2 + 2 * HPow.hPow (β := ℕ) k 2 = HPow.hPow (β := ℕ) (2 * k) 2
have rw : 2 * HPow.hPow (β := ℕ) k 2 + 2 * HPow.hPow (β := ℕ) k 2 = HPow.hPow (α := ℕ) (β := ℕ) 2 2 * HPow.hPow (β := ℕ) k 2
Tactic: rw [Nat.mul_pow, ← Nat.add_mul]
-- Lean 4 proof step from Mathlib.Data.Nat.Basic (goal)
Goal:
k : ℕ
hk : k > 0
hk0 : 0 < 2 * HPow.hPow (β := ℕ) k 2
rw : 2 * HPow.hPow (β := ℕ) k 2 + 2 * HPow.hPow (β := ℕ) k 2 = HPow.hPow (α := ℕ) (β := ℕ) 2 2 * HPow.hPow (β := ℕ) k 2
⊢ 2 * HPow.hPow (β := ℕ) k 2 + 2 * HPow.hPow (β := ℕ) k 2 = HPow.hPow (β := ℕ) (2 * k) 2
have rw₁ : HAdd.hAdd (α := ℕ) 2 2 * HPow.hPow (β := ℕ) k 2 = HPow.hPow (α := ℕ) (β := ℕ) 2 2 * HPow.hPow (β := ℕ) k 2
Tactic: rw [Nat.mul_pow, ← Nat.add_mul]
-- Lean 4 proof step from Mathlib.Data.Nat.Basic (goal)
Goal:
k : ℕ
hk : k > 0
hk0 : 0 < 2 * HPow.hPow (β := ℕ) k 2
⊢ 2 * HPow.hPow (β := ℕ) k 2 + 1 ≤ HPow.hPow (α := ℕ) 2 (2 * k)
have calc : 2 * HPow.hPow (β := ℕ) k 2 + 2 * HPow.hPow (β := ℕ) k 2 = HPow.hPow (β := ℕ) (2 * k) 2
Tactic: calc 2 * k ^ 2
      _ < 2 * k ^ 2 + 2 * k ^ 2 := Nat.lt_add_of_pos_left hk0
      _ = (2 * k) ^ 2 := by rw [Nat.mul_pow, ← Nat.add_mul]
      _ ≤ (2 ^ k) ^ 2 := Nat.pow_le_pow_left (Nat.mul_le_pow (by decide : 2 ≠ 1) _) 2
      _ = 2 ^ (2 * k) := (Nat.pow_mul' _ _ _).symm
-- Lean 4 proof step from Mathlib.Data.Nat.BinaryRec (goal)
Goal:
n : Nat
⊢ bit (decide (n % 2 = 1)) (HShiftRight.hShiftRight (β := Nat) n 1) = n
have simp : (bif decide (n % 2 = 1) then 2 * (n / 2) + 1 else 2 * (n / 2)) = n
Tactic: simp only [bit, shiftRight_one]
-- Lean 4 proof step from Mathlib.Data.Nat.BinaryRec (hypothesis)
Goal:
n : Nat
⊢ (bif decide (n % 2 = 1) then 2 * (n / 2) + 1 else 2 * (n / 2)) = n
have x : n % 2 = 0 ∨ n % 2 = 1
Tactic: cases mod_two_eq_zero_or_one n with | _ h => simpa [h] using Nat.div_add_mod n 2
-- Lean 4 proof step from Mathlib.Data.Nat.BinaryRec (goal)
Goal:
n : Nat
b : Bool
⊢ bit b n = 0 ↔ n = 0 ∧ b = false
have zero : bit b 0 = 0 ↔ Eq (α := Nat) 0 0 ∧ b = false
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.BinaryRec (goal)
Goal:
n : Nat
b : Bool
zero : bit b 0 = 0 ↔ Eq (α := Nat) 0 0 ∧ b = false
⊢ bit b n = 0 ↔ n = 0 ∧ b = false
have succ : ∀ (n : Nat), bit b (n + 1) = 0 ↔ n + 1 = 0 ∧ b = false
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.BinaryRec (goal)
Goal:
b : Bool
⊢ bit b 0 = 0 ↔ Eq (α := Nat) 0 0 ∧ b = false
have zero : bit false 0 = 0 ↔ Eq (α := Nat) 0 0 ∧ false = false
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Nat.BinaryRec (goal)
Goal:
b : Bool
zero : bit false 0 = 0 ↔ Eq (α := Nat) 0 0 ∧ false = false
⊢ bit b 0 = 0 ↔ Eq (α := Nat) 0 0 ∧ b = false
have zero₁ : bit true 0 = 0 ↔ Eq (α := Nat) 0 0 ∧ true = false
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Nat.BinaryRec (goal)
Goal:
b : Bool
n : Nat
⊢ bit b (n + 1) = 0 ↔ n + 1 = 0 ∧ b = false
have succ : bit false (n + 1) = 0 ↔ n + 1 = 0 ∧ false = false
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Nat.BinaryRec (goal)
Goal:
b : Bool
n : Nat
succ : bit false (n + 1) = 0 ↔ n + 1 = 0 ∧ false = false
⊢ bit b (n + 1) = 0 ↔ n + 1 = 0 ∧ b = false
have succ₁ : bit true (n + 1) = 0 ↔ n + 1 = 0 ∧ true = false
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Nat.BinaryRec (goal)
Goal:
b : Bool
x n : Nat
⊢ bit b x < HPow.hPow (α := Nat) 2 (n + 1) ↔ x < HPow.hPow (α := Nat) 2 n
have false : bit false x < HPow.hPow (α := Nat) 2 (n + 1) ↔ x < HPow.hPow (α := Nat) 2 n
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Nat.BinaryRec (goal)
Goal:
b : Bool
x n : Nat
false : bit Bool.false x < HPow.hPow (α := Nat) 2 (n + 1) ↔ x < HPow.hPow (α := Nat) 2 n
⊢ bit b x < HPow.hPow (α := Nat) 2 (n + 1) ↔ x < HPow.hPow (α := Nat) 2 n
have true : bit true x < HPow.hPow (α := Nat) 2 (n + 1) ↔ x < HPow.hPow (α := Nat) 2 n
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Nat.BinaryRec (goal)
Goal:
n : Nat
n0 : ¬n = 0
⊢ (if HShiftRight.hShiftRight (β := Nat) n 1 = 0 then 0 else (HShiftRight.hShiftRight (β := Nat) n 1).log2.succ) <
    if n = 0 then 0 else n.log2.succ
have zero : ∀ (n0 : ¬Eq (α := Nat) 0 0),
  (if HShiftRight.hShiftRight (α := Nat) (β := Nat) 0 1 = 0 then 0
    else (HShiftRight.hShiftRight (α := Nat) (β := Nat) 0 1).log2.succ) <
    if Eq (α := Nat) 0 0 then 0 else (log2 0).succ
Tactic: obtain _ | n := n
Cleared hypotheses: n, n0
-- Lean 4 proof step from Mathlib.Data.Nat.BinaryRec (goal)
Goal:
n : Nat
n0 : ¬n = 0
zero :
  ∀ (n0 : ¬Eq (α := Nat) 0 0),
    (if HShiftRight.hShiftRight (α := Nat) (β := Nat) 0 1 = 0 then 0
      else (HShiftRight.hShiftRight (α := Nat) (β := Nat) 0 1).log2.succ) <
      if Eq (α := Nat) 0 0 then 0 else (log2 0).succ
⊢ (if HShiftRight.hShiftRight (β := Nat) n 1 = 0 then 0 else (HShiftRight.hShiftRight (β := Nat) n 1).log2.succ) <
    if n = 0 then 0 else n.log2.succ
have succ : ∀ (n : Nat) (n0 : ¬n + 1 = 0),
  (if HShiftRight.hShiftRight (β := Nat) (n + 1) 1 = 0 then 0
    else (HShiftRight.hShiftRight (β := Nat) (n + 1) 1).log2.succ) <
    if n + 1 = 0 then 0 else (n + 1).log2.succ
Tactic: obtain _ | n := n
Cleared hypotheses: n, n0
-- Lean 4 proof step from Mathlib.Data.Nat.BinaryRec (goal)
Goal:
n : Nat
n0 : ¬n + 1 = 0
⊢ (if HShiftRight.hShiftRight (β := Nat) (n + 1) 1 = 0 then 0
    else (HShiftRight.hShiftRight (β := Nat) (n + 1) 1).log2.succ) <
    if n + 1 = 0 then 0 else (n + 1).log2.succ
have succ : ∀ (n0 : ¬HAdd.hAdd (α := Nat) 0 1 = 0),
  (if HShiftRight.hShiftRight (β := Nat) (HAdd.hAdd (α := Nat) 0 1) 1 = 0 then 0
    else (HShiftRight.hShiftRight (β := Nat) (HAdd.hAdd (α := Nat) 0 1) 1).log2.succ) <
    if HAdd.hAdd (α := Nat) 0 1 = 0 then 0 else (HAdd.hAdd (α := Nat) 0 1).log2.succ
Tactic: obtain _ | n := n
Cleared hypotheses: n, n0
-- Lean 4 proof step from Mathlib.Data.Nat.BinaryRec (goal)
Goal:
n : Nat
n0 : ¬n + 1 = 0
succ :
  ∀ (n0 : ¬HAdd.hAdd (α := Nat) 0 1 = 0),
    (if HShiftRight.hShiftRight (β := Nat) (HAdd.hAdd (α := Nat) 0 1) 1 = 0 then 0
      else (HShiftRight.hShiftRight (β := Nat) (HAdd.hAdd (α := Nat) 0 1) 1).log2.succ) <
      if HAdd.hAdd (α := Nat) 0 1 = 0 then 0 else (HAdd.hAdd (α := Nat) 0 1).log2.succ
⊢ (if HShiftRight.hShiftRight (β := Nat) (n + 1) 1 = 0 then 0
    else (HShiftRight.hShiftRight (β := Nat) (n + 1) 1).log2.succ) <
    if n + 1 = 0 then 0 else (n + 1).log2.succ
have succ₁ : ∀ (n : Nat) (n0 : ¬n + 1 + 1 = 0),
  (if HShiftRight.hShiftRight (β := Nat) (n + 1 + 1) 1 = 0 then 0
    else (HShiftRight.hShiftRight (β := Nat) (n + 1 + 1) 1).log2.succ) <
    if n + 1 + 1 = 0 then 0 else (n + 1 + 1).log2.succ
Tactic: obtain _ | n := n
Cleared hypotheses: n, n0
-- Lean 4 proof step from Mathlib.Data.Nat.BinaryRec (hypothesis)
Goal:
n : Nat
n0 : ¬n + 1 + 1 = 0
⊢ (if HShiftRight.hShiftRight (β := Nat) (n + 1 + 1) 1 = 0 then 0
    else (HShiftRight.hShiftRight (β := Nat) (n + 1 + 1) 1).log2.succ) <
    if n + 1 + 1 = 0 then 0 else (n + 1 + 1).log2.succ
have this : HShiftRight.hShiftRight (β := Nat) (n + 1 + 1) 1 ≠ 0
Tactic: have : (n + 1 + 1) >>> 1 ≠ 0 := Nat.div_ne_zero_iff.mpr ⟨by decide, le_add_left ..⟩
-- Lean 4 proof step from Mathlib.Data.Nat.BinaryRec (goal)
Goal:
n : Nat
n0 : ¬n = 0
⊢ (if HShiftRight.hShiftRight (β := Nat) n 1 = 0 then 0 else (HShiftRight.hShiftRight (β := Nat) n 1).log2.succ) <
    if n = 0 then 0 else n.log2.succ
have zero : ∀ (n0 : ¬Eq (α := Nat) 0 0),
  (if HShiftRight.hShiftRight (α := Nat) (β := Nat) 0 1 = 0 then 0
    else (HShiftRight.hShiftRight (α := Nat) (β := Nat) 0 1).log2.succ) <
    if Eq (α := Nat) 0 0 then 0 else (log2 0).succ
Tactic: decreasing_by
  obtain _ | n := n; · exact (n0 rfl).elim
  obtain _ | n := n; · simp
  have : (n + 1 + 1) >>> 1 ≠ 0 := Nat.div_ne_zero_iff.mpr ⟨by decide, le_add_left ..⟩
  simpa only [if_neg n0, if_neg this, log2_eq_succ_log2_shiftRight this] using lt_succ_self _
Cleared hypotheses: n, n0
-- Lean 4 proof step from Mathlib.Data.Nat.BinaryRec (goal)
Goal:
n : Nat
n0 : ¬n = 0
zero :
  ∀ (n0 : ¬Eq (α := Nat) 0 0),
    (if HShiftRight.hShiftRight (α := Nat) (β := Nat) 0 1 = 0 then 0
      else (HShiftRight.hShiftRight (α := Nat) (β := Nat) 0 1).log2.succ) <
      if Eq (α := Nat) 0 0 then 0 else (log2 0).succ
⊢ (if HShiftRight.hShiftRight (β := Nat) n 1 = 0 then 0 else (HShiftRight.hShiftRight (β := Nat) n 1).log2.succ) <
    if n = 0 then 0 else n.log2.succ
have succ : ∀ (n : Nat) (n0 : ¬n + 1 = 0),
  (if HShiftRight.hShiftRight (β := Nat) (n + 1) 1 = 0 then 0
    else (HShiftRight.hShiftRight (β := Nat) (n + 1) 1).log2.succ) <
    if n + 1 = 0 then 0 else (n + 1).log2.succ
Tactic: decreasing_by
  obtain _ | n := n; · exact (n0 rfl).elim
  obtain _ | n := n; · simp
  have : (n + 1 + 1) >>> 1 ≠ 0 := Nat.div_ne_zero_iff.mpr ⟨by decide, le_add_left ..⟩
  simpa only [if_neg n0, if_neg this, log2_eq_succ_log2_shiftRight this] using lt_succ_self _
Cleared hypotheses: n, n0
-- Lean 4 proof step from Mathlib.Data.Nat.BinaryRec (goal)
Goal:
n : Nat
n0 : ¬n = 0
zero :
  ∀ (n0 : ¬Eq (α := Nat) 0 0),
    (if HShiftRight.hShiftRight (α := Nat) (β := Nat) 0 1 = 0 then 0
      else (HShiftRight.hShiftRight (α := Nat) (β := Nat) 0 1).log2.succ) <
      if Eq (α := Nat) 0 0 then 0 else (log2 0).succ
succ :
  ∀ (n : Nat) (n0 : ¬n + 1 = 0),
    (if HShiftRight.hShiftRight (β := Nat) (n + 1) 1 = 0 then 0
      else (HShiftRight.hShiftRight (β := Nat) (n + 1) 1).log2.succ) <
      if n + 1 = 0 then 0 else (n + 1).log2.succ
zero₁ :
  ∀ (n0 : ¬Eq (α := Nat) 0 0),
    (if HShiftRight.hShiftRight (α := Nat) (β := Nat) 0 1 = 0 then 0
      else (HShiftRight.hShiftRight (α := Nat) (β := Nat) 0 1).log2.succ) <
      if Eq (α := Nat) 0 0 then 0 else (log2 0).succ
succ₁ succ₂ :
  ∀ (n : Nat) (n0 : ¬n + 1 = 0),
    (if HShiftRight.hShiftRight (β := Nat) (n + 1) 1 = 0 then 0
      else (HShiftRight.hShiftRight (β := Nat) (n + 1) 1).log2.succ) <
      if n + 1 = 0 then 0 else (n + 1).log2.succ
⊢ (if HShiftRight.hShiftRight (β := Nat) n 1 = 0 then 0 else (HShiftRight.hShiftRight (β := Nat) n 1).log2.succ) <
    if n = 0 then 0 else n.log2.succ
have succ₃ : ∀ (n0 : ¬HAdd.hAdd (α := Nat) 0 1 = 0),
  (if HShiftRight.hShiftRight (β := Nat) (HAdd.hAdd (α := Nat) 0 1) 1 = 0 then 0
    else (HShiftRight.hShiftRight (β := Nat) (HAdd.hAdd (α := Nat) 0 1) 1).log2.succ) <
    if HAdd.hAdd (α := Nat) 0 1 = 0 then 0 else (HAdd.hAdd (α := Nat) 0 1).log2.succ
Tactic: decreasing_by
  obtain _ | n := n; · exact (n0 rfl).elim
  obtain _ | n := n; · simp
  have : (n + 1 + 1) >>> 1 ≠ 0 := Nat.div_ne_zero_iff.mpr ⟨by decide, le_add_left ..⟩
  simpa only [if_neg n0, if_neg this, log2_eq_succ_log2_shiftRight this] using lt_succ_self _
Cleared hypotheses: n, n0
-- Lean 4 proof step from Mathlib.Data.Nat.BinaryRec (goal)
Goal:
n : Nat
n0 : ¬n = 0
zero :
  ∀ (n0 : ¬Eq (α := Nat) 0 0),
    (if HShiftRight.hShiftRight (α := Nat) (β := Nat) 0 1 = 0 then 0
      else (HShiftRight.hShiftRight (α := Nat) (β := Nat) 0 1).log2.succ) <
      if Eq (α := Nat) 0 0 then 0 else (log2 0).succ
succ :
  ∀ (n : Nat) (n0 : ¬n + 1 = 0),
    (if HShiftRight.hShiftRight (β := Nat) (n + 1) 1 = 0 then 0
      else (HShiftRight.hShiftRight (β := Nat) (n + 1) 1).log2.succ) <
      if n + 1 = 0 then 0 else (n + 1).log2.succ
zero₁ :
  ∀ (n0 : ¬Eq (α := Nat) 0 0),
    (if HShiftRight.hShiftRight (α := Nat) (β := Nat) 0 1 = 0 then 0
      else (HShiftRight.hShiftRight (α := Nat) (β := Nat) 0 1).log2.succ) <
      if Eq (α := Nat) 0 0 then 0 else (log2 0).succ
succ₁ succ₂ :
  ∀ (n : Nat) (n0 : ¬n + 1 = 0),
    (if HShiftRight.hShiftRight (β := Nat) (n + 1) 1 = 0 then 0
      else (HShiftRight.hShiftRight (β := Nat) (n + 1) 1).log2.succ) <
      if n + 1 = 0 then 0 else (n + 1).log2.succ
succ₃ :
  ∀ (n0 : ¬HAdd.hAdd (α := Nat) 0 1 = 0),
    (if HShiftRight.hShiftRight (β := Nat) (HAdd.hAdd (α := Nat) 0 1) 1 = 0 then 0
      else (HShiftRight.hShiftRight (β := Nat) (HAdd.hAdd (α := Nat) 0 1) 1).log2.succ) <
      if HAdd.hAdd (α := Nat) 0 1 = 0 then 0 else (HAdd.hAdd (α := Nat) 0 1).log2.succ
⊢ (if HShiftRight.hShiftRight (β := Nat) n 1 = 0 then 0 else (HShiftRight.hShiftRight (β := Nat) n 1).log2.succ) <
    if n = 0 then 0 else n.log2.succ
have succ₄ : ∀ (n : Nat) (n0 : ¬n + 1 + 1 = 0),
  (if HShiftRight.hShiftRight (β := Nat) (n + 1 + 1) 1 = 0 then 0
    else (HShiftRight.hShiftRight (β := Nat) (n + 1 + 1) 1).log2.succ) <
    if n + 1 + 1 = 0 then 0 else (n + 1 + 1).log2.succ
Tactic: decreasing_by
  obtain _ | n := n; · exact (n0 rfl).elim
  obtain _ | n := n; · simp
  have : (n + 1 + 1) >>> 1 ≠ 0 := Nat.div_ne_zero_iff.mpr ⟨by decide, le_add_left ..⟩
  simpa only [if_neg n0, if_neg this, log2_eq_succ_log2_shiftRight this] using lt_succ_self _
Cleared hypotheses: n, n0
-- Lean 4 proof step from Mathlib.Data.Nat.BinaryRec (goal)
Goal:
n : Nat
n0 : ¬n = 0
zero :
  ∀ (n0 : ¬Eq (α := Nat) 0 0),
    (if HShiftRight.hShiftRight (α := Nat) (β := Nat) 0 1 = 0 then 0
      else (HShiftRight.hShiftRight (α := Nat) (β := Nat) 0 1).log2.succ) <
      if Eq (α := Nat) 0 0 then 0 else (log2 0).succ
succ :
  ∀ (n : Nat) (n0 : ¬n + 1 = 0),
    (if HShiftRight.hShiftRight (β := Nat) (n + 1) 1 = 0 then 0
      else (HShiftRight.hShiftRight (β := Nat) (n + 1) 1).log2.succ) <
      if n + 1 = 0 then 0 else (n + 1).log2.succ
zero₁ :
  ∀ (n0 : ¬Eq (α := Nat) 0 0),
    (if HShiftRight.hShiftRight (α := Nat) (β := Nat) 0 1 = 0 then 0
      else (HShiftRight.hShiftRight (α := Nat) (β := Nat) 0 1).log2.succ) <
      if Eq (α := Nat) 0 0 then 0 else (log2 0).succ
succ₁ succ₂ :
  ∀ (n : Nat) (n0 : ¬n + 1 = 0),
    (if HShiftRight.hShiftRight (β := Nat) (n + 1) 1 = 0 then 0
      else (HShiftRight.hShiftRight (β := Nat) (n + 1) 1).log2.succ) <
      if n + 1 = 0 then 0 else (n + 1).log2.succ
succ₃ :
  ∀ (n0 : ¬HAdd.hAdd (α := Nat) 0 1 = 0),
    (if HShiftRight.hShiftRight (β := Nat) (HAdd.hAdd (α := Nat) 0 1) 1 = 0 then 0
      else (HShiftRight.hShiftRight (β := Nat) (HAdd.hAdd (α := Nat) 0 1) 1).log2.succ) <
      if HAdd.hAdd (α := Nat) 0 1 = 0 then 0 else (HAdd.hAdd (α := Nat) 0 1).log2.succ
succ₄ :
  ∀ (n : Nat) (n0 : ¬n + 1 + 1 = 0),
    (if HShiftRight.hShiftRight (β := Nat) (n + 1 + 1) 1 = 0 then 0
      else (HShiftRight.hShiftRight (β := Nat) (n + 1 + 1) 1).log2.succ) <
      if n + 1 + 1 = 0 then 0 else (n + 1 + 1).log2.succ
succ₅ :
  ∀ (n0 : ¬HAdd.hAdd (α := Nat) 0 1 = 0),
    (if HShiftRight.hShiftRight (β := Nat) (HAdd.hAdd (α := Nat) 0 1) 1 = 0 then 0
      else (HShiftRight.hShiftRight (β := Nat) (HAdd.hAdd (α := Nat) 0 1) 1).log2.succ) <
      if HAdd.hAdd (α := Nat) 0 1 = 0 then 0 else (HAdd.hAdd (α := Nat) 0 1).log2.succ
succ₆ succ₇ :
  ∀ (n : Nat) (n0 : ¬n + 1 + 1 = 0),
    (if HShiftRight.hShiftRight (β := Nat) (n + 1 + 1) 1 = 0 then 0
      else (HShiftRight.hShiftRight (β := Nat) (n + 1 + 1) 1).log2.succ) <
      if n + 1 + 1 = 0 then 0 else (n + 1 + 1).log2.succ
⊢ (if HShiftRight.hShiftRight (β := Nat) n 1 = 0 then 0 else (HShiftRight.hShiftRight (β := Nat) n 1).log2.succ) <
    if n = 0 then 0 else n.log2.succ
have succ₈ : ∀ (n : Nat) (n0 : ¬n + 1 + 1 = 0) (this : HShiftRight.hShiftRight (β := Nat) (n + 1 + 1) 1 ≠ 0),
  (if HShiftRight.hShiftRight (β := Nat) (n + 1 + 1) 1 = 0 then 0
    else (HShiftRight.hShiftRight (β := Nat) (n + 1 + 1) 1).log2.succ) <
    if n + 1 + 1 = 0 then 0 else (n + 1 + 1).log2.succ
Tactic: decreasing_by
  obtain _ | n := n; · exact (n0 rfl).elim
  obtain _ | n := n; · simp
  have : (n + 1 + 1) >>> 1 ≠ 0 := Nat.div_ne_zero_iff.mpr ⟨by decide, le_add_left ..⟩
  simpa only [if_neg n0, if_neg this, log2_eq_succ_log2_shiftRight this] using lt_succ_self _
Cleared hypotheses: n, n0
-- Lean 4 proof step from Mathlib.Data.Nat.BinaryRec (goal)
Goal:
motive : Nat → Sort u
zero : motive 0
bit : (b : Bool) → (n : Nat) → (n = 0 → b = true) → motive n → motive (Nat.bit b n)
b : Bool
n : Nat
ih : motive n
h : ¬(n = 0 → b = true)
⊢ Nat.bit b n = 0
have rw : n = 0 ∧ b = false
Tactic: rw [bit_eq_zero_iff]
-- Lean 4 proof step from Mathlib.Data.Nat.BinaryRec (goal)
Goal:
motive : Nat → Sort u
zero : motive 0
bit : (b : Bool) → (n : Nat) → (n = 0 → b = true) → motive n → motive (Nat.bit b n)
b : Bool
n : Nat
ih : motive n
h : ¬(n = 0 → b = true)
⊢ n = 0 ∧ b = false
have zero₁ : ∀ (ih : motive 0) (h : ¬(Eq (α := Nat) 0 0 → b = true)), Eq (α := Nat) 0 0 ∧ b = false
Tactic: cases n
Cleared hypotheses: n, ih, h
-- Lean 4 proof step from Mathlib.Data.Nat.BinaryRec (goal)
Goal:
motive : Nat → Sort u
zero : motive 0
bit : (b : Bool) → (n : Nat) → (n = 0 → b = true) → motive n → motive (Nat.bit b n)
b : Bool
n : Nat
ih : motive n
h : ¬(n = 0 → b = true)
zero₁ : ∀ (ih : motive 0) (h : ¬(Eq (α := Nat) 0 0 → b = true)), Eq (α := Nat) 0 0 ∧ b = false
⊢ n = 0 ∧ b = false
have succ : ∀ (n : Nat) (ih : motive (n + 1)) (h : ¬(n + 1 = 0 → b = true)), n + 1 = 0 ∧ b = false
Tactic: cases n
Cleared hypotheses: n, ih, h
-- Lean 4 proof step from Mathlib.Data.Nat.BinaryRec (goal)
Goal:
motive : Nat → Sort u
zero : motive 0
bit : (b : Bool) → (n : Nat) → (n = 0 → b = true) → motive n → motive (Nat.bit b n)
b : Bool
ih : motive 0
h : ¬(Eq (α := Nat) 0 0 → b = true)
⊢ Eq (α := Nat) 0 0 ∧ b = false
have zero₁ : ∀ (h : ¬(Eq (α := Nat) 0 0 → false = true)), Eq (α := Nat) 0 0 ∧ false = false
Tactic: cases b
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Data.Nat.BinaryRec (goal)
Goal:
motive : Nat → Sort u
zero : motive 0
bit : (b : Bool) → (n : Nat) → (n = 0 → b = true) → motive n → motive (Nat.bit b n)
b : Bool
ih : motive 0
h : ¬(Eq (α := Nat) 0 0 → b = true)
zero₁ : ∀ (h : ¬(Eq (α := Nat) 0 0 → false = true)), Eq (α := Nat) 0 0 ∧ false = false
⊢ Eq (α := Nat) 0 0 ∧ b = false
have zero₂ : ∀ (h : ¬(Eq (α := Nat) 0 0 → true = true)), Eq (α := Nat) 0 0 ∧ true = false
Tactic: cases b
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Data.Nat.BinaryRec (goal)
Goal:
motive : Nat → Sort u
zero : motive 0
bit : (b : Bool) → (n : Nat) → (n = 0 → b = true) → motive n → motive (Nat.bit b n)
b : Bool
n : Nat
ih : motive (n + 1)
h : ¬(n + 1 = 0 → b = true)
⊢ n + 1 = 0 ∧ b = false
have succ : ∀ (h : ¬(n + 1 = 0 → false = true)), n + 1 = 0 ∧ false = false
Tactic: cases b
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Data.Nat.BinaryRec (goal)
Goal:
motive : Nat → Sort u
zero : motive 0
bit : (b : Bool) → (n : Nat) → (n = 0 → b = true) → motive n → motive (Nat.bit b n)
b : Bool
n : Nat
ih : motive (n + 1)
h : ¬(n + 1 = 0 → b = true)
succ : ∀ (h : ¬(n + 1 = 0 → false = true)), n + 1 = 0 ∧ false = false
⊢ n + 1 = 0 ∧ b = false
have succ₁ : ∀ (h : ¬(n + 1 = 0 → true = true)), n + 1 = 0 ∧ true = false
Tactic: cases b
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Data.Nat.BinaryRec (goal)
Goal:
motive : Nat → Sort u
zero : motive 0
one : motive 1
bit : (b : Bool) → (n : Nat) → n ≠ 0 → motive n → motive (Nat.bit b n)
b : Bool
n : Nat
h : n = 0 → b = true
ih : motive n
h' : n = 0
⊢ Nat.bit b n = Nat.bit true 0
have rw : Nat.bit b 0 = Nat.bit true 0
Tactic: rw [h', h h']
-- Lean 4 proof step from Mathlib.Data.Nat.BinaryRec (goal)
Goal:
motive : Nat → Sort u
zero : motive 0
one : motive 1
bit : (b : Bool) → (n : Nat) → n ≠ 0 → motive n → motive (Nat.bit b n)
b : Bool
n : Nat
h : n = 0 → b = true
ih : motive n
h' : n = 0
rw : Nat.bit b 0 = Nat.bit true 0
⊢ Nat.bit b n = Nat.bit true 0
have rw₁ : Nat.bit true 0 = Nat.bit true 0
Tactic: rw [h', h h']
-- Lean 4 proof step from Mathlib.Data.Nat.BinaryRec (goal)
Goal:
b : Bool
n : Nat
⊢ bit b n = 2 * n + b.toNat
have false : bit false n = 2 * n + false.toNat
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Nat.BinaryRec (goal)
Goal:
b : Bool
n : Nat
false : bit Bool.false n = 2 * n + Bool.false.toNat
⊢ bit b n = 2 * n + b.toNat
have true : bit true n = 2 * n + true.toNat
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Nat.BinaryRec (goal)
Goal:
b : Bool
n : Nat
⊢ bit b n / 2 = n
have rw : b.toNat < 2
Tactic: rw [bit_val, Nat.add_comm, add_mul_div_left, div_eq_of_lt, Nat.zero_add]
-- Lean 4 proof step from Mathlib.Data.Nat.BinaryRec (goal)
Goal:
b : Bool
n : Nat
rw : b.toNat < 2
⊢ bit b n / 2 = n
have H : LT.lt (α := Nat) 0 2
Tactic: rw [bit_val, Nat.add_comm, add_mul_div_left, div_eq_of_lt, Nat.zero_add]
-- Lean 4 proof step from Mathlib.Data.Nat.BinaryRec (goal)
Goal:
b : Bool
n : Nat
⊢ b.toNat < 2
have false : false.toNat < 2
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Nat.BinaryRec (goal)
Goal:
b : Bool
n : Nat
false : Bool.false.toNat < 2
⊢ b.toNat < 2
have true : true.toNat < 2
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Nat.BinaryRec (goal)
Goal:
b : Bool
n : Nat
⊢ bit b n % 2 = b.toNat
have false : bit false n % 2 = false.toNat
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Nat.BinaryRec (goal)
Goal:
b : Bool
n : Nat
false : bit Bool.false n % 2 = Bool.false.toNat
⊢ bit b n % 2 = b.toNat
have true : bit true n % 2 = true.toNat
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Nat.BinaryRec (goal)
Goal:
motive : Nat → Sort u
h : (b : Bool) → (n : Nat) → motive (bit b n)
b : Bool
n : Nat
⊢ bitCasesOn (motive := motive) (bit b n) h = h b n
have change : Eq.rec (motive :=
    fun (x : Sort u) (h : motive (bit ((bit b n).testBit 0) (HShiftRight.hShiftRight (β := Nat) (bit b n) 1)) = x) ↦ x)
    (h ((bit b n).testBit 0) (HShiftRight.hShiftRight (β := Nat) (bit b n) 1)) sorry =
  h b n
Tactic: change congrArg motive (bit b n).bit_testBit_zero_shiftRight_one ▸ h _ _ = h b n
-- Lean 4 proof step from Mathlib.Data.Nat.BinaryRec (goal)
Goal:
motive : Nat → Sort u
h : (b : Bool) → (n : Nat) → motive (bit b n)
b : Bool
n : Nat
⊢ Eq.rec (motive :=
      fun (x : Sort u) (h : motive (bit ((bit b n).testBit 0) (HShiftRight.hShiftRight (β := Nat) (bit b n) 1)) = x) ↦
      x) (h ((bit b n).testBit 0) (HShiftRight.hShiftRight (β := Nat) (bit b n) 1)) ⋯ =
    h b n
have generalize : ∀ (e : motive (bit ((bit b n).testBit 0) (HShiftRight.hShiftRight (β := Nat) (bit b n) 1)) = motive (bit b n)),
  Eq.rec (motive :=
      fun (x : Sort u) (h : motive (bit ((bit b n).testBit 0) (HShiftRight.hShiftRight (β := Nat) (bit b n) 1)) = x) ↦
      x) (h ((bit b n).testBit 0) (HShiftRight.hShiftRight (β := Nat) (bit b n) 1)) e =
    h b n
Tactic: generalize congrArg motive (bit b n).bit_testBit_zero_shiftRight_one = e