mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.mul_nc : Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Mon
-- Mathlib.Order.SupClosed
IsSublattice.prod : ∀ {α : Type u_3} {β : Type u_4} [inst : Lattice α] [inst_1 : Lattice β] {s : Set α} {t : Set β},
  IsSublattice s → IsSublattice t → IsSublattice (s ×ˢ t)
-- Mathlib.Data.Sym.Sym2
Sym2.decidablePred_mem_diagSet : (α : Type u) → [DecidableEq α] → DecidablePred fun x => x ∈ Sym2.diagSet
-- Mathlib.CategoryTheory.Adjunction.Mates
CategoryTheory.conjugateEquiv_symm_comp : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L₁ L₂ L₃ : CategoryTheory.Functor C D} {R₁ R₂ R₃ : CategoryTheory.Functor D C} (adj₁ : L₁ ⊣ R₁) (adj₂ : L₂ ⊣ R₂)
  (adj₃ : L₃ ⊣ R₃) (α : R₁ ⟶ R₂) (β : R₂ ⟶ R₃),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.conjugateEquiv adj₂ adj₃).symm β)
      ((CategoryTheory.conjugateEquiv adj₁ adj₂).symm α) =
    (CategoryTheory.conjugateEquiv adj₁ adj₃).symm (CategoryTheory.CategoryStruct.comp α β)
-- Mathlib.CategoryTheory.Monoidal.Ring
/-- The category of commutative ring objects in a cartesian monoidal category.  -/
CategoryTheory.CommRingObjCat : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] → [CategoryTheory.BraidedCategory C] → Type (max u v)
-- Mathlib.Data.Rat.Cast.CharZero
NNRat.coe_castHom : ∀ {α : Type u_3} [inst : DivisionSemiring α] [inst_1 : CharZero α], ⇑(NNRat.castHom α) = NNRat.cast
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitDisc.coe_eq_zero : ∀ {z : Complex.UnitDisc}, ↑z = 0 ↔ z = 0
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarAlgHom.injective_codRestrict : ∀ {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] [inst_3 : Star A] [inst_4 : NonUnitalNonAssocSemiring B] [inst_5 : Module R B] [inst_6 : Star B]
  [inst_7 : FunLike F A B] [inst_8 : NonUnitalAlgHomClass F R A B] [inst_9 : StarHomClass F A B] (f : F)
  (S : NonUnitalStarSubalgebra R B) (hf : ∀ (x : A), f x ∈ S),
  Function.Injective ⇑(NonUnitalStarAlgHom.codRestrict f S hf) ↔ Function.Injective ⇑f
-- Mathlib.NumberTheory.Divisors
Nat.sum_divisorsAntidiagonal : ∀ {M : Type u_1} [inst : AddCommMonoid M] (f : ℕ → ℕ → M) {n : ℕ},
  ∑ i ∈ n.divisorsAntidiagonal, f i.1 i.2 = ∑ i ∈ n.divisors, f i (n / i)
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Splitting.rightHomologyData_ι : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S : CategoryTheory.ShortComplex C} [inst_2 : CategoryTheory.Limits.HasZeroObject C] (s : S.Splitting),
  s.rightHomologyData.ι = 0
-- Init.Grind.Interactive
/-- `set_config configItem+ in tacs` executes `tacs` with the updated configuration options `configItem+`
 -/
Lean.Parser.Tactic.Grind.setConfig : Lean.ParserDescr
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Iio_inter_Ioo : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c : α}, Set.Iio a ∩ Set.Ioo b c = Set.Ioo b (min a c)
-- Mathlib.RingTheory.Ideal.Span
Ideal.span_sdiff_singleton_zero : ∀ {α : Type u} [inst : Semiring α] {s : Set α}, Ideal.span (s \ {0}) = Ideal.span s
-- Init.Data.UInt.Bitwise
UInt8.shiftRight_and : ∀ {a b c : UInt8}, (a &&& b) >>> c = a >>> c &&& b >>> c
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equifibered
/-- A natural transformation is equifibered if every commutative square of the following form is
a pullback.
```
F(X) → F(Y)
 ↓      ↓
G(X) → G(Y)
```
 -/
