mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Equivalence.ε_comp_map_ε_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D] (e : C ≌ D)
  [inst_4 : e.functor.Monoidal] [inst_5 : e.inverse.Monoidal] [e.IsMonoidal] {Z : C}
  (h : e.inverse.obj (e.functor.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε e.inverse)
      (CategoryTheory.CategoryStruct.comp (e.inverse.map (CategoryTheory.Functor.LaxMonoidal.ε e.functor)) h) =
    CategoryTheory.CategoryStruct.comp (e.unit.app (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) h
-- Mathlib.Data.Matrix.Basis
Matrix.of_symm_single : ∀ {m : Type u_2} {n : Type u_3} {α : Type u_7} [inst : DecidableEq m] [inst_1 : DecidableEq n] [inst_2 : Zero α] (i : m)
  (j : n) (a : α), Matrix.of.symm (Matrix.single i j a) = Pi.single i (Pi.single j a)
-- Mathlib.CategoryTheory.Abelian.Projective.Ext
CategoryTheory.ProjectiveResolution.extAddEquivCohomologyClass_symm_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X Y : C} (R : CategoryTheory.ProjectiveResolution X) {n : ℕ}
  (a : CochainComplex.HomComplex.CohomologyClass R.cochainComplex ((CochainComplex.singleFunctor C 0).obj Y) ↑n),
  R.extAddEquivCohomologyClass.symm a = R.extEquivCohomologyClass.symm a
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getD_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] {f : α → β → γ} {k : α} {fallback : γ},
  (Std.ExtTreeMap.map f t).getD k fallback = (Option.map (f k) t[k]?).getD fallback
-- Init.Data.UInt.Lemmas
UInt16.toUInt8_eq : ∀ (a b : UInt16), a.toUInt8 = b.toUInt8 ↔ a % 256 = b % 256
-- Mathlib.Order.Hom.Lattice
SupHom.comp_apply : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Max α] [inst_1 : Max β] [inst_2 : Max γ] (f : SupHom β γ)
  (g : SupHom α β) (a : α), (f.comp g) a = f (g a)
-- Std.Data.DHashMap.Raw
/-- Checks if a mapping for the given key exists and returns the key-value pair if it does, otherwise panics.
The key in the returned pair will be `BEq` to the input `a`.
 -/
Std.DHashMap.Raw.getEntry! : {α : Type u} →
  {β : α → Type v} → [BEq α] → [Hashable α] → [Inhabited ((a : α) × β a)] → Std.DHashMap.Raw α β → α → (a : α) × β a
