mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Abelian.Preradical.Colon
CategoryTheory.Abelian.Preradical.shortComplexObj_X₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (Φ : CategoryTheory.Abelian.Preradical C) (X : C), (Φ.shortComplexObj X).X₂ = (CategoryTheory.Functor.id C).obj X
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
ContDiff.cosh : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {n : WithTop ℕ∞},
  ContDiff ℝ n f → ContDiff ℝ n fun x => Real.cosh (f x)
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitClosedDisc.instMulActionCircle : MulAction Circle Complex.UnitClosedDisc
-- Mathlib.Algebra.Homology.HomologicalComplex
/-- The differential mapping out of `C.X i`, or zero if there isn't one.
 -/
HomologicalComplex.dFrom : {ι : Type u_1} →
  {V : Type u} →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
        {c : ComplexShape ι} → (C : HomologicalComplex V c) → (i : ι) → C.X i ⟶ C.xNext i
-- Mathlib.Analysis.Normed.Module.Convex
convex_closedEBall : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (a : E) (r : ENNReal),
  Convex ℝ (Metric.closedEBall a r)
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddSubsemigroup.bot_prod_bot : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N], ⊥.prod ⊥ = ⊥
-- Mathlib.Combinatorics.Quiver.Cast
/-- Change the endpoints of a path using equalities.  -/
Quiver.Path.cast : {U : Type u_1} → [inst : Quiver U] → {u v u' v' : U} → u = u' → v = v' → Quiver.Path u v → Quiver.Path u' v'
-- Mathlib.GroupTheory.GroupAction.Defs
AddAction.vadd_mem_orbit_vadd : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] (g h : G) (a : α),
  g +ᵥ a ∈ AddAction.orbit G (h +ᵥ a)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.skipPrefix?_copy : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.ForwardPattern pat]
  [inst_1 : String.Slice.Pattern.Model.PatternModel pat] [String.Slice.Pattern.Model.LawfulForwardPatternModel pat]
  {s : String.Slice}, s.copy.skipPrefix? pat = Option.map String.Slice.Pos.copy (s.skipPrefix? pat)
-- Mathlib.Algebra.Order.Group.Nat
/-- See also `pow_left_strictMonoOn₀`.  -/
Nat.pow_left_strictMono : ∀ {n : ℕ}, n ≠ 0 → StrictMono fun x => x ^ n
-- Mathlib.Data.Fintype.Sets
Set.toFinset_nonempty : ∀ {α : Type u_1} {s : Set α} [inst : Fintype ↑s], s.toFinset.Nonempty ↔ s.Nonempty
-- Mathlib.Algebra.Order.Sub.Defs
AddLECancellable.lt_tsub_of_add_lt_right : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [OrderedSub α] {a b c : α},
  AddLECancellable c → a + c < b → a < b - c
