mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.DifferentialObject
CategoryTheory.DifferentialObject.mk.injEq : ∀ {S : Type u_1} [inst : AddMonoidWithOne S] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.HasShift C S] (obj : C)
  (d : obj ⟶ (CategoryTheory.shiftFunctor C 1).obj obj)
  (d_squared :
    autoParam (CategoryTheory.CategoryStruct.comp d ((CategoryTheory.shiftFunctor C 1).map d) = 0)
      CategoryTheory.DifferentialObject.d_squared._autoParam)
  (obj_1 : C) (d_1 : obj_1 ⟶ (CategoryTheory.shiftFunctor C 1).obj obj_1)
  (d_squared_1 :
    autoParam (CategoryTheory.CategoryStruct.comp d_1 ((CategoryTheory.shiftFunctor C 1).map d_1) = 0)
      CategoryTheory.DifferentialObject.d_squared._autoParam),
  ({ obj := obj, d := d, d_squared := d_squared } = { obj := obj_1, d := d_1, d_squared := d_squared_1 }) =
    (obj = obj_1 ∧ d ≍ d_1)
-- Mathlib.Tactic.Widget.StringDiagram
Mathlib.Tactic.Widget.StringDiagram.AtomNode.mk.inj : ∀ {vPos hPosSrc hPosTar : ℕ} {atom : Mathlib.Tactic.BicategoryLike.Atom} {vPos_1 hPosSrc_1 hPosTar_1 : ℕ}
  {atom_1 : Mathlib.Tactic.BicategoryLike.Atom},
  { vPos := vPos, hPosSrc := hPosSrc, hPosTar := hPosTar, atom := atom } =
      { vPos := vPos_1, hPosSrc := hPosSrc_1, hPosTar := hPosTar_1, atom := atom_1 } →
    vPos = vPos_1 ∧ hPosSrc = hPosSrc_1 ∧ hPosTar = hPosTar_1 ∧ atom = atom_1
-- Aesop.Stats.Basic
Aesop.ScriptGenerated.hasMVar : Aesop.ScriptGenerated → Bool
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Equiv.union_congr : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ m₃ m₄ : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α], m₁.Equiv m₃ → m₂.Equiv m₄ → (m₁ ∪ m₂).Equiv (m₃ ∪ m₄)
-- Mathlib.Data.Matrix.Mul
Matrix.two_mul_expl : ∀ {R : Type u_10} [inst : NonUnitalNonAssocSemiring R] (A B : Matrix (Fin 2) (Fin 2) R),
  (A * B) 0 0 = A 0 0 * B 0 0 + A 0 1 * B 1 0 ∧
    (A * B) 0 1 = A 0 0 * B 0 1 + A 0 1 * B 1 1 ∧
      (A * B) 1 0 = A 1 0 * B 0 0 + A 1 1 * B 1 0 ∧ (A * B) 1 1 = A 1 0 * B 0 1 + A 1 1 * B 1 1
-- Mathlib.RingTheory.Ideal.Operations
IsNilpotent.eq_1 : ∀ {R : Type u_3} [inst : Zero R] [inst_1 : Pow R ℕ] (x : R), IsNilpotent x = ∃ n, x ^ n = 0
-- Mathlib.Algebra.Group.Units.Equiv
Equiv.subLeft_involutive : ∀ {G : Type u_5} [inst : AddCommGroup G] (a : G), Function.Involutive ⇑(Equiv.subLeft a)
-- Mathlib.AlgebraicGeometry.Morphisms.Etale
/-- If `f ≫ g` is étale and `g` unramified, then `f` is étale.  -/
AlgebraicGeometry.Etale.of_comp : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {Z : AlgebraicGeometry.Scheme} (g : Y ⟶ Z)
  [AlgebraicGeometry.Etale (CategoryTheory.CategoryStruct.comp f g)] [AlgebraicGeometry.LocallyOfFiniteType g]
  [AlgebraicGeometry.FormallyUnramified g], AlgebraicGeometry.Etale f
