mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
/-- See Note [custom simps projection]  -/
LinearIsometryEquiv.Simps.symm_apply : {R : Type u_1} →
  {R₂ : Type u_2} →
    [inst : Semiring R] →
      [inst_1 : Semiring R₂] →
        (σ₁₂ : R →+* R₂) →
          {σ₂₁ : R₂ →+* R} →
            [inst_2 : RingHomInvPair σ₁₂ σ₂₁] →
              [inst_3 : RingHomInvPair σ₂₁ σ₁₂] →
                (E : Type u_11) →
                  (E₂ : Type u_12) →
                    [inst_4 : SeminormedAddCommGroup E] →
                      [inst_5 : SeminormedAddCommGroup E₂] →
                        [inst_6 : Module R E] → [inst_7 : Module R₂ E₂] → (E ≃ₛₗᵢ[σ₁₂] E₂) → E₂ → E
-- Mathlib.CategoryTheory.Enriched.FunctorCategory
CategoryTheory.Enriched.FunctorCategory.functorEnrichedId_app : ∀ (V : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} C] {J : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} J]
  [inst_4 : CategoryTheory.EnrichedOrdinaryCategory V C] (F₁ : CategoryTheory.Functor J C)
  [inst_5 : CategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom V F₁ F₁] (j : J),
  (CategoryTheory.Enriched.FunctorCategory.functorEnrichedId V F₁).app j =
    CategoryTheory.Enriched.FunctorCategory.enrichedId V ((CategoryTheory.Under.forget j).comp F₁)
-- Mathlib.NumberTheory.ModularForms.Basic
/-- These are `SlashInvariantForm`s that are holomorphic and zero at infinity.  -/
CuspForm : Subgroup (GL (Fin 2) ℝ) → ℤ → Type
-- Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic
CategoryTheory.Limits.Concrete.colimit_rep_eq_iff_exists : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type s}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC] {J : Type w}
  [inst_3 : CategoryTheory.Category.{r, w} J] (F : CategoryTheory.Functor J C)
  [CategoryTheory.Limits.PreservesColimit F (CategoryTheory.forget C)] [CategoryTheory.IsFiltered J]
  [inst_6 : CategoryTheory.Limits.HasColimit F] {i j : J} (x : CategoryTheory.ToType (F.obj i))
  (y : CategoryTheory.ToType (F.obj j)),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimit.ι F i)) x =
      (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimit.ι F j)) y ↔
    ∃ k f g, (CategoryTheory.ConcreteCategory.hom (F.map f)) x = (CategoryTheory.ConcreteCategory.hom (F.map g)) y
-- Mathlib.RingTheory.LinearDisjoint
/-- If `A` and `B` are linearly disjoint subalgebras in a commutative algebra `S` over `R`
such that `A ⊔ B = S`, then any `R`-basis of `B` is also an `A`-basis of `S`.
 -/
Subalgebra.LinearDisjoint.basisOfBasisRight : {R : Type u} →
  {S : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : CommSemiring S] →
        [inst_2 : Algebra R S] →
          {A B : Subalgebra R S} →
            A.LinearDisjoint B → A ⊔ B = ⊤ → {ι : Type u_1} → Module.Basis ι R ↥B → Module.Basis ι (↥A) S
