mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Convenient.Category
ContinuousGeneratedByCat.str : {ι : Type t} →
  {X : ι → Type u} →
    [inst : (i : ι) → TopologicalSpace (X i)] → (self : ContinuousGeneratedByCat X) → TopologicalSpace ↑self
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.neighborFinset_disjoint_singleton : ∀ {V : Type u_1} (G : SimpleGraph V) (v : V) [inst : Fintype ↑(G.neighborSet v)], Disjoint (G.neighborFinset v) {v}
-- Std.Time.DateTime
/-- Getter for the `Year` inside of a `DateTime`
 -/
Std.Time.DateTime.year : Std.Time.DateTime → Std.Time.Year.Offset
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.hom_comp : ∀ {k : Type u} {G : Type v} [inst : Semiring k] [inst_1 : Monoid G] (A B C : Rep.{w, u, v} k G) (f : A ⟶ B) (g : B ⟶ C),
  Rep.Hom.hom (CategoryTheory.CategoryStruct.comp f g) = (Rep.Hom.hom g).comp (Rep.Hom.hom f)
-- Mathlib.RingTheory.GradedAlgebra.Basic
/-- The projection maps of graded algebra  -/
GradedAlgebra.proj : {ι : Type u_1} →
  {R : Type u_2} →
    {A : Type u_3} →
      [inst : DecidableEq ι] →
        [inst_1 : AddMonoid ι] →
          [inst_2 : CommSemiring R] →
            [inst_3 : Semiring A] → [inst_4 : Algebra R A] → (𝒜 : ι → Submodule R A) → [GradedAlgebra 𝒜] → ι → A →ₗ[R] A
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.rocIterator.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} [inst : Ord α] (t : Std.DTreeMap.Internal.Impl α β) (lowerBound upperBound : α),
  Std.DTreeMap.Internal.rocIterator t lowerBound upperBound =
    {
      internalState :=
        { iter := Std.DTreeMap.Internal.Zipper.prependMapGT t lowerBound Std.DTreeMap.Internal.Zipper.done,
          upper := upperBound } }
-- Mathlib.Topology.UniformSpace.Equiv
/-- If `ι` has a unique element, then `ι → α` is uniformly isomorphic to `α`.  -/
UniformEquiv.funUnique : (ι : Type u_4) → (α : Type u_5) → [Unique ι] → [inst : UniformSpace α] → (ι → α) ≃ᵤ α
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
PowerSeries.IsWeierstrassDivisorAt.eq_1 : ∀ {A : Type u_1} [inst : CommRing A] (g : PowerSeries A) (I : Ideal A),
  g.IsWeierstrassDivisorAt I = IsUnit ((PowerSeries.coeff ((PowerSeries.map (Ideal.Quotient.mk I)) g).order.toNat) g)
-- Mathlib.Order.Disjoint
disjoint_ofDual_iff : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderBot α] {a b : αᵒᵈ},
  Disjoint (OrderDual.ofDual a) (OrderDual.ofDual b) ↔ Codisjoint a b
-- Batteries.Util.ProofWanted
proof_wanted.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Data.Set.Card
Set.ncard_compl : ∀ {α : Type u_1} (s : Set α),
  autoParam s.Finite Set.ncard_compl._auto_1 →
    autoParam sᶜ.Finite Set.ncard_compl._auto_3 → sᶜ.ncard = Nat.card α - s.ncard
-- Mathlib.Analysis.Normed.Module.Multilinear.Curry
/-- Interpret a continuous multilinear map in `n + 1` variables
as a continuous linear map in `p`th variable
with values in the continuous multilinear maps in the other variables.  -/
ContinuousMultilinearMap.curryMid : {𝕜 : Type u} →
  {n : ℕ} →
    {Ei : Fin n.succ → Type wEi} →
      {G : Type wG} →
        [inst : NontriviallyNormedField 𝕜] →
          [inst_1 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)] →
            [inst_2 : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)] →
              [inst_3 : NormedAddCommGroup G] →
                [inst_4 : NormedSpace 𝕜 G] →
                  (p : Fin (n + 1)) → ContinuousMultilinearMap 𝕜 Ei G → Ei p →L[𝕜] Ei (p.succAbove i) [×n]→L[𝕜] G
