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

State before:
a b c v : ℤα
⊢ norm v = ↑(natNorm v)
Tactic:
unfold natNorm
State after:
a b c v : ℤα
⊢ norm v = ↑(natAbs (norm v))

State before:
a b c v : ℤα
⊢ norm v = ↑(natAbs (norm v))
Tactic:
have p : 0 ≤ (norm v : ℝ) := by
  rw [← normSq_coe]
  exact normSq_nonneg _
State after:
a b c v : ℤα
p : 0 ≤ ↑(norm v)
⊢ norm v = ↑(natAbs (norm v))

State before:
a b c v : ℤα
p : 0 ≤ ↑(norm v)
⊢ norm v = ↑(natAbs (norm v))
Tactic:
have h : 0 ≤ norm v := by exact_mod_cast p
State after:
a b c v : ℤα
p : 0 ≤ ↑(norm v)
h : 0 ≤ norm v
⊢ norm v = ↑(natAbs (norm v))

State before:
a b c v : ℤα
p : 0 ≤ ↑(norm v)
h : 0 ≤ norm v
⊢ norm v = ↑(natAbs (norm v))
Tactic:
rw [← abs_eq_self] at h
State after:
a b c v : ℤα
p : 0 ≤ ↑(norm v)
h : |norm v| = norm v
⊢ norm v = ↑(natAbs (norm v))

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

State before:
a b c v : ℤα
p : 0 ≤ ↑(norm v)
h : |norm v| = norm v
⊢ norm v = |norm v|
Tactic:
symm
State after:
a b c v : ℤα
p : 0 ≤ ↑(norm v)
h : |norm v| = norm v
⊢ |norm v| = norm v

State before:
a b c v : ℤα
p : 0 ≤ ↑(norm v)
h : |norm v| = norm v
⊢ |norm v| = norm v
Tactic:
exact h
State after:
no goals

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

State before:
a b c v : ℤα
⊢ 0 ≤ ↑normSq (OneHom.toFun (↑↑inclusion) v)
Tactic:
exact normSq_nonneg _
State after:
no goals

State before:
a b c v : ℤα
p : 0 ≤ ↑(norm v)
⊢ 0 ≤ norm v
Tactic:
exact_mod_cast p
State after:
no goals