mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit
/-- `(G ⋙ lim).obj j` = `limit (G.obj j)` definitionally, so this
is just a variant of `limit_ext'`.  -/
CategoryTheory.Limits.comp_lim_obj_ext : ∀ {J : Type u₁} {K : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} J] [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  [inst_2 : Small.{v, u₂} K] {j : J} {G : CategoryTheory.Functor J (CategoryTheory.Functor K (Type v))}
  (x y : (G.comp CategoryTheory.Limits.lim).obj j),
  (∀ (k : K),
      (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.π (G.obj j) k)) x =
        (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.π (G.obj j) k)) y) →
    x = y
-- Mathlib.Combinatorics.Additive.DoublingConst
Finset.mulConst_empty_right : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] (A : Finset G), A.mulConst ∅ = 0
-- Mathlib.Topology.UniformSpace.UniformConvergence
UniformCauchySeqOn.uniformCauchySeqOnFilter : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : UniformSpace β] {F : ι → α → β} {s : Set α} {p : Filter ι},
  UniformCauchySeqOn F p s → UniformCauchySeqOnFilter F p (Filter.principal s)
-- Std.Internal.Do.PredTrans
Std.Internal.Do.PredTrans.mk.inj : ∀ {Pred : Type u} {EPred : Type v} {α : Type w} {apply apply_1 : (α → Pred) → EPred → Pred},
  { apply := apply } = { apply := apply_1 } → apply = apply_1
-- Mathlib.Algebra.Order.Monovary
antivaryOn_inv_right₀ : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : Semifield β] [inst_2 : LinearOrder β]
  [IsStrictOrderedRing β] {s : Set ι} {f : ι → α} {g : ι → β},
  (∀ i ∈ s, 0 < g i) → (AntivaryOn f g⁻¹ s ↔ MonovaryOn f g s)
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
LinearMap.adjoint_lTensor : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : InnerProductSpace 𝕜 G] [inst_7 : FiniteDimensional 𝕜 E]
  [inst_8 : FiniteDimensional 𝕜 F] [inst_9 : FiniteDimensional 𝕜 G] (f : E →ₗ[𝕜] F),
  LinearMap.adjoint (LinearMap.lTensor G f) = LinearMap.lTensor G (LinearMap.adjoint f)
-- Mathlib.GroupTheory.Rank
Subgroup.rank_congr : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G} [inst_1 : Group.FG ↥H] [inst_2 : Group.FG ↥K],
  H = K → Group.rank ↥H = Group.rank ↥K
-- Mathlib.CategoryTheory.ObjectProperty.LimitsClosure
CategoryTheory.ObjectProperty.instNonemptyLimitsClosure : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) {α : Type t}
  (J : α → Type u') [inst_1 : (a : α) → CategoryTheory.Category.{v', u'} (J a)] [P.Nonempty],
  (P.limitsClosure J).Nonempty
-- Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Submodule.le_orthogonal_iff_le_orthogonal : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {K₀ K₁ : Submodule 𝕜 E} [K₀.HasOrthogonalProjection] [K₁.HasOrthogonalProjection], K₀ ≤ K₁ᗮ ↔ K₁ ≤ K₀ᗮ
-- Mathlib.Topology.Algebra.Group.Quotient
QuotientGroup.isQuotientMap_mk : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Group G] (N : Subgroup G),
  Topology.IsQuotientMap QuotientGroup.mk
-- Mathlib.Topology.Algebra.Monoid.Defs
ContinuousOn.const_add : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : Add M] [SeparatelyContinuousAdd M] {X : Type u_2}
  [inst_3 : TopologicalSpace X] {f : X → M} {s : Set X}, ContinuousOn f s → ∀ (b : M), ContinuousOn (fun x => b + f x) s
-- Mathlib.Topology.MetricSpace.Pseudo.Constructions
NNReal.dist_eq : ∀ (a b : NNReal), dist a b = |↑a - ↑b|
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.solveElim.inj : ∀ {c₁ c₂ c₁_1 c₂_1 : Lean.Meta.Grind.Arith.Cutsat.DvdCnstr},
  Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.solveElim c₁ c₂ =
      Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.solveElim c₁_1 c₂_1 →
    c₁ = c₁_1 ∧ c₂ = c₂_1
