internlm/Lean-Github huggingface dataset:
Theorem: Nat.lsb_getBit_iff
Proof state before:
n : Nat
h_ind :
  ∀ {i : Nat},
    getBit (Nat.lsb (n / 2 + 1)) i = true ↔
      getBit (n / 2 + 1) i = true ∧ ∀ (j : Nat), j < i → getBit (n / 2 + 1) j = false
i : Nat
heven : n % 2 = 0
this : n + 2 = (n / 2 + 1) <<< 1
m : Nat
h : ∀ (j : Nat), j < i → getBit m j = false
hj : zero < succ i
⊢ (decide (zero ≥ 1) && getBit m (zero - 1)) = false
Tactic:
case zero =>
  rw [decide_eq_false (p:=zero ≥ 1) (by decide), Bool.false_and]
Proof state after:
no goals
Theorem: Nat.lsb_getBit_iff
Proof state before:
n : Nat
h_ind :
  ∀ {i : Nat},
    getBit (Nat.lsb (n / 2 + 1)) i = true ↔
      getBit (n / 2 + 1) i = true ∧ ∀ (j : Nat), j < i → getBit (n / 2 + 1) j = false
i : Nat
heven : n % 2 = 0
this : n + 2 = (n / 2 + 1) <<< 1
m : Nat
h : ∀ (j : Nat), j < i → getBit m j = false
j : Nat
hj : succ j < succ i
⊢ (decide (succ j ≥ 1) && getBit m (succ j - 1)) = false
Tactic:
case succ j =>
  have : j < i := lt_of_succ_lt_succ hj
  rw [decide_eq_true (p:=j.succ ≥ 1) j.zero_lt_succ, Bool.true_and, Nat.succ_sub_one]
  exact h j this
Proof state after:
no goals
Theorem: Nat.lsb_getBit_iff
Proof state before:
n : Nat
h_ind :
  ∀ {i : Nat},
    getBit (Nat.lsb (n / 2 + 1)) i = true ↔
      getBit (n / 2 + 1) i = true ∧ ∀ (j : Nat), j < i → getBit (n / 2 + 1) j = false
i : Nat
heven : n % 2 = 0
this : n + 2 = (n / 2 + 1) <<< 1
m : Nat
h : ∀ (j : Nat), j < i → getBit m j = false
hj : zero < succ i
⊢ (decide (zero ≥ 1) && getBit m (zero - 1)) = false
Tactic:
rw [decide_eq_false (p:=zero ≥ 1) (by decide), Bool.false_and]
Proof state after:
no goals
Theorem: Nat.lsb_getBit_iff
Proof state before:
n : Nat
h_ind :
  ∀ {i : Nat},
    getBit (Nat.lsb (n / 2 + 1)) i = true ↔
      getBit (n / 2 + 1) i = true ∧ ∀ (j : Nat), j < i → getBit (n / 2 + 1) j = false
i : Nat
heven : n % 2 = 0
this : n + 2 = (n / 2 + 1) <<< 1
m : Nat
h : ∀ (j : Nat), j < i → getBit m j = false
hj : zero < succ i
⊢ ¬zero ≥ 1
Tactic:
decide
Proof state after:
no goals
Theorem: Nat.lsb_getBit_iff
Proof state before:
n : Nat
h_ind :
  ∀ {i : Nat},
    getBit (Nat.lsb (n / 2 + 1)) i = true ↔
      getBit (n / 2 + 1) i = true ∧ ∀ (j : Nat), j < i → getBit (n / 2 + 1) j = false
i : Nat
heven : n % 2 = 0
this : n + 2 = (n / 2 + 1) <<< 1
m : Nat
h : ∀ (j : Nat), j < i → getBit m j = false
j : Nat
hj : succ j < succ i
⊢ (decide (succ j ≥ 1) && getBit m (succ j - 1)) = false
Tactic:
have : j < i := lt_of_succ_lt_succ hj
Proof state after:
n : Nat
h_ind :
  ∀ {i : Nat},
    getBit (Nat.lsb (n / 2 + 1)) i = true ↔
      getBit (n / 2 + 1) i = true ∧ ∀ (j : Nat), j < i → getBit (n / 2 + 1) j = false
i : Nat
heven : n % 2 = 0
this✝ : n + 2 = (n / 2 + 1) <<< 1
m : Nat
h : ∀ (j : Nat), j < i → getBit m j = false
j : Nat
hj : succ j < succ i
this : j < i
⊢ (decide (succ j ≥ 1) && getBit m (succ j - 1)) = false
Theorem: Nat.lsb_getBit_iff
Proof state before:
n : Nat
h_ind :
  ∀ {i : Nat},
    getBit (Nat.lsb (n / 2 + 1)) i = true ↔
      getBit (n / 2 + 1) i = true ∧ ∀ (j : Nat), j < i → getBit (n / 2 + 1) j = false
