mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Option.Lemmas
_private.Init.Data.Option.Lemmas.0.Option.bind.match_1.splitter : {α : Type u_1} →
  {β : Type u_2} →
    (motive : Option α → (α → Option β) → Sort u_3) →
      (x : Option α) →
        (x_1 : α → Option β) →
          ((x : α → Option β) → motive none x) → ((a : α) → (f : α → Option β) → motive (some a) f) → motive x x_1
-- Mathlib.RingTheory.TensorProduct.Maps
/-- If `S` is commutative, for a pair of morphisms `f : A →ₐ[R] S`, `g : B →ₐ[R] S`,
We obtain a map `A ⊗[R] B →ₐ[R] S` that commutes with `f`, `g` via `a ⊗ b ↦ f(a) * g(b)`.

This is a special case of `Algebra.TensorProduct.productLeftAlgHom` for when the two base rings are
the same.
 -/
Algebra.TensorProduct.productMap : {R : Type uR} →
  {S : Type uS} →
    {A : Type uA} →
      {B : Type uB} →
        [inst : CommSemiring R] →
          [inst_1 : Semiring A] →
            [inst_2 : Semiring B] →
              [inst_3 : CommSemiring S] →
                [inst_4 : Algebra R A] →
                  [inst_5 : Algebra R B] →
                    [inst_6 : Algebra R S] → (A →ₐ[R] S) → (B →ₐ[R] S) → TensorProduct R A B →ₐ[R] S
-- Mathlib.Combinatorics.Quiver.Symmetric
Quiver.Push.ofMapReverse : ∀ {V : Type u_2} [inst : Quiver V] {V' : Type u_4} (σ : V → V') [h : Quiver.HasInvolutiveReverse V],
  (Quiver.Push.of σ).MapReverse
-- Mathlib.CategoryTheory.Abelian.Yoneda
CategoryTheory.Abelian.preadditiveCoyonedaObj_map_surjective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {G : C}
  [CategoryTheory.Projective G],
  CategoryTheory.IsSeparator G →
    ∀ {X : C} (p : G ⟶ X) [CategoryTheory.Epi p] {Y : C},
      Function.Surjective (CategoryTheory.preadditiveCoyonedaObj G).map
-- Lean.Meta.AppBuilder
_private.Lean.Meta.AppBuilder.0.Lean.Meta.mkAppOptMAux : Lean.Expr → Array (Option Lean.Expr) → ℕ → Array Lean.Expr → ℕ → Array Lean.MVarId → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Algebra.Order.Ring.Ordering.Defs
RingPreordering.instSetLike : (R : Type u_1) → [inst : CommRing R] → SetLike (RingPreordering R) R
-- Mathlib.Data.PFun
/-- Turns a function into a partial function with a prescribed domain.  -/
PFun.res : {α : Type u_1} → {β : Type u_2} → (α → β) → Set α → α →. β
-- Mathlib.Algebra.Homology.ShortComplex.Abelian
/-- Let `S` be a short complex in an abelian category. Let `kf` be a
limit kernel fork of `S.g` and `cc` a limit cokernel cofork of `S.f`.
Let `kf.pt ⟶ H ⟶ cc.pt` be an epi-mono factorization of `kf.ι ≫ cc.π : kf.pt ⟶ cc.pt`,
then `H` identifies to the homology of `S`.  -/
CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.isoHomology : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      (S : CategoryTheory.ShortComplex C) →
        {kf : CategoryTheory.Limits.KernelFork S.g} →
          {cc : CategoryTheory.Limits.CokernelCofork S.f} →
            CategoryTheory.Limits.IsLimit kf →
              CategoryTheory.Limits.IsColimit cc →
                {H : C} →
                  {π : kf.pt ⟶ H} →
                    {ι : H ⟶ cc.pt} →
                      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι kf)
                            (CategoryTheory.Limits.Cofork.π cc) =
                          CategoryTheory.CategoryStruct.comp π ι →
                        [CategoryTheory.Epi π] → [CategoryTheory.Mono ι] → H ≅ S.homology