-- Mathlib.LinearAlgebra.Dimension.Constructions
Module.Basis.sumQuot_repr_inl : ∀ {R : Type u_2} {V : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup V] [inst_2 : Module R V] {W : Submodule R V}
  {m : Type u_4} {n : Type u_5} (bW : Module.Basis m R ↥W) (bQ : Module.Basis n R (V ⧸ W)) (w : ↥W) (i : m),
  ((bW.sumQuot bQ).repr ↑w) (Sum.inl i) = (bW.repr w) i
-- Mathlib.Topology.MetricSpace.Closeds
TopologicalSpace.NonemptyCompacts.isometry_toCompacts : ∀ {α : Type u_1} [inst : EMetricSpace α], Isometry TopologicalSpace.NonemptyCompacts.toCompacts
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.monomial_zero_eq_C : ∀ {R : Type u_1} [inst : Semiring R], ⇑(PowerSeries.monomial 0) = ⇑PowerSeries.C
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.getEntry?.match_1.eq_1 : ∀ {α : Type u_2} {β : α → Type u_1} (motive : List ((a : α) × β a) → Sort u_3) (h_1 : Unit → motive [])
  (h_2 : (k : α) → (v : β k) → (l : List ((a : α) × β a)) → motive (⟨k, v⟩ :: l)),
  (match [] with
    | [] => h_1 ()
    | ⟨k, v⟩ :: l => h_2 k v l) =
    h_1 ()
-- Mathlib.Tactic.WLOG
Mathlib.Tactic.WLOGResult.mk : Lean.MVarId → Lean.FVarId × Lean.FVarId → Lean.MVarId → Lean.FVarId → Array Lean.FVarId → Mathlib.Tactic.WLOGResult
-- Mathlib.Topology.Order.IntermediateValue
isPreconnected_uIcc : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {a b : α}, IsPreconnected (Set.uIcc a b)
-- Lean.Elab.MutualInductive
/-- Given that the resulting type is of the form `Sort u` where `u` contains a single metavariable `?r`,
and if `univForInfer` is the result of `processResultingUniverseForInference` and is of the form `?r + k`,
then try to infer the minimal `?r` such that `?r + k` is the supremum of the constructor arguments' universe levels, if one exists.

Usually, we also throw in the constraint that `1 ≤ ?r + k`, but if `isPropCandidate` is true we allow the solution `u = 0`.
 -/
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.inferResultingUniverse : Array Lean.Elab.Command.InductiveView →
  ℕ →
    List Lean.InductiveType →
      Array Lean.Expr → Array Lean.LMVarId → Lean.Elab.TermElabM Lean.Elab.Command.ResultingUniverseResult✝
-- Mathlib.AlgebraicGeometry.Gluing
/-- (Implementation detail)
The glue data associated to a locally directed diagram.

One usually does not want to use this directly, and instead use the generic `colimit` API.
 -/
AlgebraicGeometry.Scheme.IsLocallyDirected.glueData : {J : Type w} →
  [inst : CategoryTheory.Category.{v, w} J] →
    (F : CategoryTheory.Functor J AlgebraicGeometry.Scheme) →
      [∀ {i j : J} (f : i ⟶ j), AlgebraicGeometry.IsOpenImmersion (F.map f)] →
        [(F.comp AlgebraicGeometry.Scheme.forget).IsLocallyDirected] →
          [Quiver.IsThin J] → [Small.{u, w} J] → AlgebraicGeometry.Scheme.GlueData
