-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
σ : R →+* S
E : Type u_4
inst_2 : AddCommGroup E
inst_3 : Module R E
F : Type u_5
inst_4 : AddCommGroup F
inst_5 : Module S F
c : Set (E →ₛₗ.[σ] F)
hc : DirectedOn (fun (x1 x2 : E →ₛₗ.[σ] F) ↦ x1 ≤ x2) c
cne : c.Nonempty
hdir : DirectedOn (fun (x1 x2 : Submodule R E) ↦ x1 ≤ x2) (domain '' c)
P : (x : ↥(sSup (domain '' c))) → { p : (↑c : Type (max u_4 u_5)) // (↑x : E) ∈ (↑p : E →ₛₗ.[σ] F).domain }
f : ↥(sSup (domain '' c)) → F :=
  fun (x : ↥(sSup (domain '' c))) ↦
    (↑(↑(↑(P x) : (↑c : Type (max u_4 u_5))) : E →ₛₗ.[σ] F) :
        ↥(↑(↑(P x) : (↑c : Type (max u_4 u_5))) : E →ₛₗ.[σ] F).domain → F)
      (Subtype.mk (p := fun (x_1 : E) ↦ x_1 ∈ (↑(↑(P x) : (↑c : Type (max u_4 u_5))) : E →ₛₗ.[σ] F).domain) (↑x : E) ⋯)
f_eq :
  ∀ (p : (↑c : Type (max u_4 u_5))) (x : ↥(sSup (domain '' c))) (y : ↥(↑p : E →ₛₗ.[σ] F).domain)
    (_hxy : (↑x : E) = (↑y : E)), f x = (↑(↑p : E →ₛₗ.[σ] F) : ↥(↑p : E →ₛₗ.[σ] F).domain → F) y
x y : ↥(sSup (domain '' c))
p : E →ₛₗ.[σ] F
hpc : p ∈ c
hpx : (↑(↑(P x) : (↑c : Type (max u_4 u_5))) : E →ₛₗ.[σ] F) ≤ p
hpy : (↑(↑(P y) : (↑c : Type (max u_4 u_5))) : E →ₛₗ.[σ] F) ≤ p
x' : ↥p.domain :=
  (inclusion ⋯ : (a : ↥(↑(↑(P x) : (↑c : Type (max u_4 u_5))) : E →ₛₗ.[σ] F).domain) → ↥p.domain)
    (Subtype.mk (p := fun (x_1 : E) ↦ x_1 ∈ (↑(↑(P x) : (↑c : Type (max u_4 u_5))) : E →ₛₗ.[σ] F).domain) (↑x : E) ⋯)
y' : ↥p.domain :=
  (inclusion ⋯ : (a : ↥(↑(↑(P y) : (↑c : Type (max u_4 u_5))) : E →ₛₗ.[σ] F).domain) → ↥p.domain)
    (Subtype.mk (p := fun (x : E) ↦ x ∈ (↑(↑(P y) : (↑c : Type (max u_4 u_5))) : E →ₛₗ.[σ] F).domain) (↑y : E) ⋯)
w :
  f (x + y) =
    (↑(↑(Subtype.mk (p := fun (x : E →ₛₗ.[σ] F) ↦ x ∈ c) p hpc) : E →ₛₗ.[σ] F) : ↥(↑⟨p, hpc⟩ : E →ₛₗ.[σ] F).domain → F)
        x' +
      f y
w₁ :
  f (x + y) =
    (↑(↑(Subtype.mk (p := fun (x : E →ₛₗ.[σ] F) ↦ x ∈ c) p hpc) : E →ₛₗ.[σ] F) : ↥(↑⟨p, hpc⟩ : E →ₛₗ.[σ] F).domain → F)
        x' +
      (↑(↑(Subtype.mk (p := fun (x : E →ₛₗ.[σ] F) ↦ x ∈ c) p hpc) : E →ₛₗ.[σ] F) :
          ↥(↑⟨p, hpc⟩ : E →ₛₗ.[σ] F).domain → F)
        y'
w₂ :
  (↑(↑(Subtype.mk (p := fun (x : E →ₛₗ.[σ] F) ↦ x ∈ c) p hpc) : E →ₛₗ.[σ] F) : ↥(↑⟨p, hpc⟩ : E →ₛₗ.[σ] F).domain → F)
      (x' + y') =
    (↑(↑(Subtype.mk (p := fun (x : E →ₛₗ.[σ] F) ↦ x ∈ c) p hpc) : E →ₛₗ.[σ] F) : ↥(↑⟨p, hpc⟩ : E →ₛₗ.[σ] F).domain → F)
        x' +
      (↑(↑(Subtype.mk (p := fun (x : E →ₛₗ.[σ] F) ↦ x ∈ c) p hpc) : E →ₛₗ.[σ] F) :
          ↥(↑⟨p, hpc⟩ : E →ₛₗ.[σ] F).domain → F)
        y'
⊢ f (x + y) = f x + f y
have w₃ : (↑(↑(Subtype.mk (p := fun (x : E →ₛₗ.[σ] F) ↦ x ∈ c) p hpc) : E →ₛₗ.[σ] F) : ↥(↑⟨p, hpc⟩ : E →ₛₗ.[σ] F).domain → F) x' +
    (↑(↑(Subtype.mk (p := fun (x : E →ₛₗ.[σ] F) ↦ x ∈ c) p hpc) : E →ₛₗ.[σ] F) : ↥(↑⟨p, hpc⟩ : E →ₛₗ.[σ] F).domain → F)
      y' =
  (↑(↑(Subtype.mk (p := fun (x : E →ₛₗ.[σ] F) ↦ x ∈ c) p hpc) : E →ₛₗ.[σ] F) : ↥(↑⟨p, hpc⟩ : E →ₛₗ.[σ] F).domain → F)
      x' +
    (↑(↑(Subtype.mk (p := fun (x : E →ₛₗ.[σ] F) ↦ x ∈ c) p hpc) : E →ₛₗ.[σ] F) : ↥(↑⟨p, hpc⟩ : E →ₛₗ.[σ] F).domain → F)
      y'
Tactic: rw [f_eq ⟨p, hpc⟩ x x' rfl, f_eq ⟨p, hpc⟩ y y' rfl, f_eq ⟨p, hpc⟩ (x + y) (x' + y') rfl,
      map_add]