i : Nat
heven : n % 2 = 0
this✝ : n + 2 = (n / 2 + 1) <<< 1
m : Nat
h : ∀ (j : Nat), j < i → getBit m j = false
j : Nat
hj : succ j < succ i
this : j < i
⊢ (decide (succ j ≥ 1) && getBit m (succ j - 1)) = false
Tactic:
rw [decide_eq_true (p:=j.succ ≥ 1) j.zero_lt_succ, Bool.true_and, Nat.succ_sub_one]
Proof state after:
n : Nat
h_ind :
  ∀ {i : Nat},
    getBit (Nat.lsb (n / 2 + 1)) i = true ↔
      getBit (n / 2 + 1) i = true ∧ ∀ (j : Nat), j < i → getBit (n / 2 + 1) j = false
i : Nat
heven : n % 2 = 0
this✝ : n + 2 = (n / 2 + 1) <<< 1
m : Nat
h : ∀ (j : Nat), j < i → getBit m j = false
j : Nat
hj : succ j < succ i
this : j < i
⊢ getBit m j = false
Theorem: Nat.lsb_getBit_iff
Proof state before:
n : Nat
h_ind :
  ∀ {i : Nat},
    getBit (Nat.lsb (n / 2 + 1)) i = true ↔
      getBit (n / 2 + 1) i = true ∧ ∀ (j : Nat), j < i → getBit (n / 2 + 1) j = false
i : Nat
heven : n % 2 = 0
this✝ : n + 2 = (n / 2 + 1) <<< 1
m : Nat
h : ∀ (j : Nat), j < i → getBit m j = false
j : Nat
hj : succ j < succ i
this : j < i
⊢ getBit m j = false
Tactic:
exact h j this
Proof state after:
no goals
Theorem: Nat.lsb_getBit_iff
Proof state before:
case mpr
n : Nat
h_ind :
  ∀ {i : Nat},
    getBit (Nat.lsb (n / 2 + 1)) i = true ↔
      getBit (n / 2 + 1) i = true ∧ ∀ (j : Nat), j < i → getBit (n / 2 + 1) j = false
i : Nat
heven : n % 2 = 0
this : n + 2 = (n / 2 + 1) <<< 1
m : Nat
⊢ (∀ (j : Nat), j < succ i → (decide (j ≥ 1) && getBit m (j - 1)) = false) → ∀ (j : Nat), j < i → getBit m j = false
Tactic:
intro h j hj
Proof state after:
case mpr
n : Nat
h_ind :
  ∀ {i : Nat},
    getBit (Nat.lsb (n / 2 + 1)) i = true ↔
      getBit (n / 2 + 1) i = true ∧ ∀ (j : Nat), j < i → getBit (n / 2 + 1) j = false
i : Nat
heven : n % 2 = 0
this : n + 2 = (n / 2 + 1) <<< 1
m : Nat
h : ∀ (j : Nat), j < succ i → (decide (j ≥ 1) && getBit m (j - 1)) = false
j : Nat
hj : j < i
⊢ getBit m j = false
Theorem: Nat.lsb_getBit_iff
Proof state before:
case mpr
n : Nat
h_ind :
  ∀ {i : Nat},
    getBit (Nat.lsb (n / 2 + 1)) i = true ↔
      getBit (n / 2 + 1) i = true ∧ ∀ (j : Nat), j < i → getBit (n / 2 + 1) j = false
i : Nat
heven : n % 2 = 0
this : n + 2 = (n / 2 + 1) <<< 1
m : Nat
h : ∀ (j : Nat), j < succ i → (decide (j ≥ 1) && getBit m (j - 1)) = false
j : Nat
hj : j < i
⊢ getBit m j = false
Tactic:
have h_succ := h j.succ (Nat.succ_lt_succ hj)
Proof state after:
case mpr
n : Nat
h_ind :
  ∀ {i : Nat},
    getBit (Nat.lsb (n / 2 + 1)) i = true ↔
      getBit (n / 2 + 1) i = true ∧ ∀ (j : Nat), j < i → getBit (n / 2 + 1) j = false
i : Nat
heven : n % 2 = 0
this : n + 2 = (n / 2 + 1) <<< 1
m : Nat
h : ∀ (j : Nat), j < succ i → (decide (j ≥ 1) && getBit m (j - 1)) = false
j : Nat
hj : j < i
h_succ : (decide (succ j ≥ 1) && getBit m (succ j - 1)) = false
⊢ getBit m j = false
Theorem: Nat.lsb_getBit_iff
Proof state before:
case mpr
n : Nat
h_ind :
  ∀ {i : Nat},
    getBit (Nat.lsb (n / 2 + 1)) i = true ↔
      getBit (n / 2 + 1) i = true ∧ ∀ (j : Nat), j < i → getBit (n / 2 + 1) j = false
