mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Elab.InfoTree.InlayHints
Lean.Elab.InlayHintLinkLocation.mk : Lean.Name → Lean.Syntax.Range → Lean.Elab.InlayHintLinkLocation
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.widePullbackShapeOp_map : ∀ (J : Type w) {X₁ X₂ : CategoryTheory.Limits.WidePullbackShape J} (a : X₁ ⟶ X₂),
  (CategoryTheory.Limits.widePullbackShapeOp J).map a = CategoryTheory.Limits.widePullbackShapeOpMap J X₁ X₂ a
-- Mathlib.AlgebraicTopology.SimplicialNerve
/-- The underlying object of the linear order.  -/
CategoryTheory.SimplicialThickening.as : {J : Type u_1} → [inst : LinearOrder J] → CategoryTheory.SimplicialThickening J → J
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.size_diff_eq_size_left : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp],
  (∀ a ∈ t₁, a ∉ t₂) → (t₁ \ t₂).size = t₁.size
-- Mathlib.Analysis.Calculus.Gradient.Basic
/-- **Alias** of the forward direction of `hasGradientAt_iff_hasFDerivAt`. -/
HasGradientAt.hasFDerivAt : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F] [inst_2 : InnerProductSpace 𝕜 F]
  [inst_3 : CompleteSpace F] {f : F → 𝕜} {f' x : F},
  HasGradientAt f f' x → HasFDerivAt f ((InnerProductSpace.toDual 𝕜 F) f') x
-- Mathlib.LinearAlgebra.Dual.Defs
Submodule.dualCoannihilator_iSup_eq : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Sort u_3}
  (U : ι → Submodule R (Module.Dual R M)), (⨆ i, U i).dualCoannihilator = ⨅ i, (U i).dualCoannihilator
-- Mathlib.MeasureTheory.SetSemiring
MeasureTheory.IsSetSemiring.sUnion_disjointOfDiffUnion_subset : ∀ {α : Type u_1} {C : Set (Set α)} {s : Set α} {I : Finset (Set α)} (hC : MeasureTheory.IsSetSemiring C) (hs : s ∈ C)
  (hI : ↑I ⊆ C), ⋃₀ ↑(hC.disjointOfDiffUnion hs hI) ⊆ s
-- Mathlib.CategoryTheory.Join.Basic
CategoryTheory.Join.mkNatIso_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {F G : CategoryTheory.Functor (CategoryTheory.Join C D) E}
  (eₗ : (CategoryTheory.Join.inclLeft C D).comp F ≅ (CategoryTheory.Join.inclLeft C D).comp G)
  (eᵣ : (CategoryTheory.Join.inclRight C D).comp F ≅ (CategoryTheory.Join.inclRight C D).comp G)
  (h :
    autoParam
      (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Functor.whiskerRight (CategoryTheory.Join.edgeTransform C D) F)
          ((CategoryTheory.Prod.snd C D).isoWhiskerLeft eᵣ).hom =
        CategoryTheory.CategoryStruct.comp ((CategoryTheory.Prod.fst C D).isoWhiskerLeft eₗ).hom
          (CategoryTheory.Functor.whiskerRight (CategoryTheory.Join.edgeTransform C D) G))
      CategoryTheory.Join.mkNatIso._auto_1),
  (CategoryTheory.Join.mkNatIso eₗ eᵣ h).inv = CategoryTheory.Join.mkNatTrans eₗ.inv eᵣ.inv ⋯
