mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Bicategory.LocallyDiscrete
CategoryTheory.CommSq.toLoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] {X₁ X₂ X₃ X₄ : C} {t : X₁ ⟶ X₂} {l : X₁ ⟶ X₃}
  {r : X₂ ⟶ X₄} {b : X₃ ⟶ X₄}, CategoryTheory.CommSq t l r b → CategoryTheory.CommSq t.toLoc l.toLoc r.toLoc b.toLoc
-- LeanSearchClient.Syntax
LeanSearchClient.searchTermImpl : Lean.Elab.Term.TermElab
-- Mathlib.Algebra.Group.Hom.Instances
MonoidHom.flip_apply : ∀ {M : Type uM} {N : Type uN} {P : Type uP} {x : MulOneClass M} {x_1 : MulOneClass N} {x_2 : CommMonoid P}
  (f : M →* N →* P) (x_3 : M) (y : N), (f.flip y) x_3 = (f x_3) y
-- Mathlib.Data.Rat.Cast.Order
NNRat.preimage_cast_Ioo : ∀ {K : Type u_5} [inst : Semifield K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] (p q : ℚ≥0),
  NNRat.cast ⁻¹' Set.Ioo ↑p ↑q = Set.Ioo p q
-- Init.Data.List.Control
_private.Init.Data.List.Control.0.List.findM?.match_1.eq_2 : ∀ {α : Type} (motive : List α → Sort u_1) (a : α) (as : List α) (h_1 : Unit → motive [])
  (h_2 : (a : α) → (as : List α) → motive (a :: as)),
  (match a :: as with
    | [] => h_1 ()
    | a :: as => h_2 a as) =
    h_2 a as
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.commRight_tmul : ∀ (R : Type uR) {S : Type uS} {A : Type uA} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  [inst_3 : Semiring A] [inst_4 : Algebra R A] (s : S) (a : A),
  (Algebra.TensorProduct.commRight R S A) (s ⊗ₜ[R] a) = a ⊗ₜ[R] s
-- Mathlib.CategoryTheory.Preadditive.Basic
CategoryTheory.Preadditive.epi_of_isZero_cokernel' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C} {f : X ⟶ Y}
  (c : CategoryTheory.Limits.CokernelCofork f) (hc : CategoryTheory.Limits.IsColimit c),
  CategoryTheory.Limits.IsZero c.pt → CategoryTheory.Epi f
-- Mathlib.Combinatorics.SetFamily.HarrisKleitman
/-- **Harris-Kleitman inequality**: Any two upper sets of finsets correlate.  -/
IsUpperSet.le_card_inter_finset : ∀ {α : Type u_1} [inst : DecidableEq α] {𝒜 ℬ : Finset (Finset α)} [inst_1 : Fintype α],
  IsUpperSet ↑𝒜 → IsUpperSet ↑ℬ → 𝒜.card * ℬ.card ≤ 2 ^ Fintype.card α * (𝒜 ∩ ℬ).card
-- Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage
Dynamics.dynEntourage_one : ∀ {X : Type u_1} {T : X → X} {U : SetRel X X}, Dynamics.dynEntourage T U 1 = U
-- Mathlib.Algebra.Homology.HomologicalComplex
/-- Construct an `α`-indexed chain complex from a dependently-typed differential.
 -/
