mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Triangulated.Basic
/-- The functor `C ⥤ Triangle C` which sends `X` to `contractibleTriangle X`.  -/
CategoryTheory.Pretriangulated.contractibleTriangleFunctor : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.HasShift C ℤ] →
      [CategoryTheory.Limits.HasZeroObject C] →
        [CategoryTheory.Limits.HasZeroMorphisms C] →
          CategoryTheory.Functor C (CategoryTheory.Pretriangulated.Triangle C)
-- Init.Data.List.Basic
_private.Init.Data.List.Basic.0.List.range'TR.go.match_1.eq_2 : ∀ (motive : ℕ → ℕ → List ℕ → Sort u_1) (n e : ℕ) (acc : List ℕ) (h_1 : (x : ℕ) → (acc : List ℕ) → motive 0 x acc)
  (h_2 : (n e : ℕ) → (acc : List ℕ) → motive n.succ e acc),
  (match n.succ, e, acc with
    | 0, x, acc => h_1 x acc
    | n.succ, e, acc => h_2 n e acc) =
    h_2 n e acc
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.HasImageMap.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f g : CategoryTheory.Arrow C}
  [inst_1 : CategoryTheory.Limits.HasImage f.hom] [inst_2 : CategoryTheory.Limits.HasImage g.hom] {sq : f ⟶ g}
  (m : CategoryTheory.Limits.ImageMap sq), CategoryTheory.Limits.HasImageMap sq
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1.Cfg.inhabited : (Γ : Type u_1) →
  (Λ : Type u_2) → (σ : Type u_3) → [inst : Inhabited Γ] → [Inhabited σ] → Inhabited (Turing.TM1.Cfg Γ Λ σ)
-- Lean.Meta.Tactic.Subst
/-- Given `h : @HEq α a α b` in the given goal, produce a new goal where `h : @Eq α a b`.
If `h` is not of the give form, then just return `(h, mvarId)`
 -/
Lean.Meta.heqToEq : Lean.MVarId → Lean.FVarId → optParam Bool true → Lean.MetaM (Lean.FVarId × Lean.MVarId)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Equiv.erase : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α] (k : α), m₁.Equiv m₂ → (m₁.erase k).Equiv (m₂.erase k)
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyMapData.ofZeros_φH : ∀ {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) (hg₁ : S₁.g = 0) (hf₂ : S₂.f = 0)
  (hg₂ : S₂.g = 0), (CategoryTheory.ShortComplex.LeftHomologyMapData.ofZeros φ hf₁ hg₁ hf₂ hg₂).φH = φ.τ₂
-- Mathlib.Topology.Category.TopPair
/-- Constructs the topological pair `(X, ∅)` from `X : TopCat`.  -/
TopPair.ofTopCat : TopCat → TopPair
-- Mathlib.Algebra.Lie.Nilpotent
LieModule.coe_lowerCentralSeries_eq_int : ∀ (R : Type u) (L : Type v) (M : Type w) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [LieModule R L M] (k : ℕ),
  ↑(LieModule.lowerCentralSeries R L M k) = ↑(LieModule.lowerCentralSeries ℤ L M k)
-- Mathlib.CategoryTheory.Functor.Currying
CategoryTheory.Functor.curryingFlipEquiv_symm_apply_map_app : ∀ {C : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} D]
  {E : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} E] (a : CategoryTheory.Functor (C × D) E) {X Y : D}
  (f : X ⟶ Y) (j : C),
  ((CategoryTheory.Functor.curryingFlipEquiv.symm a).map f).app j =
    a.map (CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id j) f)
-- Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
/-- Transport a term of type `IsTerminal` across an isomorphism.  -/
CategoryTheory.Limits.IsTerminal.ofIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {Y Z : C} → CategoryTheory.Limits.IsTerminal Y → (Y ≅ Z) → CategoryTheory.Limits.IsTerminal Z
-- Mathlib.CategoryTheory.Sites.Point.Basic
CategoryTheory.GrothendieckTopology.Point.instHasExactColimitsOfShapeOppositeElementsFiberOfLocallySmallOfAB5OfSizeOfHasFiniteLimits : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point)
  {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A]
  [inst_2 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] [CategoryTheory.LocallySmall.{w, v, u} C]
  [CategoryTheory.AB5OfSize.{w, w, v', u'} A] [CategoryTheory.Limits.HasFiniteLimits A],
  CategoryTheory.HasExactColimitsOfShape Φ.fiber.Elementsᵒᵖ A
-- Std.Data.ExtTreeMap.Basic
/-- Returns a list of all values present in the tree map in ascending  order.  -/
Std.ExtTreeMap.values : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtTreeMap α β cmp → List β
-- Mathlib.Data.Fin.VecNotation
Matrix.vec_single_eq_const : ∀ {α : Type u} (a : α), ![a] = fun x => a
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
CategoryTheory.Bicategory.mateEquiv_comp_id_right : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d : B} {l₁ : a ⟶ b} {r₁ : b ⟶ a}
  (adj₁ : CategoryTheory.Bicategory.Adjunction l₁ r₁) {l₂ : c ⟶ d} {r₂ : d ⟶ c}
  (adj₂ : CategoryTheory.Bicategory.Adjunction l₂ r₂) {f : a ⟶ c} {g : b ⟶ d}
  (φ :
    CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp l₂ (CategoryTheory.CategoryStruct.id d)) ⟶
      CategoryTheory.CategoryStruct.comp l₁ g),
  (CategoryTheory.Bicategory.mateEquiv adj₁ (adj₂.comp (CategoryTheory.Bicategory.Adjunction.id d))) φ =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Bicategory.mateEquiv adj₁ adj₂)
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Bicategory.rightUnitor (CategoryTheory.CategoryStruct.comp f l₂)).inv
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Bicategory.associator f l₂ (CategoryTheory.CategoryStruct.id d)).hom φ)))
      (CategoryTheory.Bicategory.whiskerLeft g (CategoryTheory.Bicategory.leftUnitor r₂).inv)
-- Mathlib.RingTheory.HahnSeries.Basic
/-- The support of a Hahn series is just the set of indices whose coefficients are nonzero.
Notably, it is well-founded.  -/
HahnSeries.support : {Γ : Type u_1} → {R : Type u_3} → [inst : PartialOrder Γ] → [inst_1 : Zero R] → HahnSeries Γ R → Set Γ
-- Mathlib.Order.Fin.Basic
Fin.predAbove_right_monotone : ∀ {n : ℕ} (p : Fin n), Monotone p.predAbove
-- Mathlib.Algebra.Homology.Factorizations.CM5a
/-- The projections from `mid f n₀`.  -/
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.midπ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {K L : CochainComplex C ℤ} →
        (f : K ⟶ L) →
          [inst_2 : CategoryTheory.EnoughInjectives C] →
            [inst_3 : CategoryTheory.Mono f] →
              (n₀ : ℤ) →
                [inst_4 : K.IsStrictlyGE (n₀ + 1)] →
                  [inst_5 : L.IsStrictlyGE (n₀ + 1)] →
                    (q : ℕ) →
                      CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.mid✝ f n₀ ⟶
                        ((CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.functor✝ f n₀).obj (Opposite.op q)).obj.mid
