mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.Functor.toStructuredArrow_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (G : CategoryTheory.Functor E C) (X : D)
  (F : CategoryTheory.Functor C D) (f : (Y : E) → X ⟶ F.obj (G.obj Y))
  (h : ∀ {Y Z : E} (g : Y ⟶ Z), CategoryTheory.CategoryStruct.comp (f Y) (F.map (G.map g)) = f Z) (Y : E),
  (G.toStructuredArrow X F f h).obj Y = CategoryTheory.StructuredArrow.mk (f Y)
-- Mathlib.Geometry.Euclidean.Sphere.OrthRadius
EuclideanGeometry.Sphere.inter_orthRadius_eq_empty_of_radius_lt_dist : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {p : P},
  s.radius < dist p s.center → Metric.sphere s.center s.radius ∩ ↑(s.orthRadius p) = ∅
-- Mathlib.Algebra.Lie.Basic
lie_neg : ∀ {L : Type v} {M : Type w} [inst : LieRing L] [inst_1 : AddCommGroup M] [inst_2 : LieRingModule L M] (x : L) (m : M),
  ⁅x, -m⁆ = -⁅x, m⁆
-- Mathlib.Algebra.Homology.CommSq
/-- The short complex attached to the cokernel cofork of a commutative square.  -/
CategoryTheory.CommSq.shortComplex : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {X₁ X₂ X₃ X₄ : C} →
        [CategoryTheory.Limits.HasBinaryBiproduct X₂ X₃] →
          {f : X₁ ⟶ X₂} →
            {g : X₁ ⟶ X₃} →
              {inl : X₂ ⟶ X₄} → {inr : X₃ ⟶ X₄} → CategoryTheory.CommSq f g inl inr → CategoryTheory.ShortComplex C
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKeyD_alter_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] [Inhabited α] {k fallback : α} {f : Option (β k) → Option (β k)},
  (t.alter k f).getKeyD k fallback = if (f (t.get? k)).isSome = true then k else fallback
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
CategoryTheory.Bicategory.Adj.Hom₂.ext_iff : ∀ {B : Type u} {inst : CategoryTheory.Bicategory B} {a b : CategoryTheory.Bicategory.Adj B} {α β : a ⟶ b}
  {x y : CategoryTheory.Bicategory.Adj.Hom₂ α β}, x = y ↔ x.τl = y.τl ∧ x.τr = y.τr
-- Lean.Attributes
Lean.AttributeExtensionState.mk.inj : ∀ {newEntries : List Lean.AttributeExtensionOLeanEntry} {map : Std.HashMap Lean.Name Lean.AttributeImpl}
  {newEntries_1 : List Lean.AttributeExtensionOLeanEntry} {map_1 : Std.HashMap Lean.Name Lean.AttributeImpl},
  { newEntries := newEntries, map := map } = { newEntries := newEntries_1, map := map_1 } →
    newEntries = newEntries_1 ∧ map = map_1
-- Mathlib.Data.Finsupp.Single
/-- `Finsupp.single a b` is injective in `b`. For the statement that it is injective in `a`, see
`Finsupp.single_left_injective`  -/
Finsupp.single_injective : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] (a : α), Function.Injective (Finsupp.single a)
-- Lean.Meta.LazyDiscrTree
/-- The elements in the match result.

The top-level array represents an array from `score` values to the
results with that score. A `score` is the number of non-star matches
in a pattern against the term, and thus bounded by the size of the
term being matched against.  The elements of this array are themselves
arrays of non-empty arrays so that we can defer concatenating results until
needed.
 -/
Lean.Meta.LazyDiscrTree.MatchResult.elts : {α : Type} → Lean.Meta.LazyDiscrTree.MatchResult α → Array (Array (Array α))
-- Lean.Elab.MatchAltView
Lean.Elab.Term.MatchAltView.patterns : {k : Lean.SyntaxNodeKinds} → Lean.Elab.Term.MatchAltView k → Array Lean.Syntax
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.bicone_ι_π_self : ∀ {J : Type w} {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} (B : CategoryTheory.Limits.Bicone F) (j : J),
  CategoryTheory.CategoryStruct.comp (B.ι j) (B.π j) = CategoryTheory.CategoryStruct.id (F j)
