mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
WeierstrassCurve.natDegree_preΨ : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) {n : ℤ},
  ↑n ≠ 0 → (W.preΨ n).natDegree = (n.natAbs ^ 2 - if Even n then 4 else 1) / 2
-- Mathlib.GroupTheory.Nilpotent
/-- If a finite group is the direct product of its Sylow groups, it is nilpotent  -/
Group.isNilpotent_of_product_of_sylow_group : ∀ {G : Type u_1} [hG : Group G] [Finite G] (e : ((p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p) G) → ↥↑P) ≃* G),
  Group.IsNilpotent G
-- Mathlib.Data.Finset.Lattice.Fold
Finset.apply_inf_eq_inf_comp_of_linearOrder : ∀ {α : Type u_2} {β : Type u_3} {ι : Type u_5} [inst : LinearOrder α] [inst_1 : OrderTop α] {s : Finset ι} {f : ι → α}
  [inst_2 : SemilatticeInf β] [inst_3 : OrderTop β] (g : α → β), Monotone g → g ⊤ = ⊤ → g (s.inf f) = s.inf (g ∘ f)
-- Mathlib.GroupTheory.OrderOfElement
/-- Every finite left cancellative monoid is a group.  -/
LeftCancelMonoid.groupOfFinite : {G : Type u_1} → [LeftCancelMonoid G] → [Finite G] → Group G
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
/-- A zero morphism `0 : X ⟶ Y` is an isomorphism if and only if
the identities on both `X` and `Y` are zero.
 -/
CategoryTheory.Limits.isIsoZeroEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (X Y : C) →
        CategoryTheory.IsIso 0 ≃ CategoryTheory.CategoryStruct.id X = 0 ∧ CategoryTheory.CategoryStruct.id Y = 0
-- Mathlib.ModelTheory.Encoding
_private.Mathlib.ModelTheory.Encoding.0.FirstOrder.Language.Term.listEncode.match_1.splitter : {L : FirstOrder.Language} →
  {α : Type u_3} →
    (motive : L.Term α → Sort u_4) →
      (x : L.Term α) →
        ((i : α) → motive (FirstOrder.Language.var i)) →
          ((l : ℕ) → (f : L.Functions l) → (ts : Fin l → L.Term α) → motive (FirstOrder.Language.func f ts)) → motive x
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
tprod_mulIndicator_of_mem_union_disjoint : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] (s : γ → Set β)
  (f : β → α), Pairwise (Function.onFun Disjoint s) → ∀ i ∈ ⋃ d, s d, ∏' (d : γ), (s d).mulIndicator f i = f i
-- Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
/-- The colimit cocone for the coproduct with a zero object is colimiting.  -/
CategoryTheory.Limits.binaryCofanZeroLeftIsColimit : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
      [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
        (X : C) → CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.binaryCofanZeroLeft X)
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.instIsIsoH₁Hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E F : CategoryTheory.PreOneHypercover S} (e : E ≅ F)
  {i j : E.I₀} (k : E.I₁ i j), CategoryTheory.IsIso (e.hom.h₁ k)
-- Mathlib.Algebra.Order.Group.Unbundled.Int
Int.emod_abs : ∀ (a b : ℤ), a % |b| = a % b
-- Lean.Meta.Tactic.Simp.Types
/-- When using `Simp.Config.index := false`, and `set_option diagnostics true`,
for every theorem used by `simp`, we check whether the theorem would be
also applied if `index := true`, and we store it here if it would not have
been tried.
 -/
Lean.Meta.Simp.Diagnostics.thmsWithBadKeys : Lean.Meta.Simp.Diagnostics → Lean.PArray Lean.Meta.SimpTheorem
-- Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
RootPairing.pairingIn_lt_zero_iff : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (S : Type u_5)
  [inst_5 : CommRing S] [inst_6 : LinearOrder S] [IsStrictOrderedRing S] [inst_8 : Algebra S R] [FaithfulSMul S R]
  [inst_10 : Module S M] [IsScalarTower S R M] [inst_12 : P.IsValuedIn S] {i j : ι} [Finite ι],
  P.pairingIn S i j < 0 ↔ P.pairingIn S j i < 0
