Theorem: ℤω.sqrt3_inv_hMul_self (Mordell4/Eisenstein.lean)

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

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

State before:
case h
a b c : ℤω
h : rt3 = 0
⊢ False
Tactic:
have := Real.sqrt_eq_iff_mul_self_eq (by norm_num : (0:ℝ) ≤ 3) (by norm_num : (0:ℝ) ≤ 0)
State after:
case h
a b c : ℤω
h : rt3 = 0
this : Real.sqrt 3 = 0 ↔ 0 * 0 = 3
⊢ False

State before:
case h
a b c : ℤω
h : rt3 = 0
this : Real.sqrt 3 = 0 ↔ 0 * 0 = 3
⊢ False
Tactic:
rw [this] at h
State after:
case h
a b c : ℤω
h : 0 * 0 = 3
this : Real.sqrt 3 = 0 ↔ 0 * 0 = 3
⊢ False

State before:
case h
a b c : ℤω
h : 0 * 0 = 3
this : Real.sqrt 3 = 0 ↔ 0 * 0 = 3
⊢ False
Tactic:
norm_num at h
State after:
no goals

State before:
a b c : ℤω
h : rt3 = 0
⊢ 0 ≤ 3
Tactic:
norm_num
State after:
no goals

State before:
a b c : ℤω
h : rt3 = 0
⊢ 0 ≤ 0
Tactic:
norm_num
State after:
no goals