mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Localization.FractionRing
IsFractionRing.div_surjective : ∀ (A : Type u_4) [inst : CommRing A] {K : Type u_5} [inst_1 : Field K] [inst_2 : Algebra A K] [IsFractionRing A K]
  (z : K), ∃ x, ∃ y ∈ nonZeroDivisors A, (algebraMap A K) x / (algebraMap A K) y = z
-- Mathlib.RingTheory.LocalIso
Algebra.IsLocalIso.mk : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S],
  (∀ (q : Ideal S) [q.IsPrime], ∃ g ∉ q, Algebra.IsStandardOpenImmersion R (Localization.Away g)) →
    Algebra.IsLocalIso R S
-- Mathlib.LinearAlgebra.Matrix.PosDef
Matrix.PosSemidef.trace_nonneg : ∀ {n : Type u_2} {R : Type u_3} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [inst_3 : Fintype n]
  [AddLeftMono R] {A : Matrix n n R}, A.PosSemidef → 0 ≤ A.trace
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Sentence.realize_inf : ∀ {L : FirstOrder.Language} (M : Type w) [inst : L.Structure M] {φ ψ : L.Sentence}, M ⊨ φ ⊓ ψ ↔ M ⊨ φ ∧ M ⊨ ψ
-- Mathlib.CategoryTheory.Sites.MorphismProperty
CategoryTheory.Precoverage.morphismProperty_le_iff_le_precoverage : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {K : CategoryTheory.Precoverage C}
  {P : CategoryTheory.MorphismProperty C}, K.morphismProperty ≤ P ↔ K ≤ P.precoverage
-- Mathlib.Order.Filter.AtTopBot.Ring
Filter.Tendsto.atTop_of_const_mul₀ : ∀ {α : Type u_1} {β : Type u_2} [inst : Semiring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {l : Filter β}
  {f : β → α} {c : α}, 0 < c → Filter.Tendsto (fun x => c * f x) l Filter.atTop → Filter.Tendsto f l Filter.atTop
-- Lean.Meta.MkIffOfInductiveProp
_private.Lean.Meta.MkIffOfInductiveProp.0.Lean.Meta.Shape.mk.sizeOf_spec : ∀ (variablesKept : List Bool) (neqs : Option ℕ),
  sizeOf { variablesKept := variablesKept, neqs := neqs } = 1 + sizeOf variablesKept + sizeOf neqs
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LetValue.pap.sizeOf_spec : ∀ {pu : Lean.Compiler.LCNF.Purity} (fn : Lean.Name) (args : Array (Lean.Compiler.LCNF.Arg pu))
  (h : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.LetValue._auto_15),
  sizeOf (Lean.Compiler.LCNF.LetValue.pap fn args h) = 1 + sizeOf fn + sizeOf args + sizeOf h
-- Lean.ProjFns
Lean.ProjectionFunctionInfo.mk.injEq : ∀ (ctorName : Lean.Name) (numParams i : ℕ) (fromClass : Bool) (ctorName_1 : Lean.Name) (numParams_1 i_1 : ℕ)
  (fromClass_1 : Bool),
  ({ ctorName := ctorName, numParams := numParams, i := i, fromClass := fromClass } =
      { ctorName := ctorName_1, numParams := numParams_1, i := i_1, fromClass := fromClass_1 }) =
    (ctorName = ctorName_1 ∧ numParams = numParams_1 ∧ i = i_1 ∧ fromClass = fromClass_1)
-- LeanSearchClient.LoogleSyntax
LeanSearchClient.LoogleResult.failure.sizeOf_spec : ∀ (error : String) (suggestions : Option (List String)),
  sizeOf (LeanSearchClient.LoogleResult.failure error suggestions) = 1 + sizeOf error + sizeOf suggestions
-- Lean.Language.Basic
Lean.Language.SnapshotLeaf.mk : Lean.Language.Snapshot → Lean.Language.SnapshotLeaf
-- Mathlib.Data.Nat.Factorization.Root
Nat.ceilRoot_one_right : ∀ {n : ℕ}, n ≠ 0 → n.ceilRoot 1 = 1
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.mem_alter_of_compare_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k k' : α} {f : Option (β k) → Option (β k)},
  cmp k k' = Ordering.eq → (k' ∈ t.alter k f ↔ (f (t.get? k)).isSome = true)
