mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.Truncated.trunc_map_app : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (n m : ℕ)
  (h : autoParam (m ≤ n) CategoryTheory.SimplicialObject.Truncated.trunc._auto_1)
  {X Y : CategoryTheory.Functor (SimplexCategory.Truncated n)ᵒᵖ C} (α : X ⟶ Y) (X_1 : (SimplexCategory.Truncated m)ᵒᵖ),
  ((CategoryTheory.SimplicialObject.Truncated.trunc C n m h).map α).app X_1 =
    α.app (Opposite.op ((SimplexCategory.Truncated.incl m n ⋯).obj (Opposite.unop X_1)))
-- Mathlib.FieldTheory.SplittingField.Construction
Polynomial.SplittingFieldAux.succ : ∀ {K : Type v} [inst : Field K] (n : ℕ) (f : Polynomial K),
  Polynomial.SplittingFieldAux (n + 1) f = Polynomial.SplittingFieldAux n f.removeFactor
-- Mathlib.GroupTheory.MonoidLocalization.Finite
/-- The localization of a finitely generated monoid at a finitely generated submonoid is
finitely generated.  -/
Localization.fg : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} [Monoid.FG M], S.FG → Monoid.FG (Localization S)
-- Mathlib.Probability.Moments.SubGaussian
ProbabilityTheory.HasSubgaussianMGF.memLp : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {c : NNReal},
  ProbabilityTheory.HasSubgaussianMGF X c μ → ∀ (p : NNReal), MeasureTheory.MemLp X (↑p) μ