-- Mathlib.Algebra.Module.Rat
/-- If `E` is a vector space over two division rings `R` and `S`, then scalar multiplications
agree on rational numbers in `R` and `S`.  -/
ratCast_smul_eq : ∀ {E : Type u_3} (R : Type u_4) (S : Type u_5) [inst : AddCommGroup E] [inst_1 : DivisionRing R]
  [inst_2 : DivisionRing S] [inst_3 : Module R E] [inst_4 : Module S E] (r : ℚ) (x : E), ↑r • x = ↑r • x
-- Mathlib.CategoryTheory.Limits.Types.Pushouts
CategoryTheory.Limits.Types.Pushout.Rel'.inl_inl : ∀ {S X₁ X₂ : Type u} {f : S ⟶ X₁} {g : S ⟶ X₂} (x₀ y₀ : S),
  (CategoryTheory.ConcreteCategory.hom g) x₀ = (CategoryTheory.ConcreteCategory.hom g) y₀ →
    CategoryTheory.Limits.Types.Pushout.Rel' f g (Sum.inl ((CategoryTheory.ConcreteCategory.hom f) x₀))
      (Sum.inl ((CategoryTheory.ConcreteCategory.hom f) y₀))
-- Lean.PrettyPrinter.Delaborator.Attributes
/-- Returns whether or not the given declaration has the `@[pp_using_anonymous_constructor]` attribute.
 -/
Lean.hasPPUsingAnonymousConstructorAttribute : Lean.Environment → Lean.Name → Bool
-- Mathlib.Topology.Category.FinTopCat
FinTopCat.mk : (toTop : TopCat) → [fintype : Fintype ↑toTop] → FinTopCat
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
CategoryTheory.Limits.pushoutIsoOpPullback_inr_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : Cᵒᵖ} (f : X ⟶ Z) (g : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasPushout f g],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr f g)
      (CategoryTheory.Limits.pushoutIsoOpPullback f g).hom =
    (CategoryTheory.Limits.pullback.snd f.unop g.unop).op
-- Mathlib.Analysis.BoxIntegral.Partition.Tagged
/-- Given two partitions `π₁` and `π₁`, one of them tagged and the other is not, returns the tagged
partition with `toPrepartition = π₁.toPrepartition ⊓ π₂` and tags coming from `π₁`.

Note that usually the result is not a Henstock partition.  -/
BoxIntegral.TaggedPrepartition.infPrepartition : {ι : Type u_1} →
  {I : BoxIntegral.Box ι} →
    BoxIntegral.TaggedPrepartition I → BoxIntegral.Prepartition I → BoxIntegral.TaggedPrepartition I
-- Mathlib.Analysis.LocallyConvex.BalancedCoreHull
IsClosed.balancedCore : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NormedDivisionRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [ContinuousSMul 𝕜 E] {U : Set E}, IsClosed U → IsClosed (balancedCore 𝕜 U)
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.orderIsoMapComap_symm_apply' : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  {τ₂₁ : R₂ →+* R} [inst_6 : RingHomInvPair τ₁₂ τ₂₁] [inst_7 : RingHomInvPair τ₂₁ τ₁₂] (e : M ≃ₛₗ[τ₁₂] M₂)
  (p : Submodule R₂ M₂), (Submodule.orderIsoMapComap e).symm p = Submodule.map (↑e.symm) p
-- Mathlib.Algebra.Category.Semigrp.Basic
/-- Build an `AddEquiv` from an isomorphism in the category `AddMagmaCat`.  -/
CategoryTheory.Iso.addMagmaCatIsoToAddEquiv : {X Y : AddMagmaCat} → (X ≅ Y) → ↑X ≃+ ↑Y
-- Init.Grind.AC
Lean.Grind.AC.Expr.op.inj : ∀ {lhs rhs lhs_1 rhs_1 : Lean.Grind.AC.Expr}, lhs.op rhs = lhs_1.op rhs_1 → lhs = lhs_1 ∧ rhs = rhs_1
-- Mathlib.Analysis.Calculus.ContDiff.Operations
/-- The product of two `C^n` functions is `C^n`.  -/
ContDiff.mul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {n : WithTop ℕ∞} {𝔸 : Type u_3} [inst_3 : NormedRing 𝔸] [inst_4 : NormedAlgebra 𝕜 𝔸]
  {f g : E → 𝔸}, ContDiff 𝕜 n f → ContDiff 𝕜 n g → ContDiff 𝕜 n fun x => f x * g x