-- Std.Do.PostCond
Std.Do.PostCond.entails.eq_1 : ∀ {α : Type u_1} {ps : Std.Do.PostShape} (p q : Std.Do.PostCond α ps),
  p.entails q = ((∀ (a : α), p.1 a ⊢ₛ q.1 a) ∧ p.2.entails q.2)
-- Mathlib.Topology.MetricSpace.Isometry
IsometryClass.edist_eq : ∀ {F : Type u_1} {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β]
  [inst_2 : FunLike F α β] [IsometryClass F α β] (f : F) (x y : α), edist (f x) (f y) = edist x y
-- Init.Data.Dyadic.Inv
/-- For positive `a` and `b`, `divAtPrec a b prec` exceeds `a * invAtPrec b prec` by less than
`a * 2 ^ (-prec)`.
 -/
Dyadic.divAtPrec_sub_mul_lt_mul_invAtPrec : ∀ {a b : Dyadic},
  0 < a → 0 < b → ∀ (prec : ℤ), a.divAtPrec b prec - a * Dyadic.ofIntWithPrec 1 prec < a * b.invAtPrec prec
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp_id_right_hom_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.Pseudofunctor B C) {a b : B} (f : a ⟶ b) {Z : F.obj a ⟶ F.obj b}
  (h : CategoryTheory.CategoryStruct.comp (F.map f) (F.map (CategoryTheory.CategoryStruct.id b)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.mapComp f (CategoryTheory.CategoryStruct.id b)).hom h =
    CategoryTheory.CategoryStruct.comp (F.map₂ (CategoryTheory.Bicategory.rightUnitor f).hom)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor (F.map f)).inv
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (F.mapId b).inv) h))
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.measurePreserving_mul_left : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Mul G] [MeasurableMul G] (μ : MeasureTheory.Measure G)
  [μ.IsMulLeftInvariant] (g : G), MeasureTheory.MeasurePreserving (fun x => g * x) μ μ
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.degree_le_mul_left : ∀ {R : Type u} [inst : Semiring R] [NoZeroDivisors R] {q : Polynomial R} (p : Polynomial R),
  q ≠ 0 → p.degree ≤ (p * q).degree
-- Mathlib.Algebra.Ring.Subsemiring.Basic
RingHom.comp_restrict : ∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] {σR : Type u_1} {σS : Type u_2}
  [inst_2 : SetLike σR R] [inst_3 : SetLike σS S] [inst_4 : SubsemiringClass σR R] [inst_5 : SubsemiringClass σS S]
  (f : R →+* S) (s' : σR) (s : σS) (h : ∀ x ∈ s', f x ∈ s),
  (SubsemiringClass.subtype s).comp (f.restrict s' s h) = f.comp (SubsemiringClass.subtype s')
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
CategoryTheory.Limits.has_kernel_pair_of_mono : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Mono f],
  CategoryTheory.Limits.HasPullback f f
