mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.toFunctorToCategoricalPullback_map_app_fst : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (X : Type u₄)
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] {S S' : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X}
  (φ : S ⟶ S') (x : X),
  (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.toFunctorToCategoricalPullback F G X).map φ).app x).fst =
    φ.fst.app x
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic
groupCohomology.inhomogeneousCochains.d_def : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) (n : ℕ),
  (groupCohomology.inhomogeneousCochains A).d n (n + 1) = inhomogeneousCochains.d A n
-- Mathlib.Topology.Sheaves.CommRingCat
TopCat.Sheaf.objSupIsoProdEqLocus_inv_eq_iff : ∀ {X : TopCat} (F : TopCat.Sheaf CommRingCat X) {U V W UW VW : TopologicalSpace.Opens ↑X} (e : W ≤ U ⊔ V)
  (x :
    ↑(CommRingCat.of
        ↥(((CommRingCat.Hom.hom (F.obj.map (CategoryTheory.homOfLE ⋯).op)).comp
                (RingHom.fst ↑(F.obj.obj (Opposite.op U)) ↑(F.obj.obj (Opposite.op V)))).eqLocus
            ((CommRingCat.Hom.hom (F.obj.map (CategoryTheory.homOfLE ⋯).op)).comp
              (RingHom.snd ↑(F.obj.obj (Opposite.op U)) ↑(F.obj.obj (Opposite.op V)))))))
  (y : ↑(F.obj.obj (Opposite.op W))) (h₁ : UW = U ⊓ W) (h₂ : VW = V ⊓ W),
  (CategoryTheory.ConcreteCategory.hom (F.obj.map (CategoryTheory.homOfLE e).op))
        ((CategoryTheory.ConcreteCategory.hom (F.objSupIsoProdEqLocus U V).inv) x) =
      y ↔
    (CategoryTheory.ConcreteCategory.hom (F.obj.map (CategoryTheory.homOfLE ⋯).op)) (↑x).1 =
        (CategoryTheory.ConcreteCategory.hom (F.obj.map (CategoryTheory.homOfLE ⋯).op)) y ∧
      (CategoryTheory.ConcreteCategory.hom (F.obj.map (CategoryTheory.homOfLE ⋯).op)) (↑x).2 =
        (CategoryTheory.ConcreteCategory.hom (F.obj.map (CategoryTheory.homOfLE ⋯).op)) y
-- Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
/-- Given `φ : K ⟶ L`, `K⟦(1 : ℤ)⟧` is homotopy equivalent to
the mapping cone of `inr φ : L ⟶ mappingCone φ`.  -/
CochainComplex.mappingCone.rotateHomotopyEquiv : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] →
        {K L : CochainComplex C ℤ} →
          (φ : K ⟶ L) →
            HomotopyEquiv ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) 1).obj K)
              (CochainComplex.mappingCone (CochainComplex.mappingCone.inr φ))
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
CategoryTheory.Functor.instIsSplitEpiBiprodComparison : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (F : CategoryTheory.Functor C D) (X Y : C) [inst_4 : CategoryTheory.Limits.HasBinaryBiproduct X Y]
  [inst_5 : CategoryTheory.Limits.HasBinaryBiproduct (F.obj X) (F.obj Y)] [F.PreservesZeroMorphisms],
  CategoryTheory.IsSplitEpi (F.biprodComparison X Y)
