mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.le_add_sub : ∀ (a b : Ordinal.{u_4}), a ≤ b + (a - b)
-- Mathlib.GroupTheory.SpecificGroups.Alternating
/-- The alternating group on a finite type, realized as a subgroup of `Equiv.Perm`.
For $A_n$, use `alternatingGroup (Fin n)`.  -/
alternatingGroup : (α : Type u_1) → [Fintype α] → [DecidableEq α] → Subgroup (Equiv.Perm α)
-- Aesop.Options.Public
Aesop.instInhabitedOptions : Inhabited Aesop.Options
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Ioc_union_Ioi' : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c : α}, c ≤ b → Set.Ioc a b ∪ Set.Ioi c = Set.Ioi (min a c)
-- Mathlib.Algebra.Order.Hom.Ring
OrderRingHom.instPreorder : {α : Type u_2} →
  {β : Type u_3} →
    [inst : NonAssocSemiring α] →
      [inst_1 : Preorder α] → [inst_2 : NonAssocSemiring β] → [inst_3 : Preorder β] → Preorder (α →+*o β)
-- Mathlib.Analysis.Normed.Group.Hom
/-- The lifting of a norm nonincreasing morphism is norm nonincreasing.  -/
NormedAddGroupHom.Equalizer.lift_normNoninc : ∀ {V : Type u_1} {W : Type u_2} {V₁ : Type u_3} [inst : SeminormedAddCommGroup V] [inst_1 : SeminormedAddCommGroup W]
  [inst_2 : SeminormedAddCommGroup V₁] {f g : NormedAddGroupHom V W} (φ : NormedAddGroupHom V₁ V)
  (h : f.comp φ = g.comp φ), φ.NormNoninc → (NormedAddGroupHom.Equalizer.lift φ h).NormNoninc
-- Mathlib.RingTheory.FilteredAlgebra.Basic
IsFiltration.is_sup : ∀ {ι : Type u_1} {σ : Type u_3} {inst : Preorder ι} {inst_1 : Preorder σ} {F : ι → σ} {F_lt : outParam (ι → σ)}
  [self : IsFiltration F F_lt] (B : σ) (j : ι), (∀ i < j, F i ≤ B) → F_lt j ≤ B
-- Mathlib.RingTheory.DedekindDomain.Different
FractionalIdeal.dual_ne_zero_iff : ∀ {A : Type u_1} {K : Type u_2} {L : Type u} {B : Type u_3} [inst : CommRing A] [inst_1 : Field K] [inst_2 : CommRing B]
  [inst_3 : Field L] [inst_4 : Algebra A K] [inst_5 : Algebra B L] [inst_6 : Algebra A B] [inst_7 : Algebra K L]
  [inst_8 : Algebra A L] [inst_9 : IsScalarTower A K L] [inst_10 : IsScalarTower A B L] [inst_11 : IsDomain A]
  [inst_12 : IsFractionRing A K] [inst_13 : FiniteDimensional K L] [inst_14 : Algebra.IsSeparable K L]
  [inst_15 : IsIntegralClosure B A L] [inst_16 : IsFractionRing B L] [inst_17 : IsIntegrallyClosed A]
  [inst_18 : IsDedekindDomain B] {I : FractionalIdeal (nonZeroDivisors B) L}, FractionalIdeal.dual A K I ≠ 0 ↔ I ≠ 0
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
/-- **Alias** of `MeasureTheory.integrable_finsetSum'`. -/
MeasureTheory.integrable_finset_sum' : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ε' : Type u_8} [inst : TopologicalSpace ε']
  [inst_1 : ESeminormedAddCommMonoid ε'] [ContinuousAdd ε'] {ι : Type u_9} (s : Finset ι) {f : ι → α → ε'},
  (∀ i ∈ s, MeasureTheory.Integrable (f i) μ) → MeasureTheory.Integrable (∑ i ∈ s, f i) μ
-- Mathlib.Data.Multiset.ZeroCons
Multiset.card_eq_zero : ∀ {α : Type u_1} {s : Multiset α}, s.card = 0 ↔ s = 0
-- Mathlib.CategoryTheory.Limits.Opposites
/-- Turn a colimit for `F : Jᵒᵖ ⥤ Cᵒᵖ` into a limit for `F.unop : J ⥤ C`.  -/
CategoryTheory.Limits.isLimitConeUnopOfCocone : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} J] →
        (F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ) →
          {c : CategoryTheory.Limits.Cocone F} →
            CategoryTheory.Limits.IsColimit c → CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.coneUnopOfCocone c)
