mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.InnerProductSpace.Defs
PreInnerProductSpace.Core.mk.inj : ∀ {𝕜 : Type u_4} {F : Type u_5} {inst : RCLike 𝕜} {inst_1 : AddCommGroup F} {inst_2 : Module 𝕜 F} {toInner : Inner 𝕜 F}
  {conj_inner_symm : ∀ (x y : F), (starRingEnd 𝕜) (inner 𝕜 y x) = inner 𝕜 x y}
  {re_inner_nonneg : ∀ (x : F), 0 ≤ RCLike.re (inner 𝕜 x x)}
  {add_left : ∀ (x y z : F), inner 𝕜 (x + y) z = inner 𝕜 x z + inner 𝕜 y z}
  {smul_left : ∀ (x y : F) (r : 𝕜), inner 𝕜 (r • x) y = (starRingEnd 𝕜) r * inner 𝕜 x y} {toInner_1 : Inner 𝕜 F}
  {conj_inner_symm_1 : ∀ (x y : F), (starRingEnd 𝕜) (inner 𝕜 y x) = inner 𝕜 x y}
  {re_inner_nonneg_1 : ∀ (x : F), 0 ≤ RCLike.re (inner 𝕜 x x)}
  {add_left_1 : ∀ (x y z : F), inner 𝕜 (x + y) z = inner 𝕜 x z + inner 𝕜 y z}
  {smul_left_1 : ∀ (x y : F) (r : 𝕜), inner 𝕜 (r • x) y = (starRingEnd 𝕜) r * inner 𝕜 x y},
  { toInner := toInner, conj_inner_symm := conj_inner_symm, re_inner_nonneg := re_inner_nonneg, add_left := add_left,
        smul_left := smul_left } =
      { toInner := toInner_1, conj_inner_symm := conj_inner_symm_1, re_inner_nonneg := re_inner_nonneg_1,
        add_left := add_left_1, smul_left := smul_left_1 } →
    toInner = toInner_1
-- Mathlib.Data.NNReal.Defs
/-- Constructor of ℝ≥0 from a nonnegative real number.

Important: You should use `NNReal.mk` instead of the anonymous constructor `⟨_, _⟩` to avoid abuse
of the definitional equality between `ℝ≥0` and `{ r : ℝ // 0 ≤ r }`.  -/
NNReal.mk : (x : ℝ) → 0 ≤ x → NNReal
-- Mathlib.Analysis.Convex.Basic
Submodule.starConvex : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] (K : Submodule 𝕜 E), StarConvex 𝕜 0 ↑K
-- Mathlib.Algebra.Algebra.StrictPositivity
IsUnit.isStrictlyPositive_iff_conjugate_of_isSelfAdjoint : ∀ {A : Type u_1} [inst : Semiring A] [inst_1 : StarRing A] [inst_2 : PartialOrder A] [StarOrderedRing A] (a b : A),
  IsUnit b →
    autoParam (IsSelfAdjoint b) IsUnit.isStrictlyPositive_iff_conjugate_of_isSelfAdjoint._auto_1 →
      (IsStrictlyPositive (b * a * b) ↔ IsStrictlyPositive a)
-- Mathlib.GroupTheory.Index
Subgroup.fintypeOfIndexNeZero.eq_1 : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} (hH : H.index ≠ 0),
  Subgroup.fintypeOfIndexNeZero hH = Fintype.ofFinite (G ⧸ H)
-- Mathlib.RingTheory.DiscreteValuationRing.Basic
Irreducible.maximalIdeal_eq : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsDiscreteValuationRing R] {ϖ : R},
  Irreducible ϖ → IsLocalRing.maximalIdeal R = Ideal.span {ϖ}
-- Mathlib.Algebra.Ring.BooleanRing
/-- The "identity" equivalence between `AsBoolRing α` and `α`.  -/
toBoolRing : {α : Type u_1} → α ≃ AsBoolRing α
-- Lean.AddDecl
/-- Saves the state of `Lean.Option`s associated with environment linters into `envLinterSnapshotExt`
 -/
