mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Category.Grp.Limits
CommGrpCat.commGroupObj.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommGrpCat) (j : J),
  CommGrpCat.commGroupObj F j =
    { toMul := CommGrpCat.commGroupObj._aux_1 F j, mul_assoc := ⋯, toOne := CommGrpCat.commGroupObj._aux_4 F j,
      one_mul := ⋯, mul_one := ⋯, toNPow := CommGrpCat.commGroupObj._aux_8 F j, npow_zero := ⋯, npow_succ := ⋯,
      toInv := CommGrpCat.commGroupObj._aux_12 F j, toDiv := CommGrpCat.commGroupObj._aux_14 F j,
      toZPow := CommGrpCat.commGroupObj._aux_16 F j, div_eq_mul_inv := ⋯, zpow_zero' := ⋯, zpow_succ' := ⋯,
      zpow_neg' := ⋯, inv_mul_cancel := ⋯, mul_comm := ⋯ }
-- Lean.Util.MonadCache
Lean.MonadCacheT.instMonad : {ω α β : Type} →
  {m : Type → Type} →
    [inst : STWorld ω m] → [inst_1 : BEq α] → [inst_2 : Hashable α] → [Monad m] → Monad (Lean.MonadCacheT α β m)
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Functor.FullyFaithful.grpObj_mul : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  {F : CategoryTheory.Functor C D} [inst_4 : F.Monoidal] (hF : F.FullyFaithful) (X : C)
  [inst_5 : CategoryTheory.GrpObj (F.obj X)],
  CategoryTheory.MonObj.mul =
    hF.preimage
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.δ F X X) CategoryTheory.MonObj.mul)
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.IsBase.closure_of_superset : ∀ {α : Type u_2} {M : Matroid α} {X B : Set α}, M.IsBase B → B ⊆ X → M.closure X = M.E
-- Mathlib.Topology.Order.Category.AlexDisc
AlexDisc.mk : (toTopCat : TopCat) → [is_alexandrovDiscrete : AlexandrovDiscrete ↑toTopCat] → AlexDisc
-- Mathlib.LinearAlgebra.Quotient.Pi
Submodule.quotientPi_aux.toFun.eq_1 : ∀ {ι : Type u_1} {R : Type u_2} [inst : CommRing R] {Ms : ι → Type u_3} [inst_1 : (i : ι) → AddCommGroup (Ms i)]
  [inst_2 : (i : ι) → Module R (Ms i)] (p : (i : ι) → Submodule R (Ms i)),
  Submodule.quotientPi_aux.toFun p = ⇑(Submodule.quotientPiLift p (fun i => (p i).mkQ) ⋯)
-- Mathlib.Analysis.Calculus.FDeriv.Add
DifferentiableOn.sub_iff_left : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F}
  {s : Set E}, DifferentiableOn 𝕜 g s → (DifferentiableOn 𝕜 (f - g) s ↔ DifferentiableOn 𝕜 f s)
-- Lean.Meta.Tactic.Grind.CastLike
/-- Returns `true` if `declName` is the name of a cast-like function used to implement `grind` solvers  -/
Lean.Meta.Grind.isCastLikeDeclName : Lean.Name → Bool
-- Lean.Meta.Tactic.TryThis
/-- Add a suggestion for `have h : t := e`.  -/
Lean.Meta.Tactic.TryThis.addHaveSuggestion : Lean.Syntax →
  Option Lean.Name →
    Option Lean.Expr →
      Lean.Expr →
        optParam (Option Lean.Syntax) none →
          optParam (Option Lean.Elab.Tactic.SavedState) none → Lean.Elab.Tactic.TacticM Unit
-- Std.Time.Zoned.TimeZone
/-- The abbreviation of the time zone.
 -/
