mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Ext
CommMonoid.ext : ∀ {M : Type u_1} ⦃m₁ m₂ : CommMonoid M⦄, HMul.hMul = HMul.hMul → m₁ = m₂
-- Mathlib.SetTheory.ZFC.PSet
PSet.instWellFoundedRelation : WellFoundedRelation PSet.{u_1}
-- Aesop.Nanos
Aesop.instInhabitedNanos.default : Aesop.Nanos
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Real.coe_tanPartialHomeomorph_symm : ↑Real.tanPartialHomeomorph.symm = Real.arctan
-- Mathlib.RingTheory.LaurentSeries
/-- The derivative of a Laurent series.  -/
LaurentSeries.derivative : (R : Type u_3) →
  {V : Type u_4} →
    [inst : AddCommGroup V] → [inst_1 : Semiring R] → [inst_2 : Module R V] → LaurentSeries V →ₗ[R] LaurentSeries V
-- Mathlib.Algebra.SkewMonoidAlgebra.Lift
/-- Any monoid homomorphism `G →* A` can be lifted to an algebra homomorphism
`SkewMonoidAlgebra k G →ₐ[k] A`.  -/
SkewMonoidAlgebra.lift : (k : Type u_1) →
  (G : Type u_2) →
    [inst : CommSemiring k] →
      [inst_1 : Monoid G] →
        (A : Type u_4) →
          [inst_2 : Semiring A] →
            [inst_3 : Algebra k A] →
              [inst_4 : MulSemiringAction G k] →
                [inst_5 : SMulCommClass G k k] → (G →* A) ≃ (SkewMonoidAlgebra k G →ₐ[k] A)
-- Lean.Parser.Term
Lean.Parser.Term.attributes.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.LinearAlgebra.BilinearForm.IsometryEquiv
LinearMap.BilinForm.IsometryEquiv.coe_toLinearEquiv : ∀ {R : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : Module R M₁] [inst_4 : Module R M₂] {B₁ : LinearMap.BilinForm R M₁}
  {B₂ : LinearMap.BilinForm R M₂} (f : B₁.IsometryEquiv B₂), ⇑f.toLinearEquiv = ⇑f
-- Mathlib.Computability.TuringMachine.Computable
Turing.TM2Computable.toTM2ComputableAux : {α β αΓ βΓ : Type} →
  {ea : α → List αΓ} → {eb : β → List βΓ} → {f : α → β} → Turing.TM2Computable ea eb f → Turing.TM2ComputableAux αΓ βΓ
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.readyForRatAdd_insert : ∀ {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n)
  (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n), f.ReadyForRatAdd → (f.insert c).ReadyForRatAdd
-- Mathlib.Analysis.Calculus.FDeriv.CompCLM
HasFDerivWithinAt.clm_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {G : Type u_4} [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] {x : E}
  {s : Set E} {H : Type u_5} [inst_5 : NormedAddCommGroup H] [inst_6 : NormedSpace 𝕜 H] {c : E → G →L[𝕜] H}
  {c' : E →L[𝕜] G →L[𝕜] H} {u : E → G} {u' : E →L[𝕜] G},
  HasFDerivWithinAt c c' s x →
    HasFDerivWithinAt u u' s x → HasFDerivWithinAt (fun y => (c y) (u y)) (c x ∘SL u' + c'.flip (u x)) s x
-- Mathlib.Order.Filter.AtTopBot.Prod
Filter.eventually_atBot_prod_self : ∀ {α : Type u_3} [Nonempty α] [inst : Preorder α] [IsCodirectedOrder α] {p : α × α → Prop},
  (∀ᶠ (x : α × α) in Filter.atBot, p x) ↔ ∃ a, ∀ (k l : α), k ≤ a → l ≤ a → p (k, l)
-- Mathlib.Topology.UniformSpace.Equiv
UniformEquiv.toHomeomorph_apply : ∀ {α : Type u} {β : Type u_1} [inst : UniformSpace α] [inst_1 : UniformSpace β] (e : α ≃ᵤ β), ⇑e.toHomeomorph = ⇑e
-- Mathlib.Data.TypeVec
_private.Mathlib.Data.TypeVec.0.TypeVec.diagSub.match_1.eq_2 : ∀ (motive : (n : ℕ) → (α : TypeVec.{u_1} n) → (x : Fin2 n) → α x → Sort u_2) (n : ℕ) (α : TypeVec.{u_1} (n + 1))
  (x : α Fin2.fz) (h_1 : (n : ℕ) → (α : TypeVec.{u_1} (n + 1)) → (a : Fin2 n) → (x : α a.fs) → motive (n + 1) α a.fs x)
  (h_2 : (n : ℕ) → (α : TypeVec.{u_1} (n + 1)) → (x : α Fin2.fz) → motive (n + 1) α Fin2.fz x),
  (match n + 1, α, Fin2.fz, x with
    | .(n + 1), α, a.fs, x => h_1 n α a x
    | .(n + 1), α, Fin2.fz, x => h_2 n α x) =
    h_2 n α x
