mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.ofList_eq_insertMany_empty : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {l : List ((a : α) × β a)}, Std.ExtDHashMap.ofList l = ∅.insertMany l
-- Std.Time.Format.Modifier
/-- `ExtendedDayPeriod` is a more granular day-period classification used by the `B` pattern,
subdividing the day into named English CLDR segments.
 -/
Std.Time.ExtendedDayPeriod : Type
-- Mathlib.RepresentationTheory.Coinvariants
Representation.Coinvariants.sub_mem_ker : ∀ {k : Type u_1} {G : Type u_2} {V : Type u_3} [inst : CommRing k] [inst_1 : Monoid G] [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] {ρ : Representation k G V} (g : G) (x : V), (ρ g) x - x ∈ Representation.Coinvariants.ker ρ
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.edge_vert : ∀ {V : Type u} {G : SimpleGraph V} (self : G.Subgraph) {v w : V}, self.Adj v w → v ∈ self.verts
-- Mathlib.Computability.EpsilonNFA
/-- **Alias** of the forward direction of `εNFA.isPath_nil`. -/
εNFA.IsPath.eq_of_nil : ∀ {α : Type u} {σ : Type v} (M : εNFA α σ) {s t : σ}, M.IsPath s t [] → s = t
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.arg_eq_nhds_of_re_neg_of_im_neg : ∀ {x : ℂ}, x.re < 0 → x.im < 0 → Complex.arg =ᶠ[nhds x] fun x => Real.arcsin ((-x).im / ‖x‖) - Real.pi
-- Mathlib.Topology.LocallyConstant.Basic
/-- Push forward of locally constant maps under any map, by post-composition.  -/
LocallyConstant.map : {X : Type u_1} →
  {Y : Type u_2} → {Z : Type u_3} → [inst : TopologicalSpace X] → (Y → Z) → LocallyConstant X Y → LocallyConstant X Z
-- Init.Data.UInt.Bitwise
USize.or_eq_zero_iff : ∀ {a b : USize}, a ||| b = 0 ↔ a = 0 ∧ b = 0
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.Subcomplex.isIso_toOfSimplex_iff : ∀ {X : SSet} {n : ℕ} (x : X.obj (Opposite.op { len := n })),
  CategoryTheory.IsIso (SSet.Subcomplex.toOfSimplex x) ↔ CategoryTheory.Mono (SSet.yonedaEquiv.symm x)
-- Mathlib.Topology.Algebra.Order.UpperLower
IsOpen.lowerClosure : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : Preorder α] [HasUpperLowerClosure α] {s : Set α},
  IsOpen s → IsOpen ↑(lowerClosure s)
-- Mathlib.Algebra.Order.Group.Lattice
inv_inf : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : Group α] [MulLeftMono α] [MulRightMono α] (a b : α), (a ⊓ b)⁻¹ = a⁻¹ ⊔ b⁻¹
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
CategoryTheory.Triangulated.TStructure.natTransTruncLEOfLE_trans_app : ∀ {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) (a b c : ℤ) (hab : a ≤ b) (hbc : b ≤ c) (X : C),
  CategoryTheory.CategoryStruct.comp ((t.natTransTruncLEOfLE a b hab).app X) ((t.natTransTruncLEOfLE b c hbc).app X) =
    (t.natTransTruncLEOfLE a c ⋯).app X
-- Mathlib.RingTheory.DividedPowers.Basic
/-- A more general of `DividedPowers.exp_add`  -/
DividedPowers.exp_add' : ∀ {A : Type u_1} [inst : CommSemiring A] {a b : A} (dp : ℕ → A → A),
  (∀ (n : ℕ), dp n (a + b) = ∑ k ∈ Finset.HasAntidiagonal.antidiagonal n, dp k.1 a * dp k.2 b) →
    (PowerSeries.mk fun n => dp n (a + b)) = (PowerSeries.mk fun n => dp n a) * PowerSeries.mk fun n => dp n b
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.Opens.mk.congr_simp : ∀ {α : Type u_2} [inst : TopologicalSpace α] (carrier carrier_1 : Set α) (e_carrier : carrier = carrier_1)
  (is_open' : IsOpen carrier), { carrier := carrier, is_open' := is_open' } = { carrier := carrier_1, is_open' := ⋯ }
