mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.Stalk
/-- Given a local ring `R` and scheme `X`, morphisms `Spec R ⟶ X` corresponds to pairs
`(x, f)` where `x : X` and `f : 𝒪_{X, x} ⟶ R` is a local ring homomorphism.
 -/
AlgebraicGeometry.SpecToEquivOfLocalRing : (X : AlgebraicGeometry.Scheme) →
  (R : CommRingCat) →
    [IsLocalRing ↑R] → (AlgebraicGeometry.Spec R ⟶ X) ≃ (x : ↥X) × { f // IsLocalHom (CommRingCat.Hom.hom f) }
-- Mathlib.Data.Rat.Init
/-- The canonical homomorphism `ℚ≥0 → K`.

Do not use directly. Use the coercion instead.  -/
NNRatCast.nnratCast : {K : Type u_1} → [self : NNRatCast K] → ℚ≥0 → K
-- Mathlib.CategoryTheory.Category.Preorder
CategoryTheory.eqToHom_comp_homOfLE : ∀ {X : Type u} [inst : Preorder X] {a b c : X} (hab : a = b) (hbc : b ≤ c),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom hab) (CategoryTheory.homOfLE hbc) =
    CategoryTheory.homOfLE ⋯
-- Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
CliffordAlgebra.unop_reverseOp : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} (x : CliffordAlgebra Q),
  MulOpposite.unop (CliffordAlgebra.reverseOp x) = CliffordAlgebra.reverse x
-- Lean.Data.Lsp.Workspace
Lean.Lsp.FileSystemWatcher.delete : ℕ
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.coe_comp_structureMap : ∀ {ι : Type u_1} (R : ι → Type u_2) (A : (i : ι) → Set (R i)) {𝓕 : Filter ι},
  DFunLike.coe ∘ RestrictedProduct.structureMap R A 𝓕 = fun x i => ↑(x i)
-- Mathlib.Order.Hom.WithTopBot
WithTop.toDualBotEquiv.eq_1 : ∀ {α : Type u_1} [inst : LE α], WithTop.toDualBotEquiv = OrderIso.refl (WithTop αᵒᵈ)
-- Mathlib.AlgebraicTopology.DoldKan.PInfty
AlgebraicTopology.DoldKan.PInfty_f_comp_QInfty_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {X : CategoryTheory.SimplicialObject C} (n : ℕ),
  CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.PInfty.f n) (AlgebraicTopology.DoldKan.QInfty.f n) = 0
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getD_erase : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α],
  (↑m).WF →
    ∀ {k a : α} {fallback : β a}, (m.erase k).getD a fallback = if (k == a) = true then fallback else m.getD a fallback
-- Std.Data.DTreeMap.Internal.WF.Defs
Std.DTreeMap.Internal.Impl.WF.below.erase : ∀ {α : Type u} [inst : Ord α] {motive : {β : α → Type v} → (a : Std.DTreeMap.Internal.Impl α β) → a.WF → Prop}
  {x : α → Type v} {t : Std.DTreeMap.Internal.Impl α x} {h : t.Balanced} {k : α} (a : t.WF),
  Std.DTreeMap.Internal.Impl.WF.below a → motive t a → Std.DTreeMap.Internal.Impl.WF.below ⋯
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.map_φ : ∀ {R : Type r} {S : Type s} [inst : CommRing R] [inst_1 : CommRing S] (W : WeierstrassCurve R) (f : R →+* S) (n : ℤ),
  (W.map f).φ n = Polynomial.map (Polynomial.mapRingHom f) (W.φ n)
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgEquiv.symm_arrowCongr : ∀ {R : Type u_1} {A₁ : Type u_2} {A₂ : Type u_3} {A₁' : Type u_5} {A₂' : Type u_6} [inst : CommSemiring R]
  [inst_1 : Semiring A₁] [inst_2 : Semiring A₂] [inst_3 : Semiring A₁'] [inst_4 : Semiring A₂'] [inst_5 : Algebra R A₁]
  [inst_6 : Algebra R A₂] [inst_7 : Algebra R A₁'] [inst_8 : Algebra R A₂'] [inst_9 : Star A₁] [inst_10 : Star A₂]
  [inst_11 : Star A₁'] [inst_12 : Star A₂'] (e₁ : A₁ ≃⋆ₐ[R] A₁') (e₂ : A₂ ≃⋆ₐ[R] A₂'),
  (e₁.arrowCongr e₂).symm = e₁.symm.arrowCongr e₂.symm
