/-

From https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Lean4.20autocomplete

Will have to keep on fiddling the topic of meta-programming, syntax and dealing with files in Lean

related:

- https://github.com/utensil/LeanBlueprintExample/blob/main/Exe/Decls.lean
- https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/get.20filename.20.2B.20pos

-/

import Lean.Meta.Tactic.TryThis
import Lean.Data.FuzzyMatching
open Lean.Meta.Tactic

namespace Mathlib.Tactic.imp

open Lean Elab Command System
open Lean.FuzzyMatching

Infer module name of source file name.

def moduleNameOfFileName (fname : FilePath) (rootDir : Option FilePath) : IO Name := do
  Lean.initSearchPath (<- Lean.findSysroot) [(<-IO.currentDir) / "lake-packages/mathlib/"]
  let fname ← IO.FS.realPath fname
  let rootDir ← match rootDir with
    | some rootDir => pure rootDir
    | none         => IO.currentDir
  let mut rootDir ← IO.FS.realPath rootDir
  -- v4.32: `realPathNormalized` was removed; normalize explicitly
  rootDir := rootDir.normalize
  if !rootDir.toString.endsWith System.FilePath.pathSeparator.toString then
    rootDir := ⟨rootDir.toString ++ System.FilePath.pathSeparator.toString⟩
  if !rootDir.toString.isPrefixOf fname.normalize.toString then
    throw $ IO.userError s!"input file '{fname}' must be contained in root directory ({rootDir})"
  -- NOTE: use `fname` instead of `fname.normalize` to preserve casing on all platforms
  let fnameSuffixComponents := fname.withExtension "" |>.components.drop (rootDir.components.length + 1)
  let modName    := fnameSuffixComponents.foldl Name.mkStr Name.anonymous
  pure modName

A syntax that allows strings to be printed without surrounding them by guillemets «...».

declare_syntax_cat write_me_output_stx

@[inherit_doc 
Parser.Category.write_me_output_stx: Parser.Category
Parser.Category.write_me_output_stx
Warning: Parser.Category.write_me_output_stx does not have a doc string]
syntax "import " 
ident: Parser.Parser
ident : 
write_me_output_stx: Parser.Category
write_me_output_stx

imp <string> tries to find a file matching Mathlib.<string>. It prints a list of candidates, taking the names from Mathlib.lean. If there is only one candidate, it suggests import Mathlib.<uniqueCandidate> as a Try this.

Using imp! <string> uses fuzzy-matching, rather than exact matching.

elab (name := 
commandImp!: ParserDescr
commandImp!) 
tk: Syntax
tk
Warning: Variable name `tk` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).

Note: This linter can be disabled with `set_option linter.unusedVariables false`:"imp" 
fz: Option (TSyntax Name.anonymous)
fz:("!")? 
na: TSyntax `ident
na:(
colGt: optParam String "checkColGt" → Parser.Parser
colGt 
ident: Parser.Parser
ident) : 
command: Parser.Category
command => do
  let 
inp: String
inp := 
na: TSyntax `ident
na.
getId: Ident → Name
getId.
toString: Name → optParam Bool true → String
toString
  -- v4.32: `String.drop` returns `String.Slice` (convert with `toString`), and mathlib's
  -- `Mathlib.lean` now uses `public import Mathlib.` (22 chars) instead of `import Mathlib.` (15)
  let 
dat: Array String
dat := 
(← IO.FS.lines ".lake/packages/mathlib/Mathlib.lean"): Array String
(← 
IO.FS.lines: FilePath → IO (Array String)
IO.FS.lines
(← IO.FS.lines ".lake/packages/mathlib/Mathlib.lean"): Array String
 
".lake/packages/mathlib/Mathlib.lean": String
".lake/packages/mathlib/Mathlib.lean"
(← IO.FS.lines ".lake/packages/mathlib/Mathlib.lean"): Array String
).
map: {α β : Type} → (α → β) → Array α → Array β
map (fun 
l: String
l => (
l: String
l.
drop: String → Nat → String.Slice
drop 
22: Nat
22).
toString: String.Slice → String
toString)
  let 
cands: Array String
cands := 
dat: Array String
dat.
filter: {α : Type} → (α → Bool) → (as : Array α) → optParam Nat 0 → optParam Nat as.size → Array α
filter <| (if 
fz: Option (TSyntax Name.anonymous)
fz.
isSome: {α : Type} → Option α → Bool
isSome then 
fuzzyMatch: String → String → optParam Float 0.2 → Bool
fuzzyMatch else 
String.isPrefixOf: String → String → Bool
String.isPrefixOf) 
inp: String
inp

  
liftTermElabM: {α : Type} → TermElabM α → CommandElabM α
liftTermElabM do
    
cands: Array String
cands.
toList: {α : Type} → Array α → List α
toList.
forM: {m : Type → Type} → [Monad m] → {α : Type} → List α → (α → m PUnit) → m PUnit
forM fun 
imp: String
imp => do
      let 
impS: Name
impS ← 
moduleNameOfFileName: FilePath → Option FilePath → IO Name
moduleNameOfFileName (
".lake/packages/mathlib/Mathlib/": String
".lake/packages/mathlib/Mathlib/" ++ 
imp: String
imp.
replace: {ρ : Type} →
  {σ : String.Slice → Type} →
    [inst : (s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)] →
      [(s : String.Slice) → Std.IteratorLoop (σ s) Id Id] →
        {α : Type} →
          [String.ToSlice α] → String → (pattern : ρ) → [String.Slice.Pattern.ToForwardSearcher pattern σ] → α → String
replace 
".": String
"." 
"/": String
"/" ++ 
".lean": String
".lean") 
".lake/packages/mathlib/": String
".lake/packages/mathlib/"
      let 
imp: TSyntax `write_me_output_stx
imp : 
TSyntax: SyntaxNodeKinds → Type
TSyntax 
`write_me_output_stx: Name
`write_me_output_stx ← `(write_me_output_stx| import $(
mkIdent: Name → Ident
mkIdent 
impS: Name
impS))
      let 
stx: Syntax
stx ← 
getRef: {m : Type → Type} → [self : MonadRef m] → m Syntax
getRef
      -- v4.32: `addSuggestion` takes a `Suggestion`; wrap the syntax in `SuggestionText`
      
TryThis.addSuggestion: Syntax →
  TryThis.Suggestion →
    optParam (Option Syntax) none →
      optParam String "Try this:" →
        optParam (Option String) none →
          optParam Meta.Hint.DiffGranularity Meta.Hint.DiffGranularity.none →
            optParam MessageData MessageData.nil → CoreM Unit
TryThis.addSuggestion 
stx: Syntax
stx (
TryThis.SuggestionText.tsyntax: {kind : SyntaxNodeKind} → TSyntax kind → TryThis.SuggestionText
TryThis.SuggestionText.tsyntax 
imp: TSyntax `write_me_output_stx
imp)


@[inherit_doc 
commandImp!: ParserDescr
commandImp!
Warning: commandImp! does not have a doc string]
macro "imp!" 
na: TSyntax `ident
na:(
colGt: optParam String "checkColGt" → Parser.Parser
colGt 
ident: Parser.Parser
ident) : 
command: Parser.Category
command => `(
command: Parser.Category
command| imp ! $
na: TSyntax `ident
na)

end Mathlib.Tactic.imp

imp! Ring
Try this:
  [apply] import Ideal.Quotient.Index
Try this:
  [apply] import Sheaves.CommRingCat
Try this:
  [apply] import Ideal.Quotient.Noetherian
Try this:
  [apply] import Ideal.Quotient.Operations
Try this:
  [apply] import Algebra.IsSimpleRing
Try this:
  [apply] import BigOperators.Ring.Finset
Try this:
  [apply] import BigOperators.Ring.List
Try this:
  [apply] import BigOperators.Ring.Multiset
