mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.Monoid.Units
AddUnits.instPreorder : {α : Type u_1} → [inst : AddMonoid α] → [Preorder α] → Preorder (AddUnits α)
-- Init.Data.Array.Lemmas
Array.swap_swap : ∀ {α : Type u_1} {xs : Array α} {i j : ℕ} (hi : i < xs.size) (hj : j < xs.size), (xs.swap i j hi hj).swap i j ⋯ ⋯ = xs
-- Aesop.Rule.Basic
Aesop.Rule.compareByPriority : {α : Type} → [Ord α] → Aesop.Rule α → Aesop.Rule α → Ordering
-- Mathlib.Logic.Equiv.Defs
Equiv.ulift_symm_apply : ∀ {α : Type v}, ⇑Equiv.ulift.symm = ULift.up
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Affine.Simplex.interior.eq_1 : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] [inst_4 : PartialOrder k] {n : ℕ} (s : Affine.Simplex k P n),
  s.interior = Affine.Simplex.setInterior (Set.Ioo 0 1) s
-- Mathlib.Data.Vector.Basic
List.Vector.cons_val : ∀ {α : Type u_1} {n : ℕ} (a : α) (v : List.Vector α n), ↑(a ::ᵥ v) = a :: ↑v
-- Mathlib.Algebra.Order.Monoid.Canonical.Basic
exists_le_add_iff_le_left : ∀ {α : Type u_1} [inst : LinearOrder α] {P : α → Prop} {b c : α} [inst_1 : Add α] [CanonicallyOrderedAdd α]
  [AddLeftMono α] [IsLeftCancelAdd α], (∃ a ≤ b + c, P a) ↔ (∃ a < b, P a) ∨ ∃ d ≤ c, P (b + d)
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
_private.Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree.0.WeierstrassCurve.expDegree_rec : ∀ (m : ℕ),
  (WeierstrassCurve.expDegree✝ (2 * (m + 3)) =
        2 * WeierstrassCurve.expDegree✝ (m + 2) + WeierstrassCurve.expDegree✝ (m + 3) +
          WeierstrassCurve.expDegree✝ (m + 5) ∧
      WeierstrassCurve.expDegree✝ (2 * (m + 3)) =
        WeierstrassCurve.expDegree✝ (m + 1) + WeierstrassCurve.expDegree✝ (m + 3) +
          2 * WeierstrassCurve.expDegree✝ (m + 4)) ∧
    (WeierstrassCurve.expDegree✝ (2 * (m + 2) + 1) =
        WeierstrassCurve.expDegree✝ (m + 4) + 3 * WeierstrassCurve.expDegree✝ (m + 2) + if Even m then 2 * 3 else 0) ∧
      WeierstrassCurve.expDegree✝ (2 * (m + 2) + 1) =
        WeierstrassCurve.expDegree✝ (m + 1) + 3 * WeierstrassCurve.expDegree✝ (m + 3) + if Even m then 0 else 2 * 3
-- Mathlib.Order.Filter.Bases.Basic
Filter.IsBasis.filter_eq_generate : ∀ {α : Type u_1} {ι : Sort u_4} {p : ι → Prop} {s : ι → Set α} (h : Filter.IsBasis p s),
  h.filter = Filter.generate {U | ∃ i, p i ∧ s i = U}
-- Mathlib.RingTheory.AdicCompletion.LocalRing
AdicCompletion.isLocalRing_of_fg : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsLocalRing R],
  (IsLocalRing.maximalIdeal R).FG → IsLocalRing (AdicCompletion (IsLocalRing.maximalIdeal R) R)
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
/-- `toSpecΓ _` is an isomorphism so these are mutually two-sided inverses.  -/
AlgebraicGeometry.LocallyRingedSpace.Γ_Spec_left_triangle : ∀ (X : AlgebraicGeometry.LocallyRingedSpace),
  CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.toSpecΓ (AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X)))
      (X.toΓSpec.c.app (Opposite.op ⊤)) =
    CategoryTheory.CategoryStruct.id (AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X))