-- Mathlib.GroupTheory.ResiduallyFinite
/-- If `G` is residually finite, for every pair of distinct elements `g`, `h` there exists a finite
index normal subgroup `H` such that `g` and `h` differ in the quotient `G ⧸ H`.  -/
Group.exists_finiteIndexNormalSubgroup_of_residuallyFinite : ∀ {G : Type u_1} [inst : Group G] [Group.ResiduallyFinite G] (g h : G), g ≠ h → ∃ H, ↑g ≠ ↑h
-- Mathlib.Analysis.Calculus.ContDiff.CPolynomial
CPolynomialAt.contDiffAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type v} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {x : E}, CPolynomialAt 𝕜 f x → ∀ {n : WithTop ℕ∞}, ContDiffAt 𝕜 n f x
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.inv_def : ∀ {ι : Type u_1} (G : ι → Type u_4) [inst : (i : ι) → Group (G i)] (x : Monoid.CoprodI G),
  x⁻¹ =
    MulOpposite.unop
      ((Monoid.CoprodI.lift fun i => (MonoidHom.op Monoid.CoprodI.of).comp (MulEquiv.inv' (G i)).toMonoidHom) x)
-- Mathlib.Analysis.Matrix.Spectrum
/-- rank of a Hermitian matrix is the number of nonzero eigenvalues of the Hermitian matrix  -/
Matrix.IsHermitian.rank_eq_card_non_zero_eigs : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {n : Type u_2} [inst_1 : Fintype n] {A : Matrix n n 𝕜} [inst_2 : DecidableEq n]
  (hA : A.IsHermitian), A.rank = Fintype.card { i // hA.eigenvalues i ≠ 0 }
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.eq_empty_iff_size_eq_zero : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α],
  m = ∅ ↔ m.size = 0
-- Mathlib.Data.Set.Operations
/-- Restriction of `f` to `s` factors through `s.imageFactorization f : s → f '' s`.  -/
Set.imageFactorization : {α : Type u} → {β : Type v} → (f : α → β) → (s : Set α) → ↑s → ↑(f '' s)
-- Std.Internal.Do.Order.Lemmas
Std.Internal.Do.CompleteLattice.meet_le_of_le_himp : ∀ {l : Type u} [inst : Lean.Order.CompleteLattice l] {P Q R : l}
  [∀ (a : l), Lean.Order.PreservesSup (Lean.Order.meet a)],
  Lean.Order.PartialOrder.rel P (Lean.Order.himp Q R) → Lean.Order.PartialOrder.rel (Lean.Order.meet P Q) R
-- Init.Data.List.Lemmas
List.getElem_dropLast : ∀ {α : Type u_1} {xs : List α} {i : ℕ} (h : i < xs.dropLast.length), xs.dropLast[i] = xs[i]
-- Lean.Syntax
Lean.SyntaxNode.getKind : Lean.SyntaxNode → Lean.SyntaxNodeKind
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.contains_diff : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α}, (m₁ \ m₂).contains k = (m₁.contains k && !m₂.contains k)
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.FinalizeContext.elabs : Lean.Elab.Command.FinalizeContext✝ → Array Lean.Elab.Command.InductiveElabStep2
-- Init.Data.SInt.Lemmas
ISize.neg_mul : ∀ (a b : ISize), -a * b = -(a * b)
-- Init.System.IO
/-- Runs a `BaseIO` action, which cannot throw an exception, as an `IO` action.

This function is usually used implicitly via [automatic monadic
lifting](https://lean-lang.org/doc/reference/4.33.0/find/?domain=Verso.Genre.Manual.section&name=lifting-monads) rather than being called explicitly.
 -/
BaseIO.toIO : {α : Type} → BaseIO α → IO α
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.ideal_mono : ∀ {X : AlgebraicGeometry.Scheme}, Monotone AlgebraicGeometry.Scheme.IdealSheafData.ideal
-- Mathlib.Order.Fin.Basic
Fin.valOrderEmb_apply : ∀ (n : ℕ) (self : Fin n), (Fin.valOrderEmb n) self = ↑self
-- Mathlib.CategoryTheory.Limits.Final
/-- The functor `Grothendieck.map α` for a natural transformation `α : F ⟶ G`, with
`F G : C ⥤ Cat`, is final if for each `X : C`, the functor `α.app X` is final.  -/
CategoryTheory.Grothendieck.final_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {F G : CategoryTheory.Functor C CategoryTheory.Cat}
  (α : F ⟶ G) [hα : ∀ (X : C), (α.app X).toFunctor.Final], (CategoryTheory.Grothendieck.map α).Final
-- Mathlib.GroupTheory.Exponent
AddGroup.exponent_dvd_sub_iff_zsmul_eq_zsmul : ∀ {G : Type u} [inst : AddGroup G] {n m : ℤ}, ↑(AddMonoid.exponent G) ∣ n - m ↔ ∀ (g : G), n • g = m • g
-- Mathlib.Algebra.GroupWithZero.Associated
DvdNotUnit.eq_1 : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] (a b : α), DvdNotUnit a b = (a ≠ 0 ∧ ∃ x, ¬IsUnit x ∧ b = a * x)
-- Mathlib.GroupTheory.FiniteIndexNormalSubgroup
FiniteIndexNormalAddSubgroup.ext_iff : ∀ {G : Type u_1} {inst : AddGroup G} {x y : FiniteIndexNormalAddSubgroup G}, x = y ↔ x.carrier = y.carrier
-- Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
AlgebraicGeometry.HasRingHomProperty.of_isOpenImmersion : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme}
  {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop}
  [AlgebraicGeometry.HasRingHomProperty P Q] {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y},
  (RingHom.ContainsIdentities fun {R S} [CommRing R] [CommRing S] => Q) → ∀ [AlgebraicGeometry.IsOpenImmersion f], P f
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr
Std.Tactic.BVDecide.BVExpr.Cache.Inv_empty : ∀ {assign : Std.Tactic.BVDecide.BVExpr.Assignment} (aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit),
  Std.Tactic.BVDecide.BVExpr.Cache.Inv assign aig Std.Tactic.BVDecide.BVExpr.Cache.empty
-- Init.Data.List.Lex
List.not_lex_nil : ∀ {α : Type u_1} {r : α → α → Prop} {l : List α}, ¬List.Lex r l []
-- Mathlib.Topology.Instances.Rat
NNRat.instMetricSpace : MetricSpace ℚ≥0
-- Mathlib.Topology.Basic
IsOpen.union : ∀ {X : Type u} {s₁ s₂ : Set X} [inst : TopologicalSpace X], IsOpen s₁ → IsOpen s₂ → IsOpen (s₁ ∪ s₂)
-- Mathlib.GroupTheory.Coxeter.Length
CoxeterSystem.IsReduced.drop : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} {cs : CoxeterSystem M W} {ω : List B},
  cs.IsReduced ω → ∀ (j : ℕ), cs.IsReduced (List.drop j ω)
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
/-- Auxiliary definition for `OneHypercoverDenseData.essSurj.restriction`.  -/
CategoryTheory.Functor.OneHypercoverDenseData.essSurj.restriction.res : {C₀ : Type u₀} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v₀, u₀} C₀] →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {F : CategoryTheory.Functor C₀ C} →
          {J₀ : CategoryTheory.GrothendieckTopology C₀} →
            {J : CategoryTheory.GrothendieckTopology C} →
              {A : Type u'} →
                [inst_2 : CategoryTheory.Category.{v', u'} A] →
                  [CategoryTheory.Functor.IsDenseSubsite J₀ J F] →
                    (data : (X : C) → F.OneHypercoverDenseData J₀ J X) →
                      [inst_4 : CategoryTheory.Limits.HasLimitsOfSize.{w, w, v', u'} A] →
                        (G₀ : CategoryTheory.Sheaf J₀ A) →
                          {X : C} →
                            {X₀ Y₀ : C₀} →
                              {f : F.obj X₀ ⟶ X} →
                                {g : Y₀ ⟶ X₀} →
                                  (data X).SieveStruct f g →
                                    (CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObj data G₀ X ⟶
                                      G₀.obj.obj (Opposite.op Y₀))
-- Lean.Compiler.IR.Basic
Lean.IR.IRType.void : Lean.IR.IRType
-- Mathlib.Algebra.Group.Units.Defs
IsUnit.inv_mul_cancel : ∀ {α : Type u} [inst : DivisionMonoid α] {a : α}, IsUnit a → a⁻¹ * a = 1
-- Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
OrderIso.map_csSup_of_directedOn' : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompletePartialOrderSup α]
  [inst_1 : ConditionallyCompletePartialOrderSup β] (e : α ≃o β) {s : Set α},
  DirectedOn (fun x1 x2 => x1 ≤ x2) s → s.Nonempty → BddAbove s → e (sSup s) = sSup (⇑e '' s)
-- Mathlib.Probability.Distributions.Gaussian.Real
/-- The convolution of two real Gaussian distributions with means `m₁, m₂` and variances `v₁, v₂`
is a real Gaussian distribution with mean `m₁ + m₂` and variance `v₁ + v₂`.  -/
ProbabilityTheory.gaussianReal_conv_gaussianReal : ∀ {m₁ m₂ : ℝ} {v₁ v₂ : NNReal},
  (ProbabilityTheory.gaussianReal m₁ v₁).conv (ProbabilityTheory.gaussianReal m₂ v₂) =
    ProbabilityTheory.gaussianReal (m₁ + m₂) (v₁ + v₂)
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.characteristic_iff_map_eq : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G}, H.Characteristic ↔ ∀ (ϕ : G ≃* G), Subgroup.map ϕ.toMonoidHom H = H
-- Mathlib.Analysis.InnerProductSpace.LinearMap
InnerProductSpace.isIdempotentElem_rankOne_self_iff : ∀ {𝕜 : Type u_4} [inst : RCLike 𝕜] {F : Type u_8} [inst_1 : NormedAddCommGroup F] [inst_2 : InnerProductSpace 𝕜 F]
  {x : F}, x ≠ 0 → (IsIdempotentElem (((InnerProductSpace.rankOne 𝕜) x) x) ↔ ‖x‖ = 1)
-- Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
MeasureTheory.NullMeasurableSet.smul_measure : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
  MeasureTheory.NullMeasurableSet s μ → ∀ (c : ENNReal), MeasureTheory.NullMeasurableSet s (c • μ)
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.truncGE_map_truncGEπ_app_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) (X : C) {Z : C}
  (h : (t.truncGE n).obj ((t.truncGE n).obj X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((t.truncGE n).map ((t.truncGEπ n).app X)) h =
    CategoryTheory.CategoryStruct.comp ((t.truncGEπ n).app ((t.truncGE n).obj X)) h
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.HasModel.toNat_two_pow_sub_one_sub_toInt : ∀ {n : ℕ} {lo : BitVec n}, n > 0 → (2 ^ (n - 1) - lo.toInt).toNat = 2 ^ n - (BitVec.Signed.rotate✝ lo).toNat
-- Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
NumberField.InfinitePlace.Completion.ofCompletion.inj : ∀ {K : Type u_1} {inst : Field K} {v : NumberField.InfinitePlace K} {toCompletion toCompletion_1 : (↑v).Completion},
  { toCompletion := toCompletion } = { toCompletion := toCompletion_1 } → toCompletion = toCompletion_1
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
/-- The Hom types for the categorical pullback are given by pairs of maps compatible with the
structural isomorphisms.  -/
CategoryTheory.Limits.CategoricalPullback.Hom : {A : Type u₁} →
  {B : Type u₂} →
    {C : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} A] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            {F : CategoryTheory.Functor A B} →
              {G : CategoryTheory.Functor C B} →
                CategoryTheory.Limits.CategoricalPullback F G →
                  CategoryTheory.Limits.CategoricalPullback F G → Type (max v₁ v₃)
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
CategoryTheory.Bicategory.conjugateEquiv_apply' : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {c d : B} {l₁ l₂ : c ⟶ d} {r₁ r₂ : d ⟶ c}
  (adj₁ : CategoryTheory.Bicategory.Adjunction l₁ r₁) (adj₂ : CategoryTheory.Bicategory.Adjunction l₂ r₂) (α : l₂ ⟶ l₁),
  (CategoryTheory.Bicategory.conjugateEquiv adj₁ adj₂) α =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor r₁).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft r₁ adj₂.unit)
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Bicategory.whiskerLeft r₁ (CategoryTheory.Bicategory.whiskerRight α r₂))
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator r₁ l₁ r₂).inv
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight adj₁.counit r₂)
              (CategoryTheory.Bicategory.leftUnitor r₂).hom))))
