mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
UniformConvergenceCLM.instTopologicalSpace.eq_1 : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3}
  (F : Type u_4) [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜₁ E] [inst_4 : TopologicalSpace E]
  [inst_5 : AddCommGroup F] [inst_6 : Module 𝕜₂ F] [inst_7 : TopologicalSpace F] [inst_8 : IsTopologicalAddGroup F]
  (𝔖 : Set (Set E)),
  UniformConvergenceCLM.instTopologicalSpace σ F 𝔖 =
    TopologicalSpace.induced DFunLike.coe (UniformOnFun.topologicalSpace E F 𝔖)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology
CochainComplex.HomComplex.leftHomologyData_π_hom_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  (K L : CochainComplex C ℤ) (n : ℤ) (x : CochainComplex.HomComplex.Cocycle K L n),
  (AddCommGrpCat.Hom.hom (CochainComplex.HomComplex.leftHomologyData K L n).π) x =
    CochainComplex.HomComplex.CohomologyClass.mk x
-- Mathlib.FieldTheory.Finite.Basic
/-- The sum of a nontrivial subgroup of the units of a field is zero.  -/
FiniteField.sum_subgroup_units_eq_zero : ∀ {K : Type u_1} [inst : Ring K] [NoZeroDivisors K] {G : Subgroup Kˣ} [inst_2 : Fintype ↥G], G ≠ ⊥ → ∑ x, ↑↑x = 0
-- Plausible.Random
/-- Generate a random `Fin`.
 -/
Plausible.Random.randFin : {m : Type → Type u_1} → [Monad m] → {g : Type} → {n : ℕ} → [RandomGen g] → Plausible.RandGT g m (Fin n.succ)
-- Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Real.volume_eball : ∀ (a : ℝ) (r : ENNReal), MeasureTheory.volume (Metric.eball a r) = 2 * r
-- Mathlib.GroupTheory.MonoidLocalization.Maps
AddSubmonoid.LocalizationMap.map.eq_1 : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N] {P : Type u_3}
  [inst_2 : AddCommMonoid P] (f : S.LocalizationMap N) {g : M →+ P} {T : AddSubmonoid P} (hy : ∀ (y : ↥S), g ↑y ∈ T)
  {Q : Type u_4} [inst_3 : AddCommMonoid Q] (k : T.LocalizationMap Q), f.map hy k = f.lift ⋯
-- Mathlib.Data.Fintype.Sets
Set.toFinset_singleton : ∀ {α : Type u_1} (a : α) [inst : Fintype ↑{a}], {a}.toFinset = {a}
-- Mathlib.Order.Hom.BoundedLattice
InfTopHom.coe_toTopHom : ∀ {α : Type u_2} {β : Type u_3} [inst : Min α] [inst_1 : Top α] [inst_2 : Min β] [inst_3 : Top β] (f : InfTopHom α β),
  ⇑f.toTopHom = ⇑f
-- Mathlib.Computability.NFA
NFA.Path.cons.congr_simp : ∀ {α : Type u} {σ : Type v} {M : NFA α σ} (t s u : σ) (a : α) (x : List α) (a_1 : t ∈ M.step s a)
  (a_2 a_3 : M.Path t u x), a_2 = a_3 → NFA.Path.cons t s u a x a_1 a_2 = NFA.Path.cons t s u a x a_1 a_3
