Lemmas.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 8 curated AI-written annotations and 1204 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 project documentation, Pinned FLT blueprint introduction

31 declarations, 0 contain sorry, 0 declared as axioms

Miscellaneous lemmas for the patching folder

Generic algebraic lemmas (units of products, ideals of quotient rings, products of submodules, etc.) used throughout the patching argument.

Imports (13)

Imported by 3 files

lemma IsUnit.pi_iff line 32 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monoid, Iff, IsUnit
Proof uses: Eq.mpr, Exists, And, Eq, HMul.hMul, OfNat.ofNat, id, congr, congrArg, forall_congr, congrFun', funext, Iff.symm, Classical.skolem
11 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma forall_prod_iff line 37 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nonempty, Iff
Proof uses: Iff.intro, Eq.mp, dite, Eq, Classical.decEq, Eq.rec, Not, Nonempty.some, inferInstance, congrArg, dite_eq_left_of_eq_true, eq_self

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
def Ideal.idealQuotientEquiv Bijection between ideals of R / I and ideals of R containing I, via comap/map along the quotient map line 46 source
Source documentation
Bijection between ideals of R / I and ideals of R containing I, via comap/map along the quotient map.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Ideal, Equiv, HasQuotient.Quotient, Subtype, LE.le
Proof uses: Equiv.mk, Subtype.mk, Ideal.comap, RingHom, Ideal.Quotient.mk, Ideal.map
30 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
def Ideal.idealQuotientEquiv {R : Type*} [CommRing R] (I : Ideal R) :
  Ideal (R ⧸ I) ≃ { J // I ≤ J } where
…
```
def Submodule.pi' The product of a family of submodules N i ≤ M i, viewed as a submodule of Π i, M i over the product ring Π i, R i line 64 source
Source documentation
The product of a family of submodules N i ≤ M i, viewed as a submodule of Π i, M i over the product ring Π i, R i.

standard axioms: Quot.sound, propext what this means
Statement uses: CommRing, AddCommGroup, Module, Submodule
Proof uses: Submodule.mk, AddSubmonoid.mk, AddSubsemigroup.mk, Set.ofPred, Membership.mem
21 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
def Submodule.pi' : Submodule (Π i, R i) (Π i, M i) where
…
```
lemma Submodule.mem_pi' line 72 source
standard axioms: Quot.sound, propext what this means
Statement uses: CommRing, AddCommGroup, Module, Submodule, Iff, Membership.mem, Submodule.pi'
Proof uses: Iff.rfl
16 instances, coercions and auxiliary constants left out.
def LinearMap.piMap' A more dependent version of LinearMap.piMap, making a product of linear maps into a linear map over the product of rings line 78 source
Source documentation
A more dependent version of LinearMap.piMap, making a product of linear maps into a linear map over the product of rings.

standard axioms: Quot.sound what this means
Statement uses: CommRing, AddCommGroup, Module, LinearMap, RingHom.id
Proof uses: LinearMap.mk, AddHom.mk
23 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
def LinearMap.piMap' (f : ∀ i, M i →ₗ[R i] N i) : (Π i, M i) →ₗ[Π i, R i] Π i, N i where
…
```
instance (instance at line 83) line 83 source
lemma pi'_jacobson line 89 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Eq, Submodule, Submodule.pi', Ideal.jacobson, Bot.bot, Ideal
Proof uses: Ideal.ext, Eq.mpr, Iff, Membership.mem, IsUnit, HAdd.hAdd, HMul.hMul, OfNat.ofNat, id, congr, congrArg, Eq.trans, forall_congr, Eq.rec, Eq.refl, propext, forall_comm, Iff.symm, forall_prod_iff
46 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
instance (instance at line 96) line 96 source
theorem exists_subgroup_isOpen_and_subset line 102 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, CompactSpace, T2Space, TotallyDisconnectedSpace, CommGroup, IsTopologicalGroup, Set, Membership.mem, Filter, nhds, OfNat.ofNat, Exists, Subgroup, And, IsOpen, LE.le
Proof uses: Iff.mp, mem_nhds_iff, IsClopen, compact_exists_isClopen_in_isOpen, OpenSubgroup, IsTopologicalGroup.exist_openSubgroup_sub_clopen_nhds_of_one, Subsemigroup.carrier, Submonoid.toSubsemigroup, Subgroup.toSubmonoid, OpenSubgroup.mk, Exists.intro, And.intro, LE.le.trans
38 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
theorem TwoSidedIdeal.span_le' line 112 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NonUnitalNonAssocRing, Set, TwoSidedIdeal, Iff, LE.le, TwoSidedIdeal.span
Proof uses: Iff.intro, LE.le.trans, TwoSidedIdeal.subset_span, Membership.mem, Iff.mp, TwoSidedIdeal.mem_span_iff
18 instances, coercions and auxiliary constants left out.
theorem TwoSidedIdeal.span_neg line 117 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NonUnitalNonAssocRing, Set, Eq, TwoSidedIdeal, TwoSidedIdeal.span, Neg.neg
Proof uses: le_antisymm, Eq.mpr, LE.le, id, congrArg, propext, TwoSidedIdeal.span_le', Membership.mem, Eq.rec, TwoSidedIdeal.neg_mem, TwoSidedIdeal.subset_span, neg_neg, Iff.mpr, Set.neg, Set.neg_mem_neg
21 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
theorem TwoSidedIdeal.span_singleton_zero line 126 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NonUnitalNonAssocRing, Eq, TwoSidedIdeal, TwoSidedIdeal.span, Singleton.singleton, Set, OfNat.ofNat, Bot.bot
Proof uses: Iff.mp, LE.le, le_bot_iff, Iff.mpr, TwoSidedIdeal.span_le', of_eq_true
28 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem TwoSidedIdeal.mem_span_singleton line 130 source
standard axioms: Quot.sound, propext what this means
Statement uses: NonUnitalNonAssocRing, Membership.mem, TwoSidedIdeal, TwoSidedIdeal.span, Singleton.singleton, Set
Proof uses: TwoSidedIdeal.subset_span, rfl
4 instances, coercions and auxiliary constants left out.
def TwoSidedIdeal.leAddSubgroup The largest two-sided ideal contained in a given additive subgroup G ≤ α: those x ∈ α whose two-sided span is contained in G line 136 source
Source documentation
The largest two-sided ideal contained in a given additive subgroup G ≤ α: those x ∈ α whose two-sided span is contained in G.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NonUnitalNonAssocRing, AddSubgroup, TwoSidedIdeal
Proof uses: TwoSidedIdeal.mk', Set.ofPred, LE.le, Set, TwoSidedIdeal.span, Singleton.singleton, Membership.mem
15 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
def TwoSidedIdeal.leAddSubgroup {α} [NonUnitalNonAssocRing α] (G : AddSubgroup α) :
    TwoSidedIdeal α :=
…
```
lemma TwoSidedIdeal.leAddSubgroup_subset line 157 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NonUnitalNonAssocRing, AddSubgroup, LE.le, Set, TwoSidedIdeal, TwoSidedIdeal.leAddSubgroup
Proof uses: Membership.mem, Eq.rec, Eq, TwoSidedIdeal.span, Singleton.singleton, TwoSidedIdeal.mem_span_singleton, HSub.hSub, OfNat.ofNat, Eq.symm, sub_zero
21 instances, coercions and auxiliary constants left out.
lemma TwoSidedIdeal.mem_leAddSubgroup' line 161 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NonUnitalNonAssocRing, AddSubgroup, Iff, Membership.mem, TwoSidedIdeal, TwoSidedIdeal.leAddSubgroup, LE.le, Set, TwoSidedIdeal.span, Singleton.singleton
Proof uses: Eq.mpr, HSub.hSub, OfNat.ofNat, id, Eq, Eq.rec, Eq.refl, Eq.trans, congrArg, Eq.symm, sub_zero, Iff.rfl
25 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma TwoSidedIdeal.mem_leAddSubgroup line 166 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Ring, AddSubgroup, Iff, Membership.mem, TwoSidedIdeal, TwoSidedIdeal.leAddSubgroup, HMul.hMul
Proof uses: Iff.intro, TwoSidedIdeal.mul_mem_right, TwoSidedIdeal.span, Singleton.singleton, Set, HSub.hSub, OfNat.ofNat, TwoSidedIdeal.mul_mem_left, Eq.rec, Eq, TwoSidedIdeal.mem_span_singleton, Eq.symm, sub_zero, Eq.mpr, id, Eq.mp, congrArg, Eq.trans, congrFun', one_mul and 28 more
72 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
theorem exists_twoSidedIdeal_isOpen_and_subset line 178 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, CompactSpace, T2Space, TotallyDisconnectedSpace, Ring, IsTopologicalRing, Set, Membership.mem, Filter, nhds, OfNat.ofNat, Exists, TwoSidedIdeal, And, IsOpen, LE.le
Proof uses: AddSubgroup, exists_addSubgroup_isOpen_and_subset, Exists.intro, TwoSidedIdeal.leAddSubgroup, And.intro, Iff.mpr, isOpen_iff_mem_nhds, HMul.hMul, Iff.mp, TwoSidedIdeal.mem_leAddSubgroup, IsCompact, IsCompact.induction_on, Eq.mpr, EmptyCollection.emptyCollection, id, Eq, congrArg, funext, Eq.trans, True and 41 more
58 instances, coercions and auxiliary constants left out.

Tactic trace: 40 steps
Open to load the checked before-and-after goal states.
theorem exists_ideal_isOpen_and_subset line 222 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, CompactSpace, T2Space, TotallyDisconnectedSpace, Ring, IsTopologicalRing, Set, Membership.mem, Filter, nhds, OfNat.ofNat, Exists, Ideal, And, IsOpen, LE.le
Proof uses: TwoSidedIdeal, exists_twoSidedIdeal_isOpen_and_subset, Exists.intro, OrderHom, TwoSidedIdeal.asIdeal, And.intro
32 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
instance (instance at line 229) line 229 source
lemma WellFoundedGT.exists_eq_sup line 235 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CompleteLattice, WellFoundedGT, OrderHom, Nat, Exists, Eq, iSup
Proof uses: LE.le, Iff.mp, wellFoundedGT_iff_monotone_chain_condition, Exists.intro, le_antisymm, le_iSup, iSup_le, Or.elim, le_total, OrderHom.monotone', Eq.ge
29 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma WellFoundedLT.exists_eq_inf line 241 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CompleteLattice, WellFoundedLT, OrderHom, Nat, OrderDual, Exists, Eq, iInf
Proof uses: WellFoundedGT.exists_eq_sup
23 instances, coercions and auxiliary constants left out.
lemma IsLocalRing.maximalIdeal_pow_card_smul_top_le line 246 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsLocalRing, IsNoetherianRing, AddCommGroup, Module, Submodule, Finite, HasQuotient.Quotient, LE.le, HSMul.hSMul, Ideal, HPow.hPow, Nat, IsLocalRing.maximalIdeal, Nat.card, Top.top
Proof uses: Submodule.smul_mono, Ideal.pow_le_pow_right, le_rfl, Exists, Eq, Bot.bot, OrderDual, OrderHom, OrderHom.mk, iInf, WellFoundedLT.exists_eq_inf, Ideal.iInf_pow_smul_eq_bot_of_isLocalRing, Ideal.IsMaximal.ne_top, Exists.intro, id, Eq.mp, congrArg, Set.ncard, HAdd.hAdd, HSub.hSub and 60 more
176 instances, coercions and auxiliary constants left out.

Tactic trace: 32 steps
Open to load the checked before-and-after goal states.
theorem Submodule.comap_smul_of_le_range line 288 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, AddCommGroup, Module, LinearMap, RingHom.id, Submodule, LE.le, LinearMap.range, Ideal, Eq, Submodule.comap, HSMul.hSMul, Max.max, LinearMap.ker
Proof uses: Eq.mpr, Submodule.map, id, congrArg, Eq.symm, Submodule.comap_map_eq, Submodule.map_smul'', Min.min, Submodule.map_comap_eq, Iff.mpr, inf_eq_right, Eq.refl
46 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem Submodule.comap_smul_of_surjective line 294 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, AddCommGroup, Module, LinearMap, RingHom.id, Submodule, Function.Surjective, Ideal, Eq, Submodule.comap, HSMul.hSMul, Max.max, LinearMap.ker
Proof uses: Submodule.comap_smul_of_le_range, LE.le.trans_eq, Top.top, LinearMap.range, le_top, Eq.symm, LinearMap.range_eq_top_of_surjective
32 instances, coercions and auxiliary constants left out.
def Pi.liftQuotientₗ line 303 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, AddCommGroup, Module, Finite, LinearMap, RingHom.id, Ideal, HasQuotient.Quotient, Submodule, HSMul.hSMul, Top.top
Proof uses: LinearMap.comp, LinearMap.ker, LinearMap.compLeft, Algebra.linearMap, Submodule.liftQ, Submodule.mkQ, LinearEquiv.symm, LinearMap.quotKerEquivOfSurjective
53 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
lemma Pi.liftQuotientₗ_surjective line 321 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, AddCommGroup, Module, Finite, LinearMap, RingHom.id, Ideal, Function.Surjective, HasQuotient.Quotient, Submodule, HSMul.hSMul, Top.top, Pi.liftQuotientₗ
Proof uses: Eq.mpr, LinearMap.ker, LinearMap.compLeft, Algebra.linearMap, Submodule.liftQ, LinearMap.comp, Submodule.mkQ, id, Eq, LinearEquiv, LinearEquiv.symm, LinearMap.quotKerEquivOfSurjective, LinearMap.range, congrArg, Eq.symm, propext, LinearMap.range_eq_top, Submodule.range_liftQ, Function.Surjective.comp, Submodule.mkQ_surjective
63 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Pi.liftQuotientₗ_bijective line 328 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, AddCommGroup, Module, Finite, LinearMap, RingHom.id, Ideal, Function.Surjective, LE.le, Submodule, LinearMap.ker, HasQuotient.Quotient, LinearMap.compLeft, Algebra.linearMap, Function.Bijective, HSMul.hSMul, Top.top, Pi.liftQuotientₗ
Proof uses: And.intro, Function.Injective, Eq.mpr, Submodule.liftQ, LinearMap.comp, Submodule.mkQ, id, Eq, LinearEquiv, LinearEquiv.symm, LinearMap.quotKerEquivOfSurjective, Bot.bot, congrArg, Eq.symm, propext, LinearMap.ker_eq_bot, Submodule.map, Submodule.ker_liftQ, le_bot_iff, Submodule.comap and 25 more
101 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma IsModuleTopology.compactSpace line 343 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, TopologicalSpace, AddCommGroup, Module, IsModuleTopology, CompactSpace, Module.Finite
Proof uses: CompactSpace.mk, Submodule.isCompact_of_fg, IsModuleTopology.toContinuousAdd, Top.top, Submodule, Module.Finite.fg_top
37 instances, coercions and auxiliary constants left out.
lemma disjoint_nonZeroDivisors_of_mem_minimalPrimes line 350 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Ideal, Membership.mem, Set, minimalPrimes, Disjoint, Submonoid, nonZeroDivisors
Proof uses: Eq.mpr, LE.le, Compl.compl, id, Eq, congrArg, Eq.symm, propext, Set.subset_compl_iff_disjoint_right, Set.subset_def, Exists, HMul.hMul, OfNat.ofNat, Not, forall_congr, implies_congr, Eq.trans, funext, Ideal.IsPrime, And.left and 51 more
138 instances, coercions and auxiliary constants left out.

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