mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.FDeriv.Congr
Filter.EventuallyEq.fderivWithin_eq_of_insert : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f f₁ : E → F} {x : E} {s : Set E},
  f₁ =ᶠ[nhdsWithin x (insert x s)] f → fderivWithin 𝕜 f₁ s x = fderivWithin 𝕜 f s x
-- Mathlib.Topology.Category.UniformSpace
UniformSpaceCat.coe_mk : ∀ {X Y : UniformSpaceCat} (f : X.carrier → Y.carrier) (hf : UniformContinuous f), ⇑{ hom' := ⟨f, hf⟩ }.hom = f
-- Mathlib.Order.Monotone.Basic
/-- **Alias** of the reverse direction of `monotone_comp_ofDual_iff`. -/
Antitone.dual_left : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  Antitone f → Monotone (f ∘ ⇑OrderDual.ofDual)
-- Lean.HeadIndex
Lean.HeadIndex.mvar.inj : ∀ {mvarId mvarId_1 : Lean.MVarId}, Lean.HeadIndex.mvar mvarId = Lean.HeadIndex.mvar mvarId_1 → mvarId = mvarId_1
-- Mathlib.Data.Finset.Max
Finset.min'_eq_inf' : ∀ {α : Type u_2} [inst : LinearOrder α] (s : Finset α) (H : s.Nonempty), s.min' H = s.inf' H id
-- Mathlib.Order.Filter.NAry
Filter.map₂_sup_right : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {m : α → β → γ} {f : Filter α} {g₁ g₂ : Filter β},
  Filter.map₂ m f (g₁ ⊔ g₂) = Filter.map₂ m f g₁ ⊔ Filter.map₂ m f g₂
-- Mathlib.Algebra.Group.Action.Defs
IsLeftCancelSMul.left_cancel' : ∀ {G : Type u_9} {P : Type u_10} {inst : SMul G P} [self : IsLeftCancelSMul G P] (a : G) (b c : P),
  a • b = a • c → b = c
-- Std.Data.DHashMap.Internal.Defs
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw.WFImp.buckets_hash_self : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β},
  Std.DHashMap.Internal.Raw.WFImp m → Std.DHashMap.Internal.IsHashSelf m.buckets
