mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Localization.Submodule
IsLocalization.coeSubmodule_span : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Type u_2) [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (s : Set R),
  IsLocalization.coeSubmodule S (Ideal.span s) = Submodule.span R (⇑(algebraMap R S) '' s)
-- Mathlib.ModelTheory.Basic
/-- A first-order language consists of a type of functions of every natural-number arity and a
type of relations of every natural-number arity.  -/
FirstOrder.Language : Type (max (u + 1) (v + 1))
-- Mathlib.CategoryTheory.GradedObject
/-- Given maps `p : I → J`, `q : J → K` and `r : I → K` such that `q.comp p = r`,
`X : GradedObject I C`, `k : K`, the datum of cofans `X.CofanMapObjFun p j` for all
`j : J` and of a cofan for all the points of these cofans, this is a cofan of
type `X.CofanMapObjFun r k`, which is a colimit (see `isColimitCofanMapObjComp`) if the
given cofans are.  -/
CategoryTheory.GradedObject.cofanMapObjComp : {I : Type u_1} →
  {J : Type u_2} →
    {K : Type u_3} →
      {C : Type u_4} →
        [inst : CategoryTheory.Category.{v_1, u_4} C] →
          (X : CategoryTheory.GradedObject I C) →
            (p : I → J) →
              (q : J → K) →
                (r : I → K) →
                  (∀ (i : I), q (p i) = r i) →
                    (k : K) →
                      (c : (j : J) → q j = k → X.CofanMapObjFun p j) →
                        (CategoryTheory.Limits.Cofan fun j => (c ↑j ⋯).pt) → X.CofanMapObjFun r k
-- Mathlib.Topology.Sheaves.Over
TopologicalSpace.Opens.sheafEquivOver_counitIso_inv_app_hom_app : ∀ {X : Type u} [inst : TopologicalSpace X] (U : TopologicalSpace.Opens X) {A : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} A] (X_1 : CategoryTheory.Sheaf (Opens.grothendieckTopology ↥U) A)
  (X_2 : (TopologicalSpace.Opens ↥U)ᵒᵖ),
  (U.sheafEquivOver.counitIso.inv.app X_1).hom.app X_2 = X_1.obj.map (CategoryTheory.eqToHom ⋯).op
-- Init.System.ST
EST.Out : Type → Type → Type → Type
-- Mathlib.Analysis.BoxIntegral.UnitPartition
Equiv.smulRight.congr_simp : ∀ {α : Type u_4} {β : Type u_5} [inst : GroupWithZero α] [inst_1 : MulAction α β] {a a_1 : α} (e_a : a = a_1)
  (ha : a ≠ 0), Equiv.smulRight ha = Equiv.smulRight ⋯
-- Lean.Meta.Tactic.Grind.Arith.Linear.StructId
_private.Lean.Meta.Tactic.Grind.Arith.Linear.StructId.0.Lean.Meta.Grind.Arith.Linear.addZeroLtOne : Lean.Grind.Linarith.Var → Lean.Meta.Grind.Arith.Linear.LinearM Unit
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.sumRingEquiv_symm_C_X : ∀ (R : Type u) (S₁ : Type v) (S₂ : Type w) [inst : CommSemiring R] (s : S₂),
  (MvPolynomial.sumRingEquiv R S₁ S₂).symm (MvPolynomial.C (MvPolynomial.X s)) = MvPolynomial.X (Sum.inr s)
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
/-- If either `α` or `β` has second-countable topology, then the open sets in `α × β` belong to the
product sigma-algebra.  -/
Prod.opensMeasurableSpace : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [OpensMeasurableSpace α]
  [inst_3 : TopologicalSpace β] [inst_4 : MeasurableSpace β] [OpensMeasurableSpace β]
  [h : SecondCountableTopologyEither α β], OpensMeasurableSpace (α × β)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonCallHierarchyIncomingCall : Lean.ToJson Lean.Lsp.CallHierarchyIncomingCall
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey?_filter_key : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] {f : α → Bool} {k : α},
  m.WF → (Std.DHashMap.Raw.filter (fun k x => f k) m).getKey? k = Option.filter f (m.getKey? k)
