mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Core
/-- Constructs a new thunk that applies `f` to the result of `x` when forced.
 -/
Thunk.bind : {α : Type u_1} → {β : Type u_2} → Thunk α → (α → Thunk β) → Thunk β
-- Mathlib.CategoryTheory.Monoidal.Comon_
/-- Construct an isomorphism of comonoids by giving an isomorphism between the underlying objects
and checking compatibility with counit and comultiplication only in the forward direction.
 -/
CategoryTheory.Comon.mkIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {M N : CategoryTheory.Comon C} →
        (f : M.X ≅ N.X) →
          autoParam
              (CategoryTheory.CategoryStruct.comp f.hom CategoryTheory.ComonObj.counit = CategoryTheory.ComonObj.counit)
              CategoryTheory.Comon.mkIso._auto_1 →
            autoParam
                (CategoryTheory.CategoryStruct.comp f.hom CategoryTheory.ComonObj.comul =
                  CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.comul
                    (CategoryTheory.MonoidalCategoryStruct.tensorHom f.hom f.hom))
                CategoryTheory.Comon.mkIso._auto_3 →
              (M ≅ N)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMonObj.ofIso_zero : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {M X : C}
  [inst_2 : CategoryTheory.AddMonObj M] (e : M ≅ X),
  CategoryTheory.AddMonObj.zero = CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.zero e.hom
-- Mathlib.Algebra.Category.Grp.Limits
CommGrpCat.instReflectsIsomorphismsGrpCatForget₂MonoidHomCarrierCarrier : (CategoryTheory.forget₂ CommGrpCat GrpCat).ReflectsIsomorphisms
-- Mathlib.Algebra.Star.Basic
symm_starAddEquiv : ∀ {R : Type u} [inst : AddMonoid R] [inst_1 : StarAddMonoid R], starAddEquiv.symm = starAddEquiv
-- Init.Data.Iterators.Basic
Std.Iter.mk.injEq : ∀ {α β : Type w} (internalState internalState_1 : α),
  ({ internalState := internalState } = { internalState := internalState_1 }) = (internalState = internalState_1)
-- Mathlib.RingTheory.OrderOfVanishing.Basic
/-- The order of zero is `Module.length R R`. Use this when it is necessary to unfold the definition
of `ord` to avoid annoyances of working with `R ⧸ Ideal.span {0}` instead of `R`.
 -/
Ring.ord_zero : ∀ (R : Type u_1) [inst : CommRing R], Ring.ord R 0 = Module.length R R
-- Std.Http.Protocol.H1.Event
Std.Http.Protocol.H1.Event.endHeaders.sizeOf_spec : ∀ {dir : Std.Http.Protocol.H1.Direction} (head : Std.Http.Protocol.H1.Message.Head dir),
  sizeOf (Std.Http.Protocol.H1.Event.endHeaders head) = 1 + sizeOf head
-- Batteries.Data.List.Lemmas
List.diff.eq_1 : ∀ {α : Type u_1} [inst : BEq α] (x : List α), x.diff [] = x
-- Std.Time.Zoned.ZoneRules
Std.Time.TimeZone.Transition.mk : Std.Time.Second.Offset → Std.Time.TimeZone.LocalTimeType → Std.Time.TimeZone.Transition
-- Mathlib.Algebra.Group.Irreducible.Lemmas
MulEquiv.irreducible_iff : ∀ {F : Type u_1} {M : Type u_2} {N : Type u_3} [inst : Monoid M] [inst_1 : Monoid N] {x : M} [inst_2 : EquivLike F M N]
  [MulEquivClass F M N] (f : F), Irreducible (f x) ↔ Irreducible x
-- Mathlib.Data.EReal.Operations
/-- `EReal.toENNReal` is multiplicative. For the version with the nonnegativity
hypothesis on the first variable, see `EReal.toENNReal_mul`.  -/
EReal.toENNReal_mul' : ∀ {x y : EReal}, 0 ≤ y → (x * y).toENNReal = x.toENNReal * y.toENNReal
-- Mathlib.CategoryTheory.Extensive
CategoryTheory.FinitaryExtensive.hasFiniteCoproducts : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.FinitaryExtensive C],
  CategoryTheory.Limits.HasFiniteCoproducts C