-- Mathlib.Order.UpperLower.Basic
IsLowerSet.eq_univ_or_Iio : ∀ {α : Type u_1} [inst : LinearOrder α] {s : Set α} [WellFoundedLT α], IsLowerSet s → s = Set.univ ∨ ∃ a, s = Set.Iio a
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
IncidenceAlgebra.coe_sub : ∀ {𝕜 : Type u_2} {α : Type u_5} [inst : AddGroup 𝕜] [inst_1 : LE α] (f g : IncidenceAlgebra 𝕜 α), ⇑(f - g) = ⇑f - ⇑g
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.throw_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] {α : Type u}
  (err : PUnit.{u_1 + 1}) (post : α → Pred) (epost : EPost.Cons✝ Pred EPred),
  ⦃ epost.head ⦄ MonadExceptOf.throw err ⦃ post; epost ⦄
-- Mathlib.Algebra.Group.Subgroup.Map
AddSubgroup.coe_equivMapOfInjective_apply : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (H : AddSubgroup G) (f : G →+ N)
  (hf : Function.Injective ⇑f) (h : ↥H), ↑((H.equivMapOfInjective f hf) h) = f ↑h
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.support_bypass_subset_support : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} [inst : DecidableEq V] (p : G.Walk u v), p.bypass.support ⊆ p.support
-- Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
PiTensorProduct.mapL_smul : ∀ {ι : Type u_1} [inst : Fintype ι] {𝕜 : Type u_2} {E : ι → Type u_3} [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)]
  [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)] {E' : ι → Type u_5}
  [inst_4 : (i : ι) → SeminormedAddCommGroup (E' i)] [inst_5 : (i : ι) → NormedSpace 𝕜 (E' i)]
  (f : (i : ι) → E i →L[𝕜] E' i) [inst_6 : DecidableEq ι] (i : ι) (c : 𝕜) (u : E i →L[𝕜] E' i),
  PiTensorProduct.mapL (Function.update f i (c • u)) = c • PiTensorProduct.mapL (Function.update f i u)
-- Mathlib.Order.Partition.Finpartition
/-- Equivalence between a finpartition's parts as a dependent sum and the partitioned set.  -/
Finpartition.equivSigmaParts : {α : Type u_1} → [inst : DecidableEq α] → {s : Finset α} → (P : Finpartition s) → ↥s ≃ (t : ↥P.parts) × ↥↑t
-- Mathlib.RepresentationTheory.Subrepresentation
Subrepresentation.mem_ofSubmodule_iff : ∀ {A : Type u_1} {G : Type u_2} {M : Type u_4} [inst : CommSemiring A] [inst_1 : Monoid G] [inst_2 : AddCommMonoid M]
  [inst_3 : Module (MonoidAlgebra A G) M] {N : Submodule (MonoidAlgebra A G) M} {m : M},
  m ∈ Subrepresentation.ofSubmodule N ↔ m ∈ N
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.Monic.leadingCoeff_C_mul : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.Monic → ∀ (r : R), (Polynomial.C r * p).leadingCoeff = r
-- Init.Data.Array.MapIdx
_private.Init.Data.Array.MapIdx.0.List.mapFinIdx.go.match_1.splitter : {α : Type u_1} →
  {β : Type u_2} →
    (as : List α) →
      (motive : (x : List α) → (x_1 : Array β) → x.length + x_1.size = as.length → Sort u_3) →
        (x : List α) →
          (x_1 : Array β) →
            (x_2 : x.length + x_1.size = as.length) →
              ((acc : Array β) → (h : [].length + acc.size = as.length) → motive [] acc h) →
                ((a : α) →
                    (as_1 : List α) →
                      (acc : Array β) → (h : (a :: as_1).length + acc.size = as.length) → motive (a :: as_1) acc h) →
                  motive x x_1 x_2
-- Mathlib.FieldTheory.Finite.Basic
_private.Mathlib.FieldTheory.Finite.Basic.0.termQ : Lean.ParserDescr
-- Mathlib.Data.DFinsupp.Multiset
Multiset.toDFinsupp_singleton : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α), Multiset.toDFinsupp {a} = fun₀ | a => 1
-- Mathlib.Computability.PartrecBasis
Nat.Partrec'.idv : ∀ {n : ℕ}, Nat.Partrec'.Vec id
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
Std.Tactic.BVDecide.LRAT.Internal.Clause.empty_eq : ∀ {α : outParam (Type u)} {β : Type v} [self : Std.Tactic.BVDecide.LRAT.Internal.Clause α β],
  Std.Tactic.BVDecide.LRAT.Internal.Clause.toList Std.Tactic.BVDecide.LRAT.Internal.Clause.empty = []
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
CategoryTheory.MonoidalClosed.uncurry_natural_left_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {A X X' Y : C}
  [inst_2 : CategoryTheory.Closed A] (f : X ⟶ X') (g : X' ⟶ A ⟹ Y) {Z : C} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalClosed.uncurry (CategoryTheory.CategoryStruct.comp f g))
      h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A f)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalClosed.uncurry g) h)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.tan_pi_sub : ∀ (x : ℂ), Complex.tan (↑Real.pi - x) = -Complex.tan x