-- Init.Data.Nat.Internal.SOM
Nat.Internal.SOM.Expr.toPoly_denote : ∀ (ctx : Nat.Internal.Linear.Context) (e : Nat.Internal.SOM.Expr),
  Nat.Internal.SOM.Poly.denote ctx e.toPoly = Nat.Internal.SOM.Expr.denote ctx e
-- Lean.Server.Requests
Lean.Server.RequestM.parseRequestParams : (paramType : Type) → [Lean.FromJson paramType] → Lean.Json → Lean.Server.RequestM paramType
-- Mathlib.CategoryTheory.MorphismProperty.Representable
/-- The lift obtained from the universal property of `(A₁ ×_X A₂) ×_{A₁} (A₁ ×_X A₃)`.  -/
CategoryTheory.Functor.relativelyRepresentable.lift₃ : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          [inst_2 : F.Full] →
            {A₁ A₂ A₃ : C} →
              {X : D} →
                {f₁ : F.obj A₁ ⟶ X} →
                  (hf₁ : F.relativelyRepresentable f₁) →
                    (f₂ : F.obj A₂ ⟶ X) →
                      (f₃ : F.obj A₃ ⟶ X) →
                        [inst_3 : CategoryTheory.Limits.HasPullback (hf₁.fst' f₂) (hf₁.fst' f₃)] →
                          [F.Faithful] →
                            {Z : C} →
                              (x₁ : Z ⟶ A₁) →
                                (x₂ : Z ⟶ A₂) →
                                  (x₃ : Z ⟶ A₃) →
                                    CategoryTheory.CategoryStruct.comp (F.map x₁) f₁ =
                                        CategoryTheory.CategoryStruct.comp (F.map x₂) f₂ →
                                      CategoryTheory.CategoryStruct.comp (F.map x₁) f₁ =
                                          CategoryTheory.CategoryStruct.comp (F.map x₃) f₃ →
                                        (Z ⟶ hf₁.pullback₃ f₂ f₃)
-- Lean.Parser.Syntax
Lean.Parser.Command.elab.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace
SSet.S.IsUniquelyCodimOneFace.iff : ∀ {X : SSet} {d : ℕ} (x : X.obj (Opposite.op { len := d })) (y : X.obj (Opposite.op { len := d + 1 })),
  { dim := d, simplex := x }.IsUniquelyCodimOneFace { dim := d + 1, simplex := y } ↔
    ∃! i, (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X i)) y = x
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.isFractional : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  (I : FractionalIdeal S P), IsFractional S ↑I
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.containsThenInsertIfNew_snd : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF)
  {k : α} {v : β k},
  (Std.DTreeMap.Internal.Impl.containsThenInsertIfNew k v t ⋯).2.impl =
    (Std.DTreeMap.Internal.Impl.insertIfNew k v t ⋯).impl
-- Mathlib.RingTheory.Ideal.Quotient.PowTransition
Submodule.powSMulQuotInclusion_mk : ∀ {R : Type u_3} [inst : CommRing R] (I : Ideal R) {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {a b c : ℕ} (h : c = b + a) (N : Submodule R M) (x : ↥(I ^ a • N)),
  (Submodule.powSMulQuotInclusion I M h N) (Submodule.Quotient.mk x) = Submodule.Quotient.mk ↑x
-- Mathlib.Topology.Spectral.Prespectral
PrespectralSpace.of_isInducing : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [PrespectralSpace Y]
  (f : X → Y), Topology.IsInducing f → IsSpectralMap f → PrespectralSpace X
-- Mathlib.Tactic.Explode.Datatypes
/-- `Entry.depth` * `│` + `┌` Normal intro  -/
Mathlib.Explode.Status.intro : Mathlib.Explode.Status
-- Mathlib.CategoryTheory.Limits.Elements
/-- An initial object in the category `F.Elements` of a contravariant functor defines a
representation for that functor.  -/
CategoryTheory.Functor.Elements.representableByOfIsInitial : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor Cᵒᵖ (Type w)} →
      {E : F.Elements} → CategoryTheory.Limits.IsInitial E → F.RepresentableBy (Opposite.unop E.fst)
