rw [lm]
two_nonneg : 2 ≥ 0
sq2_pos : Real.sqrt 2 > 0
sq2_nonneg : Real.sqrt 2 ≥ 0
lm : Real.sqrt 2 ^ 2 = Real.sqrt 2 ^ 1 * Real.sqrt 2 ^ 1
one_plus_one : 1 + 1 = 2
⊢ Real.sqrt 2 ^ 2 = 2
two_nonneg : 2 ≥ 0
sq2_pos : Real.sqrt 2 > 0
sq2_nonneg : Real.sqrt 2 ≥ 0
lm : Real.sqrt 2 ^ 2 = Real.sqrt 2 ^ 1 * Real.sqrt 2 ^ 1
one_plus_one : 1 + 1 = 2
⊢ Real.sqrt 2 ^ 1 * Real.sqrt 2 ^ 1 = 2