mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Enriched.FunctorCategory
CategoryTheory.Enriched.FunctorCategory.enrichedComp.eq_1 : ∀ (V : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} C] {J : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} J]
  [inst_4 : CategoryTheory.EnrichedOrdinaryCategory V C] (F₁ F₂ F₃ : CategoryTheory.Functor J C)
  [inst_5 : CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₁ F₂]
  [inst_6 : CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₂ F₃]
  [inst_7 : CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₁ F₃],
  CategoryTheory.Enriched.FunctorCategory.enrichedComp V F₁ F₂ F₃ =
    CategoryTheory.Limits.end_.lift
      (fun j =>
        CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.tensorHom
            (CategoryTheory.Limits.end_.π (CategoryTheory.Enriched.FunctorCategory.diagram V F₁ F₂) j)
            (CategoryTheory.Limits.end_.π (CategoryTheory.Enriched.FunctorCategory.diagram V F₂ F₃) j))
          (CategoryTheory.eComp V (Opposite.unop (F₁.op.obj (Opposite.op j))) (F₂.obj j) (F₃.obj j)))
      ⋯
-- Mathlib.CategoryTheory.Monoidal.Bimon_
/-- Auxiliary definition for `equivMonComonCounitIsoApp`.  -/
CategoryTheory.Bimon.equivMonComonCounitIsoAppXAux : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        (M : CategoryTheory.Mon (CategoryTheory.Comon C)) →
          (((CategoryTheory.Bimon.ofMonComon C).comp (CategoryTheory.Bimon.toMonComon C)).obj M).X.X ≅ M.X.X
-- Init.Data.AC
Lean.Data.AC.Context.sort_loop_nonEmpty : ∀ {ys : List ℕ} (xs : List ℕ), xs ≠ [] → Lean.Data.AC.sort.loop xs ys ≠ []
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
ciInf_eq_bot_of_bot_mem : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : OrderBot α] {f : ι → α},
  ⊥ ∈ Set.range f → iInf f = ⊥
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgEquiv.refl_symm : ∀ {R : Type u_2} {A : Type u_3} [inst : Add A] [inst_1 : Mul A] [inst_2 : SMul R A] [inst_3 : Star A],
  (StarAlgEquiv.refl R A).symm = StarAlgEquiv.refl R A
-- Mathlib.Algebra.Star.Subalgebra
/-- The star subalgebra `StarSubalgebra.adjoin R {x}` generated by a single `x : A` is commutative
if `x` is normal.  -/
StarAlgebra.isMulCommutative_adjoin_singleton : ∀ (R : Type u_2) {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : StarRing A] [inst_5 : StarModule R A] (x : A) [IsStarNormal x],
  IsMulCommutative ↥(StarAlgebra.adjoin R {x})
