awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
⊢ Nontrivial.{w} (LieSubmodule R L M) ↔ Nontrivial M

Tactic:
not_iff_not.mp
    ((not_nontrivial_iff_subsingleton.trans <| subsingleton_iff R L M).trans
      not_nontrivial_iff_subsingleton.symm)

Premises used: not_iff_not, not_nontrivial_iff_subsingleton, Iff.mp, Iff.trans, LieSubmodule.subsingleton_iff, Iff.symm
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N N' : LieSubmodule R L M
inst_5 : Nontrivial M
⊢ Nontrivial.{w} (LieSubmodule R L M)

Tactic:
(nontrivial_iff R L M).mpr ‹_›

Premises used: Iff.mpr, LieSubmodule.nontrivial_iff
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N : LieSubmodule R L M
mp : Nontrivial.{w} ↥N → N ≠ ⊥
mpr : N ≠ ⊥ → Nontrivial.{w} ↥N
⊢ Nontrivial.{w} ↥N ↔ N ≠ ⊥

Tactic:
constructor
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
m₁ m₂ : M
h₁ : Membership.mem (γ := LieSubmodule R L M) ⊥ m₁
h₂ : Membership.mem (γ := LieSubmodule R L M) ⊥ m₂
h₁₂ :
  Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := LieSubmodule R L M) ⊥ x) m₁ h₁ ≠
    Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := LieSubmodule R L M) ⊥ x) m₂ h₂
⊢ False

Tactic:
simp [(LieSubmodule.mem_bot _).mp h₁, (LieSubmodule.mem_bot _).mp h₂] at h₁₂

Premises used: LieSubmodule.mem_bot, Iff.mp
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N : LieSubmodule R L M
mpr : Subsingleton.{w + 1} ↥N → N = ⊥
⊢ N ≠ ⊥ → Nontrivial.{w} ↥N

Tactic:
contrapose!
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N : LieSubmodule R L M
mpr : Subsingleton.{w + 1} ↥N → ∀ m ∈ N, m = 0
⊢ Subsingleton.{w + 1} ↥N → N = ⊥

Tactic:
rw [LieSubmodule.eq_bot_iff]

Premises used: LieSubmodule.eq_bot_iff
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N : LieSubmodule R L M
h : ∀ (a b : ↥N), a = b
m : M
hm : m ∈ N
⊢ m = 0

Tactic:
simpa using h ⟨m, hm⟩ ⟨_, N.zero_mem⟩

Premises used: LieSubmodule.zero_mem, Subtype.mk
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N : LieSubmodule R L M
⊢ (↑N.incl : ↥N →ₗ[R] M) = (↑N : Submodule R M).subtype

Tactic:
rfl