-- Mathlib.Combinatorics.Matroid.Dual
Matroid.dual_nonempty : ∀ {α : Type u_1} {M : Matroid α} [M.Nonempty], M✶.Nonempty
-- Init.Data.Nat.Dvd
Nat.mul_dvd_mul_left : ∀ {b c : ℕ} (a : ℕ), b ∣ c → a * b ∣ a * c
-- Mathlib.CategoryTheory.Linear.Basic
CategoryTheory.Linear.preadditiveIntLinear : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → [inst_1 : CategoryTheory.Preadditive C] → CategoryTheory.Linear ℤ C
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.Point.mk.congr_simp : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Affine R} [inst_1 : Nontrivial R]
  [inst_2 : WeierstrassCurve.IsElliptic W'] {x x_1 : R} (e_x : x = x_1) {y y_1 : R} (e_y : y = y_1)
  (h : W'.Equation x y), WeierstrassCurve.Affine.Point.mk h = WeierstrassCurve.Affine.Point.mk ⋯
-- Mathlib.Topology.Algebra.LinearTopology
/-- If `M` is a linearly topologized `R`-module and `i ↦ m i` tends to zero,
then `i ↦ a i • m i` still tends to zero for any family `a : ι → R`.  -/
IsLinearTopology.tendsto_smul_zero : ∀ (R : Type u_1) {M : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : TopologicalSpace M] [IsLinearTopology R M] {ι : Type u_4} {f : Filter ι} (a : ι → R) (m : ι → M),
  Filter.Tendsto m f (nhds 0) → Filter.Tendsto (a • m) f (nhds 0)
-- Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic
CategoryTheory.Types.instIsEquivalenceForgetTypeFun : (CategoryTheory.forget (Type u)).IsEquivalence
-- Init.Data.Int.DivMod.Lemmas
Int.dvd_sub_self_of_fmod_eq : ∀ {a b c : ℤ}, a.fmod b = c → b ∣ c - a
-- Std.Async.System
Std.Async.System.instInhabitedCPUInfo : Inhabited Std.Async.System.CPUInfo
-- Mathlib.Algebra.Group.Pointwise.Set.Finite
Set.Finite.vadd : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] {s : Set α} {t : Set β}, s.Finite → t.Finite → (s +ᵥ t).Finite
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
/-- If a set is a right-neighborhood of all of its points, then it is measurable.  -/
MeasurableSet.of_mem_nhdsGT : ∀ {α : Type u_1} [inst : TopologicalSpace α] {mα : MeasurableSpace α} [BorelSpace α] [inst_2 : LinearOrder α]
  [OrderTopology α] [SecondCountableTopology α] {s : Set α}, (∀ x ∈ s, s ∈ nhdsWithin x (Set.Ioi x)) → MeasurableSet s
-- Batteries.Data.List.Basic
/-- Auxiliary for `lookmap`: `lookmap.go f l acc = acc.toList ++ lookmap f l`.  -/
List.lookmap.go : {α : Type u_1} → (α → Option α) → List α → Array α → List α
-- Mathlib.Algebra.Homology.Embedding.AreComplementary
ComplexShape.Embedding.AreComplementary.isStrictlySupportedOutside₁_iff : ∀ {ι : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} {c : ComplexShape ι} {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  {C : Type u_4} [inst : CategoryTheory.Category.{v_1, u_4} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {e₁ : c₁.Embedding c} {e₂ : c₂.Embedding c},
  e₁.AreComplementary e₂ → ∀ (K : HomologicalComplex C c), K.IsStrictlySupportedOutside e₁ ↔ K.IsStrictlySupported e₂
-- Mathlib.Tactic.Simps.Basic
/-- The stem to use for the projection names. If `none`, the default, use the suffix of the
current declaration name, or the empty string if the declaration is an instance and the instance
is named according to the `inst` convention.  -/
Simps.Config.nameStem : Simps.Config → Option String
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.pow_toLinearMap : ∀ {R : Type uR} {A₁ : Type uA₁} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Algebra R A₁] (σ : A₁ ≃ₐ[R] A₁)
  (n : ℕ), (σ ^ n).toLinearMap = σ.toLinearMap ^ n
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
MeasureTheory.JordanDecomposition.mk : {α : Type u_2} →
  [inst : MeasurableSpace α] →
    (posPart negPart : MeasureTheory.Measure α) →
      [posPart_finite : MeasureTheory.IsFiniteMeasure posPart] →
        [negPart_finite : MeasureTheory.IsFiniteMeasure negPart] →
          posPart.MutuallySingular negPart → MeasureTheory.JordanDecomposition α
-- Init.Data.BitVec.Basic
/-- Append a single bit to the end of a bitvector, using big endian order (see `append`).
That is, the new bit is the least significant bit.  -/
BitVec.concat : {n : ℕ} → BitVec n → Bool → BitVec (n + 1)
-- Mathlib.Topology.VectorBundle.Riemannian
/-- In a continuous Riemannian bundle, the trivialization at a point is locally bounded in norm.  -/
eventually_norm_trivializationAt_lt : ∀ {B : Type u_1} [inst : TopologicalSpace B] (F : Type u_2) [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace ℝ F]
  (E : B → Type u_3) [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_4 : (x : B) → NormedAddCommGroup (E x)]
  [inst_5 : (x : B) → InnerProductSpace ℝ (E x)] [inst_6 : FiberBundle F E] [inst_7 : VectorBundle ℝ F E]
  [h : IsContinuousRiemannianBundle F E] (x : B),
  ∃ C > 0, ∀ᶠ (y : B) in nhds x, ‖Bundle.Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) y‖ < C
-- Mathlib.LinearAlgebra.Dimension.Basic
rank_le_of_isSMulRegular : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {S : Type u_1}
  [inst_3 : CommSemiring S] [inst_4 : Algebra S R] [inst_5 : Module S M] [IsScalarTower S R M] (L L' : Submodule R M)
  {s : S}, IsSMulRegular M s → (∀ x ∈ L, s • x ∈ L') → Module.rank R ↥L ≤ Module.rank R ↥L'
-- Lean.Meta.Match.CaseArraySizes
Lean.Meta.CaseArraySizesSubgoal.elems : Lean.Meta.CaseArraySizesSubgoal → Array Lean.FVarId
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.Ici_add_Ici_subset : ∀ {α : Type u_1} [inst : Add α] [inst_1 : Preorder α] [AddLeftMono α] [AddRightMono α] (a b : α),
  Set.Ici a + Set.Ici b ⊆ Set.Ici (a + b)
-- Init.Guard
/-- The `guard_hyp` type specifier, one of `:`, `:~`, `:ₛ`, `:ₐ`  -/
Lean.Parser.colon : Lean.ParserDescr
-- Mathlib.Analysis.Analytic.Composition
/-- Eta-expanded form of `AnalyticAt.comp_of_eq`

---

Version of `AnalyticAt.comp` where point equality is a separate hypothesis.  -/
AnalyticAt.fun_comp_of_eq : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {g : F → G} {f : E → F} {y : F} {x : E},
  AnalyticAt 𝕜 g y → AnalyticAt 𝕜 f x → f x = y → AnalyticAt 𝕜 (fun x => g (f x)) x
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.map₂IdIso.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {R : CategoryTheory.Functor C D} (T : D) (α : T ⟶ (CategoryTheory.Functor.id D).obj T)
  (β : R.comp (CategoryTheory.Functor.id D) ⟶ (CategoryTheory.Functor.id C).comp R)
  (hα : α = CategoryTheory.CategoryStruct.id T)
  (hβ : β = CategoryTheory.CategoryStruct.comp R.rightUnitor.hom R.leftUnitor.inv),
  CategoryTheory.StructuredArrow.map₂IdIso T α β hα hβ = CategoryTheory.StructuredArrow.map₂IdIso T α β hα hβ
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.cokernelSequenceOpcyclesE_exact : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃)
  (f₁₂ : i₀ ⟶ i₂) (h₁₂ : CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.cokernelSequenceOpcyclesE_exact._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.cokernelSequenceOpcyclesE_exact._auto_3),
  (X.cokernelSequenceOpcyclesE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).Exact
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.of_keysArray_unit_perm : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α Unit cmp}, t₁.keysArray.Perm t₂.keysArray → t₁.Equiv t₂
-- Mathlib.Order.Filter.Pointwise
Filter.NeBot.of_div_right : ∀ {α : Type u_2} [inst : Div α] {f g : Filter α}, (f / g).NeBot → g.NeBot
-- Init.Data.Range.Polymorphic.Internal.SignedBitVec
_private.Init.Data.Range.Polymorphic.Internal.SignedBitVec.0.BitVec.Signed.instRxiIsAlwaysFinite : ∀ {n : ℕ}, Std.Rxi.IsAlwaysFinite (BitVec n)
-- Mathlib.NumberTheory.Height.NumberField
NumberField.count_multisetInfinitePlace_eq_mult : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] [inst_2 : DecidableEq (AbsoluteValue K ℝ)]
  (v : NumberField.InfinitePlace K), Multiset.count (↑v) (NumberField.multisetInfinitePlace K) = v.mult
