awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
L₂ : Type u_1
M₂ : Type u_2
inst_7 : LieRing L₂
inst_8 : LieAlgebra R L₂
inst_9 : AddCommGroup M₂
inst_10 : Module R M₂
inst_11 : LieRingModule L₂ M₂
f : L →ₗ⁅R⁆ L₂
g : M →ₗ[R] M₂
hfg :
  ∀ (x : L) (m : M),
    Eq.{u_2 + 1} (α := M₂)
      (Bracket.bracket.{u_1, u_2} (L := L₂) ((f : (a : L) → L₂) x : L₂) ((g : (a : M) → M₂) m) : M₂)
      ((g : (a : M) → M₂) ⁅x, m⁆ : M₂)
inst_12 : LieModule R L₂ M₂
hf_surj : Surjective.{v + 1, u_1 + 1} (α := L) (β := L₂) (⇑f : (a : L) → L₂)
hg_surj : Surjective.{w + 1, u_2 + 1} (α := M) (β := M₂) (⇑g : (a : M) → M₂)
k : ℕ
ih :
  (↑(lowerCentralSeries R L₂ M₂ k) : Submodule R M₂) ≤ Submodule.map g (↑(lowerCentralSeries R L M k) : Submodule R M)
succ :
  Subset.{u_2} (α := Set M₂)
    {m : M₂ |
      ∃ (x : L₂) (n : M),
        Membership.mem (γ := LieSubmodule R L M) (lowerCentralSeries R L M k) n ∧ ⁅x, (g : (a : M) → M₂) n⁆ = m}
    (Set.image.{w, u_2} (α := M) (⇑g : (a : M) → M₂)
      {m : M | ∃ (x : L) (n : M), Membership.mem (γ := LieSubmodule R L M) (lowerCentralSeries R L M k) n ∧ ⁅x, n⁆ = m})
⊢ (↑(lowerCentralSeries R L₂ M₂ (k + 1)) : Submodule R M₂) ≤
    Submodule.map g (↑(lowerCentralSeries R L M (k + 1)) : Submodule R M)

Tactic:
suffices
      {m | ∃ (x : L₂) (n : _), n ∈ lowerCentralSeries R L M k ∧ ⁅x, g n⁆ = m} ⊆
        g '' {m | ∃ (x : L) (n : _), n ∈ lowerCentralSeries R L M k ∧ ⁅x, n⁆ = m} by
      simp only [← LieSubmodule.mem_toSubmodule] at this
      simp_rw [lowerCentralSeries_succ, LieSubmodule.lieIdeal_oper_eq_linear_span',
        Submodule.map_span, LieSubmodule.mem_top, true_and, ← LieSubmodule.mem_toSubmodule]
      refine Submodule.span_mono (Set.Subset.trans ?_ this)
      rintro m₁ ⟨x, n, hn, rfl⟩
      obtain ⟨n', hn', rfl⟩ := ih hn
      exact ⟨x, n', hn', rfl⟩
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
L₂ : Type u_1
M₂ : Type u_2
inst_7 : LieRing L₂
inst_8 : LieAlgebra R L₂
inst_9 : AddCommGroup M₂
inst_10 : Module R M₂
inst_11 : LieRingModule L₂ M₂
f : L →ₗ⁅R⁆ L₂
g : M →ₗ[R] M₂
hfg :
  ∀ (x : L) (m : M),
    Eq.{u_2 + 1} (α := M₂)
      (Bracket.bracket.{u_1, u_2} (L := L₂) ((f : (a : L) → L₂) x : L₂) ((g : (a : M) → M₂) m) : M₂)
      ((g : (a : M) → M₂) ⁅x, m⁆ : M₂)
