mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Action.Continuous
/-- If `f = f'`, restriction of scalars along `f` and `f'` is the same.  -/
ContAction.resCongr : (V : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    {FV : V → V → Type u_2} →
      {CV : V → Type u_3} →
        [inst_1 : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)] →
          [inst_2 : CategoryTheory.ConcreteCategory V FV] →
            [inst_3 : CategoryTheory.HasForget₂ V TopCat] →
              {G : Type u_4} →
                [inst_4 : Monoid G] →
                  [inst_5 : TopologicalSpace G] →
                    {H : Type u_5} →
                      [inst_6 : Monoid H] →
                        [inst_7 : TopologicalSpace H] →
                          (f f' : G →ₜ* H) → f = f' → (ContAction.res V f ≅ ContAction.res V f')
-- Init.Data.Rat.Basic
Rat.normalize.dvd_den : ∀ {num : ℤ} {den g : ℕ}, g = num.natAbs.gcd den → g ∣ den
-- Mathlib.Algebra.Module.Submodule.Defs
Submodule.coe_smul : ∀ {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 : ↥p), ↑(r • x) = r • ↑x
-- Mathlib.CategoryTheory.Monoidal.Free.Coherence
/-- Given an object `X` of the free monoidal category and an object `n` in normal form, taking
the tensor product `n ⊗ X` in the free monoidal category is functorial in both `X` and `n`.  -/
CategoryTheory.FreeMonoidalCategory.tensorFunc : (C : Type u) →
  CategoryTheory.Functor (CategoryTheory.FreeMonoidalCategory C)
    (CategoryTheory.Functor ((CategoryTheory.Discrete ∘ CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject) C)
      (CategoryTheory.FreeMonoidalCategory C))
-- Lean.DocString.Links
/-- Rewrites Lean reference manual links in `docstring` to point at the reference manual.

This assumes that all such links have already been validated by `validateDocComment`.
 -/
Lean.rewriteManualLinks : String → BaseIO String
-- Mathlib.NumberTheory.ModularForms.QExpansion
ModularFormClass.differentiableAt_cuspFunction : ∀ {k : ℤ} {F : Type u_1} [inst : FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} (f : F)
  [ModularFormClass F Γ k],
  0 < h → h ∈ Γ.strictPeriods → ∀ {q : ℂ}, ‖q‖ < 1 → DifferentiableAt ℂ (UpperHalfPlane.cuspFunction h ⇑f) q
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.prod_lt_one_iff_of_le_one : ∀ {ι : Type u_1} {N : Type u_5} [inst : CommMonoid N] [inst_1 : PartialOrder N] {f : ι → N} {s : Finset ι}
  [MulLeftMono N], (∀ x ∈ s, f x ≤ 1) → (∏ x ∈ s, f x < 1 ↔ ∃ x ∈ s, f x < 1)
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the forward direction of `monovaryOn_inv_right₀`. -/
MonovaryOn.of_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) → MonovaryOn f g⁻¹ s → AntivaryOn f g s
-- Mathlib.Analysis.Calculus.Deriv.Slope
hasDerivWithinAt_iff_tendsto_slope : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} {s : Set 𝕜},
  HasDerivWithinAt f f' s x ↔ Filter.Tendsto (slope f x) (nhdsWithin x (s \ {x})) (nhds f')
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Arrow.id_left : ∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] (f : CategoryTheory.Arrow T),
  CategoryTheory.Arrow.Hom.left (CategoryTheory.CategoryStruct.id f) = CategoryTheory.CategoryStruct.id f.left
