mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.Stalk
AlgebraicGeometry.germ_stalkClosedPointIso_hom : ∀ (R : CommRingCat) [inst : IsLocalRing ↑R],
  CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Spec R).presheaf.germ ⊤ (IsLocalRing.closedPoint ↑R) trivial)
      (AlgebraicGeometry.stalkClosedPointIso R).hom =
    (AlgebraicGeometry.Scheme.ΓSpecIso R).hom
-- Mathlib.Algebra.Lie.Nilpotent
LieIdeal.lcs_top : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (M : Type u_3)
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] (k : ℕ),
  ⊤.lcs M k = LieModule.lowerCentralSeries R L M k
-- Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily
CategoryTheory.PreZeroHypercoverFamily.ext : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {x y : CategoryTheory.PreZeroHypercoverFamily C},
  x.property = y.property → x = y
-- Mathlib.Topology.Sion
/-- From the quasi-convexity of `f (·, y)`, deduce that `sublevelLeft` is connected  -/
_private.Mathlib.Topology.Sion.0.Sion.isPreconnected_sublevelLeft : ∀ {E : Type u_1} {F : Type u_2} {β : Type u_3} [inst : LinearOrder β] {X : Set E} {Y : Set F} {f : E → F → β}
  [inst_1 : TopologicalSpace E] [inst_2 : AddCommGroup E] [inst_3 : Module ℝ E] [IsTopologicalAddGroup E]
  [ContinuousSMul ℝ E],
  (∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y) → ∀ (b : β) (y : ↑Y), IsPreconnected (Sion.sublevelLeft✝ X f b ↑y)
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
SheafOfModules.Presentation.ofIsIso_relations : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : CategoryTheory.HasSheafify J AddCommGrpCat]
  [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] {M N : SheafOfModules R} (f : M ⟶ N)
  [inst_3 : CategoryTheory.IsIso f] (σ : M.Presentation),
  (SheafOfModules.Presentation.ofIsIso f σ).relations =
    σ.relations.ofEpi ((CategoryTheory.Limits.kernelCompMono σ.generators.π f).symm ≪≫ CategoryTheory.eqToIso ⋯).hom
-- Mathlib.Order.Filter.AtTopBot.Field
/-- If `f` tends to negative infinity along a nontrivial filter `l`, then
`fun x ↦ r * f x` tends to negative infinity if and only if `0 < r`.  -/
Filter.tendsto_const_mul_atBot_iff_pos : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {l : Filter β}
  {f : β → α} {r : α} [l.NeBot],
  Filter.Tendsto f l Filter.atBot → (Filter.Tendsto (fun x => r * f x) l Filter.atBot ↔ 0 < r)
-- Mathlib.Algebra.Order.Kleene
/-- A Kleene algebra is an idempotent semiring with an additional unary operator `kstar`
(for Kleene star) that satisfies the following properties:
* `1 ≤ a∗`
* `a * a∗ ≤ a∗`
* `a∗ * a ≤ a∗`
* If `b * a ≤ b`, then `b * a∗ ≤ b`
* If `a * b ≤ b`, then `a∗ * b ≤ b`
 -/
KleeneAlgebra : Type u_5 → Type u_5
-- Std.Data.DTreeMap.Internal.Zipper
/-- Removes all elements with key less than or equal to `lowerBound`.

Does not modify size information stored in the tree.
 -/
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.Impl.pruneLE : {α : Type u_1} → {β : α → Type u_2} → [Ord α] → Std.DTreeMap.Internal.Impl α β → α → Std.DTreeMap.Internal.Impl α β
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.functorialityEquivalence_functor : ∀ {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) (e : C ≌ D),
  (CategoryTheory.Limits.Cocone.functorialityEquivalence F e).functor =
    CategoryTheory.Limits.Cocone.functoriality F e.functor
-- Mathlib.Analysis.InnerProductSpace.PiL2
InnerProductSpace.symm_toEuclideanLin_rankOne : ∀ {𝕜 : Type u_7} {m : Type u_8} {n : Type u_9} [inst : RCLike 𝕜] [inst_1 : Fintype m] [inst_2 : Fintype n]
  [inst_3 : DecidableEq n] (x : EuclideanSpace 𝕜 m) (y : EuclideanSpace 𝕜 n),
  Matrix.toEuclideanLin.symm ↑(((InnerProductSpace.rankOne 𝕜) x) y) = Matrix.vecMulVec x.ofLp (star y.ofLp)
