mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
spinGroup.star_mul_self : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} (x : ↥(spinGroup Q)), star x * x = 1
-- Mathlib.Algebra.BigOperators.Expect
Finset.expect_apply : ∀ {ι : Type u_1} {α : Type u_6} {π : α → Type u_7} [inst : (a : α) → CommSemiring (π a)]
  [inst_1 : (a : α) → Module ℚ≥0 (π a)] (s : Finset ι) (f : ι → (a : α) → π a) (a : α),
  s.expect (fun i => f i) a = s.expect fun i => f i a
-- Lean.Data.PersistentArray
Lean.PersistentArray.get! : {α : Type u} → [Inhabited α] → Lean.PersistentArray α → ℕ → α
-- Mathlib.Algebra.Category.Grp.Ulift
/-- The universe lift functor for additive groups is fully faithful.  -/
AddGrpCat.uliftFunctorFullyFaithful : AddGrpCat.uliftFunctor.FullyFaithful
-- Mathlib.Algebra.Category.ModuleCat.Sheaf
/-- The obvious free sheaf of modules of rank `1`.  -/
SheafOfModules.unit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} → (R : CategoryTheory.Sheaf J RingCat) → SheafOfModules R
-- Aesop.Tree.RunMetaM
Aesop.Rapp.runMetaMInParentState : {m : Type → Type} →
  [Monad m] →
    [MonadLiftT Lean.MetaM m] → [MonadFinally m] → {α : Type} → m α → Aesop.Rapp → m (α × Lean.Meta.SavedState)
-- Mathlib.RingTheory.Polynomial.Pochhammer
ascPochhammer_natDegree : ∀ (S : Type u) [inst : Semiring S] (n : ℕ) [NoZeroDivisors S] [Nontrivial S], (ascPochhammer S n).natDegree = n
-- Mathlib.Order.Hom.Lattice
LatticeHom.id_comp : ∀ {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] (f : LatticeHom α β),
  (LatticeHom.id β).comp f = f
-- Mathlib.Analysis.Calculus.FormalMultilinearSeries
/-- Realize a ContinuousMultilinearMap on `∀ i : ι, E i` as the evaluation of a
FormalMultilinearSeries by choosing an arbitrary identification `ι ≃ Fin (Fintype.card ι)`.  -/
ContinuousMultilinearMap.toFormalMultilinearSeries : {𝕜 : Type u} →
  {F : Type w} →
    [inst : Semiring 𝕜] →
      [inst_1 : AddCommMonoid F] →
        [inst_2 : Module 𝕜 F] →
          [inst_3 : TopologicalSpace F] →
            [inst_4 : ContinuousAdd F] →
              [inst_5 : ContinuousConstSMul 𝕜 F] →
                {ι : Type u_1} →
                  {E : ι → Type u_2} →
                    [inst_6 : (i : ι) → AddCommGroup (E i)] →
                      [inst_7 : (i : ι) → Module 𝕜 (E i)] →
                        [inst_8 : (i : ι) → TopologicalSpace (E i)] →
                          [inst_9 : ∀ (i : ι), IsTopologicalAddGroup (E i)] →
                            [inst_10 : ∀ (i : ι), ContinuousConstSMul 𝕜 (E i)] →
                              [Fintype ι] → ContinuousMultilinearMap 𝕜 E F → FormalMultilinearSeries 𝕜 ((i : ι) → E i) F
