mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Declaration
/-- The kernel compiles (mutual) inductive declarations (see `inductiveDecls`) into a set of
- `Declaration.inductDecl` (for each inductive datatype in the mutual Declaration),
- `Declaration.ctorDecl` (for each Constructor in the mutual Declaration),
- `Declaration.recDecl` (automatically generated recursors).

This data is used to implement iota-reduction efficiently and compile nested inductive
declarations.

A series of checks are performed by the kernel to check whether a `inductiveDecls`
is valid or not.  -/
Lean.InductiveVal : Type
-- Mathlib.Analysis.Asymptotics.Defs
/-- Definition of `IsLittleO` in terms of `IsBigOWith`.  -/
Asymptotics.isLittleO_iff_forall_isBigOWith : ∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {f : α → E} {g : α → F} {l : Filter α},
  f =o[l] g ↔ ∀ ⦃c : ℝ⦄, 0 < c → Asymptotics.IsBigOWith c l f g
-- Mathlib.CategoryTheory.Discrete.Basic
/-- We can promote a type-level `Equiv` to
an equivalence between the corresponding `discrete` categories.
 -/
CategoryTheory.Discrete.equivalence : {I : Type u₁} → {J : Type u₂} → I ≃ J → (CategoryTheory.Discrete I ≌ CategoryTheory.Discrete J)
-- Mathlib.Analysis.Convex.Quasiconvex
MonotoneOn.quasiconcaveOn : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : LinearOrder E] [IsOrderedAddMonoid E] [inst_5 : PartialOrder β] [inst_6 : Module 𝕜 E] [PosSMulMono 𝕜 E]
  {s : Set E} {f : E → β}, MonotoneOn f s → Convex 𝕜 s → QuasiconcaveOn 𝕜 s f
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.cokernelSequenceCycles_X₃ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k)
  (h : CategoryTheory.CategoryStruct.comp f g = fg) (n : ℤ), (X.cokernelSequenceCycles f g fg h n).X₃ = X.cycles f g n
-- Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
/-- The distinguished infinite place.  -/
NumberField.Units.dirichletUnitTheorem.w₀ : {K : Type u_1} → [inst : Field K] → [NumberField K] → NumberField.InfinitePlace K
-- Mathlib.Combinatorics.SimpleGraph.Ends.Defs
SimpleGraph.ComponentCompl.supp.eq_1 : ∀ {V : Type u} {G : SimpleGraph V} {K : Set V} (C : G.ComponentCompl K),
  C.supp = {v | ∃ (h : v ∉ K), G.componentComplMk h = C}
-- Mathlib.GroupTheory.Perm.Centralizer
/-- Cardinality of a conjugacy class in `Equiv.Perm α` of a given `cycleType`  -/
Equiv.Perm.card_isConj_eq : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] (g : Equiv.Perm α),
  Nat.card ↑{h | IsConj g h} =
    (Fintype.card α).factorial /
      ((Fintype.card α - g.cycleType.sum).factorial * g.cycleType.prod *
        ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType).factorial)
-- Mathlib.RingTheory.Localization.AtPrime.Basic
Localization.localRingHom_mk : ∀ {R : Type u_1} [inst : CommSemiring R] {P : Type u_3} [inst_1 : CommSemiring P] (I : Ideal R) [hI : I.IsPrime]
  (J : Ideal P) [inst_2 : J.IsPrime] (f : R →+* P) (hIJ : I = Ideal.comap f J) (x : R) (y : ↥I.primeCompl),
  (Localization.localRingHom I J f hIJ) (Localization.mk x y) = Localization.mk (f x) ⟨f ↑y, ⋯⟩
