mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.List.Lemmas
List.eq_replicate_of_mem : ∀ {α : Type u_1} {a : α} {l : List α}, (∀ b ∈ l, b = a) → l = List.replicate l.length a
-- Mathlib.RingTheory.Unramified.Finite
/-- An unramified free algebra is finitely generated. Iversen I.2.8  -/
Algebra.FormallyUnramified.finite_of_free : ∀ (R : Type u_1) (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.FormallyUnramified R S] [Algebra.EssFiniteType R S] [Module.Free R S], Module.Finite R S
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.coinvariantsKerOfIsBoundary₀_coe : ∀ {k G A : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : AddCommGroup A] [inst_3 : Module k A]
  [inst_4 : DistribMulAction G A] [inst_5 : SMulCommClass G k A] (x : A) (hx : groupHomology.IsBoundary₀ G x),
  ↑(groupHomology.coinvariantsKerOfIsBoundary₀ x hx) = x
-- Lean.Expr
Lean.instInhabitedFVarId.default : Lean.FVarId
-- Mathlib.Logic.Nonempty
/-- Using `Classical.choice`, lifts a (`Prop`-valued) `Nonempty` instance to a (`Type`-valued)
`Inhabited` instance. `Classical.inhabited_of_nonempty` already exists, in `Init/Classical.lean`,
but the assumption is not a type class argument, which makes it unsuitable for some applications.  -/
Classical.inhabited_of_nonempty' : {α : Sort u_3} → [h : Nonempty α] → Inhabited α
-- Mathlib.Order.Filter.Bases.Basic
Filter.mk.congr_simp : ∀ {α : Type u_1} (sets sets_1 : Set (Set α)) (e_sets : sets = sets_1) (univ_sets : Set.univ ∈ sets)
  (sets_of_superset : ∀ {x y : Set α}, x ∈ sets → x ⊆ y → y ∈ sets)
  (inter_sets : ∀ {x y : Set α}, x ∈ sets → y ∈ sets → x ∩ y ∈ sets),
  { sets := sets, univ_sets := univ_sets, sets_of_superset := sets_of_superset, inter_sets := inter_sets } =
    { sets := sets_1, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ }
-- Lean.MetavarContext
Lean.LevelMetavarDecl.mk.sizeOf_spec : ∀ (depth index : ℕ), sizeOf { depth := depth, index := index } = 1 + sizeOf depth + sizeOf index
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Under.mapIso_functor : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X Y : T} (f : X ≅ Y),
  (CategoryTheory.Under.mapIso f).functor = CategoryTheory.Under.map f.hom
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
Lean.Meta.Grind.Arith.Cutsat.ToIntInfo.powThm? : Lean.Meta.Grind.Arith.Cutsat.ToIntInfo → Option (Option Lean.Expr)
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
/-- Given a functor `F : Set.Iic ⥤ C`, this is the morphism in `C`, as an element
in `Arrow C`, that is obtained by applying `F.map` to an inequality.  -/
CategoryTheory.SmallObject.SuccStruct.arrowMap : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w} →
      [inst_1 : LinearOrder J] →
        {j : J} → CategoryTheory.Functor (↑(Set.Iic j)) C → (i₁ i₂ : J) → i₁ ≤ i₂ → i₂ ≤ j → CategoryTheory.Arrow C
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
/-- The transpose of a matrix.  -/
CStarMatrix.transpose : {m : Type u_1} → {n : Type u_2} → {A : Type u_5} → CStarMatrix m n A → CStarMatrix n m A
-- Mathlib.Analysis.Calculus.Deriv.Basic
derivWithin_zero_of_not_differentiableWithinAt : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F]
  [inst_3 : TopologicalSpace F] {f : 𝕜 → F} {x : 𝕜} {s : Set 𝕜}, ¬DifferentiableWithinAt 𝕜 f s x → derivWithin f s x = 0
