mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Dynamics.PeriodicPts.Lemmas
Function.Commute.minimalPeriod_of_comp_dvd_mul : ∀ {α : Type u_1} {f : α → α} {x : α} {g : α → α},
  Function.Commute f g → Function.minimalPeriod (f ∘ g) x ∣ Function.minimalPeriod f x * Function.minimalPeriod g x
-- Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory
/-- **Alias** of `CategoryTheory.MonoidalCategoryStruct.tensorObj`. -/
CategoryTheory.Functor.chosenProd : {C : Type u} → {𝒞 : CategoryTheory.Category.{v, u} C} → [self : CategoryTheory.MonoidalCategoryStruct C] → C → C → C
-- Init.Data.Int.Linear
Int.Internal.Linear.eq_le_subst_nonpos_cert : Int.Internal.Linear.Var → Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → Bool
-- Mathlib.Order.Filter.Map
Filter.pure_neBot : ∀ {α : Type u} {a : α}, (pure a).NeBot
-- Lean.MetavarContext
Lean.instReprMetavarKind.repr : Lean.MetavarKind → ℕ → Std.Format
-- Mathlib.Condensed.Light.Functors
/-- The functor from `LightProfinite` to `LightCondSet` preserves finite limits.
 -/
instPreservesFiniteLimitsLightProfiniteLightCondSetLightProfiniteToLightCondSet : CategoryTheory.Limits.PreservesFiniteLimits lightProfiniteToLightCondSet
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getKeyD_unitOfList_of_mem : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α] {l : List α} {k k' fallback : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a == b) = false) l →
      k ∈ l → (Std.DHashMap.Raw.Const.unitOfList l).getKeyD k' fallback = k
-- Init.Data.Option.Lemmas
Option.all_eq_true : ∀ {α : Type u_1} (p : α → Bool) (x : Option α), Option.all p x = true ↔ ∀ (y : α), x = some y → p y = true
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
Equiv.summable_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α}
  (e : γ ≃ β), Summable (f ∘ ⇑e) ↔ Summable f
-- Mathlib.Topology.ContinuousMap.Compact
ContinuousMap.norm_lt_iff_of_nonempty : ∀ {α : Type u_1} {E : Type u_3} [inst : TopologicalSpace α] [inst_1 : CompactSpace α]
  [inst_2 : SeminormedAddCommGroup E] (f : C(α, E)) [Nonempty α] {M : ℝ}, ‖f‖ < M ↔ ∀ (x : α), ‖f x‖ < M
-- Mathlib.Topology.MetricSpace.Bounded
comap_dist_left_atTop_eq_cocompact : ∀ {α : Type u} [inst : PseudoMetricSpace α] [ProperSpace α] (x : α),
  Filter.comap (dist x) Filter.atTop = Filter.cocompact α
-- Mathlib.CategoryTheory.Shift.Twist
/-- The invertible elements in the center of `C` which are used to
modify the `shiftFunctorAdd` isomorphisms.  -/
CategoryTheory.TwistShiftData.z : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : Type w} →
      [inst_1 : AddMonoid A] →
        [inst_2 : CategoryTheory.HasShift C A] →
          CategoryTheory.TwistShiftData C A → A → A → (CategoryTheory.CatCenter C)ˣ