-- Mathlib.Algebra.Order.Nonneg.Basic
Nonneg.mk_natCast : ∀ {α : Type u_1} [inst : AddMonoidWithOne α] [inst_1 : PartialOrder α] [inst_2 : AddLeftMono α]
  [inst_3 : ZeroLEOneClass α] (n : ℕ), ⟨↑n, ⋯⟩ = ↑n
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRootMonic.map_modByMonic : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
  (h : IsAdjoinRootMonic S f) (g : Polynomial R), h.map (g %ₘ f) = h.map g
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.pow_subset_pow_left : ∀ {α : Type u_2} [inst : Monoid α] {s t : Set α} {n : ℕ}, s ⊆ t → s ^ n ⊆ t ^ n
-- Lean.Parser.Do
Lean.Parser.Term.doLetElse : Lean.Parser.Parser
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
/-- **Chinese remainder theorem** for a Dedekind domain: if the ideal `I` factors as
`∏ i, P i ^ e i`, then `R ⧸ I` factors as `Π i, R ⧸ (P i ^ e i)`.
See `IsDedekindDomain.quotientEquivPiOfProdEq` for the version in terms of `Ideal R`.  -/
IsDedekindDomain.HeightOneSpectrum.quotientEquivPiOfProdEq : {R : Type u_1} →
  [inst : CommRing R] →
    {ι : Type u_4} →
      [IsDedekindDomain R] →
        [inst_2 : Fintype ι] →
          (I : Ideal R) →
            (P : ι → IsDedekindDomain.HeightOneSpectrum R) →
              (e : ι → ℕ) →
                (Pairwise fun i j => P i ≠ P j) →
                  ∏ i, (P i).asIdeal ^ e i = I → R ⧸ I ≃+* ((i : ι) → R ⧸ (P i).asIdeal ^ e i)
-- Mathlib.Algebra.Star.StarAlgHom
/-- Upgrade an algebra equivalence to a ⋆-algebra equivalence given that it preserves the
`star` operation.  -/
StarAlgEquiv.ofAlgEquiv : {R : Type u_6} →
  {A : Type u_7} →
    {B : Type u_8} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Semiring B] →
            [inst_3 : Algebra R A] →
              [inst_4 : Algebra R B] →
                [inst_5 : Star A] →
                  [inst_6 : Star B] → (f : A ≃ₐ[R] B) → (∀ (x : A), f (star x) = star (f x)) → A ≃⋆ₐ[R] B
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
/-- **Alias** of `Ordinal.exists_ord_cof_eq`.

---

Every well-order has a cofinal subset of order type `(cof α).ord`.  -/
Ordinal.ord_cof_eq : ∀ (α : Type u) [inst : LinearOrder α] [inst_1 : WellFoundedLT α],
  ∃ s, IsCofinal s ∧ (Ordinal.type fun x1 x2 => x1 < x2) = (Order.cof α).ord
