mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Enriched.EnrichedCat
/-- Construct a bundled `EnrichedCat` from the underlying type and the typeclass.  -/
CategoryTheory.EnrichedCat.of : (V : Type v) →
  [inst : CategoryTheory.Category.{w, v} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      (C : Type u) → [CategoryTheory.EnrichedCategory V C] → CategoryTheory.EnrichedCat V
-- Mathlib.NumberTheory.ArithmeticFunction.Zeta
ArithmeticFunction.ppow_apply : ∀ {R : Type u_1} [inst : Semiring R] {f : ArithmeticFunction R} {k x : ℕ}, 0 < k → (f.ppow k) x = f x ^ k
-- Mathlib.Topology.Algebra.Algebra
ContinuousAlgHom.coe_restrictScalars' : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_3} [inst_1 : CommSemiring S] [inst_2 : Algebra R S] {B : Type u_4}
  [inst_3 : Ring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R B] [inst_6 : Algebra S B]
  [inst_7 : IsScalarTower R S B] {C : Type u_5} [inst_8 : Ring C] [inst_9 : TopologicalSpace C] [inst_10 : Algebra R C]
  [inst_11 : Algebra S C] [inst_12 : IsScalarTower R S C] (f : B →A[S] C), ⇑(ContinuousAlgHom.restrictScalars R f) = ⇑f
-- Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
Submonoid.copy.congr_simp : ∀ {M : Type u_1} [inst : MulOneClass M] (S S_1 : Submonoid M) (e_S : S = S_1) (s s_1 : Set M) (e_s : s = s_1)
  (hs : s = ↑S), S.copy s hs = S_1.copy s_1 ⋯
-- Mathlib.Data.Sum.Interval
Finset.sumLexLift_eq_empty : ∀ {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} {γ₁ : Type u_5} {γ₂ : Type u_6}
  {f₁ : α₁ → β₁ → Finset γ₁} {f₂ : α₂ → β₂ → Finset γ₂} {g₁ : α₁ → β₂ → Finset γ₁} {g₂ : α₁ → β₂ → Finset γ₂}
  {a : α₁ ⊕ α₂} {b : β₁ ⊕ β₂},
  Finset.sumLexLift f₁ f₂ g₁ g₂ a b = ∅ ↔
    (∀ (a₁ : α₁) (b₁ : β₁), a = Sum.inl a₁ → b = Sum.inl b₁ → f₁ a₁ b₁ = ∅) ∧
      (∀ (a₁ : α₁) (b₂ : β₂), a = Sum.inl a₁ → b = Sum.inr b₂ → g₁ a₁ b₂ = ∅ ∧ g₂ a₁ b₂ = ∅) ∧
        ∀ (a₂ : α₂) (b₂ : β₂), a = Sum.inr a₂ → b = Sum.inr b₂ → f₂ a₂ b₂ = ∅
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.Zip
_private.Std.Data.Iterators.Lemmas.Combinators.Monadic.Zip.0.Std.Iterators.Types.Zip.instIterator.match_3.eq_1 : ∀ {m : Type u_1 → Type u_2} {α₁ β₁ : Type u_1} [inst : Std.Iterator α₁ m β₁] {α₂ β₂ : Type u_1}
  [inst_1 : Std.Iterator α₂ m β₂] (it : Std.IterM m (β₁ × β₂)) (motive : it.internalState.right.Step → Sort u_3)
  (it₂' : Std.IterM m β₂) (out₂ : β₂) (hp : it.internalState.right.IsPlausibleStep (Std.IterStep.yield it₂' out₂))
  (h_1 :
    (it₂' : Std.IterM m β₂) →
      (out₂ : β₂) →
        (hp : it.internalState.right.IsPlausibleStep (Std.IterStep.yield it₂' out₂)) →
          motive ⟨Std.IterStep.yield it₂' out₂, hp⟩)
  (h_2 :
    (it₂' : Std.IterM m β₂) →
      (hp : it.internalState.right.IsPlausibleStep (Std.IterStep.skip it₂')) → motive ⟨Std.IterStep.skip it₂', hp⟩)
  (h_3 : (hp : it.internalState.right.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, hp⟩),
  (match ⟨Std.IterStep.yield it₂' out₂, hp⟩ with
    | ⟨Std.IterStep.yield it₂' out₂, hp⟩ => h_1 it₂' out₂ hp
    | ⟨Std.IterStep.skip it₂', hp⟩ => h_2 it₂' hp
    | ⟨Std.IterStep.done, hp⟩ => h_3 hp) =
    h_1 it₂' out₂ hp
-- Mathlib.NumberTheory.DirichletCharacter.GaussSum
/-- If `χ` is primitive, but `e` is not, then `gaussSum χ e = 0`.  -/
gaussSum_eq_zero_of_isPrimitive_of_not_isPrimitive : ∀ {N : ℕ} [inst : NeZero N] {R : Type u_1} [inst_1 : CommRing R] (e : AddChar (ZMod N) R) [IsDomain R]
  {χ : DirichletCharacter R N}, χ.IsPrimitive → ¬e.IsPrimitive → gaussSum χ e = 0
-- Mathlib.Logic.Equiv.Defs
/-- The sort of maps from `PUnit` is equivalent to the codomain.  -/
Equiv.punitArrowEquiv : (α : Sort u_1) → (PUnit.{u} → α) ≃ α
-- Mathlib.Algebra.Module.Submodule.Ker
LinearMap.ker_restrict : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  {p : Submodule R M} {q : Submodule R₂ M₂} {f : M →ₛₗ[τ₁₂] M₂} (hf : ∀ x ∈ p, f x ∈ q),
  (f.restrict hf).ker = Submodule.comap p.subtype f.ker
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
LinearOrderedCommMonoidWithZero.toOrderBot : {α : Type u_3} → [self : LinearOrderedCommMonoidWithZero α] → OrderBot α
-- Std.Data.ExtTreeMap.Basic
/-- Creates a new empty tree map. It is also possible and recommended to
use the empty collection notations `∅` and `{}` to create an empty tree map. `simp` replaces
`empty` with `∅`.
 -/
Std.ExtTreeMap.empty : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.ExtTreeMap α β cmp
-- Mathlib.LinearAlgebra.QuadraticForm.TensorProduct
/-- If two quadratic maps from `A ⊗[R] M₂` agree on elements of the form `1 ⊗ m`, they are equal.

In other words, if a base change exists for a quadratic map, it is unique.

Note that unlike `QuadraticForm.baseChange`, this does not need `Invertible (2 : R)`.  -/
baseChange_ext : ∀ {R : Type uR} {A : Type uA} {M₂ : Type uM₂} {N₁ : Type uN₁} [inst : CommRing R] [inst_1 : CommRing A]
  [inst_2 : AddCommGroup M₂] [inst_3 : AddCommGroup N₁] [inst_4 : Algebra R A] [inst_5 : Module R N₁]
  [inst_6 : Module A N₁] [IsScalarTower R A N₁] [inst_8 : Module R M₂]
  ⦃Q₁ Q₂ : QuadraticMap A (TensorProduct R A M₂) N₁⦄, (∀ (m : M₂), Q₁ (1 ⊗ₜ[R] m) = Q₂ (1 ⊗ₜ[R] m)) → Q₁ = Q₂
-- Mathlib.Probability.IdentDistrib
ProbabilityTheory.IdentDistrib.aestronglyMeasurable_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  [inst_2 : MeasurableSpace γ] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} {f : α → γ} {g : β → γ}
  [inst_3 : TopologicalSpace γ] [TopologicalSpace.PseudoMetrizableSpace γ] [BorelSpace γ],
  ProbabilityTheory.IdentDistrib f g μ ν →
    (MeasureTheory.AEStronglyMeasurable f μ ↔ MeasureTheory.AEStronglyMeasurable g ν)
-- Mathlib.Algebra.Order.GroupWithZero.Finset
Finset.mul₀_sup' : ∀ {ι : Type u_1} {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : SemilatticeSup G₀] {a : G₀} [PosMulReflectLT G₀],
  0 ≤ a → ∀ (f : ι → G₀) (s : Finset ι) (hs : s.Nonempty), a * s.sup' hs f = s.sup' hs fun i => a * f i
-- Mathlib.Analysis.Complex.UpperHalfPlane.Measure
UpperHalfPlane.instIsFiniteMeasureOnCompactsVolume : MeasureTheory.IsFiniteMeasureOnCompacts MeasureTheory.volume
-- Mathlib.Algebra.GCDMonoid.Nat
Int.lcm_nonneg : ∀ (i j : ℤ), 0 ≤ lcm i j
-- Mathlib.CategoryTheory.Localization.Predicate
/-- uniqueness of the lifted functor  -/
CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.uniq : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {L : CategoryTheory.Functor C D}
  {W : CategoryTheory.MorphismProperty C} {E : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  (self : CategoryTheory.Localization.StrictUniversalPropertyFixedTarget L W E) (F₁ F₂ : CategoryTheory.Functor D E),
  L.comp F₁ = L.comp F₂ → F₁ = F₂
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.topEquiv_apply : ∀ {M : Type u_5} [inst : MulOneClass M] (x : ↥⊤), Submonoid.topEquiv x = ↑x
-- Mathlib.AlgebraicGeometry.Stalk
/-- The morphism from `Spec(O_x)` to `X` given by `IsAffineOpen.fromSpec` does not depend on the affine
open neighborhood of `x` we choose.
 -/
AlgebraicGeometry.IsAffineOpen.fromSpecStalk_eq : ∀ {X : AlgebraicGeometry.Scheme} {U V : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U)
  (hV : AlgebraicGeometry.IsAffineOpen V) (x : ↥X) (hxU : x ∈ U) (hxV : x ∈ V),
  hU.fromSpecStalk hxU = hV.fromSpecStalk hxV
-- Mathlib.Combinatorics.Matroid.Circuit
Matroid.IsCircuit.finite : ∀ {α : Type u_1} {M : Matroid α} {C : Set α} [M.Finitary], M.IsCircuit C → C.Finite
-- Mathlib.Algebra.DirectSum.Ring
DirectSum.ringHom_ext'_iff : ∀ {ι : Type u_1} [inst : DecidableEq ι] {A : ι → Type u_2} {R : Type u_3} [inst_1 : (i : ι) → AddCommMonoid (A i)]
  [inst_2 : AddMonoid ι] [inst_3 : DirectSum.GSemiring A] [inst_4 : Semiring R]
  {F G : (DirectSum ι fun i => A i) →+* R},
  F = G ↔ ∀ (i : ι), (↑F).comp (DirectSum.of A i) = (↑G).comp (DirectSum.of A i)
-- Init.Data.Slice.Array.Lemmas
Subarray.forIn_toArray : ∀ {α : Type u} {s : Subarray α} {m : Type v → Type w} [inst : Monad m] [LawfulMonad m] {γ : Type v} {init : γ}
  {f : α → γ → m (ForInStep γ)}, forIn (Std.Slice.toArray s) init f = forIn s init f
-- Init.Core
DoResultSBC.continue.injEq : ∀ {α σ : Type u} (a a_1 : σ), (DoResultSBC.continue a = DoResultSBC.continue a_1) = (a = a_1)
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
/-- The isomorphism of functors between
`((F ⊠ G) ⊠ H ⟶ (tensor C).prod (𝟭 C) ⋙ tensor C ⋙ -)` and
`(F ⊠ G ⊠ H ⟶ (𝟭 C).prod (tensor C) ⋙ tensor C ⋙ -)` that corresponds to the associator
isomorphism for Day convolution through `corepresentableBy₂` and `corepresentableBy₂`.  -/
CategoryTheory.MonoidalCategory.DayConvolution.associatorCorepresentingIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {V : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} V] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          [inst_3 : CategoryTheory.MonoidalCategory V] →
            (F G H : CategoryTheory.Functor C V) →
              ((CategoryTheory.Functor.whiskeringLeft (C × C) C V).obj (CategoryTheory.MonoidalCategory.tensor C)).comp
                  (((CategoryTheory.Functor.whiskeringLeft ((C × C) × C) (C × C) V).obj
                        ((CategoryTheory.MonoidalCategory.tensor C).prod (CategoryTheory.Functor.id C))).comp
                    (CategoryTheory.coyoneda.obj
                      (Opposite.op
                        (CategoryTheory.MonoidalCategory.externalProduct
                          (CategoryTheory.MonoidalCategory.externalProduct F G) H)))) ≅
                ((CategoryTheory.Functor.whiskeringLeft (C × C) C V).obj
                      (CategoryTheory.MonoidalCategory.tensor C)).comp
                  (((CategoryTheory.Functor.whiskeringLeft (C × C × C) (C × C) V).obj
                        ((CategoryTheory.Functor.id C).prod (CategoryTheory.MonoidalCategory.tensor C))).comp
                    (CategoryTheory.coyoneda.obj
                      (Opposite.op
                        (CategoryTheory.MonoidalCategory.externalProduct F
                          (CategoryTheory.MonoidalCategory.externalProduct G H)))))
-- Mathlib.Data.ENat.Basic
/-- **Alias** of `ENat.succ_natCast`. -/
ENat.succ_coe : ∀ (n : ℕ), SuccOrder.succ ↑n = ↑(n + 1)
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rco.size_toArray : ∀ {α : Type u} {r : Std.Rco α} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.Rxo.HasSize α] [inst_4 : Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α]
  [inst_6 : Std.Rxo.IsAlwaysFinite α] [Std.Rxo.LawfulHasSize α], r.toArray.size = r.size
-- Mathlib.GroupTheory.Abelianization.Defs
/-- `of` is the canonical projection from G to its abelianization.  -/
Abelianization.of : {G : Type u} → [inst : Group G] → G →* Abelianization G
-- Mathlib.RingTheory.Extension.Cotangent.Basis
/-- The canonical basis on `(g X - 1)/(g X - 1)²`.  -/
_private.Mathlib.RingTheory.Extension.Cotangent.Basis.0.Algebra.Generators.PresentationOfFreeCotangent.Aux.basisRight : {R : Type u_1} →
  {S : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          {ι : Type u_4} →
            {P : Algebra.Generators R S ι} →
              {σ : Type u_5} →
                {b : Module.Basis σ S P.toExtension.Cotangent} →
                  (D : Algebra.Generators.PresentationOfFreeCotangent.Aux✝ P b) →
                    Module.Basis Unit S
                      (Algebra.Generators.PresentationOfFreeCotangent.Aux.presRight✝ D).toExtension.Cotangent
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get?_filterMap : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} {γ : α → Type w}
  [inst : LawfulBEq α] {f : (a : α) → β a → Option (γ a)} {k : α},
  (Std.DHashMap.filterMap f m).get? k = (m.get? k).bind (f k)
-- Mathlib.Data.W.Basic
/-- The canonical bijection with the sigma type, showing that `WType` is a fixed point of
the polynomial functor `X ↦ Σ a : α, β a → X`.  -/
WType.equivSigma : {α : Type u_1} → (β : α → Type u_2) → WType β ≃ (a : α) × (β a → WType β)
-- Mathlib.Combinatorics.Additive.ApproximateSubgroup
IsApproximateAddSubgroup.zero_mem : ∀ {G : Type u_2} [inst : AddGroup G] {K : ℝ} {A : Set G}, IsApproximateAddSubgroup K A → 0 ∈ A
-- Mathlib.Algebra.GroupWithZero.Action.Hom
AddMonoidHom.instIsScalarTower : ∀ {M : Type u_1} {N : Type u_2} {A : Type u_3} {B : Type u_4} [inst : AddZeroClass A] [inst_1 : AddZeroClass B]
  [inst_2 : SMul M N] [inst_3 : DistribSMul M B] [inst_4 : DistribSMul N B] [IsScalarTower M N B],
  IsScalarTower M N (A →+ B)
-- Mathlib.RingTheory.MvPowerSeries.Substitution
MvPowerSeries.truncTotal_subst_eq_truncTotal_subst_truncTotal_of_le : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] {τ : Type u_4} {S : Type u_5} [inst_1 : CommRing S]
  [inst_2 : Algebra R S] {a : σ → MvPowerSeries τ S} {f : MvPowerSeries σ R} [inst_3 : Finite τ] {x : σ → ℕ} {k : ℕ},
  MvPowerSeries.HasSubst a →
    (∀ (i : σ), k ≤ x i) →
      (MvPowerSeries.truncTotal k) (MvPowerSeries.subst a f) =
        (MvPowerSeries.truncTotal k) (MvPowerSeries.subst (fun i => ↑((MvPowerSeries.truncTotal (x i)) (a i))) f)
-- Init.Data.SInt.Basic
instMulInt16 : Mul Int16
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenAddSubgroup.isOpen : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] (U : OpenAddSubgroup G), IsOpen ↑U
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.image_neg_eq_neg : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Neg α] (s : Finset α), Finset.image (fun x => -x) s = -s
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.isSome_maxKey?_of_isSome_maxKey?_erase : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  (t.erase k).maxKey?.isSome = true → t.maxKey?.isSome = true
-- Mathlib.Order.Monotone.Defs
antitone_lam : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder γ] {f : α → β → γ},
  (∀ (b : β), Antitone fun a => f a b) → Antitone f
-- Mathlib.Combinatorics.SimpleGraph.Maps
/-- Induced graphs embed in the original graph.

Note that if `G.induce s = ⊤` (i.e., if `s` is a clique) then this gives the embedding of a
complete graph.  -/
SimpleGraph.Embedding.induce : {V : Type u_1} → {G : SimpleGraph V} → (s : Set V) → SimpleGraph.induce s G ↪g G
-- Mathlib.Order.UpperLower.CompleteLattice
UpperSet.coe_sup : ∀ {α : Type u_1} [inst : LE α] (s t : UpperSet α), ↑(s ⊔ t) = ↑s ∩ ↑t
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
AlgebraicGeometry.LocallyRingedSpace.comp_base : ∀ {X Y Z : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Y) (g : Y ⟶ Z),
  (CategoryTheory.CategoryStruct.comp f g).base = CategoryTheory.CategoryStruct.comp f.base g.base
-- Mathlib.Analysis.InnerProductSpace.Calculus
contDiffAt_inner : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : NormedSpace ℝ E] {p : E × E} {n : WithTop ℕ∞}, ContDiffAt ℝ n (fun p => inner 𝕜 p.1 p.2) p
-- Lean.Data.Lsp.Extra
Lean.Lsp.LeanModule.data? : Lean.Lsp.LeanModule → Option Lean.Json
-- Mathlib.MeasureTheory.Function.LpSpace.Complete
MeasureTheory.Lp.tendsto_Lp_iff_tendsto_eLpNorm'' : ∀ {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {E : Type u_3}
  [inst : NormedAddCommGroup E] {ι : Type u_4} {fi : Filter ι} [inst_1 : Fact (1 ≤ p)] (f : ι → α → E)
  (f_ℒp : ∀ (n : ι), MeasureTheory.MemLp (f n) p μ) (f_lim : α → E) (f_lim_ℒp : MeasureTheory.MemLp f_lim p μ),
  Filter.Tendsto (fun n => MeasureTheory.MemLp.toLp (f n) ⋯) fi (nhds (MeasureTheory.MemLp.toLp f_lim f_lim_ℒp)) ↔
    Filter.Tendsto (fun n => MeasureTheory.eLpNorm (f n - f_lim) p μ) fi (nhds 0)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Over
CategoryTheory.Over.whiskerLeft_left_snd : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {X : C}
  {R S T : CategoryTheory.Over X} (f : S ⟶ T),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.Hom.left (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R f))
      (CategoryTheory.Limits.pullback.snd R.hom T.hom) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd R.hom S.hom) (CategoryTheory.Over.Hom.left f)
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.mk_X : ∀ {R : Type u_1} [inst : CommRing R] {f : Polynomial R}, (AdjoinRoot.mk f) Polynomial.X = AdjoinRoot.root f
-- Mathlib.GroupTheory.Coset.Basic
/-- If `s ≤ t`, then there is a map `H ⧸ s.addSubgroupOf H → H ⧸ t.addSubgroupOf H`.  -/
AddSubgroup.quotientAddSubgroupOfMapOfLE : {α : Type u_1} →
  [inst : AddGroup α] →
    {s t : AddSubgroup α} → (H : AddSubgroup α) → s ≤ t → ↥H ⧸ s.addSubgroupOf H → ↥H ⧸ t.addSubgroupOf H
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Real.ball_zero_eq_Ioo : ∀ (r : ℝ), Metric.ball 0 r = Set.Ioo (-r) r
-- Mathlib.Topology.UniformSpace.Dini
/-- **Dini's theorem**: if `F n` is a monotone decreasing collection of continuous functions
converging pointwise to a continuous function `f`, then `F n` converges to `f` in the
compact-open topology.  -/
ContinuousMap.tendsto_of_antitone_of_pointwise : ∀ {ι : Type u_1} {α : Type u_2} {G : Type u_3} [inst : Preorder ι] [inst_1 : TopologicalSpace α]
  [inst_2 : NormedAddCommGroup G] [inst_3 : Lattice G] [HasSolidNorm G] [IsOrderedAddMonoid G] {F : ι → C(α, G)}
  {f : C(α, G)},
  Antitone F →
    (∀ (x : α), Filter.Tendsto (fun x_1 => (F x_1) x) Filter.atTop (nhds (f x))) →
      Filter.Tendsto F Filter.atTop (nhds f)
