mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Nat.Lemmas
Nat.instAssociativeMax : Std.Associative max
-- Lean.LibrarySuggestions.Basic
/-- Combine two premise selectors, returning the best suggestions.  -/
Lean.LibrarySuggestions.Selector.combine : Lean.LibrarySuggestions.Selector → Lean.LibrarySuggestions.Selector → Lean.LibrarySuggestions.Selector
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.lt_pred_iff_succ_lt : ∀ {a b : Ordinal.{u_4}}, a < b.pred ↔ Order.succ a < b
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof.subst1.sizeOf_spec : ∀ (k : ℤ) (c₁ : Lean.Meta.Grind.Arith.Linear.EqCnstr) (c₂ : Lean.Meta.Grind.Arith.Linear.DiseqCnstr),
  sizeOf (Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof.subst1 k c₁ c₂) = 1 + sizeOf k + sizeOf c₁ + sizeOf c₂
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
Mathlib.Tactic.BicategoryLike.WhiskerRight.of.injEq : ∀ (η η_1 : Mathlib.Tactic.BicategoryLike.Atom),
  (Mathlib.Tactic.BicategoryLike.WhiskerRight.of η = Mathlib.Tactic.BicategoryLike.WhiskerRight.of η_1) = (η = η_1)
-- Lean.Meta.InferType
/-- Check if `e` is a proof, i.e. the type of `e` is a proposition.  -/
Lean.Meta.isProof : Lean.Expr → Lean.MetaM Bool
-- Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
CategoryTheory.ObjectProperty.isoMk_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) {X Y : P.FullSubcategory}
  (e : X.obj ≅ Y.obj), (P.isoMk e).hom = CategoryTheory.ObjectProperty.homMk e.hom
-- Mathlib.CategoryTheory.Distributive.Monoidal
/-- The canonical left distributivity isomorphism  -/
CategoryTheory.leftDistrib : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v, u_1} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.Limits.HasBinaryCoproducts C] →
        [CategoryTheory.IsMonoidalLeftDistrib C] →
          (X Y Z : C) →
            CategoryTheory.MonoidalCategoryStruct.tensorObj X Y ⨿ CategoryTheory.MonoidalCategoryStruct.tensorObj X Z ≅
              CategoryTheory.MonoidalCategoryStruct.tensorObj X (Y ⨿ Z)
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.distinguished_cocone_triangle₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (P : CategoryTheory.ObjectProperty C) [P.IsTriangulatedClosed₂] {X Z : C}
  (c : Z ⟶ (CategoryTheory.shiftFunctor C 1).obj X),
  P X →
    P Z →
      ∃ Y,
        ∃ (_ : P Y),
          ∃ a b,
            CategoryTheory.Pretriangulated.Triangle.mk a b c ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
-- Init.Data.Nat.Lemmas
Nat.add_eq_two_iff : ∀ {m n : ℕ}, m + n = 2 ↔ m = 0 ∧ n = 2 ∨ m = 1 ∧ n = 1 ∨ m = 2 ∧ n = 0
-- Init.Data.Ord.String
String.instTransOrd : Std.TransOrd String
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
/-- The orthogonal projection is symmetric.  -/
Submodule.starProjection_isSymmetric : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : Submodule 𝕜 E) [inst_3 : K.HasOrthogonalProjection], (↑K.starProjection).IsSymmetric
-- Mathlib.CategoryTheory.Idempotents.Karoubi
/-- The category `Karoubi C` is preadditive if `C` is.  -/
CategoryTheory.Idempotents.instPreadditiveKaroubi : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [CategoryTheory.Preadditive C] → CategoryTheory.Preadditive (CategoryTheory.Idempotents.Karoubi C)
-- Mathlib.Algebra.Group.Submonoid.Defs
AddSubmonoid.instTop.eq_1 : ∀ {M : Type u_1} [inst : AddZeroClass M],
  AddSubmonoid.instTop = { top := { carrier := Set.univ, add_mem' := ⋯, zero_mem' := ⋯ } }
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RatAddSound
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.entails_of_irrelevant_assignment : ∀ {n : ℕ} {p : Std.Tactic.BVDecide.LRAT.Internal.PosFin n → Bool}
  {c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n}
  {l : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)},
  Std.Tactic.BVDecide.LRAT.Internal.Entails.eval p (c.delete l.negate) →
    Std.Tactic.BVDecide.LRAT.Internal.Entails.eval (fun v => if v = l.1 then l.2 else p v) (c.delete l.negate)
