mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Filter.CountablyGenerated
Filter.CountableFilterBasis.mk.injEq : ∀ {α : Type u_6} (toFilterBasis : FilterBasis α) (countable : toFilterBasis.sets.Countable)
  (toFilterBasis_1 : FilterBasis α) (countable_1 : toFilterBasis_1.sets.Countable),
  ({ toFilterBasis := toFilterBasis, countable := countable } =
      { toFilterBasis := toFilterBasis_1, countable := countable_1 }) =
    (toFilterBasis = toFilterBasis_1)
-- Mathlib.Data.Finset.Disjoint
Finset.disjoint_coe : ∀ {α : Type u_2} {s t : Finset α}, Disjoint ↑s ↑t ↔ Disjoint s t
-- Mathlib.Order.Defs.PartialOrder
PartialOrder.le_antisymm : ∀ {α : Type u_2} [self : PartialOrder α] (a b : α), a ≤ b → b ≤ a → a = b
-- Mathlib.Data.List.Chain
List.isChain_pmap : ∀ {α : Type u_1} {β : Type u_2} {S : β → β → Prop} {p : α → Prop} (f : (a : α) → p a → β) {l : List α}
  (hl : ∀ a ∈ l, p a),
  List.IsChain S (List.pmap f l hl) ↔ List.IsChain (fun a b => ∃ (ha : p a) (hb : p b), S (f a ha) (f b hb)) l
-- Mathlib.Algebra.Category.Semigrp.Basic
/-- Build an isomorphism in the category
`AddSemigroup` from an `AddEquiv` between `AddSemigroup`s.  -/
AddEquiv.toAddSemigrpIso : {X Y : Type u} → [inst : AddSemigroup X] → [inst_1 : AddSemigroup Y] → X ≃+ Y → (AddSemigrp.of X ≅ AddSemigrp.of Y)
-- Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
AddChar.zmodAddEquiv_apply : ∀ {n : ℕ} [inst : NeZero n] (x : ZMod n), AddChar.zmodAddEquiv x = AddChar.circleEquivComplex (AddChar.zmod n x)
-- Mathlib.Topology.Order.LeftRightLim
continuousWithinAt_rightLim_Ici : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace β] [inst_2 : TopologicalSpace α]
  [OrderTopology α] [T3Space β] {f : α → β} {a : α},
  Filter.Tendsto f (nhdsWithin a (Set.Ioi a)) (nhds (Function.rightLim f a)) →
    ContinuousWithinAt (Function.rightLim f) (Set.Ici a) a
-- Mathlib.RingTheory.UniqueFactorizationDomain.GCDMonoid
instIsGCDMonoidOfUniqueFactorizationMonoid : ∀ (α : Type u_2) [inst : CommMonoidWithZero α] [UniqueFactorizationMonoid α], IsGCDMonoid α
-- Mathlib.Combinatorics.SimpleGraph.Metric
SimpleGraph.Adj.diff_dist_adj : ∀ {V : Type u_1} {G : SimpleGraph V} {u v w : V},
  G.Adj v w → G.dist u w = G.dist u v ∨ G.dist u w = G.dist u v + 1 ∨ G.dist u w = G.dist u v - 1
-- Mathlib.Algebra.Group.Pi.Lemmas
Set.piecewise_sub : ∀ {I : Type u} {f : I → Type v} [inst : (i : I) → Sub (f i)] (s : Set I) [inst_1 : (i : I) → Decidable (i ∈ s)]
  (f₁ f₂ g₁ g₂ : (i : I) → f i), s.piecewise (f₁ - f₂) (g₁ - g₂) = s.piecewise f₁ g₁ - s.piecewise f₂ g₂
-- Mathlib.Topology.Semicontinuity.Basic
lowerSemicontinuousOn_iff_isClosed_epigraph : ∀ {α : Type u_1} [inst : TopologicalSpace α] {γ : Type u_4} [inst_1 : LinearOrder γ] [inst_2 : TopologicalSpace γ]
  [ClosedIciTopology γ] {f : α → γ} {s : Set α},
  IsClosed s → (LowerSemicontinuousOn f s ↔ IsClosed {p | p.1 ∈ s ∧ f p.1 ≤ p.2})
-- Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
MeasureTheory.lintegral_norm_eq_lintegral_edist : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  (f : α → β), ∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ = ∫⁻ (a : α), edist (f a) 0 ∂μ
-- Mathlib.Algebra.Category.Ring.Under.Limits
/-- Variant of `Under.equalizerForkIsLimit` for algebra maps.  -/
CommRingCat.Under.equalizerFork'IsLimit : {R : CommRingCat} →
  {A B : Type u} →
    [inst : CommRing A] →
      [inst_1 : CommRing B] →
        [inst_2 : Algebra (↑R) A] →
          [inst_3 : Algebra (↑R) B] →
            (f g : A →ₐ[↑R] B) → CategoryTheory.Limits.IsLimit (CommRingCat.Under.equalizerFork' f g)
-- Mathlib.GroupTheory.Coset.Basic
/-- Given a subgroup `s`, the function that sends a subgroup `t` to the pair consisting of
its intersection with `s` and its image in the quotient `α ⧸ s` is strictly monotone, even though
it is not injective in general.  -/
QuotientGroup.strictMono_comap_prod_image : ∀ {α : Type u_1} [inst : Group α] (s : Subgroup α),
  StrictMono fun t => (Subgroup.comap s.subtype t, QuotientGroup.mk '' ↑t)
-- Mathlib.Algebra.Order.Group.Nat
Nat.instIsOrderedCancelAddMonoid : IsOrderedCancelAddMonoid ℕ
-- Batteries.Data.List.Lemmas
List.foldrIdx_const : ∀ {α : Type u_1} {xs : List α} {α_1 : Type u_2} {f : α → α_1 → α_1} {i : α_1} {s : ℕ},
  List.foldrIdx (Function.const ℕ f) i xs s = List.foldr f i xs
-- Mathlib.Analysis.Convex.Strict
strictConvex_uIoc : ∀ {𝕜 : Type u_1} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : TopologicalSpace β]
  [inst_3 : AddCommMonoid β] [inst_4 : LinearOrder β] [IsOrderedCancelAddMonoid β] [OrderTopology β]
  [inst_7 : Module 𝕜 β] [PosSMulStrictMono 𝕜 β] (r s : β), StrictConvex 𝕜 (Set.uIoc r s)
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKeyD_filter_key : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {f : α → Bool} {k fallback : α},
  (Std.HashMap.filter (fun k x => f k) m).getKeyD k fallback = (Option.filter f (m.getKey? k)).getD fallback