-- Mathlib.CategoryTheory.Bicategory.CatEnriched
CategoryTheory.CatEnriched.hComp_id : ∀ {C : Type u_1} [inst : CategoryTheory.EnrichedCategory CategoryTheory.Cat C] {a b : CategoryTheory.CatEnriched C}
  {f f' : a ⟶ b} (η : f ⟶ f'),
  CategoryTheory.CatEnriched.hComp η (CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.id b)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
      (CategoryTheory.CategoryStruct.comp η (CategoryTheory.eqToHom ⋯))
-- Mathlib.Algebra.Module.Submodule.LinearMap
LinearMap.restrict_eq_codRestrict_domRestrict : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  {f : M →ₛₗ[σ₁₂] M₂} {p : Submodule R M} {q : Submodule R₂ M₂} (hf : ∀ x ∈ p, f x ∈ q),
  f.restrict hf = LinearMap.codRestrict q (f.domRestrict p) ⋯
-- Mathlib.Topology.Algebra.AsymptoticCone
asymptoticCone_biUnion : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Field k] [inst_1 : LinearOrder k] [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] [inst_4 : AddTorsor V P] [inst_5 : TopologicalSpace V] {ι : Type u_4} {s : Set ι},
  s.Finite → ∀ (f : ι → Set P), asymptoticCone k (⋃ i ∈ s, f i) = ⋃ i ∈ s, asymptoticCone k (f i)
