mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Matrix.Vec
/-- The starred Hadamard bilinear form equals the starred Kronecker bilinear form on diagonal
embeddings.  -/
Matrix.star_dotProduct_hadamard_mulVec_eq_kronecker : ∀ {m : Type u_2} {n : Type u_3} {R : Type u_1} [inst : NonUnitalSemiring R] [inst_1 : DecidableEq m]
  [inst_2 : Fintype m] [inst_3 : DecidableEq n] [inst_4 : Fintype n] [inst_5 : StarAddMonoid R] (x : m → R)
  (A B : Matrix m n R) (x' : n → R),
  star x ⬝ᵥ (A.hadamard B).mulVec x' =
    star (Matrix.diagonal x).vec ⬝ᵥ (Matrix.kroneckerMap (fun x1 x2 => x1 * x2) A B).mulVec (Matrix.diagonal x').vec
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
/-- the dimension of each type (II) simplex  -/
SSet.Subcomplex.PairingCore.dim : {X : SSet} → {A : X.Subcomplex} → (self : A.PairingCore) → self.ι → ℕ
-- Mathlib.Algebra.Ring.PUnit
PUnit.instIsCancelMulZero : IsCancelMulZero PUnit.{u_1 + 1}
-- Mathlib.Analysis.Matrix.Order
/-- **Schur product theorem**: the Hadamard (entrywise) product of positive definite
matrices is positive definite.  -/
Matrix.PosDef.hadamard : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {ι : Type u_3} {A B : Matrix ι ι 𝕜}, A.PosDef → B.PosDef → (A.hadamard B).PosDef
-- Init.Data.Nat.Div.Lemmas
Nat.mod_mod_eq_mod_mod_mod : ∀ {a b c : ℕ}, a < c → b < c → a % b % c = a % c % (b % c)
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.inl_v_snd_v : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] (p q : ℤ)
  (hpq : p + -1 = q),
  CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inl φ).v p q hpq)
      ((CochainComplex.mappingCone.snd φ).v q q ⋯) =
    0
-- Mathlib.Order.Filter.Prod
Filter.prod_iInf_right : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} [Nonempty ι] {f : Filter α} {g : ι → Filter β},
  f ×ˢ ⨅ i, g i = ⨅ i, f ×ˢ g i
-- Mathlib.Algebra.Group.Center
/-- multiplication commutes  -/
IsMulCentral.comm : ∀ {M : Type u_1} [inst : Mul M] {z : M}, IsMulCentral z → ∀ (a : M), Commute z a
-- Mathlib.RingTheory.Derivation.Basic
Derivation.instIsScalarTower : ∀ {R : Type u_1} {A : Type u_2} {M : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : AddCommMonoid M] [inst_3 : Algebra R A] [inst_4 : Module A M] [inst_5 : Module R M] {S : Type u_5}
  {T : Type u_6} [inst_6 : Monoid S] [inst_7 : DistribMulAction S M] [inst_8 : SMulCommClass R S M]
  [inst_9 : SMulCommClass S A M] [inst_10 : Monoid T] [inst_11 : DistribMulAction T M] [inst_12 : SMulCommClass R T M]
  [inst_13 : SMulCommClass T A M] [inst_14 : SMul S T] [IsScalarTower S T M], IsScalarTower S T (Derivation R A M)
-- Mathlib.Algebra.Category.Grp.Basic
CommGrpCat.mk : (carrier : Type u) → [str : CommGroup carrier] → CommGrpCat
-- Lean.Parser.Term
Lean.Parser.semicolonOrLinebreak : Lean.Parser.Parser
-- Lean.Meta.Tactic.Grind.Types
/-- `interpreted := true` if node should be viewed as an abstract value.  -/
Lean.Meta.Grind.ENode.interpreted : Lean.Meta.Grind.ENode → Bool
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyMapData.ofIsColimitCokernelCofork_φH : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (hg₁ : S₁.g = 0)
  (c₁ : CategoryTheory.Limits.CokernelCofork S₁.f) (hc₁ : CategoryTheory.Limits.IsColimit c₁) (hg₂ : S₂.g = 0)
  (c₂ : CategoryTheory.Limits.CokernelCofork S₂.f) (hc₂ : CategoryTheory.Limits.IsColimit c₂) (f : c₁.pt ⟶ c₂.pt)
  (comm :
    CategoryTheory.CategoryStruct.comp φ.τ₂ (CategoryTheory.Limits.Cofork.π c₂) =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofork.π c₁) f),
  (CategoryTheory.ShortComplex.LeftHomologyMapData.ofIsColimitCokernelCofork φ hg₁ c₁ hc₁ hg₂ c₂ hc₂ f comm).φH = f
