mathlib-initiative/mathlib-types huggingface dataset:
-- Batteries.Data.MLList.Basic
/-- Drop the first `n` elements.  -/
MLList.drop : {m : Type u_1 → Type u_1} → {α : Type u_1} → [Monad m] → MLList m α → ℕ → MLList m α
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- Convert a `NormalExpr` expression into a list of `WhiskerLeft` expressions.  -/
Mathlib.Tactic.BicategoryLike.NormalExpr.toList : Mathlib.Tactic.BicategoryLike.NormalExpr → List Mathlib.Tactic.BicategoryLike.WhiskerLeft
-- Mathlib.Order.Height
/-- The maximal length of a chain in a set `s` with relation `r`.  -/
Set.chainHeight : {α : Type u_1} → Set α → (α → α → Prop) → ℕ∞
-- Mathlib.Data.Bundle
Bundle.TotalSpace.ext_iff : ∀ {B : Type u_1} {F : Type u_4} {E : B → Type u_5} {x y : Bundle.TotalSpace F E},
  x = y ↔ x.proj = y.proj ∧ x.snd ≍ y.snd
-- Mathlib.Algebra.Free
FreeAddMagma.add_bind : ∀ {α β : Type u} (f : α → FreeAddMagma β) (x y : FreeAddMagma α), x + y >>= f = (x >>= f) + (y >>= f)
-- Mathlib.CategoryTheory.Abelian.Projective.Resolution
CategoryTheory.ProjectiveResolution.homotopyEquiv_inv_π : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X : C}
  (P Q : CategoryTheory.ProjectiveResolution X), CategoryTheory.CategoryStruct.comp (P.homotopyEquiv Q).inv P.π = Q.π
-- Mathlib.Algebra.Squarefree.Basic
squarefree_one : ∀ {R : Type u_1} [inst : CommMonoid R], Squarefree 1
-- Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
integral_gaussian_complex : ∀ {b : ℂ}, 0 < b.re → ∫ (x : ℝ), Complex.exp (-b * ↑x ^ 2) = (↑Real.pi / b) ^ (1 / 2)
-- Mathlib.CategoryTheory.Join.Pseudofunctor
CategoryTheory.Join.pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_α : ∀ (D : Type u₂) [inst : CategoryTheory.Category.{v₂, u₂} D] (C : CategoryTheory.Cat),
  ↑((CategoryTheory.Join.pseudofunctorLeft D).obj C) = CategoryTheory.Join (↑C) D