-- Mathlib.Topology.Separation.Hausdorff
/-- There does not exist a nontrivial preirreducible T₂ space.  -/
not_preirreducible_nontrivial_t2 : ∀ (X : Type u_4) [inst : TopologicalSpace X] [PreirreducibleSpace X] [Nontrivial X] [T2Space X], False
-- Mathlib.Analysis.InnerProductSpace.l2Space
HilbertBasis.coe_mkOfOrthogonalEqBot : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : CompleteSpace E] {v : ι → E} (hv : Orthonormal 𝕜 v)
  (hsp : (Submodule.span 𝕜 (Set.range v))ᗮ = ⊥), ⇑(HilbertBasis.mkOfOrthogonalEqBot hv hsp) = v
-- Mathlib.Topology.Instances.AddCircle.Defs
/-- The image of the closed-open interval `[a, a + p)` under the quotient map `𝕜 → AddCircle p` is
the entire space.  -/
AddCircle.coe_image_Ioc_eq : ∀ {𝕜 : Type u_1} [inst : AddCommGroup 𝕜] (p : 𝕜) [inst_1 : LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)]
  (a : 𝕜) [Archimedean 𝕜], QuotientAddGroup.mk '' Set.Ioc a (a + p) = Set.univ
-- Mathlib.MeasureTheory.Integral.Asymptotics
/-- Let `f : X x Y → Z`. If as `y` tends to `l`, `f(x, y) = O(g(y))` uniformly on `s : Set X`
of finite measure, then the integral of `f` along `s` is `O(g(y))`.  -/
Asymptotics.IsBigO.set_integral_isBigO : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] {g : α → F} {l : Filter α} {ι : Type u_4}
  [inst_1 : MeasurableSpace ι] {f : ι × α → E} {s : Set ι} {μ : MeasureTheory.Measure ι} [inst_2 : NormedSpace ℝ E]
  [inst_3 : NormedAddCommGroup F],
  f =O[Filter.principal s ×ˢ l] (g ∘ Prod.snd) → μ s < ⊤ → (fun x => ∫ (i : ι) in s, f (i, x) ∂μ) =O[l] g
-- Std.Data.DHashMap.RawLemmas
/-- Simpler variant of `get!_filterMap` when `LawfulBEq` is available.  -/
Std.DHashMap.Raw.Const.get!_filterMap' : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {γ : Type w} {m : Std.DHashMap.Raw α fun x => β}
  [LawfulBEq α] [inst_3 : Inhabited γ] {f : α → β → Option γ} {k : α},
  m.WF →
    Std.DHashMap.Raw.Const.get! (Std.DHashMap.Raw.filterMap f m) k = ((Std.DHashMap.Raw.Const.get? m k).bind (f k)).get!
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getD_unitOfList : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {l : List α} {k : α} {fallback : Unit},
  (Std.HashMap.Raw.unitOfList l).getD k fallback = ()
-- Mathlib.Topology.Order.DenselyOrdered
interior_Ici' : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a : α},
  (Set.Iio a).Nonempty → interior (Set.Ici a) = Set.Ioi a
-- Mathlib.RingTheory.Ideal.Span
Ideal.mem_span_singleton_sup : ∀ {α : Type u} [inst : Semiring α] {x y : α} {I : Ideal α}, x ∈ Ideal.span {y} ⊔ I ↔ ∃ a, ∃ b ∈ I, a * y + b = x
-- Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
MeasureTheory.taylor_charFun_two : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P]
  {X : Ω → ℝ},
  AEMeasurable X P →
    ∫ (x : Ω), X x ∂P = 0 →
      ∫ (x : Ω), (X ^ 2) x ∂P = 1 →
        (fun t => MeasureTheory.charFun (MeasureTheory.Measure.map X P) t - (1 - ↑t ^ 2 / 2)) =o[nhds 0] fun t => t ^ 2
