mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.mkSpanSingleton.congr_simp : ∀ {K : Type u_7} {L : Type u_8} {E : Type u_9} {F : Type u_10} [inst : DivisionRing K] [inst_1 : DivisionRing L]
  {σ : K →+* L} [inst_2 : AddCommGroup E] [inst_3 : Module K E] [inst_4 : AddCommGroup F] [inst_5 : Module L F]
  (x x_1 : E) (e_x : x = x_1) (y y_1 : F),
  y = y_1 → ∀ (hx : x ≠ 0), LinearPMap.mkSpanSingleton x y hx = LinearPMap.mkSpanSingleton x_1 y_1 ⋯
-- Mathlib.Algebra.Homology.HomologicalBicomplex
/-- Flip a complex of complexes over the diagonal,
exchanging the horizontal and vertical directions.
 -/
HomologicalComplex₂.flip : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {I₁ : Type u_2} →
        {I₂ : Type u_3} →
          {c₁ : ComplexShape I₁} → {c₂ : ComplexShape I₂} → HomologicalComplex₂ C c₁ c₂ → HomologicalComplex₂ C c₂ c₁
-- Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
CategoryTheory.IsCardinalFiltered.coeq_condition_assoc : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {κ : Cardinal.{w}} [hκ : Fact κ.IsRegular]
  [inst_1 : CategoryTheory.IsCardinalFiltered J κ] {K : Type v'} {j j' : J} (f : K → (j ⟶ j')) (hK : HasCardinalLT K κ)
  (k : K) {Z : J} (h : CategoryTheory.IsCardinalFiltered.coeq f hK ⟶ Z),
  CategoryTheory.CategoryStruct.comp (f k)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.IsCardinalFiltered.coeqHom f hK) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.IsCardinalFiltered.toCoeq f hK) h
-- Init.Data.Repr
instReprSum : {α : Type u_1} → {β : Type u_2} → [Repr α] → [Repr β] → Repr (α ⊕ β)
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.piCongrLeft'_symm_apply : ∀ {ι : Type u_7} {ι' : Type u_8} (R : ι → Type u_9) (e : ι ≃ ι') [inst : (i : ι) → NonUnitalNonAssocSemiring (R i)]
  (f : (b : ι') → R (e.symm b)) (x : ι), (RingEquiv.piCongrLeft' R e).symm f x = ⋯ ▸ f (e x)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.denote'.go.eq_def : ∀ {α : Type u_1} [inst : Lean.Grind.Semiring α] (ctx : Lean.Grind.CommRing.Context α) (m : Lean.Grind.CommRing.Mon)
  (acc : α),
  Lean.Grind.CommRing.Mon.denote'.go ctx m acc =
    match m with
    | Lean.Grind.CommRing.Mon.unit => acc
    | Lean.Grind.CommRing.Mon.mult pw m =>
      Lean.Grind.CommRing.Mon.denote'.go ctx m (acc * Lean.Grind.CommRing.Power.denote ctx pw)
-- Mathlib.NumberTheory.Padics.PadicIntegers
/-- The inverse of a `p`-adic integer with norm equal to `1` is also a `p`-adic integer.
Otherwise, the inverse is defined to be `0`.  -/
PadicInt.inv : {p : ℕ} → [hp : Fact (Nat.Prime p)] → ℤ_[p] → ℤ_[p]
-- Batteries.Data.AssocList
Batteries.AssocList.instForInProdOfMonad : {m : Type u_1 → Type u_2} → {α : Type u_3} → {β : Type u_4} → [Monad m] → ForIn m (Batteries.AssocList α β) (α × β)
-- Mathlib.Topology.Sheaves.EtaleSpace
TopCat.Presheaf.EtaleSpace.congr_simp : ∀ {X : TopCat} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {CC : C → Type v} {FC : C → C → Type w}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC]
  [inst_3 : CategoryTheory.Limits.HasColimits C] (F F_1 : TopCat.Presheaf C X), F = F_1 → F.EtaleSpace = F_1.EtaleSpace
-- Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
/-- The set of associated primes of a submodule.  -/
Submodule.associatedPrimes : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommSemiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → Submodule R M → Set (Ideal R)
-- Init.Data.Order.FactoriesExtra
Std.isGE_compare : ∀ {α : Type u} [inst : Ord α] [inst_1 : LE α] [Std.LawfulOrderOrd α] {a b : α}, (compare a b).isGE = true ↔ b ≤ a
-- Mathlib.Topology.Irreducible
/-- A set is irreducible if and only if for every cover by a finite collection of closed sets, it is
contained in one of the members of the collection.  -/
isIrreducible_iff_sUnion_isClosed : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X},
  IsIrreducible s ↔ ∀ (t : Finset (Set X)), (∀ z ∈ t, IsClosed z) → s ⊆ ⋃₀ ↑t → ∃ z ∈ t, s ⊆ z
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKeyD_union_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k fallback : α}, k ∉ m₂ → (m₁ ∪ m₂).getKeyD k fallback = m₁.getKeyD k fallback
-- Mathlib.MeasureTheory.Group.Arithmetic
MeasurableSet.inv : ∀ {G : Type u_2} [inst : Inv G] [inst_1 : MeasurableSpace G] [MeasurableInv G] {s : Set G},
  MeasurableSet s → MeasurableSet s⁻¹