-- Mathlib.NumberTheory.SelbergSieve
/-- `errSum μ⁺` is the error term in the upper bound on `sifted_sum`.  -/
BoundingSieve.errSum : {s : BoundingSieve} → (ℕ → ℝ) → ℝ
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
Lean.Meta.Grind.Arith.Cutsat.ToIntM.Context : Type
-- Mathlib.LinearAlgebra.DFinsupp
/-- `DFinsupp.equivCongrLeft` as a linear equivalence.

This is the `DFinsupp` version of `Finsupp.domLCongr`.  -/
DFinsupp.domLCongr : {ι : Type u_1} →
  {ι' : Type u_2} →
    {R : Type u_3} →
      {M : ι → Type u_5} →
        [inst : Semiring R] →
          [inst_1 : (i : ι) → AddCommMonoid (M i)] →
            [inst_2 : (i : ι) → Module R (M i)] → (e : ι ≃ ι') → (Π₀ (i : ι), M i) ≃ₗ[R] Π₀ (i : ι'), M (e.symm i)
-- Mathlib.MeasureTheory.Group.Action
MeasureTheory.measure_symmDiff_inv_smul : ∀ {G : Type u} {α : Type w} {m : MeasurableSpace α} [inst : Group G] [inst_1 : MulAction G α]
  (μ : MeasureTheory.Measure α) [MeasureTheory.SMulInvariantMeasure G α μ] (c : G) (s t : Set α),
  μ (symmDiff s (c⁻¹ • t)) = μ (symmDiff (c • s) t)
-- Mathlib.Data.W.Constructions
WType.Listα.cons.sizeOf_spec : ∀ {γ : Type u} [inst : SizeOf γ] (a : γ), sizeOf (WType.Listα.cons a) = 1 + sizeOf a
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.one_def : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R], 1 = (MvPolynomial.monomial 0) 1
-- Init.Prelude
HMul.mk : {α : Type u} → {β : Type v} → {γ : outParam (Type w)} → (α → β → γ) → HMul α β γ
-- Mathlib.GroupTheory.Index
Subgroup.index_inf_le : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G}, (H ⊓ K).index ≤ H.index * K.index
-- Init.Data.String.Basic
/-- Copies a region of a string to a new string.

The region of `s` from `b` (inclusive) to `e` (exclusive) is copied to a newly-allocated `String`.

If `b`'s offset is greater than or equal to that of `e`, then the resulting string is `""`.

If possible, prefer `String.slice`, which avoids the allocation.
 -/
