mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
/-- `cyclotomic' n R` is monic.  -/
Polynomial.cyclotomic'.monic : ∀ (n : ℕ) (R : Type u_2) [inst : CommRing R] [inst_1 : IsDomain R], (Polynomial.cyclotomic' n R).Monic
-- Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory
CategoryTheory.Triangulated.AbelianSubcategory.mor₁_πQ : ∀ {C : Type u_1} {A : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Limits.HasZeroObject C] [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : CategoryTheory.HasShift C ℤ] [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [inst_5 : CategoryTheory.Pretriangulated C] [inst_6 : CategoryTheory.Category.{v_2, u_2} A]
  {ι : CategoryTheory.Functor A C} {X₁ X₂ : A} {f₁ : X₁ ⟶ X₂} {X₃ : C} {f₂ : ι.obj X₂ ⟶ X₃}
  {f₃ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj (ι.obj X₁)},
  CategoryTheory.Pretriangulated.Triangle.mk (ι.map f₁) f₂ f₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles →
    ∀ {Q : A} (β : X₃ ⟶ ι.obj Q) [inst_7 : ι.Full] [inst_8 : CategoryTheory.Preadditive A] [ι.Faithful],
      CategoryTheory.CategoryStruct.comp f₁ (CategoryTheory.Triangulated.AbelianSubcategory.πQ f₂ β) = 0
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.isLongestRevMatch_iff_isRevMatch : ∀ {ρ : Type} (pat : ρ) [inst : String.Slice.Pattern.Model.PatternModel pat]
  [String.Slice.Pattern.Model.NoSuffixPatternModel pat] {s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.Model.IsLongestRevMatch pat pos ↔ String.Slice.Pattern.Model.IsRevMatch pat pos
-- Mathlib.NumberTheory.Bernoulli
bernoulli'.eq_def : ∀ (n : ℕ), bernoulli' n = 1 - ∑ k, ↑(n.choose ↑k) / (↑n - ↑↑k + 1) * bernoulli' ↑k
-- Mathlib.CategoryTheory.Idempotents.KaroubiKaroubi
/-- The unit isomorphism of the equivalence  -/
CategoryTheory.Idempotents.KaroubiKaroubi.unitIso : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    CategoryTheory.Functor.id (CategoryTheory.Idempotents.Karoubi C) ≅
      (CategoryTheory.Idempotents.toKaroubi (CategoryTheory.Idempotents.Karoubi C)).comp
        (CategoryTheory.Idempotents.KaroubiKaroubi.inverse C)
-- Mathlib.FieldTheory.Normal.Closure
/-- If `K/F` is algebraic, the "generated by roots" condition in IsNormalClosure can be replaced
by "generated by images of embeddings".  -/
Algebra.IsAlgebraic.isNormalClosure_iff : ∀ {F : Type u_1} {K : Type u_2} {L : Type u_3} [inst : Field F] [inst_1 : Field K] [inst_2 : Field L]
  [inst_3 : Algebra F K] [inst_4 : Algebra F L] [Algebra.IsAlgebraic F K],
  IsNormalClosure F K L ↔
    (∀ (x : K), (Polynomial.map (algebraMap F L) (minpoly F x)).Splits) ∧ IntermediateField.normalClosure F K L = ⊤
-- Mathlib.Tactic.FieldSimp.Lemmas
/-- Inductive type representing the options for the sign of an element in a type-expression `M`

If the sign is "-", then we also carry an expression for a field instance on `M`, to allow us to
construct that negation when needed.  -/
Mathlib.Tactic.FieldSimp.Sign : {v : Lean.Level} → Q(Type v) → Type
-- Mathlib.Combinatorics.Enumerative.Catalan.Basic
/-- A helper sequence that can be used to prove the equality of the recursive and the explicit
definition using a telescoping sum argument.  -/
_private.Mathlib.Combinatorics.Enumerative.Catalan.Basic.0.gosperCatalan : ℕ → ℕ → ℚ
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.of_ne_one : ∀ {α : Type u_1} (a : α), FreeMonoid.of a ≠ 1
-- Mathlib.Topology.Algebra.Ring.Basic
NonUnitalSubsemiring.instIsTopologicalSemiring : ∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : NonUnitalSemiring R] [IsTopologicalSemiring R]
  (S : NonUnitalSubsemiring R), IsTopologicalSemiring ↥S
-- Mathlib.Analysis.Asymptotics.Lemmas
/-- Transfer `IsLittleO` over a `Homeomorph`.  -/
Homeomorph.isLittleO_congr : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {E : Type u_3}
  [inst_2 : Norm E] {F : Type u_4} [inst_3 : Norm F] (e : α ≃ₜ β) {b : β} {f : β → E} {g : β → F},
  f =o[nhds b] g ↔ (f ∘ ⇑e) =o[nhds (e.symm b)] (g ∘ ⇑e)
-- Init.Data.UInt.Lemmas
UInt16.ofNatLT_add : ∀ {a b : ℕ} (hab : a + b < 2 ^ 16), UInt16.ofNatLT (a + b) hab = UInt16.ofNatLT a ⋯ + UInt16.ofNatLT b ⋯
-- Mathlib.Tactic.Translate.Core
/-- Elaboration of the `(rename := ...)` option.  -/
Mathlib.Tactic.Translate.elabRename : Array (Lean.TSyntax `Mathlib.Tactic.Translate.renameRule) →
  Lean.Name → Array Lean.Name → Lean.MetaM (Lean.NameMap Lean.Name)
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.arrowCongr_trans : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} {A₃ : Type uA₃} {A₁' : Type uA₁'} {A₂' : Type uA₂'} {A₃' : Type uA₃'}
  [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂] [inst_3 : Semiring A₃] [inst_4 : Semiring A₁']
  [inst_5 : Semiring A₂'] [inst_6 : Semiring A₃'] [inst_7 : Algebra R A₁] [inst_8 : Algebra R A₂]
  [inst_9 : Algebra R A₃] [inst_10 : Algebra R A₁'] [inst_11 : Algebra R A₂'] [inst_12 : Algebra R A₃']
  (e₁ : A₁ ≃ₐ[R] A₂) (e₁' : A₁' ≃ₐ[R] A₂') (e₂ : A₂ ≃ₐ[R] A₃) (e₂' : A₂' ≃ₐ[R] A₃'),
  (e₁.trans e₂).arrowCongr (e₁'.trans e₂') = (e₁.arrowCongr e₁').trans (e₂.arrowCongr e₂')
-- Init.Data.List.Lemmas
List.getLast?_eq_getElem? : ∀ {α : Type u_1} {l : List α}, l.getLast? = l[l.length - 1]?
-- Std.Do.PostCond
/-- A postcondition for the given predicate shape, with one `Assertion` for the terminating case and
one `Assertion` for each `.except` layer in the predicate shape.
```
variable (α σ ε : Type)
example : PostCond α (.arg σ .pure) = ((α → σ → ULift Prop) × PUnit) := rfl
example : PostCond α (.except ε .pure) = ((α → ULift Prop) × (ε → ULift Prop) × PUnit) := rfl
example : PostCond α (.arg σ (.except ε .pure)) = ((α → σ → ULift Prop) × (ε → ULift Prop) × PUnit) := rfl
example : PostCond α (.except ε (.arg σ .pure)) = ((α → σ → ULift Prop) × (ε → σ → ULift Prop) × PUnit) := rfl
```
 -/
Std.Do.«termPost⟨_,,⟩» : Lean.ParserDescr
-- Mathlib.RingTheory.MvPowerSeries.Equiv
PowerSeries.toMvPowerSeries_C : ∀ {R : Type u_1} {σ : Type u_2} [inst : CommSemiring R] (i : σ) (r : R),
  (PowerSeries.toMvPowerSeries i) (PowerSeries.C r) = MvPowerSeries.C r
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.equivLaxMonoidalFunctorPUnit_unitIso_hom_app_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (X : CategoryTheory.LaxMonoidalFunctor (CategoryTheory.Discrete PUnit.{w + 1}) C)
  (X_1 : CategoryTheory.Discrete PUnit.{w + 1}),
  (CategoryTheory.AddMon.equivLaxMonoidalFunctorPUnit.unitIso.hom.app X).hom.app X_1 =
    CategoryTheory.CategoryStruct.id (X.obj X_1)
-- Mathlib.Topology.TietzeExtension
Pi.instTietzeExtension : ∀ {ι : Type u_1} {Y : ι → Type v} [inst : (i : ι) → TopologicalSpace (Y i)] [∀ (i : ι), TietzeExtension (Y i)],
  TietzeExtension ((i : ι) → Y i)
-- Mathlib.Algebra.Lie.NonUnitalNonAssocAlgebra
LieAlgebra.instInhabitedCommutatorRing : (L : Type v) → [Inhabited L] → Inhabited (CommutatorRing L)
-- Std.Data.DTreeMap.Internal.Operations
/-- The tree.  -/
Std.DTreeMap.Internal.Impl.SizedBalancedTree.impl : {α : Type u} →
  {β : α → Type v} →
    {lb ub : ℕ} → Std.DTreeMap.Internal.Impl.SizedBalancedTree α β lb ub → Std.DTreeMap.Internal.Impl α β
-- Mathlib.Computability.TuringMachine.Config
/-- `zero` is the constant zero function: `zero v = [0]`.  -/
Turing.ToPartrec.Code.zero : Turing.ToPartrec.Code
-- Mathlib.AlgebraicTopology.DoldKan.Compatibility
AlgebraicTopology.DoldKan.Compatibility.equivalenceCounitIso_inv_app : ∀ {A : Type u_1} {B : Type u_3} {B' : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} B] [inst_2 : CategoryTheory.Category.{v_4, u_4} B'] {eB : B ≌ B'}
  {F : CategoryTheory.Functor A B'} {G : CategoryTheory.Functor B A} (η : G.comp F ≅ eB.functor) (X : B),
  (AlgebraicTopology.DoldKan.Compatibility.equivalenceCounitIso η).inv.app X =
    CategoryTheory.CategoryStruct.comp (eB.unitIso.hom.app X) (eB.inverse.map (η.inv.app X))
-- Init.Data.Nat.Lemmas
Nat.sub_lt_self : ∀ {a b : ℕ}, 0 < a → a ≤ b → b - a < b
-- Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
CategoryTheory.ObjectProperty.faithful_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C), P.ι.Faithful
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.getD_inter : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k fallback : α}, (t₁ ∩ t₂).getD k fallback = if k ∈ t₂ then t₁.getD k fallback else fallback
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.disjoint_vadd_set_right : ∀ {α : Type u_2} {β : Type u_3} [inst : AddGroup α] [inst_1 : AddAction α β] {s t : Set β} {a : α},
  Disjoint s (a +ᵥ t) ↔ Disjoint (-a +ᵥ s) t
-- Init.Data.Iterators.Basic
Std.Iter.mk : {α β : Type w} → α → Std.Iter β
-- Mathlib.Algebra.Category.Ring.Colimits
/-- The bundled ring giving the colimit of a diagram.  -/
RingCat.Colimits.colimit : {J : Type v} → [inst : CategoryTheory.SmallCategory J] → CategoryTheory.Functor J RingCat → RingCat
-- Init.Data.BitVec.Lemmas
BitVec.toNat_mod_cancel : ∀ {n : ℕ} (x : BitVec n), x.toNat % 2 ^ n = x.toNat
-- Mathlib.Order.Filter.Map
Filter.iSup_pure_eq_top : ∀ {α : Type u_1}, ⨆ a, pure a = ⊤
-- Mathlib.Probability.ProbabilityMassFunction.Basic
PMF.tsum_coe_indicator_ne_top : ∀ {α : Type u_1} (p : PMF α) (s : Set α), ∑' (a : α), s.indicator (⇑p) a ≠ ⊤
-- Mathlib.GroupTheory.MonoidLocalization.Maps
AddSubmonoid.LocalizationMap.map_surjective_of_surjOn : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N] {P : Type u_3}
  [inst_2 : AddCommMonoid P] (f : S.LocalizationMap N) {g : M →+ P} {T : AddSubmonoid P} (hy : ∀ (y : ↥S), g ↑y ∈ T)
  {Q : Type u_4} [inst_3 : AddCommMonoid Q] {k : T.LocalizationMap Q},
  Set.SurjOn ⇑g ↑S ↑T → Function.Surjective ⇑g → Function.Surjective ⇑(f.map hy k)
-- Mathlib.Order.Heyting.Regular
Heyting.Regular.coe_inj : ∀ {α : Type u_1} [inst : HeytingAlgebra α] {a b : Heyting.Regular α}, ↑a = ↑b ↔ a = b
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRoot.mk.sizeOf_spec : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] {f : Polynomial R}
  [inst_3 : SizeOf R] [inst_4 : SizeOf S] (map : Polynomial R →ₐ[R] S) (map_surjective : Function.Surjective ⇑map)
  (ker_map : RingHom.ker map = Ideal.span {f}),
  sizeOf { map := map, map_surjective := map_surjective, ker_map := ker_map } = 1 + sizeOf map + sizeOf ker_map
-- Mathlib.CategoryTheory.Monad.Monadicity
/-- Typeclass expressing that for all reflexive pairs `f,g`, `G` preserves colimits of
`parallelPair f g`.  -/
CategoryTheory.Monad.PreservesColimitOfIsReflexivePair : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₁, u₂} D] → CategoryTheory.Functor C D → Prop
-- Mathlib.FieldTheory.SplittingField.Construction
/-- Auxiliary construction to a splitting field of a polynomial, which removes
`n` (arbitrarily-chosen) factors. It is the type constructed in `SplittingFieldAuxAux`.
 -/
Polynomial.SplittingFieldAux : ℕ → {K : Type u} → [inst : Field K] → Polynomial K → Type u
-- Lean.Meta.Tactic.Grind.Main
Lean.Meta.Grind.Result.splitDiags : Lean.Meta.Grind.Result → Lean.PArray Lean.Meta.Grind.SplitDiagInfo
-- Mathlib.CategoryTheory.Limits.ExactFunctor
/-- Exactness, as a property of objects in `C ⥤ D`.  -/
CategoryTheory.exactFunctor : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (D : Type u₂) →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.ObjectProperty (CategoryTheory.Functor C D)
-- Mathlib.Tactic.Order.Graph.Basic
Mathlib.Tactic.Order.Graph.DFSState.mk : Std.HashSet ℕ → Mathlib.Tactic.Order.Graph.DFSState
-- Mathlib.Algebra.Module.Submodule.LinearMap
LinearMap.restrict.congr_simp : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  (f f_1 : M →ₛₗ[σ₁₂] M₂) (e_f : f = f_1) {p : Submodule R M} {q : Submodule R₂ M₂} (hf : ∀ x ∈ p, f x ∈ q),
  f.restrict hf = f_1.restrict ⋯
-- Mathlib.CategoryTheory.Category.TwoP
pointedToTwoPFst_obj_X : ∀ (X : Pointed), (pointedToTwoPFst.obj X).X = Option X.X
-- Mathlib.Order.Heyting.Basic
sdiff_sdiff_comm : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] {a b c : α}, (a \ b) \ c = (a \ c) \ b
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.SavedContext.options : Lean.Elab.Term.SavedContext → Lean.Options
-- Mathlib.CategoryTheory.ObjectProperty.Small
CategoryTheory.ObjectProperty.instSmallOfObjOfSmall : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type u_1} (X : ι → C) [Small.{w, u_1} ι],
  CategoryTheory.ObjectProperty.Small.{w, v, u} (CategoryTheory.ObjectProperty.ofObj X)
-- Mathlib.Control.Functor
Functor.Comp.functor : {F : Type u → Type w} → {G : Type v → Type u} → [Functor F] → [Functor G] → Functor (Functor.Comp F G)
-- Mathlib.Probability.HasLaw
ProbabilityTheory.HasLaw.variance_eq : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {μ : MeasureTheory.Measure ℝ} {X : Ω → ℝ},
  ProbabilityTheory.HasLaw X μ P → ProbabilityTheory.variance X P = ProbabilityTheory.variance id μ
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.PrettyPrinter.Delaborator.TopDownAnalyze.checkpointDefEq : Lean.Expr → Lean.Expr → Lean.MetaM Bool
-- Mathlib.NumberTheory.Harmonic.ZetaAsymp
ZetaAsymptotics.tendsto_riemannZeta_sub_one_div_Gammaℝ : Filter.Tendsto (fun s => riemannZeta s - 1 / s.Gammaℝ / (s - 1)) (nhdsWithin 1 {1}ᶜ)
  (nhds ((↑Real.eulerMascheroniConstant - Complex.log (4 * ↑Real.pi)) / 2))
-- Mathlib.Combinatorics.HalesJewett
Combinatorics.Line.diagonal.eq_1 : ∀ (α : Type u_5) (ι : Type u_6) [inst : Nonempty ι],
  Combinatorics.Line.diagonal α ι = { idxFun := fun x => none, proper := ⋯ }
-- Init.Data.Rat.Lemmas
Rat.lt_div_iff' : ∀ {a b c : ℚ}, 0 < c → (a < b / c ↔ c * a < b)
-- Mathlib.Data.ENNReal.Operations
ENNReal.top_mul : ∀ {a : ENNReal}, a ≠ 0 → ⊤ * a = ⊤
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Continuous.log : ∀ {α : Type u_1} [inst : TopologicalSpace α] {f : α → ℝ},
  Continuous f → (∀ (x : α), f x ≠ 0) → Continuous fun x => Real.log (f x)
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.iUnion_div_left_image : ∀ {α : Type u_2} [inst : Div α] {s t : Set α}, ⋃ a ∈ s, (fun x => a / x) '' t = s / t
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.le_maxKeyD_of_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α},
  k ∈ t → ∀ {fallback : α}, (cmp k (t.maxKeyD fallback)).isLE = true
-- Mathlib.GroupTheory.OrderOfElement
IsOfFinOrder.pow_eq_pow_iff_modEq : ∀ {G : Type u_1} [inst : Monoid G] {x : G} {n m : ℕ}, IsOfFinOrder x → (x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x])
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getKeyD_unitOfList_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {l : List α} {k k' fallback : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l →
      k ∈ l → (Std.ExtDTreeMap.Const.unitOfList l cmp).getKeyD k' fallback = k
-- Mathlib.CategoryTheory.Bicategory.Extension
CategoryTheory.Bicategory.LeftLift.whiskerHom_right : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a}
  {s t : CategoryTheory.Bicategory.LeftLift f g} (i : s ⟶ t) {x : B} (h : x ⟶ c),
  (CategoryTheory.Bicategory.LeftLift.whiskerHom i h).right =
    CategoryTheory.Bicategory.whiskerLeft h (CategoryTheory.StructuredArrow.Hom.right i)
-- Mathlib.Analysis.Analytic.Constructions
AnalyticWithinAt.curry_right : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} {G : Type u_5}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E × F → G} {s : Set (E × F)} {p : E × F},
  AnalyticWithinAt 𝕜 f s p → AnalyticWithinAt 𝕜 (fun y => f (p.1, y)) {y | (p.1, y) ∈ s} p.2
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.Pre.mul.sizeOf_spec : ∀ {R : Type u_1} {X : Type u_2} [inst : SizeOf R] [inst_1 : SizeOf X] (a a_1 : FreeAlgebra.Pre R X),
  sizeOf (a.mul a_1) = 1 + sizeOf a + sizeOf a_1
-- Mathlib.CategoryTheory.Triangulated.Opposite.OpOp
CategoryTheory.Pretriangulated.Opposite.instCommShiftOppositeUnopUnopInt : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.HasShift C ℤ] → (CategoryTheory.unopUnop C).CommShift ℤ
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
/-- The signed measure associated with a Jordan decomposition.  -/
MeasureTheory.JordanDecomposition.toSignedMeasure : {α : Type u_1} → [inst : MeasurableSpace α] → MeasureTheory.JordanDecomposition α → MeasureTheory.SignedMeasure α
-- Init.Data.Int.Gcd
Int.gcd_mul_left_add_right : ∀ (m n k : ℤ), m.gcd (m * k + n) = m.gcd n
-- Mathlib.Logic.Equiv.Basic
Equiv.Perm.sumCongr_refl_swap : ∀ {α : Type u_9} {β : Type u_10} [inst : DecidableEq α] [inst_1 : DecidableEq β] (i j : β),
  Equiv.Perm.sumCongr (Equiv.refl α) (Equiv.swap i j) = Equiv.swap (Sum.inr i) (Sum.inr j)
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.whiskeringEquivalence_unitIso : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (e : K ≌ J),
  (CategoryTheory.Limits.Cone.whiskeringEquivalence e).unitIso =
    CategoryTheory.NatIso.ofComponents
      (fun s =>
        CategoryTheory.Limits.Cone.ext
          (CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.Limits.Cone F)).obj s).pt) ⋯)
      ⋯
-- Mathlib.CategoryTheory.Abelian.Basic
/-- A preadditive category `C` with finite products is abelian when this
structure is nonempty for any morphism `f` in `C`, see `Abelian.mk'`.  -/
CategoryTheory.Abelian.AbelianStruct : {C : Type u_1} →
  [inst : CategoryTheory.Category.{u_2, u_1} C] →
    [CategoryTheory.Preadditive C] → {X Y : C} → (X ⟶ Y) → Type (max u_1 u_2)
-- Mathlib.Topology.Neighborhoods
IsClosed.mem_of_frequently_of_tendsto : ∀ {X : Type u} [inst : TopologicalSpace X] {α : Type u_1} {x : X} {s : Set X} {f : α → X} {b : Filter α},
  IsClosed s → (∃ᶠ (x : α) in b, f x ∈ s) → Filter.Tendsto f b (nhds x) → x ∈ s
-- Mathlib.GroupTheory.Coset.Basic
RightCosetEquivalence.eq_1 : ∀ {α : Type u_1} [inst : Mul α] (s : Set α) (a b : α),
  RightCosetEquivalence s a b = (MulOpposite.op a • s = MulOpposite.op b • s)
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.Prod.symmetry_inv_app : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (X : C × D), (CategoryTheory.Prod.symmetry C D).inv.app X = CategoryTheory.CategoryStruct.id X
-- Mathlib.Algebra.Homology.HomologicalBicomplex
HomologicalComplex₂.flipEquivalence_counitIso : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {I₁ : Type u_2} {I₂ : Type u_3} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂),
  (HomologicalComplex₂.flipEquivalence C c₁ c₂).counitIso = HomologicalComplex₂.flipEquivalenceCounitIso C c₁ c₂
-- Mathlib.Order.Concept
Concept.intent_max : ∀ {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (c d : Concept α β r), (c ⊔ d).intent = c.intent ∩ d.intent
-- Batteries.Data.List.Lemmas
List.dropInfix?_go_eq_some_iff : ∀ {α : Type u_1} [inst : BEq α] {i l acc p s : List α},
  List.dropInfix?.go i l acc = some (p, s) ↔
    ∃ p',
      p = acc.reverse ++ p' ∧
        (∃ i', l = p' ++ i' ++ s ∧ (i' == i) = true) ∧
          ∀ (p'' i'' s'' : List α), l = p'' ++ i'' ++ s'' → (i'' == i) = true → p''.length ≥ p'.length
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineSubspace.equivMapOfInjective_toFun : ∀ {𝕜 : Type u_1} {V₁ : Type u_3} {V₂ : Type u_5} {P₁ : Type u_8} {P₂ : Type u_11} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V₁] [inst_2 : NormedSpace 𝕜 V₁] [inst_3 : PseudoMetricSpace P₁]
  [inst_4 : NormedAddTorsor V₁ P₁] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂] (E : AffineSubspace 𝕜 P₁) [inst_9 : Nonempty ↥E]
  (φ : P₁ →ᵃ[𝕜] P₂) (hφ : Function.Injective ⇑φ) (p : ↑↑E), (E.equivMapOfInjective φ hφ) p = ⟨φ ↑p, ⋯⟩
