-- Mathlib/Algebra/Lie/Submodule.lean
lemma isCompactElement_lieSpan_singleton (m : M) :
    CompleteLattice.IsCompactElement (lieSpan R L {m})

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
m : M
s : Set (LieSubmodule R L M)
hne : s.Nonempty
hdir : DirectedOn (fun x1 x2 => x1 ≤ x2) s
hsup : m ∈ ↑(sSup s)
this : ↑(sSup s) = ⋃ N ∈ s, ↑N
N : LieSubmodule R L M
hN : N ∈ s
hN' : m ∈ N
⊢ lieSpan R L {m} ≤ N

Tactic:
simpa

Result:
no goals

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
m : M
⊢ CompleteLattice.IsCompactElement (lieSpan R L {m})

Tactic:
rw [CompleteLattice.isCompactElement_iff_le_of_directed_sSup_le]

Result:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
m : M
⊢ ∀ (s : Set (LieSubmodule R L M)),
    s.Nonempty → DirectedOn (fun x1 x2 => x1 ≤ x2) s → lieSpan R L {m} ≤ sSup s → ∃ x ∈ s, lieSpan R L {m} ≤ x

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
m : M
s : Set (LieSubmodule R L M)
hne : s.Nonempty
hdir : DirectedOn (fun x1 x2 => x1 ≤ x2) s
hsup : m ∈ ↑(sSup s)
⊢ ∃ x ∈ s, lieSpan R L {m} ≤ x

Tactic:
suffices (↑(sSup s) : Set M) = ⋃ N ∈ s, ↑N by
  obtain ⟨N : LieSubmodule R L M, hN : N ∈ s, hN' : m ∈ N⟩ := by
    simp_rw [this, Set.mem_iUnion, SetLike.mem_coe, exists_prop] at hsup; assumption
  exact ⟨N, hN, by simpa⟩

Result:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
m : M
s : Set (LieSubmodule R L M)
hne : s.Nonempty
hdir : DirectedOn (fun x1 x2 => x1 ≤ x2) s
hsup : m ∈ ↑(sSup s)
⊢ ↑(sSup s) = ⋃ N ∈ s, ↑N

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
m : M
s : Set (LieSubmodule R L M)
hne : s.Nonempty
hdir : DirectedOn (fun x1 x2 => x1 ≤ x2) s
hsup : m ∈ ↑(sSup s)
this : ↑(sSup s) = ⋃ N ∈ s, ↑N
⊢ ∃ x ∈ s, lieSpan R L {m} ≤ x

Tactic:
obtain ⟨N : LieSubmodule R L M, hN : N ∈ s, hN' : m ∈ N⟩ := by
  simp_rw [this, Set.mem_iUnion, SetLike.mem_coe, exists_prop] at hsup; assumption

Result:
case intro.intro
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
m : M
s : Set (LieSubmodule R L M)
hne : s.Nonempty
hdir : DirectedOn (fun x1 x2 => x1 ≤ x2) s
hsup : m ∈ ↑(sSup s)
this : ↑(sSup s) = ⋃ N ∈ s, ↑N
N : LieSubmodule R L M
hN : N ∈ s
hN' : m ∈ N
⊢ ∃ x ∈ s, lieSpan R L {m} ≤ x

Proof state:
case intro.intro
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
m : M
s : Set (LieSubmodule R L M)
hne : s.Nonempty
hdir : DirectedOn (fun x1 x2 => x1 ≤ x2) s
hsup : m ∈ ↑(sSup s)
this : ↑(sSup s) = ⋃ N ∈ s, ↑N
N : LieSubmodule R L M
hN : N ∈ s
hN' : m ∈ N
⊢ ∃ x ∈ s, lieSpan R L {m} ≤ x

Tactic:
exact ⟨N, hN, by simpa⟩

Result:
no goals

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
m : M
s : Set (LieSubmodule R L M)
hdir : DirectedOn (fun x1 x2 => x1 ≤ x2) s
hsup : m ∈ ↑(sSup s)
hne : Nonempty ↑s
⊢ ↑(sSup s) = ⋃ N ∈ s, ↑N

Tactic:
have := Submodule.coe_iSup_of_directed _ hdir.directed_val

