S02_Proving_Identities_in_Algebraic_Structures.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 9 curated AI-written annotations and 7 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned Mathematics in Lean documentation, Pinned Mathematics in Lean textbook

25 declarations, 12 contain sorry, 0 declared as axioms

Imports (3)

Imported by 1 file

MIL.lean

example (example at line 24) line 24 source
example (example at line 26) line 26 source
example (example at line 28) line 28 source
example (example at line 30) line 30 source
theorem MyRing.add_zero a + 0 = a in any ring, from commutativity and zero_add line 39 source
L4DEL explanation
Swap the two summands, then use the left-identity law that is already available.
1. The goal is a + 0 = a for an element a of a ring R.
2. rw [add_comm] turns a + 0 into 0 + a.
3. rw [zero_add] turns 0 + a into a, leaving a = a, which rw closes by rfl.
4. The theorem lives in namespace MyRing so that it does not clash with the library's own add_zero; the #check lines after it show how the two names are told apart.
Sources and attribution: Pinned Lean source (dd6d752fedb1)
no axioms what this means
Statement uses: Ring, Eq, HAdd.hAdd, OfNat.ofNat
Proof uses: Eq.mpr, id, congrArg, add_comm, zero_add, Eq.refl
28 instances, coercions and auxiliary constants left out.

namespace: a prefix that groups names, so that MyRing.add_zero and the library's add_zero are different declarations.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem add_zero (a : R) : a + 0 = a := by rw [add_comm, zero_add]
```
theorem MyRing.add_neg_cancel line 41 source
standard axioms: propext what this means
Statement uses: Ring, Eq, HAdd.hAdd, Neg.neg, OfNat.ofNat
Proof uses: Eq.mpr, id, congrArg, add_comm, neg_add_cancel, Eq.refl
42 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem MyRing.neg_add_cancel_left line 51 source
standard axioms: propext what this means
Statement uses: Ring, Eq, HAdd.hAdd, Neg.neg
Proof uses: Eq.mpr, id, congrArg, Eq.symm, add_assoc, OfNat.ofNat, neg_add_cancel, zero_add, Eq.refl
34 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem MyRing.add_neg_cancel_right Prove these: sorry line 55 source
Source comment
Prove these:

depends on sorry what this means
Statement uses: Ring, Eq, HAdd.hAdd, Neg.neg
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat
21 instances, coercions and auxiliary constants left out.

Distinct definitions of this name: MIL/C02_Basics/solutions/Solutions_S02_Proving_Identities_in_Algebraic_Structures.lean:8 (same statement text; different proof or body). Qualify references as MyRing.add_neg_cancel_right@path.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem add_neg_cancel_right (a b : R) : a + b + -b = a := by
…
```
theorem MyRing.add_left_cancel Exercise: left cancellation of addition (sorry) sorry line 58 source
L4DEL explanation
If a + b = a + c then b = c; here the proof is left as a sorry for the reader.
1. This declaration is an exercise: its body is sorry, so Lean accepts it only with a warning and nothing is proved.
2. The statement takes h : a + b = a + c and asks for b = c in a ring R.
3. The preceding theorem MyRing.neg_add_cancel_left, -a + (a + b) = b, is the natural tool for the exercise.
See also: MyRing.neg_add_cancel_left
Sources and attribution: Pinned Lean source (dd6d752fedb1)
depends on sorry what this means
Statement uses: Ring, Eq, HAdd.hAdd
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat
9 instances, coercions and auxiliary constants left out.

Distinct definitions of this name: MIL/C02_Basics/solutions/Solutions_S02_Proving_Identities_in_Algebraic_Structures.lean:11 (same statement text; different proof or body). Qualify references as MyRing.add_left_cancel@path.

sorry: a placeholder proof; Lean accepts it but reports a warning, because nothing has actually been proved.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem add_left_cancel {a b c : R} (h : a + b = a + c) : b = c := by
…
```
theorem MyRing.add_right_cancel sorry line 61 source
depends on sorry what this means
Statement uses: Ring, Eq, HAdd.hAdd
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat
9 instances, coercions and auxiliary constants left out.

Distinct definitions of this name: MIL/C02_Basics/solutions/Solutions_S02_Proving_Identities_in_Algebraic_Structures.lean:14 (same statement text; different proof or body). Qualify references as MyRing.add_right_cancel@path.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem MyRing.mul_zero a * 0 = 0 via cancellation line 64 source
L4DEL explanation
Show a*0 + a*0 equals a*0 + 0, then cancel one a*0 from the left.
1. have h : a * 0 + a * 0 = a * 0 + 0 states the equation to be cancelled.
2. Inside h, rw [← mul_add] rewrites a * 0 + a * 0 into a * (0 + 0), then two uses of add_zero remove the trailing + 0 on each side, so both sides agree.
3. rw [add_left_cancel h] finishes the goal by cancelling the left summand.
4. In this exercise file add_left_cancel is itself a sorry exercise, so this proof only stands once that exercise is solved; the solutions file proves it.
See also: MyRing.add_zero
Sources and attribution: Pinned Lean source (dd6d752fedb1)
depends on sorry what this means
Statement uses: Ring, Eq, HMul.hMul, OfNat.ofNat
Proof uses: HAdd.hAdd, Eq.mpr, id, congrArg, Eq.symm, mul_add, MyRing.add_zero, Eq.refl, MyRing.add_left_cancel
17 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
theorem mul_zero (a : R) : a * 0 = 0 := by
…
```
theorem MyRing.zero_mul sorry line 69 source
depends on sorry what this means
Statement uses: Ring, Eq, HMul.hMul, OfNat.ofNat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, Nat
15 instances, coercions and auxiliary constants left out.

