mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.normalCore_le : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G), H.normalCore ≤ H
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.instHasCokernelFromSubtype : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {K : Type}
  [inst_2 : Finite K] [inst_3 : CategoryTheory.Limits.HasFiniteBiproducts C] (f : K → C) (p : K → Prop),
  CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.biproduct.fromSubtype f p)
-- Mathlib.Analysis.Calculus.LogDeriv
/-- If two functions agree in a neighborhood of `x`, then so do their logarithmic derivatives.  -/
logDeriv_congr_nhds : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {f g : 𝕜 → 𝕜'} {x : 𝕜}, f =ᶠ[nhds x] g → logDeriv f =ᶠ[nhds x] logDeriv g
-- Mathlib.Topology.Connected.PathConnected
/-- If for each `i`, `x i` is joined to `y i` within `s i`, then `x` is joined to `y` within the
product set `Set.univ.pi s`.  -/
JoinedIn.pi : ∀ {ι : Type u_3} {Z : ι → Type u_4} [inst : (i : ι) → TopologicalSpace (Z i)] {s : (i : ι) → Set (Z i)}
  {x y : (i : ι) → Z i}, (∀ (i : ι), JoinedIn (s i) (x i) (y i)) → JoinedIn (Set.univ.pi s) x y
-- Mathlib.Data.Fintype.EquivFin
Equiv.ofRightInverseOfCardLE_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : Fintype β] (hαβ : Fintype.card α ≤ Fintype.card β)
  (f : α → β) (g : β → α) (h : Function.RightInverse g f) (a : α), (Equiv.ofRightInverseOfCardLE hαβ f g h) a = f a
-- Mathlib.Algebra.Order.GroupWithZero.Defs
/-- **Alias** of `lt_of_mul_lt_mul_right`. -/
lt_of_mul_lt_mul_of_nonneg_right : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] {a b c : α} [MulPosReflectLT α],
  b * a < c * a → 0 ≤ a → b < c
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.map₂_tprod_tprod : ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)]
  [inst_2 : (i : ι) → Module R (s i)] {t : ι → Type u_11} {t' : ι → Type u_12} [inst_3 : (i : ι) → AddCommMonoid (t i)]
  [inst_4 : (i : ι) → Module R (t i)] [inst_5 : (i : ι) → AddCommMonoid (t' i)] [inst_6 : (i : ι) → Module R (t' i)]
  (f : (i : ι) → s i →ₗ[R] t i →ₗ[R] t' i) (x : (i : ι) → s i) (y : (i : ι) → t i),
  ((PiTensorProduct.map₂ f) ((PiTensorProduct.tprod R) x)) ((PiTensorProduct.tprod R) y) =
    ⨂ₜ[R] (i : ι), ((f i) (x i)) (y i)
-- Mathlib.CategoryTheory.Sites.Types
CategoryTheory.subcanonical_typesGrothendieckTopology : CategoryTheory.typesGrothendieckTopology.Subcanonical
-- Mathlib.CategoryTheory.Limits.Lattice
CategoryTheory.Limits.CompleteLattice.finiteLimitCone_isLimit_lift : ∀ {α : Type u} {J : Type w} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.FinCategory J]
  [inst_2 : SemilatticeInf α] [inst_3 : OrderTop α] (F : CategoryTheory.Functor J α) (s : CategoryTheory.Limits.Cone F),
  (CategoryTheory.Limits.CompleteLattice.finiteLimitCone F).isLimit.lift s = CategoryTheory.homOfLE ⋯
-- Init.Data.List.Count
List.countP_cons_of_neg : ∀ {α : Type u_1} {p : α → Bool} {a : α} {l : List α}, ¬p a = true → List.countP p (a :: l) = List.countP p l
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.maxKey_le_maxKey_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α} {v : β}
  {he : t.isEmpty = false}, (cmp (t.maxKey he) ((t.insert k v).maxKey ⋯)).isLE = true