-- Mathlib.Combinatorics.Quiver.Schreier
Quiver.SchreierGraph.labelling_map : ∀ (V : Type u_1) {M : Type u_2} [inst : SMul M V] {S : Type u_3} (ι : S → M) {X Y : Quiver.SchreierGraph V ι}
  (e : X ⟶ Y), (Quiver.SchreierGraph.labelling V ι).map e = ↑e
-- Lean.Meta.Tactic.Simp.Arith.Int.Simp
Lean.Meta.Simp.Arith.Int.simpExpr? : Lean.Expr → Lean.MetaM (Option (Lean.Expr × Lean.Expr))
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.toArrowArrowFunctor_map_right_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.Square C} (φ : X ⟶ Y),
  (CategoryTheory.Square.toArrowArrowFunctor.map φ).right.left = φ.τ₂
-- Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
/-- The property that is satisfied by fibrant objects.
(This is only introduced in order to consider the full subcategory
`FibrantObject`. Otherwise, the typeclass `IsFibrant`
is preferred.)  -/
HomotopicalAlgebra.fibrantObjects : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [HomotopicalAlgebra.CategoryWithFibrations C] →
      [CategoryTheory.Limits.HasTerminal C] → CategoryTheory.ObjectProperty C
-- Mathlib.Topology.Category.LightProfinite.Sequence
LightProfinite.natUnionInftyEmbedding.eq_1 : LightProfinite.natUnionInftyEmbedding =
  {
    toFun := fun x =>
      match x with
      | none => 0
      | some n => 1 / (↑n + 1),
    continuous_toFun := LightProfinite.natUnionInftyEmbedding._proof_1 }
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.pullback.lift.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z}
  [inst_1 : CategoryTheory.Limits.HasPullback f g] (h h_1 : W ⟶ X) (e_h : h = h_1) (k k_1 : W ⟶ Y) (e_k : k = k_1)
  (w : CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp k g),
  CategoryTheory.Limits.pullback.lift h k w = CategoryTheory.Limits.pullback.lift h_1 k_1 ⋯
-- Mathlib.Data.Set.Subsingleton
/-- `s`, coerced to a type, is a subsingleton type if and only if `s` is a subsingleton set.  -/
Set.subsingleton_coe : ∀ {α : Type u} (s : Set α), Subsingleton ↑s ↔ s.Subsingleton
-- Mathlib.Algebra.Ring.Basic
AddMonoidHom.mul_apply : ∀ {R : Type u_1} [inst : NonUnitalNonAssocSemiring R] (x y : R), (AddMonoidHom.mul x) y = x * y
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.IsImage.leftInvOn_piecewise : ∀ {α : Type u_1} {β : Type u_2} {e : PartialEquiv α β} {s : Set α} {t : Set β} {e' : PartialEquiv α β}
  [inst : (i : α) → Decidable (i ∈ s)] [inst_1 : (i : β) → Decidable (i ∈ t)],
  e.IsImage s t →
    e'.IsImage s t → Set.LeftInvOn (t.piecewise ↑e.symm ↑e'.symm) (s.piecewise ↑e ↑e') (s.ite e.source e'.source)
-- Mathlib.Analysis.Asymptotics.ExpGrowth
ExpGrowth.expGrowthInf_monotone : Monotone ExpGrowth.expGrowthInf
-- Mathlib.CategoryTheory.Shift.Adjunction
/-- Given an adjunction `F ⊣ G` and a `CommShift` structure on `F`, this constructs
the unique compatible `CommShift` structure on `G`.
 -/
CategoryTheory.Adjunction.rightAdjointCommShift : {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] →
        {F : CategoryTheory.Functor C D} →
          {G : CategoryTheory.Functor D C} →
            (F ⊣ G) →
              (A : Type u_3) →
                [inst_2 : AddGroup A] →
                  [inst_3 : CategoryTheory.HasShift C A] →
                    [inst_4 : CategoryTheory.HasShift D A] → [F.CommShift A] → G.CommShift A