-- Aesop.Search.Main
Aesop.traceScript : {Q : Type} → [inst : Aesop.Queue Q] → Bool → Aesop.SearchM Q Unit
-- Mathlib.Algebra.Order.Module.Defs
/-- Typeclass for strict reverse monotonicity of scalar multiplication by nonnegative elements on
the left, namely `a • b₁ < a • b₂ → b₁ < b₂` if `0 ≤ a`.

You should usually not use this very granular typeclass directly, but rather a typeclass like
`IsOrderedModule`.  -/
PosSMulReflectLT : (α : Type u_1) → (β : Type u_2) → [SMul α β] → [Preorder α] → [Preorder β] → [Zero α] → Prop
-- Mathlib.Algebra.Category.ModuleCat.Colimits
ModuleCat.forget₂PreservesColimitsOfSize : ∀ (R : Type w) [inst : Ring R] [CategoryTheory.Limits.HasColimitsOfSize.{u, v, w', w' + 1} AddCommGrpCat],
  CategoryTheory.Limits.PreservesColimitsOfSize.{u, v, w', w', max w (w' + 1), w' + 1}
    (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat)
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMapClass.uniformContinuous : ∀ {F : Type u_1} {β : Type u_3} {γ : Type u_4} [inst : UniformSpace β] [inst_1 : UniformSpace γ] [inst_2 : Zero γ]
  [inst_3 : FunLike F β γ] [CompactlySupportedContinuousMapClass F β γ] (f : F), UniformContinuous ⇑f
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.instZeroCoeOfZeroMemClass : {ι : Type u_1} →
  (R : ι → Type u_2) →
    {𝓕 : Filter ι} →
      {S : ι → Type u_3} →
        [inst : (i : ι) → SetLike (S i) (R i)] →
          {B : (i : ι) → S i} →
            [inst_1 : (i : ι) → Zero (R i)] →
              [∀ (i : ι), ZeroMemClass (S i) (R i)] → Zero (RestrictedProduct (fun i => R i) (fun i => ↑(B i)) 𝓕)
-- Mathlib.Data.List.Nodup
List.Nodup.concat : ∀ {α : Type u} {l : List α} {a : α}, a ∉ l → l.Nodup → (l.concat a).Nodup
-- Mathlib.Algebra.Polynomial.Taylor
/-- `Polynomial.taylor` as an `AlgHom` for commutative semirings  -/
Polynomial.taylorAlgHom : {R : Type u_1} → [inst : CommSemiring R] → R → Polynomial R →ₐ[R] Polynomial R
-- Mathlib.CategoryTheory.Monoidal.Bimon_
CategoryTheory.Bimon.equivMonComonUnitIsoApp_hom_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (M : CategoryTheory.Bimon C),
  M.equivMonComonUnitIsoApp.hom.hom.hom = CategoryTheory.CategoryStruct.id M.X.X
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.maxKey_alter_eq_self : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α] (h : t.WF)
  {k : α} {f : Option β → Option β} {he : (Std.DTreeMap.Internal.Impl.Const.alter k f t ⋯).impl.isEmpty = false},
  (Std.DTreeMap.Internal.Impl.Const.alter k f t ⋯).impl.maxKey he = k ↔
    (f (Std.DTreeMap.Internal.Impl.Const.get? t k)).isSome = true ∧ ∀ k' ∈ t, (compare k' k).isLE = true
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- The product of a monotone function and a strictly monotone function is strictly monotone.  -/
MonotoneOn.mul_strictMono' : ∀ {α : Type u_1} {β : Type u_2} [inst : Mul α] [inst_1 : Preorder α] [inst_2 : Preorder β] {s : Set β}
  [MulLeftStrictMono α] [MulRightMono α] {f g : β → α},
  MonotoneOn f s → StrictMonoOn g s → StrictMonoOn (fun x => f x * g x) s