-- Aesop.Builder.Basic
Aesop.RuleBuilderOptions.mk : Option (Array Lean.Name) →
  Option Aesop.IndexingMode →
    Option (Array Aesop.CasesPattern) →
      Option Lean.Term →
        Option Lean.Meta.TransparencyMode → Option Lean.Meta.TransparencyMode → Aesop.RuleBuilderOptions
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
MeasureTheory.setLIntegral_congr_fun : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → ENNReal} {s : Set α},
  MeasurableSet s → Set.EqOn f g s → ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ
-- Lean.Meta.Tactic.Simp.SimpTheorems
_private.Lean.Meta.Tactic.Simp.SimpTheorems.0.Lean.Meta.preprocess : Lean.Expr → Lean.Expr → Bool → Bool → Lean.MetaM (List (Lean.Expr × Lean.Expr))
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
OrderedFinpartition.compAlongOrderedFinpartitionL_apply : ∀ {𝕜 : 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] {n : ℕ} (c : OrderedFinpartition n)
  (f : F [×c.length]→L[𝕜] G) (p : (i : Fin c.length) → E [×c.partSize i]→L[𝕜] F),
  ((OrderedFinpartition.compAlongOrderedFinpartitionL 𝕜 E F G c) f) p = c.compAlongOrderedFinpartition f p
-- Mathlib.Data.Fin.SuccPred
Fin.succAbove_ne_zero_zero : ∀ {n : ℕ} [inst : NeZero n] {a : Fin (n + 1)}, a ≠ 0 → a.succAbove 0 = 0
-- Mathlib.Analysis.Calculus.DerivativeTest
/-- The First Derivative test, maximum version.  -/
isLocalMax_of_deriv : ∀ {f : ℝ → ℝ} {b : ℝ},
  ContinuousAt f b →
    (∀ᶠ (x : ℝ) in nhdsWithin b {b}ᶜ, DifferentiableAt ℝ f x) →
      (∀ᶠ (x : ℝ) in nhdsWithin b (Set.Iio b), 0 ≤ deriv f x) →
        (∀ᶠ (x : ℝ) in nhdsWithin b (Set.Ioi b), deriv f x ≤ 0) → IsLocalMax f b
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.instAddZeroClass : {α : Type u} →
  {R : Type u_2} →
    [inst : TopologicalSpace α] →
      [inst_1 : PseudoMetricSpace R] →
        [inst_2 : AddZeroClass R] → [BoundedAdd R] → [ContinuousAdd R] → AddZeroClass (BoundedContinuousFunction α R)
-- Mathlib.Algebra.Ring.Subring.Defs
/-- A subring of a non-unital ring inherits a non-unital ring structure  -/
SubringClass.toNonAssocRing : {R : Type u} →
  {S : Type v} → [inst : NonAssocRing R] → [inst_1 : SetLike S R] → [hSR : SubringClass S R] → (s : S) → NonAssocRing ↥s
