awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.Abelian
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
s : Set L
h : ∀ x ∈ s, ∀ y ∈ s, ⁅x, y⁆ = 0
x_1 x_2 : ↥(lieSpan R L s)
x y : L
hy : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) y
t : R
u : L
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) u
hu :
  ⁅Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) u hx,
      Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) y hy⁆ =
    0
⊢ ⁅u, y⁆ = 0

Tactic:
simp only [Subtype.ext_iff, coe_bracket, ZeroMemClass.coe_zero] at hu

Premises used: Subtype.ext_iff, LieSubalgebra.coe_bracket, ZeroMemClass.coe_zero
-- Module: Mathlib.Algebra.Lie.Abelian
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
s : Set L
h : ∀ x ∈ s, ∀ y ∈ s, ⁅x, y⁆ = 0
x_1 x_2 : ↥(lieSpan R L s)
x y : L
hy : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) y
t : R
u : L
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) u
hu : ⁅u, y⁆ = 0
⊢ ⁅Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) (t • u) ⋯,
      Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) y hy⁆ =
    0

Tactic:
simp [Subtype.ext_iff, hu]

Premises used: Subtype.ext_iff
-- Module: Mathlib.Algebra.Lie.Abelian
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
s : Set L
h : ∀ x ∈ s, ∀ y ∈ s, ⁅x, y⁆ = 0
x_1 x_2 : ↥(lieSpan R L s)
x y : L
hy : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) y
u v : L
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) u
hy_1 : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) v
hu :
  ⁅Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) u hx,
      Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) y hy⁆ =
    0
hv :
  ⁅Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) v hy_1,
      Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) y hy⁆ =
    0
refine_2 : ∀ (hu : ⁅u, y⁆ = 0) (hv : ⁅v, y⁆ = 0), ⁅⁅u, v⁆, y⁆ = 0
⊢ ⁅Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) ⁅u, v⁆ ⋯,
      Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) y hy⁆ =
    0

Tactic:
simp only [Subtype.ext_iff, coe_bracket, ZeroMemClass.coe_zero] at hu hv ⊢

Premises used: Subtype.ext_iff, LieSubalgebra.coe_bracket, ZeroMemClass.coe_zero
-- Module: Mathlib.Algebra.Lie.Abelian
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
s : Set L
h : ∀ x ∈ s, ∀ y ∈ s, ⁅x, y⁆ = 0
x_1 x_2 : ↥(lieSpan R L s)
x y : L
hy : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) y
u v : L
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) u
hy_1 : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) v
hu : ⁅u, y⁆ = 0
hv : ⁅v, y⁆ = 0
⊢ ⁅⁅u, v⁆, y⁆ = 0

Tactic:
simp [hu, hv]
-- Module: Mathlib.Algebra.Lie.Abelian
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
x : L
⊢ Membership.mem (γ := LieIdeal R L) (LieModule.ker R L M) x ↔ ∀ (m : M), ⁅x, m⁆ = 0

Tactic:
simp only [LieModule.ker, LieHom.mem_ker, LinearMap.ext_iff, LinearMap.zero_apply,
    toEnd_apply_apply]

Premises used: LinearMap.zero_apply, LinearMap.ext_iff, LieModule.toEnd_apply_apply, LieHom.mem_ker, LieModule.ker
-- Module: Mathlib.Algebra.Lie.Abelian
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
⊢ IsLieAbelian.{v} ↥I ↔ I ≤ LieModule.ker R L ↥I

Tactic:
⟨fun hI x hx ↦ LieHom.mem_ker.mpr ?_, fun h ↦ ⟨fun ⟨x, hx⟩ ⟨y, hy⟩ ↦ ?_⟩⟩

Premises used: Iff.mpr, Bracket.bracket, Subtype.mk, LieModule.IsTrivial.mk, LieHom.mem_ker, Iff.intro, _private.0.LieIdeal.isLieAbelian_iff.match_1, OfNat.ofNat, Eq
-- Module: Mathlib.Algebra.Lie.Abelian
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
refine_1 :
  ∀ (hI : IsLieAbelian.{v} ↥I) (x : L) (hx : x ∈ I),
    Eq (α := Module.End R ↥I) ((toEnd R L ↥I : (a : L) → Module.End R ↥I) x : Module.End R ↥I) (0 : Module.End R ↥I)