Std.Time.TimeZone.abbreviation : Std.Time.TimeZone → String
-- Init.Data.Int.Order
Int.self_le_toNat : ∀ (a : ℤ), a ≤ ↑a.toNat
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Fin
Fin.reduceSubNat : Lean.Meta.Simp.DSimproc
-- Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
/-- A minimal Weierstrass equation has good reduction if and only if
the valuation of its discriminant is 1.  -/
WeierstrassCurve.HasGoodReduction : (R : Type u_1) →
  [inst : CommRing R] →
    [inst_1 : IsDomain R] →
      [IsDiscreteValuationRing R] →
        {K : Type u_2} → [inst_3 : Field K] → [inst_4 : Algebra R K] → [IsFractionRing R K] → WeierstrassCurve K → Prop
-- Aesop.Index.Basic
Aesop.IndexMatchLocation.none.sizeOf_spec : sizeOf Aesop.IndexMatchLocation.none = 1
-- Mathlib.Data.Finset.Sups
Finset.coe_infs : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeInf α] (s t : Finset α), ↑(s ⊼ t) = ↑s ⊼ ↑t
-- Mathlib.CategoryTheory.Functor.Currying
CategoryTheory.Functor.currying_functor_obj_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]
  (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) {X Y : C × D} (f : X ⟶ Y),
  (CategoryTheory.Functor.currying.functor.obj F).map f =
    CategoryTheory.CategoryStruct.comp ((F.map f.1).app X.2) ((F.obj Y.1).map f.2)
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Equiv.instDistribMulActionAut : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommGroup N] → [inst_4 : Module R N] → (P : RootPairing ι R M N) → DistribMulAction P.Aut M
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
SimpleGraph.left_nonuniformWitnesses_subset : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : IsStrictOrderedRing 𝕜]
  (G : SimpleGraph α) [inst_3 : DecidableRel G.Adj] {ε : 𝕜} {s t : Finset α},
  ¬G.IsUniform ε s t → (G.nonuniformWitnesses ε s t).1 ⊆ s
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.max?.match_1.splitter : {α : Type u_1} →
  (motive : RBTree.RBNode α → Sort u_2) →
    (x : RBTree.RBNode α) →
      (Unit → motive RBTree.RBNode.nil) →
        ((c : RBTree.RBColor) → (l : RBTree.RBNode α) → (v : α) → motive (RBTree.RBNode.node c l v RBTree.RBNode.nil)) →
          ((c : RBTree.RBColor) →
              (l : RBTree.RBNode α) →
                (v : α) →
                  (r : RBTree.RBNode α) → (r = RBTree.RBNode.nil → False) → motive (RBTree.RBNode.node c l v r)) →
            motive x
-- Mathlib.Topology.Algebra.UniformConvergence
instMonoidUniformFun.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : Monoid β],
  instMonoidUniformFun =
    { toMul := instMulUniformFun, mul_assoc := ⋯, toOne := instOneUniformFun, one_mul := ⋯, mul_one := ⋯,
      toNPow := NPow.ofPow, npow_zero := ⋯, npow_succ := ⋯ }
-- Init.Data.Array.Basic
/-- Swaps a new element with the element at the given index. Panics if the index is out of bounds.

Returns the value formerly found at `i`, paired with an array in which the value at `i` has been
replaced with `v`.

Examples:
* `#["spinach", "broccoli", "carrot"].swapAt! 1 "pepper" = (#["spinach", "pepper", "carrot"], "broccoli")`
* `#["spinach", "broccoli", "carrot"].swapAt! 2 "pepper" = (#["spinach", "broccoli", "pepper"], "carrot")`
 -/
Array.swapAt! : {α : Type u} → Array α → ℕ → α → α × Array α
-- Mathlib.Analysis.Asymptotics.LinearGrowth
Monotone.linearGrowthInf_comp_mul : ∀ {u : ℕ → EReal} {m : ℕ},
  Monotone u → m ≠ 0 → (LinearGrowth.linearGrowthInf fun n => u (m * n)) = ↑m * LinearGrowth.linearGrowthInf u
