mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Category.ModuleCat.Biproducts
/-- The isomorphism `A × B ≃ₗ[R] M` coming from a right split exact sequence `0 ⟶ A ⟶ M ⟶ B ⟶ 0`
of modules.  -/
lequivProdOfRightSplitExact : {R : Type u} →
  {A : Type uA} →
    {M : Type uM} →
      {B : Type uB} →
        [inst : Ring R] →
          [inst_1 : AddCommGroup A] →
            [inst_2 : AddCommGroup B] →
              [inst_3 : AddCommGroup M] →
                [inst_4 : Module R A] →
                  [inst_5 : Module R B] →
                    [inst_6 : Module R M] →
                      {j : A →ₗ[R] M} →
                        {g : M →ₗ[R] B} →
                          {f : B →ₗ[R] M} →
                            Function.Injective ⇑j → j.range = g.ker → g ∘ₗ f = LinearMap.id → (A × B) ≃ₗ[R] M
-- Mathlib.Algebra.Order.Module.Defs
StrictOrderedSemiring.toPosSMulStrictMonoNat : ∀ {α : Type u_1} [inst : Semiring α] [inst_1 : PartialOrder α] [IsStrictOrderedRing α], PosSMulStrictMono ℕ α
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
IsUnramifiedAtInfinitePlaces_of_odd_finrank : ∀ {k : Type u_1} [inst : Field k] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra k K] [IsGalois k K],
  Odd (Module.finrank k K) → IsUnramifiedAtInfinitePlaces k K
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
Matroid.IsRestriction.eq_restrict : ∀ {α : Type u_1} {M N : Matroid α}, N.IsRestriction M → M.restrict N.E = N
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.M.isubtree_cons : ∀ {F : PFunctor.{uA, uB}} [inst : DecidableEq F.A] [inst_1 : Inhabited F.M] (ps : PFunctor.Approx.Path F) {a : F.A}
  (f : F.B a → F.M) {i : F.B a},
  PFunctor.M.isubtree (⟨a, i⟩ :: ps) (PFunctor.M.mk ⟨a, f⟩) = PFunctor.M.isubtree ps (f i)
-- Mathlib.Data.ZMod.Units
/-- Any element of `ZMod N` has the form `u * d` where `u` is a unit and `d` is a divisor of `N`.  -/
ZMod.eq_unit_mul_divisor : ∀ {N : ℕ} (a : ZMod N), ∃ d, d ∣ N ∧ ∃ u, IsUnit u ∧ a = u * ↑d
-- Mathlib.Analysis.Normed.Group.Basic
norm_pow_natAbs : ∀ {E : Type u_5} [inst : SeminormedGroup E] (a : E) (n : ℤ), ‖a ^ n.natAbs‖ = ‖a ^ n‖
-- Mathlib.CategoryTheory.Monoidal.Discrete
CategoryTheory.Discrete.addMonoidal_tensorUnit_as : ∀ (M : Type u) [inst : AddMonoid M],
  (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Discrete M)).as = 0
-- Mathlib.Analysis.Fourier.FourierTransformDeriv
VectorFourier.norm_fourierPowSMulRight_le : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {V : Type u_2} {W : Type u_3}
  [inst_2 : NormedAddCommGroup V] [inst_3 : NormedSpace ℝ V] [inst_4 : NormedAddCommGroup W] [inst_5 : NormedSpace ℝ W]
  (L : V →L[ℝ] W →L[ℝ] ℝ) (f : V → E) (v : V) (n : ℕ),
  ‖VectorFourier.fourierPowSMulRight L f v n‖ ≤ (2 * Real.pi * ‖L‖) ^ n * ‖v‖ ^ n * ‖f v‖
