mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Mon
/-- Additive monoid objects in `C` are "just" lax monoidal functors from
the trivial monoidal category to `C`.
 -/
CategoryTheory.AddMon.equivLaxMonoidalFunctorPUnit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      CategoryTheory.LaxMonoidalFunctor (CategoryTheory.Discrete PUnit.{w + 1}) C ≌ CategoryTheory.AddMon C
-- Mathlib.Algebra.BigOperators.Ring.Finset
/-- A product of sums can be written as a sum of products.  -/
Fintype.prod_sum : ∀ {ι : Type u_5} {R : Type u_7} [inst : Fintype ι] [inst_1 : CommSemiring R] [inst_2 : DecidableEq ι] {κ : ι → Type u_8}
  [inst_3 : (i : ι) → Fintype (κ i)] (f : (i : ι) → κ i → R), ∏ i, ∑ j, f i j = ∑ x, ∏ i, f i (x i)
-- Mathlib.Order.Interval.Finset.Defs
/-- This mixin class describes an order where all intervals bounded below are finite. This is
slightly weaker than `LocallyFiniteOrder` + `OrderTop` as it allows empty types.  -/
LocallyFiniteOrderTop : (α : Type u_1) → [Preorder α] → Type u_1
-- Mathlib.Algebra.CubicDiscriminant
/-- The degree-1 coefficient  -/
Cubic.c : {R : Type u_1} → Cubic R → R
-- Mathlib.Data.ZMod.QuotientRing
/-- The **Chinese remainder theorem**, version for `ZMod n`.  -/
ZMod.equivPi : (n : ℕ) → n ≠ 0 → ZMod n ≃+* ((p : ↥n.primeFactors) → ZMod (↑p ^ n.factorization ↑p))
-- Mathlib.Topology.Instances.EReal.Lemmas
EReal.continuousOn_toReal : ContinuousOn EReal.toReal {⊥, ⊤}ᶜ
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.tensorδ_fst_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (W X Y Z : C) {Z_1 : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj W X ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorδ W X Y Z)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.SemiCartesianMonoidalCategory.fst (CategoryTheory.MonoidalCategoryStruct.tensorObj W X)
          (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z))
        h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.SemiCartesianMonoidalCategory.fst W Y)
        (CategoryTheory.SemiCartesianMonoidalCategory.fst X Z))
      h
-- Mathlib.CategoryTheory.MorphismProperty.Local
CategoryTheory.MorphismProperty.IsLocalAtSource.of_le : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C}
  {K L : CategoryTheory.Precoverage C} [P.IsLocalAtSource L], K ≤ L → P.IsLocalAtSource K
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.restrict_apply : ∀ {α : Type u_1} {mα : MeasurableSpace α} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M]
  (v : MeasureTheory.VectorMeasure α M) {i : Set α},
  MeasurableSet i → ∀ {j : Set α}, MeasurableSet j → (v.restrict i) j = v (j ∩ i)
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences
CategoryTheory.Abelian.Ext.preadditiveYoneda_homologySequenceδ_singleTriangle_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact)
  [inst_3 : HasDerivedCategory C] {Y : C} {n₀ : ℕ} (x : CategoryTheory.Abelian.Ext S.X₁ Y n₀) {n₁ : ℕ}
  (h : 1 + n₀ = n₁),
  (CategoryTheory.ConcreteCategory.hom
        ((CategoryTheory.preadditiveYoneda.obj ((DerivedCategory.singleFunctor C 0).obj Y)).homologySequenceδ
          ((CategoryTheory.Pretriangulated.triangleOpEquivalence (DerivedCategory C)).functor.obj
            (Opposite.op hS.singleTriangle))
          ↑n₀ ↑n₁ ⋯))
      x.hom =
    (hS.extClass.comp x h).hom
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.coeff_single_X_pow : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : DecidableEq σ] (s s' : σ) (n n' : ℕ),
  MvPolynomial.coeff (fun₀ | s' => n') (MvPolynomial.X s ^ n) = if s = s' ∧ n = n' ∨ n = 0 ∧ n' = 0 then 1 else 0
