mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.KrullDimension
/-- Alternative definition of coheight, with the supremum only ranging over those series
that begin at `a`.
 -/
Order.coheight_eq_iSup_head_eq : ∀ {α : Type u_1} [inst : Preorder α] (a : α), Order.coheight a = ⨆ p, ⨆ (_ : RelSeries.head p = a), ↑p.length
-- Mathlib.Algebra.Group.Units.Defs
/-- Units of a monoid form a group.  -/
Units.instGroup : {α : Type u} → [inst : Monoid α] → Group αˣ
-- Init.Data.Int.Order
Int.lt_add_of_neg_add_lt_right : ∀ {a b c : ℤ}, -c + a < b → a < b + c
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
TensorProduct.inner_mapIncl_mapIncl : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F] (E' : Submodule 𝕜 E)
  (F' : Submodule 𝕜 F) (x y : TensorProduct 𝕜 ↥E' ↥F'),
  inner 𝕜 ((TensorProduct.mapIncl E' F') x) ((TensorProduct.mapIncl E' F') y) = inner 𝕜 x y
-- Mathlib.Order.Hom.Bounded
TopHom.instFunLike.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Top α] [inst_1 : Top β],
  TopHom.instFunLike = { coe := TopHom.toFun, coe_injective := ⋯ }
-- Init.Data.Range.Polymorphic.UInt
UInt64.succMany?_ofBitVec : ∀ {k : ℕ} {x : BitVec 64}, Std.PRange.succMany? k { toBitVec := x } = UInt64.ofBitVec <$> Std.PRange.succMany? k x
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.Overlap.zero.sizeOf_spec : ∀ {u : Lean.Level} {α : Q(Type u)} {bt : Q(«$α») → Type} {sα : Q(CommSemiring «$α»)} {e : Q(«$α»)}
  [inst : (a : Q(«$α»)) → SizeOf (bt a)] (x : Q(Mathlib.Meta.NormNum.IsNat «$e» 0)),
  sizeOf (Mathlib.Tactic.Ring.Common.Overlap.zero x) = 1 + sizeOf x
-- Mathlib.Data.Nat.Factorization.Basic
Nat.Prime.pow_dvd_iff_dvd_ordProj : ∀ {p k n : ℕ}, Nat.Prime p → n ≠ 0 → (p ^ k ∣ n ↔ p ^ k ∣ p ^ n.factorization p)
-- Std.Async.Signal
Std.Async.Signal.sigwinch.sizeOf_spec : sizeOf Std.Async.Signal.sigwinch = 1
-- Std.Async.Signal
/-- Interrupt program.

Notes:
- Normally delivered when the user presses CTRL+C. Not generated when terminal raw mode is enabled.
 -/
Std.Async.Signal.sigint : Std.Async.Signal
-- Mathlib.Analysis.Normed.Group.Constructions
/-- Product of normed groups, using the sup norm.  -/
Prod.normedCommGroup : {E : Type u_2} → {F : Type u_3} → [NormedCommGroup E] → [NormedCommGroup F] → NormedCommGroup (E × F)
-- Mathlib.Data.Finsupp.MonomialOrder.DegLex
/-- `ofDegLex` is the identity function from the `DegLex` of a type.  -/
ofDegLex : {α : Type u_1} → DegLex α ≃ α
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey!_modify_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ [inst : Inhabited α] {k : α} {f : β → β}, (t.modify k f).getKey! k = if k ∈ t then k else default
-- Mathlib.CategoryTheory.Triangulated.Opposite.Functor
CategoryTheory.Functor.map_opShiftFunctorEquivalence_unitIso_hom_app_unop_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] [inst_2 : CategoryTheory.HasShift C ℤ]
  [inst_3 : CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [inst_4 : F.CommShift ℤ] (X : Cᵒᵖ) (n : ℤ)
  {Z : D} (h : F.obj (Opposite.unop X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (F.map ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).unitIso.hom.app X).unop) h =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Functor.commShiftIso F n).hom.app (Opposite.unop ((CategoryTheory.shiftFunctor Cᵒᵖ n).obj X)))
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.shiftFunctor D n).map ((CategoryTheory.Functor.commShiftIso F.op n).inv.app X).unop)
        (CategoryTheory.CategoryStruct.comp
          ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence D n).unitIso.hom.app
              (Opposite.op (F.obj (Opposite.unop X)))).unop
          h))