-- Mathlib.Analysis.Normed.Group.Rat
Rat.instNormedAddCommGroup : NormedAddCommGroup ℚ
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
/-- `EqOnSource e e'` means that `e` and `e'` have the same source, and coincide there. They
should really be considered the same partial equivalence.  -/
OpenPartialHomeomorph.EqOnSource : {X : Type u_1} →
  {Y : Type u_3} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] → OpenPartialHomeomorph X Y → OpenPartialHomeomorph X Y → Prop
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.colimitsOfShape.mk' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C} {J : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} J] (X₁ X₂ : CategoryTheory.Functor J C)
  (c₁ : CategoryTheory.Limits.Cocone X₁) (c₂ : CategoryTheory.Limits.Cocone X₂)
  (h₁ : CategoryTheory.Limits.IsColimit c₁) (h₂ : CategoryTheory.Limits.IsColimit c₂) (f : X₁ ⟶ X₂),
  W.functorCategory J f →
    ∀ (φ : c₁.pt ⟶ c₂.pt),
      (∀ (j : J),
          CategoryTheory.CategoryStruct.comp (c₁.ι.app j) φ =
            CategoryTheory.CategoryStruct.comp (f.app j) (c₂.ι.app j)) →
        W.colimitsOfShape J φ
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get?_insertManyIfNewUnit_empty_list : ∀ {α : Type u} {instOrd : Ord α} [Std.TransOrd α] [inst : BEq α] [Std.LawfulBEqOrd α] {l : List α} {k : α},
  Std.DTreeMap.Internal.Impl.Const.get?
      (↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit Std.DTreeMap.Internal.Impl.empty l ⋯)) k =
    if l.contains k = true then some () else none
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getD_alter : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} [inst_2 : LawfulBEq α]
  {k k' : α} {fallback : β k'} {f : Option (β k) → Option (β k)},
  m.WF →
    (m.alter k f).getD k' fallback =
      if heq : (k == k') = true then (Option.map (cast ⋯) (f (m.get? k))).getD fallback else m.getD k' fallback
-- Mathlib.Tactic.Ring.Common
/-- Applies `⁻¹` to a polynomial to get an atom.  -/
Mathlib.Tactic.Ring.Common.evalInvAtom : {u : Lean.Level} →
  {α : Q(Type u)} →
    {bt : Q(«$α») → Type} →
      {sα : Q(CommSemiring «$α»)} →
        (dsα : Q(Semifield «$α»)) →
          (a : Q(«$α»)) →
            Mathlib.Tactic.AtomM (Mathlib.Tactic.Ring.Common.Result (Mathlib.Tactic.Ring.Common.ExBase bt sα) q(«$a»⁻¹))
-- Mathlib.Topology.Algebra.Group.Torsor
Homeomorph.constSDiv_apply : ∀ {V : Type u_1} {P : Type u_2} [inst : Group V] [inst_1 : TopologicalSpace V] [inst_2 : Torsor V P]
  [inst_3 : TopologicalSpace P] [inst_4 : IsTopologicalTorsor P] (p x : P), (Homeomorph.constSDiv p) x = p /ₛ x
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.addY_self : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} (P : Fin 3 → R), W'.addY P P = 0
-- Mathlib.Algebra.Homology.DifferentialObject
HomologicalComplex.d_eqToHom : ∀ {β : Type u_1} [inst : AddCommGroup β] (b : β) (V : Type u_2) [inst_1 : CategoryTheory.Category.{v_1, u_2} V]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms V] (X : HomologicalComplex V (ComplexShape.up' b)) {x y z : β}
  (h : y = z), CategoryTheory.CategoryStruct.comp (X.d x y) (CategoryTheory.eqToHom ⋯) = X.d x z
-- Mathlib.Algebra.Regular.Basic
/-- An element `a` is regular if and only if a positive power of `a` is regular.  -/
IsRegular.pow_iff : ∀ {R : Type u_1} [inst : Monoid R] {a : R} {n : ℕ}, 0 < n → (IsRegular (a ^ n) ↔ IsRegular a)
-- Mathlib.Analysis.CStarAlgebra.Classes
CommCStarAlgebra.toNormedAlgebra : {A : Type u_1} → [self : CommCStarAlgebra A] → NormedAlgebra ℂ A
-- Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
/-- A special case for when `a₂` has grade 0.  -/
GradedTensorProduct.tmul_coe_mul_zero_coe_tmul : ∀ {R : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring ι] [inst_1 : DecidableEq ι]
  [inst_2 : CommRing R] [inst_3 : Ring A] [inst_4 : Ring B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  (𝒜 : ι → Submodule R A) (ℬ : ι → Submodule R B) [inst_7 : GradedAlgebra 𝒜] [inst_8 : GradedAlgebra ℬ]
  [inst_9 : Module ι (Additive ℤˣ)] {j₁ : ι} (a₁ : A) (b₁ : ↥(ℬ j₁)) (a₂ : ↥(𝒜 0)) (b₂ : B),
  a₁ ᵍ⊗ₜ[R] ↑b₁ * ↑a₂ ᵍ⊗ₜ[R] b₂ = (a₁ * ↑a₂) ᵍ⊗ₜ[R] (↑b₁ * b₂)
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.compMeasurePreserving_eq_mk : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
  [inst_1 : TopologicalSpace γ] [inst_2 : MeasurableSpace β] {ν : MeasureTheory.Measure β} {f : α → β} (g : β →ₘ[ν] γ)
  (hf : MeasureTheory.MeasurePreserving f μ ν), g.compMeasurePreserving f hf = MeasureTheory.AEEqFun.mk (↑g ∘ f) ⋯
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.C_surjective : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] [IsEmpty σ], Function.Surjective ⇑MvPowerSeries.C
-- Init.Grind.Ring.CommSemiringAdapter
_private.Init.Grind.Ring.CommSemiringAdapter.0.Lean.Grind.CommRing.Expr.denoteS.match_1.eq_1 : ∀ (motive : Lean.Grind.CommRing.Expr → Sort u_1) (k : ℤ) (h_1 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.num k))
  (h_2 : (k : ℕ) → motive (Lean.Grind.CommRing.Expr.natCast k))
  (h_3 : (v : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var v))
  (h_4 : (a b : Lean.Grind.CommRing.Expr) → motive (a.add b))
  (h_5 : (a b : Lean.Grind.CommRing.Expr) → motive (a.mul b))
  (h_6 : (a : Lean.Grind.CommRing.Expr) → (k : ℕ) → motive (a.pow k))
  (h_7 : (a b : Lean.Grind.CommRing.Expr) → motive (a.sub b)) (h_8 : (a : Lean.Grind.CommRing.Expr) → motive a.neg)
  (h_9 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.intCast k)),
  (match Lean.Grind.CommRing.Expr.num k with
    | Lean.Grind.CommRing.Expr.num k => h_1 k
    | Lean.Grind.CommRing.Expr.natCast k => h_2 k
    | Lean.Grind.CommRing.Expr.var v => h_3 v
    | a.add b => h_4 a b
    | a.mul b => h_5 a b
    | a.pow k => h_6 a k
    | a.sub b => h_7 a b
    | a.neg => h_8 a
    | Lean.Grind.CommRing.Expr.intCast k => h_9 k) =
    h_1 k
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Ordinal.nfpFamily_lt_ord : ∀ {ι : Type u} {f : ι → Ordinal.{u} → Ordinal.{u}} {c : Ordinal.{u}},
  Cardinal.aleph0 < c.cof →
    Cardinal.mk ι < c.cof → (∀ (i : ι), ∀ b < c, f i b < c) → ∀ {a : Ordinal.{u}}, a < c → Ordinal.nfpFamily f a < c
