The abel tactic

Evaluate expressions in the language of additive, commutative monoids and groups.

ink

structure Mathlib.Tactic.Abel.Context : Type

• The type of the ambient additive commutative group or monoid.

  α : Lean.Expr

• The universe level for α.

  univ : Lean.Level

• The expression representing 0 : α.

  α0 : Lean.Expr

• Specify whether we are in an additive commutative group or an additive commutative monoid.

  isGroup : Bool

• The AddCommGroup α or AddCommMonoid α expression.

  inst : Lean.Expr

The Context for a call to abel.

Stores a few options for this call, and caches some common subexpressions such as typeclass instances and 0 : α.

ink

def Mathlib.Tactic.Abel.mkContext (e : Lean.Expr) : Lean.MetaM Mathlib.Tactic.Abel.Context

Populate a context object for evaluating e.

Equations

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

ink

@[inline]

abbrev Mathlib.Tactic.Abel.M (α : Type) : Type

The monad for Abel contains, in addition to the AtomM state, some information about the current type we are working over, so that we can consistently use group lemmas or monoid lemmas as appropriate.

Equations

• Mathlib.Tactic.Abel.M = ReaderT Mathlib.Tactic.Abel.Context Mathlib.Tactic.AtomM

ink

def Mathlib.Tactic.Abel.Context.app (c : Mathlib.Tactic.Abel.Context) (n : Lean.Name) (inst : Lean.Expr) : Array Lean.Expr → Lean.Expr

Apply the function n : ∀ {α} [inst : AddWhatever α], _∀ {α} [inst : AddWhatever α], _ to the implicit parameters in the context, and the given list of arguments.

Equations

• Mathlib.Tactic.Abel.Context.app c n inst = Lean.mkAppN (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const n [c.univ]) c.α) inst)

ink

def Mathlib.Tactic.Abel.Context.mkApp (c : Mathlib.Tactic.Abel.Context) (n : Lean.Name) (inst : Lean.Name) (l : Array Lean.Expr) : Lean.MetaM Lean.Expr

Apply the function n : ∀ {α} [inst α], _∀ {α} [inst α], _ to the implicit parameters in the context, and the given list of arguments.

Compared to context.app, this takes the name of the typeclass, rather than an inferred typeclass instance.

Equations

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

ink

def Mathlib.Tactic.Abel.addG : Lean.Name → Lean.Name

Add the letter "g" to the end of the name, e.g. turning term into termg.

This is used to choose between declarations taking AddCommMonoid and those taking AddCommGroup instances.

Equations

• Mathlib.Tactic.Abel.addG x = match x with | Lean.Name.str p s => Lean.Name.str p (s ++ "g") | n => n

ink

def Mathlib.Tactic.Abel.iapp (n : Lean.Name) (xs : Array Lean.Expr) : Mathlib.Tactic.Abel.M Lean.Expr

Apply the function n : ∀ {α} [AddComm{Monoid,Group} α]∀ {α} [AddComm{Monoid,Group} α] to the given list of arguments.

Will use the AddComm{Monoid,Group} instance that has been cached in the context.

Equations

• Mathlib.Tactic.Abel.iapp n xs = do let c ← read pure (Mathlib.Tactic.Abel.Context.app c (if c.isGroup = true then Mathlib.Tactic.Abel.addG n else n) c.inst xs)

ink

def Mathlib.Tactic.Abel.term {α : Type u_1} [inst : AddCommMonoid α] (n : ℕ) (x : α) (a : α) : α

A type synonym used by abel to represent n • x + a in an additive commutative monoid.

Equations

• Mathlib.Tactic.Abel.term n x a = n • x + a

ink

def Mathlib.Tactic.Abel.termg {α : Type u_1} [inst : AddCommGroup α] (n : ℤ) (x : α) (a : α) : α

A type synonym used by abel to represent n • x + a in an additive commutative group.

Equations

• Mathlib.Tactic.Abel.termg n x a = n • x + a

ink

def Mathlib.Tactic.Abel.mkTerm (n : Lean.Expr) (x : Lean.Expr) (a : Lean.Expr) : Mathlib.Tactic.Abel.M Lean.Expr