-- Mathlib.LinearAlgebra.Pi
LinearEquiv.finTwoArrow_apply : ∀ (R : Type u) (M : Type v) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  ⇑(LinearEquiv.finTwoArrow R M) = fun f => (f 0, f 1)
-- Mathlib.NumberTheory.MulChar.Basic
MulChar.ofUnitHom.eq_1 : ∀ {R : Type u_1} [inst : CommMonoid R] {R' : Type u_2} [inst_1 : CommMonoidWithZero R'] (f : Rˣ →* R'ˣ),
  MulChar.ofUnitHom f =
    { toFun := fun x => if hx : IsUnit x then ↑(f hx.unit) else 0, map_one' := ⋯, map_mul' := ⋯, map_nonunit' := ⋯ }
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.map_map : ∀ {m : Type u_1} {n : Type u_2} {A : Type u_5} {B : Type u_6} {C : Type u_7} {M : Matrix m n A} {f : A → B} {g : B → C},
  (M.map f).map g = M.map (g ∘ f)
-- Mathlib.Geometry.Manifold.ChartedSpace
/-- Same thing as `∀ i, H i`. We introduce it for technical reasons,
see note [Manifold type tags].  -/
ModelPi : {ι : Type u_5} → (ι → Type u_6) → Type (max u_5 u_6)
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.commSq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C),
  CategoryTheory.CommSq sq.f₁₂ sq.f₁₃ sq.f₂₄ sq.f₃₄
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.contains_eq_isSome_getElem? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {a : α},
  t.contains a = t[a]?.isSome
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.coe_sInf : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  (S : Set (LieSubalgebra R L)), ↑(sInf S) = ⋂ s ∈ S, ↑s
-- Mathlib.Tactic.TermCongr
/-- Given a `pf` of an `Iff`, `Eq`, or `HEq`, return a proof of `Eq`.
If `pf` is not obviously any of these, weakly try inserting `propext` to make an `Iff`
and otherwise unify the type with `Eq`.  -/
_private.Mathlib.Tactic.TermCongr.0.Mathlib.Tactic.TermCongr.CongrResult.mk'.toEqPf : Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Algebra.Order.Hom.Monoid
/-- Composition of `OrderAddMonoidHom`s as an `OrderAddMonoidHom`  -/
OrderAddMonoidHom.comp : {α : Type u_2} →
  {β : Type u_3} →
    {γ : Type u_4} →
      [inst : Preorder α] →
        [inst_1 : Preorder β] →
          [inst_2 : Preorder γ] →
            [inst_3 : AddZeroClass α] →
              [inst_4 : AddZeroClass β] → [inst_5 : AddZeroClass γ] → (β →+o γ) → (α →+o β) → α →+o γ
-- Init.Data.SInt.Lemmas
Int8.toInt_ofNat' : ∀ {n : ℕ}, (Int8.ofNat n).toInt = (↑n).bmod Int8.size
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
AugmentedSimplexCategory.equivAugmentedCosimplicialObject_functor_map_left : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C]
  {X Y : CategoryTheory.Functor (CategoryTheory.WithInitial SimplexCategory) C} (η : X ⟶ Y),
  (AugmentedSimplexCategory.equivAugmentedCosimplicialObject.functor.map η).left = η.app CategoryTheory.WithInitial.star
-- Mathlib.Order.Antisymmetrization
OrderHom.coe_antisymmetrization : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (f : α →o β),
  ⇑f.antisymmetrization = Quotient.map' ⇑f ⋯
-- Lean.Setup
Lean.ModuleSetup.mk.sizeOf_spec : ∀ (name : Lean.Name) (package? : Option Lean.PkgId) (isModule : Bool) (imports? : Option (Array Lean.Import))
  (importArts : Lean.NameMap Lean.ImportArtifacts) (dynlibs : Array System.FilePath) (plugins : Array Lean.Plugin)
  (options : Lean.LeanOptions),
  sizeOf
      { name := name, package? := package?, isModule := isModule, imports? := imports?, importArts := importArts,
        dynlibs := dynlibs, plugins := plugins, options := options } =
    1 + sizeOf name + sizeOf package? + sizeOf isModule + sizeOf imports? + sizeOf importArts + sizeOf dynlibs +
        sizeOf plugins +
      sizeOf options
-- Mathlib.Algebra.Group.Defs
isCancelMul_iff : ∀ (G : Type u) [inst : Mul G], IsCancelMul G ↔ IsLeftCancelMul G ∧ IsRightCancelMul G
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Matrix.linearIndependent_rows_of_invertible : ∀ {m : Type u} [inst : DecidableEq m] {K : Type u_3} [inst_1 : Field K] [inst_2 : Fintype m] (A : Matrix m m K)
  [Invertible A], LinearIndependent K A.row
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.functorP_obj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C), CategoryTheory.ShortComplex.SnakeInput.functorP.obj S = S.P
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.BinaryBicone.instIsSplitEpiSnd : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {P Q : C} (c : CategoryTheory.Limits.BinaryBicone P Q), CategoryTheory.IsSplitEpi c.snd
-- Init.GrindInstances.ToInt
Lean.Grind.instOfNatInt16SintOfNatNat : Lean.Grind.ToInt.OfNat Int16 (Lean.Grind.IntInterval.sint 16)
-- Mathlib.CategoryTheory.Yoneda
/-- Any corepresenting object for a corepresentable functor `F` is isomorphic to `coreprX F`.  -/
CategoryTheory.Functor.CorepresentableBy.isoCoreprX : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {F : CategoryTheory.Functor C (Type v)} →
      [hF : F.IsCorepresentable] → {Y : C} → F.CorepresentableBy Y → (Y ≅ F.coreprX)
