mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Fintype.Quotient
Quotient.map.congr_simp : ∀ {α : Sort u_1} {β : Sort u_2} {sa : Setoid α} {sb : Setoid β} (f f_1 : α → β) (e_f : f = f_1)
  (h : ∀ ⦃a b : α⦄, a ≈ b → f a ≈ f b) (a a_1 : Quotient sa), a = a_1 → Quotient.map f h a = Quotient.map f_1 ⋯ a_1
-- Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
/-- Upgrading `PiTensorProduct.mapL` to a `MonoidHom` when `E = E'`.  -/
PiTensorProduct.mapLMonoidHom : {ι : Type u_1} →
  [inst : Fintype ι] →
    {𝕜 : Type u_2} →
      {E : ι → Type u_3} →
        [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] →
          [inst_2 : NontriviallyNormedField 𝕜] →
            [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)] →
              ((i : ι) → E i →L[𝕜] E i) →* (PiTensorProduct 𝕜 fun i => E i) →L[𝕜] PiTensorProduct 𝕜 fun i => E i
-- Mathlib.Algebra.Group.ModEq
AddCommGroup.add_modEq_left : ∀ {M : Type u_1} [inst : AddCancelCommMonoid M] {a b p : M}, a + b ≡ a [PMOD p] ↔ b ≡ 0 [PMOD p]
-- Std.Http.Data.URI.Basic
/-- Finds the first value of a query parameter by key name. Returns `none` if the key is not found.
The value remains encoded as `EncodedQueryParam`.
 -/
Std.Http.URI.Query.findEncoded? : Std.Http.URI.Query → Std.Http.URI.EncodedQueryParam → Option (Option Std.Http.URI.EncodedQueryParam)
-- Mathlib.RingTheory.Congruence.Hom
/-- Given ring congruence relations `c, d` on a ring such that `d` contains `c`,
`d`'s quotient map induces a homomorphism from the quotient by `c` to the
quotient by `d`.  -/
RingCon.map : {M : Type u_1} → [inst : NonAssocSemiring M] → (c d : RingCon M) → c ≤ d → c.Quotient →+* d.Quotient
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.den_mem : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A] {𝒜 : ι → σ} {x : Submonoid A}
  (f : HomogeneousLocalization 𝒜 x), f.den ∈ x
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem?_toList_roo : ∀ {m n i : ℕ}, (m<...n).toList[i]? = if i < n - (m + 1) then some (m + 1 + i) else none
-- Mathlib.Data.Fin.Fin2
_private.Mathlib.Data.Fin.Fin2.0.Fin2.add.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → ((k : ℕ) → motive k.succ) → motive x
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getKey!_unitOfList_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α] [inst_2 : Inhabited α]
  {l : List α} {k k' : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a == b) = false) l → k ∈ l → (Std.ExtDHashMap.Const.unitOfList l).getKey! k' = k
-- Init.Data.Vector.Lemmas
Vector.any_map : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {f : α → β} {xs : Vector α n} {p : β → Bool},
  (Vector.map f xs).any p = xs.any (p ∘ f)
-- Mathlib.RepresentationTheory.Homological.Resolution
/-- The `k`-linear map underlying the differential in the standard resolution of `k` as a trivial
`k`-linear `G`-representation. It sends `(g₀, ..., gₙ) ↦ ∑ (-1)ⁱ • (g₀, ..., ĝᵢ, ..., gₙ)`.  -/
Rep.standardComplex.d : (k : Type u) →
  [inst : CommRing k] → (G : Type u) → (n : ℕ) → MonoidAlgebra k (Fin (n + 1) → G) →ₗ[k] MonoidAlgebra k (Fin n → G)
-- Mathlib.RingTheory.Localization.Basic
Localization.r_iff_of_le_nonZeroDivisors : ∀ {R : Type u_1} [inst : CommRing R] {M : Submonoid R},
  M ≤ nonZeroDivisors R → ∀ (a c : R) (b d : ↥M), (Localization.r M) (a, b) (c, d) ↔ a * ↑d = ↑b * c
-- Init.Data.String.Defs
String.singleton.eq_1 : ∀ (c : Char), String.singleton c = "".push c
-- Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex
/-- `n`-simplices in `Δ[p] ⊗ Δ[q]` identify to order preserving maps
`Fin (n + 1) →o Fin (p + 1) × Fin (q + 1)`.  -/
SSet.prodStdSimplex.objEquiv : {p q n : ℕ} →
  (CategoryTheory.MonoidalCategoryStruct.tensorObj (SSet.stdSimplex.obj { len := p })
          (SSet.stdSimplex.obj { len := q })).obj
      (Opposite.op { len := n }) ≃
    (Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))
