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

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
⊢ toNat n < length α → UInt.getBit (bitmask n) i = (decide (i < length α) && Nat.getBit i (toNat n))
Tactic:
intro hn
State after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
⊢ UInt.getBit (bitmask n) i = (decide (i < length α) && Nat.getBit i (toNat n))

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
⊢ UInt.getBit (bitmask n) i = (decide (i < length α) && Nat.getBit i (toNat n))
Tactic:
suffices ∀ k, k ≤ length α → UInt.getBit (bitmask.aux n k) i = (i < k && i.getBit (toNat n)) 
  from this (length α) Nat.le.refl
State after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
⊢ ∀ (k : Nat), k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
⊢ ∀ (k : Nat), k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
Tactic:
intro k hk
State after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
hk : k ≤ length α
⊢ UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
hk : k ≤ length α
⊢ UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
Tactic:
induction k
State after:
case zero
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
hk : Nat.zero ≤ length α
⊢ UInt.getBit (bitmask.aux n Nat.zero) i = (decide (i < Nat.zero) && Nat.getBit i (toNat n))

case succ
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
n✝ : Nat
n_ih✝ : n✝ ≤ length α → UInt.getBit (bitmask.aux n n✝) i = (decide (i < n✝) && Nat.getBit i (toNat n))
hk : Nat.succ n✝ ≤ length α
⊢ UInt.getBit (bitmask.aux n (Nat.succ n✝)) i = (decide (i < Nat.succ n✝) && Nat.getBit i (toNat n))

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
hk : Nat.zero ≤ length α
⊢ UInt.getBit (bitmask.aux n Nat.zero) i = (decide (i < Nat.zero) && Nat.getBit i (toNat n))
Tactic:
case zero =>
  conv => lhs; dsimp [bitmask.aux, UInt.getBit]; rw [toNat_zero]
  simp [bitmask.aux, Nat.not_lt_zero i]
State after:
no goals

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
h_ind : k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
hk : Nat.succ k ≤ length α
⊢ UInt.getBit (bitmask.aux n (Nat.succ k)) i = (decide (i < Nat.succ k) && Nat.getBit i (toNat n))
Tactic:
case succ k h_ind =>
  have : k < 2^length α := trans (Nat.le_of_succ_le hk) (Nat.exp_lt_pow _ Nat.le.refl)
  have : 2^toNat n < 2^length α := Nat.pow_lt_pow_right Nat.le.refl hn
  have : 1 < 2^length α := calc
    1 < 2^1 := by decide
    _ ≤ 2^k.succ := Nat.pow_le_pow_of_le_right (Nat.zero_lt_succ 1) (Nat.succ_le_succ k.zero_le)
    _ ≤ 2^length α := Nat.pow_le_pow_of_le_right (Nat.zero_lt_succ 1) hk
  conv =>
    lhs; simp only [UInt.getBit_xor, bitmask.aux]; rw [h_ind (Nat.le_of_succ_le hk)]
    unfold UInt.getBit
    simp only [toNat_shiftLeft, toNat_land, toNat_shiftRight, toNat_ofNat k, toNat_ofNat 1]
    rw [Nat.mod_eq_of_lt hn, Nat.mod_eq_of_lt ‹k < 2^length α›, Nat.mod_eq_of_lt hk, Nat.mod_eq_of_lt ‹1<2^length α›]
    tactic =>
      have : (k >>> toNat n &&& 1) <<< k < 2^length α :=
        calc (k >>> toNat n &&& 1) <<< k
          _ = (k >>> toNat n &&& 1) * 2^k := Nat.shiftLeft_eq _ k
          _ ≤ 1*2^k := Nat.mul_le_mul_right _ $ by rw [Nat.land_one]; exact Nat.le_of_lt_succ (Nat.mod_lt _ (Nat.zero_lt_succ 1))
          _ = 2^k := Nat.one_mul _
          _ < 2^length α := Nat.pow_lt_pow_right Nat.le.refl hk
    rw [Nat.mod_eq_of_lt this]
    rhs; rw [Nat.shiftLeft_getBit, Nat.land_getBit, Nat.shiftRight_getBit]
    change decide (i ≥ k) && (k.getBit (i-k+toNat n) && Nat.getBit (2^0) (i-k))
    rw [Nat.getBit_two_pow, ←and_decideEq (λ x => Nat.getBit k (x + toNat n))]
    tactic =>
      have : 0 = i-k ↔ i ≤ k :=
        ⟨Nat.le_of_sub_eq_zero ∘ Eq.symm, Eq.symm ∘ Nat.sub_eq_zero_of_le⟩
      have : (i ≥ k ∧ i ≤ k) ↔ i = k :=
        ⟨λ h => Nat.le_antisymm h.right h.left, λ h => by cases h; exact ⟨Nat.le.refl, Nat.le.refl⟩⟩
    rw [decide_eq_decide.mpr ‹0=i-k ↔ i≤k›, Bool.and_comm _ (decide _), ←Bool.and_assoc]
    rw [decide_and_decide, decide_eq_decide.mpr ‹(i≥k ∧ i≤k) ↔ i=k›]
    rw [Nat.zero_add, ←decideEq_and (f:=λ x => Nat.getBit x (toNat n))]
  rw [←Bool.bne_and]
  cases Nat.lt_or_ge i k
  case inl hlt =>
    rw [decide_eq_true hlt, decide_eq_false (Nat.ne_of_lt hlt), decide_eq_true (Nat.lt_succ_of_lt hlt)]
    rfl
  case inr hge =>
    cases Nat.lt_or_eq_of_le hge
    case inl hgt =>
      rw [decide_eq_false (Nat.not_lt_of_le (Nat.le_of_lt hgt)), decide_eq_false (Nat.ne_of_gt hgt), decide_eq_false (Nat.not_lt_of_le hgt)]
      rfl
    case inr heq => cases heq; simp
