awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
k : ℕ
h : IsLieAbelian.{v} ↥(derivedSeriesOfIdeal R L k I) ∧ derivedSeriesOfIdeal R L k I ≠ ⊥
⊢ IsLieAbelian.{v}
    ↥(match (motive := ℕ → LieIdeal R L) k + 1 with
        | 0 => ⊥
        | k.succ => derivedSeriesOfIdeal R L k I :
        LieIdeal R L)

Tactic:
h.1

Premises used: Set.Mem, And.left
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
k : ℕ
h : IsLieAbelian.{v} ↥(derivedSeriesOfIdeal R L k I) ∧ derivedSeriesOfIdeal R L k I ≠ ⊥
⊢ IsLieAbelian.{v}
    ↥(match (motive := ℕ → LieIdeal R L) k + 1 with
        | 0 => ⊥
        | k.succ => derivedSeriesOfIdeal R L k I :
        LieIdeal R L)

Tactic:
exact h.1

Premises used: And.left
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
inst_3 : IsSolvable.{v} ↥I
s : Set ℕ := {k : ℕ | derivedSeriesOfIdeal R L k I = ⊥}
change : sInf s = 0 ↔ I = ⊥
⊢ derivedLengthOfIdeal R L I = 0 ↔ I = ⊥

Tactic:
change sInf s = 0 ↔ _

Premises used: InfSet.sInf
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
inst_3 : IsSolvable.{v} ↥I
s : Set ℕ := {k : ℕ | derivedSeriesOfIdeal R L k I = ⊥}
k : ℕ
hk : Eq.{v + 1} (α := LieIdeal R ↥I) (derivedSeries R (↥I) k) ⊥
rwa : ∀ (hk : Eq.{v + 1} (α := LieIdeal R ↥I) (derivedSeriesOfIdeal R (↥I) k ⊤) ⊥), k ∈ s
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (hk : derivedSeriesOfIdeal R L k I = ⊥), k ∈ s
⊢ k ∈ s

Tactic:
rwa [derivedSeries_def, LieIdeal.derivedSeries_eq_bot_iff] at hk

Premises used: LieAlgebra.derivedSeries_def, LieIdeal.derivedSeries_eq_bot_iff
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
inst_3 : IsSolvable.{v} ↥I
s : Set ℕ := {k : ℕ | derivedSeriesOfIdeal R L k I = ⊥}
⊢ s.Nonempty

Tactic:
have hne : s.Nonempty :=
    have ⟨k, hk⟩ := IsSolvable.solvable R I
    ⟨k, by rwa [derivedSeries_def, LieIdeal.derivedSeries_eq_bot_iff] at hk⟩
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
inst_3 : IsSolvable.{v} ↥I
s : Set ℕ := {k : ℕ | derivedSeriesOfIdeal R L k I = ⊥}
hne : s.Nonempty
⊢ sInf s = 0 ↔ I = ⊥

Tactic:
simp [s, hne.ne_empty]

Premises used: Set.Nonempty.ne_empty
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
h : IsSolvable.{v} ↥I
h_1 : ∀ (x : ℕ), derivedLengthOfIdeal R L I = 0 → (Eq.{v + 1} (α := LieIdeal R L) ⊥ ⊥ ↔ I = ⊥)
h_2 : ∀ (x k : ℕ), derivedLengthOfIdeal R L I = k.succ → (derivedSeriesOfIdeal R L k I = ⊥ ↔ I = ⊥)
⊢ Eq.{v + 1} (α := LieIdeal R L)
      (match (motive := ℕ → LieIdeal R L) derivedLengthOfIdeal R L I with
        | 0 => ⊥
        | k.succ => derivedSeriesOfIdeal R L k I :
        LieIdeal R L)
      (⊥ : LieIdeal R L) ↔
    I = ⊥

Tactic:
split
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
h : IsSolvable.{v} ↥I
x : ℕ
heq : derivedLengthOfIdeal R L I = 0
⊢ Eq.{v + 1} (α := LieIdeal R L) ⊥ ⊥ ↔ I = ⊥

Tactic:
simp_all only [derivedLength_zero]