refine_2 :
  ∀ (h : I ≤ LieModule.ker R L ↥I) (x x : ↥I) (x : L) (hx : x ∈ I) (y : L) (hy : y ∈ I),
    ⁅Subtype.mk (p := fun (x : L) ↦ x ∈ I) x hx, Subtype.mk (p := fun (x : L) ↦ x ∈ I) y hy⁆ = 0
⊢ IsLieAbelian.{v} ↥I ↔ I ≤ LieModule.ker R L ↥I

Tactic:
refine ⟨fun hI x hx ↦ LieHom.mem_ker.mpr ?_, fun h ↦ ⟨fun ⟨x, hx⟩ ⟨y, hy⟩ ↦ ?_⟩⟩
-- Module: Mathlib.Algebra.Lie.Abelian
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
hI : IsLieAbelian.{v} ↥I
x : L
hx : x ∈ I
refine_1 :
  ∀ (y : ↥I),
    Eq.{v + 1} (α := L) (↑((((toEnd R L ↥I : (a : L) → Module.End R ↥I) x : Module.End R ↥I) : (a : ↥I) → ↥I) y) : L)
      (↑((0 : (a : ↥I) → ↥I) y) : L)
⊢ Eq (α := Module.End R ↥I) ((toEnd R L ↥I : (a : L) → Module.End R ↥I) x : Module.End R ↥I) (0 : Module.End R ↥I)

Tactic:
ext y
-- Module: Mathlib.Algebra.Lie.Abelian
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
hI : IsLieAbelian.{v} ↥I
x : L
hx : x ∈ I
y : ↥I
⊢ ⁅Subtype.mk (p := fun (x : L) ↦ x ∈ I) x hx, y⁆ = 0

Tactic:
have := IsTrivial.trivial (⟨x, hx⟩ : I) y
-- Module: Mathlib.Algebra.Lie.Abelian
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
hI : IsLieAbelian.{v} ↥I
x : L
hx : x ∈ I
y : ↥I
this : ⁅Subtype.mk (p := fun (x : L) ↦ x ∈ I) x hx, y⁆ = 0
⊢ ⁅(↑(Subtype.mk (p := fun (x : L) ↦ x ∈ I) x hx) : L), y⁆ = 0

Tactic:
rw [LieIdeal.coe_bracket_of_module] at this

Premises used: LieIdeal.coe_bracket_of_module
-- Module: Mathlib.Algebra.Lie.Abelian
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
hI : IsLieAbelian.{v} ↥I
x : L
hx : x ∈ I
y : ↥I
this : ⁅(↑(Subtype.mk (p := fun (x : L) ↦ x ∈ I) x hx) : L), y⁆ = 0
⊢ Eq.{v + 1} (α := L) (↑((((toEnd R L ↥I : (a : L) → Module.End R ↥I) x : Module.End R ↥I) : (a : ↥I) → ↥I) y) : L)
    (↑((0 : (a : ↥I) → ↥I) y) : L)

Tactic:
simp [this]
-- Module: Mathlib.Algebra.Lie.Abelian
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
h : I ≤ LieModule.ker R L ↥I
x_1 x_2 : ↥I
x : L
hx : x ∈ I
y : L
hy : y ∈ I
⊢ ⁅Subtype.mk (p := fun (x : L) ↦ x ∈ I) x hx, Subtype.mk (p := fun (x : L) ↦ x ∈ I) y hy⁆ = 0

Tactic:
simpa using LinearMap.congr_fun (h hx) ⟨y, hy⟩

Premises used: Subtype.mk, LinearMap.congr_fun
-- Module: Mathlib.Algebra.Lie.Abelian
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
rw :
  (∀ (x : L), (∀ (m : M), ⁅x, m⁆ = 0) → x = 0) ↔
    ∀ (m : L),
      Membership.mem (γ := LieSubmodule R L L) (LieModule.ker R L M) m ↔ Membership.mem (γ := LieSubmodule R L L) ⊥ m
