awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (hypothesis)
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
⊢ m ∈ N
have hm₁ : ∀ (N : LieSubmodule R L M), s ⊆ (↑N : Set M) → m ∈ N
Tactic: rw [mem_lieSpan] at hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (goal)
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
⊢ LE.le (α := LieSubmodule R L M) (lieSpan R L s) (lieSpan R L t)
have rw : s ⊆ (↑(lieSpan R L t) : Set M)
Tactic: rw [lieSpan_le]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (goal)
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
⊢ (↑(lieSpan R L (↑p : Set M)) : Submodule R M) = p ↔ ∃ (N : LieSubmodule R L M), (↑N : Submodule R M) = p
have rw : (↑(lieSpan R L (↑p : Set M)) : Submodule R M) = p ↔ ∀ (x : L), ∀ m ∈ p, ⁅x, m⁆ ∈ p
Tactic: rw [p.exists_lieSubmodule_coe_eq_iff L]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (goal)
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
⊢ (↑(lieSpan R L (↑p : Set M)) : Submodule R M) = p ↔ ∀ (x : L), ∀ m ∈ p, ⁅x, m⁆ ∈ p
have mp : (↑(lieSpan R L (↑p : Set M)) : Submodule R M) = p → ∀ (x : L), ∀ m ∈ p, ⁅x, m⁆ ∈ p
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (goal)
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
⊢ (↑(lieSpan R L (↑p : Set M)) : Submodule R M) = p ↔ ∀ (x : L), ∀ m ∈ p, ⁅x, m⁆ ∈ p
have mpr : (∀ (x : L), ∀ m ∈ p, ⁅x, m⁆ ∈ p) → (↑(lieSpan R L (↑p : Set M)) : Submodule R M) = p
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (goal)
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
⊢ ⁅x, m⁆ ∈ p
have mp : Membership.mem (γ := LieSubmodule R L M) (lieSpan R L (↑p : Set M)) ⁅x, m⁆
Tactic: rw [← h, mem_toSubmodule]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (goal)
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
⊢ (↑(lieSpan R L (↑p : Set M)) : Submodule R M) = p
have 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)
Tactic: rw [← toSubmodule_mk p @h, coe_toSubmodule, toSubmodule_inj, lieSpan_eq]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (goal)
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)
⊢ (↑(lieSpan R L (↑p : Set M)) : Submodule R M) = p
have 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)
Tactic: rw [← toSubmodule_mk p @h, coe_toSubmodule, toSubmodule_inj, lieSpan_eq]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (goal)
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)
⊢ (↑(lieSpan R L (↑p : Set M)) : Submodule R M) = p
have mpr₂ : lieSpan R L (↑{ toSubmodule := p, lie_mem := h : LieSubmodule R L M } : Set M) =
  { toSubmodule := p, lie_mem := h : LieSubmodule R L M }
