mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.String.toBitVec_getElem_utf8EncodeChar_zero_of_utf8Size_eq_three : ∀ {c : Char} (h : c.utf8Size = 3),
  (String.utf8EncodeChar c)[0].toBitVec = 14#4 ++ BitVec.extractLsb' 12 4 c.val.toBitVec
-- Mathlib.RingTheory.OrderOfVanishing.Basic
/-- The order of vanishing of `a * b` is the order of vanishing of `a` plus the order
of vanishing of `b`.
 -/
Ring.ord_mul : ∀ (R : Type u_1) [inst : CommRing R] {a b : R}, b ∈ nonZeroDivisors R → Ring.ord R (a * b) = Ring.ord R a + Ring.ord R b
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.zeroLEOneClass : ∀ {α : Type u} [inst : One α] [inst_1 : Zero α] [inst_2 : LE α] [ZeroLEOneClass α], ZeroLEOneClass (WithTop α)
-- Mathlib.Topology.FiberBundle.Basic
FiberPrebundle.mk : {B : Type u_2} →
  {F : Type u_3} →
    {E : B → Type u_5} →
      [inst : TopologicalSpace B] →
        [inst_1 : TopologicalSpace F] →
          [inst_2 : (x : B) → TopologicalSpace (E x)] →
            (pretrivializationAtlas : Set (Bundle.Pretrivialization F Bundle.TotalSpace.proj)) →
              (pretrivializationAt : B → Bundle.Pretrivialization F Bundle.TotalSpace.proj) →
                (∀ (x : B), x ∈ (pretrivializationAt x).baseSet) →
                  (∀ (x : B), pretrivializationAt x ∈ pretrivializationAtlas) →
                    (∀ e ∈ pretrivializationAtlas,
                        ∀ e' ∈ pretrivializationAtlas,
                          ContinuousOn (↑e ∘ ↑e'.symm) (e'.target ∩ ↑e'.symm ⁻¹' e.source)) →
                      (∀ (b : B), Topology.IsInducing (↑(pretrivializationAt b) ∘ Bundle.TotalSpace.mk b)) →
                        FiberPrebundle F E
-- Mathlib.CategoryTheory.Bicategory.Functor.Lax
/-- Lax associativity.  -/
CategoryTheory.LaxFunctor.map₂_associator_app_assoc : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] (self : CategoryTheory.LaxFunctor B CategoryTheory.Cat)
  {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (X : ↑(self.obj a)) {Z : ↑(self.obj d)}
  (h_1 :
    (self.map (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h))).toFunctor.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((self.map h).toFunctor.map ((self.mapComp f g).toNatTrans.app X))
      (CategoryTheory.CategoryStruct.comp ((self.mapComp (CategoryTheory.CategoryStruct.comp f g) h).toNatTrans.app X)
        (CategoryTheory.CategoryStruct.comp
          ((self.map₂ (CategoryTheory.Bicategory.associator f g h).hom).toNatTrans.app X) h_1)) =
    CategoryTheory.CategoryStruct.comp ((self.mapComp g h).toNatTrans.app ((self.map f).toFunctor.obj X))
      (CategoryTheory.CategoryStruct.comp ((self.mapComp f (CategoryTheory.CategoryStruct.comp g h)).toNatTrans.app X)
        h_1)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem?_erase_self : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k : α}, (m.erase k)[k]? = none
-- Mathlib.Topology.Irreducible
IsIrreducible.of_subtype : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X} [IrreducibleSpace ↑s], IsIrreducible s
-- Mathlib.Topology.VectorBundle.Basic
Bundle.Pretrivialization.symmₗ.congr_simp : ∀ (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : Semiring R] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace B] [inst_3 : AddCommMonoid F] [inst_4 : Module R F]
  [inst_5 : (x : B) → AddCommMonoid (E x)] [inst_6 : (x : B) → Module R (E x)]
  (e e_1 : Bundle.Pretrivialization F Bundle.TotalSpace.proj) (e_e : e = e_1)
  [inst_7 : Bundle.Pretrivialization.IsLinear R e] (b : B),
  Bundle.Pretrivialization.symmₗ R e b = Bundle.Pretrivialization.symmₗ R e_1 b
