GeometricallyReduced_isGeometricallyReduced_iff_of_separable_algebraic.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 348 curated AI-written annotations and 373 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 12 manuscript-grounded curated result annotations were composed from pinned companion PDFs and named source records in a Codex session on 2026-10-14; no human review is claimed, and the exact runtime model identifier was not exposed to the artifact generator. Twelve supporting declarations for the Hilbert-functions result were upgraded on 2026-10-14 from mechanically condensed doc comments to declaration-specific explanations bound to exact page-one terminology in the pinned human-written companion. The other Hilbert challenge statements were deliberately not described as companion-backed results because that manuscript proves P5 specifically. Fifteen previously unannotated declarations along the Hilbert P5 proof spine were annotated on 2026-10-14 from the pinned companion's seven-page argument, covering the two-generator decomposition, finite-difference bounds, critical-case reduction, and final log-concavity step. Each quotation is bound to its exact manuscript page and Lean declaration; no human review is claimed. Twenty-four further declarations along the Hilbert P5 box-count and finite-difference spine were annotated on 2026-10-14, covering the two-dimensional slice count, three-dimensional box formula, first- and second-difference identities, the seven-threshold curvature expression, boundary handling, pointwise transport, sum linearity, and lower-or-upper region classification. Every annotation is bound to an exact quotation on pages 2 or 3 of the pinned human-written companion; Lean-specific boundary and threshold helpers are identified as implementation lemmas rather than separate manuscript claims. No human review is claimed. Twenty-eight further declarations along the Hilbert P5 argument were annotated on 2026-10-14 from pages 2 through 6 of the pinned human-written companion. They expose the shifted residual sequence, exact lower- and upper-region formulas, symmetry by complementary divisors, the curvature-one and curvature-two splits, and the final algebraic reductions. Lean-only transport and integer-arithmetic helpers are labeled as proof infrastructure rather than new manuscript claims; each quotation is page-bound in the source ledger, and no human review is claimed. Twenty high-level declarations completing the Hilbert P5 curvature-one and curvature-two case spine were annotated on 2026-10-14 from pages 3 through 7 of the pinned human-written companion. The explanations separate cases A and B, lower and upper monomial regions, shifted residual evaluation, impossible mixed regions, and the surviving upper-upper estimate; wrapper lemmas are explicitly described as proof structure. Every quotation is page-bound, and no human review is claimed. Twenty-two graph-reconstruction declarations were upgraded or added on 2026-10-14 from the pinned four-page human-written companion, covering the incidence-deletion deck, edge and degree recovery, unique isolated vertices, vertex-type reconstruction, neighboring-type descent, adjacency recovery, and final bipartite isomorphism. The result annotation also records that `G_not_regular` is present in the Lean statement but unused by its proof term and absent from the companion theorem. Exact historical quotations from Paul J. Kelly (1957) and Bondy with Hemminger (1977) are linked separately; no human review is claimed. Eighteen declarations along the Erdős 741(i) strict-natural-density counterexample were added on 2026-10-14, covering the carry-free base-four digit split, full cross-sum coverage, sparse pure self-sums, fixed-factor fat intervals, the lower-scale density deficit, upper-scale sum growth, and the final convergence contradiction. The result annotation was corrected to distinguish the negative strict-natural-density Lean theorem from the compatible affirmative upper-density companion theorem; Ulam AI's written counterexample is explicitly identified as using a different interval length with the same mechanism. The quotations are page- and hash-bound where the PDFs expose text; Paul Erdős's scanned 1994 question was visually checked and is linked separately without a machine-audit claim. No human review is claimed. Twenty-eight additional declaration-level annotations were added on 2026-10-14 for the Erdős 12(i) proof, and its IsGood definition was upgraded from a source-comment condensation. They cover the prime and Chinese-remainder moduli, the actual Lean congruence-block witness, exclusion of cross-block and same-block triples, lower and upper counting bounds, and the positive liminf. The prior result annotation was corrected because the pinned human-written companion proves the same theorem with a different base-2-to-base-3 construction; it is no longer presented as the Lean proof. The original property-P definition from Erdős and Sárközy (1970) is separately linked and page-bound; no human review is claimed. The remaining fifty declarations in the Erdős 12(i) file were annotated on 2026-10-14, completing declaration-level coverage of all eighty definitions, lemmas, and theorems in that file. These additions expose the prime-recursion invariants, divisibility transport, Chinese-remainder witness bounds, numerical density envelopes, injective block coding, and liminf support lemmas instead of leaving the proof spine as raw Lean; no human review is claimed. Eighteen supporting declarations for Erdős 125 were added on 2026-10-14, completing all nineteen declarations in the file. The annotations follow the pinned companion through digit-block decomposition, irrational logarithmic approximation, the explicit Lean contraction factor 11/12, geometric iteration, and the lower-density conclusion. The original 1996 question of Burr, Erdős, Graham, and Li and the 2026 discussion contributions of GTSoukalas, Terence Tao, and Giuseppe Melfi are linked separately; no human review is claimed. Twenty-eight supporting declarations for Erdős 138 were upgraded or added on 2026-10-14, completing all twenty-nine declarations in the file. The annotations separate the greedy difference proof from the Lean-specific representation bridges and ultrafilter compactness proof of existence, and bind quotations from the pinned companion, the AlphaProof Nexus paper, Erdős's 1981 source, van der Waerden's recollection, and the 2026 Erdős Problems discussion. No human review is claimed. The curated Erdős 12(ii), 138, and 152 annotations were further linked on 2026-10-14 to exact quotations from Felix Behrend, Bartel van der Waerden, and Paul Erdős with Pál Turán; the historical quotation sources are labeled separately from the pinned AlphaProof proof companions. The curated Hilbert-functions result, its OrderIdeal and pureOSequence definitions, and the Erdős 846 annotation were further linked on 2026-10-14 to exact quotations from Richard P. Stanley and from Moe Putterman, Mehtaab Sawhney, and Gregory Valiant. The Stanley PDF is hash- and page-bound in the source ledger; these historical sources are labeled separately from the pinned AlphaProof proof companions. Three additional target-specific annotations for Ben Green's Problem 57, exact last-iterate anchored-GDA convergence, and Graffiti.pc Conjecture 2 were composed on 2026-10-14 from the exact pinned Lean statements, quotations from the AlphaProof Nexus paper, and quotations from Green, Ryu with Yuan and Yin, Surina et al., and Wang with Dai and Tong; no human review is claimed. Two additional target-specific quantum-optics annotations for the explicit AME(11,5) construction and the even N >= 4, D = N monochromatic-quantum-graph theorem were composed on 2026-10-14 from the exact pinned Lean statements, page-bound quotations from the AlphaProof Nexus paper, Helwig et al., and Krenn, Gu, and Zeilinger, and Mario Krenn's public priority correction. The AME annotation makes no first-discovery claim; the monochromatic annotation states that the local AlphaProof wrapper contains sorry and links the separate pinned proof-bearing Formal Conjectures artifact without silently treating it as local verification. Twelve declarations that the pinned source repeats verbatim in several files were annotated in only one of the copies, so the build rejected them as differing copies. On 2026-10-16 each curated annotation was copied unchanged to every identical copy: the eleven Hilbert-functions definitions from hilbert_functions_5 to hilbert_functions_1, _2, _3, _4, _7 and _8, and Erdos12.IsGood from erdos_12.parts.i to erdos_12.parts.ii (the better-sourced annotation was kept in each case). Each copy's quotations are bound in the source ledger like the original's; no new text was written and no human review is claimed. The remaining source-derived annotations were 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 source prose.