i : Nat
heven : n % 2 = 0
this : n + 2 = (n / 2 + 1) <<< 1
m : Nat
h : ∀ (j : Nat), j < succ i → (decide (j ≥ 1) && getBit m (j - 1)) = false
j : Nat
hj : j < i
h_succ : (decide (succ j ≥ 1) && getBit m (succ j - 1)) = false
⊢ getBit m j = false
Tactic:
conv at h_succ =>
  rw [decide_eq_true (p:=j.succ≥1) j.zero_lt_succ, Bool.true_and, Nat.succ_sub_one]
Proof state after:
case mpr
n : Nat
h_ind :
  ∀ {i : Nat},
    getBit (Nat.lsb (n / 2 + 1)) i = true ↔
      getBit (n / 2 + 1) i = true ∧ ∀ (j : Nat), j < i → getBit (n / 2 + 1) j = false
i : Nat
heven : n % 2 = 0
this : n + 2 = (n / 2 + 1) <<< 1
m : Nat
h : ∀ (j : Nat), j < succ i → (decide (j ≥ 1) && getBit m (j - 1)) = false
j : Nat
hj : j < i
h_succ : getBit m j = false
⊢ getBit m j = false
Theorem: Nat.lsb_getBit_iff
Proof state before:
case mpr
n : Nat
h_ind :
  ∀ {i : Nat},
    getBit (Nat.lsb (n / 2 + 1)) i = true ↔
      getBit (n / 2 + 1) i = true ∧ ∀ (j : Nat), j < i → getBit (n / 2 + 1) j = false
i : Nat
heven : n % 2 = 0
this : n + 2 = (n / 2 + 1) <<< 1
m : Nat
h : ∀ (j : Nat), j < succ i → (decide (j ≥ 1) && getBit m (j - 1)) = false
j : Nat
hj : j < i
h_succ : getBit m j = false
⊢ getBit m j = false
Tactic:
exact h_succ
Proof state after:
no goals
Theorem: Nat.lsb_getBit_iff
Proof state before:
n : Nat
h_ind :
  ∀ {i : Nat},
    getBit (Nat.lsb (n / 2 + 1)) i = true ↔
      getBit (n / 2 + 1) i = true ∧ ∀ (j : Nat), j < i → getBit (n / 2 + 1) j = false
i : Nat
hodd : n % 2 = 1
⊢ getBit (Nat.lsb (n + 2)) (succ i) = true ↔
    getBit (n + 2) (succ i) = true ∧ ∀ (j : Nat), j < succ i → getBit (n + 2) j = false
Tactic:
have := calc
  (n+2) % 2
    = n%2 := Nat.add_mod_right ..
  _ = 1 := hodd
Proof state after:
n : Nat
h_ind :
  ∀ {i : Nat},
    getBit (Nat.lsb (n / 2 + 1)) i = true ↔
      getBit (n / 2 + 1) i = true ∧ ∀ (j : Nat), j < i → getBit (n / 2 + 1) j = false
i : Nat
hodd : n % 2 = 1
this : (n + 2) % 2 = 1
⊢ getBit (Nat.lsb (n + 2)) (succ i) = true ↔
    getBit (n + 2) (succ i) = true ∧ ∀ (j : Nat), j < succ i → getBit (n + 2) j = false
Theorem: Nat.lsb_getBit_iff
Proof state before:
n : Nat
h_ind :
  ∀ {i : Nat},
    getBit (Nat.lsb (n / 2 + 1)) i = true ↔
      getBit (n / 2 + 1) i = true ∧ ∀ (j : Nat), j < i → getBit (n / 2 + 1) j = false
i : Nat
hodd : n % 2 = 1
this : (n + 2) % 2 = 1
⊢ getBit (Nat.lsb (n + 2)) (succ i) = true ↔
    getBit (n + 2) (succ i) = true ∧ ∀ (j : Nat), j < succ i → getBit (n + 2) j = false
Tactic:
conv =>
  lhs; lhs
  rw [Nat.lsb_of_odd this]; dsimp [getBit]
  change getBit 0 i; rw [zero_getBit]
Proof state after:
n : Nat
h_ind :
  ∀ {i : Nat},
    getBit (Nat.lsb (n / 2 + 1)) i = true ↔
      getBit (n / 2 + 1) i = true ∧ ∀ (j : Nat), j < i → getBit (n / 2 + 1) j = false
i : Nat
hodd : n % 2 = 1
this : (n + 2) % 2 = 1
⊢ false = true ↔ getBit (n + 2) (succ i) = true ∧ ∀ (j : Nat), j < succ i → getBit (n + 2) j = false
Theorem: Nat.lsb_getBit_iff
Proof state before:
n : Nat
h_ind :
  ∀ {i : Nat},
    getBit (Nat.lsb (n / 2 + 1)) i = true ↔
      getBit (n / 2 + 1) i = true ∧ ∀ (j : Nat), j < i → getBit (n / 2 + 1) j = false
