mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Lie.Weights.Cartan
LieAlgebra.rootSpaceProduct_tmul : ∀ (R : Type u_1) (L : Type u_2) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  (H : LieSubalgebra R L) [inst_3 : LieRing.IsNilpotent ↥H] (χ₁ χ₂ χ₃ : ↥H → R) (hχ : χ₁ + χ₂ = χ₃)
  (x : ↥(LieAlgebra.rootSpace H χ₁)) (y : ↥(LieAlgebra.rootSpace H χ₂)),
  ↑((LieAlgebra.rootSpaceProduct R L H χ₁ χ₂ χ₃ hχ) (x ⊗ₜ[R] y)) = ⁅↑x, ↑y⁆
-- Mathlib.Analysis.Matrix.LDL
/-- The diagonal matrix `D` of the LDL decomposition.  -/
LDL.diag : {𝕜 : Type u_1} →
  [inst : RCLike 𝕜] →
    {n : Type u_2} →
      [inst_1 : LinearOrder n] →
        [WellFoundedLT n] → [LocallyFiniteOrderBot n] → {S : Matrix n n 𝕜} → [Fintype n] → S.PosDef → Matrix n n 𝕜
-- Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
/-- If `Irreducible (cyclotomic (p ^ (k + 1)) K)` (in particular for `K = ℚ`) and `p` is a prime,
then the norm of `(zeta (p ^ (k + 1)) K L) ^ (p ^ s) - 1` is `p ^ (p ^ s)`
if `p ^ (k - s + 1) ≠ 2`.  -/
IsCyclotomicExtension.norm_zeta_pow_sub_one_of_prime_pow_ne_two : ∀ {p : ℕ} {K : Type u} (L : Type v) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {k : ℕ}
  [inst_3 : Fact (Nat.Prime p)] [inst_4 : IsCyclotomicExtension {p ^ (k + 1)} K L],
  Irreducible (Polynomial.cyclotomic (p ^ (k + 1)) K) →
    ∀ {s : ℕ},
      s ≤ k →
        p ^ (k - s + 1) ≠ 2 → (Algebra.norm K) (IsCyclotomicExtension.zeta (p ^ (k + 1)) K L ^ p ^ s - 1) = ↑p ^ p ^ s
-- Mathlib.Combinatorics.Colex
Finset.Colex.mem_initSeg_self : ∀ {α : Type u_1} [inst : LinearOrder α] {s : Finset α} [inst_1 : Fintype α], s ∈ Finset.Colex.initSeg s
-- Mathlib.Data.PSigma.Order
PSigma.Lex.noMaxOrder : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : Preorder ι] [inst_1 : (i : ι) → Preorder (α i)]
  [∀ (i : ι), NoMaxOrder (α i)], NoMaxOrder (Σₗ' (i : ι), α i)
-- Lean.Meta.Sym.LitValues
Lean.Meta.Sym.getStringValue? : Lean.Expr → Option String
-- Mathlib.Algebra.Ring.Parity
_private.Mathlib.Algebra.Ring.Parity.0.natCast_eq_zero_or_one_of_two_eq_zero' : ∀ {R : Type u_4} [inst : AddMonoidWithOne R] (n : ℕ), 2 = 0 → (Even n → ↑n = 0) ∧ (Odd n → ↑n = 1)
-- Mathlib.Algebra.Category.Semigrp.Basic
/-- Turn a morphism in `MagmaCat` back into a `MulHom`.  -/
MagmaCat.Hom.hom : {X Y : MagmaCat} → X.Hom Y → ↑X →ₙ* ↑Y
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey?_filter_containsKey_of_containsKey_eq_false_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)} {k : α},
  Std.Internal.List.DistinctKeys l₁ →
    Std.Internal.List.containsKey k l₂ = false →
      Std.Internal.List.getKey? k (List.filter (fun p => Std.Internal.List.containsKey p.fst l₂) l₁) = none