-- Mathlib.Algebra.Group.Pi.Lemmas
Function.ExtendByZero.hom_apply : ∀ {ι : Type u_1} {η : Type v} (R : Type w) (s : ι → η) [inst : AddZeroClass R] (f : ι → R) (a : η),
  (Function.ExtendByZero.hom R s) f a = Function.extend s f 0 a
-- Lean.Data.Lsp.Extra
Lean.Lsp.LeanModuleHierarchyImportedByParams.mk.inj : ∀ {module module_1 : Lean.Lsp.LeanModule}, { module := module } = { module := module_1 } → module = module_1
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get?_insertMany_list_of_not_mem_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {l : List α} {k k' : α},
      cmp k k' = Ordering.eq →
        k ∉ t → List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l → k ∈ l → (t.insertMany l).get? k' = some k
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem!_inter_of_not_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  [inst_1 : Inhabited β], k ∉ t₂ → (t₁ ∩ t₂)[k]! = default
-- Mathlib.Data.Finset.Sum
Finset.gc_map_inr_toRight : ∀ {α : Type u_1} {β : Type u_2}, GaloisConnection (fun x => Finset.map Function.Embedding.inr x) Finset.toRight
-- Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue
/-- For all `ε > 0` and finite families `A`, we can partition the remainders of `A` mod `b`
into `abv.card ε` sets, such that all elements in each part of remainders are close together.  -/
AbsoluteValue.IsAdmissible.exists_partition' : ∀ {R : Type u_1} [inst : EuclideanDomain R] {abv : AbsoluteValue R ℤ} (self : abv.IsAdmissible) (n : ℕ) {ε : ℝ},
  0 < ε →
    ∀ {b : R}, b ≠ 0 → ∀ (A : Fin n → R), ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ → ↑(abv (A i₁ % b - A i₀ % b)) < abv b • ε
-- Mathlib.AlgebraicTopology.SimplexCategory.Rev
SimplexCategory.rev_map_rev_map : ∀ {n m : SimplexCategory} (f : n ⟶ m), SimplexCategory.rev.map (SimplexCategory.rev.map f) = f
-- Mathlib.GroupTheory.OrderOfElement
exists_zpow_eq_one : ∀ {G : Type u_1} [inst : Group G] [Finite G] (x : G), ∃ i, ∃ (_ : i ≠ 0), x ^ i = 1
-- Std.Time.Time.Unit.Basic
/-- Converts a `Minute.Offset` to an `Hour.Offset`.
 -/
Std.Time.Minute.Offset.toHours : Std.Time.Minute.Offset → Std.Time.Hour.Offset
-- Std.Data.Iterators.Combinators.Monadic.DropWhile
/-- Internal state of the `dropWhile` combinator. Do not depend on its internals.
 -/
Std.Iterators.Types.DropWhile : Type w → (m : Type w → Type w') → (β : Type w) → (β → Std.Iterators.PostconditionT m (ULift.{w, 0} Bool)) → Type w
-- Lean.Parser.Do
Lean.Parser.Term.doIdDecl.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.X_pow_add_C_ne_one : ∀ {R : Type u} [Nontrivial R] [inst : Semiring R] {n : ℕ}, 0 < n → ∀ (a : R), Polynomial.X ^ n + Polynomial.C a ≠ 1
-- Mathlib.Data.QPF.Multivariate.Basic
MvQPF.supp_eq : ∀ {n : ℕ} {F : TypeVec.{u} n → Type u_1} [q : MvQPF F] {α : TypeVec.{u} n} {i : Fin2 n} (x : F α),
  MvFunctor.supp x i =
    {u | ∀ (a : (MvQPF.P F).A) (f : ((MvQPF.P F).B a).Arrow α), MvQPF.abs ⟨a, f⟩ = x → u ∈ f i '' Set.univ}
-- Mathlib.RingTheory.Algebraic.Basic
isAlgebraic_intCast : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] [Nontrivial R] (n : ℤ),
  IsAlgebraic R ↑n
-- Mathlib.Data.Set.Lattice
/-- Equivalence from the disjoint union of a family of sets forming a partition of `β`, to `β`
itself.  -/
Set.sigmaEquiv : {α : Type u_1} → {β : Type u_2} → (s : α → Set β) → (∀ (b : β), ∃! i, b ∈ s i) → (i : α) × ↑(s i) ≃ β
-- Mathlib.Algebra.Order.Monoid.Unbundled.Pow
nsmul_le_nsmul_left_of_nonpos : ∀ {M : Type u_3} [inst : AddMonoid M] [inst_1 : Preorder M] [AddLeftMono M] {a : M} {n m : ℕ},
  a ≤ 0 → n ≤ m → m • a ≤ n • a
-- Mathlib.Analysis.Calculus.Deriv.MeanValue
/-- Let `f : ℝ → ℝ` be a differentiable function. If `f' < C`, then `f` grows slower than
`C * x` on `D`, i.e., `f y - f x < C * (y - x)` whenever `x < y`.  -/
image_sub_lt_mul_sub_of_deriv_lt : ∀ {f : ℝ → ℝ}, Differentiable ℝ f → ∀ {C : ℝ}, (∀ (x : ℝ), deriv f x < C) → ∀ ⦃x y : ℝ⦄, x < y → f y - f x < C * (y - x)
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.IsCharTwoJEqZeroNF.a₂ : ∀ {R : Type u_1} {inst : CommRing R} {W : WeierstrassCurve R} [self : W.IsCharTwoJEqZeroNF], W.a₂ = 0
-- Mathlib.Topology.OpenPartialHomeomorph.Basic
TopologicalSpace.Opens.openPartialHomeomorphSubtypeCoe_source : ∀ {X : Type u_1} [inst : TopologicalSpace X] (s : TopologicalSpace.Opens X) (hs : Nonempty ↥s),
  (s.openPartialHomeomorphSubtypeCoe hs).source = Set.univ
-- Mathlib.Analysis.Calculus.ContDiff.Operations
/-- The product map of two `C^n` functions within a set at a point is `C^n`
within the product set at the product point.  -/
ContDiffAt.prodMap' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : WithTop ℕ∞}
  {E' : Type u_3} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E'] {F' : Type u_4}
  [inst_7 : NormedAddCommGroup F'] [inst_8 : NormedSpace 𝕜 F'] {f : E → F} {g : E' → F'} {p : E × E'},
  ContDiffAt 𝕜 n f p.1 → ContDiffAt 𝕜 n g p.2 → ContDiffAt 𝕜 n (Prod.map f g) p
-- Init.Data.SInt.Bitwise
ISize.xor_assoc : ∀ (a b c : ISize), a ^^^ b ^^^ c = a ^^^ (b ^^^ c)
-- Mathlib.Order.Heyting.Basic
compl_le_hnot : ∀ {α : Type u_2} [inst : BiheytingAlgebra α] {a : α}, aᶜ ≤ ￢a
-- Init.Data.BitVec.Lemmas
BitVec.msb_cast : ∀ {w v : ℕ} (h : w = v) (x : BitVec w), (BitVec.cast h x).msb = x.msb
-- Mathlib.Data.Sym.Sym2
Sym2.coe_lift_symm_apply : ∀ {α : Type u_1} {β : Type u_2} (F : Sym2 α → β) (a₁ a₂ : α), ↑(Sym2.lift.symm F) a₁ a₂ = F s(a₁, a₂)
-- Mathlib.NumberTheory.ModularForms.LFunction
CuspForm.Λ_eq_mellin : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} [inst : Γ.IsArithmetic] {k : ℤ} (hk : 0 < k) {F : Type u_1}
  [inst_1 : FunLike F UpperHalfPlane ℂ] (f : F) [inst_2 : CuspFormClass F Γ k],
  ModularForm.Λ hk f = mellin fun t => f (↑UpperHalfPlane.ofComplex (Complex.I * ↑t))
-- Mathlib.LinearAlgebra.Multilinear.Basic
/-- **Alias** of `neg_apply`. -/
MultilinearMap.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.CategoryTheory.CatCommSq
CategoryTheory.CatCommSq.iso_hom_naturality_assoc : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄] (T : CategoryTheory.Functor C₁ C₂) (L : CategoryTheory.Functor C₁ C₃)
  (R : CategoryTheory.Functor C₂ C₄) (B : CategoryTheory.Functor C₃ C₄) [h : CategoryTheory.CatCommSq T L R B]
  {x y : C₁} (f : x ⟶ y) {Z : C₄} (h_1 : B.obj (L.obj y) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (R.map (T.map f))
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.CatCommSq.iso T L R B).hom.app y) h_1) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.CatCommSq.iso T L R B).hom.app x)
      (CategoryTheory.CategoryStruct.comp (B.map (L.map f)) h_1)
