mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
AddMonoidAlgebra.coeff_toMultiplicativeBialgEquiv_symm_apply : ∀ (R : Type u_1) (A : Type u_3) (M : Type u_8) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Bialgebra R A]
  [inst_3 : AddMonoid M] (a : MonoidAlgebra A (Multiplicative M)),
  ((AddMonoidAlgebra.toMultiplicativeBialgEquiv R A M).symm a).coeff = Finsupp.mapDomain (⇑Multiplicative.toAdd) a.coeff
-- Mathlib.GroupTheory.IsSubnormal
/-- A subnormal additive subgroup of a simple additive group is either trivial or the
whole group.  -/
AddSubgroup.IsSubnormal.eq_bot_or_top_of_isSimpleAddGroup : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G}, IsSimpleAddGroup G → H.IsSubnormal → H = ⊥ ∨ H = ⊤
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.skipSuffixWhile_eq_endPos : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.BackwardPattern pat] [String.Slice.Pattern.Model.LawfulBackwardPatternModel pat]
  {s : String}, s.endsWith pat = false → s.skipSuffixWhile pat = s.endPos
-- Mathlib.CategoryTheory.Sites.LocallySurjective
CategoryTheory.Presheaf.isLocallyInjective_of_isLocallyInjective_of_isLocallySurjective_fac : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} A] {FA : A → A → Type u_1} {CA : A → Type w'}
  [inst_2 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] [inst_3 : CategoryTheory.ConcreteCategory A FA]
  {F₁ F₂ F₃ : CategoryTheory.Functor Cᵒᵖ A} {f₁ : F₁ ⟶ F₂} {f₂ : F₂ ⟶ F₃} (f₃ : F₁ ⟶ F₃),
  CategoryTheory.CategoryStruct.comp f₁ f₂ = f₃ →
    ∀ [CategoryTheory.Presheaf.IsLocallyInjective J f₃] [CategoryTheory.Presheaf.IsLocallySurjective J f₁],
      CategoryTheory.Presheaf.IsLocallyInjective J f₂
-- Aesop.Forward.Match
/-- Returns `true` if any hypothesis contained in `m` satisfies `f`.  -/
Aesop.ForwardRuleMatch.anyHyp : Aesop.ForwardRuleMatch → (Lean.FVarId → Bool) → Bool
-- Mathlib.Data.Set.Operations
Set.mem_univ : ∀ {α : Type u} (x : α), x ∈ Set.univ
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
/-- Typeclass for monotonicity of multiplication on the right,
namely `a₁ ≤ a₂ → a₁ * b ≤ a₂ * b`.

You should usually not use this very granular typeclass directly, but rather a typeclass like
`IsOrderedMonoid`.  -/
MulRightMono : (M : Type u_1) → [Mul M] → [LE M] → Prop
-- Mathlib.Combinatorics.Enumerative.Composition
CompositionAsSet.mem_boundaries_iff_exists_blocks_sum_take_eq : ∀ {n : ℕ} (c : CompositionAsSet n) {j : Fin (n + 1)},
  j ∈ c.boundaries ↔ ∃ i < c.boundaries.card, (List.take i c.blocks).sum = ↑j
-- Mathlib.Algebra.Order.Module.Defs
PosMulReflectLE.toPosSMulReflectLE : ∀ {α : Type u_1} [inst : Zero α] [inst_1 : Mul α] [inst_2 : Preorder α] [PosMulReflectLE α], PosSMulReflectLE α α
-- Mathlib.Algebra.Homology.LeftResolution.Reduced
/-- Given an additive functor `ι : C ⥤ A` between idempotent complete categories,
any `Λ : LeftResolution ι` induces a term `Λ.reduced : LeftResolution ι`
such that `Λ.reduced.F` preserves zero morphisms.  -/
CategoryTheory.Abelian.LeftResolution.reduced : {A : Type u_1} →
  {C : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_2} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_1} A] →
        {ι : CategoryTheory.Functor C A} →
          CategoryTheory.Abelian.LeftResolution ι →
            [inst_2 : CategoryTheory.Preadditive C] →
              [inst_3 : CategoryTheory.Preadditive A] →
                [ι.Additive] →
                  [CategoryTheory.IsIdempotentComplete A] →
                    [CategoryTheory.IsIdempotentComplete C] → CategoryTheory.Abelian.LeftResolution ι