-- Mathlib.CategoryTheory.FiberedCategory.BasedCategory
/-- The composition of two based functors.  -/
CategoryTheory.BasedFunctor.comp : {𝒮 : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
    {𝒳 : CategoryTheory.BasedCategory 𝒮} →
      {𝒴 : CategoryTheory.BasedCategory 𝒮} →
        {𝒵 : CategoryTheory.BasedCategory 𝒮} →
          CategoryTheory.BasedFunctor 𝒳 𝒴 → CategoryTheory.BasedFunctor 𝒴 𝒵 → CategoryTheory.BasedFunctor 𝒳 𝒵
-- Lean.Data.Json.Elab
/-- Json true value syntax.  -/
Lean.Json.jsonTrue : Lean.ParserDescr
-- Mathlib.LinearAlgebra.Projectivization.Constructions
Projectivization.orthogonal_cross_left : ∀ {F : Type u_1} [inst : Field F] [inst_1 : DecidableEq F] {v w : Projectivization F (Fin 3 → F)},
  v ≠ w → v.orthogonal (v.cross w)
-- Mathlib.Logic.Embedding.Set
Function.Embedding.image_apply : ∀ {α : Type u_1} {β : Type u_2} (f : α ↪ β) (s : Set α), f.image s = ⇑f '' s
-- Mathlib.Data.Seq.Defs
Stream'.Seq.terminatedAt_zero_iff : ∀ {α : Type u} {s : Stream'.Seq α}, s.TerminatedAt 0 ↔ s = Stream'.Seq.nil
-- Lean.Parser.Extra
Lean.Parser.withCache.formatter : Lean.Name → Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter
-- Mathlib.Analysis.Meromorphic.TrailingCoefficient
/-- Eta-expanded form of `meromorphicTrailingCoeffAt_comp_add_const_eq_meromorphicTrailingCoeffAt`

---

`meromorphicTrailingCoefficientAt` is invariant under translation.  -/
meromorphicTrailingCoeffAt_fun_comp_add_const_eq_meromorphicTrailingCoeffAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {x c : 𝕜},
  meromorphicTrailingCoeffAt (fun x => f (x + c)) x = meromorphicTrailingCoeffAt f (x + c)
-- Mathlib.Topology.CWComplex.Classical.Finite
/-- **Alias** of `Topology.RelCWComplex.FiniteDimensional.eventually_isEmpty_cell`.

---

For some natural number `n`, the type `cell C m` is empty for all `m ≥ n`.  -/
Topology.CWComplex.FiniteDimensional.eventually_isEmpty_cell : ∀ {X : Type u} {inst : TopologicalSpace X} {C D : Set X} {inst_1 : Topology.RelCWComplex C D}
  [self : Topology.RelCWComplex.FiniteDimensional C],
  ∀ᶠ (n : ℕ) in Filter.atTop, IsEmpty (Topology.RelCWComplex.cell C n)
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
SimpleGraph.regularityReduced_edges_card_aux : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {G : SimpleGraph α} [inst_2 : DecidableRel G.Adj]
  {P : Finpartition Finset.univ} {ε : ℝ} [Nonempty α],
  0 < ε →
    P.IsEquipartition →
      P.IsUniform G (ε / 8) →
        4 / ε ≤ ↑P.parts.card →
          2 * (↑G.edgeFinset.card - ↑(SimpleGraph.regularityReduced P G (ε / 8) (ε / 4)).edgeFinset.card) <
            2 * ε * ↑(Fintype.card α ^ 2)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getThenInsertIfNew?_snd : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} {k : α} {v : β},
  (Std.DHashMap.Const.getThenInsertIfNew? m k v).2 = m.insertIfNew k v
-- Mathlib.InformationTheory.Hamming
Hamming.instMetricSpace : {ι : Type u_2} → {β : ι → Type u_3} → [Fintype ι] → [(i : ι) → DecidableEq (β i)] → MetricSpace (Hamming β)
-- Mathlib.Order.Partition.Finpartition
Finpartition.mem_atomise : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α} {F : Finset (Finset α)},
  t ∈ (Finpartition.atomise s F).parts ↔ t.Nonempty ∧ ∃ Q ⊆ F, {i ∈ s | ∀ u ∈ F, u ∈ Q ↔ i ∈ u} = t
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.eval₂_mul_eq_zero_of_left : ∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] {p q : MvPolynomial σ R}
  (f : R →+* S₁) (g : σ → S₁), MvPolynomial.eval₂ f g p = 0 → MvPolynomial.eval₂ f g (p * q) = 0
