mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
/-- Fibers of `grothendieckPrecompFunctorToComma L R`, composed with `Comma.fst L R`, are isomorphic
to the projection `proj L (R.obj X)`.  -/
CategoryTheory.CostructuredArrow.ιCompGrothendieckPrecompFunctorToCommaCompFst : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {E : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} E] →
            (L : CategoryTheory.Functor C D) →
              (R : CategoryTheory.Functor E D) →
                (X : E) →
                  (CategoryTheory.Grothendieck.ι (R.comp (CategoryTheory.CostructuredArrow.functor L)) X).comp
                      ((CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToComma L R).comp
                        (CategoryTheory.Comma.fst L R)) ≅
                    CategoryTheory.CostructuredArrow.proj L (R.obj X)
-- Mathlib.Tactic.Translate.UnfoldBoundary
/-- For types, we store a cast for translating from and to the type respectively.  -/
Mathlib.Tactic.UnfoldBoundary.UnfoldBoundaries.casts : Mathlib.Tactic.UnfoldBoundary.UnfoldBoundaries → Lean.NameMap (Lean.Name × Lean.Name)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem?_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k a : α} {v : β},
  (t.insertIfNew k v)[a]? = if cmp k a = Ordering.eq ∧ k ∉ t then some v else t[a]?
-- Mathlib.RingTheory.TensorProduct.Basic
/-- The tensor product of two `R`-algebras is an `R`-algebra.  -/
Algebra.TensorProduct.instAlgebra : {R : Type uR} →
  {A : Type uA} →
    {B : Type uB} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Algebra R A] → [inst_3 : Semiring B] → [inst_4 : Algebra R B] → Algebra R (TensorProduct R A B)
-- Mathlib.Algebra.Order.Floor.Ring
Int.lt_succ_floor : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] (a : R), a < ↑⌊a⌋.succ
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.instIsCommAddMonObjTensorObj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.SymmetricCategory C] {M N : C} [inst_3 : CategoryTheory.AddMonObj M]
  [inst_4 : CategoryTheory.AddMonObj N] [CategoryTheory.IsCommAddMonObj M] [CategoryTheory.IsCommAddMonObj N],
  CategoryTheory.IsCommAddMonObj (CategoryTheory.MonoidalCategoryStruct.tensorObj M N)
-- Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
CategoryTheory.ObjectProperty.FullSubcategory.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} (obj : C)
  (property : P obj) (obj_1 : C) (property_1 : P obj_1),
  ({ obj := obj, property := property } = { obj := obj_1, property := property_1 }) = (obj = obj_1)
-- Init.Data.List.Find
List.find?_flatten_eq_none_iff : ∀ {α : Type u_1} {xs : List (List α)} {p : α → Bool},
  List.find? p xs.flatten = none ↔ ∀ ys ∈ xs, ∀ x ∈ ys, (!p x) = true
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic
/-- `monomial` is well-ordered.  -/
Tactic.ComputeAsymptotics.MultiseriesExpansion.monomial_sorted : ∀ {basis : Tactic.ComputeAsymptotics.Basis} {n : ℕ},
  (Tactic.ComputeAsymptotics.MultiseriesExpansion.monomial basis n).Sorted