-- Init.Data.UInt.Lemmas
UInt32.toBitVec_ofNatTruncate_of_lt : ∀ {n : ℕ} (hn : n < UInt32.size), (UInt32.ofNatClamp n).toBitVec = n#'hn
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
/-- The pointwise addition of sets `s + t` is defined as `{x + y | x ∈ s, y ∈ t}` in locale
`Pointwise`.  -/
Set.add : {α : Type u_2} → [Add α] → Add (Set α)
-- Mathlib.RingTheory.Polynomial.Basic
Polynomial.restriction_zero : ∀ {R : Type u} [inst : Ring R], Polynomial.restriction 0 = 0
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getEntryDₘ.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (l : Std.DTreeMap.Internal.Impl α β) (fallback : (a : α) × β a),
  Std.DTreeMap.Internal.Impl.getEntryDₘ k l fallback = (l.getEntry?ₘ k).getD fallback
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKeyD_erase : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF)
  {k a fallback : α},
  (Std.DTreeMap.Internal.Impl.erase k t ⋯).impl.getKeyD a fallback =
    if compare k a = Ordering.eq then fallback else t.getKeyD a fallback
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.ConnectedComponent.supp_injective : ∀ {V : Type u} {G : SimpleGraph V}, Function.Injective SimpleGraph.ConnectedComponent.supp
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
Submonoid.unop_inj : ∀ {M : Type u_2} [inst : MulOneClass M] {S T : Submonoid Mᵐᵒᵖ}, S.unop = T.unop ↔ S = T
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.instMonoidalMonMapMon.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : CategoryTheory.BraidedCategory C]
  [inst_5 : CategoryTheory.BraidedCategory D] [inst_6 : F.Braided],
  F.instMonoidalMonMapMon =
    { εIso := CategoryTheory.Mon.mkIso (CategoryTheory.Functor.Monoidal.εIso F) ⋯ ⋯,
        μIso := fun M N => CategoryTheory.Mon.mkIso (CategoryTheory.Functor.Monoidal.μIso F M.X N.X) ⋯ ⋯,
        μIso_hom_natural_left := ⋯, μIso_hom_natural_right := ⋯, associativity := ⋯, left_unitality := ⋯,
        right_unitality := ⋯ }.toMonoidal
-- Mathlib.Algebra.Polynomial.Coeff
Polynomial.coeff_mul_intCast : ∀ {S : Type v} [inst : Ring S] {p : Polynomial S} {a : ℤ} {k : ℕ}, (p * ↑a).coeff k = p.coeff k * ↑a
-- Init.Data.List.Basic
List.length_dropLast_cons : ∀ {α : Type u} {a : α} {as : List α}, (a :: as).dropLast.length = as.length
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.integral_sub : ∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {f g : α → G},
  MeasureTheory.Integrable f μ →
    MeasureTheory.Integrable g μ → ∫ (a : α), f a - g a ∂μ = ∫ (a : α), f a ∂μ - ∫ (a : α), g a ∂μ
-- Init.Data.Bool
/-- Converts `true` to `1` and `false` to `0`.
 -/
Bool.toNat : Bool → ℕ
-- Init.Data.Array.GetLit
_private.Init.Data.Array.GetLit.0.List.take.match_1.eq_3 : ∀ {α : Type u_1} (motive : ℕ → List α → Sort u_2) (n : ℕ) (a : α) (as : List α) (h_1 : (x : List α) → motive 0 x)
  (h_2 : (n : ℕ) → motive n.succ []) (h_3 : (n : ℕ) → (a : α) → (as : List α) → motive n.succ (a :: as)),
  (match n.succ, a :: as with
    | 0, x => h_1 x
    | n.succ, [] => h_2 n
    | n.succ, a :: as => h_3 n a as) =
    h_3 n a as
-- Mathlib.Algebra.Category.CommAlgCat.Monoidal
CommAlgCat.associator_hom_hom : ∀ {R : Type u} [inst : CommRing R] (A B C : CommAlgCat R),
  CommAlgCat.Hom.hom (CategoryTheory.MonoidalCategoryStruct.associator A B C).hom =
    ↑(Algebra.TensorProduct.assoc R R R ↑A ↑B ↑C)
-- Mathlib.Topology.MetricSpace.CantorScheme
CantorScheme.Antitone.closureAntitone : ∀ {β : Type u_1} {α : Type u_2} {A : List β → Set α} [inst : TopologicalSpace α],
  CantorScheme.Antitone A → (∀ (l : List β), IsClosed (A l)) → CantorScheme.ClosureAntitone A
-- Init.Data.String.Modify
String.Pos.splits_pastSet : ∀ {s : String} {p : s.Pos} {c : Char} {hp : p ≠ s.endPos},
  (p.pastSet c hp).Splits ((s.sliceTo p).copy ++ String.singleton c) (s.sliceFrom (p.next hp)).copy
