mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Category.FGModuleCat.Colimits
/-- The forgetful functor from `FGModuleCat k` to `ModuleCat k` creates all finite colimits.  -/
FGModuleCat.forget₂CreatesColimit : {J : Type} →
  [inst : CategoryTheory.SmallCategory J] →
    [CategoryTheory.FinCategory J] →
      {k : Type u} →
        [inst_2 : Ring k] →
          (F : CategoryTheory.Functor J (FGModuleCat k)) →
            CategoryTheory.CreatesColimit F (CategoryTheory.forget₂ (FGModuleCat k) (ModuleCat k))
-- Mathlib.Analysis.Normed.Field.Lemmas
UniformContinuous.inv₀ : ∀ {α : Type u_1} [inst : NormedDivisionRing α] {X : Type u_4} [inst_1 : UniformSpace X] {f : X → α},
  UniformContinuous f → (Set.range f)ᶜ ∈ nhds 0 → UniformContinuous f⁻¹
-- Mathlib.Tactic.GCongr.Core
/-- Index of the hypothesis itself.  -/
Mathlib.Tactic.GCongr.GCongrHyp.hypIdx : Mathlib.Tactic.GCongr.GCongrHyp → ℕ
-- Mathlib.Algebra.Order.Ring.Basic
/-- **Alias** of the reverse direction of `Odd.pow_neg_iff`. -/
Odd.pow_neg : ∀ {R : Type u_3} [inst : Semiring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] {a : R} {n : ℕ} [ExistsAddOfLE R],
  Odd n → a < 0 → a ^ n < 0
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.sInf_adj : ∀ {V : Type u} {G : SimpleGraph V} {a b : V} {s : Set G.Subgraph}, (sInf s).Adj a b ↔ (∀ G' ∈ s, G'.Adj a b) ∧ G.Adj a b
-- Std.Data.HashSet.Raw
Std.HashSet.Raw.mk : {α : Type u} → Std.HashMap.Raw α Unit → Std.HashSet.Raw α
-- Mathlib.Logic.Equiv.Defs
Equiv.arrowCongr'_trans : ∀ {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} {α₃ : Type u_5} {β₃ : Type u_6} (e₁ : α₁ ≃ α₂)
  (e₁' : β₁ ≃ β₂) (e₂ : α₂ ≃ α₃) (e₂' : β₂ ≃ β₃),
  (e₁.trans e₂).arrowCongr' (e₁'.trans e₂') = (e₁.arrowCongr' e₁').trans (e₂.arrowCongr' e₂')
-- Std.Data.TreeMap.Raw.Lemmas
/-- This is a restatement of `mem_of_mem_insertIfNew` that is written to exactly match the
proof obligation in the statement of `get_insertIfNew`.  -/
Std.TreeMap.Raw.mem_of_mem_insertIfNew' : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k a : α} {v : β}, a ∈ t.insertIfNew k v → ¬(cmp k a = Ordering.eq ∧ k ∉ t) → a ∈ t
-- Mathlib.Topology.MetricSpace.IsometricSMul
ULift.isIsometricVAdd : ∀ {M : Type u} {X : Type w} [inst : PseudoEMetricSpace X] [inst_1 : VAdd M X] [IsIsometricVAdd M X],
  IsIsometricVAdd (ULift.{u_2, u} M) X
-- Mathlib.Algebra.RingQuot
RingQuot.Rel.below.mul_right : ∀ {R : Type uR} [inst : Semiring R] {r : R → R → Prop} {motive : (a a_1 : R) → RingQuot.Rel r a a_1 → Prop} ⦃a b c : R⦄
  (a_1 : RingQuot.Rel r b c), RingQuot.Rel.below a_1 → motive b c a_1 → RingQuot.Rel.below ⋯
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- If `F.cocones` is corepresented by `X`, each cocone `s` gives a morphism `X ⟶ s.pt`.  -/
CategoryTheory.Limits.IsColimit.OfNatIso.homOfCocone : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          {X : C} → F.cocones.CorepresentableBy X → (s : CategoryTheory.Limits.Cocone F) → X ⟶ s.pt
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
/-- A slight reformulation of `IsLocalStructomorphWithinAt` when `f` is an open partial homeomorph
and the set we're considering is a superset of `f.source`.  -/
OpenPartialHomeomorph.isLocalStructomorphWithinAt_iff' : ∀ {H : Type u_1} [inst : TopologicalSpace H] {G : StructureGroupoid H} [ClosedUnderRestriction G]
  (f : OpenPartialHomeomorph H H) {s : Set H} {x : H},
  f.source ⊆ s →
    x ∈ f.source ∪ sᶜ →
      (G.IsLocalStructomorphWithinAt (↑f) s x ↔
        x ∈ s → ∃ e ∈ G, e.source ⊆ f.source ∧ Set.EqOn (↑f) (↑e) e.source ∧ x ∈ e.source)
