mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
CategoryTheory.Functor.inr_biprodComparison' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (F : CategoryTheory.Functor C D) (X Y : C) [inst_4 : CategoryTheory.Limits.HasBinaryBiproduct X Y]
  [inst_5 : CategoryTheory.Limits.HasBinaryBiproduct (F.obj X) (F.obj Y)],
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr (F.biprodComparison' X Y) =
    F.map CategoryTheory.Limits.biprod.inr
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.Measure.pi_caratheodory : ∀ {ι : Type u_1} {α : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → MeasurableSpace (α i)]
  (μ : (i : ι) → MeasureTheory.Measure (α i)),
  MeasurableSpace.pi ≤ (MeasureTheory.OuterMeasure.pi fun i => (μ i).toOuterMeasure).caratheodory
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.NewRawFact.generation : Lean.Meta.Grind.NewRawFact → ℕ
-- Std.Time.Date.Unit.Weekday
_private.Std.Time.Date.Unit.Weekday.0.Std.Time.instReprWeekday.repr.match_1.splitter : (motive : Std.Time.Weekday → Sort u_1) →
  (x : Std.Time.Weekday) →
    (Unit → motive Std.Time.Weekday.monday) →
      (Unit → motive Std.Time.Weekday.tuesday) →
        (Unit → motive Std.Time.Weekday.wednesday) →
          (Unit → motive Std.Time.Weekday.thursday) →
            (Unit → motive Std.Time.Weekday.friday) →
              (Unit → motive Std.Time.Weekday.saturday) → (Unit → motive Std.Time.Weekday.sunday) → motive x
-- Aesop.Script.GoalWithMVars
Aesop.GoalWithMVars.mk.sizeOf_spec : ∀ (goal : Lean.MVarId) (mvars : Std.HashSet Lean.MVarId),
  sizeOf { goal := goal, mvars := mvars } = 1 + sizeOf goal + sizeOf mvars
-- Mathlib.Topology.Algebra.Order.Group
continuous_mabs : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : CommGroup G] [inst_2 : LinearOrder G] [IsOrderedMonoid G]
  [OrderTopology G], Continuous mabs
-- Batteries.Lean.Meta.Simp
/-- Construct the `Expr` `cast h e`, from a `Simp.Result` with proof `h`.  -/
Lean.Meta.Simp.mkCast : Lean.Meta.Simp.Result → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.CategoryTheory.Localization.HomEquiv
CategoryTheory.Localization.homEquiv_comp : ∀ {C : Type u_1} {D₁ : Type u_5} {D₂ : Type u_6} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_5, u_5} D₁] [inst_2 : CategoryTheory.Category.{v_6, u_6} D₂]
  (W : CategoryTheory.MorphismProperty C) (L₁ : CategoryTheory.Functor C D₁) [inst_3 : L₁.IsLocalization W]
  (L₂ : CategoryTheory.Functor C D₂) [inst_4 : L₂.IsLocalization W] {X Y Z : C} (f : L₁.obj X ⟶ L₁.obj Y)
  (g : L₁.obj Y ⟶ L₁.obj Z),
  (CategoryTheory.Localization.homEquiv W L₁ L₂) (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Localization.homEquiv W L₁ L₂) f)
      ((CategoryTheory.Localization.homEquiv W L₁ L₂) g)
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.centralizer_le : ∀ (R : Type u) {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (s t : Set A),
  s ⊆ t → Subalgebra.centralizer R t ≤ Subalgebra.centralizer R s
-- Mathlib.GroupTheory.Index
/-- A finite index subgroup has finite quotient.  -/
Subgroup.fintypeQuotientOfFiniteIndex : {G : Type u_1} → [inst : Group G] → {H : Subgroup G} → [H.FiniteIndex] → Fintype (G ⧸ H)
-- Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
CategoryTheory.Precoverage.ZeroHypercover.singleton.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S T : C} (f f_1 : S ⟶ T)
  (e_f : f = f_1) (hf : CategoryTheory.Presieve.singleton f ∈ J.coverings T),
  CategoryTheory.Precoverage.ZeroHypercover.singleton f hf = CategoryTheory.Precoverage.ZeroHypercover.singleton f_1 ⋯
