mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.Interval.Basic
NonemptyInterval.coe_add_interval : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : Add α] [inst_2 : AddLeftMono α] [inst_3 : AddRightMono α]
  (s t : NonemptyInterval α), ↑(s + t) = ↑s + ↑t
-- Mathlib.Algebra.Group.Equiv.Defs
MulEquiv.surjective : ∀ {M : Type u_4} {N : Type u_5} [inst : Mul M] [inst_1 : Mul N] (e : M ≃* N), Function.Surjective ⇑e
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.exists_eval_ne_zero_of_natDegree_lt_card : ∀ {R : Type u} [inst : CommRing R] [IsDomain R] (f : Polynomial R),
  f ≠ 0 → ↑f.natDegree < Cardinal.mk R → ∃ r, Polynomial.eval r f ≠ 0
-- Lean.Parser.Command
/-- Adds a docstring to an existing declaration, replacing any existing docstring.
The provided docstring should be written as a docstring for the `add_decl_doc` command, as in
```
/-- My new docstring -/
add_decl_doc oldDeclaration
```

This is useful for auto-generated declarations
for which there is no place to write a docstring in the source code.

Parent projections in structures are an example of this:
```
structure Triple (α β γ : Type) extends Prod α β where
  thrd : γ

/-- Extracts the first two projections of a triple. -/
add_decl_doc Triple.toProd
```

Documentation can only be added to declarations in the same module.
 -/
Lean.Parser.Command.addDocString : Lean.Parser.Parser
-- Mathlib.LinearAlgebra.TensorProduct.Basic
TensorProduct.addCommGroup : {R : Type u_1} →
  [inst : CommSemiring R] →
    {M : Type u_2} →
      {N : Type u_3} →
        [inst_1 : AddCommGroup M] →
          [inst_2 : AddCommMonoid N] →
            [inst_3 : Module R M] → [inst_4 : Module R N] → AddCommGroup (TensorProduct R M N)
-- Mathlib.Algebra.Group.Units.Defs
isUnit_iff_eq_one : ∀ {M : Type u_1} [inst : Monoid M] {a : M} [Subsingleton Mˣ], IsUnit a ↔ a = 1
-- Mathlib.Geometry.Euclidean.Circumcenter
/-- Two n-simplices among cospherical points in an n-dimensional
subspace have the same circumsphere.  -/
EuclideanGeometry.circumsphere_eq_of_cospherical_subset : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : AffineSubspace ℝ P} {ps : Set P},
  ps ⊆ ↑s →
    ∀ [Nonempty ↥s] {n : ℕ} [FiniteDimensional ℝ ↥s.direction],
      Module.finrank ℝ ↥s.direction = n →
        EuclideanGeometry.Cospherical ps →
          ∀ {sx₁ sx₂ : Affine.Simplex ℝ P n},
            Set.range sx₁.points ⊆ ps → Set.range sx₂.points ⊆ ps → sx₁.circumsphere = sx₂.circumsphere
-- Mathlib.FieldTheory.RatFunc.AsPolynomial
RatFunc.algebraMap_C : ∀ {K : Type u} [inst : CommRing K] [inst_1 : IsDomain K] (a : K),
  (algebraMap (Polynomial K) (RatFunc K)) (Polynomial.C a) = RatFunc.C a
-- Mathlib.RingTheory.Filtration
Ideal.Filtration.inf_submodule : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {I : Ideal R}
  (F F' : I.Filtration M), (F ⊓ F').submodule = F.submodule ⊓ F'.submodule
-- Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder
/-- Any nontrivial linearly ordered abelian group with zero that is locally finite
is isomorphic to `ℤᵐ⁰`.  -/
LocallyFiniteOrder.orderMonoidWithZeroEquiv : (G : Type u_3) →
  [inst : LinearOrderedCommGroupWithZero G] →
    [LocallyFiniteOrder Gˣ] → [Nontrivial Gˣ] → G ≃*o WithZero (Multiplicative ℤ)
