mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.Additive.AP.Three.Defs
mulRothNumber_le : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Monoid α] (s : Finset α), mulRothNumber s ≤ s.card
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.leadingTerm_mul : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] [NoZeroDivisors R]
  (p q : MvPolynomial σ R), m.leadingTerm (p * q) = m.leadingTerm p * m.leadingTerm q
-- Mathlib.Data.Multiset.ZeroCons
Multiset.rel_zero_left : ∀ {α : Type u_1} {β : Type v} {r : α → β → Prop} {b : Multiset β}, Multiset.Rel r 0 b ↔ b = 0
-- Std.Sync.CancellationToken
Std.CancellationToken.Consumer.select.inj : ∀ {finished finished_1 : Std.Async.Waiter Unit},
  Std.CancellationToken.Consumer.select finished = Std.CancellationToken.Consumer.select finished_1 →
    finished = finished_1
-- Mathlib.Order.Interval.Finset.Fin
Fin.finsetImage_castAdd_Ioi : ∀ {n : ℕ} (m : ℕ) [inst : NeZero m] (i : Fin n),
  Finset.image (Fin.castAdd m) (Finset.Ioi i) = Finset.Ioo (Fin.castAdd m i) (Fin.natAdd n 0)
-- Lean.Message
/-- Lifted `Format.compose`  -/
Lean.MessageData.compose : Lean.MessageData → Lean.MessageData → Lean.MessageData
-- Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace
WeakDual.CharacterSpace.union_zero : ∀ (𝕜 : Type u_1) (A : Type u_2) [inst : CommSemiring 𝕜] [inst_1 : TopologicalSpace 𝕜] [inst_2 : ContinuousAdd 𝕜]
  [inst_3 : ContinuousConstSMul 𝕜 𝕜] [inst_4 : NonUnitalNonAssocSemiring A] [inst_5 : TopologicalSpace A]
  [inst_6 : Module 𝕜 A], WeakDual.characterSpace 𝕜 A ∪ {0} = {φ | ∀ (x y : A), φ (x * y) = φ x * φ y}
-- Mathlib.Analysis.Convex.StrictConvexSpace
/-- A closed ball in a strictly convex space is strictly convex.  -/
strictConvex_closedBall : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : NormedField 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : NormedAddCommGroup E]
  [inst_3 : NormedSpace 𝕜 E] [StrictConvexSpace 𝕜 E] (x : E) (r : ℝ), StrictConvex 𝕜 (Metric.closedBall x r)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.mem_diff_iff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, k ∈ t₁ \ t₂ ↔ k ∈ t₁ ∧ k ∉ t₂
-- Mathlib.Data.Rat.Cast.Lemmas
Rat.cast_inv_int : ∀ {α : Type u_1} [inst : DivisionRing α] (n : ℤ), ↑(↑n)⁻¹ = (↑n)⁻¹
-- Mathlib.Order.SuccPred.Archimedean
strictMono_of_pred_lt : ∀ {α : Type u_3} {β : Type u_4} [inst : PartialOrder α] [inst_1 : Preorder β] [inst_2 : PredOrder α]
  [IsPredArchimedean α] {f : α → β}, (∀ (a : α), ¬IsMin a → f (Order.pred a) < f a) → StrictMono f