-- Init.Prelude
/-- Transitive chaining of proofs, used e.g. by `calc`.

It takes two relations `r` and `s` as "input", and produces an "output"
relation `t`, with the property that `r a b` and `s b c` implies `t a c`.
The `calc` tactic uses this so that when it sees a chain with `a ≤ b` and `b < c`
it knows that this should be a proof of `a < c` because there is an instance
`Trans (·≤·) (·<·) (·<·)`.
 -/
Trans : {α : Sort u_1} →
  {β : Sort u_2} →
    {γ : Sort u_3} →
      (α → β → Sort u) →
        (β → γ → Sort v) → outParam (α → γ → Sort w) → Sort (max (max (max (max (max (max 1 u) u_1) u_2) u_3) v) w)
-- Mathlib.Data.Finset.Fold
Finset.fold_union_empty_singleton : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Finset α), Finset.fold (fun x1 x2 => x1 ∪ x2) ∅ singleton s = s
-- Mathlib.Data.DFinsupp.Module
DFinsupp.support_smul : ∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] {γ : Type w} [inst_1 : (i : ι) → Zero (β i)]
  [inst_2 : (i : ι) → SMulZeroClass γ (β i)] [inst_3 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] (b : γ)
  (v : Π₀ (i : ι), β i), (b • v).support ⊆ v.support