⊢ IsFaithful R L M ↔ Eq (α := LieIdeal R L) (LieModule.ker R L M) ⊥

Tactic:
rw [isFaithful_iff', LieSubmodule.ext_iff]

Premises used: LieModule.isFaithful_iff', LieSubmodule.ext_iff
-- Module: Mathlib.Algebra.Lie.Abelian
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
⊢ (∀ (x : L), (∀ (m : M), ⁅x, m⁆ = 0) → x = 0) ↔
    ∀ (m : L),
      Membership.mem (γ := LieSubmodule R L L) (LieModule.ker R L M) m ↔ Membership.mem (γ := LieSubmodule R L L) ⊥ m

Tactic:
aesop
-- Module: Mathlib.Algebra.Lie.Abelian
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 : IsFaithful R L M
⊢ Eq (α := LieIdeal R L) (LieModule.ker R L M) ⊥

Tactic:
(isFaithful_iff_ker_eq_bot R L M).mp inferInstance

Premises used: inferInstance, LieModule.isFaithful_iff_ker_eq_bot, Iff.mp
-- Module: Mathlib.Algebra.Lie.Abelian
Goal:
R : Type u
L : Type v
M : Type w
N : 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 : AddCommGroup N
inst_8 : Module R N
inst_9 : LieRingModule L N
inst_10 : LieModule R L N
x y : M
hx : Membership.mem (γ := Set M) {m : M | ∀ (x : L), ⁅x, m⁆ = 0} x
hy : Membership.mem (γ := Set M) {m : M | ∀ (x : L), ⁅x, m⁆ = 0} y
z : L
rw : ⁅z, x⁆ + ⁅z, y⁆ = 0
rw₁ : 0 + ⁅z, y⁆ = 0
rw₂ : HAdd.hAdd (α := M) 0 0 = 0
rw₃ rw₄ : Eq.{w + 1} (α := M) 0 0
⊢ ⁅z, x + y⁆ = 0

Tactic:
rw [lie_add, hx, hy, add_zero]

Premises used: add_zero, lie_add
-- Module: Mathlib.Algebra.Lie.Abelian
Goal:
R : Type u
L : Type v
M : Type w
N : 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 : AddCommGroup N
inst_8 : Module R N
inst_9 : LieRingModule L N
inst_10 : LieModule R L N
c : R
x : M
hx : Membership.mem (γ := Set M) {m : M | ∀ (x : L), ⁅x, m⁆ = 0} x
y : L
rw : c • ⁅y, x⁆ = 0
rw₁ : HSMul.hSMul (β := M) c 0 = 0
rw₂ rw₃ : Eq.{w + 1} (α := M) 0 0
⊢ ⁅y, c • x⁆ = 0

Tactic:
rw [lie_smul, hx, smul_zero]

Premises used: lie_smul, smul_zero
-- Module: Mathlib.Algebra.Lie.Abelian
Goal:
R : Type u
L : Type v
M : Type w
N : 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 : AddCommGroup N
inst_8 : Module R N
inst_9 : LieRingModule L N
inst_10 : LieModule R L N
x : L
m : M
hm : Membership.mem (γ := Set M) {m : M | ∀ (x : L), ⁅x, m⁆ = 0} m
y : L
rw : Eq.{w + 1} (α := M) ⁅y, 0⁆ 0
rw₁ rw₂ : Eq.{w + 1} (α := M) 0 0
⊢ ⁅y, ⁅x, m⁆⁆ = 0

Tactic:
rw [hm, lie_zero]

Premises used: lie_zero
-- Module: Mathlib.Algebra.Lie.Abelian
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
⊢ Membership.mem (γ := LieSubmodule R L M) (maxTrivSubmodule R L M) m ↔ ∀ (x : L), ⁅x, m⁆ = 0

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Algebra.Lie.Abelian
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
I : LieIdeal R L
rw :
  ∀ (x : M),
    Membership.mem (γ := Set M) {x : M | ∃ (x_1 : ↥I) (n : ↥(maxTrivSubmodule R L M)), ⁅(↑x_1 : L), (↑n : M)⁆ = x} x →
      x = 0
⊢ Eq (α := LieSubmodule R L M) ⁅I, maxTrivSubmodule R L M⁆ ⊥

Tactic:
rw [← LieSubmodule.toSubmodule_inj, LieSubmodule.lieIdeal_oper_eq_linear_span,
    LieSubmodule.bot_toSubmodule, Submodule.span_eq_bot]

Premises used: LieSubmodule.bot_toSubmodule, Submodule.span_eq_bot, LieSubmodule.toSubmodule_inj, LieSubmodule.lieIdeal_oper_eq_linear_span
-- Module: Mathlib.Algebra.Lie.Abelian
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
I : LieIdeal R L
x : L
hx : x ∈ I
m : M
hm : Membership.mem (γ := LieSubmodule R L M) (maxTrivSubmodule R L M) m
⊢ ⁅(↑(Subtype.mk (p := fun (x : L) ↦ x ∈ I) x hx) : L),
      (↑(Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := LieSubmodule R L M) (maxTrivSubmodule R L M) x) m hm) :
        M)⁆ =
    0

