Theorem: UInt.getBit_lsb_ctz (Algdata/Classes/UInt.lean)

State before:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a : α
⊢ a ≠ 0 → UInt.getBit (UInt.lsb a) (toNat (UInt.ctz a)) = true
Tactic:
intro ha
State after:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a : α
ha : a ≠ 0
⊢ UInt.getBit (UInt.lsb a) (toNat (UInt.ctz a)) = true

State before:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a : α
ha : a ≠ 0
⊢ UInt.getBit (UInt.lsb a) (toNat (UInt.ctz a)) = true
Tactic:
have : UInt.lsb a ≠ 0 := λ h => absurd (UInt.eq_zero_of_lsb_eq_zero a h) ha
State after:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a : α
ha : a ≠ 0
this : UInt.lsb a ≠ 0
⊢ UInt.getBit (UInt.lsb a) (toNat (UInt.ctz a)) = true

State before:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a : α
ha : a ≠ 0
this : UInt.lsb a ≠ 0
⊢ UInt.getBit (UInt.lsb a) (toNat (UInt.ctz a)) = true
Tactic:
rw [UInt.ctz_eq_ctz']
State after:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a : α
ha : a ≠ 0
this : UInt.lsb a ≠ 0
⊢ UInt.getBit (UInt.lsb a) (toNat (UInt.ctz' a)) = true

State before:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a : α
ha : a ≠ 0
this : UInt.lsb a ≠ 0
⊢ UInt.getBit (UInt.lsb a) (toNat (UInt.ctz' a)) = true
Tactic:
dsimp [UInt.ctz']
State after:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a : α
ha : a ≠ 0
this : UInt.lsb a ≠ 0
⊢ UInt.getBit (UInt.lsb a)
      (toNat
        (Nat.fold
          (fun n x => UInt.when (decide ¬UInt.lsb a &&& bitmask (OfNat.ofNat n) = 0) (1 <<< OfNat.ofNat n) ||| x)
          (Nat.log2RU (length α)) (UInt.when (decide (UInt.lsb a = 0)) (OfNat.ofNat (length α))))) =
    true

State before:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a : α
ha : a ≠ 0
this : UInt.lsb a ≠ 0
⊢ UInt.getBit (UInt.lsb a)
      (toNat
        (Nat.fold
          (fun n x => UInt.when (decide ¬UInt.lsb a &&& bitmask (OfNat.ofNat n) = 0) (1 <<< OfNat.ofNat n) ||| x)
          (Nat.log2RU (length α)) (UInt.when (decide (UInt.lsb a = 0)) (OfNat.ofNat (length α))))) =
    true
Tactic:
rw [decide_eq_false this, UInt.when_false_eq]
State after:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a : α
ha : a ≠ 0
this : UInt.lsb a ≠ 0
⊢ UInt.getBit (UInt.lsb a)
      (toNat
        (Nat.fold
          (fun n x => UInt.when (decide ¬UInt.lsb a &&& bitmask (OfNat.ofNat n) = 0) (1 <<< OfNat.ofNat n) ||| x)
          (Nat.log2RU (length α)) 0)) =
    true

State before:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a : α
ha : a ≠ 0
this : UInt.lsb a ≠ 0
⊢ UInt.getBit (UInt.lsb a)
      (toNat
        (Nat.fold
          (fun n x => UInt.when (decide ¬UInt.lsb a &&& bitmask (OfNat.ofNat n) = 0) (1 <<< OfNat.ofNat n) ||| x)
          (Nat.log2RU (length α)) 0)) =
    true
Tactic:
cases UInt.lsb_singleton a ha with | intro i hi =>
generalize UInt.lsb a = x at *; clear ‹a≠0› a ‹x≠0›
let f (i : Nat) (y : α) : α := UInt.when (x &&& bitmask (OfNat.ofNat i) ≠ 0) ((1 : α) <<< OfNat.ofNat i) ||| y
conv =>
  change UInt.getBit x (toNat $ Nat.fold f (Nat.log2RU $ length α) 0) = true
have : UInt.getBit x i = true := (decide_eq_true (Eq.refl i) ▸ hi i)
have : i < length α := by
  cases Nat.lt_or_ge i (length α)
  case inl hlt => exact hlt
  case inr hge =>
    have := calc
      false = UInt.getBit x i := (UInt.getBit_high x i hge).symm
      _     = true := ‹_›
    cases this
have : 0 < length α := trans i.zero_le ‹i < length α›
suffices UInt.toNat (Nat.fold f (Nat.log2RU $ length α) 0) = i
  by rw [this]; assumption
have foldf_high : ∀ (n k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false := by
  intro n k hnk
  induction n generalizing k
  case zero => dsimp [Nat.fold]; exact UInt.getBit_zero k
  case succ n h_ind =>
    dsimp [Nat.fold]
    rw [UInt.getBit_lor, h_ind k (Nat.le_of_succ_le hnk), Bool.or_false]
    cases decide (x &&& bitmask (OfNat.ofNat n) ≠ 0)
    case true =>
      rw [UInt.when_true_eq, UInt.getBit_shiftLeft]
      have : UInt.getBit (1 : α) (k - toNat (OfNat.ofNat (α:=α) n) % length α) = false := by
        rw [UInt.toNat_ofNat]
        have := calc
          n % 2^length α % length α
            ≤ n % 2^length α := Nat.mod_le ..
          _ ≤ n := Nat.mod_le ..
          _ < n.succ := n.lt_succ_self
          _ ≤ k := hnk
        have : k - n % 2^length α % length α > 0 :=
          Nat.lt_sub_of_add_lt (Nat.zero_add .. ▸ this)
        rw [UInt.getBit_one, decide_eq_false (Nat.ne_of_gt this), Bool.and_false]
      simp only [this, Bool.and_false]
    case false =>
      exact UInt.when_false_eq (α:=α) .. ▸ UInt.getBit_zero (α:=α) k
suffices ∀ (n : Nat), n < length α → ∀ (k : Nat), k < n → UInt.getBit (Nat.fold f n 0) k = i.getBit k by
  have what_is_shown :=
    this (Nat.log2RU $ length α) (Nat.log2RU_lt_self _ ‹0 < length α›)
  apply Nat.bitext; intro k
  cases Nat.lt_or_ge k (Nat.log2RU $ length α)
  case a.inl hlt => exact what_is_shown k hlt
  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 _
intro n hn k hk
induction n generalizing k
case zero => cases hk
case succ n h_ind =>
  unfold Nat.fold
  conv =>
    lhs; arg 1;
    change UInt.when (x &&& bitmask (OfNat.ofNat n) ≠ 0) ((1 : α) <<< OfNat.ofNat n) ||| Nat.fold f n 0
  rw [UInt.getBit_lor]
  have : n < length α := Nat.lt_of_succ_lt hn
  have : n < 2^length α := trans this (Nat.exp_lt_pow _ .refl)
  cases hk
  case step hlt =>
    rw [h_ind (Nat.lt_of_succ_lt hn) k hlt]
    cases decide (x &&& bitmask (OfNat.ofNat n) ≠ 0)
    case false => rw [UInt.when_false_eq, UInt.getBit_zero, Bool.false_or]
    case true =>
      simp only [
        UInt.when_true_eq, UInt.getBit_shiftLeft, UInt.toNat_ofNat,
        Nat.mod_eq_of_lt ‹n < 2^length α›,
        Nat.mod_eq_of_lt ‹n < length α›
      ]
      rw [decide_eq_false (Nat.not_le_of_lt hlt)]
      simp only [Bool.false_and, Bool.and_false, Bool.false_or]
  case refl =>
    rw [foldf_high n n .refl, Bool.or_false]
    have : ∀ b, UInt.getBit (UInt.when b ((1 : α) <<< OfNat.ofNat n)) n = b := by
      intro b; cases b
      case true =>
        simp only [
          UInt.when_true_eq, UInt.getBit_shiftLeft,
          UInt.toNat_ofNat,
          Nat.mod_eq_of_lt ‹n < 2^length α›,
          Nat.mod_eq_of_lt ‹n < length α›
        ]
        rw [decide_eq_true ‹n < length α›, decide_eq_true (p:=n≥n) .refl]
        rw [Nat.sub_self, UInt.getBit_one, decide_eq_true ‹0 < length α›, decide_eq_true rfl]
        simp only [Bool.true_and]
      case false => rw [UInt.when_false_eq, UInt.getBit_zero]
    rw [this]; clear this
    suffices ∀ y, decide ((x &&& y) ≠ 0) = UInt.getBit y i by
      rw [this]
      have hgetbit := UInt.getBit_bitmask (OfNat.ofNat (α:=α) n) i
      simp only [UInt.toNat_ofNat, Nat.mod_eq_of_lt ‹n < 2^length α›] at hgetbit
      rw [decide_eq_true ‹i < length α›, Bool.true_and] at hgetbit
      exact hgetbit ‹n < length α›
    intro y
    cases hyi : UInt.getBit y i
    case true =>
      apply decide_eq_true; intro hcontra
      have := calc
        true = (true && true) := rfl
        _    = (UInt.getBit x i && UInt.getBit y i) := by rw [hi i, decide_eq_true rfl, hyi]
        _    = UInt.getBit (x &&& y) i := by rw [UInt.getBit_land]
        _    = UInt.getBit (α:=α) 0 i := by rw [hcontra]
        _    = false := UInt.getBit_zero i
      cases this
    case false =>
      apply decide_eq_false; apply not_not_intro
      apply UInt.bitext; intro j hj
      rw [UInt.getBit_zero, UInt.getBit_land, hi j]
      if hij : i = j
      then cases hij; rw [hyi, Bool.and_false]
      else rw [decide_eq_false hij, Bool.false_and]
State after:
no goals

State before:
case intro
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a : α
ha : a ≠ 0
this : UInt.lsb a ≠ 0
i : Nat
hi : ∀ (j : Nat), UInt.getBit (UInt.lsb a) j = decide (i = j)
⊢ UInt.getBit (UInt.lsb a)
      (toNat
        (Nat.fold
          (fun n x => UInt.when (decide ¬UInt.lsb a &&& bitmask (OfNat.ofNat n) = 0) (1 <<< OfNat.ofNat n) ||| x)
          (Nat.log2RU (length α)) 0)) =
    true
Tactic:
generalize UInt.lsb a = x at *
State after:
case intro
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a : α
ha : a ≠ 0
i : Nat
x : α
this : x ≠ 0
hi : ∀ (j : Nat), UInt.getBit x j = decide (i = j)
⊢ UInt.getBit x
      (toNat
        (Nat.fold (fun n x_1 => UInt.when (decide ¬x &&& bitmask (OfNat.ofNat n) = 0) (1 <<< OfNat.ofNat n) ||| x_1)
          (Nat.log2RU (length α)) 0)) =
    true

State before:
case intro
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a : α
ha : a ≠ 0
i : Nat
x : α
this : x ≠ 0
hi : ∀ (j : Nat), UInt.getBit x j = decide (i = j)
⊢ UInt.getBit x
      (toNat
        (Nat.fold (fun n x_1 => UInt.when (decide ¬x &&& bitmask (OfNat.ofNat n) = 0) (1 <<< OfNat.ofNat n) ||| x_1)
          (Nat.log2RU (length α)) 0)) =
    true
Tactic:
clear ‹a≠0› a ‹x≠0›
State after:
case intro
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
i : Nat
x : α
hi : ∀ (j : Nat), UInt.getBit x j = decide (i = j)
⊢ UInt.getBit x
      (toNat
        (Nat.fold (fun n x_1 => UInt.when (decide ¬x &&& bitmask (OfNat.ofNat n) = 0) (1 <<< OfNat.ofNat n) ||| x_1)
          (Nat.log2RU (length α)) 0)) =
    true

State before:
case intro
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
i : Nat
x : α
hi : ∀ (j : Nat), UInt.getBit x j = decide (i = j)
⊢ UInt.getBit x
      (toNat
        (Nat.fold (fun n x_1 => UInt.when (decide ¬x &&& bitmask (OfNat.ofNat n) = 0) (1 <<< OfNat.ofNat n) ||| x_1)
          (Nat.log2RU (length α)) 0)) =
    true
Tactic:
let f (i : Nat) (y : α) : α := UInt.when (x &&& bitmask (OfNat.ofNat i) ≠ 0) ((1 : α) <<< OfNat.ofNat i) ||| y
State after:
case intro
α : 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
⊢ UInt.getBit x
      (toNat
        (Nat.fold (fun n x_1 => UInt.when (decide ¬x &&& bitmask (OfNat.ofNat n) = 0) (1 <<< OfNat.ofNat n) ||| x_1)
          (Nat.log2RU (length α)) 0)) =
    true

State before:
case intro
α : 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
⊢ UInt.getBit x
      (toNat
        (Nat.fold (fun n x_1 => UInt.when (decide ¬x &&& bitmask (OfNat.ofNat n) = 0) (1 <<< OfNat.ofNat n) ||| x_1)
          (Nat.log2RU (length α)) 0)) =
    true
Tactic:
conv =>
  change UInt.getBit x (toNat $ Nat.fold f (Nat.log2RU $ length α) 0) = true
State after:
case intro
α : 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
⊢ UInt.getBit x (toNat (Nat.fold f (Nat.log2RU (length α)) 0)) = true

State before:
case intro
α : 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
⊢ UInt.getBit x (toNat (Nat.fold f (Nat.log2RU (length α)) 0)) = true
Tactic:
have : UInt.getBit x i = true := (decide_eq_true (Eq.refl i) ▸ hi i)
State after:
case intro
α : 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
⊢ UInt.getBit x (toNat (Nat.fold f (Nat.log2RU (length α)) 0)) = true

State before:
case intro
α : 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
⊢ UInt.getBit x (toNat (Nat.fold f (Nat.log2RU (length α)) 0)) = true
Tactic:
have : i < length α := by
  cases Nat.lt_or_ge i (length α)
  case inl hlt => exact hlt
  case inr hge =>
    have := calc
      false = UInt.getBit x i := (UInt.getBit_high x i hge).symm
      _     = true := ‹_›
    cases this
State after:
case intro
α : 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 α
⊢ UInt.getBit x (toNat (Nat.fold f (Nat.log2RU (length α)) 0)) = true

State before:
case intro
α : 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 α
⊢ UInt.getBit x (toNat (Nat.fold f (Nat.log2RU (length α)) 0)) = true
Tactic:
have : 0 < length α := trans i.zero_le ‹i < length α›
State after:
case intro
α : 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 α
⊢ UInt.getBit x (toNat (Nat.fold f (Nat.log2RU (length α)) 0)) = true

State before:
case intro
α : 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 α
⊢ UInt.getBit x (toNat (Nat.fold f (Nat.log2RU (length α)) 0)) = true
Tactic:
suffices UInt.toNat (Nat.fold f (Nat.log2RU $ length α) 0) = i
  by rw [this]; assumption
State after:
case intro
α : 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 α
⊢ toNat (Nat.fold f (Nat.log2RU (length α)) 0) = i

State before:
case intro
α : 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 α
⊢ toNat (Nat.fold f (Nat.log2RU (length α)) 0) = i
Tactic:
have foldf_high : ∀ (n k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false := by
  intro n k hnk
  induction n generalizing k
  case zero => dsimp [Nat.fold]; exact UInt.getBit_zero k
  case succ n h_ind =>
    dsimp [Nat.fold]
    rw [UInt.getBit_lor, h_ind k (Nat.le_of_succ_le hnk), Bool.or_false]
    cases decide (x &&& bitmask (OfNat.ofNat n) ≠ 0)
    case true =>
      rw [UInt.when_true_eq, UInt.getBit_shiftLeft]
      have : UInt.getBit (1 : α) (k - toNat (OfNat.ofNat (α:=α) n) % length α) = false := by
        rw [UInt.toNat_ofNat]
        have := calc
          n % 2^length α % length α
            ≤ n % 2^length α := Nat.mod_le ..
          _ ≤ n := Nat.mod_le ..
          _ < n.succ := n.lt_succ_self
          _ ≤ k := hnk
        have : k - n % 2^length α % length α > 0 :=
          Nat.lt_sub_of_add_lt (Nat.zero_add .. ▸ this)
        rw [UInt.getBit_one, decide_eq_false (Nat.ne_of_gt this), Bool.and_false]
      simp only [this, Bool.and_false]
    case false =>
      exact UInt.when_false_eq (α:=α) .. ▸ UInt.getBit_zero (α:=α) k
State after:
case intro
α : 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
⊢ toNat (Nat.fold f (Nat.log2RU (length α)) 0) = i

State before:
case intro
α : 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
⊢ toNat (Nat.fold f (Nat.log2RU (length α)) 0) = i
Tactic:
suffices ∀ (n : Nat), n < length α → ∀ (k : Nat), k < n → UInt.getBit (Nat.fold f n 0) k = i.getBit k by
  have what_is_shown :=
    this (Nat.log2RU $ length α) (Nat.log2RU_lt_self _ ‹0 < length α›)
  apply Nat.bitext; intro k
  cases Nat.lt_or_ge k (Nat.log2RU $ length α)
  case a.inl hlt => exact what_is_shown k hlt
  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 _
State after:
case intro
α : 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), n < length α → ∀ (k : Nat), k < n → UInt.getBit (Nat.fold f n 0) k = Nat.getBit i k

State before:
case intro
α : 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), n < length α → ∀ (k : Nat), k < n → UInt.getBit (Nat.fold f n 0) k = Nat.getBit i k
Tactic:
intro n hn k hk
State after:
case intro
α : 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
hn : n < length α
k : Nat
hk : k < n
⊢ UInt.getBit (Nat.fold f n 0) k = Nat.getBit i k

State before:
case intro
α : 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
hn : n < length α
k : Nat
hk : k < n
⊢ UInt.getBit (Nat.fold f n 0) k = Nat.getBit i k
Tactic:
induction n generalizing k
State after:
case intro.zero
α : 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

case intro.succ
α : 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
n_ih✝ : 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

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:
case zero => cases hk
State after:
no goals

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:
case succ n h_ind =>
  unfold Nat.fold
  conv =>
    lhs; arg 1;
    change UInt.when (x &&& bitmask (OfNat.ofNat n) ≠ 0) ((1 : α) <<< OfNat.ofNat n) ||| Nat.fold f n 0
  rw [UInt.getBit_lor]
  have : n < length α := Nat.lt_of_succ_lt hn
  have : n < 2^length α := trans this (Nat.exp_lt_pow _ .refl)
  cases hk
  case step hlt =>
    rw [h_ind (Nat.lt_of_succ_lt hn) k hlt]
    cases decide (x &&& bitmask (OfNat.ofNat n) ≠ 0)
    case false => rw [UInt.when_false_eq, UInt.getBit_zero, Bool.false_or]
    case true =>
      simp only [
        UInt.when_true_eq, UInt.getBit_shiftLeft, UInt.toNat_ofNat,
        Nat.mod_eq_of_lt ‹n < 2^length α›,
        Nat.mod_eq_of_lt ‹n < length α›
      ]
      rw [decide_eq_false (Nat.not_le_of_lt hlt)]
      simp only [Bool.false_and, Bool.and_false, Bool.false_or]
  case refl =>
    rw [foldf_high n n .refl, Bool.or_false]
    have : ∀ b, UInt.getBit (UInt.when b ((1 : α) <<< OfNat.ofNat n)) n = b := by
      intro b; cases b
      case true =>
        simp only [
          UInt.when_true_eq, UInt.getBit_shiftLeft,
          UInt.toNat_ofNat,
          Nat.mod_eq_of_lt ‹n < 2^length α›,
          Nat.mod_eq_of_lt ‹n < length α›
        ]
        rw [decide_eq_true ‹n < length α›, decide_eq_true (p:=n≥n) .refl]
        rw [Nat.sub_self, UInt.getBit_one, decide_eq_true ‹0 < length α›, decide_eq_true rfl]
        simp only [Bool.true_and]
      case false => rw [UInt.when_false_eq, UInt.getBit_zero]
    rw [this]; clear this
    suffices ∀ y, decide ((x &&& y) ≠ 0) = UInt.getBit y i by
      rw [this]
      have hgetbit := UInt.getBit_bitmask (OfNat.ofNat (α:=α) n) i
      simp only [UInt.toNat_ofNat, Nat.mod_eq_of_lt ‹n < 2^length α›] at hgetbit
      rw [decide_eq_true ‹i < length α›, Bool.true_and] at hgetbit
      exact hgetbit ‹n < length α›
    intro y
    cases hyi : UInt.getBit y i
    case true =>
      apply decide_eq_true; intro hcontra
      have := calc
        true = (true && true) := rfl
        _    = (UInt.getBit x i && UInt.getBit y i) := by rw [hi i, decide_eq_true rfl, hyi]
        _    = UInt.getBit (x &&& y) i := by rw [UInt.getBit_land]
        _    = UInt.getBit (α:=α) 0 i := by rw [hcontra]
        _    = false := UInt.getBit_zero i
      cases this
    case false =>
      apply decide_eq_false; apply not_not_intro
      apply UInt.bitext; intro j hj
      rw [UInt.getBit_zero, UInt.getBit_land, hi j]
      if hij : i = j
      then cases hij; rw [hyi, Bool.and_false]
      else rw [decide_eq_false hij, Bool.false_and]
State after:
no goals

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
⊢ i < length α
Tactic:
cases Nat.lt_or_ge i (length α)
State after:
case 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
h✝ : i < length α
⊢ i < length α

case 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
h✝ : i ≥ length α
⊢ i < length α

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
hlt : i < length α
⊢ i < length α
Tactic:
case inl hlt => exact hlt
State after:
no goals

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
hge : i ≥ length α
⊢ i < length α
Tactic:
case inr hge =>
  have := calc
    false = UInt.getBit x i := (UInt.getBit_high x i hge).symm
    _     = true := ‹_›
  cases this
State after:
no goals

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
hlt : i < length α
⊢ i < length α
Tactic:
exact hlt
State after:
no goals

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
hge : i ≥ length α
⊢ i < length α
Tactic:
have := calc
  false = UInt.getBit x i := (UInt.getBit_high x i hge).symm
  _     = true := ‹_›
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
hge : i ≥ length α
this : false = true
⊢ i < length α

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
hge : i ≥ length α
this : false = true
⊢ i < length α
Tactic:
cases this
State after:
no goals

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 α
this : toNat (Nat.fold f (Nat.log2RU (length α)) 0) = i
⊢ UInt.getBit x (toNat (Nat.fold f (Nat.log2RU (length α)) 0)) = true
Tactic:
rw [this]
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 α
this : toNat (Nat.fold f (Nat.log2RU (length α)) 0) = i
⊢ UInt.getBit x i = true

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 α
this : toNat (Nat.fold f (Nat.log2RU (length α)) 0) = i
⊢ UInt.getBit x i = true
Tactic:
assumption
State after:
no goals

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 α
⊢ ∀ (n k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
Tactic:
intro n k hnk
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 α
n k : Nat
hnk : k ≥ n
⊢ UInt.getBit (Nat.fold f n 0) k = false

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 α
n k : Nat
hnk : k ≥ n
⊢ UInt.getBit (Nat.fold f n 0) k = false
Tactic:
induction n generalizing k
State after:
case zero
α : 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 α
k : Nat
hnk : k ≥ Nat.zero
⊢ UInt.getBit (Nat.fold f Nat.zero 0) k = false

case succ
α : 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 α
n✝ : Nat
n_ih✝ : ∀ (k : Nat), k ≥ n✝ → UInt.getBit (Nat.fold f n✝ 0) k = false
k : Nat
hnk : k ≥ Nat.succ n✝
⊢ UInt.getBit (Nat.fold f (Nat.succ n✝) 0) k = false

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 α
k : Nat
hnk : k ≥ Nat.zero
⊢ UInt.getBit (Nat.fold f Nat.zero 0) k = false
Tactic:
case zero => dsimp [Nat.fold]; exact UInt.getBit_zero k
State after:
no goals

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 α
n : Nat
h_ind : ∀ (k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
k : Nat
hnk : k ≥ Nat.succ n
⊢ UInt.getBit (Nat.fold f (Nat.succ n) 0) k = false
Tactic:
case succ n h_ind =>
  dsimp [Nat.fold]
  rw [UInt.getBit_lor, h_ind k (Nat.le_of_succ_le hnk), Bool.or_false]
  cases decide (x &&& bitmask (OfNat.ofNat n) ≠ 0)
  case true =>
    rw [UInt.when_true_eq, UInt.getBit_shiftLeft]
    have : UInt.getBit (1 : α) (k - toNat (OfNat.ofNat (α:=α) n) % length α) = false := by
      rw [UInt.toNat_ofNat]
      have := calc
        n % 2^length α % length α
          ≤ n % 2^length α := Nat.mod_le ..
        _ ≤ n := Nat.mod_le ..
        _ < n.succ := n.lt_succ_self
        _ ≤ k := hnk
      have : k - n % 2^length α % length α > 0 :=
        Nat.lt_sub_of_add_lt (Nat.zero_add .. ▸ this)
      rw [UInt.getBit_one, decide_eq_false (Nat.ne_of_gt this), Bool.and_false]
    simp only [this, Bool.and_false]
  case false =>
    exact UInt.when_false_eq (α:=α) .. ▸ UInt.getBit_zero (α:=α) k
State after:
no goals

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 α
k : Nat
hnk : k ≥ Nat.zero
⊢ UInt.getBit (Nat.fold f Nat.zero 0) k = false
Tactic:
dsimp [Nat.fold]
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 α
k : Nat
hnk : k ≥ Nat.zero
⊢ UInt.getBit 0 k = false

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 α
k : Nat
hnk : k ≥ Nat.zero
⊢ UInt.getBit 0 k = false
Tactic:
exact UInt.getBit_zero k
State after:
no goals

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 α
n : Nat
h_ind : ∀ (k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
k : Nat
hnk : k ≥ Nat.succ n
⊢ UInt.getBit (Nat.fold f (Nat.succ n) 0) k = false
Tactic:
dsimp [Nat.fold]
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 α
n : Nat
h_ind : ∀ (k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
k : Nat
hnk : k ≥ Nat.succ n
⊢ UInt.getBit
      (UInt.when (decide ¬x &&& bitmask (OfNat.ofNat n) = 0) (1 <<< OfNat.ofNat n) |||
        Nat.fold (fun i y => UInt.when (decide ¬x &&& bitmask (OfNat.ofNat i) = 0) (1 <<< OfNat.ofNat i) ||| y) n 0)
      k =
    false

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 α
n : Nat
h_ind : ∀ (k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
k : Nat
hnk : k ≥ Nat.succ n
⊢ UInt.getBit
      (UInt.when (decide ¬x &&& bitmask (OfNat.ofNat n) = 0) (1 <<< OfNat.ofNat n) |||
        Nat.fold (fun i y => UInt.when (decide ¬x &&& bitmask (OfNat.ofNat i) = 0) (1 <<< OfNat.ofNat i) ||| y) n 0)
      k =
    false
Tactic:
rw [UInt.getBit_lor, h_ind k (Nat.le_of_succ_le hnk), Bool.or_false]
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 α
n : Nat
h_ind : ∀ (k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
k : Nat
hnk : k ≥ Nat.succ n
⊢ UInt.getBit (UInt.when (decide ¬x &&& bitmask (OfNat.ofNat n) = 0) (1 <<< OfNat.ofNat n)) k = false

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 α
n : Nat
h_ind : ∀ (k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
k : Nat
hnk : k ≥ Nat.succ n
⊢ UInt.getBit (UInt.when (decide ¬x &&& bitmask (OfNat.ofNat n) = 0) (1 <<< OfNat.ofNat n)) k = false
Tactic:
cases decide (x &&& bitmask (OfNat.ofNat n) ≠ 0)
State after:
case false
α : 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 α
n : Nat
h_ind : ∀ (k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
k : Nat
hnk : k ≥ Nat.succ n
⊢ UInt.getBit (UInt.when false (1 <<< OfNat.ofNat n)) k = false

case true
α : 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 α
n : Nat
h_ind : ∀ (k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
k : Nat
hnk : k ≥ Nat.succ n
⊢ UInt.getBit (UInt.when true (1 <<< OfNat.ofNat n)) k = false

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 α
n : Nat
h_ind : ∀ (k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
k : Nat
hnk : k ≥ Nat.succ n
⊢ UInt.getBit (UInt.when true (1 <<< OfNat.ofNat n)) k = false
Tactic:
case true =>
  rw [UInt.when_true_eq, UInt.getBit_shiftLeft]
  have : UInt.getBit (1 : α) (k - toNat (OfNat.ofNat (α:=α) n) % length α) = false := by
    rw [UInt.toNat_ofNat]
    have := calc
      n % 2^length α % length α
        ≤ n % 2^length α := Nat.mod_le ..
      _ ≤ n := Nat.mod_le ..
      _ < n.succ := n.lt_succ_self
      _ ≤ k := hnk
    have : k - n % 2^length α % length α > 0 :=
      Nat.lt_sub_of_add_lt (Nat.zero_add .. ▸ this)
    rw [UInt.getBit_one, decide_eq_false (Nat.ne_of_gt this), Bool.and_false]
  simp only [this, Bool.and_false]
State after:
no goals

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 α
n : Nat
h_ind : ∀ (k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
k : Nat
hnk : k ≥ Nat.succ n
⊢ UInt.getBit (UInt.when false (1 <<< OfNat.ofNat n)) k = false
Tactic:
case false =>
  exact UInt.when_false_eq (α:=α) .. ▸ UInt.getBit_zero (α:=α) k
State after:
no goals

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 α
n : Nat
h_ind : ∀ (k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
k : Nat
hnk : k ≥ Nat.succ n
⊢ UInt.getBit (UInt.when true (1 <<< OfNat.ofNat n)) k = false
Tactic:
rw [UInt.when_true_eq, UInt.getBit_shiftLeft]
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 α
n : Nat
h_ind : ∀ (k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
k : Nat
hnk : k ≥ Nat.succ n
⊢ (decide (k < length α) && decide (k ≥ toNat (OfNat.ofNat n) % length α) &&
      UInt.getBit 1 (k - toNat (OfNat.ofNat n) % length α)) =
    false

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 α
n : Nat
h_ind : ∀ (k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
k : Nat
hnk : k ≥ Nat.succ n
⊢ (decide (k < length α) && decide (k ≥ toNat (OfNat.ofNat n) % length α) &&
      UInt.getBit 1 (k - toNat (OfNat.ofNat n) % length α)) =
    false
Tactic:
have : UInt.getBit (1 : α) (k - toNat (OfNat.ofNat (α:=α) n) % length α) = false := by
  rw [UInt.toNat_ofNat]
  have := calc
    n % 2^length α % length α
      ≤ n % 2^length α := Nat.mod_le ..
    _ ≤ n := Nat.mod_le ..
    _ < n.succ := n.lt_succ_self
    _ ≤ k := hnk
  have : k - n % 2^length α % length α > 0 :=
    Nat.lt_sub_of_add_lt (Nat.zero_add .. ▸ this)
  rw [UInt.getBit_one, decide_eq_false (Nat.ne_of_gt this), Bool.and_false]
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 α
n : Nat
h_ind : ∀ (k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
k : Nat
hnk : k ≥ Nat.succ n
this : UInt.getBit 1 (k - toNat (OfNat.ofNat n) % length α) = false
⊢ (decide (k < length α) && decide (k ≥ toNat (OfNat.ofNat n) % length α) &&
      UInt.getBit 1 (k - toNat (OfNat.ofNat n) % length α)) =
    false

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 α
n : Nat
h_ind : ∀ (k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
k : Nat
hnk : k ≥ Nat.succ n
this : UInt.getBit 1 (k - toNat (OfNat.ofNat n) % length α) = false
⊢ (decide (k < length α) && decide (k ≥ toNat (OfNat.ofNat n) % length α) &&
      UInt.getBit 1 (k - toNat (OfNat.ofNat n) % length α)) =
    false
Tactic:
simp only [this, Bool.and_false]
State after:
no goals

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 α
n : Nat
h_ind : ∀ (k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
k : Nat
hnk : k ≥ Nat.succ n
⊢ UInt.getBit 1 (k - toNat (OfNat.ofNat n) % length α) = false
Tactic:
rw [UInt.toNat_ofNat]
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 α
n : Nat
h_ind : ∀ (k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
k : Nat
hnk : k ≥ Nat.succ n
⊢ UInt.getBit 1 (k - n % 2 ^ length α % length α) = false

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 α
n : Nat
h_ind : ∀ (k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
k : Nat
hnk : k ≥ Nat.succ n
⊢ UInt.getBit 1 (k - n % 2 ^ length α % length α) = false
Tactic:
have := calc
  n % 2^length α % length α
    ≤ n % 2^length α := Nat.mod_le ..
  _ ≤ n := Nat.mod_le ..
  _ < n.succ := n.lt_succ_self
  _ ≤ k := hnk
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 α
n : Nat
h_ind : ∀ (k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
k : Nat
hnk : k ≥ Nat.succ n
this : n % 2 ^ length α % length α < k
⊢ UInt.getBit 1 (k - n % 2 ^ length α % length α) = false

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 α
n : Nat
h_ind : ∀ (k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
k : Nat
hnk : k ≥ Nat.succ n
this : n % 2 ^ length α % length α < k
⊢ UInt.getBit 1 (k - n % 2 ^ length α % length α) = false
Tactic:
have : k - n % 2^length α % length α > 0 :=
  Nat.lt_sub_of_add_lt (Nat.zero_add .. ▸ this)
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 α
n : Nat
h_ind : ∀ (k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
k : Nat
hnk : k ≥ Nat.succ n
this✝ : n % 2 ^ length α % length α < k
this : k - n % 2 ^ length α % length α > 0
⊢ UInt.getBit 1 (k - n % 2 ^ length α % length α) = false

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 α
n : Nat
h_ind : ∀ (k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
k : Nat
hnk : k ≥ Nat.succ n
this✝ : n % 2 ^ length α % length α < k
this : k - n % 2 ^ length α % length α > 0
⊢ UInt.getBit 1 (k - n % 2 ^ length α % length α) = false
Tactic:
rw [UInt.getBit_one, decide_eq_false (Nat.ne_of_gt this), Bool.and_false]
State after:
no goals

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 α
n : Nat
h_ind : ∀ (k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
k : Nat
hnk : k ≥ Nat.succ n
⊢ UInt.getBit (UInt.when false (1 <<< OfNat.ofNat n)) k = false
Tactic:
exact UInt.when_false_eq (α:=α) .. ▸ UInt.getBit_zero (α:=α) k
State after:
no goals

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
⊢ toNat (Nat.fold f (Nat.log2RU (length α)) 0) = i
Tactic:
have what_is_shown :=
  this (Nat.log2RU $ length α) (Nat.log2RU_lt_self _ ‹0 < length α›)
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
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
⊢ toNat (Nat.fold f (Nat.log2RU (length α)) 0) = i

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
⊢ toNat (Nat.fold f (Nat.log2RU (length α)) 0) = i
Tactic:
apply Nat.bitext
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
⊢ ∀ (i_1 : Nat), Nat.getBit (toNat (Nat.fold f (Nat.log2RU (length α)) 0)) i_1 = Nat.getBit i i_1

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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 α
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
Tactic:
cases hk
State after:
case refl
α : 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 α
this✝ : n < length α
this : n < 2 ^ length α
⊢ (UInt.getBit (UInt.when (decide (x &&& bitmask (OfNat.ofNat n) ≠ 0)) (1 <<< OfNat.ofNat n)) n ||
      UInt.getBit (Nat.fold f n 0) n) =
    Nat.getBit i n

case step
α : 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
this✝ : n < length α
this : n < 2 ^ length α
a✝ : Nat.le (Nat.succ k) 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

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
this✝ : n < length α
this : n < 2 ^ length α
hlt : Nat.le (Nat.succ k) 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:
case step hlt =>
  rw [h_ind (Nat.lt_of_succ_lt hn) k hlt]
  cases decide (x &&& bitmask (OfNat.ofNat n) ≠ 0)
  case false => rw [UInt.when_false_eq, UInt.getBit_zero, Bool.false_or]
  case true =>
    simp only [
      UInt.when_true_eq, UInt.getBit_shiftLeft, UInt.toNat_ofNat,
      Nat.mod_eq_of_lt ‹n < 2^length α›,
      Nat.mod_eq_of_lt ‹n < length α›
    ]
    rw [decide_eq_false (Nat.not_le_of_lt hlt)]
    simp only [Bool.false_and, Bool.and_false, Bool.false_or]
State after:
no goals

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 α
this✝ : n < length α
this : n < 2 ^ length α
⊢ (UInt.getBit (UInt.when (decide (x &&& bitmask (OfNat.ofNat n) ≠ 0)) (1 <<< OfNat.ofNat n)) n ||
      UInt.getBit (Nat.fold f n 0) n) =
    Nat.getBit i n
Tactic:
case refl =>
  rw [foldf_high n n .refl, Bool.or_false]
  have : ∀ b, UInt.getBit (UInt.when b ((1 : α) <<< OfNat.ofNat n)) n = b := by
    intro b; cases b
    case true =>
      simp only [
        UInt.when_true_eq, UInt.getBit_shiftLeft,
        UInt.toNat_ofNat,
        Nat.mod_eq_of_lt ‹n < 2^length α›,
        Nat.mod_eq_of_lt ‹n < length α›
      ]
      rw [decide_eq_true ‹n < length α›, decide_eq_true (p:=n≥n) .refl]
      rw [Nat.sub_self, UInt.getBit_one, decide_eq_true ‹0 < length α›, decide_eq_true rfl]
      simp only [Bool.true_and]
    case false => rw [UInt.when_false_eq, UInt.getBit_zero]
  rw [this]; clear this
  suffices ∀ y, decide ((x &&& y) ≠ 0) = UInt.getBit y i by
    rw [this]
    have hgetbit := UInt.getBit_bitmask (OfNat.ofNat (α:=α) n) i
    simp only [UInt.toNat_ofNat, Nat.mod_eq_of_lt ‹n < 2^length α›] at hgetbit
    rw [decide_eq_true ‹i < length α›, Bool.true_and] at hgetbit
    exact hgetbit ‹n < length α›
  intro y
  cases hyi : UInt.getBit y i
  case true =>
    apply decide_eq_true; intro hcontra
    have := calc
      true = (true && true) := rfl
      _    = (UInt.getBit x i && UInt.getBit y i) := by rw [hi i, decide_eq_true rfl, hyi]
      _    = UInt.getBit (x &&& y) i := by rw [UInt.getBit_land]
      _    = UInt.getBit (α:=α) 0 i := by rw [hcontra]
      _    = false := UInt.getBit_zero i
    cases this
  case false =>
    apply decide_eq_false; apply not_not_intro
    apply UInt.bitext; intro j hj
    rw [UInt.getBit_zero, UInt.getBit_land, hi j]
    if hij : i = j
    then cases hij; rw [hyi, Bool.and_false]
    else rw [decide_eq_false hij, Bool.false_and]
State after:
no goals

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
this✝ : n < length α
this : n < 2 ^ length α
hlt : Nat.le (Nat.succ k) 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:
rw [h_ind (Nat.lt_of_succ_lt hn) k hlt]
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
this✝ : n < length α
this : n < 2 ^ length α
hlt : Nat.le (Nat.succ k) n
⊢ (UInt.getBit (UInt.when (decide (x &&& bitmask (OfNat.ofNat n) ≠ 0)) (1 <<< OfNat.ofNat n)) k || Nat.getBit i k) =
    Nat.getBit i k

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
this✝ : n < length α
this : n < 2 ^ length α
hlt : Nat.le (Nat.succ k) n
⊢ (UInt.getBit (UInt.when (decide (x &&& bitmask (OfNat.ofNat n) ≠ 0)) (1 <<< OfNat.ofNat n)) k || Nat.getBit i k) =
    Nat.getBit i k
Tactic:
cases decide (x &&& bitmask (OfNat.ofNat n) ≠ 0)
State after:
case false
α : 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
this✝ : n < length α
this : n < 2 ^ length α
hlt : Nat.le (Nat.succ k) n
⊢ (UInt.getBit (UInt.when false (1 <<< OfNat.ofNat n)) k || Nat.getBit i k) = Nat.getBit i k

case true
α : 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
this✝ : n < length α
this : n < 2 ^ length α
hlt : Nat.le (Nat.succ k) n
⊢ (UInt.getBit (UInt.when true (1 <<< OfNat.ofNat n)) k || Nat.getBit i k) = Nat.getBit i k

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
this✝ : n < length α
this : n < 2 ^ length α
hlt : Nat.le (Nat.succ k) n
⊢ (UInt.getBit (UInt.when false (1 <<< OfNat.ofNat n)) k || Nat.getBit i k) = Nat.getBit i k
Tactic:
case false => rw [UInt.when_false_eq, UInt.getBit_zero, Bool.false_or]
State after:
no goals

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
this✝ : n < length α
this : n < 2 ^ length α
hlt : Nat.le (Nat.succ k) n
⊢ (UInt.getBit (UInt.when true (1 <<< OfNat.ofNat n)) k || Nat.getBit i k) = Nat.getBit i k
Tactic:
case true =>
  simp only [
    UInt.when_true_eq, UInt.getBit_shiftLeft, UInt.toNat_ofNat,
    Nat.mod_eq_of_lt ‹n < 2^length α›,
    Nat.mod_eq_of_lt ‹n < length α›
  ]
  rw [decide_eq_false (Nat.not_le_of_lt hlt)]
  simp only [Bool.false_and, Bool.and_false, Bool.false_or]
State after:
no goals

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
this✝ : n < length α
this : n < 2 ^ length α
hlt : Nat.le (Nat.succ k) n
⊢ (UInt.getBit (UInt.when false (1 <<< OfNat.ofNat n)) k || Nat.getBit i k) = Nat.getBit i k
Tactic:
rw [UInt.when_false_eq, UInt.getBit_zero, Bool.false_or]
State after:
no goals

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
this✝ : n < length α
this : n < 2 ^ length α
hlt : Nat.le (Nat.succ k) n
⊢ (UInt.getBit (UInt.when true (1 <<< OfNat.ofNat n)) k || Nat.getBit i k) = Nat.getBit i k
Tactic:
simp only [
  UInt.when_true_eq, UInt.getBit_shiftLeft, UInt.toNat_ofNat,
  Nat.mod_eq_of_lt ‹n < 2^length α›,
  Nat.mod_eq_of_lt ‹n < length α›
]
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
this✝ : n < length α
this : n < 2 ^ length α
hlt : Nat.le (Nat.succ k) n
⊢ (decide (k < length α) && decide (k ≥ n) && UInt.getBit 1 (k - n) || Nat.getBit i k) = Nat.getBit i k

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
this✝ : n < length α
this : n < 2 ^ length α
hlt : Nat.le (Nat.succ k) n
⊢ (decide (k < length α) && decide (k ≥ n) && UInt.getBit 1 (k - n) || Nat.getBit i k) = Nat.getBit i k
Tactic:
rw [decide_eq_false (Nat.not_le_of_lt hlt)]
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
this✝ : n < length α
this : n < 2 ^ length α
hlt : Nat.le (Nat.succ k) n
⊢ (decide (k < length α) && false && UInt.getBit 1 (k - n) || Nat.getBit i k) = Nat.getBit i k

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
this✝ : n < length α
this : n < 2 ^ length α
hlt : Nat.le (Nat.succ k) n
⊢ (decide (k < length α) && false && UInt.getBit 1 (k - n) || Nat.getBit i k) = Nat.getBit i k
Tactic:
simp only [Bool.false_and, Bool.and_false, Bool.false_or]
State after:
no goals

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 α
this✝ : n < length α
this : n < 2 ^ length α
⊢ (UInt.getBit (UInt.when (decide (x &&& bitmask (OfNat.ofNat n) ≠ 0)) (1 <<< OfNat.ofNat n)) n ||
      UInt.getBit (Nat.fold f n 0) n) =
    Nat.getBit i n
Tactic:
rw [foldf_high n n .refl, Bool.or_false]
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 α
this✝ : n < length α
this : n < 2 ^ length α
⊢ UInt.getBit (UInt.when (decide (x &&& bitmask (OfNat.ofNat n) ≠ 0)) (1 <<< OfNat.ofNat n)) n = Nat.getBit i n

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 α
this✝ : n < length α
this : n < 2 ^ length α
⊢ UInt.getBit (UInt.when (decide (x &&& bitmask (OfNat.ofNat n) ≠ 0)) (1 <<< OfNat.ofNat n)) n = Nat.getBit i n
Tactic:
have : ∀ b, UInt.getBit (UInt.when b ((1 : α) <<< OfNat.ofNat n)) n = b := by
  intro b; cases b
  case true =>
    simp only [
      UInt.when_true_eq, UInt.getBit_shiftLeft,
      UInt.toNat_ofNat,
      Nat.mod_eq_of_lt ‹n < 2^length α›,
      Nat.mod_eq_of_lt ‹n < length α›
    ]
    rw [decide_eq_true ‹n < length α›, decide_eq_true (p:=n≥n) .refl]
    rw [Nat.sub_self, UInt.getBit_one, decide_eq_true ‹0 < length α›, decide_eq_true rfl]
    simp only [Bool.true_and]
  case false => rw [UInt.when_false_eq, UInt.getBit_zero]
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 α
this✝¹ : n < length α
this✝ : n < 2 ^ length α
this : ∀ (b : Bool), UInt.getBit (UInt.when b (1 <<< OfNat.ofNat n)) n = b
⊢ UInt.getBit (UInt.when (decide (x &&& bitmask (OfNat.ofNat n) ≠ 0)) (1 <<< OfNat.ofNat n)) n = Nat.getBit i n

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 α
this✝¹ : n < length α
this✝ : n < 2 ^ length α
this : ∀ (b : Bool), UInt.getBit (UInt.when b (1 <<< OfNat.ofNat n)) n = b
⊢ UInt.getBit (UInt.when (decide (x &&& bitmask (OfNat.ofNat n) ≠ 0)) (1 <<< OfNat.ofNat n)) n = Nat.getBit i n
Tactic:
rw [this]
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 α
this✝¹ : n < length α
this✝ : n < 2 ^ length α
this : ∀ (b : Bool), UInt.getBit (UInt.when b (1 <<< OfNat.ofNat n)) n = b
⊢ decide (x &&& bitmask (OfNat.ofNat n) ≠ 0) = Nat.getBit i n

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 α
this✝¹ : n < length α
this✝ : n < 2 ^ length α
this : ∀ (b : Bool), UInt.getBit (UInt.when b (1 <<< OfNat.ofNat n)) n = b
⊢ decide (x &&& bitmask (OfNat.ofNat n) ≠ 0) = Nat.getBit i n
Tactic:
clear this
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 α
this✝ : n < length α
this : n < 2 ^ length α
⊢ decide (x &&& bitmask (OfNat.ofNat n) ≠ 0) = Nat.getBit i n

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 α
this✝ : n < length α
this : n < 2 ^ length α
⊢ decide (x &&& bitmask (OfNat.ofNat n) ≠ 0) = Nat.getBit i n
Tactic:
suffices ∀ y, decide ((x &&& y) ≠ 0) = UInt.getBit y i by
  rw [this]
  have hgetbit := UInt.getBit_bitmask (OfNat.ofNat (α:=α) n) i
  simp only [UInt.toNat_ofNat, Nat.mod_eq_of_lt ‹n < 2^length α›] at hgetbit
  rw [decide_eq_true ‹i < length α›, Bool.true_and] at hgetbit
  exact hgetbit ‹n < length α›
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 α
this✝ : n < length α
this : n < 2 ^ length α
⊢ ∀ (y : α), decide (x &&& y ≠ 0) = UInt.getBit y i

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 α
this✝ : n < length α
this : n < 2 ^ length α
⊢ ∀ (y : α), decide (x &&& y ≠ 0) = UInt.getBit y i
Tactic:
intro y
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 α
this✝ : n < length α
this : n < 2 ^ length α
y : α
⊢ decide (x &&& y ≠ 0) = UInt.getBit y i

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 α
this✝ : n < length α
this : n < 2 ^ length α
y : α
⊢ decide (x &&& y ≠ 0) = UInt.getBit y i
Tactic:
cases hyi : UInt.getBit y i
State after:
case false
α : 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 α
this✝ : n < length α
this : n < 2 ^ length α
y : α
hyi : UInt.getBit y i = false
⊢ decide (x &&& y ≠ 0) = false

case true
α : 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 α
this✝ : n < length α
this : n < 2 ^ length α
y : α
hyi : UInt.getBit y i = true
⊢ decide (x &&& y ≠ 0) = true

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 α
this✝ : n < length α
this : n < 2 ^ length α
y : α
hyi : UInt.getBit y i = true
⊢ decide (x &&& y ≠ 0) = true
Tactic:
case true =>
  apply decide_eq_true; intro hcontra
  have := calc
    true = (true && true) := rfl
    _    = (UInt.getBit x i && UInt.getBit y i) := by rw [hi i, decide_eq_true rfl, hyi]
    _    = UInt.getBit (x &&& y) i := by rw [UInt.getBit_land]
    _    = UInt.getBit (α:=α) 0 i := by rw [hcontra]
    _    = false := UInt.getBit_zero i
  cases this
State after:
no goals

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 α
this✝ : n < length α
this : n < 2 ^ length α
y : α
hyi : UInt.getBit y i = false
⊢ decide (x &&& y ≠ 0) = false
Tactic:
case false =>
  apply decide_eq_false; apply not_not_intro
  apply UInt.bitext; intro j hj
  rw [UInt.getBit_zero, UInt.getBit_land, hi j]
  if hij : i = j
  then cases hij; rw [hyi, Bool.and_false]
  else rw [decide_eq_false hij, Bool.false_and]
State after:
no goals

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 α
this✝ : n < length α
this : n < 2 ^ length α
⊢ ∀ (b : Bool), UInt.getBit (UInt.when b (1 <<< OfNat.ofNat n)) n = b
Tactic:
intro b
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 α
this✝ : n < length α
this : n < 2 ^ length α
b : Bool
⊢ UInt.getBit (UInt.when b (1 <<< OfNat.ofNat n)) n = b

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 α
this✝ : n < length α
this : n < 2 ^ length α
b : Bool
⊢ UInt.getBit (UInt.when b (1 <<< OfNat.ofNat n)) n = b
Tactic:
cases b
State after:
case false
α : 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 α
this✝ : n < length α
this : n < 2 ^ length α
⊢ UInt.getBit (UInt.when false (1 <<< OfNat.ofNat n)) n = false

case true
α : 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 α
this✝ : n < length α
this : n < 2 ^ length α
⊢ UInt.getBit (UInt.when true (1 <<< OfNat.ofNat n)) n = true

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 α
this✝ : n < length α
this : n < 2 ^ length α
⊢ UInt.getBit (UInt.when true (1 <<< OfNat.ofNat n)) n = true
Tactic:
case true =>
  simp only [
    UInt.when_true_eq, UInt.getBit_shiftLeft,
    UInt.toNat_ofNat,
    Nat.mod_eq_of_lt ‹n < 2^length α›,
    Nat.mod_eq_of_lt ‹n < length α›
  ]
  rw [decide_eq_true ‹n < length α›, decide_eq_true (p:=n≥n) .refl]
  rw [Nat.sub_self, UInt.getBit_one, decide_eq_true ‹0 < length α›, decide_eq_true rfl]
  simp only [Bool.true_and]
State after:
no goals

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 α
this✝ : n < length α
this : n < 2 ^ length α
⊢ UInt.getBit (UInt.when false (1 <<< OfNat.ofNat n)) n = false
Tactic:
case false => rw [UInt.when_false_eq, UInt.getBit_zero]
State after:
no goals

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 α
this✝ : n < length α
this : n < 2 ^ length α
⊢ UInt.getBit (UInt.when true (1 <<< OfNat.ofNat n)) n = true
Tactic:
simp only [
  UInt.when_true_eq, UInt.getBit_shiftLeft,
  UInt.toNat_ofNat,
  Nat.mod_eq_of_lt ‹n < 2^length α›,
  Nat.mod_eq_of_lt ‹n < length α›
]
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 α
this✝ : n < length α
this : n < 2 ^ length α
⊢ (decide (n < length α) && decide (n ≥ n) && UInt.getBit 1 (n - n)) = true

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 α
this✝ : n < length α
this : n < 2 ^ length α
⊢ (decide (n < length α) && decide (n ≥ n) && UInt.getBit 1 (n - n)) = true
Tactic:
rw [decide_eq_true ‹n < length α›, decide_eq_true (p:=n≥n) .refl]
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 α
this✝ : n < length α
this : n < 2 ^ length α
⊢ (true && true && UInt.getBit 1 (n - n)) = true

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 α
this✝ : n < length α
this : n < 2 ^ length α
⊢ (true && true && UInt.getBit 1 (n - n)) = true
Tactic:
rw [Nat.sub_self, UInt.getBit_one, decide_eq_true ‹0 < length α›, decide_eq_true rfl]
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 α
this✝ : n < length α
this : n < 2 ^ length α
⊢ (true && true && (true && true)) = true

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 α
this✝ : n < length α
this : n < 2 ^ length α
⊢ (true && true && (true && true)) = true
Tactic:
simp only [Bool.true_and]
State after:
no goals

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 α
this✝ : n < length α
this : n < 2 ^ length α
⊢ UInt.getBit (UInt.when false (1 <<< OfNat.ofNat n)) n = false
Tactic:
rw [UInt.when_false_eq, UInt.getBit_zero]
State after:
no goals

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 α
this✝¹ : n < length α
this✝ : n < 2 ^ length α
this : ∀ (y : α), decide (x &&& y ≠ 0) = UInt.getBit y i
⊢ decide (x &&& bitmask (OfNat.ofNat n) ≠ 0) = Nat.getBit i n
Tactic:
rw [this]
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 α
this✝¹ : n < length α
this✝ : n < 2 ^ length α
this : ∀ (y : α), decide (x &&& y ≠ 0) = UInt.getBit y i
⊢ UInt.getBit (bitmask (OfNat.ofNat n)) i = Nat.getBit i n

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 α
this✝¹ : n < length α
this✝ : n < 2 ^ length α
this : ∀ (y : α), decide (x &&& y ≠ 0) = UInt.getBit y i
⊢ UInt.getBit (bitmask (OfNat.ofNat n)) i = Nat.getBit i n
Tactic:
have hgetbit := UInt.getBit_bitmask (OfNat.ofNat (α:=α) n) i
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 α
this✝¹ : n < length α
this✝ : n < 2 ^ length α
this : ∀ (y : α), decide (x &&& y ≠ 0) = UInt.getBit y i
hgetbit :
  toNat (OfNat.ofNat n) < length α →
    UInt.getBit (bitmask (OfNat.ofNat n)) i = (decide (i < length α) && Nat.getBit i (toNat (OfNat.ofNat n)))
⊢ UInt.getBit (bitmask (OfNat.ofNat n)) i = Nat.getBit i n

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 α
this✝¹ : n < length α
this✝ : n < 2 ^ length α
this : ∀ (y : α), decide (x &&& y ≠ 0) = UInt.getBit y i
hgetbit :
  toNat (OfNat.ofNat n) < length α →
    UInt.getBit (bitmask (OfNat.ofNat n)) i = (decide (i < length α) && Nat.getBit i (toNat (OfNat.ofNat n)))
⊢ UInt.getBit (bitmask (OfNat.ofNat n)) i = Nat.getBit i n
Tactic:
simp only [UInt.toNat_ofNat, Nat.mod_eq_of_lt ‹n < 2^length α›] at hgetbit
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 α
this✝¹ : n < length α
this✝ : n < 2 ^ length α
this : ∀ (y : α), decide (x &&& y ≠ 0) = UInt.getBit y i
hgetbit : n < length α → UInt.getBit (bitmask (OfNat.ofNat n)) i = (decide (i < length α) && Nat.getBit i n)
⊢ UInt.getBit (bitmask (OfNat.ofNat n)) i = Nat.getBit i n

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 α
this✝¹ : n < length α
this✝ : n < 2 ^ length α
this : ∀ (y : α), decide (x &&& y ≠ 0) = UInt.getBit y i
hgetbit : n < length α → UInt.getBit (bitmask (OfNat.ofNat n)) i = (decide (i < length α) && Nat.getBit i n)
⊢ UInt.getBit (bitmask (OfNat.ofNat n)) i = Nat.getBit i n
Tactic:
rw [decide_eq_true ‹i < length α›, Bool.true_and] at hgetbit
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 α
this✝¹ : n < length α
this✝ : n < 2 ^ length α
this : ∀ (y : α), decide (x &&& y ≠ 0) = UInt.getBit y i
hgetbit : n < length α → UInt.getBit (bitmask (OfNat.ofNat n)) i = Nat.getBit i n
⊢ UInt.getBit (bitmask (OfNat.ofNat n)) i = Nat.getBit i n

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 α
this✝¹ : n < length α
this✝ : n < 2 ^ length α
this : ∀ (y : α), decide (x &&& y ≠ 0) = UInt.getBit y i
hgetbit : n < length α → UInt.getBit (bitmask (OfNat.ofNat n)) i = Nat.getBit i n
⊢ UInt.getBit (bitmask (OfNat.ofNat n)) i = Nat.getBit i n
Tactic:
exact hgetbit ‹n < length α›
State after:
no goals

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 α
this✝ : n < length α
this : n < 2 ^ length α
y : α
hyi : UInt.getBit y i = true
⊢ decide (x &&& y ≠ 0) = true
Tactic:
apply decide_eq_true
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
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 α
this✝ : n < length α
this : n < 2 ^ length α
y : α
hyi : UInt.getBit y i = true
⊢ x &&& y ≠ 0

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
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 α
this✝ : n < length α
this : n < 2 ^ length α
y : α
hyi : UInt.getBit y i = true
⊢ x &&& y ≠ 0
Tactic:
intro hcontra
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
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 α
this✝ : n < length α
this : n < 2 ^ length α
y : α
hyi : UInt.getBit y i = true
hcontra : x &&& y = 0
⊢ False

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
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 α
this✝ : n < length α
this : n < 2 ^ length α
y : α
hyi : UInt.getBit y i = true
hcontra : x &&& y = 0
⊢ False
Tactic:
have := calc
  true = (true && true) := rfl
  _    = (UInt.getBit x i && UInt.getBit y i) := by rw [hi i, decide_eq_true rfl, hyi]
  _    = UInt.getBit (x &&& y) i := by rw [UInt.getBit_land]
  _    = UInt.getBit (α:=α) 0 i := by rw [hcontra]
  _    = false := UInt.getBit_zero i
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
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 α
this✝¹ : n < length α
this✝ : n < 2 ^ length α
y : α
hyi : UInt.getBit y i = true
hcontra : x &&& y = 0
this : true = false
⊢ False

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
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 α
this✝¹ : n < length α
this✝ : n < 2 ^ length α
y : α
hyi : UInt.getBit y i = true
hcontra : x &&& y = 0
this : true = false
⊢ False
Tactic:
cases this
State after:
no goals

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 α
this✝ : n < length α
this : n < 2 ^ length α
y : α
hyi : UInt.getBit y i = true
hcontra : x &&& y = 0
⊢ (true && true) = (UInt.getBit x i && UInt.getBit y i)
Tactic:
rw [hi i, decide_eq_true rfl, hyi]
State after:
no goals

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 α
this✝ : n < length α
this : n < 2 ^ length α
y : α
hyi : UInt.getBit y i = true
hcontra : x &&& y = 0
⊢ (UInt.getBit x i && UInt.getBit y i) = UInt.getBit (x &&& y) i
Tactic:
rw [UInt.getBit_land]
State after:
no goals

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 α
this✝ : n < length α
this : n < 2 ^ length α
y : α
hyi : UInt.getBit y i = true
hcontra : x &&& y = 0
⊢ UInt.getBit (x &&& y) i = UInt.getBit 0 i
Tactic:
rw [hcontra]
State after:
no goals

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 α
this✝ : n < length α
this : n < 2 ^ length α
y : α
hyi : UInt.getBit y i = false
⊢ decide (x &&& y ≠ 0) = false
Tactic:
apply decide_eq_false
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
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 α
this✝ : n < length α
this : n < 2 ^ length α
y : α
hyi : UInt.getBit y i = false
⊢ ¬x &&& y ≠ 0

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
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 α
this✝ : n < length α
this : n < 2 ^ length α
y : α
hyi : UInt.getBit y i = false
⊢ ¬x &&& y ≠ 0
Tactic:
apply not_not_intro
State after:
case a.h
α : 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 α
this✝ : n < length α
this : n < 2 ^ length α
y : α
hyi : UInt.getBit y i = false
⊢ x &&& y = 0

State before:
case a.h
α : 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 α
this✝ : n < length α
this : n < 2 ^ length α
y : α
hyi : UInt.getBit y i = false
⊢ x &&& y = 0
Tactic:
apply UInt.bitext
State after:
case a.h.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
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 α
this✝ : n < length α
this : n < 2 ^ length α
y : α
hyi : UInt.getBit y i = false
⊢ ∀ (i : Nat), i < length α → UInt.getBit (x &&& y) i = UInt.getBit 0 i

State before:
case a.h.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
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 α
this✝ : n < length α
this : n < 2 ^ length α
y : α
hyi : UInt.getBit y i = false
⊢ ∀ (i : Nat), i < length α → UInt.getBit (x &&& y) i = UInt.getBit 0 i
Tactic:
intro j hj
State after:
case a.h.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
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 α
this✝ : n < length α
this : n < 2 ^ length α
y : α
hyi : UInt.getBit y i = false
j : Nat
hj : j < length α
⊢ UInt.getBit (x &&& y) j = UInt.getBit 0 j

State before:
case a.h.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
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 α
this✝ : n < length α
this : n < 2 ^ length α
y : α
hyi : UInt.getBit y i = false
j : Nat
hj : j < length α
⊢ UInt.getBit (x &&& y) j = UInt.getBit 0 j
Tactic:
rw [UInt.getBit_zero, UInt.getBit_land, hi j]
State after:
case a.h.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
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 α
this✝ : n < length α
this : n < 2 ^ length α
y : α
hyi : UInt.getBit y i = false
j : Nat
hj : j < length α
⊢ (decide (i = j) && UInt.getBit y j) = false

State before:
case a.h.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
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 α
this✝ : n < length α
this : n < 2 ^ length α
y : α
hyi : UInt.getBit y i = false
j : Nat
hj : j < length α
⊢ (decide (i = j) && UInt.getBit y j) = false
Tactic:
if hij : i = j
then cases hij; rw [hyi, Bool.and_false]
else rw [decide_eq_false hij, Bool.false_and]
State after:
no goals

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 α
this✝ : n < length α
this : n < 2 ^ length α
y : α
hyi : UInt.getBit y i = false
j : Nat
hj : j < length α
hij : i = j
⊢ (decide (i = j) && UInt.getBit y j) = false
Tactic:
cases hij
State after:
case refl
α : 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 α
this✝ : n < length α
this : n < 2 ^ length α
y : α
hyi : UInt.getBit y i = false
hj : i < length α
⊢ (decide (i = i) && UInt.getBit y i) = false

State before:
case refl
α : 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 α
this✝ : n < length α
this : n < 2 ^ length α
y : α
hyi : UInt.getBit y i = false
hj : i < length α
⊢ (decide (i = i) && UInt.getBit y i) = false
Tactic:
rw [hyi, Bool.and_false]
State after:
no goals

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 α
this✝ : n < length α
this : n < 2 ^ length α
y : α
hyi : UInt.getBit y i = false
j : Nat
hj : j < length α
hij : ¬i = j
⊢ (decide (i = j) && UInt.getBit y j) = false
Tactic:
rw [decide_eq_false hij, Bool.false_and]
State after:
no goals