-- Mathlib.Analysis.CStarAlgebra.GelfandDuality
/-- The Gelfand transform is bijective when the algebra is a C⋆-algebra over `ℂ`.  -/
gelfandTransform_bijective : ∀ (A : Type u_1) [inst : CommCStarAlgebra A], Function.Bijective ⇑(WeakDual.gelfandTransform ℂ A)
-- Mathlib.CategoryTheory.ComposableArrows.Basic
_private.Mathlib.CategoryTheory.ComposableArrows.Basic.0.CategoryTheory.ComposableArrows.Precomp.obj.match_1.splitter : {n : ℕ} →
  (motive : Fin (n + 1 + 1) → Sort u_1) →
    (x : Fin (n + 1 + 1)) →
      ((isLt : 0 < n + 1 + 1) → motive ⟨0, isLt⟩) →
        ((i : ℕ) → (hi : i + 1 < n + 1 + 1) → motive ⟨i.succ, hi⟩) → motive x
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.restrict_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : Zero β] (f : MeasureTheory.SimpleFunc α β)
  {s : Set α}, MeasurableSet s → ∀ (a : α), (f.restrict s) a = s.indicator (⇑f) a
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem?_union : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, (m₁ ∪ m₂)[k]? = m₂[k]?.or m₁[k]?
-- Mathlib.Order.KrullDimension
Order.height_eq_coe_add_one_iff : ∀ {α : Type u_1} [inst : Preorder α] {x : α} {n : ℕ},
  Order.height x = ↑n + 1 ↔ Order.height x < ⊤ ∧ (∃ y < x, Order.height y = ↑n) ∧ ∀ y < x, Order.height y ≤ ↑n
-- Mathlib.FieldTheory.PurelyInseparable.AdjoinPthRoots
instFieldAdjoinPthRoots : (k : Type u_1) → [Field k] → Field (AdjoinPthRoots k)
-- Mathlib.NumberTheory.Padics.Hensel
_private.Mathlib.NumberTheory.Padics.Hensel.0.ih_0 : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : CommSemiring R] [inst_2 : Algebra R ℤ_[p]]
  {F : Polynomial R} {a : ℤ_[p]},
  ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2 → ih_gen✝ 0 a
-- Mathlib.GroupTheory.Index
AddSubgroup.one_lt_index_of_ne_top : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} [Finite (G ⧸ H)], H ≠ ⊤ → 1 < H.index
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.NonemptyCompacts.mem_singleton : ∀ {α : Type u_1} [inst : TopologicalSpace α] (x y : α), x ∈ {y} ↔ x = y
-- Lean.Elab.InfoTree.Types
Lean.Elab.Info.ofErrorNameInfo.inj : ∀ {i i_1 : Lean.Elab.ErrorNameInfo}, Lean.Elab.Info.ofErrorNameInfo i = Lean.Elab.Info.ofErrorNameInfo i_1 → i = i_1
-- Mathlib.Analysis.Meromorphic.IsolatedZeros
/-- Formulation of `MeromorphicAt.frequently_zero_iff_eventuallyEq_zero` as an identity principle: If
`f` and `g` are meromorphic at `x`, then `f` and `g` agree eventually in a punctured neighborhood of
`x` iff they agree at points arbitrarily close to (but different from) `x`.
 -/
MeromorphicAt.frequently_eq_iff_eventuallyEq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : 𝕜} {f g : 𝕜 → E},
  MeromorphicAt f x → MeromorphicAt g x → ((∃ᶠ (z : 𝕜) in nhdsWithin x {x}ᶜ, f z = g z) ↔ f =ᶠ[nhdsWithin x {x}ᶜ] g)
-- Mathlib.SetTheory.ZFC.Rank
PSet.rank_lt_of_mem : ∀ {x y : PSet.{u_1}}, y ∈ x → y.rank < x.rank
-- Mathlib.RingTheory.Coalgebra.MonoidAlgebra
LaurentPolynomial.comul_C : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Module R A]
  [inst_3 : Coalgebra R A] (a : A),
  CoalgebraStruct.comul (LaurentPolynomial.C a) =
    (TensorProduct.map (AddMonoidAlgebra.lsingle 0) (AddMonoidAlgebra.lsingle 0)) (CoalgebraStruct.comul a)