-- Init.Data.UInt.Lemmas
UInt64.mod_self : ∀ {a : UInt64}, a % a = 0
-- Mathlib.Combinatorics.SimpleGraph.Ends.Defs
/-- In an infinite graph, the set of components out of a finite set is nonempty.  -/
SimpleGraph.componentCompl_nonempty_of_infinite : ∀ {V : Type u} (G : SimpleGraph V) [Infinite V] (K : Finset V), Nonempty (G.ComponentCompl ↑K)
-- Mathlib.SetTheory.Ordinal.Exponential
Ordinal.lt_opow_of_isSuccLimit : ∀ {a b c : Ordinal.{u_1}}, b ≠ 0 → Order.IsSuccLimit c → (a < b ^ c ↔ ∃ c' < c, a < b ^ c')
-- Mathlib.Analysis.LocallyConvex.Basic
Balanced.convexHull : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  {s : Set E} [inst_3 : PartialOrder 𝕜], Balanced 𝕜 s → Balanced 𝕜 ((convexHull 𝕜) s)
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.Opens.instFrame : {α : Type u_2} → [inst : TopologicalSpace α] → Order.Frame (TopologicalSpace.Opens α)
-- Mathlib.Geometry.Manifold.VectorBundle.Tangent
TangentBundle.symmL_model_space : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_8} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] (b b' : F),
  Bundle.Trivialization.symmL 𝕜 (trivializationAt F (TangentSpace (modelWithCornersSelf 𝕜 F)) b) b' = 1
-- Lean.Elab.InfoTree.Types
Lean.Elab.Info.ofCompletionInfo : Lean.Elab.CompletionInfo → Lean.Elab.Info
-- Mathlib.Combinatorics.Quiver.Path
Quiver.Path.instInhabited : {V : Type u} → [inst : Quiver V] → {a : V} → Inhabited (Quiver.Path a a)
-- Mathlib.Algebra.Category.Grp.Basic
AddCommGrpCat.hom_ofHom : ∀ {X Y : Type u} [inst : AddCommGroup X] [inst_1 : AddCommGroup Y] (f : X →+ Y),
  AddCommGrpCat.Hom.hom (AddCommGrpCat.ofHom f) = f
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.IsMaximumClique.mk : ∀ {α : Type u_3} [inst : Finite α] {G : SimpleGraph α} {s : Finset α},
  G.IsClique ↑s → (∀ (t : Finset α), G.IsClique ↑t → t.card ≤ s.card) → G.IsMaximumClique s
-- Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory
/-- A finite-products-preserving functor distributes over the tensor product of functors.  -/
CategoryTheory.Functor.Monoidal.tensorObjComp : {C : Type u_2} →
  {D : Type u_3} →
    {E : Type u_4} →
      [inst : CategoryTheory.Category.{v_2, u_2} C] →
        [inst_1 : CategoryTheory.Category.{v_3, u_3} D] →
          [inst_2 : CategoryTheory.Category.{v_4, u_4} E] →
            [inst_3 : CategoryTheory.CartesianMonoidalCategory C] →
              [inst_4 : CategoryTheory.CartesianMonoidalCategory E] →
                (F G : CategoryTheory.Functor D C) →
                  (H : CategoryTheory.Functor C E) →
                    [CategoryTheory.Limits.PreservesFiniteProducts H] →
                      (CategoryTheory.MonoidalCategoryStruct.tensorObj F G).comp H ≅
                        CategoryTheory.MonoidalCategoryStruct.tensorObj (F.comp H) (G.comp H)
-- Mathlib.Topology.Sets.Opens
/-- A homeomorphism induces an order-preserving equivalence on open sets, by taking comaps.  -/
Homeomorph.opensCongr : {α : Type u_2} →
  {β : Type u_3} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] → α ≃ₜ β → TopologicalSpace.Opens α ≃o TopologicalSpace.Opens β
-- Mathlib.MeasureTheory.Measure.Regular
MeasureTheory.Measure.InnerRegular.innerRegularWRT_isClosed_isOpen : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace α] [R1Space α]
  [OpensMeasurableSpace α] [h : μ.InnerRegular], μ.InnerRegularWRT IsClosed IsOpen
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.coe_union : ∀ (x y : ZFSet.{u}), ↑(x ∪ y) = ↑x ∪ ↑y
-- Mathlib.Tactic.Linter.FindDeprecations
/-- `removeDeprecations fname rgs` reads the content of `fname` and removes from it the substrings
whose ranges are in the array `rgs`.

The command makes the assumption that `rgs` is *sorted*.
 -/