-- Mathlib.LinearAlgebra.BilinearForm.Basic
LinearMap.BilinForm.sub_apply : ∀ {R₁ : Type u_4} {M₁ : Type u_5} [inst : CommRing R₁] [inst_1 : AddCommGroup M₁] [inst_2 : Module R₁ M₁]
  (B₁ D₁ : LinearMap.BilinForm R₁ M₁) (x y : M₁), ((B₁ - D₁) x) y = (B₁ x) y - (D₁ x) y
-- Mathlib.Data.EReal.Basic
EReal.toENNReal_le_toENNReal : ∀ {x y : EReal}, x ≤ y → x.toENNReal ≤ y.toENNReal
-- Mathlib.Topology.Inseparable
Inseparable.of_eq : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X}, x = y → Inseparable x y
-- Init.Data.String.Lemmas.Pattern.String.ForwardPattern
String.Slice.skipSuffix?_string_eq_skipSuffix?_toSlice : ∀ {pat : String} {s : String.Slice}, s.skipSuffix? pat = s.skipSuffix? pat.toSlice
-- Mathlib.Analysis.Convex.Exposed
IsExposed.antisymm : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : TopologicalSpace 𝕜] [inst_1 : Ring 𝕜] [inst_2 : PartialOrder 𝕜]
  [inst_3 : AddCommMonoid E] [inst_4 : TopologicalSpace E] [inst_5 : Module 𝕜 E] {A B : Set E},
  IsExposed 𝕜 A B → IsExposed 𝕜 B A → A = B
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
/-- Suppose `a : X → Set A` is continuous on `t : Set X` and `0 ≤ a x` for all `x ∈ t`.
Suppose further that `s : X → Set ℝ≥0` is a family of sets with `s x` compact when
`x ∈ t` such that `s x₀` contains the spectrum of `a x` for all sufficiently close `x ∈ t`.
If `f : ℝ≥0 → ℝ≥0` is continuous on `s x` for each `x ∈ t` and `f 0 = 0`, then
`fun x ↦ cfc f (a x)` is continuous on `t`.  -/
ContinuousOn.cfcₙ_nnreal : ∀ {X : Type u_1} {A : Type u_2} [inst : NonUnitalNormedRing A] [inst_1 : StarRing A] [inst_2 : NormedSpace ℝ A]
  [inst_3 : IsScalarTower ℝ A A] [inst_4 : SMulCommClass ℝ A A] [ContinuousStar A]
  [inst_6 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_7 : PartialOrder A]
  [inst_8 : StarOrderedRing A] [inst_9 : NonnegSpectrumClass ℝ A] [T2Space A] [IsSemitopologicalRing A]
  [inst_12 : TopologicalSpace X] {s : X → Set NNReal} (f : NNReal → NNReal) {a : X → A} {t : Set X},
  (∀ x ∈ t, IsCompact (s x)) →
    ContinuousOn a t →
      (∀ x₀ ∈ t, ∀ᶠ (x : X) in nhdsWithin x₀ t, quasispectrum NNReal (a x) ⊆ s x₀) →
        (∀ x ∈ t, 0 ≤ a x) →
          autoParam (∀ x ∈ t, ContinuousOn f (s x)) ContinuousOn.cfcₙ_nnreal._auto_1 →
            autoParam (f 0 = 0) ContinuousOn.cfcₙ_nnreal._auto_3 → ContinuousOn (fun x => cfcₙ f (a x)) t
-- Batteries.Data.List.Basic
List.zipWithLeftTR.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → Option β → γ) (as : List α) (bs : List β),
  List.zipWithLeftTR f as bs = List.zipWithLeftTR.go f as bs #[]
-- Lean.Meta.Tactic.NormCast
Lean.Meta.NormCast.NormCastExtension.mk.injEq : ∀ (up down squash up_1 down_1 squash_1 : Lean.Meta.SimpExtension),
  ({ up := up, down := down, squash := squash } = { up := up_1, down := down_1, squash := squash_1 }) =
    (up = up_1 ∧ down = down_1 ∧ squash = squash_1)
