mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits
PresheafOfModules.colimitPresheafOfModules_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {J : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J (PresheafOfModules R))
  [inst_2 :
    ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
      CategoryTheory.Limits.PreservesColimit (F.comp (PresheafOfModules.evaluation R Y))
        (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))]
  [inst_3 : ∀ (X : Cᵒᵖ), CategoryTheory.Limits.HasColimit (F.comp (PresheafOfModules.evaluation R X))] (X : Cᵒᵖ),
  (PresheafOfModules.colimitPresheafOfModules F).obj X =
    CategoryTheory.Limits.colimit (F.comp (PresheafOfModules.evaluation R X))
-- Std.Time.DateTime.Timestamp
Std.Time.Timestamp.instHAddOffset_1 : HAdd Std.Time.Timestamp Std.Time.Week.Offset Std.Time.Timestamp
-- Mathlib.NumberTheory.PythagoreanTriples
Int.sq_ne_two_mod_four : ∀ (z : ℤ), z * z % 4 ≠ 2
-- Lean.Elab.Command.Scope
/-- Globally unique internal identifiers for the `varDecls`.
There is one identifier per variable introduced by the binders
(recall that a binder such as `(a b c : Ty)` can produce more than one variable),
and each identifier is the user-provided variable name with a macro scope.
This is used by `TermElabM` in `Lean.Elab.Term.Context` to help with processing macros
that capture these variables.
 -/
Lean.Elab.Command.Scope.varUIds : Lean.Elab.Command.Scope → Array Lean.Name
-- Init.Data.List.Lemmas
List.head_singleton : ∀ {α : Type u_1} {a : α}, [a].head ⋯ = a
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get!_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] [inst : BEq α]
  [Std.LawfulBEqOrd α] [inst_2 : Std.LawfulEqOrd α] (h : t.WF) {l : List ((a : α) × β a)} {k : α}
  [inst_3 : Inhabited (β k)], (List.map Sigma.fst l).contains k = false → (↑(t.insertMany l ⋯)).get! k = t.get! k
-- Mathlib.Analysis.Convex.StdSimplex
stdSimplex.ext : ∀ {S : Type u_1} [inst : Semiring S] [inst_1 : PartialOrder S] {X : Type u_2} [inst_2 : Fintype X]
  {s t : ↑(stdSimplex S X)}, ⇑s = ⇑t → s = t
-- Mathlib.CategoryTheory.Limits.Chosen.End
/-- Given `F : Jᵒᵖ ⥤ J ⥤ C`, this is the projection `chosenEnd F ⟶ (F.obj (op j)).obj j`
for any `j : J`.  -/
CategoryTheory.Limits.chosenEnd.π : {J : Type u_3} →
  {C : Type u_4} →
    [inst : CategoryTheory.Category.{v_3, u_4} C] →
      [inst_1 : CategoryTheory.Category.{v_4, u_3} J] →
        (F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)) →
          [inst_2 : CategoryTheory.Limits.ChosenEndsOfShape J C] →
            (j : J) → CategoryTheory.Limits.chosenEnd F ⟶ (F.obj (Opposite.op j)).obj j
