mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Lattice
/-- A type with a commutative, associative and idempotent binary `inf` operation has the structure of a
meet-semilattice.

The partial order is defined so that `a ≤ b` unfolds to `b ⊓ a = a`; cf. `inf_eq_right`.
 -/
SemilatticeInf.mk' : {α : Type u_1} →
  [inst : Min α] →
    (∀ (a b : α), a ⊓ b = b ⊓ a) → (∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)) → (∀ (a : α), a ⊓ a = a) → SemilatticeInf α
-- Mathlib.Data.List.GetD
List.getI_eq_iget_getElem? : ∀ {α : Type u} (l : List α) [inst : Inhabited α] (n : ℕ), l.getI n = l[n]?.getD default
-- Mathlib.Topology.VectorBundle.Basic
VectorBundleCore.coordChange_comp : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField R] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace R F] [inst_3 : TopologicalSpace B] {ι : Type u_5} (self : VectorBundleCore R B F ι) (i j k : ι),
  ∀ x ∈ self.baseSet i ∩ self.baseSet j ∩ self.baseSet k,
    ∀ (v : F), (self.coordChange j k x) ((self.coordChange i j x) v) = (self.coordChange i k x) v
-- Lean.Linter.Init
/-- Global registry of options associated with environment linters.
These are precisely options, whose value will be snapshotted during `addDecl`.
 -/
Lean.Linter.envLinterOptionsRef : IO.Ref (Array (Lean.Option Bool))
-- Lean.Server.RequestCancellation
Lean.Server.RequestCancellationToken.mk.sizeOf_spec : ∀ (cancelledByCancelRequest cancelledByEdit : IO.CancelToken)
  (requestCancellationPromise editCancellationPromise : IO.Promise Unit),
  sizeOf
      { cancelledByCancelRequest := cancelledByCancelRequest, cancelledByEdit := cancelledByEdit,
        requestCancellationPromise := requestCancellationPromise, editCancellationPromise := editCancellationPromise } =
    1 + sizeOf cancelledByCancelRequest + sizeOf cancelledByEdit + sizeOf requestCancellationPromise +
      sizeOf editCancellationPromise
-- Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
/-- Every normal monomorphism is a regular monomorphism.  -/
CategoryTheory.NormalMono.regularMono : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
        (f : X ⟶ Y) → [I : CategoryTheory.NormalMono f] → CategoryTheory.RegularMono f
-- Mathlib.Topology.Instances.Matrix
Summable.matrix_blockDiagonal : ∀ {X : Type u_1} {m : Type u_4} {n : Type u_5} {p : Type u_6} {R : Type u_8} [inst : AddCommMonoid R]
  [inst_1 : TopologicalSpace R] {L : SummationFilter X} [inst_2 : DecidableEq p] {f : X → p → Matrix m n R},
  Summable f L → Summable (fun x => Matrix.blockDiagonal (f x)) L
-- Batteries.Data.Array.Lemmas
Array.toList_swapIfInBounds : ∀ {α : Type u_1} {i j : ℕ} {a : Array α}, (a.swapIfInBounds i j).toList = a.toList.swap i j
-- Mathlib.NumberTheory.Dioph
/-- The set of places where one Diophantine function divides another is Diophantine.  -/
Dioph.dvd_dioph : ∀ {α : Type} {f g : (α → ℕ) → ℕ}, Dioph.DiophFn f → Dioph.DiophFn g → Dioph {v | f v ∣ g v}
-- Mathlib.CategoryTheory.Limits.Final.Type
CategoryTheory.Functor.bijective_sectionsPrecomp : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) (P : CategoryTheory.Functor D (Type w)) [F.Initial],
  Function.Bijective F.sectionsPrecomp
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.image_preimage_eq_prod_univ : ∀ {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},
  s ⊆ e.baseSet → ↑e '' proj ⁻¹' s = s ×ˢ Set.univ
-- Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
RootPairing.ker_copolarization_eq_ker_corootForm : ∀ {ι : 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) [inst_5 : Fintype ι],
  P.CoPolarization.ker = LinearMap.ker P.CorootForm