-- Mathlib.Algebra.Polynomial.Div
Polynomial.pow_mul_divByMonic_rootMultiplicity_eq : ∀ {R : Type u} [inst : Ring R] (p : Polynomial R) (a : R),
  (Polynomial.X - Polynomial.C a) ^ Polynomial.rootMultiplicity a p *
      (p /ₘ (Polynomial.X - Polynomial.C a) ^ Polynomial.rootMultiplicity a p) =
    p
-- Mathlib.RepresentationTheory.Character
FDRep.character.eq_1 : ∀ {k : Type u} [inst : Field k] {G : Type v} [inst_1 : Monoid G] (V : FDRep k G) (g : G),
  V.character g = (LinearMap.trace k ↑V.V) (V.ρ g)
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.mem_mk_iff : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (S : Set L)
  (h₁ : ∀ {a b : L}, a ∈ S → b ∈ S → a + b ∈ S) (h₂ : S 0)
  (h₃ :
    ∀ (c : R) {x : L},
      x ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂ }.carrier →
        c • x ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂ }.carrier)
  (h₄ :
    ∀ {x y : L},
      x ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃ }.carrier →
        y ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃ }.carrier →
          ⁅x, y⁆ ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃ }.carrier)
  {x : L}, x ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃, lie_mem' := h₄ } ↔ x ∈ S
-- Mathlib.LinearAlgebra.SpecialLinearGroup
Matrix.SpecialLinearGroup.toLin_equiv.toLinearMap_eq : ∀ {R : Type u_1} {V : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup V] [inst_2 : Module R V] {n : Type u_3}
  [inst_3 : Fintype n] [inst_4 : DecidableEq n] (b : Module.Basis n R V) (g : Matrix.SpecialLinearGroup n R),
  ↑↑((Matrix.SpecialLinearGroup.toLin_equiv b) g) = (Matrix.toLin b b) ↑g
-- Mathlib.CategoryTheory.Sites.Sheaf
CategoryTheory.sheafBotEquivalence_counitIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (A : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} A],
  (CategoryTheory.sheafBotEquivalence A).counitIso =
    CategoryTheory.Iso.refl
      ({ obj := fun P => { obj := P, property := ⋯ }, map := fun {X Y} f => { hom := f }, map_id := ⋯,
            map_comp := ⋯ }.comp
        (CategoryTheory.sheafToPresheaf ⊥ A))
-- Init.Data.Ord.Basic
Ordering.isNe_iff_ne_eq : ∀ {o : Ordering}, o.isNe = true ↔ ¬o = Ordering.eq
-- Mathlib.Topology.Compactification.OnePoint.Basic
OnePoint.equivOfIsEmbeddingOfRangeEq_apply_coe : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : T2Space Y]
  [inst_3 : CompactSpace Y] (y : Y) (f : X → Y) (hf : Topology.IsEmbedding f) (hy : Set.range f = {y}ᶜ) (x : X),
  (OnePoint.equivOfIsEmbeddingOfRangeEq y f hf hy) ↑x = f x
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Grading
ExteriorAlgebra.GradedAlgebra.ι_apply : ∀ (R : Type u_1) (M : Type u_2) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (m : M),
  (ExteriorAlgebra.GradedAlgebra.ι R M) m = (DirectSum.of (fun i => ↥(⋀[R]^i M)) 1) ⟨(ExteriorAlgebra.ι R) m, ⋯⟩
-- Mathlib.Order.CompleteLattice.Finset
Finset.minimal_iff_forall_erase : ∀ {α : Type u_2} [inst : DecidableEq α] {P : Finset α → Prop} {s : Finset α},
  (∀ ⦃s t : Finset α⦄, P t → t ⊆ s → P s) → (Minimal P s ↔ P s ∧ ∀ x ∈ s, ¬P (s.erase x))
-- Mathlib.Analysis.Normed.Module.Connected
Metric.isPreconnected_eball : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [NormedSpace ℝ E] {x : E} {r : ENNReal},
  IsPreconnected (Metric.eball x r)
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.StructuralAtom.rightUnitor.inj : ∀ {e : Lean.Expr} {f : Mathlib.Tactic.BicategoryLike.Mor₁} {e_1 : Lean.Expr} {f_1 : Mathlib.Tactic.BicategoryLike.Mor₁},
  Mathlib.Tactic.BicategoryLike.StructuralAtom.rightUnitor e f =
      Mathlib.Tactic.BicategoryLike.StructuralAtom.rightUnitor e_1 f_1 →
    e = e_1 ∧ f = f_1