-- Mathlib.Algebra.Order.Floor.Extended
ENat.floor_add_natCast : ∀ (r : ENNReal) (n : ℕ), ⌊r + ↑n⌋ₑ = ⌊r⌋ₑ + ↑n
-- Lean.Elab.InfoTree.Types
Lean.Elab.CompletionInfo.id.sizeOf_spec : ∀ (stx : Lean.Syntax) (id : Lean.Name) (danglingDot : Bool) (lctx : Lean.LocalContext)
  (expectedType? : Option Lean.Expr),
  sizeOf (Lean.Elab.CompletionInfo.id stx id danglingDot lctx expectedType?) =
    1 + sizeOf stx + sizeOf id + sizeOf danglingDot + sizeOf lctx + sizeOf expectedType?
-- Init.Data.Vector.Lemmas
Vector.ext_iff : ∀ {α : Type u_1} {n : ℕ} {xs ys : Vector α n}, xs = ys ↔ ∀ (i : ℕ) (x : i < n), xs[i] = ys[i]
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.map_update_neg : ∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommGroup (M₁ i)] [inst_2 : AddCommGroup M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] (f : MultilinearMap R M₁ M₂) [inst_5 : DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (x : M₁ i),
  f (Function.update m i (-x)) = -f (Function.update m i x)
-- Mathlib.LinearAlgebra.RootSystem.Base
RootPairing.Base.mk.inj : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} {inst : CommRing R} {inst_1 : AddCommGroup M}
  {inst_2 : Module R M} {inst_3 : AddCommGroup N} {inst_4 : Module R N} {P : RootPairing ι R M N} {support : Finset ι}
  {linearIndepOn_root : LinearIndepOn R ⇑P.root ↑support} {linearIndepOn_coroot : LinearIndepOn R ⇑P.coroot ↑support}
  {root_mem_or_neg_mem :
    ∀ (i : ι),
      P.root i ∈ AddSubmonoid.closure (⇑P.root '' ↑support) ∨ -P.root i ∈ AddSubmonoid.closure (⇑P.root '' ↑support)}
  {coroot_mem_or_neg_mem :
    ∀ (i : ι),
      P.coroot i ∈ AddSubmonoid.closure (⇑P.coroot '' ↑support) ∨
        -P.coroot i ∈ AddSubmonoid.closure (⇑P.coroot '' ↑support)}
  {support_1 : Finset ι} {linearIndepOn_root_1 : LinearIndepOn R ⇑P.root ↑support_1}
  {linearIndepOn_coroot_1 : LinearIndepOn R ⇑P.coroot ↑support_1}
  {root_mem_or_neg_mem_1 :
    ∀ (i : ι),
      P.root i ∈ AddSubmonoid.closure (⇑P.root '' ↑support_1) ∨
        -P.root i ∈ AddSubmonoid.closure (⇑P.root '' ↑support_1)}
  {coroot_mem_or_neg_mem_1 :
    ∀ (i : ι),
      P.coroot i ∈ AddSubmonoid.closure (⇑P.coroot '' ↑support_1) ∨
        -P.coroot i ∈ AddSubmonoid.closure (⇑P.coroot '' ↑support_1)},
  { support := support, linearIndepOn_root := linearIndepOn_root, linearIndepOn_coroot := linearIndepOn_coroot,
        root_mem_or_neg_mem := root_mem_or_neg_mem, coroot_mem_or_neg_mem := coroot_mem_or_neg_mem } =
      { support := support_1, linearIndepOn_root := linearIndepOn_root_1,
        linearIndepOn_coroot := linearIndepOn_coroot_1, root_mem_or_neg_mem := root_mem_or_neg_mem_1,
        coroot_mem_or_neg_mem := coroot_mem_or_neg_mem_1 } →
    support = support_1