inst_12 : LieModule R L₂ M₂
hf_surj : Surjective.{v + 1, u_1 + 1} (α := L) (β := L₂) (⇑f : (a : L) → L₂)
hg_surj : Surjective.{w + 1, u_2 + 1} (α := M) (β := M₂) (⇑g : (a : M) → M₂)
k : ℕ
ih :
  (↑(lowerCentralSeries R L₂ M₂ k) : Submodule R M₂) ≤ Submodule.map g (↑(lowerCentralSeries R L M k) : Submodule R M)
x : L₂
n : M
hn : Membership.mem (γ := LieSubmodule R L M) (lowerCentralSeries R L M k) n
succ :
  ∀ (y : L),
    Membership.mem.{u_2, u_2} (α := M₂) (γ := Set M₂)
      (Set.image.{w, u_2} (α := M) (⇑g : (a : M) → M₂)
        {m : M |
          ∃ (x : L) (n : M), Membership.mem (γ := LieSubmodule R L M) (lowerCentralSeries R L M k) n ∧ ⁅x, n⁆ = m})
      (Bracket.bracket.{u_1, u_2} (L := L₂) ((f : (a : L) → L₂) y : L₂) ((g : (a : M) → M₂) n) : M₂)
⊢ Membership.mem.{u_2, u_2} (α := M₂) (γ := Set M₂)
    (Set.image.{w, u_2} (α := M) (⇑g : (a : M) → M₂)
      {m : M | ∃ (x : L) (n : M), Membership.mem (γ := LieSubmodule R L M) (lowerCentralSeries R L M k) n ∧ ⁅x, n⁆ = m})
    (⁅x, (g : (a : M) → M₂) n⁆ : M₂)

Tactic:
obtain ⟨y, rfl⟩ := hf_surj x

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
L₂ : Type u_1
M₂ : Type u_2
inst_7 : LieRing L₂
inst_8 : LieAlgebra R L₂
inst_9 : AddCommGroup M₂
inst_10 : Module R M₂
inst_11 : LieRingModule L₂ M₂
f : L →ₗ⁅R⁆ L₂
g : M →ₗ[R] M₂
hfg :
  ∀ (x : L) (m : M),
    Eq.{u_2 + 1} (α := M₂)
      (Bracket.bracket.{u_1, u_2} (L := L₂) ((f : (a : L) → L₂) x : L₂) ((g : (a : M) → M₂) m) : M₂)
      ((g : (a : M) → M₂) ⁅x, m⁆ : M₂)
inst_12 : LieModule R L₂ M₂
hf_surj : Surjective.{v + 1, u_1 + 1} (α := L) (β := L₂) (⇑f : (a : L) → L₂)
hg_surj : Surjective.{w + 1, u_2 + 1} (α := M) (β := M₂) (⇑g : (a : M) → M₂)
k : ℕ
ih :
  (↑(lowerCentralSeries R L₂ M₂ k) : Submodule R M₂) ≤ Submodule.map g (↑(lowerCentralSeries R L M k) : Submodule R M)
n : M
hn : Membership.mem (γ := LieSubmodule R L M) (lowerCentralSeries R L M k) n
y : L
⊢ Membership.mem.{u_2, u_2} (α := M₂) (γ := Set M₂)
    (Set.image.{w, u_2} (α := M) (⇑g : (a : M) → M₂)
      {m : M | ∃ (x : L) (n : M), Membership.mem (γ := LieSubmodule R L M) (lowerCentralSeries R L M k) n ∧ ⁅x, n⁆ = m})
    (Bracket.bracket.{u_1, u_2} (L := L₂) ((f : (a : L) → L₂) y : L₂) ((g : (a : M) → M₂) n) : M₂)

Tactic:
⟨⁅y, n⁆, ⟨y, n, hn, rfl⟩, (hfg y n).symm⟩

