mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Server.Requests
Lean.Server.RequestHandlerCompleteness.partial.inj : ∀ {refreshMethod : String} {refreshIntervalMs : ℕ} {refreshMethod_1 : String} {refreshIntervalMs_1 : ℕ},
  Lean.Server.RequestHandlerCompleteness.partial refreshMethod refreshIntervalMs =
      Lean.Server.RequestHandlerCompleteness.partial refreshMethod_1 refreshIntervalMs_1 →
    refreshMethod = refreshMethod_1 ∧ refreshIntervalMs = refreshIntervalMs_1
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
IsSelfAdjoint.coe_mem_spectrum_complex : ∀ {A : Type u_2} [inst : TopologicalSpace A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : Algebra ℂ A]
  [ContinuousFunctionalCalculus ℂ A IsStarNormal] {a : A} {x : ℝ},
  autoParam (IsSelfAdjoint a) IsSelfAdjoint.coe_mem_spectrum_complex._auto_1 → (↑x ∈ spectrum ℂ a ↔ x ∈ spectrum ℝ a)
-- Mathlib.Algebra.Group.Defs
add_right_cancel_iff : ∀ {G : Type u_1} [inst : Add G] [IsRightCancelAdd G] {a b c : G}, b + a = c + a ↔ b = c
-- Mathlib.Algebra.GroupWithZero.Defs
mul_self_eq_zero : ∀ {M₀ : Type u_1} [inst : MulZeroClass M₀] [NoZeroDivisors M₀] {a : M₀}, a * a = 0 ↔ a = 0
-- Mathlib.CategoryTheory.Elements
CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalence_inverse : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor Cᵒᵖ (Type v)),
  (CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalence F).inverse =
    (CategoryTheory.CategoryOfElements.fromCostructuredArrow F).rightOp
-- Mathlib.AlgebraicGeometry.Fiber
AlgebraicGeometry.Scheme.Hom.asFiberHom_fiberι : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (x : ↥X),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.asFiberHom f x)
      (AlgebraicGeometry.Scheme.Hom.fiberι f (f x)) =
    X.fromSpecResidueField x
-- Init.Data.UInt.Lemmas
UInt64.ofNatClamp_finVal : ∀ (n : Fin UInt64.size), UInt64.ofNatClamp ↑n = UInt64.ofFin n
-- Mathlib.GroupTheory.OrderOfElement
isOfFinOrder_pow : ∀ {G : Type u_1} [inst : Monoid G] {a : G} {n : ℕ}, IsOfFinOrder (a ^ n) ↔ IsOfFinOrder a ∨ n = 0
-- Mathlib.Computability.TuringMachine.Tape
/-- Any two extensions by blank `l₁,l₂` of `l` have a common join (which can be taken to be the
longer of `l₁` and `l₂`).  -/
Turing.BlankExtends.above : {Γ : Type u_1} →
  [inst : Inhabited Γ] →
    {l l₁ l₂ : List Γ} →
      Turing.BlankExtends l l₁ →
        Turing.BlankExtends l l₂ → { l' // Turing.BlankExtends l₁ l' ∧ Turing.BlankExtends l₂ l' }
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalAlgHom.subtype_comp_codRestrict : ∀ {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] [inst_3 : NonUnitalNonAssocSemiring B] [inst_4 : Module R B] [inst_5 : FunLike F A B]
  [inst_6 : NonUnitalAlgHomClass F R A B] (f : F) (S : NonUnitalSubalgebra R B) (hf : ∀ (x : A), f x ∈ S),
  (NonUnitalSubalgebraClass.subtype S).comp (NonUnitalAlgHom.codRestrict f S hf) =
    NonUnitalAlgHomClass.toNonUnitalAlgHom f
-- Mathlib.LinearAlgebra.Ray
/-- A vector is in the same ray as a nonnegative multiple of one it is in the same ray as.  -/
SameRay.nonneg_smul_right : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] {x y : M} {S : Type u_5} [inst_5 : CommSemiring S]
  [inst_6 : PartialOrder S] [inst_7 : Algebra S R] [inst_8 : Module S M] [SMulPosMono S R] [IsScalarTower S R M]
  {a : S}, SameRay R x y → 0 ≤ a → SameRay R x (a • y)
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.eq_of_isIso : ∀ {n m : ℕ} (f : { len := n } ⟶ { len := m }) [CategoryTheory.IsIso f], n = m
-- Mathlib.LinearAlgebra.Basis.Flag
Module.Basis.flag_strictMono : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {n : ℕ}
  [Nontrivial R] (b : Module.Basis (Fin n) R M), StrictMono b.flag