-- Mathlib.Tactic.FBinop
FBinopElab.instToExprSRec : Lean.ToExpr FBinopElab.SRec
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.apply_of_lt_skipPrefixWhile_prop : ∀ {P : Char → Prop} [inst : DecidablePred P] {s : String} {pos : s.Pos} (h : pos < s.skipPrefixWhile P), P (pos.get ⋯)
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
/-- **Chinese remainder theorem** for a Dedekind domain: if the ideal `I` factors as
`∏ i, P i ^ e i`, then `R ⧸ I` factors as `Π i, R ⧸ (P i ^ e i)`.  -/
IsDedekindDomain.quotientEquivPiOfProdEq : {R : Type u_1} →
  [inst : CommRing R] →
    [IsDedekindDomain R] →
      {ι : Type u_4} →
        [inst_2 : Fintype ι] →
          (I : Ideal R) →
            (P : ι → Ideal R) →
              (e : ι → ℕ) →
                (∀ (i : ι), Prime (P i)) →
                  (Pairwise fun i j => P i ≠ P j) → ∏ i, P i ^ e i = I → R ⧸ I ≃+* ((i : ι) → R ⧸ P i ^ e i)
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.Pattern.Model.CharPred.Decidable.not_revMatchesAt_of_get : ∀ {p : Char → Prop} [inst : DecidablePred p] {s : String.Slice} {pos : s.Pos} {h : pos ≠ s.startPos},
  ¬p ((pos.prev h).get ⋯) → ¬String.Slice.Pattern.Model.RevMatchesAt p pos
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.dblU.eq_1 : ∀ {F : Type u} [inst : Field F] (W : WeierstrassCurve.Projective F) (P : Fin 3 → F),
  W.dblU P = (MvPolynomial.eval P) W.polynomialX ^ 3 / P 2 ^ 2
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.Append
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.Append.0.Std.IterM.toArray_eq_match_step.match_1.eq_2 : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} (motive : Std.IterStep (Std.IterM m β) β → Sort u_3) (it' : Std.IterM m β)
  (h_1 : (it' : Std.IterM m β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.IterM m β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.skip it' with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_2 it'
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic
_private.Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic.0.Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.monomialRpow.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (m : ℕ) → motive m.succ),
  (match 0 with
    | 0 => h_1 ()
    | m.succ => h_2 m) =
    h_1 ()
-- Init.Data.Vector.Lemmas
Vector.all_map : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {f : α → β} {xs : Vector α n} {p : β → Bool},
  (Vector.map f xs).all p = xs.all (p ∘ f)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get?_erase_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {k : α}, Std.DHashMap.Const.get? (m.erase k) k = none
-- Mathlib.Data.Sum.Order
Sum.not_inr_le_inl : ∀ {α : Type u_1} {β : Type u_2} [inst : LE α] [inst_1 : LE β] {a : α} {b : β}, ¬Sum.inr b ≤ Sum.inl a
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.eq_1 : ∀ (M : Type u_1), Mᵈᵐᵃ = Mᵐᵒᵖ
-- Mathlib.RingTheory.Ideal.Height
/-- If J is a prime ideal containing I, and its height is less than or equal to the height of I,
then J is a minimal prime over I  -/
Ideal.mem_minimalPrimes_of_height_le : ∀ {R : Type u_1} [inst : CommRing R] {I J : Ideal R},
  I ≤ J → ∀ [J.IsPrime] [J.FiniteHeight], J.height ≤ I.height → J ∈ I.minimalPrimes
-- Mathlib.Analysis.Meromorphic.FactorizedRational
/-- Variant of `meromorphicTrailingCoeffAt_factorizedRational`: Compute log of the norm of the trailing
coefficient.  The convention that `log 0 = 0` gives a closed formula easier than the one in
`meromorphicTrailingCoeffAt_factorizedRational`.
 -/
Function.FactorizedRational.log_norm_meromorphicTrailingCoeffAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {d : 𝕜 → ℤ} {x : 𝕜},
  Function.HasFiniteSupport d →
    Real.log ‖meromorphicTrailingCoeffAt (∏ᶠ (u : 𝕜), (fun x => x - u) ^ d u) x‖ = ∑ᶠ (u : 𝕜), ↑(d u) * Real.log ‖x - u‖
-- Mathlib.Algebra.Group.Subgroup.Map
Subgroup.map_one_eq_bot : ∀ {G : Type u_1} [inst : Group G] (K : Subgroup G) {N : Type u_5} [inst_1 : Group N], Subgroup.map 1 K = ⊥
-- Lean.Language.Lean.Types
/-- Snapshot after command elaborator has returned. Also contains diagnostics from the elaborator's main
task. Asynchronous elaboration tasks may not yet be finished.
 -/
Lean.Language.Lean.CommandResultSnapshot : Type
-- Mathlib.Tactic.Linter.Header
/-- The "header" style linter checks that a file starts with
```
/-
Copyright ...
Apache ...
Authors ...
-/

import statements*
module doc-string*
remaining file
```
It emits a warning if
* the copyright statement is malformed;
* `Mathlib.Tactic` is imported;
* any import in `Lake` is present;
* the first non-`import` command is not a module doc-string.

The linter allows `import`-only files and does not require a copyright statement in `Mathlib.Init`.
 -/
_private.Mathlib.Tactic.Linter.Header.0.Mathlib.Linter.Style.header.headerLinter : Lean.Linter
-- Mathlib.GroupTheory.Index
AddMonoidHom.card_fiber_eq_of_mem_range : ∀ {G : Type u_1} {M : Type u_2} {F : Type u_3} [inst : AddGroup G] [inst_1 : Fintype G] [inst_2 : AddMonoid M]
  [inst_3 : DecidableEq M] [inst_4 : FunLike F G M] [AddMonoidHomClass F G M] (f : F) {x y : M},
  x ∈ Set.range ⇑f → y ∈ Set.range ⇑f → {g | f g = x}.card = {g | f g = y}.card
-- Mathlib.Analysis.Calculus.FormalMultilinearSeries
ContinuousLinearMap.compFormalMultilinearSeries_apply' : ∀ {𝕜 : Type u} {E : Type v} {F : Type w} {G : Type x} [inst : Semiring 𝕜] [inst_1 : AddCommMonoid E]
  [inst_2 : Module 𝕜 E] [inst_3 : TopologicalSpace E] [inst_4 : ContinuousAdd E] [inst_5 : ContinuousConstSMul 𝕜 E]
  [inst_6 : AddCommMonoid F] [inst_7 : Module 𝕜 F] [inst_8 : TopologicalSpace F] [inst_9 : ContinuousAdd F]
  [inst_10 : ContinuousConstSMul 𝕜 F] [inst_11 : AddCommMonoid G] [inst_12 : Module 𝕜 G] [inst_13 : TopologicalSpace G]
  [inst_14 : ContinuousAdd G] [inst_15 : ContinuousConstSMul 𝕜 G] (f : F →L[𝕜] G) (p : FormalMultilinearSeries 𝕜 E F)
  (n : ℕ) (v : Fin n → E), (f.compFormalMultilinearSeries p n) v = f ((p n) v)
-- Init.Internal.Order.Lemmas
Lean.Order.Array.monotone_array_filterMapM : ∀ {m : Type u → Type v} [inst : Monad m] [inst_1 : (α : Type u) → Lean.Order.PartialOrder (m α)] [Lean.Order.MonoBind m]
  {α β : Type u} {γ : Type w} [inst_3 : Lean.Order.PartialOrder γ] (f : γ → α → m (Option β)) (xs : Array α),
  Lean.Order.monotone f → Lean.Order.monotone fun x => Array.filterMapM (f x) xs
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.norm_cbmApplyMeasure_le : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] (μ : MeasureTheory.VectorMeasure X F) (B : E →L[ℝ] F →L[ℝ] G) (s : Set X),
  ‖MeasureTheory.cbmApplyMeasure μ B s‖ ≤ ‖B‖ * ‖μ s‖
-- Init.Data.Char.Basic
/-- Returns `true` if the character is a space `(' ', U+0020)`, a tab `('\t', U+0009)`, a carriage
return `('\r', U+000D)`, or a newline `('\n', U+000A)`.
 -/
Char.isWhitespace : Char → Bool
-- Mathlib.Tactic.Linter.TextBased
/-- Lint on any occurrences of the string "Adaptation note:" or variants thereof.  -/
_private.Mathlib.Tactic.Linter.TextBased.0.Mathlib.Linter.TextBased.adaptationNoteLinter : Mathlib.Linter.TextBased.TextbasedLinter✝
-- Init.Data.SInt.Lemmas
ISize.ofIntLE.eq_1 : ∀ (i : ℤ) (_hl : ISize.minValue.toInt ≤ i) (_hr : i ≤ ISize.maxValue.toInt), ISize.ofIntLE i _hl _hr = ISize.ofInt i
-- Mathlib.GroupTheory.GroupAction.Hom
DistribMulActionHom.instZeroId.eq_1 : ∀ {M : Type u_1} [inst : Monoid M] {A : Type u_4} [inst_1 : AddMonoid A] [inst_2 : DistribMulAction M A],
  DistribMulActionHom.instZeroId = { one := DistribMulActionHom.id M }
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
/-- A linearly ordered commutative group with a zero element.  -/
LinearOrderedCommGroupWithZero : Type u_3 → Type u_3
-- Mathlib.Algebra.Star.MonoidHom
StarMulEquiv.mk : {A : Type u_6} →
  {B : Type u_7} →
    [inst : Mul A] →
      [inst_1 : Mul B] →
        [inst_2 : Star A] →
          [inst_3 : Star B] →
            (toMulEquiv : A ≃* B) → (∀ (a : A), toMulEquiv.toFun (star a) = star (toMulEquiv.toFun a)) → A ≃⋆* B
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
/-- The order on `WithZero α`, defined by `⊥ < ↑a` and `a < b → ↑a < ↑b`.  -/
WithZero.instLT : {α : Type u_1} → [LT α] → LT (WithZero α)
-- Lean.Elab.Do.Legacy
_private.Lean.Elab.Do.Legacy.0.Lean.Elab.Term.Do.varSetToArray : Lean.Elab.Term.Do.VarSet → Array Lean.Elab.Term.Do.Var
-- Mathlib.Combinatorics.Enumerative.Schroder
Nat.largeSchroder_zero : Nat.largeSchroder 0 = 1
-- Std.Sat.AIG.RelabelNat
/-- Insert a `Decl.atom` into the `State` structure.
 -/
Std.Sat.AIG.RelabelNat.State.addAtom : {α : Type} →
  [inst : DecidableEq α] →
    [inst_1 : Hashable α] →
      {idx : ℕ} →
        {decls : Array (Std.Sat.AIG.Decl α)} →
          {hidx : idx < decls.size} →
            Std.Sat.AIG.RelabelNat.State α decls idx →
              (a : α) → decls[idx] = Std.Sat.AIG.Decl.atom a → Std.Sat.AIG.RelabelNat.State α decls (idx + 1)
-- Mathlib.RingTheory.AdicCompletion.Completeness
MvPowerSeries.toAdicCompletionAlgEquiv.congr_simp : ∀ (σ : Type u_3) (R : Type u_4) [inst : Finite σ] [inst_1 : CommRing R],
  MvPowerSeries.toAdicCompletionAlgEquiv σ R = MvPowerSeries.toAdicCompletionAlgEquiv σ R
-- Mathlib.Topology.LocallyFinsupp
Function.locallyFinsuppWithin.instAddCommMonoid : {X : Type u_1} →
  [inst : TopologicalSpace X] →
    {U : Set X} → {Y : Type u_2} → [inst_1 : AddCommMonoid Y] → AddCommMonoid (Function.locallyFinsuppWithin U Y)
-- Mathlib.CategoryTheory.Sigma.Basic
CategoryTheory.Sigma.SigmaHom.mk : {I : Type w₁} →
  {C : I → Type u₁} →
    [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] →
      {i : I} → {X Y : C i} → (X ⟶ Y) → CategoryTheory.Sigma.SigmaHom ⟨i, X⟩ ⟨i, Y⟩
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.instIsFiniteMeasureVariationContinuousLinearMapRealIdTranspose : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] (μ : MeasureTheory.VectorMeasure X F) (B : E →L[ℝ] F →L[ℝ] G)
  [MeasureTheory.IsFiniteMeasure μ.variation], MeasureTheory.IsFiniteMeasure (μ.transpose B).variation
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_def_of_pos : ∀ {x : ℝ}, 0 < x → ∀ (y : ℝ), x ^ y = Real.exp (Real.log x * y)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.get_union_of_mem_right : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} (mem : k ∈ m₂), (m₁ ∪ m₂).get k ⋯ = m₂.get k mem
-- Mathlib.Analysis.InnerProductSpace.Rayleigh
/-- For a self-adjoint operator `T`, a minimum of the Rayleigh quotient of `T` on a sphere centred
at the origin is an eigenvector of `T`, with eigenvalue the global infimum of the Rayleigh
quotient.  -/
IsSelfAdjoint.hasEigenvector_of_isMinOn : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : CompleteSpace E] {T : E →L[𝕜] E},
  IsSelfAdjoint T →
    ∀ {x₀ : E},
      x₀ ≠ 0 →
        IsMinOn T.reApplyInnerSelf (Metric.sphere 0 ‖x₀‖) x₀ →
          Module.End.HasEigenvector (↑T) (↑(⨅ x, T.rayleighQuotient ↑x)) x₀