-- Mathlib.Computability.RE
ComputablePred.computable_iff : ∀ {α : Type u_1} [inst : Primcodable α] {p : α → Prop}, ComputablePred p ↔ ∃ f, Computable f ∧ p = fun a => f a = true
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
/-- The left injection into a product is a continuous linear map.  -/
ContinuousLinearMap.inl : (R : Type u_1) →
  [inst : Semiring R] →
    (M₁ : Type u_2) →
      [inst_1 : TopologicalSpace M₁] →
        [inst_2 : AddCommMonoid M₁] →
          [inst_3 : Module R M₁] →
            (M₂ : Type u_3) →
              [inst_4 : TopologicalSpace M₂] → [inst_5 : AddCommMonoid M₂] → [inst_6 : Module R M₂] → M₁ →L[R] M₁ × M₂
-- Mathlib.Analysis.Calculus.Deriv.Mul
HasDerivWithinAt.finsetProd : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} {ι : Type u_2} [inst_1 : DecidableEq ι]
  {𝔸' : Type u_3} [inst_2 : NormedCommRing 𝔸'] [inst_3 : NormedAlgebra 𝕜 𝔸'] {u : Finset ι} {f : ι → 𝕜 → 𝔸'}
  {f' : ι → 𝔸'},
  (∀ i ∈ u, HasDerivWithinAt (f i) (f' i) s x) →
    HasDerivWithinAt (∏ i ∈ u, f i) (∑ i ∈ u, (∏ j ∈ u.erase i, f j x) • f' i) s x
-- Mathlib.GroupTheory.FiniteIndexNormalSubgroup
FiniteIndexNormalSubgroup.comap_id : ∀ {G : Type u_1} [inst : Group G] (K : FiniteIndexNormalSubgroup G),
  FiniteIndexNormalSubgroup.comap (MonoidHom.id G) K = K
-- Mathlib.Analysis.Complex.Tietze
Complex.instTietzeExtension : TietzeExtension ℂ
-- Mathlib.Algebra.Regular.Basic
IsAddRightRegular.nsmul : ∀ {R : Type u_1} [inst : AddMonoid R] {a : R} (n : ℕ), IsAddRightRegular a → IsAddRightRegular (n • a)
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.Embedding.preimage_edgeSet : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G ↪g G'),
  Sym2.map ⇑f ⁻¹' G'.edgeSet = G.edgeSet
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
/-- A morphism is `QuasiSeparated` if diagonal map is quasi-compact.  -/
AlgebraicGeometry.QuasiSeparated : {X Y : AlgebraicGeometry.Scheme} → (X ⟶ Y) → Prop
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.centralizer_univ : ∀ (R : Type u) {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : StarRing A]
  [inst_3 : Module R A] [inst_4 : IsScalarTower R A A] [inst_5 : SMulCommClass R A A],
  NonUnitalStarSubalgebra.centralizer R Set.univ = NonUnitalStarSubalgebra.center R A
-- Mathlib.Algebra.Category.ModuleCat.Basic
ModuleCat.lsmul_eq_smul_id : ∀ {S : Type u} [inst : CommRing S] (M : ModuleCat S) (s : S),
  ModuleCat.ofHom ((LinearMap.lsmul S ↑M) s) = s • CategoryTheory.CategoryStruct.id M
-- Lean.Elab.Tactic.Try
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.evalSuggestAtomic : Lean.TSyntax `tactic → Lean.Elab.Tactic.TacticM (Lean.TSyntax `tactic)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.insert.congr_simp : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (v v_1 : β k),
  v = v_1 →
    ∀ (t : Std.DTreeMap.Internal.Impl α β) (hl : t.Balanced),
      Std.DTreeMap.Internal.Impl.insert k v t hl = Std.DTreeMap.Internal.Impl.insert k v_1 t hl
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.Path.listL.eq_def : ∀ {α : Type u_1} (x : RBTree.RBNode.Path α),
  x.listL =
    match x with
    | RBTree.RBNode.Path.root => []
    | RBTree.RBNode.Path.left c parent v r => parent.listL
    | RBTree.RBNode.Path.right c l v parent => parent.listL ++ (l.toList ++ [v])
-- Mathlib.GroupTheory.HNNExtension
HNNExtension.NormalWord.cons_toList : ∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} {d : HNNExtension.NormalWord.TransversalPair G A B} (g : G)
  (u : ℤˣ) (w : HNNExtension.NormalWord d) (h1 : w.head ∈ d.set u)
  (h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ HNNExtension.toSubgroup A B u → u = u'),
  (HNNExtension.NormalWord.cons g u w h1 h2).toList = (u, w.head) :: w.toList
-- Init.Data.Vector.OfFn
Vector.ofFn_succ' : ∀ {n : ℕ} {α : Type u_1} {f : Fin (n + 1) → α}, Vector.ofFn f = Vector.cast ⋯ (#v[f 0] ++ Vector.ofFn fun i => f i.succ)
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.iInter₂_vadd_subset : ∀ {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ι → Sort u_6} [inst : VAdd α β] (s : (i : ι) → κ i → Set α)
  (t : Set β), (⋂ i, ⋂ j, s i j) +ᵥ t ⊆ ⋂ i, ⋂ j, s i j +ᵥ t
-- Mathlib.Algebra.Polynomial.Degree.Domain
Polynomial.eq_zero_of_dvd_of_degree_lt : ∀ {R : Type u} [inst : Semiring R] [NoZeroDivisors R] {p q : Polynomial R}, p ∣ q → q.degree < p.degree → q = 0
-- Mathlib.RingTheory.Bialgebra.TensorProduct
Bialgebra.TensorProduct.coalgebra_rid_eq_algebra_rid_apply : ∀ {R : Type u_1} {S : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Semiring A]
  [inst_3 : Bialgebra S A] [inst_4 : Algebra R A] [inst_5 : Algebra R S] [inst_6 : IsScalarTower R S A]
  (x : TensorProduct R A R), (Coalgebra.TensorProduct.rid R S A) x = (Algebra.TensorProduct.rid R R A) x
-- Mathlib.Data.FinEnum
FinEnum.instUInt32 : FinEnum UInt32
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.derivative_ofNat : ∀ {R : Type u} [inst : Semiring R] (n : ℕ) [inst_1 : n.AtLeastTwo], Polynomial.derivative (OfNat.ofNat n) = 0
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
CategoryTheory.Limits.Cofork.unop.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : Cᵒᵖ} {f g : X ⟶ Y}
  (c : CategoryTheory.Limits.Cofork f g),
  c.unop =
    ((CategoryTheory.Limits.Cocone.precompose (CategoryTheory.Limits.opParallelPairIso f.unop g.unop).hom).obj
        (CategoryTheory.Limits.Cocone.whisker CategoryTheory.Limits.walkingParallelPairOpEquiv.inverse c)).unop
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Equiv.mul_eq_comp : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} (x y : P.Equiv P),
  x * y = x.comp y
-- Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated
/-- Given `CompStruct f g h` and `CompStruct f' g' h'` with the same vertices and edges such
that `f` ≃ `f'` and `g` ≃ `g'`, then the long diagonal edges `h` and `h'` are also homotopic.
 -/
SSet.Truncated.Edge.CompStruct.comp_unique : ∀ {A : SSet.Truncated 2} [A.Quasicategory₂]
  {x y z : A.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Quasicategory₂._proof_1 })}
  {f f' : SSet.Truncated.Edge x y} {g g' : SSet.Truncated.Edge y z} {h h' : SSet.Truncated.Edge x z}
  (s : f.CompStruct g h) (s' : f'.CompStruct g' h'),
  SSet.Truncated.HomotopicL f f' → SSet.Truncated.HomotopicL g g' → SSet.Truncated.HomotopicL h h'
-- Mathlib.Topology.Sets.Order
ClopenUpperSet.coe_toUpperSet : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LE α] (s : ClopenUpperSet α), ↑s.toUpperSet = ↑s
-- Init.Data.ToString.Basic
instReprExcept : {ε : Type u_1} → {α : Type u_2} → [Repr ε] → [Repr α] → Repr (Except ε α)
-- Lean.Meta.Tactic.Grind.MatchCond
/-- Replaces the left-hand side of an equality (or heterogeneous equality) `e` with `lhsNew`.
 -/
