mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Convex.Function
/-- A strictly concave function admits at most one global maximum.  -/
StrictConcaveOn.eq_of_isMaxOn : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommMonoid β] [inst_4 : PartialOrder β] [IsOrderedAddMonoid β] [inst_6 : AddCommMonoid E]
  [inst_7 : SMul 𝕜 E] [inst_8 : Module 𝕜 β] [PosSMulMono 𝕜 β] {f : E → β} {s : Set E} {x y : E},
  StrictConcaveOn 𝕜 s f → IsMaxOn f s x → IsMaxOn f s y → x ∈ s → y ∈ s → x = y
-- Mathlib.CategoryTheory.Monoidal.Closed.Cartesian
/-- If an initial object `I` exists in a CCC then it is a strict initial object,
i.e. any morphism to `I` is an iso.
This actually shows a slightly stronger version: any morphism to an initial object from an
exponentiable object is an isomorphism.
 -/
CategoryTheory.strict_initial : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] {A : C}
  [CategoryTheory.Closed A] {I : C} (t : CategoryTheory.Limits.IsInitial I) (f : A ⟶ I), CategoryTheory.IsIso f
-- Mathlib.Algebra.Homology.DerivedCategory.Plus
DerivedCategory.Plus.isLE_ι_obj_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] (X : DerivedCategory.Plus C) (n : ℤ), (DerivedCategory.Plus.ι.obj X).IsLE n ↔ X.IsLE n
-- Lean.Parser.Extra
/-- The parser `name` parses a name literal like `` `foo``. The syntax is the same as for identifiers
(see `ident`) but with a leading backquote.

This parser has arity 1: it produces a `nameLitKind` node containing the raw literal
(including the backquote).
You can use `TSyntax.getName` to extract the name from the resulting syntax object.  -/
Lean.Parser.nameLit : Lean.Parser.Parser
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.SplitSource.guard.injEq : ∀ (origin origin_1 : Lean.Meta.Grind.Origin),
  (Lean.Meta.Grind.SplitSource.guard origin = Lean.Meta.Grind.SplitSource.guard origin_1) = (origin = origin_1)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.Point.instInvolutiveNeg : {R : Type r} → [inst : CommRing R] → {W' : WeierstrassCurve.Affine R} → InvolutiveNeg W'.Point
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.instRing : {α : Type u} →
  [inst : TopologicalSpace α] → {R : Type u_1} → [inst_1 : SeminormedRing R] → Ring (BoundedContinuousFunction α R)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getD_union_of_not_mem_left : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {m₁ m₂ : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  m₁.WF →
    m₂.WF →
      ∀ {k : α} {fallback : β},
        k ∉ m₁ → Std.DTreeMap.Raw.Const.getD (m₁ ∪ m₂) k fallback = Std.DTreeMap.Raw.Const.getD m₂ k fallback
-- Mathlib.Topology.Order.NhdsSet
nhdsSet_Ioi : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderClosedTopology α] {a : α},
  nhdsSet (Set.Ioi a) = Filter.principal (Set.Ioi a)
-- Init.Data.Int.Gcd
Int.gcd_ne_zero_right : ∀ {b a : ℤ}, b ≠ 0 → a.gcd b ≠ 0
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.Multicofork.ofSigmaCofork_ι_app_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape}
  {I : CategoryTheory.Limits.MultispanIndex J C} {c : CategoryTheory.Limits.Cofan I.left}
  (hc : CategoryTheory.Limits.IsColimit c) {d : CategoryTheory.Limits.Cofan I.right}
  (a : CategoryTheory.Limits.Cofork (I.fstSigmaMapOfIsColimit d hc) (I.sndSigmaMapOfIsColimit d hc)) (i : J.L),
  (CategoryTheory.Limits.Multicofork.ofSigmaCofork a).ι.app (CategoryTheory.Limits.WalkingMultispan.left i) =
    CategoryTheory.CategoryStruct.comp (c.inj i)
      (CategoryTheory.CategoryStruct.comp (I.fstSigmaMapOfIsColimit d hc) a.π)
-- Std.Sat.CNF.Basic
/-- `Clause` `c` occurs in `CNF` formula `f`.
 -/
Std.Sat.CNF.Mem : {α : Type u_1} → Std.Sat.CNF α → Std.Sat.CNF.Clause α → Prop
-- Mathlib.Topology.CompactOpen
Filter.Tendsto.compCM : ∀ {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] [LocallyCompactPair Y Z] {α : Type u_6} {l : Filter α} {g : α → C(Y, Z)} {g₀ : C(Y, Z)}
  {f : α → C(X, Y)} {f₀ : C(X, Y)},
  Filter.Tendsto g l (nhds g₀) →
    Filter.Tendsto f l (nhds f₀) → Filter.Tendsto (fun a => (g a).comp (f a)) l (nhds (g₀.comp f₀))
-- Mathlib.Algebra.Order.Group.Basic
zpow_lt_zpow_right : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] {m n : ℤ} {a : α},
  1 < a → m < n → a ^ m < a ^ n
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
/-- Similar to `stronglyMeasurable.approx`, but enforces that the norm of every function in the
sequence is less than `c` everywhere. If `‖f x‖ ≤ c` this sequence of simple functions verifies
`Tendsto (fun n => hf.approxBounded n x) atTop (𝓝 (f x))`.  -/
MeasureTheory.StronglyMeasurable.approxBounded : {α : Type u_1} →
  {β : Type u_2} →
    {f : α → β} →
      [inst : TopologicalSpace β] →
        {x : MeasurableSpace α} →
          [Norm β] → [SMul ℝ β] → MeasureTheory.StronglyMeasurable f → ℝ → ℕ → MeasureTheory.SimpleFunc α β
-- Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
/-- The Jacobi symbol of `a` and `b`  -/
jacobiSym : ℤ → ℕ → ℤ
-- Lean.Parser.Basic
Lean.Parser.numLitNoAntiquot : Lean.Parser.Parser
-- Mathlib.AlgebraicTopology.DoldKan.GammaCompN
AlgebraicTopology.DoldKan.N₁Γ₀_hom_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasFiniteCoproducts C] (K : ChainComplex C ℕ),
  AlgebraicTopology.DoldKan.N₁Γ₀.hom.app K =
    CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.Γ₀.splitting K).toKaroubiNondegComplexIsoN₁.inv
      ((CategoryTheory.Idempotents.toKaroubi (ChainComplex C ℕ)).map
        (AlgebraicTopology.DoldKan.Γ₀NondegComplexIso K).hom)
-- Mathlib.Algebra.Algebra.Subalgebra.MulOpposite
Subalgebra.unop_op : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  (S : Subalgebra R A), S.op.unop = S
-- Mathlib.Algebra.Polynomial.Module.Basic
PolynomialModule.exists : ∀ {R : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {P : PolynomialModule R M → Prop}, (∃ p, P p) ↔ ∃ q, P { coeff := q }
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.singletonZeroHom_apply : ∀ {α : Type u_2} [inst : Zero α] (a : α), Finset.singletonZeroHom a = {a}
-- Mathlib.Combinatorics.Matroid.Dual
Matroid.dual_isBase_iff' : ∀ {α : Type u_1} {M : Matroid α} {B : Set α}, M✶.IsBase B ↔ M.IsBase (M.E \ B) ∧ B ⊆ M.E
-- Mathlib.CategoryTheory.Monoidal.Multifunctor
CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.secondMap₃_app_app_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {D : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F : CategoryTheory.Functor C D}
  (δ : CategoryTheory.MonoidalCategory.curriedTensorPost F ⟶ CategoryTheory.MonoidalCategory.curriedTensorPre F)
  (X₁ X₂ X₃ : C),
  (((CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.secondMap₃ δ).app X₁).app X₂).app X₃ =
    CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X₁) ((δ.app X₂).app X₃)
-- Mathlib.Order.SuccPred.Archimedean
IsPredArchimedean.mk : ∀ {α : Type u_3} [inst : Preorder α] [inst_1 : PredOrder α],
  (∀ {a b : α}, a ≤ b → ∃ n, Order.pred^[n] b = a) → IsPredArchimedean α
-- Mathlib.Topology.Sheaves.EtaleSpace
/-- The base point.  -/
TopCat.Presheaf.EtaleSpace.base : {X : TopCat} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {CC : C → Type v} →
        {FC : C → C → Type w} →
          [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] →
            [inst_2 : CategoryTheory.ConcreteCategory C FC] →
              [inst_3 : CategoryTheory.Limits.HasColimits C] → {F : TopCat.Presheaf C X} → F.EtaleSpace → ↑X
-- Mathlib.Algebra.Group.Action.Defs
/-- The right and left actions of `M` on `α` are equal.  -/
IsCentralScalar.op_smul_eq_smul : ∀ {M : Type u_9} {α : Type u_10} {inst : SMul M α} {inst_1 : SMul Mᵐᵒᵖ α} [self : IsCentralScalar M α] (m : M) (a : α),
  MulOpposite.op m • a = m • a
-- Mathlib.NumberTheory.ModularForms.SlashInvariantForms
SlashInvariantForm.instIsSMulApplyUpperHalfPlaneComplex : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} [inst : Γ.HasDetOne] {α : Type u_2} [inst_1 : SMul α ℂ]
  [inst_2 : IsScalarTower α ℂ ℂ], IsSMulApply α (SlashInvariantForm Γ k) UpperHalfPlane ℂ
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.toFinsupp_C_mul_X : ∀ {R : Type u} [inst : Semiring R] (a : R), (Polynomial.C a * Polynomial.X).toFinsupp = AddMonoidAlgebra.single 1 a
-- Mathlib.CategoryTheory.Category.Quiv
/-- Prefunctors between quivers define arrows in `Quiv`.  -/
CategoryTheory.Prefunctor.toQuivHom : {C D : Type u} →
  [inst : Quiver C] → [inst_1 : Quiver D] → C ⥤q D → (CategoryTheory.Quiv.of C ⟶ CategoryTheory.Quiv.of D)
-- Mathlib.AlgebraicTopology.SimplicialSet.Nerve
/-- The nerve of a category  -/
CategoryTheory.nerve : (C : Type u) → [CategoryTheory.Category.{v, u} C] → SSet
-- Mathlib.Data.Set.Lattice.Image
Set.kernImage_empty : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, Set.kernImage f ∅ = (Set.range f)ᶜ
-- Mathlib.Algebra.GroupWithZero.Prod
Prod.instMonoidWithZero : {M₀ : Type u_1} → {N₀ : Type u_2} → [MonoidWithZero M₀] → [MonoidWithZero N₀] → MonoidWithZero (M₀ × N₀)
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.le_set_normalizer_iff : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} {s : Set G},
  H ≤ Subgroup.normalizer s ↔ ∀ h ∈ H, ∀ g ∈ s, h * g * h⁻¹ ∈ s
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.containsThenInsertIfNew!_snd_eq_insertIfNew! : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (t : Std.DTreeMap.Internal.Impl α β) (a : α) (b : β a),
  (Std.DTreeMap.Internal.Impl.containsThenInsertIfNew! a b t).2 = Std.DTreeMap.Internal.Impl.insertIfNew! a b t
-- Batteries.Data.UnionFind.Lemmas
Batteries.UnionFind.parent_push : ∀ {a : ℕ} {m : Batteries.UnionFind}, m.push.parent a = m.parent a
-- Lean.Parser.Term
/-- `value_of% x` elaborates to the value of `x`, which can be a local or global definition.
 -/
Lean.Parser.Term.valueOf : Lean.Parser.Parser
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.isoMk_inv_right : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {P : CategoryTheory.MorphismProperty T}
  {Q : CategoryTheory.MorphismProperty A} {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative]
  [inst_4 : W.IsMultiplicative] [inst_5 : Q.RespectsIso] [inst_6 : W.RespectsIso]
  {X Y : CategoryTheory.MorphismProperty.Comma L R P Q W} (l : X.left ≅ Y.left) (r : X.right ≅ Y.right)
  (h :
    autoParam
      (CategoryTheory.CategoryStruct.comp (L.map l.hom) Y.hom = CategoryTheory.CategoryStruct.comp X.hom (R.map r.hom))
      CategoryTheory.MorphismProperty.Comma.isoMk._auto_1),
  (CategoryTheory.MorphismProperty.Comma.isoMk l r h).inv.right = r.inv
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.maxKey!_eq_maxKey! : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : Inhabited α] [inst_3 : BEq α]
  [Std.LawfulBEqOrd α] {t : Std.DTreeMap.Internal.Impl α β},
  t.Ordered → t.maxKey! = Std.Internal.List.maxKey! t.toListModel
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.image_neg_of_apply_neg_eq : ∀ {α : Type u_2} {β : Type u_3} [inst : InvolutiveNeg α] {s : Set α} {f g : α → β},
  (∀ x ∈ s, f (-x) = g x) → f '' (-s) = g '' s
-- Mathlib.Topology.Order.OrderClosed
BddAbove.of_closure : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : Preorder α] {s : Set α}, BddAbove (closure s) → BddAbove s
-- Mathlib.RingTheory.Ideal.Span
Ideal.span_iUnion : ∀ {α : Type u} [inst : Semiring α] {ι : Sort u_1} (s : ι → Set α), Ideal.span (⋃ i, s i) = ⨆ i, Ideal.span (s i)
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.CosimplicialObject.Augmented.toArrow_obj_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject.Augmented C),
  (CategoryTheory.CosimplicialObject.Augmented.toArrow.obj X).right = X.right.obj { len := 0 }
-- Mathlib.Topology.ContinuousMap.Algebra
/-- Coercion to a function as an `AlgHom`.  -/
ContinuousMap.coeFnAlgHom : {α : Type u_1} →
  [inst : TopologicalSpace α] →
    (R : Type u_2) →
      [inst_1 : CommSemiring R] →
        {A : Type u_3} →
          [inst_2 : TopologicalSpace A] →
            [inst_3 : Semiring A] → [inst_4 : Algebra R A] → [inst_5 : IsTopologicalSemiring A] → C(α, A) →ₐ[R] α → A
-- Mathlib.Algebra.Group.Action.Defs
op_smul_eq_mul : ∀ {α : Type u_9} [inst : Mul α] (a b : α), MulOpposite.op a • b = b * a
-- Mathlib.CategoryTheory.Comma.Over.OverClass
CategoryTheory.OverClass.asOverHom_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (S : C) [inst_1 : CategoryTheory.OverClass X S]
  [inst_2 : CategoryTheory.OverClass Y S] [inst_3 : CategoryTheory.OverClass Z S] (f : X ⟶ Y) (g : Y ⟶ Z)
  [inst_4 : CategoryTheory.HomIsOver f S] [inst_5 : CategoryTheory.HomIsOver g S],
  CategoryTheory.OverClass.asOverHom S (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.OverClass.asOverHom S f) (CategoryTheory.OverClass.asOverHom S g)
-- Aesop.BaseM
Aesop.BaseM.instMonadHashMapCacheAdapterExprEntry : Lean.MonadHashMapCacheAdapter Lean.Expr Aesop.RulePatternCache.Entry Aesop.BaseM
-- Mathlib.Analysis.Fourier.Notation
FourierInvModule.mk.inj : ∀ {R : Type u_5} {E : Type u_6} {F : outParam (Type u_7)} {inst : Add E} {inst_1 : Add F} {inst_2 : SMul R E}
  {inst_3 : SMul R F} {toFourierTransformInv : FourierTransformInv E F}
  {fourierInv_add :
    ∀ (f g : E),
      FourierTransformInv.fourierInv (f + g) = FourierTransformInv.fourierInv f + FourierTransformInv.fourierInv g}
  {fourierInv_smul : ∀ (r : R) (f : E), FourierTransformInv.fourierInv (r • f) = r • FourierTransformInv.fourierInv f}
  {toFourierTransformInv_1 : FourierTransformInv E F}
  {fourierInv_add_1 :
    ∀ (f g : E),
      FourierTransformInv.fourierInv (f + g) = FourierTransformInv.fourierInv f + FourierTransformInv.fourierInv g}
  {fourierInv_smul_1 :
    ∀ (r : R) (f : E), FourierTransformInv.fourierInv (r • f) = r • FourierTransformInv.fourierInv f},
  { toFourierTransformInv := toFourierTransformInv, fourierInv_add := fourierInv_add,
        fourierInv_smul := fourierInv_smul } =
      { toFourierTransformInv := toFourierTransformInv_1, fourierInv_add := fourierInv_add_1,
        fourierInv_smul := fourierInv_smul_1 } →
    toFourierTransformInv = toFourierTransformInv_1
-- Mathlib.Algebra.BigOperators.Expect
/-- Delaborator for `Finset.expect`. The `pp.funBinderTypes` option controls whether
to show the domain type when the expect is over `Finset.univ`.  -/
BigOperators.delabFinsetExpect : Lean.PrettyPrinter.Delaborator.Delab
-- Init.Data.String.Pattern.String
_private.Init.Data.String.Pattern.String.0.String.Slice.Pattern.ForwardSliceSearcher.instIteratorIdSearchStep.match_3.splitter : (s : String.Slice) →
  (motive :
      Std.IterStep (Std.IterM Id (String.Slice.Pattern.SearchStep s)) (String.Slice.Pattern.SearchStep s) → Sort u_1) →
    (x : Std.IterStep (Std.IterM Id (String.Slice.Pattern.SearchStep s)) (String.Slice.Pattern.SearchStep s)) →
      ((it' : Std.IterM Id (String.Slice.Pattern.SearchStep s)) →
          (out : String.Slice.Pattern.SearchStep s) → motive (Std.IterStep.yield it' out)) →
        ((it' : Std.IterM Id (String.Slice.Pattern.SearchStep s)) → motive (Std.IterStep.skip it')) →
          (Unit → motive Std.IterStep.done) → motive x
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem!_alter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k k' : α}
  [inst : Inhabited β] {f : Option β → Option β},
  (t.alter k f)[k']! = if cmp k k' = Ordering.eq then (f t[k]?).get! else t[k']!
-- Mathlib.Order.LiminfLimsup
Filter.limsInf_le_of_le : ∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {f : Filter α} {a : α},
  autoParam (Filter.IsBounded (fun x1 x2 => x1 ≥ x2) f) Filter.limsInf_le_of_le._auto_1 →
    (∀ (b : α), (∀ᶠ (n : α) in f, b ≤ n) → b ≤ a) → f.limsInf ≤ a
-- Mathlib.RingTheory.AdicCompletion.Basic
IsPrecomplete.map_algebraMap_iff : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] {I : Ideal R} {M : Type u_4} [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : CommRing S] [inst_4 : Module S M] [inst_5 : Algebra R S] [IsScalarTower R S M],
  IsPrecomplete (Ideal.map (algebraMap R S) I) M ↔ IsPrecomplete I M
-- Mathlib.Algebra.MonoidAlgebra.Basic
/-- **Alias** of `AddMonoidAlgebra.lift_mapRingHom_algebraMap`. -/
AddMonoidAlgebra.lift_mapRangeRingHom_algebraMap : ∀ {R : Type u_1} {S : Type u_2} {A : Type u_4} {M : Type u_7} [inst : CommSemiring R] [inst_1 : AddMonoid M]
  [inst_2 : Semiring A] [inst_3 : Algebra R A] [inst_4 : CommSemiring S] [inst_5 : Algebra S A] [inst_6 : Algebra R S]
  [IsScalarTower R S A] (f : Multiplicative M →* A) (x : AddMonoidAlgebra R M),
  ((AddMonoidAlgebra.lift S A M) f) ((AddMonoidAlgebra.mapRingHom M (algebraMap R S)) x) =
    ((AddMonoidAlgebra.lift R A M) f) x
-- Mathlib.RingTheory.MvPowerSeries.Order
/-- The order of a formal power series is at least `n` if
the `d`th coefficient is `0` for all `d` such that `weight w d < n`.  -/
MvPowerSeries.nat_le_weightedOrder : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (w : σ → ℕ) {f : MvPowerSeries σ R} {n : ℕ},
  (∀ (d : σ →₀ ℕ), (Finsupp.weight w) d < n → (MvPowerSeries.coeff d) f = 0) → ↑n ≤ MvPowerSeries.weightedOrder w f
-- Mathlib.CategoryTheory.Limits.Elements
CategoryTheory.CategoryOfElements.instHasInitialElementsOppositeOfIsRepresentable : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type u_1)}
  [F.IsRepresentable], CategoryTheory.Limits.HasInitial F.Elements
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
SzemerediRegularity.card_eq_of_mem_parts_chunk : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {P : Finpartition Finset.univ} {hP : P.IsEquipartition}
  {G : SimpleGraph α} [inst_2 : DecidableRel G.Adj] {ε : ℝ} {U : Finset α} {hU : U ∈ P.parts} {s : Finset α},
  s ∈ (SzemerediRegularity.chunk hP G ε hU).parts →
    s.card = Fintype.card α / SzemerediRegularity.stepBound P.parts.card ∨
      s.card = Fintype.card α / SzemerediRegularity.stepBound P.parts.card + 1
-- Init.Control.Option
OptionT.instMonadAttach : {m : Type u → Type v} → [Monad m] → [MonadAttach m] → MonadAttach (OptionT m)
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.CosimplicialObject.Augmented.const_obj_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C),
  (CategoryTheory.CosimplicialObject.Augmented.const.obj X).hom =
    CategoryTheory.CategoryStruct.id ((CategoryTheory.CosimplicialObject.const C).obj X)
-- Mathlib.AlgebraicTopology.SingularSet
sSetTopAdj_unit_app_app_down : ∀ (S : SSet) (m : SimplexCategoryᵒᵖ) (a : S.obj m),
  ((CategoryTheory.ConcreteCategory.hom ((sSetTopAdj.unit.app S).app m)) a).down =
    CategoryTheory.CategoryStruct.comp (SSet.toTopSimplex.inv.app (Opposite.unop m))
      (SSet.toTop.map (SSet.yonedaEquiv.symm a))
-- Mathlib.Topology.Homeomorph.Defs
IsHomeomorph.toEquiv_homeomorph : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X → Y)
  (hf : IsHomeomorph f), (IsHomeomorph.homeomorph f hf).toEquiv = Equiv.ofBijective f ⋯
-- Mathlib.Algebra.Algebra.RestrictScalars
/-- `RestrictScalars.addEquiv` is the additive equivalence with the original module.  -/
RestrictScalars.addEquiv : (R : Type u_1) → (S : Type u_2) → (M : Type u_3) → [inst : AddCommMonoid M] → RestrictScalars R S M ≃+ M
-- Mathlib.MeasureTheory.Measure.Count
/-- **Alias** of the reverse direction of `MeasureTheory.Measure.count_ne_zero_iff`. -/
MeasureTheory.Measure.count_ne_zero : ∀ {α : Type u_1} [inst : MeasurableSpace α] {s : Set α}, s.Nonempty → MeasureTheory.Measure.count s ≠ 0
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.ofArray.eq_1 : ∀ {R : Type u_7} {m n : ℕ} (A : Array R) (hA : A.size = m * n) (i : Fin m) (j : Fin n),
  Matrix.ofArray A hA i j = A[i.mkDivMod j]
-- Mathlib.Data.Num.Prime
Num.decidablePrime : DecidablePred Num.Prime
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- Given f : Y ⟶ X, this is the obvious functor from T/Y to (T/X)/f  -/
CategoryTheory.Over.iteratedSliceBackward : {T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] →
    {X : T} → (f : CategoryTheory.Over X) → CategoryTheory.Functor (CategoryTheory.Over f.left) (CategoryTheory.Over f)
-- Mathlib.Topology.Semicontinuity.Hemicontinuity
/-- Pointwise unions of upper hemicontinuous maps are upper hemicontinuous.  -/
UpperHemicontinuousWithinAt.union : ∀ {α : Type u_3} {β : Type u_4} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f g : α → Set β} {s : Set α}
  {x : α},
  UpperHemicontinuousWithinAt f s x →
    UpperHemicontinuousWithinAt g s x → UpperHemicontinuousWithinAt (fun x => f x ∪ g x) s x
-- Mathlib.Data.ENNReal.Inv
ENNReal.eq_top_of_forall_nnreal_le : ∀ {x : ENNReal}, (∀ (r : NNReal), ↑r ≤ x) → x = ⊤
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKeyD_minKey : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {he : t.isEmpty = false} {fallback : α}, t.getKeyD (t.minKey he) fallback = t.minKey he
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
AlgebraicGeometry.instCompactSpaceCarrierCarrierCommRingCatPullbackSchemeOfQuasiCompact : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [AlgebraicGeometry.QuasiCompact f] [CompactSpace ↥Y],
  CompactSpace ↥(CategoryTheory.Limits.pullback f g)
-- Mathlib.Order.Disjoint
Codisjoint.sup_right : ∀ {α : Type u_1} [inst : SemilatticeSup α] [inst_1 : OrderTop α] {a b : α} (c : α),
  Codisjoint a b → Codisjoint a (b ⊔ c)
-- Mathlib.GroupTheory.Perm.Cycle.Concrete
Cycle.formPerm_eq_self_of_notMem : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Cycle α) (h : s.Nodup), ∀ x ∉ s, (s.formPerm h) x = x
-- Mathlib.Analysis.InnerProductSpace.Defs
InnerProductSpace.Core.norm_eq_sqrt_re_inner : ∀ {𝕜 : Type u_1} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F]
  [c : PreInnerProductSpace.Core 𝕜 F] (x : F), ‖x‖ = √(RCLike.re (inner 𝕜 x x))
-- Mathlib.CategoryTheory.Sites.Over
/-- Given `F : Sheaf J A` and `X : C`, this is the pullback of `F` on `J.over X`.  -/
CategoryTheory.Sheaf.over : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {A : Type u'} →
        [inst_1 : CategoryTheory.Category.{v', u'} A] →
          CategoryTheory.Sheaf J A → (X : C) → CategoryTheory.Sheaf (J.over X) A
-- Mathlib.Combinatorics.Enumerative.Schroder
_private.Mathlib.Combinatorics.Enumerative.Schroder.0.Nat.smallSchroder.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1) (h_3 : (n : ℕ) → motive n.succ),
  (match 0 with
    | 0 => h_1 ()
    | 1 => h_2 ()
    | n.succ => h_3 n) =
    h_1 ()
-- Mathlib.RingTheory.Coprime.Basic
IsCoprime.neg_neg : ∀ {R : Type u} [inst : CommRing R] {x y : R}, IsCoprime x y → IsCoprime (-x) (-y)
-- Init.Data.Order.Factories
/-- If an `LE α` is reflexive, antisymmetric and transitive, then it represents a partial order.
 -/
Std.IsPartialOrder.of_le : ∀ {α : Type u} [inst : LE α],
  autoParam (Std.Refl fun x1 x2 => x1 ≤ x2) Std.IsPartialOrder.of_le._auto_1 →
    autoParam (Std.Antisymm fun x1 x2 => x1 ≤ x2) Std.IsPartialOrder.of_le._auto_3 →
      ∀
        (le_trans :
          autoParam (Trans (fun x1 x2 => x1 ≤ x2) (fun x1 x2 => x1 ≤ x2) fun x1 x2 => x1 ≤ x2)
            Std.IsPartialOrder.of_le._auto_5),
        Std.IsPartialOrder α