mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.FunctionField
/-- The function field of an irreducible scheme is the local ring at its generic point.
Despite the name, this is a field only when the scheme is integral.  -/
AlgebraicGeometry.Scheme.functionField : (X : AlgebraicGeometry.Scheme) → [IrreducibleSpace ↥X] → CommRingCat
-- Mathlib.Algebra.Group.WithOne.Basic
/-- `WithOne.coe` as a bundled morphism  -/
WithOne.coeMulHom : {α : Type u} → [inst : Mul α] → α →ₙ* WithOne α
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.normal_subgroupOf_of_le_normalizer : ∀ {G : Type u_1} [inst : Group G] {H N : Subgroup G}, H ≤ Subgroup.normalizer ↑N → (N.subgroupOf H).Normal
-- Mathlib.Topology.Category.CompHausLike.Limits
/-- The inclusion maps into the explicit finite coproduct are open embeddings.  -/
CompHausLike.finiteCoproduct.isOpenEmbedding_ι : ∀ {P : TopCat → Prop} {α : Type w} [inst : Finite α] (X : α → CompHausLike P)
  [inst_1 : CompHausLike.HasExplicitFiniteCoproduct X] (a : α),
  Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (CompHausLike.finiteCoproduct.ι X a))
-- Mathlib.Analysis.Distribution.TestFunction
TestFunction.lineDerivCLM_add : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4} [inst_3 : NormedAddCommGroup F]
  [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace 𝕜 F] {n k : ℕ∞} [inst_6 : Algebra ℝ 𝕜] [inst_7 : IsScalarTower ℝ 𝕜 F]
  {v₁ v₂ : E}, TestFunction.lineDerivCLM 𝕜 (v₁ + v₂) = TestFunction.lineDerivCLM 𝕜 v₁ + TestFunction.lineDerivCLM 𝕜 v₂
-- Mathlib.Order.Filter.Map
Filter.map_top : ∀ {α : Type u_1} {β : Type u_2} (f : α → β), Filter.map f ⊤ = Filter.principal (Set.range f)
-- Mathlib.Algebra.Group.TypeTags.Pointwise
Multiplicative.ofAdd_image_setAdd : ∀ {M : Type u_1} [inst : AddMonoid M] (s t : Set M),
  ⇑Multiplicative.ofAdd '' (s + t) = ⇑Multiplicative.ofAdd '' s * ⇑Multiplicative.ofAdd '' t
-- Init.GrindInstances.Ring.UInt
Lean.Grind.instIsCharPUInt16OfNatNat : Lean.Grind.IsCharP UInt16 65536
-- Mathlib.Data.List.Induction
List.bidirectionalRec.eq_1 : ∀ {α : Type u_1} {motive : List α → Sort u_2} (nil : motive []) (singleton : (a : α) → motive [a])
  (cons_append : (a : α) → (l : List α) → (b : α) → motive l → motive (a :: (l ++ [b]))),
  List.bidirectionalRec nil singleton cons_append [] = nil
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
fderiv_ccosh : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : E → ℂ} {x : E},
  DifferentiableAt ℂ f x → fderiv ℂ (fun x => Complex.cosh (f x)) x = Complex.sinh (f x) • fderiv ℂ f x
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.InfinitePlace.isUnramified_iff : ∀ {k : Type u_1} [inst : Field k] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra k K]
  {w : NumberField.InfinitePlace K},
  NumberField.InfinitePlace.IsUnramified k w ↔ w.IsReal ∨ (w.comap (algebraMap k K)).IsComplex
-- Mathlib.Data.ENat.Basic
ENat.add_left_injective_of_ne_top : ∀ {n : ℕ∞}, n ≠ ⊤ → Function.Injective fun x => x + n
-- Mathlib.Analysis.Normed.Module.Ball.Pointwise
/-- Image of a bounded set in a normed space under scalar multiplication by a constant is
bounded. See also `Bornology.IsBounded.smul` for a similar lemma about an isometric action.  -/
Bornology.IsBounded.smul₀ : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  {s : Set E}, Bornology.IsBounded s → ∀ (c : 𝕜), Bornology.IsBounded (c • s)
-- Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
UniformConvergenceCLM.instIsSMulApply : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3}
  (F : Type u_4) [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜₁ E] [inst_4 : TopologicalSpace E]
  [inst_5 : AddCommGroup F] [inst_6 : Module 𝕜₂ F] {M : Type u_6} [inst_7 : Monoid M] [inst_8 : DistribMulAction M F]
  [inst_9 : SMulCommClass 𝕜₂ M F] [inst_10 : TopologicalSpace F] [inst_11 : ContinuousConstSMul M F] (𝔖 : Set (Set E)),
  IsSMulApply M (UniformConvergenceCLM σ F 𝔖) E F