-- Mathlib.Data.Finset.Sum
Finset.disjSum_ssubset_disjSum_of_subset_of_ssubset : ∀ {α : Type u_1} {β : Type u_2} {s₁ s₂ : Finset α} {t₁ t₂ : Finset β}, s₁ ⊆ s₂ → t₁ ⊂ t₂ → s₁.disjSum t₁ ⊂ s₂.disjSum t₂
-- Mathlib.Algebra.Group.Subsemigroup.Operations
MulHom.coe_srangeRestrict : ∀ {M : Type u_1} [inst : Mul M] {N : Type u_5} [inst_1 : Mul N] (f : M →ₙ* N) (x : M), ↑(f.srangeRestrict x) = f x
-- Mathlib.CategoryTheory.ObjectProperty.Small
CategoryTheory.ObjectProperty.map.eq_1 : ∀ {C : Type u} {D : Type u'} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Category.{v', u'} D]
  (P : CategoryTheory.ObjectProperty C) (F : CategoryTheory.Functor C D) (Y : D),
  P.map F Y = ∃ X, P X ∧ Nonempty (F.obj X ≅ Y)
-- Mathlib.Data.Part
Part.instDiv.eq_1 : ∀ {α : Type u_1} [inst : Div α], Part.instDiv = { div := fun a b => (fun x1 x2 => x1 / x2) <$> a <*> b }
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
CategoryTheory.Abelian.extFunctor_map_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] (n : ℕ) {X₁ X₂ : Cᵒᵖ} (f : X₁ ⟶ X₂) (Y : C),
  ((CategoryTheory.Abelian.extFunctor n).map f).app Y =
    AddCommGrpCat.ofHom (AddMonoidHom.mk' (fun α => (CategoryTheory.Abelian.Ext.mk₀ f.unop).comp α ⋯) ⋯)
-- Mathlib.Order.Max
Subsingleton.isBot : ∀ {α : Type u_1} [inst : Preorder α] [Subsingleton α] (a : α), IsBot a
-- Mathlib.Algebra.Module.LocalizedModule.Submodule
Submodule.localized'_iSup : ∀ {R : Type u_1} (S : Type u_2) {M : Type u_3} {N : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Algebra R S] [inst_7 : Module S N] [inst_8 : IsScalarTower R S N] (p : Submonoid R)
  [inst_9 : IsLocalization p S] (f : M →ₗ[R] N) [inst_10 : IsLocalizedModule p f] {ι : Type u_5}
  (g : ι → Submodule R M), Submodule.localized' S p f (⨆ i, g i) = ⨆ i, Submodule.localized' S p f (g i)
-- Mathlib.AlgebraicGeometry.Cover.Sigma
AlgebraicGeometry.Scheme.Cover.toSigma_h₀ : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {S : AlgebraicGeometry.Scheme}
  [inst : AlgebraicGeometry.IsZariskiLocalAtSource P] [inst_1 : UnivLE.{v, u}]
  (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) S) (i : 𝒰.I₀),
  𝒰.toSigma.h₀ i = CategoryTheory.Limits.Sigma.ι 𝒰.X i
-- Mathlib.Algebra.Module.LinearMap.FiniteRange
LinearMap.IsRightQuasiInverse.eq_1 : ∀ {K : Type u_1} {V₂ : Type u_4} {V₃ : Type u_6} [inst : CommRing K] [inst_1 : AddCommGroup V₂] [inst_2 : Module K V₂]
  [inst_3 : AddCommGroup V₃] [inst_4 : Module K V₃] (u : V₃ →ₗ[K] V₂) (v : V₂ →ₗ[K] V₃),
  u.IsRightQuasiInverse v = (v ∘ₗ u ≈ LinearMap.id)
-- Mathlib.Data.List.DropRight
List.rdropWhile_eq_self_iff : ∀ {α : Type u_1} {p : α → Bool} {l : List α}, List.rdropWhile p l = l ↔ ∀ (hl : l ≠ []), ¬p (l.getLast hl) = true
-- Lean.LoadDynlib
/-- Dynamically loads a shared library.

The path may also be used perform a system-dependent search for library.
To avoid this, use an absolute path (e.g., from `IO.FS.realPath`).
 -/
Lean.Dynlib.load : System.FilePath → IO Lean.Dynlib
-- Mathlib.Tactic.RSuffices
/-- The `rsuffices` tactic is an alternative version of `suffices`, that allows the usage
of any syntax that would be valid in an `obtain` block. This tactic just calls `obtain`
on the expression, and then `rotate_left`.
 -/
Mathlib.Tactic.rsuffices : Lean.ParserDescr
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.min?_eq_none_iff : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp], t.min? = none ↔ t = ∅
-- Mathlib.AlgebraicGeometry.Morphisms.Integral
AlgebraicGeometry.IsIntegralHom.toIsAffineHom : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [self : AlgebraicGeometry.IsIntegralHom f],
  AlgebraicGeometry.IsAffineHom f