Tactic:
hm x
-- Module: Mathlib.Algebra.Lie.Abelian
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
I : LieIdeal R L
x : L
hx : x ∈ I
m : M
hm : Membership.mem (γ := LieSubmodule R L M) (maxTrivSubmodule R L M) m
⊢ ⁅(↑(Subtype.mk (p := fun (x : L) ↦ x ∈ I) x hx) : L),
      (↑(Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := LieSubmodule R L M) (maxTrivSubmodule R L M) x) m hm) :
        M)⁆ =
    0

Tactic:
exact hm x
-- Module: Mathlib.Algebra.Lie.Abelian
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
N : LieSubmodule R L M
⊢ N ≤ maxTrivSubmodule R L M ↔ Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ N = ⊥

Tactic:
⟨fun h => ?_, fun h m hm => ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Algebra.Lie.Abelian
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
N : LieSubmodule R L M
refine_1 : ∀ (h : N ≤ maxTrivSubmodule R L M), Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ N = ⊥
refine_2 :
  ∀ (h : Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ N = ⊥) (m : M) (hm : m ∈ N),
    Membership.mem (γ := LieSubmodule R L M) (maxTrivSubmodule R L M) m
⊢ N ≤ maxTrivSubmodule R L M ↔ Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ N = ⊥

Tactic:
refine ⟨fun h => ?_, fun h m hm => ?_⟩
-- Module: Mathlib.Algebra.Lie.Abelian
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
N : LieSubmodule R L M
h : N ≤ maxTrivSubmodule R L M
refine_1 :
  Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ N ≤ Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ (maxTrivSubmodule R L M)
⊢ Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ N = ⊥

Tactic:
rw [← le_bot_iff, ← ideal_oper_maxTrivSubmodule_eq_bot R L M ⊤]

Premises used: le_bot_iff, LieModule.ideal_oper_maxTrivSubmodule_eq_bot, Top.top
-- Module: Mathlib.Algebra.Lie.Abelian
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
N : LieSubmodule R L M
h : N ≤ maxTrivSubmodule R L M
⊢ Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ N ≤ Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ (maxTrivSubmodule R L M)

Tactic:
LieSubmodule.mono_lie_right ⊤ h

Premises used: LieSubmodule.mono_lie_right, Top.top
-- Module: Mathlib.Algebra.Lie.Abelian
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
N : LieSubmodule R L M
h : N ≤ maxTrivSubmodule R L M
⊢ Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ N ≤ Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ (maxTrivSubmodule R L M)

Tactic:
exact LieSubmodule.mono_lie_right ⊤ h

Premises used: LieSubmodule.mono_lie_right, Top.top
-- Module: Mathlib.Algebra.Lie.Abelian
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
N : LieSubmodule R L M
h : Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ N = ⊥
m : M
hm : m ∈ N
refine_2 :
  ∀ (h : ∀ (x : L), Membership.mem (γ := LieIdeal R L) ⊤ x → ∀ m ∈ N, ⁅x, m⁆ = 0) (m : M) (hm : m ∈ N) (x : L),
    ⁅x, m⁆ = 0
