mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Comma.Over.Pullback
/-- Note that the binary coproducts assumption is necessary: the existence of a left adjoint to
`Under.forget X` is equivalent to the existence of each binary coproduct `X ⨿ -`.  -/
CategoryTheory.Under.instIsRightAdjointForget : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryCoproducts C],
  (CategoryTheory.Under.forget X).IsRightAdjoint
-- Mathlib.Algebra.Group.Subsemigroup.Operations
/-- The semigroup hom associated to an inclusion of subsemigroups.  -/
Subsemigroup.inclusion : {M : Type u_1} → [inst : Mul M] → {S T : Subsemigroup M} → S ≤ T → ↥S →ₙ* ↥T
-- Std.Data.DTreeMap.Internal.Balancing
/-- Internal implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.rotateL : {α : Type u} →
  {β : α → Type v} →
    (k : α) →
      β k →
        Std.DTreeMap.Internal.Impl α β →
          (rk : α) →
            β rk → Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl α β
-- Mathlib.Topology.Connected.Clopen
/-- If `ι` indexes a disjoint union decomposition of `α`, it is equivalent to the connected
components of `α`.  -/
ConnectedComponents.equivOfIsClopenOfIsConnected : {α : Type u} →
  [inst : TopologicalSpace α] →
    {ι : Type u_3} →
      {U : ι → Set α} →
        (∀ (i : ι), IsClopen (U i)) →
          Pairwise (Function.onFun Disjoint U) →
            ⋃ i, U i = Set.univ → (∀ (i : ι), IsConnected (U i)) → ConnectedComponents α ≃ ι
-- Init.Data.Nat.Dvd
Nat.dvd_trans : ∀ {a b c : ℕ}, a ∣ b → b ∣ c → a ∣ c
-- Mathlib.Topology.UniformSpace.LocallyUniformConvergence
TendstoLocallyUniformlyOn.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : TopologicalSpace α] [inst_1 : UniformSpace β] (F : ι → α → β)
  (f : α → β) (p : Filter ι) (s : Set α),
  TendstoLocallyUniformlyOn F f p s =
    ∀ u ∈ uniformity β, ∀ x ∈ s, ∃ t ∈ nhdsWithin x s, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
-- Mathlib.CategoryTheory.Limits.Shapes.End
CategoryTheory.Limits.endFunctor_obj : ∀ (J : Type u) [inst : CategoryTheory.Category.{v, u} J] (C : Type u') [inst_1 : CategoryTheory.Category.{v', u'} C]
  [inst_2 : ∀ (F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)), CategoryTheory.Limits.HasEnd F]
  (F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)),
  (CategoryTheory.Limits.endFunctor J C).obj F = CategoryTheory.Limits.end_ F
-- Mathlib.Algebra.Polynomial.Bivariate
Polynomial.evalEval_zero : ∀ {R : Type u_1} [inst : Semiring R] (x y : R), Polynomial.evalEval x y 0 = 0
-- Mathlib.Data.Complex.Basic
Complex.instSub : Sub ℂ
-- Mathlib.Algebra.Group.Graph
/-- The graph of a group homomorphism as a subgroup.

See also `AddMonoidHom.mgraph` for the graph as a submonoid.  -/
AddMonoidHom.graph : {G : Type u_1} → {H : Type u_2} → [inst : AddGroup G] → [inst_1 : AddGroup H] → (G →+ H) → AddSubgroup (G × H)
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.log_div_log : ∀ {b x : ℝ}, Real.log x / Real.log b = Real.logb b x
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- Given three nonzero vectors, the angle between the second and the third plus the angle
between the first and the second equals the angle between the first and the third.  -/
Orientation.oangle_add_swap : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y z : V}, x ≠ 0 → y ≠ 0 → z ≠ 0 → o.oangle y z + o.oangle x y = o.oangle x z
-- Mathlib.Order.Interval.Finset.Fin
Fin.map_valEmbedding_Icc : ∀ {n : ℕ} (a b : Fin n), Finset.map Fin.valEmbedding (Finset.Icc a b) = Finset.Icc ↑a ↑b
-- Mathlib.Topology.Bornology.Basic
Filter.disjoint_cobounded_iff : ∀ {α : Type u_2} [inst : Bornology α] {l : Filter α},
  Disjoint l (Bornology.cobounded α) ↔ ∃ s ∈ l, Bornology.IsBounded s