-- Init.Data.List.Count
List.Sublist.count_le : ∀ {α : Type u_1} [inst : BEq α] {l₁ l₂ : List α} (a : α), l₁.Sublist l₂ → List.count a l₁ ≤ List.count a l₂
-- Mathlib.Algebra.Group.Submonoid.Defs
AddSubmonoid.subtype.eq_1 : ∀ {M : Type u_4} [inst : AddZeroClass M] (S : AddSubmonoid M),
  S.subtype = { toFun := Subtype.val, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.Order.Cover
WCovBy.stdRefl : ∀ {α : Type u_1} [inst : Preorder α], Std.Refl fun x1 x2 => x1 ⩿ x2
-- Lean.Environment
/-- Obsolete simpler version of `exportEntriesFnEx` that returns the same entries for all levels.
Its value is ignored if the latter is also specified.
 -/
Lean.PersistentEnvExtensionDescr.exportEntriesFn : {α β σ : Type} → Lean.PersistentEnvExtensionDescr α β σ → σ → Array α
-- Init.Coe
instCoeTCOfCoe : {β : Sort u_1} → {γ : Sort u_2} → {α : Sort u_3} → [Coe β γ] → [CoeTC α β] → CoeTC α γ
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.degree_lt_iff_coeff_zero : ∀ {R : Type u} [inst : Semiring R] (f : Polynomial R) (n : ℕ), f.degree < ↑n ↔ ∀ (m : ℕ), n ≤ m → f.coeff m = 0
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.GrothendieckTopology.OneHypercover.comp_s₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {S : C}
  {X Y Z : J.OneHypercover S} (f : X.Hom Y) (g : Y.Hom Z) {i j : X.I₀} (a : X.I₁ i j),
  (CategoryTheory.CategoryStruct.comp f g).s₁ a = g.s₁ (f.s₁ a)
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable
/-- If the indicator functions of a.e.-measurable sets `Aᵢ` converge a.e. to the indicator function
of a set `A` along a nontrivial countably generated filter, then `A` is also a.e.-measurable.  -/
nullMeasurableSet_of_tendsto_indicator : ∀ {α : Type u_3} [inst : MeasurableSpace α] {A : Set α} {ι : Type u_4} (L : Filter ι) [L.IsCountablyGenerated]
  {As : ι → Set α} [L.NeBot] {μ : MeasureTheory.Measure α},
  (∀ (i : ι), MeasureTheory.NullMeasurableSet (As i) μ) →
    (∀ᵐ (x : α) ∂μ, ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A) → MeasureTheory.NullMeasurableSet A μ
-- Mathlib.Topology.Algebra.ConstMulAction
/-- The scalar multiplication `(•) : Γ → T → T` is continuous in the second argument.  -/
ContinuousConstSMul.continuous_const_smul : ∀ {Γ : Type u_1} {T : Type u_2} {inst : TopologicalSpace T} {inst_1 : SMul Γ T} [self : ContinuousConstSMul Γ T]
  (γ : Γ), Continuous fun x => γ • x
-- Mathlib.Order.Max
noBotOrder_iff_noMinOrder : ∀ (α : Type u_3) [inst : LinearOrder α], NoBotOrder α ↔ NoMinOrder α
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey?_eq_none : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], (↑m).WF → ∀ {a : α}, m.contains a = false → m.getKey? a = none
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.uniqueIioOne : Unique ↑(Set.Iio 1)
-- Mathlib.Algebra.Order.ToIntervalMod
toIocMod_sub_self : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α), toIocMod hp a b - b = -toIocDiv hp a b • p
-- Init.Data.Order.Lemmas
Classical.Order.instLawfulOrderLT : ∀ {α : Type u} [inst : LE α], Std.LawfulOrderLT α
-- Mathlib.Order.OmegaCompletePartialOrder
/-- Iteration of a function on an initial element interpreted as a chain.  -/
OmegaCompletePartialOrder.fixedPoints.iterateChain : {α : Type u_2} →
  [inst : OmegaCompletePartialOrder α] → (f : α →o α) → (x : α) → x ≤ f x → OmegaCompletePartialOrder.Chain α
