mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.ConcreteCategory.EpiMono
CategoryTheory.ConcreteCategory.injective_eq_monomorphisms_iff : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC],
  CategoryTheory.MorphismProperty.injective C = CategoryTheory.MorphismProperty.monomorphisms C ↔
    (CategoryTheory.forget C).PreservesMonomorphisms
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.instIsIsoH₁Inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E F : CategoryTheory.PreOneHypercover S} (e : E ≅ F)
  {i j : F.I₀} (k : F.I₁ i j), CategoryTheory.IsIso (e.inv.h₁ k)
-- Mathlib.RingTheory.PiTensorProduct
/-- Lifting a multilinear map to an algebra homomorphism from tensor product
 -/
PiTensorProduct.liftAlgHom : {ι : Type u_1} →
  {R : Type u_3} →
    {A : ι → Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : (i : ι) → Semiring (A i)] →
          [inst_2 : (i : ι) → Algebra R (A i)] →
            {S : Type u_5} →
              [inst_3 : Semiring S] →
                [inst_4 : Algebra R S] →
                  (f : MultilinearMap R A S) →
                    f 1 = 1 →
                      (∀ (x y : (i : ι) → A i), f (x * y) = f x * f y) → (PiTensorProduct R fun i => A i) →ₐ[R] S
-- Mathlib.FieldTheory.SeparableDegree
/-- The separable degree of a polynomial is equal to
the number of distinct roots of it over any algebraically closed field.  -/
Polynomial.natSepDegree_eq_of_isAlgClosed : ∀ {F : Type u} (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (f : Polynomial F)
  [inst_3 : DecidableEq E] [IsAlgClosed E], f.natSepDegree = (f.aroots E).toFinset.card
-- Init.Data.String.Lemmas.Pattern.String.ForwardSearcher
_private.Init.Data.String.Lemmas.Pattern.String.ForwardSearcher.0.String.Slice.Pattern.Model.ForwardSliceSearcher.Invariants.isValidSearchFrom_toList : ∀ {pat s : String.Slice} {stackPos needlePos : String.Pos.Raw} (it : Std.Iter (String.Slice.Pattern.SearchStep s))
  (h : String.Slice.Pattern.Model.ForwardSliceSearcher.Invariants✝ pat s needlePos stackPos)
  {table : Vector ℕ pat.utf8ByteSize} {ht : table = String.Slice.Pattern.ForwardSliceSearcher.buildTable pat}
  {hn : needlePos < pat.rawEndPos},
  it = { internalState := String.Slice.Pattern.ForwardSliceSearcher.proper pat table ht stackPos needlePos hn } →
    ∀ {p : s.Pos},
      p = String.Slice.Pattern.Model.ForwardSliceSearcher.Invariants.base✝ h →
        String.Slice.Pattern.Model.IsValidSearchFrom pat p it.toList
-- Mathlib.Topology.UniformSpace.Basic
/-- An entourage of the diagonal in `α` and an entourage in `β` yield an entourage in `α × β`
once we permute coordinates.  -/
entourageProd : {α : Type ua} → {β : Type ub} → SetRel α α → SetRel β β → SetRel (α × β) (α × β)
-- Mathlib.Algebra.Algebra.Subalgebra.Prod
Subalgebra.center_prod : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B],
  Subalgebra.center R (A × B) = (Subalgebra.center R A).prod (Subalgebra.center R B)
-- Mathlib.Analysis.Analytic.OfScalars
FormalMultilinearSeries.ofScalars_norm : ∀ {𝕜 : Type u_1} (E : Type u_2) [inst : NontriviallyNormedField 𝕜] [inst_1 : SeminormedRing E]
  [inst_2 : NormedAlgebra 𝕜 E] (c : ℕ → 𝕜) (n : ℕ) [NormOneClass E], ‖FormalMultilinearSeries.ofScalars E c n‖ = ‖c n‖
