feat: add_group tactic by kbuzzard · Pull Request #37067 · leanprover-community/mathlib4

kbuzzard · 2026-03-24T00:07:38Z

Written by Claude Code, additivising the group tactic, although there were some problems which needed human input.

This is me burning Claude credits as a result of this comment #mathlib4 > MulAut and to_additive @ 💬 . Just to be clear, all comments below are human-written by me with 0 AI assistance.

To my amusement, naively additivising the group tactic to make an add_group tactic does not work. The problem is that the algorithm run by group involves adding ← zpow_neg_one to the simp set, which rewrites x⁻¹ to x ^ (-1) for x in any group: the idea is that x ^ (z : Int) is preferred in the algorithm and x⁻¹ is eliminated. Amusingly, when additivised, this becomes -x -> -1 • x which then immediately becomes (-1 • 1) • x which then becomes ((-1 • 1) • 1) • x etc etc, as the integers are themselves an additive group. So we need to find another way of normalising terms of the form -x.

Claude found the following trick: drop ← neg_one_zsmul and neg_one_zsmul_add, and use neg_add_rev and neg_zero to reduce -(a+b) and -0, use zsmul_neg to reduce n • (-a) to (-n) • a and then use things like add_neg_cancel_right and neg_add_cancel_right to do -b + b and b + -b together with some new zsmul_neg_trick lemmas which normalise (n • b) + -b to (n - 1) • b. etc. The idea is to ensure that any consecutive chains of b's and -b's and z • b's will now all get amalgamated into something of the form z • b, but we cannot change -b to -1 • b so have to try harder than in the multiplicative case.

Here is a detailed (human-written!) explanation of the difference between Tactic/AddGroup.lean and the additivisation of Tactic/Group.Lean.