-- Lean.Data.Lsp.Extra
Lean.Lsp.WaitForDiagnosticsParams.mk.injEq : ∀ (uri : Lean.Lsp.DocumentUri) (version : ℕ) (uri_1 : Lean.Lsp.DocumentUri) (version_1 : ℕ),
  ({ uri := uri, version := version } = { uri := uri_1, version := version_1 }) = (uri = uri_1 ∧ version = version_1)
-- Mathlib.AlgebraicTopology.SimplicialSet.Op
SSet.σ_opObjEquiv : ∀ (X : SSet) {n : ℕ} (i : Fin (n + 1)) (x : X.op.obj (Opposite.op { len := n })),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.σ X i)) (SSet.opObjEquiv x) =
    SSet.opObjEquiv ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.σ X.op i.rev)) x)
-- Mathlib.RingTheory.Localization.Integer
/-- We can clear the denominators of a finite set of fractions.  -/
IsLocalization.exist_integer_multiples_of_finset : ∀ {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] (s : Finset S), ∃ b, ∀ a ∈ s, IsLocalization.IsInteger R (↑b • a)
-- Mathlib.Topology.Defs.Sequences
/-- The sequential closure of a set `s : Set X` in a topological space `X` is the set of all `a : X`
which arise as limit of sequences in `s`. Note that the sequential closure of a set is not
guaranteed to be sequentially closed.  -/
seqClosure : {X : Type u_1} → [TopologicalSpace X] → Set X → Set X
-- Mathlib.Topology.Order.UpperLowerSetTopology
/-- A monotone map between preorders spaces induces a continuous map between themselves considered
with the lower set topology.  -/
Topology.WithLowerSet.map : {α : Type u_1} →
  {β : Type u_2} →
    [inst : Preorder α] → [inst_1 : Preorder β] → (α →o β) → C(Topology.WithLowerSet α, Topology.WithLowerSet β)
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
CFC.posPart_neg : ∀ {A : Type u_1} [inst : NonUnitalRing A] [inst_1 : Module ℝ A] [inst_2 : SMulCommClass ℝ A A]
  [inst_3 : IsScalarTower ℝ A A] [inst_4 : StarRing A] [inst_5 : TopologicalSpace A]
  [inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [T2Space A] (a : A), (-a)⁺ = a⁻
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
/-- Given a pseudofunctor `F` from `LocallyDiscrete Cᵒᵖ` to `Cat`, and a family of
morphisms `f i : X i ⟶ S`, the objects of the category of descent data for
the `X i` relative to the morphisms `f i` consist of families of
objects `obj i` in `F.obj (.mk (op (X i)))` together with morphisms `hom`
between the pullbacks of `obj i₁` and `obj i₂` over any object `Y` which maps
to both `X i₁` and `X i₂` (in a way that is compatible with the morphisms to `S`).
The compatibilities these morphisms satisfy imply that the morphisms `hom` are isomorphisms.  -/
CategoryTheory.Pseudofunctor.DescentData : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat →
      {ι : Type t} → {S : C} → {X : ι → C} → ((i : ι) → X i ⟶ S) → Type (max (max (max (max t u) u') v) v')
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.instMulCoeOfMulMemClass : {ι : Type u_1} →
  (R : ι → Type u_2) →
    {𝓕 : Filter ι} →
      {S : ι → Type u_3} →
        [inst : (i : ι) → SetLike (S i) (R i)] →
          {B : (i : ι) → S i} →
            [inst_1 : (i : ι) → Mul (R i)] →
              [∀ (i : ι), MulMemClass (S i) (R i)] → Mul (RestrictedProduct (fun i => R i) (fun i => ↑(B i)) 𝓕)
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.toList'_map : ∀ {α : Type u} (l : List α) (s : Stream'.WSeq α),
  Computation.corec
      (fun x =>
        match x with
        | (l, s) =>
          match Stream'.Seq.destruct s with
          | none => Sum.inl l.reverse
          | some (none, s') => Sum.inr (l, s')
          | some (some a, s') => Sum.inr (a :: l, s'))
      (l, s) =
    (fun x => l.reverse ++ x) <$> s.toList
-- Init.Data.BitVec.Bitblast
BitVec.toInt_eq_neg_toNat_neg_of_msb_true : ∀ {w : ℕ} {x : BitVec w}, x.msb = true → x.toInt = -↑(-x).toNat
-- Mathlib.LinearAlgebra.Ray
/-- If `x` and `y` are on the same ray as `z`, then so is `x + y`.  -/
SameRay.add_left : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] {x y z : M}, SameRay R x z → SameRay R y z → SameRay R (x + y) z
-- Mathlib.Algebra.Algebra.Hom
uniqueOfRight : {R : Type u_1} →
  {S : Type u_2} →
    {T : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring S] →
          [inst_2 : Semiring T] →
            [inst_3 : Algebra R S] → [inst_4 : Algebra R T] → [Subsingleton T] → Unique (S →ₐ[R] T)
-- Mathlib.Order.Cover
/-- If `a < b`, then `b` does not cover `a` iff there's an element in between.  -/
not_covBy_iff : ∀ {α : Type u_1} [inst : LT α] {a b : α}, a < b → (¬a ⋖ b ↔ ∃ c, a < c ∧ c < b)
-- Lean.Elab.PreDefinition.WF.GuessLex
/-- Given a `GuessLexRel`, produce a binary `Expr` that relates two `Nat` values accordingly.  -/
Lean.Elab.WF.GuessLex.GuessLexRel.toNatRel : Lean.Elab.WF.GuessLex.GuessLexRel → Lean.Expr
-- Mathlib.Topology.Algebra.Monoid
instSeparatelyContinuousAddULift : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : Add M] [SeparatelyContinuousAdd M],
  SeparatelyContinuousAdd (ULift.{u, u_3} M)
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.hasColimitsOfShape_opposite_opposite_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J],
  CategoryTheory.Limits.HasColimitsOfShape Jᵒᵖ Cᵒᵖ ↔ CategoryTheory.Limits.HasLimitsOfShape J C