-- Lean.Message
_private.Lean.Message.0.Lean.MessageData.stripNestedTags.stripNestedNamePrefix : Lean.Name → Lean.Name
-- Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
iteratedDeriv_fun_sum : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {ι : Type u_7} {n : ℕ} {x : 𝕜} {f : ι → 𝕜 → F} {I : Finset ι},
  (∀ i ∈ I, ContDiffAt 𝕜 (↑n) (f i) x) → iteratedDeriv n (fun z => ∑ i ∈ I, f i z) x = ∑ i ∈ I, iteratedDeriv n (f i) x
-- Mathlib.FieldTheory.AlgebraicClosure
/-- An intermediate field of `E / F` is contained in the algebraic closure of `F` in `E`
if and only if it is algebraic over `F`.  -/
le_algebraicClosure_iff : ∀ (F : Type u_1) (E : Type u_2) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (L : IntermediateField F E),
  L ≤ algebraicClosure F E ↔ Algebra.IsAlgebraic F ↥L
-- Mathlib.Order.SuccPred.LinearLocallyFinite
toZ_strictMono : ∀ {ι : Type u_1} [inst : LinearOrder ι] [inst_1 : SuccOrder ι] [inst_2 : IsSuccArchimedean ι] [inst_3 : PredOrder ι]
  {i0 : ι}, StrictMono (toZ i0)
-- Mathlib.Order.Category.Lat
Lat.ofHom_comp : ∀ {X Y Z : Type u} [inst : Lattice X] [inst_1 : Lattice Y] [inst_2 : Lattice Z] (f : LatticeHom X Y)
  (g : LatticeHom Y Z), Lat.ofHom (g.comp f) = CategoryTheory.CategoryStruct.comp (Lat.ofHom f) (Lat.ofHom g)
-- Std.Http.Internal.Char
/-- Checks if a byte is a valid character in a URI fragment component according to RFC 3986.
`fragment = *( pchar / "/" / "?" )`
 -/
Std.Http.Internal.Char.isFragmentChar : UInt8 → Bool
-- Mathlib.Topology.Order.LocalExtr
IsLocalMinOn.min : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : LinearOrder β] {f g : α → β} {a : α} {s : Set α},
  IsLocalMinOn f s a → IsLocalMinOn g s a → IsLocalMinOn (fun x => min (f x) (g x)) s a
-- Mathlib.Data.Nat.Prime.Defs
Nat.exists_prime_and_dvd : ∀ {n : ℕ}, n ≠ 1 → ∃ p, Nat.Prime p ∧ p ∣ n
-- Mathlib.Algebra.Homology.HomotopyCategory.Shift
/-- The shift functor by `n` on `CochainComplex C ℤ` identifies to the identity
functor when `n = 0`.  -/
CochainComplex.shiftFunctorZero' : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      (n : ℤ) → n = 0 → (CochainComplex.shiftFunctor C n ≅ CategoryTheory.Functor.id (CochainComplex C ℤ))
-- Lean.Data.Trie
Lean.Data.Trie.leaf.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (a : Option α), sizeOf (Lean.Data.Trie.leaf a) = 1 + sizeOf a
-- Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
integral_smul_const : ∀ {X : Type u_1} {E : Type u_3} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] {𝕜 : Type u_8} [inst_3 : RCLike 𝕜] [inst_4 : NormedSpace 𝕜 E] [CompleteSpace E] (f : X → 𝕜)
  (c : E), ∫ (x : X), f x • c ∂μ = (∫ (x : X), f x ∂μ) • c
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurable_quotient_mk'' : ∀ {α : Type u_1} [inst : MeasurableSpace α] {s : Setoid α}, Measurable Quotient.mk''
-- Init.Data.Array.Count
Array.count_erase : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] (a b : α) (xs : Array α),
  Array.count a (xs.erase b) = Array.count a xs - if (b == a) = true then 1 else 0
-- Mathlib.Analysis.Normed.Group.Hom
/-- Coercion of a `NormedAddGroupHom` is an `AddMonoidHom`. Similar to `AddMonoidHom.coeFn`.  -/
NormedAddGroupHom.coeAddHom : {V₁ : Type u_2} →
  {V₂ : Type u_3} →
    [inst : SeminormedAddCommGroup V₁] → [inst_1 : SeminormedAddCommGroup V₂] → NormedAddGroupHom V₁ V₂ →+ V₁ → V₂