-- Init.Data.SInt.Lemmas
Int32.toInt_sub_of_le : ∀ (a b : Int32), 0 ≤ b → b ≤ a → (a - b).toInt = a.toInt - b.toInt
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.InfinitePlace.even_finrank_of_not_isUnramified : ∀ {k : Type u_1} [inst : Field k] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra k K]
  {w : NumberField.InfinitePlace K} [IsGalois k K],
  ¬NumberField.InfinitePlace.IsUnramified k w → Even (Module.finrank k K)
-- Init.Data.Int.Order
Int.add_le_add_left : ∀ {a b : ℤ}, a ≤ b → ∀ (c : ℤ), c + a ≤ c + b
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Adjunction.AlgCoalgEquiv.unitIso_inv_app_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C C} (adj : F ⊣ G)
  (X : CategoryTheory.Endofunctor.Algebra F),
  ((CategoryTheory.Endofunctor.Adjunction.AlgCoalgEquiv.unitIso adj).inv.app X).f = CategoryTheory.CategoryStruct.id X.a
-- Mathlib.Topology.Instances.Rat
NNRat.nndist_eq : ∀ (p q : ℚ≥0), nndist p q = nndist ↑p ↑q
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.SavedState.grind : Lean.Meta.Grind.SavedState → Lean.Meta.Grind.State
-- Mathlib.Data.Real.ConjExponents
ENNReal.holderConjugate_coe_iff : ∀ {p q : NNReal}, (↑p).HolderConjugate ↑q ↔ p.HolderConjugate q
-- Mathlib.Algebra.Module.CharacterModule
CharacterModule.eq_zero_of_ofSpanSingleton_apply_self : ∀ {A : Type uA} [inst : AddCommGroup A] (a : A), (CharacterModule.ofSpanSingleton a) ⟨a, ⋯⟩ = 0 → a = 0
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.instAddMonoid : {α : Type u} →
  {R : Type u_2} →
    [inst : TopologicalSpace α] →
      [inst_1 : PseudoMetricSpace R] →
        [inst_2 : AddMonoid R] → [BoundedAdd R] → [ContinuousAdd R] → AddMonoid (BoundedContinuousFunction α R)
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.image_const_mul_uIcc : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] (a b c : α),
  (fun x => a * x) '' Set.uIcc b c = Set.uIcc (a * b) (a * c)
-- Mathlib.Testing.Plausible.Functions
Plausible.Injective.testable : {α : Type u} →
  {β : Type v} →
    (f : α → β) →
      [I :
          Plausible.Testable
            (Plausible.NamedBinder "x"
              (∀ (x : α), Plausible.NamedBinder "y" (∀ (y : α), Plausible.NamedBinder "H" (f x = f y → x = y))))] →
        Plausible.Testable (Function.Injective f)
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Arrow.homMk.congr_simp : ∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] {f g : CategoryTheory.Arrow T} (u u_1 : f.left ⟶ g.left)
  (e_u : u = u_1) (v v_1 : f.right ⟶ g.right) (e_v : v = v_1)
  (w : CategoryTheory.CategoryStruct.comp u g.hom = CategoryTheory.CategoryStruct.comp f.hom v),
  CategoryTheory.Arrow.homMk u v w = CategoryTheory.Arrow.homMk u_1 v_1 ⋯
-- Mathlib.LinearAlgebra.Matrix.Hermitian
Matrix.isHermitian_add_transpose_self : ∀ {α : Type u_1} {n : Type u_4} [inst : AddCommMonoid α] [inst_1 : StarAddMonoid α] (A : Matrix n n α),
  (A + A.conjTranspose).IsHermitian
-- Mathlib.Tactic.Basic
/-- `introv` introduces the parameters to a dependent function according to their parameter name. If the
first parameter is not depended on by the rest of the function type, `introv` with no (remaining)
arguments does nothing.

* `introv h₁ h₂ ...` introduces non-depended-on parameters in between sequences of depended-on
  parameters, using the names `h₁`, `h₂`, ... in turn. Use `_` to anonymize a specific hypothesis.

