mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Abelian.Injective.Extend
CategoryTheory.InjectiveResolution.cochainComplexXIso.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Preadditive C] {X : C} (R : CategoryTheory.InjectiveResolution X) (n : ℤ) (k : ℕ)
  (h : ↑k = n), R.cochainComplexXIso n k h = HomologicalComplex.extendXIso R.cocomplex ComplexShape.embeddingUpNat h
-- Mathlib.Data.Rat.Cast.CharZero
Rat.cast_eq_zero : ∀ {α : Type u_3} [inst : DivisionRing α] [CharZero α] {p : ℚ}, ↑p = 0 ↔ p = 0
-- Std.Sync.RecursiveMutex
Std.instCoeOutRecursiveMutexBaseRecursiveMutex : {α : Type} → CoeOut (Std.RecursiveMutex α) Std.BaseRecursiveMutex
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instZero : {α : Type u_1} → [Zero α] → Zero αᵒᵈ
-- Lean.Data.DeclarationRange
Lean.DeclarationRanges : Type
-- Mathlib.GroupTheory.SpecificGroups.ZGroup
/-- If a cyclic `p`-subgroup `P` acts by conjugation on a subgroup `K` of coprime order, then
either `⁅K, P⁆ = ⊥` or `⁅K, P⁆ = P`.  -/
IsPGroup.commutator_eq_bot_or_commutator_eq_self : ∀ {G : Type u_1} [inst : Group G] {p : ℕ} [Fact (Nat.Prime p)] {P K : Subgroup G} [IsCyclic ↥P],
  IsPGroup p ↥P → K ≤ Subgroup.normalizer ↑P → (Nat.card ↥P).Coprime (Nat.card ↥K) → ⁅K, P⁆ = ⊥ ∨ ⁅K, P⁆ = P
-- Mathlib.Algebra.Category.ModuleCat.Adjunctions
CategoryTheory.Free.single_comp_single : ∀ (R : Type u_1) [inst : CommRing R] (C : Type u) [inst_1 : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y)
  (g : Y ⟶ Z) (r s : R),
  (CategoryTheory.CategoryStruct.comp (fun₀ | f => r) fun₀ | g => s) =
    fun₀ | CategoryTheory.CategoryStruct.comp f g => r * s
-- Init.Data.SInt.Lemmas
Int32.sub_self : ∀ (a : Int32), a - a = 0
-- Mathlib.Algebra.Homology.ShortComplex.ShortExact
CategoryTheory.ShortComplex.ShortExact.op : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C}, S.ShortExact → S.op.ShortExact
-- Std.Data.HashSet.Lemmas
Std.HashSet.all_eq_not_any_not : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} {p : α → Bool}, m.all p = !m.any fun a => !p a
-- Mathlib.AlgebraicGeometry.Limits
AlgebraicGeometry.coprodSpec_apply : ∀ (R S : Type u) [inst : CommRing R] [inst_1 : CommRing S]
  (x : ↥(AlgebraicGeometry.Spec (CommRingCat.of R) ⨿ AlgebraicGeometry.Spec (CommRingCat.of S))),
  (AlgebraicGeometry.coprodSpec R S) x =
    (PrimeSpectrum.primeSpectrumProd R S).symm
      ((AlgebraicGeometry.coprodMk (AlgebraicGeometry.Spec (CommRingCat.of R))
            (AlgebraicGeometry.Spec (CommRingCat.of S))).symm
        x)
-- Mathlib.CategoryTheory.Functor.Currying
CategoryTheory.Functor.flipping_functor_obj_map_app : ∀ {C : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} D]
  {E : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} E]
  (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) {X Y : D} (f : X ⟶ Y) (j : C),
  ((CategoryTheory.Functor.flipping.functor.obj F).map f).app j = (F.obj j).map f