-- Lean.Util.FindLevelMVar
Lean.Expr.findLevelMVar? : Lean.Expr → (Lean.LMVarId → Bool) → Option Lean.LMVarId
-- Mathlib.Topology.Homeomorph.Defs
Equiv.toEquiv_toHomeomorphOfContinuousOpen : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : X ≃ Y)
  (h₁ : Continuous ⇑e) (h₂ : IsOpenMap ⇑e), (e.toHomeomorphOfContinuousOpen h₁ h₂).toEquiv = e
-- Mathlib.RingTheory.Jacobson.Semiprimary
IsSemisimpleModule.jacobson_le_ker : ∀ (R : Type u_1) (R₂ : Type u_2) (M : Type u_3) (M₂ : Type u_4) [inst : Ring R] [inst_1 : Ring R₂]
  [inst_2 : AddCommGroup M] [inst_3 : Module R M] [inst_4 : AddCommGroup M₂] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  [RingHomSurjective τ₁₂] [IsSemisimpleModule R₂ M₂] (f : M →ₛₗ[τ₁₂] M₂), Module.jacobson R M ≤ f.ker
-- Mathlib.Algebra.RingQuot
RingQuot.instRing : {R : Type uR} → [inst : Ring R] → (r : R → R → Prop) → Ring (RingQuot r)
-- Mathlib.CategoryTheory.MorphismProperty.Representable
/-- Variant of the pullback square when `F` is full, and given `f' : F.obj b ⟶ Y`.  -/
CategoryTheory.Functor.relativelyRepresentable.isPullback' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {Y : D} {b : C} {f' : F.obj b ⟶ Y} (hf' : F.relativelyRepresentable f') {a : C}
  (g : F.obj a ⟶ Y) [inst_2 : F.Full], CategoryTheory.IsPullback (F.map (hf'.fst' g)) (F.map (hf'.snd g)) f' g
-- Mathlib.Geometry.Convex.Cone.Face.Basic
PointedCone.IsFaceOf.sInf : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] {C : PointedCone R M} (F : Set (PointedCone R M)),
  (∀ f ∈ F, f.IsFaceOf C) → (C ⊓ sInf F).IsFaceOf C
-- Mathlib.Algebra.CharP.Two
CharTwo.neg_eq : ∀ {R : Type u_1} [inst : Ring R] [CharP R 2] (x : R), -x = x
-- Mathlib.CategoryTheory.Localization.Monoidal.Basic
CategoryTheory.Localization.Monoidal.associator_naturality₁ : ∀ {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] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : W.IsMonoidal]
  [inst_4 : L.IsLocalization W] {unit : D} (ε : L.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ unit)
  {X₁ X₂ X₃ Y₁ : CategoryTheory.LocalizedMonoidal L W ε} (f₁ : X₁ ⟶ Y₁),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerRight f₁ X₂) X₃)
      (CategoryTheory.MonoidalCategoryStruct.associator Y₁ X₂ X₃).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X₁ X₂ X₃).hom
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight f₁ (CategoryTheory.MonoidalCategoryStruct.tensorObj X₂ X₃))
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
HomogeneousIdeal.instSupSet : {ι : Type u_1} →
  {σ : Type u_2} →
    {A : Type u_3} →
      [inst : Semiring A] →
        [inst_1 : DecidableEq ι] →
          [inst_2 : AddMonoid ι] →
            [inst_3 : SetLike σ A] →
              [inst_4 : AddSubmonoidClass σ A] → {𝒜 : ι → σ} → [inst_5 : GradedRing 𝒜] → SupSet (HomogeneousIdeal 𝒜)
-- Mathlib.AlgebraicGeometry.StructureSheaf
/-- The structure sheaf on $Spec R$, valued in `CommRingCat`.