-- Mathlib.CategoryTheory.Action
CategoryTheory.ActionCategory.curry_apply_right : ∀ {X : Type u} {G : Type u_2} [inst : Group G] [inst_1 : MulAction G X] {H : Type u_3} [inst_2 : Group H]
  (F : CategoryTheory.Functor (CategoryTheory.ActionCategory G X) (CategoryTheory.SingleObj H)) (g : G),
  ((CategoryTheory.ActionCategory.curry F) g).right = g
-- Mathlib.Algebra.Lie.Weights.IsSimple
LieIdeal.rootSet_apply_coroot_eq_zero_of_notMem_rootSet : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : LieRing L] [inst_2 : LieAlgebra K L]
  [inst_3 : FiniteDimensional K L] {H : LieSubalgebra K L} [inst_4 : H.IsCartanSubalgebra] [CharZero K]
  [inst_6 : LieAlgebra.IsKilling K L] [LieModule.IsTriangularizable K (↥H) L] (I : LieIdeal K L)
  {α : ↥LieSubalgebra.root},
  α ∈ I.rootSet → ∀ {β : ↥LieSubalgebra.root}, β ∉ I.rootSet → ↑α (LieAlgebra.IsKilling.coroot ↑β) = 0
-- Mathlib.Order.RelSeries
/-- A type is finite dimensional if its `LTSeries` has bounded length.  -/
FiniteDimensionalOrder : (γ : Type u_3) → [Preorder γ] → Prop
-- Mathlib.Analysis.Polynomial.Basic
Polynomial.div_tendsto_atTop_of_degree_gt : ∀ {𝕜 : Type u_1} [inst : NormedField 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (P Q : Polynomial 𝕜)
  [OrderTopology 𝕜],
  Q.degree < P.degree →
    Q ≠ 0 →
      0 ≤ P.leadingCoeff / Q.leadingCoeff →
        Filter.Tendsto (fun x => Polynomial.eval x P / Polynomial.eval x Q) Filter.atTop Filter.atTop
-- Mathlib.Algebra.Group.Hom.Defs
/-- Group homomorphisms preserve inverse.  -/
MonoidHom.map_inv : ∀ {α : Type u_2} {β : Type u_3} [inst : Group α] [inst_1 : DivisionMonoid β] (f : α →* β) (a : α), f a⁻¹ = (f a)⁻¹
-- Mathlib.RingTheory.MvPolynomial.EulerIdentity
/-- Euler's identity for homogeneous polynomials.  -/
MvPolynomial.IsHomogeneous.sum_X_mul_pderiv : ∀ {R : Type u_1} {σ : Type u_2} [inst : CommSemiring R] {φ : MvPolynomial σ R} [inst_1 : Fintype σ] {n : ℕ},
  φ.IsHomogeneous n → ∑ i, MvPolynomial.X i * (MvPolynomial.pderiv i) φ = n • φ
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Real.iteratedDeriv_add_one_cosh : ∀ (n : ℕ), iteratedDeriv (n + 1) Real.cosh = iteratedDeriv n Real.sinh
-- Mathlib.Analysis.Calculus.FDeriv.Add
DifferentiableAt.sub_iff_right : ∀ {𝕜 : 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}
  {x : E}, DifferentiableAt 𝕜 f x → (DifferentiableAt 𝕜 (f - g) x ↔ DifferentiableAt 𝕜 g x)
-- Mathlib.CategoryTheory.Abelian.Preradical.Colon
/-- For `X : C`, the morphism `(toColon Φ Ψ)` is an isomorphism if and only if
`(Ψ.r.obj (Φ.quotient.obj X))` is the zero object.  -/
CategoryTheory.Abelian.Preradical.isIso_toColon_hom_left_app_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {Φ Ψ : CategoryTheory.Abelian.Preradical C} {X : C},
  CategoryTheory.IsIso ((CategoryTheory.Over.Hom.left (Φ.toColon Ψ).hom).app X) ↔
    CategoryTheory.Limits.IsZero (Ψ.r.obj (Φ.quotient.obj X))
-- Init.Data.List.Sort.Lemmas
_private.Init.Data.List.Sort.Lemmas.0.List.mergeSort.eq_2 : ∀ {α : Type u_1} (x : α → α → Bool) (a : α), [a].mergeSort x = [a]
-- Mathlib.Algebra.Group.Irreducible.Indecomposable
IsAddIndecomposable.subset : ∀ {ι : Type u_1} {M : Type u_2} [inst : AddMonoid M] (v : ι → M) (s : Set ι), {i | IsAddIndecomposable v s i} ⊆ s
-- Mathlib.Algebra.BigOperators.Fin
Fin.prod_Iio_castLE : ∀ {M : Type u_2} [inst : CommMonoid M] {n m : ℕ} (h : n ≤ m) (f : Fin m → M) (a : Fin n),
  ∏ i < Fin.castLE h a, f i = ∏ i < a, f (Fin.castLE h i)
-- Batteries.Data.List.Lemmas
List.getElem_swap_right : ∀ {α : Type u_1} {xs : List α} {i j : ℕ} (hj : j < (xs.swap i j).length),
  (xs.swap i j)[j] = if hi : i < xs.length then xs[i] else xs[j]
-- Mathlib.CategoryTheory.Monoidal.Category
/-- The pentagon identity relating the isomorphism between `X ⊗ (Y ⊗ (Z ⊗ W))` and `((X ⊗ Y) ⊗ Z) ⊗ W`
 -/
CategoryTheory.MonoidalCategory.pentagon_assoc : ∀ {C : Type u} {𝒞 : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.MonoidalCategory C] (W X Y Z : C) {Z_1 : C}
  (h :
    CategoryTheory.MonoidalCategoryStruct.tensorObj W
        (CategoryTheory.MonoidalCategoryStruct.tensorObj X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)) ⟶
      Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.associator W X Y).hom
        Z)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.associator W (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z).hom
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft W
            (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom)
          h)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorObj W X) Y Z).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.associator W X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)).hom
        h)
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.fromEdgeSet_univ : ∀ {V : Type u}, SimpleGraph.fromEdgeSet Set.univ = ⊤
-- Init.Data.String.Pattern.String
String.Slice.Pattern.ForwardSliceSearcher.instForwardPattern : {pat : String.Slice} → String.Slice.Pattern.ForwardPattern pat
-- Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence
_private.Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence.0.Mathlib.Tactic.Monoidal.«term_◁_» : Lean.TrailingParserDescr
-- Mathlib.GroupTheory.FiniteIndexNormalSubgroup
FiniteIndexNormalSubgroup.instSetLike : {G : Type u_1} → [inst : Group G] → SetLike (FiniteIndexNormalSubgroup G) G
-- Mathlib.GroupTheory.FiniteIndexNormalSubgroup
FiniteIndexNormalSubgroup.instSubgroupClass : ∀ {G : Type u_1} [inst : Group G], SubgroupClass (FiniteIndexNormalSubgroup G) G
-- Mathlib.CategoryTheory.Shift.ShiftedHomOpposite
CategoryTheory.ShiftedHom.opEquiv_symm_apply_comp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ] {X Y : C} {a : ℤ}
  (f : CategoryTheory.ShiftedHom (Opposite.op X) (Opposite.op Y) a) {b : ℤ} {Z : C}
  (z : CategoryTheory.ShiftedHom X Z b) {c : ℤ} (h : b + a = c),
  ((CategoryTheory.ShiftedHom.opEquiv a).symm f).comp z h =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.ShiftedHom.opEquiv a).symm (CategoryTheory.CategoryStruct.comp (Quiver.Hom.op z) f))
      ((CategoryTheory.shiftFunctorAdd' C b a c h).inv.app Z)
-- Lean.Meta.MonadSimp
Lean.Meta.MonadSimp.withNewLemmas : {m : Type → Type} → [self : Lean.Meta.MonadSimp m] → {α : Type} → Array Lean.Expr → m α → m α
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.prod_cons : ∀ {ι : Type u_1} {M : Type u_4} {s : Finset ι} {a : ι} [inst : CommMonoid M] {f : ι → M} (h : a ∉ s),
  ∏ x ∈ Finset.cons a s h, f x = f a * ∏ x ∈ s, f x
-- Mathlib.Algebra.Group.Action.Defs
IsCancelVAdd.left_cancel : ∀ {G : Type u_11} {P : Type u_12} [inst : VAdd G P] [IsCancelVAdd G P] (a : G) (b c : P), a +ᵥ b = a +ᵥ c → b = c
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.update_eq_erase : ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → Zero (β i)] [inst_1 : DecidableEq ι] (f : Π₀ (i : ι), β i) (i : ι),
  f.update i 0 = DFinsupp.erase i f
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.prod.inl_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C)
  [inst_2 : CategoryTheory.Limits.HasBinaryProduct X Y],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.inl X Y) CategoryTheory.Limits.prod.fst =
    CategoryTheory.CategoryStruct.id X