-- Mathlib.NumberTheory.ArithmeticFunction.Misc
ArithmeticFunction.sigma_one_apply : ∀ (n : ℕ), (ArithmeticFunction.sigma 1) n = ∑ d ∈ n.divisors, d
-- Mathlib.Algebra.Category.CommAlgCat.Monoidal
CommAlgCat.binaryCofan_pt : ∀ {R : Type u} [inst : CommRing R] (A B : CommAlgCat R), (A.binaryCofan B).pt = CommAlgCat.of R (TensorProduct R ↑A ↑B)
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalSubsemiring.decidableMemCenter : {R : Type u_1} →
  [inst : NonUnitalSemiring R] →
    [DecidableEq R] → [Fintype R] → DecidablePred fun x => x ∈ NonUnitalSubsemiring.center R
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.comp_whiskerRight_assoc : ∀ {B : Type u} [self : CategoryTheory.Bicategory B] {a b c : B} {f g h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h) (i : b ⟶ c)
  {Z : a ⟶ c} (h_1 : CategoryTheory.CategoryStruct.comp h i ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.CategoryStruct.comp η θ) i)
      h_1 =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight η i)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight θ i) h_1)
-- Init.Data.List.Perm
List.cons_perm_iff_perm_erase : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a : α} {l₁ l₂ : List α},
  (a :: l₁).Perm l₂ ↔ a ∈ l₂ ∧ l₁.Perm (l₂.erase a)
-- Mathlib.Data.ZMod.Basic
ZModModule.two_le_char : ∀ (n : ℕ) (G : Type u_2) [inst : AddCommGroup G] [Module (ZMod n) G] [NeZero n] [Nontrivial G], 2 ≤ n
-- Mathlib.Analysis.Calculus.FDeriv.Norm
DifferentiableAt.differentiableAt_norm_of_smul : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {x : E} {t : ℝ},
  DifferentiableAt ℝ (fun x => ‖x‖) (t • x) → DifferentiableAt ℝ (fun x => ‖x‖) x
-- Mathlib.Analysis.InnerProductSpace.PiL2
OrthonormalBasis.repr_apply_apply : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι] (b : OrthonormalBasis ι 𝕜 E) (v : E) (i : ι),
  (b.repr v).ofLp i = inner 𝕜 (b i) v
-- Mathlib.RingTheory.Adjoin.FG
/-- A subalgebra `S` is finitely generated if there exists `t : Finset A` such that
`Algebra.adjoin R t = S`.  -/
Subalgebra.FG : {R : Type u} →
  {A : Type v} → [inst : CommSemiring R] → [inst_1 : Semiring A] → [inst_2 : Algebra R A] → Subalgebra R A → Prop
-- Init.Data.SInt.Lemmas
Int16.le_iff_toInt_le : ∀ {x y : Int16}, x ≤ y ↔ x.toInt ≤ y.toInt
-- Mathlib.Algebra.Group.Subgroup.Ker
MonoidHom.ker_prod : ∀ {G : Type u_1} [inst : Group G] {M : Type u_8} {N : Type u_9} [inst_1 : MulOneClass M] [inst_2 : MulOneClass N]
  (f : G →* M) (g : G →* N), (f.prod g).ker = f.ker ⊓ g.ker
