mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Async.Basic
/-- Sequences two computations, allowing the second to depend on the value computed by the first.
 -/
Std.Async.EAsync.bind : {ε α β : Type} → Std.Async.EAsync ε α → (α → Std.Async.EAsync ε β) → Std.Async.EAsync ε β
-- Mathlib.Algebra.GroupWithZero.Defs
GroupWithZero.toMonoidWithZero : {G₀ : Type u} → [self : GroupWithZero G₀] → MonoidWithZero G₀
-- Mathlib.RingTheory.Etale.Finite
CommAlgCat.FiniteEtale.equivOfIsSepClosed_inverse_map : ∀ (Ω : Type u) [inst : Field Ω] [inst_1 : IsSepClosed Ω] {X Y : FintypeCat} (f : X ⟶ Y),
  (CommAlgCat.FiniteEtale.equivOfIsSepClosed Ω).inverse.map f =
    (CommAlgCat.FiniteEtale.ofHom
        (AlgHom.pi fun i => Pi.evalAlgHom Ω (fun a => Ω) ((CategoryTheory.ConcreteCategory.hom f) i))).op
-- Mathlib.Topology.MetricSpace.Thickening
/-- The closure of a set equals the intersection of its open thickenings of positive radii
accumulating at zero.  -/
Metric.closure_eq_iInter_thickening' : ∀ {α : Type u} [inst : PseudoEMetricSpace α] (E : Set α),
  ∀ s ⊆ Set.Ioi 0, (∀ (ε : ℝ), 0 < ε → (s ∩ Set.Ioc 0 ε).Nonempty) → closure E = ⋂ δ ∈ s, Metric.thickening δ E
-- Mathlib.Data.Multiset.Lattice
Multiset.inf_dedup : ∀ {α : Type u_1} [inst : SemilatticeInf α] [inst_1 : OrderTop α] [inst_2 : DecidableEq α] (s : Multiset α),
  s.dedup.inf = s.inf
-- Mathlib.CategoryTheory.Functor.ReflectsIso.Jointly
/-- A family of functors jointly reflects epimorphisms if for every morphism `f : X ⟶ Y`
such that the image of `f` under all `F i` is an epimorphism, then `f` is an epimorphism.  -/
CategoryTheory.JointlyReflectEpimorphisms : {C : Type u_1} →
  [inst : CategoryTheory.Category.{u_4, u_1} C] →
    {I : Type u_2} →
      {D : I → Type u_3} →
        [inst_1 : (i : I) → CategoryTheory.Category.{u_5, u_3} (D i)] →
          ((i : I) → CategoryTheory.Functor C (D i)) → Prop
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
AddMonoidAlgebra.mapDomainOfBialgHom_id : ∀ {R : Type u_1} {G : Type u_5} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : AddGroup G],
  AddMonoidAlgebra.mapDomainOfBialgHom (BialgHom.id R (AddMonoidAlgebra R G)) = AddMonoidHom.id G
-- Mathlib.Data.Real.ConjExponents
/-- For `r`, instead of `p`  -/
NNReal.HolderTriple.one_div_pos' : ∀ {p q r : NNReal}, p.HolderTriple q r → 0 < 1 / r
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Comon_
CategoryTheory.comonEquiv_unitIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C],
  CategoryTheory.comonEquiv.unitIso = CategoryTheory.NatIso.ofComponents CategoryTheory.isoCartesianComon ⋯
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.hasLeftExtension_iff_of_iso₁ : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  {L L' : CategoryTheory.Functor C D} (iso₁ : L ≅ L') (F : CategoryTheory.Functor C H),
  L.HasLeftKanExtension F ↔ L'.HasLeftKanExtension F
-- Mathlib.CategoryTheory.Bicategory.Yoneda
/-- The Yoneda pseudofunctor from `B` to `Bᵒᵖ ⥤ᵖ Cat`.

It consists of the following:
* On objects: sends `x : B` to the pseudofunctor `Bᵒᵖ ⥤ᵖ Cat` given by
  `a ↦ (a ⟶ x)` on objects and on 1- and 2-morphisms given by "precomposing"
