mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.pushforward_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} (f : Y ⟶ X) (R : CategoryTheory.Presieve Y)
  (g : X ⟶ Z),
  CategoryTheory.Presieve.pushforward (CategoryTheory.CategoryStruct.comp f g) R =
    CategoryTheory.Presieve.pushforward g (CategoryTheory.Presieve.pushforward f R)
-- Mathlib.Analysis.Real.Sqrt
Real.sqrt_pos : ∀ {x : ℝ}, 0 < √x ↔ 0 < x
-- Init.Data.Array.Zip
Array.zipWith_map_left : ∀ {α : Type u_1} {β : Type u_2} {α' : Type u_3} {γ : Type u_4} {as : Array α} {bs : Array β} {f : α → α'}
  {g : α' → β → γ}, Array.zipWith g (Array.map f as) bs = Array.zipWith (fun a b => g (f a) b) as bs
-- Mathlib.RingTheory.WittVector.Truncated
TruncatedWittVector.instNeg : (p n : ℕ) → (R : Type u_1) → [CommRing R] → [Fact (Nat.Prime p)] → Neg (TruncatedWittVector p n R)
-- Mathlib.Analysis.SpecialFunctions.Pow.Continuity
ContinuousOn.cpow_const : ∀ {α : Type u_1} [inst : TopologicalSpace α] {f : α → ℂ} {s : Set α} {b : ℂ},
  ContinuousOn f s → (∀ a ∈ s, f a ∈ Complex.slitPlane) → ContinuousOn (fun x => f x ^ b) s
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instNonUnitalNonAssocSemiringOfNonUnitalRingHomClass : {ι : 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 ι] →
                [Nonempty ι] →
                  [inst_5 : (i : ι) → NonUnitalNonAssocSemiring (G i)] →
                    [∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)] →
                      NonUnitalNonAssocSemiring (DirectLimit G f)
-- Mathlib.LinearAlgebra.Projectivization.Independence
/-- Independence is the negation of dependence.  -/
Projectivization.independent_iff_not_dependent : ∀ {ι : Type u_1} {K : Type u_2} {V : Type u_3} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  {f : ι → Projectivization K V}, Projectivization.Independent f ↔ ¬Projectivization.Dependent f
-- Mathlib.CategoryTheory.Sites.Point.Map
CategoryTheory.GrothendieckTopology.Point.presheafFiberMapIso_inv_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) (F : CategoryTheory.Functor C D)
  (K : CategoryTheory.GrothendieckTopology D) [inst_2 : F.IsCocontinuous J K]
  [inst_3 : CategoryTheory.LocallySmall.{w, v', u'} D] (A : Type u'') [inst_4 : CategoryTheory.Category.{v'', u''} A]
  [inst_5 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} A] (X : CategoryTheory.Functor Dᵒᵖ A),
  (Φ.presheafFiberMapIso F K A).inv.app X = (Φ.presheafFiberMapObjIso F K X).inv
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
/-- A Grothendieck abelian category has enough injectives.  -/
CategoryTheory.IsGrothendieckAbelian.enoughInjectives : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [CategoryTheory.IsGrothendieckAbelian.{w, v, u} C], CategoryTheory.EnoughInjectives C
-- Mathlib.CategoryTheory.Iso
CategoryTheory.Iso.self_symm_id_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (α : X ≅ Y) (β : X ≅ Z), α ≪≫ α.symm ≪≫ β = β
-- Mathlib.Data.NNReal.Defs
NNReal.instIsStrictOrderedRing : IsStrictOrderedRing NNReal
-- Mathlib.CategoryTheory.Limits.Shapes.Diagonal
/-- Given the following diagram with `S ⟶ S'` a monomorphism,

```
    X ⟶ X'
      ↘      ↘
        S ⟶ S'
      ↗      ↗
    Y ⟶ Y'
```

This iso witnesses the fact that

```
      X ×[S] Y ⟶ (X' ×[S'] Y') ×[Y'] Y
          |                  |
          |                  |
          ↓                  ↓
(X' ×[S'] Y') ×[X'] X ⟶ X' ×[S'] Y'
```