-- Mathlib.Data.Set.Card.Arithmetic
Finset.set_ncard_biUnion_le : ∀ {α : Type u_1} {ι : Type u_2} (t : Finset ι) (s : ι → Set α), (⋃ i ∈ t, s i).ncard ≤ ∑ i ∈ t, (s i).ncard
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.stepNormal.eq_1 : Turing.ToPartrec.stepNormal Turing.ToPartrec.Code.zero' = fun k v => Turing.ToPartrec.Cfg.ret k (0 :: v)
-- Mathlib.Algebra.Category.Semigrp.Basic
AddMagmaCat.mk.inj : ∀ {carrier : Type u} {str : Add carrier} {carrier_1 : Type u} {str_1 : Add carrier_1},
  { carrier := carrier, str := str } = { carrier := carrier_1, str := str_1 } → carrier = carrier_1 ∧ str ≍ str_1
-- Mathlib.Data.Multiset.Sections
Multiset.sections_add : ∀ {α : Type u_1} (s t : Multiset (Multiset α)),
  (s + t).Sections = s.Sections.bind fun m => Multiset.map (fun x => m + x) t.Sections
-- Mathlib.GroupTheory.Nilpotent
AddSubgroup.upperCentralSeriesAux.eq_def : ∀ (G : Type u_2) [inst : AddGroup G] (x : ℕ),
  AddSubgroup.upperCentralSeriesAux G x =
    match x with
    | 0 => ⟨⊥, ⋯⟩
    | n.succ =>
      let un := AddSubgroup.upperCentralSeriesAux G n;
      have _un_characteristic := ⋯;
      ⟨un.fst.upperCentralSeriesStep, ⋯⟩
-- Mathlib.FieldTheory.PolynomialGaloisGroup
Polynomial.instEquivLikeGalSplittingField : {F : Type u_1} → [inst : Field F] → (p : Polynomial F) → EquivLike p.Gal p.SplittingField p.SplittingField
-- Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
Subgroup.op_inf : ∀ {G : Type u_2} [inst : Group G] (S₁ S₂ : Subgroup G), (S₁ ⊓ S₂).op = S₁.op ⊓ S₂.op
-- Mathlib.CategoryTheory.Pi.Basic
/-- For a family of categories `C i` indexed by `I`, an equality `i = j` in `I` induces
an equivalence `C i ≌ C j`.  -/
CategoryTheory.Pi.eqToEquivalence : {I : Type w₀} →
  (C : I → Type u₁) → [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] → {i j : I} → i = j → (C i ≌ C j)
