mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.Widget.LibraryRewrite
/-- Construct the `RewriteInterface` from a `Rewrite`.  -/
Mathlib.Tactic.LibraryRewrite.Rewrite.toInterface : Mathlib.Tactic.LibraryRewrite.Rewrite →
  Lean.Name ⊕ Lean.FVarId →
    Option ℕ → Option Lean.Name → Lean.Lsp.Range → Lean.MetaM Mathlib.Tactic.LibraryRewrite.RewriteInterface
-- Mathlib.NumberTheory.MulChar.Basic
/-- Turn a homomorphism between unit groups into a `MulChar`.  -/
MulChar.ofUnitHom : {R : Type u_1} → [inst : CommMonoid R] → {R' : Type u_2} → [inst_1 : CommMonoidWithZero R'] → (Rˣ →* R'ˣ) → MulChar R R'
-- Mathlib.Topology.Order.LeftRightLim
leftLim_eq_of_not_tendsto : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace β] [hα : TopologicalSpace α]
  [h'α : OrderTopology α] (f : α → β) {a : α},
  (¬∃ y, Filter.Tendsto f (nhdsWithin a (Set.Iio a)) (nhds y)) → Function.leftLim f a = f a
-- Std.Time.Zoned.TimeZone
Std.Time.TimeZone.instTransOrdOffset : Std.TransOrd Std.Time.TimeZone.Offset
-- Mathlib.Topology.ClusterPt
accPt_sup : ∀ {X : Type u} [inst : TopologicalSpace X] {x : X} {F G : Filter X}, AccPt x (F ⊔ G) ↔ AccPt x F ∨ AccPt x G
-- Mathlib.CategoryTheory.Abelian.LeftDerived
CategoryTheory.ProjectiveResolution.isoLeftDerivedToHomotopyCategoryObj_hom_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.HasProjectiveResolutions C]
  [inst_4 : CategoryTheory.Abelian D] {X Y : C} (f : X ⟶ Y) (P : CategoryTheory.ProjectiveResolution X)
  (Q : CategoryTheory.ProjectiveResolution Y) (φ : P.complex ⟶ Q.complex),
  CategoryTheory.CategoryStruct.comp (φ.f 0) (Q.π.f 0) = CategoryTheory.CategoryStruct.comp (P.π.f 0) f →
    ∀ (F : CategoryTheory.Functor C D) [inst_5 : F.Additive],
      CategoryTheory.CategoryStruct.comp (F.leftDerivedToHomotopyCategory.map f)
          (Q.isoLeftDerivedToHomotopyCategoryObj F).hom =
        CategoryTheory.CategoryStruct.comp (P.isoLeftDerivedToHomotopyCategoryObj F).hom
          (((F.mapHomologicalComplex (ComplexShape.down ℕ)).comp
                (HomotopyCategory.quotient D (ComplexShape.down ℕ))).map
            φ)