State after:
no goals

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
hk : Nat.zero ≤ length α
⊢ UInt.getBit (bitmask.aux n Nat.zero) i = (decide (i < Nat.zero) && Nat.getBit i (toNat n))
Tactic:
conv => lhs; dsimp [bitmask.aux, UInt.getBit]; rw [toNat_zero]
State after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
hk : Nat.zero ≤ length α
⊢ Nat.getBit 0 i = (decide (i < Nat.zero) && Nat.getBit i (toNat n))

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
hk : Nat.zero ≤ length α
⊢ Nat.getBit 0 i = (decide (i < Nat.zero) && Nat.getBit i (toNat n))
Tactic:
simp [bitmask.aux, Nat.not_lt_zero i]
State after:
no goals

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
h_ind : k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
hk : Nat.succ k ≤ length α
⊢ UInt.getBit (bitmask.aux n (Nat.succ k)) i = (decide (i < Nat.succ k) && Nat.getBit i (toNat n))
Tactic:
have : k < 2^length α := trans (Nat.le_of_succ_le hk) (Nat.exp_lt_pow _ Nat.le.refl)
State after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
h_ind : k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
hk : Nat.succ k ≤ length α
this : k < 2 ^ length α
⊢ UInt.getBit (bitmask.aux n (Nat.succ k)) i = (decide (i < Nat.succ k) && Nat.getBit i (toNat n))

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
h_ind : k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
hk : Nat.succ k ≤ length α
this : k < 2 ^ length α
⊢ UInt.getBit (bitmask.aux n (Nat.succ k)) i = (decide (i < Nat.succ k) && Nat.getBit i (toNat n))
Tactic:
have : 2^toNat n < 2^length α := Nat.pow_lt_pow_right Nat.le.refl hn
State after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
h_ind : k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
hk : Nat.succ k ≤ length α
this✝ : k < 2 ^ length α
this : 2 ^ toNat n < 2 ^ length α
⊢ UInt.getBit (bitmask.aux n (Nat.succ k)) i = (decide (i < Nat.succ k) && Nat.getBit i (toNat n))

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
h_ind : k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
hk : Nat.succ k ≤ length α
this✝ : k < 2 ^ length α
this : 2 ^ toNat n < 2 ^ length α
⊢ UInt.getBit (bitmask.aux n (Nat.succ k)) i = (decide (i < Nat.succ k) && Nat.getBit i (toNat n))
Tactic:
have : 1 < 2^length α := calc
  1 < 2^1 := by decide
  _ ≤ 2^k.succ := Nat.pow_le_pow_of_le_right (Nat.zero_lt_succ 1) (Nat.succ_le_succ k.zero_le)
  _ ≤ 2^length α := Nat.pow_le_pow_of_le_right (Nat.zero_lt_succ 1) hk