-- Mathlib.Analysis.Convex.TotallyBounded
TotallyBounded.convexHull : ∀ {E : Type u_1} {s : Set E} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : UniformSpace E]
  [IsUniformAddGroup E] [LocallyConvexSpace ℝ E] [ContinuousSMul ℝ E],
  TotallyBounded s → TotallyBounded ((convexHull ℝ) s)
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.cylinder.homotopyEquiv_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} (K : HomologicalComplex C c) [inst_2 : DecidableRel c.Rel]
  [inst_3 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [inst_4 : K.HasCylinder]
  (hc : ∀ (j : ι), ∃ i, c.Rel i j),
  (HomologicalComplex.cylinder.homotopyEquiv K hc).hom = HomologicalComplex.cylinder.π K
-- Mathlib.Order.Max
IsEmpty.toNoMinOrder : ∀ {α : Type u_1} [inst : LT α] [IsEmpty α], NoMinOrder α
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.IrreducibleCloseds.coe_map : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : β → α)
  (hf : Continuous f) (s : TopologicalSpace.IrreducibleCloseds β),
  ↑(TopologicalSpace.IrreducibleCloseds.map f hf s) = closure (f '' ↑s)
-- Lean.Expr
_private.Lean.Expr.0.Lean.mkAppRangeAux : ℕ → Array Lean.Expr → ℕ → Lean.Expr → Lean.Expr
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
_private.Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc.0.CategoryTheory.Limits.termL₁' : Lean.ParserDescr
-- Init.Data.SInt.Lemmas
Int64.toBitVec_toInt32 : ∀ (x : Int64), x.toInt32.toBitVec = BitVec.signExtend 32 x.toBitVec
-- Lean.Data.Trie
Lean.Data.Trie.instEmptyCollection : {α : Type} → EmptyCollection (Lean.Data.Trie α)
-- Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
/-- A morphism of schemes `f : X ⟶ Y` is locally of finite presentation if for each affine `U ⊆ Y`
and `V ⊆ f ⁻¹' U`, The induced map `Γ(Y, U) ⟶ Γ(X, V)` is of finite presentation.  -/
AlgebraicGeometry.LocallyOfFinitePresentation : {X Y : AlgebraicGeometry.Scheme} → (X ⟶ Y) → Prop
-- Mathlib.LinearAlgebra.Basis.Basic
Module.Basis.index_nonempty : ∀ {ι : Type u_1} {R : Type u_3} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (b : Module.Basis ι R M) [Nontrivial M], Nonempty ι
-- Mathlib.Algebra.Group.Nat.Defs
Nat.instCommSemigroup : CommSemigroup ℕ
-- Mathlib.Data.Finset.PImage
Finset.pimage_inter : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] {f : α →. β} [inst_1 : (x : α) → Decidable (f x).Dom]
  {s t : Finset α} [inst_2 : DecidableEq α], Finset.pimage f (s ∩ t) ⊆ Finset.pimage f s ∩ Finset.pimage f t
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
CategoryTheory.Functor.leftKanExtensionCompIsoOfPreserves_inv_fac : ∀ {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) [inst_4 : G.PreservesLeftKanExtension F L] [inst_5 : L.HasLeftKanExtension F],
  CategoryTheory.CategoryStruct.comp (L.leftKanExtensionUnit (F.comp G))
      (L.whiskerLeft (G.leftKanExtensionCompIsoOfPreserves F L).inv) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (L.leftKanExtensionUnit F) G)
      (L.associator (L.leftKanExtension F) G).hom
