mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.PushoutObjObj.mapArrowRight_right : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)} {f₁ : CategoryTheory.Arrow C₁}
  {f₂ f₂' : CategoryTheory.Arrow C₂} (sq₁₂ : F.PushoutObjObj f₁.hom f₂.hom) (sq₁₂' : F.PushoutObjObj f₁.hom f₂'.hom)
  (sq : f₂ ⟶ f₂'), (sq₁₂.mapArrowRight sq₁₂' sq).right = (F.obj f₁.right).map (CategoryTheory.Arrow.Hom.right sq)
-- ProofWidgets.Component.HtmlDisplay
ProofWidgets.HtmlCommand.elabHtmlCmd : Lean.Elab.Command.CommandElab
-- Lean.Data.JsonRpc
/-- Error codes defined by
[JSON-RPC](https://www.jsonrpc.org/specification#error_object) and
[LSP](https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#errorCodes).  -/
Lean.JsonRpc.ErrorCode : Type
-- Mathlib.Algebra.MvPolynomial.Division
MvPolynomial.modMonomial_add_divMonomial : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] (x : MvPolynomial σ R) (s : σ →₀ ℕ),
  x.modMonomial s + (MvPolynomial.monomial s) 1 * x.divMonomial s = x
-- Mathlib.Data.List.Cycle
List.nextOr.eq_3 : ∀ {α : Type u_1} [inst : DecidableEq α] (x x_1 y z : α) (xs : List α),
  (y :: z :: xs).nextOr x x_1 = if x = y then z else (z :: xs).nextOr x x_1
-- Mathlib.RingTheory.QuasiFinite.Polynomial
Polynomial.not_ker_le_map_C_of_surjective_of_weaklyQuasiFiniteAt : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (f : Polynomial R →ₐ[R] S),
  Function.Surjective ⇑f →
    ∀ (P : Ideal S) [inst_3 : P.IsPrime] [Algebra.WeaklyQuasiFiniteAt R P],
      ¬RingHom.ker f ≤ Ideal.map Polynomial.C (Ideal.under R P)
-- Std.Data.DTreeMap.Lemmas
_private.Std.Data.DTreeMap.Lemmas.0.Std.DTreeMap.ext : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t t' : Std.DTreeMap α β cmp}, t.inner = t'.inner → t = t'
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.tan_zero : Real.Angle.tan 0 = 0
-- Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
Finset.prod_anti_set_of_le_one : ∀ {ι : Type u_1} {R : Type u_2} [inst : CommMonoidWithZero R] [inst_1 : Preorder R] [ZeroLEOneClass R] [PosMulMono R]
  {f : ι → R}, (∀ (x : ι), 0 ≤ f x) → (∀ (x : ι), f x ≤ 1) → Antitone fun s => ∏ x ∈ s, f x
-- Mathlib.RingTheory.AlgebraicIndependent.Defs
AlgebraicIndependent.aeval_repr : ∀ {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A]
  [inst_2 : Algebra R A] (hx : AlgebraicIndependent R x) (p : ↥(Algebra.adjoin R (Set.range x))),
  (MvPolynomial.aeval x) (hx.repr p) = ↑p
-- Lean.Elab.Tactic.Omega.Frontend
/-- Parse an `Expr` and extract facts, also returning the number of new facts found.
 -/
Lean.Elab.Tactic.Omega.MetaProblem.addFact : Lean.Elab.Tactic.Omega.MetaProblem → Lean.Expr → Lean.Elab.Tactic.Omega.OmegaM (Lean.Elab.Tactic.Omega.MetaProblem × ℕ)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey?_filterMap : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} {γ : α → Type w}
  [inst : Std.TransCmp cmp] [inst_1 : Std.LawfulEqCmp cmp] {f : (a : α) → β a → Option (γ a)} {k : α},
  (Std.DTreeMap.filterMap f t).getKey? k = (t.getKey? k).pfilter fun x h' => (f x (t.get x ⋯)).isSome
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.map_eq_iff_precomp : ∀ {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)
  (W : CategoryTheory.MorphismProperty C) [L.IsLocalization W] [W.HasRightCalculusOfFractions] {Y Z : C}
  (f₁ f₂ : Y ⟶ Z),
  L.map f₁ = L.map f₂ ↔
    ∃ X s, ∃ (_ : W s), CategoryTheory.CategoryStruct.comp s f₁ = CategoryTheory.CategoryStruct.comp s f₂
-- Mathlib.CategoryTheory.Action.Monoidal
Action.instMonoidalPreadditive : ∀ (V : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} V] (G : Type u_2) [inst_1 : Monoid G]
  [inst_2 : CategoryTheory.MonoidalCategory V] [inst_3 : CategoryTheory.Preadditive V]
  [CategoryTheory.MonoidalPreadditive V], CategoryTheory.MonoidalPreadditive (Action V G)
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.inclusion.isScalarTower_left : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {S T : Subalgebra R A}
  (h : S ≤ T) (X : Type u_1) [inst_3 : SMul X R] [inst_4 : SMul X A] [inst_5 : IsScalarTower X R A],
  IsScalarTower X ↥S ↥T
