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

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b : α
⊢ a &&& b = 0 → a + b = a ^^^ b
Tactic:
intro h
State after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b : α
h : a &&& b = 0
⊢ a + b = a ^^^ b

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b : α
h : a &&& b = 0
⊢ a + b = a ^^^ b
Tactic:
apply toNat_inj
State after:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b : α
h : a &&& b = 0
⊢ toNat (a + b) = toNat (a ^^^ b)

State before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b : α
h : a &&& b = 0
⊢ toNat (a + b) = toNat (a ^^^ b)
Tactic:
simp [toNat_add, toNat_xor]
State after:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b : α
h : a &&& b = 0
⊢ (toNat a + toNat b) % 2 ^ length α = toNat a ^^^ toNat b

State before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b : α
h : a &&& b = 0
⊢ (toNat a + toNat b) % 2 ^ length α = toNat a ^^^ toNat b
Tactic:
have : toNat a &&& toNat b = 0 :=
  toNat_land a b ▸ h ▸ toNat_zero
State after:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b : α
h : a &&& b = 0
this : toNat a &&& toNat b = 0
⊢ (toNat a + toNat b) % 2 ^ length α = toNat a ^^^ toNat b

State before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b : α
h : a &&& b = 0
this : toNat a &&& toNat b = 0
⊢ (toNat a + toNat b) % 2 ^ length α = toNat a ^^^ toNat b
Tactic:
rw [Nat.add_eq_xor this]
State after:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b : α
h : a &&& b = 0
this : toNat a &&& toNat b = 0
⊢ (toNat a ^^^ toNat b) % 2 ^ length α = toNat a ^^^ toNat b

State before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b : α
h : a &&& b = 0
this : toNat a &&& toNat b = 0
⊢ (toNat a ^^^ toNat b) % 2 ^ length α = toNat a ^^^ toNat b
Tactic:
have : toNat a ^^^ toNat b < 2^length α
  := Nat.bitwise_lt_exp2 bne (toNat_lt a) (toNat_lt b)
State after:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b : α
h : a &&& b = 0
this✝ : toNat a &&& toNat b = 0
this : toNat a ^^^ toNat b < 2 ^ length α
⊢ (toNat a ^^^ toNat b) % 2 ^ length α = toNat a ^^^ toNat b

State before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b : α
h : a &&& b = 0
this✝ : toNat a &&& toNat b = 0
this : toNat a ^^^ toNat b < 2 ^ length α
⊢ (toNat a ^^^ toNat b) % 2 ^ length α = toNat a ^^^ toNat b
Tactic:
rw [Nat.mod_eq_of_lt this]
State after:
no goals