mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.DSlope
ContinuousOn.of_dslope : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {a : 𝕜} {s : Set 𝕜}, ContinuousOn (dslope f a) s → ContinuousOn f s
-- Mathlib.CategoryTheory.Monoidal.Discrete
CategoryTheory.Discrete.monoidalFunctor.eq_1 : ∀ {M : Type u} [inst : Monoid M] {N : Type u'} [inst_1 : Monoid N] (F : M →* N),
  CategoryTheory.Discrete.monoidalFunctor F = CategoryTheory.Discrete.functor fun X => { as := F X }
-- Mathlib.Data.Part
/-- The domain of a partial value  -/
Part.Dom : {α : Type u} → Part α → Prop
-- Mathlib.Topology.MetricSpace.GromovHausdorff
GromovHausdorff.dist_ghDist : ∀ (p q : GromovHausdorff.GHSpace), dist p q = GromovHausdorff.ghDist p.Rep q.Rep
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
/-- The identity continuous homomorphism.  -/
ContinuousMonoidHom.id : (A : Type u_2) → [inst : Monoid A] → [inst_1 : TopologicalSpace A] → A →ₜ* A
-- Aesop.Script.SpecificTactics
Aesop.Script.TacticBuilder.obtain : Lean.MVarId → Lean.Expr → Aesop.CtorNames → Aesop.Script.TacticBuilder
-- Init.Data.Slice.Array.Lemmas
Subarray.getElem_toList : ∀ {α : Type u_1} {i : ℕ} {xs : Subarray α} {h : i < (Std.Slice.toList xs).length}, (Std.Slice.toList xs)[i] = xs[i]
-- Lean.MetavarContext
Lean.MetavarContext.MkBinding.Context.mk.injEq : ∀ (quotContext : Lean.Name) (preserveOrder : Bool) (binderInfoForMVars : Lean.BinderInfo)
  (mvarIdsToAbstract : Lean.MVarIdSet) (quotContext_1 : Lean.Name) (preserveOrder_1 : Bool)
  (binderInfoForMVars_1 : Lean.BinderInfo) (mvarIdsToAbstract_1 : Lean.MVarIdSet),
  ({ quotContext := quotContext, preserveOrder := preserveOrder, binderInfoForMVars := binderInfoForMVars,
        mvarIdsToAbstract := mvarIdsToAbstract } =
      { quotContext := quotContext_1, preserveOrder := preserveOrder_1, binderInfoForMVars := binderInfoForMVars_1,
        mvarIdsToAbstract := mvarIdsToAbstract_1 }) =
    (quotContext = quotContext_1 ∧
      preserveOrder = preserveOrder_1 ∧
        binderInfoForMVars = binderInfoForMVars_1 ∧ mvarIdsToAbstract = mvarIdsToAbstract_1)
-- Mathlib.Topology.UniformSpace.Cauchy
cauchy_iff : ∀ {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α},
  Cauchy f ↔ f.NeBot ∧ ∀ s ∈ uniformity α, ∃ t ∈ f, t ×ˢ t ⊆ s
-- Mathlib.Data.List.Monad
List.instLawfulAlternative_mathlib : LawfulAlternative List
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
/-- `measurableLEEval μ ν` is the set of `∫⁻ x, f x ∂μ` for all `f ∈ measurableLE μ ν`.  -/
MeasureTheory.Measure.LebesgueDecomposition.measurableLEEval : {α : Type u_1} → {m : MeasurableSpace α} → MeasureTheory.Measure α → MeasureTheory.Measure α → Set ENNReal
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.cokernelImageι_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasImage f]
  [inst_3 : CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.image.ι f)]
  [inst_4 : CategoryTheory.Limits.HasCokernel f]
  [inst_5 : CategoryTheory.Epi (CategoryTheory.Limits.factorThruImage f)],
  (CategoryTheory.Limits.cokernelImageι f).inv =
    CategoryTheory.Limits.cokernel.desc f (CategoryTheory.Limits.cokernel.π (CategoryTheory.Limits.image.ι f)) ⋯
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.Augmented.hom_ext_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.SimplicialObject.Augmented C}
  {f g : X ⟶ Y}, f = g ↔ f.left = g.left ∧ f.right = g.right