-- Mathlib.Algebra.Homology.Homotopy
/-- Compatibility of `nullHomotopicMap'` with the postcomposition by a morphism
of complexes.  -/
Homotopy.nullHomotopicMap'_comp : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D E : HomologicalComplex V c} (hom : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)) (g : D ⟶ E),
  CategoryTheory.CategoryStruct.comp (Homotopy.nullHomotopicMap' hom) g =
    Homotopy.nullHomotopicMap' fun i j hij => CategoryTheory.CategoryStruct.comp (hom i j hij) (g.f j)
-- Mathlib.Algebra.Module.Congruence.Defs
VAddCon.mk.inj : ∀ {S : Type u_2} {M : Type u_3} {inst : VAdd S M} {toSetoid : Setoid M}
  {vadd : ∀ (s : S) {x y : M}, toSetoid x y → toSetoid (s +ᵥ x) (s +ᵥ y)} {toSetoid_1 : Setoid M}
  {vadd_1 : ∀ (s : S) {x y : M}, toSetoid_1 x y → toSetoid_1 (s +ᵥ x) (s +ᵥ y)},
  { toSetoid := toSetoid, vadd := vadd } = { toSetoid := toSetoid_1, vadd := vadd_1 } → toSetoid = toSetoid_1
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.semilinearMapClass : ∀ {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₃ : Type u_11} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M] [inst_5 : Module S M₃] {σ : R →+* S},
  SemilinearMapClass (M →ₛₗ[σ] M₃) σ M M₃
-- Mathlib.Geometry.Euclidean.Sphere.Basic
EuclideanGeometry.Sphere.mk_center_radius : ∀ {P : Type u_2} [inst : MetricSpace P] (s : EuclideanGeometry.Sphere P), { center := s.center, radius := s.radius } = s
-- Mathlib.Algebra.Polynomial.Module.AEval
Module.AEval.mem_mapSubmodule_apply : ∀ (R : Type u_2) {A : Type u_3} (M : Type u_1) [inst : CommSemiring R] [inst_1 : Semiring A] (a : A)
  [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : Module A M] [inst_5 : Module R M]
  [inst_6 : IsScalarTower R A M] {p : ↥((Algebra.lsmul R R M) a).invtSubmodule} {m : Module.AEval R M a},
  m ∈ (Module.AEval.mapSubmodule R M a) p ↔ (Module.AEval.of R M a).symm m ∈ ↑p
-- Mathlib.NumberTheory.RamificationInertia.Inertia
/-- **Alias** of `Ideal.inertiaDeg'_map_eq`. -/
Ideal.inertiaDeg_map_eq : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R)
  {S₁ : Type u_1} [inst_3 : CommRing S₁] [inst_4 : Algebra R S₁] (P : Ideal S) {E : Type u_2}
  [inst_5 : EquivLike E S S₁] [AlgEquivClass E R S S₁] (e : E), p.inertiaDeg' (Ideal.map e P) = p.inertiaDeg' P
-- Lean.Meta.Sym.Eta
/-- Applies `etaReduce` to all subexpressions. Returns `e` unchanged if no subexpression is eta-reducible.  -/
Lean.Meta.Sym.etaReduceAll : Lean.Expr → Lean.CoreM Lean.Expr
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.instNeg : {k : Type u_1} → {G : Type u_2} → [inst : AddGroup k] → Neg (SkewMonoidAlgebra k G)
-- Mathlib.Topology.Connected.PathConnected
AddSubgroup.pathComponentZero.eq_1 : ∀ (G : Type u_4) [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalAddGroup G],
  AddSubgroup.pathComponentZero G = { toAddSubmonoid := AddSubmonoid.pathComponentZero G, neg_mem' := ⋯ }
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cocycle.coe_add : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} {n : ℤ} (z₁ z₂ : CochainComplex.HomComplex.Cocycle F G n), ↑(z₁ + z₂) = ↑z₁ + ↑z₂
-- Init.Data.List.Basic
List.head.congr_simp : ∀ {α : Type u} (as as_1 : List α) (e_as : as = as_1) (a : as ≠ []), as.head a = as_1.head ⋯
-- Mathlib.Order.Filter.IsBounded
Filter.isBoundedUnder_le_mul_of_nonneg : ∀ {α : Type u_1} {ι : Type u_4} [inst : Preorder α] [inst_1 : Mul α] [inst_2 : Zero α] [PosMulMono α] [MulPosMono α]
  {f : Filter ι} {u v : ι → α},
  (∃ᶠ (x : ι) in f, 0 ≤ u x) →
    Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u →
      0 ≤ᶠ[f] v →
        Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f v → Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f (u * v)