-- Std.Http.Data.Chunk
/-- Inserts a trailer header field from string name and value, panicking if either is invalid.
 -/
Std.Http.Trailer.insert! : Std.Http.Trailer → String → String → Std.Http.Trailer
-- Mathlib.Data.List.Cycle
_private.Mathlib.Data.List.Cycle.0.Cycle.decidableNontrivialCoe.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (x : α) (h_1 : Unit → motive []) (h_2 : (x : α) → motive [x])
  (h_3 : (x y : α) → (l : List α) → motive (x :: y :: l)),
  (match [x] with
    | [] => h_1 ()
    | [x] => h_2 x
    | x :: y :: l => h_3 x y l) =
    h_2 x
-- Lean.AuxRecursor
Lean.NoConfusionInfo.regular.injEq : ∀ (arity lhs rhs arity_1 lhs_1 rhs_1 : ℕ),
  (Lean.NoConfusionInfo.regular arity lhs rhs = Lean.NoConfusionInfo.regular arity_1 lhs_1 rhs_1) =
    (arity = arity_1 ∧ lhs = lhs_1 ∧ rhs = rhs_1)
-- Mathlib.Algebra.ContinuedFractions.Computation.Approximations
/-- Creates the simple continued fraction of a value.  -/
SimpContFract.of : {K : Type u_1} → K → [inst : Field K] → [inst_1 : LinearOrder K] → [FloorRing K] → SimpContFract K
-- Mathlib.CategoryTheory.Adjunction.Limits
/-- A right adjoint preserves limits.  -/
CategoryTheory.Adjunction.rightAdjoint_preservesLimits : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G),
  CategoryTheory.Limits.PreservesLimitsOfSize.{v, u, v₂, v₁, u₂, u₁} G
-- Mathlib.Algebra.Group.AddChar
AddChar.coe_prod : ∀ {ι : Type u_1} {A : Type u_2} {M : Type u_3} [inst : AddMonoid A] [inst_1 : CommMonoid M] (s : Finset ι)
  (ψ : ι → AddChar A M), ⇑(∏ i ∈ s, ψ i) = ∏ i ∈ s, ⇑(ψ i)
-- Std.Time.Format.Modifier
/-- Hour and minute with colon, with optional seconds, and "Z" for zero offset (e.g., "+01:30", "+01:30:15", "Z")
 -/
Std.Time.OffsetZ.hourMinuteSecondColon : Std.Time.OffsetZ
-- Mathlib.Algebra.Order.GroupWithZero.Defs
/-- **Alias** of `le_of_mul_le_mul_right`. -/
le_of_mul_le_mul_of_pos_right : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] {a b c : α} [MulPosReflectLE α],
  b * a ≤ c * a → 0 < a → b ≤ c
-- Mathlib.Algebra.Algebra.Opposite
AlgHom.toRingHom_unop : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (f : Aᵐᵒᵖ →ₐ[R] Bᵐᵒᵖ),
  (AlgHom.unop f).toRingHom = RingHom.unop f.toRingHom
