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

State before:
a b c : ℤα
⊢ rt7⁻¹ * rt7 = 1
Tactic:
apply inv_mul_cancel
State after:
case h
a b c : ℤα
⊢ rt7 ≠ 0

State before:
case h
a b c : ℤα
⊢ rt7 ≠ 0
Tactic:
intro h
State after:
case h
a b c : ℤα
h : rt7 = 0
⊢ False

State before:
case h
a b c : ℤα
h : rt7 = 0
⊢ False
Tactic:
norm_num at h
State after:
no goals