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

State before:
a b c : ℤα
hb : b ≠ 0
⊢ ¬natNorm (a * b) < natNorm a
Tactic:
rw [natNorm_hMul]
State after:
a b c : ℤα
hb : b ≠ 0
⊢ ¬natNorm a * natNorm b < natNorm a

State before:
a b c : ℤα
hb : b ≠ 0
⊢ ¬natNorm a * natNorm b < natNorm a
Tactic:
intro h
State after:
a b c : ℤα
hb : b ≠ 0
h : natNorm a * natNorm b < natNorm a
⊢ False

State before:
a b c : ℤα
hb : b ≠ 0
h : natNorm a * natNorm b < natNorm a
⊢ False
Tactic:
apply hb
State after:
a b c : ℤα
hb : b ≠ 0
h : natNorm a * natNorm b < natNorm a
⊢ b = 0

State before:
a b c : ℤα
hb : b ≠ 0
h : natNorm a * natNorm b < natNorm a
⊢ b = 0
Tactic:
clear hb
State after:
a b c : ℤα
h : natNorm a * natNorm b < natNorm a
⊢ b = 0

State before:
a b c : ℤα
h : natNorm a * natNorm b < natNorm a
⊢ b = 0
Tactic:
rw [← natNorm_eq_zero_iff]
State after:
a b c : ℤα
h : natNorm a * natNorm b < natNorm a
⊢ natNorm b = 0

State before:
a b c : ℤα
h : natNorm a * natNorm b < natNorm a
⊢ natNorm b = 0
Tactic:
cases b.natNorm
State after:
case zero
a b c : ℤα
h : natNorm a * natNorm b < natNorm a
⊢ Nat.zero = 0

case succ
a b c : ℤα
h : natNorm a * natNorm b < natNorm a
n✝ : ℕ
⊢ Nat.succ n✝ = 0

State before:
case zero
a b c : ℤα
h : natNorm a * natNorm b < natNorm a
⊢ Nat.zero = 0
Tactic:
rfl
State after:
no goals

State before:
case succ
a b c : ℤα
h : natNorm a * natNorm b < natNorm a
n✝ : ℕ
⊢ Nat.succ n✝ = 0
Tactic:
exfalso
State after:
case succ.h
a b c : ℤα
h : natNorm a * natNorm b < natNorm a
n✝ : ℕ
⊢ False