-- Mathlib.GroupTheory.Index
/-- An additive subgroup has index dividing 2 if and only if there exists `a` such
that for all `b`, at least one of `a + b` and `b` belongs to `H`.  -/
AddSubgroup.index_dvd_two_iff' : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G}, H.index ∣ 2 ↔ ∃ a, ∀ (b : G), a + b ∈ H ∨ b ∈ H
-- Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
/-- A type synonym for families of polynomials. This is used in the induction for the case of
`C : R → R[X]` of Chevalley's theorem with complexity bound.  -/
_private.Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity.0.ChevalleyThm.PolynomialC.InductionObj : (R : Type u_2) → [CommRing R] → ℕ → Type u_2
-- Mathlib.MeasureTheory.VectorMeasure.Basic
/-- The equiv between `VectorMeasure α ℝ≥0∞` and `Measure α` formed by
`MeasureTheory.VectorMeasure.ennrealToMeasure` and
`MeasureTheory.Measure.toENNRealVectorMeasure`.  -/
MeasureTheory.VectorMeasure.equivMeasure : {α : Type u_1} → [inst : MeasurableSpace α] → MeasureTheory.VectorMeasure α ENNReal ≃ MeasureTheory.Measure α
-- Mathlib.AlgebraicGeometry.AffineTransitionLimit
/-- Suppose `{ Xᵢ }` is an inverse system of qcqs schemes with affine transition maps.
Then any affine open cover of `lim Xᵢ` comes from a finite level.  -/
AlgebraicGeometry.Scheme.exists_isOpenCover_and_isAffine : ∀ {I : Type u} [inst : CategoryTheory.Category.{u, u} I] (D : CategoryTheory.Functor I AlgebraicGeometry.Scheme)
  (c : CategoryTheory.Limits.Cone D) (hc : CategoryTheory.Limits.IsLimit c) [CategoryTheory.IsCofiltered I]
  [∀ {i j : I} (f : i ⟶ j), AlgebraicGeometry.IsAffineHom (D.map f)] [∀ (i : I), CompactSpace ↥(D.obj i)]
  [∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)] {J : Type u_1} (U : J → c.pt.Opens),
  TopologicalSpace.IsOpenCover U →
    (∀ (i : J), AlgebraicGeometry.IsAffineOpen (U i)) →
      ∃ i s V,
        TopologicalSpace.IsOpenCover V ∧
          ∀ (j : ↥s),
            AlgebraicGeometry.IsAffineOpen (V j) ∧ U ↑j = (TopologicalSpace.Opens.map (c.π.app i).base).obj (V j)
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
IsPrimitiveRoot.mk_of_lt : ∀ {M : Type u_1} [inst : CommMonoid M] {k : ℕ} (ζ : M),
  0 < k → ζ ^ k = 1 → (∀ (l : ℕ), 0 < l → l < k → ζ ^ l ≠ 1) → IsPrimitiveRoot ζ k
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.denote_mul_nc : ∀ {α : Type u_1} [inst : Lean.Grind.Ring α] (ctx : Lean.Grind.CommRing.Context α) (p₁ p₂ : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Poly.denote ctx (p₁.mul_nc p₂) =
    Lean.Grind.CommRing.Poly.denote ctx p₁ * Lean.Grind.CommRing.Poly.denote ctx p₂
-- Mathlib.Algebra.Homology.ModelCategory.Injective
CochainComplex.Plus.modelCategoryQuillen.instHasLiftingPropertyOfMonoOfWeakEquivalenceOfFibration : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {A B X Y : CochainComplex.Plus C} (i : A ⟶ B) (p : X ⟶ Y) [CategoryTheory.Mono i]
  [HomotopicalAlgebra.WeakEquivalence i] [HomotopicalAlgebra.Fibration p], CategoryTheory.HasLiftingProperty i p
-- Mathlib.CategoryTheory.ObjectProperty.Shift
CategoryTheory.ObjectProperty.shiftClosure_top : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A : Type u_2} [inst_1 : AddMonoid A]
  [inst_2 : CategoryTheory.HasShift C A], ⊤.shiftClosure A = ⊤
