⊢ sqrt 2 / 2 / (sqrt 2 / 2) = 1
⊢ tan (π / 4) = 1
rw [tan_eq_sin_div_cos, cos_pi_div_four, sin_pi_div_four]
h : sqrt 2 / 2 > 0
⊢ sqrt 2 / 2 / (sqrt 2 / 2) = 1
⊢ sqrt 2 / 2 / (sqrt 2 / 2) = 1
have h : sqrt 2 / 2 > 0 := by cancel_denoms
no goals
h : sqrt 2 / 2 > 0
⊢ sqrt 2 / 2 / (sqrt 2 / 2) = 1
exact div_self (ne_of_gt h)
no goals
⊢ sqrt 2 / 2 > 0
cancel_denoms