mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Sum.Lemmas
_private.Init.Data.Sum.Lemmas.0.Sum.isLeft.match_1.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (motive : α ⊕ β → Sort u_3) (val : β) (h_1 : (val : α) → motive (Sum.inl val))
  (h_2 : (val : β) → motive (Sum.inr val)),
  (match Sum.inr val with
    | Sum.inl val => h_1 val
    | Sum.inr val => h_2 val) =
    h_2 val
-- Mathlib.LinearAlgebra.AffineSpace.MidpointZero
homothety_invOf_two : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_3} [inst : CommRing R] [inst_1 : Invertible 2] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] (a b : P), (AffineMap.homothety a ⅟2) b = midpoint R a b
-- Mathlib.Algebra.Category.BialgCat.Basic
BialgEquiv.toBialgIso_inv : ∀ {R : Type u} [inst : CommRing R] {X Y : Type v} [inst_1 : Ring X] [inst_2 : Ring Y] [inst_3 : Bialgebra R X]
  [inst_4 : Bialgebra R Y] (e : X ≃ₐc[R] Y), e.toBialgIso.inv = BialgCat.ofHom ↑e.symm
-- Mathlib.Analysis.Complex.Harmonic.MeanValue
/-- **Alias** of `InnerProductSpace.HarmonicOnNhd.circleAverage_eq`.

---

The Mean Value Property of harmonic functions: If f : ℂ → F is harmonic in a neighborhood of a
closed disc of radius R and center c, then the circle average circleAverage f c R equals
f c.
 -/
HarmonicOnNhd.circleAverage_eq : ∀ {F : Type u_1} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] [CompleteSpace F] {f : ℂ → F} {c : ℂ} {R : ℝ},
  InnerProductSpace.HarmonicOnNhd f (Metric.closedBall c |R|) → Real.circleAverage f c R = f c
-- Mathlib.CategoryTheory.ShrinkYoneda
CategoryTheory.shrinkCoyonedaEquiv_symm_app_shrinkCoyonedaObjObjEquiv_symm : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] {X : Cᵒᵖ}
  {P : CategoryTheory.Functor C (Type w)} (s : P.obj (Opposite.unop X)) {Y : Cᵒᵖ} (f : Y ⟶ X),
  (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.shrinkCoyonedaEquiv.symm s).app (Opposite.unop Y)))
      (CategoryTheory.shrinkCoyonedaObjObjEquiv.symm f.unop) =
    (CategoryTheory.ConcreteCategory.hom (P.map f.unop)) s
-- Mathlib.RingTheory.Ideal.Cotangent
Ideal.toCotangent_surjective : ∀ {R : Type u} [inst : CommRing R] (I : Ideal R), Function.Surjective ⇑I.toCotangent
-- Mathlib.LinearAlgebra.AffineSpace.Combination
Finset.weightedVSubVSubWeights_apply_of_ne : ∀ (k : Type u_1) [inst : Ring k] {ι : Type u_4} [inst_1 : DecidableEq ι] {i j t : ι},
  t ≠ i → t ≠ j → Finset.weightedVSubVSubWeights k i j t = 0
-- Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
MeasureTheory.Measure.addHaar_sphere : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  [FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] [Nontrivial E] (x : E) (r : ℝ),
  μ (Metric.sphere x r) = 0
-- Mathlib.Algebra.GroupWithZero.Defs
IsLeftCancelMulZero.to_isCancelMulZero : ∀ {M₀ : Type u_1} [inst : CommMagma M₀] [inst_1 : Zero M₀] [IsLeftCancelMulZero M₀], IsCancelMulZero M₀
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEStronglyMeasurable.comp_aemeasurable : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {g : α → β} {γ : Type u_5} {x : MeasurableSpace γ}
  {x_1 : MeasurableSpace α} {f : γ → α} {μ : MeasureTheory.Measure γ},
  MeasureTheory.AEStronglyMeasurable g (MeasureTheory.Measure.map f μ) →
    AEMeasurable f μ → MeasureTheory.AEStronglyMeasurable (g ∘ f) μ
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.Poly.denote.match_1.eq_1 : ∀ (motive : Lean.Grind.CommRing.Poly → Sort u_1) (k : ℤ) (h_1 : (k : ℤ) → motive (Lean.Grind.CommRing.Poly.num k))
  (h_2 :
    (k : ℤ) →
      (m : Lean.Grind.CommRing.Mon) → (p : Lean.Grind.CommRing.Poly) → motive (Lean.Grind.CommRing.Poly.add k m p)),
  (match Lean.Grind.CommRing.Poly.num k with
    | Lean.Grind.CommRing.Poly.num k => h_1 k
    | Lean.Grind.CommRing.Poly.add k m p => h_2 k m p) =
    h_1 k