* On 1- and 2-morphisms it is given by "postcomposing"  -/
CategoryTheory.Bicategory.yoneda : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    CategoryTheory.Pseudofunctor B (CategoryTheory.Pseudofunctor Bᵒᵖ CategoryTheory.Cat)
-- Init.Data.UInt.Lemmas
UInt64.ofNatLT_sub : ∀ {a b : ℕ} (ha : a < 2 ^ 64) (hab : b ≤ a), UInt64.ofNatLT (a - b) ⋯ = UInt64.ofNatLT a ha - UInt64.ofNatLT b ⋯
-- Init.Data.UInt.Lemmas
UInt32.toNat_zero : UInt32.toNat 0 = 0
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Closeds.instSetLike : {α : Type u_2} → [inst : TopologicalSpace α] → SetLike (TopologicalSpace.Closeds α) α
-- Mathlib.RingTheory.AdjoinRoot
/-- Embedding of the original ring `R` into `AdjoinRoot p`.  -/
AdjoinRoot.ofAlgHom : {R : Type u_1} →
  (S : Type u_2) →
    [inst : CommRing R] → [inst_1 : CommSemiring S] → [inst_2 : Algebra S R] → (p : Polynomial R) → R →ₐ[S] AdjoinRoot p
-- Mathlib.MeasureTheory.Function.LpSpace.Complete
MeasureTheory.Lp.cauchySeq_Lp_iff_cauchySeq_eLpNorm : ∀ {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {E : Type u_3}
  [inst : NormedAddCommGroup E] {ι : Type u_4} [Nonempty ι] [inst_2 : SemilatticeSup ι] [hp : Fact (1 ≤ p)]
  (f : ι → ↥(MeasureTheory.Lp E p μ)),
  CauchySeq f ↔ Filter.Tendsto (fun n => MeasureTheory.eLpNorm (↑↑(f n.1) - ↑↑(f n.2)) p μ) Filter.atTop (nhds 0)
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.const_le : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} [inst : LE β] {x y : β}, x ≤ y → ↑x ≤ ↑y
-- Mathlib.CategoryTheory.Yoneda
/-- Extensionality via Yoneda. The typical usage would be
```
-- Goal is `X ≅ Y`
apply Yoneda.ext
-- Goals are now functions `(Z ⟶ X) → (Z ⟶ Y)`, `(Z ⟶ Y) → (Z ⟶ X)`, and the fact that these
-- functions are inverses and natural in `Z`.
```
 -/
CategoryTheory.Yoneda.ext : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (X Y : C) →
      (p : {Z : C} → (Z ⟶ X) → (Z ⟶ Y)) →
        (q : {Z : C} → (Z ⟶ Y) → (Z ⟶ X)) →
          (∀ {Z : C} (f : Z ⟶ X), q (p f) = f) →
            (∀ {Z : C} (f : Z ⟶ Y), p (q f) = f) →
              (∀ {Z Z' : C} (f : Z' ⟶ Z) (g : Z ⟶ X),
                  p (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp f (p g)) →
                (X ≅ Y)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get!_alter_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp],
  t.WF →
    ∀ {k : α} [inst_1 : Inhabited (β k)] {f : Option (β k) → Option (β k)}, (t.alter k f).get! k = (f (t.get? k)).get!
-- Mathlib.Order.Filter.Defs
/-- `f.Eventually p` or `∀ᶠ x in f, p x` mean that `{x | p x} ∈ f`. E.g., `∀ᶠ x in atTop, p x`
means that `p` holds true for sufficiently large `x`.  -/
Filter.Eventually : {α : Type u_1} → (α → Prop) → Filter α → Prop
-- Mathlib.Data.Set.Image
Set.preimage_subset_preimage_iff : ∀ {α : Type u_1} {β : Type u_2} {s t : Set α} {f : β → α}, s ⊆ Set.range f → (f ⁻¹' s ⊆ f ⁻¹' t ↔ s ⊆ t)
-- Mathlib.Analysis.Calculus.Deriv.MeanValue
/-- Let `f : ℝ → ℝ` be a differentiable function. If `f' ≤ C`, then `f` grows at most as fast
as `C * x`, i.e., `f y - f x ≤ C * (y - x)` whenever `x ≤ y`.  -/
image_sub_le_mul_sub_of_deriv_le : ∀ {f : ℝ → ℝ}, Differentiable ℝ f → ∀ {C : ℝ}, (∀ (x : ℝ), deriv f x ≤ C) → ∀ ⦃x y : ℝ⦄, x ≤ y → f y - f x ≤ C * (y - x)
-- Mathlib.RingTheory.Ideal.Operations
Ideal.iSup_mul : ∀ {R : Type u} [inst : Semiring R] {ι : Sort u_1} (J : ι → Ideal R) (I : Ideal R), (⨆ i, J i) * I = ⨆ i, J i * I
-- Mathlib.AlgebraicTopology.MooreComplex
AlgebraicTopology.NormalizedMooreComplex.map_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {X Y : CategoryTheory.SimplicialObject C} (f : X ⟶ Y) (n : ℕ),
  (AlgebraicTopology.NormalizedMooreComplex.map f).f n =
    (AlgebraicTopology.NormalizedMooreComplex.objX Y n).factorThru
      (CategoryTheory.CategoryStruct.comp (AlgebraicTopology.NormalizedMooreComplex.objX X n).arrow
        (f.app (Opposite.op { len := n })))
      ⋯