-- Mathlib.CategoryTheory.Abelian.Basic
CategoryTheory.Abelian.epi_of_cokernel_π_eq_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {P Q : C} (f : P ⟶ Q),
  CategoryTheory.Limits.cokernel.π f = 0 → CategoryTheory.Epi f
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Univ
/-- The universal characteristic polynomial for `n × n`-matrices,
is the characteristic polynomial of `Matrix.mvPolynomialX n n ℤ` with entries `Xᵢⱼ`.

Its `i`-th coefficient is a homogeneous polynomial of degree `n - i`,
see `Matrix.charpoly.univ_coeff_isHomogeneous`.

By evaluating the coefficients at the entries of a matrix `M`,
one obtains the characteristic polynomial of `M`,
see `Matrix.charpoly.univ_map_eval₂Hom`.  -/
Matrix.charpoly.univ : (R : Type u_1) →
  (n : Type u_3) → [inst : CommRing R] → [Fintype n] → [DecidableEq n] → Polynomial (MvPolynomial (n × n) R)
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
PowerSeries.IsWeierstrassDivisorAt.div_add : ∀ {A : Type u_1} [inst : CommRing A] {g : PowerSeries A} {I : Ideal A} (H : g.IsWeierstrassDivisorAt I)
  (f f' : PowerSeries A) [inst_1 : IsAdicComplete I A], H.div (f + f') = H.div f + H.div f'
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.upperBound?.eq_1 : ∀ {α : Type u_1} (cut : α → Ordering) (x : Option α), RBTree.RBNode.upperBound? cut RBTree.RBNode.nil x = x
-- Std.Time.DateTime
/-- Add `Month.Offset` to a `DateTime`, rolling over excess days.
 -/
Std.Time.DateTime.addMonthsRollOver : Std.Time.DateTime → Std.Time.Month.Offset → Std.Time.DateTime
-- Mathlib.Data.TwoPointing
TwoPointing.pi_snd : ∀ (α : Type u_1) {β : Type u_2} (q : TwoPointing β) [inst : Nonempty α],
  (TwoPointing.pi α q).toProd.2 = Function.const α q.toProd.2
-- Mathlib.Data.Sign.Defs
SignType.coe_one : ∀ {α : Type u_1} [inst : Zero α] [inst_1 : One α] [inst_2 : Neg α], ↑1 = 1
-- Mathlib.Algebra.Order.ToIntervalMod
toIocMod_add_toIcoMod_zero : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α), toIocMod hp 0 (a - b) + toIcoMod hp 0 (b - a) = p
-- Init.Data.Int.Order
Int.sub_nonpos_of_le : ∀ {a b : ℤ}, a ≤ b → a - b ≤ 0
-- Mathlib.Data.W.Constructions
WType.rightInverse_nat : Function.RightInverse WType.ofNat WType.toNat
-- Mathlib.Data.Multiset.ZeroCons
Multiset.insert_eq_cons : ∀ {α : Type u_1} (a : α) (s : Multiset α), insert a s = a ::ₘ s
-- Mathlib.RingTheory.MvPowerSeries.Derivative
/-- The formal partial derivative of a multivariate formal power series with respect to
variable `i`, as an `R`-derivation on `MvPowerSeries σ R`.  -/
MvPowerSeries.pderiv : {σ : Type u_1} → (R : Type u_2) → [inst : CommSemiring R] → σ → Derivation R (MvPowerSeries σ R) (MvPowerSeries σ R)
-- Mathlib.Order.Category.Frm
/-- The underlying `FrameHom`.  -/
Frm.Hom.hom' : {X Y : Frm} → X.Hom Y → FrameHom ↑X ↑Y
-- Mathlib.Algebra.Group.Units.Basic
AddRightCancelMonoid.eq_zero_of_add_left : ∀ {α : Type u} [inst : AddRightCancelMonoid α] [Subsingleton (AddUnits α)] {a b : α}, a + b = 0 → b = 0
-- Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
CategoryTheory.SimplicialObject.Split.nondegComplexFunctor_obj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (S : CategoryTheory.SimplicialObject.Split C),
  CategoryTheory.SimplicialObject.Split.nondegComplexFunctor.obj S = S.s.nondegComplex