-- Mathlib.CategoryTheory.Bicategory.CatEnriched
CategoryTheory.CatEnriched.instBicategory : {C : Type u_1} →
  [CategoryTheory.EnrichedCategory CategoryTheory.Cat C] → CategoryTheory.Bicategory (CategoryTheory.CatEnriched C)
-- Std.Sat.AIG.RelabelNat
Std.Sat.AIG.RelabelNat.State.addFalse.congr_simp : ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Hashable α] {idx : ℕ} {decls : Array (Std.Sat.AIG.Decl α)}
  {hidx : idx < decls.size} (state state_1 : Std.Sat.AIG.RelabelNat.State α decls idx),
  state = state_1 → ∀ (h : decls[idx] = Std.Sat.AIG.Decl.false), state.addFalse h = state_1.addFalse h
-- Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful
/-- Given a bounded `f : α →+* β` between seminormed rings, is the seminorm on `β` is
power-multiplicative, then `f` is a contraction.  -/
contraction_of_isPowMul : ∀ {α : Type u_1} {β : Type u_2} [inst : SeminormedRing α] [inst_1 : SeminormedRing β],
  IsPowMul norm → ∀ {f : α →+* β}, f.IsBounded → ∀ (x : α), ‖f x‖ ≤ ‖x‖
-- Mathlib.RingTheory.Bialgebra.GroupLike
/-- `GroupLike.val` as a monoid hom.  -/
GroupLike.valMonoidHom : (R : Type u_1) →
  (A : Type u_2) → [inst : CommSemiring R] → [inst_1 : Semiring A] → [inst_2 : Bialgebra R A] → GroupLike R A →* A
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.coe_piecewise : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {s : Set α} (hs : MeasurableSet s)
  (f g : MeasureTheory.SimpleFunc α β), ⇑(MeasureTheory.SimpleFunc.piecewise s hs f g) = s.piecewise ⇑f ⇑g
-- Mathlib.Order.Concept
Concept.extent_sInf : ∀ {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (S : Set (Concept α β r)), (sInf S).extent = ⋂ i ∈ S, i.extent
-- Mathlib.LinearAlgebra.Matrix.Swap
Matrix.GeneralLinearGroup.map_swap : ∀ {R : Type u_1} {n : Type u_2} [inst : CommRing R] [inst_1 : DecidableEq n] [inst_2 : Fintype n] {S : Type u_3}
  [inst_3 : CommRing S] (f : R →+* S) (i j : n),
  (Matrix.GeneralLinearGroup.map f) (Matrix.GeneralLinearGroup.swap R i j) = Matrix.GeneralLinearGroup.swap S i j
-- Mathlib.ModelTheory.Bundled
/-- Bundles `M ⊨ T` as a `T.ModelType`.  -/
FirstOrder.Language.Theory.Model.bundled : {L : FirstOrder.Language} →
  {T : L.Theory} → {M : Type w} → [LM : L.Structure M] → [ne : Nonempty M] → M ⊨ T → T.ModelType
-- Plausible.Testable
Plausible.Testable.orTestable : {p q : Prop} → [Plausible.Testable p] → [Plausible.Testable q] → Plausible.Testable (p ∨ q)
-- Mathlib.CategoryTheory.Limits.Types.Colimits
CategoryTheory.Limits.Types.isColimit_iff_coconeTypesIsColimit : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J (Type u)}
  (c : CategoryTheory.Limits.Cocone F),
  Nonempty (CategoryTheory.Limits.IsColimit c) ↔ (F.coconeTypesEquiv.symm c).IsColimit
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.category_comp_τ₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : CategoryTheory.Square C} (f : X.Hom Y) (g : Y.Hom Z),
  (CategoryTheory.CategoryStruct.comp f g).τ₂ = CategoryTheory.CategoryStruct.comp f.τ₂ g.τ₂
-- Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic
DomAddAct.vadd_Lp_zero : ∀ {M : Type u_1} {α : Type u_3} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E]
  {μ : MeasureTheory.Measure α} {p : ENNReal} [inst_2 : VAdd M α] [inst_3 : MeasureTheory.VAddInvariantMeasure M α μ]
  [inst_4 : MeasurableConstVAdd M α] (c : Mᵈᵃᵃ), c +ᵥ 0 = 0
-- Mathlib.RingTheory.NormalClosure
Ring.instIsTorsionFreeNormalClosure : ∀ (R : Type u_1) (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : IsDomain R] [inst_3 : IsDomain S]
  [inst_4 : Algebra R S] [inst_5 : Module.IsTorsionFree R S], Module.IsTorsionFree S (Ring.NormalClosure R S)
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits
AlgebraicGeometry.PresheafedSpace.pushforwardDiagramToColimit_map : ∀ {J : Type u'} [inst : CategoryTheory.Category.{v', u'} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Limits.HasColimitsOfShape J TopCat]
  (F : CategoryTheory.Functor J (AlgebraicGeometry.PresheafedSpace C)) {j j' : J} (f : j ⟶ j'),
  (AlgebraicGeometry.PresheafedSpace.pushforwardDiagramToColimit F).map f =
    (CategoryTheory.CategoryStruct.comp
        ((TopCat.Presheaf.pushforward C
              (CategoryTheory.Limits.colimit.ι (F.comp (AlgebraicGeometry.PresheafedSpace.forget C)) j')).map
          (F.map f).c)
        (CategoryTheory.CategoryStruct.comp
          (TopCat.Presheaf.Pushforward.comp ((F.comp (AlgebraicGeometry.PresheafedSpace.forget C)).map f)
              (CategoryTheory.Limits.colimit.ι (F.comp (AlgebraicGeometry.PresheafedSpace.forget C)) j')
              (F.obj j).presheaf).inv
          (TopCat.Presheaf.pushforwardEq ⋯ (F.obj j).presheaf).hom)).op
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.maxKey?_eq_none_iff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  t.maxKey? = none ↔ t.isEmpty = true
-- Mathlib.Data.Nat.MaxPowDiv
Nat.maxPowDvdDiv.go.eq_1 : ∀ (n p : ℕ) (hp : 1 < p ∧ n ≠ 0),
  Nat.maxPowDvdDiv.go n p hp =
    if hmod : n % p = 0 then
      match Nat.maxPowDvdDiv.go n (p * p) ⋯ with
      | (e, q) => if q % p = 0 then (2 * e + 1, q / p) else (2 * e, q)
    else (0, n)
-- Mathlib.Data.ENat.Basic
ENat.add_lt_add_of_le_of_lt : ∀ {a b c d : ℕ∞}, a ≠ ⊤ → a ≤ b → c < d → a + c < b + d
-- ProofWidgets.Component.MakeEditLink
/-- Assuming that `s` is the content of a file starting at position `p`,
advance `p` to the end of `s`.  -/
Lean.Lsp.Position.advance : Lean.Lsp.Position → Substring.Raw → Lean.Lsp.Position
-- Mathlib.Data.Finsupp.Single
Finsupp.equivFunOnFinite_symm_single : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] [inst_1 : DecidableEq α] [inst_2 : Finite α] (x : α) (m : M),
  Finsupp.equivFunOnFinite.symm (Pi.single x m) = fun₀ | x => m
-- Mathlib.Analysis.Calculus.IteratedDeriv.Defs
/-- The `n`-th Fréchet derivative applied to a vector `(m 0, ..., m (n-1))` is the derivative
multiplied by the product of the `m i`s.  -/
iteratedFDeriv_apply_eq_iteratedDeriv_mul_prod : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {n : ℕ} {f : 𝕜 → F} {x : 𝕜} {m : Fin n → 𝕜},
  (iteratedFDeriv 𝕜 n f x) m = (∏ i, m i) • iteratedDeriv n f x
-- Mathlib.Algebra.Category.ModuleCat.Basic
ModuleCat.homLinearEquiv_symm_apply : ∀ {R : Type u} [inst : Ring R] {M N : ModuleCat R} {S : Type u_1} [inst_1 : Semiring S] [inst_2 : Module S ↑N]
  [inst_3 : SMulCommClass R S ↑N] (a : ↑M →ₗ[R] ↑N), ModuleCat.homLinearEquiv.symm a = ModuleCat.homAddEquiv.invFun a
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
/-- Integration of (nonnegative bounded continuous) test functions against finite Borel measures
depends continuously on the measure.  -/
MeasureTheory.FiniteMeasure.continuous_testAgainstNN_eval : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [inst_2 : OpensMeasurableSpace Ω]
  (f : BoundedContinuousFunction Ω NNReal), Continuous fun μ => μ.testAgainstNN f
-- Mathlib.Topology.MetricSpace.UniformConvergence
UniformOnFun.instPseudoMetricSpaceOfBoundedSpace : {α : Type u_1} →
  {β : Type u_2} →
    {𝔖 : Set (Set α)} →
      [Finite ↑𝔖] → [inst : PseudoMetricSpace β] → [BoundedSpace β] → PseudoMetricSpace (UniformOnFun α β 𝔖)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
WeierstrassCurve.Jacobian.Point.mk_point : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} {P : WeierstrassCurve.Jacobian.PointClass R}
  (h : W'.NonsingularLift P), { point := P, nonsingular := h }.point = P
-- Aesop.Frontend.Command
Aesop.Frontend.Parser.addRules : Lean.ParserDescr
-- Mathlib.Analysis.Normed.Ring.Units
Units.val_ofNearby : ∀ {R : Type u_1} [inst : NormedRing R] [inst_1 : HasSummableGeomSeries R] (x : Rˣ) (y : R) (h : ‖y - ↑x‖ < ‖↑x⁻¹‖⁻¹),
  ↑(x.ofNearby y h) = y
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
/-- `MonoidAlgebra.lift` as a `MulEquiv`.  -/
MonoidAlgebra.liftMulEquiv : (R : Type u_1) →
  (A : Type u_3) →
    (M : Type u_8) →
      [inst : CommSemiring R] →
        [inst_1 : CommSemiring A] →
          [inst_2 : Algebra R A] → [inst_3 : Monoid M] → (M →* A) ≃* WithConv (MonoidAlgebra R M →ₐ[R] A)
-- Mathlib.Analysis.Calculus.FDeriv.Const
fderiv_ofNat : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] (n : ℕ) [inst_7 : OfNat F n], fderiv 𝕜 (OfNat.ofNat n) = 0
-- Mathlib.Data.Nat.Factorial.DoubleFactorial
/-- Extension for `Nat.doubleFactorial`.  -/
Mathlib.Meta.Positivity.evalDoubleFactorial : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.Φ.eq_1 : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve R) (n : ℤ),
  W.Φ n = Polynomial.X * W.ΨSq n - W.preΨ (n + 1) * W.preΨ (n - 1) * if Even n then 1 else W.Ψ₂Sq
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso
CategoryTheory.Limits.pushout_inr_iso_of_left_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z)
  [inst_1 : CategoryTheory.IsIso f], CategoryTheory.IsIso (CategoryTheory.Limits.pushout.inr f g)