-- Init.Data.UInt.Lemmas
UInt64.toNat.inj : ∀ {a b : UInt64}, a.toNat = b.toNat → a = b
-- Mathlib.Algebra.Group.Subsemigroup.Operations
/-- The preimage of an `AddSubsemigroup` along an `AddSemigroup` homomorphism is an
`AddSubsemigroup`.  -/
AddSubsemigroup.comap : {M : Type u_1} → {N : Type u_2} → [inst : Add M] → [inst_1 : Add N] → (M →ₙ+ N) → AddSubsemigroup N → AddSubsemigroup M
-- Mathlib.GroupTheory.GroupExtension.Defs
GroupExtension.Equiv.Simps.symm_apply.eq_1 : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : Group N] [inst_1 : Group E] [inst_2 : Group G]
  {S : GroupExtension N E G} {E' : Type u_4} [inst_3 : Group E'] {S' : GroupExtension N E' G} (equiv : S.Equiv S'),
  GroupExtension.Equiv.Simps.symm_apply equiv = ⇑equiv.symm
-- Lean.Server.FileWorker.SignatureHelp
Lean.Server.FileWorker.SignatureHelp.SearchControl.noConfusionType : Sort v✝ →
  Lean.Server.FileWorker.SignatureHelp.SearchControl → Lean.Server.FileWorker.SignatureHelp.SearchControl → Sort v✝
-- Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
WeierstrassCurve.integralModel_a₆_eq : ∀ (R : Type u_1) [inst : CommRing R] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra R K] (W : WeierstrassCurve K)
  [hW : WeierstrassCurve.IsIntegral R W], (algebraMap R K) (WeierstrassCurve.integralModel R W).a₆ = W.a₆
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
/-- The isomorphism `D₊(f) ×[Proj 𝒜] D₊(g) ≅ D₊(fg)`.  -/
AlgebraicGeometry.Proj.pullbackAwayιIso : {σ : Type u_1} →
  {A : Type u} →
    [inst : CommRing A] →
      [inst_1 : SetLike σ A] →
        [inst_2 : AddSubgroupClass σ A] →
          (𝒜 : ℕ → σ) →
            [inst_3 : GradedRing 𝒜] →
              {f : A} →
                {m : ℕ} →
                  (f_deg : f ∈ 𝒜 m) →
                    (hm : 0 < m) →
                      {m' : ℕ} →
                        {g : A} →
                          (g_deg : g ∈ 𝒜 m') →
                            (hm' : 0 < m') →
                              {x : A} →
                                x = f * g →
                                  (CategoryTheory.Limits.pullback (AlgebraicGeometry.Proj.awayι 𝒜 f f_deg hm)
                                      (AlgebraicGeometry.Proj.awayι 𝒜 g g_deg hm') ≅
                                    AlgebraicGeometry.Spec (CommRingCat.of (HomogeneousLocalization.Away 𝒜 x)))
-- Mathlib.Algebra.Ring.Subring.Basic
RingHom.eqLocus_same : ∀ {R : Type u} [inst : NonAssocRing R] {S : Type v} [inst_1 : Semiring S] (f : R →+* S), f.eqLocus f = ⊤
-- Mathlib.Topology.Homotopy.HSpaces
IsTopologicalGroup.toHSpace.eq_1 : ∀ (M : Type u) [inst : MulOneClass M] [inst_1 : TopologicalSpace M] [inst_2 : ContinuousMul M],
  IsTopologicalGroup.toHSpace M =
    { hmul := { toFun := Function.uncurry Mul.mul, continuous_toFun := ⋯ }, e := 1, hmul_e_e := ⋯,
      eHmul :=
        (ContinuousMap.HomotopyRel.refl
              ({ toFun := Function.uncurry Mul.mul, continuous_toFun := ⋯ }.comp
                ((ContinuousMap.const M 1).prodMk (ContinuousMap.id M)))
              {1}).cast
          ⋯ ⋯,
      hmulE :=
        (ContinuousMap.HomotopyRel.refl
              ({ toFun := Function.uncurry Mul.mul, continuous_toFun := ⋯ }.comp
                ((ContinuousMap.id M).prodMk (ContinuousMap.const M 1)))
              {1}).cast
          ⋯ ⋯ }
-- Mathlib.Combinatorics.Pigeonhole
/-- The strong pigeonhole principle for finitely many pigeons and pigeonholes.
There is a pigeonhole with at most as many pigeons as
the floor of the average number of pigeons across all pigeonholes.
("The minimum is at most the mean" specialized to integers.)

More formally, given a function `f` between finite types `α` and `β` and a number `n` such that
`card α < card β * n`, there exists an element `y : β` such that its preimage has less than `n`
elements.  -/
Fintype.exists_card_fiber_lt_of_card_lt_mul : ∀ {α : Type u} {β : Type v} [inst : DecidableEq β] [inst_1 : Fintype α] [inst_2 : Fintype β] (f : α → β) {n : ℕ},
  Fintype.card α < Fintype.card β * n → ∃ y, {x | f x = y}.card < n
-- Mathlib.CategoryTheory.Limits.Types.Multiequalizer
/-- The bijection `I.sections ≃ c.pt` when `c : Multifork I` is a limit multifork
in the category of types.  -/
CategoryTheory.Limits.Multifork.IsLimit.sectionsEquiv : {J : CategoryTheory.Limits.MulticospanShape} →
  {I : CategoryTheory.Limits.MulticospanIndex J (Type u)} →
    {c : CategoryTheory.Limits.Multifork I} → CategoryTheory.Limits.IsLimit c → I.sections ≃ c.pt
-- Mathlib.FieldTheory.Minpoly.Basic
/-- Suppose `x : B`, where `B` is an `A`-algebra.

The minimal polynomial `minpoly A x` of `x`
is a monic polynomial with coefficients in `A` of smallest degree that has `x` as its root,
if such exists (`IsIntegral A x`) or zero otherwise.

For example, if `V` is a `𝕜`-vector space for some field `𝕜` and `f : V →ₗ[𝕜] V` then
the minimal polynomial of `f` is `minpoly 𝕜 f`.
 -/
minpoly : (A : Type u_1) → {B : Type u_2} → [inst : CommRing A] → [inst_1 : Ring B] → [Algebra A B] → B → Polynomial A
-- Mathlib.Analysis.SpecialFunctions.ExpDeriv
AnalyticOn.cexp : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : E → ℂ} {s : Set E},
  AnalyticOn ℂ f s → AnalyticOn ℂ (fun z => Complex.exp (f z)) s
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.size_add_size_eq_size_union_add_size_inter : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → t₁.size + t₂.size = (t₁ ∪ t₂).size + (t₁ ∩ t₂).size
-- Mathlib.Algebra.Order.ToIntervalMod
toIocMod_intCast_mul_add' : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedAddMonoid R]
  [inst_3 : Archimedean R] {p : R} (hp : 0 < p) (a b : R) (m : ℤ), toIocMod hp (↑m * p + a) b = ↑m * p + toIocMod hp a b
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.stdSimplex.ofSimplex_yonedaEquiv_δ : ∀ {n : ℕ} (i : Fin (n + 2)),
  SSet.Subcomplex.ofSimplex (SSet.yonedaEquiv (SSet.stdSimplex.δ i)) = SSet.stdSimplex.face {i}ᶜ
-- Mathlib.MeasureTheory.Measure.MutuallySingular
MeasureTheory.Measure.MutuallySingular.disjoint_ae : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α},
  μ.MutuallySingular ν → Disjoint (MeasureTheory.ae μ) (MeasureTheory.ae ν)
-- Mathlib.Analysis.Meromorphic.Basic
/-- Eta-expanded form of `MeromorphicOn.smul` -/
MeromorphicOn.fun_smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {R : Type u_4} [inst_3 : NormedRing R] [inst_4 : Module R E] [IsBoundedSMul R E]
  {U : Set 𝕜} [inst_6 : NormedAlgebra 𝕜 R] [IsScalarTower 𝕜 R E] {s : 𝕜 → R},
  MeromorphicOn s U → ∀ {f : 𝕜 → E}, MeromorphicOn f U → MeromorphicOn (fun i => s i • f i) U
-- Mathlib.Algebra.Group.Units.Defs
Units.instGroup.eq_1 : ∀ {α : Type u} [inst : Monoid α], Units.instGroup = { toDivInvMonoid := Units.instDivInvMonoid, inv_mul_cancel := ⋯ }
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.Iter.forIn_mapM : ∀ {α β β₂ γ : Type w} [inst : Std.Iterator α Id β] {ps : Std.Do.PostShape} {n : Type w → Type u_1}
  {o : Type w → Type u_2} [inst_1 : Monad n] [LawfulMonad n] [inst_3 : Monad o] [LawfulMonad o]
  [inst_5 : Std.Do.WPMonad o ps] [inst_6 : MonadAttach n] [WeaklyLawfulMonadAttach n] [inst_8 : MonadLiftT n o]
  [LawfulMonadLiftT n o] [Std.Iterators.Finite α Id] [inst_11 : Std.IteratorLoop α Id o] [Std.LawfulIteratorLoop α Id o]
  {it : Std.Iter β} {f : β → n β₂} {init : γ} {g : β₂ → γ → o (ForInStep γ)} {P : Std.Do.Assertion ps}
  {Q : Std.Do.PostCond γ ps},
  ⦃P⦄
      forIn it init fun out acc => do
        let __do_lift ← liftM (f out)
        g __do_lift acc ⦃Q⦄ →
    ⦃P⦄ forIn (Std.Iter.mapM f it) init g ⦃Q⦄
-- Std.Data.HashMap.Basic
/-- Inserts multiple keys with the value `()` into the hash map by iterating over the given collection
and calling `insertIfNew`. If the same key appears multiple times, the first occurrence takes
precedence.

This is mainly useful to implement `HashSet.insertMany`, so if you are considering using this,
`HashSet` or `HashSet.Raw` might be a better fit for you.
 -/
Std.HashMap.insertManyIfNewUnit : {α : Type u} →
  {x : BEq α} → {x_1 : Hashable α} → {ρ : Type w} → [ForIn Id ρ α] → Std.HashMap α Unit → ρ → Std.HashMap α Unit
-- Mathlib.Algebra.Group.TypeTags.Basic
/-- Reinterpret `x : Additive α` as an element of `α`.  -/
Additive.toMul : {α : Type u} → Additive α ≃ α
-- Init.Data.Range.Polymorphic.BitVec
BitVec.instRxiHasSize : {n : ℕ} → Std.Rxi.HasSize (BitVec n)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKeyD_eq_getD_getKey? : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {a fallback : α}, m.getKeyD a fallback = (m.getKey? a).getD fallback
-- Lean.Util.CollectAxioms
/-- Environment extension that records axiom dependencies for all declarations in a module.
Entries are computed once by `beforeExportFn` when the olean is serialized, not during
elaboration. During elaboration, `collectAxioms` walks bodies directly. Downstream modules
look up pre-computed entries for imported declarations, so axiom collection never crosses
module boundaries.
 -/
_private.Lean.Util.CollectAxioms.0.Lean.exportedAxiomsExt : Lean.PersistentEnvExtension (Lean.Name × Array Lean.Name) (Lean.Name × Array Lean.Name) Lean.ExportedAxiomsState✝
-- Lean.Data.DeclarationRange
Lean.instInhabitedDeclarationRange.default : Lean.DeclarationRange
-- Mathlib.Topology.UniformSpace.UniformEmbedding
isUniformEmbedding_subtypeEmb : ∀ {α : Type u} {β : Type v} [inst : UniformSpace α] [inst_1 : UniformSpace β] (p : α → Prop) {e : α → β},
  IsUniformEmbedding e → IsDenseEmbedding e → IsUniformEmbedding (IsDenseEmbedding.subtypeEmb p e)
-- Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory
CategoryTheory.ShortComplex.ShortExact.surjective_g : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC]
  [inst_3 : CategoryTheory.HasForget₂ C Ab] [inst_4 : CategoryTheory.Preadditive C]
  [inst_5 : (CategoryTheory.forget₂ C Ab).Additive] [(CategoryTheory.forget₂ C Ab).PreservesHomology]
  {S : CategoryTheory.ShortComplex C} [CategoryTheory.Limits.HasZeroObject C],
  S.ShortExact → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget₂ C Ab).map S.g))