-- Std.Time.Zoned.ZoneRules
/-- ID of the timezone
 -/
Std.Time.TimeZone.LocalTimeType.identifier : Std.Time.TimeZone.LocalTimeType → String
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
hasSumLocallyUniformlyOn_of_forall_compact : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : AddCommMonoid α] {f : ι → β → α} {g : β → α} {s : Set β}
  [inst_1 : UniformSpace α] [inst_2 : TopologicalSpace β],
  IsOpen s →
    ∀ [LocallyCompactSpace β], (∀ K ⊆ s, IsCompact K → HasSumUniformlyOn f g K) → HasSumLocallyUniformlyOn f g s
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Pred
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Pred.0.Std.Tactic.BVDecide.BVPred.bitblast.match_7.eq_1 : ∀ (motive : Std.Tactic.BVDecide.BVPred → Sort u_1) (w : ℕ) (lhs : Std.Tactic.BVDecide.BVExpr w)
  (op : Std.Tactic.BVDecide.BVBinPred) (rhs : Std.Tactic.BVDecide.BVExpr w)
  (h_1 :
    (w : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) →
        (op : Std.Tactic.BVDecide.BVBinPred) →
          (rhs : Std.Tactic.BVDecide.BVExpr w) → motive (Std.Tactic.BVDecide.BVPred.bin lhs op rhs))
  (h_2 :
    (w : ℕ) → (expr : Std.Tactic.BVDecide.BVExpr w) → (idx : ℕ) → motive (Std.Tactic.BVDecide.BVPred.getLsbD expr idx)),
  (match Std.Tactic.BVDecide.BVPred.bin lhs op rhs with
    | Std.Tactic.BVDecide.BVPred.bin lhs op rhs => h_1 w lhs op rhs
    | Std.Tactic.BVDecide.BVPred.getLsbD expr idx => h_2 w expr idx) =
    h_1 w lhs op rhs
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.basicOpen_le_basicOpen_iff : ∀ {R : Type u} [inst : CommSemiring R] (f g : R),
  PrimeSpectrum.basicOpen f ≤ PrimeSpectrum.basicOpen g ↔ f ∈ (Ideal.span {g}).radical