-- Init.Data.Vector.Lemmas
Vector.toList_beq_toList : ∀ {α : Type u_1} {n : ℕ} [inst : BEq α] {xs ys : Vector α n}, (xs.toList == ys.toList) = (xs == ys)
-- Mathlib.GroupTheory.MonoidLocalization.Maps
Submonoid.LocalizationMap.of_mulEquivOfMulEquiv : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {P : Type u_3}
  [inst_2 : CommMonoid P] (f : S.LocalizationMap N) {T : Submonoid P} {Q : Type u_4} [inst_3 : CommMonoid Q]
  {k : T.LocalizationMap Q} {j : M ≃* P} (H : Submonoid.map j.toMonoidHom S = T),
  (f.ofMulEquivOfLocalizations (f.mulEquivOfMulEquiv k H)).toMonoidHom = k.toMonoidHom.comp j.toMonoidHom
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.containsThenInsertIfNew!_snd_eq_containsThenInsertIfNew_snd : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (t : Std.DTreeMap.Internal.Impl α β) (htb : t.Balanced) (a : α)
  (b : β a),
  (Std.DTreeMap.Internal.Impl.containsThenInsertIfNew! a b t).2 =
    (Std.DTreeMap.Internal.Impl.containsThenInsertIfNew a b t htb).2.impl
-- Mathlib.Geometry.Manifold.Submersion
Manifold.IsSubmersionAt.domChart_mem_maximalAtlas : ∀ {𝕜 : Type u_1} {E'' : Type u_3} {H : Type u_7} {G : Type u_9} {E : Type u} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E'']
  [inst_4 : NormedSpace 𝕜 E''] [inst_5 : TopologicalSpace H] [inst_6 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} {N : Type u_13} [inst_7 : TopologicalSpace M]
  [inst_8 : ChartedSpace H M] [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N}
  {x : M} (h : Manifold.IsSubmersionAt I J n f x), h.domChart ∈ IsManifold.maximalAtlas I n M
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getD_filter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {f : (a : α) → β a → Bool} {k : α} {fallback : β k},
  t.WF → (Std.DTreeMap.Raw.filter f t).getD k fallback = (Option.filter (f k) (t.get? k)).getD fallback
