mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Category.MonCat.Adjunctions
AddMonCat.adj.eq_1 : AddMonCat.adj =
  CategoryTheory.Adjunction.mkOfHomEquiv
    {
      homEquiv := fun X Y =>
        CategoryTheory.ConcreteCategory.homEquiv.trans (FreeAddMonoid.lift.symm.trans TypeCat.homEquiv.symm),
      homEquiv_naturality_left_symm := @AddMonCat.adj._proof_3, homEquiv_naturality_right := @AddMonCat.adj._proof_2 }
-- Mathlib.Geometry.Euclidean.Angle.Incenter
/-- The excenter of a triangle opposite a vertex bisects the exterior angle at another vertex
(that is, the interior angles between vertices and the excenter differ by `π`).  -/
Affine.Triangle.oangle_excenter_singleton_eq_add_pi : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  (t : Affine.Triangle ℝ P) {i₁ i₂ i₃ : Fin 3},
  i₁ ≠ i₂ →
    i₁ ≠ i₃ →
      i₂ ≠ i₃ →
        EuclideanGeometry.oangle (t.points i₁) (t.points i₂) (Affine.Simplex.excenter t {i₁}) =
          EuclideanGeometry.oangle (Affine.Simplex.excenter t {i₁}) (t.points i₂) (t.points i₃) + ↑Real.pi
-- Mathlib.Algebra.Category.Semigrp.Basic
MagmaCat.coe_comp : ∀ {X Y Z : MagmaCat} {f : X ⟶ Y} {g : Y ⟶ Z},
  ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) =
    ⇑(CategoryTheory.ConcreteCategory.hom g) ∘ ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.subsingleton_of_bot : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L],
  Subsingleton (LieSubalgebra R ↥⊥)
-- Init.Data.Array.BinSearch
_private.Init.Data.Array.BinSearch.0.Array.binInsertAux.eq_def : ∀ {α : Type u} {m : Type u → Type v} [inst : Monad m] (lt : α → α → Bool) (merge : α → m α) (add : Unit → m α)
  (as : Array α) (k : α) (x x_1 : Fin as.size) (x_2 : ↑x ≤ ↑x_1) (x_3 : lt as[x] k = true),
  Array.binInsertAux✝ lt merge add as k x x_1 x_2 x_3 =
    match x, x_1, x_2, x_3 with
    | lo, hi, h, w =>
      let mid := (↑lo + ↑hi) / 2;
      let midVal := as[mid];
      if w₁ : lt midVal k = true then
        if h' : mid = ↑lo then do
          let v ← add ()
          pure (as.insertIdx (↑lo + 1) v ⋯)
        else Array.binInsertAux✝ lt merge add as k ⟨mid, ⋯⟩ hi ⋯ w₁
      else
        if w₂ : lt k midVal = true then
          have this := ⋯;
          Array.binInsertAux✝ lt merge add as k lo ⟨mid, ⋯⟩ ⋯ w
        else as.modifyM mid fun v => merge v
-- Mathlib.Condensed.Discrete.LocallyConstant
CompHausLike.LocallyConstant.instIsIsoFunctorTypeUnitSheafCoherentTopologyAdjunction : ∀ (P : TopCat → Prop) [inst : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), CompHausLike.HasProp P (Subtype p)]
  [inst_1 : CompHausLike.HasProp P PUnit.{u + 1}] [inst_2 : CompHausLike.HasExplicitFiniteCoproducts P]
  [inst_3 : CompHausLike.HasExplicitPullbacks P]
  (hs :
    ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y),
      CategoryTheory.EffectiveEpi f → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f))
  [inst_4 : CompHausLike.HasExplicitFiniteCoproducts P],
  CategoryTheory.IsIso (CompHausLike.LocallyConstant.adjunction P hs).unit