-- Lean.Meta.Tactic.Util
Lean.Meta.TacticResultCNM.modified.injEq : ∀ (mvarId mvarId_1 : Lean.MVarId),
  (Lean.Meta.TacticResultCNM.modified mvarId = Lean.Meta.TacticResultCNM.modified mvarId_1) = (mvarId = mvarId_1)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.mapAddMonNatIso_hom_app_hom : ∀ {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 D]
  {F F' : CategoryTheory.Functor C D} [inst_4 : F.LaxMonoidal] [inst_5 : F'.LaxMonoidal] (e : F ≅ F')
  [inst_6 : CategoryTheory.NatTrans.IsMonoidal e.hom] (X : CategoryTheory.AddMon C),
  ((CategoryTheory.Functor.mapAddMonNatIso e).hom.app X).hom = e.hom.app X.X
-- Mathlib.Data.Sym.Basic
Sym.coe_cast : ∀ {α : Type u_1} {n m : ℕ} {s : Sym α n} (h : n = m), ↑((Sym.cast h) s) = ↑s
-- Mathlib.Algebra.Group.Subgroup.Pointwise
Subgroup.normalizer_le_normalizer_sup_normal : ∀ {G : Type u_2} [inst : Group G] {H K : Subgroup G} [hK : K.Normal],
  Subgroup.normalizer ↑H ≤ Subgroup.normalizer ↑(H ⊔ K)
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.C_eq_natCast : ∀ {R : Type u_1} [inst : Semiring R] [MulSemiringAction (Multiplicative ℕ) R] (n : ℕ), SkewPolynomial.C ↑n = ↑n
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.contains_of_isEmpty : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], (↑m).WF → ∀ {a : α}, (↑m).isEmpty = true → m.contains a = false
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteGrp.ofHom_comp : ∀ {X Y Z : Type u} [inst : Group X] [inst_1 : TopologicalSpace X] [inst_2 : IsTopologicalGroup X]
  [inst_3 : CompactSpace X] [inst_4 : TotallyDisconnectedSpace X] [inst_5 : Group Y] [inst_6 : TopologicalSpace Y]
  [inst_7 : IsTopologicalGroup Y] [inst_8 : CompactSpace Y] [inst_9 : TotallyDisconnectedSpace Y] [inst_10 : Group Z]
  [inst_11 : TopologicalSpace Z] [inst_12 : IsTopologicalGroup Z] [inst_13 : CompactSpace Z]
  [inst_14 : TotallyDisconnectedSpace Z] (f : X →ₜ* Y) (g : Y →ₜ* Z),
  ProfiniteGrp.ofHom (g.comp f) = CategoryTheory.CategoryStruct.comp (ProfiniteGrp.ofHom f) (ProfiniteGrp.ofHom g)
-- Mathlib.CategoryTheory.Limits.Connected
CategoryTheory.ProdPreservesConnectedLimits.forgetCone_π : ∀ {C : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} C] [inst_1 : CategoryTheory.Limits.HasBinaryProducts C]
  {J : Type v₂} [inst_2 : CategoryTheory.SmallCategory J] {X : C} {K : CategoryTheory.Functor J C}
  (s : CategoryTheory.Limits.Cone (K.comp (CategoryTheory.Limits.prod.functor.obj X))),
  (CategoryTheory.ProdPreservesConnectedLimits.forgetCone s).π =
    CategoryTheory.CategoryStruct.comp s.π (CategoryTheory.ProdPreservesConnectedLimits.γ₂ X)
-- Mathlib.Geometry.Manifold.BumpFunction
SmoothBumpFunction.mk.inj : ∀ {E : Type uE} {inst : NormedAddCommGroup E} {inst_1 : NormedSpace ℝ E} {H : Type uH} {inst_2 : TopologicalSpace H}
  {I : ModelWithCorners ℝ E H} {M : Type uM} {inst_3 : TopologicalSpace M} {inst_4 : ChartedSpace H M} {c : M}
  {toContDiffBump : ContDiffBump (↑(extChartAt I c) c)}
  {closedBall_subset :
    Metric.closedBall (↑(extChartAt I c) c) toContDiffBump.rOut ∩ Set.range ↑I ⊆ (extChartAt I c).target}
  {toContDiffBump_1 : ContDiffBump (↑(extChartAt I c) c)}
  {closedBall_subset_1 :
    Metric.closedBall (↑(extChartAt I c) c) toContDiffBump_1.rOut ∩ Set.range ↑I ⊆ (extChartAt I c).target},
  { toContDiffBump := toContDiffBump, closedBall_subset := closedBall_subset } =
      { toContDiffBump := toContDiffBump_1, closedBall_subset := closedBall_subset_1 } →
    toContDiffBump = toContDiffBump_1
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.cokernelSequenceCyclesEIso_hom_τ₂ : ∀ {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.cokernelSequenceCyclesEIso._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.cokernelSequenceCyclesEIso._auto_3),
  (X.cokernelSequenceCyclesEIso f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).hom.τ₂ = (X.cyclesIso f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯).inv