-- Mathlib.Algebra.Order.GroupWithZero.Defs
MulLeftStrictMono.toPosMulStrictMono : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] [MulLeftStrictMono α], PosMulStrictMono α
-- Mathlib.Analysis.Complex.Basic
Complex.exists_norm_eq_mul_self : ∀ (z : ℂ), ∃ c, ‖c‖ = 1 ∧ ↑‖z‖ = c * z
-- Init.Data.Order.Classes
Std.LawfulOrderSup.mk : ∀ {α : Type u} [inst : Max α] [inst_1 : LE α], (∀ (a b c : α), a ⊔ b ≤ c ↔ a ≤ c ∧ b ≤ c) → Std.LawfulOrderSup α
-- Mathlib.Data.List.Basic
List.length_eq_two' : ∀ {α : Type u} {l : List α} (h : l ≠ []), l.length = 2 ↔ l = [l.head h, l.getLast h]
-- Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
CategoryTheory.Functor.leftKanExtensionIsoFiberwiseColimit_inv_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] (L : CategoryTheory.Functor C D) {H : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} H] (F : CategoryTheory.Functor C H)
  [inst_3 : L.HasPointwiseLeftKanExtension F] [inst_4 : L.HasLeftKanExtension F] (X : D),
  (L.leftKanExtensionIsoFiberwiseColimit F).inv.app X =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.HasColimit.isoOfNatIso
          (CategoryTheory.Functor.isoWhiskerRight (CategoryTheory.CostructuredArrow.ιCompGrothendieckProj L X) F)).hom
      (L.leftKanExtensionObjIsoColimit F X).inv
-- Mathlib.CategoryTheory.ObjectProperty.Retract
CategoryTheory.ObjectProperty.IsStableUnderRetracts.containsZero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) [P.IsStableUnderRetracts]
  [CategoryTheory.Limits.HasZeroObject C] {X : C}, P X → P.ContainsZero
-- Mathlib.Algebra.Order.Ring.Ordering.Defs
RingPreordering.IsOrdering.toHasMemOrNegMem : ∀ {R : Type u_1} {inst : CommRing R} {P : RingPreordering R} [self : P.IsOrdering], HasMemOrNegMem P
-- Mathlib.Topology.Algebra.Monoid
Filter.TendstoNhdsWithinIio.mul_const : ∀ {α : Type u_2} {𝕜 : Type u_6} [inst : Preorder 𝕜] [inst_1 : Zero 𝕜] [inst_2 : Mul 𝕜] [inst_3 : TopologicalSpace 𝕜]
  [SeparatelyContinuousMul 𝕜] {l : Filter α} {f : α → 𝕜} {b c : 𝕜},
  0 < b →
    ∀ [MulPosStrictMono 𝕜],
      Filter.Tendsto f l (nhdsWithin c (Set.Iio c)) →
        Filter.Tendsto (fun a => f a * b) l (nhdsWithin (c * b) (Set.Iio (c * b)))
-- Mathlib.Analysis.BoxIntegral.Box.Basic
/-- The distortion of a box `I` is the maximum of the ratios of the lengths of its edges.
It is defined as the maximum of the ratios
`nndist I.lower I.upper / nndist (I.lower i) (I.upper i)`.  -/
BoxIntegral.Box.distortion : {ι : Type u_1} → [Fintype ι] → BoxIntegral.Box ι → NNReal
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
lt_add_of_lt_add_right : ∀ {α : Type u_1} [inst : Add α] [inst_1 : Preorder α] [AddRightMono α] {a b c d : α}, a < b + c → b ≤ d → a < d + c
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- Multiplying the second vector passed to `oangle` by a nonzero real does not change twice the
angle.  -/
Orientation.two_zsmul_oangle_smul_right_of_ne_zero : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) (x y : V) {r : ℝ}, r ≠ 0 → 2 • o.oangle x (r • y) = 2 • o.oangle x y
-- Mathlib.Data.Set.Basic
Set.forall_mem_empty : ∀ {α : Type u} {p : α → Prop}, (∀ x ∈ ∅, p x) ↔ True
-- Mathlib.Algebra.GroupWithZero.Defs
/-- Zero is a left absorbing element for multiplication  -/
SemigroupWithZero.zero_mul : ∀ {S₀ : Type u} [self : SemigroupWithZero S₀] (a : S₀), 0 * a = 0
-- Mathlib.Algebra.Polynomial.Expand
Polynomial.map_iterateFrobenius_expand : ∀ {R : Type u} [inst : CommSemiring R] (p : ℕ) [inst_1 : ExpChar R p] (f : Polynomial R) (n : ℕ),
  Polynomial.map (iterateFrobenius R p n) ((Polynomial.expand R (p ^ n)) f) = f ^ p ^ n