-- Init.Data.List.Basic
List.range'_eq_range'TR : @List.range' = @List.range'TR
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.whiskerRight_iff : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : B} {f g : a ⟶ b} (η θ : f ⟶ g),
  CategoryTheory.Bicategory.whiskerRight η (CategoryTheory.CategoryStruct.id b) =
      CategoryTheory.Bicategory.whiskerRight θ (CategoryTheory.CategoryStruct.id b) ↔
    η = θ
-- Mathlib.CategoryTheory.Elements
CategoryTheory.Functor.Elements.ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)} (x y : F.Elements)
  (h₁ : x.fst = y.fst), (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.eqToHom h₁))) x.snd = y.snd → x = y
-- Mathlib.Order.Category.BddDistLat
/-- The underlying distrib lattice of a bounded distributive lattice.  -/
BddDistLat.toDistLat : BddDistLat → DistLat
-- Mathlib.Geometry.Convex.Cone.Pointed
/-- The image of a pointed cone under an `R`-linear map is a pointed cone.  -/
PointedCone.map : {R : Type u_1} →
  {E : Type u_2} →
    {F : Type u_3} →
      [inst : Semiring R] →
        [inst_1 : PartialOrder R] →
          [inst_2 : IsOrderedRing R] →
            [inst_3 : AddCommMonoid E] →
              [inst_4 : Module R E] →
                [inst_5 : AddCommMonoid F] → [inst_6 : Module R F] → (E →ₗ[R] F) → PointedCone R E → PointedCone R F
-- Mathlib.Algebra.Group.End
_private.Mathlib.Algebra.Group.End.0.Equiv.Perm.pow_aux : ∀ {α : Type u_4} {p : α → Prop} {f : Equiv.Perm α}, (∀ (x : α), p (f x) ↔ p x) → ∀ {n : ℕ} (x : α), p ((f ^ n) x) ↔ p x
-- Mathlib.Order.Sublocale
/-- The restriction corresponding to a sublocale forms a Galois insertion with the forgetful map
from the sublocale to the original locale.  -/
Sublocale.giRestrict : {X : Type u_1} → [inst : Order.Frame X] → (S : Sublocale X) → GaloisInsertion (⇑S.restrict) Subtype.val
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
/-- The univariate polynomials `ΨSqₙ` congruent to `ψₙ²`.  -/
WeierstrassCurve.ΨSq : {R : Type r} → [inst : CommRing R] → WeierstrassCurve R → ℤ → Polynomial R
-- Init.Data.UInt.Lemmas
UInt64.toNat_ofNatTruncate_of_lt : ∀ {n : ℕ}, n < UInt64.size → (UInt64.ofNatClamp n).toNat = n
-- Mathlib.NumberTheory.SelbergSieve
/-- The finite set of prime numbers whose multiples are to be sifted from `support`. We work with
their product because it lets us treat `nu` as a multiplicative arithmetic function. It also
plays well with Moebius inversion.  -/
BoundingSieve.prodPrimes : BoundingSieve → ℕ
-- Mathlib.Data.Nat.Fib.Basic
Nat.fastFibAux_bit_true : ∀ (n : ℕ),
  (Nat.bit true n).fastFibAux =
    have p := n.fastFibAux;
    (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2))
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.cylinder.ι₀_π : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} (K : HomologicalComplex C c) [inst_2 : DecidableRel c.Rel]
  [inst_3 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [inst_4 : K.HasCylinder],
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.cylinder.ι₀ K) (HomologicalComplex.cylinder.π K) =
    CategoryTheory.CategoryStruct.id K
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Real.arctan_pos : ∀ {x : ℝ}, 0 < Real.arctan x ↔ 0 < x
-- Init.Data.Array.Attach
Array.attach_reverse : ∀ {α : Type u_1} {xs : Array α},
  xs.reverse.attach =
    Array.map
      (fun x =>
        match x with
        | ⟨x, h⟩ => ⟨x, ⋯⟩)
      xs.attach.reverse
-- Mathlib.Algebra.Polynomial.RingDivision
Polynomial.natDegree_pos_of_aeval_root : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Semiring S] [inst_2 : Algebra R S] {p : Polynomial R},
  p ≠ 0 → ∀ {z : S}, (Polynomial.aeval z) p = 0 → (∀ (x : R), (algebraMap R S) x = 0 → x = 0) → 0 < p.natDegree
-- Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit
_private.Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit.0.CategoryTheory.coherentTopology.struct.map : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preregular C] →
      [inst_2 : CategoryTheory.FinitaryExtensive C] →
        {F : CategoryTheory.Functor ℕᵒᵖ (CategoryTheory.Sheaf (CategoryTheory.coherentTopology C) (Type v))} →
          (self : CategoryTheory.coherentTopology.struct✝ F) →
            (n : ℕ) →
              CategoryTheory.coherentTopology.struct.X✝ self (n + 1) ⟶ CategoryTheory.coherentTopology.struct.X✝ self n
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.isAddUnit_iff : ∀ {α : Type u_2} [inst : SubtractionMonoid α] {s : Set α}, IsAddUnit s ↔ ∃ a, s = {a} ∧ IsAddUnit a
-- Init.Data.List.Basic
/-- Returns `true` if `p` returns `true` for any element of `l`.

`O(|l|)`. Short-circuits upon encountering the first `true`.

Examples:
* `[2, 4, 6].any (· % 2 = 0) = true`
* `[2, 4, 6].any (· % 2 = 1) = false`
* `[2, 4, 5, 6].any (· % 2 = 0) = true`
* `[2, 4, 5, 6].any (· % 2 = 1) = true`
 -/
List.any : {α : Type u} → List α → (α → Bool) → Bool
-- Lean.Parser.Command
Lean.Parser.Command.example.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Algebra.Group.UniqueProds.Basic
/-- `TwoUniqueProd` is preserved under multiplicative equivalences.  -/
MulEquiv.twoUniqueProds_iff : ∀ {G : Type u} {H : Type v} [inst : Mul G] [inst_1 : Mul H] (f : G ≃* H), TwoUniqueProds G ↔ TwoUniqueProds H
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.iCondIndep.congr_simp : ∀ {Ω : Type u_1} {ι : Type u_2} (m' m'_1 : MeasurableSpace Ω) (e_m' : m' = m'_1) {mΩ : MeasurableSpace Ω}
  [inst : StandardBorelSpace Ω] (hm' : m' ≤ mΩ) (m m_1 : ι → MeasurableSpace Ω),
  m = m_1 →
    ∀ (μ μ_1 : MeasureTheory.Measure Ω) (e_μ : μ = μ_1) [inst_1 : MeasureTheory.IsFiniteMeasure μ],
      ProbabilityTheory.iCondIndep m' hm' m μ = ProbabilityTheory.iCondIndep m'_1 ⋯ m_1 μ_1
-- Init.Data.SInt.Lemmas
ISize.toNatClampNeg_ofIntTruncate_of_lt_two_pow_numBits : ∀ {n : ℤ}, n < 2 ^ (System.Platform.numBits - 1) → (ISize.ofIntClamp n).toNatClampNeg = n.toNat
-- Mathlib.Combinatorics.Matroid.IndepAxioms
IndepMatroid.ofFinitary.congr_simp : ∀ {α : Type u_1} (E E_1 : Set α) (e_E : E = E_1) (Indep Indep_1 : Set α → Prop) (e_Indep : Indep = Indep_1)
  (indep_empty : Indep ∅) (indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I)
  (indep_aug : ∀ ⦃I B : Set α⦄, Indep I → ¬Maximal Indep I → Maximal Indep B → ∃ x ∈ B \ I, Indep (insert x I))
  (indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I)
  (subset_ground : ∀ (I : Set α), Indep I → I ⊆ E),
  IndepMatroid.ofFinitary E Indep indep_empty indep_subset indep_aug indep_compact subset_ground =
    IndepMatroid.ofFinitary E_1 Indep_1 ⋯ ⋯ ⋯ ⋯ ⋯
-- Mathlib.RingTheory.Int.Basic
Int.Prime.dvd_mul' : ∀ {m n : ℤ} {p : ℕ}, Nat.Prime p → ↑p ∣ m * n → ↑p ∣ m ∨ ↑p ∣ n
-- Mathlib.NumberTheory.ModularForms.LFunction
CuspForm.differentiable_Λ : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} [inst : Γ.IsArithmetic] {k : ℤ} (hk : 0 < k) {F : Type u_1}
  [inst_1 : FunLike F UpperHalfPlane ℂ] (f : F) [inst_2 : CuspFormClass F Γ k], Differentiable ℂ (ModularForm.Λ hk f)
