mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Bicategory.Yoneda
CategoryTheory.Bicategory.yoneda₀_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_α : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] (x : B) (y : Bᵒᵖ),
  ↑((CategoryTheory.Bicategory.yoneda₀ x).obj y) = (Opposite.unop y ⟶ x)
-- Mathlib.RingTheory.Valuation.ValuationRing
ValuationRing.instInvValueGroup : (A : Type u) →
  [inst : CommRing A] → (K : Type v) → [inst_1 : Field K] → [inst_2 : Algebra A K] → Inv (ValuationRing.ValueGroup A K)
-- Lean.Elab.ParseImportsFast
Lean.PrintImportsResult.mk : Array Lean.PrintImportResult → Lean.PrintImportsResult
-- Mathlib.GroupTheory.Subgroup.Simple
/-- A `Group` is simple when it has exactly two normal `Subgroup`s.  -/
IsSimpleGroup : (G : Type u_1) → [Group G] → Prop
-- Init.Data.SInt.Lemmas
Int16.toInt_maxValue_add_one : Int16.maxValue.toInt + 1 = 2 ^ 15
-- Mathlib.Topology.MetricSpace.PiNat
/-- Given a countable family of metric spaces, one may put a distance on their product `Π i, E i`.

It is highly non-canonical, though, and therefore not registered as a global instance.
The distance we use here is `dist x y = ∑' i, min (1/2)^(encode i) (dist (x i) (y i))`.  -/
PiCountable.dist : {ι : Type u_2} → [Encodable ι] → {F : ι → Type u_3} → [(i : ι) → PseudoMetricSpace (F i)] → Dist ((i : ι) → F i)
-- Mathlib.RingTheory.Coalgebra.Basic
CoalgebraStruct.mk : {R : Type u} →
  {A : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid A] →
        [inst_2 : Module R A] → (A →ₗ[R] TensorProduct R A A) → (A →ₗ[R] R) → CoalgebraStruct R A
-- Mathlib.CategoryTheory.Limits.FinallySmall
CategoryTheory.initiallySmall_of_initial_of_initiallySmall : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {K : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} K]
  [CategoryTheory.InitiallySmall K] (F : CategoryTheory.Functor K J) [F.Initial], CategoryTheory.InitiallySmall J
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equifibered
CategoryTheory.NatTrans.Equifibered.rightOp : ∀ {J : Type u_1} {C : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_3} C] {F G : CategoryTheory.Functor Jᵒᵖ C} {α : F ⟶ G},
  CategoryTheory.NatTrans.Equifibered α → CategoryTheory.NatTrans.Coequifibered (CategoryTheory.NatTrans.rightOp α)
-- Lean.Compiler.ExternAttr
_private.Lean.Compiler.ExternAttr.0.Lean.expandExternPatternAux.eq_def : ∀ (args : List String) (pattern : String) (it : pattern.Pos) (r : String),
  Lean.expandExternPatternAux args pattern it r =
    if h : it.IsAtEnd then r
    else
      have c := it.get h;
      if c ≠ '#' then Lean.expandExternPatternAux args pattern (it.next h) (r.push c)
      else
        let it₁ := it.next h;
        match Lean.parseOptNum✝ (pattern.sliceFrom it₁) (pattern.sliceFrom it₁).startPos 0 with
        | (it₂, j) =>
          have j := j - 1;
          have this := ⋯;
          Lean.expandExternPatternAux args pattern (String.Pos.ofSliceFrom it₂) (r ++ args.getD j "")
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.Measure.snd.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  (ρ : MeasureTheory.Measure (α × β)), ρ.snd = MeasureTheory.Measure.map Prod.snd ρ
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.toList_insert_perm : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [inst : BEq α]
  [Std.TransCmp cmp] [Std.LawfulBEqCmp cmp],
  t.WF →
    ∀ {k : α} {v : β k},
      (t.insert k v).toList.Perm (⟨k, v⟩ :: List.filter (fun x => decide ¬(k == x.fst) = true) t.toList)
