LeanPool.LowDimSolvClassification.Tactics

def V (M : Type u_1) : Type u_1

Pair-or-single carrier used by the Lie-algebra atom store: each atom is either a single expression or a pair of expressions tracked together.

Equations

• V M = (M ⊕ M × M)

structure AtomD.State : Type

State of the Lie-algebra atom monad: the running list of atoms collected so far.

• atoms : Array (V Lean.Expr)

  TODO.

@[reducible, inline]

abbrev AtomD (α : Type) : Type

The Lie-algebra atom monad: MetaM with state tracking the atoms encountered.

Equations

• AtomD = StateRefT' IO.RealWorld AtomD.State Lean.MetaM

def AtomD.run {α : Type} (m : AtomD α) : Lean.MetaM α

Run an AtomD computation starting from the empty atom state.

Equations

• m.run = StateRefT'.run' m { }

def AtomD.addAtomSimple (e : Lean.Expr) : AtomD (ℕ × Bool × Lean.Expr)

TODO.

Equations

• One or more equations did not get rendered due to their size.

def AtomD.addAtomDouble (e₁ e₂ : Lean.Expr) : AtomD (ℕ × Bool × Lean.Expr × Lean.Expr)

TODO.

Equations

• One or more equations did not get rendered due to their size.

def AtomD.addAtomQ {u : Lean.Level} {α : Q(Type u)} (e : Q(«$α»)) : AtomD (ℕ × { e' : Q(«$α») // «$e» =Q «$e'» })

TODO.

Equations

• AtomD.addAtomQ e = do let __x ← AtomD.addAtomSimple e match __x with | (n, fst, e') => pure (n, ⟨e', ⋯⟩)