-- Mathlib.CategoryTheory.Adjunction.Unique
CategoryTheory.Adjunction.unit_rightAdjointUniq_hom_assoc : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} {G G' : CategoryTheory.Functor D C}
  (adj1 : F ⊣ G) (adj2 : F ⊣ G') {Z : CategoryTheory.Functor C C} (h : F.comp G' ⟶ Z),
  CategoryTheory.CategoryStruct.comp adj1.unit
      (CategoryTheory.CategoryStruct.comp (F.whiskerLeft (adj1.rightAdjointUniq adj2).hom) h) =
    CategoryTheory.CategoryStruct.comp adj2.unit h
-- Mathlib.FieldTheory.IsPerfectClosure
PerfectRing.liftAux_id : ∀ {K : Type u_1} {M : Type u_3} [inst : CommSemiring K] [inst_1 : CommSemiring M] (j : K →+* M) (p : ℕ)
  [inst_2 : ExpChar M p] [inst_3 : PerfectRing M p], PerfectRing.liftAux (RingHom.id K) j p = ⇑j
-- Mathlib.Data.Finset.Card
Finset.exists_mem_ne : ∀ {α : Type u_1} {s : Finset α}, 1 < s.card → ∀ (a : α), ∃ b ∈ s, b ≠ a
-- Mathlib.LinearAlgebra.BilinearForm.Hom
LinearMap.BilinForm.congr_congr : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {M' : Type u_7}
  {M'' : Type u_8} [inst_3 : AddCommMonoid M'] [inst_4 : AddCommMonoid M''] [inst_5 : Module R M']
  [inst_6 : Module R M''] (e : M' ≃ₗ[R] M'') (f : M ≃ₗ[R] M') (B : LinearMap.BilinForm R M),
  (LinearMap.BilinForm.congr e) ((LinearMap.BilinForm.congr f) B) = (LinearMap.BilinForm.congr (f ≪≫ₗ e)) B
-- Mathlib.CategoryTheory.Localization.LocalizerMorphism
/-- The 2-commutative square expressing that `Φ.localizedFunctor L₁ L₂` lifts the
functor `Φ.functor`  -/
CategoryTheory.LocalizerMorphism.catCommSq : {C₁ : Type u₁} →
  {C₂ : Type u₂} →
    {D₁ : Type u₄} →
      {D₂ : Type u₅} →
        [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
          [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
            [inst_2 : CategoryTheory.Category.{v₄, u₄} D₁] →
              [inst_3 : CategoryTheory.Category.{v₅, u₅} D₂] →
                {W₁ : CategoryTheory.MorphismProperty C₁} →
                  {W₂ : CategoryTheory.MorphismProperty C₂} →
                    (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) →
                      (L₁ : CategoryTheory.Functor C₁ D₁) →
                        [inst_4 : L₁.IsLocalization W₁] →
                          (L₂ : CategoryTheory.Functor C₂ D₂) →
                            [inst_5 : L₂.IsLocalization W₂] →
                              CategoryTheory.CatCommSq Φ.functor L₁ L₂ (Φ.localizedFunctor L₁ L₂)
-- Mathlib.Algebra.FreeAlgebra
/-- Multiplication in `Pre R X` defined as `Pre.mul`. Note: Used for notation only.  -/
FreeAlgebra.Pre.hasMul : (R : Type u_1) → (X : Type u_2) → Mul (FreeAlgebra.Pre R X)
-- Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
SummationFilter.symmetricIoc.eq_1 : ∀ (G : Type u_1) [inst : Neg G] [inst_1 : Preorder G] [inst_2 : LocallyFiniteOrder G],
  SummationFilter.symmetricIoc G = { filter := Filter.map (fun N => Finset.Ioc (-N) N) Filter.atTop }
-- Std.Data.HashSet.Lemmas
Std.HashSet.isEmpty_insertMany_list : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {l : List α},
  (m.insertMany l).isEmpty = (m.isEmpty && l.isEmpty)
-- Mathlib.Algebra.Algebra.Equiv
/-- Helper instance since the coercion is not always found.  -/
AlgEquiv.instFunLike : {R : Type uR} →
  {A₁ : Type uA₁} →
    {A₂ : Type uA₂} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A₁] →
          [inst_2 : Semiring A₂] → [inst_3 : Algebra R A₁] → [inst_4 : Algebra R A₂] → FunLike (A₁ ≃ₐ[R] A₂) A₁ A₂
-- Mathlib.Geometry.Manifold.Riemannian.PathELength
Manifold.riemannianEDist_self : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M]
  [inst_5 : (x : M) → ENorm (TangentSpace I x)] [∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)] {x : M},
  Manifold.riemannianEDist I x x = 0
-- Mathlib.Topology.Algebra.UniformMulAction
UniformSpace.Completion.instSMulCommClassOfUniformContinuousConstSMul : ∀ (M : Type v) (N : Type w) (X : Type x) [inst : UniformSpace X] [inst_1 : SMul M X] [inst_2 : SMul N X]
  [SMulCommClass M N X] [UniformContinuousConstSMul M X] [UniformContinuousConstSMul N X],
  SMulCommClass M N (UniformSpace.Completion X)
-- Mathlib.Tactic.Translate.Reorder
Mathlib.Tactic.Translate.instInhabitedArgReorder : Inhabited Mathlib.Tactic.Translate.ArgReorder
-- Mathlib.Analysis.Normed.Group.Subgroup
/-- If `x` is an element of a subgroup `s` of a seminormed group `E`, its norm in `s` is equal to
its norm in `E`.

This is a reversed version of the `simp` lemma `Subgroup.coe_norm` for use by `norm_cast`.  -/
Subgroup.norm_coe : ∀ {E : Type u_1} [inst : SeminormedGroup E] {s : Subgroup E} (x : ↥s), ‖↑x‖ = ‖x‖
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.filter_eq : ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → Zero (β i)] [inst_1 : DecidableEq ι] (f : Π₀ (i : ι), β i) (i : ι),
  DFinsupp.filter (fun x => i = x) f = fun₀ | i => f i