-- Mathlib.Order.Heyting.Basic
sdiff_sup_self : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] (a b : α), b \ a ⊔ a = b ⊔ a
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
/-- Given a `PushoutObjObj` of `f₁ : Arrow C₁` and `f₂ : Arrow C₂`, a `PushoutObjObj` of `f₁` and
`f₂' : Arrow C₂`, and a morphism `f₂ ⟶ f₂'`, this defines a morphism between the induced
pushout maps.  -/
CategoryTheory.Functor.PushoutObjObj.mapArrowRight : {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₃)} →
              {f₁ : CategoryTheory.Arrow C₁} →
                {f₂ f₂' : CategoryTheory.Arrow C₂} →
                  (sq₁₂ : F.PushoutObjObj f₁.hom f₂.hom) →
                    (sq₁₂' : F.PushoutObjObj f₁.hom f₂'.hom) →
                      (f₂ ⟶ f₂') → (CategoryTheory.Arrow.mk sq₁₂.ι ⟶ CategoryTheory.Arrow.mk sq₁₂'.ι)
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.Const.wfImp_alter : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] [inst_2 : Hashable α] [LawfulHashable α]
  {m : Std.DHashMap.Internal.Raw₀ α fun x => β},
  Std.DHashMap.Internal.Raw.WFImp ↑m →
    ∀ {a : α} {f : Option β → Option β}, Std.DHashMap.Internal.Raw.WFImp ↑(Std.DHashMap.Internal.Raw₀.Const.alter m a f)
-- Mathlib.Topology.Category.LightProfinite.Extend
/-- A cone over `S.diagram'` whose cone point is `S`.  -/
LightProfinite.asLimitCone' : (S : LightProfinite) → CategoryTheory.Limits.Cone S.diagram'
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
SSet.prodStdSimplex.pairingCore.Type₁.isIndex : ∀ {m : ℕ} {k : Fin (m + 1)} {n : ℕ} (self : SSet.prodStdSimplex.pairingCore.Type₁ k n),
  SSet.prodStdSimplex.pairingCore.IsIndex self.x ⋯ self.index.succ
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.isEmpty_insertIfNew! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {k : α} {v : β k}, (Std.DTreeMap.Internal.Impl.insertIfNew! k v t).isEmpty = false
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.G_eq_zero_of_odd : ∀ (L : PeriodPair) (n : ℕ), Odd n → L.G n = 0
-- Mathlib.GroupTheory.GroupAction.Basic
AddAction.stabilizerEquivStabilizer_symm : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] {g : G} {a b : α} (hg : b = g +ᵥ a),
  (AddAction.stabilizerEquivStabilizer hg).symm = AddAction.stabilizerEquivStabilizer ⋯
-- Init.Core
/-- Constructs a new thunk from a function `Unit → α` that will be called when the thunk is first
forced.

The result is cached. It is re-used when the thunk is forced again.
 -/
Thunk.mk : {α : Type u} → (Unit → α) → Thunk α
-- Lean.Setup
Lean.instReprIRPhases : Repr Lean.IRPhases
-- Mathlib.Algebra.Group.Units.Basic
instCanLiftUnitsValIsUnit : ∀ {M : Type u_1} [inst : Monoid M], CanLift M Mˣ Units.val IsUnit
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getD_eq_fallback : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {a : α} {fallback : β a}, a ∉ t → t.getD a fallback = fallback
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
/-- Not marked `@[ext]` as the `ext` tactic already solves this.  -/
Matrix.GeneralLinearGroup.ext : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] ⦃A B : GL n R⦄,
  (∀ (i j : n), ↑A i j = ↑B i j) → A = B
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.Const.modify.eq_1 : ∀ {α : Type u} [inst : BEq α] {β : Type v} (a : α) (f : β → β),
  Std.DHashMap.Internal.AssocList.Const.modify a f Std.DHashMap.Internal.AssocList.nil =
    Std.DHashMap.Internal.AssocList.nil
