mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Polynomial.Mirror
Polynomial.mirror_natDegree : ∀ {R : Type u_1} [inst : Semiring R] (p : Polynomial R), p.mirror.natDegree = p.natDegree
-- Mathlib.Topology.OpenPartialHomeomorph.Constructions
OpenPartialHomeomorph.subtypeRestr.congr_simp : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e e_1 : OpenPartialHomeomorph X Y),
  e = e_1 → ∀ {s : TopologicalSpace.Opens X} (hs : Nonempty ↥s), e.subtypeRestr hs = e_1.subtypeRestr hs
-- Mathlib.Logic.Equiv.Set
Equiv.image_symm_eq_preimage : ∀ {α : Type u_1} {β : Type u_2} (e : α ≃ β) (s : Set β), ⇑e.symm '' s = ⇑e ⁻¹' s
-- Mathlib.Data.Nat.Choose.Factorization
/-- A `pow` form of `Nat.factorization_choose_le`  -/
Nat.pow_factorization_choose_le : ∀ {p n k : ℕ}, 0 < n → p ^ (n.choose k).factorization p ≤ n
-- Mathlib.Logic.Equiv.Basic
Equiv.uniqueSigma.eq_1 : ∀ {α : Type u_10} (β : α → Type u_9) [inst : Unique α],
  Equiv.uniqueSigma β = { toFun := fun p => ⋯ ▸ p.snd, invFun := fun b => ⟨default, b⟩, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Order.Atoms
IsSimpleOrder.instIsAtomistic : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : BoundedOrder α] [IsSimpleOrder α], IsAtomistic α
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.insertManyIfNew_eq_insertListIfNewₘ_toListModel : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m m₂ : Std.DHashMap.Internal.Raw₀ α β),
  ↑(m.insertManyIfNew ↑m₂) = m.insertListIfNewₘ (Std.DHashMap.Internal.toListModel (↑m₂).buckets)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