-- Lean.Data.LOption
Lean.instInhabitedLOption : {a : Type u_1} → Inhabited (Lean.LOption a)
-- Mathlib.FieldTheory.Minpoly.Field
/-- A technical finiteness result.  -/
minpoly.Fintype.subtypeProd : {E : Type u_3} → {X : Set E} → X.Finite → {L : Type u_4} → (F : E → Multiset L) → Fintype ((x : ↑X) → { l // l ∈ F ↑x })
-- Mathlib.LinearAlgebra.Multilinear.Basic
/-- This expresses the difference between the values of a multilinear map
at two points "close to `x`" in terms of the "derivative" of the multilinear map at `x`
and of "second-order" terms.  -/
MultilinearMap.map_add_sub_map_add_sub_linearDeriv : ∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommGroup (M₁ i)] [inst_2 : AddCommGroup M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] (f : MultilinearMap R M₁ M₂) [inst_5 : DecidableEq ι] [inst_6 : Fintype ι]
  (x h h' : (i : ι) → M₁ i),
  f (x + h) - f (x + h') - (f.linearDeriv x) (h - h') =
    ∑ s with 2 ≤ s.card, (f (s.piecewise h x) - f (s.piecewise h' x))
-- Mathlib.Topology.Algebra.Group.OpenMapping
/-- A surjective morphism of topological groups is open when the source group is sigma-compact and
the target group is a Baire space (for instance a locally compact group).  -/
MonoidHom.isOpenMap_of_sigmaCompact : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G] [SigmaCompactSpace G]
  {H : Type u_3} [inst_4 : Group H] [inst_5 : TopologicalSpace H] [BaireSpace H] [T2Space H] [ContinuousMul H]
  (f : G →* H), Function.Surjective ⇑f → Continuous ⇑f → IsOpenMap ⇑f
-- Mathlib.CategoryTheory.Iso
/-- Composition of two isomorphisms  -/
CategoryTheory.Iso.trans : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {X Y Z : C} → (X ≅ Y) → (Y ≅ Z) → (X ≅ Z)
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.forget_obj : ∀ {ι : Type u_1} (V : Type u) [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] (c : ComplexShape ι) (C : HomologicalComplex V c) (a : ι),
  (HomologicalComplex.forget V c).obj C a = C.X a
-- Init.Prelude
instInhabitedForall : (α : Sort u) → {β : Sort v} → [Inhabited β] → Inhabited (α → β)
-- Mathlib.AlgebraicTopology.DoldKan.Compatibility
AlgebraicTopology.DoldKan.Compatibility.equivalenceUnitIso_eq : ∀ {A : Type u_1} {A' : Type u_2} {B : Type u_3} {B' : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} A'] [inst_2 : CategoryTheory.Category.{v_3, u_3} B]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} B'] {eA : A ≌ A'} {eB : B ≌ B'} {e' : A' ≌ B'}
  {F : CategoryTheory.Functor A B'} {hF : eA.functor.comp e'.functor ≅ F} {G : CategoryTheory.Functor B A}
  {hG : eB.functor.comp e'.inverse ≅ G.comp eA.functor} {ε : eA.functor ≅ F.comp e'.inverse},
  AlgebraicTopology.DoldKan.Compatibility.υ hF = ε →
    (AlgebraicTopology.DoldKan.Compatibility.equivalence hF hG).unitIso =
      AlgebraicTopology.DoldKan.Compatibility.equivalenceUnitIso hG ε
-- Mathlib.NumberTheory.Divisors
Int.divisors_one : Int.divisors 1 = {1, -1}
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.AbelianImages
/-- If a functor preserves kernels and cokernels, it preserves coimage-image comparisons.  -/
CategoryTheory.Abelian.PreservesCoimageImageComparison.iso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] →
            (F : CategoryTheory.Functor C D) →
              [inst_4 : F.PreservesZeroMorphisms] →
                {X Y : C} →
                  (f : X ⟶ Y) →
                    [inst_5 : CategoryTheory.Limits.HasKernel f] →
                      [inst_6 : CategoryTheory.Limits.HasCokernel f] →
                        [inst_7 : CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.π f)] →
                          [inst_8 : CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι f)] →
                            [inst_9 : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) F] →
                              [inst_10 :
                                  CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) F] →
                                [CategoryTheory.Limits.PreservesLimit
                                      (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.cokernel.π f) 0) F] →
                                  [CategoryTheory.Limits.PreservesColimit
                                        (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.kernel.ι f) 0) F] →
                                    [inst_13 :
                                        CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.π (F.map f))] →
                                      [inst_14 :
                                          CategoryTheory.Limits.HasCokernel
                                            (CategoryTheory.Limits.kernel.ι (F.map f))] →
                                        CategoryTheory.Arrow.mk
                                            (F.map (CategoryTheory.Abelian.coimageImageComparison f)) ≅
                                          CategoryTheory.Arrow.mk
                                            (CategoryTheory.Abelian.coimageImageComparison (F.map f))
-- Mathlib.RingTheory.Polynomial.GaussNorm
/-- If `v x = 0 → x = 0` for all `x : R` and `v` is nonnegative, then the Gauss norm is zero if and
only if the polynomial is zero.  -/
Polynomial.gaussNorm_eq_zero_iff : ∀ {R : Type u_1} {F : Type u_2} [inst : Semiring R] [inst_1 : FunLike F R ℝ] (v : F) {c : ℝ} (p : Polynomial R)
  [ZeroHomClass F R ℝ] [NonnegHomClass F R ℝ],
  (∀ (x : R), v x = 0 → x = 0) → 0 < c → (Polynomial.gaussNorm v c p = 0 ↔ p = 0)