Premises used: Set.Mem, Bracket.bracket, setOf, And.intro, Exists.intro, Set.image, Eq.symm, rfl
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
L₂ : Type u_1
M₂ : Type u_2
inst_7 : LieRing L₂
inst_8 : LieAlgebra R L₂
inst_9 : AddCommGroup M₂
inst_10 : Module R M₂
inst_11 : LieRingModule L₂ M₂
f : L →ₗ⁅R⁆ L₂
g : M →ₗ[R] M₂
hfg :
  ∀ (x : L) (m : M),
    Eq.{u_2 + 1} (α := M₂)
      (Bracket.bracket.{u_1, u_2} (L := L₂) ((f : (a : L) → L₂) x : L₂) ((g : (a : M) → M₂) m) : M₂)
      ((g : (a : M) → M₂) ⁅x, m⁆ : M₂)
inst_12 : LieModule R L₂ M₂
hf_surj : Surjective.{v + 1, u_1 + 1} (α := L) (β := L₂) (⇑f : (a : L) → L₂)
hg_surj : Surjective.{w + 1, u_2 + 1} (α := M) (β := M₂) (⇑g : (a : M) → M₂)
k : ℕ
ih :
  (↑(lowerCentralSeries R L₂ M₂ k) : Submodule R M₂) ≤ Submodule.map g (↑(lowerCentralSeries R L M k) : Submodule R M)
n : M
hn : Membership.mem (γ := LieSubmodule R L M) (lowerCentralSeries R L M k) n
y : L
⊢ Membership.mem.{u_2, u_2} (α := M₂) (γ := Set M₂)
    (Set.image.{w, u_2} (α := M) (⇑g : (a : M) → M₂)
      {m : M | ∃ (x : L) (n : M), Membership.mem (γ := LieSubmodule R L M) (lowerCentralSeries R L M k) n ∧ ⁅x, n⁆ = m})
    (Bracket.bracket.{u_1, u_2} (L := L₂) ((f : (a : L) → L₂) y : L₂) ((g : (a : M) → M₂) n) : M₂)

Tactic:
exact ⟨⁅y, n⁆, ⟨y, n, hn, rfl⟩, (hfg y n).symm⟩
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
L₂ : Type u_1
M₂ : Type u_2
inst_7 : LieRing L₂
inst_8 : LieAlgebra R L₂
inst_9 : AddCommGroup M₂
inst_10 : Module R M₂
inst_11 : LieRingModule L₂ M₂
f : L →ₗ⁅R⁆ L₂
g : M →ₗ[R] M₂
hfg :
  ∀ (x : L) (m : M),
    Eq.{u_2 + 1} (α := M₂)
      (Bracket.bracket.{u_1, u_2} (L := L₂) ((f : (a : L) → L₂) x : L₂) ((g : (a : M) → M₂) m) : M₂)
      ((g : (a : M) → M₂) ⁅x, m⁆ : M₂)
inst_12 : LieModule R L₂ M₂
hf_surj : Surjective.{v + 1, u_1 + 1} (α := L) (β := L₂) (⇑f : (a : L) → L₂)
hg_surj : Surjective.{w + 1, u_2 + 1} (α := M) (β := M₂) (⇑g : (a : M) → M₂)
k : ℕ
zero :
  (↑(lowerCentralSeries R L₂ M₂ 0) : Submodule R M₂) ≤ Submodule.map g (↑(lowerCentralSeries R L M 0) : Submodule R M)
succ :
  ∀ (k : ℕ)
    (ih :
      (↑(lowerCentralSeries R L₂ M₂ k) : Submodule R M₂) ≤
        Submodule.map g (↑(lowerCentralSeries R L M k) : Submodule R M)),
    (↑(lowerCentralSeries R L₂ M₂ (k + 1)) : Submodule R M₂) ≤
      Submodule.map g (↑(lowerCentralSeries R L M (k + 1)) : Submodule R M)
⊢ (↑(lowerCentralSeries R L₂ M₂ k) : Submodule R M₂) ≤ Submodule.map g (↑(lowerCentralSeries R L M k) : Submodule R M)

