mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Nat.MaxPowDiv
/-- **Alias** of `padicValNat_base_mul`. -/
Nat.maxPowDiv.base_mul_eq_succ : ∀ {p n : ℕ}, 1 < p → n ≠ 0 → padicValNat p (p * n) = padicValNat p n + 1
-- Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
ENNReal.log_monotone : Monotone ENNReal.log
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.Relations.isUniversal_transitive : ∀ {L : FirstOrder.Language} (r : L.Relations 2), FirstOrder.Language.BoundedFormula.IsUniversal r.transitive
-- Lean.Elab.Match
/-- Constructs a "redundant alternative" error message.

Optionally accepts the name of the constructor (e.g., for use in the `induction` tactic) and/or the
message-data representation of the alternative in question.
 -/
Lean.Elab.Term.mkRedundantAlternativeMsg : Option Lean.Name → Option Lean.MessageData → Lean.MessageData
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.lt_of_matchAt?_eq_some : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [String.Slice.Pattern.Model.StrictPatternModel pat] {s : String.Slice} {startPos endPos : s.Pos},
  String.Slice.Pattern.Model.matchAt? pat startPos = some endPos → startPos < endPos
-- Mathlib.Algebra.Order.Ring.Defs
instOrderedRingOfIsStrictOrderedRing : ∀ {R : Type u} [inst : Semiring R] [inst_1 : PartialOrder R] [IsStrictOrderedRing R], Lean.Grind.OrderedRing R
-- Lean.Parser.Types
Lean.Parser.leadPrec : ℕ
-- Mathlib.Topology.UniformSpace.Separation
SeparationQuotient.map_mk : ∀ {α : Type u} {β : Type v} [inst : UniformSpace α] [inst_1 : UniformSpace β] {f : α → β},
  UniformContinuous f → ∀ (a : α), SeparationQuotient.map f (SeparationQuotient.mk a) = SeparationQuotient.mk (f a)
-- Std.Data.DTreeMap.Raw.WF
Std.DTreeMap.Raw.WF.empty : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering}, Std.DTreeMap.Raw.empty.WF
-- Mathlib.Computability.RegularExpressions
RegularExpression.deriv.eq_6 : ∀ {α : Type u_1} [inst : DecidableEq α] (x : α) (P : RegularExpression α), P.star.deriv x = P.deriv x * P.star
-- Mathlib.Topology.Homotopy.HomotopyGroup
GenLoop.coe_copy : ∀ {N : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {x : X} (f : ↑(GenLoop N X x)) {g : (N → ↑unitInterval) → X}
  (h : g = ⇑f), ⇑(GenLoop.copy f g h) = g
-- Mathlib.LinearAlgebra.TensorProduct.Subalgebra
Subalgebra.mulMap_range : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  (A B : Subalgebra R S), (A.mulMap B).range = A ⊔ B
-- Mathlib.Topology.Compactness.CountablyCompact
/-- A compact space is countably compact.  -/
instCompactSpaceCountablyCompactSpace : ∀ {X : Type u_4} [inst : TopologicalSpace X] [CompactSpace X], CountablyCompactSpace X
-- Mathlib.Tactic.CategoryTheory.MonoidalComp
CategoryTheory.MonoidalCoherence.assoc : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (X Y Z W : C) →
        [CategoryTheory.MonoidalCoherence
              (CategoryTheory.MonoidalCategoryStruct.tensorObj X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z))
              W] →
          CategoryTheory.MonoidalCoherence
            (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z) W