-- Mathlib.Tactic.CrossRefAttribute
Mathlib.CrossRef.instOrdDatabase.ord : Mathlib.CrossRef.Database → Mathlib.CrossRef.Database → Ordering
-- Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
/-- The entire function of `s` which agrees with
` Gamma ((s + 1) / 2) * π ^ (-(s + 1) / 2) * ∑' (n : ℕ), sin (2 * π * a * n) / n ^ s`
for `1 < re s`.
 -/
HurwitzZeta.completedSinZeta : UnitAddCircle → ℂ → ℂ
-- Mathlib.Algebra.Order.GroupWithZero.Basic
one_lt_div₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [MulPosReflectLT G₀] {a b : G₀},
  0 < b → (1 < a / b ↔ b < a)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueD_filter_containsKey_of_containsKey_eq_false_left : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] {l₁ l₂ : List ((_ : α) × β)} {k : α} {fallback : β},
  Std.Internal.List.DistinctKeys l₁ →
    Std.Internal.List.containsKey k l₁ = false →
      Std.Internal.List.getValueD k (List.filter (fun p => Std.Internal.List.containsKey p.fst l₂) l₁) fallback =
        fallback
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
/-- Given a fully faithful functor `ι : D ⥤ C ⥤ V` and mere existence of Day convolutions of
`ι.obj d` and `ι.obj d'` such that the convolution remains in the essential image of `ι`,
construct an `InducedLawfulDayConvolutionMonoidalCategoryStructCore` by letting all other
data be the generic ones from the `HasPointwiseLeftKanExtension` API.  -/
CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.ofHasDayConvolutions : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {V : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} V] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          [inst_3 : CategoryTheory.MonoidalCategory V] →
            {D : Type u₃} →
              [inst_4 : CategoryTheory.Category.{v₃, u₃} D] →
                (ι : CategoryTheory.Functor D (CategoryTheory.Functor C V)) →
                  ι.FullyFaithful →
                    [hasDayConvolution :
                        ∀ (d d' : D),
                          (CategoryTheory.MonoidalCategory.tensor C).HasPointwiseLeftKanExtension
                            (CategoryTheory.MonoidalCategory.externalProduct (ι.obj d) (ι.obj d'))] →
                      (∀ (d d' : D),
                          ι.essImage
                            ((CategoryTheory.MonoidalCategory.tensor C).pointwiseLeftKanExtension
                              (CategoryTheory.MonoidalCategory.externalProduct (ι.obj d) (ι.obj d')))) →
                        [hasDayConvolutionUnit :
                            (CategoryTheory.Functor.fromPUnit
                                  (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).HasPointwiseLeftKanExtension
                              (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit V))] →
                          ι.essImage
                              ((CategoryTheory.Functor.fromPUnit
                                    (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).pointwiseLeftKanExtension
                                (CategoryTheory.Functor.fromPUnit
                                  (CategoryTheory.MonoidalCategoryStruct.tensorUnit V))) →
                            CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore C V D
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Predicates
Tactic.ComputeAsymptotics.UnitMonomial.FirstNonzeroIsNeg.of_head : ∀ {hd : ℝ} (tl : Tactic.ComputeAsymptotics.UnitMonomial),
  hd < 0 → Tactic.ComputeAsymptotics.UnitMonomial.FirstNonzeroIsNeg (hd :: tl)
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.GeneratorNode.mctx : Lean.Meta.SynthInstance.GeneratorNode → Lean.MetavarContext
-- Mathlib.CategoryTheory.Elements
CategoryTheory.CategoryOfElements.comp_val : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)} {p q r : F.Elements}
  {f : p ⟶ q} {g : q ⟶ r}, ↑(CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp ↑f ↑g
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.maxKey!_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α],
  t.WF →
    ∀ {k : α} {v : β k}, (t.insert k v).maxKey! = t.maxKey?.elim k fun k' => if (cmp k' k).isLE = true then k else k'
-- Mathlib.RingTheory.OrderOfVanishing.Basic
Ring.ord_mul_of_isUnit_left : ∀ {R : Type u_1} [inst : CommRing R] {a : R}, IsUnit a → ∀ (x : R), Ring.ord R (a * x) = Ring.ord R x
-- Lean.Meta.CongrTheorems
_private.Lean.Meta.CongrTheorems.0.Lean.Meta.mkCongrSimpCore?.mk?.go : Bool →
  Lean.Expr →
    Lean.Meta.FunInfo →
      Array Lean.Meta.CongrArgKind →
        Array Lean.Expr →
          ℕ → Array Lean.Expr → Array (Option Lean.Meta.EqInfo✝) → Array Lean.Expr → Lean.MetaM Lean.Meta.CongrTheorem
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.DHashMap.Internal.Raw₀.Const.insertMany.eq_1 : ∀ {α : Type u} {β : Type v} {ρ : Type w} [inst : ForIn Id ρ (α × β)] [inst_1 : BEq α] [inst_2 : Hashable α]
  (m : Std.DHashMap.Internal.Raw₀ α fun x => β) (l : ρ),
  Std.DHashMap.Internal.Raw₀.Const.insertMany m l =
    (have r := ⟨m, ⋯⟩;
      do
      let __s ←
        forIn l r fun x __s =>
            let r := __s;
            match x with
            | (a, b) =>
              have r := ⟨(↑r).insert a b, ⋯⟩;
              pure (ForInStep.yield r)
      have r :
        { m' //
          ∀ (P : (Std.DHashMap.Internal.Raw₀ α fun x => β) → Prop),
            (∀ {m'' : Std.DHashMap.Internal.Raw₀ α fun x => β} {a : α} {b : β}, P m'' → P (m''.insert a b)) →
              P m → P m' } :=
        __s
      pure r).run
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.vlt.ne_zero : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] {x y : R}, x <ᵥ y → y ≠ 0
-- Init.Data.Array.Monadic
Array.idRun_forIn_yield_eq_foldl : ∀ {α : Type u_1} {β : Type u_2} {xs : Array α} (f : α → β → Id β) (init : β),
  (forIn xs init fun a b => ForInStep.yield <$> f a b).run = Array.foldl (fun b a => (f a b).run) init xs
-- Mathlib.Algebra.Order.Ring.Cast
Int.cast_le_neg_one_or_one_le_cast_of_ne_zero : ∀ (R : Type u_1) [inst : Ring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] {n : ℤ}, n ≠ 0 → ↑n ≤ -1 ∨ 1 ≤ ↑n
-- Mathlib.FieldTheory.Minpoly.IsConjRoot
/-- `y` is a conjugate root of `x` over `K` if and only if `y` is a root of the minimal polynomial of
`x`. This is variant of `isConjRoot_iff_aeval_eq_zero`.
 -/
isConjRoot_iff_mem_minpoly_rootSet : ∀ {K : Type u_2} {S : Type u_4} [inst : CommRing S] [inst_1 : Field K] [inst_2 : Algebra K S] [inst_3 : IsDomain S]
  {x y : S}, IsIntegral K x → (IsConjRoot K x y ↔ y ∈ (minpoly K x).rootSet S)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.erase!.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α),
  Std.DTreeMap.Internal.Impl.erase! k Std.DTreeMap.Internal.Impl.leaf = Std.DTreeMap.Internal.Impl.leaf
-- Mathlib.Topology.EMetricSpace.PairReduction
/-- We recursively define a log-size ball sequence `(Vᵢ, tᵢ, rᵢ)` by
* `V₀ = J`, `t₀` is chosen arbitrarily in `J`, `r₀` is the log-size radius of `t₀` in `V₀`
* `Vᵢ₊₁ = Vᵢ \ {x ∈ V | d(t, x) ≤ (rᵢ - 1)c}`, `tᵢ₊₁` is chosen arbitrarily in `Vᵢ₊₁`, `rᵢ₊₁` is
  the log-size radius of `tᵢ₊₁` in `Vᵢ₊₁`.  -/
PairReduction.logSizeBallSeq : {T : Type u_1} →
  [PseudoEMetricSpace T] →
    [DecidableEq T] → (J : Finset T) → J.Nonempty → ENNReal → ENNReal → ℕ → PairReduction.logSizeBallStruct T
-- Mathlib.MeasureTheory.Integral.MeanInequalities
/-- Hölder's inequality for functions `α → ℝ≥0`. The integral of the product of two functions
is bounded by the product of their `ℒp` and `ℒq` seminorms when `p` and `q` are conjugate
exponents.  -/
NNReal.lintegral_mul_le_Lp_mul_Lq : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {p q : ℝ},
  p.HolderConjugate q →
    ∀ {f g : α → NNReal},
      AEMeasurable f μ →
        AEMeasurable g μ →
          ∫⁻ (a : α), ↑((f * g) a) ∂μ ≤ (∫⁻ (a : α), ↑(f a) ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), ↑(g a) ^ q ∂μ) ^ (1 / q)
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
AlgebraicGeometry.ProjectiveSpectrum.Proj.stalkMap_toSpec : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] (f : A) (x : ↥(ProjectiveSpectrum.basicOpen 𝒜 f)) {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m),
  AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec 𝒜 f) x =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.ProjectiveSpectrum.Proj.specStalkEquiv 𝒜 f x f_deg hm).hom
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.stalkIso' 𝒜 ↑x).toCommRingCatIso.inv
        ((AlgebraicGeometry.Proj.toLocallyRingedSpace 𝒜).restrictStalkIso ⋯ x).inv)
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Tactic.ComputeAsymptotics.BasisExtension.insert_tail_wellFormedBasis : ∀ {basis : Tactic.ComputeAsymptotics.Basis} {f : ℝ → ℝ} {ex_tl : Tactic.ComputeAsymptotics.BasisExtension basis},
  Tactic.ComputeAsymptotics.WellFormedBasis (Tactic.ComputeAsymptotics.BasisExtension.insert f ex_tl).getBasis →
    Tactic.ComputeAsymptotics.WellFormedBasis ex_tl.getBasis
-- Mathlib.Data.Matrix.PEquiv
/-- `toMatrix` returns a matrix containing ones and zeros. `f.toMatrix i j` is `1` if
`f i = some j` and `0` otherwise  -/
PEquiv.toMatrix : {m : Type u_3} → {n : Type u_4} → {α : Type u_5} → [DecidableEq n] → [Zero α] → [One α] → (m ≃. n) → Matrix m n α
-- Std.Data.DHashMap.Internal.Raw
_private.Std.Data.DHashMap.Internal.Raw.0.Std.DHashMap.Raw.filter.eq_1 : ∀ {α : Type u} {β : α → Type v} (f : (a : α) → β a → Bool) (m : Std.DHashMap.Raw α β),
  Std.DHashMap.Raw.filter f m = if h : 0 < m.buckets.size then ↑(Std.DHashMap.Internal.Raw₀.filter f ⟨m, h⟩) else ∅
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.min!_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : Inhabited α] {k : α},
  (t.insert k).min! = t.min?.elim k fun k' => if cmp k k' = Ordering.lt then k else k'