-- Mathlib.CategoryTheory.Shift.SingleFunctors
/-- The isomorphism `F.postcomp G ≅ F.postcomp G'` induced by an isomorphism `e : G ≅ G'`
which commutes with the shift.  -/
CategoryTheory.SingleFunctors.postcompIsoOfIso : {C : Type u_1} →
  {D : Type u_2} →
    {E : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} E] →
            {A : Type u_5} →
              [inst_3 : AddMonoid A] →
                [inst_4 : CategoryTheory.HasShift D A] →
                  [inst_5 : CategoryTheory.HasShift E A] →
                    (F : CategoryTheory.SingleFunctors C D A) →
                      {G G' : CategoryTheory.Functor D E} →
                        (e : G ≅ G') →
                          [inst_6 : G.CommShift A] →
                            [inst_7 : G'.CommShift A] →
                              [CategoryTheory.NatTrans.CommShift e.hom A] → F.postcomp G ≅ F.postcomp G'
-- Mathlib.Analysis.InnerProductSpace.Basic
/-- The inner product of a nonzero vector with a nonzero multiple of
itself, divided by the product of their norms, has absolute value 1.  -/
abs_real_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_ne_zero_mul : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] {x : F} {r : ℝ},
  x ≠ 0 → r ≠ 0 → |inner ℝ x (r • x)| / (‖x‖ * ‖r • x‖) = 1
-- Batteries.Data.UnionFind.Basic
/-- Size of union-find structure.  -/
Batteries.UnionFind.size : Batteries.UnionFind → ℕ
-- Mathlib.RingTheory.SimpleModule.Isotypic
instFiniteElemSubmoduleIsotypicComponentsOfIsNoetherian : ∀ (R : Type u_2) (M : Type u) [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsNoetherian R M],
  Finite ↑(isotypicComponents R M)
-- Mathlib.CategoryTheory.Shift.Induced
CategoryTheory.HasShift.Induced.zero_inv_app_obj : ∀ {C : Type u_2} {D : Type u_1} [inst : CategoryTheory.Category.{v_1, u_2} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_1} D] (F : CategoryTheory.Functor C D) {A : Type u_3} [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift C A] (s : A → CategoryTheory.Functor D D)
  (i : (a : A) → F.comp (s a) ≅ (CategoryTheory.shiftFunctor C a).comp F)
  [inst_4 : ((CategoryTheory.Functor.whiskeringLeft C D D).obj F).Full]
  [inst_5 : ((CategoryTheory.Functor.whiskeringLeft C D D).obj F).Faithful] (X : C),
  (CategoryTheory.HasShift.Induced.zero F s i).inv.app (F.obj X) =
    CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.shiftFunctorZero C A).inv.app X)) ((i 0).inv.app X)
-- Mathlib.RingTheory.Polynomial.GaussNorm
/-- If `v` is a nonarchimedean absolute value, then the Gauss norm is an absolute value.  -/
Polynomial.gaussNorm_isAbsoluteValue : ∀ {c : ℝ} {R : Type u_3} [inst : Ring R] {v : AbsoluteValue R ℝ},
  IsNonarchimedean ⇑v → 0 < c → IsAbsoluteValue (Polynomial.gaussNorm v c)
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem!_erase : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  [inst : Inhabited β] {k a : α}, (m.erase k)[a]! = if (k == a) = true then default else m[a]!
-- Mathlib.Analysis.BoxIntegral.Box.Basic
BoxIntegral.Box.upper_mem : ∀ {ι : Type u_1} (I : BoxIntegral.Box ι), I.upper ∈ I
-- Std.Data.DHashMap.Raw
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Raw.WF.empty₀ : ∀ {α : Type u_1} {β : α → Type u_2} [inst : BEq α] [inst_1 : Hashable α] {c : ℕ},
  (↑(Std.DHashMap.Internal.Raw₀.emptyWithCapacity c)).WF