-- Mathlib.Algebra.MonoidAlgebra.Module
AddMonoidAlgebra.distribMulActionHom_ext'_iff : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} [inst : Semiring S] {N : Type u_7} [inst_1 : Monoid R]
  [inst_2 : AddMonoid N] [inst_3 : DistribMulAction R N] [inst_4 : DistribMulAction R S]
  {f g : AddMonoidAlgebra S M →+[R] N},
  f = g ↔
    ∀ (a : M),
      f.comp (AddMonoidAlgebra.singleDistribMulActionHom a) = g.comp (AddMonoidAlgebra.singleDistribMulActionHom a)
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
AddMonoidAlgebra.mapAddEquiv_single : ∀ {R : Type u_3} {S : Type u_4} {M : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Add M] (e : R ≃+ S)
  (r : R) (m : M), (AddMonoidAlgebra.mapAddEquiv M e) (AddMonoidAlgebra.single m r) = AddMonoidAlgebra.single m (e r)
-- Mathlib.Topology.UniformSpace.Equiv
UniformEquiv.injective : ∀ {α : Type u} {β : Type u_1} [inst : UniformSpace α] [inst_1 : UniformSpace β] (h : α ≃ᵤ β), Function.Injective ⇑h
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.Equiv.of_forall_contains_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp],
  t₁.WF → t₂.WF → (∀ (k : α), t₁.contains k = t₂.contains k) → t₁.Equiv t₂
-- Mathlib.RingTheory.LaurentSeries
LaurentSeries.exists_ratFunc_eq_v : ∀ {K : Type u_2} [inst : Field K] (x : LaurentSeries K), ∃ f, Valued.v f = Valued.v x
-- Mathlib.Analysis.SpecialFunctions.Pow.Continuity
NNReal.continuousOn_rpow_const : ∀ {r : ℝ} {s : Set NNReal}, 0 ∉ s ∨ 0 ≤ r → ContinuousOn (fun z => z ^ r) s
-- Mathlib.CategoryTheory.GlueData
CategoryTheory.instHasPullbackF' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] (D : CategoryTheory.GlueData' C) (i j k : D.J),
  CategoryTheory.Limits.HasPullback (D.f' i j) (D.f' i k)
-- Mathlib.Data.Set.Functor
Set.seq_eq_set_seq : ∀ {α β : Type u} (s : Set (α → β)) (t : Set α), s <*> t = s.seq t
-- Mathlib.Data.Vector3
_private.Mathlib.Data.Vector3.0.Fin2.toNat.match_1.eq_2 : ∀ (motive : (x : ℕ) → Fin2 x → Sort u_1) (n : ℕ) (i : Fin2 n) (h_1 : (n : ℕ) → motive (n + 1) Fin2.fz)
  (h_2 : (n : ℕ) → (i : Fin2 n) → motive (n + 1) i.fs),
  (match n + 1, i.fs with
    | .(n + 1), Fin2.fz => h_1 n
    | .(n + 1), i.fs => h_2 n i) =
    h_2 n i