-- Mathlib.Algebra.Category.ModuleCat.Basic
LinearMap.id_moduleCat_comp : ∀ {R : Type u_1} [inst : Ring R] {G : Type u} [inst_1 : AddCommGroup G] [inst_2 : Module R G] {H : ModuleCat R}
  (f : G →ₗ[R] ↑H), ModuleCat.Hom.hom (CategoryTheory.CategoryStruct.id H) ∘ₗ f = f
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubAddAction.instBot.eq_1 : ∀ {R : Type u} {M : Type v} [inst : VAdd R M], SubAddAction.instBot = { bot := { carrier := ∅, vadd_mem' := ⋯ } }
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKeyD_insertIfNew : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k a fallback : α} {v : β},
  (m.insertIfNew k v).getKeyD a fallback = if (k == a) = true ∧ k ∉ m then k else m.getKeyD a fallback
-- Batteries.Data.List.Perm
List.swap_perm : ∀ {α : Type u_1} (xs : List α) (i j : ℕ), (xs.swap i j).Perm xs
-- Mathlib.Algebra.Notation.Pi.Defs
Pi.sub_comp : ∀ {α : Type u_2} {β : Type u_3} {G : Type u_7} [inst : Sub G] (f g : β → G) (z : α → β), (f - g) ∘ z = f ∘ z - g ∘ z
-- Mathlib.Algebra.Star.StarAlgHom
NonUnitalStarAlgHom.coe_id : ∀ (R : Type u_1) (A : Type u_2) [inst : Monoid R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : DistribMulAction R A]
  [inst_3 : Star A], ⇑(NonUnitalStarAlgHom.id R A) = id
-- Mathlib.Topology.Convenient.GeneratedBy
TopologicalSpace.generatedBy_le : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)] {Y : Type v} {tY : TopologicalSpace Y},
  TopologicalSpace.generatedBy X ≤ tY
-- Mathlib.CategoryTheory.Products.Unitor
CategoryTheory.prod.rightUnitorEquivalence_functor : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C],
  (CategoryTheory.prod.rightUnitorEquivalence C).functor = CategoryTheory.prod.rightUnitor C
-- Std.Http.Data.Body.Stream
/-- Receives a chunk from the channel. Blocks until a producer sends one.
Returns `none` if the channel is closed and no producer is waiting.
 -/
Std.Http.Body.Stream.recv : Std.Http.Body.Stream → Std.Async.Async (Option Std.Http.Chunk)
-- Init.Data.List.Lemmas
List.insert_eq : ∀ {α : Type u_1} [inst : BEq α] [inst_1 : LawfulBEq α] {l : List α} {a : α},
  List.insert a l = if a ∈ l then l else a :: l