-- Mathlib.Algebra.Order.Hom.MonoidWithZero
OrderMonoidWithZeroHom.ofClass_comp : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} {hα : Preorder α} {hα' : MulZeroOneClass α} {hβ : Preorder β}
  {hβ' : MulZeroOneClass β} {hγ : Preorder γ} {hγ' : MulZeroOneClass γ} (f : β →*₀o γ) (g : α →*₀o β),
  MonoidWithZeroHom.ofClass (f.comp g) = (MonoidWithZeroHom.ofClass f).comp (MonoidWithZeroHom.ofClass g)
-- Mathlib.LinearAlgebra.Matrix.SchurComplement
/-- If a block matrix is invertible and so is its bottom left element, then so is the corresponding
Schur complement.  -/
Matrix.invertibleOfFromBlocks₁₁Invertible : {m : Type u_2} →
  {n : Type u_3} →
    {α : Type u_4} →
      [inst : Fintype m] →
        [inst_1 : Fintype n] →
          [inst_2 : DecidableEq m] →
            [inst_3 : DecidableEq n] →
              [inst_4 : CommRing α] →
                (A : Matrix m m α) →
                  (B : Matrix m n α) →
                    (C : Matrix n m α) →
                      (D : Matrix n n α) →
                        [inst_5 : Invertible A] → [Invertible (Matrix.fromBlocks A B C D)] → Invertible (D - C * ⅟A * B)
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.add_eq_max' : ∀ {a b : Cardinal.{u_1}}, Cardinal.aleph0 ≤ b → a + b = max a b
-- Mathlib.GroupTheory.Submonoid.Center
AddSubsemigroup.centerToAddOpposite_apply_coe : ∀ {M : Type u_2} [inst : Add M] (r : ↥(AddSubsemigroup.center M)),
  ↑(AddSubsemigroup.centerToAddOpposite r) = AddOpposite.op ↑r
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.RoiSliceData.mk.injEq : ∀ {α : Type u} {β : Type v} [inst : Ord α] (treeMap : Std.DTreeMap.Internal.Impl α fun x => β) (range : Std.Roi α)
  (treeMap_1 : Std.DTreeMap.Internal.Impl α fun x => β) (range_1 : Std.Roi α),
  ({ treeMap := treeMap, range := range } = { treeMap := treeMap_1, range := range_1 }) =
    (treeMap = treeMap_1 ∧ range = range_1)
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey?_filter_key : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {f : α → Bool} {k : α}, (Std.HashMap.filter (fun k x => f k) m).getKey? k = Option.filter f (m.getKey? k)
-- Mathlib.Data.Nat.Multiplicity
/-- The multiplicity of `p` in `choose (n + k) k` is the number of carries when `k` and `n`
are added in base `p`. The set is expressed by filtering `Ico 1 b` where `b`
is any bound greater than `log p (n + k)`.  -/
Nat.Prime.emultiplicity_choose' : ∀ {p n k b : ℕ},
  Nat.Prime p →
    Nat.log p (n + k) < b →
      emultiplicity p ((n + k).choose k) = ↑{i ∈ Finset.Ico 1 b | p ^ i ≤ k % p ^ i + n % p ^ i}.card
-- Mathlib.CategoryTheory.Localization.DerivabilityStructure.Basic
CategoryTheory.LocalizerMorphism.instIsRightDerivabilityStructureOppositeOpOpOfIsLeftDerivabilityStructure : ∀ {C₁ : Type u₁} {C₂ : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂)
  [Φ.IsLeftDerivabilityStructure], Φ.op.IsRightDerivabilityStructure
-- Mathlib.Topology.Connected.PathConnected
/-- The canonical map which sends a path component of `X` (as a term of `ZerothHomotopy X`) to the
connected component containing it (as a term of `ConnectedComponents X`).  -/
ZerothHomotopy.toConnectedComponents : {X : Type u_1} → [inst : TopologicalSpace X] → ZerothHomotopy X → ConnectedComponents X
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isLittleO_irrefl : ∀ {α : Type u_1} {E'' : Type u_9} [inst : NormedAddCommGroup E''] {f'' : α → E''} {l : Filter α},
  (∃ᶠ (x : α) in l, f'' x ≠ 0) → ¬f'' =o[l] f''
-- Mathlib.Condensed.Light.Epi
LightCondSet.epi_iff_locallySurjective_on_lightProfinite : ∀ {X Y : LightCondSet} (f : X ⟶ Y),
  CategoryTheory.Epi f ↔
    ∀ (S : LightProfinite) (y : Y.obj.obj (Opposite.op S)),
      ∃ S' φ,
        ∃ (_ : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom φ)),
          ∃ x,
            (CategoryTheory.ConcreteCategory.hom (f.hom.app (Opposite.op S'))) x =
              (CategoryTheory.ConcreteCategory.hom (Y.obj.map (Opposite.op φ))) y
-- Mathlib.Algebra.Module.Presentation.Basic
/-- Given `relations : Relations A`, an `A`-module `M` and `solution : relations.Solution M`,
this property asserts that `solution` gives a presentation of `M` by generators and relations.  -/
Module.Relations.Solution.IsPresentation : {A : Type u} →
  [inst : Ring A] →
    {relations : Module.Relations A} →
      {M : Type v} → [inst_1 : AddCommGroup M] → [inst_2 : Module A M] → relations.Solution M → Prop
-- Std.Sync.Broadcast
_private.Std.Sync.Broadcast.0.Std.instReprSlot.repr : {α : Type} → [Repr α] → Std.Slot✝ α → ℕ → Std.Format
-- Mathlib.RepresentationTheory.Coinvariants
/-- Given a normal subgroup `S ≤ G`, a `G`-representation `A` induces a `G`-representation on
the `S`-coinvariants `A_S`.  -/
Rep.toCoinvariants : {k : Type u} →
  {G : Type v} →
    [inst : CommRing k] → [inst_1 : Group G] → Rep.{w, u, v} k G → (S : Subgroup G) → [S.Normal] → Rep.{w, u, v} k G
-- Mathlib.Algebra.Category.Grp.Kernels
/-- The kernel of a group homomorphism is a kernel in the categorical sense.  -/
AddCommGrpCat.kernelIsLimit : {G H : AddCommGrpCat} → (f : G ⟶ H) → CategoryTheory.Limits.IsLimit (AddCommGrpCat.kernelCone f)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getThenInsertIfNew?_fst : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β) {k : α}
  {v : β}, (Std.DHashMap.Internal.Raw₀.Const.getThenInsertIfNew? m k v).1 = Std.DHashMap.Internal.Raw₀.Const.get? m k
-- Std.Time.Time.Unit.Hour
Std.Time.Hour.instReprOrdinal : Repr Std.Time.Hour.Ordinal
-- Mathlib.Analysis.RCLike.Basic
_private.Mathlib.Analysis.RCLike.Basic.0.term𝓚 : Lean.ParserDescr
-- Mathlib.CategoryTheory.Monad.Products
CategoryTheory.algebraEquivUnder_counitIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C) [inst_1 : CategoryTheory.Limits.HasBinaryCoproducts C],
  (CategoryTheory.algebraEquivUnder X).counitIso =
    CategoryTheory.NatIso.ofComponents
      (fun f =>
        CategoryTheory.Under.isoMk
          (CategoryTheory.Iso.refl
            (((CategoryTheory.underToAlgebra X).comp (CategoryTheory.algebraToUnder X)).obj f).right)
          ⋯)
      ⋯
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
AddMonoidAlgebra.comapDomain.eq_1 : ∀ {R : Type u_3} {M : Type u_6} {N : Type u_7} [inst : Semiring R] (f : M → N) (hf : Function.Injective f)
  (x : AddMonoidAlgebra R N),
  AddMonoidAlgebra.comapDomain f hf x = AddMonoidAlgebra.ofCoeff (Finsupp.comapDomain f x.coeff ⋯)
-- Mathlib.Algebra.Group.Equiv.Opposite
/-- An additive monoid homomorphism `f : M →+ N` such that `f x` additively commutes
with `f y` for all `x, y` defines an additive monoid homomorphism to `Sᵃᵒᵖ`.  -/
AddMonoidHom.toOpposite : {M : Type u_3} →
  {N : Type u_4} →
    [inst : AddZeroClass M] →
      [inst_1 : AddZeroClass N] → (f : M →+ N) → (∀ (x y : M), AddCommute (f x) (f y)) → M →+ Nᵃᵒᵖ
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
tprod_mulIndicator_of_disjoint_on_mulSupport_of_mem : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] (s : γ → Set β)
  (f : β → α),
  ∀ i ∈ ⋃ d, s d,
    Pairwise (Function.onFun Disjoint fun j => s j ∩ Function.mulSupport f) → ∏' (d : γ), (s d).mulIndicator f i = f i