-- Mathlib.RepresentationTheory.FiniteIndex
Rep.indToCoindAux_mul_fst : ∀ {k : Type u} {G : Type v} [inst : CommRing k] [inst_1 : Group G] {S : Subgroup G}
  [inst_2 : DecidableRel ⇑(QuotientGroup.rightRel S)] {A : Rep.{w, u, v} k ↥S} (g₁ g₂ : G) (a : ↑A) (s : ↥S),
  (A.indToCoindAux (↑s * g₁)) ((A.ρ s) a) g₂ = (A.indToCoindAux g₁) a g₂
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.coe_lt_one : ∀ {α : Type u} [inst : One α] [inst_1 : LT α] {a : α}, ↑a < 1 ↔ a < 1
-- Mathlib.Data.Stream.Init
Stream'.mem_const : ∀ {α : Type u} (a : α), a ∈ Stream'.const a
-- Mathlib.LinearAlgebra.Finsupp.LinearCombination
/-- Interprets (l : α →₀ R) as a linear combination of the elements in the family (v : α → M) and
evaluates this linear combination.  -/
Finsupp.linearCombination : {α : Type u_1} →
  {M : Type u_2} →
    (R : Type u_5) →
      [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → (α → M) → (α →₀ R) →ₗ[R] M
-- Init.SimpLemmas
false_and : ∀ (p : Prop), (False ∧ p) = False
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getKey_modify_self : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp},
  t.WF →
    ∀ [Inhabited α] {k : α} {f : β → β} {hc : k ∈ Std.DTreeMap.Raw.Const.modify t k f},
      (Std.DTreeMap.Raw.Const.modify t k f).getKey k hc = k