-- Init.Data.SInt.Lemmas
Int8.toInt8_toInt32 : ∀ (n : Int8), n.toInt32.toInt8 = n
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.maxKey!_eq_default : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → t.isEmpty = true → t.maxKey! = default
-- Mathlib.RingTheory.Ideal.Operations
Ideal.mem_radical_of_pow_mem : ∀ {R : Type u} [inst : CommSemiring R] {I : Ideal R} {x : R} {m : ℕ}, x ^ m ∈ I.radical → x ∈ I.radical
-- Mathlib.RingTheory.Polynomial.Ideal
Polynomial.ker_modByMonicHom : ∀ {R : Type u_1} [inst : CommRing R] {q : Polynomial R},
  q.Monic → q.modByMonicHom.ker = Submodule.restrictScalars R (Ideal.span {q})
-- Mathlib.GroupTheory.Sylow
Sylow.instFiniteQuotientSubgroupNormalizer : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] [Fact (Nat.Prime p)] [Finite (Sylow p G)] (P : Sylow p G),
  Finite (G ⧸ Subgroup.normalizer ↑P)
-- Mathlib.Analysis.Asymptotics.Defs
/-- **Alias** of the reverse direction of `Asymptotics.isBigOWith_abs_right`. -/
Asymptotics.IsBigOWith.abs_right : ∀ {α : Type u_1} {E : Type u_3} [inst : Norm E] {c : ℝ} {f : α → E} {l : Filter α} {u : α → ℝ},
  Asymptotics.IsBigOWith c l f u → Asymptotics.IsBigOWith c l f fun x => |u x|