-- Mathlib.Algebra.Group.Action.Defs
vadd_assoc : ∀ {α : Type u_5} {M : Type u_9} {N : Type u_10} [inst : VAdd M N] [inst_1 : VAdd N α] [inst_2 : VAdd M α]
  [VAddAssocClass M N α] (x : M) (y : N) (z : α), (x +ᵥ y) +ᵥ z = x +ᵥ y +ᵥ z
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cochain.d_comp_ofHom_v : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) (p' p q : ℤ) (hpq : p + 0 = q),
  CategoryTheory.CategoryStruct.comp (F.d p' p) ((CochainComplex.HomComplex.Cochain.ofHom φ).v p q hpq) =
    CategoryTheory.CategoryStruct.comp (F.d p' q) (φ.f q)
-- Lean.Meta.CongrTheorems
/-- Creates a congruence theorem that is useful for the simplifier and `congr` tactic.
 -/
Lean.Meta.mkCongrSimpCore? : Lean.Expr →
  Lean.Meta.FunInfo → Array Lean.Meta.CongrArgKind → optParam Bool true → Lean.MetaM (Option Lean.Meta.CongrTheorem)
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroup.ofClass.eq_1 : ∀ {S : Type u_3} {G : Type u_4} [inst : AddGroup G] [inst_1 : SetLike S G] [inst_2 : AddSubgroupClass S G] (s : S),
  AddSubgroup.ofClass s = { carrier := ↑s, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }
-- Mathlib.Data.Int.Bitwise
Int.bit_negSucc : ∀ (b : Bool) (n : ℕ), Int.bit b (Int.negSucc n) = Int.negSucc (Nat.bit (!b) n)
-- Mathlib.FieldTheory.PolynomialGaloisGroup
Polynomial.Gal.galActionHom_restrict : ∀ {F : Type u_1} [inst : Field F] (p : Polynomial F) (E : Type u_2) [inst_1 : Field E] [inst_2 : Algebra F E]
  [inst_3 : Fact (Polynomial.map (algebraMap F E) p).Splits] (ϕ : Gal(E/F)) (x : ↑(p.rootSet E)),
  ↑(((Polynomial.Gal.galActionHom p E) ((Polynomial.Gal.restrict p E) ϕ)) x) = ϕ ↑x
-- Mathlib.Algebra.Order.Interval.Set.Instances
Set.Icc.instPow : {R : Type u_1} → [inst : Semiring R] → [inst_1 : PartialOrder R] → [IsOrderedRing R] → Pow ↑(Set.Icc 0 1) ℕ
-- Mathlib.LinearAlgebra.CliffordAlgebra.Basic
/-- A version of `mul_mul_mul_comm` for `ι`.  -/
CliffordAlgebra.mul_ι_mul_ι_mul_comm : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} (x : CliffordAlgebra Q) (a b : M) (y : CliffordAlgebra Q),
  x * (CliffordAlgebra.ι Q) a * ((CliffordAlgebra.ι Q) b * y) =
    (algebraMap R (CliffordAlgebra Q)) (QuadraticMap.polar (⇑Q) a b) * (x * y) -
      x * (CliffordAlgebra.ι Q) b * ((CliffordAlgebra.ι Q) a * y)
-- Mathlib.FieldTheory.IsSepClosed
IsSepClosed.exists_eval₂_eq_zero_of_injective : ∀ {K : Type v} [inst : Field K] {k : Type u_1} [inst_1 : CommSemiring k] [IsSepClosed K] (f : k →+* K),
  Function.Injective ⇑f → ∀ (p : Polynomial k), p.degree ≠ 0 → p.Separable → ∃ x, Polynomial.eval₂ f x p = 0
-- Mathlib.CategoryTheory.Limits.Fubini
/-- The Fubini theorem for a functor `F : J ⥤ K ⥤ C`,
showing that the limit of `uncurry.obj F` can be computed as
the limit of the limits of the functors `F.obj j`.
 -/
CategoryTheory.Limits.limitUncurryIsoLimitCompLim : {J : Type u_1} →
  {K : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} J] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} K] →
        {C : Type u_3} →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} C] →
            (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) →
              [inst_3 : CategoryTheory.Limits.HasLimitsOfShape K C] →
                [inst_4 : CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.uncurry.obj F)] →
                  [inst_5 : CategoryTheory.Limits.HasLimit (F.comp CategoryTheory.Limits.lim)] →
                    CategoryTheory.Limits.limit (CategoryTheory.Functor.uncurry.obj F) ≅
                      CategoryTheory.Limits.limit (F.comp CategoryTheory.Limits.lim)