-- Init.Data.Range.Polymorphic.Basic
Std.Rxo.size_pos_iff_lt : ∀ {α : Type u} [inst : LT α] [inst_1 : Std.PRange.UpwardEnumerable α] [inst_2 : Std.Rxo.HasSize α]
  [Std.Rxo.LawfulHasSize α] {lo hi : α}, 0 < Std.Rxo.HasSize.size lo hi ↔ lo < hi
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem?_toArray_roo_eq_some : ∀ {m n i : ℕ}, i < n - (m + 1) → (m<...n).toArray[i]? = some (m + 1 + i)
-- Mathlib.Algebra.Order.Group.Synonym
toDual_smul' : ∀ {β : Type u_2} {α : Type u_1} [inst : SMul β α] (b : β) (a : α), OrderDual.toDual b • a = b • a
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
MeasureTheory.AECover.integrable_of_integral_norm_tendsto : ∀ {α : Type u_1} {ι : Type u_2} {E : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {l : Filter ι}
  [inst_1 : NormedAddCommGroup E] [l.NeBot] [l.IsCountablyGenerated] {φ : ι → Set α},
  MeasureTheory.AECover μ l φ →
    ∀ {f : α → E} (I : ℝ),
      (∀ (i : ι), MeasureTheory.IntegrableOn f (φ i) μ) →
        Filter.Tendsto (fun i => ∫ (x : α) in φ i, ‖f x‖ ∂μ) l (nhds I) → MeasureTheory.Integrable f μ
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.isCycle₂_of_mem_cycles₂ : ∀ {k G A : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : AddCommGroup A] [inst_3 : Module k A]
  [inst_4 : DistribMulAction G A] [inst_5 : SMulCommClass G k A],
  ∀ x ∈ groupHomology.cycles₂ (Rep.ofDistribMulAction k G A), groupHomology.IsCycle₂ x
-- Lean.Meta.Tactic.Grind.Intro
/-- Helper function for `mkCleanName`.
It ensures base name is a simple `Name` and does not have a `_<idx>` suffix
 -/
_private.Lean.Meta.Tactic.Grind.Intro.0.Lean.Meta.Grind.mkBaseName : Lean.Name → Lean.Expr → Lean.MetaM Lean.Name
-- Init.Data.PLift
instDecidableEqPLift.decEq : {α : Sort u_1} → [DecidableEq α] → (x x_1 : PLift α) → Decidable (x = x_1)
-- Std.Time.Format.Basic
Std.Time.instCoeStringFormatPart : Coe String Std.Time.FormatPart
-- Mathlib.LinearAlgebra.TensorProduct.Tower
LinearEquiv.coe_baseChange : ∀ (R : Type u_1) (A : Type u_2) (M : Type u_4) (N : Type u_5) [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : AddCommMonoid N] [inst_5 : Module R M]
  [inst_6 : Module R N] (f : M ≃ₗ[R] N), ↑(LinearEquiv.baseChange R A M N f) = LinearMap.baseChange A ↑f
-- Init.Tactics
/-- The arguments to the `simpa` family tactics.  -/
Lean.Parser.Tactic.simpaArgsRest : Lean.ParserDescr
-- Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
MeasureTheory.hasFiniteIntegral_congr : ∀ {α : Type u_1} {ε : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : ENorm ε] {f g : α → ε},
  f =ᵐ[μ] g → (MeasureTheory.HasFiniteIntegral f μ ↔ MeasureTheory.HasFiniteIntegral g μ)
-- Mathlib.Order.BooleanAlgebra.Set
Set.mem_sdiff_singleton : ∀ {α : Type u_1} {s : Set α} {a b : α}, a ∈ s \ {b} ↔ a ∈ s ∧ a ≠ b
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoMod_sub_zsmul' : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α) (m : ℤ), toIcoMod hp (a - m • p) b = toIcoMod hp a b - m • p
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
/-- The cycles in degree `i` of a homological complex.  -/
HomologicalComplex.cycles : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {ι : Type u_2} → {c : ComplexShape ι} → (K : HomologicalComplex C c) → (i : ι) → [K.HasHomology i] → C
-- Mathlib.RingTheory.Smooth.StandardSmoothCotangent
/-- If `P` is a submersive presentation, this is the section of the map
`I ⧸ I ^ 2 → ⊕ S dxᵢ` given by projecting to the summands indexed by `σ` and composing with the
inverse of `P.cotangentEquiv`.

By `SubmersivePresentation.sectionCotangent_comp` this is indeed a section.
 -/
Algebra.SubmersivePresentation.sectionCotangent : {R : Type u_1} →
  {S : Type u_2} →
    {ι : Type u_3} →
      {σ : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : CommRing S] →
            [inst_2 : Algebra R S] →
              [inst_3 : Finite σ] →
                (P : Algebra.SubmersivePresentation R S ι σ) →
                  P.toExtension.CotangentSpace →ₗ[S] P.toExtension.Cotangent
-- Mathlib.Analysis.SpecialFunctions.Integrals.Basic
/-- The integrand is chosen to match the conclusion of `Real.deriv_log_log`.  -/
integral_inv_div_log : ∀ {a b : ℝ}, 1 < a → 1 < b → ∫ (t : ℝ) in a..b, t⁻¹ / Real.log t = Real.log (Real.log b) - Real.log (Real.log a)
-- Mathlib.Algebra.Group.Basic
mul_mul_inv_mul_cancel : ∀ {G : Type u_3} [inst : Group G] (a b c : G), a * b * (b⁻¹ * c) = a * c
-- Init.Data.SInt.Lemmas
Int8.toISize_ofBitVec : ∀ (b : BitVec 8), (Int8.ofBitVec b).toISize = ISize.ofBitVec (BitVec.signExtend System.Platform.numBits b)
-- Lean.Meta.Closure
Lean.Meta.Closure.process : Lean.Meta.Closure.ClosureM Unit
-- Mathlib.Data.Set.Sigma
Set.sigma_union : ∀ {ι : Type u_1} {α : ι → Type u_3} {s : Set ι} {t₁ t₂ : (i : ι) → Set (α i)},
  (s.sigma fun i => t₁ i ∪ t₂ i) = s.sigma t₁ ∪ s.sigma t₂
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometry.dist_map : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P]
  [inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂] (f : P →ᵃⁱ[𝕜] P₂) (x y : P),
  dist (f x) (f y) = dist x y
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
AlgebraicGeometry.ΓSpec.isIso_adjunction_counit : CategoryTheory.IsIso AlgebraicGeometry.ΓSpec.adjunction.counit
-- Mathlib.Data.Setoid.Basic
Setoid.mk.congr_simp : ∀ {α : Sort u} (r r_1 : α → α → Prop) (e_r : r = r_1) (iseqv : Equivalence r),
  { r := r, iseqv := iseqv } = { r := r_1, iseqv := ⋯ }