-- Mathlib.Topology.UniformSpace.AbstractCompletion
/-- The completion is a T₀ space.  -/
AbstractCompletion.separation : ∀ {α : Type u} [inst : UniformSpace α] (self : AbstractCompletion.{v, u} α), T0Space self.space
-- Mathlib.LinearAlgebra.TensorProduct.Subalgebra
/-- If `A` and `B` are subalgebras in a commutative algebra `S` over `R`,
there is the natural `R`-algebra homomorphism
`A ⊗[R] B →ₐ[R] A ⊔ B` induced by multiplication in `S`,
which is surjective (`Subalgebra.mulMap'_surjective`).  -/
Subalgebra.mulMap' : {R : Type u_1} →
  {S : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : CommSemiring S] → [inst_2 : Algebra R S] → (A B : Subalgebra R S) → TensorProduct R ↥A ↥B →ₐ[R] ↥(A ⊔ B)
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndepFun.indepFun_prodMk_prodMk₀ : ∀ {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : ι → Type u_10}
  {m : (i : ι) → MeasurableSpace (β i)} {f : (i : ι) → Ω → β i},
  ProbabilityTheory.iIndepFun f μ →
    (∀ (i : ι), AEMeasurable (f i) μ) →
      ∀ (i j k l : ι),
        i ≠ k → i ≠ l → j ≠ k → j ≠ l → ProbabilityTheory.IndepFun (fun a => (f i a, f j a)) (fun a => (f k a, f l a)) μ
