mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
SSet.Subcomplex.Pairing.RankFunction.Cell.ι_b_app : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [inst : LinearOrder ι] {f : P.RankFunction ι}
  [inst_1 : P.IsProper] [inst_2 : SuccOrder ι] [inst_3 : NoMaxOrder ι] {j : ι} (c : f.Cell j) (x : SimplexCategoryᵒᵖ),
  CategoryTheory.CategoryStruct.comp (c.ιSigmaStdSimplex.app x) ((f.b j).app x) = c.mapToSucc.app x
-- Mathlib.Algebra.Order.Interval.Set.Group
Set.neg_mem_Icc_iff : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] {a c d : α},
  -a ∈ Set.Icc c d ↔ a ∈ Set.Icc (-d) (-c)
-- Lean.Parser.Command
Lean.Parser.Command.structFields.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Init.Data.UInt.Lemmas
UInt16.toNat_mod_uInt32Size : ∀ (n : UInt16), n.toNat % UInt32.size = n.toNat
-- Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
NumberField.InfinitePlace.Completion.ofCompletion_surjective : ∀ {K : Type u_1} [inst : Field K] (v : NumberField.InfinitePlace K),
  Function.Surjective NumberField.InfinitePlace.Completion.ofCompletion
-- Mathlib.Algebra.Group.Subgroup.Defs
/-- An additive subgroup of an `AddCommGroup` is an `AddCommGroup`.  -/
AddSubgroupClass.toAddCommGroup : {S : Type u_4} →
  (H : S) → {G : Type u_5} → [inst : AddCommGroup G] → [inst_1 : SetLike S G] → [AddSubgroupClass S G] → AddCommGroup ↥H
-- Mathlib.Order.Filter.Germ.Basic
/-- If `f : α → β` is constant w.r.t. `l` and `g : β → γ`, then `g ∘ f : α → γ` also is.  -/
Filter.Germ.isConstant_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : Filter α} {f : α → β} {g : β → γ},
  (↑f).IsConstant → (↑(g ∘ f)).IsConstant
-- Init.Data.Order.Lemmas
Std.min_self : ∀ {α : Type u} [inst : Min α] [Std.IdempotentOp min] {a : α}, a ⊓ a = a
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey?_insertIfNew_of_isEmpty : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF)
  {k : α} {v : β k}, t.isEmpty = true → (Std.DTreeMap.Internal.Impl.insertIfNew k v t ⋯).impl.minKey? = some k
-- Lean.Compiler.LCNF.Types
/-- Return true iff `e : Prop` or `e : As → Prop`.
 -/
Lean.Compiler.LCNF.isPropFormer : Lean.Expr → Lean.MetaM Bool
-- Mathlib.Algebra.Algebra.Subalgebra.Unitization
NonUnitalSubring.unitization_range : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : SetLike S R] [hSR : NonUnitalSubringClass S R] (s : S),
  (NonUnitalSubring.unitization s).range = subalgebraOfSubring (Subring.closure ↑s)
-- Mathlib.Algebra.Ring.Subring.Basic
/-- The subring generated by a set includes the set.  -/
Subring.subset_closure : ∀ {R : Type u} [inst : NonAssocRing R] {s : Set R}, s ⊆ ↑(Subring.closure s)
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Ideal.homogeneousCore'_mono : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : Semiring A] [inst_1 : SetLike σ A] (𝒜 : ι → σ),
  Monotone (Ideal.homogeneousCore' 𝒜)
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2.Stmt.peek.inj : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} {k : K} {a : σ → Option (Γ k) → σ}
  {a_1 : Turing.TM2.Stmt Γ Λ σ} {k_1 : K} {a_2 : σ → Option (Γ k_1) → σ} {a_3 : Turing.TM2.Stmt Γ Λ σ},
  Turing.TM2.Stmt.peek k a a_1 = Turing.TM2.Stmt.peek k_1 a_2 a_3 → k = k_1 ∧ a ≍ a_2 ∧ a_1 = a_3
-- Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverseObj_π_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasProducts C] {X : TopCat}
  (F : TopCat.Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X)
  (c : CategoryTheory.Limits.Cone (TopCat.Presheaf.SheafConditionEqualizerProducts.diagram F U))
  (x : (CategoryTheory.Pairwise ι)ᵒᵖ),
  (TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverseObj F U c).π.app x =
    Opposite.rec
      (fun x =>
        CategoryTheory.Pairwise.casesOn x
          (fun i =>
            CategoryTheory.CategoryStruct.comp (c.π.app CategoryTheory.Limits.WalkingParallelPair.zero)
              (CategoryTheory.Limits.Pi.π (fun i => F.obj (Opposite.op (U i))) i))
          fun i j =>
          CategoryTheory.CategoryStruct.comp (c.π.app CategoryTheory.Limits.WalkingParallelPair.one)
            (CategoryTheory.Limits.Pi.π (fun p => F.obj (Opposite.op (U p.1 ⊓ U p.2))) (i, j)))
      x
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.UInt
UInt64.reduceOfNat : Lean.Meta.Simp.DSimproc
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.Λ'.succ.sizeOf_spec : ∀ (q : Turing.PartrecToTM2.Λ'), sizeOf q.succ = 1 + sizeOf q
-- Lean.ToExpr
Lean.instToExprPreresolved : Lean.ToExpr Lean.Syntax.Preresolved
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHom_comp_assoc : ∀ {C : Type u_1} {D : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} C}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} D} {inst_2 : CategoryTheory.MonoidalCategory C}
  [self : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] {c c' c'' : C} {d d' d'' : D} (f₁ : c ⟶ c')
  (f₂ : c' ⟶ c'') (g₁ : d ⟶ d') (g₂ : d' ⟶ d'') {Z : D}
  (h : CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj c'' d'' ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHom (CategoryTheory.CategoryStruct.comp f₁ f₂)
        (CategoryTheory.CategoryStruct.comp g₁ g₂))
      h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHom f₁ g₁)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHom f₂ g₂) h)
-- Mathlib.Data.Fintype.Fin
Fin.card_filter_univ_eq_vector_get_eq_count : ∀ {α : Type u_1} {n : ℕ} [inst : DecidableEq α] (a : α) (v : List.Vector α n),
  {i | v.get i = a}.card = List.count a v.toList
-- Mathlib.CategoryTheory.Monoidal.Opposite.Mon
MonObj.mopEquiv_functor_obj_mon_one_unmop : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (M : CategoryTheory.Mon C), CategoryTheory.MonObj.one.unmop = CategoryTheory.MonObj.one
-- Mathlib.Combinatorics.HalesJewett
/-- The underlying multiset of almost monochromatic lines of a color-focused collection.  -/
Combinatorics.Line.ColorFocused.lines : {α : Type u_5} →
  {ι : Type u_6} →
    {κ : Type u_7} →
      {C : (ι → Option α) → κ} → Combinatorics.Line.ColorFocused C → Multiset (Combinatorics.Line.AlmostMono C)
-- Mathlib.SetTheory.Descriptive.Tree
/-- The residual tree obtained by regarding the node x as new root  -/
Descriptive.Tree.subAt : {A : Type u_1} → ↥(Descriptive.tree A) → List A → ↥(Descriptive.tree A)
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.characteristic_inf : ∀ {G : Type u_1} [inst : AddGroup G] {H K : AddSubgroup G} [H.Characteristic] [K.Characteristic], (H ⊓ K).Characteristic
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.whiskerLeft_hom_inv : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) {g h : b ⟶ c} (η : g ≅ h),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f η.hom)
      (CategoryTheory.Bicategory.whiskerLeft f η.inv) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.comp f g)
-- Init.Data.Rat.Lemmas
Rat.mul_neg_iff_of_pos_right : ∀ {a b : ℚ}, 0 < b → (a * b < 0 ↔ a < 0)
-- Mathlib.Algebra.DirectSum.Ring
DirectSum.instMul : {ι : Type u_1} →
  [DecidableEq ι] →
    (A : ι → Type u_2) →
      [inst : Add ι] →
        [inst_1 : (i : ι) → AddCommMonoid (A i)] →
          [DirectSum.GNonUnitalNonAssocSemiring A] → Mul (DirectSum ι fun i => A i)
-- Mathlib.Control.Functor
Functor.Const.functor : {γ : Type u_1} → Functor (Functor.Const γ)
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2to1.Λ'.go.inj : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} {k : K} {a : Turing.TM2to1.StAct K Γ σ k}
  {a_1 : Turing.TM2.Stmt Γ Λ σ} {k_1 : K} {a_2 : Turing.TM2to1.StAct K Γ σ k_1} {a_3 : Turing.TM2.Stmt Γ Λ σ},
  Turing.TM2to1.Λ'.go k a a_1 = Turing.TM2to1.Λ'.go k_1 a_2 a_3 → k = k_1 ∧ a ≍ a_2 ∧ a_1 = a_3