-- Mathlib.Geometry.Manifold.StructureGroupoid
/-- Pregroupoids contain the identity map (on `univ`)  -/
Pregroupoid.id_mem : ∀ {H : Type u_2} [inst : TopologicalSpace H] (self : Pregroupoid H), self.property id Set.univ
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.integral_comp_mul_sub : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b c : ℝ} (f : ℝ → E),
  c ≠ 0 → ∀ (d : ℝ), ∫ (x : ℝ) in a..b, f (c * x - d) = c⁻¹ • ∫ (x : ℝ) in c * a - d..c * b - d, f x
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.utf8Size_assemble₃ : ∀ {w x y : UInt8} {c : Char}, ByteArray.utf8DecodeChar?.assemble₃ w x y = some c → c.utf8Size = 3
-- Lean.Meta.Tactic.Grind.CollectParams
_private.Lean.Meta.Tactic.Grind.CollectParams.0.Lean.Meta.Grind.Collector.State : Type
-- Mathlib.RingTheory.DedekindDomain.Different
Submodule.le_traceDual_mul_iff : ∀ {A : Type u_1} {K : Type u_2} {L : Type u} {B : Type u_3} [inst : CommRing A] [inst_1 : Field K] [inst_2 : CommRing B]
  [inst_3 : Field L] [inst_4 : Algebra A K] [inst_5 : Algebra B L] [inst_6 : Algebra A B] [inst_7 : Algebra K L]
  [inst_8 : Algebra A L] [inst_9 : IsScalarTower A K L] [inst_10 : IsScalarTower A B L] {I J J' : Submodule B L},
  I ≤ Submodule.traceDual A K (J * J') ↔ I * J ≤ Submodule.traceDual A K J'
-- Mathlib.Algebra.Ring.Semiconj
SemiconjBy.neg_right : ∀ {R : Type u} [inst : Mul R] [inst_1 : HasDistribNeg R] {a x y : R}, SemiconjBy a x y → SemiconjBy a (-x) (-y)
-- Init.Data.UInt.Lemmas
UInt32.ofFin_div : ∀ (a b : Fin UInt32.size), UInt32.ofFin (a / b) = UInt32.ofFin a / UInt32.ofFin b
-- Mathlib.LinearAlgebra.Matrix.Unique
Matrix.uniqueAddEquiv_apply : ∀ {m : Type u_1} {n : Type u_2} {A : Type u_3} [inst : Unique m] [inst_1 : Unique n] [inst_2 : Add A]
  (M : Matrix m n A), Matrix.uniqueAddEquiv M = M default default
-- Std.Data.Internal.List.Associative
Std.Internal.List.DistinctKeys.containsKey_eq_false : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k},
  Std.Internal.List.DistinctKeys (⟨k, v⟩ :: l) → Std.Internal.List.containsKey k l = false
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.«mrefinePat⌜_⌝» : Lean.ParserDescr
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddSubmonoid.isLocalizationMap_iff_bijective : ∀ {M : Type u_1} {G : Type u_2} {F : Type u_3} [inst : AddCommMonoid M] [inst_1 : AddCommGroup G] {S : AddSubmonoid G}
  [inst_2 : FunLike F G M] [AddHomClass F G M] {f : F}, S.IsLocalizationMap ⇑f ↔ Function.Bijective ⇑f
-- Mathlib.FieldTheory.RatFunc.Luroth
/-- The integer normalization of `φ` as a bivariate polynomial.  -/
_private.Mathlib.FieldTheory.RatFunc.Luroth.0.RatFunc.Luroth.Φ' : {K : Type u_1} → [inst : Field K] → IntermediateField K (RatFunc K) → Polynomial (Polynomial K)
-- Mathlib.GroupTheory.Exponent
/-- If there exists a multiplication-preserving equivalence between `G` and `H`,
then the exponent of `G` is equal to the exponent of `H`.
 -/
Monoid.exponent_eq_of_mulEquiv : ∀ {G : Type u} [inst : Monoid G] {H : Type u_1} [inst_1 : Monoid H] (e : G ≃* H), Monoid.exponent G = Monoid.exponent H
-- Mathlib.Algebra.Order.Archimedean.Basic
/-- If `a < b * c`, `0 < b ≤ 1` and `0 < c < 1`, then there is a power `c ^ n` with `n : ℕ`
strictly between `a` and `b`.  -/
exists_pow_btwn_of_lt_mul : ∀ {K : Type u_4} [inst : Semifield K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] [Archimedean K] [ExistsAddOfLE K]
  {a b c : K}, a < b * c → 0 < b → b ≤ 1 → 0 < c → c < 1 → ∃ n, a < c ^ n ∧ c ^ n < b
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : AlgebraicGeometry.IsOpenImmersion f],
  CategoryTheory.Limits.HasPullback g f
-- Mathlib.CategoryTheory.Limits.Final
/-- When `F : C ⥤ D` is initial, and `G : D ⥤ E` has a limit, then `F ⋙ G` has a limit also and
`limit (F ⋙ G) ≅ limit G`.  -/
CategoryTheory.Functor.Initial.limitIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) →
          [inst_2 : F.Initial] →
            {E : Type u₃} →
              [inst_3 : CategoryTheory.Category.{v₃, u₃} E] →
                (G : CategoryTheory.Functor D E) →
                  [inst_4 : CategoryTheory.Limits.HasLimit G] →
                    CategoryTheory.Limits.limit (F.comp G) ≅ CategoryTheory.Limits.limit G
