Theorem: ℤα.natNorm_coe (Mordell4/Rt7Ring.lean)

State before:
a b c : ℤα
⊢ ↑normSq (OneHom.toFun (↑↑inclusion) a) = ↑(natNorm a)
Tactic:
unfold natNorm
State after:
a b c : ℤα
⊢ ↑normSq (OneHom.toFun (↑↑inclusion) a) = ↑(natAbs (norm a))

State before:
a b c : ℤα
⊢ ↑normSq (OneHom.toFun (↑↑inclusion) a) = ↑(natAbs (norm a))
Tactic:
rw [normSq_coe]
State after:
a b c : ℤα
⊢ ↑(norm a) = ↑(natAbs (norm a))

State before:
a b c : ℤα
⊢ ↑(norm a) = ↑(natAbs (norm a))
Tactic:
suffices h : a.norm = a.norm.natAbs
State after:
a b c : ℤα
h : norm a = ↑(natAbs (norm a))
⊢ ↑(norm a) = ↑(natAbs (norm a))

case h
a b c : ℤα
⊢ norm a = ↑(natAbs (norm a))

State before:
a b c : ℤα
h : norm a = ↑(natAbs (norm a))
⊢ ↑(norm a) = ↑(natAbs (norm a))

case h
a b c : ℤα
⊢ norm a = ↑(natAbs (norm a))
Tactic:
congr
State after:
case h
a b c : ℤα
⊢ norm a = ↑(natAbs (norm a))

State before:
case h
a b c : ℤα
⊢ norm a = ↑(natAbs (norm a))
Tactic:
norm_cast
State after:
case h
a b c : ℤα
⊢ norm a = |norm a|

State before:
case h
a b c : ℤα
⊢ norm a = |norm a|
Tactic:
exact this
State after:
no goals