-- Mathlib.Topology.Category.FinTopCat
FinTopCat.instConcreteCategoryContinuousMapCarrierToTop : CategoryTheory.ConcreteCategory FinTopCat fun x1 x2 => C(↑x1.toTop, ↑x2.toTop)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.Slice.Pos.skip?_prop_eq_some_iff : ∀ {P : Char → Prop} [inst : DecidablePred P] {s : String.Slice} {pos res : s.Pos},
  pos.skip? P = some res ↔ ∃ (h : pos ≠ s.endPos), res = pos.next h ∧ P (pos.get h)
-- Mathlib.Data.Finsupp.PointwiseSMul
/-- **Alias** of `AddMonoidAlgebra.mem_vaddAntidiagonal_of_addGroup`. -/
Finsupp.mem_vaddAntidiagonal_of_addGroup : ∀ {G : Type u_1} {P : Type u_2} {R : Type u_3} {V : Type u_4} [inst : AddGroup G] [inst_1 : AddAction G P]
  [inst_2 : Semiring R] [inst_3 : Zero V] (f : AddMonoidAlgebra R G) (x : P → V) (p : P) (gh : G × P),
  gh ∈ Finset.VAddAntidiagonal p ⋯ ↔ f.coeff gh.1 ≠ 0 ∧ x gh.2 ≠ 0 ∧ gh.2 = -gh.1 +ᵥ p
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.preNatIso.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} D]
  (F : CategoryTheory.Functor C CategoryTheory.Cat) {G H : CategoryTheory.Functor D C} (α : G ≅ H),
  CategoryTheory.Grothendieck.preNatIso F α =
    CategoryTheory.NatIso.ofComponents
      (fun X => ({ base := G.obj X.base, fiber := X.fiber }.transportIso (α.app X.base)).symm) ⋯
-- Mathlib.Algebra.Star.StarRingHom
NonUnitalStarRingHom.ext : ∀ {A : Type u_1} {B : Type u_2} [inst : NonUnitalNonAssocSemiring A] [inst_1 : Star A]
  [inst_2 : NonUnitalNonAssocSemiring B] [inst_3 : Star B] {f g : A →⋆ₙ+* B}, (∀ (x : A), f x = g x) → f = g
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.mapAlongAddMonoidHom_apply : ∀ {ι₁ : Type u_3} {ι₂ : Type u_4} (R₁ : ι₁ → Type u_5) (R₂ : ι₂ → Type u_6) {𝓕₁ : Filter ι₁} {𝓕₂ : Filter ι₂}
  {S₁ : ι₁ → Type u_7} {S₂ : ι₂ → Type u_8} [inst : (i : ι₁) → SetLike (S₁ i) (R₁ i)]
  [inst_1 : (j : ι₂) → SetLike (S₂ j) (R₂ j)] {B₁ : (i : ι₁) → S₁ i} {B₂ : (j : ι₂) → S₂ j} (f : ι₂ → ι₁)
  (hf : Filter.Tendsto f 𝓕₂ 𝓕₁) [inst_2 : (i : ι₁) → AddMonoid (R₁ i)] [inst_3 : (i : ι₂) → AddMonoid (R₂ i)]
  [inst_4 : ∀ (i : ι₁), AddSubmonoidClass (S₁ i) (R₁ i)] [inst_5 : ∀ (i : ι₂), AddSubmonoidClass (S₂ i) (R₂ i)]
  (φ : (j : ι₂) → R₁ (f j) →+ R₂ j) (hφ : ∀ᶠ (j : ι₂) in 𝓕₂, Set.MapsTo ⇑(φ j) ↑(B₁ (f j)) ↑(B₂ j))
  (x : RestrictedProduct (fun i => R₁ i) (fun i => ↑(B₁ i)) 𝓕₁) (j : ι₂),
  ((RestrictedProduct.mapAlongAddMonoidHom R₁ R₂ f hf φ hφ) x) j = (φ j) (x (f j))
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.symm_mapAlgEquiv : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] (f : S ≃ₐ[R] T) (p : Polynomial S) (q : Polynomial T)
  (h : Associated (Polynomial.map (↑f) p) q),
  (AdjoinRoot.mapAlgEquiv f p q h).symm = AdjoinRoot.mapAlgEquiv f.symm q p ⋯
