mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Extension.Cotangent.Basic
/-- `H¹(L_{S/R})` is independent of the presentation chosen.  -/
Algebra.Generators.H1Cotangent.equiv : {R : Type u} →
  {S : Type v} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          {ι : Type w} →
            {ι' : Type u_1} →
              (P : Algebra.Generators R S ι) →
                (P' : Algebra.Generators R S ι') → P.toExtension.H1Cotangent ≃ₗ[S] P'.toExtension.H1Cotangent
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem?_insertManyIfNewUnit_list : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α Unit cmp} [Std.TransCmp cmp] [inst : BEq α]
  [Std.LawfulBEqCmp cmp],
  t.WF → ∀ {l : List α} {k : α}, (t.insertManyIfNewUnit l)[k]? = if k ∈ t ∨ l.contains k = true then some () else none
-- Lean.Elab.Term.TermElabM
/-- If the `trace.Meta.synthInstance` option is not already set, gives a hint explaining this option.
 -/
Lean.Elab.Term.useTraceSynthMsg : Lean.MessageData
-- Mathlib.LinearAlgebra.Matrix.ToLin
Matrix.toLinearMapRight'_apply : ∀ {R : Type u_1} [inst : Semiring R] {m : Type u_3} {n : Type u_4} [inst_1 : Fintype m] [inst_2 : DecidableEq m]
  (M : Matrix m n R) (v : m → R), (Matrix.toLinearMapRight' M) v = Matrix.vecMul v M
-- Init.Data.Float.Model.Float32
/-- Converts a `UInt64` to a `Float32.Model`, returning positive zero on zero.  -/
Float32.Model.ofUInt64 : UInt64 → Float32.Model
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.toSubring_eq_top : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {S : Subalgebra R A},
  S.toSubring = ⊤ ↔ S = ⊤
-- Mathlib.CategoryTheory.Preadditive.Projective.Basic
/-- Given an adjunction `F ⊣ G` such that `G` preserves epis, `F` maps a projective presentation of
`X` to a projective presentation of `F(X)`.  -/
CategoryTheory.Adjunction.mapProjectivePresentation : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} D] →
        {F : CategoryTheory.Functor C D} →
          {G : CategoryTheory.Functor D C} →
            (F ⊣ G) →
              [G.PreservesEpimorphisms] →
                (X : C) → CategoryTheory.ProjectivePresentation X → CategoryTheory.ProjectivePresentation (F.obj X)
-- Mathlib.CategoryTheory.Retract
CategoryTheory.RetractArrow.map_r_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W} (h : CategoryTheory.RetractArrow f g) (F : CategoryTheory.Functor C D),
  (h.map F).r.right = F.map (CategoryTheory.Arrow.Hom.right h.r)