-- Mathlib.Order.Hom.CompleteLattice
sInfHom.mk.sizeOf_spec : ∀ {α : Type u_8} {β : Type u_9} [inst : InfSet α] [inst_1 : InfSet β] [inst_2 : SizeOf α] [inst_3 : SizeOf β]
  (toFun : α → β) (map_sInf' : ∀ (s : Set α), toFun (sInf s) = sInf (toFun '' s)),
  sizeOf { toFun := toFun, map_sInf' := map_sInf' } = 1
-- Mathlib.Topology.Order.IntermediateValue
intermediate_value_Ici : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {δ : Type u_1} [inst_4 : LinearOrder δ] [inst_5 : TopologicalSpace δ] [OrderClosedTopology δ]
  {a : α} {f : α → δ},
  ContinuousOn f (Set.Ici a) → Filter.Tendsto f Filter.atTop Filter.atTop → Set.Ici (f a) ⊆ f '' Set.Ici a
-- Mathlib.Algebra.Homology.ShortComplex.Homology
/-- If a short complex `S` has both a left homology data `h₁` and a right homology data `h₂`,
this is the canonical morphism `h₁.H ⟶ h₂.H`.  -/
CategoryTheory.ShortComplex.leftRightHomologyComparison' : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S : CategoryTheory.ShortComplex C} → (h₁ : S.LeftHomologyData) → (h₂ : S.RightHomologyData) → h₁.H ⟶ h₂.H
-- Mathlib.CategoryTheory.Sites.Descent.Precoverage
_private.Mathlib.CategoryTheory.Sites.Descent.Precoverage.0.CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.mem_sieve : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S}
  {ι' : Type t'} {X' : ι' → C} {f' : (j : ι') → X' j ⟶ S} {i : ι} {Z : C} (q : Z ⟶ X i) ⦃j : ι'⦄ (a : Z ⟶ X' j),
  autoParam (CategoryTheory.CategoryStruct.comp a (f' j) = CategoryTheory.CategoryStruct.comp q (f i))
      CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.mem_sieve._auto_1✝ →
    (CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.sieve✝ f f' i).arrows (CategoryTheory.Over.homMk q ⋯)
-- Lean.ScopedEnvExtension
Lean.ScopedEnvExtension.State.state : {σ : Type} → Lean.ScopedEnvExtension.State σ → σ
-- Mathlib.CategoryTheory.Limits.MorphismProperty
CategoryTheory.MorphismProperty.Over.instPreservesFiniteLimitsTopOverForget : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] (P : CategoryTheory.MorphismProperty T) (X : T)
  [CategoryTheory.Limits.HasPullbacks T] [P.IsMultiplicative] [P.IsStableUnderBaseChange] [P.HasOfPostcompProperty P],
  CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.MorphismProperty.Over.forget P ⊤ X)
-- Mathlib.CategoryTheory.Quotient.Linear
/-- The scalar multiplications on morphisms in `Quotient R`.  -/
CategoryTheory.Quotient.Linear.smul : {R : Type u_1} →
  {C : Type u_2} →
    [inst : Semiring R] →
      [inst_1 : CategoryTheory.Category.{v_1, u_2} C] →
        [inst_2 : CategoryTheory.Preadditive C] →
          [inst_3 : CategoryTheory.Linear R C] →
            (r : HomRel C) →
              [CategoryTheory.Congruence r] →
                (∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X ⟶ Y), r f₁ f₂ → r (a • f₁) (a • f₂)) →
                  (X Y : CategoryTheory.Quotient r) → SMul R (X ⟶ Y)
-- Mathlib.Computability.TuringMachine.Tape
/-- A direction for the Turing machine `move` command, either
left or right.  -/
Turing.Dir : Type
-- Mathlib.CategoryTheory.Bicategory.Coherence
CategoryTheory.FreeBicategory.normalizeAux_nil_comp : ∀ {B : Type u} [inst : Quiver B] {a b c : B} (f : CategoryTheory.FreeBicategory.Hom a b)
  (g : CategoryTheory.FreeBicategory.Hom b c),
  CategoryTheory.FreeBicategory.normalizeAux Quiver.Path.nil (f.comp g) =
    (CategoryTheory.FreeBicategory.normalizeAux Quiver.Path.nil f).comp
      (CategoryTheory.FreeBicategory.normalizeAux Quiver.Path.nil g)
-- Mathlib.Data.Quot
Quotient.instInhabitedQuotient : {α : Sort u_1} → (s : Setoid α) → [Inhabited α] → Inhabited (Quotient s)
-- Mathlib.Analysis.Normed.Group.Defs
/-- the `ℝ`-valued norm function.  -/
«term‖_‖» : Lean.ParserDescr
-- Mathlib.Topology.Constructible
Topology.IsLocallyConstructible.finsetInf : ∀ {X : Type u_2} [inst : TopologicalSpace X] {ι : Type u_4} {s : Finset ι} {t : ι → Set X},
  (∀ i ∈ s, Topology.IsLocallyConstructible (t i)) → Topology.IsLocallyConstructible (s.inf t)
-- Mathlib.MeasureTheory.Group.Integral
MeasureTheory.integral_inv_eq_self : ∀ {G : Type u_4} {E : Type u_5} [inst : MeasurableSpace G] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E]
  [inst_3 : Group G] [MeasurableInv G] (f : G → E) (μ : MeasureTheory.Measure G) [μ.IsInvInvariant],
  ∫ (x : G), f x⁻¹ ∂μ = ∫ (x : G), f x ∂μ
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.cycles₁.eq_1 : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  groupHomology.cycles₁ A = (ModuleCat.Hom.hom (groupHomology.d₁₀ A)).ker
-- Lean.Widget.InteractiveGoal
Lean.Widget.InteractiveGoals.mk.sizeOf_spec : ∀ (goals : Array Lean.Widget.InteractiveGoal), sizeOf { goals := goals } = 1 + sizeOf goals
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.concat.eq_1 : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} (p : G.Walk u v) (h : G.Adj v w),
  p.concat h = p.append (SimpleGraph.Walk.cons h SimpleGraph.Walk.nil)