CategoryTheory.NatTrans.Equifibered : {J : Type u_1} →
  {C : Type u_3} →
    [inst : CategoryTheory.Category.{v_1, u_1} J] →
      [inst_1 : CategoryTheory.Category.{v_2, u_3} C] → CategoryTheory.MorphismProperty (CategoryTheory.Functor J C)
-- Mathlib.GroupTheory.Nilpotent
Subgroup.comap_upperCentralSeries : ∀ {G : Type u_1} [inst : Group G] {H : Type u_2} [inst_1 : Group H] (e : H ≃* G) (n : ℕ),
  Subgroup.comap (↑e) (Subgroup.upperCentralSeries G n) = Subgroup.upperCentralSeries H n
-- Aesop.Forward.Substitution
/-- Get the instantiation associated with level `li` in `s`. Precondition:
`li` is in the domain of `s`.  -/
Aesop.Substitution.findLevel? : Aesop.PremiseIndex → Aesop.Substitution → Option Lean.Level
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
/-- Multiplication in the colimit. See also `colimitMulAux`.  -/
MonCat.FilteredColimits.colimitMul : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    (F : CategoryTheory.Functor J MonCat) → [CategoryTheory.IsFiltered J] → Mul (MonCat.FilteredColimits.M F)
-- Mathlib.GroupTheory.Subgroup.Centralizer
AddSubgroup.mem_centralizer_singleton_iff : ∀ {G : Type u_1} [inst : AddGroup G] {g k : G}, k ∈ AddSubgroup.centralizer {g} ↔ k + g = g + k
-- Mathlib.NumberTheory.PrimeCounting
Nat.primesLE_eq_filter_Ioc_zero : ∀ (n : ℕ), n.primesLE = Finset.filter Nat.Prime (Finset.Ioc 0 n)
-- Mathlib.RingTheory.Ideal.MinimalPrime.Localization
Ideal.exists_minimalPrimes_comap_eq : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] {I : Ideal S} (f : R →+* S),
  ∀ p ∈ (Ideal.comap f I).minimalPrimes, ∃ p' ∈ I.minimalPrimes, Ideal.comap f p' = p
-- Mathlib.Data.Set.Sigma
Set.image_sigma_eq_iUnion : ∀ {ι : Type u_1} {α : ι → Type u_3} {s : Set ι} {t : (i : ι) → Set (α i)} {γ : Type u_7} (f : (i : ι) × α i → γ),
  f '' s.sigma t = ⋃ i ∈ s, f ∘ Sigma.mk i '' t i
-- Mathlib.RingTheory.Ideal.Basic
Ideal.add_pow_mem_of_pow_mem_of_le_of_commute : ∀ {α : Type u_6} [inst : Semiring α] (I : Ideal α) {a b : α} {m n k : ℕ},
  a ^ m ∈ I → b ^ n ∈ I → m + n ≤ k + 1 → Commute a b → (a + b) ^ k ∈ I
-- Mathlib.AlgebraicGeometry.Normalization
AlgebraicGeometry.Scheme.Hom.toNormalization_inr_normalizationCoprodIso_hom : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.QuasiCompact f]
  [inst_1 : AlgebraicGeometry.QuasiSeparated f] {U V : AlgebraicGeometry.Scheme} {iU : U ⟶ X} {iV : V ⟶ X}
  (e : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk iU iV))
  [inst_2 : AlgebraicGeometry.QuasiCompact iU] [inst_3 : AlgebraicGeometry.QuasiSeparated iU]
  [inst_4 : AlgebraicGeometry.QuasiCompact iV] [inst_5 : AlgebraicGeometry.QuasiSeparated iV],
  CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.Scheme.Hom.toNormalization (CategoryTheory.CategoryStruct.comp iV f))
      (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr
        (AlgebraicGeometry.Scheme.Hom.normalizationCoprodIso f e).hom) =
    CategoryTheory.CategoryStruct.comp iV (AlgebraicGeometry.Scheme.Hom.toNormalization f)