-- Mathlib.CategoryTheory.Limits.Shapes.Images
/-- Any other factorisation of the morphism `f` through a monomorphism receives a map from the
image.  -/
CategoryTheory.Limits.image.lift : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      {f : X ⟶ Y} →
        [inst_1 : CategoryTheory.Limits.HasImage f] →
          (F' : CategoryTheory.Limits.MonoFactorisation f) → CategoryTheory.Limits.image f ⟶ F'.I
-- Mathlib.Order.Filter.AtTopBot.Archimedean
Filter.Tendsto.atTop_zsmul_const : ∀ {α : Type u_1} {R : Type u_2} {l : Filter α} {r : R} [inst : AddCommGroup R] [inst_1 : LinearOrder R]
  [IsOrderedAddMonoid R] [Archimedean R] {f : α → ℤ},
  0 < r → Filter.Tendsto f l Filter.atTop → Filter.Tendsto (fun x => f x • r) l Filter.atTop
-- Mathlib.Analysis.Normed.Algebra.Unitization
Unitization.nndist_inr : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : NormedSpace 𝕜 A] [inst_3 : IsScalarTower 𝕜 A A] [inst_4 : SMulCommClass 𝕜 A A]
  [inst_5 : RegularNormedAlgebra 𝕜 A] (a b : A), nndist ↑a ↑b = nndist a b
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.instAddGroupCoeOfAddSubgroupClass.eq_1 : ∀ {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [inst : (i : ι) → SetLike (S i) (R i)]
  {B : (i : ι) → S i} [inst_1 : (i : ι) → AddGroup (R i)] [inst_2 : ∀ (i : ι), AddSubgroupClass (S i) (R i)],
  RestrictedProduct.instAddGroupCoeOfAddSubgroupClass R = Function.Injective.addGroup DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
-- Lean.Elab.InfoTree.Main
Lean.Elab.CompletionInfo.format : Lean.Elab.ContextInfo → Lean.Elab.CompletionInfo → IO Std.Format
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey_eq_getKey! : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {a : α} {h : a ∈ t}, t.getKey a h = t.getKey! a
-- Mathlib.Topology.Instances.EReal.Lemmas
_private.Mathlib.Topology.Instances.EReal.Lemmas.0.EReal.continuousAt_mul_symm1 : ∀ {a b : EReal}, ContinuousAt (fun p => p.1 * p.2) (a, b) → ContinuousAt (fun p => p.1 * p.2) (-a, b)
-- Lean.AuxRecursor
Lean.recOnSuffix : String
-- Init.Data.Slice.Array.Lemmas
Array.toArray_mkSlice_roc : ∀ {α : Type u_1} {xs : Array α} {lo hi : ℕ},
  Std.Slice.toArray (Std.Roc.Sliceable.mkSlice xs lo<...=hi) = xs.extract (lo + 1) (hi + 1)
-- Mathlib.Analysis.Normed.Group.Uniform
/-- A homomorphism `f` of seminormed groups is Lipschitz, if there exists a constant `C` such that
for all `x`, one has `‖f x‖ ≤ C * ‖x‖`. The analogous condition for a linear map of
(semi)normed spaces is in `Mathlib/Analysis/Normed/Operator/Basic.lean`.  -/
MonoidHomClass.lipschitz_of_bound : ∀ {𝓕 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : SeminormedGroup E] [inst_1 : SeminormedGroup F]
  [inst_2 : FunLike 𝓕 E F] [MonoidHomClass 𝓕 E F] (f : 𝓕) (C : ℝ),
  (∀ (x : E), ‖f x‖ ≤ C * ‖x‖) → LipschitzWith C.toNNReal ⇑f
-- Mathlib.Algebra.Order.Ring.StandardPart
ArchimedeanClass.FiniteElement.mk_natCast : ∀ {K : Type u_1} [inst : LinearOrder K] [inst_1 : Field K] [inst_2 : IsOrderedRing K] (n : ℕ),
  ArchimedeanClass.FiniteElement.mk ↑n ⋯ = ↑n
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.preLeftIso.eq_1 : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {C : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C] (F : CategoryTheory.Functor C A) (L : CategoryTheory.Functor A T)
  (R : CategoryTheory.Functor B T),
  CategoryTheory.Comma.preLeftIso F L R =
    CategoryTheory.NatIso.ofComponents
      (fun X =>
        CategoryTheory.Comma.isoMk (CategoryTheory.Iso.refl ((CategoryTheory.Comma.preLeft F L R).obj X).left)
          (CategoryTheory.Iso.refl ((CategoryTheory.Comma.preLeft F L R).obj X).right) ⋯)
      ⋯
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
CategoryTheory.Limits.PreservesFiniteBiproducts.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  {F : CategoryTheory.Functor C D} [inst_4 : F.PreservesZeroMorphisms],
  (∀ {J : Type} [Finite J], CategoryTheory.Limits.PreservesBiproductsOfShape J F) →
    CategoryTheory.Limits.PreservesFiniteBiproducts F
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.cons.eq_1 : ∀ {α : Type u} (a : α), Stream'.WSeq.cons a = Stream'.Seq.cons (some a)
-- Std.Data.HashMap.Lemmas
Std.HashMap.contains_of_isEmpty : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {a : α}, m.isEmpty = true → m.contains a = false
-- Mathlib.Order.RelClasses
IsStrictOrder.swap : ∀ {α : Type u} (r : α → α → Prop) [IsStrictOrder α r], IsStrictOrder α (Function.swap r)
-- Mathlib.Algebra.Homology.DifferentialObject
/-- Since `eqToHom` only preserves the fact that `X.X i = X.X j` but not `i = j`, this definition
is used to aid the simplifier.  -/
CategoryTheory.DifferentialObject.objEqToHom : {β : Type u_1} →
  [inst : AddCommGroup β] →
    {b : β} →
      {V : Type u_2} →
        [inst_1 : CategoryTheory.Category.{v_1, u_2} V] →
          [inst_2 : CategoryTheory.Limits.HasZeroMorphisms V] →
            (X : CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V)) →
              {i j : β} → i = j → (X.obj i ⟶ X.obj j)
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.coeff_smul_apply : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] {A : Type u_8} [inst_1 : SMulZeroClass A R] (a : A)
  (x : MonoidAlgebra R M) (m : M), (a • x).coeff m = a • x.coeff m