/-- A variant of `WeierstrassCurve.j_eq_zero_iff` without assuming a reduced ring.  -/
WeierstrassCurve.j_eq_zero_iff' : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) [inst_1 : W.IsElliptic], W.j = 0 ↔ W.c₄ ^ 3 = 0
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.map_X₃ : ∀ {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] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] (S : CategoryTheory.ShortComplex C)
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms], (S.map F).X₃ = F.obj S.X₃
-- Mathlib.CategoryTheory.Monoidal.ExternalProduct.KanExtension
/-- Given an extension `α : H ⟶ L ⋙ H'`, this is the canonical extension
`H ⊠ K ⟶ L.prod (𝟭 E) ⋙ H' ⊠ K` it induces through bifunctoriality of the external product.  -/
CategoryTheory.MonoidalCategory.ExternalProduct.extensionUnitLeft : {V : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      {D : Type u₂} →
        {D' : Type u₃} →
          {E : Type u₄} →
            [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
              [inst_3 : CategoryTheory.Category.{v₃, u₃} D'] →
                [inst_4 : CategoryTheory.Category.{v₄, u₄} E] →
                  {H : CategoryTheory.Functor D V} →
                    {L : CategoryTheory.Functor D D'} →
                      (H' : CategoryTheory.Functor D' V) →
                        (H ⟶ L.comp H') →
                          (K : CategoryTheory.Functor E V) →
                            CategoryTheory.MonoidalCategory.externalProduct H K ⟶
                              (L.prod (CategoryTheory.Functor.id E)).comp
                                (CategoryTheory.MonoidalCategory.externalProduct H' K)
-- Mathlib.LinearAlgebra.TensorProduct.Tower
TensorProduct.AlgebraTensorModule.down_uliftEquiv_symm_tmul : ∀ (R : Type uR) (A : Type uA) {M : Type uM} {N : Type uN} [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module A M]
  [inst_6 : IsScalarTower R A M] [inst_7 : AddCommMonoid N] [inst_8 : Module R N] (m : ULift.{u_1, uM} M)
  (n : ULift.{u_2, uN} N),
  ((TensorProduct.AlgebraTensorModule.uliftEquiv R A M N).symm (m ⊗ₜ[ULift.{u_4, uR} R] n)).down = m.down ⊗ₜ[R] n.down
-- Mathlib.Algebra.Group.Subgroup.Defs
SubgroupClass.inclusion_mk : ∀ {G : Type u_1} [inst : Group G] {S : Type u_4} {H K : S} [inst_1 : SetLike S G] [inst_2 : SubgroupClass S G]
  [inst_3 : LE S] [inst_4 : IsConcreteLE S G] {h : H ≤ K} (x : G) (hx : x ∈ H),
  (SubgroupClass.inclusion h) ⟨x, hx⟩ = ⟨x, ⋯⟩
-- Mathlib.Data.Seq.Defs
Stream'.Seq.tail_cons : ∀ {α : Type u} (a : α) (s : Stream'.Seq α), (Stream'.Seq.cons a s).tail = s
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
SSet.prodStdSimplex.pairingCore.IsIndex.type₁_d : ∀ {m : ℕ} {k : Fin (m + 1)} {n : ℕ} {x : ((SSet.horn (m + 1) k.castSucc).unionProd (SSet.boundary n)).N} {d : ℕ}
  {hd : x.dim = d + 1} {i : Fin (d + 1)} (h : SSet.prodStdSimplex.pairingCore.IsIndex x hd i.succ), h.type₁.d = d
-- Mathlib.Order.Cover
CovBy.of_lt_of_le : ∀ {α : Type u_1} [inst : Preorder α] {a b c : α}, a ⋖ c → a < b → b ≤ c → a ⋖ b
-- Mathlib.GroupTheory.Goursat
/-- **Goursat's lemma** for a subgroup of a product with surjective projections.

If `I` is a subgroup of `G × H` which projects fully on both factors, then there exist normal
subgroups `M ≤ G` and `N ≤ H` such that `G' × H' ≤ I` and the image of `I` in `G ⧸ M × H ⧸ N` is the
graph of an isomorphism `G ⧸ M ≃ H ⧸ N'`.

`G'` and `H'` can be explicitly constructed as `I.goursatFst` and `I.goursatSnd` respectively.  -/
AddSubgroup.goursat_surjective : ∀ {G : Type u_1} {H : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup H] {I : AddSubgroup (G × H)}
  (hI₁ : Function.Surjective (Prod.fst ∘ ⇑I.subtype)) (hI₂ : Function.Surjective (Prod.snd ∘ ⇑I.subtype)),
  have this := ⋯;
  have this_1 := ⋯;
  ∃ e,
    (((QuotientAddGroup.mk' I.goursatFst).prodMap (QuotientAddGroup.mk' I.goursatSnd)).comp I.subtype).range =
      e.toAddMonoidHom.graph
-- Mathlib.Order.Interval.Set.Image
StrictAnti.image_Ioo_subset : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : Preorder α] [inst_1 : Preorder β] {a b : α},
  StrictAnti f → f '' Set.Ioo a b ⊆ Set.Ioo (f b) (f a)
-- Mathlib.Algebra.Group.Submonoid.BigOperators
Submonoid.mem_closure_finset : ∀ {M : Type u_1} [inst : CommMonoid M] {x : M} {s : Finset M},
  x ∈ Submonoid.closure ↑s ↔ ∃ f, Function.support f ⊆ ↑s ∧ ∏ a ∈ s, a ^ f a = x
-- Mathlib.Order.Hom.Bounded
BoundedOrderHom.dual_id : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : BoundedOrder α],
  BoundedOrderHom.dual (BoundedOrderHom.id α) = BoundedOrderHom.id αᵒᵈ
-- Mathlib.Algebra.Vertex.VertexOperator
VertexOperator.of_coeff_apply_coeff : ∀ {R : Type u_1} {V : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup V] [inst_2 : Module R V]
  (f : ℤ → Module.End R V) (hf : ∀ (x : V), BddBelow (Function.support fun y => (f y) x)) (x : V) (n : ℤ),
  ((HahnModule.of R).symm ((VertexOperator.of_coeff f hf) x)).coeff n = (f n) x
-- Mathlib.Algebra.GroupWithZero.Divisibility
pow_dvd_pow_iff : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [IsCancelMulZero α] {a : α} {m n : ℕ},
  a ≠ 0 → ¬IsUnit a → (a ^ n ∣ a ^ m ↔ n ≤ m)
-- Lean.Meta.Sym.DSimp.DSimpM
Lean.Meta.Sym.DSimp.Context.mk.inj : ∀ {config config_1 : Lean.Meta.Sym.DSimp.Config}, { config := config } = { config := config_1 } → config = config_1
-- Mathlib.Analysis.Calculus.ContDiff.Basic
/-- Bilinear functions are `C^n`.  -/
IsBoundedBilinearMap.contDiff : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {b : E × F → G} {n : WithTop ℕ∞},
  IsBoundedBilinearMap 𝕜 b → ContDiff 𝕜 n b
-- Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution
/-- The convolution of `f` and `g` with bilinear map `L` exists at `x` when the sum over
the fiber is summable.  -/
DiscreteConvolution.ConvolutionExistsAt : {M : Type u_1} →
  {S : Type u_2} →
    {E : Type u_3} →
      {E' : Type u_4} →
        {F : Type u_6} →
          [Monoid M] →
            [inst : CommSemiring S] →
              [inst_1 : AddCommMonoid E] →
                [inst_2 : AddCommMonoid E'] →
                  [inst_3 : AddCommMonoid F] →
                    [inst_4 : Module S E] →
                      [inst_5 : Module S E'] →
                        [inst_6 : Module S F] →
                          [TopologicalSpace F] → (E →ₗ[S] E' →ₗ[S] F) → (M → E) → (M → E') → M → Prop
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.eval_pow : ∀ {R : Type u} [inst : CommSemiring R] {p : Polynomial R} {x : R} (n : ℕ),
  Polynomial.eval x (p ^ n) = Polynomial.eval x p ^ n
-- Mathlib.Algebra.Order.Module.Defs
smulPosStrictMono_iff_SMulPosReflectLE : ∀ {α : Type u_1} {β : Type u_2} [inst : SMul α β] [inst_1 : LinearOrder α] [inst_2 : LinearOrder β] [inst_3 : Zero β],
  SMulPosStrictMono α β ↔ SMulPosReflectLE α β
-- Lean.Server.FileWorker.SemanticHighlighting
Lean.Server.FileWorker.AbsoluteLspSemanticToken.mk : Lean.Lsp.Position → Lean.Lsp.Position → Lean.Lsp.SemanticTokenType → ℕ → Lean.Server.FileWorker.AbsoluteLspSemanticToken
-- Init.Data.List.Monadic
List.foldrM_unattach : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {P : α → Prop}
  {xs : List (Subtype P)} {f : α → β → m β} {init : β},
  List.foldrM f init xs.unattach =
    List.foldrM
      (fun x b =>
        match x with
        | ⟨x, h⟩ => binderNameHint x f (binderNameHint h () (binderNameHint b (f x) (f (wfParam x) b))))
      init xs
-- Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
CategoryTheory.Functor.LaxRightLinear.μᵣ_associativity_inv_assoc : ∀ {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'] [inst_6 : F.LaxRightLinear C] (d : D) (c c' : C)
  {Z : D'}
  (h :
    F.obj
        (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj d
          (CategoryTheory.MonoidalCategoryStruct.tensorObj c c')) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft
        (CategoryTheory.Functor.LaxRightLinear.μᵣ F d c) c')
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.LaxRightLinear.μᵣ F
          (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj d c) c')
        (CategoryTheory.CategoryStruct.comp
          (F.map (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso d c c').inv) h)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso (F.obj d) c c').inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.LaxRightLinear.μᵣ F d (CategoryTheory.MonoidalCategoryStruct.tensorObj c c')) h)
-- Mathlib.Analysis.Calculus.FDeriv.Basic
differentiableOn_univ : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F}, DifferentiableOn 𝕜 f Set.univ ↔ Differentiable 𝕜 f
-- Mathlib.MeasureTheory.Integral.Lebesgue.Add
MeasureTheory.lintegral_trim_ae : ∀ {α : Type u_1} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m ≤ m0) {f : α → ENNReal},
  AEMeasurable f (μ.trim hm) → ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ
-- Lean.Declaration
Lean.ConstantInfo.opaqueInfo.sizeOf_spec : ∀ (val : Lean.OpaqueVal), sizeOf (Lean.ConstantInfo.opaqueInfo val) = 1 + sizeOf val
-- Mathlib.CategoryTheory.Sites.LocalSite
CategoryTheory.GrothendieckTopology.IsLocalSite.pointPresheafFiberIso_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] [inst_2 : J.IsLocalSite] {A : Type u'}
  [inst_3 : CategoryTheory.Category.{v', u'} A] [inst_4 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A]
  {P P' : CategoryTheory.Functor Cᵒᵖ A} (F : P ⟶ P'),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.GrothendieckTopology.IsLocalSite.point J).presheafFiber.map F)
      (CategoryTheory.GrothendieckTopology.IsLocalSite.pointPresheafFiberIso J P').hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.IsLocalSite.pointPresheafFiberIso J P).hom
      (F.app (Opposite.op (⊤_ C)))
-- Mathlib.Data.Set.Defs
Set.instSingletonSet : {α : Type u} → Singleton α (Set α)
-- Mathlib.CategoryTheory.GlueData
CategoryTheory.GlueData'.f_mono : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] (self : CategoryTheory.GlueData' C) (i j : self.J)
  (h : i ≠ j), CategoryTheory.Mono (self.f i j h)
-- Mathlib.Combinatorics.Matroid.Rank.Cardinal
Matroid.Spanning.isBase_of_le_cRank_of_finite : ∀ {α : Type u} {M : Matroid α} {X : Set α}, M.Spanning X → Cardinal.mk ↑X ≤ M.cRank → X.Finite → M.IsBase X
-- Lean.DocString.Parser
/-- The base column of the docstring, which is the least indentation of any non-empty line in it,
including the opening and closing delimiters. For indented docstrings (e.g. inside `where`
blocks), beginning-of-line checks use this column instead of requiring column 0. With the default
value 0, the check is equivalent to `column == 0`.
 -/
Lean.Doc.Parser.BlockCtxt.baseColumn : Lean.Doc.Parser.BlockCtxt → ℕ
-- Mathlib.Algebra.Regular.SMul
/-- An element of a group acting on a Type is regular. This relies on the availability
of the inverse given by groups, since there is no `LeftCancelSMul` typeclass.  -/
isSMulRegular_of_group : ∀ {R : Type u_1} {G : Type u_4} [inst : Group G] [inst_1 : MulAction G R] (g : G), IsSMulRegular R g
-- Mathlib.Algebra.Order.Group.PosPart
Pi.posPart_apply : ∀ {ι : Type u_2} {α : ι → Type u_3} [inst : (i : ι) → Lattice (α i)] [inst_1 : (i : ι) → AddGroup (α i)]
  (f : (i : ι) → α i) (i : ι), f⁺ i = (f i)⁺
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
/-- If the product of bounded continuous functions is zero, then the norm of their sum is the
maximum of their norms.  -/
BoundedContinuousFunction.norm_add_eq_max : ∀ {α : Type u} [inst : TopologicalSpace α] {R : Type u_1} [inst_1 : NonUnitalSeminormedRing R] [IsCancelMulZero R]
  {f g : BoundedContinuousFunction α R}, f * g = 0 → ‖f + g‖ = max ‖f‖ ‖g‖
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
_private.Mathlib.Topology.Algebra.InfiniteSum.NatInt.0.cond.match_1.eq_2 : ∀ (motive : Bool → Sort u_1) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  (match false with
    | true => h_1 ()
    | false => h_2 ()) =
    h_2 ()
-- Lean.Meta.PProdN
/-- Given a value of type `t₁ ×' … ×' tᵢ ×' … ×' tₙ`, return a value of type `tᵢ`  -/
Lean.Meta.PProdN.projM : ℕ → ℕ → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.GroupTheory.Generators
Group.Generators.mk.inj : ∀ {G : Type u_5} {inst : Group G} {ι : Type u_6} {val : ι → G} {closure_eq_top : Subgroup.closure (Set.range val) = ⊤}
  {val_1 : ι → G} {closure_eq_top_1 : Subgroup.closure (Set.range val_1) = ⊤},
  { val := val, closure_eq_top := closure_eq_top } = { val := val_1, closure_eq_top := closure_eq_top_1 } → val = val_1
-- Mathlib.Algebra.GCDMonoid.Basic
/-- The LCM is normalized to itself.  -/
NormalizedGCDMonoid.normalize_lcm : ∀ {α : Type u_2} {inst : CommMonoidWithZero α} [self : NormalizedGCDMonoid α] (a b : α), normalize (lcm a b) = lcm a b
-- Mathlib.Analysis.Convex.Function
ConcaveOn.dual : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid β] [inst_4 : PartialOrder β] [inst_5 : SMul 𝕜 E] [inst_6 : SMul 𝕜 β] {s : Set E} {f : E → β},
  ConcaveOn 𝕜 s f → ConvexOn 𝕜 s (⇑OrderDual.toDual ∘ f)
-- Mathlib.Topology.Compactification.StoneCech
continuous_stoneCechExtend : ∀ {α : Type u} [inst : TopologicalSpace α] {β : Type v} [inst_1 : TopologicalSpace β] [inst_2 : T2Space β] {g : α → β}
  (hg : Continuous g) [inst_3 : CompactSpace β], Continuous (stoneCechExtend hg)
-- Std.Data.HashSet.Lemmas
Std.HashSet.Equiv.erase : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α] (k : α),
  m₁.Equiv m₂ → (m₁.erase k).Equiv (m₂.erase k)
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.coe_equivMapOfInjective_apply : ∀ {F : Type w} {R : Type u} {S : Type v} [inst : NonUnitalNonAssocRing R] [inst_1 : NonUnitalNonAssocRing S]
  [inst_2 : FunLike F R S] [inst_3 : NonUnitalRingHomClass F R S] (s : NonUnitalSubring R) (f : F)
  (hf : Function.Injective ⇑f) (x : ↥s), ↑((s.equivMapOfInjective f hf) x) = f ↑x
-- Mathlib.LinearAlgebra.Complex.Module
Complex.equivRealProdLm_apply : ∀ (a : ℂ), Complex.equivRealProdLm a = (a.re, a.im)
-- Mathlib.RingTheory.Localization.Cardinality
/-- **Alias** of `Cardinal.mk_fractionRing`. -/
FractionRing.cardinalMk : ∀ (R : Type u) [inst : CommRing R], Cardinal.mk (FractionRing R) = Cardinal.mk R
-- Mathlib.Logic.Basic
congr_fun_rfl : ∀ {α : Sort u_1} {β : Sort u_2} (f : α → β) (a : α), ⋯ = ⋯
-- Mathlib.CategoryTheory.Bicategory.Functor.Oplax
/-- The underlying prelax functor.  -/
CategoryTheory.OplaxFunctor.toPrelaxFunctor : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] → CategoryTheory.OplaxFunctor B C → CategoryTheory.PrelaxFunctor B C
-- Mathlib.Algebra.Category.ModuleCat.Tannaka
CategoryTheory.End.ext_iff : ∀ {C : Type u} [inst : CategoryTheory.CategoryStruct.{v, u} C] {X : C} {x y : CategoryTheory.End X},
  x = y ↔ x.asHom = y.asHom
-- Init.Data.Option.Lemmas
Option.get_none_eq_iff_true : ∀ {α : Type u_1} {a : α} {h : none.isSome = true}, none.get h = a ↔ True
-- Mathlib.Order.Category.HeytAlg
/-- The type of morphisms in `HeytAlg R`.  -/
HeytAlg.Hom : HeytAlg → HeytAlg → Type u
-- Mathlib.Analysis.Polynomial.CauchyBound
Polynomial.cauchyBound_C : ∀ {K : Type u_1} [inst : NormedDivisionRing K] (x : K), (Polynomial.C x).cauchyBound = 1
-- Mathlib.Algebra.Polynomial.Coeff
Polynomial.constantCoeff_apply : ∀ {R : Type u} [inst : Semiring R] (p : Polynomial R), Polynomial.constantCoeff p = p.coeff 0
-- Mathlib.Analysis.Normed.Group.Pointwise
Bornology.IsBounded.neg : ∀ {E : Type u_1} [inst : SeminormedAddGroup E] {s : Set E}, Bornology.IsBounded s → Bornology.IsBounded (-s)
-- Mathlib.Analysis.Seminorm
Seminorm.comp.congr_simp : ∀ {𝕜 : Type u_3} {𝕜₂ : Type u_4} {E : Type u_7} {E₂ : Type u_8} [inst : SeminormedRing 𝕜] [inst_1 : SeminormedRing 𝕜₂]
  {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_2 : RingHomIsometric σ₁₂] [inst_3 : AddCommGroup E] [inst_4 : AddCommGroup E₂]
  [inst_5 : Module 𝕜 E] [inst_6 : Module 𝕜₂ E₂] (p p_1 : Seminorm 𝕜₂ E₂),
  p = p_1 → ∀ (f f_1 : E →ₛₗ[σ₁₂] E₂), f = f_1 → p.comp f = p_1.comp f_1
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_sub_natCast : ∀ {x : ℝ}, x ≠ 0 → ∀ (y : ℝ) (n : ℕ), x ^ (y - ↑n) = x ^ y / x ^ n
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.mapRange_id : ∀ {α : Type u_1} {mα : MeasurableSpace α} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M]
  (v : MeasureTheory.VectorMeasure α M), v.mapRange (AddMonoidHom.id M) ⋯ = v
-- Init.Data.Range.Polymorphic.PRange
/-- The lower bound of the range. `lower` is included in the range.
   -/
Std.Rci.lower : {α : Type u} → Std.Rci α → α
-- Mathlib.Topology.Algebra.Group.Pointwise
IsClosed.mul_closure_one_eq : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G] {F : Set G},
  IsClosed F → F * closure {1} = F
-- Std.Internal.Do.ExceptPost
/-- The trivial partial order on `EPost.Nil`: all values are equal.  -/
Std.Internal.Do.instPartialOrderNil : Lean.Order.PartialOrder EPost⟨⟩
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
CategoryTheory.Oplax.LaxTrans.isoMk_hom_as_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} {η θ : F ⟶ G} (app : (a : B) → η.app a ≅ θ.app a)
  (naturality :
    autoParam
      (∀ {a b : B} (f : a ⟶ b),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (app a).hom (G.map f))
            (θ.naturality f) =
          CategoryTheory.CategoryStruct.comp (η.naturality f)
            (CategoryTheory.Bicategory.whiskerLeft (F.map f) (app b).hom))
      CategoryTheory.Oplax.LaxTrans.isoMk._auto_1)
  (a : B), (CategoryTheory.Oplax.LaxTrans.isoMk app naturality).hom.as.app a = (app a).hom
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.colimit.ι_post_assoc : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Functor J C) {D : Type u'} [inst_2 : CategoryTheory.Category.{v', u'} D]
  [inst_3 : CategoryTheory.Limits.HasColimit F] (G : CategoryTheory.Functor C D)
  [inst_4 : CategoryTheory.Limits.HasColimit (F.comp G)] (j : J) {Z : D}
  (h : G.obj (CategoryTheory.Limits.colimit F) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (F.comp G) j)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.post F G) h) =
    CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.colimit.ι F j)) h