Evaluate a term with coefficient n, atom x and successor terms a.

Equations

• Mathlib.Tactic.Abel.mkTerm n x a = Mathlib.Tactic.Abel.iapp `Mathlib.Tactic.Abel.term #[n, x, a]

ink

def Mathlib.Tactic.Abel.intToExpr (n : ℤ) : Mathlib.Tactic.Abel.M Lean.Expr

Interpret an integer as a coefficient to a term.

Equations

• Mathlib.Tactic.Abel.intToExpr n = do let __do_lift ← read liftM (Lean.Expr.ofInt (Lean.mkConst (if __do_lift.isGroup = true then `Int else `Nat)) n)

ink

inductive Mathlib.Tactic.Abel.NormalExpr : Type

• zero: Lean.Expr → Mathlib.Tactic.Abel.NormalExpr
• nterm: Lean.Expr → Lean.Expr × ℤ → ℕ × Lean.Expr → Mathlib.Tactic.Abel.NormalExpr → Mathlib.Tactic.Abel.NormalExpr

A normal form for abel. Expressions are represented as a list of terms of the form e = n • x, where n : ℤ and x is an arbitrary element of the additive commutative monoid or group. We explicitly track the Expr forms of e and n, even though they could be reconstructed, for efficiency.

ink

instance Mathlib.Tactic.Abel.instInhabitedNormalExpr : Inhabited Mathlib.Tactic.Abel.NormalExpr

Equations

• Mathlib.Tactic.Abel.instInhabitedNormalExpr = { default := Mathlib.Tactic.Abel.NormalExpr.zero default }

ink

def Mathlib.Tactic.Abel.NormalExpr.e : Mathlib.Tactic.Abel.NormalExpr → Lean.Expr

Extract the expression from a normal form.

Equations

• Mathlib.Tactic.Abel.NormalExpr.e x = match x with | Mathlib.Tactic.Abel.NormalExpr.zero e => e | Mathlib.Tactic.Abel.NormalExpr.nterm e n x a => e

ink

instance Mathlib.Tactic.Abel.instCoeNormalExprExpr : Coe Mathlib.Tactic.Abel.NormalExpr Lean.Expr

Equations

• Mathlib.Tactic.Abel.instCoeNormalExprExpr = { coe := Mathlib.Tactic.Abel.NormalExpr.e }

ink

def Mathlib.Tactic.Abel.NormalExpr.term' (n : Lean.Expr × ℤ) (x : ℕ × Lean.Expr) (a : Mathlib.Tactic.Abel.NormalExpr) : Mathlib.Tactic.Abel.M Mathlib.Tactic.Abel.NormalExpr

Construct the normal form representing a single term.

Equations

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

ink

def Mathlib.Tactic.Abel.NormalExpr.zero' : Mathlib.Tactic.Abel.M Mathlib.Tactic.Abel.NormalExpr

Construct the normal form representing zero.

Equations

• Mathlib.Tactic.Abel.NormalExpr.zero' = do let __do_lift ← read pure (Mathlib.Tactic.Abel.NormalExpr.zero __do_lift.α0)

ink

theorem Mathlib.Tactic.Abel.const_add_term {α : Type u_1} [inst : AddCommMonoid α] (k : α) (n : ℕ) (x : α) (a : α) (a' : α) (h : k + a = a') : k + Mathlib.Tactic.Abel.term n x a = Mathlib.Tactic.Abel.term n x a'

ink

theorem Mathlib.Tactic.Abel.const_add_termg {α : Type u_1} [inst : AddCommGroup α] (k : α) (n : ℤ) (x : α) (a : α) (a' : α) (h : k + a = a') : k + Mathlib.Tactic.Abel.termg n x a = Mathlib.Tactic.Abel.termg n x a'

ink

theorem Mathlib.Tactic.Abel.term_add_const {α : Type u_1} [inst : AddCommMonoid α] (n : ℕ) (x : α) (a : α) (k : α) (a' : α) (h : a + k = a') : Mathlib.Tactic.Abel.term n x a + k = Mathlib.Tactic.Abel.term n x a'

ink

theorem Mathlib.Tactic.Abel.term_add_constg {α : Type u_1} [inst : AddCommGroup α] (n : ℤ) (x : α) (a : α) (k : α) (a' : α) (h : a + k = a') : Mathlib.Tactic.Abel.termg n x a + k = Mathlib.Tactic.Abel.termg n x a'

ink

theorem Mathlib.Tactic.Abel.term_add_term {α : Type u_1} [inst : AddCommMonoid α] (n₁ : ℕ) (x : α) (a₁ : α) (n₂ : ℕ) (a₂ : α) (n' : ℕ) (a' : α) (h₁ : n₁ + n₂ = n') (h₂ : a₁ + a₂ = a') : Mathlib.Tactic.Abel.term n₁ x a₁ + Mathlib.Tactic.Abel.term n₂ x a₂ = Mathlib.Tactic.Abel.term n' x a'

ink

theorem Mathlib.Tactic.Abel.term_add_termg {α : Type u_1} [inst : AddCommGroup α] (n₁ : ℤ) (x : α) (a₁ : α) (n₂ : ℤ) (a₂ : α) (n' : ℤ) (a' : α) (h₁ : n₁ + n₂ = n') (h₂ : a₁ + a₂ = a') : Mathlib.Tactic.Abel.termg n₁ x a₁ + Mathlib.Tactic.Abel.termg n₂ x a₂ = Mathlib.Tactic.Abel.termg n' x a'

ink

theorem Mathlib.Tactic.Abel.zero_term {α : Type u_1} [inst : AddCommMonoid α] (x : α) (a : α) : Mathlib.Tactic.Abel.term 0 x a = a

ink

theorem Mathlib.Tactic.Abel.zero_termg {α : Type u_1} [inst : AddCommGroup α] (x : α) (a : α) : Mathlib.Tactic.Abel.termg 0 x a = a

ink

partial def Mathlib.Tactic.Abel.evalAdd : Mathlib.Tactic.Abel.NormalExpr → Mathlib.Tactic.Abel.NormalExpr → Mathlib.Tactic.Abel.M (Mathlib.Tactic.Abel.NormalExpr × Lean.Expr)

Intepret the sum of two expressions in abel's normal form.

ink

theorem Mathlib.Tactic.Abel.term_neg {α : Type u_1} [inst : AddCommGroup α] (n : ℤ) (x : α) (a : α) (n' : ℤ) (a' : α) (h₁ : -n = n') (h₂ : -a = a') : -Mathlib.Tactic.Abel.termg n x a = Mathlib.Tactic.Abel.termg n' x a'

ink

def Mathlib.Tactic.Abel.evalNeg : Mathlib.Tactic.Abel.NormalExpr → Mathlib.Tactic.Abel.M (Mathlib.Tactic.Abel.NormalExpr × Lean.Expr)

Interpret a negated expression in abel's normal form.

Equations

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

ink

def Mathlib.Tactic.Abel.smul {α : Type u_1} [inst : AddCommMonoid α] (n : ℕ) (x : α) : α

A synonym for •, used internally in abel.

Equations

• Mathlib.Tactic.Abel.smul n x = n • x

ink

def Mathlib.Tactic.Abel.smulg {α : Type u_1} [inst : AddCommGroup α] (n : ℤ) (x : α) : α

A synonym for •, used internally in abel.

Equations

• Mathlib.Tactic.Abel.smulg n x = n • x

ink

theorem Mathlib.Tactic.Abel.zero_smul {α : Type u_1} [inst : AddCommMonoid α] (c : ℕ) : Mathlib.Tactic.Abel.smul c 0 = 0

ink

theorem Mathlib.Tactic.Abel.zero_smulg {α : Type u_1} [inst : AddCommGroup α] (c : ℤ) : Mathlib.Tactic.Abel.smulg c 0 = 0

ink

theorem Mathlib.Tactic.Abel.term_smul {α : Type u_1} [inst : AddCommMonoid α] (c : ℕ) (n : ℕ) (x : α) (a : α) (n' : ℕ) (a' : α) (h₁ : c * n = n') (h₂ : Mathlib.Tactic.Abel.smul c a = a') : Mathlib.Tactic.Abel.smul c (Mathlib.Tactic.Abel.term n x a) = Mathlib.Tactic.Abel.term n' x a'

ink

theorem Mathlib.Tactic.Abel.term_smulg {α : Type u_1} [inst : AddCommGroup α] (c : ℤ) (n : ℤ) (x : α) (a : α) (n' : ℤ) (a' : α) (h₁ : c * n = n') (h₂ : Mathlib.Tactic.Abel.smulg c a = a') : Mathlib.Tactic.Abel.smulg c (Mathlib.Tactic.Abel.termg n x a) = Mathlib.Tactic.Abel.termg n' x a'

ink

def Mathlib.Tactic.Abel.evalSMul (k : Lean.Expr × ℤ) : Mathlib.Tactic.Abel.NormalExpr → Mathlib.Tactic.Abel.M (Mathlib.Tactic.Abel.NormalExpr × Lean.Expr)

Auxiliary function for evalSMul'.

Equations

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

ink

theorem Mathlib.Tactic.Abel.term_atom {α : Type u_1} [inst : AddCommMonoid α] (x : α) : x = Mathlib.Tactic.Abel.term 1 x 0

ink

theorem Mathlib.Tactic.Abel.term_atomg {α : Type u_1} [inst : AddCommGroup α] (x : α) : x = Mathlib.Tactic.Abel.termg 1 x 0

ink

theorem Mathlib.Tactic.Abel.term_atom_pf {α : Type u_1} [inst : AddCommMonoid α] (x : α) (x' : α) (h : x = x') : x = Mathlib.Tactic.Abel.term 1 x' 0

ink

theorem Mathlib.Tactic.Abel.term_atom_pfg {α : Type u_1} [inst : AddCommGroup α] (x : α) (x' : α) (h : x = x') : x = Mathlib.Tactic.Abel.termg 1 x' 0

ink

def Mathlib.Tactic.Abel.evalAtom (e : Lean.Expr) : Mathlib.Tactic.Abel.M (Mathlib.Tactic.Abel.NormalExpr × Lean.Expr)

Interpret an expression as an atom for abel's normal form.

Equations

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

ink

theorem Mathlib.Tactic.Abel.unfold_sub {α : Type u_1} [inst : SubtractionMonoid α] (a : α) (b : α) (c : α) (h : a + -b = c) : a - b = c

ink

theorem Mathlib.Tactic.Abel.unfold_smul {α : Type u_1} [inst : AddCommMonoid α] (n : ℕ) (x : α) (y : α) (h : Mathlib.Tactic.Abel.smul n x = y) : n • x = y

ink

theorem Mathlib.Tactic.Abel.unfold_smulg {α : Type u_1} [inst : AddCommGroup α] (n : ℕ) (x : α) (y : α) (h : Mathlib.Tactic.Abel.smulg (Int.ofNat n) x = y) : ↑n • x = y

ink

theorem Mathlib.Tactic.Abel.unfold_zsmul {α : Type u_1} [inst : AddCommGroup α] (n : ℤ) (x : α) (y : α) (h : Mathlib.Tactic.Abel.smulg n x = y) : n • x = y

ink

theorem Mathlib.Tactic.Abel.subst_into_smul {α : Type u_1} [inst : AddCommMonoid α] (l : ℕ) (r : α) (tl : ℕ) (tr : α) (t : α) (prl : l = tl) (prr : r = tr) (prt : Mathlib.Tactic.Abel.smul tl tr = t) : Mathlib.Tactic.Abel.smul l r = t

ink

theorem Mathlib.Tactic.Abel.subst_into_smulg {α : Type u_1} [inst : AddCommGroup α] (l : ℤ) (r : α) (tl : ℤ) (tr : α) (t : α) (prl : l = tl) (prr : r = tr) (prt : Mathlib.Tactic.Abel.smulg tl tr = t) : Mathlib.Tactic.Abel.smulg l r = t

ink

theorem Mathlib.Tactic.Abel.subst_into_smul_upcast {α : Type u_1} [inst : AddCommGroup α] (l : ℕ) (r : α) (tl : ℕ) (zl : ℤ) (tr : α) (t : α) (prl₁ : l = tl) (prl₂ : ↑tl = zl) (prr : r = tr) (prt : Mathlib.Tactic.Abel.smulg zl tr = t) : Mathlib.Tactic.Abel.smul l r = t

ink

theorem Mathlib.Tactic.Abel.subst_into_add {α : Type u_1} [inst : AddCommMonoid α] (l : α) (r : α) (tl : α) (tr : α) (t : α) (prl : l = tl) (prr : r = tr) (prt : tl + tr = t) : l + r = t

ink

theorem Mathlib.Tactic.Abel.subst_into_addg {α : Type u_1} [inst : AddCommGroup α] (l : α) (r : α) (tl : α) (tr : α) (t : α) (prl : l = tl) (prr : r = tr) (prt : tl + tr = t) : l + r = t

ink

theorem Mathlib.Tactic.Abel.subst_into_negg {α : Type u_1} [inst : AddCommGroup α] (a : α) (ta : α) (t : α) (pra : a = ta) (prt : -ta = t) : -a = t

ink

def Mathlib.Tactic.Abel.evalSMul' (eval : Lean.Expr → Mathlib.Tactic.Abel.M (Mathlib.Tactic.Abel.NormalExpr × Lean.Expr)) (is_smulg : Bool) (orig : Lean.Expr) (e₁ : Lean.Expr) (e₂ : Lean.Expr) : Mathlib.Tactic.Abel.M (Mathlib.Tactic.Abel.NormalExpr × Lean.Expr)

Normalize a term orig of the form smul e₁ e₂ or smulg e₁ e₂. Normalized terms use smul for monoids and smulg for groups, so there are actually four cases to handle:

• Using smul in a monoid just simplifies the pieces using subst_into_smul
• Using smulg in a group just simplifies the pieces using subst_into_smulg
• Using smul a b in a group requires converting a from a nat to an int and then simplifying smulg ↑a b↑a b using subst_into_smul_upcast
• Using smulg in a monoid is impossible (or at least out of scope), because you need a group argument to write a smulg term

Equations

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

ink

partial def Mathlib.Tactic.Abel.eval (e : Lean.Expr) : Mathlib.Tactic.Abel.M (Mathlib.Tactic.Abel.NormalExpr × Lean.Expr)

Evaluate an expression into its abel normal form, by recursing into subexpressions.

ink

def Mathlib.Tactic.Abel.abel1 : Lean.ParserDescr

Tactic for solving equations in the language of additive, commutative monoids and groups. This version of abel fails if the target is not an equality that is provable by the axioms of commutative monoids/groups.

abel1! will use a more aggressive reducibility setting to identify atoms. This can prove goals that abel cannot, but is more expensive.

Equations

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

ink

def Mathlib.Tactic.Abel.abel1! : Lean.ParserDescr

Tactic for solving equations in the language of additive, commutative monoids and groups. This version of abel fails if the target is not an equality that is provable by the axioms of commutative monoids/groups.

abel1! will use a more aggressive reducibility setting to identify atoms. This can prove goals that abel cannot, but is more expensive.

Equations

• Mathlib.Tactic.Abel.abel1! = Lean.ParserDescr.node `Mathlib.Tactic.Abel.abel1! 1024 (Lean.ParserDescr.nonReservedSymbol "abel1!" false)

