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
k : ℕ
ih :
  (↑(↑(derivedSeriesOfIdeal R L k ⊤) : Submodule R L) : Set L) =
    (↑(↑(derivedSeriesOfIdeal ℤ L k ⊤) : Submodule ℤ L) : Set L)
succ :
  (↑(Submodule.span R
          {x : L |
            ∃ (x_1 : L),
              Membership.mem (γ := LieIdeal R L) (derivedSeriesOfIdeal R L k ⊤) x_1 ∧
                ∃ (n : L), Membership.mem (γ := LieSubmodule R L L) (derivedSeriesOfIdeal R L k ⊤) n ∧ ⁅x_1, n⁆ = x}) :
      Set L) =
    (↑(Submodule.span ℤ
          {x : L |
            ∃ (x_1 : L),
              Membership.mem (γ := LieIdeal ℤ L) (derivedSeriesOfIdeal ℤ L k ⊤) x_1 ∧
                ∃ (n : L), Membership.mem (γ := LieSubmodule ℤ L L) (derivedSeriesOfIdeal ℤ L k ⊤) n ∧ ⁅x_1, n⁆ = x}) :
      Set L)
⊢ (↑(↑(Bracket.bracket (L := LieIdeal R L) (derivedSeriesOfIdeal R L k ⊤) (derivedSeriesOfIdeal R L k ⊤)) :
          Submodule R L) :
      Set L) =
    (↑(↑(Bracket.bracket (L := LieIdeal ℤ L) (derivedSeriesOfIdeal ℤ L k ⊤) (derivedSeriesOfIdeal ℤ L k ⊤)) :
          Submodule ℤ L) :
      Set L)

Tactic:
rw [LieSubmodule.lieIdeal_oper_eq_linear_span', LieSubmodule.lieIdeal_oper_eq_linear_span']

Premises used: LieSubmodule.lieIdeal_oper_eq_linear_span'
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
k : ℕ
ih :
  (↑(↑(derivedSeriesOfIdeal R L k ⊤) : Submodule R L) : Set L) =
    (↑(↑(derivedSeriesOfIdeal ℤ L k ⊤) : Submodule ℤ L) : Set L)
⊢ ∀ (x : L),
    x ∈ (↑(↑(derivedSeriesOfIdeal R L k ⊤) : Submodule R L) : Set L) ↔
      x ∈ (↑(↑(derivedSeriesOfIdeal ℤ L k ⊤) : Submodule ℤ L) : Set L)

Tactic:
rw [Set.ext_iff] at ih

Premises used: Set.ext_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
k : ℕ
ih :
  ∀ (x : L),
    x ∈ (↑(↑(derivedSeriesOfIdeal R L k ⊤) : Submodule R L) : Set L) ↔
      x ∈ (↑(↑(derivedSeriesOfIdeal ℤ L k ⊤) : Submodule ℤ L) : Set L)
⊢ ∀ (x : L),
    Membership.mem (γ := LieSubmodule R L L) (derivedSeriesOfIdeal R L k ⊤) x ↔
      Membership.mem (γ := LieSubmodule ℤ L L) (derivedSeriesOfIdeal ℤ L k ⊤) x

Tactic:
simp only [SetLike.mem_coe, LieSubmodule.mem_toSubmodule] at ih

Premises used: LieSubmodule.mem_toSubmodule, SetLike.mem_coe
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
k : ℕ
ih :
  ∀ (x : L),
    Membership.mem (γ := LieSubmodule R L L) (derivedSeriesOfIdeal R L k ⊤) x ↔
      Membership.mem (γ := LieSubmodule ℤ L L) (derivedSeriesOfIdeal ℤ L k ⊤) x
succ :
  (↑(Submodule.span R
          {x : L |
            ∃ (x_1 : L),
              Membership.mem (γ := LieSubmodule ℤ L L) (derivedSeriesOfIdeal ℤ L k ⊤) x_1 ∧
                ∃ (n : L), Membership.mem (γ := LieSubmodule ℤ L L) (derivedSeriesOfIdeal ℤ L k ⊤) n ∧ ⁅x_1, n⁆ = x}) :
      Set L) =
    (↑(Submodule.span ℤ
          {x : L |
            ∃ (x_1 : L),
              Membership.mem (γ := LieIdeal ℤ L) (derivedSeriesOfIdeal ℤ L k ⊤) x_1 ∧
                ∃ (n : L), Membership.mem (γ := LieSubmodule ℤ L L) (derivedSeriesOfIdeal ℤ L k ⊤) n ∧ ⁅x_1, n⁆ = x}) :
      Set L)