-- Mathlib.Topology.Order.LeftRightLim
tendsto_rightLim_atTop_of_tendsto : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace β] [inst_2 : TopologicalSpace α]
  [OrderTopology α] [T3Space β] {f : α → β} {b : β},
  Filter.Tendsto f Filter.atTop (nhds b) → Filter.Tendsto (Function.rightLim f) Filter.atTop (nhds b)
-- Lean.Meta.Tactic.Grind.Split
/-- Returns `true` if `c` is congruent to a case-split that was already performed.  -/
_private.Lean.Meta.Tactic.Grind.Split.0.Lean.Meta.Grind.isCongrToPrevSplit : Lean.Expr → Lean.Meta.Grind.GoalM Bool
-- Mathlib.Algebra.Group.Prod
AddHom.prodMap_def : ∀ {M : Type u_3} {N : Type u_4} {M' : Type u_6} {N' : Type u_7} [inst : Add M] [inst_1 : Add N] [inst_2 : Add M']
  [inst_3 : Add N'] (f : M →ₙ+ M') (g : N →ₙ+ N'),
  f.prodMap g = (f.comp (AddHom.fst M N)).prod (g.comp (AddHom.snd M N))
-- Mathlib.CategoryTheory.Countable
/-- A countable category `α` is equivalent to a *small* category with objects in `Type`.  -/
CategoryTheory.CountableCategory.HomAsType : (α : Type u) → [inst : CategoryTheory.Category.{v, u} α] → [CategoryTheory.CountableCategory α] → Type
-- Mathlib.Topology.UniformSpace.Defs
/-- A function `f : α → β` is *uniformly continuous* if `(f x, f y)` tends to the diagonal
as `(x, y)` tends to the diagonal. In other words, if `x` is sufficiently close to `y`, then
`f x` is close to `f y` no matter where `x` and `y` are located in `α`.  -/
UniformContinuous : {α : Type ua} → {β : Type ub} → [UniformSpace α] → [UniformSpace β] → (α → β) → Prop
-- Mathlib.Topology.Separation.Basic
nhdsWithin_compl_singleton_le : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T1Space X] (x y : X), nhdsWithin x {x}ᶜ ≤ nhdsWithin x {y}ᶜ
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.map_inf : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {K : Type u_3}
  [inst_3 : Field K] [inst_4 : Algebra F K] (s t : IntermediateField F E) (f : E →ₐ[F] K),
  IntermediateField.map f (s ⊓ t) = IntermediateField.map f s ⊓ IntermediateField.map f t
-- Lean.PrettyPrinter.Delaborator.Builtins
_private.Lean.PrettyPrinter.Delaborator.Builtins.0.Lean.PrettyPrinter.Delaborator.delabForallParamsWithSignature.shouldGroupWithNext : Lean.NameSet → Lean.Expr → Lean.Expr → Bool
-- Mathlib.Order.Filter.CountablyGenerated
Filter.CountableFilterBasis.mk.sizeOf_spec : ∀ {α : Type u_6} [inst : SizeOf α] (toFilterBasis : FilterBasis α) (countable : toFilterBasis.sets.Countable),
  sizeOf { toFilterBasis := toFilterBasis, countable := countable } = 1 + sizeOf toFilterBasis + sizeOf countable
-- Mathlib.Algebra.Group.Basic
ite_one_mul : ∀ {M : Type u_4} [inst : MulOneClass M] {P : Prop} [inst_1 : Decidable P] {a b : M},
  (if P then 1 else a * b) = (if P then 1 else a) * if P then 1 else b
-- Lean.CoreM
/-- Custom `try-catch` for all monads based on `CoreM`. We usually don't want to catch "runtime
exceptions" these monads, but on `CommandElabM` or, in specific cases, using `tryCatchRuntimeEx`.
See issues #2775 and #2744 as well as `MonadAlwaysExcept`. Also, we never want to catch interrupt
exceptions inside the elaborator.
 -/
Lean.Core.tryCatch : {α : Type} → Lean.CoreM α → (Lean.Exception → Lean.CoreM α) → Lean.CoreM α
-- Std.Data.HashMap.Lemmas
Std.HashMap.Equiv.congr_left : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ m₃ : Std.HashMap α β},
  m₁.Equiv m₂ → (m₁.Equiv m₃ ↔ m₂.Equiv m₃)