-- Batteries.Recycling.RBTree.WF
/-- The well-formedness invariant for a red-black tree is exactly the `mk` constructor,
because the other constructors of `WF` are redundant.
 -/
RBTree.RBNode.WF_iff : ∀ {α : Type u_1} {cmp : α → α → Ordering} {t : RBTree.RBNode α},
  RBTree.RBNode.WF cmp t ↔ RBTree.RBNode.Ordered cmp t ∧ ∃ c n, t.Balanced c n
-- Mathlib.MeasureTheory.OuterMeasure.Operations
/-- **Alias** of `FunLike.coeAddMonoidHom_apply`. -/
MeasureTheory.OuterMeasure.coeFnAddMonoidHom_apply : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : AddZero F] [inst_2 : AddZeroClass β]
  [inst_3 : IsZeroApply F α β] [inst_4 : IsAddApply F α β] (f : F), (FunLike.coeAddMonoidHom F α β) f = ⇑f
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.congrLeft_counitIso_inv_app : ∀ {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 : C ≌ D) (X : CategoryTheory.Functor D E),
  e.congrLeft.counitIso.inv.app X = (e.invFunIdAssoc X).inv
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get!_eq_get! : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] [inst_1 : Inhabited β], t.WF → ∀ {a : α}, Std.DTreeMap.Raw.Const.get! t a = t.get! a
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ico_map_sectR : ∀ {α : Type u_2} {β : Type u_3} [inst : PartialOrder α] [inst_1 : Preorder β] [inst_2 : LocallyFiniteOrder α]
  [inst_3 : LocallyFiniteOrder β] [inst_4 : DecidableLE (α × β)] (c : α) (a b : β),
  Finset.map (Function.Embedding.sectR c β) (Finset.Ico a b) = Finset.Ico (c, a) (c, b)
-- Init.Data.String.Basic
String.Pos.byteIdx_offset_next : ∀ {s : String} (p : s.Pos) (h : p ≠ s.endPos), (p.next h).offset.byteIdx = p.offset.byteIdx + (p.get h).utf8Size
-- Init.Data.String.Defs
/-- Checks whether a string is empty.

Empty strings are equal to `""` and have length and end position `0`.

Examples:
* `"".isEmpty = true`
* `"empty".isEmpty = false`
* `" ".isEmpty = false`
 -/
String.isEmpty : String → Bool
-- Std.Time.Date.Unit.Weekday
Std.Time.Weekday.instLawfulEqOrd : Std.LawfulEqOrd Std.Time.Weekday
-- Lean.Language.Basic
Lean.Language.SyntaxGuarded.mk : {α : Type} → Lean.Syntax → α → Lean.Language.SyntaxGuarded α
-- Mathlib.Order.Filter.CardinalInter
Filter.cardinalInter_ofCardinalInter : ∀ {α : Type u} {c : Cardinal.{u}} (l : Set (Set α)) (hc : 2 < c)
  (hl : ∀ (S : Set (Set α)), Cardinal.mk ↑S < c → S ⊆ l → ⋂₀ S ∈ l) (h_mono : ∀ (s t : Set α), s ∈ l → s ⊆ t → t ∈ l),
  CardinalInterFilter (Filter.ofCardinalInter l hc hl h_mono) c
-- Mathlib.Analysis.Convex.SpecificFunctions.Deriv
hasDerivAt_sqrt_mul_log : ∀ {x : ℝ}, x ≠ 0 → HasDerivAt (fun x => √x * Real.log x) ((2 + Real.log x) / (2 * √x)) x
-- Mathlib.Order.BourbakiWitt
ChainCompletePartialOrder.bot_isAdmissible : ∀ {α : Type u_1} [inst : ChainCompletePartialOrder α] {x : α} {f : α → α},
  (∀ (x : α), x ≤ f x) → ChainCompletePartialOrder.IsAdmissible x f (ChainCompletePartialOrder.bot x f)