ChainComplex.of : {V : Type u} →
  [inst : CategoryTheory.Category.{v, u} V] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
      {α : Type u_2} →
        [inst_2 : AddRightCancelSemigroup α] →
          [inst_3 : One α] →
            [DecidableEq α] →
              (X : α → V) →
                (d : (n : α) → X (n + 1) ⟶ X n) →
                  (∀ (n : α), CategoryTheory.CategoryStruct.comp (d (n + 1)) (d n) = 0) → ChainComplex V α
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
/-- A `WeierstrassCurve` is in normal form of characteristic = 3, if it is
`Y² = X³ + a₂X² + a₆` (`WeierstrassCurve.IsCharThreeJNeZeroNF`) or
`Y² = X³ + a₄X + a₆` (`WeierstrassCurve.IsShortNF`).  -/
WeierstrassCurve.IsCharThreeNF : {R : Type u_1} → [CommRing R] → WeierstrassCurve R → Prop
-- Mathlib.RingTheory.GradedAlgebra.Basic
GradedRing.projZeroRingHom_apply : ∀ {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [inst : Semiring A] [inst_1 : DecidableEq ι] [inst_2 : AddCommMonoid ι]
  [inst_3 : PartialOrder ι] [inst_4 : CanonicallyOrderedAdd ι] [inst_5 : SetLike σ A] [inst_6 : AddSubmonoidClass σ A]
  (𝒜 : ι → σ) [inst_7 : GradedRing 𝒜] (a : A), (GradedRing.projZeroRingHom 𝒜) a = ↑(((DirectSum.decompose 𝒜) a) 0)
-- Mathlib.Data.Nat.Nth
Nat.count_nth : ∀ {p : ℕ → Prop} [inst : DecidablePred p] {n : ℕ},
  (∀ (hf : (Set.ofPred p).Finite), n < hf.toFinset.card) → Nat.count p (Nat.nth p n) = n
-- Mathlib.Geometry.Euclidean.Circumcenter
/-- Given a nonempty affine subspace, whose direction is
finite-dimensional, that contains a set of points, those points are
cospherical if and only if they are equidistant from some point in
that subspace.  -/
EuclideanGeometry.cospherical_iff_exists_mem_of_finiteDimensional : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : AffineSubspace ℝ P} {ps : Set P},
  ps ⊆ ↑s →
    ∀ [Nonempty ↥s] [FiniteDimensional ℝ ↥s.direction],
      EuclideanGeometry.Cospherical ps ↔ ∃ center ∈ s, ∃ radius, ∀ p ∈ ps, dist p center = radius
-- Mathlib.RingTheory.PowerSeries.WellKnown
/-- Note that `mk 1` is the constant function `1` so the power series `1 + X + X^2 + ...`. This theorem
states that for any `d : ℕ`, `(1 + X + X^2 + ... : S⟦X⟧) ^ (d + 1)` is equal to the power series
`mk fun n => Nat.choose (d + n) d : S⟦X⟧`.
 -/
PowerSeries.mk_one_pow_eq_mk_choose_add : ∀ (S : Type u_1) [inst : CommRing S] (d : ℕ), PowerSeries.mk 1 ^ (d + 1) = PowerSeries.mk fun n => ↑((d + n).choose d)
-- Mathlib.AlgebraicGeometry.ZariskisMainTheorem
/-- [Stacks Tag 04XV](https://stacks.math.columbia.edu/tag/04XV) ((1) <=> (2)) -/
AlgebraicGeometry.IsClosedImmersion.iff_isProper_and_mono : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y),
  AlgebraicGeometry.IsClosedImmersion f ↔ AlgebraicGeometry.IsProper f ∧ CategoryTheory.Mono f
-- Mathlib.Algebra.Group.Defs
neg_neg : ∀ {G : Type u_1} [inst : InvolutiveNeg G] (a : G), - -a = a
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instAddGroup.eq_1 : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [inst_2 : IsTopologicalAddGroup G],
  SeparationQuotient.instAddGroup =
    { toAddMonoid := SeparationQuotient.instAddMonoid, toNeg := SeparationQuotient.instNeg,
      toSub := SeparationQuotient.instSub, toZSMul := ZSMul.ofSMul, sub_eq_add_neg := ⋯, zsmul_zero' := ⋯,
      zsmul_succ' := ⋯, zsmul_neg' := ⋯, neg_add_cancel := ⋯ }
-- Mathlib.CategoryTheory.Center.Localization
CategoryTheory.CatCenter.localization_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (r : CategoryTheory.CatCenter C) (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C)
  [inst_2 : L.IsLocalization W] (X : C), (r.localization L W).app (L.obj X) = L.map (r.app X)
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Fan.nonempty_isLimit_iff_isIso_piLift : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f : β → C}
  [inst_1 : CategoryTheory.Limits.HasProduct f] (c : CategoryTheory.Limits.Fan f),
  Nonempty (CategoryTheory.Limits.IsLimit c) ↔ CategoryTheory.IsIso (CategoryTheory.Limits.Pi.lift c.proj)
