mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Category.Ring.FilteredColimits
RingCat.FilteredColimits.forget_preservesFilteredColimits : CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget RingCat)
-- Mathlib.CategoryTheory.MorphismProperty.LocalClosure
CategoryTheory.MorphismProperty.sourceLocalClosure.below.comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {K : CategoryTheory.Precoverage C}
  {P : CategoryTheory.MorphismProperty C}
  {motive : ⦃X Y : C⦄ → (x : X ⟶ Y) → CategoryTheory.MorphismProperty.sourceLocalClosure K P x → Prop} {X Y : C}
  (f : X ⟶ Y) (hf : CategoryTheory.MorphismProperty.sourceLocalClosure K P f) (R : CategoryTheory.Presieve X)
  (hR : R ∈ K.coverings X) {U : C} (g : U ⟶ X) (a : R g),
  CategoryTheory.MorphismProperty.sourceLocalClosure.below hf →
    motive f hf → CategoryTheory.MorphismProperty.sourceLocalClosure.below ⋯
-- Init.Data.String.Basic
List.asString_nil : String.ofList [] = ""
-- Mathlib.RingTheory.Filtration
Ideal.trivialFiltration_N : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (I : Ideal R)
  (N : Submodule R M) (x : ℕ), (I.trivialFiltration N).N x = N
-- Init.Data.Range.Polymorphic.IntLemmas
Int.isSome_getElem?_toList_rco_eq : ∀ {m n : ℤ} {i : ℕ}, ((m...n).toList[i]?.isSome = true) = (i < (n - m).toNat)
-- Init.Data.Bool
/-- Converts `true` to `1` and `false` to `0`.
 -/
Bool.toInt : Bool → ℤ
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
CategoryTheory.Bicategory.Adj.iso₂Mk_inv_τr : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : CategoryTheory.Bicategory.Adj B} {α β : a ⟶ b}
  (el : α.l ≅ β.l) (er : β.r ≅ α.r)
  (h :
    autoParam ((CategoryTheory.Bicategory.conjugateEquiv β.adj α.adj) el.hom = er.hom)
      CategoryTheory.Bicategory.Adj.iso₂Mk._auto_1),
  (CategoryTheory.Bicategory.Adj.iso₂Mk el er h).inv.τr = er.inv
-- Lean.DocString.Parser
/-- The nested list context, innermost first.
 -/
Lean.Doc.Parser.BlockCtxt.inLists : Lean.Doc.Parser.BlockCtxt → List Lean.Doc.Parser.InList
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.isSome_apply_of_mem_filterMap : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.DTreeMap.Raw α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] {f : α → β → Option γ} {k : α} (h : t.WF) (h' : k ∈ Std.DTreeMap.Raw.filterMap f t),
  (f (t.getKey k ⋯) (Std.DTreeMap.Raw.Const.get t k ⋯)).isSome = true
-- Mathlib.Computability.Encoding
Computability.Γ'.bit.sizeOf_spec : ∀ (b : Bool), sizeOf (Computability.Γ'.bit b) = 1 + sizeOf b
-- Mathlib.Algebra.Group.Hom.Defs
instInhabitedAddHom : {M : Type u_4} → {N : Type u_5} → [inst : Add M] → [inst_1 : AddZeroClass N] → Inhabited (M →ₙ+ N)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
WeierstrassCurve.isMinimal_iff : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsDiscreteValuationRing R] {K : Type u_2}
  [inst_3 : Field K] [inst_4 : Algebra R K] [inst_5 : IsFractionRing R K] (W : WeierstrassCurve K),
  WeierstrassCurve.IsMinimal R W ↔
    MaximalFor (fun C => WeierstrassCurve.IsIntegral R (C • W)) (fun C => WeierstrassCurve.valuation_Δ_aux R (C • W)) 1