-- Mathlib.Algebra.Homology.HomologicalComplex
CochainComplex.mkHom_f_0 : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  (P Q : CochainComplex V ℕ) (zero : P.X 0 ⟶ Q.X 0) (one : P.X 1 ⟶ Q.X 1)
  (one_zero_comm : CategoryTheory.CategoryStruct.comp zero (Q.d 0 1) = CategoryTheory.CategoryStruct.comp (P.d 0 1) one)
  (succ :
    (n : ℕ) →
      (p :
          (f : P.X n ⟶ Q.X n) ×'
            (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ×'
              CategoryTheory.CategoryStruct.comp f (Q.d n (n + 1)) =
                CategoryTheory.CategoryStruct.comp (P.d n (n + 1)) f') →
        (f'' : P.X (n + 2) ⟶ Q.X (n + 2)) ×'
          CategoryTheory.CategoryStruct.comp p.snd.fst (Q.d (n + 1) (n + 2)) =
            CategoryTheory.CategoryStruct.comp (P.d (n + 1) (n + 2)) f''),
  (P.mkHom Q zero one one_zero_comm succ).f 0 = zero
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonPrepareRenameParams.fromJson : Lean.Json → Except String Lean.Lsp.PrepareRenameParams
-- Mathlib.Algebra.Group.Units.Hom
IsUnit.liftRight_inv_mul : ∀ {M : Type u_3} {N : Type u_4} [inst : Monoid M] [inst_1 : Monoid N] (f : M →* N) (h : ∀ (x : M), IsUnit (f x))
  (x : M), ↑((IsUnit.liftRight f h) x)⁻¹ * f x = 1
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.eval₂_dvd : ∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] (f : R →+* S₁)
  (g : σ → S₁) {p q : MvPolynomial σ R}, p ∣ q → MvPolynomial.eval₂ f g p ∣ MvPolynomial.eval₂ f g q
-- Mathlib.Analysis.LocallyConvex.Polar
/-- The polar of a set closed under scalar multiplication as a submodule  -/
LinearMap.polarSubmodule : {𝕜 : Type u_1} →
  {E : Type u_2} →
    {F : Type u_3} →
      [inst : NontriviallyNormedField 𝕜] →
        [inst_1 : AddCommMonoid E] →
          [inst_2 : AddCommMonoid F] →
            [inst_3 : Module 𝕜 E] →
              [inst_4 : Module 𝕜 F] →
                (E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) → {S : Type u_4} → [inst_5 : SetLike S E] → [SMulMemClass S 𝕜 E] → S → Submodule 𝕜 F
-- Mathlib.RingTheory.GradedAlgebra.AlgHom
/-- Restrict the base ring to a "smaller" ring.  -/
GradedAlgHom.restrictScalars : {R : Type u_1} →
  {A : Type u_6} →
    {B : Type u_7} →
      {ι : Type u_10} →
        [inst : CommSemiring R] →
          [inst_1 : Semiring A] →
            [inst_2 : Semiring B] →
              [inst_3 : Algebra R A] →
                [inst_4 : Algebra R B] →
                  [inst_5 : DecidableEq ι] →
                    [inst_6 : AddMonoid ι] →
                      {𝒜 : ι → Submodule R A} →
                        {ℬ : ι → Submodule R B} →
                          [inst_7 : GradedAlgebra 𝒜] →
                            [inst_8 : GradedAlgebra ℬ] →
                              (R₀ : Type u_11) →
                                [inst_9 : CommSemiring R₀] →
                                  [inst_10 : Algebra R₀ R] →
                                    [inst_11 : Algebra R₀ A] →
                                      [inst_12 : Algebra R₀ B] →
                                        [inst_13 : IsScalarTower R₀ R A] →
                                          [inst_14 : IsScalarTower R₀ R B] →
                                            (𝒜 →ₐᵍ[R] ℬ) →
                                              (fun x => Submodule.restrictScalars R₀ (𝒜 x)) →ₐᵍ[R₀] fun x =>
                                                Submodule.restrictScalars R₀ (ℬ x)
-- Std.Time.Format.DateFormat
Std.Time.DateFormatSymbols.mk.sizeOf_spec : ∀ (monthLong monthShort monthNarrow : Vector String 12)
  (weekdayLong weekdayShort weekdayNarrow weekdayTwoLetter : Vector String 7)
  (eraShort eraLong eraNarrow : Vector String 2) (quarterShort quarterLong quarterNarrow : Vector String 4)
  (amShort pmShort amLong pmLong amNarrow pmNarrow : String)
  (dayPeriodShort dayPeriodLong dayPeriodNarrow : Std.Time.DayPeriodSymbols)
  (extendedDayPeriodShort extendedDayPeriodLong extendedDayPeriodNarrow : Vector String 6),
  sizeOf
      { monthLong := monthLong, monthShort := monthShort, monthNarrow := monthNarrow, weekdayLong := weekdayLong,
        weekdayShort := weekdayShort, weekdayNarrow := weekdayNarrow, weekdayTwoLetter := weekdayTwoLetter,
        eraShort := eraShort, eraLong := eraLong, eraNarrow := eraNarrow, quarterShort := quarterShort,
        quarterLong := quarterLong, quarterNarrow := quarterNarrow, amShort := amShort, pmShort := pmShort,
        amLong := amLong, pmLong := pmLong, amNarrow := amNarrow, pmNarrow := pmNarrow,
        dayPeriodShort := dayPeriodShort, dayPeriodLong := dayPeriodLong, dayPeriodNarrow := dayPeriodNarrow,
        extendedDayPeriodShort := extendedDayPeriodShort, extendedDayPeriodLong := extendedDayPeriodLong,
        extendedDayPeriodNarrow := extendedDayPeriodNarrow } =
    1 + sizeOf monthLong + sizeOf monthShort + sizeOf monthNarrow + sizeOf weekdayLong + sizeOf weekdayShort +
                                            sizeOf weekdayNarrow +
                                          sizeOf weekdayTwoLetter +
                                        sizeOf eraShort +
                                      sizeOf eraLong +
                                    sizeOf eraNarrow +
                                  sizeOf quarterShort +
                                sizeOf quarterLong +
                              sizeOf quarterNarrow +
                            sizeOf amShort +
                          sizeOf pmShort +
                        sizeOf amLong +
                      sizeOf pmLong +
                    sizeOf amNarrow +
                  sizeOf pmNarrow +
                sizeOf dayPeriodShort +
              sizeOf dayPeriodLong +
            sizeOf dayPeriodNarrow +
          sizeOf extendedDayPeriodShort +
        sizeOf extendedDayPeriodLong +
      sizeOf extendedDayPeriodNarrow
-- Lean.Elab.DeclModifiers
Lean.Elab.instBEqComputeKind : BEq Lean.Elab.ComputeKind
-- Mathlib.Order.Filter.Ultrafilter.Basic
/-- The `tendsto` relation can be checked on ultrafilters.  -/
Filter.tendsto_iff_ultrafilter : ∀ {α : Type u} {β : Type v} (f : α → β) (l₁ : Filter α) (l₂ : Filter β),
  Filter.Tendsto f l₁ l₂ ↔ ∀ (g : Ultrafilter α), ↑g ≤ l₁ → Filter.Tendsto f (↑g) l₂
-- Mathlib.Probability.Kernel.Composition.CompProd
ProbabilityTheory.Kernel.compProd_congr : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {κ : ProbabilityTheory.Kernel α β} {η η' : ProbabilityTheory.Kernel (α × β) γ}
  [ProbabilityTheory.IsSFiniteKernel η] [ProbabilityTheory.IsSFiniteKernel η'],
  (∀ (a : α), ∀ᵐ (b : β) ∂κ a, η (a, b) = η' (a, b)) → κ.compProd η = κ.compProd η'
-- Mathlib.Computability.Partrec
Nat.Partrec.some : Nat.Partrec Part.some
-- Mathlib.CategoryTheory.Localization.Triangulated
CategoryTheory.Triangulated.Localization.complete_distinguished_triangle_morphism : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D)
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : CategoryTheory.Limits.HasZeroObject C] [inst_5 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [inst_6 : CategoryTheory.Pretriangulated C] [inst_7 : CategoryTheory.HasShift D ℤ] [inst_8 : L.CommShift ℤ]
  (W : CategoryTheory.MorphismProperty C) [L.IsLocalization W] [W.HasLeftCalculusOfFractions]
  [W.IsCompatibleWithTriangulation] (T₁ T₂ : CategoryTheory.Pretriangulated.Triangle D),
  T₁ ∈ L.essImageDistTriang →
    T₂ ∈ L.essImageDistTriang →
      ∀ (a : T₁.obj₁ ⟶ T₂.obj₁) (b : T₁.obj₂ ⟶ T₂.obj₂),
        CategoryTheory.CategoryStruct.comp T₁.mor₁ b = CategoryTheory.CategoryStruct.comp a T₂.mor₁ →
          ∃ c,
            CategoryTheory.CategoryStruct.comp T₁.mor₂ c = CategoryTheory.CategoryStruct.comp b T₂.mor₂ ∧
              CategoryTheory.CategoryStruct.comp T₁.mor₃ ((CategoryTheory.shiftFunctor D 1).map a) =
                CategoryTheory.CategoryStruct.comp c T₂.mor₃
-- Lean.Data.Lsp.InitShutdown
Lean.Lsp.InitializeParams.mk.inj : ∀ {processId? : Option ℤ} {clientInfo? : Option Lean.Lsp.ClientInfo} {rootUri? : Option String}
  {initializationOptions? : Option Lean.Lsp.InitializationOptions} {capabilities : Lean.Lsp.ClientCapabilities}
  {trace : Lean.Lsp.Trace} {workspaceFolders? : Option (Array Lean.Lsp.WorkspaceFolder)} {processId?_1 : Option ℤ}
  {clientInfo?_1 : Option Lean.Lsp.ClientInfo} {rootUri?_1 : Option String}
  {initializationOptions?_1 : Option Lean.Lsp.InitializationOptions} {capabilities_1 : Lean.Lsp.ClientCapabilities}
  {trace_1 : Lean.Lsp.Trace} {workspaceFolders?_1 : Option (Array Lean.Lsp.WorkspaceFolder)},
  { processId? := processId?, clientInfo? := clientInfo?, rootUri? := rootUri?,
        initializationOptions? := initializationOptions?, capabilities := capabilities, trace := trace,
        workspaceFolders? := workspaceFolders? } =
      { processId? := processId?_1, clientInfo? := clientInfo?_1, rootUri? := rootUri?_1,
        initializationOptions? := initializationOptions?_1, capabilities := capabilities_1, trace := trace_1,
        workspaceFolders? := workspaceFolders?_1 } →
    processId? = processId?_1 ∧
      clientInfo? = clientInfo?_1 ∧
        rootUri? = rootUri?_1 ∧
          initializationOptions? = initializationOptions?_1 ∧
            capabilities = capabilities_1 ∧ trace = trace_1 ∧ workspaceFolders? = workspaceFolders?_1
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get!_insert : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {k a : α}
  [inst_1 : Inhabited (β a)] {v : β k}, (m.insert k v).get! a = if h : (k == a) = true then cast ⋯ v else m.get! a
-- Mathlib.Topology.MetricSpace.CantorScheme
/-- A scheme where the children of each set are pairwise disjoint induces an injective map.  -/
CantorScheme.Disjoint.map_injective : ∀ {β : Type u_1} {α : Type u_2} {A : List β → Set α},
  CantorScheme.Disjoint A → Function.Injective (CantorScheme.inducedMap A).snd
-- Aesop.Script.SpecificTactics
Aesop.unfoldManyAtS : (Lean.Name → Option (Option Lean.Name)) →
  Lean.MVarId → Lean.FVarId → Aesop.ScriptM (Option (Lean.MVarId × Array Lean.Name))
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.MonoidalOpposite.unmop_mop : ∀ {C : Type u₁} (X : C), { unmop := X }.unmop = X
-- Init.Data.SInt.Bitwise
Int32.or_not_self : ∀ {a : Int32}, a ||| ~~~a = -1
-- Mathlib.LinearAlgebra.RootSystem.CartanMatrix
Set.BijOn.equiv.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} (f : α → β) (h : Set.BijOn f s t),
  Set.BijOn.equiv f h = Equiv.ofBijective (Set.MapsTo.restrict f s t ⋯) ⋯
-- Mathlib.Data.Multiset.Filter
Multiset.mem_filter_of_mem : ∀ {α : Type u_1} {p : α → Prop} [inst : DecidablePred p] {a : α} {l : Multiset α}, a ∈ l → p a → a ∈ Multiset.filter p l
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.or_and_right : ∀ {σs : List (Type u)} {P Q R : Std.Do.SPred σs}, (P ∨ Q) ∧ R ⊣⊢ₛ P ∧ R ∨ Q ∧ R
-- Batteries.Data.String.Lemmas
Substring.Raw.Valid.valid : ∀ {l m r : List Char} {s : Substring.Raw}, Substring.Raw.ValidFor l m r s → s.Valid
-- Mathlib.CategoryTheory.Retract
/-- the split epimorphism  -/
CategoryTheory.Retract.r : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {X Y : C} → CategoryTheory.Retract X Y → (Y ⟶ X)
-- Mathlib.Algebra.Order.Module.HahnEmbedding
HahnSeries.archimedeanClassOrderIsoWithTop.congr_simp : ∀ (Γ : Type u_1) (R : Type u_2) [inst : LinearOrder Γ] [inst_1 : LinearOrder R] [inst_2 : AddCommGroup R]
  [inst_3 : IsOrderedAddMonoid R] [inst_4 : Archimedean R] [inst_5 : Nontrivial R],
  HahnSeries.archimedeanClassOrderIsoWithTop Γ R = HahnSeries.archimedeanClassOrderIsoWithTop Γ R
-- Mathlib.Order.Filter.AtTopBot.Basic
Filter.hasAntitoneBasis_atTop : ∀ {α : Type u_3} [inst : Preorder α] [IsDirectedOrder α] [Nonempty α], Filter.atTop.HasAntitoneBasis Set.Ici
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.isEmpty_eq_size_eq_zero : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β}, t.WF → t.isEmpty = (t.size == 0)
-- Mathlib.Algebra.Ring.Prod
RingEquiv.zeroRingProd_symm_apply : ∀ (R : Type u_1) (S : Type u_3) [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] [inst_2 : Subsingleton S]
  (self : S × R), (RingEquiv.zeroRingProd R S).symm self = self.2
-- Mathlib.Combinatorics.Matroid.Circuit
Matroid.fundCircuit_sdiff_eq_inter : ∀ {α : Type u_1} {I : Set α} {e : α} (M : Matroid α), e ∉ I → M.fundCircuit e I \ {e} = M.fundCircuit e I ∩ I
-- Mathlib.CategoryTheory.Subfunctor.Image
/-- Given a morphism `p : F' ⟶ F` of type-valued functors, this is the morphism
from `F'` to its range.  -/
CategoryTheory.Subfunctor.toRange : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F F' : CategoryTheory.Functor C (Type w)} → (p : F' ⟶ F) → F' ⟶ (CategoryTheory.Subfunctor.range p).toFunctor
-- Init.Data.Fin.Bitwise
Fin.xor_val_of_uInt32Size : ∀ (a b : Fin UInt32.size), ↑(a ^^^ b) = ↑a ^^^ ↑b
-- Lean.Elab.PreDefinition.Structural.IndGroupInfo
Lean.Elab.Structural.IndGroupInst.params : Lean.Elab.Structural.IndGroupInst → Array Lean.Expr
-- Mathlib.Data.Nat.Choose.Basic
Nat.choose_eq_descFactorial_div_factorial : ∀ (n k : ℕ), n.choose k = n.descFactorial k / k.factorial
-- Mathlib.Topology.Algebra.Constructions.DomMulAct
DomAddAct.isEmbedding_mk : ∀ {M : Type u_1} [inst : TopologicalSpace M], Topology.IsEmbedding ⇑DomAddAct.mk
-- Mathlib.Analysis.Meromorphic.NormalForm
/-- Eta-expanded form of `meromorphicNFOn_comp_sub_const_iff_meromorphicNFOn`