_private.Mathlib.Tactic.Linter.FindDeprecations.0.Mathlib.Tactic.removeDeprecations : String → Array Lean.Syntax.Range → IO String
-- Mathlib.Data.Matrix.Block
Matrix.blockDiagonal'_eq_blockDiagonal : ∀ {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [inst : DecidableEq o] [inst_1 : Zero α]
  (M : o → Matrix m n α) {k k' : o} (i : m) (j : n),
  Matrix.blockDiagonal M (i, k) (j, k') = Matrix.blockDiagonal' M ⟨k, i⟩ ⟨k', j⟩
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
/-- If `f : 𝕜 → 𝕜` is continuous on `s` and `a : X → A` is continuous on `t : Set X`,
and `a x` satisfies the predicate `p` associated to `𝕜` and `s` is a common neighborhood of the
spectra of `a x` for all `x ∈ t`, then `fun x ↦ cfc f (a x)` is continuous on `t`.

This is weaker than `ContinuousOn.cfc` since it requires `f` to be continuous on a *neighborhood* of
the spectra, but in practice it is often easier to apply because `s` is not required to be compact,
nor does it require an indexed family of compact sets. This is proven using `ContinuousOn.cfc` and
`upperHemicontinuous_spectrum` to produce the necessary family of compact sets.  -/
ContinuousOn.cfc_of_mem_nhdsSet : ∀ {X : Type u_1} {𝕜 : Type u_2} {A : Type u_3} {p : A → Prop} [inst : RCLike 𝕜] [inst_1 : NormedRing A]
  [inst_2 : StarRing A] [inst_3 : NormedAlgebra 𝕜 A] [inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p]
  [ContinuousStar A] [CompleteSpace A] [inst_7 : TopologicalSpace X] {s : Set 𝕜} (f : 𝕜 → 𝕜) {a : X → A} {t : Set X},
  s ∈ nhdsSet (⋃ x ∈ t, spectrum 𝕜 (a x)) →
    ContinuousOn a t →
      autoParam (∀ x ∈ t, p (a x)) ContinuousOn.cfc_of_mem_nhdsSet._auto_1 →
        autoParam (ContinuousOn f s) ContinuousOn.cfc_of_mem_nhdsSet._auto_3 → ContinuousOn (fun x => cfc f (a x)) t
-- Lean.Setup
Lean.Import.mk : Lean.Name → Bool → Bool → Bool → Lean.Import
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.forIn'_roi : ∀ {α β : Type u} {m : Type u → Type v} {Pred EPred : Type u} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] [inst_4 : LT α]
  [DecidableLT α] [inst_6 : Std.PRange.UpwardEnumerable α] [inst_7 : Std.Rxi.IsAlwaysFinite α]
  [inst_8 : Std.PRange.LawfulUpwardEnumerable α] [inst_9 : Std.PRange.LawfulUpwardEnumerableLT α] {xs : Std.Roi α}
  {init : β} {f : (a : α) → a ∈ xs → β → m (ForInStep β)} (inv : Std.Internal.Do.Invariant xs.toList β Pred)
  {epost : EPred},
  (∀ (pref : List α) (cur : α) (suff : List α) (h : xs.toList = pref ++ cur :: suff) (b : β),
      ⦃ inv { «prefix» := pref, suffix := cur :: suff, property := ⋯ } b ⦄ f cur ⋯ b ⦃ fun r =>
        match r with
        | ForInStep.yield b' => inv { «prefix» := pref ++ [cur], suffix := suff, property := ⋯ } b'
        | ForInStep.done b' => inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b';
        epost ⦄) →
    ⦃ inv { «prefix» := [], suffix := xs.toList, property := ⋯ } init ⦄ forIn' xs init f ⦃ fun b =>
      inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b; epost ⦄
-- Mathlib.GroupTheory.Finiteness
Submonoid.FG.bot : ∀ {M : Type u_1} [inst : Monoid M], ⊥.FG
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.ext : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E] [inst_7 : Module R₂ E₂]
  {e e' : E ≃ₛₗᵢ[σ₁₂] E₂}, (∀ (x : E), e x = e' x) → e = e'
-- Mathlib.Order.Bounds.Image
image2_upperBounds_upperBounds_subset_upperBounds_image2 : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {f : α → β → γ}
  {s : Set α} {t : Set β},
  (∀ (b : β), Antitone (Function.swap f b)) →
    (∀ (a : α), Antitone (f a)) → Set.image2 f (lowerBounds s) (lowerBounds t) ⊆ upperBounds (Set.image2 f s t)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.mem_of_mem_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k a : α}
  {v : β}, a ∈ t.insertIfNew k v → cmp k a ≠ Ordering.eq → a ∈ t
-- Mathlib.RingTheory.TensorProduct.MvPolynomial
/-- Tensoring `MvPolynomial σ R` on the left by an `R`-algebra `A` is algebraically
equivalent to `MvPolynomial σ A`.  -/
MvPolynomial.algebraTensorAlgEquiv : (R : Type u) →
  [inst : CommSemiring R] →
    {σ : Type u_1} →
      (A : Type u_4) →
        [inst_1 : CommSemiring A] → [inst_2 : Algebra R A] → TensorProduct R A (MvPolynomial σ R) ≃ₐ[A] MvPolynomial σ A