-- Mathlib.GroupTheory.FreeGroup.Reduce
/-- If two words have a common maximal reduction, then they correspond to the same
element in the additive free group.  -/
FreeAddGroup.reduce.exact : ∀ {α : Type u_1} {L₁ L₂ : List (α × Bool)} [inst : DecidableEq α],
  FreeAddGroup.reduce L₁ = FreeAddGroup.reduce L₂ → FreeAddGroup.mk L₁ = FreeAddGroup.mk L₂
-- Mathlib.Algebra.Ring.Action.End
MulSemiringAction.toRingAut_apply : ∀ (G : Type u_1) (R : Type u_2) [inst : Group G] [inst_1 : Semiring R] [inst_2 : MulSemiringAction G R] (a : G),
  (MulSemiringAction.toRingAut G R) a = (MulSemiringAction.toRingEquiv G R) a
-- Mathlib.Analysis.Meromorphic.Divisor
/-- Eta-expanded form of `MeromorphicOn.divisor_comp_add_const_eq_divisor`

---

Divisors are invariant under translation.  -/
MeromorphicOn.divisor_fun_comp_add_const_eq_divisor : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {U : Set 𝕜} {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {c x : 𝕜} {f : 𝕜 → E},
  (MeromorphicOn.divisor (fun x => f (x + c)) U) (x - c) = (MeromorphicOn.divisor f (U + {c})) x
-- Mathlib.Analysis.Normed.Group.Continuity
ContinuousAt.nnnorm' : ∀ {α : Type u_1} {E : Type u_4} [inst : SeminormedGroup E] [inst_1 : TopologicalSpace α] {f : α → E} {a : α},
  ContinuousAt f a → ContinuousAt (fun x => ‖f x‖₊) a
-- Mathlib.Analysis.Asymptotics.Defs
Filter.Eventually.trans_isBigO : ∀ {α : Type u_1} {E : Type u_3} {G : Type u_5} {F' : Type u_7} [inst : Norm E] [inst_1 : Norm G]
  [inst_2 : SeminormedAddCommGroup F'] {l : Filter α} {f : α → E} {g : α → F'} {k : α → G},
  (∀ᶠ (x : α) in l, ‖f x‖ ≤ ‖g x‖) → g =O[l] k → f =O[l] k
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
/-- **Alias** of `SSet.yonedaEquiv_map`. -/
SSet.stdSimplex.yonedaEquiv_map : ∀ {n m : SimplexCategory} (f : n ⟶ m), SSet.yonedaEquiv (SSet.stdSimplex.map f) = SSet.stdSimplex.objEquiv.symm f
-- Mathlib.Data.Sum.Order
Sum.swap.eq_1 : ∀ {α : Type u_1} {β : Type u_2}, Sum.swap = Sum.elim Sum.inr Sum.inl
-- Mathlib.CategoryTheory.Monoidal.Bimon_
/-- The unit for the equivalence `Comon (Mon C) ≌ Mon (Comon C)`.  -/
CategoryTheory.Bimon.equivMonComonUnitIsoApp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        (M : CategoryTheory.Bimon C) →
          M ≅ ((CategoryTheory.Bimon.toMonComon C).comp (CategoryTheory.Bimon.ofMonComon C)).obj M
-- Init.ShareCommon
ShareCommon.StateFactory.mkImpl : ShareCommon.StateFactoryBuilder → ShareCommon.StateFactory
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.prodMkRight.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (γ : Type u_5)
  [inst : MeasurableSpace γ] (κ : ProbabilityTheory.Kernel α β),
  ProbabilityTheory.Kernel.prodMkRight γ κ = κ.comap Prod.fst ⋯
-- Init.Data.Array.Lemmas
Array.foldl_filterMap' : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → Option β} {g : γ → β → γ} {xs : Array α} {init : γ} {stop : ℕ},
  stop = (Array.filterMap f xs).size →
    Array.foldl g init (Array.filterMap f xs) 0 stop =
      Array.foldl
        (fun x y =>
          match f y with
          | some b => g x b
          | none => x)
        init xs
-- Init.Data.Fin.Lemmas
Fin.subNat_addNat : ∀ {n : ℕ} (i : Fin n) (m : ℕ) (h : optParam (m ≤ ↑(i.addNat m)) ⋯), Fin.subNat m (i.addNat m) h = i
-- Mathlib.Algebra.Category.Ring.Limits
/-- The category of rings has all limits.  -/
RingCat.hasLimitsOfSize : ∀ [UnivLE.{v, u}], CategoryTheory.Limits.HasLimitsOfSize.{w, v, u, u + 1} RingCat
-- Mathlib.RingTheory.HopfAlgebra.Convolution
_private.Mathlib.RingTheory.HopfAlgebra.Convolution.0.LinearMap.«term𝑮» : Lean.ParserDescr
-- Mathlib.Algebra.Lie.Rank
LieModule.isRegular_iff_coeff_polyCharpoly_rank_ne_zero : ∀ (R : Type u_1) {L : Type u_3} (M : Type u_4) {ι : Type u_5} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : LieAlgebra R L] [inst_3 : Module.Finite R L] [inst_4 : Module.Free R L] [inst_5 : AddCommGroup M]
  [inst_6 : Module R M] [inst_7 : LieRingModule L M] [inst_8 : LieModule R L M] [inst_9 : Module.Finite R M]
  [inst_10 : Module.Free R M] [inst_11 : Fintype ι] (b : Module.Basis ι R L) (x : L) [inst_12 : DecidableEq ι],
  LieModule.IsRegular R M x ↔
    (MvPolynomial.eval ⇑(b.repr x)) (((↑(LieModule.toEnd R L M)).polyCharpoly b).coeff (LieModule.rank R L M)) ≠ 0
-- Mathlib.Algebra.Prime.Lemmas
prime_units_mul : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] {y : M} (u : Mˣ), Prime (↑u * y) ↔ Prime y
-- Mathlib.RingTheory.AlgebraicIndependent.Adjoin
AlgebraicIndependent.aevalEquivField_algebraMap_apply_coe : ∀ {ι : Type u_1} {F : Type u_2} {E : Type u_3} {x : ι → E} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E]
  (hx : AlgebraicIndependent F x) (a : MvPolynomial ι F),
  ↑(hx.aevalEquivField ((algebraMap (MvPolynomial ι F) (FractionRing (MvPolynomial ι F))) a)) = (MvPolynomial.aeval x) a
