mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Sync.CancellationContext
Std.CancellationContext.mk.inj : ∀ {state : Std.Mutex Std.CancellationContext.State} {token : Std.CancellationToken} {id : UInt64}
  {state_1 : Std.Mutex Std.CancellationContext.State} {token_1 : Std.CancellationToken} {id_1 : UInt64},
  { state := state, token := token, id := id } = { state := state_1, token := token_1, id := id_1 } →
    state = state_1 ∧ token = token_1 ∧ id = id_1
-- Mathlib.Algebra.Free
FreeMagma.lift_symm_apply : ∀ {α : Type u} {β : Type v} [inst : Mul β] (F : FreeMagma α →ₙ* β) (a : α),
  FreeMagma.lift.symm F a = (⇑F ∘ FreeMagma.of) a
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the forward direction of `monovaryOn_iff_forall_mul_nonneg`. -/
MonovaryOn.sub_mul_sub_nonneg : ∀ {ι : Type u_1} {α : Type u_2} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {f g : ι → α}
  {s : Set ι}, MonovaryOn f g s → ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → 0 ≤ (f j - f i) * (g j - g i)
-- Lean.Environment
Lean.Kernel.Exception.unknownConstant.injEq : ∀ (env : Lean.Kernel.Environment) (name : Lean.Name) (env_1 : Lean.Kernel.Environment) (name_1 : Lean.Name),
  (Lean.Kernel.Exception.unknownConstant env name = Lean.Kernel.Exception.unknownConstant env_1 name_1) =
    (env = env_1 ∧ name = name_1)
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
/-- The Cartesian product of two bounded linear maps, as a bounded linear map.  -/
ContinuousLinearMap.prod : {R : Type u_1} →
  [inst : Semiring R] →
    {M₁ : Type u_2} →
      [inst_1 : TopologicalSpace M₁] →
        [inst_2 : AddCommMonoid M₁] →
          [inst_3 : Module R M₁] →
            {M₂ : Type u_3} →
              [inst_4 : TopologicalSpace M₂] →
                [inst_5 : AddCommMonoid M₂] →
                  [inst_6 : Module R M₂] →
                    {M₃ : Type u_4} →
                      [inst_7 : TopologicalSpace M₃] →
                        [inst_8 : AddCommMonoid M₃] →
                          [inst_9 : Module R M₃] → (M₁ →L[R] M₂) → (M₁ →L[R] M₃) → M₁ →L[R] M₂ × M₃
-- Mathlib.RingTheory.Smooth.IntegralClosure
/-- The comparison map from `S ⊗[R] integralClosure R B` to `integralClosure S (S ⊗[R] B)`.
This is injective when `S` is `R`-flat, and (TODO) bijective when `S` is `R`-smooth.  -/
TensorProduct.toIntegralClosure : (R : Type u_1) →
  (S : Type u_2) →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          (B : Type u_4) →
            [inst_3 : CommRing B] →
              [inst_4 : Algebra R B] →
                TensorProduct R S ↥(integralClosure R B) →ₐ[S] ↥(integralClosure S (TensorProduct R S B))
-- Mathlib.GroupTheory.GroupAction.Period
MulAction.period_bounded_of_exponent_pos : ∀ (α : Type v) {M : Type u} [inst : Monoid M] [inst_1 : MulAction M α],
  0 < Monoid.exponent M → ∀ (m : M), BddAbove (Set.range fun a => MulAction.period m a)
-- Init.Data.Rat.Basic
/-- Addition of rational numbers. (This definition is `@[irreducible]` because you don't want to
unfold it. Use `Rat.add_def` instead.)
 -/
Rat.add : ℚ → ℚ → ℚ
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.mem_ofObjects_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {I : Type u_1} (Y : I → C) {Z X : C} (g : Z ⟶ X),
  (CategoryTheory.Sieve.ofObjects Y X).arrows g ↔ ∃ i, Nonempty (Z ⟶ Y i)
-- Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
CategoryTheory.Functor.LeftLinear.toLaxLeftLinear : {D : Type u_1} →
  {D' : Type u_2} →
    {inst : CategoryTheory.Category.{v_1, u_1} D} →
      {inst_1 : CategoryTheory.Category.{v_2, u_2} D'} →
        {F : CategoryTheory.Functor D D'} →
          {C : Type u_3} →
            {inst_2 : CategoryTheory.Category.{v_3, u_3} C} →
              {inst_3 : CategoryTheory.MonoidalCategory C} →
                {inst_4 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D} →
                  {inst_5 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D'} →
                    [self : F.LeftLinear C] → F.LaxLeftLinear C
-- Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Set.powersetCard.instAddActionElemFinset : (G : Type u_1) →
  [inst : AddGroup G] →
    {α : Type u_2} → [AddAction G α] → {n : ℕ} → [DecidableEq α] → AddAction G ↑(Set.powersetCard α n)
-- Mathlib.Data.Matrix.Mul
Matrix.diag_vecMulVec : ∀ {n : Type u_3} {α : Type v} [inst : Mul α] (u v : n → α), (Matrix.vecMulVec u v).diag = u * v
-- Mathlib.Data.UInt
UInt8.instCommMonoid : CommMonoid UInt8
-- Mathlib.Data.Set.Lattice
Set.biUnion_sdiff_biUnion_subset : ∀ {α : Type u_1} {β : Type u_2} (t : α → Set β) (s₁ s₂ : Set α), (⋃ x ∈ s₁, t x) \ ⋃ x ∈ s₂, t x ⊆ ⋃ x ∈ s₁ \ s₂, t x
-- Mathlib.CategoryTheory.GradedObject.Unitor
/-- The cofan `mapBifunctorRightUnitorCofan F Y e p hp X j` is a colimit.  -/
CategoryTheory.GradedObject.mapBifunctorRightUnitorCofanIsColimit : {C : Type u_1} →
  {D : Type u_2} →
    {I : Type u_3} →
      {J : Type u_4} →
        [inst : CategoryTheory.Category.{v_1, u_1} C] →
          [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
            [inst_2 : Zero I] →
              [inst_3 : DecidableEq I] →
                [inst_4 : CategoryTheory.Limits.HasInitial C] →
                  (F : CategoryTheory.Functor D (CategoryTheory.Functor C D)) →
                    (Y : C) →
                      (e : F.flip.obj Y ≅ CategoryTheory.Functor.id D) →
                        [inst_5 :
                            ∀ (X : D),
                              CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.obj X)] →
                          (p : J × I → J) →
                            (hp : ∀ (j : J), p (j, 0) = j) →
                              (X : CategoryTheory.GradedObject J D) →
                                (j : J) →
                                  CategoryTheory.Limits.IsColimit
                                    (CategoryTheory.GradedObject.mapBifunctorRightUnitorCofan F Y e p hp X j)
-- Mathlib.CategoryTheory.Limits.Preserves.Lattice
CategoryTheory.Limits.CompleteLattice.preservesColimit_finite_toFunctor : ∀ {α : Type u} {β : Type v} {F : Type u_1} [inst : FunLike F α β] (f : F) [inst_1 : SemilatticeSup α]
  [inst_2 : OrderBot α] [inst_3 : SemilatticeSup β] [inst_4 : OrderBot β] [inst_5 : SupBotHomClass F α β] {J : Type w}
  [inst_6 : CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] (K : CategoryTheory.Functor J α),
  CategoryTheory.Limits.PreservesColimit K (↑f).toFunctor
-- Init.Data.Int.Gcd
Int.gcd_one_right : ∀ (a : ℤ), a.gcd 1 = 1
-- Mathlib.Topology.UniformSpace.LocallyUniformConvergence
TendstoLocallyUniformlyOn.congr : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : TopologicalSpace α] [inst_1 : UniformSpace β] {F : ι → α → β}
  {f : α → β} {s : Set α} {p : Filter ι} {G : ι → α → β},
  TendstoLocallyUniformlyOn F f p s → (∀ (n : ι), Set.EqOn (F n) (G n) s) → TendstoLocallyUniformlyOn G f p s
-- Mathlib.Algebra.Category.BialgCat.Basic
BialgCat.forget_reflects_isos : ∀ {R : Type u} [inst : CommRing R], (CategoryTheory.forget (BialgCat R)).ReflectsIsomorphisms
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.mem_addFundamentalFrontier : ∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] {s : Set α} {x : α},
  x ∈ MeasureTheory.addFundamentalFrontier G s ↔ x ∈ s ∧ ∃ g, g ≠ 0 ∧ x ∈ g +ᵥ s
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.contains_inter!_eq_false_of_contains_eq_false_right : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  m₁.WF →
    m₂.WF →
      ∀ {k : α},
        Std.DTreeMap.Internal.Impl.contains k m₂ = false → Std.DTreeMap.Internal.Impl.contains k (m₁.inter! m₂) = false
-- Mathlib.Data.Int.GCD
Nat.exists_mul_mod_eq_of_coprime : ∀ {k n : ℕ} (r : ℕ), n.Coprime k → k ≠ 0 → ∃ m < k, n * m % k = r % k
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.proj_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (S : D) (T : CategoryTheory.Functor C D) (X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit S) T),
  (CategoryTheory.StructuredArrow.proj S T).obj X = X.right
-- Mathlib.MeasureTheory.Function.LpOrder
MeasureTheory.Lp.instHasSolidNorm : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {p : ENNReal}
  [inst : NormedAddCommGroup E] [inst_1 : Lattice E] [inst_2 : HasSolidNorm E] [inst_3 : IsOrderedAddMonoid E]
  [inst_4 : Fact (1 ≤ p)], HasSolidNorm ↥(MeasureTheory.Lp E p μ)
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebraClass.subtype_injective : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Star A]
  [inst_3 : Module R A] {S : Type w''} [inst_4 : SetLike S A] [inst_5 : NonUnitalSubsemiringClass S A]
  [hSR : SMulMemClass S R A] [inst_6 : StarMemClass S A] (s : S),
  Function.Injective ⇑(NonUnitalStarSubalgebraClass.subtype s)