Try this:
  [apply] import BigOperators.Ring.Nat
Try this:
  [apply] import BigOperators.RingEquiv
Try this:
  [apply] import Category.BoolRing
Try this:
  [apply] import Category.ModuleCat.ChangeOfRings
Try this:
  [apply] import Category.ModuleCat.ChangeOfRingsExact
Try this:
  [apply] import Category.ModuleCat.Presheaf.ChangeOfRings
Try this:
  [apply] import Category.ModuleCat.Sheaf.ChangeOfRings
Try this:
  [apply] import Category.Ring.Adjunctions
Try this:
  [apply] import Category.Ring.Basic
Try this:
  [apply] import Category.Ring.Colimits
Try this:
  [apply] import Category.Ring.Constructions
Try this:
  [apply] import Category.Ring.Epi
Try this:
  [apply] import Category.Ring.EqualizerPushout
Try this:
  [apply] import Category.Ring.FilteredColimits
Try this:
  [apply] import Category.Ring.FinitePresentation
Try this:
  [apply] import Category.Ring.Instances
Try this:
  [apply] import Category.Ring.Limits
Try this:
  [apply] import Category.Ring.LinearAlgebra
Try this:
  [apply] import Category.Ring.Small
Try this:
  [apply] import Category.Ring.Topology
Try this:
  [apply] import Category.Ring.Under.Basic
Try this:
  [apply] import Category.Ring.Under.Limits
Try this:
  [apply] import Category.Ring.Under.Property
Try this:
  [apply] import CharP.LocalRing
Try this:
  [apply] import Colimit.Ring
Try this:
  [apply] import DirectSum.Ring
Try this:
  [apply] import LieRinehartAlgebra.Defs
Try this:
  [apply] import LieRinehartAlgebra.Subalgebra
Try this:
  [apply] import Module.LinearMap.DivisionRing
Try this:
  [apply] import Module.RingHom
Try this:
  [apply] import MvPolynomial.CommRing
Try this:
  [apply] import Order.BigOperators.Ring.Finset
Try this:
  [apply] import Order.BigOperators.Ring.List
Try this:
  [apply] import Order.BigOperators.Ring.Multiset
Try this:
  [apply] import Order.Floor.Ring
Try this:
  [apply] import Order.Hom.Ring
Try this:
  [apply] import Order.Nonneg.Ring
Try this:
  [apply] import Order.Positive.Ring
Try this:
  [apply] import Order.Ring.Abs
Try this:
  [apply] import Order.Ring.Archimedean
Try this:
  [apply] import Order.Ring.Basic
Try this:
  [apply] import Order.Ring.Canonical
Try this:
  [apply] import Order.Ring.Cast
Try this:
  [apply] import Order.Ring.Cone
Try this:
  [apply] import Order.Ring.Defs
Try this:
  [apply] import Order.Ring.Finset
Try this:
  [apply] import Order.Ring.GeomSum
Try this:
  [apply] import Order.Ring.Idempotent
Try this:
  [apply] import Order.Ring.InjSurj
Try this:
  [apply] import Order.Ring.Int
Try this:
  [apply] import Order.Ring.Interval
Try this:
  [apply] import Order.Ring.IsNonarchimedean
Try this:
  [apply] import Order.Ring.Nat
Try this:
  [apply] import Order.Ring.Opposite
Try this:
  [apply] import Order.Ring.Ordering.Basic
Try this:
  [apply] import Order.Ring.Ordering.Defs
Try this:
  [apply] import Order.Ring.Pow
Try this:
  [apply] import Order.Ring.Prod
Try this:
  [apply] import Order.Ring.Rat
Try this:
  [apply] import Order.Ring.StandardPart
Try this:
  [apply] import Order.Ring.Star
Try this:
  [apply] import Order.Ring.Synonym
Try this:
  [apply] import Order.Ring.Unbundled.Basic
Try this:
  [apply] import Order.Ring.Unbundled.Rat
Try this:
  [apply] import Order.Ring.Units
Try this:
  [apply] import Order.Ring.WithTop
Try this:
  [apply] import Polynomial.GroupRingAction
Try this:
  [apply] import Polynomial.RingDivision
Try this:
  [apply] import Ring.Action.Basic
Try this:
  [apply] import Ring.Action.ConjAct
Try this:
  [apply] import Ring.Action.End
Try this:
  [apply] import Ring.Action.Field
Try this:
  [apply] import Ring.Action.Group
Try this:
  [apply] import Ring.Action.Invariant
Try this:
  [apply] import Ring.Action.Pointwise.Finset
Try this:
  [apply] import Ring.Action.Pointwise.Set
Try this:
  [apply] import Ring.Action.Rat
Try this:
  [apply] import Ring.Action.Submonoid
Try this:
  [apply] import Ring.Action.Subobjects
Try this:
  [apply] import Ring.AddAut
Try this:
  [apply] import Ring.Associated
Try this:
  [apply] import Ring.Associator
Try this:
  [apply] import Ring.Aut
Try this:
  [apply] import Ring.Basic
Try this:
  [apply] import Ring.BooleanRing
Try this:
  [apply] import Ring.Center
Try this:
  [apply] import Ring.Centralizer
Try this:
  [apply] import Ring.CentroidHom
Try this:
  [apply] import Ring.CharZero
Try this:
  [apply] import Ring.Commute
Try this:
  [apply] import Ring.CompTypeclasses
Try this:
  [apply] import Ring.Defs
Try this:
  [apply] import Ring.Divisibility.Basic
Try this:
  [apply] import Ring.Divisibility.Lemmas
Try this:
  [apply] import Ring.Equiv
Try this:
  [apply] import Ring.Ext
Try this:
  [apply] import Ring.Fin
Try this:
  [apply] import Ring.GeomSum
Try this:
  [apply] import Ring.GrindInstances
Try this:
  [apply] import Ring.Hom.Defs
Try this:
  [apply] import Ring.Hom.InjSurj
Try this:
  [apply] import Ring.Idempotent
Try this:
  [apply] import Ring.Identities
Try this:
  [apply] import Ring.InjSurj
Try this:
  [apply] import Ring.Int.Defs
Try this:
  [apply] import Ring.Int.Field
Try this:
  [apply] import Ring.Int.Parity
Try this:
  [apply] import Ring.Int.Units
Try this:
  [apply] import Ring.Invertible
Try this:
  [apply] import Ring.IsFormallyReal
Try this:
  [apply] import Ring.MinimalAxioms
Try this:
  [apply] import Ring.Nat
Try this:
  [apply] import Ring.NegOnePow
Try this:
  [apply] import Ring.NonZeroDivisors
Try this:
  [apply] import Ring.Opposite
Try this:
  [apply] import Ring.PUnit
Try this:
  [apply] import Ring.Parity
Try this:
  [apply] import Ring.Periodic
Try this:
  [apply] import Ring.Pi
Try this:
  [apply] import Ring.Pointwise.Finset
Try this:
  [apply] import Ring.Pointwise.Set
Try this:
  [apply] import Ring.Prod
Try this:
  [apply] import Ring.Rat
Try this:
  [apply] import Ring.Regular
Try this:
  [apply] import Ring.Semiconj
Try this:
  [apply] import Ring.Semireal.Defs
Try this:
  [apply] import Ring.Shrink
Try this:
  [apply] import Ring.Subgroup
Try this:
  [apply] import Ring.Submonoid.Basic
Try this:
  [apply] import Ring.Submonoid.Pointwise
Try this:
  [apply] import Ring.Subring.Basic
Try this:
  [apply] import Ring.Subring.Defs
Try this:
  [apply] import Ring.Subring.IntPolynomial
Try this:
  [apply] import Ring.Subring.MulOpposite
Try this:
  [apply] import Ring.Subring.Order
Try this:
  [apply] import Ring.Subring.Pointwise