Note that the zpow_trick lemmas in Tactic/Group.lean are additivised, so we import Group.lean in AddGroup.lean to access these additivised lemmas.
Mathlib.Algebra.Group.Commutator has no additive version (and it's not clear that it should have one), so we don't use an additive version of commutatorElement_def (which expands ⁅g₁, g₂⁆ to g₁ * g₂ * g₁⁻¹ * g₂⁻¹). Note: that means that we cannot additivise a test.
Line 67 of the additive file uses neg_add_rev, neg_zero, zsmul_neg, ← neg_zsmul, as a workaround for the looping ← zpow_neg_one.
Int.mul_neg, Int.neg_mul are dropped (they don't seem to be needed, all tests are passing, ring_nf is probably doing this.)
sub_eq_add_neg is added: people use subtraction in additive groups; division doesn't seem to be covered for multiplicative groups? So add_group can solve a + b - b = a but group cannot solve a * b / b = a.

There is also one fewer test in the add_group tests, as I had to remove the commutator test.

I don't know much at all about tactic-writing, the PR is all Claude code, but a lot of it is to_additive copypasta. The review of the code above is my own.

github-actions · 2026-03-24T00:08:56Z

PR summary 028964f2c6

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.Tactic`	1
`Mathlib.Tactic.AddGroup` (new file)	524

Declarations diff

+ neg_neg_trick
+ zsmul_neg_trick
+ zsmul_neg_trick'

You can run this locally as follows

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

No changes to technical debt.

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

…' into kbuzzard-add-group

mathlib-merge-conflicts · 2026-04-17T01:40:29Z

This pull request has conflicts, please merge master and resolve them.

Co-authored-by: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>

thorimur

Thanks for this! :) I think this is a good use of an LLM: closely patterning off of existing material plus human thought about the output.

The code is quite clean, but has two (fixable) issues:

Style-wise, we should actually disprefer the pattern of single-use aux tactics that it's patterned off of! :) There are also a couple small issues re: control flow and error messages.
It doesn't take care of cases like (-b) + n • b = (n - 1) • b, because the trick lemmas only apply to e.g. (_ + (-b)) + n • b, which has the wrong associativity. So we just need three more lemmas. We also need to use neg_one_zsmul the ordinary way round to handle (-1) • b = -b.

Hopefully all of these are resolved by these suggestions.

I haven't done a full audit of the simp set to ensure that every lemma is used, but it seems reasonable.

thorimur · 2026-04-24T01:55:06Z

+/-
+Copyright (c) 2026 Kevin Buzzard. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Thomas Browning, Patrick Massot, Kevin Buzzard


Hmm, do we have guidelines for handling authorship when taking large inspiration from another file? On the one hand, it's nice to give credit. On the other hand, authorship answers the question "who do I ping on zulip", and is the answer this gives correct? (Have they been asked if they'd like to be "held responsible"?)

I'm tempted to say the right move is actually just

Suggested change

Authors: Thomas Browning, Patrick Massot, Kevin Buzzard

Authors: Kevin Buzzard

and credit them in the module docstring, unless you've discussed this with them!

thorimur · 2026-04-24T19:45:09Z

+open Lean
+open Lean.Meta
+open Lean.Parser.Tactic
+open Lean.Elab.Tactic


Suggested change

open Lean

open Lean.Meta

open Lean.Parser.Tactic

open Lean.Elab.Tactic

open Lean Meta Parser Elab Tactic

thorimur · 2026-04-24T20:13:56Z

+-- The next three lemmas are not general purpose lemmas, they are intended for use only by
+-- the `add_group` tactic.
+-- They handle the case where a negated element `-b` appears adjacent to a `zsmul` of the same
+-- element, or adjacent to another negated copy.
+theorem zsmul_neg_trick {G : Type*} [AddGroup G] (a b : G) (n : ℤ) :
+    a + n • b + (-b) = a + (n + (-1)) • b := by
+  rw [add_assoc, ← neg_one_zsmul b, ← add_zsmul]
+
+theorem zsmul_neg_trick' {G : Type*} [AddGroup G] (a b : G) (n : ℤ) :
+    a + (-b) + n • b = a + ((-1) + n) • b := by
+  rw [add_assoc, ← neg_one_zsmul b, ← add_zsmul]
+
+theorem neg_neg_trick {G : Type*} [AddGroup G] (a b : G) :
+    a + (-b) + (-b) = a + (-2 : ℤ) • b := by
+  have h : -b = (-1 : ℤ) • b := (neg_one_zsmul b).symm
+  rw [h, add_assoc, ← add_zsmul]; norm_num


The current iteration of add_group can't prove the following:

example (b : G) {n : Int} : (-b) + n • b = (n - 1) • b := by add_group

So I believe we just need to duplicate these trick lemmas to handle the (_ + _) cases; they seem to only handle the ((_ + _) + _) cases.

We also struggle with

example (b : G) : (-b) = (-1) • b := by add_group

Since we're committing to the neg lifestyle via the other trick lemmas, I think we actually want to use neg_one_zsmul in the ordinary direction to put (-1) • in terms of -, then (in more general cases) apply our trick lemmas.

Here, I also deapostrophe'd their names to be more descriptive, and prefixed them with a _. This causes them to be filtered out from autocompletion! :)

Suggested change

-- The next three lemmas are not general purpose lemmas, they are intended for use only by

-- the `add_group` tactic.

-- They handle the case where a negated element `-b` appears adjacent to a `zsmul` of the same

-- element, or adjacent to another negated copy.

theorem zsmul_neg_trick {G : Type*} [AddGroup G] (a b : G) (n : ℤ) :

a + n • b + (-b) = a + (n + (-1)) • b := by

rw [add_assoc, ← neg_one_zsmul b, ← add_zsmul]

theorem zsmul_neg_trick' {G : Type*} [AddGroup G] (a b : G) (n : ℤ) :

a + (-b) + n • b = a + ((-1) + n) • b := by

rw [add_assoc, ← neg_one_zsmul b, ← add_zsmul]

theorem neg_neg_trick {G : Type*} [AddGroup G] (a b : G) :

a + (-b) + (-b) = a + (-2 : ℤ) • b := by

have h : -b = (-1 : ℤ) • b := (neg_one_zsmul b).symm

rw [h, add_assoc, ← add_zsmul]; norm_num

-- The next six lemmas are not general purpose lemmas; they are intended for use only by

-- the `add_group` tactic, and so are prefixed with `_` to keep them out of autocomplete.

-- They handle the case where a negated element `-b` appears adjacent to a `zsmul` of the same

-- element, or adjacent to another negated copy.

-- This means we also want to convert `(-1) • b` to `-b` in order to apply these lemmas.

theorem _zsmul_neg_trick {G : Type*} [AddGroup G] (b : G) (n : ℤ) :

n • b + (-b) = (n + (-1)) • b := by

rw [← neg_one_zsmul b, ← add_zsmul]

theorem _neg_zsmul_trick {G : Type*} [AddGroup G] (b : G) (n : ℤ) :

(-b) + n • b = ((-1) + n) • b := by

rw [← neg_one_zsmul b, ← add_zsmul]

theorem _neg_neg_trick {G : Type*} [AddGroup G] (b : G) :

(-b) + (-b) = (-2 : ℤ) • b := by

have h : -b = (-1 : ℤ) • b := (neg_one_zsmul b).symm

rw [h, ← add_zsmul]; norm_num

theorem _add_zsmul_neg_trick {G : Type*} [AddGroup G] (a b : G) (n : ℤ) :

a + n • b + (-b) = a + (n + (-1)) • b := by

rw [add_assoc, _zsmul_neg_trick]

theorem _add_neg_zsmul_trick {G : Type*} [AddGroup G] (a b : G) (n : ℤ) :

a + (-b) + n • b = a + ((-1) + n) • b := by

rw [add_assoc, _neg_zsmul_trick]

theorem _add_neg_neg_trick {G : Type*} [AddGroup G] (a b : G) :

a + (-b) + (-b) = a + (-2 : ℤ) • b := by

rw [add_assoc, _neg_neg_trick]

thorimur · 2026-04-24T20:41:59Z

+/-- Auxiliary tactic for the `add_group` tactic. Calls the simplifier only. -/
+syntax (name := aux_add_group₁) "aux_add_group₁" (location)? : tactic
+
+macro_rules
+| `(tactic| aux_add_group₁ $[at $location]?) =>
+  `(tactic| simp -decide -failIfUnchanged only
+    [addCommutatorElement_def, neg_add_rev, neg_zero, zsmul_neg, ← neg_zsmul,
+      add_zero, zero_add,
+      ← natCast_zsmul, ← mul_zsmul',
+      Int.natCast_add, Int.natCast_mul, neg_neg,
+      zsmul_zero, zero_zsmul, one_zsmul,
+      ← add_assoc,
+      ← add_zsmul, ← add_one_zsmul, ← one_add_zsmul,
+      Mathlib.Tactic.Group.zsmul_trick,
+      Mathlib.Tactic.Group.zsmul_trick_zero,
+      Mathlib.Tactic.Group.zsmul_trick_zero',
+      zsmul_neg_trick, zsmul_neg_trick',
+      add_neg_cancel_right, neg_add_cancel_right,
+      neg_neg_trick,
+      sub_eq_add_neg,
+      tsub_self, sub_self, add_neg_cancel, neg_add_cancel]
+  $[at $location]?)
+
+/-- Auxiliary tactic for the `add_group` tactic. Calls `ring_nf` to normalize scalars. -/
+syntax (name := aux_add_group₂) "aux_add_group₂" (location)? : tactic
+
+macro_rules
+| `(tactic| aux_add_group₂ $[at $location]?) =>
+  `(tactic| ring_nf (ifUnchanged := .silent) $[at $location]?)
+
+/-- `add_group` normalizes expressions in additive groups that occur in the goal. `add_group` does
+not assume commutativity, instead using only the additive group axioms without any information about
+which group is manipulated. If the goal is an equality, and after normalization the two sides are
+equal, `add_group` closes the goal.
+
+For multiplicative groups, use the `group` tactic instead.
+For additive commutative groups, use the `abel` tactic instead.
+
+* `add_group at l1 l2 ...` normalizes at the given locations.
+
+Example:
+```lean
+example {G : Type} [AddGroup G] (a b c d : G) (h : c = (a + 2 • b) + (-(b + b) + (-a)) + d) :
+    a + c + (-d) = a := by
+  add_group at h -- normalizes `h` which becomes `h : c = d`
+  rw [h]         -- the goal is now `a + d + (-d) = a`
+  add_group      -- which is then normalized and closed
+```
+-/
+syntax (name := add_group) "add_group" (location)? : tactic
+
+macro_rules
+| `(tactic| add_group $[$loc]?) =>
+  `(tactic| repeat (fail_if_no_progress (aux_add_group₁ $[$loc]? <;> aux_add_group₂ $[$loc]?)))


There are a couple of things I think we can change here:

We don't actually need the aux_* tactics. We can/should just inline them inside the macro, since we use them exactly once and don't extend them downstream. (Otherwise their only purpose nowadays is basically to pollute the tactic documentation page! 😅) The simp call is maybe worth isolating for readability, but we can do that with a let in the body of the macro_rules for the main tactic. (Honestly maybe we should do this for group too, since I see that's where this pattern is coming from.)

add_group should probably fail with the appropriate message if no progress is made. For that, we can use first | repeat1 (fail_if_no_progress ...) | fail "`add_group` made no progress; repeat1 ensures that the tactic is successful at least once. Ideally ifUnchanged becomes a config option to add_group, but we can handle that in a separate PR :)

Nit: syntax kind (name := ...)s are usually lowerCamelCase.

(Future issue) Technically repeat(1) (fail_if_no_progress ...) is a bad pattern, I think, because repeat repeats until any failure, then rewinds. We should probably only be repeating until we stop making progress, and surface any other non-progress-related errors. repeat obscures the latter sort of error. (I'm also a little worried about fail_if_no_progress's main-goal-only focus when combined with repeat.) But, this is also a problem with group. So let's not hold up this functionality over that.

I've added the new lemmas/names from the above suggestion, including neg_one_zsmul in the forward direction, and tweaked the docstring to try to point users to abel earlier if it better suits their needs. Feel free to tweak it further! :)

Suggested change

/-- Auxiliary tactic for the `add_group` tactic. Calls the simplifier only. -/

syntax (name := aux_add_group₁) "aux_add_group₁" (location)? : tactic

macro_rules

| `(tactic| aux_add_group₁ $[at $location]?) =>

`(tactic| simp -decide -failIfUnchanged only

[addCommutatorElement_def, neg_add_rev, neg_zero, zsmul_neg, ← neg_zsmul,

add_zero, zero_add,

← natCast_zsmul, ← mul_zsmul',

Int.natCast_add, Int.natCast_mul, neg_neg,

zsmul_zero, zero_zsmul, one_zsmul,

← add_assoc,

← add_zsmul, ← add_one_zsmul, ← one_add_zsmul,

Mathlib.Tactic.Group.zsmul_trick,

Mathlib.Tactic.Group.zsmul_trick_zero,

Mathlib.Tactic.Group.zsmul_trick_zero',

zsmul_neg_trick, zsmul_neg_trick',

add_neg_cancel_right, neg_add_cancel_right,

neg_neg_trick,

sub_eq_add_neg,

tsub_self, sub_self, add_neg_cancel, neg_add_cancel]

$[at $location]?)

/-- Auxiliary tactic for the `add_group` tactic. Calls `ring_nf` to normalize scalars. -/

syntax (name := aux_add_group₂) "aux_add_group₂" (location)? : tactic

macro_rules

| `(tactic| aux_add_group₂ $[at $location]?) =>

`(tactic| ring_nf (ifUnchanged := .silent) $[at $location]?)

/-- `add_group` normalizes expressions in additive groups that occur in the goal. `add_group` does

not assume commutativity, instead using only the additive group axioms without any information about

which group is manipulated. If the goal is an equality, and after normalization the two sides are

equal, `add_group` closes the goal.

For multiplicative groups, use the `group` tactic instead.

For additive commutative groups, use the `abel` tactic instead.

* `add_group at l1 l2 ...` normalizes at the given locations.

Example:

```lean

example {G : Type} [AddGroup G] (a b c d : G) (h : c = (a + 2 • b) + (-(b + b) + (-a)) + d) :

a + c + (-d) = a := by

add_group at h -- normalizes `h` which becomes `h : c = d`

rw [h] -- the goal is now `a + d + (-d) = a`

add_group -- which is then normalized and closed

```

-/

syntax (name := add_group) "add_group" (location)? : tactic

macro_rules

| `(tactic| add_group $[$loc]?) =>

`(tactic| repeat (fail_if_no_progress (aux_add_group₁ $[$loc]? <;> aux_add_group₂ $[$loc]?)))

/--

`add_group` normalizes expressions in additive groups without assuming commutativity. Unlike

`abel`, which does take advantage of commutativity, `add_group` instead only uses the additive

group axioms without any information about which group is manipulated. If the goal is an equality,

and after normalization the two sides are equal, `add_group` closes the goal.

`add_group at l1 l2 ...` normalizes at the given locations.

For additive commutative groups, use the `abel` tactic instead.

For multiplicative groups, use the `group` tactic instead.

Example:

```lean

example {G : Type} [AddGroup G] (a b c d : G) (h : c = (a + 2 • b) + (-(b + b) + (-a)) + d) :

a + c + (-d) = a := by

add_group at h -- normalizes `h` which becomes `h : c = d`

rw [h] -- the goal is now `a + d + (-d) = a`

add_group -- which is then normalized and closed

```

-/

syntax (name := addGroup) "add_group" (location)? : tactic

macro_rules

| `(tactic| add_group $[$loc]?) => do

let simpTacStx ←

`(tactic| simp -decide -failIfUnchanged only

[addCommutatorElement_def, neg_add_rev, neg_zero, zsmul_neg, ← neg_zsmul,

add_zero, zero_add,

← natCast_zsmul, ← mul_zsmul',

Int.natCast_add, Int.natCast_mul,

neg_neg,

zsmul_zero, zero_zsmul, one_zsmul,

← add_assoc,

← add_zsmul, ← add_one_zsmul, ← one_add_zsmul,

neg_one_zsmul,

Mathlib.Tactic.Group.zsmul_trick,

Mathlib.Tactic.Group.zsmul_trick_zero,

Mathlib.Tactic.Group.zsmul_trick_zero',

Mathlib.Tactic.AddGroup._zsmul_neg_trick,

Mathlib.Tactic.AddGroup._neg_zsmul_trick,

Mathlib.Tactic.AddGroup._neg_neg_trick,

Mathlib.Tactic.AddGroup._add_zsmul_neg_trick,

Mathlib.Tactic.AddGroup._add_neg_zsmul_trick,

Mathlib.Tactic.AddGroup._add_neg_neg_trick,

add_neg_cancel_right, neg_add_cancel_right,

sub_eq_add_neg,

tsub_self, sub_self, add_neg_cancel, neg_add_cancel]

$[$loc]?)

/- First, we simplify with a custom simp set, then use `ring_nf`. If neither make progress, we

stop. If we do not make any progress at all, we fail. -/

`(tactic| first

| repeat1 (fail_if_no_progress ($simpTacStx <;> ring_nf (ifUnchanged := .silent) $[$loc]?))

| fail "`add_group` made no progress")

thorimur · 2026-04-24T20:43:59Z

+Other than this issue, this is a direct port from Thomas Browning and Patrick Massot's `group`
+tactic.


Technically, after these changes, it will be a little different... :)

Suggested change

Other than this issue, this is a direct port from Thomas Browning and Patrick Massot's `group`

tactic.

Other than this issue, the strategy parallels Thomas Browning and Patrick Massot's `group`

tactic.

thorimur · 2026-04-24T20:56:39Z

+public import Mathlib.Algebra.Order.Sub.Basic
+public meta import Mathlib.Tactic.FailIfNoProgress
+public import Mathlib.Tactic.Group
+public import Mathlib.Tactic.Ring


As far as I can see this is the only import we need. But maybe should keep the other two in comments if they provide the other lemmas, in case that changes in the future?

Do you know if that is indeed why they're present, or were the imports LLM-generated as well?

Suggested change

public import Mathlib.Algebra.Order.Sub.Basic

public meta import Mathlib.Tactic.FailIfNoProgress

public import Mathlib.Tactic.Group

public import Mathlib.Tactic.Ring

public import Mathlib.Tactic.Group

thorimur · 2026-04-24T20:59:21Z

+
+variable {G : Type} [AddGroup G]
+
+attribute [instance] addCommutatorElement


The fact that something like open scoped (add)commutatorElement doesn't work is surely an oversight in the source file for addCommutatorElement, right (given the docstring)? Can we fix that (possibly in another PR)?

Aha, great! :)