-- Mathlib.RingTheory.Smooth.Quotient
/-- A pure `RingHom` variant of `Algebra.FormallySmooth.of_surjective_of_ker_eq_map_of_flat`  -/
RingHom.FormallySmooth.of_flat_of_ker_eq_map_of_square_zero : ∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] {R' : Type u_3} {S' : Type u_4}
  [inst_2 : CommRing R'] [inst_3 : CommRing S'] (f : R →+* S),
  f.Flat →
    ∀ (qR : R →+* R') (qS : S →+* S') (g : R' →+* S'),
      Function.Surjective ⇑qR →
        Function.Surjective ⇑qS →
          qS.comp f = g.comp qR →
            RingHom.ker qR ^ 2 = ⊥ → RingHom.ker qS = Ideal.map f (RingHom.ker qR) → g.FormallySmooth → f.FormallySmooth
-- Lean.Data.Lsp.Basic
Lean.Lsp.DocumentChange.edit.sizeOf_spec : ∀ (a : Lean.Lsp.TextDocumentEdit), sizeOf (Lean.Lsp.DocumentChange.edit a) = 1 + sizeOf a
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
HasProdUniformlyOn_sineTerm_prod_on_compact : ∀ {Z : Set ℂ},
  Z ⊆ Complex.integerComplement →
    IsCompact Z →
      HasProdUniformlyOn (fun n z => 1 + sineTerm z n) (fun x => Complex.sin (↑Real.pi * x) / (↑Real.pi * x)) Z
-- Mathlib.Topology.Algebra.Group.Quotient
QuotientAddGroup.t1Space_iff : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [SeparatelyContinuousAdd G] {N : AddSubgroup G},
  T1Space (G ⧸ N) ↔ IsClosed ↑N
-- Init.Data.Range.Polymorphic.PRange
/-- This type class ensures that the intersection according to `Rcc.HasRcoIntersection`
of two ranges contains exactly those elements that are contained in both ranges.
 -/
Std.Rcc.LawfulRcoIntersection : (α : Type w) → [LT α] → [LE α] → [Std.Rcc.HasRcoIntersection α] → Prop
-- Mathlib.Algebra.Group.Fin.Tuple
Fin.insertNth_one_right : ∀ {n : ℕ} {α : Fin (n + 1) → Type u_1} [inst : (j : Fin (n + 1)) → One (α j)] (i : Fin (n + 1)) (x : α i),
  i.insertNth x 1 = Pi.mulSingle i x
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.SavedState.mk.sizeOf_spec : ∀ («meta» : Lean.Meta.SavedState) (grind : Lean.Meta.Grind.State),
  sizeOf { «meta» := «meta», grind := grind } = 1 + sizeOf «meta» + sizeOf grind
-- Init.Data.SInt.Basic
instXorOpInt64 : XorOp Int64
-- Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients
/-- **Alias** of `Ring.HasFiniteQuotients.finite_setOfPred_mem`. -/
Ring.HasFiniteQuotients.finite_setOf_mem : ∀ {R : Type u_1} [inst : CommRing R] [Ring.HasFiniteQuotients R] (x : R), x ≠ 0 → {I | x ∈ I}.Finite
-- Mathlib.AlgebraicGeometry.Modules.Tilde
AlgebraicGeometry.tilde.map_id_assoc : ∀ {R : CommRingCat} {M : ModuleCat ↑R} {Z : (AlgebraicGeometry.Spec R).Modules} (h : AlgebraicGeometry.tilde M ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.tilde.map (CategoryTheory.CategoryStruct.id M)) h = h
-- Mathlib.RingTheory.HahnSeries.Addition
HahnSeries.order_smul_not_lt : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] {V : Type u_8} [inst_1 : Zero V] [inst_2 : SMulZeroClass R V]
  [inst_3 : Zero Γ] (r : R) (x : HahnSeries Γ V), r • x ≠ 0 → ¬(r • x).order < x.order
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.comap_top : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B] (f : A →ₐ[R] B), Subalgebra.comap f ⊤ = ⊤
-- Mathlib.Order.SuccPred.Basic
Order.pred_succ : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : PredOrder α] [inst_2 : SuccOrder α] [NoMaxOrder α] (a : α),
  Order.pred (Order.succ a) = a
