Ultraproduct.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

47 declarations, 0 contain sorry, 0 declared as axioms

Ultraproducts of submodules

For a filter F on the index set, we define eventuallyProd F N as the submodule of Πᵢ M i consisting of elements eventually in the submodule N i. Basic monotonicity and lattice properties.

Imports (4)

Imported by 4 files

def eventuallyProd Given a filter F on the index set and a family of submodules N i ≤ M i, the submodule of Π i, M i consisting of those tuples v for which v i ∈ N i holds F-eventually line 34 source
Source documentation
Given a filter F on the index set and a family of submodules N i ≤ M i, the submodule of Π i, M i consisting of those tuples v for which v i ∈ N i holds F-eventually.

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

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
def eventuallyProd (F : Filter ι) : Submodule (Π i, R i) (Π i, M i) where
…
```
lemma mem_eventuallyProd line 42 source
standard axioms: Quot.sound, propext what this means
Statement uses: CommRing, AddCommGroup, Module, Submodule, Filter, Iff, Membership.mem, eventuallyProd, Filter.Eventually
Proof uses: Iff.rfl
16 instances, coercions and auxiliary constants left out.
lemma eventuallyProd_mono_left line 46 source
standard axioms: Quot.sound, propext what this means
Statement uses: CommRing, AddCommGroup, Module, Filter, Submodule, LE.le, eventuallyProd
Proof uses: Membership.mem, Filter.Eventually.mp, of_eq_true, Filter.Eventually, Eq.trans, True, congrFun', congrArg, funext, implies_congr_ctx, Eq.refl, eq_true, Eq.mp, forall_congr, implies_true
26 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma eventuallyProd_mono_right line 52 source
standard axioms: Quot.sound, propext what this means
Statement uses: CommRing, AddCommGroup, Module, Submodule, Filter, LE.le, eventuallyProd
Proof uses: Filter.Eventually.filter_mono, Membership.mem
18 instances, coercions and auxiliary constants left out.
lemma eventuallyProd_eq_sup line 56 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, AddCommGroup, Module, Submodule, Filter, Eq, eventuallyProd, Max.max, Bot.bot, Submodule.pi'
Proof uses: le_antisymm, Membership.mem, Exists, And, Filter.Eventually, OfNat.ofNat, HSub.hSub, Exists.intro, ite, Classical.propDecidable, And.intro, Filter.mp_mem, Set.ofPred, Eq.mp, Filter.univ_mem', Set, id, ite_eq_left, dite, Eq.mpr and 19 more
60 instances, coercions and auxiliary constants left out.

Tactic trace: 21 steps
Open to load the checked before-and-after goal states.
instance eventuallyProd.isPrime line 72 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Ideal, Ultrafilter, Ideal.IsPrime, eventuallyProd
Proof uses: Ideal.IsPrime.mk, Eq.mpr, Ne, Top.top, Not, Eq, id, congrArg, ne_eq, Membership.mem, OfNat.ofNat, propext, Ideal.eq_top_iff_one, Filter.Frequently, Submodule, Eq.trans, Filter.Eventually, of_eq_true, True, congrFun' and 11 more
41 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
def UltraProduct The ultraproduct of a family of additive groups M i along a filter F: the quotient of Π i, M i by tuples that are zero F-eventually line 87 source
Source documentation
The ultraproduct of a family of additive groups M i along a filter F: the quotient of Π i, M i by tuples that are zero F-eventually.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Filter
Proof uses: HasQuotient.Quotient, Submodule, Int, eventuallyProd, Bot.bot
15 instances, coercions and auxiliary constants left out.
```
def UltraProduct : Type _ :=
…
```
instance (instance at line 93) line 93 source
Source documentation
The ultraproduct of AddCommGroups is an AddCommGroup.
```
instance : AddCommGroup (UltraProduct M F) := inferInstanceAs
…
```
Mentions: UltraProduct
instance (instance at line 97) line 97 source
Source documentation
The ultraproduct of CommRings is a CommRing.
```
instance : CommRing (UltraProduct R F) := inferInstanceAs
…
```
Mentions: UltraProduct
def UltraProduct.π The canonical projection from the product Π i, R i to the ultraproduct as a ring homomorphism line 103 source
Source documentation
The canonical projection from the product Π i, R i to the ultraproduct as a ring homomorphism.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Filter, RingHom, UltraProduct
Proof uses: Ideal.Quotient.mk, eventuallyProd, Bot.bot, Submodule
18 instances, coercions and auxiliary constants left out.
```
def UltraProduct.π : (Π i, R i) →+* UltraProduct R F :=
…
```
Mentions: UltraProduct
instance (instance at line 106) line 106 source
def UltraProduct.πₗ The canonical projection from the product Π i, M i of R i-modules to the ultraproduct as a Π i, R i-linear map line 112 source
Source documentation
The canonical projection from the product Π i, M i of R i-modules to the ultraproduct as a Π i, R i-linear map.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, AddCommGroup, Module, Filter, LinearMap, RingHom.id, UltraProduct
Proof uses: Submodule.mkQ, eventuallyProd, Bot.bot, Submodule
19 instances, coercions and auxiliary constants left out.
```
def UltraProduct.πₗ : (Π i, M i) →ₗ[Π i, R i] UltraProduct M F :=
…
```
Mentions: UltraProduct
lemma UltraProduct.π_surjective line 115 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Filter, Function.Surjective, UltraProduct, RingHom, UltraProduct.π
Proof uses: Submodule.mkQ_surjective, eventuallyProd, Bot.bot, Submodule
20 instances, coercions and auxiliary constants left out.
lemma UltraProduct.πₗ_surjective line 119 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, AddCommGroup, Module, Filter, Function.Surjective, UltraProduct, LinearMap, RingHom.id, UltraProduct.πₗ
Proof uses: Submodule.mkQ_surjective, eventuallyProd, Bot.bot, Submodule
21 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
instance (instance at line 124) line 124 source
instance (instance at line 138) line 138 source
lemma UltraProduct.instIsScalarTower making this an instance timesout everything line 142 source
Source comment
making this an instance timesout everything.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, AddCommGroup, Filter, Module, Algebra, IsScalarTower, UltraProduct
33 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
lemma UltraProduct.instIsScalarTower
    {R₁ : Type*} [CommRing R₁] [∀ i, Module R₁ (M i)] [Algebra R₀ R₁]
    [∀ i, IsScalarTower R₀ R₁ (M i)] :
    IsScalarTower R₀ R₁ (UltraProduct M F) :=
…
```
Mentions: UltraProduct
instance (instance at line 148) line 148 source
instance (instance at line 152) line 152 source
lemma UltraProduct.πₗ_eq_zero line 164 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, AddCommGroup, Module, Filter, Iff, Eq, UltraProduct, LinearMap, RingHom.id, UltraProduct.πₗ, OfNat.ofNat, Filter.Eventually
Proof uses: Submodule.Quotient.mk_eq_zero, eventuallyProd, Bot.bot, Submodule
27 instances, coercions and auxiliary constants left out.
lemma UltraProduct.πₗ_eq_iff line 168 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, AddCommGroup, Module, Filter, Iff, Eq, UltraProduct, LinearMap, RingHom.id, UltraProduct.πₗ, Filter.Eventually
Proof uses: Iff.trans, HasQuotient.Quotient, Submodule, eventuallyProd, Bot.bot, Submodule.Quotient.mk, Membership.mem, HSub.hSub, Submodule.Quotient.eq, of_eq_true, Eq.trans, True, congrFun', congrArg, funext, OfNat.ofNat, iff_self
39 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma UltraProduct.π_eq_iff line 172 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Filter, Iff, Eq, UltraProduct, RingHom, UltraProduct.π, Filter.Eventually
Proof uses: Iff.trans, HasQuotient.Quotient, Submodule, eventuallyProd, Bot.bot, Submodule.Quotient.mk, Membership.mem, HSub.hSub, Submodule.Quotient.eq, of_eq_true, Eq.trans, True, congrFun', congrArg, funext, OfNat.ofNat, iff_self
40 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma UltraProduct.π_eq_zero_iff line 176 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Filter, Iff, Eq, UltraProduct, RingHom, UltraProduct.π, OfNat.ofNat, Filter.Eventually
Proof uses: UltraProduct.π_eq_iff
21 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 179) line 179 source
lemma UltraProduct.π_smul line 188 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, AddCommGroup, Module, Filter, UltraProduct, Eq, HSMul.hSMul, RingHom, UltraProduct.π
Proof uses: rfl
39 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
instance (instance at line 190) line 190 source
instance (instance at line 195) line 195 source
instance (instance at line 203) line 203 source
instance (instance at line 211) line 211 source
instance (instance at line 212) line 212 source
instance (instance at line 213) line 213 source
instance (instance at line 214) line 214 source
def UltraProduct.map A family of linear maps f i : M i →ₗ[R i] N i induces a linear map between the corresponding ultraproducts line 221 source
Source documentation
A family of linear maps f i : M i →ₗ[R i] N i induces a linear map between the corresponding ultraproducts.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, AddCommGroup, Module, Filter, LinearMap, RingHom.id, UltraProduct
Proof uses: Submodule.mapQ, eventuallyProd, Bot.bot, Submodule, LinearMap.piMap', Membership.mem
23 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
def UltraProduct.map (f : ∀ i, M i →ₗ[R i] N i) :
    UltraProduct M F →ₗ[∀ i, R i] UltraProduct N F :=