-- Mathlib.Topology.Category.Profinite.Nobeling.Successor
/-- The `ℤ`-linear map induced by precomposing with `CC'₀`  -/
Profinite.NobelingProof.Linear_CC'₀ : {I : Type u} →
  (C : Set (I → Bool)) →
    [inst : LinearOrder I] →
      [inst_1 : WellFoundedLT I] →
        {o : Ordinal.{u}} →
          (ho : o < Ordinal.type fun x1 x2 => x1 < x2) →
            LocallyConstant ↑C ℤ →ₗ[ℤ] LocallyConstant ↑(Profinite.NobelingProof.C' C ho) ℤ
-- Mathlib.CategoryTheory.Limits.Presheaf
CategoryTheory.Presheaf.compULiftYonedaIsoULiftYonedaCompLan.coconeApp_naturality : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D}
  {G :
    CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ (Type (max w v₁ v₂)))
      (CategoryTheory.Functor Dᵒᵖ (Type (max w v₁ v₂)))}
  (φ : F.comp CategoryTheory.uliftYoneda.{max w v₁, v₂, u₂} ⟶ CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁}.comp G)
  {P : CategoryTheory.Functor Cᵒᵖ (Type (max w v₁ v₂))} {x y : P.Elements} (f : x ⟶ y),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.uliftYoneda.{max v₂ w, v₁, u₁}.map (↑f).unop)
      (CategoryTheory.Presheaf.compULiftYonedaIsoULiftYonedaCompLan.coconeApp φ x) =
    CategoryTheory.Presheaf.compULiftYonedaIsoULiftYonedaCompLan.coconeApp φ y
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.fundamentalDomain_idealLattice : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K]
  (I : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ),
  MeasureTheory.IsAddFundamentalDomain (↥(NumberField.mixedEmbedding.idealLattice K I))
    (ZSpan.fundamentalDomain (NumberField.mixedEmbedding.fractionalIdealLatticeBasis K I)) MeasureTheory.volume