-- Init.Grind.Module.Envelope
Lean.Grind.IntModule.OfNatModule.sub : {α : Type u} →
  [inst : Lean.Grind.NatModule α] →
    Lean.Grind.IntModule.OfNatModule.Q α → Lean.Grind.IntModule.OfNatModule.Q α → Lean.Grind.IntModule.OfNatModule.Q α
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
/-- The underlying object in the base category.  -/
CategoryTheory.Pseudofunctor.Grothendieck.base : {𝒮 : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
    {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮) CategoryTheory.Cat} → F.Grothendieck → 𝒮
-- Mathlib.Algebra.Order.Floor.Ring
Int.fract_sub_intCast : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] [IsOrderedRing R] (a : R) (m : ℤ),
  Int.fract (a - ↑m) = Int.fract a
-- Mathlib.Analysis.Calculus.FDeriv.Add
HasFDerivWithinAt.sum : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {x : E}
  {s : Set E} {ι : Type u_4} {u : Finset ι} {A : ι → E → F} {A' : ι → E →L[𝕜] F},
  (∀ i ∈ u, HasFDerivWithinAt (A i) (A' i) s x) → HasFDerivWithinAt (∑ i ∈ u, A i) (∑ i ∈ u, A' i) s x
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRootMonic.coeff_apply_le : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
  (h : IsAdjoinRootMonic S f) (z : S) (i : ℕ), f.natDegree ≤ i → h.coeff z i = 0
-- Mathlib.CategoryTheory.Category.Bipointed
/-- The underlying function of a morphism of bipointed types.  -/
Bipointed.Hom.toFun : {X Y : Bipointed} → X.Hom Y → X.X → Y.X
-- Mathlib.CategoryTheory.MorphismProperty.Comma
/-- See Note [custom simps projection]  -/
CategoryTheory.MorphismProperty.Comma.Hom.Simps.hom : {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} →
                      {X Y : CategoryTheory.MorphismProperty.Comma L R P Q W} → X.Hom Y → (X.toComma ⟶ Y.toComma)
-- Mathlib.RingTheory.PicardGroup
CommRing.Pic.subsingleton_iff : ∀ {R : Type u} [inst : CommRing R],
  Subsingleton (CommRing.Pic R) ↔
    ∀ (M : Type u) [inst_1 : AddCommGroup M] [inst_2 : Module R M], Module.Invertible R M → Module.Free R M
-- Init.Data.Nat.Basic
Nat.lt_of_sub_eq_sub_one : ∀ {m n l : ℕ}, m - n = l + 1 → n < m
-- Lean.Parser.Term
Lean.Parser.Term.doubleQuotedName.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.RingTheory.GradedAlgebra.RingHom
GradedRingHom.instGradedFunLike : ∀ {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_6} {τ : Type u_7} [inst : Semiring A] [inst_1 : Semiring B]
  [inst_2 : SetLike σ A] [inst_3 : SetLike τ B] {𝒜 : ι → σ} {ℬ : ι → τ}, GradedFunLike (𝒜 →+*ᵍ ℬ) 𝒜 ℬ
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddMonoidHom.coe_coe : ∀ {A : Type u_2} {B : Type u_3} [inst : AddMonoid A] [inst_1 : AddMonoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B] {F : Type u_7} [inst_4 : FunLike F A B] [inst_5 : AddMonoidHomClass F A B]
  [inst_6 : ContinuousMapClass F A B] (f : F), ⇑↑f = ⇑f
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.mem_alter_of_compare_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k k' : α}
  {f : Option β → Option β}, cmp k k' = Ordering.eq → (k' ∈ t.alter k f ↔ (f t[k]?).isSome = true)
-- Mathlib.RingTheory.Ideal.NatInt
Nat.maximalIdeal_eq_span_two_three : IsLocalRing.maximalIdeal ℕ = Ideal.span {2, 3}
-- Mathlib.Analysis.BoxIntegral.Basic
BoxIntegral.integralSum_congr : ∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {I : BoxIntegral.Box ι}
  {π : BoxIntegral.TaggedPrepartition I} {f₁ f₂ : (ι → ℝ) → E} {vol₁ vol₂ : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤},
  Set.EqOn f₁ f₂ (BoxIntegral.Box.Icc I) →
    Set.EqOn ⇑vol₁ ⇑vol₂ ↑π.boxes → BoxIntegral.integralSum f₁ vol₁ π = BoxIntegral.integralSum f₂ vol₂ π
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.CommRing.toRing : Lean.Meta.Grind.Arith.CommRing.CommRing → Lean.Meta.Grind.Arith.CommRing.Ring
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.isoHomologyπ_inv_hom_id_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i j : ι) (hi : c.prev j = i) (h : K.d i j = 0)
  [inst_2 : K.HasHomology j] {Z : C} (h_1 : K.homology j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.isoHomologyπ i j hi h).inv
      (CategoryTheory.CategoryStruct.comp (K.homologyπ j) h_1) =
    h_1