-- Lean.Meta.Sym.SymM
/-- Returns maximally shared commonly used terms  -/
Lean.Meta.Sym.getSharedExprs : Lean.Meta.Sym.SymM Lean.Meta.Sym.SharedExprs
-- Mathlib.Geometry.Manifold.StructureGroupoid
StructureGroupoid.symm : ∀ {H : Type u_1} [inst : TopologicalSpace H] (G : StructureGroupoid H) {e : OpenPartialHomeomorph H H},
  e ∈ G → e.symm ∈ G
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.map₁_quotientGroupMk'_epi : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) (S : Subgroup G) [inst_2 : S.Normal]
  [inst_3 : Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)],
  CategoryTheory.Epi (groupHomology.map (QuotientGroup.mk' S) (A.resOfQuotientIso S).inv 1)
-- Mathlib.Topology.ContinuousMap.Algebra
/-- Composition on the left by a (continuous) homomorphism of topological `AddMonoid`s, as an
`AddMonoidHom`. Similar to `AddMonoidHom.comp_left`.  -/
AddMonoidHom.compLeftContinuous : (α : Type u_1) →
  {β : Type u_2} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        {γ : Type u_3} →
          [inst_2 : AddMonoid β] →
            [inst_3 : ContinuousAdd β] →
              [inst_4 : TopologicalSpace γ] →
                [inst_5 : AddMonoid γ] → [inst_6 : ContinuousAdd γ] → (g : β →+ γ) → Continuous ⇑g → C(α, β) →+ C(α, γ)
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.toCharNeTwoNF_s : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [inst_1 : Invertible 2], W.toCharNeTwoNF.s = ⅟2 * -W.a₁
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
AlgebraicGeometry.isCompact_and_isOpen_iff_finite_and_eq_biUnion_affineOpens : ∀ {X : AlgebraicGeometry.Scheme} {U : Set ↥X}, IsCompact U ∧ IsOpen U ↔ ∃ s, s.Finite ∧ U = ⋃ i ∈ s, ↑↑i
-- Mathlib.Topology.EMetricSpace.Diam
/-- The diameter of the empty set vanishes  -/
Metric.ediam_empty : ∀ {X : Type u_2} [inst : PseudoEMetricSpace X], Metric.ediam ∅ = 0
-- Mathlib.Topology.DiscreteQuotient
DiscreteQuotient.instTopologicalSpaceQuotient : {X : Type u_2} → [inst : TopologicalSpace X] → (S : DiscreteQuotient X) → TopologicalSpace (Quotient S.toSetoid)
-- Mathlib.MeasureTheory.Measure.PreVariation
MeasureTheory.preVariationFun_apply : ∀ {X : Type u_1} [inst : MeasurableSpace X] (f : Set X → ENNReal) {s : Set X} (h : MeasurableSet s),
  MeasureTheory.preVariationFun f s = ⨆ P, ∑ p ∈ P.parts, f ↑p
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
/-- Let `{x | p x}` be an additive subsemigroup of an additive commutative monoid `M`. Let
`f : M → N` be a map subadditive on `{x | p x}`, i.e., `p x → p y → f (x + y) ≤ f x + f y`. Let
`g i`, `i ∈ s`, be a nonempty finite family of elements of `M` such that `∀ i ∈ s, p (g i)`. Then
`f (∑ i ∈ s, g i) ≤ ∑ i ∈ s, f (g i)`.  -/
Finset.le_sum_nonempty_of_subadditive_on_pred : ∀ {ι : Type u_1} {M : Type u_4} {N : Type u_5} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N] [inst_2 : Preorder N]
  [IsOrderedAddMonoid N] (f : M → N) (p : M → Prop),
  (∀ (x y : M), p x → p y → f (x + y) ≤ f x + f y) →
    (∀ (x y : M), p x → p y → p (x + y)) →
      ∀ (g : ι → M) (s : Finset ι), s.Nonempty → (∀ i ∈ s, p (g i)) → f (∑ i ∈ s, g i) ≤ ∑ i ∈ s, f (g i)
-- Lean.DocString.Types
Lean.Doc.Inline.link.injEq : ∀ {i : Type u} (content : Array (Lean.Doc.Inline i)) (url : String) (content_1 : Array (Lean.Doc.Inline i))
  (url_1 : String),
  (Lean.Doc.Inline.link content url = Lean.Doc.Inline.link content_1 url_1) = (content = content_1 ∧ url = url_1)
-- Mathlib.NumberTheory.Padics.PadicNumbers
PadicSeq.norm_one : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)], PadicSeq.norm 1 = 1
-- Mathlib.Algebra.Homology.DerivedCategory.Basic
CategoryTheory.SingleFunctors.postcompIsoOfIso.congr_simp : ∀ {C : Type u_1} {D : Type u_2} {E : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} E] {A : Type u_5}
  [inst_3 : AddMonoid A] [inst_4 : CategoryTheory.HasShift D A] [inst_5 : CategoryTheory.HasShift E A]
  (F : CategoryTheory.SingleFunctors C D A) {G G' : CategoryTheory.Functor D E} (e e_1 : G ≅ G') (e_e : e = e_1)
  [inst_6 : G.CommShift A] [inst_7 : G'.CommShift A] [inst_8 : CategoryTheory.NatTrans.CommShift e.hom A],
  F.postcompIsoOfIso e = F.postcompIsoOfIso e_1
-- Mathlib.Algebra.Group.Action.Sigma
Sigma.instFaithfulSMulOfNonempty : ∀ {ι : Type u_1} {M : Type u_2} {α : ι → Type u_4} [inst : (i : ι) → SMul M (α i)] [Nonempty ι]
  [∀ (i : ι), FaithfulSMul M (α i)], FaithfulSMul M ((i : ι) × α i)
-- Mathlib.RingTheory.WittVector.Basic
/-- `f : α → β` induces a map from `𝕎 α` to `𝕎 β` by applying `f` componentwise.
If `f` is a ring homomorphism, then so is `f`, see `WittVector.map f`.  -/
WittVector.mapFun : {p : ℕ} → {α : Type u_3} → {β : Type u_4} → (α → β) → WittVector p α → WittVector p β
-- Mathlib.Algebra.QuadraticAlgebra.Defs
/-- `QuadraticAlgebra.im` as a `LinearMap`  -/
QuadraticAlgebra.imₗ : {R : Type u_1} → (a b : R) → [inst : Semiring R] → QuadraticAlgebra R a b →ₗ[R] R
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.entryAtIdx.eq_1 : ∀ {α : Type u} {β : α → Type v} (x size : ℕ) (k : α) (v : β k) (l' r' : Std.DTreeMap.Internal.Impl α β)
  (hl : (Std.DTreeMap.Internal.Impl.inner size k v l' r').Balanced)
  (x_1 : x < (Std.DTreeMap.Internal.Impl.inner size k v l' r').size),
  (Std.DTreeMap.Internal.Impl.inner size k v l' r').entryAtIdx hl x x_1 =
    match h : compare x l'.size with
    | Ordering.lt => l'.entryAtIdx ⋯ x ⋯
    | Ordering.eq => ⟨k, v⟩
    | Ordering.gt => r'.entryAtIdx ⋯ (x - l'.size - 1) ⋯