So let's wait for that to be merged then change this to

Suggested change

attribute [instance] addCommutatorElement

open scoped addCommutatorElement

thorimur · 2026-04-24T20:59:58Z

+example (n : ℕ) (a : G) : (n - n) • a = 0 := by add_group
+
+example (n : ℤ) (a : G) : (n - n) • a = 0 := by add_group
+


Let's add these tests, which failed without the new extra three lemmas + neg_one_zsmul added in another suggestion.

Suggested change

example (b : G) {n : ℤ} : (-b) + n • b = (n - 1) • b := by add_group

example (b : G) : (-b) + (-b) = (-2) • b := by add_group

example (b : G) {n : ℤ} : n • b + (-b) = (n - 1) • b := by add_group

example (b : G) : -b = (-1) • b := by add_group

thorimur · 2026-04-24T21:00:40Z

+set_option linter.unusedTactic false in
+example (x : G) (h : x = 0) : x = 0 := by
+  add_group
+  exact h


Given other suggestions:

Suggested change

set_option linter.unusedTactic false in

example (x : G) (h : x = 0) : x = 0 := by

add_group

exact h

/--

error: `add_group` made no progress

G : Type

inst✝ : AddGroup G

x : G

h : x = 0

⊢ x = 0

-/

#guard_msgs in