Lean.snapshotEnvLinterOptions : Lean.Name → Lean.CoreM Unit
-- Mathlib.Topology.Path
Path.trans_symm : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y z : X} (γ : Path x y) (γ' : Path y z),
  (γ.trans γ').symm = γ'.symm.trans γ.symm
-- Mathlib.Probability.Kernel.IonescuTulcea.Traj
MeasureTheory.instIsProbabilityMeasureForallValNatMemFinsetInducedFamilyOfForallIic : ∀ {X : ℕ → Type u_1} [inst : (n : ℕ) → MeasurableSpace (X n)]
  (μ : (n : ℕ) → MeasureTheory.Measure ((i : ↥(Finset.Iic n)) → X ↑i))
  [∀ (n : ℕ), MeasureTheory.IsProbabilityMeasure (μ n)] (I : Finset ℕ),
  MeasureTheory.IsProbabilityMeasure (MeasureTheory.inducedFamily μ I)
-- Mathlib.RingTheory.AdicCompletion.RingHom
/-- Universal property of `IsAdicComplete` for rings.
The lift ring map `lift I f hf : R →+* S` of a sequence of compatible
ring maps `f n : R →+* S ⧸ (I ^ n)`.
 -/
IsAdicComplete.liftRingHom : {R : Type u_1} →
  {S : Type u_2} →
    [inst : NonAssocSemiring R] →
      [inst_1 : CommRing S] →
        (I : Ideal S) →
          [IsAdicComplete I S] →
            (f : (n : ℕ) → R →+* S ⧸ I ^ n) →
              (∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorPow I hle).comp (f n) = f m) → R →+* S
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Submodule
PresheafOfModules.Submodule.bot_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  {M : PresheafOfModules R} (X : Cᵒᵖ), ⊥.obj X = ⊥ X
-- Mathlib.Data.ENat.Basic
ENat.map_ofNat : ∀ {α : Type u_1} (f : ℕ → α) (n : ℕ) [inst : n.AtLeastTwo], ENat.map f (OfNat.ofNat n) = ↑(f n)
-- Mathlib.CategoryTheory.Limits.Presentation
/-- If `F : J ⥤ C` is a functor that has a colimit, then this is the obvious
colimit presentation of `colimit F`.  -/
CategoryTheory.Limits.ColimitPresentation.colimit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w} →
      [inst_1 : CategoryTheory.Category.{t, w} J] →
        (F : CategoryTheory.Functor J C) →
          [inst_2 : CategoryTheory.Limits.HasColimit F] →
            CategoryTheory.Limits.ColimitPresentation J (CategoryTheory.Limits.colimit F)
-- Mathlib.Algebra.Polynomial.Laurent
LaurentPolynomial.T_pow : ∀ {R : Type u_1} [inst : Semiring R] (m : ℤ) (n : ℕ), LaurentPolynomial.T m ^ n = LaurentPolynomial.T (↑n * m)
-- Mathlib.Algebra.Algebra.Spectrum.Basic
resolvent.eq_1 : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Ring A] [inst_2 : Algebra R A] (a : A) (r : R),
  resolvent a r = Ring.inverse ((algebraMap R A) r - a)
-- Init.Data.SInt.Lemmas
ISize.toInt64_div_of_ne_right : ∀ (a b : ISize), b ≠ -1 → (a / b).toInt64 = a.toInt64 / b.toInt64
-- Init.Grind.Ring.Basic
Lean.Grind.IsCharP.natCast_ext : ∀ {α : Type u_1} (p : ℕ) [inst : Lean.Grind.Semiring α] [Lean.Grind.IsCharP α p] {x y : ℕ}, x % p = y % p → ↑x = ↑y
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.Context.mk : Lean.Name → Bool → Lean.PrettyPrinter.Parenthesizer.Context
-- Mathlib.Topology.EMetricSpace.BoundedVariation
BoundedVariationOn.tendsto_atTop_limUnder : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] [CompleteSpace E]
  [hE : Nonempty E] {f : α → E},
  BoundedVariationOn f Set.univ → Filter.Tendsto f Filter.atTop (nhds (Filter.atTop.limUnder f))
-- Mathlib.Algebra.Order.GroupWithZero.Defs
/-- Typeclass for reverse monotonicity of multiplication by positive elements on the left,
namely `b * a₁ ≤ b * a₂ → a₁ ≤ a₂` if `0 < b`.