-- Mathlib.Analysis.Analytic.Composition
FormalMultilinearSeries.compChangeOfVariables_length : ∀ (m M N : ℕ) {i : (n : ℕ) × (Fin n → ℕ)} (hi : i ∈ FormalMultilinearSeries.compPartialSumSource m M N),
  (FormalMultilinearSeries.compChangeOfVariables m M N i hi).snd.length = i.fst
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Functor.essSurj_mapArrow : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [F.Full] [F.EssSurj], F.mapArrow.EssSurj
-- Mathlib.Order.Filter.Partial
Filter.mem_pmap : ∀ {α : Type u} {β : Type v} (f : α →. β) (l : Filter α) (s : Set β), s ∈ Filter.pmap f l ↔ f.core s ∈ l
-- Mathlib.Data.Finset.Update
Function.update_updateFinset : ∀ {ι : Type u_1} {π : ι → Type u_2} {x : (i : ι) → π i} [inst : DecidableEq ι] {s : Finset ι} {y : (i : ↥s) → π ↑i}
  {i : ι} {z : π i} (hi : i ∉ s),
  Function.update (Function.updateFinset x s y) i z =
    Function.updateFinset x (s ∪ {i}) ((Equiv.piFinsetUnion π ⋯) (y, uniqueElim z))
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.IsBase.rankFinite_of_finite : ∀ {α : Type u_1} {M : Matroid α} {B : Set α}, M.IsBase B → B.Finite → M.RankFinite
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.neg : Lean.Grind.CommRing.Expr → Lean.Grind.CommRing.Expr
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
uniformContinuous_of_tendsto_one : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : Group α] [IsUniformGroup α] {hom : Type u_3}
  [inst_3 : UniformSpace β] [inst_4 : Group β] [IsUniformGroup β] [inst_6 : FunLike hom α β] [MonoidHomClass hom α β]
  {f : hom}, Filter.Tendsto (⇑f) (nhds 1) (nhds 1) → UniformContinuous ⇑f
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.isLittleOTVS_map : ∀ {α : Type u_1} {β : Type u_2} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : Module 𝕜 F] {f : α → E} {g : α → F} {k : β → α} {l : Filter β},
  f =o[𝕜; Filter.map k l] g ↔ (f ∘ k) =o[𝕜; l] (g ∘ k)
-- Mathlib.RepresentationTheory.Homological.TateCohomology.Basic
TateCohomology.instPreservesZeroMorphismsRepCochainComplexModuleCatIntTateComplexFunctor : ∀ {R G : Type u} [inst : CommRing R] [inst_1 : Group G] [inst_2 : Fintype G],
  (tateComplexFunctor R G).PreservesZeroMorphisms
-- Mathlib.NumberTheory.LSeries.AbstractFuncEq
/-- Constant terms at `∞`  -/
WeakFEPair.g₀ : {E : Type u_1} → [inst : NormedAddCommGroup E] → [inst_1 : NormedSpace ℂ E] → WeakFEPair E → E
-- Mathlib.Order.Filter.Ultrafilter.Defs
Ultrafilter.instMembershipSet : {α : Type u} → Membership (Set α) (Ultrafilter α)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
_private.Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting.0.CategoryTheory.Limits.termI₂_2 : Lean.ParserDescr
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getD_insertIfNew : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k a : α} {fallback v : β},
      Std.DTreeMap.Raw.Const.getD (t.insertIfNew k v) a fallback =
        if cmp k a = Ordering.eq ∧ k ∉ t then v else Std.DTreeMap.Raw.Const.getD t a fallback
-- Mathlib.Algebra.Homology.ShortComplex.Exact
/-- If `S` is an exact short complex and `f : S.X₂ ⟶ J` is a morphism to an injective object `J`
such that `S.f ≫ f = 0`, this is a morphism `φ : S.X₃ ⟶ J` such that `S.g ≫ φ = f`.  -/
CategoryTheory.ShortComplex.Exact.descToInjective : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {S : CategoryTheory.ShortComplex C} →
        S.Exact →
          {J : C} →
            (f : S.X₂ ⟶ J) → [CategoryTheory.Injective J] → CategoryTheory.CategoryStruct.comp S.f f = 0 → (S.X₃ ⟶ J)