-- Mathlib.Algebra.Homology.QuasiIso
homotopyEquivalences_le_quasiIso : ∀ {ι : Type u_1} (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  (c : ComplexShape ι) [inst_2 : CategoryTheory.CategoryWithHomology C],
  HomologicalComplex.homotopyEquivalences C c ≤ HomologicalComplex.quasiIso C c
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.yonedaAddGrpObj.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] (G : C)
  [inst_2 : CategoryTheory.AddGrpObj G],
  CategoryTheory.yonedaAddGrpObj G =
    { obj := fun X => AddGrpCat.of (Opposite.unop X ⟶ G),
      map := fun {X Y} φ => AddGrpCat.ofHom (AddMonCat.Hom.hom ((CategoryTheory.yonedaAddMonObj G).map φ)), map_id := ⋯,
      map_comp := ⋯ }
-- Mathlib.Algebra.Group.Hom.Instances
/-- `ZeroHom M N` is an `AddCommMonoid` if `N` is commutative.  -/
ZeroHom.instAddCommMonoid : {M : Type uM} → {N : Type uN} → [inst : Zero M] → [inst_1 : AddCommMonoid N] → AddCommMonoid (ZeroHom M N)
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits
PresheafOfModules.limitPresheafOfModules_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {J : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J (PresheafOfModules R))
  [inst_2 :
    ∀ (X : Cᵒᵖ),
      Small.{v, max u₂ v}
        ↑((F.comp (PresheafOfModules.evaluation R X)).comp (CategoryTheory.forget (ModuleCat ↑(R.obj X)))).sections]
  {x Y : Cᵒᵖ} (f : x ⟶ Y),
  (PresheafOfModules.limitPresheafOfModules F).map f =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.limMap (F.whiskerLeft (PresheafOfModules.restriction R f)))
      (CategoryTheory.preservesLimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))
          (F.comp (PresheafOfModules.evaluation R Y))).inv
-- Mathlib.RingTheory.IdealFilter.Topology
/-- The topology `F.addGroupFilterBasis.topology` endows `A` with the structure of a topological
additive group.  -/
WithIdealFilter.instIsTopologicalAddGroup : ∀ {A : Type u_1} [inst : Ring A] {F : IdealFilter A}, IsTopologicalAddGroup (WithIdealFilter F)
-- Mathlib.Condensed.TopComparison
/-- If `G` preserves the relevant pullbacks and every effective epi in `C` is a quotient map (which is
the case when `C` is `CompHaus` or `Profinite`), then `yonedaPresheaf` satisfies the equalizer
condition which is required to be a sheaf for the regular topology.
 -/
equalizerCondition_yonedaPresheaf : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor C TopCat) (X : Type w')
  [inst_1 : TopologicalSpace X]
  [∀ (Z B : C) (π : Z ⟶ B) [CategoryTheory.EffectiveEpi π],
      CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan π π) G],
  (∀ (Z B : C) (π : Z ⟶ B) [CategoryTheory.EffectiveEpi π],
      Topology.IsQuotientMap ⇑(CategoryTheory.ConcreteCategory.hom (G.map π))) →
    CategoryTheory.regularTopology.EqualizerCondition (ContinuousMap.yonedaPresheaf G X)
-- Mathlib.Analysis.InnerProductSpace.Calculus
ContDiffWithinAt.dist : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
  [inst : NormedSpace ℝ E] {G : Type u_4} [inst_2 : NormedAddCommGroup G] [inst_3 : NormedSpace ℝ G] {f g : G → E}
  {s : Set G} {x : G} {n : WithTop ℕ∞},
  ContDiffWithinAt ℝ n f s x →
    ContDiffWithinAt ℝ n g s x → f x ≠ g x → ContDiffWithinAt ℝ n (fun y => dist (f y) (g y)) s x
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.coe_centralizer : ∀ (R : Type u_1) {A : Type u_2} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A] (s : Set A),
  ↑(NonUnitalSubalgebra.centralizer R s) = s.centralizer
-- Mathlib.Algebra.Azumaya.Defs
AlgHom.mulLeftRight.eq_1 : ∀ (R : Type u_1) (A : Type u_2) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A],
  AlgHom.mulLeftRight R A = Algebra.lsmul R R A
-- Mathlib.Topology.Maps.Proper.Basic
/-- If the composition of two continuous functions `g ∘ f` is proper and `g` is injective,
then `f` is proper.  -/
isProperMap_of_comp_of_inj : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {f : X → Y} {g : Y → Z},
  Continuous f → Continuous g → IsProperMap (g ∘ f) → Function.Injective g → IsProperMap f
-- Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
/-- The minimal polynomial of an element `x` is uniquely characterized by its defining property:
if there is another monic polynomial of minimal degree that has `x` as a root, then this polynomial
is equal to the minimal polynomial of `x`. See also `minpoly.unique` which relaxes the
assumptions on `S` in exchange for stronger assumptions on `R`.  -/
IsIntegrallyClosed.minpoly.unique : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [IsDomain R] [inst_3 : Algebra R S]
  [IsIntegrallyClosed R] [IsDomain S] [Module.IsTorsionFree R S] {s : S} {P : Polynomial R},
  P.Monic →
    (Polynomial.aeval s) P = 0 →
      (∀ (Q : Polynomial R), Q.Monic → (Polynomial.aeval s) Q = 0 → P.degree ≤ Q.degree) → P = minpoly R s
-- Init.Data.List.Scan.Lemmas
List.take_scanl : ∀ {β : Type u_1} {α : Type u_2} {f : β → α → β} (init : β) (as : List α) (i : ℕ),
  List.take (i + 1) (List.scanl f init as) = List.scanl f init (List.take i as)
-- Mathlib.MeasureTheory.Function.LpSpace.Indicator
MeasureTheory.indicatorConstLp_coeFn_mem : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] {s : Set α} {hs : MeasurableSet s} {hμs : μ s ≠ ⊤} {c : E},
  ∀ᵐ (x : α) ∂μ, x ∈ s → ↑↑(MeasureTheory.indicatorConstLp p hs hμs c) x = c
-- Init.Data.List.Find
List.Sublist.findIdx?_eq_none : ∀ {α : Type u_1} {p : α → Bool} {l₁ l₂ : List α}, l₁.Sublist l₂ → List.findIdx? p l₂ = none → List.findIdx? p l₁ = none
-- Std.Time.DateTime.PlainDateTime
Std.Time.instInhabitedPlainDateTime : Inhabited Std.Time.PlainDateTime
-- Mathlib.Analysis.Calculus.FDeriv.Defs
hasFDerivAt_iff_isLittleO : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : SeminormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {f' : E →L[𝕜] F} {x : E}, HasFDerivAt f f' x ↔ (fun x' => f x' - f x - f' (x' - x)) =o[nhds x] fun x' => x' - x
-- Batteries.Data.Fin.Coding
_private.Batteries.Data.Fin.Coding.0.Fin.decodePi.match_1.eq_1 : ∀ (n : ℕ) (motive : Fin (n + 1) → Sort u_1) (isLt : 0 < n + 1) (h_1 : (isLt : 0 < n + 1) → motive ⟨0, isLt⟩)
  (h_2 : (i : ℕ) → (hi : i + 1 < n + 1) → motive ⟨i.succ, hi⟩),
  (match ⟨0, isLt⟩ with
    | ⟨0, isLt⟩ => h_1 isLt
    | ⟨i.succ, hi⟩ => h_2 i hi) =
    h_1 isLt
-- Mathlib.Data.Set.Basic
Set.union_comm : ∀ {α : Type u} (a b : Set α), a ∪ b = b ∪ a
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
_private.Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno.0.OrderedFinpartition.extend.match_1.splitter : {n : ℕ} →
  (c : OrderedFinpartition n) →
    (motive : Option (Fin c.length) → Sort u_1) →
      (i : Option (Fin c.length)) → (Unit → motive none) → ((i : Fin c.length) → motive (some i)) → motive i
-- Mathlib.SetTheory.Ordinal.Basic
/-- An ordinal lifted to the same universe equals itself.  -/
Ordinal.lift_id : ∀ (a : Ordinal.{u}), Ordinal.lift.{u, u} a = a
-- Mathlib.SetTheory.Ordinal.FixedPointApproximants
OrdinalApprox.lfpApprox.eq_1 : ∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α) (x : α) (a : Ordinal.{u}),
  OrdinalApprox.lfpApprox f x a = x ⊔ ⨆ b, ⨆ (_ : b < a), f (OrdinalApprox.lfpApprox f x b)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.AddGrp.instAddGrpObj.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {H : CategoryTheory.AddGrp C}
  [inst_3 : CategoryTheory.IsCommAddMonObj H.X],
  CategoryTheory.AddGrp.instAddGrpObj =
    { toAddMonObj := CategoryTheory.AddGrp.instAddMonObj,
      neg := CategoryTheory.AddGrp.homMk' { hom := CategoryTheory.AddGrpObj.neg, isAddMonHom_hom := ⋯ }, left_neg := ⋯,
      right_neg := ⋯ }