-- Mathlib.Analysis.Convex.Function
/-- Strict concavity of functions  -/
StrictConcaveOn : (𝕜 : Type u_1) →
  {E : Type u_2} →
    {β : Type u_5} →
      [Semiring 𝕜] →
        [PartialOrder 𝕜] →
          [AddCommMonoid E] → [AddCommMonoid β] → [PartialOrder β] → [SMul 𝕜 E] → [SMul 𝕜 β] → Set E → (E → β) → Prop
-- Mathlib.Logic.Equiv.Prod
Equiv.sigmaPUnit_apply : ∀ (α : Type u_9) (p : (_ : α) × PUnit.{u_10 + 1}), (Equiv.sigmaPUnit α) p = p.fst
-- Init.Prelude
_private.Init.Prelude.0.Lean.extractImported : List Lean.MacroScope → Lean.Name → Lean.Name → List Lean.Name → Lean.MacroScopesView
-- Mathlib.Topology.DenseEmbedding
IsDenseInducing.continuous : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {i : α → β},
  IsDenseInducing i → Continuous i
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.mem_insertMany_list : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : BEq α] [Std.LawfulBEqCmp cmp],
  t.WF → ∀ {l : List ((a : α) × β a)} {k : α}, k ∈ t.insertMany l ↔ k ∈ t ∨ (List.map Sigma.fst l).contains k = true
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.minKey?_eq_some_iff_getKey?_eq_self_and_forall : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {km : α}, t.minKey? = some km ↔ t.getKey? km = some km ∧ ∀ k ∈ t, (cmp km k).isLE = true
-- Batteries.Tactic.HelpCmd
_private.Batteries.Tactic.HelpCmd.0.Batteries.Tactic.tokensToList : Lean.Parser.FirstTokens → List String
-- Lean.Server.FileWorker.SignatureHelp
Lean.Server.FileWorker.SignatureHelp.SearchControl : Type
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get!_inter_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : LawfulBEq α]
  {k : α} [inst_1 : Inhabited (β k)], k ∉ m₂ → (m₁ ∩ m₂).get! k = default
-- Mathlib.Topology.Sets.VietorisTopology
/-- The topology of `NonemptyCompacts α` has a basis consisting of sets of the form
`{s | s ⊆ U₁ ∪ … ∪ Uₙ, s ∩ U₁ ≠ ∅, …, s ∩ Uₙ ≠ ∅}`, where `U₁, …, Uₙ` are open sets and `n > 0`.

See also `TopologicalSpace.IsTopologicalBasis.nonemptyCompacts` for a variant where the sets `Uᵢ`
are chosen from some basis.  -/
TopologicalSpace.NonemptyCompacts.isTopologicalBasis : ∀ {α : Type u_1} [inst : TopologicalSpace α],
  TopologicalSpace.IsTopologicalBasis
    ((fun u => {K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty}) '' {u | u.Finite ∧ u.Nonempty ∧ ∀ U ∈ u, IsOpen U})
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Over
CategoryTheory.ChosenPullbacksAlong.Over.leftUnitor_hom_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.ChosenPullbacks C] {X : C}
  (Z : CategoryTheory.Over X),
  CategoryTheory.Over.Hom.left (CategoryTheory.MonoidalCategoryStruct.leftUnitor Z).hom =
    CategoryTheory.ChosenPullbacksAlong.snd
      (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over X)).hom Z.hom
-- Mathlib.Data.Fin.Tuple.Basic
Fin.repeat_add : ∀ {n : ℕ} {α : Sort u_1} (a : Fin n → α) (m₁ m₂ : ℕ),
  Fin.repeat (m₁ + m₂) a = Fin.append (Fin.repeat m₁ a) (Fin.repeat m₂ a) ∘ Fin.cast ⋯
-- Mathlib.Algebra.Star.Prod
Prod.instStarModule : ∀ {R : Type u} {S : Type v} {α : Type w} [inst : SMul α R] [inst_1 : SMul α S] [inst_2 : Star α] [inst_3 : Star R]
  [inst_4 : Star S] [StarModule α R] [StarModule α S], StarModule α (R × S)
-- Mathlib.Order.Hom.Basic
/-- To show that `f : α →o β` and `g : β →o α` make up an order isomorphism it is enough to show
that `g` is the inverse of `f`.  -/
OrderIso.ofHomInv : {α : Type u_2} →
  {β : Type u_3} →
    [inst : Preorder α] →
      [inst_1 : Preorder β] → (f : α →o β) → (g : β →o α) → f.comp g = OrderHom.id → g.comp f = OrderHom.id → α ≃o β