-- Mathlib.Order.WellFounded
/-- A strictly monotone function `f` on a cowell-order satisfies `f x ≤ x` for all `x`.  -/
StrictMono.le_id : ∀ {β : Type u_2} [inst : LinearOrder β] [WellFoundedGT β] {f : β → β}, StrictMono f → f ≤ id
-- Lean.Elab.InfoTree.Types
Lean.Elab.FVarAliasInfo.userName : Lean.Elab.FVarAliasInfo → Lean.Name
-- Mathlib.MeasureTheory.Covering.Differentiation
/-- If `ρ` is absolutely continuous with respect to `μ`, then for almost every `x`,
the ratio `ρ a / μ a` converges as `a` shrinks to `x` along a Vitali family for `μ`.  -/
VitaliFamily.ae_tendsto_div : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  (v : VitaliFamily μ) [SecondCountableTopology α] [BorelSpace α] [MeasureTheory.IsLocallyFiniteMeasure μ]
  {ρ : MeasureTheory.Measure α} [MeasureTheory.IsLocallyFiniteMeasure ρ],
  ρ.AbsolutelyContinuous μ → ∀ᵐ (x : α) ∂μ, ∃ c, Filter.Tendsto (fun a => ρ a / μ a) (v.filterAt x) (nhds c)
-- Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Real.rpow_eq_nhds_of_pos : ∀ {p : ℝ × ℝ}, 0 < p.1 → (fun x => x.1 ^ x.2) =ᶠ[nhds p] fun x => Real.exp (Real.log x.1 * x.2)
-- Mathlib.Topology.MetricSpace.Thickening
Metric.thickening_of_nonpos : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {δ : ℝ}, δ ≤ 0 → ∀ (s : Set α), Metric.thickening δ s = ∅
-- Std.Data.DHashMap.Internal.Model
_private.Std.Data.DHashMap.Internal.Model.0.Std.DHashMap.Internal.Raw₀.Const.insertListₘ.match_1.splitter : {α : Type u_2} →
  {β : Type u_1} →
    (motive : List (α × β) → Sort u_3) →
      (l : List (α × β)) → (Unit → motive []) → ((hd : α × β) → (tl : List (α × β)) → motive (hd :: tl)) → motive l
-- Mathlib.Tactic.Ring.Common
/-- Zero is a polynomial. `e` is the expression `0`.  -/
Mathlib.Tactic.Ring.Common.ExSumNat.zero : Mathlib.Tactic.Ring.Common.ExSumNat q(0)
-- Mathlib.CategoryTheory.Presentable.LocallyPresentable
/-- Given a regular cardinal `κ`, a category `C` is `κ`-locally presentable
if it is cocomplete and admits a (small) family `G : ι → C` of `κ`-presentable
objects such that any object identifies as a `κ`-filtered colimit of these objects.  -/
CategoryTheory.IsCardinalLocallyPresentable : (C : Type u) → [CategoryTheory.Category.{v, u} C] → (κ : Cardinal.{w}) → [Fact κ.IsRegular] → Prop
-- Mathlib.Data.Ordmap.Invariants
/-- The full balance operation. This is the same as `balance`, but with less manual inlining.
It is somewhat easier to work with this version in proofs.  -/
Ordnode.balance' : {α : Type u_1} → Ordnode α → α → Ordnode α → Ordnode α
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
AntitoneOn.add_const : ∀ {α : Type u_1} {β : Type u_2} [inst : Add α] [inst_1 : Preorder α] [inst_2 : Preorder β] {f : β → α} {s : Set β}
  [AddRightMono α], AntitoneOn f s → ∀ (a : α), AntitoneOn (fun x => f x + a) s
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey!_erase_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → ∀ {k : α}, (t.erase k).getKey! k = default
-- Mathlib.MeasureTheory.VectorMeasure.Variation.Basic
MeasureTheory.VectorMeasure.variation_eq_ennrealToMeasure : ∀ {X : Type u_1} {mX : MeasurableSpace X} (μ : MeasureTheory.VectorMeasure X ENNReal), μ.variation = μ.ennrealToMeasure
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.hasSum_of_disjoint_iUnion : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {M : Type u_3} [inst : AddCommMonoid M]
  [inst_1 : TopologicalSpace M] [Countable β] {v : MeasureTheory.VectorMeasure α M} {f : β → Set α},
  (∀ (i : β), MeasurableSet (f i)) → Pairwise (Function.onFun Disjoint f) → HasSum (fun i => v (f i)) (v (⋃ i, f i))
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.size_filter_eq_size_iff : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  {f : α → β → Bool},
  (Std.DTreeMap.filter f t).size = t.size ↔
    ∀ (a : α) (h : a ∈ t), f (t.getKey a h) (Std.DTreeMap.Const.get t a h) = true
