mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.GeneralLinearGroup.Basic
LinearMap.GeneralLinearGroup.congrLinearEquiv_refl : ∀ {R₁ : Type u_3} {M₁ : Type u_6} [inst : Semiring R₁] [inst_1 : AddCommMonoid M₁] [inst_2 : Module R₁ M₁],
  LinearMap.GeneralLinearGroup.congrLinearEquiv (LinearEquiv.refl R₁ M₁) =
    MulEquiv.refl (LinearMap.GeneralLinearGroup R₁ M₁)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
_private.Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting.0.CategoryTheory.Limits.termF₂_1 : Lean.ParserDescr
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.wf_union₀ : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  {m₁ m₂ : Std.DHashMap.Raw α β} {h₁ : 0 < m₁.buckets.size} {h₂ : 0 < m₂.buckets.size},
  m₁.WF → m₂.WF → (↑(Std.DHashMap.Internal.Raw₀.union ⟨m₁, h₁⟩ ⟨m₂, h₂⟩)).WF
-- Mathlib.CategoryTheory.Sites.Closed
/-- A closure (increasing, inflationary and idempotent) operation on sieves that commutes with pullback
induces a Grothendieck topology.
In fact, such operations are in bijection with Grothendieck topologies.
 -/
CategoryTheory.topologyOfClosureOperator : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (c : (X : C) → ClosureOperator (CategoryTheory.Sieve X)) →
      (∀ ⦃X Y : C⦄ (f : Y ⟶ X) (S : CategoryTheory.Sieve X),
          (c Y) (CategoryTheory.Sieve.pullback f S) = CategoryTheory.Sieve.pullback f ((c X) S)) →
        CategoryTheory.GrothendieckTopology C
-- Mathlib.Algebra.Module.Presentation.Cokernel
/-- The shape of the presentation by generators and relations of the cokernel
of `f : M₁ →ₗ[A] M₂`. It consists of a generator for each generator of `M₂`, and
there are two types of relations: one for each relation in the presentation in `M₂`,
and one for each generator of `M₁`.  -/
Module.Presentation.cokernelRelations : {A : Type u} →
  [inst : Ring A] →
    {M₁ : Type v₁} →
      {M₂ : Type v₂} →
        [inst_1 : AddCommGroup M₁] →
          [inst_2 : Module A M₁] →
            [inst_3 : AddCommGroup M₂] →
              [inst_4 : Module A M₂] →
                (pres₂ : Module.Presentation A M₂) →
                  {f : M₁ →ₗ[A] M₂} → {ι : Type w₁} → {g₁ : ι → M₁} → pres₂.CokernelData f g₁ → Module.Relations A
-- Mathlib.Algebra.Homology.Bifunctor
HomologicalComplex.mapBifunctor.d₂_eq_zero' : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} D] {I₁ : Type u_4}
  {I₂ : Type u_5} {J : Type u_6} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂}
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C₁] [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C₂]
  [inst_5 : CategoryTheory.Preadditive D] (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂)
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [inst_6 : F.PreservesZeroMorphisms]
  [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (c : ComplexShape J) [inst_8 : TotalComplexShape c₁ c₂ c]
  [inst_9 : K₁.HasMapBifunctor K₂ F c] [inst_10 : DecidableEq J] (i₁ : I₁) {i₂ i₂' : I₂},
  c₂.Rel i₂ i₂' → ∀ (j : J), c₁.π c₂ c (i₁, i₂') ≠ j → HomologicalComplex.mapBifunctor.d₂ K₁ K₂ F c i₁ i₂ j = 0
-- Mathlib.CategoryTheory.Dialectica.Monoidal
CategoryTheory.Dial.whiskerRight_F : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] {X₁ X₂ : CategoryTheory.Dial C} (f : X₁ ⟶ X₂)
  (Y : CategoryTheory.Dial C),
  (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Y).F =
    CategoryTheory.Limits.prod.lift
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.prod.map CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.fst) f.F)
      (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.snd)