-- Mathlib.Topology.MetricSpace.ThickenedIndicator
continuous_thickenedIndicatorAux : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α] {δ : ℝ}, 0 < δ → ∀ (E : Set α), Continuous (thickenedIndicatorAux δ E)
-- Mathlib.Order.SuccPred.Basic
SuccOrder.ext : ∀ {α : Type u_3} {inst : Preorder α} {x y : SuccOrder α}, SuccOrder.succ = SuccOrder.succ → x = y
-- Mathlib.Data.Nat.ModEq
Nat.le_mod_add_mod_of_dvd_add_of_not_dvd : ∀ {a b c : ℕ}, c ∣ a + b → ¬c ∣ a → c ≤ a % c + b % c
-- Mathlib.Logic.Function.Basic
Function.Surjective.of_comp_iff' : ∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β},
  Function.Bijective f → ∀ (g : γ → α), Function.Surjective (f ∘ g) ↔ Function.Surjective g
-- Init.Core
/-- `LawfulLeftIdentity op o` indicates `o` is a verified left identity of
`op`.
 -/
Std.LawfulLeftIdentity : {α : Sort u} → {β : Sort u_1} → (α → β → β) → outParam α → Prop
-- Init.Data.SInt.Lemmas
Int16.neg_neg : ∀ {a : Int16}, - -a = a
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
Std.DHashMap.Internal.AssocList.getEntryD_eq : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l : Std.DHashMap.Internal.AssocList α β} {a : α}
  {fallback : (a : α) × β a},
  Std.DHashMap.Internal.AssocList.getEntryD a fallback l = Std.Internal.List.getEntryD a fallback l.toList
-- Mathlib.Algebra.Homology.HomologicalComplex
ChainComplex.of_d : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  {α : Type u_2} [inst_2 : AddRightCancelSemigroup α] [inst_3 : One α] [inst_4 : DecidableEq α] (X : α → V)
  (d : (n : α) → X (n + 1) ⟶ X n) (j : α), ChainComplex.of.d X d (j + 1) j = d j
-- Mathlib.CategoryTheory.Limits.Cones
/-- A morphism between the (co)vertex objects in `C`  -/
CategoryTheory.Limits.CoconeMorphism.hom : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          {A B : CategoryTheory.Limits.Cocone F} → CategoryTheory.Limits.CoconeMorphism A B → (A.pt ⟶ B.pt)
-- Mathlib.Analysis.LocallyConvex.BalancedCoreHull
balancedCore_balanced : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E] (s : Set E), Balanced 𝕜 (balancedCore 𝕜 s)
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RcoSliceData.mk : {α : Type u} →
  {β : α → Type v} →
    [inst : Ord α] → Std.DTreeMap.Internal.Impl α β → Std.Rco α → Std.DTreeMap.Internal.RcoSliceData α β
-- Mathlib.Order.Hom.Lattice
instCoeTCInfHomOfInfHomClass : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : FunLike F α β] → [inst_1 : Min α] → [inst_2 : Min β] → [InfHomClass F α β] → CoeTC F (InfHom α β)
-- Lean.Linter.UnusedVariables
/-- The set of `FVarId`s that are used directly. These may or may not be aliases.  -/
Lean.Linter.UnusedVariables.References.fvarUses : Lean.Linter.UnusedVariables.References → Std.HashSet Lean.FVarId
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Iso.isoInverseOfIsoFunctor_isoFunctorOfIsoInverse : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {G G' : C ≌ D} (i : G.inverse ≅ G'.inverse), i.isoFunctorOfIsoInverse.isoInverseOfIsoFunctor = i
-- Init.Data.UInt.Bitwise
UInt8.and_le_left : ∀ {a b : UInt8}, a &&& b ≤ a
-- Mathlib.Tactic.Sat.FromLRAT
/-- Parse a natural number  -/
Mathlib.Tactic.Sat.Parser.parseNat : Std.Internal.Parsec.String.Parser ℕ
-- Mathlib.Data.Set.Lattice.Image
Set.mapsTo_iUnion₂_iUnion₂ : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_8} {s : (i : ι) → κ i → Set α}
  {t : (i : ι) → κ i → Set β} {f : α → β},
  (∀ (i : ι) (j : κ i), Set.MapsTo f (s i j) (t i j)) → Set.MapsTo f (⋃ i, ⋃ j, s i j) (⋃ i, ⋃ j, t i j)
-- Mathlib.Order.Defs.PartialOrder
instTransGEGT : {α : Type u_1} → [inst : Preorder α] → Trans GE.ge GT.gt GT.gt
-- Mathlib.MeasureTheory.Measure.Haar.NormedSpace
MeasureTheory.Measure.integral_comp_div : ∀ {F : Type u_2} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] (g : ℝ → F) (a : ℝ),
  ∫ (x : ℝ), g (x / a) = |a| • ∫ (y : ℝ), g y
-- Mathlib.Control.Traversable.Instances
List.traverse_append : ∀ {F : Type u → Type u} [inst : Applicative F] {α' β' : Type u} (f : α' → F β') [LawfulApplicative F] (as bs : List α'),
  traverse f (as ++ bs) = (fun x1 x2 => x1 ++ x2) <$> traverse f as <*> traverse f bs
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Zero.state : {α : Type} → Std.CloseableChannel.Zero✝ α → Std.Mutex (Std.CloseableChannel.Zero.State✝ α)
-- Mathlib.Analysis.Complex.UnitDisc.Basic
/-- **Alias** of `Complex.UnitClosedDisc.coe_closedBall_smul`. -/
Complex.UnitClosedDisc.coe_smul_closedBall : ∀ (z : Complex.UnitClosedDisc) (w : Complex.UnitDisc), ↑(z • w) = ↑z * ↑w
-- Mathlib.LinearAlgebra.Matrix.StdBasis
Matrix.stdBasis.eq_1 : ∀ (R : Type u_1) (m : Type u_2) (n : Type u_3) [inst : Fintype m] [inst_1 : Finite n] [inst_2 : Semiring R],
  Matrix.stdBasis R m n =
    ((Pi.basis fun x => Pi.basisFun R n).reindex (Equiv.sigmaEquivProd m n)).map (Matrix.ofLinearEquiv R)
-- Mathlib.Analysis.RCLike.Basic
/-- The `ℝ → K` coercion, as a continuous linear map  -/
RCLike.ofRealCLM : {K : Type u_1} → [inst : RCLike K] → ℝ →L[ℝ] K
-- Lean.Widget.TaggedText
_private.Lean.Widget.TaggedText.0.Lean.Widget.TaggedText.instInhabitedTaggedState : Inhabited Lean.Widget.TaggedText.TaggedState✝
-- Mathlib.CategoryTheory.WithTerminal.Basic
/-- Lift a functor `F : C ⥤ D` to `WithInitial C ⥤ D`.  -/
CategoryTheory.WithInitial.lift : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} D] →
        {Z : D} →
          (F : CategoryTheory.Functor C D) →
            (M : (x : C) → Z ⟶ F.obj x) →
              (∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (M x) (F.map f) = M y) →
                CategoryTheory.Functor (CategoryTheory.WithInitial C) D
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.mul_def : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  (I J : FractionalIdeal S P), I * J = ⟨↑I * ↑J, ⋯⟩
-- Mathlib.Tactic.SetNotationForOrder
/-- Declare `∀ x ⊂ y, ...` as syntax for `∀ x, x ⊂ y → ...` and `∃ x ⊂ y, ...` as syntax for
`∃ x, x ⊂ y ∧ ...`  -/
Mathlib.Meta.SetNotationForOrder.«binderPred⊂_» : Lean.ParserDescr
-- Mathlib.GroupTheory.MonoidLocalization.Maps
AddSubmonoid.LocalizationMap.lift_apply : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N] {P : Type u_3}
  [inst_2 : AddCommMonoid P] (f : S.LocalizationMap N) {g : M →+ P} (hg : ∀ (y : ↥S), IsAddUnit (g ↑y)) (z : N),
  (f.lift hg) z = g (f.sec z).1 + ↑(-(IsAddUnit.liftRight (g.domRestrict S) hg) (f.sec z).2)
-- Mathlib.LinearAlgebra.Dimension.Basic
Module.le_rank_iff_exists_linearMap : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Nontrivial R] {n : ℕ},
  ↑n ≤ Module.rank R M ↔ ∃ f, Function.Injective ⇑f