-- Mathlib.Topology.MetricSpace.Pseudo.Basic
Topology.IsEmbedding.isSeparable_preimage : ∀ {β : Type v} {α : Type u_2} [inst : TopologicalSpace α] [TopologicalSpace.PseudoMetrizableSpace α] {f : β → α}
  [inst_2 : TopologicalSpace β],
  Topology.IsEmbedding f → ∀ {s : Set α}, TopologicalSpace.IsSeparable s → TopologicalSpace.IsSeparable (f ⁻¹' s)
-- Std.Time.Date.PlainDate
/-- Adds a given number of weeks to a `PlainDate`.
 -/
Std.Time.PlainDate.addWeeks : Std.Time.PlainDate → Std.Time.Week.Offset → Std.Time.PlainDate
-- Lean.Meta.Tactic.Grind.Types
_private.Lean.Meta.Tactic.Grind.Types.0.Lean.Meta.Grind.incCounter : {α : Type u_1} → [inst : Hashable α] → [inst_1 : BEq α] → Lean.PHashMap α ℕ → α → Lean.PHashMap α ℕ
-- Mathlib.Algebra.Module.LocalizedModule.Basic
_private.Mathlib.Algebra.Module.LocalizedModule.Basic.0.LocalizedModule.mul_smul_aux : ∀ {R : Type u} [inst : CommSemiring R] {S : Submonoid R} {M : Type v} [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {T : Type u_1} [inst_3 : CommSemiring T] [inst_4 : Algebra R T] [inst_5 : IsLocalization S T] (x y : T)
  (p : LocalizedModule S M), (x * y) • p = x • y • p
-- Mathlib.Data.Finset.Sum
Finset.empty_disjSum : ∀ {α : Type u_1} {β : Type u_2} (t : Finset β), ∅.disjSum t = Finset.map Function.Embedding.inr t
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.degree_le_zero_iff : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.degree ≤ 0 ↔ p = Polynomial.C (p.coeff 0)
-- Mathlib.RingTheory.Invariant.Basic
/-- The stabilizer subgroup of `Q` surjects onto `Aut(Frac(B/Q)/Frac(A/P))`.  -/
IsFractionRing.stabilizerHom_surjective : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] (G : Type u_3)
  [inst_3 : Group G] [Finite G] [inst_5 : MulSemiringAction G B] [inst_6 : SMulCommClass G A B] (P : Ideal A)
  (Q : Ideal B) [Q.IsPrime] [inst_8 : Q.LiesOver P] (K : Type u_4) (L : Type u_5) [inst_9 : Field K] [inst_10 : Field L]
  [inst_11 : Algebra (A ⧸ P) K] [inst_12 : Algebra (B ⧸ Q) L] [inst_13 : Algebra (A ⧸ P) L]
  [inst_14 : IsScalarTower (A ⧸ P) (B ⧸ Q) L] [inst_15 : Algebra K L] [inst_16 : IsScalarTower (A ⧸ P) K L]
  [Algebra.IsInvariant A B G] [inst_18 : IsFractionRing (A ⧸ P) K] [inst_19 : IsFractionRing (B ⧸ Q) L],
  Function.Surjective ⇑(IsFractionRing.stabilizerHom G P Q K L)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.mem_of_getKey?_eq_some : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k k' : α},
  t.getKey? k = some k' → k' ∈ t
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.one : One Ordinal.{u_1}
-- Mathlib.Data.Vector3
_private.Mathlib.Data.Vector3.0.Fin2.toNat.match_1.splitter : (motive : (x : ℕ) → Fin2 x → Sort u_1) →
  (x : ℕ) →
    (x_1 : Fin2 x) → ((n : ℕ) → motive (n + 1) Fin2.fz) → ((n : ℕ) → (i : Fin2 n) → motive (n + 1) i.fs) → motive x x_1
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
SheafOfModules.GeneratingSections.localGeneratorsData_X : ∀ {C : Type u'} [inst : CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : CategoryTheory.HasWeakSheafify J AddCommGrpCat]
  [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat]
  [inst_3 : ∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat]
  [inst_4 : CategoryTheory.Limits.HasBinaryProducts C]
  [inst_5 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R}
  (G : M.GeneratingSections) (a : C), G.localGeneratorsData.X a = id a
-- Mathlib.Computability.RegularExpressions
RegularExpression.deriv.eq_2 : ∀ {α : Type u_1} [inst : DecidableEq α] (x : α), RegularExpression.epsilon.deriv x = 0
-- Lean.Meta.Tactic.Grind.Types
/-- Returns the root element in the equivalence class of `e`.  -/
Lean.Meta.Grind.Goal.getRoot : Lean.Meta.Grind.Goal → Lean.Expr → Lean.MetaM Lean.Expr
-- Lean.Parser.Do
Lean.Parser.Term.doForDecl : Lean.Parser.Parser
-- Mathlib.CategoryTheory.Simple
/-- A nonzero epimorphism from a simple object is an isomorphism.  -/
CategoryTheory.isIso_of_epi_of_nonzero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X Y : C}
  [CategoryTheory.Simple X] {f : X ⟶ Y} [CategoryTheory.Epi f], f ≠ 0 → CategoryTheory.IsIso f
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.extensionProduct_le_of_isTriangulatedClosed₂' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  {P₁ P₂ Q : CategoryTheory.ObjectProperty C} [Q.IsTriangulatedClosed₂],
  P₁ ≤ Q → P₂ ≤ Q → P₁.extensionProduct P₂ ≤ Q.isoClosure
-- Mathlib.Algebra.Polynomial.Sequence
/-- The first `m` polynomials of a polynomial sequence span all polynomials of degree `< m` if their
leading coefficients are units.  -/
Polynomial.Sequence.span_degreeLT : ∀ {R : Type u_1} [inst : Ring R] (S : Polynomial.Sequence R) {m : ℕ},
  (∀ i < m, IsUnit (↑S i).leadingCoeff) → Submodule.span R (↑S '' Set.Iio m) = Polynomial.degreeLT R m
-- Mathlib.RingTheory.Coalgebra.Hom
CoalgHom.comp_id : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : AddCommMonoid B] [inst_4 : Module R B] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B]
  (φ : A →ₗc[R] B), φ.comp (CoalgHom.id R A) = φ
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
tsum_dite_left : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {L : SummationFilter β}
  (P : Prop) [inst_2 : Decidable P] (x : β → P → α),
  (∑'[L] (b : β), if h : P then x b h else 0) = if h : P then ∑'[L] (b : β), x b h else 0
-- Mathlib.CategoryTheory.Limits.Indization.Category
CategoryTheory.instCreatesColimitsOfShapeIndFunctorOppositeTypeInclusionOfIsFiltered : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type v} →
      [inst_1 : CategoryTheory.SmallCategory J] →
        [CategoryTheory.IsFiltered J] → CategoryTheory.CreatesColimitsOfShape J (CategoryTheory.Ind.inclusion C)