-- Mathlib.Analysis.SpecialFunctions.Integrals.Basic
/-- The reduction formula for the integral of `cos x ^ n` for any natural `n ≥ 2`.  -/
integral_cos_pow : ∀ {a b : ℝ} (n : ℕ),
  ∫ (x : ℝ) in a..b, Real.cos x ^ (n + 2) =
    (Real.cos b ^ (n + 1) * Real.sin b - Real.cos a ^ (n + 1) * Real.sin a) / (↑n + 2) +
      (↑n + 1) / (↑n + 2) * ∫ (x : ℝ) in a..b, Real.cos x ^ n
-- Mathlib.Algebra.Group.Subgroup.Ker
AddSubgroup.comap_map_eq_self : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] {f : G →+ N} {H : AddSubgroup G},
  f.ker ≤ H → AddSubgroup.comap f (AddSubgroup.map f H) = H
-- Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
WeierstrassCurve.integralModel_a₁_eq : ∀ (R : Type u_1) [inst : CommRing R] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra R K] (W : WeierstrassCurve K)
  [hW : WeierstrassCurve.IsIntegral R W], (algebraMap R K) (WeierstrassCurve.integralModel R W).a₁ = W.a₁
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.Const.getEntryGE? : {α : Type u} → {β : Type v} → [Ord α] → α → (Std.DTreeMap.Internal.Impl α fun x => β) → Option (α × β)
-- Init.Data.Range.Polymorphic.Basic
Std.Rco.lower_le_of_mem : ∀ {α : Type u} {r : Std.Rco α} {a : α} [inst : LE α] [inst_1 : LT α], a ∈ r → r.lower ≤ a
-- Mathlib.Topology.Semicontinuity.Defs
/-- A function `f : α → Set β` is lower hemicontinuous at `x` within a set `s` if, whenever `t` is
an open set intersecting `f x`, then `t` also intersects `f x'` for all `x'` sufficiently close to
`x` within `s`.  -/
LowerHemicontinuousWithinAt : {α : Type u_1} → {β : Type u_2} → [TopologicalSpace α] → [TopologicalSpace β] → (α → Set β) → Set α → α → Prop
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
AddSubmonoid.coe_op : ∀ {M : Type u_2} [inst : AddZeroClass M] (x : AddSubmonoid M), ↑x.op = AddOpposite.unop ⁻¹' ↑x
-- Init.Data.Order.PackageFactories
Std.PartialOrderPackage.mk : {α : Type u} →
  [toPreorderPackage : Std.PreorderPackage α] → (∀ (a b : α), a ≤ b → b ≤ a → a = b) → Std.PartialOrderPackage α
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- The characteristic maps are continuous when restricting to `closedBall 0 1`.  -/
Topology.CWComplex.continuousOn : ∀ {X : Type u} {inst : TopologicalSpace X} {C : Set X} [self : Topology.CWComplex C] (n : ℕ)
  (i : Topology.CWComplex.cell C n), ContinuousOn (↑(Topology.CWComplex.map n i)) (Metric.closedBall 0 1)
