Theorem: Nat.lsb_getBit_iff (Algdata/Data/Nat/Bits.lean)

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
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

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
State after:
no goals

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
State after:
no goals

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›]
State after:
no goals

State before:
i : Nat
⊢ getBit (Nat.lsb 0) i = true ↔ getBit 0 i = true ∧ ∀ (j : Nat), j < i → getBit 0 j = false
Tactic:
simp
State after:
no goals

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)]
State after:
i : Nat
⊢ getBit 1 i = true ↔ getBit 1 i = true ∧ ∀ (j : Nat), j < i → getBit 1 j = false

State before:
i : Nat
⊢ getBit 1 i = true ↔ getBit 1 i = true ∧ ∀ (j : Nat), j < i → getBit 1 j = false
Tactic:
constructor
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

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
State after:
case mpr
i : Nat
⊢ (getBit 1 i = true ∧ ∀ (j : Nat), j < i → getBit 1 j = false) → getBit 1 i = true

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
State after:
no goals

State before:
i : Nat
⊢ 1 % 2 = 1
Tactic:
decide
State after:
no goals

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
State after:
case mp
i : Nat
h : getBit 1 i = true
⊢ getBit 1 i = true ∧ ∀ (j : Nat), j < i → getBit 1 j = false

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
State after:
case mp
i : Nat
h : getBit 1 i = true
⊢ ∀ (j : Nat), j < i → getBit 1 j = false

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)
State after:
case mp
i : Nat
h : getBit 1 i = true
this : i = 0
⊢ ∀ (j : Nat), j < i → getBit 1 j = false

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
State after:
case mp.refl
h : getBit 1 0 = true
⊢ ∀ (j : Nat), j < 0 → getBit 1 j = false

State before:
case mp.refl
h : getBit 1 0 = true
⊢ ∀ (j : Nat), j < 0 → getBit 1 j = false
Tactic:
intro _ hj
State after:
case mp.refl
h : getBit 1 0 = true
j✝ : Nat
hj : j✝ < 0
⊢ getBit 1 j✝ = false

State before:
case mp.refl
h : getBit 1 0 = true
j✝ : Nat
hj : j✝ < 0
⊢ getBit 1 j✝ = false
Tactic:
cases hj
State after:
no goals

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]
State after:
i : Nat
h : decide (0 = i) = true
⊢ i = 0

State before:
i : Nat
h : decide (0 = i) = true
⊢ i = 0
Tactic:
exact Eq.symm (of_decide_eq_true h)
State after:
no goals

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
State after:
no goals

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
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

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
State after:
no goals

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)) (succ i) = true ↔
    getBit (n + 2) (succ i) = true ∧ ∀ (j : Nat), j < succ i → getBit (n + 2) j = false