Premises used: Submodule.subtype, rfl
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N : LieSubmodule R L M
m : ↥N
⊢ (N.incl : (a : ↥N) → M) m = (↑m : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N : LieSubmodule R L M
⊢ Eq (α := (a : ↥N) → M) (⇑N.incl : (a : ↥N) → M) (Subtype.val (p := fun (x : M) ↦ x ∈ N))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N : LieSubmodule R L M
⊢ Function.Injective (α := ↥N) (β := M) (⇑N.incl : (a : ↥N) → M)

Tactic:
Subtype.coe_injective

Premises used: Subtype.coe_injective
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N N' : LieSubmodule R L M
h : N ≤ N'
m : ↥N
⊢ (↑((inclusion h : (a : ↥N) → ↥N') m) : M) = (↑m : M)

Tactic:
rfl

Premises used: Set.Mem, rfl
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N N' : LieSubmodule R L M
h : N ≤ N'
m : ↥N
⊢ (inclusion h : (a : ↥N) → ↥N') m = Subtype.mk (p := fun (x : M) ↦ x ∈ N') (↑m : M) ⋯

Tactic:
rfl

Premises used: Set.Mem, rfl
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N N' : LieSubmodule R L M
h : N ≤ N'
x y : ↥N
⊢ Eq (α := ↥N') ((inclusion h : (a : ↥N) → ↥N') x : ↥N') ((inclusion h : (a : ↥N) → ↥N') y : ↥N') → x = y

Tactic:
simp only [inclusion_apply, imp_self, Subtype.mk_eq_mk, SetLike.coe_eq_coe]

Premises used: SetLike.coe_eq_coe, imp_self, LieSubmodule.inclusion_apply, Subtype.mk_eq_mk
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
s : Set M
x : M
rw :
  Membership.mem (γ := Set M)
      (⋂ (s_1 : LieSubmodule R L M),
        ⋂ (_ : Membership.mem (γ := Set (LieSubmodule R L M)) {N : LieSubmodule R L M | s ⊆ (↑N : Set M)} s_1),
          (↑s_1 : Set M))
      x ↔
    ∀ (N : LieSubmodule R L M), s ⊆ (↑N : Set M) → x ∈ N
⊢ Membership.mem (γ := LieSubmodule R L M) (lieSpan R L s) x ↔ ∀ (N : LieSubmodule R L M), s ⊆ (↑N : Set M) → x ∈ N

Tactic:
rw [← SetLike.mem_coe, lieSpan, coe_sInf]

Premises used: SetLike.mem_coe, LieSubmodule.lieSpan, LieSubmodule.coe_sInf
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
s : Set M
x : M
⊢ Membership.mem (γ := Set M)
      (⋂ (s_1 : LieSubmodule R L M),
        ⋂ (_ : Membership.mem (γ := Set (LieSubmodule R L M)) {N : LieSubmodule R L M | s ⊆ (↑N : Set M)} s_1),
          (↑s_1 : Set M))
      x ↔
    ∀ (N : LieSubmodule R L M), s ⊆ (↑N : Set M) → x ∈ N

Tactic:
mem_iInter₂

Premises used: Set.Mem, setOf, Set.mem_iInter₂
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
s : Set M
x : M
⊢ Membership.mem (γ := Set M)
      (⋂ (s_1 : LieSubmodule R L M),
        ⋂ (_ : Membership.mem (γ := Set (LieSubmodule R L M)) {N : LieSubmodule R L M | s ⊆ (↑N : Set M)} s_1),
          (↑s_1 : Set M))
      x ↔
    ∀ (N : LieSubmodule R L M), s ⊆ (↑N : Set M) → x ∈ N

Tactic:
exact mem_iInter₂

Premises used: Set.mem_iInter₂
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
s : Set M
m : M
hm : m ∈ s
rw : ∀ (N : LieSubmodule R L M), s ⊆ (↑N : Set M) → m ∈ N
⊢ m ∈ (↑(lieSpan R L s) : Set M)

Tactic:
rw [SetLike.mem_coe, mem_lieSpan]

Premises used: SetLike.mem_coe, LieSubmodule.mem_lieSpan
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
s : Set M
m : M
hm : m ∈ s
N : LieSubmodule R L M
hN : s ⊆ (↑N : Set M)
⊢ m ∈ N

Tactic:
hN hm
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
s : Set M
m : M
hm : m ∈ s
N : LieSubmodule R L M
hN : s ⊆ (↑N : Set M)
⊢ m ∈ N

Tactic:
exact hN hm
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
s : Set M
rw : s ⊆ (↑(↑(lieSpan R L s) : Submodule R M) : Set M)
⊢ LE.le (α := Submodule R M) (Submodule.span R s) (↑(lieSpan R L s) : Submodule R M)

Tactic:
rw [Submodule.span_le]

Premises used: Submodule.span_le
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
s : Set M
⊢ s ⊆ (↑(↑(lieSpan R L s) : Submodule R M) : Set M)

Tactic:
apply subset_lieSpan

Premises used: LieSubmodule.subset_lieSpan
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
s : Set M
N : LieSubmodule R L M
mp : lieSpan R L s ≤ N → s ⊆ (↑N : Set M)
mpr : s ⊆ (↑N : Set M) → lieSpan R L s ≤ N
⊢ lieSpan R L s ≤ N ↔ s ⊆ (↑N : Set M)

Tactic:
constructor
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
s : Set M
N : LieSubmodule R L M
⊢ lieSpan R L s ≤ N → s ⊆ (↑N : Set M)

Tactic:
Subset.trans subset_lieSpan

Premises used: Set.Subset.trans, LieSubmodule.subset_lieSpan, Set.Subset
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
s : Set M
N : LieSubmodule R L M
⊢ lieSpan R L s ≤ N → s ⊆ (↑N : Set M)

Tactic:
exact Subset.trans subset_lieSpan

Premises used: Set.Subset.trans, LieSubmodule.subset_lieSpan
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
s : Set M
N : LieSubmodule R L M
hs : s ⊆ (↑N : Set M)
m : M
hm : Membership.mem (γ := LieSubmodule R L M) (lieSpan R L s) m
⊢ ∀ (N : LieSubmodule R L M), s ⊆ (↑N : Set M) → m ∈ N

Tactic:
rw [mem_lieSpan] at hm

Premises used: LieSubmodule.mem_lieSpan
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
s : Set M
N : LieSubmodule R L M
hs : s ⊆ (↑N : Set M)
m : M
hm : ∀ (N : LieSubmodule R L M), s ⊆ (↑N : Set M) → m ∈ N
⊢ m ∈ N

Tactic:
hm _ hs
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
s : Set M
N : LieSubmodule R L M
hs : s ⊆ (↑N : Set M)
m : M
hm : ∀ (N : LieSubmodule R L M), s ⊆ (↑N : Set M) → m ∈ N
⊢ m ∈ N

Tactic:
exact hm _ hs
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
s t : Set M
h : s ⊆ t
rw : s ⊆ (↑(lieSpan R L t) : Set M)
⊢ LE.le (α := LieSubmodule R L M) (lieSpan R L s) (lieSpan R L t)

Tactic:
rw [lieSpan_le]

Premises used: LieSubmodule.lieSpan_le
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
s t : Set M
h : s ⊆ t
⊢ s ⊆ (↑(lieSpan R L t) : Set M)

Tactic:
Subset.trans h subset_lieSpan

Premises used: Set.Subset.trans, LieSubmodule.subset_lieSpan
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
s t : Set M
h : s ⊆ t
⊢ s ⊆ (↑(lieSpan R L t) : Set M)

Tactic:
exact Subset.trans h subset_lieSpan

Premises used: Set.Subset.trans, LieSubmodule.subset_lieSpan
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N : LieSubmodule R L M
⊢ lieSpan R L (↑N : Set M) = N

Tactic:
le_antisymm (lieSpan_le.mpr rfl.subset) subset_lieSpan

Premises used: Iff.mpr, LieSubmodule.subset_lieSpan, Eq.subset, le_antisymm, LieSubmodule.lieSpan_le, rfl
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
p : Submodule R M
rw : (↑(lieSpan R L (↑p : Set M)) : Submodule R M) = p ↔ ∀ (x : L), ∀ m ∈ p, ⁅x, m⁆ ∈ p
⊢ (↑(lieSpan R L (↑p : Set M)) : Submodule R M) = p ↔ ∃ (N : LieSubmodule R L M), (↑N : Submodule R M) = p

Tactic:
rw [p.exists_lieSubmodule_coe_eq_iff L]

Premises used: Submodule.exists_lieSubmodule_coe_eq_iff
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
p : Submodule R M
mp : (↑(lieSpan R L (↑p : Set M)) : Submodule R M) = p → ∀ (x : L), ∀ m ∈ p, ⁅x, m⁆ ∈ p
mpr : (∀ (x : L), ∀ m ∈ p, ⁅x, m⁆ ∈ p) → (↑(lieSpan R L (↑p : Set M)) : Submodule R M) = p
⊢ (↑(lieSpan R L (↑p : Set M)) : Submodule R M) = p ↔ ∀ (x : L), ∀ m ∈ p, ⁅x, m⁆ ∈ p

Tactic:
constructor
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
p : Submodule R M
h : (↑(lieSpan R L (↑p : Set M)) : Submodule R M) = p
x : L
m : M
hm : m ∈ p
mp : Membership.mem (γ := LieSubmodule R L M) (lieSpan R L (↑p : Set M)) ⁅x, m⁆
⊢ ⁅x, m⁆ ∈ p

Tactic:
rw [← h, mem_toSubmodule]

Premises used: LieSubmodule.mem_toSubmodule
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
p : Submodule R M
h : (↑(lieSpan R L (↑p : Set M)) : Submodule R M) = p
x : L
m : M
hm : m ∈ p
⊢ Membership.mem (γ := LieSubmodule R L M) (lieSpan R L (↑p : Set M)) ⁅x, m⁆

Tactic:
lie_mem _ (subset_lieSpan hm)

Premises used: Set.Mem, LieSubmodule.subset_lieSpan, LieSubmodule.lie_mem
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
p : Submodule R M
h : (↑(lieSpan R L (↑p : Set M)) : Submodule R M) = p
x : L
m : M
hm : m ∈ p
⊢ Membership.mem (γ := LieSubmodule R L M) (lieSpan R L (↑p : Set M)) ⁅x, m⁆

Tactic:
exact lie_mem _ (subset_lieSpan hm)

Premises used: LieSubmodule.subset_lieSpan, LieSubmodule.lie_mem
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
p : Submodule R M
h : ∀ (x : L), ∀ m ∈ p, ⁅x, m⁆ ∈ p
mpr :
  (↑(lieSpan R L (↑(↑{ toSubmodule := p, lie_mem := h : LieSubmodule R L M } : Submodule R M) : Set M)) :
      Submodule R M) =
    (↑{ toSubmodule := p, lie_mem := h : LieSubmodule R L M } : Submodule R M)
mpr₁ :
  (↑(lieSpan R L (↑{ toSubmodule := p, lie_mem := h : LieSubmodule R L M } : Set M)) : Submodule R M) =
    (↑{ toSubmodule := p, lie_mem := h : LieSubmodule R L M } : Submodule R M)
mpr₂ :
  lieSpan R L (↑{ toSubmodule := p, lie_mem := h : LieSubmodule R L M } : Set M) =
    { toSubmodule := p, lie_mem := h : LieSubmodule R L M }
mpr₃ mpr₄ : { toSubmodule := p, lie_mem := h : LieSubmodule R L M } = { toSubmodule := p, lie_mem := h }
⊢ (↑(lieSpan R L (↑p : Set M)) : Submodule R M) = p

Tactic:
rw [← toSubmodule_mk p @h, coe_toSubmodule, toSubmodule_inj, lieSpan_eq]

Premises used: LieSubmodule.toSubmodule_inj, LieSubmodule.lieSpan_eq, LieSubmodule.coe_toSubmodule, LieSubmodule.toSubmodule_mk
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
⊢ Eq.{w + 1} (α := LieSubmodule R L M) (lieSpan R L ∅) ⊥

Tactic:
(LieSubmodule.gi R L M).gc.l_bot

Premises used: GaloisConnection.l_bot, LieSubmodule.gi, GaloisInsertion.gc
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
⊢ Eq.{w + 1} (α := LieSubmodule R L M) (lieSpan R L univ) ⊤

Tactic:
eq_top_iff.2 <| SetLike.le_def.2 <| subset_lieSpan

Premises used: Iff.mpr, eq_top_iff, SetLike.le_def, LieSubmodule.subset_lieSpan
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
s : Set M
rw : LE.le (α := LieSubmodule R L M) (lieSpan R L s) ⊥ ↔ ∀ m ∈ s, m = 0
rw₁ : s ⊆ (↑⊥ : Set M) ↔ ∀ m ∈ s, m = 0
rw₂ : s ⊆ {0} ↔ ∀ m ∈ s, m = 0
rw₃ rw₄ : (∀ y ∈ s, y = 0) ↔ ∀ m ∈ s, m = 0
⊢ Eq (α := LieSubmodule R L M) (lieSpan R L s) ⊥ ↔ ∀ m ∈ s, m = 0

Tactic:
rw [_root_.eq_bot_iff, lieSpan_le, bot_coe, subset_singleton_iff]

Premises used: Set.subset_singleton_iff, LieSubmodule.bot_coe, LieSubmodule.lieSpan_le, eq_bot_iff
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
s t : Set M
⊢ Eq (α := LieSubmodule R L M) (lieSpan R L (s ∪ t)) (lieSpan R L s ⊔ lieSpan R L t)

Tactic:
(LieSubmodule.gi R L M).gc.l_sup

Premises used: LieSubmodule.gi, GaloisConnection.l_sup, GaloisInsertion.gc
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
ι : Sort u_1
s : ι → Set M
⊢ Eq.{w + 1} (α := LieSubmodule R L M) (lieSpan R L (⋃ (i : ι), s i)) (⨆ (i : ι), lieSpan R L (s i))

Tactic:
(LieSubmodule.gi R L M).gc.l_iSup

Premises used: GaloisConnection.l_iSup, LieSubmodule.gi, Set.iUnion, GaloisInsertion.gc
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
s : Set M
p : (x : M) → Membership.mem (γ := LieSubmodule R L M) (lieSpan R L s) x → Prop
mem : ∀ (x : M) (h : x ∈ s), p x ⋯
zero : p 0 ⋯
add :
  ∀ (x y : M) (hx : Membership.mem (γ := LieSubmodule R L M) (lieSpan R L s) x)
    (hy : Membership.mem (γ := LieSubmodule R L M) (lieSpan R L s) y), p x hx → p y hy → p (x + y) ⋯
smul : ∀ (a : R) (x : M) (hx : Membership.mem (γ := LieSubmodule R L M) (lieSpan R L s) x), p x hx → p (a • x) ⋯
x : M
lie : ∀ (x : L) (y : M) (hy : Membership.mem (γ := LieSubmodule R L M) (lieSpan R L s) y), p y hy → p ⁅x, y⁆ ⋯
hx : Membership.mem (γ := LieSubmodule R L M) (lieSpan R L s) x
let : p x hx
⊢ p x hx

Tactic:
let p : LieSubmodule R L M :=
    { carrier := { x | ∃ hx, p x hx }
      add_mem' := fun ⟨_, hpx⟩ ⟨_, hpy⟩ ↦ ⟨_, add _ _ _ _ hpx hpy⟩
      zero_mem' := ⟨_, zero⟩
      smul_mem' := fun r ↦ fun ⟨_, hpx⟩ ↦ ⟨_, smul r _ _ hpx⟩
      lie_mem := fun ⟨_, hpy⟩ ↦ ⟨_, lie _ _ _ hpy⟩ }
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
s : Set M
p_1 : (x : M) → Membership.mem (γ := LieSubmodule R L M) (lieSpan R L s) x → Prop
mem : ∀ (x : M) (h : x ∈ s), p_1 x ⋯
zero : p_1 0 ⋯
add :
  ∀ (x y : M) (hx : Membership.mem (γ := LieSubmodule R L M) (lieSpan R L s) x)
    (hy : Membership.mem (γ := LieSubmodule R L M) (lieSpan R L s) y), p_1 x hx → p_1 y hy → p_1 (x + y) ⋯
smul : ∀ (a : R) (x : M) (hx : Membership.mem (γ := LieSubmodule R L M) (lieSpan R L s) x), p_1 x hx → p_1 (a • x) ⋯
x : M
lie : ∀ (x : L) (y : M) (hy : Membership.mem (γ := LieSubmodule R L M) (lieSpan R L s) y), p_1 y hy → p_1 ⁅x, y⁆ ⋯
hx : Membership.mem (γ := LieSubmodule R L M) (lieSpan R L s) x
p : LieSubmodule R L M :=
  { carrier := {x : M | ∃ (hx : Membership.mem (γ := LieSubmodule R L M) (lieSpan R L s) x), p_1 x hx}, add_mem' := ⋯,
    zero_mem' := ⋯, smul_mem' := ⋯, lie_mem := ⋯ }
⊢ p_1 x hx

Tactic:
lieSpan_le (N := p) |>.mpr (fun y hy ↦ ⟨subset_lieSpan hy, mem y hy⟩) hx |>.elim fun _ ↦ id

Premises used: Iff.mpr, LieSubmodule.subset_lieSpan, id, Exists.intro, LieSubmodule.lieSpan_le, Exists.elim
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
s : Set M
p_1 : (x : M) → Membership.mem (γ := LieSubmodule R L M) (lieSpan R L s) x → Prop
mem : ∀ (x : M) (h : x ∈ s), p_1 x ⋯
zero : p_1 0 ⋯
add :
  ∀ (x y : M) (hx : Membership.mem (γ := LieSubmodule R L M) (lieSpan R L s) x)
    (hy : Membership.mem (γ := LieSubmodule R L M) (lieSpan R L s) y), p_1 x hx → p_1 y hy → p_1 (x + y) ⋯
smul : ∀ (a : R) (x : M) (hx : Membership.mem (γ := LieSubmodule R L M) (lieSpan R L s) x), p_1 x hx → p_1 (a • x) ⋯
x : M
lie : ∀ (x : L) (y : M) (hy : Membership.mem (γ := LieSubmodule R L M) (lieSpan R L s) y), p_1 y hy → p_1 ⁅x, y⁆ ⋯
hx : Membership.mem (γ := LieSubmodule R L M) (lieSpan R L s) x
p : LieSubmodule R L M :=
  { carrier := {x : M | ∃ (hx : Membership.mem (γ := LieSubmodule R L M) (lieSpan R L s) x), p_1 x hx}, add_mem' := ⋯,
    zero_mem' := ⋯, smul_mem' := ⋯, lie_mem := ⋯ }
⊢ p_1 x hx

Tactic:
exact lieSpan_le (N := p) |>.mpr (fun y hy ↦ ⟨subset_lieSpan hy, mem y hy⟩) hx |>.elim fun _ ↦ id

Premises used: Iff.mpr, LieSubmodule.subset_lieSpan, Exists.intro, LieSubmodule.lieSpan_le, Exists.elim
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
m : M
rw :
  ∀ (s : Set (LieSubmodule R L M)),
    s.Nonempty →
      DirectedOn (fun (x1 x2 : LieSubmodule R L M) ↦ x1 ≤ x2) s →
        lieSpan R L {m} ≤ sSup s → ∃ x ∈ s, lieSpan R L {m} ≤ x
⊢ IsCompactElement (α := LieSubmodule R L M) (lieSpan R L {m})

Tactic:
rw [CompleteLattice.isCompactElement_iff_le_of_directed_sSup_le]

Premises used: CompleteLattice.isCompactElement_iff_le_of_directed_sSup_le
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
m : M
s : Set (LieSubmodule R L M)
hne : s.Nonempty
hdir : DirectedOn (fun (x1 x2 : LieSubmodule R L M) ↦ x1 ≤ x2) s
hsup : lieSpan R L {m} ≤ sSup s
⊢ m ∈ (↑(sSup s) : Set M)

Tactic:
replace hsup : m ∈ (↑(sSup s) : Set M) := (SetLike.le_def.mp hsup) (subset_lieSpan rfl)
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
m : M
s : Set (LieSubmodule R L M)
hne : s.Nonempty
hdir : DirectedOn (fun (x1 x2 : LieSubmodule R L M) ↦ x1 ≤ x2) s
hsup : m ∈ (↑(sSup s) : Set M)
this : (↑(sSup s) : Set M) = ⋃ N ∈ s, (↑N : Set M)
⊢ ∃ x ∈ s, lieSpan R L {m} ≤ x

Tactic:
simp_all
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
m : M
s : Set (LieSubmodule R L M)
hne : s.Nonempty
hdir : DirectedOn (fun (x1 x2 : LieSubmodule R L M) ↦ x1 ≤ x2) s
hsup : m ∈ (↑(sSup s) : Set M)
suffices : (↑(sSup s) : Set M) = ⋃ N ∈ s, (↑N : Set M)
⊢ ∃ x ∈ s, lieSpan R L {m} ≤ x

Tactic:
suffices (↑(sSup s) : Set M) = ⋃ N ∈ s, ↑N by simp_all
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
m : M
s : Set (LieSubmodule R L M)
hne : s.Nonempty
hdir : DirectedOn (fun (x1 x2 : LieSubmodule R L M) ↦ x1 ≤ x2) s
hsup : m ∈ (↑(sSup s) : Set M)
⊢ Nonempty.{w + 1} (↑s : Type w)

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