-- Mathlib.Algebra.Star.StarProjection
IsStarProjection.one_sub_mul_self : ∀ {R : Type u_1} {p : R} [inst : NonAssocRing R] [inst_1 : Star R], IsStarProjection p → (1 - p) * p = 0
-- Mathlib.CategoryTheory.Thin
CategoryTheory.subsingleton_iso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [Quiver.IsThin C] {X Y : C}, Subsingleton (X ≅ Y)
-- Mathlib.CategoryTheory.Limits.WeakLimits.WeakEqualizers
/-- A category `HasWeakEqualizers` if it has all weak limits of shape `WalkingParallelPair`,
i.e. if it has a weak equalizer for every parallel pair of morphisms.  -/
CategoryTheory.Limits.HasWeakEqualizers : (C : Type u_1) → [CategoryTheory.Category.{v_1, u_1} C] → Prop
-- Mathlib.CategoryTheory.Limits.Indization.Category
/-- For small finitely cocomplete categories `C : Type u`, the category of Ind-objects `Ind C` is
equivalent to the category of left-exact functors `Cᵒᵖ ⥤ Type u`  -/
CategoryTheory.Ind.leftExactFunctorEquivalence : (C : Type u) →
  [inst : CategoryTheory.SmallCategory C] →
    [CategoryTheory.Limits.HasFiniteColimits C] → CategoryTheory.Ind C ≌ Cᵒᵖ ⥤ₗ Type u
-- Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc
CategoryTheory.SmallObject.SuccStruct.arrowMap_extendToSucc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {J : Type u} [inst_1 : LinearOrder J]
  [inst_2 : SuccOrder J] {j : J} (hj : ¬IsMax j) (F : CategoryTheory.Functor (↑(Set.Iic j)) C) {X : C}
  (τ : F.obj ⟨j, ⋯⟩ ⟶ X) (i₁ i₂ : J) (hi : i₁ ≤ i₂) (hi₂ : i₂ ≤ j),
  CategoryTheory.SmallObject.SuccStruct.arrowMap (CategoryTheory.SmallObject.SuccStruct.extendToSucc hj F τ) i₁ i₂ hi
      ⋯ =
    CategoryTheory.SmallObject.SuccStruct.arrowMap F i₁ i₂ hi hi₂
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
/-- a type (II) simplex  -/
SSet.Subcomplex.Pairing.RankFunction.Cell.s : {X : SSet} →
  {A : X.Subcomplex} →
    {P : A.Pairing} → {ι : Type v} → [inst : LinearOrder ι] → {f : P.RankFunction ι} → {i : ι} → f.Cell i → ↑P.II
-- Init.Data.SInt.Lemmas
ISize.ofIntLE_sub : ∀ {a b : ℤ} {hab₁ : ISize.minValue.toInt ≤ a - b} {hab₂ : a - b ≤ ISize.maxValue.toInt},
  ISize.ofIntLE (a - b) hab₁ hab₂ = ISize.ofInt a - ISize.ofInt b
-- Mathlib.Order.GaloisConnection.Defs
GaloisConnection.l_eq_bot : ∀ {α : Type u} {β : Type v} [inst : PartialOrder α] [inst_1 : Preorder β] [inst_2 : OrderBot α] {u : α → β} {l : β → α},
  GaloisConnection l u → ∀ {x : β}, l x = ⊥ ↔ x ≤ u ⊥
