internlm/Lean-Github huggingface dataset:
Theorem: UInt.getBit_lsb_ctz
Proof state before:
case a
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
i : Nat
x : α
hi : ∀ (j : Nat), UInt.getBit x j = decide (i = j)
f : Nat → α → α := fun i y => UInt.when (decide (x &&& bitmask (OfNat.ofNat i) ≠ 0)) (1 <<< OfNat.ofNat i) ||| y
this✝² : UInt.getBit x i = true
this✝¹ : i < length α
this✝ : 0 < length α
foldf_high : ∀ (n k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
this : ∀ (n : Nat), n < length α → ∀ (k : Nat), k < n → UInt.getBit (Nat.fold f n 0) k = Nat.getBit i k
what_is_shown :
  ∀ (k : Nat), k < Nat.log2RU (length α) → UInt.getBit (Nat.fold f (Nat.log2RU (length α)) 0) k = Nat.getBit i k
⊢ ∀ (i_1 : Nat), Nat.getBit (toNat (Nat.fold f (Nat.log2RU (length α)) 0)) i_1 = Nat.getBit i i_1
Tactic:
intro k
Proof state after:
case a
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
i : Nat
x : α
hi : ∀ (j : Nat), UInt.getBit x j = decide (i = j)
f : Nat → α → α := fun i y => UInt.when (decide (x &&& bitmask (OfNat.ofNat i) ≠ 0)) (1 <<< OfNat.ofNat i) ||| y
this✝² : UInt.getBit x i = true
this✝¹ : i < length α
this✝ : 0 < length α
foldf_high : ∀ (n k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
this : ∀ (n : Nat), n < length α → ∀ (k : Nat), k < n → UInt.getBit (Nat.fold f n 0) k = Nat.getBit i k
what_is_shown :
  ∀ (k : Nat), k < Nat.log2RU (length α) → UInt.getBit (Nat.fold f (Nat.log2RU (length α)) 0) k = Nat.getBit i k
k : Nat
⊢ Nat.getBit (toNat (Nat.fold f (Nat.log2RU (length α)) 0)) k = Nat.getBit i k
Theorem: UInt.getBit_lsb_ctz
Proof state before:
case a
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
i : Nat
x : α
hi : ∀ (j : Nat), UInt.getBit x j = decide (i = j)
f : Nat → α → α := fun i y => UInt.when (decide (x &&& bitmask (OfNat.ofNat i) ≠ 0)) (1 <<< OfNat.ofNat i) ||| y
this✝² : UInt.getBit x i = true
this✝¹ : i < length α
this✝ : 0 < length α
foldf_high : ∀ (n k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
this : ∀ (n : Nat), n < length α → ∀ (k : Nat), k < n → UInt.getBit (Nat.fold f n 0) k = Nat.getBit i k
what_is_shown :
  ∀ (k : Nat), k < Nat.log2RU (length α) → UInt.getBit (Nat.fold f (Nat.log2RU (length α)) 0) k = Nat.getBit i k
k : Nat
⊢ Nat.getBit (toNat (Nat.fold f (Nat.log2RU (length α)) 0)) k = Nat.getBit i k
Tactic:
cases Nat.lt_or_ge k (Nat.log2RU $ length α)
Proof state after:
case a.inl
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
i : Nat
x : α
hi : ∀ (j : Nat), UInt.getBit x j = decide (i = j)
f : Nat → α → α := fun i y => UInt.when (decide (x &&& bitmask (OfNat.ofNat i) ≠ 0)) (1 <<< OfNat.ofNat i) ||| y
this✝² : UInt.getBit x i = true
this✝¹ : i < length α
this✝ : 0 < length α
foldf_high : ∀ (n k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
this : ∀ (n : Nat), n < length α → ∀ (k : Nat), k < n → UInt.getBit (Nat.fold f n 0) k = Nat.getBit i k
what_is_shown :
  ∀ (k : Nat), k < Nat.log2RU (length α) → UInt.getBit (Nat.fold f (Nat.log2RU (length α)) 0) k = Nat.getBit i k
k : Nat
h✝ : k < Nat.log2RU (length α)
⊢ Nat.getBit (toNat (Nat.fold f (Nat.log2RU (length α)) 0)) k = Nat.getBit i k

case a.inr
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
i : Nat
x : α
hi : ∀ (j : Nat), UInt.getBit x j = decide (i = j)
f : Nat → α → α := fun i y => UInt.when (decide (x &&& bitmask (OfNat.ofNat i) ≠ 0)) (1 <<< OfNat.ofNat i) ||| y
this✝² : UInt.getBit x i = true
this✝¹ : i < length α
this✝ : 0 < length α
foldf_high : ∀ (n k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
this : ∀ (n : Nat), n < length α → ∀ (k : Nat), k < n → UInt.getBit (Nat.fold f n 0) k = Nat.getBit i k
what_is_shown :
  ∀ (k : Nat), k < Nat.log2RU (length α) → UInt.getBit (Nat.fold f (Nat.log2RU (length α)) 0) k = Nat.getBit i k
k : Nat
h✝ : k ≥ Nat.log2RU (length α)
⊢ Nat.getBit (toNat (Nat.fold f (Nat.log2RU (length α)) 0)) k = Nat.getBit i k
Theorem: UInt.getBit_lsb_ctz
Proof state before:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
i : Nat
x : α
hi : ∀ (j : Nat), UInt.getBit x j = decide (i = j)
f : Nat → α → α := fun i y => UInt.when (decide (x &&& bitmask (OfNat.ofNat i) ≠ 0)) (1 <<< OfNat.ofNat i) ||| y
this✝² : UInt.getBit x i = true
this✝¹ : i < length α
this✝ : 0 < length α
foldf_high : ∀ (n k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
this : ∀ (n : Nat), n < length α → ∀ (k : Nat), k < n → UInt.getBit (Nat.fold f n 0) k = Nat.getBit i k
what_is_shown :
  ∀ (k : Nat), k < Nat.log2RU (length α) → UInt.getBit (Nat.fold f (Nat.log2RU (length α)) 0) k = Nat.getBit i k
k : Nat
hlt : k < Nat.log2RU (length α)
⊢ Nat.getBit (toNat (Nat.fold f (Nat.log2RU (length α)) 0)) k = Nat.getBit i k
Tactic:
case a.inl hlt => exact what_is_shown k hlt
Proof state after:
no goals
Theorem: UInt.getBit_lsb_ctz
Proof state before:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
i : Nat
x : α
hi : ∀ (j : Nat), UInt.getBit x j = decide (i = j)
f : Nat → α → α := fun i y => UInt.when (decide (x &&& bitmask (OfNat.ofNat i) ≠ 0)) (1 <<< OfNat.ofNat i) ||| y
this✝² : UInt.getBit x i = true
this✝¹ : i < length α
this✝ : 0 < length α
foldf_high : ∀ (n k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
this : ∀ (n : Nat), n < length α → ∀ (k : Nat), k < n → UInt.getBit (Nat.fold f n 0) k = Nat.getBit i k
what_is_shown :
  ∀ (k : Nat), k < Nat.log2RU (length α) → UInt.getBit (Nat.fold f (Nat.log2RU (length α)) 0) k = Nat.getBit i k
k : Nat
hge : k ≥ Nat.log2RU (length α)
⊢ Nat.getBit (toNat (Nat.fold f (Nat.log2RU (length α)) 0)) k = Nat.getBit i k
Tactic:
case a.inr hge =>
  unfold UInt.getBit at foldf_high; rw [foldf_high _ _ hge]
  suffices Nat.getBit i k = false
    from Eq.symm this
  apply Nat.getBit_high ?_ k hge
  calc
    i < length α := ‹_›
    _ ≤ 2^Nat.log2RU (length α) := Nat.le_pow2_log2RU_self _
Proof state after:
no goals
Theorem: UInt.getBit_lsb_ctz
Proof state before:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
i : Nat
x : α
hi : ∀ (j : Nat), UInt.getBit x j = decide (i = j)
f : Nat → α → α := fun i y => UInt.when (decide (x &&& bitmask (OfNat.ofNat i) ≠ 0)) (1 <<< OfNat.ofNat i) ||| y
this✝² : UInt.getBit x i = true
this✝¹ : i < length α
this✝ : 0 < length α
foldf_high : ∀ (n k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
this : ∀ (n : Nat), n < length α → ∀ (k : Nat), k < n → UInt.getBit (Nat.fold f n 0) k = Nat.getBit i k
what_is_shown :
  ∀ (k : Nat), k < Nat.log2RU (length α) → UInt.getBit (Nat.fold f (Nat.log2RU (length α)) 0) k = Nat.getBit i k
k : Nat
hlt : k < Nat.log2RU (length α)
⊢ Nat.getBit (toNat (Nat.fold f (Nat.log2RU (length α)) 0)) k = Nat.getBit i k
Tactic:
exact what_is_shown k hlt
Proof state after:
no goals
Theorem: UInt.getBit_lsb_ctz
Proof state before:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
i : Nat
x : α
hi : ∀ (j : Nat), UInt.getBit x j = decide (i = j)
f : Nat → α → α := fun i y => UInt.when (decide (x &&& bitmask (OfNat.ofNat i) ≠ 0)) (1 <<< OfNat.ofNat i) ||| y
this✝² : UInt.getBit x i = true
this✝¹ : i < length α
this✝ : 0 < length α
foldf_high : ∀ (n k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
this : ∀ (n : Nat), n < length α → ∀ (k : Nat), k < n → UInt.getBit (Nat.fold f n 0) k = Nat.getBit i k
what_is_shown :
  ∀ (k : Nat), k < Nat.log2RU (length α) → UInt.getBit (Nat.fold f (Nat.log2RU (length α)) 0) k = Nat.getBit i k
k : Nat
hge : k ≥ Nat.log2RU (length α)
⊢ Nat.getBit (toNat (Nat.fold f (Nat.log2RU (length α)) 0)) k = Nat.getBit i k
Tactic:
unfold UInt.getBit at foldf_high
Proof state after:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
i : Nat
x : α
hi : ∀ (j : Nat), UInt.getBit x j = decide (i = j)
f : Nat → α → α := fun i y => UInt.when (decide (x &&& bitmask (OfNat.ofNat i) ≠ 0)) (1 <<< OfNat.ofNat i) ||| y
this✝² : UInt.getBit x i = true
this✝¹ : i < length α
this✝ : 0 < length α
foldf_high : ∀ (n k : Nat), k ≥ n → Nat.getBit (toNat (Nat.fold f n 0)) k = false
this : ∀ (n : Nat), n < length α → ∀ (k : Nat), k < n → UInt.getBit (Nat.fold f n 0) k = Nat.getBit i k
what_is_shown :
  ∀ (k : Nat), k < Nat.log2RU (length α) → UInt.getBit (Nat.fold f (Nat.log2RU (length α)) 0) k = Nat.getBit i k
k : Nat
hge : k ≥ Nat.log2RU (length α)
⊢ Nat.getBit (toNat (Nat.fold f (Nat.log2RU (length α)) 0)) k = Nat.getBit i k
Theorem: UInt.getBit_lsb_ctz
Proof state before:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
i : Nat
x : α
hi : ∀ (j : Nat), UInt.getBit x j = decide (i = j)
f : Nat → α → α := fun i y => UInt.when (decide (x &&& bitmask (OfNat.ofNat i) ≠ 0)) (1 <<< OfNat.ofNat i) ||| y
this✝² : UInt.getBit x i = true
this✝¹ : i < length α
this✝ : 0 < length α
foldf_high : ∀ (n k : Nat), k ≥ n → Nat.getBit (toNat (Nat.fold f n 0)) k = false
this : ∀ (n : Nat), n < length α → ∀ (k : Nat), k < n → UInt.getBit (Nat.fold f n 0) k = Nat.getBit i k
what_is_shown :
  ∀ (k : Nat), k < Nat.log2RU (length α) → UInt.getBit (Nat.fold f (Nat.log2RU (length α)) 0) k = Nat.getBit i k
k : Nat
hge : k ≥ Nat.log2RU (length α)
⊢ Nat.getBit (toNat (Nat.fold f (Nat.log2RU (length α)) 0)) k = Nat.getBit i k
Tactic:
rw [foldf_high _ _ hge]
Proof state after:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
i : Nat
x : α
hi : ∀ (j : Nat), UInt.getBit x j = decide (i = j)
f : Nat → α → α := fun i y => UInt.when (decide (x &&& bitmask (OfNat.ofNat i) ≠ 0)) (1 <<< OfNat.ofNat i) ||| y
this✝² : UInt.getBit x i = true
this✝¹ : i < length α
this✝ : 0 < length α
foldf_high : ∀ (n k : Nat), k ≥ n → Nat.getBit (toNat (Nat.fold f n 0)) k = false
this : ∀ (n : Nat), n < length α → ∀ (k : Nat), k < n → UInt.getBit (Nat.fold f n 0) k = Nat.getBit i k
what_is_shown :
  ∀ (k : Nat), k < Nat.log2RU (length α) → UInt.getBit (Nat.fold f (Nat.log2RU (length α)) 0) k = Nat.getBit i k
k : Nat
hge : k ≥ Nat.log2RU (length α)
⊢ false = Nat.getBit i k
Theorem: UInt.getBit_lsb_ctz
Proof state before:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
i : Nat
x : α
hi : ∀ (j : Nat), UInt.getBit x j = decide (i = j)
f : Nat → α → α := fun i y => UInt.when (decide (x &&& bitmask (OfNat.ofNat i) ≠ 0)) (1 <<< OfNat.ofNat i) ||| y
this✝² : UInt.getBit x i = true
this✝¹ : i < length α
this✝ : 0 < length α
foldf_high : ∀ (n k : Nat), k ≥ n → Nat.getBit (toNat (Nat.fold f n 0)) k = false
this : ∀ (n : Nat), n < length α → ∀ (k : Nat), k < n → UInt.getBit (Nat.fold f n 0) k = Nat.getBit i k
what_is_shown :
  ∀ (k : Nat), k < Nat.log2RU (length α) → UInt.getBit (Nat.fold f (Nat.log2RU (length α)) 0) k = Nat.getBit i k
k : Nat
hge : k ≥ Nat.log2RU (length α)
⊢ false = Nat.getBit i k
Tactic:
suffices Nat.getBit i k = false
  from Eq.symm this
Proof state after:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
i : Nat
x : α
hi : ∀ (j : Nat), UInt.getBit x j = decide (i = j)
f : Nat → α → α := fun i y => UInt.when (decide (x &&& bitmask (OfNat.ofNat i) ≠ 0)) (1 <<< OfNat.ofNat i) ||| y
this✝² : UInt.getBit x i = true
this✝¹ : i < length α
this✝ : 0 < length α
foldf_high : ∀ (n k : Nat), k ≥ n → Nat.getBit (toNat (Nat.fold f n 0)) k = false
this : ∀ (n : Nat), n < length α → ∀ (k : Nat), k < n → UInt.getBit (Nat.fold f n 0) k = Nat.getBit i k
what_is_shown :
  ∀ (k : Nat), k < Nat.log2RU (length α) → UInt.getBit (Nat.fold f (Nat.log2RU (length α)) 0) k = Nat.getBit i k
k : Nat
hge : k ≥ Nat.log2RU (length α)
⊢ Nat.getBit i k = false
Theorem: UInt.getBit_lsb_ctz
Proof state before:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
i : Nat
x : α
hi : ∀ (j : Nat), UInt.getBit x j = decide (i = j)
f : Nat → α → α := fun i y => UInt.when (decide (x &&& bitmask (OfNat.ofNat i) ≠ 0)) (1 <<< OfNat.ofNat i) ||| y
this✝² : UInt.getBit x i = true
this✝¹ : i < length α
this✝ : 0 < length α
foldf_high : ∀ (n k : Nat), k ≥ n → Nat.getBit (toNat (Nat.fold f n 0)) k = false
this : ∀ (n : Nat), n < length α → ∀ (k : Nat), k < n → UInt.getBit (Nat.fold f n 0) k = Nat.getBit i k
what_is_shown :
  ∀ (k : Nat), k < Nat.log2RU (length α) → UInt.getBit (Nat.fold f (Nat.log2RU (length α)) 0) k = Nat.getBit i k
k : Nat
hge : k ≥ Nat.log2RU (length α)
⊢ Nat.getBit i k = false
Tactic:
apply Nat.getBit_high ?_ k hge
Proof state after:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
i : Nat
x : α
hi : ∀ (j : Nat), UInt.getBit x j = decide (i = j)
f : Nat → α → α := fun i y => UInt.when (decide (x &&& bitmask (OfNat.ofNat i) ≠ 0)) (1 <<< OfNat.ofNat i) ||| y
this✝² : UInt.getBit x i = true
this✝¹ : i < length α
this✝ : 0 < length α
foldf_high : ∀ (n k : Nat), k ≥ n → Nat.getBit (toNat (Nat.fold f n 0)) k = false
this : ∀ (n : Nat), n < length α → ∀ (k : Nat), k < n → UInt.getBit (Nat.fold f n 0) k = Nat.getBit i k
what_is_shown :
  ∀ (k : Nat), k < Nat.log2RU (length α) → UInt.getBit (Nat.fold f (Nat.log2RU (length α)) 0) k = Nat.getBit i k
k : Nat
hge : k ≥ Nat.log2RU (length α)
⊢ i < 2 ^ Nat.log2RU (length α)
Theorem: UInt.getBit_lsb_ctz
Proof state before:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
i : Nat
x : α
hi : ∀ (j : Nat), UInt.getBit x j = decide (i = j)
f : Nat → α → α := fun i y => UInt.when (decide (x &&& bitmask (OfNat.ofNat i) ≠ 0)) (1 <<< OfNat.ofNat i) ||| y
this✝² : UInt.getBit x i = true
this✝¹ : i < length α
this✝ : 0 < length α
foldf_high : ∀ (n k : Nat), k ≥ n → Nat.getBit (toNat (Nat.fold f n 0)) k = false
this : ∀ (n : Nat), n < length α → ∀ (k : Nat), k < n → UInt.getBit (Nat.fold f n 0) k = Nat.getBit i k
what_is_shown :
  ∀ (k : Nat), k < Nat.log2RU (length α) → UInt.getBit (Nat.fold f (Nat.log2RU (length α)) 0) k = Nat.getBit i k
k : Nat
hge : k ≥ Nat.log2RU (length α)
⊢ i < 2 ^ Nat.log2RU (length α)
Tactic:
calc
  i < length α := ‹_›
  _ ≤ 2^Nat.log2RU (length α) := Nat.le_pow2_log2RU_self _
Proof state after:
no goals
Theorem: UInt.getBit_lsb_ctz
Proof state before:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
i : Nat
x : α
hi : ∀ (j : Nat), UInt.getBit x j = decide (i = j)
f : Nat → α → α := fun i y => UInt.when (decide (x &&& bitmask (OfNat.ofNat i) ≠ 0)) (1 <<< OfNat.ofNat i) ||| y
this✝¹ : UInt.getBit x i = true
this✝ : i < length α
this : 0 < length α
foldf_high : ∀ (n k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
hn : Nat.zero < length α
k : Nat
hk : k < Nat.zero
⊢ UInt.getBit (Nat.fold f Nat.zero 0) k = Nat.getBit i k
Tactic:
cases hk
Proof state after:
no goals
Theorem: UInt.getBit_lsb_ctz
Proof state before:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
i : Nat
x : α
hi : ∀ (j : Nat), UInt.getBit x j = decide (i = j)
f : Nat → α → α := fun i y => UInt.when (decide (x &&& bitmask (OfNat.ofNat i) ≠ 0)) (1 <<< OfNat.ofNat i) ||| y
this✝¹ : UInt.getBit x i = true
this✝ : i < length α
this : 0 < length α
foldf_high : ∀ (n k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
n : Nat
h_ind : n < length α → ∀ (k : Nat), k < n → UInt.getBit (Nat.fold f n 0) k = Nat.getBit i k
hn : Nat.succ n < length α
k : Nat
hk : k < Nat.succ n
⊢ UInt.getBit (Nat.fold f (Nat.succ n) 0) k = Nat.getBit i k
Tactic:
unfold Nat.fold
Proof state after:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
i : Nat
x : α
hi : ∀ (j : Nat), UInt.getBit x j = decide (i = j)
f : Nat → α → α := fun i y => UInt.when (decide (x &&& bitmask (OfNat.ofNat i) ≠ 0)) (1 <<< OfNat.ofNat i) ||| y
this✝¹ : UInt.getBit x i = true
this✝ : i < length α
this : 0 < length α
foldf_high : ∀ (n k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
n : Nat
h_ind : n < length α → ∀ (k : Nat), k < n → UInt.getBit (Nat.fold f n 0) k = Nat.getBit i k
hn : Nat.succ n < length α
k : Nat
hk : k < Nat.succ n
⊢ UInt.getBit (f n (Nat.fold f n 0)) k = Nat.getBit i k
Theorem: UInt.getBit_lsb_ctz
Proof state before:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
i : Nat
x : α
hi : ∀ (j : Nat), UInt.getBit x j = decide (i = j)
f : Nat → α → α := fun i y => UInt.when (decide (x &&& bitmask (OfNat.ofNat i) ≠ 0)) (1 <<< OfNat.ofNat i) ||| y
this✝¹ : UInt.getBit x i = true
this✝ : i < length α
this : 0 < length α
foldf_high : ∀ (n k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
n : Nat
h_ind : n < length α → ∀ (k : Nat), k < n → UInt.getBit (Nat.fold f n 0) k = Nat.getBit i k
hn : Nat.succ n < length α
k : Nat
hk : k < Nat.succ n
⊢ UInt.getBit (f n (Nat.fold f n 0)) k = Nat.getBit i k
Tactic:
conv =>
  lhs; arg 1;
  change UInt.when (x &&& bitmask (OfNat.ofNat n) ≠ 0) ((1 : α) <<< OfNat.ofNat n) ||| Nat.fold f n 0
Proof state after:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
i : Nat
x : α
hi : ∀ (j : Nat), UInt.getBit x j = decide (i = j)
f : Nat → α → α := fun i y => UInt.when (decide (x &&& bitmask (OfNat.ofNat i) ≠ 0)) (1 <<< OfNat.ofNat i) ||| y
this✝¹ : UInt.getBit x i = true
this✝ : i < length α
this : 0 < length α
foldf_high : ∀ (n k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
n : Nat
h_ind : n < length α → ∀ (k : Nat), k < n → UInt.getBit (Nat.fold f n 0) k = Nat.getBit i k
hn : Nat.succ n < length α
k : Nat
hk : k < Nat.succ n
⊢ UInt.getBit (UInt.when (decide (x &&& bitmask (OfNat.ofNat n) ≠ 0)) (1 <<< OfNat.ofNat n) ||| Nat.fold f n 0) k =
    Nat.getBit i k
Theorem: UInt.getBit_lsb_ctz
Proof state before:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
i : Nat
x : α
hi : ∀ (j : Nat), UInt.getBit x j = decide (i = j)
f : Nat → α → α := fun i y => UInt.when (decide (x &&& bitmask (OfNat.ofNat i) ≠ 0)) (1 <<< OfNat.ofNat i) ||| y
this✝¹ : UInt.getBit x i = true
this✝ : i < length α
this : 0 < length α
foldf_high : ∀ (n k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
n : Nat
h_ind : n < length α → ∀ (k : Nat), k < n → UInt.getBit (Nat.fold f n 0) k = Nat.getBit i k
hn : Nat.succ n < length α
k : Nat
hk : k < Nat.succ n
⊢ UInt.getBit (UInt.when (decide (x &&& bitmask (OfNat.ofNat n) ≠ 0)) (1 <<< OfNat.ofNat n) ||| Nat.fold f n 0) k =
    Nat.getBit i k
Tactic:
rw [UInt.getBit_lor]
Proof state after:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
i : Nat
x : α
hi : ∀ (j : Nat), UInt.getBit x j = decide (i = j)
f : Nat → α → α := fun i y => UInt.when (decide (x &&& bitmask (OfNat.ofNat i) ≠ 0)) (1 <<< OfNat.ofNat i) ||| y
this✝¹ : UInt.getBit x i = true
this✝ : i < length α
this : 0 < length α
foldf_high : ∀ (n k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
n : Nat
h_ind : n < length α → ∀ (k : Nat), k < n → UInt.getBit (Nat.fold f n 0) k = Nat.getBit i k
hn : Nat.succ n < length α
k : Nat
hk : k < Nat.succ n
⊢ (UInt.getBit (UInt.when (decide (x &&& bitmask (OfNat.ofNat n) ≠ 0)) (1 <<< OfNat.ofNat n)) k ||
      UInt.getBit (Nat.fold f n 0) k) =
    Nat.getBit i k
Theorem: UInt.getBit_lsb_ctz
Proof state before:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
i : Nat
x : α
hi : ∀ (j : Nat), UInt.getBit x j = decide (i = j)
f : Nat → α → α := fun i y => UInt.when (decide (x &&& bitmask (OfNat.ofNat i) ≠ 0)) (1 <<< OfNat.ofNat i) ||| y
this✝¹ : UInt.getBit x i = true
this✝ : i < length α
this : 0 < length α
foldf_high : ∀ (n k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
n : Nat
h_ind : n < length α → ∀ (k : Nat), k < n → UInt.getBit (Nat.fold f n 0) k = Nat.getBit i k
hn : Nat.succ n < length α
k : Nat
hk : k < Nat.succ n
⊢ (UInt.getBit (UInt.when (decide (x &&& bitmask (OfNat.ofNat n) ≠ 0)) (1 <<< OfNat.ofNat n)) k ||
      UInt.getBit (Nat.fold f n 0) k) =
    Nat.getBit i k
Tactic:
have : n < length α := Nat.lt_of_succ_lt hn
Proof state after:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
i : Nat
x : α
hi : ∀ (j : Nat), UInt.getBit x j = decide (i = j)
f : Nat → α → α := fun i y => UInt.when (decide (x &&& bitmask (OfNat.ofNat i) ≠ 0)) (1 <<< OfNat.ofNat i) ||| y
this✝² : UInt.getBit x i = true
this✝¹ : i < length α
this✝ : 0 < length α
foldf_high : ∀ (n k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
n : Nat
h_ind : n < length α → ∀ (k : Nat), k < n → UInt.getBit (Nat.fold f n 0) k = Nat.getBit i k
hn : Nat.succ n < length α
k : Nat
hk : k < Nat.succ n
this : n < length α
⊢ (UInt.getBit (UInt.when (decide (x &&& bitmask (OfNat.ofNat n) ≠ 0)) (1 <<< OfNat.ofNat n)) k ||
      UInt.getBit (Nat.fold f n 0) k) =
    Nat.getBit i k
Theorem: UInt.getBit_lsb_ctz
Proof state before:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
i : Nat
x : α
hi : ∀ (j : Nat), UInt.getBit x j = decide (i = j)
f : Nat → α → α := fun i y => UInt.when (decide (x &&& bitmask (OfNat.ofNat i) ≠ 0)) (1 <<< OfNat.ofNat i) ||| y
this✝² : UInt.getBit x i = true
this✝¹ : i < length α
this✝ : 0 < length α
foldf_high : ∀ (n k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
n : Nat
h_ind : n < length α → ∀ (k : Nat), k < n → UInt.getBit (Nat.fold f n 0) k = Nat.getBit i k
hn : Nat.succ n < length α
k : Nat
hk : k < Nat.succ n
this : n < length α
⊢ (UInt.getBit (UInt.when (decide (x &&& bitmask (OfNat.ofNat n) ≠ 0)) (1 <<< OfNat.ofNat n)) k ||
      UInt.getBit (Nat.fold f n 0) k) =
    Nat.getBit i k
Tactic:
have : n < 2^length α := trans this (Nat.exp_lt_pow _ .refl)
Proof state after:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
i : Nat
x : α
hi : ∀ (j : Nat), UInt.getBit x j = decide (i = j)
f : Nat → α → α := fun i y => UInt.when (decide (x &&& bitmask (OfNat.ofNat i) ≠ 0)) (1 <<< OfNat.ofNat i) ||| y
this✝³ : UInt.getBit x i = true
this✝² : i < length α
this✝¹ : 0 < length α
foldf_high : ∀ (n k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
n : Nat
h_ind : n < length α → ∀ (k : Nat), k < n → UInt.getBit (Nat.fold f n 0) k = Nat.getBit i k
hn : Nat.succ n < length α
k : Nat
hk : k < Nat.succ n
this✝ : n < length α
this : n < 2 ^ length α
⊢ (UInt.getBit (UInt.when (decide (x &&& bitmask (OfNat.ofNat n) ≠ 0)) (1 <<< OfNat.ofNat n)) k ||
      UInt.getBit (Nat.fold f n 0) k) =
    Nat.getBit i k