mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.EilenbergSteenrod
TopPair.HomologyPretheory.Hom.mk.sizeOf_spec : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} {HP HP' : TopPair.HomologyPretheory C c} [inst_2 : SizeOf C] [inst_3 : SizeOf ι]
  (homₚ : (i : ι) → HP.Hₚ i ⟶ HP'.Hₚ i) (hom : (i : ι) → HP.H i ⟶ HP'.H i)
  (iso_comm :
    autoParam
      (∀ (i : ι),
        CategoryTheory.CategoryStruct.comp (HP.iso i).hom (TopPair.incl.whiskerLeft (homₚ i)) =
          CategoryTheory.CategoryStruct.comp (hom i) (HP'.iso i).hom)
      TopPair.HomologyPretheory.Hom.iso_comm._autoParam)
  (w :
    autoParam
      (∀ (i j : ι),
        CategoryTheory.CategoryStruct.comp (HP.δ i j) (TopPair.proj₂.whiskerLeft (hom j)) =
          CategoryTheory.CategoryStruct.comp (homₚ i) (HP'.δ i j))
      TopPair.HomologyPretheory.Hom.w._autoParam),
  sizeOf { homₚ := homₚ, hom := hom, iso_comm := iso_comm, w := w } = 1
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.Splits.C : ∀ {R : Type u_1} [inst : Semiring R] (a : R), (Polynomial.C a).Splits
-- Mathlib.CategoryTheory.Preadditive.Biproducts
/-- A functor between preadditive categories that preserves (zero morphisms and) finite coproducts
preserves finite biproducts.  -/
CategoryTheory.Limits.preservesBiproduct_of_preservesCoproduct : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {D : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} D] [inst_3 : CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D)
  [inst_4 : F.PreservesZeroMorphisms] {J : Type u_1} [Finite J] {f : J → C}
  [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Discrete.functor f) F],
  CategoryTheory.Limits.PreservesBiproduct f F
-- Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction
UpperHalfPlane.num_continuous : Continuous ↿UpperHalfPlane.num
-- Lean.Meta.Injective
_private.Lean.Meta.Injective.0.Lean.Meta.mkInjectiveTheoremTypeCore? : Lean.ConstructorVal → Bool → Lean.MetaM (Option Lean.Expr)
-- Lean.Elab.App
/-- The index of the parameter currently being worked on  -/
_private.Lean.Elab.App.0.Lean.Elab.Term.ElabAppArgs.State.paramIdx : Lean.Elab.Term.ElabAppArgs.State → ℕ
-- Mathlib.Analysis.Convex.DoublyStochasticMatrix
/-- A square matrix is doubly stochastic iff all entries are nonnegative, and left or right
multiplication by the vector of all 1s gives the vector of all 1s.
 -/
doublyStochastic : (R : Type u_3) →
  (n : Type u_4) →
    [inst : Fintype n] →
      [inst_1 : DecidableEq n] →
        [inst_2 : Semiring R] → [inst_3 : PartialOrder R] → [IsOrderedRing R] → Submonoid (Matrix n n R)
-- Mathlib.LinearAlgebra.Matrix.Integer
Matrix.num_ofNat : ∀ {m : Type u_1} [inst : Fintype m] [inst_1 : DecidableEq m] (a : ℕ) [inst_2 : a.AtLeastTwo], (OfNat.ofNat a).num = ↑a
-- Mathlib.Order.Filter.IndicatorFunction
mulIndicator_eventuallyEq : ∀ {α : Type u_1} {M : Type u_3} [inst : One M] {s t : Set α} {f g : α → M} {l : Filter α},
  f =ᶠ[l ⊓ Filter.principal s] g → s =ᶠ[l] t → s.mulIndicator f =ᶠ[l] t.mulIndicator g
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Relations.Solution.mk.inj : ∀ {A : Type u} {inst : Ring A} {relations : Module.Relations A} {M : Type v} {inst_1 : AddCommGroup M}
  {inst_2 : Module A M} {var : relations.G → M}
  {linearCombination_var_relation : ∀ (r : relations.R), (Finsupp.linearCombination A var) (relations.relation r) = 0}
  {var_1 : relations.G → M}
  {linearCombination_var_relation_1 :
    ∀ (r : relations.R), (Finsupp.linearCombination A var_1) (relations.relation r) = 0},
  { var := var, linearCombination_var_relation := linearCombination_var_relation } =
      { var := var_1, linearCombination_var_relation := linearCombination_var_relation_1 } →
    var = var_1
-- Std.Tactic.BVDecide.Reflect
Std.Tactic.BVDecide.Reflect.BitVec.reverse_congr : ∀ (w : ℕ) (x x' : BitVec w), x = x' → x'.reverse = x.reverse
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roc.succ_mem_succ_succ_iff : ∀ {α : Type u} [inst : LE α] [DecidableLE α] [inst_2 : LT α] [inst_3 : Std.PRange.UpwardEnumerable α]
  [Std.PRange.LinearlyUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α]
  [Std.PRange.LawfulUpwardEnumerableLT α] [inst_7 : Std.PRange.InfinitelyUpwardEnumerable α] [Std.Rxc.IsAlwaysFinite α]
  [Std.PRange.LawfulUpwardEnumerable α] {lo hi a : α},
  (Std.PRange.succ a ∈ (Std.PRange.succ lo)<...=Std.PRange.succ hi) ↔ a ∈ lo<...=hi
-- Mathlib.ModelTheory.Definability
/-- Every TermDefinable function has a tupleGraph that is definable.  -/
Set.TermDefinable.definable_tupleGraph : ∀ {M : Type w} (A : Set M) (L : FirstOrder.Language) [inst : L.Structure M] {α : Type u₁} {f : (α → M) → M},
  A.TermDefinable L f → A.Definable L (Function.tupleGraph f)
-- Mathlib.Algebra.Homology.Embedding.ExtendHomology
HomologicalComplex.quasiIso_extendMap_iff : ∀ {ι : 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]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {K L : HomologicalComplex C c} (φ : K ⟶ L) (e : c.Embedding c')
  [inst_3 : ∀ (j : ι), K.HasHomology j] [inst_4 : ∀ (j : ι), L.HasHomology j],
  QuasiIso (HomologicalComplex.extendMap φ e) ↔ QuasiIso φ
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.Λ'.succ.injEq : ∀ (q q_1 : Turing.PartrecToTM2.Λ'), (q.succ = q_1.succ) = (q = q_1)
-- Mathlib.Analysis.Complex.Basic
RCLike.conj_tsum : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] {L : SummationFilter α} (f : α → 𝕜),
  (starRingEnd 𝕜) (∑'[L] (a : α), f a) = ∑'[L] (a : α), (starRingEnd 𝕜) (f a)
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.extend_function_of_lt : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} (f : ↑s ↪ β),
  Cardinal.mk ↑s < Cardinal.mk α → Nonempty (α ≃ β) → ∃ g, ∀ (x : ↑s), g ↑x = f x
-- Mathlib.Algebra.Lie.Extension
/-- The underlying type.  -/
LieAlgebra.ofTwoCocycle.carrier : {R : Type u_5} →
  {L : Type u_6} →
    {M : Type u_7} →
      [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] →
                  [inst_6 : LieModule R L M] →
                    {c : ↥(LieModule.Cohomology.twoCocycle R L M)} → LieAlgebra.ofTwoCocycle c → L × M
-- Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
/-- The functor which sends a split simplicial object in a preadditive category to
the chain complex which consists of nondegenerate simplices.  -/
CategoryTheory.SimplicialObject.Split.nondegComplexFunctor : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      CategoryTheory.Functor (CategoryTheory.SimplicialObject.Split C) (ChainComplex C ℕ)
-- Mathlib.LinearAlgebra.AnnihilatingPolynomial
Polynomial.span_minpoly_eq_annihilator : ∀ (𝕜 : Type u_1) [inst : Field 𝕜] {M : Type u_3} [inst_1 : AddCommGroup M] [inst_2 : Module 𝕜 M] (f : Module.End 𝕜 M),
  Ideal.span {minpoly 𝕜 f} = Module.annihilator (Polynomial 𝕜) (Module.AEval' f)
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanClass.mk_add_lt_mk_left_iff : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] {a b : M},
  ArchimedeanClass.mk (a + b) < ArchimedeanClass.mk a ↔ ArchimedeanClass.mk b < ArchimedeanClass.mk a
-- Mathlib.Algebra.Ring.Defs
NonUnitalSemiring.toNonUnitalNonAssocSemiring : {α : Type u} → [self : NonUnitalSemiring α] → NonUnitalNonAssocSemiring α
-- Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
/-- The **universal property with parameters** of the topology on the restricted product:
for any topological space `Y` of "parameters", a map from `(Πʳ i, [R i, A i]) × Y` is continuous
*iff* its restriction to each `(Πʳ i, [R i, A i]_[𝓟 S]) × Y` (with `S` cofinite) is continuous.  -/
RestrictedProduct.continuous_dom_prod_right : ∀ {ι : Type u_1} {R : ι → Type u_2} {A : (i : ι) → Set (R i)} [inst : (i : ι) → TopologicalSpace (R i)],
  (∀ (i : ι), IsOpen (A i)) →
    ∀ {X : Type u_3} {Y : Type u_4} [inst_1 : TopologicalSpace X] [inst_2 : TopologicalSpace Y]
      {f : RestrictedProduct (fun i => R i) (fun i => A i) Filter.cofinite × Y → X},
      Continuous f ↔
        ∀ (S : Set ι) (hS : Filter.cofinite ≤ Filter.principal S),
          Continuous (f ∘ Prod.map (RestrictedProduct.inclusion R A hS) id)
-- Mathlib.Order.Filter.Prod
Filter.prod_comm' : ∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β}, f ×ˢ g = Filter.comap Prod.swap (g ×ˢ f)
-- Mathlib.Analysis.Convex.Side
AffineSubspace.isPreconnected_setOfPred_sOppSide : ∀ {V : Type u_2} {P : Type u_4} [inst : SeminormedAddCommGroup V] [inst_1 : NormedSpace ℝ V]
  [inst_2 : PseudoMetricSpace P] [inst_3 : NormedAddTorsor V P] (s : AffineSubspace ℝ P) (x : P),
  IsPreconnected {y | s.SOppSide x y}
-- Lean.Meta.Match.MatcherInfo
Lean.Meta.Match.Overlaps : Type
-- Mathlib.CategoryTheory.Preadditive.Biproducts
CategoryTheory.Functor.splitEpiBiproductComparison.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {J : Type w₁}
  (F : CategoryTheory.Functor C D) (f : J → C) [inst_4 : CategoryTheory.Limits.HasBiproduct f]
  [inst_5 : CategoryTheory.Limits.HasBiproduct (F.obj ∘ f)] [inst_6 : F.PreservesZeroMorphisms],
  F.splitEpiBiproductComparison f = F.splitEpiBiproductComparison f
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
/-- A topological vector space `E` is **polynormable** over `𝕜` if its topology is induced by
*some* family of `𝕜`-seminorms. Equivalently, its topology is induced by *all* its continuous
seminorm.

If `𝕜` is `RCLike`, this is equivalent to `LocallyConvexSpace 𝕜 E`.  -/
PolynormableSpace : (𝕜 : Type u_2) →
  (E : Type u_6) →
    [inst : NormedField 𝕜] → [inst_1 : AddCommGroup E] → [Module 𝕜 E] → [topology : TopologicalSpace E] → Prop
-- Init.Data.Int.Linear
Int.Internal.Linear.le_of_le_diseq : ∀ (ctx : Int.Internal.Linear.Context) (p₁ p₂ p₃ : Int.Internal.Linear.Poly),
  Int.Internal.Linear.le_of_le_diseq_cert p₁ p₂ p₃ = true →
    Int.Internal.Linear.Poly.denote' ctx p₁ ≤ 0 →
      Int.Internal.Linear.Poly.denote' ctx p₂ ≠ 0 → Int.Internal.Linear.Poly.denote' ctx p₃ ≤ 0
-- Mathlib.LinearAlgebra.RootSystem.Chain
RootPairing.one_le_chainTopCoeff_of_root_add_mem : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Finite ι] [inst_1 : CommRing R]
  [inst_2 : CharZero R] [inst_3 : IsDomain 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.IsCrystallographic] {i j : ι} [P.IsReduced],
  P.root i + P.root j ∈ Set.range ⇑P.root → 1 ≤ RootPairing.chainTopCoeff i j
-- Mathlib.RingTheory.Radical.Basic
UniqueFactorizationMonoid.radical_dvd_radical_iff_primeFactors_subset_primeFactors : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [inst_1 : NormalizationMonoid M] [inst_2 : UniqueFactorizationMonoid M]
  {a b : M},
  UniqueFactorizationMonoid.radical a ∣ UniqueFactorizationMonoid.radical b ↔
    UniqueFactorizationMonoid.primeFactors a ⊆ UniqueFactorizationMonoid.primeFactors b
-- Mathlib.Algebra.Group.Submonoid.Basic
Submonoid.instInfSet : {M : Type u_1} → [inst : MulOneClass M] → InfSet (Submonoid M)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.ResolvableCompletionItemData.mk.sizeOf_spec : ∀ (uri : Lean.Lsp.DocumentUri) (pos : Lean.Lsp.Position) (cPos? : Option ℕ)
  (id? : Option Lean.Lsp.CompletionIdentifier),
  sizeOf { uri := uri, pos := pos, cPos? := cPos?, id? := id? } =
    1 + sizeOf uri + sizeOf pos + sizeOf cPos? + sizeOf id?
-- Init.Data.List.Impl
/-- Auxiliary for `erasePTR`: `erasePTR.go p l xs acc = acc.toList ++ eraseP p xs`,
unless `xs` does not contain any elements satisfying `p`, where it returns `l`.  -/
_private.Init.Data.List.Impl.0.List.erasePTR.go : {α : Type u_1} → (α → Bool) → List α → List α → Array α → List α
-- Lean.Data.Lsp.TextSync
Lean.Lsp.DidCloseTextDocumentParams.mk.sizeOf_spec : ∀ (textDocument : Lean.Lsp.TextDocumentIdentifier), sizeOf { textDocument := textDocument } = 1 + sizeOf textDocument
-- Mathlib.AlgebraicGeometry.ColimitsOver
CategoryTheory.MorphismProperty.Over.mapPullbackAdj.congr_simp : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] (P Q : CategoryTheory.MorphismProperty T)
  [inst_1 : Q.IsMultiplicative] {X Y : T} [inst_2 : P.IsStableUnderComposition] [inst_3 : Q.IsStableUnderBaseChange]
  (f : X ⟶ Y) [inst_4 : P.HasPullbacksAlong f] [inst_5 : P.IsStableUnderBaseChangeAlong f]
  [inst_6 : Q.HasOfPostcompProperty Q] (hPf : P f) (hQf : Q f),
  CategoryTheory.MorphismProperty.Over.mapPullbackAdj P Q f hPf hQf =
    CategoryTheory.MorphismProperty.Over.mapPullbackAdj P Q f hPf hQf
-- Mathlib.LinearAlgebra.PerfectPairing.Basic
LinearMap.IsPerfPair.of_bijective : ∀ {R : Type u_1} {M : Type u_3} {N : Type u_5} [inst : AddCommGroup M] [inst_1 : AddCommGroup N] [inst_2 : CommRing R]
  [inst_3 : Module R M] [inst_4 : Module R N] (p : M →ₗ[R] N →ₗ[R] R) [Module.IsReflexive R N],
  Function.Bijective ⇑p → p.IsPerfPair
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.instDistribMulAction : {α : Type u} →
  {β : Type v} →
    {𝕜 : Type u_2} →
      [inst : PseudoMetricSpace 𝕜] →
        [inst_1 : TopologicalSpace α] →
          [inst_2 : PseudoMetricSpace β] →
            [inst_3 : MonoidWithZero 𝕜] →
              [inst_4 : AddMonoid β] →
                [inst_5 : DistribMulAction 𝕜 β] →
                  [IsBoundedSMul 𝕜 β] →
                    [inst : BoundedAdd β] →
                      [inst_6 : ContinuousAdd β] → DistribMulAction 𝕜 (BoundedContinuousFunction α β)
-- Mathlib.Data.List.Sort
/-- For a reflexive relation, insert then erasing is the identity.  -/
List.erase_orderedInsert : ∀ {α : Type u_1} {r : α → α → Prop} [inst : DecidableRel r] [inst_1 : DecidableEq α] [Std.Refl r] (x : α) (xs : List α),
  (List.orderedInsert r x xs).erase x = xs
-- Init.Data.Array.Lemmas
Array.size_replicate : ∀ {α : Type u_1} {n : ℕ} {v : α}, (Array.replicate n v).size = n
-- Lean.Meta.Tactic.Grind.Anchor
Lean.Meta.Grind.HasAnchor.getAnchor : {α : Type u} → [self : Lean.Meta.Grind.HasAnchor α] → α → UInt64
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.Equiv.getKey?_eq : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] {k : α}, m₁.WF → m₂.WF → m₁.Equiv m₂ → m₁.getKey? k = m₂.getKey? k
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.isMaximumClique_compl : ∀ {α : Type u_3} {G : SimpleGraph α} [inst : Finite α] (s : Finset α), Gᶜ.IsMaximumClique s ↔ G.IsMaximumIndepSet s
-- Init.Data.SInt.Bitwise
Int32.toInt16_not : ∀ (a : Int32), (~~~a).toInt16 = ~~~a.toInt16
-- Mathlib.CategoryTheory.LiftingProperties.Basic
CategoryTheory.HasLiftingProperty.iff_unop : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A B X Y : Cᵒᵖ} (i : A ⟶ B) (p : X ⟶ Y),
  CategoryTheory.HasLiftingProperty i p ↔ CategoryTheory.HasLiftingProperty p.unop i.unop