-- Init.Data.List.Find
List.Sublist.findIdx?_isSome : ∀ {α : Type u_1} {p : α → Bool} {l₁ l₂ : List α},
  l₁.Sublist l₂ → (List.findIdx? p l₁).isSome = true → (List.findIdx? p l₂).isSome = true
-- Mathlib.Data.Nat.Bits
Nat.bit_lt_bit : ∀ {m n : ℕ} (a b : Bool), m < n → Nat.bit a m < Nat.bit b n
-- Mathlib.Topology.OpenPartialHomeomorph.Defs
OpenPartialHomeomorph.mapsTo_symm : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y), Set.MapsTo (↑e.symm) e.target e.source
-- Mathlib.LinearAlgebra.Matrix.Unique
/-- `M₁(A)` is equivalent to `A` as an `R`-algebra.  -/
Matrix.uniqueAlgEquiv : {m : Type u_1} →
  {A : Type u_3} →
    {R : Type u_4} →
      [inst : Unique m] →
        [inst_1 : Semiring A] → [inst_2 : CommSemiring R] → [inst_3 : Algebra R A] → Matrix m m A ≃ₐ[R] A
-- Mathlib.CategoryTheory.Sites.Precoverage
/-- **Alias** of `CategoryTheory.Functor.PreservesPairwisePullbacks.preservesLimit`. -/
CategoryTheory.Functor.preservesLimit_cospan_of_mem_presieve : ∀ {C : Type u_1} {D : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} C}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} D} {F : CategoryTheory.Functor C D} {X : C}
  (R : CategoryTheory.Presieve X) [self : F.PreservesPairwisePullbacks R] ⦃Y Z : C⦄ ⦃f : Y ⟶ X⦄ ⦃g : Z ⟶ X⦄,
  R f → R g → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) F
-- Init.Tactics
/-- `revert x...` is the inverse of `intro x...`: it moves the given hypotheses
into the main goal's target type.
 -/
Lean.Parser.Tactic.revert : Lean.ParserDescr
-- Mathlib.Algebra.DirectSum.Internal
SetLike.GradeZero.coe_intCast : ∀ {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [inst : Ring R] [inst_1 : AddMonoid ι] [inst_2 : SetLike σ R]
  [inst_3 : AddSubgroupClass σ R] (A : ι → σ) [inst_4 : SetLike.GradedMonoid A] (z : ℤ), ↑↑z = ↑z
-- Mathlib.CategoryTheory.Adjunction.Basic
/-- The hom set equivalence associated to an adjunction.  -/
CategoryTheory.Adjunction.homEquiv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          {G : CategoryTheory.Functor D C} → (F ⊣ G) → (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G.obj Y)
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
/-- The elliptic atom `Wₐ(a, b)` that defines an elliptic net. Note that this is defined in terms of
truncated integer division, and hence should only be used when `a` and `b` have the same parity.  -/
IsEllipticNet.atom : {R : Type u_1} → [CommRing R] → (ℤ → R) → ℤ → ℤ → R
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
/-- An additive monoid morphism `f : M ⟶ N` induces an additive monoid homomorphism
`M(X) →+ N(X)` for every `X`.  -/
CategoryTheory.IsAddMonHom.addMonoidHom : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v, u_1} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      {M N : C} →
        [inst_2 : CategoryTheory.AddMonObj M] →
          [inst_3 : CategoryTheory.AddMonObj N] →
            (f : M ⟶ N) → [CategoryTheory.IsAddMonHom f] → (X : C) → (X ⟶ M) →+ (X ⟶ N)