i : Nat
hodd : n % 2 = 1
this : (n + 2) % 2 = 1
⊢ false = true ↔ getBit (n + 2) (succ i) = true ∧ ∀ (j : Nat), j < succ i → getBit (n + 2) j = false
Tactic:
suffices (n+2).getBit 0 = true by
  constructor
  . intro h; cases h
  . intro h; calc
      false = getBit (n+2) 0 := Eq.symm $ h.right 0 i.zero_lt_succ
      _     = true := this
Proof state after:
n : Nat
h_ind :
  ∀ {i : Nat},
    getBit (Nat.lsb (n / 2 + 1)) i = true ↔
      getBit (n / 2 + 1) i = true ∧ ∀ (j : Nat), j < i → getBit (n / 2 + 1) j = false
i : Nat
hodd : n % 2 = 1
this : (n + 2) % 2 = 1
⊢ getBit (n + 2) 0 = true
Theorem: Nat.lsb_getBit_iff
Proof state before:
n : Nat
h_ind :
  ∀ {i : Nat},
    getBit (Nat.lsb (n / 2 + 1)) i = true ↔
      getBit (n / 2 + 1) i = true ∧ ∀ (j : Nat), j < i → getBit (n / 2 + 1) j = false
i : Nat
hodd : n % 2 = 1
this : (n + 2) % 2 = 1
⊢ getBit (n + 2) 0 = true
Tactic:
rw [Nat.getBit, decide_eq_true ‹(n+2)%2 = 1›]
Proof state after:
no goals
Theorem: Nat.lsb_getBit_iff
Proof state before:
n : Nat
h_ind :
  ∀ {i : Nat},
    getBit (Nat.lsb (n / 2 + 1)) i = true ↔
      getBit (n / 2 + 1) i = true ∧ ∀ (j : Nat), j < i → getBit (n / 2 + 1) j = false
i : Nat
hodd : n % 2 = 1
this✝ : (n + 2) % 2 = 1
this : getBit (n + 2) 0 = true
⊢ false = true ↔ getBit (n + 2) (succ i) = true ∧ ∀ (j : Nat), j < succ i → getBit (n + 2) j = false
Tactic:
constructor
Proof state after:
case mp
n : Nat
h_ind :
  ∀ {i : Nat},
    getBit (Nat.lsb (n / 2 + 1)) i = true ↔
      getBit (n / 2 + 1) i = true ∧ ∀ (j : Nat), j < i → getBit (n / 2 + 1) j = false
i : Nat
hodd : n % 2 = 1
this✝ : (n + 2) % 2 = 1
this : getBit (n + 2) 0 = true
⊢ false = true → getBit (n + 2) (succ i) = true ∧ ∀ (j : Nat), j < succ i → getBit (n + 2) j = false

case mpr
n : Nat
h_ind :
  ∀ {i : Nat},
    getBit (Nat.lsb (n / 2 + 1)) i = true ↔
      getBit (n / 2 + 1) i = true ∧ ∀ (j : Nat), j < i → getBit (n / 2 + 1) j = false
i : Nat
hodd : n % 2 = 1
this✝ : (n + 2) % 2 = 1
this : getBit (n + 2) 0 = true
⊢ (getBit (n + 2) (succ i) = true ∧ ∀ (j : Nat), j < succ i → getBit (n + 2) j = false) → false = true
Theorem: Nat.lsb_getBit_iff
Proof state before:
case mp
n : Nat
h_ind :
  ∀ {i : Nat},
    getBit (Nat.lsb (n / 2 + 1)) i = true ↔
      getBit (n / 2 + 1) i = true ∧ ∀ (j : Nat), j < i → getBit (n / 2 + 1) j = false
i : Nat
hodd : n % 2 = 1
this✝ : (n + 2) % 2 = 1
this : getBit (n + 2) 0 = true
⊢ false = true → getBit (n + 2) (succ i) = true ∧ ∀ (j : Nat), j < succ i → getBit (n + 2) j = false

case mpr
n : Nat
h_ind :
  ∀ {i : Nat},
    getBit (Nat.lsb (n / 2 + 1)) i = true ↔
      getBit (n / 2 + 1) i = true ∧ ∀ (j : Nat), j < i → getBit (n / 2 + 1) j = false
i : Nat
hodd : n % 2 = 1
this✝ : (n + 2) % 2 = 1
this : getBit (n + 2) 0 = true
⊢ (getBit (n + 2) (succ i) = true ∧ ∀ (j : Nat), j < succ i → getBit (n + 2) j = false) → false = true
Tactic:
. intro h; cases h
Proof state after:
case mpr
n : Nat
h_ind :
  ∀ {i : Nat},
    getBit (Nat.lsb (n / 2 + 1)) i = true ↔
      getBit (n / 2 + 1) i = true ∧ ∀ (j : Nat), j < i → getBit (n / 2 + 1) j = false
