mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.Translate.Core
/-- Return the `relevant_arg` option based on the computed `relevantArg?`
and the given `cfg.relevantArg?`.  -/
Mathlib.Tactic.Translate.getRelevantArg : Mathlib.Tactic.Translate.TranslateData →
  Mathlib.Tactic.Translate.Config →
    Option Mathlib.Tactic.Translate.RelevantArg →
      Lean.Name → optParam Bool true → Lean.CoreM Mathlib.Tactic.Translate.RelevantArg
-- Init.Data.String.Substring
/-- Returns the previous position in a substring, just prior to the given position. If the position is
at the beginning of the substring, it is returned unmodified.

Both the input position and the returned position are interpreted relative to the substring's start
position, not the underlying string.
 -/
Substring.Raw.prev : Substring.Raw → String.Pos.Raw → String.Pos.Raw
-- Mathlib.Data.Set.Disjoint
Set.not_disjoint_iff : ∀ {α : Type u} {s t : Set α}, ¬Disjoint s t ↔ ∃ x ∈ s, x ∈ t
-- Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
/-- The product of two boundaryless manifolds is boundaryless.  -/
ModelWithCorners.BoundarylessManifold.prod : ∀ {𝕜 : 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'] {N : Type u_7}
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace H' N] {J : ModelWithCorners 𝕜 E' H'} [BoundarylessManifold I M]
  [BoundarylessManifold J N], BoundarylessManifold (I.prod J) (M × N)
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- The underlying expression of a normalized 1-morphism.  -/
Mathlib.Tactic.BicategoryLike.NormalizedHom.e : Mathlib.Tactic.BicategoryLike.NormalizedHom → Mathlib.Tactic.BicategoryLike.Mor₁
-- Mathlib.Data.Finsupp.Basic
/-- A version of `sum_mapDomain_index` that takes a bundled `AddMonoidHom`,
rather than separate linearity hypotheses.
 -/
Finsupp.sum_mapDomain_index_addMonoidHom : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_6} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N]
  {f : α → β} {s : α →₀ M} (h : β → M →+ N),
  ((Finsupp.mapDomain f s).sum fun b m => (h b) m) = s.sum fun a m => (h (f a)) m
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.rankPos_iff : ∀ {α : Type u_1} (M : Matroid α), M.RankPos ↔ ¬M.IsBase ∅
-- Mathlib.Algebra.BigOperators.Finprod
MonoidHom.map_finprod_of_injective : ∀ {M : Type u_2} {N : Type u_3} {α : Sort u_4} [inst : CommMonoid M] [inst_1 : CommMonoid N] (g : M →* N),
  Function.Injective ⇑g → ∀ (f : α → M), g (∏ᶠ (i : α), f i) = ∏ᶠ (i : α), g (f i)
-- Mathlib.Analysis.Convex.Deriv
ConcaveOn.slope_le_rightDeriv : ∀ {S : Set ℝ} {f : ℝ → ℝ} {x y : ℝ},
  ConcaveOn ℝ S f →
    x ∈ S → y ∈ S → x < y → DifferentiableWithinAt ℝ f (Set.Ioi x) x → slope f x y ≤ derivWithin f (Set.Ioi x) x
-- Mathlib.Topology.Sets.Order
ClopenUpperSet.isClopen : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LE α] (s : ClopenUpperSet α), IsClopen ↑s
-- Std.Sat.AIG.CachedLemmas
_private.Std.Sat.AIG.CachedLemmas.0.Std.Sat.AIG.mkGateCached.go.match_1.eq_4 : ∀ (motive : Option Bool → Option Bool → Sort u_1) (x : Option Bool) (h_1 : (x : Option Bool) → motive (some false) x)
  (h_2 : (x : Option Bool) → motive x (some false)) (h_3 : (x : Option Bool) → motive (some true) x)
  (h_4 : (x : Option Bool) → motive x (some true)) (h_5 : (x x_1 : Option Bool) → motive x x_1),
  (x = some false → False) →
    (x = some true → False) →
      (match x, some true with
        | some false, x => h_1 x
        | x, some false => h_2 x
        | some true, x => h_3 x
        | x, some true => h_4 x
        | x, x_3 => h_5 x x_3) =
        h_4 x
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.self_le_maxKey!_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited α]
  {k : α} {v : β}, (cmp k (t.insertIfNew k v).maxKey!).isLE = true