-- Mathlib.CategoryTheory.Limits.Preserves.Filtered
/-- Reflecting filtered colimits at any universe implies reflecting filtered colimits at universe `0`.
 -/
CategoryTheory.Limits.reflectsSmallestFilteredColimits_of_reflectsFilteredColimits : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.ReflectsFilteredColimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F],
  CategoryTheory.Limits.ReflectsFilteredColimitsOfSize.{0, 0, v₁, v₂, u₁, u₂} F
-- Mathlib.Algebra.Squarefree.Basic
Squarefree.ne_zero : ∀ {R : Type u_1} [inst : MonoidWithZero R] [Nontrivial R] {m : R}, Squarefree m → m ≠ 0
-- Mathlib.CategoryTheory.Category.TwoP
TwoP.mk.sizeOf_spec : ∀ (X : Type u) (toTwoPointing : TwoPointing X),
  sizeOf { X := X, toTwoPointing := toTwoPointing } = 1 + sizeOf X + sizeOf toTwoPointing
-- Mathlib.CategoryTheory.Limits.Shapes.Products
/-- The `∏ᶜ` functor composed with the pointwise constant functor `Π i, I i ⥤ (α → C)` is isomorphic
to the constant functor with value `∏ᶜ X`.  -/
CategoryTheory.Limits.Pi.constCompPiIsoConst : {α : Type w₂} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      [inst_1 : CategoryTheory.Limits.HasProductsOfShape α C] →
        {I : α → Type u_1} →
          [inst_2 : (i : α) → CategoryTheory.Category.{v_1, u_1} (I i)] →
            (X : α → C) →
              (CategoryTheory.Functor.pi fun i => (CategoryTheory.Functor.const (I i)).obj (X i)).comp
                  (CategoryTheory.Limits.Pi.functor α) ≅
                (CategoryTheory.Functor.const ((i : α) → I i)).obj (∏ᶜ X)