-- Std.Data.Iterators.Combinators.Monadic.DropWhile
Std.Iterators.Types.DropWhile.instIterator : {α : Type w} →
  {m : Type w → Type w'} →
    {β : Type w} →
      [Monad m] →
        [Std.Iterator α m β] →
          {P : β → Std.Iterators.PostconditionT m (ULift.{w, 0} Bool)} →
            Std.Iterator (Std.Iterators.Types.DropWhile α m β P) m β
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getThenInsertIfNew?_snd : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {v : β}, (t.getThenInsertIfNew? k v).2 = t.insertIfNew k v
-- Mathlib.Data.TypeVec
/-- append an arrow and a function as well as their respective source and target types / typevecs  -/
TypeVec.appendFun : {n : ℕ} →
  {α : TypeVec.{u_1} n} →
    {α' : TypeVec.{u_2} n} → {β : Type u_1} → {β' : Type u_2} → α.Arrow α' → (β → β') → (α ::: β).Arrow (α' ::: β')
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.minKeyD_eq_getD_keysArray : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {fallback : α}, t.minKeyD fallback = t.keysArray.getD 0 fallback
-- Mathlib.GroupTheory.Coset.Card
Subgroup.card_eq_card_quotient_mul_card_subgroup : ∀ {α : Type u_1} [inst : Group α] (s : Subgroup α), Nat.card α = Nat.card (α ⧸ s) * Nat.card ↥s
-- Mathlib.Data.Set.Pairwise.Basic
Set.pairwise_union : ∀ {α : Type u_1} {r : α → α → Prop} {s t : Set α},
  (s ∪ t).Pairwise r ↔ s.Pairwise r ∧ t.Pairwise r ∧ ∀ a ∈ s, ∀ b ∈ t, a ≠ b → r a b ∧ r b a
-- Mathlib.Order.Filter.Finite
Filter.principal_surjective : ∀ {α : Type u} [Finite α], Function.Surjective Filter.principal
-- Mathlib.Analysis.Normed.Group.Uniform
LocallyLipschitzOn.div : ∀ {α : Type u_4} {E : Type u_5} [inst : SeminormedCommGroup E] [inst_1 : PseudoEMetricSpace α] {f g : α → E}
  {s : Set α}, LocallyLipschitzOn s f → LocallyLipschitzOn s g → LocallyLipschitzOn s fun x => f x / g x
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.whiskerLeft_mapId_inv_app_assoc : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {a b : B}
  (f : a ⟶ b) (X : ↑(F.obj a)) {Z : ↑(F.obj b)}
  (h : (F.map (CategoryTheory.CategoryStruct.id b)).toFunctor.obj ((F.map f).toFunctor.obj X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((F.mapId b).inv.toNatTrans.app ((F.map f).toFunctor.obj X)) h =
    CategoryTheory.CategoryStruct.comp ((F.map₂ (CategoryTheory.Bicategory.rightUnitor f).inv).toNatTrans.app X)
      (CategoryTheory.CategoryStruct.comp ((F.mapComp f (CategoryTheory.CategoryStruct.id b)).hom.toNatTrans.app X) h)
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.edgeFinset_ssubset_edgeFinset : ∀ {V : Type u_1} {G₁ G₂ : SimpleGraph V} [inst : Fintype ↑G₁.edgeSet] [inst_1 : Fintype ↑G₂.edgeSet],
  G₁.edgeFinset ⊂ G₂.edgeFinset ↔ G₁ < G₂
-- Mathlib.GroupTheory.OrderOfElement
/-- Elements of finite order are of finite order in submonoids.  -/
AddSubmonoid.isOfFinAddOrder_coe : ∀ {G : Type u_1} [inst : AddMonoid G] {H : AddSubmonoid G} {x : ↥H}, IsOfFinAddOrder ↑x ↔ IsOfFinAddOrder x
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
instIsDiscreteValuationRingSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers : ∀ (A : Type u_1) [inst : CommRing A] [inst_1 : IsDedekindDomain A] (K : Type u_2) [inst_2 : Field K]
  [inst_3 : Algebra A K] [inst_4 : IsFractionRing A K] (v : IsDedekindDomain.HeightOneSpectrum A),
  IsDiscreteValuationRing ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)
-- Mathlib.Combinatorics.Enumerative.Catalan.Tree
_private.Mathlib.Combinatorics.Enumerative.Catalan.Tree.0.BinaryTree.treesOfNumNodesEq.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive n.succ) → motive x
-- Mathlib.Order.Interval.Basic
Interval.dual_bot : ∀ {α : Type u_1} [inst : Preorder α], Interval.dual ⊥ = ⊥
-- Mathlib.Data.Matrix.Block
Matrix.blockDiag_neg : ∀ {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [inst : AddGroup α] (M : Matrix (m × o) (n × o) α),
  (-M).blockDiag = -M.blockDiag
-- Mathlib.Algebra.Order.Ring.WithTop
WithBot.instPosMulMono : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : MulZeroClass α] [inst_2 : Preorder α] [PosMulMono α],
  PosMulMono (WithBot α)