-- Mathlib.CategoryTheory.Monoidal.Limits.Preserves
/-- When `C` is braided and `tensorLeft c` preserves a colimit, then so does `tensorRight k`.  -/
CategoryTheory.MonoidalCategory.Limits.preservesColimit_of_braided_and_preservesColimit_tensor_left : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {J : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} J] (F : CategoryTheory.Functor J C)
  [CategoryTheory.BraidedCategory C] (c : C)
  [CategoryTheory.Limits.PreservesColimit F (CategoryTheory.MonoidalCategory.tensorLeft c)],
  CategoryTheory.Limits.PreservesColimit F (CategoryTheory.MonoidalCategory.tensorRight c)
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
ModularGroup.coe_T : ↑ModularGroup.T = !![1, 1; 0, 1]
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.hom_inv_id_tensor_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {V W X Y Z : C}
  (f : V ≅ W) (g : X ⟶ Y) (h : Y ⟶ Z) {Z_1 : C} (h_1 : CategoryTheory.MonoidalCategoryStruct.tensorObj V Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f.hom g)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f.inv h) h_1) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id V) g)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id V) h) h_1)
-- Mathlib.MeasureTheory.Group.Arithmetic
MeasurableConstSMul.measurable_const_smul : ∀ {M : Type u_2} {α : Type u_3} {inst : SMul M α} {inst_1 : MeasurableSpace α} [self : MeasurableConstSMul M α] (c : M),
  Measurable fun x => c • x
-- Init.Data.Vector.Lemmas
Vector.findM?_toArray : ∀ {m : Type → Type} {α : Type} {n : ℕ} [inst : Monad m] {p : α → m Bool} {xs : Vector α n},
  Array.findM? p xs.toArray = Vector.findM? p xs
-- Mathlib.Topology.Category.LightProfinite.AsLimit
/-- The transition map from `S_m` to `S_n` in `S.diagram`, when `m ≤ n`.  -/
LightProfinite.transitionMapLE : (S : LightProfinite) → {n m : ℕ} → n ≤ m → (S.component m ⟶ S.component n)
-- Mathlib.Condensed.Discrete.Colimit
/-- The functor `locallyConstantPresheaf` takes sequential limits of finite sets with surjective
projection maps to colimits.
 -/
LightCondensed.isColimitLocallyConstantPresheaf : {F : CategoryTheory.Functor ℕᵒᵖ FintypeCat} →
  (c : CategoryTheory.Limits.Cone (F.comp FintypeCat.toLightProfinite)) →
    (X : Type u) →
      CategoryTheory.Limits.IsLimit c →
        [∀ (i : ℕᵒᵖ), CategoryTheory.Epi (c.π.app i)] →
          CategoryTheory.Limits.IsColimit ((LightCondensed.locallyConstantPresheaf X).mapCocone c.op)
-- Mathlib.Order.FixedPoints
OrderHom.lfp_le_gfp : ∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α), OrderHom.lfp f ≤ OrderHom.gfp f
-- Std.Data.DTreeMap.Raw.Basic
/-- Tries to retrieve the key-value pair with the largest key that is less than or equal to the
given key, returning `none` if no such pair exists.
 -/
