-- Mathlib/LinearAlgebra/LinearPMap.lean
theorem sSup_aux (c : Set (E →ₗ.[R] F)) (hc : DirectedOn (· ≤ ·) c) :
    ∃ f : ↥(sSup (domain '' c)) →ₗ[R] F, (⟨_, f⟩ : E →ₗ.[R] F) ∈ upperBounds c

Proof state:
case inl
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
c : Set (E →ₗ.[R] F)
hc : DirectedOn (fun x1 x2 => x1 ≤ x2) c
ceq : c = ∅
⊢ ∃ f, { domain := sSup (domain '' c), toFun := f } ∈ upperBounds c

Tactic:
subst c

Result:
case inl
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
hc : DirectedOn (fun x1 x2 => x1 ≤ x2) ∅
⊢ ∃ f, { domain := sSup (domain '' ∅), toFun := f } ∈ upperBounds ∅

Proof state:
case inr
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
c : Set (E →ₗ.[R] F)
hc : DirectedOn (fun x1 x2 => x1 ≤ x2) c
cne : c.Nonempty
hdir : DirectedOn (fun x1 x2 => x1 ≤ x2) (domain '' c)
P : (x : ↥(sSup (domain '' c))) → { p // ↑x ∈ (↑p).domain }
f : ↥(sSup (domain '' c)) → F := fun x => ↑↑↑(P x) ⟨↑x, ⋯⟩
f_eq : ∀ (p : ↑c) (x : ↥(sSup (domain '' c))) (y : ↥(↑p).domain), ↑x = ↑y → f x = ↑↑p y
⊢ ∃ f, { domain := sSup (domain '' c), toFun := f } ∈ upperBounds c

Tactic:
use { toFun := f, map_add' := ?_, map_smul' := ?_ }, ?_

Result:
case w.refine_1
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
c : Set (E →ₗ.[R] F)
hc : DirectedOn (fun x1 x2 => x1 ≤ x2) c
cne : c.Nonempty
hdir : DirectedOn (fun x1 x2 => x1 ≤ x2) (domain '' c)
P : (x : ↥(sSup (domain '' c))) → { p // ↑x ∈ (↑p).domain }
f : ↥(sSup (domain '' c)) → F := fun x => ↑↑↑(P x) ⟨↑x, ⋯⟩
f_eq : ∀ (p : ↑c) (x : ↥(sSup (domain '' c))) (y : ↥(↑p).domain), ↑x = ↑y → f x = ↑↑p y
⊢ ∀ (x y : ↥(sSup (domain '' c))), f (x + y) = f x + f y

case w.refine_2
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
c : Set (E →ₗ.[R] F)
hc : DirectedOn (fun x1 x2 => x1 ≤ x2) c
cne : c.Nonempty
hdir : DirectedOn (fun x1 x2 => x1 ≤ x2) (domain '' c)
P : (x : ↥(sSup (domain '' c))) → { p // ↑x ∈ (↑p).domain }
f : ↥(sSup (domain '' c)) → F := fun x => ↑↑↑(P x) ⟨↑x, ⋯⟩
f_eq : ∀ (p : ↑c) (x : ↥(sSup (domain '' c))) (y : ↥(↑p).domain), ↑x = ↑y → f x = ↑↑p y
⊢ ∀ (m : R) (x : ↥(sSup (domain '' c))),
    { toFun := f, map_add' := ?w.refine_1 }.toFun (m • x) =
      (RingHom.id R) m • { toFun := f, map_add' := ?w.refine_1 }.toFun x

case h
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
c : Set (E →ₗ.[R] F)
hc : DirectedOn (fun x1 x2 => x1 ≤ x2) c
cne : c.Nonempty
hdir : DirectedOn (fun x1 x2 => x1 ≤ x2) (domain '' c)
P : (x : ↥(sSup (domain '' c))) → { p // ↑x ∈ (↑p).domain }
f : ↥(sSup (domain '' c)) → F := fun x => ↑↑↑(P x) ⟨↑x, ⋯⟩
f_eq : ∀ (p : ↑c) (x : ↥(sSup (domain '' c))) (y : ↥(↑p).domain), ↑x = ↑y → f x = ↑↑p y
⊢ { domain := sSup (domain '' c), toFun := { toFun := f, map_add' := ?w.refine_1, map_smul' := ?w.refine_2 } } ∈
    upperBounds c

Proof state:
case intro.intro.intro
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
c : Set (E →ₗ.[R] F)
hc : DirectedOn (fun x1 x2 => x1 ≤ x2) c
cne : c.Nonempty
hdir : DirectedOn (fun x1 x2 => x1 ≤ x2) (domain '' c)
P : (x : ↥(sSup (domain '' c))) → { p // ↑x ∈ (↑p).domain }
f : ↥(sSup (domain '' c)) → F := fun x => ↑↑↑(P x) ⟨↑x, ⋯⟩
p : ↑c
x : ↥(sSup (domain '' c))
y : ↥(↑p).domain
hxy : ↑x = ↑y
q : E →ₗ.[R] F
_hqc : q ∈ c
hxq : ↑↑(P x) ≤ q
hpq : ↑p ≤ q
⊢ f x = ↑↑p y

Tactic:
convert (hxq.2 _).trans (hpq.2 _).symm <;> [skip; exact inclusion hpq.1 y; rfl]

Result:
case intro.intro.intro.convert_2
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
c : Set (E →ₗ.[R] F)
hc : DirectedOn (fun x1 x2 => x1 ≤ x2) c
cne : c.Nonempty
hdir : DirectedOn (fun x1 x2 => x1 ≤ x2) (domain '' c)
P : (x : ↥(sSup (domain '' c))) → { p // ↑x ∈ (↑p).domain }
f : ↥(sSup (domain '' c)) → F := fun x => ↑↑↑(P x) ⟨↑x, ⋯⟩
p : ↑c
x : ↥(sSup (domain '' c))
y : ↥(↑p).domain
hxy : ↑x = ↑y
q : E →ₗ.[R] F
_hqc : q ∈ c
hxq : ↑↑(P x) ≤ q
hpq : ↑p ≤ q
⊢ ↑⟨↑x, ⋯⟩ = ↑((inclusion ⋯) y)

Proof state:
case h
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
c : Set (E →ₗ.[R] F)
hc : DirectedOn (fun x1 x2 => x1 ≤ x2) c
cne : c.Nonempty
hdir : DirectedOn (fun x1 x2 => x1 ≤ x2) (domain '' c)
P : (x : ↥(sSup (domain '' c))) → { p // ↑x ∈ (↑p).domain }
f : ↥(sSup (domain '' c)) → F := fun x => ↑↑↑(P x) ⟨↑x, ⋯⟩
f_eq : ∀ (p : ↑c) (x : ↥(sSup (domain '' c))) (y : ↥(↑p).domain), ↑x = ↑y → f x = ↑↑p y
p : E →ₗ.[R] F
hpc : p ∈ c
⊢ p ≤ { domain := sSup (domain '' c), toFun := { toFun := f, map_add' := ⋯, map_smul' := ⋯ } }

Tactic:
refine ⟨le_sSup <| Set.mem_image_of_mem domain hpc, fun x y hxy => Eq.symm ?_⟩

Result:
case h
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
c : Set (E →ₗ.[R] F)
hc : DirectedOn (fun x1 x2 => x1 ≤ x2) c
cne : c.Nonempty
hdir : DirectedOn (fun x1 x2 => x1 ≤ x2) (domain '' c)
P : (x : ↥(sSup (domain '' c))) → { p // ↑x ∈ (↑p).domain }
f : ↥(sSup (domain '' c)) → F := fun x => ↑↑↑(P x) ⟨↑x, ⋯⟩
f_eq : ∀ (p : ↑c) (x : ↥(sSup (domain '' c))) (y : ↥(↑p).domain), ↑x = ↑y → f x = ↑↑p y
p : E →ₗ.[R] F
hpc : p ∈ c
x : ↥p.domain
y : ↥{ domain := sSup (domain '' c), toFun := { toFun := f, map_add' := ⋯, map_smul' := ⋯ } }.domain
hxy : ↑x = ↑y
⊢ ↑{ domain := sSup (domain '' c), toFun := { toFun := f, map_add' := ⋯, map_smul' := ⋯ } } y = ↑p x

Proof state:
case h
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
c : Set (E →ₗ.[R] F)
hc : DirectedOn (fun x1 x2 => x1 ≤ x2) c
cne : c.Nonempty
hdir : DirectedOn (fun x1 x2 => x1 ≤ x2) (domain '' c)
x : ↥(sSup (domain '' c))
⊢ ∃ x_1, ↑x ∈ (↑x_1).domain

Tactic:
have := (mem_sSup_of_directed (cne.image _) hdir).1 x.2

Result:
case h
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
c : Set (E →ₗ.[R] F)
hc : DirectedOn (fun x1 x2 => x1 ≤ x2) c
cne : c.Nonempty
hdir : DirectedOn (fun x1 x2 => x1 ≤ x2) (domain '' c)
x : ↥(sSup (domain '' c))
this : ∃ y ∈ domain '' c, ↑x ∈ y
⊢ ∃ x_1, ↑x ∈ (↑x_1).domain