-- Mathlib.Algebra.Category.CoalgCat.ComonEquivalence
CoalgCat.ofComonObjCoalgebraStruct_comul : ∀ {R : Type u} [inst : CommRing R] (X : ModuleCat R) [inst_1 : CategoryTheory.ComonObj X],
  CoalgebraStruct.comul = ModuleCat.Hom.hom CategoryTheory.ComonObj.comul
-- Mathlib.Combinatorics.SimpleGraph.Ends.Defs
SimpleGraph.ComponentCompl.hom_eq_iff_le : ∀ {V : Type u} {G : SimpleGraph V} {K L : Set V} (C : G.ComponentCompl L) (h : K ⊆ L) (D : G.ComponentCompl K),
  SimpleGraph.ComponentCompl.hom h C = D ↔ ↑C ⊆ ↑D
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.isSt_trans_real : ∀ {r s t : ℝ}, (↑r).IsSt s → (↑s).IsSt t → (↑r).IsSt t
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
AlgebraicGeometry.LocallyRingedSpace.toΓSpec_base : ∀ (X : AlgebraicGeometry.LocallyRingedSpace), X.toΓSpec.base = X.toΓSpecBase
-- Mathlib.Algebra.Category.ModuleCat.Semi
/-- Turn a homomorphism into a bilinear map.  -/
SemimoduleCat.Hom.hom₂ : {R : Type u_1} →
  [inst : CommSemiring R] → {M N P : SemimoduleCat R} → (M ⟶ SemimoduleCat.of R (N ⟶ P)) → ↑M →ₗ[R] ↑N →ₗ[R] ↑P
-- Mathlib.Topology.Algebra.InfiniteSum.Group
/-- A more general version of `Summable.congr`, allowing the functions to
disagree on a finite set.  -/
Summable.congr_cofinite : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommGroup α] [inst_1 : TopologicalSpace α] [IsTopologicalAddGroup α]
  {f g : β → α}, Summable f → f =ᶠ[Filter.cofinite] g → Summable g
-- Init.Data.String.Lemmas.Pattern.Split.Char
_private.Init.Data.String.Lemmas.Pattern.Split.Char.0.String.Slice.Pattern.Model.split.match_1.eq_1 : ∀ {s : String.Slice} (motive : Option s.Pos → Sort u_1) (pos : s.Pos)
  (h_1 : (pos_1 : s.Pos) → some pos = some pos_1 → motive (some pos_1)) (h_2 : some pos = none → motive none),
  (match hd : some pos with
    | some pos_1 => h_1 pos_1 hd
    | none => h_2 hd) =
    h_1 pos ⋯
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey?_emptyWithCapacity : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {a : α} {c : ℕ},
  (Std.HashMap.emptyWithCapacity c).getKey? a = none
-- Mathlib.Data.Finset.Piecewise
Finset.piecewise_mem_set_pi : ∀ {ι : Type u_1} (s : Finset ι) [inst : (j : ι) → Decidable (j ∈ s)] {π : ι → Type u_3} {t : Set ι}
  {t' : (i : ι) → Set (π i)} {f g : (i : ι) → π i}, f ∈ t.pi t' → g ∈ t.pi t' → s.piecewise f g ∈ t.pi t'
-- Lean.Server.FileWorker.SemanticHighlighting
/-- Adds a surrounding token to the set. These are tokens whose interval includes the boundaries being
processed, but are superseded by the current token.
 -/
_private.Lean.Server.FileWorker.SemanticHighlighting.0.Lean.Server.FileWorker.HandleOverlapState.insertSurrounding : Lean.Server.FileWorker.HandleOverlapState✝ →
  Lean.Server.FileWorker.AbsoluteLspSemanticToken → Lean.Server.FileWorker.HandleOverlapState✝
-- Mathlib.Topology.Homotopy.Basic
/-- The type of homotopies between `f₀ f₁ : C(X, Y)`, where the intermediate maps satisfy the predicate
`P : C(X, Y) → Prop`
 -/
ContinuousMap.HomotopyWith : {X : Type u} →
  {Y : Type v} →
    [inst : TopologicalSpace X] → [inst_1 : TopologicalSpace Y] → C(X, Y) → C(X, Y) → (C(X, Y) → Prop) → Type (max u v)
-- Mathlib.Algebra.Homology.HomologicalComplexLimits
HomologicalComplex.instPreservesFiniteLimitsSingle : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] {c : ComplexShape ι}
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_2 : CategoryTheory.Limits.HasZeroObject C]
  [inst_3 : DecidableEq ι] (i : ι), CategoryTheory.Limits.PreservesFiniteLimits (HomologicalComplex.single C c i)