Tactic:
induction k with
  | zero => simpa [LinearMap.range_eq_top]
  | succ k ih =>
    suffices
      {m | ∃ (x : L₂) (n : _), n ∈ lowerCentralSeries R L M k ∧ ⁅x, g n⁆ = m} ⊆
        g '' {m | ∃ (x : L) (n : _), n ∈ lowerCentralSeries R L M k ∧ ⁅x, n⁆ = m} by
      simp only [← LieSubmodule.mem_toSubmodule] at this
      simp_rw [lowerCentralSeries_succ, LieSubmodule.lieIdeal_oper_eq_linear_span',
        Submodule.map_span, LieSubmodule.mem_top, true_and, ← LieSubmodule.mem_toSubmodule]
      refine Submodule.span_mono (Set.Subset.trans ?_ this)
      rintro m₁ ⟨x, n, hn, rfl⟩
      obtain ⟨n', hn', rfl⟩ := ih hn
      exact ⟨x, n', hn', rfl⟩
    rintro m₂ ⟨x, n, hn, rfl⟩
    obtain ⟨y, rfl⟩ := hf_surj x
    exact ⟨⁅y, n⁆, ⟨y, n, hn, rfl⟩, (hfg y n).symm⟩

Premises used: LinearMap.range_eq_top, rfl
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
L₂ : Type u_1
M₂ : Type u_2
inst_7 : LieRing L₂
inst_8 : LieAlgebra R L₂
inst_9 : AddCommGroup M₂
inst_10 : Module R M₂
inst_11 : LieRingModule L₂ M₂
f : L →ₗ⁅R⁆ L₂
g : M →ₗ[R] M₂
hfg :
  ∀ (x : L) (m : M),
    Eq.{u_2 + 1} (α := M₂)
      (Bracket.bracket.{u_1, u_2} (L := L₂) ((f : (a : L) → L₂) x : L₂) ((g : (a : M) → M₂) m) : M₂)
      ((g : (a : M) → M₂) ⁅x, m⁆ : M₂)
inst_12 : LieModule R L₂ M₂
hf_surj : Surjective.{v + 1, u_1 + 1} (α := L) (β := L₂) (⇑f : (a : L) → L₂)
hg_surj : Surjective.{w + 1, u_2 + 1} (α := M) (β := M₂) (⇑g : (a : M) → M₂)
inst_13 : LieModule.IsNilpotent L M
obtain : ∀ (k : ℕ) (hk : Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥), LieModule.IsNilpotent L₂ M₂
⊢ LieModule.IsNilpotent L₂ M₂

Tactic:
obtain ⟨k, hk⟩ := IsNilpotent.nilpotent R L M

Premises used: LieModule.IsNilpotent.nilpotent
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
L₂ : Type u_1
M₂ : Type u_2
inst_7 : LieRing L₂
inst_8 : LieAlgebra R L₂
inst_9 : AddCommGroup M₂
inst_10 : Module R M₂
inst_11 : LieRingModule L₂ M₂
f : L →ₗ⁅R⁆ L₂
g : M →ₗ[R] M₂
hfg :
  ∀ (x : L) (m : M),
    Eq.{u_2 + 1} (α := M₂)
      (Bracket.bracket.{u_1, u_2} (L := L₂) ((f : (a : L) → L₂) x : L₂) ((g : (a : M) → M₂) m) : M₂)
      ((g : (a : M) → M₂) ⁅x, m⁆ : M₂)
inst_12 : LieModule R L₂ M₂
hf_surj : Surjective.{v + 1, u_1 + 1} (α := L) (β := L₂) (⇑f : (a : L) → L₂)
hg_surj : Surjective.{w + 1, u_2 + 1} (α := M) (β := M₂) (⇑g : (a : M) → M₂)
inst_13 : LieModule.IsNilpotent L M
k : ℕ
hk : Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥
rw : ∃ (k : ℕ), Eq (α := LieSubmodule R L₂ M₂) (lowerCentralSeries R L₂ M₂ k) ⊥
⊢ LieModule.IsNilpotent L₂ M₂