Credit: Google DeepMind published the AlphaProof Nexus proof artifacts. The pinned repository identifies the mathematical sources and collaborators, including OEIS, Erdős Problems, Gergely Bérczi, and Mario Krenn; those source records remain the authority for individual credit.

Project sources: Pinned AlphaProof Nexus results documentation, AlphaProof Nexus paper, Pinned human-written natural-language proof companions

60 declarations, 0 contain sorry, 0 declared as axioms

Imports (1)

Mathlib

class IsSeparablyGenerated line 40 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra
4 instances, coercions and auxiliary constants left out.

Also declared: APNOutputs/StacksProject/GeometricallyReduced_isReduced_tensorProduct_of_separable.lean:40 (same declaration text), APNOutputs/StacksProject/GeometricallyReduced_isReduced_tensorProduct_of_separablyGenerated.lean:40 (same declaration text), APNOutputs/StacksProject/Separability_exists_isPurelyInseparable_isSeparablyGenerated_of_essFiniteType.lean:40 (same declaration text).
class IsSeparableExtensionSP line 44 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra
4 instances, coercions and auxiliary constants left out.

Also declared: APNOutputs/StacksProject/GeometricallyReduced_isReduced_tensorProduct_of_separable.lean:44 (same declaration text), APNOutputs/StacksProject/GeometricallyReduced_isReduced_tensorProduct_of_separablyGenerated.lean:44 (same declaration text).
class IsSeparablyFinitelyGenerated line 47 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra
4 instances, coercions and auxiliary constants left out.