-- Mathlib.RingTheory.AdjoinRoot
/-- An unwrapped version of `AdjoinRoot.free_of_monic` for better discoverability.  -/
Polynomial.Monic.free_quotient : ∀ {R : Type u_1} [inst : CommRing R] {g : Polynomial R}, g.Monic → Module.Free R (Polynomial R ⧸ Ideal.span {g})
-- Mathlib.Data.Rat.Defs
Rat.addCommMonoid : AddCommMonoid ℚ
-- Mathlib.Data.Vector.Defs
List.Vector.instGetElemNatLt : {α : Type u_1} → {n : ℕ} → GetElem (List.Vector α n) ℕ α fun x i => i < n
-- Mathlib.RingTheory.Smooth.NoetherianDescent
_private.Mathlib.RingTheory.Smooth.NoetherianDescent.0.Algebra.Smooth.DescentAux.mk.injEq : ∀ {A : Type u} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] (vars rels : Type)
  (P : Algebra.Presentation A B vars rels) (σ : B →ₐ[A] MvPolynomial vars A ⧸ P.ker ^ 2)
  (h : vars → MvPolynomial vars A) (p : rels → MvPolynomial rels (MvPolynomial vars A))
  (hphom : ∀ (j : rels), (p j).IsHomogeneous 2)
  (hp : ∀ (j : rels), (MvPolynomial.eval P.relation) (p j) = (MvPolynomial.aeval h) (P.relation j))
  (q : vars → MvPolynomial rels P.Ring) (hqhom : ∀ (i : vars), (q i).IsHomogeneous 1)
  (hq : ∀ (i : vars), (MvPolynomial.eval P.relation) (q i) = h i - MvPolynomial.X i) (vars_1 rels_1 : Type)
  (P_1 : Algebra.Presentation A B vars_1 rels_1) (σ_1 : B →ₐ[A] MvPolynomial vars_1 A ⧸ P_1.ker ^ 2)
  (h_1 : vars_1 → MvPolynomial vars_1 A) (p_1 : rels_1 → MvPolynomial rels_1 (MvPolynomial vars_1 A))
  (hphom_1 : ∀ (j : rels_1), (p_1 j).IsHomogeneous 2)
  (hp_1 : ∀ (j : rels_1), (MvPolynomial.eval P_1.relation) (p_1 j) = (MvPolynomial.aeval h_1) (P_1.relation j))
  (q_1 : vars_1 → MvPolynomial rels_1 P_1.Ring) (hqhom_1 : ∀ (i : vars_1), (q_1 i).IsHomogeneous 1)
  (hq_1 : ∀ (i : vars_1), (MvPolynomial.eval P_1.relation) (q_1 i) = h_1 i - MvPolynomial.X i),
  ({ vars := vars, rels := rels, P := P, σ := σ, h := h, p := p, hphom := hphom, hp := hp, q := q, hqhom := hqhom,
        hq := hq } =
      { vars := vars_1, rels := rels_1, P := P_1, σ := σ_1, h := h_1, p := p_1, hphom := hphom_1, hp := hp_1, q := q_1,
        hqhom := hqhom_1, hq := hq_1 }) =
    (vars = vars_1 ∧ rels = rels_1 ∧ P ≍ P_1 ∧ σ ≍ σ_1 ∧ h ≍ h_1 ∧ p ≍ p_1 ∧ q ≍ q_1)