-- Mathlib.Computability.Encoding
/-- Deprecated alias for `unaryEncodingNat`.  -/
Computability.unaryFinEncodingNat : Computability.Encoding ℕ Bool
-- Mathlib.RingTheory.Ideal.Quotient.Defs
Ideal.Quotient.eq_zero_iff_mem : ∀ {R : Type u} [inst : Ring R] {I : Ideal R} {a : R} [inst_1 : I.IsTwoSided], (Ideal.Quotient.mk I) a = 0 ↔ a ∈ I
-- Mathlib.Topology.Sequences
/-- The preimage of a sequentially closed set under a sequentially continuous map is sequentially
closed.  -/
IsSeqClosed.preimage : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {s : Set Y},
  IsSeqClosed s → SeqContinuous f → IsSeqClosed (f ⁻¹' s)
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
/-- **Alias** of `Finset.card_vadd_finset_le`. -/
Finset.vadd_finset_card_le : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : VAdd α β] {s : Finset β} {a : α},
  (a +ᵥ s).card ≤ s.card
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
continuousOn_extChartAt : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  {I : ModelWithCorners 𝕜 E H} [inst_5 : ChartedSpace H M] (x : M),
  ContinuousOn (↑(extChartAt I x)) (extChartAt I x).source
-- Mathlib.Algebra.Algebra.Hom
AlgHom.ofLinearMap_id : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  (map_one : LinearMap.id 1 = 1) (map_mul : ∀ (x y : A), LinearMap.id (x * y) = LinearMap.id x * LinearMap.id y),
  AlgHom.ofLinearMap LinearMap.id map_one map_mul = AlgHom.id R A