-- Mathlib.RepresentationTheory.Homological.FiniteCyclic
/-- Given a finite cyclic group `G` generated by `g` and a `G` representation `(V, ρ)`, `V_G` is
isomorphic to `V ⧸ Im(ρ(g - 1))`.  -/
Representation.FiniteCyclicGroup.coinvariantsEquiv : {k : Type u_1} →
  {G : Type u_2} →
    [inst : CommRing k] →
      [inst_1 : Group G] →
        {V : Type u_4} →
          [inst_2 : AddCommGroup V] →
            [inst_3 : Module k V] →
              (ρ : Representation k G V) →
                (g : G) →
                  [Fintype G] →
                    (∀ (x : G), x ∈ Subgroup.zpowers g) → ρ.Coinvariants ≃ₗ[k] V ⧸ (ρ g - LinearMap.id).range
-- Mathlib.LinearAlgebra.TensorProduct.Tower
TensorProduct.AlgebraTensorModule.lTensor_comp : ∀ {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {Q : Type uQ} {Q' : Type uQ'} [inst : CommSemiring R]
  [inst_1 : Semiring A] [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module A M]
  [inst_6 : IsScalarTower R A M] [inst_7 : AddCommMonoid N] [inst_8 : Module R N] [inst_9 : AddCommMonoid Q]
  [inst_10 : Module R Q] [inst_11 : AddCommMonoid Q'] [inst_12 : Module R Q'] (f₂ : Q →ₗ[R] Q') (f₁ : N →ₗ[R] Q),
  (TensorProduct.AlgebraTensorModule.lTensor A M) (f₂ ∘ₗ f₁) =
    (TensorProduct.AlgebraTensorModule.lTensor A M) f₂ ∘ₗ (TensorProduct.AlgebraTensorModule.lTensor A M) f₁
-- Batteries.Data.String.Lemmas
String.validFor_mkIterator : ∀ (s : String), String.Legacy.Iterator.ValidFor [] s.toList (String.Legacy.mkIterator s)
-- Mathlib.AlgebraicGeometry.ResidueField
AlgebraicGeometry.Scheme.instOverSpecResidueField : {X : AlgebraicGeometry.Scheme} → (x : ↥X) → (AlgebraicGeometry.Spec (X.residueField x)).Over X
-- Mathlib.Algebra.Homology.Embedding.RestrictionHomology
HomologicalComplex.restriction.sc'Iso_hom_τ₃ : ∀ {ι : 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]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsRelIff] (i j k : ι) {i' j' k' : ι'}
  (hi' : e.f i = i') (hj' : e.f j = j') (hk' : e.f k = k') (hi'' : c'.prev j' = i') (hk'' : c'.next j' = k'),
  (HomologicalComplex.restriction.sc'Iso K e i j k hi' hj' hk' hi'' hk'').hom.τ₃ = (K.restrictionXIso e hk').hom
-- Mathlib.Data.Matrix.DMatrix
DMatrix.instUnique : {m : Type u_1} → {n : Type u_2} → {α : m → n → Type v} → [(i : m) → (j : n) → Unique (α i j)] → Unique (DMatrix m n α)
-- Mathlib.Tactic.Attr.Register
/-- The simpset `qify_simps` is used by the tactic `qify` to move expressions from `ℕ` or `ℤ` to `ℚ`
which gives a well-behaved division.  -/
Parser.Attr.qify_simps : Lean.ParserDescr
-- Batteries.Data.List.Lemmas
List.set_eq_modify : ∀ {α : Type u_1} (a : α) (n : ℕ) (l : List α), l.set n a = l.modify n fun x => a
-- Mathlib.Algebra.Order.Group.Synonym
isAddRegular_toColex : ∀ {α : Type u_1} [inst : AddMonoid α] {a : α}, IsAddRegular (toColex a) ↔ IsAddRegular a
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
AffineMap.finrank_eq : ∀ {R : Type u_1} {S : Type u_2} {V : Type u_3} {W : Type u_4} {P : Type u_5} [inst : Ring R] [inst_1 : Ring S]
  [inst_2 : AddCommGroup V] [inst_3 : Module R V] [Module.Finite R V] [Module.Free R V] [inst_6 : AddTorsor V P]
  [inst_7 : AddCommGroup W] [inst_8 : Module R W] [inst_9 : Module S W] [Module.Finite S W]
  [inst_11 : SMulCommClass R S W] [Module.Free S W] [StrongRankCondition R] [StrongRankCondition S],
  Module.finrank S (P →ᵃ[R] W) = (Module.finrank R V + 1) * Module.finrank S W
-- Mathlib.Order.Monotone.Union
/-- If `f` is strictly monotone both on `s` and `t`, with `s` to the left of `t` and the center
point belonging to both `s` and `t`, then `f` is strictly monotone on `s ∪ t`  -/
StrictMonoOn.union : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : Preorder β] {f : α → β} {s t : Set α} {c : α},
  StrictMonoOn f s → StrictMonoOn f t → IsGreatest s c → IsLeast t c → StrictMonoOn f (s ∪ t)
-- Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Polynomial.isMonicOfDegree_X_add_one : ∀ {R : Type u_1} [inst : Semiring R] [Nontrivial R] (r : R), (Polynomial.X + Polynomial.C r).IsMonicOfDegree 1
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
AlgebraicGeometry.LocallyRingedSpace.restrict_presheaf_map : ∀ {U : TopCat} (X : AlgebraicGeometry.LocallyRingedSpace) {f : U ⟶ X.toTopCat}
  (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) {X_1 Y : (TopologicalSpace.Opens ↑U)ᵒᵖ}
  (f_1 : X_1 ⟶ Y), (X.restrict h).presheaf.map f_1 = X.presheaf.map (h.functor.map f_1.unop).op
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.support_C_mul_X_pow_subset : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : MulSemiringAction (Multiplicative ℕ) R] (n : ℕ) (c : R),
  (SkewPolynomial.C c * SkewPolynomial.X ^ n).support ⊆ {n}
-- Mathlib.Topology.FiberBundle.Basic
/-- The index set of a fiber bundle core, as a convenience function for dot notation  -/
FiberBundleCore.Index : {ι : Type u_1} →
  {B : Type u_2} →
    {F : Type u_3} → [inst : TopologicalSpace B] → [inst_1 : TopologicalSpace F] → FiberBundleCore ι B F → Type u_1
-- Lean.Meta.Tactic.Grind.Theorems
Lean.Meta.Grind.instInhabitedTheorems.default : {α : Type} → Lean.Meta.Grind.Theorems α
-- Mathlib.Algebra.Homology.DerivedCategory.SingleTriangle
CategoryTheory.ShortComplex.ShortExact.singleδ.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact),
  hS.singleδ =
    CategoryTheory.CategoryStruct.comp
      (((CategoryTheory.SingleFunctors.evaluation C (DerivedCategory C) 0).mapIso
              (DerivedCategory.singleFunctorsPostcompQIso C)).hom.app
        S.X₃)
      (CategoryTheory.CategoryStruct.comp (DerivedCategory.triangleOfSESδ ⋯)
        ((CategoryTheory.shiftFunctor (DerivedCategory C) 1).map
          (((CategoryTheory.SingleFunctors.evaluation C (DerivedCategory C) 0).mapIso
                  (DerivedCategory.singleFunctorsPostcompQIso C)).inv.app
            S.X₁)))