-- Mathlib.Topology.Compactness.Lindelof
IsLindelof.elim_nhds_subcover' : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X},
  IsLindelof s →
    ∀ (U : (x : X) → x ∈ s → Set X), (∀ (x : X) (hx : x ∈ s), U x hx ∈ nhds x) → ∃ t, t.Countable ∧ s ⊆ ⋃ x ∈ t, U ↑x ⋯
-- Mathlib.Analysis.Calculus.LocalExtr.Basic
/-- **Fermat's Theorem**: the derivative of a function at a local extremum equals zero.  -/
IsLocalExtr.hasFDerivAt_eq_zero : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {f' : StrongDual ℝ E} {a : E},
  IsLocalExtr f a → HasFDerivAt f f' a → f' = 0
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric
SemimoduleCat.MonoidalCategory.braiding_naturality_left : ∀ {R : Type u} [inst : CommSemiring R] {X Y : SemimoduleCat R} (f : X ⟶ Y) (Z : SemimoduleCat R),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z) (Y.braiding Z).hom =
    CategoryTheory.CategoryStruct.comp (X.braiding Z).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z f)
-- Std.Time.Format.Modifier
Std.Time.instInhabitedExtendedDayPeriod : Inhabited Std.Time.ExtendedDayPeriod
-- Mathlib.Geometry.Manifold.GroupLieAlgebra
contMDiff_mulInvariantVectorField : ∀ {𝕜 : 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} {G : Type u_4}
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : Group G]
  [inst_7 : LieGroup I (minSmoothness 𝕜 3) G] (v : GroupLieAlgebra I G),
  ContMDiff I I.tangent (minSmoothness 𝕜 2) fun g => ⟨g, mulInvariantVectorField v g⟩
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
/-- The quotient `G ⧸ N` of a complete first countable topological additive group
`G` by a normal additive subgroup is itself complete. Consequently, quotients of Banach spaces by
subspaces are complete. [N. Bourbaki, *General Topology*, IX.3.1 Proposition 4][bourbaki1966b]