-- Mathlib.GroupTheory.GroupAction.Hom
MulActionHom.prodMap.eq_1 : ∀ {M : Type u_1} {N : Type u_2} {α : Type u_3} {β : Type u_4} {γ : Type u_5} {δ : Type u_6} [inst : SMul M α]
  [inst_1 : SMul M β] [inst_2 : SMul N γ] [inst_3 : SMul N δ] {σ : M → N} (f : α →ₑ[σ] γ) (g : β →ₑ[σ] δ),
  f.prodMap g = { toFun := Prod.map ⇑f ⇑g, map_smul' := ⋯ }
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgHom.ofId_apply : ∀ (R : Type u_7) (A : Type u_8) [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A] [inst_3 : StarMul A]
  [inst_4 : Algebra R A] [inst_5 : StarModule R A] (a : R), (StarAlgHom.ofId R A) a = (algebraMap R A) a
-- Mathlib.RingTheory.Ideal.HasGoingUp
Algebra.HasGoingUp.exists_ideal_ge_liesOver_of_lt : ∀ {R : Type u_1} {S : Type u_2} {inst : CommRing R} {inst_1 : CommRing S} {inst_2 : Algebra R S}
  [self : Algebra.HasGoingUp R S] {q : Ideal R} [q.IsPrime] (P : Ideal S) [P.IsPrime],
  Ideal.under R P < q → ∃ Q, P ≤ Q ∧ Q.IsPrime ∧ Q.LiesOver q
-- Mathlib.Algebra.GroupWithZero.Submonoid.Pointwise
Submonoid.mem_inv_pointwise_smul_iff₀ : ∀ {G₀ : Type u_1} {M : Type u_3} [inst : Monoid M] [inst_1 : GroupWithZero G₀] [inst_2 : MulDistribMulAction G₀ M]
  {a : G₀}, a ≠ 0 → ∀ (S : Submonoid M) (x : M), x ∈ a⁻¹ • S ↔ a • x ∈ S
-- Mathlib.CategoryTheory.Sigma.Basic
CategoryTheory.Sigma.SigmaHom.assoc : ∀ {I : Type w₁} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {X Y Z W : (i : I) × C i}
  (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ W),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) h =
    CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.lift_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {V W X Y Z : C} (f : V ⟶ W) (g : V ⟶ X) (h : W ⟶ Y) (k : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift f g)
      (CategoryTheory.MonoidalCategoryStruct.tensorHom h k) =
    CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.comp f h)
      (CategoryTheory.CategoryStruct.comp g k)
-- Mathlib.Algebra.Group.Action.Equidecomp
Equidecomp.left_inv : ∀ {X : Type u_1} {G : Type u_2} [inst : Group G] [inst_1 : MulAction G X] {f : Equidecomp X G} {x : X},
  x ∈ f.source → ↑f.symm (↑f.toPartialEquiv x) = x
-- Mathlib.LinearAlgebra.Lagrange
Polynomial.eq_zero_of_degree_lt_of_eval_index_eq_zero : ∀ {R : Type u_1} [inst : CommRing R] [IsDomain R] {f : Polynomial R} {ι : Type u_2} {v : ι → R} (s : Finset ι),
  Set.InjOn v ↑s → f.degree < ↑s.card → (∀ i ∈ s, Polynomial.eval (v i) f = 0) → f = 0
-- Mathlib.CategoryTheory.MorphismProperty.Comma
/-- The object property on `StructuredArrow X R` induced by a morphism property.  -/
CategoryTheory.MorphismProperty.structuredArrowObj : {B : Type u_2} →
  [inst : CategoryTheory.Category.{v_2, u_2} B] →
    {T : Type u_3} →
      [inst_1 : CategoryTheory.Category.{v_3, u_3} T] →
        (R : CategoryTheory.Functor B T) →
          {X : T} →
            CategoryTheory.MorphismProperty T → CategoryTheory.ObjectProperty (CategoryTheory.StructuredArrow X R)
-- Aesop.Stats.Basic
Aesop.ForwardRuleStateStats.mk.sizeOf_spec : ∀ (ruleName : Aesop.RuleName) (clusterStateStats : Array Aesop.ForwardClusterStateStats),
  sizeOf { ruleName := ruleName, clusterStateStats := clusterStateStats } =
    1 + sizeOf ruleName + sizeOf clusterStateStats