-- Mathlib.Algebra.Category.ModuleCat.Biproducts
ModuleCat.instHasBinaryBiproducts : ∀ {R : Type u} [inst : Ring R], CategoryTheory.Limits.HasBinaryBiproducts (ModuleCat R)
-- Mathlib.CategoryTheory.Abelian.Basic
/-- Every abelian category is, in particular, `NonPreadditiveAbelian`.  -/
CategoryTheory.Abelian.nonPreadditiveAbelian : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.Abelian C] → CategoryTheory.NonPreadditiveAbelian C
-- Mathlib.LinearAlgebra.Matrix.RowCol
Matrix.mul_updateCol : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [inst : DecidableEq n] [inst_1 : Fintype m]
  [inst_2 : NonUnitalNonAssocSemiring α] (A : Matrix l m α) (B : Matrix m n α) (j : n) (c : m → α),
  A * B.updateCol j c = (A * B).updateCol j (A.mulVec c)
-- Lean.Environment
/-- Result of `Lean.Environment.promiseChecked`.  -/
Lean.Environment.PromiseCheckedResult : Type
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
_private.Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic.0.IsProperLinearSet.floor_add_of_mem_closure : ∀ {ι : Type u_3} {s : Set (ι → ℕ)} (hs : IsProperLinearSet s) [inst : Finite ι] {x y : ι → ℕ}
  {i : ↑(IsProperLinearSet.basisSet✝ hs)} {t : Set (ι → ℕ)},
  t ⊆ IsProperLinearSet.basisSet✝ hs →
    ↑i ∉ t → y ∈ AddSubmonoid.closure t → IsProperLinearSet.floor✝ hs (x + y) i = IsProperLinearSet.floor✝ hs x i
-- Init.Data.Vector.Lex
Vector.singleton_lex_singleton : ∀ {α : Type u_1} {a b : α} [inst : BEq α] {lt : α → α → Bool}, #v[a].lex #v[b] lt = lt a b
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SignatureHelpContext.activeSignatureHelp? : Lean.Lsp.SignatureHelpContext → Option Lean.Lsp.SignatureHelp
-- Mathlib.Lean.Exception
/-- Check if an exception is a "failed to synthesize" exception.

These exceptions are raised in several different places,
and the only commonality is the prefix of the string, so that's what we look for.
 -/
Lean.Exception.isFailedToSynthesize : Lean.Exception → IO Bool
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.encodeCode.eq_7 : ∀ (cf cg : Nat.Partrec.Code), (cf.prec cg).encodeCode = 2 * (2 * Nat.pair cf.encodeCode cg.encodeCode) + 1 + 4
-- Mathlib.NumberTheory.ArithmeticFunction.LFunction
/-- A private uniform space instance on `ArithmeticFunction R` in order to define `eulerProduct` as
a `tprod`. If `R` is viewed as having the discrete topology, then the resulting topology on
`ArithmeticFunction R` is the topology of pointwise convergence (see `tendsto_iff`).

See `tendsTo_eulerProduct_of_tendsTo` for the outward facing `eulerProduct` API.  -/
ArithmeticFunction.uniformSpace : {R : Type u_2} → [inst : CommSemiring R] → UniformSpace (ArithmeticFunction R)
-- Mathlib.RingTheory.PicardGroup
Module.Invertible.rTensorEquiv_apply_apply : ∀ {R : Type u} {M : Type v} {N : Type u_1} (P : Type u_2) (Q : Type u_3) [inst : CommSemiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : AddCommMonoid Q]
  [inst_5 : Module R M] [inst_6 : Module R N] [inst_7 : Module R P] [inst_8 : Module R Q]
  (e : TensorProduct R M N ≃ₗ[R] R) (f : P →ₗ[R] Q) (a : TensorProduct R P M),
  ((Module.Invertible.rTensorEquiv P Q e) f) a = (TensorProduct.liftAux (TensorProduct.mk R Q M ∘ₗ f)) a