ink

theorem Mathlib.Tactic.Abel.term_eq {α : Type u_1} [inst : AddCommMonoid α] (n : ℕ) (x : α) (a : α) : Mathlib.Tactic.Abel.term n x a = n • x + a

ink

theorem Mathlib.Tactic.Abel.termg_eq {α : Type u_1} [inst : AddCommGroup α] (n : ℤ) (x : α) (a : α) : Mathlib.Tactic.Abel.termg n x a = n • x + a

A type synonym used by abel to represent n • x + a in an additive commutative group.

ink

def Mathlib.Tactic.Abel.NormalExpr.isAtom : Mathlib.Tactic.Abel.NormalExpr → Bool

True if this represents an atomic expression.

Equations

• Mathlib.Tactic.Abel.NormalExpr.isAtom x = match x with | Mathlib.Tactic.Abel.NormalExpr.nterm e (fst, Int.ofNat 1) x (Mathlib.Tactic.Abel.NormalExpr.zero e_1) => true | x => false

ink

inductive Mathlib.Tactic.Abel.AbelMode : Type

• The default form

  term: Mathlib.Tactic.Abel.AbelMode

• Raw form: the representation abel uses internally.

  raw: Mathlib.Tactic.Abel.AbelMode

The normalization style for abel_nf.

