mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.RegularWreathProduct
RegularWreathProduct.inv_right : ∀ {D : Type u_1} {Q : Type u_2} [inst : Group D] [inst_1 : Group Q] (a : D ≀ᵣ Q), a⁻¹.right = a.right⁻¹
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass
CategoryTheory.ShortComplex.ext_mk₀_f_comp_ext_mk₀_g : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] (S : CategoryTheory.ShortComplex C),
  (CategoryTheory.Abelian.Ext.mk₀ S.f).comp (CategoryTheory.Abelian.Ext.mk₀ S.g) ⋯ = 0
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
CategoryTheory.Limits.IsZero.epi : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C},
  CategoryTheory.Limits.IsZero X → ∀ {Y : C} (f : Y ⟶ X), CategoryTheory.Epi f
-- Std.Time.Date.Unit.Week
Std.Time.Week.OfYear.instOfNatOrdinal : {n : ℕ} → OfNat Std.Time.Week.OfYear.Ordinal n
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
HomogeneousIdeal.toIdeal_bot : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : Semiring A] [inst_1 : DecidableEq ι] [inst_2 : AddMonoid ι]
  [inst_3 : SetLike σ A] [inst_4 : AddSubmonoidClass σ A] {𝒜 : ι → σ} [inst_5 : GradedRing 𝒜], ⊥.toIdeal = ⊥
-- Aesop.Script.Step
Aesop.Script.LazyStep.BuildInput.mk.injEq : ∀ {α : Type} (tac : Lean.MetaM α) (postGoals : α → Array Lean.MVarId) (tacticBuilder : α → Aesop.Script.TacticBuilder)
  (tac_1 : Lean.MetaM α) (postGoals_1 : α → Array Lean.MVarId) (tacticBuilder_1 : α → Aesop.Script.TacticBuilder),
  ({ tac := tac, postGoals := postGoals, tacticBuilder := tacticBuilder } =
      { tac := tac_1, postGoals := postGoals_1, tacticBuilder := tacticBuilder_1 }) =
    (tac = tac_1 ∧ postGoals = postGoals_1 ∧ tacticBuilder = tacticBuilder_1)
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.monomial_sum_prod : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {α : Type u_2} (s : Finset α) (f : α → σ →₀ ℕ) (g : α → R),
  (MvPolynomial.monomial (∑ i ∈ s, f i)) (∏ i ∈ s, g i) = ∏ i ∈ s, (MvPolynomial.monomial (f i)) (g i)
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- Uses `right` co(ntra)variant.  -/
Right.neg_nonpos_iff : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α] [AddRightMono α] {a : α}, -a ≤ 0 ↔ 0 ≤ a
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.BinaryFan.leftUnitor_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C}
  {s : CategoryTheory.Limits.Cone (CategoryTheory.Functor.empty C)} (P : CategoryTheory.Limits.IsLimit s)
  {t : CategoryTheory.Limits.BinaryFan s.pt X} (Q : CategoryTheory.Limits.IsLimit t),
  (CategoryTheory.Limits.BinaryFan.leftUnitor P Q).inv =
    Q.lift
      (CategoryTheory.Limits.BinaryFan.mk (P.lift { pt := X, π := { app := fun x => x.as.elim, naturality := ⋯ } })
        (CategoryTheory.CategoryStruct.id { pt := X, π := { app := fun x => x.as.elim, naturality := ⋯ } }.pt))
-- Mathlib.Algebra.Order.Group.Defs
neg_le_self_iff : ∀ {α : Type u} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [IsOrderedAddMonoid α] {a : α}, -a ≤ a ↔ 0 ≤ a
-- Init.Grind.Ordered.Field
Lean.Grind.Field.IsOrdered.mul_inv_lt_iff_lt_mul : ∀ {R : Type u} [inst : Lean.Grind.Field R] [inst_1 : LE R] [inst_2 : LT R] [Std.LawfulOrderLT R]
  [inst_4 : Std.IsLinearOrder R] [Lean.Grind.OrderedRing R] (a c : R) {b : R}, 0 < b → (a * b⁻¹ < c ↔ a < c * b)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.arcsin_of_le_neg_one : ∀ {x : ℝ}, x ≤ -1 → Real.arcsin x = -(Real.pi / 2)