-- Mathlib.Combinatorics.Quiver.Symmetric
/-- Shorthand for the "forward" arrow corresponding to `f` in `symmetrify V`  -/
Quiver.Hom.toPos : {V : Type u_2} → [inst : Quiver V] → {X Y : V} → (X ⟶ Y) → (X ⟶ Y)
-- Mathlib.Order.Closure
ClosureOperator.isClosed_iff : ∀ {α : Type u_1} [inst : Preorder α] (self : ClosureOperator α) {x : α}, self.IsClosed x ↔ self.toFun x = x
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.toListRev_filter : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m] [inst_2 : Std.Iterator α m β]
  [Std.Iterators.Finite α m] {f : β → Bool} {it : Std.IterM m β},
  (Std.IterM.filter f it).toListRev = List.filter f <$> it.toListRev
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.isValidSearchFrom_cast_iff : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s t : String.Slice} (hst : s.copy = t.copy)
  {pos : s.Pos} {l : List (String.Slice.Pattern.SearchStep t)},
  String.Slice.Pattern.Model.IsValidSearchFrom pat (pos.cast hst) l ↔
    String.Slice.Pattern.Model.IsValidSearchFrom pat pos
      (List.map (fun x => String.Slice.Pattern.SearchStep.cast ⋯ x) l)
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.mopFunctor_map : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y),
  (CategoryTheory.mopFunctor C).map f = f.mop
-- Mathlib.Combinatorics.Quiver.Basic
Quiver.homOfEq_eq_iff : ∀ {V : Type u_1} [inst : Quiver V] {X Y X' Y' : V} (f : X ⟶ Y) (g : X' ⟶ Y') (hX : X = X') (hY : Y = Y'),
  Quiver.homOfEq f hX hY = g ↔ f = Quiver.homOfEq g ⋯ ⋯
-- Mathlib.Order.SuccPred.Basic
Order.not_isMin_succ : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : SuccOrder α] [Nontrivial α] (a : α), ¬IsMin (Order.succ a)
-- Lean.Parser.Types
Lean.Parser.ParserFn : Type
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.re_zero : ∀ {d : ℤ}, Zsqrtd.re 0 = 0
-- Mathlib.FieldTheory.PurelyInseparable.Tower
/-- The same-universe version of `Field.lift_rank_mul_lift_insepDegree_of_isPurelyInseparable`.  -/
Field.rank_mul_insepDegree_of_isPurelyInseparable : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (K : Type v) [inst_3 : Field K]
  [inst_4 : Algebra F K] [inst_5 : Algebra E K] [IsScalarTower F E K] [IsPurelyInseparable F E],
  Module.rank F E * Field.insepDegree E K = Field.insepDegree F K
-- Mathlib.Tactic.Attr.Register
/-- Simp set for integral rules.  -/
Parser.Attr.integral_simps : Lean.ParserDescr
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.ordered_keys : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → List.Pairwise (fun a b => compare a b = Ordering.lt) t.keys
-- Mathlib.Algebra.Algebra.Bilinear
LinearMap.mul_apply' : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : SMulCommClass R A A] [inst_4 : IsScalarTower R A A] (a b : A), ((LinearMap.mul R A) a) b = a * b
-- Mathlib.Analysis.Analytic.Constructions
/-- Finite products of analytic functions are analytic  -/
Finset.analyticOnNhd_fun_prod : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {A : Type u_9} [inst_3 : NormedCommRing A] [inst_4 : NormedAlgebra 𝕜 A] {f : α → E → A}
  {s : Set E} (N : Finset α), (∀ n ∈ N, AnalyticOnNhd 𝕜 (f n) s) → AnalyticOnNhd 𝕜 (fun z => ∏ n ∈ N, f n z) s
-- Mathlib.Topology.UniformSpace.LocallyUniformConvergence
/-- If every `x ∈ s` has a neighbourhood within `s` on which `F i` tends uniformly to `f`, then
`F i` tends locally uniformly on `s` to `f`.