You should usually not use this very granular typeclass directly, but rather a typeclass like
`IsStrictOrderedRing`.  -/
PosMulReflectLE : (α : Type u_1) → [Mul α] → [Zero α] → [Preorder α] → Prop
-- Mathlib.Topology.Instances.AddCircle.Defs
AddCircle.equivIoc_coe_eq : ∀ {𝕜 : Type u_1} [inst : AddCommGroup 𝕜] {p : 𝕜} [inst_1 : LinearOrder 𝕜] [inst_2 : IsOrderedAddMonoid 𝕜]
  [hp : Fact (0 < p)] {a : 𝕜} [inst_3 : Archimedean 𝕜] {x : 𝕜} (hx : x ∈ Set.Ioc a (a + p)),
  (AddCircle.equivIoc p a) ↑x = ⟨x, hx⟩
-- Mathlib.Util.Export
Lean.Export.Alloc.next : {α : Type u_1} → [inst : BEq α] → [inst_1 : Hashable α] → Lean.Export.Alloc α → ℕ
-- Mathlib.Combinatorics.SimpleGraph.Operations
SimpleGraph.edge_comm : ∀ {V : Type u_1} (s t : V), SimpleGraph.edge s t = SimpleGraph.edge t s
-- Mathlib.CategoryTheory.Limits.Opposites
/-- Turn a colimit for `F.rightOp : J ⥤ Cᵒᵖ` into a limit for `F : Jᵒᵖ ⥤ C`.  -/
CategoryTheory.Limits.isLimitOfCoconeRightOpOfCone : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} J] →
        (F : CategoryTheory.Functor Jᵒᵖ C) →
          {c : CategoryTheory.Limits.Cone F} →
            CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.coconeRightOpOfCone c) →
              CategoryTheory.Limits.IsLimit c
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.Mod.mk.sizeOf_spec : ∀ {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] [inst_5 : SizeOf C] [inst_6 : SizeOf D] (X : D)
  [mod : CategoryTheory.ModObj A X], sizeOf { X := X, mod := mod } = 1 + sizeOf X + sizeOf mod
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Oplax
/-- Right unitor for the vertical composition of lax natural transformations.  -/
CategoryTheory.Oplax.LaxTrans.rightUnitor : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.OplaxFunctor B C} →
          (η : F ⟶ G) → CategoryTheory.CategoryStruct.comp η (CategoryTheory.CategoryStruct.id G) ≅ η
-- Mathlib.Algebra.Category.CommBialgCat
instIsCommMonObjOppositeCommAlgCatXUnopMonObjCommBialgCatFunctorCommBialgCatEquivComonCommAlgCatOfIsCocommCarrier : ∀ {R : Type u} [inst : CommRing R] {A : CommBialgCat R} [Coalgebra.IsCocomm R ↑A],
  CategoryTheory.IsCommMonObj (Opposite.unop ((commBialgCatEquivComonCommAlgCat R).functor.obj A)).X
-- Mathlib.Topology.Algebra.Module.Complement
Submodule.projectionL_apply_right : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {p q : Submodule R M} (h : Submodule.IsTopCompl p q) (x : ↥q), (p.projectionL q h) ↑x = 0
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.mk_mem_carrier : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] {𝒜 : ℕ → σ}
  [inst_3 : GradedRing 𝒜] {f : A} (x : ↑((AlgebraicGeometry.Proj.toLocallyRingedSpace 𝒜).restrict ⋯).toTopCat)
  (z : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)),
  HomogeneousLocalization.mk z ∈ AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.carrier x ↔
    ↑z.num ∈ (↑x).asHomogeneousIdeal
-- Mathlib.Algebra.GroupWithZero.Submonoid.Pointwise
Submonoid.pointwise_smul_le_pointwise_smul_iff₀ : ∀ {G₀ : Type u_1} {M : Type u_3} [inst : Monoid M] [inst_1 : GroupWithZero G₀] [inst_2 : MulDistribMulAction G₀ M]
  {a : G₀}, a ≠ 0 → ∀ {S T : Submonoid M}, a • S ≤ a • T ↔ S ≤ T