-- Mathlib.RingTheory.UniqueFactorizationDomain.Basic
MulEquiv.uniqueFactorizationMonoid : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoidWithZero α] [inst_1 : CommMonoidWithZero β] (e : α ≃* β),
  UniqueFactorizationMonoid α → UniqueFactorizationMonoid β
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.Iso.connectedComponentEquiv_apply : ∀ {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (φ : G ≃g G') (C : G.ConnectedComponent),
  φ.connectedComponentEquiv C = SimpleGraph.ConnectedComponent.map (RelIso.toRelEmbedding φ).toRelHom C
-- Mathlib.NumberTheory.Padics.ProperSpace
/-- The set of p-adic integers `ℤ_[p]` is totally bounded.  -/
PadicInt.totallyBounded_univ : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)], TotallyBounded Set.univ
-- Mathlib.LinearAlgebra.BilinearForm.Isometry
/-- The composition of two isometries between bilinear forms.  -/
LinearMap.BilinForm.Isometry.comp : {R : Type u_1} →
  {M₁ : Type u_3} →
    {M₂ : Type u_4} →
      {M₃ : Type u_5} →
        [inst : CommSemiring R] →
          [inst_1 : AddCommMonoid M₁] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : AddCommMonoid M₃] →
                [inst_4 : Module R M₁] →
                  [inst_5 : Module R M₂] →
                    [inst_6 : Module R M₃] →
                      {B₁ : LinearMap.BilinForm R M₁} →
                        {B₂ : LinearMap.BilinForm R M₂} →
                          {B₃ : LinearMap.BilinForm R M₃} → (B₂ →bᵢ B₃) → (B₁ →bᵢ B₂) → B₁ →bᵢ B₃
-- Mathlib.RingTheory.Spectrum.Prime.Basic
/-- The zero locus of a set `s` of elements of a commutative (semi)ring `R` is the set of all
prime ideals of the ring that contain the set `s`.

An element `f` of `R` can be thought of as a dependent function on the prime spectrum of `R`.
At a point `x` (a prime ideal) the function (i.e., element) `f` takes values in the quotient ring
`R` modulo the prime ideal `x`. In this manner, `zeroLocus s` is exactly the subset of
`PrimeSpectrum R` where all "functions" in `s` vanish simultaneously.
 -/
PrimeSpectrum.zeroLocus : {R : Type u} → [inst : CommSemiring R] → Set R → Set (PrimeSpectrum R)
-- Mathlib.Algebra.Module.Equiv.Basic
LinearMap.funLeft_apply : ∀ (R : Type u_1) (M : Type u_5) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {m : Type u_9}
  {n : Type u_10} (f : m → n) (g : n → M) (i : m), (LinearMap.funLeft R M f) g i = g (f i)
-- Mathlib.NumberTheory.Padics.Hensel
_private.Mathlib.NumberTheory.Padics.Hensel.0.soln_unique : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : CommSemiring R] [inst_2 : Algebra R ℤ_[p]]
  {F : Polynomial R} {a : ℤ_[p]}
  (hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2),
  (Polynomial.aeval a) F ≠ 0 →
    ∀ (z : ℤ_[p]),
      (Polynomial.aeval z) F = 0 → ‖z - a‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ → z = soln_gen✝ hnorm
-- Mathlib.Geometry.Convex.ConvexSpace.AffineSpace
AddTorsor.convexCombination_single : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P] (x : P),
  AddTorsor.convexCombination (Convexity.StdSimplex.single x) = x
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.negAddY_smul : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} (P Q : Fin 3 → R) (u v : R),
  W'.negAddY (u • P) (v • Q) = (u * v) ^ 2 * W'.negAddY P Q
-- Mathlib.Data.Nat.PrimeFin
Nat.Coprime.disjoint_primeFactors : ∀ {a b : ℕ}, a.Coprime b → Disjoint a.primeFactors b.primeFactors
-- Init.System.IO
/-- Creates a new hard link.