-- Mathlib.Algebra.Category.Grp.Limits
/-- A functor `F : J ⥤ GrpCat.{u}` has a limit iff `(F ⋙ forget GrpCat).sections` is
`u`-small.  -/
GrpCat.hasLimit_iff_small_sections : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J GrpCat),
  CategoryTheory.Limits.HasLimit F ↔ Small.{u, max u v} ↑(F.comp (CategoryTheory.forget GrpCat)).sections
-- Mathlib.Algebra.Polynomial.Div
Polynomial.zero_divByMonic : ∀ {R : Type u} [inst : Ring R] (p : Polynomial R), 0 /ₘ p = 0
-- Mathlib.Analysis.Normed.Lp.lpHolder
Memℓp.bilin_of_top_left : ∀ {ι : Type u_1} {𝕜 : Type u_2} {E : ι → Type u_3} {F : ι → Type u_4} {G : ι → Type u_5} [inst : RCLike 𝕜]
  [inst_1 : (i : ι) → NormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_3 : (i : ι) → NormedAddCommGroup (F i)] [inst_4 : (i : ι) → NormedSpace 𝕜 (F i)]
  [inst_5 : (i : ι) → NormedAddCommGroup (G i)] [inst_6 : (i : ι) → NormedSpace 𝕜 (G i)] {q : ENNReal}
  (B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i) {K : ℝ},
  (∀ (i : ι), ‖B i‖ ≤ K) →
    ∀ {e : (i : ι) → E i} {f : (i : ι) → F i}, Memℓp e ⊤ → Memℓp f q → Memℓp (fun i => ((B i) (e i)) (f i)) q