-- Init.Data.SInt.Lemmas
Int16.toUInt16_le : ∀ {a b : Int16}, 0 ≤ a → a ≤ b → a.toUInt16 ≤ b.toUInt16
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.skeletalFunctor_obj : ∀ (a : SimplexCategory), SimplexCategory.skeletalFunctor.obj a = NonemptyFinLinOrd.of (Fin (a.len + 1))
-- Mathlib.Data.Matrix.ColumnRowPartitioned
/-- Given a column partitioned matrix extract the second column  -/
Matrix.toCols₂ : {R : Type u_1} → {m : Type u_2} → {n₁ : Type u_6} → {n₂ : Type u_7} → Matrix m (n₁ ⊕ n₂) R → Matrix m n₂ R
-- Mathlib.Algebra.Order.Floor.Ring
Int.fract_div_mul_self_mem_Ico : ∀ {k : Type u_4} [inst : Field k] [inst_1 : LinearOrder k] [IsOrderedRing k] [inst_3 : FloorRing k] (a b : k),
  0 < a → Int.fract (b / a) * a ∈ Set.Ico 0 a
-- Std.Internal.Do.PredTrans
/-- Partial order on predicate transformers, inherited from the function space.  -/
Std.Internal.Do.instPartialOrderPredTrans : {Pred : Type u_1} →
  {EPred : Type u_2} →
    {α : Type u_3} → [Lean.Order.PartialOrder Pred] → Lean.Order.PartialOrder (Std.Internal.Do.PredTrans Pred EPred α)
-- Mathlib.Algebra.Homology.ShortComplex.Homology
/-- a left homology map data  -/
CategoryTheory.ShortComplex.HomologyMapData.left : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        {φ : S₁ ⟶ S₂} →
          {h₁ : S₁.HomologyData} →
            {h₂ : S₂.HomologyData} →
              CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂ →
                CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁.left h₂.left
-- Mathlib.Algebra.Lie.Cochain
/-- Lie algebra 2-cochains over `L` with coefficients in the module `M`.  -/
LieModule.Cohomology.twoCochain : (R : Type u_1) →
  [inst : CommRing R] →
    (L : Type u_2) →
      [inst_1 : LieRing L] →
        [inst_2 : LieAlgebra R L] →
          (M : Type u_3) → [inst_3 : AddCommGroup M] → [inst_4 : Module R M] → Submodule R (L →ₗ[R] L →ₗ[R] M)
