mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.AdjoinRoot
/-- See `finrank_quotient_span_eq_natDegree'` for a version over a ring when `f` is monic.
 -/
finrank_quotient_span_eq_natDegree : ∀ {K : Type u_5} [inst : Field K] {f : Polynomial K}, Module.finrank K (Polynomial K ⧸ Ideal.span {f}) = f.natDegree
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.Functor.Monoidal.toUnit_ε_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.Monoidal] (X : C) {Z : D}
  (h : F.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit (F.obj X))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε F) h) =
    CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.SemiCartesianMonoidalCategory.toUnit X)) h
-- Mathlib.Data.Nat.Bitwise
Nat.zero_of_testBit_eq_false : ∀ {n : ℕ}, (∀ (i : ℕ), n.testBit i = false) → n = 0
-- Mathlib.Analysis.Normed.Group.Constructions
Multiplicative.toNNNorm : {E : Type u_2} → [NNNorm E] → NNNorm (Multiplicative E)
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
/-- The Weierstrass `℘` function. This has the notation `℘[L]` in the namespace `PeriodPairs`.  -/
PeriodPair.«term℘[_]» : Lean.ParserDescr
-- Mathlib.CategoryTheory.Subobject.MonoOver
CategoryTheory.MonoOver.instCoeOut : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → {X : C} → CoeOut (CategoryTheory.MonoOver X) C
-- Mathlib.RingTheory.FormalGroup.Basic
/-- Given an algebra map `f : R →+* S` and a formal group law `F` over `R`, then `f_* F` is a
formal group law formal group law over `S`. This is constructed by applying `f` to all coefficients
of the underlying power series.  -/
FormalGroup.map : {R : Type u_1} →
  [inst : CommRing R] → {S : Type u_2} → [inst_1 : CommRing S] → FormalGroup R → (R →+* S) → FormalGroup S
-- Init.Data.UInt.Lemmas
UInt8.ofNatLT_mul : ∀ {a b : ℕ} (ha : a < 2 ^ 8) (hb : b < 2 ^ 8) (hab : a * b < 2 ^ 8),
  UInt8.ofNatLT (a * b) hab = UInt8.ofNatLT a ha * UInt8.ofNatLT b hb
-- Mathlib.Order.Interval.Finset.Nat
Nat.Icc_eq_range' : ∀ (a b : ℕ), Finset.Icc a b = { val := ↑(List.range' a (b + 1 - a)), nodup := ⋯ }
-- Mathlib.Data.Num.Basic
/-- `bit0 n` appends a `0` to the end of `n`, where `bit0 n = n0`.  -/
ZNum.bit0 : ZNum → ZNum
-- Mathlib.CategoryTheory.Sites.IsSheafFor
CategoryTheory.Presieve.IsSheafFor.isAmalgamation : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C}
  {R : CategoryTheory.Presieve X} (t : CategoryTheory.Presieve.IsSheafFor P R)
  {x : CategoryTheory.Presieve.FamilyOfElements P R} (hx : x.Compatible), x.IsAmalgamation (t.amalgamate x hx)
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Connected
/-- The forgetful functor from the under category creates any connected limit.  -/
CategoryTheory.Under.createsColimitsOfShapeForgetOfIsConnected : {J : Type u'} →
  [inst : CategoryTheory.Category.{v', u'} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        [CategoryTheory.IsConnected J] →
          {B : C} → CategoryTheory.CreatesColimitsOfShape J (CategoryTheory.Under.forget B)
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.Homotopy.refl_apply : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : C(X, Y))
  (x : ↑unitInterval × X), (ContinuousMap.Homotopy.refl f) x = f x.2
-- Init.Data.Range.Polymorphic.Lemmas
Std.Ric.eq_succMany?_of_toList_eq_append_cons : ∀ {α : Type u} {r : Std.Ric α} [inst : Std.PRange.Least? α] [inst_1 : LE α] [inst_2 : DecidableLE α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerable α]
  [inst_5 : Std.PRange.LawfulUpwardEnumerableLE α] [inst_6 : Std.PRange.LawfulUpwardEnumerableLeast? α]
  [inst_7 : Std.Rxc.IsAlwaysFinite α] {pref suff : List α} {cur : α} (h : r.toList = pref ++ cur :: suff),
  cur = (Std.PRange.succMany? pref.length Std.PRange.UpwardEnumerable.least).get ⋯
-- Mathlib.Topology.Algebra.StarSubalgebra
StarSubalgebra.instIsSemitopologicalSemiringSubtypeMem : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : TopologicalSpace A]
  [inst_3 : Semiring A] [inst_4 : Algebra R A] [inst_5 : StarRing A] [inst_6 : StarModule R A]
  [IsSemitopologicalSemiring A] (s : StarSubalgebra R A), IsSemitopologicalSemiring ↥s