-- Mathlib.Data.Real.Basic
Real.ofCauchy_nnratCast : ∀ (q : ℚ≥0), { cauchy := ↑q } = ↑q
-- Mathlib.RingTheory.Finiteness.Small
Submodule.small_span : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Small.{u, u_1} R]
  (s : Set M) [Small.{u, u_2} ↑s], Small.{u, u_2} ↥(Submodule.span R s)
-- Lean.Meta.WHNF
/-- Create the `i`th projection `major`. It tries to use the auto-generated projection functions if available. Otherwise falls back
to `Expr.proj`.
 -/
Lean.Meta.mkProjFn : Lean.ConstructorVal → List Lean.Level → Array Lean.Expr → ℕ → Lean.Expr → Lean.CoreM Lean.Expr
-- Lean.Meta.Tactic.Generalize
_private.Lean.Meta.Tactic.Generalize.0.Lean.Meta.generalizeCore.go : Array Lean.Meta.GeneralizeArg → Lean.Meta.TransparencyMode → Lean.Expr → ℕ → Lean.MetaM Lean.Expr
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.restrict_loops_eq : ∀ {α : Type u_1} {M : Matroid α} {R : Set α}, R ⊆ M.E → (M.restrict R).loops = M.loops ∩ R
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.ExcenterExists.isTangentAt_exsphere_iff_eq_touchpoint : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] {s : Affine.Simplex ℝ P n} {signs : Finset (Fin (n + 1))},
  s.ExcenterExists signs →
    ∀ {i : Fin (n + 1)} {p : P},
      (s.exsphere signs).IsTangentAt p (affineSpan ℝ (Set.range (s.faceOpposite i).points)) ↔ p = s.touchpoint signs i
-- Mathlib.LinearAlgebra.Quotient.Defs
Submodule.Quotient.mk_surjective : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (p : Submodule R M),
  Function.Surjective Submodule.Quotient.mk