Note this is **not** a tautology, since our definition of `TendstoLocallyUniformlyOn` is slightly
more general (although the conditions are equivalent if `β` is locally compact and `s` is open,
see `tendstoLocallyUniformlyOn_TFAE`).  -/
tendstoLocallyUniformlyOn_of_forall_exists_nhds : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : TopologicalSpace α] [inst_1 : UniformSpace β] {F : ι → α → β}
  {f : α → β} {s : Set α} {p : Filter ι},
  (∀ x ∈ s, ∃ t ∈ nhdsWithin x s, TendstoUniformlyOn F f p t) → TendstoLocallyUniformlyOn F f p s
-- Mathlib.CategoryTheory.DifferentialObject
CategoryTheory.DifferentialObject.shiftZero_hom_app_f : ∀ {S : Type u_1} [inst : AddCommGroupWithOne S] (C : Type u) [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.HasShift C S]
  (X : CategoryTheory.DifferentialObject S C),
  ((CategoryTheory.DifferentialObject.shiftZero C).hom.app X).f = (CategoryTheory.shiftFunctorZero C S).hom.app X.obj
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι_map_tensorHom_hom_eq_tensorHom : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (V : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V] (D : Type u₃)
  [inst_4 : CategoryTheory.Category.{v₃, u₃} D] [inst_5 : CategoryTheory.MonoidalCategoryStruct D]
  [inst_6 : CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct C V D] {d₁ d₂ d₁' d₂' : D}
  (f : d₁ ⟶ d₂) (f' : d₁' ⟶ d₂'),
  (CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι C V D).map
      (CategoryTheory.MonoidalCategoryStruct.tensorHom f f') =
    CategoryTheory.MonoidalCategory.DayConvolution.map
      ((CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι C V D).map f)
      ((CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι C V D).map f')
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem?_inter_of_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α}, k ∈ m₂ → (m₁ ∩ m₂)[k]? = m₁[k]?
-- Lean.Server.FileWorker.RequestHandling
Lean.Server.FileWorker.handleWaitForDiagnostics : Lean.Lsp.WaitForDiagnosticsParams → Lean.Server.RequestM (Lean.Server.RequestTask Lean.Lsp.WaitForDiagnostics)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVExpr.PackedBitVec.w : Std.Tactic.BVDecide.BVExpr.PackedBitVec → ℕ
-- Init.Data.Iterators.Consumers.Monadic.Access
/-- `IteratorAccess α m` provides efficient implementations for random access or iterators that support
it. `it.nextAtIdx? n` either returns the step in which the `n`th value of `it` is emitted
(necessarily of the form `.yield _ _`) or `.done` if `it` terminates before emitting the `n`th
value.

For monadic iterators, the monadic effects of this operation may differ from manually iterating
to the `n`-th value because `nextAtIdx?` can take shortcuts. By the signature, the return value
is guaranteed to plausible in the sense of `IterM.IsPlausibleNthOutputStep`.

This class is experimental and users of the iterator API should not explicitly depend on it.
 -/
Std.IteratorAccess : (α : Type w) → (m : Type w → Type w') → {β : Type w} → [Std.Iterator α m β] → Type (max w w')
-- Mathlib.FieldTheory.CardinalEmb
Field.Emb.Cardinal.instIsSeparableSubtypeMemIntermediateFieldAdjoinImageToTypeOrdRankCompCoeBasisWellOrderedBasisLeastExtIioSingletonSet : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E]
  [rank_inf : Fact (Cardinal.aleph0 ≤ Module.rank F E)] [inst_3 : Algebra.IsAlgebraic F E] [Algebra.IsSeparable F E]
  (i : (Module.rank F E).ord.ToType),
  Algebra.IsSeparable
    ↥(IntermediateField.adjoin F
        (⇑(Field.Emb.Cardinal.wellOrderedBasis F E) ∘ Field.Emb.Cardinal.leastExt F E '' Set.Iio i))
    ↥(↥(IntermediateField.adjoin F
            (⇑(Field.Emb.Cardinal.wellOrderedBasis F E) ∘ Field.Emb.Cardinal.leastExt F E ''
              Set.Iio i)))⟮(Field.Emb.Cardinal.wellOrderedBasis F E) (Field.Emb.Cardinal.leastExt F E i)⟯
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.instBEqPoly.beq.eq_3 : ∀ (x x_1 : Lean.Grind.CommRing.Poly),
  (∀ (a b : ℤ), x = Lean.Grind.CommRing.Poly.num a → x_1 = Lean.Grind.CommRing.Poly.num b → False) →
    (∀ (a : ℤ) (a_1 : Lean.Grind.CommRing.Mon) (a_2 : Lean.Grind.CommRing.Poly) (b : ℤ) (b_1 : Lean.Grind.CommRing.Mon)
        (b_2 : Lean.Grind.CommRing.Poly),
        x = Lean.Grind.CommRing.Poly.add a a_1 a_2 → x_1 = Lean.Grind.CommRing.Poly.add b b_1 b_2 → False) →
      Lean.Grind.CommRing.instBEqPoly.beq x x_1 = false
-- Mathlib.Data.Matrix.Mul
dotProduct_sum : ∀ {m : Type u_2} {α : Type v} [inst : Fintype m] [inst_1 : NonUnitalNonAssocSemiring α] {ι : Type u_10} (u : m → α)
  (s : Finset ι) (v : ι → m → α), u ⬝ᵥ ∑ i ∈ s, v i = ∑ i ∈ s, u ⬝ᵥ v i
-- Mathlib.Data.Nat.Choose.Cast
Nat.cast_choose : ∀ (K : Type u_1) [inst : DivisionSemiring K] [CharZero K] {a b : ℕ},
  a ≤ b → ↑(b.choose a) = ↑b.factorial / (↑a.factorial * ↑(b - a).factorial)
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.and_mono : ∀ {σs : List (Type u)} {P P' Q Q' : Std.Do.SPred σs}, (P ⊢ₛ P') → (Q ⊢ₛ Q') → P ∧ Q ⊢ₛ P' ∧ Q'
-- Mathlib.Algebra.Free
FreeAddMagma.instTraversable : Traversable FreeAddMagma
-- Mathlib.Topology.MetricSpace.CauSeqFilter
/-- In a normed field, `CauSeq` coincides with the usual notion of Cauchy sequences.  -/
isCauSeq_iff_cauchySeq : ∀ {α : Type u} [inst : NormedField α] {u : ℕ → α}, IsCauSeq norm u ↔ CauchySeq u
-- Mathlib.GroupTheory.Perm.Sign
Equiv.Perm.signBijAux_surj : ∀ {n : ℕ} {f : Equiv.Perm (Fin n)}, ∀ a ∈ Equiv.Perm.finPairsLT n, ∃ b ∈ Equiv.Perm.finPairsLT n, f.signBijAux b = a
-- Mathlib.Combinatorics.SimpleGraph.CycleGraph
_private.Mathlib.Combinatorics.SimpleGraph.CycleGraph.0.SimpleGraph.cycleGraph.cycleCons.match_1.eq_2 : ∀ (n : ℕ) (motive : Fin (n + 3) → Sort u_1) (m : ℕ) (h : m + 1 < n + 3) (h_1 : (h : 0 < n + 3) → motive ⟨0, h⟩)
  (h_2 : (m : ℕ) → (h : m + 1 < n + 3) → motive ⟨m.succ, h⟩),
  (match ⟨m.succ, h⟩ with
    | ⟨0, h⟩ => h_1 h
    | ⟨m.succ, h⟩ => h_2 m h) =
    h_2 m h
-- Mathlib.AlgebraicTopology.DoldKan.Projections
/-- This is the inductive definition of the projections `P q : K[X] ⟶ K[X]`,
with `P 0 := 𝟙 _` and `P (q+1) := P q ≫ (𝟙 _ + Hσ q)`.  -/
AlgebraicTopology.DoldKan.P : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {X : CategoryTheory.SimplicialObject C} →
        ℕ → (AlgebraicTopology.AlternatingFaceMapComplex.obj X ⟶ AlgebraicTopology.AlternatingFaceMapComplex.obj X)
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
_private.Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms.0.SimplexCategoryGenRel.standardσ.match_1.eq_1 : ∀ {m₁ m₂ : ℕ} (motive : (L : List ℕ) → m₂ + L.length = m₁ → Sort u_1) (h : m₂ + [].length = m₁)
  (h_1 : (h : m₂ + [].length = m₁) → motive [] h)
  (h_2 : (a : ℕ) → (t : List ℕ) → (h : m₂ + (a :: t).length = m₁) → motive (a :: t) h),
  (match [], h with
    | [], h => h_1 h
    | a :: t, h => h_2 a t h) =
    h_1 h
-- Mathlib.LinearAlgebra.ExteriorPower.Basic
exteriorPower.ιMulti_family_eq_coe_comp : ∀ (R : Type u) [inst : CommRing R] (n : ℕ) {M : Type u_1} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {I : Type u_4}
  [inst_3 : LinearOrder I] (v : I → M),
  ExteriorAlgebra.ιMulti_family R n v = Subtype.val ∘ exteriorPower.ιMulti_family R n v
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
CategoryTheory.Oplax.StrongTrans.Hom.of.injEq : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} {η θ : F ⟶ G} (as as_1 : CategoryTheory.Oplax.StrongTrans.Modification η θ),
  ({ as := as } = { as := as_1 }) = (as = as_1)