-- Mathlib.Data.Nat.Count
/-- A fintype instance for the set relevant to `Nat.count`. Locally an instance in scope `count`  -/
Nat.CountSet.fintype : (p : ℕ → Prop) → [DecidablePred p] → (n : ℕ) → Fintype { i // i < n ∧ p i }
-- Init.Data.List.Find
List.findIdx?_nil : ∀ {α : Type u_1} {p : α → Bool}, List.findIdx? p [] = none
-- Mathlib.LinearAlgebra.Quotient.Basic
Submodule.QuotientTop.unique : {R : Type u_1} → {M : Type u_2} → [inst : Ring R] → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → Unique (M ⧸ ⊤)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.size_le_size_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  {v : β k}, t.size ≤ (t.insertIfNew k v).size
-- Mathlib.Combinatorics.SetFamily.Shadow
/-- Being in the upper shadow of `𝒜` means we have a superset in `𝒜`.  -/
Finset.exists_subset_of_mem_upShadow : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {𝒜 : Finset (Finset α)} {s : Finset α},
  s ∈ 𝒜.upShadow → ∃ t ∈ 𝒜, t ⊆ s
-- Std.Data.HashMap.Lemmas
Std.HashMap.get?_inter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α}, (m₁ ∩ m₂).get? k = if k ∈ m₂ then m₁.get? k else none
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get!_eq_default_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {a : α} [inst_1 : Inhabited (β a)], t.contains a = false → t.get! a = default
-- Mathlib.Computability.PartrecBasis
Nat.Partrec'.prim : ∀ {n : ℕ} {f : List.Vector ℕ n → ℕ}, Nat.Primrec' f → Nat.Partrec' ↑f
-- Mathlib.CategoryTheory.Monoidal.Center
CategoryTheory.Center.instReflectsIsomorphismsForget : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C],
  (CategoryTheory.Center.forget C).ReflectsIsomorphisms
-- Mathlib.Algebra.Homology.DerivedCategory.SingleTriangle
/-- The morphism `h₁.singleTriangle h₁ ⟶ h₂.singleTriangle` that is induced by a
map of short exact sequences of objects of `C`.
 -/
CategoryTheory.ShortComplex.ShortExact.singleTriangle.map : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [inst_2 : HasDerivedCategory C] →
        {S₁ S₂ : CategoryTheory.ShortComplex C} →
          (h₁ : S₁.ShortExact) → (h₂ : S₂.ShortExact) → (S₁ ⟶ S₂) → (h₁.singleTriangle ⟶ h₂.singleTriangle)
-- Mathlib.Topology.ContinuousMap.Star
/-- `ContinuousMap.compStarAlgHom'` sends the identity continuous map to the identity
`StarAlgHom`  -/
ContinuousMap.compStarAlgHom'_id : ∀ {X : Type u_1} [inst : TopologicalSpace X] (𝕜 : Type u_4) [inst_1 : CommSemiring 𝕜] (A : Type u_5)
  [inst_2 : TopologicalSpace A] [inst_3 : Semiring A] [inst_4 : IsTopologicalSemiring A] [inst_5 : Star A]
  [inst_6 : ContinuousStar A] [inst_7 : Algebra 𝕜 A],
  ContinuousMap.compStarAlgHom' 𝕜 A (ContinuousMap.id X) = StarAlgHom.id 𝕜 C(X, A)