-- Mathlib.GroupTheory.MonoidLocalization.Maps
Submonoid.LocalizationMap.mulEquivOfLocalizations_symm_apply : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {P : Type u_3}
  [inst_2 : CommMonoid P] (f : S.LocalizationMap N) {k : S.LocalizationMap P} {x : P},
  (f.mulEquivOfLocalizations k).symm x = (k.lift ⋯) x
-- Mathlib.Topology.ContinuousMap.Basic
Homeomorph.instContinuousMapClass : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β],
  ContinuousMapClass (α ≃ₜ β) α β
-- Mathlib.MeasureTheory.Integral.Prod
MeasureTheory.integrable_swap_iff : ∀ {α : Type u_1} {β : Type u_2} {E : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [inst_2 : NormedAddCommGroup E] [MeasureTheory.SFinite ν]
  [MeasureTheory.SFinite μ] {f : α × β → E},
  MeasureTheory.Integrable (f ∘ Prod.swap) (ν.prod μ) ↔ MeasureTheory.Integrable f (μ.prod ν)
-- Mathlib.Algebra.Group.Defs
/-- A group is called *cyclic* if it is generated by a single element. 

[Wikidata Q245462](https://www.wikidata.org/wiki/Q245462) -/
IsCyclic : (G : Type u) → [Pow G ℤ] → Prop
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.yonedaMon_obj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (M : CategoryTheory.Mon C), CategoryTheory.yonedaMon.obj M = CategoryTheory.yonedaMonObj M.X
-- Mathlib.Data.Nat.Factorial.Basic
Nat.descFactorialBinary.eq_1 : ∀ (n k : ℕ), n.descFactorialBinary k = if n < k then 0 else (n - k + 1).ascFactorialBinary k
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.ContinuousHom.id_comp : ∀ {β : Type u_3} {γ : Type u_4} [inst : OmegaCompletePartialOrder β] [inst_1 : OmegaCompletePartialOrder γ]
  (f : β →𝒄 γ), OmegaCompletePartialOrder.ContinuousHom.id.comp f = f
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Linear
CategoryTheory.Abelian.Ext.mk₀_linearEquiv₀_apply : ∀ {R : Type t} [inst : Ring R] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.Linear R C] [inst_4 : CategoryTheory.HasExt C] {X Y : C}
  (f : CategoryTheory.Abelian.Ext X Y 0), CategoryTheory.Abelian.Ext.mk₀ (CategoryTheory.Abelian.Ext.linearEquiv₀ f) = f
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
_private.Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic.0.IsProperLinearSet.eq_base_vadd_closure_periods : ∀ {ι : Type u_3} {s : Set (ι → ℕ)} (hs : IsProperLinearSet s),
  s = IsProperLinearSet.base✝ hs +ᵥ ↑(AddSubmonoid.closure (IsProperLinearSet.periods✝ hs))
-- Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
CategoryTheory.MorphismProperty.Under.mapPushoutAdj_counit_app : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] (P Q : CategoryTheory.MorphismProperty T)
  [inst_1 : Q.IsMultiplicative] {X Y : T} [inst_2 : P.IsStableUnderComposition] [inst_3 : Q.IsStableUnderCobaseChange]
  (f : X ⟶ Y) [inst_4 : P.HasPushoutsAlong f] [inst_5 : P.IsStableUnderCobaseChangeAlong f]
  [inst_6 : Q.HasOfPrecompProperty Q] (hPf : P f) (hQf : Q f) (A : P.Under Q Y),
  (CategoryTheory.MorphismProperty.Under.mapPushoutAdj P Q f hPf hQf).counit.app A =
    CategoryTheory.MorphismProperty.Under.homMk
      (CategoryTheory.Limits.pushout.desc (CategoryTheory.CategoryStruct.id A.right) A.hom ⋯) ⋯ ⋯