-- Mathlib.Data.Multiset.Bind
Multiset.sigma_add : ∀ {α : Type u_1} {σ : α → Type u_4} (s : Multiset α) (t u : (a : α) → Multiset (σ a)),
  (s.sigma fun a => t a + u a) = s.sigma t + s.sigma u
-- Lean.Data.Lsp.TextSync
Lean.Lsp.instFromJsonDidSaveTextDocumentParams.fromJson : Lean.Json → Except String Lean.Lsp.DidSaveTextDocumentParams
-- Mathlib.Combinatorics.Graph.Basic
Graph.exists_isLink_of_mem_edgeSet : ∀ {α : Type u_1} {β : Type u_2} {e : β} {G : Graph α β}, e ∈ G.edgeSet → ∃ x y, G.IsLink e x y
-- Mathlib.MeasureTheory.OuterMeasure.Basic
MeasureTheory.pos_mono : ∀ {α : Type u_1} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {μ : F}
  ⦃s t : Set α⦄, s ⊆ t → 0 < μ s → 0 < μ t
-- Std.Data.HashSet.Raw
/-- Creates a hash set from a list of elements. Note that unlike repeatedly calling `insert`, if the
collection contains multiple elements that are equal (with regard to `==`), then the last element
in the collection will be present in the returned hash set.
 -/
Std.HashSet.Raw.ofList : {α : Type u} → [BEq α] → [Hashable α] → List α → Std.HashSet.Raw α
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.normAtPlace_add_le : ∀ {K : Type u_1} [inst : Field K] (w : NumberField.InfinitePlace K) (x y : NumberField.mixedEmbedding.mixedSpace K),
  (NumberField.mixedEmbedding.normAtPlace w) (x + y) ≤
    (NumberField.mixedEmbedding.normAtPlace w) x + (NumberField.mixedEmbedding.normAtPlace w) y
-- Init.Data.SInt.Lemmas
Int16.ofNat_sub : ∀ (a b : ℕ), b ≤ a → Int16.ofNat (a - b) = Int16.ofNat a - Int16.ofNat b
-- Lean.Meta.BinderNameHint
_private.Lean.Meta.BinderNameHint.0.Lean.Expr.resolveBinderNameHint.go : Lean.Expr → Lean.MonadCacheT Lean.ExprStructEq Lean.Expr (StateT (Array Lean.Name) Lean.CoreM) Lean.Expr
-- Mathlib.Order.TypeTags
WithBot.bot.eq_1 : ∀ {α : Type u_1}, WithBot.bot = { bot := none }
-- Mathlib.Data.Finsupp.Weight
Finsupp.NonTorsionWeight.eq_zero_of_smul_eq_zero : ∀ {σ : Type u_1} {M : Type u_2} {R : Type u_3} {inst : Semiring R} {inst_1 : AddCommMonoid M} {inst_2 : Module R M}
  {w : σ → M} [self : Finsupp.NonTorsionWeight R w] {r : R} {s : σ}, r • w s = 0 → r = 0
