mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Finmap
Multiset.NodupKeys.nodup : ∀ {α : Type u} {β : α → Type v} {m : Multiset ((a : α) × β a)}, m.NodupKeys → m.Nodup
-- Mathlib.CategoryTheory.Limits.Preserves.Finite
CategoryTheory.Limits.instReflectsFiniteProductsOfReflectsFiniteLimits : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.ReflectsFiniteLimits F],
  CategoryTheory.Limits.ReflectsFiniteProducts F
-- Mathlib.Analysis.ODE.PicardLindelof
ODE.picard_apply : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E → E} {α : ℝ → E} {t₀ : ℝ} {x₀ : E}
  {t : ℝ}, ODE.picard f t₀ x₀ α t = x₀ + ∫ (τ : ℝ) in t₀..t, f τ (α τ)
-- Mathlib.Algebra.Group.Units.Basic
Units.mul_eq_one_iff_inv_eq : ∀ {α : Type u} [inst : Monoid α] {u : αˣ} {a : α}, ↑u * a = 1 ↔ ↑u⁻¹ = a
-- Mathlib.Algebra.Star.StarRingHom
/-- A *non-unital ⋆-ring homomorphism* is a non-unital ring homomorphism between non-unital
non-associative semirings `A` and `B` equipped with a `star` operation, and this homomorphism is
also `star`-preserving.  -/
NonUnitalStarRingHom : (A : Type u_1) →
  (B : Type u_2) →
    [NonUnitalNonAssocSemiring A] → [Star A] → [NonUnitalNonAssocSemiring B] → [Star B] → Type (max u_1 u_2)
-- Mathlib.Topology.ContinuousMap.Algebra
/-- Coercion to a function as a `MonoidHom`. Similar to `MonoidHom.coeFn`.  -/
ContinuousMap.coeFnMonoidHom : {α : Type u_1} →
  {β : Type u_2} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] → [inst_2 : Monoid β] → [inst_3 : ContinuousMul β] → C(α, β) →* α → β
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.degree_eq_natDegree : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p ≠ 0 → p.degree = ↑p.natDegree
-- Lean.Elab.Command
/-- Option for showing elaboration errors from partial syntax errors.  -/
Lean.Elab.Command.showPartialSyntaxErrors : Lean.Option Bool
-- Mathlib.Topology.Algebra.Valued.LocallyCompact
Valued.integer.properSpace_iff_compactSpace_integer : ∀ {K : Type u_1} {Γ₀ : Type u_2} [inst : Field K] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] [inst_2 : Valued K Γ₀]
  [inst_3 : Valued.v.RankOne], ProperSpace K ↔ CompactSpace ↥(Valued.integer K)
-- Mathlib.LinearAlgebra.Basis.Submodule
Module.Basis.restrictScalars_repr_apply : ∀ {ι : Type u_1} (R : Type u_3) {M : Type u_5} {S : Type u_7} [inst : CommRing R] [inst_1 : IsDomain R]
  [inst_2 : Ring S] [inst_3 : Nontrivial S] [inst_4 : AddCommGroup M] [inst_5 : Algebra R S] [inst_6 : Module S M]
  [inst_7 : Module R M] [inst_8 : IsScalarTower R S M] [inst_9 : Module.IsTorsionFree R S] (b : Module.Basis ι S M)
  (m : ↥(Submodule.span R (Set.range ⇑b))) (i : ι),
  (algebraMap R S) (((Module.Basis.restrictScalars R b).repr m) i) = (b.repr ↑m) i
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.OplaxMonoidal.δ_natural_left_assoc : ∀ {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) [self : F.OplaxMonoidal] {X Y : C} (f : X ⟶ Y) (X' : C) {Z : D}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (F.obj Y) (F.obj X') ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.δ F X X')
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (F.map f) (F.obj X')) h) =
    CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X'))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.δ F Y X') h)