-- Mathlib.Analysis.InnerProductSpace.NormDet
_private.Mathlib.Analysis.InnerProductSpace.NormDet.0.LinearMap.orthonormalBasis_range : {𝕜 : Type u_1} →
  {U : Type u_2} →
    {V : Type u_3} →
      [inst : RCLike 𝕜] →
        [inst_1 : NormedAddCommGroup U] →
          [inst_2 : InnerProductSpace 𝕜 U] →
            [FiniteDimensional 𝕜 U] →
              [inst_4 : NormedAddCommGroup V] →
                [inst_5 : InnerProductSpace 𝕜 V] →
                  {ι : Type u_5} →
                    [inst_6 : Fintype ι] →
                      {f : U →ₗ[𝕜] V} → f.ker = ⊥ → OrthonormalBasis ι 𝕜 U → OrthonormalBasis ι 𝕜 ↥f.range
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
/-- `constOfIsEmpty` as a linear isometry equivalence.  -/
ContinuousAlternatingMap.constOfIsEmptyLIE : (𝕜 : Type u) →
  (E : Type wE) →
    (F : Type wF) →
      (ι : Type v) →
        [inst : NontriviallyNormedField 𝕜] →
          [inst_1 : SeminormedAddCommGroup E] →
            [inst_2 : NormedSpace 𝕜 E] →
              [inst_3 : SeminormedAddCommGroup F] →
                [inst_4 : NormedSpace 𝕜 F] → [inst_5 : Fintype ι] → [IsEmpty ι] → F ≃ₗᵢ[𝕜] E [⋀^ι]→L[𝕜] F
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.coe_sinOrderIso_apply : ∀ (x : ↑(Set.Icc (-(Real.pi / 2)) (Real.pi / 2))), ↑(Real.sinOrderIso x) = Real.sin ↑x
-- Mathlib.Algebra.Category.MonCat.Basic
/-- Build an `AddEquiv` from an isomorphism in the category
`AddMonCat`.  -/
CategoryTheory.Iso.addMonCatIsoToAddEquiv : {X Y : AddMonCat} → (X ≅ Y) → ↑X ≃+ ↑Y
-- Lean.MonadEnv
Lean.matchConstRec : {m : Type → Type} →
  {α : Type} →
    [Monad m] → [Lean.MonadEnv m] → Lean.Expr → (Unit → m α) → (Lean.RecursorVal → List Lean.Level → m α) → m α
-- Qq.MetaM
Qq.MaybeDefEq.defEq.sizeOf_spec : ∀ {u : Lean.Level}
  {α :
    let u := u;
    Q(Sort u)}
  {a b : Q(«$α»)} (a_1 : «$a» =Q «$b»), sizeOf (Qq.MaybeDefEq.defEq a_1) = 1 + sizeOf a_1
-- Mathlib.Data.Pi.Interval
Pi.uIcc_eq : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : Fintype ι] [inst_1 : DecidableEq ι] [inst_2 : (i : ι) → DecidableEq (α i)]
  [inst_3 : (i : ι) → Lattice (α i)] [inst_4 : (i : ι) → LocallyFiniteOrder (α i)] (a b : (i : ι) → α i),
  Finset.uIcc a b = Fintype.piFinset fun i => Finset.uIcc (a i) (b i)
-- Mathlib.Analysis.Convex.Cone.InnerDual
ProperCone.innerDual_le_innerDual : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : CompleteSpace E]
  {s t : Set E}, t ⊆ s → ProperCone.innerDual s ≤ ProperCone.innerDual t