This is provided as a bundled `SheafedSpace` as `Spec.SheafedSpace R` later.  -/
AlgebraicGeometry.Spec.structureSheaf : (R : Type u) → [inst : CommRing R] → TopCat.Sheaf CommRingCat (AlgebraicGeometry.PrimeSpectrum.Top R)
-- Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete
CategoryTheory.LocallyDiscrete.mkPseudofunctor_mapComp : ∀ {B₀ : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} B₀] [inst_1 : CategoryTheory.Bicategory C]
  (obj : B₀ → C) (map : {b b' : B₀} → (b ⟶ b') → (obj b ⟶ obj b'))
  (mapId : (b : B₀) → map (CategoryTheory.CategoryStruct.id b) ≅ CategoryTheory.CategoryStruct.id (obj b))
  (mapComp :
    {b₀ b₁ b₂ : B₀} →
      (f : b₀ ⟶ b₁) →
        (g : b₁ ⟶ b₂) →
          map (CategoryTheory.CategoryStruct.comp f g) ≅ CategoryTheory.CategoryStruct.comp (map f) (map g))
  (map₂_associator :
    autoParam
      (∀ {b₀ b₁ b₂ b₃ : B₀} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃),
        CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.comp f g) h).hom
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapComp f g).hom (map h))
              (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (map f) (map g) (map h)).hom
                (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (mapComp g h).inv)
                  (mapComp f (CategoryTheory.CategoryStruct.comp g h)).inv))) =
          CategoryTheory.eqToHom ⋯)
      CategoryTheory.LocallyDiscrete.mkPseudofunctor._auto_1)
  (map₂_left_unitor :
    autoParam
      (∀ {b₀ b₁ : B₀} (f : b₀ ⟶ b₁),
        CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.id b₀) f).hom
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapId b₀).hom (map f))
              (CategoryTheory.Bicategory.leftUnitor (map f)).hom) =
          CategoryTheory.eqToHom ⋯)
      CategoryTheory.LocallyDiscrete.mkPseudofunctor._auto_3)
  (map₂_right_unitor :
    autoParam
      (∀ {b₀ b₁ : B₀} (f : b₀ ⟶ b₁),
        CategoryTheory.CategoryStruct.comp (mapComp f (CategoryTheory.CategoryStruct.id b₁)).hom
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (mapId b₁).hom)
              (CategoryTheory.Bicategory.rightUnitor (map f)).hom) =
          CategoryTheory.eqToHom ⋯)
      CategoryTheory.LocallyDiscrete.mkPseudofunctor._auto_5)
  {a b c : CategoryTheory.LocallyDiscrete B₀} (x : a ⟶ b) (x_1 : b ⟶ c),
  (CategoryTheory.LocallyDiscrete.mkPseudofunctor obj map mapId mapComp map₂_associator map₂_left_unitor
          map₂_right_unitor).mapComp
      x x_1 =
    mapComp x.as x_1.as
-- Mathlib.Analysis.Calculus.FDeriv.Equiv
fderiv_continuousLinearEquiv_comp' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {G' : Type u_5} [inst_7 : NormedAddCommGroup G']
  [inst_8 : NormedSpace 𝕜 G'] (L : G ≃L[𝕜] G') (f : E → F →L[𝕜] G),
  (fderiv 𝕜 fun x => ↑L ∘SL f x) = fun x => ↑((ContinuousLinearEquiv.refl 𝕜 F).arrowCongr L) ∘SL fderiv 𝕜 f x
-- Mathlib.Topology.Inseparable
Inseparable.eq_1 : ∀ {X : Type u_1} [inst : TopologicalSpace X] (x y : X), Inseparable x y = (nhds x = nhds y)
-- Mathlib.Algebra.Lie.Derivation.Basic
LieDerivation.lie_coe_lieDerivation_apply : ∀ (R : Type u_1) (L : Type u_2) (M : Type u_3) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M] (x : L)
  (D : LieDerivation R L M), ⁅x, ↑D⁆ = ↑⁅x, D⁆
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.snd_mk : ∀ {R : Type u} {M : Type v} (r : R) (m : M), TrivSqZeroExt.snd (r, m) = m
-- Init.Data.UInt.Bitwise
UInt32.toNat_shiftLeft : ∀ (a b : UInt32), (a <<< b).toNat = a.toNat <<< (b.toNat % 32) % 2 ^ 32
-- Mathlib.Data.Real.Basic
/-- Show an underlying Cauchy sequence for real numbers.