-- Init.Data.Range.Polymorphic.PRange
Std.Rci.instMembershipOfLE : {α : Type u} → [LE α] → Membership α (Std.Rci α)
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
/-- The "nondegenerate simplices" `N n` for all `n : ℕ`.  -/
CategoryTheory.SimplicialObject.Splitting.N : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] → {X : CategoryTheory.SimplicialObject C} → X.Splitting → ℕ → C
-- Mathlib.CategoryTheory.Join.Basic
CategoryTheory.Join.whiskerLeft_inclRight_mkNatTrans : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E]
  {F F' : CategoryTheory.Functor (CategoryTheory.Join C D) E}
  (αₗ : (CategoryTheory.Join.inclLeft C D).comp F ⟶ (CategoryTheory.Join.inclLeft C D).comp F')
  (αᵣ : (CategoryTheory.Join.inclRight C D).comp F ⟶ (CategoryTheory.Join.inclRight C D).comp F')
  (h :
    autoParam
      (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Functor.whiskerRight (CategoryTheory.Join.edgeTransform C D) F)
          ((CategoryTheory.Prod.snd C D).whiskerLeft αᵣ) =
        CategoryTheory.CategoryStruct.comp ((CategoryTheory.Prod.fst C D).whiskerLeft αₗ)
          (CategoryTheory.Functor.whiskerRight (CategoryTheory.Join.edgeTransform C D) F'))
      _auto_114✝),
  (CategoryTheory.Join.inclRight C D).whiskerLeft (CategoryTheory.Join.mkNatTrans αₗ αᵣ h) = αᵣ
-- Mathlib.Data.Matrix.Basic
/-- A version of `Matrix.scalar_commute` for rectangular matrices.  -/
Matrix.scalar_comm : ∀ {m : Type u_2} {n : Type u_3} {α : Type u_11} [inst : Semiring α] [inst_1 : DecidableEq n] [inst_2 : Fintype n]
  [inst_3 : DecidableEq m] [inst_4 : Fintype m] (r : α),
  (∀ (r' : α), Commute r r') → ∀ (M : Matrix m n α), (Matrix.scalar m) r * M = M * (Matrix.scalar n) r
-- Mathlib.Data.Ordmap.Invariants
_private.Mathlib.Data.Ordmap.Invariants.0.Ordnode.eraseMax.match_1.eq_1 : ∀ {α : Type u_1} (motive : Ordnode α → Sort u_2) (h_1 : Unit → motive Ordnode.nil)
  (h_2 : (size : ℕ) → (l : Ordnode α) → (x : α) → motive (Ordnode.node size l x Ordnode.nil))
  (h_3 :
    (size : ℕ) →
      (l : Ordnode α) →
        (x : α) →
          (sz : ℕ) →
            (l' : Ordnode α) → (y : α) → (r' : Ordnode α) → motive (Ordnode.node size l x (Ordnode.node sz l' y r'))),
  (match Ordnode.nil with
    | Ordnode.nil => h_1 ()
    | Ordnode.node size l x Ordnode.nil => h_2 size l x
    | Ordnode.node size l x (Ordnode.node sz l' y r') => h_3 size l x sz l' y r') =
    h_1 ()
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.isScalarTower_bot : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (S : IntermediateField K L)
  {R : Type u_4} [inst_3 : Semiring R] [inst_4 : Algebra L R], IsScalarTower (↥S) L R
-- Mathlib.Algebra.Homology.CochainComplexPlus
/-- The class of quasi-isomorphisms in the category of bounded
below cochain complexes.  -/
CochainComplex.Plus.quasiIso : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      [CategoryTheory.CategoryWithHomology C] → CategoryTheory.MorphismProperty (CochainComplex.Plus C)
-- Mathlib.NumberTheory.Chebyshev
Chebyshev.pi_ge : ∀ (n : ℕ), (↑n * Real.log 2 - Real.log (↑n + 1)) / Real.log ↑n ≤ ↑n.primeCounting
-- Mathlib.Algebra.Order.Ring.Rat
Rat.instIsStrictOrderedRing : IsStrictOrderedRing ℚ
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
SSet.Edge.exists_of_simplex : ∀ {X : SSet} (s : X.obj (Opposite.op { len := 1 })), ∃ x₀ x₁ e, e.edge = s
-- Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
CategoryTheory.MorphismProperty.Under.pushoutCompForgetIso_hom_app_right : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {P Q : CategoryTheory.MorphismProperty T}
  [inst_1 : Q.IsMultiplicative] {X Y : T} (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasPushoutsAlong f]
  [inst_3 : P.IsStableUnderCobaseChangeAlong f] [inst_4 : Q.IsStableUnderCobaseChange] (X_1 : P.Under Q X),
  ((CategoryTheory.MorphismProperty.Under.pushoutCompForgetIso f).hom.app X_1).right =
    CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.pushout X_1.hom f)
-- Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Algebra.SubmersivePresentation.basisCotangent.eq_1 : ∀ {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [inst_3 : Finite σ] (P : Algebra.SubmersivePresentation R S ι σ),
  P.basisCotangent = P.basisDeriv.map P.cotangentEquiv.symm
-- Mathlib.Algebra.Homology.Bifunctor
HomologicalComplex.ιMapBifunctor.congr_simp : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} D] {I₁ : Type u_4}
  {I₂ : Type u_5} {J : Type u_6} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂}
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C₁] [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C₂]
  [inst_5 : CategoryTheory.Preadditive D] (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂)
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [inst_6 : F.PreservesZeroMorphisms]
  [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (c : ComplexShape J) [inst_8 : TotalComplexShape c₁ c₂ c]
  [inst_9 : K₁.HasMapBifunctor K₂ F c] [inst_10 : DecidableEq J] (i₁ : I₁) (i₂ : I₂) (j : J)
  (h : c₁.π c₂ c (i₁, i₂) = j), K₁.ιMapBifunctor K₂ F c i₁ i₂ j h = K₁.ιMapBifunctor K₂ F c i₁ i₂ j h
-- Mathlib.Topology.Homotopy.Lifting
IsCoveringMap.monodromy_trans_apply : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {p : E → X}
  (cov : IsCoveringMap p) {x y z : X} (γ : Path.Homotopic.Quotient x y) (γ' : Path.Homotopic.Quotient y z)
  (e : ↑(p ⁻¹' {x})), cov.monodromy (γ.trans γ') e = cov.monodromy γ' (cov.monodromy γ e)
-- Mathlib.Topology.FiberBundle.Basic
FiberBundleCore.isOpen_baseSet : ∀ {ι : Type u_5} {B : Type u_6} [inst : TopologicalSpace B] {F : Type u_7} [inst_1 : TopologicalSpace F]
  (self : FiberBundleCore ι B F) (i : ι), IsOpen (self.baseSet i)
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.rootSet.eq_1 : ∀ {T : Type w} [inst : CommRing T] (p : Polynomial T) (S : Type u_1) [inst_1 : CommRing S] [inst_2 : IsDomain S]
  [inst_3 : Algebra T S], p.rootSet S = ↑(p.aroots S).toFinset
-- Mathlib.Data.PEquiv
PEquiv.ext : ∀ {α : Type u} {β : Type v} {f g : α ≃. β}, (∀ (x : α), f x = g x) → f = g
-- Mathlib.RingTheory.Valuation.ValuativeRel.Trivial
ValuativeRel.subsingleton_units_valueGroupWithZero_of_trivialRel : ∀ (R Γ : Type) [inst : Ring R] [inst_1 : DecidableEq R] [inst_2 : IsDomain R]
  [inst_3 : LinearOrderedCommGroupWithZero Γ] [inst_4 : ValuativeRel R] [Valuation.Compatible 1],
  Subsingleton (ValuativeRel.ValueGroupWithZero R)ˣ
-- Mathlib.Algebra.Group.InjSurj
Function.Surjective.addSemigroup.eq_1 : ∀ {M₁ : Type u_1} {M₂ : Type u_2} [inst : Add M₂] [inst_1 : AddSemigroup M₁] (f : M₁ → M₂) (hf : Function.Surjective f)
  (mul : ∀ (x y : M₁), f (x + y) = f x + f y),
  Function.Surjective.addSemigroup f hf mul = { toAdd := inst, add_assoc := ⋯ }
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
/-- **Alias** of `mvfderiv_zero`. -/
extDerivFun_zero : ∀ {𝕜 : 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] {F : Type u_8} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {x : M}, d% 0 x = 0
-- Mathlib.Order.SuccPred.Archimedean
/-- **Alias** of `Order.succ_min`. -/
succ_min : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : SuccOrder α] (a b : α),
  Order.succ (min a b) = min (Order.succ a) (Order.succ b)
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.ext : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Semiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : Module A V] [inst_5 : Module A W]
  {ρ : Representation A G V} {σ : Representation A G W} {f g : ρ.IntertwiningMap σ},
  f.toLinearMap = g.toLinearMap → f = g
-- Init.GrindInstances.Ring.Fin
Lean.Grind.Fin.add_comm : ∀ {n : ℕ} (a b : Fin n), a + b = b + a
-- LeanSearchClient.Basic
loogle.queries : Lean.Option ℕ
-- Mathlib.Data.SetLike.Basic
SetLike.ext'_iff : ∀ {A : Type u_1} {B : Type u_2} [i : SetLike A B] {p q : A}, p = q ↔ ↑p = ↑q
-- Mathlib.Dynamics.BirkhoffSum.Basic
birkhoffSum_neg : ∀ {α : Type u_1} {G : Type u_2} [inst : AddCommGroup G] (f : α → α) (g : α → G) (n : ℕ) (x : α),
  birkhoffSum f (-g) n x = -birkhoffSum f g n x
-- Lean.Elab.MutualInductive
/-- Registers an inductive type elaborator for the given syntax node kind.

Commands registered using this attribute are allowed to be used together in mutual blocks with
other inductive type commands. This attribute is mostly used internally for `inductive` and
`structure`.

An inductive type elaborator should have type `Lean.Elab.Command.InductiveElabDescr`.
 -/
Lean.Elab.Command.inductiveElabAttr : Lean.KeyedDeclsAttribute Lean.Elab.Command.InductiveElabDescr
-- Mathlib.RingTheory.DedekindDomain.SInteger
Set.unitEquivUnitsInteger_symm_apply_coe : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (S : Set (IsDedekindDomain.HeightOneSpectrum R))
  (K : Type v) [inst_2 : Field K] [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (x : (↥(S.integer K))ˣ),
  ↑((S.unitEquivUnitsInteger K).symm x) = Units.mk0 ↑↑x ⋯
-- Lean.Meta.Tactic.FunIndCollect
/-- Which functions have exactly one candidate application. Used by `try?` to determine whether
we can use `fun_induction foo` or need `fun_induction foo x y z`.
 -/
Lean.Meta.FunInd.SeenCalls.uniques : Lean.Meta.FunInd.SeenCalls → Lean.NameSet
-- Mathlib.Analysis.Normed.Group.Constructions
pi_nnnorm_lt_iff' : ∀ {ι : Type u_1} {G : ι → Type u_4} [inst : Fintype ι] [inst_1 : (i : ι) → SeminormedGroup (G i)] {x : (i : ι) → G i}
  {r : NNReal}, 0 < r → (‖x‖₊ < r ↔ ∀ (i : ι), ‖x i‖₊ < r)
-- Std.Data.Internal.List.Associative
Std.Internal.List.containsKey_of_length_eq : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l₁ →
    Std.Internal.List.DistinctKeys l₂ →
      l₂.length = l₁.length →
        (∀ (a : α), Std.Internal.List.containsKey a l₁ = true → Std.Internal.List.containsKey a l₂ = true) →
          ∀ (a : α), Std.Internal.List.containsKey a l₂ = true → Std.Internal.List.containsKey a l₁ = true
-- Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv
Complex.contDiffAt_log : ∀ {x : ℂ}, x ∈ Complex.slitPlane → ∀ {n : WithTop ℕ∞}, ContDiffAt ℂ n Complex.log x
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidHom.mk.sizeOf_spec : ∀ {α : Type u_6} {β : Type u_7} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : AddZeroClass α]
  [inst_3 : AddZeroClass β] [inst_4 : SizeOf α] [inst_5 : SizeOf β] (toAddMonoidHom : α →+ β)
  (monotone' : Monotone (↑toAddMonoidHom).toFun),
  sizeOf { toAddMonoidHom := toAddMonoidHom, monotone' := monotone' } = 1 + sizeOf toAddMonoidHom
-- Mathlib.Geometry.Manifold.ChartedSpace
ChartedSpace.mem_chart_source : ∀ {H : Type u_5} {inst : TopologicalSpace H} {M : Type u_6} {inst_1 : TopologicalSpace M} [self : ChartedSpace H M]
  (x : M), x ∈ (ChartedSpace.chartAt x).source
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
CategoryTheory.Oplax.OplaxTrans.whiskerRight_naturality_comp : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} (η : CategoryTheory.Oplax.OplaxTrans F G) {a b c : B} {a' : C} (f : a ⟶ b)
  (g : b ⟶ c) (h : G.obj c ⟶ a'),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerRight (η.naturality (CategoryTheory.CategoryStruct.comp f g)) h)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.associator (η.app a) (G.map (CategoryTheory.CategoryStruct.comp f g)) h).hom
        (CategoryTheory.Bicategory.whiskerLeft (η.app a) (CategoryTheory.Bicategory.whiskerRight (G.mapComp f g) h))) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerRight (F.mapComp f g) (η.app c)) h)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.associator (F.map f) (F.map g) (η.app c)).hom
          h)
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Bicategory.associator (F.map f) (CategoryTheory.CategoryStruct.comp (F.map g) (η.app c))
              h).hom
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Bicategory.whiskerLeft (F.map f)
              (CategoryTheory.Bicategory.whiskerRight (η.naturality g) h))
            (CategoryTheory.CategoryStruct.comp
              (CategoryTheory.Bicategory.associator (F.map f) (CategoryTheory.CategoryStruct.comp (η.app b) (G.map g))
                  h).inv
              (CategoryTheory.CategoryStruct.comp
                (CategoryTheory.Bicategory.whiskerRight
                  (CategoryTheory.Bicategory.associator (F.map f) (η.app b) (G.map g)).inv h)
                (CategoryTheory.CategoryStruct.comp
                  (CategoryTheory.Bicategory.whiskerRight
                    (CategoryTheory.Bicategory.whiskerRight (η.naturality f) (G.map g)) h)
                  (CategoryTheory.CategoryStruct.comp
                    (CategoryTheory.Bicategory.whiskerRight
                      (CategoryTheory.Bicategory.associator (η.app a) (G.map f) (G.map g)).hom h)
                    (CategoryTheory.Bicategory.associator (η.app a)
                        (CategoryTheory.CategoryStruct.comp (G.map f) (G.map g)) h).hom)))))))