-- Mathlib.Tactic.Order.Graph.Tarjan
Mathlib.Tactic.Order.Graph.TarjanState.mk.injEq : ∀ (toDFSState : Mathlib.Tactic.Order.Graph.DFSState) (id lowlink : Std.HashMap ℕ ℕ) (stack : Array ℕ)
  (onStack : Std.HashSet ℕ) (time : ℕ) (toDFSState_1 : Mathlib.Tactic.Order.Graph.DFSState)
  (id_1 lowlink_1 : Std.HashMap ℕ ℕ) (stack_1 : Array ℕ) (onStack_1 : Std.HashSet ℕ) (time_1 : ℕ),
  ({ toDFSState := toDFSState, id := id, lowlink := lowlink, stack := stack, onStack := onStack, time := time } =
      { toDFSState := toDFSState_1, id := id_1, lowlink := lowlink_1, stack := stack_1, onStack := onStack_1,
        time := time_1 }) =
    (toDFSState = toDFSState_1 ∧
      id = id_1 ∧ lowlink = lowlink_1 ∧ stack = stack_1 ∧ onStack = onStack_1 ∧ time = time_1)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.isEmpty_diff_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t₁.isEmpty = true → (t₁ \ t₂).isEmpty = true
-- Mathlib.FieldTheory.Minpoly.Field
minpoly.ne_zero_of_finite : ∀ (A : Type u_1) {B : Type u_2} [inst : Field A] [inst_1 : Ring B] [inst_2 : Algebra A B] (e : B)
  [FiniteDimensional A B], minpoly A e ≠ 0
-- Std.Sat.AIG.If
_private.Std.Sat.AIG.If.0.Std.Sat.AIG.RefVec.ite.match_1.eq_1 : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α)
  (motive : Std.Sat.AIG.RefVec.IfInput aig w → Sort u_1) (discr : aig.Ref) (lhs rhs : aig.RefVec w)
  (h_1 : (discr : aig.Ref) → (lhs rhs : aig.RefVec w) → motive { discr := discr, lhs := lhs, rhs := rhs }),
  (match { discr := discr, lhs := lhs, rhs := rhs } with
    | { discr := discr, lhs := lhs, rhs := rhs } => h_1 discr lhs rhs) =
    h_1 discr lhs rhs
-- Aesop.Util.UnorderedArraySet
/-- O(n*m)  -/
Aesop.UnorderedArraySet.merge : {α : Type u_1} → [inst : BEq α] → Aesop.UnorderedArraySet α → Aesop.UnorderedArraySet α → Aesop.UnorderedArraySet α
-- Mathlib.Analysis.InnerProductSpace.Orthonormal
/-- The double sum of weighted inner products of pairs of vectors from an orthonormal sequence is the
sum of the weights.
 -/
Orthonormal.inner_left_right_finset : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_4} {s : Finset ι} {v : ι → E},
  Orthonormal 𝕜 v → ∀ {a : ι → ι → 𝕜}, ∑ i ∈ s, ∑ j ∈ s, a i j • inner 𝕜 (v j) (v i) = ∑ k ∈ s, a k k
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.DocumentColorOptions : Type
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Defs
IsIntegralClosure.algebraMap_injective : ∀ (A : Type u_1) (R : Type u_2) (B : Type u_3) {inst : CommRing R} {inst_1 : CommSemiring A} {inst_2 : CommRing B}
  {inst_3 : Algebra R B} {inst_4 : Algebra A B} [self : IsIntegralClosure A R B], Function.Injective ⇑(algebraMap A B)
-- Mathlib.Algebra.GroupWithZero.Action.Defs
smul_neg : ∀ {M : Type u_1} {A : Type u_7} [inst : AddGroup A] [inst_1 : DistribSMul M A] (r : M) (x : A), r • -x = -(r • x)
-- Lean.Compiler.ExternAttr
Lean.mkSimpleFnCall : String → List String → String
-- Mathlib.RingTheory.Morita.Matrix
ModuleCat.matrixEquivalence_counitIso : ∀ (R : Type u) {ι : Type v} [inst : Ring R] [inst_1 : Fintype ι] [inst_2 : DecidableEq ι] (i : ι),
  (ModuleCat.matrixEquivalence R i).counitIso = MatrixModCat.counitIso R i