-- Mathlib.CategoryTheory.Limits.WeakLimits.WeakKernels
/-- `HasWeakKernels` represents the existence of weak kernels for every morphism.  -/
CategoryTheory.Limits.HasWeakKernels : (C : Type u_1) → [inst : CategoryTheory.Category.{v_1, u_1} C] → [CategoryTheory.Limits.HasZeroMorphisms C] → Prop
-- Lean.Parser.Term
Lean.Parser.Term.matchDiscr.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.GroupTheory.OreLocalization.OreSet
OreLocalization.oreSetComm_oreDenom : ∀ {R : Type u_2} [inst : CommMonoid R] (S : Submonoid R) (r : R) (s : ↥S), OreLocalization.oreDenom r s = s
-- Mathlib.Data.Set.Lattice.Image
Set.preimage_sUnion : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set (Set β)}, f ⁻¹' ⋃₀ s = ⋃ t ∈ s, f ⁻¹' t
-- Mathlib.RepresentationTheory.Continuous.Basic
ContRepresentation.coind₁Map_comp_coind₁ResMap : ∀ {R : Type u_1} {V : Type u_3} {W : Type u_4} {U : Type u_5} [inst : Ring R] [inst_1 : AddCommGroup V]
  [inst_2 : TopologicalSpace V] [inst_3 : IsTopologicalAddGroup V] [inst_4 : Module R V] [inst_5 : AddCommGroup W]
  [inst_6 : TopologicalSpace W] [inst_7 : IsTopologicalAddGroup W] [inst_8 : Module R W] [inst_9 : AddCommGroup U]
  [inst_10 : Module R U] [inst_11 : TopologicalSpace U] [inst_12 : IsTopologicalAddGroup U] {G : Type u_7}
  {H : Type u_8} [inst_13 : Group G] [inst_14 : TopologicalSpace G] [inst_15 : TopologicalSpace R]
  [inst_16 : ContinuousSMul R V] [inst_17 : ContinuousSMul R W] [inst_18 : Group H] [inst_19 : TopologicalSpace H]
  {π : ContRepresentation R G V} [inst_20 : IsTopologicalGroup G] [inst_21 : IsTopologicalGroup H]
  [inst_22 : ContinuousSMul R U] {π' : ContRepresentation R H W} (φ : H →ₜ* G) {σ : ContRepresentation R H U}
  (f : ContIntertwiningMap (π.restrict ↑φ) π') (g : ContIntertwiningMap π' σ),
  (ContRepresentation.coind₁Map g).comp (ContRepresentation.coind₁ResMap φ f) =
    ContRepresentation.coind₁ResMap φ (g.comp f)
-- Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv
HasStrictDerivAt.clog_real : ∀ {f : ℝ → ℂ} {x : ℝ} {f' : ℂ},
  HasStrictDerivAt f f' x → f x ∈ Complex.slitPlane → HasStrictDerivAt (fun t => Complex.log (f t)) (f' / f x) x
-- Lean.Meta.Tactic.Assert
/-- The hypothesis' `BinderInfo`  -/
Lean.Meta.Hypothesis.binderInfo : Lean.Meta.Hypothesis → Lean.BinderInfo
-- Mathlib.Algebra.Field.Defs
/-- `a ^ -(n + 1) = (a ^ (n + 1))⁻¹`  -/
DivisionRing.zpow_neg' : ∀ {K : Type u_2} [self : DivisionRing K] (n : ℕ) (a : K), a ^ Int.negSucc n = (a ^ ↑n.succ)⁻¹
-- Mathlib.Tactic.Translate.UnfoldBoundary
/-- The functions that we want to unfold again after the translation has happened.  -/
Mathlib.Tactic.UnfoldBoundary.UnfoldBoundaries.insertionFuns : Mathlib.Tactic.UnfoldBoundary.UnfoldBoundaries → Lean.NameSet
-- Mathlib.RingTheory.Multiplicity
min_le_emultiplicity_add : ∀ {α : Type u_1} [inst : Semiring α] {p a b : α}, min (emultiplicity p a) (emultiplicity p b) ≤ emultiplicity p (a + b)
-- Mathlib.Analysis.Normed.Group.Basic
smul_closedBall'' : ∀ {E : Type u_5} [inst : SeminormedCommGroup E] {a b : E} {r : ℝ},
  a • Metric.closedBall b r = Metric.closedBall (a • b) r
-- Mathlib.RingTheory.WittVector.Truncated
TruncatedWittVector.truncate_comp_wittVector_truncate : ∀ {p n : ℕ} {R : Type u_1} [inst : CommRing R] [inst_1 : Fact (Nat.Prime p)] {m : ℕ} (hm : n ≤ m),
  (TruncatedWittVector.truncate hm).comp (WittVector.truncate m) = WittVector.truncate n
-- Mathlib.LinearAlgebra.Dual.Defs
LinearMap.dualMap_apply : ∀ {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : Module R M₁] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M₂] (f : M₁ →ₗ[R] M₂) (g : Module.Dual R M₂)
  (x : M₁), (f.dualMap g) x = g (f x)
