mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Category.ModuleCat.Topology.Homology
TopModuleCat.instMonoKerι : ∀ {R : Type u} [inst : Ring R] [inst_1 : TopologicalSpace R] {M N : TopModuleCat R} (φ : M ⟶ N),
  CategoryTheory.Mono (TopModuleCat.kerι φ)
-- Mathlib.CategoryTheory.Bicategory.InducedBicategory
/-- `InducedBicategory B C`, where `F : B → C`, is a typeclass synonym for `B`. This is given
a bicategory structure where the 1-morphisms `X ⟶ Y` are the 1-morphisms in `C` from `F X` to
`F Y`, and the 2-morphisms `f ⟶ g` are also the 2-morphisms in `C` from `f` to `g`.
 -/
CategoryTheory.Bicategory.InducedBicategory : {B : Type u_1} → (C : Type u_2) → (B → C) → Type u_1
-- Mathlib.ModelTheory.ElementaryMaps
/-- An elementary embedding of first-order structures is an embedding that commutes with the
realizations of formulas.  -/
FirstOrder.«term_↪ₑ[_]_» : Lean.TrailingParserDescr
-- Mathlib.MeasureTheory.Function.UniformIntegrable
MeasureTheory.UniformIntegrable.ae_eq : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup β] {p : ENNReal} {f g : ι → α → β},
  MeasureTheory.UniformIntegrable f p μ → (∀ (n : ι), f n =ᵐ[μ] g n) → MeasureTheory.UniformIntegrable g p μ
-- Mathlib.AlgebraicGeometry.Sites.ConstantSheaf
AlgebraicGeometry.isSheaf_fpqcTopology_continuousMapPresheafAb : ∀ (A : Type v) [inst : TopologicalSpace A] [inst_1 : AddCommGroup A] [inst_2 : IsTopologicalAddGroup A],
  CategoryTheory.Presheaf.IsSheaf AlgebraicGeometry.Scheme.fpqcTopology (AlgebraicGeometry.continuousMapPresheafAb A)
-- Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
/-- Any `K`-algebra module that is 1-dimensional over `K` is simple.  -/
is_simple_module_of_finrank_eq_one : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {A : Type u_1}
  [inst_3 : Semiring A] [inst_4 : Module A V] [inst_5 : SMul K A] [IsScalarTower K A V],
  Module.finrank K V = 1 → IsSimpleOrder (Submodule A V)
-- Mathlib.Algebra.Group.Center
Set.add_mem_addCenter : ∀ {M : Type u_1} [inst : Add M] {z₁ z₂ : M}, z₁ ∈ Set.addCenter M → z₂ ∈ Set.addCenter M → z₁ + z₂ ∈ Set.addCenter M
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getD_eq_fallback_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {a : α}
  {fallback : β a}, m.contains a = false → m.getD a fallback = fallback
-- Mathlib.Analysis.Distribution.TemperedDistribution
TemperedDistribution.smulLeftCLM_sum : ∀ {ι : Type u_1} {E : Type u_3} {F : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : AddCommGroup F] [inst_3 : Module ℂ F] [inst_4 : TopologicalSpace F] [inst_5 : IsTopologicalAddGroup F]
  [inst_6 : ContinuousConstSMul ℂ F] {g : ι → E → ℂ} {s : Finset ι},
  (∀ i ∈ s, Function.HasTemperateGrowth (g i)) →
    (TemperedDistribution.smulLeftCLM F fun x => ∑ i ∈ s, g i x) = ∑ i ∈ s, TemperedDistribution.smulLeftCLM F (g i)
-- Init.Data.String.Lemmas.Pattern.Find.Pred
String.Pos.find?_bool_eq_none_iff_of_splits : ∀ {p : Char → Bool} {s : String} {pos : s.Pos} {t u : String},
  pos.Splits t u → (pos.find? p = none ↔ ∀ c ∈ u.toList, p c = false)