Tactic:
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›]
State after:
no goals

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:
rw [Nat.lsb_getBit_zero]
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
⊢ getBit (n + 2) 0 = true ↔ getBit (n + 2) zero = true ∧ ∀ (j : Nat), j < zero → getBit (n + 2) j = false

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 (n + 2) 0 = true ↔ getBit (n + 2) zero = true ∧ ∀ (j : Nat), j < zero → getBit (n + 2) j = false
Tactic:
constructor
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
⊢ getBit (n + 2) 0 = true → getBit (n + 2) zero = true ∧ ∀ (j : Nat), j < zero → 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
⊢ (getBit (n + 2) zero = true ∧ ∀ (j : Nat), j < zero → getBit (n + 2) j = false) → getBit (n + 2) 0 = true

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
⊢ getBit (n + 2) 0 = true → getBit (n + 2) zero = true ∧ ∀ (j : Nat), j < zero → 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
⊢ (getBit (n + 2) zero = true ∧ ∀ (j : Nat), j < zero → getBit (n + 2) j = false) → getBit (n + 2) 0 = true
Tactic:
show (n+2).getBit 0 = true → (n+2).getBit zero = true ∧ ∀ j, j < 0 → _
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
⊢ getBit (n + 2) 0 = true → getBit (n + 2) zero = true ∧ ∀ (j : Nat), j < 0 → 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
⊢ (getBit (n + 2) zero = true ∧ ∀ (j : Nat), j < zero → getBit (n + 2) j = false) → getBit (n + 2) 0 = true

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
⊢ getBit (n + 2) 0 = true → getBit (n + 2) zero = true ∧ ∀ (j : Nat), j < 0 → 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
⊢ (getBit (n + 2) zero = true ∧ ∀ (j : Nat), j < zero → getBit (n + 2) j = false) → getBit (n + 2) 0 = true
Tactic:
. intro h; apply And.intro h ?_
  intro _ hj; cases hj
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
⊢ (getBit (n + 2) zero = true ∧ ∀ (j : Nat), j < zero → getBit (n + 2) j = false) → getBit (n + 2) 0 = true

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
⊢ (getBit (n + 2) zero = true ∧ ∀ (j : Nat), j < zero → getBit (n + 2) j = false) → getBit (n + 2) 0 = true
Tactic:
show (n+2).getBit zero = true ∧ _ → (n+2).getBit zero = true
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
⊢ (getBit (n + 2) zero = true ∧ ∀ (j : Nat), j < zero → getBit (n + 2) j = false) → getBit (n + 2) zero = true

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
⊢ (getBit (n + 2) zero = true ∧ ∀ (j : Nat), j < zero → getBit (n + 2) j = false) → getBit (n + 2) zero = true
Tactic:
. exact And.left
State after:
no goals

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
⊢ getBit (n + 2) 0 = true → getBit (n + 2) zero = true ∧ ∀ (j : Nat), j < 0 → getBit (n + 2) j = false
Tactic:
intro h
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
h : getBit (n + 2) 0 = true
⊢ getBit (n + 2) zero = true ∧ ∀ (j : Nat), j < 0 → getBit (n + 2) j = false

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
h : getBit (n + 2) 0 = true
⊢ getBit (n + 2) zero = true ∧ ∀ (j : Nat), j < 0 → getBit (n + 2) j = false
Tactic:
apply And.intro h ?_
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
h : getBit (n + 2) 0 = true
⊢ ∀ (j : Nat), j < 0 → getBit (n + 2) j = false

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
h : getBit (n + 2) 0 = true
⊢ ∀ (j : Nat), j < 0 → getBit (n + 2) j = false
Tactic:
intro _ hj
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
h : getBit (n + 2) 0 = true
j✝ : Nat
hj : j✝ < 0
⊢ getBit (n + 2) j✝ = false

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
h : getBit (n + 2) 0 = true
j✝ : Nat
hj : j✝ < 0
⊢ getBit (n + 2) j✝ = false
Tactic:
cases hj
State after:
no goals

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
⊢ (getBit (n + 2) zero = true ∧ ∀ (j : Nat), j < zero → getBit (n + 2) j = false) → getBit (n + 2) zero = true
Tactic:
exact And.left
State after:
no goals

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)) (succ i) = true ↔
    getBit (n + 2) (succ i) = true ∧ ∀ (j : Nat), j < succ i → getBit (n + 2) j = false
Tactic:
cases Nat.mod_two_eq_zero_or_one n
State after:
case inl
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
h✝ : n % 2 = 0
⊢ getBit (Nat.lsb (n + 2)) (succ i) = true ↔
    getBit (n + 2) (succ i) = true ∧ ∀ (j : Nat), j < succ i → getBit (n + 2) j = false

case inr
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
h✝ : 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

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
⊢ 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:
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
State after:
no goals

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:
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›]
State after:
no goals

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
⊢ 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 = (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]
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
⊢ getBit (Nat.lsb (n + 2)) (succ i) = true ↔
    getBit (n + 2) (succ i) = true ∧ ∀ (j : Nat), j < succ i → getBit (n + 2) j = false

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
⊢ 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:
simp only [
  this, ←Nat.lsb_shiftLeft,
  Nat.succ_eq_add_one,
  ←Nat.shiftRight_getBit,
  Nat.shiftLeft_shiftRight_self,
  Nat.shiftLeft_getBit
]
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
⊢ getBit (Nat.lsb (n / 2 + 1)) i = true ↔
    getBit (n / 2 + 1) i = true ∧ ∀ (j : Nat), j < i + 1 → (decide (j ≥ 1) && getBit (n / 2 + 1) (j - 1)) = false

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
⊢ getBit (Nat.lsb (n / 2 + 1)) i = true ↔
    getBit (n / 2 + 1) i = true ∧ ∀ (j : Nat), j < i + 1 → (decide (j ≥ 1) && getBit (n / 2 + 1) (j - 1)) = false
Tactic:
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
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),
    (∀ (j : Nat), j < i → getBit m j = false) ↔ ∀ (j : Nat), j < succ i → (decide (j ≥ 1) && getBit m (j - 1)) = false

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),
    (∀ (j : Nat), j < i → getBit m j = false) ↔ ∀ (j : Nat), j < succ i → (decide (j ≥ 1) && getBit m (j - 1)) = false
