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

State before:
a b c : ℤα
⊢ rt7 ^ 2 = 7
Tactic:
have : (0 : ℝ) ≤ 7 := by norm_num
State after:
a b c : ℤα
this : 0 ≤ 7
⊢ rt7 ^ 2 = 7

State before:
a b c : ℤα
this : 0 ≤ 7
⊢ rt7 ^ 2 = 7
Tactic:
rw [pow_two]
State after:
a b c : ℤα
this : 0 ≤ 7
⊢ rt7 * rt7 = 7

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

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

State before:
a b c : ℤα
⊢ 0 ≤ 7
Tactic:
norm_num
State after:
no goals