-- Mathlib.Algebra.Ring.Ext
AddGroupWithOne.ext_iff : ∀ {R : Type u} {inst₁ inst₂ : AddGroupWithOne R}, inst₁ = inst₂ ↔ HAdd.hAdd = HAdd.hAdd ∧ One.one = One.one
-- Mathlib.Analysis.Analytic.ConvergenceRadius
FormalMultilinearSeries.not_summable_norm_of_radius_lt_nnnorm : ∀ {𝕜 : Type u_1} {E : Type u_3} {F : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  (p : FormalMultilinearSeries 𝕜 E F) {x : E}, p.radius < ↑‖x‖₊ → ¬Summable fun n => ‖p n‖ * ‖x‖ ^ n
-- Init.Data.Int.DivMod.Lemmas
Int.fdiv_left_inj : ∀ {a b d : ℤ}, d ∣ a → d ∣ b → (a.fdiv d = b.fdiv d ↔ a = b)
-- Mathlib.Algebra.Order.Group.Cone
/-- The cone of elements that are at least 1.  -/
GroupCone.oneLE : (H : Type u_1) → [inst : CommGroup H] → [inst_1 : PartialOrder H] → [IsOrderedMonoid H] → GroupCone H
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
/-- Post-composition by a uniformly continuous function is uniformly continuous for the
uniform structures of `𝔖`-convergence.

More precisely, if `f : γ → β` is uniformly continuous, then
`(fun g ↦ f ∘ g) : (α →ᵤ[𝔖] γ) → (α →ᵤ[𝔖] β)` is uniformly continuous.  -/
UniformOnFun.postcomp_uniformContinuous : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : UniformSpace β] {𝔖 : Set (Set α)} [inst_1 : UniformSpace γ]
  {f : γ → β},
  UniformContinuous f → UniformContinuous (⇑(UniformOnFun.ofFun 𝔖) ∘ (fun x => f ∘ x) ∘ ⇑(UniformOnFun.toFun 𝔖))
-- Init.System.Promise
_private.Init.System.Promise.0.IO.Promise.mk.inj : ∀ {α : Type} {prom : IO.PromisePointed✝.type} {h : Nonempty α} {prom_1 : IO.PromisePointed✝.type} {h_1 : Nonempty α},
  { prom := prom, h := h } = { prom := prom_1, h := h_1 } → prom = prom_1
-- Init.Notation
/-- The implementation of the `<*>` operator.

In a monad, `mf <*> mx` is the same as `do let f ← mf; x ← mx; pure (f x)`: it evaluates the
function first, then the argument, and applies one to the other.

To avoid surprising evaluation semantics, `mx` is taken "lazily", using a `Unit → f α` function.


Conventions for notations in identifiers:

 * The recommended spelling of `<*>` in identifiers is `seq`. -/