-- Mathlib.GroupTheory.Coset.Defs
QuotientGroup.rightRel.eq_1 : ∀ {α : Type u_1} [inst : Group α] (s : Subgroup α), QuotientGroup.rightRel s = MulAction.orbitRel (↥s) α
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic
Polynomial.Chebyshev.complex_ofReal_eval_S : ∀ (x : ℝ) (n : ℤ), ↑(Polynomial.eval x (Polynomial.Chebyshev.S ℝ n)) = Polynomial.eval (↑x) (Polynomial.Chebyshev.S ℂ n)
-- Init.Data.BitVec.Lemmas
BitVec.extractLsb.eq_1 : ∀ {n : ℕ} (hi lo : ℕ) (x : BitVec n), BitVec.extractLsb hi lo x = BitVec.extractLsb' lo (hi - lo + 1) x
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.self_le_maxKey!_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → ∀ {k : α} {v : β k}, (cmp k (t.insert k v).maxKey!).isLE = true
-- Mathlib.Tactic.Ring.Basic
/-- Frontend of `ring1`: attempt to close a goal `g`, assuming it is an equation of semirings.  -/
Mathlib.Tactic.Ring.proveEq : Lean.MVarId → Mathlib.Tactic.AtomM Unit
-- Mathlib.Data.TypeVec
TypeVec.repeatEq_iff_eq : ∀ {n : ℕ} {α : TypeVec.{u_1} n} {i : Fin2 n} {x y : α i},
  TypeVec.ofRepeat (α.repeatEq i (TypeVec.prod.mk i x y)) ↔ x = y
-- Mathlib.FieldTheory.RatFunc.AsPolynomial
/-- `RatFunc.C a` is the constant rational function `a`.  -/
RatFunc.C : {K : Type u} → [inst : CommRing K] → [inst_1 : IsDomain K] → K →+* RatFunc K
-- Mathlib.CategoryTheory.Abelian.Projective.Ext
CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_mk_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X Y : C} (R : CategoryTheory.ProjectiveResolution X) {n : ℕ}
  [inst_3 : HasDerivedCategory C]
  (x : CochainComplex.HomComplex.Cocycle R.cochainComplex ((CochainComplex.singleFunctor C 0).obj Y) ↑n),
  (R.extEquivCohomologyClass.symm (CochainComplex.HomComplex.CohomologyClass.mk x)).hom =
    (CategoryTheory.ShiftedHom.mk₀ 0 ⋯
          (CategoryTheory.CategoryStruct.comp ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X)
            (CategoryTheory.inv (DerivedCategory.Q.map R.π')))).comp
      ((CategoryTheory.ShiftedHom.map (CochainComplex.HomComplex.Cocycle.equivHomShift.symm x) DerivedCategory.Q).comp
        (CategoryTheory.ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y)) ⋯)
      ⋯
-- Aesop.Search.Queue
Aesop.Options.queue : Aesop.Options → (Q : Type) × Aesop.Queue Q
-- Mathlib.CategoryTheory.WithTerminal.Cone
_private.Mathlib.CategoryTheory.WithTerminal.Cone.0.CategoryTheory.WithTerminal.id.match_1.splitter : {C : Type u_1} →
  (motive : CategoryTheory.WithTerminal C → Sort u_2) →
    (x : CategoryTheory.WithTerminal C) →
      ((a : C) → motive (CategoryTheory.WithTerminal.of a)) →
        (Unit → motive CategoryTheory.WithTerminal.star) → motive x
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.ArgSpec.many.inj : ∀ {name : Lean.Name} {type : Lean.Expr} {name_1 : Lean.Name} {type_1 : Lean.Expr},
  Lean.Doc.ArgSpec.many✝ name type = Lean.Doc.ArgSpec.many✝ name_1 type_1 → name = name_1 ∧ type = type_1
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
/-- **Alias** of `EisensteinSeries.eisensteinSeriesSIF_apply`. -/
EisensteinSeries.eisensteinSeries_SIF_apply : ∀ {N : ℕ} (a : Fin 2 → ZMod N) (k : ℤ) (z : UpperHalfPlane),
  (EisensteinSeries.eisensteinSeriesSIF a k) z = eisensteinSeries a k z
-- Lean.Declaration
Lean.ConstantInfo.isAxiom : Lean.ConstantInfo → Bool
-- Mathlib.Algebra.Module.Equiv.Basic
AddEquiv.toNatLinearEquiv_toAddEquiv : ∀ {M : Type u_5} {M₂ : Type u_7} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid M₂] (e : M ≃+ M₂),
  ↑e.toNatLinearEquiv = e
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionAssocIso_inv_naturality_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.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] {c₁ c₂ c₃ c₄ : C} {d₁ d₂ : D} (f : c₁ ⟶ c₂)
  (g : c₃ ⟶ c₄) (h : d₁ ⟶ d₂) {Z : D}
  (h_1 :
    CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj
        (CategoryTheory.MonoidalCategoryStruct.tensorObj c₂ c₄) d₂ ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHom f
        (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHom g h))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso c₂ c₄ d₂).inv h_1) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso c₁ c₃ d₁).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHom
          (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) h)
        h_1)