Distinct definitions of this name: APNOutputs/StacksProject/GeometricallyReduced_isReduced_tensorProduct_of_separable.lean:47 (same statement text; different proof or body), APNOutputs/StacksProject/GeometricallyReduced_isReduced_tensorProduct_of_separablyGenerated.lean:47 (same statement text; different proof or body). Qualify references as IsSeparablyFinitelyGenerated@path.
lemma reduced_quotient_directed_idempotents Helper lemma: quotient of a reduced ring by an idempotent is reduced line 62 source
Source comment
Helper lemma: quotient of a reduced ring by an idempotent is reduced.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsReduced, Ideal, Membership.mem, Exists, And, Eq, HMul.hMul, HasQuotient.Quotient
Proof uses: IsReduced.mk, Quot.ind, Submodule.quotientRel, IsNilpotent, OfNat.ofNat, Quot.mk, Nat, HPow.hPow, Iff.mp, RingHom, Ideal.Quotient.mk, Ideal.Quotient.eq_zero_iff_mem, Nat.casesAuxOn, pow_zero, Eq.mp, congrArg, Eq.symm, mul_one, Eq.mpr, id and 67 more
95 instances, coercions and auxiliary constants left out.

Tactic trace: 44 steps
Open to load the checked before-and-after goal states.
```
lemma reduced_quotient_directed_idempotents {R : Type*} [CommRing R] [IsReduced R]
    (I : Ideal R)
    (hI : ∀ x ∈ I, ∃ e ∈ I, e * e = e ∧ x = x * e) :
    IsReduced (R ⧸ I) := by
…
```
Mentions: R
lemma retract_reduced line 113 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, RingHom, Eq, RingHom.comp, RingHom.id, IsReduced
Proof uses: IsReduced.mk, IsNilpotent, IsNilpotent.map, OfNat.ofNat, IsReduced.eq_zero, Eq.mpr, id, congrArg, map_zero, Eq.refl, Trans.trans, rfl, Eq.mp
32 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma isAlgebraic_of_isSeparable line 126 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, Algebra.IsSeparable, Algebra.IsAlgebraic
23 instances, coercions and auxiliary constants left out.
lemma reduced_of_surjective_directed_idempotents line 132 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, RingHom, Function.Surjective, Eq, OfNat.ofNat, Exists, And, HMul.hMul, IsReduced
Proof uses: IsReduced.mk, IsNilpotent, Nat, HPow.hPow, Eq.mpr, id, congrArg, map_pow, Eq.refl, Nat.casesAuxOn, Trans.trans, Eq.symm, pow_zero, mul_one, MulZeroClass.mul_zero, HAdd.hAdd, GT.gt, Nat.succ, Nat.zero_lt_succ, HSub.hSub and 64 more
77 instances, coercions and auxiliary constants left out.

Tactic trace: 38 steps
Open to load the checked before-and-after goal states.
lemma ideal_generated_by_idempotents line 180 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Set, Ideal, Eq, Ideal.span, Membership.mem, Exists, And, HMul.hMul
Proof uses: Submodule.span_induction, Exists.intro, OfNat.ofNat, And.intro, Ideal.zero_mem, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.mul_congr, Mathlib.Tactic.Ring.cast_zero, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_zero, Mathlib.Tactic.Ring.zero_mul, Submodule, Submodule.span, HAdd.hAdd, HSub.hSub, Ideal.sub_mem, Ideal.add_mem, Ideal.mul_mem_left, Trans.trans, Nat and 50 more
72 instances, coercions and auxiliary constants left out.

Tactic trace: 43 steps
Open to load the checked before-and-after goal states.
lemma eval_poly_trick line 223 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, Polynomial, Polynomial.Separable, Eq, AlgHom, Polynomial.aeval, OfNat.ofNat, Exists, And, Polynomial.map, algebraMap, HMul.hMul, HSub.hSub, Polynomial.X, RingHom, Polynomial.C, IsCoprime
Proof uses: Polynomial.IsRoot, Eq.mpr, Polynomial.eval, id, congrArg, propext, Polynomial.IsRoot.def, Polynomial.eval₂, Polynomial.eval_map, Eq.symm, Polynomial.aeval_def, Dvd.dvd, Iff.mpr, Polynomial.dvd_iff_isRoot, Exists.intro, And.intro, Polynomial.Separable.map, Polynomial.Separable.isCoprime, Eq.mp
67 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
lemma eval_poly_idemp line 238 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, Polynomial, Polynomial.Separable, Eq, AlgHom, Polynomial.aeval, OfNat.ofNat, Exists, TensorProduct, And, HMul.hMul, HSub.hSub, TensorProduct.tmul
Proof uses: Polynomial.map, algebraMap, Polynomial.X, RingHom, Polynomial.C, IsCoprime, eval_poly_trick, HAdd.hAdd, Polynomial.aeval_X, Eq.mpr, id, congrArg, Polynomial.aeval_C, Algebra.TensorProduct.algebraMap_apply, CommSemiring, AddCommMonoid, Module, Eq.rec, Eq.refl, Polynomial.aeval_map_algebraMap and 74 more
159 instances, coercions and auxiliary constants left out.