Distinct definitions of this name: MIL/C02_Basics/solutions/Solutions_S02_Proving_Identities_in_Algebraic_Structures.lean:17 (same statement text; different proof or body). Qualify references as MyRing.zero_mul@path.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem MyRing.neg_eq_of_add_eq_zero sorry line 72 source
depends on sorry what this means
Statement uses: Ring, Eq, HAdd.hAdd, OfNat.ofNat, Neg.neg
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, Nat
27 instances, coercions and auxiliary constants left out.

Distinct definitions of this name: MIL/C02_Basics/solutions/Solutions_S02_Proving_Identities_in_Algebraic_Structures.lean:21 (same statement text; different proof or body). Qualify references as MyRing.neg_eq_of_add_eq_zero@path.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem MyRing.eq_neg_of_add_eq_zero sorry line 75 source
depends on sorry what this means
Statement uses: Ring, Eq, HAdd.hAdd, OfNat.ofNat, Neg.neg
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, Nat
27 instances, coercions and auxiliary constants left out.

Distinct definitions of this name: MIL/C02_Basics/solutions/Solutions_S02_Proving_Identities_in_Algebraic_Structures.lean:24 (same statement text; different proof or body). Qualify references as MyRing.eq_neg_of_add_eq_zero@path.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem MyRing.neg_zero line 78 source
depends on sorry what this means
Statement uses: Ring, Eq, Neg.neg, OfNat.ofNat
Proof uses: MyRing.neg_eq_of_add_eq_zero, Eq.mpr, HAdd.hAdd, id, congrArg, MyRing.add_zero, Eq.refl
17 instances, coercions and auxiliary constants left out.

Also declared: MIL/C02_Basics/solutions/Solutions_S02_Proving_Identities_in_Algebraic_Structures.lean:29 (same declaration text).

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem MyRing.neg_neg sorry line 82 source
depends on sorry what this means
Statement uses: Ring, Eq, Neg.neg
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat
13 instances, coercions and auxiliary constants left out.

Distinct definitions of this name: MIL/C02_Basics/solutions/Solutions_S02_Proving_Identities_in_Algebraic_Structures.lean:33 (same statement text; different proof or body). Qualify references as MyRing.neg_neg@path.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
example (example at line 91) line 91 source
example (example at line 96) line 96 source
example (example at line 99) line 99 source
theorem MyRing.self_sub sorry line 105 source
depends on sorry what this means
Statement uses: Ring, Eq, HSub.hSub, OfNat.ofNat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, Nat
19 instances, coercions and auxiliary constants left out.

Distinct definitions of this name: MIL/C02_Basics/solutions/Solutions_S02_Proving_Identities_in_Algebraic_Structures.lean:42 (same statement text; different proof or body). Qualify references as MyRing.self_sub@path.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem MyRing.one_add_one_eq_two line 108 source
standard axioms: propext what this means
Statement uses: Ring, Eq, HAdd.hAdd, OfNat.ofNat, Nat
Proof uses: Mathlib.Meta.NormNum.isNat_eq_true, Mathlib.Meta.NormNum.isNat_add, Eq.refl, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_one, Mathlib.Meta.NormNum.instAtLeastTwo
29 instances, coercions and auxiliary constants left out.

Also declared: MIL/C02_Basics/solutions/Solutions_S02_Proving_Identities_in_Algebraic_Structures.lean:45 (same declaration text).

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem MyRing.two_mul sorry line 111 source
depends on sorry what this means
Statement uses: Ring, Eq, HMul.hMul, OfNat.ofNat, Nat, HAdd.hAdd
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
26 instances, coercions and auxiliary constants left out.

Distinct definitions of this name: MIL/C02_Basics/solutions/Solutions_S02_Proving_Identities_in_Algebraic_Structures.lean:48 (same statement text; different proof or body). Qualify references as MyRing.two_mul@path.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem MyGroup.mul_inv_cancel sorry line 134 source
depends on sorry what this means
Statement uses: Group, Eq, HMul.hMul, Inv.inv, OfNat.ofNat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, Nat
25 instances, coercions and auxiliary constants left out.

Distinct definitions of this name: MIL/C02_Basics/solutions/Solutions_S02_Proving_Identities_in_Algebraic_Structures.lean:58 (same statement text; different proof or body). Qualify references as MyGroup.mul_inv_cancel@path.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem MyGroup.mul_one sorry line 137 source
depends on sorry what this means
Statement uses: Group, Eq, HMul.hMul, OfNat.ofNat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, Nat
23 instances, coercions and auxiliary constants left out.

Distinct definitions of this name: MIL/C02_Basics/solutions/Solutions_S02_Proving_Identities_in_Algebraic_Structures.lean:63 (same statement text; different proof or body). Qualify references as MyGroup.mul_one@path.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem MyGroup.mul_inv_rev sorry line 140 source
depends on sorry what this means
Statement uses: Group, Eq, Inv.inv, HMul.hMul
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat
21 instances, coercions and auxiliary constants left out.

Distinct definitions of this name: MIL/C02_Basics/solutions/Solutions_S02_Proving_Identities_in_Algebraic_Structures.lean:66 (same statement text; different proof or body). Qualify references as MyGroup.mul_inv_rev@path.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.