-- Mathlib.Algebra.Homology.ShortComplex.ModuleCat
CategoryTheory.ShortComplex.π_moduleCatCyclesIso_hom_assoc_apply : ∀ {R : Type u} [inst : Ring R] (S : CategoryTheory.ShortComplex (ModuleCat R)) {Z : ModuleCat R}
  (h : S.moduleCatLeftHomologyData.H ⟶ Z) (x : ↑S.cycles),
  (CategoryTheory.ConcreteCategory.hom h)
      ((CategoryTheory.ConcreteCategory.hom S.moduleCatHomologyIso.hom)
        ((CategoryTheory.ConcreteCategory.hom S.homologyπ) x)) =
    (CategoryTheory.ConcreteCategory.hom h)
      ((CategoryTheory.ConcreteCategory.hom S.moduleCatLeftHomologyData.π)
        ((CategoryTheory.ConcreteCategory.hom S.moduleCatCyclesIso.hom) x))
-- Mathlib.Combinatorics.Quiver.Covering
/-- The star of the symmetrification of a quiver at a vertex `u` is equivalent to the sum of the
star and the costar at `u` in the original quiver.  -/
Quiver.symmetrifyStar : {U : Type u_1} →
  [inst : Quiver U] → (u : U) → Quiver.Star (Quiver.Symmetrify.of.obj u) ≃ Quiver.Star u ⊕ Quiver.Costar u