-- Mathlib.ModelTheory.LanguageMap
/-- Lifts an embedding to the expanded language with constants.  -/
FirstOrder.Language.Embedding.liftWithConstants : {L : FirstOrder.Language} →
  {M : Type w} →
    [inst : L.Structure M] →
      (A : Set M) →
        {N : Type w'} →
          [inst_1 : L.Structure N] → (f : L.Embedding M N) → (L.withConstants ↑A).Embedding M (f.withConstants A)
-- Mathlib.LinearAlgebra.AffineSpace.Slope
slope_def_field : ∀ {k : Type u_1} [inst : Field k] (f : k → k) (a b : k), slope f a b = (f b - f a) / (b - a)
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
/-- Hölder's inequality for functions `α → ℝ`. The integral of the product of two nonnegative
functions is bounded by the product of their `ℒp` and `ℒq` seminorms when `p` and `q` are conjugate
exponents.  -/
MeasureTheory.integral_mul_le_Lp_mul_Lq_of_nonneg : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {p q : ℝ},
  p.HolderConjugate q →
    ∀ {f g : α → ℝ},
      0 ≤ᵐ[μ] f →
        0 ≤ᵐ[μ] g →
          MeasureTheory.MemLp f (ENNReal.ofReal p) μ →
            MeasureTheory.MemLp g (ENNReal.ofReal q) μ →
              ∫ (a : α), f a * g a ∂μ ≤ (∫ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫ (a : α), g a ^ q ∂μ) ^ (1 / q)
-- Mathlib.Algebra.GCDMonoid.Basic
/-- Define `NormalizationMonoid` on a structure from a `MonoidHom` inverse to `Associates.mk`.  -/
strongNormalizationMonoidOfMonoidHomRightInverse : {α : Type u_1} →
  [inst : CommMonoidWithZero α] →
    [IsCancelMulZero α] →
      [DecidableEq α] → (f : Associates α →* α) → Function.RightInverse (⇑f) Associates.mk → StrongNormalizationMonoid α
-- Mathlib.Algebra.Order.Floor.Extended
/-- `⌊r⌋ₑ` is the greatest extended natural `n` such that `n ≤ r`.  -/
ENat.«term⌊_⌋ₑ» : Lean.ParserDescr
-- Plausible.Arbitrary
Plausible.Sum.Arbitrary : {α β : Type} → [Plausible.Arbitrary α] → [Plausible.Arbitrary β] → Plausible.Arbitrary (α ⊕ β)
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.zero_smulRight : ∀ {M₁ : Type u_4} [inst : TopologicalSpace M₁] [inst_1 : AddCommMonoid M₁] {M₂ : Type u_6}
  [inst_2 : TopologicalSpace M₂] [inst_3 : AddCommMonoid M₂] {R : Type u_9} {S : Type u_10} [inst_4 : Semiring R]
  [inst_5 : Semiring S] [inst_6 : Module R M₁] [inst_7 : Module R M₂] [inst_8 : Module R S] [inst_9 : Module S M₂]
  [inst_10 : IsScalarTower R S M₂] [inst_11 : TopologicalSpace S] [inst_12 : ContinuousSMul S M₂] {x : M₂},
  ContinuousLinearMap.smulRight 0 x = 0
-- Init.Data.UInt.Lemmas
UInt16.pow_zero : ∀ (x : UInt16), x ^ 0 = 1
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.foldrM_eq_foldrM_keysArray : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} {δ : Type w} {m : Type w → Type w'}
  [inst : Monad m] [LawfulMonad m] {f : α → δ → m δ} {init : δ},
  Std.TreeMap.foldrM (fun a x d => f a d) init t = Array.foldrM f init t.keysArray
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.minView!.eq_2 : ∀ {α : Type u} {β : α → Type v} (k : α) (v : β k) (r : Std.DTreeMap.Internal.Impl α β) (size : ℕ) (k' : α) (v' : β k')
  (l' r' : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.minView! k v (Std.DTreeMap.Internal.Impl.inner size k' v' l' r') r =
    { k := (Std.DTreeMap.Internal.Impl.minView! k' v' l' r').k,
      v := (Std.DTreeMap.Internal.Impl.minView! k' v' l' r').v,
      tree := Std.DTreeMap.Internal.Impl.balanceR! k v (Std.DTreeMap.Internal.Impl.minView! k' v' l' r').tree r }
-- Mathlib.Data.Matrix.Basic
/-- A version of `Set.matrix` for `Subring`s.
Given a `Subring` `S`, `S.matrix` is the `Subring` of square matrices `m`
all of whose entries `m i j` belong to `S`.  -/
Subring.matrix : {n : Type u_3} →
  {R : Type u_14} →
    [inst : NonAssocRing R] → [inst_1 : Fintype n] → [inst_2 : DecidableEq n] → Subring R → Subring (Matrix n n R)
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
mulIndicator_iUnion_of_pairwise_disjoint_on_mulSupport : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] (s : γ → Set β)
  (f : β → α),
  Pairwise (Function.onFun Disjoint fun j => s j ∩ Function.mulSupport f) →
    ∀ (i : β), (⋃ d, s d).mulIndicator f i = ∏' (d : γ), (s d).mulIndicator f i
-- Mathlib.Algebra.GroupWithZero.Idempotent
IsIdempotentElem.coe_zero : ∀ {M₀ : Type u_1} [inst : MulZeroClass M₀], ↑0 = 0
-- Mathlib.Geometry.Manifold.GroupLieAlgebra
contMDiff_addInvariantVectorField : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : AddGroup G]
  [inst_7 : LieAddGroup I (minSmoothness 𝕜 3) G] (v : AddGroupLieAlgebra I G),
  ContMDiff I I.tangent (minSmoothness 𝕜 2) fun g => ⟨g, addInvariantVectorField v g⟩
-- Init.Grind.Module.Envelope
Lean.Grind.IntModule.OfNatModule.instCommutativeHAdd : ∀ (α : Type u) [inst : Lean.Grind.NatModule α], Std.Commutative fun x1 x2 => x1 + x2
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Associates.count.eq_1 : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : DecidableEq (Associates α)]
  [inst_2 : (p : Associates α) → Decidable (Irreducible p)] (p : Associates α),
  p.count = if hp : Irreducible p then Associates.bcount ⟨p, hp⟩ else 0