-- Mathlib.CategoryTheory.Subfunctor.Image
CategoryTheory.Subfunctor.range_toRange : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F F' : CategoryTheory.Functor C (Type w)} (p : F' ⟶ F),
  CategoryTheory.Subfunctor.range (CategoryTheory.Subfunctor.toRange p) = ⊤
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.coyonedaEquiv.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {F : CategoryTheory.Functor C (Type v₁)},
  CategoryTheory.coyonedaEquiv =
    { toFun := fun η => (CategoryTheory.ConcreteCategory.hom (η.app X)) (CategoryTheory.CategoryStruct.id X),
      invFun := fun ξ =>
        { app := fun x => TypeCat.ofHom fun x_1 => (CategoryTheory.ConcreteCategory.hom (F.map x_1)) ξ,
          naturality := ⋯ },
      left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.RingTheory.NonUnitalSubring.Defs
/-- A non-unital subring of a non-unital ring inherits a non-unital ring structure  -/
NonUnitalSubring.toNonUnitalRing : {R : Type u_1} → [inst : NonUnitalRing R] → (s : NonUnitalSubring R) → NonUnitalRing ↥s
-- Std.Time.Internal.Bounded
Std.Time.Internal.Bounded.instDecidableEq : {rel : ℤ → ℤ → Prop} → {n m : ℤ} → DecidableEq (Std.Time.Internal.Bounded rel n m)
-- Init.Data.Range.Polymorphic.Lemmas
Std.Ric.pairwise_toList_ne : ∀ {α : Type u} {r : Std.Ric α} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.Least? α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLE α] [Std.PRange.LawfulUpwardEnumerableLeast? α]
  [inst_7 : Std.Rxc.IsAlwaysFinite α], List.Pairwise (fun a b => a ≠ b) r.toList
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.colimit.isColimit.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Functor J C) [inst_2 : CategoryTheory.Limits.HasColimit F],
  CategoryTheory.Limits.colimit.isColimit F = (CategoryTheory.Limits.getColimitCocone F).isColimit
-- Mathlib.Topology.Semicontinuity.Lindelof
/-- If a function `s : X → E` can be written as the supremum of a family `𝓕` of lower semicontinuous
functions then, assuming that `X` is hereditarily Lindelöf (for example, second countable),
`s` can in fact be written as the supremum of some *countable* subfamily `𝓕'`.

This is implication a) ⇒ b) in
[N. Bourbaki, *Topologie Générale*, Chapitre IX, Appendice I, Proposition 3][bourbaki1974]

See the module docstring for a discussion of the assumptions on `E`.  -/
exists_countable_lowerSemicontinuous_isLUB : ∀ {X : Type u_1} {E : Type u_2} [inst : TopologicalSpace X] [HereditarilyLindelofSpace X] [inst_2 : LinearOrder E]
  [inst_3 : TopologicalSpace E] [OrderClosedTopology E] [DenselyOrdered E] [TopologicalSpace.SeparableSpace E]
  {s : X → E} {𝓕 : Set (X → E)}, (∀ f ∈ 𝓕, LowerSemicontinuous f) → IsLUB 𝓕 s → ∃ 𝓕' ⊆ 𝓕, 𝓕'.Countable ∧ IsLUB 𝓕' s
-- Mathlib.Analysis.AperiodicOrder.Delone.Basic
/-- There exists a radius `r > 0` such that any ball of radius `r`
centered at a point of `D` contains at most one point of `D`.  -/
Delone.DeloneSet.subset_ball_singleton : ∀ {X : Type u_1} [inst : MetricSpace X] (D : Delone.DeloneSet X),
  ∃ r > 0, ∀ {x y z : X}, x ∈ D → y ∈ D → x ∈ Metric.ball z r → y ∈ Metric.ball z r → x = y
