mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Category.CommBialgCat
CommBialgCat.ofHom_comp : ∀ {R : Type u} [inst : CommRing R] {X Y Z : Type v} [inst_1 : CommRing X] [inst_2 : Bialgebra R X] [inst_3 : CommRing Y]
  [inst_4 : Bialgebra R Y] [inst_5 : CommRing Z] [inst_6 : Bialgebra R Z] (f : X →ₐc[R] Y) (g : Y →ₐc[R] Z),
  CommBialgCat.ofHom (g.comp f) = CategoryTheory.CategoryStruct.comp (CommBialgCat.ofHom f) (CommBialgCat.ofHom g)
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.smulRight_apply : ∀ {M₁ : Type u_4} [inst : TopologicalSpace M₁] [inst_1 : AddCommMonoid M₁] {M₂ : Type u_6}
  [inst_2 : TopologicalSpace M₂] [inst_3 : AddCommMonoid M₂] {R : Type u_9} {S : Type u_10} [inst_4 : Semiring R]
  [inst_5 : Semiring S] [inst_6 : Module R M₁] [inst_7 : Module R M₂] [inst_8 : Module R S] [inst_9 : Module S M₂]
  [inst_10 : IsScalarTower R S M₂] [inst_11 : TopologicalSpace S] [inst_12 : ContinuousSMul S M₂] {c : M₁ →L[R] S}
  {f : M₂} {x : M₁}, (c.smulRight f) x = c x • f
-- Mathlib.Data.NNReal.Defs
NNReal.inv_lt_inv : ∀ {x y : NNReal}, x ≠ 0 → x < y → y⁻¹ < x⁻¹
-- Mathlib.Order.Hom.Lattice
InfHom.coe_inf : ∀ {α : Type u_2} {β : Type u_3} [inst : Min α] [inst_1 : SemilatticeInf β] (f g : InfHom α β), ⇑(f ⊓ g) = ⇑f ⊓ ⇑g
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.w_prod_snd : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {C' : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C'] {D' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D'] (S : D) (S' : D') (T : CategoryTheory.Functor C D)
  (T' : CategoryTheory.Functor C' D') {X Y : CategoryTheory.StructuredArrow (S, S') (T.prod T')} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp X.hom.2 (T'.map (CategoryTheory.StructuredArrow.Hom.right f).2) = Y.hom.2
-- Init.Data.String.Basic
/-- Constructs a valid position `s` from a position, panicking if the position is not valid.  -/
String.Slice.pos! : (s : String.Slice) → String.Pos.Raw → s.Pos
-- Mathlib.CategoryTheory.Limits.Shapes.Terminal
/-- Notation for the terminal object in `C`  -/
CategoryTheory.Limits.«term⊤__» : Lean.ParserDescr
-- Mathlib.Order.Notation
/-- Syntax typeclass for Heyting implication `⇨`.  -/
HImp : Type u_1 → Type u_1
-- Lean.Meta.Injective
_private.Lean.Meta.Injective.0.Lean.Meta.mkHInjType?.mkArgs2 : Lean.ConstructorVal →
  Array Lean.Expr →
    (Array Lean.Expr → Lean.MetaM (Option Lean.Meta.MkHInjTypeResult✝)) →
      ℕ → Lean.Expr → Array Lean.Expr → Lean.MetaM (Option Lean.Meta.MkHInjTypeResult✝)
-- Mathlib.CategoryTheory.Preadditive.Projective.Resolution
/-- the chain complex must have homology  -/
CategoryTheory.ProjectiveResolution.hasHomology : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {Z : C} (self : CategoryTheory.ProjectiveResolution Z) (i : ℕ),
  HomologicalComplex.HasHomology self.complex i
-- Mathlib.FieldTheory.IsAlgClosed.Basic
IsAlgClosed.card_aroots_eq_natDegree : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : Field B] [IsAlgClosed B] [inst_3 : Algebra A B]
  [FaithfulSMul A B] {p : Polynomial A}, (p.aroots B).card = p.natDegree