-- Lean.Structure
Lean.StructureDescr.mk : Lean.Name → Array Lean.StructureFieldInfo → Lean.StructureDescr
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.mk_set_le : ∀ {α : Type u} (s : Set α), Cardinal.mk ↑s ≤ Cardinal.mk α
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Pi
cfcₙ_map_prod : ∀ {A : Type u_1} {B : Type u_2} {R : Type u_3} {S : Type u_4} [inst : CommSemiring R] [inst_1 : CommRing S]
  [inst_2 : Nontrivial R] [inst_3 : StarRing R] [inst_4 : MetricSpace R] [inst_5 : IsTopologicalSemiring R]
  [inst_6 : ContinuousStar R] [inst_7 : Algebra R S] [inst_8 : NonUnitalRing A] [inst_9 : NonUnitalRing B]
  [inst_10 : Module S A] [inst_11 : Module R A] [inst_12 : Module R B] [inst_13 : Module S B]
  [inst_14 : SMulCommClass R A A] [inst_15 : SMulCommClass R B B] [inst_16 : IsScalarTower R A A]
  [inst_17 : IsScalarTower R B B] [inst_18 : StarRing A] [inst_19 : StarRing B] [inst_20 : TopologicalSpace A]
  [inst_21 : TopologicalSpace B] [IsScalarTower R S A] [IsScalarTower R S B] {pab : A × B → Prop} {pa : A → Prop}
  {pb : B → Prop} [inst_24 : NonUnitalContinuousFunctionalCalculus R (A × B) pab]
  [inst_25 : NonUnitalContinuousFunctionalCalculus R A pa] [inst_26 : NonUnitalContinuousFunctionalCalculus R B pb]
  [ContinuousMapZero.UniqueHom R A] [ContinuousMapZero.UniqueHom R B] (f : R → R) (a : A) (b : B),
  autoParam (ContinuousOn f (quasispectrum R a ∪ quasispectrum R b)) cfcₙ_map_prod._auto_1 →
    autoParam (pab (a, b)) cfcₙ_map_prod._auto_3 →
      autoParam (pa a) cfcₙ_map_prod._auto_5 →
        autoParam (pb b) cfcₙ_map_prod._auto_7 → cfcₙ f (a, b) = (cfcₙ f a, cfcₙ f b)