-- Mathlib.Algebra.Module.ZLattice.Covolume
/-- Let `L₁` be a sub-`ℤ`-lattice of `L₂`. Then the index of `L₁` inside `L₂` is equal to
`covolume L₁ / covolume L₂`.
 -/
ZLattice.covolume_div_covolume_eq_relIndex : ∀ {ι : Type u_2} [inst : Fintype ι] (L₁ L₂ : Submodule ℤ (ι → ℝ)) [inst_1 : DiscreteTopology ↥L₁] [IsZLattice ℝ L₁]
  [inst_3 : DiscreteTopology ↥L₂] [IsZLattice ℝ L₂],
  L₁ ≤ L₂ →
    ZLattice.covolume L₁ MeasureTheory.volume / ZLattice.covolume L₂ MeasureTheory.volume =
      ↑(L₁.toAddSubgroup.relIndex L₂.toAddSubgroup)
-- Mathlib.Order.Filter.AtTopBot.Monoid
Filter.Tendsto.atTop_of_le_const_add : ∀ {α : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] [inst_1 : Preorder M] [IsOrderedCancelAddMonoid M]
  {l : Filter α} {f g : α → M},
  (∃ C, ∀ (x : α), f x ≤ C) → Filter.Tendsto (fun x => f x + g x) l Filter.atTop → Filter.Tendsto g l Filter.atTop
-- Init.Data.UInt.Lemmas
USize.eq_iff_toBitVec_eq : ∀ {a b : USize}, a = b ↔ a.toBitVec = b.toBitVec
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.minKeyD_insert_le_minKeyD : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF →
    t.isEmpty = false →
      ∀ {k : α} {v : β} {fallback : α}, (cmp ((t.insert k v).minKeyD fallback) (t.minKeyD fallback)).isLE = true
-- Lean.Meta.Tactic.ElimInfo
Lean.Meta.CustomEliminators.map : Lean.Meta.CustomEliminators → Lean.SMap (Bool × Array Lean.Name) Lean.Name
-- Mathlib.Order.Category.PartOrdEmb
PartOrdEmb.instReflectsIsomorphismsForgetOrderEmbeddingCarrier : (CategoryTheory.forget PartOrdEmb).ReflectsIsomorphisms
-- Mathlib.Analysis.Convex.FunctionTopology
/-- **Alias** of `isClosed_setOfPred_convexOn`.

---

The set of convex functions on a set `s` is closed.  -/
isClosed_setOf_convexOn : ∀ {𝕜 : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : PartialOrder β]
  [inst_3 : TopologicalSpace β] [OrderClosedTopology β] [inst_5 : AddCommMonoid α] [inst_6 : AddCommMonoid β]
  [inst_7 : SMul 𝕜 α] [inst_8 : SMul 𝕜 β] [ContinuousConstSMul 𝕜 β] [ContinuousAdd β] {s : Set α},
  IsClosed {f | ConvexOn 𝕜 s f}
-- Mathlib.Algebra.Order.Rearrangement
/-- **Strict inequality case of the Rearrangement Inequality**: Pointwise scalar multiplication of
`f` and `g`, which antivary together on `s`, is strictly decreased by a permutation if and only if
`f ∘ σ` and `g` do not antivary together on `s`. Stated by permuting the entries of `f`.  -/
AntivaryOn.sum_smul_lt_sum_comp_perm_smul_iff : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semiring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [ExistsAddOfLE α] [inst_4 : AddCommMonoid β] [inst_5 : LinearOrder β] [IsOrderedCancelAddMonoid β]
  [inst_7 : Module α β] [PosSMulStrictMono α β] {s : Finset ι} {σ : Equiv.Perm ι} {f : ι → α} {g : ι → β},
  AntivaryOn f g ↑s → {x | σ x ≠ x} ⊆ ↑s → (∑ i ∈ s, f i • g i < ∑ i ∈ s, f (σ i) • g i ↔ ¬AntivaryOn (f ∘ ⇑σ) g ↑s)