-- Init.Data.SInt.Lemmas
UInt8.toInt8_ofBitVec : ∀ (b : BitVec 8), { toBitVec := b }.toInt8 = Int8.ofBitVec b
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
/-- Given a multilinear map in `n` variables, if one restricts it to `k` variables putting `z` on
the other coordinates, then the resulting restricted function satisfies an inequality
`‖f.restr v‖ ≤ C * ‖z‖^(n-k) * Π ‖v i‖` if the original function satisfies `‖f v‖ ≤ C * Π ‖v i‖`.  -/
MultilinearMap.restr_norm_le : ∀ {𝕜 : Type u} {G : Type wG} {G' : Type wG'} [inst : NontriviallyNormedField 𝕜] [inst_1 : SeminormedAddCommGroup G]
  [inst_2 : NormedSpace 𝕜 G] [inst_3 : SeminormedAddCommGroup G'] [inst_4 : NormedSpace 𝕜 G'] {k n : ℕ}
  (f : MultilinearMap 𝕜 (fun x => G) G') (s : Finset (Fin n)) (hk : s.card = k) (z : G) {C : ℝ},
  (∀ (m : Fin n → G), ‖f m‖ ≤ C * ∏ i, ‖m i‖) → ∀ (v : Fin k → G), ‖(f.restr s hk z) v‖ ≤ C * ‖z‖ ^ (n - k) * ∏ i, ‖v i‖
-- Mathlib.Algebra.Module.Equiv.Basic
LinearEquiv.arrowCongr_symm_apply : ∀ {R₁ : Type u_9} {R₂ : Type u_10} {R₁' : Type u_12} {R₂' : Type u_13} {M₁ : Type u_17} {M₂ : Type u_18}
  {M₁' : Type u_20} {M₂' : Type u_21} [inst : Semiring R₁] [inst_1 : Semiring R₂] [inst_2 : CommSemiring R₁']
  [inst_3 : CommSemiring R₂'] [inst_4 : AddCommMonoid M₁] [inst_5 : AddCommMonoid M₂] [inst_6 : AddCommMonoid M₁']
  [inst_7 : AddCommMonoid M₂'] [inst_8 : Module R₁ M₁] [inst_9 : Module R₂ M₂] [inst_10 : Module R₁' M₁']
  [inst_11 : Module R₂' M₂'] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {σ₁'₂' : R₁' →+* R₂'} {σ₂'₁' : R₂' →+* R₁'}
  {σ₁₁' : R₁ →+* R₁'} {σ₂₂' : R₂ →+* R₂'} {σ₂₁' : R₂ →+* R₁'} {σ₁₂' : R₁ →+* R₂'} [inst_12 : RingHomInvPair σ₁₂ σ₂₁]
  [inst_13 : RingHomInvPair σ₂₁ σ₁₂] [inst_14 : RingHomInvPair σ₁'₂' σ₂'₁'] [inst_15 : RingHomInvPair σ₂'₁' σ₁'₂']
  [inst_16 : RingHomCompTriple σ₁₁' σ₁'₂' σ₁₂'] [inst_17 : RingHomCompTriple σ₂₁ σ₁₂' σ₂₂']
  [inst_18 : RingHomCompTriple σ₂₂' σ₂'₁' σ₂₁'] [inst_19 : RingHomCompTriple σ₁₂ σ₂₁' σ₁₁'] (e₁ : M₁ ≃ₛₗ[σ₁₂] M₂)
  (e₂ : M₁' ≃ₛₗ[σ₁'₂'] M₂') (f : M₂ →ₛₗ[σ₂₂'] M₂') (x : M₁), ((e₁.arrowCongr e₂).symm f) x = e₂.symm (f (e₁ x))
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
mdifferentiableWithinAt_id : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {s : Set M} {x : M}, MDiffAt[s] id x
-- Mathlib.Analysis.Convolution
/-- The definition of convolution where the bilinear operator is scalar multiplication.
Note: it often helps the elaborator to give the type of the convolution explicitly.  -/
MeasureTheory.convolution_lsmul : ∀ {𝕜 : Type u𝕜} {G : Type uG} {F : Type uF} [inst : NormedAddCommGroup F] {x : G} [inst_1 : NontriviallyNormedField 𝕜]
  [inst_2 : NormedSpace 𝕜 F] [inst_3 : MeasurableSpace G] {μ : MeasureTheory.Measure G} [inst_4 : NormedSpace ℝ F]
  [inst_5 : Sub G] {f : G → 𝕜} {g : G → F},
  MeasureTheory.convolution f g (ContinuousLinearMap.lsmul 𝕜 𝕜) μ x = ∫ (t : G), f t • g (x - t) ∂μ
-- Mathlib.RingTheory.TensorProduct.Finite
_private.Mathlib.RingTheory.TensorProduct.Finite.0.RingHom.Finite.tensorProductMap_id : ∀ {R : Type u_1} {S : Type u_2} {S' : Type u_3} {T : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : CommRing T] [inst_3 : CommRing S'] [inst_4 : Algebra R S] [inst_5 : Algebra R T] [inst_6 : Algebra R S']
  {f : S →ₐ[R] S'}, f.Finite → (Algebra.TensorProduct.map f (AlgHom.id R T)).Finite
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.Splits.natDegree_eq_card_roots : ∀ {R : Type u_1} [inst : CommRing R] {f : Polynomial R} [inst_1 : IsDomain R], f.Splits → f.natDegree = f.roots.card
-- Mathlib.Data.Matrix.Basic
/-- The `RingHom` between spaces of square matrices induced by a `RingHom` between their
coefficients. This is `Matrix.map` as a `RingHom`.  -/
RingHom.mapMatrix : {m : Type u_2} →
  {α : Type u_11} →
    {β : Type u_12} →
      [inst : Fintype m] →
        [inst_1 : DecidableEq m] →
          [inst_2 : NonAssocSemiring α] → [inst_3 : NonAssocSemiring β] → (α →+* β) → Matrix m m α →+* Matrix m m β
-- Mathlib.Algebra.Group.Subgroup.Finite
/-- Product of a multiset of elements in a subgroup of a `CommGroup` is in the subgroup.  -/
Subgroup.multiset_prod_mem : ∀ {G : Type u_3} [inst : CommGroup G] (K : Subgroup G) (g : Multiset G), (∀ a ∈ g, a ∈ K) → g.prod ∈ K
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRoot.coe_liftHom : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
  (h : IsAdjoinRoot S f) {T : Type u_1} [inst_3 : CommRing T] {x : T} [inst_4 : Algebra R T]
  (hx' : (Polynomial.aeval x) f = 0), ↑(h.liftHom x hx') = h.lift (algebraMap R T) x hx'
-- Mathlib.Order.RelClasses
/-- Set notation form of `eq_or_lt_of_le` -/
eq_or_ssubset_of_subset : ∀ {α : Type u_2} [UsesSetNotationForOrder α] [inst : PartialOrder α] {a b : α}, a ⊆ b → a = b ∨ a ⊂ b
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
/-- This lemma says that `fun x => a ^ x` is strictly differentiable for `a < 0`. Note that these
values of `a` are outside of the "official" domain of `a ^ x`, and we may redefine `a ^ x`
for negative `a` if some other definition will be more convenient.  -/
Real.hasStrictDerivAt_const_rpow_of_neg : ∀ {a x : ℝ},
  a < 0 →
    HasStrictDerivAt (fun x => a ^ x)
      (a ^ x * Real.log a - Real.exp (Real.log a * x) * Real.sin (x * Real.pi) * Real.pi) x
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.BinaryFan.braiding_hom_snd_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {s : CategoryTheory.Limits.BinaryFan X Y}
  (P : CategoryTheory.Limits.IsLimit s) {t : CategoryTheory.Limits.BinaryFan Y X} (Q : CategoryTheory.Limits.IsLimit t)
  {Z : C} (h : (CategoryTheory.Limits.pair Y X).obj { as := CategoryTheory.Limits.WalkingPair.right } ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryFan.braiding P Q).hom
      (CategoryTheory.CategoryStruct.comp t.snd h) =
    CategoryTheory.CategoryStruct.comp s.fst h
-- Mathlib.RingTheory.LocalRing.Module
IsLocalRing.subsingleton_tensorProduct : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : IsLocalRing R] [Module.Finite R M],
  Subsingleton (TensorProduct R (IsLocalRing.ResidueField R) M) ↔ Subsingleton M
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.cyclesMap_id_comp : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A B C : Rep.{u, u, u} k G} (φ : A ⟶ B) (ψ : B ⟶ C) (n : ℕ),
  groupHomology.cyclesMap (MonoidHom.id G) (CategoryTheory.CategoryStruct.comp φ ψ) n =
    CategoryTheory.CategoryStruct.comp (groupHomology.cyclesMap (MonoidHom.id G) φ n)
      (groupHomology.cyclesMap (MonoidHom.id G) ψ n)
-- Lean.Meta.Sym.Pattern
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.mkCheckTypeMask.go : Lean.Expr → ℕ → Bool → Array Bool → Array Bool
-- Lean.Elab.DocString
Lean.Doc.WithSyntax.mk : {α : Type u} → α → Lean.Syntax → Lean.Doc.WithSyntax α
-- Mathlib.Topology.Category.Profinite.Extend
/-- If `c` is a limit cone, `G.mapCocone c.op` is a colimit cone and the projection maps in `c`
are epimorphic, then `cocone G c.pt` is a colimit cone.
 -/
Profinite.Extend.isColimitCocone : {I : Type u} →
  [inst : CategoryTheory.SmallCategory I] →
    [CategoryTheory.IsCofiltered I] →
      {F : CategoryTheory.Functor I FintypeCat} →
        (c : CategoryTheory.Limits.Cone (F.comp FintypeCat.toProfinite)) →
          {C : Type u_1} →
            [inst_2 : CategoryTheory.Category.{v_1, u_1} C] →
              (G : CategoryTheory.Functor Profiniteᵒᵖ C) →
                CategoryTheory.Limits.IsLimit c →
                  [∀ (i : I), CategoryTheory.Epi (c.π.app i)] →
                    CategoryTheory.Limits.IsColimit (G.mapCocone c.op) →
                      CategoryTheory.Limits.IsColimit (Profinite.Extend.cocone G c.pt)
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.ofVal_bijective : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] [inst_1 : Ring R] (v : Valuation R Γ₀),
  Function.Bijective WithVal.ofVal
-- Lean.Declaration
Lean.ConstantInfo.defnInfo.inj : ∀ {val val_1 : Lean.DefinitionVal}, Lean.ConstantInfo.defnInfo val = Lean.ConstantInfo.defnInfo val_1 → val = val_1
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
_private.Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point.0.WeierstrassCurve.Projective.nonsingular_add_of_Z_ne_zero : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} [inst_1 : DecidableEq F] {P Q : Fin 3 → F},
  W.Nonsingular P →
    W.Nonsingular Q →
      P 2 ≠ 0 →
        Q 2 ≠ 0 →
          ¬(P 0 * Q 2 = Q 0 * P 2 ∧ P 1 * Q 2 = W.negY Q * P 2) →
            W.Nonsingular
              ![W.toAffine.addX (P 0 / P 2) (Q 0 / Q 2)
                  (W.toAffine.slope (P 0 / P 2) (Q 0 / Q 2) (P 1 / P 2) (Q 1 / Q 2)),
                W.toAffine.addY (P 0 / P 2) (Q 0 / Q 2) (P 1 / P 2)
                  (W.toAffine.slope (P 0 / P 2) (Q 0 / Q 2) (P 1 / P 2) (Q 1 / Q 2)),
                1]
-- Mathlib.RingTheory.SimpleModule.Basic
LinearMap.instIsSimpleModuleEndOfNontrivial : ∀ {M : Type u_4} [inst : AddCommGroup M] (R : Type u_6) [inst_1 : DivisionRing R] [inst_2 : Module R M] [Nontrivial M],
  IsSimpleModule (Module.End R M) M
-- Mathlib.Algebra.Category.MonCat.Colimits
MonCat.Colimits.Relation.below.mul_1 : ∀ {J : Type v} [inst : CategoryTheory.Category.{u, v} J] {F : CategoryTheory.Functor J MonCat}
  {motive : (a a_1 : MonCat.Colimits.Prequotient F) → MonCat.Colimits.Relation F a a_1 → Prop}
  (x x' y : MonCat.Colimits.Prequotient F) (x_1 : MonCat.Colimits.Relation F x x'),
  MonCat.Colimits.Relation.below x_1 → motive x x' x_1 → MonCat.Colimits.Relation.below ⋯
-- Lean.Environment
_private.Lean.Environment.0.Lean.ImportState.mk.sizeOf_spec : ∀ (moduleNameMap : Std.HashMap Lean.Name Lean.ImportedModule✝) (moduleNames : Array Lean.Name),
  sizeOf { moduleNameMap := moduleNameMap, moduleNames := moduleNames } = 1 + sizeOf moduleNameMap + sizeOf moduleNames
-- Lean.Meta.Match.Basic
Lean.Meta.Match.Pattern.as.injEq : ∀ (varId : Lean.FVarId) (p : Lean.Meta.Match.Pattern) (hId varId_1 : Lean.FVarId) (p_1 : Lean.Meta.Match.Pattern)
  (hId_1 : Lean.FVarId),
  (Lean.Meta.Match.Pattern.as varId p hId = Lean.Meta.Match.Pattern.as varId_1 p_1 hId_1) =
    (varId = varId_1 ∧ p = p_1 ∧ hId = hId_1)
-- Mathlib.CategoryTheory.Bicategory.SingleObj
CategoryTheory.MonoidalSingleObj.endMonoidalStarFunctorEquivalence_counitIso : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C],
  (CategoryTheory.MonoidalSingleObj.endMonoidalStarFunctorEquivalence C).counitIso =
    CategoryTheory.Iso.refl
      ({ obj := fun X => X, map := fun {X Y} f => f, map_id := ⋯, map_comp := ⋯ }.comp
        (CategoryTheory.MonoidalSingleObj.endMonoidalStarFunctor C))
-- Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
SimplexCategory.σ_σ₀Iter' : ∀ (i : ℕ) {n m : ℕ} (j : Fin (m + 1)) (j' : Fin (n + 1)) (hi : autoParam (n + i = m) SimplexCategory.σ_σ₀Iter'._auto_1),
  autoParam (↑j = ↑j' + i) SimplexCategory.σ_σ₀Iter'._auto_3 →
    CategoryTheory.CategoryStruct.comp (SimplexCategory.σ j) (SimplexCategory.σ₀Iter i hi) =
      CategoryTheory.CategoryStruct.comp (SimplexCategory.σ₀Iter i ⋯) (SimplexCategory.σ j')
-- Mathlib.NumberTheory.Padics.RingHoms
PadicInt.nthHomSeq.eq_1 : ∀ {R : Type u_1} [inst : NonAssocSemiring R] {p : ℕ} {f : (k : ℕ) → R →+* ZMod (p ^ k)} [hp_prime : Fact (Nat.Prime p)]
  (f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1) (r : R),
  PadicInt.nthHomSeq f_compat r = ⟨fun n => ↑(PadicInt.nthHom f r n), ⋯⟩
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
AntitoneOn.const_add : ∀ {α : Type u_1} {β : Type u_2} [inst : Add α] [inst_1 : Preorder α] [inst_2 : Preorder β] {f : β → α} {s : Set β}
  [AddLeftMono α], AntitoneOn f s → ∀ (a : α), AntitoneOn (fun x => a + f x) s
-- Mathlib.CategoryTheory.Functor.EpiMono
CategoryTheory.Adjunction.strongMono_map_of_isEquivalence : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} {A B : C} [F.IsEquivalence]
  (f : B ⟶ A) [_h : CategoryTheory.StrongMono f], CategoryTheory.StrongMono (F.map f)
-- Init.Data.BitVec.Lemmas
BitVec.add_comm : ∀ {n : ℕ} (x y : BitVec n), x + y = y + x
-- Mathlib.Order.Interval.Set.Pi
Set.image_mulSingle_Ico_left : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : DecidableEq ι] [inst_1 : (i : ι) → PartialOrder (α i)]
  [inst_2 : (i : ι) → One (α i)] (i : ι) (a : α i), Pi.mulSingle i '' Set.Ico a 1 = Set.Ico (Pi.mulSingle i a) 1
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
RootPairing.GeckConstruction.u.congr_simp : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} {b : P.Base}
  {inst_5 : DecidableEq ι} [inst_6 : DecidableEq ι] (i i_1 : ↥b.support),
  i = i_1 →
    ∀ (a a_1 : ↥b.support ⊕ ι), a = a_1 → RootPairing.GeckConstruction.u i a = RootPairing.GeckConstruction.u i_1 a_1
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.isCentralScalar : ∀ {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [inst : SMul R α] [inst_1 : SMul Rᵐᵒᵖ α]
  [IsCentralScalar R α], IsCentralScalar R (Matrix m n α)
-- Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
AlgebraicGeometry.Scheme.AffineZariskiSite.PreservesLocalization.isOpenImmersion : ∀ {X : AlgebraicGeometry.Scheme} (F : CategoryTheory.Functor X.AffineZariskiSiteᵒᵖ CommRingCat)
  (α : (AlgebraicGeometry.Scheme.AffineZariskiSite.toOpensFunctor X).op.comp X.presheaf ⟶ F),
  CategoryTheory.NatTrans.Coequifibered α →
    ∀ ⦃U V : X.AffineZariskiSite⦄ (f : U ⟶ V),
      AlgebraicGeometry.IsOpenImmersion ((F.rightOp.comp AlgebraicGeometry.Scheme.Spec).map f)
-- Mathlib.Analysis.CStarAlgebra.Multiplier
DoubleCentralizer.add_toProd : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : NormedSpace 𝕜 A] [inst_3 : SMulCommClass 𝕜 A A] [inst_4 : IsScalarTower 𝕜 A A]
  (a b : DoubleCentralizer 𝕜 A), (a + b).toProd = a.toProd + b.toProd