-- Lean.Elab.Syntax
_private.Lean.Elab.Syntax.0.Lean.Elab.Term.toParserDescr.process : Lean.Syntax → Lean.Elab.Term.ToParserDescr
-- Mathlib.MeasureTheory.Group.Prod
MeasureTheory.absolutelyContinuous_map_mul_right : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [MeasurableMul₂ G] (μ : MeasureTheory.Measure G)
  [MeasureTheory.SFinite μ] [MeasurableInv G] [μ.IsMulLeftInvariant] (g : G),
  μ.AbsolutelyContinuous (MeasureTheory.Measure.map (fun x => x * g) μ)
-- Mathlib.Algebra.Category.ModuleCat.FilteredColimits
ModuleCat.FilteredColimits.colimit_add_mk_eq : ∀ {R : Type u} [inst : Ring R] {J : Type v} [inst_1 : CategoryTheory.SmallCategory J]
  [inst_2 : CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J (ModuleCat R)) (x y : (j : J) × ↑(F.obj j))
  (k : J) (f : x.fst ⟶ k) (g : y.fst ⟶ k),
  ModuleCat.FilteredColimits.M.mk F x + ModuleCat.FilteredColimits.M.mk F y =
    ModuleCat.FilteredColimits.M.mk F
      ⟨k, (CategoryTheory.ConcreteCategory.hom (F.map f)) x.snd + (CategoryTheory.ConcreteCategory.hom (F.map g)) y.snd⟩
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.mapRange.addMonoidHom_apply : ∀ {ι : Type u} {β₁ : ι → Type v₁} {β₂ : ι → Type v₂} [inst : (i : ι) → AddZeroClass (β₁ i)]
  [inst_1 : (i : ι) → AddZeroClass (β₂ i)] (f : (i : ι) → β₁ i →+ β₂ i) (x : Π₀ (i : ι), β₁ i),
  (DFinsupp.mapRange.addMonoidHom f) x = DFinsupp.mapRange (fun i x => (f i) x) ⋯ x
