-- Lean 4 proof step from Mathlib.Algebra.Star.Module (goal)
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : StarMul R
inst_2 : TrivialStar R
inst_3 : AddCommGroup A
inst_4 : Module R A
inst_5 : StarAddMonoid A
inst_6 : StarModule R A
inst_7 : Invertible (α := R) 2
hl :
  ∀ (x : ↥(selfAdjoint A)),
    Eq.{u_2 + 1} (α := A)
      (↑((((LinearMap.prod (selfAdjointPart R) (skewAdjointPart R) ∘ₗ
                        LinearMap.coprod (Submodule.subtype (selfAdjoint.submodule R A))
                          (Submodule.subtype (skewAdjoint.submodule R A)) :
                      ↥(selfAdjoint A) × ↥(skewAdjoint A) →ₗ[R] ↥(selfAdjoint A) × ↥(skewAdjoint A)) ∘ₗ
                    (LinearMap.inl R ↥(selfAdjoint A) ↥(skewAdjoint A) :
                      ↥(selfAdjoint A) →ₗ[R] ↥(selfAdjoint A) × ↥(skewAdjoint A)) :
                  ↥(selfAdjoint A) →ₗ[R] ↥(selfAdjoint A) × ↥(skewAdjoint A)) :
                (a : ↥(selfAdjoint A)) → ↥(selfAdjoint A) × ↥(skewAdjoint A))
              x).1 :
        A)
      (↑((LinearMap.id ∘ₗ LinearMap.inl R ↥(selfAdjoint A) ↥(skewAdjoint A) :
                (a : ↥(selfAdjoint A)) → ↥(selfAdjoint A) × ↥(skewAdjoint A))
              x).1 :
        A)
hl₁ :
  ∀ (x : ↥(selfAdjoint A)),
    Eq.{u_2 + 1} (α := A)
      (↑((((LinearMap.prod (selfAdjointPart R) (skewAdjointPart R) ∘ₗ
                        LinearMap.coprod (Submodule.subtype (selfAdjoint.submodule R A))
                          (Submodule.subtype (skewAdjoint.submodule R A)) :
                      ↥(selfAdjoint A) × ↥(skewAdjoint A) →ₗ[R] ↥(selfAdjoint A) × ↥(skewAdjoint A)) ∘ₗ
                    (LinearMap.inl R ↥(selfAdjoint A) ↥(skewAdjoint A) :
                      ↥(selfAdjoint A) →ₗ[R] ↥(selfAdjoint A) × ↥(skewAdjoint A)) :
                  ↥(selfAdjoint A) →ₗ[R] ↥(selfAdjoint A) × ↥(skewAdjoint A)) :
                (a : ↥(selfAdjoint A)) → ↥(selfAdjoint A) × ↥(skewAdjoint A))
              x).2 :
        A)
      (↑((LinearMap.id ∘ₗ LinearMap.inl R ↥(selfAdjoint A) ↥(skewAdjoint A) :
                (a : ↥(selfAdjoint A)) → ↥(selfAdjoint A) × ↥(skewAdjoint A))
              x).2 :
        A)
⊢ Eq (α := ↥(selfAdjoint A) × ↥(skewAdjoint A) →ₗ[R] ↥(selfAdjoint A) × ↥(skewAdjoint A))
    (LinearMap.prod (selfAdjointPart R) (skewAdjointPart R) ∘ₗ
        LinearMap.coprod (Submodule.subtype (selfAdjoint.submodule R A))
          (Submodule.subtype (skewAdjoint.submodule R A)) :
      ↥(selfAdjoint A) × ↥(skewAdjoint A) →ₗ[R] ↥(selfAdjoint A) × ↥(skewAdjoint A))
    (LinearMap.id : ↥(selfAdjoint A) × ↥(skewAdjoint A) →ₗ[R] ↥(selfAdjoint A) × ↥(skewAdjoint A))
have hr : ∀ (x : ↥(skewAdjoint A)),
  Eq.{u_2 + 1} (α := A)
    (↑((((LinearMap.prod (selfAdjointPart R) (skewAdjointPart R) ∘ₗ
                      LinearMap.coprod (Submodule.subtype (selfAdjoint.submodule R A))
                        (Submodule.subtype (skewAdjoint.submodule R A)) :
                    ↥(selfAdjoint A) × ↥(skewAdjoint A) →ₗ[R] ↥(selfAdjoint A) × ↥(skewAdjoint A)) ∘ₗ
                  (LinearMap.inr R ↥(selfAdjoint A) ↥(skewAdjoint A) :
                    ↥(skewAdjoint A) →ₗ[R] ↥(selfAdjoint A) × ↥(skewAdjoint A)) :
                ↥(skewAdjoint A) →ₗ[R] ↥(selfAdjoint A) × ↥(skewAdjoint A)) :
              (a : ↥(skewAdjoint A)) → ↥(selfAdjoint A) × ↥(skewAdjoint A))
            x).1 :
      A)
    (↑((LinearMap.id ∘ₗ LinearMap.inr R ↥(selfAdjoint A) ↥(skewAdjoint A) :
              (a : ↥(skewAdjoint A)) → ↥(selfAdjoint A) × ↥(skewAdjoint A))
            x).1 :
      A)
Tactic: ext x