-- Mathlib.LinearAlgebra.Multilinear.Curry
MultilinearMap.coe_currySumEquiv : ∀ {R : Type uR} {ι : Type uι} {ι' : Type uι'} {M₂ : Type v₂} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₂]
  [inst_2 : Module R M₂] {N : ι ⊕ ι' → Type u_1} [inst_3 : (i : ι ⊕ ι') → AddCommMonoid (N i)]
  [inst_4 : (i : ι ⊕ ι') → Module R (N i)], ⇑MultilinearMap.currySumEquiv = MultilinearMap.currySum
-- Lean.Server.ServerTask
Lean.Server.ServerTask.mk.sizeOf_spec : ∀ {α : Type u} [inst : SizeOf α] (task : Task α), sizeOf { task := task } = 1 + sizeOf task
-- Mathlib.Probability.Distributions.Binomial
ProbabilityTheory.binomial_real_singleton : ∀ (n k : ℕ) (p : ↑unitInterval), (ProbabilityTheory.binomial n p).real {k} = ↑(n.choose k) * ↑p ^ k * (1 - ↑p) ^ (n - k)
-- Mathlib.Condensed.Basic
Condensed.id_hom : ∀ {C : Type w} [inst : CategoryTheory.Category.{v, w} C] (X : Condensed C),
  (CategoryTheory.CategoryStruct.id X).hom = CategoryTheory.CategoryStruct.id X.obj
-- Mathlib.Order.TypeTags
WithTop.top : {α : Type u_1} → Top (WithTop α)
-- Std.Data.HashMap.Lemmas
Std.HashMap.contains_eq_isSome_getElem? : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {a : α}, m.contains a = m[a]?.isSome
-- Std.Time.Format.Modifier
Std.Time.instReprExtendedDayPeriod.repr : Std.Time.ExtendedDayPeriod → ℕ → Std.Format
-- Lean.Widget.InteractiveGoal
Lean.Widget.InteractiveGoals : Type
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.insertMany_list_singleton : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} {k : α} {v : β},
  Std.DHashMap.Const.insertMany m [(k, v)] = m.insert k v
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.natDegree_finSuccEquiv : ∀ {R : Type u} [inst : CommSemiring R] {n : ℕ} (f : MvPolynomial (Fin (n + 1)) R),
  ((MvPolynomial.finSuccEquiv R n) f).natDegree = MvPolynomial.degreeOf 0 f
-- Mathlib.Algebra.GroupWithZero.NonZeroDivisors
val_unitsNonZeroDivisorsEquiv_symm_apply_coe : ∀ {M₀ : Type u_1} [inst : MonoidWithZero M₀] (u : M₀ˣ), ↑↑(unitsNonZeroDivisorsEquiv.symm u) = ↑u
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.haar.chaar_self : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalGroup G]
  (K₀ : TopologicalSpace.PositiveCompacts G), MeasureTheory.Measure.haar.chaar K₀ K₀.toCompacts = 1
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.mul.eq_1 : ∀ {α : Type u_2} [inst : Mul α], Set.mul = { mul := Set.image2 fun x1 x2 => x1 * x2 }
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.cokernelSequenceCyclesEIso_hom_τ₁ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.cokernelSequenceCyclesEIso._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.cokernelSequenceCyclesEIso._auto_3),
  (X.cokernelSequenceCyclesEIso f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).hom.τ₁ =
    CategoryTheory.CategoryStruct.id ((X.H n₀).obj (CategoryTheory.ComposableArrows.mk₁ f₃))
-- Std.Time.Time.Unit.Basic
/-- Converts a `Minute.Offset` to a `Nanosecond.Offset`.
 -/
Std.Time.Minute.Offset.toNanoseconds : Std.Time.Minute.Offset → Std.Time.Nanosecond.Offset
-- Mathlib.Order.Filter.Prod
Filter.map_pure_prod : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (a : α) (B : Filter β),
  Filter.map (Function.uncurry f) (pure a ×ˢ B) = Filter.map (f a) B