-- Mathlib.Topology.Algebra.InfiniteSum.Group
HasProd.inv₀ : ∀ {α : Type u_1} {K : Type u_4} [inst : CommGroupWithZero K] [inst_1 : TopologicalSpace K] {f : α → K}
  {L : SummationFilter α} {a : K} [ContinuousInv₀ K], HasProd f a L → a ≠ 0 → HasProd (fun x => (f x)⁻¹) a⁻¹ L
-- Mathlib.Topology.ExtendFrom
extendFrom_eq : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [T2Space Y] {A : Set X}
  {f : X → Y} {x : X} {y : Y}, x ∈ closure A → Filter.Tendsto f (nhdsWithin x A) (nhds y) → extendFrom A f x = y
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
/-- The mates equivalence commutes with this composition, essentially by `mateEquiv_vcomp`.  -/
CategoryTheory.Bicategory.mateEquiv_conjugateEquiv_vcomp : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d : B} {g : a ⟶ c} {h : b ⟶ d} {l₁ : a ⟶ b} {r₁ : b ⟶ a}
  {l₂ : c ⟶ d} {r₂ : d ⟶ c} {l₃ : c ⟶ d} {r₃ : d ⟶ c} (adj₁ : CategoryTheory.Bicategory.Adjunction l₁ r₁)
  (adj₂ : CategoryTheory.Bicategory.Adjunction l₂ r₂) (adj₃ : CategoryTheory.Bicategory.Adjunction l₃ r₃)
  (α : CategoryTheory.CategoryStruct.comp g l₂ ⟶ CategoryTheory.CategoryStruct.comp l₁ h) (β : l₃ ⟶ l₂),
  (CategoryTheory.Bicategory.mateEquiv adj₁ adj₃) (CategoryTheory.Bicategory.leftAdjointSquareConjugate.vcomp α β) =
    CategoryTheory.Bicategory.rightAdjointSquareConjugate.vcomp ((CategoryTheory.Bicategory.mateEquiv adj₁ adj₂) α)
      ((CategoryTheory.Bicategory.conjugateEquiv adj₂ adj₃) β)
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.toCompositionAsSet_length : ∀ {n : ℕ} (c : Composition n), c.toCompositionAsSet.length = c.length
-- Mathlib.CategoryTheory.Sites.Precoverage
CategoryTheory.Precoverage.instHasPullbacksOfHasPullbacks : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.Precoverage C)
  [CategoryTheory.Limits.HasPullbacks C], J.HasPullbacks
-- Mathlib.Util.CountHeartbeats
/-- `#count_heartbeats tac` counts the heartbeats used by the tactic sequence `tac`
and prints an info line with the number of heartbeats.

* `#count_heartbeats! n in tac`, where `n` is an optional natural number literal, runs `tac`
  `n` times on the same goal while counting the heartbeats, and prints an info line with range and
  standard deviation. `n` can be left out, and defaults to 10.

Example:

```
example : 1 + 1 = 2 := by
  -- The next line will print an info message of this format; the exact number may vary.
  -- info: 4646
  #count_heartbeats simp

example : 1 + 1 = 2 := by
  -- The next line will print an info message of this format; the exact numbers may vary.
  -- info: Min: 4 Max: 4 StdDev: 2%
  #count_heartbeats! 37 in simp
```
 -/
Mathlib.CountHeartbeats.«tactic#count_heartbeats!_In__» : Lean.ParserDescr
-- Mathlib.SetTheory.Ordinal.Arithmetic
/-- **Alias** of `Ordinal.nsmul_eq_mul`. -/
Ordinal.smul_eq_mul : ∀ (n : ℕ) (a : Ordinal.{u_4}), n • a = a * ↑n
-- Mathlib.Algebra.Order.Group.Indicator
Set.le_indicator_apply : ∀ {α : Type u_2} {M : Type u_3} [inst : LE M] [inst_1 : Zero M] {s : Set α} {g : α → M} {a : α} {y : M},
  (a ∈ s → y ≤ g a) → (a ∉ s → y ≤ 0) → y ≤ s.indicator g a
-- Mathlib.Logic.Relation
Relation.reflTransGen_transGen : ∀ {α : Type u_1} {r : α → α → Prop}, Relation.ReflTransGen (Relation.TransGen r) = Relation.ReflTransGen r
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.GrothendieckTopology.OneHypercover.multiforkLift.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} A]
  {J : CategoryTheory.GrothendieckTopology C} {S : C} {E : J.OneHypercover S} {F : CategoryTheory.Sheaf J A}
  (c : CategoryTheory.Limits.Multifork (E.multicospanIndex F.obj)),
  CategoryTheory.GrothendieckTopology.OneHypercover.multiforkLift c = ⋯.amalgamateOfArrows E.f ⋯ c.ι ⋯
-- Mathlib.Tactic.ClickSuggestions.Rewrite
/-- Generate the suggestion for rewriting with `lem`.  -/
Mathlib.Tactic.ClickSuggestions.RwLemma.try : Mathlib.Tactic.ClickSuggestions.RwInfo →
  Mathlib.Tactic.ClickSuggestions.RwLemma →
    Mathlib.Tactic.ClickSuggestions.ClickSuggestionsM
      (Mathlib.Tactic.ClickSuggestions.Result Mathlib.Tactic.ClickSuggestions.RwKey)
-- Mathlib.Algebra.Lie.Prod
/-- The first projection of a product is a Lie algebra map.  -/
LieHom.fst : (R : Type u_1) →
  (L₁ : Type u_2) →
    (L₂ : Type u_3) →
      [inst : CommRing R] →
        [inst_1 : LieRing L₁] →
          [inst_2 : LieAlgebra R L₁] → [inst_3 : LieRing L₂] → [inst_4 : LieAlgebra R L₂] → L₁ × L₂ →ₗ⁅R⁆ L₁
-- Lean.Util.PtrSet
Lean.Ptr : Type u → Type u
-- Init.Data.String.Decode
String.utf8EncodeCharFast.eq_def : ∀ (c : Char),
  String.utf8EncodeCharFast c =
    have v := c.val;
    if v ≤ 127 then [v.toUInt8]
    else
      if v ≤ 2047 then [(v >>> 6).toUInt8 &&& 31 ||| 192, v.toUInt8 &&& 63 ||| 128]
      else
        if v ≤ 65535 then
          [(v >>> 12).toUInt8 &&& 15 ||| 224, (v >>> 6).toUInt8 &&& 63 ||| 128, v.toUInt8 &&& 63 ||| 128]
        else
          [(v >>> 18).toUInt8 &&& 7 ||| 240, (v >>> 12).toUInt8 &&& 63 ||| 128, (v >>> 6).toUInt8 &&& 63 ||| 128,
            v.toUInt8 &&& 63 ||| 128]