-- Mathlib.RingTheory.MvPolynomial.FreeCommRing
/-- Given a finite set of monomials `monoms : ι → Finset (κ →₀ ℕ)`, the
`genericPolyMap monoms` is an indexed collection of elements of the `FreeCommRing`,
that can be evaluated to any collection `p : ι → MvPolynomial κ R` of
polynomials such that `∀ i, (p i).support ⊆ monoms i`.  -/
FirstOrder.Ring.genericPolyMap : {ι : Type u_1} → {κ : Type u_2} → (monoms : ι → Finset (κ →₀ ℕ)) → ι → FreeCommRing ((i : ι) × ↥(monoms i) ⊕ κ)
-- Init.Data.List.Basic
List.nil_append : ∀ {α : Type u} (as : List α), [] ++ as = as
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.d₃₂_single_one_thd : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u, u, u} k G} (g h : G) (a : ↑A),
  ((CategoryTheory.ConcreteCategory.hom (groupHomology.d₃₂ A)) fun₀ | (g, h, 1) => a) =
    (fun₀ | (h, 1) => (A.ρ g⁻¹) a) - fun₀ | (g * h, 1) => a
-- Mathlib.Geometry.RingedSpace.PresheafedSpace
AlgebraicGeometry.PresheafedSpace.presheaf : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] → (self : AlgebraicGeometry.PresheafedSpace C) → TopCat.Presheaf C ↑self
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.coe_id : ∀ (R : Type u_1) {V : Type u_2} (P : Type u_4) [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : Module R V]
  [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P], ⇑(ContinuousAffineMap.id R P) = id
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.Δ_of_isCharTwoJNeZeroNF_of_char_two : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [W.IsCharTwoJNeZeroNF] [CharP R 2], W.Δ = W.a₆
-- Mathlib.Data.EReal.Basic
EReal.coe_ennreal_nonneg : ∀ (x : ENNReal), 0 ≤ ↑x
-- Mathlib.GroupTheory.Congruence.Defs
/-- The inductively defined smallest additive congruence relation containing
a given binary relation.  -/
addConGen : {M : Type u_1} → [inst : Add M] → (M → M → Prop) → AddCon M
-- Mathlib.Dynamics.Ergodic.MeasurePreserving
MeasureTheory.MeasurePreserving.restrict_image_emb : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μa : MeasureTheory.Measure α}
  {μb : MeasureTheory.Measure β} {f : α → β},
  MeasureTheory.MeasurePreserving f μa μb →
    MeasurableEmbedding f → ∀ (s : Set α), MeasureTheory.MeasurePreserving f (μa.restrict s) (μb.restrict (f '' s))
-- Mathlib.GroupTheory.GroupAction.Defs
MulAction.orbitRel.quotient_eq_of_quotient_subgroup_eq : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] {H : Subgroup G} {a b : α},
  ⟦a⟧ = ⟦b⟧ → ⟦a⟧ = ⟦b⟧
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.decompEquiv.congr_simp : ∀ (R : Type u_1) (V : Type u_3) {W : Type u_4} (Q : Type u_5) [inst : Ring R] [inst_1 : AddCommGroup V]
  [inst_2 : Module R V] [inst_3 : TopologicalSpace V] [inst_4 : IsTopologicalAddGroup V] [inst_5 : AddCommGroup W]
  [inst_6 : Module R W] [inst_7 : TopologicalSpace W] [inst_8 : AddTorsor W Q] [inst_9 : TopologicalSpace Q]
  [inst_10 : IsTopologicalAddTorsor Q], ContinuousAffineMap.decompEquiv R V Q = ContinuousAffineMap.decompEquiv R V Q