Try this:
  [apply] import Ring.Subring.Units
Try this:
  [apply] import Ring.Subsemiring.Basic
Try this:
  [apply] import Ring.Subsemiring.Defs
Try this:
  [apply] import Ring.Subsemiring.MulOpposite
Try this:
  [apply] import Ring.Subsemiring.Order
Try this:
  [apply] import Ring.Subsemiring.Pointwise
Try this:
  [apply] import Ring.SumsOfSquares
Try this:
  [apply] import Ring.Torsion
Try this:
  [apply] import Ring.TransferInstance
Try this:
  [apply] import Ring.ULift
Try this:
  [apply] import Ring.Units
Try this:
  [apply] import Ring.WithZero
Try this:
  [apply] import RingQuot
Try this:
  [apply] import Star.RingQuot
Try this:
  [apply] import Star.StarRingHom
Try this:
  [apply] import Morphisms.RingHomProperties
Try this:
  [apply] import RelativeGluing
Try this:
  [apply] import Complex.RemovableSingularity
Try this:
  [apply] import Complex.RiemannMapping
Try this:
  [apply] import InnerProductSpace.Reproducing
Try this:
  [apply] import Normed.Ring.Basic
Try this:
  [apply] import Normed.Ring.Finite
Try this:
  [apply] import Normed.Ring.InfiniteProd
Try this:
  [apply] import Normed.Ring.InfiniteSum
Try this:
  [apply] import Normed.Ring.Int
Try this:
  [apply] import Normed.Ring.Lemmas
Try this:
  [apply] import Normed.Ring.TransferInstance
Try this:
  [apply] import Normed.Ring.Ultra
Try this:
  [apply] import Normed.Ring.Units
Try this:
  [apply] import Normed.Ring.WithAbs
Try this:
  [apply] import Normed.Unbundled.RingSeminorm
Try this:
  [apply] import SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder
Try this:
  [apply] import Monoidal.Cartesian.Ring
Try this:
  [apply] import Monoidal.Ring
Try this:
  [apply] import Additive.RuzsaCovering
Try this:
  [apply] import FunLike.Ring
Try this:
  [apply] import Nat.Cast.Order.Ring
Try this:
  [apply] import Real.Embedding
Try this:
  [apply] import ZMod.QuotientRing
Try this:
  [apply] import Manifold.Sheaf.LocallyRingedSpace
Try this:
  [apply] import RingedSpace.Basic
Try this:
  [apply] import RingedSpace.LocallyRingedSpace
Try this:
  [apply] import RingedSpace.LocallyRingedSpace.HasColimits
Try this:
  [apply] import RingedSpace.LocallyRingedSpace.ResidueField
Try this:
  [apply] import RingedSpace.OpenImmersion
Try this:
  [apply] import RingedSpace.PresheafedSpace
Try this:
  [apply] import RingedSpace.PresheafedSpace.Gluing
Try this:
  [apply] import RingedSpace.PresheafedSpace.HasColimits
Try this:
  [apply] import RingedSpace.SheafedSpace
Try this:
  [apply] import RingedSpace.Stalks
Try this:
  [apply] import GroupAction.Ring
Try this:
  [apply] import Dimension.DivisionRing
Try this:
  [apply] import RootSystem.RootPairingCat
Try this:
  [apply] import Algebra.Ring.Basic
Try this:
  [apply] import Algebra.Ring.Definability
Try this:
  [apply] import Algebra.Ring.FreeCommRing
Try this:
  [apply] import HeckeRing.Defs
Try this:
  [apply] import ModularForms.LevelOne.GradedRing
Try this:
  [apply] import NumberField.AdeleRing
Try this:
  [apply] import NumberField.InfiniteAdeleRing
Try this:
  [apply] import Padics.RingHoms
Try this:
  [apply] import Filter.AtTopBot.Ring
Try this:
  [apply] import Filter.Ring
Try this:
  [apply] import FinGroupCharZero
Try this:
  [apply] import Homological.GroupCohomology.LongExactSequence
Try this:
  [apply] import Homological.GroupHomology.LongExactSequence
Try this:
  [apply] import Intertwining
Try this:
  [apply] import AdicCompletion.Algebra
Try this:
  [apply] import AdicCompletion.AsTensorProduct
Try this:
  [apply] import AdicCompletion.Basic
Try this:
  [apply] import AdicCompletion.Completeness
Try this:
  [apply] import AdicCompletion.Exactness
Try this:
  [apply] import AdicCompletion.Functoriality
Try this:
  [apply] import AdicCompletion.LocalRing
Try this:
  [apply] import AdicCompletion.Noetherian
Try this:
  [apply] import AdicCompletion.RingHom
Try this:
  [apply] import AdicCompletion.Topology
Try this:
  [apply] import Adjoin.Basic
Try this:
  [apply] import Adjoin.Dimension
Try this:
  [apply] import Adjoin.FG
Try this:
  [apply] import Adjoin.FGBaseChange
Try this:
  [apply] import Adjoin.Field
Try this:
  [apply] import Adjoin.Polynomial
Try this:
  [apply] import Adjoin.Polynomial.Basic
Try this:
  [apply] import Adjoin.Polynomial.Bivariate
Try this:
  [apply] import Adjoin.PowerBasis
Try this:
  [apply] import Adjoin.Singleton
Try this:
  [apply] import Adjoin.Tower
Try this:
  [apply] import AdjoinRoot
Try this:
  [apply] import AlgebraTower
Try this:
  [apply] import Algebraic.Basic
Try this:
  [apply] import Algebraic.Cardinality
Try this:
  [apply] import Algebraic.Defs
Try this:
  [apply] import Algebraic.Integral
Try this:
  [apply] import Algebraic.LinearIndependent
Try this:
  [apply] import Algebraic.MvPolynomial
Try this:
  [apply] import Algebraic.Pi
Try this:
  [apply] import Algebraic.StronglyTranscendental
Try this:
  [apply] import AlgebraicIndependent.Adjoin
Try this:
  [apply] import AlgebraicIndependent.AlgebraicClosure
Try this:
  [apply] import AlgebraicIndependent.Basic
Try this:
  [apply] import AlgebraicIndependent.Defs
Try this:
  [apply] import AlgebraicIndependent.RankAndCardinality
Try this:
  [apply] import AlgebraicIndependent.TranscendenceBasis
Try this:
  [apply] import AlgebraicIndependent.Transcendental
Try this:
  [apply] import Artinian.Algebra
Try this:
  [apply] import Artinian.Defs
Try this:
  [apply] import Artinian.Instances
Try this:
  [apply] import Artinian.Module
Try this:
  [apply] import Artinian.Ring
Try this:
  [apply] import Bezout
Try this:
  [apply] import Bialgebra.Basic
Try this:
  [apply] import Bialgebra.Convolution
Try this:
  [apply] import Bialgebra.Equiv
Try this:
  [apply] import Bialgebra.GroupLike
Try this:
  [apply] import Bialgebra.Hom
Try this:
  [apply] import Bialgebra.MonoidAlgebra
Try this:
  [apply] import Bialgebra.Quotient
Try this:
  [apply] import Bialgebra.SymmetricAlgebra
Try this:
  [apply] import Bialgebra.TensorProduct
Try this:
  [apply] import Binomial
Try this:
  [apply] import ChainOfDivisors
Try this:
  [apply] import ClassGroup
Try this:
  [apply] import ClassGroup.Basic
Try this:
  [apply] import ClassGroup.ExtendedHom
Try this:
  [apply] import Coalgebra.Basic
Try this:
  [apply] import Coalgebra.CoassocSimps
Try this:
  [apply] import Coalgebra.Convolution
Try this:
  [apply] import Coalgebra.Equiv
Try this:
  [apply] import Coalgebra.GroupLike
Try this:
  [apply] import Coalgebra.Hom