-- Lean.Data.Lsp.Internal
Lean.Lsp.LeanModuleQuery.mk.inj : ∀ {identifier : String} {openNamespaces : Array Lean.Lsp.OpenNamespace} {identifier_1 : String}
  {openNamespaces_1 : Array Lean.Lsp.OpenNamespace},
  { identifier := identifier, openNamespaces := openNamespaces } =
      { identifier := identifier_1, openNamespaces := openNamespaces_1 } →
    identifier = identifier_1 ∧ openNamespaces = openNamespaces_1
-- Aesop.Builder.Basic
Aesop.PhaseSpec.norm : Aesop.NormRuleInfo → Aesop.PhaseSpec
-- Mathlib.Algebra.Group.Action.Equidecomp
Equidecomp.restr_target : ∀ {X : Type u_1} {G : Type u_2} [inst : SMul G X] (f : Equidecomp X G) (A : Set X),
  (f.restr A).target = f.target ∩ ↑f.symm ⁻¹' A
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
le_ciSup_ciSup_eq_right : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLattice α] {b : β} {f : (x : β) → b = x → α},
  f b ⋯ ≤ ⨆ x, ⨆ (h : b = x), f x h
-- Mathlib.Topology.Category.CompHaus.Basic
/-- (Implementation) The bijection of homsets to establish the reflective adjunction of compact
Hausdorff spaces in topological spaces.
 -/
stoneCechEquivalence : (X : TopCat) → (Y : CompHaus) → (stoneCechObj X ⟶ Y) ≃ (X ⟶ compHausToTop.obj Y)
-- Mathlib.CategoryTheory.Galois.Examples
/-- The forgetful functor from finite `G`-sets to sets is a `FiberFunctor`.  -/
CategoryTheory.FintypeCat.instFiberFunctorActionFintypeCatForget₂HomSubtypeFunObjFiniteV : ∀ (G : Type u) [inst : Group G],
  CategoryTheory.PreGaloisCategory.FiberFunctor (CategoryTheory.forget₂ (Action FintypeCat G) FintypeCat)