-- Mathlib.RingTheory.Smooth.Basic
/-- Localization at an element is smooth.  -/
Algebra.Smooth.of_isLocalization_Away : ∀ {R : Type u_4} [inst : CommRing R] {A : Type u_5} [inst_1 : CommRing A] [inst_2 : Algebra R A] (r : R)
  [IsLocalization.Away r A], Algebra.Smooth R A
-- Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
EReal.expHomeomorph_apply : ∀ (x : EReal), EReal.expHomeomorph x = x.exp
-- Mathlib.LinearAlgebra.RootSystem.Reduced
RootPairing.instFlipIsReduced : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) [Finite ι]
  [CharZero R] [IsDomain R] [Module.IsTorsionFree R M] [P.IsReduced] [Module.IsTorsionFree R N], P.flip.IsReduced
-- Mathlib.Lean.CoreM
CoreM.withImportModules.unsafe_impl_5 : {α : Type} → Array Lean.Name → Lean.CoreM α → Option Lean.SearchPath → Lean.Options → UInt32 → String → IO α
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
/-- Constructing a bounded continuous function from a uniformly bounded continuous
function taking values in a normed group.  -/
BoundedContinuousFunction.ofNormedAddCommGroup : {α : Type u} →
  {β : Type v} →
    [inst : TopologicalSpace α] →
      [inst_1 : SeminormedAddCommGroup β] →
        (f : α → β) → Continuous f → (C : ℝ) → (∀ (x : α), ‖f x‖ ≤ C) → BoundedContinuousFunction α β
-- Lean.Elab.DefView
/-- Prepends the `defeq` attribute, removing existing ones if there are any.
The `defeq` attribute's validator also tags `backward_defeq` on success, so the
superset invariant `defeq ⊆ backward_defeq` is preserved.  -/
Lean.Elab.DefView.markDefEq : Lean.Elab.DefView → Lean.Elab.DefView
-- Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
CategoryTheory.ObjectProperty.isoModSerre_zero_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (P : CategoryTheory.ObjectProperty C) [inst_2 : P.IsSerreClass] (X Y : C), P.isoModSerre 0 ↔ P X ∧ P Y
-- Mathlib.Algebra.Star.Basic
/-- `star` as a ring automorphism, for commutative `R`.  -/
starRingAut : {R : Type u} → [inst : CommSemiring R] → [StarRing R] → RingAut R
-- Mathlib.Analysis.Convex.StrictCombination
norm_sum_lt_of_strictConvexSpace : ∀ {V : Type u_2} {ι : Type u_4} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [StrictConvexSpace ℝ V]
  {t : Finset ι} {w : ι → ℝ} {r : ℝ} {z : ι → V},
  (∀ i ∈ t, 0 ≤ w i) →
    ∑ i ∈ t, w i = 1 →
      ∀ {i j : ι}, i ∈ t → j ∈ t → z i ≠ z j → w i ≠ 0 → w j ≠ 0 → (∀ i ∈ t, ‖z i‖ ≤ r) → ‖∑ k ∈ t, w k • z k‖ < r
-- Mathlib.CategoryTheory.Action.Monoidal
Action.tensorHom_hom : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G]
  [inst_2 : CategoryTheory.MonoidalCategory V] {X₁ Y₁ X₂ Y₂ : Action V G} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂),
  (CategoryTheory.MonoidalCategoryStruct.tensorHom f g).hom =
    CategoryTheory.MonoidalCategoryStruct.tensorHom f.hom g.hom
