mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Matrix.ToLin
isStablyFiniteRing_iff_injective_of_surjective : ∀ {A : Type u_3} [inst : Semiring A],
  IsStablyFiniteRing A ↔ ∀ (n : ℕ) (f : Module.End A (Fin n → A)), Function.Surjective ⇑f → Function.Injective ⇑f
-- Mathlib.Algebra.Order.GroupWithZero.Defs
mul_le_of_mul_le_of_nonneg_left : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] {a b c d : α} [PosMulMono α],
  a * b ≤ c → d ≤ b → 0 ≤ a → a * d ≤ c
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- A cone postcomposed with the inverse of a natural isomorphism is a limit cone
if and only if the original cone is.
 -/
CategoryTheory.Limits.IsLimit.postcomposeInvEquiv : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F G : CategoryTheory.Functor J C} →
          (α : F ≅ G) →
            (c : CategoryTheory.Limits.Cone G) →
              CategoryTheory.Limits.IsLimit ((CategoryTheory.Limits.Cone.postcompose α.inv).obj c) ≃
                CategoryTheory.Limits.IsLimit c
-- Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic
ProbabilityTheory.HasIndepIncrements.indepFun_sub_sub : ∀ {T : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : T → Ω → E}
  [inst : Preorder T] [inst_1 : MeasurableSpace E] [inst_2 : Sub E],
  ProbabilityTheory.HasIndepIncrements X P →
    ∀ {r s t : T}, r ≤ s → s ≤ t → ProbabilityTheory.IndepFun (X s - X r) (X t - X s) P
-- Mathlib.Analysis.Normed.Ring.Lemmas
SeparationQuotient.instNormedCommRing : {α : Type u_1} → [inst : SeminormedCommRing α] → NormedCommRing (SeparationQuotient α)
-- Mathlib.Data.Bool.Basic
Bool.or_inr : ∀ {a b : Bool}, b = true → (a || b) = true
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.instFaithfulIncl : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C], (CategoryTheory.Limits.FormalCoproduct.incl C).Faithful
-- Mathlib.Data.PNat.Interval
PNat.card_Ico : ∀ (a b : ℕ+), (Finset.Ico a b).card = ↑b - ↑a
-- Mathlib.MeasureTheory.VectorMeasure.SetIntegral
MeasureTheory.VectorMeasure.setIntegral_indicator : ∀ {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedAddCommGroup G] {μ : MeasureTheory.VectorMeasure X F} {f : X → E}
  {s t : Set X} [inst_3 : NormedSpace ℝ E] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace ℝ G]
  {B : E →L[ℝ] F →L[ℝ] G},
  MeasurableSet s → MeasurableSet t → ∫ᵛ (x : X) in s, t.indicator f x ∂[B; μ] = ∫ᵛ (x : X) in s ∩ t, f x ∂[B; μ]
-- Mathlib.RepresentationTheory.Invariants
Rep.instIsRightAdjointModuleCatInvariantsFunctor : ∀ (k : Type u) (G : Type v) [inst : CommRing k] [inst_1 : Group G], (Rep.invariantsFunctor k G).IsRightAdjoint
-- Mathlib.Analysis.Convex.Gauge
/-- If `s` is a convex neighborhood of the origin in a topological real vector space, then `gauge s`
is continuous. If the ambient space is a normed space, then `gauge s` is Lipschitz continuous, see
`Convex.lipschitz_gauge`.  -/
continuousAt_gauge : ∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {s : Set E} {x : E} [inst_2 : TopologicalSpace E]
  [IsTopologicalAddGroup E] [ContinuousSMul ℝ E], Convex ℝ s → s ∈ nhds 0 → ContinuousAt (gauge s) x