-- Mathlib.CategoryTheory.Sites.LocallySurjective
/-- A morphism of presheaves `f : F ⟶ G` is locally surjective with respect to a Grothendieck
topology if every section of `G` is locally in the image of `f`.  -/
CategoryTheory.Presheaf.IsLocallySurjective : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.GrothendieckTopology C →
      {A : Type u'} →
        [inst_1 : CategoryTheory.Category.{v', u'} A] →
          {FA : A → A → Type u_1} →
            {CA : A → Type w'} →
              [inst_2 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] →
                [CategoryTheory.ConcreteCategory A FA] → {F G : CategoryTheory.Functor Cᵒᵖ A} → (F ⟶ G) → Prop
-- Mathlib.Algebra.Group.Submonoid.Pointwise
Submonoid.inv_iSup : ∀ {G : Type u_2} [inst : Group G] {ι : Sort u_7} (S : ι → Submonoid G), (⨆ i, S i)⁻¹ = ⨆ i, (S i)⁻¹
-- Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
SSet.relativeCellComplexOfMono.Cell.ι_b_ι : ∀ {X Y : SSet} {i : X ⟶ Y} {d : ℕ} (c : SSet.relativeCellComplexOfMono.Cell i d),
  CategoryTheory.CategoryStruct.comp c.ιSigmaStdSimplex
      (CategoryTheory.CategoryStruct.comp (SSet.relativeCellComplexOfMono.b i d) ((SSet.skeletonOfMono i) (d + 1)).ι) =
    c.map
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction_homEquiv_apply' : ∀ {X : AlgebraicGeometry.LocallyRingedSpace} {R : Type u} [inst : CommRing R]
  (f : CommRingCat.of R ⟶ AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X)),
  (AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction.homEquiv X (Opposite.op (CommRingCat.of R))) (Opposite.op f) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.identityToΓSpec.app X)
      (AlgebraicGeometry.Spec.locallyRingedSpaceMap f)
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.Context.config : Lean.Meta.Simp.Context → Lean.Meta.Simp.Config
-- Std.Time.Date.Unit.Weekday
_private.Std.Time.Date.Unit.Weekday.0.Std.Time.Weekday.toOrdinal.eq_3 : Std.Time.Weekday.wednesday.toOrdinal = 3
-- Mathlib.LinearAlgebra.Dual.Defs
/-- Maps a module M to the dual of the dual of M. See `Module.erange_coe` and
`Module.evalEquiv`.  -/
Module.Dual.eval : (R : Type u_1) →
  (M : Type u_3) →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → M →ₗ[R] Module.Dual R (Module.Dual R M)