The representative chosen is the one passed in the VM to `Quot.mk`, so two Cauchy sequences
converging to the same number may be printed differently.
 -/
Real.instRepr : Repr ℝ
-- Mathlib.Topology.DiscreteQuotient
DiscreteQuotient.inhabitedQuotient : {X : Type u_2} →
  [inst : TopologicalSpace X] → (S : DiscreteQuotient X) → [Inhabited X] → Inhabited (Quotient S.toSetoid)
-- Init.Data.Ord.Basic
Ordering.isGE_lt : Ordering.lt.isGE = false
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
/-- The group isomorphism between group homs `G → H` and bialgebra homs `R[G] → R[H]` of group
algebras over a domain.  -/
MonoidAlgebra.mapDomainBialgHomMulEquiv : {R : Type u_1} →
  {G : Type u_5} →
    {H : Type u_6} →
      [inst : CommRing R] →
        [IsDomain R] →
          [inst_2 : CommGroup G] →
            [inst_3 : CommGroup H] → (G →* H) ≃* WithConv (MonoidAlgebra R G →ₐc[R] MonoidAlgebra R H)
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.Triangle.eqToHom_hom₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  {A B : CategoryTheory.Pretriangulated.Triangle C} (h : A = B),
  (CategoryTheory.eqToHom h).hom₁ = CategoryTheory.eqToHom ⋯
-- Init.Coe
instCoeOTC : {α : Sort u_1} → CoeOTC α α
-- Std.Internal.UV.UDP
/-- Sets the multicast interface for sending packets.
 -/
Std.Internal.UV.UDP.Socket.setMulticastInterface : Std.Internal.UV.UDP.Socket → Std.Net.IPAddr → IO Unit
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_functor_obj_str : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C C} (adj : F ⊣ G)
  (A : CategoryTheory.Endofunctor.Algebra F),
  ((CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv adj).functor.obj A).str = (adj.homEquiv A.a A.a) A.str
-- Mathlib.RingTheory.GradedAlgebra.AlgHom
GradedAlgHom.coe_toAlgHom_mk : ∀ {R : Type u_1} {A : Type u_6} {B : Type u_7} {ι : Type u_10} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : DecidableEq ι] [inst_6 : AddMonoid ι]
  {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} [inst_7 : GradedAlgebra 𝒜] [inst_8 : GradedAlgebra ℬ] {f : A →ₐ[R] B}
  (h : ∀ {i : ι} {x : A}, x ∈ 𝒜 i → f.toRingHom x ∈ ℬ i), ↑{ toAlgHom := f, map_mem := h } = f