-- Mathlib.Algebra.GroupWithZero.Associated
Associates.mk_quot_out : ∀ {M : Type u_1} [inst : Monoid M] (a : M), Associated (Quot.out (Associates.mk a)) a
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.inv_mul : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {z : ℤ_[p]}, ‖z‖ = 1 → z.inv * z = 1
-- Mathlib.Data.PNat.Basic
PNat.one_add_natPred : ∀ (n : ℕ+), 1 + n.natPred = ↑n
-- Mathlib.Tactic.Basic
Mathlib.Tactic.evalIntrov : Lean.Elab.Tactic.Tactic
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousAlternatingMap.range_toAlternatingMap : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : TopologicalSpace M] [inst_4 : AddCommMonoid N] [inst_5 : Module R N]
  [inst_6 : TopologicalSpace N], Set.range ContinuousAlternatingMap.toAlternatingMap = {f | Continuous ⇑f}
-- Mathlib.CategoryTheory.Discrete.Basic
CategoryTheory.Discrete.functor_ext : ∀ {C : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} C] {I : Type u₁}
  {G F : CategoryTheory.Functor (CategoryTheory.Discrete I) C},
  (∀ (i : I), G.obj { as := i } = F.obj { as := i }) → G = F
-- Init.Data.Nat.Mod
Nat.lt_of_mul_lt_mul_left : ∀ {a b c : ℕ}, a * b < a * c → b < c
-- Mathlib.Topology.Semicontinuity.Defs
Semicontinuous.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] (r : α → β → Prop),
  Semicontinuous r = ∀ (x : α), SemicontinuousAt r x
-- Mathlib.Analysis.CStarAlgebra.Module.Constructions
WithCStarModule.norm_equiv_le_norm_prod : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] {E : Type u_2} {F : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : Module ℂ E] [inst_4 : SMul A E] [inst_5 : NormedAddCommGroup F]
  [inst_6 : Module ℂ F] [inst_7 : SMul A F] [inst_8 : CStarModule A E] [inst_9 : CStarModule A F] [StarOrderedRing A]
  (x : WithCStarModule A (E × F)), ‖(WithCStarModule.equiv A (E × F)) x‖ ≤ ‖x‖
-- Mathlib.Algebra.MvPolynomial.Polynomial
MvPolynomial.polynomial_eval_eval₂ : ∀ {R : Type u_1} {S : Type u_2} {σ : Type u_3} [inst : CommSemiring R] [inst_1 : CommSemiring S] {x : S}
  (f : R →+* Polynomial S) (g : σ → Polynomial S) (p : MvPolynomial σ R),
  Polynomial.eval x (MvPolynomial.eval₂ f g p) =
    MvPolynomial.eval₂ ((Polynomial.evalRingHom x).comp f) (fun s => Polynomial.eval x (g s)) p
-- Std.Internal.UV.TCP
/-- Gets the remote address of a connected TCP socket.
 -/
Std.Internal.UV.TCP.Socket.getPeerName : Std.Internal.UV.TCP.Socket → IO Std.Net.SocketAddress
-- Mathlib.Algebra.Quaternion
Quaternion.im_intCast : ∀ {R : Type u_3} [inst : CommRing R] (z : ℤ), (↑z).im = 0
-- Mathlib.CategoryTheory.Sites.MayerVietorisSquare
CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  [inst_1 : CategoryTheory.HasWeakSheafify J (Type v)] [inst_2 : CategoryTheory.HasSheafify J AddCommGrpCat]
  (S : J.MayerVietorisSquare),
  S.shortComplex.f =
    CategoryTheory.Limits.biprod.lift
      ((CategoryTheory.presheafToSheaf J AddCommGrpCat).map
        (CategoryTheory.Functor.whiskerRight (CategoryTheory.yoneda.map S.f₁₂) AddCommGrpCat.free))
      (-(CategoryTheory.presheafToSheaf J AddCommGrpCat).map
          (CategoryTheory.Functor.whiskerRight (CategoryTheory.yoneda.map S.f₁₃) AddCommGrpCat.free))