-- Mathlib.Order.Height
Set.chainHeight_eq_of_relEmbedding : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {r' : β → β → Prop} (s : Set α) (e : r ↪r r'),
  (⇑e '' s).chainHeight r' = s.chainHeight r
-- Mathlib.Order.Interval.Basic
NonemptyInterval.instNontrivial : ∀ {α : Type u_1} [inst : Preorder α] [Nontrivial α], Nontrivial (NonemptyInterval α)
-- Init.Data.Array.Range
Array.zipIdx_eq_zip_range' : ∀ {α : Type u_1} {xs : Array α} {i : ℕ}, xs.zipIdx i = xs.zip (Array.range' i xs.size)
-- Mathlib.Analysis.Normed.Operator.Banach
ContinuousLinearMap.bijective_iff_dense_range_and_antilipschitz : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜'] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {σ : 𝕜 →+* 𝕜'} {σ' : 𝕜' →+* 𝕜}
  [inst_4 : RingHomInvPair σ σ'] {F : Type u_4} [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜' F]
  [CompleteSpace E] [CompleteSpace F] [RingHomInvPair σ' σ] [RingHomIsometric σ] [RingHomIsometric σ'] (f : E →SL[σ] F),
  Function.Bijective ⇑f ↔ (↑f).range.topologicalClosure = ⊤ ∧ ∃ c, AntilipschitzWith c ⇑f
-- Mathlib.Analysis.Normed.Module.Ball.Homeomorph
OpenPartialHomeomorph.continuousOn_univBall_symm : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {P : Type u_2}
  [inst_2 : PseudoMetricSpace P] [inst_3 : NormedAddTorsor E P] (c : P) (r : ℝ),
  ContinuousOn (↑(OpenPartialHomeomorph.univBall c r).symm) (Metric.ball c r)
-- Lean.Elab.ConfigEval.DeriveEvalConfigItem
Lean.Elab.ConfigEval.instInhabitedHandlerTrie.default : Lean.Elab.ConfigEval.HandlerTrie✝
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_rcc_eq_if : ∀ {m n : ℕ}, (m...=n).toList = if m ≤ n then m :: ((m + 1)...=n).toList else []
-- Lean.Elab.Task
/-- Given a monadic value in `MetaM`, creates a task that runs it in the current state,
returning a monadic value with the cached result (and subsequent state as it was after running).
 -/
Lean.Meta.MetaM.asTask' : {α : Type} → Lean.MetaM α → Lean.MetaM (Task (Lean.MetaM α))
-- Mathlib.Algebra.Group.TypeTags.Basic
isRegular_ofAdd : ∀ {α : Type u} [inst : AddMonoid α] {a : α}, IsRegular (Multiplicative.ofAdd a) ↔ IsAddRegular a
-- Mathlib.Algebra.Homology.ShortComplex.Linear
CategoryTheory.ShortComplex.homologyMap'_smul : ∀ {R : Type u_1} {C : Type u_2} [inst : Semiring R] [inst_1 : CategoryTheory.Category.{v_1, u_2} C]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Linear R C] {S₁ S₂ : CategoryTheory.ShortComplex C}
  {φ : S₁ ⟶ S₂} (h₁ : S₁.HomologyData) (h₂ : S₂.HomologyData) (a : R),
  CategoryTheory.ShortComplex.homologyMap' (a • φ) h₁ h₂ = a • CategoryTheory.ShortComplex.homologyMap' φ h₁ h₂
-- Init.Try
/-- `∎` (typed as `\qed`) is a macro that expands to `by try? (wrapWithBy := true)` in term mode.
The `wrapWithBy` config option causes suggestions to be prefixed with `by`.  -/
«term∎» : Lean.ParserDescr
-- Mathlib.NumberTheory.ModularForms.Discriminant
_private.Mathlib.NumberTheory.ModularForms.Discriminant.0.ModularForm.eta_comp_eqOn_const_mul_csqrt_eta : ∃ c,
  c ≠ 0 ∧
    Set.EqOn (ModularForm.eta ∘ fun z => -1 / z) (c • (Complex.sqrt * ModularForm.eta)) UpperHalfPlane.upperHalfPlaneSet