⊢ (↑(Submodule.span R
          {x : L |
            ∃ (x_1 : L),
              Membership.mem (γ := LieIdeal R L) (derivedSeriesOfIdeal R L k ⊤) x_1 ∧
                ∃ (n : L), Membership.mem (γ := LieSubmodule R L L) (derivedSeriesOfIdeal R L k ⊤) n ∧ ⁅x_1, n⁆ = x}) :
      Set L) =
    (↑(Submodule.span ℤ
          {x : L |
            ∃ (x_1 : L),
              Membership.mem (γ := LieIdeal ℤ L) (derivedSeriesOfIdeal ℤ L k ⊤) x_1 ∧
                ∃ (n : L), Membership.mem (γ := LieSubmodule ℤ L L) (derivedSeriesOfIdeal ℤ L k ⊤) n ∧ ⁅x_1, n⁆ = x}) :
      Set L)

Tactic:
simp only [ih]
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
k : ℕ
ih :
  ∀ (x : L),
    Membership.mem (γ := LieSubmodule R L L) (derivedSeriesOfIdeal R L k ⊤) x ↔
      Membership.mem (γ := LieSubmodule ℤ L L) (derivedSeriesOfIdeal ℤ L k ⊤) x
succ :
  (↑(Submodule.span R
          {x : L |
            ∃ (x_1 : L),
              Membership.mem (γ := LieSubmodule ℤ L L) (derivedSeriesOfIdeal ℤ L k ⊤) x_1 ∧
                ∃ (n : L), Membership.mem (γ := LieSubmodule ℤ L L) (derivedSeriesOfIdeal ℤ L k ⊤) n ∧ ⁅x_1, n⁆ = x}) :
      Set L) ≤
    (↑(Submodule.span ℤ
          {x : L |
            ∃ (x_1 : L),
              Membership.mem (γ := LieIdeal ℤ L) (derivedSeriesOfIdeal ℤ L k ⊤) x_1 ∧
                ∃ (n : L), Membership.mem (γ := LieSubmodule ℤ L L) (derivedSeriesOfIdeal ℤ L k ⊤) n ∧ ⁅x_1, n⁆ = x}) :
      Set L)
succ₁ :
  (↑(Submodule.span ℤ
          {x : L |
            ∃ (x_1 : L),
              Membership.mem (γ := LieIdeal ℤ L) (derivedSeriesOfIdeal ℤ L k ⊤) x_1 ∧
                ∃ (n : L), Membership.mem (γ := LieSubmodule ℤ L L) (derivedSeriesOfIdeal ℤ L k ⊤) n ∧ ⁅x_1, n⁆ = x}) :
      Set L) ≤
    (↑(Submodule.span R
          {x : L |
            ∃ (x_1 : L),
              Membership.mem (γ := LieSubmodule ℤ L L) (derivedSeriesOfIdeal ℤ L k ⊤) x_1 ∧
                ∃ (n : L), Membership.mem (γ := LieSubmodule ℤ L L) (derivedSeriesOfIdeal ℤ L k ⊤) n ∧ ⁅x_1, n⁆ = x}) :
      Set L)
⊢ (↑(Submodule.span R
          {x : L |
            ∃ (x_1 : L),
              Membership.mem (γ := LieSubmodule ℤ L L) (derivedSeriesOfIdeal ℤ L k ⊤) x_1 ∧
                ∃ (n : L), Membership.mem (γ := LieSubmodule ℤ L L) (derivedSeriesOfIdeal ℤ L k ⊤) n ∧ ⁅x_1, n⁆ = x}) :
      Set L) =
    (↑(Submodule.span ℤ
          {x : L |
            ∃ (x_1 : L),
              Membership.mem (γ := LieIdeal ℤ L) (derivedSeriesOfIdeal ℤ L k ⊤) x_1 ∧
                ∃ (n : L), Membership.mem (γ := LieSubmodule ℤ L L) (derivedSeriesOfIdeal ℤ L k ⊤) n ∧ ⁅x_1, n⁆ = x}) :
      Set L)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