-- Mathlib.LinearAlgebra.BilinearForm.Properties
LinearMap.BilinForm.IsAlt.eq_of_add_add_eq_zero : ∀ {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} [IsCancelAdd R] {a b c : M}, B.IsAlt → a + b + c = 0 → (B a) b = (B b) c
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- If `Y' ≅ Y`, then `X ⨿ Y` also is the coproduct of `X` and `Y'`.  -/
CategoryTheory.Limits.BinaryCofan.isColimitCompRightIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Y' : C} →
      (c : CategoryTheory.Limits.BinaryCofan X Y) →
        (f : Y' ⟶ Y) →
          [CategoryTheory.IsIso f] →
            CategoryTheory.Limits.IsColimit c →
              CategoryTheory.Limits.IsColimit
                (CategoryTheory.Limits.BinaryCofan.mk c.inl (CategoryTheory.CategoryStruct.comp f c.inr))
-- Lean.Widget.Types
Lean.Widget.instRpcEncodableWidgetInstance : Lean.Server.RpcEncodable Lean.Widget.WidgetInstance
-- Mathlib.Order.TransfiniteIteration
transfiniteIterate.congr_simp : ∀ {I : Type u} [inst : SupSet I] (φ φ_1 : I → I),
  φ = φ_1 →
    ∀ {J : Type w} [inst_1 : LinearOrder J] [inst_2 : SuccOrder J] [inst_3 : WellFoundedLT J] (j j_1 : J),
      j = j_1 → ∀ (a a_1 : I), a = a_1 → transfiniteIterate φ j a = transfiniteIterate φ_1 j_1 a_1
-- Mathlib.GroupTheory.FreeAbelianGroup
instInhabitedFreeAbelianGroup : (α : Type u_1) → Inhabited (FreeAbelianGroup α)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.mem_union_iff : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, k ∈ m₁ ∪ m₂ ↔ k ∈ m₁ ∨ k ∈ m₂
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.mulConst.go.eq_1 : ∀ (k k_1 : ℤ),
  Lean.Grind.CommRing.Poly.mulConst.go k (Lean.Grind.CommRing.Poly.num k_1) = Lean.Grind.CommRing.Poly.num (k * k_1)
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.ContinuousHom.coe_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : OmegaCompletePartialOrder α] [inst_1 : OmegaCompletePartialOrder β] (a : α)
  (f : α →𝒄 β), ↑f a = f a
-- Mathlib.Algebra.Order.Group.Synonym
pow_toLex : ∀ {α : Type u_1} {β : Type u_2} [inst : Pow α β] (a : α) (b : β), a ^ toLex b = a ^ b
-- Mathlib.CategoryTheory.Shift.Localization
CategoryTheory.LocalizerMorphism.commShift_iso_inv_app : ∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) {M : Type u_3}
  [inst_2 : AddMonoid M] [inst_3 : CategoryTheory.HasShift C₁ M] [inst_4 : CategoryTheory.HasShift C₂ M]
  [inst_5 : Φ.functor.CommShift M] {D₁ : Type u_4} {D₂ : Type u_5} [inst_6 : CategoryTheory.Category.{v_3, u_4} D₁]
  [inst_7 : CategoryTheory.Category.{v_4, u_5} D₂] (L₁ : CategoryTheory.Functor C₁ D₁) [inst_8 : L₁.IsLocalization W₁]
  (L₂ : CategoryTheory.Functor C₂ D₂) [inst_9 : CategoryTheory.HasShift D₁ M] [inst_10 : CategoryTheory.HasShift D₂ M]
  [inst_11 : L₁.CommShift M] [inst_12 : L₂.CommShift M] (G : CategoryTheory.Functor D₁ D₂)
  (e : Φ.functor.comp L₂ ≅ L₁.comp G) (m : M) (X : C₁),
  (CategoryTheory.Functor.commShiftIso G m).inv.app (L₁.obj X) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D₂ m).map (e.inv.app X))
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso L₂ m).inv.app (Φ.functor.obj X))
        (CategoryTheory.CategoryStruct.comp (L₂.map ((CategoryTheory.Functor.commShiftIso Φ.functor m).inv.app X))
          (CategoryTheory.CategoryStruct.comp (e.hom.app ((CategoryTheory.shiftFunctor C₁ m).obj X))
            (G.map ((CategoryTheory.Functor.commShiftIso L₁ m).hom.app X)))))
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
MeasurableSpace.generateFrom_iUnion_countablePartition : ∀ (α : Type u_3) [m : MeasurableSpace α] [inst : MeasurableSpace.CountablyGenerated α],
  MeasurableSpace.generateFrom (⋃ n, MeasurableSpace.countablePartition α n) = m
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.biproduct.congr_simp : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (f f_1 : J → C) (e_f : f = f_1)
  [inst_2 : CategoryTheory.Limits.HasBiproduct f], (⨁ f) = ⨁ f_1