Tactic trace: 67 steps
Open to load the checked before-and-after goal states.
lemma idemp_of_two line 310 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Eq, HMul.hMul, HSub.hSub, OfNat.ofNat, Exists, And, HAdd.hAdd
Proof uses: Exists.intro, Trans.trans, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Mathlib.Tactic.Ring.mul_congr, Mathlib.Tactic.Ring.atom_pf, Mathlib.Tactic.Ring.add_mul, Mathlib.Tactic.Ring.mul_add, Mathlib.Tactic.Ring.mul_pf_left, Mathlib.Tactic.Ring.mul_pf_right, Mathlib.Tactic.Ring.one_mul, Mathlib.Tactic.Ring.mul_zero, Mathlib.Tactic.Ring.add_pf_add_zero, Mathlib.Tactic.Ring.zero_mul, Mathlib.Tactic.Ring.mul_pp_pf_overlap, Mathlib.Meta.NormNum.IsNat.to_raw_eq, Mathlib.Meta.NormNum.isNat_add and 31 more
53 instances, coercions and auxiliary constants left out.

Tactic trace: 25 steps
Open to load the checked before-and-after goal states.
def u_elem line 338 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, IsScalarTower, TensorProduct
Proof uses: HSub.hSub, TensorProduct.tmul, RingHom, algebraMap, OfNat.ofNat
52 instances, coercions and auxiliary constants left out.
def I_rel line 343 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, IsScalarTower, Ideal, TensorProduct
Proof uses: Ideal.span, Set.range, u_elem
42 instances, coercions and auxiliary constants left out.
def S_ring line 348 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, IsScalarTower
Proof uses: HasQuotient.Quotient, TensorProduct, Ideal, I_rel
30 instances, coercions and auxiliary constants left out.
instance (instance at line 353) line 353 source
def fL_hom line 358 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, IsScalarTower, RingHom, S_ring
Proof uses: RingHom.comp, TensorProduct, HasQuotient.Quotient, Ideal, I_rel, Ideal.Quotient.mk, AlgHom.toRingHom, Algebra.TensorProduct.includeLeft
40 instances, coercions and auxiliary constants left out.
def fA_hom line 363 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, IsScalarTower, RingHom, S_ring
Proof uses: RingHom.comp, TensorProduct, HasQuotient.Quotient, Ideal, I_rel, Ideal.Quotient.mk, AlgHom.toRingHom, Algebra.TensorProduct.includeRight
39 instances, coercions and auxiliary constants left out.
lemma fL_fA_comm line 370 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, IsScalarTower, Commute, S_ring, RingHom, fL_hom, fA_hom
Proof uses: TensorProduct, TensorProduct.tmul, OfNat.ofNat, Commute.all, Commute.map, HasQuotient.Quotient, Ideal, I_rel, Ideal.Quotient.mk
60 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
def S_algebra_L line 379 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, IsScalarTower, S_ring
Proof uses: RingHom.toAlgebra, fL_hom
16 instances, coercions and auxiliary constants left out.
def S_algebra_A line 384 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, IsScalarTower, S_ring
Proof uses: RingHom.toAlgebra, fA_hom
16 instances, coercions and auxiliary constants left out.
def S_algebra_k' line 389 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, IsScalarTower, S_ring
Proof uses: RingHom.toAlgebra, RingHom.comp, fL_hom, algebraMap
17 instances, coercions and auxiliary constants left out.
def fL_alg line 396 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, IsScalarTower, AlgHom, S_ring
Proof uses: AlgHom.mk, fL_hom
19 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def fA_alg line 401 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, IsScalarTower, AlgHom, S_ring
Proof uses: AlgHom.mk, fA_hom
19 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
def lift_to_S line 416 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, IsScalarTower, AlgHom, TensorProduct, S_ring
Proof uses: Algebra.TensorProduct.lift, fL_alg, fA_alg, fL_fA_comm
36 instances, coercions and auxiliary constants left out.
def base_change_map line 421 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, IsScalarTower, RingHom, TensorProduct
Proof uses: AlgHom.toRingHom, Algebra.TensorProduct.lift, AlgHom.restrictScalars, Algebra.TensorProduct.includeLeft, Algebra.TensorProduct.includeRight
46 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def S_to_base_change line 430 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, IsScalarTower, RingHom, S_ring, TensorProduct
Proof uses: Ideal.Quotient.lift, I_rel, base_change_map
49 instances, coercions and auxiliary constants left out.

