-- Lean 4 proof step from Mathlib.Algebra.Exact (goal)
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
P : Type u_6
P' : Type u_7
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
e : N ≃ₗ[R] M × P
hf : Injective.{u_2 + 1, u_4 + 1} (α := M) (β := N) (⇑((↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P) : (a : M) → N)
h :
  Exact.{u_2, u_4, u_6} (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)
x : M × P
⊢ Eq (α := M × P)
    ((e : (a : N) → M × P)
        ((LinearEquiv.symm
              (↑((fun (l : { l : P →ₗ[R] N // (snd R M P ∘ₗ (↑e : N →ₗ[R] M × P)) ∘ₗ l = 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.symm
                            (LinearEquiv.ofBijective
                              (((↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P) ∘ₗ fst R M P + (↑l : P →ₗ[R] N) ∘ₗ snd 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 : P →ₗ[R] N) ↦ (snd R M P ∘ₗ (↑e : N →ₗ[R] M × P)) ∘ₗ l = LinearMap.id)
                            ((↑(↑e_1 : N ≃ₗ[R] M × P).symm : M × P →ₗ[R] N) ∘ₗ inr R M P) ⋯ :
                          { l : P →ₗ[R] N // (snd R M P ∘ₗ (↑e : N →ₗ[R] M × P)) ∘ₗ l = 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 : M × P) → N)
          x) :
      M × P)
    ((e : (a : N) → M × P)
        (((↑(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).symm :
            (a : M × P) → N)
          x) :
      M × P)
have refine_5 : Eq.{u_2 + 1} (α := M)
  ((e : (a : N) → M × P)
      ((LinearEquiv.symm
            (↑((fun (l : { l : P →ₗ[R] N // (snd R M P ∘ₗ (↑e : N →ₗ[R] M × P)) ∘ₗ l = 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.symm
                          (LinearEquiv.ofBijective
                            (((↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P) ∘ₗ fst R M P + (↑l : P →ₗ[R] N) ∘ₗ snd 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 : P →ₗ[R] N) ↦ (snd R M P ∘ₗ (↑e : N →ₗ[R] M × P)) ∘ₗ l = LinearMap.id)
                          ((↑(↑e_1 : N ≃ₗ[R] M × P).symm : M × P →ₗ[R] N) ∘ₗ inr R M P) sorry :
                        { l : P →ₗ[R] N // (snd R M P ∘ₗ (↑e : N →ₗ[R] M × P)) ∘ₗ l = 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 : M × P) → N)
        x)).1
  ((e : (a : N) → M × P)
      (((↑(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).symm :
          (a : M × P) → N)
        x)).1
Tactic: ext