-- Mathlib.Analysis.Convex.StdSimplex
stdSimplex.eq_1 : ∀ (𝕜 : Type u_2) (ι : Type u_1) [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : Fintype ι],
  stdSimplex 𝕜 ι = {f | (∀ (x : ι), 0 ≤ f x) ∧ ∑ x, f x = 1}
-- Mathlib.Algebra.Order.Group.Cyclic
LinearOrderedCommGroup.Subgroup.genLTOne_mem : ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : LinearOrder G] [inst_2 : IsOrderedMonoid G] (H : Subgroup G)
  [inst_3 : Nontrivial ↥H] [hH : IsCyclic ↥H], LinearOrderedCommGroup.Subgroup.genLTOne H ∈ H
-- Init.Data.Fin.Lemmas
Fin.forall_iff : ∀ {n : ℕ} {p : Fin n → Prop}, (∀ (i : Fin n), p i) ↔ ∀ (i : ℕ) (h : i < n), p ⟨i, h⟩
-- Mathlib.NumberTheory.ClassNumber.Finite
/-- We can approximate `a / b : L` with `q / r`, where `r` has finitely many options for `L`.  -/
ClassGroup.exists_mem_finset_approx' : ∀ {R : Type u_1} {S : Type u_2} [inst : EuclideanDomain R] [inst_1 : CommRing S] [inst_2 : IsDomain S]
  [inst_3 : Algebra R S] {abv : AbsoluteValue R ℤ} {ι : Type u_5} [inst_4 : DecidableEq ι] [inst_5 : Fintype ι]
  (bS : Module.Basis ι R S) (adm : abv.IsAdmissible) [inst_6 : Infinite R] [inst_7 : DecidableEq R]
  [Algebra.IsAlgebraic R S] (a : S) {b : S},
  b ≠ 0 → ∃ q, ∃ r ∈ ClassGroup.finsetApprox bS adm, abv ((Algebra.norm R) (r • a - q * b)) < abv ((Algebra.norm R) b)
-- Mathlib.CategoryTheory.Monad.Algebra
CategoryTheory.Monad.Algebra.Hom.ext'_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {X Y : T.Algebra}
  {f g : X ⟶ Y}, f = g ↔ f.f = g.f
-- Mathlib.LinearAlgebra.DirectSum.Finsupp
TensorProduct.finsuppLeft'_apply : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] {M : Type u_3}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module S M] [inst_6 : IsScalarTower R S M] {N : Type u_4}
  [inst_7 : AddCommMonoid N] [inst_8 : Module R N] {ι : Type u_5} [inst_9 : DecidableEq ι]
  (x : TensorProduct R (ι →₀ M) N), (TensorProduct.finsuppLeft R S M N ι) x = (TensorProduct.finsuppLeft R S M N ι) x
-- Mathlib.Analysis.Convex.Quasiconvex
ConcaveOn.quasiconcaveOn : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid β] [inst_4 : PartialOrder β] [IsOrderedAddMonoid β] [inst_6 : Module 𝕜 E]
  [inst_7 : Module 𝕜 β] [PosSMulMono 𝕜 β] {s : Set E} {f : E → β}, ConcaveOn 𝕜 s f → QuasiconcaveOn 𝕜 s f
-- Mathlib.LinearAlgebra.TensorProduct.Submodule
Submodule.mulMap_map_comp_eq : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] (M N : Submodule R S)
  {T : Type w} [inst_3 : Semiring T] [inst_4 : Algebra R T] (f : S →ₐ[R] T),
  (Submodule.map (↑f) M).mulMap (Submodule.map (↑f) N) ∘ₗ
      TensorProduct.map ((↑f).submoduleMap M) ((↑f).submoduleMap N) =
    ↑f ∘ₗ M.mulMap N
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.mem_support_derivative : ∀ {R : Type u} {n : ℕ} [inst : Semiring R] {p : Polynomial R} [IsAddTorsionFree R],
  n ∈ (Polynomial.derivative p).support ↔ n + 1 ∈ p.support
-- Mathlib.RepresentationTheory.Homological.TateCohomology.Basic
/-- The chain map on the Tate complex induced by a morphism of representations.  -/
tateComplex.map : {R G : Type u} →
  [inst : CommRing R] →
    [inst_1 : Group G] → [inst_2 : Fintype G] → {X Y : Rep.{u, u, u} R G} → (X ⟶ Y) → (tateComplex X ⟶ tateComplex Y)