-- Init.Data.Int.DivMod.Lemmas
Int.mul_sub_bmod_self_right : ∀ (a : ℤ) (b : ℕ) (c : ℤ), (a * ↑b - c).bmod b = (-c).bmod b
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
AddLECancellable.injective_left : ∀ {α : Type u_1} [inst : Add α] [IsAddCommutative α] [inst_2 : PartialOrder α] {a : α},
  AddLECancellable a → Function.Injective fun x => x + a
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
/-- In a countably generated measurable space, the atoms are measurable.  -/
MeasurableSpace.measurableSet_measurableAtom : ∀ {α : Type u_1} {mα : MeasurableSpace α} [MeasurableSpace.CountablyGenerated α] (x : α),
  MeasurableSet (measurableAtom x)
-- Mathlib.Topology.Closure
subset_interior_iff : ∀ {X : Type u} [inst : TopologicalSpace X] {s t : Set X}, t ⊆ interior s ↔ ∃ U, IsOpen U ∧ t ⊆ U ∧ U ⊆ s
-- Mathlib.CategoryTheory.MorphismProperty.Limits
/-- `P` has pushouts if for every `f` satisfying `P`, pushouts of arbitrary morphisms along `f`
exist.  -/
CategoryTheory.MorphismProperty.HasPushouts : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.MorphismProperty C → Prop
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- The orbits of a normal subgroup form a block system  -/
MulAction.IsBlockSystem.of_normal : ∀ {G : Type u_1} [inst : Group G] {X : Type u_2} [inst_1 : MulAction G X] {N : Subgroup G} [N.Normal],
  MulAction.IsBlockSystem G (Set.range fun a => MulAction.orbit (↥N) a)
-- Mathlib.Data.NNRat.Defs
NNRat.abs_coe : ∀ (q : ℚ≥0), |↑q| = ↑q
-- Mathlib.RingTheory.DividedPowerAlgebra.Init
DividedPowerAlgebra.LinearMap.dp_mul : ∀ {R : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {S : Type u_4}
  [inst_3 : CommSemiring S] {N : Type u_5} [inst_4 : AddCommMonoid N] [inst_5 : Module R N] [inst_6 : Module S N]
  (f : M →ₗ[R] N) {m n : ℕ} {a : M},
  DividedPowerAlgebra.dp S m (f a) * DividedPowerAlgebra.dp S n (f a) =
    (m + n).choose m • DividedPowerAlgebra.dp S (m + n) (f a)
-- Mathlib.Algebra.Category.Grp.Injective
Module.Baer.of_divisible : ∀ (A : Type u) [inst : AddCommGroup A] [DivisibleBy A ℤ], Module.Baer ℤ A
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.braiding_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.SymmetricCategory C] (M N : CategoryTheory.AddMon C), (β_ M N).hom.hom = (β_ M.X N.X).hom
-- Mathlib.RingTheory.OrzechProperty
OrzechProperty.injective_of_surjective_of_injective : ∀ {R : Type u} [inst : Semiring R] [OrzechProperty R] {M : Type v} [inst_2 : AddCommMonoid M] [inst_3 : Module R M]
  [Module.Finite R M] {N : Type w} [inst_5 : AddCommMonoid N] [inst_6 : Module R N] (i f : N →ₗ[R] M),
  Function.Injective ⇑i → Function.Surjective ⇑f → Function.Injective ⇑f