-- Mathlib.AlgebraicGeometry.Limits
AlgebraicGeometry.Scheme.empty_ext_iff : ∀ {X : AlgebraicGeometry.Scheme} {f g : ∅ ⟶ X}, f = g ↔ True
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.SplitInfo.getExpr : Lean.Meta.Grind.SplitInfo → Lean.Expr
-- Mathlib.GroupTheory.GroupAction.ConjAct
ConjAct.instInhabited : {G : Type u_3} → [DivInvMonoid G] → Inhabited (ConjAct G)
-- Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
IsBoundedBilinearMap.isBigO_comp : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : Semiring 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : SeminormedAddCommGroup F] [inst_4 : Module 𝕜 F] [inst_5 : SeminormedAddCommGroup G]
  [inst_6 : Module 𝕜 G] {f : E × F → G} {α : Type u_5},
  IsBoundedBilinearMap 𝕜 f →
    ∀ {g : α → E} {h : α → F} {l : Filter α}, (fun x => f (g x, h x)) =O[l] fun x => ‖g x‖ * ‖h x‖
-- Mathlib.Topology.EMetricSpace.Diam
/-- The diameter of a subsingleton vanishes.  -/
Metric.ediam_subsingleton : ∀ {X : Type u_2} {s : Set X} [inst : PseudoEMetricSpace X], s.Subsingleton → Metric.ediam s = 0
-- Std.Data.ExtDHashMap.Basic
/-- Tries to retrieve the mapping for the given key, returning `none` if no such mapping is present.

Uses the `LawfulBEq` instance to cast the retrieved value to the correct type.
 -/
Std.ExtDHashMap.get? : {α : Type u} →
  {β : α → Type v} → {x : BEq α} → {x_1 : Hashable α} → [LawfulBEq α] → Std.ExtDHashMap α β → (a : α) → Option (β a)
-- Mathlib.Data.Fin.Tuple.NatAntidiagonal
Multiset.Nat.nodup_antidiagonalTuple : ∀ (k n : ℕ), (Multiset.Nat.antidiagonalTuple k n).Nodup
-- Mathlib.GroupTheory.Perm.Sign
Equiv.Perm.sign_surjective : ∀ (α : Type u) [inst : DecidableEq α] [inst_1 : Fintype α] [Nontrivial α], Function.Surjective ⇑Equiv.Perm.sign
-- Mathlib.Topology.MetricSpace.Lipschitz
/-- **Alias** of the reverse direction of `lipschitzOnWith_iff_dist_le_mul`. -/
LipschitzOnWith.of_dist_le_mul : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {K : NNReal} {s : Set α}
  {f : α → β}, (∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ ↑K * dist x y) → LipschitzOnWith K f s
-- Mathlib.Data.Sym.Sym2
Sym2.mkEmbedding_apply : ∀ {α : Type u_1} (a b : α), (Sym2.mkEmbedding a) b = s(a, b)
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
/-- **Alias** of `UniformOnFun.isClosed_setOfPred_continuous`.

---

Suppose that the topology on `α` is defined by its restrictions to the sets of `𝔖`.

Then the set of continuous functions is closed
in the topology of uniform convergence on the sets of `𝔖`.  -/
UniformOnFun.isClosed_setOf_continuous : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace β] {𝔖 : Set (Set α)} [inst_1 : TopologicalSpace α],
  Topology.IsCoherentWith 𝔖 → IsClosed {f | Continuous ((UniformOnFun.toFun 𝔖) f)}
-- Mathlib.Algebra.Ring.Subsemiring.Defs
Subsemiring.copy_eq : ∀ {R : Type u} [inst : NonAssocSemiring R] (S : Subsemiring R) (s : Set R) (hs : s = ↑S), S.copy s hs = S
-- Mathlib.Analysis.Complex.RealDeriv
/-- If a complex function `e` is differentiable at a real point, then its restriction to `ℝ` is
differentiable there as a function `ℝ → ℂ`, with the same derivative.  -/
HasDerivAt.comp_ofReal : ∀ {e : ℂ → ℂ} {e' : ℂ} {z : ℝ}, HasDerivAt e e' ↑z → HasDerivAt (fun y => e ↑y) e' z
-- Mathlib.Analysis.Normed.Module.Multilinear.Curry
ContinuousMultilinearMap.norm_map_snoc_le : ∀ {𝕜 : Type u} {n : ℕ} {Ei : Fin n.succ → Type wEi} {G : Type wG} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)] [inst_2 : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)]
  [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 Ei G)
  (m : (i : Fin n) → Ei i.castSucc) (x : Ei (Fin.last n)), ‖f (Fin.snoc m x)‖ ≤ (‖f‖ * ∏ i, ‖m i‖) * ‖x‖