-- Init.Data.Nat.Lcm
Nat.gcd_le_mul : ∀ {m n : ℕ}, 0 < m → 0 < n → m.gcd n ≤ m * n
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.map_apply_inl : ∀ {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [inst : MulOneClass M] [inst_1 : MulOneClass N]
  [inst_2 : MulOneClass M'] [inst_3 : MulOneClass N'] (f : M →* M') (g : N →* N') (x : M),
  (Monoid.Coprod.map f g) (Monoid.Coprod.inl x) = Monoid.Coprod.inl (f x)
-- Mathlib.Order.LiminfLimsup
/-- If `x ≤ Filter.liminf u atTop`, then for all `ε < 0`, there exists a positive natural
number `n` such that ` x + ε < u n`.  -/
Filter.exists_lt_of_le_liminf : ∀ {α : Type u_1} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : AddZeroClass α] [AddLeftStrictMono α] {x ε : α}
  {u : ℕ → α}, Filter.IsBoundedUnder GE.ge Filter.atTop u → x ≤ Filter.liminf u Filter.atTop → ε < 0 → ∃ n, x + ε < u ↑n
-- Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
AlgebraicGeometry.sourceAffineLocally_morphismRestrict : ∀ (P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) {X Y : AlgebraicGeometry.Scheme}
  (f : X ⟶ Y) (U : Y.Opens) (hU : AlgebraicGeometry.IsAffineOpen U),
  AlgebraicGeometry.sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] => P) (f ∣_ U) ↔
    ∀ (V : ↑X.affineOpens) (e : ↑V ≤ (TopologicalSpace.Opens.map f.base).obj U),
      P (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appLE f U (↑V) e))
-- Mathlib.Data.Set.Lattice
Set.compl_sUnion : ∀ {α : Type u_1} (S : Set (Set α)), (⋃₀ S)ᶜ = ⋂₀ (compl '' S)
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.instSemilatticeInf : {α : Type u} →
  {β : Type v} →
    [inst : TopologicalSpace α] →
      [inst_1 : NormedAddCommGroup β] →
        [inst_2 : Lattice β] →
          [HasSolidNorm β] → [IsOrderedAddMonoid β] → SemilatticeInf (BoundedContinuousFunction α β)
-- Lean.Meta.InferType
/-- `isPropQuick e` is an "approximate" predicate which returns `LBool.true`
if `e` is a proposition.
 -/