is a pullback square. The diagonal map of this square is `pullback.map`.
Also see `pullback_lift_map_is_pullback`.
 -/
CategoryTheory.Limits.pullbackFstFstIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasPullbacks C] →
      {X Y S X' Y' S' : C} →
        (f : X ⟶ S) →
          (g : Y ⟶ S) →
            (f' : X' ⟶ S') →
              (g' : Y' ⟶ S') →
                (i₁ : X ⟶ X') →
                  (i₂ : Y ⟶ Y') →
                    (i₃ : S ⟶ S') →
                      CategoryTheory.CategoryStruct.comp f i₃ = CategoryTheory.CategoryStruct.comp i₁ f' →
                        CategoryTheory.CategoryStruct.comp g i₃ = CategoryTheory.CategoryStruct.comp i₂ g' →
                          [CategoryTheory.Mono i₃] →
                            CategoryTheory.Limits.pullback
                                (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst f' g') i₁)
                                (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.snd f' g') i₂) ≅
                              CategoryTheory.Limits.pullback f g
-- Mathlib.ModelTheory.Basic
/-- A first-order equivalence is also a first-order embedding.  -/
FirstOrder.Language.Equiv.toEmbedding : {L : FirstOrder.Language} →
  {M : Type w} → {N : Type w'} → [inst : L.Structure M] → [inst_1 : L.Structure N] → L.Equiv M N → L.Embedding M N
-- Init.Prelude
/-- The power operation on natural numbers, usually accessed via the `^` operator.

This function is overridden in both the kernel and the compiler to efficiently evaluate using the
arbitrary-precision arithmetic library. The definition provided here is the logical model.
 -/
Nat.pow : ℕ → ℕ → ℕ
-- Mathlib.CategoryTheory.ComposableArrows.Basic
/-- Auxiliary definition for the action on maps of the functor `F.precomp f`.
It sends `0 ≤ 1` to `f` and `i + 1 ≤ j + 1` to `F.map' i j`.  -/
CategoryTheory.ComposableArrows.Precomp.map : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {n : ℕ} →
      (F : CategoryTheory.ComposableArrows C n) →
        {X : C} →
          (X ⟶ F.left) →
            (i j : Fin (n + 1 + 1)) →
              i ≤ j →
                (CategoryTheory.ComposableArrows.Precomp.obj F X i ⟶ CategoryTheory.ComposableArrows.Precomp.obj F X j)
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.RoiSlice : (α : Type u_1) → Type u_2 → [Ord α] → Type (max u_2 u_1)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.ofList_equiv_foldl : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {l : List ((a : α) × β a)},
  (Std.DHashMap.ofList l).Equiv (List.foldl (fun acc p => acc.insert p.fst p.snd) ∅ l)
-- Init.ShareCommon
ShareCommon.Object.hash : ShareCommon.Object → UInt64
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
/-- Multiplication action of `SL(2, ℤ)` on `GL(2, ℝ)⁺`.  -/
ModularGroup.SLOnGLPos : SMul (Matrix.SpecialLinearGroup (Fin 2) ℤ) ↥(Matrix.GLPos (Fin 2) ℝ)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.mk_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : D} {Y : C} {T : CategoryTheory.Functor C D} (f : S ⟶ T.obj Y), (CategoryTheory.StructuredArrow.mk f).right = Y
-- Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.constr_range : ∀ {M' : Type u_7} [inst : AddCommMonoid M'] {ι : Type u_10} {R : Type u_11} {M : Type u_12} [inst_1 : Semiring R]
  [inst_2 : AddCommMonoid M] [inst_3 : Module R M] (b : Module.Basis ι R M) [inst_4 : Module R M'] (S : Type u_13)
  [inst_5 : Semiring S] [inst_6 : Module S M'] [inst_7 : SMulCommClass R S M'] {f : ι → M'},
  ((b.constr S) f).range = Submodule.span R (Set.range f)
-- Lean.Meta.Sym.DSimp.DSimpM
Lean.Meta.Sym.DSimp.instInhabitedConfig.default : Lean.Meta.Sym.DSimp.Config
-- Init.Data.BitVec.Lemmas
BitVec.and_or_distrib_right : ∀ {w : ℕ} {x y z : BitVec w}, (x ||| y) &&& z = x &&& z ||| y &&& z
-- Mathlib.Condensed.Discrete.Module
/-- `CondensedMod.LocallyConstant.functor` is fully faithful.
 -/
CondensedMod.LocallyConstant.fullyFaithfulFunctor : (R : Type (u + 1)) → [inst : Ring R] → (CondensedMod.LocallyConstant.functor R).FullyFaithful
-- Mathlib.MeasureTheory.Measure.Map
MeasureTheory.Measure.mapₗ_ne_zero_iff : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α}
  {f : α → β}, Measurable f → ((MeasureTheory.Measure.mapₗ f) μ ≠ 0 ↔ μ ≠ 0)
-- Mathlib.Algebra.Star.MonoidHom
StarMulEquiv.ofBijective_apply : ∀ {A : Type u_2} {B : Type u_3} [inst : Monoid A] [inst_1 : Monoid B] [inst_2 : Star A] [inst_3 : Star B] {f : A →⋆* B}
  (hf : Function.Bijective ⇑f) (a : A), (StarMulEquiv.ofBijective f hf) a = f a
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
/-- The `SubMulAction` of `fixingSubgroup M s` on the complement of `s`.  -/
SubMulAction.ofFixingSubgroup : (M : Type u_1) →
  {α : Type u_2} → [inst : Group M] → [inst_1 : MulAction M α] → (s : Set α) → SubMulAction (↥(fixingSubgroup M s)) α
-- Mathlib.Topology.MetricSpace.HausdorffDistance
Metric.hausdorffEDist_def : ∀ {α : Type u_2} [inst : PseudoEMetricSpace α] (s t : Set α),
  Metric.hausdorffEDist s t = max (⨆ x ∈ s, Metric.infEDist x t) (⨆ y ∈ t, Metric.infEDist y s)
-- Mathlib.CategoryTheory.EpiMono
/-- Every iso is a split epi.  -/
CategoryTheory.IsSplitEpi.of_iso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.IsIso f],
  CategoryTheory.IsSplitEpi f
-- Mathlib.Algebra.Lie.Abelian
LieAlgebra.center_eq_bot : ∀ (R : Type u) (L : Type v) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [LieModule.IsFaithful R L L], LieAlgebra.center R L = ⊥
-- Mathlib.Order.BooleanAlgebra.Basic
compl_le_compl_iff_le : ∀ {α : Type u} {x y : α} [inst : BooleanAlgebra α], yᶜ ≤ xᶜ ↔ x ≤ y
-- Mathlib.CategoryTheory.Bicategory.LocallyGroupoid
/-- The inv direction of the (strong) natural isomorphism of pseudofunctors
between `(pseudofunctorToPith F).comp (inclusion B)` and `F`.  -/
CategoryTheory.Bicategory.Pith.pseudofunctorToPithCompInclusionStrongIsoInv : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {B' : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory B'] →
        [inst_2 : CategoryTheory.Bicategory.IsLocallyGroupoid B'] →
          (F : CategoryTheory.Pseudofunctor B' B) →
            F.StrongTrans
              ((CategoryTheory.Bicategory.Pith.pseudofunctorToPith F).comp (CategoryTheory.Bicategory.Pith.inclusion B))
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring
HomogeneousSubsemiring.mk.inj : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} {inst : AddMonoid ι} {inst_1 : Semiring A} {inst_2 : SetLike σ A}
  {inst_3 : AddSubmonoidClass σ A} {𝒜 : ι → σ} {inst_4 : DecidableEq ι} {inst_5 : GradedRing 𝒜}
  {toSubsemiring : Subsemiring A} {is_homogeneous' : DirectSum.SetLike.IsHomogeneous 𝒜 toSubsemiring}
  {toSubsemiring_1 : Subsemiring A} {is_homogeneous'_1 : DirectSum.SetLike.IsHomogeneous 𝒜 toSubsemiring_1},
  { toSubsemiring := toSubsemiring, is_homogeneous' := is_homogeneous' } =
      { toSubsemiring := toSubsemiring_1, is_homogeneous' := is_homogeneous'_1 } →
    toSubsemiring = toSubsemiring_1
-- Mathlib.Tactic.GRewrite.Core
/-- Whether to use `kabstract` to find the rewrites locations.  -/
Mathlib.Tactic.GRewrite.Config.useKAbstract : Mathlib.Tactic.GRewrite.Config → Bool
-- Batteries.Data.List.Lemmas
List.chain_lt_range' : ∀ {step : ℕ} (s n : ℕ), 0 < step → List.IsChain (fun x1 x2 => x1 < x2) (s :: List.range' (s + step) n step)
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
CategoryTheory.Localization.Preadditive.add'_comm : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Preadditive C]
  {L : CategoryTheory.Functor C D} (W : CategoryTheory.MorphismProperty C) [inst_3 : L.IsLocalization W]
  [inst_4 : W.HasLeftCalculusOfFractions] {X Y : C} (f₁ f₂ : L.obj X ⟶ L.obj Y),
  CategoryTheory.Localization.Preadditive.add' W f₁ f₂ = CategoryTheory.Localization.Preadditive.add' W f₂ f₁
-- Mathlib.Algebra.GroupWithZero.Pi
Pi.mulZeroClass : {ι : Type u_1} → {α : ι → Type u_2} → [(i : ι) → MulZeroClass (α i)] → MulZeroClass ((i : ι) → α i)
-- Init.Data.Rat.Lemmas
Rat.den_pow : ∀ (q : ℚ) (n : ℕ), (q ^ n).den = q.den ^ n
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.sin_nonneg_of_mem_Icc : ∀ {x : ℝ}, x ∈ Set.Icc 0 Real.pi → 0 ≤ Real.sin x
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.ιE.eq_1 : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ)
  (hn₁ : n₀ + 1 = n₁) (hn₂ : n₁ + 1 = n₂),
  X.ιE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂ =
    CategoryTheory.CategoryStruct.comp (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).homologyι
      (X.opcyclesIso f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).hom
-- Mathlib.Algebra.Group.EvenFunction
Function.Odd.const_smul : ∀ {α : Type u_1} {β : Type u_2} [inst : Neg α] {γ : Type u_3} {g : α → γ} [inst_1 : Monoid β] [inst_2 : AddGroup γ]
  [inst_3 : DistribMulAction β γ], Function.Odd g → ∀ (r : β), Function.Odd (r • g)
-- Mathlib.GroupTheory.Perm.List
List.formPerm_eq_formPerm_iff : ∀ {α : Type u_1} [inst : DecidableEq α] {l l' : List α},
  l.Nodup → l'.Nodup → (l.formPerm = l'.formPerm ↔ l ~r l' ∨ l.length ≤ 1 ∧ l'.length ≤ 1)
-- Mathlib.CategoryTheory.Monoidal.Opposite.Mon
MonObj.mopEquiv_functor_obj_X_unmop : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (M : CategoryTheory.Mon C), ((MonObj.mopEquiv C).functor.obj M).X.unmop = M.X
-- Std.Tactic.Do.Syntax
/-- Theorems tagged with the `spec` attribute are used by the `mspec` and `mvcgen` tactics.

* When used on a theorem `foo_spec : Triple (foo a b c) P Q`, then `mspec` and `mvcgen` will use
  `foo_spec` as a specification for calls to `foo`.
* Otherwise, when used on a definition that `@[simp]` would work on, it is added to the internal
  simp set of `mvcgen` that is used within `wp⟦·⟧` contexts to simplify match discriminants and
  applications of constants.
 -/
Lean.Parser.Attr.spec : Lean.ParserDescr
-- Mathlib.Data.Set.Finite.Basic
Set.Finite.sep : ∀ {α : Type u} {s : Set α}, s.Finite → ∀ (p : α → Prop), {a | a ∈ s ∧ p a}.Finite
-- Mathlib.Algebra.Group.Units.Basic
IsAddUnit.add_left_injective : ∀ {M : Type u_1} [inst : AddMonoid M] {b : M}, IsAddUnit b → Function.Injective fun x => x + b
-- Mathlib.Topology.MetricSpace.Holder
/-- **Alias** of `convex_setOfPred_holderOnWith`.

---

For fixed `f : X → Y`, `A : Set X` and `C : ℝ≥0`, the set of all parameters `r : ℝ≥0` such that
`f` is `(C, r)`-Hölder on `A` is convex.  -/
convex_setOf_holderOnWith : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] (f : X → Y) (C : NNReal)
  (A : Set X), Convex NNReal {r | HolderOnWith C r f A}
-- Mathlib.Algebra.CharP.Frobenius
coe_iterateFrobenius : ∀ (R : Type u_1) [inst : CommSemiring R] (p n : ℕ) [inst_1 : ExpChar R p],
  ⇑(iterateFrobenius R p n) = (⇑(frobenius R p))^[n]
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
/-- **Alias** of `NumberField.HeightOneSpectrum.one_lt_absNorm`.

---

The norm of a maximal ideal is `> 1`  -/
NumberField.HeightOneSpectrum.NumberField.RingOfIntegers.HeightOneSpectrum.one_lt_absNorm : ∀ {R : Type u_2} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R)
  [Module.Finite ℤ R] [inst_3 : Module.Free ℤ R], 1 < Ideal.absNorm v.asIdeal
-- Mathlib.RingTheory.LocalRing.ResidueField.Basic
IsLocalRing.ResidueField.mapEquiv.symm : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : IsLocalRing R] [inst_2 : CommRing S]
  [inst_3 : IsLocalRing S] (f : R ≃+* S),
  (IsLocalRing.ResidueField.mapEquiv f).symm = IsLocalRing.ResidueField.mapEquiv f.symm
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
CategoryTheory.Bicategory.Equivalence.mk.injEq : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {a b : B} (hom : a ⟶ b) (inv : b ⟶ a)
  (unit : CategoryTheory.CategoryStruct.id a ≅ CategoryTheory.CategoryStruct.comp hom inv)
  (counit : CategoryTheory.CategoryStruct.comp inv hom ≅ CategoryTheory.CategoryStruct.id b)
  (left_triangle :
    autoParam
      (CategoryTheory.Bicategory.leftZigzagIso unit counit =
        CategoryTheory.Bicategory.leftUnitor hom ≪≫ (CategoryTheory.Bicategory.rightUnitor hom).symm)
      CategoryTheory.Bicategory.Equivalence.left_triangle._autoParam)
  (hom_1 : a ⟶ b) (inv_1 : b ⟶ a)
  (unit_1 : CategoryTheory.CategoryStruct.id a ≅ CategoryTheory.CategoryStruct.comp hom_1 inv_1)
  (counit_1 : CategoryTheory.CategoryStruct.comp inv_1 hom_1 ≅ CategoryTheory.CategoryStruct.id b)
  (left_triangle_1 :
    autoParam
      (CategoryTheory.Bicategory.leftZigzagIso unit_1 counit_1 =
        CategoryTheory.Bicategory.leftUnitor hom_1 ≪≫ (CategoryTheory.Bicategory.rightUnitor hom_1).symm)
      CategoryTheory.Bicategory.Equivalence.left_triangle._autoParam),
  ({ hom := hom, inv := inv, unit := unit, counit := counit, left_triangle := left_triangle } =
      { hom := hom_1, inv := inv_1, unit := unit_1, counit := counit_1, left_triangle := left_triangle_1 }) =
    (hom = hom_1 ∧ inv = inv_1 ∧ unit ≍ unit_1 ∧ counit ≍ counit_1)
-- Lean.Compiler.IR.Basic
Lean.IR.instInhabitedArg : Inhabited Lean.IR.Arg
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.instInvolutiveStar : {n : Type u_2} → {A : Type u_5} → [InvolutiveStar A] → InvolutiveStar (CStarMatrix n n A)
-- Mathlib.Topology.Instances.EReal.Lemmas
EReal.le_limsup_add : ∀ {α : Type u_3} {f : Filter α} {u v : α → EReal}, Filter.limsup u f + Filter.liminf v f ≤ Filter.limsup (u + v) f
-- Mathlib.Analysis.Analytic.ChangeOrigin
/-- The radius of convergence of `p.changeOrigin x` is at least `p.radius - ‖x‖`. In other words,
`p.changeOrigin x` is well defined on the largest ball contained in the original ball of
convergence.  -/
FormalMultilinearSeries.changeOrigin_radius : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  (p : FormalMultilinearSeries 𝕜 E F) {x : E}, p.radius - ↑‖x‖₊ ≤ (p.changeOrigin x).radius
-- Mathlib.Algebra.Homology.CommSq
CategoryTheory.Limits.KernelFork.ofι.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  {f : X ⟶ Y} {Z : C} (ι ι_1 : Z ⟶ X) (e_ι : ι = ι_1) (w : CategoryTheory.CategoryStruct.comp ι f = 0),
  CategoryTheory.Limits.KernelFork.ofι ι w = CategoryTheory.Limits.KernelFork.ofι ι_1 ⋯
-- Mathlib.Analysis.InnerProductSpace.Defs
/-- Seminormed group structure constructed from a `PreInnerProductSpace.Core` structure  -/
InnerProductSpace.Core.toSeminormedAddCommGroup : {𝕜 : Type u_1} →
  {F : Type u_3} →
    [inst : RCLike 𝕜] →
      [inst_1 : AddCommGroup F] → [inst_2 : Module 𝕜 F] → [c : PreInnerProductSpace.Core 𝕜 F] → SeminormedAddCommGroup F
-- Mathlib.LinearAlgebra.PerfectPairing.Basic
/-- If the coefficients are a field, and one of the spaces is finite-dimensional, it is sufficient
to check only injectivity instead of bijectivity of the bilinear pairing.  -/
LinearMap.IsPerfPair.of_injective : ∀ {K : Type u_2} {M : Type u_3} {N : Type u_5} [inst : AddCommGroup M] [inst_1 : AddCommGroup N] [inst_2 : Field K]
  [inst_3 : Module K M] [inst_4 : Module K N] {p : M →ₗ[K] N →ₗ[K] K} [FiniteDimensional K M],
  Function.Injective ⇑p → Function.Injective ⇑p.flip → p.IsPerfPair
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic
SSet.innerAnodyneExtensions_le : SSet.innerAnodyneExtensions ≤ SSet.anodyneExtensions
-- Lean.Meta.Tactic.FunIndInfo
Lean.Meta.instReprFunIndParamKind.repr : Lean.Meta.FunIndParamKind → ℕ → Std.Format
-- Init.Data.List.Control
/-- Applies a monadic function that returns a list to each element of a list, from left to right, and
concatenates the resulting lists.
 -/
List.flatMapM : {m : Type u → Type v} → [Monad m] → {α : Type w} → {β : Type u} → (α → m (List β)) → List α → m (List β)
-- Mathlib.Geometry.RingedSpace.SheafedSpace
AlgebraicGeometry.SheafedSpace.coeCarrier : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CoeOut (AlgebraicGeometry.SheafedSpace C) TopCat
-- Lean.Server.Requests
Lean.Server.RequestError : Type
-- Mathlib.Combinatorics.Enumerative.Partition.GenFun
Nat.Partition.genFun_eq_tprod : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : TopologicalSpace R] [T2Space R] (f : ℕ → ℕ → R),
  Nat.Partition.genFun f = ∏' (i : ℕ), (1 + ∑' (j : ℕ), f (i + 1) (j + 1) • PowerSeries.X ^ ((i + 1) * (j + 1)))