Result:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
m : M
s : Set (LieSubmodule R L M)
hdir : DirectedOn (fun x1 x2 => x1 ≤ x2) s
hsup : m ∈ ↑(sSup s)
hne : Nonempty ↑s
this : ↑(⨆ x, ↑↑x) = ⋃ i, ↑↑↑i
⊢ ↑(sSup s) = ⋃ N ∈ s, ↑N

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
m : M
⊢ ∀ (s : Set (LieSubmodule R L M)),
    s.Nonempty → DirectedOn (fun x1 x2 => x1 ≤ x2) s → lieSpan R L {m} ≤ sSup s → ∃ x ∈ s, lieSpan R L {m} ≤ x

Tactic:
intro s hne hdir hsup

Result:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
m : M
s : Set (LieSubmodule R L M)
hne : s.Nonempty
hdir : DirectedOn (fun x1 x2 => x1 ≤ x2) s
hsup : lieSpan R L {m} ≤ sSup s
⊢ ∃ x ∈ s, lieSpan R L {m} ≤ x

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
m : M
s : Set (LieSubmodule R L M)
hdir : DirectedOn (fun x1 x2 => x1 ≤ x2) s
hsup : m ∈ ↑(sSup s)
hne : Nonempty ↑s
this : ↑(⨆ i, ↑i) = ⋃ i ∈ s, ↑i
⊢ ↑(sSup s) = ⋃ N ∈ s, ↑N

Tactic:
rw [← this, SetLike.coe_set_eq, sSup_eq_iSup, iSup_subtype]

Result:
no goals

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
m : M
s : Set (LieSubmodule R L M)
hne : s.Nonempty
hdir : DirectedOn (fun x1 x2 => x1 ≤ x2) s
hsup✝ : m ∈ ↑(sSup s)
this : ↑(sSup s) = ⋃ N ∈ s, ↑N
hsup : ∃ i ∈ s, m ∈ i
⊢ ?m.340010

Tactic:
assumption

Result:
no goals

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
m : M
s : Set (LieSubmodule R L M)
hdir : DirectedOn (fun x1 x2 => x1 ≤ x2) s
hsup : m ∈ ↑(sSup s)
hne : Nonempty ↑s
this : ↑(⨆ x, ↑↑x) = ⋃ i, ↑↑↑i
⊢ ↑(sSup s) = ⋃ N ∈ s, ↑N

Tactic:
simp_rw [← iSup_toSubmodule, Set.iUnion_coe_set, coe_toSubmodule] at this

Result:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
m : M
s : Set (LieSubmodule R L M)
hdir : DirectedOn (fun x1 x2 => x1 ≤ x2) s
hsup : m ∈ ↑(sSup s)
hne : Nonempty ↑s
this : ↑(⨆ i, ↑i) = ⋃ i ∈ s, ↑i
⊢ ↑(sSup s) = ⋃ N ∈ s, ↑N

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
m : M
s : Set (LieSubmodule R L M)
hne : s.Nonempty
hdir : DirectedOn (fun x1 x2 => x1 ≤ x2) s
hsup : lieSpan R L {m} ≤ sSup s
⊢ ∃ x ∈ s, lieSpan R L {m} ≤ x

Tactic:
replace hsup : m ∈ (↑(sSup s) : Set M) := (SetLike.le_def.mp hsup) (subset_lieSpan rfl)

Result:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
m : M
s : Set (LieSubmodule R L M)
hne : s.Nonempty
hdir : DirectedOn (fun x1 x2 => x1 ≤ x2) s
hsup : m ∈ ↑(sSup s)
⊢ ∃ x ∈ s, lieSpan R L {m} ≤ x

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
m : M
s : Set (LieSubmodule R L M)
hne : s.Nonempty
hdir : DirectedOn (fun x1 x2 => x1 ≤ x2) s
hsup : m ∈ ↑(sSup s)
⊢ ↑(sSup s) = ⋃ N ∈ s, ↑N

Tactic:
replace hne : Nonempty s := Set.nonempty_coe_sort.mpr hne

Result:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
m : M
s : Set (LieSubmodule R L M)
hdir : DirectedOn (fun x1 x2 => x1 ≤ x2) s
hsup : m ∈ ↑(sSup s)
hne : Nonempty ↑s
⊢ ↑(sSup s) = ⋃ N ∈ s, ↑N