Lean.Meta.isPropQuick : Lean.Expr → Lean.MetaM Lean.LBool
-- Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
CochainComplex.mappingCone.triangle.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {K L : CochainComplex C ℤ} (φ : K ⟶ L),
  CochainComplex.mappingCone.triangle φ =
    CategoryTheory.Pretriangulated.Triangle.mk φ (CochainComplex.mappingCone.inr φ)
      ((-CochainComplex.mappingCone.fst φ).rightShift 1 0 CochainComplex.mappingCone.triangle._proof_3).homOf
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnSeries.coeff_single_mul_add : ∀ {Γ : Type u_1} {R : Type u_3} [inst : AddCommMonoid Γ] [inst_1 : PartialOrder Γ] [inst_2 : IsOrderedCancelAddMonoid Γ]
  [inst_3 : NonUnitalNonAssocSemiring R] {r : R} {x : HahnSeries Γ R} {a b : Γ},
  ((HahnSeries.single b) r * x).coeff (a + b) = r * x.coeff a
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.toENat_injOn : Set.InjOn (⇑Cardinal.toENat) (Set.Iic Cardinal.aleph0)
-- Std.Data.HashMap.Raw
/-- The notation `m[a]` or `m[a]'h` is preferred over calling this function directly.

Retrieves the mapping for the given key. Ensures that such a mapping exists by requiring a proof of
`a ∈ m`.
 -/
Std.HashMap.Raw.get : {α : Type u} → {β : Type v} → [inst : BEq α] → [inst_1 : Hashable α] → (m : Std.HashMap.Raw α β) → (a : α) → a ∈ m → β
-- Mathlib.Combinatorics.SimpleGraph.Basic
/-- The support of a graph is empty if there at most one vertex.  -/
SimpleGraph.support_of_subsingleton : ∀ {V : Type u} (G : SimpleGraph V) [Subsingleton V], G.support = ∅
-- Mathlib.GroupTheory.Torsion
/-- The `p`- and `q`-primary components are disjoint for `p ≠ q`.  -/
CommMonoid.primaryComponent.disjoint : ∀ {G : Type u_1} [inst : CommMonoid G] {p : ℕ} [hp : Fact (Nat.Prime p)] {p' : ℕ} [hp' : Fact (Nat.Prime p')],
  p ≠ p' → Disjoint (CommMonoid.primaryComponent G p) (CommMonoid.primaryComponent G p')
-- Mathlib.Analysis.Convex.Side
AffineSubspace.not_wOppSide_bot : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : CommRing R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P] (x y : P),
  ¬⊥.WOppSide x y
-- Mathlib.LinearAlgebra.Prod
LinearMap.prod_ext_iff : ∀ {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M] [inst_5 : Module R M₂]
  [inst_6 : Module R M₃] {f g : M × M₂ →ₗ[R] M₃},
  f = g ↔ f ∘ₗ LinearMap.inl R M M₂ = g ∘ₗ LinearMap.inl R M M₂ ∧ f ∘ₗ LinearMap.inr R M M₂ = g ∘ₗ LinearMap.inr R M M₂
-- Mathlib.Topology.SmallInductiveDimension
/-- A topological space has dimension `≤ n` if it has dimension `< n + 1`.  -/
HasSmallInductiveDimensionLE : (X : Type u_1) → [TopologicalSpace X] → ℕ → Prop
-- Mathlib.Algebra.ContinuedFractions.Basic
GenContFract.Pair.mk.inj : ∀ {α : Type u_1} {a b a_1 b_1 : α}, { a := a, b := b } = { a := a_1, b := b_1 } → a = a_1 ∧ b = b_1
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
/-- A predicate singling out infinite places among the absolute values on a number field `K`.  -/
NumberField.IsInfinitePlace : {K : Type u_1} → [inst : Field K] → AbsoluteValue K ℝ → Prop
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
CategoryTheory.ShortComplex.iCycles.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasLeftHomology], S.iCycles = S.leftHomologyData.i
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.isColoop_iff_forall_mem_closure_iff_mem : ∀ {α : Type u_1} {M : Matroid α} {e : α}, M.IsColoop e ↔ ∀ (X : Set α), e ∈ M.closure X ↔ e ∈ X
-- Lean.Parser.Term
/-- Logs a warning, tagging the message as a named diagnostic with the specified name and validating
that an associated error explanation exists. The error name must be followed by a `Syntax` at which
the warning is to be logged. The message is the final argument and may be passed as an interpolated
string or a `MessageData` term.
 -/