example (x : G) (h : x = 0) : x = 0 := by

add_group

thorimur · 2026-04-24T21:26:54Z

+`(-1 : ℤ) • a` because `(-1 : ℤ)` is itself `-(1 : ℤ)`, causing simp to loop (since `ℤ` is also
+an `AddGroup`). Instead, we handle negation via `neg_add_rev` to distribute negation over sums,
+`zsmul_neg`/`neg_zsmul` for `n • (-a)`, and custom trick lemmas for combining `-b` with adjacent
+`zsmul` terms.


(See other comments)

Suggested change

`zsmul` terms.

`zsmul` terms. We also use `neg_one_zsmul` in the forward direction to normalize `(-1) • b` to `-b`.

kbuzzard added 2 commits March 23, 2026 23:41

feat: add_group tactic

f7ce1e1

add comment about missing test

d4b5fd4

github-actions Bot added the t-meta Tactics, attributes or user commands label Mar 24, 2026

kbuzzard commented Mar 24, 2026

View reviewed changes

Comment thread Mathlib/Tactic/AddGroup.lean Outdated

kbuzzard added 3 commits March 24, 2026 00:13

Update Mathlib/Tactic/AddGroup.lean

fd50164

remove comment on import

e9784ff

add porting comment

ded7d69

vihdzp added the LLM-generated PRs with substantial input from LLMs - review accordingly label Mar 24, 2026