-- Init.Data.UInt.Lemmas
UInt8.ofBitVec_uInt32ToBitVec : ∀ (n : UInt32), { toBitVec := BitVec.setWidth 8 n.toBitVec } = n.toUInt8
-- Mathlib.Algebra.Order.Floor.Defs
/-- See `exists_floor` for a variant which instead assumes an `Archimedean` ring.  -/
exists_floor' : ∀ {α : Type u_4} [inst : Ring α] [inst_1 : PartialOrder α] [IsOrderedRing α] [Nontrivial α] (x : α),
  (∃ n, ↑n ≤ x) → (∃ n, x ≤ ↑n) → ∃ fl, ∀ (z : ℤ), z ≤ fl ↔ ↑z ≤ x
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
AddSubsemigroup.opEquiv.eq_1 : ∀ {M : Type u_2} [inst : Add M],
  AddSubsemigroup.opEquiv =
    { toFun := AddSubsemigroup.op, invFun := AddSubsemigroup.unop, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
IntermediateField.fg_top_iff : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E],
  ⊤.FG ↔ Algebra.EssFiniteType F E
-- Mathlib.Order.Interval.Set.Basic
Set.Ioc_inter_Iic : ∀ {α : Type u_1} [inst : SemilatticeInf α] (a b c : α), Set.Ioc a b ∩ Set.Iic c = Set.Ioc a (b ⊓ c)
-- Mathlib.Analysis.Matrix.Normed
/-- Normed non-unital ring instance (using sup norm of L1 norm) for matrices over a normed
non-unital ring. Not declared as an instance because there are several natural choices for defining
the norm of a matrix.  -/
Matrix.linftyOpNonUnitalNormedRing : {n : Type u_4} → {α : Type u_5} → [Fintype n] → [NonUnitalNormedRing α] → NonUnitalNormedRing (Matrix n n α)
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
CategoryTheory.ChosenPullbacksAlong.snd'_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Y Z X : C} (f : Y ⟶ X) (g : Z ⟶ X)
  [inst_1 : CategoryTheory.ChosenPullbacksAlong g],
  CategoryTheory.Over.Hom.left (CategoryTheory.ChosenPullbacksAlong.snd' f g) =
    CategoryTheory.ChosenPullbacksAlong.snd f g
-- Mathlib.Data.Setoid.Basic
Setoid.quotient_mk_sInf_eq : ∀ {α : Type u_1} {S : Set (Setoid α)} {x y : α}, ⟦x⟧ = ⟦y⟧ ↔ ∀ s ∈ S, s x y
-- Mathlib.Algebra.Free
instReprFreeMagma : {α : Type u} → [Repr α] → Repr (FreeMagma α)
-- Mathlib.Order.Max
/-- **Alias** of the reverse direction of `isMax_ofDual_iff`. -/
IsMin.ofDual : ∀ {α : Type u_1} [inst : LE α] {a : αᵒᵈ}, IsMin a → IsMax (OrderDual.ofDual a)
-- Mathlib.Analysis.Analytic.WithLp
PiLp.analyticOn_ofLp : ∀ {𝕜 : Type u_1} {ι : Type u_2} [inst : Fintype ι] {E : ι → Type u_3} [inst_1 : NontriviallyNormedField 𝕜]
  [inst_2 : (i : ι) → NormedAddCommGroup (E i)] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)] (p : ENNReal)
  [inst_4 : Fact (1 ≤ p)] (s : Set (PiLp p E)), AnalyticOn 𝕜 WithLp.ofLp s
-- Mathlib.NumberTheory.LSeries.Convolution
/-- The L-series of the (convolution) product of two `ℂ`-valued arithmetic functions `f` and `g`
is summable when both L-series are summable.  -/
ArithmeticFunction.LSeriesSummable_mul : ∀ {f g : ArithmeticFunction ℂ} {s : ℂ},
  LSeriesSummable (fun n => f n) s → LSeriesSummable (fun n => g n) s → LSeriesSummable (fun n => (f * g) n) s
-- Qq.MatchImpl
Qq.Impl.PatVarDecl.mk.injEq : ∀ (ty : Option Q(Lean.Expr)) (fvarId : Lean.FVarId) (userName : Lean.Name) (ty_1 : Option Q(Lean.Expr))
  (fvarId_1 : Lean.FVarId) (userName_1 : Lean.Name),
  ({ ty := ty, fvarId := fvarId, userName := userName } = { ty := ty_1, fvarId := fvarId_1, userName := userName_1 }) =
    (ty = ty_1 ∧ fvarId = fvarId_1 ∧ userName = userName_1)