-- Mathlib.RepresentationTheory.Invariants
Rep.invariantsAdjunction_counit_app : ∀ (k : Type u) (G : Type v) [inst : CommRing k] [inst_1 : Group G] (X : Rep.{u_1, u, v} k G),
  (Rep.invariantsAdjunction k G).counit.app X =
    Rep.ofHom { toLinearMap := X.ρ.invariants.subtype, isIntertwining' := ⋯ }
-- Mathlib.Topology.Algebra.Group.Basic
Topology.IsInducing.topologicalGroup : ∀ {G : Type w} {H : Type x} [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G] {F : Type u_1}
  [inst_3 : Group H] [inst_4 : TopologicalSpace H] [inst_5 : FunLike F H G] [MonoidHomClass F H G] (f : F),
  Topology.IsInducing ⇑f → IsTopologicalGroup H
-- Mathlib.FieldTheory.IsPerfectClosure
PerfectRing.lift.congr_simp : ∀ {K : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing K] [inst_1 : CommRing L] [inst_2 : CommRing M]
  (i i_1 : K →+* L) (e_i : i = i_1) (j j_1 : K →+* M),
  j = j_1 →
    ∀ (p p_1 : ℕ) (e_p : p = p_1) [inst_3 : ExpChar M p] [inst_4 : ExpChar K p] [inst_5 : PerfectRing M p]
      [inst_6 : IsPRadical i p] [inst_7 : ExpChar L p], PerfectRing.lift i j p = PerfectRing.lift i_1 j_1 p_1
-- Mathlib.Data.Multiset.Sum
Multiset.disjSum_strictMono_right : ∀ {α : Type u_1} {β : Type u_2} (s : Multiset α), StrictMono s.disjSum
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.eval₂_X_mul : ∀ {R : Type u} {S : Type v} [inst : Semiring R] {p : Polynomial R} [inst_1 : Semiring S] (f : R →+* S) (x : S),
  Polynomial.eval₂ f x (Polynomial.X * p) = Polynomial.eval₂ f x p * x
-- Mathlib.Analysis.Normed.Group.Basic
nnnorm_zpow_abs : ∀ {E : Type u_5} [inst : SeminormedGroup E] (a : E) (n : ℤ), ‖a ^ |n|‖₊ = ‖a ^ n‖₊
-- Mathlib.Order.PartialSups
le_partialSups : ∀ {α : Type u_1} {ι : Type u_3} [inst : SemilatticeSup α] [inst_1 : Preorder ι] [inst_2 : LocallyFiniteOrderBot ι]
  (f : ι → α), f ≤ ⇑(partialSups f)
-- Mathlib.Data.Finset.Sups
Finset.disjSups_union_left : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeSup α] [inst_2 : OrderBot α]
  [inst_3 : DecidableRel Disjoint] {s₁ s₂ t : Finset α}, (s₁ ∪ s₂).disjSups t = s₁.disjSups t ∪ s₂.disjSups t
-- Init.Meta.Defs
Lean.versionString : String
-- Mathlib.NumberTheory.FactorisationProperties
Nat.infinite_odd_abundant : {n | Odd n ∧ n.Abundant}.Infinite
-- Mathlib.RingTheory.Localization.AtPrime.Basic
IsLocalization.subsingleton_primeSpectrum_of_mem_minimalPrimes : ∀ {R : Type u_5} [inst : CommSemiring R] (p : Ideal R) (hp : p ∈ minimalPrimes R) (S : Type u_6)
  [inst_1 : CommSemiring S] [inst_2 : Algebra R S] [IsLocalization.AtPrime S p], Subsingleton (PrimeSpectrum S)
-- Mathlib.GroupTheory.OrderOfElement
addOrderOf_zero : ∀ {G : Type u_1} [inst : AddMonoid G], addOrderOf 0 = 1
-- Mathlib.Data.Finset.Lattice.Fold
Finset.inf_insert : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeInf α] [inst_1 : OrderTop α] {s : Finset β} {f : β → α}
  [inst_2 : DecidableEq β] {b : β}, (insert b s).inf f = f b ⊓ s.inf f
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
MeasureTheory.AECover.integrable_of_lintegral_enorm_tendsto : ∀ {α : Type u_1} {ι : Type u_2} {E : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {l : Filter ι}
  [inst_1 : NormedAddCommGroup E] [l.NeBot] [l.IsCountablyGenerated] {φ : ι → Set α},
  MeasureTheory.AECover μ l φ →
    ∀ {f : α → E} (I : ℝ),
      MeasureTheory.AEStronglyMeasurable f μ →
        Filter.Tendsto (fun i => ∫⁻ (x : α) in φ i, ‖f x‖ₑ ∂μ) l (nhds (ENNReal.ofReal I)) →
          MeasureTheory.Integrable f μ
-- Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit
CategoryTheory.Limits.Types.Limit.mk.congr_simp : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u))
  [inst_1 : CategoryTheory.Limits.HasLimit F] (x x_1 : (j : J) → F.obj j) (e_x : x = x_1)
  (h : ∀ (j j' : J) (f : j ⟶ j'), (CategoryTheory.ConcreteCategory.hom (F.map f)) (x j) = x j'),
  CategoryTheory.Limits.Types.Limit.mk F x h = CategoryTheory.Limits.Types.Limit.mk F x_1 ⋯
-- Mathlib.NumberTheory.LucasLehmer
LucasLehmer.X.ω_mul_ωb : ∀ {q : ℕ}, LucasLehmer.X.ω * LucasLehmer.X.ωb = 1
-- Mathlib.CategoryTheory.Shift.Basic
/-- compatibility with the right addition with 0  -/
CategoryTheory.ShiftMkCore.add_zero_hom_app : ∀ {C : Type u} {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddMonoid A]
  (self : CategoryTheory.ShiftMkCore C A) (n : A) (X : C),
  (self.add n 0).hom.app X =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (self.zero.inv.app ((self.F n).obj X))
-- Mathlib.CategoryTheory.LiftingProperties.ParametrizedAdjunction
CategoryTheory.ParametrizedAdjunction.arrowHomEquiv_apply_left : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)}
  {G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)} (adj₂ : F ⊣₂ G) {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁}
  {X₂ Y₂ : C₂} {f₂ : X₂ ⟶ Y₂} {X₃ Y₃ : C₃} {f₃ : X₃ ⟶ Y₃} (sq₁₂ : F.PushoutObjObj f₁ f₂) (sq₁₃ : G.PullbackObjObj f₁ f₃)
  (α : CategoryTheory.Arrow.mk sq₁₂.ι ⟶ CategoryTheory.Arrow.mk f₃),
  ((adj₂.arrowHomEquiv sq₁₂ sq₁₃) α).left =
    adj₂.homEquiv (CategoryTheory.CategoryStruct.comp sq₁₂.inl (CategoryTheory.Arrow.Hom.left α))