-- Mathlib.CategoryTheory.Monoidal.Grp
/-- Constructor for morphisms in `AddGrp C`.  -/
CategoryTheory.AddGrp.homMk'' : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      {A B : CategoryTheory.AddGrp C} →
        (f : A.X ⟶ B.X) →
          autoParam (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.zero f = CategoryTheory.AddMonObj.zero)
              CategoryTheory.AddGrp.homMk''._auto_1 →
            autoParam
                (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add f =
                  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f f)
                    CategoryTheory.AddMonObj.add)
                CategoryTheory.AddGrp.homMk''._auto_3 →
              (A ⟶ B)
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.instAddCommGroup : {R : Type u_1} → {a b : R} → [AddCommGroup R] → AddCommGroup (QuadraticAlgebra R a b)
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
/-- Simplification procedure for multiplication of `BitVec`s.  -/
BitVec.reduceMul : Lean.Meta.Simp.DSimproc
-- Mathlib.Probability.Kernel.Basic
ProbabilityTheory.Kernel.instIsFiniteKernelBoolBoolKernelOfIsFiniteMeasure : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ]
  [MeasureTheory.IsFiniteMeasure ν], ProbabilityTheory.IsFiniteKernel (ProbabilityTheory.Kernel.boolKernel μ ν)
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.biproduct.isoProduct_hom : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {f : J → C} [inst_2 : CategoryTheory.Limits.HasBiproduct f],
  (CategoryTheory.Limits.biproduct.isoProduct f).hom =
    CategoryTheory.Limits.Pi.lift (CategoryTheory.Limits.biproduct.π f)
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
/-- A global section of a quasi-compact scheme is nilpotent if and only if its associated
basic open is empty.  -/
AlgebraicGeometry.Scheme.isNilpotent_iff_basicOpen_eq_bot : ∀ {X : AlgebraicGeometry.Scheme} [CompactSpace ↥X] (f : ↑(X.presheaf.obj (Opposite.op ⊤))),
  IsNilpotent f ↔ X.basicOpen f = ⊥
-- Mathlib.Data.ENNReal.Holder
ENNReal.HolderTriple.instInfty : ∀ (p : ENNReal), p.HolderTriple ⊤ p
-- Mathlib.MeasureTheory.PiSystem
generatePiSystem.base : ∀ {α : Type u_1} {S : Set (Set α)} {s : Set α}, s ∈ S → generatePiSystem S s
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Adjunction.IsMonoidal.leftAdjoint_μ : ∀ {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.MonoidalCategory D}
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} {adj : F ⊣ G} {inst_4 : F.OplaxMonoidal}
  {inst_5 : G.LaxMonoidal} [self : adj.IsMonoidal] (X Y : D),
  CategoryTheory.Functor.LaxMonoidal.μ G X Y =
    CategoryTheory.CategoryStruct.comp
      (adj.unit.app (CategoryTheory.MonoidalCategoryStruct.tensorObj (G.obj X) (G.obj Y)))
      (G.map
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.δ F (G.obj X) (G.obj Y))
          (CategoryTheory.MonoidalCategoryStruct.tensorHom (adj.counit.app X) (adj.counit.app Y))))
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.PrettyPrinter.Delaborator.TopDownAnalyze.tryUnify : Lean.Expr → Lean.Expr → Lean.PrettyPrinter.Delaborator.TopDownAnalyze.AnalyzeM Unit
-- Mathlib.RingTheory.AdicCompletion.Algebra
AdicCompletion.instNatCast : {R : Type u_1} → [inst : CommRing R] → (I : Ideal R) → NatCast (AdicCompletion I R)
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
MonoidAlgebra.coeff_map : ∀ {R : Type u_3} {S : Type u_4} {M : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+ S)
  (x : MonoidAlgebra R M), (MonoidAlgebra.map f x).coeff = Finsupp.mapRange ⇑f ⋯ x.coeff
-- Mathlib.Order.LiminfLimsup
/-- The `bliminf` of a function `u` along a filter `f`, bounded by a predicate `p`, is the supremum
of the `a` such that the inequality `a ≤ u x` eventually holds for `f` whenever `p x` holds.  -/
Filter.bliminf : {α : Type u_1} → {β : Type u_2} → [ConditionallyCompleteLattice α] → (β → α) → Filter β → (β → Prop) → α
-- Mathlib.AlgebraicGeometry.RelativeGluing
AlgebraicGeometry.Scheme.Cover.RelativeGluingData.equifibered : ∀ {S : AlgebraicGeometry.Scheme} {𝒰 : S.OpenCover} [inst : CategoryTheory.Category.{u_2, u_1} 𝒰.I₀]
  [inst_1 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰]
  (self : AlgebraicGeometry.Scheme.Cover.RelativeGluingData 𝒰), CategoryTheory.NatTrans.Equifibered self.natTrans
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtensionAt.hasPointwiseLeftKanExtensionAt : ∀ {C : Type u_1} {D : Type u_2} {H : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_4, u_4} H]
  {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} {E : L.LeftExtension F} {Y : D}
  (h : E.IsPointwiseLeftKanExtensionAt Y), L.HasPointwiseLeftKanExtensionAt F Y