-- Mathlib.MeasureTheory.Measure.Support
/-- A point `x` is in the support of measure `μ` iff every neighborhood of `x` has positive
measure.  -/
MeasureTheory.Measure.mem_support_iff_forall : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] {μ : MeasureTheory.Measure X} (x : X),
  x ∈ μ.support ↔ ∀ U ∈ nhds x, 0 < μ U
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
MeasureTheory.integrableOn_condExpL2_of_measure_ne_top : ∀ {α : Type u_1} {E : Type u_2} {𝕜 : Type u_7} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : CompleteSpace E] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {s : Set α} (hm : m ≤ m0),
  μ s ≠ ⊤ → ∀ (f : ↥(MeasureTheory.Lp E 2 μ)), MeasureTheory.IntegrableOn (↑↑↑((MeasureTheory.condExpL2 E 𝕜 hm) f)) s μ
-- Mathlib.Algebra.Field.Defs
/-- Scalar multiplication by a rational number.

Unless there is a risk of a `Module ℚ _` instance diamond, write `qsmul := _`. This will set
`qsmul` to `(Rat.cast · * ·)` thanks to unification in the default proof of `qsmul_def`.

Do not use directly. Instead use the `•` notation.  -/
Field.qsmul : {K : Type u} → [self : Field K] → ℚ → K → K
-- Mathlib.Algebra.DirectSum.Algebra
DirectSum.GAlgebra.map_mul : ∀ {ι : Type uι} {R : Type uR} {A : ι → Type uA} {inst : CommSemiring R} {inst_1 : (i : ι) → AddCommMonoid (A i)}
  {inst_2 : (i : ι) → Module R (A i)} {inst_3 : AddMonoid ι} {inst_4 : DirectSum.GSemiring A}
  [self : DirectSum.GAlgebra R A] (r s : R),
  GradedMonoid.mk 0 (DirectSum.GAlgebra.toFun (r * s)) =
    GradedMonoid.mk (0 + 0) (GradedMonoid.GMul.mul (DirectSum.GAlgebra.toFun r) (DirectSum.GAlgebra.toFun s))
-- Init.Data.List.Notation
/-- The syntax `[a, b, c]` is shorthand for `a :: b :: c :: []`, or
`List.cons a (List.cons b (List.cons c List.nil))`. It allows conveniently constructing
list literals.

For lists of length at least 64, an alternative desugaring strategy is used
which uses let bindings as intermediates as in
`let left := [d, e, f]; a :: b :: c :: left` to avoid creating very deep expressions.
Note that this changes the order of evaluation, although it should not be observable
unless you use side effecting operations like `dbg_trace`.


Conventions for notations in identifiers:

 * The recommended spelling of `[]` in identifiers is `nil`.

 * The recommended spelling of `[a]` in identifiers is `singleton`. -/
«term[_]» : Lean.ParserDescr
-- Mathlib.CategoryTheory.Functor.CurryingThree
/-- Uncurrying a functor in three variables.  -/
CategoryTheory.Functor.uncurry₃ : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {C₃ : Type u_4} →
      {E : Type u_9} →
        [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
          [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
            [inst_2 : CategoryTheory.Category.{v_3, u_4} C₃] →
              [inst_3 : CategoryTheory.Category.{v_9, u_9} E] →
                CategoryTheory.Functor
                  (CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ E)))
                  (CategoryTheory.Functor (C₁ × C₂ × C₃) E)
-- Mathlib.Order.Monotone.Basic
List.foldl_monotone : ∀ {α : Type u} {β : Type v} [inst : Preorder α] {f : α → β → α},
  (∀ (b : β), Monotone fun a => f a b) → ∀ (l : List β), Monotone fun a => List.foldl f a l
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get?_eq_some_get! : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited β] {a : α}, a ∈ t → Std.DTreeMap.Const.get? t a = some (Std.DTreeMap.Const.get! t a)
-- LeanSearchClient.LoogleSyntax
LeanSearchClient.loogleCache : IO.Ref (Std.HashMap (String × ℕ) LeanSearchClient.LoogleResult)
-- Lean.DocString.Types
/-- Strong emphasis, typically rendered using bold text.
 -/