ink

structure Mathlib.Tactic.Abel.AbelNF.Config : Type

• the reducibility setting to use when comparing atoms for defeq

  red : Lean.Meta.TransparencyMode

• if true, atoms inside ring expressions will be reduced recursively

  recursive : Bool

• The normalization style.

  mode : Mathlib.Tactic.Abel.AbelMode

Configuration for abel_nf.

ink

def Mathlib.Tactic.Abel.elabAbelNFConfig : Lean.Syntax → Lean.Elab.TermElabM Mathlib.Tactic.Abel.AbelNF.Config

Function elaborating AbelNF.Config.

Equations

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

ink

def Mathlib.Tactic.Abel.abelNFCore (cfg : Mathlib.Tactic.Abel.AbelNF.Config) (e : Lean.Expr) : Lean.MetaM Lean.Meta.Simp.Result

The core of abel_nf, which rewrites the expression e into abel normal form.

• cfg: the configuration options
• e: the expression to rewrite

Equations

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

ink

partial def Mathlib.Tactic.Abel.abelNFCore.go (cfg : Mathlib.Tactic.Abel.AbelNF.Config) (ctx : Lean.Meta.Simp.Context) (simp : Lean.Meta.Simp.Result → Lean.Meta.SimpM Lean.Meta.Simp.Result) (root : Bool) (parent : Lean.Expr) : Lean.MetaM Lean.Meta.Simp.Result