-- Mathlib.Topology.KrullDimension
Topology.IsOpenEmbedding.coheight_eq : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [QuasiSober Y]
  [inst_3 : T0Space Y] [QuasiSober X] [inst_5 : T0Space X] {x : X} (f : X → Y),
  Topology.IsOpenEmbedding f → Order.coheight (f x) = Order.coheight x
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.smul_mk'_self : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : IsLocalization M S] {m : ↥M} {r : R},
  ↑m • IsLocalization.mk' S r m = (algebraMap R S) r
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.colimit.cocone.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Functor J C) [inst_2 : CategoryTheory.Limits.HasColimit F],
  CategoryTheory.Limits.colimit.cocone F = (CategoryTheory.Limits.getColimitCocone F).cocone
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring
IsHomogeneous.subsemiringClosure : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : AddMonoid ι] [inst_1 : Semiring A] [inst_2 : SetLike σ A]
  [inst_3 : AddSubmonoidClass σ A] {𝒜 : ι → σ} [inst_4 : DecidableEq ι] [inst_5 : GradedRing 𝒜] {s : Set A},
  (∀ (i : ι) ⦃x : A⦄, x ∈ s → ↑(((DirectSum.decompose 𝒜) x) i) ∈ s) →
    DirectSum.SetLike.IsHomogeneous 𝒜 (Subsemiring.closure s)
