mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Comma.Over.OverClass
/-- Bundle a morphism `f : X ⟶ Y` with `HomIsOver f S` into a morphism in `Over S`.  -/
CategoryTheory.OverClass.asOverHom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      (S : C) →
        [inst_1 : CategoryTheory.OverClass X S] →
          [inst_2 : CategoryTheory.OverClass Y S] →
            (f : X ⟶ Y) →
              [CategoryTheory.HomIsOver f S] → CategoryTheory.OverClass.asOver X S ⟶ CategoryTheory.OverClass.asOver Y S
-- Std.Http.Data.Headers.Name
Std.Http.Header.Name.mk.inj : ∀ {value : String}
  {isValidHeaderValue :
    autoParam (Std.Http.Header.IsValidHeaderName value) Std.Http.Header.Name.isValidHeaderValue._autoParam}
  {isLowerCase : autoParam (Std.Http.Internal.IsLowerCase value) Std.Http.Header.Name.isLowerCase._autoParam}
  {value_1 : String}
  {isValidHeaderValue_1 :
    autoParam (Std.Http.Header.IsValidHeaderName value_1) Std.Http.Header.Name.isValidHeaderValue._autoParam}
  {isLowerCase_1 : autoParam (Std.Http.Internal.IsLowerCase value_1) Std.Http.Header.Name.isLowerCase._autoParam},
  { value := value, isValidHeaderValue := isValidHeaderValue, isLowerCase := isLowerCase } =
      { value := value_1, isValidHeaderValue := isValidHeaderValue_1, isLowerCase := isLowerCase_1 } →
    value = value_1
-- Mathlib.CategoryTheory.MorphismProperty.Local
CategoryTheory.MorphismProperty.IsLocalAtTarget.inf : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {K : CategoryTheory.Precoverage C}
  (P Q : CategoryTheory.MorphismProperty C) [P.IsLocalAtTarget K] [Q.IsLocalAtTarget K], (P ⊓ Q).IsLocalAtTarget K
-- Mathlib.Probability.Independence.CharacteristicFunction
ProbabilityTheory.iIndepFun.charFunDual_map_sum_eq_prod : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {ι : Type u_2} {E : Type u_3}
  [inst : MeasurableSpace E] [inst_1 : NormedAddCommGroup E] [BorelSpace E] [SecondCountableTopology E] {X : ι → Ω → E}
  [inst_4 : Fintype ι] [inst_5 : NormedSpace ℝ E],
  (∀ (i : ι), AEMeasurable (X i) P) →
    ProbabilityTheory.iIndepFun X P →
      MeasureTheory.charFunDual (MeasureTheory.Measure.map (∑ i, X i) P) =
        ∏ i, MeasureTheory.charFunDual (MeasureTheory.Measure.map (X i) P)
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.IsReduced.append_overlap : ∀ {α : Type u} {L₁ L₂ L₃ : List (α × Bool)},
  FreeAddGroup.IsReduced (L₁ ++ L₂) →
    FreeAddGroup.IsReduced (L₂ ++ L₃) → L₂ ≠ [] → FreeAddGroup.IsReduced (L₁ ++ L₂ ++ L₃)
-- Mathlib.CategoryTheory.Sites.SheafOfTypes
/-- The property of being separated is preserved under isomorphisms.  -/
CategoryTheory.Presieve.isSeparated_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)}
  (J : CategoryTheory.GrothendieckTopology C) {P' : CategoryTheory.Functor Cᵒᵖ (Type w)} (i : P ≅ P'),
  CategoryTheory.Presieve.IsSeparated J P → CategoryTheory.Presieve.IsSeparated J P'
