mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.Module.Archimedean
ArchimedeanClass.mk_le_mk_smul : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] {K : Type u_2}
  [inst_3 : Ring K] [inst_4 : LinearOrder K] [IsOrderedRing K] [Archimedean K] [inst_7 : Module K M] [PosSMulMono K M]
  (a : M) (k : K), ArchimedeanClass.mk a ≤ ArchimedeanClass.mk (k • a)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransform.category_comp_base : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆}
  [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  {X Y Z : CategoryTheory.Limits.CatCospanTransform F G F' G'}
  (α : CategoryTheory.Limits.CatCospanTransformMorphism X Y) (β : CategoryTheory.Limits.CatCospanTransformMorphism Y Z),
  (CategoryTheory.CategoryStruct.comp α β).base = CategoryTheory.CategoryStruct.comp α.base β.base
-- Mathlib.RingTheory.PrincipalIdealDomain
/-- A version of Bézout's lemma for greatest common divisors over arbitrary `Finset`s.  -/
Finset.gcd_eq_sum_mul : ∀ {R : Type u} {α : Type u_1} [inst : CommRing R] [IsBezout R] [inst_2 : NormalizedGCDMonoid R] (s : Finset α)
  (f : α → R), ∃ g, s.gcd f = ∑ a ∈ s, f a * g a
-- Mathlib.Topology.Closure
interior_compl : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, interior sᶜ = (closure s)ᶜ
-- Init.Grind.ToIntLemmas
Lean.Grind.IntInterval.lo?.eq_1 : ∀ (lo hi : ℤ), (Lean.Grind.IntInterval.co lo hi).lo? = some lo
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
/-- The first projection functor.  -/
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.fst : {A : Type u₁} →
  {B : Type u₂} →
    {C : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} A] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            {F : CategoryTheory.Functor A B} →
              {G : CategoryTheory.Functor C B} →
                {X : Type u₄} →
                  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] →
                    CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X → CategoryTheory.Functor X A
-- Lean.DocString.Extension
/-- Saved data that describes a custom block element.

The type of value contained within the `Dynamic` determines the interpretation of the custom
element, including how it is rendered to Markdown for the language server.
 -/
Lean.ElabBlock : Type
-- Mathlib.CategoryTheory.Limits.HasLimits
/-- If `t.op : Cocone F.op` is a colimit cocone, then `t : Cone F` is a limit cone.  -/
CategoryTheory.Limits.isLimitOfOp : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {F : CategoryTheory.Functor J C} →
          {t : CategoryTheory.Limits.Cone F} → CategoryTheory.Limits.IsColimit t.op → CategoryTheory.Limits.IsLimit t
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.unop_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (X Y : Cᵒᵖ), Quiver.Hom.unop 0 = 0
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.Mod.comp_hom' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D]
  {A : C} [inst_4 : CategoryTheory.MonObj A] {M N K : CategoryTheory.Mod D A} (f : M ⟶ N) (g : N ⟶ K),
  (CategoryTheory.CategoryStruct.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom
-- Mathlib.LinearAlgebra.Lagrange
Polynomial.eq_of_degree_sub_lt_of_eval_finset_eq : ∀ {R : Type u_1} [inst : CommRing R] [IsDomain R] {f g : Polynomial R} (s : Finset R),
  (f - g).degree < ↑s.card → (∀ x ∈ s, Polynomial.eval x f = Polynomial.eval x g) → f = g
-- Mathlib.CategoryTheory.Triangulated.Opposite.OpOp
CategoryTheory.Pretriangulated.instCommShiftOppositeInverseOpOpEquivalenceInt : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.HasShift C ℤ] → (CategoryTheory.opOpEquivalence C).inverse.CommShift ℤ
-- Aesop.Forward.Substitution
/-- Insert the mapping `li ↦ inst` into the substitution `s`. Precondition: `li`
is in the domain of `s` and `inst` is normalised.  -/
Aesop.Substitution.insertLevel : Aesop.LevelIndex → Lean.Level → Aesop.Substitution → Aesop.Substitution
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.instSemigroup : {X : Type u_1} → {Y : Type u_2} → [inst : TopologicalSpace X] → [Semigroup Y] → Semigroup (LocallyConstant X Y)
-- Init.Data.String.Substring
Substring.Raw.Internal.frontImpl : Substring.Raw → Char
-- Std.Data.TreeSet.Basic
Std.TreeSet.instDecidableMem : {α : Type u} → {cmp : α → α → Ordering} → {m : Std.TreeSet α cmp} → {a : α} → Decidable (a ∈ m)
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
PresheafOfModules.forgetToPresheafModuleCat_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (X : Cᵒᵖ)
  (hX : CategoryTheory.Limits.IsInitial X) (M : PresheafOfModules R),
  (PresheafOfModules.forgetToPresheafModuleCat X hX).obj M = PresheafOfModules.forgetToPresheafModuleCatObj X hX M