k : ℕ
ih :
  ∀ (x : L),
    Membership.mem (γ := LieSubmodule R L L) (derivedSeriesOfIdeal R L k ⊤) x ↔
      Membership.mem (γ := LieSubmodule ℤ L L) (derivedSeriesOfIdeal ℤ L k ⊤) x
⊢ (↑(Submodule.span R
          {x : L |
            ∃ (x_1 : L),
              Membership.mem (γ := LieSubmodule ℤ L L) (derivedSeriesOfIdeal ℤ L k ⊤) x_1 ∧
                ∃ (n : L), Membership.mem (γ := LieSubmodule ℤ L L) (derivedSeriesOfIdeal ℤ L k ⊤) n ∧ ⁅x_1, n⁆ = x}) :
      Set L) ≤
    (↑(Submodule.span ℤ
          {x : L |
            ∃ (x_1 : L),
              Membership.mem (γ := LieIdeal ℤ L) (derivedSeriesOfIdeal ℤ L k ⊤) x_1 ∧
                ∃ (n : L), Membership.mem (γ := LieSubmodule ℤ L L) (derivedSeriesOfIdeal ℤ L k ⊤) n ∧ ⁅x_1, n⁆ = x}) :
      Set L)

Tactic:
coe_derivedSeries_eq_int_aux _ _ L k ih

Premises used: Set.Mem, setOf, _private.0.LieIdeal.coe_derivedSeries_eq_int_aux
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
k : ℕ
ih :
  ∀ (x : L),
    Membership.mem (γ := LieSubmodule R L L) (derivedSeriesOfIdeal R L k ⊤) x ↔
      Membership.mem (γ := LieSubmodule ℤ L L) (derivedSeriesOfIdeal ℤ L k ⊤) x
⊢ (↑(Submodule.span R
          {x : L |
            ∃ (x_1 : L),
              Membership.mem (γ := LieSubmodule ℤ L L) (derivedSeriesOfIdeal ℤ L k ⊤) x_1 ∧
                ∃ (n : L), Membership.mem (γ := LieSubmodule ℤ L L) (derivedSeriesOfIdeal ℤ L k ⊤) n ∧ ⁅x_1, n⁆ = x}) :
      Set L) ≤
    (↑(Submodule.span ℤ
          {x : L |
            ∃ (x_1 : L),
              Membership.mem (γ := LieIdeal ℤ L) (derivedSeriesOfIdeal ℤ L k ⊤) x_1 ∧
                ∃ (n : L), Membership.mem (γ := LieSubmodule ℤ L L) (derivedSeriesOfIdeal ℤ L k ⊤) n ∧ ⁅x_1, n⁆ = x}) :
      Set L)

Tactic:
exact coe_derivedSeries_eq_int_aux _ _ L k ih

Premises used: _private.0.LieIdeal.coe_derivedSeries_eq_int_aux
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
k : ℕ
ih :
  ∀ (x : L),
    Membership.mem (γ := LieSubmodule R L L) (derivedSeriesOfIdeal R L k ⊤) x ↔
      Membership.mem (γ := LieSubmodule ℤ L L) (derivedSeriesOfIdeal ℤ L k ⊤) x
⊢ (↑(Submodule.span ℤ
          {x : L |
            ∃ (x_1 : L),
              Membership.mem (γ := LieIdeal ℤ L) (derivedSeriesOfIdeal ℤ L k ⊤) x_1 ∧
                ∃ (n : L), Membership.mem (γ := LieSubmodule ℤ L L) (derivedSeriesOfIdeal ℤ L k ⊤) n ∧ ⁅x_1, n⁆ = x}) :
      Set L) ≤
    (↑(Submodule.span R
          {x : L |
            ∃ (x_1 : L),
              Membership.mem (γ := LieSubmodule ℤ L L) (derivedSeriesOfIdeal ℤ L k ⊤) x_1 ∧
                ∃ (n : L), Membership.mem (γ := LieSubmodule ℤ L L) (derivedSeriesOfIdeal ℤ L k ⊤) n ∧ ⁅x_1, n⁆ = x}) :
      Set L)

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
k : ℕ
zero :
  (↑(↑(derivedSeriesOfIdeal R L 0 ⊤) : Submodule R L) : Set L) =
    (↑(↑(derivedSeriesOfIdeal ℤ L 0 ⊤) : Submodule ℤ L) : Set L)