-- Mathlib.Analysis.Complex.ReImTopology
Complex.frontier_setOfPred_im_le : ∀ (a : ℝ), frontier {z | z.im ≤ a} = {z | z.im = a}
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnModule.of_sub : ∀ {Γ : Type u_1} {R : Type u_3} {V : Type u_5} [inst : PartialOrder Γ] [inst_1 : SMul R V] [inst_2 : AddCommGroup V]
  (x y : HahnSeries Γ V), (HahnModule.of R) (x - y) = (HahnModule.of R) x - (HahnModule.of R) y
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.iUnion_bot : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι}, ⊥.iUnion = ∅
-- Std.Time.Date.Basic
/-- Convert `Week.Offset` into `Nanosecond.Offset`.
 -/
Std.Time.Nanosecond.Offset.ofWeeks : Std.Time.Week.Offset → Std.Time.Nanosecond.Offset
-- Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
ENNReal.tendsto_rpow_atBot_of_base_lt_one : ∀ {b : ENNReal}, b < 1 → Filter.Tendsto (fun x => b ^ x) Filter.atBot (nhds ⊤)
-- Std.Time.Time.Unit.Nanosecond
Std.Time.Nanosecond.instSubOffset : Sub Std.Time.Nanosecond.Offset
-- Init.Prelude
Nat.not_lt_zero : ∀ (n : ℕ), ¬n < 0
-- Mathlib.Topology.LocallyConstant.Basic
/-- The locally constant function to `Fin 2` associated to a clopen set.  -/
LocallyConstant.ofIsClopen : {X : Type u_5} →
  [inst : TopologicalSpace X] → {U : Set X} → [(x : X) → Decidable (x ∈ U)] → IsClopen U → LocallyConstant X (Fin 2)
-- Lean.Data.Lsp.Workspace
Lean.Lsp.instToJsonDidChangeWatchedFilesRegistrationOptions.toJson : Lean.Lsp.DidChangeWatchedFilesRegistrationOptions → Lean.Json
-- Mathlib.RingTheory.Ideal.Height
Ideal.height_strict_mono_of_isPrime_of_isPrime : ∀ {R : Type u_1} [inst : CommRing R] {I J : Ideal R} [I.IsPrime] [J.IsPrime],
  I < J → ∀ [J.FiniteHeight], I.height < J.height
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.eq_bot_of_subsingleton : ∀ {M : Type u_1} [inst : MulOneClass M] (S : Submonoid M) [Subsingleton ↥S], S = ⊥
-- Mathlib.GroupTheory.OrderOfElement
/-- The equivalence between `Subgroup.zpowers` of two elements `x, y` of the same order, mapping
`x ^ i` to `y ^ i`.  -/
zpowersEquivZPowers : {G : Type u_1} →
  [inst : Group G] → {x y : G} → [Finite G] → orderOf x = orderOf y → ↥(Subgroup.zpowers x) ≃ ↥(Subgroup.zpowers y)
-- Mathlib.Algebra.Ring.Opposite
AddOpposite.instNonUnitalNonAssocRing : {R : Type u_1} → [NonUnitalNonAssocRing R] → NonUnitalNonAssocRing Rᵃᵒᵖ
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.arrowArrowEquivalence'_inverse : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  CategoryTheory.Square.arrowArrowEquivalence'.inverse = CategoryTheory.Square.fromArrowArrowFunctor'
-- Mathlib.FieldTheory.Galois.Basic
IntermediateField.fixingSubgroup_fixedField : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (H : Subgroup Gal(E/F))
  [FiniteDimensional F E], (IntermediateField.fixedField H).fixingSubgroup = H