-- Mathlib.Topology.Compactness.Compact
IsCompact.elim_nhds_subcover : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X},
  IsCompact s → ∀ (U : X → Set X), (∀ x ∈ s, U x ∈ nhds x) → ∃ t, (∀ x ∈ t, x ∈ s) ∧ s ⊆ ⋃ x ∈ t, U x
-- Lean.Parser.Term
Lean.Parser.Term.matchExpr : Lean.Parser.Parser
-- Mathlib.Topology.Sheaves.MayerVietoris
Opens.mayerVietorisSquare_X₂ : ∀ {T : Type u} [inst : TopologicalSpace T] (U V : TopologicalSpace.Opens T), (Opens.mayerVietorisSquare U V).X₂ = U
-- Mathlib.Topology.Connected.Clopen
/-- The quotient of a space by its connected components  -/
ConnectedComponents : (α : Type u) → [TopologicalSpace α] → Type u
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.Precomp.map_comp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {n : ℕ} (F : CategoryTheory.ComposableArrows C n) {X : C}
  (f : X ⟶ F.left) {i j k : Fin (n + 1 + 1)} (hij : i ≤ j) (hjk : j ≤ k),
  CategoryTheory.ComposableArrows.Precomp.map F f i k ⋯ =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.Precomp.map F f i j hij)
      (CategoryTheory.ComposableArrows.Precomp.map F f j k hjk)
-- Mathlib.RingTheory.Coprime.Lemmas
Finset.prod_dvd_of_isRelPrime : ∀ {α : Type u_2} {I : Type u_1} [inst : CommMonoid α] [DecompositionMonoid α] {z : α} {s : I → α} {t : Finset I},
  (↑t).Pairwise (Function.onFun IsRelPrime s) → (∀ i ∈ t, s i ∣ z) → ∏ x ∈ t, s x ∣ z
-- Batteries.Data.Float.Lemmas
_private.Batteries.Data.Float.Lemmas.0.Float.Model.UnpackedFloat.pack.match_1.splitter : (motive : Float.Model.UnpackedFloat → Sort u_1) →
  (x : Float.Model.UnpackedFloat) →
    (Unit → motive Float.Model.UnpackedFloat.notANumber) →
      ((s : Float.Model.UnpackedFloat.Sign) → motive (Float.Model.UnpackedFloat.infinity s)) →
        ((s : Float.Model.UnpackedFloat.Sign) → motive (Float.Model.UnpackedFloat.zero s)) →
          ((s : Float.Model.UnpackedFloat.Sign) →
              (m : ℕ) →
                (e : ℤ) → (mantissa_pos : 0 < m) → motive (Float.Model.UnpackedFloat.finite s m e mantissa_pos)) →
            motive x
-- Mathlib.LinearAlgebra.Orientation
/-- A module `M` over a linearly ordered commutative ring has precisely two "orientations" with
respect to an empty index type. (Note that these are only orientations of `M` of in the conventional
mathematical sense if `M` is zero-dimensional.)  -/
Orientation.eq_or_eq_neg_of_isEmpty : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : LinearOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] {ι : Type u_3} [inst_5 : IsEmpty ι] (o : Orientation R M ι),
  o = positiveOrientation ∨ o = -positiveOrientation
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.UInt
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.UInt.0.UInt8.fromExpr : Lean.Expr → Lean.Meta.SimpM (Option UInt8)
-- Mathlib.Data.Matrix.Mul
Matrix.mulVec_apply_eq_sum : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : NonUnitalNonAssocSemiring α] [inst_1 : Fintype n]
  (M : Matrix m n α) (v : n → α) (i : m), M.mulVec v i = ∑ j, M i j * v j
-- Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
CategoryTheory.Functor.RightLinear.toOplaxRightLinear : {D : Type u_1} →
  {D' : Type u_2} →
    {inst : CategoryTheory.Category.{v_1, u_1} D} →
      {inst_1 : CategoryTheory.Category.{v_2, u_2} D'} →
        {F : CategoryTheory.Functor D D'} →
          {C : Type u_3} →
            {inst_2 : CategoryTheory.Category.{v_3, u_3} C} →
              {inst_3 : CategoryTheory.MonoidalCategory C} →
                {inst_4 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D} →
                  {inst_5 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D'} →
                    [self : F.RightLinear C] → F.OplaxRightLinear C
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.coe_injective : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E]
  [inst_7 : Module R₂ E₂], Function.Injective DFunLike.coe
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.whiskerLeft_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {G H : CategoryTheory.AddGrp C} (f : G ⟶ H) (I : CategoryTheory.AddGrp C),
  (CategoryTheory.MonoidalCategoryStruct.whiskerRight f I).hom.hom =
    CategoryTheory.MonoidalCategoryStruct.whiskerRight f.hom.hom I.X
-- Mathlib.Data.ZMod.Basic
ZMod.intCast_eq_intCast_iff' : ∀ (a b : ℤ) (c : ℕ), ↑a = ↑b ↔ a % ↑c = b % ↑c
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
CategoryTheory.Functor.isZero_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  [CategoryTheory.Limits.HasZeroObject D] (F : CategoryTheory.Functor C D),
  CategoryTheory.Limits.IsZero F ↔ ∀ (X : C), CategoryTheory.Limits.IsZero (F.obj X)
-- Mathlib.SetTheory.Cardinal.Continuum
Cardinal.continuum_mul_self : Cardinal.continuum * Cardinal.continuum = Cardinal.continuum
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonHoverParams.fromJson : Lean.Json → Except String Lean.Lsp.HoverParams
-- Std.Data.DHashMap.Raw
/-- Checks if a mapping for the given key exists and returns the key if it does, otherwise `fallback`.
If a mapping exists the result is guaranteed to be pointer equal to the key in the map.
 -/
Std.DHashMap.Raw.getKeyD : {α : Type u} → {β : α → Type v} → [BEq α] → [Hashable α] → Std.DHashMap.Raw α β → α → α → α
-- Lean.Compiler.IR.Basic
Lean.IR.Arg.alphaEqv : Lean.IR.IndexRenaming → Lean.IR.Arg → Lean.IR.Arg → Bool
-- Mathlib.RingTheory.TensorProduct.IsBaseChangeFree
IsBaseChange.of_basis : ∀ {R : Type u_1} [inst : CommSemiring R] {V : Type u_2} [inst_1 : AddCommMonoid V] [inst_2 : Module R V] (A : Type u_3)
  [inst_3 : CommSemiring A] [inst_4 : Algebra A R] [inst_5 : Module A V] [inst_6 : IsScalarTower A R V] {ι : Type u_4}
  (b : Module.Basis ι R V), IsBaseChange R (Finsupp.linearCombination A ⇑b)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
lt_of_add_lt_of_nonneg_right : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α] [AddRightMono α] {a b c : α}, a + b < c → 0 ≤ a → b < c
-- Mathlib.GroupTheory.Perm.Fin
Fin.cons_removeNth_eq_comp_cycleRange_symm : ∀ {n : ℕ} {α : Type u_1} (x : Fin (n + 1) → α) (p : Fin (n + 1)),
  Fin.cons (x p) (p.removeNth x) = x ∘ ⇑(Equiv.symm p.cycleRange)
-- Mathlib.CategoryTheory.Iso
CategoryTheory.Iso.map_inv_hom_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  {X Y : C} (e : X ≅ Y) (F : CategoryTheory.Functor C D),
  CategoryTheory.CategoryStruct.comp (F.map e.inv) (F.map e.hom) = CategoryTheory.CategoryStruct.id (F.obj Y)
-- Lean.Data.KVMap
/-- A key-value map. We use it to represent user-selected options and `Expr.mdata`.

Remark: we do not use a Lean `Std.TreeMap` here because we need to manipulate `KVMap` objects in
C++ and `Std.TreeMap` is implemented in Lean. So, we use just a `List` until we can
generate C++ code from Lean code.
 -/
Lean.KVMap : Type
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
mabs_dite : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : Group α] (p : Prop) [inst_2 : Decidable p] (a : p → α) (b : ¬p → α),
  |if h : p then a h else b h|ₘ = if h : p then |a h|ₘ else |b h|ₘ
-- Mathlib.Algebra.Order.Monoid.Defs
mul_self_le_one_iff : ∀ {α : Type u_1} [inst : CommMonoid α] [inst_1 : LinearOrder α] [IsOrderedMonoid α] {a : α}, a * a ≤ 1 ↔ a ≤ 1
-- Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
_private.Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic.0.CategoryTheory.Limits.compNatIso.match_1.eq_2 : ∀ (motive : CategoryTheory.Limits.WalkingParallelPair → Sort u_1)
  (h_1 : Unit → motive CategoryTheory.Limits.WalkingParallelPair.zero)
  (h_2 : Unit → motive CategoryTheory.Limits.WalkingParallelPair.one),
  (match CategoryTheory.Limits.WalkingParallelPair.one with
    | CategoryTheory.Limits.WalkingParallelPair.zero => h_1 ()
    | CategoryTheory.Limits.WalkingParallelPair.one => h_2 ()) =
    h_2 ()
-- Mathlib.Data.Quot
Quotient.map'_mk : ∀ {α : Sort u_1} {β : Sort u_2} {s : Setoid α} {t : Setoid β} (f : α → β) (h : ∀ (a b : α), s a b → t (f a) (f b))
  (x : α), Quotient.map' f h ⟦x⟧ = ⟦f x⟧
-- Mathlib.GroupTheory.Congruence.Defs
Con.conGen_iSup : ∀ {M : Type u_1} [inst : Mul M] {ι : Sort u_4} (r : ι → M → M → Prop), conGen (iSup r) = ⨆ i, conGen (r i)
-- Mathlib.Data.Finset.Empty
Finset.coe_empty : ∀ {α : Type u_1}, ↑∅ = ∅
-- Mathlib.ModelTheory.ElementaryMaps
FirstOrder.Language.ElementaryEmbedding.instInhabited : {L : FirstOrder.Language} → {M : Type u_1} → [inst : L.Structure M] → Inhabited (L.ElementaryEmbedding M M)
-- Lean.Parser.Extension
Lean.Parser.ParserAliasInfo.declName : Lean.Parser.ParserAliasInfo → Lean.Name
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rii.mem_toList : ∀ {α : Type u} {r : Std.Rii α} [inst : Std.PRange.Least? α] [inst_1 : Std.PRange.UpwardEnumerable α]
  [inst_2 : Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLeast? α]
  [inst_4 : Std.Rxi.IsAlwaysFinite α] {a : α}, a ∈ r.toList
-- Lean.Data.JsonRpc
Lean.JsonRpc.ErrorCode.invalidRequest.sizeOf_spec : sizeOf Lean.JsonRpc.ErrorCode.invalidRequest = 1
-- Mathlib.Analysis.Convex.SpecificFunctions.Deriv
_private.Mathlib.Analysis.Convex.SpecificFunctions.Deriv.0.Nat.iterate.match_1.eq_2 : ∀ {α : Sort u_2} (motive : ℕ → α → Sort u_1) (k : ℕ) (a : α) (h_1 : (a : α) → motive 0 a)
  (h_2 : (k : ℕ) → (a : α) → motive k.succ a),
  (match k.succ, a with
    | 0, a => h_1 a
    | k.succ, a => h_2 k a) =
    h_2 k a
-- Std.Http.Data.URI.Parser
_private.Std.Http.Data.URI.Parser.0.Std.Http.URI.Parser.parseRequestTarget.absoluteFromScheme : Std.Http.URI.Config → Std.Http.URI.Scheme → Std.Internal.Parsec.ByteArray.Parser Std.Http.RequestTarget
-- Mathlib.Order.Heyting.Hom
BiheytingHomClass.toLatticeHomClass : ∀ {F : Type u_6} {α : Type u_7} {β : Type u_8} {inst : BiheytingAlgebra α} {inst_1 : BiheytingAlgebra β}
  {inst_2 : FunLike F α β} [self : BiheytingHomClass F α β], LatticeHomClass F α β
-- Init.Data.List.TakeDrop
List.set_drop : ∀ {α : Type u_1} {l : List α} {i j : ℕ} {a : α}, (List.drop i l).set j a = List.drop i (l.set (i + j) a)
-- Mathlib.Algebra.Polynomial.AlgebraMap
/-- *McCoy theorem*: a polynomial `P : R[X]` is a zerodivisor if and only if there is `a : R`
such that `a ≠ 0` and `a • P = 0`.  -/
Polynomial.notMem_nonZeroDivisors_iff : ∀ {R : Type u} [inst : CommSemiring R] {P : Polynomial R}, P ∉ nonZeroDivisors (Polynomial R) ↔ ∃ a, a ≠ 0 ∧ a • P = 0
-- Mathlib.Order.Filter.AtTopBot.Defs
Filter.eventually_ne_atBot : ∀ {α : Type u_3} [inst : Preorder α] [NoBotOrder α] (a : α), ∀ᶠ (x : α) in Filter.atBot, x ≠ a
-- Std.Do.WP.SimpLemmas
Option.tryCatch.eq_2 : ∀ {α : Type u_1} (handle : Unit → Option α), none.tryCatch handle = handle ()
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.mapNatIso_inverse_map_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : D} {T T' : CategoryTheory.Functor C D} (i : T ≅ T')
  {Y X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit S) T'} (f : Y ⟶ X),
  ((CategoryTheory.StructuredArrow.mapNatIso i).inverse.map f).right = f.right
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.isEmpty_alter : ∀ {α : 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 =
    ((t.isEmpty || t.size == 1 && t.contains k) && (f (Std.DTreeMap.Const.get? t k)).isNone)
-- Mathlib.Algebra.Group.Commute.Units
isUnit_mul_self_iff : ∀ {M : Type u_1} [inst : Monoid M] {a : M}, IsUnit (a * a) ↔ IsUnit a
-- Init.Data.BitVec.Bitblast
BitVec.adc_spec : ∀ {w : ℕ} (x y : BitVec w) (c : Bool), x.adc y c = (BitVec.carry w x y c, x + y + BitVec.setWidth w (BitVec.ofBool c))
-- Init.Data.List.Attach
List.tail_attach : ∀ {α : Type u_1} {xs : List α},
  xs.attach.tail =
    List.map
      (fun x =>
        match x with
        | ⟨x, h⟩ => ⟨x, ⋯⟩)
      xs.tail.attach
-- Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
/-- The negation of a weighted homogeneous polynomial of degree `n` is weighted homogeneous
of weighted degree `n`.  -/
MvPolynomial.IsWeightedHomogeneous.neg : ∀ {M : Type u_2} {σ : Type u_3} [inst : AddCommMonoid M] {n : M} {R : Type u_4} [inst_1 : CommRing R] {w : σ → M}
  {φ : MvPolynomial σ R}, MvPolynomial.IsWeightedHomogeneous w φ n → MvPolynomial.IsWeightedHomogeneous w (-φ) n
-- Mathlib.Algebra.Order.Floor.Ring
/-- There exists at most one `FloorRing` structure on a given linear ordered ring.  -/
subsingleton_floorRing : ∀ {R : Type u_4} [inst : Ring R] [inst_1 : LinearOrder R], Subsingleton (FloorRing R)
-- Mathlib.Topology.UniformSpace.AbstractCompletion
AbstractCompletion.extend_coe : ∀ {α : Type uα} [inst : UniformSpace α] (pkg : AbstractCompletion.{vα, uα} α) {β : Type uβ} [inst_1 : UniformSpace β]
  {f : α → β} [T2Space β], UniformContinuous f → ∀ (a : α), pkg.extend f (pkg.coe a) = f a
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax
CategoryTheory.Lax.OplaxTrans.whiskerRight_as_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G H : CategoryTheory.LaxFunctor B C} {η θ : F ⟶ G} (Γ : η ⟶ θ) (ι : G ⟶ H) (a : B),
  (CategoryTheory.Lax.OplaxTrans.whiskerRight Γ ι).as.app a =
    CategoryTheory.Bicategory.whiskerRight (Γ.as.app a) (ι.app a)