-- Mathlib.Algebra.Group.Prod
AddEquiv.prodAssoc.eq_1 : ∀ {M : Type u_3} {N : Type u_4} {P : Type u_5} [inst : AddZeroClass M] [inst_1 : AddZeroClass N]
  [inst_2 : AddZeroClass P], AddEquiv.prodAssoc = { toEquiv := Equiv.prodAssoc M N P, map_add' := ⋯ }
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem?_toList_roc_eq_none : ∀ {m n i : ℕ}, n ≤ i + m → (m<...=n).toList[i]? = none
-- Mathlib.RingTheory.DedekindDomain.Different
FractionalIdeal.trace_mem_dual_one : ∀ (A : Type u_1) (K : Type u_2) (L : Type u) (B : Type u_5) [inst : CommRing A] [inst_1 : Field K] [inst_2 : CommRing B]
  [inst_3 : Field L] [inst_4 : Algebra A K] [inst_5 : Algebra B L] [inst_6 : Algebra A B] [inst_7 : Algebra K L]
  [inst_8 : Algebra A L] [inst_9 : IsScalarTower A K L] [inst_10 : IsScalarTower A B L] [inst_11 : IsDomain A]
  [inst_12 : IsFractionRing A K] [inst_13 : FiniteDimensional K L] [inst_14 : Algebra.IsSeparable K L]
  [inst_15 : IsIntegralClosure B A L] [inst_16 : IsFractionRing B L] [inst_17 : IsIntegrallyClosed A]
  [inst_18 : IsDedekindDomain B] (C : Type u_3) (M : Type u_4) [inst_19 : CommRing C] [inst_20 : IsDedekindDomain C]
  [inst_21 : Field M] [inst_22 : Algebra C M] [inst_23 : IsFractionRing C M] [inst_24 : Algebra A C]
  [inst_25 : Algebra B C] [inst_26 : Algebra A M] [inst_27 : Algebra B M] [inst_28 : Algebra K M]
  [inst_29 : Algebra L M] [inst_30 : IsScalarTower A C M] [inst_31 : IsScalarTower A K M] [IsScalarTower B C M]
  [IsScalarTower B L M] [IsScalarTower K L M] [inst_35 : IsIntegralClosure C A M] [inst_36 : FiniteDimensional K M]
  [FiniteDimensional L M] [inst_38 : Algebra.IsSeparable K M],
  ∀ x ∈ FractionalIdeal.dual A K 1, (Algebra.trace L M) x ∈ FractionalIdeal.dual A K 1
-- Mathlib.Algebra.Ring.Periodic
Function.Antiperiodic.sub_eq : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [inst : AddGroup α] [inst_1 : InvolutiveNeg β],
  Function.Antiperiodic f c → ∀ (x : α), f (x - c) = -f x
-- Mathlib.Analysis.Analytic.ChangeOrigin
/-- If a function admits a power series expansion `p` on a ball `B (x, r)`, then it also admits a
power series on any subball of this ball (even with a different center), given by `p.changeOrigin`.
 -/
HasFPowerSeriesOnBall.changeOrigin : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [CompleteSpace F] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {x y : E} {r : ENNReal},
  HasFPowerSeriesOnBall f p x r → ↑‖y‖₊ < r → HasFPowerSeriesOnBall f (p.changeOrigin y) (x + y) (r - ↑‖y‖₊)
-- Mathlib.Algebra.Homology.ShortComplex.FunctorEquivalence
CategoryTheory.ShortComplex.FunctorEquivalence.unitIso_inv_app_τ₁_app : ∀ (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] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  (X : CategoryTheory.ShortComplex (CategoryTheory.Functor J C)) (X_1 : J),
  ((CategoryTheory.ShortComplex.FunctorEquivalence.unitIso J C).inv.app X).τ₁.app X_1 =
    CategoryTheory.CategoryStruct.id (X.X₁.obj X_1)
-- Mathlib.Order.KrullDimension
/-- The **height** of an element `a` in a preorder `α` is the supremum of the rightmost index of all
relation series of `α` ordered by `<` and ending below or at `a`. In other words, it is
the largest `n` such that there's a series `a₀ < a₁ < ... < aₙ = a` (or `∞` if there is
no largest `n`).
 -/