-- Init.Control.Id
Id.instOfNat : {α : Type u_1} → {n : ℕ} → [OfNat α n] → OfNat (Id α) n
-- Mathlib.CategoryTheory.Monoidal.Functor
/-- the cotensorator of an oplax monoidal functor  -/
CategoryTheory.Functor.OplaxMonoidal.δ : {C : Type u₁} →
  {inst : CategoryTheory.Category.{v₁, u₁} C} →
    {inst_1 : CategoryTheory.MonoidalCategory C} →
      {D : Type u₂} →
        {inst_2 : CategoryTheory.Category.{v₂, u₂} D} →
          {inst_3 : CategoryTheory.MonoidalCategory D} →
            (F : CategoryTheory.Functor C D) →
              [self : F.OplaxMonoidal] →
                (X Y : C) →
                  F.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) ⟶
                    CategoryTheory.MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y)
-- Mathlib.Algebra.Notation.Indicator
Set.indicator_zero_preimage : ∀ {α : Type u_1} {M : Type u_3} [inst : Zero M] {t : Set α} (s : Set M), t.indicator 0 ⁻¹' s ∈ {Set.univ, ∅}
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.ext_iff : ∀ {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂}
  {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} {e e' : M ≃ₛₗ[σ] M₂},
  e = e' ↔ ∀ (x : M), e x = e' x
-- Mathlib.Algebra.Regular.Prod
Prod.isAddLeftRegular_mk : ∀ {R : Type u_2} {S : Type u_3} [inst : Add R] [inst_1 : Add S] {a : R} {b : S},
  IsAddLeftRegular (a, b) ↔ IsAddLeftRegular a ∧ IsAddLeftRegular b
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get!_inter_of_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited β],
  m₁.WF → m₂.WF → ∀ {k : α}, k ∈ m₂ → Std.DHashMap.Raw.Const.get! (m₁ ∩ m₂) k = Std.DHashMap.Raw.Const.get! m₁ k
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.image_nsmul_of_ne_zero : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddMonoid α] [inst_1 : AddMonoid β] [inst_2 : FunLike F α β]
  [AddHomClass F α β] {n : ℕ}, n ≠ 0 → ∀ (f : F) (s : Set α), ⇑f '' (n • s) = n • ⇑f '' s
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
CategoryTheory.Lax.StrongTrans.toLax_naturality : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.LaxFunctor B C} (η : CategoryTheory.Lax.StrongTrans F G) {a b : B} (f : a ⟶ b),
  η.toLax.naturality f = (η.naturality f).hom