-- Std.Data.TreeSet.Raw.Basic
Std.TreeSet.Raw.instBEq : {α : Type u} → {cmp : α → α → Ordering} → BEq (Std.TreeSet.Raw α cmp)
-- Mathlib.Algebra.Lie.Basic
LieRingModule.toBracket : {L : Type v} → {M : Type w} → {inst : LieRing L} → {inst_1 : AddCommGroup M} → [self : LieRingModule L M] → Bracket L M
-- Mathlib.Algebra.Lie.Rank
LieAlgebra.rank_eq_natTrailingDegree : ∀ (R : Type u_1) (L : Type u_3) {ι : Type u_5} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : Module.Finite R L] [inst_4 : Module.Free R L] [inst_5 : Fintype ι] (b : Module.Basis ι R L) [Nontrivial R]
  [inst_7 : DecidableEq ι], LieAlgebra.rank R L = ((↑(LieAlgebra.ad R L)).polyCharpoly b).natTrailingDegree
-- Mathlib.Topology.Compactification.StoneCech
/-- Auxiliary construction towards the Stone-Čech compactification of a topological space.
It should not be used after the Stone-Čech compactification is constructed.  -/
PreStoneCech : (α : Type u) → [TopologicalSpace α] → Type u
-- Lean.Parser.Command
Lean.Parser.Command.derivingClass : Lean.Parser.Parser
-- Mathlib.MeasureTheory.Measure.MutuallySingular
MeasureTheory.Measure.MutuallySingular.sum_left : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {ν : MeasureTheory.Measure α} {ι : Type u_2} [Countable ι]
  {μ : ι → MeasureTheory.Measure α},
  (MeasureTheory.Measure.sum μ).MutuallySingular ν ↔ ∀ (i : ι), (μ i).MutuallySingular ν