-- Mathlib.Topology.Constructions
isClosedMap_toMul : ∀ {X : Type u} [inst : TopologicalSpace X], IsClosedMap ⇑Additive.toMul
-- Mathlib.RingTheory.Bialgebra.Equiv
BialgEquiv.toEquiv_symm : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B]
  (e : A ≃ₐc[R] B), e.symm.toEquiv = e.toEquiv.symm
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.add_toLinearMap : ∀ {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 + g).toLinearMap = f.toLinearMap + g.toLinearMap
-- Mathlib.CategoryTheory.Limits.Preserves.Filtered
CategoryTheory.Limits.ReflectsColimits.reflectsFilteredColimits : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.ReflectsColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F],
  CategoryTheory.Limits.ReflectsFilteredColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F
-- Mathlib.Order.Minimal
OrderEmbedding.minimal_mem_image : ∀ {α : Type u_2} {β : Type u_3} {x : α} [inst : Preorder α] [inst_1 : Preorder β] {s : Set α} (f : α ↪o β),
  Minimal (fun x => x ∈ s) x → Minimal (fun x => x ∈ ⇑f '' s) (f x)
-- Mathlib.AlgebraicGeometry.Pullbacks
/-- Given an open cover `{ Yᵢ }` of `Y`, then `X ×[Z] Y` is covered by `X ×[Z] Yᵢ`.  -/
AlgebraicGeometry.Scheme.Pullback.openCoverOfRight : {X Y Z : AlgebraicGeometry.Scheme} →
  Y.OpenCover → (f : X ⟶ Z) → (g : Y ⟶ Z) → (CategoryTheory.Limits.pullback f g).OpenCover