Tactic trace: 25 steps
Open to load the checked before-and-after goal states.
lemma S_ring_isReduced line 468 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, IsScalarTower, IsReduced, TensorProduct, Algebra.IsSeparable, S_ring
Proof uses: reduced_quotient_directed_idempotents, I_rel, ideal_generated_by_idempotents, Set.range, u_elem, Eq.refl, Ideal, Membership.mem, Set, Eq, Exists, And, HMul.hMul, Polynomial, minpoly, Polynomial.Separable, Algebra.IsSeparable.isSeparable, RingHom, algebraMap, AlgHom and 64 more
101 instances, coercions and auxiliary constants left out.

Tactic trace: 40 steps
Open to load the checked before-and-after goal states.
lemma isAlgClosure_of_isAlgebraic line 523 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, Algebra.IsAlgebraic, IsScalarTower, IsAlgClosure
Proof uses: IsAlgClosure.mk, IsAlgClosure.isAlgClosed, Algebra.IsAlgebraic.trans
54 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma isReduced_equiv line 530 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, RingEquiv, Iff, IsReduced
Proof uses: Iff.intro, retract_reduced, RingEquiv.toRingHom, RingEquiv.symm, RingHom.ext, RingHom.comp, RingHom.id, RingEquiv.apply_symm_apply, RingEquiv.symm_apply_apply
29 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma geom_reduced_of_alg_closure line 537 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, IsAlgClosure, Iff, Algebra.IsGeometricallyReduced, IsReduced, TensorProduct
Proof uses: AlgEquiv, AlgebraicClosure, IsAlgClosure.equiv, MvPolynomial, AlgebraicClosure.Vars, AlgebraicClosure.maxIdeal, Algebra.TensorProduct.congr, AlgEquiv.refl, Eq.mpr, id, Eq, congrArg, propext, Algebra.isGeometricallyReduced_iff, Iff.symm, isReduced_equiv, AlgEquiv.toRingEquiv
100 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma zero_of_coprime_annihilators line 546 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Eq, HMul.hMul, OfNat.ofNat, IsCoprime, Membership.mem, Ideal, Ideal.span, Singleton.singleton, Set
Proof uses: Exists, Iff.mp, Ideal.mem_span_singleton', HAdd.hAdd, Trans.trans, Eq.symm, mul_one, Eq.mpr, id, congrArg, Eq.refl, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Mathlib.Tactic.Ring.mul_congr, Mathlib.Tactic.Ring.atom_pf, Mathlib.Tactic.Ring.add_congr, Mathlib.Tactic.Ring.add_mul and 13 more
61 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma zero_of_prod_linear_aux line 563 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, List, CommRing, Algebra, Polynomial.Separable, List.prod, Polynomial, List.map, HSub.hSub, Polynomial.X, RingHom, Polynomial.C, Eq, AlgHom, Polynomial.aeval, OfNat.ofNat, Membership.mem, Ideal, Ideal.span, Singleton.singleton and 2 more
Proof uses: List.rec, List.nil, rfl, Trans.trans, HMul.hMul, Eq.symm, mul_one, Eq.mpr, id, congrArg, Eq.mp, map_one, Eq.refl, MulZeroClass.mul_zero, List.cons, Polynomial.Separable.of_mul_right, IsCoprime, Polynomial.Separable.isCoprime, map_mul, MonoidHom.id and 23 more
142 instances, coercions and auxiliary constants left out.

Tactic trace: 52 steps
Open to load the checked before-and-after goal states.
lemma mem_ideal_span_of_poly_aux line 623 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Algebra, Polynomial, Membership.mem, Ideal, Ideal.span, Singleton.singleton, Set, HSub.hSub, AlgHom, Polynomial.aeval
Proof uses: Eq.mpr, Exists, Eq, HMul.hMul, Finset.sum, Nat, Finset.range, HAdd.hAdd, Polynomial.natDegree, OfNat.ofNat, HSMul.hSMul, Polynomial.coeff, HPow.hPow, id, Eq.trans, congrArg, congr, Polynomial.aeval_eq_sum_range, Exists.imp, Function.comp and 14 more
81 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma mem_ideal_span_of_poly line 628 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, IsScalarTower, Polynomial, Membership.mem, TensorProduct, Ideal, Ideal.span, Singleton.singleton, Set, u_elem, AlgHom, Polynomial.aeval
Proof uses: TensorProduct.tmul, RingHom, algebraMap, OfNat.ofNat, Eq, Algebra.TensorProduct.includeLeft, rfl, Eq.mpr, id, congrArg, Polynomial.aeval_algHom_apply, Polynomial.aeval_algebraMap_apply, Eq.refl, Algebra.TensorProduct.includeRight, HSub.hSub, mem_ideal_span_of_poly_aux, Eq.mp
79 instances, coercions and auxiliary constants left out.