-- Mathlib.Analysis.Analytic.Basic
hasFPowerSeriesWithinAt_insert : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x y : E},
  HasFPowerSeriesWithinAt f p (insert y s) x ↔ HasFPowerSeriesWithinAt f p s x
-- Mathlib.CategoryTheory.Idempotents.Karoubi
CategoryTheory.Idempotents.Karoubi.comp_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P Q R : CategoryTheory.Idempotents.Karoubi C}
  (f : P ⟶ Q) (g : Q ⟶ R), (CategoryTheory.CategoryStruct.comp f g).f = CategoryTheory.CategoryStruct.comp f.f g.f
-- Mathlib.CategoryTheory.Limits.Opposites
/-- If `C` has colimits, we can construct limits for `Cᵒᵖ`.
 -/
CategoryTheory.Limits.hasLimits_op_of_hasColimits : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C]
  [CategoryTheory.Limits.HasColimitsOfSize.{v₂, u₂, v₁, u₁} C],
  CategoryTheory.Limits.HasLimitsOfSize.{v₂, u₂, v₁, u₁} Cᵒᵖ
-- Mathlib.RepresentationTheory.Coinduced
Rep.coindVEquiv_symm_apply_coe : ∀ {k : Type u} {G : Type v} {H : Type w} [inst : CommRing k] [inst_1 : Monoid G] [inst_2 : Monoid H] (φ : G →* H)
  (A : Rep.{max u w, u, v} k G) (f : Rep.res φ (Rep.leftRegular k H) ⟶ A) (h : H),
  ↑((Rep.coindVEquiv φ A).symm f) h = (Rep.Hom.hom f).toLinearMap (MonoidAlgebra.single h 1)
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ioo_eq_empty : ∀ {α : Type u_2} {a b : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α], ¬a < b → Finset.Ioo a b = ∅
-- Mathlib.Topology.Spectral.ConstructibleTopology
/-- A type synonym for `X` that is equipped with the constructible topology of `X`.  -/
WithConstructibleTopology : (X : Type u_2) → [TopologicalSpace X] → Type u_2
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfcHom_eq_cfc_extend : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A] [inst_6 : Ring A]
  [inst_7 : StarRing A] [inst_8 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] {a : A} (g : R → R)
  (ha : p a) (f : C(↑(spectrum R a), R)), (cfcHom ha) f = cfc (Function.extend Subtype.val (⇑f) g) a
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteGrp.Hom.hom.eq_1 : ∀ {M N : ProfiniteGrp.{u}} (f : M.Hom N), f.hom = CategoryTheory.ConcreteCategory.hom f
-- Mathlib.Data.Nat.Factorization.Basic
Nat.dvd_iff_div_factorization_eq_tsub : ∀ {d n : ℕ}, d ≠ 0 → d ≤ n → (d ∣ n ↔ (n / d).factorization = n.factorization - d.factorization)
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.Scheme.ofRestrict_toLRSHom_c_app : ∀ {U : TopCat} (X : AlgebraicGeometry.Scheme) {f : U ⟶ TopCat.of ↥X}
  (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (V : (TopologicalSpace.Opens ↥X)ᵒᵖ),
  (AlgebraicGeometry.Scheme.Hom.toLRSHom (X.ofRestrict h)).c.app V =
    X.presheaf.map (⋯.adjunction.counit.app (Opposite.unop V)).op
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.comm : ∀ {α : Type u} {β : α → Type v} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β}, t₁.Equiv t₂ ↔ t₂.Equiv t₁
-- Mathlib.Topology.UniformSpace.Basic
instPartialOrderUniformSpace : {α : Type ua} → PartialOrder (UniformSpace α)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Substructure
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Substructure.0.Std.Tactic.BVDecide.BVLogicalExpr.bitblast.go.match_5.eq_5 : ∀ (motive : Std.Tactic.BVDecide.BVLogicalExpr → Sort u_1) (g : Std.Tactic.BVDecide.Gate)
  (lhs rhs : Std.Tactic.BVDecide.BoolExpr Std.Tactic.BVDecide.BVPred)
  (h_1 : (var : Std.Tactic.BVDecide.BVPred) → motive (Std.Tactic.BVDecide.BoolExpr.literal var))
  (h_2 : (val : Bool) → motive (Std.Tactic.BVDecide.BoolExpr.const val))
  (h_3 : (expr : Std.Tactic.BVDecide.BoolExpr Std.Tactic.BVDecide.BVPred) → motive expr.not)
  (h_4 : (discr lhs rhs : Std.Tactic.BVDecide.BoolExpr Std.Tactic.BVDecide.BVPred) → motive (discr.ite lhs rhs))
  (h_5 :
    (g : Std.Tactic.BVDecide.Gate) →
      (lhs rhs : Std.Tactic.BVDecide.BoolExpr Std.Tactic.BVDecide.BVPred) →
        motive (Std.Tactic.BVDecide.BoolExpr.gate g lhs rhs)),
  (match Std.Tactic.BVDecide.BoolExpr.gate g lhs rhs with
    | Std.Tactic.BVDecide.BoolExpr.literal var => h_1 var
    | Std.Tactic.BVDecide.BoolExpr.const val => h_2 val
    | expr.not => h_3 expr
    | discr.ite lhs rhs => h_4 discr lhs rhs
    | Std.Tactic.BVDecide.BoolExpr.gate g lhs rhs => h_5 g lhs rhs) =
    h_5 g lhs rhs