-- Mathlib.Topology.Algebra.Group.Basic
OrderDual.instContinuousNeg : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Neg G] [ContinuousNeg G], ContinuousNeg Gᵒᵈ
-- Mathlib.Algebra.Order.Hom.Ring
OrderRingIso.coe_toRingEquiv : ∀ {α : Type u_2} {β : Type u_3} [inst : Mul α] [inst_1 : Add α] [inst_2 : LE α] [inst_3 : Mul β] [inst_4 : Add β]
  [inst_5 : LE β] (f : α ≃+*o β), ⇑f.toRingEquiv = ⇑f
-- Mathlib.RingTheory.PrincipalIdealDomain
IsBezout.span_gcd_eq_span_gcd : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsBezout R] [IsDomain R] [inst_3 : GCDMonoid R] (x y : R),
  Ideal.span {gcd x y} = Ideal.span {IsBezout.gcd x y}
-- Lean.Data.Lsp.Ipc
Lean.Lsp.Ipc.CallHierarchy.brecOn_2.go : {motive_1 : Lean.Lsp.Ipc.CallHierarchy → Sort u} →
  {motive_2 : Array Lean.Lsp.Ipc.CallHierarchy → Sort u} →
    {motive_3 : List Lean.Lsp.Ipc.CallHierarchy → Sort u} →
      (t : List Lean.Lsp.Ipc.CallHierarchy) →
        ((t : Lean.Lsp.Ipc.CallHierarchy) → t.below → motive_1 t) →
          ((t : Array Lean.Lsp.Ipc.CallHierarchy) → Lean.Lsp.Ipc.CallHierarchy.below_1 t → motive_2 t) →
            ((t : List Lean.Lsp.Ipc.CallHierarchy) → Lean.Lsp.Ipc.CallHierarchy.below_2 t → motive_3 t) →
              motive_3 t ×' Lean.Lsp.Ipc.CallHierarchy.below_2 t
-- Init.Data.Array.Basic
Array.forIn'.loop : {α : Type u} →
  {β : Type v} →
    {m : Type v → Type w} →
      [Monad m] → (as : Array α) → ((a : α) → a ∈ as → β → m (ForInStep β)) → (i : ℕ) → i ≤ as.size → β → m β
-- Mathlib.Tactic.Linarith.Datatypes
Mathlib.Tactic.Linarith.Preprocessor.mk : Mathlib.Tactic.Linarith.PreprocessorBase →
  (Lean.Expr → Lean.MetaM (List Lean.Expr)) → Mathlib.Tactic.Linarith.Preprocessor
-- Init.Data.String.PosRaw
String.Pos.Raw.zero_addChar_byteIdx : ∀ (c : Char), (0 + c).byteIdx = c.utf8Size
-- Mathlib.Analysis.Meromorphic.NormalForm
/-- **Local identity theorem**: two meromorphic functions in normal form agree in a
neighborhood iff they agree in a pointed neighborhood.

See `ContinuousAt.eventuallyEq_nhds_iff_eventuallyEq_nhdsNE` for the analogous
statement for continuous functions.
 -/
MeromorphicNFAt.eventuallyEq_nhdsNE_iff_eventuallyEq_nhds : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜} {g : 𝕜 → E},
  MeromorphicNFAt f x → MeromorphicNFAt g x → (f =ᶠ[nhdsWithin x {x}ᶜ] g ↔ f =ᶠ[nhds x] g)