-- Mathlib.Order.WithBot
WithTop.not_top_lt : ∀ {α : Type u_1} [inst : LT α] (a : WithTop α), ¬⊤ < a
-- Mathlib.Analysis.Normed.Group.Basic
SeminormedAddGroup.disjoint_nhds : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] (x : E) (f : Filter E),
  Disjoint (nhds x) f ↔ ∃ δ > 0, ∀ᶠ (y : E) in f, δ ≤ ‖-y + x‖
-- Mathlib.Order.Lattice
Prod.instMin_mathlib.eq_1 : ∀ (α : Type u) (β : Type v) [inst : Min α] [inst_1 : Min β],
  Prod.instMin_mathlib α β = { min := fun p q => (p.1 ⊓ q.1, p.2 ⊓ q.2) }
-- Mathlib.RingTheory.Smooth.IntegralClosure
StandardEtalePresentation.baseChange.eq_1 : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] (P : StandardEtalePresentation R S),
  P.baseChange = { P := P.map (algebraMap R T), x := 1 ⊗ₜ[R] P.x, hasMap := ⋯, lift_bijective := ⋯ }
-- Mathlib.CategoryTheory.Sites.LocallySurjective
CategoryTheory.Presheaf.IsLocallySurjective.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} A] {FA : A → A → Type u_1} {CA : A → Type w'}
  [inst_2 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] [inst_3 : CategoryTheory.ConcreteCategory A FA]
  {F G : CategoryTheory.Functor Cᵒᵖ A} {f : F ⟶ G},
  (∀ {U : C} (s : CategoryTheory.ToType (G.obj (Opposite.op U))), CategoryTheory.Presheaf.imageSieve f s ∈ J U) →
    CategoryTheory.Presheaf.IsLocallySurjective J f
-- Mathlib.RingTheory.NormalClosure
_private.Mathlib.RingTheory.NormalClosure.0.Ring.termE : Lean.ParserDescr
-- Mathlib.LinearAlgebra.FiniteDimensional.Basic
/-- Any division ring is stably finite.  -/
LinearMap.instIsStablyFiniteRing : ∀ {K : Type u} [inst : DivisionRing K], IsStablyFiniteRing K
-- Lean.Elab.Syntax
/-- See comment at `Parser.ParserCategory`.  -/
Lean.Elab.Term.ToParserDescrContext.behavior : Lean.Elab.Term.ToParserDescrContext → Lean.Parser.LeadingIdentBehavior
-- Mathlib.Data.Int.LeastGreatest
/-- A computable version of `exists_greatest_of_bdd`: given a decidable predicate on the
integers, with an explicit upper bound and a proof that it is somewhere true, return
the greatest value for which the predicate is true.  -/
Int.greatestOfBdd : {P : ℤ → Prop} →
  [DecidablePred P] → (b : ℤ) → (∀ (z : ℤ), P z → z ≤ b) → (∃ z, P z) → { ub // P ub ∧ ∀ (z : ℤ), P z → z ≤ ub }
-- Mathlib.CategoryTheory.Types.Basic
/-- `ofTypeFunctor m` converts from Lean's `Type`-based `Category` to `CategoryTheory`. This
allows us to use these functors in category theory.  -/
CategoryTheory.ofTypeFunctor : (m : Type u → Type v) → [inst : Functor m] → [LawfulFunctor m] → CategoryTheory.Functor (Type u) (Type v)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey?_eraseKey_self : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k : α},
  Std.Internal.List.DistinctKeys l → Std.Internal.List.getKey? k (Std.Internal.List.eraseKey k l) = none
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
_private.Mathlib.Combinatorics.Enumerative.IncidenceAlgebra.0.IncidenceAlgebra.muFun_apply : ∀ (𝕜 : Type u_2) {α : Type u_5} [inst : AddCommGroup 𝕜] [inst_1 : One 𝕜] [inst_2 : Preorder α]
  [inst_3 : LocallyFiniteOrder α] [inst_4 : DecidableEq α] (a b : α),
  IncidenceAlgebra.muFun✝ 𝕜 a b = if a = b then 1 else -∑ x ∈ (Finset.Ico a b).attach, IncidenceAlgebra.muFun✝ 𝕜 a ↑x
-- Init.Data.Slice.Lemmas
Std.Slice.forIn_toArray : ∀ {α : Type v} {γ : Type u} {β : Type v} {m : Type w → Type x} [inst : Monad m] [LawfulMonad m] {δ : Type w}
  [inst_2 : Std.ToIterator (Std.Slice γ) Id α β] [inst_3 : Std.Iterator α Id β] [inst_4 : Std.IteratorLoop α Id m]
  [Std.LawfulIteratorLoop α Id m] [Std.Iterators.Finite α Id] {s : Std.Slice γ} {init : δ}
  {f : β → δ → m (ForInStep δ)}, forIn s.toArray init f = forIn s init f
-- Mathlib.GroupTheory.GroupAction.MultipleTransitivity
/-- For any two embeddings from a finite type into `β`, some permutation of `β` maps one to the
other. This is the action-form of `Equiv.Perm.exists_extending_pair`.  -/
Equiv.Perm.exists_smul_eq_embedding : ∀ {ι : Type u_2} [Finite ι] {β : Type u_3} (x y : ι ↪ β), ∃ σ, σ • x = y
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.neg_bind : ∀ {α β : Type u} (f : α → FreeAddGroup β) (x : FreeAddGroup α), -x >>= f = -(x >>= f)
-- Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Nat.nthRoot.eq_3 : ∀ (x n : ℕ), n.succ.succ.nthRoot x = Nat.nthRoot.go n x x x
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr
Std.Tactic.BVDecide.BVExpr.Cache.empty.eq_1 : ∀ {aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit}, Std.Tactic.BVDecide.BVExpr.Cache.empty = { map := ∅, hbound := ⋯ }
-- Init.ShareCommon
ShareCommon.StateFactoryImpl : Type 1
-- Mathlib.Analysis.SpecialFunctions.Log.Summable
Real.multipliable_one_add_of_summable : ∀ {ι : Type u_1} {f : ι → ℝ}, Summable f → Multipliable fun i => 1 + f i
-- Mathlib.AlgebraicTopology.ModelCategory.Instances
HomotopicalAlgebra.instIsStableUnderRetractsTrivialCofibrationsOfCofibrationsOfWeakEquivalences : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C]
  [inst_2 : HomotopicalAlgebra.CategoryWithCofibrations C] [(HomotopicalAlgebra.cofibrations C).IsStableUnderRetracts]
  [(HomotopicalAlgebra.weakEquivalences C).IsStableUnderRetracts],
  (HomotopicalAlgebra.trivialCofibrations C).IsStableUnderRetracts