-- Mathlib.Computability.Primrec.List
Nat.Primrec'.comp₁ : ∀ (f : ℕ → ℕ),
  (Nat.Primrec' fun v => f v.head) → ∀ {n : ℕ} {g : List.Vector ℕ n → ℕ}, Nat.Primrec' g → Nat.Primrec' fun v => f (g v)
-- Init.Data.Sum.Lemmas
Sum.elim_comp_inl : ∀ {α : Type u_1} {γ : Sort u_2} {β : Type u_3} (f : α → γ) (g : β → γ), Sum.elim f g ∘ Sum.inl = f
-- Mathlib.GroupTheory.ResiduallyFinite
AddGroup.ResiduallyFinite.mk : ∀ {G : Type u_1} [inst : AddGroup G], ⨅ H, H.toAddSubgroup = ⊥ → AddGroup.ResiduallyFinite G
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
AddSubmonoid.unop_eq_bot : ∀ {M : Type u_2} [inst : AddZeroClass M] {S : AddSubmonoid Mᵃᵒᵖ}, S.unop = ⊥ ↔ S = ⊥
-- Init.Data.UInt.Log2
/-- Base-two logarithm of word-sized unsigned integers. Returns `⌊max 0 (log₂ a)⌋`.

This function is overridden at runtime with an efficient implementation. This definition is
the logical model.

Examples:
 * `USize.log2 0 = 0`
 * `USize.log2 1 = 0`
 * `USize.log2 2 = 1`
 * `USize.log2 4 = 2`
 * `USize.log2 7 = 2`
 * `USize.log2 8 = 3`
 -/
USize.log2 : USize → USize
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.im_intCast : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} [inst : AddCommGroupWithOne R] (z : ℤ), (↑z).im = 0
-- Mathlib.Topology.Algebra.Group.ClosedSubgroup
ClosedAddSubgroup.instInfClosedAddSubgroup.eq_1 : ∀ (G : Type u) [inst : AddGroup G] [inst_1 : TopologicalSpace G],
  ClosedAddSubgroup.instInfClosedAddSubgroup G = { min := fun U V => { toAddSubgroup := ↑U ⊓ ↑V, isClosed' := ⋯ } }
-- Lean.Widget.InteractiveDiagnostic
Lean.Widget.MsgEmbed.brecOn_2.go : {motive_1 : Lean.Widget.MsgEmbed → Sort u} →
  {motive_2 : Lean.Widget.TaggedText Lean.Widget.MsgEmbed → Sort u} →
    {motive_3 :
        Lean.Widget.StrictOrLazy (Array (Lean.Widget.TaggedText Lean.Widget.MsgEmbed))
            (Lean.Server.WithRpcRef Lean.Widget.LazyTraceChildren) →
          Sort u} →
      {motive_4 : Array (Lean.Widget.TaggedText Lean.Widget.MsgEmbed) → Sort u} →
        {motive_5 : List (Lean.Widget.TaggedText Lean.Widget.MsgEmbed) → Sort u} →
          (t :
              Lean.Widget.StrictOrLazy (Array (Lean.Widget.TaggedText Lean.Widget.MsgEmbed))
                (Lean.Server.WithRpcRef Lean.Widget.LazyTraceChildren)) →
            ((t : Lean.Widget.MsgEmbed) → t.below → motive_1 t) →
              ((t : Lean.Widget.TaggedText Lean.Widget.MsgEmbed) → Lean.Widget.MsgEmbed.below_1 t → motive_2 t) →
                ((t :
                      Lean.Widget.StrictOrLazy (Array (Lean.Widget.TaggedText Lean.Widget.MsgEmbed))
                        (Lean.Server.WithRpcRef Lean.Widget.LazyTraceChildren)) →
                    Lean.Widget.MsgEmbed.below_2 t → motive_3 t) →
                  ((t : Array (Lean.Widget.TaggedText Lean.Widget.MsgEmbed)) →
                      Lean.Widget.MsgEmbed.below_3 t → motive_4 t) →
                    ((t : List (Lean.Widget.TaggedText Lean.Widget.MsgEmbed)) →
                        Lean.Widget.MsgEmbed.below_4 t → motive_5 t) →
                      motive_3 t ×' Lean.Widget.MsgEmbed.below_2 t
-- Mathlib.RingTheory.WittVector.Defs
/-- The polynomials used for defining the addition of the ring of Witt vectors.  -/
WittVector.wittAdd : (p : ℕ) → [hp : Fact (Nat.Prime p)] → ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
-- Mathlib.Analysis.CStarAlgebra.Module.Constructions
_private.Mathlib.Analysis.CStarAlgebra.Module.Constructions.0.WithCStarModule.lipschitzWith_one_equiv_pi_aux : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] {ι : Type u_2} {E : ι → Type u_3}
  [inst_2 : Fintype ι] [inst_3 : (i : ι) → NormedAddCommGroup (E i)] [inst_4 : (i : ι) → Module ℂ (E i)]
  [inst_5 : (i : ι) → SMul A (E i)] [inst_6 : (i : ι) → CStarModule A (E i)] [inst_7 : StarOrderedRing A],
  LipschitzWith 1 ⇑(WithCStarModule.equiv A ((i : ι) → E i))
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.top_adj : ∀ {V : Type u} (v w : V), ⊤.Adj v w ↔ v ≠ w
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonResolvableCompletionItem : Lean.ToJson Lean.Lsp.ResolvableCompletionItem
-- Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
perfectField_of_perfectClosure_eq_bot : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] [h : PerfectField E],
  perfectClosure F E = ⊥ → PerfectField F
-- Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Real.differentiableAt_Gamma : ∀ {s : ℝ}, (∀ (m : ℕ), s ≠ -↑m) → DifferentiableAt ℝ Real.Gamma s
-- Lean.Elab.PreDefinition.PartialFixpoint.Eqns
/-- Generate the "unfold" lemma for `declName`.  -/
_private.Lean.Elab.PreDefinition.PartialFixpoint.Eqns.0.Lean.Elab.PartialFixpoint.mkUnfoldEq : Lean.Name → Lean.Elab.PartialFixpoint.EqnInfo → Lean.MetaM Lean.Name
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
/-- `FreeGroupBasis.ofRepr` constructs a basis given an equivalence with a free group.  -/
FreeGroupBasis.ofRepr : {ι : Type u_1} → {G : Type u_2} → [inst : Group G] → G ≃* FreeGroup ι → FreeGroupBasis ι G
-- Init.Data.UInt.Basic
/-- Negation of 8-bit unsigned integers, computed modulo `UInt8.size`.

`UInt8.neg a` is equivalent to `255 - a + 1`.

This function is overridden at runtime with an efficient implementation.
 -/
UInt8.neg : UInt8 → UInt8
-- Mathlib.RingTheory.LocalProperties.Basic
/-- A property `P` of comm rings is said to be preserved by localization
if `P` holds for `M⁻¹R` whenever `P` holds for `R`.  -/
LocalizationPreserves : ((R : Type u) → [CommRing R] → Prop) → Prop
-- Lean.SubExpr
Lean.SubExpr.GoalsLocation.mk.injEq : ∀ (mvarId : Lean.MVarId) (loc : Lean.SubExpr.GoalLocation) (mvarId_1 : Lean.MVarId) (loc_1 : Lean.SubExpr.GoalLocation),
  ({ mvarId := mvarId, loc := loc } = { mvarId := mvarId_1, loc := loc_1 }) = (mvarId = mvarId_1 ∧ loc = loc_1)
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
IntermediateField.aeval_gen_minpoly : ∀ (F : Type u_1) [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (α : E),
  (Polynomial.aeval (IntermediateField.AdjoinSimple.gen F α)) (minpoly F α) = 0
-- Mathlib.RingTheory.Extension.Presentation.Core
Algebra.Presentation.tensorModelOfHasCoeffsHom_comp : ∀ {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] {P : Algebra.Presentation R S ι σ} (R₀ : Type u_5) [inst_3 : CommRing R₀]
  [inst_4 : Algebra R₀ R] [inst_5 : Algebra R₀ S] [inst_6 : IsScalarTower R₀ R S] [inst_7 : P.HasCoeffs R₀],
  (P.tensorModelOfHasCoeffsHom R₀).comp (P.tensorModelOfHasCoeffsInv R₀) = AlgHom.id R S
-- Mathlib.CategoryTheory.Shift.ShiftSequence
CategoryTheory.Functor.shiftIso_add' : ∀ {C : Type u_1} {A : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} A] (F : CategoryTheory.Functor C A) {M : Type u_4} [inst_2 : AddMonoid M]
  [inst_3 : CategoryTheory.HasShift C M] [inst_4 : F.ShiftSequence M] (n m mn : M) (hnm : m + n = mn) (a a' a'' : M)
  (ha' : n + a = a') (ha'' : m + a' = a''),
  F.shiftIso mn a a'' ⋯ =
    CategoryTheory.Functor.isoWhiskerRight (CategoryTheory.shiftFunctorAdd' C m n mn hnm) (F.shift a) ≪≫
      (CategoryTheory.shiftFunctor C m).associator (CategoryTheory.shiftFunctor C n) (F.shift a) ≪≫
        (CategoryTheory.shiftFunctor C m).isoWhiskerLeft (F.shiftIso n a a' ha') ≪≫ F.shiftIso m a' a'' ha''
-- Mathlib.Analysis.BoxIntegral.UnitPartition
/-- A `BoxIntegral.Box` has integral vertices if its vertices have coordinates in `ℤ`.  -/
BoxIntegral.hasIntegralVertices : {ι : Type u_1} → BoxIntegral.Box ι → Prop
-- Mathlib.CategoryTheory.Subobject.Limits
CategoryTheory.Limits.isIso_kernelSubobject_zero_arrow : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C],
  CategoryTheory.IsIso (CategoryTheory.Limits.kernelSubobject 0).arrow
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransformMorphism.whiskerRight_base : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} {A'' : Type u₇} {B'' : Type u₈}
  {C'' : Type u₉} [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  [inst_6 : CategoryTheory.Category.{v₇, u₇} A''] [inst_7 : CategoryTheory.Category.{v₈, u₈} B'']
  [inst_8 : CategoryTheory.Category.{v₉, u₉} C''] {F'' : CategoryTheory.Functor A'' B''}
  {G'' : CategoryTheory.Functor C'' B''} {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (α : ψ ⟶ ψ')
  (φ : CategoryTheory.Limits.CatCospanTransform F' G' F'' G''),
  (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerRight α φ).base =
    CategoryTheory.Functor.whiskerRight α.base φ.base
-- Mathlib.AlgebraicGeometry.Gluing
AlgebraicGeometry.Scheme.GlueData.ι_eq_iff : ∀ (D : AlgebraicGeometry.Scheme.GlueData) (i j : D.J) (x : ↥(D.U i)) (y : ↥(D.U j)),
  (D.ι i) x = (D.ι j) y ↔ D.Rel ⟨i, x⟩ ⟨j, y⟩
-- Mathlib.Topology.EMetricSpace.Defs
instPseudoEMetricSpaceOrderDual : {X : Type u_1} → [PseudoEMetricSpace X] → PseudoEMetricSpace Xᵒᵈ
-- Mathlib.Topology.Algebra.InfiniteSum.Constructions
/-- For the statement that `tsum` commutes with `Finset.sum`,
see `Summable.tsum_finsetSum`.  -/
Summable.tsum_sum : ∀ {α : Type u_4} {β : Type u_5} {M : Type u_6} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M] [ContinuousAdd M]
  [T2Space M] {f : α ⊕ β → M},
  Summable (f ∘ Sum.inl) →
    Summable (f ∘ Sum.inr) → ∑' (i : α ⊕ β), f i = ∑' (i : α), f (Sum.inl i) + ∑' (i : β), f (Sum.inr i)
-- Mathlib.CategoryTheory.Localization.Triangulated
CategoryTheory.Functor.distTriang_iff : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D)
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : CategoryTheory.Limits.HasZeroObject C] [inst_5 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [inst_6 : CategoryTheory.Pretriangulated C] [inst_7 : CategoryTheory.HasShift D ℤ] [inst_8 : L.CommShift ℤ]
  [inst_9 : CategoryTheory.Limits.HasZeroObject D] [inst_10 : CategoryTheory.Preadditive D]
  [inst_11 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [inst_12 : CategoryTheory.Pretriangulated D]
  [L.mapArrow.EssSurj] [L.IsTriangulated] (T : CategoryTheory.Pretriangulated.Triangle D),
  T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles ↔ T ∈ L.essImageDistTriang
-- Mathlib.NumberTheory.NumberField.House
_private.Mathlib.NumberTheory.NumberField.House.0.NumberField.house.c₁.congr_simp : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] {inst_2 : DecidableEq (K →+* ℂ)}
  [inst_3 : DecidableEq (K →+* ℂ)], NumberField.house.c₁✝ K = NumberField.house.c₁✝ K