String.extract : {s : String} → s.Pos → s.Pos → String
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
MulRingSeminorm.mk.sizeOf_spec : ∀ {R : Type u_2} [inst : NonAssocRing R] [inst_1 : SizeOf R] (toAddGroupSeminorm : AddGroupSeminorm R)
  (map_one' : toAddGroupSeminorm.toFun 1 = 1)
  (map_mul' : ∀ (x y : R), toAddGroupSeminorm.toFun (x * y) = toAddGroupSeminorm.toFun x * toAddGroupSeminorm.toFun y),
  sizeOf { toAddGroupSeminorm := toAddGroupSeminorm, map_one' := map_one', map_mul' := map_mul' } =
    1 + sizeOf toAddGroupSeminorm + sizeOf map_one'
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.monMonoidalStruct : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [CategoryTheory.BraidedCategory C] → CategoryTheory.MonoidalCategoryStruct (CategoryTheory.Mon C)
-- Mathlib.Dynamics.SymbolicDynamics.Basic
SymbolicDynamics.FullShift.shift.eq_1 : ∀ {A : Type u_1} {G : Type u_2} [inst : AddMonoid G] (g : G) (x : G → A) (h : G),
  SymbolicDynamics.FullShift.shift g x h = x (g + h)
-- Mathlib.Order.Hom.Basic
OrderEmbedding.ltEmbedding.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (f : α ↪o β),
  f.ltEmbedding = { toEmbedding := f.toEmbedding, map_rel_iff' := ⋯ }
-- Mathlib.Order.Category.BddOrd
/-- Construct a bundled `BddOrd` from the underlying type and typeclass.  -/
BddOrd.of : (X : Type u_1) → [inst : PartialOrder X] → [BoundedOrder X] → BddOrd
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalSubsemiring.toSubsemigroup_strictMono : ∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R], StrictMono NonUnitalSubsemiring.toSubsemigroup
-- Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Subgroup.relindex_adjoinNegOne_eq_two : ∀ {n : Type u_1} [inst : Fintype n] [inst_1 : DecidableEq n] {R : Type u_2} [inst_2 : Ring R] {𝒢 : Subgroup (GL n R)},
  -1 ∉ 𝒢 → 𝒢.relIndex 𝒢.adjoinNegOne = 2
-- Mathlib.RingTheory.Valuation.Basic
AddValuation.map_sub_swap : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀] (v : AddValuation R Γ₀)
  (x y : R), v (x - y) = v (y - x)
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
/-- The associator isomorphism for the monoidal structure on `AugmentedSimplexCategory`  -/
AugmentedSimplexCategory.associator : (x y z : AugmentedSimplexCategory) → (x.tensorObj y).tensorObj z ≅ x.tensorObj (y.tensorObj z)
-- Mathlib.LinearAlgebra.Prod
LinearMap.ker_prod_ker_le_ker_coprod : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {M₂ : Type u_3}
  [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M₂] {M₃ : Type u_4} [inst_5 : AddCommMonoid M₃] [inst_6 : Module R M₃]
  (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₃), f.ker.prod g.ker ≤ (f.coprod g).ker
-- Mathlib.Algebra.Category.MonCat.Colimits
MonCat.Colimits.cocone_naturality_components : ∀ {J : Type v} [inst : CategoryTheory.Category.{u, v} J] (F : CategoryTheory.Functor J MonCat) (j j' : J) (f : j ⟶ j')
  (x : ↑(F.obj j)),
  (CategoryTheory.ConcreteCategory.hom (MonCat.Colimits.coconeMorphism F j'))
      ((CategoryTheory.ConcreteCategory.hom (F.map f)) x) =
    (CategoryTheory.ConcreteCategory.hom (MonCat.Colimits.coconeMorphism F j)) x
-- Mathlib.MeasureTheory.Integral.Regular
/-- Given an inner regular finite measure, the measure of an open set is the supremum of the
integrals of nonnegative continuous functions supported in this set and bounded by `1`.  -/
IsOpen.measure_eq_biSup_integral_continuous : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] [BorelSpace X] [T2Space X] {U : Set X},
  IsOpen U →
    ∀ (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ] [μ.InnerRegularCompactLTTop] [NormalSpace X],
      μ U =
        ⨆ f,
          ⨆ (_ : Continuous f),
            ⨆ (_ : Set.EqOn f 0 Uᶜ), ⨆ (_ : 0 ≤ f), ⨆ (_ : f ≤ 1), ENNReal.ofReal (∫ (x : X), f x ∂μ)
-- Std.Http.Data.Chunk
/-- A proposition stating that `s` is a valid chunk-extension name: every character in `s` is an
HTTP token character and `s` is non-empty.

Reference: https://httpwg.org/specs/rfc9112.html#chunked.extension
 -/
Std.Http.Chunk.IsValidExtensionName : String → Prop
-- Std.Data.DTreeMap.Internal.Model
/-- Model implementation of the `getEntry?` function.
Internal implementation detail of the tree map
 -/
Std.DTreeMap.Internal.Impl.getEntry?ₘ : {α : Type u} → {β : α → Type v} → [Ord α] → Std.DTreeMap.Internal.Impl α β → α → Option ((a : α) × β a)
-- Mathlib.GroupTheory.Perm.MaximalSubgroups
/-- `MulAction.stabilizer (Perm α) s` is a maximal subgroup of `Perm α`,
provided `s` and `sᶜ` are nonempty, and `Nat.card α ≠ 2 * Nat.card s`.

This is the intransitive case of the O'Nan–Scott classification.  -/
Equiv.Perm.isCoatom_stabilizer : ∀ {α : Type u_2} [Finite α] {s : Set α},
  s.Nonempty → sᶜ.Nonempty → Nat.card α ≠ 2 * s.ncard → IsCoatom (MulAction.stabilizer (Equiv.Perm α) s)
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.instCommRing : (K : Type u) → [inst : CommRing K] → CommRing (RatFunc K)
-- Mathlib.LinearAlgebra.Ray
exists_pos_right_iff_sameRay_and_ne_zero : ∀ {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}, y ≠ 0 → ((∃ r, 0 < r ∧ x = r • y) ↔ SameRay R x y ∧ x ≠ 0)
-- Init.Data.List.Basic
List.Perm.below.nil : ∀ {α : Type u} {motive : (a a_1 : List α) → a.Perm a_1 → Prop}, List.Perm.below ⋯
-- Mathlib.Order.SuccPred.Tree
/-- All of the immediate subtrees of a given rooted tree, that is subtrees which are rooted at a direct
child of the root (or, order-theoretically, at an atom).
 -/
RootedTree.subtrees : (t : RootedTree) → Set (SubRootedTree t)
-- Mathlib.Geometry.Manifold.LocalSourceTargetProperty
/-- A choice of chart on the target `N` of the local property `P` of `f` at `x`:
w.r.t. this chart and `domChart`, `f` has the local property `P` at `x`.  -/
Manifold.LocalPresentationAt.codChart : {𝕜 : Type u_1} →
  {E : Type u_2} →
    {F : Type u_4} →
      {H : Type u_6} →
        {G : Type u_8} →
          [inst : NontriviallyNormedField 𝕜] →
            [inst_1 : NormedAddCommGroup E] →
              [inst_2 : NormedSpace 𝕜 E] →
                [inst_3 : NormedAddCommGroup F] →
                  [inst_4 : NormedSpace 𝕜 F] →
                    [inst_5 : TopologicalSpace H] →
                      [inst_6 : TopologicalSpace G] →
                        {I : ModelWithCorners 𝕜 E H} →
                          {J : ModelWithCorners 𝕜 F G} →
                            {M : Type u_10} →
                              {N : Type u_12} →
                                [inst_7 : TopologicalSpace M] →
                                  [inst_8 : ChartedSpace H M] →
                                    [inst_9 : TopologicalSpace N] →
                                      [inst_10 : ChartedSpace G N] →
                                        {n : WithTop ℕ∞} →
                                          {f : M → N} →
                                            {x : M} →
                                              {P :
                                                  (M → N) →
                                                    OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop} →
                                                Manifold.LocalPresentationAt I J n f x P → OpenPartialHomeomorph N G
-- Lean.Class
/-- Compute positions of universe level parameters that only appear in output parameter types.

During type class resolution, the cache key for a query like
`HAppend.{0, 0, ?u} (BitVec 8) (BitVec 8) ?m` should be independent of the specific
metavariable IDs in output parameter positions. To achieve this, output parameter arguments
are erased from the cache key. However, universe levels that only appear in output parameter
types (e.g., `?u` corresponding to the result type's universe) must also be erased to avoid
cache misses when the same query is issued with different universe metavariable IDs.

This function identifies which universe level parameter positions are "output-only" by
collecting all level param names that appear in non-output parameter domains, then returning
the positions of any level params not in that set.
 -/
_private.Lean.Class.0.Lean.computeOutLevelParams : Lean.Expr → Array ℕ → List Lean.Name → Array ℕ
-- Mathlib.SetTheory.Cardinal.Subfield
Subfield.cardinalMk_closure : ∀ {α : Type u} (s : Set α) [inst : DivisionRing α] [Infinite ↑s], Cardinal.mk ↥(Subfield.closure s) = Cardinal.mk ↑s
-- Mathlib.Topology.Instances.EReal.Lemmas
EReal.liminf_add_top_of_ne_bot : ∀ {α : Type u_3} {f : Filter α} {u v : α → EReal},
  Filter.liminf u f = ⊤ → Filter.liminf v f ≠ ⊥ → Filter.liminf (u + v) f = ⊤
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.map_edgeFinset_induce_of_support_subset : ∀ {V : Type u_1} {s : Set V} [inst : DecidablePred fun x => x ∈ s] [inst_1 : Fintype V] {G : SimpleGraph V}
  [inst_2 : DecidableRel G.Adj],
  G.support ⊆ s →
    Finset.map (Function.Embedding.subtype fun x => x ∈ s).sym2Map (SimpleGraph.induce s G).edgeFinset = G.edgeFinset
-- Mathlib.NumberTheory.ModularForms.Discriminant
_private.Mathlib.NumberTheory.ModularForms.Discriminant.0.ModularForm.csqrt_I_pow_24 : Complex.I.sqrt ^ 24 = 1
-- Mathlib.Topology.EMetricSpace.Defs
EMetricSpace.ext_iff : ∀ {α : Type u_2} {m m' : EMetricSpace α}, m = m' ↔ m.toEDist = m'.toEDist
-- Mathlib.Topology.Continuous
/-- If a continuous map `f` maps `s` to `t`, then it maps `closure s` to `closure t`.  -/
Set.MapsTo.closure : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {s : Set X}
  {t : Set Y}, Set.MapsTo f s t → Continuous f → Set.MapsTo f (closure s) (closure t)
-- Init.WF
Subrelation.wf : ∀ {α : Sort u} {r q : α → α → Prop}, Subrelation q r → WellFounded r → WellFounded q
-- Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
CategoryTheory.FunctorToTypes.coprod.desc_inl : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F F₁ F₂ : CategoryTheory.Functor C (Type w)} (τ₁ : F₁ ⟶ F)
  (τ₂ : F₂ ⟶ F),
  CategoryTheory.CategoryStruct.comp CategoryTheory.FunctorToTypes.coprod.inl
      (CategoryTheory.FunctorToTypes.coprod.desc τ₁ τ₂) =
    τ₁
-- Lean.Meta.AppBuilder
/-- If `e` is `@congrArg α β a b f h`, returns `α`, `f` and `h`.
Also works if `e` can be turned into such an application (e.g. `congrFun`).
 -/
Lean.Meta.congrArg? : Lean.Expr → Lean.MetaM (Option (Lean.Expr × Lean.Expr × Lean.Expr))
-- Init.Data.UInt.Lemmas
UInt16.ofBitVec_add : ∀ (a b : BitVec 16), { toBitVec := a + b } = { toBitVec := a } + { toBitVec := b }
-- Mathlib.Order.Defs.Unbundled
/-- `Std.Antisymm` as a definition, suitable for use in proofs.  -/
AntiSymmetric : {α : Sort u_1} → (α → α → Prop) → Prop
-- Mathlib.Probability.UniformOn
ProbabilityTheory.uniformOn_disjoint_union : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [MeasurableSingletonClass Ω] {s t u : Set Ω},
  s.Finite →
    t.Finite →
      Disjoint s t →
        (ProbabilityTheory.uniformOn s) u * (ProbabilityTheory.uniformOn (s ∪ t)) s +
            (ProbabilityTheory.uniformOn t) u * (ProbabilityTheory.uniformOn (s ∪ t)) t =
          (ProbabilityTheory.uniformOn (s ∪ t)) u
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.get?_diff : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, (m₁ \ m₂).get? k = if k ∈ m₂ then none else m₁.get? k
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.contains_modify : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp},
  t.WF → ∀ {k k' : α} {f : β → β}, (Std.DTreeMap.Raw.Const.modify t k f).contains k' = t.contains k'
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
_private.Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme.0.AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjMap_ι : ∀ {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) (U V : ↑X.affineOpens) (h : U ≤ V),
  CategoryTheory.CategoryStruct.comp (I.glueDataObjMap h) (I.glueData.ι V) = I.glueData.ι U
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.instNoZeroDivisors : ∀ {R : Type u} [inst : Semiring R] [NoZeroDivisors R], NoZeroDivisors (Polynomial R)
-- Init.Grind.Module.Envelope
Lean.Grind.IntModule.OfNatModule.toQ_smul : ∀ {α : Type u} [inst : Lean.Grind.NatModule α] (n : ℕ) (a : α),
  Lean.Grind.IntModule.OfNatModule.toQ (n • a) = n • Lean.Grind.IntModule.OfNatModule.toQ a
-- Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
SymmetricAlgebra.algebraMap_eq_zero_iff : ∀ {R : Type u_1} (M : Type u_2) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (x : R),
  (algebraMap R (SymmetricAlgebra R M)) x = 0 ↔ x = 0
-- Init.Core
Quotient.ind₂ : ∀ {α : Sort uA} {β : Sort uB} {s₁ : Setoid α} {s₂ : Setoid β} {motive : Quotient s₁ → Quotient s₂ → Prop},
  (∀ (a : α) (b : β), motive ⟦a⟧ ⟦b⟧) → ∀ (q₁ : Quotient s₁) (q₂ : Quotient s₂), motive q₁ q₂
-- Mathlib.MeasureTheory.SpecificCodomains.Pi
MeasureTheory.eval_integral : ∀ {X : Type u_1} {mX : MeasurableSpace X} {μ : MeasureTheory.Measure X} {ι : Type u_2} [inst : Fintype ι]
  {E : ι → Type u_3} [inst_1 : (i : ι) → NormedAddCommGroup (E i)] {f : X → (i : ι) → E i}
  [inst_2 : (i : ι) → NormedSpace ℝ (E i)] [∀ (i : ι), CompleteSpace (E i)],
  (∀ (i : ι), MeasureTheory.Integrable (fun x => f x i) μ) → ∀ (i : ι), (∫ (x : X), f x ∂μ) i = ∫ (x : X), f x i ∂μ
-- Mathlib.AlgebraicTopology.SimplicialSet.Dimension
/-- **Alias** of `SSet.nonDegenerate_eq_empty_of_hasDimensionLT`. -/
SSet.nonDegenerate_eq_bot_of_hasDimensionLT : ∀ (X : SSet) (d : ℕ) [X.HasDimensionLT d] (n : ℕ),
  autoParam (d ≤ n) SSet.nonDegenerate_eq_empty_of_hasDimensionLT._auto_1 → X.nonDegenerate n = ∅
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getD_eq_getD_get? : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] {a : α}
  {fallback : β}, Std.DTreeMap.Const.getD t a fallback = (Std.DTreeMap.Const.get? t a).getD fallback
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
CategoryTheory.Pseudofunctor.DescentData.subtypeCompatibleHomEquiv.eq_1 : ∀ {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) {M N : ↑(F.obj { as := Opposite.op S })},
  CategoryTheory.Pseudofunctor.DescentData.subtypeCompatibleHomEquiv F f =
    { toFun := fun φ => { hom := ↑φ, comm := ⋯ }, invFun := fun g => ⟨g.hom, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.MeasureTheory.SetSemiring
MeasureTheory.IsSetSemiring.disjointOfUnion_props : ∀ {α : Type u_1} {C : Set (Set α)} {J : Finset (Set α)},
  MeasureTheory.IsSetSemiring C →
    ↑J ⊆ C →
      ∃ K,
        (↑J).PairwiseDisjoint K ∧
          (∀ i ∈ J, ↑(K i) ⊆ C) ∧
            (⋃ x ∈ J, ↑(K x)).PairwiseDisjoint id ∧
              (∀ j ∈ J, ⋃₀ ↑(K j) ⊆ j) ∧ (∀ j ∈ J, ∅ ∉ K j) ∧ ⋃₀ ↑J = ⋃₀ ⋃ x ∈ J, ↑(K x)
-- Mathlib.MeasureTheory.Group.Prod
/-- A *left*-invariant measure is quasi-preserved by *right*-addition.
This should not be confused with `(measurePreserving_add_right μ g).quasiMeasurePreserving`.  -/
MeasureTheory.quasiMeasurePreserving_add_right : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [MeasurableAdd₂ G] (μ : MeasureTheory.Measure G)
  [MeasureTheory.SFinite μ] [MeasurableNeg G] [μ.IsAddLeftInvariant] (g : G),
  MeasureTheory.Measure.QuasiMeasurePreserving (fun h => h + g) μ μ
-- Mathlib.RingTheory.LocalRing.ResidueField.Ideal
instLiesOverResidueFieldBotIdeal : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) [inst_1 : I.IsPrime], ⊥.LiesOver I
-- Mathlib.Algebra.Group.TypeTags.Basic
toMul_neg : ∀ {α : Type u} [inst : Inv α] (x : Additive α), Additive.toMul (-x) = (Additive.toMul x)⁻¹
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology
CochainComplex.HomComplex.leftHomologyData'_K_coe : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  (K L : CochainComplex C ℤ) (n m p : ℤ) (hm : n + 1 = m) (hp : m + 1 = p),
  ↑(CochainComplex.HomComplex.leftHomologyData' K L n m p hm hp).K = CochainComplex.HomComplex.Cocycle K L m
-- Std.Data.HashMap.Raw
/-- Checks if a mapping for the given key exists and returns the key if it does, otherwise `none`.
The result in the `some` case is guaranteed to be pointer equal to the key in the map.
 -/
Std.HashMap.Raw.getKey? : {α : Type u} → {β : Type v} → [BEq α] → [Hashable α] → Std.HashMap.Raw α β → α → Option α
-- Mathlib.GroupTheory.Coset.Basic
rightAddCoset_eq_iff : ∀ {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α) {x y : α},
  AddOpposite.op x +ᵥ ↑s = AddOpposite.op y +ᵥ ↑s ↔ y + -x ∈ s
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.interSmaller.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (l₁ l₂ : List ((a : α) × β a)),
  Std.Internal.List.interSmaller l₁ l₂ =
    List.foldl (fun sofar kv => Std.Internal.List.interSmallerFn l₁ sofar kv.fst) [] l₂
-- Mathlib.Topology.Category.TopCat.Adjunctions
TopCat.instIsRightAdjointForgetContinuousMapCarrier : (CategoryTheory.forget TopCat).IsRightAdjoint
-- Mathlib.Data.Set.Sigma
Set.sigma_preimage_right : ∀ {ι : Type u_1} {α : ι → Type u_3} {s : Set ι} {t : (i : ι) → Set (α i)} {β : ι → Type u_6} {g : (i : ι) → β i → α i},
  (s.sigma fun i => g i ⁻¹' t i) = (fun p => ⟨p.fst, g p.fst p.snd⟩) ⁻¹' s.sigma t
-- Mathlib.Algebra.Ring.Basic
AddMonoidHom.coe_mulLeft : ∀ {R : Type u_1} [inst : NonUnitalNonAssocSemiring R] (r : R), ⇑(AddMonoidHom.mulLeft r) = HMul.hMul r