Tactic:
intro m
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
⊢ (∀ (j : Nat), j < i → getBit m j = false) ↔ ∀ (j : Nat), j < succ i → (decide (j ≥ 1) && getBit m (j - 1)) = false

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
⊢ (∀ (j : Nat), j < i → getBit m j = false) ↔ ∀ (j : Nat), j < succ i → (decide (j ≥ 1) && getBit m (j - 1)) = false
Tactic:
constructor
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
heven : n % 2 = 0
this : n + 2 = (n / 2 + 1) <<< 1
m : Nat
⊢ (∀ (j : Nat), j < i → getBit m j = false) → ∀ (j : Nat), j < succ i → (decide (j ≥ 1) && getBit m (j - 1)) = 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
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

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
heven : n % 2 = 0
this : n + 2 = (n / 2 + 1) <<< 1
m : Nat
⊢ (∀ (j : Nat), j < i → getBit m j = false) → ∀ (j : Nat), j < succ i → (decide (j ≥ 1) && getBit m (j - 1)) = 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
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
  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
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
⊢ (∀ (j : Nat), j < succ i → (decide (j ≥ 1) && getBit m (j - 1)) = false) → ∀ (j : Nat), j < i → getBit m j = false

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
  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
State after:
no goals

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
⊢ n + 2 = n / 2 * 2 + 2
Tactic:
rw [Nat.div_mul_cancel (Nat.dvd_of_mod_eq_zero heven)]
State after:
no goals

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
⊢ (n / 2 + 1) * 2 = (n / 2 + 1) <<< 1
Tactic:
rw [Nat.mul_comm, Nat.shiftLeft_one]
State after:
no goals

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
this :
  ∀ (m : Nat),
    (∀ (j : Nat), j < i → getBit m j = false) ↔ ∀ (j : Nat), j < succ i → (decide (j ≥ 1) && getBit m (j - 1)) = false
⊢ getBit (Nat.lsb (n / 2 + 1)) i = true ↔
    getBit (n / 2 + 1) i = true ∧ ∀ (j : Nat), j < i + 1 → (decide (j ≥ 1) && getBit (n / 2 + 1) (j - 1)) = false
Tactic:
rw [←this]
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
this :
  ∀ (m : Nat),
    (∀ (j : Nat), j < i → getBit m j = false) ↔ ∀ (j : Nat), j < succ i → (decide (j ≥ 1) && getBit m (j - 1)) = false
⊢ getBit (Nat.lsb (n / 2 + 1)) i = true ↔
    getBit (n / 2 + 1) i = true ∧ ∀ (j : Nat), j < i → getBit (n / 2 + 1) j = false

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
this :
  ∀ (m : Nat),
    (∀ (j : Nat), j < i → getBit m j = false) ↔ ∀ (j : Nat), j < succ i → (decide (j ≥ 1) && getBit m (j - 1)) = false
⊢ getBit (Nat.lsb (n / 2 + 1)) i = true ↔
    getBit (n / 2 + 1) i = true ∧ ∀ (j : Nat), j < i → getBit (n / 2 + 1) j = false
Tactic:
exact h_ind
State after:
no goals

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
heven : n % 2 = 0
this : n + 2 = (n / 2 + 1) <<< 1
m : Nat
⊢ (∀ (j : Nat), j < i → getBit m j = false) → ∀ (j : Nat), j < succ i → (decide (j ≥ 1) && getBit m (j - 1)) = false
Tactic:
intro h j hj
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
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 : j < succ i
⊢ (decide (j ≥ 1) && getBit m (j - 1)) = false

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
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 : j < succ i
⊢ (decide (j ≥ 1) && getBit m (j - 1)) = false
Tactic:
cases j
State after:
case mp.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
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

case mp.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
i : Nat
heven : n % 2 = 0
this : n + 2 = (n / 2 + 1) <<< 1
m : Nat
h : ∀ (j : Nat), j < i → getBit m j = false
n✝ : Nat
hj : succ n✝ < succ i
⊢ (decide (succ n✝ ≥ 1) && getBit m (succ n✝ - 1)) = false

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]
State after:
no goals

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
State after:
no goals

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]
State after:
no goals

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
State after:
no goals

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
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

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]
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

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
State after:
no goals

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
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

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)
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

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]
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

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
State after:
no goals

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
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

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]
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

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
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

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›]
State after:
no goals

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
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

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
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

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
State after:
no goals

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
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

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
State after:
no goals

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
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

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
State after:
no goals