State after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
h_ind : k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
hk : Nat.succ k ≤ length α
this✝¹ : k < 2 ^ length α
this✝ : 2 ^ toNat n < 2 ^ length α
this : 1 < 2 ^ length α
⊢ UInt.getBit (bitmask.aux n (Nat.succ k)) i = (decide (i < Nat.succ k) && Nat.getBit i (toNat n))

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
h_ind : k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
hk : Nat.succ k ≤ length α
this✝¹ : k < 2 ^ length α
this✝ : 2 ^ toNat n < 2 ^ length α
this : 1 < 2 ^ length α
⊢ UInt.getBit (bitmask.aux n (Nat.succ k)) i = (decide (i < Nat.succ k) && Nat.getBit i (toNat n))
Tactic:
conv =>
  lhs; simp only [UInt.getBit_xor, bitmask.aux]; rw [h_ind (Nat.le_of_succ_le hk)]
  unfold UInt.getBit
  simp only [toNat_shiftLeft, toNat_land, toNat_shiftRight, toNat_ofNat k, toNat_ofNat 1]
  rw [Nat.mod_eq_of_lt hn, Nat.mod_eq_of_lt ‹k < 2^length α›, Nat.mod_eq_of_lt hk, Nat.mod_eq_of_lt ‹1<2^length α›]
  tactic =>
    have : (k >>> toNat n &&& 1) <<< k < 2^length α :=
      calc (k >>> toNat n &&& 1) <<< k
        _ = (k >>> toNat n &&& 1) * 2^k := Nat.shiftLeft_eq _ k
        _ ≤ 1*2^k := Nat.mul_le_mul_right _ $ by rw [Nat.land_one]; exact Nat.le_of_lt_succ (Nat.mod_lt _ (Nat.zero_lt_succ 1))
        _ = 2^k := Nat.one_mul _
        _ < 2^length α := Nat.pow_lt_pow_right Nat.le.refl hk
  rw [Nat.mod_eq_of_lt this]
  rhs; rw [Nat.shiftLeft_getBit, Nat.land_getBit, Nat.shiftRight_getBit]
  change decide (i ≥ k) && (k.getBit (i-k+toNat n) && Nat.getBit (2^0) (i-k))
  rw [Nat.getBit_two_pow, ←and_decideEq (λ x => Nat.getBit k (x + toNat n))]
  tactic =>
    have : 0 = i-k ↔ i ≤ k :=
      ⟨Nat.le_of_sub_eq_zero ∘ Eq.symm, Eq.symm ∘ Nat.sub_eq_zero_of_le⟩
    have : (i ≥ k ∧ i ≤ k) ↔ i = k :=
      ⟨λ h => Nat.le_antisymm h.right h.left, λ h => by cases h; exact ⟨Nat.le.refl, Nat.le.refl⟩⟩
  rw [decide_eq_decide.mpr ‹0=i-k ↔ i≤k›, Bool.and_comm _ (decide _), ←Bool.and_assoc]
  rw [decide_and_decide, decide_eq_decide.mpr ‹(i≥k ∧ i≤k) ↔ i=k›]
  rw [Nat.zero_add, ←decideEq_and (f:=λ x => Nat.getBit x (toNat n))]
State after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
h_ind : k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
hk : Nat.succ k ≤ length α
this✝¹ : k < 2 ^ length α
this✝ : 2 ^ toNat n < 2 ^ length α
this : 1 < 2 ^ length α
⊢ ((decide (i < k) && Nat.getBit i (toNat n)) != (decide (i = k) && Nat.getBit i (toNat n))) =
    (decide (i < Nat.succ k) && Nat.getBit i (toNat n))

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
h_ind : k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
hk : Nat.succ k ≤ length α
this✝¹ : k < 2 ^ length α
this✝ : 2 ^ toNat n < 2 ^ length α
this : 1 < 2 ^ length α
⊢ ((decide (i < k) && Nat.getBit i (toNat n)) != (decide (i = k) && Nat.getBit i (toNat n))) =
    (decide (i < Nat.succ k) && Nat.getBit i (toNat n))