-- Mathlib.Algebra.Homology.Augment
ChainComplex.augmentTruncate_inv_f_zero : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  (C : ChainComplex V ℕ), C.augmentTruncate.inv.f 0 = CategoryTheory.CategoryStruct.id (C.X 0)
-- Mathlib.LinearAlgebra.Matrix.Basis
/-- A matrix whose columns form a basis `b'`, expressed w.r.t. a basis `b`, is invertible.  -/
Module.Basis.invertibleToMatrix : {ι : Type u_1} →
  {R₂ : Type u_7} →
    {M₂ : Type u_8} →
      [inst : CommRing R₂] →
        [inst_1 : AddCommGroup M₂] →
          [inst_2 : Module R₂ M₂] →
            [inst_3 : DecidableEq ι] →
              [inst_4 : Fintype ι] → (b b' : Module.Basis ι R₂ M₂) → Invertible (b.toMatrix ⇑b')
-- Init.Data.Int.DivMod.Lemmas
Int.emod_negSucc : ∀ (m : ℕ) (n : ℤ), Int.negSucc m % n = Int.subNatNat n.natAbs (m % n.natAbs).succ
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.Monad.mk.inj : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {toFunctor : CategoryTheory.Functor C C}
  {η : CategoryTheory.Functor.id C ⟶ toFunctor} {μ : toFunctor.comp toFunctor ⟶ toFunctor}
  {assoc :
    autoParam
      (∀ (X : C),
        CategoryTheory.CategoryStruct.comp (toFunctor.map (μ.app X)) (μ.app X) =
          CategoryTheory.CategoryStruct.comp (μ.app (toFunctor.obj X)) (μ.app X))
      CategoryTheory.Monad.assoc._autoParam}
  {left_unit :
    autoParam
      (∀ (X : C),
        CategoryTheory.CategoryStruct.comp (η.app (toFunctor.obj X)) (μ.app X) =
          CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.id C).obj (toFunctor.obj X)))
      CategoryTheory.Monad.left_unit._autoParam}
  {right_unit :
    autoParam
      (∀ (X : C),
        CategoryTheory.CategoryStruct.comp (toFunctor.map (η.app X)) (μ.app X) =
          CategoryTheory.CategoryStruct.id (toFunctor.obj ((CategoryTheory.Functor.id C).obj X)))
      CategoryTheory.Monad.right_unit._autoParam}
  {toFunctor_1 : CategoryTheory.Functor C C} {η_1 : CategoryTheory.Functor.id C ⟶ toFunctor_1}
  {μ_1 : toFunctor_1.comp toFunctor_1 ⟶ toFunctor_1}
  {assoc_1 :
    autoParam
      (∀ (X : C),
        CategoryTheory.CategoryStruct.comp (toFunctor_1.map (μ_1.app X)) (μ_1.app X) =
          CategoryTheory.CategoryStruct.comp (μ_1.app (toFunctor_1.obj X)) (μ_1.app X))
      CategoryTheory.Monad.assoc._autoParam}
  {left_unit_1 :
    autoParam
      (∀ (X : C),
        CategoryTheory.CategoryStruct.comp (η_1.app (toFunctor_1.obj X)) (μ_1.app X) =
          CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.id C).obj (toFunctor_1.obj X)))
      CategoryTheory.Monad.left_unit._autoParam}
  {right_unit_1 :
    autoParam
      (∀ (X : C),
        CategoryTheory.CategoryStruct.comp (toFunctor_1.map (η_1.app X)) (μ_1.app X) =
          CategoryTheory.CategoryStruct.id (toFunctor_1.obj ((CategoryTheory.Functor.id C).obj X)))
      CategoryTheory.Monad.right_unit._autoParam},
  { toFunctor := toFunctor, η := η, μ := μ, assoc := assoc, left_unit := left_unit, right_unit := right_unit } =
      { toFunctor := toFunctor_1, η := η_1, μ := μ_1, assoc := assoc_1, left_unit := left_unit_1,
        right_unit := right_unit_1 } →
    toFunctor = toFunctor_1 ∧ η ≍ η_1 ∧ μ ≍ μ_1