-- Lean.Meta.Tactic.Grind.Internalize
/-- Returns `true` if we can generate a congruence proof for `e₁ = e₂`.
See paper: Congruence Closure in Intensional Type Theory for additional details.
 -/
_private.Lean.Meta.Tactic.Grind.Internalize.0.Lean.Meta.Grind.isCongruentCheck : Lean.Expr → Lean.Expr → Lean.Meta.Grind.GoalM Bool
-- Mathlib.CategoryTheory.Action.Basic
/-- The type of `V`-morphisms that can be lifted back to morphisms in the category `Action`.  -/
Action.HomSubtype : (V : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    (G : Type u_2) →
      [inst_1 : Monoid G] →
        {FV : V → V → Type u_3} →
          {CV : V → Type u_4} →
            [inst_2 : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)] →
              [CategoryTheory.ConcreteCategory V FV] → Action V G → Action V G → Type (max 0 u_3)
-- Init.Data.Order.PackageFactories
Std.Packages.LinearPreorderOfLEArgs.mk : {α : Type u} →
  (toPreorderOfLEArgs : Std.Packages.PreorderOfLEArgs α) →
    (ord :
        autoParam
          (let this := toPreorderOfLEArgs.le;
          let this := toPreorderOfLEArgs.decidableLE;
          Ord α)
          Std.Packages.LinearPreorderOfLEArgs.ord._autoParam) →
      (le_total : autoParam (∀ (a b : α), a ≤ b ∨ b ≤ a) Std.Packages.LinearPreorderOfLEArgs.le_total._autoParam) →
        autoParam
            (let this := toPreorderOfLEArgs.le;
            let this_1 := toPreorderOfLEArgs.decidableLE;
            let this_2 := ord;
            ∀ (a b : α), (compare a b).isLE = true ↔ a ≤ b)
            Std.Packages.LinearPreorderOfLEArgs.isLE_compare._autoParam →
          autoParam
              (let this := toPreorderOfLEArgs.le;
              let this_1 := toPreorderOfLEArgs.decidableLE;
              have this_2 := le_total;
              let this_3 := ord;
              ∀ (a b : α), (compare a b).isGE = true ↔ b ≤ a)
              Std.Packages.LinearPreorderOfLEArgs.isGE_compare._autoParam →
            Std.Packages.LinearPreorderOfLEArgs α
-- Init.Data.SInt.Lemmas
Int16.toUInt16_ofBitVec : ∀ (b : BitVec 16), (Int16.ofBitVec b).toUInt16 = { toBitVec := b }
-- Mathlib.CategoryTheory.Abelian.FunctorCategory
/-- The abelian coimage in a functor category can be calculated componentwise.  -/
CategoryTheory.Abelian.FunctorCategory.coimageObjIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type w} →
      [inst_1 : CategoryTheory.Category.{z, w} D] →
        [inst_2 : CategoryTheory.Abelian D] →
          {F G : CategoryTheory.Functor C D} →
            (α : F ⟶ G) → (X : C) → (CategoryTheory.Abelian.coimage α).obj X ≅ CategoryTheory.Abelian.coimage (α.app X)
-- Mathlib.Analysis.Matrix.Hermitian
/-- The diagonal elements of a complex Hermitian matrix are real.  -/
Matrix.IsHermitian.coe_re_diag : ∀ {𝕜 : Type u_1} {n : Type u_3} {A : Matrix n n 𝕜} [inst : RCLike 𝕜],
  A.IsHermitian → (fun i => ↑(RCLike.re (A.diag i))) = A.diag