-- Mathlib.CategoryTheory.Monad.Limits
/-- For `D : J ⥤ Coalgebra T`, `D ⋙ forget T` has a limit, then `D` has a limit provided limits
of shape `J` are preserved by `T`.
 -/
CategoryTheory.Comonad.forget_creates_limits_of_comonad_preserves : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [inst_1 : CategoryTheory.Category.{v, u} J]
  {T : CategoryTheory.Comonad C} [CategoryTheory.Limits.PreservesLimitsOfShape J T.toFunctor]
  (D : CategoryTheory.Functor J T.Coalgebra) [CategoryTheory.Limits.HasLimit (D.comp T.forget)],
  CategoryTheory.Limits.HasLimit D
-- Mathlib.Data.List.Sort
/-- **Alias** of the forward direction of `List.sortedLT_map_toDual`. -/
List.SortedLT.map_toDual : ∀ {α : Type u_1} [inst : Preorder α] {l : List α}, (List.map (⇑OrderDual.toDual) l).SortedLT → l.SortedGT
-- Mathlib.Data.Nat.Find
Nat.findGreatest_eq_zero_iff : ∀ {k : ℕ} {P : ℕ → Prop} [inst : DecidablePred P], Nat.findGreatest P k = 0 ↔ ∀ ⦃n : ℕ⦄, 0 < n → n ≤ k → ¬P n
-- Mathlib.Algebra.Ring.CentroidHom
/-- The canonical homomorphism from the center into the center of the centroid  -/
CentroidHom.centerToCentroidCenter : {α : Type u_5} →
  [inst : NonUnitalNonAssocSemiring α] → ↥(NonUnitalSubsemiring.center α) →ₙ+* ↥(Subsemiring.center (CentroidHom α))
-- Mathlib.Algebra.Lie.Subalgebra
LieEquiv.ofSubalgebras_apply : ∀ {R : Type u} {L₁ : Type v} {L₂ : Type w} [inst : CommRing R] [inst_1 : LieRing L₁] [inst_2 : LieRing L₂]
  [inst_3 : LieAlgebra R L₁] [inst_4 : LieAlgebra R L₂] (L₁' : LieSubalgebra R L₁) (L₂' : LieSubalgebra R L₂)
  (e : L₁ ≃ₗ⁅R⁆ L₂) (h : LieSubalgebra.map e.toLieHom L₁' = L₂') (x : ↥L₁'),
  ↑((LieEquiv.ofSubalgebras L₁' L₂' e h) x) = e ↑x
-- Std.Data.DHashMap.Internal.Raw
_private.Std.Data.DHashMap.Internal.Raw.0.Std.DHashMap.Raw.diff.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m₁ m₂ : Std.DHashMap.Raw α β),
  m₁.diff m₂ =
    if h₁ : 0 < m₁.buckets.size then
      if h₂ : 0 < m₂.buckets.size then ↑(Std.DHashMap.Internal.Raw₀.diff ⟨m₁, h₁⟩ ⟨m₂, h₂⟩) else m₁
    else m₂
-- Mathlib.CategoryTheory.Presentable.Finite
CategoryTheory.isFinitelyPresentable_iff_preservesFilteredColimits : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C},
  CategoryTheory.IsFinitelyPresentable X ↔
    CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.coyoneda.obj (Opposite.op X))
-- Mathlib.Topology.Irreducible
/-- A set is preirreducible if and only if
for every cover by two closed sets, it is contained in one of the two covering sets.  -/
isPreirreducible_iff_isClosed_union_isClosed : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X},
  IsPreirreducible s ↔ ∀ (z₁ z₂ : Set X), IsClosed z₁ → IsClosed z₂ → s ⊆ z₁ ∪ z₂ → s ⊆ z₁ ∨ s ⊆ z₂