---

`MeromorphicNFOn` is invariant under translation.  -/
meromorphicNFOn_fun_comp_sub_const_iff_meromorphicNFOn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {c : 𝕜} {U : Set 𝕜},
  MeromorphicNFOn (fun x => f (x - c)) U ↔ MeromorphicNFOn f (U - {c})
-- Mathlib.RingTheory.Artinian.Ring
/-- Commutative Artinian reduced local ring is a field.  -/
IsArtinianRing.isField_of_isReduced_of_isLocalRing : ∀ (R : Type u_1) [inst : CommRing R] [IsArtinianRing R] [IsReduced R] [IsLocalRing R], IsField R
-- Mathlib.Data.Rat.Cast.Order
/-- Coercion from `ℚ` as an order embedding.  -/
NNRat.castOrderEmbedding : {K : Type u_5} → [inst : Semifield K] → [inst_1 : LinearOrder K] → [IsStrictOrderedRing K] → ℚ≥0 ↪o K
-- Init.Data.SInt.Lemmas
ISize.mul_comm : ∀ (a b : ISize), a * b = b * a
-- Mathlib.RingTheory.Localization.Algebra
/-- The span of `I` in a localization of `R` at `M` is the localization of `I` at `M`.  -/
Algebra.idealMap_isLocalizedModule : ∀ {R : Type u_1} (S : Type u_2) [inst : CommSemiring R] [inst_1 : CommSemiring S] (M : Submonoid R)
  [inst_2 : Algebra R S] [IsLocalization M S] (I : Ideal R), IsLocalizedModule M (Algebra.idealMap S I)