-- Mathlib.CategoryTheory.Types.Basic
/-- Use the `ConcreteCategory.hom` projection for `@[simps]` lemmas.  -/
TypeCat.Hom.Simps.hom : (X Y : Type u) → (X ⟶ Y) → TypeCat.Fun X Y
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
/-- The canonical `ι`-coloring of a `completeMultipartiteGraph` with parts indexed by `ι`  -/
SimpleGraph.completeMultipartiteGraph.coloring : {ι : Type u_4} → (V : ι → Type u_5) → (SimpleGraph.completeMultipartiteGraph V).Coloring ι
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.comp_left_assoc : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {P : CategoryTheory.MorphismProperty T}
  {Q : CategoryTheory.MorphismProperty A} {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative]
  [inst_4 : W.IsMultiplicative] {X Y Z : CategoryTheory.MorphismProperty.Comma L R P Q W} (f : X ⟶ Y) (g : Y ⟶ Z)
  {Z_1 : A} (h : Z.left ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g).left h =
    CategoryTheory.CategoryStruct.comp f.left (CategoryTheory.CategoryStruct.comp g.left h)
-- Mathlib.CategoryTheory.GuitartExact.VerticalComposition
CategoryTheory.TwoSquare.GuitartExact.of_vComp' : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : Type u_6}
  [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} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_4} D₁]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} D₂] [inst_5 : CategoryTheory.Category.{v_6, u_6} D₃]
  {H₁ : CategoryTheory.Functor C₁ D₁} {L₁ : CategoryTheory.Functor C₁ C₂} {R₁ : CategoryTheory.Functor D₁ D₂}
  {H₂ : CategoryTheory.Functor C₂ D₂} (w : CategoryTheory.TwoSquare H₁ L₁ R₁ H₂) {L₂ : CategoryTheory.Functor C₂ C₃}
  {R₂ : CategoryTheory.Functor D₂ D₃} {H₃ : CategoryTheory.Functor C₃ D₃} (w' : CategoryTheory.TwoSquare H₂ L₂ R₂ H₃)
  {L₁₂ : CategoryTheory.Functor C₁ C₃} {R₁₂ : CategoryTheory.Functor D₁ D₃} (eL : L₁.comp L₂ ≅ L₁₂)
  (eR : R₁.comp R₂ ≅ R₁₂) [R₁.EssSurj] [w.GuitartExact] [h : (w.vComp' w' eL eR).GuitartExact], w'.GuitartExact
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
mdifferentiable_snd : ∀ {𝕜 : 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'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'], MDiff Prod.snd
-- Lean.Data.Lsp.Basic
Lean.Lsp.RenameFile.mk.inj : ∀ {oldUri newUri : Lean.Lsp.DocumentUri} {options? : Option Lean.Lsp.CreateFile.Options} {annotationId? : Option String}
  {oldUri_1 newUri_1 : Lean.Lsp.DocumentUri} {options?_1 : Option Lean.Lsp.CreateFile.Options}
  {annotationId?_1 : Option String},
  { oldUri := oldUri, newUri := newUri, options? := options?, annotationId? := annotationId? } =
      { oldUri := oldUri_1, newUri := newUri_1, options? := options?_1, annotationId? := annotationId?_1 } →
    oldUri = oldUri_1 ∧ newUri = newUri_1 ∧ options? = options?_1 ∧ annotationId? = annotationId?_1
-- Mathlib.Geometry.Euclidean.Circumcenter
/-- Given a finite nonempty affinely independent family of points,
there is a unique (circumcenter, circumradius) pair for those points
in the affine subspace they span.  -/
AffineIndependent.existsUnique_dist_eq : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {ι : Type u_3} [hne : Nonempty ι] [Finite ι] {p : ι → P},
  AffineIndependent ℝ p →
    ∃! cs, cs.center ∈ affineSpan ℝ (Set.range p) ∧ Set.range p ⊆ Metric.sphere cs.center cs.radius
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
IsEllipticNet.atomRel_abs₁ : ∀ {R : Type u_1} [inst : CommRing R] {W : ℤ → R},
  Function.Odd W → ∀ (a b c d : ℤ), IsEllipticNet.atomRel W |a| b c d = IsEllipticNet.atomRel W a b c d
-- Init.Data.Iterators.Basic
Std.IterM.TerminationMeasures.Productive.Rel.eq_1 : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [inst : Std.Iterator α m β],
  Std.IterM.TerminationMeasures.Productive.Rel =
    Relation.TransGen (InvImage Std.IterM.IsPlausibleSkipSuccessorOf Std.IterM.TerminationMeasures.Productive.it)
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.ciSup_mul_ciSup : ∀ {ι : Type u} {ι' : Type w} (f : ι → Cardinal.{v}) (g : ι' → Cardinal.{v}), (⨆ i, f i) * ⨆ j, g j = ⨆ i, ⨆ j, f i * g j
-- Init.Data.Vector.Lemmas
Vector.contains_mk : ∀ {α : Type u_1} {n : ℕ} [inst : BEq α] {xs : Array α} {size : xs.size = n} {a : α},
  (Vector.mk xs size).contains a = xs.contains a
-- Lean.Meta.Tactic.Grind.PropagatorAttr
/-- Builtin propagators.  -/
Lean.Meta.Grind.BuiltinPropagators : Type
-- Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
CategoryTheory.limitCompWhiskeringRightIsoLimitComp_inv_π_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {E : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  {J : Type u_4} [inst_3 : CategoryTheory.Category.{v_4, u_4} J] [inst_4 : CategoryTheory.Limits.HasLimitsOfShape J D]
  (F : CategoryTheory.Functor D E) [inst_5 : CategoryTheory.Limits.PreservesLimitsOfShape J F]
  (G : CategoryTheory.Functor J (CategoryTheory.Functor C D)) (j : J) {Z : CategoryTheory.Functor C E}
  (h : ((CategoryTheory.Functor.whiskeringRight C D E).obj F).obj (G.obj j) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.limitCompWhiskeringRightIsoLimitComp F G).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.limit.π (G.comp ((CategoryTheory.Functor.whiskeringRight C D E).obj F)) j) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (CategoryTheory.Limits.limit.π G j) F) h