-- Mathlib.CategoryTheory.Skeletal
/-- The thin skeleton is thin.  -/
CategoryTheory.ThinSkeleton.thin : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C], Quiver.IsThin (CategoryTheory.ThinSkeleton C)
-- Batteries.Data.Fin.Coding
_private.Batteries.Data.Fin.Coding.0.Fin.decodePi.match_1.eq_2 : ∀ (n : ℕ) (motive : Fin (n + 1) → Sort u_1) (i : ℕ) (hi : i + 1 < n + 1) (h_1 : (isLt : 0 < n + 1) → motive ⟨0, isLt⟩)
  (h_2 : (i : ℕ) → (hi : i + 1 < n + 1) → motive ⟨i.succ, hi⟩),
  (match ⟨i.succ, hi⟩ with
    | ⟨0, isLt⟩ => h_1 isLt
    | ⟨i.succ, hi⟩ => h_2 i hi) =
    h_2 i hi
-- Mathlib.LinearAlgebra.TensorProduct.Basic
TensorProduct.lift_mk_compr₂ₛₗ : ∀ {R : Type u_1} {R₂ : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7}
  {N : Type u_8} {P₂ : Type u_17} [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N] [inst_4 : AddCommMonoid P₂]
  [inst_5 : Module R M] [inst_6 : Module R N] [inst_7 : Module R₂ P₂] (g : TensorProduct R M N →ₛₗ[σ₁₂] P₂),
  TensorProduct.lift ((TensorProduct.mk R M N).compr₂ₛₗ g) = g
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.mk.congr_simp : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (X : ι → V) (d d_1 : (i j : ι) → X i ⟶ X j)
  (e_d : d = d_1) (shape : ∀ (i j : ι), ¬c.Rel i j → d i j = 0)
  (d_comp_d' : ∀ (i j k : ι), c.Rel i j → c.Rel j k → CategoryTheory.CategoryStruct.comp (d i j) (d j k) = 0),
  { X := X, d := d, shape := shape, d_comp_d' := d_comp_d' } = { X := X, d := d_1, shape := ⋯, d_comp_d' := ⋯ }
-- Lean.Environment
Lean.PersistentEnvExtension.addEntry : {α β σ : Type} →
  (ext : Lean.PersistentEnvExtension α β σ) →
    Lean.Environment →
      β →
        optParam Lean.EnvExtension.AsyncMode ext.toEnvExtension.asyncMode →
          optParam Lean.Name Lean.Name.anonymous → Lean.Environment
-- Aesop.Tree.Data
Aesop.NodeState.instToString : ToString Aesop.NodeState
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.image_eq_preimage_symm : ∀ {R : Type u_4} {S : Type u_5} [inst : Mul R] [inst_1 : Mul S] [inst_2 : Add R] [inst_3 : Add S] (e : R ≃+* S)
  (s : Set R), ⇑e '' s = ⇑e.symm ⁻¹' s
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.rename_polynomial_aeval_X : ∀ (R : Type u) [inst : CommSemiring R] {σ : Type u_2} {τ : Type u_3} (f : σ → τ) (i : σ) (p : Polynomial R),
  (MvPolynomial.rename f) ((Polynomial.aeval (MvPolynomial.X i)) p) = (Polynomial.aeval (MvPolynomial.X (f i))) p
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
StrictAnti.inv : ∀ {α : Type u} {β : Type u_1} [inst : Group α] [inst_1 : Preorder α] [MulLeftStrictMono α] [MulRightStrictMono α]
  [inst_4 : Preorder β] {f : β → α}, StrictAnti f → StrictMono fun x => (f x)⁻¹
-- Mathlib.NumberTheory.Padics.Hensel
_private.Mathlib.NumberTheory.Padics.Hensel.0.newton_seq_norm_le : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : CommSemiring R] [inst_2 : Algebra R ℤ_[p]]
  {F : Polynomial R} {a : ℤ_[p]}
  (hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2) (n : ℕ),
  ‖(Polynomial.aeval (newton_seq_gen✝ hnorm n)) F‖ ≤
    ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2 * T_gen✝ p F a ^ 2 ^ n
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
mem_zmultiples_of_prime_card : ∀ {G : Type u_2} [inst : AddGroup G] {p : ℕ} [hp : Fact (Nat.Prime p)],
  Nat.card G = p → ∀ {g g' : G}, g ≠ 0 → g' ∈ AddSubgroup.zmultiples g
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.mem_modify : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : EquivBEq α] [LawfulHashable α] {k k' : α} {f : β → β},
  m.WF → (k' ∈ Std.DHashMap.Raw.Const.modify m k f ↔ k' ∈ m)
-- Mathlib.Algebra.Order.Group.PosPart
le_iff_oneLePart_leOnePart : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : CommGroup α] [MulLeftMono α] (a b : α), a ≤ b ↔ a⁺ᵐ ≤ b⁺ᵐ ∧ b⁻ᵐ ≤ a⁻ᵐ
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
contMDiffOn_iff_of_mem_maximalAtlas' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {e : OpenPartialHomeomorph M H}
  {e' : OpenPartialHomeomorph M' H'} {f : M → M'} {s : Set M} {n : WithTop ℕ∞},
  e ∈ IsManifold.maximalAtlas I n M →
    e' ∈ IsManifold.maximalAtlas I' n M' →
      s ⊆ e.source →
        Set.MapsTo f s e'.source →
          (ContMDiffOn I I' n f s ↔ ContDiffOn 𝕜 n (↑(e'.extend I') ∘ f ∘ ↑(e.extend I).symm) (↑(e.extend I) '' s))
-- Mathlib.Algebra.Category.Ring.Basic
CommRingCat.of.sizeOf_spec : ∀ (carrier : Type u) [commRing : CommRing carrier],
  sizeOf (CommRingCat.of carrier) = 1 + sizeOf carrier + sizeOf commRing
-- Mathlib.Algebra.Group.Subgroup.MulOpposite
AddSubgroup.opEquiv_symm_apply : ∀ {G : Type u_2} [inst : AddGroup G] (H : AddSubgroup Gᵃᵒᵖ), (RelIso.symm AddSubgroup.opEquiv) H = H.unop
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.monadMap_OptionT : ∀ {m : Type u → Type v} {Pred EPred : Type u} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred]
  (f : {β : Type u} → m β → m β) {α : Type u} (x : OptionT m α) (post : α → Pred) (epost : EPost.Cons✝ Pred EPred),
  ⦃ Std.Internal.Do.wp (f x.run) (Std.Internal.Do.EPost.Cons.pushOption post epost) epost.tail ⦄
    MonadFunctor.monadMap (fun {β} => f) x ⦃ post; epost ⦄
-- Mathlib.RingTheory.Valuation.Basic
Valuation.isEquiv_iff_val_lt_val : ∀ {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀]
  [inst_2 : LinearOrderedCommMonoidWithZero Γ'₀] {v : Valuation R Γ₀} {v' : Valuation R Γ'₀},
  v.IsEquiv v' ↔ ∀ {x y : R}, v x < v y ↔ v' x < v' y
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.transportIso_hom_fiber : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat}
  (x : CategoryTheory.Grothendieck F) {c : C} (α : x.base ≅ c), (x.transportIso α).hom.fiber = CategoryTheory.eqToHom ⋯
-- Mathlib.Combinatorics.SimpleGraph.Diam
SimpleGraph.radius_eq_top_of_not_connected : ∀ {α : Type u_1} {G : SimpleGraph α}, ¬G.Connected → G.radius = ⊤
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.one_sub_X_sq_mul_derivative_derivative_U_eq_poly_in_U : ∀ {R : Type u_1} [inst : CommRing R] (n : ℤ),
  (1 - Polynomial.X ^ 2) * (⇑Polynomial.derivative)^[2] (Polynomial.Chebyshev.U R n) =
    3 * Polynomial.X * Polynomial.derivative (Polynomial.Chebyshev.U R n) - (↑n + 2) * ↑n * Polynomial.Chebyshev.U R n
-- Init.Data.BitVec.Bitblast
/-- This is false if `v < w` and `b = intMin`. See also `signExtend_neg_of_ne_intMin`.  -/
BitVec.signExtend_neg_of_le : ∀ {v w : ℕ}, w ≤ v → ∀ (b : BitVec v), BitVec.signExtend w (-b) = -BitVec.signExtend w b
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get?_empty : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {a : α}, ∅.get? a = none
-- Mathlib.CategoryTheory.Abelian.Exact
/-- A functor preserving zero morphisms, monos, and cokernels preserves homology.  -/
CategoryTheory.Functor.preservesHomology_of_preservesMonos_and_cokernels : ∀ {A : Type u₁} {B : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Abelian A] [inst_3 : CategoryTheory.Abelian B] (L : CategoryTheory.Functor A B)
  [inst_4 : L.PreservesZeroMorphisms] [L.PreservesMonomorphisms]
  [∀ {X Y : A} (f : X ⟶ Y), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) L],
  L.PreservesHomology