lake exe mk_all

0154b20

kbuzzard commented Mar 24, 2026

View reviewed changes

Comment thread Mathlib/Tactic/AddGroup.lean Outdated

kbuzzard added 3 commits March 24, 2026 00:26

Update Mathlib/Tactic/AddGroup.lean

f34b14c

add sub_eq_add_neg

5667632

:Merge remote-tracking branch 'refs/remotes/origin/kbuzzard-add-group…

f5e8307

…' into kbuzzard-add-group

mathlib-triage Bot assigned JovanGerb Mar 25, 2026

mathlib-triage Bot unassigned JovanGerb Apr 16, 2026

mathlib-merge-conflicts Bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Apr 17, 2026

Merge branch 'master' into kbuzzard-add-group

009e48a

github-actions Bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Apr 17, 2026

sync with leanprover-community#31597

0641e04

SnirBroshi reviewed Apr 20, 2026

View reviewed changes

Comment thread MathlibTest/AddGroup.lean Outdated

kbuzzard and others added 5 commits April 22, 2026 12:35

Update MathlibTest/AddGroup.lean

bfb5373

Co-authored-by: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>

open addCommutatorElement in test

e722b15

Merge branch 'master' into kbuzzard-add-group

e6af49a

commutator example compiling; tactic failing

639563d