-- Mathlib.Data.Sum.Basic
PSum.inr_injective : ∀ {α : Sort u_3} {β : Sort u_4}, Function.Injective PSum.inr
-- Mathlib.Algebra.Order.Archimedean.Basic
archimedean_iff_rat_lt : ∀ {K : Type u_4} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K],
  Archimedean K ↔ ∀ (x : K), ∃ q, x < ↑q
-- Init.Data.List.Basic
List.intersperse.eq_def : ∀ {α : Type u} (sep : α) (x : List α),
  List.intersperse sep x =
    match x with
    | [] => []
    | [x] => [x]
    | x :: xs => x :: sep :: List.intersperse sep xs
-- Mathlib.Combinatorics.SetFamily.HarrisKleitman
IsLowerSet.memberSubfamily_subset_nonMemberSubfamily : ∀ {α : Type u_1} [inst : DecidableEq α] {𝒜 : Finset (Finset α)} {a : α},
  IsLowerSet ↑𝒜 → Finset.memberSubfamily a 𝒜 ⊆ Finset.nonMemberSubfamily a 𝒜
-- Lean.Data.Lsp.Extra
Lean.Lsp.instToJsonModuleHierarchyOptions : Lean.ToJson Lean.Lsp.ModuleHierarchyOptions
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.isoMk.eq_1 : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {L₁ : CategoryTheory.Functor A T}
  {R₁ : CategoryTheory.Functor B T} {X Y : CategoryTheory.Comma L₁ R₁} (l : X.left ≅ Y.left) (r : X.right ≅ Y.right)
  (h :
    CategoryTheory.CategoryStruct.comp (L₁.map l.hom) Y.hom = CategoryTheory.CategoryStruct.comp X.hom (R₁.map r.hom)),
  CategoryTheory.Comma.isoMk l r h =
    { hom := { left := l.hom, right := r.hom, w := h }, inv := { left := l.inv, right := r.inv, w := ⋯ },
      hom_inv_id := ⋯, inv_hom_id := ⋯ }
-- Batteries.Data.List.Basic
List.IsChain.below : {α : Type u_1} →
  {R : α → α → Prop} → {motive : (a : List α) → List.IsChain R a → Prop} → {a : List α} → List.IsChain R a → Prop
-- Std.Data.DHashMap.Raw
_private.Std.Data.DHashMap.Raw.0.Std.DHashMap.Raw.erase.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Raw α β) (a : α),
  m.erase a = if h : 0 < m.buckets.size then ↑(Std.DHashMap.Internal.Raw₀.erase ⟨m, h⟩ a) else m
-- Mathlib.Combinatorics.HalesJewett
/-- The word representing a combinatorial subspace. `l.idxfun i = Sum.inr e` means that
`l x i = x e` for all `x` and `l.idxfun i = some a` means that `l x i = a` for all `x`.  -/
Combinatorics.Subspace.idxFun : {η : Type u_5} → {α : Type u_6} → {ι : Type u_7} → Combinatorics.Subspace η α ι → ι → α ⊕ η
-- Mathlib.LinearAlgebra.Basis.SMul
Module.Basis.smul_apply : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {G : Type u_5} [inst_3 : Group G] [inst_4 : DistribMulAction G M] [inst_5 : SMulCommClass G R M] (g : G)
  (b : Module.Basis ι R M) (i : ι), (g • b) i = g • b i
-- Mathlib.ModelTheory.Types
FirstOrder.Language.Theory.CompleteType.iInter_setOfPred_subset : ∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {ι : Type u_1} (S : ι → (L.withConstants α).Theory),
  ⋂ i, {p | S i ⊆ ↑p} = {p | ⋃ i, S i ⊆ ↑p}
-- Mathlib.Data.PFun
PFun.prodLift_apply : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α →. β) (g : α →. γ) (x : α),
  f.prodLift g x = { Dom := (f x).Dom ∧ (g x).Dom, get := fun h => ((f x).get ⋯, (g x).get ⋯) }