Std.DTreeMap.Raw.Const.getEntryLE? : {α : Type u} → {cmp : α → α → Ordering} → {β : Type v} → Std.DTreeMap.Raw α (fun x => β) cmp → α → Option (α × β)
-- Lean.Elab.Tactic.Omega.Core
/-- Recursively solve all equalities.  -/
Lean.Elab.Tactic.Omega.Problem.solveEqualities : Lean.Elab.Tactic.Omega.Problem → Lean.Elab.Tactic.Omega.OmegaM Lean.Elab.Tactic.Omega.Problem
-- Aesop.Check
Aesop.Check.toOption : Aesop.Check → Lean.Option Bool
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.coe_linear_eq_coe_contLinear : ∀ {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [inst : Ring R] [inst_1 : AddCommGroup V]
  [inst_2 : Module R V] [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] [inst_5 : AddCommGroup W]
  [inst_6 : Module R W] [inst_7 : TopologicalSpace Q] [inst_8 : AddTorsor W Q] [inst_9 : TopologicalSpace V]
  [inst_10 : IsTopologicalAddTorsor P] [inst_11 : TopologicalSpace W] [inst_12 : IsTopologicalAddTorsor Q]
  (f : P →ᴬ[R] Q), ⇑(↑f).linear = ⇑f.contLinear
-- Lean.Meta.Tactic.Grind.Intro
_private.Lean.Meta.Tactic.Grind.Intro.0.Lean.Meta.Grind.IntroResult.newLocal : Lean.FVarId → Lean.Meta.Grind.Goal → Lean.Meta.Grind.IntroResult✝
-- Lean.Compiler.LCNF.Types
/-- `uint16` is a 16-bit unsigned integer.
 -/
Lean.Compiler.LCNF.ImpureType.uint16 : Lean.Expr
-- Mathlib.Order.CompleteBooleanAlgebra
CompleteAtomicBooleanAlgebra.toCompletelyDistribLattice : {α : Type u} → [CompleteAtomicBooleanAlgebra α] → CompletelyDistribLattice α
-- Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
AlgebraicTopology.AlternatingCofaceMapComplex.map.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {X Y : CategoryTheory.CosimplicialObject C} (f : X ⟶ Y),
  AlgebraicTopology.AlternatingCofaceMapComplex.map f = CochainComplex.ofHom (fun n => f.app { len := n }) ⋯
-- Mathlib.Analysis.Meromorphic.NormalForm
/-- Analytic functions are meromorphic in normal form.  -/
AnalyticAt.meromorphicNFAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜}, AnalyticAt 𝕜 f x → MeromorphicNFAt f x
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Adjunction.Coalgebra.toAlgebraOf_obj_str : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C C} (adj : F ⊣ G)
  (V : CategoryTheory.Endofunctor.Coalgebra G),
  ((CategoryTheory.Endofunctor.Adjunction.Coalgebra.toAlgebraOf adj).obj V).str = (adj.homEquiv V.V V.V).symm V.str
-- Mathlib.RingTheory.DedekindDomain.SelmerGroup
IsDedekindDomain.selmerGroup.fromUnitLift_injective : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {K : Type v} [inst_2 : Field K] [inst_3 : Algebra R K]
  [inst_4 : IsFractionRing R K] {n : ℕ} [inst_5 : Fact (0 < n)],
  Function.Injective ⇑IsDedekindDomain.selmerGroup.fromUnitLift
-- Mathlib.Analysis.Normed.Operator.Basic
ContinuousLinearMap.opNorm_subsingleton : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [inst : SeminormedAddCommGroup E]
  [inst_1 : SeminormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] (f : E →SL[σ₁₂] F)
  [Subsingleton E], ‖f‖ = 0
-- Mathlib.Data.List.Infix
List.instIsPartialOrderIsSuffix : ∀ {α : Type u_1}, IsPartialOrder (List α) fun x1 x2 => x1 <:+ x2
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRoot.map_repr : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
  (h : IsAdjoinRoot S f) (x : S), h.map (h.repr x) = x
-- Batteries.Data.Float.Lemmas
Float.Model.UnpackedFloat.pack.eq_2 : ∀ (spec : Float.Model.Format) (s : Float.Model.UnpackedFloat.Sign),
  Float.Model.UnpackedFloat.pack spec (Float.Model.UnpackedFloat.infinity s) =
    Float.Model.UnpackedFloat.packedInfinity spec s