-- Batteries.Data.List.Count
List.coe_snd_idxToSigmaCount : ∀ {α : Type u_1} [inst : BEq α] [inst_1 : ReflBEq α] {xs : List α} {i : Fin xs.length},
  ↑(xs.idxToSigmaCount i).snd = List.countBefore xs[↑i] xs ↑i
-- Mathlib.Topology.Order.LawsonTopology
Topology.lawsonClosed_iff_scottClosed_of_isLowerSet : ∀ {α : Type u_1} [inst : Preorder α] (L S : TopologicalSpace α) [Topology.IsLawson α] [Topology.IsScott α Set.univ]
  (s : Set α), IsLowerSet s → (IsClosed s ↔ IsClosed s)
-- Mathlib.Analysis.Calculus.Deriv.Mul
/-- **Alias** of `derivWithin_finsetProd`. -/
derivWithin_finset_prod : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} {ι : Type u_2} [inst_1 : DecidableEq ι]
  {𝔸' : Type u_3} [inst_2 : NormedCommRing 𝔸'] [inst_3 : NormedAlgebra 𝕜 𝔸'] {u : Finset ι} {f : ι → 𝕜 → 𝔸'},
  (∀ i ∈ u, DifferentiableWithinAt 𝕜 (f i) s x) →
    derivWithin (∏ i ∈ u, f i) s x = ∑ i ∈ u, (∏ j ∈ u.erase i, f j x) • derivWithin (f i) s x
-- Init.Data.Order.MinMaxOn
maxOn_eq_right : ∀ {β : Type u_1} {α : Sort u_2} [inst : LE β] [inst_1 : DecidableLE β] {f : α → β} {x y : α},
  ¬f y ≤ f x → maxOn f x y = y
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
/-- If a continuous alternating map is constructed from an alternating map via the constructor
`mkContinuous`, then its norm is bounded by the bound given to the constructor if it is
nonnegative.  -/
AlternatingMap.mkContinuous_norm_le : ∀ {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 F] [inst_5 : Fintype ι] (f : E [⋀^ι]→ₗ[𝕜] F) {C : ℝ},
  0 ≤ C → ∀ (H : ∀ (m : ι → E), ‖f m‖ ≤ C * ∏ i, ‖m i‖), ‖f.mkContinuous C H‖ ≤ C
-- Mathlib.Order.CompleteBooleanAlgebra
/-- Structure containing the minimal axioms required to check that an order is a frame. Do NOT use,
except for implementing `Order.Frame` via `Order.Frame.ofMinimalAxioms`.

This structure omits the `himp`, `compl` fields, which can be recovered using
`Order.Frame.ofMinimalAxioms`.  -/
Order.Frame.MinimalAxioms : (α : Type u) → [CompleteLattice α] → Prop
-- Mathlib.Control.Functor
Functor.Comp.id_map : ∀ {F : Type u → Type w} {G : Type v → Type u} [inst : Functor F] [inst_1 : Functor G] [LawfulFunctor F]
  [LawfulFunctor G] {α : Type v} (x : Functor.Comp F G α), Functor.Comp.map id x = x
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.single_add_erase : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] (m : M) (x : MonoidAlgebra R M),
  MonoidAlgebra.single m (x.coeff m) + MonoidAlgebra.erase m x = x
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Iso.inv_hom_id_triangle_hom₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  {A B : CategoryTheory.Pretriangulated.Triangle C} (e : A ≅ B),
  CategoryTheory.CategoryStruct.comp e.inv.hom₁ e.hom.hom₁ = CategoryTheory.CategoryStruct.id B.obj₁
-- Init.ShareCommon
ShareCommon.StateFactory.get : ShareCommon.StateFactory → ShareCommon.StateFactoryImpl
-- Mathlib.Combinatorics.Additive.Corner.Roth
/-- **Roth's theorem** for finite abelian groups.