-- Init.Data.Int.Order
Int.negSucc_lt_zero : ∀ (n : ℕ), Int.negSucc n < 0
-- Init.Data.Option.List
Option.toList_eq_nil_iff : ∀ {α : Type u_1} {o : Option α}, o.toList = [] ↔ o = none
-- Init.Data.List.Zip
List.map_prod_right_eq_zip : ∀ {α : Type u_1} {β : Type u_2} {l : List α} {f : α → β}, List.map (fun x => (f x, x)) l = (List.map f l).zip l
-- Mathlib.Analysis.Normed.Module.WeakDual
/-- The polar set `polar 𝕜 s` of `s : Set E` seen as a subset of the dual of `E` with the
weak-star topology is `WeakDual.polar 𝕜 s`.  -/
WeakDual.polar : (𝕜 : Type u_1) →
  {M : Type u_2} →
    [inst : NontriviallyNormedField 𝕜] →
      [inst_1 : AddCommGroup M] → [inst_2 : TopologicalSpace M] → [inst_3 : Module 𝕜 M] → Set M → Set (WeakDual 𝕜 M)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
CategoryTheory.Limits.PushoutCocone.isIso_inr_of_epi_of_isColimit : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} [CategoryTheory.Epi f]
  {t : CategoryTheory.Limits.PushoutCocone f f} (ht : CategoryTheory.Limits.IsColimit t), CategoryTheory.IsIso t.inr
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.update.eq_1 : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] (m : M) (r : R) (x : AddMonoidAlgebra R M),
  AddMonoidAlgebra.update m r x = AddMonoidAlgebra.ofCoeff (x.coeff.update m r)