-- Mathlib.LinearAlgebra.Basis.Cardinality
/-- Over any ring `R`, if `b` is an infinite basis for a module `M`,
and `s` is a maximal linearly independent set,
then the cardinality of `b` is bounded by the cardinality of `s`.
 -/
infinite_basis_le_maximal_linearIndependent' : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [Nontrivial R] [inst_3 : Module R M]
  {ι : Type w} (b : Module.Basis ι R M) [Infinite ι] {κ : Type w'} (v : κ → M) (i : LinearIndependent R v),
  i.Maximal → Cardinal.lift.{w', w} (Cardinal.mk ι) ≤ Cardinal.lift.{w, w'} (Cardinal.mk κ)
-- Mathlib.Data.Sum.Order
Sum.instAntisymmLex_mathlib : ∀ {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) [Std.Antisymm r] [Std.Antisymm s],
  Std.Antisymm (Sum.Lex r s)
-- Lean.Parser.Term
Lean.Parser.Term.app.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
UniformContinuous.const_add : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : AddGroup α] [IsUniformAddGroup α]
  [inst_3 : UniformSpace β] {f : β → α}, UniformContinuous f → ∀ (a : α), UniformContinuous fun x => a + f x
-- Mathlib.RingTheory.Adjoin.Tower
/-- **Artin--Tate lemma**: if A ⊆ B ⊆ C is a chain of subrings of commutative rings, and
A is Noetherian, and C is algebra-finite over A, and C is module-finite over B,
then B is algebra-finite over A.

References: Atiyah--Macdonald Proposition 7.8; Altman--Kleiman 16.17.  -/
fg_of_fg_of_fg : ∀ (A : Type w) (B : Type u₁) (C : Type u_1) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : CommRing C]
  [inst_3 : Algebra A B] [inst_4 : Algebra B C] [inst_5 : Algebra A C] [IsScalarTower A B C] [IsNoetherianRing A],
  ⊤.FG → ⊤.FG → Function.Injective ⇑(algebraMap B C) → ⊤.FG
-- Mathlib.CategoryTheory.Presentable.Directed
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.tgt : ∀ {J : Type w} [inst : CategoryTheory.SmallCategory J] {κ : Cardinal.{w}}
  (self : CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram J κ) {i j : J} {f : i ⟶ j},
  self.W f → self.P j