-- Mathlib.CategoryTheory.Abelian.Pseudoelements
/-- A coercion from an object of an abelian category to its pseudoelements.  -/
CategoryTheory.Abelian.Pseudoelement.objectToSort : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.Abelian C] → CoeSort C (Type (max u v))
-- Mathlib.LinearAlgebra.Matrix.SemiringInverse
/-- The adjugate matrix, but only the terms of a given sign.  -/
Matrix.adjp : {n : Type u_1} → {R : Type u_3} → [Fintype n] → [DecidableEq n] → [CommSemiring R] → ℤˣ → Matrix n n R → Matrix n n R
-- Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Fin.invAccumulate.eq_1 : ∀ (n m : ℕ) (s : Fin m → ℕ) (i : Fin n),
  Fin.invAccumulate n m s i = (if hi : ↑i < m then s ⟨↑i, hi⟩ else 0) - if hi : ↑i + 1 < m then s ⟨↑i + 1, hi⟩ else 0
-- Mathlib.FieldTheory.SeparablyGenerated
MvPolynomial.exists_mem_support_not_dvd_of_forall_totalDegree_le : ∀ {k : Type u_1} {K : Type u_2} {ι : Type u_3} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K] (p : ℕ),
  Nat.Prime p →
    (∀ (s : Finset K), LinearIndepOn k id ↑s → LinearIndepOn k (fun x => x ^ p) ↑s) →
      ∀ {a : ι → K} {F : MvPolynomial ι k},
        (∀ (F' : MvPolynomial ι k), F' ≠ 0 → (MvPolynomial.aeval a) F' = 0 → F.totalDegree ≤ F'.totalDegree) →
          F ≠ 0 → (MvPolynomial.aeval a) F = 0 → ∃ i, ∃ σ ∈ F.support, ¬p ∣ σ i
-- Std.Data.DTreeMap.Raw.Basic
/-- Tries to retrieve the largest key that is less than the given key,
panicking if no such key exists.
 -/
Std.DTreeMap.Raw.getKeyLT! : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → [Inhabited α] → Std.DTreeMap.Raw α β cmp → α → α
-- Mathlib.CategoryTheory.Abelian.Pseudoelements
CategoryTheory.Abelian.Pseudoelement.over_coe_def : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {P Q : C} (a : Q ⟶ P),
  Quot.mk (CategoryTheory.Abelian.PseudoEqual P) (CategoryTheory.Over.mk a) = ⟦CategoryTheory.Over.mk a⟧
-- Mathlib.LinearAlgebra.Prod
LinearMap.prodMap_id : ∀ {R : Type u} {M : Type v} {M₂ : Type w} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂], LinearMap.id.prodMap LinearMap.id = LinearMap.id
-- Init.Data.List.ToArray
Array.getLast!_toList : ∀ {α : Type u_1} [inst : Inhabited α] (xs : Array α), xs.toList.getLast! = xs.back!
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.FriendlyOperationClass.FriendlyOperation : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis} {γ : Type u_1}
  {op :
    γ →
      Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl →
        Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl}
  [h : Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.FriendlyOperationClass op] (c : γ),
  Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.FriendlyOperation (op c)
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.isClosed_closedCell : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : Topology.RelCWComplex C D] [T2Space X] {n : ℕ}
  {i : Topology.RelCWComplex.cell C n}, IsClosed (Topology.RelCWComplex.closedCell n i)
