mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.Group.Continuity
tendsto_norm_div_self_nhdsGE : ∀ {E : Type u_4} [inst : SeminormedCommGroup E] (x : E),
  Filter.Tendsto (fun a => ‖a / x‖) (nhds x) (nhdsWithin 0 (Set.Ici 0))
-- Mathlib.Geometry.Convex.Cone.Basic
/-- A convex cone is reproducing if its set of element differences equals the entire module,
i.e., every element of `M` can be written as a difference of two elements of `C`.  -/
ConvexCone.IsReproducing : {R : Type u_2} →
  {M : Type u_4} →
    [inst : Semiring R] →
      [inst_1 : PartialOrder R] → [inst_2 : AddCommGroup M] → [inst_3 : Module R M] → ConvexCone R M → Prop
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.L1.setToFun_eq_setToL1 : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {T : Set α → E →L[ℝ] F} {C : ℝ} [inst_4 : CompleteSpace F] (hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
  (f : ↥(MeasureTheory.Lp E 1 μ)), MeasureTheory.setToFun μ T hT ↑↑f = (MeasureTheory.L1.setToL1 hT) f
-- Mathlib.Analysis.Normed.Ring.Ultra
IsUltrametricDist.nnnorm_intCast_le_one : ∀ (R : Type u_1) [inst : SeminormedRing R] [NormOneClass R] [IsUltrametricDist R] (z : ℤ), ‖↑z‖₊ ≤ 1
-- Mathlib.Algebra.Ring.Shrink
Shrink.instNonUnitalCommSemiring : {α : Type u_1} → [inst : Small.{v, u_1} α] → [NonUnitalCommSemiring α] → NonUnitalCommSemiring (Shrink.{v, u_1} α)
-- Mathlib.Analysis.Convex.Star
starConvex_iff_forall_pos : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] {x : E} {s : Set E},
  x ∈ s → (StarConvex 𝕜 x s ↔ ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s)
-- Mathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit
CategoryTheory.Functor.weightedLimObjObj_w_assoc : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  (W : CategoryTheory.Functor J (Type w)) (F : CategoryTheory.Functor J C)
  [inst_2 : CategoryTheory.Limits.HasWeightedLimit W F] ⦃j₁ j₂ : J⦄ (x : W.obj j₁) (f : j₁ ⟶ j₂) {Z : C}
  (h : F.obj j₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (W.weightedLimObjObjπ F x) (CategoryTheory.CategoryStruct.comp (F.map f) h) =
    CategoryTheory.CategoryStruct.comp (W.weightedLimObjObjπ F ((CategoryTheory.ConcreteCategory.hom (W.map f)) x)) h
-- Mathlib.Algebra.Order.Floor.Ring
Int.floor_eq_zero_iff : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] {a : R}, ⌊a⌋ = 0 ↔ a ∈ Set.Ico 0 1
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.C.eq_2 : ∀ (R : Type u_1) [inst : CommRing R], Polynomial.Chebyshev.C R 1 = Polynomial.X
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem!_insertMany_list : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp] [inst : BEq α]
  [Std.LawfulBEqCmp cmp] [inst : Inhabited β],
  t.WF →
    ∀ {l : List (α × β)} {k : α},
      (t.insertMany l)[k]! =
        (List.findSomeRev?
              (fun x =>
                match x with
                | (a, b) => if cmp a k = Ordering.eq then some b else none)
              l).getD
          t[k]!
-- Init.Data.Float.Float32
instLTFloat32 : LT Float32
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.mem_comap : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B] (S : Subalgebra R B) (f : A →ₐ[R] B) (x : A),
  x ∈ Subalgebra.comap f S ↔ f x ∈ S