-- Mathlib.Order.Category.BddDistLat
BddDistLat.hom_id : ∀ {X : BddDistLat}, BddDistLat.Hom.hom (CategoryTheory.CategoryStruct.id X) = BoundedLatticeHom.id ↑X.toDistLat
-- Mathlib.Data.Ordmap.Invariants
Ordnode.balancedSz_zero : ∀ {l : ℕ}, Ordnode.BalancedSz l 0 ↔ l ≤ 1
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKey_insertIfNew : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  (h : t.WF) {k : α} {v : β k},
  (Std.DTreeMap.Internal.Impl.insertIfNew k v t ⋯).impl.maxKey ⋯ =
    t.maxKey?.elim k fun k' => if compare k' k = Ordering.lt then k else k'
-- Mathlib.RingTheory.Coprime.Basic
IsRelPrime.of_add_mul_right_right : ∀ {R : Type u} [inst : CommSemiring R] {x y z : R}, IsRelPrime x (y + z * x) → IsRelPrime x y
-- Init.Meta.Defs
/-- Creates syntax representing a Lean constant application, but avoids degenerate empty applications.
 -/
Lean.Syntax.mkCApp : Lean.Name → Lean.TSyntaxArray `term → Lean.Term
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.coe_toSubalgebra : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : StarRing A] [inst_4 : Algebra R A] [inst_5 : StarModule R A] (S : StarSubalgebra R A), ↑S.toSubalgebra = ↑S
-- Mathlib.Topology.Order.Basic
nhds_top_basis_Ici : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : OrderTop α] [OrderTopology α]
  [Nontrivial α] [DenselyOrdered α], (nhds ⊤).HasBasis (fun a => a < ⊤) Set.Ici
-- Mathlib.Data.List.TFAE
List.tfae_cons_cons : ∀ {a b : Prop} {l : List Prop}, (a :: b :: l).TFAE ↔ (a ↔ b) ∧ (b :: l).TFAE
-- Init.Data.Array.Attach
Array.attach_filter : ∀ {α : Type u_1} {xs : Array α} (p : α → Bool),
  (Array.filter p xs).attach = Array.filterMap (fun x => if w : p ↑x = true then some ⟨↑x, ⋯⟩ else none) xs.attach
-- Mathlib.Analysis.Complex.Circle
Circle.ext_iff : ∀ {x y : Circle}, x = y ↔ ↑x = ↑y
-- Mathlib.RingTheory.Ideal.Maps
RingEquiv.idealComapOrderIso_apply : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : Semiring S] (e : R ≃+* S) (I : Ideal S),
  e.idealComapOrderIso I = Ideal.comap e I
-- Mathlib.CategoryTheory.Monoidal.Center
CategoryTheory.Center.ofBraided_ε_f : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C],
  (CategoryTheory.Functor.LaxMonoidal.ε (CategoryTheory.Center.ofBraided C)).f =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Center C)).fst
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.fromOpcycles_d : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i j k : ι) [inst_2 : K.HasHomology i],
  CategoryTheory.CategoryStruct.comp (K.fromOpcycles i j) (K.d j k) = 0
-- Mathlib.GroupTheory.Coxeter.Basic
CoxeterSystem.prod_alternatingWord_eq_prod_alternatingWord_sub : ∀ {B : Type u_1} {W : Type u_3} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i i' : B),
  ∀ m ≤ M.M i i' * 2,
    cs.wordProd (CoxeterSystem.alternatingWord i i' m) =
      cs.wordProd (CoxeterSystem.alternatingWord i' i (M.M i i' * 2 - m))
-- Mathlib.RingTheory.MvPolynomial.Homogeneous
MvPolynomial.mem_iff_homogeneousComponent_mem : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R] {I : Ideal (MvPolynomial σ R)},
  Ideal.IsHomogeneous (MvPolynomial.homogeneousSubmodule σ R) I →
    ∀ (p : MvPolynomial σ R), p ∈ I ↔ ∀ (n : ℕ), (MvPolynomial.homogeneousComponent n) p ∈ I
-- Mathlib.FieldTheory.Finiteness
/-- In a Noetherian module over a division ring, all bases are indexed by a finite type.  -/
IsNoetherian.fintypeBasisIndex : {K : Type u} →
  {V : Type v} →
    [inst : DivisionRing K] →
      [inst_1 : AddCommGroup V] →
        [inst_2 : Module K V] → {ι : Type u_1} → [IsNoetherian K V] → Module.Basis ι K V → Fintype ι
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.pullbackRestrictIsoRestrict_inv_fst : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U : Y.Opens),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.pullbackRestrictIsoRestrict f U).inv
      (CategoryTheory.Limits.pullback.fst f U.ι) =
    ((TopologicalSpace.Opens.map f.base).obj U).ι
-- Mathlib.Topology.MetricSpace.Lipschitz
lipschitzOnWith_iff_dist_le_mul : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {K : NNReal} {s : Set α}
  {f : α → β}, LipschitzOnWith K f s ↔ ∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ ↑K * dist x y
-- Init.Data.Range.Polymorphic.Iterators
Std.Roc.Internal.isPlausibleIndirectOutput_iter_iff : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LE α] [inst_2 : DecidableLE α] [inst_3 : LT α]
  [Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α] [Std.PRange.LawfulUpwardEnumerableLT α]
  {r : Std.Roc α} {a : α}, (Std.Roc.Internal.iter r).IsPlausibleIndirectOutput a ↔ a ∈ r
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.insertManyIfNewUnit_ind : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {ρ : Type w} [inst : ForIn Id ρ α]
  {motive : (Std.DHashMap α fun x => Unit) → Prop} (m : Std.DHashMap α fun x => Unit) (l : ρ),
  motive m →
    (∀ (m : Std.DHashMap α fun x => Unit) (a : α), motive m → motive (m.insertIfNew a ())) →
      motive (Std.DHashMap.Const.insertManyIfNewUnit m l)
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.id_comp : ∀ {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] (f : P →ᴬ[R] Q),
  (ContinuousAffineMap.id R Q).comp f = f
-- Mathlib.RingTheory.Algebraic.Denominator
Algebra.denominator_dvd_iff : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : IsPrincipalIdealRing R] [inst_2 : CommRing S]
  [inst_3 : Algebra R S] {r : R} {x : S}, Algebra.denominator R x ∣ r ↔ IsIntegral R (r • x)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CallHierarchyOutgoingCallsParams.mk.inj : ∀ {item item_1 : Lean.Lsp.CallHierarchyItem}, { item := item } = { item := item_1 } → item = item_1
-- Mathlib.LinearAlgebra.Matrix.Transvection
/-- Multiplying by all the matrices in `listTransvecRow M` kills all the coefficients in the
last row but the last one.  -/
Matrix.Pivot.mul_listTransvecRow_last_row : ∀ {𝕜 : Type u_3} [inst : Field 𝕜] {r : ℕ} (M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜),
  M (Sum.inr ()) (Sum.inr ()) ≠ 0 →
    ∀ (i : Fin r), (M * (Matrix.Pivot.listTransvecRow M).prod) (Sum.inr ()) (Sum.inl i) = 0
-- Mathlib.RingTheory.WittVector.Defs
WittVector.wittOne.congr_simp : ∀ (p p_1 : ℕ) (e_p : p = p_1) [hp : Fact (Nat.Prime p)] (a a_1 : ℕ),
  a = a_1 → WittVector.wittOne p a = WittVector.wittOne p_1 a_1
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.image_mul_right_Icc' : ∀ {G₀ : Type u_2} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [MulPosReflectLT G₀] {c : G₀} (a b : G₀),
  0 < c → (fun x => x * c) '' Set.Icc a b = Set.Icc (a * c) (b * c)
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.intCast_comp : ∀ {R : Type u} [inst : Ring R] {p : Polynomial R} (i : ℤ), (↑i).comp p = ↑i
-- Mathlib.Analysis.Normed.Group.Defs
ENormedAddCommMonoid.mk : {E : Type u_8} →
  [inst : TopologicalSpace E] →
    [toESeminormedAddCommMonoid : ESeminormedAddCommMonoid E] → (∀ (x : E), ‖x‖ₑ = 0 ↔ x = 0) → ENormedAddCommMonoid E
-- Init.Data.List.Lemmas
List.idRun_foldlM : ∀ {β : Type u_1} {α : Type u_2} {f : β → α → Id β} {b : β} {l : List α},
  (List.foldlM f b l).run = List.foldl (fun x1 x2 => (f x1 x2).run) b l
-- Mathlib.Algebra.Category.Grp.Limits
CommGrpCat.forget₂Group_preservesLimit : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommGrpCat),
  CategoryTheory.Limits.PreservesLimit F (CategoryTheory.forget₂ CommGrpCat GrpCat)
-- Mathlib.CategoryTheory.Presentable.Directed
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₁_P : ∀ {J : Type w} [inst : CategoryTheory.SmallCategory J] {κ : Cardinal.{w}} [inst_1 : Fact κ.IsRegular] {ι : Type w}
  (D : ι → CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.DiagramWithUniqueTerminal J κ)
  (hι : HasCardinalLT ι κ) (m a : J),
  (CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₁ D hι m).P a = ((∃ a_1, (D a_1).P a) ∨ m = a)
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
/-- Given a dense subsite `F : C₀ ⥤ C` and a family
`data : ∀ X, OneHypercoverDenseData F J₀ J X` and a sheaf `G₀` on `J₀`,
this is the value on an object `X : C` of the "extension" of `G₀`
as a sheaf on `J` (see `OneHypercoverDenseData.essSurj.presheaf` and
`OneHypercoverDenseData.essSurj.isSheaf`): it is defined as
a multiequalizer using `data X`.  -/
CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObj : {C₀ : Type u₀} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v₀, u₀} C₀] →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {F : CategoryTheory.Functor C₀ C} →
          {J₀ : CategoryTheory.GrothendieckTopology C₀} →
            {J : CategoryTheory.GrothendieckTopology C} →
              {A : Type u'} →
                [inst_2 : CategoryTheory.Category.{v', u'} A] →
                  ((X : C) → F.OneHypercoverDenseData J₀ J X) →
                    [CategoryTheory.Limits.HasLimitsOfSize.{w, w, v', u'} A] → CategoryTheory.Sheaf J₀ A → C → A
-- Mathlib.Topology.UniformSpace.Dini
/-- **Dini's theorem**: if `F n` is a monotone increasing collection of continuous functions
converging pointwise to a continuous function `f`, then `F n` converges locally uniformly to `f`.  -/
Monotone.tendstoLocallyUniformly_of_forall_tendsto : ∀ {ι : Type u_1} {α : Type u_2} {G : Type u_3} [inst : Preorder ι] [inst_1 : TopologicalSpace α]
  [inst_2 : NormedAddCommGroup G] [inst_3 : Lattice G] [HasSolidNorm G] [IsOrderedAddMonoid G] {F : ι → α → G}
  {f : α → G},
  (∀ (i : ι), Continuous (F i)) →
    Monotone F →
      Continuous f →
        (∀ (x : α), Filter.Tendsto (fun x_1 => F x_1 x) Filter.atTop (nhds (f x))) →
          TendstoLocallyUniformly F f Filter.atTop
-- Mathlib.CategoryTheory.Limits.Presheaf
CategoryTheory.Functor.isPointwiseLeftKanExtensionOfIsLeftKanExtension.congr_simp : ∀ {C : Type u_1} {D : Type u_2} {H : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_4, u_4} H]
  {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} [inst_3 : L.HasPointwiseLeftKanExtension F]
  (F' : CategoryTheory.Functor D H) (α : F ⟶ L.comp F') [inst_4 : F'.IsLeftKanExtension α] (Y : D),
  CategoryTheory.Functor.isPointwiseLeftKanExtensionOfIsLeftKanExtension F' α Y =
    CategoryTheory.Functor.isPointwiseLeftKanExtensionOfIsLeftKanExtension F' α Y
-- Mathlib.SetTheory.Cardinal.Finite
Nat.card_eq_card_toFinset : ∀ {α : Type u_1} (s : Set α) [inst : Fintype ↑s], Nat.card ↑s = s.toFinset.card
-- Mathlib.MeasureTheory.Measure.MeasureSpace
/-- **Alias** of `MeasureTheory.measure_sdiff_null'`. -/
MeasureTheory.measure_diff_null' : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s₁ s₂ : Set α},
  μ (s₁ ∩ s₂) = 0 → μ (s₁ \ s₂) = μ s₁