-- Init.Data.Range.Polymorphic.PRange
Std.Rcc.mk.injEq : ∀ {α : Type u} (lower upper lower_1 upper_1 : α),
  ((lower...=upper) = lower_1...=upper_1) = (lower = lower_1 ∧ upper = upper_1)
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.sum_le_univ_sum_of_nonneg : ∀ {ι : Type u_1} {N : Type u_5} [inst : AddCommMonoid N] [inst_1 : Preorder N] {f : ι → N} [AddLeftMono N]
  [inst_3 : Fintype ι] {s : Finset ι}, (∀ (x : ι), 0 ≤ f x) → ∑ x ∈ s, f x ≤ ∑ x, f x
-- Lean.Elab.Tactic.Omega.Core
/-- The number of variables in the problem.  -/
Lean.Elab.Tactic.Omega.Problem.numVars : Lean.Elab.Tactic.Omega.Problem → ℕ
-- Mathlib.FieldTheory.Galois.GaloisClosure
FiniteGaloisIntermediateField.instCoeSortType : (k : Type u_1) →
  (K : Type u_2) →
    [inst : Field k] →
      [inst_1 : Field K] → [inst_2 : Algebra k K] → CoeSort (FiniteGaloisIntermediateField k K) (Type u_2)
-- Mathlib.CategoryTheory.Shift.Adjunction
/-- Constructor for `Adjunction.CommShift`.  -/
CategoryTheory.Adjunction.CommShift.mk' : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  (adj : F ⊣ G) (A : Type u_3) [inst_2 : AddMonoid A] [inst_3 : CategoryTheory.HasShift C A]
  [inst_4 : CategoryTheory.HasShift D A] [inst_5 : F.CommShift A] [inst_6 : G.CommShift A],
  CategoryTheory.NatTrans.CommShift adj.unit A → adj.CommShift A
-- Lean.PrettyPrinter.Delaborator.Builtins
Lean.PrettyPrinter.Delaborator.delabCond : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_leftUnitor : ∀ {C : Type u_1} {D : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} C}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} D} {inst_2 : CategoryTheory.MonoidalCategory C}
  [self : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] (c : C) (d : D),
  CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight d
      (CategoryTheory.MonoidalCategoryStruct.leftUnitor c).hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso d
          (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) c).hom
      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft
        (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso d).hom c)
-- Mathlib.AlgebraicTopology.SimplicialSet.Op
/-- The covariant involution of the category of simplicial sets that
is induced by `SimplexCategory.rev : SimplexCategory ⥤ SimplexCategory`.
This functor is purposely not made `implicit_reducible` so as to avoid
confusion between `X.op _⦋n⦌` and `X _⦋n⦌`: use the bijection `opObjEquiv`.  -/
SSet.opFunctor : CategoryTheory.Functor SSet SSet
-- Lean.Meta.Tactic.Grind.ForallProp
Lean.Meta.Grind.propagateForallPropDown : Lean.Expr → Lean.Meta.Grind.GoalM Unit
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.rpow_ofNNReal : ∀ {M : NNReal} {P : ℝ}, 0 ≤ P → ↑M ^ P = ↑(M ^ P)
-- Mathlib.Algebra.Group.Action.Basic
smul_pow' : ∀ {M : Type u_2} {A : Type u_3} [inst : Monoid M] [inst_1 : Monoid A] [inst_2 : MulDistribMulAction M A] (r : M) (x : A)
  (n : ℕ), r • x ^ n = (r • x) ^ n
-- Init.Data.Array.Find
Array.idxOf?_empty : ∀ {α : Type u_1} {a : α} [inst : BEq α], #[].idxOf? a = none
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Under.map_map_right : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X Y : T} {f : X ⟶ Y} {U V : CategoryTheory.Under Y}
  {g : U ⟶ V}, CategoryTheory.Under.Hom.right ((CategoryTheory.Under.map f).map g) = CategoryTheory.Under.Hom.right g