-- Mathlib.Data.Finsupp.Option
Finsupp.optionElim_ne_zero_iff : ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] (y : M) (f : α →₀ M), Finsupp.optionElim y f ≠ 0 ↔ f ≠ 0 ∨ y ≠ 0
-- Mathlib.RingTheory.PowerSeries.Substitution
PowerSeries.summable_subst : ∀ {R : Type u_2} [inst : CommRing R] {τ : Type u_3} {S : Type u_4} [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {x : ℕ → PowerSeries R} {a : MvPowerSeries τ S} [inst_3 : UniformSpace R] [DiscreteUniformity R]
  [inst_5 : UniformSpace S] [DiscreteUniformity S],
  Summable x → PowerSeries.HasSubst a → Summable fun i => PowerSeries.subst a (x i)
-- Mathlib.Topology.Category.TopCat.OpenNhds
/-- An inducing map `f : X ⟶ Y` induces an adjunction between `OpenNhds (f x)` and `OpenNhds x`.
 -/
Topology.IsInducing.adjunctionNhds : {X Y : TopCat} →
  {f : X ⟶ Y} →
    (h : Topology.IsInducing ⇑(CategoryTheory.ConcreteCategory.hom f)) →
      (x : ↑X) → TopologicalSpace.OpenNhds.map f x ⊣ h.functorNhds x
-- Init.Data.String.Search
String.Internal.posOfImpl : String → Char → String.Pos.Raw
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
HasProdLocallyUniformlyOn.tendstoLocallyUniformlyOn_finsetRange : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] {g : β → α} {s : Set β} [inst_1 : UniformSpace α]
  [inst_2 : TopologicalSpace β] {f : ℕ → β → α},
  HasProdLocallyUniformlyOn f g s → TendstoLocallyUniformlyOn (fun N b => ∏ i ∈ Finset.range N, f i b) g Filter.atTop s
-- Mathlib.Combinatorics.Graph.Simple
Graph.Adj.ne : ∀ {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} [G.Loopless], G.Adj u v → u ≠ v
-- Mathlib.CategoryTheory.FintypeCat
FintypeCat.id_apply : ∀ (X : FintypeCat) (x : X.obj), (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) x = x
-- Mathlib.CategoryTheory.SingleObj
MulEquiv.toSingleObjEquiv_unitIso_inv : ∀ {M : Type u} {N : Type v} [inst : Monoid M] [inst_1 : Monoid N] (e : M ≃* N),
  e.toSingleObjEquiv.unitIso.inv = CategoryTheory.eqToHom ⋯
-- Mathlib.Topology.Category.Profinite.AsLimit
/-- An abbreviation for `X.fintypeDiagram ⋙ FintypeCat.toProfinite`.  -/
Profinite.diagram : (X : Profinite) → CategoryTheory.Functor (DiscreteQuotient ↑X.toTop) Profinite
-- Mathlib.Data.Finite.Defs
/-- Constructor for `Set.Finite` using a `Finite` instance.  -/
Set.toFinite : ∀ {α : Type u} (s : Set α) [Finite ↑s], s.Finite
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.StronglyMeasurable.div' : ∀ {α : Type u_1} {β : Type u_2} {f g : α → β} {mα : MeasurableSpace α} [inst : TopologicalSpace β] [inst_1 : Div β]
  [ContinuousDiv β],
  MeasureTheory.StronglyMeasurable f → MeasureTheory.StronglyMeasurable g → MeasureTheory.StronglyMeasurable (f / g)