-- Mathlib.CategoryTheory.Monoidal.Free.Coherence
CategoryTheory.FreeMonoidalCategory.normalizeMapAux.eq_9 : ∀ {C : Type u} (T X Y W : CategoryTheory.FreeMonoidalCategory C) (f : T.Hom Y) (g : X.Hom W),
  CategoryTheory.FreeMonoidalCategory.normalizeMapAux (f.tensor g) =
    CategoryTheory.Discrete.natTrans fun x =>
      match x with
      | { as := X_1 } =>
        CategoryTheory.CategoryStruct.comp
          ((CategoryTheory.FreeMonoidalCategory.normalizeMapAux g).app { as := T.normalizeObj X_1 })
          (W.normalizeObj'.map ((CategoryTheory.FreeMonoidalCategory.normalizeMapAux f).app { as := X_1 }))
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.coe_copy : ∀ {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₃ : Type u_11} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M] [inst_5 : Module S M₃] {σ : R →+* S}
  (f : M →ₛₗ[σ] M₃) (f' : M → M₃) (h : f' = ⇑f), ⇑(f.copy f' h) = f'
-- Mathlib.Geometry.Convex.ConvexSpace.AffineSpace
AddTorsor.convexCombination_assoc : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  (f : Convexity.StdSimplex R (Convexity.StdSimplex R P)),
  AddTorsor.convexCombination (Convexity.StdSimplex.map AddTorsor.convexCombination f) =
    AddTorsor.convexCombination f.join
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.IsSubgraph.vertexSet_mono : ∀ {α : Type u_1} {β : Type u_2} {H G : Graph α β}, H.IsSubgraph G → H.vertexSet ⊆ G.vertexSet
-- Init.Data.SInt.Lemmas
Int8.neg_zero : -0 = 0
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.Hom.mul_def : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {M X : C} [inst_2 : CategoryTheory.MonObj M] (f₁ f₂ : X ⟶ M),
  f₁ * f₂ =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift f₁ f₂) CategoryTheory.MonObj.mul
-- Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
isTranscendenceBasis_iff_algebraicIndependent_isAlgebraic : ∀ {ι : Type u} {R : Type u_1} {A : Type w} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [Nontrivial R],
  IsTranscendenceBasis R x ↔ AlgebraicIndependent R x ∧ Algebra.IsAlgebraic (↥(Algebra.adjoin R (Set.range x))) A
-- Mathlib.GroupTheory.Perm.Cycle.Factors
Equiv.Perm.cycleFactorsFinset.eq_1 : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Fintype α] (f : Equiv.Perm α),
  f.cycleFactorsFinset = Trunc.lift (fun l => { val := ↑↑l, nodup := ⋯ }) ⋯ f.truncCycleFactors
-- Lean.Syntax
Lean.Syntax.getAntiquotSpliceSuffix : Lean.Syntax → Lean.Syntax
-- Init.Prelude
/-- The message to display on stack overflow.  -/
Lean.maxRecDepthErrorMessage : String
-- Init.Data.Fin.Fold
Fin.foldr_succ_last : ∀ {n : ℕ} {α : Sort u_1} (f : Fin (n + 1) → α → α) (x : α),
  Fin.foldr (n + 1) f x = Fin.foldr n (fun x => f x.castSucc) (f (Fin.last n) x)