Lean.Doc.Inline.bold : {i : Type u} → Array (Lean.Doc.Inline i) → Lean.Doc.Inline i
-- Mathlib.Order.Hom.Basic
OrderIso.ofSurjective_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : LE α] [inst_1 : LE β] (f : α ↪o β) (hf : Function.Surjective ⇑f) (a : α),
  (OrderIso.ofSurjective f hf) a = f a
-- Mathlib.Analysis.Normed.Algebra.GelfandMazur
/-- A version of the **Gelfand-Mazur Theorem** for nontrivial normed `ℂ`-algebras `F`
with multiplicative norm: any such `F` is isomorphic to `ℂ` as a `ℂ`-algebra.  -/
NormedAlgebra.Complex.nonempty_algEquiv : ∀ (F : Type u_1) [inst : NormedRing F] [NormOneClass F] [NormMulClass F] [inst_3 : NormedAlgebra ℂ F] [Nontrivial F],
  Nonempty (ℂ ≃ₐ[ℂ] F)
-- Mathlib.Topology.EMetricSpace.BoundedVariation
/-- If a function has bounded variation, then the variation on semi-infinite closed
intervals tends to `0` at `-∞`.  -/
BoundedVariationOn.tendsto_eVariationOn_Iic_zero : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] {f : α → E} {s : Set α},
  BoundedVariationOn f s →
    Filter.Tendsto (fun y => eVariationOn f (s ∩ Set.Iic y)) (Filter.principal s ⊓ Filter.atBot) (nhds 0)
-- Lean.Data.Lsp.Basic
Lean.Lsp.MarkupContent.mk.injEq : ∀ (kind : Lean.Lsp.MarkupKind) (value : String) (kind_1 : Lean.Lsp.MarkupKind) (value_1 : String),
  ({ kind := kind, value := value } = { kind := kind_1, value := value_1 }) = (kind = kind_1 ∧ value = value_1)
-- Mathlib.Algebra.Group.Submonoid.Support
/-- A submonoid is pointed if it has zero support.  -/
AddSubmonoid.IsPointed : {G : Type u_1} → [inst : AddGroup G] → AddSubmonoid G → Prop
-- Mathlib.Topology.ContinuousMap.BoundedCompactlySupported
norm_lt_iff_of_nonempty_compactlySupported : ∀ {α : Type u_1} {γ : Type u_2} [inst : TopologicalSpace α] [inst_1 : NonUnitalNormedRing γ] [c : Nonempty α]
  {f : BoundedContinuousFunction α γ}, f ∈ compactlySupported α γ → ∀ {M : ℝ}, ‖f‖ < M ↔ ∀ (x : α), ‖f x‖ < M
-- Mathlib.CategoryTheory.Center.Basic
CategoryTheory.CatCenter.smul_iso_inv_eq' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (z : (CategoryTheory.CatCenter C)ˣ) {X Y : C} (f : X ≅ Y),
  (z • f).inv = CategoryTheory.CategoryStruct.comp ((↑z⁻¹).app Y) f.inv
-- Init.Data.List.Lemmas
_private.Init.Data.List.Lemmas.0.List.flatten.match_1.splitter : {α : Type u_1} →
  (motive : List (List α) → Sort u_2) →
    (x : List (List α)) → (Unit → motive []) → ((l : List α) → (L : List (List α)) → motive (l :: L)) → motive x
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.mulConst.go : ℤ → Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly
-- Mathlib.Algebra.Category.MonCat.Basic
CommMonCat.hom_ext : ∀ {M N : CommMonCat} {f g : M ⟶ N}, CommMonCat.Hom.hom f = CommMonCat.Hom.hom g → f = g
-- Mathlib.Probability.Martingale.Centering
MeasureTheory.Submartingale.monotone_predictablePart : ∀ {Ω : Type u_1} {E : Type u_2} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] {f : ℕ → Ω → E} {ℱ : MeasureTheory.Filtration ℕ m0} [CompleteSpace E]
  [inst_3 : PartialOrder E] [IsOrderedAddMonoid E],
  MeasureTheory.Submartingale f ℱ μ → ∀ᵐ (ω : Ω) ∂μ, Monotone fun x => MeasureTheory.predictablePart f ℱ μ x ω
