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

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
m n : Nat
⊢ OfNat.ofNat m + OfNat.ofNat n = OfNat.ofNat (m + n)
Tactic:
apply UInt.toNat_inj
State after:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
m n : Nat
⊢ toNat (OfNat.ofNat m + OfNat.ofNat n) = toNat (OfNat.ofNat (m + n))

State before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
m n : Nat
⊢ toNat (OfNat.ofNat m + OfNat.ofNat n) = toNat (OfNat.ofNat (m + n))
Tactic:
simp only [toNat_add, toNat_ofNat, Nat.mod_add_mod, Nat.add_mod_mod]
State after:
no goals