Order.height : {α : Type u_1} → [Preorder α] → α → ℕ∞
-- Mathlib.CategoryTheory.Action
CategoryTheory.actionAsFunctor_map : ∀ (M : Type u_1) [inst : Monoid M] (X : Type u) [inst_1 : MulAction M X] {X_1 Y : CategoryTheory.SingleObj M}
  (f : X_1 ⟶ Y), (CategoryTheory.actionAsFunctor M X).map f = TypeCat.ofHom fun x => f • x
-- Mathlib.Analysis.Convex.Deriv
/-- If `f : ℝ → ℝ` is strictly convex on `S` and differentiable at `x ∈ S`, then the slope of any
secant line with left endpoint at `x` is strictly greater than the derivative of `f` at `x`.  -/
StrictConvexOn.lt_slope_of_hasDerivAt : ∀ {S : Set ℝ} {f : ℝ → ℝ} {x y f' : ℝ},
  StrictConvexOn ℝ S f → x ∈ S → y ∈ S → x < y → HasDerivAt f f' x → f' < slope f x y
-- Mathlib.GroupTheory.Congruence.Defs
/-- The supremum of two congruence relations equals the smallest congruence relation containing
the supremum of the underlying binary operations.  -/
Con.sup_def : ∀ {M : Type u_1} [inst : Mul M] (c d : Con M), c ⊔ d = conGen (⇑c ⊔ ⇑d)
-- Batteries.Data.PairingHeap
Batteries.PairingHeapImp.Heap.WF.tail : ∀ {α : Type u_1} {s : Batteries.PairingHeapImp.Heap α} {le : α → α → Bool},
  Batteries.PairingHeapImp.Heap.WF le s → Batteries.PairingHeapImp.Heap.WF le (Batteries.PairingHeapImp.Heap.tail le s)
-- Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
RootPairing.posRootForm.congr_simp : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (S : Type u_5)
  [inst_5 : CommRing S] [inst_6 : LinearOrder S] [inst_7 : IsStrictOrderedRing S] [inst_8 : Algebra S R]
  [inst_9 : FaithfulSMul S R] [inst_10 : P.IsValuedIn S] [inst_11 : Fintype ι], P.posRootForm S = P.posRootForm S
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.Indep.closure_iInter_eq_biInter_closure_of_forall_subset : ∀ {α : Type u_2} {M : Matroid α} {ι : Sort u_3} {I : Set α} [Nonempty ι] {Js : ι → Set α},
  M.Indep I → (∀ (i : ι), Js i ⊆ I) → M.closure (⋂ i, Js i) = ⋂ i, M.closure (Js i)
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Trimming
/-- We call a multiseries `Trimmed` if it is either a constant, `.nil`, or `cons (exp, coef) tl`
where `coef` is trimmed and is not zero. Intuitively, when a multiseries is trimmed, its leading
monomial gives the main asymptotic behavior of the approximated function.  -/
Tactic.ComputeAsymptotics.MultiseriesExpansion.Trimmed : {basis : Tactic.ComputeAsymptotics.Basis} → Tactic.ComputeAsymptotics.MultiseriesExpansion basis → Prop
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey?_alter_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k : α} {f : Option (β k) → Option (β k)},
  (t.alter k f).getKey? k = if (f (t.get? k)).isSome = true then some k else none
-- Mathlib.CategoryTheory.Monoidal.Braided.Reflection
_private.Mathlib.CategoryTheory.Monoidal.Braided.Reflection.0.CategoryTheory.Monoidal.Reflective.adjRetraction.eq_1 : ∀ {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] [inst_2 : CategoryTheory.MonoidalCategory D]
  [inst_3 : CategoryTheory.SymmetricCategory D] [inst_4 : CategoryTheory.MonoidalClosed D]
  {R : CategoryTheory.Functor C D} [inst_5 : R.Faithful] [inst_6 : R.Full] {L : CategoryTheory.Functor D C}
  (adj : L ⊣ R) (c : C) (d : D)
  [inst_7 :
    CategoryTheory.IsIso
      (L.map (CategoryTheory.MonoidalCategoryStruct.tensorHom (adj.unit.app (d ⟹ R.obj c)) (adj.unit.app d)))],
  CategoryTheory.Monoidal.Reflective.adjRetraction✝ adj c d =
    CategoryTheory.MonoidalClosed.curry (CategoryTheory.Monoidal.Reflective.adjRetractionAux✝ adj c d)
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.Ici_mul_Ici_subset' : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Preorder α] [MulLeftMono α] [MulRightMono α] (a b : α),
  Set.Ici a * Set.Ici b ⊆ Set.Ici (a * b)