-- Mathlib.RingTheory.Ideal.IsPrincipal
/-- A nonzero principal ideal in an integral domain `R` is isomorphic to `R` as a module.
The isomorphism we choose here sends `1` to the generator chosen by `Ideal.generator`.  -/
Ideal.isoBaseOfIsPrincipal : {R : Type u_1} →
  [inst : CommRing R] → [IsDomain R] → {I : Ideal R} → [hprinc : Submodule.IsPrincipal I] → I ≠ ⊥ → R ≃ₗ[R] ↥I
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
_private.Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense.0.CategoryTheory.Functor.OneHypercoverDenseData.isSheaf_iff.liftAux.congr_simp : ∀ {C₀ : Type u₀} {C : Type u} [inst : CategoryTheory.Category.{v₀, u₀} C₀] [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor C₀ C} {J₀ : CategoryTheory.GrothendieckTopology C₀}
  {J : CategoryTheory.GrothendieckTopology C} {A : Type u'} [inst_2 : CategoryTheory.Category.{v', u'} A]
  [inst_3 : CategoryTheory.Functor.IsDenseSubsite J₀ J F] {data : (X : C) → F.OneHypercoverDenseData J₀ J X}
  {G : CategoryTheory.Functor Cᵒᵖ A} (hG₀ : CategoryTheory.Presheaf.IsSheaf J₀ (F.op.comp G)) {X : C} {S : J.Cover X}
  (s : CategoryTheory.Limits.Multifork (S.index G)) (i : (data X).I₀),
  CategoryTheory.Functor.OneHypercoverDenseData.isSheaf_iff.liftAux✝ hG₀ s i =
    CategoryTheory.Functor.OneHypercoverDenseData.isSheaf_iff.liftAux✝ hG₀ s i
-- Mathlib.Analysis.Convex.Gauge
/-- If the given subset is `Absorbent` then the set we take an infimum over in `gauge` is nonempty,
which is useful for proving many properties about the gauge.  -/
Absorbent.gauge_set_nonempty : ∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {s : Set E} {x : E},
  Absorbent ℝ s → {r | 0 < r ∧ x ∈ r • s}.Nonempty
-- Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Polynomial.IsMonicOfDegree.natDegree_eq : ∀ {R : Type u_1} [inst : Semiring R] {p : Polynomial R} {n : ℕ}, p.IsMonicOfDegree n → p.natDegree = n
-- Init.Data.SInt.IntToBitVec
ISize.toBitVec64_and : ∀ (a b : ISize) (h : System.Platform.numBits = 64), (a &&& b).toBitVec64 h = a.toBitVec64 h &&& b.toBitVec64 h
-- Mathlib.Data.Sign.Defs
instInhabitedSignType.default : SignType
-- Mathlib.Data.Set.Inclusion
Set.inclusion_eq_id : ∀ {α : Type u_1} {s : Set α} (h : s ⊆ s), Set.inclusion h = id
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.affineOpensRestrict_apply_coe_coe : ∀ {X : AlgebraicGeometry.Scheme} (U : X.Opens) (a : ↑(↑U).affineOpens),
  ↑↑((AlgebraicGeometry.affineOpensRestrict U) a) = (AlgebraicGeometry.Scheme.Hom.opensFunctor U.ι).obj ↑a
-- Mathlib.Topology.Order.OrderClosed
SuccOrder.nhdsLE_eq_nhds : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [ClosedIciTopology α] [SuccOrder α] (a : α),
  nhdsWithin a (Set.Iic a) = nhds a
-- Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice
csInf_inv : ∀ {M : Type u_1} [inst : ConditionallyCompleteLattice M] [inst_1 : Group M] [MulLeftMono M] [MulRightMono M]
  {s : Set M}, s.Nonempty → BddAbove s → sInf s⁻¹ = (sSup s)⁻¹
-- Batteries.Recycling.RBTree.Alter
/-- The defining property of a balanced path: If `path` is a `c₀,n₀` tree with a `c,n` hole,
then filling the hole with a `c,n` tree yields a `c₀,n₀` tree.
 -/
RBTree.RBNode.Path.Balanced.fill : ∀ {α : Type u_1} {c₀ : RBTree.RBColor} {n₀ : ℕ} {c : RBTree.RBColor} {n : ℕ} {path : RBTree.RBNode.Path α}
  {t : RBTree.RBNode α}, RBTree.RBNode.Path.Balanced c₀ n₀ path c n → t.Balanced c n → (path.fill t).Balanced c₀ n₀
-- Mathlib.Algebra.Algebra.Equiv
/-- Algebra equivalences are symmetric.  -/
AlgEquiv.symm : {R : Type uR} →
  {A₁ : Type uA₁} →
    {A₂ : Type uA₂} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A₁] →
          [inst_2 : Semiring A₂] → [inst_3 : Algebra R A₁] → [inst_4 : Algebra R A₂] → (A₁ ≃ₐ[R] A₂) → A₂ ≃ₐ[R] A₁