-- Mathlib.CategoryTheory.Bicategory.Monad.Basic
CategoryTheory.Bicategory.OplaxTrans.ComonadBicat.mkOfComonad_comul : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a : B} (t : a ⟶ a) [inst_1 : CategoryTheory.Bicategory.Comonad t],
  CategoryTheory.Bicategory.Comonad.comul = CategoryTheory.Bicategory.Comonad.comul
-- Mathlib.CategoryTheory.Sites.Sieves
/-- This presieve generates `functorPushforward`.
See `arrows_generate_map_eq_functorPushforward`.  -/
CategoryTheory.Presieve.map : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) → {X : C} → CategoryTheory.Presieve X → CategoryTheory.Presieve (F.obj X)
-- Mathlib.Data.ENNReal.Operations
ENNReal.add_sSup : ∀ {s : Set ENNReal} {a : ENNReal}, s.Nonempty → a + sSup s = ⨆ b ∈ s, a + b
-- Mathlib.Algebra.Group.Prod
/-- Combine two `MonoidHom`s `f : M →* N`, `g : M →* P` into `f.prod g : M →* N × P`
given by `(f.prod g) x = (f x, g x)`.  -/
MonoidHom.prod : {M : Type u_3} →
  {N : Type u_4} →
    {P : Type u_5} →
      [inst : MulOneClass M] → [inst_1 : MulOneClass N] → [inst_2 : MulOneClass P] → (M →* N) → (M →* P) → M →* N × P
-- Mathlib.Algebra.Lie.Normalizer
LieSubmodule.comap_normalizer : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} {M' : Type u_4} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : LieAlgebra R L] [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M]
  [inst_6 : LieModule R L M] [inst_7 : AddCommGroup M'] [inst_8 : Module R M'] [inst_9 : LieRingModule L M']
  [inst_10 : LieModule R L M'] (N : LieSubmodule R L M) (f : M' →ₗ⁅R,L⁆ M),
  LieSubmodule.comap f N.normalizer = (LieSubmodule.comap f N).normalizer
-- Mathlib.NumberTheory.Height.Basic
/-- Eta-expanded form of `Height.mulHeight_one` -/
Height.fun_mulHeight_one : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] {ι : Type u_2},
  (Height.mulHeight fun x => 1) = 1
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgEquiv.coe_trans : ∀ {R : Type u_2} {A : Type u_3} {B : Type u_4} {C : Type u_5} [inst : Add A] [inst_1 : Add B] [inst_2 : Mul A]
  [inst_3 : Mul B] [inst_4 : SMul R A] [inst_5 : SMul R B] [inst_6 : Star A] [inst_7 : Star B] [inst_8 : Add C]
  [inst_9 : Mul C] [inst_10 : SMul R C] [inst_11 : Star C] (e₁ : A ≃⋆ₐ[R] B) (e₂ : B ≃⋆ₐ[R] C),
  ⇑(e₁.trans e₂) = ⇑e₂ ∘ ⇑e₁
-- Init.Data.List.MinMaxIdx
_private.Init.Data.List.MinMaxIdx.0.List.combineMinIdxOn.eq_1 : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] (f : α → β) {xs ys : List α} (i j : ℕ)
  (hi : i < xs.length) (hj : j < ys.length),
  List.combineMinIdxOn✝ f i j hi hj = if f xs[i] ≤ f ys[j] then i else xs.length + j
-- Mathlib.Algebra.MvPolynomial.Equiv
/-- The algebra isomorphism between multivariable polynomials in `Option S₁` and
polynomials with coefficients in `MvPolynomial S₁ R`.
 -/
MvPolynomial.optionEquivLeft : (R : Type u) → (S₁ : Type v) → [inst : CommSemiring R] → MvPolynomial (Option S₁) R ≃ₐ[R] Polynomial (MvPolynomial S₁ R)
-- Mathlib.Data.List.Cycle
List.isRotated_prev_eq : ∀ {α : Type u_1} [inst : DecidableEq α] {l l' : List α} (h : l ~r l'),
  l.Nodup → ∀ {x : α} (hx : x ∈ l), l.prev x hx = l'.prev x ⋯