-- Mathlib.RingTheory.Localization.AtPrime.Basic
/-- **Alias** of `IsLocalization.AtPrime.under_map_eq_map`. -/
IsLocalization.AtPrime.comap_map_eq_map : ∀ {S : Type u_6} {R : Type u_7} [inst : CommRing R] (p : Ideal R) [inst_1 : p.IsMaximal] {Sₚ : Type u_9}
  [inst_2 : CommRing S] [inst_3 : Algebra R S] [inst_4 : CommRing Sₚ] [inst_5 : Algebra S Sₚ] [inst_6 : Algebra R Sₚ]
  [IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ] [IsScalarTower R S Sₚ],
  Ideal.under S (Ideal.map (algebraMap R Sₚ) p) = Ideal.map (algebraMap R S) p
-- Lean.Elab.Tactic.Basic
/-- Close the main goal using the given tactic. If it fails, log the error and `admit`  -/
Lean.Elab.Tactic.closeUsingOrAdmit : Lean.Elab.Tactic.TacticM Unit → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.Algebra.Group.Pointwise.Set.BigOperators
/-- An n-ary version of `Set.mul_mem_mul`.  -/
Set.finsetProd_mem_finsetProd : ∀ {ι : Type u_1} {α : Type u_2} [inst : CommMonoid α] (t : Finset ι) (f : ι → Set α) (g : ι → α),
  (∀ i ∈ t, g i ∈ f i) → ∏ i ∈ t, g i ∈ ∏ i ∈ t, f i
-- Mathlib.MeasureTheory.Measure.Regular
/-- A measure `μ` is inner regular if, for any measurable set `s`, then
`μ(s) = sup {μ(K) | K ⊆ s compact}`.  -/
MeasureTheory.Measure.InnerRegular : {α : Type u_1} → [inst : MeasurableSpace α] → [TopologicalSpace α] → MeasureTheory.Measure α → Prop
-- Init.Grind.Lemmas
Lean.Grind.eq_eq_of_eq_true_right : ∀ {a b : Prop}, b = True → (a = b) = a
-- Mathlib.Topology.UniformSpace.Cauchy
/-- A sequence of points such that `seq n ∈ setSeq n`. Here `setSeq` is an antitone
sequence of sets `setSeq n ∈ f` with diameters controlled by a given sequence
of entourages.  -/
SequentiallyComplete.seq : {α : Type u} →
  [uniformSpace : UniformSpace α] →
    {f : Filter α} → Cauchy f → {U : ℕ → SetRel α α} → (∀ (n : ℕ), U n ∈ uniformity α) → ℕ → α
-- Mathlib.RingTheory.RootsOfUnity.Basic
map_rootsOfUnity : ∀ {M : Type u_1} {N : Type u_2} [inst : CommMonoid M] [inst_1 : CommMonoid N] (f : Mˣ →* Nˣ) (k : ℕ),
  Subgroup.map f (rootsOfUnity k M) ≤ rootsOfUnity k N