-- Mathlib.Topology.Category.TopCat.GrothendieckTopology
TopCat.instIsMultiplicativeIsOpenEmbedding : TopCat.isOpenEmbedding.IsMultiplicative
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.coeff_C_zero : ∀ {R : Type u_1} [inst : Semiring R] {a : R}, (SkewPolynomial.C a).coeff 0 = a
-- Mathlib.Logic.Function.Basic
Function.Injective.dite : ∀ {α : Sort u_1} {β : Sort u_2} (p : α → Prop) [inst : DecidablePred p] {f : { a // p a } → β} {f' : { a // ¬p a } → β},
  Function.Injective f →
    Function.Injective f' →
      (∀ {x x' : α} {hx : p x} {hx' : ¬p x'}, f ⟨x, hx⟩ ≠ f' ⟨x', hx'⟩) →
        Function.Injective fun x => if h : p x then f ⟨x, h⟩ else f' ⟨x, h⟩
-- Mathlib.Order.BoundedOrder.Basic
lt_top_iff_not_top_le : ∀ {α : Type u} [inst : Preorder α] [inst_1 : OrderTop α] {a : α}, a < ⊤ ↔ ¬⊤ ≤ a
-- Mathlib.Analysis.Convex.Side
Affine.Simplex.wSameSide_affineSpan_faceOpposite_point_left_iff : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P] {n : ℕ}
  [inst_6 : NeZero n] (s : Affine.Simplex R P n) {w : Fin (n + 1) → R},
  ∑ j, w j = 1 →
    ∀ {i : Fin (n + 1)},
      (affineSpan R (Set.range (s.faceOpposite i).points)).WSameSide (s.points i)
          ((Finset.affineCombination R Finset.univ s.points) w) ↔
        0 ≤ w i
-- Lean.Meta.LitValues
/-- If `e` is a literal value, ensure it is encoded using the standard representation.
Otherwise, just return `e`.
 -/
Lean.Meta.normLitValue : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Analysis.CStarAlgebra.ContinuousMap
ContinuousMap.instCStarAlgebra : {α : Type u_1} →
  {A : Type u_2} → [inst : TopologicalSpace α] → [CompactSpace α] → [inst_2 : CStarAlgebra A] → CStarAlgebra C(α, A)
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.Mor₂.of.inj : ∀ {η η_1 : Mathlib.Tactic.BicategoryLike.Atom},
  Mathlib.Tactic.BicategoryLike.Mor₂.of η = Mathlib.Tactic.BicategoryLike.Mor₂.of η_1 → η = η_1
-- Mathlib.RingTheory.MvPowerSeries.Substitution
MvPowerSeries.HasSubst.cons_subst_zero_left : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] {f : MvPowerSeries (Fin 2) R} (i j k : σ),
  MvPowerSeries.constantCoeff f = 0 →
    MvPowerSeries.HasSubst ![MvPowerSeries.subst ![MvPowerSeries.X i, MvPowerSeries.X j] f, MvPowerSeries.X k]
-- Mathlib.Analysis.Calculus.LogDeriv
logDeriv_inv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] (x : 𝕜), logDeriv (fun x => x⁻¹) x = -1 / x
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddSubsemigroup.map_bot : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (f : M →ₙ+ N), AddSubsemigroup.map f ⊥ = ⊥
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.tsum_eapproxDiff : ∀ {α : Type u_1} [inst : MeasurableSpace α] (f : α → ENNReal),
  Measurable f → ∀ (a : α), ∑' (n : ℕ), ↑((MeasureTheory.SimpleFunc.eapproxDiff f n) a) = f a
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get!_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited β],
  t.WF →
    ∀ {k a : α} {v : β},
      Std.DTreeMap.Raw.Const.get! (t.insert k v) a =
        if cmp k a = Ordering.eq then v else Std.DTreeMap.Raw.Const.get! t a