-- Mathlib.Algebra.Order.Ring.Canonical
mul_self_tsub_one : ∀ {R : Type u} [inst : CommSemiring R] [inst_1 : PartialOrder R] [CanonicallyOrderedAdd R] [inst_3 : Sub R]
  [OrderedSub R] [Std.Total fun x1 x2 => x1 ≤ x2] [AddLeftReflectLE R] (a : R), a * a - 1 = (a + 1) * (a - 1)
-- Lean.Meta.Tactic.Grind.EMatchTheorem
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.SelectM : Type → Type
-- Mathlib.Algebra.Homology.ShortComplex.ModuleCat
/-- The canonical linear map `S.X₁ →ₗ[R] LinearMap.ker S.g` induced by `S.f`.  -/
CategoryTheory.ShortComplex.moduleCatToCycles : {R : Type u} →
  [inst : Ring R] → (S : CategoryTheory.ShortComplex (ModuleCat R)) → ↑S.X₁ →ₗ[R] ↥(ModuleCat.Hom.hom S.g).ker
-- Std.Time.Format
/-- Formats a `DateTime` value into an RFC850 format string.
 -/
Std.Time.DateTime.toRFC850String : Std.Time.DateTime → String
-- Mathlib.Data.Rat.Cast.Order
Rat.preimage_cast_Ico : ∀ {K : Type u_5} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] (p q : ℚ),
  Rat.cast ⁻¹' Set.Ico ↑p ↑q = Set.Ico p q
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
/-- The pre-path object in a full subcategory of `C` induced by a pre-path object
in the category `C`.  -/
HomotopicalAlgebra.PrepathObject.toFullSubcategory : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {P : CategoryTheory.ObjectProperty C} →
      {X : P.FullSubcategory} →
        (Q : HomotopicalAlgebra.PrepathObject X.obj) → P Q.P → HomotopicalAlgebra.PrepathObject X