-- Init.Data.List.Impl
/-- Drop `none`s from a list, and replace each remaining `some a` with `a`.  -/
List.reduceOption : {α : Type u_1} → List (Option α) → List α
-- Lean.Elab.InfoTree.Types
Lean.Elab.Info.ofCommandInfo.inj : ∀ {i i_1 : Lean.Elab.CommandInfo}, Lean.Elab.Info.ofCommandInfo i = Lean.Elab.Info.ofCommandInfo i_1 → i = i_1
-- Mathlib.SetTheory.Cardinal.HasCardinalLT
hasCardinalLT_union : ∀ {X : Type u_1} {S₁ S₂ : Set X} {κ : Cardinal.{u_2}},
  Cardinal.aleph0 ≤ κ → HasCardinalLT (↑S₁) κ → HasCardinalLT (↑S₂) κ → HasCardinalLT (↑(S₁ ∪ S₂)) κ
-- Mathlib.Data.Fin.VecNotation
Matrix.cons_val_four : ∀ {α : Type u} {m : ℕ} (x : α) (u : Fin m.succ.succ.succ.succ → α),
  Matrix.vecCons x u 4 = Matrix.vecHead (Matrix.vecTail (Matrix.vecTail (Matrix.vecTail u)))
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.nnnorm_sub_eq_max : ∀ {α : Type u} [inst : TopologicalSpace α] {R : Type u_1} [inst_1 : NonUnitalSeminormedRing R] [IsCancelMulZero R]
  {f g : BoundedContinuousFunction α R}, f * g = 0 → ‖f - g‖₊ = max ‖f‖₊ ‖g‖₊