-- Mathlib.Algebra.Category.Semigrp.Basic
/-- The type of morphisms in `AddSemigrp R`.  -/
AddSemigrp.Hom : AddSemigrp → AddSemigrp → Type u
-- Mathlib.RingTheory.Extension.Cotangent.Basis
/-- The image of `g : R[X₁, ..., Xₙ]` in `T`.  -/
_private.Mathlib.RingTheory.Extension.Cotangent.Basis.0.Algebra.Generators.PresentationOfFreeCotangent.Aux.gbar : {R : Type u_1} →
  {S : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          {ι : Type u_4} →
            {P : Algebra.Generators R S ι} →
              {σ : Type u_5} →
                {b : Module.Basis σ S P.toExtension.Cotangent} →
                  (D : Algebra.Generators.PresentationOfFreeCotangent.Aux✝ P b) →
                    Algebra.Generators.PresentationOfFreeCotangent.Aux.T✝ D
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- `BinaryBiproduct.bicone P Q` is a colimit cocone.  -/
CategoryTheory.Limits.BinaryBiproduct.isColimit : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (P Q : C) →
        [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct P Q] →
          CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryBiproduct.bicone P Q).toCocone
-- Mathlib.Algebra.Notation.FiniteSupport
Function.mulSupport_along_fiber_finite_of_finite : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : One γ] (f : α × β → γ) (a : α),
  Function.HasFiniteMulSupport f → Function.HasFiniteMulSupport fun b => f (a, b)
-- Mathlib.CategoryTheory.Category.Basic
/-- `Category.mk'` is the dual of `Category.mk`, which we need for `to_dual`.
Please avoid using this directly.  -/
CategoryTheory.Category.mk' : {obj : Type u} →
  [inst : CategoryTheory.CategoryStruct.{v, u} obj] →
    (∀ {X Y : obj} (f : Y ⟶ X), CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.id X) = f) →
      (∀ {X Y : obj} (f : Y ⟶ X), CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id Y) f = f) →
        (∀ {W X Y Z : obj} (f : X ⟶ W) (g : Y ⟶ X) (h : Z ⟶ Y),
            CategoryTheory.CategoryStruct.comp h (CategoryTheory.CategoryStruct.comp g f) =
              CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp h g) f) →
          CategoryTheory.Category.{v, u} obj
-- Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
ContinuousLinearEquiv.symm_conjContinuousAlgEquiv : ∀ {𝕜 : Type u_1} {G : Type u_4} {H : Type u_5} [inst : AddCommGroup G] [inst_1 : AddCommGroup H]
  [inst_2 : NormedField 𝕜] [inst_3 : Module 𝕜 G] [inst_4 : Module 𝕜 H] [inst_5 : TopologicalSpace G]
  [inst_6 : TopologicalSpace H] [inst_7 : IsTopologicalAddGroup G] [inst_8 : IsTopologicalAddGroup H]
  [inst_9 : ContinuousConstSMul 𝕜 G] [inst_10 : ContinuousConstSMul 𝕜 H] (e : G ≃L[𝕜] H),
  e.conjContinuousAlgEquiv.symm = e.symm.conjContinuousAlgEquiv
-- Mathlib.FieldTheory.Normal.Defs
/-- Typeclass for normal field extensions: an algebraic extension of fields `K/F` is *normal*
if the minimal polynomial of every element `x` in `K` splits in `K`, i.e. every `F`-conjugate
of `x` is in `K`.  -/
Normal : (F : Type u_1) → (K : Type u_2) → [inst : Field F] → [inst_1 : Field K] → [Algebra F K] → Prop
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.bot : {R : Type u_1} →
  {S : Type u_2} →
    [inst : Ring R] →
      [inst_1 : Ring S] →
        {σ : R →+* S} →
          {E : Type u_4} →
            [inst_2 : AddCommGroup E] →
              [inst_3 : Module R E] →
                {F : Type u_5} → [inst_4 : AddCommGroup F] → [inst_5 : Module S F] → Bot (E →ₛₗ.[σ] F)
