mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.Congruence.Basic
Con.comap.congr_simp : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] (f f_1 : M → N) (e_f : f = f_1)
  (H : ∀ (x y : M), f (x * y) = f x * f y) (c c_1 : Con N), c = c_1 → Con.comap f H c = Con.comap f_1 ⋯ c_1
-- Mathlib.Data.TypeVec
TypeVec.dropFun_RelLast' : ∀ {n : ℕ} {α : TypeVec.{u_1} n} {β : Type u_1} (R : β → β → Prop), TypeVec.dropFun (α.RelLast' R) = α.repeatEq
-- Mathlib.LinearAlgebra.Eigenspace.Basic
Module.End.mapsTo_genEigenspace_of_comm : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {f g : Module.End R M},
  Commute f g → ∀ (μ : R) (k : ℕ∞), Set.MapsTo ⇑g ↑((f.genEigenspace μ) k) ↑((f.genEigenspace μ) k)
-- Mathlib.GroupTheory.Perm.Finite
Equiv.Perm.subtypePermOfFintype_apply : ∀ {α : Type u} (f : Equiv.Perm α) {p : α → Prop} [inst : Finite { x // p x }] (h : ∀ (x : α), p x → p (f x))
  (x : { x // p x }), (f.subtypePermOfFintype h) x = ⟨f ↑x, ⋯⟩
-- Lean.Meta.Sym.ReplaceS
_private.Lean.Meta.Sym.ReplaceS.0.Lean.Meta.Sym.visit.match_1.eq_12 : ∀ (motive : Lean.Expr → Sort u_1) (declName : Lean.Name) (t v b : Lean.Expr) (nondep : Bool)
  (h_1 : (a : Lean.Literal) → motive (Lean.Expr.lit a)) (h_2 : (mvarId : Lean.MVarId) → motive (Lean.Expr.mvar mvarId))
  (h_3 : (deBruijnIndex : ℕ) → motive (Lean.Expr.bvar deBruijnIndex))
  (h_4 : (fvarId : Lean.FVarId) → motive (Lean.Expr.fvar fvarId))
  (h_5 : (declName : Lean.Name) → (us : List Lean.Level) → motive (Lean.Expr.const declName us))
  (h_6 : (u : Lean.Level) → motive (Lean.Expr.sort u)) (h_7 : (f a : Lean.Expr) → motive (f.app a))
  (h_8 : (data : Lean.MData) → (a : Lean.Expr) → motive (Lean.Expr.mdata data a))
  (h_9 : (typeName : Lean.Name) → (idx : ℕ) → (a : Lean.Expr) → motive (Lean.Expr.proj typeName idx a))
  (h_10 :
    (binderName : Lean.Name) →
      (d b : Lean.Expr) → (binderInfo : Lean.BinderInfo) → motive (Lean.Expr.forallE binderName d b binderInfo))
  (h_11 :
    (binderName : Lean.Name) →
      (d b : Lean.Expr) → (binderInfo : Lean.BinderInfo) → motive (Lean.Expr.lam binderName d b binderInfo))
  (h_12 :
    (declName : Lean.Name) → (t v b : Lean.Expr) → (nondep : Bool) → motive (Lean.Expr.letE declName t v b nondep)),
  (match Lean.Expr.letE declName t v b nondep with
    | Lean.Expr.lit a => h_1 a
    | Lean.Expr.mvar mvarId => h_2 mvarId
    | Lean.Expr.bvar deBruijnIndex => h_3 deBruijnIndex
    | Lean.Expr.fvar fvarId => h_4 fvarId
    | Lean.Expr.const declName us => h_5 declName us
    | Lean.Expr.sort u => h_6 u
    | f.app a => h_7 f a
    | Lean.Expr.mdata data a => h_8 data a
    | Lean.Expr.proj typeName idx a => h_9 typeName idx a
    | Lean.Expr.forallE binderName d b binderInfo => h_10 binderName d b binderInfo
    | Lean.Expr.lam binderName d b binderInfo => h_11 binderName d b binderInfo
    | Lean.Expr.letE declName t v b nondep => h_12 declName t v b nondep) =
    h_12 declName t v b nondep
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
/-- For a `WeierstrassCurve` defined over a field of characteristic = 2,
there is an explicit change of variables of it to `WeierstrassCurve.IsCharTwoNF`, that is,
`Y² + XY = X³ + a₂X² + a₆` (`WeierstrassCurve.IsCharTwoJNeZeroNF`) or
`Y² + a₃Y = X³ + a₄X + a₆` (`WeierstrassCurve.IsCharTwoJEqZeroNF`).  -/
WeierstrassCurve.toCharTwoNF : {F : Type u_2} → [inst : Field F] → WeierstrassCurve F → [DecidableEq F] → WeierstrassCurve.VariableChange F
-- Mathlib.Algebra.Module.Torsion.Basic
Module.Quotient.mk_smul_mk : ∀ {R : Type u_1} (M : Type u_2) [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (I : Ideal R)
  [inst_3 : I.IsTwoSided] (r : R) (m : M),
  (Ideal.Quotient.mk I) r • Submodule.Quotient.mk m = Submodule.Quotient.mk (r • m)
-- Mathlib.LinearAlgebra.Projection
Submodule.quotientEquivOfIsCompl_apply_mk_right : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {p q : Submodule R E}
  (h : IsCompl p q) (x : ↥q), (p.quotientEquivOfIsCompl q h) (Submodule.Quotient.mk ↑x) = x
-- Mathlib.Data.FinEnum
/-- Any enumeration of an empty type has length 0.  -/
FinEnum.card_eq_zero : ∀ {α : Type u} [inst : FinEnum α] [IsEmpty α], FinEnum.card α = 0
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
IsLeftUniformGroup.uniformity_eq : ∀ {G : Type u_7} {inst : UniformSpace G} {inst_1 : Group G} [self : IsLeftUniformGroup G],
  uniformity G = Filter.comap (fun x => x.1⁻¹ * x.2) (nhds 1)
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.getEntryGE?ₘ'.match_1.eq_2 : ∀ {α : Type u_2} {β : α → Type u_1} [inst : Ord α] (k : α)
  (motive : Option ((a : α) × β a) → Std.DTreeMap.Internal.Impl.ExplorationStep α β (compare k) → Sort u_3)
  (base : Option ((a : α) × β a)) (a : List ((a : α) × β a)) (c : Std.DTreeMap.Internal.Cell α β (compare k))
  (r : List ((a : α) × β a))
  (h_1 :
    (x : Option ((a : α) × β a)) →
      (k' : α) →
        (a : compare k k' = Ordering.lt) →
          (v : β k') →
            (a_1 : List ((a : α) × β a)) → motive x (Std.DTreeMap.Internal.Impl.ExplorationStep.lt k' a v a_1))
  (h_2 :
    (base : Option ((a : α) × β a)) →
      (a : List ((a : α) × β a)) →
        (c : Std.DTreeMap.Internal.Cell α β (compare k)) →
          (r : List ((a : α) × β a)) → motive base (Std.DTreeMap.Internal.Impl.ExplorationStep.eq a c r))
  (h_3 :
    (base : Option ((a : α) × β a)) →
      (a : List ((a : α) × β a)) →
        (a_1 : α) →
          (a_2 : compare k a_1 = Ordering.gt) →
            (a_3 : β a_1) → motive base (Std.DTreeMap.Internal.Impl.ExplorationStep.gt a a_1 a_2 a_3)),
  (match base, Std.DTreeMap.Internal.Impl.ExplorationStep.eq a c r with
    | x, Std.DTreeMap.Internal.Impl.ExplorationStep.lt k' a v a_1 => h_1 x k' a v a_1
    | base, Std.DTreeMap.Internal.Impl.ExplorationStep.eq a c r => h_2 base a c r
    | base, Std.DTreeMap.Internal.Impl.ExplorationStep.gt a a_1 a_2 a_3 => h_3 base a a_1 a_2 a_3) =
    h_2 base a c r
-- Mathlib.Tactic.DuplicateDecls
/-- An inductive type for the kind of duplicate declarations to search for.  -/
Mathlib.Tactic.DuplicateDecls.Target : Type
-- Mathlib.Algebra.FiniteSupport.Basic
Function.HasFiniteSupport.smul_right : ∀ {α : Type u_1} {R : Type u_2} {M : Type u_3} [inst : Zero M] [inst_1 : SMulZeroClass R M] (f : α → R) {g : α → M},
  Function.HasFiniteSupport g → Function.HasFiniteSupport (f • g)
-- Mathlib.Data.QPF.Multivariate.Constructions.Const
MvQPF.Const.mvqpf : {n : ℕ} → {A : Type u} → MvQPF (MvQPF.Const n A)
-- Mathlib.CategoryTheory.Limits.WeakLimits.WeakKernels
/-- A weak equalizer of `f` and `g` is a weak kernel of `f - g`.  -/
CategoryTheory.Preadditive.isWeakLimitKernelForkOfFork : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {X Y : C} →
        {f g : X ⟶ Y} →
          {c : CategoryTheory.Limits.Fork f g} →
            CategoryTheory.Limits.IsWeakLimit c →
              CategoryTheory.Limits.IsWeakLimit (CategoryTheory.Preadditive.kernelForkOfFork c)
-- Mathlib.Probability.Independence.Basic
/-- A family of sets of sets `π : ι → Set (Set Ω)` is independent with respect to a measure `μ` if
for any finite set of indices `s = {i_1, ..., i_n}`, for any sets
`f i_1 ∈ π i_1, ..., f i_n ∈ π i_n`, then `μ (⋂ i in s, f i) = ∏ i ∈ s, μ (f i) `.
It will be used for families of π-systems.  -/
ProbabilityTheory.iIndepSets : {Ω : Type u_1} →
  {ι : Type u_2} →
    {_mΩ : MeasurableSpace Ω} →
      (ι → Set (Set Ω)) → autoParam (MeasureTheory.Measure Ω) ProbabilityTheory.iIndepSets._auto_1 → Prop
-- Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Multiset.prod_dvd_prod_of_le : ∀ {M : Type u_5} [inst : CommMonoid M] {s t : Multiset M}, s ≤ t → s.prod ∣ t.prod
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
mfderiv_zero_of_not_mdifferentiableAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {x : M},
  ¬MDiffAt f x → mfderiv% f x = 0
-- Qq.Match
_private.Qq.Match.0.Qq.floatExprAntiquot : ℕ → Lean.Term → StateT (Array Qq.Lift✝) Lean.MacroM Lean.Term
-- Mathlib.Data.Fin.Tuple.Basic
Fin.append_elim0 : ∀ {m : ℕ} {α : Sort u_1} (u : Fin m → α), Fin.append u Fin.elim0 = u ∘ Fin.cast ⋯
-- Mathlib.Analysis.CStarAlgebra.GelfandDuality
WeakDual.CharacterSpace.mem_spectrum_iff_exists : ∀ {A : Type u_1} [inst : NormedCommRing A] [inst_1 : NormedAlgebra ℂ A] [CompleteSpace A] {a : A} {z : ℂ},
  z ∈ spectrum ℂ a ↔ ∃ f, f a = z
-- Mathlib.Order.Interval.Finset.Basic
Finset.left_mem_uIcc : ∀ {α : Type u_2} [inst : Lattice α] [inst_1 : LocallyFiniteOrder α] {a b : α}, a ∈ Finset.uIcc a b
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get?_union_of_not_mem_left : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.ExtDTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] {k : α},
  k ∉ t₁ → Std.ExtDTreeMap.Const.get? (t₁.union t₂) k = Std.ExtDTreeMap.Const.get? t₂ k
-- Mathlib.Algebra.Ring.Pi
Pi.commSemiring : {I : Type u} → {f : I → Type v} → [(i : I) → CommSemiring (f i)] → CommSemiring ((i : I) → f i)
-- Init.Data.Vector.Lemmas
Vector.getElem?_set_ne : ∀ {α : Type u_1} {n i j : ℕ} {xs : Vector α n} {x : α} (hi : i < n), i ≠ j → (xs.set i x hi)[j]? = xs[j]?
-- Mathlib.CategoryTheory.Monad.Algebra
CategoryTheory.Monad.adj_counit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C),
  T.adj.counit = { app := fun Y => { f := Y.a, h := ⋯ }, naturality := ⋯ }
-- Mathlib.Data.Fintype.Quotient
/-- Given a collection of setoids indexed by a type `ι`, a list `l` of indices, and a function that
for each `i ∈ l` gives a term of the corresponding quotient type, then there is a corresponding
term in the quotient of the product of the setoids indexed by `l`.  -/
Quotient.listChoice : {ι : Type u_1} →
  [DecidableEq ι] →
    {α : ι → Sort u_2} →
      {S : (i : ι) → Setoid (α i)} → {l : List ι} → ((i : ι) → i ∈ l → Quotient (S i)) → Quotient piSetoid
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
CategoryTheory.IsPushout.flip_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P}
  {inr : Y ⟶ P}, CategoryTheory.IsPushout f g inl inr ↔ CategoryTheory.IsPushout g f inr inl
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.rpow_left_injective : ∀ {x : ℝ}, x ≠ 0 → Function.Injective fun y => y ^ x
-- Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
MvPolynomial.esymmAlgHomMonomial.eq_1 : ∀ (σ : Type u_1) {R : Type u_3} {n : ℕ} [inst : CommSemiring R] [inst_1 : Fintype σ] (t : Fin n →₀ ℕ) (r : R),
  MvPolynomial.esymmAlgHomMonomial σ t r = ↑((MvPolynomial.esymmAlgHom σ R n) ((MvPolynomial.monomial t) r))
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.Functor.CorepresentableBy.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {F : CategoryTheory.Functor C (Type v)} →
      {X : C} →
        (homEquiv : {Y : C} → (X ⟶ Y) ≃ F.obj Y) →
          autoParam
              (∀ {Y Y' : C} (g : Y ⟶ Y') (f : X ⟶ Y),
                homEquiv (CategoryTheory.CategoryStruct.comp f g) =
                  (CategoryTheory.ConcreteCategory.hom (F.map g)) (homEquiv f))
              CategoryTheory.Functor.CorepresentableBy.homEquiv_comp._autoParam →
            F.CorepresentableBy X
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.ofEq_rfl : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_10} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup V]
  [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P] [inst_4 : NormedAddTorsor V P] {s₁ : AffineSubspace 𝕜 P}
  [inst_5 : Nonempty ↥s₁], AffineIsometryEquiv.ofEq s₁ s₁ ⋯ = AffineIsometryEquiv.refl 𝕜 ↥s₁
-- Mathlib.RingTheory.PowerSeries.Evaluation
PowerSeries.eval₂_C : ∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] (φ : R →+* S) (a : S)
  [inst_2 : UniformSpace R] [inst_3 : UniformSpace S] (r : R), PowerSeries.eval₂ φ a (PowerSeries.C r) = φ r
-- Mathlib.Tactic.Order.CollectFacts
Mathlib.Tactic.Order.AtomicFact.isInf : ℕ → ℕ → ℕ → Mathlib.Tactic.Order.AtomicFact
-- Init.Data.List.MapIdx
List.mapFinIdx.go.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (as : List α) (f : (i : ℕ) → α → i < as.length → β) (acc : Array β)
  (a : [].length + acc.size = as.length), List.mapFinIdx.go as f [] acc a = acc.toList
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
Std.DHashMap.Internal.AssocList.getKey!_eq : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Inhabited α] {l : Std.DHashMap.Internal.AssocList α β} {a : α},
  Std.DHashMap.Internal.AssocList.getKey! a l = Std.Internal.List.getKey! a l.toList
-- Mathlib.Order.CompleteLattice.Defs
toDual_sInf : ∀ {α : Type u_1} [inst : InfSet α] (s : Set α), OrderDual.toDual (sInf s) = sSup (⇑OrderDual.ofDual ⁻¹' s)
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.hasKernels_of_hasEqualizers : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [CategoryTheory.Limits.HasEqualizers C], CategoryTheory.Limits.HasKernels C
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineMap.vsub_lineMap : ∀ {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddTorsor V₁ P₁] (p₁ p₂ p₃ : P₁) (c : k),
  p₁ -ᵥ (AffineMap.lineMap p₂ p₃) c = (AffineMap.lineMap (p₁ -ᵥ p₂) (p₁ -ᵥ p₃)) c
-- Std.Data.Iterators.Lemmas.Combinators.TakeWhile
_private.Std.Data.Iterators.Lemmas.Combinators.TakeWhile.0.Std.Iter.atIdxSlow?_eq_match.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match n.succ with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_2 n
-- Mathlib.GroupTheory.Finiteness
/-- An equivalent expression of `Monoid.FG` in terms of `Set.Finite` instead of `Finset`.  -/
Monoid.fg_iff : ∀ {M : Type u_1} [inst : Monoid M], Monoid.FG M ↔ ∃ S, Submonoid.closure S = ⊤ ∧ S.Finite
-- Init.Data.Array.Extract
Array.extract_takeWhile : ∀ {α : Type u_1} {p : α → Bool} {as : Array α} {i : ℕ},
  (Array.takeWhile p as).extract 0 i = Array.takeWhile p (as.extract 0 i)
-- Mathlib.Algebra.Group.Action.Pretransitive
MulAction.IsPretransitive.mk : ∀ {M : Type u_5} {α : Type u_6} [inst : SMul M α], (∀ (x y : α), ∃ g, g • x = y) → MulAction.IsPretransitive M α
-- Lean.DocString.Types
/-- The part's title  -/
Lean.Doc.Part.title : {i : Type u} → {b : Type v} → {p : Type w} → Lean.Doc.Part i b p → Array (Lean.Doc.Inline i)
-- Mathlib.CategoryTheory.Abelian.LeftDerived
CategoryTheory.instIsIsoAppFromLeftDerivedZero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.HasProjectiveResolutions C]
  [inst_4 : CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [inst_5 : F.Additive]
  [CategoryTheory.Limits.PreservesFiniteColimits F] (X : C), CategoryTheory.IsIso (F.fromLeftDerivedZero.app X)
-- Mathlib.Probability.Decision.Risk.Defs
/-- The Bayes risk with respect to a prior `π`, defined as the infimum of the average risks of all
estimators.  -/
ProbabilityTheory.bayesRisk : {Θ : Type u_1} →
  {𝓧 : Type u_2} →
    {𝓨 : Type u_3} →
      {mΘ : MeasurableSpace Θ} →
        {m𝓧 : MeasurableSpace 𝓧} →
          [MeasurableSpace 𝓨] → (Θ → 𝓨 → ENNReal) → ProbabilityTheory.Kernel Θ 𝓧 → MeasureTheory.Measure Θ → ENNReal
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
_private.Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula.0.WeierstrassCurve.Jacobian.toAffine_slope_of_eq : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Jacobian F} [inst_1 : DecidableEq F] {P Q : Fin 3 → F},
  P 2 ≠ 0 →
    Q 2 ≠ 0 →
      P 0 * Q 2 ^ 2 = Q 0 * P 2 ^ 2 →
        P 1 * Q 2 ^ 3 ≠ W.negY Q * P 2 ^ 3 →
          W.toAffine.slope (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (P 1 / P 2 ^ 3) (Q 1 / Q 2 ^ 3) = -W.dblU P / W.dblZ P
-- Mathlib.Data.Set.Piecewise
Set.piecewise_insert_of_ne : ∀ {α : Type u_1} {δ : α → Sort u_7} (s : Set α) (f g : (i : α) → δ i) [inst : (j : α) → Decidable (j ∈ s)] {i j : α},
  i ≠ j → ∀ [inst_1 : (i : α) → Decidable (i ∈ insert j s)], (insert j s).piecewise f g i = s.piecewise f g i
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.leadingCoeff_C_mul_of_isUnit : ∀ {R : Type u} {a : R} [inst : Semiring R],
  IsUnit a → ∀ (p : Polynomial R), (Polynomial.C a * p).leadingCoeff = a * p.leadingCoeff
-- Mathlib.RingTheory.HahnSeries.Lex
HahnSeries.embDomainOrderAddMonoidHom_apply : ∀ {Γ : Type u_1} {R : Type u_2} [inst : LinearOrder Γ] [inst_1 : PartialOrder R] {Γ' : Type u_3}
  [inst_2 : LinearOrder Γ'] (f : Γ ↪o Γ') [inst_3 : AddMonoid R] (a : Lex (HahnSeries Γ R)),
  (HahnSeries.embDomainOrderAddMonoidHom f) a = (HahnSeries.embDomainOrderEmbedding f).toOrderHom.toFun a
-- Mathlib.NumberTheory.Divisors
Int.divisors_neg : ∀ {z : ℤ}, (-z).divisors = z.divisors
-- Mathlib.CategoryTheory.Skeletal
CategoryTheory.Functor.instFullSkeletonMapSkeleton : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [F.Full], F.mapSkeleton.Full
-- Mathlib.Order.Hom.Basic
OrderIso.ofUnique_apply : ∀ (α : Type u_6) (β : Type u_7) [inst : Unique α] [inst_1 : Unique β] [inst_2 : Preorder α] [inst_3 : Preorder β]
  (a : α), (OrderIso.ofUnique α β) a = default
-- Mathlib.CategoryTheory.ConcreteCategory.Basic
CategoryTheory.hom_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC] {X : C},
  ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) = id
-- Mathlib.Combinatorics.SimpleGraph.Finsubgraph
SimpleGraph.Finsubgraph.coe_sInf : ∀ {V : Type u} {G : SimpleGraph V} [inst : Finite V] (s : Set G.Finsubgraph), ↑(sInf s) = ⨅ G_1 ∈ s, ↑G_1
-- Lean.Meta.HaveTelescope
_private.Lean.Meta.HaveTelescope.0.Lean.Meta.SimpHaveResult.mk : Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Bool → Lean.Meta.SimpHaveResult✝
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
CategoryTheory.Functor.mapBinaryBicone_inr : ∀ {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] {X Y : C}
  (b : CategoryTheory.Limits.BinaryBicone X Y), (F.mapBinaryBicone b).inr = F.map b.inr
-- Mathlib.RingTheory.Ideal.Quotient.Basic
finite_iff_ideal_quotient : ∀ {R : Type u_3} [inst : Ring R] (I : Ideal R), Finite R ↔ Finite ↥I ∧ Finite (R ⧸ I)
-- Mathlib.RingTheory.AdicCompletion.AsTensorProduct
AdicCompletion.ofTensorProductEquivOfFiniteNoetherian_symm_of : ∀ {R : Type u} [inst : CommRing R] (I : Ideal R) (M : Type u) [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : IsNoetherianRing R] [inst_4 : Module.Finite R M] (x : M),
  (AdicCompletion.ofTensorProductEquivOfFiniteNoetherian I M).symm ((AdicCompletion.of I M) x) = 1 ⊗ₜ[R] x
-- Mathlib.Algebra.Group.End
Equiv.Perm.inv_def : ∀ {α : Type u_4} (f : Equiv.Perm α), f⁻¹ = Equiv.symm f
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
CategoryTheory.Bicategory.rightAdjointSquare.comp_vhcomp : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d e f x y z : B} {g₁ : a ⟶ d} {h₁ : b ⟶ e} {k₁ : c ⟶ f}
  {g₂ : d ⟶ x} {h₂ : e ⟶ y} {k₂ : f ⟶ z} {r₁ : b ⟶ a} {r₂ : c ⟶ b} {r₃ : e ⟶ d} {r₄ : f ⟶ e} {r₅ : y ⟶ x} {r₆ : z ⟶ y}
  (α : CategoryTheory.CategoryStruct.comp r₁ g₁ ⟶ CategoryTheory.CategoryStruct.comp h₁ r₃)
  (β : CategoryTheory.CategoryStruct.comp r₂ h₁ ⟶ CategoryTheory.CategoryStruct.comp k₁ r₄)
  (γ : CategoryTheory.CategoryStruct.comp r₃ g₂ ⟶ CategoryTheory.CategoryStruct.comp h₂ r₅)
  (δ : CategoryTheory.CategoryStruct.comp r₄ h₂ ⟶ CategoryTheory.CategoryStruct.comp k₂ r₆),
  CategoryTheory.Bicategory.rightAdjointSquare.comp α β γ δ =
    CategoryTheory.Bicategory.rightAdjointSquare.vcomp (CategoryTheory.Bicategory.rightAdjointSquare.hcomp α β)
      (CategoryTheory.Bicategory.rightAdjointSquare.hcomp γ δ)
-- Mathlib.RingTheory.Smooth.NoetherianDescent
_private.Mathlib.RingTheory.Smooth.NoetherianDescent.0.Algebra.Smooth.DescentAux.rels : {A : Type u} →
  {B : Type u_2} →
    [inst : CommRing A] → [inst_1 : CommRing B] → [inst_2 : Algebra A B] → Algebra.Smooth.DescentAux✝ A B → Type
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
/-- Version of `tprod_eq_mul_tprod_ite` for `CommMonoid` rather than `CommGroup`.
Requires a different convergence assumption involving `Function.update`.  -/
Multipliable.tprod_eq_mul_tprod_ite' : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {L : SummationFilter β} [T2Space α]
  [ContinuousMul α] [inst_4 : DecidableEq β] [L.LeAtTop] [L.NeBot] {f : β → α} (b : β),
  Multipliable (Function.update f b 1) L → ∏'[L] (x : β), f x = f b * ∏'[L] (x : β), if x = b then 1 else f x
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgEquiv.symm_symm : ∀ {R : Type u_2} {A : Type u_3} {B : Type u_4} [inst : Add A] [inst_1 : Add B] [inst_2 : Mul A] [inst_3 : Mul B]
  [inst_4 : SMul R A] [inst_5 : SMul R B] [inst_6 : Star A] [inst_7 : Star B] (e : A ≃⋆ₐ[R] B), e.symm.symm = e
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.instSMulCommClassSubtypeMemCenter : ∀ {R : Type u_5} {M : Type u_6} [inst : Semiring R] [inst_1 : MulAction R M],
  SMulCommClass R (↥(Subsemiring.center R)) M
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
/-- Induction principle for the type `X.N` of nondegenerate simplices of
a simplicial set `X`.  -/
SSet.N.induction : {X : SSet} →
  {motive : X.N → Sort u_1} → ((n : ℕ) → (x : ↑(X.nonDegenerate n)) → motive (SSet.N.mk ↑x ⋯)) → (s : X.N) → motive s
-- Mathlib.RingTheory.FiniteLength
/-- A module of finite length is either trivial or a simple extension of a module known
to be of finite length.  -/
IsFiniteLength : (R : Type u_1) → [inst : Ring R] → (M : Type u_2) → [inst_1 : AddCommGroup M] → [Module R M] → Prop
-- Mathlib.MeasureTheory.Group.Integral
/-- Translating a function by right-multiplication does not change its integral with respect to a
right-invariant measure.  -/
MeasureTheory.integral_mul_right_eq_self : ∀ {G : Type u_4} {E : Type u_5} [inst : MeasurableSpace G] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E]
  {μ : MeasureTheory.Measure G} [inst_3 : Group G] [MeasurableMul G] [μ.IsMulRightInvariant] (f : G → E) (g : G),
  ∫ (x : G), f (x * g) ∂μ = ∫ (x : G), f x ∂μ
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get!_inter_of_not_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited β],
  m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₂ → Std.DHashMap.Raw.Const.get! (m₁ ∩ m₂) k = default
-- Mathlib.LinearAlgebra.Dual.BaseChange
IsBaseChange.toDualBaseChange_tmul : ∀ {R : Type u_1} [inst : CommSemiring R] {V : Type u_2} [inst_1 : AddCommMonoid V] [inst_2 : Module R V] {W : Type u_3}
  [inst_3 : AddCommMonoid W] [inst_4 : Module R W] {A : Type u_4} [inst_5 : CommSemiring A] [inst_6 : Algebra R A]
  [inst_7 : Module A W] [inst_8 : IsScalarTower R A W] {j : V →ₗ[R] W} (ibc : IsBaseChange A j)
  [inst_9 : Module.Free R V] [inst_10 : Module.Finite R V] (a : A) (f : Module.Dual R V) (v : V),
  (ibc.toDualBaseChange (a ⊗ₜ[R] f)) (j v) = a * (algebraMap R A) (f v)
-- Mathlib.Order.Cover
not_covBy_iff_exists_mem_Ioo : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a < b → (¬a ⋖ b ↔ ∃ c, c ∈ Set.Ioo a b)