-- Mathlib.SetTheory.ZFC.Cardinal
/-- The cardinality of a ZFC set.  -/
ZFSet.card : ZFSet.{u} → Cardinal.{u}
-- Mathlib.Data.Num.ZNum
ZNum.cast_bitm1 : ∀ {α : Type u_1} [inst : AddGroupWithOne α] (n : ZNum), ↑n.bitm1 = ↑n + ↑n - 1
-- Mathlib.Order.Atoms
isStronglyCoatomic_iff : ∀ (α : Type u_5) [inst : Preorder α], IsStronglyCoatomic α ↔ ∀ (a b : α), a < b → ∃ x, a ≤ x ∧ x ⋖ b
-- Mathlib.CategoryTheory.Shift.CommShift
CategoryTheory.Functor.commShiftIso_zero' : ∀ {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) (A : Type u_4) [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift C A] [inst_4 : CategoryTheory.HasShift D A] [inst_5 : F.CommShift A] (a : A)
  (h : a = 0), CategoryTheory.Functor.commShiftIso F a = CategoryTheory.Functor.CommShift.isoZero' F A a h
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- If two unoriented angles are equal, and the signs of the corresponding oriented angles are
equal, then the oriented angles are equal (even in degenerate cases).  -/
Orientation.oangle_eq_of_angle_eq_of_sign_eq : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {w x y z : V},
  InnerProductGeometry.angle w x = InnerProductGeometry.angle y z →
    (o.oangle w x).sign = (o.oangle y z).sign → o.oangle w x = o.oangle y z
-- Mathlib.AlgebraicGeometry.StructureSheaf
AlgebraicGeometry.StructureSheaf.instAwayObjOppositeOpensCarrierTopObjFunctorTypeIsSheafGrothendieckTopologyStructureSheafInTypeOpBasicOpen : ∀ {R : Type u} [inst : CommRing R] (f : R),
  IsLocalization.Away f ((AlgebraicGeometry.structureSheafInType R R).obj.obj (Opposite.op (PrimeSpectrum.basicOpen f)))
-- Init.Data.Range.Polymorphic.Map
Std.Rxo.LawfulHasSize.ofMap : ∀ {α : Type u_1} {β : Type u_2} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.UpwardEnumerable β]
  [inst_2 : LT α] [inst_3 : LT β] [inst_4 : Std.Rxo.HasSize α] [inst_5 : Std.Rxo.HasSize β] [Std.Rxo.LawfulHasSize β]
  (f : Std.PRange.UpwardEnumerable.Map α β) [f.PreservesLT] [f.PreservesRxoSize], Std.Rxo.LawfulHasSize α
-- Mathlib.Topology.PartialHomeomorph.Defs
PartialHomeomorph.continuousOn : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : PartialHomeomorph X Y),
  ContinuousOn (↑e) e.source
-- Init.Data.Float.Float
/-- Converts a floating-point number to a string.

This function does not reduce in the kernel.
 -/
Float.toString : Float → String
-- Mathlib.Algebra.Module.Presentation.Cokernel
Module.Presentation.CokernelData.mk.injEq : ∀ {A : Type u} [inst : Ring A] {M₁ : Type v₁} {M₂ : Type v₂} [inst_1 : AddCommGroup M₁] [inst_2 : Module A M₁]
  [inst_3 : AddCommGroup M₂] [inst_4 : Module A M₂] {pres₂ : Module.Presentation A M₂} {f : M₁ →ₗ[A] M₂} {ι : Type w₁}
  {g₁ : ι → M₁} (lift : ι → pres₂.G →₀ A) (π_lift : ∀ (i : ι), pres₂.π (lift i) = f (g₁ i)) (lift_1 : ι → pres₂.G →₀ A)
  (π_lift_1 : ∀ (i : ι), pres₂.π (lift_1 i) = f (g₁ i)),
  ({ lift := lift, π_lift := π_lift } = { lift := lift_1, π_lift := π_lift_1 }) = (lift = lift_1)