-- Mathlib.MeasureTheory.PiSystem
MeasurableSpace.DynkinSystem.GenerateHas.below.basic : ∀ {α : Type u_3} {s : Set (Set α)} {motive : (a : Set α) → MeasurableSpace.DynkinSystem.GenerateHas s a → Prop}
  (t : Set α) (a : t ∈ s), MeasurableSpace.DynkinSystem.GenerateHas.below ⋯
-- Mathlib.Data.Nat.MaxPowDiv
Nat.divMaxPow_mul_pow_padicValNat : ∀ (p n : ℕ), n.divMaxPow p * p ^ padicValNat p n = n
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rio.toList_toArray : ∀ {α : Type u} {r : Std.Rio α} [inst : Std.PRange.Least? α] [inst_1 : LT α] [inst_2 : DecidableLT α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerable α]
  [inst_5 : Std.Rxo.IsAlwaysFinite α], r.toArray.toList = r.toList
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
/-- The morphism `𝟙_ C ⟶ (ihom X).obj Y` corresponding to a morphism `X ⟶ Y`.  -/
CategoryTheory.MonoidalClosed.curry' : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {X Y : C} →
        [inst_2 : CategoryTheory.Closed X] → (X ⟶ Y) → (CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ X ⟹ Y)
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.ExBase.sum.injEq : ∀ {u : Lean.Level} {α : Q(Type u)} {BaseType : Q(«$α») → Type} {sα : Q(CommSemiring «$α»)} {e : Q(«$α»)}
  (x x_1 : Mathlib.Tactic.Ring.Common.ExSum BaseType sα e),
  (Mathlib.Tactic.Ring.Common.ExBase.sum x = Mathlib.Tactic.Ring.Common.ExBase.sum x_1) = (x = x_1)
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.toReal_nonneg : ∀ {α : Type u_2} [inst : TopologicalSpace α] {f : CompactlySupportedContinuousMap α NNReal}, 0 ≤ f.toReal
-- Mathlib.Algebra.Group.Subgroup.Defs
HasMemOrInvMem.inv_mem_of_notMem : ∀ {S : Type u_3} {G : Type u_4} [inst : Inv G] [inst_1 : SetLike S G] (s : S) [HasMemOrInvMem s], ∀ x ∉ s, x⁻¹ ∈ s
-- Mathlib.Algebra.DualNumber
/-- For two `R`-algebra morphisms out of `A[ε]` to agree, it suffices for them to agree on the
elements of `A` and the `A`-multiples of `ε`.  -/
DualNumber.algHom_ext' : ∀ {R : Type u_1} {B : Type u_3} {A : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] ⦃f g : DualNumber A →ₐ[R] B⦄,
  f.comp (TrivSqZeroExt.inlAlgHom R A A) = g.comp (TrivSqZeroExt.inlAlgHom R A A) →
    f.toLinearMap ∘ₗ ↑R (LinearMap.toSpanSingleton A (DualNumber A) DualNumber.eps) =
        g.toLinearMap ∘ₗ ↑R (LinearMap.toSpanSingleton A (DualNumber A) DualNumber.eps) →
      f = g
-- Mathlib.RingTheory.GradedAlgebra.AlgHom
GradedAlgHom.coe_pow : ∀ {R : Type u_1} {A : Type u_6} {ι : Type u_10} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : DecidableEq ι] [inst_4 : AddMonoid ι] {𝒜 : ι → Submodule R A} [inst_5 : GradedAlgebra 𝒜] (f : 𝒜 →ₐᵍ[R] 𝒜)
  (n : ℕ), ⇑(f ^ n) = (⇑f)^[n]
-- Std.Async.Basic
Std.Async.EAsync.instMonadAwaitAsyncTaskError : Std.Async.MonadAwait Std.Async.AsyncTask (Std.Async.EAsync IO.Error)
-- Mathlib.Combinatorics.Tiling.Tile
/-- An alternative extensionality principle for `PlacedTile` that avoids `HEq`, using equality of
quotient preimages.  -/
DiscreteTiling.PlacedTile.ext_iff_of_preimage : ∀ {G : Type u_1} {X : Type u_2} {ιₚ : Type u_3} [inst : Group G] [inst_1 : MulAction G X]
  {ps : DiscreteTiling.Protoset G X ιₚ} {pt₁ pt₂ : DiscreteTiling.PlacedTile ps},
  pt₁ = pt₂ ↔
    pt₁.index = pt₂.index ∧
      Quotient.mk
            (QuotientGroup.leftRel
              (Subgroup.map (MulAction.stabilizer G ↑(↑ps pt₁.index)).subtype (↑ps pt₁.index).symmetries)) ⁻¹'
          {pt₁.groupElts} =
        Quotient.mk
            (QuotientGroup.leftRel
              (Subgroup.map (MulAction.stabilizer G ↑(↑ps pt₂.index)).subtype (↑ps pt₂.index).symmetries)) ⁻¹'
          {pt₂.groupElts}