The `link` path will be a link pointing to the `orig` path.
Note that systems often require these two paths to both be located on the same filesystem.
If `orig` names a symbolic link, it is platform-specific whether the symbolic link is followed.

This function coincides with the [POSIX `link`
function](https://pubs.opengroup.org/onlinepubs/9699919799/functions/link.html).
 -/
IO.FS.hardLink : System.FilePath → System.FilePath → IO Unit
-- Init.PropLemmas
and_imp_right_iff_true : ∀ {P Q : Prop}, P ∧ Q → Q ↔ True
-- Mathlib.CategoryTheory.Limits.Cones
/-- If `H` is an equivalence, we invert `H.mapCone` and get a cone for `F` from a cone
for `F ⋙ H`.  -/
CategoryTheory.Functor.mapConeInv : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {D : Type u₄} →
          [inst_2 : CategoryTheory.Category.{v₄, u₄} D] →
            (H : CategoryTheory.Functor C D) →
              {F : CategoryTheory.Functor J C} →
                [H.IsEquivalence] → CategoryTheory.Limits.Cone (F.comp H) → CategoryTheory.Limits.Cone F
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
/-- We give `Finset α` the measurable structure inherited from `Set α`.

This is the smallest sigma-algebra generated by `(a ∈ ·)` for all `a : α`.
See `measurable_finset_iff`.  -/
Finset.instMeasurableSpace : {α : Type u_1} → MeasurableSpace (Finset α)
-- Lean.Parser.Term
Lean.Parser.Term.noErrorIfUnused.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Lean.DocString.Add
/-- Validates all links to the Lean reference manual in `docstring`.

This is intended to be used before saving a docstring that is later subject to rewriting with
`rewriteManualLinks`.
 -/
Lean.validateDocComment : {m : Type → Type} →
  [Monad m] →
    [MonadLiftT IO m] →
      [Lean.MonadLog m] →
        [Lean.AddMessageContext m] → [Lean.MonadOptions m] → Lean.TSyntax `Lean.Parser.Command.docComment → m Unit
-- Mathlib.Combinatorics.Additive.FreimanHom
IsAddFreimanHom.mapsTo : ∀ {α : Type u_2} {β : Type u_3} [inst : AddCommMonoid α] [inst_1 : AddCommMonoid β] {n : ℕ} {A : Set α} {B : Set β}
  {f : α → β}, IsAddFreimanHom n A B f → Set.MapsTo f A B
-- Mathlib.Order.SuccPred.Limit
Order.not_isPredPrelimit_iff : ∀ {α : Type u_1} [inst : LT α] {a : α}, ¬Order.IsPredPrelimit a ↔ ∃ b, a ⋖ b
-- Mathlib.Data.Bool.Basic
Bool.eq_false_of_not_eq_true' : ∀ {a : Bool}, (!a) = true → a = false
-- Mathlib.LinearAlgebra.BilinearForm.Orthogonal
LinearMap.BilinForm.orthogonal_le : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {B : LinearMap.BilinForm R M} {N L : Submodule R M}, N ≤ L → B.orthogonal L ≤ B.orthogonal N
-- Mathlib.Algebra.Homology.Embedding.Extend
_private.Mathlib.Algebra.Homology.Embedding.Extend.0.HomologicalComplex.extend.d.match_1.splitter : {ι : Type u_1} →
  (motive : Option ι → Option ι → Sort u_2) →
    (x x_1 : Option ι) →
      ((x : Option ι) → motive none x) →
        ((i j : ι) → motive (some i) (some j)) → ((val : ι) → motive (some val) none) → motive x x_1
-- Init.Data.Nat.Lemmas
Nat.one_mod_eq_one : ∀ {n : ℕ}, 1 % n = 1 ↔ n ≠ 1
-- Init.Control.Lawful.MonadLift.Basic
LawfulMonadLiftT.mk : ∀ {m : Type u → Type v} {n : Type u → Type w} [inst : Monad m] [inst_1 : Monad n] [inst_2 : MonadLiftT m n],
  (∀ {α : Type u} (a : α), monadLift (pure a) = pure a) →
    (∀ {α β : Type u} (ma : m α) (f : α → m β),
        monadLift (ma >>= f) = do
          let x ← monadLift ma
          monadLift (f x)) →
      LawfulMonadLiftT m n
-- Init.Data.Int.Gcd
Int.gcd_mul_left_right : ∀ (a b : ℤ), a.gcd (b * a) = a.natAbs
-- Init.SizeOf
Lean.Syntax.missing.sizeOf_spec : sizeOf Lean.Syntax.missing = 1
-- Init.Sym.Simp.SimprocDSL
/-- Maximum depth of recursive discharge attempts.  -/
Lean.Parser.Command.symSimpFieldMaxDischargeDepth : Lean.ParserDescr
-- Mathlib.Algebra.Group.AddChar
/-- If `n` is a natural number, then `ψ ^ n = mulShift ψ n`.  -/
AddChar.pow_mulShift : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : CommMonoid M] (ψ : AddChar R M) (n : ℕ), ψ ^ n = ψ.mulShift ↑n
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
le_mabs_self : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : Group α] (a : α), a ≤ |a|ₘ
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.IsBigO.eq_zero_of_norm_pow_within : ∀ {E'' : Type u_9} {F'' : Type u_10} [inst : NormedAddCommGroup E''] [inst_1 : NormedAddCommGroup F''] {f : E'' → F''}
  {s : Set E''} {x₀ : E''} {n : ℕ}, (f =O[nhdsWithin x₀ s] fun x => ‖x - x₀‖ ^ n) → x₀ ∈ s → n ≠ 0 → f x₀ = 0
-- Mathlib.Data.Sym.Sym2
Sym2.map_congr : ∀ {α : Type u_1} {β : Type u_2} {f g : α → β} {s : Sym2 α}, (∀ x ∈ s, f x = g x) → Sym2.map f s = Sym2.map g s
-- Mathlib.Algebra.Group.Hom.Defs
ZeroHom.mk : {M : Type u_10} → {N : Type u_11} → [inst : Zero M] → [inst_1 : Zero N] → (toFun : M → N) → toFun 0 = 0 → ZeroHom M N
-- Init.Data.String.Lemmas.Pattern.Basic
_private.Init.Data.String.Lemmas.Pattern.Basic.0.String.Slice.Pattern.ToForwardSearcher.DefaultForwardSearcher.instIteratorIdSearchStepOfForwardPattern.match_3.eq_1 : ∀ {ρ : Type} (pat : ρ) (s : String.Slice) (it : Std.IterM Id (String.Slice.Pattern.SearchStep s))
  (motive : Option (s.sliceFrom it.internalState.currPos).Pos → Sort u_1)
  (pos : (s.sliceFrom it.internalState.currPos).Pos)
  (h_1 : (pos_1 : (s.sliceFrom it.internalState.currPos).Pos) → some pos = some pos_1 → motive (some pos_1))
  (h_2 : some pos = none → motive none),
  (match h' : some pos with
    | some pos_1 => h_1 pos_1 h'
    | none => h_2 h') =
    h_1 pos ⋯
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
/-- `SemiNormedGrp₁` is a type synonym for `SemiNormedGrp`,
which we shall equip with the category structure consisting only of the norm non-increasing maps.
 -/
SemiNormedGrp₁ : Type (u + 1)
-- Std.Sat.AIG.LawfulOperator
Std.Sat.AIG.denote.go.congr_simp : ∀ {α : Type} (x x_1 : ℕ) (e_x : x = x_1) (decls decls_1 : Array (Std.Sat.AIG.Decl α)) (e_decls : decls = decls_1)
  (assign assign_1 : α → Bool),
  assign = assign_1 →
    ∀ (h1 : x < decls.size) (h2 : Std.Sat.AIG.IsDAG α decls),
      Std.Sat.AIG.denote.go x decls assign h1 h2 = Std.Sat.AIG.denote.go x_1 decls_1 assign_1 ⋯ ⋯
-- Mathlib.Data.DFinsupp.Order
DFinsupp.instAddLeftReflectLE : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → AddCommMonoid (α i)] [inst_1 : (i : ι) → PartialOrder (α i)]
  [∀ (i : ι), AddLeftReflectLE (α i)], AddLeftReflectLE (Π₀ (i : ι), α i)
-- Mathlib.Order.InitialSeg
InitialSeg.instInhabited : {α : Type u_1} → (r : α → α → Prop) → Inhabited (InitialSeg r r)
-- Mathlib.GroupTheory.ClassEquation
/-- The **class equation** for finite groups. The cardinality of a group is equal to the size
of its center plus the sum of the size of all its nontrivial conjugacy classes.  -/
Group.nat_card_center_add_sum_card_noncenter_eq_card : ∀ (G : Type u_1) [inst : Group G] [Finite G],
  Nat.card ↥(Subgroup.center G) + ∑ᶠ (x : ConjClasses G) (_ : x ∈ ConjClasses.noncenter G), Nat.card ↑x.carrier =
    Nat.card G
-- Mathlib.Algebra.Homology.Double
HomologicalComplex.double.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {X₀ X₁ : C} (f f_1 : X₀ ⟶ X₁),
  f = f_1 →
    ∀ {ι : Type u_2} {c : ComplexShape ι} {i₀ i₀_1 : ι} (e_i₀ : i₀ = i₀_1) {i₁ i₁_1 : ι} (e_i₁ : i₁ = i₁_1)
      (hi₀₁ : c.Rel i₀ i₁), HomologicalComplex.double f hi₀₁ = HomologicalComplex.double f_1 ⋯
-- Init.Grind.Interactive
/-- `dsimp` applies the definitional simplifier to the goal target.
Only available in `sym =>` mode.

- `dsimp` — uses the default (identity) variant
- `dsimp myVariant` — uses a named variant registered via `register_sym_dsimp`
- `dsimp [id₁, id₂, ...]` — default variant with extra declarations to unfold
- `dsimp myVariant [id₁, id₂, ...]` — named variant with extra declarations
 -/
Lean.Parser.Tactic.Grind.symDSimp : Lean.ParserDescr
-- Init.Data.String.Basic
String.Slice.replaceStartEnd : (s : String.Slice) → (newStart newEnd : s.Pos) → newStart ≤ newEnd → String.Slice
-- Init.Data.Vector.OfFn
Vector.getElem?_ofFn : ∀ {i : ℕ} {α : Type u_1} {n : ℕ} {f : Fin n → α}, (Vector.ofFn f)[i]? = if h : i < n then some (f ⟨i, h⟩) else none
-- Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology
CategoryTheory.Functor.instIsDenseSubsiteInducedTopologyOfIsCoverDense : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (G : CategoryTheory.Functor C D)
  (K : CategoryTheory.GrothendieckTopology D) [G.LocallyCoverDense K] [G.IsLocallyFull K] [G.IsLocallyFaithful K]
  [G.IsCoverDense K], CategoryTheory.Functor.IsDenseSubsite (G.inducedTopology K) K G
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.ofDiseqSplit.injEq : ∀ (c₁ : Lean.Meta.Grind.Arith.Linear.DiseqCnstr) (decVar : Lean.FVarId) (h : Lean.Meta.Grind.Arith.Linear.UnsatProof)
  (decVars : Array Lean.FVarId) (c₁_1 : Lean.Meta.Grind.Arith.Linear.DiseqCnstr) (decVar_1 : Lean.FVarId)
  (h_1 : Lean.Meta.Grind.Arith.Linear.UnsatProof) (decVars_1 : Array Lean.FVarId),
  (Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.ofDiseqSplit c₁ decVar h decVars =
      Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.ofDiseqSplit c₁_1 decVar_1 h_1 decVars_1) =
    (c₁ = c₁_1 ∧ decVar = decVar_1 ∧ h = h_1 ∧ decVars = decVars_1)
-- Mathlib.Control.Basic
/-- Like `zipWithM` but evaluates the result as it traverses the lists using `*>`.  -/
zipWithM' : {α β γ : Type u} → {F : Type u → Type v} → [Applicative F] → (α → β → F γ) → List α → List β → F PUnit.{u + 1}
-- Mathlib.CategoryTheory.Shift.Adjunction
CategoryTheory.Adjunction.commShift_of_rightAdjoint : ∀ {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} {G : CategoryTheory.Functor D C}
  (adj : F ⊣ G) (A : Type u_3) [inst_2 : AddGroup A] [inst_3 : CategoryTheory.HasShift C A]
  [inst_4 : CategoryTheory.HasShift D A] [inst_5 : G.CommShift A], adj.CommShift A
-- Lean.ToLevel
/-- A `Level` that represents the universe level `u`.  -/
Lean.ToLevel.toLevel : [self : Lean.ToLevel] → Lean.Level
-- Lean.Data.Json.FromToJson.Basic
Lean.Json.Structured.fromJson? : Lean.Json → Except String Lean.Json.Structured
-- Mathlib.CategoryTheory.Limits.WeakLimits.WeakEqualizers
CategoryTheory.Limits.weakEqualizer.lift_ι_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} {f g : X ⟶ Y}
  [inst_1 : CategoryTheory.Limits.HasWeakEqualizer f g] {W : C} (k : W ⟶ X)
  (h : CategoryTheory.CategoryStruct.comp k f = CategoryTheory.CategoryStruct.comp k g) {Z : C} (h_1 : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.weakEqualizer.lift k h)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.weakEqualizer.ι f g) h_1) =
    CategoryTheory.CategoryStruct.comp k h_1
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.CoordinateRing.degree_norm_smul_basis : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Affine R} [IsDomain R] (p q : Polynomial R),
  ((Algebra.norm (Polynomial R)) (p • 1 + q • (WeierstrassCurve.Affine.CoordinateRing.mk W') Polynomial.X)).degree =
    max (2 • p.degree) (2 • q.degree + 3)
-- Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin
ContinuousAlternatingMap.alternatizeUncurryFinCLM.eq_1 : ∀ (𝕜 : Type u_1) (E : Type u_2) (F : Type u_3) [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : ℕ},
  ContinuousAlternatingMap.alternatizeUncurryFinCLM 𝕜 E F =
    AlternatingMap.mkContinuousLinear ContinuousAlternatingMap.alternatizeUncurryFinCLM.aux✝ (↑n + 1) ⋯
-- Mathlib.Algebra.GroupWithZero.Action.Defs
DistribMulAction.toMulAction : {M : Type u_12} →
  {A : Type u_13} → {inst : Monoid M} → {inst_1 : AddMonoid A} → [self : DistribMulAction M A] → MulAction M A
-- Mathlib.CategoryTheory.Shift.CommShift
CategoryTheory.NatTrans.app_shift_assoc : ∀ {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₁ F₂ : CategoryTheory.Functor C D} (τ : F₁ ⟶ F₂) {A : Type u_5}
  [inst_2 : AddMonoid A] [inst_3 : CategoryTheory.HasShift C A] [inst_4 : CategoryTheory.HasShift D A]
  [inst_5 : F₁.CommShift A] [inst_6 : F₂.CommShift A] [CategoryTheory.NatTrans.CommShift τ A] (a : A) (X : C) {Z : D}
  (h : F₂.obj ((CategoryTheory.shiftFunctor C a).obj X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (τ.app ((CategoryTheory.shiftFunctor C a).obj X)) h =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso F₁ a).hom.app X)
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D a).map (τ.app X))
        (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso F₂ a).inv.app X) h))
-- Mathlib.Order.Interval.Set.Pi
Set.image_update_uIcc_left : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Lattice (α i)] [inst_1 : DecidableEq ι] (f : (i : ι) → α i)
  (i : ι) (a : α i), Function.update f i '' Set.uIcc a (f i) = Set.uIcc (Function.update f i a) f
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.single_eq_same : ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → Zero (β i)] [inst_1 : DecidableEq ι] {i : ι} {b : β i},
  (fun₀ | i => b) i = b
-- Mathlib.LinearAlgebra.TensorProduct.Tower
Submodule.baseChange_top : ∀ {R : Type u_1} {M : Type u_2} (A : Type u_3) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M], Submodule.baseChange A ⊤ = ⊤
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.combine_mul_k'.eq_1 : ∀ (fuel : ℕ) (a b : ℤ),
  Int.Internal.Linear.Poly.combine_mul_k' fuel a b =
    Nat.rec (motive := fun x => Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → Int.Internal.Linear.Poly)
      (fun p₁ p₂ => (p₁.mul a).append (p₂.mul b))
      (fun x ih p₁ =>
        Int.Internal.Linear.Poly.rec (motive := fun x => Int.Internal.Linear.Poly → Int.Internal.Linear.Poly)
          (fun k₁ p₂ =>
            Int.Internal.Linear.Poly.rec (fun k₂ => Int.Internal.Linear.Poly.num ((a.mul k₁).add (b.mul k₂)))
              (fun a₂ x₂ p₂ x => Int.Internal.Linear.Poly.add (b.mul a₂) x₂ (ih p₁ p₂)) p₂)
          (fun a₁ x₁ p₁ x p₂ =>
            Int.Internal.Linear.Poly.rec (fun x => Int.Internal.Linear.Poly.add (a.mul a₁) x₁ (ih p₁ p₂))
              (fun a₂ x₂ p₂ x =>
                Bool.rec
                  (Bool.rec (Int.Internal.Linear.Poly.add (b.mul a₂) x₂ (ih (Int.Internal.Linear.Poly.add a₁ x₁ p₁) p₂))
                    (Int.Internal.Linear.Poly.add (a.mul a₁) x₁ (ih p₁ (Int.Internal.Linear.Poly.add a₂ x₂ p₂)))
                    (Nat.blt x₂ x₁))
                  (have a := (a.mul a₁).add (b.mul a₂);
                  Bool.rec (Int.Internal.Linear.Poly.add a x₁ (ih p₁ p₂)) (ih p₁ p₂) (a.beq' 0))
                  (Nat.beq x₁ x₂))
              p₂)
          p₁)
      fuel
-- Mathlib.CategoryTheory.MorphismProperty.CommaSites
CategoryTheory.MorphismProperty.locallyCoverDense_forget_of_le : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.MorphismProperty C} {S : C}
  [P.IsStableUnderComposition] (K : CategoryTheory.Precoverage C) [K.HasIsos] [K.IsStableUnderBaseChange]
  [K.IsStableUnderComposition] [K.HasPullbacks],
  K ≤ P.precoverage → (CategoryTheory.MorphismProperty.Over.forget P ⊤ S).LocallyCoverDense (K.toGrothendieck.over S)
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.IsAffineOpen.toSpecΓ_isoSpec_inv_assoc : ∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U) {Z : AlgebraicGeometry.Scheme}
  (h : ↑U ⟶ Z), CategoryTheory.CategoryStruct.comp U.toSpecΓ (CategoryTheory.CategoryStruct.comp hU.isoSpec.inv h) = h
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
Subsemigroup.unop.eq_1 : ∀ {M : Type u_2} [inst : Mul M] (x : Subsemigroup Mᵐᵒᵖ), x.unop = { carrier := MulOpposite.op ⁻¹' ↑x, mul_mem' := ⋯ }
-- Mathlib.Algebra.GroupWithZero.Basic
right_ne_zero_of_mul_eq_one : ∀ {M₀ : Type u_1} [inst : MulZeroOneClass M₀] [Nontrivial M₀] {a b : M₀}, a * b = 1 → b ≠ 0
-- Mathlib.Algebra.Order.IsBotOne
/-- **Alias** of `eq_one_of_le_one`.

---

**Alias** of the forward direction of `le_one_iff_eq_one`. -/
LE.le.eq_one : ∀ {α : Type u_1} {a : α} [inst : PartialOrder α] [inst_1 : One α] [IsBotOneClass α], a ≤ 1 → a = 1
-- Init.Data.Ord.Basic
Ordering.then_eq : ∀ {o : Ordering}, o.then Ordering.eq = o