_private.Lean.Meta.Tactic.Grind.MatchCond.0.Lean.Meta.Grind.replaceLhs? : Lean.Expr → Lean.Expr → Option Lean.Expr → Option Lean.Expr
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.instPow.eq_1 : ∀ {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [inst : (i : ι) → SetLike (S i) (R i)]
  {B : (i : ι) → S i} [inst_1 : (i : ι) → Monoid (R i)] [inst_2 : ∀ (i : ι), SubmonoidClass (S i) (R i)],
  RestrictedProduct.instPow R = { pow := fun x n => ⟨fun i => x i ^ n, ⋯⟩ }
-- Mathlib.Order.Filter.AtTopBot.Ring
Filter.Tendsto.atBot_mul_atBot₀ : ∀ {α : Type u_1} {β : Type u_2} [inst : Ring α] [inst_1 : PartialOrder α] [IsOrderedRing α] {l : Filter β}
  {f g : β → α},
  Filter.Tendsto f l Filter.atBot → Filter.Tendsto g l Filter.atBot → Filter.Tendsto (fun x => f x * g x) l Filter.atTop
-- Batteries.Tactic.Lint.Frontend
Batteries.Tactic.Lint.instReprLintVerbosity : Repr Batteries.Tactic.Lint.LintVerbosity
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.denoteInt : {α : Type u_1} → [Lean.Grind.Ring α] → ℤ → α
-- Lean.Meta.Sym.Arith.Types
Lean.Meta.Sym.Arith.instInhabitedCommRing.default : Lean.Meta.Sym.Arith.CommRing
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Affine.Simplex.map_mkOfPoint : ∀ {k : Type u_1} {V : Type u_2} {V₂ : Type u_3} {P : Type u_5} {P₂ : Type u_6} [inst : Ring k] [inst_1 : AddCommGroup V]
  [inst_2 : AddCommGroup V₂] [inst_3 : Module k V] [inst_4 : Module k V₂] [inst_5 : AddTorsor V P]
  [inst_6 : AddTorsor V₂ P₂] (f : P →ᵃ[k] P₂) (hf : Function.Injective ⇑f) (p : P),
  (Affine.Simplex.mkOfPoint k p).map f hf = Affine.Simplex.mkOfPoint k (f p)
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.InfinitePlace.IsUnramified.comap : ∀ {k : Type u_1} [inst : Field k] (K : Type u_2) [inst_1 : Field K] {F : Type u_3} [inst_2 : Field F]
  [inst_3 : Algebra k K] [inst_4 : Algebra k F] [inst_5 : Algebra K F] [IsScalarTower k K F]
  {w : NumberField.InfinitePlace F},
  NumberField.InfinitePlace.IsUnramified k w → NumberField.InfinitePlace.IsUnramified k (w.comap (algebraMap K F))
-- Mathlib.CategoryTheory.Functor.TwoSquare
/-- The opposite of a `2`-square.  -/
CategoryTheory.TwoSquare.op : {C₁ : Type u₁} →
  {C₂ : Type u₂} →
    {C₃ : Type u₃} →
      {C₄ : Type u₄} →
        [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
          [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
            [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃] →
              [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] →
                {T : CategoryTheory.Functor C₁ C₂} →
                  {L : CategoryTheory.Functor C₁ C₃} →
                    {R : CategoryTheory.Functor C₂ C₄} →
                      {B : CategoryTheory.Functor C₃ C₄} →
                        CategoryTheory.TwoSquare T L R B → CategoryTheory.TwoSquare L.op T.op B.op R.op
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.mem_sup_of_normal_left : ∀ {G : Type u_1} [inst : Group G] {s t : Subgroup G} [hs : s.Normal] {x : G}, x ∈ s ⊔ t ↔ ∃ y ∈ s, ∃ z ∈ t, y * z = x
-- Mathlib.Algebra.Group.Subgroup.Map
Subgroup.le_comap_map : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (f : G →* N) (H : Subgroup G),
  H ≤ Subgroup.comap f (Subgroup.map f H)
-- Mathlib.CategoryTheory.Localization.SmallShiftedHom
/-- Given `f : SmallShiftedHom.{w} W X Y a`, this is the element in
`SmallHom.{w} W (X⟦n⟧) (Y⟦a'⟧)` that is obtained by shifting by `n`
when `a + n = a'`.  -/
CategoryTheory.Localization.SmallShiftedHom.shift : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {W : CategoryTheory.MorphismProperty C} →
      {M : Type w'} →
        [inst_1 : AddMonoid M] →
          [inst_2 : CategoryTheory.HasShift C M] →
            [W.IsCompatibleWithShift M] →
              {X Y : C} →
                {a : M} →
                  [inst_4 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Y] →
                    [CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M Y Y] →
                      CategoryTheory.Localization.SmallShiftedHom W X Y a →
                        (n a' : M) →
                          a + n = a' →
                            CategoryTheory.Localization.SmallHom W ((CategoryTheory.shiftFunctor C n).obj X)
                              ((CategoryTheory.shiftFunctor C a').obj Y)
-- Mathlib.Analysis.Normed.Group.Basic
dist_prod_prod_le : ∀ {ι : Type u_3} {E : Type u_5} [inst : SeminormedCommGroup E] (s : Finset ι) (f a : ι → E),
  dist (∏ b ∈ s, f b) (∏ b ∈ s, a b) ≤ ∑ b ∈ s, dist (f b) (a b)
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.constₐ_apply_apply : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] (R : Type u_6) [inst_1 : CommSemiring R]
  [inst_2 : Semiring Y] [inst_3 : Algebra R Y] (y : Y) (a : X), ((LocallyConstant.constₐ R) y) a = y
-- Mathlib.Tactic.Linter.TextBased.UnicodeLinter
/-- Allowed (by the linter) ASCII characters  -/
_private.Mathlib.Tactic.Linter.TextBased.UnicodeLinter.0.Mathlib.Linter.TextBased.UnicodeLinter.ASCII.allowed : Char → Bool
-- Init.Dynamic
instNonemptyTypeName : ∀ {α : Type u_1}, Nonempty (TypeName α)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
/-- If `G` is a monoid object, then `Hom(-, G)` as a presheaf of monoids is represented by `G`.  -/
CategoryTheory.yonedaGrpObjRepresentableBy : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      (G : C) →
        [inst_2 : CategoryTheory.GrpObj G] →
          ((CategoryTheory.yonedaGrpObj G).comp (CategoryTheory.forget GrpCat)).RepresentableBy G
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
/-- The pushout of an epimorphism is an epimorphism  -/
CategoryTheory.Limits.pushout.inl_of_epi : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z}
  [inst_1 : CategoryTheory.Limits.HasPushout f g] [CategoryTheory.Epi g],
  CategoryTheory.Epi (CategoryTheory.Limits.pushout.inl f g)
-- Mathlib.Topology.NhdsWithin
mem_nhdsWithin : ∀ {α : Type u_1} [inst : TopologicalSpace α] {t : Set α} {a : α} {s : Set α},
  t ∈ nhdsWithin a s ↔ ∃ u, IsOpen u ∧ a ∈ u ∧ u ∩ s ⊆ t
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf
/-- `Proj` of a graded ring as a `LocallyRingedSpace`  -/
AlgebraicGeometry.Proj.toLocallyRingedSpace : {A : Type u_1} →
  {σ : Type u_2} →
    [inst : CommRing A] →
      [inst_1 : SetLike σ A] →
        [inst_2 : AddSubgroupClass σ A] → (𝒜 : ℕ → σ) → [GradedRing 𝒜] → AlgebraicGeometry.LocallyRingedSpace
-- Mathlib.Analysis.InnerProductSpace.PiL2
/-- A shorthand for `PiLp.continuousLinearEquiv`.  -/
EuclideanSpace.equiv : (ι : Type u_1) → (𝕜 : Type u_3) → [inst : RCLike 𝕜] → EuclideanSpace 𝕜 ι ≃L[𝕜] ι → 𝕜
-- Lean.AddDecl
/-- If the `warn.sorry` option is set to true and there are no errors in the log already,
logs a warning if the declaration uses `sorry`.
 -/
Lean.warnIfUsesSorry : Lean.Declaration → Lean.CoreM Unit
-- Init.Data.List.Basic
List.take_succ_cons : ∀ {α : Type u} {a : α} {as : List α} {i : ℕ}, List.take (i + 1) (a :: as) = a :: List.take i as
-- Mathlib.Combinatorics.Additive.CauchyDavenport
/-- The **Cauchy-Davenport Theorem** for linearly ordered cancellative semigroups. The size of
`s * t` is lower-bounded by `|s| + |t| - 1`.  -/
cauchy_davenport_mul_of_linearOrder_isCancelMul : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : Mul α] [IsCancelMul α] [MulLeftMono α] [MulRightMono α]
  {s t : Finset α}, s.Nonempty → t.Nonempty → s.card + t.card - 1 ≤ (s * t).card
-- Mathlib.Algebra.Category.Grp.Basic
GrpCat.of.eq_1 : ∀ (M : Type u) [inst : Group M], GrpCat.of M = { carrier := M, str := inst }
-- Mathlib.RingTheory.PicardGroup
Module.Invertible.rTensor_bijective_iff : ∀ {R : Type u} (M : Type v) {N : Type u_1} {P : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Module R P] [Module.Invertible R M] {f : N →ₗ[R] P},
  Function.Bijective ⇑(LinearMap.rTensor M f) ↔ Function.Bijective ⇑f
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.combine'.match_1.congr_eq_2 : ∀ (motive : Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → Sort u_1) (p₁ p₂ : Int.Internal.Linear.Poly)
  (h_1 : (k₁ k₂ : ℤ) → motive (Int.Internal.Linear.Poly.num k₁) (Int.Internal.Linear.Poly.num k₂))
  (h_2 :
    (k₁ a : ℤ) →
      (x : Int.Internal.Linear.Var) →
        (p : Int.Internal.Linear.Poly) → motive (Int.Internal.Linear.Poly.num k₁) (Int.Internal.Linear.Poly.add a x p))
  (h_3 :
    (a : ℤ) →
      (x : Int.Internal.Linear.Var) →
        (p : Int.Internal.Linear.Poly) →
          (k₂ : ℤ) → motive (Int.Internal.Linear.Poly.add a x p) (Int.Internal.Linear.Poly.num k₂))
  (h_4 :
    (a₁ : ℤ) →
      (x₁ : Int.Internal.Linear.Var) →
        (p₁ : Int.Internal.Linear.Poly) →
          (a₂ : ℤ) →
            (x₂ : Int.Internal.Linear.Var) →
              (p₂ : Int.Internal.Linear.Poly) →
                motive (Int.Internal.Linear.Poly.add a₁ x₁ p₁) (Int.Internal.Linear.Poly.add a₂ x₂ p₂))
  (k₁ a : ℤ) (x : Int.Internal.Linear.Var) (p : Int.Internal.Linear.Poly),
  p₁ = Int.Internal.Linear.Poly.num k₁ →
    p₂ = Int.Internal.Linear.Poly.add a x p →
      (match p₁, p₂ with
        | Int.Internal.Linear.Poly.num k₁, Int.Internal.Linear.Poly.num k₂ => h_1 k₁ k₂
        | Int.Internal.Linear.Poly.num k₁, Int.Internal.Linear.Poly.add a x p => h_2 k₁ a x p
        | Int.Internal.Linear.Poly.add a x p, Int.Internal.Linear.Poly.num k₂ => h_3 a x p k₂
        | Int.Internal.Linear.Poly.add a₁ x₁ p₁, Int.Internal.Linear.Poly.add a₂ x₂ p₂ => h_4 a₁ x₁ p₁ a₂ x₂ p₂) ≍
        h_2 k₁ a x p
-- Mathlib.Topology.Algebra.Module.FiniteDimension
Submodule.CoFG.topologicalClosure : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : AddCommGroup E] [inst_1 : TopologicalSpace E] [inst_2 : Ring 𝕜]
  [inst_3 : Module 𝕜 E] [inst_4 : ContinuousAdd E] [inst_5 : ContinuousConstSMul 𝕜 E] (s : Submodule 𝕜 E) [s.CoFG],
  s.topologicalClosure.CoFG
-- Mathlib.LinearAlgebra.Matrix.ToLin
/-- If `M` and `M'` are each other's inverse matrices, they provide an equivalence between `n → A`
and `m → A` corresponding to `M.vecMul` and `M'.vecMul`.  -/
Matrix.toLinearEquivRight'OfInv : {R : Type u_1} →
  [inst : Semiring R] →
    {m : Type u_3} →
      {n : Type u_4} →
        [inst_1 : Fintype m] →
          [inst_2 : DecidableEq m] →
            [inst_3 : Fintype n] →
              [inst_4 : DecidableEq n] →
                {M : Matrix m n R} → {M' : Matrix n m R} → M * M' = 1 → M' * M = 1 → (n → R) ≃ₗ[R] m → R
-- Mathlib.Data.EReal.Basic
EReal.coe_ennreal_ne_zero : ∀ {x : ENNReal}, ↑x ≠ 0 ↔ x ≠ 0
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get!_modify_self : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {k : α}
  [inst_1 : Inhabited (β k)] {f : β k → β k}, (m.modify k f).get! k = (Option.map f (m.get? k)).get!
-- Mathlib.Dynamics.FixedPoints.Prufer
/-- Let `n : ℤ` and `s` a subset of a commutative group `G` that is invariant under preimage for
the map `x ↦ x^n`. Then `s` is invariant under the pointwise action of the subgroup of elements
`g : G` such that `g^(n^j) = 1` for some `j : ℕ`. (This subgroup is called the Prüfer subgroup when
`G` is the `Circle` and `n` is prime.)  -/
smul_eq_self_of_preimage_zpow_eq_self : ∀ {G : Type u_1} [inst : CommGroup G] {n : ℤ} {s : Set G},
  (fun x => x ^ n) ⁻¹' s = s → ∀ {g : G} {j : ℕ}, g ^ n ^ j = 1 → g • s = s
-- Mathlib.AlgebraicTopology.ExtraDegeneracy
CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.homotopy_h : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : CategoryTheory.SimplicialObject.Augmented C}
  (ed : X.ExtraDegeneracy) {n : ℕ} (i : Fin (n + 1)),
  ed.homotopy.h i = CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.homotopy.h ed i
-- Mathlib.Order.Filter.Pi
Filter.pi_neBot : ∀ {ι : Type u_1} {α : ι → Type u_2} {f : (i : ι) → Filter (α i)}, (Filter.pi f).NeBot ↔ ∀ (i : ι), (f i).NeBot
-- Mathlib.Topology.Algebra.UniformRing
UniformSpace.Completion.commRing : (R : Type u_2) →
  [inst : CommRing R] →
    [inst_1 : UniformSpace R] → [IsUniformAddGroup R] → [IsTopologicalRing R] → CommRing (UniformSpace.Completion R)
-- Mathlib.Probability.Distributions.Fernique
/-- **Fernique's theorem** for finite measures whose product is invariant by rotation: there exists
`C > 0` such that the function `x ↦ exp (C * ‖x‖ ^ 2)` is integrable.  -/
ProbabilityTheory.exists_integrable_exp_sq_of_map_rotation_eq_self : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [SecondCountableTopology E]
  [inst_3 : MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.Measure.map (⇑(ContinuousLinearMap.rotation (-(Real.pi / 4)))) (μ.prod μ) = μ.prod μ →
    ∃ C, 0 < C ∧ MeasureTheory.Integrable (fun x => Real.exp (C * ‖x‖ ^ 2)) μ
-- Mathlib.Order.JordanHolder
JordanHolderLattice.IsMaximal : {X : Type u} → {inst : Lattice X} → [self : JordanHolderLattice X] → X → X → Prop
-- Init.Data.Rat.Lemmas
Rat.num_divInt : ∀ (a b : ℤ), (Rat.divInt a b).num = b.sign * a / ↑(b.gcd a)
-- Mathlib.Algebra.Divisibility.Units
IsRelPrime.of_mul_left_left : ∀ {α : Type u_1} [inst : CommMonoid α] {x y z : α}, IsRelPrime (x * y) z → IsRelPrime x z