-- Mathlib.CategoryTheory.Groupoid
/-- `Groupoid.inv` is involutive.  -/
CategoryTheory.Groupoid.invEquiv : {C : Type u} → [inst : CategoryTheory.Groupoid C] → {X Y : C} → (X ⟶ Y) ≃ (Y ⟶ X)
-- Mathlib.Data.ENat.Basic
ENat.sub_eq_top_iff : ∀ {a b : ℕ∞}, a - b = ⊤ ↔ a = ⊤ ∧ b ≠ ⊤
-- Mathlib.Order.RelSeries
SetRel.finiteDimensional_inv : ∀ {α : Type u_1} {r : SetRel α α}, r.inv.FiniteDimensional ↔ r.FiniteDimensional
-- Mathlib.Topology.Defs.Filter
/-- Notation for the filter of punctured neighborhoods of a point.  -/
Topology.nhdsNE : Lean.ParserDescr
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.NatTrans.leftOp_app : ∀ {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ᵒᵖ} (α : F ⟶ G) (X : Cᵒᵖ),
  (CategoryTheory.NatTrans.leftOp α).app X = (α.app (Opposite.unop X)).unop
-- Mathlib.Analysis.Complex.Trigonometric
Complex.norm_exp_I_mul_ofReal : ∀ (x : ℝ), ‖Complex.exp (Complex.I * ↑x)‖ = 1
-- Init.Data.Option.Lemmas
Option.mem_of_mem_join : ∀ {α : Type u_1} {a : α} {x : Option (Option α)}, a ∈ x.join → some a ∈ x
-- Init.Data.String.Lemmas.IsEmpty
String.Slice.copy_slice_self : ∀ {s : String.Slice} {p : s.Pos}, (s.slice p p ⋯).copy = ""
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.expMap_sum : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {ι : Type u_2} (s : Finset ι)
  (f : ι → NumberField.mixedEmbedding.realSpace K),
  ↑NumberField.mixedEmbedding.fundamentalCone.expMap (∑ i ∈ s, f i) =
    ∏ i ∈ s, ↑NumberField.mixedEmbedding.fundamentalCone.expMap (f i)
-- Init.Prelude
Lean.MonadRef.mk : {m : Type → Type} → m Lean.Syntax → ({α : Type} → Lean.Syntax → m α → m α) → Lean.MonadRef m
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2.stmts₁.eq_4 : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} (a : σ → σ) (q : Turing.TM2.Stmt Γ Λ σ),
  Turing.TM2.stmts₁ (Turing.TM2.Stmt.load a q) = insert (Turing.TM2.Stmt.load a q) (Turing.TM2.stmts₁ q)
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
CategoryTheory.isRegularMono_op_iff_isRegularEpi : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y),
  CategoryTheory.IsRegularMono f.op ↔ CategoryTheory.IsRegularEpi f
-- Mathlib.Tactic.TacticAnalysis.Declarations
/-- Run `aesop` at every step in proofs, reporting where it succeeds.  -/
linter.tacticAnalysis.tryAtEachStepAesop : Lean.Option Bool
-- Mathlib.Topology.Sheaves.Over
/-- `overPullback` and `sheafRestrict` are isomorphic under `sheafEquivOver`.  -/
TopologicalSpace.Opens.sheafRestrictSheafEquivOver : {A : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} A] →
    {X : TopCat} →
      (U : TopologicalSpace.Opens ↑X) →
        U.sheafRestrict.comp U.sheafEquivOver.inverse ≅ (Opens.grothendieckTopology ↑X).overPullback A U
-- Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
MeasureTheory.restrict_compl_sigmaFiniteSetWRT : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.SFinite ν],
  μ.AbsolutelyContinuous ν → μ.restrict (μ.sigmaFiniteSetWRT ν)ᶜ = ⊤ • ν.restrict (μ.sigmaFiniteSetWRT ν)ᶜ
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
uniformContinuous_sub : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : AddGroup α] [IsUniformAddGroup α],
  UniformContinuous fun p => p.1 - p.2
