-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : FiniteDimensional.{u_1, u_2} 𝕜 ↥K
hK : FiniteDimensional.{u_1, u_2} 𝕜 ↥Kᗮ
e : (↥K × ↥Kᗮ) ≃ₗ[𝕜] E := K.prodEquivOfIsCompl Kᗮ ⋯
b : Basis.{0, u_1, u_2} (Fin (finrank.{u_1, u_2} 𝕜 ↥K) ⊕ Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)) 𝕜 (↥K × ↥Kᗮ) :=
  Basis.prod (finBasis 𝕜 ↥K) (finBasis 𝕜 ↥Kᗮ)
this :
  Eq.{u_1 + 1} (α :=
    Matrix (Fin (finrank.{u_1, u_2} 𝕜 ↥K) ⊕ Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ))
      (Fin (finrank.{u_1, u_2} 𝕜 ↥K) ⊕ Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)) 𝕜)
    ((LinearMap.toMatrix b b :
          (a : ↥K × ↥Kᗮ →ₗ[𝕜] ↥K × ↥Kᗮ) →
            Matrix (Fin (finrank 𝕜 ↥K) ⊕ Fin (finrank 𝕜 ↥Kᗮ)) (Fin (finrank 𝕜 ↥K) ⊕ Fin (finrank 𝕜 ↥Kᗮ)) 𝕜)
        ((↑e.symm : E →ₗ[𝕜] ↥K × ↥Kᗮ) ∘ₗ
          (↑K.reflection.toLinearEquiv : E →ₗ[𝕜] E) ∘ₗ (↑e.symm.symm : ↥K × ↥Kᗮ →ₗ[𝕜] E)) :
      Matrix (Fin (finrank.{u_1, u_2} 𝕜 ↥K) ⊕ Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ))
        (Fin (finrank.{u_1, u_2} 𝕜 ↥K) ⊕ Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)) 𝕜)
    (Matrix.fromBlocks 1 0 0 (-1) :
      Matrix (Fin (finrank.{u_1, u_2} 𝕜 ↥K) ⊕ Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ))
        (Fin (finrank.{u_1, u_2} 𝕜 ↥K) ⊕ Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)) 𝕜)
pos :
  (LinearMap.det : (a : ↥K × ↥Kᗮ →ₗ[𝕜] ↥K × ↥Kᗮ) → 𝕜)
      ((↑e.symm : E →ₗ[𝕜] ↥K × ↥Kᗮ) ∘ₗ (↑K.reflection.toLinearEquiv : E →ₗ[𝕜] E) ∘ₗ (↑e.symm.symm : ↥K × ↥Kᗮ →ₗ[𝕜] E)) =
    HPow.hPow (α := 𝕜) (-1) (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)
pos₁ :
  Matrix.det (n := Fin (finrank.{u_1, u_2} 𝕜 ↥K) ⊕ Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ))
      ((LinearMap.toMatrix b b :
          (a : ↥K × ↥Kᗮ →ₗ[𝕜] ↥K × ↥Kᗮ) →
            Matrix (Fin (finrank 𝕜 ↥K) ⊕ Fin (finrank 𝕜 ↥Kᗮ)) (Fin (finrank 𝕜 ↥K) ⊕ Fin (finrank 𝕜 ↥Kᗮ)) 𝕜)
        ((↑e.symm : E →ₗ[𝕜] ↥K × ↥Kᗮ) ∘ₗ
          (↑K.reflection.toLinearEquiv : E →ₗ[𝕜] E) ∘ₗ (↑e.symm.symm : ↥K × ↥Kᗮ →ₗ[𝕜] E))) =
    HPow.hPow (α := 𝕜) (-1) (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)
pos₂ :
  Matrix.det (n := Fin (finrank.{u_1, u_2} 𝕜 ↥K) ⊕ Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)) (Matrix.fromBlocks 1 0 0 (-1)) =
    HPow.hPow (α := 𝕜) (-1) (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)
pos₃ :
  HMul.hMul (α := 𝕜) (Matrix.det (n := Fin (finrank.{u_1, u_2} 𝕜 ↥K)) 1)
      (Matrix.det (n := Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)) (-1)) =
    HPow.hPow (α := 𝕜) (-1) (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)
pos₄ :
  HMul.hMul (α := 𝕜) 1 (Matrix.det (n := Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)) (-1)) =
    HPow.hPow (α := 𝕜) (-1) (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)
pos₅ : Matrix.det (n := Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)) (-1) = HPow.hPow (α := 𝕜) (-1) (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)
pos₆ :
  HPow.hPow (α := 𝕜) (-1) (Fintype.card (Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ))) *
      Matrix.det (n := Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)) 1 =
    HPow.hPow (α := 𝕜) (-1) (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)
pos₇ :
  HPow.hPow (α := 𝕜) (-1) (finrank.{u_1, u_2} 𝕜 ↥Kᗮ) * Matrix.det (n := Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)) 1 =
    HPow.hPow (α := 𝕜) (-1) (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)
pos₈ : HPow.hPow (α := 𝕜) (-1) (finrank.{u_1, u_2} 𝕜 ↥Kᗮ) * 1 = HPow.hPow (α := 𝕜) (-1) (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)
pos₉ pos₁₀ : HPow.hPow (α := 𝕜) (-1) (finrank.{u_1, u_2} 𝕜 ↥Kᗮ) = HPow.hPow (α := 𝕜) (-1) (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)
⊢ (LinearMap.det : (a : E →ₗ[𝕜] E) → 𝕜) (↑K.reflection.toLinearEquiv : E →ₗ[𝕜] E) =
    HPow.hPow (α := 𝕜) (-1) (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)

Tactic:
rw [← LinearMap.det_conj _ e.symm, ← LinearMap.det_toMatrix b, this, Matrix.det_fromBlocks_zero₂₁,
    Matrix.det_one, one_mul, Matrix.det_neg, Fintype.card_fin, Matrix.det_one, mul_one]

Premises used: LinearEquiv.symm, Fintype.card_fin, Matrix.det_neg, LinearMap.det_conj, Matrix.det_fromBlocks_zero₂₁, Matrix.det_one, mul_one, LinearMap.det_toMatrix, one_mul