-- Lean.Meta.AppBuilder
Lean.Meta.mkNone : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
HurwitzZeta.hurwitzZetaOdd_neg : ∀ (a : UnitAddCircle) (s : ℂ), HurwitzZeta.hurwitzZetaOdd (-a) s = -HurwitzZeta.hurwitzZetaOdd a s
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
CategoryTheory.StrictlyUnitaryLaxFunctor.ext_iff : ∀ {B : Type u₁} {inst : CategoryTheory.Bicategory B} {C : Type u₂} {inst_1 : CategoryTheory.Bicategory C}
  {x y : CategoryTheory.StrictlyUnitaryLaxFunctor B C},
  x = y ↔
    x.obj = y.obj ∧
      @Prefunctor.map B inst.toQuiver C inst_1.toQuiver x.toPrefunctor ≍
          @Prefunctor.map B inst.toQuiver C inst_1.toQuiver y.toPrefunctor ∧
        @CategoryTheory.PrelaxFunctorStruct.map₂ B inst.toQuiver
              (fun a b => (CategoryTheory.Bicategory.homCategory a b).toQuiver) C inst_1.toQuiver
              (fun a b => (CategoryTheory.Bicategory.homCategory a b).toQuiver) x.toPrelaxFunctorStruct ≍
            @CategoryTheory.PrelaxFunctorStruct.map₂ B inst.toQuiver
              (fun a b => (CategoryTheory.Bicategory.homCategory a b).toQuiver) C inst_1.toQuiver
              (fun a b => (CategoryTheory.Bicategory.homCategory a b).toQuiver) y.toPrelaxFunctorStruct ∧
          x.mapId ≍ y.mapId ∧
            @CategoryTheory.LaxFunctor.mapComp B inst C inst_1 x.toLaxFunctor ≍
              @CategoryTheory.LaxFunctor.mapComp B inst C inst_1 y.toLaxFunctor
-- Mathlib.Topology.Order.Priestley
PriestleySpace.mk : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : TopologicalSpace α],
  (∀ {x y : α}, ¬x ≤ y → ∃ U, IsClopen U ∧ IsUpperSet U ∧ x ∈ U ∧ y ∉ U) → PriestleySpace α
-- Mathlib.Algebra.Module.ZLattice.Summable
ZLattice.summable_norm_sub_rpow : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] (L : Submodule ℤ E)
  [DiscreteTopology ↥L], ∀ r < -↑(Module.finrank ℤ ↥L), ∀ (x : E), Summable fun z => ‖↑z - x‖ ^ r
-- Mathlib.Tactic.LinearCombination.Lemmas
Mathlib.Tactic.LinearCombination.smul_lt_const_weak : ∀ {α : Type u_1} {K : Type u_2} {t s : K} [inst : Ring K] [inst_1 : PartialOrder K] [IsOrderedRing K]
  [inst_3 : AddCommGroup α] [inst_4 : PartialOrder α] [IsOrderedAddMonoid α] [inst_6 : Module K α]
  [IsStrictOrderedModule K α], t < s → ∀ {a : α}, 0 ≤ a → t • a ≤ s • a
-- Mathlib.SetTheory.Cardinal.Regular
Cardinal.lt_aleph0_or_isRegular_or_isSingular : ∀ {c : Cardinal.{u_1}}, c < Cardinal.aleph0 ∨ c.IsRegular ∨ c.IsSingular
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
/-- The constant map is alternating when `ι` is empty.  -/
ContinuousAlternatingMap.constOfIsEmpty : (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] → [IsEmpty ι] → N → M [⋀^ι]→L[R] N
-- Mathlib.CategoryTheory.Monad.Algebra
CategoryTheory.Monad.Algebra.comp_eq_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {A A' A'' : T.Algebra}
  (f : A ⟶ A') (g : A' ⟶ A''), CategoryTheory.Monad.Algebra.Hom.comp f g = CategoryTheory.CategoryStruct.comp f g
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.NumDenSameDeg.num_one : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubmonoidClass σ A] {𝒜 : ι → σ} (x : Submonoid A) [inst_3 : AddCommMonoid ι] [inst_4 : DecidableEq ι]
  [inst_5 : GradedRing 𝒜], ↑(HomogeneousLocalization.NumDenSameDeg.num 1) = 1