Premises used: LieAlgebra.derivedLength_zero
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
h_1 : IsSolvable.{v} ↥I
x k : ℕ
h : derivedLengthOfIdeal R L I = k.succ
⊢ IsLieAbelian.{v} ↥(derivedSeriesOfIdeal R L k I)

Tactic:
obtain ⟨_, h₂⟩ := (derivedSeries_of_derivedLength_succ R L I k).mp h

Premises used: LieAlgebra.derivedSeries_of_derivedLength_succ, Iff.mp
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
h_1 : IsSolvable.{v} ↥I
x k : ℕ
h : derivedLengthOfIdeal R L I = k.succ
left : IsLieAbelian.{v} ↥(derivedSeriesOfIdeal R L k I)
⊢ derivedSeriesOfIdeal R L k I ≠ ⊥

Tactic:
obtain ⟨_, h₂⟩ := (derivedSeries_of_derivedLength_succ R L I k).mp h

Premises used: LieAlgebra.derivedSeries_of_derivedLength_succ, Iff.mp
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
x k : ℕ
h_1 : IsSolvable.{v} ↥⊥
h : derivedLengthOfIdeal R L ⊥ = k.succ
left : IsLieAbelian.{v} ↥(derivedSeriesOfIdeal R L k ⊥)
h₂ : Ne (α := LieIdeal R L) (derivedSeriesOfIdeal R L k ⊥) ⊥
apply : Eq (α := LieIdeal R L) (derivedSeriesOfIdeal R L k ⊥) ⊥
⊢ False

Tactic:
apply h₂
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
x k : ℕ
h_1 : IsSolvable.{v} ↥⊥
h : derivedLengthOfIdeal R L ⊥ = k.succ
left : IsLieAbelian.{v} ↥(derivedSeriesOfIdeal R L k ⊥)
h₂ : Ne (α := LieIdeal R L) (derivedSeriesOfIdeal R L k ⊥) ⊥
⊢ Eq (α := LieIdeal R L) (derivedSeriesOfIdeal R L k ⊥) ⊥

Tactic:
apply derivedSeries_of_bot_eq_bot

Premises used: LieAlgebra.derivedSeries_of_bot_eq_bot
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
h_1 : IsSolvable.{v} ↥I
x k : ℕ
h : derivedLengthOfIdeal R L I = k.succ
left : IsLieAbelian.{v} ↥(derivedSeriesOfIdeal R L k I)
h₂ : derivedSeriesOfIdeal R L k I ≠ ⊥
⊢ I ≠ ⊥

Tactic:
have h₃ : I ≠ ⊥ := by rintro rfl; apply h₂; apply derivedSeries_of_bot_eq_bot
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
h_1 : IsSolvable.{v} ↥I
x k : ℕ
h : derivedLengthOfIdeal R L I = k.succ
left : IsLieAbelian.{v} ↥(derivedSeriesOfIdeal R L k I)
h₂ : derivedSeriesOfIdeal R L k I ≠ ⊥
h₃ : I ≠ ⊥
⊢ derivedSeriesOfIdeal R L k I = ⊥ ↔ I = ⊥

Tactic:
simp only [h₂, h₃]
-- Module: Mathlib.Algebra.Lie.Subalgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
x y : L
hx :
  Membership.mem (γ := Set L)
    (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (Submodule.toAddSubmonoid.{u, v} (R := R) 0))) x
_hy :
  Membership.mem (γ := Set L)
    (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (Submodule.toAddSubmonoid.{u, v} (R := R) 0))) y
rw :
  Membership.mem (γ := Set L)
    (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (Submodule.toAddSubmonoid.{u, v} (R := R) 0))) 0
⊢ Membership.mem (γ := Set L)
    (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (Submodule.toAddSubmonoid.{u, v} (R := R) 0))) ⁅x, y⁆

Tactic:
rw [(Submodule.mem_bot R).1 hx, zero_lie]

Premises used: Submodule.mem_bot, zero_lie, Iff.mp
-- Module: Mathlib.Algebra.Lie.Subalgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
x y : L
hx :
  Membership.mem (γ := Set L)
    (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (Submodule.toAddSubmonoid.{u, v} (R := R) 0))) x