-- Mathlib.AlgebraicGeometry.AffineScheme
/-- The stalk of `Spec R` at `x` is isomorphic to `Rₚ`,
where `p` is the prime corresponding to `x`.  -/
AlgebraicGeometry.Spec.stalkIso : (R : CommRingCat) →
  (x : PrimeSpectrum ↑R) → (AlgebraicGeometry.Spec R).presheaf.stalk x ≅ CommRingCat.of (Localization.AtPrime x.asIdeal)
-- Mathlib.MeasureTheory.VectorMeasure.Variation.Basic
MeasureTheory.VectorMeasure.variation_add_le : ∀ {X : Type u_1} {V : Type u_2} {mX : MeasurableSpace X} [inst : TopologicalSpace V] [inst_1 : ENormedAddCommMonoid V]
  [inst_2 : T2Space V] {μ ν : MeasureTheory.VectorMeasure X V} [inst_3 : ContinuousAdd V],
  (μ + ν).variation ≤ μ.variation + ν.variation
-- Mathlib.Algebra.Module.Submodule.Defs
Submodule.smul_mem_iff_of_isUnit : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] {module_M : Module R M} (p : Submodule R M)
  {r : R} {x : M}, IsUnit r → (r • x ∈ p ↔ x ∈ p)
-- Mathlib.Algebra.Category.ModuleCat.Products
ModuleCat.coproductCocone.eq_1 : ∀ {R : Type u} [inst : Ring R] {ι : Type v} (Z : ι → ModuleCat R) [inst_1 : DecidableEq ι],
  ModuleCat.coproductCocone Z =
    CategoryTheory.Limits.Cofan.mk (ModuleCat.of R (DirectSum ι fun i => ↑(Z i))) fun i =>
      ModuleCat.ofHom (DirectSum.lof R ι (fun i => ↑(Z i)) i)
-- Mathlib.CategoryTheory.Monad.Adjunction
CategoryTheory.Adjunction.adjToMonadIso_hom_toNatTrans_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) (X : C),
  (CategoryTheory.Adjunction.adjToMonadIso T).hom.app X = CategoryTheory.CategoryStruct.id (T.obj X)
-- Mathlib.Data.Set.Finite.Basic
Set.Finite.toFinset_ssubset : ∀ {α : Type u} {s : Set α} {hs : s.Finite} {t : Finset α}, hs.toFinset ⊂ t ↔ s ⊂ ↑t
-- Mathlib.Topology.UniformSpace.Completion
/-- "Extension" to the completion. It is defined for any map `f` but
returns an arbitrary constant value if `f` is not uniformly continuous  -/
UniformSpace.Completion.extension : {α : Type u_1} → [inst : UniformSpace α] → {β : Type u_2} → [UniformSpace β] → (α → β) → UniformSpace.Completion α → β
-- Mathlib.CategoryTheory.EpiMono
CategoryTheory.SplitMono.comp_retraction : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Z Y X : C} {f : Z ⟶ Y} {g : Y ⟶ X}
  (smf : CategoryTheory.SplitMono f) (smg : CategoryTheory.SplitMono g),
  (smf.comp smg).retraction = CategoryTheory.CategoryStruct.comp smg.retraction smf.retraction
-- Batteries.Logic
heq_iff_eq : ∀ {α : Sort u_1} {a b : α}, a ≍ b ↔ a = b
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
/-- Pack a `BitVec` with its width into a single parameter-less structure.
 -/
Std.Tactic.BVDecide.BVExpr.PackedBitVec : Type
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.map_top : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B] (f : A →ₐ[R] B), Subalgebra.map f ⊤ = f.range
-- Mathlib.Algebra.Star.SelfAdjoint
IsSelfAdjoint.ratCast : ∀ {R : Type u_1} [inst : DivisionRing R] [inst_1 : StarRing R] (x : ℚ), IsSelfAdjoint ↑x
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
/-- The `moduleFilterBasis` induced by the filter basis `Seminorm.basisSets`.  -/
SeminormFamily.moduleFilterBasis : {𝕜 : Type u_2} →
  {F : Type u_7} →
    {ι : Type u_9} →
      [inst : NormedDivisionRing 𝕜] →
        [inst_1 : AddCommGroup F] → [inst_2 : Module 𝕜 F] → SeminormFamily 𝕜 F ι → ModuleFilterBasis 𝕜 F