Tactic trace: 21 steps
Open to load the checked before-and-after goal states.
lemma fd_helper line 655 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, Algebra.IsSeparable, List, FiniteDimensional, Subtype, Membership.mem, IntermediateField, IntermediateField.adjoin, setOf
Proof uses: IsIntegral, IsAlgebraic.isIntegral, Algebra.IsAlgebraic.isAlgebraic, isAlgebraic_of_isSeparable, Finite, Set.Finite.to_subtype, List.finite_toSet, IntermediateField.finiteDimensional_adjoin, Set
43 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma sep_helper line 661 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, Algebra.IsSeparable, List, Subtype, Membership.mem, IntermediateField, IntermediateField.adjoin, setOf
Proof uses: inferInstance
63 instances, coercions and auxiliary constants left out.
lemma alg_helper line 664 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, Algebra.IsSeparable, List, Subtype, Membership.mem, IntermediateField, IntermediateField.adjoin, setOf, IsIntegral
Proof uses: Eq, Subtype.mk, Exists.imp, Polynomial, And, Polynomial.Monic, Polynomial.eval₂, algebraMap, OfNat.ofNat, of_eq_true, Eq.trans, True, forall_congr, Finset.sum, Nat, Finset.range, HAdd.hAdd, Polynomial.natDegree, HMul.hMul, RingHom and 18 more
98 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma in_adjoin_helper line 669 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, Algebra.IsSeparable, List, Subtype, Membership.mem, IntermediateField, IntermediateField.adjoin, setOf, Eq, Singleton.singleton, Set, Top.top
Proof uses: Eq.rec, trivial, Eq.symm
80 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma range_helper line 673 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, Algebra.IsSeparable, List, Subtype, Membership.mem, IntermediateField, IntermediateField.adjoin, setOf, Singleton.singleton, Set, Subalgebra, AlgHom.range, Polynomial, Polynomial.aeval
Proof uses: Eq, IntermediateField.toSubalgebra, Algebra.adjoin, IntermediateField.adjoin_simple_toSubalgebra_of_integral, IsIntegral, Algebra.IsSeparable.isIntegral, Eq.mpr, id, congrArg, Eq.symm, Algebra.adjoin_singleton_eq_range_aeval
70 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma eq_helper line 678 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, Algebra.IsSeparable, List, Subtype, Membership.mem, IntermediateField, IntermediateField.adjoin, setOf, Polynomial, Eq, AlgHom, Polynomial.aeval, Subtype.mk, IntermediateField.subset_adjoin
Proof uses: of_eq_true, Eq.trans, True, congrArg, Finset.sum, Nat, Finset.range, HAdd.hAdd, Polynomial.natDegree, OfNat.ofNat, HSMul.hSMul, Polynomial.coeff, HPow.hPow, Polynomial.aeval_eq_sum_range, id, Eq.mp, AddSubmonoidClass.coe_finset_sum, Finset.sum_congr, Eq.refl, Finset and 1 more
92 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma exists_primitive_element_of_list line 682 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, Algebra.IsSeparable, List, Exists, Membership.mem, Polynomial, Eq, AlgHom, Polynomial.aeval
Proof uses: IntermediateField, IntermediateField.adjoin, setOf, IsAlgebraic, Algebra.IsAlgebraic.isAlgebraic, isAlgebraic_of_isSeparable, FiniteDimensional, Subtype, fd_helper, sep_helper, Singleton.singleton, Set, Top.top, Field.exists_primitive_element, Exists.intro, IntermediateField.subset_adjoin, Subtype.mk, in_adjoin_helper, Subalgebra, AlgHom.range and 4 more
68 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
lemma common_primitive_of_two line 699 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, IsScalarTower, Algebra.IsSeparable, Exists, And, Membership.mem, TensorProduct, Ideal, Ideal.span, Singleton.singleton, Set, u_elem
Proof uses: List, List.cons, List.nil, Polynomial, Eq, AlgHom, Polynomial.aeval, exists_primitive_element_of_list, of_eq_true, Eq.trans, Or, True, congr, congrArg, eq_self, False, or_false, true_or, or_true, Exists.intro and 4 more
63 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
lemma exists_primitive_of_I_rel line 719 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, IsScalarTower, Algebra.IsSeparable, TensorProduct, Membership.mem, Ideal, I_rel, Exists, Ideal.span, Singleton.singleton, Set, u_elem
Proof uses: Submodule.span_induction, Set.range, Eq, Exists.intro, Ideal.subset_span, Set.mem_singleton, OfNat.ofNat, Ideal.zero_mem, Submodule, Submodule.span, HAdd.hAdd, And, common_primitive_of_two, LE.le, Eq.mpr, HasSubset.Subset, id, congrArg, propext, Ideal.span_le and 5 more
85 instances, coercions and auxiliary constants left out.