-- Mathlib.Data.Finset.Basic
Finset.mem_union_of_disjoint : ∀ {α : Type u_4} [inst : DecidableEq α] {s t : Finset α}, Disjoint s t → ∀ {x : α}, x ∈ s ∪ t ↔ Xor (x ∈ s) (x ∈ t)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.max_eq_max! : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : Inhabited α]
  {he : t.isEmpty = false}, t.max he = t.max!
-- Mathlib.CategoryTheory.Limits.Shapes.Preorder.WellOrderContinuous
/-- If `F : J ⥤ C` is well-order-continuous and `m : J` is a limit element, then
`F.obj m` identifies to the colimit of the `F.obj j` for `j < m`.  -/
CategoryTheory.Functor.isColimitOfIsWellOrderContinuous : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w} →
      [inst_1 : PartialOrder J] →
        (F : CategoryTheory.Functor J C) →
          [F.IsWellOrderContinuous] →
            (m : J) → Order.IsSuccLimit m → CategoryTheory.Limits.IsColimit ((Set.principalSegIio m).cocone F)
-- Std.Data.HashSet.Lemmas
Std.HashSet.Equiv.comm : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α}, m₁.Equiv m₂ ↔ m₂.Equiv m₁
-- Lean.Meta.Tactic.Ext
Lean.Meta.Ext.ExtTheorem.mk.inj : ∀ {declName : Lean.Name} {priority : ℕ} {keys : Array Lean.Meta.DiscrTree.Key} {declName_1 : Lean.Name} {priority_1 : ℕ}
  {keys_1 : Array Lean.Meta.DiscrTree.Key},
  { declName := declName, priority := priority, keys := keys } =
      { declName := declName_1, priority := priority_1, keys := keys_1 } →
    declName = declName_1 ∧ priority = priority_1 ∧ keys = keys_1
-- Mathlib.Algebra.Order.Interval.Set.Group
/-- If we remove a smaller interval from a larger, the result is nonempty  -/
Set.nonempty_Ico_sdiff : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [IsOrderedAddMonoid α] {x dx y dy : α},
  dy < dx → 0 < dx → Nonempty ↑(Set.Ico x (x + dx) \ Set.Ico y (y + dy))
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey!_unitOfList_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α] [inst_2 : Inhabited α]
  {l : List α} {k k' : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a == b) = false) l → k ∈ l → (Std.ExtHashMap.unitOfList l).getKey! k' = k
-- Mathlib.Algebra.Category.Grp.Basic
AddCommGrpCat.hom_comp : ∀ {X Y T : AddCommGrpCat} (f : X ⟶ Y) (g : Y ⟶ T),
  AddCommGrpCat.Hom.hom (CategoryTheory.CategoryStruct.comp f g) =
    (AddCommGrpCat.Hom.hom g).comp (AddCommGrpCat.Hom.hom f)
-- Init.Data.Int.Order
Int.neg_add_le_left_of_le_add : ∀ {a b c : ℤ}, a ≤ b + c → -b + a ≤ c
-- Mathlib.FieldTheory.SeparableDegree
/-- A polynomial has zero separable degree if and only if it is constant.  -/
Polynomial.natSepDegree_eq_zero_iff : ∀ {F : Type u} [inst : Field F] (f : Polynomial F), f.natSepDegree = 0 ↔ f.natDegree = 0
-- Mathlib.FieldTheory.Relrank
Subfield.relfinrank_eq_one_iff : ∀ {E : Type v} [inst : Field E] {A B : Subfield E}, A.relfinrank B = 1 ↔ B ≤ A
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.valueGroupOrderIso₀_symm_apply : ∀ {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] {R : Type u_3} [inst_1 : Ring R] (v : Valuation R Γ₀)
  (a : WithZero ↥(MonoidWithZeroHom.ofClass v).valueGroup),
  (WithVal.valueGroupOrderIso₀ v).symm a = (WithZero.map' ↑(WithVal.valueGroupEquiv v).symm) a
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.rpow_lt_top_iff_of_pos : ∀ {x : ENNReal} {y : ℝ}, 0 < y → (x ^ y < ⊤ ↔ x < ⊤)
-- Mathlib.RingTheory.LaurentSeries
LaurentSeries.powerSeriesPart_coeff : ∀ {R : Type u_1} [inst : Semiring R] (x : LaurentSeries R) (n : ℕ),
  (PowerSeries.coeff n) x.powerSeriesPart = x.coeff (HahnSeries.order x + ↑n)
-- Mathlib.Order.Filter.CountableInter
/-- A set is in the `countableInterFilter` generated by `g` if and only if
it contains a countable intersection of elements of `g`.  -/
Filter.mem_countableGenerate_iff : ∀ {α : Type u_2} {g : Set (Set α)} {s : Set α}, s ∈ Filter.countableGenerate g ↔ ∃ S ⊆ g, S.Countable ∧ ⋂₀ S ⊆ s
-- Mathlib.Algebra.Category.ModuleCat.Basic
ModuleCat.comp_apply : ∀ {R : Type u} [inst : Ring R] {M N O : ModuleCat R} (f : M ⟶ N) (g : N ⟶ O) (x : ↑M),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) x =
    (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) x)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.canonicalEmbedding.norm_le_iff : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (x : K) (r : ℝ),
  ‖(NumberField.canonicalEmbedding K) x‖ ≤ r ↔ ∀ (φ : K →+* ℂ), ‖φ x‖ ≤ r