-- Mathlib.Algebra.Group.Action.Defs
neg_vadd_vadd : ∀ {G : Type u_3} {α : Type u_5} [inst : AddGroup G] [inst_1 : AddAction G α] (g : G) (a : α), -g +ᵥ g +ᵥ a = a
-- Mathlib.Topology.DenseEmbedding
IsDenseEmbedding.mk : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {e : α → β},
  IsDenseInducing e → Function.Injective e → IsDenseEmbedding e
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey_maxKey? : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] [inst_2 : BEq α] [inst_3 : Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {km : α} {hc : Std.Internal.List.containsKey km l = true},
      (Std.Internal.List.maxKey? l).get ⋯ = km → Std.Internal.List.getKey km l hc = km
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toList_rco_eq_cons : ∀ {m n : ℤ}, m < n → (m...n).toList = m :: ((m + 1)...n).toList
-- Aesop.Script.Step
Aesop.Script.Step.preGoal : Aesop.Script.Step → Lean.MVarId
-- Mathlib.Tactic.FunProp.Theorems
Mathlib.Meta.FunProp.Theorem.function : Mathlib.Meta.FunProp.FunctionTheorem → Mathlib.Meta.FunProp.Theorem
-- Mathlib.MeasureTheory.Group.Prod
MeasureTheory.quasiMeasurePreserving_sub : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [MeasurableAdd₂ G] (μ ν : MeasureTheory.Measure G)
  [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] [MeasurableNeg G] [μ.IsAddLeftInvariant],
  MeasureTheory.Measure.QuasiMeasurePreserving (fun p => p.1 - p.2) (μ.prod ν) μ
-- Mathlib.Analysis.Normed.Group.Subgroup
/-- If `x` is an element of an additive subgroup `s` of a seminormed
additive group `E`, its norm in `s` is equal to its norm in `E`.  -/
AddSubgroupClass.coe_norm : ∀ {E : Type u_1} [inst : SeminormedAddGroup E] {S : Type u_2} [inst_1 : SetLike S E] [inst_2 : AddSubgroupClass S E]
  (s : S) (x : ↥s), ‖x‖ = ‖↑x‖
-- Mathlib.Order.WithBot
WithTop.nontrivial : ∀ {α : Type u_1} [Nonempty α], Nontrivial (WithTop α)
-- Mathlib.NumberTheory.Divisors
Nat.swap_mem_divisorsAntidiagonal : ∀ {n : ℕ} {x : ℕ × ℕ}, x.swap ∈ n.divisorsAntidiagonal ↔ x ∈ n.divisorsAntidiagonal
-- Mathlib.Topology.MetricSpace.PiNat
Metric.PiNatEmbed.separation : ∀ {X : Type u_3} [inst : MetricSpace X] [inst_1 : TopologicalSpace.SeparableSpace X] {x : X} {C : Set X},
  C ∈ nhds x → ∃ n, C ∈ Filter.comap (Metric.PiNatEmbed.distDenseSeq X n) (nhds (Metric.PiNatEmbed.distDenseSeq X n x))
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.foldlM_eq_foldlM_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {δ : Type w} {m : Type w → Type w'} {β : Type v}
  {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp] [inst_1 : Monad m] [inst_2 : LawfulMonad m]
  {f : δ → α → β → m δ} {init : δ},
  Std.ExtDTreeMap.foldlM f init t = List.foldlM (fun a b => f a b.1 b.2) init (Std.ExtDTreeMap.Const.toList t)
-- Mathlib.Topology.Algebra.Module.FiniteDimension
ContinuousLinearMap.toLinearMap_eq_iff_eq_toContinuousLinearMap : ∀ {𝕜 : Type u} [hnorm : NontriviallyNormedField 𝕜] {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E]
  [inst_2 : TopologicalSpace E] [inst_3 : IsTopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E]
  [inst_5 : CompleteSpace 𝕜] [inst_6 : T2Space E] [inst_7 : FiniteDimensional 𝕜 E] (g : E →L[𝕜] E) (f : E →ₗ[𝕜] E),
  ↑g = f ↔ g = LinearMap.toContinuousLinearMap f
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getD_ofList_of_mem : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} [inst : LawfulBEq α] {l : List ((a : α) × β a)}
  {k k' : α} (k_beq : (k == k') = true) {v : β k} {fallback : β k'},
  List.Pairwise (fun a b => (a.fst == b.fst) = false) l →
    ⟨k, v⟩ ∈ l → (Std.DHashMap.ofList l).getD k' fallback = cast ⋯ v
-- Mathlib.Analysis.Normed.Affine.ContinuousAffineMap
ContinuousAffineMap.instSeminormedAddCommGroup : {𝕜 : Type u_1} →
  {V : Type u_3} →
    {W : Type u_4} →
      [inst : SeminormedAddCommGroup V] →
        [inst_1 : SeminormedAddCommGroup W] →
          [inst_2 : NontriviallyNormedField 𝕜] →
            [inst_3 : NormedSpace 𝕜 V] → [inst_4 : NormedSpace 𝕜 W] → SeminormedAddCommGroup (V →ᴬ[𝕜] W)
-- Mathlib.Algebra.Polynomial.Reverse
Polynomial.reflect_zero : ∀ {R : Type u_1} [inst : Semiring R] {N : ℕ}, Polynomial.reflect N 0 = 0
-- Mathlib.RingTheory.HopfAlgebra.GroupLike
IsGroupLikeElem.isUnit : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : HopfAlgebra R A] {a : A},
  IsGroupLikeElem R a → IsUnit a
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
/-- Coercion of a `BoundedContinuousFunction` is an `AddMonoidHom`.
Similar to `AddMonoidHom.coeFn`.  -/
BoundedContinuousFunction.coeFnAddMonoidHom : {α : Type u} →
  {R : Type u_2} →
    [inst : TopologicalSpace α] →
      [inst_1 : PseudoMetricSpace R] →
        [inst_2 : AddMonoid R] →
          [inst_3 : BoundedAdd R] → [inst_4 : ContinuousAdd R] → BoundedContinuousFunction α R →+ α → R