-- Mathlib.CategoryTheory.Filtered.Final
Monotone.initial_functor_iff : ∀ {J₁ : Type u_1} {J₂ : Type u_2} [inst : Preorder J₁] [inst_1 : Preorder J₂] [IsCodirectedOrder J₁] {f : J₁ → J₂}
  (hf : Monotone f), hf.functor.Initial ↔ ∀ (j₁ : J₂), ∃ j₂, f j₂ ≤ j₁
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
IsCyclic.card_powMonoidHom_ker : ∀ (G : Type u_2) [inst : CommGroup G] [IsCyclic G] [Finite G] (d : ℕ),
  Nat.card ↥(powMonoidHom d).ker = (Nat.card G).gcd d
-- Lean.Expr
/-- Return `some e'` if `e = mkInaccessible e'`.  -/
Lean.inaccessible? : Lean.Expr → Option Lean.Expr
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.Λ'.move : (Turing.PartrecToTM2.Γ' → Bool) →
  Turing.PartrecToTM2.K' → Turing.PartrecToTM2.K' → Turing.PartrecToTM2.Λ' → Turing.PartrecToTM2.Λ'
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
/-- A slight reformulation of `IsLocalStructomorphWithinAt` when `f` is an open partial homeomorph
and the set we're considering is `f.source`.  -/
OpenPartialHomeomorph.isLocalStructomorphWithinAt_source_iff : ∀ {H : Type u_1} [inst : TopologicalSpace H] {G : StructureGroupoid H} [ClosedUnderRestriction G]
  (f : OpenPartialHomeomorph H H) {x : H},
  G.IsLocalStructomorphWithinAt (↑f) f.source x ↔
    x ∈ f.source → ∃ e ∈ G, e.source ⊆ f.source ∧ Set.EqOn (↑f) (↑e) e.source ∧ x ∈ e.source
-- Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
MvPolynomial.DirectSum.coeLinearMap_eq_dfinsuppSum : ∀ (R : Type u_1) {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} [inst_1 : AddCommMonoid M] (w : σ → M)
  [inst_2 : DecidableEq σ] [inst_3 : DecidableEq R] [inst_4 : DecidableEq M]
  (x : DirectSum M fun i => ↥(MvPolynomial.weightedHomogeneousSubmodule R w i)),
  (DirectSum.coeLinearMap fun i => MvPolynomial.weightedHomogeneousSubmodule R w i) x = DFinsupp.sum x fun x x_1 => ↑x_1
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.d₁₀_eq_zero_of_isTrivial : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) [A.IsTrivial], groupHomology.d₁₀ A = 0
-- Mathlib.RingTheory.Support
Module.support_eq_empty : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Subsingleton M],
  Module.support R M = ∅
-- Init.Data.String.Pattern.Basic
/-- A step taken during the traversal of a `Slice` by a forward or backward searcher.
 -/
String.Slice.Pattern.SearchStep : String.Slice → Type
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.DiseqCnstr.mk.sizeOf_spec : ∀ (lhs rhs : Lean.Grind.AC.Seq) (h : Lean.Meta.Grind.AC.DiseqCnstrProof),
  sizeOf { lhs := lhs, rhs := rhs, h := h } = 1 + sizeOf lhs + sizeOf rhs + sizeOf h
-- Init.Data.List.Nat.Basic
List.le_max?_getD_of_mem : ∀ {l : List ℕ} {a k : ℕ}, a ∈ l → a ≤ l.max?.getD k
-- Mathlib.Analysis.InnerProductSpace.Adjoint
LinearMap.IsSymmetric.toSelfAdjoint_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : CompleteSpace E] {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) {x : E}, ↑↑hT.toSelfAdjoint x = T x
-- Mathlib.Analysis.Complex.Norm
Complex.cauSeqConj.eq_1 : ∀ (f : CauSeq ℂ fun x => ‖x‖), Complex.cauSeqConj f = ⟨fun n => (starRingEnd ℂ) (↑f n), ⋯⟩
-- Init.Data.String.Lemmas.Pattern.String.ForwardPattern
_private.Init.Data.String.Lemmas.Pattern.String.ForwardPattern.0.String.Slice.revAll.eq_1 : ∀ {ρ : Type} (s : String.Slice) (pat : ρ) [inst : String.Slice.Pattern.BackwardPattern pat],
  s.revAll pat = (s.skipSuffixWhile pat == s.startPos)