-- Mathlib.Order.Filter.Partial
Filter.mem_rmap : ∀ {α : Type u} {β : Type v} (r : SetRel α β) (l : Filter α) (s : Set β), s ∈ Filter.rmap r l ↔ r.core s ∈ l
-- Lean.Parser.Basic
Lean.Parser.manyAux : Lean.Parser.ParserFn → Lean.Parser.ParserFn
-- Mathlib.GroupTheory.Nilpotent
/-- **Alias** of `Subgroup.lowerCentralSeries_pi_le`. -/
lowerCentralSeries_pi_le : ∀ {η : Type u_2} {Gs : η → Type u_3} [inst : (i : η) → Group (Gs i)] (Ss : (i : η) → Subgroup (Gs i)) (n : ℕ),
  (Subgroup.pi Set.univ Ss).lowerCentralSeries n ≤ Subgroup.pi Set.univ fun i => (Ss i).lowerCentralSeries n
-- Batteries.Tactic.Case
/-- Implementation for `case` and `case'`.  -/
Batteries.Tactic.evalCase : Bool →
  Lean.Syntax →
    Array (Lean.TSyntax `Lean.binderIdent) →
      Array (Lean.TSyntaxArray `Lean.binderIdent) →
        Array (Option Lean.Term) → Lean.TSyntax `Batteries.Tactic.casePattTac → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
/-- Constructor for cocycles to `mappingCocone`.  -/
CochainComplex.mappingCocone.liftCocycle : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {K L : CochainComplex C ℤ} →
        (φ : K ⟶ L) →
          [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] →
            {M : CochainComplex C ℤ} →
              {n m : ℤ} →
                (α : CochainComplex.HomComplex.Cocycle M K n) →
                  (β : CochainComplex.HomComplex.Cochain M L m) →
                    m + 1 = n →
                      CochainComplex.HomComplex.δ m n β + (↑α).comp (CochainComplex.HomComplex.Cochain.ofHom φ) ⋯ = 0 →
                        CochainComplex.HomComplex.Cocycle M (CochainComplex.mappingCocone φ) n
-- Init.Data.Nat.Basic
_private.Init.Data.Nat.Basic.0.Nat.repeat.match_1.eq_1 : ∀ {α : Type u_2} (motive : ℕ → α → Sort u_1) (a : α) (h_1 : (a : α) → motive 0 a)
  (h_2 : (n : ℕ) → (a : α) → motive n.succ a),
  (match 0, a with
    | 0, a => h_1 a
    | n.succ, a => h_2 n a) =
    h_1 a
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
/-- Given `f` a multilinear map, then the derivative of `x ↦ f (g₁ x, ..., gₙ x)` at `x` applied
to a vector `v` is given by `∑ i, f (g₁ x, ..., g'ᵢ v, ..., gₙ x)`.  -/
HasFDerivAt.multilinear_comp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {ι : Type u_2} {E : ι → Type u_3} [inst_3 : (i : ι) → NormedAddCommGroup (E i)]
  [inst_4 : (i : ι) → NormedSpace 𝕜 (E i)] [inst_5 : Fintype ι] (f : ContinuousMultilinearMap 𝕜 E F)
  [inst_6 : DecidableEq ι] {G : Type u_4} [inst_7 : NormedAddCommGroup G] [inst_8 : NormedSpace 𝕜 G]
  {g : (i : ι) → G → E i} {g' : (i : ι) → G →L[𝕜] E i} {x : G},
  (∀ (i : ι), HasFDerivAt (g i) (g' i) x) →
    HasFDerivAt (fun x => f fun i => g i x) (∑ i, f.toContinuousLinearMap (fun j => g j x) i ∘SL g' i) x
-- Mathlib.CategoryTheory.Bicategory.InducedBicategory
CategoryTheory.Bicategory.InducedBicategory.bicategory_rightUnitor_hom_hom : ∀ {B : Type u_1} {C : Type u_2} [inst : CategoryTheory.Bicategory C] {F : B → C}
  {a b : CategoryTheory.Bicategory.InducedBicategory C F} (x : a ⟶ b),
  (CategoryTheory.Bicategory.rightUnitor x).hom.hom = (CategoryTheory.Bicategory.rightUnitor x.hom).hom
-- Mathlib.LinearAlgebra.RootSystem.RootPositive
RootPairing.RootPositiveForm.toInvariantForm.congr_simp : ∀ {ι : Type u_1} {R : Type u_2} {S : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing S]
  [inst_1 : LinearOrder S] [inst_2 : CommRing R] [inst_3 : Algebra S R] [inst_4 : AddCommGroup M] [inst_5 : Module R M]
  [inst_6 : AddCommGroup N] [inst_7 : Module R N] {P : RootPairing ι R M N} [inst_8 : P.IsValuedIn S]
  (B B_1 : RootPairing.RootPositiveForm S P),
  B = B_1 → ∀ [inst_9 : FaithfulSMul S R], B.toInvariantForm = B_1.toInvariantForm
-- Std.Time.Date.Unit.Year
/-- The era before the Common Era (BCE), always represents a date before year 0.  -/
Std.Time.Year.Era.bce : Std.Time.Year.Era
-- Mathlib.CategoryTheory.Category.RelCat
/-- A type synonym for `Type u`, which carries the category instance for which
morphisms are binary relations.  -/
CategoryTheory.RelCat : Type (u + 1)
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
AlgebraicGeometry.quasiSeparated_isStableUnderBaseChange : CategoryTheory.MorphismProperty.IsStableUnderBaseChange @AlgebraicGeometry.QuasiSeparated
-- Mathlib.GroupTheory.Nilpotent
Subgroup.lowerCentralSeries_eq_bot_iff_upperCentralSeries_eq_top : ∀ {G : Type u_1} [inst : Group G] {n : ℕ}, ⊤.lowerCentralSeries n = ⊥ ↔ Subgroup.upperCentralSeries G n = ⊤
-- Mathlib.Topology.Algebra.ConstMulAction
ContinuousWithinAt.const_vadd : ∀ {M : Type u_1} {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : VAdd M α] [ContinuousConstVAdd M α]
  [inst_3 : TopologicalSpace β] {g : β → α} {b : β} {s : Set β},
  ContinuousWithinAt g s b → ∀ (c : M), ContinuousWithinAt (c +ᵥ g) s b
-- Mathlib.Data.List.Nodup
List.Nodup.pairwise_of_forall_ne : ∀ {α : Type u} {l : List α} {r : α → α → Prop}, l.Nodup → (∀ a ∈ l, ∀ b ∈ l, a ≠ b → r a b) → List.Pairwise r l
-- Mathlib.LinearAlgebra.Eigenspace.Zero
LinearMap.hasEigenvalue_zero_tfae : ∀ {K : Type u_2} {M : Type u_3} [inst : Field K] [inst_1 : AddCommGroup M] [inst_2 : Module K M]
  [inst_3 : Module.Finite K M] (φ : Module.End K M),
  [φ.HasEigenvalue 0, (minpoly K φ).IsRoot 0, Polynomial.constantCoeff (LinearMap.charpoly φ) = 0, LinearMap.det φ = 0,
      ⊥ < LinearMap.ker φ, ∃ m, m ≠ 0 ∧ φ m = 0].TFAE
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rcc.forIn'_eq_forIn'_toList : ∀ {α : Type u} {r : Std.Rcc α} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerableLE α] [inst_4 : Std.Rxc.IsAlwaysFinite α]
  [inst_5 : Std.PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [inst_6 : Monad m]
  [LawfulMonad m] {f : (a : α) → a ∈ r → γ → m (ForInStep γ)},
  forIn' r init f = forIn' r.toList init fun a ha acc => f a ⋯ acc
-- Init.Omega.IntList
Lean.Omega.IntList.mul_distrib_left : ∀ (xs ys zs : Lean.Omega.IntList), (xs + ys) * zs = xs * zs + ys * zs
-- Init.Data.Array.Lemmas
Array.sum_push : ∀ {α : Type u_1} [inst : Add α] [inst_1 : Zero α] [Std.Associative fun x1 x2 => x1 + x2]
  [Std.LawfulIdentity (fun x1 x2 => x1 + x2) 0] {xs : Array α} {x : α}, (xs.push x).sum = xs.sum + x
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.setIntegral_nonpos_le : ∀ {X : Type u_1} {mX : MeasurableSpace X} {μ : MeasureTheory.Measure X} {f : X → ℝ} {s : Set X},
  MeasurableSet s →
    MeasureTheory.StronglyMeasurable f →
      MeasureTheory.Integrable f μ → ∫ (x : X) in {y | f y ≤ 0}, f x ∂μ ≤ ∫ (x : X) in s, f x ∂μ
-- Mathlib.Analysis.Normed.Affine.Simplex
/-- A simplex is equilateral if all the edge lengths are equal.  -/
Affine.Simplex.Equilateral : {R : Type u_1} →
  {V : Type u_2} →
    {P : Type u_3} →
      [inst : Ring R] →
        [inst_1 : SeminormedAddCommGroup V] →
          [inst_2 : PseudoMetricSpace P] →
            [inst_3 : Module R V] → [inst_4 : NormedAddTorsor V P] → {n : ℕ} → Affine.Simplex R P n → Prop
-- Init.Data.Range.Lemmas
_private.Init.Data.Range.Lemmas.0.Std.Legacy.Range.forIn'.loop.match_1.eq_2 : ∀ {β : Type u_1} (motive : ForInStep β → Sort u_2) (b : β) (h_1 : (b : β) → motive (ForInStep.done b))
  (h_2 : (b : β) → motive (ForInStep.yield b)),
  (match ForInStep.yield b with
    | ForInStep.done b => h_1 b
    | ForInStep.yield b => h_2 b) =
    h_2 b
-- Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
Profinite.NobelingProof.Products.lt_nil_empty : ∀ {I : Type u_1} [inst : LinearOrder I], {m | m < Profinite.NobelingProof.Products.nil} = ∅
-- Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
CategoryTheory.MorphismProperty.IsCardinalForSmallObjectArgument.isSmall : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {I : CategoryTheory.MorphismProperty C} (κ : Cardinal.{w})
  {inst_1 : Fact κ.IsRegular} {inst_2 : OrderBot κ.ord.ToType} [self : I.IsCardinalForSmallObjectArgument κ],
  CategoryTheory.MorphismProperty.IsSmall.{w, v, u} I
-- Mathlib.CategoryTheory.Abelian.Injective.Extend
CategoryTheory.InjectiveResolution.Hom.hom'_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X : C}
  {R : CategoryTheory.InjectiveResolution X} {X' : C} {R' : CategoryTheory.InjectiveResolution X'} {f : X ⟶ X'}
  (φ : R.Hom R' f) (n : ℤ) (m : ℕ) (h : ↑m = n),
  φ.hom'.f n =
    CategoryTheory.CategoryStruct.comp (R.cochainComplexXIso n m h).hom
      (CategoryTheory.CategoryStruct.comp (φ.hom.f m) (R'.cochainComplexXIso n m h).inv)
-- Mathlib.Combinatorics.Quiver.Prefunctor
/-- The identity morphism between quivers.  -/
Prefunctor.id : (V : Type u_1) → [inst : Quiver V] → V ⥤q V
-- Mathlib.Geometry.Manifold.Diffeomorph
ContinuousLinearEquiv.contMDiffWithinAt_transContinuousLinearEquiv_left : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {F : Type u_4}
  [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜 F] {H : Type u_5} [inst_7 : TopologicalSpace H]
  {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'}
  {M : Type u_9} [inst_9 : TopologicalSpace M] [inst_10 : ChartedSpace H M] {M' : Type u_10}
  [inst_11 : TopologicalSpace M'] [inst_12 : ChartedSpace H' M'] {n : WithTop ℕ∞} (e : E ≃L[𝕜] F) {f : M → M'} {x : M}
  {s : Set M}, ContMDiffWithinAt (I.transContinuousLinearEquiv e) I' n f s x ↔ ContMDiffWithinAt I I' n f s x
-- Mathlib.Order.Filter.SmallSets
Filter.frequently_smallSets' : ∀ {α : Type u_4} {l : Filter α} {p : Set α → Prop},
  (∀ ⦃s t : Set α⦄, s ⊆ t → p s → p t) → ((∃ᶠ (s : Set α) in l.smallSets, p s) ↔ ∀ t ∈ l, p t)
-- Mathlib.RingTheory.Kaehler.Basic
KaehlerDifferential.D_tensorProductTo : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (x : ↥(KaehlerDifferential.ideal R S)),
  (KaehlerDifferential.D R S).tensorProductTo ↑x = (KaehlerDifferential.ideal R S).toCotangent x
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.eq_empty_iff_forall_not_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t = ∅ ↔ ∀ (a : α), a ∉ t