Theorem: Iran1998P9.compute_norm (Compfiles/Iran1998P9.lean)

State before:
v : EuclideanSpace ℝ (Fin 3)
⊢ ‖v‖ = √(∑ i : Fin 3, v i ^ 2)
Tactic:
rw[EuclideanSpace.norm_eq v]
State after:
v : EuclideanSpace ℝ (Fin 3)
⊢ √(∑ i : Fin 3, ‖v i‖ ^ 2) = √(∑ i : Fin 3, v i ^ 2)

State before:
v : EuclideanSpace ℝ (Fin 3)
⊢ √(∑ i : Fin 3, ‖v i‖ ^ 2) = √(∑ i : Fin 3, v i ^ 2)
Tactic:
congr
State after:
case e_x.e_f
v : EuclideanSpace ℝ (Fin 3)
⊢ (fun i => ‖v i‖ ^ 2) = fun i => v i ^ 2

State before:
case e_x.e_f
v : EuclideanSpace ℝ (Fin 3)
⊢ (fun i => ‖v i‖ ^ 2) = fun i => v i ^ 2
Tactic:
ext
State after:
case e_x.e_f.h
v : EuclideanSpace ℝ (Fin 3)
x✝ : Fin 3
⊢ ‖v x✝‖ ^ 2 = v x✝ ^ 2

State before:
case e_x.e_f.h
v : EuclideanSpace ℝ (Fin 3)
x✝ : Fin 3
⊢ ‖v x✝‖ ^ 2 = v x✝ ^ 2
Tactic:
rw [Real.norm_eq_abs, sq_abs]
State after:
no goals