-- Mathlib.GroupTheory.GroupAction.Hom
MulDistribMulActionHomClass.eq_1 : ∀ (F : Type u_10) (M : Type u_11) (A : Type u_12) (B : Type u_13) [inst : Monoid M] [inst_1 : Monoid A]
  [inst_2 : Monoid B] [inst_3 : MulDistribMulAction M A] [inst_4 : MulDistribMulAction M B] [inst_5 : FunLike F A B],
  MulDistribMulActionHomClass F M A B = MulDistribMulActionSemiHomClass F (⇑(MonoidHom.id M)) A B
-- Mathlib.Tactic.Linarith.Frontend
Mathlib.Tactic.Linarith.LinarithConfig.mk.sizeOf_spec : ∀ (discharger : Lean.Elab.Tactic.TacticM Unit) (exfalso : Bool) (transparency : Lean.Meta.TransparencyMode)
  (splitHypotheses splitNe minimize : Bool) (preprocessors : List Mathlib.Tactic.Linarith.GlobalBranchingPreprocessor)
  (oracle : Mathlib.Tactic.Linarith.CertificateOracle),
  sizeOf
      { discharger := discharger, exfalso := exfalso, transparency := transparency, splitHypotheses := splitHypotheses,
        splitNe := splitNe, minimize := minimize, preprocessors := preprocessors, oracle := oracle } =
    1 + sizeOf exfalso + sizeOf transparency + sizeOf splitHypotheses + sizeOf splitNe + sizeOf minimize +
        sizeOf preprocessors +
      sizeOf oracle
-- Std.Data.DHashMap.Raw
_private.Std.Data.DHashMap.Raw.0.Std.DHashMap.Raw.containsThenInsertIfNew.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Raw α β) (a : α) (b : β a),
  m.containsThenInsertIfNew a b =
    if h : 0 < m.buckets.size then
      match Std.DHashMap.Internal.Raw₀.containsThenInsertIfNew ⟨m, h⟩ a b with
      | (previous, ⟨r, property⟩) => (previous, r)
    else (false, m)
-- Mathlib.FieldTheory.IsAlgClosed.Basic
/-- A (random) isomorphism between an algebraic closure of `K` and an algebraic closure
of an algebraic extension of `K`  -/
IsAlgClosure.equivOfAlgebraic : (K : Type u_1) →
  (J : Type u_2) →
    (L : Type v) →
      (M : Type w) →
        [inst : Field K] →
          [inst_1 : Field J] →
            [inst_2 : Field L] →
              [inst_3 : Field M] →
                [inst_4 : Algebra K M] →
                  [IsAlgClosure K M] →
                    [inst_6 : Algebra K J] →
                      [inst_7 : Algebra J L] →
                        [IsAlgClosure J L] →
                          [inst_9 : Algebra K L] → [IsScalarTower K J L] → [Algebra.IsAlgebraic K J] → L ≃ₐ[K] M