Tactic:
rw [isNilpotent_iff R]

Premises used: LieModule.isNilpotent_iff
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
L₂ : Type u_1
M₂ : Type u_2
inst_7 : LieRing L₂
inst_8 : LieAlgebra R L₂
inst_9 : AddCommGroup M₂
inst_10 : Module R M₂
inst_11 : LieRingModule L₂ M₂
f : L →ₗ⁅R⁆ L₂
g : M →ₗ[R] M₂
hfg :
  ∀ (x : L) (m : M),
    Eq.{u_2 + 1} (α := M₂)
      (Bracket.bracket.{u_1, u_2} (L := L₂) ((f : (a : L) → L₂) x : L₂) ((g : (a : M) → M₂) m) : M₂)
      ((g : (a : M) → M₂) ⁅x, m⁆ : M₂)
inst_12 : LieModule R L₂ M₂
hf_surj : Surjective.{v + 1, u_1 + 1} (α := L) (β := L₂) (⇑f : (a : L) → L₂)
hg_surj : Surjective.{w + 1, u_2 + 1} (α := M) (β := M₂) (⇑g : (a : M) → M₂)
inst_13 : LieModule.IsNilpotent L M
k : ℕ
hk : Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥
h : Eq (α := LieSubmodule R L₂ M₂) (lowerCentralSeries R L₂ M₂ k) ⊥
⊢ ∃ (k : ℕ), Eq (α := LieSubmodule R L₂ M₂) (lowerCentralSeries R L₂ M₂ k) ⊥

Tactic:
use k
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
L₂ : Type u_1
M₂ : Type u_2
inst_7 : LieRing L₂
inst_8 : LieAlgebra R L₂
inst_9 : AddCommGroup M₂
inst_10 : Module R M₂
inst_11 : LieRingModule L₂ M₂
f : L →ₗ⁅R⁆ L₂
g : M →ₗ[R] M₂
hfg :
  ∀ (x : L) (m : M),
    Eq.{u_2 + 1} (α := M₂)
      (Bracket.bracket.{u_1, u_2} (L := L₂) ((f : (a : L) → L₂) x : L₂) ((g : (a : M) → M₂) m) : M₂)
      ((g : (a : M) → M₂) ⁅x, m⁆ : M₂)
inst_12 : LieModule R L₂ M₂
hf_surj : Surjective.{v + 1, u_1 + 1} (α := L) (β := L₂) (⇑f : (a : L) → L₂)
hg_surj : Surjective.{w + 1, u_2 + 1} (α := M) (β := M₂) (⇑g : (a : M) → M₂)
inst_13 : LieModule.IsNilpotent L M
k : ℕ
hk : Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥
h :
  ∀ (hk : Eq (α := Submodule R M) (↑(lowerCentralSeries R L M k) : Submodule R M) (↑⊥ : Submodule R M)),
    Eq (α := Submodule R M₂) (↑(lowerCentralSeries R L₂ M₂ k) : Submodule R M₂) (↑⊥ : Submodule R M₂)
⊢ Eq (α := LieSubmodule R L₂ M₂) (lowerCentralSeries R L₂ M₂ k) ⊥

Tactic:
rw [← LieSubmodule.toSubmodule_inj] at hk ⊢

Premises used: LieSubmodule.toSubmodule_inj
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
L₂ : Type u_1
M₂ : Type u_2
inst_7 : LieRing L₂
inst_8 : LieAlgebra R L₂
inst_9 : AddCommGroup M₂
inst_10 : Module R M₂
inst_11 : LieRingModule L₂ M₂
f : L →ₗ⁅R⁆ L₂
g : M →ₗ[R] M₂
hfg :
  ∀ (x : L) (m : M),
    Eq.{u_2 + 1} (α := M₂)
      (Bracket.bracket.{u_1, u_2} (L := L₂) ((f : (a : L) → L₂) x : L₂) ((g : (a : M) → M₂) m) : M₂)
      ((g : (a : M) → M₂) ⁅x, m⁆ : M₂)
