mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.mem_alter!_of_compare_eq : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t.WF →
    ∀ {k k' : α} {f : Option β → Option β},
      compare k k' = Ordering.eq →
        (k' ∈ Std.DTreeMap.Internal.Impl.Const.alter! k f t ↔
          (f (Std.DTreeMap.Internal.Impl.Const.get? t k)).isSome = true)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
/-- The singleton operation as a `ZeroHom`.  -/
Finset.singletonZeroHom : {α : Type u_2} → [inst : Zero α] → ZeroHom α (Finset α)
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.inductionOn₂ : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : Filter α} (f : l.Germ β) (g : l.Germ γ)
  {p : l.Germ β → l.Germ γ → Prop}, (∀ (f : α → β) (g : α → γ), p ↑f ↑g) → p f g
-- Init.Core
/-- Lifts a function from an underlying type to a function on a quotient, requiring that it respects the
quotient's relation.

Given a relation `r : α → α → Prop` and a quotient's value `q : Quot r`, applying a `f : α → β`
requires a proof `c` that `f` respects `r`. In this case, `Quot.liftOn q f h : β` evaluates
to the result of applying `f` to the underlying value in `α` from `q`.

`Quot.liftOn` is a version of the built-in primitive `Quot.lift` with its parameters re-ordered.

[Quotient types](https://lean-lang.org/doc/reference/4.33.0/find/?domain=Verso.Genre.Manual.section&name=quotients) are described in more detail in the Lean Language
Reference.
 -/
Quot.liftOn : {α : Sort u} → {β : Sort v} → {r : α → α → Prop} → Quot r → (f : α → β) → (∀ (a b : α), r a b → f a = f b) → β
-- Mathlib.CategoryTheory.ObjectProperty.Opposite
CategoryTheory.ObjectProperty.op_ofObj : ∀ {C : Type u} [inst : CategoryTheory.CategoryStruct.{v, u} C] {ι : Type u_1} (X : ι → C),
  (CategoryTheory.ObjectProperty.ofObj X).op = CategoryTheory.ObjectProperty.ofObj fun i => Opposite.op (X i)
-- Init.Data.UInt.Lemmas
UInt64.ofNatLT_mul : ∀ {a b : ℕ} (ha : a < 2 ^ 64) (hb : b < 2 ^ 64) (hab : a * b < 2 ^ 64),
  UInt64.ofNatLT (a * b) hab = UInt64.ofNatLT a ha * UInt64.ofNatLT b hb
-- Mathlib.FieldTheory.SplittingField.Construction
Polynomial.natDegree_removeFactor : ∀ {K : Type v} [inst : Field K] (f : Polynomial K), f.removeFactor.natDegree = f.natDegree - 1
-- Mathlib.CategoryTheory.Category.PartialFun
PartialFun.Iso.mk_hom : ∀ {α β : PartialFun} (e : α ≃ β) (x : α), (PartialFun.Iso.mk e).hom x = ↑(some (e x))
-- Mathlib.GroupTheory.FreeGroup.NielsenSchreier
IsFreeGroupoid.SpanningTree.treeHom_root : ∀ {G : Type u} [inst : CategoryTheory.Groupoid G] [inst_1 : IsFreeGroupoid G]
  (T : WideSubquiver (Quiver.Symmetrify (IsFreeGroupoid.Generators G)))
  [inst_2 : Quiver.Arborescence (WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T)],
  IsFreeGroupoid.SpanningTree.treeHom T (IsFreeGroupoid.SpanningTree.root'✝ T) =
    CategoryTheory.CategoryStruct.id (IsFreeGroupoid.SpanningTree.root'✝ T)
-- Mathlib.Analysis.Convex.GaugeRescale
gaugeRescale_self : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E] [T1Space E] {s : Set E},
  Absorbent ℝ s → Bornology.IsVonNBounded ℝ s → gaugeRescale s s = id
-- Mathlib.Geometry.Euclidean.Projection
/-- Subtracting the `orthogonalProjection` from `p` produces a result in the kernel of the linear
part of the orthogonal projection.  -/
EuclideanGeometry.orthogonalProjection_vsub_orthogonalProjection : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] [inst_3 : MetricSpace P] [inst_4 : NormedAddTorsor V P] (s : AffineSubspace 𝕜 P)
  [inst_5 : Nonempty ↥s] [inst_6 : s.direction.HasOrthogonalProjection] (p : P),
  s.direction.orthogonalProjectionOnto (p -ᵥ ↑((EuclideanGeometry.orthogonalProjection s) p)) = 0
-- Aesop.Script.CtorNames
Aesop.CtorNames.mkFreshArgNames : Lean.LocalContext → Aesop.CtorNames → Aesop.CtorNames × Lean.LocalContext
-- Mathlib.Data.Prod.Basic
Prod.mk_right_injective : ∀ {α : Type u_5} {β : Type u_6} (a : α), Function.Injective (Prod.mk a)
-- Mathlib.Analysis.InnerProductSpace.EuclideanDist
Euclidean.mem_ball_self : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : TopologicalSpace E] [inst_2 : IsTopologicalAddGroup E]
  [inst_3 : T2Space E] [inst_4 : Module ℝ E] [inst_5 : ContinuousSMul ℝ E] [inst_6 : FiniteDimensional ℝ E] {x : E}
  {r : ℝ}, 0 < r → x ∈ Euclidean.ball x r
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Expr.denoteSAsRing.eq_7 : ∀ {α : Type u_1} [inst : Lean.Grind.Semiring α] (ctx : Lean.Grind.CommRing.Context α) (a b : Lean.Grind.CommRing.Expr),
  Lean.Grind.CommRing.Expr.denoteSAsRing ctx (a.sub b) = 0