-- Mathlib.Order.RelSeries
LTSeries.monotone : ∀ {α : Type u_1} [inst : Preorder α] (x : LTSeries α), Monotone x.toFun
-- Mathlib.RingTheory.Extension.Presentation.Submersive
Algebra.PreSubmersivePresentation.map_inj : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (self : Algebra.PreSubmersivePresentation R S ι σ), Function.Injective self.map
-- Mathlib.RingTheory.Extension.Cotangent.Basic
Algebra.Extension.Hom.sub_tmul : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {P : Algebra.Extension R S}
  {R' : Type u'} {S' : Type v'} [inst_3 : CommRing R'] [inst_4 : CommRing S'] [inst_5 : Algebra R' S']
  {P' : Algebra.Extension R' S'} [inst_6 : Algebra R R'] [inst_7 : Algebra S S'] [inst_8 : Algebra R S']
  [inst_9 : IsScalarTower R R' S'] [inst_10 : IsScalarTower R S S'] (f g : P.Hom P') (r : S) (x : P.Ring),
  (f.sub g) (r ⊗ₜ[P.Ring] (KaehlerDifferential.D R P.Ring) x) = r • Algebra.Extension.Cotangent.mk ((f.subToKer g) x)
-- Mathlib.Order.Heyting.Basic
sdiff_le_iff : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] {a b c : α}, a \ b ≤ c ↔ a ≤ b ⊔ c
-- Mathlib.Logic.Equiv.Prod
Equiv.prodCongrRight_trans_prodComm : ∀ {α₁ : Type u_9} {β₁ : Type u_11} {β₂ : Type u_12} (e : α₁ → β₁ ≃ β₂),
  (Equiv.prodCongrRight e).trans (Equiv.prodComm α₁ β₂) = (Equiv.prodComm α₁ β₁).trans (Equiv.prodCongrLeft e)
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F.unop : C ⥤ D` creates colimits of `K.leftOp : Jᵒᵖ ⥤ C`, then `F : Cᵒᵖ ⥤ Dᵒᵖ` creates
limits of `K : J ⥤ Cᵒᵖ`.  -/
CategoryTheory.Limits.createsLimitOfUnop : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : Type w} →
          [inst_2 : CategoryTheory.Category.{w', w} J] →
            (K : CategoryTheory.Functor J Cᵒᵖ) →
              (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) →
                [CategoryTheory.CreatesColimit K.leftOp F.unop] → CategoryTheory.CreatesLimit K F
-- Mathlib.GroupTheory.Submonoid.Inverses
/-- The `MonoidHom` from `S.leftInv` to `S` sending an element to its right inverse in `S`.  -/
Submonoid.fromCommLeftInv : {M : Type u_1} → [inst : CommMonoid M] → (S : Submonoid M) → ↥S.leftInv →* ↥S
-- Mathlib.CategoryTheory.Square
/-- The functor `Square C ⥤ Square D` induced by a functor `C ⥤ D`.  -/
CategoryTheory.Functor.mapSquare : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} D] →
        CategoryTheory.Functor C D → CategoryTheory.Functor (CategoryTheory.Square C) (CategoryTheory.Square D)
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LetValue.updateReuse! : {pu : Lean.Compiler.LCNF.Purity} →
  Lean.Compiler.LCNF.LetValue pu →
    Lean.FVarId →
      Lean.Compiler.LCNF.CtorInfo → Bool → Array (Lean.Compiler.LCNF.Arg pu) → Lean.Compiler.LCNF.LetValue pu
-- Mathlib.Data.Vector.Zip
List.Vector.zipWith_tail : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : ℕ} (f : α → β → γ) (x : List.Vector α n) (y : List.Vector β n),
  (List.Vector.zipWith f x y).tail = List.Vector.zipWith f x.tail y.tail
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.DBuilderName.regular.sizeOf_spec : ∀ (b : Aesop.BuilderName), sizeOf (Aesop.Frontend.DBuilderName.regular b) = 1 + sizeOf b
-- Mathlib.Control.Bitraversable.Instances
instLawfulBitraversableSum : LawfulBitraversable Sum
-- Mathlib.Analysis.Calculus.FDeriv.Bilinear
IsBoundedBilinearMap.differentiableWithinAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {b : E × F → G} {u : Set (E × F)},
  IsBoundedBilinearMap 𝕜 b → ∀ (p : E × F), DifferentiableWithinAt 𝕜 b u p
-- Mathlib.Control.Monad.Cont
instMonadContOptionT : {m : Type u → Type v} → [Monad m] → [MonadCont m] → MonadCont (OptionT m)
-- Mathlib.Tactic.NormNum.Core
_private.Mathlib.Tactic.NormNum.Core.0.Mathlib.Meta.NormNum.mkNormNumExt.unsafe_1 : Lean.Name → Lean.Environment → Lean.Options → ExceptT String Id Mathlib.Meta.NormNum.NormNumExt
-- Mathlib.Order.Hom.Lattice
InfHom.subtypeVal_coe : ∀ {β : Type u_3} [inst : SemilatticeInf β] {P : β → Prop} (Pinf : ∀ ⦃x y : β⦄, P x → P y → P (x ⊓ y)),
  ⇑(InfHom.subtypeVal Pinf) = Subtype.val
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
/-- The set in the `lsub` characterization of `cof` is nonempty.  -/
Ordinal.cof_lsub_def_nonempty : ∀ (o : Ordinal.{u}), {a | ∃ ι f, Ordinal.lsub f = o ∧ Cardinal.mk ι = a}.Nonempty
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Over
/-- The pullback of a monoid object is a monoid object.  -/
CategoryTheory.Over.grpObjMkPullbackSnd : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasPullbacks C] →
      {X R S : C} →
        {f : R ⟶ X} →
          {g : S ⟶ X} →
            [CategoryTheory.GrpObj (CategoryTheory.Over.mk f)] →
              CategoryTheory.GrpObj (CategoryTheory.Over.mk (CategoryTheory.Limits.pullback.snd f g))
-- Mathlib.Topology.Order.Hom.Basic
/-- The type of continuous monotone maps from `α` to `β`, aka Priestley homomorphisms.  -/
«term_→Co_» : Lean.TrailingParserDescr
-- Mathlib.RingTheory.Polynomial.HilbertPoly
Polynomial.hilbertPoly.eq_2 : ∀ {F : Type u_1} [inst : Field F] (p : Polynomial F) (d : ℕ),
  p.hilbertPoly d.succ = ∑ i ∈ p.support, p.coeff i • Polynomial.preHilbertPoly F d i
-- Mathlib.Order.BoundedOrder.Lattice
min_eq_top : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : OrderTop α] {a b : α}, min a b = ⊤ ↔ a = ⊤ ∧ b = ⊤
-- Init.Data.UInt.Lemmas
UInt8.two_mul : ∀ {a : UInt8}, 2 * a = a + a
-- Mathlib.CategoryTheory.Monoidal.Mod
/-- **Alias** of `CategoryTheory.Mod.id_hom'`. -/
CategoryTheory.Mod_.id_hom' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D]
  {A : C} [inst_4 : CategoryTheory.MonObj A] (M : CategoryTheory.Mod D A),
  (CategoryTheory.CategoryStruct.id M).hom = CategoryTheory.CategoryStruct.id M.X
-- Std.Data.DTreeMap.Internal.Operations
/-- Slower version of `getThenInsertIfNew?` which can be used in the absence of balance
information but still assumes the preconditions of `getThenInsertIfNew?`, otherwise might panic.
 -/
Std.DTreeMap.Internal.Impl.Const.getThenInsertIfNew?! : {α : Type u} →
  {β : Type v} →
    [Ord α] → (Std.DTreeMap.Internal.Impl α fun x => β) → α → β → Option β × Std.DTreeMap.Internal.Impl α fun x => β