-- Mathlib.NumberTheory.ModularForms.SlashInvariantForms
/-- Functions `ℍ → ℂ` that are invariant under the `SlashAction`.  -/
SlashInvariantForm : outParam (Subgroup (GL (Fin 2) ℝ)) → outParam ℤ → Type
-- Mathlib.Topology.Convenient.Category
ContinuousGeneratedByCat.equivalence_unitIso : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)],
  ContinuousGeneratedByCat.equivalence.unitIso = ContinuousGeneratedByCat.equivalenceUnitIso
-- Lean.Elab.ParseImportsFast
Lean.ParseImports.setExported : Lean.ParseImports.Parser
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
ClosedSubmodule.toSubmodule_top : ∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : TopologicalSpace M]
  [inst_3 : Module R M], ↑⊤ = ⊤
-- Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
CategoryTheory.ObjectProperty.instHasFiniteCoproductsFullSubcategoryOfIsClosedUnderFiniteCoproducts : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C)
  [CategoryTheory.Limits.HasFiniteCoproducts C] [P.IsClosedUnderFiniteCoproducts],
  CategoryTheory.Limits.HasFiniteCoproducts P.FullSubcategory
-- Init.Data.Range.Polymorphic.UpwardEnumerable
Std.PRange.UpwardEnumerable.succMany?_add_one_eq_succ?_bind_succMany? : ∀ {α : Type u_1} [inst : Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerable α] {n : ℕ} {a : α},
  Std.PRange.succMany? (n + 1) a = (Std.PRange.succ? a).bind fun x => Std.PRange.succMany? n x
-- Mathlib.Algebra.Expr
/-- Produce an `Add` instance for `Q($α)` such that `x + y : Q($α)` is `q($x + $y)`.  -/
Expr.instAdd : {u : Lean.Level} → (α : Q(Type u)) → Q(Add «$α») → Add Q(«$α»)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.mem_of_mem_erase : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k a : α}, a ∈ m.erase k → a ∈ m
-- Init.Data.List.Basic
List.concat.eq_def : ∀ {α : Type u} (x : List α) (x_1 : α),
  x.concat x_1 =
    match x, x_1 with
    | [], b => [b]
    | a :: as, b => a :: as.concat b
-- Init.Data.SInt.Basic
/-- Bitwise or for word-sized signed integers. Usually accessed via the `|||` operator.

Each bit of the resulting integer is set if at least one of the corresponding bits of the input
integers is set, according to the two's complement representation.

This function is overridden at runtime with an efficient implementation.
 -/
ISize.lor : ISize → ISize → ISize
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.instInhabitedCtorInfo.default : Lean.Compiler.LCNF.CtorInfo
-- Mathlib.Combinatorics.Matroid.Minor.Order
/-- `N` is a strict minor of `M` if `N` is a minor of `M` and `N ≠ M`.
Equivalently, `N` is obtained from `M` by deleting/contracting subsets of the ground set
that are not both empty.  -/
Matroid.IsStrictMinor : {α : Type u_1} → Matroid α → Matroid α → Prop
-- Mathlib.Topology.Algebra.Group.Quotient
QuotientAddGroup.instLocallyCompactSpace : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [SeparatelyContinuousAdd G] [LocallyCompactSpace G]
  (N : AddSubgroup G), LocallyCompactSpace (G ⧸ N)
-- Init.Data.Range.Polymorphic.UpwardEnumerable
Std.PRange.UpwardEnumerable.lt_of_le_of_lt : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerable α] {a b c : α},
  Std.PRange.UpwardEnumerable.LE a b → Std.PRange.UpwardEnumerable.LT b c → Std.PRange.UpwardEnumerable.LT a c
-- Mathlib.CategoryTheory.Limits.Constructions.Filtered
/-- The `liftToFinset` functor, precomposed with forming a colimit, is a coproduct on the original
functor.  -/
CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetLimIso : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    (α : Type w) →
      [inst_1 : CategoryTheory.Limits.HasFiniteProducts C] →
        [inst_2 : CategoryTheory.Limits.HasLimitsOfShape (Finset (CategoryTheory.Discrete α))ᵒᵖ C] →
          [inst_3 : CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete α) C] →
            (CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinset C α).comp CategoryTheory.Limits.lim ≅
              CategoryTheory.Limits.lim