-- Mathlib.SetTheory.Cardinal.Free
Cardinal.mk_abelianization_le : ∀ (G : Type u) [inst : Group G], Cardinal.mk (Abelianization G) ≤ Cardinal.mk G
-- Mathlib.Algebra.Module.Submodule.Range
LinearMap.map_le_range : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_6} [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₂}
  [inst_6 : RingHomSurjective τ₁₂] {f : M →ₛₗ[τ₁₂] M₂} {p : Submodule R M}, Submodule.map f p ≤ f.range
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
ENNReal.tsum_le_tsum : ∀ {α : Type u_1} {f g : α → ENNReal}, (∀ (a : α), f a ≤ g a) → ∑' (a : α), f a ≤ ∑' (a : α), g a
-- Mathlib.CategoryTheory.Limits.Cones
/-- The construction `mapCone` respects functor composition.  -/
CategoryTheory.Functor.mapConeMapCone : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {D : Type u₄} →
          [inst_2 : CategoryTheory.Category.{v₄, u₄} D] →
            {E : Type u₅} →
              [inst_3 : CategoryTheory.Category.{v₅, u₅} E] →
                {F : CategoryTheory.Functor J C} →
                  {H : CategoryTheory.Functor C D} →
                    {H' : CategoryTheory.Functor D E} →
                      (c : CategoryTheory.Limits.Cone F) → H'.mapCone (H.mapCone c) ≅ (H.comp H').mapCone c
-- Mathlib.CategoryTheory.Limits.Types.Colimits
CategoryTheory.Limits.Types.colimitEquivColimitType_symm_apply : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u))
  [inst_1 : CategoryTheory.Limits.HasColimit F] (j : J) (x : F.obj j),
  (CategoryTheory.Limits.Types.colimitEquivColimitType F).symm (Quot.mk F.ColimitTypeRel ⟨j, x⟩) =
    (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimit.ι F j)) x