-- Mathlib.Analysis.Calculus.FDeriv.CompCLM
DifferentiableOn.clm_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {G : Type u_4} [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] {s : Set E}
  {H : Type u_5} [inst_5 : NormedAddCommGroup H] [inst_6 : NormedSpace 𝕜 H] {c : E → G →L[𝕜] H} {u : E → G},
  DifferentiableOn 𝕜 c s → DifferentiableOn 𝕜 u s → DifferentiableOn 𝕜 (fun y => (c y) (u y)) s
-- Mathlib.Probability.Distributions.Gaussian.Fernique
/-- For a centered Gaussian measure `μ`, the product measure `μ.prod μ` is invariant under rotation.
The hypothesis `∀ L : StrongDual ℝ E, μ[L] = 0` is equivalent to the simpler
`μ[id] = 0`, but at this point we don't know yet that `μ` has a first moment so we can't use it.
See `map_rotation_eq_self`.  -/
ProbabilityTheory.IsGaussian.map_rotation_eq_self_of_forall_strongDual_eq_zero : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  {μ : MeasureTheory.Measure E} [ProbabilityTheory.IsGaussian μ] [SecondCountableTopology E] [CompleteSpace E],
  (∀ (L : StrongDual ℝ E), ∫ (x : E), L x ∂μ = 0) →
    ∀ (θ : ℝ), MeasureTheory.Measure.map (⇑(ContinuousLinearMap.rotation θ)) (μ.prod μ) = μ.prod μ
-- Mathlib.Data.Finset.PImage
Finset.pimage_subset : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] {f : α →. β} [inst_1 : (x : α) → Decidable (f x).Dom]
  {s : Finset α} {t : Finset β}, Finset.pimage f s ⊆ t ↔ ∀ x ∈ s, ∀ y ∈ f x, y ∈ t
-- Mathlib.Tactic.Simproc.ExistsAndEq
/-- Type for storing the path in the body expression leading to `a = a'`. We store only the chosen
directions at each `And` node because there is no branching at `Exists` nodes, and `Exists` nodes
will be removed from the body.  -/
ExistsAndEq.Path : Type
-- Lean.Compiler.InitAttr
Lean.isIOUnitBuiltinInitFn : Lean.Environment → Lean.Name → Bool
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- The maps from the cone point of a multifork to the objects on the left.  -/
CategoryTheory.Limits.Multifork.ι : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.Limits.MulticospanShape} →
      {I : CategoryTheory.Limits.MulticospanIndex J C} →
        (K : CategoryTheory.Limits.Multifork I) → (a : J.L) → K.pt ⟶ I.left a