-- Lean.Meta.Tactic.Grind.Types
/-- State of the injective function procedure.  -/
Lean.Meta.Grind.GoalState.inj : Lean.Meta.Grind.GoalState → Lean.Meta.Grind.Injective.State
-- Mathlib.Topology.Homotopy.Basic
/-- Given continuous maps `f₀` and `f₁`, we say `f₀` and `f₁` are homotopic if there exists a
`ContinuousMap.Homotopy f₀ f₁`.
 -/
ContinuousMap.Homotopic : {X : Type u} → {Y : Type v} → [inst : TopologicalSpace X] → [inst_1 : TopologicalSpace Y] → C(X, Y) → C(X, Y) → Prop
-- Init.Data.String.Lemmas.Pattern.String.ForwardPattern
_private.Init.Data.String.Lemmas.Pattern.String.ForwardPattern.0.String.Slice.Pattern.BackwardSliceSearcher.isSome_skipSuffix? : ∀ {pat s : String.Slice},
  (String.Slice.Pattern.BackwardSliceSearcher.skipSuffix? pat s).isSome =
    String.Slice.Pattern.BackwardSliceSearcher.endsWith pat s
-- Mathlib.CategoryTheory.Limits.Shapes.Preorder.Basic
Preorder.instHasColimitsOfShape : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (J : Type w) [inst_1 : Preorder J] [OrderTop J],
  CategoryTheory.Limits.HasColimitsOfShape J C