-- Mathlib.Order.WithBot
WithTop.untopD_mono : ∀ {α : Type u_1} {a : α} [inst : LE α] {x y : WithTop α}, x ≠ ⊤ → y ≤ x → WithTop.untopD a y ≤ WithTop.untopD a x
-- Init.Data.Array.Lemmas
Array.back?_eq_some_iff : ∀ {α : Type u_1} {xs : Array α} {a : α}, xs.back? = some a ↔ ∃ ys, xs = ys.push a
-- Mathlib.LinearAlgebra.TensorProduct.Map
LinearMap.map_lTensor : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} {Q : Type u_10} {S : Type u_11}
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : AddCommMonoid Q]
  [inst_5 : AddCommMonoid S] [inst_6 : Module R M] [inst_7 : Module R N] [inst_8 : Module R S] [inst_9 : Module R P]
  [inst_10 : Module R Q] (f : M →ₗ[R] P) (g : N →ₗ[R] Q) (g' : S →ₗ[R] N) (x : TensorProduct R M S),
  (TensorProduct.map f g) ((LinearMap.lTensor M g') x) = (TensorProduct.map f (g ∘ₗ g')) x
-- Mathlib.CategoryTheory.Monad.Adjunction
/-- For a pair of functors `L : C ⥤ D`, `R : D ⥤ C`, an adjunction `h : L ⊣ R` induces a monad on
the category `C`.
 -/
CategoryTheory.Adjunction.toMonad : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {L : CategoryTheory.Functor C D} → {R : CategoryTheory.Functor D C} → (L ⊣ R) → CategoryTheory.Monad C
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.coe_zero : ∀ {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup V]
  [inst_2 : Module R V] [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] [inst_5 : AddCommGroup W]
  [inst_6 : Module R W] [inst_7 : TopologicalSpace W], ⇑0 = 0
-- Mathlib.CategoryTheory.Skeletal
Quotient.recOnSubsingleton.congr_simp : ∀ {α : Sort u} {s : Setoid α} {motive : Quotient s → Sort v} [h : ∀ (a : α), Subsingleton (motive ⟦a⟧)] (q : Quotient s)
  (f f_1 : (a : α) → motive ⟦a⟧), f = f_1 → Quotient.recOnSubsingleton q f = Quotient.recOnSubsingleton q f_1
-- Mathlib.Analysis.Normed.Group.Pointwise
singleton_div_ball_one : ∀ {E : Type u_1} [inst : SeminormedCommGroup E] (δ : ℝ) (x : E), {x} / Metric.ball 1 δ = Metric.ball x δ
-- Mathlib.Data.Finset.Insert
Finset.coe_pair : ∀ {α : Type u_1} [inst : DecidableEq α] {a b : α}, ↑{a, b} = {a, b}
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute
/-- An element commutes with `cfc f a` if it commutes with both `a` and `star a`.

If the base ring is `ℝ` or `ℝ≥0`, see `Commute.cfc_real` or `Commute.cfc_nnreal` which don't require
the `Commute (star a) b` hypothesis.  -/
Commute.cfc : ∀ {𝕜 : Type u_1} {A : Type u_2} {p : A → Prop} [inst : RCLike 𝕜] [inst_1 : Ring A] [inst_2 : StarRing A]
  [inst_3 : Algebra 𝕜 A] [inst_4 : TopologicalSpace A] [inst_5 : ContinuousFunctionalCalculus 𝕜 A p]
  [IsSemitopologicalRing A] [T2Space A] {a b : A}, Commute a b → Commute (star a) b → ∀ (f : 𝕜 → 𝕜), Commute (cfc f a) b
-- Mathlib.Topology.DiscreteQuotient
DiscreteQuotient.LEComap.mono : ∀ {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : C(X, Y)}
  {A A' : DiscreteQuotient X} {B B' : DiscreteQuotient Y},
  DiscreteQuotient.LEComap f A B → A' ≤ A → B ≤ B' → DiscreteQuotient.LEComap f A' B'
-- Mathlib.Topology.Connected.Clopen
nonempty_inter : ∀ {α : Type u} [inst : TopologicalSpace α] [PreconnectedSpace α] {s t : Set α},
  IsOpen s → IsOpen t → s ∪ t = Set.univ → s.Nonempty → t.Nonempty → (s ∩ t).Nonempty
-- Mathlib.Topology.Bornology.Constructions
instBornologySubtype : {α : Type u_1} → [Bornology α] → {p : α → Prop} → Bornology (Subtype p)
-- Mathlib.CategoryTheory.Equivalence
/-- The other triangle equality. The proof follows the following proof in Globular:
http://globular.science/1905.001  -/
CategoryTheory.Equivalence.unit_inverse_comp_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D) (Y : D) {Z : C} (h : e.inverse.obj Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (e.unit.app (e.inverse.obj Y))
      (CategoryTheory.CategoryStruct.comp (e.inverse.map (e.counit.app Y)) h) =
    h
-- Lean.Declaration
Lean.Declaration.quotDecl.sizeOf_spec : sizeOf Lean.Declaration.quotDecl = 1
-- Mathlib.Algebra.MonoidAlgebra.Cardinal
MonoidAlgebra.cardinalMk_of_infinite : ∀ (R M : Type u) [inst : Semiring R] [Infinite M] [Nontrivial R],
  Cardinal.mk (MonoidAlgebra R M) = max (Cardinal.mk R) (Cardinal.mk M)
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.card_roots_le_one_of_irreducible : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] {p : Polynomial R}, Irreducible p → p.roots.card ≤ 1
-- Mathlib.CategoryTheory.Sites.IsSheafFor
/-- Get the amalgamation of the given compatible family, provided we have a sheaf.  -/
CategoryTheory.Presieve.IsSheafFor.amalgamate : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {P : CategoryTheory.Functor Cᵒᵖ (Type w)} →
      {X : C} →
        {R : CategoryTheory.Presieve X} →
          CategoryTheory.Presieve.IsSheafFor P R →
            (x : CategoryTheory.Presieve.FamilyOfElements P R) → x.Compatible → P.obj (Opposite.op X)