-- Mathlib.Topology.Instances.NNReal.Lemmas
/-- The sum over the complement of a finset tends to `0` when the finset grows to cover the whole
space. This does not need a summability assumption, as otherwise all sums are zero.  -/
NNReal.tendsto_tsum_compl_atTop_zero : ∀ {α : Type u_3} (f : α → NNReal), Filter.Tendsto (fun s => ∑' (b : { x // x ∉ s }), f ↑b) Filter.atTop (nhds 0)
-- Mathlib.NumberTheory.Padics.PadicNumbers
Padic.AddValuation.map_mul : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (x y : ℚ_[p]), (x * y).addValuationDef = x.addValuationDef + y.addValuationDef
-- Lean.PrettyPrinter
/-- Generates `MessageData` for a declaration `c` as `c.{<levels>} <params> : <type>`, with terminfo.  -/
Lean.MessageData.signature : Lean.Name → Lean.MessageData
-- Mathlib.GroupTheory.MonoidLocalization.Maps
AddSubmonoid.LocalizationMap.lift_surjective_iff : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N] {P : Type u_3}
  [inst_2 : AddCommMonoid P] (f : S.LocalizationMap N) {g : M →+ P} (hg : ∀ (y : ↥S), IsAddUnit (g ↑y)),
  Function.Surjective ⇑(f.lift hg) ↔ ∀ (v : P), ∃ x, v + g ↑x.2 = g x.1
-- Batteries.Util.ProofWanted
/-- Auto-generate a `declId` for an anonymous `instance_wanted` based on the class head of the
result type. Returns `inst<HeadName>` if free in the current namespace, otherwise
`inst<HeadName>_1`, `inst<HeadName>_2`, … — matching Lean's own anonymous-`instance` naming
style and keeping the name user-resolvable (no macro-scope hygiene suffix).  -/
_private.Batteries.Util.ProofWanted.0.autoInstanceWantedName : Lean.Syntax → Lean.TSyntax `term → Lean.Elab.Command.CommandElabM (Lean.TSyntax `Lean.Parser.Command.declId)
-- Mathlib.Topology.Instances.Matrix
Summable.matrix_diagonal : ∀ {X : Type u_1} {n : Type u_5} {R : Type u_8} [inst : AddCommMonoid R] [inst_1 : TopologicalSpace R]
  {L : SummationFilter X} [inst_2 : DecidableEq n] {f : X → n → R},
  Summable f L → Summable (fun x => Matrix.diagonal (f x)) L
-- Mathlib.AlgebraicTopology.SimplicialSet.Horn
SSet.horn.ι_ι : ∀ {n : ℕ} (i j : Fin (n + 2)) (hij : j ≠ i),
  CategoryTheory.CategoryStruct.comp (SSet.horn.ι i j hij) (SSet.horn (n + 1) i).ι = SSet.stdSimplex.δ j
-- Mathlib.Combinatorics.Matroid.Map
Matroid.instRankFiniteElemRestrictSubtype : ∀ {α : Type u_1} {M : Matroid α} [M.RankFinite] {X : Set α}, (M.restrictSubtype X).RankFinite
-- Mathlib.Topology.Compactness.Compact
/-- If a compact set belongs to a filter and all cluster points in this set and in the filter
lie in a set `s'` then the filter is less than or equal to `𝓝ˢ s'`.  -/
IsCompact.le_nhdsSet_of_clusterPt : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X},
  IsCompact s → ∀ {l : Filter X} {s' : Set X}, s ∈ l → (∀ x ∈ s, ClusterPt x l → x ∈ s') → l ≤ nhdsSet s'
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.FunDecl.collectUsed : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.FunDecl pu → optParam Lean.FVarIdHashSet ∅ → Lean.FVarIdHashSet
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.dec : Lean.FVarId → Lean.Meta.Grind.Arith.Linear.IneqCnstrProof
-- Mathlib.Data.Finset.Sups
Finset.empty_sdiffs : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : GeneralizedBooleanAlgebra α] {t : Finset α}, ∅.diffs t = ∅
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Ioo_union_Icc_eq_Ioc : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c : α}, a < b → b ≤ c → Set.Ioo a b ∪ Set.Icc b c = Set.Ioc a c
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
WeierstrassCurve.Projective.Point.toAffineLift_of_Z_ne_zero : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3 → F} {hP : W.NonsingularLift ⟦P⟧}
  (hPz : P 2 ≠ 0),
  { point := ⟦P⟧, nonsingular := hP }.toAffineLift = WeierstrassCurve.Affine.Point.some (P 0 / P 2) (P 1 / P 2) ⋯