-- Mathlib.CategoryTheory.Action.Basic
Action.resCongr.congr_simp : ∀ (V : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_3} {H : Type u_4} [inst_1 : Monoid G]
  [inst_2 : Monoid H] {f f' : G →* H} (h : f = f'), Action.resCongr V h = Action.resCongr V h
-- Mathlib.Computability.RegularExpressions
_private.Mathlib.Computability.RegularExpressions.0.RegularExpression.rmatch.match_1.eq_1 : ∀ {α : Type u_1} (motive : RegularExpression α → List α → Sort u_2) (P : RegularExpression α)
  (h_1 : (P : RegularExpression α) → motive P [])
  (h_2 : (P : RegularExpression α) → (a : α) → (as : List α) → motive P (a :: as)),
  (match P, [] with
    | P, [] => h_1 P
    | P, a :: as => h_2 P a as) =
    h_1 P
-- Mathlib.CategoryTheory.Skeletal
Quotient.recOnSubsingleton₂.congr_simp : ∀ {α : Sort uA} {β : Sort uB} {s₁ : Setoid α} {s₂ : Setoid β} {motive : Quotient s₁ → Quotient s₂ → Sort uC}
  [s : ∀ (a : α) (b : β), Subsingleton (motive ⟦a⟧ ⟦b⟧)] (q₁ : Quotient s₁) (q₂ : Quotient s₂)
  (g g_1 : (a : α) → (b : β) → motive ⟦a⟧ ⟦b⟧),
  g = g_1 → Quotient.recOnSubsingleton₂ q₁ q₂ g = Quotient.recOnSubsingleton₂ q₁ q₂ g_1
-- Mathlib.Control.LawfulFix
/-- The series of approximations of `fix f` (see `approx`) as a `Chain`  -/
Part.Fix.approxChain : {α : Type u_1} →
  {β : α → Type u_2} →
    (((a : α) → Part (β a)) →o (a : α) → Part (β a)) → OmegaCompletePartialOrder.Chain ((a : α) → Part (β a))
-- Mathlib.Data.Vector.Basic
/-- Reverse a vector.  -/
List.Vector.reverse : {α : Type u_1} → {n : ℕ} → List.Vector α n → List.Vector α n
-- Mathlib.Topology.Sequences
/-- The sequential closure of a sequentially closed set is the set itself.  -/
IsSeqClosed.seqClosure_eq : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, IsSeqClosed s → seqClosure s = s
-- Init.Data.String.Lemmas.Pattern.Find.Pred
String.Pos.find?_bool_eq_some_iff : ∀ {p : Char → Bool} {s : String} {pos pos' : s.Pos},
  pos.find? p = some pos' ↔
    pos ≤ pos' ∧
      (∃ (h : pos' ≠ s.endPos), p (pos'.get h) = true) ∧
        ∀ (pos'' : s.Pos), pos ≤ pos'' → ∀ (h' : pos'' < pos'), p (pos''.get ⋯) = false
-- Mathlib.MeasureTheory.Constructions.BorelSpace.WithTop
WithTop.instMeasurableSpace : {ι : Type u_1} →
  [inst : LinearOrder ι] → [inst_1 : TopologicalSpace ι] → [OrderTopology ι] → MeasurableSpace (WithTop ι)
-- Mathlib.RepresentationTheory.Basic
Representation.inv_apply_eq_iff : ∀ {k : Type u_1} {G : Type u_2} {V : Type u_3} [inst : Semiring k] [inst_1 : Group G] [inst_2 : AddCommMonoid V]
  [inst_3 : Module k V] (ρ : Representation k G V) {g : G} {x y : V}, (ρ g⁻¹) x = y ↔ x = (ρ g) y
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.size_alter_eq_self_of_not_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k : α} {f : Option (β k) → Option (β k)},
  k ∉ t → (f (t.get? k)).isNone = true → (t.alter k f).size = t.size