-- Mathlib.Tactic.FunProp.FunctionData
/-- Get `FunctionData` for `f`.  -/
Mathlib.Meta.FunProp.getFunctionData? : Lean.Expr → (optParam (Lean.Name → Bool) fun x => false) → Lean.MetaM Mathlib.Meta.FunProp.MaybeFunctionData
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
/-- An abbreviation for `WeierstrassCurve.Jacobian.Point.fromAffine` for dot notation.  -/
WeierstrassCurve.Affine.Point.toJacobian : {R : Type r} →
  [inst : CommRing R] →
    [Nontrivial R] → {W : WeierstrassCurve.Affine R} → W.Point → (WeierstrassCurve.toJacobian W).Point
-- Init.Data.List.Sublist
List.IsPrefix.subset : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <+: l₂ → l₁ ⊆ l₂
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
map_abs : ∀ {α : Type u_1} [inst : AddGroup α] [inst_1 : LinearOrder α] {β : Type u_2} {F : Type u_3} [inst_2 : AddGroup β]
  [inst_3 : LinearOrder β] [inst_4 : FunLike F α β] [OrderHomClass F α β] [AddMonoidHomClass F α β] (f : F) (a : α),
  f |a| = |f a|
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.characteristic_iSup : ∀ {G : Type u_1} [inst : AddGroup G] {ι : Sort u_5} {H : ι → AddSubgroup G} [∀ (i : ι), (H i).Characteristic],
  (⨆ i, H i).Characteristic
