mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.Widget.StringDiagram
Mathlib.Tactic.Widget.StringDiagram.Kind.none.sizeOf_spec : sizeOf Mathlib.Tactic.Widget.StringDiagram.Kind.none = 1
-- Mathlib.CategoryTheory.Preadditive.Basic
/-- A preadditive category has a cokernel for `f - g` if it has a coequalizer for `f` and `g`.  -/
CategoryTheory.Preadditive.hasCokernel_of_hasCoequalizer : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C} (f g : X ⟶ Y)
  [CategoryTheory.Limits.HasCoequalizer f g], CategoryTheory.Limits.HasCokernel (f - g)
-- Mathlib.Algebra.Order.GroupWithZero.Basic
div_lt_div₀' : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] [MulPosReflectLT G₀]
  {a b c d : G₀}, a ≤ c → d < b → 0 < c → 0 < d → a / b < c / d
-- Mathlib.Algebra.Group.Defs
isRightRegular_iff_isRegular : ∀ {G : Type u_1} [inst : CommMagma G] {a : G}, IsRightRegular a ↔ IsRegular a
-- Init.Data.BitVec.Bitblast
_private.Init.Data.BitVec.Bitblast.0.BitVec.addRecAux.eq_def : ∀ {l w : ℕ} (x : BitVec (l * w)) (rem : ℕ) (acc : BitVec w),
  BitVec.addRecAux✝ x rem acc =
    match rem with
    | 0 => acc
    | n.succ => BitVec.addRecAux✝ x n (acc + BitVec.extractLsb' (n * w) w x)
-- Mathlib.MeasureTheory.Measure.GiryMonad
MeasureTheory.Measure.ae_ae_of_ae_bind : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {m : MeasureTheory.Measure α}
  {f : α → MeasureTheory.Measure β} {p : β → Prop},
  AEMeasurable f m → (∀ᵐ (b : β) ∂m.bind f, p b) → ∀ᵐ (a : α) ∂m, ∀ᵐ (b : β) ∂f a, p b
-- Mathlib.Analysis.Calculus.Deriv.Mul
HasDerivAt.mul_const : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {𝔸 : Type u_3} [inst_1 : NormedRing 𝔸]
  [inst_2 : NormedAlgebra 𝕜 𝔸] {c : 𝕜 → 𝔸} {c' : 𝔸},
  HasDerivAt c c' x → ∀ (d : 𝔸), HasDerivAt (fun y => c y * d) (c' * d) x
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKeyD_eraseKey_eq_of_beq_minKeyD_eq_false : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k fallback : α},
      (Std.Internal.List.eraseKey k l).isEmpty = false →
        (k == Std.Internal.List.minKeyD l fallback) = false →
          Std.Internal.List.minKeyD (Std.Internal.List.eraseKey k l) fallback = Std.Internal.List.minKeyD l fallback
-- Mathlib.RingTheory.SimpleModule.WedderburnArtin
/-- The existence part of the Artin–Wedderburn theorem.  -/
isSemisimpleRing_iff_pi_matrix_divisionRing : ∀ {R : Type u} [inst : Ring R],
  IsSemisimpleRing R ↔ ∃ n D d x, Nonempty (R ≃+* ((i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) (D i)))
-- Mathlib.Algebra.Lie.OfAssociative
LieModule.toEnd_lie : ∀ (R : Type u) {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M] (x y : L)
  (z : M), ((LieModule.toEnd R L M) x) ⁅y, z⁆ = ⁅((LieAlgebra.ad R L) x) y, z⁆ + ⁅y, ((LieModule.toEnd R L M) x) z⁆
-- Mathlib.Algebra.Category.MonCat.Basic
AddMonCat.neg_hom_apply : ∀ {M N : AddMonCat} (e : M ≅ N) (x : ↑M),
  (CategoryTheory.ConcreteCategory.hom e.inv) ((CategoryTheory.ConcreteCategory.hom e.hom) x) = x