-- Mathlib.Order.TypeTags
WithBot.recBotCoe.eq_1 : ∀ {α : Type u_1} {C : WithBot α → Sort u_2} (bot : C ⊥) (coe : (a : α) → C ↑a), WithBot.recBotCoe bot coe none = bot
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.RenameOptions.prepareProvider : Lean.Lsp.RenameOptions → Bool
-- Mathlib.Computability.TuringMachine.Config
_private.Mathlib.Computability.TuringMachine.Config.0.Turing.ToPartrec.Code.eval.match_1.eq_4 : ∀ (motive : Turing.ToPartrec.Code → Sort u_1) (f fs : Turing.ToPartrec.Code)
  (h_1 : Unit → motive Turing.ToPartrec.Code.zero') (h_2 : Unit → motive Turing.ToPartrec.Code.succ)
  (h_3 : Unit → motive Turing.ToPartrec.Code.tail) (h_4 : (f fs : Turing.ToPartrec.Code) → motive (f.cons fs))
  (h_5 : (f g : Turing.ToPartrec.Code) → motive (f.comp g)) (h_6 : (f g : Turing.ToPartrec.Code) → motive (f.case g))
  (h_7 : (f : Turing.ToPartrec.Code) → motive f.fix),
  (match f.cons fs with
    | Turing.ToPartrec.Code.zero' => h_1 ()
    | Turing.ToPartrec.Code.succ => h_2 ()
    | Turing.ToPartrec.Code.tail => h_3 ()
    | f.cons fs => h_4 f fs
    | f.comp g => h_5 f g
    | f.case g => h_6 f g
    | f.fix => h_7 f) =
    h_4 f fs
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrpObj.lift_neg_comp_left_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {A B : C} [inst_2 : CategoryTheory.AddGrpObj A] [inst_3 : CategoryTheory.AddGrpObj B] (f : A ⟶ B)
  [CategoryTheory.IsAddMonHom f] {Z : C} (h : B ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.comp CategoryTheory.AddGrpObj.neg f)
        f)
      (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit A)
      (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.zero h)
-- Mathlib.Geometry.Manifold.Notation
_private.Mathlib.Geometry.Manifold.Notation.0.Manifold.Elab.findModel.go : Lean.Expr → Lean.Elab.TermElabM (Option Manifold.Elab.FindModelResult)
-- Init.Core
instInhabitedPProd : {α : Sort u_1} → {β : Sort u_2} → [Inhabited α] → [Inhabited β] → Inhabited (α ×' β)
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
SSet.Subcomplex.Pairing.RankFunction.Cell.mapToSucc_ι : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [inst : LinearOrder ι] {f : P.RankFunction ι}
  [inst_1 : P.IsProper] {j : ι} [inst_2 : SuccOrder ι] [inst_3 : NoMaxOrder ι] (c : f.Cell j),
  CategoryTheory.CategoryStruct.comp c.mapToSucc (f.filtration (Order.succ j)).ι = c.map
-- Lean.Meta.Tactic.Grind.Arith.CommRing.RingM
Lean.Meta.Grind.Arith.CommRing.MonadSetTermId.setTermId : {m : Type → Type} → [self : Lean.Meta.Grind.Arith.CommRing.MonadSetTermId m] → Lean.Expr → m Unit
-- Mathlib.CategoryTheory.Extensive
CategoryTheory.FinitaryExtensive.isPullback_initial_to : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.FinitaryExtensive C] {ι : Type u_1}
  [Finite ι] {F : CategoryTheory.Functor (CategoryTheory.Discrete ι) C} {c : CategoryTheory.Limits.Cocone F}
  (hc : CategoryTheory.Limits.IsColimit c) (i j : CategoryTheory.Discrete ι),
  i ≠ j →
    CategoryTheory.IsPullback (CategoryTheory.Limits.initial.to (F.obj i)) (CategoryTheory.Limits.initial.to (F.obj j))
      (c.ι.app i) (c.ι.app j)