-- Mathlib.Order.Filter.Basic
Filter.ext' : ∀ {α : Type u} {f₁ f₂ : Filter α}, (∀ (p : α → Prop), (∀ᶠ (x : α) in f₁, p x) ↔ ∀ᶠ (x : α) in f₂, p x) → f₁ = f₂
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
CategoryTheory.Limits.inr_pushoutLeftPushoutInrIso_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) (g' : Z ⟶ W)
  [inst_1 : CategoryTheory.Limits.HasPushout f g]
  [inst_2 : CategoryTheory.Limits.HasPushout (CategoryTheory.Limits.pushout.inr f g) g'],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr (CategoryTheory.Limits.pushout.inr f g) g')
      (CategoryTheory.Limits.pushoutLeftPushoutInrIso f g g').hom =
    CategoryTheory.Limits.pushout.inr f (CategoryTheory.CategoryStruct.comp g g')
-- Std.Data.TreeMap.Basic
/-- Transforms the tree map into a list of mappings in ascending order.  -/
Std.TreeMap.toArray : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap α β cmp → Array (α × β)
-- Mathlib.Algebra.Order.Archimedean.Basic
exists_rat_gt : ∀ {K : Type u_4} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] [Archimedean K] (x : K), ∃ q, x < ↑q
-- Init.Data.SInt.Bitwise
instAssociativeInt8HXor : Std.Associative fun x1 x2 => x1 ^^^ x2
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Substructure
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Substructure.0.Std.Tactic.BVDecide.BVLogicalExpr.bitblast.go.match_5.eq_3 : ∀ (motive : Std.Tactic.BVDecide.BVLogicalExpr → Sort u_1)
  (expr : Std.Tactic.BVDecide.BoolExpr Std.Tactic.BVDecide.BVPred)
  (h_1 : (var : Std.Tactic.BVDecide.BVPred) → motive (Std.Tactic.BVDecide.BoolExpr.literal var))
  (h_2 : (val : Bool) → motive (Std.Tactic.BVDecide.BoolExpr.const val))
  (h_3 : (expr : Std.Tactic.BVDecide.BoolExpr Std.Tactic.BVDecide.BVPred) → motive expr.not)
  (h_4 : (discr lhs rhs : Std.Tactic.BVDecide.BoolExpr Std.Tactic.BVDecide.BVPred) → motive (discr.ite lhs rhs))
  (h_5 :
    (g : Std.Tactic.BVDecide.Gate) →
      (lhs rhs : Std.Tactic.BVDecide.BoolExpr Std.Tactic.BVDecide.BVPred) →
        motive (Std.Tactic.BVDecide.BoolExpr.gate g lhs rhs)),
  (match expr.not with
    | Std.Tactic.BVDecide.BoolExpr.literal var => h_1 var
    | Std.Tactic.BVDecide.BoolExpr.const val => h_2 val
    | expr.not => h_3 expr
    | discr.ite lhs rhs => h_4 discr lhs rhs
    | Std.Tactic.BVDecide.BoolExpr.gate g lhs rhs => h_5 g lhs rhs) =
    h_3 expr
-- Mathlib.RingTheory.AlgebraicIndependent.Basic
/-- If `{f_i(x) | i : ι}` is algebraically independent over `R`, then
`{f_i : MvPolynomial ι R | i : ι}` is also algebraically independent over `R`.
In fact, the `x = {x_i : A | i : ι}` is also transcendental over `R` provided that `R`
is a field and `ι` is finite; the proof needs transcendence degree.  -/
AlgebraicIndependent.of_aeval : ∀ {ι : Type u} {R : Type u_2} {A : Type v} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  {f : ι → MvPolynomial ι R}, (AlgebraicIndependent R fun i => (MvPolynomial.aeval x) (f i)) → AlgebraicIndependent R f
-- Mathlib.Algebra.CharP.Lemmas
Commute.exists_add_pow_prime_eq : ∀ {R : Type u_1} [inst : Semiring R] {p : ℕ},
  Nat.Prime p → ∀ {x y : R}, Commute x y → ∃ r, (x + y) ^ p = x ^ p + y ^ p + ↑p * x * y * r
-- Mathlib.RingTheory.Coalgebra.Equiv
CoalgEquiv.mk.sizeOf_spec : ∀ {R : Type u_5} [inst : CommSemiring R] {A : Type u_6} {B : Type u_7} [inst_1 : AddCommMonoid A]
  [inst_2 : AddCommMonoid B] [inst_3 : Module R A] [inst_4 : Module R B] [inst_5 : CoalgebraStruct R A]
  [inst_6 : CoalgebraStruct R B] [inst_7 : SizeOf R] [inst_8 : SizeOf A] [inst_9 : SizeOf B] (toCoalgHom : A →ₗc[R] B)
  (invFun : B → A) (left_inv : autoParam (Function.LeftInverse invFun toCoalgHom.toFun) Equiv.left_inv._autoParam)
  (right_inv : autoParam (Function.RightInverse invFun toCoalgHom.toFun) Equiv.right_inv._autoParam),
  sizeOf { toCoalgHom := toCoalgHom, invFun := invFun, left_inv := left_inv, right_inv := right_inv } =
    1 + sizeOf toCoalgHom
-- Mathlib.Topology.Algebra.Monoid
Filter.Tendsto.val_neg_addUnits : ∀ {ι : Type u_1} {N : Type u_4} [inst : TopologicalSpace N] [inst_1 : AddMonoid N] [inst_2 : ContinuousAdd N]
  [inst_3 : T2Space N] {f : ι → AddUnits N} {r₁ r₂ : N} {l : Filter ι} [inst_4 : l.NeBot]
  (h₁ : Filter.Tendsto (fun x => ↑(f x)) l (nhds r₁)) (h₂ : Filter.Tendsto (fun x => ↑(-f x)) l (nhds r₂)),
  ↑(-h₁.addUnits h₂) = r₂
-- Mathlib.Order.Monotone.Basic
strictMonoOn_comp_ofDual_iff : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
  StrictMonoOn (f ∘ ⇑OrderDual.ofDual) s ↔ StrictAntiOn f s
-- Mathlib.RingTheory.AdicCompletion.Completeness
_private.Mathlib.RingTheory.AdicCompletion.Completeness.0.AdicCompletion.ofValEqZeroAux_prop : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {a b c : ℕ} {x : AdicCompletion I M} (h : c = b + a) (ha : ↑x a = 0),
  (Submodule.powSMulQuotInclusion I M h ⊤) (AdicCompletion.ofValEqZeroAux I h ha) = ↑x c
-- Mathlib.Data.Sym.Sym2
Sym2.toFinset_ne_empty : ∀ {α : Type u_1} [inst : DecidableEq α] (z : Sym2 α), z.toFinset ≠ ∅
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.instOrdDiagnosticCode.ord : Lean.Lsp.DiagnosticCode → Lean.Lsp.DiagnosticCode → Ordering
-- Mathlib.Algebra.Algebra.Unitization
Unitization.inl_fst_add_inr_snd_eq : ∀ {R : Type u_3} {A : Type u_4} [inst : AddZeroClass R] [inst_1 : AddZeroClass A] (x : Unitization R A),
  Unitization.inl x.toProd.1 + ↑x.toProd.2 = x
-- Mathlib.Algebra.Group.Action.Pretransitive
MulAction.isPretransitive_iff : ∀ (M : Type u_5) (α : Type u_6) [inst : SMul M α], MulAction.IsPretransitive M α ↔ ∀ (x y : α), ∃ g, g • x = y
-- Mathlib.Topology.Homotopy.TopCat.ZerothHomotopy
TopCat.toSSetObj₀Equiv.eq_1 : ∀ {X : TopCat},
  TopCat.toSSetObj₀Equiv =
    (X.toSSetObjEquiv (Opposite.op { len := 0 })).trans
      { toFun := fun f => f.toFun default, invFun := fun x => { toFun := fun x_1 => x, continuous_toFun := ⋯ },
        left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.toCocycles_comp_isoCocycles₂_hom_apply : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) (x : (Fin 1 → G) → ↑A),
  (CategoryTheory.ConcreteCategory.hom (groupCohomology.isoCocycles₂ A).hom)
      ((CategoryTheory.ConcreteCategory.hom (groupCohomology.toCocycles A 1 2)) x) =
    (groupCohomology.shortComplexH2 A).moduleCatToCycles
      ((CategoryTheory.ConcreteCategory.hom (groupCohomology.cochainsIso₁ A).hom) x)