-- Init.Data.String.Hashable
String.instHashablePos.hash : {s : String} → s.Pos → UInt64
-- Mathlib.Topology.Separation.Regular
TopologicalSpace.IsTopologicalBasis.exists_closure_subset : ∀ {X : Type u_1} [inst : TopologicalSpace X] [RegularSpace X] {B : Set (Set X)},
  TopologicalSpace.IsTopologicalBasis B → ∀ {x : X} {s : Set X}, s ∈ nhds x → ∃ t ∈ B, x ∈ t ∧ closure t ⊆ s
-- Mathlib.AlgebraicGeometry.Geometrically.Integral
AlgebraicGeometry.instGeometricallyReducedOfGeometricallyIntegral : ∀ {X S : AlgebraicGeometry.Scheme} (f : X ⟶ S) [AlgebraicGeometry.GeometricallyIntegral f],
  AlgebraicGeometry.GeometricallyReduced f
-- Mathlib.Topology.Defs.Filter
nhds_def : ∀ {X : Type u_3} [inst : TopologicalSpace X] (x : X), nhds x = ⨅ s ∈ {s | x ∈ s ∧ IsOpen s}, Filter.principal s
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
FreeSimplexQuiver.Hom.δ.inj : ∀ {n : ℕ} {i i_1 : Fin (n + 2)}, FreeSimplexQuiver.Hom.δ i = FreeSimplexQuiver.Hom.δ i_1 → i = i_1
-- Mathlib.Analysis.Normed.Affine.Isometry
LinearIsometryEquiv.coe_toAffineIsometryEquiv : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup V]
  [inst_2 : NormedSpace 𝕜 V] [inst_3 : SeminormedAddCommGroup V₂] [inst_4 : NormedSpace 𝕜 V₂] (e : V ≃ₗᵢ[𝕜] V₂),
  ⇑e.toAffineIsometryEquiv = ⇑e
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHomRight_comp : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] (w : D) {x y z : C} (f : x ⟶ y) (g : y ⟶ z),
  CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight w (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight w f)
      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight w g)