-- Mathlib.Combinatorics.SimpleGraph.VertexCover
SimpleGraph.IsVertexCover.subset : ∀ {V : Type u_1} {G : SimpleGraph V} {c d : Set V}, c ⊆ d → G.IsVertexCover c → G.IsVertexCover d
-- Lean.Meta.Tactic.Grind.Theorems
Lean.Meta.Grind.Origin.stx.sizeOf_spec : ∀ (id : Lean.Name) (ref : Lean.Syntax), sizeOf (Lean.Meta.Grind.Origin.stx id ref) = 1 + sizeOf id + sizeOf ref
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.getNextToResume : Lean.Meta.SynthInstance.SynthM (Lean.Meta.SynthInstance.ConsumerNode × Lean.Meta.SynthInstance.Answer)
-- Mathlib.Geometry.RingedSpace.PresheafedSpace
AlgebraicGeometry.PresheafedSpace.toRestrictTop_base : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : AlgebraicGeometry.PresheafedSpace C),
  X.toRestrictTop.base = (TopologicalSpace.Opens.inclusionTopIso ↑X).inv
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.constLinearEquivOfIsEmpty_apply : ∀ {ι : Type u_7} {R' : Type u_10} {M'' : Type u_11} {N'' : Type u_13} [inst : CommSemiring R']
  [inst_1 : AddCommMonoid M''] [inst_2 : AddCommMonoid N''] [inst_3 : Module R' M''] [inst_4 : Module R' N'']
  [inst_5 : IsEmpty ι] (m : N''), AlternatingMap.constLinearEquivOfIsEmpty m = AlternatingMap.constOfIsEmpty R' M'' ι m
-- Mathlib.RingTheory.IntegralClosure.Algebra.Basic
RingHom.IsIntegralElem.neg : ∀ {R : Type u_1} {S : Type u_4} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) {x : S},
  f.IsIntegralElem x → f.IsIntegralElem (-x)
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoDiv_mul_sub_toIcoMod : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedAddMonoid R]
  [inst_3 : Archimedean R] {p : R} (hp : 0 < p) (a b : R), ↑(toIcoDiv hp a b) * p + toIcoMod hp a b = b
-- Init.Data.UInt.Lemmas
USize.toUInt64_eq_mod_usizeSize_iff : ∀ (a : USize) (b : UInt64), a.toUInt64 = b % UInt64.ofNat USize.size ↔ a = b.toUSize
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.FriendlyOperation.cons : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis} (exp : ℝ)
  (coef : Tactic.ComputeAsymptotics.MultiseriesExpansion basis_tl),
  Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.FriendlyOperation
    (Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.cons exp coef)
-- Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution
DiscreteConvolution.ConvolutionExistsAt.smul_convolution : ∀ {M : Type u_1} {S : Type u_2} {E : Type u_3} {E' : Type u_4} [inst : Monoid M] [inst_1 : CommSemiring S]
  [inst_2 : AddCommMonoid E] [inst_3 : AddCommMonoid E'] [inst_4 : Module S E] [inst_5 : Module S E'] {F : Type u_10}
  [inst_6 : AddCommMonoid F] [inst_7 : Module S F] [inst_8 : TopologicalSpace F] [ContinuousConstSMul S F] [T2Space F]
  {c : S} {f : M → E} {g : M → E'} {x : M} (L : E →ₗ[S] E' →ₗ[S] F),
  DiscreteConvolution.ConvolutionExistsAt L f g x →
    DiscreteConvolution.convolution L (c • f) g x = c • DiscreteConvolution.convolution L f g x
-- Mathlib.CategoryTheory.EquivalenceRelation
CategoryTheory.SymmetricRelation.symmetry₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {R X : C} {p₁ p₂ : R ⟶ X}
  (self : CategoryTheory.SymmetricRelation p₁ p₂), CategoryTheory.CategoryStruct.comp self.s p₂ = p₁
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.mintroPat.quot : Lean.ParserDescr
-- Mathlib.NumberTheory.ArithmeticFunction.Carmichael
ArithmeticFunction.carmichael_lcm : ∀ (a b : ℕ),
  ArithmeticFunction.carmichael (a.lcm b) = (ArithmeticFunction.carmichael a).lcm (ArithmeticFunction.carmichael b)
-- Mathlib.LinearAlgebra.Matrix.Notation
Matrix.vec3_add : ∀ {α : Type u} [inst : Add α] (a₀ a₁ a₂ b₀ b₁ b₂ : α), ![a₀, a₁, a₂] + ![b₀, b₁, b₂] = ![a₀ + b₀, a₁ + b₁, a₂ + b₂]
-- Mathlib.Algebra.Divisibility.Units
isUnit_iff_forall_dvd : ∀ {α : Type u_1} [inst : CommMonoid α] {x : α}, IsUnit x ↔ ∀ (y : α), x ∣ y
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.mk.eq_1 : ∀ {M : Type u_1}, DomMulAct.mk = MulOpposite.opEquiv
-- Std.Data.DHashMap.Internal.Raw
Std.DHashMap.Internal.Raw₀.get!.congr_simp : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] [inst_2 : Hashable α]
  (m m_1 : Std.DHashMap.Internal.Raw₀ α β), m = m_1 → ∀ (a : α) [inst_3 : Inhabited (β a)], m.get! a = m_1.get! a