…
```
Mentions: UltraProduct
lemma UltraProduct.map_πₗ line 228 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, AddCommGroup, Module, Filter, LinearMap, RingHom.id, Eq, UltraProduct, UltraProduct.map, UltraProduct.πₗ
Proof uses: rfl
24 instances, coercions and auxiliary constants left out.
def UltraProduct.mapRingHom A family of ring homomorphisms f i : R i →+* S i induces a ring homomorphism between the corresponding ultraproducts line 234 source
Source documentation
A family of ring homomorphisms f i : R i →+* S i induces a ring homomorphism between the corresponding ultraproducts.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Filter, RingHom, UltraProduct
Proof uses: Ideal.quotientMap, eventuallyProd, Bot.bot, Submodule, RingHom.pi, RingHom.comp, Pi.evalRingHom
21 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
def UltraProduct.mapRingHom {S : ι → Type*} [∀ i, CommRing (S i)] (f : ∀ i, R i →+* S i) :
    UltraProduct R F →+* UltraProduct S F :=
…
```
Mentions: UltraProduct
lemma UltraProduct.mapRingHom_π line 241 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Filter, RingHom, Eq, UltraProduct, UltraProduct.mapRingHom, UltraProduct.π
Proof uses: rfl
18 instances, coercions and auxiliary constants left out.
lemma UltraProduct.map_surjective line 245 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, AddCommGroup, Module, Filter, LinearMap, RingHom.id, Function.Surjective, UltraProduct, UltraProduct.map
Proof uses: Eq, UltraProduct.πₗ, Exists, UltraProduct.πₗ_surjective, Exists.intro, of_eq_true, Eq.trans, True, congrFun', congrArg, funext, eq_self, Classical.choose, Classical.choose_spec
24 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma UltraProduct.mapRingHom_surjective line 254 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Filter, RingHom, Function.Surjective, UltraProduct, UltraProduct.mapRingHom
Proof uses: UltraProduct.map_surjective, Int, AddMonoidHom.toIntLinearMap, RingHom.toAddMonoidHom
17 instances, coercions and auxiliary constants left out.
lemma UltraProduct.surjective_of_eventually_surjective line 262 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, AddCommGroup, Module, LinearMap, RingHom.id, Finite, Ultrafilter, Filter.Eventually, Function.Surjective, UltraProduct, LinearMap.comp, UltraProduct.πₗ, LinearMap.pi
Proof uses: Eq, Exists, UltraProduct.πₗ_surjective, Filter.mp_mem, Set.ofPred, Filter.univ_mem', Membership.mem, Set, id, Iff.mp, Ultrafilter.eventually_exists_iff, Exists.intro, Iff.mpr, UltraProduct.πₗ_eq_iff
86 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma UltraProduct.bijective_of_eventually_bijective line 271 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, AddCommGroup, Module, LinearMap, RingHom.id, Finite, Ultrafilter, Filter.Eventually, Function.Bijective, UltraProduct, LinearMap.comp, UltraProduct.πₗ, LinearMap.pi
Proof uses: And.intro, Function.Injective, Function.Surjective, Eq.mpr, Eq, OfNat.ofNat, id, congrArg, propext, injective_iff_map_eq_zero, RingHom, Eq.mp, And, Exists, Filter.Eventually.exists, Filter.Eventually.and, And.left, Eq.trans, Eq.symm, LinearMap.map_zero and 12 more
100 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
lemma UltraProduct.isUnit_π_iff line 286 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Filter, Iff, IsUnit, UltraProduct, RingHom, UltraProduct.π, Filter.Eventually
Proof uses: Eq.mpr, Exists, Eq, HMul.hMul, OfNat.ofNat, id, congr, congrArg, congrFun', funext, propext, Function.Surjective.exists, UltraProduct.π_surjective, Eq.symm, map_one, Iff.symm, Filter.skolem
49 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
instance (instance at line 291) line 291 source
lemma UltraProduct.exists_bijective_of_bddAbove_card line 301 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, AddCommGroup, Module, Algebra.FiniteType, Int, Ultrafilter, Nat, Filter.Eventually, And, Finite, LT.lt, Nat.card, Nonempty, LinearEquiv, RingHom.id, Function.Bijective, UltraProduct, LinearMap, LinearMap.comp, UltraProduct.πₗ and 6 more
Proof uses: Exists, ModuleTypeCardLT, Fin, Sigma.fst, Sigma, Filter.mp_mem, Set.ofPred, Filter.univ_mem', Membership.mem, Set, id, Exists.intro, ModuleTypeCardLT.ofModule, Nonempty.intro, ModuleTypeCardLT.equivOfModule, Iff.mp, Ultrafilter.eventually_exists_iff, Iff.mpr, Equiv.finite_iff, LinearEquiv.toEquiv and 10 more
109 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
lemma UltraProduct.exists_algEquiv_of_bddAbove_card Let R₀ be a topological ring, topologically of finite type (over ℤ) line 327 source
Source documentation
Let R₀ be a topological ring, topologically of finite type (over ℤ). Consider a family of (cardinality) finite continuous R₀-algebras R i with the discrete topology whose cardinalites are unifomly bounded.
Then 𝒰(Rᵢ) ≃ₐ[R] R i for F-many i.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Algebra, TopologicalSpace, IsTopologicalRing, Algebra.TopologicallyFG, Int, T2Space, Ultrafilter, Nat, Filter.Eventually, And, Finite, LT.lt, Nat.card, ContinuousSMul, Nonempty, AlgEquiv, UltraProduct
Proof uses: Exists, TopologicalAlgebraTypeCardLT, Fin, PSigma.fst, PSigma, Ring, IsHomeomorph, Filter.mp_mem, Set.ofPred, Membership.mem, Set, Filter.univ_mem', id, Exists.intro, TopologicalAlgebraTypeCardLT.ofAlgebra, TopologicalAlgebraTypeCardLT.equivOfAlgebra, TopologicalAlgebraTypeCardLT.isHomeomorph_equivOfAlgebra, Iff.mp, Ultrafilter.eventually_exists_iff, LinearMap and 41 more
114 instances, coercions and auxiliary constants left out.