-- Mathlib.Algebra.Lie.Submodule
/-- A Lie submodule of a Lie module is a submodule that is closed under the Lie bracket.
This is a sufficient condition for the subset itself to form a Lie module.  -/
LieSubmodule : (R : Type u) →
  (L : Type v) →
    (M : Type w) →
      [inst : CommRing R] →
        [inst_1 : LieRing L] → [inst_2 : AddCommGroup M] → [Module R M] → [LieRingModule L M] → Type w
-- Std.Data.Internal.List.Associative
Std.Internal.List.maxKey!_le : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  [inst_4 : Inhabited α] {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    l.isEmpty = false →
      ∀ {k : α},
        (compare (Std.Internal.List.maxKey! l) k).isLE = true ↔
          ∀ (k' : α), Std.Internal.List.containsKey k' l = true → (compare k' k).isLE = true
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
AugmentedSimplexCategory.instFullSimplexCategoryInclusion : AugmentedSimplexCategory.inclusion.Full
-- Mathlib.Analysis.InnerProductSpace.Defs
InnerProductSpace.Core.inner_im_symm : ∀ {𝕜 : Type u_1} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F]
  [c : PreInnerProductSpace.Core 𝕜 F] (x y : F), RCLike.im (inner 𝕜 x y) = -RCLike.im (inner 𝕜 y x)
-- Mathlib.Order.SuccPred.Archimedean
strictMonoOn_of_lt_succ : ∀ {α : Type u_3} {β : Type u_4} [inst : PartialOrder α] [inst_1 : Preorder β] [inst_2 : SuccOrder α]
  [IsSuccArchimedean α] {s : Set α} {f : α → β},
  s.OrdConnected → (∀ (a : α), ¬IsMax a → a ∈ s → Order.succ a ∈ s → f a < f (Order.succ a)) → StrictMonoOn f s
-- Mathlib.Data.Multiset.Fintype
/-- Create a type that has the same number of elements as the multiset.
Terms of this type are triples `⟨x, ⟨i, h⟩⟩` where `x : α`, `i : ℕ`, and `h : i < m.count x`.
This way repeated elements of a multiset appear multiple times from different values of `i`.  -/
Multiset.instCoeSortType : {α : Type u_1} → [DecidableEq α] → CoeSort (Multiset α) (Type u_1)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
WeierstrassCurve.Affine.Y_sub_negPolynomial : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Affine R}, Polynomial.X - W'.negPolynomial = W'.polynomialY
-- Mathlib.Geometry.Manifold.Algebra.SMul
instContMDiffVAddOfNatWithTopENat : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {H' : Type u_4}
  [inst_4 : TopologicalSpace H'] {E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  {I' : ModelWithCorners 𝕜 E' H'} {G : Type u_8} [inst_7 : TopologicalSpace G] [inst_8 : ChartedSpace H G]
  {M : Type u_9} [inst_9 : TopologicalSpace M] [inst_10 : ChartedSpace H' M] [inst_11 : VAdd G M]
  [ContMDiffVAdd I I' 2 G M], ContMDiffVAdd I I' 1 G M
-- Mathlib.Algebra.Ring.Subsemiring.Basic
RingHom.eq_of_eqOn_sdense : ∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] {s : Set R},
  Subsemiring.closure s = ⊤ → ∀ {f g : R →+* S}, Set.EqOn (⇑f) (⇑g) s → f = g
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.StronglyMeasurable.finStronglyMeasurable_of_set_sigmaFinite : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : TopologicalSpace β] [inst_1 : Zero β] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α},
  MeasureTheory.StronglyMeasurable f →
    ∀ {t : Set α},
      MeasurableSet t →
        (∀ x ∈ tᶜ, f x = 0) → MeasureTheory.SigmaFinite (μ.restrict t) → MeasureTheory.FinStronglyMeasurable f μ
-- Mathlib.FieldTheory.KummerExtension
/-- The natural embedding of the roots of unity of `K` into `Gal(K[ⁿ√a]/K)`, by sending
`η ↦ (ⁿ√a ↦ η • ⁿ√a)`. Also see `autAdjoinRootXPowSubC` for the `AlgEquiv` version.  -/
autAdjoinRootXPowSubCHom : {K : Type u} →
  [inst : Field K] →
    (n : ℕ) →
      (a : K) →
        ↥(rootsOfUnity n K) →*
          AdjoinRoot (Polynomial.X ^ n - Polynomial.C a) →ₐ[K] AdjoinRoot (Polynomial.X ^ n - Polynomial.C a)
-- Mathlib.RingTheory.Extension.Presentation.Core
Algebra.SubmersivePresentation.invJacobianOfHasCoeffs.congr_simp : ∀ {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [inst_3 : Finite σ] (P P_1 : Algebra.SubmersivePresentation R S ι σ) (e_P : P = P_1)
  (R₀ : Type u_5) [inst_4 : CommRing R₀] [inst_5 : Algebra R₀ R] [inst_6 : Algebra R₀ S] [inst_7 : IsScalarTower R₀ R S]
  [inst_8 : P.HasCoeffs R₀], P.invJacobianOfHasCoeffs R₀ = P_1.invJacobianOfHasCoeffs R₀
-- Mathlib.Data.Finset.Sups
Finset.coe_sups : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeSup α] (s t : Finset α), ↑(s ⊻ t) = ↑s ⊻ ↑t
-- Mathlib.NumberTheory.Padics.PadicNumbers
Padic.complete' : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] (f : CauSeq ℚ_[p] ⇑padicNormE),
  ∃ q, ∀ ε > 0, ∃ N, ∀ i ≥ N, padicNormE (q - ↑f i) < ε
-- Mathlib.Combinatorics.Quiver.Covering
/-- Constructor for `Quiver.PathStar`. Defined to be `Sigma.mk`.  -/
Quiver.PathStar.mk : {U : Type u_1} → [inst : Quiver U] → {u v : U} → Quiver.Path u v → Quiver.PathStar u
-- Mathlib.Order.Category.HeytAlg
HeytAlg.hasForgetToLat_forget₂_obj_str : ∀ (X : HeytAlg), (CategoryTheory.HasForget₂.forget₂.obj X).str = GeneralizedHeytingAlgebra.toDistribLattice
-- Mathlib.LinearAlgebra.TensorProduct.Defs
TensorProduct.instModule : {R : Type u_1} →
  [inst : CommSemiring R] →
    {M : Type u_7} →
      {N : Type u_8} →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : AddCommMonoid N] → [inst_3 : Module R M] → [inst_4 : Module R N] → Module R (TensorProduct R M N)