Tactic:
rw [←Bool.bne_and]
State after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
h_ind : k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
hk : Nat.succ k ≤ length α
this✝¹ : k < 2 ^ length α
this✝ : 2 ^ toNat n < 2 ^ length α
this : 1 < 2 ^ length α
⊢ (decide (i < k) != decide (i = k) && Nat.getBit i (toNat n)) = (decide (i < Nat.succ k) && Nat.getBit i (toNat n))

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
h_ind : k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
hk : Nat.succ k ≤ length α
this✝¹ : k < 2 ^ length α
this✝ : 2 ^ toNat n < 2 ^ length α
this : 1 < 2 ^ length α
⊢ (decide (i < k) != decide (i = k) && Nat.getBit i (toNat n)) = (decide (i < Nat.succ k) && Nat.getBit i (toNat n))
Tactic:
cases Nat.lt_or_ge i k
State after:
case inl
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
h_ind : k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
hk : Nat.succ k ≤ length α
this✝¹ : k < 2 ^ length α
this✝ : 2 ^ toNat n < 2 ^ length α
this : 1 < 2 ^ length α
h✝ : i < k
⊢ (decide (i < k) != decide (i = k) && Nat.getBit i (toNat n)) = (decide (i < Nat.succ k) && Nat.getBit i (toNat n))

case inr
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
h_ind : k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
hk : Nat.succ k ≤ length α
this✝¹ : k < 2 ^ length α
this✝ : 2 ^ toNat n < 2 ^ length α
this : 1 < 2 ^ length α
h✝ : i ≥ k
⊢ (decide (i < k) != decide (i = k) && Nat.getBit i (toNat n)) = (decide (i < Nat.succ k) && Nat.getBit i (toNat n))

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
h_ind : k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
hk : Nat.succ k ≤ length α
this✝¹ : k < 2 ^ length α
this✝ : 2 ^ toNat n < 2 ^ length α
this : 1 < 2 ^ length α
hlt : i < k
⊢ (decide (i < k) != decide (i = k) && Nat.getBit i (toNat n)) = (decide (i < Nat.succ k) && Nat.getBit i (toNat n))
Tactic:
case inl hlt =>
  rw [decide_eq_true hlt, decide_eq_false (Nat.ne_of_lt hlt), decide_eq_true (Nat.lt_succ_of_lt hlt)]
  rfl
State after:
no goals

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
h_ind : k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
hk : Nat.succ k ≤ length α
this✝¹ : k < 2 ^ length α
this✝ : 2 ^ toNat n < 2 ^ length α
this : 1 < 2 ^ length α
hge : i ≥ k
⊢ (decide (i < k) != decide (i = k) && Nat.getBit i (toNat n)) = (decide (i < Nat.succ k) && Nat.getBit i (toNat n))
Tactic:
case inr hge =>
  cases Nat.lt_or_eq_of_le hge
  case inl hgt =>
    rw [decide_eq_false (Nat.not_lt_of_le (Nat.le_of_lt hgt)), decide_eq_false (Nat.ne_of_gt hgt), decide_eq_false (Nat.not_lt_of_le hgt)]
    rfl
  case inr heq => cases heq; simp
State after:
no goals

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
h_ind : k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
hk : Nat.succ k ≤ length α
this✝ : k < 2 ^ length α
this : 2 ^ toNat n < 2 ^ length α
⊢ 1 < 2 ^ 1
Tactic:
decide
State after:
no goals

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
h_ind : k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
hk : Nat.succ k ≤ length α
this✝¹ : k < 2 ^ length α
this✝ : 2 ^ toNat n < 2 ^ length α
this : 1 < 2 ^ length α
⊢ ((decide (i < k) && Nat.getBit i (toNat n)) != Nat.getBit ((k >>> toNat n &&& 1) <<< k % 2 ^ length α) i) = ?m.37836
Tactic:
have : (k >>> toNat n &&& 1) <<< k < 2^length α :=
  calc (k >>> toNat n &&& 1) <<< k
    _ = (k >>> toNat n &&& 1) * 2^k := Nat.shiftLeft_eq _ k
    _ ≤ 1*2^k := Nat.mul_le_mul_right _ $ by rw [Nat.land_one]; exact Nat.le_of_lt_succ (Nat.mod_lt _ (Nat.zero_lt_succ 1))
    _ = 2^k := Nat.one_mul _
    _ < 2^length α := Nat.pow_lt_pow_right Nat.le.refl hk