-- Mathlib.Data.Matrix.Basic
Matrix.diagAddMonoidHom_apply : ∀ (n : Type u_3) (α : Type u_11) [inst : AddZeroClass α] (A : Matrix n n α) (i : n),
  (Matrix.diagAddMonoidHom n α) A i = A.diag i
-- Mathlib.Data.Finset.Empty
/-- A `Finset` for an empty type is empty.  -/
Finset.eq_empty_of_isEmpty : ∀ {α : Type u_1} [IsEmpty α] (s : Finset α), s = ∅
-- Mathlib.RepresentationTheory.Coinvariants
Rep.coinvariantsAdjunction_counit_app : ∀ (k : Type u) (G : Type v) [inst : CommRing k] [inst_1 : Monoid G] (X : ModuleCat k),
  (Rep.coinvariantsAdjunction k G).counit.app X =
    Rep.desc (CategoryTheory.CategoryStruct.id ((Rep.trivialFunctor k G).obj X))
-- Mathlib.AlgebraicTopology.SimplicialSet.Boundary
/-- The morphism `Δ[n] ⟶ ∂Δ[n + 1]` corresponding to face
the face `i : Fin (n + 2)`.  -/
SSet.boundary.ι : {n : ℕ} → Fin (n + 2) → (SSet.stdSimplex.obj { len := n } ⟶ (SSet.boundary (n + 1)).toSSet)
-- Mathlib.Algebra.Order.Antidiag.Nat
_private.Mathlib.Algebra.Order.Antidiag.Nat.0.Nat.primeFactorsPiBij.congr_simp : ∀ (d n : ℕ) (f f_1 : (a : ℕ) → a ∈ n.primeFactors → Fin d) (e_f : f = f_1)
  (a : f ∈ n.primeFactors.pi fun x => Finset.univ) (a_1 a_2 : Fin d),
  a_1 = a_2 → Nat.primeFactorsPiBij✝ d n f a a_1 = Nat.primeFactorsPiBij✝ d n f_1 ⋯ a_2