-- Init.Data.String.Lemmas.Iterate
String.Slice.Model.revPositionsFrom_eq_cons : ∀ {s : String.Slice} {p : s.Pos} (hp : p ≠ s.startPos),
  String.Slice.Model.revPositionsFrom p = ⟨p.prev hp, ⋯⟩ :: String.Slice.Model.revPositionsFrom (p.prev hp)
-- Batteries.Data.DList.Basic
/-- "Run" a `DList` by appending it on the right by a `List α` to get another `List α`.  -/
Batteries.DList.apply : {α : Type u} → Batteries.DList α → List α → List α
-- Mathlib.Data.Finset.Basic
Equiv.sumPiEquivProdPi.eq_1 : ∀ {ι : Type u_10} {ι' : Type u_11} (π : ι ⊕ ι' → Type u_9),
  Equiv.sumPiEquivProdPi π =
    { toFun := fun f => (fun i => f (Sum.inl i), fun i' => f (Sum.inr i')), invFun := fun g t => Sum.rec g.1 g.2 t,
      left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.RingTheory.DividedPowerAlgebra.Init
_private.Mathlib.RingTheory.DividedPowerAlgebra.Init.0.DividedPowerAlgebra.lift'_imp : ∀ (R : Type u_2) (M : Type u_3) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {A : Type u_4}
  [inst_3 : CommSemiring A] [inst_4 : Algebra R A] {f : ℕ × M → A},
  (∀ (m : M), f (0, m) = 1) →
    (∀ (n : ℕ) (r : R) (m : M), f (n, r • m) = r ^ n • f (n, m)) →
      (∀ (n p : ℕ) (m : M), f (n, m) * f (p, m) = (n + p).choose n • f (n + p, m)) →
        (∀ (n : ℕ) (u v : M),
            f (n, u + v) =
              ∑ x ∈ Finset.HasAntidiagonal.antidiagonal n,
                match x with
                | (k, l) => f (k, u) * f (l, v)) →
          ∀ (p q : MvPolynomial (ℕ × M) R),
            DividedPowerAlgebra.Rel R M p q → (MvPolynomial.eval₂AlgHom R f) p = (MvPolynomial.eval₂AlgHom R f) q