-- Mathlib.RingTheory.Coalgebra.CoassocSimps
CoassocSimps.assoc_symm_comp_map_rid_symm_assoc : ∀ {R : Type u_1} {M : Type u_3} {N : Type u_4} {P : Type u_5} {M' : Type u_6} [inst : CommSemiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : AddCommMonoid N] [inst_4 : Module R N]
  [inst_5 : AddCommMonoid P] [inst_6 : Module R P] [inst_7 : AddCommMonoid M'] [inst_8 : Module R M'] (f : M →ₗ[R] M')
  (g : P →ₗ[R] TensorProduct R M N),
  ↑(TensorProduct.assoc R M' N R).symm ∘ₗ TensorProduct.map f ↑(TensorProduct.rid R N).symm ∘ₗ g =
    TensorProduct.map (TensorProduct.map f LinearMap.id) LinearMap.id ∘ₗ
      ↑(TensorProduct.rid R (TensorProduct R M N)).symm ∘ₗ g
-- Mathlib.RingTheory.Coalgebra.Basic
Pi.comul_comp_dFinsuppCoeFnLinearMap : ∀ {R : Type u_1} {n : Type u_2} [inst : CommSemiring R] [inst_1 : Fintype n] [inst_2 : DecidableEq n] {A : n → Type u_3}
  [inst_3 : (i : n) → AddCommMonoid (A i)] [inst_4 : (i : n) → Module R (A i)]
  [inst_5 : (i : n) → CoalgebraStruct R (A i)],
  CoalgebraStruct.comul ∘ₗ DFinsupp.coeFnLinearMap R =
    TensorProduct.map (DFinsupp.coeFnLinearMap R) (DFinsupp.coeFnLinearMap R) ∘ₗ CoalgebraStruct.comul
-- Lean.KeyedDeclsAttribute
Lean.KeyedDeclsAttribute.ExtensionState.mk : {γ : Type} →
  List Lean.KeyedDeclsAttribute.OLeanEntry →
    Lean.KeyedDeclsAttribute.Table γ →
      Lean.PHashSet Lean.Name → Lean.PHashSet Lean.Name → Lean.KeyedDeclsAttribute.ExtensionState γ
-- Mathlib.Topology.Defs.Induced
Topology.IsEmbedding.toIsInducing : ∀ {X : Type u_1} {Y : Type u_2} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] {f : X → Y},
  Topology.IsEmbedding f → Topology.IsInducing f
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.mkIso.congr_simp : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {X : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] {S S' : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X}
  (eₗ eₗ_1 : S.fst ≅ S'.fst) (e_eₗ : eₗ = eₗ_1) (eᵣ eᵣ_1 : S.snd ≅ S'.snd) (e_eᵣ : eᵣ = eᵣ_1)
  (w :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight eₗ.hom F) S'.iso.hom =
      CategoryTheory.CategoryStruct.comp S.iso.hom (CategoryTheory.Functor.whiskerRight eᵣ.hom G)),
  CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.mkIso eₗ eᵣ w =
    CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.mkIso eₗ_1 eᵣ_1 ⋯
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.IsAffineOpen.appLE_eq_away_map : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {U : Y.Opens} (hU : AlgebraicGeometry.IsAffineOpen U) {V : X.Opens}
  (hV : AlgebraicGeometry.IsAffineOpen V) (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U)
  (r : ↑(Y.presheaf.obj (Opposite.op U))),
  AlgebraicGeometry.Scheme.Hom.appLE f (Y.basicOpen r)
      (X.basicOpen ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appLE f U V e)) r)) ⋯ =
    CommRingCat.ofHom
      (IsLocalization.Away.map (↑(Y.presheaf.1 (Opposite.op (Y.basicOpen r))))
        (↑(X.presheaf.1
            (Opposite.op
              (X.basicOpen ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appLE f U V e)) r)))))
        (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appLE f U V e)) r)
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
abs_choice : ∀ {α : Type u_1} [inst : AddGroup α] [inst_1 : LinearOrder α] (x : α), |x| = x ∨ |x| = -x
-- Mathlib.RingTheory.Spectrum.Prime.RingHom
PrimeSpectrum.sigmaToPi_not_surjective_of_infinite : ∀ {ι : Type u_3} (R : ι → Type u_2) [inst : (i : ι) → CommSemiring (R i)] [Infinite ι] [∀ (i : ι), Nontrivial (R i)],
  ¬Function.Surjective (PrimeSpectrum.sigmaToPi R)
-- Mathlib.ModelTheory.Syntax
/-- `&n` is notation for the bound variable indexed by `n` in a bounded formula.  -/
FirstOrder.«term&_» : Lean.ParserDescr
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.balanceLErasePrecond_zero_iff' : ∀ {n : ℕ}, Std.DTreeMap.Internal.Impl.BalanceLErasePrecond n 0 ↔ n ≤ 3
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey!_eq_getKeyD_default : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited α] {a : α}, m.getKey! a = m.getKeyD a default