succ :
  ∀ (k : ℕ)
    (ih :
      (↑(↑(derivedSeriesOfIdeal R L k ⊤) : Submodule R L) : Set L) =
        (↑(↑(derivedSeriesOfIdeal ℤ L k ⊤) : Submodule ℤ L) : Set L)),
    (↑(↑(derivedSeriesOfIdeal R L (k + 1) ⊤) : Submodule R L) : Set L) =
      (↑(↑(derivedSeriesOfIdeal ℤ L (k + 1) ⊤) : Submodule ℤ L) : Set L)
⊢ (↑(↑(derivedSeriesOfIdeal R L k ⊤) : Submodule R L) : Set L) =
    (↑(↑(derivedSeriesOfIdeal ℤ L k ⊤) : Submodule ℤ L) : Set L)

Tactic:
induction k with
  | zero => rfl
  | succ k ih =>
    rw [derivedSeriesOfIdeal_succ, derivedSeriesOfIdeal_succ]
    rw [LieSubmodule.lieIdeal_oper_eq_linear_span', LieSubmodule.lieIdeal_oper_eq_linear_span']
    rw [Set.ext_iff] at ih
    simp only [SetLike.mem_coe, LieSubmodule.mem_toSubmodule] at ih
    simp only [ih]
    apply le_antisymm
    · exact coe_derivedSeries_eq_int_aux _ _ L k ih
    · simp

Premises used: LieSubmodule.lieIdeal_oper_eq_linear_span', LieSubmodule.mem_toSubmodule, LieAlgebra.derivedSeriesOfIdeal_succ, le_antisymm, SetLike.mem_coe, Set.ext_iff
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
I J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
⊢ IsSolvable.{v} ↥⊥

Tactic:
⟨⟨0, Subsingleton.elim _ ⊥⟩⟩

Premises used: LieAlgebra.IsSolvable.mk_int, Bot.bot, Exists.intro, Subsingleton.elim, OfNat.ofNat
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
⊢ IsSolvable L ↔ ∃ (k : ℕ), Eq (α := LieIdeal R L) (derivedSeries R L k) ⊥