-- Mathlib.LinearAlgebra.Projectivization.PSL.Stabilizer
Matrix.SpecialLinearGroup.mem_lineStab_iff : ∀ {F : Type u_1} [inst : Field F] {ι : Type u_2} [inst_1 : DecidableEq ι] [inst_2 : Fintype ι]
  (A : Matrix.SpecialLinearGroup ι F) (L : Submodule F (ι → F)),
  A ∈ Matrix.SpecialLinearGroup.lineStab L ↔ ∀ (w : ι → F), A • w - w ∈ L
-- Mathlib.Topology.Algebra.UniformConvergence
UniformOnFun.ofFun_smul : ∀ {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} {M : Type u_5} [inst : SMul M β] (c : M) (f : α → β),
  (UniformOnFun.ofFun 𝔖) (c • f) = c • (UniformOnFun.ofFun 𝔖) f
-- Mathlib.LinearAlgebra.Matrix.Trace
Matrix.traceLinearMap_apply : ∀ (n : Type u_3) (α : Type u_5) (R : Type u_6) [inst : Fintype n] [inst_1 : AddCommMonoid R] [inst_2 : Semiring α]
  [inst_3 : Module α R] (A : Matrix n n R), (Matrix.traceLinearMap n α R) A = A.trace
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
MonotoneOn.const_add : ∀ {α : Type u_1} {β : Type u_2} [inst : Add α] [inst_1 : Preorder α] [inst_2 : Preorder β] {f : β → α} {s : Set β}
  [AddLeftMono α], MonotoneOn f s → ∀ (a : α), MonotoneOn (fun x => a + f x) s
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
CategoryTheory.Limits.biprod.map_lift_mapBiprod : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] (X Y : C)
  [inst_5 : CategoryTheory.Limits.HasBinaryBiproduct X Y]
  [inst_6 : CategoryTheory.Limits.PreservesBinaryBiproduct X Y F] {W : C} (f : W ⟶ X) (g : W ⟶ Y),
  CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Limits.biprod.lift f g)) (F.mapBiprod X Y).hom =
    CategoryTheory.Limits.biprod.lift (F.map f) (F.map g)
-- Mathlib.GroupTheory.Subgroup.Simple
/-- Any normal additive subgroup is either `⊥` or `⊤`  -/
IsSimpleAddGroup.eq_bot_or_eq_top_of_normal : ∀ {A : Type u_2} {inst : AddGroup A} [self : IsSimpleAddGroup A] (H : AddSubgroup A), H.Normal → H = ⊥ ∨ H = ⊤
-- Mathlib.GroupTheory.GroupAction.Primitive
/-- The codomain of an equivariant map of large image is preprimitive if the domain is.  -/
AddAction.IsPreprimitive.of_card_lt : ∀ {G : Type u_1} {X : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G X] {H : Type u_3} {Y : Type u_4}
  [inst_2 : AddGroup H] [inst_3 : AddAction H Y] {φ : G → H} {f : X →ₑ[φ] Y} [Finite Y] [AddAction.IsPretransitive H Y]
  [AddAction.IsPreprimitive G X], Nat.card Y < 2 * (Set.range ⇑f).ncard → AddAction.IsPreprimitive H Y
-- Init.Prelude
/-- Throws an exception of type `ε` to the nearest enclosing `catch`.
 -/
MonadExceptOf.throw : {ε : semiOutParam (Type u)} → {m : Type v → Type w} → [self : MonadExceptOf ε m] → {α : Type v} → ε → m α
-- Mathlib.RingTheory.Extension.Presentation.Submersive
Algebra.PreSubmersivePresentation.jacobian_eq_det_aevalDifferential : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.PreSubmersivePresentation R S ι σ) [inst_3 : Finite σ], P.jacobian = LinearMap.det P.aevalDifferential
-- Mathlib.CategoryTheory.ObjectProperty.HasCardinalLT
/-- The property that the subtype of objects satisfying a property `P : ObjectProperty C`
is of cardinality `< κ`.  -/
CategoryTheory.ObjectProperty.HasCardinalLT : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.ObjectProperty C → Cardinal.{w} → Prop
-- Mathlib.Algebra.Order.Interval.Set.Instances
Set.Ico.coe_lt_one : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : PartialOrder R] (x : ↑(Set.Ico 0 1)), ↑x < 1
-- Mathlib.Analysis.ODE.Transform
IsIntegralCurveOn.comp_mul : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {γ : ℝ → E} {v : ℝ → E → E} {s : Set ℝ},
  IsIntegralCurveOn γ v s → ∀ (a : ℝ), IsIntegralCurveOn (γ ∘ fun x => x * a) (a • v ∘ fun x => x * a) {t | t * a ∈ s}