-- Mathlib.Order.Filter.Cofinite
Filter.disjoint_cofinite_right : ∀ {α : Type u_2} {l : Filter α}, Disjoint l Filter.cofinite ↔ ∃ s ∈ l, s.Finite
-- Init.Data.UInt.Lemmas
UInt32.zero_le : ∀ {a : UInt32}, 0 ≤ a
-- Mathlib.CategoryTheory.Limits.Presentation
CategoryTheory.Limits.ColimitPresentation.w : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : CategoryTheory.Category.{t, w} J]
  {X : C} (pres : CategoryTheory.Limits.ColimitPresentation J X) {i j : J} (f : i ⟶ j),
  CategoryTheory.CategoryStruct.comp (pres.diag.map f) (pres.ι.app j) = pres.ι.app i
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.contains_eq_isSome_getKey? : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {a : α}, m.contains a = (m.getKey? a).isSome
-- Mathlib.Topology.IsLocalHomeomorph
IsLocalHomeomorphOn.isDiscrete_image_iff : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {s : Set X},
  IsLocalHomeomorphOn f s → IsOpen s → (IsDiscrete (f '' s) ↔ IsDiscrete s)
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
/-- The `vectorSpan` of two points is the span of their difference.  -/
vectorSpan_pair : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] (p₁ p₂ : P), vectorSpan k {p₁, p₂} = k ∙ (p₁ -ᵥ p₂)
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.Measure.map_div_left_eq_self : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : DivisionMonoid G] [MeasurableMul G] [MeasurableInv G]
  (μ : MeasureTheory.Measure G) [μ.IsInvInvariant] [μ.IsMulLeftInvariant] (g : G),
  MeasureTheory.Measure.map (fun t => g / t) μ = μ
-- Lean.Declaration
Lean.instInhabitedInductiveVal.default : Lean.InductiveVal
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionItemKind.file : Lean.Lsp.CompletionItemKind
-- Lean.Meta.Tactic.Grind.Extension
/-- Constraints of the form `is_value x` and `is_strict_value x`.
A value is defined as
- A constructor fully applied to value arguments.
- A literal: numerals, strings, etc.
- A lambda. In the strict case, lambdas are not considered.
 -/
Lean.Meta.Grind.EMatchTheoremConstraint.isValue : ℕ → Bool → Lean.Meta.Grind.EMatchTheoremConstraint
-- Mathlib.CategoryTheory.Limits.Pi
/-- If we have a functor `F : J ⥤ Π i, C i` into a category of indexed families,
and we have limits for each of the `F ⋙ Pi.eval C i`,
then `F` has a limit.
 -/
CategoryTheory.pi.hasLimit_of_hasLimit_comp_eval : ∀ {I : Type v₁} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {J : Type v₁}
  [inst_1 : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J ((i : I) → C i)}
  [∀ (i : I), CategoryTheory.Limits.HasLimit (F.comp (CategoryTheory.Pi.eval C i))], CategoryTheory.Limits.HasLimit F
-- Mathlib.LinearAlgebra.Matrix.DotProduct
Matrix.conjTranspose_mul_self_mulVec_eq_zero : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_4} [inst : Fintype m] [inst_1 : Fintype n] [inst_2 : PartialOrder R]
  [inst_3 : NonUnitalRing R] [inst_4 : StarRing R] [StarOrderedRing R] [NoZeroDivisors R] (A : Matrix m n R)
  (v : n → R), (A.conjTranspose * A).mulVec v = 0 ↔ A.mulVec v = 0
-- Mathlib.SetTheory.Cardinal.Finite
/-- If the cardinality is positive, that means it is a finite type, so there is
an equivalence between `α` and `Fin (Nat.card α)`. See also `Finite.equivFin`.  -/
Nat.equivFinOfCardPos : {α : Type u_3} → Nat.card α ≠ 0 → α ≃ Fin (Nat.card α)
-- Mathlib.Geometry.Manifold.StructureGroupoid
/-- A groupoid is closed under restriction if and only if it contains the trivial restriction-closed
groupoid.  -/
closedUnderRestriction_iff_id_le : ∀ {H : Type u_1} [inst : TopologicalSpace H] (G : StructureGroupoid H), ClosedUnderRestriction G ↔ idRestrGroupoid ≤ G
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVExpr.const.injEq : ∀ {w : ℕ} (val val_1 : BitVec w),
  (Std.Tactic.BVDecide.BVExpr.const val = Std.Tactic.BVDecide.BVExpr.const val_1) = (val = val_1)