The recursive case of abelNF.

• root: true when the function is called directly from abelNFCore and false when called by evalAtom in recursive mode.
• parent: The input expression to simplify. In pre we make use of both parent and e to determine if we are at the top level in order to prevent a loop go -> eval -> evalAtom -> go which makes no progress.

ink

partial def Mathlib.Tactic.Abel.abelNFCore.evalAtom (cfg : Mathlib.Tactic.Abel.AbelNF.Config) (ctx : Lean.Meta.Simp.Context) (simp : Lean.Meta.Simp.Result → Lean.Meta.SimpM Lean.Meta.Simp.Result) (parent : Lean.Expr) : Lean.MetaM Lean.Meta.Simp.Result

The evalAtom implementation passed to eval calls go if cfg.recursive is true, and does nothing otherwise.

ink

def Mathlib.Tactic.Abel.abelNFTarget (cfg : Mathlib.Tactic.Abel.AbelNF.Config) : Lean.Elab.Tactic.TacticM Unit

Use abel_nf to rewrite the main goal.

Equations

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

ink

def Mathlib.Tactic.Abel.abelNFLocalDecl (cfg : Mathlib.Tactic.Abel.AbelNF.Config) (fvarId : Lean.FVarId) : Lean.Elab.Tactic.TacticM Unit

