mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Elab.ConfigEval.DeriveEvalExpr
/-- Ensures an `EvalExpr` instance exists for the given type by deriving one if necessary.
Derivation can handle `EvalExpr` instance for nonrecursive inductive types without universes, parameters, or indices,
and which only does simple recursion.
 -/
Lean.Elab.ConfigEval.ensureEvalExpr : Option (Lean.TSyntax `Lean.Parser.Command.visibility) →
  Lean.TSyntax `Lean.Parser.Term.attrKind → Lean.Syntax → Lean.Syntax → Lean.Expr → Lean.Elab.Command.CommandElabM Unit
-- Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
CategoryTheory.whiskeringLeft_preservesColimit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E]
  [CategoryTheory.Limits.HasColimitsOfSize.{w, w', v₂, u₂} D] (F : CategoryTheory.Functor C E),
  CategoryTheory.Limits.PreservesColimitsOfSize.{w, w', max u₃ v₂, max u₁ v₂, max (max (max u₂ u₃) v₂) v₃,
      max (max (max u₁ u₂) v₁) v₂}
    ((CategoryTheory.Functor.whiskeringLeft C E D).obj F)
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
/-- Mapping a `zeroCokernelCofork` of `f : X ⟶ Y` along a functor `G` that preserves zero morphisms
is isomorphic to the `zeroCokernelCofork` of `G.map f`.  -/
CategoryTheory.Limits.mapZeroCokernelCofork : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] →
            (G : CategoryTheory.Functor C D) →
              [inst_4 : G.PreservesZeroMorphisms] →
                [inst_5 : CategoryTheory.Limits.HasZeroObject C] →
                  [inst_6 : CategoryTheory.Limits.HasZeroObject D] →
                    {X Y : C} →
                      (f : X ⟶ Y) →
                        (CategoryTheory.Limits.cokernel.zeroCokernelCofork f).map G ≅
                          CategoryTheory.Limits.cokernel.zeroCokernelCofork (G.map f)
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
SSet.prodStdSimplex.pairingCore.IsType₂.φ_of_gt : ∀ {m : ℕ} {k : Fin (m + 1)} {n : ℕ} (x : ((SSet.horn (m + 1) k.castSucc).unionProd (SSet.boundary n)).N) {d : ℕ}
  (hd : x.dim = d) (i : Fin (d + 2)) (hi : (SSet.prodStdSimplex.pairingCore.min x hd).castSucc < i),
  SSet.prodStdSimplex.pairingCore.IsType₂.φ x hd i = (SSet.prodStdSimplex.objEquiv (x.cast hd).simplex) (i.pred ⋯)
-- Mathlib.CategoryTheory.GlueData
CategoryTheory.GlueData.cocycle : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] (self : CategoryTheory.GlueData C) (i j k : self.J),
  CategoryTheory.CategoryStruct.comp (self.t' i j k)
      (CategoryTheory.CategoryStruct.comp (self.t' j k i) (self.t' k i j)) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.pullback (self.f i j) (self.f i k))