-- Mathlib.Order.Closure
ClosureOperator.closure_isGLB : ∀ {α : Type u_1} [inst : Preorder α] {c : ClosureOperator α} (x : α), IsGLB {y | x ≤ y ∧ c.IsClosed y} (c x)
-- Init.Data.UInt.Lemmas
UInt32.toBitVec_add : ∀ {a b : UInt32}, (a + b).toBitVec = a.toBitVec + b.toBitVec
-- Lean.Parser.Types
Lean.Parser.adaptCacheableContext : (Lean.Parser.CacheableParserContext → Lean.Parser.CacheableParserContext) → Lean.Parser.Parser → Lean.Parser.Parser
-- Mathlib.Algebra.BigOperators.Ring.Multiset
Multiset.prod_map_sum : ∀ {R : Type u_4} [inst : CommSemiring R] {s : Multiset (Multiset R)},
  (Multiset.map Multiset.sum s).prod = (Multiset.map Multiset.prod s.Sections).sum
-- Lean.Widget.InteractiveGoal
Lean.Widget.InteractiveGoal.mk.sizeOf_spec : ∀ (toInteractiveGoalCore : Lean.Widget.InteractiveGoalCore) (userName? : Option String) (goalPrefix : String)
  (mvarId : Lean.MVarId) (isInserted? isRemoved? : Option Bool),
  sizeOf
      { toInteractiveGoalCore := toInteractiveGoalCore, userName? := userName?, goalPrefix := goalPrefix,
        mvarId := mvarId, isInserted? := isInserted?, isRemoved? := isRemoved? } =
    1 + sizeOf toInteractiveGoalCore + sizeOf userName? + sizeOf goalPrefix + sizeOf mvarId + sizeOf isInserted? +
      sizeOf isRemoved?
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.zeroLocus_def : ∀ (X : AlgebraicGeometry.Scheme) {U : X.Opens} (s : Set ↑(X.presheaf.obj (Opposite.op U))),
  X.zeroLocus s = ⋂ f ∈ s, (X.basicOpen f).carrierᶜ