-- Mathlib.Algebra.Group.Hom.Defs
AddHom.ext : ∀ {M : Type u_4} {N : Type u_5} [inst : Add M] [inst_1 : Add N] ⦃f g : M →ₙ+ N⦄, (∀ (x : M), f x = g x) → f = g
-- Init.Data.Range.Polymorphic.Map
Std.PRange.UpwardEnumerable.Map.PreservesRxoSize.size_eq : ∀ {α : Type u_1} {β : Type u_2} {inst : Std.PRange.UpwardEnumerable α} {inst_1 : Std.PRange.UpwardEnumerable β}
  {inst_2 : Std.Rxo.HasSize α} {inst_3 : Std.Rxo.HasSize β} {f : Std.PRange.UpwardEnumerable.Map α β}
  [self : f.PreservesRxoSize] {a b : α}, Std.Rxo.HasSize.size a b = Std.Rxo.HasSize.size (f.toFun a) (f.toFun b)
-- Mathlib.Tactic.DeriveTraversable
/-- `mkFunCtor ctor [(true, (arg₁ : m type₁)), (false, (arg₂ : type₂)), (true, (arg₃ : m type₃)),
(false, (arg₄ : type₄))]` makes `fun (x₁ : type₁) (x₃ : type₃) => ctor x₁ arg₂ x₃ arg₄`.  -/
_private.Mathlib.Tactic.DeriveTraversable.0.Mathlib.Deriving.Traversable.traverseConstructor.mkFunCtor : Lean.Name →
  List (Bool × Lean.Expr) →
    optParam (Array Lean.Expr) #[] → optParam (Array Lean.Expr) #[] → Lean.Elab.TermElabM Lean.Expr