Tactic trace: 27 steps
Open to load the checked before-and-after goal states.
```
lemma UltraProduct.exists_algEquiv_of_bddAbove_card
    [TopologicalSpace R₀]
    [IsTopologicalRing R₀]
    [Algebra.TopologicallyFG ℤ R₀]
    [∀ i, TopologicalSpace (R i)]
    [∀ i, T2Space (R i)] (F : Ultrafilter ι)
    (N : ℕ) (H : ∀ᶠ i in F, Finite (R i) ∧ Nat.card (R i) < N)
    (hcont : ∀ᶠ i in F, ContinuousSMul R₀ (R i)) :
    ∀ᶠ i in F, Nonempty (UltraProduct R F ≃ₐ[R₀] R i) := by
…
```
Mentions: Algebra.TopologicallyFG, UltraProduct
lemma UltraProduct.exists_ringEquiv_of_bddAbove_card Let R₀ be a topological ring, topologically of finite type (over ℤ) line 374 source
Source documentation
Let R₀ be a topological ring, topologically of finite type (over ℤ). Consider a family of (cardinality) finite rings R i with the discrete topology whose cardinalites are unifomly bounded.
Given a family of continuous ring homs f i : R →+* R i, there exists F-many i such that 𝒰(Rᵢ) ≃+* R i and this map is compatible with f.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, TopologicalSpace, IsTopologicalRing, Algebra.TopologicallyFG, Int, T2Space, Ultrafilter, Nat, Filter.Eventually, And, Finite, LT.lt, Nat.card, RingHom, Continuous, Exists, RingEquiv, UltraProduct, Eq, RingHom.comp and 3 more
Proof uses: Algebra, RingHom.toAlgebra, Nonempty, AlgEquiv, UltraProduct.exists_algEquiv_of_bddAbove_card, Filter.mp_mem, Set.ofPred, ContinuousSMul, Filter.univ_mem', Membership.mem, Set, id, ContinuousSMul.mk, Prod, HMul.hMul, Prod.fst, Prod.snd, Eq.mp, Continuous.fun_mul, Continuous.comp' and 5 more
50 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
lemma UltraProduct.exists_ringEquiv_of_bddAbove_card
    [TopologicalSpace R₀]
    [IsTopologicalRing R₀]
    [Algebra.TopologicallyFG ℤ R₀]
    [∀ i, TopologicalSpace (R i)]
    [∀ i, IsTopologicalRing (R i)]
    [∀ i, T2Space (R i)] (F : Ultrafilter ι)
    (N : ℕ) (H : ∀ᶠ i in F, Finite (R i) ∧ Nat.card (R i) < N)
    (f : ∀ i, R₀ →+* R i) (hf : ∀ᶠ i in F, Continuous (f i)) :
    ∀ᶠ i in F, ∃ e : UltraProduct R F ≃+*
      R i, e.toRingHom.comp ((π R F).comp (RingHom.pi f)) = f i := by