-- Mathlib.Data.Set.Insert
Set.ofPred_mem_list_eq_singleton_of_nodup : ∀ {α : Type u_1} {l : List α}, l.Nodup → ∀ {a : α}, {x | x ∈ l} = {a} ↔ l = [a]
-- Mathlib.Data.Nat.Cast.Defs
nsmul_one : ∀ {A : Type u_2} [inst : AddMonoidWithOne A] (n : ℕ), n • 1 = ↑n
-- Mathlib.Analysis.CStarAlgebra.Unitary.Maps
Unitary.mulLeft_mul_apply : ∀ {R : Type u_1} {A : Type u_2} [inst : NormedRing A] [inst_1 : StarRing A] [inst_2 : CStarRing A] [inst_3 : Ring R]
  [inst_4 : Module R A] [inst_5 : SMulCommClass R A A] (u v : ↥(unitary A)) (x : A),
  ((Unitary.mulLeft R A) (u * v)) x = ((Unitary.mulLeft R A) u) (((Unitary.mulLeft R A) v) x)
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
CategoryTheory.Functor.PreOneHypercoverDenseData.multicospanShape_fst : ∀ {C₀ : Type u₀} {C : Type u} [inst : CategoryTheory.Category.{v₀, u₀} C₀] [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor C₀ C} {X : C} (data : F.PreOneHypercoverDenseData X) (j : data.I₁'),
  data.multicospanShape.fst j = j.fst.1
-- Mathlib.Topology.Bornology.Basic
BoundedSpace.mk : ∀ {α : Type u_4} [inst : Bornology α], Bornology.IsBounded Set.univ → BoundedSpace α
-- Batteries.Data.Nat.Bisect
_private.Batteries.Data.Nat.Bisect.0.Nat.bisect.match_1.eq_1 : ∀ (motive : Bool → Sort u_1) (h_1 : false = false → motive false) (h_2 : false = true → motive true),
  (match hmid : false with
    | false => h_1 hmid
    | true => h_2 hmid) =
    h_1 ⋯
-- Mathlib.Data.List.Forall2
List.rel_mem : ∀ {α : Type u_1} {β : Type u_2} {R : α → β → Prop},
  Relator.BiUnique R →
    Relator.LiftFun R (Relator.LiftFun (List.Forall₂ R) Iff) (fun x1 x2 => x1 ∈ x2) fun x1 x2 => x1 ∈ x2
-- Init.Data.SInt.Lemmas
Int32.toBitVec_maxValue : Int32.maxValue.toBitVec = BitVec.intMax 32
-- Mathlib.Topology.Algebra.Support
HasCompactSupport.mono : ∀ {α : Type u_2} {β : Type u_4} {γ : Type u_5} [inst : TopologicalSpace α] [inst_1 : Zero β] [inst_2 : Zero γ]
  {f : α → β} {f' : α → γ}, HasCompactSupport f → Function.support f' ⊆ Function.support f → HasCompactSupport f'
-- Std.Time.Format.Basic
Std.Time.GenericFormat.mk.sizeOf_spec : ∀ {awareness : Std.Time.Awareness} (config : Std.Time.FormatConfig) (string : Std.Time.FormatString),
  sizeOf { config := config, string := string } = 1 + sizeOf config + sizeOf string
-- Mathlib.Order.GaloisConnection.Basic
/-- Lift the suprema and infima along a Galois insertion  -/
GaloisInsertion.liftLattice : {α : Type u} →
  {β : Type v} →
    {l : α → β} → {u : β → α} → [inst : PartialOrder β] → [inst_1 : Lattice α] → GaloisInsertion l u → Lattice β
-- Mathlib.Algebra.Group.Equiv.Defs
/-- The identity map is an additive isomorphism.  -/
AddEquiv.refl : (M : Type u_9) → [inst : Add M] → M ≃+ M
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roo.toArray.congr_simp : ∀ {α : Type u} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [inst_4 : Std.Rxo.IsAlwaysFinite α] (r r_1 : Std.Roo α),
  r = r_1 → r.toArray = r_1.toArray
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Matrix.invOf_eq : ∀ {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α] (A : Matrix n n α)
  [inst_3 : Invertible A.det] [inst_4 : Invertible A], ⅟A = ⅟A.det • A.adjugate
-- Mathlib.Analysis.Calculus.Deriv.Basic
hasDerivAtFilter_ofNat : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] (L : Filter (𝕜 × 𝕜)) (n : ℕ) [inst_3 : OfNat F n], HasDerivAtFilter (OfNat.ofNat n) 0 L
-- Mathlib.Order.Interval.Finset.Defs
Finset.Ioi_ofDual : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrderTop α] (a : αᵒᵈ),
  Finset.Ioi (OrderDual.ofDual a) = Finset.map OrderDual.ofDual.toEmbedding (Finset.Iio a)