State after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
h_ind : k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
hk : Nat.succ k ≤ length α
this✝² : k < 2 ^ length α
this✝¹ : 2 ^ toNat n < 2 ^ length α
this✝ : 1 < 2 ^ length α
this : (k >>> toNat n &&& 1) <<< k < 2 ^ length α
⊢ ((decide (i < k) && Nat.getBit i (toNat n)) != Nat.getBit ((k >>> toNat n &&& 1) <<< k % 2 ^ length α) i) = ?m.37836

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
h_ind : k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
hk : Nat.succ k ≤ length α
this✝¹ : k < 2 ^ length α
this✝ : 2 ^ toNat n < 2 ^ length α
this : 1 < 2 ^ length α
⊢ k >>> toNat n &&& 1 ≤ 1
Tactic:
rw [Nat.land_one]
State after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
h_ind : k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
hk : Nat.succ k ≤ length α
this✝¹ : k < 2 ^ length α
this✝ : 2 ^ toNat n < 2 ^ length α
this : 1 < 2 ^ length α
⊢ k >>> toNat n % 2 ≤ 1

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
h_ind : k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
hk : Nat.succ k ≤ length α
this✝¹ : k < 2 ^ length α
this✝ : 2 ^ toNat n < 2 ^ length α
this : 1 < 2 ^ length α
⊢ k >>> toNat n % 2 ≤ 1
Tactic:
exact Nat.le_of_lt_succ (Nat.mod_lt _ (Nat.zero_lt_succ 1))
State after:
no goals

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
h_ind : k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
hk : Nat.succ k ≤ length α
this✝² : k < 2 ^ length α
this✝¹ : 2 ^ toNat n < 2 ^ length α
this✝ : 1 < 2 ^ length α
this : (k >>> toNat n &&& 1) <<< k < 2 ^ length α
⊢ (decide (i ≥ k) && (Nat.getBit k (0 + toNat n) && decide (0 = i - k))) = ?m.39484
Tactic:
have : 0 = i-k ↔ i ≤ k :=
  ⟨Nat.le_of_sub_eq_zero ∘ Eq.symm, Eq.symm ∘ Nat.sub_eq_zero_of_le⟩
State after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
h_ind : k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
hk : Nat.succ k ≤ length α
this✝³ : k < 2 ^ length α
this✝² : 2 ^ toNat n < 2 ^ length α
this✝¹ : 1 < 2 ^ length α
this✝ : (k >>> toNat n &&& 1) <<< k < 2 ^ length α
this : 0 = i - k ↔ i ≤ k
⊢ (decide (i ≥ k) && (Nat.getBit k (0 + toNat n) && decide (0 = i - k))) = ?m.39484

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
h_ind : k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
hk : Nat.succ k ≤ length α
this✝³ : k < 2 ^ length α
this✝² : 2 ^ toNat n < 2 ^ length α
this✝¹ : 1 < 2 ^ length α
this✝ : (k >>> toNat n &&& 1) <<< k < 2 ^ length α
this : 0 = i - k ↔ i ≤ k
⊢ (decide (i ≥ k) && (Nat.getBit k (0 + toNat n) && decide (0 = i - k))) = ?m.39484
Tactic:
have : (i ≥ k ∧ i ≤ k) ↔ i = k :=
  ⟨λ h => Nat.le_antisymm h.right h.left, λ h => by cases h; exact ⟨Nat.le.refl, Nat.le.refl⟩⟩
