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

State before:
a b c : ℤα
⊢ natNorm a = 0 ↔ a = 0
Tactic:
constructor
State after:
case mp
a b c : ℤα
⊢ natNorm a = 0 → a = 0

case mpr
a b c : ℤα
⊢ a = 0 → natNorm a = 0

State before:
case mp
a b c : ℤα
⊢ natNorm a = 0 → a = 0
Tactic:
intro h
State after:
case mp
a b c : ℤα
h : natNorm a = 0
⊢ a = 0

State before:
case mp
a b c : ℤα
h : natNorm a = 0
⊢ a = 0
Tactic:
have : (a.natNorm : ℝ) = 0 := by exact_mod_cast h
State after:
case mp
a b c : ℤα
h : natNorm a = 0
this : ↑(natNorm a) = 0
⊢ a = 0

State before:
case mp
a b c : ℤα
h : natNorm a = 0
this : ↑(natNorm a) = 0
⊢ a = 0
Tactic:
rw [← natNorm_coe] at this
State after:
case mp
a b c : ℤα
h : natNorm a = 0
this : ↑normSq (OneHom.toFun (↑↑inclusion) a) = 0
⊢ a = 0

State before:
case mp
a b c : ℤα
h : natNorm a = 0
this : ↑normSq (OneHom.toFun (↑↑inclusion) a) = 0
⊢ a = 0
Tactic:
rw [normSq_eq_zero] at this
State after:
case mp
a b c : ℤα
h : natNorm a = 0
this : OneHom.toFun (↑↑inclusion) a = 0
⊢ a = 0

State before:
case mp
a b c : ℤα
h : natNorm a = 0
this : OneHom.toFun (↑↑inclusion) a = 0
⊢ a = 0
Tactic:
rwa [coe_eq_zero] at this
State after:
no goals

State before:
a b c : ℤα
h : natNorm a = 0
⊢ ↑(natNorm a) = 0
Tactic:
exact_mod_cast h
State after:
no goals

State before:
case mpr
a b c : ℤα
⊢ a = 0 → natNorm a = 0
Tactic:
intro h
State after:
case mpr
a b c : ℤα
h : a = 0
⊢ natNorm a = 0

State before:
case mpr
a b c : ℤα
h : a = 0
⊢ natNorm a = 0
Tactic:
rw [h]
State after:
case mpr
a b c : ℤα
h : a = 0
⊢ natNorm 0 = 0

State before:
case mpr
a b c : ℤα
h : a = 0
⊢ natNorm 0 = 0
Tactic:
decide
State after:
no goals