Theorem: sq2_pow_twice (Lectures/PowerIrrationals.lean)

State before:
⊢ (Real.sqrt 2 ^ Real.sqrt 2) ^ Real.sqrt 2 = 2
Tactic:
have two_nonneg : (2 : ℝ) ≥ 0 := by norm_cast
State after:
two_nonneg : 2 ≥ 0
⊢ (Real.sqrt 2 ^ Real.sqrt 2) ^ Real.sqrt 2 = 2

State before:
two_nonneg : 2 ≥ 0
⊢ (Real.sqrt 2 ^ Real.sqrt 2) ^ Real.sqrt 2 = 2
Tactic:
have sq2_pos : (Real.sqrt 2) > 0 := by simp [Real.sqrt_pos]
State after:
two_nonneg : 2 ≥ 0
sq2_pos : Real.sqrt 2 > 0
⊢ (Real.sqrt 2 ^ Real.sqrt 2) ^ Real.sqrt 2 = 2

State before:
two_nonneg : 2 ≥ 0
sq2_pos : Real.sqrt 2 > 0
⊢ (Real.sqrt 2 ^ Real.sqrt 2) ^ Real.sqrt 2 = 2
Tactic:
have sq2_nonneg : (Real.sqrt 2) ≥ 0 := by
  apply Real.sqrt_nonneg
State after:
two_nonneg : 2 ≥ 0
sq2_pos : Real.sqrt 2 > 0
sq2_nonneg : Real.sqrt 2 ≥ 0
⊢ (Real.sqrt 2 ^ Real.sqrt 2) ^ Real.sqrt 2 = 2

State before:
two_nonneg : 2 ≥ 0
sq2_pos : Real.sqrt 2 > 0
sq2_nonneg : Real.sqrt 2 ≥ 0
⊢ (Real.sqrt 2 ^ Real.sqrt 2) ^ Real.sqrt 2 = 2
Tactic:
rw [← Real.rpow_mul sq2_nonneg, Real.mul_self_sqrt two_nonneg]
State after:
two_nonneg : 2 ≥ 0
sq2_pos : Real.sqrt 2 > 0
sq2_nonneg : Real.sqrt 2 ≥ 0
⊢ Real.sqrt 2 ^ 2 = 2

State before:
two_nonneg : 2 ≥ 0
sq2_pos : Real.sqrt 2 > 0
sq2_nonneg : Real.sqrt 2 ≥ 0
⊢ Real.sqrt 2 ^ 2 = 2
Tactic:
have lm := Real.rpow_add sq2_pos 1 1
State after:
two_nonneg : 2 ≥ 0
sq2_pos : Real.sqrt 2 > 0
sq2_nonneg : Real.sqrt 2 ≥ 0
lm : Real.sqrt 2 ^ (1 + 1) = Real.sqrt 2 ^ 1 * Real.sqrt 2 ^ 1
⊢ Real.sqrt 2 ^ 2 = 2

State before:
two_nonneg : 2 ≥ 0
sq2_pos : Real.sqrt 2 > 0
sq2_nonneg : Real.sqrt 2 ≥ 0
lm : Real.sqrt 2 ^ (1 + 1) = Real.sqrt 2 ^ 1 * Real.sqrt 2 ^ 1
⊢ Real.sqrt 2 ^ 2 = 2
Tactic:
have one_plus_one : (1: ℝ) + (1: ℝ) = 2 := by norm_num
State after:
two_nonneg : 2 ≥ 0
sq2_pos : Real.sqrt 2 > 0
sq2_nonneg : Real.sqrt 2 ≥ 0
lm : Real.sqrt 2 ^ (1 + 1) = Real.sqrt 2 ^ 1 * Real.sqrt 2 ^ 1
one_plus_one : 1 + 1 = 2
⊢ Real.sqrt 2 ^ 2 = 2

State before:
two_nonneg : 2 ≥ 0
sq2_pos : Real.sqrt 2 > 0
sq2_nonneg : Real.sqrt 2 ≥ 0
lm : Real.sqrt 2 ^ (1 + 1) = Real.sqrt 2 ^ 1 * Real.sqrt 2 ^ 1
one_plus_one : 1 + 1 = 2
⊢ Real.sqrt 2 ^ 2 = 2
Tactic:
rw [one_plus_one] at lm
State after:
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

State before:
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
Tactic:
rw [lm]
State after:
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

State before:
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
Tactic:
simp [Real.rpow_one]
State after:
no goals

State before:
⊢ 2 ≥ 0
Tactic:
norm_cast
State after:
no goals

State before:
two_nonneg : 2 ≥ 0
⊢ Real.sqrt 2 > 0
Tactic:
simp [Real.sqrt_pos]
State after:
no goals

State before:
two_nonneg : 2 ≥ 0
sq2_pos : Real.sqrt 2 > 0
⊢ Real.sqrt 2 ≥ 0
Tactic:
apply Real.sqrt_nonneg
State after:
no goals

State before:
two_nonneg : 2 ≥ 0
sq2_pos : Real.sqrt 2 > 0
sq2_nonneg : Real.sqrt 2 ≥ 0
lm : Real.sqrt 2 ^ (1 + 1) = Real.sqrt 2 ^ 1 * Real.sqrt 2 ^ 1
⊢ 1 + 1 = 2
Tactic:
norm_num
State after:
no goals