-- 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 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' := ⋯ }.toFun (m • x) = (RingHom.id R) m • { toFun := f, map_add' := ⋯ }.toFun x

Tactic:
intro c x

Result:
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✝))
⊢ { toFun := f, map_add' := ⋯ }.toFun (c • x) = (RingHom.id R) c • { toFun := f, map_add' := ⋯ }.toFun x

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

Tactic:
rcases hc (P x).1.1 (P x).1.2 p.1 p.2 with ⟨q, _hqc, hxq, hpq⟩

Result:
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

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

Tactic:
intro p hpc

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
⊢ p ≤ { domain := sSup (domain '' c), toFun := { toFun := f, map_add' := ⋯, map_smul' := ⋯ } }

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
x' : ↥p.domain := (inclusion ⋯) ⟨↑x, ⋯⟩
y' : ↥p.domain := (inclusion ⋯) ⟨↑y, ⋯⟩
⊢ f (x + y) = f x + 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]

Result:
no goals

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
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

Tactic:
exact f_eq ⟨p, hpc⟩ _ _ hxy.symm

Result:
no goals

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

Tactic:
exact hxy

Result:
no goals

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)
⊢ (x : ↥(sSup (domain '' c))) → { p // ↑x ∈ (↑p).domain }

Tactic:
rintro x

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)
x : ↥(sSup (domain '' c))
⊢ { p // ↑x ∈ (↑p).domain }

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)
x : ↥(sSup (domain '' c))
⊢ { p // ↑x ∈ (↑p).domain }

Tactic:
apply Classical.indefiniteDescription

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))
⊢ ∃ x_1, ↑x ∈ (↑x_1).domain