mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.mapRightComp_inv_app_left : ∀ {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) {P : CategoryTheory.MorphismProperty T} {Q : CategoryTheory.MorphismProperty A}
  {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative] [inst_4 : W.IsMultiplicative]
  {R₁ R₂ R₃ : CategoryTheory.Functor B T} [inst_5 : Q.RespectsIso] [inst_6 : W.RespectsIso] (r : R₁ ⟶ R₂) (r' : R₂ ⟶ R₃)
  (hr :
    ∀ (X : CategoryTheory.MorphismProperty.Comma L R₁ P Q W),
      P (CategoryTheory.CategoryStruct.comp X.hom (r.app X.right)))
  (hr' :
    ∀ (X : CategoryTheory.MorphismProperty.Comma L R₂ P Q W),
      P (CategoryTheory.CategoryStruct.comp X.hom (r'.app X.right)))
  (hrr' :
    ∀ (X : CategoryTheory.MorphismProperty.Comma L R₁ P Q W),
      P (CategoryTheory.CategoryStruct.comp X.hom ((CategoryTheory.CategoryStruct.comp r r').app X.right)))
  (X : CategoryTheory.MorphismProperty.Comma L R₁ P Q W),
  ((CategoryTheory.MorphismProperty.Comma.mapRightComp L r r' hr hr' hrr').inv.app X).left =
    CategoryTheory.CategoryStruct.id X.left
-- Mathlib.Algebra.DirectSum.Internal
/-- A direct sum of powers of a submodule of an algebra has a multiplicative structure.  -/
Submodule.nat_power_gradedMonoid : ∀ {S : Type u_3} {R : Type u_4} [inst : CommSemiring S] [inst_1 : Semiring R] [inst_2 : Algebra S R]
  (p : Submodule S R), SetLike.GradedMonoid fun i => p ^ i
-- Mathlib.NumberTheory.LSeries.Basic
LSeries.norm_term_eq : ∀ (f : ℕ → ℂ) (s : ℂ) (n : ℕ), ‖LSeries.term f s n‖ = if n = 0 then 0 else ‖f n‖ / ↑n ^ s.re
-- Mathlib.Analysis.Normed.Ring.WithAbs
WithAbs.instIsScalarTower_1 : ∀ {S : Type u_2} [inst : Semiring S] [inst_1 : PartialOrder S] {R : Type u_3} {T : Type u_4} [inst_2 : Semiring R]
  (v : AbsoluteValue R S) {P : Type u_5} [inst_3 : SMul P R] [inst_4 : SMul T R] [inst_5 : SMul P T]
  [IsScalarTower P T R], IsScalarTower P T (WithAbs v)
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- Construct a multicofork using a collection `π` of morphisms.  -/
CategoryTheory.Limits.Multicofork.ofπ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.Limits.MultispanShape} →
      (I : CategoryTheory.Limits.MultispanIndex J C) →
        (P : C) →
          (π : (b : J.R) → I.right b ⟶ P) →
            (∀ (a : J.L),
                CategoryTheory.CategoryStruct.comp (I.fst a) (π (J.fst a)) =
                  CategoryTheory.CategoryStruct.comp (I.snd a) (π (J.snd a))) →
              CategoryTheory.Limits.Multicofork I
-- Mathlib.Algebra.GroupWithZero.Hom
/-- `α →*₀ β` denotes the type of zero-preserving monoid homomorphisms from `α` to `β`.  -/
«term_→*₀_» : Lean.TrailingParserDescr
-- Mathlib.Algebra.Module.LinearMap.FiniteRange
LinearMap.HasFiniteRange.of_finite_dom : ∀ {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} [inst : Semiring K] [inst_1 : AddCommMonoid V] [inst_2 : Module K V]
  [inst_3 : AddCommMonoid V₂] [inst_4 : Module K V₂] [Module.Finite K V] {f : V →ₗ[K] V₂}, f.HasFiniteRange
-- Mathlib.CategoryTheory.Category.ReflQuiv
CategoryTheory.Cat.freeReflMap_obj : ∀ {V : Type u_1} [inst : CategoryTheory.ReflQuiver V] {W : Type u_2} [inst_1 : CategoryTheory.ReflQuiver W]
  (F : V ⥤rq W) (v : V),
  (CategoryTheory.Cat.freeReflMap F).obj (CategoryTheory.Cat.FreeRefl.mk v) = CategoryTheory.Cat.FreeRefl.mk (F.obj v)
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.instMul : {X : Type u_1} →
  {R : Type u_2} →
    [inst : Zero X] →
      [inst_1 : TopologicalSpace X] →
        [inst_2 : TopologicalSpace R] → [inst_3 : MulZeroClass R] → [ContinuousMul R] → Mul (ContinuousMapZero X R)
-- Mathlib.Analysis.Calculus.FDeriv.Comp
DifferentiableOn.fun_comp : ∀ {𝕜 : 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] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E → F} {s : Set E} {g : F → G} {t : Set F},
  DifferentiableOn 𝕜 g t → DifferentiableOn 𝕜 f s → Set.MapsTo f s t → DifferentiableOn 𝕜 (fun x => g (f x)) s
-- Mathlib.Geometry.Euclidean.Angle.Sphere
/-- The circumcenter of a triangle may be expressed explicitly as a multiple (by half the inverse
of the tangent of the angle at one of the vertices) of a `π / 2` rotation of the vector between
the other two vertices, plus the midpoint of those vertices.  -/
Affine.Triangle.inv_tan_div_two_smul_rotation_pi_div_two_vadd_midpoint_eq_circumcenter : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  (t : Affine.Triangle ℝ P) {i₁ i₂ i₃ : Fin 3},
  i₁ ≠ i₂ →
    i₁ ≠ i₃ →
      i₂ ≠ i₃ →
        ((EuclideanGeometry.oangle (t.points i₁) (t.points i₂) (t.points i₃)).tan⁻¹ / 2) •
              (EuclideanGeometry.o.rotation ↑(Real.pi / 2)) (t.points i₃ -ᵥ t.points i₁) +ᵥ
            midpoint ℝ (t.points i₁) (t.points i₃) =
          Affine.Simplex.circumcenter t
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.size_diff_add_size_inter_eq_size_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  (t₁ \ t₂).size + (t₁ ∩ t₂).size = t₁.size
-- Mathlib.Algebra.Polynomial.BigOperators
Polynomial.degree_list_sum_le_of_forall_degree_le : ∀ {S : Type u_1} [inst : Semiring S] (l : List (Polynomial S)) (n : WithBot ℕ),
  (∀ p ∈ l, p.degree ≤ n) → l.sum.degree ≤ n
-- Init.Data.BitVec.Bitblast
/-- If the division equation `d.toNat * q.toNat + r.toNat = n.toNat` holds,
then `n.umod d = r`.  -/
BitVec.umod_eq_of_mul_add_toNat : ∀ {w : ℕ} {d n q r : BitVec w}, r < d → d.toNat * q.toNat + r.toNat = n.toNat → n % d = r
-- Init.Data.Option.Lemmas
Option.join_min : ∀ {α : Type u_1} [inst : Min α] {o o' : Option (Option α)}, (o ⊓ o').join = o.join ⊓ o'.join
-- Mathlib.CategoryTheory.MorphismProperty.Representable
/-- When `C` has pullbacks, then `F.map f` is representable with respect to `F` for any
`f : a ⟶ b` in `C`.  -/
CategoryTheory.Functor.relativelyRepresentable.map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [F.Full] [CategoryTheory.Limits.HasPullbacks C] {a b : C} (f : a ⟶ b)
  [∀ (c : C) (g : c ⟶ b), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) F],
  F.relativelyRepresentable (F.map f)
-- Mathlib.Algebra.Homology.Augment
ChainComplex.augment_d_one_zero : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  (C : ChainComplex V ℕ) {X : V} (f : C.X 0 ⟶ X) (w : CategoryTheory.CategoryStruct.comp (C.d 1 0) f = 0),
  (C.augment f w).d 1 0 = f
-- Mathlib.Analysis.SpecialFunctions.Log.Deriv
ContDiff.log : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {n : WithTop ℕ∞},
  ContDiff ℝ n f → (∀ (x : E), f x ≠ 0) → ContDiff ℝ n fun x => Real.log (f x)
-- Mathlib.Data.Finmap
Finmap.mem_erase : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a a' : α} {s : Finmap β},
  a' ∈ Finmap.erase a s ↔ a' ≠ a ∧ a' ∈ s
-- Mathlib.RingTheory.IsTensorProduct
Algebra.IsPushout.cancelBaseChangeAlg.congr_simp : ∀ (R : Type u_1) (S : Type v₃) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (A : Type u_8)
  (B : Type u_9) [inst_3 : CommRing A] [inst_4 : CommRing B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  [inst_7 : Algebra A B] [inst_8 : Algebra S B] [inst_9 : IsScalarTower R A B] [inst_10 : IsScalarTower R S B]
  [inst_11 : Algebra.IsPushout R S A B] (C : Type u_11) [inst_12 : CommRing C] [inst_13 : Algebra R C]
  [inst_14 : Algebra A C] [inst_15 : IsScalarTower R A C],
  Algebra.IsPushout.cancelBaseChangeAlg R S A B C = Algebra.IsPushout.cancelBaseChangeAlg R S A B C
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.eq : ∀ {x y : PSet.{u_1}}, ZFSet.mk x = ZFSet.mk y ↔ x.Equiv y
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalAlgebra.adjoin_univ : ∀ (R : Type u) (A : Type v) [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A], NonUnitalAlgebra.adjoin R Set.univ = ⊤
-- Batteries.Recycling.RBTree.Basic
RBTree.RBMap.instRepr : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → [Repr α] → [Repr β] → Repr (RBTree.RBMap α β cmp)
-- Mathlib.SetTheory.Ordinal.Notation
ONote.oadd_mul_nfBelow : ∀ {e₁ : ONote} {n₁ : ℕ+} {a₁ : ONote} {b₁ : Ordinal.{0}},
  (e₁.oadd n₁ a₁).NFBelow b₁ →
    ∀ {o₂ : ONote} {b₂ : Ordinal.{0}}, o₂.NFBelow b₂ → (e₁.oadd n₁ a₁ * o₂).NFBelow (e₁.repr + b₂)
-- Mathlib.RingTheory.QuasiFinite.Weakly
/-- Use `Algebra.QuasiFinite.of_surjective_algHom` instead for `Algebra.QuasiFiniteAt R p`.  -/
Algebra.WeaklyQuasiFiniteAt.of_algHom_localization : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : CommRing T] [inst_4 : Algebra R T] (p : Ideal S) [inst_5 : p.IsPrime] [Algebra.WeaklyQuasiFiniteAt R p]
  (q : Ideal T) [inst_7 : q.IsPrime] (f : Localization.AtPrime p →ₐ[R] Localization.AtPrime q),
  Function.Surjective ⇑f → Algebra.WeaklyQuasiFiniteAt R q
-- Mathlib.RingTheory.TensorProduct.Basic
Algebra.TensorProduct.right_isScalarTower : ∀ {R : Type uR} {A : Type uA} {B : Type uB} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : CommSemiring B] [inst_4 : Algebra R B], IsScalarTower R B (TensorProduct R A B)
-- Mathlib.NumberTheory.LegendreSymbol.AddCharacter
/-- The additive character on `ZMod n` associated to a primitive `n`th root of unity
is primitive  -/
AddChar.zmodChar_primitive_of_primitive_root : ∀ {C : Type v} [inst : CommMonoid C] (n : ℕ) [inst_1 : NeZero n] {ζ : C} (h : IsPrimitiveRoot ζ n),
  (AddChar.zmodChar n ⋯).IsPrimitive
-- Mathlib.Analysis.Normed.Group.Continuity
tendsto_one_iff_norm_tendsto_zero : ∀ {α : Type u_1} {E : Type u_4} [inst : SeminormedGroup E] {f : α → E} {a : Filter α},
  Filter.Tendsto f a (nhds 1) ↔ Filter.Tendsto (fun x => ‖f x‖) a (nhds 0)
-- Mathlib.Probability.Distributions.Binomial
ProbabilityTheory.map_cast_binomial_eq_sum_dirac : ∀ {R : Type u_1} [inst : MeasurableSpace R] [inst_1 : AddMonoidWithOne R] [MeasurableSingletonClass R] (n : ℕ)
  (p : ↑unitInterval),
  MeasureTheory.Measure.map Nat.cast (ProbabilityTheory.binomial n p) =
    ∑ k ≤ n, ENNReal.ofReal (↑(n.choose k) * ↑p ^ k * (1 - ↑p) ^ (n - k)) • MeasureTheory.Measure.dirac ↑k
-- Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
/-- If `X × -` preserves colimits in `D` for any `X : D`, then the product functor `F ⨯ -` for
`F : C ⥤ D` also preserves colimits.

Note this is (mathematically) a special case of the statement that
"if limits commute with colimits in `D`, then they do as well in `C ⥤ D`"
but the story in Lean is a bit more complex, and this statement isn't directly a special case.
That is, even with a formalised proof of the general statement, there would still need to be some
work to convert to this version: namely, the natural isomorphism
`(evaluation C D).obj k ⋙ prod.functor.obj (F.obj k) ≅
  prod.functor.obj F ⋙ (evaluation C D).obj k`
 -/
CategoryTheory.FunctorCategory.prod_preservesColimits : ∀ {C : Type u} [inst : CategoryTheory.Category.{v₁, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{u, u₂} D]
  [inst_2 : CategoryTheory.Limits.HasBinaryProducts D] [CategoryTheory.Limits.HasColimits D]
  [∀ (X : D), CategoryTheory.Limits.PreservesColimits (CategoryTheory.Limits.prod.functor.obj X)]
  (F : CategoryTheory.Functor C D), CategoryTheory.Limits.PreservesColimits (CategoryTheory.Limits.prod.functor.obj F)
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
/-- In a measurable space with measurable singletons, every function is integrable with respect to
a Dirac measure.
See `integrable_dirac'` for a version which requires `f` to be strongly measurable but does not
need singletons to be measurable.  -/
MeasureTheory.integrable_dirac : ∀ {α : Type u_1} {ε : Type u_5} {m : MeasurableSpace α} [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε]
  [MeasurableSingletonClass α] {a : α} {f : α → ε},
  ‖f a‖ₑ < ⊤ → MeasureTheory.Integrable f (MeasureTheory.Measure.dirac a)
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomAddAct.mk_zero : ∀ {M : Type u_1} [inst : Zero M], DomAddAct.mk 0 = 0
-- Init.Data.Int.Linear
Int.Internal.Linear.diseq_split_resolve : ∀ (ctx : Int.Internal.Linear.Context) (p₁ p₂ p₃ : Int.Internal.Linear.Poly),
  Int.Internal.Linear.diseq_split_cert p₁ p₂ p₃ = true →
    Int.Internal.Linear.Poly.denote' ctx p₁ ≠ 0 →
      ¬Int.Internal.Linear.Poly.denote' ctx p₂ ≤ 0 → Int.Internal.Linear.Poly.denote' ctx p₃ ≤ 0
-- Mathlib.Analysis.CStarAlgebra.Module.Synonym
/-- `WithCStarModule.equiv` as an additive equivalence.  -/
WithCStarModule.addEquiv : (A : Type u_3) → (E : Type u_4) → [inst : AddCommGroup E] → WithCStarModule A E ≃+ E
-- Lean.Compiler.IR.Basic
Lean.IR.JoinPointId.mk.inj : ∀ {idx idx_1 : Lean.IR.Index}, { idx := idx } = { idx := idx_1 } → idx = idx_1
-- Mathlib.RingTheory.Ideal.Cotangent
IsLocalRing.instFiniteDimensionalResidueFieldCotangentSpaceOfIsNoetherianRing : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsLocalRing R] [IsNoetherianRing R],
  FiniteDimensional (IsLocalRing.ResidueField R) (IsLocalRing.CotangentSpace R)
-- Mathlib.RingTheory.Localization.AtPrime.Basic
/-- Isomorphic rings have isomorphic localizations.  -/
Localization.localRingEquiv : {R : Type u_1} →
  [inst : CommSemiring R] →
    {P : Type u_3} →
      [inst_1 : CommSemiring P] →
        (I : Ideal R) →
          [hI : I.IsPrime] →
            (J : Ideal P) →
              [inst_2 : J.IsPrime] →
                (f : R ≃+* P) → I = Ideal.comap f J → Localization.AtPrime I ≃+* Localization.AtPrime J
-- Lean.Elab.InfoTree.InlayHints
Lean.Elab.InlayHint.mk.sizeOf_spec : ∀ (toInlayHintInfo : Lean.Elab.InlayHintInfo) (lctx : Lean.LocalContext)
  (deferredResolution : Lean.Elab.InlayHintInfo → Lean.MetaM Lean.Elab.InlayHintInfo),
  sizeOf { toInlayHintInfo := toInlayHintInfo, lctx := lctx, deferredResolution := deferredResolution } =
    1 + sizeOf toInlayHintInfo + sizeOf lctx
-- Mathlib.Analysis.Calculus.ContDiff.Defs
HasFTaylorSeriesUpToOn.analyticOn : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {p : E → FormalMultilinearSeries 𝕜 E F},
  HasFTaylorSeriesUpToOn ⊤ f p s → AnalyticOn 𝕜 (fun x => p x 0) s → AnalyticOn 𝕜 f s
-- Init.Data.Array.MapIdx
Array.zipIdx.eq_1 : ∀ {α : Type u} (xs : Array α) (start : ℕ), xs.zipIdx start = Array.mapIdx (fun i a => (a, start + i)) xs
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor
/-- This is the universal property of `PresheafOfModules.ModuleColimit` as a module.
See also `PresheafOfModules.colimitAdjunction`.  -/
PresheafOfModules.ModuleColimit.homEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] →
      [inst_2 : CategoryTheory.IsCofiltered C] →
        [inst_3 : CategoryTheory.InitiallySmall C] →
          {R : CategoryTheory.Functor Cᵒᵖ RingCat} →
            {cR : CategoryTheory.Limits.Cocone R} →
              (hcR : CategoryTheory.Limits.IsColimit cR) →
                {M : PresheafOfModules R} →
                  {cM : CategoryTheory.Limits.Cocone M.presheaf} →
                    (hcM : CategoryTheory.Limits.IsColimit cM) →
                      {N : ModuleCat ↑cR.pt} →
                        (ModuleCat.of (↑cR.pt) (PresheafOfModules.ModuleColimit hcR hcM) ⟶ N) ≃+
                          (M ⟶ (PresheafOfModules.constFunctor cR).obj N)
-- Mathlib.Topology.Category.Profinite.Extend
Profinite.Extend.cocone_ι_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (G : CategoryTheory.Functor Profiniteᵒᵖ C)
  (S : Profinite) (i : CategoryTheory.CostructuredArrow FintypeCat.toProfinite.op (Opposite.op S)),
  (Profinite.Extend.cocone G S).ι.app i = G.map i.hom
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_lt_rpow_of_exponent_gt : ∀ {x y z : ℝ}, 0 < x → x < 1 → z < y → x ^ y < x ^ z
-- Init.Grind.AC
Lean.Grind.AC.eq_simp_rhs_middle : ∀ {α : Sort u_1} (ctx : Lean.Grind.AC.Context α) {x : Std.Associative ctx.op}
  (lhs₁ rhs₁ head tail lhs₂ rhs₂ rhs₂' : Lean.Grind.AC.Seq),
  Lean.Grind.AC.simp_middle_cert lhs₁ rhs₁ head tail rhs₂ rhs₂' = true →
    Lean.Grind.AC.Seq.denote ctx lhs₁ = Lean.Grind.AC.Seq.denote ctx rhs₁ →
      Lean.Grind.AC.Seq.denote ctx lhs₂ = Lean.Grind.AC.Seq.denote ctx rhs₂ →
        Lean.Grind.AC.Seq.denote ctx lhs₂ = Lean.Grind.AC.Seq.denote ctx rhs₂'
-- Aesop.Tree.Data
Aesop.instDecidableEqGoalId.decEq : (x x_1 : Aesop.GoalId) → Decidable (x = x_1)
-- Mathlib.Analysis.Convex.Function
/-- **Alias** of the reverse direction of `neg_strictConcaveOn_iff`.

---

A function `-f` is strictly concave iff `f` is strictly convex.  -/
StrictConvexOn.neg : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommGroup β] [inst_4 : PartialOrder β] [IsOrderedAddMonoid β] [inst_6 : SMul 𝕜 E] [inst_7 : Module 𝕜 β]
  {s : Set E} {f : E → β}, StrictConvexOn 𝕜 s f → StrictConcaveOn 𝕜 s (-f)
-- Mathlib.Data.Matrix.PEquiv
PEquiv.toMatrix_bot : ∀ {m : Type u_3} {n : Type u_4} {α : Type u_5} [inst : DecidableEq n] [inst_1 : Zero α] [inst_2 : One α], ⊥.toMatrix = 0
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKeyD_erase_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k fallback : α}, (t.erase k).getKeyD k fallback = fallback
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_multiset_count : ∀ {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : DecidableEq M] (s : Multiset M),
  s.sum = ∑ m ∈ s.toFinset, Multiset.count m s • m
-- Mathlib.Algebra.Central.TensorProduct
Algebra.TensorProduct.includeRight_map_center_le : ∀ (K : Type u_1) (B : Type u_2) (C : Type u_3) [inst : CommSemiring K] [inst_1 : Semiring B] [inst_2 : Semiring C]
  [inst_3 : Algebra K B] [inst_4 : Algebra K C],
  Subalgebra.map Algebra.TensorProduct.includeRight (Subalgebra.center K C) ≤ Subalgebra.center K (TensorProduct K B C)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get!_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp],
  t.WF →
    ∀ {k a : α} [inst_1 : Inhabited (β a)] {v : β k},
      (t.insertIfNew k v).get! a = if h : cmp k a = Ordering.eq ∧ k ∉ t then cast ⋯ v else t.get! a
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.CoordinateRing.XYIdeal_add_eq : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Affine R} (x₁ x₂ y₁ ℓ : R),
  WeierstrassCurve.Affine.CoordinateRing.XYIdeal W' (W'.addX x₁ x₂ ℓ) (Polynomial.C (W'.addY x₁ x₂ y₁ ℓ)) =
    Ideal.span
        {(WeierstrassCurve.Affine.CoordinateRing.mk W')
            (W'.negPolynomial - Polynomial.C (WeierstrassCurve.Affine.linePolynomial x₁ y₁ ℓ))} ⊔
      WeierstrassCurve.Affine.CoordinateRing.XIdeal W' (W'.addX x₁ x₂ ℓ)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
WeierstrassCurve.Jacobian.Z_eq_zero_of_equiv : ∀ {R : Type r} [inst : CommRing R] {P Q : Fin 3 → R}, P ≈ Q → (P 2 = 0 ↔ Q 2 = 0)
-- Mathlib.Data.Fin.SuccPred
/-- `succ` commutes with `succAbove`.  -/
Fin.succ_succAbove_succ : ∀ {n : ℕ} (i : Fin (n + 1)) (j : Fin n), i.succ.succAbove j.succ = (i.succAbove j).succ
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.eq_norm_expr_nc : ∀ {α : Type u_1} [inst : Lean.Grind.Ring α] (ctx : Lean.Grind.CommRing.Context α)
  (lhs rhs lhs' rhs' : Lean.Grind.CommRing.Expr),
  Lean.Grind.CommRing.norm_eq_nc_cert lhs rhs lhs' rhs' = true →
    (Lean.Grind.CommRing.Expr.denote ctx lhs = Lean.Grind.CommRing.Expr.denote ctx rhs) =
      (Lean.Grind.CommRing.Expr.denote ctx lhs' = Lean.Grind.CommRing.Expr.denote ctx rhs')
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.id_tensorHom : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (V : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V] (D : Type u₃)
  [inst_4 : CategoryTheory.Category.{v₃, u₃} D]
  [inst_5 : CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore C V D]
  [inst_6 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d)
        (CategoryTheory.MonoidalCategory.tensorLeft v)]
  [inst_7 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  [inst_8 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  [inst_9 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) d)
        (CategoryTheory.MonoidalCategory.tensorLeft v)]
  (x : D) {y y' : D} (f : y ⟶ y'),
  CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id x) f =
    CategoryTheory.MonoidalCategoryStruct.whiskerLeft x f
-- Mathlib.SetTheory.Cardinal.Pigeonhole
/-- A function whose domain's cardinality is infinite and strictly greater than its codomain's
has a fiber with cardinality strictly great than the codomain.  -/
Cardinal.infinite_pigeonhole_card_lt : ∀ {β α : Type u} (f : β → α),
  Cardinal.mk α < Cardinal.mk β → Cardinal.aleph0 ≤ Cardinal.mk β → ∃ a, Cardinal.mk α < Cardinal.mk ↑(f ⁻¹' {a})
-- Mathlib.Data.List.NatAntidiagonal
/-- The antidiagonal of `0` is the list `[(0, 0)]`  -/
List.Nat.antidiagonal_zero : List.Nat.antidiagonal 0 = [(0, 0)]
-- Mathlib.Topology.Sheaves.Alexandrov
Alexandrov.exists_le_of_le_sup : ∀ {X : Type v} [inst : TopologicalSpace X] [inst_1 : Preorder X] [inst_2 : Topology.IsUpperSet X] {ι : Type v} {x : X}
  (Us : ι → TopologicalSpace.Opens X), Alexandrov.principalOpen x ≤ iSup Us → ∃ i, Alexandrov.principalOpen x ≤ Us i
-- Lean.Meta.Tactic.Grind.PP
_private.Lean.Meta.Tactic.Grind.PP.0.Lean.Meta.Grind.M : Type → Type
-- Mathlib.LinearAlgebra.Matrix.Polynomial
Polynomial.natDegree_det_X_add_C_le : ∀ {n : Type u_1} {α : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : CommRing α] (A B : Matrix n n α),
  (Polynomial.X • A.map ⇑Polynomial.C + B.map ⇑Polynomial.C).det.natDegree ≤ Fintype.card n
-- Mathlib.Data.Finset.Card
Finset.card_mk : ∀ {α : Type u_1} {m : Multiset α} {nodup : m.Nodup}, { val := m, nodup := nodup }.card = m.card
-- Lean.Expr
Lean.Literal.hash : Lean.Literal → UInt64
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
Matroid.Dep.of_isRestriction : ∀ {α : Type u_1} {M : Matroid α} {X : Set α} {N : Matroid α}, N.Dep X → N.IsRestriction M → M.Dep X
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Basic
/-- The differential in the complex of inhomogeneous chains used to calculate group homology.  -/
groupHomology.inhomogeneousChains.d : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      (A : Rep.{u, u, u} k G) → (n : ℕ) → ModuleCat.of k ((Fin (n + 1) → G) →₀ ↑A) ⟶ ModuleCat.of k ((Fin n → G) →₀ ↑A)
-- Mathlib.Algebra.Order.Group.OrderIso
OrderIso.mulLeft.eq_1 : ∀ {α : Type u} [inst : Group α] [inst_1 : LE α] [inst_2 : MulLeftMono α] (a : α),
  OrderIso.mulLeft a = { toEquiv := Equiv.mulLeft a, map_rel_iff' := ⋯ }