-- Std.Time.Time.Unit.Millisecond
Std.Time.Millisecond.instTransOrdOrdinal : Std.TransOrd Std.Time.Millisecond.Ordinal
-- Mathlib.Analysis.LocallyConvex.Bounded
Bornology.IsVonNBounded.sub : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : SeminormedRing 𝕜] [inst_1 : AddGroup E] [inst_2 : TopologicalSpace E]
  [IsTopologicalAddGroup E] [inst_4 : DistribMulAction 𝕜 E] {s t : Set E},
  Bornology.IsVonNBounded 𝕜 s → Bornology.IsVonNBounded 𝕜 t → Bornology.IsVonNBounded 𝕜 (s - t)
-- Lean.Meta.Sym.ReplaceS
_private.Lean.Meta.Sym.ReplaceS.0.Lean.Meta.Sym.visit.match_1.eq_11 : ∀ (motive : Lean.Expr → Sort u_1) (binderName : Lean.Name) (d b : Lean.Expr) (binderInfo : Lean.BinderInfo)
  (h_1 : (a : Lean.Literal) → motive (Lean.Expr.lit a)) (h_2 : (mvarId : Lean.MVarId) → motive (Lean.Expr.mvar mvarId))
  (h_3 : (deBruijnIndex : ℕ) → motive (Lean.Expr.bvar deBruijnIndex))
  (h_4 : (fvarId : Lean.FVarId) → motive (Lean.Expr.fvar fvarId))
  (h_5 : (declName : Lean.Name) → (us : List Lean.Level) → motive (Lean.Expr.const declName us))
  (h_6 : (u : Lean.Level) → motive (Lean.Expr.sort u)) (h_7 : (f a : Lean.Expr) → motive (f.app a))
  (h_8 : (data : Lean.MData) → (a : Lean.Expr) → motive (Lean.Expr.mdata data a))
  (h_9 : (typeName : Lean.Name) → (idx : ℕ) → (a : Lean.Expr) → motive (Lean.Expr.proj typeName idx a))
  (h_10 :
    (binderName : Lean.Name) →
      (d b : Lean.Expr) → (binderInfo : Lean.BinderInfo) → motive (Lean.Expr.forallE binderName d b binderInfo))
  (h_11 :
    (binderName : Lean.Name) →
      (d b : Lean.Expr) → (binderInfo : Lean.BinderInfo) → motive (Lean.Expr.lam binderName d b binderInfo))
  (h_12 :
    (declName : Lean.Name) → (t v b : Lean.Expr) → (nondep : Bool) → motive (Lean.Expr.letE declName t v b nondep)),
  (match Lean.Expr.lam binderName d b binderInfo with
    | Lean.Expr.lit a => h_1 a
    | Lean.Expr.mvar mvarId => h_2 mvarId
    | Lean.Expr.bvar deBruijnIndex => h_3 deBruijnIndex
    | Lean.Expr.fvar fvarId => h_4 fvarId
    | Lean.Expr.const declName us => h_5 declName us
    | Lean.Expr.sort u => h_6 u
    | f.app a => h_7 f a
    | Lean.Expr.mdata data a => h_8 data a
    | Lean.Expr.proj typeName idx a => h_9 typeName idx a
    | Lean.Expr.forallE binderName d b binderInfo => h_10 binderName d b binderInfo
    | Lean.Expr.lam binderName d b binderInfo => h_11 binderName d b binderInfo
    | Lean.Expr.letE declName t v b nondep => h_12 declName t v b nondep) =
    h_11 binderName d b binderInfo
-- Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
integral_exp_mul_Ioi : ∀ {a : ℝ}, a < 0 → ∀ (c : ℝ), ∫ (x : ℝ) in Set.Ioi c, Real.exp (a * x) = -Real.exp (a * c) / a
-- Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
HomotopicalAlgebra.CofibrantObject.bifibrantResolutionMap_fac' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C]
  {X₁ X₂ : HomotopicalAlgebra.CofibrantObject C} (f : X₁ ⟶ X₂),
  CategoryTheory.CategoryStruct.comp (HomotopicalAlgebra.CofibrantObject.toHoCat.map X₁.iBifibrantResolutionObj)
      (HomotopicalAlgebra.CofibrantObject.toHoCat.map
        (HomotopicalAlgebra.CofibrantObject.homMk (HomotopicalAlgebra.CofibrantObject.bifibrantResolutionMap f).hom)) =
    CategoryTheory.CategoryStruct.comp (HomotopicalAlgebra.CofibrantObject.toHoCat.map f)
      (HomotopicalAlgebra.CofibrantObject.toHoCat.map X₂.iBifibrantResolutionObj)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.mem_iff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp] {k : α},
  t₁.WF → t₂.WF → t₁.Equiv t₂ → (k ∈ t₁ ↔ k ∈ t₂)
-- Mathlib.Algebra.Order.BigOperators.GroupWithZero.Multiset
Multiset.one_le_prod_map : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] [inst_1 : PartialOrder R] [ZeroLEOneClass R] [PosMulMono R]
  {α : Type u_2} {s : Multiset α} {f : α → R}, (∀ a ∈ s, 1 ≤ f a) → 1 ≤ (Multiset.map f s).prod
-- Mathlib.Analysis.Normed.Module.RCLike.Extend
/-- `StrongDual.extendRCLike` bundled into a linear isometry equivalence.  -/
StrongDual.extendRCLikeₗᵢ : {𝕜 : Type u_1} →
  {F : Type u_3} →
    [inst : RCLike 𝕜] →
      [inst_1 : SeminormedAddCommGroup F] →
        [inst_2 : NormedSpace 𝕜 F] →
          [inst_3 : NormedSpace ℝ F] → [IsScalarTower ℝ 𝕜 F] → StrongDual ℝ F ≃ₗᵢ[ℝ] StrongDual 𝕜 F
-- Mathlib.Algebra.Homology.Embedding.CochainComplex
CochainComplex.instIsStrictlyLEExtendNatIntEmbeddingDownNatOfNat : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (X : ChainComplex C ℕ),
  CochainComplex.IsStrictlyLE (HomologicalComplex.extend X ComplexShape.embeddingDownNat) 0
-- Mathlib.RingTheory.Ideal.Quotient.Operations
Ideal.Quotient.factorₐ_apply : ∀ (R₁ : Type u_1) {A : Type u_3} [inst : CommSemiring R₁] [inst_1 : Ring A] [inst_2 : Algebra R₁ A] {I J : Ideal A}
  [inst_3 : I.IsTwoSided] [inst_4 : J.IsTwoSided] (hIJ : I ≤ J) (x : A ⧸ I),
  (Ideal.Quotient.factorₐ R₁ hIJ) x = (Ideal.Quotient.factor hIJ) x
-- Mathlib.Algebra.Group.Pi.Lemmas
Sigma.uncurry_neg : ∀ {α : Type u_5} {β : α → Type u_6} {γ : (a : α) → β a → Type u_7} [inst : (a : α) → (b : β a) → Neg (γ a b)]
  (x : (a : α) → (b : β a) → γ a b), Sigma.uncurry (-x) = -Sigma.uncurry x
-- Mathlib.Geometry.Manifold.Immersion
/-- If `f` is an immersion at `x` w.r.t. some complement `F`, it is an immersion at `x`.

Note that the proof contains a small formalisation-related subtlety: `F` can live in any universe,
while being an immersion at `x` requires the existence of a complement in the same universe as
the model normed space of `N`. This is solved by `smallComplement` and `smallEquiv`.
 -/
