internlm/Lean-Github huggingface dataset:
Theorem: Nat.lsb_shiftLeft
Proof state before:
⊢ ∀ (n : Nat), 2 * Nat.lsb n = Nat.lsb (2 * n)
Tactic:
intro n
Proof state after:
n : Nat
⊢ 2 * Nat.lsb n = Nat.lsb (2 * n)
Theorem: Nat.lsb_shiftLeft
Proof state before:
n : Nat
⊢ 2 * Nat.lsb n = Nat.lsb (2 * n)
Tactic:
cases n
Proof state after:
case zero

⊢ 2 * Nat.lsb zero = Nat.lsb (2 * zero)

case succ
n✝ : Nat
⊢ 2 * Nat.lsb (succ n✝) = Nat.lsb (2 * succ n✝)
Theorem: Nat.lsb_shiftLeft
Proof state before:
⊢ 2 * Nat.lsb zero = Nat.lsb (2 * zero)
Tactic:
case zero => rfl
Proof state after:
no goals
Theorem: Nat.lsb_shiftLeft
Proof state before:
n : Nat
⊢ 2 * Nat.lsb (succ n) = Nat.lsb (2 * succ n)
Tactic:
case succ n =>
  unfold Nat.lsb
  have : 2 * n.succ - 1 = 2 * (n.succ - 1) + 1 := by
    simp only [Nat.mul_succ, Nat.succ_sub_one]
  have : ∀ (k l : Nat), (2*k) &&& (2*l + 1) = 2*k &&& 2*l := by
    intro k l
    have : ∀ m, 2*m &&& 1 = 0 := by intros; rw [Nat.land_one, Nat.mul_mod_right]
    have : 2*l + 1 = 2*l ^^^ 1 := Nat.add_eq_xor (this l)
    calc
      2*k &&& (2*l + 1)
        = 2*k &&& (2*l ^^^ 1) := by rw [‹2*l + 1 = 2*l ^^^ 1›]
      _ = (2*k &&& 2*l) ^^^ (2*k &&& 1) := Nat.and_xor ..
      _ = (2*k &&& 2*l) ^^^ 0 := by rw [‹∀ m, 2*m &&& 1 = 0›]
      _ = 2*k &&& 2 * l:= by rw [Nat.xor_zero]
  rw [‹2*n.succ - 1 = 2 * (n.succ - 1) + 1›, this]
  conv =>
    rhs; simp only [←Nat.shiftLeft_one]
    simp only [←Nat.land_shiftLeft, ←Nat.xor_shiftLeft]
Proof state after:
no goals
Theorem: Nat.lsb_shiftLeft
Proof state before:
this : ∀ (n : Nat), 2 * Nat.lsb n = Nat.lsb (2 * n)
⊢ ∀ (n k : Nat), Nat.lsb n <<< k = Nat.lsb (n <<< k)
Tactic:
intro n k
Proof state after:
this : ∀ (n : Nat), 2 * Nat.lsb n = Nat.lsb (2 * n)
n k : Nat
⊢ Nat.lsb n <<< k = Nat.lsb (n <<< k)
Theorem: Nat.lsb_shiftLeft
Proof state before:
this : ∀ (n : Nat), 2 * Nat.lsb n = Nat.lsb (2 * n)
n k : Nat
⊢ Nat.lsb n <<< k = Nat.lsb (n <<< k)
Tactic:
induction k generalizing n
Proof state after:
case zero
this : ∀ (n : Nat), 2 * Nat.lsb n = Nat.lsb (2 * n)
n : Nat
⊢ Nat.lsb n <<< zero = Nat.lsb (n <<< zero)

case succ
this : ∀ (n : Nat), 2 * Nat.lsb n = Nat.lsb (2 * n)
n✝ : Nat
n_ih✝ : ∀ (n : Nat), Nat.lsb n <<< n✝ = Nat.lsb (n <<< n✝)
n : Nat
⊢ Nat.lsb n <<< succ n✝ = Nat.lsb (n <<< succ n✝)
Theorem: Nat.lsb_shiftLeft
Proof state before:
this : ∀ (n : Nat), 2 * Nat.lsb n = Nat.lsb (2 * n)
n : Nat
⊢ Nat.lsb n <<< zero = Nat.lsb (n <<< zero)
Tactic:
case zero => rfl
Proof state after:
no goals
Theorem: Nat.lsb_shiftLeft
Proof state before:
this : ∀ (n : Nat), 2 * Nat.lsb n = Nat.lsb (2 * n)
k : Nat
h_ind : ∀ (n : Nat), Nat.lsb n <<< k = Nat.lsb (n <<< k)
n : Nat
⊢ Nat.lsb n <<< succ k = Nat.lsb (n <<< succ k)
Tactic:
case succ k h_ind =>
  simp only [Nat.succ_eq_add_one, ←Nat.shiftLeft_shiftLeft, h_ind]
  conv => change 2*(n <<< k).lsb = (2* (n <<< k)).lsb
  rw [this]
Proof state after:
no goals
Theorem: Nat.lsb_shiftLeft
Proof state before:
this : ∀ (n : Nat), 2 * Nat.lsb n = Nat.lsb (2 * n)
n : Nat
⊢ Nat.lsb n <<< zero = Nat.lsb (n <<< zero)
Tactic:
rfl
Proof state after:
no goals
Theorem: Nat.lsb_shiftLeft
Proof state before:
this : ∀ (n : Nat), 2 * Nat.lsb n = Nat.lsb (2 * n)
k : Nat
h_ind : ∀ (n : Nat), Nat.lsb n <<< k = Nat.lsb (n <<< k)
n : Nat
⊢ Nat.lsb n <<< succ k = Nat.lsb (n <<< succ k)
Tactic:
simp only [Nat.succ_eq_add_one, ←Nat.shiftLeft_shiftLeft, h_ind]
Proof state after:
this : ∀ (n : Nat), 2 * Nat.lsb n = Nat.lsb (2 * n)
k : Nat
h_ind : ∀ (n : Nat), Nat.lsb n <<< k = Nat.lsb (n <<< k)
n : Nat
⊢ Nat.lsb (n <<< k) <<< 1 = Nat.lsb (n <<< k <<< 1)
Theorem: Nat.lsb_shiftLeft
Proof state before:
this : ∀ (n : Nat), 2 * Nat.lsb n = Nat.lsb (2 * n)
k : Nat
h_ind : ∀ (n : Nat), Nat.lsb n <<< k = Nat.lsb (n <<< k)
n : Nat
⊢ Nat.lsb (n <<< k) <<< 1 = Nat.lsb (n <<< k <<< 1)
Tactic:
conv => change 2*(n <<< k).lsb = (2* (n <<< k)).lsb
Proof state after:
this : ∀ (n : Nat), 2 * Nat.lsb n = Nat.lsb (2 * n)
k : Nat
h_ind : ∀ (n : Nat), Nat.lsb n <<< k = Nat.lsb (n <<< k)
n : Nat
⊢ 2 * Nat.lsb (n <<< k) = Nat.lsb (2 * n <<< k)
Theorem: Nat.lsb_shiftLeft
Proof state before:
this : ∀ (n : Nat), 2 * Nat.lsb n = Nat.lsb (2 * n)
k : Nat
h_ind : ∀ (n : Nat), Nat.lsb n <<< k = Nat.lsb (n <<< k)
n : Nat
⊢ 2 * Nat.lsb (n <<< k) = Nat.lsb (2 * n <<< k)
Tactic:
rw [this]
Proof state after:
no goals
Theorem: Nat.lsb_shiftLeft
Proof state before:
⊢ 2 * Nat.lsb zero = Nat.lsb (2 * zero)
Tactic:
rfl
Proof state after:
no goals
Theorem: Nat.lsb_shiftLeft
Proof state before:
n : Nat
⊢ 2 * Nat.lsb (succ n) = Nat.lsb (2 * succ n)
Tactic:
unfold Nat.lsb
Proof state after:
n : Nat
⊢ 2 * (succ n ^^^ succ n &&& succ n - 1) = 2 * succ n ^^^ 2 * succ n &&& 2 * succ n - 1
Theorem: Nat.lsb_shiftLeft
Proof state before:
n : Nat
⊢ 2 * (succ n ^^^ succ n &&& succ n - 1) = 2 * succ n ^^^ 2 * succ n &&& 2 * succ n - 1
Tactic:
have : 2 * n.succ - 1 = 2 * (n.succ - 1) + 1 := by
  simp only [Nat.mul_succ, Nat.succ_sub_one]
Proof state after:
n : Nat
this : 2 * succ n - 1 = 2 * (succ n - 1) + 1
⊢ 2 * (succ n ^^^ succ n &&& succ n - 1) = 2 * succ n ^^^ 2 * succ n &&& 2 * succ n - 1
Theorem: Nat.lsb_shiftLeft
Proof state before:
n : Nat
this : 2 * succ n - 1 = 2 * (succ n - 1) + 1
⊢ 2 * (succ n ^^^ succ n &&& succ n - 1) = 2 * succ n ^^^ 2 * succ n &&& 2 * succ n - 1
Tactic:
have : ∀ (k l : Nat), (2*k) &&& (2*l + 1) = 2*k &&& 2*l := by
  intro k l
  have : ∀ m, 2*m &&& 1 = 0 := by intros; rw [Nat.land_one, Nat.mul_mod_right]
  have : 2*l + 1 = 2*l ^^^ 1 := Nat.add_eq_xor (this l)
  calc
    2*k &&& (2*l + 1)
      = 2*k &&& (2*l ^^^ 1) := by rw [‹2*l + 1 = 2*l ^^^ 1›]
    _ = (2*k &&& 2*l) ^^^ (2*k &&& 1) := Nat.and_xor ..
    _ = (2*k &&& 2*l) ^^^ 0 := by rw [‹∀ m, 2*m &&& 1 = 0›]
    _ = 2*k &&& 2 * l:= by rw [Nat.xor_zero]
Proof state after:
n : Nat
this✝ : 2 * succ n - 1 = 2 * (succ n - 1) + 1
this : ∀ (k l : Nat), 2 * k &&& 2 * l + 1 = 2 * k &&& 2 * l
⊢ 2 * (succ n ^^^ succ n &&& succ n - 1) = 2 * succ n ^^^ 2 * succ n &&& 2 * succ n - 1
Theorem: Nat.lsb_shiftLeft
Proof state before:
n : Nat
this✝ : 2 * succ n - 1 = 2 * (succ n - 1) + 1
this : ∀ (k l : Nat), 2 * k &&& 2 * l + 1 = 2 * k &&& 2 * l
⊢ 2 * (succ n ^^^ succ n &&& succ n - 1) = 2 * succ n ^^^ 2 * succ n &&& 2 * succ n - 1
Tactic:
rw [‹2*n.succ - 1 = 2 * (n.succ - 1) + 1›, this]
Proof state after:
n : Nat
this✝ : 2 * succ n - 1 = 2 * (succ n - 1) + 1
this : ∀ (k l : Nat), 2 * k &&& 2 * l + 1 = 2 * k &&& 2 * l
⊢ 2 * (succ n ^^^ succ n &&& succ n - 1) = 2 * succ n ^^^ 2 * succ n &&& 2 * (succ n - 1)
Theorem: Nat.lsb_shiftLeft
Proof state before:
n : Nat
this✝ : 2 * succ n - 1 = 2 * (succ n - 1) + 1
this : ∀ (k l : Nat), 2 * k &&& 2 * l + 1 = 2 * k &&& 2 * l
⊢ 2 * (succ n ^^^ succ n &&& succ n - 1) = 2 * succ n ^^^ 2 * succ n &&& 2 * (succ n - 1)
Tactic:
conv =>
  rhs; simp only [←Nat.shiftLeft_one]
  simp only [←Nat.land_shiftLeft, ←Nat.xor_shiftLeft]
Proof state after:
no goals
Theorem: Nat.lsb_shiftLeft
Proof state before:
n : Nat
⊢ 2 * succ n - 1 = 2 * (succ n - 1) + 1
Tactic:
simp only [Nat.mul_succ, Nat.succ_sub_one]
Proof state after:
no goals
Theorem: Nat.lsb_shiftLeft
Proof state before:
n : Nat
this : 2 * succ n - 1 = 2 * (succ n - 1) + 1
⊢ ∀ (k l : Nat), 2 * k &&& 2 * l + 1 = 2 * k &&& 2 * l
Tactic:
intro k l
Proof state after:
n : Nat
this : 2 * succ n - 1 = 2 * (succ n - 1) + 1
k l : Nat
⊢ 2 * k &&& 2 * l + 1 = 2 * k &&& 2 * l
Theorem: Nat.lsb_shiftLeft
Proof state before:
n : Nat
this : 2 * succ n - 1 = 2 * (succ n - 1) + 1
k l : Nat
⊢ 2 * k &&& 2 * l + 1 = 2 * k &&& 2 * l
Tactic:
have : ∀ m, 2*m &&& 1 = 0 := by intros; rw [Nat.land_one, Nat.mul_mod_right]
Proof state after:
n : Nat
this✝ : 2 * succ n - 1 = 2 * (succ n - 1) + 1
k l : Nat
this : ∀ (m : Nat), 2 * m &&& 1 = 0
⊢ 2 * k &&& 2 * l + 1 = 2 * k &&& 2 * l
Theorem: Nat.lsb_shiftLeft
Proof state before:
n : Nat
this✝ : 2 * succ n - 1 = 2 * (succ n - 1) + 1
k l : Nat
this : ∀ (m : Nat), 2 * m &&& 1 = 0
⊢ 2 * k &&& 2 * l + 1 = 2 * k &&& 2 * l
Tactic:
have : 2*l + 1 = 2*l ^^^ 1 := Nat.add_eq_xor (this l)
Proof state after:
n : Nat
this✝¹ : 2 * succ n - 1 = 2 * (succ n - 1) + 1
k l : Nat
this✝ : ∀ (m : Nat), 2 * m &&& 1 = 0
this : 2 * l + 1 = 2 * l ^^^ 1
⊢ 2 * k &&& 2 * l + 1 = 2 * k &&& 2 * l
Theorem: Nat.lsb_shiftLeft
Proof state before:
n : Nat
this✝¹ : 2 * succ n - 1 = 2 * (succ n - 1) + 1
k l : Nat
this✝ : ∀ (m : Nat), 2 * m &&& 1 = 0
this : 2 * l + 1 = 2 * l ^^^ 1
⊢ 2 * k &&& 2 * l + 1 = 2 * k &&& 2 * l
Tactic:
calc
  2*k &&& (2*l + 1)
    = 2*k &&& (2*l ^^^ 1) := by rw [‹2*l + 1 = 2*l ^^^ 1›]
  _ = (2*k &&& 2*l) ^^^ (2*k &&& 1) := Nat.and_xor ..
  _ = (2*k &&& 2*l) ^^^ 0 := by rw [‹∀ m, 2*m &&& 1 = 0›]
  _ = 2*k &&& 2 * l:= by rw [Nat.xor_zero]
Proof state after:
no goals
Theorem: Nat.lsb_shiftLeft
Proof state before:
n : Nat
this : 2 * succ n - 1 = 2 * (succ n - 1) + 1
k l : Nat
⊢ ∀ (m : Nat), 2 * m &&& 1 = 0
Tactic:
intros
Proof state after:
n : Nat
this : 2 * succ n - 1 = 2 * (succ n - 1) + 1
k l m✝ : Nat
⊢ 2 * m✝ &&& 1 = 0
Theorem: Nat.lsb_shiftLeft
Proof state before:
n : Nat
this : 2 * succ n - 1 = 2 * (succ n - 1) + 1
k l m✝ : Nat
⊢ 2 * m✝ &&& 1 = 0
Tactic:
rw [Nat.land_one, Nat.mul_mod_right]
Proof state after:
no goals
Theorem: Nat.lsb_shiftLeft
Proof state before:
n : Nat
this✝¹ : 2 * succ n - 1 = 2 * (succ n - 1) + 1
k l : Nat
this✝ : ∀ (m : Nat), 2 * m &&& 1 = 0
this : 2 * l + 1 = 2 * l ^^^ 1
⊢ 2 * k &&& 2 * l + 1 = 2 * k &&& (2 * l ^^^ 1)
Tactic:
rw [‹2*l + 1 = 2*l ^^^ 1›]
Proof state after:
no goals
Theorem: Nat.lsb_shiftLeft
Proof state before:
n : Nat
this✝¹ : 2 * succ n - 1 = 2 * (succ n - 1) + 1
k l : Nat
this✝ : ∀ (m : Nat), 2 * m &&& 1 = 0
this : 2 * l + 1 = 2 * l ^^^ 1
⊢ 2 * k &&& 2 * l ^^^ 2 * k &&& 1 = 2 * k &&& 2 * l ^^^ 0
Tactic:
rw [‹∀ m, 2*m &&& 1 = 0›]
Proof state after:
no goals
Theorem: Nat.lsb_shiftLeft
Proof state before:
n : Nat
this✝¹ : 2 * succ n - 1 = 2 * (succ n - 1) + 1
k l : Nat
this✝ : ∀ (m : Nat), 2 * m &&& 1 = 0
this : 2 * l + 1 = 2 * l ^^^ 1
⊢ 2 * k &&& 2 * l ^^^ 0 = 2 * k &&& 2 * l
Tactic:
rw [Nat.xor_zero]
Proof state after:
no goals
Theorem: Nat.lsb_of_even
Proof state before:
n : Nat
⊢ n % 2 = 0 → Nat.lsb n = Nat.lsb (n / 2) <<< 1
Tactic:
intro heven
Proof state after:
n : Nat
heven : n % 2 = 0
⊢ Nat.lsb n = Nat.lsb (n / 2) <<< 1
Theorem: Nat.lsb_of_even
Proof state before:
n : Nat
heven : n % 2 = 0
⊢ Nat.lsb n = Nat.lsb (n / 2) <<< 1
Tactic:
have hn : n = 0 + 2 * (n/2) := Eq.symm $ heven ▸ Nat.mod_add_div n 2
Proof state after:
n : Nat
heven : n % 2 = 0
hn : n = 0 + 2 * (n / 2)
⊢ Nat.lsb n = Nat.lsb (n / 2) <<< 1
Theorem: Nat.lsb_of_even
Proof state before:
n : Nat
heven : n % 2 = 0
hn : n = 0 + 2 * (n / 2)
⊢ Nat.lsb n = Nat.lsb (n / 2) <<< 1
Tactic:
rw [Nat.zero_add, ←Nat.shiftLeft_one] at hn
Proof state after:
n : Nat
heven : n % 2 = 0
hn : n = (n / 2) <<< 1
⊢ Nat.lsb n = Nat.lsb (n / 2) <<< 1
Theorem: Nat.lsb_of_even
Proof state before:
n : Nat
heven : n % 2 = 0
hn : n = (n / 2) <<< 1
⊢ Nat.lsb n = Nat.lsb (n / 2) <<< 1
Tactic:
conv => lhs; rw [hn, ←Nat.lsb_shiftLeft]
Proof state after:
no goals
Theorem: Nat.lsb_getBit_zero
Proof state before:
n : Nat
⊢ getBit (Nat.lsb n) 0 = getBit n 0
Tactic:
cases Nat.mod_two_eq_zero_or_one n
Proof state after:
case inl
n : Nat
h✝ : n % 2 = 0
⊢ getBit (Nat.lsb n) 0 = getBit n 0