Because an additive topological group is not equipped with a `UniformSpace` instance by default,
we must explicitly provide it in order to consider completeness. See
`QuotientAddGroup.completeSpace_right` for a version in which `G` is already equipped with a uniform
structure.  -/
QuotientAddGroup.completeSpace_right' : ∀ (G : Type u) [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalAddGroup G]
  [FirstCountableTopology G] (N : AddSubgroup G) [inst_4 : N.Normal] [CompleteSpace G], CompleteSpace (G ⧸ N)
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.hasLimit_equivalence_comp_iff : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u} [inst_2 : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor J C} (e : K ≌ J),
  CategoryTheory.Limits.HasLimit (e.functor.comp F) ↔ CategoryTheory.Limits.HasLimit F
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.parallelPair.parallelPairObj_zero : ∀ {C : Type u} {X Y : C},
  CategoryTheory.Limits.parallelPair.parallelPairObj X Y CategoryTheory.Limits.WalkingParallelPair.zero = X
-- Mathlib.CategoryTheory.Sums.Products
CategoryTheory.Sum.natTransOfWhiskerLeftInlInr_id : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {A' : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} A'] {B : Type u} [inst_2 : CategoryTheory.Category.{v, u} B]
  {F : CategoryTheory.Functor (A ⊕ A') B},
  CategoryTheory.Sum.natTransOfWhiskerLeftInlInr
      (CategoryTheory.CategoryStruct.id ((CategoryTheory.Sum.inl_ A A').comp F))
      (CategoryTheory.CategoryStruct.id ((CategoryTheory.Sum.inr_ A A').comp F)) =
    CategoryTheory.CategoryStruct.id F
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
CategoryTheory.SimplicialObject.Split.mk : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (X : CategoryTheory.SimplicialObject C) → X.Splitting → CategoryTheory.SimplicialObject.Split C
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.size.match_1.eq_2 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → Sort u_3)
  (h_1 :
    (sz : ℕ) →
      (k : α) →
        (v : β k) → (l r : Std.DTreeMap.Internal.Impl α β) → motive (Std.DTreeMap.Internal.Impl.inner sz k v l r))
  (h_2 : Unit → motive Std.DTreeMap.Internal.Impl.leaf),
  (match Std.DTreeMap.Internal.Impl.leaf with
    | Std.DTreeMap.Internal.Impl.inner sz k v l r => h_1 sz k v l r
    | Std.DTreeMap.Internal.Impl.leaf => h_2 ()) =
    h_2 ()
-- Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
ModelWithCorners.instIsEmptyElemBoundaryOfBoundarylessManifold : ∀ {𝕜 : 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] [BoundarylessManifold I M],
  IsEmpty ↑(ModelWithCorners.boundary M)
-- Mathlib.Algebra.BigOperators.Group.List.Defs
List.prod_hom_rel : ∀ {ι : Type u_1} {M : Type u_2} {N : Type u_3} [inst : Monoid M] [inst_1 : Monoid N] (l : List ι) {r : M → N → Prop}
  {f : ι → M} {g : ι → N},
  r 1 1 → (∀ ⦃i : ι⦄ ⦃a : M⦄ ⦃b : N⦄, r a b → r (f i * a) (g i * b)) → r (List.map f l).prod (List.map g l).prod
-- Mathlib.MeasureTheory.VectorMeasure.Basic
/-- **Alias** of `neg_apply`. -/
MeasureTheory.VectorMeasure.neg_apply : ∀ {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst : FunLike F α β} {inst_1 : Neg β}
  {inst_2 : Neg F} [self : IsNegApply F α β] (f : F) (x : α), (-f) x = -f x
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Left.pos_add_of_right : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α] [IsBotZeroClass α] [AddLeftStrictMono α] {b : α},
  0 < b → ∀ (a : α), 0 < a + b
-- Mathlib.FieldTheory.RatFunc.Degree
RatFunc.intDegree_zero : ∀ {K : Type u} [inst : Field K], RatFunc.intDegree 0 = 0
-- Init.Data.Ord.Basic
Ordering.eq_beq_gt : (Ordering.eq == Ordering.gt) = false