-- Mathlib.Tactic.CategoryTheory.Bicategory.Normalize
Mathlib.Tactic.Bicategory.evalComp_nil_cons : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : B} {f g h i j : a ⟶ b} (α : f ≅ g) (β : g ≅ h) (η : h ⟶ i)
  (ηs : i ⟶ j),
  CategoryTheory.CategoryStruct.comp α.hom
      (CategoryTheory.CategoryStruct.comp β.hom (CategoryTheory.CategoryStruct.comp η ηs)) =
    CategoryTheory.CategoryStruct.comp (α ≪≫ β).hom (CategoryTheory.CategoryStruct.comp η ηs)
-- Mathlib.Order.Interval.Finset.Defs
Set.instFintypeIoc.eq_1 : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] (b a : α),
  Set.instFintypeIoc b a = Fintype.ofFinset (Finset.Ioc b a) ⋯
-- Mathlib.RingTheory.Bialgebra.GroupLike
GroupLike.instCommMonoid : {R : Type u_1} →
  {A : Type u_2} →
    [inst : CommSemiring R] → [inst_1 : CommSemiring A] → [inst_2 : Bialgebra R A] → CommMonoid (GroupLike R A)
-- Mathlib.Probability.Process.LocalProperty
/-- A process `X` satisfies a stable property `p` locally if there exists a pre-localizing
sequence `τ` for which the stopped processes of `fun i ↦ {ω | ⊥ < τ n ω}.indicator (X i)` satisfy
`p`.  -/
ProbabilityTheory.IsStable.locally_of_isPreLocalizingSequence : ∀ {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω}
  [inst : ConditionallyCompleteLinearOrderBot ι] [inst_1 : TopologicalSpace ι] [inst_2 : OrderTopology ι]
  {𝓕 : MeasureTheory.Filtration ι mΩ} {X : ι → Ω → E} {p : (ι → Ω → E) → Prop} [inst_3 : Zero E] [DenselyOrdered ι]
  [FirstCountableTopology ι] [NoMaxOrder ι] {τ : ℕ → Ω → WithTop ι},
  ProbabilityTheory.IsStable 𝓕 p →
    ∀ [𝓕.IsRightContinuous],
      ProbabilityTheory.IsPreLocalizingSequence 𝓕 τ P →
        (∀ (n : ℕ), p (MeasureTheory.stoppedProcess (fun i => {ω | ⊥ < τ n ω}.indicator (X i)) (τ n))) →
          ProbabilityTheory.Locally p 𝓕 X P
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.sum_mapDomain_index : ∀ {k : Type u_1} {G : Type u_2} [inst : AddCommMonoid k] {G' : Type u_3} {f : G → G'} {v : SkewMonoidAlgebra k G}
  {k' : Type u_5} [inst_1 : AddCommMonoid k'] {h : G' → k → k'},
  (∀ (b : G'), h b 0 = 0) →
    (∀ (b : G') (m₁ m₂ : k), h b (m₁ + m₂) = h b m₁ + h b m₂) →
      ((SkewMonoidAlgebra.mapDomain f) v).sum h = v.sum fun a m => h (f a) m
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyMapData.ofIsLimitKernelFork_φK : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (hf₁ : S₁.f = 0) (c₁ : CategoryTheory.Limits.KernelFork S₁.g)
  (hc₁ : CategoryTheory.Limits.IsLimit c₁) (hf₂ : S₂.f = 0) (c₂ : CategoryTheory.Limits.KernelFork S₂.g)
  (hc₂ : CategoryTheory.Limits.IsLimit c₂) (f : c₁.pt ⟶ c₂.pt)
  (comm :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι c₁) φ.τ₂ =
      CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.Fork.ι c₂)),
  (CategoryTheory.ShortComplex.LeftHomologyMapData.ofIsLimitKernelFork φ hf₁ c₁ hc₁ hf₂ c₂ hc₂ f comm).φK = f
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.forM_eq_forM_toList : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {f : α → m PUnit.{u_1 + 1}} [inst : Monad m] [LawfulMonad m]
  {t : RBTree.RBNode α}, RBTree.RBNode.forM f t = t.toList.forM f
-- Mathlib.CategoryTheory.IsConnected
/-- If `Discrete α` is connected, then `α` is (type-)equivalent to `PUnit`.  -/
CategoryTheory.discreteIsConnectedEquivPUnit : {α : Type u₁} → [CategoryTheory.IsConnected (CategoryTheory.Discrete α)] → α ≃ PUnit.{u₁ + 1}