Tactic: rw [← toSubmodule_mk p @h, coe_toSubmodule, toSubmodule_inj, lieSpan_eq]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (goal)
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 }
⊢ (↑(lieSpan R L (↑p : Set M)) : Submodule R M) = p
have mpr₃ : { toSubmodule := p, lie_mem := h : LieSubmodule R L M } = { toSubmodule := p, lie_mem := h }
Tactic: rw [← toSubmodule_mk p @h, coe_toSubmodule, toSubmodule_inj, lieSpan_eq]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (goal)
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
⊢ Eq (α := LieSubmodule R L M) (lieSpan R L s) ⊥ ↔ ∀ m ∈ s, m = 0
have rw : LE.le (α := 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]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (goal)
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
⊢ Eq (α := LieSubmodule R L M) (lieSpan R L s) ⊥ ↔ ∀ m ∈ s, m = 0
have rw₁ : s ⊆ (↑⊥ : Set M) ↔ ∀ m ∈ s, m = 0
Tactic: rw [_root_.eq_bot_iff, lieSpan_le, bot_coe, subset_singleton_iff]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (goal)
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
⊢ Eq (α := LieSubmodule R L M) (lieSpan R L s) ⊥ ↔ ∀ m ∈ s, m = 0
have rw₂ : s ⊆ {0} ↔ ∀ m ∈ s, m = 0
Tactic: rw [_root_.eq_bot_iff, lieSpan_le, bot_coe, subset_singleton_iff]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (goal)
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
⊢ Eq (α := LieSubmodule R L M) (lieSpan R L s) ⊥ ↔ ∀ m ∈ s, m = 0
have rw₃ : (∀ y ∈ s, y = 0) ↔ ∀ m ∈ s, m = 0
Tactic: rw [_root_.eq_bot_iff, lieSpan_le, bot_coe, subset_singleton_iff]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (goal)
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
⊢ IsCompactElement (α := LieSubmodule R L M) (lieSpan R L {m})
have 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
Tactic: rw [CompleteLattice.isCompactElement_iff_le_of_directed_sSup_le]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (hypothesis)
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
⊢ ∃ x ∈ s, lieSpan R L {m} ≤ x
have hsup₁ : m ∈ (↑(sSup s) : Set M)
Tactic: replace hsup : m ∈ (↑(sSup s) : Set M) := (SetLike.le_def.mp hsup) (subset_lieSpan rfl)
Cleared hypotheses: hsup
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (goal)
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)
⊢ ∃ x ∈ s, lieSpan R L {m} ≤ x
have suffices : (↑(sSup s) : Set M) = ⋃ N ∈ s, (↑N : Set M)
Tactic: suffices (↑(sSup s) : Set M) = ⋃ N ∈ s, ↑N by simp_all
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (hypothesis)
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)
⊢ (↑(sSup s) : Set M) = ⋃ N ∈ s, (↑N : Set M)
have hne₁ : Nonempty.{w + 1} (↑s : Type w)
Tactic: replace hne : Nonempty s := Set.nonempty_coe_sort.mpr hne
Cleared hypotheses: hne
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (hypothesis)
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)
hdir : DirectedOn (fun (x1 x2 : LieSubmodule R L M) ↦ x1 ≤ x2) s
hsup : m ∈ (↑(sSup s) : Set M)
hne : Nonempty.{w + 1} (↑s : Type w)
⊢ (↑(sSup s) : Set M) = ⋃ N ∈ s, (↑N : Set M)
have this : (↑(⨆ (x : { x : LieSubmodule R L M // x ∈ s }), (↑(↑x : LieSubmodule R L M) : Submodule R M)) : Set M) =
  ⋃ (i : { x : LieSubmodule R L M // x ∈ s }), (↑(↑(↑i : LieSubmodule R L M) : Submodule R M) : Set M)
Tactic: have := Submodule.coe_iSup_of_directed _ hdir.directed_val
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (hypothesis)
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)
hdir : DirectedOn (fun (x1 x2 : LieSubmodule R L M) ↦ x1 ≤ x2) s
hsup : m ∈ (↑(sSup s) : Set M)
hne : Nonempty.{w + 1} (↑s : Type w)
this :
  (↑(⨆ (x : { x : LieSubmodule R L M // x ∈ s }), (↑(↑x : LieSubmodule R L M) : Submodule R M)) : Set M) =
    ⋃ (i : { x : LieSubmodule R L M // x ∈ s }), (↑(↑(↑i : LieSubmodule R L M) : Submodule R M) : Set M)
⊢ (↑(sSup s) : Set M) = ⋃ N ∈ s, (↑N : Set M)
have this₁ : (↑(⨆ (i : { x : LieSubmodule R L M // x ∈ s }), (↑i : LieSubmodule R L M)) : Set M) = ⋃ i ∈ s, (↑i : Set M)
Tactic: simp_rw [← iSup_toSubmodule, Set.iUnion_coe_set, coe_toSubmodule] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (goal)
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)
hdir : DirectedOn (fun (x1 x2 : LieSubmodule R L M) ↦ x1 ≤ x2) s
hsup : m ∈ (↑(sSup s) : Set M)
hne : Nonempty.{w + 1} (↑s : Type w)
this : (↑(⨆ (i : { x : LieSubmodule R L M // x ∈ s }), (↑i : LieSubmodule R L M)) : Set M) = ⋃ i ∈ s, (↑i : Set M)
⊢ (↑(sSup s) : Set M) = ⋃ N ∈ s, (↑N : Set M)
have rw : (↑(sSup s) : Set M) = (↑(⨆ (i : { x : LieSubmodule R L M // x ∈ s }), (↑i : LieSubmodule R L M)) : Set M)
Tactic: rw [← this, SetLike.coe_set_eq, sSup_eq_iSup, iSup_subtype]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (goal)
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)
hdir : DirectedOn (fun (x1 x2 : LieSubmodule R L M) ↦ x1 ≤ x2) s
hsup : m ∈ (↑(sSup s) : Set M)
hne : Nonempty.{w + 1} (↑s : Type w)
this : (↑(⨆ (i : { x : LieSubmodule R L M // x ∈ s }), (↑i : LieSubmodule R L M)) : Set M) = ⋃ i ∈ s, (↑i : Set M)
rw : (↑(sSup s) : Set M) = (↑(⨆ (i : { x : LieSubmodule R L M // x ∈ s }), (↑i : LieSubmodule R L M)) : Set M)
⊢ (↑(sSup s) : Set M) = ⋃ N ∈ s, (↑N : Set M)
have rw₁ : sSup s = ⨆ (i : { x : LieSubmodule R L M // x ∈ s }), (↑i : LieSubmodule R L M)
Tactic: rw [← this, SetLike.coe_set_eq, sSup_eq_iSup, iSup_subtype]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (goal)
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)
hdir : DirectedOn (fun (x1 x2 : LieSubmodule R L M) ↦ x1 ≤ x2) s
hsup : m ∈ (↑(sSup s) : Set M)
hne : Nonempty.{w + 1} (↑s : Type w)
this : (↑(⨆ (i : { x : LieSubmodule R L M // x ∈ s }), (↑i : LieSubmodule R L M)) : Set M) = ⋃ i ∈ s, (↑i : Set M)
rw : (↑(sSup s) : Set M) = (↑(⨆ (i : { x : LieSubmodule R L M // x ∈ s }), (↑i : LieSubmodule R L M)) : Set M)
rw₁ : sSup s = ⨆ (i : { x : LieSubmodule R L M // x ∈ s }), (↑i : LieSubmodule R L M)
⊢ (↑(sSup s) : Set M) = ⋃ N ∈ s, (↑N : Set M)
have rw₂ : Eq.{w + 1} (α := LieSubmodule R L M) (⨆ a ∈ s, a)
  (⨆ (i : { x : LieSubmodule R L M // x ∈ s }), (↑i : LieSubmodule R L M))
Tactic: rw [← this, SetLike.coe_set_eq, sSup_eq_iSup, iSup_subtype]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (goal)
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)
hdir : DirectedOn (fun (x1 x2 : LieSubmodule R L M) ↦ x1 ≤ x2) s
hsup : m ∈ (↑(sSup s) : Set M)
hne : Nonempty.{w + 1} (↑s : Type w)
this : (↑(⨆ (i : { x : LieSubmodule R L M // x ∈ s }), (↑i : LieSubmodule R L M)) : Set M) = ⋃ i ∈ s, (↑i : Set M)
rw : (↑(sSup s) : Set M) = (↑(⨆ (i : { x : LieSubmodule R L M // x ∈ s }), (↑i : LieSubmodule R L M)) : Set M)
rw₁ : sSup s = ⨆ (i : { x : LieSubmodule R L M // x ∈ s }), (↑i : LieSubmodule R L M)
rw₂ :
  Eq.{w + 1} (α := LieSubmodule R L M) (⨆ a ∈ s, a)
    (⨆ (i : { x : LieSubmodule R L M // x ∈ s }), (↑i : LieSubmodule R L M))
⊢ (↑(sSup s) : Set M) = ⋃ N ∈ s, (↑N : Set M)
have rw₃ : Eq.{w + 1} (α := LieSubmodule R L M) (⨆ a ∈ s, a)
  (⨆ (i : LieSubmodule R L M),
    ⨆ (h : i ∈ s), (↑(Subtype.mk (p := fun (x : LieSubmodule R L M) ↦ x ∈ s) i h) : LieSubmodule R L M))
Tactic: rw [← this, SetLike.coe_set_eq, sSup_eq_iSup, iSup_subtype]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (goal)
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
⊢ sSup ((fun (x : M) ↦ lieSpan R L {x}) '' (↑N : Set M)) = N
have refine : N ≤ sSup ((fun (x : M) ↦ lieSpan R L {x}) '' (↑N : Set M))
Tactic: refine le_antisymm (sSup_le <| by simp) ?_
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (goal)
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 : Submodule R M) ≤
    sSup {x : Submodule R M | ∃ (s : LieSubmodule R L M), (∃ x ∈ N, lieSpan R L {x} = s) ∧ (↑s : Submodule R M) = x}
have refine : ∀ (m : M) (hm : m ∈ (↑N : Submodule R M)) (N' : Submodule R M)
  (hN' :
    ∀ (p : Submodule R M),
      Membership.mem (γ := Set (Submodule R M))
          {x : Submodule R M | ∃ (s : LieSubmodule R L M), (∃ x ∈ N, lieSpan R L {x} = s) ∧ (↑s : Submodule R M) = x}
          p →
        p ≤ N'),
  m ∈ N'
Tactic: refine fun m hm ↦ Submodule.mem_sSup.mpr fun N' hN' ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (hypothesis)
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 : M
hm : m ∈ (↑N : Submodule R M)
N' : Submodule R M
hN' :
  ∀ (p : Submodule R M),
    Membership.mem (γ := Set (Submodule R M))
        {x : Submodule R M | ∃ (s : LieSubmodule R L M), (∃ x ∈ N, lieSpan R L {x} = s) ∧ (↑s : Submodule R M) = x} p →
      p ≤ N'
⊢ m ∈ N'
have hN'₁ : ∀ m ∈ N, (↑(lieSpan R L {m}) : Submodule R M) ≤ N'
Tactic: replace hN' : ∀ m ∈ N, lieSpan R L {m} ≤ N' := by simpa using hN'
Cleared hypotheses: hN'
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (goal)
Goal:
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieRing L'
inst_3 : LieAlgebra R L'
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : LieRingModule L M
inst_7 : AddCommGroup M'
inst_8 : Module R M'
inst_9 : LieRingModule L M'
f : M →ₗ⁅R,L⁆ M'
N N₂ : LieSubmodule R L M
N' : LieSubmodule R L M'
x : L
m' : M'
h : m' ∈ (Submodule.map (↑f : M →ₗ[R] M') (↑N : Submodule R M)).carrier
⊢ ⁅x, m'⁆ ∈ (Submodule.map (↑f : M →ₗ[R] M') (↑N : Submodule R M)).carrier
have rcases : ∀ (m : M) (hm : m ∈ (↑(↑N : Submodule R M) : Set M)) (hfm : ((↑f : M →ₗ[R] M') : (a : M) → M') m = m'),
  ⁅x, m'⁆ ∈ (Submodule.map (↑f : M →ₗ[R] M') (↑N : Submodule R M)).carrier
Tactic: rcases h with ⟨m, hm, hfm⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (goal)
Goal:
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieRing L'
inst_3 : LieAlgebra R L'
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : LieRingModule L M
inst_7 : AddCommGroup M'
inst_8 : Module R M'
inst_9 : LieRingModule L M'
f : M →ₗ⁅R,L⁆ M'
N N₂ : LieSubmodule R L M
N' : LieSubmodule R L M'
x : L
m' : M'
m : M
hm : m ∈ (↑(↑N : Submodule R M) : Set M)
hfm : ((↑f : M →ₗ[R] M') : (a : M) → M') m = m'
⊢ ⁅x, m'⁆ ∈ (Submodule.map (↑f : M →ₗ[R] M') (↑N : Submodule R M)).carrier
have h : ⁅x, m⁆ ∈ (↑(↑N : Submodule R M) : Set M) ∧ ((↑f : M →ₗ[R] M') : (a : M) → M') ⁅x, m⁆ = ⁅x, m'⁆
Tactic: use ⁅x, m⁆
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (goal)
Goal:
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieRing L'
inst_3 : LieAlgebra R L'
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : LieRingModule L M
inst_7 : AddCommGroup M'
inst_8 : Module R M'
inst_9 : LieRingModule L M'
f : M →ₗ⁅R,L⁆ M'
N N₂ : LieSubmodule R L M
N' : LieSubmodule R L M'
x : L
m' : M'
m : M
hm : m ∈ (↑(↑N : Submodule R M) : Set M)
hfm : ((↑f : M →ₗ[R] M') : (a : M) → M') m = m'
⊢ ⁅x, m⁆ ∈ (↑(↑N : Submodule R M) : Set M) ∧ ((↑f : M →ₗ[R] M') : (a : M) → M') ⁅x, m⁆ = ⁅x, m'⁆
have h : ⁅x, m⁆ ∈ (↑(↑N : Submodule R M) : Set M)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (goal)
Goal:
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieRing L'
inst_3 : LieAlgebra R L'
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : LieRingModule L M
inst_7 : AddCommGroup M'
inst_8 : Module R M'
inst_9 : LieRingModule L M'
f : M →ₗ⁅R,L⁆ M'
N N₂ : LieSubmodule R L M
N' : LieSubmodule R L M'
x : L
m' : M'
m : M
hm : m ∈ (↑(↑N : Submodule R M) : Set M)
hfm : ((↑f : M →ₗ[R] M') : (a : M) → M') m = m'
h : ⁅x, m⁆ ∈ (↑(↑N : Submodule R M) : Set M)
⊢ ⁅x, m⁆ ∈ (↑(↑N : Submodule R M) : Set M) ∧ ((↑f : M →ₗ[R] M') : (a : M) → M') ⁅x, m⁆ = ⁅x, m'⁆
have h₁ : ((↑f : M →ₗ[R] M') : (a : M) → M') ⁅x, m⁆ = ⁅x, m'⁆
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (goal)
Goal:
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieRing L'
inst_3 : LieAlgebra R L'
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : LieRingModule L M
inst_7 : AddCommGroup M'
inst_8 : Module R M'
inst_9 : LieRingModule L M'
f : M →ₗ⁅R,L⁆ M'
N N₂ : LieSubmodule R L M
N' : LieSubmodule R L M'
x : L
m : M
h : m ∈ (Submodule.comap (↑f : M →ₗ[R] M') (↑N' : Submodule R M')).carrier
⊢ ⁅x, m⁆ ∈ (Submodule.comap (↑f : M →ₗ[R] M') (↑N' : Submodule R M')).carrier
have suffices : Membership.mem (α := M') N' (⁅x, (f : (a : M) → M') m⁆ : M')
Tactic: suffices ⁅x, f m⁆ ∈ N' by simp [this]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (goal)
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
⊢ comap N.incl N₂ = ⊤ ↔ N ≤ N₂
have rw : (↑(comap N.incl N₂) : Submodule R ↥N) = (↑⊤ : Submodule R ↥N) ↔ N ≤ N₂
Tactic: rw [← LieSubmodule.toSubmodule_inj, LieSubmodule.toSubmodule_comap, LieSubmodule.incl_coe,
    LieSubmodule.top_toSubmodule, Submodule.comap_subtype_eq_top, toSubmodule_le_toSubmodule]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (goal)
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
rw : (↑(comap N.incl N₂) : Submodule R ↥N) = (↑⊤ : Submodule R ↥N) ↔ N ≤ N₂
⊢ comap N.incl N₂ = ⊤ ↔ N ≤ N₂
have rw₁ : Submodule.comap (↑N.incl : ↥N →ₗ[R] M) (↑N₂ : Submodule R M) = (↑⊤ : Submodule R ↥N) ↔ N ≤ N₂
Tactic: rw [← LieSubmodule.toSubmodule_inj, LieSubmodule.toSubmodule_comap, LieSubmodule.incl_coe,
    LieSubmodule.top_toSubmodule, Submodule.comap_subtype_eq_top, toSubmodule_le_toSubmodule]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (goal)
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
rw : (↑(comap N.incl N₂) : Submodule R ↥N) = (↑⊤ : Submodule R ↥N) ↔ N ≤ N₂
rw₁ : Submodule.comap (↑N.incl : ↥N →ₗ[R] M) (↑N₂ : Submodule R M) = (↑⊤ : Submodule R ↥N) ↔ N ≤ N₂
⊢ comap N.incl N₂ = ⊤ ↔ N ≤ N₂
have rw₂ : Submodule.comap (↑N : Submodule R M).subtype (↑N₂ : Submodule R M) = (↑⊤ : Submodule R ↥N) ↔ N ≤ N₂
Tactic: rw [← LieSubmodule.toSubmodule_inj, LieSubmodule.toSubmodule_comap, LieSubmodule.incl_coe,
    LieSubmodule.top_toSubmodule, Submodule.comap_subtype_eq_top, toSubmodule_le_toSubmodule]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (goal)
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
rw : (↑(comap N.incl N₂) : Submodule R ↥N) = (↑⊤ : Submodule R ↥N) ↔ N ≤ N₂
rw₁ : Submodule.comap (↑N.incl : ↥N →ₗ[R] M) (↑N₂ : Submodule R M) = (↑⊤ : Submodule R ↥N) ↔ N ≤ N₂
rw₂ : Submodule.comap (↑N : Submodule R M).subtype (↑N₂ : Submodule R M) = (↑⊤ : Submodule R ↥N) ↔ N ≤ N₂
⊢ comap N.incl N₂ = ⊤ ↔ N ≤ N₂
have rw₃ : Submodule.comap (↑N : Submodule R M).subtype (↑N₂ : Submodule R M) = ⊤ ↔ N ≤ N₂
Tactic: rw [← LieSubmodule.toSubmodule_inj, LieSubmodule.toSubmodule_comap, LieSubmodule.incl_coe,
    LieSubmodule.top_toSubmodule, Submodule.comap_subtype_eq_top, toSubmodule_le_toSubmodule]