State after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
h_ind : k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
hk : Nat.succ k ≤ length α
this✝⁴ : k < 2 ^ length α
this✝³ : 2 ^ toNat n < 2 ^ length α
this✝² : 1 < 2 ^ length α
this✝¹ : (k >>> toNat n &&& 1) <<< k < 2 ^ length α
this✝ : 0 = i - k ↔ i ≤ k
this : i ≥ k ∧ i ≤ k ↔ i = k
⊢ (decide (i ≥ k) && (Nat.getBit k (0 + toNat n) && decide (0 = i - k))) = ?m.39484

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
h_ind : k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
hk : Nat.succ k ≤ length α
this✝³ : k < 2 ^ length α
this✝² : 2 ^ toNat n < 2 ^ length α
this✝¹ : 1 < 2 ^ length α
this✝ : (k >>> toNat n &&& 1) <<< k < 2 ^ length α
this : 0 = i - k ↔ i ≤ k
h : i = k
⊢ i ≥ k ∧ i ≤ k
Tactic:
cases h
State after:
case refl
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
this✝³ : 2 ^ toNat n < 2 ^ length α
this✝² : 1 < 2 ^ length α
h_ind : i ≤ length α → UInt.getBit (bitmask.aux n i) i = (decide (i < i) && Nat.getBit i (toNat n))
hk : Nat.succ i ≤ length α
this✝¹ : i < 2 ^ length α
this✝ : (i >>> toNat n &&& 1) <<< i < 2 ^ length α
this : 0 = i - i ↔ i ≤ i
⊢ i ≥ i ∧ i ≤ i

State before:
case refl
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
this✝³ : 2 ^ toNat n < 2 ^ length α
this✝² : 1 < 2 ^ length α
h_ind : i ≤ length α → UInt.getBit (bitmask.aux n i) i = (decide (i < i) && Nat.getBit i (toNat n))
hk : Nat.succ i ≤ length α
this✝¹ : i < 2 ^ length α
this✝ : (i >>> toNat n &&& 1) <<< i < 2 ^ length α
this : 0 = i - i ↔ i ≤ i
⊢ i ≥ i ∧ i ≤ i
Tactic:
exact ⟨Nat.le.refl, Nat.le.refl⟩
State after:
no goals

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
h_ind : k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
hk : Nat.succ k ≤ length α
this✝¹ : k < 2 ^ length α
this✝ : 2 ^ toNat n < 2 ^ length α
this : 1 < 2 ^ length α
hlt : i < k
⊢ (decide (i < k) != decide (i = k) && Nat.getBit i (toNat n)) = (decide (i < Nat.succ k) && Nat.getBit i (toNat n))
Tactic:
rw [decide_eq_true hlt, decide_eq_false (Nat.ne_of_lt hlt), decide_eq_true (Nat.lt_succ_of_lt hlt)]
State after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
h_ind : k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
hk : Nat.succ k ≤ length α
this✝¹ : k < 2 ^ length α
this✝ : 2 ^ toNat n < 2 ^ length α
this : 1 < 2 ^ length α
hlt : i < k
⊢ (true != false && Nat.getBit i (toNat n)) = (true && Nat.getBit i (toNat n))

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
h_ind : k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
hk : Nat.succ k ≤ length α
this✝¹ : k < 2 ^ length α
this✝ : 2 ^ toNat n < 2 ^ length α
this : 1 < 2 ^ length α
hlt : i < k
⊢ (true != false && Nat.getBit i (toNat n)) = (true && Nat.getBit i (toNat n))
Tactic:
rfl
State after:
no goals

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
h_ind : k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
hk : Nat.succ k ≤ length α
this✝¹ : k < 2 ^ length α
this✝ : 2 ^ toNat n < 2 ^ length α
this : 1 < 2 ^ length α
hge : i ≥ k
⊢ (decide (i < k) != decide (i = k) && Nat.getBit i (toNat n)) = (decide (i < Nat.succ k) && Nat.getBit i (toNat n))
Tactic:
cases Nat.lt_or_eq_of_le hge
State after:
case inl
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
h_ind : k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
hk : Nat.succ k ≤ length α
this✝¹ : k < 2 ^ length α
this✝ : 2 ^ toNat n < 2 ^ length α
this : 1 < 2 ^ length α
hge : i ≥ k
h✝ : k < i
⊢ (decide (i < k) != decide (i = k) && Nat.getBit i (toNat n)) = (decide (i < Nat.succ k) && Nat.getBit i (toNat n))

