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

State before:
n : Nat
⊢ n % 2 = 1 → Nat.lsb n = 1
Tactic:
intro h
State after:
n : Nat
h : n % 2 = 1
⊢ Nat.lsb n = 1

State before:
n : Nat
h : n % 2 = 1
⊢ Nat.lsb n = 1
Tactic:
unfold Nat.lsb
State after:
n : Nat
h : n % 2 = 1
⊢ n ^^^ n &&& n - 1 = 1

State before:
n : Nat
h : n % 2 = 1
⊢ n ^^^ n &&& n - 1 = 1
Tactic:
have : n = 2*(n/2) + 1 :=
  Eq.symm $ Nat.add_comm .. ▸ h ▸ Nat.mod_add_div n 2
State after:
n : Nat
h : n % 2 = 1
this : n = 2 * (n / 2) + 1
⊢ n ^^^ n &&& n - 1 = 1

State before:
n : Nat
h : n % 2 = 1
this : n = 2 * (n / 2) + 1
⊢ n ^^^ n &&& n - 1 = 1
Tactic:
clear h
State after:
n : Nat
this : n = 2 * (n / 2) + 1
⊢ n ^^^ n &&& n - 1 = 1

State before:
n : Nat
this : n = 2 * (n / 2) + 1
⊢ n ^^^ n &&& n - 1 = 1
Tactic:
rw [this, Nat.add_sub_cancel]
State after:
n : Nat
this : n = 2 * (n / 2) + 1
⊢ 2 * (n / 2) + 1 ^^^ 2 * (n / 2) + 1 &&& 2 * (n / 2) = 1

State before:
n : Nat
this : n = 2 * (n / 2) + 1
⊢ 2 * (n / 2) + 1 ^^^ 2 * (n / 2) + 1 &&& 2 * (n / 2) = 1
Tactic:
have : 2*(n/2) + 1 = 2*(n/2) ^^^ 1 := by
  apply Nat.add_eq_xor
  rw [Nat.land_one, Nat.mul_mod_right]
State after:
n : Nat
this✝ : n = 2 * (n / 2) + 1
this : 2 * (n / 2) + 1 = 2 * (n / 2) ^^^ 1
⊢ 2 * (n / 2) + 1 ^^^ 2 * (n / 2) + 1 &&& 2 * (n / 2) = 1

State before:
n : Nat
this✝ : n = 2 * (n / 2) + 1
this : 2 * (n / 2) + 1 = 2 * (n / 2) ^^^ 1
⊢ 2 * (n / 2) + 1 ^^^ 2 * (n / 2) + 1 &&& 2 * (n / 2) = 1
Tactic:
simp only [this]
State after:
n : Nat
this✝ : n = 2 * (n / 2) + 1
this : 2 * (n / 2) + 1 = 2 * (n / 2) ^^^ 1
⊢ 2 * (n / 2) ^^^ 1 ^^^ (2 * (n / 2) ^^^ 1) &&& 2 * (n / 2) = 1

State before:
n : Nat
this✝ : n = 2 * (n / 2) + 1
this : 2 * (n / 2) + 1 = 2 * (n / 2) ^^^ 1
⊢ 2 * (n / 2) ^^^ 1 ^^^ (2 * (n / 2) ^^^ 1) &&& 2 * (n / 2) = 1
Tactic:
rw [Nat.xor_and, Nat.land_self]
State after:
n : Nat
this✝ : n = 2 * (n / 2) + 1
this : 2 * (n / 2) + 1 = 2 * (n / 2) ^^^ 1
⊢ 2 * (n / 2) ^^^ 1 ^^^ (2 * (n / 2) ^^^ 1 &&& 2 * (n / 2)) = 1

State before:
n : Nat
this✝ : n = 2 * (n / 2) + 1
this : 2 * (n / 2) + 1 = 2 * (n / 2) ^^^ 1
⊢ 2 * (n / 2) ^^^ 1 ^^^ (2 * (n / 2) ^^^ 1 &&& 2 * (n / 2)) = 1
Tactic:
rw [←Nat.xor_assoc, Nat.xor_comm _ 1, Nat.xor_assoc 1, Nat.xor_self, Nat.xor_zero]
State after:
n : Nat
this✝ : n = 2 * (n / 2) + 1
this : 2 * (n / 2) + 1 = 2 * (n / 2) ^^^ 1
⊢ 1 ^^^ 1 &&& 2 * (n / 2) = 1

State before:
n : Nat
this✝ : n = 2 * (n / 2) + 1
this : 2 * (n / 2) + 1 = 2 * (n / 2) ^^^ 1
⊢ 1 ^^^ 1 &&& 2 * (n / 2) = 1
Tactic:
have : ∀ k, 1 &&& 2 * k = 0 := by
  intro k; rw [Nat.land_comm, Nat.land_one, Nat.mul_mod_right]
State after:
n : Nat
this✝¹ : n = 2 * (n / 2) + 1
this✝ : 2 * (n / 2) + 1 = 2 * (n / 2) ^^^ 1
this : ∀ (k : Nat), 1 &&& 2 * k = 0
⊢ 1 ^^^ 1 &&& 2 * (n / 2) = 1

State before:
n : Nat
this✝¹ : n = 2 * (n / 2) + 1
this✝ : 2 * (n / 2) + 1 = 2 * (n / 2) ^^^ 1
this : ∀ (k : Nat), 1 &&& 2 * k = 0
⊢ 1 ^^^ 1 &&& 2 * (n / 2) = 1
Tactic:
rw [this, Nat.xor_zero]
State after:
no goals

State before:
n : Nat
this : n = 2 * (n / 2) + 1
⊢ 2 * (n / 2) + 1 = 2 * (n / 2) ^^^ 1
Tactic:
apply Nat.add_eq_xor
State after:
case disjoint
n : Nat
this : n = 2 * (n / 2) + 1
⊢ 2 * (n / 2) &&& 1 = 0

State before:
case disjoint
n : Nat
this : n = 2 * (n / 2) + 1
⊢ 2 * (n / 2) &&& 1 = 0
Tactic:
rw [Nat.land_one, Nat.mul_mod_right]
State after:
no goals

State before:
n : Nat
this✝ : n = 2 * (n / 2) + 1
this : 2 * (n / 2) + 1 = 2 * (n / 2) ^^^ 1
⊢ ∀ (k : Nat), 1 &&& 2 * k = 0
Tactic:
intro k
State after:
n : Nat
this✝ : n = 2 * (n / 2) + 1
this : 2 * (n / 2) + 1 = 2 * (n / 2) ^^^ 1
k : Nat
⊢ 1 &&& 2 * k = 0

State before:
n : Nat
this✝ : n = 2 * (n / 2) + 1
this : 2 * (n / 2) + 1 = 2 * (n / 2) ^^^ 1
k : Nat
⊢ 1 &&& 2 * k = 0
Tactic:
rw [Nat.land_comm, Nat.land_one, Nat.mul_mod_right]
State after:
no goals