-- Init.Data.Vector.Count
Vector.countP_eq_zero : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {p : α → Bool}, Vector.countP p xs = 0 ↔ ∀ a ∈ xs, ¬p a = true
-- Lean.Setup
/-- Dynamic libraries to load with the module.  -/
Lean.ModuleSetup.dynlibs : Lean.ModuleSetup → Array System.FilePath
-- Mathlib.Analysis.Normed.Group.Basic
dist_norm_norm_le_norm_neg_add : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] (a b : E), dist ‖a‖ ‖b‖ ≤ ‖-a + b‖
-- Mathlib.Order.Interval.Set.InitialSeg
/-- **Alias** of `Set.principalSegIio_apply`. -/
Set.principalSegIio_toRelEmbedding : ∀ {α : Type u_1} [inst : Preorder α] {j : α} (k : ↑(Set.Iio j)), (Set.principalSegIio j).toRelEmbedding k = ↑k
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.translationNumber_units_inv : ∀ (f : CircleDeg1Liftˣ), (↑f⁻¹).translationNumber = -(↑f).translationNumber
-- Init.Data.SInt.Lemmas
Int64.div_zero : ∀ {a : Int64}, a / 0 = 0
-- Mathlib.RingTheory.AdicCompletion.AsTensorProduct
_private.Mathlib.RingTheory.AdicCompletion.AsTensorProduct.0.AdicCompletion.piEquivOfFintype_comp_ofTensorProduct_eq : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) (ι : Type u_4) [inst_1 : Fintype ι] [inst_2 : DecidableEq ι],
  ↑(AdicCompletion.piEquivOfFintype I fun x => R) ∘ₗ AdicCompletion.ofTensorProduct I (ι → R) =
    ↑(TensorProduct.piScalarRight R (AdicCompletion I R) (AdicCompletion I R) ι)