-- Lean.Elab.DefView
Lean.Elab.instToSnapshotTreeBodyProcessedSnapshot : Lean.Language.ToSnapshotTree Lean.Elab.BodyProcessedSnapshot
-- Mathlib.Analysis.Matrix.Spectrum
/-- The eigenvalues of a Hermitian matrix `A` are all zero iff `A = 0`.  -/
Matrix.IsHermitian.eigenvalues_eq_zero_iff : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {n : Type u_2} [inst_1 : Fintype n] {A : Matrix n n 𝕜} [inst_2 : DecidableEq n]
  (hA : A.IsHermitian), hA.eigenvalues = 0 ↔ A = 0
-- Mathlib.Geometry.Manifold.ContMDiff.Constructions
contMDiffAt_fst : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_8} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {G : Type u_9} [inst_8 : TopologicalSpace G] {J : ModelWithCorners 𝕜 F G} {N : Type u_10}
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} {p : M × N},
  ContMDiffAt (I.prod J) I n Prod.fst p
-- Init.Data.UInt.IntToBitVec
USize.toBitVec64_ofNat : ∀ (n : ℕ) (h : System.Platform.numBits = 64), (OfNat.ofNat n).toBitVec64 h = BitVec.ofNat 64 n
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
/-- `LinearIndepOn.pair_iff` is a version that works over arbitrary rings.  -/
linearIndepOn_pair_iff : ∀ {ι : Type u'} {K : Type u_3} {V : Type u} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  {i j : ι} (v : ι → V), i ≠ j → v i ≠ 0 → (LinearIndepOn K v {i, j} ↔ ∀ (c : K), c • v i ≠ v j)
-- Lean.Meta.Tactic.Simp.Arith.Nat.Basic
Lean.Meta.Simp.Arith.Nat.toLinearCnstr? : Lean.Expr → Lean.MetaM (Option (Lean.Meta.Simp.Arith.Nat.LinearCnstr × Array Lean.Expr))
-- Mathlib.Topology.Algebra.MulAction
Continuous.fun_vadd : ∀ {M : Type u_1} {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace X]
  [inst_2 : TopologicalSpace Y] [inst_3 : VAdd M X] [ContinuousVAdd M X] {f : Y → M} {g : Y → X},
  Continuous f → Continuous g → Continuous fun i => f i +ᵥ g i
-- Mathlib.RingTheory.RingHom.StandardSmooth
/-- Every standard smooth homomorphism `R → S` factors into `R -> R[X₁,...,Xₙ] → S`
where `n` is the relative dimension and `R[X₁,...,Xₙ] → S` is etale.  -/
Algebra.IsStandardSmoothOfRelativeDimension.exists_etale_mvPolynomial : ∀ (n : ℕ) (R : Type u) (S : Type v) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.IsStandardSmoothOfRelativeDimension n R S], ∃ g, g.Etale
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.op_L₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C), S.op.L₃ = S.L₀.op
-- Mathlib.Algebra.Homology.DifferentialObject
HomologicalComplex.dgoEquivHomologicalComplexUnitIso_inv_app_f : ∀ {β : Type u_1} [inst : AddCommGroup β] (b : β) (V : Type u_2) [inst_1 : CategoryTheory.Category.{v_1, u_2} V]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms V]
  (X : CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V)) (i : β),
  ((HomologicalComplex.dgoEquivHomologicalComplexUnitIso b V).inv.app X).f i =
    CategoryTheory.CategoryStruct.id (X.obj i)
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.ite_le_natDegree_coeff : ∀ {R : Type u} [inst : Semiring R] (p : Polynomial R) (n : ℕ) (I : Decidable (n < 1 + p.natDegree)),
  (if n < 1 + p.natDegree then p.coeff n else 0) = p.coeff n