-- Mathlib.RingTheory.Localization.Submodule
IsLocalization.coeSubmodule_isPrincipal : ∀ {R : Type u_3} [inst : CommRing R] {M : Submonoid R} (S : Type u_4) [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [IsLocalization M S] {I : Ideal R},
  M ≤ nonZeroDivisors R → ((IsLocalization.coeSubmodule S I).IsPrincipal ↔ Submodule.IsPrincipal I)
-- Mathlib.Algebra.Polynomial.CancelLeads
Polynomial.natDegree_cancelLeads_lt_of_natDegree_le_natDegree : ∀ {R : Type u_1} [inst : CommRing R] {p q : Polynomial R},
  p.natDegree ≤ q.natDegree → 0 < q.natDegree → (p.cancelLeads q).natDegree < q.natDegree
-- Mathlib.Algebra.Order.Floor.Div
gc_smul_ceilDiv : ∀ {α : Type u_2} {β : Type u_3} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [inst_2 : AddCommMonoid β]
  [inst_3 : PartialOrder β] [inst_4 : SMulZeroClass α β] [inst_5 : CeilDiv α β] {a : α},
  0 < a → GaloisConnection (fun x => x ⌈/⌉ a) fun x => a • x
-- Mathlib.CategoryTheory.NatIso
CategoryTheory.Iso.hom_inv_id_app_app_app_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {E' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} E']
  {F G : CategoryTheory.Functor C (CategoryTheory.Functor D (CategoryTheory.Functor E E'))} (e : F ≅ G) (X₁ : C)
  (X₂ : D) (X₃ : E) {Z : E'} (h : ((F.obj X₁).obj X₂).obj X₃ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (((e.hom.app X₁).app X₂).app X₃)
      (CategoryTheory.CategoryStruct.comp (((e.inv.app X₁).app X₂).app X₃) h) =
    h
-- Lean.Elab.DefView
Lean.Elab.DefKind.example : Lean.Elab.DefKind
-- Mathlib.Algebra.Homology.Embedding.TruncLE
HomologicalComplex.instMonoFTruncLE'ToRestriction : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsTruncLE] [inst_3 : ∀ (i' : ι'), K.HasHomology i']
  (i : ι), CategoryTheory.Mono ((K.truncLE'ToRestriction e).f i)
-- Mathlib.Order.Category.FinBddDistLat
FinBddDistLat.Iso.mk_inv : ∀ {α β : FinBddDistLat} (e : ↑α.toDistLat ≃o ↑β.toDistLat),
  (FinBddDistLat.Iso.mk e).inv =
    FinBddDistLat.ofHom
      (have __src := { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯ };
      { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ })
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientAddGroup.leftRel_eq_top : ∀ {G : Type u_1} [inst : AddGroup G] {N : AddSubgroup G}, QuotientAddGroup.leftRel N = ⊤ ↔ N = ⊤
-- Mathlib.GroupTheory.MonoidLocalization.Basic
/-- Given a `CommMonoid` `M` and submonoid `S`, `mk` sends `x : M`, `y ∈ S` to the equivalence
class of `(x, y)` in the localization of `M` at `S`.  -/
Localization.mk : {M : Type u_1} → [inst : CommMonoid M] → {S : Submonoid M} → M → ↥S → Localization S
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.symm_symm : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁}
  [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [inst_4 : TopologicalSpace M₁]
  [inst_5 : AddCommMonoid M₁] {M₂ : Type u_5} [inst_6 : TopologicalSpace M₂] [inst_7 : AddCommMonoid M₂]
  [inst_8 : Module R₁ M₁] [inst_9 : Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂), e.symm.symm = e
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjHom_comp_assoc : ∀ {X : AlgebraicGeometry.Scheme} {I J K : X.IdealSheafData} (hIJ : I ≤ J) (hJK : J ≤ K) (U : ↑X.affineOpens)
  {Z : AlgebraicGeometry.Scheme} (h : I.glueDataObj U ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjHom hJK U)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjHom hIJ U) h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjHom ⋯ U) h
-- Mathlib.FieldTheory.IsAlgClosed.Basic
IsAlgClosure.separable : ∀ (R : Type u_1) (K : Type u_2) [inst : Field R] [inst_1 : Field K] [inst_2 : Algebra R K] [IsAlgClosure R K]
  [CharZero R], Algebra.IsSeparable R K
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.minEntry!_eq_get!_minEntry? : ∀ {α : Type u} {β : Type v} [Ord α] {l : Std.DTreeMap.Internal.Impl α fun x => β} [inst : Inhabited (α × β)],
  Std.DTreeMap.Internal.Impl.Const.minEntry! l = (Std.DTreeMap.Internal.Impl.Const.minEntry? l).get!
-- Mathlib.NumberTheory.Harmonic.EulerMascheroni
Real.strictMono_eulerMascheroniSeq : StrictMono Real.eulerMascheroniSeq
-- Mathlib.Algebra.Homology.ShortComplex.ModuleCat
CategoryTheory.ShortComplex.π_moduleCatCyclesIso_hom_assoc : ∀ {R : Type u} [inst : Ring R] (S : CategoryTheory.ShortComplex (ModuleCat R)) {Z : ModuleCat R}
  (h : S.moduleCatLeftHomologyData.H ⟶ Z),
  CategoryTheory.CategoryStruct.comp S.homologyπ (CategoryTheory.CategoryStruct.comp S.moduleCatHomologyIso.hom h) =
    CategoryTheory.CategoryStruct.comp S.moduleCatCyclesIso.hom
      (CategoryTheory.CategoryStruct.comp S.moduleCatLeftHomologyData.π h)
-- Mathlib.Data.Matrix.Mul
Matrix.instIsDedekindFiniteMonoidOfIsStablyFiniteRing : ∀ (n : Type u_11) (R : Type u_12) [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : MulOne R]
  [inst_3 : AddCommMonoid R] [IsStablyFiniteRing R], IsDedekindFiniteMonoid (Matrix n n R)
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
/-- In an R₁ topological space with Borel measure `μ`,
the measure of the closure of a compact set `K` is equal to the measure of `K`.

See also `MeasureTheory.Measure.OuterRegular.measure_closure_eq_of_isCompact`
for a version that assumes `μ` to be outer regular
but does not assume the `σ`-algebra to be Borel.  -/
IsCompact.measure_closure : ∀ {γ : Type u_3} [inst : TopologicalSpace γ] [inst_1 : MeasurableSpace γ] [BorelSpace γ] [R1Space γ] {K : Set γ},
  IsCompact K → ∀ (μ : MeasureTheory.Measure γ), μ (closure K) = μ K
-- Mathlib.NumberTheory.EulerProduct.DirichletLSeries
tsum_riemannZetaSummand : ∀ {s : ℂ} (hs : 1 < s.re), ∑' (n : ℕ), (riemannZetaSummandHom ⋯) n = riemannZeta s
-- Mathlib.CategoryTheory.Functor.ReflectsIso.Jointly
CategoryTheory.JointlyReflectEpimorphisms.epi : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_4, u_1} C] {I : Type u_2} {D : I → Type u_3}
  [inst_1 : (i : I) → CategoryTheory.Category.{u_5, u_3} (D i)] {F : (i : I) → CategoryTheory.Functor C (D i)},
  CategoryTheory.JointlyReflectEpimorphisms F →
    ∀ {X Y : C} (f : X ⟶ Y) [∀ (i : I), CategoryTheory.Epi ((F i).map f)], CategoryTheory.Epi f
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mapLeftComp_inv_app_left : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (R : CategoryTheory.Functor B T)
  {L₁ L₂ L₃ : CategoryTheory.Functor A T} (l : L₁ ⟶ L₂) (l' : L₂ ⟶ L₃) (X : CategoryTheory.Comma L₃ R),
  ((CategoryTheory.Comma.mapLeftComp R l l').inv.app X).left = CategoryTheory.CategoryStruct.id X.left
-- Mathlib.Algebra.Group.Subsemigroup.Defs
Subsemigroup.instInhabited : {M : Type u_1} → [inst : Mul M] → Inhabited (Subsemigroup M)
-- Mathlib.Data.Fin.Tuple.Sort
/-- The permutation that sorts `f` is the identity if and only if `f` is monotone.  -/
Tuple.sort_eq_refl_iff_monotone : ∀ {n : ℕ} {α : Type u_1} [inst : LinearOrder α] {f : Fin n → α}, Tuple.sort f = Equiv.refl (Fin n) ↔ Monotone f
-- Std.Http.Data.Method
Std.Http.Method.report.sizeOf_spec : sizeOf Std.Http.Method.report = 1
-- Mathlib.Data.Finset.Density
Finset.dens_inter_add_dens_sdiff : ∀ {α : Type u_2} [inst : Fintype α] [inst_1 : DecidableEq α] (s t : Finset α), (s ∩ t).dens + (s \ t).dens = s.dens
-- Lean.Elab.ConfigEval.Instances
Lean.Elab.ConfigEval.EvalTerm.instString : Lean.Elab.ConfigEval.EvalTerm String
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.DiseqCnstrProof.brecOn.go : {motive_1 : Lean.Meta.Grind.AC.DiseqCnstr → Sort u} →
  {motive_2 : Lean.Meta.Grind.AC.DiseqCnstrProof → Sort u} →
    (t : Lean.Meta.Grind.AC.DiseqCnstrProof) →
      ((t : Lean.Meta.Grind.AC.DiseqCnstr) → t.below → motive_1 t) →
        ((t : Lean.Meta.Grind.AC.DiseqCnstrProof) → t.below → motive_2 t) → motive_2 t ×' t.below
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getD_erase : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k a : α}
  {fallback : β}, (t.erase k).getD a fallback = if cmp k a = Ordering.eq then fallback else t.getD a fallback
-- Mathlib.Order.ConditionallyCompletePartialOrder.Basic
/-- If a set is bounded below and above, and nonempty, its infimum is less than or equal to
its supremum.  -/
DirectedOn.csInf_le_csSup : ∀ {α : Type u_1} [inst : ConditionallyCompletePartialOrder α] {s : Set α},
  DirectedOn (fun x1 x2 => x1 ≥ x2) s →
    DirectedOn (fun x1 x2 => x1 ≤ x2) s → BddBelow s → BddAbove s → s.Nonempty → sInf s ≤ sSup s
-- Mathlib.Analysis.CStarAlgebra.GelfandDuality
gelfandTransform_map_star : ∀ {A : Type u_1} [inst : CommCStarAlgebra A] (a : A),
  (WeakDual.gelfandTransform ℂ A) (star a) = star ((WeakDual.gelfandTransform ℂ A) a)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
/-- The multiplicative action for a Jacobian point representative on a Weierstrass curve.  -/
WeierstrassCurve.Jacobian.instMulActionForallFinOfNatNat : {R : Type r} → [inst : CommRing R] → MulAction R (Fin 3 → R)
-- Mathlib.GroupTheory.SpecificGroups.Dihedral
DihedralGroup.r_pow : ∀ {n : ℕ} (i : ZMod n) (k : ℕ), DihedralGroup.r i ^ k = DihedralGroup.r (i * ↑k)
-- Init.Data.Nat.Lemmas
Nat.le_iff_lt_add_one : ∀ {x y : ℕ}, x ≤ y ↔ x < y + 1
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.prod_lipschitzWith_toLp : ∀ (p : ENNReal) (α : Type u_2) (β : Type u_3) [hp : Fact (1 ≤ p)] [inst : PseudoEMetricSpace α]
  [inst_1 : PseudoEMetricSpace β], LipschitzWith (2 ^ (1 / p).toReal) (WithLp.toLp p)
-- Mathlib.Data.Num.ZNum
ZNum.to_of_int : ∀ (n : ℤ), ↑↑n = n
-- Mathlib.Topology.AlexandrovDiscrete
isOpen_nhdsKer : ∀ {α : Type u_3} [inst : TopologicalSpace α] [AlexandrovDiscrete α] {s : Set α}, IsOpen (nhdsKer s)
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.instSMulCommClassAddMonoidHom_1 : ∀ {A : Type u_5} {B : Type u_6} {M : Type u_7} {M' : Type u_8} [inst : AddMonoid A] [inst_1 : DistribSMul M A]
  [inst_2 : AddZeroClass B] [inst_3 : DistribSMul M' B], SMulCommClass Mᵈᵐᵃ M' (A →+ B)
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instCommMonoid : {α : Type u_1} → {l : Filter α} → {M : Type u_5} → [CommMonoid M] → CommMonoid (l.Germ M)
-- Mathlib.AlgebraicTopology.ModelCategory.Cylinder
HomotopicalAlgebra.Cylinder.ofFactorizationData_i₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] {A : C}
  (h :
    (HomotopicalAlgebra.cofibrations C).MapFactorizationData (HomotopicalAlgebra.trivialFibrations C)
      (CategoryTheory.Limits.codiag A)),
  (HomotopicalAlgebra.Cylinder.ofFactorizationData h).i₁ =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr h.i
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.isEmpty_eq_size_eq_zero : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp}, t.WF → t.isEmpty = (t.size == 0)
-- Mathlib.CategoryTheory.Abelian.Preradical.Colon
/-- For `X : C`, the kernel fork `KernelFork.ofι (Φ.ι.app X) (Φ.ι_π_app X)` exhibits
`Φ.ι.app X : Φ.r.obj X ⟶ X` as the kernel of the projection `Φ.π.app X : X ⟶ Φ.quotient.obj X`.  -/
CategoryTheory.Abelian.Preradical.isLimitKernelForkObj : {C : Type u_1} →
  [inst : CategoryTheory.Category.{u_2, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      (Φ : CategoryTheory.Abelian.Preradical C) →
        (X : C) → CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι (Φ.ι.app X) ⋯)
-- Mathlib.Algebra.Algebra.Hom
AlgHom.coe_toMonoidHom : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (f : A →ₐ[R] B), ⇑↑f = ⇑f
-- Mathlib.Algebra.Divisibility.Basic
dvd_mul_right : ∀ {α : Type u_1} [inst : Semigroup α] (a b : α), a ∣ a * b
-- Mathlib.CategoryTheory.Limits.Preserves.Ulift
/-- The functor `uliftFunctor : Type u ⥤ Type (max u v)` preserves limits of arbitrary size.
 -/
CategoryTheory.Limits.Types.instPreservesLimitsOfSizeUliftFunctor : CategoryTheory.Limits.PreservesLimitsOfSize.{w', w, u, max u v, u + 1, max (u + 1) (v + 1)}
  CategoryTheory.uliftFunctor.{v, u}
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.singleton_pow : ∀ {α : Type u_2} [inst : Monoid α] (a : α) (n : ℕ), {a} ^ n = {a ^ n}
-- Mathlib.Data.Ordmap.Ordset
Ordnode.insertWith.eq_1 : ∀ {α : Type u_1} [inst : LE α] [inst_1 : DecidableLE α] (f : α → α) (x : α),
  Ordnode.insertWith f x Ordnode.nil = Ordnode.singleton x
-- Mathlib.Order.CompleteLattice.Basic
iSup_insert : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {f : β → α} {s : Set β} {b : β},
  ⨆ x ∈ insert b s, f x = f b ⊔ ⨆ x ∈ s, f x
-- Init.Data.Range.Polymorphic.BitVec
BitVec.instRxcHasSize : {n : ℕ} → Std.Rxc.HasSize (BitVec n)
-- Mathlib.Topology.Algebra.Group.Pointwise
IsOpen.closure_div : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G] {t : Set G},
  IsOpen t → ∀ (s : Set G), closure s / t = s / t
-- Init.Data.Nat.Compare
Nat.compare_swap : ∀ (a b : ℕ), (compare a b).swap = compare b a
-- Mathlib.CategoryTheory.Monoidal.Action.Opposites
CategoryTheory.MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionHomRight : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] (c : Cᴹᵒᵖ) {d d' : D} (f : d ⟶ d'),
  CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight c f =
    CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft f c.unmop
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
/-- A bicone over `F : J → C`, which is both a limit cone and a colimit cocone.  -/
CategoryTheory.Limits.LimitBicone : {J : Type w} →
  {C : Type uC} →
    [inst : CategoryTheory.Category.{uC', uC} C] →
      [CategoryTheory.Limits.HasZeroMorphisms C] → (J → C) → Type (max (max uC uC') w)
-- Mathlib.Data.Set.Operations
/-- **Alias** of `Set.mem_ofPred_eq`. -/
Set.mem_setOf_eq : ∀ {α : Type u} {x : α} {p : α → Prop}, (x ∈ {y | p y}) = p x
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
CategoryTheory.Limits.inl_opProdIsoCoprod_inv_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A B : C}
  [inst_1 : CategoryTheory.Limits.HasBinaryProduct A B] {Z : Cᵒᵖ} (h : Opposite.op (A ⨯ B) ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.opProdIsoCoprod A B).inv h) =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst.op h
-- Mathlib.Analysis.Fourier.Inversion
/-- **Fourier inversion formula**: If a function `f` on a finite-dimensional real inner product
space is continuous, integrable, and its Fourier transform `𝓕 f` is also integrable,
then `𝓕⁻ (𝓕 f) = f`.  -/
Continuous.fourierInv_fourier_eq : ∀ {V : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
  [inst_2 : MeasurableSpace V] [inst_3 : BorelSpace V] [inst_4 : FiniteDimensional ℝ V] [inst_5 : NormedAddCommGroup E]
  [inst_6 : NormedSpace ℂ E] {f : V → E} [CompleteSpace E],
  Continuous f →
    MeasureTheory.Integrable f MeasureTheory.volume →
      MeasureTheory.Integrable (FourierTransform.fourier f) MeasureTheory.volume →
        FourierTransformInv.fourierInv (FourierTransform.fourier f) = f
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- `X` identifies to the kernel of a zero map `X ⟶ Y`.  -/
CategoryTheory.Limits.KernelFork.IsLimit.ofId : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} →
        (f : X ⟶ Y) →
          (hf : f = 0) →
            CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι (CategoryTheory.CategoryStruct.id X) ⋯)
-- Mathlib.NumberTheory.SmoothNumbers
/-- The cardinality of the set of `k`-smooth numbers `≤ N` is bounded by `2^π(k-1) * √N`.  -/
Nat.smoothNumbersUpTo_card_le : ∀ (N k : ℕ), (N.smoothNumbersUpTo k).card ≤ 2 ^ k.primesBelow.card * N.sqrt
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddEquiv.symm_comp_self : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace N] [inst_2 : Add M]
  [inst_3 : Add N] (e : M ≃ₜ+ N), ⇑e.symm ∘ ⇑e = id
-- Mathlib.Order.Interval.Set.Pi
Set.image_single_uIcc_right : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Lattice (α i)] [inst_1 : DecidableEq ι]
  [inst_2 : (i : ι) → Zero (α i)] (i : ι) (b : α i), Pi.single i '' Set.uIcc 0 b = Set.uIcc 0 (Pi.single i b)
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
AddOpposite.comap_op_leftUniformSpace : ∀ (G : Type u_1) [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalAddGroup G],
  UniformSpace.comap AddOpposite.op (IsTopologicalAddGroup.leftUniformSpace Gᵃᵒᵖ) =
    IsTopologicalAddGroup.rightUniformSpace G
-- Mathlib.Tactic.Polynomial.Core
Mathlib.Tactic.Polynomial.PolynomialExt.mk.injEq : ∀ (infer infer_1 : Lean.Expr → Lean.MetaM Lean.Expr), ({ infer := infer } = { infer := infer_1 }) = (infer = infer_1)
-- Mathlib.GroupTheory.Complement
AddSubgroup.isComplement_addSubgroup_right_iff_existsUnique_quotientAddGroupMk : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} {S : Set G},
  AddSubgroup.IsComplement S ↑H ↔ ∀ (q : G ⧸ H), ∃! s, ↑↑s = q
-- Mathlib.Algebra.Group.Basic
mul_eq_right : ∀ {M : Type u_4} [inst : Monoid M] [IsRightCancelMul M] {a b : M}, a * b = b ↔ a = 1
-- Mathlib.CategoryTheory.Filtered.Basic
CategoryTheory.instIsFilteredULiftHom : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFiltered C],
  CategoryTheory.IsFiltered (CategoryTheory.ULiftHom C)
-- Mathlib.ModelTheory.Semantics
_private.Mathlib.ModelTheory.Semantics.0.FirstOrder.Language.Term.restrictVarLeft.match_1.eq_2 : ∀ {L : FirstOrder.Language} {α : Type u_4} {β : Type u_6} [inst : DecidableEq α] {γ : Type u_3}
  (motive : (x : L.Term (α ⊕ γ)) → (↥x.varFinsetLeft → β) → Sort u_5) (a : γ)
  (_f : ↥(FirstOrder.Language.var (Sum.inr a)).varFinsetLeft → β)
  (h_1 :
    (a : α) →
      (f : ↥(FirstOrder.Language.var (Sum.inl a)).varFinsetLeft → β) → motive (FirstOrder.Language.var (Sum.inl a)) f)
  (h_2 :
    (a : γ) →
      (_f : ↥(FirstOrder.Language.var (Sum.inr a)).varFinsetLeft → β) → motive (FirstOrder.Language.var (Sum.inr a)) _f)
  (h_3 :
    (l : ℕ) →
      (F : L.Functions l) →
        (ts : Fin l → L.Term (α ⊕ γ)) →
          (f : ↥(FirstOrder.Language.func F ts).varFinsetLeft → β) → motive (FirstOrder.Language.func F ts) f),
  (match FirstOrder.Language.var (Sum.inr a), _f with
    | FirstOrder.Language.var (Sum.inl a), f => h_1 a f
    | FirstOrder.Language.var (Sum.inr a), _f => h_2 a _f
    | FirstOrder.Language.func F ts, f => h_3 l F ts f) =
    h_2 a _f
-- Mathlib.Order.Basic
dense_or_discrete' : ∀ {α : Type u_2} [inst : LinearOrder α] (a₁ a₂ : α),
  (∃ a < a₁, a₂ < a) ∨ (∀ a < a₁, a ≤ a₂) ∧ ∀ (a : α), a₂ < a → a₁ ≤ a
-- Mathlib.Combinatorics.Matroid.Dual
Matroid.IsBase.inter_isBasis_iff_compl_inter_isBasis_dual : ∀ {α : Type u_1} {M : Matroid α} {B X : Set α},
  M.IsBase B →
    autoParam (X ⊆ M.E) Matroid.IsBase.inter_isBasis_iff_compl_inter_isBasis_dual._auto_1 →
      (M.IsBasis (B ∩ X) X ↔ M✶.IsBasis (M.E \ B ∩ (M.E \ X)) (M.E \ X))
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
HasStrictDerivAt.ccos : ∀ {f : ℂ → ℂ} {f' x : ℂ},
  HasStrictDerivAt f f' x → HasStrictDerivAt (fun x => Complex.cos (f x)) (-Complex.sin (f x) * f') x
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.le_rootMultiplicity_map : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] {p : Polynomial A} {f : A →+* B},
  Polynomial.map f p ≠ 0 →
    ∀ (a : A), Polynomial.rootMultiplicity a p ≤ Polynomial.rootMultiplicity (f a) (Polynomial.map f p)
-- Mathlib.ModelTheory.Fraisse
/-- If a class has a Fraïssé limit, it must be Fraïssé.  -/
FirstOrder.Language.IsFraisseLimit.isFraisse : ∀ {L : FirstOrder.Language} (K : Set (CategoryTheory.Bundled L.Structure)) {M : Type w} [inst : L.Structure M]
  [inst_1 : Countable ((l : ℕ) × L.Functions l)] [inst_2 : Countable M],
  FirstOrder.Language.IsFraisseLimit K M → FirstOrder.Language.IsFraisse K
-- Std.Sat.AIG.Lemmas
Std.Sat.AIG.denote_mkGate : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {assign : α → Bool} {aig : Std.Sat.AIG α}
  {input : aig.BinaryInput},
  ⟦assign, aig.mkGate input⟧ =
    (⟦assign, { aig := aig, ref := input.lhs }⟧ && ⟦assign, { aig := aig, ref := input.rhs }⟧)