tactic now uses addCommutatorElement_def

a8e574c

mathlib-triage Bot assigned thorimur Apr 23, 2026

thorimur reviewed Apr 24, 2026

View reviewed changes

thorimur added the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 25, 2026

	Authors: Thomas Browning, Patrick Massot, Kevin Buzzard
	Authors: Kevin Buzzard

		Other than this issue, this is a direct port from Thomas Browning and Patrick Massot's `group`
		tactic.


		variable {G : Type} [AddGroup G]

		attribute [instance] addCommutatorElement

	attribute [instance] addCommutatorElement
	open scoped addCommutatorElement

		example (n : ℕ) (a : G) : (n - n) • a = 0 := by add_group

		example (n : ℤ) (a : G) : (n - n) • a = 0 := by add_group

+example (b : G) {n : ℤ} : (-b) + n • b = (n - 1) • b := by add_group
+example (b : G) : (-b) + (-b) = (-2) • b := by add_group
+example (b : G) {n : ℤ} : n • b + (-b) = (n - 1) • b := by add_group
+example (b : G) : -b = (-1) • b := by add_group

	`zsmul` terms.
	`zsmul` terms. We also use `neg_one_zsmul` in the forward direction to normalize `(-1) • b` to `-b`.

Conversation

kbuzzard commented Mar 24, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions Bot commented Mar 24, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 028964f2c6

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