-- Mathlib.Data.Finset.Image
Finset.fiber_nonempty_iff_mem_image : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] {f : α → β} {s : Finset α} {y : β},
  {x ∈ s | f x = y}.Nonempty ↔ y ∈ Finset.image f s
-- Init.Data.List.Nat.Count
/-- The number of elements satisfying a predicate in the tail of a list is
at least one less than the number of elements satisfying the predicate in the list.
 -/
List.le_countP_tail : ∀ {α : Type u_1} {p : α → Bool} {l : List α}, List.countP p l - 1 ≤ List.countP p l.tail
-- Mathlib.Order.Interval.Set.WithBotTop
WithBot.preimage_coe_Icc : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, WithBot.some ⁻¹' Set.Icc ↑b ↑a = Set.Icc b a
-- Mathlib.Algebra.Opposites
MulOpposite.opEquiv.eq_1 : ∀ {α : Type u_1},
  MulOpposite.opEquiv = { toFun := MulOpposite.op, invFun := MulOpposite.unop, left_inv := ⋯, right_inv := ⋯ }
-- Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
_private.Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr.0.Lean.Meta.Grind.Arith.CommRing.mkEq : {M : Type → Type} → [Monad M] → [Lean.Meta.Grind.Arith.CommRing.MonadRing M] → Lean.Expr → Lean.Expr → M Lean.Expr
-- Init.Util
/-- Print stack trace to stderr before evaluating given closure if `cond` is true.
Currently supported on Linux only.
 -/
dbgStackTraceIf : {α : Type u} → Bool → (Unit → α) → α
-- Mathlib.FieldTheory.Finite.Basic
FiniteField.X_pow_card_sub_X_ne_zero : ∀ (K' : Type u_3) [inst : Field K'] {p : ℕ}, 1 < p → Polynomial.X ^ p - Polynomial.X ≠ 0
-- Mathlib.Combinatorics.Quiver.Subquiver
Quiver.instInhabitedLabelling : {V : Type u} → [inst : Quiver V] → (L : Sort u_2) → [Inhabited L] → Inhabited (Quiver.Labelling V L)
-- Std.Internal.Do.WP.Conjunctive
_private.Std.Internal.Do.WP.Conjunctive.0.Std.Internal.Do.EStateM.wpInst.match_1.eq_2 : ∀ {ε σ α : Type} (motive : EStateM.Result ε σ α → Sort u_1) (el : ε) (s' : σ)
  (h_1 : (a : α) → (s' : σ) → motive (EStateM.Result.ok a s'))
  (h_2 : (el : ε) → (s' : σ) → motive (EStateM.Result.error el s')),
  (match EStateM.Result.error el s' with
    | EStateM.Result.ok a s' => h_1 a s'
    | EStateM.Result.error el s' => h_2 el s') =
    h_2 el s'
-- Init.Data.String.Lemmas.IsEmpty
String.copy_sliceFrom_startPos : ∀ {s : String}, (s.sliceFrom s.endPos).copy = ""
-- Mathlib.Topology.Algebra.Ring.Basic
IsTopologicalRing.mk : ∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : NonUnitalNonAssocRing R]
  [toIsTopologicalSemiring : IsTopologicalSemiring R] [toContinuousNeg : ContinuousNeg R], IsTopologicalRing R
-- Mathlib.Algebra.Group.ModEq
AddCommGroup.sub_modEq_iff_modEq_add' : ∀ {G : Type u_1} [inst : AddCommGroup G] {p a b c : G}, a - b ≡ c [PMOD p] ↔ a ≡ b + c [PMOD p]
-- Mathlib.FieldTheory.Relrank
IntermediateField.relfinrank_dvd_of_le_left : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {A B : IntermediateField F E}
  (C : IntermediateField F E), A ≤ B → B.relfinrank C ∣ A.relfinrank C
-- Std.Data.DHashMap.Internal.AssocList.Basic
Std.DHashMap.Internal.AssocList.nil.sizeOf_spec : ∀ {α : Type u} {β : α → Type v} [inst : SizeOf α] [inst_1 : (a : α) → SizeOf (β a)],
  sizeOf Std.DHashMap.Internal.AssocList.nil = 1