i : Nat
hodd : n % 2 = 1
this✝ : (n + 2) % 2 = 1
this : getBit (n + 2) 0 = true
⊢ (getBit (n + 2) (succ i) = true ∧ ∀ (j : Nat), j < succ i → getBit (n + 2) j = false) → false = true
Theorem: Nat.lsb_getBit_iff
Proof state before:
case mpr
n : Nat
h_ind :
  ∀ {i : Nat},
    getBit (Nat.lsb (n / 2 + 1)) i = true ↔
      getBit (n / 2 + 1) i = true ∧ ∀ (j : Nat), j < i → getBit (n / 2 + 1) j = false
i : Nat
hodd : n % 2 = 1
this✝ : (n + 2) % 2 = 1
this : getBit (n + 2) 0 = true
⊢ (getBit (n + 2) (succ i) = true ∧ ∀ (j : Nat), j < succ i → getBit (n + 2) j = false) → false = true
Tactic:
. intro h; calc
    false = getBit (n+2) 0 := Eq.symm $ h.right 0 i.zero_lt_succ
    _     = true := this
Proof state after:
no goals
Theorem: Nat.lsb_getBit_iff
Proof state before:
case mp
n : Nat
h_ind :
  ∀ {i : Nat},
    getBit (Nat.lsb (n / 2 + 1)) i = true ↔
      getBit (n / 2 + 1) i = true ∧ ∀ (j : Nat), j < i → getBit (n / 2 + 1) j = false
i : Nat
hodd : n % 2 = 1
this✝ : (n + 2) % 2 = 1
this : getBit (n + 2) 0 = true
⊢ false = true → getBit (n + 2) (succ i) = true ∧ ∀ (j : Nat), j < succ i → getBit (n + 2) j = false
Tactic:
intro h
Proof state after:
case mp
n : Nat
h_ind :
  ∀ {i : Nat},
    getBit (Nat.lsb (n / 2 + 1)) i = true ↔
      getBit (n / 2 + 1) i = true ∧ ∀ (j : Nat), j < i → getBit (n / 2 + 1) j = false
i : Nat
hodd : n % 2 = 1
this✝ : (n + 2) % 2 = 1
this : getBit (n + 2) 0 = true
h : false = true
⊢ getBit (n + 2) (succ i) = true ∧ ∀ (j : Nat), j < succ i → getBit (n + 2) j = false
Theorem: Nat.lsb_getBit_iff
Proof state before:
case mp
n : Nat
h_ind :
  ∀ {i : Nat},
    getBit (Nat.lsb (n / 2 + 1)) i = true ↔
      getBit (n / 2 + 1) i = true ∧ ∀ (j : Nat), j < i → getBit (n / 2 + 1) j = false
i : Nat
hodd : n % 2 = 1
this✝ : (n + 2) % 2 = 1
this : getBit (n + 2) 0 = true
h : false = true
⊢ getBit (n + 2) (succ i) = true ∧ ∀ (j : Nat), j < succ i → getBit (n + 2) j = false
Tactic:
cases h
Proof state after:
no goals
Theorem: Nat.lsb_getBit_iff
Proof state before:
case mpr
n : Nat
h_ind :
  ∀ {i : Nat},
    getBit (Nat.lsb (n / 2 + 1)) i = true ↔
      getBit (n / 2 + 1) i = true ∧ ∀ (j : Nat), j < i → getBit (n / 2 + 1) j = false
i : Nat
hodd : n % 2 = 1
this✝ : (n + 2) % 2 = 1
this : getBit (n + 2) 0 = true
⊢ (getBit (n + 2) (succ i) = true ∧ ∀ (j : Nat), j < succ i → getBit (n + 2) j = false) → false = true
Tactic:
intro h
Proof state after:
case mpr
n : Nat
h_ind :
  ∀ {i : Nat},
    getBit (Nat.lsb (n / 2 + 1)) i = true ↔
      getBit (n / 2 + 1) i = true ∧ ∀ (j : Nat), j < i → getBit (n / 2 + 1) j = false
i : Nat
hodd : n % 2 = 1
this✝ : (n + 2) % 2 = 1
this : getBit (n + 2) 0 = true
h : getBit (n + 2) (succ i) = true ∧ ∀ (j : Nat), j < succ i → getBit (n + 2) j = false
⊢ false = true
Theorem: Nat.lsb_getBit_iff
Proof state before:
case mpr
n : Nat
h_ind :
  ∀ {i : Nat},
    getBit (Nat.lsb (n / 2 + 1)) i = true ↔
      getBit (n / 2 + 1) i = true ∧ ∀ (j : Nat), j < i → getBit (n / 2 + 1) j = false
i : Nat
hodd : n % 2 = 1
this✝ : (n + 2) % 2 = 1
this : getBit (n + 2) 0 = true
h : getBit (n + 2) (succ i) = true ∧ ∀ (j : Nat), j < succ i → getBit (n + 2) j = false
⊢ false = true
Tactic:
calc
false = getBit (n+2) 0 := Eq.symm $ h.right 0 i.zero_lt_succ
_     = true := this
Proof state after:
no goals
Theorem: Nat.eq_zero_of_lsb_eq_zero
Proof state before:
n : Nat
⊢ Nat.lsb n = 0 → n = 0
Tactic:
intro h
Proof state after:
n : Nat
h : Nat.lsb n = 0
⊢ n = 0
Theorem: Nat.eq_zero_of_lsb_eq_zero
Proof state before:
n : Nat
h : Nat.lsb n = 0
⊢ n = 0
Tactic:
apply bitext
Proof state after:
case a
n : Nat
h : Nat.lsb n = 0
⊢ ∀ (i : Nat), getBit n i = getBit 0 i
Theorem: Nat.eq_zero_of_lsb_eq_zero
Proof state before:
case a
n : Nat
h : Nat.lsb n = 0
⊢ ∀ (i : Nat), getBit n i = getBit 0 i
Tactic:
intro i
Proof state after:
case a
n : Nat
h : Nat.lsb n = 0
i : Nat
⊢ getBit n i = getBit 0 i
Theorem: Nat.eq_zero_of_lsb_eq_zero
Proof state before:
case a
n : Nat
h : Nat.lsb n = 0
i : Nat
⊢ getBit n i = getBit 0 i
Tactic:
rw [Nat.zero_getBit]
Proof state after:
case a
n : Nat
h : Nat.lsb n = 0
i : Nat
⊢ getBit n i = false
Theorem: Nat.eq_zero_of_lsb_eq_zero
Proof state before:
case a
n : Nat
h : Nat.lsb n = 0
i : Nat
⊢ getBit n i = false
Tactic:
induction i using Nat.recComplete
Proof state after:
case a.ind
n : Nat
h : Nat.lsb n = 0
n✝ : Nat
a✝ : ∀ (k : Nat), k < n✝ → getBit n k = false
⊢ getBit n n✝ = false
Theorem: Nat.eq_zero_of_lsb_eq_zero
Proof state before:
n : Nat
h : Nat.lsb n = 0
i : Nat
h_ind : ∀ (k : Nat), k < i → getBit n k = false
⊢ getBit n i = false
Tactic:
case a.ind i h_ind =>
cases hni : n.getBit i
case false => rfl
case true =>
  calc
    true = n.lsb.getBit i := Eq.symm $ n.lsb_getBit_iff.mpr ⟨hni, h_ind⟩
    _    = Nat.getBit 0 i := by rw [h]
    _    = false          := Nat.zero_getBit i
Proof state after:
no goals
Theorem: Nat.eq_zero_of_lsb_eq_zero
Proof state before:
n : Nat
h : Nat.lsb n = 0
i : Nat
h_ind : ∀ (k : Nat), k < i → getBit n k = false
⊢ getBit n i = false
Tactic:
cases hni : n.getBit i
Proof state after:
case false
n : Nat
h : Nat.lsb n = 0
i : Nat
h_ind : ∀ (k : Nat), k < i → getBit n k = false
hni : getBit n i = false
⊢ false = false

case true
n : Nat
h : Nat.lsb n = 0
i : Nat
h_ind : ∀ (k : Nat), k < i → getBit n k = false
hni : getBit n i = true
⊢ true = false
Theorem: Nat.eq_zero_of_lsb_eq_zero
Proof state before:
n : Nat
h : Nat.lsb n = 0
i : Nat
h_ind : ∀ (k : Nat), k < i → getBit n k = false
hni : getBit n i = false
⊢ false = false
Tactic:
case false => rfl
Proof state after:
no goals
Theorem: Nat.eq_zero_of_lsb_eq_zero
Proof state before:
n : Nat
h : Nat.lsb n = 0
i : Nat
h_ind : ∀ (k : Nat), k < i → getBit n k = false
hni : getBit n i = true
⊢ true = false
Tactic:
case true =>
  calc
    true = n.lsb.getBit i := Eq.symm $ n.lsb_getBit_iff.mpr ⟨hni, h_ind⟩
    _    = Nat.getBit 0 i := by rw [h]
    _    = false          := Nat.zero_getBit i
Proof state after:
no goals
Theorem: Nat.eq_zero_of_lsb_eq_zero
Proof state before:
n : Nat
h : Nat.lsb n = 0
i : Nat
h_ind : ∀ (k : Nat), k < i → getBit n k = false
hni : getBit n i = false
⊢ false = false
Tactic:
rfl
Proof state after:
no goals
Theorem: Nat.eq_zero_of_lsb_eq_zero
Proof state before:
n : Nat
h : Nat.lsb n = 0
i : Nat
h_ind : ∀ (k : Nat), k < i → getBit n k = false
hni : getBit n i = true
⊢ true = false
Tactic:
calc
  true = n.lsb.getBit i := Eq.symm $ n.lsb_getBit_iff.mpr ⟨hni, h_ind⟩
  _    = Nat.getBit 0 i := by rw [h]
  _    = false          := Nat.zero_getBit i