-- Mathlib.RingTheory.Ideal.Over
Ideal.top_liesOver_top : ∀ (A : Type u_2) [inst : CommSemiring A] (B : Type u_3) [inst_1 : Semiring B] [inst_2 : Algebra A B], ⊤.LiesOver ⊤
-- Mathlib.Analysis.Normed.Group.Uniform
/-- **Alias** of the forward direction of `lipschitzWith_inv_iff`. -/
LipschitzWith.of_inv : ∀ {α : Type u_4} {E : Type u_5} [inst : SeminormedCommGroup E] [inst_1 : PseudoEMetricSpace α] {K : NNReal} {f : α → E},
  LipschitzWith K f⁻¹ → LipschitzWith K f
-- Mathlib.Data.QPF.Multivariate.Basic
MvQPF.abs_map : ∀ {n : ℕ} {F : TypeVec.{u} n → Type u_1} [self : MvQPF F] {α β : TypeVec.{u} n} (f : α.Arrow β) (p : ↑(MvQPF.P F) α),
  MvQPF.abs (MvFunctor.map f p) = MvFunctor.map f (MvQPF.abs p)
-- Mathlib.Analysis.Complex.Trigonometric
Real.cos_one_le : Real.cos 1 ≤ 5 / 9
-- Mathlib.Analysis.Normed.Group.Uniform
/-- **Alias** of the forward direction of `lipschitzOnWith_inv_iff`. -/
LipschitzOnWith.of_inv : ∀ {α : Type u_4} {E : Type u_5} [inst : SeminormedCommGroup E] [inst_1 : PseudoEMetricSpace α] {K : NNReal} {f : α → E}
  {s : Set α}, LipschitzOnWith K f⁻¹ s → LipschitzOnWith K f s
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
_private.Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic.0.CategoryTheory.WithInitial.map.match_1.eq_2 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C]
  (motive : (X Y : CategoryTheory.WithInitial C) → (X ⟶ Y) → Sort u_3) (a : C)
  (x : CategoryTheory.WithInitial.star ⟶ CategoryTheory.WithInitial.of a)
  (h_1 :
    (a a_1 : C) →
      (f : CategoryTheory.WithInitial.of a ⟶ CategoryTheory.WithInitial.of a_1) →
        motive (CategoryTheory.WithInitial.of a) (CategoryTheory.WithInitial.of a_1) f)
  (h_2 :
    (a : C) →
      (x : CategoryTheory.WithInitial.star ⟶ CategoryTheory.WithInitial.of a) →
        motive CategoryTheory.WithInitial.star (CategoryTheory.WithInitial.of a) x)
  (h_3 :
    (x : CategoryTheory.WithInitial.star ⟶ CategoryTheory.WithInitial.star) →
      motive CategoryTheory.WithInitial.star CategoryTheory.WithInitial.star x),
  (match CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.of a, x with
    | CategoryTheory.WithInitial.of a, CategoryTheory.WithInitial.of a_1, f => h_1 a a_1 f
    | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.of a, x => h_2 a x
    | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.star, x => h_3 x) =
    h_2 a x
-- Mathlib.CategoryTheory.Sites.Sheafification
CategoryTheory.instIsLeftAdjointFunctorOppositeSheafPresheafToSheaf : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u₂)
  [inst_1 : CategoryTheory.Category.{v₂, u₂} A] [inst_2 : CategoryTheory.HasWeakSheafify J A],
  (CategoryTheory.presheafToSheaf J A).IsLeftAdjoint
-- Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
CategoryTheory.SmallObject.isSmall : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (I : CategoryTheory.MorphismProperty C) (κ : Cardinal.{w})
  [inst_1 : Fact κ.IsRegular] [inst_2 : OrderBot κ.ord.ToType] [I.IsCardinalForSmallObjectArgument κ],
  CategoryTheory.MorphismProperty.IsSmall.{w, v, u} I