-- Mathlib.CategoryTheory.Triangulated.Triangulated
CategoryTheory.Triangulated.Octahedron.triangleMorphism₂_hom₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃}
  {comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃} {v₁₂ : X₂ ⟶ Z₁₂}
  {w₁₂ : Z₁₂ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁}
  {h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  {v₂₃ : X₃ ⟶ Z₂₃} {w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₂}
  {h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  {v₁₃ : X₃ ⟶ Z₁₃} {w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁}
  {h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  (h : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃),
  h.triangleMorphism₂.hom₂ = CategoryTheory.CategoryStruct.id X₃
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.DayFunctor
CategoryTheory.MonoidalCategory.DayFunctor.Hom.mk.sizeOf_spec : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  {F G : CategoryTheory.MonoidalCategory.DayFunctor C V} [inst_4 : SizeOf C] [inst_5 : SizeOf V]
  (natTrans : F.functor ⟶ G.functor), sizeOf { natTrans := natTrans } = 1 + sizeOf natTrans
-- Lean.Util.Path
/-- Find the compiled `.olean` of a module in the `LEAN_PATH` search path.  -/
Lean.findOLean : Lean.Name → IO System.FilePath
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurable_compl : ∀ {α : Type u_1}, Measurable fun x => xᶜ
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.instInhabited : {R : Type u_1} → [inst : CommRing R] → (f : Polynomial R) → Inhabited (AdjoinRoot f)
-- Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
NumberField.Units.rank.congr_simp : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K], NumberField.Units.rank K = NumberField.Units.rank K
-- Init.Data.UInt.Basic
/-- Bitwise exclusive or for word-sized unsigned integers. Usually accessed via the `^^^` operator.

Each bit of the resulting integer is set if exactly one of the corresponding bits of both input
integers are set.

This function is overridden at runtime with an efficient implementation.
 -/
USize.xor : USize → USize → USize
-- Lean.DocString.Extension
Lean.instReprElabInline : Repr Lean.ElabInline
-- Init.Tactics
/-- This is a "finishing" tactic modification of `simp`. It has two forms.

* `simpa [rules, ⋯] using e` will simplify the goal and the type of
  `e` using `rules`, then try to close the goal using `e`.

  Simplifying the type of `e` makes it more likely to match the goal
  (which has also been simplified). This construction also tends to be
  more robust under changes to the simp lemma set.

  The final match between the simplified `e` and the simplified goal uses
  **reducible** transparency, so it does not unfold semireducible definitions.
  Write `simpa [rules, ⋯] using! e` to perform the match at the ambient
  (default/semireducible) transparency instead.

* `simpa [rules, ⋯]` will simplify the goal and the type of a
  hypothesis `this` if present in the context, then try to close the goal using
  the `assumption` tactic.

As with `simp`, the `!` modifier after `simpa` enables auto-unfolding of
definitions in the simp set.
 -/
Lean.Parser.Tactic.tacticSimpa?__1 : Lean.ParserDescr
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyMapData.zero_φQ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData),
  (CategoryTheory.ShortComplex.RightHomologyMapData.zero h₁ h₂).φQ = 0
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Coalgebra.equivOfNatIso_counitIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C C} (α : F ≅ G),
  (CategoryTheory.Endofunctor.Coalgebra.equivOfNatIso α).counitIso =
    (CategoryTheory.Endofunctor.Coalgebra.functorOfNatTransComp α.inv α.hom).symm ≪≫
      CategoryTheory.Endofunctor.Coalgebra.functorOfNatTransEq ⋯ ≪≫
        CategoryTheory.Endofunctor.Coalgebra.functorOfNatTransId