-- Mathlib.Topology.Algebra.Valued.LocallyCompact
Valued.integer.finite_quotient_maximalIdeal_pow_of_finite_residueField : ∀ {K : Type u_1} {Γ₀ : Type u_2} [inst : Field K] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] [inst_2 : Valued K Γ₀]
  [IsDiscreteValuationRing ↥(Valued.integer K)],
  Finite (Valued.ResidueField K) → ∀ (n : ℕ), Finite (↥(Valued.integer K) ⧸ Valued.maximalIdeal K ^ n)
-- Mathlib.AlgebraicGeometry.Sites.Small
AlgebraicGeometry.Scheme.mem_smallGrothendieckTopology : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {S : AlgebraicGeometry.Scheme}
  [inst : P.IsStableUnderBaseChange] [P.IsMultiplicative] [P.RespectsIso] [P.HasOfPostcompProperty P] (X : P.Over ⊤ S)
  (R : CategoryTheory.Sieve X),
  R ∈ (AlgebraicGeometry.Scheme.smallGrothendieckTopology P S) X ↔
    ∃ 𝒰 x, ∃ (h : ∀ (j : 𝒰.I₀), P (𝒰.X j ↘ S)), 𝒰.toPresieveOverProp h ≤ R.arrows
-- Mathlib.Data.ENat.Basic
ENat.eq_top_iff_forall_gt : ∀ {n : ℕ∞}, n = ⊤ ↔ ∀ (m : ℕ), ↑m < n
-- Mathlib.Data.Rel
SetRel.id_comp : ∀ {α : Type u_1} {β : Type u_2} (R : SetRel α β), SetRel.id.comp R = R
-- Mathlib.Analysis.Meromorphic.NormalForm
/-- Eta-expanded form of `meromorphicNFOn_sphere_comp_sub_const_iff_meromorphicNFOn_sphere`

---

`MeromorphicNFOn` is invariant under translation, special case where the set is a sphere.  -/
meromorphicNFOn_sphere_fun_comp_sub_const_iff_meromorphicNFOn_sphere : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {c : 𝕜} {R : ℝ},
  MeromorphicNFOn (fun x => f (x - c)) (Metric.sphere c R) ↔ MeromorphicNFOn f (Metric.sphere 0 R)
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.mrefinePat.quot : Lean.ParserDescr
-- Mathlib.CategoryTheory.NatTrans
CategoryTheory.NatTrans.naturality' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} (self : CategoryTheory.NatTrans G F) ⦃X Y : C⦄ (f : Y ⟶ X),
  CategoryTheory.CategoryStruct.comp (self.app Y) (F.map f) = CategoryTheory.CategoryStruct.comp (G.map f) (self.app X)
-- Mathlib.Topology.Gluing
TopCat.GlueData.MkCore.t_inter : ∀ (self : TopCat.GlueData.MkCore) ⦃i j : self.J⦄ (k : self.J) (x : ↥(self.V i j)),
  ↑x ∈ self.V i k → ↑((CategoryTheory.ConcreteCategory.hom (self.t i j)) x) ∈ self.V j k
-- Mathlib.GroupTheory.Commutator.Basic
/-- Representatives `(g₁, g₂) : G × G` of additive commutators `⁅g₁, g₂⁆ ∈ G`.  -/
addCommutatorRepresentatives : (G : Type u_1) → [AddGroup G] → Set (G × G)
-- Mathlib.Tactic.Linter.FindDeprecations
/-- Takes as input a file path `fname` and an array of pairs `(declName, range of declaration)`.
The `declName` is mostly for printing information, but is not used essentially by the function.

It returns the pair `(temp file name, file without the commands that generated the declarations)`.

In the course of doing so, the function creates a temporary file from `fname`, by
* adding the import `Mathlib.Tactic.Linter.CommandRanges` and
* setting the `linter.commandRanges` option to `true`.