-- Lean.Meta.Sym.AlphaShareBuilder
Lean.Meta.Sym.Internal.MonadShareCommon.assertShared : {m : Type → Type} → [self : Lean.Meta.Sym.Internal.MonadShareCommon m] → Lean.Expr → m Unit
-- Mathlib.Data.ENNReal.Real
ENNReal.toReal_min : ∀ {a b : ENNReal}, a ≠ ⊤ → b ≠ ⊤ → (min a b).toReal = min a.toReal b.toReal
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
/-- `ContinuousAlternatingMap.pi` as an `Equiv`.  -/
ContinuousAlternatingMap.piEquiv : {R : Type u_1} →
  {M : Type u_2} →
    {ι : Type u_6} →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] →
            [inst_3 : TopologicalSpace M] →
              {ι' : Type u_7} →
                {N : ι' → Type u_8} →
                  [inst_4 : (i : ι') → AddCommMonoid (N i)] →
                    [inst_5 : (i : ι') → TopologicalSpace (N i)] →
                      [inst_6 : (i : ι') → Module R (N i)] →
                        ((i : ι') → M [⋀^ι]→L[R] N i) ≃ M [⋀^ι]→L[R] ((i : ι') → N i)
-- Mathlib.Data.Finsupp.Basic
Finsupp.sumElim_zero_single : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Zero γ] (b : β) (c : γ),
  (Finsupp.sumElim 0 fun₀ | b => c) = fun₀ | Sum.inr b => c
-- Mathlib.Algebra.Module.FinitePresentation
Module.finitePresentation_of_free_of_surjective : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] [Module.Free R M] [Module.Finite R M] (l : M →ₗ[R] N),
  Function.Surjective ⇑l → l.ker.FG → Module.FinitePresentation R N
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
CategoryTheory.ChosenPullbacksAlong.unit_pullbackId_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (X : C)
  [inst_1 : CategoryTheory.ChosenPullbacksAlong (CategoryTheory.CategoryStruct.id X)] (Y : CategoryTheory.Over X),
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.ChosenPullbacksAlong.mapPullbackAdj (CategoryTheory.CategoryStruct.id X)).unit.app Y)
      ((CategoryTheory.ChosenPullbacksAlong.pullbackId X).hom.app
        ((CategoryTheory.Over.map (CategoryTheory.CategoryStruct.id X)).obj Y)) =
    (CategoryTheory.ChosenPullbacksAlong.mapPullbackAdj (CategoryTheory.CategoryStruct.id X)).unit.app Y
-- Init.Data.SInt.Bitwise
ISize.not_eq_neg_add : ∀ (a : ISize), ~~~a = -a - 1
-- Init.Data.UInt.Bitwise
UInt64.toFin_or : ∀ (a b : UInt64), (a ||| b).toFin = a.toFin ||| b.toFin
-- Mathlib.LinearAlgebra.Matrix.ZPow
Matrix.instDivInvMonoid : {n' : Type u_1} → [DecidableEq n'] → [Fintype n'] → {R : Type u_2} → [CommRing R] → DivInvMonoid (Matrix n' n' R)
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
SimpleGraph.maximal_isAcyclic_iff_isTree : ∀ {V : Type u_1} [Nonempty V] {T : SimpleGraph V}, Maximal SimpleGraph.IsAcyclic T ↔ T.IsTree
-- Init.Data.BitVec.Bitblast
Bool.atLeastTwo_true_right : ∀ {a b : Bool}, a.atLeastTwo b true = (a || b)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKeyD_filter_not_contains_map_fst_of_contains_eq_false_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)} {k fallback : α},
  Std.Internal.List.DistinctKeys l₁ →
    Std.Internal.List.containsKey k l₁ = false →
      Std.Internal.List.getKeyD k (List.filter (fun p => !(List.map Sigma.fst l₂).contains p.fst) l₁) fallback =
        fallback
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get?_insertMany!_list_of_mem : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  t.WF →
    ∀ {l : List ((a : α) × β a)} {k k' : α} (k_beq : compare k k' = Ordering.eq) {v : β k},
      List.Pairwise (fun a b => ¬compare a.fst b.fst = Ordering.eq) l →
        ⟨k, v⟩ ∈ l → (↑(t.insertMany! l)).get? k' = some (cast ⋯ v)
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.Raw₀.getEntry?_eq_getEntry?ₘ : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (a : α),
  m.getEntry? a = m.getEntry?ₘ a
-- Lean.Meta.Injective
Lean.Meta.elimOptParam : Lean.Expr → Lean.CoreM Lean.Expr
-- Mathlib.Data.Rel
SetRel.image_inter_subset : ∀ {α : Type u_1} {β : Type u_2} (R : SetRel α β) {s₁ s₂ : Set α}, R.image (s₁ ∩ s₂) ⊆ R.image s₁ ∩ R.image s₂
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Matrix.charpoly_natDegree_eq_dim : ∀ {R : Type u} [inst : CommRing R] {n : Type v} [inst_1 : DecidableEq n] [inst_2 : Fintype n] [Nontrivial R]
  (M : Matrix n n R), M.charpoly.natDegree = Fintype.card n
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.toList_toArray : ∀ {α : Type u} {β : α → Type v} {t : Std.DTreeMap.Internal.Impl α β}, t.toArray.toList = t.toList
-- Mathlib.Order.GameAdd
/-- `Prod.GameAdd rα rβ x y` means that `x` can be reached from `y` by decreasing either entry with
respect to the relations `rα` and `rβ`.

It is so called, as it models game addition within combinatorial game theory. If `rα a₁ a₂` means
that `a₂ ⟶ a₁` is a valid move in game `α`, and `rβ b₁ b₂` means that `b₂ ⟶ b₁` is a valid move
in game `β`, then `GameAdd rα rβ` specifies the valid moves in the juxtaposition of `α` and `β`:
the player is free to choose one of the games and make a move in it, while leaving the other game
unchanged.

See `Sym2.GameAdd` for the unordered pair analog.  -/
Prod.GameAdd : {α : Type u_1} → {β : Type u_2} → (α → α → Prop) → (β → β → Prop) → α × β → α × β → Prop
-- Mathlib.RingTheory.Spectrum.Prime.Topology
/-- [Stacks Tag 00HY](https://stacks.math.columbia.edu/tag/00HY) -/
PrimeSpectrum.stableUnderSpecialization_range_iff : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] {f : R →+* S},
  StableUnderSpecialization (Set.range (PrimeSpectrum.comap f)) ↔ IsClosed (Set.range (PrimeSpectrum.comap f))
-- Mathlib.RingTheory.Valuation.ValuationRing
ValuationRing.isLocalRing : ∀ (A : Type u) [inst : CommRing A] [Nontrivial A] [PreValuationRing A], IsLocalRing A
-- Init.Data.SInt.Lemmas
Int64.mul_add : ∀ {a b c : Int64}, a * (b + c) = a * b + a * c
-- Init.Core
heq_comm : ∀ {α β : Sort u_1} {a : α} {b : β}, a ≍ b ↔ b ≍ a
-- Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Real.volume_closedBall : ∀ (a r : ℝ), MeasureTheory.volume (Metric.closedBall a r) = ENNReal.ofReal (2 * r)
-- Mathlib.CategoryTheory.Galois.Prorepresentability
/-- The canonical functor from pointed Galois objects to `C`.  -/
CategoryTheory.PreGaloisCategory.PointedGaloisObject.incl : {C : Type u₁} →
  [inst : CategoryTheory.Category.{u₂, u₁} C] →
    [inst_1 : CategoryTheory.GaloisCategory C] →
      (F : CategoryTheory.Functor C FintypeCat) →
        CategoryTheory.Functor (CategoryTheory.PreGaloisCategory.PointedGaloisObject F) C
-- Mathlib.Data.Multiset.AddSub
Multiset.le_add_left : ∀ {α : Type u_1} (s t : Multiset α), s ≤ t + s
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.minKeyD_alter_eq_self : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] {k : α}
  {f : Option β → Option β},
  (Std.DTreeMap.Const.alter t k f).isEmpty = false →
    ∀ {fallback : α},
      (Std.DTreeMap.Const.alter t k f).minKeyD fallback = k ↔
        (f (Std.DTreeMap.Const.get? t k)).isSome = true ∧ ∀ k' ∈ t, (cmp k k').isLE = true
-- Mathlib.FieldTheory.IntermediateField.Basic
/-- Turn a subalgebra closed under inverses into an intermediate field.  -/
Subalgebra.toIntermediateField : {K : Type u_1} →
  {L : Type u_2} →
    [inst : Field K] →
      [inst_1 : Field L] → [inst_2 : Algebra K L] → (S : Subalgebra K L) → (∀ x ∈ S, x⁻¹ ∈ S) → IntermediateField K L
-- Init.Data.String.Lemmas.Search
String.front?_toSlice : ∀ {s : String}, s.toSlice.front? = s.front?
-- Mathlib.GroupTheory.GroupAction.Hom
MulDistribMulActionHom.comp_assoc : ∀ {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] {P : Type u_3} [inst_2 : Monoid P] {φ : M →* N}
  {ψ : N →* P} {χ : M →* P} {A : Type u_4} [inst_3 : Monoid A] [inst_4 : MulDistribMulAction M A] {B : Type u_5}
  [inst_5 : Monoid B] [inst_6 : MulDistribMulAction N B] {C : Type u_7} [inst_7 : Monoid C]
  [inst_8 : MulDistribMulAction P C] {Q : Type u_11} {D : Type u_12} [inst_9 : Monoid Q] [inst_10 : Monoid D]
  [inst_11 : MulDistribMulAction Q D] {η : P →* Q} {θ : M →* Q} {ζ : N →* Q} (h : C →ₑ*[η] D) (g : B →ₑ*[ψ] C)
  (f : A →ₑ*[φ] B) [inst_12 : φ.CompTriple ψ χ] [inst_13 : χ.CompTriple η θ] [inst_14 : ψ.CompTriple η ζ]
  [inst_15 : φ.CompTriple ζ θ], h.comp (g.comp f) = (h.comp g).comp f
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.optionEquivLeft_C : ∀ (R : Type u) (S₁ : Type v) [inst : CommSemiring R] (r : R),
  (MvPolynomial.optionEquivLeft R S₁) (MvPolynomial.C r) = Polynomial.C (MvPolynomial.C r)
-- Std.Sat.AIG.CachedLemmas
_private.Std.Sat.AIG.CachedLemmas.0.Std.Sat.AIG.mkGateCached.go.match_1.eq_5 : ∀ (motive : Option Bool → Option Bool → Sort u_1) (x x_1 : Option Bool)
  (h_1 : (x : Option Bool) → motive (some false) x) (h_2 : (x : Option Bool) → motive x (some false))
  (h_3 : (x : Option Bool) → motive (some true) x) (h_4 : (x : Option Bool) → motive x (some true))
  (h_5 : (x x_2 : Option Bool) → motive x x_2),
  (x = some false → False) →
    (x_1 = some false → False) →
      (x = some true → False) →
        (x_1 = some true → False) →
          (match x, x_1 with
            | some false, x => h_1 x
            | x, some false => h_2 x
            | some true, x => h_3 x
            | x, some true => h_4 x
            | x, x_6 => h_5 x x_6) =
            h_5 x x_1
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- Morphisms for `WalkingMultispan`.  -/
CategoryTheory.Limits.WalkingMultispan.Hom : {J : CategoryTheory.Limits.MultispanShape} →
  CategoryTheory.Limits.WalkingMultispan J → CategoryTheory.Limits.WalkingMultispan J → Type (max w w')
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.size_toArray : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α],
  m.toArray.size = m.size
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F.rightOp : C ⥤ Dᵒᵖ` reflects colimits of shape `Jᵒᵖ`, then `F : Cᵒᵖ ⥤ D` reflects limits
of shape `J`.  -/
CategoryTheory.Limits.reflectsLimitsOfShape_of_rightOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (J : Type w) [inst_2 : CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor Cᵒᵖ D)
  [CategoryTheory.Limits.ReflectsColimitsOfShape Jᵒᵖ F.rightOp], CategoryTheory.Limits.ReflectsLimitsOfShape J F
-- Mathlib.CategoryTheory.Abelian.RightDerived
/-- We can compute a right derived functor on a morphism using a descent of that morphism
to a cochain map between chosen injective resolutions.
 -/
CategoryTheory.Functor.rightDerived_map_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.HasInjectiveResolutions C]
  [inst_4 : CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [inst_5 : F.Additive] (n : ℕ) {X Y : C}
  (f : X ⟶ Y) {P : CategoryTheory.InjectiveResolution X} {Q : CategoryTheory.InjectiveResolution Y}
  (g : P.cocomplex ⟶ Q.cocomplex),
  CategoryTheory.CategoryStruct.comp P.ι g = CategoryTheory.CategoryStruct.comp ((CochainComplex.single₀ C).map f) Q.ι →
    (F.rightDerived n).map f =
      CategoryTheory.CategoryStruct.comp (P.isoRightDerivedObj F n).hom
        (CategoryTheory.CategoryStruct.comp
          (((F.mapHomologicalComplex (ComplexShape.up ℕ)).comp
                (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n)).map
            g)
          (Q.isoRightDerivedObj F n).inv)