-- Mathlib.CategoryTheory.Shift.Basic
CategoryTheory.shiftEquiv'_functor : ∀ (C : Type u) {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddGroup A]
  [inst_2 : CategoryTheory.HasShift C A] (i j : A) (h : i + j = 0),
  (CategoryTheory.shiftEquiv' C i j h).functor = CategoryTheory.shiftFunctor C i
-- Mathlib.Order.SuccPred.Limit
Order.isPredPrelimitRecOn_pred_of_not_isMin : ∀ {α : Type u_1} {b : α} {motive : α → Sort u_2} [inst : LinearOrder α] [inst_1 : PredOrder α]
  (pred : (a : α) → ¬IsMin a → motive (Order.pred a)) (isPredPrelimit : (a : α) → Order.IsPredPrelimit a → motive a)
  (hb : ¬IsMin b), Order.isPredPrelimitRecOn (Order.pred b) pred isPredPrelimit = pred b hb
-- Mathlib.CategoryTheory.CommSq
CategoryTheory.CommSq.HasLift.mk' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A B X Y : C} {f : A ⟶ X} {i : A ⟶ B} {p : X ⟶ Y}
  {g : B ⟶ Y} {sq : CategoryTheory.CommSq f i p g} (l : sq.LiftStruct), sq.HasLift
-- Mathlib.Analysis.Calculus.LocalExtr.Polynomial
/-- The number of roots of a real polynomial (counted with multiplicities) is at most the number of
roots of its derivative (counted with multiplicities) plus one.  -/
Polynomial.card_roots_le_derivative : ∀ (p : Polynomial ℝ), p.roots.card ≤ (Polynomial.derivative p).roots.card + 1
-- Lean.Elab.Command.Scope
/-- `include`d section variable names (from `varUIds`)  -/
Lean.Elab.Command.Scope.includedVars : Lean.Elab.Command.Scope → List Lean.Name
-- Mathlib.Topology.Bornology.Constructions
Bornology.isBounded_image_fst_and_snd : ∀ {α : Type u_1} {β : Type u_2} [inst : Bornology α] [inst_1 : Bornology β] {s : Set (α × β)},
  Bornology.IsBounded (Prod.fst '' s) ∧ Bornology.IsBounded (Prod.snd '' s) ↔ Bornology.IsBounded s
-- Mathlib.Computability.Primrec.List
_private.Mathlib.Computability.Primrec.List.0.List.filter.match_1.eq_1 : ∀ (motive : Bool → Sort u_1) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  (match true with
    | true => h_1 ()
    | false => h_2 ()) =
    h_1 ()
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
SimpleGraph.Colorable.eq_1 : ∀ {V : Type u} (G : SimpleGraph V) (n : ℕ), G.Colorable n = Nonempty (G.Coloring (Fin n))
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
IntervalIntegrable.mono_fun' : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] {a b : ℝ} {μ : MeasureTheory.Measure ℝ} {f : ℝ → E} {g : ℝ → ℝ},
  IntervalIntegrable g μ a b →
    MeasureTheory.AEStronglyMeasurable f (μ.restrict (Set.uIoc a b)) →
      (fun x => ‖f x‖) ≤ᵐ[μ.restrict (Set.uIoc a b)] g → IntervalIntegrable f μ a b
-- Mathlib.Algebra.Homology.SpectralObject.FirstPage
CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.HasFirstPageComputation.hi₀₁ : ∀ {ι : Type u_2} {κ : Type u_3} {inst : Preorder ι} {c : ℤ → ComplexShape κ} {r₀ : ℤ}
  {data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀} [self : data.HasFirstPageComputation]
  (pq : κ), data.i₀ r₀ pq ⋯ = data.i₁ pq
-- Init.Data.List.MinMaxOn
List.maxOn?_singleton : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] {x : α} {f : α → β}, List.maxOn? f [x] = some x
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
CategoryTheory.StrictlyUnitaryPseudofunctor.mk : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        (toPseudofunctor : CategoryTheory.Pseudofunctor B C) →
          (map_id :
              autoParam
                (∀ (X : B),
                  toPseudofunctor.map (CategoryTheory.CategoryStruct.id X) =
                    CategoryTheory.CategoryStruct.id (toPseudofunctor.obj X))
                CategoryTheory.StrictlyUnitaryPseudofunctor.map_id._autoParam) →
            autoParam (∀ (X : B), toPseudofunctor.mapId X = CategoryTheory.eqToIso ⋯)
                CategoryTheory.StrictlyUnitaryPseudofunctor.mapId_eq_eqToIso._autoParam →
              CategoryTheory.StrictlyUnitaryPseudofunctor B C
-- Mathlib.Topology.Inseparable
stableUnderSpecialization_sUnion : ∀ {X : Type u_1} [inst : TopologicalSpace X] (S : Set (Set X)),
  (∀ s ∈ S, StableUnderSpecialization s) → StableUnderSpecialization (⋃₀ S)
-- Mathlib.Topology.Sheaves.Presheaf
/-- If `f : X ⟶ Y` is an open map, this expresses the naturality of the isomorphism
`IsOpenMap.pullbackObjIso` between the pullback by `f` of a presheaf and the composition
of that presheaf and of the functor `(Open X)ᵒᵖ ⥤ (Open Y)ᵒᵖ` induced by `f`.
 -/
IsOpenMap.pullbackObjIso_hom_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X Y : TopCat}
  {f : X ⟶ Y} (hf : IsOpenMap ⇑(CategoryTheory.ConcreteCategory.hom f)) {ℱ 𝒢 : TopCat.Presheaf C Y} (u : ℱ ⟶ 𝒢),
  CategoryTheory.CategoryStruct.comp ((TopCat.Presheaf.pullback C f).map u) (hf.pullbackObjIso 𝒢).hom =
    CategoryTheory.CategoryStruct.comp (hf.pullbackObjIso ℱ).hom (hf.functor.op.whiskerLeft u)
-- Mathlib.Topology.Order.DenselyOrdered
frontier_Ici : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [DenselyOrdered α]
  [NoMinOrder α] {a : α}, frontier (Set.Ici a) = {a}