-- Mathlib.Topology.WithTopology
WithTopology.preimage_toTopology : ∀ {X : Type u_1} (t : TopologicalSpace X) (s : Set (WithTopology X t)),
  WithTopology.toTopology t ⁻¹' s = WithTopology.ofTopology '' s
-- Init.Data.String.Lemmas.Pattern.Char
String.Slice.Pattern.Model.Char.matchesAt_iff : ∀ {c : Char} {s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.Model.MatchesAt c pos ↔ ∃ (h : pos ≠ s.endPos), pos.get h = c
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
mabs_of_lt_one : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : Group α] {a : α} [MulLeftMono α], a < 1 → |a|ₘ = a⁻¹
-- Mathlib.RingTheory.FreeCommRing
FreeCommRing.of.eq_1 : ∀ {α : Type u} (x : α), FreeCommRing.of x = FreeAbelianGroup.of (Multiplicative.ofAdd {x})
-- Mathlib.CategoryTheory.Monoidal.Closed.FunctorToTypes
_private.Mathlib.CategoryTheory.Monoidal.Closed.FunctorToTypes.0.CategoryTheory.Functor.homObjEquiv.match_1.splitter : {C : Type u_3} →
  [inst : CategoryTheory.Category.{u_1, u_3} C] →
    (F A : CategoryTheory.Functor C (Type u_2)) →
      (X : C) →
        (motive : (CategoryTheory.MonoidalCategoryStruct.tensorObj F A).obj X → Sort u_4) →
          (x : (CategoryTheory.MonoidalCategoryStruct.tensorObj F A).obj X) →
            ((x : F.obj X) → (y : A.obj X) → motive (x, y)) → motive x
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.String
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.String.0.String.reduceListChar : Lean.Expr → String → Lean.Meta.SimpM Lean.Meta.Simp.DStep
-- Mathlib.Topology.UniformSpace.Compact
IsClosed.relPreimage_of_isCompact : ∀ {α : Type ua} {β : Type ub} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {s : SetRel α β},
  IsClosed s → ∀ {t : Set β}, IsCompact t → IsClosed (s.preimage t)