-- Mathlib.Algebra.Group.Action.Pointwise.Finset
Finset.inv_op_smul_finset_distrib : ∀ {α : Type u_2} [inst : Group α] [inst_1 : DecidableEq α] (a : α) (s : Finset α), (MulOpposite.op a • s)⁻¹ = a⁻¹ • s⁻¹
-- Mathlib.FieldTheory.PurelyInseparable.Exponent
/-- Version of `minpoly_natDegree_eq` using `ExpChar`.  -/
IsPurelyInseparable.minpoly_natDegree_eq' : ∀ (K : Type u_2) {L : Type u_3} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : IsPurelyInseparable K L] (p : ℕ) [ExpChar K p] (a : L),
  (minpoly K a).natDegree = p ^ IsPurelyInseparable.elemExponent K a
-- Mathlib.CategoryTheory.Triangulated.Functor
CategoryTheory.Functor.mapTriangleIso_inv_app_hom₃ : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.HasShift C ℤ]
  [inst_3 : CategoryTheory.HasShift D ℤ] {F₁ F₂ : CategoryTheory.Functor C D} (e : F₁ ≅ F₂) [inst_4 : F₁.CommShift ℤ]
  [inst_5 : F₂.CommShift ℤ] [inst_6 : CategoryTheory.NatTrans.CommShift e.hom ℤ]
  (X : CategoryTheory.Pretriangulated.Triangle C),
  ((CategoryTheory.Functor.mapTriangleIso e).inv.app X).hom₃ = e.inv.app X.obj₃
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_roo_eq_nil : ∀ {m n : ℕ}, n ≤ m + 1 → (m<...n).toList = []
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.Cover.Arrow.map_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C}
  {S T : J.Cover X} (I : S.Arrow) (f : S ⟶ T), (I.map f).f = I.f
-- Mathlib.Data.Complex.Basic
Complex.equivRealProdAddHom_symm_apply : ∀ (p : ℝ × ℝ), Complex.equivRealProdAddHom.symm p = ↑p.1 + ↑p.2 * Complex.I
-- Std.Data.DHashMap.IteratorLemmas
Std.DHashMap.Raw.toArray_valuesIter : ∀ {α β : Type u} {m : Std.DHashMap.Raw α fun x => β}, m.valuesIter.toArray = (List.map Sigma.snd m.toList).toArray
-- Mathlib.NumberTheory.Divisors
Int.prodMk_mem_divisorsAntidiag : ∀ {x y z : ℤ}, z ≠ 0 → ((x, y) ∈ z.divisorsAntidiag ↔ x * y = z)
-- Lean.Compiler.ExternAttr
Lean.ExternEntry.inline.inj : ∀ {backend : Lean.Name} {pattern : String} {backend_1 : Lean.Name} {pattern_1 : String},
  Lean.ExternEntry.inline backend pattern = Lean.ExternEntry.inline backend_1 pattern_1 →
    backend = backend_1 ∧ pattern = pattern_1
-- Mathlib.Algebra.GroupWithZero.Associated
Associates.isPrimal_mk : ∀ {M : Type u_1} [inst : CommMonoid M] {a : M}, IsPrimal (Associates.mk a) ↔ IsPrimal a
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Matrix.isElliptic_neg_iff : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : Preorder R] {m : Matrix (Fin 2) (Fin 2) R},
  (-m).IsElliptic ↔ m.IsElliptic
-- Lean.Meta.LetToHave
/-- Note: We want to cache all prefixes of each application, hence no `instantiateRevRange`-type logic here.
 -/