-- Mathlib.CategoryTheory.Limits.Creates
CategoryTheory.CreatesColimitsOfShape.CreatesColimit : {C : Type u₁} →
  {inst : CategoryTheory.Category.{v₁, u₁} C} →
    {D : Type u₂} →
      {inst_1 : CategoryTheory.Category.{v₂, u₂} D} →
        {J : Type w} →
          {inst_2 : CategoryTheory.Category.{w', w} J} →
            {F : CategoryTheory.Functor C D} →
              [self : CategoryTheory.CreatesColimitsOfShape J F] →
                {K : CategoryTheory.Functor J C} → CategoryTheory.CreatesColimit K F
-- Mathlib.Computability.DFA
DFA.evalFrom_comap : ∀ {α : Type u} {σ : Type v} (M : DFA α σ) {α' : Type u_1} (f : α' → α) (s : σ) (x : List α'),
  (DFA.comap f M).evalFrom s x = M.evalFrom s (List.map f x)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.link2!.induct_unfolding : ∀ {α : Type u} {β : α → Type v}
  (motive : Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl α β → Prop),
  (∀ (r : Std.DTreeMap.Internal.Impl α β), motive Std.DTreeMap.Internal.Impl.leaf r r) →
    (∀ (sz' : ℕ) (k' : α) (v' : β k') (l'' r'' : Std.DTreeMap.Internal.Impl α β),
        motive (Std.DTreeMap.Internal.Impl.inner sz' k' v' l'' r'') Std.DTreeMap.Internal.Impl.leaf
          (Std.DTreeMap.Internal.Impl.inner sz' k' v' l'' r'')) →
      (∀ (sz' : ℕ) (k' : α) (v' : β k') (l'' r'' : Std.DTreeMap.Internal.Impl α β) (sz'_1 : ℕ) (k'_1 : α)
          (v'_1 : β k'_1) (l''_1 r''_1 : Std.DTreeMap.Internal.Impl α β),
          Std.DTreeMap.Internal.delta * sz' < sz'_1 →
            motive (Std.DTreeMap.Internal.Impl.inner sz' k' v' l'' r'') l''_1
                ((Std.DTreeMap.Internal.Impl.inner sz' k' v' l'' r'').link2! l''_1) →
              motive (Std.DTreeMap.Internal.Impl.inner sz' k' v' l'' r'')
                (Std.DTreeMap.Internal.Impl.inner sz'_1 k'_1 v'_1 l''_1 r''_1)
                (Std.DTreeMap.Internal.Impl.balanceL! k'_1 v'_1
                  ((Std.DTreeMap.Internal.Impl.inner sz' k' v' l'' r'').link2! l''_1) r''_1)) →
        (∀ (sz' : ℕ) (k' : α) (v' : β k') (l'' r'' : Std.DTreeMap.Internal.Impl α β) (sz'_1 : ℕ) (k'_1 : α)
            (v'_1 : β k'_1) (l''_1 r''_1 : Std.DTreeMap.Internal.Impl α β),
            ¬Std.DTreeMap.Internal.delta * sz' < sz'_1 →
              Std.DTreeMap.Internal.delta * sz'_1 < sz' →
                motive r'' (Std.DTreeMap.Internal.Impl.inner sz'_1 k'_1 v'_1 l''_1 r''_1)
                    (r''.link2! (Std.DTreeMap.Internal.Impl.inner sz'_1 k'_1 v'_1 l''_1 r''_1)) →
                  motive (Std.DTreeMap.Internal.Impl.inner sz' k' v' l'' r'')
                    (Std.DTreeMap.Internal.Impl.inner sz'_1 k'_1 v'_1 l''_1 r''_1)
                    (Std.DTreeMap.Internal.Impl.balanceR! k' v' l''
                      (r''.link2! (Std.DTreeMap.Internal.Impl.inner sz'_1 k'_1 v'_1 l''_1 r''_1)))) →
          (∀ (sz' : ℕ) (k' : α) (v' : β k') (l'' r'' : Std.DTreeMap.Internal.Impl α β) (sz'_1 : ℕ) (k'_1 : α)
              (v'_1 : β k'_1) (l''_1 r''_1 : Std.DTreeMap.Internal.Impl α β),
              ¬Std.DTreeMap.Internal.delta * sz' < sz'_1 →
                ¬Std.DTreeMap.Internal.delta * sz'_1 < sz' →
                  motive (Std.DTreeMap.Internal.Impl.inner sz' k' v' l'' r'')
                    (Std.DTreeMap.Internal.Impl.inner sz'_1 k'_1 v'_1 l''_1 r''_1)
                    ((Std.DTreeMap.Internal.Impl.inner sz' k' v' l'' r'').glue!
                      (Std.DTreeMap.Internal.Impl.inner sz'_1 k'_1 v'_1 l''_1 r''_1))) →
            ∀ (l r : Std.DTreeMap.Internal.Impl α β), motive l r (l.link2! r)
-- Mathlib.SetTheory.Ordinal.Exponential
Ordinal.opow_zero : ∀ (a : Ordinal.{u_1}), a ^ 0 = 1
-- Mathlib.CategoryTheory.Triangulated.Basic
/-- The triangle `productTriangle T` satisfies the universal property of the categorical
product of the triangles `T`.  -/
CategoryTheory.Pretriangulated.productTriangle.isLimitFan : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.HasShift C ℤ] →
      {J : Type u_1} →
        (T : J → CategoryTheory.Pretriangulated.Triangle C) →
          [inst_2 : CategoryTheory.Limits.HasProduct fun j => (T j).obj₁] →
            [inst_3 : CategoryTheory.Limits.HasProduct fun j => (T j).obj₂] →
              [inst_4 : CategoryTheory.Limits.HasProduct fun j => (T j).obj₃] →
                [inst_5 : CategoryTheory.Limits.HasProduct fun j => (CategoryTheory.shiftFunctor C 1).obj (T j).obj₁] →
                  CategoryTheory.Limits.IsLimit (CategoryTheory.Pretriangulated.productTriangle.fan T)
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.min_le_of_contains : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α}
  (hc : t.contains k = true), (cmp (t.min ⋯) k).isLE = true
-- Mathlib.LinearAlgebra.DFinsupp
DFinsupp.mapRange.linearMap_apply : ∀ {ι : Type u_1} {R : Type u_3} [inst : Semiring R] {β₁ : ι → Type u_8} {β₂ : ι → Type u_9}
  [inst_1 : (i : ι) → AddCommMonoid (β₁ i)] [inst_2 : (i : ι) → AddCommMonoid (β₂ i)]
  [inst_3 : (i : ι) → Module R (β₁ i)] [inst_4 : (i : ι) → Module R (β₂ i)] (f : (i : ι) → β₁ i →ₗ[R] β₂ i)
  (x : Π₀ (i : ι), β₁ i), (DFinsupp.mapRange.linearMap f) x = DFinsupp.mapRange (fun i x => (f i) x) ⋯ x
-- Mathlib.Algebra.NonAssoc.LieAdmissible.Defs
LieAdmissibleRing.mk : {L : Type u_1} →
  [toNonUnitalNonAssocRing : NonUnitalNonAssocRing L] →
    (∀ (x y z : L),
        associator x y z + associator z x y + associator y z x =
          associator y x z + associator z y x + associator x z y) →
      LieAdmissibleRing L
-- Mathlib.Order.BoundedOrder.Basic
bot_lt_iff_not_le_bot : ∀ {α : Type u} [inst : Preorder α] [inst_1 : OrderBot α] {a : α}, ⊥ < a ↔ ¬a ≤ ⊥
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
AddMonoidAlgebra.mapDomainBialgHomEquiv.eq_1 : ∀ {R : Type u_1} {G : Type u_5} {H : Type u_6} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : AddGroup G]
  [inst_3 : AddGroup H],
  AddMonoidAlgebra.mapDomainBialgHomEquiv =
    { toFun := AddMonoidAlgebra.mapDomainBialgHom R, invFun := AddMonoidAlgebra.mapDomainOfBialgHom, left_inv := ⋯,
      right_inv := ⋯ }
-- Mathlib.Data.Set.Lattice
Set.subset_sInter : ∀ {α : Type u_1} {S : Set (Set α)} {t : Set α}, (∀ t' ∈ S, t ⊆ t') → t ⊆ ⋂₀ S
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rco.pairwise_toList_ne : ∀ {α : Type u} {r : Std.Rco α} [LE α] [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α]
  [inst_5 : Std.Rxo.IsAlwaysFinite α], List.Pairwise (fun a b => a ≠ b) r.toList
-- Mathlib.GroupTheory.GroupAction.SubMulAction.Closure
SubMulAction.mem_closure : ∀ {R : Type u_1} {M : Type u_2} [inst : SMul R M] {s : Set M} {x : M},
  x ∈ SubMulAction.closure R s ↔ ∀ (p : SubMulAction R M), s ⊆ ↑p → x ∈ p
-- Mathlib.Algebra.Group.PNatPowAssoc
ppow_one : ∀ {M : Type u_1} [inst : Mul M] [inst_1 : Pow M ℕ+] [PNatPowAssoc M] (x : M), x ^ 1 = x
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
CategoryTheory.SmallObject.SuccStruct.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : SizeOf C] (X₀ : C) (succ : C → C)
  (toSucc : (X : C) → X ⟶ succ X), sizeOf { X₀ := X₀, succ := succ, toSucc := toSucc } = 1 + sizeOf X₀
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
CategoryTheory.Bicategory.Adj.lIso_hom : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : CategoryTheory.Bicategory.Adj B} {adj₁ adj₂ : a ⟶ b}
  (e : adj₁ ≅ adj₂), (CategoryTheory.Bicategory.Adj.lIso e).hom = e.hom.τl
-- Lean.Data.FuzzyMatching
/-- Add additional information to each character in a string.  -/
_private.Lean.Data.FuzzyMatching.0.Lean.FuzzyMatching.stringInfo : String → Array Lean.FuzzyMatching.CharRole
-- Mathlib.Algebra.Polynomial.EraseLead
Polynomial.eraseLead_add_monomial_natDegree_leadingCoeff : ∀ {R : Type u_1} [inst : Semiring R] (f : Polynomial R),
  f.eraseLead + (Polynomial.monomial f.natDegree) f.leadingCoeff = f
-- Mathlib.Algebra.GCDMonoid.Basic
normalize_gcd : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] (a b : α), normalize (gcd a b) = gcd a b
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getThenInsertIfNew?_snd : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k : α} {v : β}, (Std.ExtDTreeMap.Const.getThenInsertIfNew? t k v).2 = t.insertIfNew k v
-- Mathlib.Data.PNat.Defs
PNat.instWellFoundedRelation : WellFoundedRelation ℕ+
-- Mathlib.Data.PNat.Xgcd
/-- `finish` happens when the reducing process ends.  -/
PNat.XgcdType.finish : PNat.XgcdType → PNat.XgcdType
-- Mathlib.Analysis.InnerProductSpace.Spectrum
ContinuousLinearMap.eq_zero_of_forall_hasEigenvalue_eq_zero : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [CompleteSpace E] {T : E →L[𝕜] E},
  IsCompactOperator ⇑T → (↑T).IsSymmetric → ((∀ (μ : 𝕜), Module.End.HasEigenvalue (↑T) μ → μ = 0) ↔ T = 0)
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
AlgebraicGeometry.LocallyRingedSpace.Γ_obj_op : ∀ (X : AlgebraicGeometry.LocallyRingedSpace),
  AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X) = X.presheaf.obj (Opposite.op ⊤)
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.U_eval_neg_one : ∀ (R : Type u_1) [inst : CommRing R] (n : ℤ),
  Polynomial.eval (-1) (Polynomial.Chebyshev.U R n) = ↑↑n.negOnePow * (↑n + 1)
-- Init.PropLemmas
ite_else_decide_self : ∀ (p : Prop) [h : Decidable p] {w : Decidable p} (q : Bool), (if p then q else decide p) = (decide p && q)
-- Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
CategoryTheory.Functor.instIsIsoAppRanCounit_1 : ∀ {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] (L : CategoryTheory.Functor C D) {H : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} H] [L.Full] [L.Faithful] (F : CategoryTheory.Functor C H)
  [L.HasPointwiseRightKanExtension F] [inst_6 : ∀ (F : CategoryTheory.Functor C H), L.HasRightKanExtension F],
  CategoryTheory.IsIso (L.ranCounit.app F)
-- Mathlib.FieldTheory.RatFunc.AsPolynomial
RatFunc.algebraMap_eq_C : ∀ {K : Type u} [inst : CommRing K] [inst_1 : IsDomain K], algebraMap K (RatFunc K) = RatFunc.C
-- Mathlib.Algebra.Order.Field.Basic
one_div_le : ∀ {α : Type u_2} [inst : Semifield α] [inst_1 : PartialOrder α] [PosMulReflectLT α] {a b : α},
  0 < a → 0 < b → (1 / a ≤ b ↔ 1 / b ≤ a)
-- Mathlib.CategoryTheory.NatIso
CategoryTheory.Iso.inv_hom_id_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} (α : F ≅ G) (X : C),
  CategoryTheory.CategoryStruct.comp (α.inv.app X) (α.hom.app X) = CategoryTheory.CategoryStruct.id (G.obj X)
-- Mathlib.Analysis.Normed.Module.Ball.Pointwise
ball_sub_closedBall : ∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] [NormedSpace ℝ E] {δ ε : ℝ},
  0 < ε → 0 ≤ δ → ∀ (a b : E), Metric.ball a ε - Metric.closedBall b δ = Metric.ball (a - b) (ε + δ)
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsLimit.lift_comp_conePointsIsoOfNatIso_inv_assoc : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F G : CategoryTheory.Functor J C} {r s : CategoryTheory.Limits.Cone G} {t : CategoryTheory.Limits.Cone F}
  (P : CategoryTheory.Limits.IsLimit t) (Q : CategoryTheory.Limits.IsLimit s) (w : F ≅ G) {Z : C} (h : t.pt ⟶ Z),
  CategoryTheory.CategoryStruct.comp (Q.lift r)
      (CategoryTheory.CategoryStruct.comp (P.conePointsIsoOfNatIso Q w).inv h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.IsLimit.map r P w.inv) h
-- Mathlib.Algebra.MonoidAlgebra.Defs
/-- This prevents `ofCoeff x` being printed as `{ coeff := x }` by `delabStructureInstance`.  -/
AddMonoidAlgebra.delabOfCoeff : Lean.PrettyPrinter.Delaborator.Delab
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get_ofList_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [Std.TransCmp cmp] {l : List (α × β)} {k k' : α},
  cmp k k' = Ordering.eq →
    ∀ {v : β},
      List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l →
        (k, v) ∈ l →
          ∀ {h : k' ∈ Std.DTreeMap.Raw.Const.ofList l cmp},
            Std.DTreeMap.Raw.Const.get (Std.DTreeMap.Raw.Const.ofList l cmp) k' h = v
-- Mathlib.Order.Heyting.Basic
OrderDual.instGeneralizedCoheytingAlgebra : {α : Type u_2} → [GeneralizedHeytingAlgebra α] → GeneralizedCoheytingAlgebra αᵒᵈ
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.entryAtIdx?.induct_unfolding : ∀ {α : Type u} {β : α → Type v} (motive : Std.DTreeMap.Internal.Impl α β → ℕ → Option ((a : α) × β a) → Prop),
  (∀ (x : ℕ), motive Std.DTreeMap.Internal.Impl.leaf x none) →
    (∀ (size : ℕ) (k : α) (v : β k) (l r : Std.DTreeMap.Internal.Impl α β) (n : ℕ),
        compare n l.size = Ordering.lt →
          motive l n (l.entryAtIdx? n) → motive (Std.DTreeMap.Internal.Impl.inner size k v l r) n (l.entryAtIdx? n)) →
      (∀ (size : ℕ) (k : α) (v : β k) (l r : Std.DTreeMap.Internal.Impl α β) (n : ℕ),
          compare n l.size = Ordering.eq → motive (Std.DTreeMap.Internal.Impl.inner size k v l r) n (some ⟨k, v⟩)) →
        (∀ (size : ℕ) (k : α) (v : β k) (l r : Std.DTreeMap.Internal.Impl α β) (n : ℕ),
            compare n l.size = Ordering.gt →
              motive r (n - l.size - 1) (r.entryAtIdx? (n - l.size - 1)) →
                motive (Std.DTreeMap.Internal.Impl.inner size k v l r) n (r.entryAtIdx? (n - l.size - 1))) →
          ∀ (a : Std.DTreeMap.Internal.Impl α β) (a_1 : ℕ), motive a a_1 (a.entryAtIdx? a_1)
-- Mathlib.Control.Bitraversable.Basic
LawfulBitraversable.bitraverse_id_id : ∀ {t : Type u → Type u → Type u} {inst : Bitraversable t} [self : LawfulBitraversable t] {α β : Type u},
  bitraverse pure pure = pure
-- Mathlib.AlgebraicGeometry.Birational.Birational
AlgebraicGeometry.Scheme.PartialIso.mk : {X Y : AlgebraicGeometry.Scheme} →
  (source : X.Opens) → Dense ↑source → (target : Y.Opens) → Dense ↑target → (↑source ≅ ↑target) → X.PartialIso Y