-- Std.Data.Iterators.Lemmas.Combinators.Zip
Std.Iter.step_intermediateZip : ∀ {α₁ α₂ β₁ β₂ : Type w} [inst : Std.Iterator α₁ Id β₁] [inst_1 : Std.Iterator α₂ Id β₂] {it₁ : Std.Iter β₁}
  {memo : Option { out // ∃ it, it.toIterM.IsPlausibleOutput out }} {it₂ : Std.Iter β₂},
  (Std.Iter.Intermediate.zip it₁ memo it₂).step =
    match memo with
    | none =>
      match it₁.step with
      | ⟨Std.IterStep.yield it₁' out, hp⟩ =>
        Std.PlausibleIterStep.skip (Std.Iter.Intermediate.zip it₁' (some ⟨out, ⋯⟩) it₂) ⋯
      | ⟨Std.IterStep.skip it₁', hp⟩ => Std.PlausibleIterStep.skip (Std.Iter.Intermediate.zip it₁' none it₂) ⋯
      | ⟨Std.IterStep.done, hp⟩ => Std.PlausibleIterStep.done ⋯
    | some out₁ =>
      match it₂.step with
      | ⟨Std.IterStep.yield it₂' out₂, hp⟩ =>
        Std.PlausibleIterStep.yield (Std.Iter.Intermediate.zip it₁ none it₂') (↑out₁, out₂) ⋯
      | ⟨Std.IterStep.skip it₂', hp⟩ => Std.PlausibleIterStep.skip (Std.Iter.Intermediate.zip it₁ (some out₁) it₂') ⋯
      | ⟨Std.IterStep.done, hp⟩ => Std.PlausibleIterStep.done ⋯
-- Lean.Parser.Extension
Lean.Parser.mkParserState : String → Lean.Parser.ParserState
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Relations.Solution.IsPresentationCore.isPresentation : ∀ {A : Type u} [inst : Ring A] {relations : Module.Relations A} {M : Type v} [inst_1 : AddCommGroup M]
  [inst_2 : Module A M] {solution : relations.Solution M} (h : solution.IsPresentationCore), solution.IsPresentation
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.DayFunctor
CategoryTheory.MonoidalCategory.DayFunctor.Hom.mk.injEq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  {F G : CategoryTheory.MonoidalCategory.DayFunctor C V} (natTrans natTrans_1 : F.functor ⟶ G.functor),
  ({ natTrans := natTrans } = { natTrans := natTrans_1 }) = (natTrans = natTrans_1)
-- Mathlib.RingTheory.FiniteType
Algebra.FiniteType.prod : ∀ {R : Type uR} {A : Type uA} {B : Type uB} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] [hA : Algebra.FiniteType R A] [hB : Algebra.FiniteType R B],
  Algebra.FiniteType R (A × B)
-- Lean.Data.Lsp.CodeActions
Lean.Lsp.instFromJsonCodeActionTriggerKind : Lean.FromJson Lean.Lsp.CodeActionTriggerKind
-- Mathlib.Analysis.Normed.Group.AddTorsor
IsometryEquiv.constVSub_symm_apply : ∀ {V : Type u_2} {P : Type u_3} [inst : SeminormedAddCommGroup V] [inst_1 : PseudoMetricSpace P]
  [inst_2 : NormedAddTorsor V P] (x : P) (x_1 : V), (IsometryEquiv.constVSub x).symm x_1 = -x_1 +ᵥ x
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.norm_toLp_snd : ∀ (p : ENNReal) (α : Type u_2) (β : Type u_3) [hp : Fact (1 ≤ p)] [inst : SeminormedAddCommGroup α]
  [inst_1 : SeminormedAddCommGroup β] (y : β), ‖WithLp.toLp p (0, y)‖ = ‖y‖
-- Mathlib.Computability.AkraBazzi.SumTransform
AkraBazziRecurrence.eventually_one_sub_smoothingFn_gt_const_real : ∀ c < 1, ∀ᶠ (x : ℝ) in Filter.atTop, c < 1 - AkraBazziRecurrence.smoothingFn x
-- Mathlib.NumberTheory.Height.Projectivization
Height.logHeight.eq_1 : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] {ι : Type u_2} (x : ι → K),
  Height.logHeight x = Real.log (Height.mulHeight x)
-- Mathlib.CategoryTheory.Triangulated.Subcategory
/-- Given `P : ObjectProperty C` with `C` a pretriangulated category, this
is the property that whenever `X₁ ⟶ X₂ ⟶ X₃ ⟶ X₁⟦1⟧` is a distinguished triangle
such that `P X₂` and `P X₃` hold, then `P.isoClosure X₁` holds.  -/
CategoryTheory.ObjectProperty.IsTriangulatedClosed₁ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
      [inst_2 : CategoryTheory.HasShift C ℤ] →
        [inst_3 : CategoryTheory.Preadditive C] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [CategoryTheory.Pretriangulated C] → CategoryTheory.ObjectProperty C → Prop