-- Mathlib.FieldTheory.Minpoly.ConjRootClass
ConjRootClass.mk_zero : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L], ConjRootClass.mk K 0 = 0
-- Mathlib.Algebra.Order.Ring.Abs
abs_le_one_iff_mul_self_le_one : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {a : α}, |a| ≤ 1 ↔ a * a ≤ 1
-- Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Algebra.PreSubmersivePresentation.cotangentComplexAux.eq_1 : ∀ {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] [inst_3 : Finite σ] (P : Algebra.PreSubmersivePresentation R S ι σ),
  P.cotangentComplexAux =
    ↑(Finsupp.linearEquivFunOnFinite S S σ) ∘ₗ
      Finsupp.lcomapDomain P.map ⋯ ∘ₗ ↑P.cotangentSpaceBasis.repr ∘ₗ P.toExtension.cotangentComplex
-- Mathlib.Analysis.Complex.Norm
Complex.instNormedAddCommGroup : NormedAddCommGroup ℂ
-- Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
curveIntegral_def : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {a b : E}
  [inst_5 : NormedSpace ℝ F] (ω : E → E →L[𝕜] F) (γ : Path a b),
  curveIntegral ω γ = ∫ (t : ℝ) in 0..1, curveIntegralFun ω γ t
-- Lean.Data.PersistentArray
Lean.PersistentArray.append : {α : Type u} → Lean.PersistentArray α → Lean.PersistentArray α → Lean.PersistentArray α
-- Lean.Meta.Tactic.Grind.Split
Lean.Meta.Grind.SplitCandidateAnchors : Type
-- Mathlib.Order.Circular
not_btw_of_sbtw : ∀ {α : Type u_1} [inst : CircularPreorder α] {a b c : α}, sbtw a b c → ¬btw c b a
-- Mathlib.Probability.Process.Stopping
MeasureTheory.stoppedValue_const : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : Nonempty ι] (u : ι → Ω → β) (i : ι),
  (MeasureTheory.stoppedValue u fun x => ↑i) = u i
-- Mathlib.Algebra.Lie.IdealOperations
LieSubmodule.comap_map_eq : ∀ {R : Type u} {L : Type v} {M : Type w} {M₂ : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : Module R M] [inst_4 : LieRingModule L M] [inst_5 : AddCommGroup M₂]
  [inst_6 : Module R M₂] [inst_7 : LieRingModule L M₂] (N : LieSubmodule R L M) (f : M →ₗ⁅R,L⁆ M₂),
  f.ker = ⊥ → LieSubmodule.comap f (LieSubmodule.map f N) = N
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.dvd_derivative_iff : ∀ {R : Type u} [inst : Semiring R] [NoZeroDivisors R] {P : Polynomial R},
  P ∣ Polynomial.derivative P ↔ Polynomial.derivative P = 0