-- Mathlib.RingTheory.Ideal.Quotient.Operations
/-- The **first isomorphism theorem** for commutative rings (`RingHom.rangeS` version).  -/
RingHom.quotientKerEquivRangeS : {R : Type u} → {S : Type v} → [inst : Ring R] → [inst_1 : Semiring S] → (f : R →+* S) → R ⧸ RingHom.ker f ≃+* ↥f.rangeS
-- Mathlib.NumberTheory.Bernoulli
_private.Mathlib.NumberTheory.Bernoulli.0.Bernoulli.pIntegral_choose_mul_pow_div : ∀ {k m p : ℕ},
  m < k →
    ∀ [inst : Fact (Nat.Prime p)],
      2 * k - 2 * m ≥ 2 →
        Bernoulli.pIntegral✝ p (↑((2 * k).choose (2 * m)) * ↑p ^ (2 * k - 2 * m - 1) / (2 * ↑k - 2 * ↑m + 1))
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Real.iteratedDeriv_add_one_cos : ∀ (n : ℕ), iteratedDeriv (n + 1) Real.cos = -iteratedDeriv n Real.sin
-- Mathlib.Analysis.BoxIntegral.UnitPartition
_private.Mathlib.Analysis.BoxIntegral.UnitPartition.0.BoxIntegral.unitPartition.tendsto_card_div_pow₁ : {ι : Type u_1} →
  (s : Set (ι → ℝ)) →
    [inst : Finite ι] →
      {c : ℝ} →
        c ≠ 0 →
          ↑(s ∩ c⁻¹ • ↑(Submodule.span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))) ≃
            ↑(c • s ∩ ↑(Submodule.span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))
-- Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
AlgebraicGeometry.HasRingHomProperty.of_isZariskiLocalAtSource_of_isZariskiLocalAtTarget : ∀ (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsZariskiLocalAtTarget P]
  [AlgebraicGeometry.IsZariskiLocalAtSource P],
  AlgebraicGeometry.HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] f =>
    P (AlgebraicGeometry.Spec.map (CommRingCat.ofHom f))