-- Init.Data.Nat.Lemmas
Nat.mul_self_lt_mul_self_iff : ∀ {m n : ℕ}, m * m < n * n ↔ m < n
-- Init.Data.Float.Model.Unpacked.Round
/-- Given a finite float represented by a sign, mantissa and exponent,
round it to conform to the given `Format`.

If necessary, this will both decrease and increase the exponent.
 -/
Float.Model.UnpackedFloat.round : Float.Model.Format → Float.Model.UnpackedFloat.Sign → ℕ → ℤ → Float.Model.UnpackedFloat
-- Mathlib.MeasureTheory.Group.MeasurableEquiv
MeasurableEquiv.coe_mulRight : ∀ {G : Type u_1} [inst : Group G] [inst_1 : MeasurableSpace G] [inst_2 : MeasurableMul G] (g : G),
  ⇑(MeasurableEquiv.mulRight g) = fun x => x * g
-- Mathlib.Algebra.Homology.Homotopy
/-- The null homotopic map associated to a family `hom` of morphisms `C_i ⟶ D_j`.
This is the same datum as for the field `hom` in the structure `Homotopy`. For
this definition, we do not need the field `zero` of that structure
as this definition uses only the maps `C_i ⟶ C_j` when `c.Rel j i`.  -/
Homotopy.nullHomotopicMap : {ι : Type u_1} →
  {V : Type u} →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Preadditive V] →
        {c : ComplexShape ι} → {C D : HomologicalComplex V c} → ((i j : ι) → C.X i ⟶ D.X j) → (C ⟶ D)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.toReal_coe_eq_self_add_two_pi_iff : ∀ {θ : ℝ}, (↑θ).toReal = θ + 2 * Real.pi ↔ θ ∈ Set.Ioc (-3 * Real.pi) (-Real.pi)
-- Mathlib.CategoryTheory.Bicategory.Opposites
Bicategory.Opposite.Hom2.op2'.inj : ∀ {B : Type u} {inst : CategoryTheory.Bicategory B} {a b : Bᵒᵖ} {f g : a ⟶ b} {unop2 unop2_1 : f.unop ⟶ g.unop},
  { unop2 := unop2 } = { unop2 := unop2_1 } → unop2 = unop2_1
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_hom_fst : ∀ {X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst : ∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g] (i : 𝒰.I₀),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso 𝒰 f g i).hom
      (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g) =
    CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Scheme.Pullback.p1 𝒰 f g) (𝒰.f i)
-- Init.Data.String.Pattern.Basic
String.Slice.Pattern.instBEqSearchStep.beq : {s : String.Slice} → String.Slice.Pattern.SearchStep s → String.Slice.Pattern.SearchStep s → Bool
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- The expression for the composition `η ≫ θ`.  -/
Mathlib.Tactic.BicategoryLike.Mor₂.comp : Lean.Expr →
  Option Mathlib.Tactic.BicategoryLike.IsoLift →
    Mathlib.Tactic.BicategoryLike.Mor₁ →
      Mathlib.Tactic.BicategoryLike.Mor₁ →
        Mathlib.Tactic.BicategoryLike.Mor₁ →
          Mathlib.Tactic.BicategoryLike.Mor₂ → Mathlib.Tactic.BicategoryLike.Mor₂ → Mathlib.Tactic.BicategoryLike.Mor₂