-- Lean.Parser.Term
Lean.Parser.Term.binrel.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Algebra.Order.Interval.Basic
NonemptyInterval.fst_natCast : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : NatCast α] (n : ℕ), (↑n).toProd.1 = ↑n
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
/-- the coherence condition for the left square  -/
CategoryTheory.Limits.CatCospanTransformMorphism.left_coherence : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {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}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'}
  (self : CategoryTheory.Limits.CatCospanTransformMorphism ψ ψ'),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CatCommSq.iso F ψ.left ψ.base F').hom
      (CategoryTheory.Functor.whiskerRight self.left F') =
    CategoryTheory.CategoryStruct.comp (F.whiskerLeft self.base) (CategoryTheory.CatCommSq.iso F ψ'.left ψ'.base F').hom
-- Mathlib.Order.Comparable
/-- The comparability relation `CompRel r a b` means that either `r a b` or `r b a`.  -/
CompRel : {α : Type u_1} → (α → α → Prop) → α → α → Prop
-- Mathlib.Order.PrimeIdeal
Order.PFilter.isPrime_iff : ∀ {P : Type u_1} [inst : Preorder P] (F : Order.PFilter P), F.IsPrime ↔ Order.IsIdeal (↑F)ᶜ
-- ProofWidgets.Component.Panel.Basic
/-- In the infoview, an **info block** is a top-level collapsible block corresponding to a given
location in a Lean file (e.g. with the header `▼ Basic.lean:12:34`).

A **panel widget** is a component which can appear as a panel inside an info block in the infoview.
For example, a tactic state display.
The type `PanelWidgetProps` represents the props passed to a panel widget.
The TypeScript version is exported as `PanelWidgetProps` from `@leanprover/infoview`.

Note that to be a good citizen which doesn't mess up the infoview layout,
a panel widget should be a block element,
and should provide some way to collapse it,
for example by using `<details>` as the top-level tag.  -/
ProofWidgets.PanelWidgetProps : Type
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.instCompleteLatticePresieve : {C : Type u_1} → [inst : CategoryTheory.Category.{u_2, u_1} C] → (X : C) → CompleteLattice (CategoryTheory.Presieve X)
-- Std.Do.PostCond
Std.Do.ExceptConds.imp.eq_1 : ∀ (x_2 y_2 : Std.Do.ExceptConds Std.Do.PostShape.pure), (x_2 →ₑ y_2) = PUnit.unit
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.size_le_size_alter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  {f : Option β → Option β}, t.size - 1 ≤ (t.alter k f).size
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.instIsSubApplyForall : ∀ {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [inst : Ring R] [inst_1 : (i : ι) → AddCommGroup (M₁ i)]
  [inst_2 : AddCommGroup M₂] [inst_3 : (i : ι) → Module R (M₁ i)] [inst_4 : Module R M₂]
  [inst_5 : (i : ι) → TopologicalSpace (M₁ i)] [inst_6 : TopologicalSpace M₂] [inst_7 : IsTopologicalAddGroup M₂],
  IsSubApply (ContinuousMultilinearMap R M₁ M₂) ((i : ι) → M₁ i) M₂
-- Mathlib.Combinatorics.Matroid.Minor.Contract
Matroid.contract_closure_eq : ∀ {α : Type u_1} (M : Matroid α) (C X : Set α), (M.contract C).closure X = M.closure (X ∪ C) \ C
-- Lean.Meta.LazyDiscrTree
/-- Returns `true` if `e` is one of the following
- A nat literal (numeral)
- `Nat.zero`
- `Nat.succ x` where `isNumeral x`
- `OfNat.ofNat _ x _` where `isNumeral x`  -/
Lean.Meta.LazyDiscrTree.MatchClone.isNumeral : Lean.Expr → Bool
-- Mathlib.Algebra.Star.MonoidHom
StarMonoidHom.coe_mk : ∀ {A : Type u_2} {B : Type u_3} [inst : Monoid A] [inst_1 : Star A] [inst_2 : Monoid B] [inst_3 : Star B] (f : A →* B)
  (h : ∀ (a : A), (↑f).toFun (star a) = star ((↑f).toFun a)), ⇑{ toMonoidHom := f, map_star' := h } = ⇑f
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKeyD_le_of_containsKey : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α},
      Std.Internal.List.containsKey k l = true →
        ∀ {fallback : α}, (compare (Std.Internal.List.minKeyD l fallback) k).isLE = true
-- Mathlib.Algebra.Module.Submodule.Equiv
LinearEquiv.ofInjective.congr_simp : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] {module_M : Module R M} {module_M₂ : Module R₂ M₂}
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} (f : M →ₛₗ[σ₁₂] M₂) [inst_4 : RingHomInvPair σ₁₂ σ₂₁]
  [inst_5 : RingHomInvPair σ₂₁ σ₁₂] (h : Function.Injective ⇑f),
  LinearEquiv.ofInjective f h = LinearEquiv.ofInjective f h
-- Mathlib.Algebra.Group.Pointwise.Set.ListOfFn
Set.mem_sum_list_ofFn : ∀ {α : Type u_1} [inst : AddMonoid α] {n : ℕ} {a : α} {s : Fin n → Set α},
  a ∈ (List.ofFn s).sum ↔ ∃ f, (List.ofFn fun i => ↑(f i)).sum = a
-- Qq.MatchImpl
Qq.Impl.PatVarDecl : Type
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- An alternative version of `Subcomplex.mk`: Instead of requiring that `E` is closed it requires
that `E` is a CW-complex.  -/
Topology.CWComplex.Subcomplex.mk'' : {X : Type u_1} →
  [t : TopologicalSpace X] →
    [T2Space X] →
      (C : Set X) →
        [h : Topology.CWComplex C] →
          (E : Set X) →
            (I : (n : ℕ) → Set (Topology.RelCWComplex.cell C n)) →
              [Topology.CWComplex E] →
                ⋃ n, ⋃ j, Topology.RelCWComplex.openCell n ↑j = E → Topology.RelCWComplex.Subcomplex C
-- Mathlib.Logic.Relation
Relation.SymmGen.symm : ∀ {α : Type u_1} {r : α → α → Prop} {a b : α}, Relation.SymmGen r a b → Relation.SymmGen r b a
-- Init.Data.List.Monadic
List.zipWithM'.induct_unfolding : ∀ {m : Type u → Type v} [inst : Monad m] {α : Type w} {β : Type x} {γ : Type u} (f : α → β → m γ)
  (motive : List α → List β → m (List γ) → Prop),
  (∀ (x : α) (xs : List α) (y : β) (ys : List β),
      motive xs ys (List.zipWithM' f xs ys) →
        motive (x :: xs) (y :: ys) do
          let z ← f x y
          let zs ← List.zipWithM' f xs ys
          pure (z :: zs)) →
    (∀ (t : List α) (ys : List β),
        (∀ (x : α) (xs : List α) (y : β) (ys_1 : List β), t = x :: xs → ys = y :: ys_1 → False) →
          motive t ys (pure [])) →
      ∀ (xs : List α) (ys : List β), motive xs ys (List.zipWithM' f xs ys)
-- Mathlib.RingTheory.IsTensorProduct
IsBaseChange.lift.congr_simp : ∀ {R : Type u_1} {M : Type v₁} {N : Type v₂} {S : Type v₃} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N]
  [inst_2 : CommSemiring R] [inst_3 : CommSemiring S] [inst_4 : Algebra R S] [inst_5 : Module R M] [inst_6 : Module R N]
  [inst_7 : Module S N] [inst_8 : IsScalarTower R S N] {f f_1 : M →ₗ[R] N} (e_f : f = f_1) (h : IsBaseChange S f)
  {Q : Type u_3} [inst_9 : AddCommMonoid Q] [inst_10 : Module S Q] [inst_11 : Module R Q]
  [inst_12 : IsScalarTower R S Q] (g g_1 : M →ₗ[R] Q), g = g_1 → h.lift g = ⋯.lift g_1
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mod
CategoryTheory.Mod.trivialAction_X : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (M : CategoryTheory.Mon C) (X : C), (CategoryTheory.Mod.trivialAction M X).X = X
-- Init.Data.BitVec.Bitblast
/-- If `x &&& y = 0`, then addition does not overflow, and thus `(x + y).toNat = x.toNat + y.toNat`.
 -/
BitVec.toNat_add_of_and_eq_zero : ∀ {w : ℕ} {x y : BitVec w}, x &&& y = 0#w → (x + y).toNat = x.toNat + y.toNat
-- Mathlib.Topology.MetricSpace.PiNat
/-- A function to a pseudo-metric-space is `1`-Lipschitz if and only if points in the same cylinder
of length `n` are sent to points within distance `(1/2)^n`.
Not expressed using `LipschitzWith` as we don't have a metric space structure  -/
PiNat.lipschitz_with_one_iff_forall_dist_image_le_of_mem_cylinder : ∀ {E : ℕ → Type u_1} {α : Type u_2} [inst : PseudoMetricSpace α] {f : ((n : ℕ) → E n) → α},
  (∀ (x y : (n : ℕ) → E n), dist (f x) (f y) ≤ dist x y) ↔
    ∀ (x y : (n : ℕ) → E n) (n : ℕ), y ∈ PiNat.cylinder x n → dist (f x) (f y) ≤ (1 / 2) ^ n
-- Mathlib.Algebra.Polynomial.Div
Polynomial.exists_eq_pow_rootMultiplicity_mul_and_not_dvd : ∀ {R : Type u} [inst : Ring R] (p : Polynomial R),
  p ≠ 0 →
    ∀ (a : R),
      ∃ q,
        p = (Polynomial.X - Polynomial.C a) ^ Polynomial.rootMultiplicity a p * q ∧ ¬Polynomial.X - Polynomial.C a ∣ q
-- Mathlib.Data.List.Basic
List.getLast_append_singleton : ∀ {α : Type u} {a : α} (l : List α), (l ++ [a]).getLast ⋯ = a
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
/-- If `F : J ⥤ K ⥤ C` is a functor into a functor category which has a colimit,
then the evaluation of that colimit at `k` is the colimit of the evaluations of `F.obj j` at `k`.
 -/
CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation : {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.HasColimitsOfShape J C] →
              (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) →
                (k : K) →
                  (CategoryTheory.Limits.colimit F).obj k ≅
                    CategoryTheory.Limits.colimit (F.comp ((CategoryTheory.evaluation K C).obj k))
-- Init.Data.Array.Attach
Array.attachWith_eq_empty_iff : ∀ {α : Type u_1} {xs : Array α} {P : α → Prop} {H : ∀ a ∈ xs, P a}, xs.attachWith P H = #[] ↔ xs = #[]
-- Std.Data.TreeMap.Basic
/-- Returns the `n`-th smallest key.  -/
Std.TreeMap.keyAtIdx : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → (t : Std.TreeMap α β cmp) → (n : ℕ) → n < t.size → α
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnModule.instDistribSMul : {Γ : Type u_1} →
  {Γ' : Type u_2} →
    {R : Type u_3} →
      {V : Type u_5} →
        [inst : PartialOrder Γ] →
          [inst_1 : PartialOrder Γ'] →
            [inst_2 : VAdd Γ Γ'] →
              [IsOrderedCancelVAdd Γ Γ'] →
                [inst_4 : AddCommMonoid V] →
                  [inst_5 : MonoidWithZero R] →
                    [inst_6 : DistribSMul R V] → DistribSMul (HahnSeries Γ R) (HahnModule Γ' R V)
-- Mathlib.Analysis.Normed.Ring.Basic
NNReal.norm_eq : ∀ (x : NNReal), ‖↑x‖ = ↑x
-- Mathlib.Data.Finset.Prod
Finset.diag.eq_1 : ∀ {α : Type u_1} (s : Finset α), s.diag = Finset.map { toFun := Function.diag, inj' := ⋯ } s
-- Mathlib.Combinatorics.Young.YoungDiagram
YoungDiagram.mk : (cells : Finset (ℕ × ℕ)) → IsLowerSet ↑cells → YoungDiagram
-- Mathlib.Topology.Order.LawsonTopology
Topology.lawson.eq_1 : ∀ (α : Type u_2) [inst : Preorder α], Topology.lawson α = Topology.lower α ⊓ Topology.scott α Set.univ
-- Mathlib.Computability.Language
/-- Nonterminal symbols (must not be present when the word being generated is finalized)  -/
Symbol.nonterminal : {T : Type u_4} → {N : Type u_5} → N → Symbol T N
-- Mathlib.Data.Nat.Prime.Int
/-- Two prime powers with positive exponents are equal only when the primes and the
exponents are equal.  -/
Nat.Prime.pow_inj : ∀ {p q m n : ℕ}, Nat.Prime p → Nat.Prime q → p ^ (m + 1) = q ^ (n + 1) → p = q ∧ m = n
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.Subgraph.Connected.mk : ∀ {V : Type u} {G : SimpleGraph V} {H : G.Subgraph}, H.coe.Connected → H.Connected
-- Mathlib.Data.Finset.Sups
Finset.disjSups_right_comm : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : DistribLattice α] [inst_2 : OrderBot α]
  [inst_3 : DecidableRel Disjoint] (s t u : Finset α), (s.disjSups t).disjSups u = (s.disjSups u).disjSups t
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
SimplexCategoryGenRel.simplicialEvalσ.eq_1 : ∀ (j : ℕ), SimplexCategoryGenRel.simplicialEvalσ [] j = j
-- Mathlib.Data.Multiset.Defs
Multiset.instPartialOrder : {α : Type u_1} → PartialOrder (Multiset α)
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.Struct.ltFn? : Lean.Meta.Grind.Arith.Linear.Struct → Option Lean.Expr
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.inv_inr : ∀ {R : Type u} {M : Type v} [inst : DivisionSemiring R] [inst_1 : AddCommGroup M] [inst_2 : Module Rᵐᵒᵖ M]
  [inst_3 : Module R M] (m : M), (TrivSqZeroExt.inr m)⁻¹ = 0
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrpObj.right_neg_assoc : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.CartesianMonoidalCategory C}
  (X : C) [self : CategoryTheory.AddGrpObj X] {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.id X) CategoryTheory.AddGrpObj.neg)
      (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit X)
      (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.zero h)
-- Mathlib.Topology.WithTopology
WithTopology.ofTopology_surjective : ∀ {X : Type u_1} (t : TopologicalSpace X), Function.Surjective WithTopology.ofTopology
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidHom.instFunLike.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : MulOneClass α]
  [inst_3 : MulOneClass β], OrderMonoidHom.instFunLike = { coe := fun f => (↑f.toMonoidHom).toFun, coe_injective := ⋯ }
-- Mathlib.Analysis.InnerProductSpace.Dual
/-- An element `x` of an inner product space `E` induces an element of the strong dual space
`StrongDual 𝕜 E`, the map `fun y => ⟪x, y⟫`; moreover this operation is a conjugate-linear isometric
embedding of `E` into `StrongDual 𝕜 E`.
If `E` is complete, this operation is surjective, hence a conjugate-linear isometric equivalence;
see `toDual`.
 -/
InnerProductSpace.toDualMap : (𝕜 : Type u_1) →
  (E : Type u_2) →
    [inst : RCLike 𝕜] →
      [inst_1 : SeminormedAddCommGroup E] → [inst_2 : InnerProductSpace 𝕜 E] → E →ₗᵢ⋆[𝕜] StrongDual 𝕜 E
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.Hom.toExtensionHom_toAlgHom_apply : ∀ {R : Type u} {S : Type v} {ι : Type w} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.Generators R S ι) {R' : Type u_1} {S' : Type u_2} {ι' : Type u_3} [inst_3 : CommRing R']
  [inst_4 : CommRing S'] [inst_5 : Algebra R' S'] (P' : Algebra.Generators R' S' ι') [inst_6 : Algebra R R']
  [inst_7 : Algebra S S'] [inst_8 : Algebra R S'] [inst_9 : IsScalarTower R R' S'] [inst_10 : IsScalarTower R S S']
  (f : P.Hom P') (x : P.toExtension.Ring), f.toExtensionHom.toAlgHom x = f.toAlgHom x
-- Mathlib.RingTheory.Valuation.ValuationRing
PreValuationRing.mk : ∀ {A : Type u} [inst : Mul A], (∀ (a b : A), ∃ c, a * c = b ∨ b * c = a) → PreValuationRing A