-- Mathlib.MeasureTheory.Group.Convolution
MeasureTheory.Measure.lintegral_mconv_eq_lintegral_prod : ∀ {M : Type u_1} [inst : Monoid M] [inst_1 : MeasurableSpace M] [MeasurableMul₂ M] {μ ν : MeasureTheory.Measure M}
  {f : M → ENNReal}, Measurable f → ∫⁻ (z : M), f z ∂μ.mconv ν = ∫⁻ (z : M × M), f (z.1 * z.2) ∂μ.prod ν
-- Mathlib.RingTheory.Polynomial.Quotient
Ideal.quotient_map_C_eq_zero : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal R},
  ∀ a ∈ I, ((Ideal.Quotient.mk (Ideal.map Polynomial.C I)).comp Polynomial.C) a = 0
-- Mathlib.Analysis.SpecialFunctions.Arsinh
ContDiffAt.arsinh : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {a : E} {n : ℕ∞},
  ContDiffAt ℝ (↑n) f a → ContDiffAt ℝ (↑n) (fun x => Real.arsinh (f x)) a
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.fst_apply_inl : ∀ {M : Type u_1} {N : Type u_2} [inst : Monoid M] [inst_1 : Monoid N] (x : M),
  Monoid.Coprod.fst (Monoid.Coprod.inl x) = x
-- Mathlib.NumberTheory.NumberField.Units.Regulator
NumberField.Units.basisOfIsMaxRank_apply : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K]
  {u : Fin (NumberField.Units.rank K) → (NumberField.RingOfIntegers K)ˣ} (hu : NumberField.Units.IsMaxRank u)
  (i : Fin (NumberField.Units.rank K)),
  (NumberField.Units.basisOfIsMaxRank hu) i = (NumberField.Units.logEmbedding K) (Additive.ofMul (u i))
-- Mathlib.Algebra.Group.Hom.Defs
OneHom.funLike.eq_1 : ∀ {M : Type u_4} {N : Type u_5} [inst : One M] [inst_1 : One N],
  OneHom.funLike = { coe := OneHom.toFun, coe_injective := ⋯ }
-- Mathlib.Topology.Algebra.Group.GroupTopology
/-- A group topology on a group `α` is a topology for which multiplication and inversion
are continuous.  -/
GroupTopology : (α : Type u) → [Group α] → Type u
-- Mathlib.Tactic.FunProp.Types
/-- Result of `funProp`, it is a proof of function property `P f`  -/
Mathlib.Meta.FunProp.Result : Type
-- Mathlib.Algebra.Homology.TotalComplex
/-- The functor which sends a bicomplex to its total complex.  -/
HomologicalComplex₂.totalFunctor : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {I₁ : Type u_2} →
        {I₂ : Type u_3} →
          {I₁₂ : Type u_4} →
            (c₁ : ComplexShape I₁) →
              (c₂ : ComplexShape I₂) →
                (c₁₂ : ComplexShape I₁₂) →
                  [inst_2 : TotalComplexShape c₁ c₂ c₁₂] →
                    [DecidableEq I₁₂] →
                      [∀ (K : HomologicalComplex₂ C c₁ c₂), K.HasTotal c₁₂] →
                        CategoryTheory.Functor (HomologicalComplex₂ C c₁ c₂) (HomologicalComplex C c₁₂)
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.hasBasis_nhds_of_ne_top : ∀ {x : ENNReal}, x ≠ ⊤ → (nhds x).HasBasis (fun x => 0 < x) fun ε => Set.Icc (x - ε) (x + ε)
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.lift_of_apply : ∀ {α : Type u} (x : FreeAddGroup α), (FreeAddGroup.lift FreeAddGroup.of) x = x
-- Mathlib.Data.Multiset.DershowitzManna
_private.Mathlib.Data.Multiset.DershowitzManna.0.Multiset.isDershowitzMannaLT_singleton_insert : ∀ {α : Type u_1} [inst : Preorder α] {M N : Multiset α} {a : α},
  Multiset.OneStep✝ N (a ::ₘ M) → ∃ M', N = a ::ₘ M' ∧ Multiset.OneStep✝ M' M ∨ N = M + M' ∧ ∀ x ∈ M', x < a