Use abel_nf to rewrite hypothesis h.

Equations

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

ink

def Mathlib.Tactic.Abel.abel_term : Lean.ParserDescr

Unsupported legacy syntax from mathlib3, which allowed passing additional terms to abel.

Equations

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

ink

def Mathlib.Tactic.Abel.abel!_term : Lean.ParserDescr

Unsupported legacy syntax from mathlib3, which allowed passing additional terms to abel!.

Equations

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

ink

def Mathlib.Tactic.Abel.abelNF : Lean.ParserDescr

Simplification tactic for expressions in the language of abelian groups, which rewrites all group expressions into a normal form.

• abel_nf! will use a more aggressive reducibility setting to identify atoms.
• abel_nf (config := cfg) allows for additional configuration:
  • red: the reducibility setting (overridden by !)
  • recursive: if true, abel_nf will also recurse into atoms
• abel_nf works as both a tactic and a conv tactic. In tactic mode, abel_nf at h can be used to rewrite in a hypothesis.

Equations

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

ink

def Mathlib.Tactic.Abel.tacticAbel_nf!___ : Lean.ParserDescr

Simplification tactic for expressions in the language of abelian groups, which rewrites all group expressions into a normal form.

• abel_nf! will use a more aggressive reducibility setting to identify atoms.
• abel_nf (config := cfg) allows for additional configuration:
  • red: the reducibility setting (overridden by !)
  • recursive: if true, abel_nf will also recurse into atoms