-- Mathlib.NumberTheory.Padics.Hensel
_private.Mathlib.NumberTheory.Padics.Hensel.0.newton_seq_gen.eq_1 : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : CommSemiring R] [inst_2 : Algebra R ℤ_[p]]
  {F : Polynomial R} {a : ℤ_[p]}
  (hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2) (n : ℕ),
  newton_seq_gen✝ hnorm n = ↑(newton_seq_aux✝ hnorm n)
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Real.rpowIntegrand₀₁_one_ge_rpow_sub_two : ∀ {p t : ℝ}, p ∈ Set.Ioo 0 1 → 1 ≤ t → 1 / 2 * t ^ (p - 2) ≤ p.rpowIntegrand₀₁ t 1
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.liftToInitialUnique_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  {Z : D} (F : CategoryTheory.Functor C D) (hZ : CategoryTheory.Limits.IsInitial Z)
  (G : CategoryTheory.Functor (CategoryTheory.WithInitial C) D) (h : CategoryTheory.WithInitial.incl.comp G ≅ F)
  (hG : G.obj CategoryTheory.WithInitial.star ≅ Z) (X : CategoryTheory.WithInitial C),
  (CategoryTheory.WithInitial.liftToInitialUnique F hZ G h hG).hom.app X =
    (match X with
      | CategoryTheory.WithInitial.of x => h.app x
      | CategoryTheory.WithInitial.star => hG).hom
-- Mathlib.Algebra.Lie.Basic
LieModuleHom.zsmul_apply : ∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup N] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : LieRingModule L M] [inst_7 : LieRingModule L N] (z : ℤ) (f : M →ₗ⁅R,L⁆ N) (m : M), (z • f) m = z • f m
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.Mon.mul.go.match_3.splitter : (motive : ℕ → Sort u_1) → (fuel : ℕ) → (Unit → motive 0) → ((fuel : ℕ) → motive fuel.succ) → motive fuel
-- Init.Data.String.Defs
String.instDecidableLtPos_1 : {s : String.Slice} → (l r : s.Pos) → Decidable (l < r)
-- Mathlib.Analysis.InnerProductSpace.PiL2
Complex.coe_orthonormalBasisOneI : ⇑Complex.orthonormalBasisOneI = ![1, Complex.I]
-- Qq.Delab
Qq.Impl.checkQqDelabOptions : Lean.PrettyPrinter.Delaborator.DelabM Unit
-- Mathlib.AlgebraicTopology.MooreComplex
_private.Mathlib.AlgebraicTopology.MooreComplex.0.AlgebraicTopology.NormalizedMooreComplex.objX.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive n.succ) → motive x
-- Mathlib.RingTheory.Length
Module.length_eq_zero_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  Module.length R M = 0 ↔ Subsingleton M
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.forIn_eq_forIn_keysArray : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} {δ : Type w} {m : Type w → Type w'}
  [inst : Monad m] [LawfulMonad m] {f : α → δ → m (ForInStep δ)} {init : δ},
  (forIn t init fun a d => f a.fst d) = forIn t.keysArray init f
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
CategoryTheory.Limits.IsZero.unop : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : Cᵒᵖ},
  CategoryTheory.Limits.IsZero X → CategoryTheory.Limits.IsZero (Opposite.unop X)
-- Std.Time.DateTime.Timestamp
/-- Adds a `Millisecond.Offset` to the given `Timestamp`.
 -/