inst_12 : LieModule R L₂ M₂
hf_surj : Surjective.{v + 1, u_1 + 1} (α := L) (β := L₂) (⇑f : (a : L) → L₂)
hg_surj : Surjective.{w + 1, u_2 + 1} (α := M) (β := M₂) (⇑g : (a : M) → M₂)
inst_13 : LieModule.IsNilpotent L M
k : ℕ
hk : Eq (α := Submodule R M) (↑(lowerCentralSeries R L M k) : Submodule R M) (↑⊥ : Submodule R M)
⊢ Eq (α := Submodule R M₂) (↑(lowerCentralSeries R L₂ M₂ k) : Submodule R M₂) (↑⊥ : Submodule R M₂)

Tactic:
simp [← hf_surj.lieModule_lcs_map_eq hfg hg_surj k, hk]

Premises used: Function.Surjective.lieModule_lcs_map_eq
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
⊢ IsNilpotent.{v, w} (↥⊤) M ↔ IsNilpotent L M

Tactic:
Equiv.lieModule_isNilpotent_iff LieSubalgebra.topEquiv (1 : M ≃ₗ[R] M) fun _ _ => rfl

Premises used: Equiv.lieModule_isNilpotent_iff, LieSubalgebra.topEquiv, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
⊢ IsNilpotent.{v, w} L ↥⊤ ↔ IsNilpotent L M

Tactic:
Equiv.lieModule_isNilpotent_iff 1 (LinearEquiv.ofTop ⊤ rfl) fun _ _ ↦ rfl

Premises used: Equiv.lieModule_isNilpotent_iff, LinearEquiv.ofTop, Top.top, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
M₁ M₂ : LieSubmodule R L M
h₁ : M₁ ≤ M₂
inst_7 : IsNilpotent.{v, w} L ↥M₂
f : L →ₗ⁅R⁆ L := LieHom.id
g : ↥M₁ →ₗ[R] ↥M₂ := Submodule.inclusion h₁
⊢ ∀ (x : L) (m : ↥M₁),
    Eq (α := ↥M₂) (Bracket.bracket (L := L) ((f : (a : L) → L) x : L) ((g : (a : ↥M₁) → ↥M₂) m) : ↥M₂)
      ((g : (a : ↥M₁) → ↥M₂) ⁅x, m⁆ : ↥M₂)

Tactic:
aesop
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
M₁ M₂ : LieSubmodule R L M
h₁ : M₁ ≤ M₂
inst_7 : IsNilpotent.{v, w} L ↥M₂
f : L →ₗ⁅R⁆ L := LieHom.id
g : ↥M₁ →ₗ[R] ↥M₂ := Submodule.inclusion h₁
⊢ ∀ (x : L) (m : ↥M₁),
    Eq (α := ↥M₂) (Bracket.bracket (L := L) ((f : (a : L) → L) x : L) ((g : (a : ↥M₁) → ↥M₂) m) : ↥M₂)
      ((g : (a : ↥M₁) → ↥M₂) ⁅x, m⁆ : ↥M₂)

Tactic:
have hfg : ∀ x m, ⁅f x, g m⁆ = g ⁅x, m⁆ := by aesop
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
M₁ M₂ : LieSubmodule R L M
h₁ : M₁ ≤ M₂
inst_7 : IsNilpotent.{v, w} L ↥M₂
f : L →ₗ⁅R⁆ L := LieHom.id
g : ↥M₁ →ₗ[R] ↥M₂ := Submodule.inclusion h₁
hfg :
  ∀ (x : L) (m : ↥M₁),
    Eq (α := ↥M₂) (Bracket.bracket (L := L) ((f : (a : L) → L) x : L) ((g : (a : ↥M₁) → ↥M₂) m) : ↥M₂)
      ((g : (a : ↥M₁) → ↥M₂) ⁅x, m⁆ : ↥M₂)