-- Mathlib.RingTheory.Extension.Presentation.Core
Algebra.Presentation.coeffs_relation_subset_coeffs : ∀ {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] {P : Algebra.Presentation R S ι σ} (x : σ), ↑(MvPolynomial.coeffs (P.relation x)) ⊆ P.coeffs
-- Mathlib.Algebra.BigOperators.Expect
Finset.expect_image : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : Module ℚ≥0 M] {f : ι → M}
  {t : Finset κ} [inst_2 : DecidableEq ι] {m : κ → ι},
  Set.InjOn m ↑t → ((Finset.image m t).expect fun i => f i) = t.expect fun i => f (m i)
-- Lean.Meta.Tactic.Grind.Arith.Simproc
Lean.Meta.Grind.Arith.normIntAddInst : Lean.Meta.Simp.DSimproc
-- Mathlib.Topology.Algebra.PontryaginDual
PontryaginDual.instContinuousMapClassCircle : ∀ {A : Type u_1} [inst : Monoid A] [inst_1 : TopologicalSpace A], ContinuousMapClass (PontryaginDual A) A Circle
-- Std.Tactic.BVDecide.Syntax
/-- Whether to use the binary LRAT proof format.
 -/
Lean.Elab.Tactic.BVDecide.BVDecideConfig.binaryProofs : Lean.Elab.Tactic.BVDecide.BVDecideConfig → Bool
-- Mathlib.Topology.UniformSpace.UniformApproximation
/-- A uniform limit of continuous functions is continuous.  -/
TendstoUniformly.continuous : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : TopologicalSpace α] [inst_1 : UniformSpace β] {F : ι → α → β}
  {f : α → β} {p : Filter ι}, TendstoUniformly F f p → (∃ᶠ (n : ι) in p, Continuous (F n)) → Continuous f
-- Mathlib.LinearAlgebra.AffineSpace.Independent
AffineIndependent.indicator_extend_eq_of_affineCombination_comp_embedding_eq : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {ι : Type u_4} {ι₂ : Type u_5} {p : ι → P},
  AffineIndependent k p →
    ∀ {s₁ : Finset ι} {s₂ : Finset ι₂} {w₁ : ι → k} {w₂ : ι₂ → k},
      ∑ i ∈ s₁, w₁ i = 1 →
        ∑ i ∈ s₂, w₂ i = 1 →
          ∀ (e : ι₂ ↪ ι),
            (Finset.affineCombination k s₂ (p ∘ ⇑e)) w₂ = (Finset.affineCombination k s₁ p) w₁ →
              (↑(Finset.map e s₂)).indicator (Function.extend (⇑e) w₂ 0) = (↑s₁).indicator w₁
-- Mathlib.Algebra.MvPolynomial.Variables
MvPolynomial.vars_sum_subset : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {ι : Type u_3} (t : Finset ι) (φ : ι → MvPolynomial σ R)
  [inst_1 : DecidableEq σ], (∑ i ∈ t, φ i).vars ⊆ t.biUnion fun i => (φ i).vars