-- Std.Time.Duration
Std.Time.instToStringDuration.leftPad : ℕ → String → String
-- Mathlib.Data.Multiset.Powerset
/-- `powersetCard n s` is the multiset of all submultisets of `s` of length `n`.  -/
Multiset.powersetCard : {α : Type u_1} → ℕ → Multiset α → Multiset (Multiset α)
-- Mathlib.Order.Interval.Set.Pi
Set.image_update_Ico_right : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : DecidableEq ι] [inst_1 : (i : ι) → PartialOrder (α i)] (f : (i : ι) → α i)
  (i : ι) (b : α i), Function.update f i '' Set.Ico (f i) b = Set.Ico f (Function.update f i b)
-- Mathlib.Data.PNat.Find
PNat.lt_find_iff : ∀ {p : ℕ+ → Prop} [inst : DecidablePred p] (h : ∃ n, p n) (n : ℕ+), n < PNat.find h ↔ ∀ m ≤ n, ¬p m
-- Mathlib.Algebra.Group.Invertible.Basic
nonempty_invertible_iff_isUnit : ∀ {α : Type u} [inst : Monoid α] (a : α), Nonempty (Invertible a) ↔ IsUnit a
-- Mathlib.LinearAlgebra.FreeModule.PID
/-- If `S` a finite-dimensional ring extension of a PID `R` which is free as an `R`-module,
then any nonzero `S`-ideal `I` is free as an `R`-submodule of `S`, and we can
find a basis for `S` and `I` such that the inclusion map is a square diagonal
matrix.