-- Init.Data.List.Nat.Count
List.count_insert : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a b : α} {l : List α},
  List.count a (List.insert b l) = max (List.count a l) (if (b == a) = true then 1 else 0)
-- Mathlib.Algebra.Order.Module.Defs
instSMulPosStrictMonoNatOfIsOrderedCancelAddMonoid : ∀ {M : Type u_3} [inst : PartialOrder M] [inst_1 : AddCommMonoid M] [IsOrderedCancelAddMonoid M], SMulPosStrictMono ℕ M
-- Init.Data.String.Lemmas.Pattern.Basic
/-- This data-carrying typeclass is used to give semantics to a pattern type that implements
`ForwardPattern` and/or `ToForwardSearcher` by providing an abstract, not necessarily
decidable `PatternModel.Matches` predicate that implementations of `ForwardPattern`
and `ToForwardSearcher` can be validated against.

Correctness results for generic functions relying on the pattern infrastructure, for example the
correctness result for `String.Slice.split`, are then
stated in terms of `PatternModel.Matches`, and can be specialized to specific patterns
from there.

The corresponding compatibility typeclasses are
`String.Slice.Pattern.Model.LawfulForwardPatternModel`
and
`String.Slice.Pattern.Model.LawfulToForwardSearcherModel`.
 -/