-- Mathlib.Geometry.Manifold.Immersion
/-- A linear equivalence `E × F ≃L[𝕜] E''` which belongs to the data of an immersion `f` at `x`:
the particular equivalence is arbitrary, but this choice matches the witnesses given by
`h.domChart` and `h.codChart`.  -/
Manifold.IsImmersionAtOfComplement.equiv : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      {E'' : Type u} →
        {F : Type u_5} →
          [inst_1 : NormedAddCommGroup E] →
            [inst_2 : NormedSpace 𝕜 E] →
              [inst_3 : NormedAddCommGroup E''] →
                [inst_4 : NormedSpace 𝕜 E''] →
                  [inst_5 : NormedAddCommGroup F] →
                    [inst_6 : NormedSpace 𝕜 F] →
                      {H : Type u_7} →
                        [inst_7 : TopologicalSpace H] →
                          {G : Type u_9} →
                            [inst_8 : TopologicalSpace G] →
                              {I : ModelWithCorners 𝕜 E H} →
                                {J : ModelWithCorners 𝕜 E'' G} →
                                  {M : Type u_11} →
                                    [inst_9 : TopologicalSpace M] →
                                      [inst_10 : ChartedSpace H M] →
                                        {N : Type u_13} →
                                          [inst_11 : TopologicalSpace N] →
                                            [inst_12 : ChartedSpace G N] →
                                              {n : WithTop ℕ∞} →
                                                {f : M → N} →
                                                  {x : M} →
                                                    Manifold.IsImmersionAtOfComplement F I J n f x → (E × F) ≃L[𝕜] E''
-- Mathlib.Data.Fintype.Pi
Finset.instSetLike.hcongr_1 : ∀ (α α' : Type u_1), α = α' → Finset.instSetLike ≍ Finset.instSetLike
-- Mathlib.Topology.Homotopy.Equiv
ContinuousMap.HomotopyEquiv.mk : {X : Type u} →
  {Y : Type v} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] →
        (toFun : C(X, Y)) →
          (invFun : C(Y, X)) →
            (invFun.comp toFun).Homotopic (ContinuousMap.id X) →
              (toFun.comp invFun).Homotopic (ContinuousMap.id Y) → ContinuousMap.HomotopyEquiv X Y
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.ite_eq_one_sub_sq_mul_weierstrassP : ∀ (L : PeriodPair),
  ∀ l₀ ∈ L.lattice,
    ∀ (z : ℂ),
      (if z = l₀ then 1 else (z - l₀) ^ 2 * L.weierstrassP z) =
        (z - l₀) ^ 2 * L.weierstrassPExcept l₀ z + 1 - (z - l₀) ^ 2 / l₀ ^ 2
-- Lean.Meta.CompletionName
/-- Return true if name is blacklisted for completion purposes.
 -/