-- Mathlib.Order.Monotone.Basic
monotone_add_nat_of_le_succ : ∀ {α : Type u} [inst : Preorder α] {f : ℕ → α} {k : ℕ}, (∀ n ≥ k, f n ≤ f (n + 1)) → Monotone fun n => f (n + k)
-- Batteries.Recycling.RBTree.Alter
RBTree.RBNode.modify_eq_alter : ∀ {α : Type u_1} {cut : α → Ordering} {f : α → α} (t : RBTree.RBNode α),
  RBTree.RBNode.modify cut f t = RBTree.RBNode.alter cut (Option.map f) t
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.contains_map : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} {γ : α → Type w} [EquivBEq α]
  [LawfulHashable α] {f : (a : α) → β a → γ a} {k : α}, (Std.DHashMap.map f m).contains k = m.contains k
-- Init.Conv
/-- `tac <;> tac'` runs `tac` on the main goal and `tac'` on each produced goal, concatenating all goals
produced by `tac'`.
 -/
Lean.Parser.Tactic.Conv.«conv_<;>_» : Lean.TrailingParserDescr
-- Mathlib.Order.SymmDiff
codisjoint_bihimp_sup : ∀ {α : Type u_2} [inst : BooleanAlgebra α] (a b : α), Codisjoint (bihimp a b) (a ⊔ b)
-- Mathlib.Order.Partition.Finpartition
/-- Given a finpartition `P` of `a` and finpartitions of each part of `P`, this yields the
finpartition of `a` obtained by juxtaposing all the subpartitions.  -/
Finpartition.bind : {α : Type u_1} →
  [inst : Lattice α] →
    [inst_1 : OrderBot α] →
      [IsModularLattice α] →
        [DecidableEq α] → {a : α} → (P : Finpartition a) → ((i : α) → i ∈ P.parts → Finpartition i) → Finpartition a
-- Mathlib.MeasureTheory.Group.Arithmetic
MeasurableDiv.measurable_div_const : ∀ {G₀ : Type u_2} {inst : MeasurableSpace G₀} {inst_1 : Div G₀} [self : MeasurableDiv G₀] (c : G₀),
  Measurable fun x => x / c
-- Std.Data.ExtDHashMap.Basic
/-- Removes the mapping for the given key if it exists.  -/
Std.ExtDHashMap.erase : {α : Type u} →
  {β : α → Type v} →
    {x : BEq α} → {x_1 : Hashable α} → [EquivBEq α] → [LawfulHashable α] → Std.ExtDHashMap α β → α → Std.ExtDHashMap α β
-- Mathlib.MeasureTheory.Integral.Lebesgue.Map
MeasureTheory.MeasurePreserving.lintegral_comp : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} {g : α → β},
  MeasureTheory.MeasurePreserving g μ ν →
    ∀ {f : β → ENNReal}, Measurable f → ∫⁻ (a : α), f (g a) ∂μ = ∫⁻ (b : β), f b ∂ν