-- Mathlib.CategoryTheory.Shift.CommShift
CategoryTheory.Functor.CommShift.isoAdd'_inv_app : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} {A : Type u_4} [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift C A] [inst_4 : CategoryTheory.HasShift D A] {a b c : A} (h : a + b = c)
  (e₁ : (CategoryTheory.shiftFunctor C a).comp F ≅ F.comp (CategoryTheory.shiftFunctor D a))
  (e₂ : (CategoryTheory.shiftFunctor C b).comp F ≅ F.comp (CategoryTheory.shiftFunctor D b)) (X : C),
  (CategoryTheory.Functor.CommShift.isoAdd' h e₁ e₂).inv.app X =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd' D a b c h).hom.app (F.obj X))
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D b).map (e₁.inv.app X))
        (CategoryTheory.CategoryStruct.comp (e₂.inv.app ((CategoryTheory.shiftFunctor C a).obj X))
          (F.map ((CategoryTheory.shiftFunctorAdd' C a b c h).inv.app X))))
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.coe_coe_toAddEquiv_symm : ∀ {R : Type u_4} {S : Type u_5} [inst : Mul R] [inst_1 : Mul S] [inst_2 : Add R] [inst_3 : Add S] (e : R ≃+* S),
  ⇑(↑e).symm = ⇑e.symm
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfcHom_injective : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A] [inst_6 : Ring A]
  [inst_7 : StarRing A] [inst_8 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] {a : A} (ha : p a),
  Function.Injective ⇑(cfcHom ha)
-- Mathlib.AlgebraicTopology.RelativeCellComplex.Basic
HomotopicalAlgebra.RelativeCellComplex.hom_ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w'} [inst_1 : LinearOrder J] [inst_2 : OrderBot J]
  [inst_3 : SuccOrder J] [inst_4 : WellFoundedLT J] {α : J → Type t} {A B : (j : J) → α j → C}
  {basicCell : (j : J) → (i : α j) → A j i ⟶ B j i} {X Y : C} {f : X ⟶ Y}
  (c : HomotopicalAlgebra.RelativeCellComplex basicCell f) {Z : C} {φ₁ φ₂ : Y ⟶ Z},
  CategoryTheory.CategoryStruct.comp f φ₁ = CategoryTheory.CategoryStruct.comp f φ₂ →
    (∀ (γ : c.Cells), CategoryTheory.CategoryStruct.comp γ.ι φ₁ = CategoryTheory.CategoryStruct.comp γ.ι φ₂) → φ₁ = φ₂
-- Mathlib.RingTheory.PrincipalIdealDomain
bot_isPrincipal : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M], ⊥.IsPrincipal
-- Mathlib.Algebra.Category.Grp.Limits
CommGrpCat.forget_createsLimitsOfShape.eq_1 : ∀ (J : Type v) [inst : CategoryTheory.Category.{w, v} J],
  CommGrpCat.forget_createsLimitsOfShape J = { CreatesLimit := fun {K} => inferInstance }
-- Mathlib.NumberTheory.ModularForms.QExpansion
CuspFormClass.zero_at_infty_comp_ofComplex : ∀ {k : ℤ} {F : Type u_1} [inst : FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} (f : F) [CuspFormClass F Γ k]
  [Fact (IsCusp OnePoint.infty Γ)], (Filter.comap Complex.im Filter.atTop).ZeroAtFilter (⇑f ∘ ↑UpperHalfPlane.ofComplex)
-- Mathlib.RingTheory.DedekindDomain.Factorization
FractionalIdeal.count_inv : ∀ {R : Type u_1} [inst : CommRing R] (K : Type u_2) [inst_1 : Field K] [inst_2 : Algebra R K]
  [inst_3 : IsFractionRing R K] [inst_4 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R)
  (I : FractionalIdeal (nonZeroDivisors R) K), FractionalIdeal.count K v I⁻¹ = -FractionalIdeal.count K v I
-- Init.Data.String.Lemmas.Pattern.Find.Pred
String.Slice.Pos.find?_bool_eq_some_iff_splits : ∀ {p : Char → Bool} {s : String.Slice} {pos : s.Pos} {t u : String},
  pos.Splits t u →
    ∀ {pos' : s.Pos},
      pos.find? p = some pos' ↔
        ∃ v c w, pos'.Splits (t ++ v) (String.singleton c ++ w) ∧ p c = true ∧ ∀ d ∈ v.toList, p d = false
-- Mathlib.NumberTheory.LSeries.PrimesInAP
/-- **Dirichlet's Theorem** on primes in arithmetic progression: if `q` is a positive
integer and `a : ℤ` is coprime to `q`, then there are infinitely many prime numbers `p`
such that `p ≡ a mod q`.  -/
Nat.forall_exists_prime_gt_and_zmodEq : ∀ (n : ℕ) {q : ℕ} {a : ℤ}, q ≠ 0 → IsCoprime a ↑q → ∃ p > n, Nat.Prime p ∧ ↑p ≡ a [ZMOD ↑q]
-- Mathlib.Algebra.Category.Semigrp.Basic
/-- The underlying `AddHom`.  -/
AddSemigrp.Hom.hom' : {A B : AddSemigrp} → A.Hom B → ↑A →ₙ+ ↑B
-- Mathlib.LinearAlgebra.Eigenspace.Basic
/-- A scalar `μ` is an eigenvalue for a linear map `f` if there are nonzero vectors `x`
such that `f x = μ • x`. (Def 5.5 of [axler2024]).  -/
Module.End.HasEigenvalue : {R : Type v} →
  {M : Type w} → [inst : CommRing R] → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → Module.End R M → R → Prop
-- Mathlib.Logic.IsEmpty.Defs
PProd.isEmpty_left : ∀ {α : Sort u} {β : Sort v} [IsEmpty α], IsEmpty (α ×' β)
-- Mathlib.NumberTheory.ArithmeticFunction.Defs
ArithmeticFunction.IsMultiplicative.map_gcd : ∀ {R : Type u_1} [inst : CommGroupWithZero R] {f : ArithmeticFunction R},
  f.IsMultiplicative → ∀ {x y : ℕ}, f (x.lcm y) ≠ 0 → f (x.gcd y) = f x * f y / f (x.lcm y)
-- Mathlib.Algebra.Group.Action.TransferInstance
/-- Transfer `IsScalarTower` across an `Equiv`  -/
Equiv.isScalarTower : ∀ (M : Type u_1) (N : Type u_2) {α : Type u_4} {β : Type u_5} [inst : SMul M N] [inst_1 : SMul M β] [inst_2 : SMul N β]
  (e : α ≃ β) [IsScalarTower M N β], IsScalarTower M N α
-- Mathlib.Data.Set.Subsingleton
Set.eq_singleton_or_nontrivial : ∀ {α : Type u} {a : α} {s : Set α}, a ∈ s → s = {a} ∨ s.Nontrivial
-- Mathlib.Geometry.Convex.Cone.Basic
ConvexCone.convex : ∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] (C : ConvexCone R M), Convex R ↑C
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalSubsemiring.closure_addSubmonoid_closure : ∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R] {s : Set R},
  NonUnitalSubsemiring.closure ↑(AddSubmonoid.closure s) = NonUnitalSubsemiring.closure s
-- Lean.Parser.Term
Lean.Parser.Term.proj.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Combinatorics.Quiver.Covering
Quiver.starEquivCostar_symm_apply_fst : ∀ {U : Type u_1} [inst : Quiver U] [inst_1 : Quiver.HasInvolutiveReverse U] (u : U) (e : Quiver.Costar u),
  ((Quiver.starEquivCostar u).symm e).fst = e.fst
-- Mathlib.Geometry.Manifold.Algebra.Monoid
/-- **Alias** of `contMDiffOn_finsetSum'`. -/
contMDiffOn_finset_sum' : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_3}
  [inst_1 : TopologicalSpace H] {E : Type u_4} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E]
  {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [inst_4 : AddCommMonoid G] [inst_5 : TopologicalSpace G]
  [inst_6 : ChartedSpace H G] [ContMDiffAdd I n G] {E' : Type u_6} [inst_8 : NormedAddCommGroup E']
  [inst_9 : NormedSpace 𝕜 E'] {H' : Type u_7} [inst_10 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M : Type u_8} [inst_11 : TopologicalSpace M] [inst_12 : ChartedSpace H' M] {s : Set M} {t : Finset ι}
  {f : ι → M → G}, (∀ i ∈ t, ContMDiffOn I' I n (f i) s) → ContMDiffOn I' I n (∑ i ∈ t, f i) s
-- Mathlib.Topology.VectorBundle.Basic
Bundle.Trivialization.coe_linearMapAt_of_mem : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : Semiring R] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace B] [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_4 : AddCommMonoid F]
  [inst_5 : Module R F] [inst_6 : (x : B) → AddCommMonoid (E x)] [inst_7 : (x : B) → Module R (E x)]
  (e : Bundle.Trivialization F Bundle.TotalSpace.proj) [inst_8 : Bundle.Trivialization.IsLinear R e] {b : B},
  b ∈ e.baseSet → ⇑(Bundle.Trivialization.linearMapAt R e b) = fun y => (↑e ⟨b, y⟩).2
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.instIsDomainSubtypeMem : ∀ {K : Type u} [inst : Field K] (A : ValuationSubring K), IsDomain ↥A
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mapLeft_obj_right : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (R : CategoryTheory.Functor B T)
  {L₁ L₂ : CategoryTheory.Functor A T} (l : L₁ ⟶ L₂) (X : CategoryTheory.Comma L₂ R),
  ((CategoryTheory.Comma.mapLeft R l).obj X).right = X.right
-- Mathlib.Analysis.Convex.Star
StarConvex.affinity : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : CommSemiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] {x : E} {s : Set E},
  StarConvex 𝕜 x s → ∀ (z : E) (c : 𝕜), StarConvex 𝕜 (z + c • x) ((fun x => z + c • x) '' s)
-- Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne
SimplexCategory.toMk₁_bijective : ∀ {n : ℕ}, Function.Bijective SimplexCategory.toMk₁
-- Init.Data.Int.OfNat
Nat.ToInt.mod_congr : ∀ {a b : ℕ} {a' b' : ℤ}, ↑a = a' → ↑b = b' → ↑(a % b) = a' % b'
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
/-- **Alias** of `CategoryTheory.Functor.PushoutObjObj.flip_ι`. -/
CategoryTheory.Functor.PushoutObjObj.ι_flip : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)} {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} {X₂ Y₂ : C₂} {f₂ : X₂ ⟶ Y₂}
  (sq : F.PushoutObjObj f₁ f₂), sq.flip.ι = sq.ι
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instModule : {R : Type u_1} →
  {M : Type u_3} →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          [inst_3 : TopologicalSpace M] →
            [inst_4 : ContinuousAdd M] → [ContinuousConstSMul R M] → Module R (SeparationQuotient M)