-- Mathlib.Analysis.Normed.Group.Constructions
Pi.nnnorm_single : ∀ {ι : Type u_1} {G : ι → Type u_4} [inst : Fintype ι] [inst_1 : DecidableEq ι]
  [inst_2 : (i : ι) → NormedAddCommGroup (G i)] {i : ι} (y : G i), ‖Pi.single i y‖₊ = ‖y‖₊
-- Mathlib.AlgebraicGeometry.Morphisms.Immersion
AlgebraicGeometry.isImmersion_eq_inf : @AlgebraicGeometry.IsImmersion =
  @AlgebraicGeometry.IsPreimmersion ⊓
    AlgebraicGeometry.topologically fun {x x_1} x_2 x_3 f => IsLocallyClosed (Set.range f)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey_filter_not_contains : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l₁ : List ((a : α) × β a)} {l₂ : List α} {k : α},
  Std.Internal.List.DistinctKeys l₁ →
    ∀ {h₁ : Std.Internal.List.containsKey k (List.filter (fun p => !l₂.contains p.fst) l₁) = true}
      {h₂ : Std.Internal.List.containsKey k l₁ = true},
      Std.Internal.List.getKey k (List.filter (fun p => !l₂.contains p.fst) l₁) h₁ = Std.Internal.List.getKey k l₁ h₂
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.hsum_single : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : AddCommMonoid R] {ι : Type u_7}
  [inst_2 : DecidableEq ι] (i : ι) (x : HahnSeries Γ R), (HahnSeries.SummableFamily.single i x).hsum = x
-- Mathlib.Analysis.Normed.Operator.Banach
ContinuousLinearMap.NonlinearRightInverse.bound : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜'] {σ : 𝕜 →+* 𝕜'}
  {E : Type u_3} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {F : Type u_4}
  [inst_4 : NormedAddCommGroup F] [inst_5 : NormedSpace 𝕜' F] {f : E →SL[σ] F} (fsymm : f.NonlinearRightInverse)
  (y : F), ‖fsymm.toFun y‖ ≤ ↑fsymm.nnnorm * ‖y‖
-- Mathlib.LinearAlgebra.Matrix.Cartan
CartanMatrix.E₆_isSymm : CartanMatrix.E₆.IsSymm
-- Init.Data.Iterators.Basic
Std.IterM.ext_iff : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} {x y : Std.IterM m β}, x = y ↔ x.internalState = y.internalState
-- Mathlib.Logic.Equiv.Defs
/-- If `α` has a unique element, then it is equivalent to any `PUnit`.  -/
Equiv.equivPUnit : (α : Sort u) → [Unique α] → α ≃ PUnit.{v}
-- Mathlib.Logic.Equiv.Finset
/-- Outputs the list of differences minus one of the input list, that is
`lower' [a₁, a₂, a₃, ...] n = [a₁ - n, a₂ - a₁ - 1, a₃ - a₂ - 1, ...]`.  -/
Denumerable.lower' : List ℕ → ℕ → List ℕ
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Ordinal.cof_lsub_le_lift : ∀ {ι : Type u} (f : ι → Ordinal.{max u v}), (Ordinal.lsub f).cof ≤ Cardinal.lift.{v, u} (Cardinal.mk ι)
-- Mathlib.CategoryTheory.Limits.HasLimits
/-- The canonical morphism from `G` applied to the limit of `F` to the limit of `F ⋙ G`.
 -/