-- Mathlib.Topology.Sheaves.Stalks
/-- If `x` specializes to `y`, then there is a natural map `F.stalk y ⟶ F.stalk x`.  -/
TopCat.Presheaf.stalkSpecializes : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasColimits C] →
      {X : TopCat} → (F : TopCat.Presheaf C X) → {x y : ↑X} → x ⤳ y → (F.stalk y ⟶ F.stalk x)
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
/-- The `NonUnitalSubsemiring` generated by a set.  -/
NonUnitalSubsemiring.closure : {R : Type u} → [inst : NonUnitalNonAssocSemiring R] → Set R → NonUnitalSubsemiring R
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
MeasurableSpace.countablyGeneratedAtom.congr_simp : ∀ (α : Type u_3) [inst : MeasurableSpace α] [inst_1 : MeasurableSpace.CountablyGenerated α] (a a_1 : ℕ → Prop),
  a = a_1 →
    ∀ (a_2 a_3 : α),
      a_2 = a_3 → MeasurableSpace.countablyGeneratedAtom α a a_2 = MeasurableSpace.countablyGeneratedAtom α a_1 a_3
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Poly.of_denote_le_cancelAux : ∀ (ctx : Nat.Internal.Linear.Context) (fuel : ℕ) (m₁ m₂ r₁ r₂ : Nat.Internal.Linear.Poly),
  Nat.Internal.Linear.Poly.denote_le ctx (Nat.Internal.Linear.Poly.cancelAux fuel m₁ m₂ r₁ r₂) →
    Nat.Internal.Linear.Poly.denote_le ctx (List.reverse r₁ ++ m₁, List.reverse r₂ ++ m₂)