-- Mathlib.Control.ULiftable
/-- The most common practical use of `ULiftable` (together with `up`), the function `down.{v}` takes
`x : M.{max u v} (ULift.{v} α)` and lowers it to `M.{u} α`  -/
ULiftable.down : {f : Type u₀ → Type u₁} → {g : Type (max u₀ v) → Type v₁} → [ULiftable f g] → {α : Type u₀} → g (ULift.{v, u₀} α) → f α
-- Mathlib.NumberTheory.LSeries.Basic
/-- The value of the L-series of the sequence `f` at the point `s`
if it converges absolutely there, and `0` otherwise.  -/
LSeries.notation.termL : Lean.ParserDescr
-- Mathlib.Data.Set.Card
Set.ncard_preimage_of_injective_subset_range : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set β},
  Function.Injective f → s ⊆ Set.range f → (f ⁻¹' s).ncard = s.ncard
-- Init.Data.List.TakeDrop
List.drop_eq_nil_of_eq_nil : ∀ {α : Type u_1} {as : List α} {i : ℕ}, as = [] → List.drop i as = []
-- Mathlib.GroupTheory.Perm.Fin
cycleType_finRotate : ∀ {n : ℕ}, (finRotate (n + 2)).cycleType = {n + 2}
-- Init.Data.Int.Order
Int.natAbs_eq : ∀ (a : ℤ), a = ↑a.natAbs ∨ a = -↑a.natAbs
-- Mathlib.Geometry.Euclidean.Projection
/-- Reflecting twice in the same subspace.  -/
EuclideanGeometry.reflection_reflection : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] [inst_3 : MetricSpace P] [inst_4 : NormedAddTorsor V P] (s : AffineSubspace 𝕜 P)
  [inst_5 : Nonempty ↥s] [inst_6 : s.direction.HasOrthogonalProjection] (p : P),
  (EuclideanGeometry.reflection s) ((EuclideanGeometry.reflection s) p) = p
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
Measurable.iff : ∀ {α : Type u_1} [inst : MeasurableSpace α] {p q : α → Prop},
  Measurable p → Measurable q → Measurable fun a => p a ↔ q a
-- Mathlib.Order.CompleteBooleanAlgebra
/-- The `CompletelyDistribLattice.MinimalAxioms` element corresponding to a frame.  -/
CompletelyDistribLattice.MinimalAxioms.of : ∀ {α : Type u} [inst : CompletelyDistribLattice α], CompletelyDistribLattice.MinimalAxioms α
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
/-- Every element of `⨂[R] i, s i` has a lift in `FreeAddMonoid (R × Π i, s i)`.
 -/
PiTensorProduct.nonempty_lifts : ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)]
  [inst_2 : (i : ι) → Module R (s i)] (x : PiTensorProduct R fun i => s i), x.lifts.Nonempty
-- Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian
/-- The counit isomorphism induced by `N₁Γ₀`  -/
CategoryTheory.Idempotents.DoldKan.η : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.IsIdempotentComplete C] →
        [inst_3 : CategoryTheory.Limits.HasFiniteCoproducts C] →
          CategoryTheory.Idempotents.DoldKan.Γ.comp CategoryTheory.Idempotents.DoldKan.N ≅
            CategoryTheory.Functor.id (ChainComplex C ℕ)