-- Mathlib.Analysis.Calculus.FDeriv.Equiv
ContinuousLinearEquiv.hasFDerivAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {x : E}
  (iso : E ≃L[𝕜] F), HasFDerivAt (⇑iso) (↑iso) x
-- Std.Data.DTreeMap.Raw.Basic
Std.DTreeMap.Raw.instForMSigmaOfMonad : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} → {m : Type w → Type w₂} → [Monad m] → ForM m (Std.DTreeMap.Raw α β cmp) ((a : α) × β a)
-- Init.Data.Vector.Lemmas
Vector.sum_toArray : ∀ {α : Type u_1} {n : ℕ} [inst : Add α] [inst_1 : Zero α] {xs : Vector α n}, xs.toArray.sum = xs.sum
-- Init.Data.String.Basic
String.decodeChar : (s : String) → (byteIdx : ℕ) → (s.toByteArray.utf8DecodeChar? byteIdx).isSome = true → Char
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Polynomial.Monic.quotient_isIntegralElem : ∀ {S : Type u_4} [inst : CommRing S] {g : Polynomial S},
  g.Monic →
    ∀ {I : Ideal (Polynomial S)},
      g ∈ I →
        ((Ideal.Quotient.mk I).comp (algebraMap S (Polynomial S))).IsIntegralElem ((Ideal.Quotient.mk I) Polynomial.X)
-- Init.Data.Int.Linear
Int.Internal.Linear.emod_le : ∀ (x y n : ℤ), Int.Internal.Linear.emod_le_cert y n = true → x % y + n ≤ 0
-- Mathlib.NumberTheory.DiophantineApproximation.Basic
_private.Mathlib.NumberTheory.DiophantineApproximation.Basic.0.Real.convergent.match_1.eq_2 : ∀ (motive : ℝ → ℕ → Sort u_1) (ξ : ℝ) (n : ℕ) (h_1 : (ξ : ℝ) → motive ξ 0) (h_2 : (ξ : ℝ) → (n : ℕ) → motive ξ n.succ),
  (match ξ, n.succ with
    | ξ, 0 => h_1 ξ
    | ξ, n.succ => h_2 ξ n) =
    h_2 ξ n
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Matrix.charmatrix_apply_natDegree_le : ∀ {R : Type u} [inst : CommRing R] {n : Type v} [inst_1 : DecidableEq n] [inst_2 : Fintype n] {M : Matrix n n R}
  (i j : n), (M.charmatrix i j).natDegree ≤ if i = j then 1 else 0
-- Mathlib.Topology.MetricSpace.Contracting
/-- Let `s` be a complete forward-invariant set of a self-map `f`. If `f` contracts on `s`
and `x ∈ s` satisfies `edist x (f x) ≠ ∞`, then `efixedPoint'` is the unique fixed point
of the restriction of `f` to `s ∩ Metric.eball x ∞`.  -/
ContractingWith.efixedPoint' : {α : Type u_1} →
  [inst : EMetricSpace α] →
    {K : NNReal} →
      (f : α → α) →
        {s : Set α} →
          IsComplete s →
            (hsf : Set.MapsTo f s s) →
              ContractingWith K (Set.MapsTo.restrict f s s hsf) → (x : α) → x ∈ s → edist x (f x) ≠ ⊤ → α