-- Mathlib.Data.PFunctor.Univariate.Basic
/-- The child family of types  -/
PFunctor.B : (self : PFunctor.{uA, uB}) → self.A → Type uB
-- Mathlib.Computability.Primrec.List
Primrec.vector_ofFn' : ∀ {α : Type u_1} [inst : Primcodable α] {n : ℕ}, Primrec List.Vector.ofFn
-- Mathlib.Data.List.Sigma
List.mem_dlookup : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a : α} {b : β a} {l : List (Sigma β)},
  l.NodupKeys → ⟨a, b⟩ ∈ l → b ∈ List.dlookup a l
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
cfcₙ_comp_norm : ∀ {𝕜 : Type u_1} {A : Type u_2} {p : A → Prop} [inst : RCLike 𝕜] [inst_1 : NonUnitalRing A]
  [inst_2 : TopologicalSpace A] [inst_3 : Module 𝕜 A] [inst_4 : StarRing A] [inst_5 : PartialOrder A]
  [inst_6 : StarOrderedRing A] [inst_7 : IsScalarTower 𝕜 A A] [inst_8 : SMulCommClass 𝕜 A A]
  [inst_9 : NonUnitalContinuousFunctionalCalculus 𝕜 A p] [inst_10 : Module ℝ A] [inst_11 : SMulCommClass ℝ A A]
  [inst_12 : IsScalarTower ℝ A A] [inst_13 : NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A]
  [inst_16 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] (f : 𝕜 → 𝕜) (a : A),
  autoParam (p a) cfcₙ_comp_norm._auto_1 →
    autoParam (ContinuousOn f ((fun z => ↑‖z‖) '' quasispectrum 𝕜 a)) cfcₙ_comp_norm._auto_3 →
      cfcₙ (fun x => f ↑‖x‖) a = cfcₙ f (CFC.abs a)
-- Mathlib.GroupTheory.GroupAction.Blocks
AddAction.IsTrivialBlock.vadd : ∀ {M : Type u_3} {α : Type u_4} [inst : AddGroup M] [inst_1 : AddAction M α] {B : Set α},
  AddAction.IsTrivialBlock B → ∀ (g : M), AddAction.IsTrivialBlock (g +ᵥ B)
-- Init.Data.List.MinMax
List.min_cons : ∀ {α : Type u_1} [inst : Min α] [Std.Associative min] {a : α} {l : List α} {h : a :: l ≠ []},
  (a :: l).min h = l.min?.elim a fun x => a ⊓ x
-- Mathlib.Algebra.Category.Ring.Basic
CommSemiRingCat.instCommSemiringObjForgetRingHomCarrier : {R : CommSemiRingCat} → CommSemiring ((CategoryTheory.forget CommSemiRingCat).obj R)
-- Init.Data.UInt.Bitwise
UInt64.or_eq_zero_iff : ∀ {a b : UInt64}, a ||| b = 0 ↔ a = 0 ∧ b = 0
-- Mathlib.Algebra.MvPolynomial.Equiv
/-- The algebra isomorphism between multivariable polynomials indexed by a type with a unique
element and polynomials over the ground ring.  -/
MvPolynomial.uniqueAlgEquiv : (R : Type u) → [inst : CommSemiring R] → (σ : Type u_2) → [Unique σ] → MvPolynomial σ R ≃ₐ[R] Polynomial R
-- Mathlib.RingTheory.Perfectoid.FontaineTheta
/-- The Fontaine's θ map from `𝕎 R♭` to `R`.
It is the limit of the ring maps `fontaineThetaModPPow n` from `𝕎 R♭` to `R/p^(n+1)`.
 -/
WittVector.fontaineTheta : (R : Type u) →
  [inst : CommRing R] →
    (p : ℕ) →
      [inst_1 : Fact (Nat.Prime p)] →
        [inst_2 : Fact ¬IsUnit ↑p] → [IsAdicComplete (Ideal.span {↑p}) R] → WittVector p (PreTilt R p) →+* R