CategoryTheory.Limits.limit.post : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {D : Type u'} →
          [inst_2 : CategoryTheory.Category.{v', u'} D] →
            (F : CategoryTheory.Functor J C) →
              [inst_3 : CategoryTheory.Limits.HasLimit F] →
                (G : CategoryTheory.Functor C D) →
                  [inst_4 : CategoryTheory.Limits.HasLimit (F.comp G)] →
                    G.obj (CategoryTheory.Limits.limit F) ⟶ CategoryTheory.Limits.limit (F.comp G)
-- Init.Data.Nat.ToString
Nat.repr_eq_repr : ∀ {n : ℕ}, repr n = Std.Format.text n.repr
-- Mathlib.Algebra.BigOperators.Group.List.Basic
List.rel_prod : ∀ {M : Type u_4} {N : Type u_5} [inst : Monoid M] [inst_1 : Monoid N] {R : M → N → Prop},
  R 1 1 →
    (Relator.LiftFun R (Relator.LiftFun R R) (fun x1 x2 => x1 * x2) fun x1 x2 => x1 * x2) →
      Relator.LiftFun (List.Forall₂ R) R List.prod List.prod
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Over.changeProp_obj_hom : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {P Q : CategoryTheory.MorphismProperty T} {X : T}
  [inst_1 : Q.IsMultiplicative] {P' Q' : CategoryTheory.MorphismProperty T} [inst_2 : Q'.IsMultiplicative]
  (hPP' : P ≤ P') (hQQ' : Q ≤ Q') (Y : P.Over Q X),
  ((CategoryTheory.MorphismProperty.Over.changeProp X hPP' hQQ').obj Y).hom = Y.hom
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.ClientCapabilities : Type
-- Mathlib.CategoryTheory.Bicategory.Product
CategoryTheory.Bicategory.prod_homCategory_id_snd : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C] (X Y : B × C)
  (X_1 : (X.1 ⟶ Y.1) × (X.2 ⟶ Y.2)), (CategoryTheory.CategoryStruct.id X_1).2 = CategoryTheory.CategoryStruct.id X_1.2
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_counitIso_inv_app_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape}
  (I : CategoryTheory.Limits.MulticospanIndex J C) [inst_1 : CategoryTheory.Limits.HasProduct I.left]
  [inst_2 : CategoryTheory.Limits.HasProduct I.right]
  (X :
    CategoryTheory.Limits.Fork
      (I.fstPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left))
        (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right)))
      (I.sndPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left))
        (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right)))),
  (I.multiforkEquivPiFork.counitIso.inv.app X).hom = CategoryTheory.CategoryStruct.id X.pt
-- Mathlib.Data.ENNReal.Inv
ENNReal.one_le_inv : ∀ {a : ENNReal}, 1 ≤ a⁻¹ ↔ a ≤ 1
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.mult.sizeOf_spec : ∀ (p : Lean.Grind.CommRing.Power) (m : Lean.Grind.CommRing.Mon),
  sizeOf (Lean.Grind.CommRing.Mon.mult p m) = 1 + sizeOf p + sizeOf m
-- Lean.Meta.Sym.SymM
/-- Runs `x` with a fresh issue context. Issues reported during `x` are
prepended to the issues that existed before the call.
 -/
Lean.Meta.Sym.withNewIssueContext : {α : Type} → Lean.Meta.Sym.SymM α → Lean.Meta.Sym.SymM α
-- Std.Sync.CancellationToken
/-- Cancelled due to a deadline or timeout
 -/
Std.CancellationReason.deadline : Std.CancellationReason
-- Mathlib.RepresentationTheory.Coinvariants
Rep.instLinearModuleCatCoinvariantsFunctor : ∀ (k : Type u) (G : Type v) [inst : CommRing k] [inst_1 : Monoid G],
  CategoryTheory.Functor.Linear k (Rep.coinvariantsFunctor k G)
-- Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv
/-- If `f` has an invertible derivative `f'` at `a` in the sense of strict differentiability `(hf)`,
then the inverse function `hf.localInverse f` has derivative `f'.symm` at `f a`.  -/
HasStrictFDerivAt.to_localInverse : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {f' : E ≃L[𝕜] F} {a : E} [inst_5 : CompleteSpace E] (hf : HasStrictFDerivAt f (↑f') a),
  HasStrictFDerivAt (HasStrictFDerivAt.localInverse f f' a hf) (↑f'.symm) (f a)
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- **Alias** of `CategoryTheory.Subobject.Classifier.isTerminalFrom_eq_χ₀`. -/
CategoryTheory.Classifier.isTerminalFrom_eq_χ₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (c : CategoryTheory.Subobject.Classifier C),
  CategoryTheory.Subobject.Classifier.isTerminalΩ₀.from = c.χ₀
-- Mathlib.CategoryTheory.Subobject.MonoOver
CategoryTheory.MonoOver.hasLimitsOfShape : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} J]
  (X : C) [CategoryTheory.Limits.HasLimitsOfShape J (CategoryTheory.Over X)],
  CategoryTheory.Limits.HasLimitsOfShape J (CategoryTheory.MonoOver X)
-- Mathlib.Algebra.Group.Basic
one_div_zpow : ∀ {α : Type u_1} [inst : DivisionMonoid α] (a : α) (n : ℤ), (1 / a) ^ n = 1 / a ^ n
-- Mathlib.Topology.EMetricSpace.Defs
/-- **Alias** of `Metric.mem_eball_comm`. -/
EMetric.mem_ball_comm : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x y : α} {ε : ENNReal}, x ∈ Metric.eball y ε ↔ y ∈ Metric.eball x ε
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.contains_eq_false_iff_not_mem : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] {k : α},
  m.contains k = false ↔ k ∉ m
-- Mathlib.Data.Sym.Basic
/-- Append a pair of `Sym` terms.  -/
Sym.append : {α : Type u_1} → {n n' : ℕ} → Sym α n → Sym α n' → Sym α (n + n')
-- Init.System.IO
/-- POSIX-style file permissions that describe access rights for a file's owner, members of its
assigned group, and all others.
 -/
IO.FileRight : Type
-- Mathlib.Algebra.Regular.SMul
/-- Two elements `a` and `b` are `M`-regular if and only if both products `a * b` and `b * a`
are `M`-regular.  -/
IsSMulRegular.mul_and_mul_iff : ∀ {R : Type u_1} {M : Type u_3} {a b : R} [inst : SMul R M] [inst_1 : Mul R] [IsScalarTower R R M],
  IsSMulRegular M (a * b) ∧ IsSMulRegular M (b * a) ↔ IsSMulRegular M a ∧ IsSMulRegular M b
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.Mor₂.brecOn.go : {motive : Mathlib.Tactic.BicategoryLike.Mor₂ → Sort u} →
  (t : Mathlib.Tactic.BicategoryLike.Mor₂) →
    ((t : Mathlib.Tactic.BicategoryLike.Mor₂) → Mathlib.Tactic.BicategoryLike.Mor₂.below t → motive t) →
      motive t ×' Mathlib.Tactic.BicategoryLike.Mor₂.below t
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.coeff_monomial : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : DecidableEq σ] (m n : σ →₀ ℕ) (a : R),
  MvPolynomial.coeff m ((MvPolynomial.monomial n) a) = if n = m then a else 0
-- Mathlib.Analysis.SpecialFunctions.SmoothTransition
/-- The function `expNegInvGlue` vanishes on `(-∞, 0]`.  -/
expNegInvGlue.zero_of_nonpos : ∀ {x : ℝ}, x ≤ 0 → expNegInvGlue x = 0
-- Mathlib.Topology.Order.Monotone
/-- An antitone function `f` sending `top` to `bot` and continuous at the infimum of a set sends
this infimum to the supremum of the image of this set.  -/
Antitone.map_sInf_of_continuousAt : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  [inst_3 : CompleteLinearOrder β] [inst_4 : TopologicalSpace β] [OrderClosedTopology β] {f : α → β} {s : Set α},
  ContinuousAt f (sInf s) → Antitone f → f ⊤ = ⊥ → f (sInf s) = sSup (f '' s)
-- Mathlib.Combinatorics.Young.YoungDiagram
/-- Young diagram from a sorted list  -/
YoungDiagram.ofRowLens : (w : List ℕ) → w.SortedGE → YoungDiagram