-- Init.SimpLemmas
decide_eq_false_iff_not : ∀ {p : Prop} {x : Decidable p}, decide p = false ↔ ¬p
-- Mathlib.Topology.Convenient.Category
TopCat.generatedBy_def : ∀ {ι : Type t} (X : ι → Type u) [inst : (i : ι) → TopologicalSpace (X i)] (Y : TopCat),
  TopCat.generatedBy X Y ↔ Topology.IsGeneratedBy X ↑Y
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.InjectiveInfo.h : Lean.Meta.Grind.InjectiveInfo → Lean.Expr
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.preimage_add : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Add α] [inst_1 : Add β] [inst_2 : FunLike F α β]
  [AddHomClass F α β] (m : F),
  Function.Injective ⇑m → ∀ {s t : Set β}, s ⊆ Set.range ⇑m → t ⊆ Set.range ⇑m → ⇑m ⁻¹' (s + t) = ⇑m ⁻¹' s + ⇑m ⁻¹' t
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.toContinuousMapCLM_apply_apply : ∀ {X : Type u_1} {R : Type u_2} [inst : Zero X] [inst_1 : TopologicalSpace X] [inst_2 : TopologicalSpace R]
  [inst_3 : CommSemiring R] [inst_4 : IsTopologicalSemiring R] (M : Type u_3) [inst_5 : Semiring M]
  [inst_6 : Module M R] [inst_7 : ContinuousConstSMul M R] (f : ContinuousMapZero X R) (a : X),
  ((ContinuousMapZero.toContinuousMapCLM M) f) a = f a
-- Lean.Meta.Sym.Arith.Types
/-- Commutative semirings.  -/
Lean.Meta.Sym.Arith.State.semirings : Lean.Meta.Sym.Arith.State → Array Lean.Meta.Sym.Arith.CommSemiring
-- Init.Data.Int.DivMod.Lemmas
Int.divExact_eq_fdiv : ∀ {a b : ℤ} (h : b ∣ a), a.divExact b h = a.fdiv b
-- Mathlib.Geometry.Euclidean.MongePoint
/-- The distance from the orthocenter to the reflection of the
circumcenter in a side equals the circumradius.  -/
Affine.Triangle.dist_orthocenter_reflection_circumcenter : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (t : Affine.Triangle ℝ P) {i₁ i₂ : Fin 3},
  i₁ ≠ i₂ →
    dist t.orthocenter
        ((EuclideanGeometry.reflection (affineSpan ℝ (t.points '' {i₁, i₂}))) (Affine.Simplex.circumcenter t)) =
      Affine.Simplex.circumradius t
-- Mathlib.Topology.Homeomorph.Defs
/-- Any bijection between discrete spaces is a homeomorphism.  -/
Equiv.toHomeomorphOfDiscrete : {X : Type u_1} →
  {Y : Type u_2} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] → [DiscreteTopology X] → [DiscreteTopology Y] → X ≃ Y → X ≃ₜ Y
-- Mathlib.RingTheory.TwoSidedIdeal.Operations
/-- Pushout of a two-sided ideal. Defined as the span of the image of a two-sided ideal under a ring
homomorphism.
 -/
TwoSidedIdeal.map : {R : Type u_1} →
  {S : Type u_2} →
    [inst : NonUnitalNonAssocRing R] →
      [inst_1 : NonUnitalNonAssocRing S] → {F : Type u_3} → [FunLike F R S] → F → TwoSidedIdeal R → TwoSidedIdeal S
-- Lean.Parser.Basic
/-- Check if the following token is the symbol _or_ identifier `sym`. Useful for
parsing local tokens that have not been added to the token table (but may have
been so by some unrelated code).