-- Mathlib.Algebra.Group.Submonoid.Finsupp
Submonoid.mem_closure_iff_of_fintype : ∀ {M : Type u_1} [inst : CommMonoid M] {x : M} {s : Set M} [inst_1 : Fintype ↑s],
  x ∈ Submonoid.closure s ↔ ∃ a, x = ∏ i, ↑i ^ a i
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.le_comap_iSup : ∀ {ι : Sort u_1} {α : Type u_2} {β : Type u_3} [inst : BooleanAlgebra α] [inst_1 : BooleanAlgebra β]
  (f : BoundedLatticeHom α β) (L : ι → BooleanSubalgebra β),
  ⨆ i, BooleanSubalgebra.comap f (L i) ≤ BooleanSubalgebra.comap f (⨆ i, L i)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get?_filterMap : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {γ : Type w} {t : Std.DTreeMap.Internal.Impl α fun x => β}
  [inst : Std.TransOrd α] {f : α → β → Option γ} {k : α} (h : t.WF),
  Std.DTreeMap.Internal.Impl.Const.get? (Std.DTreeMap.Internal.Impl.filterMap f t ⋯).impl k =
    (Std.DTreeMap.Internal.Impl.Const.get? t k).pbind fun x h' => f (t.getKey k ⋯) x
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapId_inv_τr : ∀ (x : CategoryTheory.LocallyDiscrete AlgebraicGeometry.Schemeᵒᵖ),
  (AlgebraicGeometry.Scheme.Modules.pseudofunctor.mapId x).inv.τr =
    CategoryTheory.NatTrans.toCatHom₂ (AlgebraicGeometry.Scheme.Modules.pushforwardId (Opposite.unop x.as)).hom
-- Mathlib.LinearAlgebra.Quotient.Defs
Submodule.quotientRel_def : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (p : Submodule R M)
  {x y : M}, p.quotientRel x y ↔ x - y ∈ p
-- Mathlib.Algebra.DirectSum.Module
DirectSum.IsInternal.collectedBasis_repr_of_mem_ne : ∀ {R : Type u} [inst : Semiring R] {ι : Type v} [dec_ι : DecidableEq ι] {M : Type u_1} [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] {A : ι → Submodule R M} (h : DirectSum.IsInternal A) {α : ι → Type u_2}
  (v : (i : ι) → Module.Basis (α i) R ↥(A i)) {x : M} {i j : ι},
  i ≠ j → ∀ {a : α j}, x ∈ A i → ((h.collectedBasis v).repr x) ⟨j, a⟩ = 0
-- Mathlib.CategoryTheory.Localization.Pi
CategoryTheory.Functor.IsLocalization.pi : ∀ {J : Type w} [Finite J] {C : J → Type u₁} {D : J → Type u₂} [inst : (j : J) → CategoryTheory.Category.{v₁, u₁} (C j)]
  [inst_1 : (j : J) → CategoryTheory.Category.{v₂, u₂} (D j)] (L : (j : J) → CategoryTheory.Functor (C j) (D j))
  (W : (j : J) → CategoryTheory.MorphismProperty (C j)) [∀ (j : J), (W j).ContainsIdentities]
  [∀ (j : J), (L j).IsLocalization (W j)],
  (CategoryTheory.Functor.pi L).IsLocalization (CategoryTheory.MorphismProperty.pi W)
-- Mathlib.GroupTheory.OreLocalization.OreSet
/-- Every submonoid of a commutative monoid is an Ore set.  -/
OreLocalization.oreSetComm : {R : Type u_2} → [inst : CommMonoid R] → (S : Submonoid R) → OreLocalization.OreSet S
-- Mathlib.Algebra.Group.Subgroup.Ker
AddMonoidHom.range_eq_map : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (f : G →+ N), f.range = AddSubgroup.map f ⊤
-- Mathlib.RingTheory.Flat.Basic
/-- If `M` is flat then `M ⊗ -` is an exact functor.  -/
Module.Flat.lTensor_exact : ∀ {R : Type u} (M : Type v) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Module.Flat R M]
  ⦃N : Type u_1⦄ ⦃N' : Type u_2⦄ ⦃N'' : Type u_3⦄ [inst_4 : AddCommGroup N] [inst_5 : AddCommGroup N']
  [inst_6 : AddCommGroup N''] [inst_7 : Module R N] [inst_8 : Module R N'] [inst_9 : Module R N''] ⦃f : N →ₗ[R] N'⦄
  ⦃g : N' →ₗ[R] N''⦄, Function.Exact ⇑f ⇑g → Function.Exact ⇑(LinearMap.lTensor M f) ⇑(LinearMap.lTensor M g)
-- Mathlib.Computability.Reduce
ManyOneEquiv.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : Primcodable α] [inst_1 : Primcodable β] (p : α → Prop) (q : β → Prop),
  ManyOneEquiv p q = (p ≤₀ q ∧ q ≤₀ p)