-- Lean.Attributes
Lean.getAttributeNames : Lean.Environment → List Lean.Name
-- Mathlib.LinearAlgebra.BilinearForm.Properties
LinearMap.BilinForm.apply_dualBasis_right : ∀ {V : Type u_5} {K : Type u_6} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {ι : Type u_9}
  [inst_3 : DecidableEq ι] [inst_4 : Finite ι] {B : LinearMap.BilinForm K V} (hB : B.Nondegenerate),
  B.IsSymm → ∀ (b : Module.Basis ι K V) (i j : ι), (B (b i)) ((B.dualBasis hB b) j) = if i = j then 1 else 0
-- Mathlib.Algebra.Group.Action.Defs
/-- Commutativity of actions is a symmetric relation. This lemma can't be an instance because this
would cause a loop in the instance search graph.  -/
SMulCommClass.symm : ∀ (M : Type u_9) (N : Type u_10) (α : Type u_11) [inst : SMul M α] [inst_1 : SMul N α] [SMulCommClass M N α],
  SMulCommClass N M α
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.opcyclesIsoCokernel_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasRightHomology] [inst_3 : CategoryTheory.Limits.HasCokernel S.f],
  S.opcyclesIsoCokernel.inv = CategoryTheory.Limits.cokernel.desc S.f S.pOpcycles ⋯
-- Init.Data.Range.Polymorphic.PRange
/-- `a...b` is the range of elements greater than or equal to `a` and less than `b`.
See also `Std.Rco`.
 -/
Std.«term_..._» : Lean.TrailingParserDescr
-- Init.Grind.Config
/-- Minimum number of instantiations to trigger detailed report in `#grind_lint`.
Remark: this option is only relevant for the `#grind_lint` command.
 -/
Lean.Grind.Config.detailed : Lean.Grind.Config → ℕ
-- Init.Data.SInt.Lemmas
Int8.toISize_toInt64 : ∀ (n : Int8), n.toInt64.toISize = n.toISize
-- Init.Data.Nat.Bitwise.Lemmas
Nat.testBit_add : ∀ (x i n : ℕ), x.testBit (i + n) = (x / 2 ^ n).testBit i
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey!_insertManyIfNewUnit_list_of_not_mem_of_mem : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α Unit} [EquivBEq α] [LawfulHashable α]
  [inst_4 : Inhabited α],
  m.WF →
    ∀ {l : List α} {k k' : α},
      (k == k') = true →
        k ∉ m → List.Pairwise (fun a b => (a == b) = false) l → k ∈ l → (m.insertManyIfNewUnit l).getKey! k' = k
-- Mathlib.FieldTheory.NormalizedTrace
Algebra.normalizedTrace_def : ∀ (F : Type u_1) (K : Type u_2) [inst : Field F] [inst_1 : Field K] [inst_2 : Algebra F K] [inst_3 : CharZero F]
  [inst_4 : Algebra.IsIntegral F K] (a : K),
  (Algebra.normalizedTrace F K) a =
    (↑(Module.finrank F ↥F⟮a⟯))⁻¹ • (Algebra.trace F ↥F⟮a⟯) (IntermediateField.AdjoinSimple.gen F a)
-- Mathlib.RingTheory.Invariant.Profinite
Ideal.Quotient.stabilizerHomSurjectiveAuxFunctor_aux : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] {G : Type u}
  [inst_3 : Group G] [inst_4 : MulSemiringAction G B] [inst_5 : SMulCommClass G A B] [inst_6 : TopologicalSpace G]
  (Q : Ideal B) {N N' : OpenNormalSubgroup G} (e : N ≤ N'),
  ∀ x ∈ MulAction.stabilizer (G ⧸ ↑N.toOpenSubgroup) (Ideal.under (↥(FixedPoints.subalgebra A B ↥↑N.toOpenSubgroup)) Q),
    (QuotientGroup.map (↑N.toOpenSubgroup) N'.toOpenSubgroup.1 (MonoidHom.id G) e) x ∈
      MulAction.stabilizer (G ⧸ ↑N'.toOpenSubgroup) (Ideal.under (↥(FixedPoints.subalgebra A B ↥↑N'.toOpenSubgroup)) Q)