How to set hypotheses with `variable` command correctly?

Stream: new members

[Ilmārs Cīrulis]

It seems I'm doing something wrong with those variable commands, probably. :(
I can't use right_angle inside the proof.

import Mathlib.Geometry.Euclidean.Triangle

open InnerProductGeometry

section ex_1

  variable (V: Type)
  variable [NormedAddCommGroup V]
  variable [InnerProductSpace ℝ V]
  variable (a b: V)
  variable (length_a: ‖a‖ = 4 * √3)
  variable (length_b: ‖b‖ = 3)
  variable (right_angle: angle a b = Real.pi / 2)

  theorem t1: ‖a - b‖ = 8 := by
    have H1: ‖a - b‖ * ‖a - b‖ = ‖a‖ * ‖a‖ + ‖b‖ * ‖b‖ - 2 * ‖a‖ * ‖b‖ * Real.cos (angle a b) := by
      exact norm_sub_sq_eq_norm_sq_add_norm_sq_sub_two_mul_norm_mul_norm_mul_cos_angle a b
    rw [right_angle] at H1 --- fails with message "unknown identifier 'right_angle'"
    sorry

end ex_1

[Kyle Miller]

The rule is that theorem automatically only includes variables that are needed for the theorem statement itself. Since right_angle does not appear in the theorem statement, it's not included.

You can force a variable to be included with include right_angle.

[Ilmārs Cīrulis]

Thank you!