-- Init.System.CancelToken
_private.Init.System.CancelToken.0.IO.CancelToken.isSetExport : IO.CancelToken → BaseIO Bool
-- Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit
CategoryTheory.Limits.colimitLimitIso.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} J]
  {K : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} K] [inst_3 : CategoryTheory.Limits.HasLimitsOfShape J C]
  [inst_4 : CategoryTheory.Limits.HasColimitsOfShape K C]
  [inst_5 : CategoryTheory.Limits.PreservesLimitsOfShape J CategoryTheory.Limits.colim]
  (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)),
  CategoryTheory.Limits.colimitLimitIso F =
    (CategoryTheory.Limits.isLimitOfPreserves CategoryTheory.Limits.colim
            (CategoryTheory.Limits.limit.isLimit F)).conePointUniqueUpToIso
        (CategoryTheory.Limits.limit.isLimit (F.comp CategoryTheory.Limits.colim)) ≪≫
      CategoryTheory.Limits.HasLimit.isoOfNatIso (CategoryTheory.Limits.colimitFlipIsoCompColim F).symm
-- Mathlib.Algebra.Order.Ring.StandardPart
ArchimedeanClass.FiniteElement.mk_one : ∀ {K : Type u_1} [inst : LinearOrder K] [inst_1 : Field K] [inst_2 : IsOrderedRing K],
  ArchimedeanClass.FiniteElement.mk 1 ⋯ = 1