-- Mathlib.Algebra.Module.Presentation.Tensor
Module.Presentation.tensor_G : ∀ {A : Type u} [inst : CommRing A] {M₁ : Type v₁} {M₂ : Type v₂} [inst_1 : AddCommGroup M₁] [inst_2 : AddCommGroup M₂]
  [inst_3 : Module A M₁] [inst_4 : Module A M₂] (pres₁ : Module.Presentation A M₁) (pres₂ : Module.Presentation A M₂),
  (pres₁.tensor pres₂).G = (pres₁.G × pres₂.G)
-- Mathlib.CategoryTheory.Triangulated.Opposite.Triangle
CategoryTheory.Pretriangulated.TriangleOpEquivalence.counitIso_hom_app_hom₃ : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  (X : CategoryTheory.Pretriangulated.Triangle Cᵒᵖ),
  ((CategoryTheory.Pretriangulated.TriangleOpEquivalence.counitIso C).hom.app X).hom₃ =
    CategoryTheory.CategoryStruct.id X.obj₃
-- Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
/-- If `X` is universally closed over a field, then `X` is quasi-compact.  -/
AlgebraicGeometry.compactSpace_of_universallyClosed : ∀ {X : AlgebraicGeometry.Scheme} {K : Type u} [inst : Field K] (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K))
  [AlgebraicGeometry.UniversallyClosed f], CompactSpace ↥X
-- Mathlib.Algebra.Regular.Opposite
/-- **Alias** of the reverse direction of `isRegular_op`. -/
IsRegular.op : ∀ {R : Type u_1} [inst : Mul R] {a : R}, IsRegular a → IsRegular (MulOpposite.op a)
-- Mathlib.Data.Set.PowersetCard
Set.powersetCard.ncard_eq : ∀ {α : Type u_1} {n : ℕ} (s : ↑(Set.powersetCard α n)), (↑s).ncard = n
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
CategoryTheory.Limits.inr_pushoutAssoc_hom_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ Z₁ Z₂ : C} (g₁ : Z₁ ⟶ X₁) (g₂ : Z₁ ⟶ X₂)
  (g₃ : Z₂ ⟶ X₂) (g₄ : Z₂ ⟶ X₃) [inst_1 : CategoryTheory.Limits.HasPushout g₁ g₂]
  [inst_2 : CategoryTheory.Limits.HasPushout g₃ g₄]
  [inst_3 :
    CategoryTheory.Limits.HasPushout (CategoryTheory.CategoryStruct.comp g₃ (CategoryTheory.Limits.pushout.inr g₁ g₂))
      g₄]
  [inst_4 :
    CategoryTheory.Limits.HasPushout g₁
      (CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.pushout.inl g₃ g₄))]
  {Z : C}
  (h :
    CategoryTheory.Limits.pushout g₁ (CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.pushout.inl g₃ g₄)) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pushout.inr
        (CategoryTheory.CategoryStruct.comp g₃ (CategoryTheory.Limits.pushout.inr g₁ g₂)) g₄)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutAssoc g₁ g₂ g₃ g₄).hom h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr g₃ g₄)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pushout.inr g₁
          (CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.pushout.inl g₃ g₄)))
        h)
-- Mathlib.Analysis.Fourier.AddCircle
/-- The star subalgebra of `C(AddCircle T, ℂ)` generated by `fourier n` for `n ∈ ℤ` .  -/
fourierSubalgebra : {T : ℝ} → StarSubalgebra ℂ C(AddCircle T, ℂ)
-- Mathlib.Algebra.Group.Subgroup.Finite
AddSubgroup.val_multiset_sum : ∀ {G : Type u_3} [inst : AddCommGroup G] (H : AddSubgroup G) (m : Multiset ↥H),
  ↑m.sum = (Multiset.map Subtype.val m).sum