• abel_nf works as both a tactic and a conv tactic. In tactic mode, abel_nf at h can be used to rewrite in a hypothesis.

Equations

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

ink

def Mathlib.Tactic.Abel.abelNFConv : Lean.ParserDescr

Simplification tactic for expressions in the language of abelian groups, which rewrites all group expressions into a normal form.

• abel_nf! will use a more aggressive reducibility setting to identify atoms.
• abel_nf (config := cfg) allows for additional configuration:
  • red: the reducibility setting (overridden by !)
  • recursive: if true, abel_nf will also recurse into atoms
• abel_nf works as both a tactic and a conv tactic. In tactic mode, abel_nf at h can be used to rewrite in a hypothesis.

Equations

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

ink

def Mathlib.Tactic.Abel.elabAbelNFConv : Lean.Elab.Tactic.Tactic

Elaborator for the abel_nf tactic.

Equations

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

ink

def Mathlib.Tactic.Abel.convAbel_nf!_ : Lean.ParserDescr

Simplification tactic for expressions in the language of abelian groups, which rewrites all group expressions into a normal form.

• abel_nf! will use a more aggressive reducibility setting to identify atoms.
• abel_nf (config := cfg) allows for additional configuration:
  • red: the reducibility setting (overridden by !)
  • recursive: if true, abel_nf will also recurse into atoms
• abel_nf works as both a tactic and a conv tactic. In tactic mode, abel_nf at h can be used to rewrite in a hypothesis.

Equations

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

ink

def Mathlib.Tactic.Abel.abel : Lean.ParserDescr

Tactic for evaluating expressions in abelian groups.

• abel! will use a more aggressive reducibility setting to determine equality of atoms.
• abel1 fails if the target is not an equality.

For example:

example [AddCommMonoid α] (a b : α) : a + (b + a) = a + a + b := by abel
example [AddCommGroup α] (a : α) : (3 : ℤ) • a = a + (2 : ℤ) • a := by abel

Equations

• Mathlib.Tactic.Abel.abel = Lean.ParserDescr.node `Mathlib.Tactic.Abel.abel 1024 (Lean.ParserDescr.nonReservedSymbol "abel" false)

ink

def Mathlib.Tactic.Abel.tacticAbel! : Lean.ParserDescr

Tactic for evaluating expressions in abelian groups.

• abel! will use a more aggressive reducibility setting to determine equality of atoms.
• abel1 fails if the target is not an equality.

For example:

example [AddCommMonoid α] (a b : α) : a + (b + a) = a + a + b := by abel
example [AddCommGroup α] (a : α) : (3 : ℤ) • a = a + (2 : ℤ) • a := by abel

Equations

• Mathlib.Tactic.Abel.tacticAbel! = Lean.ParserDescr.node `Mathlib.Tactic.Abel.tacticAbel! 1024 (Lean.ParserDescr.nonReservedSymbol "abel!" false)

ink

def Mathlib.Tactic.Abel.abelConv : Lean.ParserDescr

The tactic abel evaluates expressions in abelian groups. This is the conv tactic version, which rewrites a target which is a abel equality to True.

See also the abel tactic.

Equations

• Mathlib.Tactic.Abel.abelConv = Lean.ParserDescr.node `Mathlib.Tactic.Abel.abelConv 1024 (Lean.ParserDescr.nonReservedSymbol "abel" false)

ink

def Mathlib.Tactic.Abel.convAbel! : Lean.ParserDescr

The tactic abel evaluates expressions in abelian groups. This is the conv tactic version, which rewrites a target which is a abel equality to True.

See also the abel tactic.

Equations

• Mathlib.Tactic.Abel.convAbel! = Lean.ParserDescr.node `Mathlib.Tactic.Abel.convAbel! 1024 (Lean.ParserDescr.nonReservedSymbol "abel!" false)