-- Init.Data.String.Iterate
_private.Init.Data.String.Iterate.0.String.Slice.RevByteIterator.finitenessRelation : {m : Type → Type u_1} → [inst : Pure m] → Std.Iterators.FinitenessRelation String.Slice.RevByteIterator m
-- Mathlib.NumberTheory.NumberField.Units.Regulator
NumberField.Units.basisOfIsMaxRank.eq_1 : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K]
  {u : Fin (NumberField.Units.rank K) → (NumberField.RingOfIntegers K)ˣ} (hu : NumberField.Units.IsMaxRank u),
  NumberField.Units.basisOfIsMaxRank hu =
    (basisOfPiSpaceOfLinearIndependent ⋯).reindex (NumberField.Units.equivFinRank K).symm
-- Mathlib.MeasureTheory.PiSystem
isPiSystem_Icc : ∀ {α : Type u_1} {ι : Sort u_3} {ι' : Sort u_4} [inst : LinearOrder α] (f : ι → α) (g : ι' → α),
  IsPiSystem {S | ∃ i j, f i ≤ g j ∧ Set.Icc (f i) (g j) = S}
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
/-- An `IsPullback` square yields an isomorphism `Over.mk fst ≅ Over.mk (pullback.fst f g)`
in `Over X`.  -/
CategoryTheory.IsPullback.isoOverPullback : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y Z : C} →
      {f : X ⟶ Z} →
        {g : Y ⟶ Z} →
          [inst_1 : CategoryTheory.Limits.HasPullbacksAlong g] →
            {P : C} →
              {fst : P ⟶ X} →
                {snd : P ⟶ Y} →
                  CategoryTheory.IsPullback fst snd f g →
                    (CategoryTheory.Over.mk fst ≅ CategoryTheory.Over.mk (CategoryTheory.Limits.pullback.fst f g))
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.snd_map : ∀ {B : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} B] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T)
  (R : CategoryTheory.Functor B T) {Y X : CategoryTheory.Comma L R} (f : Y ⟶ X),
  (CategoryTheory.Comma.snd L R).map f = f.right