-- Mathlib.Analysis.Normed.Group.Quotient
/-- For any `m : M` and any `0 < ε`, there is `s ∈ S` such that `‖m + s‖ < ‖mk' S m‖ + ε`.  -/
QuotientAddGroup.exists_norm_add_lt : ∀ {M : Type u_1} [inst : SeminormedAddCommGroup M] (S : AddSubgroup M) (m : M) {ε : ℝ},
  0 < ε → ∃ s ∈ S, ‖m + s‖ < ‖(QuotientAddGroup.mk' S) m‖ + ε
-- Mathlib.NumberTheory.Cyclotomic.Basic
/-- The `A`-algebra structure on `CyclotomicRing n A K`.  -/
CyclotomicRing.algebraBase : (n : ℕ) →
  (A : Type u) →
    (K : Type w) → [inst : CommRing A] → [inst_1 : Field K] → [inst_2 : Algebra A K] → Algebra A (CyclotomicRing n A K)
-- Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
/-- Log-convexity of the Gamma function on the positive reals (stated in multiplicative form),
proved using the Hölder inequality applied to Euler's integral.  -/
Real.Gamma_mul_add_mul_le_rpow_Gamma_mul_rpow_Gamma : ∀ {s t a b : ℝ},
  0 < s → 0 < t → 0 < a → 0 < b → a + b = 1 → Real.Gamma (a * s + b * t) ≤ Real.Gamma s ^ a * Real.Gamma t ^ b
-- Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
CategoryTheory.Abelian.SpectralObject.HasSpectralSequence.mk : ∀ {C : Type u_1} {ι : Type u_2} {κ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Abelian C] [inst_2 : Preorder ι] {c : ℤ → ComplexShape κ} {r₀ : ℤ}
  {X : CategoryTheory.Abelian.SpectralObject C ι}
  {data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀},
  (∀ (r r' : ℤ) (pq : κ),
      (∀ (pq' : κ), ¬(c r).Rel pq pq') →
        ∀ (n : ℤ),
          n = data.deg pq + 1 →
            ∀ (hrr' : autoParam (r + 1 = r') CategoryTheory.Abelian.SpectralObject.HasSpectralSequence._auto_1)
              (hr : autoParam (r₀ ≤ r) CategoryTheory.Abelian.SpectralObject.HasSpectralSequence._auto_3),
              CategoryTheory.Limits.IsZero
                ((X.H n).obj (CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.homOfLE ⋯)))) →
    (∀ (r r' : ℤ) (pq : κ),
        (∀ (pq' : κ), ¬(c r).Rel pq' pq) →
          ∀ (n : ℤ),
            n = data.deg pq - 1 →
              ∀ (hrr' : autoParam (r + 1 = r') CategoryTheory.Abelian.SpectralObject.HasSpectralSequence._auto_9)
                (hr : autoParam (r₀ ≤ r) CategoryTheory.Abelian.SpectralObject.HasSpectralSequence._auto_11),
                CategoryTheory.Limits.IsZero
                  ((X.H n).obj (CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.homOfLE ⋯)))) →
      X.HasSpectralSequence data
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.preservesTerminalIso.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₁} [inst_2 : CategoryTheory.Category.{v₁, u₁} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D) [h : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty C) F],
  CategoryTheory.CartesianMonoidalCategory.preservesTerminalIso F =
    CategoryTheory.CartesianMonoidalCategory.preservesTerminalIso F