-- Mathlib.Algebra.Star.Basic
StarAddMonoid.toStarModuleInt : ∀ {α : Type u_1} [inst : AddGroup α] [inst_1 : StarAddMonoid α], StarModule ℤ α
-- Mathlib.Data.Set.Lattice
/-- If `t` is an indexed family of sets, then there is a natural map from `Σ i, t i` to `⋃ i, t i`
sending `⟨i, x⟩` to `x`.  -/
Set.sigmaToiUnion : {α : Type u_1} → {β : Type u_2} → (t : α → Set β) → (i : α) × ↑(t i) → ↑(⋃ i, t i)
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.isoCocycles₂_hom_comp_i_assoc : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) {Z : ModuleCat k}
  (h : (groupCohomology.shortComplexH2 A).X₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (groupCohomology.isoCocycles₂ A).hom
      (CategoryTheory.CategoryStruct.comp (groupCohomology.shortComplexH2 A).moduleCatLeftHomologyData.i h) =
    CategoryTheory.CategoryStruct.comp (groupCohomology.iCocycles A 2)
      (CategoryTheory.CategoryStruct.comp (groupCohomology.cochainsIso₂ A).hom h)
-- Mathlib.Probability.Kernel.Composition.Lemmas
MeasureTheory.Measure.parallelComp_comp_compProd : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {μ : MeasureTheory.Measure α} {κ : ProbabilityTheory.Kernel α β}
  [ProbabilityTheory.IsSFiniteKernel κ] {η : ProbabilityTheory.Kernel β γ} [ProbabilityTheory.IsSFiniteKernel η],
  (μ.compProd κ).bind ⇑(ProbabilityTheory.Kernel.id.parallelComp η) = μ.compProd (η.comp κ)
-- Mathlib.Data.Set.UnionLift
Set.iUnionLift_mk : ∀ {α : Type u_1} {ι : Sort u_3} {β : Sort u_2} {S : ι → Set α} {f : (i : ι) → ↑(S i) → β}
  {hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩} {T : Set α}
  {hT : T ⊆ Set.iUnion S} {i : ι} (x : ↑(S i)) (hx : ↑x ∈ T), Set.iUnionLift S f hf T hT ⟨↑x, hx⟩ = f i x
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.HasModel.le_iff_encode_le : ∀ {α : Type u} {inst : LE α} {inst_1 : LT α} {β : outParam (Type v)} {inst_2 : LE β} {inst_3 : LT β}
  {inst_4 : Std.PRange.UpwardEnumerable β} {inst_5 : Std.PRange.LawfulUpwardEnumerable β}
  {inst_6 : Std.PRange.LawfulUpwardEnumerableLE β} {inst_7 : Std.PRange.LawfulUpwardEnumerableLT β}
  [self : HasModel✝ α β] {x y : α}, x ≤ y ↔ HasModel.encode✝ x ≤ HasModel.encode✝ y
-- Mathlib.Data.Set.Function
Set.surjOn_univ_of_subsingleton_nonempty : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} [Subsingleton β] [Nonempty β],
  Set.SurjOn f s Set.univ ↔ s.Nonempty
-- Mathlib.Combinatorics.Matroid.Map
Matroid.instNonemptyMap : ∀ {α : Type u_1} {β : Type u_2} {M : Matroid α} [M.Nonempty] {f : α → β} (hf : Set.InjOn f M.E), (M.map f hf).Nonempty
-- Mathlib.NumberTheory.ClassNumber.Finite
ClassGroup.normBound.congr_simp : ∀ {R : Type u_1} {S : Type u_2} [inst : EuclideanDomain R] [inst_1 : CommRing S] [inst_2 : IsDomain S]
  [inst_3 : Algebra R S] (abv abv_1 : AbsoluteValue R ℤ),
  abv = abv_1 →
    ∀ {ι : Type u_5} {inst_4 : DecidableEq ι} [inst_5 : DecidableEq ι] [inst_6 : Fintype ι]
      (bS bS_1 : Module.Basis ι R S), bS = bS_1 → ClassGroup.normBound abv bS = ClassGroup.normBound abv_1 bS_1
