-- 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ᗮ)
a :
  ∀ (val val_1 : Fin (finrank.{u_1, u_2} 𝕜 ↥K)),
    Eq.{u_1 + 1} (α := 𝕜)
      ((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))
          (Sum.inl val) (Sum.inl val_1) :
        𝕜)
      (Matrix.fromBlocks (m := Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)) (o := Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)) 1 0 0 (-1)
          (Sum.inl val) (Sum.inl val_1) :
        𝕜)
a₁ :
  ∀ (val : Fin (finrank.{u_1, u_2} 𝕜 ↥K)) (val_1 : Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)),
    Eq.{u_1 + 1} (α := 𝕜)
      ((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))
          (Sum.inl val) (Sum.inr val_1) :
        𝕜)
      (Matrix.fromBlocks (l := Fin (finrank.{u_1, u_2} 𝕜 ↥K)) (o := Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)) 1 0 0 (-1)
          (Sum.inl val) (Sum.inr val_1) :
        𝕜)
a₂ :
  ∀ (val : Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)) (val_1 : Fin (finrank.{u_1, u_2} 𝕜 ↥K)),
    Eq.{u_1 + 1} (α := 𝕜)
      ((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))
          (Sum.inr val) (Sum.inl val_1) :
        𝕜)
      (Matrix.fromBlocks (m := Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)) (n := Fin (finrank.{u_1, u_2} 𝕜 ↥K)) 1 0 0 (-1)
          (Sum.inr val) (Sum.inl val_1) :
        𝕜)
⊢ 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ᗮ)) 𝕜)
have a₃ : ∀ (val val_1 : Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)),
  Eq.{u_1 + 1} (α := 𝕜)
    ((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))
        (Sum.inr val) (Sum.inr val_1) :
      𝕜)
    (Matrix.fromBlocks (l := Fin (finrank.{u_1, u_2} 𝕜 ↥K)) (n := Fin (finrank.{u_1, u_2} 𝕜 ↥K)) 1 0 0 (-1)
        (Sum.inr val) (Sum.inr val_1) :
      𝕜)
Tactic: ext (_ | _) (_ | _)