-- Mathlib.Algebra.Category.Grp.Basic
AddGrpCat.instInhabited.eq_1 : AddGrpCat.instInhabited = { default := AddGrpCat.of PUnit.{u_1 + 1} }
-- Lean.Parser.Extension
Lean.Parser.ParserExtension.OLeanEntry.parser.sizeOf_spec : ∀ (catName declName : Lean.Name) (prio : ℕ),
  sizeOf (Lean.Parser.ParserExtension.OLeanEntry.parser catName declName prio) =
    1 + sizeOf catName + sizeOf declName + sizeOf prio
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKey_insertIfNew_le_minKey : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β} {he : t ≠ ∅}, (cmp ((t.insertIfNew k v).minKey ⋯) (t.minKey he)).isLE = true
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.sub_domain : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] {σ : R →+* S} {E : Type u_4} [inst_2 : AddCommGroup E]
  [inst_3 : Module R E] {F : Type u_5} [inst_4 : AddCommGroup F] [inst_5 : Module S F] (f g : E →ₛₗ.[σ] F),
  (f - g).domain = f.domain ⊓ g.domain
-- Lean.Server.FileWorker.RequestHandling
_private.Lean.Server.FileWorker.RequestHandling.0.Lean.Server.FileWorker.handleDocumentHighlight.highlightReturn? : Lean.FileMap → String.Pos.Raw → Option Lean.Lsp.Range → Lean.Syntax → Option Lean.Lsp.DocumentHighlight
-- Mathlib.Data.Fintype.Fin
Finset.image_fin_univ : ∀ {n : ℕ}, Finset.image Fin.val Finset.univ = Finset.range n