Tactic trace: 31 steps
Open to load the checked before-and-after goal states.
lemma fwd_dir line 761 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, Algebra.IsSeparable, IsScalarTower, Algebra.IsGeometricallyReduced
Proof uses: AlgebraicClosure, Algebra.IsAlgebraic, isAlgebraic_of_isSeparable, IsAlgClosure, MvPolynomial, AlgebraicClosure.Vars, AlgebraicClosure.maxIdeal, isAlgClosure_of_isAlgebraic, IsReduced, TensorProduct, Iff.mp, geom_reduced_of_alg_closure, S_ring, S_ring_isReduced, Eq, RingHom, RingHom.comp, S_to_base_change, AlgHom.toRingHom, lift_to_S and 34 more
114 instances, coercions and auxiliary constants left out.

Tactic trace: 36 steps
Open to load the checked before-and-after goal states.
lemma finite_conjugates_aux line 819 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, Algebra.IsAlgebraic, TensorProduct, Exists, Finset, AlgHom, Membership.mem, Algebra.TensorProduct.map, AlgHom.id
Proof uses: TensorProduct.induction_on, Exists.intro, OfNat.ofNat, Singleton.singleton, of_eq_true, Eq.trans, Eq, True, congrArg, map_zero, eq_self, Polynomial, minpoly, Multiset.toFinset, Polynomial.roots, Polynomial.map, algebraMap, Finset.image, TensorProduct.tmul, Eq.mpr and 28 more
111 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
lemma exists_algEquiv_of_roots line 844 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, IsAlgClosed, Algebra.IsAlgebraic, Eq, Polynomial, minpoly, Exists, AlgEquiv
Proof uses: AlgHom, Polynomial.aeval, OfNat.ofNat, Eq.mpr, id, congrArg, minpoly.aeval, Eq.refl, Exists.elim, IntermediateField.exists_algHom_of_splits_of_aeval, of_eq_true, And, IsIntegral, Polynomial.Splits, Polynomial.map, algebraMap, Eq.trans, True, forall_congr, congr and 13 more
53 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
def get_y_fun line 854 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, IsScalarTower, Algebra.IsSeparable, TensorProduct
Proof uses: dite, Membership.mem, Ideal, I_rel, Classical.choose, Ideal.span, Singleton.singleton, Set, u_elem, exists_primitive_of_I_rel, Not, OfNat.ofNat
51 instances, coercions and auxiliary constants left out.
lemma get_y_spec line 862 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, IsScalarTower, Algebra.IsSeparable, TensorProduct, Membership.mem, Ideal, I_rel, Ideal.span, Singleton.singleton, Set, u_elem, get_y_fun
Proof uses: Eq.mpr, dite, Classical.choose, exists_primitive_of_I_rel, Not, OfNat.ofNat, id, Eq, congrArg, get_y_fun.eq_1, dif_pos, Classical.choose_spec
58 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma lift_comp_S_to_base_change line 870 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, IsScalarTower, Eq, RingHom, S_ring, RingHom.comp, TensorProduct, AlgHom.toRingHom, lift_to_S, S_to_base_change, RingHom.id
Proof uses: Ideal.Quotient.ringHom_ext, I_rel, RingHom.ext, HasQuotient.Quotient, Ideal, Ideal.Quotient.mk, TensorProduct.induction_on, of_eq_true, Function.comp, AlgHom, OfNat.ofNat, Eq.trans, True, congr, congrArg, map_zero, eq_self, id, TensorProduct.tmul, base_change_map and 16 more
103 instances, coercions and auxiliary constants left out.