-- Init.Data.BitVec.Bitblast
_private.Init.Data.BitVec.Bitblast.0.BitVec.resRec.match_1.eq_1 : ∀ {w : ℕ} (s : ℕ) (motive : (s' : ℕ) → s' + 1 < w → 0 < s' + 1 → s = s'.succ → Sort u_1) (hs : 0 + 1 < w)
  (hslt : 0 < 0 + 1) (hs0 : s = Nat.succ 0)
  (h_1 : (hs : 0 + 1 < w) → (hslt : 0 < 0 + 1) → (hs0 : s = Nat.succ 0) → 0 = 0 → motive 0 hs hslt hs0)
  (h_2 :
    (s'' : ℕ) →
      (hs : s'' + 1 + 1 < w) →
        (hslt : 0 < s'' + 1 + 1) → (hs0 : s = (s'' + 1).succ) → 0 = s''.succ → motive s''.succ hs hslt hs0),
  (match hs' : 0, hs, hslt, hs0 with
    | 0, hs, hslt, hs0 => h_1 hs hslt hs0 hs'
    | s''.succ, hs, hslt, hs0 => h_2 s'' hs hslt hs0 hs') =
    h_1 hs hslt hs0 ⋯
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.distinct_keys : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) t.keys
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.isReduced_iff_not_step : ∀ {α : Type u} {L₁ : List (α × Bool)}, FreeGroup.IsReduced L₁ ↔ ∀ (L₂ : List (α × Bool)), ¬FreeGroup.Red.Step L₁ L₂
-- Mathlib.RingTheory.Ideal.IsPrimary
Ideal.isPrimary_of_isMaximal_radical : ∀ {R : Type u_1} [inst : CommSemiring R] {I : Ideal R}, I.radical.IsMaximal → I.IsPrimary
-- Mathlib.MeasureTheory.Function.ConvergenceInMeasure
MeasureTheory.TendstoInMeasure.comp : ∀ {α : Type u_1} {ι : Type u_2} {κ : Type u_3} {E : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : EDist E] {l : Filter ι} {f : ι → α → E} {g : α → E} {v : Filter κ} {ns : κ → ι},
  MeasureTheory.TendstoInMeasure μ f l g → Filter.Tendsto ns v l → MeasureTheory.TendstoInMeasure μ (f ∘ ns) v g
-- Mathlib.GroupTheory.GroupAction.Support
MulAction.Supports.eq_1 : ∀ (G : Type u_1) {α : Type u_3} {β : Type u_4} [inst : SMul G α] [inst_1 : SMul G β] (s : Set α) (b : β),
  MulAction.Supports G s b = ∀ (g : G), (∀ ⦃a : α⦄, a ∈ s → g • a = a) → g • b = b
-- Batteries.Data.Vector.Lemmas
Vector.scanlM_empty : ∀ {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} {init : β} [inst : Monad m] [LawfulMonad m] {f : β → α → m β},
  Vector.scanlM f init #v[] = pure #v[init]
-- Mathlib.Data.Matrix.ColumnRowPartitioned
Matrix.toRows₂_fromRows : ∀ {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R),
  (A₁.fromRows A₂).toRows₂ = A₂
-- Mathlib.MeasureTheory.Function.LpSpace.Indicator
MeasureTheory.memLp_add_of_disjoint : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] {f g : α → E},
  Disjoint (Function.support f) (Function.support g) →
    MeasureTheory.StronglyMeasurable f →
      MeasureTheory.StronglyMeasurable g →
        (MeasureTheory.MemLp (f + g) p μ ↔ MeasureTheory.MemLp f p μ ∧ MeasureTheory.MemLp g p μ)
-- Mathlib.Algebra.GroupWithZero.NonZeroDivisors
nonZeroDivisorsEquivUnits_symm_apply_coe : ∀ {G₀ : Type u_1} [inst : GroupWithZero G₀] (u : G₀ˣ), ↑(nonZeroDivisorsEquivUnits.symm u) = ↑u
-- Mathlib.NumberTheory.FunctionField
/-- **Alias** of `RatFunc.inftyValuationDef`. -/
FunctionField.inftyValuationDef : (F : Type u_1) → [inst : Field F] → [DecidableEq (RatFunc F)] → RatFunc F → WithZero (Multiplicative ℤ)
-- Mathlib.NumberTheory.ArithmeticFunction.Defs
ArithmeticFunction.one_one : ∀ {R : Type u_1} [inst : Zero R] [inst_1 : One R], 1 1 = 1
-- Mathlib.Combinatorics.SimpleGraph.Metric
SimpleGraph.Reachable.coe_dist_eq_edist : ∀ {V : Type u_1} {G : SimpleGraph V} {u v : V}, G.Reachable u v → ↑(G.dist u v) = G.edist u v
-- Mathlib.MeasureTheory.Measure.Hausdorff
/-- Given a function `m : ℝ≥0∞ → ℝ≥0∞`, `mkMetric m` is the supremum of `μ r` over `r > 0`, where
`μ r` is the maximal outer measure `μ` such that `μ s ≤ m s` for all sets `s` that contain at least
two points. While each `mkMetric'.pre` is an *outer* measure, the supremum is a measure.  -/
MeasureTheory.Measure.mkMetric : {X : Type u_2} →
  [inst : EMetricSpace X] →
    [inst_1 : MeasurableSpace X] → [BorelSpace X] → (ENNReal → ENNReal) → MeasureTheory.Measure X
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.setIntegral_const : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {s : Set X} {μ : MeasureTheory.Measure X} [CompleteSpace E] (c : E), ∫ (x : X) in s, c ∂μ = μ.real s • c
-- Mathlib.Topology.Instances.Matrix
Matrix.blockDiagonal'_tsum : ∀ {X : Type u_1} {l : Type u_3} {R : Type u_8} {m' : l → Type u_9} {n' : l → Type u_10} [inst : AddCommMonoid R]
  [inst_1 : TopologicalSpace R] {L : SummationFilter X} [inst_2 : DecidableEq l] [T2Space R]
  {f : X → (i : l) → Matrix (m' i) (n' i) R},
  Matrix.blockDiagonal' (∑'[L] (x : X), f x) = ∑'[L] (x : X), Matrix.blockDiagonal' (f x)