-- Mathlib.Algebra.Polynomial.Sequence
/-- `S i` has degree `i`.  -/
Polynomial.Sequence.degree_eq : ∀ {R : Type u_1} [inst : Semiring R] (S : Polynomial.Sequence R) (i : ℕ), (↑S i).degree = ↑i
-- Mathlib.RingTheory.Ideal.Lattice
Ideal.mem_inf : ∀ {R : Type u} [inst : Semiring R] {I J : Ideal R} {x : R}, x ∈ I ⊓ J ↔ x ∈ I ∧ x ∈ J
-- Mathlib.Algebra.Group.Action.Equidecomp
Equidecomp.symm_involutive : ∀ {X : Type u_1} {G : Type u_2} [inst : Group G] [inst_1 : MulAction G X], Function.Involutive Equidecomp.symm
-- Init.Data.UInt.Bitwise
UInt64.ofFin_shiftLeft_mod : ∀ (a b : Fin UInt64.size), UInt64.ofFin (a <<< (b % 64)) = UInt64.ofFin a <<< UInt64.ofFin b
-- Lean.Meta.Iterator
Lean.Meta.Iterator.mk.injEq : ∀ {α : Type} (next next_1 : Lean.MetaM (Option (α × Lean.Meta.SavedState))),
  ({ next := next } = { next := next_1 }) = (next = next_1)
-- Init.Internal.Order.Lemmas
Lean.Order.Array.monotone_flatMapM : ∀ {m : Type u → Type v} [inst : Monad m] [inst_1 : (α : Type u) → Lean.Order.PartialOrder (m α)] [Lean.Order.MonoBind m]
  {α β : Type u} {γ : Type w} [inst_3 : Lean.Order.PartialOrder γ] (f : γ → α → m (Array β)) (xs : Array α),
  Lean.Order.monotone f → Lean.Order.monotone fun x => Array.flatMapM (f x) xs
-- Mathlib.Computability.Language
/-- The Kleene star of a language `L` is the set of all strings which can be written by
concatenating strings from `L`.  -/
Language.instKStar : {α : Type u_1} → KStar (Language α)
-- Mathlib.Topology.FiberBundle.Basic
/-- Extended version of the local trivialization of a fiber bundle constructed from core,
registering additionally in its type that it is a local bundle trivialization.  -/
FiberBundleCore.localTriv : {ι : Type u_1} →
  {B : Type u_2} →
    {F : Type u_3} →
      [inst : TopologicalSpace B] →
        [inst_1 : TopologicalSpace F] → (Z : FiberBundleCore ι B F) → ι → Bundle.Trivialization F Z.proj
-- Mathlib.Analysis.Seminorm
/-- A seminorm is uniformly continuous if `p.closedBall 0 r ∈ 𝓝 0` for *all* `r > 0`.
Over a `NontriviallyNormedField` it is actually enough to check that this is true
for *some* `r`, see `Seminorm.uniformContinuous'`.  -/
Seminorm.uniformContinuous_of_forall' : ∀ {𝕝 : Type u_6} {E : Type u_7} [inst : SeminormedRing 𝕝] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕝 E]
  [inst_3 : UniformSpace E] [IsUniformAddGroup E] {p : Seminorm 𝕝 E},
  (∀ r > 0, p.closedBall 0 r ∈ nhds 0) → UniformContinuous ⇑p
-- Mathlib.Data.PNat.Prime
/-- Primality predicate for `ℕ+`, defined in terms of `Nat.Prime`.  -/
PNat.Prime : ℕ+ → Prop
-- Mathlib.Logic.Function.Basic
Function.onFun_apply : ∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : β → β → γ) (g : α → β) (a b : α),
  Function.onFun f g a b = f (g a) (g b)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.isEmpty_map : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} {γ : α → Type w}
  [Std.TransCmp cmp] {f : (a : α) → β a → γ a}, (Std.DTreeMap.Raw.map f t).isEmpty = t.isEmpty