⊢ IsNilpotent.{v, w} L ↥M₁

Tactic:
(Submodule.inclusion_injective h₁).lieModuleIsNilpotent hfg

Premises used: Function.Injective.lieModuleIsNilpotent, Submodule.inclusion_injective
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
M₁ M₂ : LieSubmodule R L M
h₁ : M₁ ≤ M₂
inst_7 : IsNilpotent.{v, w} L ↥M₂
f : L →ₗ⁅R⁆ L := LieHom.id
g : ↥M₁ →ₗ[R] ↥M₂ := Submodule.inclusion h₁
hfg :
  ∀ (x : L) (m : ↥M₁),
    Eq (α := ↥M₂) (Bracket.bracket (L := L) ((f : (a : L) → L) x : L) ((g : (a : ↥M₁) → ↥M₂) m) : ↥M₂)
      ((g : (a : ↥M₁) → ↥M₂) ⁅x, m⁆ : ↥M₂)
⊢ IsNilpotent.{v, w} L ↥M₁

Tactic:
exact (Submodule.inclusion_injective h₁).lieModuleIsNilpotent hfg

Premises used: Function.Injective.lieModuleIsNilpotent, Submodule.inclusion_injective
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
k : ℕ
N : LieSubmodule R L M
inst_6 : LieModule R L M
inst_7 : IsNoetherian R M
⊢ CompleteLattice.IsSupClosedCompact.{w} (LieSubmodule R L M)

Tactic:
have hwf := CompleteLattice.WellFoundedGT.isSupClosedCompact (LieSubmodule R L M) inferInstance
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
k : ℕ
N : LieSubmodule R L M
inst_6 : LieModule R L M
inst_7 : IsNoetherian R M
hwf : CompleteLattice.IsSupClosedCompact.{w} (LieSubmodule R L M)
⊢ IsNilpotent.{v, w} L ↥(maxNilpotentSubmodule R L M)

Tactic:
hwf { N : LieSubmodule R L M | IsNilpotent L N } ⟨⊥, ?_⟩ fun N₁ h₁ N₂ h₂ => ?_

Premises used: LieModule.maxNilpotentSubmodule, Set.Mem, setOf, Membership.mem, Subtype, Bot.bot, Exists.intro, LieModule.IsNilpotent
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
k : ℕ
N : LieSubmodule R L M
inst_6 : LieModule R L M
inst_7 : IsNoetherian R M
hwf : CompleteLattice.IsSupClosedCompact.{w} (LieSubmodule R L M)
refine_1 : Membership.mem (γ := Set (LieSubmodule R L M)) {N : LieSubmodule R L M | IsNilpotent.{v, w} L ↥N} ⊥
refine_2 :
  ∀ (N₁ : LieSubmodule R L M)
    (h₁ : Membership.mem (γ := Set (LieSubmodule R L M)) {N : LieSubmodule R L M | IsNilpotent.{v, w} L ↥N} N₁)
    (N₂ : LieSubmodule R L M)
    (h₂ : Membership.mem (γ := Set (LieSubmodule R L M)) {N : LieSubmodule R L M | IsNilpotent.{v, w} L ↥N} N₂),
    Membership.mem (γ := Set (LieSubmodule R L M)) {N : LieSubmodule R L M | IsNilpotent.{v, w} L ↥N} (N₁ ⊔ N₂)
⊢ IsNilpotent.{v, w} L ↥(maxNilpotentSubmodule R L M)

Tactic:
refine hwf { N : LieSubmodule R L M | IsNilpotent L N } ⟨⊥, ?_⟩ fun N₁ h₁ N₂ h₂ => ?_