-- Init.Data.SInt.Lemmas
ISize.two_mul : ∀ {a : ISize}, 2 * a = a + a
-- Std.Net.Addr
Std.Net.IPAddr.v6.injEq : ∀ (addr addr_1 : Std.Net.IPv6Addr), (Std.Net.IPAddr.v6 addr = Std.Net.IPAddr.v6 addr_1) = (addr = addr_1)
-- Mathlib.ModelTheory.Graph
FirstOrder.Language.structure_simpleGraphOfStructure : ∀ {V : Type u} [S : FirstOrder.Language.graph.Structure V] [inst : V ⊨ FirstOrder.Language.Theory.simpleGraph],
  (FirstOrder.Language.simpleGraphOfStructure V).structure = S
-- Init.Data.List.Basic
List.mapTR.loop : {α : Type u} → {β : Type v} → (α → β) → List α → List β → List β
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackFree
/-- The canonical isomorphism `freeFunctor ⋙ pullback φ ≅ freeFunctor` for a
continuous map between ringed sites, when the underlying functor between the sites
is final.  -/
SheafOfModules.freeFunctorCompPullbackIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : CategoryTheory.GrothendieckTopology C} →
          {K : CategoryTheory.GrothendieckTopology D} →
            {F : CategoryTheory.Functor C D} →
              {S : CategoryTheory.Sheaf J RingCat} →
                {R : CategoryTheory.Sheaf K RingCat} →
                  [inst_2 : F.IsContinuous J K] →
                    (φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R) →
                      [inst_3 : (SheafOfModules.pushforward φ).IsRightAdjoint] →
                        [inst_4 : CategoryTheory.HasWeakSheafify J AddCommGrpCat] →
                          [inst_5 : CategoryTheory.HasWeakSheafify K AddCommGrpCat] →
                            [inst_6 : J.WEqualsLocallyBijective AddCommGrpCat] →
                              [inst_7 : K.WEqualsLocallyBijective AddCommGrpCat] →
                                [F.Final] →
                                  SheafOfModules.freeFunctor.comp (SheafOfModules.pullback φ) ≅
                                    SheafOfModules.freeFunctor
-- Mathlib.Data.Rel
SetRel.sUnion_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (ℛ : Set (SetRel α β)) (S : SetRel β γ),
  SetRel.comp (⋃₀ ℛ) S = ⋃ R ∈ ℛ, R.comp S