-- Mathlib.Algebra.Ring.BooleanRing
instBooleanAlgebraAsBoolAlg : {α : Type u_1} → [BooleanRing α] → BooleanAlgebra (AsBoolAlg α)
-- Init.Data.Vector.Basic
Vector.instLT : {α : Type u_1} → {n : ℕ} → [LT α] → LT (Vector α n)
-- Mathlib.Analysis.Normed.Module.MStructure
IsLprojection.Subtype.one : {X : Type u_1} →
  [inst : NormedAddCommGroup X] →
    {M : Type u_2} → [inst_1 : Ring M] → [inst_2 : Module M X] → One { P // IsLprojection X P }
-- Mathlib.Data.Sym.Sym2
Sym2.attachWith_map_subtypeVal : ∀ {α : Type u_1} {s : Sym2 α} {P : α → Prop} (h : ∀ a ∈ s, P a), Sym2.map Subtype.val (s.attachWith h) = s
-- Lean.Meta.AppBuilder
/-- Returns `a r b`, where `r` has name `rName` and is implemented using the typeclass `className`.
This method assumes `a` and `b` have the same type.
Examples of supported classes: `LE` and `LT`.
We use heterogeneous operators to ensure we have a uniform representation.
 -/
_private.Lean.Meta.AppBuilder.0.Lean.Meta.mkBinaryRel : Lean.Name → Lean.Name → Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr
-- Init.Data.UInt.Bitwise
USize.ofBitVec_xor : ∀ (a b : BitVec System.Platform.numBits), { toBitVec := a ^^^ b } = { toBitVec := a } ^^^ { toBitVec := b }
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
/-- A surjective ring homomorphism `f : R →+* S` induces a map from `HeightOneSpectrum S` to
`HeightOneSpectrum R` sending `v` to `v.asIdeal.comap f`.  -/
IsDedekindDomain.HeightOneSpectrum.comap : {R : Type u_1} →
  [inst : CommRing R] →
    {S : Type u_4} →
      [inst_1 : CommRing S] →
        (f : R →+* S) →
          Function.Surjective ⇑f → IsDedekindDomain.HeightOneSpectrum S → IsDedekindDomain.HeightOneSpectrum R
-- Mathlib.Algebra.Group.TypeTags.Basic
Additive.addLeftCancelSemigroup : {α : Type u} → [LeftCancelSemigroup α] → AddLeftCancelSemigroup (Additive α)
-- Mathlib.Tactic.Ring.Common
/-- There are several special cases when exponentiating monomials:

* `1 ^ n = 1`
* `x ^ y = (x ^ y)` when `x` is a constant (Note this may fail if e.g. `y` is not a constant)
* `(a * b) ^ e = a ^ e * b ^ e`

In all other cases we use `evalPowProdAtom`.
 -/
Mathlib.Tactic.Ring.Common.evalPowProd : {u : Lean.Level} →
  {α : Q(Type u)} →
    {bt : Q(«$α») → Type} →
      {sα : Q(CommSemiring «$α»)} →
        Mathlib.Tactic.Ring.Common.RingCompute bt sα →
          Mathlib.Tactic.Ring.Common.RingCompute Mathlib.Tactic.Ring.Common.btℕ Mathlib.Tactic.Ring.Common.sℕ →
            {a : Q(«$α»)} →
              {b : Q(ℕ)} →
                Mathlib.Tactic.Ring.Common.ExProd bt sα a →
                  Mathlib.Tactic.Ring.Common.ExProdNat b →
                    Lean.MetaM
                      (Mathlib.Tactic.Ring.Common.Result (Mathlib.Tactic.Ring.Common.ExProd bt sα) q(«$a» ^ «$b»))
-- Mathlib.Data.Matrix.Basic
RingEquiv.mapMatrix_symm : ∀ {m : Type u_2} {α : Type u_11} {β : Type u_12} [inst : Fintype m] [inst_1 : DecidableEq m]
  [inst_2 : NonAssocSemiring α] [inst_3 : NonAssocSemiring β] (f : α ≃+* β), f.mapMatrix.symm = f.symm.mapMatrix
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Carry
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Carry.0.Std.Tactic.BVDecide.BVExpr.bitblast.mkOverflowBit.match_1.eq_1 : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] (aig : Std.Sat.AIG α)
  (motive : Std.Tactic.BVDecide.BVExpr.bitblast.OverflowInput aig → Sort u_1) (w : ℕ) (lhs rhs : aig.RefVec w)
  (cin : aig.Ref)
  (h_1 :
    (w : ℕ) →
      (lhs rhs : aig.RefVec w) → (cin : aig.Ref) → motive { w := w, vec := { lhs := lhs, rhs := rhs }, cin := cin }),
  (match { w := w, vec := { lhs := lhs, rhs := rhs }, cin := cin } with
    | { w := w, vec := { lhs := lhs, rhs := rhs }, cin := cin } => h_1 w lhs rhs cin) =
    h_1 w lhs rhs cin
-- Std.Internal.UV.TCP
/-- Represents a TCP socket.
 -/
Std.Internal.UV.TCP.Socket : Type
-- Mathlib.Topology.MetricSpace.Isometry
Isometry.preimage_ball : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {f : α → β},
  Isometry f → ∀ (x : α) (r : ℝ), f ⁻¹' Metric.ball (f x) r = Metric.ball x r