-- Mathlib.GroupTheory.DoubleCoset
DoubleCoset.left_bot_eq_left_quot : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G), DoubleCoset.Quotient ↑⊥ ↑H = (G ⧸ H)
-- Mathlib.GroupTheory.Submonoid.Inverses
AddSubmonoid.leftNeg_leftNeg_eq : ∀ {M : Type u_1} [inst : AddMonoid M], ∀ S ≤ IsAddUnit.addSubmonoid M, S.leftNeg.leftNeg = S
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxc.Iterator.instFinite : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LE α] [inst_2 : DecidableLE α]
  [Std.PRange.LawfulUpwardEnumerable α] [Std.Rxc.IsAlwaysFinite α], Std.Iterators.Finite (Std.Rxc.Iterator α) Id
-- Lean.Util.Trace
Lean.MonadTrace.mk : {m : Type → Type} →
  ((Lean.TraceState → Lean.TraceState) → m Unit) →
    m Lean.TraceState →
      autoParam (m (Std.HashSet Lean.Name)) Lean.MonadTrace.getInheritedTraceOptions._autoParam → Lean.MonadTrace m
-- Mathlib.Logic.UnivLE
UnivLE.trans : ∀ [UnivLE.{u, v}] [UnivLE.{v, w}], UnivLE.{u, w}
-- Mathlib.Topology.Algebra.Algebra.Equiv
ContinuousAlgEquiv.continuousAlgEquivClass : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : TopologicalSpace A] [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A]
  [inst_6 : Algebra R B], ContinuousAlgEquivClass (A ≃A[R] B) R A B
-- Mathlib.Testing.Plausible.Sampleable
Plausible.Rat.Arbitrary : Plausible.Arbitrary ℚ
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.closedCell.eq_1 : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : Topology.RelCWComplex C D] (n : ℕ)
  (i : Topology.RelCWComplex.cell C n),
  Topology.RelCWComplex.closedCell n i = ↑(Topology.RelCWComplex.map n i) '' Metric.closedBall 0 1
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.colimit.pre_id : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Limits.HasColimitsOfShape J C] (F : CategoryTheory.Functor J C),
  CategoryTheory.Limits.colimit.pre F (CategoryTheory.Functor.id J) = CategoryTheory.Limits.colim.map F.leftUnitor.hom
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.get!_inter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  [inst_2 : Inhabited α] {k : α}, (m₁ ∩ m₂).get! k = if k ∈ m₂ then m₁.get! k else default
-- Mathlib.AlgebraicGeometry.Morphisms.LocalClosure
AlgebraicGeometry.sourceLocalClosure.instContainsIdentitiesScheme : ∀ {W P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [W.IsStableUnderBaseChange] [W.ContainsIdentities]
  [P.ContainsIdentities], (AlgebraicGeometry.sourceLocalClosure W P).ContainsIdentities
-- Lean.Meta.Tactic.Simp.Simproc
Lean.Meta.Simp.SimprocDecl.declName : Lean.Meta.Simp.SimprocDecl → Lean.Name
-- Aesop.Stats.Basic
Aesop.ScriptGenerated.Method : Type
-- Mathlib.LinearAlgebra.Eigenspace.Basic
Module.End.eigenspace_mem_invtSubmodule : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (f : Module.End R M)
  (μ : R), f.eigenspace μ ∈ f.invtSubmodule
-- Mathlib.GroupTheory.FiniteAbelian.Basic
AddSubgroup.finiteIndex_range_nsmulAddMonoidHom_of_fg : ∀ (A : Type u_1) [inst : AddCommGroup A] [AddGroup.FG A] {n : ℕ}, n ≠ 0 → (nsmulAddMonoidHom n).range.FiniteIndex
-- Init.Data.List.Count
List.count_pos_iff : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a : α} {l : List α}, 0 < List.count a l ↔ a ∈ l
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.Comonad.coassoc_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (self : CategoryTheory.Comonad C) (X : C) {Z : C}
  (h : self.obj (self.obj (self.obj X)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (self.δ.app X) (CategoryTheory.CategoryStruct.comp (self.map (self.δ.app X)) h) =
    CategoryTheory.CategoryStruct.comp (self.δ.app X) (CategoryTheory.CategoryStruct.comp (self.δ.app (self.obj X)) h)
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Matrix.diagonalInvertibleEquivInvertible_apply : ∀ {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α] (v : n → α)
  [inst_3 : Invertible (Matrix.diagonal v)],
  (Matrix.diagonalInvertibleEquivInvertible v) inst_3 = Matrix.invertibleOfDiagonalInvertible v
-- Mathlib.Topology.Order.WithTop
WithBot.tendsto_unbotA : ∀ {ι : Type u_1} [inst : LinearOrder ι] [inst_1 : TopologicalSpace ι] [inst_2 : OrderTopology ι] [inst_3 : Nonempty ι]
  {a : WithBot ι}, a ≠ ⊥ → Filter.Tendsto WithBot.unbotA (nhds a) (nhds a.unbotA)
-- Mathlib.CategoryTheory.Sites.MorphismProperty
CategoryTheory.MorphismProperty.precoverage_inf : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P Q : CategoryTheory.MorphismProperty C),
  (P ⊓ Q).precoverage = P.precoverage ⊓ Q.precoverage
-- Std.Data.Internal.List.Associative
Std.Internal.List.maxKey_eq_iff_getKey?_eq_self_and_forall : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {he : l.isEmpty = false} {km : α},
      Std.Internal.List.maxKey l he = km ↔
        Std.Internal.List.getKey? km l = some km ∧
          ∀ (k : α), Std.Internal.List.containsKey k l = true → (compare k km).isLE = true
-- Mathlib.CategoryTheory.Bicategory.LocallyGroupoid
CategoryTheory.Bicategory.Pith.mk : {B : Type u₁} → B → CategoryTheory.Bicategory.Pith B
-- Std.Data.ExtHashMap.Basic
Std.ExtHashMap.instEmptyCollection : {α : Type u} → {β : Type v} → [inst : BEq α] → [inst_1 : Hashable α] → EmptyCollection (Std.ExtHashMap α β)
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupSeminorm.instLattice : {E : Type u_3} → [inst : AddCommGroup E] → Lattice (AddGroupSeminorm E)
-- Mathlib.Algebra.Order.Ring.Archimedean
ArchimedeanClass.mk_zpow : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : Field R] [inst_2 : IsOrderedRing R] (n : ℤ) (x : R),
  ArchimedeanClass.mk (x ^ n) = n • ArchimedeanClass.mk x