Uh oh!

mathlib-merge-conflicts Bot commented Apr 17, 2026

Uh oh!

Uh oh!

thorimur left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

thorimur Apr 24, 2026

Choose a reason for hiding this comment

Uh oh!

thorimur Apr 24, 2026

Choose a reason for hiding this comment

Uh oh!

thorimur Apr 24, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

thorimur Apr 24, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

thorimur Apr 24, 2026

Choose a reason for hiding this comment

Uh oh!

thorimur Apr 24, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

thorimur Apr 24, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

SnirBroshi Apr 24, 2026

Choose a reason for hiding this comment

Uh oh!

thorimur Apr 25, 2026

Choose a reason for hiding this comment

Uh oh!

thorimur Apr 24, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

thorimur Apr 24, 2026

Choose a reason for hiding this comment

Uh oh!

thorimur Apr 24, 2026

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

kbuzzard commented Mar 24, 2026 •

edited

Loading

github-actions Bot commented Mar 24, 2026 •

edited

Loading

thorimur left a comment •

edited

Loading

thorimur Apr 24, 2026 •

edited

Loading

thorimur Apr 24, 2026 •

edited

Loading

thorimur Apr 24, 2026 •

edited

Loading

thorimur Apr 24, 2026 •

edited

Loading

thorimur Apr 24, 2026 •

edited

Loading