-- Init.Grind.Order
Lean.Grind.Order.le_of_not_lt_k : ∀ {α : Type u_1} [inst : LE α] [inst_1 : LT α] [Std.LawfulOrderLT α] [inst_3 : Std.IsLinearPreorder α]
  [inst_4 : Lean.Grind.Ring α] [Lean.Grind.OrderedRing α] {a b : α} {k k' : ℤ},
  k'.beq' (-k) = true → ¬a < b + ↑k → b ≤ a + ↑k'
-- Mathlib.RingTheory.Radical.Basic
UniqueFactorizationMonoid.radical_of_prime : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [inst_1 : NormalizationMonoid M] [inst_2 : UniqueFactorizationMonoid M]
  {a : M}, Prime a → UniqueFactorizationMonoid.radical a = normalize a
-- Init.Data.List.Monadic
List.flatMapM.loop.eq_2 : ∀ {m : Type u → Type v} [inst : Monad m] {α : Type w} {β : Type u} (f : α → m (List β)) (x : List (List β)) (a : α)
  (as : List α),
  List.flatMapM.loop f (a :: as) x = do
    let bs' ← f a
    List.flatMapM.loop f as (bs' :: x)
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.map_apply : ∀ {Ω : Type u_1} {Ω' : Type u_2} [inst : MeasurableSpace Ω] [inst_1 : MeasurableSpace Ω']
  (ν : MeasureTheory.FiniteMeasure Ω) {f : Ω → Ω'},
  Measurable f → ∀ {A : Set Ω'}, MeasurableSet A → (ν.map f) A = ν (f ⁻¹' A)
-- Mathlib.NumberTheory.Zsqrtd.GaussianInt
GaussianInt.toComplex_sub : ∀ (x y : GaussianInt), GaussianInt.toComplex (x - y) = GaussianInt.toComplex x - GaussianInt.toComplex y
-- Init.Data.Order.Ord
/-- A typeclass for types with a comparison function that satisfies `compare a b = .eq` if and only if
the boolean equality `a == b` holds.

This typeclass distinguishes itself from `LawfulEqOrd` by using boolean equality (`==`) instead of
logical equality (`=`).
 -/
Std.LawfulBEqOrd : (α : Type u) → [BEq α] → [Ord α] → Prop
-- Mathlib.Topology.Baire.Lemmas
/-- If a countable family of closed sets cover a dense `Gδ` set, then the union of their interiors
is dense. Formulated here with `⋃`.  -/
IsGδ.dense_iUnion_interior_of_closed : ∀ {X : Type u_1} {ι : Sort u_3} [inst : TopologicalSpace X] [BaireSpace X] [Countable ι] {s : Set X},
  IsGδ s → Dense s → ∀ {f : ι → Set X}, (∀ (i : ι), IsClosed (f i)) → s ⊆ ⋃ i, f i → Dense (⋃ i, interior (f i))
-- Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic
_private.Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic.0.ProbabilityTheory.HasIndepIncrements.indepFun_sub_sub.match_1_1.congr_eq_1 : ∀ (motive : ℕ → Sort u_1) (x : ℕ) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1) (h_3 : (x : ℕ) → motive x),
  x = 0 →
    (match x with
      | 0 => h_1 ()
      | 1 => h_2 ()
      | x => h_3 x) ≍
      h_1 ()
-- Mathlib.CategoryTheory.Sites.Precoverage
/-- **Alias** of `CategoryTheory.Precoverage.PullbacksPreservedBy.preservesPairwisePullbacks_of_mem`. -/
CategoryTheory.Precoverage.preservesPairwisePullbacks_of_mem : ∀ {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} {J : CategoryTheory.Precoverage C} {F : CategoryTheory.Functor C D}
  [self : J.PullbacksPreservedBy F] ⦃X : C⦄ ⦃R : CategoryTheory.Presieve X⦄,
  R ∈ J.coverings X → F.PreservesPairwisePullbacks R
-- Mathlib.CategoryTheory.Sites.Hypercover.One
/-- The refinement morphisms between objects in the coverings of the fibre products over `S`.  -/
CategoryTheory.PreOneHypercover.Hom.h₁ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {S : C} →
      {E : CategoryTheory.PreOneHypercover S} →
        {F : CategoryTheory.PreOneHypercover S} →
          (self : E.Hom F) → {i j : E.I₀} → (k : E.I₁ i j) → E.Y k ⟶ F.Y (self.s₁ k)
-- Mathlib.Tactic.Sat.FromLRAT
Sat.Literal.pos : ℕ → Sat.Literal
-- Mathlib.Analysis.SpecialFunctions.Arsinh
Real.sinhEquiv_symm_apply : ∀ (x : ℝ), Real.sinhEquiv.symm x = Real.arsinh x
-- Mathlib.Data.Finsupp.Fintype
Finsupp.fintype : {ι : Type u_1} → {α : Type u_2} → [DecidableEq ι] → [Fintype ι] → [inst : Zero α] → [Fintype α] → Fintype (ι →₀ α)
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
AddMonoidAlgebra.mapDomain_add : ∀ {R : Type u_3} {M : Type u_6} {N : Type u_7} [inst : Semiring R] (f : M → N) (x y : AddMonoidAlgebra R M),
  AddMonoidAlgebra.mapDomain f (x + y) = AddMonoidAlgebra.mapDomain f x + AddMonoidAlgebra.mapDomain f y
-- Mathlib.Topology.Constructions
nhds_ofMul : ∀ {X : Type u} [inst : TopologicalSpace X] (x : X), nhds (Additive.ofMul x) = Filter.map (⇑Additive.ofMul) (nhds x)
-- Mathlib.CategoryTheory.Abelian.Ext
/-- If `X : C` is projective and `n : ℕ`, then `Ext^(n + 1) X Y ≅ 0` for any `Y`.  -/
isZero_Ext_succ_of_projective : ∀ {R : Type u_1} [inst : Ring R] {C : Type u_2} [inst_1 : CategoryTheory.Category.{v_1, u_2} C]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.Linear R C] [inst_4 : CategoryTheory.EnoughProjectives C]
  (X Y : C) [CategoryTheory.Projective X] (n : ℕ),
  CategoryTheory.Limits.IsZero (((Ext R C (n + 1)).obj (Opposite.op X)).obj Y)
-- Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Real.volume_val : ∀ (s : Set ℝ), MeasureTheory.volume s = StieltjesFunction.id.measure s
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.instIsSubApply : ∀ {R : Type u_1} [inst : Ring R] {R₂ : Type u_2} [inst_1 : Ring R₂] {M : Type u_4} [inst_2 : TopologicalSpace M]
  [inst_3 : AddCommGroup M] {M₂ : Type u_5} [inst_4 : TopologicalSpace M₂] [inst_5 : AddCommGroup M₂]
  [inst_6 : Module R M] [inst_7 : Module R₂ M₂] {σ₁₂ : R →+* R₂} [inst_8 : IsTopologicalAddGroup M₂],
  IsSubApply (M →SL[σ₁₂] M₂) M M₂
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.smul_mk : ∀ {S : Type u_1} {R : Type u_3} {c₁ c₂ c₃ : R} [inst : SMul S R] (s : S) (re im_i im_j im_k : R),
  s • { re := re, imI := im_i, imJ := im_j, imK := im_k } =
    { re := s • re, imI := s • im_i, imJ := s • im_j, imK := s • im_k }
-- Mathlib.LinearAlgebra.AffineSpace.Midpoint
AffineEquiv.midpoint_pointReflection_left : ∀ {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 ((AffineEquiv.pointReflection R x) y) y = x
-- Init.Control.Id
/-- Turn a collection with a pure `ForIn` instance into a list.  -/
ForIn.toList : {ρ : Type u_1} → {α : Type u} → [ForIn Id ρ α] → ρ → List α
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1to1.read.eq_1 : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} {n : ℕ} (dec : List.Vector Bool n → Γ)
  (f : Γ → Turing.TM1.Stmt Bool (Turing.TM1to1.Λ' Γ Λ σ) σ),
  Turing.TM1to1.read dec f = Turing.TM1to1.readAux n fun v => Turing.TM1to1.move n Turing.Dir.left (f (dec v))
-- Mathlib.Algebra.BigOperators.NatAntidiagonal
Finset.Nat.prod_antidiagonal_eq_prod_range_succ_mk : ∀ {M : Type u_3} [inst : CommMonoid M] (f : ℕ × ℕ → M) (n : ℕ),
  ∏ ij ∈ Finset.HasAntidiagonal.antidiagonal n, f ij = ∏ k ∈ Finset.range n.succ, f (k, n - k)
-- Init.Data.List.Lemmas
List.foldr_hom : ∀ {β₁ : Type u_1} {β₂ : Type u_2} {α : Type u_3} (f : β₁ → β₂) {g₁ : α → β₁ → β₁} {g₂ : α → β₂ → β₂} {l : List α}
  {init : β₁}, (∀ (x : α) (y : β₁), g₂ x (f y) = f (g₁ x y)) → List.foldr g₂ (f init) l = f (List.foldr g₁ init l)
-- Std.Do.WP.Monad
_private.Std.Do.WP.Monad.0.Std.Do.EStateM.instWP.match_1.eq_1 : ∀ {ε σ α : Type u_1} (motive : EStateM.Result ε σ α → Sort u_2) (a : α) (s' : σ)
  (h_1 : (a : α) → (s' : σ) → motive (EStateM.Result.ok a s'))
  (h_2 : (e : ε) → (s' : σ) → motive (EStateM.Result.error e s')),
  (match EStateM.Result.ok a s' with
    | EStateM.Result.ok a s' => h_1 a s'
    | EStateM.Result.error e s' => h_2 e s') =
    h_1 a s'
-- Mathlib.Analysis.Distribution.TemperedDistribution
TemperedDistribution.instLaplacian : {E : Type u_3} →
  {F : Type u_4} →
    [inst : NormedAddCommGroup E] →
      [inst_1 : InnerProductSpace ℝ E] →
        [FiniteDimensional ℝ E] →
          [inst_3 : AddCommGroup F] →
            [inst_4 : Module ℂ F] →
              [inst_5 : TopologicalSpace F] →
                [IsTopologicalAddGroup F] →
                  [ContinuousConstSMul ℂ F] → Laplacian (TemperedDistribution E F) (TemperedDistribution E F)
-- Lean.Data.Json.Basic
Lean.Json.isNull : Lean.Json → Bool
-- Mathlib.Analysis.Calculus.FDeriv.Mul
hasStrictFDerivAt_ringInverse : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {R : Type u_5} [inst_1 : NormedRing R] [HasSummableGeomSeries R]
  [inst_3 : NormedAlgebra 𝕜 R] (x : Rˣ),
  HasStrictFDerivAt Ring.inverse (-((ContinuousLinearMap.mulLeftRight 𝕜 R) ↑x⁻¹) ↑x⁻¹) ↑x
-- Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
MvPolynomial.esymm_one : ∀ (σ : Type u_5) (R : Type u_6) [inst : CommSemiring R] [inst_1 : Fintype σ],
  MvPolynomial.esymm σ R 1 = ∑ i, MvPolynomial.X i
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Functor.opUnopIso_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) (X : C), F.opUnopIso.hom.app X = CategoryTheory.CategoryStruct.id (F.obj X)
-- Lean.Expr
Lean.instForInMVarIdMapProdMVarIdOfMonad : {m : Type u_1 → Type u_2} → {α : Type} → [Monad m] → ForIn m (Lean.MVarIdMap α) (Lean.MVarId × α)
-- Mathlib.Order.Birkhoff
exists_birkhoff_representation : ∀ (α : Type u) [Finite α] [inst : DistribLattice α], ∃ β x x_1 f, Function.Injective ⇑f
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.inv_hom_h₀_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E F : CategoryTheory.PreOneHypercover S} (e : E ≅ F)
  (i : F.I₀) {Z : C} (h : F.X (e.hom.s₀ (e.inv.s₀ i)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (e.inv.h₀ i) (CategoryTheory.CategoryStruct.comp (e.hom.h₀ (e.inv.s₀ i)) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h
-- Mathlib.LinearAlgebra.TensorProduct.Map
LinearEquiv.symm_lTensor : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Module R P] (f : N ≃ₗ[R] P), (LinearEquiv.lTensor M f).symm = LinearEquiv.lTensor M f.symm
-- Mathlib.RingTheory.HahnSeries.Cardinal
HahnSeries.cardSupp_hsum_powers_le : ∀ {Γ : Type u_1} {R : Type u_2} [inst : LinearOrder Γ] [inst_1 : AddCommMonoid Γ] [inst_2 : IsOrderedCancelAddMonoid Γ]
  [inst_3 : CommRing R] (x : HahnSeries Γ R),
  (HahnSeries.SummableFamily.powers x).hsum.cardSupp ≤ max Cardinal.aleph0 x.cardSupp
-- Mathlib.Order.ConditionallyCompletePartialOrder.Basic
csSup_Ioc : ∀ {α : Type u_1} [inst : ConditionallyCompletePartialOrderSup α] {a b : α}, a < b → sSup (Set.Ioc a b) = b
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.IsInducedSubgraph.ext_of_vertexSet : ∀ {α : Type u_1} {β : Type u_2} {G H : Graph α β}, H.vertexSet = G.vertexSet → H.IsInducedSubgraph G → H = G
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.instHashableSimpCacheKey.hash : Lean.Elab.Tactic.Grind.SimpCacheKey → UInt64
-- Mathlib.Data.NNReal.Defs
Real.natCast_le_toNNReal : ∀ {n : ℕ} {r : ℝ}, n ≠ 0 → (↑n ≤ r.toNNReal ↔ ↑n ≤ r)
-- Mathlib.AlgebraicGeometry.Cover.Over
AlgebraicGeometry.Scheme.instOverPullbackCoverOver : {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
  (S : AlgebraicGeometry.Scheme) →
    [inst : P.IsStableUnderBaseChange] →
      [inst_1 : AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P] →
        {X W : AlgebraicGeometry.Scheme} →
          (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X) →
            (f : W ⟶ X) →
              [inst_2 : W.Over S] →
                [inst_3 : X.Over S] →
                  [inst_4 : AlgebraicGeometry.Scheme.Cover.Over S 𝒰] →
                    [inst_5 : AlgebraicGeometry.Scheme.Hom.IsOver f S] →
                      AlgebraicGeometry.Scheme.Cover.Over S (AlgebraicGeometry.Scheme.Cover.pullbackCoverOver S 𝒰 f)
-- Std.Data.DTreeMap.Raw.Slice
Std.DTreeMap.Raw.instSliceableRoiSlice : {α : Type u} →
  {β : α → Type v} →
    (cmp : autoParam (α → α → Ordering) Std.DTreeMap.Raw.instSliceableRoiSlice._auto_1) →
      Std.Roi.Sliceable (Std.DTreeMap.Raw α β cmp) α (Std.DTreeMap.Internal.RoiSlice α β)
-- Mathlib.Topology.Algebra.Polynomial
Polynomial.coeff_le_of_roots_le : ∀ {F : Type u_3} {K : Type u_4} [inst : CommRing F] [inst_1 : NormedField K] {p : Polynomial F} {f : F →+* K} {B : ℝ}
  (i : ℕ),
  p.Monic →
    (Polynomial.map f p).Splits →
      (∀ z ∈ (Polynomial.map f p).roots, ‖z‖ ≤ B) →
        ‖(Polynomial.map f p).coeff i‖ ≤ B ^ (p.natDegree - i) * ↑(p.natDegree.choose i)
-- Mathlib.LinearAlgebra.Alternating.Basic
MultilinearMap.alternatization_apply : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N' : Type u_6}
  [inst_3 : AddCommGroup N'] [inst_4 : Module R N'] {ι : Type u_7} [inst_5 : Fintype ι] [inst_6 : DecidableEq ι]
  (m : MultilinearMap R (fun x => M) N') (v : ι → M),
  (MultilinearMap.alternatization m) v = ∑ σ, Equiv.Perm.sign σ • (MultilinearMap.domDomCongr σ m) v
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousAlternatingMap.instNeg : {R : Type u_1} →
  {M : Type u_2} →
    {N : Type u_3} →
      {ι : Type u_4} →
        [inst : Ring R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              [inst_3 : TopologicalSpace M] →
                [inst_4 : AddCommGroup N] →
                  [inst_5 : Module R N] →
                    [inst_6 : TopologicalSpace N] → [IsTopologicalAddGroup N] → Neg (M [⋀^ι]→L[R] N)
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupNorm.instAdd : {E : Type u_3} → [inst : Group E] → Add (GroupNorm E)
-- Mathlib.RingTheory.NonUnitalSubring.Defs
NonUnitalSubringClass.mk : ∀ {S : Type u_1} {R : Type u} [inst : NonUnitalNonAssocRing R] [inst_1 : SetLike S R]
  [toNonUnitalSubsemiringClass : NonUnitalSubsemiringClass S R] [toNegMemClass : NegMemClass S R],
  NonUnitalSubringClass S R