⊢ ∀ (x : L), ⁅x, m⁆ = 0

Tactic:
rw [LieSubmodule.lie_eq_bot_iff] at h

Premises used: LieSubmodule.lie_eq_bot_iff
-- Module: Mathlib.Algebra.Lie.Abelian
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
N : LieSubmodule R L M
h : ∀ (x : L), Membership.mem (γ := LieIdeal R L) ⊤ x → ∀ m ∈ N, ⁅x, m⁆ = 0
m : M
hm : m ∈ N
⊢ ∀ (x : L), ⁅x, m⁆ = 0

Tactic:
fun x => h x (LieSubmodule.mem_top x) m hm

Premises used: LieSubmodule.mem_top
-- Module: Mathlib.Algebra.Lie.Abelian
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
N : LieSubmodule R L M
h : ∀ (x : L), Membership.mem (γ := LieIdeal R L) ⊤ x → ∀ m ∈ N, ⁅x, m⁆ = 0
m : M
hm : m ∈ N
⊢ ∀ (x : L), ⁅x, m⁆ = 0

Tactic:
exact fun x => h x (LieSubmodule.mem_top x) m hm

Premises used: LieSubmodule.mem_top
-- Module: Mathlib.Algebra.Lie.Abelian
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
N : LieSubmodule R L M
⊢ IsTrivial.{v, w} L ↥N ↔ N ≤ maxTrivSubmodule R L M

Tactic:
⟨fun h m hm x => IsTrivial.casesOn h fun h => Subtype.ext_iff.mp (h x ⟨m, hm⟩), fun h =>
    { trivial := fun x m => Subtype.ext (h m.2 x) }⟩

Premises used: LieModule.IsTrivial.casesOn, LieModule.IsTrivial.mk, Iff.intro, Subtype.property, Subtype.ext
-- Module: Mathlib.Algebra.Lie.Abelian
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
mp : IsTrivial L M → Eq (α := LieSubmodule R L M) (maxTrivSubmodule R L M) ⊤
mpr : Eq (α := LieSubmodule R L M) (maxTrivSubmodule R L M) ⊤ → IsTrivial L M
⊢ IsTrivial L M ↔ Eq (α := LieSubmodule R L M) (maxTrivSubmodule R L M) ⊤

Tactic:
constructor
-- Module: Mathlib.Algebra.Lie.Abelian
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
h : ∀ (x : L) (m : M), ⁅x, m⁆ = 0
mp :
  ∀ (m : M),
    Membership.mem (γ := LieSubmodule R L M) (maxTrivSubmodule R L M) m ↔ Membership.mem (γ := LieSubmodule R L M) ⊤ m
⊢ Eq (α := LieSubmodule R L M) (maxTrivSubmodule R L M) ⊤

Tactic:
ext
-- Module: Mathlib.Algebra.Lie.Abelian
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
h : ∀ (x : L) (m : M), ⁅x, m⁆ = 0
m : M
⊢ Membership.mem (γ := LieSubmodule R L M) (maxTrivSubmodule R L M) m ↔ Membership.mem (γ := LieSubmodule R L M) ⊤ m

Tactic:
simp only [mem_maxTrivSubmodule, h, forall_const, LieSubmodule.mem_top]

Premises used: LieModule.mem_maxTrivSubmodule, LieSubmodule.mem_top, forall_const
-- Module: Mathlib.Algebra.Lie.Abelian
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
h : Eq (α := LieSubmodule R L M) (maxTrivSubmodule R L M) ⊤
mpr : ∀ (x : L) (m : M), ⁅x, m⁆ = 0
⊢ IsTrivial L M

Tactic:
constructor
-- Module: Mathlib.Algebra.Lie.Abelian
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
h : Eq (α := LieSubmodule R L M) (maxTrivSubmodule R L M) ⊤
x : L
m : M
mpr : ∀ (x : L), ⁅x, m⁆ = 0
⊢ ⁅x, m⁆ = 0