-- Batteries.Lean.Except
Except.pmap_ok : ∀ {ε : Type u} {α β : Type v} (a : α) (f : (a' : α) → Except.ok a = Except.ok a' → β),
  (Except.ok a).pmap f = Except.ok (f a ⋯)
-- Mathlib.GroupTheory.Congruence.Opposite
/-- If `c` is a multiplicative congruence on `Mᵐᵒᵖ`, then `(a, b) ↦ c bᵒᵖ aᵒᵖ` is a multiplicative
congruence on `M`.  -/
Con.unop : {M : Type u_1} → [inst : Mul M] → Con Mᵐᵒᵖ → Con M
-- Mathlib.RingTheory.WittVector.Identities
WittVector.p_nonzero : ∀ (p : ℕ) (R : Type u_1) [hp : Fact (Nat.Prime p)] [inst : CommRing R] [Nontrivial R] [CharP R p], ↑p ≠ 0
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.AddGrp.instAddMonObj : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        {H : CategoryTheory.AddGrp C} → [CategoryTheory.IsCommAddMonObj H.X] → CategoryTheory.AddMonObj H
-- Init.Data.Array.Lemmas
Array.foldl_flatten : ∀ {β : Type u_1} {α : Type u_2} {f : β → α → β} {b : β} {xss : Array (Array α)},
  Array.foldl f b xss.flatten = Array.foldl (fun b xs => Array.foldl f b xs) b xss
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.monic_X_pow : ∀ {R : Type u} [inst : Semiring R] (n : ℕ), (Polynomial.X ^ n).Monic
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Affine.Simplex.span_eq_top : ∀ {k : Type u_1} {V : Type u_2} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [FiniteDimensional k V] {n : ℕ} (T : Affine.Simplex k V n),
  Module.finrank k V = n → affineSpan k (Set.range T.points) = ⊤
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.comp_left : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {P : CategoryTheory.MorphismProperty T}
  {Q : CategoryTheory.MorphismProperty A} {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative]
  [inst_4 : W.IsMultiplicative] {X Y Z : CategoryTheory.MorphismProperty.Comma L R P Q W} (f : X ⟶ Y) (g : Y ⟶ Z),
  (CategoryTheory.CategoryStruct.comp f g).left = CategoryTheory.CategoryStruct.comp f.left g.left
-- Mathlib.Order.CompleteLattice.Basic
/-- **Alias** of `sSup_sdiff_singleton_bot`. -/
sSup_diff_singleton_bot : ∀ {α : Type u_1} [inst : CompleteLattice α] (s : Set α), sSup (s \ {⊥}) = sSup s
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.degree_add_le : ∀ {R : Type u} [inst : Semiring R] (p q : Polynomial R), (p + q).degree ≤ max p.degree q.degree
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get?_eq_some_iff_exists_compare_eq_eq_and_mem_toArray : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k : α} {v : β},
      Std.DTreeMap.Raw.Const.get? t k = some v ↔
        ∃ k', cmp k k' = Ordering.eq ∧ (k', v) ∈ Std.DTreeMap.Raw.Const.toArray t
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.LetRecToLift.declName : Lean.Elab.Term.LetRecToLift → Lean.Name
-- Mathlib.Data.Finsupp.Defs
/-- **Alias** of `Finsupp.hasFiniteSupport`. -/
Finsupp.finite_support : ∀ {α : Type u_1} {M : Type u_4} [inst : Zero M] (f : α →₀ M), Function.HasFiniteSupport ⇑f
-- Mathlib.RingTheory.Multiplicity
FiniteMultiplicity.pow_dvd_iff_le_multiplicity : ∀ {α : Type u_1} [inst : Monoid α] {a b : α}, FiniteMultiplicity a b → ∀ {k : ℕ}, a ^ k ∣ b ↔ k ≤ multiplicity a b
-- Mathlib.GroupTheory.GroupAction.Blocks
MulAction.isBlock_iff_disjoint_smul_of_ne : ∀ {G : Type u_1} [inst : Group G] {X : Type u_2} [inst_1 : MulAction G X] {B : Set X},
  MulAction.IsBlock G B ↔ ∀ ⦃g : G⦄, g • B ≠ B → Disjoint (g • B) B
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.Equiv.getGE!_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [inst : Inhabited α] {k : α},
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.getGE! k = t₂.getGE! k
-- Mathlib.Algebra.Module.Submodule.RestrictScalars
Submodule.restrictScalars_iInf : ∀ (S : Type u_1) {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Semiring S]
  [inst_3 : Module S M] [inst_4 : Module R M] [inst_5 : SMul S R] [inst_6 : IsScalarTower S R M] {ι : Sort u_4}
  (s : ι → Submodule R M), Submodule.restrictScalars S (iInf s) = ⨅ i, Submodule.restrictScalars S (s i)
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
Matrix.charmatrix_blockTriangular_iff : ∀ {R : Type u_1} [inst : CommRing R] {n : Type u_4} [inst_1 : DecidableEq n] [inst_2 : Fintype n] {α : Type u_5}
  [inst_3 : Preorder α] {M : Matrix n n R} {b : n → α}, M.charmatrix.BlockTriangular b ↔ M.BlockTriangular b
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Connected
/-- (Implementation) Show that the raised cone is a limit.  -/
CategoryTheory.CostructuredArrow.CreatesConnected.isLimitRaiseCone : {J : Type u'} →
  [inst : CategoryTheory.Category.{v', u'} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {D : Type u_1} →
          [inst_2 : CategoryTheory.Category.{v_1, u_1} D] →
            {K : CategoryTheory.Functor C D} →
              [inst_3 : CategoryTheory.IsConnected J] →
                {B : D} →
                  {F : CategoryTheory.Functor J (CategoryTheory.CostructuredArrow K B)} →
                    {c : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.CostructuredArrow.proj K B))} →
                      CategoryTheory.Limits.IsLimit c →
                        CategoryTheory.Limits.IsLimit (CategoryTheory.CostructuredArrow.CreatesConnected.raiseCone c)
-- Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
PositiveLinearMap.norm_apply_le_of_nonneg : ∀ {B₁ : Type u_3} {B₂ : Type u_4} [inst : CStarAlgebra B₁] [inst_1 : CStarAlgebra B₂] [inst_2 : PartialOrder B₁]
  [inst_3 : PartialOrder B₂] [StarOrderedRing B₁] [StarOrderedRing B₂] (f : B₁ →ₚ[ℂ] B₂) (x : B₁),
  0 ≤ x → ‖f x‖ ≤ ‖f 1‖ * ‖x‖
-- Mathlib.RingTheory.HahnSeries.Basic
/-- **Alias** of `HahnSeries.ofSuppBddBelow_zero`. -/
HahnSeries.zero_ofSuppBddBelow : ∀ {Γ : Type u_1} {R : Type u_3} [inst : Zero R] [inst_1 : LinearOrder Γ] [inst_2 : LocallyFiniteOrder Γ]
  [inst_3 : Nonempty Γ], HahnSeries.ofSuppBddBelow 0 ⋯ = 0
-- Mathlib.Order.Bounds.Basic
/-- If `s ⊆ t` and `t` is bounded below, then so is `s`.  -/
BddBelow.mono : ∀ {α : Type u_1} [inst : Preorder α] ⦃s t : Set α⦄, s ⊆ t → BddBelow t → BddBelow s
-- Mathlib.CategoryTheory.Triangulated.TStructure.Basic
CategoryTheory.Triangulated.TStructure.instIsStableUnderShiftBoundedInt : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C), t.bounded.IsStableUnderShift ℤ
-- Mathlib.Order.Defs.Unbundled
Equivalence.isTrans : ∀ {α : Sort u_1} (r : α → α → Prop), Equivalence r → IsTrans α r
-- Batteries.Data.Fin.Lemmas
Fin.findSome?_eq_some_iff : ∀ {n : ℕ} {α : Type u_1} {a : α} {f : Fin n → Option α},
  Fin.findSome? f = some a ↔ ∃ i, f i = some a ∧ ∀ j < i, f j = none