-- Mathlib.CategoryTheory.Limits.Yoneda
CategoryTheory.coyonedaFunctor_reflectsLimits : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  CategoryTheory.Limits.ReflectsLimitsOfSize.{t, w, v, max u v, u, max u (v + 1)} CategoryTheory.coyoneda
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.ringEquiv_symm_apply_toCLM : ∀ {𝕜₁ : Type u_1} [inst : NormedField 𝕜₁] {E : Type u_3} [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E]
  [inst_3 : Module 𝕜₁ E] [inst_4 : IsTopologicalAddGroup E] (toCLM : E →L[𝕜₁] E),
  (ContinuousLinearMapWOT.ringEquiv.symm toCLM).toCLM = toCLM
-- Lean.Meta.Tactic.Grind.Arith.FieldNormNum
_private.Lean.Meta.Tactic.Grind.Arith.FieldNormNum.0.Lean.Meta.Grind.Arith.FieldNormNum.M : Type → Type
-- Mathlib.RingTheory.TwoSidedIdeal.Kernel
TwoSidedIdeal.ker.congr_simp : ∀ {R : Type u_1} {S : Type u_2} [inst : NonUnitalNonAssocRing R] [inst_1 : NonUnitalNonAssocSemiring S] {F : Type u_3}
  [inst_2 : FunLike F R S] [inst_3 : NonUnitalRingHomClass F R S] (f f_1 : F),
  f = f_1 → TwoSidedIdeal.ker f = TwoSidedIdeal.ker f_1
-- Mathlib.NumberTheory.LSeries.DirichletContinuation
/-- The L function of the trivial Dirichlet character mod `N` has a simple pole with
residue `∏ p ∈ N.primeFactors, (1 - p⁻¹)` at `s = 1`.  -/
DirichletCharacter.LFunctionTrivChar_residue_one : ∀ {N : ℕ} [inst : NeZero N],
  Filter.Tendsto (fun s => (s - 1) * DirichletCharacter.LFunctionTrivChar N s) (nhdsWithin 1 {1}ᶜ)
    (nhds (∏ p ∈ N.primeFactors, (1 - (↑p)⁻¹)))
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.Λ'.read.injEq : ∀ (f f_1 : Option Turing.PartrecToTM2.Γ' → Turing.PartrecToTM2.Λ'),
  (Turing.PartrecToTM2.Λ'.read f = Turing.PartrecToTM2.Λ'.read f_1) = (f = f_1)
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.isUnsatEq.eq_2 : ∀ (p : Int.Internal.Linear.Poly), (∀ (k : ℤ), p = Int.Internal.Linear.Poly.num k → False) → p.isUnsatEq = false
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getEntryGE?.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α),
  Std.DTreeMap.Internal.Impl.getEntryGE? k = Std.DTreeMap.Internal.Impl.getEntryGE?.go k none
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddMonoidHom.comp.eq_1 : ∀ {A : Type u_2} {B : Type u_3} {C : Type u_4} [inst : AddMonoid A] [inst_1 : AddMonoid B] [inst_2 : AddMonoid C]
  [inst_3 : TopologicalSpace A] [inst_4 : TopologicalSpace B] [inst_5 : TopologicalSpace C] (g : B →ₜ+ C) (f : A →ₜ+ B),
  g.comp f = { toAddMonoidHom := g.comp f.toAddMonoidHom, continuous_toFun := ⋯ }
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.coe_addEquiv_apply : ∀ {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂}
  {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂) (x : M),
  ↑e x = e x
-- Batteries.Data.Fin.Lemmas
Fin.coe_clamp : ∀ (n m : ℕ), ↑(Fin.clamp n m) = min n m
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
/-- A sheaf of modules is finitely presented if it is locally the cokernel of a
morphism between coproducts of finitely many copies of the sheaf of rings.  -/
SheafOfModules.isFinitePresentation : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      (R : CategoryTheory.Sheaf J RingCat) →
        [∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] →
          [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] →
            CategoryTheory.ObjectProperty (SheafOfModules R)