Manifold.IsImmersionAtOfComplement.isImmersionAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} {F : Type u_5}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E'']
  [inst_4 : NormedSpace 𝕜 E''] [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜 F] {H : Type u_7}
  [inst_7 : TopologicalSpace H] {G : Type u_9} [inst_8 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [inst_9 : TopologicalSpace M] [inst_10 : ChartedSpace H M]
  {N : Type u_13} [inst_11 : TopologicalSpace N] [inst_12 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M},
  Manifold.IsImmersionAtOfComplement F I J n f x → Manifold.IsImmersionAt I J n f x
-- Mathlib.Topology.MetricSpace.HausdorffDimension
dimH_sUnion : ∀ {X : Type u_2} [inst : EMetricSpace X] {S : Set (Set X)}, S.Countable → dimH (⋃₀ S) = ⨆ s ∈ S, dimH s
-- Mathlib.NumberTheory.RamificationInertia.Valuation
IsDedekindDomain.HeightOneSpectrum.uniformContinuous_algebraMap_liesOver : ∀ {A : Type u_1} (K : Type u_2) (L : Type u_3) {B : Type u_4} [inst : CommRing A] [inst_1 : IsDedekindDomain A]
  [inst_2 : CommRing B] [inst_3 : IsDedekindDomain B] [inst_4 : Algebra A B] [Module.IsTorsionFree A B]
  [inst_6 : Field K] [inst_7 : Field L] [inst_8 : Algebra K L] [inst_9 : Algebra A K] [inst_10 : IsFractionRing A K]
  [inst_11 : Algebra A L] [IsScalarTower A K L] [inst_13 : Algebra B L] [inst_14 : IsFractionRing B L]
  [IsScalarTower A B L] (v : IsDedekindDomain.HeightOneSpectrum A) (w : IsDedekindDomain.HeightOneSpectrum B)
  [w.asIdeal.LiesOver v.asIdeal],
  UniformContinuous
    ⇑(algebraMap (WithVal (IsDedekindDomain.HeightOneSpectrum.valuation K v))
        (WithVal (IsDedekindDomain.HeightOneSpectrum.valuation L w)))
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
tsum_indicator_of_notMem : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] (s : γ → Set β)
  (f : β → α) (i : β), (∀ (d : γ), i ∉ s d) → ∑' (d : γ), (s d).indicator f i = 0
-- Mathlib.AlgebraicTopology.CechNerve
CategoryTheory.CosimplicialObject.cechConerve_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 :
    ∀ (n : ℕ) (f : CategoryTheory.Arrow C),
      CategoryTheory.Limits.HasWidePushout f.left (fun x => f.right) fun x => f.hom]
  {X Y : CategoryTheory.Arrow C} (F : X ⟶ Y),
  CategoryTheory.CosimplicialObject.cechConerve.map F = CategoryTheory.Arrow.mapCechConerve F
-- Mathlib.Topology.Partial
ptendsto_nhds : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] {f : Y →. X} {l : Filter Y} {x : X},
  Filter.PTendsto f l (nhds x) ↔ ∀ (s : Set X), IsOpen s → x ∈ s → f.core s ∈ l
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.norm : Lean.Meta.Grind.Arith.Cutsat.LeCnstr → Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof
-- Lean.Parser.Do
Lean.Parser.Term.doLetMetaExpr.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.Group.Subgroup.Ker
AddSubgroup.map_subtype_lt_map_subtype : ∀ {G : Type u_1} [inst : AddGroup G] {G' : AddSubgroup G} {H K : AddSubgroup ↥G'},
  AddSubgroup.map G'.subtype H < AddSubgroup.map G'.subtype K ↔ H < K
-- Init.Data.Vector.Basic
/-- Set an element in a vector using a `Nat` index. Panics if the index is out of bounds.

This will perform the update destructively provided that the vector has a reference count of 1.
 -/
Vector.set! : {α : Type u_1} → {n : ℕ} → Vector α n → ℕ → α → Vector α n
-- Mathlib.CategoryTheory.Monad.Algebra
/-- To construct an isomorphism of algebras, it suffices to give an isomorphism of the carriers which
commutes with the structure morphisms.
 -/
CategoryTheory.Monad.Algebra.isoMk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {T : CategoryTheory.Monad C} →
      {A B : T.Algebra} →
        (h : A.A ≅ B.A) →
          autoParam
              (CategoryTheory.CategoryStruct.comp (T.map h.hom) B.a = CategoryTheory.CategoryStruct.comp A.a h.hom)
              CategoryTheory.Monad.Algebra.isoMk._auto_1 →
            (A ≅ B)