-- Mathlib.Data.NNRat.Floor
NNRat.coe_ceil : ∀ (q : ℚ≥0), ↑⌈q⌉₊ = ⌈↑q⌉
-- Mathlib.Algebra.Homology.ExactSequence
CategoryTheory.ComposableArrows.Exact.isIso_map' : ∀ {C : Type u_2} [inst : CategoryTheory.Category.{v_2, u_2} C] [inst_1 : CategoryTheory.Preadditive C]
  [CategoryTheory.Balanced C] {n : ℕ} {S : CategoryTheory.ComposableArrows C n},
  S.Exact →
    ∀ (k : ℕ) (hk : k + 3 ≤ n),
      S.map' k (k + 1) ⋯ ⋯ = 0 → S.map' (k + 2) (k + 3) ⋯ hk = 0 → CategoryTheory.IsIso (S.map' (k + 1) (k + 2) ⋯ ⋯)
-- Mathlib.RingTheory.DedekindDomain.Factorization
IsDedekindDomain.HeightOneSpectrum.emultiplicity_sup : ∀ {R : Type u_3} [inst : CommRing R] [IsDedekindDomain R] (p : IsDedekindDomain.HeightOneSpectrum R) (I J : Ideal R),
  emultiplicity p.asIdeal (I ⊔ J) = min (emultiplicity p.asIdeal I) (emultiplicity p.asIdeal J)
-- Mathlib.Data.Nat.Choose.Lucas
/-- For a prime power `n`, the greatest common divisor of `choose n 1, ⋯, choose n (n - 1)`
is actually the minimal prime factor of `n`.  -/
Choose.gcd_choose_eq_minFac_of_isPrimePow : ∀ {n : ℕ}, IsPrimePow n → (Finset.Icc 1 (n - 1)).gcd n.choose = n.minFac
-- Mathlib.GroupTheory.Sylow
not_dvd_card_sylow : ∀ (p : ℕ) (G : Type u_1) [inst : Group G] [hp : Fact (Nat.Prime p)] [Finite (Sylow p G)], ¬p ∣ Nat.card (Sylow p G)
-- Mathlib.Topology.Algebra.GroupWithZero
ContinuousWithinAt.div : ∀ {α : Type u_1} {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : TopologicalSpace G₀] [ContinuousInv₀ G₀]
  [ContinuousMul G₀] {f g : α → G₀} [inst_4 : TopologicalSpace α] {s : Set α} {a : α},
  ContinuousWithinAt f s a → ContinuousWithinAt g s a → g a ≠ 0 → ContinuousWithinAt (f / g) s a
-- Mathlib.CategoryTheory.NatIso
/-- Construct a natural isomorphism between functors by giving object level isomorphisms,
and checking naturality only in the forward direction.
 -/
CategoryTheory.NatIso.ofComponents : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F G : CategoryTheory.Functor C D} →
          (app : (X : C) → F.obj X ≅ G.obj X) →
            autoParam
                (∀ {X Y : C} (f : X ⟶ Y),
                  CategoryTheory.CategoryStruct.comp (F.map f) (app Y).hom =
                    CategoryTheory.CategoryStruct.comp (app X).hom (G.map f))
                CategoryTheory.NatIso.ofComponents._auto_1 →
              (F ≅ G)
-- Std.Sat.AIG.CachedLemmas
Std.Sat.AIG.instLawfulOperatorBinaryInputMkGateCached : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α],
  Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.BinaryInput Std.Sat.AIG.mkGateCached
-- Mathlib.CategoryTheory.Subobject.ArtinianObject
CategoryTheory.isArtinianObject_of_mono : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (i : X ⟶ Y) [CategoryTheory.Mono i]
  [CategoryTheory.IsArtinianObject Y], CategoryTheory.IsArtinianObject X