-- Mathlib.Algebra.Order.Group.Action
le_pow_smul : ∀ {G : Type u_4} [inst : Monoid G] {α : Type u_5} [inst_1 : Preorder α] {g : G} {a : α} [inst_2 : MulAction G α]
  [CovariantClass G α HSMul.hSMul LE.le], a ≤ g • a → ∀ (n : ℕ), a ≤ g ^ n • a
-- Mathlib.Algebra.BigOperators.Expect
algebraMap.coe_expect : ∀ {ι : Type u_1} {M : Type u_4} {N : Type u_5} [inst : Semifield M] [inst_1 : CharZero M] [inst_2 : Semifield N]
  [inst_3 : CharZero N] [inst_4 : Algebra M N] (s : Finset ι) (f : ι → M),
  ↑(s.expect fun i => f i) = s.expect fun i => ↑(f i)
-- Lean.Environment
_private.Lean.Environment.0.Lean.AsyncConst.constInfo : Lean.AsyncConst✝ → Lean.AsyncConstantInfo
-- Aesop.Tree.Data
Aesop.Rapp.modify : (Aesop.RappData Aesop.Goal Aesop.MVarCluster → Aesop.RappData Aesop.Goal Aesop.MVarCluster) → Aesop.Rapp → Aesop.Rapp
-- Mathlib.Data.Set.Lattice
Set.iUnion_union_distrib : ∀ {β : Type u_2} {ι : Sort u_5} (s t : ι → Set β), ⋃ i, s i ∪ t i = (⋃ i, s i) ∪ ⋃ i, t i
-- Mathlib.CategoryTheory.MorphismProperty.Factorization
CategoryTheory.MorphismProperty.HasFunctorialFactorization.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C},
  Nonempty (W₁.FunctorialFactorizationData W₂) → W₁.HasFunctorialFactorization W₂