-- Mathlib.RingTheory.Derivation.ToSquareZero
derivationToSquareZeroOfLift_apply : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : CommRing B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (I : Ideal B) [inst_5 : Algebra A B] (hI : I ^ 2 = ⊥)
  [inst_6 : IsScalarTower R A B] (f : A →ₐ[R] B)
  (e : (Ideal.Quotient.mkₐ R I).comp f = IsScalarTower.toAlgHom R A (B ⧸ I)) (x : A),
  ↑((derivationToSquareZeroOfLift I hI f e) x) = f x - (algebraMap A B) x
-- Init.Sym.DSimp.DSimprocDSL
/-- zeta delta reduction. That is, expands all let-declarations.  -/
Lean.Parser.Sym.DSimp.zetaDelta : Lean.ParserDescr
-- Lean.Meta.MethodSpecs
_private.Lean.Meta.MethodSpecs.0.Lean.MethodSpecsInfo.mk : Lean.Name → Bool → Array (Lean.Name × Lean.Name) → Array Lean.MethodSpecTheorem✝ → Lean.MethodSpecsInfo✝
-- Mathlib.Tactic.Attr.Register
/-- The `@[nontriviality]` simp set is used by the `nontriviality` tactic to automatically
discharge theorems about the trivial case (where we know `Subsingleton α` and many theorems
in e.g. groups are trivially true).  -/
Parser.Attr.nontriviality : Lean.ParserDescr
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.ConnectedComponent.maximal_connected_toSubgraph : ∀ {V : Type u} {G : SimpleGraph V} (C : G.ConnectedComponent), Maximal SimpleGraph.Subgraph.Connected C.toSubgraph
-- Batteries.Data.List.Perm
List.subperm_cons : ∀ {α : Type u_1} (a : α) {l₁ l₂ : List α}, (a :: l₁).Subperm (a :: l₂) ↔ l₁.Subperm l₂
-- Mathlib.ModelTheory.Arithmetic.Presburger.Basic
FirstOrder.presburgerFunc.add.sizeOf_spec : sizeOf FirstOrder.presburgerFunc.add = 1
-- Mathlib.GroupTheory.Congruence.Defs
AddCon.comap_rel : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] {f : M → N} (H : ∀ (x y : M), f (x + y) = f x + f y)
  {c : AddCon N} {x y : M}, (AddCon.comap f H c) x y ↔ c (f x) (f y)
-- Mathlib.Algebra.Group.Defs
AddMonoid.mk : {M : Type u} →
  [toAddSemigroup : AddSemigroup M] →
    [toZero : Zero M] →
      (∀ (a : M), 0 + a = a) →
        (∀ (a : M), a + 0 = a) →
          [toNSMul : NSMul M] →
            autoParam (∀ (x : M), 0 • x = 0) AddMonoid.nsmul_zero._autoParam →
              autoParam (∀ (n : ℕ) (x : M), (n + 1) • x = n • x + x) AddMonoid.nsmul_succ._autoParam → AddMonoid M
-- Mathlib.Topology.MetricSpace.Isometry
IsometryEquiv.funUnique_apply : ∀ (ι : Type u_2) (α : Type u) [inst : PseudoEMetricSpace α] [inst_1 : Unique ι] [inst_2 : Fintype ι]
  (f : (i : ι) → (fun a => α) i), (IsometryEquiv.funUnique ι α) f = f default
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.instFromJsonCompletionItemCapabilities.fromJson : Lean.Json → Except String Lean.Lsp.CompletionItemCapabilities
-- Mathlib.Analysis.Convex.Side
AffineSubspace.sOppSide_smul_vsub_vadd_right : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x p₁ p₂ : P},
  x ∉ s → p₁ ∈ s → p₂ ∈ s → ∀ {t : R}, t < 0 → s.SOppSide x (t • (x -ᵥ p₁) +ᵥ p₂)