-- Mathlib.Topology.Algebra.Algebra.Equiv
ContinuousAlgEquiv.coe_mk : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : TopologicalSpace A] [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A]
  [inst_6 : Algebra R B] (e : A ≃ₐ[R] B) (he : Continuous e.toFun) (he' : Continuous e.invFun),
  ⇑{ toAlgEquiv := e, continuous_toFun := he, continuous_invFun := he' } = ⇑e
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Ideal.homogeneousCore_eq_sSup : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : Semiring A] [inst_1 : DecidableEq ι] [inst_2 : AddMonoid ι]
  [inst_3 : SetLike σ A] [inst_4 : AddSubmonoidClass σ A] (𝒜 : ι → σ) [inst_5 : GradedRing 𝒜] (I : Ideal A),
  Ideal.homogeneousCore 𝒜 I = sSup {J | J.toIdeal ≤ I}
-- Mathlib.Data.Nat.Cast.Basic
Sum.elim_natCast_natCast : ∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : NatCast γ] (n : ℕ), Sum.elim ↑n ↑n = ↑n
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.hasFPowerSeriesAt_weierstrassPExcept : ∀ (L : PeriodPair) (l : ℂ),
  HasFPowerSeriesAt (L.weierstrassPExcept l)
    (FormalMultilinearSeries.ofScalars ℂ fun i =>
      if i = 0 then L.weierstrassPExcept l l else (↑i + 1) * L.sumInvPow l (i + 2))
    l
-- Mathlib.SetTheory.ZFC.Ordinal
/-- A set `x` is a von Neumann ordinal when it's a transitive set, that's transitive under `∈`. We
prove that this further implies that `x` is well-ordered under `∈` in `isOrdinal_iff_isWellOrder`.

