-- Mathlib/LinearAlgebra/Span/Basic.lean
theorem singleton_span_isCompactElement (x : M) :
    CompleteLattice.IsCompactElement (span R {x} : Submodule R M)

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
⊢ ∀ (s : Set (Submodule R M)),
    s.Nonempty → DirectedOn (fun x1 x2 => x1 ≤ x2) s → span R {x} ≤ sSup s → ∃ x_1 ∈ s, span R {x} ≤ x_1

Tactic:
intro d hemp hdir hsup

Result:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
d : Set (Submodule R M)
hemp : d.Nonempty
hdir : DirectedOn (fun x1 x2 => x1 ≤ x2) d
hsup : span R {x} ≤ sSup d
⊢ ∃ x_1 ∈ d, span R {x} ≤ x_1

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
d : Set (Submodule R M)
hemp : d.Nonempty
hdir : DirectedOn (fun x1 x2 => x1 ≤ x2) d
hsup : span R {x} ≤ sSup d
this : x ∈ sSup d
y : Submodule R M
hyd : y ∈ d
hxy : x ∈ y
⊢ span R {x} ≤ y

Tactic:
simpa only [span_le, singleton_subset_iff]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
d : Set (Submodule R M)
hemp : d.Nonempty
hdir : DirectedOn (fun x1 x2 => x1 ≤ x2) d
hsup : span R {x} ≤ sSup d
this : x ∈ sSup d
⊢ ∃ x_1 ∈ d, span R {x} ≤ x_1

Tactic:
obtain ⟨y, ⟨hyd, hxy⟩⟩ := (mem_sSup_of_directed hemp hdir).mp this

Result:
case intro.intro
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
d : Set (Submodule R M)
hemp : d.Nonempty
hdir : DirectedOn (fun x1 x2 => x1 ≤ x2) d
hsup : span R {x} ≤ sSup d
this : x ∈ sSup d
y : Submodule R M
hyd : y ∈ d
hxy : x ∈ y
⊢ ∃ x_1 ∈ d, span R {x} ≤ x_1

Proof state:
case intro.intro
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
d : Set (Submodule R M)
hemp : d.Nonempty
hdir : DirectedOn (fun x1 x2 => x1 ≤ x2) d
hsup : span R {x} ≤ sSup d
this : x ∈ sSup d
y : Submodule R M
hyd : y ∈ d
hxy : x ∈ y
⊢ ∃ x_1 ∈ d, span R {x} ≤ x_1

Tactic:
exact ⟨y, ⟨hyd, by simpa only [span_le, singleton_subset_iff] ⟩⟩

Result:
no goals

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
d : Set (Submodule R M)
hemp : d.Nonempty
hdir : DirectedOn (fun x1 x2 => x1 ≤ x2) d
hsup : span R {x} ≤ sSup d
⊢ ∃ x_1 ∈ d, span R {x} ≤ x_1

Tactic:
have : x ∈ (sSup d) := (SetLike.le_def.mp hsup) (mem_span_singleton_self x)

Result:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
d : Set (Submodule R M)
hemp : d.Nonempty
hdir : DirectedOn (fun x1 x2 => x1 ≤ x2) d
hsup : span R {x} ≤ sSup d
this : x ∈ sSup d
⊢ ∃ x_1 ∈ d, span R {x} ≤ x_1

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
⊢ CompleteLattice.IsCompactElement (span R {x})

Tactic:
rw [CompleteLattice.isCompactElement_iff_le_of_directed_sSup_le]

Result:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
⊢ ∀ (s : Set (Submodule R M)),
    s.Nonempty → DirectedOn (fun x1 x2 => x1 ≤ x2) s → span R {x} ≤ sSup s → ∃ x_1 ∈ s, span R {x} ≤ x_1