-- Mathlib.CategoryTheory.Localization.SmallShiftedHom
/-- The type of morphisms from `X` to `Y⟦m⟧` in the localized category
with respect to `W : MorphismProperty C` that is shrunk to `Type w`
when `HasSmallLocalizedShiftedHom.{w} W X Y` holds.  -/
CategoryTheory.Localization.SmallShiftedHom : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (W : CategoryTheory.MorphismProperty C) →
      {M : Type w'} →
        [inst_1 : AddMonoid M] →
          [inst_2 : CategoryTheory.HasShift C M] →
            (X Y : C) → [CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Y] → M → Type w
-- Mathlib.Algebra.GradedMonoid
GradedMonoid.GMonoid.mk : {ι : Type u_1} →
  {A : ι → Type u_2} →
    [inst : AddMonoid ι] →
      [toGMul : GradedMonoid.GMul A] →
        [toGOne : GradedMonoid.GOne A] →
          (∀ (a : GradedMonoid A), 1 * a = a) →
            (∀ (a : GradedMonoid A), a * 1 = a) →
              (∀ (a b c : GradedMonoid A), a * b * c = a * (b * c)) →
                (gnpow : (n : ℕ) → {i : ι} → A i → A (n • i)) →
                  autoParam (∀ (a : GradedMonoid A), GradedMonoid.mk (0 • a.fst) (gnpow 0 a.snd) = 1)
                      GradedMonoid.GMonoid.gnpow_zero'._autoParam →
                    autoParam
                        (∀ (n : ℕ) (a : GradedMonoid A),
                          GradedMonoid.mk (n.succ • a.fst) (gnpow n.succ a.snd) = ⟨n • a.fst, gnpow n a.snd⟩ * a)
                        GradedMonoid.GMonoid.gnpow_succ'._autoParam →
                      GradedMonoid.GMonoid A
-- Mathlib.Data.Nat.Cast.Defs
_private.Mathlib.Data.Nat.Cast.Defs.0.Nat.unaryCast.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match 0 with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_1 ()
-- Mathlib.Topology.Homotopy.HomotopyGroup
GenLoop.continuous_currySum : ∀ {N : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {M : Type u_3} (x : X), Continuous (GenLoop.currySum x)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
/-- The norm at the infinite place `w` of an element of the mixed space  -/
NumberField.mixedEmbedding.normAtPlace : {K : Type u_1} → [inst : Field K] → NumberField.InfinitePlace K → NumberField.mixedEmbedding.mixedSpace K →*₀ ℝ
-- Init.Core
/-- Gets the thunk's value. If the value is cached, it is returned in constant time; if not, it is
computed.

Computed values are cached, so the value is not recomputed.
 -/
Thunk.get : {α : Type u_1} → Thunk α → α
-- Mathlib.Algebra.Homology.ShortComplex.Abelian
CategoryTheory.ShortComplex.LeftHomologyData.ofAbelian_K : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex C),
  (CategoryTheory.ShortComplex.LeftHomologyData.ofAbelian S).K = CategoryTheory.Limits.kernel S.g
-- Lean.MonadEnv
/-- Matches if `e` is a constant that is an inductive type with one constructor.
Such types can be used with primitive projections.
See also `Lean.matchConstNonRecStructure` for a more restrictive version.
 -/
Lean.matchConstStructure : {m : Type → Type} →
  {α : Type} →
    [Monad m] →
      [Lean.MonadEnv m] →
        [Lean.MonadError m] →
          Lean.Expr → (Unit → m α) → (Lean.InductiveVal → List Lean.Level → Lean.ConstructorVal → m α) → m α
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
/-- If A is an R-algebra all of whose elements are integral over R,
and x is an element of an A-algebra that is integral over A, then x is integral over R.  -/
isIntegral_trans : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Ring B]
  [inst_3 : Algebra A B] [inst_4 : Algebra R B] [inst_5 : Algebra R A] [IsScalarTower R A B] [Algebra.IsIntegral R A]
  (x : B), IsIntegral A x → IsIntegral R x
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Ideal.squarefree_span_singleton : ∀ {R : Type u_1} [inst : CommRing R] [IsDomain R] [IsPrincipalIdealRing R] {a : R},
  Squarefree (Ideal.span {a}) ↔ Squarefree a
-- Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
/-- Given `P : ObjectProperty C`, and a presentation `P.LimitOfShape J X`
of an object `X : C`, this is the induced functor `J ⥤ StructuredArrow P.ι X`.  -/
CategoryTheory.ObjectProperty.LimitOfShape.toStructuredArrow : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {P : CategoryTheory.ObjectProperty C} →
      {J : Type u'} →
        [inst_1 : CategoryTheory.Category.{v', u'} J] →
          {X : C} → P.LimitOfShape J X → CategoryTheory.Functor J (CategoryTheory.StructuredArrow X P.ι)
-- Init.Data.Iterators.Basic
Std.IterStep.successor.eq_2 : ∀ {α : Type u} {β : Type w} (it : α), (Std.IterStep.skip it).successor = some it
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
AddSubgroup.isAddCyclic : ∀ {α : Type u_1} [inst : AddGroup α] [IsAddCyclic α] (H : AddSubgroup α), IsAddCyclic ↥H
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mapRightEq_hom_app_left : ∀ {B : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} B] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T)
  {R₁ R₂ : CategoryTheory.Functor B T} (r r' : R₂ ⟶ R₁) (h : r = r') (X : CategoryTheory.Comma L R₂),
  ((CategoryTheory.Comma.mapRightEq L r r' h).hom.app X).left = CategoryTheory.CategoryStruct.id X.left
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
Matrix.conjTranspose_natCast_smul : ∀ {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid α]
  [inst_2 : StarAddMonoid α] [inst_3 : Module R α] (c : ℕ) (M : Matrix m n α),
  (↑c • M).conjTranspose = ↑c • M.conjTranspose
-- Mathlib.CategoryTheory.SmallObject.TransfiniteIteration
CategoryTheory.SmallObject.SuccStruct.iterationCocone_pt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (Φ : CategoryTheory.SmallObject.SuccStruct C) (J : Type w)
  [inst_1 : LinearOrder J] [inst_2 : OrderBot J] [inst_3 : SuccOrder J] [inst_4 : WellFoundedLT J]
  [inst_5 : CategoryTheory.Limits.HasIterationOfShape J C], (Φ.iterationCocone J).pt = Φ.iteration J
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mathlib.Tactic.MonTauto.rightUnitor_neg_tensor_zero_add : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {M X₁ : C}
  [inst_2 : CategoryTheory.AddMonObj M] (f : X₁ ⟶ M),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor X₁).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.tensorHom f CategoryTheory.AddMonObj.zero)
        CategoryTheory.AddMonObj.add) =
    f