-- Mathlib.Tactic.Positivity.Basic
Mathlib.Meta.Positivity.min_ne_of_lt_of_ne : ∀ {R : Type u_2} [inst : LinearOrder R] {a b c : R}, c < a → b ≠ c → min a b ≠ c
-- Mathlib.ModelTheory.Encoding
_private.Mathlib.ModelTheory.Encoding.0.FirstOrder.Language.BoundedFormula.listDecode.match_1.eq_6 : ∀ {L : FirstOrder.Language} {α : Type u_3}
  (motive : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ) → Sort u_4)
  (x : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ))
  (h_1 :
    (n : ℕ) →
      (l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)) →
        motive (Sum.inr (Sum.inr n.succ.succ) :: l))
  (h_2 :
    (n₁ : ℕ) →
      (t₁ : L.Term (α ⊕ Fin n₁)) →
        (n₂ : ℕ) →
          (t₂ : L.Term (α ⊕ Fin n₂)) →
            (l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)) →
              motive (Sum.inl ⟨n₁, t₁⟩ :: Sum.inl ⟨n₂, t₂⟩ :: l))
  (h_3 :
    (n : ℕ) →
      (R : L.Relations n) →
        (k : ℕ) →
          (l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)) →
            motive (Sum.inr (Sum.inl ⟨n, R⟩) :: Sum.inr (Sum.inr k) :: l))
  (h_4 : (l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)) → motive (Sum.inr (Sum.inr 0) :: l))
  (h_5 : (l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)) → motive (Sum.inr (Sum.inr 1) :: l))
  (h_6 : (x : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)) → motive x),
  (∀ (n : ℕ) (l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
      x = Sum.inr (Sum.inr n.succ.succ) :: l → False) →
    (∀ (n₁ : ℕ) (t₁ : L.Term (α ⊕ Fin n₁)) (n₂ : ℕ) (t₂ : L.Term (α ⊕ Fin n₂))
        (l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
        x = Sum.inl ⟨n₁, t₁⟩ :: Sum.inl ⟨n₂, t₂⟩ :: l → False) →
      (∀ (n : ℕ) (R : L.Relations n) (k : ℕ) (l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
          x = Sum.inr (Sum.inl ⟨n, R⟩) :: Sum.inr (Sum.inr k) :: l → False) →
        (∀ (l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
            x = Sum.inr (Sum.inr 0) :: l → False) →
          (∀ (l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
              x = Sum.inr (Sum.inr 1) :: l → False) →
            (match x with
              | Sum.inr (Sum.inr n.succ.succ) :: l => h_1 n l
              | Sum.inl ⟨n₁, t₁⟩ :: Sum.inl ⟨n₂, t₂⟩ :: l => h_2 n₁ t₁ n₂ t₂ l
              | Sum.inr (Sum.inl ⟨n, R⟩) :: Sum.inr (Sum.inr k) :: l => h_3 n R k l
              | Sum.inr (Sum.inr 0) :: l => h_4 l
              | Sum.inr (Sum.inr 1) :: l => h_5 l
              | x => h_6 x) =
              h_6 x
-- Mathlib.GroupTheory.GroupExtension.Defs
GroupExtension.Equiv.rightHom_map : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : Group N] [inst_1 : Group E] [inst_2 : Group G]
  {S : GroupExtension N E G} {E' : Type u_4} [inst_3 : Group E'] {S' : GroupExtension N E' G} (equiv : S.Equiv S')
  (e : E), S'.rightHom (equiv e) = S.rightHom e
-- Init.Data.Vector.MapIdx
Array.mapIdx_toVector : ∀ {α : Type u_1} {β : Type u_2} {f : ℕ → α → β} {xs : Array α},
  Vector.mapIdx f xs.toVector = Vector.cast ⋯ (Array.mapIdx f xs).toVector
-- Mathlib.MeasureTheory.Group.Arithmetic
/-- Compositional version of `Measurable.smul` for use by `fun_prop`.  -/
Measurable.smul' : ∀ {M : Type u_2} {X : Type u_3} {α : Type u_4} {β : Type u_5} [inst : MeasurableSpace X] [inst_1 : SMul M X]
  {m : MeasurableSpace α} {mβ : MeasurableSpace β} [inst_2 : MeasurableSpace M] [MeasurableSMul₂ M X] {f : α → β → M}
  {g : α → β → X} {h : α → β}, Measurable ↿f → Measurable ↿g → Measurable h → Measurable fun a => (f a • g a) (h a)
-- Mathlib.Topology.MetricSpace.Congruence
/-- Congruence follows from pairwise preserved distance. Backward direction of
`congruent_iff_pairwise_dist_eq`.  -/
Congruent.of_pairwise_dist_eq : ∀ {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} {v₁ : ι → P₁} {v₂ : ι → P₂} [inst : PseudoMetricSpace P₁]
  [inst_1 : PseudoMetricSpace P₂], (Pairwise fun i₁ i₂ => dist (v₁ i₁) (v₁ i₂) = dist (v₂ i₁) (v₂ i₂)) → Congruent v₁ v₂
-- Mathlib.RingTheory.DedekindDomain.LinearDisjoint
/-- Let `A ⊆ B` be a finite extension of Dedekind domains and assume that `A ⊆ R₁, R₂ ⊆ B` are two
subrings such that `Frac R₁ ⊔ Frac R₂ = Frac B`, `Frac R₁` and `Frac R₂` are linearly disjoint
over `Frac A`, and that `𝓓(R₁/A)` and `𝓓(R₂/A)` are coprime where `𝓓` denotes the different ideal
and `Frac R` denotes the fraction field of a domain `R`.
We have `𝓓(B/A) = 𝓓(R₁/A) * 𝓓(R₂/A)`.
 -/
IsDedekindDomain.differentIdeal_eq_differentIdeal_mul_differentIdeal_of_isCoprime : ∀ (A : Type u_1) (B : Type u_2) {K : Type u_3} {L : Type u_4} [inst : CommRing A] [inst_1 : Field K]
  [inst_2 : Algebra A K] [IsFractionRing A K] [inst_4 : CommRing B] [inst_5 : Field L] [inst_6 : Algebra B L]
  [inst_7 : Algebra A L] [inst_8 : Algebra K L] [FiniteDimensional K L] [inst_10 : IsScalarTower A K L] (R₁ : Type u_5)
  (R₂ : Type u_6) [inst_11 : CommRing R₁] [inst_12 : CommRing R₂] [inst_13 : IsDomain R₁] [inst_14 : Algebra A R₁]
  [inst_15 : Algebra A R₂] [inst_16 : Algebra R₁ B] [inst_17 : Algebra R₂ B] [inst_18 : Algebra R₁ L]
  [inst_19 : Algebra R₂ L] [IsScalarTower A R₁ L] [IsScalarTower R₁ B L] [IsScalarTower R₂ B L] [Module.Finite A R₂]
  {F₁ F₂ : IntermediateField K L} [inst_24 : Algebra R₁ ↥F₁] [inst_25 : Algebra R₂ ↥F₂] [Module.IsTorsionFree R₁ ↥F₁]
  [IsScalarTower A (↥F₂) L] [IsScalarTower A R₂ ↥F₂] [IsScalarTower R₁ (↥F₁) L] [IsScalarTower R₂ (↥F₂) L]
  [Algebra.IsSeparable K ↥F₂] [Algebra.IsSeparable (↥F₁) L] [inst_33 : IsDomain A] [inst_34 : IsDedekindDomain B]
  [inst_35 : IsDedekindDomain R₁] [inst_36 : IsDedekindDomain R₂] [IsFractionRing B L] [IsFractionRing R₁ ↥F₁]
  [IsFractionRing R₂ ↥F₂] [IsIntegrallyClosed A] [IsIntegralClosure B R₁ L] [inst_42 : Module.IsTorsionFree R₁ B]
  [inst_43 : Module.IsTorsionFree R₂ B], ⋯
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoDiv_add_zsmul : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α) (m : ℤ), toIcoDiv hp a (b + m • p) = toIcoDiv hp a b + m
-- Mathlib.Algebra.GCDMonoid.Finset
Finset.gcd_union : ∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] {s₁ s₂ : Finset β}
  {f : β → α} [inst_2 : DecidableEq β], (s₁ ∪ s₂).gcd f = gcd (s₁.gcd f) (s₂.gcd f)
-- Mathlib.RepresentationTheory.Continuous.TopRep
TopRep.smul_comp' : ∀ {k : Type u} {G : Type v} [inst : TopologicalSpace k] [inst_1 : CommRing k] [inst_2 : Monoid G] (A B C : TopRep k G)
  (r : k) (f : A ⟶ B) (g : B ⟶ C),
  CategoryTheory.CategoryStruct.comp (r • f) g = r • CategoryTheory.CategoryStruct.comp f g
-- Mathlib.Algebra.Exact.Basic
Function.Injective.comp_exact_iff_exact : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} {P : Type u_6} {P' : Type u_7} [inst : Semiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : AddCommMonoid P']
  [inst_5 : Module R M] [inst_6 : Module R N] [inst_7 : Module R P] [inst_8 : Module R P'] {f : M →ₗ[R] N}
  {g : N →ₗ[R] P} {i : P →ₗ[R] P'}, Function.Injective ⇑i → (Function.Exact ⇑f ⇑(i ∘ₗ g) ↔ Function.Exact ⇑f ⇑g)
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
/-- A commutative simple group is a finite group.  -/
IsSimpleAddGroup.finite : ∀ {α : Type u_1} [inst : AddCommGroup α] [IsSimpleAddGroup α], Finite α
-- Mathlib.Algebra.Group.Commute.Defs
AddCommute.eq_1 : ∀ {S : Type u_3} [inst : Add S] (a b : S), AddCommute a b = AddSemiconjBy a b b
-- Mathlib.Geometry.Manifold.Diffeomorph
ModelWithCorners.transContinuousLinearEquiv_range : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {H : Type u_5}
  [inst_5 : TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) (e : E ≃L[𝕜] E'),
  Set.range ↑(I.transContinuousLinearEquiv e) = ⇑e '' Set.range ↑I
-- Mathlib.CategoryTheory.Category.Cat
CategoryTheory.Cat.Hom.isoMk_hom : ∀ {C D : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Category.{v, u} D]
  {F G : CategoryTheory.Functor C D} (e : F ≅ G),
  (CategoryTheory.Cat.Hom.isoMk e).hom = CategoryTheory.NatTrans.toCatHom₂ e.hom
-- Init.Data.Nat.Internal.SOM
Nat.Internal.SOM.Poly.mul_denote : ∀ (ctx : Nat.Internal.Linear.Context) (p₁ p₂ : Nat.Internal.SOM.Poly),
  Nat.Internal.SOM.Poly.denote ctx (p₁.mul p₂) =
    Nat.Internal.SOM.Poly.denote ctx p₁ * Nat.Internal.SOM.Poly.denote ctx p₂
-- Mathlib.CategoryTheory.Shift.ShiftedHomOpposite
CategoryTheory.ShiftedHom.opEquiv_symm_add : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ] {X Y : C}
  [inst_2 : CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] {n : ℤ}
  (x y : CategoryTheory.ShiftedHom (Opposite.op Y) (Opposite.op X) n),
  (CategoryTheory.ShiftedHom.opEquiv n).symm (x + y) =
    (CategoryTheory.ShiftedHom.opEquiv n).symm x + (CategoryTheory.ShiftedHom.opEquiv n).symm y
-- Mathlib.Data.Set.SymmDiff
Set.mem_bihimp_iff : ∀ {α : Type u} {a : α} {s t : Set α}, a ∈ bihimp s t ↔ (a ∈ s ↔ a ∈ t)
-- Mathlib.GroupTheory.GroupAction.ConjAct
ConjAct.instDivInvMonoid : {G : Type u_3} → [DivInvMonoid G] → DivInvMonoid (ConjAct G)
-- Mathlib.AlgebraicGeometry.Cover.Sigma
AlgebraicGeometry.Scheme.Cover.sigmaFunctor_obj : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {S : AlgebraicGeometry.Scheme}
  [inst : AlgebraicGeometry.IsZariskiLocalAtSource P] [inst_1 : UnivLE.{v, u}]
  (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) S),
  AlgebraicGeometry.Scheme.Cover.sigmaFunctor.obj 𝒰 = 𝒰.sigma
-- Lean.Data.Trie
Lean.Data.Trie.node1.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (a : Option α) (a_1 : UInt8) (a_2 : Lean.Data.Trie α),
  sizeOf (Lean.Data.Trie.node1 a a_1 a_2) = 1 + sizeOf a + sizeOf a_1 + sizeOf a_2
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteGrp.instReflectsIsomorphismsForgetContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfinite : (CategoryTheory.forget ProfiniteGrp.{u}).ReflectsIsomorphisms
-- Mathlib.Topology.Compactness.Lindelof
/-- `Filter.coLindelof` is the filter generated by complements to Lindelöf sets.  -/
Filter.coLindelof : (X : Type u_2) → [TopologicalSpace X] → Filter X
-- Mathlib.Algebra.Algebra.Prod
AlgHom.prodEquiv_symm_apply : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : Semiring B] [inst_4 : Algebra R B] [inst_5 : Semiring C] [inst_6 : Algebra R C]
  (f : A →ₐ[R] B × C), AlgHom.prodEquiv.symm f = ((AlgHom.fst R B C).comp f, (AlgHom.snd R B C).comp f)
-- Batteries.Data.Fin.Lemmas
Fin.isSome_find?_of_eq_true : ∀ {n : ℕ} {i : Fin n} {p : Fin n → Bool}, p i = true → (Fin.find? p).isSome = true
-- Mathlib.Topology.UniformSpace.Completion
_private.Mathlib.Topology.UniformSpace.Completion.0.CauchyFilter.subset_gen_relComp : ∀ {α : Type u} [inst : UniformSpace α] {s t : SetRel α α},
  (CauchyFilter.gen s).comp (CauchyFilter.gen t) ⊆ CauchyFilter.gen (s.comp t)
-- Mathlib.Logic.IsEmpty.Defs
instIsEmptyPSum : ∀ {α : Sort u} {β : Sort v} [IsEmpty α] [IsEmpty β], IsEmpty (α ⊕' β)
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
/-- `BilinForm.toMatrix b` is the equivalence between `R`-bilinear forms on `M` and
`n`-by-`n` matrices with entries in `R`, if `b` is an `R`-basis for `M`.  -/
LinearMap.BilinForm.toMatrix : {R₁ : Type u_1} →
  {M₁ : Type u_2} →
    [inst : CommSemiring R₁] →
      [inst_1 : AddCommMonoid M₁] →
        [inst_2 : Module R₁ M₁] →
          {n : Type u_5} →
            [Fintype n] → [DecidableEq n] → Module.Basis n R₁ M₁ → LinearMap.BilinForm R₁ M₁ ≃ₗ[R₁] Matrix n n R₁
-- Mathlib.Analysis.Normed.Module.Multilinear.Curry
/-- A continuous multilinear map with variables indexed by `ι` taking values in the space of
continuous multilinear maps with variables indexed by `ι'` defines a continuous multilinear map with
variables indexed by `ι ⊕ ι'`.  -/
ContinuousMultilinearMap.uncurrySum : {𝕜 : Type u} →
  {ι : Type v} →
    {ι' : Type v'} →
      {G : Type wG} →
        {G' : Type wG'} →
          [Fintype ι] →
            [Fintype ι'] →
              [inst : NontriviallyNormedField 𝕜] →
                [inst_1 : NormedAddCommGroup G] →
                  [inst_2 : NormedSpace 𝕜 G] →
                    [inst_3 : NormedAddCommGroup G'] →
                      [inst_4 : NormedSpace 𝕜 G'] →
                        ContinuousMultilinearMap 𝕜 (fun x => G) (ContinuousMultilinearMap 𝕜 (fun x => G) G') →
                          ContinuousMultilinearMap 𝕜 (fun x => G) G'
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.String.Legacy.anyAux.eq_def : ∀ (s : String) (stopPos : String.Pos.Raw) (p : Char → Bool) (i : String.Pos.Raw),
  String.Legacy.anyAux s stopPos p i =
    if h : i < stopPos then
      if p (String.Pos.Raw.get s i) = true then true
      else
        have this := ⋯;
        String.Legacy.anyAux s stopPos p (String.Pos.Raw.next s i)
    else false
-- Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
NumberField.IsTotallyReal.isReal : ∀ {K : Type u_1} {inst : Field K} [self : NumberField.IsTotallyReal K] (v : NumberField.InfinitePlace K), v.IsReal
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey?_erase_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  (t.erase k).getKey? k = none
-- Mathlib.Data.Finset.Empty
Finset.nonempty_of_ne_empty : ∀ {α : Type u_1} {s : Finset α}, s ≠ ∅ → s.Nonempty
-- Mathlib.RingTheory.Smooth.StandardSmoothCotangent
/-- **Alias** of `Algebra.IsStandardSmoothOfRelativeDimension.subsingleton_kaehlerDifferential`. -/
Algebra.IsStandardSmoothOfRelationDimension.subsingleton_kaehlerDifferential : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.IsStandardSmoothOfRelativeDimension 0 R S], Subsingleton Ω[S⁄R]
-- Mathlib.Tactic.Explode.Datatypes
/-- Instead of simply keeping a list of entries (`List Entry`), we create a datatype `Entries`
that allows us to compare expressions faster.  -/
Mathlib.Explode.Entries : Type
-- Mathlib.Topology.Algebra.Algebra.Equiv
ContinuousAlgEquiv.coe_injective : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : TopologicalSpace A] [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A]
  [inst_6 : Algebra R B], Function.Injective ContinuousAlgEquiv.toContinuousAlgHom
-- Mathlib.Algebra.Ring.Basic
MulOpposite.instHasDistribNeg : {α : Type u_3} → [inst : Mul α] → [HasDistribNeg α] → HasDistribNeg αᵐᵒᵖ
-- Mathlib.Tactic.Linter.DocPrime
/-- The "docPrime" linter emits a warning on declarations that have no doc-string and whose
name ends with a `'`.

The file `scripts/nolints_prime_decls.txt` contains a list of temporary exceptions to this linter.
This list should not be appended to, and become emptied over time.
 -/
Mathlib.Linter.linter.docPrime : Lean.Option Bool
-- Mathlib.Data.ENat.Lattice
ENat.iSup_mul : ∀ {ι : Sort u_2} (f : ι → ℕ∞) (a : ℕ∞), (⨆ i, f i) * a = ⨆ i, f i * a
-- Init.Data.String.Subslice
/-- Creates a `String` from a `Subslice` by copying out the bytes.
 -/
String.Slice.Subslice.copy : {s : String.Slice} → s.Subslice → String
-- Init.Data.Array.Erase
Array.set_eraseIdx_le : ∀ {α : Type u_1} {xs : Array α} {i : ℕ} {w : i < xs.size} {j : ℕ} {a : α},
  i ≤ j → ∀ (hj : j < (xs.eraseIdx i w).size), (xs.eraseIdx i w).set j a hj = (xs.set (j + 1) a ⋯).eraseIdx i ⋯
-- Aesop.Script.SScript
_private.Aesop.Script.SScript.0.Aesop.Script.SScript.render.go : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadError m] →
      [Lean.MonadQuotation m] → Array Lean.Syntax.Tactic → Aesop.Script.SScript → m (Array Lean.Syntax.Tactic)
-- Mathlib.Analysis.Analytic.Order
/-- The analytic order of the function `(· - c)` at `x` is zero if `x ≠ c`.  -/
analyticOrderAt_id_sub_const_of_ne : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {c x : 𝕜}, x ≠ c → analyticOrderAt (fun x => x - c) x = 0
-- Std.Data.HashMap.Lemmas
Std.HashMap.map_id_equiv : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β},
  (Std.HashMap.map (fun x v => v) m).Equiv m
-- Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
MeasureTheory.charFunDual_apply : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {mE : MeasurableSpace E}
  {μ : MeasureTheory.Measure E} (L : StrongDual ℝ E),
  MeasureTheory.charFunDual μ L = ∫ (v : E), Complex.exp (↑(L v) * Complex.I) ∂μ
-- Mathlib.Combinatorics.Matroid.Minor.Contract
Matroid.contract_isColoop_iff : ∀ {α : Type u_1} {M : Matroid α} {e : α} {C : Set α}, (M.contract C).IsColoop e ↔ M.IsColoop e ∧ e ∉ C
-- Init.Data.BitVec.Lemmas
BitVec.toNat_twoPow : ∀ (w i : ℕ), (BitVec.twoPow w i).toNat = 2 ^ i % 2 ^ w
-- Batteries.Data.Fin.Coding
_private.Batteries.Data.Fin.Coding.0.Fin.encodePi.match_5.eq_1 : ∀ (motive : (n : ℕ) → (f : Fin n → ℕ) → ((i : Fin n) → Fin (f i)) → Sort u_1) (x : Fin 0 → ℕ)
  (x_1 : (i : Fin 0) → Fin (x i)) (h_1 : (x : Fin 0 → ℕ) → (x_2 : (i : Fin 0) → Fin (x i)) → motive 0 x x_2)
  (h_2 : (n : ℕ) → (f : Fin (n + 1) → ℕ) → (x : (i : Fin (n + 1)) → Fin (f i)) → motive n.succ f x),
  (match 0, x, x_1 with
    | 0, x, x_2 => h_1 x x_2
    | n.succ, f, x => h_2 n f x) =
    h_1 x x_1
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.isLittleO_pi : ∀ {α : Type u_1} {F' : Type u_7} [inst : SeminormedAddCommGroup F'] {g' : α → F'} {l : Filter α} {ι : Type u_17}
  [inst_1 : Fintype ι] {E' : ι → Type u_18} [inst_2 : (i : ι) → SeminormedAddCommGroup (E' i)] {f : α → (i : ι) → E' i},
  f =o[l] g' ↔ ∀ (i : ι), (fun x => f x i) =o[l] g'
-- Mathlib.Algebra.Category.Ring.Basic
/-- Turn a morphism in `RingCat` back into a `RingHom`.  -/
RingCat.Hom.hom : {R S : RingCat} → R.Hom S → ↑R →+* ↑S
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.mrange_fst : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N],
  AddMonoidHom.mrange (AddMonoidHom.fst M N) = ⊤
-- Mathlib.Topology.Defs.Ultrafilter
/-- If `F` is an ultrafilter, then `Filter.Ultrafilter.lim F` is a limit of the filter, if it exists.
Note that dot notation `F.lim` can be used for `F : Filter.Ultrafilter X`.
 -/
Ultrafilter.lim : {X : Type u_1} → [TopologicalSpace X] → Ultrafilter X → X
-- Mathlib.GroupTheory.Torsion
IsMulTorsion.torsionMulEquiv_symm_apply_coe : ∀ {G : Type u_1} [inst : CommMonoid G] (tG : IsMulTorsion G) (a : G), ↑(tG.torsionMulEquiv.symm a) = a
-- Mathlib.GroupTheory.Perm.Fin
Fin.cycleIcc_comp_succAbove : ∀ {n : ℕ} (i j : Fin (n + 1)), i ≤ j → ⇑(i.cycleIcc j) ∘ j.succAbove = i.succAbove
-- Mathlib.SetTheory.Cardinal.Cofinality.Basic
Order.one_lt_cof : ∀ {α : Type u} [inst : Preorder α] [Nonempty α] [h : NoTopOrder α], 1 < Order.cof α
-- Mathlib.LinearAlgebra.AffineSpace.Centroid
/-- `centroidWeights` at any point.  -/
Finset.centroidWeights_apply : ∀ (k : Type u_1) [inst : DivisionRing k] {ι : Type u_4} (s : Finset ι) (i : ι),
  Finset.centroidWeights k s i = (↑s.card)⁻¹
-- Mathlib.Topology.Sheaves.Limits
TopCat.instHasLimitsPresheaf : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimits C] (X : TopCat),
  CategoryTheory.Limits.HasLimits (TopCat.Presheaf C X)
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.NatTrans.removeUnop_id : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ),
  CategoryTheory.NatTrans.removeUnop (CategoryTheory.CategoryStruct.id F.unop) = CategoryTheory.CategoryStruct.id F