-- Init.Data.SInt.Lemmas
instAssociativeISizeHAdd : Std.Associative fun x1 x2 => x1 + x2
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
/-- The equivalence class of a Jacobian point representative on a Weierstrass curve.  -/
WeierstrassCurve.Jacobian.PointClass : (R : Type r) → [CommRing R] → Type r
-- Mathlib.CategoryTheory.Subobject.Limits
CategoryTheory.Limits.factorThruKernelSubobject_comp_arrow : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasKernel f] {W : C} (h : W ⟶ X)
  (w : CategoryTheory.CategoryStruct.comp h f = 0),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.factorThruKernelSubobject f h w)
      (CategoryTheory.Limits.kernelSubobject f).arrow =
    h
-- Mathlib.AlgebraicGeometry.Sites.QuasiCompact
AlgebraicGeometry.Scheme.bot_mem_propQCTopology : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} (X : AlgebraicGeometry.Scheme) [IsEmpty ↥X],
  ⊥ ∈ (AlgebraicGeometry.Scheme.propQCTopology P) X
-- Mathlib.LinearAlgebra.Matrix.Ideal
Ideal.mem_matrix : ∀ {R : Type u_1} [inst : Semiring R] (n : Type u_2) [inst_1 : Fintype n] [inst_2 : DecidableEq n] (I : Ideal R)
  (M : Matrix n n R), M ∈ Ideal.matrix n I ↔ ∀ (i j : n), M i j ∈ I
-- Init.Data.Array.Basic
Array.instLT : {α : Type u} → [LT α] → LT (Array α)
-- Mathlib.RingTheory.Extension.Cotangent.Basis
_private.Mathlib.RingTheory.Extension.Cotangent.Basis.0.Algebra.Generators.PresentationOfFreeCotangent.Aux.hf : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {ι : Type u_4}
  {P : Algebra.Generators R S ι} {σ : Type u_5} {b : Module.Basis σ S P.toExtension.Cotangent}
  (self : Algebra.Generators.PresentationOfFreeCotangent.Aux✝ P b) (b_1 : P.toExtension.Cotangent),
  Algebra.Extension.Cotangent.mk (Algebra.Generators.PresentationOfFreeCotangent.Aux.f✝ self b_1) = b_1
-- Mathlib.Algebra.Category.Grp.Basic
CommGrpCat.ext_iff : ∀ {X Y : CommGrpCat} {f g : X ⟶ Y},
  f = g ↔ ∀ (x : ↑X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x
-- Mathlib.Topology.ContinuousMap.Compact
ContinuousMap.dist_lt_of_nonempty : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : CompactSpace α] [inst_2 : PseudoMetricSpace β]
  {f g : C(α, β)} {C : ℝ} [Nonempty α], (∀ (x : α), dist (f x) (g x) < C) → dist f g < C
-- Aesop.Percent
Aesop.instInhabitedPercent.default : Aesop.Percent
-- Mathlib.Combinatorics.SimpleGraph.Operations
SimpleGraph.deleteEdges_edge : ∀ {V : Type u_1} {u v : V} {s : Set (Sym2 V)}, s(u, v) ∈ s → (SimpleGraph.edge u v).deleteEdges s = ⊥
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.getKeyGT?_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  t₁.Equiv t₂ → t₁.getKeyGT? k = t₂.getKeyGT? k
-- Lean.Compiler.Old
Lean.Compiler.mkEagerLambdaLiftingName : Lean.Name → ℕ → Lean.Name
-- Mathlib.Order.Category.BddOrd
_private.Mathlib.Order.Category.BddOrd.0.BddOrd.Hom.mk.injEq : ∀ {X Y : BddOrd} (hom' hom'_1 : BoundedOrderHom ↑X.toPartOrd ↑Y.toPartOrd),
  ({ hom' := hom' } = { hom' := hom'_1 }) = (hom' = hom'_1)
-- Batteries.Data.RunningStats
/-- Initialize running statistics.  -/
Batteries.RunningStats.init : ℕ → Float → Float → Batteries.RunningStats
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.Homotopy.op_h₀ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂),
  h.op.h₀ = h.h₃.op
-- Mathlib.Order.WithBot
WithTop.le_iff_forall : ∀ {α : Type u_1} [inst : LE α] {x y : WithTop α}, y ≤ x ↔ ∀ (a : α), x = ↑a → ∃ b, y = ↑b ∧ b ≤ a