-- Mathlib.Topology.EMetricSpace.Diam
/-- **Alias** of `Metric.ediam`.

---

The diameter of a set in a pseudoemetric space as an extended nonnegative real number.  -/
EMetric.diam : {X : Type u_2} → [PseudoEMetricSpace X] → Set X → ENNReal
-- Mathlib.Probability.Density
MeasureTheory.HasPDF.absolutelyContinuous' : ∀ {Ω : Type u_1} {E : Type u_2} {inst : MeasurableSpace E} {m : MeasurableSpace Ω} {X : Ω → E}
  {ℙ : MeasureTheory.Measure Ω} {μ : autoParam (MeasureTheory.Measure E) MeasureTheory.HasPDF._auto_1}
  [self : MeasureTheory.HasPDF X ℙ μ], (MeasureTheory.Measure.map X ℙ).AbsolutelyContinuous μ
-- Mathlib.Computability.Primrec.Basic
Primrec.nat_min : Primrec₂ min
-- Mathlib.Data.QPF.Multivariate.Basic
MvQPF.mem_supp : ∀ {n : ℕ} {F : TypeVec.{u} n → Type u_1} [q : MvQPF F] {α : TypeVec.{u} n} (x : F α) (i : Fin2 n) (u : α i),
  u ∈ MvFunctor.supp x i ↔
    ∀ (a : (MvQPF.P F).A) (f : ((MvQPF.P F).B a).Arrow α), MvQPF.abs ⟨a, f⟩ = x → u ∈ f i '' Set.univ
-- Mathlib.Combinatorics.SimpleGraph.Hasse
SimpleGraph.pathGraph_adj : ∀ {n : ℕ} {u v : Fin n}, (SimpleGraph.pathGraph n).Adj u v ↔ ↑u + 1 = ↑v ∨ ↑v + 1 = ↑u
-- Std.Data.TreeMap.Basic
/-- Tries to retrieve the key-value pair with the smallest key that is greater than or equal to the
given key, returning `fallback` if no such pair exists.
 -/
Std.TreeMap.getEntryGED : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap α β cmp → α → α × β → α × β
-- Mathlib.Data.Semiquot
Semiquot.map_def : ∀ {α β : Type u_1}, (fun x1 x2 => x1 <$> x2) = Semiquot.map
-- Std.Data.Iterators.Lemmas.Producers.Monadic.Empty
Std.IterM.foldM_empty : ∀ {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} {β γ : Type u_1} [inst : Monad m] [LawfulMonad m]
  [inst_2 : Monad n] [LawfulMonad n] [inst_4 : MonadLiftT m n] [LawfulMonadLiftT m n] {init : γ} {f : γ → β → n γ},
  Std.IterM.foldM f init (Std.IterM.empty m β) = pure init
-- Mathlib.RingTheory.Conductor
conductor_eq_top_iff_adjoin_eq_top : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {x : S},
  conductor R x = ⊤ ↔ R[x] = ⊤
-- Mathlib.ModelTheory.Basic
Equiv.toFun_inducedStructureEquiv : ∀ {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [inst : L.Structure M] (e : M ≃ N),
  ⇑e.inducedStructureEquiv = ⇑e
-- Batteries.Data.Array.Scan
Array.scanlM_extract : ∀ {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} {start stop : ℕ} {init : β} [inst : Monad m] [LawfulMonad m]
  {f : β → α → m β} {as : Array α}, Array.scanlM f init (as.extract start stop) = Array.scanlM f init as start stop
-- Mathlib.Algebra.Category.Grp.Limits
AddGrpCat.sectionsAddGroup.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddGrpCat),
  AddGrpCat.sectionsAddGroup F = (AddGrpCat.sectionsAddSubgroup F).toAddGroup
-- Mathlib.Topology.Path
Path.add.eq_1 : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : Add X] [inst_2 : ContinuousAdd X] {a₁ b₁ a₂ b₂ : X}
  (γ₁ : Path a₁ b₁) (γ₂ : Path a₂ b₂), γ₁.add γ₂ = (γ₁.prod γ₂).map ⋯