-- Mathlib.GroupTheory.Nilpotent
Subgroup.top_lowerCentralSeries_one : ∀ {G : Type u_1} [inst : Group G], ⊤.lowerCentralSeries 1 = commutator G
-- Lean.Elab.InfoTree.Types
Lean.Elab.TacticInfo.goalsAfter : Lean.Elab.TacticInfo → List Lean.MVarId
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.instAddCommMonoid : {m : Type u_1} → {n : Type u_2} → {A : Type u_5} → [AddCommMonoid A] → AddCommMonoid (CStarMatrix m n A)
-- Init.Data.List.Int.Sum
List.sum_div_length_le_max_int : ∀ {xs : List ℤ} (h : xs ≠ []), xs.sum / ↑xs.length ≤ xs.max h
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.RightFreyd
CategoryTheory.Preadditive.RightFreyd.instAdditiveArrowQuotient : ∀ (V : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} V] [inst_1 : CategoryTheory.Preadditive V],
  (CategoryTheory.Preadditive.RightFreyd.quotient V).Additive
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.ordCompare_minKey!_modify_eq : ∀ {α : Type u} {β : Type v} [inst : Ord α] [Std.TransOrd α] {t : Std.DTreeMap α (fun x => β) compare}
  [inst_2 : Inhabited α] {k : α} {f : β → β}, compare (Std.DTreeMap.Const.modify t k f).minKey! t.minKey! = Ordering.eq