-- Mathlib.FieldTheory.Minpoly.Basic
minpoly.natDegree_eq_one_iff : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : Ring B] [inst_2 : Algebra A B] {x : B} [Nontrivial B],
  (minpoly A x).natDegree = 1 ↔ x ∈ (algebraMap A B).range
-- Lean.Data.Json.Basic
Lean.JsonNumber.instRepr : Repr Lean.JsonNumber
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.IsCycle.sign : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Fintype α] {f : Equiv.Perm α},
  f.IsCycle → Equiv.Perm.sign f = -(-1) ^ f.support.card
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
/-- The equivalence on index types induced by an isomorphism of pre-`0`-hypercovers.  -/
CategoryTheory.PreZeroHypercover.equivOfIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {S : C} → {E F : CategoryTheory.PreZeroHypercover S} → (E ≅ F) → E.I₀ ≃ F.I₀
-- Lean.Server.Completion.CompletionItemCompression
_private.Lean.Server.Completion.CompletionItemCompression.0.Lean.Lsp.ResolvableCompletionList.compressItemDataFast : String → Lean.Lsp.ResolvableCompletionItemData → String
-- Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
SSet.horn₃₂.desc.multicofork_π_three_assoc : ∀ {X : SSet} (f₀ f₁ f₃ : SSet.stdSimplex.obj { len := 2 } ⟶ X)
  (h₀₂ :
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₁ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 1) f₃)
  (h₁₂ :
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₀ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f₃)
  (h₂₃ :
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f₀ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f₁)
  {Z : SSet} (h : (SSet.horn₃₂.desc.multicofork f₀ f₁ f₃ h₀₂ h₁₂ h₂₃).pt ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      ((SSet.horn₃₂.desc.multicofork f₀ f₁ f₃ h₀₂ h₁₂ h₂₃).π ⟨3, SSet.horn₃₂.desc.multicofork_π_three._proof_1⟩) h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.faceSingletonComplIso 3).inv f₃) h
-- Mathlib.Data.Finset.Sups
Finset.diffs_subset_iff : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : GeneralizedBooleanAlgebra α] {s t u : Finset α},
  s.diffs t ⊆ u ↔ ∀ a ∈ s, ∀ b ∈ t, a \ b ∈ u
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.ZeroExtend
Std.Tactic.BVDecide.BVExpr.bitblast.blastZeroExtend.go_get_aux : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] (aig : Std.Sat.AIG α) (w : ℕ) (input : aig.RefVec w)
  (newWidth curr : ℕ) (hcurr : curr ≤ newWidth) (s : aig.RefVec curr) (idx : ℕ) (hidx : idx < curr)
  (hfoo :
    aig.decls.size ≤
      (Std.Tactic.BVDecide.BVExpr.bitblast.blastZeroExtend.go aig w input newWidth curr hcurr s).aig.decls.size),
  (Std.Tactic.BVDecide.BVExpr.bitblast.blastZeroExtend.go aig w input newWidth curr hcurr s).vec.get idx ⋯ =
    (s.get idx hidx).cast hfoo
-- Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
/-- The additive morphism from `C^n` sections to dependent maps.  -/
ContMDiffSection.coeAddHom : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {H : Type u_3} →
            [inst_3 : TopologicalSpace H] →
              (I : ModelWithCorners 𝕜 E H) →
                {M : Type u_4} →
                  [inst_4 : TopologicalSpace M] →
                    [inst_5 : ChartedSpace H M] →
                      (F : Type u_5) →
                        [inst_6 : NormedAddCommGroup F] →
                          [inst_7 : NormedSpace 𝕜 F] →
                            (n : WithTop ℕ∞) →
                              (V : M → Type u_6) →
                                [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)] →
                                  [inst_9 : (x : M) → TopologicalSpace (V x)] →
                                    [inst_10 : FiberBundle F V] →
                                      [inst_11 : (x : M) → AddCommGroup (V x)] →
                                        [inst_12 : (x : M) → Module 𝕜 (V x)] →
                                          [inst_13 : VectorBundle 𝕜 F V] → ContMDiffSection I F n V →+ (x : M) → V x