-- Init.Prelude
instNonemptyForall : ∀ {α : Sort u} {β : Sort v} [Nonempty β], Nonempty (α → β)
-- Lean.Meta.ArgsPacker.Basic
/-- The metadata required for the operation in the `Lean.Meta.ArgsPacker` module; see
the module docs there for an overview.
 -/
Lean.Meta.ArgsPacker : Type
-- Mathlib.Topology.Order.Basic
/-- A version of `isOpen_Ioo` that doesn't require a `LinearOrder`.  -/
isOpen_Ioo' : ∀ {α : Type u} [ts : TopologicalSpace α] [inst : Preorder α] [OrderTopology α] (a b : α), IsOpen (Set.Ioo a b)
-- Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution
_private.Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution.0.DiscreteConvolution.mulFiber_swapEquiv : {M : Type u_1} → [inst : CommMonoid M] → (x : M) → ↑(DiscreteConvolution.mulFiber x) ≃ ↑(DiscreteConvolution.mulFiber x)
-- Mathlib.Combinatorics.SimpleGraph.AdjMatrix
SimpleGraph.natCast_hadamard_adjMatrix : ∀ (α : Type u_1) {V : Type u_2} (G : SimpleGraph V) [inst : DecidableRel G.Adj] [inst_1 : DecidableEq V]
  [inst_2 : MulZeroOneClass α] [inst_3 : NatCast α] (a : ℕ), (↑a).hadamard (SimpleGraph.adjMatrix α G) = 0
-- Lean.Meta.SizeOf
Lean.Meta.SizeOfSpecNested.Context.indInfo : Lean.Meta.SizeOfSpecNested.Context → Lean.InductiveVal
-- Mathlib.CategoryTheory.Monoidal.Braided.Multifunctor
CategoryTheory.BraidedCategory.Hexagon.functor₁₃₂'_map_app_app : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X₁ Y₁ : C}
  (φ : X₁ ⟶ Y₁) (X₂ X₃ : C),
  (((CategoryTheory.BraidedCategory.Hexagon.functor₁₃₂' C).map φ).app X₂).app X₃ =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X₁ X₃ X₂).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerRight φ X₃)
          X₂)
        (CategoryTheory.MonoidalCategoryStruct.associator Y₁ X₃ X₂).hom)
-- Mathlib.Algebra.Group.Int.Even
Int.two_not_dvd_two_mul_add_one : ∀ (n : ℤ), ¬2 ∣ 2 * n + 1
-- Init.Try
/-- If `main` is `true`, all functions in the current module are considered for function induction, unfolding, etc.  -/
Lean.Try.Config.main : Lean.Try.Config → Bool
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.mem_of_mem_keysArray : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  k ∈ t.keysArray → k ∈ t
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.isEmpty_inter_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  t₁.isEmpty = true → (t₁ ∩ t₂).isEmpty = true
-- Mathlib.CategoryTheory.Monad.Algebra
CategoryTheory.Comonad.forget_reflects_iso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (G : CategoryTheory.Comonad C),
  G.forget.ReflectsIsomorphisms
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.registerSyntheticMVarWithCurrRef : Lean.MVarId → Lean.Elab.Term.SyntheticMVarKind → Lean.Elab.TermElabM Unit
-- Mathlib.Algebra.Order.Antidiag.Nat
Nat.finMulAntidiag_existsUnique_prime_dvd : ∀ {d n p : ℕ}, Squarefree n → p ∈ n.primeFactorsList → ∀ f ∈ d.finMulAntidiag n, ∃! i, p ∣ f i
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
CategoryTheory.Bicategory.Adj.leftUnitor_inv_τl : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : CategoryTheory.Bicategory.Adj B} (α : a ⟶ b),
  (CategoryTheory.Bicategory.leftUnitor α).inv.τl = (CategoryTheory.Bicategory.leftUnitor α.l).inv