case inr
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
h_ind : k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
hk : Nat.succ k ≤ length α
this✝¹ : k < 2 ^ length α
this✝ : 2 ^ toNat n < 2 ^ length α
this : 1 < 2 ^ length α
hge : i ≥ k
h✝ : k = i
⊢ (decide (i < k) != decide (i = k) && Nat.getBit i (toNat n)) = (decide (i < Nat.succ k) && Nat.getBit i (toNat n))

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
h_ind : k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
hk : Nat.succ k ≤ length α
this✝¹ : k < 2 ^ length α
this✝ : 2 ^ toNat n < 2 ^ length α
this : 1 < 2 ^ length α
hge : i ≥ k
hgt : k < i
⊢ (decide (i < k) != decide (i = k) && Nat.getBit i (toNat n)) = (decide (i < Nat.succ k) && Nat.getBit i (toNat n))
Tactic:
case inl hgt =>
  rw [decide_eq_false (Nat.not_lt_of_le (Nat.le_of_lt hgt)), decide_eq_false (Nat.ne_of_gt hgt), decide_eq_false (Nat.not_lt_of_le hgt)]
  rfl
State after:
no goals

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
h_ind : k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
hk : Nat.succ k ≤ length α
this✝¹ : k < 2 ^ length α
this✝ : 2 ^ toNat n < 2 ^ length α
this : 1 < 2 ^ length α
hge : i ≥ k
heq : k = i
⊢ (decide (i < k) != decide (i = k) && Nat.getBit i (toNat n)) = (decide (i < Nat.succ k) && Nat.getBit i (toNat n))
Tactic:
case inr heq => cases heq; simp
State after:
no goals

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
h_ind : k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
hk : Nat.succ k ≤ length α
this✝¹ : k < 2 ^ length α
this✝ : 2 ^ toNat n < 2 ^ length α
this : 1 < 2 ^ length α
hge : i ≥ k
hgt : k < i
⊢ (decide (i < k) != decide (i = k) && Nat.getBit i (toNat n)) = (decide (i < Nat.succ k) && Nat.getBit i (toNat n))
Tactic:
rw [decide_eq_false (Nat.not_lt_of_le (Nat.le_of_lt hgt)), decide_eq_false (Nat.ne_of_gt hgt), decide_eq_false (Nat.not_lt_of_le hgt)]
State after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
h_ind : k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
hk : Nat.succ k ≤ length α
this✝¹ : k < 2 ^ length α
this✝ : 2 ^ toNat n < 2 ^ length α
this : 1 < 2 ^ length α
hge : i ≥ k
hgt : k < i
⊢ (false != false && Nat.getBit i (toNat n)) = (false && Nat.getBit i (toNat n))

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
h_ind : k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
hk : Nat.succ k ≤ length α
this✝¹ : k < 2 ^ length α
this✝ : 2 ^ toNat n < 2 ^ length α
this : 1 < 2 ^ length α
hge : i ≥ k
hgt : k < i
⊢ (false != false && Nat.getBit i (toNat n)) = (false && Nat.getBit i (toNat n))
Tactic:
rfl
State after:
no goals

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
h_ind : k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
hk : Nat.succ k ≤ length α
this✝¹ : k < 2 ^ length α
this✝ : 2 ^ toNat n < 2 ^ length α
this : 1 < 2 ^ length α
hge : i ≥ k
heq : k = i
⊢ (decide (i < k) != decide (i = k) && Nat.getBit i (toNat n)) = (decide (i < Nat.succ k) && Nat.getBit i (toNat n))
Tactic:
cases heq
State after:
case refl
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
this✝¹ : 2 ^ toNat n < 2 ^ length α
this✝ : 1 < 2 ^ length α
h_ind : i ≤ length α → UInt.getBit (bitmask.aux n i) i = (decide (i < i) && Nat.getBit i (toNat n))
hk : Nat.succ i ≤ length α
this : i < 2 ^ length α
hge : i ≥ i
⊢ (decide (i < i) != decide (i = i) && Nat.getBit i (toNat n)) = (decide (i < Nat.succ i) && Nat.getBit i (toNat n))

State before:
case refl
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
this✝¹ : 2 ^ toNat n < 2 ^ length α
this✝ : 1 < 2 ^ length α
h_ind : i ≤ length α → UInt.getBit (bitmask.aux n i) i = (decide (i < i) && Nat.getBit i (toNat n))
hk : Nat.succ i ≤ length α
this : i < 2 ^ length α
hge : i ≥ i
⊢ (decide (i < i) != decide (i = i) && Nat.getBit i (toNat n)) = (decide (i < Nat.succ i) && Nat.getBit i (toNat n))
Tactic:
simp
State after:
no goals