Try this:
  [apply] import Coalgebra.MonoidAlgebra
Try this:
  [apply] import Coalgebra.MulOpposite
Try this:
  [apply] import Coalgebra.Quotient
Try this:
  [apply] import Coalgebra.TensorProduct
Try this:
  [apply] import Complex
Try this:
  [apply] import Conductor
Try this:
  [apply] import Congruence.Basic
Try this:
  [apply] import Congruence.BigOperators
Try this:
  [apply] import Congruence.Defs
Try this:
  [apply] import Congruence.Hom
Try this:
  [apply] import Congruence.Opposite
Try this:
  [apply] import Congruence.Star
Try this:
  [apply] import Coprime.Basic
Try this:
  [apply] import Coprime.Ideal
Try this:
  [apply] import Coprime.Lemmas
Try this:
  [apply] import DedekindDomain.AdicValuation
Try this:
  [apply] import DedekindDomain.Basic
Try this:
  [apply] import DedekindDomain.Different
Try this:
  [apply] import DedekindDomain.Dvr
Try this:
  [apply] import DedekindDomain.Factorization
Try this:
  [apply] import DedekindDomain.FiniteAdeleRing
Try this:
  [apply] import DedekindDomain.GaussLemma
Try this:
  [apply] import DedekindDomain.Ideal.Basic
Try this:
  [apply] import DedekindDomain.Ideal.Lemmas
Try this:
  [apply] import DedekindDomain.Instances
Try this:
  [apply] import DedekindDomain.IntegralClosure
Try this:
  [apply] import DedekindDomain.LinearDisjoint
Try this:
  [apply] import DedekindDomain.PID
Try this:
  [apply] import DedekindDomain.SInteger
Try this:
  [apply] import DedekindDomain.SelmerGroup
Try this:
  [apply] import Depth.Rees
Try this:
  [apply] import Derivation.Basic
Try this:
  [apply] import Derivation.DifferentialRing
Try this:
  [apply] import Derivation.Lie
Try this:
  [apply] import Derivation.MapCoeffs
Try this:
  [apply] import Derivation.ToSquareZero
Try this:
  [apply] import DiscreteValuationRing.Basic
Try this:
  [apply] import DiscreteValuationRing.TFAE
Try this:
  [apply] import Discriminant
Try this:
  [apply] import DividedPowerAlgebra.Init
Try this:
  [apply] import DividedPowers.Basic
Try this:
  [apply] import DividedPowers.DPMorphism
Try this:
  [apply] import DividedPowers.Padic
Try this:
  [apply] import DividedPowers.RatAlgebra
Try this:
  [apply] import DividedPowers.SubDPIdeal
Try this:
  [apply] import DualNumber
Try this:
  [apply] import EssentialFiniteness
Try this:
  [apply] import Etale.Basic
Try this:
  [apply] import Etale.Descent
Try this:
  [apply] import Etale.Field
Try this:
  [apply] import Etale.Finite
Try this:
  [apply] import Etale.Kaehler
Try this:
  [apply] import Etale.Locus
Try this:
  [apply] import Etale.Pi
Try this:
  [apply] import Etale.QuasiFinite
Try this:
  [apply] import Etale.StandardEtale
Try this:
  [apply] import Etale.Weakly
Try this:
  [apply] import EuclideanDomain
Try this:
  [apply] import Extension.Basic
Try this:
  [apply] import Extension.Cotangent.BaseChange
Try this:
  [apply] import Extension.Cotangent.Basic
Try this:
  [apply] import Extension.Cotangent.Basis
Try this:
  [apply] import Extension.Cotangent.Free
Try this:
  [apply] import Extension.Cotangent.LocalizationAway
Try this:
  [apply] import Extension.ExtendScalars
Try this:
  [apply] import Extension.Generators
Try this:
  [apply] import Extension.Presentation.Basic
Try this:
  [apply] import Extension.Presentation.Core
Try this:
  [apply] import Extension.Presentation.Submersive
Try this:
  [apply] import FilteredAlgebra.Basic
Try this:
  [apply] import Filtration
Try this:
  [apply] import FiniteLength
Try this:
  [apply] import FinitePresentation
Try this:
  [apply] import FiniteStability
Try this:
  [apply] import FiniteType
Try this:
  [apply] import Finiteness.Basic
Try this:
  [apply] import Finiteness.Bilinear
Try this:
  [apply] import Finiteness.Cardinality
Try this:
  [apply] import Finiteness.Cofinite
Try this:
  [apply] import Finiteness.Defs
Try this:
  [apply] import Finiteness.Descent
Try this:
  [apply] import Finiteness.FinitePresentationLocal
Try this:
  [apply] import Finiteness.FiniteTypeLocal
Try this:
  [apply] import Finiteness.Finsupp
Try this:
  [apply] import Finiteness.Ideal
Try this:
  [apply] import Finiteness.Lattice
Try this:
  [apply] import Finiteness.ModuleFinitePresentation
Try this:
  [apply] import Finiteness.Nakayama
Try this:
  [apply] import Finiteness.Nilpotent
Try this:
  [apply] import Finiteness.NilpotentKer
Try this:
  [apply] import Finiteness.Prod
Try this:
  [apply] import Finiteness.Projective
Try this:
  [apply] import Finiteness.Quotient
Try this:
  [apply] import Finiteness.Small
Try this:
  [apply] import Finiteness.Subalgebra
Try this:
  [apply] import Fintype
Try this:
  [apply] import Flat.Basic
Try this:
  [apply] import Flat.CategoryTheory
Try this:
  [apply] import Flat.Domain
Try this:
  [apply] import Flat.Equalizer
Try this:
  [apply] import Flat.EquationalCriterion
Try this:
  [apply] import Flat.FaithfullyFlat.Algebra
Try this:
  [apply] import Flat.FaithfullyFlat.Basic
Try this:
  [apply] import Flat.FaithfullyFlat.Descent
Try this:
  [apply] import Flat.IsBaseChange
Try this:
  [apply] import Flat.Localization
Try this:
  [apply] import Flat.LocallyFree
Try this:
  [apply] import Flat.Rank
Try this:
  [apply] import Flat.Stability
Try this:
  [apply] import Flat.Tensor
Try this:
  [apply] import Flat.TorsionFree
Try this:
  [apply] import FormalGroup.Basic
Try this:
  [apply] import FractionalIdeal.Basic
Try this:
  [apply] import FractionalIdeal.Extended
Try this:
  [apply] import FractionalIdeal.Inverse
Try this:
  [apply] import FractionalIdeal.Norm
Try this:
  [apply] import FractionalIdeal.Operations
Try this:
  [apply] import FreeCommRing
Try this:
  [apply] import FreeRing
Try this:
  [apply] import Frobenius
Try this:
  [apply] import GradedAlgebra.AlgHom
Try this:
  [apply] import GradedAlgebra.Basic
Try this:
  [apply] import GradedAlgebra.FiniteType
Try this:
  [apply] import GradedAlgebra.Homogeneous.Ideal
Try this:
  [apply] import GradedAlgebra.Homogeneous.Maps
Try this:
  [apply] import GradedAlgebra.Homogeneous.Submodule
Try this:
  [apply] import GradedAlgebra.Homogeneous.Subsemiring
Try this:
  [apply] import GradedAlgebra.HomogeneousLocalization
Try this:
  [apply] import GradedAlgebra.Noetherian
Try this:
  [apply] import GradedAlgebra.Radical
Try this:
  [apply] import GradedAlgebra.RingHom
Try this:
  [apply] import GradedAlgebra.TensorProduct
Try this:
  [apply] import Grassmannian
Try this:
  [apply] import HahnSeries.Addition
Try this:
  [apply] import HahnSeries.Basic
Try this:
  [apply] import HahnSeries.Binomial