-- Mathlib.Algebra.Ring.Defs
mul_neg : ∀ {α : Type u} [inst : Mul α] [inst_1 : HasDistribNeg α] (a b : α), a * -b = -(a * b)
-- Mathlib.RingTheory.Regular.RegularSequence
IsLocalRing.isWeaklyRegular_of_perm_of_subset_maximalIdeal : ∀ {R : Type u_1} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : IsLocalRing R] [IsNoetherian R M] {rs rs' : List R},
  RingTheory.Sequence.IsWeaklyRegular M rs →
    rs.Perm rs' → (∀ r ∈ rs, r ∈ IsLocalRing.maximalIdeal R) → RingTheory.Sequence.IsWeaklyRegular M rs'
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.eq_one_of_pos_of_logb_eq_zero : ∀ {b x : ℝ}, 1 < b → 0 < x → Real.logb b x = 0 → x = 1
-- Mathlib.Order.Max
/-- **Alias** of `not_isMax_of_lt`. -/
LT.lt.not_isMax : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a < b → ¬IsMax a
-- Mathlib.Topology.MetricSpace.Pseudo.Lemmas
/-- If `u` is a neighborhood of `x`, then for small enough `r`, the closed ball
`Metric.closedBall x r` is contained in `u`.  -/
eventually_closedBall_subset : ∀ {α : Type u_2} [inst : PseudoMetricSpace α] {x : α} {u : Set α},
  u ∈ nhds x → ∀ᶠ (r : ℝ) in nhds 0, Metric.closedBall x r ⊆ u
-- Batteries.Tactic.GeneralizeProofs
/-- The tactic configuration.  -/
Batteries.Tactic.GeneralizeProofs.AContext.config : Batteries.Tactic.GeneralizeProofs.AContext → Batteries.Tactic.GeneralizeProofs.Config
-- Init.Data.String.Basic
String.Slice.Pos.ofSliceFrom_startPos : ∀ {s : String.Slice} {pos : s.Pos}, String.Slice.Pos.ofSliceFrom (s.sliceFrom pos).startPos = pos