It parses the temporary file, capturing the output and uses the command ranges to remove the
ranges of the *commands* that generated the passed declaration ranges.
 -/
_private.Mathlib.Tactic.Linter.FindDeprecations.0.Mathlib.Tactic.rewriteOneFile : String → Array (Lean.Name × Lean.Syntax.Range) → Lean.Elab.Command.CommandElabM (String × String)
-- Mathlib.Data.Set.Lattice
Set.iUnion_subset : ∀ {α : Type u_1} {ι : Sort u_5} {s : ι → Set α} {t : Set α}, (∀ (i : ι), s i ⊆ t) → ⋃ i, s i ⊆ t
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.instInhabited : {σ : Type u_1} → {R : Type u_2} → [Inhabited R] → Inhabited (MvPowerSeries σ R)
-- Mathlib.Order.Interval.Finset.Basic
Finset.Icc_subset_uIcc' : ∀ {α : Type u_2} [inst : Lattice α] [inst_1 : LocallyFiniteOrder α] {a b : α}, Finset.Icc b a ⊆ Finset.uIcc a b
-- Init.Data.Array.Find
Array.findSome?_append : ∀ {α : Type u_1} {α_1 : Type u_2} {f : α → Option α_1} {xs ys : Array α},
  Array.findSome? f (xs ++ ys) = (Array.findSome? f xs).or (Array.findSome? f ys)
-- Mathlib.CategoryTheory.Monoidal.Mon
/-- The zero morphism of an additive monoid object.  -/
CategoryTheory.AddMonObj.zero : {C : Type u₁} →
  {inst : CategoryTheory.Category.{v₁, u₁} C} →
    {inst_1 : CategoryTheory.MonoidalCategory C} →
      {X : C} → [self : CategoryTheory.AddMonObj X] → CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ X
-- Mathlib.Data.Int.Order.Basic
Int.mul_nonneg_iff : ∀ {a b : ℤ}, 0 ≤ a * b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0
-- Mathlib.Topology.Algebra.InfiniteSum.Ring
Summable.one_sub_mul_tsum_pow : ∀ {α : Type u_3} [inst : Ring α] [inst_1 : TopologicalSpace α] [IsTopologicalRing α] [T2Space α] {x : α},
  (Summable fun x_1 => x ^ x_1) → (1 - x) * ∑' (i : ℕ), x ^ i = 1
-- Mathlib.LinearAlgebra.Eigenspace.Basic
Module.End.injOn_maxGenEigenspace : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsDomain R]
  [Module.IsTorsionFree R M] (f : Module.End R M),
  Set.InjOn (fun x => f.maxGenEigenspace x) {μ | f.maxGenEigenspace μ ≠ ⊥}
-- Mathlib.Data.Set.Card
Set.ncard_le_ncard_insert : ∀ {α : Type u_1} (a : α) (s : Set α), s.ncard ≤ (insert a s).ncard
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.image_mul_left' : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Group α] {t : Finset α} {a : α},
  Finset.image (fun b => a⁻¹ * b) t = t.preimage (fun b => a * b) ⋯