-- Lean.Syntax
Lean.Syntax.instForInTopDownOfMonad.loop : {m : Type u_1 → Type u_2} →
  [Monad m] →
    {β : Type u_1} → (Lean.Syntax → β → m (ForInStep β)) → Bool → Lean.Syntax → β → [Inhabited β] → m (ForInStep β)
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.endLine : Lean.Parser.ParserFn
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.submodule_span_le_lieSpan : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] {s : Set M}, Submodule.span R s ≤ ↑(LieSubmodule.lieSpan R L s)
-- Mathlib.Data.Finite.Prod
Set.Finite.of_prod_left : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β}, (s ×ˢ t).Finite → t.Nonempty → s.Finite
-- Mathlib.CategoryTheory.Endomorphism
CategoryTheory.End.smul_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {r : CategoryTheory.End Y} {f : X ⟶ Y},
  r • f = CategoryTheory.CategoryStruct.comp f r
-- Init.Data.BitVec.Lemmas
BitVec.msb_shiftLeftZeroExtend : ∀ {w : ℕ} (x : BitVec w) (i : ℕ), (x.shiftLeftZeroExtend i).msb = x.msb
-- Mathlib.NumberTheory.Real.Irrational
irrational_intCast_add_iff : ∀ {m : ℤ} {x : ℝ}, Irrational (↑m + x) ↔ Irrational x
-- Mathlib.Topology.UniformSpace.UniformConvergence
/-- Composing on the right by a function preserves uniform convergence on a set  -/
TendstoUniformlyOn.comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Type u_4} [inst : UniformSpace β] {F : ι → α → β} {f : α → β}
  {s : Set α} {p : Filter ι},
  TendstoUniformlyOn F f p s → ∀ (g : γ → α), TendstoUniformlyOn (fun n => F n ∘ g) (f ∘ g) p (g ⁻¹' s)
-- Init.Data.String.Lemmas.Splits
String.Slice.Pos.Splits.rotateRight.congr_simp : ∀ {s : String.Slice} {p p_1 : s.Pos} (e_p : p = p_1) {t₁ t₁_1 : String} (e_t₁ : t₁ = t₁_1) {t₂ t₂_1 : String}
  (e_t₂ : t₂ = t₂_1) {t₃ t₃_1 : String} (e_t₃ : t₃ = t₃_1) (h : p.Splits t₁ (t₂ ++ t₃)), h.rotateRight = ⋯.rotateRight
-- Mathlib.Algebra.Lie.Submodule
/-- The natural equivalence between the 'top' Lie subalgebra and the enclosing Lie algebra.

This is the Lie subalgebra version of `Submodule.topEquiv`.  -/
LieSubalgebra.topEquiv : {R : Type u} → {L : Type v} → [inst : CommRing R] → [inst_1 : LieRing L] → [inst_2 : LieAlgebra R L] → ↥⊤ ≃ₗ⁅R⁆ L
-- Mathlib.Topology.FiberBundle.Basic
FiberPrebundle.mem_pretrivializationAt_source : ∀ {B : Type u_2} {F : Type u_3} {E : B → Type u_5} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  [inst_2 : (x : B) → TopologicalSpace (E x)] (a : FiberPrebundle F E) (b : B) (x : E b),
  ⟨b, x⟩ ∈ (a.pretrivializationAt b).source
-- Mathlib.Algebra.Module.ZMod
/-- Reinterpret an additive subgroup of a `ℤ/nℤ`-module as a `ℤ/nℤ`-submodule.

See also: `AddSubgroup.toIntSubmodule`, `AddSubmonoid.toNatSubmodule`.  -/
AddSubgroup.toZModSubmodule : (n : ℕ) →
  {M : Type u_1} → [inst : AddCommGroup M] → [inst_1 : Module (ZMod n) M] → AddSubgroup M ≃o Submodule (ZMod n) M
-- Mathlib.Analysis.Distribution.TestFunction
TestFunction.toBoundedContinuousFunctionCLM_eq_of_scalars : ∀ {𝕜 : 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 : ℕ∞} [inst_6 : Algebra ℝ 𝕜] [inst_7 : IsScalarTower ℝ 𝕜 F]
  (𝕜' : Type u_6) [inst_8 : NontriviallyNormedField 𝕜'] [inst_9 : NormedSpace 𝕜' F] [inst_10 : Algebra ℝ 𝕜']
  [inst_11 : IsScalarTower ℝ 𝕜' F],
  ⇑(TestFunction.toBoundedContinuousFunctionCLM 𝕜) = ⇑(TestFunction.toBoundedContinuousFunctionCLM 𝕜')
-- Lean.Parser.Syntax
Lean.Parser.Command.optKind.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Algebra.Module.LinearMap.Defs
/-- A linear map preserves addition.  -/
IsLinearMap.map_add : ∀ {R : Type u} {M : Type v} {M₂ : Type w} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂] {f : M → M₂}, IsLinearMap R f → ∀ (x y : M), f (x + y) = f x + f y
-- Mathlib.LinearAlgebra.Matrix.Vec
/-- Technical lemma shared with `kronecker_mulVec_vec` and `vec_mul_eq_mulVec`.  -/
Matrix.kronecker_mulVec_vec_of_commute : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_4} {p : Type u_5} {R : Type u_3} [inst : NonUnitalSemiring R]
  [inst_1 : Fintype m] [inst_2 : Fintype n] (A : Matrix l m R) (X : Matrix m n R) (B : Matrix p n R),
  (∀ (x : R) (i : p) (j : n), Commute x (B i j)) →
    (Matrix.kroneckerMap (fun x1 x2 => x1 * x2) B A).mulVec X.vec = (A * X * B.transpose).vec
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
DifferentiableOn.cpow : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f g : E → ℂ} {s : Set E},
  DifferentiableOn ℂ f s →
    DifferentiableOn ℂ g s → Set.MapsTo f s Complex.slitPlane → DifferentiableOn ℂ (fun x => f x ^ g x) s