-- Lean.Elab.Binders
_private.Lean.Elab.Binders.0.Lean.Elab.Term.expandMatchAltsWhereDecls.loop : Lean.Expr → Lean.Syntax → Lean.Syntax → ℕ → Array Lean.Syntax → Lean.Elab.TermElabM Lean.Syntax
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
/-- Given a `k`-module `A` with a compatible `DistribMulAction` of `G`, and a function
`f : G → A` satisfying the 1-cocycle condition, produces a 1-cocycle for the representation on
`A` induced by the `DistribMulAction`.  -/
groupCohomology.cocyclesOfIsCocycle₁ : {k G A : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      [inst_2 : AddCommGroup A] →
        [inst_3 : Module k A] →
          [inst_4 : DistribMulAction G A] →
            [inst_5 : SMulCommClass G k A] →
              {f : G → A} → groupCohomology.IsCocycle₁ f → ↥(groupCohomology.cocycles₁ (Rep.ofDistribMulAction k G A))
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.stepRet_eval : ∀ {k : Turing.ToPartrec.Cont} {v : List ℕ},
  StateTransition.eval Turing.ToPartrec.step (Turing.ToPartrec.stepRet k v) = Turing.ToPartrec.Cfg.halt <$> k.eval v
-- Lean.Data.Iterators.Producers.PersistentHashMap
Lean.PersistentHashMap.Zipper.consEntries.sizeOf_spec : ∀ {α : Type u} {β : Type v} [inst : SizeOf α] [inst_1 : SizeOf β]
  (a : Subarray (Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β)))
  (a_1 : Lean.PersistentHashMap.Zipper α β),
  sizeOf (Lean.PersistentHashMap.Zipper.consEntries a a_1) = 1 + sizeOf a + sizeOf a_1
-- Std.Http.Data.URI.Encoding
/-- Decodes an `EncodedQueryString` back to a regular `String`. Converts percent-encoded sequences and '+'
signs back to their original characters. Returns `none` if the decoded bytes are not valid UTF-8.

This is almost the same code from `System.Uri.UriEscape.decodeUri`, but with `Option` instead.
 -/