-- Init.Core
DoResultPRBC.continue.injEq : ∀ {α β σ : Type u} (a a_1 : σ), (DoResultPRBC.continue a = DoResultPRBC.continue a_1) = (a = a_1)
-- Mathlib.Algebra.Algebra.Opposite
AlgHom.opComm_apply_apply : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (a : A →ₐ[R] Bᵐᵒᵖ) (x : Aᵐᵒᵖ),
  (AlgHom.opComm a) x = MulOpposite.unop (a (MulOpposite.unop x))
-- Mathlib.MeasureTheory.Measure.AddContent
MeasureTheory.addContent_sUnion : ∀ {α : Type u_1} {C : Set (Set α)} {I : Finset (Set α)} {G : Type u_2} [inst : AddCommMonoid G]
  {m : MeasureTheory.AddContent G C}, ↑I ⊆ C → (↑I).PairwiseDisjoint id → ⋃₀ ↑I ∈ C → m (⋃₀ ↑I) = ∑ u ∈ I, m u
-- Mathlib.GroupTheory.OreLocalization.Basic
/-- The universal lift from a morphism `R →+ T`, which maps elements of `S` to
additive-units of `T`, to a morphism `AddOreLocalization R S →+ T`.  -/
AddOreLocalization.universalAddHom : {R : Type u_1} →
  [inst : AddMonoid R] →
    {S : AddSubmonoid R} →
      [inst_1 : AddOreLocalization.AddOreSet S] →
        {T : Type u_2} →
          [inst_2 : AddMonoid T] →
            (f : R →+ T) → (fS : ↥S →+ AddUnits T) → (∀ (s : ↥S), f ↑s = ↑(fS s)) → AddOreLocalization S R →+ T
-- Mathlib.RingTheory.Spectrum.Prime.Basic
PrimeSpectrum.zeroLocus_iUnion₂ : ∀ {R : Type u} [inst : CommSemiring R] {ι : Sort u_1} {κ : ι → Sort u_2} (s : (i : ι) → κ i → Set R),
  PrimeSpectrum.zeroLocus (⋃ i, ⋃ j, s i j) = ⋂ i, ⋂ j, PrimeSpectrum.zeroLocus (s i j)
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Equiv.coweightEquiv_one : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N),
  ↑(RootPairing.Equiv.coweightEquiv P P 1) = LinearMap.id
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coconeOfConeRightOp_pt : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor Jᵒᵖ C} (c : CategoryTheory.Limits.Cone F.rightOp),
  (CategoryTheory.Limits.coconeOfConeRightOp c).pt = Opposite.unop c.pt
-- Mathlib.Topology.UniformSpace.Defs
nhds_basis_uniformity : ∀ {α : Type ua} {ι : Sort u_1} [inst : UniformSpace α] {p : ι → Prop} {s : ι → SetRel α α},
  (uniformity α).HasBasis p s → ∀ {x : α}, (nhds x).HasBasis p fun i => {y | (y, x) ∈ s i}
-- Lean.Elab.App
/-- For a fieldname `fieldName`, locate all the environment constants with that name
 -/
_private.Lean.Elab.App.0.Lean.Elab.Term.reverseFieldLookup : Lean.Environment → String → Array Lean.Name
-- Mathlib.Logic.Equiv.Basic
Equiv.swapCore_comm : ∀ {α : Sort u_1} [inst : DecidableEq α] (r a b : α), Equiv.swapCore a b r = Equiv.swapCore b a r
-- Mathlib.CategoryTheory.Subfunctor.SubmonoidFunctor
CategoryTheory.SubmonoidFunctor.instMonoFunctorMonCatι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {M : CategoryTheory.Functor C MonCat}
  (S : CategoryTheory.SubmonoidFunctor M), CategoryTheory.Mono S.ι