-- Mathlib.LinearAlgebra.Dimension.Torsion.Basic
finrank_quotient_eq_of_le_torsion : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {M' : Submodule R M}, M' ≤ Submodule.torsion R M → Module.finrank R (M ⧸ M') = Module.finrank R M
-- Mathlib.Topology.Algebra.Group.CompactOpen
ContinuousMonoidHom.continuous_comp_right : ∀ {A : Type u_2} {B : Type u_3} {C : Type u_4} [inst : Monoid A] [inst_1 : Monoid B] [inst_2 : Monoid C]
  [inst_3 : TopologicalSpace A] [inst_4 : TopologicalSpace B] [inst_5 : TopologicalSpace C] (f : B →ₜ* C),
  Continuous fun g => f.comp g
-- Std.Http.Data.Status
Std.Http.instInhabitedCustomStatus : Inhabited Std.Http.CustomStatus
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
SSet.Subcomplex.Pairing.RankFunction.Cell.mapToSucc.congr_simp : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [inst : LinearOrder ι] {f : P.RankFunction ι}
  [inst_1 : P.IsProper] {j : ι} [inst_2 : SuccOrder ι] [inst_3 : NoMaxOrder ι] (c : f.Cell j), c.mapToSucc = c.mapToSucc
-- Mathlib.Topology.IsLocalHomeomorph
/-- Ranges of continuous local sections of a local homeomorphism
form a basis of the source space.  -/
IsLocalHomeomorph.isTopologicalBasis : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  IsLocalHomeomorph f →
    TopologicalSpace.IsTopologicalBasis {U | ∃ V, IsOpen V ∧ ∃ s, f ∘ ⇑s = Subtype.val ∧ Set.range ⇑s = U}
-- Mathlib.Algebra.Lie.Weights.Cartan
LieAlgebra.eq_rootSpace_zero_iff_isCartan : ∀ (R : Type u_1) (L : Type u_2) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  (H : LieSubalgebra R L) [inst_3 : LieRing.IsNilpotent ↥H] [IsNoetherian R L],
  H.toLieSubmodule = LieAlgebra.rootSpace H 0 ↔ H.IsCartanSubalgebra
-- Aesop.Tree.Check
_private.Aesop.Tree.Check.0.Aesop.MVarClusterRef.checkMVars.checkDroppedMVars : Aesop.Rapp → Lean.MetaM Unit
-- Std.Data.ExtDHashMap.Basic
/-- Retrieves the mapping for the given key. Ensures that such a mapping exists by requiring a proof of
`a ∈ m`.
 -/
Std.ExtDHashMap.Const.get : {α : Type u} →
  {x : BEq α} →
    {x_1 : Hashable α} →
      {β : Type v} →
        [inst : EquivBEq α] → [inst_1 : LawfulHashable α] → (m : Std.ExtDHashMap α fun x => β) → (a : α) → a ∈ m → β
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.infiniteNeg_mul_infinitePos : ∀ {x y : ℝ*}, x.InfiniteNeg → y.InfinitePos → (x * y).InfiniteNeg
-- Mathlib.RingTheory.RamificationInertia.Inertia
/-- **Alias** of `Ideal.inertiaDeg'_eq_inertiaDeg`. -/
Ideal.inertiaDeg_eq_inertiaDeg' : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R)
  (q : Ideal S) [q.LiesOver p] [p.IsMaximal] [q.IsMaximal], p.inertiaDeg' q = q.inertiaDeg R
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.size_filterMap_eq_size_iff : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {γ : Type w} {m : Std.DHashMap.Raw α fun x => β}
  [EquivBEq α] [LawfulHashable α] {f : α → β → Option γ},
  m.WF →
    ((Std.DHashMap.Raw.filterMap f m).size = m.size ↔
      ∀ (k : α) (h : k ∈ m), (f (m.getKey k h) (Std.DHashMap.Raw.Const.get m k h)).isSome = true)
-- Mathlib.Topology.UnitInterval
/-- `Set.projIcc` is a contraction.  -/
Set.abs_projIcc_sub_projIcc : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [IsOrderedAddMonoid α] {a b c d : α} (h : a ≤ b),
  |↑(Set.projIcc a b h c) - ↑(Set.projIcc a b h d)| ≤ |c - d|
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
nnnorm_cfc_nnreal_lt_iff : ∀ {A : Type u_1} [inst : NormedRing A] [inst_1 : StarRing A] [inst_2 : NormedAlgebra ℝ A] [inst_3 : PartialOrder A]
  [inst_4 : StarOrderedRing A] [inst_5 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
  [inst_6 : NonnegSpectrumClass ℝ A] (f : NNReal → NNReal) (a : A) {c : NNReal},
  0 < c →
    autoParam (ContinuousOn f (spectrum NNReal a)) nnnorm_cfc_nnreal_lt_iff._auto_1 →
      autoParam (0 ≤ a) nnnorm_cfc_nnreal_lt_iff._auto_3 → (‖cfc f a‖₊ < c ↔ ∀ x ∈ spectrum NNReal a, f x < c)
-- Mathlib.NumberTheory.LegendreSymbol.ZModChar
/-- `χ₄` takes values in `{0, 1, -1}`  -/
ZMod.isQuadratic_χ₄ : ZMod.χ₄.IsQuadratic
-- Mathlib.RingTheory.KrullDimension.Basic
instIsMaximalOfIsPrimeOfKrullDimLEOfNatNat : ∀ {R : Type u_1} [inst : CommSemiring R] (I : Ideal R) [I.IsPrime] [Ring.KrullDimLE 0 R], I.IsMaximal
-- Mathlib.Order.Interval.Finset.Defs
Finset.Ioi_eq_Ioc : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] [inst_2 : OrderTop α] (a : α),
  Finset.Ioi a = Finset.Ioc a ⊤
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Products
CategoryTheory.Limits.ι_comp_sigmaObjIso_inv_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} D]
  {α : Type w} [inst_2 : CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete α) C]
  (f : α → CategoryTheory.Functor D C) (d : D) (s : α) {Z : C} (h : (∐ f).obj d ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun s => (f s).obj d) s)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.sigmaObjIso f d).inv h) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.Sigma.ι f s).app d) h
-- Lean.PrettyPrinter.Delaborator.Builtins
/-- Wraps the identifier (or identifier with explicit universe levels) with `@` if `pp.analysis.blockImplicit` is set to true.
 -/