Try this:
  [apply] import HahnSeries.Cardinal
Try this:
  [apply] import HahnSeries.HEval
Try this:
  [apply] import HahnSeries.HahnEmbedding
Try this:
  [apply] import HahnSeries.Lex
Try this:
  [apply] import HahnSeries.Multiplication
Try this:
  [apply] import HahnSeries.PowerSeries
Try this:
  [apply] import HahnSeries.Summable
Try this:
  [apply] import HahnSeries.Valuation
Try this:
  [apply] import Henselian
Try this:
  [apply] import HopfAlgebra.Basic
Try this:
  [apply] import HopfAlgebra.Convolution
Try this:
  [apply] import HopfAlgebra.GroupLike
Try this:
  [apply] import HopfAlgebra.MonoidAlgebra
Try this:
  [apply] import HopfAlgebra.Quotient
Try this:
  [apply] import HopfAlgebra.TensorProduct
Try this:
  [apply] import HopkinsLevitzki
Try this:
  [apply] import Ideal.AssociatedPrime.Basic
Try this:
  [apply] import Ideal.AssociatedPrime.Finiteness
Try this:
  [apply] import Ideal.AssociatedPrime.Localization
Try this:
  [apply] import Ideal.Basic
Try this:
  [apply] import Ideal.Basis
Try this:
  [apply] import Ideal.BigOperators
Try this:
  [apply] import Ideal.Colon
Try this:
  [apply] import Ideal.Cotangent
Try this:
  [apply] import Ideal.CotangentBaseChange
Try this:
  [apply] import Ideal.Defs
Try this:
  [apply] import Ideal.Finsupp
Try this:
  [apply] import Ideal.GoingDown
Try this:
  [apply] import Ideal.GoingUp
Try this:
  [apply] import Ideal.Height
Try this:
  [apply] import Ideal.IdempotentFG
Try this:
  [apply] import Ideal.Int
Try this:
  [apply] import Ideal.IsAugmentation
Try this:
  [apply] import Ideal.IsPrimary
Try this:
  [apply] import Ideal.IsPrincipal
Try this:
  [apply] import Ideal.IsPrincipalPowQuotient
Try this:
  [apply] import Ideal.KrullsHeightTheorem
Try this:
  [apply] import Ideal.Lattice
Try this:
  [apply] import Ideal.Maps
Try this:
  [apply] import Ideal.Maximal
Try this:
  [apply] import Ideal.MinimalPrime.Basic
Try this:
  [apply] import Ideal.MinimalPrime.Colon
Try this:
  [apply] import Ideal.MinimalPrime.Localization
Try this:
  [apply] import Ideal.MinimalPrime.Noetherian
Try this:
  [apply] import Ideal.MonicSpan
Try this:
  [apply] import Ideal.NatInt
Try this:
  [apply] import Ideal.Nonunits
Try this:
  [apply] import Ideal.Norm.AbsNorm
Try this:
  [apply] import Ideal.Norm.RelNorm
Try this:
  [apply] import Ideal.Oka
Try this:
  [apply] import Ideal.Operations
Try this:
  [apply] import Ideal.Over
Try this:
  [apply] import Ideal.Pointwise
Try this:
  [apply] import Ideal.Prime
Try this:
  [apply] import Ideal.Prod
Try this:
  [apply] import Ideal.Pure
Try this:
  [apply] import Ideal.Quotient.Basic
Try this:
  [apply] import Ideal.Quotient.ChineseRemainder
Try this:
  [apply] import Ideal.Quotient.Defs
Try this:
  [apply] import Ideal.Quotient.HasFiniteQuotients
Try this:
  [apply] import Ideal.Quotient.Nilpotent
Try this:
  [apply] import PowerSeries.Binomial
Try this:
  [apply] import Ideal.Quotient.Over
Try this:
  [apply] import Ideal.Quotient.PowTransition
Try this:
  [apply] import Ideal.Span
Try this:
  [apply] import Ideal.UFD
Try this:
  [apply] import IdealFilter.Basic
Try this:
  [apply] import IdealFilter.Topology
Try this:
  [apply] import Idempotents
Try this:
  [apply] import Int.Basic
Try this:
  [apply] import IntegralClosure.Algebra.Basic
Try this:
  [apply] import IntegralClosure.Algebra.Defs
Try this:
  [apply] import IntegralClosure.Algebra.Ideal
Try this:
  [apply] import IntegralClosure.GoingDown
Try this:
  [apply] import IntegralClosure.IntegralRestrict
Try this:
  [apply] import IntegralClosure.IntegrallyClosed
Try this:
  [apply] import IntegralClosure.IsIntegral.AlmostIntegral
Try this:
  [apply] import IntegralClosure.IsIntegral.Basic
Try this:
  [apply] import IntegralClosure.IsIntegral.Defs
Try this:
  [apply] import IntegralClosure.IsIntegralClosure.Basic
Try this:
  [apply] import IntegralClosure.IsIntegralClosure.Defs
Try this:
  [apply] import IntegralDomain
Try this:
  [apply] import Invariant.Basic
Try this:
  [apply] import Invariant.Defs
Try this:
  [apply] import Invariant.Galois
Try this:
  [apply] import Invariant.Profinite
Try this:
  [apply] import IsAdjoinRoot
Try this:
  [apply] import IsGaloisGroup.Basic
Try this:
  [apply] import IsGaloisGroup.Defs
Try this:
  [apply] import IsPrimary
Try this:
  [apply] import IsTensorProduct
Try this:
  [apply] import Jacobson.Artinian
Try this:
  [apply] import Jacobson.Ideal
Try this:
  [apply] import Jacobson.Polynomial
Try this:
  [apply] import Jacobson.Radical
Try this:
  [apply] import Jacobson.Ring
Try this:
  [apply] import Jacobson.Semiprimary
Try this:
  [apply] import Kaehler.Basic
Try this:
  [apply] import Kaehler.JacobiZariski
Try this:
  [apply] import Kaehler.Polynomial
Try this:
  [apply] import Kaehler.TensorProduct
Try this:
  [apply] import KrullDimension.Basic
Try this:
  [apply] import KrullDimension.Field
Try this:
  [apply] import KrullDimension.LocalRing
Try this:
  [apply] import KrullDimension.Module
Try this:
  [apply] import KrullDimension.NonZeroDivisors
Try this:
  [apply] import KrullDimension.PID
Try this:
  [apply] import KrullDimension.Polynomial
Try this:
  [apply] import KrullDimension.Regular
Try this:
  [apply] import KrullDimension.Zero
Try this:
  [apply] import Lasker
Try this:
  [apply] import LaurentSeries
Try this:
  [apply] import Length
Try this:
  [apply] import LinearDisjoint
Try this:
  [apply] import LittleWedderburn
Try this:
  [apply] import LocalIso
Try this:
  [apply] import LocalProperties.Basic
Try this:
  [apply] import LocalProperties.Exactness
Try this:
  [apply] import LocalProperties.FinitePresentation
Try this:
  [apply] import LocalProperties.Injective
Try this:
  [apply] import LocalProperties.InjectiveDimension
Try this:
  [apply] import LocalProperties.IntegrallyClosed
Try this:
  [apply] import LocalProperties.Projective
Try this:
  [apply] import LocalProperties.ProjectiveDimension
Try this:
  [apply] import LocalProperties.Reduced
Try this:
  [apply] import LocalProperties.Semilocal
Try this:
  [apply] import LocalProperties.Submodule
Try this:
  [apply] import LocalRing.Basic
Try this:
  [apply] import LocalRing.Defs
Try this:
  [apply] import LocalRing.Etale
Try this:
  [apply] import LocalRing.Length
Try this:
  [apply] import LocalRing.LocalSubring
Try this:
  [apply] import LocalRing.MaximalIdeal.Basic
Try this:
  [apply] import LocalRing.MaximalIdeal.Defs