Lean.Parser.Term.logNamedWarningAtMacro : Lean.Parser.Parser
-- Mathlib.NumberTheory.Real.Irrational
Irrational.of_ratCast_div : ∀ (q : ℚ) {x : ℝ}, Irrational (↑q / x) → Irrational x
-- Mathlib.Geometry.Manifold.MFDeriv.FDeriv
/-- **Alias** of the forward direction of `hasMFDerivAt_iff_hasFDerivAt`. -/
HasMFDerivAt.hasFDerivAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {f : E → E'}
  {x : E} {f' : TangentSpace (modelWithCornersSelf 𝕜 E) x →L[𝕜] TangentSpace (modelWithCornersSelf 𝕜 E') (f x)},
  HasMFDerivAt% f x f' → HasFDerivAt f f' x
-- Mathlib.Data.Nat.Init
/-- **Alias** of `Nat.strongRec`. -/
Nat.strongRecOn' : {motive : ℕ → Sort u_1} → ((n : ℕ) → ((m : ℕ) → m < n → motive m) → motive n) → (t : ℕ) → motive t
-- Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
iteratedDeriv_smul_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {n : ℕ} {x : 𝕜} {𝔸 : Type u_5} [inst_3 : NormedRing 𝔸] [inst_4 : NormedAlgebra 𝕜 𝔸]
  [inst_5 : Module 𝔸 F] [IsBoundedSMul 𝔸 F] [IsScalarTower 𝕜 𝔸 F] {f : 𝕜 → 𝔸},
  ContDiffAt 𝕜 (↑n) f x → ∀ (v : F), iteratedDeriv n (fun y => f y • v) x = iteratedDeriv n f x • v
-- Lean.Elab.DocString
/-- The command elaboration scope stack.

These scopes are used when running commands inside of documentation. To keep examples
self-contained, these scopes are initialized for each doc comment as if it were the beginning
of a Lean file.
 -/
Lean.Doc.State.scopes : Lean.Doc.State → List Lean.Elab.Command.Scope
-- Mathlib.Analysis.InnerProductSpace.Orthonormal
LinearEquiv.isometryOfOrthonormal_toLinearEquiv : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_4} {E' : Type u_7} [inst_3 : SeminormedAddCommGroup E'] [inst_4 : InnerProductSpace 𝕜 E'] (f : E ≃ₗ[𝕜] E')
  {v : Module.Basis ι 𝕜 E} (hv : Orthonormal 𝕜 ⇑v) (hf : Orthonormal 𝕜 (⇑f ∘ ⇑v)),
  (f.isometryOfOrthonormal hv hf).toLinearEquiv = f
-- Mathlib.Algebra.Order.Module.Defs
OrderedSemiring.toSMulPosMonoNat : ∀ {α : Type u_1} [inst : Semiring α] [inst_1 : PartialOrder α] [IsOrderedRing α], SMulPosMono ℕ α
-- Mathlib.Topology.Convenient.Category
/-- The faithful functor `TopCat ⥤ ContinuousGeneratedByCat X` which sends
a topological space `Y` to the same type `Y`, with the same topology, but
considered as an object of `ContinuousGeneratedByCat X`.  -/
TopCat.toContinuousGeneratedByCat : {ι : Type t} →
  (X : ι → Type u) →
    [inst : (i : ι) → TopologicalSpace (X i)] → CategoryTheory.Functor TopCat (ContinuousGeneratedByCat X)
-- Mathlib.GroupTheory.Torsion
CommMonoid.mem_torsion : ∀ (G : Type u_1) [inst : CommMonoid G] (g : G), g ∈ CommMonoid.torsion G ↔ IsOfFinOrder g
-- Mathlib.Order.UpperLower.CompleteLattice
UpperSet.mem_iInf₂_iff : ∀ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_5} [inst : LE α] {a : α} {f : (i : ι) → κ i → UpperSet α},
  a ∈ ⨅ i, ⨅ j, f i j ↔ ∃ i j, a ∈ f i j