-- Mathlib.Algebra.Torsor.Defs
Equiv.smulConst.eq_1 : ∀ {G : Type u_1} {P : Type u_2} [inst : Group G] [inst_1 : Torsor G P] (p : P),
  Equiv.smulConst p = { toFun := fun v => v • p, invFun := fun p' => p' /ₛ p, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.AlgebraicGeometry.Limits
/-- The map `Spec R ⨿ Spec S ⟶ Spec (R × S)`.
This is an isomorphism as witnessed by an `IsIso` instance provided below.  -/
AlgebraicGeometry.coprodSpec : (R S : Type u) →
  [inst : CommRing R] →
    [inst_1 : CommRing S] →
      AlgebraicGeometry.Spec (CommRingCat.of R) ⨿ AlgebraicGeometry.Spec (CommRingCat.of S) ⟶
        AlgebraicGeometry.Spec (CommRingCat.of (R × S))
-- Mathlib.SetTheory.Lists
_private.Mathlib.SetTheory.Lists.0.Lists.mem.decidable.match_1.eq_1 : ∀ {α : Type u_1} (motive : Lists α → Lists' α true → Sort u_2) (a : Lists α) (h_1 : (a : Lists α) → motive a Lists'.nil)
  (h_2 : (a : Lists α) → (b : Bool) → (b_1 : Lists' α b) → (l₂ : Lists' α true) → motive a (b_1.cons' l₂)),
  (match a, Lists'.nil with
    | a, Lists'.nil => h_1 a
    | a, b_1.cons' l₂ => h_2 a b b_1 l₂) =
    h_1 a
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.add_subset_range : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Add α] [inst_1 : Add β] [inst_2 : FunLike F α β]
  [AddHomClass F α β] (m : F) {s t : Set β}, s ⊆ Set.range ⇑m → t ⊆ Set.range ⇑m → s + t ⊆ Set.range ⇑m
-- Lean.Parser.Term
Lean.Parser.Term.letOptGeneralize.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.identNoAntiquot.formatter : Lean.PrettyPrinter.Formatter
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonInsertReplaceEdit : Lean.ToJson Lean.Lsp.InsertReplaceEdit
-- Mathlib.Order.Hom.Basic
OrderHom.piIso_apply : ∀ {α : Type u_2} [inst : Preorder α] {ι : Type u_6} {π : ι → Type u_7} [inst_1 : (i : ι) → Preorder (π i)]
  (f : α →o (i : ι) → π i) (i : ι), OrderHom.piIso f i = (Pi.evalOrderHom i).comp f
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
SubMulAction.conjMap_ofFixingSubgroup_bijective : ∀ {M : Type u_1} {α : Type u_2} [inst : Group M] [inst_1 : MulAction M α] {s t : Set α} {g : M} {hst : g • s = t},
  Function.Bijective ⇑(SubMulAction.conjMap_ofFixingSubgroup hst)
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.liftAddHom_comp_single : ∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : AddZeroClass M] [inst_1 : AddCommMonoid N] (f : α → M →+ N)
  (a : α), (Finsupp.liftAddHom f).comp (Finsupp.singleAddHom a) = f a
-- Mathlib.Computability.PartrecBasis
/-- A simplified basis for `Partrec`.  -/
Nat.Partrec' : {n : ℕ} → (List.Vector ℕ n →. ℕ) → Prop