-- Mathlib.Topology.UniformSpace.Defs
UniformSpace.ball_inter_right : ∀ {β : Type ub} (x : β) (V W : Set (β × β)), UniformSpace.ball x (V ∩ W) ⊆ UniformSpace.ball x W
-- Init.Data.List.Sublist
List.sublist_filter_iff : ∀ {α : Type u_1} {l₂ l₁ : List α} {p : α → Bool},
  l₁.Sublist (List.filter p l₂) ↔ ∃ l', l'.Sublist l₂ ∧ l₁ = List.filter p l'
-- Mathlib.Analysis.Calculus.Implicit
/-- Left function  -/
ImplicitFunctionData.leftFun : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          [inst_3 : CompleteSpace E] →
            {F : Type u_3} →
              [inst_4 : NormedAddCommGroup F] →
                [inst_5 : NormedSpace 𝕜 F] →
                  [inst_6 : CompleteSpace F] →
                    {G : Type u_4} →
                      [inst_7 : NormedAddCommGroup G] →
                        [inst_8 : NormedSpace 𝕜 G] → [inst_9 : CompleteSpace G] → ImplicitFunctionData 𝕜 E F G → E → F
-- Mathlib.Algebra.Ring.Opposite
MulOpposite.instAddMonoidWithOne : {R : Type u_1} → [AddMonoidWithOne R] → AddMonoidWithOne Rᵐᵒᵖ
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
SimpleGraph.TripartiteFromTriangles.toTriangle_apply : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : DecidableEq α] [inst_1 : DecidableEq β] [inst_2 : DecidableEq γ]
  (x : α × β × γ), SimpleGraph.TripartiteFromTriangles.toTriangle x = {Sum3.in₀ x.1, Sum3.in₁ x.2.1, Sum3.in₂ x.2.2}
-- Mathlib.Algebra.Module.Torsion.Free
IsAddTorsionFree.to_isTorsionFree_nat : ∀ {M : Type u_3} [inst : AddCommMonoid M] [IsAddTorsionFree M], Module.IsTorsionFree ℕ M
-- Mathlib.SetTheory.ZFC.Ordinal
/-- The von Neumann ordinal corresponding to a given `Ordinal`, as a `PSet`.

The elements of `o.toPSet` are all `a.toPSet` with `a < o`.  -/
Ordinal.toPSet : Ordinal.{u} → PSet.{u}
-- Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
Diffeomorph.image_boundary : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {N : Type u_7} [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace H' N] {n : WithTop ℕ∞},
  n ≠ 0 → ∀ (Φ : Diffeomorph I I' M N n), ⇑Φ '' ModelWithCorners.boundary M = ModelWithCorners.boundary N