-- Mathlib.RingTheory.PowerBasis
PowerBasis.equivOfMinpoly_aeval : ∀ {S : Type u_2} [inst : Ring S] {A : Type u_4} [inst_1 : CommRing A] [inst_2 : Algebra A S] {S' : Type u_7}
  [inst_3 : Ring S'] [inst_4 : Algebra A S'] (pb : PowerBasis A S) (pb' : PowerBasis A S')
  (h : minpoly A pb.gen = minpoly A pb'.gen) (f : Polynomial A),
  (pb.equivOfMinpoly pb' h) ((Polynomial.aeval pb.gen) f) = (Polynomial.aeval pb'.gen) f
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
/-- **Weierstrass division** ([washington_cyclotomic], Proposition 7.2): let `f`, `g` be
power series over a complete local ring, such that
the image of `g` in the residue field is not zero. Let `n` be the order of the image of `g` in the
residue field. Then there exists a power series `q` and a polynomial `r` of degree `< n`, such that
`f = g * q + r`.  -/
PowerSeries.exists_isWeierstrassDivision : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : IsLocalRing A] (f : PowerSeries A) {g : PowerSeries A}
  [IsAdicComplete (IsLocalRing.maximalIdeal A) A],
  (PowerSeries.map (IsLocalRing.residue A)) g ≠ 0 → ∃ q r, f.IsWeierstrassDivision g q r
-- Init.Prelude
ReaderT.instMonadExceptOf : {ρ : Type u} → {m : Type u → Type v} → (ε : Type u_1) → [MonadExceptOf ε m] → MonadExceptOf ε (ReaderT ρ m)
-- Mathlib.Analysis.InnerProductSpace.Dual
InnerProductSpace.toDual.congr_simp : ∀ (𝕜 : Type u_1) (E : Type u_2) [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : CompleteSpace E], InnerProductSpace.toDual 𝕜 E = InnerProductSpace.toDual 𝕜 E
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
cfcₙHom_comp : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : Nontrivial R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R] [inst_6 : NonUnitalRing A]
  [inst_7 : StarRing A] [inst_8 : TopologicalSpace A] [inst_9 : Module R A] [inst_10 : IsScalarTower R A A]
  [inst_11 : SMulCommClass R A A] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p] {a : A} (ha : p a)
  [ContinuousMapZero.UniqueHom R A] (f : ContinuousMapZero (↑(quasispectrum R a)) R)
  (f' : ContinuousMapZero ↑(quasispectrum R a) ↑(quasispectrum R ((cfcₙHom ha) f))),
  (∀ (x : ↑(quasispectrum R a)), f x = ↑(f' x)) →
    ∀ (g : ContinuousMapZero (↑(quasispectrum R ((cfcₙHom ha) f))) R), (cfcₙHom ha) (g.comp f') = (cfcₙHom ⋯) g
-- Mathlib.Algebra.Algebra.Unitization
Unitization.toEquiv_addEquiv : ∀ {R : Type u_3} {A : Type u_4} [inst : Add R] [inst_1 : Add A], (Unitization.addEquiv R A).toEquiv = Unitization.equiv
-- Init.Data.List.Lemmas
List.eq_nil_iff_length_eq_zero : ∀ {α : Type u_1} {l : List α}, l = [] ↔ l.length = 0
-- Mathlib.Algebra.Order.Nonneg.Lattice
/-- If `sSup ∅ ≤ a` then `{x : α // a ≤ x}` is a `ConditionallyCompleteLinearOrder`.  -/
Nonneg.conditionallyCompleteLinearOrder : {α : Type u_1} → [inst : ConditionallyCompleteLinearOrder α] → {a : α} → ConditionallyCompleteLinearOrder { x // a ≤ x }
-- Mathlib.Topology.Inseparable
Inseparable.mem_closed_iff : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X} {s : Set X}, Inseparable x y → IsClosed s → (x ∈ s ↔ y ∈ s)
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.add_mk : ∀ {α : Type u} {L₁ L₂ : List (α × Bool)}, FreeAddGroup.mk L₁ + FreeAddGroup.mk L₂ = FreeAddGroup.mk (L₁ ++ L₂)
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.preAleph_symm_aleph0 : Cardinal.preAleph.symm Cardinal.aleph0 = Ordinal.omega0
-- Mathlib.Algebra.GroupWithZero.Units.Basic
/-- The `CommGroupWithZero` version of `div_eq_div_iff_div_eq_div`.  -/
div_eq_div_iff_div_eq_div' : ∀ {G₀ : Type u_3} [inst : CommGroupWithZero G₀] {a b c d : G₀}, b ≠ 0 → c ≠ 0 → (a / b = c / d ↔ a / c = b / d)
-- Mathlib.Data.PNat.Prime
PNat.not_prime_one : ¬PNat.Prime 1
-- Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients
/-- A finite ring has finite quotients.  -/
Ring.HasFiniteQuotients.instOfFinite : ∀ {R : Type u_1} [inst : CommRing R] [Finite R], Ring.HasFiniteQuotients R
-- Lean.Parser.Term
/-- A macro which evaluates to the name of the currently elaborating declaration.  -/
Lean.Parser.Term.declName : Lean.Parser.Parser
-- Init.Data.String.Slice
/-- Returns the last character in `s`. If `s` is empty, returns `none`.

Examples:

* `"abc".toSlice.back? = some 'c'`

* `"".toSlice.back? = none`
 -/
String.Slice.back? : String.Slice → Option Char
-- Mathlib.CategoryTheory.Category.Basic
/-- A `LargeCategory` has objects in one universe level higher than the universe level of
the morphisms. It is useful for examples such as the category of types, or the category
of groups, etc.
 -/
CategoryTheory.LargeCategory : Type (u + 1) → Type (u + 1)
-- Mathlib.Data.Fin.Tuple.Reflection
/-- Creates the expression `f 0 + f 1 + ... + f (n - 1)`.  -/
_private.Mathlib.Data.Fin.Tuple.Reflection.0.FinVec.mkSumEqQ.makeRHS : {u : Lean.Level} →
  {α : Q(Type u)} → Q(AddCommMonoid «$α») → (n : ℕ) → Q(Fin «$n» → «$α») → Q(NeZero «$n») → ℕ → Lean.MetaM Q(«$α»)
-- Mathlib.Analysis.BoxIntegral.Partition.Tagged
BoxIntegral.TaggedPrepartition.distortion_le_iff : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.TaggedPrepartition I) [inst : Fintype ι] {c : NNReal},
  π.distortion ≤ c ↔ ∀ J ∈ π, J.distortion ≤ c
-- Mathlib.Analysis.Calculus.ContDiff.Basic
iteratedFDerivWithin_const_of_ne : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : ℕ},
  n ≠ 0 → ∀ (c : F) (s : Set E), iteratedFDerivWithin 𝕜 n (fun x => c) s = 0
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.DiseqCnstr.mk.injEq : ∀ (p : Lean.Grind.Linarith.Poly) (h : Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof) (p_1 : Lean.Grind.Linarith.Poly)
  (h_1 : Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof),
  ({ p := p, h := h } = { p := p_1, h := h_1 }) = (p = p_1 ∧ h = h_1)
-- Mathlib.GroupTheory.Perm.Sign
Equiv.Perm.sign_bij : ∀ {α : Type u} [inst : DecidableEq α] {β : Type v} [inst_1 : Fintype α] [inst_2 : DecidableEq β] [inst_3 : Fintype β]
  {f : Equiv.Perm α} {g : Equiv.Perm β} (i : (x : α) → f x ≠ x → β),
  (∀ (x : α) (hx : f x ≠ x) (hx' : f (f x) ≠ f x), i (f x) hx' = g (i x hx)) →
    (∀ (x₁ x₂ : α) (hx₁ : f x₁ ≠ x₁) (hx₂ : f x₂ ≠ x₂), i x₁ hx₁ = i x₂ hx₂ → x₁ = x₂) →
      (∀ (y : β), g y ≠ y → ∃ x, ∃ (hx : f x ≠ x), i x hx = y) → Equiv.Perm.sign f = Equiv.Perm.sign g
-- Mathlib.Data.Bool.Basic
Bool.ofNat_toNat : ∀ (b : Bool), Bool.ofNat b.toNat = b
-- Mathlib.RingTheory.PowerSeries.Order
PowerSeries.order_eq_emultiplicity_X : ∀ {R : Type u_2} [inst : Semiring R] (φ : PowerSeries R), φ.order = emultiplicity PowerSeries.X φ
-- Mathlib.NumberTheory.Harmonic.ZetaAsymp
/-- **Alias** of `ZetaAsymptotics.continuousOn_termTSum`. -/
ZetaAsymptotics.continuousOn_term_tsum : ContinuousOn ZetaAsymptotics.termTSum (Set.Ici 1)
-- Mathlib.MeasureTheory.Measure.Stieltjes
botSet.eq_1 : ∀ {R : Type u_1} [inst : LinearOrder R], botSet = {x | IsBot x}
-- Mathlib.CategoryTheory.Localization.Predicate
CategoryTheory.Localization.isoOfHom_hom_inv_id_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] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [inst_2 : L.IsLocalization W] {X Y : C} (f : X ⟶ Y) (hf : W f) {Z : D}
  (h : L.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (L.map f)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Localization.isoOfHom L W f hf).inv h) =
    h
-- Mathlib.Data.Set.Operations
/-- `f` is injective on `s` if the restriction of `f` to `s` is injective.  -/
Set.InjOn : {α : Type u} → {β : Type v} → (α → β) → Set α → Prop
-- Mathlib.Data.Finset.Disjoint
Finset.coe_disjUnion : ∀ {α : Type u_2} {s t : Finset α} (h : Disjoint s t), ↑(s.disjUnion t h) = ↑s ∪ ↑t
-- Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
/-- An auxiliary lemma en route to `RootPairing.finrank_corootSpan_eq'`.  -/
_private.Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate.0.RootPairing.finrank_corootSpan_le' : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Fintype ι] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : CommRing R] [IsDomain R] [inst_5 : Module R M] [inst_6 : Module R N]
  (P : RootPairing ι R M N) [P.IsAnisotropic], Module.finrank R ↥(P.corootSpan R) ≤ Module.finrank R ↥(P.rootSpan R)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.instBEqPower.beq.eq_1 : ∀ (a : Lean.Grind.CommRing.Var) (a_1 : ℕ) (b : Lean.Grind.CommRing.Var) (b_1 : ℕ),
  Lean.Grind.CommRing.instBEqPower.beq { x := a, k := a_1 } { x := b, k := b_1 } = (a == b && a_1 == b_1)
-- Mathlib.Order.Antisymmetrization
instSubsingletonAntisymmetrization : ∀ {α : Type u_1} (r : α → α → Prop) [inst : IsPreorder α r] [Subsingleton α], Subsingleton (Antisymmetrization α r)
-- Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
SSet.Subcomplex.prod.eq_1 : ∀ {X Y : SSet} (A : X.Subcomplex) (B : Y.Subcomplex), A.prod B = { obj := fun Δ => (A.obj Δ).prod (B.obj Δ), map := ⋯ }
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LetValue.isPersistent : Lean.Compiler.LCNF.LetValue Lean.Compiler.LCNF.Purity.impure → Bool
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.getEntryGT!_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited ((a : α) × β a)] {k : α}, t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.getEntryGT! k = t₂.getEntryGT! k
-- Mathlib.Order.CompleteLattice.Basic
iInf_apply : ∀ {α : Type u_8} {β : α → Type u_9} {ι : Sort u_10} [inst : (i : α) → InfSet (β i)] {f : ι → (a : α) → β a} {a : α},
  (⨅ i, f i) a = ⨅ i, f i a