-- Mathlib.Computability.TuringMachine.PostTuringMachine
/-- A set `S` of labels supports the statement `q` if all the `goto`
statements in `q` refer only to other functions in `S`.  -/
Turing.TM1.SupportsStmt : {Γ : Type u_1} → {Λ : Type u_2} → {σ : Type u_3} → Finset Λ → Turing.TM1.Stmt Γ Λ σ → Prop
-- Mathlib.Topology.Instances.EReal.Lemmas
EReal.iSup_add_le_add_iSup : ∀ {α : Type u_2} {u v : α → EReal}, ⨆ x, (u + v) x ≤ (⨆ x, u x) + ⨆ x, v x
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.map_obj_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T T' : D} {S : CategoryTheory.Functor C D} (f : T ⟶ T')
  (X : CategoryTheory.Comma S (CategoryTheory.Functor.fromPUnit T)),
  ((CategoryTheory.CostructuredArrow.map f).obj X).right = X.right
-- Mathlib.CategoryTheory.Category.Preorder
OrderHom.equivalenceFunctor_counitIso_inv_app_app : ∀ {X : Type u} {Y : Type v} [inst : Preorder X] [inst_1 : Preorder Y] (X_1 : CategoryTheory.Functor X Y) (X_2 : X),
  (OrderHom.equivalenceFunctor.counitIso.inv.app X_1).app X_2 = CategoryTheory.CategoryStruct.id (X_1.obj X_2)
-- Mathlib.Data.Multiset.Bind
Multiset.product.eq_1 : ∀ {α : Type u_1} {β : Type v} (s : Multiset α) (t : Multiset β),
  s.product t = s.bind fun a => Multiset.map (Prod.mk a) t
-- Mathlib.Algebra.Order.Module.Defs
/-- Right scalar multiplication as an order isomorphism.  -/
OrderIso.smulRight : {α : Type u_1} →
  {β : Type u_2} →
    [inst : GroupWithZero α] →
      [inst_1 : Preorder α] →
        [inst_2 : Preorder β] →
          [inst_3 : MulAction α β] → [PosSMulMono α β] → [PosSMulReflectLE α β] → {a : α} → 0 < a → β ≃o β