-- Mathlib.CategoryTheory.Limits.Shapes.Diagonal
CategoryTheory.Limits.pullback_diagonal_map_snd_snd_fst : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  {U V₁ V₂ : C} (f : X ⟶ Y) (i : U ⟶ Y) (i₁ : V₁ ⟶ CategoryTheory.Limits.pullback f i)
  (i₂ : V₂ ⟶ CategoryTheory.Limits.pullback f i),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.diagonal f)
        (CategoryTheory.Limits.pullback.map
          (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.snd f i))
          (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.snd f i)) f f
          (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.fst f i))
          (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.fst f i)) i ⋯ ⋯))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.snd
          (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.snd f i))
          (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.snd f i)))
        (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.fst f i))) =
    CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.diagonal f)
      (CategoryTheory.Limits.pullback.map
        (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.snd f i))
        (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.snd f i)) f f
        (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.fst f i))
        (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.fst f i)) i ⋯ ⋯)
-- Mathlib.Algebra.GroupWithZero.ProdHom
MonoidWithZeroHom.inl_apply_unit : ∀ {G₀ : Type u_1} {H₀ : Type u_2} [inst : GroupWithZero G₀] [inst_1 : GroupWithZero H₀]
  [inst_2 : DecidablePred fun x => x = 0] (x : G₀ˣ), (MonoidWithZeroHom.inl G₀ H₀) ↑x = ↑(x, 1)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.entryAtIdx_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {i : ℕ}
  {h' : i < t₁.size} (h : t₁.Equiv t₂), t₁.entryAtIdx i h' = t₂.entryAtIdx i ⋯
-- Mathlib.CategoryTheory.Monoidal.Ring
CategoryTheory.RingObj.toIsCommAddMonObj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.CartesianMonoidalCategory C}
  {inst_2 : CategoryTheory.BraidedCategory C} {R : C} [self : CategoryTheory.RingObj R],
  CategoryTheory.IsCommAddMonObj R
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.mem_union_of_left : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, k ∈ m₁ → k ∈ m₁ ∪ m₂
-- Mathlib.RingTheory.QuasiFinite.Basic
_private.Mathlib.RingTheory.QuasiFinite.Basic.0.Algebra.QuasiFinite.finite_of_isArtinianRing_of_isLocalRing : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.QuasiFinite R S] [IsArtinianRing R] [IsLocalRing R], Module.Finite R S
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.ResolvableCompletionItemData.mk.inj : ∀ {uri : Lean.Lsp.DocumentUri} {pos : Lean.Lsp.Position} {cPos? : Option ℕ} {id? : Option Lean.Lsp.CompletionIdentifier}
  {uri_1 : Lean.Lsp.DocumentUri} {pos_1 : Lean.Lsp.Position} {cPos?_1 : Option ℕ}
  {id?_1 : Option Lean.Lsp.CompletionIdentifier},
  { uri := uri, pos := pos, cPos? := cPos?, id? := id? } =
      { uri := uri_1, pos := pos_1, cPos? := cPos?_1, id? := id?_1 } →
    uri = uri_1 ∧ pos = pos_1 ∧ cPos? = cPos?_1 ∧ id? = id?_1
-- Mathlib.Topology.Separation.Hausdorff
t2Space_iff : ∀ (X : Type u) [inst : TopologicalSpace X],
  T2Space X ↔ Pairwise fun x y => ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.map₀_one : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι] [inst_4 : Nonempty ι]
  [inst_5 : (i : ι) → One (G i)] [∀ (i j : ι) (h : i ≤ j), OneHomClass (T h) (G i) (G j)], DirectLimit.map₀ f 1 = 1