-- Mathlib.LinearAlgebra.Eigenspace.Semisimple
Module.End.IsFinitelySemisimple.maxGenEigenspace_eq_eigenspace : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {f : Module.End R M}, f.IsFinitelySemisimple → ∀ (μ : R), f.maxGenEigenspace μ = f.eigenspace μ
-- Mathlib.SetTheory.Cardinal.Finite
Nat.subtype_card : ∀ {α : Type u_1} {p : α → Prop} (s : Finset α), (∀ (x : α), x ∈ s ↔ p x) → Nat.card { x // p x } = s.card
-- Mathlib.Algebra.Order.Group.PosPart
leOnePart_def : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : DivInvMonoid α] (a : α), a⁻ᵐ = a⁻¹ ⊔ 1
-- Mathlib.CategoryTheory.Products.Basic
/-- Construct a morphism in a product category by giving its constituent components.
This constructor should be preferred over `Prod.mk`, because Lean infers better the
source and target of the resulting morphism.  -/
CategoryTheory.Prod.mkHom : {C : Type u₁} →
  [inst : CategoryTheory.CategoryStruct.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.CategoryStruct.{v₂, u₂} D] →
        {X₁ X₂ : C} → {Y₁ Y₂ : D} → (X₁ ⟶ X₂) → (Y₁ ⟶ Y₂) → ((X₁, Y₁) ⟶ (X₂, Y₂))