The transitivity condition `a ∈ b → b ∈ c → a ∈ c` can be written without assuming `a ∈ x` and
`b ∈ x`. The lemma `isOrdinal_iff_isTrans` shows this condition is equivalent to the usual one.  -/
ZFSet.IsOrdinal : ZFSet.{u_1} → Prop
-- Lean.Compiler.IR.Basic
Lean.IR.instAlphaEqvExpr : Lean.IR.AlphaEqv Lean.IR.Expr
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.instIsTrivialVOfCompLinearMapIdρ : ∀ {k : Type u} {G : Type v} [inst : Ring k] [inst_1 : Monoid G] {H : Type u'} {V : Type w} [inst_2 : Group H]
  [inst_3 : AddCommGroup V] [inst_4 : Module k V] (ρ : Representation k H V) (f : G →* H)
  [Representation.IsTrivial (MonoidHom.comp ρ f)], Representation.IsTrivial (MonoidHom.comp (Rep.of ρ).ρ f)
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
Subsemigroup.unop_bot : ∀ {M : Type u_2} [inst : Mul M], ⊥.unop = ⊥
-- Mathlib.SetTheory.ZFC.Class
Class.classToCong_empty : ∅.classToCong = ∅
-- Mathlib.FieldTheory.PolynomialGaloisGroup
Polynomial.Gal.smul : {F : Type u_1} →
  [inst : Field F] →
    (p : Polynomial F) →
      (E : Type u_2) →
        [inst_1 : Field E] →
          [inst_2 : Algebra F E] → [Fact (Polynomial.map (algebraMap F E) p).Splits] → SMul p.Gal ↑(p.rootSet E)
-- Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
SSet.mem_skeleton_obj_iff_of_nonDegenerate : ∀ (X : SSet) {d : ℕ} (x : ↑(X.nonDegenerate d)) (n : ℕ), ↑x ∈ (X.skeleton n).obj (Opposite.op { len := d }) ↔ d < n
-- Mathlib.Tactic.NormNum.Ineq
_private.Mathlib.Tactic.NormNum.Ineq.0.Mathlib.Meta.NormNum.evalLT.core.ratArm : {u : Lean.Level} →
  {α : Q(Type u)} →
    (lα : Q(LT «$α»)) →
      {a b : Q(«$α»)} →
        Mathlib.Meta.NormNum.Result a →
          Mathlib.Meta.NormNum.Result b →
            have e := q(«$a» < «$b»);
            Lean.MetaM (Mathlib.Meta.NormNum.Result e)
-- Mathlib.Topology.Connected.Basic
connectedComponent_eq : ∀ {α : Type u} [inst : TopologicalSpace α] {x y : α},
  y ∈ connectedComponent x → connectedComponent x = connectedComponent y
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.surjOn_iff_le_map : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {f : M →* N} {H : Submonoid M}
  {K : Submonoid N}, Set.SurjOn ⇑f ↑H ↑K ↔ K ≤ Submonoid.map f H
-- Init.Data.Vector.Lemmas
Vector.map_id_fun : ∀ {n : ℕ} {α : Type u_1}, Vector.map id = id
-- Init.Data.Slice.Array.Iterator
Subarray.instToIterator : {α : Type u} → Std.ToIterator (Std.Slice (Std.Slice.Internal.SubarrayData α)) Id (SubarrayIterator α) α
-- Mathlib.Analysis.Complex.PhragmenLindelof
/-- **Phragmen-Lindelöf principle** in a strip `U = {z : ℂ | a < im z < b}`.
Let `f g : ℂ → E` be functions such that

* `f` and `g` are differentiable on `U` and are continuous on its closure;
* `‖f z‖` and `‖g z‖` are bounded from above by `A * exp(B * exp(c * |re z|))` on `U` for some
  `c < π / (b - a)`;
* `f z = g z` on the boundary of `U`.

Then `f` is equal to `g` on the closed strip `{z : ℂ | a ≤ im z ≤ b}`.
 -/
PhragmenLindelof.eqOn_horizontal_strip : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {a b : ℝ} {f g : ℂ → E},
  DiffContOnCl ℂ f (Complex.im ⁻¹' Set.Ioo a b) →
    (∃ c < Real.pi / (b - a),
        ∃ B,
          f =O[Filter.comap (abs ∘ Complex.re) Filter.atTop ⊓ Filter.principal (Complex.im ⁻¹' Set.Ioo a b)] fun z =>
            Real.exp (B * Real.exp (c * |z.re|))) →
      DiffContOnCl ℂ g (Complex.im ⁻¹' Set.Ioo a b) →
        (∃ c < Real.pi / (b - a),
            ∃ B,
              g =O[Filter.comap (abs ∘ Complex.re) Filter.atTop ⊓ Filter.principal (Complex.im ⁻¹' Set.Ioo a b)]
                fun z => Real.exp (B * Real.exp (c * |z.re|))) →
          (∀ (z : ℂ), z.im = a → f z = g z) →
            (∀ (z : ℂ), z.im = b → f z = g z) → Set.EqOn f g (Complex.im ⁻¹' Set.Icc a b)
-- Mathlib.Geometry.Manifold.PartitionOfUnity
/-- The tsupport of a partition of unity at a point `x₀` as a `Finset`.
This is the set of `i : ι` such that `x₀ ∈ tsupport f i`.  -/
SmoothPartitionOfUnity.fintsupport : {ι : Type uι} →
  {E : Type uE} →
    [inst : NormedAddCommGroup E] →
      [inst_1 : NormedSpace ℝ E] →
        {H : Type uH} →
          [inst_2 : TopologicalSpace H] →
            {I : ModelWithCorners ℝ E H} →
              {M : Type uM} →
                [inst_3 : TopologicalSpace M] →
                  [inst_4 : ChartedSpace H M] → {s : Set M} → SmoothPartitionOfUnity ι I M s → M → Finset ι
-- Lean.Elab.Declaration
_private.Lean.Elab.Declaration.0.Lean.Elab.Command.ensureValidNamespace : Lean.Name → Lean.MacroM Unit
-- Mathlib.NumberTheory.Dioph
_private.Mathlib.NumberTheory.Dioph.0.Poly.sumsq.match_1.eq_1 : ∀ {α : Type u_1} (motive : List (Poly α) → Sort u_2) (h_1 : Unit → motive [])
  (h_2 : (p : Poly α) → (ps : List (Poly α)) → motive (p :: ps)),
  (match [] with
    | [] => h_1 ()
    | p :: ps => h_2 p ps) =
    h_1 ()
-- Mathlib.Topology.Order.ScottTopology
Topology.WithScott.isOpen_iff_isUpperSet_and_scottHausdorff_open' : ∀ {α : Type u_1} [inst : Preorder α] {u : Set α},
  IsOpen (⇑Topology.WithScott.ofScott ⁻¹' u) ↔ IsUpperSet u ∧ TopologicalSpace.IsOpen u
-- Mathlib.CategoryTheory.Subfunctor.Subobject
CategoryTheory.Subfunctor.range_subobjectMk_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)}
  (A : CategoryTheory.Subfunctor F), CategoryTheory.Subfunctor.range (CategoryTheory.Subobject.mk A.ι).arrow = A
-- Mathlib.Order.Hom.BoundedLattice
/-- A `BoundedLatticeHomClass` morphism preserves the bottom element.  -/
BoundedLatticeHomClass.map_bot : ∀ {F : Type u_6} {α : Type u_7} {β : Type u_8} {inst : Lattice α} {inst_1 : Lattice β} {inst_2 : BoundedOrder α}
  {inst_3 : BoundedOrder β} {inst_4 : FunLike F α β} [self : BoundedLatticeHomClass F α β] (f : F), f ⊥ = ⊥
-- Mathlib.Data.List.Intervals
List.Ico.nodup : ∀ (n m : ℕ), (List.Ico n m).Nodup
-- Mathlib.Algebra.Category.AlgCat.Basic
/-- The free/forget adjunction for `R`-algebras.  -/
AlgCat.adj : (R : Type u) → [inst : CommRing R] → AlgCat.free R ⊣ CategoryTheory.forget (AlgCat R)
-- Mathlib.GroupTheory.FiniteIndexNormalSubgroup
FiniteIndexNormalAddSubgroup.comap_id : ∀ {G : Type u_1} [inst : AddGroup G] (K : FiniteIndexNormalAddSubgroup G),
  FiniteIndexNormalAddSubgroup.comap (AddMonoidHom.id G) K = K
-- Mathlib.Analysis.Normed.Group.Constructions
ULift.normedAddCommGroup.eq_1 : ∀ {E : Type u_2} [inst : NormedAddCommGroup E],
  ULift.normedAddCommGroup =
    NormedAddCommGroup.induced (ULift.{u_5, u_2} E) E { toFun := ULift.down, map_zero' := ⋯, map_add' := ⋯ } ⋯
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
CategoryTheory.SmallObject.restrictionLE.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : PartialOrder J] {j : J}
  (F F_1 : CategoryTheory.Functor (↑(Set.Iic j)) C),
  F = F_1 →
    ∀ {i : J} (hi : i ≤ j),
      CategoryTheory.SmallObject.restrictionLE F hi = CategoryTheory.SmallObject.restrictionLE F_1 hi
-- Init.Data.Int.DivMod.Lemmas
Int.ediv_eq_zero_of_lt : ∀ {a b : ℤ}, 0 ≤ a → a < b → a / b = 0
-- Mathlib.CategoryTheory.Category.PartialFun
partialFunEquivPointed_inverse_obj : ∀ (X : Pointed), partialFunEquivPointed.inverse.obj X = PartialFun.of { x // ¬x = X.point }
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.forM_eq_forM_toList : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashSet.Raw α} {m' : Type v → Type w} [inst_2 : Monad m']
  [LawfulMonad m'], m.WF → ∀ {f : α → m' PUnit.{v + 1}}, forM m f = forM m.toList f
-- Mathlib.Algebra.Order.Group.Action
/-- A copy of `smul_mono_right` that is understood by `gcongr`.  -/
smul_le_smul_left : ∀ {M : Type u_2} {α : Type u_3} [inst : SMul M α] [inst_1 : Preorder α] [CovariantClass M α HSMul.hSMul LE.le] (m : M)
  {a b : α}, a ≤ b → m • a ≤ m • b
-- Init.Data.Fin.Lemmas
Fin.val_mod : ∀ {n : ℕ} (a m : Fin n), ↑(a % m) = ↑a % ↑m
-- Mathlib.Algebra.GroupWithZero.Nat
Nat.instSemigroupWithZero : SemigroupWithZero ℕ
-- Init.Data.SInt.Lemmas
ISize.toInt.inj : ∀ {x y : ISize}, x.toInt = y.toInt → x = y
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SymbolKind.enum : Lean.Lsp.SymbolKind
-- Mathlib.Order.Category.BoolAlg
BoolAlg.hasForgetToHeytAlg_forget₂_obj_coe : ∀ (X : BoolAlg), ↑(CategoryTheory.HasForget₂.forget₂.obj X) = ↑X
-- Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular
SSet.N.stdSimplex_map_monoOfLE_yonedaEquiv_symm_simplex_assoc : ∀ {X : SSet} [inst : X.Nonsingular] {x y : X.N} (h : x ≤ y) {Z : SSet} (h_1 : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.map (SSet.N.monoOfLE h))
      (CategoryTheory.CategoryStruct.comp (SSet.yonedaEquiv.symm y.simplex) h_1) =
    CategoryTheory.CategoryStruct.comp (SSet.yonedaEquiv.symm x.simplex) h_1
-- Std.Http.Data.Request
/-- Creates a new HTTP HEAD Request builder with the specified URI.
 -/
Std.Http.Request.head : Std.Http.RequestTarget → Std.Http.Request.Builder
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.pentagon_inv_inv_hom_inv_inv_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {W X Y Z Z_1 : C}
  (h :
    CategoryTheory.MonoidalCategoryStruct.tensorObj
        (CategoryTheory.MonoidalCategoryStruct.tensorObj W (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)) Z ⟶
      Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator W X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorObj W X) Y Z).inv
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.whiskerRight
            (CategoryTheory.MonoidalCategoryStruct.associator W X Y).hom Z)
          h)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft W (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.associator W (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z).inv
        h)
-- Std.Http.Internal.IndexMultiMap
/-- Like `get?`, but returns a default value if absent.
 -/
Std.Internal.IndexMultiMap.getD : {α : Type u} → {β : Type v} → [inst : BEq α] → [inst_1 : Hashable α] → Std.Internal.IndexMultiMap α β → α → β → β
-- Init.Data.SInt.Bitwise
instCommutativeInt16HOr : Std.Commutative fun x1 x2 => x1 ||| x2
-- Mathlib.NumberTheory.RamificationInertia.Ramification
/-- **Alias** of `Ideal.IsDedekindDomain.ramificationIdx'_ne_zero_of_liesOver`. -/
Ideal.IsDedekindDomain.ramificationIdx_ne_zero_of_liesOver : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] [IsDedekindDomain S]
  [IsDomain R] [Module.IsTorsionFree R S] (P : Ideal S) [hP : P.IsPrime] {p : Ideal R},
  p ≠ ⊥ → ∀ [hPp : P.LiesOver p], p.ramificationIdx' P ≠ 0
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
/-- A (reducible) alias of `QuasispectrumRestricts` which enforces stronger type class assumptions
on the types involved, as it's really intended for the `spectrum`. The separate definition also
allows for dot notation.  -/
SpectrumRestricts : {R : Type u_3} →
  {S : Type u_4} →
    {A : Type u_5} →
      [inst : Semifield R] →
        [inst_1 : Semifield S] → [inst_2 : Ring A] → [Algebra R A] → [Algebra S A] → [Algebra R S] → A → (S → R) → Prop
-- Mathlib.Order.ULift
ULift.up_sdiff : ∀ {α : Type u} [inst : SDiff α] (a b : α), { down := a \ b } = { down := a } \ { down := b }
-- Mathlib.Dynamics.TopologicalEntropy.Subset
/-- **Alias** of `Dynamics.coverEntropySupBotHom`.

---

Topological entropy `CoverEntropy T` as a `SupBotHom` function of the subset.  -/
Dynamics.coverEntropy_supBotHom : {X : Type u_1} → [UniformSpace X] → (X → X) → SupBotHom (Set X) EReal
-- Mathlib.SetTheory.Ordinal.Exponential
Ordinal.isSuccLimit_opow : ∀ {a b : Ordinal.{u_1}}, 1 < a → Order.IsSuccLimit b → Order.IsSuccLimit (a ^ b)
-- Mathlib.Tactic.GRewrite.Core
/-- The rewrite lemma has unified with something, and depends on a free variable that is now
out of scope. We store a local context in which the rewrite makes sense.  -/
_private.Mathlib.Tactic.GRewrite.Core.0.Mathlib.Tactic.GRewrite.Progress.matchedOutOfScope : Lean.LocalContext → Mathlib.Tactic.GRewrite.Progress✝