-- Mathlib.Topology.Covering.Quotient
Subgroup.isQuotientCoveringMap_of_comm : ∀ {G : Type u_4} [inst : CommGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G] (S : Subgroup G),
  IsDiscrete ↑S → IsQuotientCoveringMap QuotientGroup.mk ↥S
-- Mathlib.Order.Lattice
/-- Pointwise supremum of two monotone functions is a monotone function.  -/
MonotoneOn.sup : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : SemilatticeSup β] {f g : α → β} {s : Set α},
  MonotoneOn f s → MonotoneOn g s → MonotoneOn (f ⊔ g) s
-- Lean.Meta.Tactic.Simp.Arith.Int.Basic
Int.Internal.Linear.instReprPoly_lean.repr : Int.Internal.Linear.Poly → ℕ → Std.Format
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.mem_closedBall' : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x y : α} {ε : ℝ}, y ∈ Metric.closedBall x ε ↔ dist x y ≤ ε
-- Lean.SubExpr
Lean.SubExpr.GoalLocation.hypValue.injEq : ∀ (a : Lean.FVarId) (a_1 : Lean.SubExpr.Pos) (a_2 : Lean.FVarId) (a_3 : Lean.SubExpr.Pos),
  (Lean.SubExpr.GoalLocation.hypValue a a_1 = Lean.SubExpr.GoalLocation.hypValue a_2 a_3) = (a = a_2 ∧ a_1 = a_3)