-- Mathlib.Algebra.Category.ModuleCat.Injective
Module.injective_module_of_injective_object : ∀ (R : Type u) (M : Type v) [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inj : CategoryTheory.Injective (ModuleCat.of R M)], Module.Injective R M
-- Mathlib.Analysis.Normed.Lp.PiLp
/-- This definition allows to endow `Π i, α i` with the Lp norm with the uniformity and bornology
being defeq to the product ones. It is useful to endow a type synonym of `Π i, α i` with the
Lp norm.  -/
PiLp.seminormedAddCommGroupToPi : (p : ENNReal) →
  {ι : Type u_2} →
    (α : ι → Type u_3) →
      [Fact (1 ≤ p)] → [Fintype ι] → [(i : ι) → SeminormedAddCommGroup (α i)] → SeminormedAddCommGroup ((i : ι) → α i)
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
FormalMultilinearSeries.fderiv_sum : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type v} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  {p : FormalMultilinearSeries 𝕜 E F} {x : E} [CompleteSpace F],
  ‖x‖ₑ < p.radius → fderiv 𝕜 p.sum x = p.derivSeries.sum x
-- Init.PropLemmas
imp_or_right_iff_true : ∀ {P Q : Prop}, Q → P ∨ Q ↔ True
-- Mathlib.Algebra.Category.ModuleCat.Biproducts
/-- The map from an arbitrary cone over an indexed family of abelian groups
to the Cartesian product of those groups.
 -/
