-- 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:
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
⊢ ∃ f, { domain := sSup (domain '' c), toFun := f } ∈ upperBounds c

Tactic:
rcases c.eq_empty_or_nonempty with ceq | cne

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
c : Set (E →ₗ.[R] F)
hc : DirectedOn (fun x1 x2 => x1 ≤ x2) c
ceq : c = ∅
⊢ ∃ f, { domain := sSup (domain '' c), toFun := f } ∈ upperBounds c

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
⊢ ∃ f, { domain := sSup (domain '' c), toFun := f } ∈ upperBounds c

Proof state:
case w.refine_1.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, ⋯⟩
f_eq : ∀ (p : ↑c) (x : ↥(sSup (domain '' c))) (y : ↥(↑p).domain), ↑x = ↑y → f x = ↑↑p y
x y : ↥(sSup (domain '' c))
p : E →ₗ.[R] F
hpc : p ∈ c
hpx : ↑↑(P x) ≤ p
hpy : ↑↑(P y) ≤ p
⊢ f (x + y) = f x + f y

Tactic:
set x' := inclusion hpx.1 ⟨x, (P x).2⟩

Result:
case w.refine_1.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, ⋯⟩
f_eq : ∀ (p : ↑c) (x : ↥(sSup (domain '' c))) (y : ↥(↑p).domain), ↑x = ↑y → f x = ↑↑p y
x y : ↥(sSup (domain '' c))
p : E →ₗ.[R] F
hpc : p ∈ c
hpx : ↑↑(P x) ≤ p
hpy : ↑↑(P y) ≤ p
x' : ↥p.domain := (inclusion ⋯) ⟨↑x, ⋯⟩
⊢ f (x + y) = f x + f y

Proof state:
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

Tactic:
intro x y

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

Proof state:
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), ↑x = ↑y → f x = ↑↑p y

Tactic:
intro p x y hxy

Result:
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
⊢ f x = ↑↑p y

Proof state:
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
c : R
x : ↥(sSup (domain '' c✝))
⊢ f (c • x) = c • f x

Tactic:
rw [f_eq (P x).1 (c • x) (c • ⟨x, (P x).2⟩) rfl, ← map_smul]

Result:
no goals

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)
⊢ ∃ f, { domain := sSup (domain '' c), toFun := f } ∈ upperBounds c

Tactic:
have P : ∀ x : ↥(sSup (domain '' c)), { p : c // (x : E) ∈ p.val.domain } := by
  rintro x
  apply Classical.indefiniteDescription
  have := (mem_sSup_of_directed (cne.image _) hdir).1 x.2
  rwa [Set.exists_mem_image, ← bex_def, SetCoe.exists'] at this

Result:
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, { domain := sSup (domain '' c), toFun := f } ∈ upperBounds c

Proof state:
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

Tactic:
rcases hc (P x).1.1 (P x).1.2 (P y).1.1 (P y).1.2 with ⟨p, hpc, hpx, hpy⟩

Result:
case w.refine_1.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, ⋯⟩
f_eq : ∀ (p : ↑c) (x : ↥(sSup (domain '' c))) (y : ↥(↑p).domain), ↑x = ↑y → f x = ↑↑p y
x y : ↥(sSup (domain '' c))
p : E →ₗ.[R] F
hpc : p ∈ c
hpx : ↑↑(P x) ≤ p
hpy : ↑↑(P y) ≤ p
⊢ f (x + y) = f x + f y