-- Mathlib.Tactic.Linter.FindDeprecations
/-- A convenience instance to print a `Lean.Syntax.Range` as the corresponding pair of `String.Pos`.
 -/
_private.Mathlib.Tactic.Linter.FindDeprecations.0.Mathlib.Tactic.instToStringRange_mathlib : ToString Lean.Syntax.Range
-- Mathlib.RingTheory.MvPolynomial.FreeCommRing
FirstOrder.Ring.lift_genericPolyMap : ∀ {ι : Type u_1} {κ : Type u_2} {R : Type u_3} [inst : DecidableEq κ] [inst_1 : CommRing R] [inst_2 : DecidableEq R]
  (monoms : ι → Finset (κ →₀ ℕ)) (f : (i : ι) × ↥(monoms i) ⊕ κ → R) (i : ι),
  (FreeCommRing.lift f) (FirstOrder.Ring.genericPolyMap monoms i) =
    (MvPolynomial.eval (f ∘ Sum.inr)) (↑((FirstOrder.Ring.mvPolynomialSupportLEEquiv monoms).symm (f ∘ Sum.inl)) i)
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.instIsScalarTowerSubtypeMem : ∀ (R : Type u) (L : Type v) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {R₁ : Type u_1}
  [inst_3 : Semiring R₁] [inst_4 : SMul R₁ R] [inst_5 : Module R₁ L] [inst_6 : IsScalarTower R₁ R L]
  (L' : LieSubalgebra R L), IsScalarTower R₁ R ↥L'
-- Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
CliffordAlgebra.reverse_reverse : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} (a : CliffordAlgebra Q), CliffordAlgebra.reverse (CliffordAlgebra.reverse a) = a
-- Mathlib.Topology.Defs.Basic
/-- A set is locally closed if it is the intersection of some open set and some closed set.
Also see `isLocallyClosed_tfae` and other lemmas in `Mathlib/Topology/LocallyClosed.lean`.
 -/