-- Mathlib.Topology.EMetricSpace.Basic
/-- A compact set in an emetric space is separable, i.e., it is the closure of a countable set.  -/
EMetric.countable_closure_of_compact : ∀ {γ : Type w} [inst : EMetricSpace γ] {s : Set γ}, IsCompact s → ∃ t ⊆ s, t.Countable ∧ s = closure t
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.HomEquiv.ρ_hom_inv : ∀ {C : Type u} {X : CategoryTheory.FreeMonoidalCategory C},
  CategoryTheory.FreeMonoidalCategory.HomEquiv
    ((CategoryTheory.FreeMonoidalCategory.Hom.ρ_hom X).comp (CategoryTheory.FreeMonoidalCategory.Hom.ρ_inv X))
    (CategoryTheory.FreeMonoidalCategory.Hom.id (X.tensor CategoryTheory.FreeMonoidalCategory.unit))
-- Mathlib.CategoryTheory.Subobject.Limits
CategoryTheory.Limits.factorThruImageSubobject_comp_self_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasImage f] {W W' : C} (k : W ⟶ W') (k' : W' ⟶ X)
  (h :
    (CategoryTheory.Limits.imageSubobject f).Factors
      (CategoryTheory.CategoryStruct.comp k (CategoryTheory.CategoryStruct.comp k' f))),
  (CategoryTheory.Limits.imageSubobject f).factorThru
      (CategoryTheory.CategoryStruct.comp k (CategoryTheory.CategoryStruct.comp k' f)) h =
    CategoryTheory.CategoryStruct.comp k
      (CategoryTheory.CategoryStruct.comp k' (CategoryTheory.Limits.factorThruImageSubobject f))
-- Mathlib.FieldTheory.SeparableDegree
Polynomial.rootOfSplits.congr_simp : ∀ {R : Type u_1} [inst : CommRing R] {f f_1 : Polynomial R} (e_f : f = f_1) (hf : f.Splits) (hfd : f.degree ≠ 0),
  Polynomial.rootOfSplits hf hfd = Polynomial.rootOfSplits ⋯ ⋯
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F : C ⥤ D` creates colimits, then `F.op : Cᵒᵖ ⥤ Dᵒᵖ` creates limits.  -/
CategoryTheory.Limits.createsLimitsOfSizeOp : {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.CreatesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F] →
            CategoryTheory.CreatesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.op
-- Mathlib.Algebra.Group.Subgroup.Ker
/-- The range of an injective additive group homomorphism is isomorphic to its
domain.  -/
AddMonoidHom.ofInjective : {G : Type u_1} →
  [inst : AddGroup G] → {N : Type u_5} → [inst_1 : AddGroup N] → {f : G →+ N} → Function.Injective ⇑f → G ≃+ ↥f.range
-- Mathlib.Order.Interval.Set.SuccOrder
Set.Ici.pred_eq_of_not_isMin : ∀ {J : Type u_1} [inst : PartialOrder J] [inst_1 : PredOrder J] {j : J} {i : ↑(Set.Ici j)} (hi : ¬IsMin i),
  Order.pred i = ⟨Order.pred ↑i, ⋯⟩
-- Lean.Data.Lsp.Extra
Lean.Lsp.instFromJsonDependencyBuildMode.fromJson : Lean.Json → Except String Lean.Lsp.DependencyBuildMode
-- Mathlib.Data.Countable.Defs
instCountableNat : Countable ℕ
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
/-- **Alias** of `tprod_eq_tprod_sdiff_singleton`.

---

If `f b = 1`, then the product of `f a` with `a ∈ s` is the same as the product of `f a` for
`a ∈ s ∖ {b}`.  -/
tprod_eq_tprod_diff_singleton : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α} (s : Set β) {b : β},
  f b = 1 → ∏' (a : ↑s), f ↑a = ∏' (a : ↑(s \ {b})), f ↑a
-- Mathlib.Order.Atoms
/-- A simple `BoundedOrder` induces a preorder. This is not an instance to prevent loops.  -/
IsSimpleOrder.preorder : {α : Type u_4} → [inst : LE α] → [inst_1 : BoundedOrder α] → [IsSimpleOrder α] → Preorder α
-- Init.Data.Fin.Lemmas
Fin.cast_refl : ∀ (n : ℕ) (h : n = n), Fin.cast h = id
-- Mathlib.Combinatorics.SimpleGraph.Bipartite
_private.Mathlib.Combinatorics.SimpleGraph.Bipartite.0.SimpleGraph.bipartiteDoubleCover.match_1.eq_1 : ∀ {V : Type u_1} (motive : V ⊕ V → V ⊕ V → Sort u_2) (v' w' : V) (h_1 : (v' w' : V) → motive (Sum.inl v') (Sum.inr w'))
  (h_2 : (v' w' : V) → motive (Sum.inr v') (Sum.inl w')) (h_3 : (x x_1 : V ⊕ V) → motive x x_1),
  (match Sum.inl v', Sum.inr w' with
    | Sum.inl v', Sum.inr w' => h_1 v' w'
    | Sum.inr v', Sum.inl w' => h_2 v' w'
    | x, x_1 => h_3 x x_1) =
    h_1 v' w'
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.ExcenterExists.touchpointWeights_restrict : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] {s : Affine.Simplex ℝ P n} {signs : Finset (Fin (n + 1))},
  s.ExcenterExists signs →
    ∀ (S : AffineSubspace ℝ P) (hS : affineSpan ℝ (Set.range s.points) ≤ S),
      (s.restrict S hS).touchpointWeights signs = s.touchpointWeights signs
-- Mathlib.MeasureTheory.Category.MeasCat
MeasCat.of.sizeOf_spec : ∀ (carrier : Type u) [str : MeasurableSpace carrier],
  sizeOf { carrier := carrier, str := str } = 1 + sizeOf carrier + sizeOf str
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
hasMFDerivWithinAt_fst : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] (s : Set (M × M')) (x : M × M'),
  HasMFDerivAt[s] Prod.fst x (ContinuousLinearMap.fst 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2))
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
IsUniformGroup.cauchy_iff_tendsto_swapped : ∀ {G : Type u_4} [inst : Group G] [inst_1 : UniformSpace G] [IsUniformGroup G] (𝓕 : Filter G),
  Cauchy 𝓕 ↔ 𝓕.NeBot ∧ Filter.Tendsto (fun p => p.2 / p.1) (𝓕 ×ˢ 𝓕) (nhds 1)
-- Mathlib.Algebra.Category.Semigrp.Basic
MagmaCat.instConcreteCategoryMulHomCarrier.eq_1 : MagmaCat.instConcreteCategoryMulHomCarrier =
  { hom := fun {X Y} => MagmaCat.Hom.hom', ofHom := fun {X Y} => MagmaCat.Hom.mk✝,
    hom_ofHom := @MagmaCat.instConcreteCategoryMulHomCarrier._proof_1,
    ofHom_hom := @MagmaCat.instConcreteCategoryMulHomCarrier._proof_2,
    id_apply := @MagmaCat.instConcreteCategoryMulHomCarrier._proof_3,
    comp_apply := @MagmaCat.instConcreteCategoryMulHomCarrier._proof_4 }
-- Mathlib.AlgebraicGeometry.Properties
AlgebraicGeometry.map_injective_of_isIntegral : ∀ (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsIntegral X] {U V : X.Opens} (i : U ⟶ V) [H : Nonempty ↥↑U],
  Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (X.presheaf.map i.op))
-- Mathlib.Analysis.Analytic.Composition
/-- Version of `CPolynomialAt.comp` where point equality is a separate hypothesis.  -/
CPolynomialAt.comp_of_eq : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {g : F → G} {f : E → F} {y : F} {x : E},
  CPolynomialAt 𝕜 g y → CPolynomialAt 𝕜 f x → f x = y → CPolynomialAt 𝕜 (g ∘ f) x
-- Mathlib.Algebra.Polynomial.Basic
/-- **Alias** of `Polynomial.support_trinomial_subset`. -/
Polynomial.support_trinomial' : ∀ {R : Type u} [inst : Semiring R] (k m n : ℕ) (x y z : R),
  (Polynomial.C x * Polynomial.X ^ k + Polynomial.C y * Polynomial.X ^ m + Polynomial.C z * Polynomial.X ^ n).support ⊆
    {k, m, n}
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.insertMany_list_singleton : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α],
  m.WF → ∀ {k : α} {v : β}, m.insertMany [(k, v)] = m.insert k v
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
/-- In a C⋆-algebra, commuting nonnegative elements have nonnegative products.  -/
Commute.mul_nonneg : ∀ {A : Type u_1} [inst : NonUnitalRing A] [inst_1 : PartialOrder A] [inst_2 : StarRing A] [StarOrderedRing A]
  [inst_4 : TopologicalSpace A] [inst_5 : Module ℝ A] [inst_6 : IsScalarTower ℝ A A] [inst_7 : SMulCommClass ℝ A A]
  [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] {a b : A},
  0 ≤ a → 0 ≤ b → Commute a b → 0 ≤ a * b
-- Mathlib.Order.CompactlyGenerated.Basic
iSupIndep_sUnion_of_directed : ∀ {α : Type u_2} [inst : CompleteLattice α] [IsCompactlyGenerated α] {s : Set (Set α)},
  DirectedOn (fun x1 x2 => x1 ⊆ x2) s → (∀ a ∈ s, sSupIndep a) → sSupIndep (⋃₀ s)
-- Init.Data.List.Lemmas
List.length_eq_zero_iff : ∀ {α : Type u_1} {l : List α}, l.length = 0 ↔ l = []
-- Lean.Elab.InfoTree.Types
/-- Dynamic info for custom use cases.  -/
Lean.Elab.CustomInfo : Type
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.restrictScalarsEquivalenceOfRingEquiv_unitIso : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] (e : R ≃+* S),
  (ModuleCat.restrictScalarsEquivalenceOfRingEquiv e).unitIso =
    (ModuleCat.restrictScalarsId S).symm ≪≫ ModuleCat.restrictScalarsComp' (↑e.symm) e.toRingHom (RingHom.id S) ⋯
-- Mathlib.Topology.VectorBundle.Basic
Bundle.Trivialization.continuousLinearEquivAt.congr_simp : ∀ (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : NontriviallyNormedField R]
  [inst_1 : (x : B) → AddCommMonoid (E x)] [inst_2 : (x : B) → Module R (E x)] [inst_3 : NormedAddCommGroup F]
  [inst_4 : NormedSpace R F] [inst_5 : TopologicalSpace B] [inst_6 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_7 : (x : B) → TopologicalSpace (E x)] [inst_8 : FiberBundle F E]
  (e e_1 : Bundle.Trivialization F Bundle.TotalSpace.proj) (e_e : e = e_1) [inst_9 : Bundle.Trivialization.IsLinear R e]
  (b : B) (hb : b ∈ e.baseSet),
  Bundle.Trivialization.continuousLinearEquivAt R e b hb = Bundle.Trivialization.continuousLinearEquivAt R e_1 b ⋯
-- Mathlib.CategoryTheory.Category.Quiv
CategoryTheory.Quiv.adj_homEquiv : ∀ {V C : Type u} [inst : Quiver V] [inst_1 : CategoryTheory.Category.{max u v, u} C],
  CategoryTheory.Quiv.adj.homEquiv (CategoryTheory.Quiv.of V) (CategoryTheory.Cat.of C) =
    (CategoryTheory.Cat.Hom.equivFunctor (CategoryTheory.Cat.of (CategoryTheory.Paths V))
          (CategoryTheory.Cat.of C)).trans
      CategoryTheory.Quiv.pathsEquiv
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.induction : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] {motive : AddMonoidAlgebra R M → Prop} (x : AddMonoidAlgebra R M),
  motive 0 →
    (∀ (m : M) (r : R) (x : AddMonoidAlgebra R M),
        m ∉ x.coeff.support → r ≠ 0 → motive x → motive (AddMonoidAlgebra.single m r + x)) →
      motive x
-- Mathlib.RingTheory.SimpleModule.WedderburnArtin
/-- The **Wedderburn–Artin Theorem**, algebra form: a semisimple algebra is isomorphic to a
product of matrix algebras over the opposite of the endomorphism algebras of its simple modules.  -/
IsSemisimpleRing.exists_algEquiv_pi_matrix_end_mulOpposite : ∀ (R₀ : Type u_1) (R : Type u) [inst : CommSemiring R₀] [inst_1 : Ring R] [inst_2 : Algebra R₀ R] [IsSemisimpleRing R],
  ∃ n S d,
    (∀ (i : Fin n), IsSimpleModule R ↥(S i)) ∧
      (∀ (i : Fin n), NeZero (d i)) ∧
        Nonempty (R ≃ₐ[R₀] (i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) (Module.End R ↥(S i))ᵐᵒᵖ)
-- Mathlib.AlgebraicGeometry.Gluing
/-- (Implementation detail)
The transition map `V i j ⟶ V j i` in the glue data associated to a locally directed diagram.  -/
AlgebraicGeometry.Scheme.IsLocallyDirected.t : {J : Type w} →
  [inst : CategoryTheory.Category.{v, w} J] →
    (F : CategoryTheory.Functor J AlgebraicGeometry.Scheme) →
      [inst_1 : ∀ {i j : J} (f : i ⟶ j), AlgebraicGeometry.IsOpenImmersion (F.map f)] →
        [(F.comp AlgebraicGeometry.Scheme.forget).IsLocallyDirected] →
          [Quiver.IsThin J] →
            (i j : J) →
              ↑(AlgebraicGeometry.Scheme.IsLocallyDirected.V F i j) ⟶
                ↑(AlgebraicGeometry.Scheme.IsLocallyDirected.V F j i)
-- Init.Data.Nat.Bitwise.Lemmas
Nat.testBit_two_pow_mul : ∀ {i a j : ℕ}, (2 ^ i * a).testBit j = (decide (j ≥ i) && a.testBit (j - i))
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsPath.length_lt : ∀ {V : Type u} {G : SimpleGraph V} [inst : Fintype V] {u v : V} {p : G.Walk u v}, p.IsPath → p.length < Fintype.card V
-- Mathlib.FieldTheory.Minpoly.Basic
/-- If `a` strictly divides the minimal polynomial of `x`, then `x` cannot be a root for `a`.  -/
minpoly.aeval_ne_zero_of_dvdNotUnit_minpoly : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : Ring B] [inst_2 : Algebra A B] {x : B} {a : Polynomial A},
  IsIntegral A x → a.Monic → DvdNotUnit a (minpoly A x) → (Polynomial.aeval x) a ≠ 0
-- Lean.Meta.Sym.LitValues
Lean.Meta.Sym.getInt8Value? : Lean.Expr → OptionT Id Int8
-- Mathlib.Analysis.Convex.Between
Wbtw.trans_left : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] [IsOrderedRing R] {w x y z : P},
  Wbtw R w y z → Wbtw R w x y → Wbtw R w x z
-- Init.Omega.Coeffs
Lean.Omega.Coeffs.dot_sdiv_left : ∀ (xs ys : Lean.Omega.Coeffs) {d : ℤ}, d ∣ ↑xs.gcd → (xs.sdiv d).dot ys = xs.dot ys / d
-- Init.Data.UInt.Lemmas
UInt32.toFin_mod : ∀ (a b : UInt32), (a % b).toFin = a.toFin % b.toFin
-- Lean.Compiler.IR.Basic
Lean.IR.LocalContext.isJP : Lean.IR.LocalContext → Lean.IR.Index → Bool
-- Mathlib.Algebra.Category.MonCat.Basic
/-- Typecheck an `AddMonoidHom` as a morphism in `AddCommMonCat`.  -/
AddCommMonCat.ofHom : {X Y : Type u} →
  [inst : AddCommMonoid X] → [inst_1 : AddCommMonoid Y] → (X →+ Y) → (AddCommMonCat.of X ⟶ AddCommMonCat.of Y)
-- Init.Data.Vector.Count
Vector.countP_empty : ∀ {α : Type u_1} {p : α → Bool}, Vector.countP p #v[] = 0
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.revAll_takeEndWhile : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.BackwardPattern pat] [String.Slice.Pattern.Model.LawfulBackwardPatternModel pat]
  {s : String.Slice}, (s.takeEndWhile pat).revAll pat = true
-- Mathlib.Data.Finset.SymmDiff
Finset.mem_symmDiff : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α} {a : α}, a ∈ symmDiff s t ↔ a ∈ s ∧ a ∉ t ∨ a ∈ t ∧ a ∉ s
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
/-- `biproduct f` computes the biproduct of a family of elements `f`. (It is defined as an
abbreviation for `limit (Discrete.functor f)`, so for most facts about `biproduct f`, you will
just use general facts about limits and colimits.)  -/
CategoryTheory.Limits.biproduct : {J : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] → (f : J → C) → [CategoryTheory.Limits.HasBiproduct f] → C
-- Mathlib.Logic.Equiv.PartialEquiv
/-- Create a copy of a `PartialEquiv` providing better definitional equalities.  -/
PartialEquiv.copy : {α : Type u_1} →
  {β : Type u_2} →
    (e : PartialEquiv α β) →
      (f : α → β) →
        ↑e = f → (g : β → α) → ↑e.symm = g → (s : Set α) → e.source = s → (t : Set β) → e.target = t → PartialEquiv α β
-- Mathlib.Geometry.Manifold.VectorField.Pullback
/-- The pullback of a `C^m` vector field by a `C^n` function with invertible derivative and
with `m + 1 ≤ n` is `C^m`.  -/
ContMDiff.mpullback_vectorField : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {E' : Type u_6} [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace 𝕜 E'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'}
  {V : (x : M') → TangentSpace I' x} {m n : WithTop ℕ∞} [CompleteSpace E] [inst_12 : IsManifold I 1 M]
  [inst_13 : IsManifold I' 1 M'],
  (ContMDiff I' I'.tangent m fun x => ⟨x, V x⟩) →
    ContMDiff I I' n f →
      (∀ (x : M), (mfderiv% f x).IsInvertible) →
        m + 1 ≤ n → ContMDiff I I.tangent m fun x => ⟨x, VectorField.mpullback I I' f V x⟩
-- Mathlib.Order.Fin.Tuple
Fin.strictMono_cons : ∀ {α : Type u_1} [inst : Preorder α] {n : ℕ} {f : Fin n → α} {a : α},
  StrictMono (Fin.cons a f) ↔ (∀ (j : Fin n), a < f j) ∧ StrictMono f
-- Mathlib.Algebra.BigOperators.Fin
Fin.sum_Ioi_cast : ∀ {M : Type u_2} [inst : AddCommMonoid M] {n m : ℕ} (h : n = m) (f : Fin m → M) (a : Fin n),
  ∑ i > Fin.cast h a, f i = ∑ i > a, f (Fin.cast h i)
-- Mathlib.Analysis.Normed.Lp.WithLp
WithLp.toLp_surjective : ∀ (p : ENNReal) {V : Type u_4}, Function.Surjective (WithLp.toLp p)
-- Mathlib.Combinatorics.Matroid.Circuit
Matroid.indep_iff_forall_subset_not_isCircuit : ∀ {α : Type u_1} {M : Matroid α} {I : Set α},
  autoParam (I ⊆ M.E) Matroid.indep_iff_forall_subset_not_isCircuit._auto_1 → (M.Indep I ↔ ∀ C ⊆ I, ¬M.IsCircuit C)
-- Mathlib.Analysis.Convex.Between
Wbtw.left_mem_affineSpan_of_right_ne : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R]
  [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P] {x y z : P},
  Wbtw R x y z → z ≠ y → x ∈ line[R, z, y]
-- Mathlib.RingTheory.Polynomial.RationalRoot
UniqueFactorizationMonoid.integer_of_integral : ∀ {A : Type u_1} {K : Type u_2} [inst : CommRing A] [IsDomain A] [UniqueFactorizationMonoid A] [inst_3 : Field K]
  [inst_4 : Algebra A K] [IsFractionRing A K] {x : K}, IsIntegral A x → IsLocalization.IsInteger A x