-- Mathlib.FieldTheory.RatFunc.Basic
_private.Mathlib.FieldTheory.RatFunc.Basic.0.RatFunc.num_div' : ∀ {K : Type u} [inst : Field K] (p : Polynomial K) {q : Polynomial K},
  q ≠ 0 →
    ((algebraMap (Polynomial K) (RatFunc K)) p / (algebraMap (Polynomial K) (RatFunc K)) q).num =
      Polynomial.C (q / gcd p q).leadingCoeff⁻¹ * (p / gcd p q)
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
/-- Given a pointwise left Kan extension of `F` along `L`, exhibits
`(LeftExtension.whiskerRight L F G).obj E` as a pointwise left Kan extension of `F ⋙ G` along
`L`.  -/
CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension.postcompose : {A : Type u_1} →
  {B : Type u_2} →
    {C : Type u_3} →
      {D : Type u_4} →
        [inst : CategoryTheory.Category.{v_1, u_1} A] →
          [inst_1 : CategoryTheory.Category.{v_2, u_2} B] →
            [inst_2 : CategoryTheory.Category.{v_3, u_3} C] →
              [inst_3 : CategoryTheory.Category.{v_4, u_4} D] →
                (G : CategoryTheory.Functor B D) →
                  {F : CategoryTheory.Functor A B} →
                    {L : CategoryTheory.Functor A C} →
                      [G.PreservesPointwiseLeftKanExtension F L] →
                        {E : L.LeftExtension F} →
                          E.IsPointwiseLeftKanExtension →
                            ((CategoryTheory.Functor.LeftExtension.postcompose₂ L F G).obj
                                E).IsPointwiseLeftKanExtension
