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

State before:
a b c : ℤω
⊢ rt3 ^ 2 = 3
Tactic:
have : (0 : ℝ) ≤ 3 := by norm_num
State after:
a b c : ℤω
this : 0 ≤ 3
⊢ rt3 ^ 2 = 3

State before:
a b c : ℤω
this : 0 ≤ 3
⊢ rt3 ^ 2 = 3
Tactic:
rw [pow_two]
State after:
a b c : ℤω
this : 0 ≤ 3
⊢ rt3 * rt3 = 3

State before:
a b c : ℤω
this : 0 ≤ 3
⊢ rt3 * rt3 = 3
Tactic:
rw [← Real.sqrt_mul this 3]
State after:
a b c : ℤω
this : 0 ≤ 3
⊢ Real.sqrt (3 * 3) = 3

State before:
a b c : ℤω
this : 0 ≤ 3
⊢ Real.sqrt (3 * 3) = 3
Tactic:
rw [Real.sqrt_mul_self this]
State after:
no goals

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