-- Lean.Server.Rpc.Basic
Lean.Lsp.RpcRef.mk.sizeOf_spec : ∀ (p : USize), sizeOf { p := p } = 1 + sizeOf p
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- If `X' ≅ X`, then `X ⨿ Y` also is the coproduct of `X'` and `Y`.  -/
CategoryTheory.Limits.BinaryCofan.isColimitCompLeftIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y X' : C} →
      (c : CategoryTheory.Limits.BinaryCofan X Y) →
        (f : X' ⟶ X) →
          [CategoryTheory.IsIso f] →
            CategoryTheory.Limits.IsColimit c →
              CategoryTheory.Limits.IsColimit
                (CategoryTheory.Limits.BinaryCofan.mk (CategoryTheory.CategoryStruct.comp f c.inl) c.inr)
-- Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
/-- If `W ≤ W'`, then transfinite compositions of shape `J` of morphisms in `W`
are also transfinite composition of shape `J` of morphisms in `W'`.  -/
CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofLE : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {W : CategoryTheory.MorphismProperty C} →
      {J : Type w} →
        [inst_1 : LinearOrder J] →
          [inst_2 : SuccOrder J] →
            [inst_3 : OrderBot J] →
              [inst_4 : WellFoundedLT J] →
                {X Y : C} →
                  {f : X ⟶ Y} →
                    W.TransfiniteCompositionOfShape J f →
                      {W' : CategoryTheory.MorphismProperty C} → W ≤ W' → W'.TransfiniteCompositionOfShape J f
-- Mathlib.LinearAlgebra.TensorProduct.Tower
TensorProduct.AlgebraTensorModule.cancelBaseChange_symm_tmul : ∀ (R : Type uR) (A : Type uA) (B : Type uB) {M : Type uM} {N : Type uN} [inst : CommSemiring R]
  [inst_1 : CommSemiring A] [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B]
  [inst_5 : AddCommMonoid M] [inst_6 : Module R M] [inst_7 : Module A M] [inst_8 : Module B M]
  [inst_9 : IsScalarTower R A M] [inst_10 : IsScalarTower R B M] [inst_11 : SMulCommClass A B M]
  [inst_12 : AddCommMonoid N] [inst_13 : Module R N] [inst_14 : Algebra A B] [inst_15 : IsScalarTower A B M] (m : M)
  (n : N), (TensorProduct.AlgebraTensorModule.cancelBaseChange R A B M N).symm (m ⊗ₜ[R] n) = m ⊗ₜ[A] (1 ⊗ₜ[R] n)
-- Mathlib.Analysis.Oscillation
/-- If `oscillationWithin f D x < ε` at every `x` in a compact set `K`, then there exists `δ > 0`
such that the oscillation of `f` on `ball x δ ∩ D` is less than `ε` for every `x` in `K`.  -/
IsCompact.uniform_oscillationWithin : ∀ {E : Type u} {F : Type v} [inst : PseudoEMetricSpace F] [inst_1 : PseudoEMetricSpace E] {K : Set E} {f : E → F}
  {D : Set E} {ε : ENNReal},
  IsCompact K →
    (∀ x ∈ K, oscillationWithin f D x < ε) →
      ∃ δ > 0, ∀ x ∈ K, Metric.ediam (f '' (Metric.eball x (ENNReal.ofReal δ) ∩ D)) ≤ ε
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.ExtensionState : Type
-- Mathlib.Analysis.Complex.Isometry
/-- The determinant of `rotation` (as a linear equiv) is equal to `1`.  -/
linearEquiv_det_rotation : ∀ (a : Circle), LinearEquiv.det (rotation a).toLinearEquiv = 1
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.Opens.isCompactElement_iff : ∀ {α : Type u_2} [inst : TopologicalSpace α] (s : TopologicalSpace.Opens α), IsCompactElement s ↔ IsCompact ↑s
-- Mathlib.NumberTheory.Modular
ModularGroup.fdo_eq_interior_fd : ModularGroup.fdo = interior ModularGroup.fd
-- Init.Data.List.Basic
/-- The first list is a prefix of the second.

`IsPrefix l₁ l₂`, written `l₁ <+: l₂`, means that there exists some `t : List α` such that `l₂` has
the form `l₁ ++ t`.

The function `List.isPrefixOf` is a Boolean equivalent.


Conventions for notations in identifiers:

 * The recommended spelling of `<+:` in identifiers is `prefix` (not `isPrefix`). -/
List.IsPrefix : {α : Type u} → List α → List α → Prop
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.toLinearMap_toContinuousLinearMap : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁}
  [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [inst_4 : TopologicalSpace M₁]
  [inst_5 : AddCommMonoid M₁] {M₂ : Type u_5} [inst_6 : TopologicalSpace M₂] [inst_7 : AddCommMonoid M₂]
  [inst_8 : Module R₁ M₁] [inst_9 : Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂), ↑↑e = ↑↑e
-- Mathlib.Combinatorics.Graph.Subgraph
/-- `H ≤s G` (`Graph.IsSpanningSubgraph`) is a subgraph of `G` with the same vertex set.  -/
Graph.«term_≤s_» : Lean.TrailingParserDescr
-- Lean.Data.Lsp.TextSync
Lean.Lsp.TextDocumentChangeRegistrationOptions.mk.inj : ∀ {documentSelector? : Option Lean.Lsp.DocumentSelector} {syncKind : Lean.Lsp.TextDocumentSyncKind}
  {documentSelector?_1 : Option Lean.Lsp.DocumentSelector} {syncKind_1 : Lean.Lsp.TextDocumentSyncKind},
  { documentSelector? := documentSelector?, syncKind := syncKind } =
      { documentSelector? := documentSelector?_1, syncKind := syncKind_1 } →
    documentSelector? = documentSelector?_1 ∧ syncKind = syncKind_1
-- Init.Data.List.Monadic
_private.Init.Data.List.Monadic.0.List.forIn'.loop.match_5.eq_1 : ∀ {α : Type u_1} {β : Type u_3} (as : List α) (motive : (x : List α) → β → (∃ bs, bs ++ x = as) → Sort u_2) (b : β)
  (x : ∃ bs, bs ++ [] = as) (h_1 : (b : β) → (x : ∃ bs, bs ++ [] = as) → motive [] b x)
  (h_2 : (a : α) → (as' : List α) → (b : β) → (h : ∃ bs, bs ++ a :: as' = as) → motive (a :: as') b h),
  (match [], b, x with
    | [], b, x => h_1 b x
    | a :: as', b, h => h_2 a as' b h) =
    h_1 b x
-- Qq.Macro
Qq.Impl.QuoteM : Type → Type
-- Mathlib.SetTheory.Ordinal.Exponential
Ordinal.log_eq_zero : ∀ {b o : Ordinal.{u_1}}, o < b → Ordinal.log b o = 0
-- Mathlib.NumberTheory.ModularForms.Discriminant
ModularForm.discriminant.eq_1 : ∀ (z : UpperHalfPlane), ModularForm.discriminant z = ModularForm.eta ↑z ^ 24
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
CategoryTheory.ChosenPullbacksAlong.unit_pullbackId_hom_app_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (X : C)
  [inst_1 : CategoryTheory.ChosenPullbacksAlong (CategoryTheory.CategoryStruct.id X)] (Y : CategoryTheory.Over X)
  {Z : CategoryTheory.Over X} (h : (CategoryTheory.Over.map (CategoryTheory.CategoryStruct.id X)).obj Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.ChosenPullbacksAlong.mapPullbackAdj (CategoryTheory.CategoryStruct.id X)).unit.app Y)
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.ChosenPullbacksAlong.pullbackId X).hom.app
          ((CategoryTheory.Over.map (CategoryTheory.CategoryStruct.id X)).obj Y))
        h) =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.ChosenPullbacksAlong.mapPullbackAdj (CategoryTheory.CategoryStruct.id X)).unit.app Y) h
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.instTypeNameElabLink : TypeName Lean.Doc.ElabLink✝
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
_private.Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula.0.termY : Lean.ParserDescr
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
CategoryTheory.Functor.pointwiseLeftKanExtensionCompIsoOfPreserves_hom_fac_app_assoc : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D] (G : CategoryTheory.Functor B D) (F : CategoryTheory.Functor A B)
  (L : CategoryTheory.Functor A C) [inst_4 : G.PreservesPointwiseLeftKanExtension F L]
  [inst_5 : L.HasPointwiseLeftKanExtension F] (a : A) {Z : D}
  (h : (L.pointwiseLeftKanExtension (F.comp G)).obj (L.obj a) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (G.map ((L.pointwiseLeftKanExtensionUnit F).app a))
      (CategoryTheory.CategoryStruct.comp ((G.pointwiseLeftKanExtensionCompIsoOfPreserves F L).hom.app (L.obj a)) h) =
    CategoryTheory.CategoryStruct.comp ((L.pointwiseLeftKanExtensionUnit (F.comp G)).app a) h
-- Init.Data.List.MapIdx
List.mapFinIdx.go.congr_simp : ∀ {α : Type u_1} {β : Type u_2} (as : List α) (f f_1 : (i : ℕ) → α → i < as.length → β),
  f = f_1 →
    ∀ (bs bs_1 : List α) (e_bs : bs = bs_1) (acc acc_1 : Array β) (e_acc : acc = acc_1)
      (a : bs.length + acc.size = as.length), List.mapFinIdx.go as f bs acc a = List.mapFinIdx.go as f_1 bs_1 acc_1 ⋯
-- Mathlib.CategoryTheory.Localization.Equivalence
/-- If `L₁ : C₁ ⥤ D` is a localization functor for `W₁ : MorphismProperty C₁`, then it is also
the case of a functor `L₂ : C₂ ⥤ D` for a suitable `W₂ : MorphismProperty C₂` when
we have an equivalence of category `E : C₁ ≌ C₂` and an isomorphism `E.functor ⋙ L₂ ≅ L₁`.  -/
CategoryTheory.Functor.IsLocalization.of_equivalence_source : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} D]
  (L₁ : CategoryTheory.Functor C₁ D) (W₁ : CategoryTheory.MorphismProperty C₁) (L₂ : CategoryTheory.Functor C₂ D)
  (W₂ : CategoryTheory.MorphismProperty C₂) (E : C₁ ≌ C₂),
  W₁ ≤ W₂.isoClosure.inverseImage E.functor →
    W₂.IsInvertedBy L₂ → ∀ [L₁.IsLocalization W₁] (iso : E.functor.comp L₂ ≅ L₁), L₂.IsLocalization W₂