«term_<*>_» : Lean.TrailingParserDescr
-- Mathlib.Topology.Inseparable
IsOpen.not_specializes : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X} {s : Set X}, IsOpen s → x ∉ s → y ∈ s → ¬x ⤳ y
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.modify_eq_empty_iff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {f : β → β}, Std.ExtDHashMap.Const.modify m k f = ∅ ↔ m = ∅
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.instEquivLike : {R : Type uR} →
  {A₁ : Type uA₁} →
    {A₂ : Type uA₂} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A₁] →
          [inst_2 : Semiring A₂] → [inst_3 : Algebra R A₁] → [inst_4 : Algebra R A₂] → EquivLike (A₁ ≃ₐ[R] A₂) A₁ A₂
-- Mathlib.Tactic.DepRewrite
/-- Elaborate `DepRewrite.Config`.  -/
Mathlib.Tactic.DepRewrite.elabDepRewriteConfig : Lean.Syntax →
  optParam Mathlib.Tactic.DepRewrite.Config { } →
    optParam Bool true → Lean.Elab.Tactic.TacticM Mathlib.Tactic.DepRewrite.Config
-- Mathlib.Tactic.Algebra.Basic
Mathlib.Tactic.Algebra.Cache.mk.sizeOf_spec : ∀ {u : Lean.Level} {A : Q(Type u)} {sA : Q(CommSemiring «$A»)} (toCache : Mathlib.Tactic.Ring.Common.Cache sA)
  (field : Option Q(Field «$A»)), sizeOf { toCache := toCache, field := field } = 1 + sizeOf toCache + sizeOf field
-- Mathlib.Algebra.Order.Ring.StandardPart
ArchimedeanClass.FiniteElement.mk_ratCast : ∀ {K : Type u_1} [inst : LinearOrder K] [inst_1 : Field K] [inst_2 : IsOrderedRing K] (q : ℚ),
  ArchimedeanClass.FiniteElement.mk ↑q ⋯ = ↑q
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
tsum_of_nat_of_neg_add_one : ∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M] [ContinuousAdd M] [T2Space M] {f : ℤ → M},
  (Summable fun n => f ↑n) →
    (Summable fun n => f (-(↑n + 1))) → ∑' (n : ℤ), f n = ∑' (n : ℕ), f ↑n + ∑' (n : ℕ), f (-(↑n + 1))
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoMod_add_toIocMod_zero : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α), toIcoMod hp 0 (a - b) + toIocMod hp 0 (b - a) = p
-- Mathlib.Algebra.Algebra.Defs
Algebra.linearMap_apply : ∀ (R : Type u) (A : Type w) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (r : R),
  (Algebra.linearMap R A) r = (algebraMap R A) r
-- Mathlib.Geometry.Euclidean.Sphere.Power
/-- The power of a point is positive if and only if the point lies outside the sphere.  -/
EuclideanGeometry.Sphere.power_pos_iff_radius_lt_dist_center : ∀ {P : Type u_2} [inst : MetricSpace P] {s : EuclideanGeometry.Sphere P} {p : P},
  0 ≤ s.radius → (0 < s.power p ↔ s.radius < dist p s.center)
-- Lean.Parser.Command
Lean.Parser.Command.theorem.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Init.Data.BitVec.Lemmas
BitVec.toInt_of_zero_length : ∀ {w : ℕ}, w = 0 → ∀ (x : BitVec w), x.toInt = 0
-- Mathlib.CategoryTheory.Bicategory.LocallyGroupoid
CategoryTheory.Bicategory.Pith.comp₂_iso_inv_assoc : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] {a b : CategoryTheory.Bicategory.Pith B} {x y z : a ⟶ b}
  {f : x ⟶ y} {g : y ⟶ z} {Z : a.as ⟶ b.as} (h : x.of ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g).iso.inv h =
    CategoryTheory.CategoryStruct.comp g.iso.inv (CategoryTheory.CategoryStruct.comp f.iso.inv h)