-- Mathlib.Algebra.Group.Subgroup.Pointwise
smul_coe_set : ∀ {G : Type u_2} {S : Type u_4} [inst : Group G] [inst_1 : SetLike S G] [SubgroupClass S G] {s : S} {a : G},
  a ∈ s → a • ↑s = ↑s
-- Mathlib.Combinatorics.Enumerative.DyckWord
DyckWord.mk.injEq : ∀ (toList : List DyckStep) (count_U_eq_count_D : List.count DyckStep.U toList = List.count DyckStep.D toList)
  (count_D_le_count_U :
    ∀ (i : ℕ), List.count DyckStep.D (List.take i toList) ≤ List.count DyckStep.U (List.take i toList))
  (toList_1 : List DyckStep) (count_U_eq_count_D_1 : List.count DyckStep.U toList_1 = List.count DyckStep.D toList_1)
  (count_D_le_count_U_1 :
    ∀ (i : ℕ), List.count DyckStep.D (List.take i toList_1) ≤ List.count DyckStep.U (List.take i toList_1)),
  ({ toList := toList, count_U_eq_count_D := count_U_eq_count_D, count_D_le_count_U := count_D_le_count_U } =
      { toList := toList_1, count_U_eq_count_D := count_U_eq_count_D_1, count_D_le_count_U := count_D_le_count_U_1 }) =
    (toList = toList_1)
-- Mathlib.Algebra.Order.Group.Finset
Finset.inf'_pow : ∀ {ι : Type u_1} {M : Type u_3} [inst : LinearOrder M] [inst_1 : Monoid M] [MulLeftMono M] [MulRightMono M]
  (s : Finset ι) (f : ι → M) (n : ℕ) (hs : s.Nonempty), s.inf' hs f ^ n = s.inf' hs fun a => f a ^ n
-- Mathlib.Algebra.Ring.Prod
RingEquiv.coe_prodComm_symm : ∀ {R : Type u_1} {S : Type u_3} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S],
  ⇑RingEquiv.prodComm.symm = Prod.swap
-- Lean.KeyedDeclsAttribute
Lean.KeyedDeclsAttribute.instInhabitedOLeanEntry : Inhabited Lean.KeyedDeclsAttribute.OLeanEntry
-- Mathlib.RingTheory.Congruence.Basic
RingCon.instSMulCommClassQuotient : ∀ {α : Type u_1} {β : Type u_2} {R : Type u_3} [inst : Add R] [inst_1 : MulOneClass R] [inst_2 : SMul α R]
  [inst_3 : IsScalarTower α R R] [inst_4 : SMul β R] [inst_5 : IsScalarTower β R R] (c : RingCon R)
  [SMulCommClass α β R], SMulCommClass α β c.Quotient
-- Mathlib.Algebra.Squarefree.Basic
squarefree_iff_no_irreducibles : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] [WfDvdMonoid R] {x : R},
  x ≠ 0 → (Squarefree x ↔ ∀ (p : R), Irreducible p → ¬p * p ∣ x)
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.ExBase.brecOn.go : {u : Lean.Level} →
  {α : Q(Type u)} →
    {BaseType : Q(«$α») → Type} →
      {sα : Q(CommSemiring «$α»)} →
        {motive_1 : (e : Q(«$α»)) → Mathlib.Tactic.Ring.Common.ExBase BaseType sα e → Sort u} →
          {motive_2 : (e : Q(«$α»)) → Mathlib.Tactic.Ring.Common.ExProd BaseType sα e → Sort u} →
            {motive_3 : (e : Q(«$α»)) → Mathlib.Tactic.Ring.Common.ExSum BaseType sα e → Sort u} →
              {e : Q(«$α»)} →
                (t : Mathlib.Tactic.Ring.Common.ExBase BaseType sα e) →
                  ((e : Q(«$α»)) → (t : Mathlib.Tactic.Ring.Common.ExBase BaseType sα e) → t.below → motive_1 e t) →
                    ((e : Q(«$α»)) → (t : Mathlib.Tactic.Ring.Common.ExProd BaseType sα e) → t.below → motive_2 e t) →
                      ((e : Q(«$α»)) → (t : Mathlib.Tactic.Ring.Common.ExSum BaseType sα e) → t.below → motive_3 e t) →
                        motive_1 e t ×' t.below