-- Mathlib.Data.Finsupp.Basic
Finsupp.embDomain_inl : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Zero γ] (a : α →₀ γ),
  Finsupp.embDomain Function.Embedding.inl a = a.sumElim 0
-- Mathlib.Topology.NhdsKer
nhdsKer_eq_empty : ∀ {X : Type u_2} [inst : TopologicalSpace X] {s : Set X}, nhdsKer s = ∅ ↔ s = ∅
-- Init.Data.Vector.Lemmas
Vector.instDecidableExistsVectorSucc : {α : Type u_1} →
  {n : ℕ} →
    (P : Vector α (n + 1) → Prop) → [Decidable (∀ (x : α) (xs : Vector α n), ¬P (xs.push x))] → Decidable (∃ xs, P xs)
-- Init.Data.Array.Lemmas
Array.map_inj_right : ∀ {α : Type u_1} {β : Type u_2} {xs ys : Array α} {f : α → β},
  (∀ (x y : α), f x = f y → x = y) → (Array.map f xs = Array.map f ys ↔ xs = ys)
-- Mathlib.Data.Nat.GCD.Basic
/-- **Alias** of `Nat.dvd_lcm_of_dvd_right`. -/
Nat.Dvd.dvd.nat_lcm_left : ∀ {a b : ℕ}, a ∣ b → ∀ (c : ℕ), a ∣ c.lcm b
-- Mathlib.RingTheory.DividedPowers.Basic
DividedPowers.dpow_smul_right : ∀ {A : Type u_1} [inst : CommSemiring A] {I : Ideal A} {a b : A} (hI : DividedPowers I) {n : ℕ},
  a ∈ I → hI.dpow n (a • b) = hI.dpow n a • b ^ n
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.limit.id_pre : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Limits.HasLimitsOfShape J C] (F : CategoryTheory.Functor J C),
  CategoryTheory.Limits.limit.pre F (CategoryTheory.Functor.id J) = CategoryTheory.Limits.lim.map F.leftUnitor.inv
