mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Hom.Defs
MonoidHom.cancel_right : ∀ {M : Type u_4} {N : Type u_5} {P : Type u_6} [inst : MulOne M] [inst_1 : MulOne N] [inst_2 : MulOne P]
  {g₁ g₂ : N →* P} {f : M →* N}, Function.Surjective ⇑f → (g₁.comp f = g₂.comp f ↔ g₁ = g₂)
-- Mathlib.FieldTheory.Relrank
Subfield.relfinrank_eq_of_inf_eq : ∀ {E : Type v} [inst : Field E] {A B C : Subfield E}, A ⊓ C = B ⊓ C → A.relfinrank C = B.relfinrank C
-- Mathlib.GroupTheory.Torsion
/-- The image of a quotient is torsion iff the group is torsion.  -/
IsMulTorsion.quotient_iff : ∀ {G : Type u_1} {H : Type u_2} [inst : Group G] {N : Subgroup G} [inst_1 : Group H] {f : G →* H},
  Function.Surjective ⇑f → N = f.ker → IsMulTorsion ↥N → (IsMulTorsion H ↔ IsMulTorsion G)
-- Lean.Elab.DeclModifiers
/-- If `attrs` contains an `@[deprecated]` attribute, runs the action with `Term.Context.checkDeprecated`
disabled, suppressing the `linter.deprecated` warning that would otherwise fire when a deprecated
constant is referenced. Otherwise, runs the action unchanged.

This implements the suppression rule from RFC #8942: deprecation warnings should not fire inside
the body of a declaration that is itself marked `@[deprecated]`, since the references will go away
along with the declaration.
 -/
Lean.Elab.Term.withDeprecationContextFromAttrs : {m : Type → Type u_1} →
  {α : Type} → [MonadWithReaderOf Lean.Elab.Term.Context m] → Array Lean.Elab.Attribute → m α → m α
-- Lean.Parser.Extra
Lean.Parser.sepByElemParser.formatter : Lean.PrettyPrinter.Formatter → String → Lean.PrettyPrinter.Formatter
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
_private.Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup.0.Matrix.SpecialLinearGroup.diag2_coe.match_1.splitter : (motive : Fin 2 → Sort u_1) → (i : Fin 2) → (Unit → motive 0) → (Unit → motive 1) → motive i
-- Mathlib.RingTheory.Finiteness.Lattice
/-- The submodule generated by a supremum of finite-dimensional submodules, indexed by a finite
sort is finite-dimensional.  -/
Submodule.finite_iSup : ∀ {R : Type u_2} {V : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : Module R V] {ι : Sort u_1}
  [Finite ι] (S : ι → Submodule R V) [∀ (i : ι), Module.Finite R ↥(S i)], Module.Finite R ↥(⨆ i, S i)
-- Init.Data.Iterators.Combinators.Monadic.FlatMap
Std.Iterators.Types.Flatten.it₂ : {α α₂ β : Type w} → {m : Type w → Type u_1} → Std.Iterators.Types.Flatten α α₂ β m → Option (Std.IterM m β)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
Lean.Meta.Grind.Arith.Cutsat.ToIntInfo.ofLE? : Lean.Meta.Grind.Arith.Cutsat.ToIntInfo → Option (Option Lean.Expr)
-- Std.Data.Internal.List.Associative
Std.Internal.List.isEmpty_replaceEntry : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k},
  (Std.Internal.List.replaceEntry k v l).isEmpty = l.isEmpty
-- Lean.DocString.Extension
_private.Lean.DocString.Extension.0.Lean.VersoModuleDocs.DocContext.closeAll : Lean.VersoModuleDocs.DocContext✝ → Except String Lean.VersoModuleDocs.DocContext✝
-- Lean.Data.NameMap.Basic
Lean.NameHashSet : Type
-- Init.Data.Order.Classes
Std.LawfulOrderLT.mk : ∀ {α : Type u} [inst : LT α] [inst_1 : LE α], (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) → Std.LawfulOrderLT α
-- Mathlib.Topology.PartialHomeomorph.Basic
Set.BijOn.toPartialEquiv.congr_simp : ∀ {α : Type u_1} {β : Type u_2} [inst : Nonempty α] (f f_1 : α → β) (e_f : f = f_1) (s s_1 : Set α) (e_s : s = s_1)
  (t t_1 : Set β) (e_t : t = t_1) (hf : Set.BijOn f s t),
  Set.BijOn.toPartialEquiv f s t hf = Set.BijOn.toPartialEquiv f_1 s_1 t_1 ⋯