-- Mathlib.Algebra.Category.Ring.Basic
CommSemiRingCat.instFullSemiRingCatForget₂RingHomCarrierCarrier : (CategoryTheory.forget₂ CommSemiRingCat SemiRingCat).Full
-- Init.Data.String.Decode
ByteArray.utf8DecodeChar?.assemble₂ : UInt8 → UInt8 → Option Char
-- Lean.Data.JsonRpc
Lean.JsonRpc.ErrorCode.parseError.sizeOf_spec : sizeOf Lean.JsonRpc.ErrorCode.parseError = 1
-- Init.Data.BitVec.Lemmas
BitVec.shiftLeft_ofNat_eq : ∀ {w : ℕ} {x : BitVec w} {k : ℕ}, x <<< BitVec.ofNat w k = x <<< (k % 2 ^ w)
-- Init.Data.Range.Polymorphic.RangeIterator
_private.Init.Data.Range.Polymorphic.RangeIterator.0.Std.IterM.DefaultConsumers.forIn'.match_1.eq_2 : ∀ {β : Type u_3} (γ : Type u_1) (PlausibleForInStep : β → γ → ForInStep γ → Prop) (acc : γ) (out : β)
  (motive : Subtype (PlausibleForInStep out acc) → Sort u_2) (c : γ) (h : PlausibleForInStep out acc (ForInStep.done c))
  (h_1 : (c : γ) → (h' : PlausibleForInStep out acc (ForInStep.yield c)) → motive ⟨ForInStep.yield c, h'⟩)
  (h_2 : (c : γ) → (h : PlausibleForInStep out acc (ForInStep.done c)) → motive ⟨ForInStep.done c, h⟩),
  (match ⟨ForInStep.done c, h⟩ with
    | ⟨ForInStep.yield c, h'⟩ => h_1 c h'
    | ⟨ForInStep.done c, h⟩ => h_2 c h) =
    h_2 c h
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
NumberField.Embeddings.instNonemptyRingHom : ∀ (K : Type u_1) [inst : Field K] (A : Type u_2) [inst_1 : Field A] [CharZero A] [NumberField K] [IsAlgClosed A],
  Nonempty (K →+* A)
-- Mathlib.Algebra.Polynomial.Splits
/-- **Alias** of the forward direction of `Polynomial.splits_mul_X`. -/
Polynomial.Splits.of_mul_X : ∀ {R : Type u_1} [inst : CommRing R] {f : Polynomial R} [IsDomain R], (f * Polynomial.X).Splits → f.Splits
-- Mathlib.Algebra.Lie.Weights.Basic
/-- **Alias** of `LieModule.Weight.equivSetOfPred`.

---

The set of weights is equivalent to a subtype.  -/
LieModule.Weight.equivSetOf : (R : Type u_2) →
  (L : Type u_3) →
    (M : Type u_4) →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : LieAlgebra R L] →
            [inst_3 : AddCommGroup M] →
              [inst_4 : Module R M] →
                [inst_5 : LieRingModule L M] →
                  [inst_6 : LieModule R L M] →
                    [inst_7 : LieRing.IsNilpotent L] → LieModule.Weight R L M ≃ ↑{χ | LieModule.genWeightSpace M χ ≠ ⊥}
-- Mathlib.Topology.ContinuousMap.Basic
ContinuousMap.piEquiv_apply : ∀ {I : Type u_5} (A : Type u_6) (X : I → Type u_7) [inst : TopologicalSpace A]
  [inst_1 : (i : I) → TopologicalSpace (X i)] (f : (i : I) → C(A, X i)),
  (ContinuousMap.piEquiv A X) f = ContinuousMap.pi f
-- Mathlib.Algebra.Order.Module.Defs
monotone_smul_right_of_nonneg : ∀ {α : Type u_1} {β : Type u_2} {b : β} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : Preorder β] [inst_3 : Zero β]
  [SMulPosMono α β], 0 ≤ b → Monotone fun x => x • b
-- Std.Http.Data.Body.Full
/-- Builds a response with a binary body.
Sets `Content-Type: application/octet-stream`.
Use `fromBytes` instead if you need to set a different `Content-Type` or none at all.
 -/
Std.Http.Response.Builder.bytes : Std.Http.Response.Builder → ByteArray → Std.Async.Async (Std.Http.Response Std.Http.Body.Full)
-- Mathlib.Algebra.Group.Equiv.Defs
/-- `AddEquiv α β` is the type of an equiv `α ≃ β` which preserves addition.  -/
AddEquiv : (A : Type u_9) → (B : Type u_10) → [Add A] → [Add B] → Type (max u_10 u_9)
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
/-- Any measurable space structure on a countable space is countably generated.  -/
MeasurableSpace.instCountablyGeneratedOfCountable : ∀ {α : Type u_1} [inst : MeasurableSpace α] [Countable α], MeasurableSpace.CountablyGenerated α
-- Mathlib.Geometry.Euclidean.Sphere.Tangent
EuclideanGeometry.Sphere.IsTangentAt.eq_of_isTangentAt : ∀ {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 q : P} {as : AffineSubspace ℝ P},
  s.IsTangentAt p as → s.IsTangentAt q as → p = q
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.cocycles₂.coe_mk : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u_1, u, u} k G} (f : G × G → ↑A)
  (hf : f ∈ groupCohomology.cocycles₂ A), ⇑⟨f, hf⟩ = f
-- Mathlib.ModelTheory.Equivalence
FirstOrder.Language.Theory.sup_imp_iff : ∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ} {φ ψ θ : L.BoundedFormula α n},
  T.Imp (φ ⊔ ψ) θ ↔ T.Imp φ θ ∧ T.Imp ψ θ