Try this:
  [apply] import LocalRing.MaximalIdeal.Square
Try this:
  [apply] import LocalRing.Module
Try this:
  [apply] import LocalRing.NonLocalRing
Try this:
  [apply] import LocalRing.Pullback
Try this:
  [apply] import LocalRing.Quotient
Try this:
  [apply] import LocalRing.ResidueField.Basic
Try this:
  [apply] import LocalRing.ResidueField.Defs
Try this:
  [apply] import LocalRing.ResidueField.Fiber
Try this:
  [apply] import LocalRing.ResidueField.Ideal
Try this:
  [apply] import LocalRing.ResidueField.Instances
Try this:
  [apply] import LocalRing.ResidueField.Polynomial
Try this:
  [apply] import LocalRing.RingHom.Basic
Try this:
  [apply] import LocalRing.Subring
Try this:
  [apply] import Localization.Algebra
Try this:
  [apply] import Localization.AsSubring
Try this:
  [apply] import Localization.AtPrime.Basic
Try this:
  [apply] import Localization.AtPrime.Extension
Try this:
  [apply] import Localization.Away.AdjoinRoot
Try this:
  [apply] import Localization.Away.Basic
Try this:
  [apply] import Localization.Away.Lemmas
Try this:
  [apply] import Localization.BaseChange
Try this:
  [apply] import Localization.Basic
Try this:
  [apply] import Localization.Cardinality
Try this:
  [apply] import Localization.Defs
Try this:
  [apply] import Localization.Finiteness
Try this:
  [apply] import Localization.FractionRing
Try this:
  [apply] import Localization.Free
Try this:
  [apply] import Localization.Ideal
Try this:
  [apply] import Localization.Integer
Try this:
  [apply] import Localization.Integral
Try this:
  [apply] import Localization.InvSubmonoid
Try this:
  [apply] import Localization.LocalizationLocalization
Try this:
  [apply] import Localization.Module
Try this:
  [apply] import Localization.NormTrace
Try this:
  [apply] import Localization.NumDen
Try this:
  [apply] import Localization.Pi
Try this:
  [apply] import Localization.Rat
Try this:
  [apply] import Localization.Submodule
Try this:
  [apply] import MatrixAlgebra
Try this:
  [apply] import MatrixPolynomialAlgebra
Try this:
  [apply] import Morita.Basic
Try this:
  [apply] import Morita.Matrix
Try this:
  [apply] import Multiplicity
Try this:
  [apply] import MvPolynomial
Try this:
  [apply] import MvPolynomial.Basic
Try this:
  [apply] import MvPolynomial.EulerIdentity
Try this:
  [apply] import MvPolynomial.Expand
Try this:
  [apply] import MvPolynomial.FreeCommRing
Try this:
  [apply] import MvPolynomial.Groebner
Try this:
  [apply] import MvPolynomial.Homogeneous
Try this:
  [apply] import MvPolynomial.Ideal
Try this:
  [apply] import MvPolynomial.IrreducibleQuadratic
Try this:
  [apply] import MvPolynomial.Localization
Try this:
  [apply] import MvPolynomial.MonomialOrder
Try this:
  [apply] import MvPolynomial.MonomialOrder.DegLex
Try this:
  [apply] import MvPolynomial.Symmetric.Defs
Try this:
  [apply] import MvPolynomial.Symmetric.FundamentalTheorem
Try this:
  [apply] import MvPolynomial.Symmetric.NewtonIdentities
Try this:
  [apply] import MvPolynomial.Tower
Try this:
  [apply] import MvPolynomial.WeightedHomogeneous
Try this:
  [apply] import MvPowerSeries.Basic
Try this:
  [apply] import MvPowerSeries.Equiv
Try this:
  [apply] import MvPowerSeries.Evaluation
Try this:
  [apply] import MvPowerSeries.Expand
Try this:
  [apply] import MvPowerSeries.GaussNorm
Try this:
  [apply] import MvPowerSeries.Inverse
Try this:
  [apply] import MvPowerSeries.LexOrder
Try this:
  [apply] import MvPowerSeries.LinearTopology
Try this:
  [apply] import MvPowerSeries.NoZeroDivisors
Try this:
  [apply] import MvPowerSeries.Order
Try this:
  [apply] import MvPowerSeries.PiTopology
Try this:
  [apply] import MvPowerSeries.Rename
Try this:
  [apply] import MvPowerSeries.Restricted
Try this:
  [apply] import MvPowerSeries.Substitution
Try this:
  [apply] import MvPowerSeries.Trunc
Try this:
  [apply] import Nakayama
Try this:
  [apply] import Nilpotent.Basic
Try this:
  [apply] import Nilpotent.Defs
Try this:
  [apply] import Nilpotent.Exp
Try this:
  [apply] import Nilpotent.GeometricallyReduced
Try this:
  [apply] import Nilpotent.Lemmas
Try this:
  [apply] import NoetherNormalization
Try this:
  [apply] import Noetherian.Basic
Try this:
  [apply] import Noetherian.Defs
Try this:
  [apply] import Noetherian.Filter
Try this:
  [apply] import Noetherian.Nilpotent
Try this:
  [apply] import Noetherian.OfPrime
Try this:
  [apply] import Noetherian.Orzech
Try this:
  [apply] import Noetherian.UniqueFactorizationDomain
Try this:
  [apply] import NonUnitalSubring.Basic
Try this:
  [apply] import NonUnitalSubring.Defs
Try this:
  [apply] import NonUnitalSubsemiring.Basic
Try this:
  [apply] import NonUnitalSubsemiring.Defs
Try this:
  [apply] import Norm.Basic
Try this:
  [apply] import Norm.Defs
Try this:
  [apply] import Norm.Transitivity
Try this:
  [apply] import NormTrace
Try this:
  [apply] import NormalClosure
Try this:
  [apply] import Nullstellensatz
Try this:
  [apply] import OrderOfVanishing.Basic
Try this:
  [apply] import OrderOfVanishing.Noetherian
Try this:
  [apply] import OreLocalization.Basic
Try this:
  [apply] import OreLocalization.Cardinality
Try this:
  [apply] import OreLocalization.NonZeroDivisors
Try this:
  [apply] import OreLocalization.OreSet
Try this:
  [apply] import OreLocalization.Ring
Try this:
  [apply] import OrzechProperty
Try this:
  [apply] import Perfection
Try this:
  [apply] import Perfectoid.BDeRham
Try this:
  [apply] import Perfectoid.FontaineTheta
Try this:
  [apply] import Perfectoid.Untilt
Try this:
  [apply] import PiTensorProduct
Try this:
  [apply] import PicardGroup
Try this:
  [apply] import Polynomial.Basic
Try this:
  [apply] import Polynomial.Bernstein
Try this:
  [apply] import Polynomial.Chebyshev
Try this:
  [apply] import Polynomial.Content
Try this:
  [apply] import Polynomial.ContentIdeal
Try this:
  [apply] import Polynomial.Cyclotomic.Basic
Try this:
  [apply] import Polynomial.Cyclotomic.Eval
Try this:
  [apply] import Polynomial.Cyclotomic.Expand
Try this:
  [apply] import Polynomial.Cyclotomic.Factorization
Try this:
  [apply] import Polynomial.Cyclotomic.Roots
Try this:
  [apply] import Polynomial.DegreeLT
Try this:
  [apply] import Polynomial.Dickson
Try this:
  [apply] import Polynomial.Eisenstein.Basic
Try this:
  [apply] import Polynomial.Eisenstein.Criterion
Try this:
  [apply] import Polynomial.Eisenstein.Distinguished
Try this:
  [apply] import Polynomial.Eisenstein.IsIntegral
Try this:
  [apply] import Polynomial.GaussLemma
Try this:
  [apply] import Polynomial.GaussNorm
