-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.CrossProduct (goal)
Goal:
a b : EuclideanSpace ℝ (Fin 3)
this : 0 ≤ sin (angle a b)
simp_rw :
  (RCLike.re : (a : ℝ) → ℝ)
      (inner ℝ (E := WithLp 2 (Fin 3 → ℝ))
        (toLp 2
            ((((crossProduct : (a : Fin 3 → ℝ) → (Fin 3 → ℝ) →ₗ[ℝ] Fin 3 → ℝ) a.ofLp : (Fin 3 → ℝ) →ₗ[ℝ] Fin 3 → ℝ) :
                (a : Fin 3 → ℝ) → Fin 3 → ℝ)
              b.ofLp) :
          WithLp 2 (Fin 3 → ℝ))
        (toLp 2
            ((((crossProduct : (a : Fin 3 → ℝ) → (Fin 3 → ℝ) →ₗ[ℝ] Fin 3 → ℝ) a.ofLp : (Fin 3 → ℝ) →ₗ[ℝ] Fin 3 → ℝ) :
                (a : Fin 3 → ℝ) → Fin 3 → ℝ)
              b.ofLp) :
          WithLp 2 (Fin 3 → ℝ))) =
    HMul.hMul (α := ℝ) (β := ℝ) ((RCLike.re : (a : ℝ) → ℝ) ⟪a, a⟫ : ℝ) ((RCLike.re : (a : ℝ) → ℝ) ⟪b, b⟫ : ℝ) -
      HPow.hPow (β := ℕ) ⟪a, b⟫ 2
simp_rw₁ :
  (RCLike.re : (a : ℝ) → ℝ)
      (dotProduct (m := Fin 3)
        ((((crossProduct : (a : Fin 3 → ℝ) → (Fin 3 → ℝ) →ₗ[ℝ] Fin 3 → ℝ) a.ofLp : (Fin 3 → ℝ) →ₗ[ℝ] Fin 3 → ℝ) :
            (a : Fin 3 → ℝ) → Fin 3 → ℝ)
          b.ofLp)
        (star
          ((((crossProduct : (a : Fin 3 → ℝ) → (Fin 3 → ℝ) →ₗ[ℝ] Fin 3 → ℝ) a.ofLp : (Fin 3 → ℝ) →ₗ[ℝ] Fin 3 → ℝ) :
              (a : Fin 3 → ℝ) → Fin 3 → ℝ)
            b.ofLp))) =
    HMul.hMul (α := ℝ) (β := ℝ) ((RCLike.re : (a : ℝ) → ℝ) (a.ofLp ⬝ᵥ star a.ofLp) : ℝ)
        ((RCLike.re : (a : ℝ) → ℝ) (b.ofLp ⬝ᵥ star b.ofLp) : ℝ) -
      HPow.hPow (β := ℕ) (b.ofLp ⬝ᵥ star a.ofLp) 2
simp_rw₂ :
  (RCLike.re : (a : ℝ) → ℝ)
      (dotProduct (m := Fin 3)
        ((((crossProduct : (a : Fin 3 → ℝ) → (Fin 3 → ℝ) →ₗ[ℝ] Fin 3 → ℝ) a.ofLp : (Fin 3 → ℝ) →ₗ[ℝ] Fin 3 → ℝ) :
            (a : Fin 3 → ℝ) → Fin 3 → ℝ)
          b.ofLp)
        ((((crossProduct : (a : Fin 3 → ℝ) → (Fin 3 → ℝ) →ₗ[ℝ] Fin 3 → ℝ) a.ofLp : (Fin 3 → ℝ) →ₗ[ℝ] Fin 3 → ℝ) :
            (a : Fin 3 → ℝ) → Fin 3 → ℝ)
          b.ofLp)) =
    HMul.hMul (α := ℝ) (β := ℝ) ((RCLike.re : (a : ℝ) → ℝ) (a.ofLp ⬝ᵥ a.ofLp) : ℝ)
        ((RCLike.re : (a : ℝ) → ℝ) (b.ofLp ⬝ᵥ b.ofLp) : ℝ) -
      HPow.hPow (β := ℕ) (b.ofLp ⬝ᵥ a.ofLp) 2
simp_rw₃ :
  dotProduct (m := Fin 3)
      ((((crossProduct : (a : Fin 3 → ℝ) → (Fin 3 → ℝ) →ₗ[ℝ] Fin 3 → ℝ) a.ofLp : (Fin 3 → ℝ) →ₗ[ℝ] Fin 3 → ℝ) :
          (a : Fin 3 → ℝ) → Fin 3 → ℝ)
        b.ofLp)
      ((((crossProduct : (a : Fin 3 → ℝ) → (Fin 3 → ℝ) →ₗ[ℝ] Fin 3 → ℝ) a.ofLp : (Fin 3 → ℝ) →ₗ[ℝ] Fin 3 → ℝ) :
          (a : Fin 3 → ℝ) → Fin 3 → ℝ)
        b.ofLp) =
    a.ofLp ⬝ᵥ a.ofLp * b.ofLp ⬝ᵥ b.ofLp - HPow.hPow (β := ℕ) (b.ofLp ⬝ᵥ a.ofLp) 2
simp_rw₄ :
  a.ofLp ⬝ᵥ a.ofLp * b.ofLp ⬝ᵥ b.ofLp - a.ofLp ⬝ᵥ b.ofLp * b.ofLp ⬝ᵥ a.ofLp =
    a.ofLp ⬝ᵥ a.ofLp * b.ofLp ⬝ᵥ b.ofLp - HPow.hPow (β := ℕ) (b.ofLp ⬝ᵥ a.ofLp) 2
⊢ HPow.hPow (β := ℕ)
      (Norm.norm (E := WithLp 2 (Fin 3 → ℝ))
        (toLp 2
            ((((crossProduct : (a : Fin 3 → ℝ) → (Fin 3 → ℝ) →ₗ[ℝ] Fin 3 → ℝ) a.ofLp : (Fin 3 → ℝ) →ₗ[ℝ] Fin 3 → ℝ) :
                (a : Fin 3 → ℝ) → Fin 3 → ℝ)
              b.ofLp) :
          WithLp 2 (Fin 3 → ℝ)))
      2 =
    HPow.hPow (β := ℕ) ‖a‖ 2 * HPow.hPow (β := ℕ) ‖b‖ 2 - HPow.hPow (β := ℕ) ⟪a, b⟫ 2
have simp_rw₅ : a.ofLp ⬝ᵥ a.ofLp * b.ofLp ⬝ᵥ b.ofLp - a.ofLp ⬝ᵥ b.ofLp * a.ofLp ⬝ᵥ b.ofLp =
  a.ofLp ⬝ᵥ a.ofLp * b.ofLp ⬝ᵥ b.ofLp - HPow.hPow (β := ℕ) (a.ofLp ⬝ᵥ b.ofLp) 2
Tactic: simp_rw [norm_sq_eq_re_inner (𝕜 := ℝ), EuclideanSpace.inner_eq_star_dotProduct, star_trivial,
      RCLike.re_to_real, cross_dot_cross, dotProduct_comm (ofLp b) (ofLp a), sq]