-- Mathlib.Topology.List
List.instDiscreteTopology : ∀ {α : Type u_1} [inst : TopologicalSpace α] [DiscreteTopology α], DiscreteTopology (List α)
-- Mathlib.RepresentationTheory.Coinvariants
Representation.Coinvariants.mk_eq_zero : ∀ {k : Type u_1} {G : Type u_2} {V : Type u_3} [inst : CommRing k] [inst_1 : Monoid G] [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] (ρ : Representation k G V) {x : V},
  (Representation.Coinvariants.mk ρ) x = 0 ↔ x ∈ Representation.Coinvariants.ker ρ
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.self_le_maxKey!_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {k : α} {v : β}, (cmp k (t.insert k v).maxKey!).isLE = true
-- Mathlib.Order.UpperLower.Basic
not_bddAbove_Ioi : ∀ {α : Type u_1} [inst : Preorder α] (a : α) [NoMaxOrder α], ¬BddAbove (Set.Ioi a)
-- Init.Coe
instCoeHTCOfCoeHeadOfCoeOTC : {α : Sort u_1} → {β : Sort u_2} → {γ : Sort u_3} → [CoeHead α β] → [CoeOTC β γ] → CoeHTC α γ
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
_private.Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn.0.MeasureTheory.SignedMeasure.someExistsOneDivLT_spec : ∀ {α : Type u_1} [inst : MeasurableSpace α] {s : MeasureTheory.SignedMeasure α} {i : Set α},
  ¬MeasureTheory.VectorMeasure.restrict s i ≤ MeasureTheory.VectorMeasure.restrict 0 i →
    MeasureTheory.SignedMeasure.someExistsOneDivLT✝ s i ⊆ i ∧
      MeasurableSet (MeasureTheory.SignedMeasure.someExistsOneDivLT✝ s i) ∧
        1 / (↑(MeasureTheory.SignedMeasure.findExistsOneDivLT✝ s i) + 1) <
          s (MeasureTheory.SignedMeasure.someExistsOneDivLT✝ s i)
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- **Alias** of `CategoryTheory.Subobject.Classifier.representableBy`.

---

Any subobject classifier `Ω` represents the subobjects functor `Subobject.presheaf`.  -/
CategoryTheory.Classifier.representableBy : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasPullbacks C] →
      (𝒞 : CategoryTheory.Subobject.Classifier C) → (Subobject.presheaf C).RepresentableBy 𝒞.Ω
-- Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.equivFun.eq_1 : ∀ {ι : Type u_1} {R : Type u_3} {M : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Finite ι] (b : Module.Basis ι R M),
  b.equivFun =
    b.repr ≪≫ₗ
      let __src := Finsupp.equivFunOnFinite;
      { toFun := DFunLike.coe, map_add' := ⋯, map_smul' := ⋯, invFun := __src.invFun, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientGroup.quotientKerEquivRange.eq_1 : ∀ {G : Type u} [inst : Group G] {H : Type v} [inst_1 : Group H] (φ : G →* H),
  QuotientGroup.quotientKerEquivRange φ = MulEquiv.ofBijective (QuotientGroup.rangeKerLift φ) ⋯
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getKey?_filter : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] {f : α → β → Bool} {k : α} (h : m.WF),
  (Std.DHashMap.Raw.filter f m).getKey? k = (m.getKey? k).pfilter fun x h' => f x (Std.DHashMap.Raw.Const.get m x ⋯)
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.toAdd_unzero_le_of_lt_ofAdd : ∀ {α : Type u_1} [inst : Preorder α] {a : WithZero (Multiplicative α)} {b : α} (ha : a ≠ 0),
  a ≤ ↑(Multiplicative.ofAdd b) → Multiplicative.toAdd (WithZero.unzero ha) ≤ b