-- Mathlib.Analysis.Calculus.FDeriv.Const
differentiableAt_one : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] [inst_7 : One F] (x : E), DifferentiableAt 𝕜 1 x
-- Mathlib.Tactic.ENatToNat
/-- `enat_to_nat` shifts all `ENat`s in the context to `Nat`, rewriting propositions about them.
A typical use case is `enat_to_nat; lia`.  -/
Mathlib.Tactic.ENatToNat.tacticEnat_to_nat : Lean.ParserDescr
-- Lean.ResolveName
Lean.isInaccessiblePrivateName : {m : Type → Type} →
  [Lean.MonadLog m] →
    [Lean.AddMessageContext m] → [Monad m] → [Lean.MonadEnv m] → [Lean.MonadOptions m] → Lean.Name → m Bool
-- Init.Data.Fin.Lemmas
Fin.coe_addNat : ∀ {n : ℕ} (m : ℕ) (i : Fin n), ↑(i.addNat m) = ↑i + m
-- Mathlib.CategoryTheory.MorphismProperty.Local
/-- **Alias** of `CategoryTheory.MorphismProperty.IsLocalAtTarget.iff_of_zeroHypercover`. -/
CategoryTheory.MorphismProperty.iff_of_zeroHypercover_target : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C}
  {K : CategoryTheory.Precoverage C} [P.IsLocalAtTarget K] {X Y : C} {f : X ⟶ Y} (𝒰 : K.ZeroHypercover Y)
  [inst_2 : K.HasPullbacks], P f ↔ ∀ (i : 𝒰.I₀), P (CategoryTheory.Limits.pullback.snd f (𝒰.f i))
-- Init.Data.UInt.Basic
USize.modn : USize → ℕ → USize
-- Mathlib.Data.Set.Equitable
Set.equitableOn_singleton : ∀ {α : Type u_1} {β : Type u_2} [inst : Semiring β] [inst_1 : PartialOrder β] [IsOrderedRing β] (a : α) (f : α → β),
  {a}.EquitableOn f
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.map_mapRange_eq_iff : ∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] (f : R →+* S₁)
  (g : S₁ → R) (hg : g 0 = 0) (φ : MvPolynomial σ S₁),
  (MvPolynomial.map f) (AddMonoidAlgebra.ofCoeff (Finsupp.mapRange g hg φ.coeff)) = φ ↔
    ∀ (d : σ →₀ ℕ), f (g (MvPolynomial.coeff d φ)) = MvPolynomial.coeff d φ
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.inhabited : {R₁ : Type u_1} →
  {R₂ : Type u_2} →
    [inst : Semiring R₁] →
      [inst_1 : Semiring R₂] →
        {σ₁₂ : R₁ →+* R₂} →
          {M₁ : Type u_4} →
            [inst_2 : TopologicalSpace M₁] →
              [inst_3 : AddCommMonoid M₁] →
                {M₂ : Type u_6} →
                  [inst_4 : TopologicalSpace M₂] →
                    [inst_5 : AddCommMonoid M₂] →
                      [inst_6 : Module R₁ M₁] → [inst_7 : Module R₂ M₂] → Inhabited (M₁ →SL[σ₁₂] M₂)
-- Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
MeasureTheory.Measure.QuasiMeasurePreserving.mk : ∀ {α : Type u_1} {β : Type u_2} {mβ : MeasurableSpace β} {m0 : MeasurableSpace α} {f : α → β}
  {μa : autoParam (MeasureTheory.Measure α) MeasureTheory.Measure.QuasiMeasurePreserving._auto_1}
  {μb : autoParam (MeasureTheory.Measure β) MeasureTheory.Measure.QuasiMeasurePreserving._auto_3},
  Measurable f →
    (MeasureTheory.Measure.map f μa).AbsolutelyContinuous μb → MeasureTheory.Measure.QuasiMeasurePreserving f μa μb