-- Mathlib.SetTheory.ZFC.Basic
/-- Kuratowski ordered pair  -/
ZFSet.pair : ZFSet.{u} → ZFSet.{u} → ZFSet.{u}
-- Mathlib.Order.Concept
Concept.ofObject_le_ofAttribute_iff : ∀ {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {a : α} {b : β},
  Concept.ofObject r a ≤ Concept.ofAttribute r b ↔ r a b
-- Mathlib.Data.Finset.Sups
Finset.infs_subset_iff : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeInf α] {s t u : Finset α},
  s ⊼ t ⊆ u ↔ ∀ a ∈ s, ∀ b ∈ t, a ⊓ b ∈ u
-- Mathlib.Algebra.Colimit.Module
AddCommGroup.DirectLimit.addCommGroup : {ι : Type u_2} →
  [inst : Preorder ι] →
    [inst_1 : DecidableEq ι] →
      (G : ι → Type u_4) →
        [inst_2 : (i : ι) → AddCommGroup (G i)] →
          (f : (i j : ι) → i ≤ j → G i →+ G j) → AddCommGroup (AddCommGroup.DirectLimit G f)
-- Aesop.Forward.RuleInfo
/-- Index of the slot. Slots are always part of a list of slots, and `index`
is the 0-based index of this slot in that list.  -/
Aesop.Slot.index : Aesop.Slot → Aesop.SlotIndex
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.ofList_eq_empty_iff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)},
  Std.ExtDHashMap.Const.ofList l = ∅ ↔ l = []
-- Mathlib.Data.Set.Card
Set.Finite.encard_lt_encard : ∀ {α : Type u_1} {s t : Set α}, s.Finite → s ⊂ t → s.encard < t.encard
-- Mathlib.RingTheory.AdicCompletion.Algebra
/-- `AdicCompletion.transitionMap` as an algebra homomorphism.  -/
AdicCompletion.transitionMapₐ : {R : Type u_1} → [inst : CommRing R] → (I : Ideal R) → {m n : ℕ} → m ≤ n → R ⧸ I ^ n • ⊤ →ₐ[R] R ⧸ I ^ m • ⊤
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Finite
CategoryTheory.Limits.hasFiniteColimits_of_hasColimits_of_createsFiniteColimits : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.HasFiniteColimits D]
  [CategoryTheory.Limits.CreatesFiniteColimits F], CategoryTheory.Limits.HasFiniteColimits C
-- Mathlib.Analysis.InnerProductSpace.Positive
/-- `LinearMap.trace` as a positive linear map.  -/
LinearMap.tracePositiveLinearMap : (𝕜 : Type u_1) →
  (E : Type u_2) →
    [inst : RCLike 𝕜] → [inst_1 : NormedAddCommGroup E] → [inst_2 : InnerProductSpace 𝕜 E] → (E →ₗ[𝕜] E) →ₚ[𝕜] 𝕜