Tactic:
simp [isSolvable_iff_int, SetLike.ext'_iff, LieIdeal.coe_derivedSeries_eq_int]

Premises used: LieAlgebra.isSolvable_iff_int, LieIdeal.coe_derivedSeries_eq_int, SetLike.ext'_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
inst_3 : IsSolvable L
⊢ ∃ (k : ℕ), Eq (α := LieIdeal R L) (derivedSeries R L k) ⊥

Tactic:
(isSolvable_iff R L).mp ‹_›

Premises used: LieAlgebra.isSolvable_iff, 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
k : ℕ
h : Eq (α := LieIdeal R L) (derivedSeries R L k) ⊥
⊢ IsSolvable L

Tactic:
(isSolvable_iff R L).mpr ⟨k, h⟩

Premises used: Iff.mpr, LieAlgebra.isSolvable_iff, Exists.intro
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
I_1 J_1 : LieIdeal R L
f : L' →ₗ⁅R⁆ L
I J : LieIdeal R L
inst_5 : IsSolvable.{v} ↥I
inst_6 : IsSolvable.{v} ↥J
obtain : ∀ (k : ℕ) (hk : Eq.{v + 1} (α := LieIdeal R ↥I) (derivedSeries R (↥I) k) ⊥), IsSolvable.{v} ↥(I + J)
⊢ IsSolvable.{v} ↥(I + J)

Tactic:
obtain ⟨k, hk⟩ := IsSolvable.solvable R I

Premises used: Membership.mem, Subtype, LieAlgebra.IsSolvable.solvable
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
I_1 J_1 : LieIdeal R L
f : L' →ₗ⁅R⁆ L
I J : LieIdeal R L
inst_5 : IsSolvable.{v} ↥I
inst_6 : IsSolvable.{v} ↥J
k : ℕ
hk : Eq.{v + 1} (α := LieIdeal R ↥I) (derivedSeries R (↥I) k) ⊥
obtain : ∀ (l : ℕ) (hl : Eq.{v + 1} (α := LieIdeal R ↥J) (derivedSeries R (↥J) l) ⊥), IsSolvable.{v} ↥(I + J)
⊢ IsSolvable.{v} ↥(I + J)

Tactic:
obtain ⟨l, hl⟩ := IsSolvable.solvable R J

Premises used: Membership.mem, Subtype, LieAlgebra.IsSolvable.solvable
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
I_1 J_1 : LieIdeal R L
f : L' →ₗ⁅R⁆ L
I J : LieIdeal R L
inst_5 : IsSolvable.{v} ↥I
inst_6 : IsSolvable.{v} ↥J
k : ℕ
hk : Eq.{v + 1} (α := LieIdeal R ↥I) (derivedSeries R (↥I) k) ⊥
l : ℕ
hl : Eq.{v + 1} (α := LieIdeal R ↥J) (derivedSeries R (↥J) l) ⊥
⊢ IsSolvable.{v} ↥(I + J)

Tactic:
IsSolvable.mk (LieIdeal.derivedSeries_add_eq_bot hk hl)

Premises used: LieAlgebra.IsSolvable.mk, LieIdeal.derivedSeries_add_eq_bot
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
I_1 J_1 : LieIdeal R L
f : L' →ₗ⁅R⁆ L
I J : LieIdeal R L
inst_5 : IsSolvable.{v} ↥I
inst_6 : IsSolvable.{v} ↥J
k : ℕ
hk : Eq.{v + 1} (α := LieIdeal R ↥I) (derivedSeries R (↥I) k) ⊥
l : ℕ
hl : Eq.{v + 1} (α := LieIdeal R ↥J) (derivedSeries R (↥J) l) ⊥
⊢ IsSolvable.{v} ↥(I + J)

Tactic:
exact IsSolvable.mk (LieIdeal.derivedSeries_add_eq_bot hk hl)

Premises used: LieAlgebra.IsSolvable.mk, LieIdeal.derivedSeries_add_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
inst_3 : IsSolvable L
inst_4 : Nontrivial L
obtain :
  ∀ (n : ℕ) (hn : Eq (α := LieIdeal R L) (derivedSeries R L n) ⊥), LT.lt (α := LieIdeal R L) (derivedSeries R L 1) ⊤
⊢ LT.lt (α := LieIdeal R L) (derivedSeries R L 1) ⊤

Tactic:
obtain ⟨n, hn⟩ := IsSolvable.solvable (R := R) (L := L)

Premises used: LieAlgebra.IsSolvable.solvable
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSolvable L
inst_4 : Nontrivial L
n : ℕ
hn : Eq (α := LieIdeal R L) (derivedSeries R L n) ⊥
rw : Ne (α := LieIdeal R L) (derivedSeries R L 1) ⊤
⊢ LT.lt (α := LieIdeal R L) (derivedSeries R L 1) ⊤

Tactic:
rw [lt_top_iff_ne_top]

Premises used: lt_top_iff_ne_top
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSolvable L
inst_4 : Nontrivial L
n : ℕ
hn : Eq (α := LieIdeal R L) (derivedSeries R L n) ⊥
contra : Eq (α := LieIdeal R L) (derivedSeries R L 1) ⊤
⊢ Eq.{v + 1} (α := LieIdeal R L) ⊤ ⊥

Tactic:
rw [LieIdeal.derivedSeries_eq_top n contra] at hn

Premises used: LieIdeal.derivedSeries_eq_top
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSolvable L
inst_4 : Nontrivial L
n : ℕ
hn : Eq (α := LieIdeal R L) (derivedSeries R L n) ⊥
contra : Eq (α := LieIdeal R L) (derivedSeries R L 1) ⊤
hn₁ : Eq.{v + 1} (α := LieIdeal R L) ⊤ ⊥
⊢ Eq (α := LieIdeal R L) (derivedSeries R L 1) ⊤

Tactic:
rw [LieIdeal.derivedSeries_eq_top n contra] at hn

Premises used: LieIdeal.derivedSeries_eq_top
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSolvable L
inst_4 : Nontrivial L
n : ℕ
hn : Eq.{v + 1} (α := LieIdeal R L) ⊤ ⊥
contra : Eq (α := LieIdeal R L) (derivedSeries R L 1) ⊤
⊢ False

Tactic:
top_ne_bot hn

Premises used: top_ne_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
inst_3 : IsSolvable L
inst_4 : Nontrivial L
n : ℕ
hn : Eq.{v + 1} (α := LieIdeal R L) ⊤ ⊥
contra : Eq (α := LieIdeal R L) (derivedSeries R L 1) ⊤
⊢ False

Tactic:
exact top_ne_bot hn

Premises used: top_ne_bot
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
I J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
A : Type u_1
inst_5 : CommRing A
inst_6 : Algebra R A
inst_7 : IsSolvable L
obtain : ∀ (k : ℕ) (hk : Eq (α := LieIdeal R L) (derivedSeries R L k) ⊥), IsSolvable (A ⊗[R] L)
⊢ IsSolvable (A ⊗[R] L)

Tactic:
obtain ⟨k, hk⟩ := IsSolvable.solvable R L

Premises used: LieAlgebra.IsSolvable.solvable
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
I J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
A : Type u_1
inst_5 : CommRing A
inst_6 : Algebra R A
inst_7 : IsSolvable L
k : ℕ
hk : Eq (α := LieIdeal R L) (derivedSeries R L k) ⊥
rw : ∃ (k : ℕ), Eq (α := LieIdeal A (A ⊗[R] L)) (derivedSeries A (A ⊗[R] L) k) ⊥
⊢ IsSolvable (A ⊗[R] L)

Tactic:
rw [isSolvable_iff A]

Premises used: LieAlgebra.isSolvable_iff
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
I J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
A : Type u_1
inst_5 : CommRing A
inst_6 : Algebra R A
inst_7 : IsSolvable L
k : ℕ
hk : Eq (α := LieIdeal R L) (derivedSeries R L k) ⊥
h : Eq (α := LieIdeal A (A ⊗[R] L)) (LieSubmodule.baseChange A (derivedSeries R L k)) ⊥
h₁ : Eq (α := LieIdeal A (A ⊗[R] L)) (LieSubmodule.baseChange A ⊥) ⊥
h₂ h₃ : Eq (α := LieIdeal A (A ⊗[R] L)) ⊥ ⊥
⊢ Eq (α := LieIdeal A (A ⊗[R] L)) (derivedSeries A (A ⊗[R] L) k) ⊥

Tactic:
rw [derivedSeries_baseChange, hk, LieSubmodule.baseChange_bot]

Premises used: LieAlgebra.derivedSeries_baseChange, LieSubmodule.baseChange_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
A : Type u_1
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Module.FaithfullyFlat R A
⊢ IsSolvable (A ⊗[R] L) ↔ IsSolvable L

Tactic:
⟨?_, fun _ ↦ inferInstance⟩

Premises used: inferInstance, Iff.intro
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
A : Type u_1
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Module.FaithfullyFlat R A
refine : IsSolvable (A ⊗[R] L) → IsSolvable L
⊢ IsSolvable (A ⊗[R] L) ↔ IsSolvable L

Tactic:
refine ⟨?_, fun _ ↦ inferInstance⟩
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
A : Type u_1
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Module.FaithfullyFlat R A
rw :
  (∃ (k : ℕ), Eq (α := LieIdeal A (A ⊗[R] L)) (derivedSeries A (A ⊗[R] L) k) ⊥) →
    ∃ (k : ℕ), Eq (α := LieIdeal R L) (derivedSeries R L k) ⊥
⊢ IsSolvable (A ⊗[R] L) → IsSolvable L

Tactic:
rw [isSolvable_iff A, isSolvable_iff R]

Premises used: LieAlgebra.isSolvable_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
A : Type u_1
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Module.FaithfullyFlat R A
k : ℕ
h : Eq (α := LieIdeal A (A ⊗[R] L)) (derivedSeries A (A ⊗[R] L) k) ⊥
h₁ : Eq (α := LieIdeal R L) (derivedSeries R L k) ⊥
⊢ ∃ (k : ℕ), Eq (α := LieIdeal R L) (derivedSeries R L k) ⊥

Tactic:
use k
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
A : Type u_1
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Module.FaithfullyFlat R A
k : ℕ
h : Eq (α := LieIdeal A (A ⊗[R] L)) (derivedSeries A (A ⊗[R] L) k) ⊥
h₁ :
  ∀ (h : LE.le (α := LieIdeal A (A ⊗[R] L)) (derivedSeries A (A ⊗[R] L) k) ⊥),
    LE.le (α := LieIdeal R L) (derivedSeries R L k) ⊥
⊢ Eq (α := LieIdeal R L) (derivedSeries R L k) ⊥

Tactic:
rw [eq_bot_iff] at h ⊢

Premises used: 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
A : Type u_1
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Module.FaithfullyFlat R A
k : ℕ
h : LE.le (α := LieIdeal A (A ⊗[R] L)) (derivedSeries A (A ⊗[R] L) k) ⊥
x : L
hx : Membership.mem (γ := LieSubmodule R L L) (derivedSeries R L k) x
h₁ :
  ∀ (h : LE.le (α := LieIdeal A (A ⊗[R] L)) (LieSubmodule.baseChange A (derivedSeries R L k)) ⊥) ⦃x : L⦄
    (hx : Membership.mem (γ := LieSubmodule R L L) (derivedSeries R L k) x),
    Membership.mem (γ := LieSubmodule R L L) ⊥ x
⊢ Membership.mem (γ := LieSubmodule R L L) ⊥ x

Tactic:
rw [derivedSeries_baseChange] at h

Premises used: LieAlgebra.derivedSeries_baseChange
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
A : Type u_1
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Module.FaithfullyFlat R A
k : ℕ
h : LE.le (α := LieIdeal A (A ⊗[R] L)) (LieSubmodule.baseChange A (derivedSeries R L k)) ⊥
x : L
hx : Membership.mem (γ := LieSubmodule R L L) (derivedSeries R L k) x
⊢ Membership.mem (γ := LieSubmodule A (A ⊗[R] L) (A ⊗[R] L)) ⊥ (1 ⊗ₜ[R] x)

Tactic:
specialize h <| Submodule.tmul_mem_baseChange_of_mem 1 hx

Premises used: Submodule.tmul_mem_baseChange_of_mem, OfNat.ofNat
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
A : Type u_1
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Module.FaithfullyFlat R A
k : ℕ
x : L
hx : Membership.mem (γ := LieSubmodule R L L) (derivedSeries R L k) x
h : Membership.mem (γ := LieSubmodule A (A ⊗[R] L) (A ⊗[R] L)) ⊥ (1 ⊗ₜ[R] x)
h₁ : ∀ (h : Eq (α := A ⊗[R] L) (1 ⊗ₜ[R] x) 0), x = 0
⊢ Membership.mem (γ := LieSubmodule R L L) ⊥ x

Tactic:
rw [LieSubmodule.mem_bot] at h ⊢

Premises used: LieSubmodule.mem_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
A : Type u_1
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Module.FaithfullyFlat R A
k : ℕ
x : L
hx : Membership.mem (γ := LieSubmodule R L L) (derivedSeries R L k) x
h : Eq (α := A ⊗[R] L) (1 ⊗ₜ[R] x) 0
h₁ h₂ h₃ h₄ : ∀ (h : x = 0), x = 0
⊢ x = 0

Tactic:
rwa [Module.FaithfullyFlat.one_tmul_eq_zero_iff] at h

Premises used: Module.FaithfullyFlat.one_tmul_eq_zero_iff
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
L' : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
f : L' →ₗ⁅R⁆ L
hL : IsSolvable L
h : Injective.{w₁ + 1, v + 1} (α := L') (β := L) (⇑f : (a : L') → L)
rw :
  ∀ (hL : ∃ (k : ℕ), Eq (α := LieIdeal R L) (derivedSeries R L k) ⊥)
    (h : Injective.{w₁ + 1, v + 1} (α := L') (β := L) (⇑f : (a : L') → L)),
    ∃ (k : ℕ), Eq (α := LieIdeal R L') (derivedSeries R L' k) ⊥
⊢ IsSolvable L'

Tactic:
rw [isSolvable_iff R] at hL ⊢

Premises used: LieAlgebra.isSolvable_iff
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
L' : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
f : L' →ₗ⁅R⁆ L
hL : ∃ (k : ℕ), Eq (α := LieIdeal R L) (derivedSeries R L k) ⊥
h : Injective.{w₁ + 1, v + 1} (α := L') (β := L) (⇑f : (a : L') → L)
apply : ∀ (a : ℕ), Eq (α := LieIdeal R L) (derivedSeries R L a) ⊥ → Eq (α := LieIdeal R L') (derivedSeries R L' a) ⊥
⊢ ∃ (k : ℕ), Eq (α := LieIdeal R L') (derivedSeries R L' k) ⊥

Tactic:
apply hL.imp

Premises used: Exists.imp