Examples:
```
example : ∀ a b : Nat, a = b → b = a := by
  introv h
  /-
  The goal state is:
  a b : ℕ,
  h : a = b
  ⊢ b = a
  -/
  exact h.symm
```

```
example : ∀ a b : Nat, a = b → ∀ c, b = c → a = c := by
  introv h₁ h₂
  /-
  The goal state is:
  a b : ℕ,
  h₁ : a = b,
  c : ℕ,
  h₂ : b = c
  ⊢ a = c
  -/
  exact h₁.trans h₂
```
 -/
Mathlib.Tactic.introv : Lean.ParserDescr
-- Mathlib.CategoryTheory.Limits.VanKampen
/-- Pullbacks distribute over universal coproducts on the left: This is the isomorphism
`∐ (B ×[S] Xᵢ) ≅ B ×[S] (∐ Xᵢ)`.  -/
CategoryTheory.IsUniversalColimit.isPullback_of_isColimit_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type u_3} {S B : C} {X : ι → C}
  {a : CategoryTheory.Limits.Cofan X},
  CategoryTheory.IsUniversalColimit a →
    ∀ (f : (i : ι) → X i ⟶ S) (u : a.pt ⟶ S) (v : B ⟶ S) {P : ι → C} (q₁ : (i : ι) → P i ⟶ B)
      (q₂ : (i : ι) → P i ⟶ X i),
      (∀ (i : ι), CategoryTheory.IsPullback (q₁ i) (q₂ i) v (f i)) →
        ∀ {d : CategoryTheory.Limits.Cofan P} (hd : CategoryTheory.Limits.IsColimit d),
          autoParam (∀ (i : ι), CategoryTheory.CategoryStruct.comp (a.inj i) u = f i)
              CategoryTheory.IsUniversalColimit.isPullback_of_isColimit_left._auto_1 →
            ∀ [CategoryTheory.Limits.HasPullback v u],
              CategoryTheory.IsPullback (CategoryTheory.Limits.Cofan.IsColimit.desc hd q₁)
                (CategoryTheory.Limits.Cofan.IsColimit.desc hd fun x =>
                  CategoryTheory.CategoryStruct.comp (q₂ x) (a.inj x))
                v u
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot_symm_mk_mk : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) (f p : Polynomial R),
  (AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot I f).symm
      ((Ideal.Quotient.mk (Ideal.span {Polynomial.map (Ideal.Quotient.mk I) f}))
        (Polynomial.map (Ideal.Quotient.mk I) p)) =
    (Ideal.Quotient.mk (Ideal.map (AdjoinRoot.of f) I)) ((AdjoinRoot.mk f) p)
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_basicOpen' : ∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U)
  (f : ↑(X.presheaf.obj (Opposite.op U))),
  (TopologicalSpace.Opens.map hU.fromSpec.base).obj (X.basicOpen f) =
    (AlgebraicGeometry.Spec (X.presheaf.obj (Opposite.op U))).basicOpen
      ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.ΓSpecIso (X.presheaf.obj (Opposite.op U))).inv) f)
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
/-- A series of non-negative real numbers converges to `r` in the sense of `HasSum` if and only if
the sequence of partial sum converges to `r`.  -/
hasSum_iff_tendsto_nat_of_nonneg : ∀ {f : ℕ → ℝ},
  (∀ (i : ℕ), 0 ≤ f i) →
    ∀ (r : ℝ), HasSum f r ↔ Filter.Tendsto (fun n => ∑ i ∈ Finset.range n, f i) Filter.atTop (nhds r)
-- Mathlib.Analysis.BoxIntegral.Partition.Filter
BoxIntegral.IntegrationParams.exists_memBaseSet_le_iUnion_eq : ∀ {ι : Type u_1} [inst : Fintype ι] {I : BoxIntegral.Box ι} {c : NNReal} (l : BoxIntegral.IntegrationParams)
  (π₀ : BoxIntegral.Prepartition I),
  π₀.distortion ≤ c →
    π₀.compl.distortion ≤ c →
      ∀ (r : (ι → ℝ) → ↑(Set.Ioi 0)), ∃ π, l.MemBaseSet I c r π ∧ π.toPrepartition ≤ π₀ ∧ π.iUnion = π₀.iUnion
-- Init.Data.Vector.Zip
Vector.unzip_snd : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {xs : Vector (α × β) n}, xs.unzip.2 = Vector.map Prod.snd xs
-- Lean.Level
Lean.Level.hasMVarEx : Lean.Level → Bool
-- Init.Data.List.MinMaxOn
List.maxOn_cons_cons : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] {a b : α} {l : List α} {f : α → β},
  List.maxOn f (a :: b :: l) ⋯ = List.maxOn f (maxOn f a b :: l) ⋯
-- Mathlib.RingTheory.WittVector.Basic
_private.Mathlib.RingTheory.WittVector.Basic.0.Int.castDef.match_1.splitter : (motive : ℤ → Sort u_1) → (x : ℤ) → ((n : ℕ) → motive (Int.ofNat n)) → ((n : ℕ) → motive (Int.negSucc n)) → motive x
-- Mathlib.RepresentationTheory.Continuous.Basic
instMonoidHomClassContRepresentationContinuousLinearMapId : ∀ (R : Type u_1) (G : Type u_2) (V : Type u_3) [inst : Monoid G] [inst_1 : Ring R] [inst_2 : AddCommGroup V]
  [inst_3 : TopologicalSpace V] [inst_4 : IsTopologicalAddGroup V] [inst_5 : Module R V],
  MonoidHomClass (ContRepresentation R G V) G (V →L[R] V)
-- Mathlib.Data.TypeVec
/-- cases on `(n+1)-length` vectors  -/
TypeVec.append1Cases : {n : ℕ} →
  {C : TypeVec.{u_1} (n + 1) → Sort u} →
    ((α : TypeVec.{u_1} n) → (β : Type u_1) → C (α ::: β)) → (γ : TypeVec.{u_1} (n + 1)) → C γ
-- Mathlib.Tactic.Explode.Datatypes
Mathlib.Explode.instInhabitedEntries.default : Mathlib.Explode.Entries
-- Mathlib.Order.Filter.Pointwise
Filter.NeBot.nonneg_sub : ∀ {α : Type u_2} [inst : AddGroup α] {f : Filter α}, f.NeBot → 0 ≤ f - f
-- Lean.ResolveName
/-- Interprets the syntax `n` as an identifier for a global constant, and returns a list of resolved
constant names that it could be referring to based on the currently open namespaces.
This should be used instead of `resolveGlobalConstCore` for identifiers taken from syntax
because `Syntax` objects may have names that have already been resolved.

Consider using `realizeGlobalConst` if you need to handle reserved names, and
`realizeGlobalConstWithInfo` if you want the syntax to show the resulting name's info on hover.

## Example:
```
def Boo.x   := 1
def Foo.x   := 2
def Foo.x.y := 3
```
After `open Foo`, we have
- `resolveGlobalConst x`     => `[Foo.x]`
- `resolveGlobalConst x.y`   => `[Foo.x.y]`
- `resolveGlobalConst x.z.w` => error: unknown constant

After `open Foo open Boo`, we have
- `resolveGlobalConst x`     => `[Foo.x, Boo.x]`
- `resolveGlobalConst x.y`   => `[Foo.x.y]`
- `resolveGlobalConst x.z.w` => error: unknown constant
 -/
Lean.resolveGlobalConst : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadResolveName m] →
      [Lean.MonadEnv m] →
        [Lean.MonadOptions m] →
          [Lean.MonadLog m] → [Lean.AddMessageContext m] → [Lean.MonadError m] → Lean.Syntax → m (List Lean.Name)