-- Mathlib.Algebra.GroupWithZero.NonZeroDivisors
/-- Let `M₀` be a monoid with zero and `M` an additive monoid with an `M₀`-action, then the
collection of non-zero smul-divisors forms a submonoid.

These elements are also called `M`-regular.  -/
nonZeroSMulDivisors : (M₀ : Type u_1) → [inst : MonoidWithZero M₀] → (M : Type u_2) → [Zero M] → [MulAction M₀ M] → Submonoid M₀
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Submonoid.isLocalizationMap_iff : ∀ {M : Type u_1} [inst : CommMonoid M] {N : Type u_2} [inst_1 : CommMonoid N] (S : Submonoid M) (f : M → N),
  S.IsLocalizationMap f ↔
    (∀ (y : ↥S), IsUnit (f ↑y)) ∧ (∀ (z : N), ∃ x, z * f ↑x.2 = f x.1) ∧ ∀ {x y : M}, f x = f y → ∃ c, ↑c * x = ↑c * y
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.kerFunctor_map : ∀ (Y : AlgebraicGeometry.Scheme) {f g : (CategoryTheory.Over Y)ᵒᵖ} (hfg : f ⟶ g),
  Y.kerFunctor.map hfg = CategoryTheory.homOfLE ⋯
-- Batteries.Recycling.RBTree.WF
RBTree.RBNode.reverse_ins : ∀ {α : Type u_1} {cmp : α → α → Ordering} {x : α} [inst : Std.OrientedCmp cmp] {t : RBTree.RBNode α},
  (RBTree.RBNode.ins cmp x t).reverse = RBTree.RBNode.ins (flip cmp) x t.reverse