Tactic trace: 22 steps
Open to load the checked before-and-after goal states.
lemma x_in_I_rel_of_base_change_zero line 899 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, IsScalarTower, TensorProduct, Eq, RingHom, base_change_map, OfNat.ofNat, Membership.mem, Ideal, I_rel
Proof uses: S_ring, S_to_base_change, HasQuotient.Quotient, Ideal.Quotient.mk, AlgHom.toRingHom, lift_to_S, Eq.mpr, id, congrArg, Eq.refl, RingHom.comp, RingHom.id, RingHom.congr_fun, lift_comp_S_to_base_change, Iff.mp, Ideal.Quotient.eq_zero_iff_mem, Eq.mp, map_zero
83 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma nilpotent_mem_I_rel line 913 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, IsScalarTower, IsReduced, TensorProduct, IsNilpotent, Membership.mem, Ideal, I_rel
Proof uses: RingHom, base_change_map, IsNilpotent.map, Eq, OfNat.ofNat, IsReduced.eq_zero, x_in_I_rel_of_base_change_zero
64 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma h_sep_roots_lemma line 922 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, Polynomial, Polynomial.Separable, List, Eq, Multiset.toList, Polynomial.roots, Polynomial.map, algebraMap, List.prod, List.map, HSub.hSub, Polynomial.X, RingHom, Polynomial.C
Proof uses: Eq.mpr, Multiset.prod, Multiset.map, id, congrArg, Eq.trans, Multiset.prod_map_toList, Polynomial.Separable.of_dvd, Polynomial.Separable.map, Polynomial.prod_multiset_X_sub_C_dvd
42 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma h_aeval_lemma line 928 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, IsScalarTower, Polynomial, Polynomial.Monic, Eq, AlgHom, Polynomial.aeval, OfNat.ofNat, List, Multiset.toList, Polynomial.roots, Polynomial.map, algebraMap, IsAlgClosed, TensorProduct, TensorProduct.tmul, RingHom, List.prod and 4 more
Proof uses: Eq.mpr, Finset.sum, Nat, Finset.range, HAdd.hAdd, Multiset.card, HSMul.hSMul, Polynomial.coeff, Multiset.prod, Multiset.map, HPow.hPow, id, congrArg, Eq.trans, Polynomial.natDegree, Multiset.prod_map_toList, Polynomial.aeval_eq_sum_range, Finset.sum_congr, Finset, Polynomial.natDegree_multiset_prod_X_sub_C_eq_card and 47 more
155 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
lemma h_P_r_lemma line 946 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, Polynomial, List, Eq, Multiset.toList, Polynomial.roots, Polynomial.map, algebraMap, Membership.mem, AlgHom, Polynomial.aeval, OfNat.ofNat
Proof uses: of_eq_true, Polynomial.eval₂, Eq.trans, True, congrArg, id, And, Not, Eq.mp, Multiset, Ne, Polynomial.IsRoot, congr, Polynomial.eval, Polynomial.eval_map, eq_self
56 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma h_inv_lemma line 951 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, AlgEquiv, TensorProduct, Eq, AlgHom, Algebra.TensorProduct.map, AlgEquiv.symm, AlgHom.id
Proof uses: symm, TensorProduct.induction_on, of_eq_true, OfNat.ofNat, Eq.trans, True, congrArg, map_zero, eq_self, TensorProduct.tmul, AlgEquiv.symm_apply_apply, HAdd.hAdd, map_add, RingHom.id, congr
97 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma h_map_u_lemma line 956 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, IsScalarTower, AlgEquiv, Eq, RingHom, algebraMap, TensorProduct, AlgHom, Algebra.TensorProduct.map, AlgEquiv.symm, AlgHom.id, u_elem, HSub.hSub, TensorProduct.tmul, OfNat.ofNat
Proof uses: of_eq_true, Eq.trans, True, HSMul.hSMul, congr, congrArg, Eq.symm, Algebra.algebraMap_eq_smul_one, map_sub, outParam, MonoidHom, MonoidHom.id, AlgEquiv.symm_apply_apply, map_one, eq_self, eq_true, True.intro
121 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma ideal_span_singleton_map line 963 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, RingHom, Membership.mem, Ideal, Ideal.span, Singleton.singleton, Set
Proof uses: Eq, HMul.hMul, Exists, Iff.mp, Ideal.mem_span_singleton', Eq.mpr, id, congrArg, map_mul, Iff.mpr, Exists.intro, rfl
34 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma rev_dir_reduced line 969 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, Algebra.IsSeparable, IsScalarTower, IsAlgClosure, IsReduced, TensorProduct
Proof uses: IsReduced.mk, IsNilpotent, Nat, Eq, HPow.hPow, OfNat.ofNat, Algebra.IsAlgebraic, isAlgebraic_of_isSeparable, isAlgClosure_of_isAlgebraic, Exists.intro, Finset, AlgHom, Membership.mem, Algebra.TensorProduct.map, AlgHom.id, Exists, finite_conjugates_aux, List, List.map, get_y_fun and 79 more
164 instances, coercions and auxiliary constants left out.

Tactic trace: 57 steps
Open to load the checked before-and-after goal states.
lemma rev_dir line 1034 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, Algebra.IsSeparable, IsScalarTower, Algebra.IsGeometricallyReduced
Proof uses: AlgebraicClosure, Algebra.IsAlgebraic, isAlgebraic_of_isSeparable, IsAlgClosure, MvPolynomial, AlgebraicClosure.Vars, AlgebraicClosure.maxIdeal, isAlgClosure_of_isAlgebraic, IsReduced, TensorProduct, Iff.mp, geom_reduced_of_alg_closure, rev_dir_reduced, Iff.mpr
65 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
theorem isGeometricallyReduced_iff_of_separable_algebraic line 1048 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, Algebra.IsSeparable, IsScalarTower, Iff, Algebra.IsGeometricallyReduced
Proof uses: Iff.intro, fwd_dir, rev_dir
24 instances, coercions and auxiliary constants left out.

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