-- Mathlib.RingTheory.UniqueFactorizationDomain.Defs
WfDvdMonoid.exists_factors : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [WfDvdMonoid α] (a : α),
  a ≠ 0 → ∃ f, (∀ b ∈ f, Irreducible b) ∧ Associated f.prod a
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
/-- If `X` is a colimit indexed by `J` of objects satisfying a property `P`,
it is also a colimit indexed by `J` of objects satisfying `Q` if `P ≤ Q`.  -/
CategoryTheory.ObjectProperty.ColimitOfShape.ofLE : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {P : CategoryTheory.ObjectProperty C} →
      {J : Type u'} →
        [inst_1 : CategoryTheory.Category.{v', u'} J] →
          {X : C} → P.ColimitOfShape J X → {Q : CategoryTheory.ObjectProperty C} → P ≤ Q → Q.ColimitOfShape J X
-- Lean.Meta.Tactic.Simp.SimpTheorems
/-- It stores universe parameter names for universe polymorphic proofs.
Recall that it is non-empty only when we elaborate an expression provided by the user.
When `proof` is just a constant, we can use the universe parameter names stored in the declaration.
 -/
Lean.Meta.SimpTheorem.levelParams : Lean.Meta.SimpTheorem → Array Lean.Name
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instCancelCommMonoid : {α : Type u_1} → [CancelCommMonoid α] → CancelCommMonoid αᵒᵈ
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKey?_modify : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {f : β → β}, (t.modify k f).minKey? = Option.map (fun km => if cmp km k = Ordering.eq then k else km) t.minKey?
-- Mathlib.GroupTheory.QuotientGroup.Basic
/-- The first isomorphism theorem (a definition): the canonical isomorphism between
`G/(ker φ)` to `range φ`.  -/
QuotientAddGroup.quotientKerEquivRange : {G : Type u} → [inst : AddGroup G] → {H : Type v} → [inst_1 : AddGroup H] → (φ : G →+ H) → G ⧸ φ.ker ≃+ ↥φ.range
-- Lean.Elab.MutualInductive
Lean.Elab.Command.InductiveView.binders : Lean.Elab.Command.InductiveView → Lean.Syntax
-- Mathlib.RingTheory.Valuation.Basic
/-- A `≤`-preserving, `⊤`-preserving group homomorphism `Γ₀ → Γ'₀` induces a map
`AddValuation R Γ₀ → AddValuation R Γ'₀`.
 -/
AddValuation.map : {R : Type u_3} →
  {Γ₀ : Type u_4} →
    {Γ'₀ : Type u_5} →
      [inst : Ring R] →
        [inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀] →
          [inst_2 : LinearOrderedAddCommMonoidWithTop Γ'₀] →
            (f : Γ₀ →+ Γ'₀) → f ⊤ = ⊤ → Monotone ⇑f → AddValuation R Γ₀ → AddValuation R Γ'₀
-- Mathlib.Order.SymmDiff
sup_bihimp_bihimp : ∀ {α : Type u_2} [inst : GeneralizedHeytingAlgebra α] (a b : α), bihimp (a ⊔ b) (bihimp a b) = a ⊓ b
-- Mathlib.Order.UpperLower.Closure
UpperSet.Ici_inf_erase : ∀ {α : Type u_1} [inst : Preorder α] {s : UpperSet α} {a : α},
  a ∈ s → (∀ b ∈ s, b ≤ a → b = a) → UpperSet.Ici a ⊓ s.erase a = s
-- Mathlib.RingTheory.TwoSidedIdeal.Operations
/-- Bundle an `Ideal` that is already two-sided as a `TwoSidedIdeal`.  -/
Ideal.toTwoSided : {R : Type u_1} → [inst : Ring R] → (I : Ideal R) → [I.IsTwoSided] → TwoSidedIdeal R
-- Mathlib.Probability.Martingale.Upcrossing
MeasureTheory.upcrossingsBefore_lt_of_exists_upcrossing : ∀ {Ω : Type u_1} {a b : ℝ} {f : ℕ → Ω → ℝ} {N : ℕ} {ω : Ω},
  a < b →
    ∀ {N₁ N₂ : ℕ},
      N ≤ N₁ →
        f N₁ ω < a →
          N₁ ≤ N₂ →
            b < f N₂ ω → MeasureTheory.upcrossingsBefore a b f N ω < MeasureTheory.upcrossingsBefore a b f (N₂ + 1) ω
-- Mathlib.Logic.Relator
/-- A relation is "right unique" if every element on the left is paired with at
most one element on the right.  -/
Relator.RightUnique : {α : Sort u₁} → {β : Sort u₂} → (α → β → Prop) → Prop
-- Mathlib.Data.SetLike.Basic
SetLike.instCoeTCSet : {A : Type u_1} → {B : Type u_2} → [i : SetLike A B] → CoeTC A (Set B)
-- Lean.Meta.Tactic.Grind.AC.Seq
/-- `s₁` does not start with `s₂`  -/
_private.Lean.Meta.Tactic.Grind.AC.Seq.0.Lean.Grind.AC.StartsWithResult.false : Lean.Grind.AC.StartsWithResult✝
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyData.ofZeros_p : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) (hf : S.f = 0) (hg : S.g = 0),
  (CategoryTheory.ShortComplex.RightHomologyData.ofZeros S hf hg).p = CategoryTheory.CategoryStruct.id S.X₂
-- Mathlib.CategoryTheory.Localization.Monoidal.Braided
CategoryTheory.Localization.Monoidal.instBraidedLocalizedMonoidalToMonoidalCategory : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        (L : CategoryTheory.Functor C D) →
          (W : CategoryTheory.MorphismProperty C) →
            [inst_2 : CategoryTheory.MonoidalCategory C] →
              [inst_3 : W.IsMonoidal] →
                [inst_4 : L.IsLocalization W] →
                  {unit : D} →
                    (ε : L.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ unit) →
                      [inst_5 : CategoryTheory.BraidedCategory C] →
                        (CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).Braided
-- Mathlib.Order.Circular
/-- Betweenness for circular orders. `btw a b c` states that `b` is between `a` and `c` (in that
order).  -/
Btw.btw : {α : Type u_1} → [self : Btw α] → α → α → α → Prop
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.maxKey!_modify_eq_maxKey! : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [inst : Inhabited α] {k : α} {f : β → β}, (Std.DTreeMap.Const.modify t k f).maxKey! = t.maxKey!
-- Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
/-- A simple general sufficient condition for bounding `levyProkhorovEDist` from above.  -/
MeasureTheory.levyProkhorovEDist_le_of_forall : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : PseudoEMetricSpace Ω] (μ ν : MeasureTheory.Measure Ω)
  (δ : ENNReal),
  (∀ (ε : ENNReal) (B : Set Ω),
      δ < ε →
        ε < ⊤ →
          MeasurableSet B → μ B ≤ ν (Metric.thickening ε.toReal B) + ε ∧ ν B ≤ μ (Metric.thickening ε.toReal B) + ε) →
    MeasureTheory.levyProkhorovEDist μ ν ≤ δ
-- Mathlib.Topology.Inseparable
stableUnderSpecialization_compl_iff : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, StableUnderSpecialization sᶜ ↔ StableUnderGeneralization s
-- Mathlib.Combinatorics.SimpleGraph.Metric
SimpleGraph.edist_triangle : ∀ {V : Type u_1} {G : SimpleGraph V} {u v w : V}, G.edist u w ≤ G.edist u v + G.edist v w
-- Mathlib.RingTheory.Artinian.Module
DivisionRing.instIsArtinianRing : ∀ {K : Type u_1} [inst : DivisionRing K], IsArtinianRing K
-- Init.Data.List.Find
List.findIdx_lt_length_of_exists : ∀ {α : Type u_1} {p : α → Bool} {xs : List α}, (∃ x ∈ xs, p x = true) → List.findIdx p xs < xs.length
-- Mathlib.Algebra.Ring.Periodic
List.periodic_sum : ∀ {α : Type u_1} {β : Type u_2} {c : α} [inst : Add α] [inst_1 : AddZeroClass β] (l : List (α → β)),
  (∀ f ∈ l, Function.Periodic f c) → Function.Periodic l.sum c
-- Mathlib.Analysis.Convex.Combination
/-- A version of `Convex.sum_mem` for `finsum`s. If `s` is a convex set, `w : ι → R` is a family of
nonnegative weights with sum one and `z : ι → E` is a family of elements of a module over `R` such
that `z i ∈ s` whenever `w i ≠ 0`, then the sum `∑ᶠ i, w i • z i` belongs to `s`. See also
`PartitionOfUnity.finsum_smul_mem_convex`.  -/
Convex.finsum_mem : ∀ {R : Type u_1} {E : Type u_3} [inst : Field R] [inst_1 : AddCommGroup E] [inst_2 : Module R E]
  [inst_3 : LinearOrder R] [IsStrictOrderedRing R] {ι : Sort u_8} {w : ι → R} {z : ι → E} {s : Set E},
  Convex R s → (∀ (i : ι), 0 ≤ w i) → ∑ᶠ (i : ι), w i = 1 → (∀ (i : ι), w i ≠ 0 → z i ∈ s) → ∑ᶠ (i : ι), w i • z i ∈ s
-- Mathlib.RingTheory.Congruence.BigOperators
RingCon.coe_multisetSum : ∀ {ι : Type u_1} {S : Type u_2} [inst : AddCommMonoid S] [inst_1 : Mul S] (t : RingCon S) (s : Multiset ι) (f : ι → S),
  ↑(Multiset.map f s).sum = (Multiset.map (fun i => ↑(f i)) s).sum
-- Mathlib.FieldTheory.KummerExtension
/-- The natural embedding of the roots of unity of `K` into `Gal(K[ⁿ√a]/K)`, by sending
`η ↦ (ⁿ√a ↦ η • ⁿ√a)`. This is an isomorphism when `K` contains a primitive root of unity.
See `autAdjoinRootXPowSubCEquiv`.  -/
autAdjoinRootXPowSubC : {K : Type u} →
  [inst : Field K] →
    (n : ℕ) →
      (a : K) →
        ↥(rootsOfUnity n K) →*
          AdjoinRoot (Polynomial.X ^ n - Polynomial.C a) ≃ₐ[K] AdjoinRoot (Polynomial.X ^ n - Polynomial.C a)
-- Mathlib.CategoryTheory.Monoidal.FunctorCategory
/-- (An auxiliary definition for `functorCategoryMonoidal`.)  -/
CategoryTheory.Monoidal.FunctorCategory.whiskerRight : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        [inst_2 : CategoryTheory.MonoidalCategory D] →
          {F G : CategoryTheory.Functor C D} →
            (F ⟶ G) →
              (F' : CategoryTheory.Functor C D) →
                CategoryTheory.Monoidal.FunctorCategory.tensorObj F F' ⟶
                  CategoryTheory.Monoidal.FunctorCategory.tensorObj G F'
-- Mathlib.RingTheory.AdicCompletion.AsTensorProduct
_private.Mathlib.RingTheory.AdicCompletion.AsTensorProduct.0.AdicCompletion.ofTensorProduct_bijective_of_map_from_fin : ∀ {R : Type u} [inst : CommRing R] (I : Ideal R) (M : Type u) [inst_1 : AddCommGroup M] [inst_2 : Module R M] {ι : Type}
  (f : (ι → R) →ₗ[R] M),
  Function.Surjective ⇑f → ∀ [Finite ι] [IsNoetherianRing R], Function.Bijective ⇑(AdicCompletion.ofTensorProduct I M)
-- Mathlib.Topology.IsLocalHomeomorph
isLocalHomeomorph_iff_isLocalHomeomorphOn_univ : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  IsLocalHomeomorph f ↔ IsLocalHomeomorphOn f Set.univ
-- Lean.Parser.Basic
Lean.Parser.checkLhsPrec : ℕ → Lean.Parser.Parser
-- Mathlib.Computability.ContextFreeGrammar
/-- Add extra prefix to context-free rewriting.  -/
ContextFreeRule.Rewrites.append_left : ∀ {T : Type u_1} {N : Type u_2} {r : ContextFreeRule T N} {u v : List (Symbol T N)},
  r.Rewrites u v → ∀ (p : List (Symbol T N)), r.Rewrites (p ++ u) (p ++ v)
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
SemilinearIsometryClass.mk : ∀ {𝓕 : Type u_11} {R : outParam (Type u_12)} {R₂ : outParam (Type u_13)} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : outParam (R →+* R₂)} {E : outParam (Type u_14)} {E₂ : outParam (Type u_15)} [inst_2 : SeminormedAddCommGroup E]
  [inst_3 : SeminormedAddCommGroup E₂] [inst_4 : Module R E] [inst_5 : Module R₂ E₂] [inst_6 : FunLike 𝓕 E E₂]
  [toSemilinearMapClass : SemilinearMapClass 𝓕 σ₁₂ E E₂],
  (∀ (f : 𝓕) (x : E), ‖f x‖ = ‖x‖) → SemilinearIsometryClass 𝓕 σ₁₂ E E₂
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.basicOpenIsoSpecAway.eq_1 : ∀ {R : CommRingCat} (f : ↑R),
  AlgebraicGeometry.basicOpenIsoSpecAway f =
    AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq (AlgebraicGeometry.Scheme.Opens.ι (PrimeSpectrum.basicOpen f))
      (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away f)))) ⋯
-- Mathlib.Data.List.Sort
List.sortedGE_reverse : ∀ {α : Type u_1} {l : List α} [inst : Preorder α], l.reverse.SortedGE ↔ l.SortedLE
-- Mathlib.Algebra.GroupWithZero.Defs
GroupWithZero.toDivInvMonoid : {G₀ : Type u} → [self : GroupWithZero G₀] → DivInvMonoid G₀
-- Init.Data.String.Lemmas.Pattern.Basic
/-- Predicate stating that a match for a given pattern is never a proper prefix of another match.

This implies that the notion of match and longest match coincide.
 -/
String.Slice.Pattern.Model.NoPrefixPatternModel : {ρ : Type} → (pat : ρ) → [String.Slice.Pattern.Model.PatternModel pat] → Prop