…
```
Mentions: Algebra.TopologicallyFG, UltraProduct, UltraProduct.π
lemma UltraProduct.continuous_of_bddAbove_card Let R₀ be a topological ring, topologically of finite type (over ℤ) line 401 source
Source documentation
Let R₀ be a topological ring, topologically of finite type (over ℤ). Consider a family of (cardinality) finite rings R i with the discrete topology whose cardinalites are unifomly bounded.
Given a family of continuous ring homs f i : R →+* R i, the lift R →+* 𝒰(Rᵢ) is also continuous.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, TopologicalSpace, IsTopologicalRing, Algebra.TopologicallyFG, Int, T2Space, Ultrafilter, Nat, Filter.Eventually, And, Finite, LT.lt, Nat.card, RingHom, Continuous, UltraProduct, RingHom.comp, UltraProduct.π, RingHom.pi
Proof uses: IsOpen, Ideal, RingHom.ker, Exists, RingEquiv, Eq, RingEquiv.toRingHom, Filter.Eventually.exists, Filter.Eventually.and, UltraProduct.exists_ringEquiv_of_bddAbove_card, RingEquiv.symm, Eq.mpr, id, congrArg, Eq.symm, RingHom.comp_assoc, of_eq_true, Eq.trans, True, congrFun' and 30 more
78 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
lemma UltraProduct.continuous_of_bddAbove_card
    [TopologicalSpace R₀]
    [IsTopologicalRing R₀]
    [Algebra.TopologicallyFG ℤ R₀]
    [∀ i, TopologicalSpace (R i)]
    [∀ i, IsTopologicalRing (R i)]
    [∀ i, T2Space (R i)] (F : Ultrafilter ι)
    (N : ℕ) (H : ∀ᶠ i in F, Finite (R i) ∧ Nat.card (R i) < N)
    (f : ∀ i, R₀ →+* R i) (hf : ∀ᶠ i in F, Continuous (f i)) :
    Continuous ((π R F).comp (RingHom.pi f)) := by
…
```
Mentions: Algebra.TopologicallyFG, UltraProduct.π
lemma UltraProduct.surjective_of_bddAbove_card Let R₀ be a topological ring, topologically of finite type (over ℤ) line 432 source
Source documentation
Let R₀ be a topological ring, topologically of finite type (over ℤ). Consider a family of (cardinality) finite rings R i with the discrete topology whose cardinalites are unifomly bounded.
Given a family of continuous surjective ring homs f i : R →+* R i, the lift R →+* 𝒰(Rᵢ) is also surjective.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, TopologicalSpace, IsTopologicalRing, Algebra.TopologicallyFG, Int, T2Space, Ultrafilter, Nat, Filter.Eventually, And, Finite, LT.lt, Nat.card, RingHom, Continuous, Function.Surjective, UltraProduct, RingHom.comp, UltraProduct.π, RingHom.pi
Proof uses: Exists, RingEquiv, Eq, RingEquiv.toRingHom, Filter.Eventually.exists, Filter.Eventually.and, UltraProduct.exists_ringEquiv_of_bddAbove_card, RingEquiv.symm, Eq.mpr, id, congrArg, Eq.symm, RingHom.comp_assoc, of_eq_true, Eq.trans, True, congrFun', RingHom.id, RingEquiv.symm_comp, RingHomCompTriple.comp_eq and 3 more
41 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma UltraProduct.surjective_of_bddAbove_card
    [TopologicalSpace R₀]
    [IsTopologicalRing R₀]
    [Algebra.TopologicallyFG ℤ R₀]
    [∀ i, TopologicalSpace (R i)]
    [∀ i, IsTopologicalRing (R i)]
    [∀ i, T2Space (R i)] (F : Ultrafilter ι)
    (N : ℕ) (H : ∀ᶠ i in F, Finite (R i) ∧ Nat.card (R i) < N)
    (f : ∀ i, R₀ →+* R i) (hf : ∀ᶠ i in F, Continuous (f i))
    (hf' : ∀ᶠ i in F, Function.Surjective (f i)) :
    Function.Surjective ((π R F).comp (RingHom.pi f)) := by
…
```
Mentions: Algebra.TopologicallyFG, UltraProduct.π