The maximum density of a 3AP-free set in `G` goes to zero as `|G|` tends to infinity.  -/
roth_3ap_theorem : ∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : Fintype G] (ε : ℝ),
  0 < ε → cornersTheoremBound ε ≤ Fintype.card G → ∀ (A : Finset G), ε * ↑(Fintype.card G) ≤ ↑A.card → ¬ThreeAPFree ↑A
-- Init.Data.List.SplitOn.Lemmas
_private.Init.Data.List.SplitOn.Lemmas.0.List.splitOnPPrepend.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → List α → Sort u_2) (acc : List α) (h_1 : (acc : List α) → motive [] acc)
  (h_2 : (a : α) → (t acc : List α) → motive (a :: t) acc),
  (match [], acc with
    | [], acc => h_1 acc
    | a :: t, acc => h_2 a t acc) =
    h_1 acc
-- Mathlib.Tactic.ProxyType
/-- Elaborator for `proxy_equiv%`.  -/
Mathlib.ProxyType.elab_proxy_equiv : Lean.Elab.Term.TermElab
-- Mathlib.CategoryTheory.Idempotents.Karoubi
CategoryTheory.Idempotents.instAddCommGroupHom : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [CategoryTheory.Preadditive C] → {P Q : CategoryTheory.Idempotents.Karoubi C} → AddCommGroup (P ⟶ Q)
-- Mathlib.CategoryTheory.Elements
CategoryTheory.CategoryOfElements.fromStructuredArrow_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w))
  {X Y : CategoryTheory.StructuredArrow PUnit.{w + 1} F} (f : X ⟶ Y),
  (CategoryTheory.CategoryOfElements.fromStructuredArrow F).map f = ⟨CategoryTheory.StructuredArrow.Hom.right f, ⋯⟩
-- Lean.ToExpr
_private.Lean.ToExpr.0.Lean.List.toExprAux : {α : Type u_1} → [Lean.ToExpr α] → Lean.Expr → Lean.Expr → List α → Lean.Expr
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKeyD_modify_self : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} [inst_2 : LawfulBEq α]
  [Inhabited α] {k fallback : α} {f : β k → β k},
  m.WF → (m.modify k f).getKeyD k fallback = if k ∈ m then k else fallback
-- Mathlib.Topology.Instances.Real.Lemmas
/-- A continuous, periodic function has compact range.  -/
Function.Periodic.compact_of_continuous : ∀ {α : Type u} [inst : TopologicalSpace α] {f : ℝ → α} {c : ℝ},
  Function.Periodic f c → c ≠ 0 → Continuous f → IsCompact (Set.range f)