-- Mathlib.Data.Vector.Basic
/-- The list that makes up a `Vector` made up of a single element,
retrieved via `toList`, is equal to the list of that single element.  -/
List.Vector.toList_singleton : ∀ {α : Type u_1} (v : List.Vector α 1), v.toList = [v.head]
-- Init.Data.Option.Attach
Option.bind_subtype : ∀ {α : Type u_1} {β : Type u_2} {p : α → Prop} {o : Option { x // p x }} {f : { x // p x } → Option β}
  {g : α → Option β}, (∀ (x : α) (h : p x), f ⟨x, h⟩ = g x) → o.bind f = o.unattach.bind g
-- Mathlib.AlgebraicGeometry.Birational.Birational
AlgebraicGeometry.Scheme.Opens.partialIsoOfDense_source : ∀ {X : AlgebraicGeometry.Scheme} (U : X.Opens) (hU : Dense ↑U), (U.partialIsoOfDense hU).source = ⊤
-- Init.Data.Order.PackageFactories
Std.PreorderPackage.decidableLE : {α : Type u} → [self : Std.PreorderPackage α] → DecidableLE α
-- Init.Data.List.Nat.TakeDrop
List.take_replicate : ∀ {α : Type u_1} {a : α} {i n : ℕ}, List.take i (List.replicate n a) = List.replicate (min i n) a
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
/-- If `s` is a compact set and `μ` is a locally finite measure, then `s` admits an open superset of
finite measure.  -/
IsCompact.exists_open_superset_measure_lt_top : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] {s : Set α},
  IsCompact s → ∀ (μ : MeasureTheory.Measure α) [MeasureTheory.IsLocallyFiniteMeasure μ], ∃ U ⊇ s, IsOpen U ∧ μ U < ⊤
-- Mathlib.Algebra.Order.Module.Defs
OrderDual.instPosSMulReflectLT : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : SMul α β] [inst_3 : Zero α]
  [PosSMulReflectLT α β], PosSMulReflectLT α βᵒᵈ
-- Mathlib.CategoryTheory.Category.Quiv
/-- Any prefunctor into a category lifts to a functor from the path category.  -/
CategoryTheory.Quiv.lift : {V : Type u} →
  [inst : Quiver V] →
    {C : Type u₁} →
      [inst_1 : CategoryTheory.Category.{v₁, u₁} C] → V ⥤q C → CategoryTheory.Functor (CategoryTheory.Paths V) C
-- Mathlib.Algebra.Star.StarRingHom
StarRingEquiv.instRingEquivClass : ∀ {A : Type u_1} {B : Type u_2} [inst : Add A] [inst_1 : Add B] [inst_2 : Mul A] [inst_3 : Mul B] [inst_4 : Star A]
  [inst_5 : Star B], RingEquivClass (A ≃⋆+* B) A B
-- Mathlib.Algebra.Field.ModEq
AddCommGroup.mul_modEq_mul_right : ∀ {K : Type u_1} [inst : DivisionSemiring K] {a b c p : K}, c ≠ 0 → (a * c ≡ b * c [PMOD p] ↔ a ≡ b [PMOD p / c])
-- Init.SizeOf
String.Pos.Raw.mk.sizeOf_spec : ∀ (byteIdx : ℕ), sizeOf { byteIdx := byteIdx } = 1 + sizeOf byteIdx
-- Mathlib.Analysis.Analytic.Linear
ContinuousLinearEquiv.analyticAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (f : E ≃L[𝕜] F)
  (x : E), AnalyticAt 𝕜 (⇑f) x
-- Mathlib.MeasureTheory.Measure.AEMeasurable
AEMeasurable.map_add₀ : ∀ {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] {μ ν : MeasureTheory.Measure α}
  {f : α → β},
  AEMeasurable f μ →
    AEMeasurable f ν →
      MeasureTheory.Measure.map f (μ + ν) = MeasureTheory.Measure.map f μ + MeasureTheory.Measure.map f ν
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
LinearIndependent.isCompl_span_image : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M],
  LinearIndependent R v →
    Submodule.span R (Set.range v) = ⊤ →
      ∀ {s t : Set ι}, IsCompl s t → IsCompl (Submodule.span R (v '' s)) (Submodule.span R (v '' t))