-- Mathlib.RingTheory.Coalgebra.Hom
/-- The counit of a coalgebra as a `CoalgHom`.  -/
Coalgebra.counitCoalgHom : (R : Type u) →
  (A : Type v) →
    [inst : CommSemiring R] → [inst_1 : AddCommMonoid A] → [inst_2 : Module R A] → [inst_3 : Coalgebra R A] → A →ₗc[R] R
-- Mathlib.Data.Fin.Tuple.Basic
/-- `Π i : Fin 2, α i` is equivalent to `α 0 × α 1`. See also `finTwoArrowEquiv` for a
non-dependent version and `prodEquivPiFinTwo` for a version with inputs `α β : Type u`.  -/
piFinTwoEquiv : (α : Fin 2 → Type u) → ((i : Fin 2) → α i) ≃ α 0 × α 1
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey!_diff_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited α], m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₂ → (m₁ \ m₂).getKey! k = m₁.getKey! k
-- Init.Data.String.PosRaw
/-- Increases the byte offset of the position by `1`. Not to be confused with `Pos.next`.  -/
String.Pos.Raw.inc : String.Pos.Raw → String.Pos.Raw
-- Mathlib.Data.Subtype
Function.extend_val_apply : ∀ {β : Sort u_2} {γ : Sort u_3} {p : β → Prop} {g : { x // p x } → γ} {j : β → γ} {b : β} (hb : p b),
  Function.extend Subtype.val g j b = g ⟨b, hb⟩
-- Mathlib.Algebra.Regular.SMul
/-- The product of `M`-regular elements is `M`-regular.  -/
IsSMulRegular.smul : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} {a : R} {s : S} [inst : SMul R M] [inst_1 : SMul R S] [inst_2 : SMul S M]
  [IsScalarTower R S M], IsSMulRegular M a → IsSMulRegular M s → IsSMulRegular M (a • s)
-- Init.Data.List.Lemmas
_private.Init.Data.List.Lemmas.0.List.findSome?.match_1.eq_2 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (h_1 : (b : β) → motive (some b)) (h_2 : Unit → motive none),
  (match none with
    | some b => h_1 b
    | none => h_2 ()) =
    h_2 ()
-- Mathlib.Data.Fin.Tuple.Basic
Fin.repeat_one : ∀ {n : ℕ} {α : Sort u_1} (a : Fin n → α), Fin.repeat 1 a = a ∘ Fin.cast ⋯
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation_inv_colimit_map_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} J]
  {K : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} K] [inst_3 : CategoryTheory.Limits.HasColimitsOfShape J C]
  (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) {i j : K} (f : i ⟶ j) {Z : C}
  (h : (CategoryTheory.Limits.colimit F).obj j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation F i).inv
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.colimit F).map f) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.colimMap (F.whiskerLeft ((CategoryTheory.evaluation K C).map f)))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation F j).inv h)
-- Mathlib.MeasureTheory.VectorMeasure.SetIntegral
MeasureTheory.VectorMeasure.continuousLinearMap_apply_integral : ∀ {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {H : Type u_6} {mX : MeasurableSpace X}
  [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F] [inst_2 : NormedAddCommGroup G]
  [inst_3 : NormedAddCommGroup H] {μ : MeasureTheory.VectorMeasure X F} {f : X → E} [inst_4 : NormedSpace ℝ E]
  [inst_5 : NormedSpace ℝ F] [inst_6 : NormedSpace ℝ G] [inst_7 : NormedSpace ℝ H] {B : E →L[ℝ] F →L[ℝ] G}
  [CompleteSpace G] [CompleteSpace H] {C : G →L[ℝ] H},
  MeasureTheory.Integrable f μ.variation →
    C ∫ᵛ (y : X), f y ∂[B; μ] = ∫ᵛ (y : X), f y ∂[(ContinuousLinearMap.compL ℝ F G H) C ∘SL B; μ]
-- Lean.Data.Lsp.Extra
Lean.Lsp.LeanFileProgressProcessingInfo : Type
-- Std.Time.Date.Unit.Day
Std.Time.Day.Ordinal.instOfNatOfYear : {leap : Bool} → {n : ℕ} → OfNat (Std.Time.Day.Ordinal.OfYear leap) n
-- Mathlib.Topology.Algebra.Monoid
mulHomOfMemClosureRangeCoe.eq_1 : ∀ {M₁ : Type u_6} {M₂ : Type u_7} [inst : TopologicalSpace M₂] [inst_1 : T2Space M₂] [inst_2 : Mul M₁] [inst_3 : Mul M₂]
  [inst_4 : ContinuousMul M₂] {F : Type u_8} [inst_5 : FunLike F M₁ M₂] [inst_6 : MulHomClass F M₁ M₂] (f : M₁ → M₂)
  (hf : f ∈ closure (Set.range fun f x => f x)), mulHomOfMemClosureRangeCoe f hf = { toFun := f, map_mul' := ⋯ }
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- Given an equivalence of diagrams `e`, `s` is a colimit cocone iff `s.whisker e.functor` is.  -/
CategoryTheory.Limits.IsColimit.whiskerEquivalenceEquiv : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {K : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} K] →
        {C : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            {F : CategoryTheory.Functor J C} →
              {s : CategoryTheory.Limits.Cocone F} →
                (e : K ≌ J) →
                  CategoryTheory.Limits.IsColimit s ≃
                    CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cocone.whisker e.functor s)
-- Mathlib.NumberTheory.DirichletCharacter.Orthogonality
/-- The group of Dirichlet characters mod `n` with values in a ring `R` that has enough
roots of unity is (noncanonically) isomorphic to `(ZMod n)ˣ`.  -/
DirichletCharacter.mulEquiv_units : ∀ (R : Type u_1) [inst : CommRing R] (n : ℕ) [NeZero n] [HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)],
  Nonempty (DirichletCharacter R n ≃* (ZMod n)ˣ)