-- Std.Http.Data.Response
Std.Http.Response.Builder.mk.inj : ∀ {line : Std.Http.Response.Head} {extensions : Std.Http.Extensions} {line_1 : Std.Http.Response.Head}
  {extensions_1 : Std.Http.Extensions},
  { line := line, extensions := extensions } = { line := line_1, extensions := extensions_1 } →
    line = line_1 ∧ extensions = extensions_1
-- Mathlib.Data.Multiset.Basic
Multiset.strongInductionOn.eq_1 : ∀ {α : Type u_1} {p : Multiset α → Sort u_3} (s : Multiset α)
  (ih : (s : Multiset α) → ((t : Multiset α) → t < s → p t) → p s),
  s.strongInductionOn ih = ih s fun t _h => t.strongInductionOn ih
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.instSetLike : {R : Type u} →
  {A : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : NonUnitalNonAssocSemiring A] → [inst_2 : Module R A] → SetLike (NonUnitalSubalgebra R A) A
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.uliftYonedaEquiv_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {F G : CategoryTheory.Functor Cᵒᵖ (Type (max w v₁))}
  (α : CategoryTheory.uliftYoneda.{w, v₁, u₁}.obj X ⟶ F) (β : F ⟶ G),
  CategoryTheory.uliftYonedaEquiv (CategoryTheory.CategoryStruct.comp α β) =
    (CategoryTheory.ConcreteCategory.hom (β.app (Opposite.op X))) (CategoryTheory.uliftYonedaEquiv α)
-- Mathlib.Algebra.Module.Equiv.Basic
/-- Pointwise application of a family of linear forms to a family of vectors  -/
LinearMap.piApply : {R : Type u_1} →
  {M : Type u_5} →
    {V : M → Type u_9} →
      [inst : CommSemiring R] →
        [inst_1 : (x : M) → AddCommMonoid (V x)] →
          [inst_2 : (x : M) → Module R (V x)] → ((x : M) → V x →ₗ[R] R) →ₗ[R] ((x : M) → V x) →ₗ[R] M → R
-- Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
MvPolynomial.mem_symmetricSubalgebra : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R] (p : MvPolynomial σ R),
  p ∈ MvPolynomial.symmetricSubalgebra σ R ↔ p.IsSymmetric
-- Init.Data.Array.Find
Array.findRev?_push_of_pos : ∀ {α : Type} {p : α → Bool} {a : α} {xs : Array α}, p a = true → Array.findRev? p (xs.push a) = some a
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.toListRev_mapM_filterMapM : ∀ {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''} [inst : Monad m]
  [LawfulMonad m] [inst_2 : Monad n] [inst_3 : MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n]
  [inst_6 : Monad o] [inst_7 : MonadAttach o] [LawfulMonad o] [WeaklyLawfulMonadAttach o] [inst_10 : MonadLiftT m n]
  [inst_11 : MonadLiftT n o] [LawfulMonadLiftT m n] [LawfulMonadLiftT n o] [inst : Std.Iterator α m β]
  [Std.Iterators.Finite α m] {f : β → n (Option γ)} {g : γ → o δ} {it : Std.IterM m β},
  (Std.IterM.mapM g (Std.IterM.filterMapM f it)).toListRev =
    (Std.IterM.filterMapM
        (fun b => do
          let __do_lift ← liftM (f b)
          match __do_lift with
            | none => pure none
            | some fb => some <$> g fb)
        it).toListRev