-- Mathlib.Order.Hom.Basic
OrderEmbedding.coe_ofIsEmpty : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : IsEmpty α],
  ⇑OrderEmbedding.ofIsEmpty = fun a => isEmptyElim a
-- Mathlib.Algebra.GCDMonoid.Basic
gcd_mul_left' : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : GCDMonoid α] (a b c : α),
  Associated (gcd (a * b) (a * c)) (a * gcd b c)
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
SSet.prodStdSimplex.type₁_pairingCore : ∀ {m : ℕ} (k : Fin (m + 1)) {n : ℕ} (s : SSet.prodStdSimplex.pairingCore.Type₁ k n),
  (SSet.prodStdSimplex.pairingCore k n).type₁ s = s.x
-- Lean.Meta.CompletionName
Lean.Meta.completionBlackListExt : Lean.TagDeclarationExtension
-- Mathlib.RingTheory.Unramified.Field
Algebra.FormallyUnramified.of_isSeparable : ∀ (K : Type u_1) (L : Type u_3) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] [Algebra.IsSeparable K L],
  Algebra.FormallyUnramified K L
-- Mathlib.Order.Disjoint
IsCompl.mk : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : BoundedOrder α] {x y : α},
  Disjoint x y → Codisjoint x y → IsCompl x y
-- Mathlib.GroupTheory.GroupExtension.Defs
GroupExtension.Splitting.mk : {N : Type u_1} →
  {E : Type u_2} →
    {G : Type u_3} →
      [inst : Group N] →
        [inst_1 : Group E] →
          [inst_2 : Group G] →
            {S : GroupExtension N E G} →
              (toMonoidHom : G →* E) → Function.RightInverse (↑toMonoidHom).toFun ⇑S.rightHom → S.Splitting
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
SimplexCategoryGenRel.simplicialEvalσ_of_isAdmissible : ∀ (L : List ℕ) (m₁ m₂ : ℕ),
  SimplexCategoryGenRel.IsAdmissible m₂ L →
    ∀ (hk : m₂ + L.length = m₁) (j : ℕ) (hj : j < m₁ + 1),
      ↑((SimplexCategory.Hom.toOrderHom
              (SimplexCategoryGenRel.toSimplexCategory.map (SimplexCategoryGenRel.standardσ L hk)))
            ⟨j, hj⟩) =
        SimplexCategoryGenRel.simplicialEvalσ L j
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
NonUnitalContinuousFunctionalCalculus.congr_simp : ∀ (R : Type u_1) (A : Type u_2) (p p_1 : A → Prop),
  p = p_1 →
    ∀ [inst : CommSemiring R] [inst_1 : Nontrivial R] [inst_2 : StarRing R] [inst_3 : MetricSpace R]
      [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R] [inst_6 : NonUnitalRing A] [inst_7 : StarRing A]
      [inst_8 : TopologicalSpace A] [inst_9 : Module R A] [inst_10 : IsScalarTower R A A]
      [inst_11 : SMulCommClass R A A],
      NonUnitalContinuousFunctionalCalculus R A p = NonUnitalContinuousFunctionalCalculus R A p_1
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.map_mk_ofList : ∀ {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [inst : MulOneClass M] [inst_1 : MulOneClass N]
  [inst_2 : MulOneClass M'] [inst_3 : MulOneClass N'] (f : M →* M') (g : N →* N') (l : List (M ⊕ N)),
  (Monoid.Coprod.map f g) (Monoid.Coprod.mk (FreeMonoid.ofList l)) =
    Monoid.Coprod.mk (FreeMonoid.ofList (List.map (Sum.map ⇑f ⇑g) l))
-- Init.Data.List.Attach
/-- Maps a list of terms in a subtype to the corresponding terms in the type by forgetting that they
satisfy the predicate.

This is the inverse of `List.attachWith` and a synonym for `l.map (·.val)`.

Mostly this should not be needed by users. It is introduced as an intermediate step by lemmas such
as `map_subtype`, and is ideally subsequently simplified away by `unattach_attach`.

This function is usually inserted automatically by Lean as an intermediate step while proving
termination. It is rarely used explicitly in code. It is introduced as an intermediate step during
the elaboration of definitions by [well-founded
recursion](https://lean-lang.org/doc/reference/4.33.0/find/?domain=Verso.Genre.Manual.section&name=well-founded-recursion). If this function is encountered in a proof
state, the right approach is usually the tactic `simp [List.unattach, -List.map_subtype]`.
 -/
List.unattach : {α : Type u_1} → {p : α → Prop} → List { x // p x } → List α
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.restrict_neg : ∀ {α : Type u_1} {mα : MeasurableSpace α} {M : Type u_4} [inst : AddCommGroup M] [inst_1 : TopologicalSpace M]
  [inst_2 : IsTopologicalAddGroup M] (v : MeasureTheory.VectorMeasure α M) (i : Set α), (-v).restrict i = -v.restrict i
-- Mathlib.Order.InitialSeg
wellFounded_iff_principalSeg : ∀ {β : Type u} {s : β → β → Prop} [IsTrans β s],
  WellFounded s ↔ ∀ (α : Type u) (r : α → α → Prop) (x : PrincipalSeg r s), WellFounded r
-- Mathlib.SetTheory.Cardinal.Aleph
/-- The `aleph` function gives the infinite cardinals listed by their ordinal index. `aleph 0 = ℵ₀`,
`aleph 1 = succ ℵ₀` is the first uncountable cardinal, and so on.

For a version including finite cardinals, see `Cardinal.preAleph`. 

Conventions for notations in identifiers:

 * The recommended spelling of `ℵ_` in identifiers is `aleph`. -/
Cardinal.aleph : Ordinal.{u_1} ↪o Cardinal.{u_1}
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.Key.other : Lean.Meta.LazyDiscrTree.Key
-- Mathlib.Analysis.Convex.Basic
convex_halfSpace_ge : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] [inst_4 : AddCommMonoid β] [inst_5 : PartialOrder β] [IsOrderedAddMonoid β]
  [inst_7 : Module 𝕜 β] [PosSMulMono 𝕜 β] {f : E → β}, IsLinearMap 𝕜 f → ∀ (r : β), Convex 𝕜 {w | r ≤ f w}
-- Lean.ResolveName
Lean.getRevAliases : Lean.Environment → Lean.Name → List Lean.Name
-- Init.Prelude
Lean.Syntax.SepArray.mk : {sep : String} → Array Lean.Syntax → Lean.Syntax.SepArray sep
-- Mathlib.Tactic.Linarith.Oracle.FourierMotzkin
/-- `mkLinarithData hyps vars` takes a list of hypotheses and the largest variable present in
those hypotheses. It produces an initial state for the elimination monad.
 -/
Mathlib.Tactic.Linarith.mkLinarithData : List Mathlib.Tactic.Linarith.Comp → ℕ → Mathlib.Tactic.Linarith.LinarithData
-- Mathlib.Order.Types.Arithmetic
OrderType.card_mono : ∀ {o₁ o₂ : OrderType.{u_1}}, o₁ ≤ o₂ → o₁.card ≤ o₂.card