-- Lean 4 proof step from Mathlib.Algebra.Exact (goal)
Goal:
R_1 : Type u_1
M_1 : Type u_2
M' : Type u_3
N_1 : Type u_4
N' : Type u_5
P_1 : Type u_6
P' : Type u_7
inst : Semiring R_1
inst_1 : AddCommGroup M_1
inst_2 : AddCommGroup N_1
inst_3 : AddCommGroup P_1
inst_4 : Module R_1 M_1
inst_5 : Module R_1 N_1
inst_6 : Module R_1 P_1
f : M_1 →ₗ[R_1] N_1
g : N_1 →ₗ[R_1] P_1
R : Type u_8
M : Type u_9
N : Type u_10
P : Type u_11
inst_7 : Semiring R
inst_8 : AddCommGroup M
inst_9 : AddCommGroup N
inst_10 : AddCommGroup P
inst_11 : Module R M
inst_12 : Module R N
inst_13 : Module R P
e : N ≃ₗ[R] M × P
hg : Surjective.{u_10 + 1, u_11 + 1} (α := N) (β := P) (⇑(snd R M P ∘ₗ (↑e : N →ₗ[R] M × P)) : (a : N) → P)
h :
  Exact.{u_9, u_10, u_11} (M := M) (N := N) (P := P) (⇑((↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P) : (a : M) → N)
    (⇑(snd R M P ∘ₗ (↑e : N →ₗ[R] M × P)) : (a : N) → P)
refine_5 :
  ∀ (x : N),
    Eq.{u_9 + 1} (α := M)
      (((↑((fun (l : { l : N →ₗ[R] M // l ∘ₗ (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P = LinearMap.id }) ↦
                    (Subtype.mk (p := fun (e_1 : N ≃ₗ[R] M × P) ↦
                        (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P = (↑e_1.symm : M × P →ₗ[R] N) ∘ₗ inl R M P ∧
                          snd R M P ∘ₗ (↑e : N →ₗ[R] M × P) = snd R M P ∘ₗ (↑e_1 : N →ₗ[R] M × P))
                        (LinearEquiv.ofBijective ((↑l : N →ₗ[R] M).prod (snd R M P ∘ₗ (↑e : N →ₗ[R] M × P))) ⋯) ⋯ :
                      { e_1 : N ≃ₗ[R] M × P //
                        (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P = (↑e_1.symm : M × P →ₗ[R] N) ∘ₗ inl R M P ∧
                          snd R M P ∘ₗ (↑e : N →ₗ[R] M × P) = snd R M P ∘ₗ (↑e_1 : N →ₗ[R] M × P) }))
                  ((fun
                        (e_1 :
                          { e_1 : N ≃ₗ[R] M × P //
                            (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P = (↑e_1.symm : M × P →ₗ[R] N) ∘ₗ inl R M P ∧
                              snd R M P ∘ₗ (↑e : N →ₗ[R] M × P) = snd R M P ∘ₗ (↑e_1 : N →ₗ[R] M × P) }) ↦
                      (Subtype.mk (p := fun (l : N →ₗ[R] M) ↦
                          l ∘ₗ (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P = LinearMap.id)
                          (fst R M P ∘ₗ (↑(↑e_1 : N ≃ₗ[R] M × P) : N →ₗ[R] M × P)) ⋯ :
                        { l : N →ₗ[R] M // l ∘ₗ (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P = LinearMap.id }))
                    (Subtype.mk (p := fun (e_1 : N ≃ₗ[R] M × P) ↦
                      (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P = (↑e_1.symm : M × P →ₗ[R] N) ∘ₗ inl R M P ∧
                        snd R M P ∘ₗ (↑e : N →ₗ[R] M × P) = snd R M P ∘ₗ (↑e_1 : N →ₗ[R] M × P))
                      e ⋯))) :
              N ≃ₗ[R] M × P) :
            (a : N) → M × P)
          x).1
      (((↑(Subtype.mk (p := fun (e_1 : N ≃ₗ[R] M × P) ↦
                  (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P = (↑e_1.symm : M × P →ₗ[R] N) ∘ₗ inl R M P ∧
                    snd R M P ∘ₗ (↑e : N →ₗ[R] M × P) = snd R M P ∘ₗ (↑e_1 : N →ₗ[R] M × P))
                  e ⋯) :
              N ≃ₗ[R] M × P) :
            (a : N) → M × P)
          x).1
⊢ Eq (α :=
    { e_1 : N ≃ₗ[R] M × P //
      (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P = (↑e_1.symm : M × P →ₗ[R] N) ∘ₗ inl R M P ∧
        snd R M P ∘ₗ (↑e : N →ₗ[R] M × P) = snd R M P ∘ₗ (↑e_1 : N →ₗ[R] M × P) })
    ((fun (l : { l : N →ₗ[R] M // l ∘ₗ (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P = LinearMap.id }) ↦
        (Subtype.mk (p := fun (e_1 : N ≃ₗ[R] M × P) ↦
            (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P = (↑e_1.symm : M × P →ₗ[R] N) ∘ₗ inl R M P ∧
              snd R M P ∘ₗ (↑e : N →ₗ[R] M × P) = snd R M P ∘ₗ (↑e_1 : N →ₗ[R] M × P))
            (LinearEquiv.ofBijective ((↑l : N →ₗ[R] M).prod (snd R M P ∘ₗ (↑e : N →ₗ[R] M × P))) ⋯) ⋯ :
          { e_1 : N ≃ₗ[R] M × P //
            (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P = (↑e_1.symm : M × P →ₗ[R] N) ∘ₗ inl R M P ∧
              snd R M P ∘ₗ (↑e : N →ₗ[R] M × P) = snd R M P ∘ₗ (↑e_1 : N →ₗ[R] M × P) }))
      ((fun
            (e_1 :
              { e_1 : N ≃ₗ[R] M × P //
                (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P = (↑e_1.symm : M × P →ₗ[R] N) ∘ₗ inl R M P ∧
                  snd R M P ∘ₗ (↑e : N →ₗ[R] M × P) = snd R M P ∘ₗ (↑e_1 : N →ₗ[R] M × P) }) ↦
          (Subtype.mk (p := fun (l : N →ₗ[R] M) ↦ l ∘ₗ (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P = LinearMap.id)
              (fst R M P ∘ₗ (↑(↑e_1 : N ≃ₗ[R] M × P) : N →ₗ[R] M × P)) ⋯ :
            { l : N →ₗ[R] M // l ∘ₗ (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P = LinearMap.id }))
        (Subtype.mk (p := fun (e_1 : N ≃ₗ[R] M × P) ↦
          (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P = (↑e_1.symm : M × P →ₗ[R] N) ∘ₗ inl R M P ∧
            snd R M P ∘ₗ (↑e : N →ₗ[R] M × P) = snd R M P ∘ₗ (↑e_1 : N →ₗ[R] M × P))
          e ⋯)))
    (Subtype.mk (p := fun (e_1 : N ≃ₗ[R] M × P) ↦
      (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P = (↑e_1.symm : M × P →ₗ[R] N) ∘ₗ inl R M P ∧
        snd R M P ∘ₗ (↑e : N →ₗ[R] M × P) = snd R M P ∘ₗ (↑e_1 : N →ₗ[R] M × P))
      e ⋯)
have refine_5₁ : ∀ (x : N),
  Eq.{u_11 + 1} (α := P)
    (((↑((fun (l : { l : N →ₗ[R] M // l ∘ₗ (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P = LinearMap.id }) ↦
                  (Subtype.mk (p := fun (e_1 : N ≃ₗ[R] M × P) ↦
                      (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P = (↑e_1.symm : M × P →ₗ[R] N) ∘ₗ inl R M P ∧
                        snd R M P ∘ₗ (↑e : N →ₗ[R] M × P) = snd R M P ∘ₗ (↑e_1 : N →ₗ[R] M × P))
                      (LinearEquiv.ofBijective ((↑l : N →ₗ[R] M).prod (snd R M P ∘ₗ (↑e : N →ₗ[R] M × P))) sorry) sorry :
                    { e_1 : N ≃ₗ[R] M × P //
                      (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P = (↑e_1.symm : M × P →ₗ[R] N) ∘ₗ inl R M P ∧
                        snd R M P ∘ₗ (↑e : N →ₗ[R] M × P) = snd R M P ∘ₗ (↑e_1 : N →ₗ[R] M × P) }))
                ((fun
                      (e_1 :
                        { e_1 : N ≃ₗ[R] M × P //
                          (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P = (↑e_1.symm : M × P →ₗ[R] N) ∘ₗ inl R M P ∧
                            snd R M P ∘ₗ (↑e : N →ₗ[R] M × P) = snd R M P ∘ₗ (↑e_1 : N →ₗ[R] M × P) }) ↦
                    (Subtype.mk (p := fun (l : N →ₗ[R] M) ↦ l ∘ₗ (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P = LinearMap.id)
                        (fst R M P ∘ₗ (↑(↑e_1 : N ≃ₗ[R] M × P) : N →ₗ[R] M × P)) sorry :
                      { l : N →ₗ[R] M // l ∘ₗ (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P = LinearMap.id }))
                  (Subtype.mk (p := fun (e_1 : N ≃ₗ[R] M × P) ↦
                    (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P = (↑e_1.symm : M × P →ₗ[R] N) ∘ₗ inl R M P ∧
                      snd R M P ∘ₗ (↑e : N →ₗ[R] M × P) = snd R M P ∘ₗ (↑e_1 : N →ₗ[R] M × P))
                    e sorry))) :
            N ≃ₗ[R] M × P) :
          (a : N) → M × P)
        x).2
    (((↑(Subtype.mk (p := fun (e_1 : N ≃ₗ[R] M × P) ↦
                (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P = (↑e_1.symm : M × P →ₗ[R] N) ∘ₗ inl R M P ∧
                  snd R M P ∘ₗ (↑e : N →ₗ[R] M × P) = snd R M P ∘ₗ (↑e_1 : N →ₗ[R] M × P))
                e sorry) :
            N ≃ₗ[R] M × P) :
          (a : N) → M × P)
        x).2
Tactic: ext x