-- Mathlib.Algebra.Homology.ComplexShape
ComplexShape.down'_mk : ∀ {α : Type u_2} [inst : Add α] [inst_1 : IsRightCancelAdd α] (a j i : α), i + a = j → (ComplexShape.down' a).Rel j i
-- Mathlib.Algebra.Polynomial.GroupRingAction
prodXSubSMul.coeff : ∀ (G : Type u_2) [inst : Group G] [inst_1 : Fintype G] (R : Type u_3) [inst_2 : CommRing R]
  [inst_3 : MulSemiringAction G R] (x : R) (g : G) (n : ℕ),
  g • (prodXSubSMul G R x).coeff n = (prodXSubSMul G R x).coeff n
-- Batteries.Data.List.Basic
List.takeDTR.go.eq_2 : ∀ {α : Type u_1} (dflt : α) (a : List α) (a_1 : Array α), List.takeDTR.go dflt 0 a a_1 = a_1.toList
-- Mathlib.CategoryTheory.Localization.Adjunction
CategoryTheory.Adjunction.Localization.ε.eq_1 : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} D₁]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D₂] {G : CategoryTheory.Functor C₁ C₂} {F : CategoryTheory.Functor C₂ C₁}
  (adj : G ⊣ F) (L₁ : CategoryTheory.Functor C₁ D₁) (W₁ : CategoryTheory.MorphismProperty C₁)
  [inst_4 : L₁.IsLocalization W₁] (L₂ : CategoryTheory.Functor C₂ D₂) (G' : CategoryTheory.Functor D₁ D₂)
  (F' : CategoryTheory.Functor D₂ D₁) [inst_5 : CategoryTheory.CatCommSq G L₁ L₂ G']
  [inst_6 : CategoryTheory.CatCommSq F L₂ L₁ F'],
  CategoryTheory.Adjunction.Localization.ε adj L₁ W₁ L₂ G' F' =
    CategoryTheory.Localization.liftNatTrans L₁ W₁ L₁ ((G.comp F).comp L₁) (CategoryTheory.Functor.id D₁) (G'.comp F')
      (CategoryTheory.Functor.whiskerRight adj.unit L₁)
-- Mathlib.Data.List.NodupEquivFin
List.Nodup.getEquiv_apply_coe : ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α) (H : l.Nodup) (i : Fin l.length),
  ↑((List.Nodup.getEquiv l H) i) = l.get i
-- Mathlib.SetTheory.Cardinal.Defs
/-- The cardinal exponential. `#α ^ #β` is the cardinal of `β → α`.  -/
Cardinal.instPowCardinal : Pow Cardinal.{u} Cardinal.{u}
-- Mathlib.Algebra.Homology.ShortComplex.Homology
/-- a right homology data  -/
CategoryTheory.ShortComplex.HomologyData.right : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S : CategoryTheory.ShortComplex C} → S.HomologyData → S.RightHomologyData
-- Mathlib.Analysis.Normed.Group.Basic
dist_le_norm_add_norm' : ∀ {E : Type u_5} [inst : SeminormedGroup E] (a b : E), dist a b ≤ ‖a‖ + ‖b‖
-- Mathlib.Topology.VectorBundle.Riemannian
/-- A family of inner product space structures on the fibers of a fiber bundle, defining the same
topology as the already existing one. This family is not assumed to be continuous or smooth: to
guarantee continuity, resp. smoothness, of the inner product as a function of the base point,
use `ContinuousRiemannianMetric` or `ContMDiffRiemannianMetric`.

This structure is used through `RiemannianBundle` for typeclass inference, to register the inner
product space structure on the fibers without creating diamonds.  -/
Bundle.RiemannianMetric : {B : Type u_4} →
  (E : B → Type u_6) →
    [(b : B) → TopologicalSpace (E b)] →
      [inst : (b : B) → AddCommGroup (E b)] → [(b : B) → Module ℝ (E b)] → Type (max u_4 u_6)