-- Std.Data.HashMap.IteratorLemmas
_private.Std.Data.HashMap.IteratorLemmas.0.Std.HashMap.toList_inner : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap α β},
  m.inner.toList = List.map (fun e => ⟨e.1, e.2⟩) m.toList
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
/-- The even elliptic relator `ER(m + 1, m - 1, 1, 0)` for `m ∈ ℤ`.  -/
IsEllipticNet.rel_even : ∀ {R : Type u_1} [inst : CommRing R] (W : ℤ → R) (m : ℤ),
  IsEllipticNet.rel W (m + 1) (m - 1) 1 0 =
    W (2 * m) * W 2 * W 1 ^ 2 - W (m - 1) ^ 2 * W m * W (m + 2) + W (m - 2) * W m * W (m + 1) ^ 2
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.isSome_minKey?_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β}, (t.insert k v).minKey?.isSome = true
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsColimit.mk.inj : ∀ {J : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} J} {C : Type u₃} {inst_1 : CategoryTheory.Category.{v₃, u₃} C}
  {F : CategoryTheory.Functor J C} {t : CategoryTheory.Limits.Cocone F}
  {desc : (s : CategoryTheory.Limits.Cocone F) → t.pt ⟶ s.pt}
  {fac :
    autoParam
      (∀ (s : CategoryTheory.Limits.Cocone F) (j : J),
        CategoryTheory.CategoryStruct.comp (t.ι.app j) (desc s) = s.ι.app j)
      CategoryTheory.Limits.IsColimit.fac._autoParam}
  {uniq :
    autoParam
      (∀ (s : CategoryTheory.Limits.Cocone F) (m : t.pt ⟶ s.pt),
        (∀ (j : J), CategoryTheory.CategoryStruct.comp (t.ι.app j) m = s.ι.app j) → m = desc s)
      CategoryTheory.Limits.IsColimit.uniq._autoParam}
  {desc_1 : (s : CategoryTheory.Limits.Cocone F) → t.pt ⟶ s.pt}
  {fac_1 :
    autoParam
      (∀ (s : CategoryTheory.Limits.Cocone F) (j : J),
        CategoryTheory.CategoryStruct.comp (t.ι.app j) (desc_1 s) = s.ι.app j)
      CategoryTheory.Limits.IsColimit.fac._autoParam}
  {uniq_1 :
    autoParam
      (∀ (s : CategoryTheory.Limits.Cocone F) (m : t.pt ⟶ s.pt),
        (∀ (j : J), CategoryTheory.CategoryStruct.comp (t.ι.app j) m = s.ι.app j) → m = desc_1 s)
      CategoryTheory.Limits.IsColimit.uniq._autoParam},
  { desc := desc, fac := fac, uniq := uniq } = { desc := desc_1, fac := fac_1, uniq := uniq_1 } → desc = desc_1
-- Mathlib.Algebra.Homology.HomologySequenceLemmas
CategoryTheory.ShortComplex.ShortExact.acyclic_X₃ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {c : ComplexShape ι} {S : CategoryTheory.ShortComplex (HomologicalComplex C c)},
  S.ShortExact → QuasiIso S.f → S.X₃.Acyclic