-- Std.Http.Data.Status
Std.Http.Status.failedDependency.sizeOf_spec : sizeOf Std.Http.Status.failedDependency = 1
-- Mathlib.Data.List.Lattice
List.bagInter.eq_2 : ∀ {α : Type u_1} [inst : BEq α] (x : List α), (x = [] → False) → x.bagInter [] = []
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMulEquiv.instEquivLike.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace N] [inst_2 : Mul M]
  [inst_3 : Mul N],
  ContinuousMulEquiv.instEquivLike =
    { coe := fun f => f.toFun, inv := fun f => f.invFun, left_inv := ⋯, right_inv := ⋯, coe_injective' := ⋯ }
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousAlternatingMap.pi_apply : ∀ {R : Type u_1} {M : Type u_2} {ι : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : TopologicalSpace M] {ι' : Type u_7} {M' : ι' → Type u_8} [inst_4 : (i : ι') → AddCommMonoid (M' i)]
  [inst_5 : (i : ι') → TopologicalSpace (M' i)] [inst_6 : (i : ι') → Module R (M' i)] (f : (i : ι') → M [⋀^ι]→L[R] M' i)
  (m : ι → M) (j : ι'), (ContinuousAlternatingMap.pi f) m j = (f j) m
-- Init.Data.Slice.Array.Basic
instSliceableArrayNatSubarray_4 : {α : Type u} → Std.Roo.Sliceable (Array α) ℕ (Subarray α)
-- Mathlib.CategoryTheory.Sums.Products
/-- Composing the backward direction of `functorEquiv` with the second projection is the same as
precomposition with `inr_ A A'`.  -/
CategoryTheory.Sum.functorEquivInverseCompWhiskeringLeftInrIso : {A : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} A] →
    {A' : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} A'] →
        {B : Type u} →
          [inst_2 : CategoryTheory.Category.{v, u} B] →
            (CategoryTheory.Sum.functorEquiv A A' B).inverse.comp
                ((CategoryTheory.Functor.whiskeringLeft A' (A ⊕ A') B).obj (CategoryTheory.Sum.inr_ A A')) ≅
              CategoryTheory.Prod.snd (CategoryTheory.Functor A B) (CategoryTheory.Functor A' B)
-- Mathlib.Combinatorics.SimpleGraph.Trails
SimpleGraph.Walk.IsEulerian.card_odd_degree : ∀ {V : Type u_1} {G : SimpleGraph V} [inst : DecidableEq V] [inst_1 : Fintype V] [inst_2 : DecidableRel G.Adj] {u v : V}
  {p : G.Walk u v}, p.IsEulerian → Fintype.card ↑{v | Odd (G.degree v)} = 0 ∨ Fintype.card ↑{v | Odd (G.degree v)} = 2
-- Lean.Elab.PreDefinition.WF.GuessLex
Lean.Elab.WF.GuessLex.explainFailure : Array Lean.Name →
  Array (Array Lean.Elab.WF.GuessLex.BasicMeasure) → Array Lean.Elab.WF.GuessLex.RecCallCache → Lean.MetaM Std.Format
-- Mathlib.Order.Partition.Basic
Partition.ne_bot_of_mem : ∀ {α : Type u_1} {s x : α} [inst : CompleteLattice α] {P : Partition s}, x ∈ P → x ≠ ⊥
-- Lean.Meta.Tactic.Grind.ProveEq
_private.Lean.Meta.Tactic.Grind.ProveEq.0.Lean.Meta.Grind.AbstractM.State.mk.sizeOf_spec : ∀ (cache : Std.HashMap (Lean.Expr × Lean.Expr) Lean.Expr) (varTypes lhss rhss : Array Lean.Expr),
  sizeOf { cache := cache, varTypes := varTypes, lhss := lhss, rhss := rhss } =
    1 + sizeOf cache + sizeOf varTypes + sizeOf lhss + sizeOf rhss
-- Init.System.IO
instInhabitedEIO : {ε α : Type} → [Inhabited ε] → Inhabited (EIO ε α)
-- Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage
Dynamics.dynEntourage_comp_subset : ∀ {X : Type u_1} (T : X → X) (U V : SetRel X X) (n : ℕ),
  (Dynamics.dynEntourage T U n).comp (Dynamics.dynEntourage T V n) ⊆ Dynamics.dynEntourage T (U.comp V) n
-- Lean.Level
Lean.PersistentLevelMap : Type → Type
-- Batteries.Data.Fin.Lemmas
Fin.exists_eq_true_of_isSome_find? : ∀ {n : ℕ} {p : Fin n → Bool}, (Fin.find? p).isSome = true → ∃ i, p i = true
-- Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
integral_mul_cexp_neg_mul_sq : ∀ {b : ℂ}, 0 < b.re → ∫ (r : ℝ) in Set.Ioi 0, ↑r * Complex.exp (-b * ↑r ^ 2) = (2 * b)⁻¹
-- Mathlib.CategoryTheory.Preadditive.Opposite
/-- `unop` induces morphisms of monoids on hom groups of a preadditive category  -/
CategoryTheory.unopHom : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] → (X Y : Cᵒᵖ) → (X ⟶ Y) →+ (Opposite.unop Y ⟶ Opposite.unop X)
-- Init.Data.Vector.Lemmas
Vector.back_replicate : ∀ {n : ℕ} {α : Type u_1} {a : α} [inst : NeZero n], (Vector.replicate n a).back = a
-- Mathlib.Order.Filter.Ultrafilter.Defs
Ultrafilter.instNonempty : ∀ {α : Type u} [Nonempty α], Nonempty (Ultrafilter α)
-- Mathlib.CategoryTheory.CatCommSq
/-- In a square of categories, when the left and right functors are part
of equivalence of categories, it is equivalent to show 2-commutativity for
the functors of these equivalences or for their inverses.  -/
CategoryTheory.CatCommSq.vInvEquiv : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {C₃ : Type u_3} →
      {C₄ : Type u_4} →
        [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
          [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
            [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] →
              [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄] →
                (T : CategoryTheory.Functor C₁ C₂) →
                  (L : C₁ ≌ C₃) →
                    (R : C₂ ≌ C₄) →
                      (B : CategoryTheory.Functor C₃ C₄) →
                        CategoryTheory.CatCommSq T L.functor R.functor B ≃
                          CategoryTheory.CatCommSq B L.inverse R.inverse T
-- Mathlib.Order.Filter.CountableInter
/-- `Filter.CountableGenerateSets g` is the (sets of the)
greatest `countableInterFilter` containing `g`.  -/
Filter.CountableGenerateSets : {α : Type u_2} → Set (Set α) → Set α → Prop
-- Mathlib.Dynamics.PeriodicPts.Defs
Function.periodicOrbit_eq_nil_iff_not_periodic_pt : ∀ {α : Type u_1} {f : α → α} {x : α}, Function.periodicOrbit f x = Cycle.nil ↔ x ∉ Function.periodicPts f
-- Mathlib.Order.RelIso.Basic
Equiv.sumEmpty.congr_simp : ∀ (α : Type u_9) (β : Type u_10) [inst : IsEmpty β], Equiv.sumEmpty α β = Equiv.sumEmpty α β
-- Mathlib.LinearAlgebra.Eigenspace.Matrix
/-- Eigenvalues of a diagonal linear operator are the diagonal entries.  -/
hasEigenvalue_toLin_diagonal_iff : ∀ {R : Type u_1} {n : Type u_2} {M : Type u_3} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : CommRing R]
  [Nontrivial R] [inst_4 : AddCommGroup M] [inst_5 : Module R M] (d : n → R) {μ : R} [IsDomain R]
  [Module.IsTorsionFree R M] (b : Module.Basis n R M),
  Module.End.HasEigenvalue ((Matrix.toLin b b) (Matrix.diagonal d)) μ ↔ ∃ i, d i = μ
-- Mathlib.CategoryTheory.Functor.Const
/-- If `J` is nonempty, then the constant functor over `J` is faithful.  -/
CategoryTheory.Functor.instFaithfulConstOfNonempty : ∀ (J : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} C]
  [Nonempty J], (CategoryTheory.Functor.const J).Faithful
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfc_eq_cfc_iff_eqOn : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A] [inst_6 : Ring A]
  [inst_7 : StarRing A] [inst_8 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] {f g : R → R} {a : A},
  autoParam (p a) _auto_234✝ →
    autoParam (ContinuousOn f (spectrum R a)) _auto_236✝ →
      autoParam (ContinuousOn g (spectrum R a)) _auto_238✝ → (cfc f a = cfc g a ↔ Set.EqOn f g (spectrum R a))
-- Mathlib.RingTheory.Finiteness.Basic
Submodule.fg_sup_span_induction : ∀ {R : Type u_4} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {motive : (N : Submodule R M) → N.FG → Prop},
  motive ⊥ ⋯ →
    (∀ (N : Submodule R M) (x : M) (hN : N.FG), motive N hN → motive (N ⊔ R ∙ x) ⋯) →
      ∀ (N : Submodule R M) (hN : N.FG), motive N hN
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.associator_naturality_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y : C)
  {Z Z' : C} (f : Z ⟶ Z'),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) f)
      (CategoryTheory.MonoidalCategoryStruct.associator X Y Z').hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y f))
-- Mathlib.Data.Finsupp.Weight
Finsupp.weight_sub_single_add : ∀ {σ : Type u_1} {M : Type u_2} {w : σ → M} [inst : AddCommMonoid M] {f : σ →₀ ℕ} {i : σ},
  f i ≠ 0 → (Finsupp.weight w) (f - fun₀ | i => 1) + w i = (Finsupp.weight w) f
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.insertManyIfNewUnit_cons : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α Unit cmp} [inst : Std.TransCmp cmp] {l : List α} {k : α},
  t.insertManyIfNewUnit (k :: l) = (t.insertIfNew k ()).insertManyIfNewUnit l
-- Lean.DocString.Extension
Lean.getMainModuleDoc : Lean.Environment → Lean.PersistentArray Lean.ModuleDoc
-- Mathlib.Order.Concept
Concept.intent_min : ∀ {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (c d : Concept α β r),
  (c ⊓ d).intent = upperPolar r (c.extent ∩ d.extent)
-- Mathlib.CategoryTheory.Dialectica.Basic
/-- The source object  -/
CategoryTheory.Dial.src : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasFiniteProducts C] → CategoryTheory.Dial C → C
-- Mathlib.Algebra.Lie.Nilpotent
LieModule.lowerCentralSeriesLast.eq_1 : ∀ (R : Type u) (L : Type v) (M : Type w) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M],
  LieModule.lowerCentralSeriesLast R L M =
    match LieModule.nilpotencyLength L M with
    | 0 => ⊥
    | k.succ => LieModule.lowerCentralSeries R L M k