Lean.PrettyPrinter.Delaborator.maybeAddBlockImplicit : Lean.Syntax → Lean.PrettyPrinter.Delaborator.DelabM Lean.Syntax
-- Mathlib.LinearAlgebra.Dual.Lemmas
Subspace.dualPairing_eq : ∀ {K : Type u_1} {V₁ : Type u_2} [inst : Field K] [inst_1 : AddCommGroup V₁] [inst_2 : Module K V₁] (W : Subspace K V₁),
  Submodule.dualPairing W = ↑W.quotAnnihilatorEquiv
-- Mathlib.NumberTheory.HeckeRing.Defs
HeckeCosetModule.ext_iff : ∀ {G : Type u_1} [inst : Group G] {Δ : Submonoid G} {H₁ H₂ : Subgroup G} {Z : Type u_3} [inst_1 : Zero Z]
  {f g : HeckeCosetModule Δ H₁ H₂ Z}, f = g ↔ ∀ (D : HeckeCoset Δ H₁ H₂), f D = g D
-- Mathlib.Topology.UniformSpace.Equicontinuity
/-- If `𝓕 : ι → X → α` tends to `f : X → α` *pointwise on `S : Set X`* along some nontrivial
filter, and if the family `𝓕` is equicontinuous, then the limit is continuous on `S`.  -/
Filter.Tendsto.continuousOn_of_equicontinuousOn : ∀ {ι : Type u_1} {X : Type u_3} {α : Type u_6} [tX : TopologicalSpace X] [uα : UniformSpace α] {l : Filter ι} [l.NeBot]
  {F : ι → X → α} {f : X → α} {S : Set X},
  (∀ x ∈ S, Filter.Tendsto (fun x_1 => F x_1 x) l (nhds (f x))) → EquicontinuousOn F S → ContinuousOn f S
-- Mathlib.AlgebraicGeometry.Normalization
AlgebraicGeometry.Scheme.Hom.inr_toNormalization_normalizationCoprodIso_inv : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.QuasiCompact f]
  [inst_1 : AlgebraicGeometry.QuasiSeparated f] {U V : AlgebraicGeometry.Scheme} {iU : U ⟶ X} {iV : V ⟶ X}
  (e : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk iU iV))
  [inst_2 : AlgebraicGeometry.QuasiCompact iU] [inst_3 : AlgebraicGeometry.QuasiSeparated iU]
  [inst_4 : AlgebraicGeometry.QuasiCompact iV] [inst_5 : AlgebraicGeometry.QuasiSeparated iV],
  CategoryTheory.CategoryStruct.comp iV
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.toNormalization f)
        (AlgebraicGeometry.Scheme.Hom.normalizationCoprodIso f e).inv) =
    CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.Scheme.Hom.toNormalization (CategoryTheory.CategoryStruct.comp iV f))
      CategoryTheory.Limits.coprod.inr