-- Mathlib.Data.Finset.Basic
Finset.Nonempty.toList_ne_nil : ∀ {α : Type u_1} {s : Finset α}, s.Nonempty → s.toList ≠ []
-- Mathlib.Order.Monotone.Defs
Monotone.strictMono_of_injective : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : PartialOrder β] {f : α → β},
  Monotone f → Function.Injective f → StrictMono f
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
isPiSystem_isClosed : ∀ {α : Type u_1} [inst : TopologicalSpace α], IsPiSystem {s | IsClosed s}
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.rpow_logb_of_neg : ∀ {b x : ℝ}, 0 < b → b ≠ 1 → x < 0 → b ^ Real.logb b x = -x
-- Mathlib.Algebra.Category.AlgCat.Basic
AlgCat.hasForgetToModule : (R : Type u) → [inst : CommRing R] → CategoryTheory.HasForget₂ (AlgCat R) (ModuleCat R)
-- Mathlib.AlgebraicTopology.SimplicialSet.CoherentIso
/-- From an isomorphism in a category, we can build a functor out of `WalkingIso` to
that category.  -/
CategoryTheory.WalkingIso.fromIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → {X Y : C} → (X ≅ Y) → CategoryTheory.Functor CategoryTheory.WalkingIso C
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.degree_one : ∀ {R : Type u} [inst : Semiring R] [Nontrivial R], Polynomial.degree 1 = 0
-- Mathlib.Data.PEquiv
PEquiv.symm_refl : ∀ {α : Type u}, (PEquiv.refl α).symm = PEquiv.refl α
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.id_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (A : CategoryTheory.Grp C), (CategoryTheory.CategoryStruct.id A).hom.hom = CategoryTheory.CategoryStruct.id A.X
-- Mathlib.Analysis.Distribution.TestFunction
/-- Copy of a `TestFunction` with a new `toFun` equal to the old one. Useful to fix
definitional equalities.  -/
TestFunction.copy : {E : Type u_3} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : NormedSpace ℝ E] →
      {Ω : TopologicalSpace.Opens E} →
        {F : Type u_4} →
          [inst_2 : NormedAddCommGroup F] →
            [inst_3 : NormedSpace ℝ F] →
              {n : ℕ∞} → (f : TestFunction Ω F n) → (f' : E → F) → f' = ⇑f → TestFunction Ω F n
-- Batteries.Recycling.RBTree.WF
_private.Batteries.Recycling.RBTree.WF.0.RBTree.RBNode.append.match_1.splitter : {α : Type u_1} →
  (motive : RBTree.RBNode α → RBTree.RBNode α → Sort u_2) →
    (x x_1 : RBTree.RBNode α) →
      ((x : RBTree.RBNode α) → motive RBTree.RBNode.nil x) →
        ((x : RBTree.RBNode α) → (x = RBTree.RBNode.nil → False) → motive x RBTree.RBNode.nil) →
          ((a : RBTree.RBNode α) →
              (x : α) →
                (b c : RBTree.RBNode α) →
                  (y : α) →
                    (d : RBTree.RBNode α) →
                      motive (RBTree.RBNode.node RBTree.RBColor.red a x b)
                        (RBTree.RBNode.node RBTree.RBColor.red c y d)) →
            ((a : RBTree.RBNode α) →
                (x : α) →
                  (b c : RBTree.RBNode α) →
                    (y : α) →
                      (d : RBTree.RBNode α) →
                        motive (RBTree.RBNode.node RBTree.RBColor.black a x b)
                          (RBTree.RBNode.node RBTree.RBColor.black c y d)) →
              ((l : RBTree.RBNode α) →
                  (v : α) →
                    (r b : RBTree.RBNode α) →
                      (x : α) →
                        (c : RBTree.RBNode α) →
                          motive (RBTree.RBNode.node RBTree.RBColor.black l v r)
                            (RBTree.RBNode.node RBTree.RBColor.red b x c)) →
                ((a : RBTree.RBNode α) →
                    (x : α) →
                      (b l : RBTree.RBNode α) →
                        (v : α) →
                          (r : RBTree.RBNode α) →
                            motive (RBTree.RBNode.node RBTree.RBColor.red a x b)
                              (RBTree.RBNode.node RBTree.RBColor.black l v r)) →
                  motive x x_1
-- Mathlib.Data.Set.Finite.Basic
Set.Finite.inf_of_right : ∀ {α : Type u} {s : Set α}, s.Finite → ∀ (t : Set α), (t ⊓ s).Finite
-- Mathlib.Topology.Algebra.Group.Basic
tendsto_neg_nhdsGE : ∀ {H : Type x} [inst : TopologicalSpace H] [inst_1 : AddCommGroup H] [inst_2 : PartialOrder H] [IsOrderedAddMonoid H]
  [ContinuousNeg H] {a : H}, Filter.Tendsto Neg.neg (nhdsWithin a (Set.Ici a)) (nhdsWithin (-a) (Set.Iic (-a)))
-- Mathlib.Data.Set.Function
Set.exists_eq_graphOn_image_fst : ∀ {α : Type u_1} {β : Type u_2} [Nonempty β] {s : Set (α × β)},
  (∃ f, s = Set.graphOn f (Prod.fst '' s)) ↔ Set.InjOn Prod.fst s
-- Mathlib.Order.Category.CompleteLat
CompleteLat.hasForgetToBddLat : CategoryTheory.HasForget₂ CompleteLat BddLat
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.le_antisymm : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] {f g : CauSeq α abs},
  f ≤ g → g ≤ f → f ≈ g