See `Ideal.exists_smith_normal_form` for a version of this theorem that doesn't
need to map `I` into a submodule of `R`.

This is a strengthening of `Submodule.basisOfPid`.
 -/
Ideal.smithNormalForm : {ι : Type u_1} →
  {R : Type u_2} →
    [inst : CommRing R] →
      [IsDomain R] →
        [IsPrincipalIdealRing R] →
          {S : Type u_4} →
            [inst_3 : CommRing S] →
              [IsDomain S] →
                [inst_5 : Algebra R S] →
                  [inst_6 : Fintype ι] →
                    Module.Basis ι R S →
                      (I : Ideal S) →
                        I ≠ ⊥ → Module.Basis.SmithNormalForm (Submodule.restrictScalars R I) ι (Fintype.card ι)
-- Mathlib.Algebra.GroupWithZero.Units.Fintype
UnitsInt.fintype : Fintype ℤˣ
-- Mathlib.NumberTheory.Cyclotomic.Basic
IsSepClosedOfCharZero.isCyclotomicExtension : ∀ (K : Type w) [inst : Field K] [IsSepClosed K] [CharZero K] (S : Set ℕ), IsCyclotomicExtension S K K
-- Mathlib.Data.Nat.Choose.Multinomial
/-- The **multinomial theorem**.  -/
Finset.sum_pow_of_commute : ∀ {α : Type u_1} {R : Type u_2} [inst : DecidableEq α] [inst_1 : Semiring R] (x : α → R) (s : Finset α)
  (hc : (↑s).Pairwise (Function.onFun Commute x)) (n : ℕ),
  s.sum x ^ n = ∑ k, ↑(↑↑k).countPerms * (Multiset.map x ↑↑k).noncommProd ⋯
-- Aesop.Frontend.Tactic
Aesop.Frontend.Parser.«tactic_clause(Config:=_)» : Lean.ParserDescr