-- Mathlib.Data.EReal.Basic
EReal.preimage_coe_Iic : ∀ (y : ℝ), Real.toEReal ⁻¹' Set.Iic ↑y = Set.Iic y
-- Mathlib.Analysis.Distribution.TestFunction
TestFunction.ofSupportedIn.congr_simp : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4}
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {n : ℕ∞} {K : TopologicalSpace.Compacts E}
  (K_sub_Ω : ↑K ⊆ ↑Ω) (f f_1 : ContDiffMapSupportedIn E F n K),
  f = f_1 → TestFunction.ofSupportedIn K_sub_Ω f = TestFunction.ofSupportedIn K_sub_Ω f_1
-- Mathlib.Topology.Algebra.Group.GroupTopology
AddGroupTopology.toTopologicalSpace_inf : ∀ {α : Type u} [inst : AddGroup α] (x y : AddGroupTopology α),
  (x ⊓ y).toTopologicalSpace = x.toTopologicalSpace ⊓ y.toTopologicalSpace
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.L1.SimpleFunc.setToL1S_mono_left : ∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {G'' : Type u_7} [inst_2 : NormedAddCommGroup G''] [inst_3 : PartialOrder G'']
  [IsOrderedAddMonoid G''] [inst_5 : NormedSpace ℝ G''] {T T' : Set α → E →L[ℝ] G''},
  (∀ (s : Set α) (x : E), (T s) x ≤ (T' s) x) →
    ∀ (f : ↥(α →₁ₛ[μ] E)), MeasureTheory.L1.SimpleFunc.setToL1S T f ≤ MeasureTheory.L1.SimpleFunc.setToL1S T' f
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.instIsGEObjTruncGE : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (X : C) (n : ℤ), t.IsGE ((t.truncGE n).obj X) n
-- Mathlib.Algebra.Algebra.Subalgebra.MulOpposite
Subalgebra.algEquivOpMop_apply : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  (S : Subalgebra R A) (a : ↥S.toSubsemiring), S.algEquivOpMop a = MulOpposite.op (S.addEquivOp a)
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.centerCongr_apply_coe : ∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] (e : R ≃+* S)
  (r : ↥(Subsemigroup.center R)), ↑((Subsemiring.centerCongr e) r) = e ↑r
-- Std.Data.DHashMap.Lemmas
/-- Variant of `get?_map` that holds with `EquivBEq` (i.e. without `LawfulBEq`).  -/
Std.DHashMap.Const.get?_map' : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {γ : Type w} {m : Std.DHashMap α fun x => β}
  [inst : EquivBEq α] [inst_1 : LawfulHashable α] {f : α → β → γ} {k : α},
  Std.DHashMap.Const.get? (Std.DHashMap.map f m) k =
    Option.pmap (fun v h' => f (m.getKey k h') v) (Std.DHashMap.Const.get? m k) ⋯
-- Mathlib.Algebra.CubicDiscriminant
Cubic.equiv_symm_apply_a : ∀ {R : Type u_1} [inst : Semiring R] (f : { p // p.degree ≤ 3 }), (Cubic.equiv.symm f).a = (↑f).coeff 3
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- The morphism that is part of a structured arrow.  -/
CategoryTheory.StructuredArrow.hom : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {S : D} → {T : CategoryTheory.Functor C D} → (X : CategoryTheory.StructuredArrow S T) → S ⟶ T.obj X.right
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.get?_insertMany_list_of_not_mem_of_mem : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α],
  m.WF →
    ∀ {l : List α} {k k' : α},
      (k == k') = true →
        k ∉ m → List.Pairwise (fun a b => (a == b) = false) l → k ∈ l → (m.insertMany l).get? k' = some k
-- Mathlib.Data.Quot
/-- When writing a lemma about `someSetoid x y` (which uses this instance),
call it `someSetoid_apply` not `someSetoid_r`.  -/
Setoid.instCoeFunForallForallProp_mathlib : {α : Sort u_1} → CoeFun (Setoid α) fun x => α → α → Prop
-- Lean.Elab.Tactic.Grind.Basic
/-- Cache for `BackwardRule`s created from elaborated terms, keyed by syntax byte position range (sym mode only).  -/
Lean.Elab.Tactic.Grind.Cache.backwardRuleSyntax : Lean.Elab.Tactic.Grind.Cache → Lean.PHashMap (ℕ × ℕ) Lean.Meta.Sym.BackwardRule
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.IsDetector.def : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {G : C},
  CategoryTheory.IsDetector G →
    ∀ ⦃X Y : C⦄ (f : X ⟶ Y),
      (∀ (h : G ⟶ Y), ∃! h', CategoryTheory.CategoryStruct.comp h' f = h) → CategoryTheory.IsIso f
-- Mathlib.CategoryTheory.Monoidal.CommMon_
/-- Natural transformations between functors lift to monoid objects.  -/
CategoryTheory.Functor.mapCommMonNatTrans : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        {D : Type u₂} →
          [inst_3 : CategoryTheory.Category.{v₂, u₂} D] →
            [inst_4 : CategoryTheory.MonoidalCategory D] →
              [inst_5 : CategoryTheory.BraidedCategory D] →
                {F F' : CategoryTheory.Functor C D} →
                  [inst_6 : F.LaxBraided] →
                    [inst_7 : F'.LaxBraided] →
                      (f : F ⟶ F') → [CategoryTheory.NatTrans.IsMonoidal f] → F.mapCommMon ⟶ F'.mapCommMon
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Linear
CategoryTheory.Abelian.Ext.homLinearEquiv_apply : ∀ {R : Type t} [inst : Ring R] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.Linear R C] [inst_4 : CategoryTheory.HasExt C] {X Y : C}
  {n : ℕ} [inst_5 : HasDerivedCategory C] (a : CategoryTheory.Abelian.Ext X Y n),
  CategoryTheory.Abelian.Ext.homLinearEquiv a = CategoryTheory.Abelian.Ext.homAddEquiv.toFun a
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.piComparison_comp_π : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) (f : β → C)
  [inst_2 : CategoryTheory.Limits.HasProduct f] [inst_3 : CategoryTheory.Limits.HasProduct fun b => G.obj (f b)]
  (b : β),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.piComparison G f)
      (CategoryTheory.Limits.Pi.π (fun b => G.obj (f b)) b) =
    G.map (CategoryTheory.Limits.Pi.π f b)
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
SeminormFamily.basisSets_zero : ∀ {R : Type u_1} {E : Type u_6} {ι : Type u_9} [inst : SeminormedRing R] [inst_1 : AddCommGroup E] [inst_2 : Module R E]
  (p : SeminormFamily R E ι), ∀ U ∈ p.basisSets, 0 ∈ U
-- Mathlib.Data.Seq.Computation
/-- assertion that there is some term `a` such that the `Computation` terminates  -/
Computation.Terminates.term : ∀ {α : Type u} {s : Computation α} [self : s.Terminates], ∃ a, a ∈ s
-- Mathlib.Topology.DiscreteQuotient
DiscreteQuotient.map_id : ∀ {X : Type u_2} [inst : TopologicalSpace X] {A : DiscreteQuotient X}, DiscreteQuotient.map (ContinuousMap.id X) ⋯ = id
-- Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
/-- A pair of continuous linear equivalences generates a continuous linear equivalence between
the spaces of continuous linear maps. This version is for the type alias
`UniformConvergenceCLM`.  -/
ContinuousLinearEquiv.uniformConvergenceCLMCongr : {𝕜 : Type u_6} →
  {E : Type u_7} →
    {F : Type u_8} →
      {G : Type u_9} →
        {H : Type u_10} →
          [inst : AddCommGroup E] →
            [inst_1 : AddCommGroup F] →
              [inst_2 : AddCommGroup G] →
                [inst_3 : AddCommGroup H] →
                  [inst_4 : NormedField 𝕜] →
                    [inst_5 : Module 𝕜 E] →
                      [inst_6 : Module 𝕜 F] →
                        [inst_7 : Module 𝕜 G] →
                          [inst_8 : Module 𝕜 H] →
                            [inst_9 : TopologicalSpace E] →
                              [inst_10 : TopologicalSpace F] →
                                [inst_11 : TopologicalSpace G] →
                                  [inst_12 : TopologicalSpace H] →
                                    [inst_13 : IsTopologicalAddGroup G] →
                                      [inst_14 : IsTopologicalAddGroup H] →
                                        [inst_15 : ContinuousConstSMul 𝕜 G] →
                                          [inst_16 : ContinuousConstSMul 𝕜 H] →
                                            (e₁ : E ≃L[𝕜] F) →
                                              (H ≃L[𝕜] G) →
                                                (𝔖 : Set (Set E)) →
                                                  (𝔗 : Set (Set F)) →
                                                    (∀ (t : Set F), t ∈ 𝔗 ↔ ⇑e₁ ⁻¹' t ∈ 𝔖) →
                                                      UniformConvergenceCLM (RingHom.id 𝕜) H 𝔖 ≃L[𝕜]
                                                        UniformConvergenceCLM (RingHom.id 𝕜) G 𝔗