Proof state after:
no goals
Theorem: Nat.eq_zero_of_lsb_eq_zero
Proof state before:
n : Nat
h : Nat.lsb n = 0
i : Nat
h_ind : ∀ (k : Nat), k < i → getBit n k = false
hni : getBit n i = true
⊢ getBit (Nat.lsb n) i = getBit 0 i
Tactic:
rw [h]
Proof state after:
no goals
Theorem: Nat.or_one_eq_add_one
Proof state before:
n : Nat
⊢ n % 2 = 0 → n ||| 1 = n + 1
Tactic:
intro hn
Proof state after:
n : Nat
hn : n % 2 = 0
⊢ n ||| 1 = n + 1
Theorem: Nat.or_one_eq_add_one
Proof state before:
n : Nat
hn : n % 2 = 0
⊢ n ||| 1 = n + 1
Tactic:
have hn2_neq_1: n % 2 ≠ 1 := λ h => absurd (Eq.trans hn.symm h) Nat.zero_ne_one
Proof state after:
n : Nat
hn : n % 2 = 0
hn2_neq_1 : n % 2 ≠ 1
⊢ n ||| 1 = n + 1
Theorem: Nat.or_one_eq_add_one
Proof state before:
n : Nat
hn : n % 2 = 0
hn2_neq_1 : n % 2 ≠ 1
⊢ n ||| 1 = n + 1
Tactic:
conv =>
  lhs;
  dsimp [HOr.hOr, OrOp.or, Nat.lor]; unfold bitwise
  rw [if_neg Nat.one_ne_zero, Bool.false_or, if_pos rfl]
  zeta
  rw [decide_eq_false hn2_neq_1, Bool.false_or, decide_eq_true, if_pos rfl]
  change if n = 0 then 1 else ((n/2) ||| 0) + ((n/2) ||| 0) + 1
  rw [Nat.lor_zero, ←Nat.mul_two]
  rw [Nat.div_mul_cancel ((Nat.dvd_iff_mod_eq_zero 2 n).mpr hn)]
Proof state after:
n : Nat
hn : n % 2 = 0
hn2_neq_1 : n % 2 ≠ 1
⊢ (if n = 0 then 1 else n + 1) = n + 1
Theorem: Nat.or_one_eq_add_one
Proof state before:
n : Nat
hn : n % 2 = 0
hn2_neq_1 : n % 2 ≠ 1
⊢ (if n = 0 then 1 else n + 1) = n + 1
Tactic:
by_cases n = 0
Proof state after:
case pos
n : Nat
hn : n % 2 = 0
hn2_neq_1 : n % 2 ≠ 1
h✝ : n = 0
⊢ (if n = 0 then 1 else n + 1) = n + 1

case neg
n : Nat
hn : n % 2 = 0
hn2_neq_1 : n % 2 ≠ 1
h✝ : ¬n = 0
⊢ (if n = 0 then 1 else n + 1) = n + 1
Theorem: Nat.or_one_eq_add_one
Proof state before:
n : Nat
hn : n % 2 = 0
hn2_neq_1 : n % 2 ≠ 1
h : n = 0
⊢ (if n = 0 then 1 else n + 1) = n + 1
Tactic:
case pos h => cases h; rw [if_pos rfl]
Proof state after:
no goals
Theorem: Nat.or_one_eq_add_one
Proof state before:
n : Nat
hn : n % 2 = 0
hn2_neq_1 : n % 2 ≠ 1
h : ¬n = 0
⊢ (if n = 0 then 1 else n + 1) = n + 1
Tactic:
case neg h => rw [if_neg h]
Proof state after:
no goals
Theorem: Nat.or_one_eq_add_one
Proof state before:
n : Nat
hn : n % 2 = 0
hn2_neq_1 : n % 2 ≠ 1
h : n = 0
⊢ (if n = 0 then 1 else n + 1) = n + 1
Tactic:
cases h
Proof state after:
case refl
hn : 0 % 2 = 0
hn2_neq_1 : 0 % 2 ≠ 1
⊢ (if 0 = 0 then 1 else 0 + 1) = 0 + 1
Theorem: Nat.or_one_eq_add_one
Proof state before:
case refl
hn : 0 % 2 = 0
hn2_neq_1 : 0 % 2 ≠ 1
⊢ (if 0 = 0 then 1 else 0 + 1) = 0 + 1
Tactic:
rw [if_pos rfl]
Proof state after:
no goals
Theorem: Nat.or_one_eq_add_one
Proof state before:
n : Nat
hn : n % 2 = 0
hn2_neq_1 : n % 2 ≠ 1
h : ¬n = 0
⊢ (if n = 0 then 1 else n + 1) = n + 1
Tactic:
rw [if_neg h]
Proof state after:
no goals
Theorem: Nat.shiftLeft_one_or_one
Proof state before:
n : Nat
⊢ n <<< 1 ||| 1 = 2 * n + 1
Tactic:
rw [shiftLeft_one]
Proof state after:
n : Nat
⊢ 2 * n ||| 1 = 2 * n + 1
Theorem: Nat.shiftLeft_one_or_one
Proof state before:
n : Nat
⊢ 2 * n ||| 1 = 2 * n + 1
Tactic:
apply or_one_eq_add_one
Proof state after:
case a
n : Nat
⊢ 2 * n % 2 = 0
Theorem: Nat.shiftLeft_one_or_one
Proof state before:
case a
n : Nat
⊢ 2 * n % 2 = 0
Tactic:
exact Nat.mul_mod_right 2 n
Proof state after:
no goals
Theorem: Nat.log2'_eq
Proof state before:
n : Nat
⊢ log2' n = log2 n
Tactic:
unfold log2'
Proof state after:
n : Nat
⊢ recBase2 0 0 (fun x x_1 => x_1 + 1) n = log2 n
Theorem: Nat.log2'_eq
Proof state before:
n : Nat
⊢ recBase2 0 0 (fun x x_1 => x_1 + 1) n = log2 n
Tactic:
induction n using recBase2
Proof state after:
case zero

