-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
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ᗮ)
⊢ (LinearMap.det : (a : E →ₗ[𝕜] E) → 𝕜) (↑K.reflection.toLinearEquiv : E →ₗ[𝕜] E) =
    HPow.hPow (α := 𝕜) (-1) (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)
have 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ᗮ)
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]