-- Mathlib.Algebra.Homology.Embedding.IsSupported
/-- If `K : HomologicalComplex C c'`, then `K.IsStrictlySupported e` holds for
an embedding `e : c.Embedding c'` of complex shapes if `K.X i'` is zero
whenever `i'` is not of the form `e.f i` for some `i`.  -/
HomologicalComplex.IsStrictlySupported : {ι : Type u_1} →
  {ι' : Type u_2} →
    {c : ComplexShape ι} →
      {c' : ComplexShape ι'} →
        {C : Type u_3} →
          [inst : CategoryTheory.Category.{v_1, u_3} C] →
            [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] → HomologicalComplex C c' → c.Embedding c' → Prop
-- Mathlib.Analysis.Real.Cardinality
Cardinal.cantorFunctionAux.eq_1 : ∀ (c : ℝ) (f : ℕ → Bool) (n : ℕ), Cardinal.cantorFunctionAux c f n = bif f n then c ^ n else 0
-- Mathlib.Topology.DiscreteQuotient
/-- Comap a discrete quotient along a continuous map.  -/
DiscreteQuotient.comap : {X : Type u_2} →
  {Y : Type u_3} →
    [inst : TopologicalSpace X] → [inst_1 : TopologicalSpace Y] → C(X, Y) → DiscreteQuotient Y → DiscreteQuotient X
-- Lean.Elab.InfoTree.Types
Lean.Elab.CompletionInfo.endSection : Lean.Syntax → Option Lean.Name → Bool → List String → Lean.Elab.CompletionInfo
-- Mathlib.Data.ENNReal.Operations
ENNReal.iSup_sub : ∀ {ι : Sort u_1} {f : ι → ENNReal} {a : ENNReal}, (⨆ i, f i) - a = ⨆ i, f i - a
-- Mathlib.Analysis.Convex.Body
/-- A convex body that is symmetric contains `0`.  -/
ConvexBody.zero_mem_of_symmetric : ∀ {V : Type u_1} [inst : TopologicalSpace V] [inst_1 : AddCommGroup V] [inst_2 : Module ℝ V] (K : ConvexBody V),
  (∀ x ∈ K, -x ∈ K) → 0 ∈ K
-- Mathlib.Algebra.Order.Group.OrderIso
neg_le : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α] [AddLeftMono α] [AddRightMono α] {a b : α}, -a ≤ b ↔ -b ≤ a
-- Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
SimplexCategory.δ₀Iter_succ'_assoc : ∀ (i : ℕ) {n m : ℕ} (h : autoParam (n + (i + 1) = m) SimplexCategory.δ₀Iter_succ'._auto_1) {Z : SimplexCategory}
  (h_1 : { len := m } ⟶ Z),
  CategoryTheory.CategoryStruct.comp (SimplexCategory.δ₀Iter (i + 1) h) h_1 =
    CategoryTheory.CategoryStruct.comp (SimplexCategory.δ 0)
      (CategoryTheory.CategoryStruct.comp (SimplexCategory.δ₀Iter i ⋯) h_1)
-- Mathlib.RingTheory.RingHom.Finite
RingHom.finite_stableUnderComposition : RingHom.StableUnderComposition @RingHom.Finite
-- Mathlib.FieldTheory.IntermediateField.ExtendRight
IntermediateField.extendRight.algebraMap_extendRightEquiv'_symm : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (F : IntermediateField K L)
  (M : Type u_3) [inst_3 : Field M] [inst_4 : Algebra K M] [inst_5 : Algebra L M] [inst_6 : IsScalarTower K L M]
  (S : Type u_5) [inst_7 : CommRing S] [inst_8 : Algebra S ↥F] [inst_9 : Algebra S M] [inst_10 : IsScalarTower S (↥F) M]
  (a : ↥(F.extendRight M)), (algebraMap (↥F) M) ((F.extendRightEquiv' M S).symm a) = ↑a
-- Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity
UniqueFactorizationMonoid.associated_finprod_pow_count : ∀ {R : Type u_2} [inst : CommMonoidWithZero R] [inst_1 : UniqueFactorizationMonoid R] [inst_2 : NormalizationMonoid R]
  [inst_3 : DecidableEq R] {x : R},
  x ≠ 0 → Associated (∏ᶠ (p : R), p ^ Multiset.count p (UniqueFactorizationMonoid.normalizedFactors x)) x
-- Init.Data.Array.Basic
_private.Init.Data.Array.Basic.0.Array.findIdx?_loop_eq_map_findFinIdx?_loop_val : ∀ {α : Type u} {xs : Array α} {p : α → Bool} {j : ℕ},
  Array.findIdx?.loop p xs j = Option.map (fun x => ↑x) (Array.findFinIdx?.loop✝ p xs j)
-- Std.Http.Protocol.H1.Parser
/-- Parses a single header field line.

`field-line = field-name ":" OWS field-value OWS`
 -/
_private.Std.Http.Protocol.H1.Parser.0.Std.Http.Protocol.H1.parseFieldLine : Std.Http.Protocol.H1.Config → Std.Internal.Parsec.ByteArray.Parser (String × String)
-- Mathlib.Order.CountableSupClosed
CountableInfClosed.empty : ∀ {α : Type u_2} [inst : LE α], CountableInfClosed ∅
-- Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Real.locallyFinite_volume : MeasureTheory.IsLocallyFiniteMeasure MeasureTheory.volume