_hy :
  Membership.mem (γ := Set L)
    (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (Submodule.toAddSubmonoid.{u, v} (R := R) 0))) y
⊢ Membership.mem (γ := Set L)
    (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (Submodule.toAddSubmonoid.{u, v} (R := R) 0))) 0

Tactic:
Submodule.zero_mem 0

Premises used: Set.Mem, Submodule.zero_mem, OfNat.ofNat
-- Module: Mathlib.Algebra.Lie.Subalgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
x y : L
hx :
  Membership.mem (γ := Set L)
    (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (Submodule.toAddSubmonoid.{u, v} (R := R) 0))) x
_hy :
  Membership.mem (γ := Set L)
    (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (Submodule.toAddSubmonoid.{u, v} (R := R) 0))) y
⊢ Membership.mem (γ := Set L)
    (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (Submodule.toAddSubmonoid.{u, v} (R := R) 0))) 0

Tactic:
exact Submodule.zero_mem 0

Premises used: Submodule.zero_mem, OfNat.ofNat
-- Module: Mathlib.Algebra.Lie.Subalgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
L' L'' : LieSubalgebra R L
h :
  Eq.{v + 1} (α := Set L) ((fun (L' : LieSubalgebra R L) ↦ L'.carrier) L')
    ((fun (L' : LieSubalgebra R L) ↦ L'.carrier) L'')
rcases :
  ∀ (toAddSubmonoid : AddSubmonoid L)
    (smul_mem' : ∀ (c : R) {x : L}, x ∈ toAddSubmonoid.carrier → c • x ∈ toAddSubmonoid.carrier)
    (lie_mem' :
      ∀ {x y : L},
        x ∈ { toAddSubmonoid := toAddSubmonoid, smul_mem' := smul_mem' : Submodule R L }.carrier →
          y ∈ { toAddSubmonoid := toAddSubmonoid, smul_mem' := smul_mem' : Submodule R L }.carrier →
            ⁅x, y⁆ ∈ { toAddSubmonoid := toAddSubmonoid, smul_mem' := smul_mem' : Submodule R L }.carrier)
    (h :
      Eq.{v + 1} (α := Set L)
        ((fun (L' : LieSubalgebra R L) ↦ L'.carrier)
          { toAddSubmonoid := toAddSubmonoid, smul_mem' := smul_mem', lie_mem' := @lie_mem' })
        ((fun (L' : LieSubalgebra R L) ↦ L'.carrier) L'')),
    { toAddSubmonoid := toAddSubmonoid, smul_mem' := smul_mem', lie_mem' := @lie_mem' : LieSubalgebra R L } = L''
⊢ L' = L''

Tactic:
rcases L' with ⟨⟨⟩⟩
-- Module: Mathlib.Algebra.Lie.Subalgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
L'' : LieSubalgebra R L
toAddSubmonoid : AddSubmonoid L
smul_mem' : ∀ (c : R) {x : L}, x ∈ toAddSubmonoid.carrier → c • x ∈ toAddSubmonoid.carrier
lie_mem' :
  ∀ {x y : L},
    x ∈ { toAddSubmonoid := toAddSubmonoid, smul_mem' := smul_mem' : Submodule R L }.carrier →
      y ∈ { toAddSubmonoid := toAddSubmonoid, smul_mem' := smul_mem' : Submodule R L }.carrier →
        ⁅x, y⁆ ∈ { toAddSubmonoid := toAddSubmonoid, smul_mem' := smul_mem' : Submodule R L }.carrier
h :
  Eq.{v + 1} (α := Set L)
    ((fun (L' : LieSubalgebra R L) ↦ L'.carrier)
      { toAddSubmonoid := toAddSubmonoid, smul_mem' := smul_mem', lie_mem' := @lie_mem' })
    ((fun (L' : LieSubalgebra R L) ↦ L'.carrier) L'')
rcases :
  ∀ (toAddSubmonoid_1 : AddSubmonoid L)
    (smul_mem'_1 : ∀ (c : R) {x : L}, x ∈ toAddSubmonoid_1.carrier → c • x ∈ toAddSubmonoid_1.carrier)
    (lie_mem'_1 :
      ∀ {x y : L},
        x ∈ { toAddSubmonoid := toAddSubmonoid_1, smul_mem' := smul_mem'_1 : Submodule R L }.carrier →
          y ∈ { toAddSubmonoid := toAddSubmonoid_1, smul_mem' := smul_mem'_1 : Submodule R L }.carrier →
            ⁅x, y⁆ ∈ { toAddSubmonoid := toAddSubmonoid_1, smul_mem' := smul_mem'_1 : Submodule R L }.carrier)
    (h :
      Eq.{v + 1} (α := Set L)
        ((fun (L' : LieSubalgebra R L) ↦ L'.carrier)
          { toAddSubmonoid := toAddSubmonoid, smul_mem' := smul_mem', lie_mem' := @lie_mem' })
        ((fun (L' : LieSubalgebra R L) ↦ L'.carrier)
          { toAddSubmonoid := toAddSubmonoid_1, smul_mem' := smul_mem'_1, lie_mem' := @lie_mem'_1 })),
    { toAddSubmonoid := toAddSubmonoid, smul_mem' := smul_mem', lie_mem' := @lie_mem' : LieSubalgebra R L } =
      { toAddSubmonoid := toAddSubmonoid_1, smul_mem' := smul_mem'_1, lie_mem' := @lie_mem'_1 }
⊢ { toAddSubmonoid := toAddSubmonoid, smul_mem' := smul_mem', lie_mem' := @lie_mem' : LieSubalgebra R L } = L''

Tactic:
rcases L'' with ⟨⟨⟩⟩
-- Module: Mathlib.Algebra.Lie.Subalgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
toAddSubmonoid : AddSubmonoid L
smul_mem' : ∀ (c : R) {x : L}, x ∈ toAddSubmonoid.carrier → c • x ∈ toAddSubmonoid.carrier
lie_mem' :
  ∀ {x y : L},
    x ∈ { toAddSubmonoid := toAddSubmonoid, smul_mem' := smul_mem' : Submodule R L }.carrier →
      y ∈ { toAddSubmonoid := toAddSubmonoid, smul_mem' := smul_mem' : Submodule R L }.carrier →
        ⁅x, y⁆ ∈ { toAddSubmonoid := toAddSubmonoid, smul_mem' := smul_mem' : Submodule R L }.carrier
toAddSubmonoid_1 : AddSubmonoid L
smul_mem'_1 : ∀ (c : R) {x : L}, x ∈ toAddSubmonoid_1.carrier → c • x ∈ toAddSubmonoid_1.carrier
lie_mem'_1 :
  ∀ {x y : L},
    x ∈ { toAddSubmonoid := toAddSubmonoid_1, smul_mem' := smul_mem'_1 : Submodule R L }.carrier →
      y ∈ { toAddSubmonoid := toAddSubmonoid_1, smul_mem' := smul_mem'_1 : Submodule R L }.carrier →
        ⁅x, y⁆ ∈ { toAddSubmonoid := toAddSubmonoid_1, smul_mem' := smul_mem'_1 : Submodule R L }.carrier
h :
  Eq.{v + 1} (α := Set L)
    ((fun (L' : LieSubalgebra R L) ↦ L'.carrier)
      { toAddSubmonoid := toAddSubmonoid, smul_mem' := smul_mem', lie_mem' := @lie_mem' })
    ((fun (L' : LieSubalgebra R L) ↦ L'.carrier)
      { toAddSubmonoid := toAddSubmonoid_1, smul_mem' := smul_mem'_1, lie_mem' := @lie_mem'_1 })
e_toSubmodule : toAddSubmonoid = toAddSubmonoid_1
⊢ { toAddSubmonoid := toAddSubmonoid, smul_mem' := smul_mem', lie_mem' := @lie_mem' : LieSubalgebra R L } =
    { toAddSubmonoid := toAddSubmonoid_1, smul_mem' := smul_mem'_1, lie_mem' := @lie_mem'_1 }

Tactic:
congr
-- Module: Mathlib.Algebra.Lie.Subalgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
toAddSubmonoid : AddSubmonoid L
smul_mem' : ∀ (c : R) {x : L}, x ∈ toAddSubmonoid.carrier → c • x ∈ toAddSubmonoid.carrier
lie_mem' :
  ∀ {x y : L},
    x ∈ { toAddSubmonoid := toAddSubmonoid, smul_mem' := smul_mem' : Submodule R L }.carrier →
      y ∈ { toAddSubmonoid := toAddSubmonoid, smul_mem' := smul_mem' : Submodule R L }.carrier →
        ⁅x, y⁆ ∈ { toAddSubmonoid := toAddSubmonoid, smul_mem' := smul_mem' : Submodule R L }.carrier
toAddSubmonoid_1 : AddSubmonoid L
smul_mem'_1 : ∀ (c : R) {x : L}, x ∈ toAddSubmonoid_1.carrier → c • x ∈ toAddSubmonoid_1.carrier
lie_mem'_1 :
  ∀ {x y : L},
    x ∈ { toAddSubmonoid := toAddSubmonoid_1, smul_mem' := smul_mem'_1 : Submodule R L }.carrier →
      y ∈ { toAddSubmonoid := toAddSubmonoid_1, smul_mem' := smul_mem'_1 : Submodule R L }.carrier →
        ⁅x, y⁆ ∈ { toAddSubmonoid := toAddSubmonoid_1, smul_mem' := smul_mem'_1 : Submodule R L }.carrier
h :
  Eq.{v + 1} (α := Set L)
    ((fun (L' : LieSubalgebra R L) ↦ L'.carrier)
      { toAddSubmonoid := toAddSubmonoid, smul_mem' := smul_mem', lie_mem' := @lie_mem' })
    ((fun (L' : LieSubalgebra R L) ↦ L'.carrier)
      { toAddSubmonoid := toAddSubmonoid_1, smul_mem' := smul_mem'_1, lie_mem' := @lie_mem'_1 })
⊢ toAddSubmonoid = toAddSubmonoid_1

Tactic:
SetLike.coe_injective' h

Premises used: SetLike.coe_injective'
-- Module: Mathlib.Algebra.Lie.Subalgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
toAddSubmonoid : AddSubmonoid L
smul_mem' : ∀ (c : R) {x : L}, x ∈ toAddSubmonoid.carrier → c • x ∈ toAddSubmonoid.carrier
lie_mem' :
  ∀ {x y : L},
    x ∈ { toAddSubmonoid := toAddSubmonoid, smul_mem' := smul_mem' : Submodule R L }.carrier →
      y ∈ { toAddSubmonoid := toAddSubmonoid, smul_mem' := smul_mem' : Submodule R L }.carrier →
        ⁅x, y⁆ ∈ { toAddSubmonoid := toAddSubmonoid, smul_mem' := smul_mem' : Submodule R L }.carrier
toAddSubmonoid_1 : AddSubmonoid L
smul_mem'_1 : ∀ (c : R) {x : L}, x ∈ toAddSubmonoid_1.carrier → c • x ∈ toAddSubmonoid_1.carrier
lie_mem'_1 :
  ∀ {x y : L},
    x ∈ { toAddSubmonoid := toAddSubmonoid_1, smul_mem' := smul_mem'_1 : Submodule R L }.carrier →
      y ∈ { toAddSubmonoid := toAddSubmonoid_1, smul_mem' := smul_mem'_1 : Submodule R L }.carrier →
        ⁅x, y⁆ ∈ { toAddSubmonoid := toAddSubmonoid_1, smul_mem' := smul_mem'_1 : Submodule R L }.carrier
h :
  Eq.{v + 1} (α := Set L)
    ((fun (L' : LieSubalgebra R L) ↦ L'.carrier)
      { toAddSubmonoid := toAddSubmonoid, smul_mem' := smul_mem', lie_mem' := @lie_mem' })
    ((fun (L' : LieSubalgebra R L) ↦ L'.carrier)
      { toAddSubmonoid := toAddSubmonoid_1, smul_mem' := smul_mem'_1, lie_mem' := @lie_mem'_1 })
⊢ toAddSubmonoid = toAddSubmonoid_1

Tactic:
exact SetLike.coe_injective' h

Premises used: SetLike.coe_injective'
-- Module: Mathlib.Algebra.Lie.Subalgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
L' : LieSubalgebra R L
x y z : ↥L'
a :
  (↑(Subtype.mk (p := fun (x : L) ↦ x ∈ L') ⁅(↑(x + y) : L), (↑z : L)⁆ ⋯) : L) =
    (↑(Subtype.mk (p := fun (x : L) ↦ x ∈ L') ⁅(↑x : L), (↑z : L)⁆ ⋯ +
          Subtype.mk (p := fun (x : L) ↦ x ∈ L') ⁅(↑y : L), (↑z : L)⁆ ⋯) :
      L)
⊢ Subtype.mk (p := fun (x : L) ↦ x ∈ L') ⁅(↑(x + y) : L), (↑z : L)⁆ ⋯ =
    Subtype.mk (p := fun (x : L) ↦ x ∈ L') ⁅(↑x : L), (↑z : L)⁆ ⋯ +
      Subtype.mk (p := fun (x : L) ↦ x ∈ L') ⁅(↑y : L), (↑z : L)⁆ ⋯

Tactic:
apply SetCoe.ext

Premises used: SetCoe.ext
-- Module: Mathlib.Algebra.Lie.Subalgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
L' : LieSubalgebra R L
x y z : ↥L'
⊢ (↑(Subtype.mk (p := fun (x : L) ↦ x ∈ L') ⁅(↑(x + y) : L), (↑z : L)⁆ ⋯) : L) =
    (↑(Subtype.mk (p := fun (x : L) ↦ x ∈ L') ⁅(↑x : L), (↑z : L)⁆ ⋯ +
          Subtype.mk (p := fun (x : L) ↦ x ∈ L') ⁅(↑y : L), (↑z : L)⁆ ⋯) :
      L)

Tactic:
apply add_lie

Premises used: add_lie
-- Module: Mathlib.Algebra.Lie.Subalgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
L' : LieSubalgebra R L
x y z : ↥L'
a :
  (↑(Subtype.mk (p := fun (x : L) ↦ x ∈ L') ⁅(↑x : L), (↑(y + z) : L)⁆ ⋯) : L) =
    (↑(Subtype.mk (p := fun (x : L) ↦ x ∈ L') ⁅(↑x : L), (↑y : L)⁆ ⋯ +
          Subtype.mk (p := fun (x : L) ↦ x ∈ L') ⁅(↑x : L), (↑z : L)⁆ ⋯) :
      L)
⊢ Subtype.mk (p := fun (x : L) ↦ x ∈ L') ⁅(↑x : L), (↑(y + z) : L)⁆ ⋯ =
    Subtype.mk (p := fun (x : L) ↦ x ∈ L') ⁅(↑x : L), (↑y : L)⁆ ⋯ +
      Subtype.mk (p := fun (x : L) ↦ x ∈ L') ⁅(↑x : L), (↑z : L)⁆ ⋯

Tactic:
apply SetCoe.ext

Premises used: SetCoe.ext
-- Module: Mathlib.Algebra.Lie.Subalgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
L' : LieSubalgebra R L
x y z : ↥L'
⊢ (↑(Subtype.mk (p := fun (x : L) ↦ x ∈ L') ⁅(↑x : L), (↑(y + z) : L)⁆ ⋯) : L) =
    (↑(Subtype.mk (p := fun (x : L) ↦ x ∈ L') ⁅(↑x : L), (↑y : L)⁆ ⋯ +
          Subtype.mk (p := fun (x : L) ↦ x ∈ L') ⁅(↑x : L), (↑z : L)⁆ ⋯) :
      L)

Tactic:
apply lie_add

Premises used: lie_add
-- Module: Mathlib.Algebra.Lie.Subalgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
L' : LieSubalgebra R L
x : ↥L'
a : (↑(Subtype.mk (p := fun (x : L) ↦ x ∈ L') ⁅(↑x : L), (↑x : L)⁆ ⋯) : L) = (↑0 : L)
⊢ Subtype.mk (p := fun (x : L) ↦ x ∈ L') ⁅(↑x : L), (↑x : L)⁆ ⋯ = 0

Tactic:
apply SetCoe.ext

Premises used: SetCoe.ext
-- Module: Mathlib.Algebra.Lie.Subalgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
L' : LieSubalgebra R L
x : ↥L'
⊢ (↑(Subtype.mk (p := fun (x : L) ↦ x ∈ L') ⁅(↑x : L), (↑x : L)⁆ ⋯) : L) = (↑0 : L)

Tactic:
apply lie_self

Premises used: lie_self
-- Module: Mathlib.Algebra.Lie.Subalgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
L' : LieSubalgebra R L
x y z : ↥L'
a :
  (↑(Subtype.mk (p := fun (x : L) ↦ x ∈ L')
          ⁅(↑x : L), (↑(Subtype.mk (p := fun (x : L) ↦ x ∈ L') ⁅(↑y : L), (↑z : L)⁆ ⋯) : L)⁆ ⋯) :
      L) =
    (↑(Subtype.mk (p := fun (x : L) ↦ x ∈ L')
            ⁅(↑(Subtype.mk (p := fun (x : L) ↦ x ∈ L') ⁅(↑x : L), (↑y : L)⁆ ⋯) : L), (↑z : L)⁆ ⋯ +
          Subtype.mk (p := fun (x : L) ↦ x ∈ L')
            ⁅(↑y : L), (↑(Subtype.mk (p := fun (x : L) ↦ x ∈ L') ⁅(↑x : L), (↑z : L)⁆ ⋯) : L)⁆ ⋯) :
      L)
⊢ Subtype.mk (p := fun (x : L) ↦ x ∈ L')
      ⁅(↑x : L), (↑(Subtype.mk (p := fun (x : L) ↦ x ∈ L') ⁅(↑y : L), (↑z : L)⁆ ⋯) : L)⁆ ⋯ =
    Subtype.mk (p := fun (x : L) ↦ x ∈ L')
        ⁅(↑(Subtype.mk (p := fun (x : L) ↦ x ∈ L') ⁅(↑x : L), (↑y : L)⁆ ⋯) : L), (↑z : L)⁆ ⋯ +
      Subtype.mk (p := fun (x : L) ↦ x ∈ L')
        ⁅(↑y : L), (↑(Subtype.mk (p := fun (x : L) ↦ x ∈ L') ⁅(↑x : L), (↑z : L)⁆ ⋯) : L)⁆ ⋯

Tactic:
apply SetCoe.ext

Premises used: SetCoe.ext
-- Module: Mathlib.Algebra.Lie.Subalgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
L' : LieSubalgebra R L
x y z : ↥L'
⊢ (↑(Subtype.mk (p := fun (x : L) ↦ x ∈ L')
          ⁅(↑x : L), (↑(Subtype.mk (p := fun (x : L) ↦ x ∈ L') ⁅(↑y : L), (↑z : L)⁆ ⋯) : L)⁆ ⋯) :
      L) =
    (↑(Subtype.mk (p := fun (x : L) ↦ x ∈ L')
            ⁅(↑(Subtype.mk (p := fun (x : L) ↦ x ∈ L') ⁅(↑x : L), (↑y : L)⁆ ⋯) : L), (↑z : L)⁆ ⋯ +
          Subtype.mk (p := fun (x : L) ↦ x ∈ L')
            ⁅(↑y : L), (↑(Subtype.mk (p := fun (x : L) ↦ x ∈ L') ⁅(↑x : L), (↑z : L)⁆ ⋯) : L)⁆ ⋯) :
      L)

Tactic:
apply leibniz_lie

Premises used: leibniz_lie
-- Module: Mathlib.Algebra.Lie.Subalgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
R₁ : Type u_1
inst_3 : Semiring R₁
inst_4 : SMul R₁ R
inst_5 : SMul.{u_1, u} R₁ᵐᵒᵖ R
inst_6 : Module R₁ L
inst_7 : Module.{u_1, v} R₁ᵐᵒᵖ L
inst_8 : IsScalarTower R₁ R L
inst_9 : IsScalarTower.{u_1, u, v} R₁ᵐᵒᵖ R L
inst_10 : IsCentralScalar R₁ L
L' : LieSubalgebra R L
⊢ IsCentralScalar.{u_1, v} R₁ ↥L'

Tactic:
L'.toSubmodule.isCentralScalar

Premises used: Set.Mem, Submodule.isCentralScalar, LieSubalgebra.toSubmodule
-- Module: Mathlib.Algebra.Lie.Subalgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
R₁ : Type u_1
inst_3 : Semiring R₁
inst_4 : SMul R₁ R
inst_5 : Module R₁ L
inst_6 : IsScalarTower R₁ R L
L' : LieSubalgebra R L
⊢ IsScalarTower.{u_1, u, v} R₁ R ↥L'

Tactic:
L'.toSubmodule.isScalarTower

Premises used: Submodule.isScalarTower, Set.Mem, LieSubalgebra.toSubmodule
-- Module: Mathlib.Algebra.Lie.Subalgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
R₁ : Type u_1
inst_3 : Semiring R₁
L' : LieSubalgebra R L
inst_4 : IsNoetherian R L
⊢ IsNoetherian.{u, v} R ↥L'

Tactic:
isNoetherian_submodule' _

Premises used: Set.Mem, isNoetherian_submodule'
-- Module: Mathlib.Algebra.Lie.Subalgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
R₁ : Type u_1
inst_3 : Semiring R₁
L' : LieSubalgebra R L
inst_4 : IsArtinian R L
⊢ IsArtinian.{u, v} R ↥L'

Tactic:
isArtinian_submodule' _

Premises used: Set.Mem, isArtinian_submodule'
-- Module: Mathlib.Algebra.Lie.Subalgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
L' : LieSubalgebra R L
t : R
x y : ↥L'
a : (↑⁅x, t • y⁆ : L) = (↑(t • ⁅x, y⁆) : L)
⊢ ⁅x, t • y⁆ = t • ⁅x, y⁆

Tactic:
apply SetCoe.ext

Premises used: SetCoe.ext
-- Module: Mathlib.Algebra.Lie.Subalgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
L' : LieSubalgebra R L
t : R
x y : ↥L'
⊢ (↑⁅x, t • y⁆ : L) = (↑(t • ⁅x, y⁆) : L)

Tactic:
apply lie_smul

Premises used: lie_smul
-- Module: Mathlib.Algebra.Lie.Subalgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
L' : LieSubalgebra R L
apply : ∀ (t : R) (x y : ↥L'), ⁅x, t • y⁆ = t • ⁅x, y⁆
a : ∀ (t : R) (x y : ↥L'), (↑⁅x, t • y⁆ : L) = (↑(t • ⁅x, y⁆) : L)
⊢ ∀ (t : R) (x y : ↥L'), ⁅x, t • y⁆ = t • ⁅x, y⁆

Tactic:
{ intros
      apply SetCoe.ext
      apply lie_smul }

Premises used: SetCoe.ext, lie_smul
-- Module: Mathlib.Algebra.Lie.Subalgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
L' : LieSubalgebra R L
⊢ 0 ∈ L'

Tactic:
zero_mem L'

Premises used: Set.Mem, ZeroMemClass.zero_mem
-- Module: Mathlib.Algebra.Lie.Subalgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
L' : LieSubalgebra R L
x y : L
⊢ x ∈ L' → y ∈ L' → x + y ∈ L'

Tactic:
add_mem

Premises used: AddMemClass.add_mem
-- Module: Mathlib.Algebra.Lie.Subalgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
L' : LieSubalgebra R L
x y : L
⊢ x ∈ L' → y ∈ L' → x - y ∈ L'

Tactic:
sub_mem

Premises used: sub_mem
-- Module: Mathlib.Algebra.Lie.Subalgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
L' : LieSubalgebra R L
t : R
x : L
h : x ∈ L'
⊢ t • x ∈ L'

Tactic:
SMulMemClass.smul_mem _ h

Premises used: SMulMemClass.smul_mem