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

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ UInt.when true a = a
Tactic:
unfold UInt.when
State after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ 0 - ofBool true &&& a = a

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ 0 - ofBool true &&& a = a
Tactic:
apply UInt.bitext
State after:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ ∀ (i : Nat), i < length α → UInt.getBit (0 - ofBool true &&& a) i = UInt.getBit a i

State before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ ∀ (i : Nat), i < length α → UInt.getBit (0 - ofBool true &&& a) i = UInt.getBit a i
Tactic:
intro i hi
State after:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i : Nat
hi : i < length α
⊢ UInt.getBit (0 - ofBool true &&& a) i = UInt.getBit a i

State before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i : Nat
hi : i < length α
⊢ UInt.getBit (0 - ofBool true &&& a) i = UInt.getBit a i
Tactic:
have : (0 : α) - 1 = ~~~(0 : α) := by
  rw [UInt.complement_eq, UInt.zero_add]
State after:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i : Nat
hi : i < length α
this : 0 - 1 = ~~~0
⊢ UInt.getBit (0 - ofBool true &&& a) i = UInt.getBit a i

State before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i : Nat
hi : i < length α
this : 0 - 1 = ~~~0
⊢ UInt.getBit (0 - ofBool true &&& a) i = UInt.getBit a i
Tactic:
rw [UInt.ofBool_true, this, UInt.getBit_land, UInt.getBit_complement]
State after:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i : Nat
hi : i < length α
this : 0 - 1 = ~~~0
⊢ (UInt.getBit 0 i != decide (i < length α) && UInt.getBit a i) = UInt.getBit a i

State before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i : Nat
hi : i < length α
this : 0 - 1 = ~~~0
⊢ (UInt.getBit 0 i != decide (i < length α) && UInt.getBit a i) = UInt.getBit a i
Tactic:
simp only [decide_eq_true hi, UInt.getBit_zero]
State after:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i : Nat
hi : i < length α
this : 0 - 1 = ~~~0
⊢ (false != true && UInt.getBit a i) = UInt.getBit a i

State before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i : Nat
hi : i < length α
this : 0 - 1 = ~~~0
⊢ (false != true && UInt.getBit a i) = UInt.getBit a i
Tactic:
rfl
State after:
no goals

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i : Nat
hi : i < length α
⊢ 0 - 1 = ~~~0
Tactic:
rw [UInt.complement_eq, UInt.zero_add]
State after:
no goals