-- Mathlib.Algebra.Order.BigOperators.GroupWithZero.Multiset
Multiset.prod_map_le_prod_map₀ : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] [inst_1 : PartialOrder R] [ZeroLEOneClass R] [PosMulMono R]
  {ι : Type u_2} {s : Multiset ι} (f g : ι → R),
  (∀ i ∈ s, 0 ≤ f i) → (∀ i ∈ s, f i ≤ g i) → (Multiset.map f s).prod ≤ (Multiset.map g s).prod
-- Lean.Meta.Coe
/-- Tags declarations to be unfolded during coercion elaboration.

This is mostly used to hide coercion implementation details and show the coerced result instead of
an application of auxiliary definitions (e.g. `CoeT.coe`, `Coe.coe`). This attribute only works on
reducible functions and instance projections.
 -/
Lean.Meta.coeDeclAttr : Lean.TagAttribute
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.GenericFormat.DateBuilder.X : Std.Time.GenericFormat.DateBuilder✝ → Option Std.Time.TimeZone.Offset
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits
/-- Given `F : J ⥤ PresheafOfModules.{v} R`, this is the presheaf of modules obtained by
taking a limit in the category of modules over `R.obj X` for all `X`.  -/
PresheafOfModules.limitPresheafOfModules : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {R : CategoryTheory.Functor Cᵒᵖ RingCat} →
      {J : Type u₂} →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} J] →
          (F : CategoryTheory.Functor J (PresheafOfModules R)) →
            [∀ (X : Cᵒᵖ),
                  Small.{v, max u₂ v}
                    ↑((F.comp (PresheafOfModules.evaluation R X)).comp
                          (CategoryTheory.forget (ModuleCat ↑(R.obj X)))).sections] →
              PresheafOfModules R
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
eqOn_of_cfcₙ_eq_cfcₙ : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : Nontrivial R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R] [inst_6 : NonUnitalRing A]
  [inst_7 : StarRing A] [inst_8 : TopologicalSpace A] [inst_9 : Module R A] [inst_10 : IsScalarTower R A A]
  [inst_11 : SMulCommClass R A A] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p] {f g : R → R} {a : A},
  cfcₙ f a = cfcₙ g a →
    autoParam (p a) eqOn_of_cfcₙ_eq_cfcₙ._auto_1 →
      autoParam (ContinuousOn f (quasispectrum R a)) eqOn_of_cfcₙ_eq_cfcₙ._auto_3 →
        autoParam (f 0 = 0) eqOn_of_cfcₙ_eq_cfcₙ._auto_5 →
          autoParam (ContinuousOn g (quasispectrum R a)) eqOn_of_cfcₙ_eq_cfcₙ._auto_7 →
            autoParam (g 0 = 0) eqOn_of_cfcₙ_eq_cfcₙ._auto_9 → Set.EqOn f g (quasispectrum R a)
-- Lean.Meta.Tactic.Ext
Lean.Meta.Ext.instHashableExtTheorem : Hashable Lean.Meta.Ext.ExtTheorem
-- Mathlib.Algebra.Category.Ring.Basic
SemiRingCat.hom_id : ∀ {R : SemiRingCat}, SemiRingCat.Hom.hom (CategoryTheory.CategoryStruct.id R) = RingHom.id ↑R
-- Mathlib.CategoryTheory.Adjunction.Reflective
CategoryTheory.Coreflective.toFaithful : ∀ {C : Type u₁} {D : Type u₂} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {L : CategoryTheory.Functor C D} [self : CategoryTheory.Coreflective L], L.Faithful
-- Init.Data.SInt.Lemmas
Int64.toBitVec_div : ∀ {a b : Int64}, (a / b).toBitVec = a.toBitVec.sdiv b.toBitVec
-- Mathlib.Algebra.Order.Ring.Synonym
ofDual_natCast : ∀ {R : Type u_1} [inst : NatCast R] (n : ℕ), OrderDual.ofDual ↑n = ↑n
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.C_eq_one_iff : ∀ {R : Type u_1} {a b : R} [inst : Zero R] [inst_1 : One R] {r : R}, QuadraticAlgebra.C r = 1 ↔ r = 1
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.δ_comp_σ_of_gt' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ}
  {i : Fin (n + 3)} {j : Fin (n + 2)} (H : j.succ < i),
  CategoryTheory.CategoryStruct.comp (X.σ j) (X.δ i) =
    CategoryTheory.CategoryStruct.comp (X.δ (i.pred ⋯)) (X.σ (j.castLT ⋯))