-- Mathlib.Algebra.Order.ToIntervalMod
toIocMod_sub_zsmul' : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α) (m : ℤ), toIocMod hp (a - m • p) b = toIocMod hp a b - m • p
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Equiv.filter : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β},
  m₁.WF →
    m₂.WF →
      ∀ (f : (a : α) → β a → Bool), m₁.Equiv m₂ → (Std.DHashMap.Raw.filter f m₁).Equiv (Std.DHashMap.Raw.filter f m₂)
-- Mathlib.CategoryTheory.Shift.Basic
CategoryTheory.shiftFunctorAdd'_assoc_inv_app : ∀ {C : Type u} {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddMonoid A]
  [inst_2 : CategoryTheory.HasShift C A] (a₁ a₂ a₃ a₁₂ a₂₃ a₁₂₃ : A) (h₁₂ : a₁ + a₂ = a₁₂) (h₂₃ : a₂ + a₃ = a₂₃)
  (h₁₂₃ : a₁ + a₂ + a₃ = a₁₂₃) (X : C),
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.shiftFunctor C a₃).map ((CategoryTheory.shiftFunctorAdd' C a₁ a₂ a₁₂ h₁₂).inv.app X))
      ((CategoryTheory.shiftFunctorAdd' C a₁₂ a₃ a₁₂₃ ⋯).inv.app X) =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.shiftFunctorAdd' C a₂ a₃ a₂₃ h₂₃).inv.app ((CategoryTheory.shiftFunctor C a₁).obj X))
      ((CategoryTheory.shiftFunctorAdd' C a₁ a₂₃ a₁₂₃ ⋯).inv.app X)
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RicSliceData.mk : {α : Type u} →
  {β : α → Type v} →
    [inst : Ord α] → Std.DTreeMap.Internal.Impl α β → Std.Ric α → Std.DTreeMap.Internal.RicSliceData α β
-- Init.Omega.Constraint
/-- Multiply by `-1` if the leading coefficient is negative, otherwise do nothing.  -/
Lean.Omega.positivize : Lean.Omega.Constraint × Lean.Omega.Coeffs → Lean.Omega.Constraint × Lean.Omega.Coeffs
-- Lean.Meta.Tactic.Grind.Arith.Util
Lean.Meta.Grind.Arith.CollectDecVars.State : Type
-- Mathlib.Algebra.Order.GroupWithZero.Action.Synonym
OrderDual.instSMulWithZero : {G₀ : Type u_1} → {M₀ : Type u_2} → [inst : Zero G₀] → [inst_1 : Zero M₀] → [SMulWithZero G₀ M₀] → SMulWithZero G₀ᵒᵈ M₀
-- Mathlib.CategoryTheory.Limits.Shapes.Terminal
CategoryTheory.Limits.initialIsoIsInitial_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasInitial C] {P : C}
  (t : CategoryTheory.Limits.IsInitial P),
  (CategoryTheory.Limits.initialIsoIsInitial t).hom = CategoryTheory.Limits.initialIsInitial.to P
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue_insertList_of_contains_eq_false_left : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : EquivBEq α] {l toInsert : List ((_ : α) × β)} {k : α},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.DistinctKeys toInsert →
      ∀ (contains : Std.Internal.List.containsKey k (Std.Internal.List.insertList l toInsert) = true)
        (not_contains : Std.Internal.List.containsKey k l = false),
        Std.Internal.List.getValue k (Std.Internal.List.insertList l toInsert) contains =
          Std.Internal.List.getValue k toInsert ⋯
-- Mathlib.Algebra.Algebra.Rat
RingHomClass.toLinearMapClassNNRat : ∀ {F : Type u_1} {R : Type u_2} {S : Type u_3} [inst : DivisionSemiring R] [inst_1 : CharZero R]
  [inst_2 : DivisionSemiring S] [inst_3 : CharZero S] [inst_4 : FunLike F R S] [RingHomClass F R S],
  LinearMapClass F ℚ≥0 R S
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.cokernelSequenceCyclesE_exact : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.cokernelSequenceCyclesE_exact._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.cokernelSequenceCyclesE_exact._auto_3),
  (X.cokernelSequenceCyclesE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).Exact