-- Mathlib.CategoryTheory.MorphismProperty.Representable
CategoryTheory.Functor.relativelyRepresentable.pullback₃.snd_snd_eq_p₃_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} [inst_2 : F.Full] {A₁ A₂ A₃ : C} {X : D} {f₁ : F.obj A₁ ⟶ X}
  (hf₁ : F.relativelyRepresentable f₁) (f₂ : F.obj A₂ ⟶ X) (f₃ : F.obj A₃ ⟶ X)
  [inst_3 : CategoryTheory.Limits.HasPullback (hf₁.fst' f₂) (hf₁.fst' f₃)] {Z : C} (h : A₃ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (hf₁.fst' f₂) (hf₁.fst' f₃))
      (CategoryTheory.CategoryStruct.comp (hf₁.snd f₃) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.relativelyRepresentable.pullback₃.p₃ hf₁ f₂ f₃) h
-- Mathlib.Topology.PartitionOfUnity
/-- the supports of the underlying functions are a locally finite family of sets  -/
PartitionOfUnity.locallyFinite' : ∀ {ι : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {s : optParam (Set X) Set.univ}
  (self : PartitionOfUnity ι X s), LocallyFinite fun i => Function.support ⇑(self.toFun i)
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
/-- In a `LawfulDayConvolutionMonoidalCategoryStruct`, `ι.obj (d ⊗ d')` is a
Day convolution of `(ι C V).obj d` and `(ι C V).d'`.  -/
CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.convolution : (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) →
                      CategoryTheory.MonoidalCategory.DayConvolution
                        ((CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι C V D).obj d)
                        ((CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι C V D).obj d')
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.mem_erase : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k a : α},
  a ∈ t.erase k ↔ cmp k a ≠ Ordering.eq ∧ a ∈ t
-- Mathlib.Data.String.Basic
String.Legacy.front.eq_1 : ∀ (s : String), String.Legacy.front s = String.Pos.Raw.get s 0
-- Mathlib.Analysis.Meromorphic.Basic
meromorphicAt_comp_iff_of_deriv_ne_zero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : 𝕜} [CompleteSpace 𝕜] [CharZero 𝕜] {f : 𝕜 → E} {g : 𝕜 → 𝕜},
  AnalyticAt 𝕜 g x → deriv g x ≠ 0 → (MeromorphicAt (f ∘ g) x ↔ MeromorphicAt f (g x))
-- Mathlib.Util.FormatTable
Alignment.left.sizeOf_spec : sizeOf Alignment.left = 1
-- Mathlib.Data.Nat.Init
Nat.leRec_succ_left : ∀ {n : ℕ} {motive : (m : ℕ) → n ≤ m → Sort u_1} (refl : motive n ⋯)
  (le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯) {m : ℕ} (h1 : n ≤ m) (h2 : n + 1 ≤ m),
  Nat.leRec (le_succ_of_le ⋯ refl) (fun x h ih => le_succ_of_le ⋯ ih) h2 = Nat.leRec refl le_succ_of_le h1
-- Mathlib.RingTheory.Algebraic.Integral
Algebra.IsAlgebraic.transcendental_iff : ∀ (R : Type u_1) (S : Type u_2) {A : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Ring A]
  [inst_3 : Algebra R S] [inst_4 : Algebra R A] [inst_5 : Algebra S A] [IsScalarTower R S A] [NoZeroDivisors S]
  [FaithfulSMul R S] {a : A} [Algebra.IsAlgebraic R S], Transcendental R a ↔ Transcendental S a
-- Lean.Data.Position
/-- Convert a `Lean.Position` to a `String.Pos`.  -/
Lean.FileMap.ofPosition : Lean.FileMap → Lean.Position → String.Pos.Raw
-- Mathlib.Combinatorics.Quiver.ReflQuiver
CategoryTheory.ReflPrefunctor.comp_id : ∀ {U : Type u_1} {V : Type u_2} [inst : CategoryTheory.ReflQuiver U] [inst_1 : CategoryTheory.ReflQuiver V]
  (F : U ⥤rq V), F ⋙rq 𝟭rq V = F
-- Mathlib.Algebra.GCDMonoid.Basic
normalize_eq_normalize_iff : ∀ {α : Type u_1} [inst : MonoidWithZero α] [inst_1 : NormalizationMonoid α] [IsLeftCancelMulZero α] {x y : α},
  normalize x = normalize y ↔ x ∣ y ∧ y ∣ x