-- Init.Data.BitVec.Lemmas
BitVec.zero_sshiftRight : ∀ {w n : ℕ}, (0#w).sshiftRight n = 0#w
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.support_suffix_support_cons : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} (p : G.Walk v w) (hadj : G.Adj u v),
  p.support <:+ (SimpleGraph.Walk.cons hadj p).support
-- Mathlib.Algebra.Group.Units.Hom
/-- If `f` is a homomorphism from an additive group `G` to an additive monoid `M`,
then its image lies in the `AddUnits` of `M`,
and `f.toHomUnits` is the corresponding homomorphism from `G` to `AddUnits M`.  -/
AddMonoidHom.toHomAddUnits : {G : Type u_1} → {M : Type u_2} → [inst : AddGroup G] → [inst_1 : AddMonoid M] → (G →+ M) → G →+ AddUnits M
-- Lean.Parser.Syntax
/-- `prefix:prec "op" => f` is equivalent to `notation:prec "op" x:prec => f x`.
 -/
Lean.Parser.Command.prefix : Lean.Parser.Parser
-- Mathlib.Algebra.Homology.QuasiIso
quasiIso_of_comp_right : ∀ {ι : Type u_1} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K L M : HomologicalComplex C c} (φ : K ⟶ L)
  (φ' : L ⟶ M) [inst_2 : ∀ (i : ι), K.HasHomology i] [inst_3 : ∀ (i : ι), L.HasHomology i]
  [inst_4 : ∀ (i : ι), M.HasHomology i] [hφ : QuasiIso φ'] [hφφ' : QuasiIso (CategoryTheory.CategoryStruct.comp φ φ')],
  QuasiIso φ
-- Mathlib.CategoryTheory.Monoidal.Action.Opposites
CategoryTheory.MonoidalCategory.MonoidalRightAction.rightActionOfOppositeRightAction_actionHomLeft_unop : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction Cᵒᵖ Dᵒᵖ] {d d' : Dᵒᵖ} (f : d ⟶ d') (c : Cᵒᵖ),
  CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft f.unop (Opposite.unop c) =
    Opposite.unop (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft f c)
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1.stepAux.eq_1 : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} [inst : Inhabited Γ] (x : σ) (x_1 : Turing.Tape Γ) (d : Turing.Dir)
  (q : Turing.TM1.Stmt Γ Λ σ),
  Turing.TM1.stepAux (Turing.TM1.Stmt.move d q) x x_1 = Turing.TM1.stepAux q x (Turing.Tape.move d x_1)
-- Mathlib.LinearAlgebra.TensorProduct.Pi
TensorProduct.piRight_apply : ∀ (R : Type u_1) [inst : CommSemiring R] (S : Type u_2) [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (N : Type u_3)
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] [inst_5 : Module S N] [inst_6 : IsScalarTower R S N] {ι : Type u_4}
  (M : ι → Type u_5) [inst_7 : (i : ι) → AddCommMonoid (M i)] [inst_8 : (i : ι) → Module R (M i)] [inst_9 : Fintype ι]
  [inst_10 : DecidableEq ι] (x : TensorProduct R N ((i : ι) → M i)),
  (TensorProduct.piRight R S N M) x = (TensorProduct.piRightHom R S N M) x
-- Lean.ReducibilityAttrs
_private.Lean.ReducibilityAttrs.0.Lean.setReducibilityStatusCore : Lean.Environment → Lean.Name → Lean.ReducibilityStatus → Lean.AttributeKind → Lean.Name → Lean.Environment
-- Init.Data.ByteArray.Basic
/-- Decreases the iterator's position.

If the position is zero, this function is the identity.
 -/
ByteArray.Iterator.prev : ByteArray.Iterator → ByteArray.Iterator
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.Compacts.instTopOfCompactSpace : {α : Type u_1} → [inst : TopologicalSpace α] → [CompactSpace α] → Top (TopologicalSpace.Compacts α)
-- Mathlib.Analysis.Normed.Ring.WithAbs
WithAbs.algebraMap_right_apply : ∀ {S : Type u_2} [inst : Semiring S] [inst_1 : PartialOrder S] {R : Type u_3} {T : Type u_4} [inst_2 : CommSemiring R]
  [inst_3 : Semiring T] [inst_4 : Algebra R T] {v : AbsoluteValue T S} (x : R),
  (algebraMap R (WithAbs v)) x = WithAbs.toAbs v ((algebraMap R T) x)
-- Mathlib.MeasureTheory.Measure.Restrict
volume_preimage_coe : ∀ {α : Type u_2} [inst : MeasureTheory.MeasureSpace α] {s t : Set α},
  MeasureTheory.NullMeasurableSet s MeasureTheory.volume →
    MeasurableSet t → MeasureTheory.volume (Subtype.val ⁻¹' t) = MeasureTheory.volume (t ∩ s)
-- Mathlib.Analysis.Complex.AbsMax
/-- **Maximum modulus principle**: if `f : E → F` is complex differentiable on a nonempty bounded
set `U` and is continuous on its closure, then there exists a point `z ∈ frontier U` such that
`(‖f ·‖)` takes it maximum value on `closure U` at `z`.  -/
Complex.exists_mem_frontier_isMaxOn_norm : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {F : Type v} [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℂ F] [Nontrivial E] [FiniteDimensional ℂ E] {f : E → F} {U : Set E},
  Bornology.IsBounded U → U.Nonempty → DiffContOnCl ℂ f U → ∃ z ∈ frontier U, IsMaxOn (norm ∘ f) (closure U) z
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
/-- Integrand for representing `x ↦ x^p` for `p ∈ (1,2)`  -/
Real.rpowIntegrand₁₂ : ℝ → ℝ → ℝ → ℝ
-- Mathlib.AlgebraicTopology.Quasicategory.InnerFibration
/-- **Alias** of `SSet.quasicategory_iff_innerFibration`. -/
SSet.quasicategory_iff_from_innerFibration : ∀ (X : SSet), X.Quasicategory ↔ SSet.InnerFibration (CategoryTheory.Limits.terminal.from X)
-- Mathlib.RingTheory.MvPowerSeries.Rename
_private.Mathlib.RingTheory.MvPowerSeries.Rename.0.MvPowerSeries.renameFun_mul : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} (f : σ → τ) [inst : Filter.TendstoCofinite f] [inst_1 : Semiring R]
  (p q : MvPowerSeries σ R),
  MvPowerSeries.renameFun f (p * q) = MvPowerSeries.renameFun f p * MvPowerSeries.renameFun f q
-- Mathlib.NumberTheory.LSeries.HurwitzZeta
HurwitzZeta.hurwitzZetaEven_eq : ∀ (a : UnitAddCircle) (s : ℂ),
  HurwitzZeta.hurwitzZetaEven a s = (HurwitzZeta.hurwitzZeta a s + HurwitzZeta.hurwitzZeta (-a) s) / 2
-- Lean.Elab.Command
Lean.Elab.Command.State.env : Lean.Elab.Command.State → Lean.Environment
-- Mathlib.NumberTheory.Dioph
Poly.instAddCommGroup : {α : Type u_1} → AddCommGroup (Poly α)
-- Mathlib.Topology.Order.DenselyOrdered
nhdsWithin_Ioi_neBot : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [DenselyOrdered α]
  [NoMaxOrder α] {a b : α}, a ≤ b → (nhdsWithin b (Set.Ioi a)).NeBot
-- Mathlib.NumberTheory.MahlerMeasure
/-- **Northcott's Theorem:** the set of integer polynomials of degree at most `n` and
Mahler measure at most `B` is finite.  -/
Polynomial.finite_mahlerMeasure_le : ∀ (n : ℕ) (B : NNReal), {p | p.natDegree ≤ n ∧ (Polynomial.map (Int.castRingHom ℂ) p).mahlerMeasure ≤ ↑B}.Finite
-- Mathlib.Data.Finmap
List.toFinmap.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (s : List (Sigma β)), s.toFinmap = s.toAList.toFinmap
-- Init.Data.List.Range
List.range'_eq_cons_iff : ∀ {s n step a : ℕ} {xs : List ℕ},
  List.range' s n step = a :: xs ↔ s = a ∧ 0 < n ∧ xs = List.range' (a + step) (n - 1) step
-- Batteries.Data.UnionFind.Basic
Batteries.UnionFind.FindAux.mk.injEq : ∀ {n : ℕ} (s : Array Batteries.UFNode) (root : Fin n) (size_eq : s.size = n) (s_1 : Array Batteries.UFNode)
  (root_1 : Fin n) (size_eq_1 : s_1.size = n),
  ({ s := s, root := root, size_eq := size_eq } = { s := s_1, root := root_1, size_eq := size_eq_1 }) =
    (s = s_1 ∧ root = root_1)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey?_inter_of_not_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  k ∉ t₂ → (t₁ ∩ t₂).getKey? k = none
-- Init.Data.Range.Polymorphic.UpwardEnumerable
/-- Maps elements of `α` to their successor, or none if no successor exists.  -/
Std.PRange.UpwardEnumerable.succ? : {α : Type u} → [self : Std.PRange.UpwardEnumerable α] → α → Option α
-- Mathlib.RingTheory.Extension.Basic
Algebra.Extension.toBaseChange_toRingHom : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {P : Algebra.Extension R S}
  (T : Type u_1) [inst_3 : CommRing T] [inst_4 : Algebra R T],
  (Algebra.Extension.toBaseChange T).toRingHom = Algebra.TensorProduct.includeRight.toRingHom
-- Lean.Parser.Extra
/-- No-op parser combinator that advises the pretty printer to indent the given syntax without grouping it.  -/
Lean.Parser.ppIndent : Lean.Parser.Parser → Lean.Parser.Parser
-- Mathlib.CategoryTheory.Monoidal.Free.Coherence
/-- Auxiliary definition for `normalize`. Here we prove that objects that are related by
associators and unitors map to the same normal form.  -/
CategoryTheory.FreeMonoidalCategory.normalizeMapAux : {C : Type u} → {X Y : CategoryTheory.FreeMonoidalCategory C} → X.Hom Y → (X.normalizeObj' ⟶ Y.normalizeObj')
-- Mathlib.Data.Finset.Max
Finset.le_max_of_eq : ∀ {α : Type u_2} [inst : LinearOrder α] {s : Finset α} {a b : α}, a ∈ s → s.max = ↑b → a ≤ b
-- Mathlib.Algebra.Homology.Embedding.ExtendHomology
HomologicalComplex.extend.homologyData'_iso : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c) (e : c.Embedding c') {i j k : ι}
  {j' : ι'} (hj' : e.f j = j') (hi : c.prev j = i) (hk : c.next j = k) (h : (K.sc' i j k).HomologyData),
  (HomologicalComplex.extend.homologyData' K e hj' hi hk h).iso = h.iso