-- Mathlib.GroupTheory.MonoidLocalization.GrothendieckGroup
Algebra.GrothendieckAddGroup.instAddCommGroup.eq_1 : ∀ {M : Type u_1} [inst : AddCommMonoid M],
  Algebra.GrothendieckAddGroup.instAddCommGroup =
    { toAddMonoid := inferInstance.toAddMonoid, toNeg := Algebra.GrothendieckAddGroup.instNeg, sub := SubNegMonoid.sub',
      zsmul := zsmulRec, sub_eq_add_neg := ⋯, zsmul_zero' := ⋯, zsmul_succ' := ⋯, zsmul_neg' := ⋯, neg_add_cancel := ⋯,
      add_comm := ⋯ }
-- Mathlib.Algebra.Order.Monovary
Antivary.pow_left : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : CommGroup α] [inst_1 : Preorder α] [IsOrderedMonoid α]
  [inst_3 : PartialOrder β] {f : ι → α} {g : ι → β}, Antivary f g → ∀ (n : ℕ), Antivary (f ^ n) g
-- Mathlib.Topology.Algebra.Module.Equiv
/-- An invertible continuous linear map `f` determines a continuous equivalence from `M` to itself.
 -/
ContinuousLinearEquiv.ofUnit : {R : Type u_1} →
  {M : Type u_2} →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → [inst_3 : TopologicalSpace M] → (M →L[R] M)ˣ → M ≃L[R] M
-- Mathlib.Analysis.Convex.SimplicialComplex.AffineIndependentUnion
/-- The simplicial complex associated to a simple graph, where vertices of the graph
are 0-simplices and edges are 1-simplices. The complex is constructed over the
`𝕜`-module of finitely supported functions on the vertex type.
 -/
Geometry.SimplicialComplex.ofSimpleGraph : {𝕜 : Type u_1} →
  {V : Type u_2} →
    [DecidableEq V] →
      [DecidableEq 𝕜] →
        [inst : Field 𝕜] →
          [inst_1 : LinearOrder 𝕜] → [IsStrictOrderedRing 𝕜] → SimpleGraph V → Geometry.SimplicialComplex 𝕜 (V →₀ 𝕜)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
Lean.Meta.Grind.Arith.Cutsat.SymbolicIntInterval.co.sizeOf_spec : ∀ (lo hi : Lean.Meta.Grind.Arith.Cutsat.SymbolicBound),
  sizeOf (Lean.Meta.Grind.Arith.Cutsat.SymbolicIntInterval.co lo hi) = 1 + sizeOf lo + sizeOf hi