IsLocallyClosed : {X : Type u} → [TopologicalSpace X] → Set X → Prop
-- Mathlib.Analysis.Convolution
HasCompactSupport.convolution_integrand_bound_left : ∀ {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup E'] [inst_2 : NormedAddCommGroup F] {f : G → E} {g : G → E'}
  [inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 E'] [inst_6 : NormedSpace 𝕜 F]
  (L : E →L[𝕜] E' →L[𝕜] F) [inst_7 : AddGroup G] [inst_8 : TopologicalSpace G],
  HasCompactSupport f →
    Continuous f →
      ∀ {x t : G} {s : Set G},
        x ∈ s → ‖(L (f (x - t))) (g t)‖ ≤ (-tsupport f + s).indicator (fun t => (‖L‖ * ⨆ i, ‖f i‖) * ‖g t‖) t
-- Mathlib.Analysis.Normed.Algebra.Exponential
NormedSpace.exp_hasFPowerSeriesAt_zero : ∀ {𝕂 : Type u_1} {𝔸 : Type u_2} [inst : NontriviallyNormedField 𝕂] [inst_1 : CharZero 𝕂] [ContinuousSMul ℚ 𝕂]
  [inst_3 : NormedRing 𝔸] [inst_4 : NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸],
  HasFPowerSeriesAt NormedSpace.exp (NormedSpace.expSeries 𝕂 𝔸) 0
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- The functor establishing the equivalence `CostructuredArrow.preEquivalence`.  -/
CategoryTheory.CostructuredArrow.preEquivalence.functor : {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] →
            (F : CategoryTheory.Functor C D) →
              {G : CategoryTheory.Functor D E} →
                {e : E} →
                  (f : CategoryTheory.CostructuredArrow G e) →
                    CategoryTheory.Functor
                      (CategoryTheory.CostructuredArrow (CategoryTheory.CostructuredArrow.pre F G e) f)
                      (CategoryTheory.CostructuredArrow F f.left)
-- Mathlib.Analysis.SpecialFunctions.Stirling
/-- **Robbins' sharp stepwise bound** for the Stirling sequence:
`log (stirlingSeq n) - log (stirlingSeq (n+1)) ≤ 1 / (12 n (n + 1))`.  -/
Stirling.log_stirlingSeq_sdiff_le : ∀ (n : ℕ), Real.log (Stirling.stirlingSeq n) - Real.log (Stirling.stirlingSeq (n + 1)) ≤ 1 / (12 * ↑n * (↑n + 1))
-- Mathlib.Analysis.Calculus.Deriv.Pow
hasStrictDerivAt_pow : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] (n : ℕ) (x : 𝕜),
  HasStrictDerivAt (fun x => x ^ n) (↑n * x ^ (n - 1)) x
-- Mathlib.Algebra.Group.Pi.Lemmas
/-- A family of additive monoid homomorphisms `f i : M i →+ N i` defines an additive monoid
homomorphism  `AddMonoidHom.piMap f : (Π i, M i) →+ (Π i, N i)`
given by `AddMonoidHom.piMap f x i = f i x`. This is `Pi.map` for `AddMonoidHom`s.  -/
AddMonoidHom.piMap : {ι : Type u_1} →
  {M : ι → Type u_3} →
    {N : ι → Type u_4} →
      [inst : (i : ι) → AddZeroClass (M i)] →
        [inst_1 : (i : ι) → AddZeroClass (N i)] → ((i : ι) → M i →+ N i) → ((i : ι) → M i) →+ (i : ι) → N i
-- Mathlib.Analysis.Convex.Segment
Prod.segment_subset : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid F] [inst_4 : Module 𝕜 E] [inst_5 : Module 𝕜 F] (x y : E × F),
  segment 𝕜 x y ⊆ segment 𝕜 x.1 y.1 ×ˢ segment 𝕜 x.2 y.2