-- Mathlib.Order.Antichain
IsAntichain.preimage_iso_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : LE α] [inst_1 : LE β] {t : Set β} {φ : α ≃o β},
  IsAntichain (fun x1 x2 => x1 ≤ x2) (⇑φ ⁻¹' t) ↔ IsAntichain (fun x1 x2 => x1 ≤ x2) t
-- Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
FirstOrder.Field.realize_genericMonicPolyHasRoot : ∀ {K : Type u_1} [inst : Field K] [inst_1 : FirstOrder.Ring.CompatibleRing K] (n : ℕ),
  K ⊨ FirstOrder.Field.genericMonicPolyHasRoot n ↔
    ∀ (p : { p // p.Monic ∧ p.natDegree = n }), ∃ x, Polynomial.eval x ↑p = 0
-- Mathlib.Topology.EMetricSpace.Lipschitz
LipschitzWith.edist_le_mul : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {K : NNReal} {f : α → β},
  LipschitzWith K f → ∀ (x y : α), edist (f x) (f y) ≤ ↑K * edist x y
-- Mathlib.MeasureTheory.Group.Convolution
/-- Convolution of the dirac measure at 0 with a measure μ returns μ.  -/
MeasureTheory.Measure.dirac_zero_conv : ∀ {M : Type u_1} [inst : AddMonoid M] [inst_1 : MeasurableSpace M] [MeasurableAdd₂ M] (μ : MeasureTheory.Measure M)
  [MeasureTheory.SFinite μ], (MeasureTheory.Measure.dirac 0).conv μ = μ
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.cast_symm_apply : ∀ {ι : Type u_7} {R : ι → Type u_8} [inst : (i : ι) → Mul (R i)] [inst_1 : (i : ι) → Add (R i)] {i j : ι} (h : i = j)
  (a : R j), (RingEquiv.cast h).symm a = cast ⋯ a
-- Mathlib.Topology.EMetricSpace.Lipschitz
LipschitzWith.pow_end : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {f : Function.End α} {K : NNReal},
  LipschitzWith K f → ∀ (n : ℕ), LipschitzWith (K ^ n) (f ^ n)
-- Std.Data.HashMap.Lemmas
Std.HashMap.isEmpty_alter_eq_isEmpty_erase : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α}
  {f : Option β → Option β}, (m.alter k f).isEmpty = ((m.erase k).isEmpty && (f m[k]?).isNone)
-- Mathlib.Data.Finset.Disjoint
Disjoint.forall_ne_finset : ∀ {α : Type u_2} {s t : Finset α} {a b : α}, Disjoint s t → a ∈ s → b ∈ t → a ≠ b
-- Lean.Environment
/-- Check if `ty = ∀ ..., p xs...` and `p : ∀ args..., Prop` where `xs` and `args` are of the same
length.
 -/
_private.Lean.Environment.0.Lean.subsumesInfo.isPropCheap : Std.HashMap Lean.Name Lean.ConstantInfo → Lean.Expr → Bool
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
_private.Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected.0.SimpleGraph.ConnectedComponent.walk_toSimpleGraph.eq_def : ∀ {V : Type u} {G : SimpleGraph V} (C : G.ConnectedComponent) {u v : V} (hu : u ∈ C) (hv : v ∈ C) (p : G.Walk u v),
  SimpleGraph.ConnectedComponent.walk_toSimpleGraph✝ C hu hv p =
    SimpleGraph.Walk.casesOn (motive := fun a a_1 t => u = a → v = a_1 → p ≍ t → C.toSimpleGraph.Walk ⟨u, hu⟩ ⟨v, hv⟩) p
      (fun {u_1} h =>
        Eq.ndrec (motive := fun {u_2} => v = u_2 → p ≍ SimpleGraph.Walk.nil → C.toSimpleGraph.Walk ⟨u, hu⟩ ⟨v, hv⟩)
          (fun h =>
            Eq.ndrec (motive := fun {v} =>
              (hv : v ∈ C) → (p : G.Walk u v) → p ≍ SimpleGraph.Walk.nil → C.toSimpleGraph.Walk ⟨u, hu⟩ ⟨v, hv⟩)
              (fun hv p h => SimpleGraph.Walk.nil) ⋯ hv p)
          h)
      (fun {v_1 w u_1} h p_1 h_1 =>
        Eq.ndrec (motive := fun {v_2} =>
          (h : G.Adj v_2 w) → v = u_1 → p ≍ SimpleGraph.Walk.cons h p_1 → C.toSimpleGraph.Walk ⟨u, hu⟩ ⟨v, hv⟩)
          (fun h h_2 =>
            Eq.ndrec (motive := fun {u_2} =>
              (p_2 : G.Walk w u_2) → p ≍ SimpleGraph.Walk.cons h p_2 → C.toSimpleGraph.Walk ⟨u, hu⟩ ⟨v, hv⟩)
              (fun p_2 h_3 =>
                have hw := ⋯;
                have h' := h;
                SimpleGraph.Walk.cons h' (SimpleGraph.ConnectedComponent.walk_toSimpleGraph✝ C hw hv p_2))
              h_2 p_1)
          h_1 h)
      ⋯ ⋯ ⋯
-- Mathlib.SetTheory.Cardinal.Aleph
Ordinal.preOmega_le_preOmega : ∀ {o₁ o₂ : Ordinal.{u_1}}, Ordinal.preOmega o₁ ≤ Ordinal.preOmega o₂ ↔ o₁ ≤ o₂
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.surjOn_cos : Set.SurjOn Real.cos (Set.Icc 0 Real.pi) (Set.Icc (-1) 1)
-- Mathlib.Data.EReal.Inv
EReal.strictMono_div_right_of_pos : ∀ {b : EReal}, 0 < b → b ≠ ⊤ → StrictMono fun a => a / b
-- Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
WithIdeal.instIsLinearTopology : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : WithIdeal R], IsLinearTopology R R
-- Mathlib.Algebra.Category.Semigrp.Basic
AddMagmaCat.coe_id : ∀ {X : AddMagmaCat}, ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) = id
-- Mathlib.Analysis.Normed.Module.FiniteDimension
/-- In an infinite-dimensional normed space, there exists a sequence of points which are all
bounded by `R` and at distance at least `1`. For a version not assuming `c` and `R`, see
`exists_seq_norm_le_one_le_norm_sub`.  -/
exists_seq_norm_le_one_le_norm_sub' : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type v} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [CompleteSpace 𝕜] {c : 𝕜},
  1 < ‖c‖ →
    ∀ {R : ℝ}, ‖c‖ < R → ¬FiniteDimensional 𝕜 E → ∃ f, (∀ (n : ℕ), ‖f n‖ ≤ R) ∧ Pairwise fun m n => 1 ≤ ‖f m - f n‖
-- Std.Time.Format.Modifier
/-- `classify` classifies the number of pattern letters into a `Text` type.
 -/
Std.Time.Text.classify : ℕ → Option Std.Time.Text
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.instIntCastIdOfIsTopologicalAddGroup : {R : Type u_1} →
  [inst : Ring R] →
    {M : Type u_4} →
      [inst_1 : TopologicalSpace M] →
        [inst_2 : AddCommGroup M] → [inst_3 : Module R M] → [IsTopologicalAddGroup M] → IntCast (M →L[R] M)
-- Mathlib.Algebra.Module.LinearMap.FiniteRange
LinearMap.HasFiniteRange.hasNoetherianRange : ∀ {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} [inst : Ring K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [inst_3 : AddCommGroup V₂] [inst_4 : Module K V₂] [IsNoetherianRing K] {u : V →ₗ[K] V₂},
  u.HasFiniteRange → u.HasNoetherianRange
-- Mathlib.Data.ENat.Lattice
ENat.iSup_natCast_eq_top : ∀ {ι : Sort u_1} {f : ι → ℕ}, ⨆ i, ↑(f i) = ⊤ ↔ ¬BddAbove (Set.range f)
-- Mathlib.Data.List.Sigma
List.lookupAll_nil : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (a : α), List.lookupAll a [] = []
-- Std.Data.Iterators.Lemmas.Producers.Vector
_private.Std.Data.Iterators.Lemmas.Producers.Vector.0.Std.Iterators.Types.ArrayIterator.instIterator.match_1.splitter : {m : Type u_1 → Type u_2} →
  {α : Type u_1} →
    (motive : Std.IterStep (Std.IterM m α) α → Sort u_3) →
      (x : Std.IterStep (Std.IterM m α) α) →
        ((it' : Std.IterM m α) → (out : α) → motive (Std.IterStep.yield it' out)) →
          ((it : Std.IterM m α) → motive (Std.IterStep.skip it)) → (Unit → motive Std.IterStep.done) → motive x
-- Mathlib.Algebra.Group.AddChar
AddChar.eq_one_iff : ∀ {A : Type u_1} {M : Type u_3} [inst : AddMonoid A] [inst_1 : Monoid M] {ψ : AddChar A M}, ψ = 1 ↔ ∀ (x : A), ψ x = 1
-- Mathlib.Algebra.Notation.Prod
Prod.instSub.eq_1 : ∀ {G : Type u_8} {H : Type u_9} [inst : Sub G] [inst_1 : Sub H],
  Prod.instSub = { sub := fun p q => (p.1 - q.1, p.2 - q.2) }
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Polynomial.Chebyshev.node_eq_neg_one : ∀ {n : ℕ}, n ≠ 0 → Polynomial.Chebyshev.node n n = -1
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.Hom.isoOpensRange_inv_comp_assoc : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.IsOpenImmersion f]
  {Z : AlgebraicGeometry.Scheme} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.isoOpensRange f).inv
      (CategoryTheory.CategoryStruct.comp f h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.opensRange f).ι h