-- Mathlib.AlgebraicGeometry.Modules.Tilde
SheafOfModules.IsQuasicoherent.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : ∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat]
  [inst_2 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] (M M_1 : SheafOfModules R),
  M = M_1 → M.IsQuasicoherent = M_1.IsQuasicoherent
-- Mathlib.CategoryTheory.Adjunction.PartialAdjoint
CategoryTheory.Functor.isRightAdjoint_iff_leftAdjointObjIsDefined_eq_top : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor D C), F.IsRightAdjoint ↔ F.leftAdjointObjIsDefined = ⊤
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.maxKeyD_le_maxKeyD_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t ≠ ∅ → ∀ {k : α} {v : β} {fallback : α}, (cmp (t.maxKeyD fallback) ((t.insert k v).maxKeyD fallback)).isLE = true
-- Lean.Language.Basic
Lean.Language.SnapshotTask.ReportingRange.inherit.sizeOf_spec : sizeOf Lean.Language.SnapshotTask.ReportingRange.inherit = 1
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Context : Type u → Type u
-- Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Ideal.height_le_card_of_mem_minimalPrimes_span_finset : ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] {p : Ideal R} {s : Finset R},
  p ∈ (Ideal.span ↑s).minimalPrimes → p.height ≤ ↑s.card
-- Lean.Meta.AppBuilder
/-- Returns `Decidable.decide p`  -/
Lean.Meta.mkDecide : Lean.Expr → Lean.MetaM Lean.Expr
-- Init.Data.String.Lemmas.Pattern.Find.Pred
String.Slice.Pos.find?_prop_eq_none_iff_of_splits : ∀ {p : Char → Prop} [inst : DecidablePred p] {s : String.Slice} {pos : s.Pos} {t u : String},
  pos.Splits t u → (pos.find? p = none ↔ ∀ c ∈ u.toList, ¬p c)