-- Mathlib.GroupTheory.Complement
Subgroup.IsComplement.leftCosetEquivalence_equiv_fst : ∀ {G : Type u_1} [inst : Group G] {K : Subgroup G} {S : Set G} (hSK : Subgroup.IsComplement S ↑K) (g : G),
  LeftCosetEquivalence (↑K) g ↑(hSK.equiv g).1
-- Mathlib.Topology.EMetricSpace.Pi
edist_pi_const_le : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : Fintype β] (a b : α),
  (edist (fun x => a) fun x => b) ≤ edist a b
-- Mathlib.Algebra.GCDMonoid.Basic
/-- Define `GCDMonoid` on a structure just from the `gcd` and its properties.  -/
gcdMonoidOfGCD : {α : Type u_1} →
  [inst : CommMonoidWithZero α] →
    [IsCancelMulZero α] →
      [DecidableEq α] →
        (gcd : α → α → α) →
          (∀ (a b : α), gcd a b ∣ a) →
            (∀ (a b : α), gcd a b ∣ b) → (∀ {a b c : α}, a ∣ c → a ∣ b → a ∣ gcd c b) → GCDMonoid α
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
/-- If the `vectorSpan` of a finite subset of an affinely independent
family lies in a submodule with dimension one less than its
cardinality, it equals that submodule.  -/
AffineIndependent.vectorSpan_image_finset_eq_of_le_of_card_eq_finrank_add_one : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} {ι : Type u_4} [inst : DivisionRing k] [inst_1 : AddCommGroup V]
  [inst_2 : Module k V] [inst_3 : AddTorsor V P] [inst_4 : DecidableEq P] {p : ι → P},
  AffineIndependent k p →
    ∀ {s : Finset ι} {sm : Submodule k V} [FiniteDimensional k ↥sm],
      vectorSpan k ↑(Finset.image p s) ≤ sm → s.card = Module.finrank k ↥sm + 1 → vectorSpan k ↑(Finset.image p s) = sm