-- Mathlib.FieldTheory.Extension
/-- The domain of a lift.  -/
IntermediateField.Lifts.carrier : {F : Type u_1} →
  {E : Type u_2} →
    {K : Type u_3} →
      [inst : Field F] →
        [inst_1 : Field E] →
          [inst_2 : Field K] →
            [inst_3 : Algebra F E] → [inst_4 : Algebra F K] → IntermediateField.Lifts F E K → IntermediateField F E
-- Mathlib.Order.Filter.Bases.Basic
Filter.HasBasis.sup_principal : ∀ {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α},
  l.HasBasis p s → ∀ (t : Set α), (l ⊔ Filter.principal t).HasBasis p fun i => s i ∪ t
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.map_iInf_comap_of_surjective : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective σ₁₂] {f : M →ₛₗ[σ₁₂] M₂},
  Function.Surjective ⇑f →
    ∀ {ι : Sort u_9} (S : ι → Submodule R₂ M₂), Submodule.map f (⨅ i, Submodule.comap f (S i)) = iInf S
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
/-- The obvious map `PushoutCocone f.op g.op → PullbackCone f g`  -/
CategoryTheory.Limits.PushoutCocone.op : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y Z : C} →
      {f : X ⟶ Y} → {g : X ⟶ Z} → CategoryTheory.Limits.PushoutCocone f g → CategoryTheory.Limits.PullbackCone f.op g.op
-- Lean.Level
Lean.instInhabitedLevel.default : Lean.Level
-- Mathlib.Topology.MetricSpace.Cover
/-- **Alias** of the reverse direction of `Metric.isCover_closure`. -/
Metric.IsCover.closure : ∀ {X : Type u_1} [inst : PseudoMetricSpace X] {ε : NNReal} {s N : Set X} [ProperSpace X],
  IsClosed N → Metric.IsCover ε s N → Metric.IsCover ε (closure s) N
-- Mathlib.Data.Set.Function
Set.EqOn.mono : ∀ {α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α} {f₁ f₂ : α → β}, s₁ ⊆ s₂ → Set.EqOn f₁ f₂ s₂ → Set.EqOn f₁ f₂ s₁
-- Mathlib.LinearAlgebra.Matrix.Rank
Matrix.rank_le_card_width : ∀ {m : Type um} {n : Type un} {R : Type uR} [inst : Fintype n] [inst_1 : CommSemiring R] [StrongRankCondition R]
  (A : Matrix m n R), A.rank ≤ Fintype.card n
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.Fork.ofι_π_app : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} {P : C} (ι : P ⟶ X)
  (w : CategoryTheory.CategoryStruct.comp ι f = CategoryTheory.CategoryStruct.comp ι g)
  (X_1 : CategoryTheory.Limits.WalkingParallelPair),
  (CategoryTheory.Limits.Fork.ofι ι w).π.app X_1 =
    CategoryTheory.Limits.WalkingParallelPair.casesOn (motive := fun t =>
      X_1 = t →
        (((CategoryTheory.Functor.const CategoryTheory.Limits.WalkingParallelPair).obj P).obj X_1 ⟶
          (CategoryTheory.Limits.parallelPair f g).obj X_1))
      X_1 (fun h => ⋯ ▸ ι) (fun h => ⋯ ▸ CategoryTheory.CategoryStruct.comp ι f) ⋯
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.Internal.List.interSmallerFn.match_1.eq_2 : ∀ {α : Type u_2} {β : α → Type u_1} (motive : Option ((a : α) × β a) → Sort u_3)
  (h_1 : (kv' : (a : α) × β a) → motive (some kv')) (h_2 : Unit → motive none),
  (match none with
    | some kv' => h_1 kv'
    | none => h_2 ()) =
    h_2 ()