-- Mathlib.Order.Filter.Bases.Basic
Filter.HasBasis.ex_mem : ∀ {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α}, l.HasBasis p s → ∃ i, p i
-- Mathlib.Algebra.Polynomial.Monic
Polynomial.Monic.mul_left_eq_zero_iff : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.Monic → ∀ {q : Polynomial R}, q * p = 0 ↔ q = 0
-- Mathlib.Algebra.Star.Subsemiring
StarSubsemiring.semiring : {R : Type v} → [inst : NonAssocSemiring R] → [inst_1 : StarRing R] → (s : StarSubsemiring R) → NonAssocSemiring ↥s
-- Mathlib.CategoryTheory.Join.Basic
/-- Two functors out of a join of categories are naturally isomorphic if their
compositions with the inclusions are isomorphic and the whiskering with the canonical
transformation is respected through these isomorphisms.  -/
CategoryTheory.Join.mkNatIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {E : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} E] →
            {F G : CategoryTheory.Functor (CategoryTheory.Join C D) E} →
              (eₗ : (CategoryTheory.Join.inclLeft C D).comp F ≅ (CategoryTheory.Join.inclLeft C D).comp G) →
                (eᵣ : (CategoryTheory.Join.inclRight C D).comp F ≅ (CategoryTheory.Join.inclRight C D).comp G) →
                  autoParam
                      (CategoryTheory.CategoryStruct.comp
                          (CategoryTheory.Functor.whiskerRight (CategoryTheory.Join.edgeTransform C D) F)
                          ((CategoryTheory.Prod.snd C D).isoWhiskerLeft eᵣ).hom =
                        CategoryTheory.CategoryStruct.comp ((CategoryTheory.Prod.fst C D).isoWhiskerLeft eₗ).hom
                          (CategoryTheory.Functor.whiskerRight (CategoryTheory.Join.edgeTransform C D) G))
                      CategoryTheory.Join.mkNatIso._auto_1 →
                    (F ≅ G)
-- Mathlib.Analysis.Convex.Between
sbtw_vsub_const_iff : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] {x y z : P} (p : P), Sbtw R (x -ᵥ p) (y -ᵥ p) (z -ᵥ p) ↔ Sbtw R x y z