-- Lean.Elab.DefView
Lean.Elab.instBEqDefKind.beq : Lean.Elab.DefKind → Lean.Elab.DefKind → Bool
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
/-- Composition with a function on the right is a continuous linear map on Schwartz space
provided that the function is temperate and antilipschitz.  -/
SchwartzMap.compCLMOfAntilipschitz : (𝕜 : Type u_2) →
  {D : Type u_4} →
    {E : Type u_5} →
      {F : Type u_6} →
        [inst : NormedAddCommGroup E] →
          [inst_1 : NormedSpace ℝ E] →
            [inst_2 : NormedAddCommGroup F] →
              [inst_3 : NormedSpace ℝ F] →
                [inst_4 : RCLike 𝕜] →
                  [inst_5 : NormedAddCommGroup D] →
                    [inst_6 : NormedSpace ℝ D] →
                      [inst_7 : NormedSpace 𝕜 F] →
                        {K : NNReal} →
                          {g : D → E} →
                            Function.HasTemperateGrowth g →
                              AntilipschitzWith K g → SchwartzMap E F →L[𝕜] SchwartzMap D F
-- Init.Data.Vector.Count
Vector.count_le_count_push : ∀ {α : Type u_1} [inst : BEq α] {n : ℕ} {a b : α} {xs : Vector α n}, Vector.count a xs ≤ Vector.count a (xs.push b)
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.ToCodeBlock.ToForInTermResult.uvars : Lean.Elab.Term.Do.ToCodeBlock.ToForInTermResult → Array Lean.Elab.Term.Do.Var
-- Mathlib.NumberTheory.Harmonic.Bounds
harmonic_floor_le_one_add_log : ∀ (y : ℝ), 1 ≤ y → ↑(harmonic ⌊y⌋₊) ≤ 1 + Real.log y
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
NumberField.mixedEmbedding.logMap_one : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K], NumberField.mixedEmbedding.logMap 1 = 0
-- Mathlib.Algebra.Polynomial.Lifts
/-- The polynomial `X ^ n` lifts.  -/
Polynomial.X_pow_mem_lifts : ∀ {R : Type u} [inst : Semiring R] {S : Type v} [inst_1 : Semiring S] (f : R →+* S) (n : ℕ),
  Polynomial.X ^ n ∈ Polynomial.lifts f
-- Mathlib.Topology.IsClosedRestrict
Topology.reorderRestrictProd.eq_1 : ∀ {ι : Type u_1} {α : ι → Type u_2} (S : Set ι) (s : Set ((j : ι) → α j))
  (p : ↑(Sᶜ.domRestrict '' s) × ((i : ↑S) → α ↑i)) (j : ι),
  Topology.reorderRestrictProd S s p j = if h : j ∈ S then p.2 ⟨j, h⟩ else ↑p.1 ⟨j, h⟩
-- Lean.Parser.Term
Lean.Parser.Term.stateRefT.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Topology.Connected.PathConnected
ZerothHomotopy.rec : ∀ {X : Type u_1} [inst : TopologicalSpace X] {motive : ZerothHomotopy X → Prop},
  (∀ (x : X), motive (ZerothHomotopy.mk x)) → ∀ (x : ZerothHomotopy X), motive x
-- Mathlib.Topology.ContinuousMap.CocompactMap
CocompactMap.mk.sizeOf_spec : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : SizeOf α]
  [inst_3 : SizeOf β] (toContinuousMap : C(α, β))
  (cocompact_tendsto' : Filter.Tendsto toContinuousMap.toFun (Filter.cocompact α) (Filter.cocompact β)),
  sizeOf { toContinuousMap := toContinuousMap, cocompact_tendsto' := cocompact_tendsto' } = 1 + sizeOf toContinuousMap
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
Polynomial.roots_cyclotomic_nodup : ∀ {R : Type u_1} [inst : CommRing R] {n : ℕ} [inst_1 : IsDomain R] [NeZero ↑n], (Polynomial.cyclotomic n R).roots.Nodup
-- Mathlib.Analysis.Calculus.ContDiff.Defs
contDiffWithinAt_congr_of_insert : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f f₁ : E → F} {x : E} {n : WithTop ℕ∞},
  (∀ y ∈ insert x s, f₁ y = f y) → (ContDiffWithinAt 𝕜 n f₁ s x ↔ ContDiffWithinAt 𝕜 n f s x)
-- Mathlib.Data.Multiset.FinsetOps
Multiset.ndinter.eq_1 : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Multiset α), s.ndinter t = Multiset.filter (fun x => x ∈ t) s