-- Mathlib.Data.List.Sort
/-- The list obtained from a strictly antitone tuple is sorted.  -/
List.SortedGT.strictAnti : ∀ {α : Type u_1} [inst : Preorder α] {n : ℕ} {f : Fin n → α}, (List.ofFn f).SortedGT → StrictAnti f
-- Mathlib.Data.Set.Card
Set.ncard_mono : ∀ {α : Type u_1} [Finite α], Monotone Set.ncard
-- Init.Data.String.Lemmas.Pattern.String.ForwardSearcher
_private.Init.Data.String.Lemmas.Pattern.String.ForwardSearcher.0.String.Slice.Pattern.Model.ForwardSliceSearcher.prefixFunctionRecurrence.induct_unfolding : ∀ (pat : ByteArray) (stackPos : ℕ) (hst : stackPos < pat.size) (motive : (guess : ℕ) → guess < stackPos → ℕ → Prop),
  (∀ (guess : ℕ) (hg : guess < stackPos), pat[guess] = pat[stackPos] → motive guess hg (guess + 1)) →
    (∀ (hg : 0 < stackPos), ¬pat[0] = pat[stackPos] → motive 0 hg 0) →
      (∀ (guess : ℕ) (hg : guess < stackPos),
          ¬pat[guess] = pat[stackPos] →
            ¬guess = 0 →
              ∀ (this : String.Slice.Pattern.Model.ForwardSliceSearcher.prefixFunction✝ pat (guess - 1) ⋯ < guess),
                motive (String.Slice.Pattern.Model.ForwardSliceSearcher.prefixFunction✝ pat (guess - 1) ⋯) ⋯
                    (String.Slice.Pattern.Model.ForwardSliceSearcher.prefixFunctionRecurrence✝ pat stackPos hst
                      (String.Slice.Pattern.Model.ForwardSliceSearcher.prefixFunction✝ pat (guess - 1) ⋯) ⋯) →
                  motive guess hg
                    (String.Slice.Pattern.Model.ForwardSliceSearcher.prefixFunctionRecurrence✝ pat stackPos hst
                      (String.Slice.Pattern.Model.ForwardSliceSearcher.prefixFunction✝ pat (guess - 1) ⋯) ⋯)) →
        ∀ (guess : ℕ) (hg : guess < stackPos),
          motive guess hg
            (String.Slice.Pattern.Model.ForwardSliceSearcher.prefixFunctionRecurrence✝ pat stackPos hst guess hg)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  t₁.Equiv t₂ → ∀ (k : α) (v : β), (t₁.insert k v).Equiv (t₂.insert k v)
-- Mathlib.Order.Circular
/-- A circular order is the analogue of a linear order where you can loop around. `≤` and `<` are
replaced by ternary relations `btw` and `sbtw`. `btw` is reflexive, cyclic, antisymmetric and total.
`sbtw` is transitive.  -/
CircularOrder : Type u_1 → Type u_1
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometry.coe_one : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_10} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup V]
  [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P] [inst_4 : NormedAddTorsor V P], ⇑1 = id
-- Init.Data.String.Lemmas.Pattern.Split.Pred
_private.Init.Data.String.Lemmas.Pattern.Split.Pred.0.String.Slice.Pattern.Model.split.match_1.splitter : {s : String.Slice} →
  (motive : Option s.Pos → Sort u_1) →
    (x : Option s.Pos) → ((pos : s.Pos) → x = some pos → motive (some pos)) → (x = none → motive none) → motive x
-- Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
CategoryTheory.SmallObject.functorialFactorizationData_p_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (I : CategoryTheory.MorphismProperty C) (κ : Cardinal.{w})
  [inst_1 : Fact κ.IsRegular] [inst_2 : OrderBot κ.ord.ToType] [inst_3 : I.IsCardinalForSmallObjectArgument κ]
  (f : CategoryTheory.Arrow C),
  (CategoryTheory.SmallObject.functorialFactorizationData I κ).p.app f = CategoryTheory.SmallObject.πObj I κ f.hom
-- Lean.Meta.AppBuilder
/-- Returns `a <= b`  -/
Lean.Meta.mkLe : Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr
-- Aesop.Tree.State
Aesop.Rapp.stateNoCache : Aesop.Rapp → BaseIO Aesop.NodeState
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.P'IsoUnopOpP.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C),
  S.P'IsoUnopOpP = CategoryTheory.Limits.pushoutIsoUnopPullback S.L₂.f S.v₂₃.τ₁