def AtomD.addAtomDoubleQ {u : Lean.Level} {α : Q(Type u)} (e₁ e₂ : Q(«$α»)) : AtomD (ℕ × ({ e' : Q(«$α») × Q(«$α») // «$e₁» =Q unknown_1 ∧ «$e₂» =Q unknown_1 } ⊕ { e' : Q(«$α») × Q(«$α») // «$e₁» =Q unknown_1 ∧ «$e₂» =Q unknown_1 }))

TODO.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.LieSolver.v {M : Type u_1} [LieRing M] (x : V M) : M

TODO.

Equations

• Mathlib.Tactic.LieSolver.v x = Sum.elim (fun (m : M) => m) (fun (x : M × M) => match x with | (m₁, m₂) => ⁅m₁, m₂⁆) x

def Mathlib.Tactic.LieSolver.NF (R : Type u_1) (M : Type u_2) : Type (max u_2 u_1)

TODO.

Equations

• Mathlib.Tactic.LieSolver.NF R M = List (R × V M)

@[match_pattern]

def Mathlib.Tactic.LieSolver.NF.cons {R : Type u_2} {M : Type u_3} (p : R × V M) (l : NF R M) : NF R M

TODO.

Equations

• p ::ᵣ l = p :: l

def Mathlib.Tactic.LieSolver.NF.«term_::ᵣ_» : Lean.TrailingParserDescr

TODO.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.LieSolver.NF.eval {R : Type u_2} {M : Type u_3} [SMul R M] [LieRing M] (l : NF R M) : M

TODO.

Equations

• l.eval = (List.map (fun (x : R × V M) => match x with | (r, x) => r • Mathlib.Tactic.LieSolver.v x) l).sum

@[simp]

theorem Mathlib.Tactic.LieSolver.NF.eval_cons {R : Type u_2} {M : Type u_3} [SMul R M] [LieRing M] (p : R × V M) (l : NF R M) : (p ::ᵣ l).eval = p.1 • v p.2 + l.eval

theorem Mathlib.Tactic.LieSolver.NF.atom_eq_eval {M : Type u_3} [LieRing M] (x : M) : x = eval [(1, Sum.inl x)]

theorem Mathlib.Tactic.LieSolver.NF.atom_eq_evalD {M : Type u_3} [LieRing M] (x y : M) : ⁅x, y⁆ = ((1, Sum.inr (x, y)) ::ᵣ []).eval

theorem Mathlib.Tactic.LieSolver.NF.atom_eq_evalD_skew {M : Type u_3} [LieRing M] (x y : M) : ⁅x, y⁆ = ((-1, Sum.inr (y, x)) ::ᵣ []).eval

theorem Mathlib.Tactic.LieSolver.NF.zero_eq_eval (M : Type u_3) [LieRing M] : 0 = eval []

theorem Mathlib.Tactic.LieSolver.NF.add_eq_eval₁ {R : Type u_2} {M : Type u_3} [SMul R M] [LieRing M] (a₁ : R × V M) {a₂ : R × V M} {l₁ l₂ l : NF R M} (h : l₁.eval + (a₂ ::ᵣ l₂).eval = l.eval) : (a₁ ::ᵣ l₁).eval + (a₂ ::ᵣ l₂).eval = (a₁ ::ᵣ l).eval

theorem Mathlib.Tactic.LieSolver.NF.add_eq_eval₂ {R : Type u_2} {M : Type u_3} [Semiring R] [LieRing M] [Module R M] (r₁ r₂ : R) (x : V M) {l₁ l₂ l : NF R M} (h : l₁.eval + l₂.eval = l.eval) : ((r₁, x) ::ᵣ l₁).eval + ((r₂, x) ::ᵣ l₂).eval = ((r₁ + r₂, x) ::ᵣ l).eval

theorem Mathlib.Tactic.LieSolver.NF.add_eq_eval₃ {R : Type u_2} {M : Type u_3} [Semiring R] [LieRing M] [Module R M] {a₁ : R × V M} (a₂ : R × V M) {l₁ l₂ l : NF R M} (h : (a₁ ::ᵣ l₁).eval + l₂.eval = l.eval) : (a₁ ::ᵣ l₁).eval + (a₂ ::ᵣ l₂).eval = (a₂ ::ᵣ l).eval

theorem Mathlib.Tactic.LieSolver.NF.add_eq_eval {R : Type u_2} {M : Type u_3} {R₁ : Type u_4} {R₂ : Type u_5} [LieRing M] [Semiring R] [Module R M] [Semiring R₁] [Module R₁ M] [Semiring R₂] [Module R₂ M] {l₁ l₂ l : NF R M} {l₁' : NF R₁ M} {l₂' : NF R₂ M} {x₁ x₂ : M} (hx₁ : x₁ = l₁'.eval) (hx₂ : x₂ = l₂'.eval) (h₁ : l₁.eval = l₁'.eval) (h₂ : l₂.eval = l₂'.eval) (h : l₁.eval + l₂.eval = l.eval) : x₁ + x₂ = l.eval

theorem Mathlib.Tactic.LieSolver.NF.sub_eq_eval₁ {R : Type u_2} {M : Type u_3} [SMul R M] [LieRing M] (a₁ : R × V M) {a₂ : R × V M} {l₁ l₂ l : NF R M} (h : l₁.eval - (a₂ ::ᵣ l₂).eval = l.eval) : (a₁ ::ᵣ l₁).eval - (a₂ ::ᵣ l₂).eval = (a₁ ::ᵣ l).eval

theorem Mathlib.Tactic.LieSolver.NF.sub_eq_eval₂ {R : Type u_2} {M : Type u_3} [Ring R] [LieRing M] [Module R M] (r₁ r₂ : R) (x : V M) {l₁ l₂ l : NF R M} (h : l₁.eval - l₂.eval = l.eval) : ((r₁, x) ::ᵣ l₁).eval - ((r₂, x) ::ᵣ l₂).eval = ((r₁ - r₂, x) ::ᵣ l).eval

theorem Mathlib.Tactic.LieSolver.NF.sub_eq_eval₃ {R : Type u_2} {M : Type u_3} [Ring R] [LieRing M] [Module R M] {a₁ : R × V M} (a₂ : R × V M) {l₁ l₂ l : NF R M} (h : (a₁ ::ᵣ l₁).eval - l₂.eval = l.eval) : (a₁ ::ᵣ l₁).eval - (a₂ ::ᵣ l₂).eval = ((-a₂.1, a₂.2) ::ᵣ l).eval

theorem Mathlib.Tactic.LieSolver.NF.sub_eq_eval {R : Type u_2} {M : Type u_3} {R₁ : Type u_4} {R₂ : Type u_5} {S₁ : Type u_6} {S₂ : Type u_7} [LieRing M] [Ring R] [Module R M] [Semiring R₁] [Module R₁ M] [Semiring R₂] [Module R₂ M] [Semiring S₁] [Module S₁ M] [Semiring S₂] [Module S₂ M] {l₁ l₂ l : NF R M} {l₁' : NF R₁ M} {l₂' : NF R₂ M} {l₁'' : NF S₁ M} {l₂'' : NF S₂ M} {x₁ x₂ : M} (hx₁ : x₁ = l₁''.eval) (hx₂ : x₂ = l₂''.eval) (h₁' : l₁'.eval = l₁''.eval) (h₂' : l₂'.eval = l₂''.eval) (h₁ : l₁.eval = l₁'.eval) (h₂ : l₂.eval = l₂'.eval) (h : l₁.eval - l₂.eval = l.eval) : x₁ - x₂ = l.eval

@[implicit_reducible]

instance Mathlib.Tactic.LieSolver.NF.instNeg {R : Type u_2} {M : Type u_3} [Neg R] : Neg (NF R M)

Equations

• One or more equations did not get rendered due to their size.

theorem Mathlib.Tactic.LieSolver.NF.eval_neg {R : Type u_2} {M : Type u_3} [Ring R] [LieRing M] [Module R M] (l : NF R M) : (-l).eval = -l.eval

theorem Mathlib.Tactic.LieSolver.NF.zero_sub_eq_eval {R : Type u_2} {M : Type u_3} [Ring R] [LieRing M] [Module R M] (l : NF R M) : 0 - l.eval = (-l).eval

theorem Mathlib.Tactic.LieSolver.NF.neg_eq_eval {S : Type u_1} {R : Type u_2} {M : Type u_3} [LieRing M] [Semiring S] [Module S M] [Ring R] [Module R M] {l : NF R M} {l₀ : NF S M} (hl : l.eval = l₀.eval) {x : M} (h : x = l₀.eval) : -x = (-l).eval

@[implicit_reducible]

instance Mathlib.Tactic.LieSolver.NF.instSMulOfMul {R : Type u_2} {M : Type u_3} [Mul R] : SMul R (NF R M)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Mathlib.Tactic.LieSolver.NF.smul_apply {R : Type u_2} {M : Type u_3} [Mul R] (r : R) (l : NF R M) : r • l = List.map (fun (x : R × V M) => match x with | (a, x) => (r * a, x)) l

theorem Mathlib.Tactic.LieSolver.NF.eval_smul {R : Type u_2} {M : Type u_3} [LieRing M] [Semiring R] [Module R M] {l : NF R M} {x : M} (h : x = l.eval) (r : R) : (r • l).eval = r • x

theorem Mathlib.Tactic.LieSolver.NF.smul_eq_eval {S : Type u_1} {R : Type u_2} {M : Type u_3} {R₀ : Type u_4} [LieRing M] [Semiring R] [Module R M] [Semiring R₀] [Module R₀ M] [Semiring S] [Module S M] {l : NF R M} {l₀ : NF R₀ M} {s : S} {r : R} {x : M} (hx : x = l₀.eval) (hl : l.eval = l₀.eval) (hs : r • x = s • x) : s • x = (r • l).eval

theorem Mathlib.Tactic.LieSolver.NF.eq_cons_cons {R : Type u_2} {M : Type u_3} [LieRing M] [SMul R M] {r₁ r₂ : R} (m : V M) {l₁ l₂ : NF R M} (h1 : r₁ = r₂) (h2 : l₁.eval = l₂.eval) : ((r₁, m) ::ᵣ l₁).eval = ((r₂, m) ::ᵣ l₂).eval

theorem Mathlib.Tactic.LieSolver.NF.eq_cons_const {R : Type u_2} {M : Type u_3} [LieRing M] [Semiring R] [Module R M] {r : R} (m : V M) {n : V M} {l : NF R M} (h1 : r = 0) (h2 : l.eval = v n) : ((r, m) ::ᵣ l).eval = v n

theorem Mathlib.Tactic.LieSolver.NF.eq_const_cons {R : Type u_2} {M : Type u_3} [LieRing M] [Semiring R] [Module R M] {r : R} (m : V M) {n : V M} {l : NF R M} (h1 : 0 = r) (h2 : v n = l.eval) : v n = ((r, m) ::ᵣ l).eval

theorem Mathlib.Tactic.LieSolver.NF.eq_of_eval_eq_eval {R : Type u_2} {M : Type u_3} {R₁ : Type u_4} {R₂ : Type u_5} [LieRing M] [Semiring R] [Module R M] [Semiring R₁] [Module R₁ M] [Semiring R₂] [Module R₂ M] {l₁ l₂ : NF R M} {l₁' : NF R₁ M} {l₂' : NF R₂ M} {x₁ x₂ : M} (hx₁ : x₁ = l₁'.eval) (hx₂ : x₂ = l₂'.eval) (h₁ : l₁.eval = l₁'.eval) (h₂ : l₂.eval = l₂'.eval) (h : l₁.eval = l₂.eval) : x₁ = x₂

def Mathlib.Tactic.LieSolver.NF.algebraMap {S : Type u_1} (R : Type u_2) {M : Type u_3} [CommSemiring S] [Semiring R] [Algebra S R] (l : NF S M) : NF R M

TODO.

Equations

• Mathlib.Tactic.LieSolver.NF.algebraMap R l = List.map (fun (x : S × V M) => match x with | (s, x) => ((algebraMap S R) s, x)) l

theorem Mathlib.Tactic.LieSolver.NF.eval_algebraMap {S : Type u_1} (R : Type u_2) {M : Type u_3} [CommSemiring S] [Semiring R] [Algebra S R] [LieRing M] [SMul S M] [MulAction R M] [IsScalarTower S R M] (l : NF S M) : (algebraMap R l).eval = l.eval

@[reducible, inline]

abbrev Mathlib.Tactic.LieSolver.qNF {u v : Lean.Level} (R : Q(Type u)) (M : Q(Type v)) : Type

TODO.

Equations

• Mathlib.Tactic.LieSolver.qNF R M = List ((Q(«$R») × Q(V «$M»)) × ℕ)

def Mathlib.Tactic.LieSolver.qNF.toNF {u v : Lean.Level} {M : Q(Type v)} {R : Q(Type u)} (l : qNF R M) : Q(NF «$R» «$M»)

TODO.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.LieSolver.qNF.onScalar {v : Lean.Level} {M : Q(Type v)} {u₁ u₂ : Lean.Level} {R₁ : Q(Type u₁)} {R₂ : Q(Type u₂)} (l : qNF R₁ M) (f : Q(«$R₁» → «$R₂»)) : qNF R₂ M

TODO.

Equations

• l.onScalar f = List.map (fun (x : (Q(«$R₁») × Q(V «$M»)) × ℕ) => match x with | ((a, x), k) => ((q(«$f» «$a»), x), k)) l

@[irreducible]

def Mathlib.Tactic.LieSolver.qNF.add {u v : Lean.Level} {M : Q(Type v)} {R : Q(Type u)} (iR : Q(Semiring «$R»)) : qNF R M → qNF R M → qNF R M

TODO.

Equations

• One or more equations did not get rendered due to their size.
• Mathlib.Tactic.LieSolver.qNF.add iR [] x✝ = x✝
• Mathlib.Tactic.LieSolver.qNF.add iR x✝ [] = x✝

@[irreducible]

def Mathlib.Tactic.LieSolver.qNF.mkAddProof {u v : Lean.Level} {M : Q(Type v)} {R : Q(Type u)} {iR : Q(Semiring «$R»)} {iMM : Q(LieRing «$M»)} (iRM : Q(Module «$R» «$M»)) (l₁ l₂ : qNF R M) : have a := (add iR l₁ l₂).toNF; have a_1 := l₂.toNF; have a_2 := l₁.toNF; Q(«$a_2».eval + «$a_1».eval = «$a».eval)

TODO.

Equations

• One or more equations did not get rendered due to their size.
• Mathlib.Tactic.LieSolver.qNF.mkAddProof iRM [] l₂ = q(⋯)
• Mathlib.Tactic.LieSolver.qNF.mkAddProof iRM l₁ [] = q(⋯)

@[irreducible]

def Mathlib.Tactic.LieSolver.qNF.sub {u v : Lean.Level} {M : Q(Type v)} {R : Q(Type u)} (iR : Q(Ring «$R»)) : qNF R M → qNF R M → qNF R M

TODO.

Equations

• One or more equations did not get rendered due to their size.
• Mathlib.Tactic.LieSolver.qNF.sub iR [] x✝ = x✝.onScalar q(Neg.neg)
• Mathlib.Tactic.LieSolver.qNF.sub iR x✝ [] = x✝

@[irreducible]

def Mathlib.Tactic.LieSolver.qNF.mkSubProof {u v : Lean.Level} {M : Q(Type v)} {R : Q(Type u)} (iR : Q(Ring «$R»)) (iMM : Q(LieRing «$M»)) (iRM : Q(Module «$R» «$M»)) (l₁ l₂ : qNF R M) : have a := (sub iR l₁ l₂).toNF; have a_1 := l₂.toNF; have a_2 := l₁.toNF; Q(«$a_2».eval - «$a_1».eval = «$a».eval)

TODO.

Equations

• One or more equations did not get rendered due to their size.
• Mathlib.Tactic.LieSolver.qNF.mkSubProof iR iMM iRM [] l₂ = q(⋯)
• Mathlib.Tactic.LieSolver.qNF.mkSubProof iR iMM iRM l₁ [] = q(⋯)

def Mathlib.Tactic.LieSolver.qNF.matchRings {v : Lean.Level} {M : Q(Type v)} {iMM : Q(LieRing «$M»)} {u₁ : Lean.Level} {R₁ : Q(Type u₁)} {iR₁ : Q(Semiring «$R₁»)} (iRM₁ : Q(Module «$R₁» «$M»)) {u₂ : Lean.Level} {R₂ : Q(Type u₂)} (iR₂ : Q(Semiring «$R₂»)) (iRM₂ : Q(Module «$R₂» «$M»)) (l₁ : qNF R₁ M) (l₂ : qNF R₂ M) (r : Q(«$R₂»)) (x : Q(«$M»)) : Lean.MetaM ((u : Lean.Level) × (R : Q(Type u)) × (iR : Q(Semiring «$R»)) × (x_1 : Q(Module «$R» «$M»)) × ((l₁' : qNF R M) × have a := l₁.toNF; have a_1 := l₁'.toNF; Q(«$a_1».eval = «$a».eval)) × ((l₂' : qNF R M) × have a := l₂.toNF; have a_1 := l₂'.toNF; Q(«$a_1».eval = «$a».eval)) × (r' : Q(«$R»)) × Q(«$r'» • «$x» = «$r» • «$x»))

TODO.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.LieSolver.parseFuel : ℕ

TODO.

Equations

• Mathlib.Tactic.LieSolver.parseFuel = 4096

def Mathlib.Tactic.LieSolver.parseAux {v : Lean.Level} {M : Q(Type v)} (fuel : ℕ) (iMM : Q(LieRing «$M»)) (x : Q(«$M»)) : AtomD ((u : Lean.Level) × (R : Q(Type u)) × (iR : Q(Semiring «$R»)) × (x_1 : Q(Module «$R» «$M»)) × (l : qNF R M) × have a := l.toNF; Q(«$x» = «$a».eval))

TODO.

def Mathlib.Tactic.LieSolver.parse {v : Lean.Level} {M : Q(Type v)} (iMM : Q(LieRing «$M»)) (x : Q(«$M»)) : AtomD ((u : Lean.Level) × (R : Q(Type u)) × (iR : Q(Semiring «$R»)) × (x_1 : Q(Module «$R» «$M»)) × (l : qNF R M) × have a := l.toNF; Q(«$x» = «$a».eval))

TODO.

Equations

• Mathlib.Tactic.LieSolver.parse iMM x = Mathlib.Tactic.LieSolver.parseAux Mathlib.Tactic.LieSolver.parseFuel iMM x

def Mathlib.Tactic.LieSolver.reduceCoefficientwiseAux {u v : Lean.Level} {M : Q(Type v)} (fuel : ℕ) {R : Q(Type u)} {x✝ : Q(LieRing «$M»)} {x✝¹ : Q(Semiring «$R»)} (iRM : Q(Module «$R» «$M»)) (l₁ l₂ : qNF R M) : Lean.MetaM (List Lean.MVarId × have a := l₂.toNF; have a_1 := l₁.toNF; Q(v (Sum.inl «$a_1».eval) = v (Sum.inl «$a».eval)))

TODO.

Equations

• One or more equations did not get rendered due to their size.
• Mathlib.Tactic.LieSolver.reduceCoefficientwiseAux 0 iRM l₁ l₂ = Lean.throwError (Lean.toMessageData "match_scalars_lie: ran out of fuel in reduceCoefficientwise")
• Mathlib.Tactic.LieSolver.reduceCoefficientwiseAux fuel_2.succ iRM [] [] = pure ([], q(⋯))

def Mathlib.Tactic.LieSolver.reduceCoefficientwise {u v : Lean.Level} {M : Q(Type v)} {R : Q(Type u)} {x✝ : Q(LieRing «$M»)} {x✝¹ : Q(Semiring «$R»)} (iRM : Q(Module «$R» «$M»)) (l₁ l₂ : qNF R M) : Lean.MetaM (List Lean.MVarId × have a := l₂.toNF; have a_1 := l₁.toNF; Q(v (Sum.inl «$a_1».eval) = v (Sum.inl «$a».eval)))

TODO.

Equations

• Mathlib.Tactic.LieSolver.reduceCoefficientwise iRM l₁ l₂ = Mathlib.Tactic.LieSolver.reduceCoefficientwiseAux Mathlib.Tactic.LieSolver.parseFuel iRM l₁ l₂

def Mathlib.Tactic.LieSolver.matchScalarsAux (g : Lean.MVarId) : AtomD (List Lean.MVarId)

TODO.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.LieSolver.algebraMapThms : Array Lean.Name

TODO.

Equations

• Mathlib.Tactic.LieSolver.algebraMapThms = #[`eq_natCast, `eq_intCast, `eq_ratCast]

def Mathlib.Tactic.LieSolver.postprocess (mvarId : Lean.MVarId) : Lean.MetaM Lean.MVarId

TODO.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.LieSolver.matchScalars (g : Lean.MVarId) : Lean.MetaM (List Lean.MVarId)

TODO.

Equations

• Mathlib.Tactic.LieSolver.matchScalars g = do let mvars ← (Mathlib.Tactic.LieSolver.matchScalarsAux g).run List.mapM Mathlib.Tactic.LieSolver.postprocess mvars

def Mathlib.Tactic.LieSolver.tacticMatch_scalars_lie : Lean.ParserDescr

match_scalars_lie: turn a Lie-algebra goal into a collection of scalar-coefficient goals that can be discharged by ring-like tactics.

Equations

• Mathlib.Tactic.LieSolver.tacticMatch_scalars_lie = Lean.ParserDescr.node `Mathlib.Tactic.LieSolver.tacticMatch_scalars_lie 1024 (Lean.ParserDescr.nonReservedSymbol "match_scalars_lie" false)

def Mathlib.Tactic.LieSolver.tacticModule_lie : Lean.ParserDescr

module_lie: finishing tactic that reduces a Lie-algebra equality to scalar equalities and discharges each with ring.

Equations

• Mathlib.Tactic.LieSolver.tacticModule_lie = Lean.ParserDescr.node `Mathlib.Tactic.LieSolver.tacticModule_lie 1024 (Lean.ParserDescr.nonReservedSymbol "module_lie" false)

def tacticSimplifyLie : Lean.ParserDescr

simplify_lie: unfold Lie-bracket bilinearity and reduce the goal to scalar equalities using match_scalars_lie, then attempt to close each by ring.

Equations

• tacticSimplifyLie = Lean.ParserDescr.node `tacticSimplifyLie 1024 (Lean.ParserDescr.nonReservedSymbol "simplify_lie" false)

theorem lie_solver3_example {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] (v₁ v₂ v₃ : L) : 4 • ⁅v₁, v₂⁆ + v₂ + ⁅v₁, v₃⁆ + ⁅v₂, v₁⁆ - ⁅-2 • v₁, v₂⁆ = ⁅v₁, 7 • v₂⁆ + 2 • v₂ + ⁅v₂ + v₂, v₁⁆ - v₂ + ⁅-1 • v₃, v₁⁆

theorem lie_solver3_example' {L : Type u_2} [LieRing L] (v₁ v₂ : L) : 4 • ⁅v₁, v₂⁆ + 4 • ⁅v₂, v₁⁆ = 0