-- Mathlib.Algebra.GroupWithZero.Action.Defs
/-- Pushforward a `SMulWithZero` structure along a surjective zero-preserving homomorphism.  -/
Function.Surjective.smulWithZero : {M₀ : Type u_2} →
  {A : Type u_7} →
    {A' : Type u_8} →
      [inst : Zero M₀] →
        [inst_1 : Zero A] →
          [inst_2 : SMulWithZero M₀ A] →
            [inst_3 : Zero A'] →
              [inst_4 : SMul M₀ A'] →
                (f : ZeroHom A A') →
                  Function.Surjective ⇑f → (∀ (a : M₀) (b : A), f (a • b) = a • f b) → SMulWithZero M₀ A'
-- Mathlib.CategoryTheory.Presentable.Directed
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₄_W : ∀ {J : Type w} [inst : CategoryTheory.SmallCategory J] {κ : Cardinal.{w}} [inst_1 : Fact κ.IsRegular]
  (D : CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.DiagramWithUniqueTerminal J κ) {m₁ : J}
  (φ : (x : Subtype D.P) → ↑x ⟶ m₁),
  (CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₄ D φ).W =
    (D.W ⊔ CategoryTheory.MorphismProperty.ofHoms fun x => CategoryTheory.CategoryStruct.id m₁) ⊔
      CategoryTheory.MorphismProperty.ofHoms φ
-- Mathlib.Analysis.InnerProductSpace.l2Space
/-- Given a total orthonormal family `v : ι → E`, `E` is a Hilbert sum of `fun i : ι => 𝕜`
relative to the family of linear isometries `fun i k => k • v i`.  -/
Orthonormal.isHilbertSum : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : CompleteSpace E] {v : ι → E} (hv : Orthonormal 𝕜 v),
  ⊤ ≤ (Submodule.span 𝕜 (Set.range v)).topologicalClosure →
    IsHilbertSum 𝕜 (fun x => 𝕜) fun i => LinearIsometry.toSpanSingleton 𝕜 E ⋯
-- Init.Data.Range.Polymorphic.PRange
Std.instDecidableEqRoo.decEq : {α : Type u_1} → [DecidableEq α] → (x x_1 : Std.Roo α) → Decidable (x = x_1)
-- Mathlib.AlgebraicGeometry.Spec
/-- For an algebra `f : R →+* S`, this is the ring homomorphism `S →+* (f∗ 𝒪ₛ)ₚ` for a `p : Spec R`.
This is shown to be the localization at `p` in `isLocalizedModule_toPushforwardStalkAlgHom`.
 -/
AlgebraicGeometry.StructureSheaf.toPushforwardStalk : {R S : CommRingCat} →
  (f : R ⟶ S) →
    (p : PrimeSpectrum ↑R) →
      S ⟶
        ((TopCat.Presheaf.pushforward CommRingCat (AlgebraicGeometry.Spec.topMap f)).obj
              (AlgebraicGeometry.Spec.structureSheaf ↑S).obj).stalk
          p
-- Mathlib.Algebra.Group.Action.Defs
/-- The regular action of a monoid on itself by left multiplication.

This is promoted to a module by `Semiring.toModule`.  -/
Monoid.toMulAction : (M : Type u_1) → [inst : Monoid M] → MulAction M M
-- Mathlib.Order.BoundedOrder.Basic
Bool.instBoundedOrder : BoundedOrder Bool
-- Mathlib.Order.Interval.Set.WithBotTop
WithBot.preimage_coe_Ioc : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, WithBot.some ⁻¹' Set.Ioc ↑b ↑a = Set.Ioc b a
-- Batteries.Data.Char.Basic
Char.eq_true_of_all_eq_true : ∀ {p : Char → Bool}, Char.all p = true → ∀ (c : Char), p c = true
-- Mathlib.Order.Hom.Basic
OrderIso.prodAssoc_apply : ∀ (α : Type u_6) (β : Type u_7) (γ : Type u_8) [inst : LE α] [inst_1 : LE β] [inst_2 : LE γ] (p : (α × β) × γ),
  (OrderIso.prodAssoc α β γ) p = (p.1.1, p.1.2, p.2)
-- Mathlib.Topology.Instances.AddCircle.Defs
/-- If `x` is not congruent to `a` modulo `p`, then `toIcoDiv` is continuous at `x`.

In fact, it is locally near `x`, see `eventuallyEq_toIcoDiv_nhds`.  -/
continuousAt_toIcoDiv : ∀ {𝕜 : Type u_1} [inst : AddCommGroup 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : IsOrderedAddMonoid 𝕜]
  [inst_3 : Archimedean 𝕜] [inst_4 : TopologicalSpace 𝕜] [OrderTopology 𝕜] {p : 𝕜} (hp : 0 < p) (a : 𝕜) {x : 𝕜},
  ¬x ≡ a [PMOD p] → ContinuousAt (toIcoDiv hp a) x
-- Mathlib.Analysis.Polynomial.MahlerMeasure
Polynomial.logMahlerMeasure_zero : Polynomial.logMahlerMeasure 0 = 0
-- Mathlib.Algebra.MvPolynomial.Variables
MvPolynomial.vars_one : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R], MvPolynomial.vars 1 = ∅
-- Mathlib.CategoryTheory.ObjectProperty.LimitsClosure
CategoryTheory.ObjectProperty.strictLimitsClosureIter.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P P_1 : CategoryTheory.ObjectProperty C),
  P = P_1 →
    ∀ {α : Type t} (J : α → Type u') [inst_1 : (a : α) → CategoryTheory.Category.{v', u'} (J a)] {β : Type w'}
      [inst_2 : LinearOrder β] [inst_3 : SuccOrder β] [inst_4 : WellFoundedLT β] (b b_1 : β),
      b = b_1 → ∀ (a a_1 : C), a = a_1 → P.strictLimitsClosureIter J b a = P_1.strictLimitsClosureIter J b_1 a_1
-- Std.Sync.Broadcast
_private.Std.Sync.Broadcast.0.Std.Broadcast.Receiver.mk.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (inner : Std.Bounded.Receiver✝ α), sizeOf { inner := inner } = 1 + sizeOf inner
-- Std.Internal.UV.System
Std.Internal.UV.System.instReprUnameInfo.repr : Std.Internal.UV.System.UnameInfo → ℕ → Std.Format
-- Mathlib.RingTheory.Algebraic.StronglyTranscendental
/-- [Stacks Tag 00Q0](https://stacks.math.columbia.edu/tag/00Q0) -/
isStronglyTranscendental_mk_of_mem_minimalPrimes : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [IsReduced S] {x : S},
  IsStronglyTranscendental R x → ∀ q ∈ minimalPrimes S, IsStronglyTranscendental R ((Ideal.Quotient.mk q) x)
-- Mathlib.Analysis.Normed.Group.Basic
nnnorm_le_mul_nnnorm_add : ∀ {E : Type u_5} [inst : SeminormedGroup E] (a b : E), ‖a‖₊ ≤ ‖a * b‖₊ + ‖b‖₊
-- Lean.Parser.Term
/-- Throws an error exception, tagging the associated message as a named error with the specified name
and validating that an associated error explanation exists. The error name must be followed by a
`Syntax` at which the error is to be thrown. The message is the final argument and may be passed as
an interpolated string or a `MessageData` term.
 -/
Lean.Parser.Term.throwNamedErrorAtMacro : Lean.Parser.Parser
-- Mathlib.Tactic.Algebraize
/-- If true (default), the tactic will search the local context for `RingHom` properties
that can be converted to `Algebra` properties.  -/
Mathlib.Tactic.Algebraize.Config.properties : Mathlib.Tactic.Algebraize.Config → Bool
-- Mathlib.Probability.Process.PartitionFiltration
ProbabilityTheory.measurable_countablePartitionSet : ∀ (α : Type u_2) [inst : MeasurableSpace α] [inst_1 : MeasurableSpace.CountablyGenerated α] (n : ℕ),
  Measurable (MeasurableSpace.countablePartitionSet n)
-- Mathlib.Algebra.Star.StarRingHom
StarRingEquiv.coe_mk : ∀ {A : Type u_1} {B : Type u_2} [inst : Add A] [inst_1 : Add B] [inst_2 : Mul A] [inst_3 : Mul B] [inst_4 : Star A]
  [inst_5 : Star B] (e : A ≃+* B) (h₁ : ∀ (a : A), e.toFun (star a) = star (e.toFun a)),
  ⇑{ toRingEquiv := e, map_star' := h₁ } = ⇑e
-- Mathlib.Algebra.Ring.Parity
Nat.instDecidablePredOdd : DecidablePred Odd
-- Mathlib.Algebra.Module.SpanRank
Submodule.rank_le_spanRank : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [StrongRankCondition R], Module.rank R M ≤ ⊤.spanRank
-- Mathlib.AlgebraicGeometry.Stalk
AlgebraicGeometry.Scheme.Opens.fromSpecStalkOfMem.eq_1 : ∀ {X : AlgebraicGeometry.Scheme} (U : X.Opens) (x : ↥X) (hxU : x ∈ U),
  U.fromSpecStalkOfMem x hxU =
    CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.Spec.map (CategoryTheory.inv (AlgebraicGeometry.Scheme.Hom.stalkMap U.ι ⟨x, hxU⟩)))
      ((↑U).fromSpecStalk ⟨x, hxU⟩)
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.setIntegral_map : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {μ : MeasureTheory.Measure X} {Y : Type u_5} [inst_2 : MeasurableSpace Y] {g : X → Y} {f : Y → E} {s : Set Y},
  MeasurableSet s →
    MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.map g μ) →
      AEMeasurable g μ → ∫ (y : Y) in s, f y ∂MeasureTheory.Measure.map g μ = ∫ (x : X) in g ⁻¹' s, f (g x) ∂μ
-- Init.Data.SInt.Bitwise
Int16.not_eq_neg_sub : ∀ (a : Int16), ~~~a = -a - 1
-- Std.Time.Date.Unit.Year
Std.Time.Year.instLawfulEqOrdOffset : Std.LawfulEqOrd Std.Time.Year.Offset
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.essImage_yonedaAddGrp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C],
  CategoryTheory.yonedaAddGrp.essImage = fun F => (F.comp (CategoryTheory.forget AddGrpCat)).IsRepresentable