-- Init.Data.UInt.Bitwise
USize.xor_zero : ∀ {a : USize}, a ^^^ 0 = a
-- Mathlib.Combinatorics.Matroid.Minor.Delete
/-- **Alias** of the reverse direction of `Matroid.delete_eq_self_iff`. -/
Matroid.delete_eq_self : ∀ {α : Type u_1} {M : Matroid α} {D : Set α}, Disjoint D M.E → M.delete D = M
-- Mathlib.Algebra.Polynomial.Inductions
Polynomial.X_mul_divX_add : ∀ {R : Type u} [inst : Semiring R] (p : Polynomial R), Polynomial.X * p.divX + Polynomial.C (p.coeff 0) = p
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instAddZeroClass : {α : Type u_1} → [AddZeroClass α] → AddZeroClass αᵒᵈ
-- Batteries.Data.Fin.Coding
_private.Batteries.Data.Fin.Coding.0.Fin.decodeSubtype.match_5.splitter : (motive : (n : ℕ) → (P : Fin n → Prop) → (inst : DecidablePred P) → Fin (Fin.countP fun x => decide (P x)) → Sort u_1) →
  (n : ℕ) →
    (P : Fin n → Prop) →
      (inst : DecidablePred P) →
        (k : Fin (Fin.countP fun x => decide (P x))) →
          ((x : Fin 0 → Prop) →
              (x_1 : DecidablePred x) →
                (val : ℕ) → (h : val < Fin.countP fun x_2 => decide (x x_2)) → motive 0 x x_1 ⟨val, h⟩) →
            ((n : ℕ) →
                (P : Fin (n + 1) → Prop) →
                  (inst : DecidablePred P) →
                    (k : ℕ) → (hk : k < Fin.countP fun x => decide (P x)) → motive n.succ P inst ⟨k, hk⟩) →
              motive n P inst k
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.add_mem_add : ∀ {α : Type u_2} [inst : Add α] {s t : Set α} {a b : α}, a ∈ s → b ∈ t → a + b ∈ s + t
-- Batteries.Data.List.Lemmas
List.findIdxNth_mono : ∀ {α : Type u_1} {n m : ℕ} {p : α → Bool} {xs : List α}, n ≤ m → List.findIdxNth p xs n ≤ List.findIdxNth p xs m
-- Mathlib.Algebra.Torsor.Basic
/-- Cancellation dividing the results of two divisions.  -/
sdiv_div_sdiv_cancel_left : ∀ {G : Type u_1} {P : Type u_2} [inst : CommGroup G] [inst_1 : Torsor G P] (p₁ p₂ p₃ : P),
  (p₃ /ₛ p₂) / (p₃ /ₛ p₁) = p₁ /ₛ p₂
-- Std.Http.Protocol.H1.Event
/-- Indicates that all headers have been successfully parsed.
 -/
Std.Http.Protocol.H1.Event.endHeaders : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Message.Head dir → Std.Http.Protocol.H1.Event dir
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.id_comp : ∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [inst : Ring k]
  [inst_1 : AddCommGroup V1] [inst_2 : Module k V1] [inst_3 : AddTorsor V1 P1] [inst_4 : AddCommGroup V2]
  [inst_5 : Module k V2] [inst_6 : AddTorsor V2 P2] (f : P1 →ᵃ[k] P2), (AffineMap.id k P2).comp f = f