-- Mathlib.Algebra.Order.Interval.Set.Instances
Set.Ico.instCommSemigroup : {R : Type u_2} → [inst : CommSemiring R] → [inst_1 : PartialOrder R] → [IsOrderedRing R] → CommSemigroup ↑(Set.Ico 0 1)
-- Lean.Meta.WHNF
_private.Lean.Meta.WHNF.0.Lean.Meta.isRecStuck? : Lean.RecursorVal → Array Lean.Expr → Lean.MetaM (Option Lean.MVarId)
-- Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
CategoryTheory.FunctorToTypes.binaryProductLimit_lift : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F G : CategoryTheory.Functor C (Type w))
  (s : CategoryTheory.Limits.BinaryFan F G),
  (CategoryTheory.FunctorToTypes.binaryProductLimit F G).lift s = CategoryTheory.FunctorToTypes.prod.lift s.fst s.snd
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.ChangeOfRings
/-- The restriction of scalars functor `PresheafOfModules R' ⥤ PresheafOfModules R`
induced by a morphism of presheaves of rings `R ⟶ R'`.  -/
PresheafOfModules.restrictScalars : {C : Type u'} →
  [inst : CategoryTheory.Category.{v', u'} C] →
    {R R' : CategoryTheory.Functor Cᵒᵖ RingCat} →
      (R ⟶ R') → CategoryTheory.Functor (PresheafOfModules R') (PresheafOfModules R)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
/-- The commutator of `G` as a morphism. This is the map `(x, y) ↦ x * y * x⁻¹ * y⁻¹`,
see `CategoryTheory.GrpObj.lift_commutator_eq_mul_mul_inv_inv`.
This morphism is constant with value `1` if and only if `G` is commutative
(see `CategoryTheory.isCommMonObj_iff_commutator_eq_toUnit_η`).  -/
CategoryTheory.GrpObj.commutator : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      (G : C) → [CategoryTheory.GrpObj G] → CategoryTheory.MonoidalCategoryStruct.tensorObj G G ⟶ G
-- Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
modularCyclotomicCharacter.spec : ∀ (L : Type u) [inst : CommRing L] [inst_1 : IsDomain L] {n : ℕ} [inst_2 : NeZero n]
  (hn : Nat.card ↥(rootsOfUnity n L) = n) (g : L ≃+* L) {t : Lˣ},
  t ∈ rootsOfUnity n L → g ↑t = ↑t ^ (↑((modularCyclotomicCharacter L hn) g)).val
-- Mathlib.NumberTheory.Cyclotomic.Basic
CyclotomicRing.instIsScalarTowerCyclotomicField : ∀ (n : ℕ) (A : Type u) (K : Type w) [inst : CommRing A] [inst_1 : Field K] [inst_2 : Algebra A K],
  IsScalarTower A (CyclotomicRing n A K) (CyclotomicField n K)
-- Init.Data.Rat.Basic
/-- Construct a rational number from a numerator and denominator.
This is a "smart constructor" that divides the numerator and denominator by
the gcd to ensure that the resulting rational number is normalized, and returns
zero if `den` is zero.
 -/
mkRat : ℤ → ℕ → ℚ
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap.0.List.filterMap.match_1.eq_1 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (h_1 : Unit → motive none) (h_2 : (b : β) → motive (some b)),
  (match none with
    | none => h_1 ()
    | some b => h_2 b) =
    h_1 ()
-- Mathlib.Algebra.Order.Module.Basic
inf_eq_half_smul_add_sub_abs_sub' : ∀ (𝕜 : Type u_1) {M : Type u_3} [inst : DivisionSemiring 𝕜] [NeZero 2] [inst_2 : Lattice M] [inst_3 : AddCommGroup M]
  [inst_4 : Module 𝕜 M] [IsOrderedAddMonoid M] (x y : M), x ⊓ y = 2⁻¹ • (x + y - |y - x|)
-- Mathlib.Combinatorics.Quiver.Covering
/-- The costar of the symmetrification of a quiver at a vertex `u` is equivalent to the sum of the
costar and the star at `u` in the original quiver.  -/
Quiver.symmetrifyCostar : {U : Type u_1} →
  [inst : Quiver U] → (u : U) → Quiver.Costar (Quiver.Symmetrify.of.obj u) ≃ Quiver.Costar u ⊕ Quiver.Star u
-- Mathlib.Algebra.Group.Defs
one_pow : ∀ {M : Type u_2} [inst : Monoid M] (n : ℕ), 1 ^ n = 1
-- Init.Data.SInt.Basic
/-- Bitwise left shift for 16-bit signed integers. Usually accessed via the `<<<` operator.

Signed integers are interpreted as bitvectors according to the two's complement representation.

This function is overridden at runtime with an efficient implementation.
 -/
Int16.shiftLeft : Int16 → Int16 → Int16