-- Lean.Meta.Basic
Lean.Meta.ParamInfo.mk.injEq : ∀ (binderInfo : Lean.BinderInfo) (hasFwdDeps : Bool) (backDeps : Array ℕ)
  (isProp isDecInst isInstance higherOrderOutParam dependsOnHigherOrderOutParam : Bool) (binderInfo_1 : Lean.BinderInfo)
  (hasFwdDeps_1 : Bool) (backDeps_1 : Array ℕ)
  (isProp_1 isDecInst_1 isInstance_1 higherOrderOutParam_1 dependsOnHigherOrderOutParam_1 : Bool),
  ({ binderInfo := binderInfo, hasFwdDeps := hasFwdDeps, backDeps := backDeps, isProp := isProp, isDecInst := isDecInst,
        isInstance := isInstance, higherOrderOutParam := higherOrderOutParam,
        dependsOnHigherOrderOutParam := dependsOnHigherOrderOutParam } =
      { binderInfo := binderInfo_1, hasFwdDeps := hasFwdDeps_1, backDeps := backDeps_1, isProp := isProp_1,
        isDecInst := isDecInst_1, isInstance := isInstance_1, higherOrderOutParam := higherOrderOutParam_1,
        dependsOnHigherOrderOutParam := dependsOnHigherOrderOutParam_1 }) =
    (binderInfo = binderInfo_1 ∧
      hasFwdDeps = hasFwdDeps_1 ∧
        backDeps = backDeps_1 ∧
          isProp = isProp_1 ∧
            isDecInst = isDecInst_1 ∧
              isInstance = isInstance_1 ∧
                higherOrderOutParam = higherOrderOutParam_1 ∧
                  dependsOnHigherOrderOutParam = dependsOnHigherOrderOutParam_1)