ModuleCat.HasLimit.lift : {R : Type u} →
  [inst : Ring R] →
    {J : Type w} → (f : J → ModuleCat R) → (s : CategoryTheory.Limits.Fan f) → s.pt ⟶ ModuleCat.of R ((j : J) → ↑(f j))
-- Mathlib.CategoryTheory.Comma.LocallySmall
CategoryTheory.Under.locallySmall : ∀ {T : Type u₃} [inst : CategoryTheory.Category.{v₃, u₃} T] (X : T) [CategoryTheory.LocallySmall.{w, v₃, u₃} T],
  CategoryTheory.LocallySmall.{w, v₃, max u₃ v₃} (CategoryTheory.Under X)
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits
AlgebraicGeometry.PresheafedSpace.colimit.eq_1 : ∀ {J : Type u'} [inst : CategoryTheory.Category.{v', u'} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Limits.HasColimitsOfShape J TopCat]
  [inst_3 : ∀ (X : TopCat), CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ (TopCat.Presheaf C X)]
  (F : CategoryTheory.Functor J (AlgebraicGeometry.PresheafedSpace C)),
  AlgebraicGeometry.PresheafedSpace.colimit F =
    { carrier := CategoryTheory.Limits.colimit (F.comp (AlgebraicGeometry.PresheafedSpace.forget C)),
      presheaf := CategoryTheory.Limits.limit (AlgebraicGeometry.PresheafedSpace.pushforwardDiagramToColimit F).leftOp }
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.coe_smul' : ∀ {Γ : Type u_1} {R : Type u_3} {α : Type u_5} [inst : PartialOrder Γ] [inst_1 : AddCommMonoid R] {M : Type u_7}
  [inst_2 : SMulZeroClass M R] (m : M) (s : HahnSeries.SummableFamily Γ R α), ⇑(m • s) = m • ⇑s
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientGroup.equivQuotientZPowOfEquiv_refl : ∀ {A : Type u} [inst : CommGroup A] (n : ℤ),
  MulEquiv.refl (A ⧸ (zpowGroupHom n).range) = QuotientGroup.equivQuotientZPowOfEquiv (MulEquiv.refl A) n
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
AlgebraicGeometry.SheafedSpace.GlueData.ι_isoPresheafedSpace_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (D : AlgebraicGeometry.SheafedSpace.GlueData C)
  [inst_1 : CategoryTheory.Limits.HasLimits C] (i : D.J),
  CategoryTheory.CategoryStruct.comp (D.toPresheafedSpaceGlueData.ι i) D.isoPresheafedSpace.inv = (D.ι i).hom
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.IsBase.encard_eq_encard_of_isBase : ∀ {α : Type u_1} {M : Matroid α} {B₁ B₂ : Set α}, M.IsBase B₁ → M.IsBase B₂ → B₁.encard = B₂.encard
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get!_union_of_not_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [inst : Inhabited α] [Std.TransCmp cmp] {k : α},
  k ∉ t₂ → (t₁ ∪ t₂).get! k = t₁.get! k
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey?_eq_some_getKey : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {a : α} (h : a ∈ m), m.getKey? a = some (m.getKey a h)
-- Mathlib.Order.Filter.CountablyGenerated
Filter.isCountablyGenerated_biInf_principal : ∀ {α : Type u_1} {B : Set (Set α)}, B.Countable → (⨅ s ∈ B, Filter.principal s).IsCountablyGenerated
-- Mathlib.NumberTheory.LegendreSymbol.Complex
AddChar.FiniteField.primitiveChar_to_Complex_isPrimitive : ∀ (F : Type u_1) [inst : Field F] [inst_1 : Finite F], (AddChar.FiniteField.primitiveChar_to_Complex F).IsPrimitive
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.instSMul : {S : Type u_1} → {R : Type u_3} → {c₁ c₂ c₃ : R} → [SMul S R] → SMul S (QuaternionAlgebra R c₁ c₂ c₃)
-- Mathlib.Algebra.BigOperators.Finprod
finprod_prod_filter : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : CommMonoid M] [inst_1 : DecidableEq α] (f : β → α) (s : Finset β)
  (g : β → M), ∏ᶠ (x : α), ∏ y ∈ s with f y = x, g y = ∏ k ∈ s, g k