-- Mathlib.LinearAlgebra.Determinant
LinearMap.det_def : ∀ {M : Type u_7} [inst : AddCommGroup M] {A : Type u_8} [inst_1 : CommRing A] [inst_2 : Module A M],
  LinearMap.det = if H : ∃ s, Nonempty (Module.Basis (↥s) A M) then LinearMap.detAux (Trunc.mk ⋯.some) else 1
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Finite
CategoryTheory.Limits.compCreatesFiniteColimits : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {E : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} E] →
            (F : CategoryTheory.Functor C D) →
              (G : CategoryTheory.Functor D E) →
                [CategoryTheory.Limits.CreatesFiniteColimits F] →
                  [CategoryTheory.Limits.CreatesFiniteColimits G] →
                    CategoryTheory.Limits.CreatesFiniteColimits (F.comp G)
-- Mathlib.Probability.Process.Stopping
MeasureTheory.IsStoppingTime.measurableSet_eq_top' : ∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : LinearOrder ι] {f : MeasureTheory.Filtration ι m}
  {τ : Ω → WithTop ι} [inst_1 : TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι],
  MeasureTheory.IsStoppingTime f τ → MeasurableSet {ω | τ ω = ⊤}
-- Lean.Server.References
Lean.Server.TransientWorkerILean.mk : Lean.Lsp.DocumentUri →
  ℕ → Lean.Server.DirectImports → Option Bool → Lean.Lsp.ModuleRefs → Lean.Lsp.Decls → Lean.Server.TransientWorkerILean
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F.rightOp : C ⥤ Dᵒᵖ` creates colimits of shape `Jᵒᵖ`, then `F : Cᵒᵖ ⥤ D` creates limits
of shape `J`.  -/
CategoryTheory.Limits.createsLimitsOfShapeOfRightOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (J : Type w) →
          [inst_2 : CategoryTheory.Category.{w', w} J] →
            (F : CategoryTheory.Functor Cᵒᵖ D) →
              [CategoryTheory.CreatesColimitsOfShape Jᵒᵖ F.rightOp] → CategoryTheory.CreatesLimitsOfShape J F
-- Mathlib.Data.Setoid.Partition.Card
/-- Given a partition of the ambient type, the cardinal of a finite set
is the `finsum` of the cardinalities of its traces on the parts of the partition  -/
Setoid.IsPartition.ncard_eq_finsum : ∀ {α : Type u_1} {P : Set (Set α)},
  Setoid.IsPartition P →
    ∀ (s : Set α), autoParam s.Finite Setoid.IsPartition.ncard_eq_finsum._auto_1 → s.ncard = ∑ᶠ (t : ↑P), (s ∩ ↑t).ncard
-- Mathlib.Order.Basic
Ne.gt_or_lt : ∀ {α : Type u_2} [inst : LinearOrder α] {a b : α}, a ≠ b → b < a ∨ a < b
-- Mathlib.Combinatorics.Matroid.Dual
Matroid.IsBase.ssubset_ground : ∀ {α : Type u_1} {M : Matroid α} {B : Set α} [h : M✶.RankPos], M.IsBase B → B ⊂ M.E
-- Mathlib.CategoryTheory.Monad.Limits
CategoryTheory.Comonad.ForgetCreatesColimits'.liftedCocone_pt : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [inst_1 : CategoryTheory.Category.{v, u} J]
  {T : CategoryTheory.Comonad C} (D : CategoryTheory.Functor J T.Coalgebra)
  (c : CategoryTheory.Limits.Cocone (D.comp T.forget)) (t : CategoryTheory.Limits.IsColimit c),
  (CategoryTheory.Comonad.ForgetCreatesColimits'.liftedCocone D c t).pt =
    CategoryTheory.Comonad.ForgetCreatesColimits'.coconePoint D c t
-- Mathlib.Data.QPF.Multivariate.Constructions.Cofix
MvQPF.liftR_map_last' : ∀ {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] [LawfulMvFunctor F] {α : TypeVec.{u} n} {ι : Type u}
  (R : ι → ι → Prop) (x : F (α ::: ι)) (f : ι → ι),
  (∀ (x : ι), R (f x) x) → MvFunctor.LiftR' (α.RelLast' R) (MvFunctor.map (TypeVec.id ::: f) x) x
-- Mathlib.Topology.Algebra.Ring.Basic
/-- The product topology on the Cartesian product of two topological semirings
makes the product into a topological semiring.  -/
instIsTopologicalSemiringProd : ∀ {R : Type u_1} {S : Type u_2} [inst : TopologicalSpace R] [inst_1 : TopologicalSpace S]
  [inst_2 : NonUnitalNonAssocSemiring R] [inst_3 : NonUnitalNonAssocSemiring S] [IsTopologicalSemiring R]
  [IsTopologicalSemiring S], IsTopologicalSemiring (R × S)
-- Mathlib.GroupTheory.Finiteness
/-- An additive subgroup is finitely generated if
and only if it is finitely generated as an additive submonoid.  -/
AddSubgroup.fg_iff_addSubmonoid_fg : ∀ {G : Type u_3} [inst : AddGroup G] (P : AddSubgroup G), P.FG ↔ P.FG
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getEntryLT?.eq_go : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (x : Option ((a : α) × β a))
  (t : Std.DTreeMap.Internal.Impl α β),
  (Std.DTreeMap.Internal.Impl.getEntryLT? k t).or x = Std.DTreeMap.Internal.Impl.getEntryLT?.go k x t
-- Mathlib.LinearAlgebra.Dual.Defs
Submodule.le_dualCoannihilator_dualAnnihilator : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (U : Submodule R (Module.Dual R M)), U ≤ U.dualCoannihilator.dualAnnihilator
-- Mathlib.NumberTheory.SmoothNumbers
/-- If `m ≠ 0` and the `Finset` of prime factors of `m` is contained in `s`, then `m`
is `s`-factored.  -/
Nat.mem_factoredNumbers_of_primeFactors_subset : ∀ {s : Finset ℕ} {m : ℕ}, m ≠ 0 → m.primeFactors ⊆ s → m ∈ Nat.factoredNumbers s
-- Mathlib.CategoryTheory.Join.Basic
_private.Mathlib.CategoryTheory.Join.Basic.0.CategoryTheory.Join.comp.match_1.eq_1 : ∀ {C : Type u_3} [inst : CategoryTheory.Category.{u_1, u_3} C] {D : Type u_4}
  [inst_1 : CategoryTheory.Category.{u_2, u_4} D]
  (motive : (x x_1 x_2 : CategoryTheory.Join C D) → x.Hom x_1 → x_1.Hom x_2 → Sort u_5) (_x _y _z : C)
  (f : (CategoryTheory.Join.left _x).Hom (CategoryTheory.Join.left _y))
  (g : (CategoryTheory.Join.left _y).Hom (CategoryTheory.Join.left _z))
  (h_1 :
    (_x _y _z : C) →
      (f : (CategoryTheory.Join.left _x).Hom (CategoryTheory.Join.left _y)) →
        (g : (CategoryTheory.Join.left _y).Hom (CategoryTheory.Join.left _z)) →
          motive (CategoryTheory.Join.left _x) (CategoryTheory.Join.left _y) (CategoryTheory.Join.left _z) f g)
  (h_2 :
    (_x _y : C) →
      (_z : D) →
        (x : (CategoryTheory.Join.left _x).Hom (CategoryTheory.Join.left _y)) →
          (x_1 : (CategoryTheory.Join.left _y).Hom (CategoryTheory.Join.right _z)) →
            motive (CategoryTheory.Join.left _x) (CategoryTheory.Join.left _y) (CategoryTheory.Join.right _z) x x_1)
  (h_3 :
    (_x : C) →
      (_y _z : D) →
        (x : (CategoryTheory.Join.left _x).Hom (CategoryTheory.Join.right _y)) →
          (x_1 : (CategoryTheory.Join.right _y).Hom (CategoryTheory.Join.right _z)) →
            motive (CategoryTheory.Join.left _x) (CategoryTheory.Join.right _y) (CategoryTheory.Join.right _z) x x_1)
  (h_4 :
    (_x _y _z : D) →
      (f : (CategoryTheory.Join.right _x).Hom (CategoryTheory.Join.right _y)) →
        (g : (CategoryTheory.Join.right _y).Hom (CategoryTheory.Join.right _z)) →
          motive (CategoryTheory.Join.right _x) (CategoryTheory.Join.right _y) (CategoryTheory.Join.right _z) f g),
  (match CategoryTheory.Join.left _x, CategoryTheory.Join.left _y, CategoryTheory.Join.left _z, f, g with
    | CategoryTheory.Join.left _x, CategoryTheory.Join.left _y, CategoryTheory.Join.left _z, f, g => h_1 _x _y _z f g
    | CategoryTheory.Join.left _x, CategoryTheory.Join.left _y, CategoryTheory.Join.right _z, x, x_1 =>
      h_2 _x _y _z x x_1
    | CategoryTheory.Join.left _x, CategoryTheory.Join.right _y, CategoryTheory.Join.right _z, x, x_1 =>
      h_3 _x _y _z x x_1
    | CategoryTheory.Join.right _x, CategoryTheory.Join.right _y, CategoryTheory.Join.right _z, f, g =>
      h_4 _x _y _z f g) =
    h_1 _x _y _z f g
-- Batteries.Recycling.RBTree.Basic
RBTree.RBNode.WF.below : {α : Type u_1} →
  {cmp : α → α → Ordering} →
    {motive : (a : RBTree.RBNode α) → RBTree.RBNode.WF cmp a → Prop} →
      {a : RBTree.RBNode α} → RBTree.RBNode.WF cmp a → Prop
-- Mathlib.NumberTheory.Padics.Complex
/-- `PadicAlgCl p` has characteristic zero.  -/
PadicAlgCl.charZero : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)], CharZero (PadicAlgCl p)
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.seminorm_postcompLM_le : ∀ (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} {F' : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F]
  [inst_5 : NormedSpace 𝕜 F] [inst_6 : SMulCommClass ℝ 𝕜 F] [inst_7 : NormedAddCommGroup F'] [inst_8 : NormedSpace ℝ F']
  [inst_9 : NormedSpace 𝕜 F'] [inst_10 : SMulCommClass ℝ 𝕜 F'] {n : ℕ∞} {K : TopologicalSpace.Compacts E}
  [inst_11 : LinearMap.CompatibleSMul F F' ℝ 𝕜] {i : ℕ} (T : F →L[𝕜] F') (f : ContDiffMapSupportedIn E F n K),
  (ContDiffMapSupportedIn.seminorm 𝕜 E F' n K i) ((ContDiffMapSupportedIn.postcompLM T) f) ≤
    ‖T‖ * (ContDiffMapSupportedIn.seminorm 𝕜 E F n K i) f
-- Mathlib.Topology.LocallyFinsupp
Function.locallyFinsuppWithin.mk : {X : Type u_1} →
  [inst : TopologicalSpace X] →
    {U : Set X} →
      {Y : Type u_2} →
        [inst_1 : Zero Y] →
          (toFun : X → Y) →
            Function.support toFun ⊆ U →
              (∀ z ∈ U, ∃ t ∈ nhds z, (t ∩ Function.support toFun).Finite) → Function.locallyFinsuppWithin U Y
-- Mathlib.LinearAlgebra.Matrix.Module
LinearMap.mapMatrixModule_apply : ∀ (ι : Type u_1) {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Ring R] [inst_1 : Fintype ι]
  [inst_2 : DecidableEq ι] [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : AddCommGroup N]
  [inst_6 : Module R N] (f : M →ₗ[R] N) (a : ι → M) (a_1 : ι),
  (LinearMap.mapMatrixModule ι f) a a_1 = (f.compLeft ι) a a_1
-- Batteries.Lean.EStateM
EStateM.run_seq : ∀ {ε σ α β : Type u_1} (f : EStateM ε σ (α → β)) (x : EStateM ε σ α) (s : σ),
  (f <*> x).run s =
    match f.run s with
    | EStateM.Result.ok g s => EStateM.Result.map g (x.run s)
    | EStateM.Result.error e s => EStateM.Result.error e s
-- Mathlib.Geometry.Manifold.ContMDiff.Basic
contMDiff_zero : ∀ {𝕜 : 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] {E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  {H' : Type u_6} [inst_7 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7}
  [inst_8 : TopologicalSpace M'] [inst_9 : ChartedSpace H M] [inst_10 : ChartedSpace H' M'] {n : WithTop ℕ∞}
  [inst_11 : Zero M'], ContMDiff I I' n 0
-- Mathlib.Algebra.Homology.TotalComplexShift
HomologicalComplex₂.D₁_totalShift₂XIso_hom_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (y : ℤ) [inst_2 : K.HasTotal (ComplexShape.up ℤ)]
  (n₀ n₁ n₀' n₁' : ℤ) (h₀ : n₀ + y = n₀') (h₁ : n₁ + y = n₁') {Z : C} (h : (K.total (ComplexShape.up ℤ)).X n₁' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (((HomologicalComplex₂.shiftFunctor₂ C y).obj K).D₁ (ComplexShape.up ℤ) n₀ n₁)
      (CategoryTheory.CategoryStruct.comp (K.totalShift₂XIso y n₁ n₁' h₁).hom h) =
    CategoryTheory.CategoryStruct.comp
      (y.negOnePow •
        CategoryTheory.CategoryStruct.comp (K.totalShift₂XIso y n₀ n₀' h₀).hom (K.D₁ (ComplexShape.up ℤ) n₀' n₁'))
      h
-- Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone
CategoryTheory.SmallObject.SuccStruct.ofCocone.map_comp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {J : Type u} [inst_1 : LinearOrder J] {j : J}
  {F : CategoryTheory.Functor (↑(Set.Iio j)) C} (c : CategoryTheory.Limits.Cocone F) (i₁ i₂ i₃ : J) (hi : i₁ ≤ i₂)
  (hi' : i₂ ≤ i₃) (hi₃ : i₃ ≤ j),
  CategoryTheory.SmallObject.SuccStruct.ofCocone.map c i₁ i₃ ⋯ hi₃ =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.SuccStruct.ofCocone.map c i₁ i₂ hi ⋯)
      (CategoryTheory.SmallObject.SuccStruct.ofCocone.map c i₂ i₃ hi' hi₃)
-- Mathlib.Combinatorics.Matroid.Rank.Finite
Matroid.isRkFinite_inter_ground_iff : ∀ {α : Type u_1} {M : Matroid α} {X : Set α}, M.IsRkFinite (X ∩ M.E) ↔ M.IsRkFinite X
-- Mathlib.CategoryTheory.Monoidal.Widesubcategory
CategoryTheory.MorphismProperty.IsStableUnderAssociator.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {P : CategoryTheory.MorphismProperty C},
  (∀ (c c' c'' : C), P (CategoryTheory.MonoidalCategoryStruct.associator c c' c'').hom) →
    (∀ (c c' c'' : C), P (CategoryTheory.MonoidalCategoryStruct.associator c c' c'').inv) → P.IsStableUnderAssociator
-- Mathlib.CategoryTheory.Preadditive.Biproducts
CategoryTheory.Limits.binaryBiconeOfIsSplitMonoOfCokernel_pt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C} {f : X ⟶ Y}
  [inst_2 : CategoryTheory.IsSplitMono f] {c : CategoryTheory.Limits.CokernelCofork f}
  (i : CategoryTheory.Limits.IsColimit c), (CategoryTheory.Limits.binaryBiconeOfIsSplitMonoOfCokernel i).pt = Y
-- Mathlib.CategoryTheory.Presentable.Basic
CategoryTheory.Functor.preservesColimitsOfShape_of_isCardinalAccessible_of_essentiallySmall : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) (κ : Cardinal.{w}) [inst_2 : Fact κ.IsRegular] [F.IsCardinalAccessible κ]
  (J : Type u₃) [inst_4 : CategoryTheory.Category.{v₃, u₃} J] [CategoryTheory.EssentiallySmall.{w, v₃, u₃} J]
  [CategoryTheory.IsCardinalFiltered J κ], CategoryTheory.Limits.PreservesColimitsOfShape J F
-- Mathlib.Algebra.Ring.Periodic
Function.Periodic.nsmul_sub_eq : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c x : α} [inst : SubtractionCommMonoid α],
  Function.Periodic f c → ∀ (n : ℕ), f (n • c - x) = f (-x)
-- Mathlib.Analysis.SpecialFunctions.Exp
Real.image_exp_Ioi : ∀ (a : ℝ), Real.exp '' Set.Ioi a = Set.Ioi (Real.exp a)
-- Mathlib.RingTheory.Polynomial.IsIntegral
IsIntegral.of_aeval_monic_of_isIntegral_coeff : ∀ {R : Type u_4} {A : Type u_5} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {x : A}
  {p : Polynomial A},
  p.Monic →
    p.natDegree ≠ 0 → IsIntegral R (Polynomial.eval x p) → (∀ (i : ℕ), IsIntegral R (p.coeff i)) → IsIntegral R x
-- Mathlib.CategoryTheory.Presentable.EssentiallyLarge
CategoryTheory.HasCardinalFilteredGenerator.exists_equivalence : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (κ : Cardinal.{w}) [inst_1 : Fact κ.IsRegular]
  [CategoryTheory.HasCardinalFilteredGenerator C κ], ∃ J x, Nonempty (C ≌ J)
-- Mathlib.Algebra.Group.Nat.Even
Nat.even_mul_succ_self : ∀ (n : ℕ), Even (n * (n + 1))
-- Mathlib.Analysis.Asymptotics.LinearGrowth
LinearGrowth.linearGrowthSupBotHom.eq_1 : LinearGrowth.linearGrowthSupBotHom =
  { toFun := LinearGrowth.linearGrowthSup, map_sup' := ⋯, map_bot' := LinearGrowth.linearGrowthSup_bot }
-- Mathlib.Order.SuccPred.Limit
/-- **Alias** of `Order.not_isPredPrelimit_of_isPredArchimedean`. -/
Order.not_isPredPrelimit : ∀ {α : Type u_1} {a : α} [inst : PartialOrder α] [inst_1 : PredOrder α] [IsPredArchimedean α] [NoMaxOrder α],
  ¬Order.IsPredPrelimit a
-- Mathlib.AlgebraicGeometry.Sites.AffineEtale
AlgebraicGeometry.Scheme.instIsEquivalenceSheafEtaleSmallEtaleTopologyAffineEtaleTopologySheafPushforwardContinuousSpec : ∀ {S : AlgebraicGeometry.Scheme} {A : Type u'} [inst : CategoryTheory.Category.{u, u'} A]
  [CategoryTheory.Limits.HasLimits A],
  ((AlgebraicGeometry.Scheme.AffineEtale.Spec S).sheafPushforwardContinuous A
      (AlgebraicGeometry.Scheme.AffineEtale.topology S) S.smallEtaleTopology).IsEquivalence
-- Std.Data.DTreeMap.Slice
Std.DTreeMap.instSliceableRoiSlice : {α : Type u} →
  {β : α → Type v} →
    (cmp : autoParam (α → α → Ordering) Std.DTreeMap.instSliceableRoiSlice._auto_1) →
      Std.Roi.Sliceable (Std.DTreeMap α β cmp) α (Std.DTreeMap.Internal.RoiSlice α β)
-- Mathlib.RingTheory.Kaehler.JacobiZariski
Algebra.Extension.Hom.toAlgHom.eq_1 : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {P : Algebra.Extension R S}
  {R' : Type u_1} {S' : Type u_2} [inst_3 : CommRing R'] [inst_4 : CommRing S'] [inst_5 : Algebra R' S']
  {P' : Algebra.Extension R' S'} [inst_6 : Algebra R R'] [inst_7 : Algebra S S'] [inst_8 : Algebra R S']
  [inst_9 : IsScalarTower R R' S'] (f : P.Hom P'), f.toAlgHom = { toRingHom := f.toRingHom, commutes' := ⋯ }
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
/-- The number π = 3.14159265... Defined here using choice as twice a zero of cos in [1,2],
from which one can derive all its properties. For explicit bounds on π,
see `Mathlib/Analysis/Real/Pi/Bounds.lean`.

Denoted `π`, once the `Real` namespace is opened.  -/
Real.pi : ℝ
-- Lean.PrettyPrinter.Delaborator.Builtins
Lean.PrettyPrinter.Delaborator.withMDatasOptions : {α : Type} → [Inhabited α] → Lean.PrettyPrinter.Delaborator.DelabM α → Lean.PrettyPrinter.Delaborator.DelabM α
-- Mathlib.Algebra.Ring.NonZeroDivisors
IsMulTorsionFree.pow_right_injective₀ : ∀ {M : Type u_2} [inst : MonoidWithZero M] [IsLeftCancelMulZero M] [IsMulTorsionFree M] {x : M},
  x ≠ 1 → x ≠ 0 → Function.Injective fun n => x ^ n
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
/-- The infinite part of the product formula : for `x ∈ K`, we have `Π_w ‖x‖_w = |norm(x)|` where
`‖·‖_w` is the normalized absolute value for `w`.  -/
NumberField.InfinitePlace.prod_eq_abs_norm : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (x : K), ∏ w, w x ^ w.mult = ↑|(Algebra.norm ℚ) x|
-- Mathlib.CategoryTheory.Functor.ReflectsIso.Jointly
CategoryTheory.JointlyReflectIsomorphisms.epi : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_4, u_1} C] {I : Type u_2} {D : I → Type u_3}
  [inst_1 : (i : I) → CategoryTheory.Category.{u_5, u_3} (D i)] {F : (i : I) → CategoryTheory.Functor C (D i)},
  CategoryTheory.JointlyReflectIsomorphisms F →
    ∀ {X Y : C} (f : X ⟶ Y) [hf : ∀ (i : I), CategoryTheory.Epi ((F i).map f)]
      [∀ (i : I), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f f) (F i)]
      [CategoryTheory.Limits.HasPushout f f], CategoryTheory.Epi f
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getKey?_insertMany_list_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {l : List (α × β)} {k k' : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l →
      k ∈ List.map Prod.fst l → (Std.ExtDTreeMap.Const.insertMany t l).getKey? k' = some k
-- Mathlib.Topology.UnitInterval
unitInterval.one_mem : 1 ∈ unitInterval
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.toLinearMap_id : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} [inst : Semiring A] [inst_1 : Monoid G] [inst_2 : AddCommMonoid V]
  [inst_3 : Module A V] (ρ : Representation A G V), (Representation.IntertwiningMap.id ρ).toLinearMap = LinearMap.id
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.map_comap_eq_self_of_surjective : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_4} [inst_2 : FunLike F M N]
  [mc : MonoidHomClass F M N] {f : F},
  Function.Surjective ⇑f → ∀ {S : Submonoid N}, Submonoid.map f (Submonoid.comap f S) = S
-- Mathlib.LinearAlgebra.FiniteDimensional.Defs
FiniteDimensional.finiteDimensional_pi : ∀ (K : Type u) [inst : DivisionRing K] {ι : Type u_1} [Finite ι], FiniteDimensional K (ι → K)
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.volume_measurePreserving_piCongrLeft : ∀ {ι : Type u_1} {ι' : Type u_2} [inst : Fintype ι] [inst_1 : Fintype ι'] (α : ι → Type u_4) (f : ι' ≃ ι)
  [inst_2 : (i : ι) → MeasureTheory.MeasureSpace (α i)] [∀ (i : ι), MeasureTheory.SigmaFinite MeasureTheory.volume],
  MeasureTheory.MeasurePreserving (⇑(MeasurableEquiv.piCongrLeft α f)) MeasureTheory.volume MeasureTheory.volume
-- Mathlib.RingTheory.MvPowerSeries.Substitution
MvPowerSeries.comp_subst_apply : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] {τ : Type u_4} {S : Type u_5} [inst_1 : CommRing S]
  [inst_2 : Algebra R S] {a : σ → MvPowerSeries τ S} {T : Type u_6} [inst_3 : CommRing T] [inst_4 : UniformSpace T]
  [inst_5 : T2Space T] [inst_6 : CompleteSpace T] [inst_7 : IsUniformAddGroup T] [inst_8 : IsTopologicalRing T]
  [inst_9 : IsLinearTopology T T] [inst_10 : Algebra R T] {ε : MvPowerSeries τ S →ₐ[R] T} [inst_11 : UniformSpace R]
  [inst_12 : DiscreteUniformity R] [inst_13 : UniformSpace S] [DiscreteUniformity S] (ha : MvPowerSeries.HasSubst a)
  (hε : Continuous ⇑ε) (f : MvPowerSeries σ R), ε (MvPowerSeries.subst a f) = (MvPowerSeries.aeval ⋯) f
-- Mathlib.Analysis.Normed.Unbundled.InvariantExtension
IsUltrametricDist.algNormOfAlgEquiv_apply : ∀ {K : Type u_1} [inst : NormedField K] {L : Type u_2} [inst_1 : Field L] [inst_2 : Algebra K L]
  [h_fin : FiniteDimensional K L] [hu : IsUltrametricDist K] (σ : Gal(L/K)) (x : L),
  (IsUltrametricDist.algNormOfAlgEquiv σ) x = (Classical.choose ⋯) (σ x)
-- Init.Sym.Lemmas
Lean.Sym.not_false_eq : (¬False) = True
-- Lean.MetavarContext
Lean.MetavarContext.abstractRange : Lean.Expr → ℕ → Array Lean.Expr → Lean.MetavarContext.MkBindingM Lean.Expr