Premises used: setOf, Membership.mem, Subtype, Bot.bot, Exists.intro, LieModule.IsNilpotent
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
k : ℕ
N : LieSubmodule R L M
inst_6 : LieModule R L M
inst_7 : IsNoetherian R M
hwf : CompleteLattice.IsSupClosedCompact.{w} (LieSubmodule R L M)
N₁ : LieSubmodule R L M
h₁ : Membership.mem (γ := Set (LieSubmodule R L M)) {N : LieSubmodule R L M | IsNilpotent.{v, w} L ↥N} N₁
N₂ : LieSubmodule R L M
h₂ : Membership.mem (γ := Set (LieSubmodule R L M)) {N : LieSubmodule R L M | IsNilpotent.{v, w} L ↥N} N₂
⊢ IsNilpotent.{v, w} L ↥N₁

Tactic:
simp_all
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
k : ℕ
N : LieSubmodule R L M
inst_6 : LieModule R L M
inst_7 : IsNoetherian R M
hwf : CompleteLattice.IsSupClosedCompact.{w} (LieSubmodule R L M)
N₁ : LieSubmodule R L M
h₁ : Membership.mem (γ := Set (LieSubmodule R L M)) {N : LieSubmodule R L M | IsNilpotent.{v, w} L ↥N} N₁
N₂ : LieSubmodule R L M
h₂ : Membership.mem (γ := Set (LieSubmodule R L M)) {N : LieSubmodule R L M | IsNilpotent.{v, w} L ↥N} N₂
h₃ : IsNilpotent.{v, w} L ↥N₁
⊢ IsNilpotent.{v, w} L ↥N₂

Tactic:
simp_all
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
k : ℕ
N : LieSubmodule R L M
inst_6 : LieModule R L M
inst_7 : IsNoetherian R M
hwf : CompleteLattice.IsSupClosedCompact.{w} (LieSubmodule R L M)
⊢ IsNilpotent.{v, w} L ↥⊥

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
k : ℕ
N : LieSubmodule R L M
inst_6 : LieModule R L M
inst_7 : IsNoetherian R M
hwf : CompleteLattice.IsSupClosedCompact.{w} (LieSubmodule R L M)
N₁ N₂ : LieSubmodule R L M
h₁ : IsNilpotent.{v, w} L ↥N₁
h₂ : IsNilpotent.{v, w} L ↥N₂
⊢ IsNilpotent.{v, w} L ↥(N₁ ⊔ N₂)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : IsNoetherian R M
N : LieSubmodule R L M
⊢ IsNilpotent.{v, w} L ↥N ↔ N ≤ maxNilpotentSubmodule R L M

Tactic:
⟨fun h ↦ le_sSup h, fun h ↦ isNilpotent_of_le R L M N (maxNilpotentSubmodule R L M) h⟩

Premises used: LieModule.maxNilpotentSubmodule, Iff.intro, le_sSup, LieModule.isNilpotent_of_le
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : IsNilpotent L M
rw : LE.le (α := LieSubmodule R L M) ⊤ (maxNilpotentSubmodule R L M)
⊢ Eq (α := LieSubmodule R L M) (maxNilpotentSubmodule R L M) ⊤

Tactic:
rw [eq_top_iff]

Premises used: eq_top_iff
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : IsNilpotent L M
h : Membership.mem (γ := Set (LieSubmodule R L M)) {N : LieSubmodule R L M | IsNilpotent.{v, w} L ↥N} ⊤
⊢ LE.le (α := LieSubmodule R L M) ⊤ (maxNilpotentSubmodule R L M)

Tactic:
apply le_sSup

Premises used: le_sSup
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : IsNilpotent L M
⊢ Membership.mem (γ := Set (LieSubmodule R L M)) {N : LieSubmodule R L M | IsNilpotent.{v, w} L ↥N} ⊤

Tactic:
simpa