_private.Lean.Meta.LetToHave.0.Lean.Meta.LetToHave.visitApp : Lean.Expr →
  Lean.Meta.LetToHave.Result✝ → Lean.Meta.LetToHave.Result✝ → Lean.Meta.LetToHave.M✝ Lean.Meta.LetToHave.Result✝
-- Mathlib.SetTheory.Cardinal.Ordinal
Ordinal.card_opow_le_of_omega0_le_left : ∀ {a : Ordinal.{u_1}}, Ordinal.omega0 ≤ a → ∀ (b : Ordinal.{u_1}), (a ^ b).card ≤ max a.card b.card
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- Evaluate the expression `η ⊗≫ θ := η ≫ α ≫ θ` into a normalized form.  -/
Mathlib.Tactic.BicategoryLike.MkEval.mkEvalMonoidalComp : {m : Type → Type} →
  [self : Mathlib.Tactic.BicategoryLike.MkEval m] →
    Mathlib.Tactic.BicategoryLike.Mor₂ →
      Mathlib.Tactic.BicategoryLike.Mor₂ →
        Mathlib.Tactic.BicategoryLike.Structural →
          Mathlib.Tactic.BicategoryLike.NormalExpr →
            Mathlib.Tactic.BicategoryLike.NormalExpr →
              Mathlib.Tactic.BicategoryLike.NormalExpr →
                Mathlib.Tactic.BicategoryLike.NormalExpr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → m Lean.Expr
-- Init.Data.Rat.Lemmas
Rat.normalize_eq_mk' : ∀ (n : ℤ) (d : ℕ) (h : d ≠ 0) (c : n.natAbs.gcd d = 1),
  Rat.normalize n d h = { num := n, den := d, den_nz := h, reduced := c }
-- Mathlib.CategoryTheory.Bicategory.Functor.Cat.ObjectProperty
CategoryTheory.Pseudofunctor.ObjectProperty.IsClosedUnderIsomorphisms.isClosedUnderIsomorphisms : ∀ {B : Type u} {inst : CategoryTheory.Bicategory B} {F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat}
  {P : F.ObjectProperty} [self : P.IsClosedUnderIsomorphisms] (X : B), (P.prop X).IsClosedUnderIsomorphisms
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.mem_alter_self : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] {k : α}
  {f : Option β → Option β}, k ∈ Std.DTreeMap.Const.alter t k f ↔ (f (Std.DTreeMap.Const.get? t k)).isSome = true
-- Mathlib.CategoryTheory.Monoidal.Free.Coherence
CategoryTheory.FreeMonoidalCategory.inclusion_obj : ∀ {C : Type u} (X : (CategoryTheory.Discrete ∘ CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject) C),
  CategoryTheory.FreeMonoidalCategory.inclusion.obj X = CategoryTheory.FreeMonoidalCategory.inclusionObj X.as
-- Mathlib.Algebra.Order.Kleene
KleeneAlgebra.mk : {α : Type u_5} →
  [toIdemSemiring : IdemSemiring α] →
    [toKStar : KStar α] →
      (∀ (a : α), 1 ≤ KStar.kstar a) →
        (∀ (a : α), a * KStar.kstar a ≤ KStar.kstar a) →
          (∀ (a : α), KStar.kstar a * a ≤ KStar.kstar a) →
            (∀ (a b : α), b * a ≤ b → b * KStar.kstar a ≤ b) →
              (∀ (a b : α), a * b ≤ b → KStar.kstar a * b ≤ b) → KleeneAlgebra α
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Matrix.isUnit_nonsing_inv_iff : ∀ {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α] {A : Matrix n n α},
  IsUnit A⁻¹ ↔ IsUnit A
-- Init.Data.SInt.Lemmas
Int16.toUInt16_mul : ∀ (a b : Int16), (a * b).toUInt16 = a.toUInt16 * b.toUInt16
-- Mathlib.Analysis.Convex.Between
Wbtw.left_mem_image_Ici_of_right_ne : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R]
  [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P] {x y z : P},
  Wbtw R x y z → z ≠ y → x ∈ ⇑(AffineMap.lineMap z y) '' Set.Ici 1
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
/-- Every Schwartz function is smooth at any point.  -/
SchwartzMap.contDiffAt : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] (f : SchwartzMap E F) (n : ℕ∞) {x : E}, ContDiffAt ℝ (↑n) (⇑f) x
-- Mathlib.Topology.Algebra.Monoid
separatelyContinuousAdd_induced : ∀ {M : Type u_6} {N : Type u_7} {F : Type u_8} [inst : Add M] [inst_1 : Add N] [inst_2 : FunLike F M N]
  [AddHomClass F M N] [inst_4 : TopologicalSpace N] [SeparatelyContinuousAdd N] (f : F), SeparatelyContinuousAdd M
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.nil_append : ∀ {α : Type u} (s : Stream'.WSeq α), Stream'.WSeq.nil.append s = s
-- Mathlib.LinearAlgebra.Dual.Lemmas
Subspace.dual_finrank_eq : ∀ {K : Type u_1} {V : Type u_2} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V],
  Module.finrank K (Module.Dual K V) = Module.finrank K V
-- Mathlib.Logic.Function.Iterate
Function.iterate_comm : ∀ {α : Type u} (f : α → α) (m n : ℕ), f^[n] ^[m] = f^[m] ^[n]
-- Mathlib.Topology.Category.TopCat.Monoidal
TopCat.ι₀_comp_assoc : ∀ {X Y : TopCat} (f : X ⟶ Y) {Z : TopCat} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj Y TopCat.I ⟶ Z),
  CategoryTheory.CategoryStruct.comp TopCat.ι₀
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f TopCat.I) h) =
    CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp TopCat.ι₀ h)
-- Mathlib.RingTheory.Binomial
Nat.instBinomialRing : BinomialRing ℕ
-- Mathlib.Algebra.Group.Hom.Defs
MulHom.id_apply : ∀ (M : Type u_10) [inst : Mul M] (x : M), (MulHom.id M) x = x
-- Mathlib.Order.Interval.Set.ProjIcc
Set.projIcc.congr_simp : ∀ {α : Type u_1} [inst : LinearOrder α] (a b : α) (h : a ≤ b) (x x_1 : α),
  x = x_1 → Set.projIcc a b h x = Set.projIcc a b h x_1
-- Batteries.Recycling.RBTree.Alter
RBTree.RBNode.zoom.eq_def : ∀ {α : Type u_1} (cut : α → Ordering) (x : RBTree.RBNode α) (x_1 : RBTree.RBNode.Path α),
  RBTree.RBNode.zoom cut x x_1 =
    match x, x_1 with
    | RBTree.RBNode.nil, path => (RBTree.RBNode.nil, path)
    | n@h:(RBTree.RBNode.node c a y b), path =>
      match cut y with
      | Ordering.lt => RBTree.RBNode.zoom cut a (RBTree.RBNode.Path.left c path y b)
      | Ordering.gt => RBTree.RBNode.zoom cut b (RBTree.RBNode.Path.right c a y path)
      | Ordering.eq => (n, path)
-- Mathlib.Topology.UniformSpace.Cauchy
/-- A finite indexed union is totally bounded
if and only if each set of the family is totally bounded.  -/
totallyBounded_iUnion : ∀ {α : Type u} [uniformSpace : UniformSpace α] {ι : Sort u_1} [Finite ι] {s : ι → Set α},
  TotallyBounded (⋃ i, s i) ↔ ∀ (i : ι), TotallyBounded (s i)
-- Mathlib.AlgebraicGeometry.Normalization
AlgebraicGeometry.Scheme.Hom.inl_toNormalization_normalizationCoprodIso_inv_assoc : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.QuasiCompact f]
  [inst_1 : AlgebraicGeometry.QuasiSeparated f] {U V : AlgebraicGeometry.Scheme} {iU : U ⟶ X} {iV : V ⟶ X}
  (e : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk iU iV))
  [inst_2 : AlgebraicGeometry.QuasiCompact iU] [inst_3 : AlgebraicGeometry.QuasiSeparated iU]
  [inst_4 : AlgebraicGeometry.QuasiCompact iV] [inst_5 : AlgebraicGeometry.QuasiSeparated iV]
  {Z : AlgebraicGeometry.Scheme}
  (h :
    AlgebraicGeometry.Scheme.Hom.normalization (CategoryTheory.CategoryStruct.comp iU f) ⨿
        AlgebraicGeometry.Scheme.Hom.normalization (CategoryTheory.CategoryStruct.comp iV f) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp iU
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.toNormalization f)
        (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.normalizationCoprodIso f e).inv h)) =
    CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.Scheme.Hom.toNormalization (CategoryTheory.CategoryStruct.comp iU f))
      (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl h)