Try this:
  [apply] import Polynomial.Hermite.Basic
Try this:
  [apply] import Polynomial.Hermite.Gaussian
Try this:
  [apply] import Polynomial.HilbertPoly
Try this:
  [apply] import Polynomial.Ideal
Try this:
  [apply] import Polynomial.IntegralNormalization
Try this:
  [apply] import Polynomial.IrreducibleRing
Try this:
  [apply] import Polynomial.IsIntegral
Try this:
  [apply] import Polynomial.Morse
Try this:
  [apply] import Polynomial.Nilpotent
Try this:
  [apply] import Polynomial.Opposites
Try this:
  [apply] import Polynomial.Pochhammer
Try this:
  [apply] import Polynomial.Quotient
Try this:
  [apply] import Polynomial.Radical
Try this:
  [apply] import Polynomial.RationalRoot
Try this:
  [apply] import Polynomial.Resultant.Basic
Try this:
  [apply] import Polynomial.ScaleRoots
Try this:
  [apply] import Polynomial.Selmer
Try this:
  [apply] import Polynomial.SeparableDegree
Try this:
  [apply] import Polynomial.ShiftedLegendre
Try this:
  [apply] import Polynomial.SmallDegreeVieta
Try this:
  [apply] import Polynomial.Subring
Try this:
  [apply] import Polynomial.Tower
Try this:
  [apply] import Polynomial.UniqueFactorization
Try this:
  [apply] import Polynomial.UniversalFactorizationRing
Try this:
  [apply] import Polynomial.Vieta
Try this:
  [apply] import Polynomial.Wronskian
Try this:
  [apply] import PolynomialAlgebra
Try this:
  [apply] import PolynomialLaw.Basic
Try this:
  [apply] import PowerBasis
Try this:
  [apply] import PowerSeries.Basic
Try this:
  [apply] import Spectrum.Prime.Polynomial
Try this:
  [apply] import PowerSeries.Catalan
Try this:
  [apply] import PowerSeries.CoeffMulMem
Try this:
  [apply] import PowerSeries.Derivative
Try this:
  [apply] import PowerSeries.Evaluation
Try this:
  [apply] import PowerSeries.Exp
Try this:
  [apply] import PowerSeries.Expand
Try this:
  [apply] import PowerSeries.GaussNorm
Try this:
  [apply] import PowerSeries.Ideal
Try this:
  [apply] import PowerSeries.Inverse
Try this:
  [apply] import PowerSeries.Log
Try this:
  [apply] import PowerSeries.NoZeroDivisors
Try this:
  [apply] import PowerSeries.Order
Try this:
  [apply] import PowerSeries.PiTopology
Try this:
  [apply] import PowerSeries.Restricted
Try this:
  [apply] import PowerSeries.Schroder
Try this:
  [apply] import PowerSeries.Substitution
Try this:
  [apply] import PowerSeries.Trunc
Try this:
  [apply] import PowerSeries.WeierstrassPreparation
Try this:
  [apply] import PowerSeries.WellKnown
Try this:
  [apply] import Prime
Try this:
  [apply] import PrincipalIdealDomain
Try this:
  [apply] import PrincipalIdealDomainOfPrime
Try this:
  [apply] import QuasiFinite.Basic
Try this:
  [apply] import QuasiFinite.Polynomial
Try this:
  [apply] import QuasiFinite.Weakly
Try this:
  [apply] import QuotSMulTop
Try this:
  [apply] import Radical
Try this:
  [apply] import Radical.Basic
Try this:
  [apply] import Radical.NatInt
Try this:
  [apply] import RamificationInertia.Basic
Try this:
  [apply] import RamificationInertia.Inertia
Try this:
  [apply] import RamificationInertia.Ramification
Try this:
  [apply] import ReesAlgebra
Try this:
  [apply] import Regular.Category
Try this:
  [apply] import Regular.Depth
Try this:
  [apply] import Regular.Flat
Try this:
  [apply] import Regular.Free
Try this:
  [apply] import Regular.IsSMulRegular
Try this:
  [apply] import Regular.LinearMap
Try this:
  [apply] import Regular.ProjectiveDimension
Try this:
  [apply] import Regular.RegularSequence
Try this:
  [apply] import RegularLocalRing.Defs
Try this:
  [apply] import RegularLocalRing.Polynomial
Try this:
  [apply] import RingHom.Bijective
Try this:
  [apply] import RingHom.EssFiniteType
Try this:
  [apply] import RingHom.Etale
Try this:
  [apply] import RingHom.FaithfullyFlat
Try this:
  [apply] import RingHom.Finite
Try this:
  [apply] import RingHom.FinitePresentation
Try this:
  [apply] import RingHom.FiniteType
Try this:
  [apply] import RingHom.Flat
Try this:
  [apply] import RingHom.Injective
Try this:
  [apply] import RingHom.Integral
Try this:
  [apply] import RingHom.Locally
Try this:
  [apply] import RingHom.LocallyStandardSmooth
Try this:
  [apply] import RingHom.OpenImmersion
Try this:
  [apply] import RingHom.PurelyInseparable
Try this:
  [apply] import RingHom.QuasiFinite
Try this:
  [apply] import RingHom.Smooth
Try this:
  [apply] import RingHom.StandardSmooth
Try this:
  [apply] import RingHom.Surjective
Try this:
  [apply] import RingHom.Unramified
Try this:
  [apply] import RingHomProperties
Try this:
  [apply] import RingInvo
Try this:
  [apply] import RootsOfUnity.AlgebraicallyClosed
Try this:
  [apply] import RootsOfUnity.Basic
Try this:
  [apply] import RootsOfUnity.Complex
Try this:
  [apply] import RootsOfUnity.CyclotomicUnits
Try this:
  [apply] import RootsOfUnity.EnoughRootsOfUnity
Try this:
  [apply] import RootsOfUnity.Lemmas
Try this:
  [apply] import RootsOfUnity.Minpoly
Try this:
  [apply] import RootsOfUnity.PrimitiveRoots
Try this:
  [apply] import SimpleModule.Basic
Try this:
  [apply] import SimpleModule.InjectiveProjective
Try this:
  [apply] import SimpleModule.IsAlgClosed
Try this:
  [apply] import SimpleModule.Isotypic
Try this:
  [apply] import SimpleModule.Rank
Try this:
  [apply] import SimpleModule.WedderburnArtin
Try this:
  [apply] import SimpleRing.Basic
Try this:
  [apply] import SimpleRing.Congr
Try this:
  [apply] import SimpleRing.Defs
Try this:
  [apply] import SimpleRing.DivisionRing
Try this:
  [apply] import SimpleRing.Field
Try this:
  [apply] import SimpleRing.Matrix
Try this:
  [apply] import SimpleRing.Principal
Try this:
  [apply] import Smooth.AdicCompletion
Try this:
  [apply] import Smooth.Basic
Try this:
  [apply] import Smooth.Fiber
Try this:
  [apply] import Smooth.Field
Try this:
  [apply] import Smooth.Flat
Try this:
  [apply] import Smooth.IntegralClosure
Try this:
  [apply] import Smooth.Kaehler
Try this:
  [apply] import Smooth.Local
Try this:
  [apply] import Smooth.Locus
Try this:
  [apply] import Smooth.NoetherianDescent
Try this:
  [apply] import Smooth.Pi
Try this:
  [apply] import Smooth.Quotient
Try this:
  [apply] import Smooth.StandardSmooth
Try this:
  [apply] import Smooth.StandardSmoothCotangent
Try this:
  [apply] import Smooth.StandardSmoothOfFree
Try this:
  [apply] import Spectrum.Maximal.Basic
Try this:
  [apply] import Spectrum.Maximal.Defs
Try this:
  [apply] import Spectrum.Maximal.Localization
Try this:
  [apply] import Spectrum.Maximal.Topology