-- Mathlib.Topology.ApproximateUnit
Filter.IsApproximateUnit.mk : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : Mul α] {l : Filter α},
  (∀ (m : α), Filter.Tendsto (fun x => m * x) l (nhds m)) →
    (∀ (m : α), Filter.Tendsto (fun x => x * m) l (nhds m)) → ∀ [neBot : l.NeBot], l.IsApproximateUnit
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.Augmented.drop_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (X :
    CategoryTheory.Comma (CategoryTheory.Functor.id (CategoryTheory.SimplicialObject C))
      (CategoryTheory.SimplicialObject.const C)),
  CategoryTheory.SimplicialObject.Augmented.drop.obj X = X.left
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.isRegular_X_pow : ∀ {R : Type u} {σ : Type u_1} {n : σ} [inst : CommSemiring R] (k : ℕ), IsRegular (MvPolynomial.X n ^ k)
-- Mathlib.Algebra.Homology.Embedding.Basic
ComplexShape.Embedding.f_eq_of_r_eq_some : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') {i : ι} {i' : ι'},
  e.r i' = some i → e.f i = i'
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.lt_of_tendsto_atTop : ∀ {x : ℝ*} (r : ℝ), Filter.Germ.Tendsto x Filter.atTop → ↑r < x
-- Mathlib.CategoryTheory.Monad.Products
CategoryTheory.algebraEquivUnder_unitIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C) [inst_1 : CategoryTheory.Limits.HasBinaryCoproducts C],
  (CategoryTheory.algebraEquivUnder X).unitIso =
    CategoryTheory.NatIso.ofComponents
      (fun A =>
        CategoryTheory.Monad.Algebra.isoMk
          (CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.coprodMonad X).Algebra).obj A).A) ⋯)
      ⋯
-- Mathlib.Data.List.Chain
List.isChain_iff : ∀ {α : Type u_1} (R : α → α → Prop) (a : List α),
  List.IsChain R a ↔ a = [] ∨ (∃ a_1, a = [a_1]) ∨ ∃ a_1 b l, R a_1 b ∧ List.IsChain R (b :: l) ∧ a = a_1 :: b :: l
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.mul_pow : ∀ {R : Type u_1} [inst : CommSemiring R] {a₂ c₂ : R} {ea₁ b c₁ : ℕ} {xa₁ : R},
  ea₁ * b = c₁ → a₂ ^ b = c₂ → (xa₁ ^ ea₁ * a₂) ^ b = xa₁ ^ c₁ * c₂
-- Mathlib.Geometry.Manifold.Instances.Real
iccLeftChart_extend_zero : ∀ {x y : ℝ} [hxy : Fact (x < y)] {p : ↑(Set.Icc x y)},
  (↑((IccLeftChart x y).extend (modelWithCornersEuclideanHalfSpace 1)) p).ofLp 0 = ↑p - x
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
AddLECancellable.withBot : ∀ {α : Type u} [inst : Add α] {a : α} [inst_1 : LE α], AddLECancellable a → AddLECancellable ↑a
-- Init.Data.String.Slice
/-- Removes the specified number of characters \(Unicode code points\) from the end of the slice.

If `n` is greater than the amount of characters in `s`, returns an empty slice.

Examples:

* `"red green blue".toSlice.dropEnd 5 == "red green".toSlice`

* `"red green blue".toSlice.dropEnd 11 == "red".toSlice`

* `"red green blue".toSlice.dropEnd 50 == "".toSlice`
 -/
String.Slice.dropEnd : String.Slice → ℕ → String.Slice
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.get_insertMany_list_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {l : List α} {k : α} (mem : k ∈ m) {h : k ∈ m.insertMany l}, (m.insertMany l).get k h = m.get k mem
-- Mathlib.Algebra.Order.ToIntervalMod
toIocMod_sub_intCast_mul : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedAddMonoid R]
  [inst_3 : Archimedean R] {p : R} (hp : 0 < p) (a b : R) (m : ℤ), toIocMod hp a (b - ↑m * p) = toIocMod hp a b
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.RightHomologyMapData.neg_φQ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData}
  (γ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂), γ.neg.φQ = -γ.φQ
-- Std.Data.TreeMap.Lemmas
_private.Std.Data.TreeMap.Lemmas.0.Std.TreeMap.ext : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t t' : Std.TreeMap α β cmp}, t.inner = t'.inner → t = t'
-- Mathlib.Combinatorics.Matroid.Minor.Delete
Matroid.indep_iff_delete_of_disjoint : ∀ {α : Type u_1} {M : Matroid α} {I D : Set α}, Disjoint I D → (M.Indep I ↔ (M.delete D).Indep I)
-- Mathlib.LinearAlgebra.AffineSpace.Midpoint
midpoint.eq_1 : ∀ (R : Type u_1) {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : Invertible 2] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] (x y : P), midpoint R x y = (AffineMap.lineMap x y) ⅟2
-- Mathlib.Order.CompleteBooleanAlgebra
iSup_disjoint_iff : ∀ {α : Type u} {ι : Sort w} [inst : Order.Frame α] {a : α} {f : ι → α},
  Disjoint (⨆ i, f i) a ↔ ∀ (i : ι), Disjoint (f i) a