Std.Time.Timestamp.addMilliseconds : Std.Time.Timestamp → Std.Time.Millisecond.Offset → Std.Time.Timestamp
-- Mathlib.Data.Num.Basic
PosNum.bit0.sizeOf_spec : ∀ (a : PosNum), sizeOf a.bit0 = 1 + sizeOf a
-- Init.Data.Iterators.Combinators.Monadic.Take
Std.IterM.finitelyManySkips.congr_simp : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [inst : Std.Iterator α m β] [inst_1 : Std.Iterators.Productive α m]
  (it it_1 : Std.IterM m β), it = it_1 → it.finitelyManySkips = it_1.finitelyManySkips
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic
/-- In the category of simplicial sets, a strong *inner* anodyne extension is a morphism
which belongs to the closure of *inner* horn inclusions by pushouts, coproducts,
transfinite compositions (but not by retracts). We define this class here
by saying that `f : X ⟶ Y` is a strong inner anodyne extension if `f` is a monomorphism
and there exists a regular, *inner* pairing (in the sense of Moss) for the subcomplex
`Subcomplex.range f` of `Y`.  -/
SSet.strongInnerAnodyneExtensions : CategoryTheory.MorphismProperty SSet
-- Mathlib.Order.Booleanisation
Booleanisation.compl_lift : ∀ {α : Type u_1} (a : α), (Booleanisation.lift a)ᶜ = Booleanisation.comp a
-- Mathlib.Algebra.Homology.SpectralObject.Homology
CategoryTheory.Abelian.SpectralObject.dShortComplex_X₃ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.Category.{v_2, u_2} ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {i₀ i₁ i₂ i₃ i₄ i₅ i₆ i₇ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₅ : i₄ ⟶ i₅)
  (f₆ : i₅ ⟶ i₆) (f₇ : i₆ ⟶ i₇) (n₀ n₁ n₂ n₃ n₄ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.dShortComplex._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.dShortComplex._auto_3)
  (hn₃ : autoParam (n₂ + 1 = n₃) CategoryTheory.Abelian.SpectralObject.dShortComplex._auto_5)
  (hn₄ : autoParam (n₃ + 1 = n₄) CategoryTheory.Abelian.SpectralObject.dShortComplex._auto_7),
  (X.dShortComplex f₁ f₂ f₃ f₄ f₅ f₆ f₇ n₀ n₁ n₂ n₃ n₄ hn₁ hn₂ hn₃ hn₄).X₃ = X.E f₁ f₂ f₃ n₂ n₃ n₄ ⋯ ⋯
-- Init.Data.List.Lemmas
List.getLast_replicate : ∀ {n : ℕ} {α : Type u_1} {a : α} (w : List.replicate n a ≠ []), (List.replicate n a).getLast w = a
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.instMonoidOfMulOpposite : {M : Type u_1} → [Monoid Mᵐᵒᵖ] → Monoid Mᵈᵐᵃ
-- Mathlib.Analysis.Calculus.FDeriv.Prod
hasFDerivAt_prodMk_right : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (e₀ : E)
  (f₀ : F), HasFDerivAt (fun f => (e₀, f)) (ContinuousLinearMap.inr 𝕜 E F) f₀
-- Mathlib.Algebra.Homology.DerivedCategory.HomologySequence
DerivedCategory.homologyFunctorFactorsh_inv_app_quotient_obj_assoc : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] (K : CochainComplex C ℤ) (n : ℤ) {Z : C}
  (h :
    (DerivedCategory.homologyFunctor C n).obj
        (DerivedCategory.Qh.obj ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K)) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      ((DerivedCategory.homologyFunctorFactorsh C n).inv.app ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K))
      h =
    CategoryTheory.CategoryStruct.comp ((HomotopyCategory.homologyFunctorFactors C (ComplexShape.up ℤ) n).hom.app K)
      (CategoryTheory.CategoryStruct.comp ((DerivedCategory.homologyFunctorFactors C n).inv.app K)
        (CategoryTheory.CategoryStruct.comp
          ((DerivedCategory.homologyFunctor C n).map ((DerivedCategory.quotientCompQhIso C).inv.app K)) h))