-- Mathlib.MeasureTheory.Function.JacobianOneDim
/-- Change of variable formula for differentiable functions: if a real function `f` is
antitone and differentiable on a measurable set `s`, then the Lebesgue integral of a function
`u : ℝ → ℝ≥0∞` on `f '' s` coincides with the integral of `(-f' x) * u ∘ f` on `s`.
Note that the measurability of `f '' s` is given by `MeasurableSet.image_of_antitoneOn`.  -/
MeasureTheory.lintegral_image_eq_lintegral_deriv_mul_of_antitoneOn : ∀ {s : Set ℝ} {f f' : ℝ → ℝ},
  MeasurableSet s →
    (∀ x ∈ s, HasDerivWithinAt f (f' x) s x) →
      AntitoneOn f s →
        ∀ (u : ℝ → ENNReal), ∫⁻ (x : ℝ) in f '' s, u x = ∫⁻ (x : ℝ) in s, ENNReal.ofReal (-f' x) * u (f x)
-- Lean.Meta.Tactic.Grind.Split
_private.Lean.Meta.Tactic.Grind.Split.0.Lean.Meta.Grind.selectNextSplit?.go : List Lean.Meta.Grind.SplitInfo →
  Lean.Meta.Grind.SplitCandidate✝ →
    List Lean.Meta.Grind.SplitInfo → Lean.Meta.Grind.GoalM Lean.Meta.Grind.SplitCandidate✝
-- Mathlib.Analysis.Normed.Group.Quotient
/-- The seminormed group structure on the quotient by a subgroup.  -/
QuotientGroup.instSeminormedCommGroup : {M : Type u_1} → [inst : SeminormedCommGroup M] → (S : Subgroup M) → SeminormedCommGroup (M ⧸ S)
-- Mathlib.RingTheory.Kaehler.Basic
KaehlerDifferential.exact_kerCotangentToTensor_mapBaseChange : ∀ (R : Type u) [inst : CommRing R] (A : Type u_2) (B : Type u_3) [inst_1 : CommRing A] [inst_2 : CommRing B]
  [inst_3 : Algebra R A] [inst_4 : Algebra A B] [inst_5 : Algebra R B] [inst_6 : IsScalarTower R A B],
  Function.Surjective ⇑(algebraMap A B) →
    Function.Exact ⇑(KaehlerDifferential.kerCotangentToTensor R A B) ⇑(KaehlerDifferential.mapBaseChange R A B)
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Oplax
/-- Right whiskering of a lax natural transformation and a modification.  -/
CategoryTheory.Oplax.LaxTrans.whiskerRight : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G H : CategoryTheory.OplaxFunctor B C} →
          {η θ : F ⟶ G} →
            (η ⟶ θ) → (ι : G ⟶ H) → CategoryTheory.CategoryStruct.comp η ι ⟶ CategoryTheory.CategoryStruct.comp θ ι
-- Mathlib.Data.List.Lattice
List.bagInter_sublist_left : ∀ {α : Type u_1} [inst : DecidableEq α] {l₁ l₂ : List α}, (l₁.bagInter l₂).Sublist l₁
-- Std.Net.Addr
Std.Net.IPAddr.toString : Std.Net.IPAddr → String
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
CategoryTheory.Lax.StrongTrans.id_naturality_inv : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.LaxFunctor B C) {a b : B} (f : a ⟶ b),
  ((CategoryTheory.Lax.StrongTrans.id F).naturality f).inv =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor (F.map f)).hom
      (CategoryTheory.Bicategory.leftUnitor (F.map f)).inv
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.span_singleton_eq_top_iff : ∀ (R : Type u_1) {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (x : M),
  R ∙ x = ⊤ ↔ ∀ (v : M), ∃ r, r • x = v
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.min?_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : Min α] [inst_1 : LE α]
  [Std.LawfulOrderCmp cmp] [Std.LawfulOrderMin α] [Std.LawfulOrderLeftLeaningMin α] [Std.LawfulEqCmp cmp],
  t.toList.min? = t.min?
-- Mathlib.Algebra.Ring.ULift
ULift.nonUnitalRing : {R : Type u} → [NonUnitalRing R] → NonUnitalRing (ULift.{u_1, u} R)
-- Mathlib.LinearAlgebra.Matrix.Ideal
TwoSidedIdeal.coe_equivMatrix_symm_apply : ∀ {R : Type u_1} {n : Type u_2} [inst : NonAssocRing R] [inst_1 : Fintype n] [inst_2 : Nonempty n]
  [inst_3 : DecidableEq n] (I : TwoSidedIdeal (Matrix n n R)) (i j : n),
  ↑(TwoSidedIdeal.equivMatrix.symm I) = {x | ∃ N ∈ I, N i j = x}
-- Mathlib.RepresentationTheory.Homological.FiniteCyclic
Rep.FiniteCyclicGroup.chainComplexFunctor_obj : ∀ (k : Type u) {G : Type u} [inst : CommRing k] [inst_1 : CommGroup G] [inst_2 : Fintype G] (g : G)
  (A : Rep.{u_1, u, u} k G),
  (Rep.FiniteCyclicGroup.chainComplexFunctor k g).obj A = HomologicalComplex.alternatingConst A ⋯ ⋯ ⋯
-- Mathlib.RingTheory.Ideal.GoingUp
Ideal.isMaximal_comap_of_isIntegral_of_isMaximal' : ∀ {R : Type u_3} {S : Type u_4} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
  f.IsIntegral → ∀ (I : Ideal S) [I.IsMaximal], (Ideal.comap f I).IsMaximal
-- Mathlib.Analysis.Normed.Lp.LpEquiv
AddEquiv.lpBCF.congr_simp : ∀ {α : Type u_1} {E : Type u_2} [inst : TopologicalSpace α] [inst_1 : DiscreteTopology α]
  [inst_2 : NormedAddCommGroup E], AddEquiv.lpBCF = AddEquiv.lpBCF
-- Mathlib.RingTheory.Ideal.Pointwise
/-- The action on an ideal corresponding to applying the action to every element.

This is available as an instance in the `Pointwise` locale.  -/
Ideal.pointwiseMulSemiringAction : {M : Type u_1} →
  [inst : Monoid M] → {R : Type u_4} → [inst_1 : CommRing R] → [MulSemiringAction M R] → MulSemiringAction M (Ideal R)
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
CategoryTheory.SubobjectRepresentableBy.χ.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {Ω : C}
  (h h_1 : CategoryTheory.SubobjectRepresentableBy Ω),
  h = h_1 → ∀ {U X : C} (m m_1 : U ⟶ X) (e_m : m = m_1) [inst_2 : CategoryTheory.Mono m], h.χ m = h_1.χ m_1
-- Mathlib.Analysis.Complex.Circle
Circle.exp_add : ∀ (x y : ℝ), Circle.exp (x + y) = Circle.exp x * Circle.exp y
-- Mathlib.Probability.ProbabilityMassFunction.Basic
PMF.toMeasure_apply_eq_toOuterMeasure : ∀ {α : Type u_1} [inst : MeasurableSpace α] (p : PMF α) [MeasurableSingletonClass α] (s : Set α),
  p.toMeasure s = p.toOuterMeasure s
-- Mathlib.RepresentationTheory.Tannaka
/-- The monoidal forgetful functor from `FDRep k G` to `FGModuleCat k`.  -/
TannakaDuality.FiniteGroup.forget : (k G : Type u) →
  [inst : CommRing k] → [inst_1 : Group G] → CategoryTheory.LaxMonoidalFunctor (FDRep k G) (FGModuleCat k)
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.embDomain_zero : ∀ {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : Zero R] [inst_2 : PartialOrder Γ']
  {f : Γ ↪o Γ'}, HahnSeries.embDomain f 0 = 0
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.copyBase_IsBase : ∀ {α : Type u_1} (M : Matroid α) (E : Set α) (IsBase : Set α → Prop) (hE : E = M.E)
  (h : ∀ (B : Set α), IsBase B ↔ M.IsBase B) (a : Set α), (M.copyBase E IsBase hE h).IsBase a = IsBase a
-- Mathlib.Order.Bounds.Basic
IsLeast.unique : ∀ {α : Type u_1} [inst : PartialOrder α] {s : Set α} {a b : α}, IsLeast s a → IsLeast s b → a = b
-- Mathlib.LinearAlgebra.Pi
/-- Combine a family of linear equivalences into a linear equivalence of `pi`-types.

This is `Equiv.piCongrRight` as a `LinearEquiv`  -/
LinearEquiv.piCongrRight : {R : Type u} →
  {ι : Type x} →
    [inst : Semiring R] →
      {φ : ι → Type u_1} →
        {ψ : ι → Type u_2} →
          [inst_1 : (i : ι) → AddCommMonoid (φ i)] →
            [inst_2 : (i : ι) → Module R (φ i)] →
              [inst_3 : (i : ι) → AddCommMonoid (ψ i)] →
                [inst_4 : (i : ι) → Module R (ψ i)] → ((i : ι) → φ i ≃ₗ[R] ψ i) → ((i : ι) → φ i) ≃ₗ[R] (i : ι) → ψ i
-- Mathlib.Algebra.Group.Equiv.Defs
AddEquiv.symmEquiv_apply_symm_apply : ∀ (P : Type u_9) (Q : Type u_10) [inst : Add P] [inst_1 : Add Q] (h : P ≃+ Q) (a : P),
  ((AddEquiv.symmEquiv P Q) h).symm a = h a
-- Mathlib.Condensed.EffectiveEpi
instIsRegularEpiCategoryCondensedSet : CategoryTheory.IsRegularEpiCategory CondensedSet
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVBinPred.instToString : ToString Std.Tactic.BVDecide.BVBinPred
-- Mathlib.Algebra.Homology.Embedding.AreComplementary
/-- If `ac : AreComplementary e₁ e₂` (with `e₁ : ComplexShape.Embedding c₁ c` and
`e₂ : ComplexShape.Embedding c₂ c`), and `i₁` belongs to `e₁.BoundaryLE`,
then this is the (unique) index `i₂` of `c₂` such that `ac.Boundary i₁ i₂`.  -/
ComplexShape.Embedding.AreComplementary.Boundary.indexOfBoundaryLE : {ι : Type u_1} →
  {ι₁ : Type u_2} →
    {ι₂ : Type u_3} →
      {c : ComplexShape ι} →
        {c₁ : ComplexShape ι₁} →
          {c₂ : ComplexShape ι₂} →
            {e₁ : c₁.Embedding c} → {e₂ : c₂.Embedding c} → e₁.AreComplementary e₂ → {i₁ : ι₁} → e₁.BoundaryLE i₁ → ι₂
-- Mathlib.Analysis.Complex.Circle
Circle.expHom_apply : ∀ (a : ℝ), Circle.expHom a = (⇑Additive.ofMul ∘ ⇑Circle.exp) a
-- Mathlib.CategoryTheory.Discrete.Basic
/-- Composing `Discrete.functor F` with another functor `G` amounts to composing `F` with `G.obj`  -/
CategoryTheory.Discrete.compNatIsoDiscrete : {C : Type u₂} →
  [inst : CategoryTheory.Category.{v₂, u₂} C] →
    {I : Type u₁} →
      {D : Type u₃} →
        [inst_1 : CategoryTheory.Category.{v₃, u₃} D] →
          (F : I → C) →
            (G : CategoryTheory.Functor C D) →
              (CategoryTheory.Discrete.functor F).comp G ≅ CategoryTheory.Discrete.functor (G.obj ∘ F)
-- Mathlib.RingTheory.Extension.Presentation.Basic
Algebra.Presentation.naive_relation : ∀ {R : Type u} {ι : Type w} {σ : Type t} [inst : CommRing R] {v : ι → MvPolynomial σ R}
  (s : MvPolynomial σ R ⧸ Ideal.span (Set.range v) → MvPolynomial σ R)
  (hs : ∀ (x : MvPolynomial σ R ⧸ Ideal.span (Set.range v)), (Ideal.Quotient.mk (Ideal.span (Set.range v))) (s x) = x),
  (Algebra.Presentation.naive s hs).relation = v
-- Mathlib.CategoryTheory.SmallRepresentatives
CategoryTheory.CoreSmallCategoryOfSet.mk : {Ω : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      (obj : Set Ω) →
        (hom : ↑obj → ↑obj → Set Ω) →
          (objEquiv : ↑obj ≃ C) →
            ({X Y : ↑obj} → ↑(hom X Y) ≃ (objEquiv X ⟶ objEquiv Y)) → CategoryTheory.CoreSmallCategoryOfSet Ω C