-- Mathlib.Analysis.Normed.Module.RCLike.Extend
/-- If a real-linear functional is bounded by a `𝕜`-seminorm, then its `𝕜`-linear extension
is bounded by the same seminorm.  -/
Module.Dual.norm_extendRCLike_le_seminorm : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] [inst_3 : Module ℝ E]
  [inst_4 : IsScalarTower ℝ 𝕜 E] (fr : Module.Dual ℝ E) {p : Seminorm 𝕜 E},
  (∀ (x : E), |fr x| ≤ p x) → ∀ (x : E), ‖fr.extendRCLike x‖ ≤ p x
-- Mathlib.Algebra.Category.Ring.Constructions
CommRingCat.isPushout_of_isPushout : ∀ (R S A B : Type u) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing A] [inst_3 : CommRing B]
  [inst_4 : Algebra R S] [inst_5 : Algebra S B] [inst_6 : Algebra R A] [inst_7 : Algebra A B] [inst_8 : Algebra R B]
  [inst_9 : IsScalarTower R A B] [inst_10 : IsScalarTower R S B] [Algebra.IsPushout R S A B],
  CategoryTheory.IsPushout (CommRingCat.ofHom (algebraMap R S)) (CommRingCat.ofHom (algebraMap R A))
    (CommRingCat.ofHom (algebraMap S B)) (CommRingCat.ofHom (algebraMap A B))
-- Mathlib.Algebra.Algebra.Unitization
Unitization.inr_add : ∀ (R : Type u_3) {A : Type u_4} [inst : AddZeroClass R] [inst_1 : Add A] (m₁ m₂ : A), ↑(m₁ + m₂) = ↑m₁ + ↑m₂
-- Mathlib.Probability.Kernel.Disintegration.StandardBorel
ProbabilityTheory.Kernel.isRatCondKernelCDFAux_density_Iic : ∀ {α : Type u_1} {γ : Type u_3} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ}
  [inst : MeasurableSpace.CountablyGenerated γ] (κ : ProbabilityTheory.Kernel α (γ × ℝ))
  [ProbabilityTheory.IsFiniteKernel κ],
  ProbabilityTheory.IsRatCondKernelCDFAux (fun p q => κ.density κ.fst p.1 p.2 (Set.Iic ↑q)) κ κ.fst
-- Mathlib.AlgebraicGeometry.Sites.QuasiCompact
AlgebraicGeometry.Scheme.Hom.singleton_mem_qcPrecoverage : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.Surjective f] [AlgebraicGeometry.QuasiCompact f],
  CategoryTheory.Presieve.singleton f ∈ AlgebraicGeometry.Scheme.qcPrecoverage.coverings Y