-- Mathlib.Computability.TuringMachine.Computable
/-- A Turing machine computing the identity on α.  -/
Turing.idComputer : (αΓ : Type) → [Fintype αΓ] → Turing.FinTM2
-- Mathlib.NumberTheory.Fermat
Nat.fermatNumber_eq_prod_add_two : ∀ (n : ℕ), n.fermatNumber = ∏ k ∈ Finset.range n, k.fermatNumber + 2
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
_private.Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality.0.InnerProductGeometry.inner_ortho_right_eq_sin_angle : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
  ‖x‖ = 1 →
    ‖y‖ = 1 →
      inner ℝ x (NormedSpace.normalize (InnerProductGeometry.ortho✝ y x)) = Real.sin (InnerProductGeometry.angle x y)
-- Mathlib.Analysis.Normed.Ring.WithAbs
WithAbs.ofAbs_add : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring S] [inst_1 : PartialOrder S] [inst_2 : Semiring R]
  (v : AbsoluteValue R S) (x y : WithAbs v), (x + y).ofAbs = x.ofAbs + y.ofAbs
-- Mathlib.Analysis.Calculus.FDeriv.Mul
HasFDerivWithinAt.smul_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {x : E}
  {s : Set E} {𝕜' : Type u_5} [inst_5 : NormedRing 𝕜'] [inst_6 : NormedAlgebra 𝕜 𝕜'] [inst_7 : Module 𝕜' F]
  [inst_8 : IsBoundedSMul 𝕜' F] [inst_9 : IsScalarTower 𝕜 𝕜' F] {c : E → 𝕜'} {c' : E →L[𝕜] 𝕜'},
  HasFDerivWithinAt c c' s x → ∀ (f : F), HasFDerivWithinAt (fun y => c y • f) (c'.smulRight f) s x
-- Mathlib.Topology.EMetricSpace.VariationOnFromTo
variationOnFromTo.sub_right : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] {f : α → E} {s : Set α},
  LocallyBoundedVariationOn f s →
    ∀ {a b c : α},
      a ∈ s → b ∈ s → c ∈ s → variationOnFromTo f s a b - variationOnFromTo f s a c = variationOnFromTo f s c b
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.symm_trans : ∀ {R : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} {E : Type u_5} {E₂ : Type u_6} {E₃ : Type u_7} [inst : Semiring R]
  [inst_1 : Semiring R₂] [inst_2 : Semiring R₃] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {σ₁₃ : R →+* R₃} {σ₃₁ : R₃ →+* R}
  {σ₂₃ : R₂ →+* R₃} {σ₃₂ : R₃ →+* R₂} [inst_3 : RingHomInvPair σ₁₂ σ₂₁] [inst_4 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_5 : RingHomInvPair σ₁₃ σ₃₁] [inst_6 : RingHomInvPair σ₃₁ σ₁₃] [inst_7 : RingHomInvPair σ₂₃ σ₃₂]
  [inst_8 : RingHomInvPair σ₃₂ σ₂₃] [inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [inst_10 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁]
  [inst_11 : SeminormedAddCommGroup E] [inst_12 : SeminormedAddCommGroup E₂] [inst_13 : SeminormedAddCommGroup E₃]
  [inst_14 : Module R E] [inst_15 : Module R₂ E₂] [inst_16 : Module R₃ E₃] (e₁ : E ≃ₛₗᵢ[σ₁₂] E₂) (e₂ : E₂ ≃ₛₗᵢ[σ₂₃] E₃),
  (e₁.trans e₂).symm = e₂.symm.trans e₁.symm
-- Mathlib.Data.NNReal.Defs
NNReal.div_le_of_le_mul' : ∀ {a b c : NNReal}, a ≤ b * c → a / b ≤ c