-- Std.Sat.AIG.RelabelNat
Std.Sat.AIG.RelabelNat.State.Inv2.below.newAtom : ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Hashable α] {decls : Array (Std.Sat.AIG.Decl α)}
  {motive : (a : ℕ) → (a_1 : Std.HashMap α ℕ) → Std.Sat.AIG.RelabelNat.State.Inv2 decls a a_1 → Prop} {idx : ℕ}
  {map : Std.HashMap α ℕ} {a : α} {val : ℕ} (hinv : Std.Sat.AIG.RelabelNat.State.Inv2 decls idx map)
  (hlt : idx < decls.size) (hatom : decls[idx] = Std.Sat.AIG.Decl.atom a) (hmap : map[a]? = none),
  Std.Sat.AIG.RelabelNat.State.Inv2.below hinv → motive idx map hinv → Std.Sat.AIG.RelabelNat.State.Inv2.below ⋯
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
CategoryTheory.Oplax.OplaxTrans.StrongCore.mk.injEq : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} {η : F ⟶ G}
  (naturality :
    {a b : B} →
      (f : a ⟶ b) →
        CategoryTheory.CategoryStruct.comp (F.map f) (η.app b) ≅ CategoryTheory.CategoryStruct.comp (η.app a) (G.map f))
  (naturality_hom :
    autoParam (∀ {a b : B} (f : a ⟶ b), (naturality f).hom = η.naturality f)
      CategoryTheory.Oplax.OplaxTrans.StrongCore.naturality_hom._autoParam)
  (naturality_1 :
    {a b : B} →
      (f : a ⟶ b) →
        CategoryTheory.CategoryStruct.comp (F.map f) (η.app b) ≅ CategoryTheory.CategoryStruct.comp (η.app a) (G.map f))
  (naturality_hom_1 :
    autoParam (∀ {a b : B} (f : a ⟶ b), (naturality_1 f).hom = η.naturality f)
      CategoryTheory.Oplax.OplaxTrans.StrongCore.naturality_hom._autoParam),
  ({ naturality := naturality, naturality_hom := naturality_hom } =
      { naturality := naturality_1, naturality_hom := naturality_hom_1 }) =
    (naturality = naturality_1)