-- Mathlib.Analysis.Normed.Operator.Completeness
/-- Let `s` be a bounded set in the space of continuous (semi)linear maps `E →SL[σ] F` taking values
in a proper space. Then `s` interpreted as a set in the space of maps `E → F` with topology of
pointwise convergence is precompact: its closure is a compact set.  -/
ContinuousLinearMap.isCompact_closure_image_coe_of_bounded : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {F : Type u_4} [inst : NormedAddCommGroup F] [inst_1 : NontriviallyNormedField 𝕜]
  [inst_2 : NontriviallyNormedField 𝕜₂] [inst_3 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {E' : Type u_6}
  [inst_4 : SeminormedAddCommGroup E'] [inst_5 : NormedSpace 𝕜 E'] [inst_6 : RingHomIsometric σ₁₂] [ProperSpace F]
  {s : Set (E' →SL[σ₁₂] F)}, Bornology.IsBounded s → IsCompact (closure (DFunLike.coe '' s))
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.map_eq_zero_iff : ∀ {β : Type v} {α : Type u_1} {f : α → β} {v : WithBot α} [inst : Zero β], WithBot.map f v = 0 ↔ ∃ x, v = ↑x ∧ f x = 0
-- Mathlib.Tactic.GCongr.Core
Mathlib.Tactic.GCongr.GCongrHyp.mk : ℕ → ℕ → ℕ → List (Option ℕ) → Bool → Mathlib.Tactic.GCongr.GCongrHyp
-- Mathlib.CategoryTheory.Limits.Shapes.Products
/-- The isomorphism `∏ᶜ (fun j => X.obj (Discrete.mk j)) ≅ limit X`.  -/
CategoryTheory.Limits.Pi.isoLimit : {α : Type w₂} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      (X : CategoryTheory.Functor (CategoryTheory.Discrete α) C) →
        [inst_1 : CategoryTheory.Limits.HasProduct fun j => X.obj { as := j }] →
          [inst_2 : CategoryTheory.Limits.HasLimit X] → (∏ᶜ fun j => X.obj { as := j }) ≅ CategoryTheory.Limits.limit X
-- Mathlib.Analysis.Normed.Field.Krasner
IsKrasner.mk : ∀ {K : Type u_1} {L : Type u_2} [inst : NormedField L] [inst_1 : Field K] [inst_2 : Algebra K L],
  (∀ {x y : L},
      IsSeparable K x →
        (Polynomial.map (algebraMap K L) (minpoly K x)).Splits →
          IsIntegral K y → (∀ (x' : L), IsConjRoot K x x' → x ≠ x' → ‖x - y‖ < ‖x - x'‖) → x ∈ K⟮y⟯) →
    IsKrasner K L
-- Mathlib.Data.Finset.Basic
/-- The disjoint union of finsets is a sum  -/
Equiv.Finset.disjUnionEquiv : {α : Type u_1} → [DecidableEq α] → (s t : Finset α) → (h : Disjoint s t) → ↥s ⊕ ↥t ≃ ↥(s.disjUnion t h)
-- Init.Data.Array.Attach
Array.attach_map : ∀ {α : Type u_1} {β : Type u_2} {xs : Array α} {f : α → β},
  (Array.map f xs).attach =
    Array.map
      (fun x =>
        match x with
        | ⟨x, h⟩ => ⟨f x, ⋯⟩)
      xs.attach
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
/-- The constant function as an `AffineMap`.  -/
AffineMap.const : (k : Type u_1) →
  {V1 : Type u_2} →
    (P1 : Type u_3) →
      {V2 : Type u_4} →
        {P2 : Type u_5} →
          [inst : Ring k] →
            [inst_1 : AddCommGroup V1] →
              [inst_2 : Module k V1] →
                [inst_3 : AddTorsor V1 P1] →
                  [inst_4 : AddCommGroup V2] → [inst_5 : Module k V2] → [inst_6 : AddTorsor V2 P2] → P2 → P1 →ᵃ[k] P2
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
MeasureTheory.ProbabilityMeasure.coeFn_univ : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] (ν : MeasureTheory.ProbabilityMeasure Ω), ν Set.univ = 1
-- Mathlib.AlgebraicGeometry.Properties
AlgebraicGeometry.isReduced_of_isReduced_stalk : ∀ (X : AlgebraicGeometry.Scheme) [∀ (x : ↥X), IsReduced ↑(X.presheaf.stalk x)], AlgebraicGeometry.IsReduced X
-- Mathlib.CategoryTheory.Abelian.RightDerived
CategoryTheory.InjectiveResolution.toRightDerivedZero'_comp_iCycles_assoc : ∀ {D : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} D] [inst_1 : CategoryTheory.Abelian D] {C : Type u_2}
  [inst_2 : CategoryTheory.Category.{v_2, u_2} C] [inst_3 : CategoryTheory.Abelian C] {X : C}
  (P : CategoryTheory.InjectiveResolution X) (F : CategoryTheory.Functor C D) [inst_4 : F.Additive] {Z : D}
  (h : ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj P.cocomplex).X 0 ⟶ Z),
  CategoryTheory.CategoryStruct.comp (P.toRightDerivedZero' F)
      (CategoryTheory.CategoryStruct.comp (((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj P.cocomplex).iCycles 0)
        h) =
    CategoryTheory.CategoryStruct.comp (F.map (P.ι.f 0)) h
-- Mathlib.RingTheory.RingHom.Smooth
RingHom.FormallySmooth.holdsForLocalizationAway : RingHom.HoldsForLocalizationAway @RingHom.FormallySmooth
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
/-- The chosen convolution between the functors. Denoted `F ⊛ G`.  -/
CategoryTheory.MonoidalCategory.DayConvolution.convolution : {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 : CategoryTheory.Functor C V) →
              [self : CategoryTheory.MonoidalCategory.DayConvolution F G] → CategoryTheory.Functor C V
-- Mathlib.Topology.Algebra.Valued.LocallyCompact
Valued.integer.properSpace_iff_completeSpace_and_isDiscreteValuationRing_integer_and_finite_residueField : ∀ {K : Type u_1} {Γ₀ : Type u_2} [inst : Field K] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] [inst_2 : Valued K Γ₀]
  [inst_3 : Valued.v.RankOne],
  ProperSpace K ↔ CompleteSpace K ∧ IsDiscreteValuationRing ↥(Valued.integer K) ∧ Finite (Valued.ResidueField K)
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.String.Pos.Raw.utf8GetAux.match_1.eq_1 : ∀ (motive : List Char → String.Pos.Raw → String.Pos.Raw → Sort u_1) (x x_1 : String.Pos.Raw)
  (h_1 : (x x_2 : String.Pos.Raw) → motive [] x x_2)
  (h_2 : (c : Char) → (cs : List Char) → (i p : String.Pos.Raw) → motive (c :: cs) i p),
  (match [], x, x_1 with
    | [], x, x_2 => h_1 x x_2
    | c :: cs, i, p => h_2 c cs i p) =
    h_1 x x_1