-- Init.Control.Basic
/-- If the proposition `p` is true, does nothing, else fails (using `failure`).
 -/
guard : {f : Type → Type v} → [Alternative f] → (p : Prop) → [Decidable p] → f Unit
-- Mathlib.RepresentationTheory.Continuous.TopRep
TopRep.instModuleHom : {k : Type u} →
  {G : Type v} →
    [inst : TopologicalSpace k] → [inst_1 : CommRing k] → [inst_2 : Monoid G] → {A B : TopRep k G} → Module k (A ⟶ B)
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.to_iso : ∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Y) [H : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f]
  [CategoryTheory.Epi f.base], CategoryTheory.IsIso f
-- Mathlib.MeasureTheory.Integral.IntegrableOn
/-- We say that a function `f` is *integrable at filter* `l` if it is integrable on some
set `s ∈ l`. Equivalently, it is eventually integrable on `s` in `l.smallSets`.  -/
MeasureTheory.IntegrableAtFilter : {α : Type u_1} →
  {ε : Type u_3} →
    {mα : MeasurableSpace α} →
      [inst : TopologicalSpace ε] →
        [ContinuousENorm ε] →
          (α → ε) → Filter α → autoParam (MeasureTheory.Measure α) MeasureTheory.IntegrableAtFilter._auto_1 → Prop
-- Init.Data.BitVec.Lemmas
BitVec.pow_one : ∀ {w : ℕ} {x : BitVec w}, x ^ 1 = x
-- Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
/-- A normal monomorphism is a morphism which is the kernel of some morphism.  -/
CategoryTheory.NormalMono : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} → [CategoryTheory.Limits.HasZeroMorphisms C] → (X ⟶ Y) → Type (max u₁ v₁)
-- Mathlib.CategoryTheory.Limits.Types.Products
CategoryTheory.Limits.Types.Small.productIso_inv_comp_π_apply : ∀ {J : Type v} (F : J → Type u) [inst : Small.{u, v} J] (j : J) (x : Shrink.{u, max u v} ((j : J) → F j)),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.π F j))
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Types.Small.productIso F).inv) x) =
    (equivShrink ((j : J) → F j)).symm x j