_private.Lean.Meta.CompletionName.0.Lean.Meta.isBlacklisted : Lean.Environment → Lean.Name → Bool
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Product
FundamentalGroupoidFunctor.piToPiTop_obj_as : ∀ {I : Type u} (X : I → TopCat) (g : (i : I) → ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj (X i))) (i : I),
  ((FundamentalGroupoidFunctor.piToPiTop X).obj g).as i = (g i).as
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.inf'_zero : ∀ {α : Type u_2} {β : Type u_3} [inst : Zero α] [inst_1 : SemilatticeInf β] (f : α → β), Finset.inf' 0 ⋯ f = f 0
-- Init.Data.Vector.Lemmas
Vector.append_right_inj : ∀ {α : Type u_1} {m n : ℕ} {ys₁ ys₂ : Vector α m} (xs : Vector α n), xs ++ ys₁ = xs ++ ys₂ ↔ ys₁ = ys₂
-- Mathlib.CategoryTheory.Limits.Types.Colimits
CategoryTheory.Limits.Types.Colimit.w_apply : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J (Type u)}
  [inst_1 : CategoryTheory.Limits.HasColimit F] {j j' : J} {x : F.obj j} (f : j ⟶ j'),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimit.ι F j'))
      ((CategoryTheory.ConcreteCategory.hom (F.map f)) x) =
    (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimit.ι F j)) x
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.mk'_neg : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Submonoid R} {M : Type u_6} {M' : Type u_7} [inst_1 : AddCommGroup M]
  [inst_2 : SubtractionCommMonoid M'] [inst_3 : Module R M] [inst_4 : Module R M'] (f : M →ₗ[R] M')
  [inst_5 : IsLocalizedModule S f] (m : M) (s : ↥S), IsLocalizedModule.mk' f (-m) s = -IsLocalizedModule.mk' f m s
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
CategoryTheory.Bicategory.IsRightAdjoint.mk' : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {a b : B} {right : b ⟶ a},
  Nonempty (CategoryTheory.Bicategory.LeftAdjoint right) → CategoryTheory.Bicategory.IsRightAdjoint right
-- Mathlib.RingTheory.Bialgebra.Hom
BialgHom.mk.sizeOf_spec : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B]
  [inst_7 : SizeOf R] [inst_8 : SizeOf A] [inst_9 : SizeOf B] (toCoalgHom : A →ₗc[R] B)
  (map_one' : toCoalgHom.toFun 1 = 1)
  (map_mul' : ∀ (x y : A), toCoalgHom.toFun (x * y) = toCoalgHom.toFun x * toCoalgHom.toFun y),
  sizeOf { toCoalgHom := toCoalgHom, map_one' := map_one', map_mul' := map_mul' } =
    1 + sizeOf toCoalgHom + sizeOf map_one'
-- Mathlib.Order.UpperLower.Prod
upperClosure_prod : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (s : Set α) (t : Set β),
  upperClosure (s ×ˢ t) = upperClosure s ×ˢ upperClosure t
-- Init.Data.Vector.Count
/-- This lemma is only relevant for `grind`.  -/
Std.Internal.Vector.not_of_countP_eq_zero_of_mem : ∀ {α : Type u_1} {p : α → Bool} {n : ℕ} {x : α} {xs : Vector α n}, Vector.countP p xs = 0 → x ∈ xs → ¬p x = true
-- Mathlib.Geometry.Manifold.VectorField.LieBracket
_private.Mathlib.Geometry.Manifold.VectorField.LieBracket.0.VectorField.mlieBracketWithin.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] (I : ModelWithCorners 𝕜 E H) {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] (V W : (x : M) → TangentSpace I x) (s : Set M) (x₀ : M),
  VectorField.mlieBracketWithin I V W s x₀ =
    VectorField.mpullback I (modelWithCornersSelf 𝕜 E) (↑(extChartAt I x₀))
      (VectorField.lieBracketWithin 𝕜
        (VectorField.mpullbackWithin (modelWithCornersSelf 𝕜 E) I (↑(extChartAt I x₀).symm) V (Set.range ↑I))
        (VectorField.mpullbackWithin (modelWithCornersSelf 𝕜 E) I (↑(extChartAt I x₀).symm) W (Set.range ↑I))
        (↑(extChartAt I x₀).symm ⁻¹' s ∩ Set.range ↑I))
      x₀
-- Lean.PrettyPrinter.Delaborator.Builtins
/-- Binder info for the parameter.  -/
Lean.PrettyPrinter.Delaborator.ParamKind.bInfo : Lean.PrettyPrinter.Delaborator.ParamKind → Lean.BinderInfo
-- Mathlib.Data.List.Sym
/-- **Alias** of `List.setOfPred_mem_sym2`. -/
List.setOf_mem_sym2 : ∀ {α : Type u_1} {xs : List α}, {z | z ∈ xs.sym2} = {x | x ∈ xs}.sym2
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp.Hom.mk.inj : ∀ {M N : SemiNormedGrp} {hom' hom'_1 : NormedAddGroupHom M.carrier N.carrier},
  { hom' := hom' } = { hom' := hom'_1 } → hom' = hom'_1
-- Mathlib.CategoryTheory.Monoidal.Functor
/-- The composition of two monoidal category equivalences is monoidal.  -/
CategoryTheory.Equivalence.isMonoidal_trans : ∀ {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] {E : Type u₃}
  [inst_4 : CategoryTheory.Category.{v₃, u₃} E] [inst_5 : CategoryTheory.MonoidalCategory E] (e : C ≌ D)
  [inst_6 : e.functor.Monoidal] [inst_7 : e.inverse.Monoidal] [e.IsMonoidal] (e' : D ≌ E) [inst_9 : e'.functor.Monoidal]
  [inst_10 : e'.inverse.Monoidal] [e'.IsMonoidal], (e.trans e').IsMonoidal
-- Mathlib.Algebra.GroupWithZero.Action.Defs
smul_eq_zero_iff_eq : ∀ {α : Type u_10} {β : Type u_11} [inst : Group α] [inst_1 : AddMonoid β] [inst_2 : DistribMulAction α β] (a : α)
  {x : β}, a • x = 0 ↔ x = 0
-- Lean.Util.ParamMinimizer
_private.Lean.Util.ParamMinimizer.0.Lean.Util.ParamMinimizer.Context.mk.inj : ∀ {m : Type → Type} {initialMask : Array Bool} {test : Array Bool → m Bool} {maxCalls : ℕ} {initialMask_1 : Array Bool}
  {test_1 : Array Bool → m Bool} {maxCalls_1 : ℕ},
  { initialMask := initialMask, test := test, maxCalls := maxCalls } =
      { initialMask := initialMask_1, test := test_1, maxCalls := maxCalls_1 } →
    initialMask = initialMask_1 ∧ test = test_1 ∧ maxCalls = maxCalls_1
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.size_alter_eq_self_of_mem : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α] (h : t.WF)
  {k : α} {f : Option β → Option β},
  k ∈ t →
    (f (Std.DTreeMap.Internal.Impl.Const.get? t k)).isSome = true →
      (Std.DTreeMap.Internal.Impl.Const.alter k f t ⋯).impl.size = t.size
-- Batteries.Data.String.Legacy
/-- Auxuliary definition for `String.Legacy.find`.

This is an old implementation, preserved here for users of the lemmas in
`Batteries.Data.String.Lemmas`.
 -/
String.Legacy.findAux : String → (Char → Bool) → String.Pos.Raw → String.Pos.Raw → String.Pos.Raw
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_rio_eq_cons : ∀ {n : ℕ}, 0 < n → (*...n).toList = 0 :: (1...n).toList
-- Mathlib.CategoryTheory.Limits.Presentation
CategoryTheory.Limits.LimitPresentation.ofIso_diag : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : CategoryTheory.Category.{t, w} J]
  {X : C} (P : CategoryTheory.Limits.LimitPresentation J X) {Y : C} (e : X ≅ Y), (P.ofIso e).diag = P.diag
-- Mathlib.NumberTheory.PrimeCounting
Nat.primesLE_eq_filter_range : ∀ (n : ℕ), n.primesLE = Finset.filter Nat.Prime (Finset.range (n + 1))
-- Mathlib.CategoryTheory.Filtered.Basic
/-- If `C` is filtered, and we have a right adjoint functor `R : C ⥤ D`, then `D` is filtered.  -/
CategoryTheory.IsFiltered.of_isRightAdjoint : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFiltered C] {D : Type u₁}
  [inst_2 : CategoryTheory.Category.{v₁, u₁} D] (R : CategoryTheory.Functor C D) [R.IsRightAdjoint],
  CategoryTheory.IsFiltered D
-- Mathlib.CategoryTheory.Iso
/-- The composition of isomorphisms is an isomorphism. Here the arguments of type `IsIso` are
explicit, to make this easier to use with the `refine` tactic, for instance.
 -/
CategoryTheory.IsIso.comp_isIso' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {h : Y ⟶ Z},
  CategoryTheory.IsIso f → CategoryTheory.IsIso h → CategoryTheory.IsIso (CategoryTheory.CategoryStruct.comp f h)
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Expr.add.sizeOf_spec : ∀ (a b : Lean.Grind.Linarith.Expr), sizeOf (a.add b) = 1 + sizeOf a + sizeOf b