-- Mathlib.CategoryTheory.Idempotents.Karoubi
CategoryTheory.Idempotents.Karoubi.decompId_i.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.Idempotents.Karoubi C),
  P.decompId_i = { f := P.p, comm := ⋯ }
-- Mathlib.CategoryTheory.Monoidal.Braided.Multifunctor
CategoryTheory.BraidedCategory.Hexagon.functor₁₃₂_obj_obj_obj : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C] (G k j : C),
  (((CategoryTheory.BraidedCategory.Hexagon.functor₁₃₂ C).obj G).obj k).obj j =
    CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj G j) k
-- Mathlib.MeasureTheory.Function.AEEqFun
/-- The space of equivalence classes of almost everywhere strongly measurable functions, where two
strongly measurable functions are equivalent if they agree almost everywhere, i.e.,
they differ on a set of measure `0`.  -/
MeasureTheory.«term_→ₘ[_]_» : Lean.TrailingParserDescr
-- Std.Data.DTreeMap.Raw.WF
Std.DTreeMap.Raw.WF.ofList : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List ((a : α) × β a)},
  (Std.DTreeMap.Raw.ofList l cmp).WF
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Arrow.mk_left : ∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] {X Y : T} (f : X ⟶ Y), (CategoryTheory.Arrow.mk f).left = X
-- Mathlib.Data.Setoid.Partition
/-- The elements of a set of sets partitioning α are the equivalence classes of the
equivalence relation defined by the set of sets.  -/
Setoid.eq_eqv_class_of_mem : ∀ {α : Type u_1} {c : Set (Set α)} (H : ∀ (a : α), ∃! b, b ∈ c ∧ a ∈ b) {s : Set α} {y : α},
  s ∈ c → y ∈ s → s = {x | (Setoid.mkClasses c H) x y}