-- Mathlib.AlgebraicGeometry.Geometrically.Irreducible
AlgebraicGeometry.instGeometricallyIrreducibleFiberToSpecResidueField : ∀ {X S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (s : ↥S) [AlgebraicGeometry.GeometricallyIrreducible f],
  AlgebraicGeometry.GeometricallyIrreducible (AlgebraicGeometry.Scheme.Hom.fiberToSpecResidueField f s)
-- Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
/-- Typeclass asserting that a summation filter `L` is consistent with unconditional summation,
so that any unconditionally-summable function is `L`-summable with the same sum.  -/
SummationFilter.LeAtTop : {β : Type u_2} → SummationFilter β → Prop
-- Mathlib.Algebra.Order.Ring.StandardPart
ArchimedeanClass.FiniteElement.isUnit_iff_mk_eq_zero : ∀ {K : Type u_1} [inst : LinearOrder K] [inst_1 : Field K] [inst_2 : IsOrderedRing K]
  {x : ArchimedeanClass.FiniteElement K}, IsUnit x ↔ ArchimedeanClass.mk ↑x = 0
-- Mathlib.Data.PNat.Interval
PNat.card_fintype_uIcc : ∀ (a b : ℕ+), Fintype.card ↑(Set.uIcc a b) = (↑↑b - ↑↑a).natAbs + 1
-- Batteries.Data.UnionFind.Basic
Batteries.UnionFind.findAux.eq_1 : ∀ (self : Batteries.UnionFind) (x : Fin self.size),
  self.findAux x =
    if h : self.arr[↑x].parent = ↑x then { s := self.arr, root := x, size_eq := ⋯ }
    else
      have this := ⋯;
      match self.findAux ⟨self.arr[↑x].parent, ⋯⟩ with
      | { s := arr₁, root := root, size_eq := H } =>
        { s := arr₁.modify ↑x fun s => { parent := ↑root, rank := s.rank }, root := root, size_eq := ⋯ }
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf
AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.structurePresheafInCommRing_obj_carrier : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] (U : (TopologicalSpace.Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ),
  ↑((AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.structurePresheafInCommRing 𝒜).obj U) =
    (AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.structureSheafInType 𝒜).obj.obj U
-- Mathlib.Data.Finset.Card
Finset.card_val : ∀ {α : Type u_1} (s : Finset α), s.val.card = s.card
-- Mathlib.Data.List.SplitBy
_private.Mathlib.Data.List.SplitBy.0.List.isChain_of_mem_splitByLoop : ∀ {α : Type u_1} {m : List α} {r : α → α → Bool} {l : List α} {a : α} {g : List α},
  (∀ b ∈ g.head?, r b a = true) →
    List.IsChain (fun y x => r x y = true) g →
      m ∈ List.splitBy.loop r l a g [] → List.IsChain (fun x y => r x y = true) m
-- Init.Data.Int.Order
_private.Init.Data.Int.Order.0.Int.neg.match_1.eq_2 : ∀ (motive : ℤ → Sort u_1) (n : ℕ) (h_1 : (n : ℕ) → motive (Int.ofNat n)) (h_2 : (n : ℕ) → motive (Int.negSucc n)),
  (match Int.negSucc n with
    | Int.ofNat n => h_1 n
    | Int.negSucc n => h_2 n) =
    h_2 n
-- Mathlib.Tactic.Linter.Whitespace
_private.Mathlib.Tactic.Linter.Whitespace.0.Mathlib.Linter.Style.Whitespace.getUnlintedRanges.match_1.splitter : (motive : Option Lean.Syntax.Range → Sort u_1) →
  (x : Option Lean.Syntax.Range) →
    ((trail : Lean.Syntax.Range) → motive (some trail)) →
      ((x : Option Lean.Syntax.Range) → (∀ (trail : Lean.Syntax.Range), x = some trail → False) → motive x) → motive x
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.card_succ : ∀ (o : Ordinal.{u_1}), (Order.succ o).card = o.card + 1
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.proj_clift : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  [inst_2 : TopologicalSpace Z] {T : Bundle.Trivialization F proj} {ι : Type u_5} [inst_3 : TopologicalSpace ι]
  [inst_4 : LocallyCompactPair ι ↑T.baseSet] {γ : C(ι, ↑T.baseSet)} {i : ι} {e : ↑T.source},
  proj ↑((T.clift (e, γ)) i) = ↑(γ i)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get?_of_isEmpty : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t.WF → ∀ {a : α}, t.isEmpty = true → Std.DTreeMap.Internal.Impl.Const.get? t a = none
-- Mathlib.Topology.Algebra.OpenSubgroup
/-- The preimage of an `OpenSubgroup` along a continuous `Monoid` homomorphism
is an `OpenSubgroup`.  -/
OpenSubgroup.comap : {G : Type u_1} →
  [inst : Group G] →
    [inst_1 : TopologicalSpace G] →
      {N : Type u_2} →
        [inst_2 : Group N] →
          [inst_3 : TopologicalSpace N] → (f : G →* N) → Continuous ⇑f → OpenSubgroup N → OpenSubgroup G
-- Mathlib.CategoryTheory.Action.Concrete
/-- The `G`-set `G`, acting on itself by left multiplication.  -/
Action.leftRegular : (G : Type u) → [inst : Monoid G] → Action (Type u) G
-- Init.Data.List.Nat.TakeDrop
List.drop_sub_one : ∀ {α : Type u_1} {l : List α} {i : ℕ}, 0 < i → List.drop (i - 1) l = l[i - 1]?.toList ++ List.drop i l
-- Init.Data.String.Defs
String.Slice.Pos.mk.injEq : ∀ {s : String.Slice} (offset : String.Pos.Raw) (isValidForSlice : String.Pos.Raw.IsValidForSlice s offset)
  (offset_1 : String.Pos.Raw) (isValidForSlice_1 : String.Pos.Raw.IsValidForSlice s offset_1),
  ({ offset := offset, isValidForSlice := isValidForSlice } =
      { offset := offset_1, isValidForSlice := isValidForSlice_1 }) =
    (offset = offset_1)
-- Mathlib.Algebra.Module.LinearMap.Defs
/-- The subtraction of two linear maps is linear.  -/
LinearMap.instSub : {R₁ : Type u_2} →
  {R₂ : Type u_3} →
    {M : Type u_8} →
      {N₂ : Type u_12} →
        [inst : Semiring R₁] →
          [inst_1 : Semiring R₂] →
            [inst_2 : AddCommMonoid M] →
              [inst_3 : AddCommGroup N₂] →
                [inst_4 : Module R₁ M] → [inst_5 : Module R₂ N₂] → {σ₁₂ : R₁ →+* R₂} → Sub (M →ₛₗ[σ₁₂] N₂)
-- Lean.Data.Lsp.Internal
/-- Shortened representation of `RefIdent.fvar` for more compact serialization.  -/
Lean.Lsp.RefIdent.RefIdentJsonRepr.f : String → String → Lean.Lsp.RefIdent.RefIdentJsonRepr
-- Mathlib.Algebra.Category.MonCat.Limits
/-- If `(F ⋙ forget CommMonCat).sections` is `u`-small, `F` has a limit.  -/
CommMonCat.hasLimit : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommMonCat)
  [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget CommMonCat)).sections], CategoryTheory.Limits.HasLimit F
