LeanPool.LowDimSolvClassification.Tactics

The reflected Lie expressions retain exposed definitions so the kernel can check proofs produced by the tactics. The metaprogramming implementation is compiled without exporting its definition bodies to importing modules.

@[implicit_reducible]

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)

  Distinct scalar atoms and bracket pairs, in their order of discovery.

@[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)

Find an existing atom up to definitional equality, or append a new one.

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)

Intern a bracket pair, recording whether it matches the stored orientation.

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'» })

Intern a quoted atom and retain its definitional equality with the stored expression.

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 }))

Intern a quoted bracket pair, retaining the equalities for its chosen orientation.

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

Interpret an atom as an element or as the bracket of two elements.

Equations

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

@[implicit_reducible]

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

A Lie expression represented as a sum of scalar multiples of atoms.

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

Prepend a scalar multiple of an atom to a reflected Lie expression.

Equations

• p ::ᵣ l = p :: l

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

Constructor notation for reflected Lie expressions.

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

Evaluate a reflected Lie expression by summing its scalar multiples of atoms.

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

@[instance_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

@[instance_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

Extend the scalar ring of a reflected Lie expression through an algebra map.

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

Quoted scalar-atom pairs with identifiers used to order and combine equal atoms.

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»)

Quote a normal form, discarding the atom identifiers used during normalization.

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

Apply a quoted function to every coefficient of a normal form.

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

Merge two normal forms ordered by atom identifier, adding matching coefficients.

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)

Construct the proof that merging normal forms computes their sum.

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

Merge two normal forms ordered by atom identifier, subtracting matching coefficients.

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)

Construct the proof that subtracting normal forms computes their difference.

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»))

Move two normal forms to a common scalar ring, retaining proofs of their values.

Equations

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

def Mathlib.Tactic.LieSolver.parseFuel : ℕ

Recursion budget for parsing expressions and comparing their coefficients.

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))

Normalize a quoted Lie expression with bounded recursion and prove its value.

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))

Normalize a quoted Lie expression using the standard recursion budget.

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)))

Reduce equality of normal forms to coefficient equalities with bounded recursion.

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)))

Produce coefficient goals and a proof that solving them equates the normal forms.

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)

Normalize both sides of an equality and replace it with coefficient goals.

Equations

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

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

Algebra-map identities used to simplify natural, integer, and rational coefficients.

Equations

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

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

Simplify casts and algebra maps in a generated coefficient goal.

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)

Reduce a Lie equality to coefficient goals and simplify their scalar expressions.

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