-- Mathlib.Analysis.Fourier.PoissonSummation
/-- **Poisson's summation formula**, most general form.  -/
Real.tsum_eq_tsum_fourier : ∀ {f : C(ℝ, ℂ)},
  (∀ (K : TopologicalSpace.Compacts ℝ),
      Summable fun n => ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight ↑n))‖) →
    (Summable fun n => FourierTransform.fourier ⇑f ↑n) →
      ∀ (x : ℝ), ∑' (n : ℤ), f (x + ↑n) = ∑' (n : ℤ), FourierTransform.fourier ⇑f ↑n * (fourier n) ↑x
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.natCast_mem : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (S : IntermediateField K L)
  (n : ℕ), ↑n ∈ S
-- Mathlib.MeasureTheory.Integral.CircleAverage
/-- Express the circle average over an arbitrary circle as a circle average over the unit circle.
 -/
Real.circleAverage_eq_circleAverage_zero_one : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℂ → E} {c : ℂ} {R : ℝ},
  Real.circleAverage f c R = Real.circleAverage (fun z => f (↑R * z + c)) 0 1
-- Mathlib.Topology.ClusterPt
MapClusterPt.continuousAt_comp : ∀ {X : Type u} [inst : TopologicalSpace X] {Y : Type v} {α : Type u_1} {F : Filter α} {u : α → X} {x : X}
  [inst_1 : TopologicalSpace Y] {f : X → Y}, ContinuousAt f x → MapClusterPt x F u → MapClusterPt (f x) F (f ∘ u)