-- Mathlib.RingTheory.EssentialFiniteness
Algebra.instEssFiniteTypeLocalization : ∀ (R : Type u_1) (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.EssFiniteType R S] (M : Submonoid S), Algebra.EssFiniteType R (Localization M)
-- Mathlib.Topology.UniformSpace.AbstractCompletion
/-- Lifting maps to completions  -/
AbstractCompletion.map : {α : Type uα} →
  [inst : UniformSpace α] →
    (pkg : AbstractCompletion.{vα, uα} α) →
      {β : Type uβ} →
        [inst_1 : UniformSpace β] → (pkg' : AbstractCompletion.{vβ, uβ} β) → (α → β) → pkg.space → pkg'.space
-- Init.LawfulBEqTactics
tacticDeriving_LawfulEq_tactic_step : Lean.ParserDescr
-- Mathlib.Algebra.Group.Units.Basic
RightCancelMonoid.eq_one_of_mul_left : ∀ {α : Type u} [inst : RightCancelMonoid α] [Subsingleton αˣ] {a b : α}, a * b = 1 → b = 1
-- Aesop.Forward.LevelIndex
Aesop.instToStringLevelIndex : ToString Aesop.LevelIndex
-- Mathlib.AlgebraicGeometry.Birational.Composition
AlgebraicGeometry.Scheme.PartialMap.comp_hom : ∀ {X Y Z : AlgebraicGeometry.Scheme} [inst : PreirreducibleSpace ↥X] [inst_1 : Nonempty ↥Y] (f : X.PartialMap Y)
  [inst_2 : AlgebraicGeometry.IsDominant f.hom] (g : Y.PartialMap Z),
  (f.comp g).hom =
    CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.Scheme.Hom.isoImage f.domain.ι ((TopologicalSpace.Opens.map f.hom.base).obj g.domain)).inv
      (CategoryTheory.CategoryStruct.comp (f.hom ∣_ g.domain) g.hom)
-- Mathlib.Geometry.Euclidean.Sphere.OrthRadius
EuclideanGeometry.Sphere.mem_inter_orthRadius_iff_vsub_mem_and_norm_sq : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {p q : P},
  0 ≤ s.radius →
    (q ∈ Metric.sphere s.center s.radius ∩ ↑(s.orthRadius p) ↔
      q -ᵥ p ∈ (ℝ ∙ (p -ᵥ s.center))ᗮ ∧ ‖q -ᵥ p‖ ^ 2 = s.radius ^ 2 - dist p s.center ^ 2)