-- Mathlib.Tactic.Algebra.Lemmas
Mathlib.Tactic.Algebra.nat_rawCast_1 : ∀ {R : Type u_1} [sR : CommSemiring R], Nat.rawCast 1 = 1
-- Mathlib.Topology.Category.Profinite.Projective
Profinite.instEnoughProjectives : CategoryTheory.EnoughProjectives Profinite
-- Mathlib.Algebra.Ring.Subsemiring.Defs
/-- A subsemiring contains the semiring's 1.  -/
Subsemiring.one_mem : ∀ {R : Type u} [inst : NonAssocSemiring R] (s : Subsemiring R), 1 ∈ s
-- Mathlib.Topology.Connected.Clopen
nonempty_frontier_iff : ∀ {α : Type u} [inst : TopologicalSpace α] [PreconnectedSpace α] {s : Set α},
  (frontier s).Nonempty ↔ s.Nonempty ∧ s ≠ Set.univ
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.ResolvableCompletionList.mk.inj : ∀ {isIncomplete : Bool} {items : Array Lean.Lsp.ResolvableCompletionItem} {isIncomplete_1 : Bool}
  {items_1 : Array Lean.Lsp.ResolvableCompletionItem},
  { isIncomplete := isIncomplete, items := items } = { isIncomplete := isIncomplete_1, items := items_1 } →
    isIncomplete = isIncomplete_1 ∧ items = items_1
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.loopless : ∀ {V : Type u} (self : SimpleGraph V), Std.Irrefl self.Adj
-- Mathlib.GroupTheory.Perm.Fin
Fin.cycleRange_of_lt : ∀ {n : ℕ} {i j : Fin n} [inst : NeZero n], i < j → j.cycleRange i = i + 1
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonResolvableCompletionItem.toJson : Lean.Lsp.ResolvableCompletionItem → Lean.Json
-- Init.Data.SInt.Lemmas
Int64.add_mul : ∀ {a b c : Int64}, (a + b) * c = a * c + b * c
-- Mathlib.RingTheory.Polynomial.Basic
Polynomial.restriction_one : ∀ {R : Type u} [inst : Ring R], Polynomial.restriction 1 = 1