-- Mathlib.LinearAlgebra.Matrix.Defs
/-- The left `n × l` part of an `n × (l+r)` matrix.  -/
Matrix.subLeft : {α : Type v} → {m l r : ℕ} → Matrix (Fin m) (Fin (l + r)) α → Matrix (Fin m) (Fin l) α
-- Mathlib.Algebra.Homology.LeftResolution.Reduced
/-- Auxiliary definition for `LeftResolution.karoubi`.  -/
CategoryTheory.Abelian.LeftResolution.karoubi.π' : {A : Type u_1} →
  {C : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_2} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_1} A] →
        {ι : CategoryTheory.Functor C A} →
          (Λ : CategoryTheory.Abelian.LeftResolution ι) →
            [inst_2 : CategoryTheory.Preadditive C] →
              [inst_3 : CategoryTheory.Preadditive A] →
                [ι.Additive] →
                  (CategoryTheory.Idempotents.toKaroubi A).comp
                      ((CategoryTheory.Abelian.LeftResolution.karoubi.F Λ).comp
                        ((CategoryTheory.Idempotents.functorExtension₂ C A).obj ι)) ⟶
                    CategoryTheory.Idempotents.toKaroubi A
-- Mathlib.Data.ENNReal.Basic
/-- `(1 : ℝ≥0∞) ≤ ∞`, recorded as a `Fact` for use with `Lp` spaces.  -/
fact_one_le_top_ennreal : Fact (1 ≤ ⊤)
-- Std.Tactic.BVDecide.Bitblast.BoolExpr.Basic
Std.Tactic.BVDecide.BoolExpr.ite : {α : Type} →
  Std.Tactic.BVDecide.BoolExpr α →
    Std.Tactic.BVDecide.BoolExpr α → Std.Tactic.BVDecide.BoolExpr α → Std.Tactic.BVDecide.BoolExpr α
-- Mathlib.MeasureTheory.Measure.Regular
/-- If `μ` is inner regular for measurable finite measure sets with respect to some class of sets,
then its restriction to any finite measure set is also inner regular for measurable sets with
respect to the same class of sets.  -/
MeasureTheory.Measure.InnerRegularWRT.restrict_of_measure_ne_top : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {p : Set α → Prop},
  (μ.InnerRegularWRT p fun s => MeasurableSet s ∧ μ s ≠ ⊤) →
    ∀ {A : Set α}, μ A ≠ ⊤ → (μ.restrict A).InnerRegularWRT p fun s => MeasurableSet s
-- Mathlib.Algebra.GroupWithZero.Pointwise.Finset
Finset.card_le_card_mul_left₀ : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : DecidableEq α] {s t : Finset α} {a : α}
  [IsLeftCancelMulZero α], a ∈ s → a ≠ 0 → t.card ≤ (s * t).card
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
SSet.Subcomplex.Pairing.RankFunction.Cell.type₂_dim : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [inst : LinearOrder ι] (f : P.RankFunction ι)
  [inst_1 : P.IsProper] {j : ι} (c : f.Cell j), (SSet.Subcomplex.Pairing.RankFunction.Cell.type₂ f c).dim = c.dim
-- Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
CategoryTheory.Limits.fiberwiseColimit_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C CategoryTheory.Cat}
  {H : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} H]
  (G : CategoryTheory.Functor (CategoryTheory.Grothendieck F) H)
  [inst_2 :
    ∀ {X Y : C} (f : X ⟶ Y),
      CategoryTheory.Limits.HasColimit ((F.map f).toFunctor.comp ((CategoryTheory.Grothendieck.ι F Y).comp G))]
  {X Y : C} (f : X ⟶ Y),
  (CategoryTheory.Limits.fiberwiseColimit G).map f =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.colimMap
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Functor.whiskerRight (CategoryTheory.Grothendieck.ιNatTrans f) G)
          ((F.map f).toFunctor.associator (CategoryTheory.Grothendieck.ι F Y) G).hom))
      (CategoryTheory.Limits.colimit.pre ((CategoryTheory.Grothendieck.ι F Y).comp G) (F.map f).toFunctor)