-- Lean.Message
Lean.instToJsonMessageSeverity.toJson : Lean.MessageSeverity → Lean.Json
-- Mathlib.MeasureTheory.Function.AEEqOfIntegral
MeasureTheory.ae_eq_zero_of_forall_dual : ∀ {α : Type u_1} {E : Type u_2} (𝕜 : Type u_3) {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : RCLike 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [SecondCountableTopology E] {f : α → E},
  (∀ (c : StrongDual 𝕜 E), (fun x => c (f x)) =ᵐ[μ] 0) → f =ᵐ[μ] 0
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.integral_cases : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {μ : MeasureTheory.Measure ℝ} (f : ℝ → E)
  (a b : ℝ), ∫ (x : ℝ) in a..b, f x ∂μ ∈ {∫ (x : ℝ) in Set.uIoc a b, f x ∂μ, -∫ (x : ℝ) in Set.uIoc a b, f x ∂μ}
-- Init.Sym.Lemmas
Lean.Sym.Fin.lt_eq_false : ∀ {n : ℕ} (a b : Fin n), decide (a < b) = false → (a < b) = False
-- Mathlib.CategoryTheory.Category.Pointed
/-- The category of pointed types.  -/
Pointed : Type (u + 1)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get_ofList_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} [inst : LawfulBEq α] {l : List ((a : α) × β a)}
  {k k' : α} (k_beq : (k == k') = true) {v : β k},
  List.Pairwise (fun a b => (a.fst == b.fst) = false) l →
    ⟨k, v⟩ ∈ l → ∀ {h : k' ∈ Std.ExtDHashMap.ofList l}, (Std.ExtDHashMap.ofList l).get k' h = cast ⋯ v
-- Lean.Parser.Command
Lean.Parser.Command.mutual : Lean.Parser.Parser
-- Mathlib.GroupTheory.GroupAction.Hom
/-- Reinterpret an equivariant additive monoid homomorphism as an additive monoid homomorphism.  -/
DistribMulActionHom.toAddMonoidHom : {M : Type u_1} →
  [inst : Monoid M] →
    {N : Type u_2} →
      [inst_1 : Monoid N] →
        {φ : M →* N} →
          {A : Type u_10} →
            [inst_2 : AddMonoid A] →
              [inst_3 : DistribMulAction M A] →
                {B : Type u_11} → [inst_4 : AddMonoid B] → [inst_5 : DistribMulAction N B] → (A →ₑ+[φ] B) → A →+ B
-- Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Subalgebra.bot_eq_top_iff_rank_eq_one : ∀ {F : Type u_1} {E : Type u_2} [inst : CommRing F] [StrongRankCondition F] [inst_2 : Ring E] [inst_3 : Algebra F E]
  [Nontrivial E] [Module.Free F E], ⊥ = ⊤ ↔ Module.rank F E = 1
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
SheafOfModules.QuasicoherentData.localGeneratorsData_generators : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : ∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat]
  [inst_2 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R}
  (q : M.QuasicoherentData) (i : q.I), q.localGeneratorsData.generators i = (q.presentation i).generators
-- Init.SizeOf
Except.error.sizeOf_spec : ∀ {ε : Type u} {α : Type v} [inst : SizeOf ε] [inst_1 : SizeOf α] (a : ε), sizeOf (Except.error a) = 1 + sizeOf a
-- Mathlib.Algebra.GroupWithZero.Semiconj
Commute.zpow_right₀ : ∀ {G₀ : Type u_1} [inst : GroupWithZero G₀] {a b : G₀}, Commute a b → ∀ (m : ℤ), Commute a (b ^ m)