For example, the universe `max` Function is parsed using this combinator so that
it can still be used as an identifier outside of universe (but registering it
as a token in a Term Syntax would not break the universe Parser).  -/
Lean.Parser.nonReservedSymbolFnAux : String → String → Lean.Parser.ParserFn
-- Std.Data.Internal.List.Associative
/-- Returns the smallest key in an associative list or `fallback` if the list is empty.  -/
Std.Internal.List.minKeyD : {α : Type u} → {β : α → Type v} → [Ord α] → List ((a : α) × β a) → α → α
-- Mathlib.FieldTheory.Perfect
Function.Commute.eq_1 : ∀ {α : Type u_1} (f g : α → α), Function.Commute f g = Function.Semiconj f g g
-- Mathlib.CategoryTheory.ObjectProperty.LimitsClosure
CategoryTheory.ObjectProperty.isEssentiallySmall_limitsClosure : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) {α : Type t}
  (J : α → Type u') [inst_1 : (a : α) → CategoryTheory.Category.{v', u'} (J a)] (κ : Cardinal.{w}) [Fact κ.IsRegular],
  (∀ (a : α), HasCardinalLT (J a) κ) →
    ∀ [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} P] [CategoryTheory.LocallySmall.{w, v, u} C]
      [Small.{w, t} α] [∀ (a : α), Small.{w, u'} (J a)] [∀ (a : α), CategoryTheory.LocallySmall.{w, v', u'} (J a)],
      CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} (P.limitsClosure J)
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
/-- (Implementation) The isomorphism between the subscheme and the glued scheme.  -/
AlgebraicGeometry.Scheme.IdealSheafData.subschemeIso : {X : AlgebraicGeometry.Scheme} → (I : X.IdealSheafData) → I.subscheme ≅ I.glueData.glued
-- Lean.Data.Json.Basic
Lean.Json.obj.sizeOf_spec : ∀ (kvPairs : Std.TreeMap.Raw String Lean.Json compare), sizeOf (Lean.Json.obj kvPairs) = 1 + sizeOf kvPairs
-- Mathlib.RepresentationTheory.Rep.Basic
/-- An equiv between the underlying representations induce isomorphism between objects in
`Rep k G`.  -/
Rep.mkIso : {k : Type u} →
  {G : Type v} →
    [inst : Semiring k] →
      [inst_1 : Monoid G] →
        {X Y : Type w} →
          [inst_2 : AddCommGroup X] →
            [inst_3 : AddCommGroup Y] →
              [inst_4 : Module k X] →
                [inst_5 : Module k Y] →
                  {ρ : Representation k G X} → {σ : Representation k G Y} → ρ.Equiv σ → (Rep.of ρ ≅ Rep.of σ)
-- Mathlib.Data.Int.ModEq
Int.modEq_zero_iff_dvd : ∀ {n a : ℤ}, a ≡ 0 [ZMOD n] ↔ n ∣ a
-- Lean.Expr
Lean.Expr.updateSort! : Lean.Expr → Lean.Level → Lean.Expr
-- Mathlib.Analysis.Complex.UpperHalfPlane.Basic
UpperHalfPlane.vadd_im : ∀ (x : ℝ) (z : UpperHalfPlane), (x +ᵥ z).im = z.im
-- Mathlib.RingTheory.Ideal.Quotient.Operations
Ideal.pi_mkQ_surjective : ∀ {R : Type u_2} [inst : CommRing R] {ι : Type u_3} [Finite ι] {I : ι → Ideal R},
  Pairwise (Function.onFun IsCoprime I) → Function.Surjective ⇑(LinearMap.pi fun i => Submodule.mkQ (I i))
-- Mathlib.CategoryTheory.Sites.Hypercover.One
/-- Forget the `1`-components of a `OneHypercover`.  -/
CategoryTheory.GrothendieckTopology.OneHypercover.toZeroHypercover : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} → {S : C} → J.OneHypercover S → J.toPrecoverage.ZeroHypercover S
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits
PresheafOfModules.instPreservesLimitsOfShapeModuleCatCarrierObjOppositeRingCatEvaluation : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (R : CategoryTheory.Functor Cᵒᵖ RingCat) (J : Type u₂)
  [inst_1 : CategoryTheory.Category.{v₂, u₂} J] [Small.{v, u₂} J] (X : Cᵒᵖ),
  CategoryTheory.Limits.PreservesLimitsOfShape J (PresheafOfModules.evaluation R X)
-- Mathlib.Data.ENNReal.Inv
/-- See `ENNReal.mul_inv_cancel_right` for a simpler version assuming `b ≠ 0`, `b ≠ ∞`.  -/
ENNReal.mul_inv_cancel_right' : ∀ {a b : ENNReal}, (b = 0 → a = 0) → (b = ⊤ → a = 0) → a * b * b⁻¹ = a
-- Init.Data.Range.Polymorphic.RangeIterator
/-- An efficient `IteratorLoop` instance:
As long as the compiler cannot optimize away the `Option` in the internal state, we use a special
loop implementation.
 -/