-- Mathlib.Geometry.Manifold.Algebra.Monoid
contMDiff_finsum_cond : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_3}
  [inst_1 : TopologicalSpace H] {E : Type u_4} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E]
  {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [inst_4 : AddCommMonoid G] [inst_5 : TopologicalSpace G]
  [inst_6 : ChartedSpace H G] [ContMDiffAdd I n G] {E' : Type u_6} [inst_8 : NormedAddCommGroup E']
  [inst_9 : NormedSpace 𝕜 E'] {H' : Type u_7} [inst_10 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M : Type u_8} [inst_11 : TopologicalSpace M] [inst_12 : ChartedSpace H' M] {f : ι → M → G} {p : ι → Prop},
  (∀ (i : ι), p i → ContMDiff I' I n (f i)) →
    (LocallyFinite fun i => Function.support (f i)) → ContMDiff I' I n fun x => ∑ᶠ (i : ι) (_ : p i), f i x
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_le_rpow_left_iff : ∀ {x y z : ℝ}, 1 < x → (x ^ y ≤ x ^ z ↔ y ≤ z)
-- Std.Http.Data.Response
Std.Http.Response.Head.mk.injEq : ∀ (status : Std.Http.Status) (version : Std.Http.Version) (headers : Std.Http.Headers) (status_1 : Std.Http.Status)
  (version_1 : Std.Http.Version) (headers_1 : Std.Http.Headers),
  ({ status := status, version := version, headers := headers } =
      { status := status_1, version := version_1, headers := headers_1 }) =
    (status = status_1 ∧ version = version_1 ∧ headers = headers_1)
-- Mathlib.Order.Defs.Unbundled
/-- `IsAsymm X r` means that the binary relation `r` on `X` is asymmetric, that is,
`r a b → ¬ r b a`.  -/
IsAsymm : (α : Sort u_1) → (α → α → Prop) → Prop
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVBinOp.eval_add : ∀ {w : ℕ}, Std.Tactic.BVDecide.BVBinOp.add.eval = fun x1 x2 => x1 + x2
-- Std.Sat.AIG.Basic
Std.Sat.AIG.toGraphviz.go : {α : Type} →
  [DecidableEq α] →
    [ToString α] →
      [Hashable α] →
        String →
          (decls : Array (Std.Sat.AIG.Decl α)) →
            Std.Sat.AIG.IsDAG α decls → (idx : ℕ) → idx < decls.size → StateM (Std.HashSet (Fin decls.size)) String
-- Mathlib.AlgebraicGeometry.Morphisms.Etale
AlgebraicGeometry.Scheme.instFaithfulEtaleOverForget : ∀ (X : AlgebraicGeometry.Scheme), (AlgebraicGeometry.Scheme.Etale.forget X).Faithful
-- Mathlib.Algebra.Field.Defs
/-- `a ^ (n + 1) = a ^ n * a`  -/
Semifield.zpow_succ' : ∀ {K : Type u_2} [self : Semifield K] (n : ℕ) (a : K), a ^ ↑n.succ = a ^ ↑n * a
-- Mathlib.Order.Filter.Basic
Filter.EventuallyLE.trans_eq : ∀ {α : Type u} {β : Type v} [inst : Preorder β] {l : Filter α} {f g h : α → β}, f ≤ᶠ[l] g → g =ᶠ[l] h → f ≤ᶠ[l] h
-- Mathlib.Data.ZMod.Basic
ZMod.castHom_surjective : ∀ {n m : ℕ} (h : m ∣ n), Function.Surjective ⇑(ZMod.castHom h (ZMod m))
-- Mathlib.Data.Nat.Cast.Order.Basic
Nat.cast_nonpos : ∀ {α : Type u_1} [inst : AddMonoidWithOne α] [inst_1 : PartialOrder α] [AddLeftMono α] [ZeroLEOneClass α] [CharZero α]
  {n : ℕ}, ↑n ≤ 0 ↔ n = 0
-- Mathlib.RingTheory.HahnSeries.Addition
HahnSeries.leadingCoeff_add_eq_left : ∀ {R : Type u_3} [inst : AddMonoid R] {Γ : Type u_8} [inst_1 : LinearOrder Γ] {x y : HahnSeries Γ R},
  x.orderTop < y.orderTop → (x + y).leadingCoeff = x.leadingCoeff
-- Mathlib.Topology.Category.UniformSpace
/-- A bundled uniform continuous map.  -/
UniformSpaceCat.Hom : UniformSpaceCat → UniformSpaceCat → Type (max u_1 u_2)
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.ConnectedComponent.lift_mk : ∀ {V : Type u} {G : SimpleGraph V} {β : Sort u_1} {f : V → β} {h : ∀ (v w : V) (p : G.Walk v w), p.IsPath → f v = f w}
  {v : V}, SimpleGraph.ConnectedComponent.lift f h (G.connectedComponentMk v) = f v
-- Mathlib.Algebra.Homology.HomologySequence
HomologicalComplex.HomologySequence.snakeInput_L₂ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {c : ComplexShape ι} {S : CategoryTheory.ShortComplex (HomologicalComplex C c)} (hS : S.ShortExact) (i j : ι)
  (hij : c.Rel i j),
  (HomologicalComplex.HomologySequence.snakeInput hS i j hij).L₂ =
    (HomologicalComplex.cyclesFunctor C c j).mapShortComplex.obj S
-- Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
ProbabilityTheory.HasGaussianLaw.charFunDual_map_eq_fun : ∀ {Ω : Type u_1} {E : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [inst : NormedAddCommGroup E]
  [inst_1 : MeasurableSpace E] [BorelSpace E] {X : Ω → E} [inst_3 : NormedSpace ℝ E] (L : StrongDual ℝ E),
  ProbabilityTheory.HasGaussianLaw X P →
    MeasureTheory.charFunDual (MeasureTheory.Measure.map X P) L =
      Complex.exp (↑(∫ (ω : Ω), L (X ω) ∂P) * Complex.I - ↑(ProbabilityTheory.variance (fun ω => L (X ω)) P) / 2)
-- Mathlib.FieldTheory.IntermediateField.ExtendRight
IntermediateField.extendRight.instIsScalarTowerSubtypeMem : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (F : IntermediateField K L)
  (M : Type u_3) [inst_3 : Field M] [inst_4 : Algebra K M] [inst_5 : Algebra L M] [inst_6 : IsScalarTower K L M]
  {S : Type u_5} [inst_7 : CommRing S] [inst_8 : Algebra S ↥F] [inst_9 : Algebra S M]
  [inst_10 : IsScalarTower S (↥F) M], IsScalarTower S (↥(F.extendRight M)) M
-- Mathlib.Geometry.Manifold.Instances.Sphere
stereoInvFunAux_mem : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {v : E},
  ‖v‖ = 1 → ∀ {w : E}, w ∈ (ℝ ∙ v)ᗮ → stereoInvFunAux v w ∈ Metric.sphere 0 1
-- Mathlib.CategoryTheory.Sites.Grothendieck
/-- Given `I : S.Arrow` and a morphism `g : Z ⟶ I.Y`, this is the obvious relation
from `I.precomp g` to `I`.  -/
CategoryTheory.GrothendieckTopology.Cover.Arrow.precompRelation : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X : C} →
      {J : CategoryTheory.GrothendieckTopology C} →
        {S : J.Cover X} → (I : S.Arrow) → {Z : C} → (g : Z ⟶ I.Y) → (I.precomp g).Relation I
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey_insert_le_minKey : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  (h : t.WF) {k : α} {v : β k} {he : t.isEmpty = false},
  (compare ((Std.DTreeMap.Internal.Impl.insert k v t ⋯).impl.minKey ⋯) (t.minKey he)).isLE = true
-- Mathlib.LinearAlgebra.Multilinear.DirectSum
MultilinearMap.fromDirectSumEquiv_lof : ∀ {R : Type u_1} {ι : Type u_2} {M' : Type u_3} {κ : ι → Type u_4} {M : (i : ι) → κ i → Type u_5}
  [inst : CommSemiring R] [inst_1 : (i : ι) → (j : κ i) → AddCommMonoid (M i j)]
  [inst_2 : (i : ι) → (j : κ i) → Module R (M i j)] [inst_3 : AddCommMonoid M'] [inst_4 : Module R M']
  [inst_5 : DecidableEq ι] [inst_6 : Finite ι] [inst_7 : (i : ι) → DecidableEq (κ i)]
  (f : (p : (i : ι) → κ i) → MultilinearMap R (fun i => M i (p i)) M') (p : (i : ι) → κ i) (x : (i : ι) → M i (p i)),
  ((MultilinearMap.fromDirectSumEquiv f) fun i => (DirectSum.lof R (κ i) (M i) (p i)) (x i)) = (f p) x
-- Init.Grind.Ring.Basic
Lean.Grind.Ring.intCast_mul : ∀ {α : Type u} [inst : Lean.Grind.Ring α] (x y : ℤ), ↑(x * y) = ↑x * ↑y
-- Std.Sync.Channel
/-- Try to receive a value from the channel, if this can be completed right away without blocking return
`some value`, otherwise return `none`.
 -/
Std.Channel.tryRecv : {α : Type} → Std.Channel α → BaseIO (Option α)
-- Lean.Elab.Tactic.Try
/-- Like `elabTryCore`, but returns the suggestion array (as raw tactic syntaxes) instead of
emitting "Try this:" messages. Used by the `autoTry` linter, which formats and emits the
suggestions itself so they can be rendered as append-to-tactic-sequence edits.  -/
Lean.Elab.Tactic.Try.collectTryCoreSuggestions : optParam Lean.Try.Config { } → Lean.Elab.Tactic.TacticM (Array (Lean.TSyntax `tactic))
-- Mathlib.MeasureTheory.Group.FoelnerFilter
maxFoelner.eq_1 : ∀ (G : Type u_1) {X : Type u_2} [inst : MeasurableSpace X] (μ : MeasureTheory.Measure X) [inst_1 : Group G]
  [inst_2 : MulAction G X],
  maxFoelner G μ =
    Filter.principal {s | MeasurableSet s ∧ μ s ≠ 0 ∧ μ s ≠ ⊤} ⊓
      ⨅ g, Filter.comap (fun s => μ (symmDiff (g • s) s) / μ s) (nhds 0)
-- Mathlib.Tactic.NormNum.Result
Mathlib.Meta.NormNum.IsRat.to_raw_eq : ∀ {α : Type u} {n : ℤ} {d : ℕ} [inst : DivisionRing α] {a : α}, Mathlib.Meta.NormNum.IsRat a n d → a = Rat.rawCast n d
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey?_inter_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k : α}, k ∉ t₂ → (t₁ ∩ t₂).getKey? k = none
-- Mathlib.GroupTheory.Complement
/-- A left transversal is in bijection with left cosets.  -/
Subgroup.IsComplement.leftQuotientEquiv : {G : Type u_1} → [inst : Group G] → {H : Subgroup G} → {S : Set G} → Subgroup.IsComplement S ↑H → G ⧸ H ≃ ↑S
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.coeff_erase : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] (m : M) (x : MonoidAlgebra R M),
  (MonoidAlgebra.erase m x).coeff = Finsupp.erase m x.coeff
-- Mathlib.Data.Seq.Basic
Stream'.Seq.Pairwise_tail : ∀ {α : Type u} {R : α → α → Prop} {s : Stream'.Seq α}, Stream'.Seq.Pairwise R s → Stream'.Seq.Pairwise R s.tail
-- Mathlib.Topology.LocallyFinsupp
Function.locallyFinsuppWithin.max_apply : ∀ {X : Type u_1} [inst : TopologicalSpace X] {U : Set X} {Y : Type u_2} [inst_1 : SemilatticeSup Y] [inst_2 : Zero Y]
  {D₁ D₂ : Function.locallyFinsuppWithin U Y} {x : X}, (D₁ ⊔ D₂) x = D₁ x ⊔ D₂ x
-- Mathlib.Topology.Algebra.Constructions.DomMulAct
DomMulAct.instT1Space : ∀ {M : Type u_1} [inst : TopologicalSpace M] [T1Space M], T1Space Mᵈᵐᵃ
-- Mathlib.Data.Finset.Piecewise
Finset.piecewise_insert_self : ∀ {ι : Type u_1} {π : ι → Sort u_2} (s : Finset ι) (f g : (i : ι) → π i) [inst : DecidableEq ι] {j : ι}
  [inst_1 : (i : ι) → Decidable (i ∈ insert j s)], (insert j s).piecewise f g j = f j
-- Lean.Elab.Command.Scope
/-- If true (default: false), all declarations that fail to compile
automatically receive the `noncomputable` modifier.
A scope with this flag set is created by `noncomputable section`.

Recall that a new scope inherits all values from its parent scope,
so all sections and namespaces nested within a `noncomputable` section also have this flag set.
 -/
Lean.Elab.Command.Scope.isNoncomputable : Lean.Elab.Command.Scope → Bool
-- Mathlib.Computability.PartrecCode
_private.Mathlib.Computability.PartrecCode.0.Nat.Partrec.Code.evaln.match_1.splitter : (motive : ℕ → Nat.Partrec.Code → Sort u_1) →
  (x : ℕ) →
    (x_1 : Nat.Partrec.Code) →
      ((x : Nat.Partrec.Code) → motive 0 x) →
        ((k : ℕ) → motive k.succ Nat.Partrec.Code.zero) →
          ((k : ℕ) → motive k.succ Nat.Partrec.Code.succ) →
            ((k : ℕ) → motive k.succ Nat.Partrec.Code.left) →
              ((k : ℕ) → motive k.succ Nat.Partrec.Code.right) →
                ((k : ℕ) → (cf cg : Nat.Partrec.Code) → motive k.succ (cf.pair cg)) →
                  ((k : ℕ) → (cf cg : Nat.Partrec.Code) → motive k.succ (cf.comp cg)) →
                    ((k : ℕ) → (cf cg : Nat.Partrec.Code) → motive k.succ (cf.prec cg)) →
                      ((k : ℕ) → (cf : Nat.Partrec.Code) → motive k.succ cf.rfind') → motive x x_1
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.get?_union_of_not_mem_right : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, k ∉ m₂ → (m₁ ∪ m₂).get? k = m₁.get? k
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.instCategoryArrow : {T : Type u} → [inst : CategoryTheory.Category.{v, u} T] → CategoryTheory.Category.{v, max u v} (CategoryTheory.Arrow T)
-- Mathlib.Algebra.Polynomial.Homogenize
Polynomial.homogenize_C : ∀ {R : Type u_1} [inst : CommSemiring R] (c : R) (n : ℕ),
  (Polynomial.C c).homogenize n = MvPolynomial.C c * MvPolynomial.X 1 ^ n
-- Aesop.Builder.Basic
Aesop.instInhabitedRuleBuilderOptions.default : Aesop.RuleBuilderOptions
-- Init.Data.UInt.Lemmas
USize.sub_lt : ∀ {a b : USize}, 0 < b → b ≤ a → a - b < a
-- Mathlib.Algebra.Homology.Embedding.CochainComplex
CochainComplex.isGE_of_iso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K L : CochainComplex C ℤ} (e : K ≅ L) (n : ℤ) [K.IsGE n], L.IsGE n
-- Mathlib.AlgebraicTopology.SimplicialSet.RelativeMorphism
SSet.RelativeMorphism.mk.inj : ∀ {X Y : SSet} {A : X.Subcomplex} {B : Y.Subcomplex} {φ : A.toSSet ⟶ B.toSSet} {map : X ⟶ Y}
  {comm :
    autoParam (CategoryTheory.CategoryStruct.comp A.ι map = CategoryTheory.CategoryStruct.comp φ B.ι)
      SSet.RelativeMorphism.comm._autoParam}
  {map_1 : X ⟶ Y}
  {comm_1 :
    autoParam (CategoryTheory.CategoryStruct.comp A.ι map_1 = CategoryTheory.CategoryStruct.comp φ B.ι)
      SSet.RelativeMorphism.comm._autoParam},
  { map := map, comm := comm } = { map := map_1, comm := comm_1 } → map = map_1
-- Mathlib.Algebra.Category.MonCat.Adjunctions
/-- The `adjoinOne`-forgetful adjunction from `Semigrp` to `MonCat`.  -/
MonCat.adjoinOneAdj : MonCat.adjoinOne ⊣ CategoryTheory.forget₂ MonCat Semigrp
-- Mathlib.Data.PNat.Basic
PNat.bot_eq_one : ⊥ = 1
-- Mathlib.CategoryTheory.Dialectica.Monoidal
CategoryTheory.Dial.leftUnitor_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] {X Y : CategoryTheory.Dial C} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom
        (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Dial C))) f)
      (CategoryTheory.MonoidalCategoryStruct.leftUnitor Y).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom f
-- Mathlib.Topology.Order.Basic
/-- (Order) topology on a partial order `α` generated by the subbase of open intervals
`(a, ∞) = { x ∣ a < x }, (-∞, b) = {x ∣ x < b}` for all `a, b` in `α`. We do not register it as an
instance as many ordered sets are already endowed with the same topology, most often in a non-defeq
way though. Register as a local instance when necessary.  -/
Preorder.topology : (α : Type u_1) → [Preorder α] → TopologicalSpace α
-- Mathlib.CategoryTheory.Monoidal.Braided.Opposite
CategoryTheory.BraidedCategory.unop_tensorμ : ∀ {C : Type u_2} [inst : CategoryTheory.Category.{v_2, u_2} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X Y W Z : Cᵒᵖ),
  (CategoryTheory.MonoidalCategory.tensorμ X W Y Z).unop =
    CategoryTheory.MonoidalCategory.tensorμ (Opposite.unop X) (Opposite.unop Y) (Opposite.unop W) (Opposite.unop Z)
-- Std.Data.TreeMap.Raw.Basic
/-- If there is no mapping for the given key, inserts the given mapping into the map. Otherwise,
returns the map unaltered.
 -/
Std.TreeMap.Raw.insertIfNew : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap.Raw α β cmp → α → β → Std.TreeMap.Raw α β cmp
-- Init.Data.List.Lex
List.lex_trans : ∀ {α : Type u_1} {l₁ l₂ l₃ : List α} {r : α → α → Prop},
  (∀ {x y z : α}, r x y → r y z → r x z) → List.Lex r l₁ l₂ → List.Lex r l₂ l₃ → List.Lex r l₁ l₃
-- Lean.Data.Lsp.Internal
Lean.Lsp.RefIdent.const.inj : ∀ {moduleName identName moduleName_1 identName_1 : String},
  Lean.Lsp.RefIdent.const moduleName identName = Lean.Lsp.RefIdent.const moduleName_1 identName_1 →
    moduleName = moduleName_1 ∧ identName = identName_1
-- Mathlib.Topology.Sets.OpenCover
/-- Given an open cover and a basis,
the set of basis elements contained in any of the covers is still a cover.  -/
TopologicalSpace.Opens.IsBasis.isOpenCover_mem_and_le : ∀ {ι : Type u_1} {X : Type u_3} [inst : TopologicalSpace X] {S : Set (TopologicalSpace.Opens X)},
  TopologicalSpace.Opens.IsBasis S →
    ∀ {U : ι → TopologicalSpace.Opens X}, TopologicalSpace.IsOpenCover U → TopologicalSpace.IsOpenCover fun V => (↑V).1
-- Mathlib.Data.Set.Finite.Basic
Set.finite_lt_nat : ∀ (n : ℕ), {i | i < n}.Finite
-- Lean.Meta.Sym.SymM
Lean.Meta.Sym.SharedExprs.intExpr : Lean.Meta.Sym.SharedExprs → Lean.Expr
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.strictAntiOn_logb : ∀ {b : ℝ}, 1 < b → StrictAntiOn (Real.logb b) (Set.Iio 0)
-- Mathlib.Order.SetDissipate
Set.dissipate_succ : ∀ {α : Type u_1} (s : ℕ → Set α) (n : ℕ), Set.dissipate s (n + 1) = Set.dissipate s n ∩ s (n + 1)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKey_insertManyIfNewUnit!_list_of_mem : ∀ {α : Type u} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α fun x => Unit} [Std.TransOrd α],
  t.WF →
    ∀ {l : List α} {k : α}
      {h' : Std.DTreeMap.Internal.Impl.contains k ↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit! t l) = true}
      (contains : k ∈ t),
      (↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit! t l)).getKey k h' = t.getKey k contains
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.norm.eq_1 : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K],
  NumberField.mixedEmbedding.norm =
    { toFun := fun x => ∏ w, (NumberField.mixedEmbedding.normAtPlace w) x ^ w.mult, map_zero' := ⋯, map_one' := ⋯,
      map_mul' := ⋯ }
-- Mathlib.Data.Fintype.Defs
/-- The `Finset` containing all elements of a `Fintype`  -/
Fintype.elems : {α : Type u_4} → [self : Fintype α] → Finset α
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cochain.instModuleOfLinear : {C : Type u_3} →
  [inst : CategoryTheory.Category.{u_2, u_3} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {R : Type u_1} →
        [inst_2 : Ring R] →
          [CategoryTheory.Linear R C] →
            (F G : CochainComplex C ℤ) → (n : ℤ) → Module R (CochainComplex.HomComplex.Cochain F G n)
-- Mathlib.Order.CompactlyGenerated.Basic
DirectedOn.disjoint_sSup_right : ∀ {α : Type u_2} [inst : CompleteLattice α] [IsCompactlyGenerated α] {a : α} {s : Set α},
  DirectedOn (fun x1 x2 => x1 ≤ x2) s → (Disjoint a (sSup s) ↔ ∀ ⦃b : α⦄, b ∈ s → Disjoint a b)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence
/-- The connecting homomorphism `Hᵢ(G, X₃) ⟶ Hⱼ(G, X₁)` associated to an exact sequence
`0 ⟶ X₁ ⟶ X₂ ⟶ X₃ ⟶ 0` of representations.  -/
groupHomology.δ : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      {X : CategoryTheory.ShortComplex (Rep.{u, u, u} k G)} →
        X.ShortExact → (i j : ℕ) → j + 1 = i → (groupHomology X.X₃ i ⟶ groupHomology X.X₁ j)
-- Init.Data.String.Basic
String.Slice.utf8ByteSize_copy : ∀ {s : String.Slice}, s.copy.utf8ByteSize = s.utf8ByteSize
-- Mathlib.Algebra.Category.Grp.Basic
AddCommGrpCat.forget_reflects_isos : (CategoryTheory.forget AddCommGrpCat).ReflectsIsomorphisms
-- Mathlib.Algebra.Category.Grp.FilteredColimits
AddCommGrpCat.FilteredColimits.colimitAddCommGroup : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    [inst_1 : CategoryTheory.IsFiltered J] →
      (F : CategoryTheory.Functor J AddCommGrpCat) → AddCommGroup ↑(AddCommGrpCat.FilteredColimits.G F)
-- Mathlib.MeasureTheory.Constructions.BorelSpace.WithTop
WithTop.measurable_untopD : ∀ {ι : Type u_1} [inst : LinearOrder ι] [inst_1 : TopologicalSpace ι] [inst_2 : OrderTopology ι]
  [inst_3 : MeasurableSpace ι] [BorelSpace ι] (d : ι), Measurable (WithTop.untopD d)
-- Mathlib.Topology.Algebra.Module.FiniteDimension
/-- A continuous linear equivalence between two finite-dimensional topological vector spaces over a
complete normed field of the same (finite) dimension.  -/
ContinuousLinearEquiv.ofFinrankEq : {𝕜 : Type u} →
  [hnorm : NontriviallyNormedField 𝕜] →
    {E : Type v} →
      [inst : AddCommGroup E] →
        [inst_1 : Module 𝕜 E] →
          [inst_2 : TopologicalSpace E] →
            [IsTopologicalAddGroup E] →
              [ContinuousSMul 𝕜 E] →
                {F : Type w} →
                  [inst_5 : AddCommGroup F] →
                    [inst_6 : Module 𝕜 F] →
                      [inst_7 : TopologicalSpace F] →
                        [IsTopologicalAddGroup F] →
                          [ContinuousSMul 𝕜 F] →
                            [CompleteSpace 𝕜] →
                              [T2Space E] →
                                [T2Space F] →
                                  [FiniteDimensional 𝕜 E] →
                                    [FiniteDimensional 𝕜 F] → Module.finrank 𝕜 E = Module.finrank 𝕜 F → E ≃L[𝕜] F
-- Mathlib.Algebra.Exact.Basic
/-- **Alias** of the forward direction of `Function.Exact.iff_addMonoidHom_rangeRestrict`.

---

Two maps `f : M →+ N` and `g : N →+ P` are exact if and only if the induced maps
`AddMonoidHom.range f → N → AddMonoidHom.range g` are exact.  -/
Function.Exact.addMonoidHom_rangeRestrict : ∀ {M : Type u_2} {N : Type u_4} {P : Type u_6} [inst : AddGroup M] [inst_1 : AddGroup N] [inst_2 : AddGroup P]
  {f : M →+ N} {g : N →+ P}, Function.Exact ⇑f ⇑g → Function.Exact ⇑f.range.subtype ⇑g.rangeRestrict
-- Init.Data.ByteArray.Basic
/-- Converts a packed array of bytes to a linked list.
 -/
ByteArray.toList : ByteArray → List UInt8
-- Mathlib.Topology.MetricSpace.BundledFun
PseudoMetric.isSymm_closedBall : ∀ {X : Type u_1} {R : Type u_2} [inst : Add R] [inst_1 : Zero R] [inst_2 : LE R] (d : PseudoMetric X R) {ε : R},
  SetRel.IsSymm {xy | d xy.1 xy.2 ≤ ε}