⊢ recBase2 0 0 (fun x x_1 => x_1 + 1) 0 = log2 0

case one

⊢ recBase2 0 0 (fun x x_1 => x_1 + 1) 1 = log2 1

case div2
n✝ : Nat
a✝ : recBase2 0 0 (fun x x_1 => x_1 + 1) (n✝ / 2 + 1) = log2 (n✝ / 2 + 1)
⊢ recBase2 0 0 (fun x x_1 => x_1 + 1) (n✝ + 2) = log2 (n✝ + 2)
Theorem: Nat.log2'_eq
Proof state before:
⊢ recBase2 0 0 (fun x x_1 => x_1 + 1) 0 = log2 0
Tactic:
case zero => rfl
Proof state after:
no goals
Theorem: Nat.log2'_eq
Proof state before:
⊢ recBase2 0 0 (fun x x_1 => x_1 + 1) 1 = log2 1
Tactic:
case one => rfl
Proof state after:
no goals
Theorem: Nat.log2'_eq
Proof state before:
n : Nat
h_ind : recBase2 0 0 (fun x x_1 => x_1 + 1) (n / 2 + 1) = log2 (n / 2 + 1)
⊢ recBase2 0 0 (fun x x_1 => x_1 + 1) (n + 2) = log2 (n + 2)
Tactic:
case div2 n h_ind =>
  rw [recBase2_div2, h_ind]
  conv =>
    rhs; unfold log2; rw [if_pos (Nat.le_add_left 2 n), Nat.add_div_right n (Nat.zero_lt_succ 1)]
Proof state after:
no goals
Theorem: Nat.log2'_eq
Proof state before:
⊢ recBase2 0 0 (fun x x_1 => x_1 + 1) 0 = log2 0
Tactic:
rfl
Proof state after:
no goals
Theorem: Nat.log2'_eq
Proof state before:
⊢ recBase2 0 0 (fun x x_1 => x_1 + 1) 1 = log2 1
Tactic:
rfl
Proof state after:
no goals
Theorem: Nat.log2'_eq
Proof state before:
n : Nat
h_ind : recBase2 0 0 (fun x x_1 => x_1 + 1) (n / 2 + 1) = log2 (n / 2 + 1)
⊢ recBase2 0 0 (fun x x_1 => x_1 + 1) (n + 2) = log2 (n + 2)
Tactic:
rw [recBase2_div2, h_ind]
Proof state after:
n : Nat
h_ind : recBase2 0 0 (fun x x_1 => x_1 + 1) (n / 2 + 1) = log2 (n / 2 + 1)
⊢ log2 (n / 2 + 1) + 1 = log2 (n + 2)
Theorem: Nat.log2'_eq
Proof state before:
n : Nat
h_ind : recBase2 0 0 (fun x x_1 => x_1 + 1) (n / 2 + 1) = log2 (n / 2 + 1)
⊢ log2 (n / 2 + 1) + 1 = log2 (n + 2)
Tactic:
conv =>
  rhs; unfold log2; rw [if_pos (Nat.le_add_left 2 n), Nat.add_div_right n (Nat.zero_lt_succ 1)]
Proof state after:
no goals
Theorem: Nat.log2'_div2
Proof state before:
n : Nat
⊢ log2' (n + 2) = log2' (n / 2 + 1) + 1
Tactic:
conv => lhs; unfold log2'; rw [recBase2_div2]
Proof state after:
no goals