Std.Rxo.Iterator.instIteratorLoop : {α : Type u} →
  [inst : Std.PRange.UpwardEnumerable α] →
    [inst_1 : LT α] →
      [inst_2 : DecidableLT α] →
        [Std.PRange.LawfulUpwardEnumerable α] →
          [Std.PRange.LawfulUpwardEnumerableLT α] →
            {n : Type u → Type w} → [Monad n] → Std.IteratorLoop (Std.Rxo.Iterator α) Id n
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.coboundaries₁.val_eq_coe : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{max u u_1, u, u} k G}
  (f : ↥(groupCohomology.coboundaries₁ A)), ↑f = ⇑f
-- Mathlib.Topology.AlexandrovDiscrete
Prod.instAlexandrovDiscrete : ∀ {α : Type u_3} {β : Type u_4} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [AlexandrovDiscrete α]
  [AlexandrovDiscrete β], AlexandrovDiscrete (α × β)
-- Mathlib.Analysis.Normed.Group.AddTorsor
dist_vadd_right : ∀ {V : Type u_2} {P : Type u_3} [inst : SeminormedAddCommGroup V] [inst_1 : PseudoMetricSpace P]
  [inst_2 : NormedAddTorsor V P] (v : V) (x : P), dist x (v +ᵥ x) = ‖v‖
-- Mathlib.Algebra.BigOperators.Finprod
/-- A more general version of `finprod_mem_union` that requires `s ∩ mulSupport f` and
`t ∩ mulSupport f` rather than `s` and `t` to be finite.  -/
finprod_mem_union' : ∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] {f : α → M} {s t : Set α},
  Disjoint s t →
    (s ∩ Function.mulSupport f).Finite →
      (t ∩ Function.mulSupport f).Finite →
        ∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i = (∏ᶠ (i : α) (_ : i ∈ s), f i) * ∏ᶠ (i : α) (_ : i ∈ t), f i
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroup.coe_set_mk : ∀ {G : Type u_1} [inst : AddGroup G] {s : AddSubmonoid G} (h_neg : ∀ {x : G}, x ∈ s.carrier → -x ∈ s.carrier),
  ↑{ toAddSubmonoid := s, neg_mem' := h_neg } = ↑s
-- Lean.Parser.Types
Lean.Parser.SyntaxNodeKindSet.insert : Lean.Parser.SyntaxNodeKindSet → Lean.SyntaxNodeKind → Lean.Parser.SyntaxNodeKindSet
-- Aesop.RuleSet.Name
Aesop.RuleSetName.isReserved : Aesop.RuleSetName → Bool
-- Mathlib.Analysis.Calculus.VectorField
VectorField.lieBracketWithin_swap : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {V W : E → E} {s : Set E},
  VectorField.lieBracketWithin 𝕜 V W s = -VectorField.lieBracketWithin 𝕜 W V s
-- Mathlib.RingTheory.HahnSeries.Addition
HahnSeries.coeff_neg' : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : NegZeroClass R] (x : HahnSeries Γ R),
  (-x).coeff = -x.coeff
-- Mathlib.MeasureTheory.Measure.Restrict
/-- If two measurable sets are `ae_eq` then any proposition that is almost everywhere true on one
is almost everywhere true on the other  -/
MeasureTheory.ae_restrict_of_ae_eq_of_ae_restrict : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : α → Prop},
  s =ᵐ[μ] t → ∀ {p : α → Prop}, (∀ᵐ (x : α) ∂μ.restrict s, p x) → ∀ᵐ (x : α) ∂μ.restrict t, p x
-- Mathlib.Order.Interval.Finset.SuccPred
Finset.Icc_pred_right_eq_Ico : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : LocallyFiniteOrder α] [inst_2 : PredOrder α] [NoMinOrder α] (a b : α),
  Finset.Icc a (Order.pred b) = Finset.Ico a b
-- Mathlib.RingTheory.Extension.ExtendScalars
Algebra.Extension.h1CotangentEquivCotangent.eq_1 : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.Extension R S),
  P.h1CotangentEquivCotangent =
    (P.h1CotangentExtendScalarsEquiv.symm.trans (P.extendScalars.h1CotangentEquivOfSurjective ⋯)).trans
      P.cotangentExtendScalarsEquiv
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.contains_insert : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α],
  m.WF → ∀ {k a : α}, (m.insert k).contains a = (k == a || m.contains a)