-- Mathlib.CategoryTheory.Functor.EpiMono
CategoryTheory.Functor.preservesEpimorphisms_of_adjunction : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G), F.PreservesEpimorphisms
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.balLeft_toList : ∀ {α : Type u_1} {l : RBTree.RBNode α} {v : α} {r : RBTree.RBNode α}, (l.balLeft v r).toList = l.toList ++ v :: r.toList
-- Lean.Elab.PreDefinition.TerminationHint
Lean.Elab.isCoinductiveFixpoint : Lean.Elab.PartialFixpointType → Bool
-- Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
_private.Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity.0.ChevalleyThm.PolynomialC.InductionObj.mk : {R : Type u_2} → [inst : CommRing R] → {n : ℕ} → (Fin n → Polynomial R) → ChevalleyThm.PolynomialC.InductionObj✝ R n
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getKeyGT?.go.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (best : Option α) (size : ℕ) (k' : α) (v : β k')
  (l r : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.getKeyGT?.go k best (Std.DTreeMap.Internal.Impl.inner size k' v l r) =
    match compare k k' with
    | Ordering.lt => Std.DTreeMap.Internal.Impl.getKeyGT?.go k (some k') l
    | x => Std.DTreeMap.Internal.Impl.getKeyGT?.go k best r
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.addXYZ_of_Z_eq_zero_left : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} {P Q : Fin 3 → R},
  W'.Equation P → P 2 = 0 → W'.addXYZ P Q = (P 0 * Q 2) • Q
-- Mathlib.Analysis.Convex.Exposed
isExposed_empty : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : TopologicalSpace 𝕜] [inst_1 : Ring 𝕜] [inst_2 : PartialOrder 𝕜]
  [inst_3 : AddCommMonoid E] [inst_4 : TopologicalSpace E] [inst_5 : Module 𝕜 E] {A : Set E}, IsExposed 𝕜 A ∅
-- Mathlib.Tactic.CancelDenoms.Core
Mathlib.Tactic.CancelDenoms.neg_subst : ∀ {α : Type u_1} [inst : Ring α] {n e t : α}, n * e = t → n * -e = -t
-- Init.Data.UInt.Lemmas
USize.add_right_neg : ∀ (a : USize), a + -a = 0
-- Mathlib.Topology.Homeomorph.Lemmas
/-- The natural homeomorphism `(ι ⊕ ι' → X) ≃ₜ (ι → X) × (ι' → X)`.
`Equiv.sumArrowEquivProdArrow` as a homeomorphism.  -/
Homeomorph.sumArrowHomeomorphProdArrow : {X : Type u_1} → [inst : TopologicalSpace X] → {ι : Type u_7} → {ι' : Type u_8} → (ι ⊕ ι' → X) ≃ₜ (ι → X) × (ι' → X)
-- Init.Data.Iterators.Basic
/-- This type is a wrapper around `IterM` so that it becomes a useful termination measure for
recursion over productive iterators. See also `IterM.finitelyManySkips` and `Iter.finitelyManySkips`.
 -/
Std.IterM.TerminationMeasures.Productive : (α : Type w) → (m : Type w → Type w') → {β : Type w} → [Std.Iterator α m β] → Type w
-- Init.Data.List.ToArray
List.isPrefixOfAux_toArray_zero : ∀ {α : Type u_1} [inst : BEq α] (l₁ l₂ : List α) (hle : l₁.length ≤ l₂.length),
  l₁.toArray.isPrefixOfAux l₂.toArray hle 0 = l₁.isPrefixOf l₂
-- Mathlib.CategoryTheory.Limits.Presheaf
CategoryTheory.Presheaf.restrictedULiftYonedaHomEquiv'_symm_naturality_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {ℰ : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} ℰ]
  (A : CategoryTheory.Functor C ℰ) (P : CategoryTheory.Functor Cᵒᵖ (Type (max w v₁ v₂))) {E E' : ℰ} (g : E ⟶ E')
  (f : P ⟶ (CategoryTheory.Presheaf.restrictedULiftYoneda A).obj E),
  (CategoryTheory.Presheaf.restrictedULiftYonedaHomEquiv' A P E').symm
      (CategoryTheory.CategoryStruct.comp f ((CategoryTheory.Presheaf.restrictedULiftYoneda A).map g)) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Presheaf.restrictedULiftYonedaHomEquiv' A P E).symm f)
      ((CategoryTheory.Functor.const
            (CategoryTheory.CostructuredArrow CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁} P)).map
        g)
-- Mathlib.RepresentationTheory.Equiv
Representation.finsuppTensorLeft.eq_1 : ∀ {G : Type v} [inst : Monoid G] {V : Type v'} [inst_1 : AddCommMonoid V] {W : Type w'} [inst_2 : AddCommMonoid W]
  {k : Type u} [inst_3 : CommSemiring k] [inst_4 : Module k V] [inst_5 : Module k W] (σ : Representation k G V)
  (ρ : Representation k G W) (α : Type w') [inst_6 : DecidableEq α],
  σ.finsuppTensorLeft ρ α = Representation.Equiv.mk (TensorProduct.finsuppLeft k k V W α) ⋯
-- Mathlib.ModelTheory.Order
FirstOrder.Language.order.instSubsingleton : ∀ {n : ℕ}, Subsingleton (FirstOrder.Language.order.Relations n)
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
SimpleGraph.isAcyclic_iff_pairwise_not_isEdgeReachable_two : ∀ {V : Type u_1} {G : SimpleGraph V}, G.IsAcyclic ↔ Pairwise fun x1 x2 => ¬G.IsEdgeReachable 2 x1 x2
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.Comon.mkIso_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {M N : CategoryTheory.Comon C} (f : M.X ≅ N.X)
  (f_counit :
    autoParam (CategoryTheory.CategoryStruct.comp f.hom CategoryTheory.ComonObj.counit = CategoryTheory.ComonObj.counit)
      CategoryTheory.Comon.mkIso._auto_1)
  (f_comul :
    autoParam
      (CategoryTheory.CategoryStruct.comp f.hom CategoryTheory.ComonObj.comul =
        CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.comul
          (CategoryTheory.MonoidalCategoryStruct.tensorHom f.hom f.hom))
      CategoryTheory.Comon.mkIso._auto_3),
  (CategoryTheory.Comon.mkIso f f_counit f_comul).hom.hom = f.hom
-- Mathlib.Algebra.Lie.Nilpotent
LieSubmodule.lowerCentralSeries_tensor_eq_baseChange : ∀ (R : Type u_1) (A : Type u_2) (L : Type u_3) (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : LieAlgebra R L] [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M]
  [inst_6 : LieModule R L M] [inst_7 : CommRing A] [inst_8 : Algebra R A] (k : ℕ),
  LieModule.lowerCentralSeries A (TensorProduct R A L) (TensorProduct R A M) k =
    LieSubmodule.baseChange A (LieModule.lowerCentralSeries R L M k)
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.CoreHomEquiv.homEquiv_naturality_right_symm : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : CategoryTheory.Adjunction.CoreHomEquiv F G)
  {X : C} {Y Y' : D} (f : X ⟶ G.obj Y) (g : Y ⟶ Y'),
  (adj.homEquiv X Y').symm (CategoryTheory.CategoryStruct.comp f (G.map g)) =
    CategoryTheory.CategoryStruct.comp ((adj.homEquiv X Y).symm f) g
-- Mathlib.CategoryTheory.Enriched.Ordinary.Basic
CategoryTheory.ForgetEnrichment.equivInverse_obj : ∀ (V : Type u') [inst : CategoryTheory.Category.{v', u'} V] [inst_1 : CategoryTheory.MonoidalCategory V] (D : Type u'')
  [inst_2 : CategoryTheory.Category.{v'', u''} D] [inst_3 : CategoryTheory.EnrichedOrdinaryCategory V D] (X : D),
  (CategoryTheory.ForgetEnrichment.equivInverse V D).obj X = CategoryTheory.ForgetEnrichment.of V X
-- Mathlib.Data.Finsupp.Order
Finsupp.orderedSub : ∀ {ι : Type u_1} {α : Type u_3} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [inst_2 : CanonicallyOrderedAdd α]
  [inst_3 : Sub α] [inst_4 : OrderedSub α], OrderedSub (ι →₀ α)
-- Lean.Data.Lsp.TextSync
Lean.Lsp.DidSaveTextDocumentParams.mk.sizeOf_spec : ∀ (textDocument : Lean.Lsp.TextDocumentIdentifier) (text? : Option String),
  sizeOf { textDocument := textDocument, text? := text? } = 1 + sizeOf textDocument + sizeOf text?
-- Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
SSet.stdSimplex.ι₀_whiskerLeft_toSSetObjI_μ : ∀ (X : TopCat),
  CategoryTheory.CategoryStruct.comp SSet.ι₀
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (TopCat.toSSet.obj X) SSet.stdSimplex.toSSetObjI)
        (CategoryTheory.Functor.LaxMonoidal.μ TopCat.toSSet X TopCat.I)) =
    TopCat.toSSet.map TopCat.ι₀
-- Batteries.Recycling.MonadSatisfying.Basic
/-- `SatisfiesM` distributes over `*>`, general version.  -/
SatisfiesM.seqRight : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} {p₁ : α → Prop} {a : Type u_1} {p₂ : a → Prop} {y : m a} {q : a → Prop}
  [inst : Applicative m] [LawfulApplicative m] {x : m α},
  SatisfiesM p₁ x → SatisfiesM p₂ y → (∀ {a_1 : α} {b : a}, p₁ a_1 → p₂ b → q b) → SatisfiesM q (x *> y)
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
/-- The integral closure of `ℤ` inside `CyclotomicField (p ^ k) ℚ` is
`CyclotomicRing (p ^ k) ℤ ℚ`.  -/
IsCyclotomicExtension.Rat.cyclotomicRing_isIntegralClosure_of_prime_pow : ∀ {p k : ℕ} [hp : Fact (Nat.Prime p)], IsIntegralClosure (CyclotomicRing (p ^ k) ℤ ℚ) ℤ (CyclotomicField (p ^ k) ℚ)
-- Mathlib.Topology.PartialHomeomorph.Basic
/-- A partial homeomorphism defines a homeomorphism between its source and target.  -/
PartialHomeomorph.toHomeomorphSourceTarget : {X : Type u_1} →
  {Y : Type u_3} →
    [inst : TopologicalSpace X] → [inst_1 : TopologicalSpace Y] → (e : PartialHomeomorph X Y) → ↑e.source ≃ₜ ↑e.target
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionAssocNatIso_inv_app_app_app : ∀ (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.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] (X X_1 : C) (X_2 : D),
  (((CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionAssocNatIso C D).inv.app X).app X_1).app X_2 =
    (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso X X_1 X_2).inv
-- Std.Data.ExtDHashMap.Basic
/-- Checks if a mapping for the given key exists and returns the key if it does, otherwise panics.
If no panic occurs the result is guaranteed to be pointer equal to the key in the map.
 -/
Std.ExtDHashMap.getKey! : {α : Type u} →
  {β : α → Type v} →
    {x : BEq α} → {x_1 : Hashable α} → [EquivBEq α] → [LawfulHashable α] → [Inhabited α] → Std.ExtDHashMap α β → α → α
-- Mathlib.Order.Filter.Bases.Basic
/-- If `{s i | p i}` is a basis of a filter `l` and each `s i` includes `s j` such that
`p j ∧ q j`, then `{s j | p j ∧ q j}` is a basis of `l`.  -/
Filter.HasBasis.restrict : ∀ {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α},
  l.HasBasis p s → ∀ {q : ι → Prop}, (∀ (i : ι), p i → ∃ j, p j ∧ q j ∧ s j ⊆ s i) → l.HasBasis (fun i => p i ∧ q i) s
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Ult
Std.Tactic.BVDecide.BVPred.instLawfulOperatorBinaryRefVecMkUlt : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ},
  Std.Sat.AIG.LawfulOperator α (fun x => x.BinaryRefVec w) Std.Tactic.BVDecide.BVPred.mkUlt