-- Mathlib.Geometry.Manifold.VectorBundle.Basic
VectorBundleCore.IsContMDiff.contMDiffOn_coordChange : ∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {inst : NontriviallyNormedField 𝕜} {EB : Type u_7}
  {inst_1 : NormedAddCommGroup EB} {inst_2 : NormedSpace 𝕜 EB} {HB : Type u_8} {inst_3 : TopologicalSpace HB}
  {inst_4 : TopologicalSpace B} {inst_5 : ChartedSpace HB B} {inst_6 : NormedAddCommGroup F} {inst_7 : NormedSpace 𝕜 F}
  {ι : Type u_11} {Z : VectorBundleCore 𝕜 B F ι} {IB : ModelWithCorners 𝕜 EB HB} {n : WithTop ℕ∞}
  [self : Z.IsContMDiff IB n] (i j : ι),
  ContMDiffOn IB (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) n (Z.coordChange i j) (Z.baseSet i ∩ Z.baseSet j)
-- Mathlib.GroupTheory.Subgroup.Center
Subgroup.center.isMulCommutative : ∀ (G : Type u_1) [inst : Group G], IsMulCommutative ↥(Subgroup.center G)
-- Mathlib.Data.Multiset.Lattice
Multiset.sup_mono : ∀ {α : Type u_1} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s₁ s₂ : Multiset α}, s₁ ⊆ s₂ → s₁.sup ≤ s₂.sup
-- Mathlib.Analysis.Normed.Module.Ball.Pointwise
disjoint_ball_ball_iff : ∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] [NormedSpace ℝ E] {x y : E} {δ ε : ℝ},
  0 < δ → 0 < ε → (Disjoint (Metric.ball x δ) (Metric.ball y ε) ↔ δ + ε ≤ dist x y)
-- Mathlib.CategoryTheory.Bicategory.Functor.Oplax
/-- Oplax associativity.  -/
CategoryTheory.OplaxFunctor.map₂_associator_app_assoc : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] (self : CategoryTheory.OplaxFunctor B CategoryTheory.Cat)
  {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (X : ↑(self.obj a)) {Z : ↑(self.obj d)}
  (h_1 : (self.map h).toFunctor.obj ((self.map g).toFunctor.obj ((self.map f).toFunctor.obj X)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((self.map₂ (CategoryTheory.Bicategory.associator f g h).hom).toNatTrans.app X)
      (CategoryTheory.CategoryStruct.comp ((self.mapComp f (CategoryTheory.CategoryStruct.comp g h)).toNatTrans.app X)
        (CategoryTheory.CategoryStruct.comp ((self.mapComp g h).toNatTrans.app ((self.map f).toFunctor.obj X)) h_1)) =
    CategoryTheory.CategoryStruct.comp ((self.mapComp (CategoryTheory.CategoryStruct.comp f g) h).toNatTrans.app X)
      (CategoryTheory.CategoryStruct.comp ((self.map h).toFunctor.map ((self.mapComp f g).toNatTrans.app X)) h_1)
-- Mathlib.Analysis.Calculus.FDeriv.Const
fderiv_intCast : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] [inst_7 : IntCast F] (z : ℤ), fderiv 𝕜 ↑z = 0
-- Mathlib.Data.List.Perm.Basic
List.perm_eraseIdx_of_getElem?_eq : ∀ {α : Type u_1} {l₁ l₂ : List α} {m n : ℕ}, l₁[m]? = l₂[n]? → ((l₁.eraseIdx m).Perm (l₂.eraseIdx n) ↔ l₁.Perm l₂)
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
SimplexCategoryGenRel.degeneracies.σ : ∀ {n : ℕ} (i : Fin (n + 1)), SimplexCategoryGenRel.degeneracies (SimplexCategoryGenRel.σ i)