-- Init.Data.Vector.OfFn
_private.Init.Data.Vector.OfFn.0.Vector.ofFnM.go.congr_simp : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} {n : ℕ} [inst : Monad m] (f f_1 : Fin n → m α),
  f = f_1 →
    ∀ (i i_1 : ℕ) (e_i : i = i_1) (h' : i ≤ n) (acc acc_1 : Array α) (e_acc : acc = acc_1) (w : acc.size = i),
      Vector.ofFnM.go✝ f i h' acc w = Vector.ofFnM.go✝ f_1 i_1 ⋯ acc_1 ⋯
-- Mathlib.Analysis.Distribution.TestFunction
TestFunction.toBoundedContinuousFunctionCLM_apply : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4} [inst_3 : NormedAddCommGroup F]
  [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace 𝕜 F] {n : ℕ∞} [inst_6 : Algebra ℝ 𝕜] [inst_7 : IsScalarTower ℝ 𝕜 F]
  (x : TestFunction Ω F n),
  (TestFunction.toBoundedContinuousFunctionCLM 𝕜) x = { toFun := ⇑x, continuous_toFun := ⋯, map_bounded' := ⋯ }
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
div_le_iff_le_mul : ∀ {α : Type u} [inst : Group α] [inst_1 : LE α] [MulRightMono α] {a b c : α}, a / c ≤ b ↔ a ≤ b * c
-- Mathlib.Analysis.Quaternion
Quaternion.instInnerProductSpaceReal : InnerProductSpace ℝ (Quaternion ℝ)
-- Mathlib.Data.Finite.Set
Finite.of_injective_finite_range : ∀ {α : Type u} {ι : Sort w} {f : ι → α}, Function.Injective f → ∀ [Finite ↑(Set.range f)], Finite ι
-- Mathlib.AlgebraicGeometry.Modules.Tilde
AlgebraicGeometry.isLocalizing_of_isIso_app_top : ∀ {R : CommRingCat} {M N : TopCat.Sheaf (ModuleCat ↑R) ↑(AlgebraicGeometry.Spec R).toPresheafedSpace} {φ : M ⟶ N},
  CategoryTheory.IsIso (φ.hom.app (Opposite.op ⊤)) →
    AlgebraicGeometry.IsLocalizing M → AlgebraicGeometry.IsLocalizing N → CategoryTheory.IsIso φ
-- Mathlib.Analysis.Convex.Extreme
IsExtreme.rfl : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : SMul 𝕜 E] {A : Set E}, IsExtreme 𝕜 A A
-- Lean.Data.PersistentArray
Lean.mkPersistentArray : {α : Type u} → ℕ → α → Lean.PArray α
-- Mathlib.LinearAlgebra.Matrix.WithConv
intrinsicStar_def : ∀ {m : Type u_1} {n : Type u_2} {α : Type u_3} [inst : Star α] (x : WithConv (Matrix m n α)),
  star x = WithConv.toConv (x.ofConv.map star)
-- Std.Time.Date.Unit.Weekday
Std.Time.instReprWeekday : Repr Std.Time.Weekday
-- Mathlib.Topology.MetricSpace.Isometry
Isometry.isometryEquivOnRange_apply : ∀ {α : Type u} {β : Type v} [inst : EMetricSpace α] [inst_1 : PseudoEMetricSpace β] {f : α → β} (h : Isometry f)
  (a : α), h.isometryEquivOnRange a = ⟨f a, ⋯⟩
-- Init.Data.List.Range
List.range_loop_range' : ∀ (s n : ℕ), List.range.loop s (List.range' s n) = List.range' 0 (n + s)
-- Mathlib.Order.Grade
/-- An `𝕆`-graded order where maximal elements have maximal grades.  -/
GradeMaxOrder : (𝕆 : Type u_5) → (α : Type u_6) → [Preorder 𝕆] → [Preorder α] → Type (max u_5 u_6)
-- Init.Data.List.Lemmas
List.nil_of_isEmpty : ∀ {α : Type u_1} {l : List α}, l.isEmpty = true → l = []
-- Mathlib.Algebra.Category.Ring.Basic
/-- **Alias** of `CategoryTheory.ConcreteCategory.forget_map_eq_ofHom`. -/
CommSemiRingCat.forget_map : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {FC : outParam (C → C → Type u_2)}
  {CC : outParam (C → Type w)} [inst_1 : outParam ((X Y : C) → FunLike (FC X Y) (CC X) (CC Y))]
  [inst_2 : CategoryTheory.ConcreteCategory C FC] {X Y : C} (f : X ⟶ Y),
  (CategoryTheory.forget C).map f = TypeCat.ofHom ⇑(CategoryTheory.ConcreteCategory.hom f)