-- Mathlib.Algebra.Order.Floor.Ring
Int.ceil_lt_mul : ∀ {k : Type u_4} [inst : Field k] [inst_1 : LinearOrder k] [IsOrderedRing k] [inst_3 : FloorRing k] {a b : k},
  1 < b → ↑⌈(b - 1)⁻¹⌉ / b < a → ↑⌈a⌉ < b * a
-- Mathlib.CategoryTheory.Abelian.Projective.Dimension
CategoryTheory.projectiveDimension.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] (X : C),
  CategoryTheory.projectiveDimension X = sInf {n | ∀ (i : ℕ), n < ↑i → CategoryTheory.HasProjectiveDimensionLT X i}
-- Mathlib.Analysis.BoxIntegral.Basic
BoxIntegral.integral_smul : ∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {I : BoxIntegral.Box ι} [inst_4 : Fintype ι]
  {l : BoxIntegral.IntegrationParams} {f : (ι → ℝ) → E} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤} (c : ℝ),
  BoxIntegral.integral I l (fun x => c • f x) vol = c • BoxIntegral.integral I l f vol
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- The morphism `S₁.opcycles ⟶ S₂.opcycles` induced by a morphism `S₁ ⟶ S₂` of short complexes.  -/
CategoryTheory.ShortComplex.opcyclesMap : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        [inst_2 : S₁.HasRightHomology] → [inst_3 : S₂.HasRightHomology] → (S₁ ⟶ S₂) → (S₁.opcycles ⟶ S₂.opcycles)
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
/-- Transport a non-unital subalgebra via an algebra homomorphism.  -/
NonUnitalSubalgebra.map : {F : Type v'} →
  {R : Type u} →
    {A : Type v} →
      {B : Type w} →
        [inst : CommSemiring R] →
          [inst_1 : NonUnitalNonAssocSemiring A] →
            [inst_2 : NonUnitalNonAssocSemiring B] →
              [inst_3 : Module R A] →
                [inst_4 : Module R B] →
                  [inst_5 : FunLike F A B] →
                    [NonUnitalAlgHomClass F R A B] → F → NonUnitalSubalgebra R A → NonUnitalSubalgebra R B
-- Lean.Data.KVMap
/-- Update a `Syntax` entry based on its current value.  -/
Lean.KVMap.updateSyntax : Lean.KVMap → Lean.Name → (Lean.Syntax → Lean.Syntax) → Lean.KVMap
-- Mathlib.RingTheory.RootsOfUnity.Basic
/-- A variant of `mem_rootsOfUnity` using `ζ : Mˣ`.  -/
mem_rootsOfUnity' : ∀ {M : Type u_1} [inst : CommMonoid M] (k : ℕ) (ζ : Mˣ), ζ ∈ rootsOfUnity k M ↔ ↑ζ ^ k = 1
-- Mathlib.Topology.Algebra.Group.Basic
map_add_left_nhds_zero : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [IsTopologicalAddGroup G] (x : G),
  Filter.map (fun x_1 => x + x_1) (nhds 0) = nhds x
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.instHasLeftCalculusOfFractionsUnopOfHasRightCalculusOfFractionsOpposite : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (W : CategoryTheory.MorphismProperty Cᵒᵖ)
  [h : W.HasRightCalculusOfFractions], W.unop.HasLeftCalculusOfFractions
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.ofEq : Int.Internal.Linear.Var → Lean.Meta.Grind.Arith.Cutsat.EqCnstr → Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof
-- Mathlib.AlgebraicGeometry.Spec
AlgebraicGeometry.stalkMap_toStalk_apply : ∀ {R S : CommRingCat} (f : R ⟶ S) (p : PrimeSpectrum ↑S) (x : ↑R),
  (CategoryTheory.ConcreteCategory.hom
        (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap (AlgebraicGeometry.Spec.sheafedSpaceMap f).hom p))
      ((CategoryTheory.ConcreteCategory.hom
          (AlgebraicGeometry.StructureSheaf.toStalk (↑R) (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p)))
        x) =
    (CategoryTheory.ConcreteCategory.hom
        (CategoryTheory.CategoryStruct.comp f (AlgebraicGeometry.StructureSheaf.toStalk (↑S) p)))
      x