mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
CategoryTheory.IsCofiltered.instHasLimitOfIsEventuallyConstant : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] (F : CategoryTheory.Functor J C)
  [hF : CategoryTheory.IsCofiltered.IsEventuallyConstant F] [CategoryTheory.IsCofiltered J],
  CategoryTheory.Limits.HasLimit F
-- Mathlib.GroupTheory.HNNExtension
/-- We have exactly one element of each coset of the subgroup  -/
HNNExtension.NormalWord.TransversalPair.compl : ∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} (self : HNNExtension.NormalWord.TransversalPair G A B) (u : ℤˣ),
  Subgroup.IsComplement (↑(HNNExtension.toSubgroup A B u)) (self.set u)
-- Mathlib.Data.Set.Prod
Function.pullbackDiagonal.eq_1 : ∀ {X : Type u_1} {Y : Sort u_2} (f : X → Y), Function.pullbackDiagonal f = {p | p.fst = p.snd}
-- Mathlib.MeasureTheory.Integral.CircleIntegral
/-- If `g` is continuous on the circle `sphere c |R|` and `f` is circle integrable, then `g • f` is
circle integrable.
 -/
CircleIntegrable.continuousOn_smul : ∀ {c : ℂ} {R : ℝ} {𝕜 : Type u_3} {F : Type u_4} [inst : NormedRing 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : Module 𝕜 F] [NormSMulClass 𝕜 F] {f : ℂ → F} {g : ℂ → 𝕜},
  CircleIntegrable f c R → ContinuousOn g (Metric.sphere c |R|) → CircleIntegrable (g • f) c R
-- Lean.Data.Lsp.Basic
Lean.Lsp.instFromJsonDocumentFilter.fromJson : Lean.Json → Except String Lean.Lsp.DocumentFilter
-- Batteries.Lean.Meta.Simp
/-- Flip the proof in a `Simp.Result`.  -/
Lean.Meta.Simp.mkEqSymm : Lean.Expr → Lean.Meta.Simp.Result → Lean.MetaM Lean.Meta.Simp.Result
-- Mathlib.Order.Interval.Finset.Defs
Finset.subtype_Ioc_eq : ∀ {α : Type u_1} [inst : Preorder α] (p : α → Prop) [inst_1 : DecidablePred p] [inst_2 : LocallyFiniteOrder α]
  (b a : Subtype p), Finset.Ioc b a = Finset.subtype p (Finset.Ioc ↑b ↑a)
-- Mathlib.Algebra.Star.Basic
StarModule.mk : ∀ {R : Type u} {A : Type v} [inst : Star R] [inst_1 : Star A] [inst_2 : SMul R A],
  (∀ (r : R) (a : A), star (r • a) = star r • star a) → StarModule R A