Tactic:
revert x
-- Module: Mathlib.Algebra.Lie.Abelian
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
h : Eq (α := LieSubmodule R L M) (maxTrivSubmodule R L M) ⊤
m : M
mpr : Membership.mem (γ := LieSubmodule R L M) ⊤ m
⊢ ∀ (x : L), ⁅x, m⁆ = 0

Tactic:
rw [← mem_maxTrivSubmodule R L M, h]

Premises used: LieModule.mem_maxTrivSubmodule
-- Module: Mathlib.Algebra.Lie.Abelian
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
h : Eq (α := LieSubmodule R L M) (maxTrivSubmodule R L M) ⊤
m : M
⊢ Membership.mem (γ := LieSubmodule R L M) ⊤ m

Tactic:
LieSubmodule.mem_top m

Premises used: LieSubmodule.mem_top
-- Module: Mathlib.Algebra.Lie.Abelian
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
h : Eq (α := LieSubmodule R L M) (maxTrivSubmodule R L M) ⊤
m : M
⊢ Membership.mem (γ := LieSubmodule R L M) ⊤ m

Tactic:
exact LieSubmodule.mem_top m

Premises used: LieSubmodule.mem_top
-- Module: Mathlib.Algebra.Lie.Abelian
Goal:
R : Type u
L : Type v
M : Type w
N : 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 : AddCommGroup N
inst_8 : Module R N
inst_9 : LieRingModule L N
inst_10 : LieModule R L N
f : M →ₗ⁅R,L⁆ N
m n : ↥(maxTrivSubmodule R L M)
a :
  (↑(Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := LieSubmodule R L N) (maxTrivSubmodule R L N) x)
          ((f : (a : M) → N) (↑(m + n) : M)) ⋯) :
      N) =
    (↑(HAdd.hAdd (α := ↥(maxTrivSubmodule R L N)) (β := ↥(maxTrivSubmodule R L N))
          (Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := LieSubmodule R L N) (maxTrivSubmodule R L N) x)
              ((f : (a : M) → N) (↑m : M)) ⋯ :
            ↥(maxTrivSubmodule R L N))
          (Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := LieSubmodule R L N) (maxTrivSubmodule R L N) x)
              ((f : (a : M) → N) (↑n : M)) ⋯ :
            ↥(maxTrivSubmodule R L N))) :
      N)
⊢ Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := LieSubmodule R L N) (maxTrivSubmodule R L N) x)
      ((f : (a : M) → N) (↑(m + n) : M)) ⋯ =
    HAdd.hAdd (α := ↥(maxTrivSubmodule R L N)) (β := ↥(maxTrivSubmodule R L N))
      (Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := LieSubmodule R L N) (maxTrivSubmodule R L N) x)
          ((f : (a : M) → N) (↑m : M)) ⋯ :
        ↥(maxTrivSubmodule R L N))
      (Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := LieSubmodule R L N) (maxTrivSubmodule R L N) x)
          ((f : (a : M) → N) (↑n : M)) ⋯ :
        ↥(maxTrivSubmodule R L N))

Tactic:
ext
-- Module: Mathlib.Algebra.Lie.Abelian
Goal:
R : Type u
L : Type v
M : Type w
N : 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 : AddCommGroup N
inst_8 : Module R N
inst_9 : LieRingModule L N
inst_10 : LieModule R L N
f : M →ₗ⁅R,L⁆ N
m n : ↥(maxTrivSubmodule R L M)
⊢ (↑(Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := LieSubmodule R L N) (maxTrivSubmodule R L N) x)
          ((f : (a : M) → N) (↑(m + n) : M)) ⋯) :
      N) =
    (↑(HAdd.hAdd (α := ↥(maxTrivSubmodule R L N)) (β := ↥(maxTrivSubmodule R L N))
          (Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := LieSubmodule R L N) (maxTrivSubmodule R L N) x)
              ((f : (a : M) → N) (↑m : M)) ⋯ :
            ↥(maxTrivSubmodule R L N))
          (Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := LieSubmodule R L N) (maxTrivSubmodule R L N) x)
              ((f : (a : M) → N) (↑n : M)) ⋯ :
            ↥(maxTrivSubmodule R L N))) :
      N)

Tactic:
simp