-- Mathlib.Topology.Algebra.Group.Pointwise
IsTopologicalAddGroup.t2Space_iff_zero_closed : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [IsTopologicalAddGroup G], T2Space G ↔ IsClosed {0}
-- Init.Data.BitVec.Bitblast
BitVec.DivModState.Lawful.mk : ∀ {w : ℕ} {args : BitVec.DivModArgs w} {qr : BitVec.DivModState w},
  qr.wr + qr.wn = w →
    0 < args.d →
      qr.r.toNat < args.d.toNat →
        qr.r.toNat < 2 ^ qr.wr →
          qr.q.toNat < 2 ^ qr.wr →
            args.n.toNat >>> qr.wn = args.d.toNat * qr.q.toNat + qr.r.toNat → BitVec.DivModState.Lawful args qr
-- Mathlib.Algebra.Order.GroupWithZero.Basic
neg_of_mul_pos_left : ∀ {α : Type u_1} [inst : MulZeroClass α] {a b : α} [inst_1 : LinearOrder α] [PosMulMono α] [MulPosMono α],
  0 < a * b → b ≤ 0 → a < 0
-- Mathlib.Data.Finset.NoncommProd
Finset.map_noncommSum : ∀ {F : Type u_1} {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : AddMonoid β] [inst_1 : AddMonoid γ]
  [inst_2 : FunLike F β γ] [inst_3 : AddMonoidHomClass F β γ] (s : Finset α) (f : α → β)
  (comm : (↑s).Pairwise (Function.onFun AddCommute f)) (g : F),
  g (s.noncommSum f comm) = s.noncommSum (fun i => g (f i)) ⋯
-- Mathlib.Data.Num.Lemmas
Num.natSize_to_nat : ∀ (n : Num), n.natSize = (↑n).size
-- Lean.Compiler.ExternAttr
_private.Lean.Compiler.ExternAttr.0.Lean.parseOptNum.eq_def : ∀ (pattern : String.Slice) (it : pattern.Pos) (r : ℕ),
  Lean.parseOptNum✝ pattern it r =
    if h : it.IsAtEnd then (it, r)
    else
      have c := it.get h;
      if (decide ('0' ≤ c) && decide (c ≤ '9')) = true then
        Lean.parseOptNum✝ pattern (it.next h) (r * 10 + (c.toNat - '0'.toNat))
      else (it, r)