-- Mathlib.RingTheory.LocalProperties.Basic
Localization.algEquiv.congr_simp : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) (S : Type u_2) [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : IsLocalization M S], Localization.algEquiv M S = Localization.algEquiv M S
-- Mathlib.Tactic.TacticAnalysis.Declarations
_private.Mathlib.Tactic.TacticAnalysis.Declarations.0.Mathlib.TacticAnalysis.TerminalReplacementOutcome.success.injEq : ∀ (stx stx_1 : Lean.TSyntax `tactic),
  (Mathlib.TacticAnalysis.TerminalReplacementOutcome.success✝ stx =
      Mathlib.TacticAnalysis.TerminalReplacementOutcome.success✝ stx_1) =
    (stx = stx_1)
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.mem_iSup_of_mem : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {ι : Sort u_1}
  {S : ι → Subalgebra R A} (i : ι) {x : A}, x ∈ S i → x ∈ iSup S
-- Mathlib.RingTheory.Algebraic.MvPolynomial
Set.subtypeInsertEquivOption.eq_1 : ∀ {α : Type u_1} [inst : DecidableEq α] {t : Set α} {x : α} (h : x ∉ t),
  Set.subtypeInsertEquivOption h =
    { toFun := fun y => if h : ↑y = x then none else some ⟨↑y, ⋯⟩, invFun := fun y => y.elim ⟨x, ⋯⟩ fun z => ⟨↑z, ⋯⟩,
      left_inv := ⋯, right_inv := ⋯ }
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
BitVec.reduceBitVecOfFin : Lean.Meta.Simp.DSimproc
-- Std.Data.DHashMap.Internal.Defs
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.eraseManyEntries : {α : Type u} →
  {β : α → Type v} →
    {ρ : Type w} →
      [ForIn Id ρ ((a : α) × β a)] →
        [inst : BEq α] →
          [inst_1 : Hashable α] →
            (m : Std.DHashMap.Internal.Raw₀ α β) →
              ρ →
                { m' //
                  ∀ (P : Std.DHashMap.Internal.Raw₀ α β → Prop),
                    (∀ {m'' : Std.DHashMap.Internal.Raw₀ α β} {a : α}, P m'' → P (m''.erase a)) → P m → P m' }
-- Std.Http.Data.Method
/-- Bind a resource to an additional URI path.
Source: https://www.rfc-editor.org/rfc/rfc5842#section-4
 -/
Std.Http.Method.bind : Std.Http.Method
-- Init.Data.String.Basic
_private.Init.Data.String.Basic.0.String.Pos.Raw.get?.match_1.splitter : (motive : String → String.Pos.Raw → Sort u_1) →
  (x : String) → (x_1 : String.Pos.Raw) → ((s : String) → (p : String.Pos.Raw) → motive s p) → motive x x_1
-- Mathlib.Algebra.Star.LinearMap
LinearMap.intrinsicStar_comp : ∀ {R : Type u_1} {E : Type u_2} {F : Type u_3} [inst : Semiring R] [inst_1 : InvolutiveStar R]
  [inst_2 : AddCommMonoid E] [inst_3 : Module R E] [inst_4 : StarAddMonoid E] [inst_5 : StarModule R E]
  [inst_6 : AddCommMonoid F] [inst_7 : Module R F] [inst_8 : StarAddMonoid F] [inst_9 : StarModule R F] {G : Type u_4}
  [inst_10 : AddCommMonoid G] [inst_11 : Module R G] [inst_12 : StarAddMonoid G] [inst_13 : StarModule R G]
  (f : WithConv (E →ₗ[R] F)) (g : WithConv (G →ₗ[R] E)),
  star (WithConv.toConv (f.ofConv ∘ₗ g.ofConv)) = WithConv.toConv ((star f).ofConv ∘ₗ (star g).ofConv)
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
/-- Given a subgraph and a set of vertices, delete all the vertices from the subgraph,
if present. Any edges incident to the deleted vertices are deleted as well.  -/
SimpleGraph.Subgraph.deleteVerts : {V : Type u} → {G : SimpleGraph V} → G.Subgraph → Set V → G.Subgraph
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.ConnectedComponent.eq_of_common_vertex : ∀ {V : Type u} {G : SimpleGraph V} {v : V} {c c' : G.ConnectedComponent}, v ∈ c.supp → v ∈ c'.supp → c = c'
-- Mathlib.Algebra.Algebra.Equiv
instUniqueAlgEquivOfSubsingleton : {R : Type u_1} →
  {S : Type u_2} →
    {T : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring S] →
          [inst_2 : Semiring T] →
            [inst_3 : Algebra R S] → [inst_4 : Algebra R T] → [Subsingleton S] → [Subsingleton T] → Unique (S ≃ₐ[R] T)
-- Mathlib.Topology.Algebra.Group.Basic
isClosedMap_inv : ∀ (G : Type w) [inst : TopologicalSpace G] [inst_1 : InvolutiveInv G] [ContinuousInv G], IsClosedMap Inv.inv
-- Init.Data.String.Lemmas.Order
String.Pos.ne_endPos_of_sliceTo_ne_endPos : ∀ {s : String} {p p₀ : s.Pos} {h₀ : p ≤ p₀}, p₀.sliceTo p h₀ ≠ (s.sliceTo p₀).endPos → p ≠ s.endPos
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.LeftFraction.instIsIsoMapSOfIsLocalization : ∀ {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] {W : CategoryTheory.MorphismProperty C} {X Y : C}
  {L : CategoryTheory.Functor C D} [L.IsLocalization W] (z : W.LeftFraction X Y), CategoryTheory.IsIso (L.map z.s)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfc_nonneg_iff : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R] [ContinuousSqrt R]
  [StarOrderedRing R] [inst_8 : TopologicalSpace A] [inst_9 : Ring A] [inst_10 : StarRing A] [inst_11 : PartialOrder A]
  [StarOrderedRing A] [inst_13 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] [NonnegSpectrumClass R A]
  (f : R → R) (a : A),
  autoParam (ContinuousOn f (spectrum R a)) cfc_nonneg_iff._auto_1 →
    autoParam (p a) cfc_nonneg_iff._auto_3 → (0 ≤ cfc f a ↔ ∀ x ∈ spectrum R a, 0 ≤ f x)
-- Mathlib.RingTheory.Noetherian.Filter
eventuallyConst_of_isNoetherian : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [IsNoetherian R M]
  (f : ℕ →o Submodule R M), Filter.EventuallyConst (⇑f) Filter.atTop
-- Mathlib.GroupTheory.GroupAction.Hom
AddActionHom.inverse'_comp : ∀ {M : Type u_2} {N : Type u_3} {φ : M → N} {X : Type u_5} [inst : VAdd M X] {Y : Type u_6} [inst_1 : VAdd N Y]
  {φ' : N → M} {f : X →ₑ[φ] Y} {g : Y → X} {k₂ : Function.RightInverse φ' φ} {h₁ : Function.LeftInverse g ⇑f}
  {h₂ : Function.RightInverse g ⇑f}, f.comp (f.inverse' g k₂ h₁ h₂) = AddActionHom.id N
-- Mathlib.LinearAlgebra.RootSystem.RootPositive
RootPairing.RootPositiveForm.posForm.eq_1 : ∀ {ι : Type u_1} {R : Type u_2} {S : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing S]
  [inst_1 : LinearOrder S] [inst_2 : CommRing R] [inst_3 : Algebra S R] [inst_4 : AddCommGroup M] [inst_5 : Module R M]
  [inst_6 : AddCommGroup N] [inst_7 : Module R N] {P : RootPairing ι R M N} [inst_8 : P.IsValuedIn S]
  (B : RootPairing.RootPositiveForm S P) [inst_9 : FaithfulSMul S R] [inst_10 : Module S M]
  [inst_11 : IsScalarTower S R M],
  B.posForm =
    (Submodule.span S (Set.range ⇑P.root)).subtype.restrictScalarsRange₂ (Submodule.span S (Set.range ⇑P.root)).subtype
      (Algebra.linearMap S R) ⋯ B.form ⋯
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.Spanning.union_right : ∀ {α : Type u_2} {M : Matroid α} {X S : Set α},
  M.Spanning S → autoParam (X ⊆ M.E) Matroid.Spanning.union_right._auto_1 → M.Spanning (X ∪ S)
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.AbelianImages
CategoryTheory.Abelian.PreservesCoimage.iso.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] {X Y : C} (f : X ⟶ Y)
  [inst_5 : CategoryTheory.Limits.HasKernel f]
  [inst_6 : CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι f)]
  [inst_7 : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) F]
  [inst_8 :
    CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.kernel.ι f) 0) F]
  [inst_9 : CategoryTheory.Limits.HasKernel (F.map f)]
  [inst_10 : CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι (F.map f))],
  CategoryTheory.Abelian.PreservesCoimage.iso F f =
    CategoryTheory.Limits.PreservesCokernel.iso F (CategoryTheory.Limits.kernel.ι f) ≪≫
      CategoryTheory.Limits.cokernel.mapIso (F.map (CategoryTheory.Limits.kernel.ι f))
        (CategoryTheory.Limits.kernel.ι (F.map f)) (CategoryTheory.Limits.PreservesKernel.iso F f)
        (CategoryTheory.Iso.refl (F.obj X)) ⋯
-- Mathlib.NumberTheory.DirichletCharacter.Basic
/-- The set of natural numbers `d` such that `χ` factors through a character of level `d`.  -/
DirichletCharacter.conductorSet : {R : Type u_1} → [inst : CommMonoidWithZero R] → {n : ℕ} → DirichletCharacter R n → Set ℕ
-- Std.Data.String.ToInt
String.Slice.isInt_iff : ∀ {s : String.Slice}, s.isInt = true ↔ s.isNat = true ∨ ∃ t, s.copy = "-" ++ t ∧ t.isNat = true
-- Init.Data.BitVec.Lemmas
BitVec.toInt_neg_iff : ∀ {w : ℕ} {x : BitVec w}, x.toInt < 0 ↔ 2 ^ w ≤ 2 * x.toNat
-- Mathlib.Tactic.Simps.NotationClass
/-- `isNotation` is a Boolean that specifies whether this is notation
(false for the coercions `DFunLike` and `SetLike`). If this is set to true, we add the current
class as hypothesis during type-class synthesis.  -/
Simps.AutomaticProjectionData.isNotation : Simps.AutomaticProjectionData → Bool
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubAddAction.copy.eq_1 : ∀ {R : Type u} {M : Type v} [inst : VAdd R M] (p : SubAddAction R M) (s : Set M) (hs : s = ↑p),
  p.copy s hs = { carrier := s, vadd_mem' := ⋯ }
-- Mathlib.Algebra.Ring.BooleanRing
RingEquiv.asBoolRingAsBoolAlg_apply : ∀ (α : Type u_4) [inst : BooleanRing α] (a : AsBoolRing (AsBoolAlg α)),
  (RingEquiv.asBoolRingAsBoolAlg α) a = ofBoolAlg (ofBoolRing a)
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.stdSimplex.face_obj : ∀ {n : ℕ} (S : Finset (Fin (n + 1))) (U : SimplexCategoryᵒᵖ),
  (SSet.stdSimplex.face S).obj U =
    {f | Finset.image ⇑(SimplexCategory.Hom.toOrderHom (SSet.stdSimplex.objEquiv f)) ⊤ ⊆ S}
-- Mathlib.Topology.CWComplex.Classical.Finite
/-- A CW complex is finite dimensional if `cell C n` is empty for all but finitely many `n`.  -/
Topology.RelCWComplex.FiniteDimensional : {X : Type u} → [inst : TopologicalSpace X] → (C : Set X) → {D : Set X} → [Topology.RelCWComplex C D] → Prop
-- Mathlib.GroupTheory.Index
Subgroup.index_iInf_ne_zero : ∀ {G : Type u_1} [inst : Group G] {ι : Type u_3} [Finite ι] {f : ι → Subgroup G},
  (∀ (i : ι), (f i).index ≠ 0) → (⨅ i, f i).index ≠ 0
-- Mathlib.Data.ENat.Basic
/-- **Alias** of `ENat.top_sub_natCast`. -/
ENat.top_sub_coe : ∀ (a : ℕ), ⊤ - ↑a = ⊤
-- Mathlib.RingTheory.Valuation.Integers
Valuation.Integers.valuation_unit : ∀ {F : Type u} {Γ₀ : Type v} [inst : Field F] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] {v : Valuation F Γ₀}
  {O : Type w} [inst_2 : CommRing O] [inst_3 : Algebra O F], v.Integers O → ∀ (x : Oˣ), v ((algebraMap O F) ↑x) = 1
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
_private.Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet.0.Associates.FactorSet.prod.match_1.eq_2 : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] (motive : Associates.FactorSet α → Sort u_2)
  (s : Multiset { a // Irreducible a }) (h_1 : Unit → motive none)
  (h_2 : (s : Multiset { a // Irreducible a }) → motive (some s)),
  (match some s with
    | none => h_1 ()
    | some s => h_2 s) =
    h_2 s
-- Mathlib.Tactic.NormNum.Basic
Mathlib.Meta.NormNum.ble_eq_false : ∀ {x y : ℕ}, x.ble y = false ↔ y < x
-- Init.Meta.Defs
Lean.idEndEscape : Char
-- Mathlib.Tactic.Algebra.Lemmas
Mathlib.Tactic.Algebra.eq_trans_trans : ∀ {A : Type u_2} {e₁ e₂ a b : A}, e₁ = a → e₂ = b → a = b → e₁ = e₂
-- Mathlib.Algebra.Order.Module.PositiveLinearMap
PositiveLinearMap.toLinearMap_zero : ∀ {R : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid E₁]
  [inst_2 : PartialOrder E₁] [inst_3 : AddCommMonoid E₂] [inst_4 : PartialOrder E₂] [inst_5 : Module R E₁]
  [inst_6 : Module R E₂], PositiveLinearMap.toLinearMap 0 = 0
-- Mathlib.Algebra.WithConv
WithConv.toConv_sum : ∀ {A : Type u_2} [inst : AddCommMonoid A] {ι : Type u_5} (s : Finset ι) (f : ι → A),
  WithConv.toConv (∑ i ∈ s, f i) = ∑ i ∈ s, WithConv.toConv (f i)
-- Mathlib.RingTheory.Extension.Cotangent.Basis
_private.Mathlib.RingTheory.Extension.Cotangent.Basis.0.Algebra.Generators.PresentationOfFreeCotangent.Aux.cotangentEquivProd_symm_apply : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {ι : Type u_4}
  {P : Algebra.Generators R S ι} {σ : Type u_5} {b : Module.Basis σ S P.toExtension.Cotangent}
  (D : Algebra.Generators.PresentationOfFreeCotangent.Aux✝ P b) [inst_3 : Nontrivial S]
  (x : (Algebra.Generators.PresentationOfFreeCotangent.Aux.presRight✝ D).toExtension.Cotangent)
  (y :
    TensorProduct (Algebra.Generators.PresentationOfFreeCotangent.Aux.T✝ D) S
      (Algebra.Generators.PresentationOfFreeCotangent.Aux.presLeft✝ D).toExtension.Cotangent),
  (Algebra.Generators.PresentationOfFreeCotangent.Aux.cotangentEquivProd✝ D).symm (x, y) =
    (Algebra.Generators.cotangentCompLocalizationAwayEquiv (Algebra.Generators.PresentationOfFreeCotangent.Aux.gbar✝ D)
          (Algebra.Generators.PresentationOfFreeCotangent.Aux.presLeft✝ D).toGenerators ⋯).symm
      (y, x)
-- Mathlib.Analysis.Convex.Cone.Basic
/-- The closure of image of a proper cone under a linear map is a proper cone.

We use continuous maps here to match `ProperCone.comap`.  -/
ProperCone.map : {R : Type u_2} →
  {E : Type u_3} →
    {F : Type u_4} →
      [inst : Semiring R] →
        [inst_1 : PartialOrder R] →
          [inst_2 : IsOrderedRing R] →
            [inst_3 : AddCommMonoid E] →
              [inst_4 : TopologicalSpace E] →
                [inst_5 : Module R E] →
                  [inst_6 : AddCommMonoid F] →
                    [inst_7 : TopologicalSpace F] →
                      [inst_8 : Module R F] →
                        [ContinuousAdd F] → [ContinuousConstSMul R F] → (E →L[R] F) → ProperCone R E → ProperCone R F
-- Mathlib.FieldTheory.IsAlgClosed.Basic
IntermediateField.algHomEquivAlgHomOfSplits_symm_apply : ∀ {F : Type u_1} {K : Type u_2} (A : Type u_3) [inst : Field F] [inst_1 : Field K] [inst_2 : Field A]
  [inst_3 : Algebra F K] [inst_4 : Algebra F A] [inst_5 : Algebra.IsAlgebraic F K] (L : IntermediateField F A)
  (hL : ∀ (x : K), (Polynomial.map (algebraMap F ↥L) (minpoly F x)).Splits) (f : K →ₐ[F] A),
  (IntermediateField.algHomEquivAlgHomOfSplits A L hL).symm f = f.codRestrict L.toSubalgebra ⋯
-- Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
SSet.relativeCellComplexOfMono.Cell.ι_b_ι_assoc : ∀ {X Y : SSet} {i : X ⟶ Y} {d : ℕ} (c : SSet.relativeCellComplexOfMono.Cell i d) {Z : SSet} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp c.ιSigmaStdSimplex
      (CategoryTheory.CategoryStruct.comp (SSet.relativeCellComplexOfMono.b i d)
        (CategoryTheory.CategoryStruct.comp ((SSet.skeletonOfMono i) (d + 1)).ι h)) =
    CategoryTheory.CategoryStruct.comp c.map h
-- Mathlib.Combinatorics.SimpleGraph.Copy
/-- If `G` is isomorphic to `H`, then `H` is inducingly contained in `G`.  -/
SimpleGraph.Iso.isIndContained' : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} (e : G ≃g H), H.IsIndContained G
-- Init.Internal.Order.Lemmas
_private.Init.Internal.Order.Lemmas.0.Array.isEqvAux.match_1.eq_2 : ∀ {α : Type u_1} (xs : Array α) (motive : (x : ℕ) → x ≤ xs.size → Sort u_2) (i : ℕ) (h : i + 1 ≤ xs.size)
  (h_1 : (x : 0 ≤ xs.size) → motive 0 x) (h_2 : (i : ℕ) → (h : i + 1 ≤ xs.size) → motive i.succ h),
  (match i.succ, h with
    | 0, x => h_1 x
    | i.succ, h => h_2 i h) =
    h_2 i h
-- Mathlib.Order.SupClosed
supClosed_iInter : ∀ {α : Type u_3} [inst : SemilatticeSup α] {ι : Sort u_5} {f : ι → Set α},
  (∀ (i : ι), SupClosed (f i)) → SupClosed (⋂ i, f i)
-- Mathlib.Data.List.OffDiag
List.count_offDiag_eq_mul_sub_ite : ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α) (a b : α),
  List.count (a, b) l.offDiag = List.count a l * List.count b l - if a = b then List.count a l else 0