-- Init.MetaTypes
Lean.Meta.instInhabitedEtaStructMode.default : Lean.Meta.EtaStructMode
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.instModuleOfSMulCommClass : {S : Type u_1} →
  {R : Type u_3} →
    {M : Type u_4} →
      {N : Type u_5} →
        [inst : CommSemiring R] →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommMonoid N] →
                [inst_4 : Module R N] →
                  [inst_5 : Semiring S] → [inst_6 : Module S N] → [SMulCommClass S R N] → Module S (QuadraticMap R M N)
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.testAgainstNN_mono : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] (μ : MeasureTheory.FiniteMeasure Ω)
  {f g : BoundedContinuousFunction Ω NNReal}, ⇑f ≤ ⇑g → μ.testAgainstNN f ≤ μ.testAgainstNN g
-- Mathlib.RingTheory.Bialgebra.GroupLike
GroupLike.instMonoid : {R : Type u_1} →
  {A : Type u_2} → [inst : CommSemiring R] → [inst_1 : Semiring A] → [inst_2 : Bialgebra R A] → Monoid (GroupLike R A)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
addRightStrictMono_of_addLeftStrictMono : ∀ (N : Type u_2) [inst : AddCommSemigroup N] [inst_1 : LT N] [AddLeftStrictMono N], AddRightStrictMono N
-- Aesop.Util.Tactic.Unfold
Aesop.tacticAesop_unfold_At_ : Lean.ParserDescr
-- Init.Data.String.Lemmas.IsEmpty
String.Slice.copy_ne_empty_iff : ∀ {s : String.Slice}, s.copy ≠ "" ↔ s.isEmpty = false
-- Init.Data.Array.Lemmas
Array.prod_reverse : ∀ {α : Type u_1} [inst : One α] [inst_1 : Mul α] [Std.Associative fun x1 x2 => x1 * x2]
  [Std.Commutative fun x1 x2 => x1 * x2] [Std.LawfulLeftIdentity (fun x1 x2 => x1 * x2) 1] (xs : Array α),
  xs.reverse.prod = xs.prod
-- Mathlib.MeasureTheory.Measure.Map
MeasurableEmbedding.map_injective : ∀ {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} {m1 : MeasurableSpace β} {f : α → β},
  MeasurableEmbedding f → Function.Injective (MeasureTheory.Measure.map f)
-- Mathlib.Logic.Basic
exists_apply_eq_apply2' : ∀ {α : Sort u_3} {β : Sort u_4} {γ : Sort u_5} {f : α → β → γ} {a : α} {b : β}, ∃ x y, f a b = f x y
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.instIsOrderedMonoid : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : CommMonoid β] [inst_2 : Preorder β]
  [IsOrderedMonoid β], IsOrderedMonoid (MeasureTheory.SimpleFunc α β)
-- Mathlib.Order.RelClasses
WellFoundedRelation.asymmetric₃ : ∀ {α : Sort u_1} [inst : WellFoundedRelation α] {a b c : α},
  WellFoundedRelation.rel a b → WellFoundedRelation.rel b c → ¬WellFoundedRelation.rel c a
-- Std.Data.HashMap.Lemmas
Std.HashMap.Equiv.insertMany_list : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  (l : List (α × β)), m₁.Equiv m₂ → (m₁.insertMany l).Equiv (m₂.insertMany l)
-- Mathlib.CategoryTheory.Limits.Types.Yoneda
CategoryTheory.Limits.opCompYonedaSectionsEquiv_symm_apply_coe : ∀ {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] (F : CategoryTheory.Functor J C) (X : C)
  (τ : F ⟶ (CategoryTheory.Functor.const J).obj X) (j : Jᵒᵖ),
  ↑((CategoryTheory.Limits.opCompYonedaSectionsEquiv F X).symm τ) j = τ.app (Opposite.unop j)
-- Lean.Elab.Do.Basic
Lean.Elab.Do.ReturnCont.mk.sizeOf_spec : ∀ (resultType : Lean.Expr) (k : Lean.Expr → Lean.Elab.Do.DoElabM Lean.Expr),
  sizeOf { resultType := resultType, k := k } = 1 + sizeOf resultType
-- Mathlib.FieldTheory.Separable
Polynomial.separable_gcd_left : ∀ {F : Type u_1} [inst : Field F] [inst_1 : DecidableEq (Polynomial F)] {f : Polynomial F},
  f.Separable → ∀ (g : Polynomial F), (EuclideanDomain.gcd f g).Separable