-- Lean.Meta.Basic
Lean.Meta.DefEqContext.mk.sizeOf_spec : ∀ (lhs rhs : Lean.Expr) (lctx : Lean.LocalContext) (localInstances : Lean.LocalInstances),
  sizeOf { lhs := lhs, rhs := rhs, lctx := lctx, localInstances := localInstances } =
    1 + sizeOf lhs + sizeOf rhs + sizeOf lctx + sizeOf localInstances
-- Init.Data.List.Sublist
List.prefix_iff_getElem? : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <+: l₂ ↔ ∀ (i : ℕ) (h : i < l₁.length), l₂[i]? = some l₁[i]
-- Mathlib.Algebra.Polynomial.Smeval
Polynomial.smeval_neg : ∀ (R : Type u_1) [inst : Ring R] {S : Type u_2} [inst_1 : AddCommGroup S] [inst_2 : Pow S ℕ] [inst_3 : Module R S]
  (p : Polynomial R) (x : S), (-p).smeval x = -p.smeval x
-- Mathlib.Topology.Sheaves.Stalks
TopCat.Presheaf.stalkSpecializes_comp_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X : TopCat}
  (F : TopCat.Presheaf C X) {x y z : ↑X} (h : x ⤳ y) (h' : y ⤳ z) {F_1 : C → C → Type uF} {carrier : C → Type w}
  {instFunLike : (X Y : C) → FunLike (F_1 X Y) (carrier X) (carrier Y)} [inst_2 : CategoryTheory.ConcreteCategory C F_1]
  (x_1 : carrier (F.stalk z)),
  (CategoryTheory.ConcreteCategory.hom (F.stalkSpecializes h))
      ((CategoryTheory.ConcreteCategory.hom (F.stalkSpecializes h')) x_1) =
    (CategoryTheory.ConcreteCategory.hom (F.stalkSpecializes ⋯)) x_1
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
/-- **Alias** of `zero_apply`. -/
ContinuousMultilinearMap.zero_apply : ∀ {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst : FunLike F α β} {inst_1 : Zero β}
  {inst_2 : Zero F} [self : IsZeroApply F α β] (x : α), 0 x = 0
-- Mathlib.Order.KrullDimension
Order.height_eq_krullDim_Iic : ∀ {α : Type u_1} [inst : Preorder α] (x : α), ↑(Order.height x) = Order.krullDim ↑(Set.Iic x)
-- Lean.Elab.PreDefinition.WF.GuessLex
Lean.Elab.WF.GuessLex.RecCallCache.callerName : Lean.Elab.WF.GuessLex.RecCallCache → Lean.Name
-- Init.Control.ExceptCps
/-- Use a monadic action that may throw an exception by providing explicit success and failure
continuations.
 -/
ExceptCpsT.runK : {m : Type u → Type u_1} → {β ε α : Type u} → ExceptCpsT ε m α → ε → (α → m β) → (ε → m β) → m β
-- Init.Data.List.Erase
List.eraseP_replicate_of_pos : ∀ {α : Type u_1} {p : α → Bool} {n : ℕ} {a : α},
  p a = true → List.eraseP p (List.replicate n a) = List.replicate (n - 1) a
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.Measure.pi.isAddHaarMeasure : ∀ {ι : Type u_1} {α : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → MeasurableSpace (α i)]
  (μ : (i : ι) → MeasureTheory.Measure (α i)) [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)]
  [inst_3 : (i : ι) → AddGroup (α i)] [inst_4 : (i : ι) → TopologicalSpace (α i)] [∀ (i : ι), (μ i).IsAddHaarMeasure]
  [∀ (i : ι), MeasurableAdd (α i)], (MeasureTheory.Measure.pi μ).IsAddHaarMeasure
-- Init.Data.Range.Polymorphic.Lemmas
_private.Init.Data.Range.Polymorphic.Lemmas.0.Std.Rcc.forIn'_eq_if.match_1.eq_2 : ∀ {γ : Type u_1} (motive : ForInStep γ → Sort u_2) (c : γ) (h_1 : (c : γ) → motive (ForInStep.yield c))
  (h_2 : (c : γ) → motive (ForInStep.done c)),
  (match ForInStep.done c with
    | ForInStep.yield c => h_1 c
    | ForInStep.done c => h_2 c) =
    h_2 c
-- Mathlib.LinearAlgebra.PiTensorProduct.Finsupp
PiTensorProduct.ofFinsuppEquiv'.eq_1 : ∀ {R : Type u_1} {ι : Type u_2} {κ : ι → Type u_3} [inst : CommSemiring R] [inst_1 : Fintype ι] [inst_2 : DecidableEq ι]
  [inst_3 : (i : ι) → DecidableEq (κ i)] [inst_4 : DecidableEq R],
  PiTensorProduct.ofFinsuppEquiv' =
    PiTensorProduct.ofFinsuppEquiv.trans
      (Finsupp.lcongr (Equiv.refl ((i : ι) → κ i)) ↑(PiTensorProduct.constantBaseRingEquiv ι R))
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM0.Machine.map_respects : ∀ {Γ : Type u_1} [inst : Inhabited Γ] {Γ' : Type u_2} [inst_1 : Inhabited Γ'] {Λ : Type u_3} [inst_2 : Inhabited Λ]
  {Λ' : Type u_4} [inst_3 : Inhabited Λ'] (M : Turing.TM0.Machine Γ Λ) (f₁ : Turing.PointedMap Γ Γ')
  (f₂ : Turing.PointedMap Γ' Γ) (g₁ : Turing.PointedMap Λ Λ') (g₂ : Λ' → Λ) {S : Set Λ},
  Turing.TM0.Supports M S →
    Function.RightInverse f₁.f f₂.f →
      (∀ q ∈ S, g₂ (g₁.f q) = q) →
        StateTransition.Respects (Turing.TM0.step M) (Turing.TM0.step (M.map f₁ f₂ g₁.f g₂)) fun a b =>
          a.q ∈ S ∧ Turing.TM0.Cfg.map f₁ g₁.f a = b
-- Std.Http.Server.Config
/-- Maximum aggregate byte size of all header field lines in a single message
(name + value bytes plus 4 bytes per line for `: ` and `\r\n`). Default: 64 KiB.
 -/
Std.Http.Config.maxHeaderBytes : Std.Http.Config → ℕ
-- Mathlib.Probability.Distributions.Gaussian.Real
ProbabilityTheory.gaussianReal_map_sub_const : ∀ {μ : ℝ} {v : NNReal} (y : ℝ),
  MeasureTheory.Measure.map (fun x => x - y) (ProbabilityTheory.gaussianReal μ v) =
    ProbabilityTheory.gaussianReal (μ - y) v
-- Mathlib.Algebra.Polynomial.Laurent
LaurentPolynomial.ext : ∀ {R : Type u_1} [inst : Semiring R] {p q : LaurentPolynomial R}, (∀ (a : ℤ), p.coeff a = q.coeff a) → p = q
-- Mathlib.Geometry.Euclidean.SignedDist
signedDist_triangle_left : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (v : V) (p q r : P), ((signedDist v) p) q - ((signedDist v) p) r = ((signedDist v) r) q
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
/-- `G.PreservesLeftKanExtension F L` asserts that `G` preserves all left Kan extensions
of `F` along `L`. See `PreservesLeftKanExtension.mk_of_preserves_isLeftKanExtension` for a
constructor taking a single left Kan extension as input.  -/
CategoryTheory.Functor.PreservesLeftKanExtension : {A : Type u_1} →
  {B : Type u_2} →
    {C : Type u_3} →
      {D : Type u_4} →
        [inst : CategoryTheory.Category.{v_1, u_1} A] →
          [inst_1 : CategoryTheory.Category.{v_2, u_2} B] →
            [inst_2 : CategoryTheory.Category.{v_3, u_3} C] →
              [inst_3 : CategoryTheory.Category.{v_4, u_4} D] →
                CategoryTheory.Functor B D → CategoryTheory.Functor A B → CategoryTheory.Functor A C → Prop
-- Mathlib.Topology.UniformSpace.ProdApproximation
/-- A continuous function on `X × Y`, taking values in an `R`-module with a uniform structure,
can be uniformly approximated by sums of functions of the form `(x, y) ↦ f x • g y`.

Note that no continuity properties are assumed either for multiplication on `R`, or for the scalar
multiplication of `R` on `V`.  -/
ContinuousMap.exists_finite_sum_smul_approximation_of_mem_uniformity : ∀ {X : Type u_1} {Y : Type u_2} {R : Type u_3} {V : Type u_4} [inst : TopologicalSpace X] [TotallyDisconnectedSpace X]
  [T2Space X] [CompactSpace X] [inst_4 : TopologicalSpace Y] [CompactSpace Y] [inst_6 : AddCommGroup V]
  [inst_7 : UniformSpace V] [IsUniformAddGroup V] {S : Set (V × V)} [inst_9 : TopologicalSpace R]
  [inst_10 : MonoidWithZero R] [inst_11 : MulActionWithZero R V] (f : C(X × Y, V)),
  S ∈ uniformity V → ∃ n g h, ∀ (x : X) (y : Y), (f (x, y), ∑ i, (g i) x • (h i) y) ∈ S
-- Init.Data.Nat.Gcd
Nat.gcd_dvd_gcd_mul_right_left : ∀ (m n k : ℕ), m.gcd n ∣ (m * k).gcd n
-- Lean.Meta.Tactic.Grind.Cases
Lean.Meta.Grind.instInhabitedCasesEntry.default : Lean.Meta.Grind.CasesEntry
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.instNormedSpace : {𝕜 : Type u_1} →
  {α : Type u_3} →
    {E : α → Type u_4} →
      {p : ENNReal} →
        [inst : (i : α) → NormedAddCommGroup (E i)] →
          [inst_1 : NormedField 𝕜] → [(i : α) → NormedSpace 𝕜 (E i)] → [inst_3 : Fact (1 ≤ p)] → NormedSpace 𝕜 ↥(lp E p)
-- Batteries.Data.Float.Lemmas
Float.Model.UnpackedFloat.unpack.fun_cases_unfolding : ∀ (spec : Float.Model.Format) (b : BitVec spec.numBits) (motive : Float.Model.UnpackedFloat → Prop),
  (have mantissaVec := Float.Model.UnpackedFloat.unpackMantissa b;
    have exponentVec := Float.Model.UnpackedFloat.unpackExponent b;
    have signVec := Float.Model.UnpackedFloat.unpackSign b;
    have sign := Float.Model.UnpackedFloat.Sign.ofBitVec signVec;
    exponentVec = -1#spec.exponentBits →
      mantissaVec = 0#spec.mantissaBitsWithoutImplicit → motive (Float.Model.UnpackedFloat.infinity sign)) →
    (have mantissaVec := Float.Model.UnpackedFloat.unpackMantissa b;
      have exponentVec := Float.Model.UnpackedFloat.unpackExponent b;
      exponentVec = -1#spec.exponentBits →
        ¬mantissaVec = 0#spec.mantissaBitsWithoutImplicit → motive Float.Model.UnpackedFloat.notANumber) →
      (have mantissaVec := Float.Model.UnpackedFloat.unpackMantissa b;
        have exponentVec := Float.Model.UnpackedFloat.unpackExponent b;
        have signVec := Float.Model.UnpackedFloat.unpackSign b;
        have sign := Float.Model.UnpackedFloat.Sign.ofBitVec signVec;
        ¬exponentVec = -1#spec.exponentBits →
          exponentVec = 0#spec.exponentBits →
            mantissaVec = 0#spec.mantissaBitsWithoutImplicit → motive (Float.Model.UnpackedFloat.zero sign)) →
        (let mantissaVec := Float.Model.UnpackedFloat.unpackMantissa b;
          have exponentVec := Float.Model.UnpackedFloat.unpackExponent b;
          have exponent := ↑exponentVec.toNat - (↑spec.exponentBias + ↑spec.mantissaBitsWithoutImplicit);
          have signVec := Float.Model.UnpackedFloat.unpackSign b;
          have sign := Float.Model.UnpackedFloat.Sign.ofBitVec signVec;
          ¬exponentVec = -1#spec.exponentBits →
            exponentVec = 0#spec.exponentBits →
              ∀ (h : ¬mantissaVec = 0#spec.mantissaBitsWithoutImplicit),
                motive (Float.Model.UnpackedFloat.finite sign mantissaVec.toNat (exponent + 1) ⋯)) →
          (let mantissaVec := Float.Model.UnpackedFloat.unpackMantissa b;
            have exponentVec := Float.Model.UnpackedFloat.unpackExponent b;
            have exponent := ↑exponentVec.toNat - (↑spec.exponentBias + ↑spec.mantissaBitsWithoutImplicit);
            have signVec := Float.Model.UnpackedFloat.unpackSign b;
            have sign := Float.Model.UnpackedFloat.Sign.ofBitVec signVec;
            ¬exponentVec = -1#spec.exponentBits →
              ¬exponentVec = 0#spec.exponentBits →
                motive (Float.Model.UnpackedFloat.finite sign (1#1 ++ mantissaVec).toNat exponent ⋯)) →
            motive (Float.Model.UnpackedFloat.unpack spec b)
-- Init.Data.List.Nat.Basic
List.getElem_intersperse_two_mul_add_one : ∀ {α : Type u_1} {l : List α} {sep : α} {i : ℕ} (h : 2 * i + 1 < (List.intersperse sep l).length),
  (List.intersperse sep l)[2 * i + 1] = sep
-- Lean.Data.Lsp.Ipc
Lean.Lsp.Ipc.expandModuleHierarchyImports : ℕ → Lean.Lsp.DocumentUri → Lean.Lsp.Ipc.IpcM (Option Lean.Lsp.Ipc.ModuleHierarchy × ℕ)
-- Mathlib.Data.Seq.Basic
Stream'.Seq.update_cons_zero : ∀ {α : Type u} (hd : α) (tl : Stream'.Seq α) (f : α → α),
  (Stream'.Seq.cons hd tl).update 0 f = Stream'.Seq.cons (f hd) tl
-- Mathlib.Data.Holor
Holor.assocLeft.eq_1 : ∀ {α : Type} {ds₁ ds₂ ds₃ : List ℕ}, Holor.assocLeft = cast ⋯
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.inv_empty : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Inv α], ∅⁻¹ = ∅
-- Mathlib.Data.ZMod.Defs
Fin.instNeZeroHAddNatOfNat_mathlib_1 : ∀ (n : ℕ) [NeZero n], NeZero 1
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
/-- A nonsingular projective point on a Weierstrass curve `W`.  -/
WeierstrassCurve.Projective.Point : {R : Type r} → [CommRing R] → WeierstrassCurve.Projective R → Type r
-- Lean.Elab.MutualDef
/-- Ensures that all declarations given by `preDefs` have distinct names.
Remark: we wait to perform this check until the pre-definition phase because we must account for
auxiliary declarations introduced by `where` and `let rec`.
 -/
_private.Lean.Elab.MutualDef.0.Lean.Elab.Term.checkAllDeclNamesDistinct : Array Lean.Elab.PreDefinition → Lean.Elab.TermElabM Unit
-- Mathlib.CategoryTheory.Triangulated.TriangleShift
/-- The inverse of the rotation of triangles can be expressed using a double
rotation and the shift by `-1`.  -/
CategoryTheory.Pretriangulated.invRotateIsoRotateRotateShiftFunctorNegOne : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.HasShift C ℤ] →
        [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
          CategoryTheory.Pretriangulated.invRotate C ≅
            (CategoryTheory.Pretriangulated.rotate C).comp
              ((CategoryTheory.Pretriangulated.rotate C).comp
                (CategoryTheory.Pretriangulated.Triangle.shiftFunctor C (-1)))
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.getD.eq_1 : ∀ {α : Type u} {β : Type v} [inst : BEq α] (a : α) (fallback : β),
  Std.DHashMap.Internal.AssocList.getD a fallback Std.DHashMap.Internal.AssocList.nil = fallback
-- Mathlib.CategoryTheory.Quotient.Preadditive
CategoryTheory.Quotient.functor_additive : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] (r : HomRel C)
  [inst_2 : CategoryTheory.Congruence r]
  (hr : ∀ ⦃X Y : C⦄ (f₁ f₂ g₁ g₂ : X ⟶ Y), r f₁ f₂ → r g₁ g₂ → r (f₁ + g₁) (f₂ + g₂)),
  (CategoryTheory.Quotient.functor r).Additive
-- Mathlib.Topology.Order.LeftRightLim
Monotone.leftLim_le : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : ConditionallyCompleteLinearOrder β]
  [inst_2 : TopologicalSpace β] [OrderTopology β] {f : α → β},
  Monotone f → ∀ {x y : α}, x ≤ y → Function.leftLim f x ≤ f y
-- Mathlib.Order.Heyting.Hom
BiheytingHom.comp_apply : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : BiheytingAlgebra α] [inst_1 : BiheytingAlgebra β]
  [inst_2 : BiheytingAlgebra γ] (f : BiheytingHom β γ) (g : BiheytingHom α β) (a : α), (f.comp g) a = f (g a)
-- Mathlib.Topology.Instances.Matrix
instContinuousConstSMulMatrix : ∀ {α : Type u_2} {m : Type u_4} {n : Type u_5} {R : Type u_8} [inst : TopologicalSpace R] [inst_1 : SMul α R]
  [ContinuousConstSMul α R], ContinuousConstSMul α (Matrix m n R)
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
/-- We say that a ring with a valuative relation is of rank one if
there exists a strictly monotone embedding of the "canonical" value group-with-zero into
the nonnegative reals, and the image of this embedding contains some element different
from `0` and `1`.  -/
ValuativeRel.IsRankLeOne : (R : Type u_1) → [inst : Semiring R] → [ValuativeRel R] → Prop
-- Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder
LocallyFiniteOrder.orderAddMonoidHom.congr_simp : ∀ (G : Type u_2) [inst : AddCommGroup G] [inst_1 : LinearOrder G] [inst_2 : IsOrderedAddMonoid G]
  [inst_3 : LocallyFiniteOrder G], LocallyFiniteOrder.orderAddMonoidHom G = LocallyFiniteOrder.orderAddMonoidHom G
-- Mathlib.CategoryTheory.Preadditive.Biproducts
/-- In a preadditive category, if the product over `f : J → C` exists,
then the biproduct over `f` exists.  -/
CategoryTheory.Limits.HasBiproduct.of_hasProduct : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {J : Type u_1}
  [Finite J] (f : J → C) [CategoryTheory.Limits.HasProduct f], CategoryTheory.Limits.HasBiproduct f
-- Mathlib.LinearAlgebra.QuadraticForm.Prod
QuadraticMap.Isometry.proj_apply : ∀ {ι : Type u_1} {R : Type u_2} {P : Type u_7} {Mᵢ : ι → Type u_8} [inst : CommSemiring R]
  [inst_1 : (i : ι) → AddCommMonoid (Mᵢ i)] [inst_2 : AddCommMonoid P] [inst_3 : (i : ι) → Module R (Mᵢ i)]
  [inst_4 : Module R P] [inst_5 : Fintype ι] [inst_6 : DecidableEq ι] (i : ι) (Q : QuadraticMap R (Mᵢ i) P)
  (f : (x : ι) → Mᵢ x), (QuadraticMap.Isometry.proj i Q) f = f i
-- Lean.MetavarContext
Lean.LevelMetavarDecl : Type
-- Init.Data.BitVec.Lemmas
/-- A `(x : BitVec v)` set to width `w` equals `(v - w)` zeros,
followed by the low `(min v w) bits of `x`
 -/
BitVec.setWidth_eq_append_extractLsb' : ∀ {v : ℕ} {x : BitVec v} {w : ℕ}, BitVec.setWidth w x = BitVec.cast ⋯ (0#(w - v) ++ BitVec.extractLsb' 0 (min v w) x)
-- Mathlib.Data.List.Nodup
List.Nodup.product : ∀ {α : Type u} {β : Type v} {l₁ : List α} {l₂ : List β}, l₁.Nodup → l₂.Nodup → (l₁ ×ˢ l₂).Nodup
-- Mathlib.LinearAlgebra.BilinearForm.Orthogonal
/-- **Alias** of `LinearMap.BilinForm.IsAlt.eq_iff`. -/
LinearMap.BilinForm.IsAlt.ortho_comm : ∀ {R₁ : Type u_3} {M₁ : Type u_4} [inst : CommRing R₁] [inst_1 : AddCommGroup M₁] [inst_2 : Module R₁ M₁]
  {B₁ : LinearMap.BilinForm R₁ M₁}, B₁.IsAlt → ∀ {x y : M₁}, (B₁ x) y = 0 ↔ (B₁ y) x = 0
-- Init.Data.Int.Linear
Int.gcd.eq_1 : ∀ (m n : ℤ), m.gcd n = m.natAbs.gcd n.natAbs
-- Mathlib.Algebra.Module.Rat
map_ratCast_smul : ∀ {M : Type u_1} {M₂ : Type u_2} [inst : AddCommGroup M] [inst_1 : AddCommGroup M₂] {F : Type u_3}
  [inst_2 : FunLike F M M₂] [AddMonoidHomClass F M M₂] (f : F) (R : Type u_4) (S : Type u_5) [inst_4 : DivisionRing R]
  [inst_5 : DivisionRing S] [inst_6 : Module R M] [inst_7 : Module S M₂] (c : ℚ) (x : M), f (↑c • x) = ↑c • f x
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
ContinuousMultilinearMap.opNorm_neg : ∀ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_3 : SeminormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] [inst_5 : Fintype ι]
  (f : ContinuousMultilinearMap 𝕜 E G), ‖-f‖ = ‖f‖
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.isEmpty_insertMany_list : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {l : List α},
  (t.insertMany l).isEmpty = (t.isEmpty && l.isEmpty)
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
UpperHalfPlane.instIsPretransitiveGeneralLinearGroupFinOfNatNatReal : MulAction.IsPretransitive (GL (Fin 2) ℝ) UpperHalfPlane
-- Mathlib.Order.Hom.CompleteLattice
sInfHom.dual_apply_toFun : ∀ {α : Type u_2} {β : Type u_3} [inst : InfSet α] [inst_1 : InfSet β] (f : sInfHom α β) (a : αᵒᵈ),
  (sInfHom.dual f) a = (⇑OrderDual.toDual ∘ ⇑f ∘ ⇑OrderDual.ofDual) a
-- Std.Time.Zoned.Database.Windows
/-- Returns a default `WindowsDb` instance.
 -/
Std.Time.Database.WindowsDb.default : Std.Time.Database.WindowsDb
-- Lean.Meta.Tactic.Grind.Split
Lean.Meta.Grind.SplitAnchorRefInfo.anchor : Lean.Meta.Grind.SplitAnchorRefInfo → UInt64
-- Mathlib.LinearAlgebra.Finsupp.LinearCombination
/-- An element `m ∈ M` is contained in the `R`-submodule spanned by a set `s ⊆ M`, if and only if
`m` can be written as a finite `R`-linear combination of elements of `s`.
The implementation uses a sum indexed by `Fin n` for some `n`.  -/
Submodule.mem_span_set' : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {m : M}
  {s : Set M}, m ∈ Submodule.span R s ↔ ∃ n f g, ∑ i, f i • ↑(g i) = m
-- Mathlib.Algebra.Category.FGModuleCat.Colimits
FGModuleCat.instCreatesColimitsOfShapeModuleCatForget₂LinearMapIdCarrierObjIsFG : {J : Type} →
  [inst : CategoryTheory.SmallCategory J] →
    [CategoryTheory.FinCategory J] →
      {k : Type u} →
        [inst_2 : Ring k] →
          CategoryTheory.CreatesColimitsOfShape J (CategoryTheory.forget₂ (FGModuleCat k) (ModuleCat k))
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.pure : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} [inst : Monad m] [inst_1 : Std.Do.WPMonad m ps] {α : Type u} {a : α}
  {Q : Std.Do.PostCond α ps}, ⦃Q.1 a⦄ pure a ⦃Q⦄
-- Mathlib.Algebra.Ring.Opposite
MulOpposite.instNatCast : {R : Type u_1} → [NatCast R] → NatCast Rᵐᵒᵖ
-- Lean.Parser.Types
Lean.Parser.FirstTokens.tokens.inj : ∀ {a a_1 : List Lean.Parser.Token}, Lean.Parser.FirstTokens.tokens a = Lean.Parser.FirstTokens.tokens a_1 → a = a_1
-- Init.Data.Nat.ToString
Nat.a_eq_digitChar : ∀ {n : ℕ}, 'a' = n.digitChar ↔ n = 10
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.instMulLeftMono : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Mul α], MulLeftMono (Finset α)
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.All.upperBound?_ub : ∀ {α : Type u_1} {p : α → Prop} {ub : Option α} {cut : α → Ordering} {x : α} {t : RBTree.RBNode α},
  RBTree.RBNode.All p t → (∀ {x : α}, ub = some x → p x) → RBTree.RBNode.upperBound? cut t ub = some x → p x
-- Init.Data.String.Lemmas.Intercalate
_private.Init.Data.String.Lemmas.Intercalate.0.String.intercalate.go.match_1.eq_2 : ∀ (motive : List String → Sort u_1) (h_1 : (a : String) → (as : List String) → motive (a :: as))
  (h_2 : Unit → motive []),
  (match [] with
    | a :: as => h_1 a as
    | [] => h_2 ()) =
    h_2 ()