-- Mathlib.GroupTheory.QuotientGroup.Defs
/-- The group homomorphism from `G` to `G/N`.  -/
QuotientGroup.mk' : {G : Type u_1} → [inst : Group G] → (N : Subgroup G) → [nN : N.Normal] → G →* G ⧸ N
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
SimplyConnectedSpace.ofContractible : ∀ (Y : Type u_4) [inst : TopologicalSpace Y] [ContractibleSpace Y], SimplyConnectedSpace Y
-- Mathlib.CategoryTheory.ObjectProperty.EpiMono
CategoryTheory.ObjectProperty.instIsClosedUnderQuotientsTop : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C], ⊤.IsClosedUnderQuotients
-- Mathlib.Algebra.Lie.Nilpotent
LieIdeal.instIsNilpotentSubtypeMemOfIsNilpotent : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (I : LieIdeal R L)
  [LieModule.IsNilpotent L ↥I], LieRing.IsNilpotent ↥I
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.preimageHomeomorph_apply : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  [inst_2 : TopologicalSpace Z] (e : Bundle.Trivialization F proj) {s : Set B} (hb : s ⊆ e.baseSet) (p : ↑(proj ⁻¹' s)),
  (e.preimageHomeomorph hb) p = (⟨proj ↑p, ⋯⟩, (↑e ↑p).2)
-- Mathlib.Analysis.Complex.Basic
/-- The natural `ℝ`-linear isometry equivalence between `𝕜` satisfying `RCLike 𝕜` and `ℂ` when
`RCLike.im RCLike.I = 1`.  -/
RCLike.complexLinearIsometryEquiv : {𝕜 : Type u_2} → [inst : RCLike 𝕜] → RCLike.im RCLike.I = 1 → 𝕜 ≃ₗᵢ[ℝ] ℂ
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
_private.Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic.0.tacticMap_simp : Lean.ParserDescr
-- Mathlib.Geometry.Manifold.ChartedSpace
ChartedSpace.mem_atlas_sum : ∀ {H : Type u} {M : Type u_2} {M' : Type u_3} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M]
  [inst_2 : TopologicalSpace M'] [cm : ChartedSpace H M] [cm' : ChartedSpace H M'] [h : Nonempty H]
  {e : OpenPartialHomeomorph (M ⊕ M') H},
  e ∈ atlas H (M ⊕ M') → (∃ f ∈ atlas H M, e = f.lift_openEmbedding ⋯) ∨ ∃ f' ∈ atlas H M', e = f'.lift_openEmbedding ⋯
-- Mathlib.CategoryTheory.Pi.Monoidal
CategoryTheory.Pi.monoidalCategoryStruct_tensorUnit : ∀ {I : Type w₁} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)]
  [inst_1 : (i : I) → CategoryTheory.MonoidalCategory (C i)] (i : I),
  CategoryTheory.MonoidalCategoryStruct.tensorUnit ((i : I) → C i) i =
    CategoryTheory.MonoidalCategoryStruct.tensorUnit (C i)
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
/-- The underlying family of 2-morphisms.  -/
CategoryTheory.Oplax.StrongTrans.Modification.app : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.OplaxFunctor B C} →
          {η θ : F ⟶ G} → CategoryTheory.Oplax.StrongTrans.Modification η θ → (a : B) → η.app a ⟶ θ.app a
-- Mathlib.Algebra.Group.Pi.Lemmas
/-- Semigroup homomorphism between the function spaces `I → α` and `I → β`, induced by a semigroup
homomorphism `f` between `α` and `β`.  -/
MulHom.compLeft : {α : Type u_5} → {β : Type u_6} → [inst : Mul α] → [inst_1 : Mul β] → (α →ₙ* β) → (I : Type u_7) → (I → α) →ₙ* I → β
-- Mathlib.CategoryTheory.Localization.SmallShiftedHom
/-- Given objects `X` and `Y` in a category `C`, this is the property that
all the types of morphisms from `X⟦a⟧` to `Y⟦b⟧` are `w`-small
in the localized category with respect to a class of morphisms `W`.  -/
CategoryTheory.Localization.HasSmallLocalizedShiftedHom : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    CategoryTheory.MorphismProperty C →
      (M : Type w') → [inst_1 : AddMonoid M] → [CategoryTheory.HasShift C M] → C → C → Prop
-- Mathlib.Algebra.DirectSum.Algebra
DirectSum.GAlgebra.toFun : {ι : Type uι} →
  {R : Type uR} →
    {A : ι → Type uA} →
      {inst : CommSemiring R} →
        {inst_1 : (i : ι) → AddCommMonoid (A i)} →
          {inst_2 : (i : ι) → Module R (A i)} →
            {inst_3 : AddMonoid ι} → {inst_4 : DirectSum.GSemiring A} → [self : DirectSum.GAlgebra R A] → R →+ A 0
-- Mathlib.Order.Filter.AtTopBot.Archimedean
atBot_hasCountableBasis_of_archimedean : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : PartialOrder R] [IsOrderedRing R] [Archimedean R],
  Filter.atBot.HasCountableBasis (fun x => True) fun m => Set.Iic ↑m
-- Mathlib.Analysis.Calculus.ContDiff.Defs
ContDiff.contDiffOn : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {n : WithTop ℕ∞}, ContDiff 𝕜 n f → ContDiffOn 𝕜 n f s
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.contains_maxKey? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {km : α},
  t.maxKey? = some km → t.contains km = true
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.C_injective : ∀ (σ : Type u_2) (R : Type u_3) [inst : CommSemiring R], Function.Injective ⇑MvPolynomial.C
-- Init.Core
/-- `a ∪ b` is the union of `a` and `b`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∪` in identifiers is `union`. -/
Union.union : {α : Type u} → [self : Union α] → α → α → α
-- Mathlib.Topology.NhdsSet
nhdsSet_union : ∀ {X : Type u_2} [inst : TopologicalSpace X] (s t : Set X), nhdsSet (s ∪ t) = nhdsSet s ⊔ nhdsSet t
-- Mathlib.GroupTheory.Coxeter.Inversion
CoxeterSystem.IsReduced.nodup_leftInvSeq : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {ω : List B},
  cs.IsReduced ω → (cs.leftInvSeq ω).Nodup
-- Mathlib.Analysis.Normed.MulAction
Metric.smul_image_ball : ∀ {α : Type u_1} {β : Type u_2} [inst : NormedDivisionRing α] [inst_1 : SeminormedAddCommGroup β] [inst_2 : Module α β]
  [NormSMulClass α β] {s : α},
  s ≠ 0 → ∀ (x : β) (ε : ℝ), (fun x => s • x) '' Metric.ball x ε = Metric.ball (s • x) (‖s‖ * ε)
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.instSetLike : (R : Type u) →
  (L : Type v) → [inst : CommRing R] → [inst_1 : LieRing L] → [inst_2 : LieAlgebra R L] → SetLike (LieSubalgebra R L) L
-- Mathlib.CategoryTheory.SmallObject.WellOrderInductionData
/-- An element in `F.obj (op j)`, which, by restriction, induces elements
in `F.obj (op i)` for all `i ≤ j`.  -/
CategoryTheory.Functor.WellOrderInductionData.Extension.val : {J : Type u} →
  [inst : LinearOrder J] →
    [inst_1 : SuccOrder J] →
      {F : CategoryTheory.Functor Jᵒᵖ (Type v)} →
        {d : F.WellOrderInductionData} →
          [inst_2 : OrderBot J] → {val₀ : F.obj (Opposite.op ⊥)} → {j : J} → d.Extension val₀ j → F.obj (Opposite.op j)
-- Mathlib.Algebra.Group.Subgroup.Ker
MonoidHom.range_one : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N], MonoidHom.range 1 = ⊥
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.liftHom.eq_1 : ∀ {B : Type u₁} [inst : Quiver B] {C : Type u₂} [inst_1 : CategoryTheory.CategoryStruct.{v₂, u₂} C] (F : B ⥤q C)
  (x x_1 : CategoryTheory.FreeBicategory B) (f : x ⟶ x_1),
  CategoryTheory.FreeBicategory.liftHom F (CategoryTheory.FreeBicategory.Hom.of f) = F.map f
-- Mathlib.CategoryTheory.Subobject.NoetherianObject
CategoryTheory.isEventuallyConstant_of_isNoetherianObject : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} [CategoryTheory.IsNoetherianObject X]
  (F : CategoryTheory.Functor ℕ (CategoryTheory.MonoOver X)), CategoryTheory.IsFiltered.IsEventuallyConstant F
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.mk_coe' : ∀ {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₃ : Type u_11} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M] [inst_5 : Module S M₃] {σ : R →+* S}
  (f : M →ₛₗ[σ] M₃) (h : ∀ (m : R) (x : M), f.toFun (m • x) = σ m • f.toFun x),
  { toAddHom := f.toAddHom, map_smul' := h } = f
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.formatExtendedDayPeriod : Vector String 6 → Std.Time.ExtendedDayPeriod → String
-- Mathlib.RingTheory.DividedPowers.Basic
DividedPowers.mul_dpow : ∀ {A : Type u_1} [inst : CommSemiring A] {I : Ideal A} (self : DividedPowers I) {m n : ℕ} {x : A},
  x ∈ I → self.dpow m x * self.dpow n x = ↑((m + n).choose m) * self.dpow (m + n) x
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
add_neg_lt_add_neg_iff : ∀ {α : Type u} [inst : AddCommGroup α] [inst_1 : LT α] [AddLeftStrictMono α] {a b c d : α},
  a + -b < c + -d ↔ a + d < c + b
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.mem_span_insert : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {x : M} {s : Set M}
  {y : M}, x ∈ Submodule.span R (insert y s) ↔ ∃ a, ∃ z ∈ Submodule.span R s, x = a • y + z
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective
Matrix.ProjGenLinGroup.map_mk : ∀ {n : Type u_1} {R : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing R] {S : Type u_4}
  [inst_3 : CommRing S] (f : R →+* S) (g : GL n R),
  (Matrix.ProjGenLinGroup.map f) (Matrix.ProjGenLinGroup.mk g) =
    Matrix.ProjGenLinGroup.mk ((Matrix.GeneralLinearGroup.map f) g)
-- Init.Data.Iterators.Lemmas.Combinators.Take
_private.Init.Data.Iterators.Lemmas.Combinators.Take.0.Std.IterM.step_take.match_3.eq_2 : ∀ (motive : ℕ → Sort u_1) (k : ℕ) (h_1 : Unit → motive 0) (h_2 : (k : ℕ) → motive k.succ),
  (match k.succ with
    | 0 => h_1 ()
    | k.succ => h_2 k) =
    h_2 k
-- Mathlib.Analysis.Normed.Algebra.Exponential
/-- In a normed algebra `𝔸` over `𝕂 = ℝ` or `𝕂 = ℂ`, the series defining the exponential map
has an infinite radius of convergence.  -/
NormedSpace.expSeries_radius_eq_top : ∀ (𝕂 : Type u_1) (𝔸 : Type u_2) [inst : NontriviallyNormedField 𝕂] [inst_1 : CharZero 𝕂] [ContinuousSMul ℚ 𝕂]
  [inst_3 : NormedRing 𝔸] [inst_4 : NormedAlgebra 𝕂 𝔸], (NormedSpace.expSeries 𝕂 𝔸).radius = ⊤
-- Mathlib.Algebra.Group.Equiv.Opposite
/-- An additive semigroup homomorphism `f : AddHom M N` such that `f x` additively
commutes with `f y` for all `x`, `y` defines an additive semigroup homomorphism from `Mᵃᵒᵖ`.  -/
AddHom.fromOpposite : {M : Type u_3} →
  {N : Type u_4} →
    [inst : Add M] → [inst_1 : Add N] → (f : M →ₙ+ N) → (∀ (x y : M), AddCommute (f x) (f y)) → Mᵃᵒᵖ →ₙ+ N
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
CategoryTheory.Bicategory.mateEquiv_eq_iff : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {c d e f : B} {g : c ⟶ e} {h : d ⟶ f} {l₁ : c ⟶ d} {r₁ : d ⟶ c}
  {l₂ : e ⟶ f} {r₂ : f ⟶ e} (adj₁ : CategoryTheory.Bicategory.Adjunction l₁ r₁)
  (adj₂ : CategoryTheory.Bicategory.Adjunction l₂ r₂)
  (α : CategoryTheory.CategoryStruct.comp g l₂ ⟶ CategoryTheory.CategoryStruct.comp l₁ h)
  (β : CategoryTheory.CategoryStruct.comp r₁ g ⟶ CategoryTheory.CategoryStruct.comp h r₂),
  (CategoryTheory.Bicategory.mateEquiv adj₁ adj₂) α = β ↔
    adj₁.homEquiv₁.symm β =
      CategoryTheory.CategoryStruct.comp (adj₂.homEquiv₂ α) (CategoryTheory.Bicategory.associator l₁ h r₂).hom
-- Mathlib.Analysis.Complex.OpenMapping
/-- The *open mapping theorem* for holomorphic functions, local version: is a function `g : E → ℂ`
is analytic at a point `z₀`, then either it is constant in a neighborhood of `z₀`, or it maps every
neighborhood of `z₀` to a neighborhood of `z₀`. For the particular case of a holomorphic function on
`ℂ`, see `AnalyticAt.eventually_constant_or_nhds_le_map_nhds_aux`.  -/
AnalyticAt.eventually_constant_or_nhds_le_map_nhds : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {g : E → ℂ} {z₀ : E},
  AnalyticAt ℂ g z₀ → (∀ᶠ (z : E) in nhds z₀, g z = g z₀) ∨ nhds (g z₀) ≤ Filter.map g (nhds z₀)
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.prod_sum_index : ∀ {α : Type u_1} {β : Type u_7} {M : Type u_8} {N : Type u_10} {P : Type u_11} [inst : Zero M]
  [inst_1 : AddCommMonoid N] [inst_2 : CommMonoid P] {f : α →₀ M} {g : α → M → β →₀ N} {h : β → N → P},
  (∀ (a : β), h a 0 = 1) →
    (∀ (a : β) (b₁ b₂ : N), h a (b₁ + b₂) = h a b₁ * h a b₂) → (f.sum g).prod h = f.prod fun a b => (g a b).prod h
-- Mathlib.AlgebraicTopology.SimplexCategory.MorphismProperty
SimplexCategory.morphismProperty_eq_top : ∀ (W : CategoryTheory.MorphismProperty SimplexCategory) [W.IsMultiplicative],
  (∀ {n : ℕ} (i : Fin (n + 2)), W (SimplexCategory.δ i)) →
    (∀ {n : ℕ} (i : Fin (n + 1)), W (SimplexCategory.σ i)) → W = ⊤
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey!_ofList_of_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : Inhabited α] {l : List (α × β)}
  {k k' : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l →
      k ∈ List.map Prod.fst l → (Std.TreeMap.Raw.ofList l cmp).getKey! k' = k
-- Mathlib.AlgebraicGeometry.StructureSheaf
/-- The canonical ring homomorphism interpreting an element of `R` as an element of
the stalk of `structureSheaf R` at `x`.  -/
AlgebraicGeometry.StructureSheaf.toStalk : (R : Type u) →
  [inst : CommRing R] →
    (x : ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) →
      CommRingCat.of R ⟶ (AlgebraicGeometry.structurePresheafInCommRingCat R).stalk x
-- Mathlib.Algebra.Star.CentroidHom
/-- The canonical homomorphism from the center into the centroid  -/
CentroidHom.starCenterToCentroid : {α : Type u_1} →
  [inst : NonUnitalNonAssocSemiring α] →
    [inst_1 : StarRing α] → ↥(NonUnitalStarSubsemiring.center α) →⋆ₙ+* CentroidHom α
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getD_toList_roo_eq_fallback : ∀ {m n i fallback : ℕ}, n ≤ i + (m + 1) → (m<...n).toList.getD i fallback = fallback
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
/-- If the total masses of finite measures tend to zero, then the measures tend to zero.  -/
MeasureTheory.FiniteMeasure.tendsto_zero_of_tendsto_zero_mass : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [inst_2 : OpensMeasurableSpace Ω]
  {γ : Type u_3} {F : Filter γ} {μs : γ → MeasureTheory.FiniteMeasure Ω},
  Filter.Tendsto (fun i => (μs i).mass) F (nhds 0) → Filter.Tendsto μs F (nhds 0)
-- Mathlib.RepresentationTheory.Action
/-- This a type-changing equivalence (which requires a non-trivial proof that
`LinearEquiv.refl _ _` is `G`-equivariant) to avoid abusing defeq.  -/
Representation.linearizeTrivialIso : (k : Type u) →
  (G : Type v) →
    [inst : Monoid G] →
      [inst_1 : Semiring k] →
        (X : Type w) →
          (Representation.linearize k G (Action.trivial G X)).Equiv (Representation.trivial k G (MonoidAlgebra k X))
-- Mathlib.Algebra.Ring.Hom.Defs
NonUnitalRingHom.coe_mulHom_mk : ∀ {α : Type u_2} {β : Type u_3} [inst : NonUnitalNonAssocSemiring α] [inst_1 : NonUnitalNonAssocSemiring β] (f : α → β)
  (h₁ : ∀ (x y : α), f (x * y) = f x * f y) (h₂ : { toFun := f, map_mul' := h₁ }.toFun 0 = 0)
  (h₃ :
    ∀ (x y : α),
      { toFun := f, map_mul' := h₁ }.toFun (x + y) =
        { toFun := f, map_mul' := h₁ }.toFun x + { toFun := f, map_mul' := h₁ }.toFun y),
  ↑{ toFun := f, map_mul' := h₁, map_zero' := h₂, map_add' := h₃ } = { toFun := f, map_mul' := h₁ }
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Affine.Simplex.nonempty : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_5} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P], Nonempty (Affine.Simplex k P 0)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.arccos_zero : Real.arccos 0 = Real.pi / 2
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy
CategoryTheory.Arrow.RightHomotopy.refl_hom : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] [inst_1 : CategoryTheory.Preadditive V]
  {u v : CategoryTheory.Arrow V} (f : u ⟶ v), (CategoryTheory.Arrow.RightHomotopy.refl f).hom = 0
-- Mathlib.Algebra.Group.End
Equiv.Perm.self_trans_inv : ∀ {α : Type u_4} (e : Equiv.Perm α), Equiv.trans e e⁻¹ = 1
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- If `s` is a colimit binary cofan over `X` and `Y`, then every pair of morphisms `f : X ⟶ W` and
`g : Y ⟶ W` induces a morphism `l : s.pt ⟶ W` satisfying `s.inl ≫ l = f` and `s.inr ≫ l = g`.
 -/
CategoryTheory.Limits.BinaryCofan.IsColimit.desc' : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {W X Y : C} →
      {s : CategoryTheory.Limits.BinaryCofan X Y} →
        CategoryTheory.Limits.IsColimit s →
          (f : X ⟶ W) →
            (g : Y ⟶ W) →
              { l // CategoryTheory.CategoryStruct.comp s.inl l = f ∧ CategoryTheory.CategoryStruct.comp s.inr l = g }
-- Mathlib.CategoryTheory.Triangulated.Functor
CategoryTheory.Functor.mapTriangleCompIso_hom_app_hom₃ : ∀ {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]
  [inst_3 : CategoryTheory.HasShift C ℤ] [inst_4 : CategoryTheory.HasShift D ℤ] [inst_5 : CategoryTheory.HasShift E ℤ]
  (F : CategoryTheory.Functor C D) [inst_6 : F.CommShift ℤ] (G : CategoryTheory.Functor D E) [inst_7 : G.CommShift ℤ]
  (X : CategoryTheory.Pretriangulated.Triangle C),
  ((F.mapTriangleCompIso G).hom.app X).hom₃ = CategoryTheory.CategoryStruct.id (G.obj (F.obj X.obj₃))
-- Lean.Meta.Match.Basic
Lean.Meta.Match.Pattern : Type
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.containsThenInsert.size.eq_2 : ∀ {α : Type u} {β : α → Type v} (size : ℕ) (k' : α) (v' : β k') (l' r' : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.containsThenInsert.size (Std.DTreeMap.Internal.Impl.inner size k' v' l' r') = size
-- Mathlib.Data.FinEnum
/-- Any two enumerations of the same type have the same length.  -/
FinEnum.card_unique : ∀ {α : Type u} (e₁ e₂ : FinEnum α), FinEnum.card α = FinEnum.card α
-- Mathlib.Algebra.Homology.ShortComplex.Exact
/-- The obvious splitting of a short complex when `S.f` is an isomorphism and `S.X₃` is zero.  -/
CategoryTheory.ShortComplex.Splitting.ofIsIsoOfIsZero : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      (S : CategoryTheory.ShortComplex C) → CategoryTheory.IsIso S.f → CategoryTheory.Limits.IsZero S.X₃ → S.Splitting
-- Mathlib.Data.Finset.Card
Set.BijOn.finsetCard_eq : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} (e : α → β), Set.BijOn e ↑s ↑t → s.card = t.card
-- Mathlib.Probability.Kernel.Disintegration.CondCDF
ProbabilityTheory.withDensity_preCDF : ∀ {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) (r : ℚ) [MeasureTheory.IsFiniteMeasure ρ],
  ρ.fst.withDensity (ProbabilityTheory.preCDF ρ r) = ρ.IicSnd ↑r
-- Lean.LibrarySuggestions.Basic
/-- The score of the suggestion, as a probability that this suggestion should be used.
 -/
Lean.LibrarySuggestions.Suggestion.score : Lean.LibrarySuggestions.Suggestion → Float
-- Mathlib.RingTheory.Localization.Away.Basic
/-- `selfZPow x (m : ℤ)` is `x ^ m` as an element of the localization away from `x`.  -/
selfZPow : {R : Type u_1} →
  [inst : CommSemiring R] →
    (x : R) → (B : Type u_2) → [inst_1 : CommSemiring B] → [inst_2 : Algebra R B] → [IsLocalization.Away x B] → ℤ → B
-- Mathlib.RingTheory.Artinian.Module
IsArtinian.eq_1 : ∀ (R : Type u_1) (M : Type u_2) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  IsArtinian R M = WellFoundedLT (Submodule R M)
-- Mathlib.Analysis.Analytic.CPolynomialDef
/-- Given a function `f : E → F`, we say that `f` is continuously polynomial on a set `s`
if it is continuously polynomial around every point of `s`.  -/
CPolynomialOn : (𝕜 : Type u_1) →
  {E : Type u_2} →
    {F : Type u_3} →
      [inst : NontriviallyNormedField 𝕜] →
        [inst_1 : NormedAddCommGroup E] →
          [NormedSpace 𝕜 E] → [inst_3 : NormedAddCommGroup F] → [NormedSpace 𝕜 F] → (E → F) → Set E → Prop
-- Mathlib.NumberTheory.SiegelsLemma
_private.Mathlib.NumberTheory.SiegelsLemma.0.Int.Matrix.card_T_eq : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : Fintype β] (A : Matrix α β ℤ) [inst_2 : DecidableEq β],
  (Finset.Icc 0 fun x =>
        ↑⌊(↑(Fintype.card β) * max 1 ‖A‖) ^ (↑(Fintype.card α) / (↑(Fintype.card β) - ↑(Fintype.card α)))⌋₊).card =
    (⌊(↑(Fintype.card β) * max 1 ‖A‖) ^ (↑(Fintype.card α) / (↑(Fintype.card β) - ↑(Fintype.card α)))⌋₊ + 1) ^
      Fintype.card β
-- Mathlib.CategoryTheory.Square
/-- The equivalence `Square C ≌ Arrow (Arrow C)` which sends a
commutative square `sq` to the obvious arrow from the left morphism of `sq`
to the right morphism of `sq`.  -/
CategoryTheory.Square.arrowArrowEquivalence : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Square C ≌ CategoryTheory.Arrow (CategoryTheory.Arrow C)
-- Mathlib.Algebra.Lie.SerreConstruction
/-- The terms corresponding to the `ad F`-relations.  -/
CartanMatrix.Relations.adF : (R : Type u) → {B : Type v} → [inst : CommRing R] → Matrix B B ℤ → B × B → FreeLieAlgebra R (CartanMatrix.Generators B)
-- Std.Data.Internal.List.Associative
Std.Internal.List.maxKeyD_alterKey_eq_self : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [inst_3 : Std.LawfulBEqOrd α]
  [inst_4 : Std.LawfulEqOrd α] {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α} {f : Option (β k) → Option (β k)} {fallback : α},
      (Std.Internal.List.alterKey k f l).isEmpty = false →
        (Std.Internal.List.maxKeyD (Std.Internal.List.alterKey k f l) fallback = k ↔
          (f (Std.Internal.List.getValueCast? k l)).isSome = true ∧
            ∀ (k' : α), Std.Internal.List.containsKey k' l = true → (compare k' k).isLE = true)