case inr
n : Nat
h✝ : n % 2 = 1
⊢ getBit (Nat.lsb n) 0 = getBit n 0
Theorem: Nat.lsb_getBit_zero
Proof state before:
n : Nat
heven : n % 2 = 0
⊢ getBit (Nat.lsb n) 0 = getBit n 0
Tactic:
case inl heven =>
  rw [
    Nat.lsb_of_even heven,
    Nat.shiftLeft_getBit,
    decide_eq_false (p:=0≥1) (by decide),
    Bool.false_and,
  ]
  conv => rhs; dsimp [getBit]; rw [heven]; reduce
Proof state after:
no goals
Theorem: Nat.lsb_getBit_zero
Proof state before:
n : Nat
hodd : n % 2 = 1
⊢ getBit (Nat.lsb n) 0 = getBit n 0
Tactic:
case inr hodd =>
  rw [Nat.lsb_of_odd hodd]; dsimp [getBit]; rw [hodd]; decide
Proof state after:
no goals
Theorem: Nat.lsb_getBit_zero
Proof state before:
n : Nat
heven : n % 2 = 0
⊢ getBit (Nat.lsb n) 0 = getBit n 0
Tactic:
rw [
  Nat.lsb_of_even heven,
  Nat.shiftLeft_getBit,
  decide_eq_false (p:=0≥1) (by decide),
  Bool.false_and,
]
Proof state after:
n : Nat
heven : n % 2 = 0
⊢ false = getBit n 0
Theorem: Nat.lsb_getBit_zero
Proof state before:
n : Nat
heven : n % 2 = 0
⊢ false = getBit n 0
Tactic:
conv => rhs; dsimp [getBit]; rw [heven]; reduce
Proof state after:
no goals
Theorem: Nat.lsb_getBit_zero
Proof state before:
n : Nat
heven : n % 2 = 0
⊢ ¬0 ≥ 1
Tactic:
decide
Proof state after:
no goals
Theorem: Nat.lsb_getBit_zero
Proof state before:
n : Nat
hodd : n % 2 = 1
⊢ getBit (Nat.lsb n) 0 = getBit n 0
Tactic:
rw [Nat.lsb_of_odd hodd]
Proof state after:
n : Nat
hodd : n % 2 = 1
⊢ getBit 1 0 = getBit n 0
Theorem: Nat.lsb_getBit_zero
Proof state before:
n : Nat
hodd : n % 2 = 1
⊢ getBit 1 0 = getBit n 0
Tactic:
dsimp [getBit]
Proof state after:
n : Nat
hodd : n % 2 = 1
⊢ decide (1 % 2 = 1) = decide (n % 2 = 1)
Theorem: Nat.lsb_getBit_zero
Proof state before:
n : Nat
hodd : n % 2 = 1
⊢ decide (1 % 2 = 1) = decide (n % 2 = 1)
Tactic:
rw [hodd]
Proof state after:
n : Nat
hodd : n % 2 = 1
⊢ decide (1 % 2 = 1) = decide (1 = 1)
Theorem: Nat.lsb_getBit_zero
Proof state before:
n : Nat
hodd : n % 2 = 1
⊢ decide (1 % 2 = 1) = decide (1 = 1)
Tactic:
decide
Proof state after:
no goals
Theorem: Nat.lsb_getBit_iff
Proof state before:
n i : Nat
⊢ getBit (Nat.lsb n) i = true ↔ getBit n i = true ∧ ∀ (j : Nat), j < i → getBit n j = false
Tactic:
induction n using recBase2 generalizing i
Proof state after:
case zero
i : Nat
⊢ getBit (Nat.lsb 0) i = true ↔ getBit 0 i = true ∧ ∀ (j : Nat), j < i → getBit 0 j = false