-- Mathlib.Geometry.Euclidean.Circumcenter
Affine.Simplex.PointsWithCircumcenterIndex.pointIndex.inj : ∀ {n : ℕ} {a a_1 : Fin (n + 1)},
  Affine.Simplex.PointsWithCircumcenterIndex.pointIndex a = Affine.Simplex.PointsWithCircumcenterIndex.pointIndex a_1 →
    a = a_1
-- Mathlib.Data.Nat.Digits.Defs
Nat.digits_eq_cons_digits_div : ∀ {b n : ℕ}, 1 < b → n ≠ 0 → b.digits n = n % b :: b.digits (n / b)
-- Mathlib.Data.Int.Cast.Lemmas
/-- If `α` is commutative, `zmultiplesHom` is an additive equivalence.  -/
zmultiplesAddHom : (β : Type u_4) → [inst : AddCommGroup β] → β ≃+ (ℤ →+ β)
-- Mathlib.Data.Matrix.Diagonal
Matrix.diagonal.eq_1 : ∀ {n : Type u_3} {α : Type v} [inst : DecidableEq n] [inst_1 : Zero α] (d : n → α),
  Matrix.diagonal d = Matrix.of fun i j => if i = j then d i else 0
-- Init.Prelude
_private.Init.Prelude.0.Lean.Syntax.getTailPos?.loop : Bool → Array Lean.Syntax → ℕ → Option String.Pos.Raw
-- Mathlib.Order.SymmDiff
Codisjoint.bihimp_left : ∀ {α : Type u_2} [inst : BooleanAlgebra α] {a b c : α}, Codisjoint a c → Codisjoint b c → Codisjoint (bihimp a b) c
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.Splits.eval_eq_prod_roots : ∀ {R : Type u_1} [inst : CommRing R] {f : Polynomial R} [inst_1 : IsDomain R],
  f.Splits → ∀ (x : R), Polynomial.eval x f = f.leadingCoeff * (Multiset.map (fun x_1 => x - x_1) f.roots).prod
-- Mathlib.Data.Part
Part.left_dom_of_sdiff_dom : ∀ {α : Type u_1} [inst : SDiff α] {a b : Part α}, (a \ b).Dom → a.Dom
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHom.instDistribMulAction : {M : Type u_2} →
  {α : Type u_5} →
    [inst : NonUnitalNonAssocSemiring α] →
      [inst_1 : Monoid M] →
        [inst_2 : DistribMulAction M α] →
          [SMulCommClass M α α] → [IsScalarTower M α α] → DistribMulAction M (CentroidHom α)
-- Mathlib.Logic.Small.Defs
/-- An arbitrarily chosen model in `Type w` for a `w`-small type.
 -/
Shrink : (α : Type v) → [Small.{w, v} α] → Type w