-- Mathlib.Combinatorics.Quiver.Symmetric
/-- `lift φ` is the only prefunctor extending `φ` and preserving reverses.  -/
Quiver.Symmetrify.lift_unique : ∀ {V : Type u_2} [inst : Quiver V] {V' : Type u_4} [inst_1 : Quiver V'] [inst_2 : Quiver.HasReverse V'] (φ : V ⥤q V')
  (Φ : Quiver.Symmetrify V ⥤q V'),
  Quiver.Symmetrify.of ⋙q Φ = φ →
    (∀ {X Y : Quiver.Symmetrify V} (f : X ⟶ Y), Φ.map (Quiver.reverse f) = Quiver.reverse (Φ.map f)) →
      Φ = Quiver.Symmetrify.lift φ
-- Init.Data.String.Basic
String.Pos.le_cast_iff : ∀ {s t : String} {pos : t.Pos} {pos' : s.Pos} {h : s = t}, pos ≤ pos'.cast h ↔ pos.cast ⋯ ≤ pos'
-- Mathlib.Tactic.ComputeDegree
Mathlib.Tactic.ComputeDegree.coeff_mul_add_of_le_natDegree_of_eq_ite : ∀ {R : Type u_1} [inst : Semiring R] {d df dg : ℕ} {a b : R} {f g : Polynomial R},
  f.natDegree ≤ df →
    g.natDegree ≤ dg →
      f.coeff df = a → g.coeff dg = b → df + dg ≤ d → (f * g).coeff d = if d = df + dg then a * b else 0