-- Mathlib.Topology.Algebra.UniformConvergence
instZeroUniformFun.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : Zero β], instZeroUniformFun = { zero := instZeroUniformFun._aux_1 }
-- Mathlib.Analysis.Matrix.Normed
Matrix.norm_transpose : ∀ {m : Type u_3} {n : Type u_4} {α : Type u_5} [inst : Fintype m] [inst_1 : Fintype n]
  [inst_2 : SeminormedAddCommGroup α] (A : Matrix m n α), ‖A.transpose‖ = ‖A‖
-- Mathlib.Algebra.BigOperators.Ring.Finset
Finset.dvd_sum : ∀ {ι : Type u_1} {R : Type u_4} {s : Finset ι} [inst : NonUnitalSemiring R] {f : ι → R} {a : R},
  (∀ i ∈ s, a ∣ f i) → a ∣ ∑ i ∈ s, f i
-- Mathlib.CategoryTheory.Enriched.FunctorCategory
CategoryTheory.Enriched.FunctorCategory.diagram_obj_map : ∀ (V : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} C] {J : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} J]
  [inst_4 : CategoryTheory.EnrichedOrdinaryCategory V C] (F₁ F₂ : CategoryTheory.Functor J C) (X : Jᵒᵖ) {X_1 Y : J}
  (f : X_1 ⟶ Y),
  ((CategoryTheory.Enriched.FunctorCategory.diagram V F₁ F₂).obj X).map f =
    CategoryTheory.eHomWhiskerLeft V (F₁.obj (Opposite.unop X)) (F₂.map f)