-- Mathlib.Tactic.ClickSuggestions.Unfold
/-- `#unfold? e` gives all unfolds of `e`.
In tactic mode, use `unfold?` instead.  -/
Mathlib.Tactic.ClickSuggestions.«command#unfold?_» : Lean.ParserDescr
-- Mathlib.RingTheory.DedekindDomain.Different
pow_sub_one_dvd_differentIdeal_aux : ∀ (A : Type u_1) (K : Type u_2) (L : Type u) {B : Type u_3} [inst : CommRing A] [inst_1 : Field K] [inst_2 : CommRing B]
  [inst_3 : Field L] [inst_4 : Algebra A K] [inst_5 : Algebra B L] [inst_6 : Algebra A B] [inst_7 : Algebra K L]
  [inst_8 : Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [inst_11 : IsDomain A] [IsFractionRing A K]
  [FiniteDimensional K L] [Algebra.IsSeparable K L] [IsIntegralClosure B A L] [IsFractionRing B L] [IsDedekindDomain A]
  [inst_18 : IsDedekindDomain B] [inst_19 : Module.IsTorsionFree A B] [Module.Finite A B] {p : Ideal A} [p.IsMaximal]
  (P : Ideal B) {e : ℕ}, e ≠ 0 → p ≠ ⊥ → P ^ e ∣ Ideal.map (algebraMap A B) p → P ^ (e - 1) ∣ differentIdeal A B
-- Mathlib.Data.Set.Finite.Basic
Set.eq_of_subset_of_card_le : ∀ {α : Type u} {s t : Set α} [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
  s ⊆ t → Fintype.card ↑t ≤ Fintype.card ↑s → s = t
-- Mathlib.Order.RelSeries
RelSeries.drop.eq_1 : ∀ {α : Type u_1} {r : SetRel α α} (p : RelSeries r) (i : Fin (p.length + 1)),
  p.drop i =
    { length := p.length - ↑i,
      toFun := fun x =>
        match x with
        | ⟨j, h⟩ => p.toFun ⟨j + ↑i, ⋯⟩,
      step := ⋯ }
-- Mathlib.InformationTheory.KullbackLeibler.KLFun
/-- The right derivative of `klFun` is `log x`. This also holds at `x = 0` although `klFun` is not
differentiable there since the default value of `derivWithin` in that case is 0.  -/
InformationTheory.rightDeriv_klFun : ∀ {x : ℝ}, derivWithin InformationTheory.klFun (Set.Ioi x) x = Real.log x
-- Mathlib.Algebra.Category.Grp.AB
AddCommGrpCat.HasLimit.productLimitCone.eq_1 : ∀ {J : Type w} (f : J → AddCommGrpCat),
  AddCommGrpCat.HasLimit.productLimitCone f =
    {
      cone :=
        { pt := AddCommGrpCat.of ((j : J) → ↑(f j)),
          π :=
            CategoryTheory.Discrete.natTrans fun j =>
              AddCommGrpCat.ofHom (Pi.evalAddMonoidHom (fun j => ↑(f j)) j.as) },
      isLimit := { lift := AddCommGrpCat.HasLimit.lift f, fac := ⋯, uniq := ⋯ } }
-- Mathlib.Data.Set.Finite.Basic
Set.fintypeInter : {α : Type u} → (s t : Set α) → [DecidableEq α] → [Fintype ↑s] → [Fintype ↑t] → Fintype ↑(s ∩ t)
-- Mathlib.Algebra.Module.SpanRank
Submodule.spanFinrank_span_le_encard : ∀ {R : Type u_1} {M : Type u} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (s : Set M),
  ↑(Submodule.span R s).spanFinrank ≤ s.encard
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
Mathlib.Tactic.BicategoryLike.MonadWhiskerRight.mk : {m : Type → Type} →
  (Mathlib.Tactic.BicategoryLike.WhiskerRight →
      Mathlib.Tactic.BicategoryLike.Atom₁ → m Mathlib.Tactic.BicategoryLike.WhiskerRight) →
    Mathlib.Tactic.BicategoryLike.MonadWhiskerRight m
-- Mathlib.AlgebraicGeometry.ZariskisMainTheorem
AlgebraicGeometry.instUniversallyClosedToNormalization : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.QuasiSeparated f]
  [inst_1 : AlgebraicGeometry.UniversallyClosed f],
  AlgebraicGeometry.UniversallyClosed (AlgebraicGeometry.Scheme.Hom.toNormalization f)
-- Mathlib.Analysis.Convex.Hull
convexHull_eq_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] {s : Set E}, (convexHull 𝕜) s = 0 ↔ s = 0
-- Mathlib.Analysis.InnerProductSpace.Adjoint
LinearMap.instStarRingId : {𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : RCLike 𝕜] →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : InnerProductSpace 𝕜 E] → [FiniteDimensional 𝕜 E] → StarRing (E →ₗ[𝕜] E)
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Op
SSet.Subcomplex.Pairing.op_II : ∀ {X : SSet} {A : X.Subcomplex} (P : A.Pairing), P.op.II = ⇑SSet.Subcomplex.N.opEquiv ⁻¹' P.II
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.ofLE_comp_ofLEMk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {B A : C} (X Y : CategoryTheory.Subobject B) (f : A ⟶ B)
  [inst_1 : CategoryTheory.Mono f] (h₁ : X ≤ Y) (h₂ : Y ≤ CategoryTheory.Subobject.mk f),
  CategoryTheory.CategoryStruct.comp (X.ofLE Y h₁) (Y.ofLEMk f h₂) = X.ofLEMk f ⋯
-- Mathlib.NumberTheory.ArithmeticFunction.Misc
ArithmeticFunction.sigma_eq_sum_div : ∀ (k n : ℕ), (ArithmeticFunction.sigma k) n = ∑ d ∈ n.divisors, (n / d) ^ k
-- Init.Data.Iterators.Consumers.Collect
/-- Traverses the given iterator and stores the emitted values in reverse order in a list. Because
lists are prepend-only, this `toListRev` is usually more efficient that `toList`.

This function is deprecated. Instead of `it.allowNontermination.toListRev`, use `it.toListRev`.
 -/
Std.Iter.Partial.toListRev : {α β : Type w} → [Std.Iterator α Id β] → Std.Iter.Partial β → List β
-- Mathlib.Topology.Algebra.Ring.Basic
/-- The product topology on the Cartesian product of two topological rings
makes the product into a topological ring.  -/
instIsTopologicalRingProd : ∀ {R : Type u_1} {S : Type u_2} [inst : TopologicalSpace R] [inst_1 : TopologicalSpace S]
  [inst_2 : NonUnitalNonAssocRing R] [inst_3 : NonUnitalNonAssocRing S] [IsTopologicalRing R] [IsTopologicalRing S],
  IsTopologicalRing (R × S)