-- Init.Internal.Order.Basic
Lean.Order.ImplicationOrder.instCompleteLattice : Lean.Order.CompleteLattice Lean.Order.ImplicationOrder
-- Mathlib.RingTheory.Ideal.Maximal
Ideal.isPrime_of_maximally_disjoint : ∀ {α : Type u} [inst : CommSemiring α] (I : Ideal α) (S : Submonoid α),
  Disjoint ↑I ↑S → (∀ (J : Ideal α), I < J → ¬Disjoint ↑J ↑S) → I.IsPrime
-- Lean.Meta.Sorry
/-- Constructs a `sorryAx`.
* If the current ref has a source position, then creates a labeled sorry.
  This supports "go to definition" in the InfoView and pretty printing a source position when the `pp.sorrySource` option is true.
* If `synthetic` is true, then the `sorry` is regarded as being generated by the elaborator.
  The caller should ensure that there is an associated error logged.
* If `unique` is true, the `sorry` is unique, in the sense that it is not defeq to any other `sorry` created by `mkLabeledSorry`.
 -/
Lean.Meta.mkLabeledSorry : Lean.Expr → Bool → Bool → Lean.MetaM Lean.Expr
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.SimprocOLeanEntry.keys : Lean.Meta.Simp.SimprocOLeanEntry → Array Lean.Meta.SimpTheoremKey
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getKeyD_insertManyIfNewUnit_list_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.DTreeMap α (fun x => Unit) cmp} [Std.TransCmp cmp] {l : List α}
  {k fallback : α}, k ∈ t → (Std.DTreeMap.Const.insertManyIfNewUnit t l).getKeyD k fallback = t.getKeyD k fallback
-- Lean.Elab.Tactic.Induction
_private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.ElimApp.Context.mk.injEq : ∀ (elimInfo : Lean.Meta.ElimInfo) (targets : Array Lean.Expr) (elimInfo_1 : Lean.Meta.ElimInfo)
  (targets_1 : Array Lean.Expr),
  ({ elimInfo := elimInfo, targets := targets } = { elimInfo := elimInfo_1, targets := targets_1 }) =
    (elimInfo = elimInfo_1 ∧ targets = targets_1)
-- Mathlib.Tactic.FunProp.FunctionData
Mathlib.Meta.FunProp.MaybeFunctionData.letE.injEq : ∀ (f f_1 : Lean.Expr),
  (Mathlib.Meta.FunProp.MaybeFunctionData.letE f = Mathlib.Meta.FunProp.MaybeFunctionData.letE f_1) = (f = f_1)
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.edgeFinset_card : ∀ {V : Type u_1} {G : SimpleGraph V} [inst : Fintype ↑G.edgeSet], G.edgeFinset.card = Fintype.card ↑G.edgeSet
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.mem_supportSet_iff_of_mem : ∀ {X : AlgebraicGeometry.Scheme} {I : X.IdealSheafData} {x : ↥X} {U : ↑X.affineOpens},
  x ∈ ↑U → (x ∈ I.supportSet ↔ x ∈ X.zeroLocus ↑(I.ideal U))
-- Std.Http.Data.URI.Basic
Std.Http.RequestTarget.originForm.sizeOf_spec : ∀ (path : Std.Http.URI.Path) (query : Option Std.Http.URI.Query),
  sizeOf (Std.Http.RequestTarget.originForm path query) = 1 + sizeOf path + sizeOf query
-- Init.Data.Vector.Count
Vector.count_replace : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {n : ℕ} {a b c : α} {xs : Vector α n},
  Vector.count c (xs.replace a b) =
    if xs.contains a = true then
      (Vector.count c xs + if (b == c) = true then 1 else 0) - if (a == c) = true then 1 else 0
    else Vector.count c xs