-- Mathlib.Algebra.Group.Basic
add_rotate : ∀ {G : Type u_3} [inst : AddCommSemigroup G] (a b c : G), a + b + c = b + c + a
-- Mathlib.Data.Set.Countable
Set.countable_iff_exists_subset_range : ∀ {α : Type u} [Nonempty α] {s : Set α}, s.Countable ↔ ∃ f, s ⊆ Set.range f
-- Init.Data.SInt.Bitwise
ISize.and_comm : ∀ (a b : ISize), a &&& b = b &&& a
-- Mathlib.GroupTheory.Finiteness
Submonoid.FG.map : ∀ {M : Type u_1} [inst : Monoid M] {M' : Type u_3} [inst_1 : Monoid M'] {P : Submonoid M},
  P.FG → ∀ (e : M →* M'), (Submonoid.map e P).FG
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.PrepareRenameParams.toTextDocumentPositionParams : Lean.Lsp.PrepareRenameParams → Lean.Lsp.TextDocumentPositionParams
-- Mathlib.RingTheory.PowerSeries.Trunc
PowerSeries.trunc_coe_eq_self : ∀ {R : Type u_2} [inst : CommSemiring R] {n : ℕ} {f : Polynomial R}, f.natDegree < n → (PowerSeries.trunc n) ↑f = f
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.elabBlocks' : ℕ →
  StateT (Lean.TSyntaxArray `block) Lean.Doc.DocM
    (Array (Lean.Doc.Block Lean.ElabInline Lean.ElabBlock) × Array (Lean.Doc.Part Lean.ElabInline Lean.ElabBlock Empty))
-- Mathlib.Order.Hom.Lattice
LatticeHom.instFunLike : {α : Type u_2} → {β : Type u_3} → [inst : Lattice α] → [inst_1 : Lattice β] → FunLike (LatticeHom α β) α β
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.foldl_eq_foldl_toList : ∀ {α : Type u_1} {α_1 : Type u_2} {f : α_1 → α → α_1} {init : α_1} {t : RBTree.RBNode α},
  RBTree.RBNode.foldl f init t = List.foldl f init t.toList
-- Mathlib.CategoryTheory.Action.Limits
Action.instHasFiniteColimits : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G]
  [CategoryTheory.Limits.HasFiniteColimits V], CategoryTheory.Limits.HasFiniteColimits (Action V G)
-- Init.Data.Iterators.Lemmas.Consumers.Access
_private.Init.Data.Iterators.Lemmas.Consumers.Access.0.Std.Iter.atIdxSlow?_eq_match.match_3.eq_1 : ∀ {α β : Type u_1} (motive : Std.IterStep (Std.Iter β) β → Sort u_2) (it' : Std.Iter β) (out : β)
  (h_1 : (it' : Std.Iter β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.Iter β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.yield it' out with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_1 it' out
-- Init.Coe
/-- Auxiliary class implementing `CoeHead CoeOut* Coe*`.
Users should generally not implement this directly.
 -/
CoeHTC : Sort u → Sort v → Sort (max (max 1 u) v)
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.span_le_adjoin : ∀ (R : Type uR) {A : Type uA} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (s : Set A),
  Submodule.span R s ≤ Subalgebra.toSubmodule (Algebra.adjoin R s)
-- Mathlib.Algebra.GroupWithZero.Associated
Associated.mul_right : ∀ {M : Type u_1} [inst : CommMonoid M] {a b : M}, Associated a b → ∀ (c : M), Associated (a * c) (b * c)
-- Lean.Meta.Sym.SymM
/-- When `true`, `shareCommon` maintains the `SymM` invariant that kernel projections
have been folded into projection function applications: if a new term contains one,
`shareCommon` folds it before adding the term to the table of maximally shared terms.
`cbv` disables this check because it processes kernel projections natively.
 -/
Lean.Meta.Sym.Config.enforceFoldProjs : Lean.Meta.Sym.Config → Bool
-- Lean.Compiler.IR.Basic
Lean.IR.Decl.fdecl.sizeOf_spec : ∀ (f : Lean.IR.FunId) (xs : Array Lean.IR.Param) (type : Lean.IR.IRType) (body : Lean.IR.FnBody)
  (info : Lean.IR.DeclInfo),
  sizeOf (Lean.IR.Decl.fdecl f xs type body info) = 1 + sizeOf f + sizeOf xs + sizeOf type + sizeOf body + sizeOf info
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
SSet.Subcomplex.homOfLE_comp : ∀ {X : SSet} {S₁ S₂ : X.Subcomplex} (h : S₁ ≤ S₂) {S₃ : X.Subcomplex} (h' : S₂ ≤ S₃),
  CategoryTheory.CategoryStruct.comp (SSet.Subcomplex.homOfLE h) (SSet.Subcomplex.homOfLE h') =
    SSet.Subcomplex.homOfLE ⋯
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.HasRightCalculusOfFractions.toIsMultiplicative : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {W : CategoryTheory.MorphismProperty C}
  [self : W.HasRightCalculusOfFractions], W.IsMultiplicative
-- Mathlib.Algebra.Order.Monoid.WithTop
WithBot.lt_zero_iff_eq_bot : ∀ {α : Type u_1} [inst : AddMonoid α] [inst_1 : Preorder α] [CanonicallyOrderedAdd α] (a : WithBot α), a < 0 ↔ a = ⊥
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.preservesColimits_forget : ∀ (k : Type u) (G : Type v) [inst : Ring k] [inst_1 : Monoid G],
  CategoryTheory.Limits.PreservesColimitsOfSize.{w, w, w, w, max (max u v) (w + 1), max u (w + 1)}
    (CategoryTheory.forget₂ (Rep.{w, u, v} k G) (ModuleCat k))
-- Init.Data.SInt.Lemmas
Int32.toInt64_mod : ∀ (a b : Int32), (a % b).toInt64 = a.toInt64 % b.toInt64
-- Std.Time.Date.ValidDate
_private.Std.Time.Date.ValidDate.0.Std.Time.ValidDate.ofOrdinal.go : {leap : Bool} →
  (ordinal : Std.Time.Day.Ordinal.OfYear leap) →
    (idx : Std.Time.Month.Ordinal) →
      (acc : ℤ) → ↑ordinal > acc → acc = (Std.Time.Month.Ordinal.cumulativeDays leap idx).val → Std.Time.ValidDate leap
-- Init.Data.Iterators.Lemmas.Consumers.Access
_private.Init.Data.Iterators.Lemmas.Consumers.Access.0.Std.Iter.atIdxSlow?_eq_match.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
-- Lean.LibrarySuggestions.Basic
/-- Specify a library suggestion engine.
Note that Lean does not ship a default library suggestion engine,
so this is only useful in conjunction with a downstream package which provides one.
 -/
Lean.LibrarySuggestions.elabSetLibrarySuggestions : Lean.Elab.Command.CommandElab
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.star_apply : ∀ {n : Type u_2} {A : Type u_5} [inst : Star A] {f : CStarMatrix n n A} {i j : n}, star f i j = star (f j i)
-- Mathlib.Algebra.Notation.Support
/-- The support of a function that is everywhere nonzero is the whole space.  -/
Function.support_eq_univ : ∀ {ι : Type u_1} {M : Type u_3} [inst : Zero M] {f : ι → M}, (∀ (x : ι), f x ≠ 0) → Function.support f = Set.univ
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.ae_smul_measure_iff : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {R : Type u_8} [inst : Semiring R] [IsDomain R] [inst_2 : Module R ENNReal]
  [inst_3 : IsScalarTower R ENNReal ENNReal] [Module.IsTorsionFree R ENNReal] {c : R} {p : α → Prop},
  c ≠ 0 → ∀ {μ : MeasureTheory.Measure α}, (∀ᵐ (x : α) ∂c • μ, p x) ↔ ∀ᵐ (x : α) ∂μ, p x
-- Mathlib.Analysis.Normed.Module.Ball.Pointwise
smul_sphere : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NormedField 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  [NormedSpace ℝ E] [Nontrivial E] (c : 𝕜) (x : E) {r : ℝ},
  0 ≤ r → c • Metric.sphere x r = Metric.sphere (c • x) (‖c‖ * r)
-- Mathlib.CategoryTheory.Localization.Predicate
CategoryTheory.Localization.liftingConstructionLift : {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] →
        {W : CategoryTheory.MorphismProperty C} →
          (F : CategoryTheory.Functor C D) →
            (hF : W.IsInvertedBy F) →
              CategoryTheory.Localization.Lifting W.Q W F (CategoryTheory.Localization.Construction.lift F hF)
-- Mathlib.AlgebraicTopology.ModelCategory.BrownLemma
HomotopicalAlgebra.CofibrantBrownFactorization.s_p_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] {X Y : C}
  {f : X ⟶ Y} (self : HomotopicalAlgebra.CofibrantBrownFactorization f) {Z : C} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp self.s (CategoryTheory.CategoryStruct.comp self.p h) = h
-- Init.System.IOError
/-- A constraint required by an operation was not satisfied (e.g. a directory was not empty).

This corresponds to the POSIX error `ENOTEMPTY`.
 -/
IO.Error.unsatisfiedConstraints : UInt32 → String → IO.Error
-- Mathlib.Topology.EMetricSpace.Lipschitz
/-- Being Lipschitz on a set is monotone w.r.t. that set.  -/
LipschitzOnWith.mono : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {K : NNReal} {s t : Set α}
  {f : α → β}, LipschitzOnWith K f t → s ⊆ t → LipschitzOnWith K f s
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.Prequotient.add.inj : ∀ {J : Type v} {inst : CategoryTheory.SmallCategory J} {F : CategoryTheory.Functor J CommRingCat}
  {a a_1 a_2 a_3 : CommRingCat.Colimits.Prequotient F}, a.add a_1 = a_2.add a_3 → a = a_2 ∧ a_1 = a_3
-- Mathlib.RingTheory.Localization.Basic
/-- If `S`, `Q` are localizations of `R` at the submonoid `M` respectively,
there is an isomorphism of localizations `S ≃ₐ[R] Q`.  -/
IsLocalization.algEquiv : {R : Type u_1} →
  [inst : CommSemiring R] →
    (M : Submonoid R) →
      (S : Type u_2) →
        [inst_1 : CommSemiring S] →
          [inst_2 : Algebra R S] →
            [IsLocalization M S] →
              (Q : Type u_4) → [inst_4 : CommSemiring Q] → [inst_5 : Algebra R Q] → [IsLocalization M Q] → S ≃ₐ[R] Q
-- Mathlib.GroupTheory.Nilpotent
Subgroup.upperCentralSeriesAux.match_1.congr_eq_1 : ∀ (motive : ℕ → Sort u_1) (x : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  x = 0 →
    (match x with
      | 0 => h_1 ()
      | n.succ => h_2 n) ≍
      h_1 ()
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.yonedaAddGrp_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {G H X Y : C} [inst_2 : CategoryTheory.AddGrpObj G] [inst_3 : CategoryTheory.AddGrpObj H]
  (α : CategoryTheory.yonedaAddGrpObj G ⟶ CategoryTheory.yonedaAddGrpObj H) (f : X ⟶ Y) (g : Y ⟶ G),
  (CategoryTheory.ConcreteCategory.hom (α.app (Opposite.op X))) (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp f ((CategoryTheory.ConcreteCategory.hom (α.app (Opposite.op Y))) g)
-- Mathlib.Analysis.Normed.Field.Lemmas
TendstoLocallyUniformly.inv₀ : ∀ {α : Type u_1} [inst : NormedDivisionRing α] {X : Type u_4} {ι : Type u_5} [inst_1 : TopologicalSpace X]
  {F : ι → X → α} {f : X → α} {l : Filter ι},
  TendstoLocallyUniformly F f l → Continuous f → (∀ (x : X), f x ≠ 0) → TendstoLocallyUniformly F⁻¹ f⁻¹ l
-- Mathlib.Algebra.Group.TypeTags.Basic
isAddRightRegular_toAdd : ∀ {α : Type u} [inst : AddMonoid α] {a : Multiplicative α},
  IsAddRightRegular (Multiplicative.toAdd a) ↔ IsRightRegular a
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
/-- The `realSpace` associated to a number field `K` is the real vector space indexed by the
infinite places of `K`.
 -/
NumberField.mixedEmbedding.realSpace : (K : Type u_1) → [Field K] → Type u_1
-- Mathlib.Data.Nat.Periodic
Nat.periodic_coprime : ∀ (a : ℕ), Function.Periodic a.Coprime a