-- Init.Data.UInt.Lemmas
USize.two_mul : ∀ {a : USize}, 2 * a = a + a
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.image_const_mul_Iic : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] (a b : α),
  (fun x => a * x) '' Set.Iic b = Set.Iic (a * b)
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
HasLineDerivWithinAt.hasLineDerivAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type u_3} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E] {f : E → F}
  {f' : F} {s : Set E} {x v : E}, HasLineDerivWithinAt 𝕜 f f' s x v → s ∈ nhds x → HasLineDerivAt 𝕜 f f' x v
-- Init.Notation
/-- The `@[coe]` attribute on a function (which should also appear in a
`instance : Coe A B := ⟨myFn⟩` declaration) allows the delaborator to show
applications of this function as `↑` when printing expressions.
 -/
Lean.Attr.coe : Lean.ParserDescr
-- Mathlib.Algebra.Group.Pi.Lemmas
MonoidHom.piMap_apply : ∀ {ι : Type u_1} {M : ι → Type u_3} {N : ι → Type u_4} [inst : (i : ι) → MulOneClass (M i)]
  [inst_1 : (i : ι) → MulOneClass (N i)] (g : (i : ι) → M i →* N i) (x : (i : ι) → M i) (i : ι),
  (MonoidHom.piMap g) x i = (g i) (x i)
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- A category `HasCoequalizers` if it has all colimits of shape `WalkingParallelPair`, i.e. if it
has a coequalizer for every parallel pair of morphisms.  -/
CategoryTheory.Limits.HasCoequalizers : (C : Type u) → [CategoryTheory.Category.{v, u} C] → Prop
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- The minimal distance to a set (as `ℝ≥0`) is Lipschitz in point with constant 1  -/
Metric.lipschitz_infNndist_pt : ∀ {α : Type u} [inst : PseudoMetricSpace α] (s : Set α), LipschitzWith 1 fun x => Metric.infNndist x s
-- Mathlib.RingTheory.Algebraic.Basic
Algebra.IsAlgebraic.tower_bot_of_injective : ∀ {R : Type u_3} {S : Type u_4} {A : Type u_5} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Ring A]
  [inst_3 : Algebra R S] [inst_4 : Algebra S A] [inst_5 : Algebra R A] [IsScalarTower R S A] [Algebra.IsAlgebraic R A],
  Function.Injective ⇑(algebraMap S A) → Algebra.IsAlgebraic R S
-- Mathlib.CategoryTheory.Bicategory.Product
CategoryTheory.Bicategory.prod_id_snd : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C] (X : B × C),
  (CategoryTheory.CategoryStruct.id X).2 = CategoryTheory.CategoryStruct.id X.2
-- Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
/-- The series `∑ z^n/n` converges to `-log (1-z)` on the open unit disk.  -/
Complex.hasSum_taylorSeries_neg_log : ∀ {z : ℂ}, ‖z‖ < 1 → HasSum (fun n => z ^ n / ↑n) (-Complex.log (1 - z))
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.coeff_mul_X' : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : DecidableEq σ] (m : σ →₀ ℕ) (s : σ)
  (p : MvPolynomial σ R),
  MvPolynomial.coeff m (p * MvPolynomial.X s) = if s ∈ m.support then MvPolynomial.coeff (m - fun₀ | s => 1) p else 0
-- Lean.Meta.Sym.SymM
Lean.Meta.Sym.instInhabitedConfig.default : Lean.Meta.Sym.Config
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.rpow_inv_natCast_pow : ∀ {n : ℕ}, n ≠ 0 → ∀ (x : ENNReal), (x ^ (↑n)⁻¹) ^ n = x
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get!_ofList_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : Inhabited α] {l : List α} {k k' : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l → k ∈ l → (Std.TreeSet.Raw.ofList l cmp).get! k' = k
-- Mathlib.Analysis.Calculus.Implicit
ImplicitFunctionData.range_rightDeriv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : CompleteSpace E] {F : Type u_3} [inst_4 : NormedAddCommGroup F]
  [inst_5 : NormedSpace 𝕜 F] [inst_6 : CompleteSpace F] {G : Type u_4} [inst_7 : NormedAddCommGroup G]
  [inst_8 : NormedSpace 𝕜 G] [inst_9 : CompleteSpace G] (self : ImplicitFunctionData 𝕜 E F G),
  (↑self.rightDeriv).range = ⊤
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.refl_apply : ∀ (R₁ : Type u_1) [inst : Semiring R₁] (M₁ : Type u_4) [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  [inst_3 : Module R₁ M₁] (x : M₁), (ContinuousLinearEquiv.refl R₁ M₁) x = x
-- Init.Core
Singleton.mk : {α : outParam (Type u)} → {β : Type v} → (α → β) → Singleton α β
-- Mathlib.Order.Bounds.Basic
/-- A set `s` is not bounded above if and only if for each `x` there exists `y ∈ s` such that `x`
is not greater than or equal to `y`. This version only assumes `Preorder` structure and uses
`¬(y ≤ x)`. A version for linear orders is called `not_bddAbove_iff`.  -/
not_bddAbove_iff' : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α}, ¬BddAbove s ↔ ∀ (x : α), ∃ y ∈ s, ¬y ≤ x