-- Mathlib.Data.Nat.Prime.Defs
Nat.decidablePrime_csimp : Nat.decidablePrime = Nat.decidablePrime'
-- Mathlib.RingTheory.Finiteness.Descent
RingHom.FiniteType.codescendsAlong_faithfullyFlat : RingHom.CodescendsAlong (fun {R S} [CommRing R] [CommRing S] => RingHom.FiniteType)
  fun {R S} [CommRing R] [CommRing S] => RingHom.FaithfullyFlat
-- Mathlib.AlgebraicGeometry.Birational.Birational
AlgebraicGeometry.Scheme.PartialIso.trans'_iso : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X.PartialIso Y) (g : Y.PartialIso Z) (e : f.target = g.source),
  (f.trans' g e).iso = f.iso ≪≫ Y.isoOfEq e ≪≫ g.iso
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.U_eval_zero_of_even : ∀ (R : Type u_1) [inst : CommRing R] {n : ℤ},
  Even n → Polynomial.eval 0 (Polynomial.Chebyshev.U R n) = ↑↑(n / 2).negOnePow
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.instInhabitedAlt.default_1 : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.Alt pu
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.cokernelCoforkBiproductFromSubtype_cocone : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {K : Type}
  [inst_2 : Finite K] [inst_3 : CategoryTheory.Limits.HasFiniteBiproducts C] (f : K → C) (p : K → Prop),
  (CategoryTheory.Limits.cokernelCoforkBiproductFromSubtype f p).cocone =
    CategoryTheory.Limits.CokernelCofork.ofπ (CategoryTheory.Limits.biproduct.toSubtype f pᶜ) ⋯