-- Lean.Declaration
Lean.AxiomVal.mk.injEq : ∀ (toConstantVal : Lean.ConstantVal) (isUnsafe : Bool) (toConstantVal_1 : Lean.ConstantVal) (isUnsafe_1 : Bool),
  ({ toConstantVal := toConstantVal, isUnsafe := isUnsafe } =
      { toConstantVal := toConstantVal_1, isUnsafe := isUnsafe_1 }) =
    (toConstantVal = toConstantVal_1 ∧ isUnsafe = isUnsafe_1)
-- Mathlib.Algebra.Order.Floor.Ring
Int.ceil_congr : ∀ {R : Type u_2} {S : Type u_3} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : Ring S] [inst_3 : LinearOrder S]
  [inst_4 : FloorRing R] [inst_5 : FloorRing S] {a : R} {b : S}, (∀ (n : ℤ), a ≤ ↑n ↔ b ≤ ↑n) → ⌈a⌉ = ⌈b⌉
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.contains_of_contains_erase : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k a : α}, (t.erase k).contains a = true → t.contains a = true
-- Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
Diffeomorph.boundarylessManifold_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {N : Type u_7} [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace H' N] {n : WithTop ℕ∞},
  n ≠ 0 → ∀ (Φ : Diffeomorph I I' M N n), BoundarylessManifold I M ↔ BoundarylessManifold I' N
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
CategoryTheory.Pseudofunctor.DescentData'.isoMk_inv_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} {sq : (i j : ι) → CategoryTheory.Limits.ChosenPullback (f i) (f j)}
  {sq₃ : (i₁ i₂ i₃ : ι) → CategoryTheory.Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)}
  {D₁ D₂ : F.DescentData' sq sq₃} (e : (i : ι) → D₁.obj i ≅ D₂.obj i)
  (comm :
    autoParam
      (∀ (i₁ i₂ : ι),
        CategoryTheory.CategoryStruct.comp ((F.map (sq i₁ i₂).p₁.op.toLoc).toFunctor.map (e i₁).hom) (D₂.hom i₁ i₂) =
          CategoryTheory.CategoryStruct.comp (D₁.hom i₁ i₂) ((F.map (sq i₁ i₂).p₂.op.toLoc).toFunctor.map (e i₂).hom))
      CategoryTheory.Pseudofunctor.DescentData'.isoMk._auto_1)
  (i : ι), (CategoryTheory.Pseudofunctor.DescentData'.isoMk e comm).inv.hom i = (e i).inv
-- Mathlib.Algebra.Group.Action.Defs
/-- Distributivity of `•` across `*`  -/
MulDistribMulAction.smul_mul : ∀ {M : Type u_9} {N : Type u_10} {inst : Monoid M} {inst_1 : Monoid N} [self : MulDistribMulAction M N] (r : M)
  (x y : N), r • (x * y) = r • x * r • y
-- Std.Tactic.Do.Syntax
/-- An invariant alternative of the form `| inv<n> a b c => term`, one per invariant goal.
 -/
Lean.Parser.Tactic.invariantCaseAlt : Lean.ParserDescr
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.assoc_tmul : ∀ (R : Type uR) (S : Type uS) {T : Type u_2} (A : Type uA) {C : Type uC} {D : Type uD} [inst : CommSemiring R]
  [inst_1 : CommSemiring S] [inst_2 : Algebra R S] [inst_3 : Semiring A] [inst_4 : Algebra R A] [inst_5 : Algebra S A]
  [inst_6 : IsScalarTower R S A] [inst_7 : Semiring C] [inst_8 : Algebra R C] [inst_9 : Algebra S C]
  [inst_10 : IsScalarTower R S C] [inst_11 : Semiring D] [inst_12 : Algebra R D] [inst_13 : CommSemiring T]
  [inst_14 : Algebra R T] [inst_15 : Algebra S T] [inst_16 : Algebra T A] [inst_17 : IsScalarTower R T A]
  [inst_18 : IsScalarTower S T A] (a : A) (b : C) (c : D),
  (Algebra.TensorProduct.assoc R S T A C D) (a ⊗ₜ[S] b ⊗ₜ[R] c) = a ⊗ₜ[S] (b ⊗ₜ[R] c)
-- Mathlib.CategoryTheory.PathCategory.MorphismProperty
CategoryTheory.MorphismProperty.comp_mem_paths_iff' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C}
  {X Y Z : CategoryTheory.Paths C} {p : X ⟶ Y} {q : Y ⟶ Z},
  W.paths (CategoryTheory.CategoryStruct.comp p q) ↔ W.paths p ∧ W.paths q
-- Mathlib.Algebra.Group.Basic
AddSemigroup.to_isLawfulIdentity : ∀ {M : Type u_4} [inst : AddZeroClass M], Std.LawfulIdentity (fun x1 x2 => x1 + x2) 0
-- Mathlib.Data.List.Permutation
_private.Mathlib.Data.List.Permutation.0.List.permutationsAux2.match_1.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (motive : List α × List β → Sort u_3) (us : List α) (zs : List β)
  (h_1 : (us : List α) → (zs : List β) → motive (us, zs)),
  (match (us, zs) with
    | (us, zs) => h_1 us zs) =
    h_1 us zs
-- Lean.Meta.Tactic.Grind.Arith.Simproc
_private.Lean.Meta.Tactic.Grind.Arith.Simproc.0.Lean.Meta.Grind.Arith.notField : Std.HashSet Lean.Name
-- Mathlib.Analysis.Complex.Trigonometric
Real.sinh_lt_cosh : ∀ (x : ℝ), Real.sinh x < Real.cosh x
-- Mathlib.Order.Hom.Basic
OrderIso.coe_prodComm : ∀ {α : Type u_2} {β : Type u_3} [inst : LE α] [inst_1 : LE β], ⇑OrderIso.prodComm = Prod.swap
-- Std.Data.HashSet.Lemmas
Std.HashSet.getD_eq_fallback_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {a fallback : α},
  m.contains a = false → m.getD a fallback = fallback
-- Mathlib.NumberTheory.Multiplicity
Int.eight_dvd_sq_sub_one_of_odd : ∀ {k : ℤ}, Odd k → 8 ∣ k ^ 2 - 1
-- Mathlib.Control.Traversable.Equiv
Equiv.lawfulFunctor : ∀ {t t' : Type u → Type u} (eqv : (α : Type u) → t α ≃ t' α) [inst : Functor t] [LawfulFunctor t], LawfulFunctor t'
-- Mathlib.RingTheory.HahnSeries.Basic
/-- Unexpander for `HahnSeries`.  -/
HahnSeries.unexpander : Lean.PrettyPrinter.Unexpander
-- Mathlib.Algebra.Group.Subgroup.MulOpposite
Subgroup.unop_le_unop_iff : ∀ {G : Type u_2} [inst : Group G] {S₁ S₂ : Subgroup Gᵐᵒᵖ}, S₁.unop ≤ S₂.unop ↔ S₁ ≤ S₂
-- Mathlib.CategoryTheory.Bicategory.Monad.Basic
/-- The counit 2-morphism of the comonad.  -/
CategoryTheory.Bicategory.Comonad.counit : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a : B} → {t : a ⟶ a} → [CategoryTheory.Bicategory.Comonad t] → t ⟶ CategoryTheory.CategoryStruct.id a
-- Mathlib.LinearAlgebra.Ray
exists_nonneg_left_iff_sameRay : ∀ {R : Type u_1} [inst : Field R] [inst_1 : LinearOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] {x y : M}, x ≠ 0 → ((∃ r, 0 ≤ r ∧ r • x = y) ↔ SameRay R x y)
-- Mathlib.LinearAlgebra.Matrix.Hadamard
Matrix.hadamard_self_eq_self_iff : ∀ {α : Type u_1} {m : Type u_2} {n : Type u_3} [inst : Mul α] {A : Matrix m n α},
  A.hadamard A = A ↔ ∀ (i : m) (j : n), IsIdempotentElem (A i j)
-- Mathlib.Topology.UniformSpace.Ultra.Completion
IsUltraUniformity.separationQuotient : ∀ {X : Type u_1} [inst : UniformSpace X] [IsUltraUniformity X], IsUltraUniformity (SeparationQuotient X)
-- Mathlib.GroupTheory.IndexNSmul
/-- On an additive group that is torsion-free as a `ℤ`-module, the multiplication-by-`n` map
is injective (when `n ≠ 0`).  -/
AddSubgroup.nsmulAddMonoidHom_injective_of_isTorsionFree : ∀ {M : Type u_1} [inst : AddCommGroup M] [Module.IsTorsionFree ℤ M] {n : ℕ},
  n ≠ 0 → Function.Injective ⇑(nsmulAddMonoidHom n)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.size_inter_eq_size_right : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  (h₁ : m₁.WF),
  m₂.WF →
    (∀ (a : α), Std.DTreeMap.Internal.Impl.contains a m₂ = true → Std.DTreeMap.Internal.Impl.contains a m₁ = true) →
      (m₁.inter m₂ ⋯).size = m₂.size
-- Mathlib.SetTheory.Ordinal.Notation
_private.Mathlib.SetTheory.Ordinal.Notation.0.ONote.addAux.match_3.eq_2 : ∀ (motive : ONote → Sort u_1) (e' : ONote) (n' : ℕ+) (a' : ONote) (h_1 : Unit → motive ONote.zero)
  (h_2 : (o' e' : ONote) → (n' : ℕ+) → (a' : ONote) → o' = e'.oadd n' a' → motive (e'.oadd n' a')),
  (match e'.oadd n' a' with
    | ONote.zero => h_1 ()
    | o'@h:(e'.oadd n' a') => h_2 o' e' n' a' h) =
    h_2 (e'.oadd n' a') e' n' a' ⋯
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackFree
/-- The canonical morphism `unit S ⟶ (pushforward.{u} φ).obj (unit R)`
of sheaves of modules corresponding to a continuous map between ringed sites.  -/
SheafOfModules.unitToPushforwardObjUnit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : CategoryTheory.GrothendieckTopology C} →
          {K : CategoryTheory.GrothendieckTopology D} →
            {F : CategoryTheory.Functor C D} →
              {S : CategoryTheory.Sheaf J RingCat} →
                {R : CategoryTheory.Sheaf K RingCat} →
                  [inst_2 : F.IsContinuous J K] →
                    (φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R) →
                      SheafOfModules.unit S ⟶ (SheafOfModules.pushforward φ).obj (SheafOfModules.unit R)
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.addUnitsTypeEquivIsAddUnitAddSubmonoid.eq_1 : ∀ {M : Type u_4} [inst : AddMonoid M],
  AddSubmonoid.addUnitsTypeEquivIsAddUnitAddSubmonoid =
    { toFun := fun x => ⟨↑x, ⋯⟩, invFun := fun x => IsAddUnit.addUnit ⋯, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }
-- Mathlib.Tactic.Linarith.Lemmas
Mathlib.Tactic.Linarith.mul_zero_eq : ∀ {α : Type u_1} {R : α → α → Prop} [inst : Semiring α] {a b : α}, R a 0 → b = 0 → a * b = 0
-- Mathlib.Algebra.Order.BigOperators.Group.List
List.sum_pos : ∀ {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : Preorder M] [IsOrderedAddMonoid M] (l : List M),
  (∀ x ∈ l, 0 < x) → l ≠ [] → 0 < l.sum
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
/-- If `G` preserves pushouts and `C` has them, then the pushout cocone constructed of the mapped
morphisms of the pushout cocone is a colimit.  -/
CategoryTheory.Limits.isColimitOfHasPushoutOfPreservesColimit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (G : CategoryTheory.Functor C D) →
          {W X Y : C} →
            (f : W ⟶ X) →
              (g : W ⟶ Y) →
                [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) G] →
                  [i : CategoryTheory.Limits.HasPushout f g] →
                    CategoryTheory.Limits.IsColimit
                      (CategoryTheory.Limits.PushoutCocone.mk (G.map (CategoryTheory.Limits.pushout.inl f g))
                        (G.map (CategoryTheory.Limits.pushout.inr f g)) ⋯)
-- Mathlib.Control.Bitraversable.Lemmas
Bitraversable.tsnd_comp_tfst : ∀ {t : Type u → Type u → Type u} [inst : Bitraversable t] {F G : Type u → Type u} [inst_1 : Applicative F]
  [inst_2 : Applicative G] [LawfulBitraversable t] [LawfulApplicative F] [LawfulApplicative G] {α₀ α₁ β₀ β₁ : Type u}
  (f : α₀ → F α₁) (f' : β₀ → G β₁),
  Functor.Comp.mk ∘ Functor.map (Bitraversable.tsnd f') ∘ Bitraversable.tfst f =
    bitraverse (Functor.Comp.mk ∘ Functor.map pure ∘ f) (Functor.Comp.mk ∘ pure ∘ f')
-- Mathlib.Order.SuccPred.Limit
Order.isSuccLimitRecOn_succ_of_not_isMax : ∀ {α : Type u_1} {b : α} {motive : α → Sort u_2} [inst : LinearOrder α] [inst_1 : SuccOrder α]
  (isMin : (a : α) → IsMin a → motive a) (succ : (a : α) → ¬IsMax a → motive (Order.succ a))
  (isSuccLimit : (a : α) → Order.IsSuccLimit a → motive a) (hb : ¬IsMax b),
  Order.isSuccLimitRecOn (Order.succ b) isMin succ isSuccLimit = succ b hb
-- Mathlib.CategoryTheory.Limits.Presheaf
CategoryTheory.Presheaf.isLeftKanExtension_of_preservesColimits : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {ℰ : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} ℰ]
  {A : CategoryTheory.Functor C ℰ} [CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A]
  (L : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ (Type (max w v₁ v₂))) ℰ)
  (e : A ≅ CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁}.comp L)
  [CategoryTheory.Limits.PreservesColimitsOfSize.{v₁, max w u₁ v₁ v₂, max (max (max u₁ v₁) v₂) w, v₂,
        max (max (max u₁ (v₁ + 1)) (v₂ + 1)) (w + 1), u₂}
      L],
  L.IsLeftKanExtension e.hom
-- Init.PropLemmas
or_self_iff : ∀ {a : Prop}, a ∨ a ↔ a
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.awayMapAux_mk : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubgroupClass σ A] [inst_3 : AddCommMonoid ι] [inst_4 : DecidableEq ι] (𝒜 : ι → σ)
  [inst_5 : GradedRing 𝒜] {f g x : A} (hx : x = f * g) (n : ι) (a : ↥(𝒜 n)) (i : ℕ) (hi : f ^ i ∈ 𝒜 n),
  (HomogeneousLocalization.awayMapAux✝ 𝒜 ⋯)
      (HomogeneousLocalization.mk { deg := n, num := a, den := ⟨f ^ i, hi⟩, den_mem := ⋯ }) =
    Localization.mk (↑a * g ^ i) ⟨x ^ i, ⋯⟩
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getElem?_toList_rco_eq_some_iff : ∀ {k m n : ℤ} {i : ℕ}, (m...n).toList[i]? = some k ↔ i < (n - m).toNat ∧ m + ↑i = k