-- Plausible.Arbitrary
Plausible.ULift.Arbitrary : {α : Type (max u_1 u_2)} → [Plausible.Arbitrary α] → Plausible.Arbitrary (ULift.{u_2, max u_1 u_2} α)
-- Mathlib.Algebra.Group.Subgroup.Basic
/-- A subgroup is characteristic if it is fixed by all automorphisms.
Several equivalent conditions are provided by lemmas of the form `Characteristic.iff...`  -/
Subgroup.Characteristic : {G : Type u_1} → [inst : Group G] → Subgroup G → Prop
-- Mathlib.RingTheory.Localization.Integer
IsLocalization.isInteger_one : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommSemiring S] [inst_2 : Algebra R S],
  IsLocalization.IsInteger R 1
-- Mathlib.SetTheory.Lists
Lists.to_ofList : ∀ {α : Type u_1} (l : List (Lists α)), (Lists.ofList l).toList = l
-- Std.Data.DTreeMap.Internal.WF.Defs
Std.DTreeMap.Internal.Impl.WF.below.constAlter : ∀ {α : Type u} [inst : Ord α] {motive : {β : α → Type v} → (a : Std.DTreeMap.Internal.Impl α β) → a.WF → Prop}
  {x : Type v} {t : Std.DTreeMap.Internal.Impl α fun x_1 => x} {h : t.Balanced} {k : α} {f : Option x → Option x}
  (a : t.WF), Std.DTreeMap.Internal.Impl.WF.below a → motive t a → Std.DTreeMap.Internal.Impl.WF.below ⋯
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq
CategoryTheory.BicartesianSq.flip : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z}
  {i : Y ⟶ Z}, CategoryTheory.BicartesianSq f g h i → CategoryTheory.BicartesianSq g f i h
-- Mathlib.Topology.Algebra.UniformMulAction
UniformContinuous.const_smul : ∀ {M : Type v} {X : Type x} {Y : Type y} [inst : UniformSpace X] [inst_1 : UniformSpace Y] [inst_2 : SMul M X]
  [UniformContinuousConstSMul M X] {f : Y → X}, UniformContinuous f → ∀ (c : M), UniformContinuous (c • f)
-- Mathlib.Topology.Algebra.TopologicallyNilpotent
/-- An element is topologically nilpotent if its powers converge to `0`.  -/
IsTopologicallyNilpotent : {R : Type u_1} → [MonoidWithZero R] → [TopologicalSpace R] → R → Prop
-- Mathlib.Data.Fin.Tuple.Basic
/-- For `m : Fin n`, if `m < Fin.find p h` then `m` does not satisfy `p`.  -/
Fin.find_min : ∀ {n : ℕ} {p : Fin n → Prop} [inst : DecidablePred p] (h : ∃ k, p k) {j : Fin n}, j < Fin.find p h → ¬p j
-- Mathlib.Topology.MetricSpace.Basic
NNReal.isClosedEmbedding_coe : Topology.IsClosedEmbedding NNReal.toReal
-- Mathlib.Algebra.Module.ZMod
AddSubgroup.toZModSubmodule_symm : ∀ (n : ℕ) {M : Type u_1} [inst : AddCommGroup M] [inst_1 : Module (ZMod n) M],
  ⇑(AddSubgroup.toZModSubmodule n).symm = Submodule.toAddSubgroup
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- **Alias** of the forward direction of `Left.neg_neg_iff`.

---

Uses `left` co(ntra)variant.  -/
pos_of_neg_neg : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α] [AddLeftStrictMono α] {a : α}, -a < 0 → 0 < a
-- Mathlib.Tactic.Contrapose
Mathlib.Tactic.Contrapose.contrapose₂ : ∀ {p q : Prop}, (¬q → p) → ¬p → q
-- Mathlib.CategoryTheory.Functor.FunctorHom
CategoryTheory.Functor.HomObj.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {F G : CategoryTheory.Functor C D} {A : CategoryTheory.Functor C (Type w)} [inst_2 : SizeOf C] [inst_3 : SizeOf D]
  (app : (c : C) → A.obj c → (F.obj c ⟶ G.obj c))
  (naturality :
    autoParam
      (∀ {c d : C} (f : c ⟶ d) (a : A.obj c),
        CategoryTheory.CategoryStruct.comp (F.map f) (app d ((CategoryTheory.ConcreteCategory.hom (A.map f)) a)) =
          CategoryTheory.CategoryStruct.comp (app c a) (G.map f))
      CategoryTheory.Functor.HomObj.naturality._autoParam),
  sizeOf { app := app, naturality := naturality } = 1