-- Mathlib.Data.QPF.Multivariate.Constructions.Const
MvQPF.Const.map_mk : ∀ {n : ℕ} {A : Type u} {α β : TypeVec.{u} n} (f : α.Arrow β) (x : A),
  MvFunctor.map f (MvQPF.Const.mk x) = MvQPF.Const.mk x
-- Mathlib.Analysis.Normed.Affine.ContinuousAffineMap
ContinuousAffineMap.toConstProdContinuousLinearMap_fst : ∀ (𝕜 : Type u_1) (V : Type u_3) (W : Type u_4) [inst : SeminormedAddCommGroup V] [inst_1 : SeminormedAddCommGroup W]
  [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NormedSpace 𝕜 V] [inst_4 : NormedSpace 𝕜 W] (f : V →ᴬ[𝕜] W),
  ((ContinuousAffineMap.toConstProdContinuousLinearMap 𝕜 V W) f).1 = f 0
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
IsCyclotomicExtension.Rat.inertiaDeg_eq_of_prime_pow : ∀ (p k : ℕ) [hp : Fact (Nat.Prime p)] (K : Type u_1) [inst : Field K] [inst_1 : NumberField K]
  [hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K] (P : Ideal (NumberField.RingOfIntegers K)) [hP₁ : P.IsPrime]
  [hP₂ : P.LiesOver (Ideal.span {↑p})], P.inertiaDeg ℤ = 1
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
SubMulAction.ENat_card_ofStabilizer_add_one_eq : ∀ (G : Type u_1) [inst : Group G] {α : Type u_2} [inst_1 : MulAction G α] (a : α),
  ENat.card ↥(SubMulAction.ofStabilizer G a) + 1 = ENat.card α
-- Mathlib.Order.Partition.Basic
Partition.eq_or_disjoint : ∀ {α : Type u_1} {s x y : α} [inst : CompleteLattice α] {P : Partition s}, x ∈ P → y ∈ P → x = y ∨ Disjoint x y
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_mul_const_Ico_of_neg : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] (a b : α) {c : α},
  c < 0 → (fun x => x * c) ⁻¹' Set.Ico a b = Set.Ioc (b / c) (a / c)
-- Mathlib.Topology.FiberBundle.Trivialization
/-- Natural identification as a `Pretrivialization`.  -/
Bundle.Trivialization.toPretrivialization : {B : Type u_1} →
  {F : Type u_2} →
    {Z : Type u_4} →
      [inst : TopologicalSpace B] →
        [inst_1 : TopologicalSpace F] →
          {proj : Z → B} →
            [inst_2 : TopologicalSpace Z] → Bundle.Trivialization F proj → Bundle.Pretrivialization F proj
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.CompactOpens.coe_top : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : CompactSpace α], ↑⊤ = Set.univ
-- Mathlib.Combinatorics.Matroid.IndepAxioms
IndepMatroid.matroid_E : ∀ {α : Type u_1} (M : IndepMatroid α), M.matroid.E = M.E
-- Std.Data.TreeSet.Basic
/-- Partitions a tree set into two tree sets based on a predicate.  -/
Std.TreeSet.partition : {α : Type u} → {cmp : α → α → Ordering} → (α → Bool) → Std.TreeSet α cmp → Std.TreeSet α cmp × Std.TreeSet α cmp
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
/-- The type of angles  -/
Real.Angle : Type
-- Mathlib.Topology.Order.AtTopBotIxx
comap_coe_Iio_nhdsLT : ∀ {X : Type u_1} [inst : LinearOrder X] [inst_1 : TopologicalSpace X] [OrderTopology X] (a : X),
  autoParam (Order.IsSuccPrelimit a) comap_coe_Iio_nhdsLT._auto_1 →
    Filter.comap Subtype.val (nhdsWithin a (Set.Iio a)) = Filter.atTop