-- Mathlib.Order.UpperLower.CompleteLattice
LowerSet.instInhabited : {α : Type u_1} → [inst : LE α] → Inhabited (LowerSet α)
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
StructureGroupoid.LocalInvariantProp.liftPropAt_congr_of_eventuallyEq : ∀ {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [inst : TopologicalSpace H]
  [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M] [inst_3 : TopologicalSpace H']
  [inst_4 : TopologicalSpace M'] [inst_5 : ChartedSpace H' M'] {G : StructureGroupoid H} {G' : StructureGroupoid H'}
  {P : (H → H') → Set H → H → Prop} {g g' : M → M'} {x : M},
  G.LocalInvariantProp G' P → ChartedSpace.LiftPropAt P g x → g' =ᶠ[nhds x] g → ChartedSpace.LiftPropAt P g' x
-- Mathlib.Order.Hom.Bounded
BotHom.instPartialOrder.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Bot α] [inst_1 : PartialOrder β] [inst_2 : Bot β],
  BotHom.instPartialOrder = PartialOrder.lift DFunLike.coe ⋯
-- Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
NNReal.tendsto_agmSequences_snd_agm : ∀ {x y : NNReal}, Filter.Tendsto (fun n => (x.agmSequences y n).2) Filter.atTop (nhds (x.agm y))
-- Mathlib.Tactic.Simps.Basic
_private.Mathlib.Tactic.Simps.Basic.0.instCoeNameStructName : Coe NameStruct✝ Lean.Name
-- Mathlib.Analysis.SpecialFunctions.Gamma.Beta
/-- A weaker, but easier-to-apply, version of `Complex.Gamma_ne_zero`.  -/
Complex.Gamma_ne_zero_of_re_pos : ∀ {s : ℂ}, 0 < s.re → Complex.Gamma s ≠ 0
-- Init.Data.UInt.Lemmas
UInt16.one_def : 1 = { toBitVec := 1 }
-- Mathlib.NumberTheory.Real.Irrational
irrational_sqrt_ratCast_iff_of_nonneg : ∀ {q : ℚ}, 0 ≤ q → (Irrational √↑q ↔ ¬IsSquare q)
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
/-- the auxiliary object of left fractions  -/
CategoryTheory.MorphismProperty.LeftFraction₂.Y' : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W : CategoryTheory.MorphismProperty C} → {X Y : C} → W.LeftFraction₂ X Y → C
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.ComonadIso.toNatIso_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {M N : CategoryTheory.Comonad C} (h : M ≅ N),
  (CategoryTheory.ComonadIso.toNatIso h).inv = (CategoryTheory.comonadToFunctor C).map h.inv
-- Mathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived
CategoryTheory.Functor.leftDerivedUnique.congr_simp : ∀ {C : Type u_1} {D : Type u_2} {H : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_2} D] [inst_2 : CategoryTheory.Category.{v_5, u_3} H]
  (LF' LF : CategoryTheory.Functor D H) {F : CategoryTheory.Functor C H} {L : CategoryTheory.Functor C D}
  (α α_1 : L.comp LF ⟶ F) (e_α : α = α_1) (α'₂ α'₂_1 : L.comp LF' ⟶ F) (e_α'₂ : α'₂ = α'₂_1)
  (W W_1 : CategoryTheory.MorphismProperty C) (e_W : W = W_1) [inst_3 : L.IsLocalization W]
  [inst_4 : LF.IsLeftDerivedFunctor α W] [inst_5 : LF'.IsLeftDerivedFunctor α'₂ W],
  LF'.leftDerivedUnique LF α α'₂ W = LF'.leftDerivedUnique LF α_1 α'₂_1 W_1
-- Mathlib.RingTheory.QuotSMulTop
QuotSMulTop.map_comp_mkQ : ∀ {R : Type u_2} [inst : CommRing R] (r : R) {M : Type u_1} {M' : Type u_3} [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup M'] [inst_4 : Module R M'] (f : M →ₗ[R] M'),
  (QuotSMulTop.map r) f ∘ₗ (r • ⊤).mkQ = (r • ⊤).mkQ ∘ₗ f
-- Mathlib.Data.Fin.Tuple.NatAntidiagonal
Finset.Nat.sigmaAntidiagonalTupleEquivTuple_symm_apply_fst : ∀ (k : ℕ) (x : Fin k → ℕ), ((Finset.Nat.sigmaAntidiagonalTupleEquivTuple k).symm x).fst = ∑ i, x i
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.find! : {α : Type u_1} → {β : Type u_2} → {x : BEq α} → {x_1 : Hashable α} → [Inhabited β] → Lean.PersistentHashMap α β → α → β
-- Lean.Meta.Tactic.Grind.Arith.Simproc
Lean.Meta.Grind.Arith.normNatDivInst : Lean.Meta.Simp.DSimproc
-- Mathlib.NumberTheory.LSeries.AbstractFuncEq
WeakFEPair.symm_f : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (P : WeakFEPair E) (a : ℝ), P.symm.f a = P.g a
-- Init.Data.BitVec.Basic
/-- Population count operation, to count the number of bits with value `1` in `x`.
Also known as `popcount`, `popcnt`.
 -/
BitVec.cpop : {w : ℕ} → BitVec w → BitVec w
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- An oriented angle is unchanged by replacing the first point by one strictly further away on
the same ray.  -/
Sbtw.oangle_eq_left : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₁' p₂ p₃ : P}, Sbtw ℝ p₂ p₁ p₁' → EuclideanGeometry.oangle p₁ p₂ p₃ = EuclideanGeometry.oangle p₁' p₂ p₃
-- Mathlib.SetTheory.Ordinal.Principal
/-- **Alias** of `Ordinal.not_isPrincipal_iff_of_monotone`. -/
Ordinal.not_principal_iff_of_monotone : ∀ {o : Ordinal.{u}} {op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}},
  (∀ (a : Ordinal.{u}), Monotone (op a)) →
    (∀ (a : Ordinal.{u}), Monotone (Function.swap op a)) → (¬Ordinal.IsPrincipal op o ↔ ∃ a < o, o ≤ op a a)
-- Mathlib.Data.Finset.Pi
Finset.pi_val : ∀ {α : Type u_1} {β : α → Type u} [inst : DecidableEq α] (s : Finset α) (t : (a : α) → Finset (β a)),
  (s.pi t).val = s.val.pi fun a => (t a).val
-- Mathlib.Analysis.RCLike.Basic
RCLike.norm_le_re_iff_eq_norm : ∀ {K : Type u_1} [inst : RCLike K] {z : K}, ‖z‖ ≤ RCLike.re z ↔ z = ↑‖z‖
-- Std.Data.Iterators.Lemmas.Combinators.Zip
_private.Std.Data.Iterators.Lemmas.Combinators.Zip.0.Std.Iter.step_intermediateZip.match_3.eq_1 : ∀ {α₁ β₁ : Type u_1} [inst : Std.Iterator α₁ Id β₁]
  (motive : Option { out // ∃ it, it.toIterM.IsPlausibleOutput out } → Sort u_2) (h_1 : Unit → motive none)
  (h_2 : (out₁ : { out // ∃ it, it.toIterM.IsPlausibleOutput out }) → motive (some out₁)),
  (match none with
    | none => h_1 ()
    | some out₁ => h_2 out₁) =
    h_1 ()
-- Lean.Elab.Command
Lean.Elab.Command.State : Type
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.Equiv.beq : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α],
  m₁.WF → m₂.WF → m₁.Equiv m₂ → m₁.beq m₂ = true
-- Mathlib.Data.PNat.Factors
/-- **Alias** of the reverse direction of `PNat.factorMultiset_le_iff`.

---

We now have four different results that all encode the
idea that inequality of multisets corresponds to divisibility
of positive integers.  -/
PNat.factorMultiset_mono : ∀ {m n : ℕ+}, m ∣ n → m.factorMultiset ≤ n.factorMultiset
-- Mathlib.Data.Nat.Factorization.Defs
Nat.multiplicity_eq_factorization : ∀ {n p : ℕ}, Nat.Prime p → n ≠ 0 → multiplicity p n = n.factorization p
-- Mathlib.Topology.Algebra.InfiniteSum.Order
HasProd.abs : ∀ {ι : Type u_1} {α : Type u_3} [inst : CommRing α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [inst_3 : TopologicalSpace α] [OrderTopology α] {f : ι → α} {x : α}, HasProd f x → HasProd (fun x => |f x|) |x|
-- Mathlib.Algebra.FiniteSupport.Basic
/-- Eta-expanded form of `Function.HasFiniteSupport.mul_right` -/
Function.HasFiniteSupport.fun_mul_right : ∀ {α : Type u_1} {M : Type u_4} [inst : MulZeroClass M] (f : α → M) {g : α → M},
  Function.HasFiniteSupport g → Function.HasFiniteSupport fun i => f i * g i
-- Mathlib.Analysis.CStarAlgebra.Multiplier
DoubleCentralizer.toProdHom_apply : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : NormedSpace 𝕜 A] [inst_3 : SMulCommClass 𝕜 A A] [inst_4 : IsScalarTower 𝕜 A A]
  (self : DoubleCentralizer 𝕜 A), DoubleCentralizer.toProdHom self = self.toProd
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2.Stmt.push.sizeOf_spec : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} [inst : SizeOf K] [inst_1 : (a : K) → SizeOf (Γ a)]
  [inst_2 : SizeOf Λ] [inst_3 : SizeOf σ] (k : K) (a : σ → Γ k) (a_1 : Turing.TM2.Stmt Γ Λ σ),
  sizeOf (Turing.TM2.Stmt.push k a a_1) = 1 + sizeOf k + sizeOf a_1
-- Mathlib.Algebra.MonoidAlgebra.Defs
/-- `AddMonoidAlgebra.coeff` as an `AddEquiv`.  -/
AddMonoidAlgebra.coeffAddEquiv : {R : Type u_1} → {M : Type u_4} → [inst : Semiring R] → AddMonoidAlgebra R M ≃+ (M →₀ R)
-- Mathlib.CategoryTheory.Limits.Shapes.End
CategoryTheory.Limits.end_.lift.congr_simp : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} [inst_2 : CategoryTheory.Limits.HasEnd F] {X : C}
  (f f_1 : (j : J) → X ⟶ (F.obj (Opposite.op j)).obj j) (e_f : f = f_1)
  (hf :
    ∀ ⦃i j : J⦄ (g : i ⟶ j),
      CategoryTheory.CategoryStruct.comp (f i) ((F.obj (Opposite.op i)).map g) =
        CategoryTheory.CategoryStruct.comp (f j) ((F.map g.op).app j)),
  CategoryTheory.Limits.end_.lift f hf = CategoryTheory.Limits.end_.lift f_1 ⋯
-- Mathlib.NumberTheory.LSeries.Dirichlet
/-- The L-series of the arithmetic function `ζ` and of the Möbius function are inverses.  -/
ArithmeticFunction.LSeries_zeta_mul_Lseries_moebius : ∀ {s : ℂ},
  1 < s.re →
    LSeries (fun n => ↑(ArithmeticFunction.zeta n)) s * LSeries (fun n => ↑(ArithmeticFunction.moebius n)) s = 1
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous
SheafOfModules.pushforwardPushforwardEquivalence_counit_app_val_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D} (eqv : C ≌ D)
  {S : CategoryTheory.Sheaf J RingCat} {R : CategoryTheory.Sheaf K RingCat} [inst_2 : eqv.functor.IsContinuous J K]
  [inst_3 : eqv.inverse.IsContinuous K J] (φ : S ⟶ (eqv.functor.sheafPushforwardContinuous RingCat J K).obj R)
  (ψ : R ⟶ (eqv.inverse.sheafPushforwardContinuous RingCat K J).obj S)
  (H₁ :
    CategoryTheory.Functor.whiskerRight (CategoryTheory.NatTrans.op eqv.counit) R.obj =
      CategoryTheory.CategoryStruct.comp ψ.hom (eqv.inverse.op.whiskerLeft φ.hom))
  (H₂ :
    CategoryTheory.CategoryStruct.comp φ.hom
        (CategoryTheory.CategoryStruct.comp (eqv.functor.op.whiskerLeft ψ.hom)
          (CategoryTheory.Functor.whiskerRight (CategoryTheory.NatTrans.op eqv.unit) S.obj)) =
      CategoryTheory.CategoryStruct.id S.obj)
  (M : SheafOfModules S) (U : Cᵒᵖ)
  (x :
    ↑((((SheafOfModules.pushforwardPushforwardEquivalence eqv φ ψ H₁ H₂).inverse.comp
                  (SheafOfModules.pushforwardPushforwardEquivalence eqv φ ψ H₁ H₂).functor).obj
              M).val.obj
        U)),
  (CategoryTheory.ConcreteCategory.hom
        (((SheafOfModules.pushforwardPushforwardEquivalence eqv φ ψ H₁ H₂).counit.app M).val.app U))
      x =
    (CategoryTheory.ConcreteCategory.hom (M.val.map (eqv.unit.app (Opposite.unop U)).op)) x
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
OrderedFinpartition.extendLeft_partSize : ∀ {n : ℕ} (c : OrderedFinpartition n), c.extendLeft.partSize = Fin.cons 1 c.partSize
-- Std.Async.System
Std.Async.System.instInhabitedOSInfo.default : Std.Async.System.OSInfo
-- Mathlib.CategoryTheory.ObjectProperty.Shift
CategoryTheory.ObjectProperty.le_shift : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) {A : Type u_2}
  [inst_1 : AddMonoid A] [inst_2 : CategoryTheory.HasShift C A] (a : A) [P.IsStableUnderShiftBy a], P ≤ P.shift a
-- Mathlib.Tactic.Linter.OverlappingInstances
/-- A cache for the result of `getAbstractDataProjections`.  -/
_private.Mathlib.Tactic.Linter.OverlappingInstances.0.Mathlib.Linter.OverlappingInstances.classProjectionsCache : IO.Ref (Lean.NameMap (Array Lean.Expr))
-- Mathlib.Analysis.Normed.Operator.Extend
/-- If a dense embedding `e : E →L[𝕜] G` expands the norm by a constant factor `N⁻¹`, then the
norm of the extension of `f` along `e` is bounded by `N * ‖f‖`.  -/
ContinuousLinearMap.opNorm_extend_le : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {Eₗ : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NontriviallyNormedField 𝕜₂] {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_2 : NormedAddCommGroup E]
  [inst_3 : NormedAddCommGroup Eₗ] [inst_4 : NormedAddCommGroup F] [inst_5 : NormedSpace 𝕜 E]
  [inst_6 : NormedSpace 𝕜 Eₗ] [inst_7 : NormedSpace 𝕜₂ F] [inst_8 : CompleteSpace F] (f : E →SL[σ₁₂] F) {e : E →L[𝕜] Eₗ}
  {N : NNReal} [RingHomIsometric σ₁₂], DenseRange ⇑e → (∀ (x : E), ‖x‖ ≤ ↑N * ‖e x‖) → ‖f.extend e‖ ≤ ↑N * ‖f‖
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.PublishDiagnosticsParams.mk.injEq : ∀ (uri : Lean.Lsp.DocumentUri) (version? : Option ℤ) (isIncremental? : Option Bool)
  (diagnostics : Array Lean.Lsp.Diagnostic) (uri_1 : Lean.Lsp.DocumentUri) (version?_1 : Option ℤ)
  (isIncremental?_1 : Option Bool) (diagnostics_1 : Array Lean.Lsp.Diagnostic),
  ({ uri := uri, version? := version?, isIncremental? := isIncremental?, diagnostics := diagnostics } =
      { uri := uri_1, version? := version?_1, isIncremental? := isIncremental?_1, diagnostics := diagnostics_1 }) =
    (uri = uri_1 ∧ version? = version?_1 ∧ isIncremental? = isIncremental?_1 ∧ diagnostics = diagnostics_1)
-- Mathlib.CategoryTheory.Bicategory.CatEnriched
CategoryTheory.CatEnrichedOrdinary.instEnrichedOrdinaryCategoryCat : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.EnrichedOrdinaryCategory CategoryTheory.Cat C] →
      CategoryTheory.EnrichedOrdinaryCategory CategoryTheory.Cat (CategoryTheory.CatEnrichedOrdinary C)
-- Mathlib.CategoryTheory.DifferentialObject
CategoryTheory.DifferentialObject.shiftZero_inv_app_f : ∀ {S : Type u_1} [inst : AddCommGroupWithOne S] (C : Type u) [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.HasShift C S]
  (X : CategoryTheory.DifferentialObject S C),
  ((CategoryTheory.DifferentialObject.shiftZero C).inv.app X).f = (CategoryTheory.shiftFunctorZero C S).inv.app X.obj
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.Scheme.ofRestrict_toLRSHom_base : ∀ {U : TopCat} (X : AlgebraicGeometry.Scheme) {f : U ⟶ TopCat.of ↥X}
  (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)),
  (AlgebraicGeometry.Scheme.Hom.toLRSHom (X.ofRestrict h)).base = f
-- Mathlib.Data.Complex.Basic
/-- This shortcut instance ensures we do not find `Semiring` via the noncomputable
`Complex.field` instance.  -/
Complex.instSemiring : Semiring ℂ
-- Mathlib.Tactic.Positivity.Core
/-- The result of `positivity` running on an expression `e` of type `α`.  -/
Mathlib.Meta.Positivity.Strictness : {u : Lean.Level} → {α : Q(Type u)} → Q(Zero «$α») → Q(«$α») → Option Q(PartialOrder «$α») → Type
-- Mathlib.Order.Heyting.Basic
HeytingAlgebra.toCompl : {α : Type u_4} → [self : HeytingAlgebra α] → Compl α