-- Mathlib.Data.Fintype.List
Multiset.lists_coe : ∀ {α : Type u_1} (l : List α), (↑l).lists = ↑l.permutations
-- Mathlib.Algebra.Category.Ring.Under.Property
/-- If `P` is a property of ring homs that is stable under finite products and
equalizers, and the latter are preserved by arbitrary base change,
pushout along any ring homomorphism preserves finite limits.  -/
RingHom.HasStableEqualizers.preservesFiniteLimits_pushout : ∀ {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  (RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P) →
    (RingHom.HasFiniteProducts fun {R S} [CommRing R] [CommRing S] => P) →
      (RingHom.HasEqualizers fun {R S} [CommRing R] [CommRing S] => P) →
        (RingHom.HasStableEqualizers fun {R S} [CommRing R] [CommRing S] => P) →
          ∀ [inst : (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] => P).IsStableUnderCobaseChange]
            {R S : CommRingCat} (f : R ⟶ S),
            CategoryTheory.Limits.PreservesFiniteLimits
              (CategoryTheory.MorphismProperty.Under.pushout
                (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] => P) ⊤ f)
-- Mathlib.Algebra.Algebra.Unitization
Unitization.inl_inj : ∀ {R : Type u_1} {A : Type u_2} [inst : Zero A] {x y : R}, Unitization.inl x = Unitization.inl y ↔ x = y
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.vadd_finset_subset_vadd_finset : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : VAdd α β] {s t : Finset β} {a : α},
  s ⊆ t → a +ᵥ s ⊆ a +ᵥ t
-- Lean.Data.JsonRpc
Lean.JsonRpc.instToJsonMessageDirection : Lean.ToJson Lean.JsonRpc.MessageDirection
-- Mathlib.Algebra.Regular.Opposite
/-- **Alias** of the reverse direction of `isAddLeftRegular_unop`. -/
IsAddLeftRegular.unop : ∀ {R : Type u_1} [inst : Add R] {a : Rᵃᵒᵖ}, IsAddRightRegular a → IsAddLeftRegular (AddOpposite.unop a)
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
lt_csSup_iff : ∀ {α : Type u_1} [inst : ConditionallyCompleteLinearOrder α] {s : Set α} {a : α},
  BddAbove s → s.Nonempty → (a < sSup s ↔ ∃ b ∈ s, a < b)
-- Mathlib.Data.Finset.Option
Finset.mem_eraseNone : ∀ {α : Type u_1} {s : Finset (Option α)} {x : α}, x ∈ Finset.eraseNone s ↔ some x ∈ s
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.valueGroupEquiv_symm_apply : ∀ {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] {R : Type u_3} [inst_1 : Ring R] (v : Valuation R Γ₀)
  (b : { b // (fun x => x ∈ ↑(MonoidWithZeroHom.ofClass v).valueGroup) b }),
  (WithVal.valueGroupEquiv v).symm b = ⟨↑b, ⋯⟩
-- Lean.Parser.Term
Lean.Parser.Term.unsafe.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.Order.GroupWithZero.Basic
posMulReflectLT_iff_contravariant_pos : ∀ {α : Type u_1} [inst : MulZeroClass α] [inst_1 : PartialOrder α],
  PosMulReflectLT α ↔ ContravariantClass { x // 0 < x } α (fun x y => ↑x * y) fun x1 x2 => x1 < x2