Std.Http.URI.EncodedQueryString.decode : {r : UInt8 → Bool} → Std.Http.URI.EncodedQueryString r → Option String
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
/-- The complex hyperbolic cosine function is everywhere strictly differentiable, with the
derivative `sinh x`.  -/
Complex.hasStrictDerivAt_cosh : ∀ (x : ℂ), HasStrictDerivAt Complex.cosh (Complex.sinh x) x
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.congrRightFunctor_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (E : Type u₃) [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {e f : C ≌ D} (α : e ⟶ f),
  (CategoryTheory.Equivalence.congrRightFunctor E).map α =
    CategoryTheory.Equivalence.mkHom
      ((CategoryTheory.Functor.whiskeringRight E C D).map (CategoryTheory.Equivalence.asNatTrans α))
-- Mathlib.Data.Set.Piecewise
Set.piecewise_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (s : Set α) [inst : (j : α) → Decidable (j ∈ s)] (f g : α → γ)
  (h : β → α), s.piecewise f g ∘ h = (h ⁻¹' s).piecewise (f ∘ h) (g ∘ h)
-- Mathlib.Analysis.BoxIntegral.Partition.Additive
BoxIntegral.BoxAdditiveMap.coe_mk : ∀ {ι : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] {I₀ : WithTop (BoxIntegral.Box ι)} (f : BoxIntegral.Box ι → M)
  (h :
    ∀ (J : BoxIntegral.Box ι),
      ↑J ≤ I₀ → ∀ (π : BoxIntegral.Prepartition J), π.IsPartition → ∑ Ji ∈ π.boxes, f Ji = f J),
  ⇑{ toFun := f, sum_partition_boxes' := h } = f
-- Mathlib.Algebra.Algebra.Unitization
/-- The canonical `R`-algebra projection `Unitization R A → R`.  -/
Unitization.fstHom : (R : Type u_2) →
  (A : Type u_3) →
    [inst : CommSemiring R] →
      [inst_1 : NonUnitalSemiring A] →
        [inst_2 : Module R A] →
          [inst_3 : IsScalarTower R A A] → [inst_4 : SMulCommClass R A A] → Unitization R A →ₐ[R] R
-- Init.Control.Lawful.Basic
LawfulApplicative.mk : ∀ {f : Type u → Type v} [inst : Applicative f] [toLawfulFunctor : LawfulFunctor f],
  (∀ {α β : Type u} (x : f α) (y : f β), x <* y = Function.const β <$> x <*> y) →
    (∀ {α β : Type u} (x : f α) (y : f β), x *> y = Function.const α id <$> x <*> y) →
      (∀ {α β : Type u} (g : α → β) (x : f α), pure g <*> x = g <$> x) →
        (∀ {α β : Type u} (g : α → β) (x : α), g <$> pure x = pure (g x)) →
          (∀ {α β : Type u} (g : f (α → β)) (x : α), g <*> pure x = (fun h => h x) <$> g) →
            (∀ {α β γ : Type u} (x : f α) (g : f (α → β)) (h : f (β → γ)),
                h <*> (g <*> x) = Function.comp <$> h <*> g <*> x) →
              LawfulApplicative f
-- Batteries.Data.String.Matcher
/-- The byte size of the string pattern for the matcher  -/
String.Matcher.patternSize : String.Matcher → ℕ
-- Mathlib.Topology.Sheaves.Limits
TopCat.instHasLimitsOfShapePresheaf : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : CategoryTheory.Category.{v_1, w} J]
  [CategoryTheory.Limits.HasLimitsOfShape J C] (X : TopCat),
  CategoryTheory.Limits.HasLimitsOfShape J (TopCat.Presheaf C X)
-- Lean.Meta.Tactic.Grind.SimpUtil
Lean.Meta.Grind.unfoldReducibleSimproc : Lean.Meta.Simp.DSimproc
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey?_inter_of_mem_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α}, k ∈ m₂ → (m₁ ∩ m₂).getKey? k = m₁.getKey? k
-- Mathlib.NumberTheory.LSeries.Linearity
LSeries.term_smul : ∀ (f : ℕ → ℂ) (c s : ℂ), LSeries.term (c • f) s = c • LSeries.term f s
-- Mathlib.Geometry.Manifold.StructureGroupoid
/-- Members of the structure groupoid are open partial homeomorphisms.  -/
StructureGroupoid.members : {H : Type u_2} → [inst : TopologicalSpace H] → StructureGroupoid H → Set (OpenPartialHomeomorph H H)
-- Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Real.volume_Iic : ∀ {a : ℝ}, MeasureTheory.volume (Set.Iic a) = ⊤
-- Mathlib.NumberTheory.ArithmeticFunction.Defs
ArithmeticFunction.one_apply : ∀ {R : Type u_1} [inst : Zero R] [inst_1 : One R] {x : ℕ}, 1 x = if x = 1 then 1 else 0
-- Mathlib.Algebra.GroupWithZero.Units.Basic
Ring.isUnit_iff_inverse_ne_zero : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [Nontrivial M₀] {x : M₀}, IsUnit x ↔ Ring.inverse x ≠ 0
-- Mathlib.Combinatorics.Hall.Finite
HallMarriageTheorem.hall_cond_of_restrict : ∀ {α : Type v} [inst : DecidableEq α] {ι : Type u} {t : ι → Finset α} {s : Finset ι},
  (∀ (s : Finset ι), s.card ≤ (s.biUnion t).card) → ∀ (s' : Finset ↑↑s), s'.card ≤ (s'.biUnion fun a' => t ↑a').card
-- Mathlib.Data.Matrix.Mul
dotProduct_pUnit : ∀ {α : Type v} [inst : AddCommMonoid α] [inst_1 : Mul α] (v w : PUnit.{u_10 + 1} → α),
  v ⬝ᵥ w = v PUnit.unit * w PUnit.unit
-- Mathlib.Algebra.FreeMonoid.Symbols
FreeAddMonoid.symbols_add : ∀ {α : Type u_1} [inst : DecidableEq α] {a b : FreeAddMonoid α}, (a + b).symbols = a.symbols ∪ b.symbols
-- Mathlib.Data.Nat.Hyperoperation
hyperoperation_three : ∀ (m k : ℕ), hyperoperation 3 m k = m ^ k
-- Mathlib.CategoryTheory.Quotient
CategoryTheory.Quotient.mk.injEq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {r : HomRel C} (as as_1 : C),
  ({ as := as } = { as := as_1 }) = (as = as_1)
-- Init.Data.Array.Lemmas
Array.swapAt.congr_simp : ∀ {α : Type u} (xs xs_1 : Array α) (e_xs : xs = xs_1) (i i_1 : ℕ) (e_i : i = i_1) (v v_1 : α),
  v = v_1 → ∀ (hi : i < xs.size), xs.swapAt i v hi = xs_1.swapAt i_1 v_1 ⋯
-- Mathlib.Algebra.Group.Subsemigroup.Membership
/-- A dependent version of `AddSubsemigroup.iSup_induction`.  -/
AddSubsemigroup.iSup_induction' : ∀ {ι : Sort u_1} {M : Type u_2} [inst : Add M] (S : ι → AddSubsemigroup M) {C : (x : M) → x ∈ ⨆ i, S i → Prop},
  (∀ (i : ι) (x : M) (hxS : x ∈ S i), C x ⋯) →
    (∀ (x y : M) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x + y) ⋯) →
      ∀ {x₁ : M} (hx₁ : x₁ ∈ ⨆ i, S i), C x₁ hx₁
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.sub_linear : ∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V1]
  [inst_2 : Module k V1] [inst_3 : AddTorsor V1 P1] [inst_4 : AddCommGroup V2] [inst_5 : Module k V2]
  (f g : P1 →ᵃ[k] V2), (f - g).linear = f.linear - g.linear
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getD_filter : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] {f : α → β → Bool} {k : α} {fallback : β} (h : m.WF),
  Std.DHashMap.Raw.Const.getD (Std.DHashMap.Raw.filter f m) k fallback =
    ((Std.DHashMap.Raw.Const.get? m k).pfilter fun x h' => f (m.getKey k ⋯) x).getD fallback
-- Mathlib.Data.Matrix.Mul
sum_dotProduct : ∀ {m : Type u_2} {α : Type v} [inst : Fintype m] [inst_1 : NonUnitalNonAssocSemiring α] {ι : Type u_10} (s : Finset ι)
  (u : ι → m → α) (v : m → α), (∑ i ∈ s, u i) ⬝ᵥ v = ∑ i ∈ s, u i ⬝ᵥ v
-- Mathlib.CategoryTheory.Preadditive.Comma
CategoryTheory.instAdditiveCommaSnd : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Preadditive A] {B : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} B] [inst_3 : CategoryTheory.Preadditive B] {T : Type u₃}
  [inst_4 : CategoryTheory.Category.{v₃, u₃} T] [inst_5 : CategoryTheory.Preadditive T] (L : CategoryTheory.Functor A T)
  [inst_6 : L.Additive] (R : CategoryTheory.Functor B T) [inst_7 : R.Additive], (CategoryTheory.Comma.snd L R).Additive
-- Mathlib.GroupTheory.Coset.Basic
LeftAddCosetEquivalence.eq_1 : ∀ {α : Type u_1} [inst : Add α] (s : Set α) (a b : α), LeftAddCosetEquivalence s a b = (a +ᵥ s = b +ᵥ s)
-- Lean.Meta.InferType
/-- Converts an `ArrowPropResult` into a `LBool`. `.bvar _` values are treated as `.undef`.  -/
_private.Lean.Meta.InferType.0.Lean.Meta.ArrowPropResult.toLBool : Lean.Meta.ArrowPropResult✝ → Lean.LBool