-- Mathlib.Topology.CompactOpen
ContinuousMap.continuous_compactOpen : ∀ {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {f : X → C(Y, Z)},
  Continuous f ↔ ∀ (K : Set Y), IsCompact K → ∀ (U : Set Z), IsOpen U → IsOpen {x | Set.MapsTo (⇑(f x)) K U}
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.nonneg_smul : ∀ {d : ℕ} {a : ℤ√↑d} {n : ℕ}, a.Nonneg → (↑n * a).Nonneg
-- Mathlib.Algebra.Homology.Embedding.AreComplementary
ComplexShape.Embedding.AreComplementary.equiv_inl : ∀ {ι : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} {c : ComplexShape ι} {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  {e₁ : c₁.Embedding c} {e₂ : c₂.Embedding c} (ac : e₁.AreComplementary e₂) (i₁ : ι₁), ac.equiv (Sum.inl i₁) = e₁.f i₁
-- Mathlib.NumberTheory.LSeries.Basic
/-- The `n`th term of the L-series of `f` evaluated at `s`. We set it to zero when `n = 0`.  -/
LSeries.term : (ℕ → ℂ) → ℂ → ℕ → ℂ
-- Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat
QuadraticModuleCat.toIsometry_comp : ∀ {R : Type u} [inst : CommRing R] {M N U : QuadraticModuleCat R} (f : M ⟶ N) (g : N ⟶ U),
  QuadraticModuleCat.Hom.toIsometry (CategoryTheory.CategoryStruct.comp f g) =
    (QuadraticModuleCat.Hom.toIsometry g).comp (QuadraticModuleCat.Hom.toIsometry f)
-- Lean.Elab.PreDefinition.Structural.Eqns
/-- Generate the "unfold" lemma for `declName`.  -/
_private.Lean.Elab.PreDefinition.Structural.Eqns.0.Lean.Elab.Structural.mkUnfoldEq : Lean.Name → Lean.Elab.Structural.EqnInfo → Lean.MetaM Lean.Name
-- Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
SSet.nonDegenerate_iff_of_mono : ∀ {X : SSet} {n : ℕ} {Y : SSet} (f : X ⟶ Y) [CategoryTheory.Mono f] (x : X.obj (Opposite.op { len := n })),
  (CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op { len := n }))) x ∈ Y.nonDegenerate n ↔ x ∈ X.nonDegenerate n
-- Mathlib.Tactic.ITauto
/-- A comparator for propositions. (There should really be a derive handler for this.)  -/
Mathlib.Tactic.ITauto.IProp.cmp : Mathlib.Tactic.ITauto.IProp → Mathlib.Tactic.ITauto.IProp → Ordering
-- Mathlib.RingTheory.Regular.LinearMap
IsSMulRegular.subsingleton_linearMap_iff : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] [IsNoetherianRing R] [Module.Finite R M] [Module.Finite R N],
  Subsingleton (N →ₗ[R] M) ↔ ∃ r ∈ Module.annihilator R N, IsSMulRegular M r
-- Mathlib.Combinatorics.Additive.Dissociation
mulDissociated_singleton : ∀ {α : Type u_1} [inst : CommGroup α] {a : α}, MulDissociated {a} ↔ a ≠ 1
-- Mathlib.RingTheory.RegularLocalRing.Defs
IsRegularLocalRing.toIsNoetherian : ∀ {R : Type u_1} {inst : CommRing R} [self : IsRegularLocalRing R], IsNoetherian R R
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
/-- The inverse of the unit isomorphism of the equivalence
`widePushoutShapeOpEquiv : (WidePushoutShape J)ᵒᵖ ≌ WidePullbackShape J`  -/
CategoryTheory.Limits.widePushoutShapeOpUnop : (J : Type w) →
  (CategoryTheory.Limits.widePushoutShapeUnop J).comp (CategoryTheory.Limits.widePullbackShapeOp J) ≅
    CategoryTheory.Functor.id (CategoryTheory.Limits.WidePushoutShape J)ᵒᵖ
-- Mathlib.Algebra.Group.Subgroup.Finite
Subgroup.one_lt_card_iff_ne_bot : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) [Finite ↥H], 1 < Nat.card ↥H ↔ H ≠ ⊥