-- Lean.Parser
Lean.PrettyPrinter.Formatter.strLit.formatter : Lean.PrettyPrinter.Formatter
-- Batteries.Data.Float.Lemmas
Float32.beq_self_eq_false_iff : ∀ {f : Float32}, (f == f) = false ↔ f = Float32.nan
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
/-- Eta-expanded form of `TendstoLocallyUniformly.inv` -/
TendstoLocallyUniformly.fun_inv : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : Group α] [IsUniformGroup α] {ι : Type u_3} {X : Type u_4}
  [inst_3 : TopologicalSpace X] {F : ι → X → α} {f : X → α} {l : Filter ι},
  TendstoLocallyUniformly F f l → TendstoLocallyUniformly (fun i i_1 => (F i i_1)⁻¹) (fun i => (f i)⁻¹) l
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.isIso_leftRightHomologyComparison'_of_homologyData : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.HomologyData),
  CategoryTheory.IsIso (CategoryTheory.ShortComplex.leftRightHomologyComparison' h.left h.right)
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
/-- Turn an element of a type `F` satisfying
`AddMonoidHomClass F A B` and `ContinuousMapClass F A B` into a `ContinuousAddMonoidHom`.
This is declared as the default coercion from `F` to `ContinuousAddMonoidHom A B`.  -/
ContinuousAddMonoidHom.toContinuousAddMonoidHom : {A : Type u_2} →
  {B : Type u_3} →
    [inst : AddMonoid A] →
      [inst_1 : AddMonoid B] →
        [inst_2 : TopologicalSpace A] →
          [inst_3 : TopologicalSpace B] →
            {F : Type u_7} →
              [inst_4 : FunLike F A B] → [AddMonoidHomClass F A B] → [ContinuousMapClass F A B] → F → A →ₜ+ B
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHom.comp_id : ∀ {α : Type u_5} [inst : NonUnitalNonAssocSemiring α] (f : CentroidHom α), f.comp (CentroidHom.id α) = f
-- Mathlib.Combinatorics.Matroid.Sum
Matroid.sum_isBase_iff : ∀ {α : Type u} {β : Type v} {M : Matroid α} {N : Matroid β} {B : Set (α ⊕ β)},
  (M.sum N).IsBase B ↔ M.IsBase (Sum.inl ⁻¹' B) ∧ N.IsBase (Sum.inr ⁻¹' B)
-- Mathlib.CategoryTheory.Adjunction.PartialAdjoint
CategoryTheory.Functor.partialLeftAdjointHomEquiv_comp_symm : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor D C) {X X' : F.PartialLeftAdjointSource} {Y : D} (f : X'.obj ⟶ F.obj Y) (g : X ⟶ X'),
  CategoryTheory.CategoryStruct.comp (F.partialLeftAdjointMap g) (F.partialLeftAdjointHomEquiv.symm f) =
    F.partialLeftAdjointHomEquiv.symm (CategoryTheory.CategoryStruct.comp g.hom f)
-- Mathlib.CategoryTheory.Preadditive.Injective.Basic
/-- The `ObjectProperty C` corresponding to the notion of injective objects in `C`.  -/
CategoryTheory.isInjective : (C : Type u₁) → [inst : CategoryTheory.Category.{v₁, u₁} C] → CategoryTheory.ObjectProperty C
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.arccos_eq_pi_div_two_sub_arcsin : ∀ (x : ℝ), Real.arccos x = Real.pi / 2 - Real.arcsin x
-- Mathlib.Order.Bounds.Basic
isGreatest_singleton : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, IsGreatest {a} a
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKey!.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Inhabited α] (xs : List ((a : α) × β a)),
  Std.Internal.List.minKey! xs = (Std.Internal.List.minKey? xs).get!
-- Mathlib.CategoryTheory.Category.ReflQuiv
CategoryTheory.Cat.FreeReflRel.mk : ∀ {V : Type u_1} [inst : CategoryTheory.ReflQuiver V] {X : V},
  CategoryTheory.Cat.FreeReflRel V X X (CategoryTheory.ReflQuiver.id X).toPath Quiver.Path.nil
-- Mathlib.AlgebraicGeometry.Morphisms.Constructors
/-- If a property of maps of topological spaces is satisfied by all homeomorphisms,
every isomorphism of schemes satisfies the induced property.  -/
AlgebraicGeometry.topologically_iso_le : ∀ (P : {α β : Type u} → [TopologicalSpace α] → [TopologicalSpace β] → (α → β) → Prop),
  (∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α ≃ₜ β), P ⇑f) →
    CategoryTheory.MorphismProperty.isomorphisms AlgebraicGeometry.Scheme ≤
      AlgebraicGeometry.topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => P