mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Star.Subalgebra
NonUnitalStarAlgebra.adjoin_le_starAlgebra_adjoin : ∀ (R : Type u_1) {A : Type u_2} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : StarRing A] [inst_4 : Algebra R A] [inst_5 : StarModule R A] (s : Set A),
  NonUnitalStarAlgebra.adjoin R s ≤ (StarAlgebra.adjoin R s).toNonUnitalStarSubalgebra
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.replace.match_1.splitter : {α : Type u_1} →
  (motive : List α → α → α → Sort u_2) →
    (x : List α) →
      (x_1 x_2 : α) →
        ((x x_3 : α) → motive [] x x_3) →
          ((a : α) → (as : List α) → (b c : α) → motive (a :: as) b c) → motive x x_1 x_2
-- Mathlib.Data.EReal.Operations
EReal.mul_neg_iff : ∀ {a b : EReal}, a * b < 0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.instHashableArg.hash : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.Arg pu → UInt64
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
AffineSubspace.instCanLiftSubmoduleToAffineSubspaceMemOfNat : ∀ {k : Type u_1} {V : Type u_2} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V],
  CanLift (AffineSubspace k V) (Submodule k V) (fun x => ↑x) fun x => 0 ∈ x
-- Mathlib.Probability.Process.Stopping
/-- Given a map `u : ι → Ω → E`, its stopped value with respect to the stopping
time `τ` is the map `x ↦ u (τ ω) ω`.  -/
MeasureTheory.stoppedValue : {Ω : Type u_1} → {β : Type u_2} → {ι : Type u_3} → [Nonempty ι] → (ι → Ω → β) → (Ω → WithTop ι) → Ω → β
-- Std.Time.Notation
_private.Std.Time.Notation.0.Std.Time.convertText : Std.Time.Text → Lean.MacroM (Lean.TSyntax `term)
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
NumberField.InfinitePlace.ext_iff : ∀ {K : Type u_1} [inst : Field K] {v₁ v₂ : NumberField.InfinitePlace K}, v₁ = v₂ ↔ ∀ (k : K), v₁ k = v₂ k
-- Mathlib.Data.Complex.BigOperators
Complex.im_sum : ∀ {α : Type u_1} (s : Finset α) (f : α → ℂ), (∑ i ∈ s, f i).im = ∑ i ∈ s, (f i).im
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Function.Bijective.prod_comp : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [inst : Fintype ι] [inst_1 : Fintype κ] [inst_2 : CommMonoid M]
  {e : ι → κ}, Function.Bijective e → ∀ (g : κ → M), ∏ i, g (e i) = ∏ i, g i
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.Path.listL.match_1.splitter : {α : Type u_1} →
  (motive : RBTree.RBNode.Path α → Sort u_2) →
    (x : RBTree.RBNode.Path α) →
      (Unit → motive RBTree.RBNode.Path.root) →
        ((c : RBTree.RBColor) →
            (parent : RBTree.RBNode.Path α) →
              (v : α) → (r : RBTree.RBNode α) → motive (RBTree.RBNode.Path.left c parent v r)) →
          ((c : RBTree.RBColor) →
              (l : RBTree.RBNode α) →
                (v : α) → (parent : RBTree.RBNode.Path α) → motive (RBTree.RBNode.Path.right c l v parent)) →
            motive x
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.add_contLinear : ∀ {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] [inst_8 : IsTopologicalAddGroup W] [inst_9 : TopologicalSpace V]
  [inst_10 : IsTopologicalAddTorsor P] (f g : P →ᴬ[R] W), (f + g).contLinear = f.contLinear + g.contLinear
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.hom_ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {T X Y : C} (f g : T ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj X Y),
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.SemiCartesianMonoidalCategory.fst X Y) =
      CategoryTheory.CategoryStruct.comp g (CategoryTheory.SemiCartesianMonoidalCategory.fst X Y) →
    CategoryTheory.CategoryStruct.comp f (CategoryTheory.SemiCartesianMonoidalCategory.snd X Y) =
        CategoryTheory.CategoryStruct.comp g (CategoryTheory.SemiCartesianMonoidalCategory.snd X Y) →
      f = g
-- Mathlib.Algebra.Group.Subgroup.Actions
Subgroup.smulCommClass_left : ∀ {G : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Group G] [inst_1 : MulAction G β] [inst_2 : SMul α β]
  [SMulCommClass G α β] (S : Subgroup G), SMulCommClass (↥S) α β
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.or_assoc : ∀ {σs : List (Type u)} {P Q R : Std.Do.SPred σs}, (P ∨ Q) ∨ R ⊣⊢ₛ P ∨ Q ∨ R
-- Mathlib.Computability.Partrec
Computable.id : ∀ {α : Type u_1} [inst : Primcodable α], Computable id
-- Mathlib.MeasureTheory.Group.Arithmetic
Subgroup.instMeasurableConstSMul : ∀ {G : Type u_2} {α : Type u_3} [inst : MeasurableSpace α] [inst_1 : Group G] [inst_2 : MulAction G α]
  [MeasurableConstSMul G α] (s : Subgroup G), MeasurableConstSMul (↥s) α
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
/-- Given maps `f`, `g` from a manifold into a field `𝕜` and `𝕜`-vector space `V`, respectively, the
formula for the `mfderiv` (differential) of their scalar multiplication `f • g`.

Mathematically speaking the formula is `d(f • g) = f • dg + df ⊗ g`, but to get it to typecheck
we need a phrasing involving the canonical identification `NormedSpace.fromTangentSpace` between
the vector space `V` and the tangent space to this vector space at any point. This is because two
different tangent spaces (at `(f • g) x` and `g x`) appear in the equation.

This is a defeq variant of the main lemma `fromTangentSpace_mfderiv_smul`, in which we work in the
tangent space at `f x • g x` (the simp-normal form) rather than at `(f • g) x`.  -/
_private.Mathlib.Geometry.Manifold.MFDeriv.NormedSpace.0.fromTangentSpace_mfderiv_smul' : ∀ {𝕜 : 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] {x : M} {V : Type u_18} [inst_6 : NormedAddCommGroup V]
  [inst_7 : NormedSpace 𝕜 V] {f : M → 𝕜} {g : M → V},
  MDiffAt f x →
    MDiffAt g x →
      ↑(NormedSpace.fromTangentSpace (f x • g x)) ∘SL mfderiv% (f • g) x =
        f x • ↑(NormedSpace.fromTangentSpace (g x)) ∘SL mfderiv% g x +
          ContinuousLinearMap.toSpanSingleton 𝕜 (g x) ∘SL ↑(NormedSpace.fromTangentSpace (f x)) ∘SL mfderiv% f x
-- Std.Do.WP.Basic
/-- Interpret a monadic program `x : m α` in terms of a predicate transformer `PredTrans ps α`.  -/
Std.Do.WP.wp : {m : Type u → Type v} →
  {ps : outParam Std.Do.PostShape} → [self : Std.Do.WP m ps] → {α : Type u} → m α → Std.Do.PredTrans ps α
-- Mathlib.Algebra.Category.Ring.Limits
CommRingCat.commRingObj : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J CommRingCat) → (j : J) → CommRing ((F.comp (CategoryTheory.forget CommRingCat)).obj j)
-- Mathlib.CategoryTheory.MorphismProperty.RetractArgument
/-- If `i ≫ p = f`, and `f` has the left lifting property with respect to `p`,
then `f` is a retract of `i`.  -/
CategoryTheory.RetractArrow.ofLeftLiftingProperty : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X Y Z : C} →
      {f : X ⟶ Z} →
        {i : X ⟶ Y} →
          {p : Y ⟶ Z} →
            CategoryTheory.CategoryStruct.comp i p = f →
              [CategoryTheory.HasLiftingProperty f p] → CategoryTheory.RetractArrow f i
-- Mathlib.Algebra.Group.TransferInstance
/-- Transfer `AddMonoid` across an `Equiv`  -/
Equiv.addMonoid : {α : Type u_2} → {β : Type u_3} → α ≃ β → [AddMonoid β] → AddMonoid α
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.maxKey!_modify : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] [inst_1 : Inhabited α] {k : α} {f : β k → β k}, (t.modify k f).maxKey! = t.maxKey!
-- Mathlib.Analysis.SpecialFunctions.Exponential
/-- The exponential map in a complete normed field `𝕂` of characteristic zero has strict derivative
`NormedSpace.exp x` at any point `x` in the disk of convergence.  -/
hasStrictDerivAt_exp_of_mem_ball : ∀ {𝕂 : Type u_1} [inst : NontriviallyNormedField 𝕂] [CompleteSpace 𝕂] [CharZero 𝕂] {x : 𝕂},
  x ∈ Metric.eball 0 (NormedSpace.expSeries 𝕂 𝕂).radius → HasStrictDerivAt NormedSpace.exp (NormedSpace.exp x) x
-- Mathlib.Algebra.BigOperators.Finprod
finprod_mem_inv_distrib : ∀ {α : Type u_1} {G : Type u_4} {s : Set α} [inst : DivisionCommMonoid G] (f : α → G),
  s.Finite → ∏ᶠ (x : α) (_ : x ∈ s), (f x)⁻¹ = (∏ᶠ (x : α) (_ : x ∈ s), f x)⁻¹
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.insertMany_cons : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} {l : List ((a : α) × β a)} {k : α}
  {v : β k}, m.insertMany (⟨k, v⟩ :: l) = (m.insert k v).insertMany l
-- Mathlib.Data.Finset.NAry
/-- If a `Finset` is a subset of the image of two `Set`s under a binary operation,
then it is a subset of the `Finset.image₂` of two `Finset` subsets of these `Set`s.  -/
Finset.subset_set_image₂ : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {f : α → β → γ} {u : Finset γ} {s : Set α}
  {t : Set β}, ↑u ⊆ Set.image2 f s t → ∃ s' t', ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ u ⊆ Finset.image₂ f s' t'
-- Mathlib.Analysis.Analytic.Order
/-- The order of an analytic function `f` at `z₀` equals a natural number `n` iff `f` can locally
be written as `f z = (z - z₀) ^ n • g z`, where `g` is analytic and does not vanish at `z₀`.  -/
AnalyticAt.analyticOrderNatAt_eq_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {z₀ : 𝕜},
  AnalyticAt 𝕜 f z₀ →
    analyticOrderAt f z₀ ≠ ⊤ →
      ∀ {n : ℕ},
        analyticOrderNatAt f z₀ = n ↔
          ∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in nhds z₀, f z = (z - z₀) ^ n • g z
-- Mathlib.Topology.EMetricSpace.Weak
ENNReal.edist_eq_top_iff : ∀ (a b : ENNReal), edist a b = ⊤ ↔ a ≠ b ∧ (a = ⊤ ∨ b = ⊤)
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.iCyclesIso_inv_hom_id_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i j : ι) (hj : c.next i = j) (h : K.d i j = 0)
  [inst_2 : K.HasHomology i] {Z : C} (h_1 : K.X i ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.iCyclesIso i j hj h).inv
      (CategoryTheory.CategoryStruct.comp (K.iCycles i) h_1) =
    h_1
-- Mathlib.Algebra.Category.Ring.FilteredColimits
/-- The bundled semiring giving the filtered colimit of a diagram.  -/
SemiRingCat.FilteredColimits.colimit : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    CategoryTheory.Functor J SemiRingCat → [CategoryTheory.IsFiltered J] → SemiRingCat
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
/-- The "characteristic matrix" of `M : Matrix n n R` is the matrix of polynomials $t I - M$.
The determinant of this matrix is the characteristic polynomial.
 -/
Matrix.charmatrix : {R : Type u_1} →
  [inst : CommRing R] → {n : Type u_4} → [DecidableEq n] → [Fintype n] → Matrix n n R → Matrix n n (Polynomial R)
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
MeasureTheory.eLpNorm_one_condExp_le_eLpNorm : ∀ {α : Type u_1} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_2} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [CompleteSpace E] (f : α → E),
  MeasureTheory.eLpNorm μ[f | m] 1 μ ≤ MeasureTheory.eLpNorm f 1 μ
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.volume_preserving_pi : ∀ {ι : Type u_1} [inst : Fintype ι] {α' : ι → Type u_4} {β' : ι → Type u_5}
  [inst_1 : (i : ι) → MeasureTheory.MeasureSpace (α' i)] [inst_2 : (i : ι) → MeasureTheory.MeasureSpace (β' i)]
  [∀ (i : ι), MeasureTheory.SigmaFinite MeasureTheory.volume] {f : (i : ι) → α' i → β' i},
  (∀ (i : ι), MeasureTheory.MeasurePreserving (f i) MeasureTheory.volume MeasureTheory.volume) →
    MeasureTheory.MeasurePreserving (fun a i => f i (a i)) MeasureTheory.volume MeasureTheory.volume
-- Mathlib.Order.Hom.WithTopBot
LatticeHom.withTopWithBot_id : ∀ {α : Type u_1} [inst : Lattice α], (LatticeHom.id α).withTopWithBot = BoundedLatticeHom.id (WithTop (WithBot α))
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
MeasureTheory.condExpIndL1_of_measurableSet_of_measure_ne_top : ∀ {α : Type u_1} {G : Type u_4} [inst : NormedAddCommGroup G] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {s : Set α} [inst_1 : NormedSpace ℝ G] {hm : m ≤ m0} [inst_2 : MeasureTheory.SigmaFinite (μ.trim hm)]
  (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (x : G),
  MeasureTheory.condExpIndL1 hm μ s x = MeasureTheory.condExpIndL1Fin hm hs hμs x
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey_erase_eq_of_not_compare_eq_minKey : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  (h : t.WF) {k : α} {he : (Std.DTreeMap.Internal.Impl.erase k t ⋯).impl.isEmpty = false},
  ¬compare k (t.minKey ⋯) = Ordering.eq → (Std.DTreeMap.Internal.Impl.erase k t ⋯).impl.minKey he = t.minKey ⋯
-- ProofWidgets.Component.PenroseDiagram
/-- Displays the given diagram using [Penrose](https://penrose.cs.cmu.edu/).
The website contains explanations of how to write domain (`dsl`), style (`sty`),
and substance (`sub`) programs.

The diagram may also contain embedded HTML trees which are specified in `embeds`.
Each embed is HTML together with the name of an object `x` in the substance program.
The object `x` can be of any type but *must* be assigned an `x.textBox : Rectangle` field
in the style program.
This rectangle will be replaced with the HTML tree.
Its dimensions will be overridden in the style program
to match those of the HTML node.

The following additional constants are prepended to the style program:
```penrose
theme {
  color foreground
  color tooltipBackground
  color tooltipForeground
  color tooltipBorder
}
```
and can be accessed as, for example, `theme.foreground` in the provided `sty` in order to match
the editor theme.  -/
ProofWidgets.Penrose.Diagram : ProofWidgets.Component ProofWidgets.Penrose.DiagramProps
-- Mathlib.Combinatorics.Additive.CauchyDavenport
/-- The **Cauchy-Davenport theorem** for linearly ordered additive cancellative semigroups. The
size of `s + t` is lower-bounded by `|s| + |t| - 1`.  -/
cauchy_davenport_add_of_linearOrder_isCancelAdd : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : Add α] [IsCancelAdd α] [AddLeftMono α] [AddRightMono α]
  {s t : Finset α}, s.Nonempty → t.Nonempty → s.card + t.card - 1 ≤ (s + t).card
-- Mathlib.LinearAlgebra.Projection
LinearMap.IsProj.eq_conj_prodMap : ∀ {R : Type u_1} [inst : CommRing R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {p : Submodule R E}
  {f : E →ₗ[R] E} (h : LinearMap.IsProj p f), f = (p.prodEquivOfIsCompl f.ker ⋯).conj (LinearMap.id.prodMap 0)
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey?_beq : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α}, Option.all (fun x_2 => x_2 == k) (m.getKey? k) = true
-- Mathlib.Analysis.Normed.Group.Constructions
/-- Multiplicative version of `Prod.nnnorm_mk`.  -/
Prod.nnnorm_mk' : ∀ {E : Type u_2} {F : Type u_3} [inst : SeminormedGroup E] [inst_1 : SeminormedGroup F] (x : E) (y : F),
  ‖(x, y)‖₊ = max ‖x‖₊ ‖y‖₊
-- Init.Core
not_false_iff : ¬False ↔ True
-- Mathlib.CategoryTheory.Galois.Prorepresentability
CategoryTheory.PreGaloisCategory.PointedGaloisObject.hom_ext : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.GaloisCategory C]
  {F : CategoryTheory.Functor C FintypeCat} {A B : CategoryTheory.PreGaloisCategory.PointedGaloisObject F}
  {f g : A ⟶ B}, f.val = g.val → f = g
-- Mathlib.Combinatorics.Matroid.Minor.Contract
Matroid.IsBasis.contract_isBasis_sdiff_sdiff_of_subset : ∀ {α : Type u_1} {M : Matroid α} {I J X : Set α}, M.IsBasis I X → J ⊆ I → (M.contract J).IsBasis (I \ J) (X \ J)
-- Mathlib.Topology.Order.LowerUpperTopology
Topology.IsLower.lowerBasis.eq_1 : ∀ (α : Type u_3) [inst : Preorder α], Topology.IsLower.lowerBasis α = {s | ∃ t, t.Finite ∧ (↑(upperClosure t))ᶜ = s}
-- Mathlib.Data.Nat.Digits.Defs
Nat.digits_inj_iff : ∀ {b n m : ℕ}, b.digits n = b.digits m ↔ n = m
-- Mathlib.Algebra.Field.Defs
Field.toInv : {K : Type u} → [self : Field K] → Inv K
-- Mathlib.Geometry.Manifold.VectorField.LieBracket
/-- The Lie bracket of two vector fields in a manifold.  -/
VectorField.mlieBracket : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {H : Type u_2} →
      [inst_1 : TopologicalSpace H] →
        {E : Type u_3} →
          [inst_2 : NormedAddCommGroup E] →
            [inst_3 : NormedSpace 𝕜 E] →
              (I : ModelWithCorners 𝕜 E H) →
                {M : Type u_4} →
                  [inst_4 : TopologicalSpace M] →
                    [inst_5 : ChartedSpace H M] →
                      ((x : M) → TangentSpace I x) → ((x : M) → TangentSpace I x) → (x₀ : M) → TangentSpace I x₀
-- Mathlib.Topology.Compactness.SigmaCompact
/-- A closed subset of a σ-compact set is σ-compact.  -/
IsSigmaCompact.of_isClosed_subset : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s t : Set X}, IsSigmaCompact t → IsClosed s → s ⊆ t → IsSigmaCompact s
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
WeierstrassCurve.Jacobian.map_neg : ∀ {R : Type r} {S : Type s} [inst : CommRing R] [inst_1 : CommRing S] {W' : WeierstrassCurve.Jacobian R} (f : R →+* S)
  (P : Fin 3 → R), (W'.map f).neg (⇑f ∘ P) = ⇑f ∘ W'.neg P
-- Lean.Meta.ArgsPacker
/-- The number of functions being packed  -/
Lean.Meta.ArgsPacker.numFuncs : Lean.Meta.ArgsPacker → ℕ
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Complex.iteratedDeriv_odd_sin : ∀ (n : ℕ), iteratedDeriv (2 * n + 1) Complex.sin = (-1) ^ n * Complex.cos
-- Mathlib.Algebra.Order.ToIntervalMod
toIocDiv_sub_ofNat_mul : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedAddMonoid R]
  [inst_3 : Archimedean R] {p : R} (hp : 0 < p) (a b : R) (m : ℕ) [inst_4 : m.AtLeastTwo],
  toIocDiv hp a (b - OfNat.ofNat m * p) = toIocDiv hp a b - OfNat.ofNat m
-- Init.Data.Slice.List.Basic
instSliceableListSliceNat_3 : {α : Type u} → Std.Roc.Sliceable (ListSlice α) ℕ (ListSlice α)
-- Lean.ScopedEnvExtension
Lean.ScopedEnvExtension.State : Type → Type
-- Mathlib.Tactic.Conv
/-- The command `#whnf e` evaluates `e` to Weak Head Normal Form, which means that the "head"
of the expression is reduced to a primitive - a lambda or forall, or an axiom or inductive type.
It is similar to `#reduce e`, but it does not reduce the expression completely,
only until the first constructor is exposed. For example:
```
open Nat List
set_option pp.notation false
#whnf [1, 2, 3].map succ
-- cons (succ 1) (map succ (cons 2 (cons 3 nil)))
#reduce [1, 2, 3].map succ
-- cons 2 (cons 3 (cons 4 nil))
```
The head of this expression is the `List.cons` constructor,
so we can see from this much that the list is not empty,
but the subterms `Nat.succ 1` and `List.map Nat.succ (List.cons 2 (List.cons 3 List.nil))` are
still unevaluated. `#reduce` is equivalent to using `#whnf` on every subexpression.
 -/
Mathlib.Tactic.Conv.«command#whnf_» : Lean.ParserDescr
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- For a functor `F : C ⥤ D` and an object `d : D`, the category of structured arrows `d ⟶ F.obj c`
is contravariantly equivalent to the category of costructured arrows `F.op.obj c ⟶ op d`.
 -/
CategoryTheory.structuredArrowOpEquivalence : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) →
          (d : D) → (CategoryTheory.StructuredArrow d F)ᵒᵖ ≌ CategoryTheory.CostructuredArrow F.op (Opposite.op d)
-- Mathlib.Data.Rat.Defs
Rat.mk'_pow : ∀ (num : ℤ) (den : ℕ) (hd : den ≠ 0) (hdn : num.natAbs.Coprime den) (n : ℕ),
  { num := num, den := den, den_nz := hd, reduced := hdn } ^ n =
    { num := num ^ n, den := den ^ n, den_nz := ⋯, reduced := ⋯ }
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.map_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (P : CategoryTheory.MorphismProperty C) (F : CategoryTheory.Functor C D) {E : Type u_2}
  [inst_2 : CategoryTheory.Category.{v_2, u_2} E] (G : CategoryTheory.Functor D E), (P.map F).map G = P.map (F.comp G)
-- Mathlib.Computability.Partrec
Computable.option_map : ∀ {α : Type u_1} {β : Type u_2} {σ : Type u_4} [inst : Primcodable α] [inst_1 : Primcodable β] [inst_2 : Primcodable σ]
  {f : α → Option β} {g : α → β → σ}, Computable f → Computable₂ g → Computable fun a => Option.map (g a) (f a)
-- Mathlib.Algebra.Algebra.Spectrum.Basic
AlgEquiv.spectrum_eq : ∀ {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : Ring A]
  [inst_2 : Ring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : EquivLike F A B] [AlgEquivClass F R A B]
  (f : F) (a : A), spectrum R (f a) = spectrum R a
-- Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
AlgebraicGeometry.Scheme.AffineZariskiSite.cocone_ι_app : ∀ (X : AlgebraicGeometry.Scheme) (U : X.AffineZariskiSite),
  (AlgebraicGeometry.Scheme.AffineZariskiSite.cocone X).ι.app U = ⋯.fromSpec
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.neg_zero : ∀ {R : Type u_2} [inst : CommRing R], -0 = 0
-- Mathlib.Algebra.GroupWithZero.Action.Defs
/-- Scalar multiplication by the scalar `0` is `0`.  -/
SMulWithZero.zero_smul : ∀ {M₀ : Type u_2} {A : Type u_7} {inst : Zero M₀} {inst_1 : Zero A} [self : SMulWithZero M₀ A] (m : A), 0 • m = 0
-- Mathlib.Topology.UniformSpace.Cauchy
CompleteSpace.mulOpposite : ∀ {α : Type u} [uniformSpace : UniformSpace α] [CompleteSpace α], CompleteSpace αᵐᵒᵖ
-- Mathlib.Algebra.Group.Defs
/-- In a class equipped with instances of both `Monoid` and `Inv`, this definition records what the
default definition for `Div` would be: `a * b⁻¹`.  This is later provided as the default value for
the `Div` instance in `DivInvMonoid`.

We keep it as a separate definition rather than inlining it in `DivInvMonoid` so that the `Div`
field of individual `DivInvMonoid`s constructed using that default value will not be unfolded at
`.instance` transparency.  -/
DivInvMonoid.div' : {G : Type u} → [Monoid G] → [Inv G] → G → G → G
-- Mathlib.Algebra.Group.Equiv.Defs
AddEquiv.symmEquiv_apply_apply : ∀ (P : Type u_9) (Q : Type u_10) [inst : Add P] [inst_1 : Add Q] (h : P ≃+ Q) (a : Q),
  ((AddEquiv.symmEquiv P Q) h) a = h.symm a
-- Mathlib.Algebra.Homology.Embedding.IsSupported
HomologicalComplex.IsStrictlySupported.isZero : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  {inst : CategoryTheory.Category.{v_1, u_3} C} {inst_1 : CategoryTheory.Limits.HasZeroMorphisms C}
  {K : HomologicalComplex C c'} {e : c.Embedding c'} [self : K.IsStrictlySupported e] (i' : ι'),
  (∀ (i : ι), e.f i ≠ i') → CategoryTheory.Limits.IsZero (K.X i')
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy
CategoryTheory.Arrow.LeftHomotopy.ext : ∀ {V : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} V} {inst_1 : CategoryTheory.Preadditive V}
  {u v : CategoryTheory.Arrow V} {f g : u ⟶ v} {x y : CategoryTheory.Arrow.LeftHomotopy f g}, x.hom = y.hom → x = y
-- Batteries.Recycling.RBTree.Basic
RBTree.RBNode.Balanced.below : {α : Type u_1} →
  {motive : (a : RBTree.RBNode α) → (a_1 : RBTree.RBColor) → (a_2 : ℕ) → a.Balanced a_1 a_2 → Prop} →
    {a : RBTree.RBNode α} → {a_1 : RBTree.RBColor} → {a_2 : ℕ} → a.Balanced a_1 a_2 → Prop
-- Std.Data.TreeMap.Slice
Std.TreeMap.instSliceableRccSlice : {α : Type u} →
  {β : Type v} →
    (cmp : autoParam (α → α → Ordering) Std.TreeMap.instSliceableRccSlice._auto_1) →
      Std.Rcc.Sliceable (Std.TreeMap α β cmp) α (Std.DTreeMap.Internal.Const.RccSlice α β)