String.Slice.Pattern.Model.PatternModel : {ρ : Type} → ρ → Type
-- Mathlib.Topology.Homotopy.Lifting
IsQuotientCoveringMap.fundamentalGroupToMulOpposite_apply_eq_Iff : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {p : E → X} {G : Type u_4}
  [inst_2 : Group G] [inst_3 : MulAction G E] (hp : IsQuotientCoveringMap p G) {x : X} {e : ↑(p ⁻¹' {x})}
  {γ : FundamentalGroup X x} {g : Gᵐᵒᵖ},
  (hp.fundamentalGroupToMulOpposite e) γ = g ↔ MulOpposite.unop g • ↑e = ↑(⋯.monodromy γ e)
-- Mathlib.Analysis.Normed.Ring.Basic
/-- A non-unital normed commutative ring is a non-unital seminormed commutative ring.  -/
NonUnitalNormedCommRing.toNonUnitalSeminormedCommRing : {α : Type u_2} → [β : NonUnitalNormedCommRing α] → NonUnitalSeminormedCommRing α
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getD_map_of_getKey?_eq_some : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {γ : Type w} {t : Std.DTreeMap.Internal.Impl α fun x => β}
  [Std.TransOrd α] {f : α → β → γ} {k k' : α} {fallback : γ},
  t.WF →
    t.getKey? k = some k' →
      Std.DTreeMap.Internal.Impl.Const.getD (Std.DTreeMap.Internal.Impl.map f t) k fallback =
        (Option.map (f k') (Std.DTreeMap.Internal.Impl.Const.get? t k)).getD fallback
-- Lean.DocString.Markdown
/-- Tracks which inline delimiters are already open so that nested `*` / `**` / `[…](…)` don't emit
redundant openers and closers.
 -/
Lean.Doc.MarkdownM.InlineCtx : Type
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.RankLeOneStruct.mk.inj : ∀ {R : Type u_1} {inst : Semiring R} {inst_1 : ValuativeRel R} {emb : ValuativeRel.ValueGroupWithZero R →*₀ NNReal}
  {strictMono : StrictMono ⇑emb} {emb_1 : ValuativeRel.ValueGroupWithZero R →*₀ NNReal}
  {strictMono_1 : StrictMono ⇑emb_1},
  { emb := emb, strictMono := strictMono } = { emb := emb_1, strictMono := strictMono_1 } → emb = emb_1
-- Mathlib.CategoryTheory.Subobject.FactorThru
CategoryTheory.Subobject.factorThru_mk_self : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [inst_1 : CategoryTheory.Mono f],
  (CategoryTheory.Subobject.mk f).factorThru f ⋯ = (CategoryTheory.Subobject.underlyingIso f).inv
-- Mathlib.Geometry.Manifold.Instances.Real
/-- The manifold structure on `[x, y]` is smooth.  -/
instIsManifoldIcc : ∀ (x y : ℝ) [inst : Fact (x < y)] {n : WithTop ℕ∞}, IsManifold (modelWithCornersEuclideanHalfSpace 1) n ↑(Set.Icc x y)
-- Mathlib.Data.Set.Lattice.Image
Set.mapsTo_iUnion_iUnion : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {s : ι → Set α} {t : ι → Set β} {f : α → β},
  (∀ (i : ι), Set.MapsTo f (s i) (t i)) → Set.MapsTo f (⋃ i, s i) (⋃ i, t i)
-- Mathlib.Algebra.Category.Semigrp.Basic
MagmaCat.Hom.hom.eq_1 : ∀ {X Y : MagmaCat} (f : X.Hom Y), f.hom = CategoryTheory.ConcreteCategory.hom f
-- Std.Data.HashMap.Lemmas
Std.HashMap.get.congr_simp : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} (m m_1 : Std.HashMap α β) (e_m : m = m_1) (a a_1 : α)
  (e_a : a = a_1) (h : a ∈ m), m.get a h = m_1.get a_1 ⋯
-- Mathlib.Algebra.Group.Subgroup.Defs
/-- The `normalizer` of `S` is the subgroup of `G` whose elements satisfy `g * S * g⁻¹ = S`.
When `S` is a subgroup, this is the largest subgroup of `G` inside which `S` is normal.  -/
Subgroup.normalizer : {G : Type u_1} → [inst : Group G] → Set G → Subgroup G
-- Mathlib.Order.SuccPred.CompleteLinearOrder
Order.IsSuccLimit.iSup_Iio : ∀ {α : Type u_2} [inst : ConditionallyCompleteLinearOrderBot α] {x : α}, Order.IsSuccLimit x → ⨆ a, ↑a = x
-- Lean.Elab.InfoTree.Types
Lean.Elab.Info.ofDocElabInfo.injEq : ∀ (i i_1 : Lean.Elab.DocElabInfo), (Lean.Elab.Info.ofDocElabInfo i = Lean.Elab.Info.ofDocElabInfo i_1) = (i = i_1)
-- Mathlib.Algebra.Order.Group.Opposite
AddOpposite.unop_le_one : ∀ {α : Type u_1} [inst : CommMonoid α] [inst_1 : PartialOrder α] {a : αᵃᵒᵖ}, AddOpposite.unop a ≤ 1 ↔ a ≤ 1
-- Mathlib.Topology.Algebra.OpenSubgroup
IsTopologicalAddGroup.exist_add_closure_nhds : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [IsTopologicalAddGroup G] [CompactSpace G]
  {W : Set G}, IsClopen W → ∃ T ∈ nhds 0, W + T ⊆ W
-- Mathlib.Algebra.GroupWithZero.Defs
CommGroupWithZero.toInv : {G₀ : Type u_2} → [self : CommGroupWithZero G₀] → Inv G₀
-- Mathlib.RingTheory.HahnSeries.Addition
HahnSeries.orderTop_add_eq_right : ∀ {R : Type u_3} [inst : AddMonoid R] {Γ : Type u_8} [inst_1 : LinearOrder Γ] {x y : HahnSeries Γ R},
  y.orderTop < x.orderTop → (x + y).orderTop = y.orderTop
-- Mathlib.Geometry.Manifold.Diffeomorph
ModelWithCorners.coe_transContinuousLinearEquiv_symm : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {H : Type u_5}
  [inst_5 : TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) (e : E ≃L[𝕜] E'),
  ↑(I.transContinuousLinearEquiv e).symm = ↑I.symm ∘ ⇑e.symm
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
CategoryTheory.Limits.desc_op_comp_opCoproductIsoProduct'_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C}
  {c : CategoryTheory.Limits.Cofan Z} {f : CategoryTheory.Limits.Fan fun x => Opposite.op (Z x)}
  (hc : CategoryTheory.Limits.IsColimit c) (hf : CategoryTheory.Limits.IsLimit f) (c' : CategoryTheory.Limits.Cofan Z),
  CategoryTheory.CategoryStruct.comp (hc.desc c').op (CategoryTheory.Limits.opCoproductIsoProduct' hc hf).hom =
    hf.lift c'.op
-- Mathlib.Geometry.Euclidean.PerpBisector
AffineSubspace.mem_perpBisector_iff_inner_pointReflection_vsub_eq_zero : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {c p₁ p₂ : P},
  c ∈ AffineSubspace.perpBisector p₁ p₂ ↔ inner ℝ ((Equiv.pointReflection c) p₁ -ᵥ p₂) (p₂ -ᵥ p₁) = 0
-- Mathlib.Algebra.BigOperators.Finprod
finprod_curry : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : CommMonoid M] (f : α × β → M),
  Function.HasFiniteMulSupport f → ∏ᶠ (ab : α × β), f ab = ∏ᶠ (a : α) (b : β), f (a, b)
-- Mathlib.Topology.Order.ScottTopology
Topology.IsScottHausdorff.isClosed_of_isUpperSet : ∀ {α : Type u_1} {s : Set α} {D : Set (Set α)} [inst : Preorder α] [t : TopologicalSpace α]
  [Topology.IsScottHausdorff α D], IsLowerSet D → IsUpperSet s → IsClosed s
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
/-- A Dedekind domain is equal to the intersection of its localizations at all its height one
non-zero prime ideals viewed as subalgebras of its field of fractions.  -/
IsDedekindDomain.HeightOneSpectrum.iInf_localization_eq_bot : ∀ (R : Type u_1) (K : Type u_3) [inst : CommRing R] [inst_1 : Field K] [inst_2 : IsDedekindDomain R]
  [inst_3 : Algebra R K] [hK : IsFractionRing R K], ⨅ v, Localization.subalgebra.ofField K v.asIdeal.primeCompl ⋯ = ⊥
-- Mathlib.RingTheory.Congruence.Defs
RingConGen.Rel.of : ∀ {R : Type u_1} [inst : Add R] [inst_1 : Mul R] {r : R → R → Prop} (x y : R), r x y → RingConGen.Rel r x y
-- Lean.Setup
Lean.instFromJsonModuleArtifacts.fromJson : Lean.Json → Except String Lean.ModuleArtifacts
-- Mathlib.Tactic.Ring.Basic
/-- Cast ℕ and ℤ normalized expressions ExSums into `α`, used to evaluate scalar multiplications.  -/
Mathlib.Tactic.Ring.RingCompute.cast : {u : Lean.Level} →
  {α : Q(Type u)} →
    (sα : Q(CommSemiring «$α»)) →
      Mathlib.Tactic.Ring.Common.Cache sα →
        (v : Lean.Level) →
          (β : Q(Type v)) →
            Q(CommSemiring «$β») →
              (_smul : Q(SMul «$β» «$α»)) →
                (x : Q(«$β»)) →
                  Mathlib.Tactic.AtomM
                    ((y : Q(«$α»)) ×
                      Mathlib.Tactic.Ring.Common.ExSum Mathlib.Tactic.Ring.RatCoeff sα q(«$y») ×
                        Q(∀ (a : «$α»), «$x» • a = «$y» * a))
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
/-- If `C` has colimits of shape `J` and `G` preserves them, then if `G` reflects isomorphisms then it
reflects colimits of shape `J`.
 -/
CategoryTheory.Limits.reflectsColimitsOfShape_of_reflectsIsomorphisms : ∀ {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] {G : CategoryTheory.Functor C D} [G.ReflectsIsomorphisms]
  [CategoryTheory.Limits.HasColimitsOfShape J C] [CategoryTheory.Limits.PreservesColimitsOfShape J G],
  CategoryTheory.Limits.ReflectsColimitsOfShape J G
-- Mathlib.CategoryTheory.Triangulated.Triangulated
CategoryTheory.Triangulated.Octahedron.comm₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃}
  {comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃} {v₁₂ : X₂ ⟶ Z₁₂}
  {w₁₂ : Z₁₂ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁}
  {h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  {v₂₃ : X₃ ⟶ Z₂₃} {w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₂}
  {h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  {v₁₃ : X₃ ⟶ Z₁₃} {w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁}
  {h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  (self : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃), CategoryTheory.CategoryStruct.comp self.m₁ w₁₃ = w₁₂
-- Init.Data.Array.GetLit
_private.Init.Data.Array.GetLit.0.List.take.match_1.eq_2 : ∀ {α : Type u_1} (motive : ℕ → List α → Sort u_2) (n : ℕ) (h_1 : (x : List α) → motive 0 x)
  (h_2 : (n : ℕ) → motive n.succ []) (h_3 : (n : ℕ) → (a : α) → (as : List α) → motive n.succ (a :: as)),
  (match n.succ, [] with
    | 0, x => h_1 x
    | n.succ, [] => h_2 n
    | n.succ, a :: as => h_3 n a as) =
    h_2 n
-- Mathlib.Data.Nat.Totient
Nat.totient_eq_iff_prime : ∀ {p : ℕ}, 0 < p → (p.totient = p - 1 ↔ Nat.Prime p)
-- Init.Data.SInt.Bitwise
Int16.shiftRight_or : ∀ {a b c : Int16}, (a ||| b) >>> c = a >>> c ||| b >>> c
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.eval.eq_5 : ∀ (cf cg : Nat.Partrec.Code), (cf.pair cg).eval = fun n => Nat.pair <$> cf.eval n <*> cg.eval n
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.coprod.epi_desc_of_epi_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y : C}
  [inst_1 : CategoryTheory.Limits.HasBinaryCoproduct X Y] (f : X ⟶ W) (g : Y ⟶ W) [CategoryTheory.Epi g],
  CategoryTheory.Epi (CategoryTheory.Limits.coprod.desc f g)
-- Init.Data.SInt.Lemmas
Int16.ofIntLE_sub : ∀ {a b : ℤ} {hab₁ : Int16.minValue.toInt ≤ a - b} {hab₂ : a - b ≤ Int16.maxValue.toInt},
  Int16.ofIntLE (a - b) hab₁ hab₂ = Int16.ofInt a - Int16.ofInt b
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.FriendlyOperation.comp : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis}
  {op₁ op₂ :
    Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl →
      Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl},
  Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.FriendlyOperation op₁ →
    Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.FriendlyOperation op₂ →
      Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.FriendlyOperation (op₁ ∘ op₂)
-- Mathlib.Geometry.RingedSpace.PresheafedSpace
/-- The map to the restriction of a presheafed space along the canonical inclusion from the top
subspace.
 -/
AlgebraicGeometry.PresheafedSpace.toRestrictTop : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] → (X : AlgebraicGeometry.PresheafedSpace C) → X ⟶ X.restrict ⋯
-- Mathlib.Analysis.RCLike.Basic
RCLike.reCLM_apply : ∀ {K : Type u_1} [inst : RCLike K], ⇑RCLike.reCLM = ⇑RCLike.re
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey_beq : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l : List ((a : α) × β a)} {a : α}
  (h : Std.Internal.List.containsKey a l = true), (Std.Internal.List.getKey a l h == a) = true
-- Mathlib.Analysis.Normed.Field.Lemmas
Filter.inv_nhdsNE_zero : ∀ {α : Type u_1} [inst : NormedDivisionRing α], (nhdsWithin 0 {0}ᶜ)⁻¹ = Bornology.cobounded α
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get?_of_isEmpty : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp], t.WF → ∀ {a : α}, t.isEmpty = true → t.get? a = none
-- Mathlib.Analysis.LocallyConvex.BalancedCoreHull
nhds_basis_balanced : ∀ (𝕜 : Type u_1) (E : Type u_2) [inst : NormedDivisionRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [ContinuousSMul 𝕜 E] [(nhdsWithin 0 {0}ᶜ).NeBot],
  (nhds 0).HasBasis (fun s => s ∈ nhds 0 ∧ Balanced 𝕜 s) id
-- Mathlib.Analysis.Polynomial.Basic
Polynomial.isEquivalent_cobounded_leading_monomial : ∀ {R : Type u_2} [inst : NormedRing R] [NormMulClass R] {P : Polynomial R},
  Asymptotics.IsEquivalent (Bornology.cobounded R) (fun x => Polynomial.eval x P) fun x =>
    P.leadingCoeff * x ^ P.natDegree
-- Mathlib.Geometry.Manifold.Notation
/-- Attempt to find a model with corners on a manifold, or on the charted space of a manifold.  -/
_private.Mathlib.Geometry.Manifold.Notation.0.Manifold.Elab.findModelInner.fromManifold : Lean.Expr → Lean.Elab.TermElabM Lean.Expr
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.contains_insertManyIfNewUnit_list : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtDHashMap α fun x => Unit} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List α} {k : α},
  (Std.ExtDHashMap.Const.insertManyIfNewUnit m l).contains k = (m.contains k || l.contains k)
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.algebraMap_eq : ∀ {R : Type u_1} [inst : CommRing R] (f : Polynomial R), algebraMap R (AdjoinRoot f) = AdjoinRoot.of f
-- Mathlib.SetTheory.Cardinal.Regular
Cardinal.IsInaccessible.mk : ∀ {c : Cardinal.{u_1}}, Cardinal.aleph0 < c → c ≤ c.ord.cof → c.IsStrongPrelimit → c.IsInaccessible
-- Mathlib.LinearAlgebra.TensorProduct.Map
/-- `LinearMap.rTensor M f : N ⊗ M →ₗ P ⊗ M` is the natural linear map
induced by `f : N →ₗ P`.  -/
LinearMap.rTensor : {R : Type u_1} →
  [inst : CommSemiring R] →
    (M : Type u_7) →
      {N : Type u_8} →
        {P : Type u_9} →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : AddCommMonoid N] →
              [inst_3 : AddCommMonoid P] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R N] →
                    [inst_6 : Module R P] → (N →ₗ[R] P) → TensorProduct R N M →ₗ[R] TensorProduct R P M
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.Ordered.memP_iff_upperBound? : ∀ {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {t : RBTree.RBNode α} [Std.TransCmp cmp]
  [RBTree.RBNode.IsCut cmp cut],
  RBTree.RBNode.Ordered cmp t →
    (RBTree.RBNode.MemP cut t ↔ ∃ x, RBTree.RBNode.upperBound? cut t = some x ∧ cut x = Ordering.eq)
-- Mathlib.CategoryTheory.Shift.Pullback
/-- The natural isomorphism between the identity of `PullbackShift C φ` and the
pullback of the identity of `C`.
 -/
CategoryTheory.NatTrans.PullbackShift.natIsoId : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {A : Type u_2} →
      {B : Type u_3} →
        [inst_1 : AddMonoid A] →
          [inst_2 : AddMonoid B] →
            [inst_3 : CategoryTheory.HasShift C B] →
              (φ : A →+ B) →
                CategoryTheory.Functor.id (CategoryTheory.PullbackShift C φ) ≅
                  CategoryTheory.PullbackShift.functor φ (CategoryTheory.Functor.id C)
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientAddGroup.mk'_surjective : ∀ {G : Type u_1} [inst : AddGroup G] (N : AddSubgroup G) [nN : N.Normal], Function.Surjective ⇑(QuotientAddGroup.mk' N)
-- Init.Data.Array.BasicAux
_private.Init.Data.Array.BasicAux.0.mapMonoMImp.go : {m : Type u_1 → Type u_2} → {α : Type u_1} → [Monad m] → (α → m α) → ℕ → Array α → m (Array α)
-- Mathlib.Analysis.Normed.Operator.Basic
ContinuousLinearMap.norm_postcomp_le : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {E : Type u_4} {F : Type u_5} {G : Type u_7}
  [inst : SeminormedAddCommGroup E] [inst_1 : SeminormedAddCommGroup F] [inst_2 : SeminormedAddCommGroup G]
  [inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NontriviallyNormedField 𝕜₂] [inst_5 : NontriviallyNormedField 𝕜₃]
  [inst_6 : NormedSpace 𝕜 E] [inst_7 : NormedSpace 𝕜₂ F] [inst_8 : NormedSpace 𝕜₃ G] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₃ : 𝕜₂ →+* 𝕜₃}
  {σ₁₃ : 𝕜 →+* 𝕜₃} [inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [inst_10 : RingHomIsometric σ₁₂]
  [inst_11 : RingHomIsometric σ₁₃] [RingHomIsometric σ₂₃] (L : F →SL[σ₂₃] G), ‖ContinuousLinearMap.postcomp E L‖ ≤ ‖L‖
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.RespectsIso.monomorphisms : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C], (CategoryTheory.MorphismProperty.monomorphisms C).RespectsIso
-- Mathlib.Algebra.Category.Grp.Preadditive
/-- `AddCommGrpCat.Hom.hom` bundled as an additive equivalence.  -/
AddCommGrpCat.homAddEquiv : {M N : AddCommGrpCat} → (M ⟶ N) ≃+ (↑M →+ ↑N)
-- Mathlib.Algebra.QuaternionBasis
/-- There is a natural quaternionic basis for the `QuaternionAlgebra`.  -/
QuaternionAlgebra.Basis.self : (R : Type u_1) → [inst : CommRing R] → {c₁ c₂ c₃ : R} → QuaternionAlgebra.Basis (QuaternionAlgebra R c₁ c₂ c₃) c₁ c₂ c₃
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.rpow_rpow_inv_eq_iff : ∀ {x : NNReal} {y : ℝ}, (x ^ y) ^ y⁻¹ = x ↔ y ≠ 0 ∨ x = 1
-- Mathlib.Order.RelSeries
RelSeries.head_singleton : ∀ {α : Type u_1} {r : SetRel α α} (x : α), (RelSeries.singleton r x).head = x
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyData.isIso_p : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.RightHomologyData), S.f = 0 → CategoryTheory.IsIso h.p
-- Mathlib.Algebra.Module.LinearMap.End
/-- Composition by `f : M₂ → M₃` is a linear map from the space of linear maps `M → M₂`
to the space of linear maps `M → M₃`.  -/
LinearMap.compRight : {R : Type u_1} →
  (S : Type u_3) →
    {M : Type u_4} →
      {M₁ : Type u_5} →
        {M₂ : Type u_6} →
          [inst : Semiring R] →
            [inst_1 : Semiring S] →
              [inst_2 : AddCommMonoid M] →
                [inst_3 : AddCommMonoid M₁] →
                  [inst_4 : AddCommMonoid M₂] →
                    [inst_5 : Module R M] →
                      [inst_6 : Module R M₁] →
                        [inst_7 : Module R M₂] →
                          [inst_8 : Module S M₁] →
                            [inst_9 : Module S M₂] →
                              [inst_10 : SMulCommClass R S M₁] →
                                [inst_11 : SMulCommClass R S M₂] →
                                  [LinearMap.CompatibleSMul M₁ M₂ S R] → (M₁ →ₗ[R] M₂) → (M →ₗ[R] M₁) →ₗ[S] M →ₗ[R] M₂