-- Mathlib.Topology.Homotopy.Equiv
ContinuousMap.HomotopyEquiv.trans_symm_apply : ∀ {X : Type u} {Y : Type v} {Z : Type w} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] (h₁ : ContinuousMap.HomotopyEquiv X Y) (h₂ : ContinuousMap.HomotopyEquiv Y Z) (a : Z),
  (h₁.trans h₂).symm.toFun a = h₁.symm.toFun (h₂.symm.toFun a)
-- Mathlib.Combinatorics.SetFamily.AhlswedeZhang
/-- Weighted sum of the size of the truncated infima of a set family. Relevant to the
Ahlswede-Zhang identity.  -/
AhlswedeZhang.infSum : {α : Type u_1} → [Fintype α] → [DecidableEq α] → Finset (Finset α) → ℚ
-- Batteries.Data.List.Basic
List.instUnionOfBEq_batteries : {α : Type u_1} → [BEq α] → Union (List α)
-- Lean.Meta.Constructions.SparseCasesOn
Lean.Meta.SparseCasesOnInfo.mk : Lean.Name → ℕ → ℕ → Array Lean.Name → Lean.Meta.SparseCasesOnInfo
-- Mathlib.CategoryTheory.Yoneda
/-- Representing objects are unique up to isomorphism.  -/
CategoryTheory.Functor.RepresentableBy.uniqueUpToIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {F : CategoryTheory.Functor Cᵒᵖ (Type v)} → {Y Y' : C} → F.RepresentableBy Y → F.RepresentableBy Y' → (Y ≅ Y')
-- Mathlib.Topology.Algebra.Module.Star
/-- If `A` is a topological module over a commutative `R` with trivial star and compatible actions,
then `star` is a continuous linear equivalence.  -/
starL' : (R : Type u_1) →
  {A : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : StarRing R] →
        [inst_2 : AddCommMonoid A] →
          [inst_3 : StarAddMonoid A] →
            [inst_4 : Module R A] →
              [StarModule R A] → [inst_6 : TopologicalSpace A] → [ContinuousStar A] → [TrivialStar R] → A ≃L[R] A
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
CategoryTheory.ObjectProperty.colimitsOfShape_bot : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (J : Type u')
  [inst_1 : CategoryTheory.Category.{v', u'} J] [Nonempty J], ⊥.colimitsOfShape J = ⊥
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.roots.eq_1 : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] (p : Polynomial R),
  p.roots = if h : p = 0 then ∅ else Classical.choose ⋯
-- Mathlib.Algebra.Category.MonCat.Basic
/-- The forgetful functor from `CommMonCat` to `MonCat` is fully faithful.  -/
CommMonCat.fullyFaithfulForgetToMonCat : (CategoryTheory.forget₂ CommMonCat MonCat).FullyFaithful
-- Init.Data.String.Lemmas.FindPos
String.Pos.posGE_offset : ∀ {s : String} {p : s.Pos}, s.posGE p.offset ⋯ = p
-- Mathlib.LinearAlgebra.Matrix.Gershgorin
/-- **Gershgorin's circle theorem**: for any eigenvalue `μ` of a square matrix `A`, there exists an
index `k` such that `μ` lies in the closed ball of center the diagonal term `A k k` and of
radius the sum of the norms `∑ j ≠ k, ‖A k j‖`.  -/
eigenvalue_mem_ball : ∀ {K : Type u_1} {n : Type u_2} [inst : NormedField K] [inst_1 : Fintype n] [inst_2 : DecidableEq n] {A : Matrix n n K}
  {μ : K},
  Module.End.HasEigenvalue (Matrix.toLin' A) μ → ∃ k, μ ∈ Metric.closedBall (A k k) (∑ j ∈ Finset.univ.erase k, ‖A k j‖)
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.bddAbove_range : ∀ {ι : Type u_1} [Small.{u, u_1} ι] (f : ι → Cardinal.{u}), BddAbove (Set.range f)