-- Mathlib.Algebra.Algebra.NonUnitalHom
/-- The identity map as a `NonUnitalAlgHom`.  -/
NonUnitalAlgHom.id : (R : Type u_2) →
  (A : Type u_3) →
    [inst : Monoid R] → [inst_1 : NonUnitalNonAssocSemiring A] → [inst_2 : DistribMulAction R A] → A →ₙₐ[R] A
-- Mathlib.RingTheory.Ideal.Over
Ideal.Quotient.nontrivial_of_liesOver_of_ne_top : ∀ {A : Type u_3} {B : Type u_4} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] (P : Ideal B)
  {p : Ideal A} [P.LiesOver p], p ≠ ⊤ → Nontrivial (B ⧸ P)
-- Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
/-- Eta-expanded form of `iteratedDeriv_const_smul` -/
iteratedDeriv_fun_const_smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {x : 𝕜} {R : Type u_3} [inst_3 : DistribSMul R F] [SMulCommClass 𝕜 R F]
  [ContinuousConstSMul R F] {n : ℕ} {f : 𝕜 → F},
  ContDiffAt 𝕜 (↑n) f x → ∀ (c : R), iteratedDeriv n (fun i => c • f i) x = c • iteratedDeriv n f x
-- Mathlib.Data.Nat.Factors
/-- If `p` is a prime factor of `b` then `p` is also a prime factor of `a * b` for any `a > 0`  -/
Nat.mem_primeFactorsList_mul_right : ∀ {p a b : ℕ}, p ∈ b.primeFactorsList → a ≠ 0 → p ∈ (a * b).primeFactorsList
-- Lean.Elab.Tactic.Basic
/-- Return the main goal metavariable declaration.  -/
Lean.Elab.Tactic.getMainDecl : Lean.Elab.Tactic.TacticM Lean.MetavarDecl
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
AddSubsemigroup.op_le_iff : ∀ {M : Type u_2} [inst : Add M] {S₁ : AddSubsemigroup M} {S₂ : AddSubsemigroup Mᵃᵒᵖ}, S₁.op ≤ S₂ ↔ S₁ ≤ S₂.unop
-- Mathlib.Order.CountableSupClosed
CountableInfClosed.inter : ∀ {α : Type u_2} {s t : Set α} [inst : LE α], CountableInfClosed s → CountableInfClosed t → CountableInfClosed (s ∩ t)
-- Mathlib.Tactic.FunProp.Theorems
Mathlib.Meta.FunProp.LambdaTheoremArgs.comp.sizeOf_spec : ∀ (fArgId gArgId : ℕ),
  sizeOf (Mathlib.Meta.FunProp.LambdaTheoremArgs.comp fArgId gArgId) = 1 + sizeOf fArgId + sizeOf gArgId
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Pi.map'_id_id : ∀ {α : Type w₂} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f : α → C}
  [inst_1 : CategoryTheory.Limits.HasProduct f],
  (CategoryTheory.Limits.Pi.map' id fun a => CategoryTheory.CategoryStruct.id (f a)) =
    CategoryTheory.CategoryStruct.id (∏ᶜ f)
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.le_comap_map : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N]
  (S : L.Substructure M) {f : L.Hom M N},
  S ≤ FirstOrder.Language.Substructure.comap f (FirstOrder.Language.Substructure.map f S)
-- Std.Async.Signal
/-- Converts a `Signal` to its corresponding `Int32` value as defined in `man 7 signal`.

These values are then mapped to the underlying architecture's values in runtime/uv/signal.cpp,
so make sure to update that whenever you update this code.
 -/
_private.Std.Async.Signal.0.Std.Async.Signal.toInt32 : Std.Async.Signal → Int32