-- Mathlib.Algebra.Homology.Bifunctor
HomologicalComplex.mapBifunctor.d₁_eq : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} D] {I₁ : Type u_4}
  {I₂ : Type u_5} {J : Type u_6} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂}
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C₁] [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C₂]
  [inst_5 : CategoryTheory.Preadditive D] (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂)
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [inst_6 : F.PreservesZeroMorphisms]
  [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (c : ComplexShape J) [inst_8 : TotalComplexShape c₁ c₂ c]
  [inst_9 : K₁.HasMapBifunctor K₂ F c] [inst_10 : DecidableEq J] {i₁ i₁' : I₁},
  c₁.Rel i₁ i₁' →
    ∀ (i₂ : I₂) (j : J) (h' : c₁.π c₂ c (i₁', i₂) = j),
      HomologicalComplex.mapBifunctor.d₁ K₁ K₂ F c i₁ i₂ j =
        c₁.ε₁ c₂ c (i₁, i₂) •
          CategoryTheory.CategoryStruct.comp ((F.map (K₁.d i₁ i₁')).app (K₂.X i₂)) (K₁.ιMapBifunctor K₂ F c i₁' i₂ j h')
-- Mathlib.Condensed.Light.TopCatAdjunction
lightCondSetToTopCat_map : ∀ {X Y : LightCondSet} (f : X ⟶ Y), lightCondSetToTopCat.map f = LightCondSet.toTopCatMap f
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2to1.step_run : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} [inst : DecidableEq K] {k : K}
  (q : Turing.TM2.Stmt Γ Λ σ) (v : σ) (S : (k : K) → List (Γ k)) (s : Turing.TM2to1.StAct K Γ σ k),
  Turing.TM2.stepAux (Turing.TM2to1.stRun s q) v S =
    Turing.TM2.stepAux q (Turing.TM2to1.stVar v (S k) s) (Function.update S k (Turing.TM2to1.stWrite v (S k) s))
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
lt_add_of_pos_of_lt : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α] [AddRightStrictMono α] {a b c : α},
  0 < a → b < c → b < a + c
-- Mathlib.RingTheory.HahnSeries.Lex
/-- The correspondence between finite archimedean classes of `Lex R⟦Γ⟧`
and lexicographical pairs of `HahnSeries.orderTop` and the finite archimedean class of
`HahnSeries.leadingCoeff`.  -/
HahnSeries.finiteArchimedeanClassOrderIsoLex : (Γ : Type u_1) →
  (R : Type u_2) →
    [inst : LinearOrder Γ] →
      [inst_1 : LinearOrder R] →
        [inst_2 : AddCommGroup R] →
          [inst_3 : IsOrderedAddMonoid R] →
            FiniteArchimedeanClass (Lex (HahnSeries Γ R)) ≃o Lex (Γ × FiniteArchimedeanClass R)
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Matrix.mul_inv_cancel_left_of_invertible : ∀ {m : Type u} {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α]
  (A : Matrix n n α) (B : Matrix n m α) [Invertible A], A * (A⁻¹ * B) = B
-- Mathlib.LinearAlgebra.Matrix.Nonsingular
Matrix.Nonsingular.mul : ∀ {R : Type u_1} {n : Type u_3} [inst : CommSemiring R] [inst_1 : Fintype n] [inst_2 : DecidableEq n] {A : Matrix n n R}
  [IsCancelAdd R] {B : Matrix n n R}, A.Nonsingular → B.Nonsingular → (A * B).Nonsingular
-- Mathlib.Algebra.Algebra.Tower
Submodule.map_mem_span_algebraMap_image : ∀ {R : Type u} [inst : CommSemiring R] {S : Type u_1} {T : Type u_2} [inst_1 : CommSemiring S] [inst_2 : Semiring T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [IsScalarTower R S T] (x : S) (a : Set S),
  x ∈ Submodule.span R a → (algebraMap S T) x ∈ Submodule.span R (⇑(algebraMap S T) '' a)
-- Lean.Elab.InfoTree.InlayHints
Lean.Elab.InlayHint.mk : Lean.Elab.InlayHintInfo →
  Lean.LocalContext → (Lean.Elab.InlayHintInfo → Lean.MetaM Lean.Elab.InlayHintInfo) → Lean.Elab.InlayHint
-- Init.Data.BitVec.Lemmas
BitVec.xor_append : ∀ {w v : ℕ} {x₁ x₂ : BitVec w} {y₁ y₂ : BitVec v}, x₁ ++ y₁ ^^^ x₂ ++ y₂ = (x₁ ^^^ x₂) ++ (y₁ ^^^ y₂)
-- Mathlib.Topology.Filter
Filter.nhds_nhds : ∀ {X : Type u_4} [inst : TopologicalSpace X] (x : X),
  nhds (nhds x) = ⨅ s, ⨅ (_ : IsOpen s), ⨅ (_ : x ∈ s), Filter.principal (Set.Iic (Filter.principal s))
-- Init.Data.SInt.Lemmas
ISize.add_eq_left : ∀ {a b : ISize}, a + b = a ↔ b = 0
-- Mathlib.Order.SuccPred.Basic
/-- **Alias** of the reverse direction of `Order.succ_ne_succ_iff`. -/
Order.succ_ne_succ : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : SuccOrder α] {a b : α} [NoMaxOrder α],
  a ≠ b → Order.succ a ≠ Order.succ b
-- Mathlib.CategoryTheory.Quotient
CategoryTheory.Quotient.mk.inj : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {r : HomRel C} {as as_1 : C},
  { as := as } = { as := as_1 } → as = as_1
-- Mathlib.Order.ConditionallyCompleteLattice.Finset
Finset.sup'_univ_eq_ciSup : ∀ {ι : Type u_1} {α : Type u_2} [inst : ConditionallyCompleteLattice α] [inst_1 : Fintype ι] [inst_2 : Nonempty ι]
  (f : ι → α), Finset.univ.sup' ⋯ f = ⨆ i, f i
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Ideal.prime_span_singleton_iff : ∀ {A : Type u_2} [inst : CommRing A] [IsDedekindDomain A] {a : A}, Prime (Ideal.span {a}) ↔ Prime a
-- Std.Http.Data.Chunk
Std.Http.Chunk.instBEqExtensionName.beq : Std.Http.Chunk.ExtensionName → Std.Http.Chunk.ExtensionName → Bool
-- Mathlib.Algebra.Group.Center
Set.subset_addCentralizer_addCentralizer : ∀ {M : Type u_1} {S : Set M} [inst : Add M], S ⊆ S.addCentralizer.addCentralizer
-- Init.Data.List.Lex
List.instTotalLeOfAsymmLt : ∀ {α : Type u_1} [inst : LT α] [Std.Asymm fun x1 x2 => x1 < x2], Std.Total fun x1 x2 => x1 ≤ x2
-- Lean.Elab.PreDefinition.WF.GuessLex
_private.Lean.Elab.PreDefinition.WF.GuessLex.0.Lean.Elab.WF.GuessLex.generateCombinations?.go : Array ℕ → ℕ → ℕ → OptionT (ReaderT (Array ℕ) (StateM (Array (Array ℕ)))) Unit