-- Lean.Elab.InfoTree.Types
Lean.Elab.Info.ofDocInfo.sizeOf_spec : ∀ (i : Lean.Elab.DocInfo), sizeOf (Lean.Elab.Info.ofDocInfo i) = 1 + sizeOf i
-- Mathlib.RingTheory.HahnSeries.Lex
HahnSeries.embDomainOrderEmbedding.eq_1 : ∀ {Γ : Type u_1} {R : Type u_2} [inst : LinearOrder Γ] [inst_1 : PartialOrder R] {Γ' : Type u_3}
  [inst_2 : LinearOrder Γ'] (f : Γ ↪o Γ') [inst_3 : Zero R],
  HahnSeries.embDomainOrderEmbedding f =
    { toFun := fun a => toLex (HahnSeries.embDomain f (ofLex a)), inj' := ⋯, map_rel_iff' := ⋯ }
-- Mathlib.MeasureTheory.Integral.SetToL1
/-- `setToFun` applied to the sum `T + T'` of two operators is the sum of the corresponding
`setToFun`.  -/
MeasureTheory.setToFun_add_left'' : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α}
  {μ μ' μ'' : MeasureTheory.Measure α} {T T' T'' : Set α → E →L[ℝ] F} {C C' C'' : ℝ} {f : α → E}
  {hT : MeasureTheory.DominatedFinMeasAdditive μ T C} {hT' : MeasureTheory.DominatedFinMeasAdditive μ' T' C'}
  {hT'' : MeasureTheory.DominatedFinMeasAdditive μ'' T'' C''},
  (∀ (s : Set α), MeasurableSet s → (μ + μ') s < ⊤ → T'' s = T s + T' s) →
    MeasureTheory.Integrable f μ →
      MeasureTheory.Integrable f μ' →
        μ'' ≤ μ + μ' →
          0 ≤ C →
            0 ≤ C' →
              0 ≤ C'' →
                MeasureTheory.setToFun μ'' T'' hT'' f =
                  MeasureTheory.setToFun μ T hT f + MeasureTheory.setToFun μ' T' hT' f
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey?_beq : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {a : α}, Option.all (fun x => x == a) (m.getKey? a) = true
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.ofRestrict_invApp_apply : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : AlgebraicGeometry.PresheafedSpace C) {Y : TopCat}
  {f : Y ⟶ TopCat.of ↑↑X} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f))
  (U : TopologicalSpace.Opens ↑↑(X.restrict h)) {F : C → C → Type uF} {carrier : C → Type w_1}
  {instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)} [inst_1 : CategoryTheory.ConcreteCategory C F]
  (x : carrier ((X.restrict h).presheaf.obj (Opposite.op U))),
  (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp (X.ofRestrict h) U))
      x =
    (CategoryTheory.ConcreteCategory.hom
        (CategoryTheory.CategoryStruct.id ((X.restrict h).presheaf.obj (Opposite.op U))))
      x
-- Mathlib.Topology.Algebra.Group.Basic
continuous_of_continuousAt_one₂ : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G] {H : Type u_1} {M : Type u_2}
  [inst_3 : CommMonoid M] [inst_4 : TopologicalSpace M] [ContinuousMul M] [inst_6 : Group H]
  [inst_7 : TopologicalSpace H] [IsTopologicalGroup H] (f : G →* H →* M),
  ContinuousAt (fun x => (f x.1) x.2) (1, 1) →
    (∀ (x : G), ContinuousAt (⇑(f x)) 1) →
      (∀ (y : H), ContinuousAt (fun x => (f x) y) 1) → Continuous fun x => (f x.1) x.2
-- Mathlib.NumberTheory.LucasLehmer
LucasLehmer.sZMod_eq_s : ∀ (p' i : ℕ), LucasLehmer.sZMod (p' + 2) i = ↑(LucasLehmer.s i)
-- Mathlib.CategoryTheory.Localization.Monoidal.Basic
CategoryTheory.Localization.Monoidal.leftUnitor_hom_app : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : W.IsMonoidal]
  [inst_4 : L.IsLocalization W] {unit : D} (ε : L.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ unit)
  (Y : C),
  (CategoryTheory.MonoidalCategoryStruct.leftUnitor
        ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Y)).hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Localization.Monoidal.ε' L W ε).inv
        ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Y))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Localization.Monoidal.μ L W ε (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) Y).hom
        ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).map
          (CategoryTheory.MonoidalCategoryStruct.leftUnitor Y).hom))
-- Mathlib.MeasureTheory.Group.FoelnerFilter
IsFoelner.mean_union_eq_add_of_disjoint : ∀ {G : Type u_1} {X : Type u_2} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} [inst_1 : Group G]
  [inst_2 : MulAction G X] {ι : Type u_3} {u : Ultrafilter ι} {F : ι → Set X},
  IsFoelner G μ (↑u) F →
    ∀ (s t : Set X),
      MeasurableSet t → Disjoint s t → IsFoelner.mean μ u F (s ∪ t) = IsFoelner.mean μ u F s + IsFoelner.mean μ u F t
-- Mathlib.Topology.IsLocalHomeomorph
/-- An injective local homeomorphism is an open embedding.  -/
IsLocalHomeomorph.isOpenEmbedding_of_injective : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  IsLocalHomeomorph f → Function.Injective f → Topology.IsOpenEmbedding f
-- Mathlib.Analysis.Convex.Cone.Basic
ProperCone.nonempty : ∀ {R : Type u_2} {E : Type u_3} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommMonoid E] [inst_4 : TopologicalSpace E] [inst_5 : Module R E] (C : ProperCone R E), (↑C).Nonempty
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMonoidHom.toMonoidHom_toContinuousMonoidHom : ∀ {A : Type u_2} {B : Type u_3} [inst : Monoid A] [inst_1 : Monoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B] {F : Type u_7} [inst_4 : FunLike F A B] [inst_5 : MonoidHomClass F A B]
  [inst_6 : ContinuousMapClass F A B] (f : F), ↑↑f = ↑f
-- Mathlib.AlgebraicGeometry.Group.Affine
AlgebraicGeometry.μ_pullback_left_fst : ∀ (R S T : Type u) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
  [inst_4 : Algebra R T],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.Hom.left
        (CategoryTheory.Functor.LaxMonoidal.μ
          (CategoryTheory.Over.pullback (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R S))))
          (CategoryTheory.Over.mk (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R T))))
          (CategoryTheory.Over.mk (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R T))))))
      (CategoryTheory.Limits.pullback.fst
        (CategoryTheory.MonoidalCategoryStruct.tensorObj
            (CategoryTheory.Over.mk (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R T))))
            (CategoryTheory.Over.mk (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R T))))).hom
        (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R S)))) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.Hom.left
        (CategoryTheory.MonoidalCategoryStruct.tensorHom
          (AlgebraicGeometry.Scheme.Hom.asOver
            (CategoryTheory.Limits.pullbackSymmetry
                  (AlgebraicGeometry.Spec (CommRingCat.of T) ↘ AlgebraicGeometry.Spec (CommRingCat.of R))
                  (AlgebraicGeometry.Spec (CommRingCat.of S) ↘ AlgebraicGeometry.Spec (CommRingCat.of R)) ≪≫
                AlgebraicGeometry.pullbackSpecIso' R S T).hom
            (AlgebraicGeometry.Spec (CommRingCat.of S)))
          (AlgebraicGeometry.Scheme.Hom.asOver
            (CategoryTheory.Limits.pullbackSymmetry
                  (AlgebraicGeometry.Spec (CommRingCat.of T) ↘ AlgebraicGeometry.Spec (CommRingCat.of R))
                  (AlgebraicGeometry.Spec (CommRingCat.of S) ↘ AlgebraicGeometry.Spec (CommRingCat.of R)) ≪≫
                AlgebraicGeometry.pullbackSpecIso' R S T).hom
            (AlgebraicGeometry.Spec (CommRingCat.of S)))))
      (CategoryTheory.CategoryStruct.comp
        (AlgebraicGeometry.pullbackSpecIso S (TensorProduct R S T) (TensorProduct R S T)).hom
        (CategoryTheory.CategoryStruct.comp
          (AlgebraicGeometry.Spec.map
            (CommRingCat.ofHom
              (Algebra.TensorProduct.mapRingHom (algebraMap R S) Algebra.TensorProduct.includeRight.toRingHom
                Algebra.TensorProduct.includeRight.toRingHom ⋯ ⋯)))
          (AlgebraicGeometry.pullbackSpecIso R T T).inv))
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- If a set is at finite Hausdorff edistance of a nonempty set, it is nonempty.  -/
Metric.nonempty_of_hausdorffEDist_ne_top : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {s t : Set α}, s.Nonempty → Metric.hausdorffEDist s t ≠ ⊤ → t.Nonempty
-- Mathlib.CategoryTheory.Limits.Shapes.End
CategoryTheory.Limits.Cowedge.IsColimit.hom_ext : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} {c : CategoryTheory.Limits.Cowedge F}
  (hc : CategoryTheory.Limits.IsColimit c) {X : C} {f g : c.pt ⟶ X},
  (∀ (j : (CategoryTheory.Limits.multispanShapeCoend J).R),
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multicofork.π c j) f =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multicofork.π c j) g) →
    f = g
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.prelaxfunctor_toPrelaxFunctorStruct_map₂ : ∀ {a b : CategoryTheory.Cat} {f g : a ⟶ b} (f_1 : f ⟶ g),
  CategoryTheory.WithTerminal.prelaxfunctor.map₂ f_1 =
    CategoryTheory.NatTrans.toCatHom₂ (CategoryTheory.WithTerminal.map₂ f_1.toNatTrans)
-- Mathlib.Topology.MetricSpace.Isometry
/-- **Alias** of `IsometryEquiv.preimage_eball`. -/
IsometryEquiv.preimage_emetric_ball : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] (h : α ≃ᵢ β) (x : β)
  (r : ENNReal), ⇑h ⁻¹' Metric.eball x r = Metric.eball (h.symm x) r
-- Init.Data.Fin.Lemmas
Fin.succ_last : ∀ (n : ℕ), (Fin.last n).succ = Fin.last n.succ
-- Std.Data.DTreeMap.Internal.Lemmas
/-- Internal implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.«tacticSimp_to_model[_]Using_» : Lean.ParserDescr
-- Mathlib.Data.Nat.MaxPowDiv
pow_padicValNat_dvd : ∀ {p n : ℕ}, p ^ padicValNat p n ∣ n
-- Mathlib.Algebra.Order.Group.OrderIso
OrderIso.neg.eq_1 : ∀ (α : Type u) [inst : AddGroup α] [inst_1 : LE α] [inst_2 : AddLeftMono α] [inst_3 : AddRightMono α],
  OrderIso.neg α = { toEquiv := Equiv.trans (Equiv.neg α) OrderDual.toDual, map_rel_iff' := ⋯ }
-- Std.Http.Test.Helpers
_private.Std.Http.Test.Helpers.0.Std.Http.Internal.Test.sendClose : Std.Http.Internal.Mock.Client →
  Std.Http.Internal.Mock.Server → ByteArray → Std.Http.Internal.Test.TestHandler → Std.Http.Config → IO ByteArray
-- Mathlib.Algebra.BigOperators.Finprod
finsum_congr : ∀ {M : Type u_2} {α : Sort u_4} [inst : AddCommMonoid M] {f g : α → M}, (∀ (x : α), f x = g x) → finsum f = finsum g
-- Mathlib.GroupTheory.GroupAction.Defs
MulAction.orbit_smul_subset : ∀ {M : Type u_1} {α : Type u_3} [inst : Monoid M] [inst_1 : MulAction M α] (m : M) (a : α),
  MulAction.orbit M (m • a) ⊆ MulAction.orbit M a
-- Mathlib.MeasureTheory.PiSystem
MeasurableSpace.DynkinSystem.generate_inter : ∀ {α : Type u_3} {s : Set (Set α)},
  IsPiSystem s →
    ∀ {t₁ t₂ : Set α},
      (MeasurableSpace.DynkinSystem.generate s).Has t₁ →
        (MeasurableSpace.DynkinSystem.generate s).Has t₂ → (MeasurableSpace.DynkinSystem.generate s).Has (t₁ ∩ t₂)
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.Splits.one : ∀ {R : Type u_1} [inst : Semiring R], Polynomial.Splits 1
-- Mathlib.CategoryTheory.Abelian.Pseudoelements
/-- A monomorphism is injective on pseudoelements.  -/
CategoryTheory.Abelian.Pseudoelement.pseudo_injective_of_mono : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {P Q : C} (f : P ⟶ Q)
  [CategoryTheory.Mono f], Function.Injective (CategoryTheory.Abelian.Pseudoelement.pseudoApply f)
-- Mathlib.Algebra.Algebra.Tower
AlgHom.restrictScalars.congr_simp : ∀ (R : Type u) {S : Type v} {A : Type w} {B : Type u₁} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : Semiring A] [inst_3 : Semiring B] [inst_4 : Algebra R S] [inst_5 : Algebra S A] [inst_6 : Algebra S B]
  [inst_7 : Algebra R A] [inst_8 : Algebra R B] [inst_9 : IsScalarTower R S A] [inst_10 : IsScalarTower R S B]
  (f f_1 : A →ₐ[S] B), f = f_1 → AlgHom.restrictScalars R f = AlgHom.restrictScalars R f_1
-- Mathlib.Topology.Sheaves.Stalks
TopCat.Presheaf.stalkPushforward.stalkPushforward_iso_of_isInducing : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X Y : TopCat}
  {f : X ⟶ Y},
  Topology.IsInducing ⇑(CategoryTheory.ConcreteCategory.hom f) →
    ∀ (F : TopCat.Presheaf C X) (x : ↑X), CategoryTheory.IsIso (TopCat.Presheaf.stalkPushforward C f F x)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokenType.decorator : Lean.Lsp.SemanticTokenType
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddLocalization.rec.eq_1 : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {p : AddLocalization S → Sort u}
  (f : (a : M) → (b : ↥S) → p (AddLocalization.mk a b))
  (H : ∀ {a c : M} {b d : ↥S} (h : (AddLocalization.r S) (a, b) (c, d)), ⋯ ▸ f a b = f c d) (x : AddLocalization S),
  AddLocalization.rec f H x = Quot.rec (fun y => f y.1 y.2) ⋯ x
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.Array.foldlM.loop.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (i' : ℕ) (h_1 : Unit → motive 0) (h_2 : (i' : ℕ) → motive i'.succ),
  (match i'.succ with
    | 0 => h_1 ()
    | i'.succ => h_2 i') =
    h_2 i'
-- Mathlib.Data.Num.ZNum
PosNum.divMod.eq_def : ∀ (d x : PosNum),
  d.divMod x =
    match x with
    | n.bit0 =>
      match d.divMod n with
      | (q, r₁) => d.divModAux q r₁.bit0
    | n.bit1 =>
      match d.divMod n with
      | (q, r₁) => d.divModAux q r₁.bit1
    | PosNum.one => d.divModAux 0 1
-- Mathlib.Order.Filter.Tendsto
Filter.tendsto_def : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {l₁ : Filter α} {l₂ : Filter β},
  Filter.Tendsto f l₁ l₂ ↔ ∀ s ∈ l₂, f ⁻¹' s ∈ l₁
-- Mathlib.CategoryTheory.Endomorphism
CategoryTheory.End.one : {C : Type u} → [inst : CategoryTheory.CategoryStruct.{v, u} C] → (X : C) → One (CategoryTheory.End X)