Try this:
  [apply] import Spectrum.Prime.Basic
Try this:
  [apply] import Spectrum.Prime.Chevalley
Try this:
  [apply] import Spectrum.Prime.ChevalleyComplexity
Try this:
  [apply] import Spectrum.Prime.ConstructibleSet
Try this:
  [apply] import Spectrum.Prime.Defs
Try this:
  [apply] import Spectrum.Prime.FreeLocus
Try this:
  [apply] import Spectrum.Prime.Homeomorph
Try this:
  [apply] import Spectrum.Prime.IsOpenComapC
Try this:
  [apply] import Spectrum.Prime.Jacobson
Try this:
  [apply] import Spectrum.Prime.LTSeries
Try this:
  [apply] import Spectrum.Prime.Module
Try this:
  [apply] import Spectrum.Prime.Noetherian
Try this:
  [apply] import Valuation.Discrete.IsDiscreteValuationRing
Try this:
  [apply] import Spectrum.Prime.RingHom
Try this:
  [apply] import Spectrum.Prime.TensorProduct
Try this:
  [apply] import Spectrum.Prime.Topology
Try this:
  [apply] import Support
Try this:
  [apply] import SurjectiveOnStalks
Try this:
  [apply] import Teichmuller
Try this:
  [apply] import TensorProduct.Basic
Try this:
  [apply] import TensorProduct.DirectLimitFG
Try this:
  [apply] import TensorProduct.Finite
Try this:
  [apply] import TensorProduct.Free
Try this:
  [apply] import TensorProduct.IncludeLeftSubRight
Try this:
  [apply] import TensorProduct.IsBaseChangeFree
Try this:
  [apply] import TensorProduct.IsBaseChangeHom
Try this:
  [apply] import TensorProduct.IsBaseChangePi
Try this:
  [apply] import TensorProduct.IsBaseChangeRightExact
Try this:
  [apply] import TensorProduct.Maps
Try this:
  [apply] import TensorProduct.MonoidAlgebra
Try this:
  [apply] import TensorProduct.MvPolynomial
Try this:
  [apply] import TensorProduct.Nontrivial
Try this:
  [apply] import TensorProduct.Pi
Try this:
  [apply] import TensorProduct.Quotient
Try this:
  [apply] import TotallySplit
Try this:
  [apply] import Trace.Basic
Try this:
  [apply] import Trace.Defs
Try this:
  [apply] import Trace.Quotient
Try this:
  [apply] import TwoSidedIdeal.Basic
Try this:
  [apply] import TwoSidedIdeal.BigOperators
Try this:
  [apply] import TwoSidedIdeal.Instances
Try this:
  [apply] import TwoSidedIdeal.Kernel
Try this:
  [apply] import TwoSidedIdeal.Lattice
Try this:
  [apply] import TwoSidedIdeal.Operations
Try this:
  [apply] import UniqueFactorizationDomain.Basic
Try this:
  [apply] import UniqueFactorizationDomain.ClassGroup
Try this:
  [apply] import UniqueFactorizationDomain.Defs
Try this:
  [apply] import UniqueFactorizationDomain.FactorSet
Try this:
  [apply] import UniqueFactorizationDomain.Finite
Try this:
  [apply] import UniqueFactorizationDomain.Finsupp
Try this:
  [apply] import UniqueFactorizationDomain.GCDMonoid
Try this:
  [apply] import UniqueFactorizationDomain.Ideal
Try this:
  [apply] import UniqueFactorizationDomain.Kaplansky
Try this:
  [apply] import UniqueFactorizationDomain.Localization
Try this:
  [apply] import UniqueFactorizationDomain.Moebius
Try this:
  [apply] import UniqueFactorizationDomain.Multiplicative
Try this:
  [apply] import UniqueFactorizationDomain.Multiplicity
Try this:
  [apply] import UniqueFactorizationDomain.Nat
Try this:
  [apply] import UniqueFactorizationDomain.NormalizedFactors
Try this:
  [apply] import Unramified.Basic
Try this:
  [apply] import Unramified.Dedekind
Try this:
  [apply] import Unramified.Field
Try this:
  [apply] import Unramified.Finite
Try this:
  [apply] import Unramified.LocalRing
Try this:
  [apply] import Unramified.LocalStructure
Try this:
  [apply] import Unramified.Locus
Try this:
  [apply] import Unramified.Pi
Try this:
  [apply] import Valuation.AlgebraInstances
Try this:
  [apply] import Valuation.Archimedean
Try this:
  [apply] import Valuation.Basic
Try this:
  [apply] import Valuation.Discrete.Basic
Try this:
  [apply] import WittVector.IsPoly
Try this:
  [apply] import Valuation.Discrete.RankOne
Try this:
  [apply] import Valuation.DiscreteValuativeRel
Try this:
  [apply] import Valuation.ExtendToLocalization
Try this:
  [apply] import Valuation.Extension
Try this:
  [apply] import Valuation.FiniteField
Try this:
  [apply] import Valuation.Integers
Try this:
  [apply] import Valuation.Integral
Try this:
  [apply] import Valuation.IsTrivialOn
Try this:
  [apply] import Valuation.LocalSubring
Try this:
  [apply] import Valuation.Minpoly
Try this:
  [apply] import Valuation.PrimeMultiplicity
Try this:
  [apply] import Valuation.Quotient
Try this:
  [apply] import Valuation.RamificationGroup
Try this:
  [apply] import Valuation.RankOne
Try this:
  [apply] import Valuation.ValuationRing
Try this:
  [apply] import Valuation.ValuationSubring
Try this:
  [apply] import Valuation.ValuativeRel.Basic
Try this:
  [apply] import Valuation.ValuativeRel.Trivial
Try this:
  [apply] import WittVector.Basic
Try this:
  [apply] import WittVector.Compare
Try this:
  [apply] import WittVector.Complete
Try this:
  [apply] import WittVector.Defs
Try this:
  [apply] import WittVector.DiscreteValuationRing
Try this:
  [apply] import WittVector.Domain
Try this:
  [apply] import WittVector.Frobenius
Try this:
  [apply] import WittVector.FrobeniusFractionField
Try this:
  [apply] import WittVector.Identities
Try this:
  [apply] import WittVector.InitTail
Try this:
  [apply] import Ring
Try this:
  [apply] import WittVector.Isocrystal
Try this:
  [apply] import WittVector.MulCoeff
Try this:
  [apply] import WittVector.MulP
Try this:
  [apply] import WittVector.StructurePolynomial
Try this:
  [apply] import WittVector.Teichmuller
Try this:
  [apply] import WittVector.TeichmullerSeries
Try this:
  [apply] import WittVector.Truncated
Try this:
  [apply] import WittVector.Verschiebung
Try this:
  [apply] import WittVector.WittPolynomial
Try this:
  [apply] import ZMod
Try this:
  [apply] import ZMod.Torsion
Try this:
  [apply] import ZMod.UnitsCyclic
Try this:
  [apply] import ZariskisMainTheorem
Try this:
  [apply] import NoncommRing
Try this:
  [apply] import Ring.RingNF
Try this:
  [apply] import Ring.Basic
Try this:
  [apply] import Ring.Common
Try this:
  [apply] import Ring.Compare
Try this:
  [apply] import Ring.NamePolyVars
Try this:
  [apply] import Ring.NamePowerVars
Try this:
  [apply] import Ring.PNat
Try this:
  [apply] import Algebra.Ring.Ideal
Try this:
  [apply] import Algebra.InfiniteSum.Ring
Try this:
  [apply] import Algebra.Ring.Basic
Try this:
  [apply] import Algebra.Ring.Compact
Try this:
  [apply] import Algebra.UniformRing
Try this:
  [apply] import Algebra.Ring.Real
Try this:
  [apply] import Category.TopCommRingCat