-- Mathlib.RingTheory.Unramified.Locus
/-- `Algebra.unramifiedLocus R A` is the set of primes `p` of `A` that are unramified.  -/
Algebra.unramifiedLocus : (R : Type u_1) → (A : Type u_2) → [inst : CommRing R] → [inst_1 : CommRing A] → [Algebra R A] → Set (PrimeSpectrum A)
-- Init.Data.List.MinMax
List.max?_le_iff : ∀ {α : Type u_1} {a : α} [inst : Max α] [inst_1 : LE α] [Std.LawfulOrderSup α] {xs : List α},
  xs.max? = some a → ∀ {x : α}, a ≤ x ↔ ∀ b ∈ xs, b ≤ x
-- Mathlib.Topology.ContinuousMap.Basic
ContinuousMap.piEquiv_symm_apply : ∀ {I : Type u_5} (A : Type u_6) (X : I → Type u_7) [inst : TopologicalSpace A]
  [inst_1 : (i : I) → TopologicalSpace (X i)] (f : C(A, (i : I) → X i)) (i : I),
  (ContinuousMap.piEquiv A X).symm f i = (ContinuousMap.eval i).comp f
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.mem_coe : ∀ {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} {x : P}, x ∈ ↑I ↔ x ∈ I
-- Mathlib.CategoryTheory.DifferentialObject
CategoryTheory.DifferentialObject.instFunLikeHomSubtypeObj : (S : Type u_1) →
  [inst : AddMonoidWithOne S] →
    (C : Type (u + 1)) →
      [inst_1 : CategoryTheory.LargeCategory C] →
        [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
          {FC : C → C → Type u_2} →
            {CC : C → Type u_3} →
              [inst_3 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] →
                [inst_4 : CategoryTheory.ConcreteCategory C FC] →
                  [inst_5 : CategoryTheory.HasShift C S] →
                    (X Y : CategoryTheory.DifferentialObject S C) →
                      FunLike (CategoryTheory.DifferentialObject.HomSubtype S C X Y) (CC X.obj) (CC Y.obj)
-- Mathlib.Analysis.Calculus.FDeriv.Pow
hasFDerivWithinAt_pow : ∀ {𝕜 : Type u_1} {𝔸 : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedCommRing 𝔸]
  [inst_2 : NormedAlgebra 𝕜 𝔸] (n : ℕ) {x : 𝔸} {s : Set 𝔸},
  HasFDerivWithinAt (fun x => x ^ n) ((n • x ^ (n - 1)) • ContinuousLinearMap.id 𝕜 𝔸) s x
-- Mathlib.Algebra.Lie.Free
FreeLieAlgebra.Rel.below.leibniz_lie : ∀ {R : Type u} {X : Type v} [inst : CommRing R]
  {motive : (a a_1 : FreeNonUnitalNonAssocAlgebra R X) → FreeLieAlgebra.Rel R X a a_1 → Prop}
  (a b c : FreeNonUnitalNonAssocAlgebra R X), FreeLieAlgebra.Rel.below ⋯
-- Mathlib.FieldTheory.SeparableDegree
Field.instNeZeroFinSepDegree : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] [FiniteDimensional F E],
  NeZero (Field.finSepDegree F E)
-- Aesop.Rule.Basic
Aesop.Rule.mk.inj : ∀ {α : Type} {name : Aesop.RuleName} {indexingMode : Aesop.IndexingMode} {pattern? : Option Aesop.RulePattern}
  {extra : α} {tac : Aesop.RuleTacDescr} {name_1 : Aesop.RuleName} {indexingMode_1 : Aesop.IndexingMode}
  {pattern?_1 : Option Aesop.RulePattern} {extra_1 : α} {tac_1 : Aesop.RuleTacDescr},
  { name := name, indexingMode := indexingMode, pattern? := pattern?, extra := extra, tac := tac } =
      { name := name_1, indexingMode := indexingMode_1, pattern? := pattern?_1, extra := extra_1, tac := tac_1 } →
    name = name_1 ∧ indexingMode = indexingMode_1 ∧ pattern? = pattern?_1 ∧ extra = extra_1 ∧ tac = tac_1
-- Mathlib.Topology.MetricSpace.Cover
Isometry.isCover_image_iff : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] {ε : NNReal} {s : Set X}
  {f : X → Y}, Isometry f → ∀ (C : Set X), Metric.IsCover ε (f '' s) (f '' C) ↔ Metric.IsCover ε s C