-- Mathlib.Data.Finset.Lattice.Basic
Finset.union_subset_union : ∀ {α : Type u_1} [inst : DecidableEq α] {s t u v : Finset α}, s ⊆ u → t ⊆ v → s ∪ t ⊆ u ∪ v
-- Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
ProbabilityTheory.IsRatStieltjesPoint.tendsto_atTop_one : ∀ {α : Type u_1} {f : α → ℚ → ℝ} {a : α},
  ProbabilityTheory.IsRatStieltjesPoint f a → Filter.Tendsto (f a) Filter.atTop (nhds 1)
-- Mathlib.Data.Set.Basic
Set.Subset.refl : ∀ {α : Type u} (a : Set α), a ⊆ a
-- Lean.Elab.BuiltinCommand
_private.Lean.Elab.BuiltinCommand.0.Lean.Elab.Command.addScope : Bool →
  String →
    Lean.Name →
      optParam Bool false →
        optParam Bool false →
          optParam Bool false →
            optParam (List (Lean.TSyntax `Lean.Parser.Term.attrInstance)) [] → Lean.Elab.Command.CommandElabM Unit
-- Mathlib.LinearAlgebra.Matrix.Permutation
/-- `permMatrix` as a homomorphism.  -/
Matrix.permMatrixHom : {n : Type u_1} →
  {R : Type u_2} →
    [inst : DecidableEq n] → [inst_1 : Fintype n] → [inst_2 : NonAssocSemiring R] → Equiv.Perm n →* Matrix n n R
-- Std.Data.DHashMap.Internal.AssocList.Iterator
Std.DHashMap.Internal.AssocList.instIteratorAssocListIteratorIdSigma : {α : Type u_1} →
  {β : α → Type u_2} → Std.Iterator (Std.DHashMap.Internal.AssocList.AssocListIterator α β) Id ((a : α) × β a)
-- Mathlib.Analysis.BoxIntegral.Partition.Tagged
BoxIntegral.TaggedPrepartition.isPartition_single_iff : ∀ {ι : Type u_1} {I J : BoxIntegral.Box ι} {x : ι → ℝ} (hJ : J ≤ I) (h : x ∈ BoxIntegral.Box.Icc I),
  (BoxIntegral.TaggedPrepartition.single I J hJ x h).IsPartition ↔ J = I
-- Mathlib.Order.Interval.Finset.Defs
Set.toFinset_Ioc : ∀ {α : Type u_3} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] (b a : α) [inst_2 : Fintype ↑(Set.Ioc b a)],
  (Set.Ioc b a).toFinset = Finset.Ioc b a
-- Mathlib.Order.SuccPred.Archimedean
/-- `IsSuccArchimedean` transfers across equivalences between `SuccOrder`s.  -/
IsSuccArchimedean.of_orderIso : ∀ {X : Type u_3} {Y : Type u_4} [inst : PartialOrder X] [inst_1 : PartialOrder Y] [inst_2 : SuccOrder X]
  [IsSuccArchimedean X] [inst_4 : SuccOrder Y] (f : X ≃o Y), IsSuccArchimedean Y
-- Lean.Data.Lsp.Client
Lean.Lsp.Registration.registerOptions : Lean.Lsp.Registration → Option Lean.Json
-- Batteries.Data.Fin.Fold
Fin.dfoldr_succ : ∀ {n : ℕ} {α : Fin (n + 1 + 1) → Type u_1} (f : (i : Fin (n + 1)) → α i.succ → α i.castSucc) (x : α (Fin.last (n + 1))),
  Fin.dfoldr (n + 1) α f x = f 0 (Fin.dfoldr n (α ∘ Fin.succ) (fun x => f x.succ) x)
-- Std.Data.Iterators.Lemmas.Combinators.DropWhile
_private.Std.Data.Iterators.Lemmas.Combinators.DropWhile.0.Std.Iter.toArray_eq_match_step.match_1.eq_3 : ∀ {α β : Type u_1} (motive : Std.IterStep (Std.Iter β) β → Sort u_2)
  (h_1 : (it' : Std.Iter β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.Iter β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.done with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_3 ()
-- Mathlib.Data.Nat.ModEq
Nat.modEq_add_mul_modulus_iff : ∀ {n a b c : ℕ}, a ≡ b + c * n [MOD n] ↔ a ≡ b [MOD n]
-- Mathlib.Algebra.Group.Action.Opposite
CommSemigroup.isCentralScalar : ∀ {α : Type u_3} [inst : CommSemigroup α], IsCentralScalar α α
-- Mathlib.AlgebraicTopology.SimplicialSet.CoherentIso
CategoryTheory.WalkingIso.rec_one : ∀ {motive : CategoryTheory.WalkingIso → Sort u_1} (zero : motive CategoryTheory.WalkingIso.zero)
  (one : motive CategoryTheory.WalkingIso.one),
  CategoryTheory.WalkingIso.rec zero one CategoryTheory.WalkingIso.one = one
-- Mathlib.GroupTheory.Congruence.Defs
/-- The morphism into the quotient by a congruence relation  -/
Con.toQuotient : {M : Type u_1} → [inst : Mul M] → {c : Con M} → M → c.Quotient
-- Mathlib.CategoryTheory.Triangulated.Rotate
/-- If you rotate a triangle, you get another triangle.
Given a triangle of the form:
```
      f       g       h
  X  ───> Y  ───> Z  ───> X⟦1⟧
```
applying `rotate` gives a triangle of the form:
```
      g       h        -f⟦1⟧'
  Y  ───> Z  ───>  X⟦1⟧ ───> Y⟦1⟧
```
 -/
CategoryTheory.Pretriangulated.Triangle.rotate : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.HasShift C ℤ] →
        CategoryTheory.Pretriangulated.Triangle C → CategoryTheory.Pretriangulated.Triangle C
-- Init.Coe
instCoeHTCTOfCoeHTC : {α : Sort u_1} → {β : Sort u_2} → [CoeHTC α β] → CoeHTCT α β
-- Mathlib.Algebra.Order.Floor.Ring
Int.fract_one : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] [IsOrderedRing R], Int.fract 1 = 0
-- Mathlib.Analysis.Calculus.Darboux
/-- **Darboux's theorem**: the image of a `Set.OrdConnected` set under `f'` is a `Set.OrdConnected`
set, `HasDerivWithinAt` version.  -/
Set.OrdConnected.image_hasDerivWithinAt : ∀ {f f' : ℝ → ℝ} {s : Set ℝ}, s.OrdConnected → (∀ x ∈ s, HasDerivWithinAt f (f' x) s x) → (f' '' s).OrdConnected
-- Init.Data.SInt.Lemmas
Int32.minValue_le_toInt : ∀ (x : Int32), Int32.minValue.toInt ≤ x.toInt