-- Mathlib.Topology.Subpath
/-- Concatenating the constant path at `x` with itself just yields the constant path at `x`.  -/
Path.concat_refl : ∀ {X : Type u_1} [inst : TopologicalSpace X] (n : ℕ) (x : X),
  (Path.concat (fun x_1 => x) fun x_1 => Path.refl x) = Path.refl x
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.instInhabitedGeneratorNode.default : Lean.Meta.SynthInstance.GeneratorNode
-- Mathlib.Data.Set.Prod
Set.singleton_prod_singleton : ∀ {α : Type u_1} {β : Type u_2} {a : α} {b : β}, {a} ×ˢ {b} = {(a, b)}
-- Init.Omega.Constraint
/-- Shorthand for the first component of `positivize`.  -/
Lean.Omega.positivizeConstraint : Lean.Omega.Constraint → Lean.Omega.Coeffs → Lean.Omega.Constraint
-- Mathlib.Data.DFinsupp.Order
DFinsupp.coe_lt_coe : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Zero (α i)] [inst_1 : (i : ι) → Preorder (α i)]
  {f g : Π₀ (i : ι), α i}, ⇑f < ⇑g ↔ f < g
-- Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
FiniteDimensional.eq_1 : ∀ (K : Type u_1) (V : Type u_2) [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V],
  FiniteDimensional K V = Module.Finite K V
-- Init.Data.String.Lemmas.Pattern.Basic
/-- Predicate stating compatibility between `PatternModel` and `ForwardPattern`.

This extends `LawfulForwardPattern`, but it is much stronger because it forces the
`ForwardPattern` to match the longest prefix of the given slice that matches the property
supplied by the `PatternModel` instance.
 -/
String.Slice.Pattern.Model.LawfulForwardPatternModel : {ρ : Type} →
  (pat : ρ) → [String.Slice.Pattern.ForwardPattern pat] → [String.Slice.Pattern.Model.PatternModel pat] → Prop
-- Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing
_private.Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing.0.ModularForm.E₄CubeSubE₆SqForm_qExpansion_eq : UpperHalfPlane.qExpansion 1 ⇑ModularForm.E₄CubeSubE₆SqForm✝ =
  UpperHalfPlane.qExpansion 1 ⇑ModularForm.E₄ * UpperHalfPlane.qExpansion 1 ⇑ModularForm.E₄ *
      UpperHalfPlane.qExpansion 1 ⇑ModularForm.E₄ -
    UpperHalfPlane.qExpansion 1 ⇑ModularForm.E₆ * UpperHalfPlane.qExpansion 1 ⇑ModularForm.E₆