-- Mathlib.Algebra.Ring.CharZero
nat_mul_inj : ∀ {R : Type u_2} [inst : NonAssocRing R] [NoZeroDivisors R] [CharZero R] {n : ℕ} {a b : R},
  ↑n * a = ↑n * b → n = 0 ∨ a = b
-- Mathlib.CategoryTheory.Limits.Cones
/-- To give an isomorphism between cones, it suffices to give an
isomorphism between their vertices which commutes with the cone maps.  -/
CategoryTheory.Limits.Cone.ext : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          {c c' : CategoryTheory.Limits.Cone F} →
            (φ : c.pt ≅ c'.pt) →
              autoParam (∀ (j : J), c.π.app j = CategoryTheory.CategoryStruct.comp φ.hom (c'.π.app j))
                  CategoryTheory.Limits.Cone.ext._auto_1 →
                (c ≅ c')
-- Mathlib.Algebra.Order.Kleene
kstar_idem : ∀ {α : Type u_1} [inst : KleeneAlgebra α] (a : α), KStar.kstar (KStar.kstar a) = KStar.kstar a
-- Mathlib.RingTheory.OrderOfVanishing.Basic
Ring.ord_one : ∀ (R : Type u_1) [inst : Ring R], Ring.ord R 1 = 0
-- Mathlib.Analysis.Convex.Gauge
gauge_smul_of_nonneg : ∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {α : Type u_3} [inst_2 : Field α]
  [inst_3 : LinearOrder α] [IsStrictOrderedRing α] [inst_5 : MulActionWithZero α ℝ] [IsStrictOrderedModule α ℝ]
  [inst_7 : MulActionWithZero α E] [IsScalarTower α ℝ (Set E)] {s : Set E} {a : α},
  0 ≤ a → ∀ (x : E), gauge s (a • x) = a • gauge s x
-- Mathlib.RingTheory.Ideal.MinimalPrime.Localization
IsLocalization.minimalPrimes_map : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) (A : Type u_2) [inst_1 : CommSemiring A]
  [inst_2 : Algebra R A] [IsLocalization S A] (J : Ideal R),
  (Ideal.map (algebraMap R A) J).minimalPrimes = Ideal.under R ⁻¹' J.minimalPrimes
-- Mathlib.RingTheory.WittVector.MulP
_private.Mathlib.RingTheory.WittVector.MulP.0.WittVector.wittMulN.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match n.succ with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_2 n
-- Mathlib.Order.Hom.Basic
/-- The order isomorphism between a type and its double dual.  -/
OrderIso.dualDual : (α : Type u_2) → [inst : LE α] → α ≃o αᵒᵈᵒᵈ
-- Mathlib.CategoryTheory.Sites.ConcreteSheafification
CategoryTheory.GrothendieckTopology.Plus.mk.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w}
  [inst_1 : CategoryTheory.Category.{w', w} D] {FD : D → D → Type u_1} {CD : D → Type t}
  [inst_2 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [instCC : CategoryTheory.ConcreteCategory D FD]
  [inst_3 :
    ∀ {X : C} (S : J.Cover X),
      CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan S.shape)
        (CategoryTheory.forget D)]
  [inst_4 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
  [inst_5 :
    ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  {X : C} {P : CategoryTheory.Functor Cᵒᵖ D} {S : J.Cover X} (x x_1 : CategoryTheory.Meq P S),
  x = x_1 → CategoryTheory.GrothendieckTopology.Plus.mk x = CategoryTheory.GrothendieckTopology.Plus.mk x_1
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.top_mul : ∀ {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData), ⊤ * I = I
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
/-- The universal property of an additive free group: A function from the generators of `G` to
another additive group extends in a unique way to a homomorphism from `G`.

Note that since `IsFreeAddGroup.lift` is expressed as a bijection, it already
expresses the universal property.  -/
IsFreeAddGroup.unique_lift : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : IsFreeAddGroup G] {H : Type u_2} [inst_2 : AddGroup H]
  (f : IsFreeAddGroup.Generators G → H), ∃! F, ∀ (a : IsFreeAddGroup.Generators G), F (IsFreeAddGroup.of a) = f a
-- Mathlib.Data.Finsupp.Order
Finsupp.le_iff : ∀ {ι : Type u_1} {α : Type u_3} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [CanonicallyOrderedAdd α]
  (f g : ι →₀ α), f ≤ g ↔ ∀ i ∈ f.support, f i ≤ g i
-- Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover
TopCat.Presheaf.generateEquivalenceOpensLe_inverse'_map : ∀ {X : TopCat} {ι : Type u_2} (U : ι → TopologicalSpace.Opens ↑X) {Y : TopologicalSpace.Opens ↑X} (hY : Y = iSup U)
  {X_1 Y_1 : TopCat.Presheaf.SheafCondition.OpensLeCover U} (g : X_1 ⟶ Y_1),
  (TopCat.Presheaf.generateEquivalenceOpensLe_inverse' U hY).map g =
    CategoryTheory.ObjectProperty.homMk (CategoryTheory.Over.homMk g.hom ⋯)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SignatureHelpTriggerKind.invoked : Lean.Lsp.SignatureHelpTriggerKind
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma
Finpartition.energy.congr_simp : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} (P P_1 : Finpartition s),
  P = P_1 →
    ∀ (G G_1 : SimpleGraph α),
      G = G_1 → ∀ {inst_1 : DecidableRel G.Adj} [inst_2 : DecidableRel G_1.Adj], P.energy G = P_1.energy G_1
-- Mathlib.NumberTheory.WellApproximable
approxOrderOf.eq_1 : ∀ (A : Type u_1) [inst : SeminormedGroup A] (n : ℕ) (δ : ℝ),
  approxOrderOf A n δ = Metric.thickening δ {y | orderOf y = n}
-- Init.Data.String.Decode
ByteArray.le_size_of_utf8DecodeChar?_eq_some : ∀ {b : ByteArray} {i : ℕ} {c : Char}, b.utf8DecodeChar? i = some c → i + c.utf8Size ≤ b.size
-- Init.Data.Option.Lemmas
Option.forall_ne_none : ∀ {α : Type u_1} {p : Option α → Prop}, (∀ (x : Option α), x ≠ none → p x) ↔ ∀ (x : α), p (some x)
-- Mathlib.Analysis.Normed.Order.UpperLower
IsLowerSet.cthickening : ∀ {α : Type u_1} [inst : NormedAddCommGroup α] [inst_1 : Preorder α] [IsOrderedAddMonoid α] {s : Set α},
  IsLowerSet s → ∀ (ε : ℝ), IsLowerSet (Metric.cthickening ε s)
-- Mathlib.Algebra.Homology.ShortComplex.ModuleCat
CategoryTheory.ShortComplex.toCycles_moduleCatCyclesIso_hom_assoc_apply : ∀ {R : Type u} [inst : Ring R] (S : CategoryTheory.ShortComplex (ModuleCat R)) {Z : ModuleCat R}
  (h : S.moduleCatLeftHomologyData.K ⟶ Z) (x : ↑S.X₁),
  (CategoryTheory.ConcreteCategory.hom h)
      ((CategoryTheory.ConcreteCategory.hom S.moduleCatCyclesIso.hom)
        ((CategoryTheory.ConcreteCategory.hom S.toCycles) x)) =
    (CategoryTheory.ConcreteCategory.hom h) (S.moduleCatToCycles x)
-- Mathlib.Algebra.Group.Action.Hom
AddAction.compHom_vadd_def : ∀ {E : Type u_4} {F : Type u_5} {G : Type u_6} [inst : AddMonoid E] [inst_1 : AddMonoid F] [inst_2 : AddAction F G]
  (f : E →+ F) (a : E) (x : G), a +ᵥ x = f a +ᵥ x
-- Mathlib.LinearAlgebra.Basis.Prod
Module.Basis.prod_repr_inl : ∀ {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [inst : Semiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : AddCommMonoid M'] [inst_4 : Module R M']
  (b : Module.Basis ι R M) (b' : Module.Basis ι' R M') (x : M × M') (i : ι),
  ((b.prod b').repr x) (Sum.inl i) = (b.repr x.1) i
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
measurable_of_continuousOn_compl_singleton : ∀ {α : Type u_1} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [OpensMeasurableSpace α]
  [inst_3 : TopologicalSpace γ] [inst_4 : MeasurableSpace γ] [BorelSpace γ] [T1Space α] {f : α → γ} (a : α),
  ContinuousOn f {a}ᶜ → Measurable f
-- Std.Internal.Parsec.ByteArray
/-- Skips while a predicate is satisfied.
Fails with `.eof` if input ends while the predicate still holds.
 -/
Std.Internal.Parsec.ByteArray.skipWhile : (UInt8 → Bool) → Std.Internal.Parsec.ByteArray.Parser Unit
-- Init.Data.Option.Lemmas
Option.bind_eq_bind : ∀ {α β : Type u_1}, bind = Option.bind
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.min!_eq_head!_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α],
  t.min! = t.toList.head!
-- Mathlib.Computability.Primrec.Basic
Primrec₂.nat_iff : ∀ {α : Type u_1} {β : Type u_2} {σ : Type u_3} [inst : Primcodable α] [inst_1 : Primcodable β] [inst_2 : Primcodable σ]
  {f : α → β → σ},
  Primrec₂ f ↔
    Nat.Primrec
      (Nat.unpaired fun m n =>
        Encodable.encode ((Encodable.decode m).bind fun a => Option.map (f a) (Encodable.decode n)))
-- Mathlib.Topology.UniformSpace.Equicontinuity
equicontinuousOn_iInf_rng : ∀ {ι : Type u_1} {κ : Type u_2} {X : Type u_3} {α' : Type u_7} [tX : TopologicalSpace X] {u : κ → UniformSpace α'}
  {F : ι → X → α'} {S : Set X}, EquicontinuousOn F S ↔ ∀ (k : κ), EquicontinuousOn F S
-- Lean.Elab.PreDefinition.FixedParams
/-- If `xs` are the fixed parameters that are in scope, and `toErase` are, for each function, the
positions of arguments that must no longer be fixed parameters, then this function splits partitions
`xs` into those to keep and those to erase, and updates `FixedParams` accordingly.

This is used in structural recursion, where we may discover that some fixed parameters are actually
indices and need to be treated as varying, including all parameters that depend on them.
 -/
Lean.Elab.FixedParamPerms.erase : Lean.Elab.FixedParamPerms →
  Array Lean.Expr → Array (Array ℕ) → Lean.Elab.FixedParamPerms × Array Lean.Expr × Array Lean.FVarId
-- Mathlib.Computability.RecursiveIn
Nat.RecursiveIn.comp : ∀ {O : Set (ℕ →. ℕ)} {f h : ℕ →. ℕ}, Nat.RecursiveIn O f → Nat.RecursiveIn O h → Nat.RecursiveIn O fun n => h n >>= f
-- Mathlib.Algebra.Category.Grp.Limits
AddCommGrpCat.addCommGroupObj : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J AddCommGrpCat) →
      (j : J) → AddCommGroup ((F.comp (CategoryTheory.forget AddCommGrpCat)).obj j)
-- Mathlib.Order.Defs.Unbundled
/-- **Alias** of `Std.Asymm.irrefl`. -/
IsAsymm.isIrrefl : ∀ {α : Sort u_1} {r : α → α → Prop} [Std.Asymm r], Std.Irrefl r
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
Sum.elim.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {γ : Sort u_3} (f : α → γ) (g : β → γ) (x : α ⊕ β), Sum.elim f g x = Sum.casesOn x f g
-- Mathlib.Data.Finsupp.Single
Finsupp.instNontrivial : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] [Nonempty α] [Nontrivial M], Nontrivial (α →₀ M)
-- Mathlib.GroupTheory.GroupAction.Primitive
/-- An action is preprimitive if it is pretransitive and
the only blocks are the trivial ones  -/
AddAction.IsPreprimitive.isTrivialBlock_of_isBlock : ∀ {G : Type u_1} {X : Type u_2} {inst : VAdd G X} [self : AddAction.IsPreprimitive G X] {B : Set X},
  AddAction.IsBlock G B → AddAction.IsTrivialBlock B
-- Mathlib.Algebra.MonoidAlgebra.Degree
AddMonoidAlgebra.leadingCoeff_add_eq_left : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_5} [inst : Semiring R] [inst_1 : LinearOrder B] [inst_2 : OrderBot B]
  {p q : AddMonoidAlgebra R A} {D : A → B} [inst_3 : AddZeroClass A],
  AddMonoidAlgebra.supDegree D q < AddMonoidAlgebra.supDegree D p →
    AddMonoidAlgebra.leadingCoeff D (p + q) = AddMonoidAlgebra.leadingCoeff D p
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometry.map_neg : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup E₂] [inst_4 : Module R E]
  [inst_5 : Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) (x : E), f (-x) = -f x
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
/-- If `X` is a simplicial set, then the empty subcomplex of `X` is an initial
object in `SSet`.  -/
SSet.Subcomplex.isInitialBot : {X : SSet} → CategoryTheory.Limits.IsInitial ⊥.toSSet
-- Mathlib.Data.Vector3
exists_vector_zero : ∀ {α : Type u_1} (f : Vector3 α 0 → Prop), Exists f ↔ f []
-- Mathlib.CategoryTheory.EqToHom
CategoryTheory.eqToIso_map_trans : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X Y Z : C} (p : X = Y) (q : Y = Z),
  F.mapIso (CategoryTheory.eqToIso p) ≪≫ F.mapIso (CategoryTheory.eqToIso q) = F.mapIso (CategoryTheory.eqToIso ⋯)
-- Mathlib.RingTheory.NonUnitalSubring.Defs
NonUnitalSubring.val_mul : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] (s : NonUnitalSubring R) (x y : ↥s), ↑(x * y) = ↑x * ↑y
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.power_natCast : ∀ (a : Cardinal.{u}) (n : ℕ), a ^ ↑n = a ^ n
-- Mathlib.Data.Finite.Prod
Set.Infinite.image2_left : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {s : Set α} {t : Set β} {b : β},
  s.Infinite → b ∈ t → Set.InjOn (fun a => f a b) s → (Set.image2 f s t).Infinite
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.forIn_eq_forIn_toList : ∀ {α : Type u} {δ : Type w} {m' : Type w → Type w'} {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [inst : Monad m'] [LawfulMonad m'] {f : α → β → δ → m' (ForInStep δ)} {init : δ},
  Std.DHashMap.Raw.forIn f init ↑m = forIn (Std.DHashMap.Raw.Const.toList ↑m) init fun a b => f a.1 a.2 b
-- Mathlib.Order.Atoms
IsSimpleOrder.instComplementedLattice : ∀ {α : Type u_2} [inst : Lattice α] [inst_1 : BoundedOrder α] [IsSimpleOrder α], ComplementedLattice α
-- Init.Data.List.ToArray
List.forM_toArray : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} [inst : Monad m] (l : List α) (f : α → m PUnit.{u_1 + 1}),
  forM l.toArray f = l.forM f
-- Std.Data.Internal.List.Associative
Std.Internal.List.Option.filter_false : ∀ {α : Type u} {o : Option α}, Option.filter (fun x => false) o = none
-- Mathlib.Order.Filter.Subsingleton
Filter.Subsingleton.isCountablyGenerated : ∀ {α : Type u_1} {l : Filter α}, l.Subsingleton → l.IsCountablyGenerated
-- Mathlib.CategoryTheory.MorphismProperty.WeakFactorizationSystem
CategoryTheory.MorphismProperty.rlp_eq_of_wfs : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W₁ W₂ : CategoryTheory.MorphismProperty C)
  [W₁.IsWeakFactorizationSystem W₂], W₁.rlp = W₂
-- Std.Data.ExtHashMap.Basic
/-- Returns `true` if the hash map contains no mappings.

Note that if your `BEq` instance is not reflexive or your `Hashable` instance is not
lawful, then it is possible that this function returns `false` even though is not possible
to get anything out of the hash map.
 -/
Std.ExtHashMap.isEmpty : {α : Type u} →
  {β : Type v} → {x : BEq α} → {x_1 : Hashable α} → [EquivBEq α] → [LawfulHashable α] → Std.ExtHashMap α β → Bool
-- Mathlib.GroupTheory.DivisibleHull
DivisibleHull.mk_left_injective : ∀ {M : Type u_1} [inst : AddCommMonoid M] [IsAddTorsionFree M] (s : ℕ+),
  Function.Injective fun m => DivisibleHull.mk m s
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Finite
CategoryTheory.Limits.compCreatesFiniteProducts : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {E : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} E] →
            (F : CategoryTheory.Functor C D) →
              (G : CategoryTheory.Functor D E) →
                [CategoryTheory.Limits.CreatesFiniteProducts F] →
                  [CategoryTheory.Limits.CreatesFiniteProducts G] →
                    CategoryTheory.Limits.CreatesFiniteProducts (F.comp G)
-- Init.Data.Vector.Basic
/-- The vector `#v[start, start + step, start + 2 * step, ..., start + (size - 1) * step]`.  -/
Vector.range' : ℕ → (size : ℕ) → optParam ℕ 1 → Vector ℕ size
-- Plausible.Sampleable
Plausible.SampleableExt.proxy : (α : Sort u) → [self : Plausible.SampleableExt α] → Type v
-- Mathlib.CategoryTheory.Presentable.OrthogonalReflection
CategoryTheory.OrthogonalReflection.D₁.hasCoproductsOfShape : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) (Z : C)
  [CategoryTheory.MorphismProperty.IsSmall.{w, v, u} W] [CategoryTheory.LocallySmall.{w, v, u} C]
  [CategoryTheory.Limits.HasCoproducts C],
  CategoryTheory.Limits.HasCoproductsOfShape (CategoryTheory.OrthogonalReflection.D₁ W Z) C
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
WeierstrassCurve.Jacobian.smul_equiv_smul : ∀ {R : Type r} [inst : CommRing R] (P Q : Fin 3 → R) {u v : R}, IsUnit u → IsUnit v → (u • P ≈ v • Q ↔ P ≈ Q)
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
MeasureTheory.isProbabilityMeasure_join : ∀ {α : Type u_1} [inst : MeasurableSpace α] {m : MeasureTheory.Measure (MeasureTheory.Measure α)}
  [MeasureTheory.IsProbabilityMeasure m],
  (∀ᵐ (μ : MeasureTheory.Measure α) ∂m, MeasureTheory.IsProbabilityMeasure μ) →
    MeasureTheory.IsProbabilityMeasure m.join
-- Mathlib.Algebra.Algebra.Defs
algebraMap.coe_smul' : ∀ {A : Type u_1} {B : Type u_2} (a : A) (b : B) (C : Type u_3) [inst : SMul A B] [inst_1 : CommSemiring B]
  [inst_2 : Semiring C] [inst_3 : Algebra B C] [inst_4 : Monoid A] [inst_5 : MulDistribMulAction A C]
  [SMulDistribClass A B C], ↑(a • b) = a • ↑b
-- Mathlib.Data.Set.Lattice
Set.sInter_insert : ∀ {α : Type u_1} (s : Set α) (T : Set (Set α)), ⋂₀ insert s T = s ∩ ⋂₀ T
-- Lean.Data.Options
Lean.instInhabitedOptionDeprecation : Inhabited Lean.OptionDeprecation
-- Mathlib.Topology.Inseparable
Inseparable.map_of_continuousWithinAt : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {x y : X} {f : X → Y}
  {s t : Set X},
  Inseparable x y → ContinuousWithinAt f s x → ContinuousWithinAt f t y → x ∈ t → y ∈ s → Inseparable (f x) (f y)
-- Aesop.Stats.Basic
/-- Number of fvars in the local context, excluding implementation detail
fvars.  -/
Aesop.GoalStats.lctxSize : Aesop.GoalStats → ℕ
-- Mathlib.Order.SymmDiff
bihimp_eq_inf : ∀ {α : Type u_2} [inst : BooleanAlgebra α] (a b : α), bihimp a b = a ⊓ b ↔ Codisjoint a b
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.eventually_div_right_iff : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [MeasurableMul G] (μ : MeasureTheory.Measure G)
  [μ.IsMulRightInvariant] (t : G) {p : G → Prop}, (∀ᵐ (x : G) ∂μ, p (x / t)) ↔ ∀ᵐ (x : G) ∂μ, p x
-- Mathlib.CategoryTheory.Preadditive.Mat
CategoryTheory.Functor.mapMat__map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C] {D : Type u_1}
  [inst_2 : CategoryTheory.Category.{v₁, u_1} D] [inst_3 : CategoryTheory.Preadditive D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.Additive] {X Y : CategoryTheory.Mat_ C} (f : X ⟶ Y)
  (i : { ι := X.ι, fintype := X.fintype, X := fun i => F.obj (X.X i) }.ι)
  (j : { ι := Y.ι, fintype := Y.fintype, X := fun i => F.obj (Y.X i) }.ι), F.mapMat_.map f i j = F.map (f i j)