-- Std.Time.Format.DateFormat
/-- Narrow extended-day-period strings for the `B` pattern.
Order: midnight, night, morning, noon, afternoon, evening.
 -/
Std.Time.DateFormatSymbols.extendedDayPeriodNarrow : Std.Time.DateFormatSymbols → Vector String 6
-- Mathlib.CategoryTheory.Preadditive.LeftExact
/-- A functor between preadditive categories preserves the equalizer of two
morphisms if it preserves all kernels.  -/
CategoryTheory.Functor.preservesEqualizer_of_preservesKernels : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D)
  [F.PreservesZeroMorphisms] [CategoryTheory.Limits.HasBinaryBiproducts C]
  [∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) F] {X Y : C}
  (f g : X ⟶ Y), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f g) F
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.Point.mk.eq_1 : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Affine R} [inst_1 : Nontrivial R]
  [inst_2 : WeierstrassCurve.IsElliptic W'] {x y : R} (h : W'.Equation x y),
  WeierstrassCurve.Affine.Point.mk h = WeierstrassCurve.Affine.Point.some x y ⋯
-- Mathlib.GroupTheory.Complement
/-- A left transversal is finite iff the subgroup has finite index.  -/
Subgroup.IsComplement.finite_left_iff : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} {S : Set G}, Subgroup.IsComplement S ↑H → (Finite ↑S ↔ H.FiniteIndex)
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Cfg.halt : List ℕ → Turing.ToPartrec.Cfg
-- Mathlib.RingTheory.Ideal.Over
Ideal.Quotient.stabilizerHom_apply : ∀ {A : Type u_3} {B : Type u_4} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] (P : Ideal B)
  (p : Ideal A) [inst_3 : P.LiesOver p] (G : Type u_6) [inst_4 : Group G] [inst_5 : MulSemiringAction G B]
  [inst_6 : SMulCommClass G A B] (g : ↥(MulAction.stabilizer G P)) (b : B),
  ((Ideal.Quotient.stabilizerHom P p G) g) ((Ideal.Quotient.mk P) b) = (Ideal.Quotient.mk P) (g • b)
-- Mathlib.CategoryTheory.MorphismProperty.Descent
CategoryTheory.MorphismProperty.DescendsAlong.inf : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P Q W : CategoryTheory.MorphismProperty C}
  [P.DescendsAlong Q] [W.DescendsAlong Q], (P ⊓ W).DescendsAlong Q
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
normEDS.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] (b c d : R) (n : ℤ),
  normEDS b c d n = preNormEDS (b ^ 4) c d n * if Even n then b else 1
-- Mathlib.GroupTheory.Commutator.Basic
zero_mem_addCommutatorSet : ∀ (G : Type u_1) [inst : AddGroup G], 0 ∈ addCommutatorSet G
-- Mathlib.CategoryTheory.Sites.LeftExact
CategoryTheory.instFinitaryExtensiveSheafOfHasPullbacksOfHasSheafify : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w}
  [inst_1 : CategoryTheory.Category.{w', w} D] [CategoryTheory.FinitaryExtensive D]
  [CategoryTheory.Limits.HasPullbacks D] [CategoryTheory.HasSheafify J D],
  CategoryTheory.FinitaryExtensive (CategoryTheory.Sheaf J D)