-- Mathlib.CategoryTheory.Limits.Final
/-- If `H` creates limits of shape `C` and `F : C ⥤ D` is initial, then `H` creates limits of shape
`D`.  -/
CategoryTheory.Functor.Initial.createsLimitsOfShapeOfInitial : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) →
          [F.Initial] →
            {E : Type u₃} →
              [inst_3 : CategoryTheory.Category.{v₃, u₃} E] →
                {B : Type u₄} →
                  [inst_4 : CategoryTheory.Category.{v₄, u₄} B] →
                    (H : CategoryTheory.Functor E B) →
                      [CategoryTheory.CreatesLimitsOfShape C H] → CategoryTheory.CreatesLimitsOfShape D H
-- Lean.DocString.Parser
Lean.Doc.Parser.UnorderedListType.ofNat_ctorIdx : ∀ (x : Lean.Doc.Parser.UnorderedListType), Lean.Doc.Parser.UnorderedListType.ofNat x.ctorIdx = x
-- Mathlib.SetTheory.ZFC.Ordinal
ZFSet.IsOrdinal.mk : ∀ {x : ZFSet.{u_1}}, x.IsTransitive → (∀ {y z w : ZFSet.{u_1}}, y ∈ z → z ∈ w → w ∈ x → y ∈ w) → x.IsOrdinal
-- Mathlib.CategoryTheory.Monoidal.Transport
/-- Analogous to `CategoryTheory.LaxMonoidalFunctor.μIso`  -/
CategoryTheory.Monoidal.InducingFunctorData.μIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategoryStruct D] →
            {F : CategoryTheory.Functor D C} →
              CategoryTheory.Monoidal.InducingFunctorData F →
                (X Y : D) →
                  CategoryTheory.MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y) ≅
                    F.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)
-- Mathlib.Computability.Primrec.List
Primrec.list_concat : ∀ {α : Type u_1} [inst : Primcodable α], Primrec₂ fun l a => l ++ [a]
-- Init.Omega.Constraint
Lean.Omega.Constraint.instToString : ToString Lean.Omega.Constraint
-- Mathlib.Data.NNRat.Defs
instAddCancelCommMonoidNNRat : AddCancelCommMonoid ℚ≥0
-- Mathlib.Topology.Sheaves.Alexandrov
Alexandrov.principalOpen_le_iff : ∀ {X : Type v} [inst : TopologicalSpace X] [inst_1 : Preorder X] [inst_2 : Topology.IsUpperSet X] {x : X}
  (U : TopologicalSpace.Opens X), Alexandrov.principalOpen x ≤ U ↔ x ∈ U
-- Mathlib.Analysis.Calculus.FDeriv.Affine
ContinuousAffineMap.differentiableWithinAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (f : E →ᴬ[𝕜] F)
  {x : E} {s : Set E}, DifferentiableWithinAt 𝕜 (⇑f) s x
-- Mathlib.AlgebraicGeometry.Morphisms.FiniteType
AlgebraicGeometry.LocallyOfFiniteType.mk : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y},
  (∀ {U : Y.Opens},
      AlgebraicGeometry.IsAffineOpen U →
        ∀ {V : X.Opens},
          AlgebraicGeometry.IsAffineOpen V →
            ∀ (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U),
              (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appLE f U V e)).FiniteType) →
    AlgebraicGeometry.LocallyOfFiniteType f
-- Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
CategoryTheory.FunctorToTypes.binaryCoproductCocone_pt_map_hom_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F G : CategoryTheory.Functor C (Type w)) {X Y : C} (f : X ⟶ Y)
  (a : F.obj X ⊕ G.obj X),
  (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.FunctorToTypes.binaryCoproductCocone F G).pt.map f)) a =
    Sum.map (⇑(CategoryTheory.ConcreteCategory.hom (F.map f))) (⇑(CategoryTheory.ConcreteCategory.hom (G.map f))) a
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
AffineSubspace.map_mono : ∀ {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁] [inst_4 : AddCommGroup V₂]
  [inst_5 : Module k V₂] [inst_6 : AddTorsor V₂ P₂] (f : P₁ →ᵃ[k] P₂) {s₁ s₂ : AffineSubspace k P₁},
  s₁ ≤ s₂ → AffineSubspace.map f s₁ ≤ AffineSubspace.map f s₂
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.mk.injEq : ∀ {R : Type u_14} {S : Type u_15} [inst : Semiring R] [inst_1 : Semiring S] {σ : R →+* S} {σ' : S →+* R}
  [inst_2 : RingHomInvPair σ σ'] [inst_3 : RingHomInvPair σ' σ] {M : Type u_16} {M₂ : Type u_17}
  [inst_4 : AddCommMonoid M] [inst_5 : AddCommMonoid M₂] [inst_6 : Module R M] [inst_7 : Module S M₂]
  (toLinearMap : M →ₛₗ[σ] M₂) (invFun : M₂ → M)
  (left_inv : autoParam (Function.LeftInverse invFun toLinearMap.toFun) Equiv.left_inv._autoParam)
  (right_inv : autoParam (Function.RightInverse invFun toLinearMap.toFun) Equiv.right_inv._autoParam)
  (toLinearMap_1 : M →ₛₗ[σ] M₂) (invFun_1 : M₂ → M)
  (left_inv_1 : autoParam (Function.LeftInverse invFun_1 toLinearMap_1.toFun) Equiv.left_inv._autoParam)
  (right_inv_1 : autoParam (Function.RightInverse invFun_1 toLinearMap_1.toFun) Equiv.right_inv._autoParam),
  ({ toLinearMap := toLinearMap, invFun := invFun, left_inv := left_inv, right_inv := right_inv } =
      { toLinearMap := toLinearMap_1, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1 }) =
    (toLinearMap = toLinearMap_1 ∧ invFun = invFun_1)
-- Std.Sat.AIG.CNF
/-- An AIG is unsat iff its CNF is unsat.
 -/
Std.Sat.AIG.toCNF_equisat : ∀ (entry : Std.Sat.AIG.Entrypoint ℕ), (Std.Sat.AIG.toCNF entry).Unsat ↔ entry.Unsat
-- Mathlib.RepresentationTheory.Homological.ContCohomology.Functoriality
ContinuousCohomology.cocyclesMap_id : ∀ {k : Type u} {G : Type v} [inst : Ring k] [inst_1 : TopologicalSpace k] [inst_2 : Group G]
  [inst_3 : TopologicalSpace G] [inst_4 : IsTopologicalGroup G] (X : TopRep k G) (n : ℕ),
  ContinuousCohomology.cocyclesMap (ContinuousMonoidHom.id G) (CategoryTheory.CategoryStruct.id X) n =
    CategoryTheory.CategoryStruct.id (ContinuousCohomology.cocycles X n)
-- Mathlib.CategoryTheory.Adjunction.Opposites
/-- If `G` is adjoint to `F` then `F.op` is adjoint to `G.op`.  -/
CategoryTheory.Adjunction.op : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C D} → {G : CategoryTheory.Functor D C} → (G ⊣ F) → (F.op ⊣ G.op)
-- Mathlib.Order.Closure
LowerAdjoint.closure_sup_closure_right : ∀ {α : Type u_1} {β : Type u_4} [inst : SemilatticeSup α] [inst_1 : Preorder β] {u : β → α} (l : LowerAdjoint u)
  (x y : α), u (l.toFun (x ⊔ u (l.toFun y))) = u (l.toFun (x ⊔ y))
-- Mathlib.Algebra.Order.Interval.Basic
NonemptyInterval.coe_sub_interval : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
  [inst_4 : AddLeftMono α] (s t : NonemptyInterval α), ↑(s - t) = ↑s - ↑t
-- Mathlib.Algebra.FiniteSupport.Basic
Function.HasFiniteSupport.of_comp : ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] {β : Type u_3} {f : β → M} {g : α → β} [inst_1 : Zero β],
  Function.HasFiniteSupport (f ∘ g) → f 0 = 0 → Function.Injective f → Function.HasFiniteSupport g
-- Mathlib.Order.Interval.Basic
Interval.boundedOrder : {α : Type u_1} → [inst : Preorder α] → [BoundedOrder α] → BoundedOrder (Interval α)