-- Mathlib.CategoryTheory.ObjectProperty.Basic
CategoryTheory.ObjectProperty.exists_prop_of_nonempty : ∀ {C : Type u} [inst : CategoryTheory.CategoryStruct.{v, u} C] (P : CategoryTheory.ObjectProperty C) [P.Nonempty],
  ∃ X, P X
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.num.injEq : ∀ (k k_1 : ℤ), (Lean.Grind.CommRing.Poly.num k = Lean.Grind.CommRing.Poly.num k_1) = (k = k_1)
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
/-- The equivalence `RightExtension L F ≌ RightExtension L F'` induced by
a natural isomorphism `F ≅ F'`.  -/
CategoryTheory.Functor.rightExtensionEquivalenceOfIso₂ : {C : Type u_1} →
  {H : Type u_3} →
    {D : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_3, u_3} H] →
          [inst_2 : CategoryTheory.Category.{v_4, u_4} D] →
            (L : CategoryTheory.Functor C D) →
              {F F' : CategoryTheory.Functor C H} → (F ≅ F') → (L.RightExtension F ≌ L.RightExtension F')
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
Mathlib.Tactic.BicategoryLike.instInhabitedHorizontalComp.default : Mathlib.Tactic.BicategoryLike.HorizontalComp
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.BitVec.mul_beq_mul_short_circuit_left : ∀ {w : ℕ} {x₁ x₂ y : BitVec w}, (x₁ * y == x₂ * y) = !(!x₁ == x₂ && !x₁ * y == x₂ * y)
-- Lean.DocString.DeferredCheck
Lean.Doc.instInhabitedDeferredCheckSite.default : Lean.Doc.DeferredCheckSite
-- Mathlib.Order.Std
/-- `max a b` is equivalent to `if b ≤ a then a else b`.  -/
LinearOrder.OfStdArgs.lawfulOrderLeftLeaningMax : ∀ {α : Type u_1} (self : LinearOrder.OfStdArgs α), Std.LawfulOrderLeftLeaningMax α
-- Mathlib.Analysis.Calculus.Deriv.Mul
/-- A variant of `derivWithin_const_mul` without differentiability assumption when the scalar
multiplication is by division ring elements.  -/
derivWithin_const_mul_field : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} {𝕜' : Type u_2} [inst_1 : NormedDivisionRing 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {v : 𝕜 → 𝕜'} (u : 𝕜'), derivWithin (fun y => u * v y) s x = u * derivWithin v s x
-- Mathlib.Analysis.Complex.Trigonometric
Complex.cosh_zero : Complex.cosh 0 = 1
-- Mathlib.Analysis.Calculus.FDeriv.Mul
/-- Eta-expanded form of `DifferentiableWithinAt.smul` -/
DifferentiableWithinAt.fun_smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {x : E} {s : Set E} {𝕜' : Type u_5} [inst_5 : NormedRing 𝕜'] [inst_6 : NormedAlgebra 𝕜 𝕜'] [inst_7 : Module 𝕜' F]
  [IsBoundedSMul 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {c : E → 𝕜'},
  DifferentiableWithinAt 𝕜 c s x → DifferentiableWithinAt 𝕜 f s x → DifferentiableWithinAt 𝕜 (fun i => c i • f i) s x
-- Mathlib.Algebra.Symmetrized
SymAlg.sym_ne_one_iff : ∀ {α : Type u_1} [inst : One α] (a : α), SymAlg.sym a ≠ 1 ↔ a ≠ 1
-- Mathlib.Order.Filter.Basic
Filter.empty_mem_iff_bot : ∀ {α : Type u} {f : Filter α}, ∅ ∈ f ↔ f = ⊥
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getD_union : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {fallback : β}, (t₁ ∪ t₂).getD k fallback = t₂.getD k (t₁.getD k fallback)
-- Mathlib.Analysis.MeanInequalities
/-- **Hölder inequality**: the sum of (the `r`-power of) the product of two functions is bounded
by (the `r`-power of) the product of their `L^p` and `L^q` norms, when `p`, `q`, `r` form a
`Real.HolderTriple`.  -/
Real.Lr_rpow_le_Lp_mul_Lq_of_nonneg : ∀ {ι : Type u_1} (s : Finset ι) {f g : ι → ℝ} {p q r : ℝ},
  p.HolderTriple q r →
    (∀ i ∈ s, 0 ≤ f i) →
      (∀ i ∈ s, 0 ≤ g i) → ∑ i ∈ s, (f i * g i) ^ r ≤ (∑ i ∈ s, f i ^ p) ^ (r / p) * (∑ i ∈ s, g i ^ q) ^ (r / q)
-- Mathlib.Logic.IsEmpty.Defs
IsEmpty.mk : ∀ {α : Sort u}, (∀ (a : α), False) → IsEmpty α
-- Mathlib.Topology.MetricSpace.Dilation
/-- Dilations scale the diameter by `ratio f` in pseudoemetric spaces.  -/
Dilation.ediam_image : ∀ {α : Type u_1} {β : Type u_2} {F : Type u_4} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β]
  [inst_2 : FunLike F α β] [inst_3 : DilationClass F α β] (f : F) (s : Set α),
  Metric.ediam (⇑f '' s) = ↑(Dilation.ratio f) * Metric.ediam s
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKey_eq_getLast_keys : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {he : t.isEmpty = false}, t.maxKey he = t.keys.getLast ⋯
-- Mathlib.GroupTheory.NoncommPiCoprod
Subgroup.noncommPiCoprod_apply : ∀ {G : Type u_1} [inst : Group G] {ι : Type u_2} {H : ι → Subgroup G} [inst_1 : Fintype ι]
  (comm : Pairwise fun i j => ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y) (u : (i : ι) → ↥(H i)),
  (Subgroup.noncommPiCoprod comm) u = Finset.univ.noncommProd (fun i => ↑(u i)) ⋯