case one
i : Nat
⊢ getBit (Nat.lsb 1) i = true ↔ getBit 1 i = true ∧ ∀ (j : Nat), j < i → getBit 1 j = false

case div2
n✝ : Nat
a✝ :
  ∀ {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
⊢ getBit (Nat.lsb (n✝ + 2)) i = true ↔ getBit (n✝ + 2) i = true ∧ ∀ (j : Nat), j < i → getBit (n✝ + 2) j = false
Theorem: Nat.lsb_getBit_iff
Proof state before:
i : Nat
⊢ getBit (Nat.lsb 0) i = true ↔ getBit 0 i = true ∧ ∀ (j : Nat), j < i → getBit 0 j = false
Tactic:
case zero => simp
Proof state after:
no goals
Theorem: Nat.lsb_getBit_iff
Proof state before:
i : Nat
⊢ getBit (Nat.lsb 1) i = true ↔ getBit 1 i = true ∧ ∀ (j : Nat), j < i → getBit 1 j = false
Tactic:
case one =>
  conv => lhs; rw [Nat.lsb_of_odd (n:=1) (by decide)]
  constructor
  show getBit 1 i = true → getBit 1 i = true ∧ ∀ j, j < i → getBit 1 j = false
  . intro h; apply And.intro h
    have : i = 0 := by
      conv at h => lhs; change getBit (2^0) i; rw [Nat.getBit_two_pow]
      exact Eq.symm (of_decide_eq_true h)
    cases this
    intro _ hj; cases hj
  show getBit 1 i = true ∧ (∀ j, j < i → getBit 1 j = false) → getBit 1 i
  . exact And.left
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
⊢ getBit (Nat.lsb (n + 2)) i = true ↔ getBit (n + 2) i = true ∧ ∀ (j : Nat), j < i → getBit (n + 2) j = false
Tactic:
case div2 n h_ind =>
  cases i
  case zero =>
    rw [Nat.lsb_getBit_zero]
    constructor
    show (n+2).getBit 0 = true → (n+2).getBit zero = true ∧ ∀ j, j < 0 → _ 
    . intro h; apply And.intro h ?_
      intro _ hj; cases hj
    show (n+2).getBit zero = true ∧ _ → (n+2).getBit zero = true 
    . exact And.left
  case succ i =>
    cases Nat.mod_two_eq_zero_or_one n
    case inl heven =>
      have := calc
        n+2 = (n/2)*2 + 2 := by rw [Nat.div_mul_cancel (Nat.dvd_of_mod_eq_zero heven)]
        _   = (n/2 + 1)*2 := Eq.symm $ Nat.add_mul ..
        _   = (n/2 + 1) <<< 1 := by rw [Nat.mul_comm, Nat.shiftLeft_one]
      simp only [
        this, ←Nat.lsb_shiftLeft,
        Nat.succ_eq_add_one,
        ←Nat.shiftRight_getBit,
        Nat.shiftLeft_shiftRight_self,
        Nat.shiftLeft_getBit
      ]
      suffices ∀ (m : Nat), (∀ j, j < i → m.getBit j = false) ↔ (∀ j, j < i.succ → (decide (j≥1) && m.getBit (j-1)) = false) by
        rw [←this]; exact h_ind
      intro m; constructor
      show (∀ j, j < i → m.getBit j = false) → (∀ j, j < i.succ → (decide (j≥ 1) && m.getBit (j-1)) = false)
      . intro h j hj
        cases j
        case zero =>
          rw [decide_eq_false (p:=zero ≥ 1) (by decide), Bool.false_and]
        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
      show (∀ j, j < i.succ → (decide (j ≥ 1) && m.getBit (j-1)) = false) → _
      . intro h j hj
        have h_succ := h j.succ (Nat.succ_lt_succ hj)
        conv at h_succ =>
          rw [decide_eq_true (p:=j.succ≥1) j.zero_lt_succ, Bool.true_and, Nat.succ_sub_one]
        exact h_succ
    case inr hodd =>
      have := calc
        (n+2) % 2
          = n%2 := Nat.add_mod_right ..
        _ = 1 := hodd
      conv =>
        lhs; lhs
        rw [Nat.lsb_of_odd this]; dsimp [getBit]
        change getBit 0 i; rw [zero_getBit]
      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
      rw [Nat.getBit, decide_eq_true ‹(n+2)%2 = 1›]
Proof state after:
no goals
Theorem: Nat.lsb_getBit_iff
Proof state before:
i : Nat
⊢ getBit (Nat.lsb 0) i = true ↔ getBit 0 i = true ∧ ∀ (j : Nat), j < i → getBit 0 j = false
Tactic:
simp
Proof state after:
no goals
Theorem: Nat.lsb_getBit_iff
Proof state before:
i : Nat
⊢ getBit (Nat.lsb 1) i = true ↔ getBit 1 i = true ∧ ∀ (j : Nat), j < i → getBit 1 j = false
Tactic:
conv => lhs; rw [Nat.lsb_of_odd (n:=1) (by decide)]
Proof state after:
i : Nat
⊢ getBit 1 i = true ↔ getBit 1 i = true ∧ ∀ (j : Nat), j < i → getBit 1 j = false
Theorem: Nat.lsb_getBit_iff
Proof state before:
i : Nat
⊢ getBit 1 i = true ↔ getBit 1 i = true ∧ ∀ (j : Nat), j < i → getBit 1 j = false
Tactic:
constructor
Proof state after:
case mp
i : Nat
⊢ getBit 1 i = true → getBit 1 i = true ∧ ∀ (j : Nat), j < i → getBit 1 j = false

case mpr
i : Nat
⊢ (getBit 1 i = true ∧ ∀ (j : Nat), j < i → getBit 1 j = false) → getBit 1 i = true
Theorem: Nat.lsb_getBit_iff
Proof state before:
case mp
i : Nat
⊢ getBit 1 i = true → getBit 1 i = true ∧ ∀ (j : Nat), j < i → getBit 1 j = false

case mpr
i : Nat
⊢ (getBit 1 i = true ∧ ∀ (j : Nat), j < i → getBit 1 j = false) → getBit 1 i = true
Tactic:
. intro h; apply And.intro h
  have : i = 0 := by
    conv at h => lhs; change getBit (2^0) i; rw [Nat.getBit_two_pow]
    exact Eq.symm (of_decide_eq_true h)
  cases this
  intro _ hj; cases hj
Proof state after:
case mpr
i : Nat
⊢ (getBit 1 i = true ∧ ∀ (j : Nat), j < i → getBit 1 j = false) → getBit 1 i = true
Theorem: Nat.lsb_getBit_iff
Proof state before:
case mpr
i : Nat
⊢ (getBit 1 i = true ∧ ∀ (j : Nat), j < i → getBit 1 j = false) → getBit 1 i = true
Tactic:
. exact And.left
Proof state after:
no goals
Theorem: Nat.lsb_getBit_iff
Proof state before:
i : Nat
⊢ 1 % 2 = 1
Tactic:
decide
Proof state after:
no goals
Theorem: Nat.lsb_getBit_iff
Proof state before:
case mp
i : Nat
⊢ getBit 1 i = true → getBit 1 i = true ∧ ∀ (j : Nat), j < i → getBit 1 j = false
Tactic:
intro h
Proof state after:
case mp
i : Nat
h : getBit 1 i = true
⊢ getBit 1 i = true ∧ ∀ (j : Nat), j < i → getBit 1 j = false
Theorem: Nat.lsb_getBit_iff
Proof state before:
case mp
i : Nat
h : getBit 1 i = true
⊢ getBit 1 i = true ∧ ∀ (j : Nat), j < i → getBit 1 j = false
Tactic:
apply And.intro h
Proof state after:
case mp
i : Nat
h : getBit 1 i = true
⊢ ∀ (j : Nat), j < i → getBit 1 j = false
Theorem: Nat.lsb_getBit_iff
Proof state before:
case mp
i : Nat
h : getBit 1 i = true
⊢ ∀ (j : Nat), j < i → getBit 1 j = false
Tactic:
have : i = 0 := by
  conv at h => lhs; change getBit (2^0) i; rw [Nat.getBit_two_pow]
  exact Eq.symm (of_decide_eq_true h)
Proof state after:
case mp
i : Nat
h : getBit 1 i = true
this : i = 0
⊢ ∀ (j : Nat), j < i → getBit 1 j = false
Theorem: Nat.lsb_getBit_iff
Proof state before:
case mp
i : Nat
h : getBit 1 i = true
this : i = 0
⊢ ∀ (j : Nat), j < i → getBit 1 j = false
Tactic:
cases this
Proof state after:
case mp.refl
h : getBit 1 0 = true
⊢ ∀ (j : Nat), j < 0 → getBit 1 j = false
Theorem: Nat.lsb_getBit_iff
Proof state before:
case mp.refl
h : getBit 1 0 = true
⊢ ∀ (j : Nat), j < 0 → getBit 1 j = false
Tactic:
intro _ hj
Proof state after:
case mp.refl
h : getBit 1 0 = true
j✝ : Nat
hj : j✝ < 0
⊢ getBit 1 j✝ = false
Theorem: Nat.lsb_getBit_iff
Proof state before:
case mp.refl
h : getBit 1 0 = true
j✝ : Nat
hj : j✝ < 0
⊢ getBit 1 j✝ = false
Tactic:
cases hj
Proof state after:
no goals
Theorem: Nat.lsb_getBit_iff
Proof state before:
i : Nat
h : getBit 1 i = true
⊢ i = 0
Tactic:
conv at h => lhs; change getBit (2^0) i; rw [Nat.getBit_two_pow]
Proof state after:
i : Nat
h : decide (0 = i) = true
⊢ i = 0
Theorem: Nat.lsb_getBit_iff
Proof state before:
i : Nat
h : decide (0 = i) = true
⊢ i = 0
Tactic:
exact Eq.symm (of_decide_eq_true h)
Proof state after:
no goals
Theorem: Nat.lsb_getBit_iff
Proof state before:
case mpr
i : Nat
⊢ (getBit 1 i = true ∧ ∀ (j : Nat), j < i → getBit 1 j = false) → getBit 1 i = true
Tactic:
exact And.left
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
⊢ getBit (Nat.lsb (n + 2)) i = true ↔ getBit (n + 2) i = true ∧ ∀ (j : Nat), j < i → getBit (n + 2) j = false
Tactic:
cases i
Proof state after:
case zero
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
⊢ getBit (Nat.lsb (n + 2)) zero = true ↔ getBit (n + 2) zero = true ∧ ∀ (j : Nat), j < zero → getBit (n + 2) j = false

case succ
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
n✝ : Nat
⊢ getBit (Nat.lsb (n + 2)) (succ n✝) = true ↔
    getBit (n + 2) (succ n✝) = true ∧ ∀ (j : Nat), j < succ n✝ → 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
⊢ getBit (Nat.lsb (n + 2)) zero = true ↔ getBit (n + 2) zero = true ∧ ∀ (j : Nat), j < zero → getBit (n + 2) j = false
Tactic:
case zero =>
  rw [Nat.lsb_getBit_zero]
  constructor
  show (n+2).getBit 0 = true → (n+2).getBit zero = true ∧ ∀ j, j < 0 → _ 
  . intro h; apply And.intro h ?_
    intro _ hj; cases hj
  show (n+2).getBit zero = true ∧ _ → (n+2).getBit zero = true 
  . exact And.left
Proof state after:
no goals