-- Mathlib.Tactic.CategoryTheory.CheckCompositions
/-- Check the typing of categorical compositions in the goal.  -/
Mathlib.Tactic.CheckCompositions.checkCompositionsTac : Lean.Elab.Tactic.TacticM Unit
-- Mathlib.Algebra.Homology.Factorizations.CM5a
/-- Assuming `f : K ⟶ L` is a monomorphism between complexes that are strictly `≥ n₀ + 1`,
this is a dependent sequence of terms in `CofFibFactorizationQuasiIsoLE f (n₀ + q)`
for all `q : ℕ`.  -/
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.CofFibFactorizationQuasiIsoLE.sequence : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {K L : CochainComplex C ℤ} →
        (f : K ⟶ L) →
          [CategoryTheory.EnoughInjectives C] →
            [CategoryTheory.Mono f] →
              (n₀ : ℤ) →
                [K.IsStrictlyGE (n₀ + 1)] →
                  [L.IsStrictlyGE (n₀ + 1)] →
                    (q : ℕ) →
                      CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.CofFibFactorizationQuasiIsoLE✝ f (n₀ + ↑q)
-- Mathlib.Algebra.GCDMonoid.Basic
gcd_one_right : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] (a : α), gcd a 1 = 1
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.mapIso_inverse_obj_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S S' : D} {T : CategoryTheory.Functor C D} (i : S ≅ S')
  (X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit S') T),
  ((CategoryTheory.StructuredArrow.mapIso i).inverse.obj X).right = X.right
-- Mathlib.CategoryTheory.Monoidal.Category
/-- The associator isomorphism `(X ⊗ Y) ⊗ Z ≃ X ⊗ (Y ⊗ Z)`  -/
CategoryTheory.MonoidalCategoryStruct.associator : {C : Type u} →
  {𝒞 : CategoryTheory.Category.{v, u} C} →
    [self : CategoryTheory.MonoidalCategoryStruct C] →
      (X Y Z : C) →
        CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z ≅
          CategoryTheory.MonoidalCategoryStruct.tensorObj X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
/-- Bicoloring of a cycle graph of even size  -/
SimpleGraph.cycleGraph.bicoloring_of_even : (n : ℕ) → Even n → (SimpleGraph.cycleGraph n).Coloring Bool
-- Mathlib.RingTheory.Extension.Presentation.Core
Algebra.Presentation.HasCoeffs.mk : ∀ {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] {P : Algebra.Presentation R S ι σ} {R₀ : Type u_5} [inst_3 : CommRing R₀]
  [inst_4 : Algebra R₀ R] [inst_5 : Algebra R₀ S] [inst_6 : IsScalarTower R₀ R S],
  P.coeffs ⊆ Set.range ⇑(algebraMap R₀ R) → P.HasCoeffs R₀
-- Mathlib.Data.Multiset.Powerset
/-- Helper function for the powerset of a multiset. Given a list `l`, returns a list
of sublists of `l` (using `sublists'`), as multisets.  -/
Multiset.powersetAux' : {α : Type u_1} → List α → List (Multiset α)
-- Lean.Elab.Tactic.RCases
Lean.Elab.Tactic.RCases.RCasesPatt.typed.sizeOf_spec : ∀ (ref : Lean.Syntax) (a : Lean.Elab.Tactic.RCases.RCasesPatt) (a_1 : Lean.Term),
  sizeOf (Lean.Elab.Tactic.RCases.RCasesPatt.typed ref a a_1) = 1 + sizeOf ref + sizeOf a + sizeOf a_1
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.sum_surjective : ∀ {α : Type u} [inst : AddGroup α], Function.Surjective ⇑FreeAddGroup.sum
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instBEqInsertReplaceEdit : BEq Lean.Lsp.InsertReplaceEdit
-- Init.Grind.AC
Lean.Grind.AC.Seq.sort : Lean.Grind.AC.Seq → Lean.Grind.AC.Seq
-- Mathlib.CategoryTheory.Category.TwoP
/-- The equivalence between `TwoP` and itself induced by `Prod.swap` both ways.  -/
TwoP.swapEquiv : TwoP ≌ TwoP
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
/-- See `summable_congr_cofinite` for a version allowing the functions to
disagree on a finite set.  -/
summable_congr : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f g : β → α}
  {L : SummationFilter β}, (∀ (b : β), f b = g b) → (Summable f L ↔ Summable g L)
-- Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
PrimeSpectrum.BasicConstructibleSetData.mk.inj : ∀ {R : Type u_1} {f : R} {n : ℕ} {g : Fin n → R} {f_1 : R} {n_1 : ℕ} {g_1 : Fin n_1 → R},
  { f := f, n := n, g := g } = { f := f_1, n := n_1, g := g_1 } → f = f_1 ∧ n = n_1 ∧ g ≍ g_1
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.append_copy_copy : ∀ {V : Type u} {G : SimpleGraph V} {u v w u' v' w' : V} (p : G.Walk u v) (q : G.Walk v w) (hu : u = u') (hv : v = v')
  (hw : w = w'), (p.copy hu hv).append (q.copy hv hw) = (p.append q).copy hu hw
-- Mathlib.Order.Interval.Finset.Fin
Fin.finsetImage_castAdd_Iic : ∀ {n : ℕ} (m : ℕ) (i : Fin n), Finset.image (Fin.castAdd m) (Finset.Iic i) = Finset.Iic (Fin.castAdd m i)
-- Mathlib.Data.Fin.Fin2
/-- Maps `0` to `n-1`, `1` to `n-2`, ..., `n-1` to `0`.  -/
Fin2.rev : {n : ℕ} → Fin2 n → Fin2 n
-- Mathlib.Algebra.Order.Ring.Ordering.Defs
RingPreordering.mk.sizeOf_spec : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : SizeOf R] (toSubsemiring : Subsemiring R)
  (mem_of_isSquare' :
    autoParam (∀ {x : R}, IsSquare x → x ∈ toSubsemiring.carrier) RingPreordering.mem_of_isSquare'._autoParam)
  (neg_one_notMem' : autoParam (-1 ∉ toSubsemiring.carrier) RingPreordering.neg_one_notMem'._autoParam),
  sizeOf { toSubsemiring := toSubsemiring, mem_of_isSquare' := mem_of_isSquare', neg_one_notMem' := neg_one_notMem' } =
    1 + sizeOf toSubsemiring
-- Mathlib.FieldTheory.RatFunc.Defs
/-- Non-dependent recursion principle for `K⟮X⟯`:
To construct a term of `P : Sort*` out of `x : K⟮X⟯`,
it suffices to provide a constructor `f : Π (p q : K[X]), P`
and a proof that `f p q = f p' q'` for all `p q p' q'` such that `q' * p = q * p'` where
both `q` and `q'` are not zero divisors, stated as `q ∉ K[X]⁰`, `q' ∉ K[X]⁰`.

If considering `K` as an integral domain, this is the same as saying that
we construct a value of `P` for such elements of `K⟮X⟯` by setting
`liftOn (p / q) f _ = f p q`.

When `[IsDomain K]`, one can use `RatFunc.liftOn'`, which has the stronger requirement
of `∀ {p q a : K[X]} (hq : q ≠ 0) (ha : a ≠ 0), f (a * p) (a * q) = f p q)`.
 -/
RatFunc.liftOn : {K : Type u_1} →
  [inst : CommRing K] →
    {P : Sort u_2} →
      RatFunc K →
        (f : Polynomial K → Polynomial K → P) →
          (∀ {p q p' q' : Polynomial K},
              q ∈ nonZeroDivisors (Polynomial K) →
                q' ∈ nonZeroDivisors (Polynomial K) → q' * p = q * p' → f p q = f p' q') →
            P
-- Mathlib.LinearAlgebra.TensorProduct.Map
TensorProduct.instSmall : ∀ {R : Type u_22} {M : Type u_23} {N : Type u_24} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] [Small.{u, u_23} M] [Small.{u, u_24} N],
  Small.{u, max u_24 u_23} (TensorProduct R M N)
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigOWith.sub : ∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E'] {c₁ c₂ : ℝ}
  {g : α → F} {l : Filter α} {f₁ f₂ : α → E'},
  Asymptotics.IsBigOWith c₁ l f₁ g →
    Asymptotics.IsBigOWith c₂ l f₂ g → Asymptotics.IsBigOWith (c₁ + c₂) l (fun x => f₁ x - f₂ x) g
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.rotateR.eq_2 : ∀ {α : Type u} {β : α → Type v} (k : α) (v : β k) (lk : α) (lv : β lk) (ll r : Std.DTreeMap.Internal.Impl α β) (ls : ℕ)
  (lk_1 : α) (lv_1 : β lk_1) (ll_1 lr_1 : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.rotateR k v lk lv ll (Std.DTreeMap.Internal.Impl.inner ls lk_1 lv_1 ll_1 lr_1) r =
    if (Std.DTreeMap.Internal.Impl.inner ls lk_1 lv_1 ll_1 lr_1).size < Std.DTreeMap.Internal.ratio * ll.size then
      Std.DTreeMap.Internal.Impl.singleR k v lk lv ll (Std.DTreeMap.Internal.Impl.inner ls lk_1 lv_1 ll_1 lr_1) r
    else Std.DTreeMap.Internal.Impl.doubleR k v lk lv ll lk_1 lv_1 ll_1 lr_1 r
-- Mathlib.Probability.Distributions.Beta
/-- Relation between the beta function and the gamma function over the reals.  -/
ProbabilityTheory.beta_eq_betaIntegralReal : ∀ (α β : ℝ), 0 < α → 0 < β → ProbabilityTheory.beta α β = ((↑α).betaIntegral ↑β).re
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Arrow.hom.congr_left : ∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] {f g : CategoryTheory.Arrow T} {φ₁ φ₂ : f ⟶ g},
  φ₁ = φ₂ → CategoryTheory.Arrow.Hom.left φ₁ = CategoryTheory.Arrow.Hom.left φ₂
-- Mathlib.LinearAlgebra.DirectSum.Finsupp
/-- A variant of `finsuppTensorFinsupp` where the second module is the ground ring.  -/
finsuppTensorFinsuppRid : (R : Type u_1) →
  (M : Type u_3) →
    (ι : Type u_5) →
      (κ : Type u_6) →
        [inst : CommSemiring R] →
          [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → TensorProduct R (ι →₀ M) (κ →₀ R) ≃ₗ[R] ι × κ →₀ M
-- Lean.Server.InfoUtils
Lean.Elab.Info.type? : Lean.Elab.Info → Lean.MetaM (Option Lean.Expr)
-- Init.Data.Nat.Lemmas
Nat.not_dvd_of_pos_of_lt : ∀ {n m : ℕ}, 0 < n → n < m → ¬m ∣ n
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
_private.Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer.0.CategoryTheory.Limits.WalkingMulticospan.functorExt.match_1.splitter : {J : CategoryTheory.Limits.MulticospanShape} →
  (motive : CategoryTheory.Limits.WalkingMulticospan J → Sort u_3) →
    (j : CategoryTheory.Limits.WalkingMulticospan J) →
      ((i : J.L) → motive (CategoryTheory.Limits.WalkingMulticospan.left i)) →
        ((i : J.R) → motive (CategoryTheory.Limits.WalkingMulticospan.right i)) → motive j
-- Init.Data.SInt.Basic
/-- Converts an arbitrary-precision integer to a 16-bit integer, wrapping on overflow or underflow.

Examples:
* `Int.toInt16 48 = 48`
* `Int.toInt16 (-129) = -129`
* `Int.toInt16 (128) = 128`
* `Int.toInt16 70000 = 4464`
* `Int.toInt16 (-40000) = 25536`
 -/
Int.toInt16 : ℤ → Int16
-- Mathlib.CategoryTheory.Bicategory.Functor.Lax
/-- Naturality of the lax functoriality constraint, on the right.  -/
CategoryTheory.LaxFunctor.mapComp_naturality_right : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (self : CategoryTheory.LaxFunctor B C) {a b c : B} (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g'),
  CategoryTheory.CategoryStruct.comp (self.mapComp f g) (self.map₂ (CategoryTheory.Bicategory.whiskerLeft f η)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (self.map f) (self.map₂ η))
      (self.mapComp f g')
-- Mathlib.Order.Interval.Set.Image
Set.image_subtype_val_Ioo_Ioi : ∀ {α : Type u_1} [inst : Preorder α] {a b : α} (c : ↑(Set.Ioo a b)), Subtype.val '' Set.Ioi c = Set.Ioo (↑c) b