-- Lean.Elab.Command
/-- Whether any traces were present after expansion.  -/
Lean.Elab.Command.MacroExpandedSnapshot.hasTraces : Lean.Elab.Command.MacroExpandedSnapshot → Bool
-- Mathlib.LinearAlgebra.Eigenspace.Basic
/-- Generalized eigenvalues are actually just eigenvalues.  -/
Module.End.hasGenEigenvalue_iff_hasEigenvalue : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {f : Module.End R M}
  {μ : R} {k : ℕ}, 0 < k → (f.HasGenEigenvalue μ k ↔ f.HasEigenvalue μ)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
NumberField.mixedEmbedding.det_fderivPolarCoordRealSymm : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] (x : NumberField.mixedEmbedding.realMixedSpace K),
  (NumberField.mixedEmbedding.FDerivPolarCoordRealSymm K x).det = ∏ w, (x.2 w).1
-- Mathlib.Tactic.Ring.RingNF
/-- Sum-of-products form, like `x + x * y * 2 + z ^ 2`.  -/
Mathlib.Tactic.RingNF.RingMode.SOP : Mathlib.Tactic.RingNF.RingMode
-- Mathlib.Data.Finset.Fold
Finset.fold_singleton : ∀ {α : Type u_1} {β : Type u_2} {op : β → β → β} [hc : Std.Commutative op] [ha : Std.Associative op] {f : α → β} {b : β}
  {a : α}, Finset.fold op b f {a} = op (f a) b
-- Mathlib.Algebra.Free
FreeMagma.brecOn.eq : ∀ {α : Type u} {motive : FreeMagma α → Sort u_1} (t : FreeMagma α)
  (F_1 : (t : FreeMagma α) → FreeMagma.below t → motive t), FreeMagma.brecOn t F_1 = F_1 t (FreeMagma.brecOn.go t F_1).2
-- Mathlib.Topology.Order.IntermediateValue
/-- **Intermediate Value Theorem** for continuous functions on closed intervals, unordered case.  -/
intermediate_value_uIcc : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {δ : Type u_1} [inst_4 : LinearOrder δ] [inst_5 : TopologicalSpace δ] [OrderClosedTopology δ]
  {a b : α} {f : α → δ}, ContinuousOn f (Set.uIcc a b) → Set.uIcc (f a) (f b) ⊆ f '' Set.uIcc a b
-- Std.Http.Test.Helpers
Std.Http.Internal.Test.r413 : String
-- Init.Data.Nat.Basic
_private.Init.Data.Nat.Basic.0.Nat.repeatTR.loop.eq_def : ∀ {α : Type u} (f : α → α) (x : ℕ) (x_1 : α),
  Nat.repeatTR.loop✝ f x x_1 =
    match x, x_1 with
    | 0, a => a
    | n.succ, a => Nat.repeatTR.loop✝ f n (f a)
-- Init.Data.String.Basic
String.Slice.endExclusive_sliceFrom : ∀ {s : String.Slice} {pos : s.Pos}, (s.sliceFrom pos).endExclusive = s.endExclusive
-- Mathlib.Order.RelSeries
RelSeries.toList_injective : ∀ {α : Type u_1} {r : SetRel α α}, Function.Injective RelSeries.toList
-- Mathlib.RingTheory.Congruence.Opposite
RingCon.opOrderIso_apply : ∀ {R : Type u_1} [inst : Add R] [inst_1 : Mul R] (c : RingCon R), RingCon.opOrderIso c = c.op
-- Init.Grind.Lemmas
Lean.Grind.Nat.shiftRight_congr : ∀ {a b k₁ k₂ k : ℕ}, a = k₁ → b = k₂ → (k == k₁ >>> k₂) = true → a >>> b = k