mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Computability.Partrec
Partrec.fix_aux : ∀ {α : Type u_5} {σ : Type u_6} (f : α →. σ ⊕ α) (a : α) (b : σ),
  have F := fun a n =>
    Nat.rec (Part.some (Sum.inr a)) (fun x IH => IH.bind fun s => Sum.casesOn s (fun x => Part.some s) f) n;
  (∃ n, ((∃ b', Sum.inl b' ∈ F a n) ∧ ∀ {m : ℕ}, m < n → ∃ b, Sum.inr b ∈ F a m) ∧ Sum.inl b ∈ F a n) ↔ b ∈ f.fix a
-- Lean.Meta.Tactic.Grind.AC.Seq
_private.Lean.Meta.Tactic.Grind.AC.Seq.0.Lean.Grind.AC.Seq.startsWith.match_1.splitter : (motive : Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Sort u_1) →
  (s₂ s₁ : Lean.Grind.AC.Seq) →
    ((x y : Lean.Grind.AC.Var) → motive (Lean.Grind.AC.Seq.var x) (Lean.Grind.AC.Seq.var y)) →
      ((x y : Lean.Grind.AC.Var) →
          (s : Lean.Grind.AC.Seq) → motive (Lean.Grind.AC.Seq.var x) (Lean.Grind.AC.Seq.cons y s)) →
        ((x : Lean.Grind.AC.Var) →
            (s : Lean.Grind.AC.Seq) →
              (x_1 : Lean.Grind.AC.Var) → motive (Lean.Grind.AC.Seq.cons x s) (Lean.Grind.AC.Seq.var x_1)) →
          ((x : Lean.Grind.AC.Var) →
              (s₂ : Lean.Grind.AC.Seq) →
                (y : Lean.Grind.AC.Var) →
                  (s₁ : Lean.Grind.AC.Seq) → motive (Lean.Grind.AC.Seq.cons x s₂) (Lean.Grind.AC.Seq.cons y s₁)) →
            motive s₂ s₁
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.arcsin_one : Real.arcsin 1 = Real.pi / 2
-- Mathlib.Algebra.GroupWithZero.Range
MonoidWithZeroHom.valueGroup.mk_inj : ∀ {A : Type u_1} {B : Type u_2} [inst : MonoidWithZero A] [inst_1 : CommGroupWithZero B] (f : A →*₀ B) {r₁ s₁ r₂ s₂ : A}
  {hr₁ : f r₁ ≠ 0} {hs₁ : f s₁ ≠ 0} {hr₂ : f r₂ ≠ 0} {hs₂ : f s₂ ≠ 0},
  MonoidWithZeroHom.valueGroup.mk f r₁ s₁ hr₁ hs₁ = MonoidWithZeroHom.valueGroup.mk f r₂ s₂ hr₂ hs₂ ↔
    f (r₁ * s₂) = f (r₂ * s₁)
-- Mathlib.CategoryTheory.Limits.Types.Yoneda
/-- A cone on `F` with cone point `X` is the same as an element of `lim Hom(X, F·)`,
naturally in `F` and `X`.  -/
CategoryTheory.Limits.whiskeringLimYonedaIsoCones : (J : Type v) →
  [inst : CategoryTheory.SmallCategory J] →
    (C : Type u) →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        (CategoryTheory.Functor.whiskeringLeft J C (Type v)).comp
            (((CategoryTheory.Functor.whiskeringRight (CategoryTheory.Functor C (Type v))
                      (CategoryTheory.Functor J (Type v)) (Type v)).obj
                  CategoryTheory.Limits.lim).comp
              ((CategoryTheory.Functor.whiskeringLeft Cᵒᵖ (CategoryTheory.Functor C (Type v)) (Type v)).obj
                CategoryTheory.coyoneda)) ≅
          CategoryTheory.cones J C
-- Mathlib.Data.Set.NAry
Set.image2_empty_right : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : Set α}, Set.image2 f s ∅ = ∅
-- Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra
Module.FaithfullyFlat.faithfulSMul : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B]
  [Module.FaithfullyFlat A B], FaithfulSMul A B
-- Mathlib.Algebra.Order.Field.Power
Odd.zpow_nonneg_iff : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {a : α} {n : ℤ},
  Odd n → (0 ≤ a ^ n ↔ 0 ≤ a)
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.Coyoneda.coyoneda_full : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C], CategoryTheory.coyoneda.Full
-- Mathlib.MeasureTheory.Function.Jacobian
/-- Let `f` be a function which is sufficiently close (in the Lipschitz sense) to a given linear
map `A`. Then it expands the volume of any set by at most `m` for any `m > det A`.  -/
MeasureTheory.addHaar_image_le_mul_of_det_lt : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E]
  [inst_3 : MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (A : E →L[ℝ] E)
  {m : NNReal},
  ENNReal.ofReal |A.det| < ↑m →
    ∀ᶠ (δ : NNReal) in nhdsWithin 0 (Set.Ioi 0),
      ∀ (s : Set E) (f : E → E), ApproximatesLinearOn f A s δ → μ (f '' s) ≤ ↑m * μ s
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
PreQuasiregular.val_mul : ∀ {R : Type u_1} [inst : NonUnitalSemiring R] (x y : PreQuasiregular R), (x * y).val = y.val + x.val + x.val * y.val
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.EMatchTheoremKind : Type
-- Mathlib.Algebra.Order.IsBotOne
eq_one_or_one_lt : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : One α] [IsBotOneClass α] (a : α), a = 1 ∨ 1 < a
-- Mathlib.LinearAlgebra.TensorProduct.Map
LinearMap.lTensor_map : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} {Q : Type u_10} {S : Type u_11}
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : AddCommMonoid Q]
  [inst_5 : AddCommMonoid S] [inst_6 : Module R M] [inst_7 : Module R N] [inst_8 : Module R S] [inst_9 : Module R P]
  [inst_10 : Module R Q] (g' : Q →ₗ[R] S) (f : M →ₗ[R] P) (g : N →ₗ[R] Q) (x : TensorProduct R M N),
  (LinearMap.lTensor P g') ((TensorProduct.map f g) x) = (TensorProduct.map f (g' ∘ₗ g)) x
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.addSemigroup.eq_1 : ∀ {α : Type u_2} [inst : AddSemigroup α], Set.addSemigroup = { toAdd := Set.add, add_assoc := ⋯ }
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
MeasurableSpace.measurableSet_sup : ∀ {α : Type u_1} {m₁ m₂ : MeasurableSpace α} {s : Set α},
  MeasurableSet s ↔ MeasurableSpace.GenerateMeasurable {s | MeasurableSet s ∨ MeasurableSet s} s
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
MeasureTheory.JordanDecomposition.toJordanDecomposition_toSignedMeasure : ∀ {α : Type u_1} [inst : MeasurableSpace α] (j : MeasureTheory.JordanDecomposition α),
  j.toSignedMeasure.toJordanDecomposition = j
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.mk_right_unitor_inv : ∀ {B : Type u} [inst : Quiver B] {a b : CategoryTheory.FreeBicategory B} (f : a ⟶ b),
  Quot.mk CategoryTheory.FreeBicategory.Rel (CategoryTheory.FreeBicategory.Hom₂.right_unitor_inv f) =
    (CategoryTheory.Bicategory.rightUnitor f).inv
-- Mathlib.Order.Heyting.Boundary
Coheyting.hnot_eq_top_iff_exists_boundary : ∀ {α : Type u_1} [inst : CoheytingAlgebra α] {a : α}, ￢a = ⊤ ↔ ∃ b, Coheyting.boundary b = a
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Affine.Simplex.setInterior_restrict : ∀ {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] (I : Set k) {n : ℕ} (s : Affine.Simplex k P n) {S : AffineSubspace k P}
  (hS : affineSpan k (Set.range s.points) ≤ S),
  Affine.Simplex.setInterior I (s.restrict S hS) = ⇑S.subtype ⁻¹' Affine.Simplex.setInterior I s
-- Batteries.Recycling.RBTree.Basic
/-- The minimum element of a tree is the left-most value.  -/
RBTree.RBNode.min? : {α : Type u_1} → RBTree.RBNode α → Option α
-- Mathlib.Data.Part
Part.left_dom_of_add_dom : ∀ {α : Type u_1} [inst : Add α] {a b : Part α}, (a + b).Dom → a.Dom
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxc.Iterator.step_eq_step : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LE α] [inst_2 : DecidableLE α] {it : Std.Iter α},
  it.step = ⟨Std.Rxc.Iterator.step it, ⋯⟩
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Alt.default.injEq : ∀ {pu : Lean.Compiler.LCNF.Purity} (code code_1 : Lean.Compiler.LCNF.Code pu),
  (Lean.Compiler.LCNF.Alt.default code = Lean.Compiler.LCNF.Alt.default code_1) = (code = code_1)
-- Mathlib.Order.Directed
DirectedOn.prod : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {r₂ : β → β → Prop} {d₁ : Set α} {d₂ : Set β},
  DirectedOn (fun x1 x2 => r x1 x2) d₁ →
    DirectedOn (fun x1 x2 => r₂ x1 x2) d₂ → DirectedOn (fun p q => r p.1 q.1 ∧ r₂ p.2 q.2) (d₁ ×ˢ d₂)
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.map_update_smul : ∀ {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] [inst_5 : (i : ι) → TopologicalSpace (M₁ i)] [inst_6 : TopologicalSpace M₂]
  (f : ContinuousMultilinearMap R M₁ M₂) [inst_7 : DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (c : R) (x : M₁ i),
  f (Function.update m i (c • x)) = c • f (Function.update m i x)
-- Mathlib.CategoryTheory.Category.ReflQuiv
CategoryTheory.ReflQuiv.forget_faithful : ∀ {C D : CategoryTheory.Cat} (F G : CategoryTheory.Functor ↑C ↑D),
  CategoryTheory.ReflQuiv.forget.map F.toCatHom = CategoryTheory.ReflQuiv.forget.map G.toCatHom → F = G
-- Mathlib.Data.Finsupp.Basic
Finsupp.mapDomain.addMonoidHom_id : ∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M], Finsupp.mapDomain.addMonoidHom id = AddMonoidHom.id (α →₀ M)
-- Init.Data.Nat.Coprime
Nat.Coprime.coprime_div_right : ∀ {m n a : ℕ}, m.Coprime n → a ∣ n → m.Coprime (n / a)
-- Aesop.RuleTac.Apply
Aesop.RuleTac.applyConsts : Array Lean.Name → Lean.Meta.TransparencyMode → Aesop.RuleTac
-- Mathlib.Order.CountableSupClosed
CountableSupClosed.singleton : ∀ {α : Type u_2} [inst : PartialOrder α] {x : α}, CountableSupClosed {x}
-- Batteries.Data.BinomialHeap.Basic
/-- The well formedness predicate for a binomial heap.
It asserts that:
* It consists of a list of well formed trees with the specified ranks
* The ranks are in strictly increasing order, and all are at least `n`
 -/
Batteries.BinomialHeap.Imp.Heap.WF : {α : Type u_1} → (α → α → Bool) → ℕ → Batteries.BinomialHeap.Imp.Heap α → Prop
-- Init.Data.Vector.MapIdx
Vector.back_mapIdx : ∀ {n : ℕ} {α : Type u_1} {β : Type u_2} [inst : NeZero n] {xs : Vector α n} {f : ℕ → α → β},
  (Vector.mapIdx f xs).back = f (n - 1) xs.back
-- Mathlib.Data.DFinsupp.Lex
DFinsupp.Colex.addRightMono : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : LinearOrder ι] [inst_1 : (i : ι) → AddMonoid (α i)]
  [inst_2 : (i : ι) → LinearOrder (α i)] [∀ (i : ι), AddRightStrictMono (α i)], AddRightMono (Colex (Π₀ (i : ι), α i))
-- Lean.DocString.Parser
/-- How many asterisks introduced the current level of boldness? `none` means no bold here.
 -/
Lean.Doc.Parser.InlineCtxt.boldDepth : Lean.Doc.Parser.InlineCtxt → Option ℕ
-- Mathlib.LinearAlgebra.Matrix.IsDiag
/-- Every zero matrix is diagonal.  -/
Matrix.isDiag_zero : ∀ {α : Type u_1} {n : Type u_4} [inst : Zero α], Matrix.IsDiag 0
-- Lean.PrettyPrinter.Delaborator.Basic
Lean.PrettyPrinter.Delaborator.OmissionReason : Type
-- Mathlib.Topology.Instances.AddCircle.Defs
AddCircle.addOrderOf_eq_pos_iff : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] {p : 𝕜} [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [hp : Fact (0 < p)]
  {u : AddCircle p} {n : ℕ}, 0 < n → (addOrderOf u = n ↔ ∃ m < n, m.gcd n = 1 ∧ ↑(↑m / ↑n * p) = u)
-- Std.Tactic.BVDecide.LRAT.Actions
Std.Tactic.BVDecide.LRAT.instBEqAction.beq : {β : Type u_1} →
  {α : Type u_2} → [BEq β] → [BEq α] → Std.Tactic.BVDecide.LRAT.Action β α → Std.Tactic.BVDecide.LRAT.Action β α → Bool
-- Mathlib.Probability.Distributions.Gaussian.Real
ProbabilityTheory.integrableExpSet_id_gaussianReal : ∀ {μ : ℝ} {v : NNReal}, ProbabilityTheory.integrableExpSet id (ProbabilityTheory.gaussianReal μ v) = Set.univ
-- Mathlib.Algebra.Category.Semigrp.Basic
AddSemigrp.coe_of : ∀ (R : Type u) [inst : AddSemigroup R], ↑(AddSemigrp.of R) = R
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
HomotopicalAlgebra.PathObject.IsVeryGood.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C}
  [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C] {P : HomotopicalAlgebra.PathObject A}
  [inst_2 : CategoryTheory.Limits.HasBinaryProduct A A] [inst_3 : HomotopicalAlgebra.CategoryWithFibrations C]
  [inst_4 : HomotopicalAlgebra.CategoryWithCofibrations C] [toIsGood : P.IsGood],
  autoParam (HomotopicalAlgebra.Cofibration P.ι) HomotopicalAlgebra.PathObject.IsVeryGood.cofibration_ι._autoParam →
    P.IsVeryGood
-- Mathlib.Algebra.Module.Submodule.Lattice
Submodule.topEquiv_symm_apply_coe : ∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (x : M),
  ↑(Submodule.topEquiv.symm x) = x
-- Mathlib.Order.Interval.Finset.Fin
Fin.Ioo_add_one_eq_Ioc : ∀ {n : ℕ} {a b : Fin n}, ↑b + 1 < n → Finset.Ioo a (b + 1) = Finset.Ioc a b
-- Mathlib.Data.Set.Basic
Set.notMem_empty : ∀ {α : Type u} (x : α), x ∉ ∅
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Limits
SheafOfModules.instSmallElemForallObjCompModuleCatCarrierOppositeRingCatObjFunctorIsSheafPresheafOfModulesForgetEvaluationForgetLinearMapIdCarrierSections : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] {R : CategoryTheory.Sheaf J RingCat}
  (F : CategoryTheory.Functor D (SheafOfModules R))
  [∀ (X : Cᵒᵖ),
      Small.{v, max u₂ v}
        ↑((F.comp (SheafOfModules.evaluation R X)).comp (CategoryTheory.forget (ModuleCat ↑(R.obj.obj X)))).sections]
  (X : Cᵒᵖ),
  Small.{v, max u₂ v}
    ↑(((F.comp (SheafOfModules.forget R)).comp (PresheafOfModules.evaluation R.obj X)).comp
          (CategoryTheory.forget (ModuleCat ↑(R.obj.obj X)))).sections
-- Mathlib.NumberTheory.Harmonic.EulerMascheroni
Real.eulerMascheroniSeq_lt_eulerMascheroniConstant : ∀ (n : ℕ), Real.eulerMascheroniSeq n < Real.eulerMascheroniConstant
-- Mathlib.CategoryTheory.Limits.Final
/-- See also the strictly more general `initial_comp` below.  -/
CategoryTheory.Functor.initial_comp_equivalence : ∀ {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] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D E) [F.Initial] [G.IsEquivalence], (F.comp G).Initial
-- Mathlib.Data.Multiset.Powerset
Multiset.powersetCard_mono : ∀ {α : Type u_1} (n : ℕ) {s t : Multiset α}, s ≤ t → Multiset.powersetCard n s ≤ Multiset.powersetCard n t
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.ne_bot_iff_exists_ne_zero : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G}, H ≠ ⊥ ↔ ∃ a, a ≠ 0
-- Init.Data.SInt.Lemmas
Int32.le_rfl : ∀ {a : Int32}, a ≤ a
-- Mathlib.Algebra.Order.Monoid.Lex
OrderMonoidHom.inl_mul_inr_eq_mk : ∀ (α : Type u_1) (β : Type u_2) [inst : Monoid α] [inst_1 : PartialOrder α] [inst_2 : Monoid β] [inst_3 : Preorder β]
  (m : α) (n : β), (OrderMonoidHom.inl α β) m * (OrderMonoidHom.inr α β) n = (m, n)
-- Mathlib.Logic.Denumerable
_private.Mathlib.Logic.Denumerable.0.Nat.Subtype.toFunAux.congr_simp : ∀ {s : Set ℕ} {inst : DecidablePred fun x => x ∈ s} [inst_1 : DecidablePred fun x => x ∈ s] (x x_1 : ↑s),
  x = x_1 → Nat.Subtype.toFunAux✝ x = Nat.Subtype.toFunAux✝ x_1
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.bounded_singleton : ∀ {α : Type u_1} {r : α → α → Prop} [inst : IsWellOrder α r],
  Order.IsSuccLimit (Ordinal.type r) → ∀ (x : α), Set.Bounded r {x}
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.size_alter_eq_self_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k : α} {f : Option β → Option β},
  k ∈ t → (f (Std.ExtDTreeMap.Const.get? t k)).isSome = true → (Std.ExtDTreeMap.Const.alter t k f).size = t.size
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.one_eq_map_iff : ∀ {β : Type v} {α : Type u_1} {f : α → β} {v : WithBot α} [inst : One β], 1 = WithBot.map f v ↔ ∃ x, v = ↑x ∧ f x = 1
-- Mathlib.Algebra.Order.GroupWithZero.Basic
mul_self_le_mul_self : ∀ {α : Type u_1} [inst : MulZeroClass α] {a b : α} [inst_1 : Preorder α] [PosMulMono α] [MulPosMono α],
  0 ≤ a → a ≤ b → a * a ≤ b * b
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- The canonical isomorphism between the chosen biproduct and the chosen product.  -/
CategoryTheory.Limits.biprod.isoProd : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (X Y : C) → [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y] → X ⊞ Y ≅ X ⨯ Y
-- Mathlib.Data.Finsupp.Pointwise
Finsupp.instNonUnitalNonAssocSemiring : {α : Type u₁} → {β : Type u₂} → [inst : NonUnitalNonAssocSemiring β] → NonUnitalNonAssocSemiring (α →₀ β)
-- Mathlib.MeasureTheory.Group.Arithmetic
AEMeasurable.vadd_const : ∀ {M : Type u_2} {X : Type u_3} {α : Type u_4} [inst : MeasurableSpace X] [inst_1 : VAdd M X] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {f : α → M} [inst_2 : MeasurableSpace M] [MeasurableVAdd M X],
  AEMeasurable f μ → ∀ (y : X), AEMeasurable (fun x => f x +ᵥ y) μ
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
PowerSeries.IsWeierstrassDivisorAt.coeff_div_sub_seq_mem : ∀ {A : Type u_1} [inst : CommRing A] {g : PowerSeries A} {I : Ideal A} (H : g.IsWeierstrassDivisorAt I)
  (f : PowerSeries A) [inst_1 : IsPrecomplete I A] (k i : ℕ), (PowerSeries.coeff i) (H.div f - H.seq f k) ∈ I ^ k
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.toListModel_insertIfNew : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  {m : Std.DHashMap.Internal.Raw₀ α β},
  Std.DHashMap.Internal.Raw.WFImp ↑m →
    ∀ {a : α} {b : β a},
      (Std.DHashMap.Internal.toListModel (↑(m.insertIfNew a b)).buckets).Perm
        (Std.Internal.List.insertEntryIfNew a b (Std.DHashMap.Internal.toListModel (↑m).buckets))
-- Init.Data.Order.Opposite
Std.OppositeOrderInstances.instDecidableLTOpposite : {α : Type u_1} → {i : LT α} → [id : DecidableLT α] → DecidableLT α
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Cat
CategoryTheory.Monoidal.whiskerLeft : ∀ (X : CategoryTheory.Cat) {A B : CategoryTheory.Cat} (F : A ⟶ B),
  CategoryTheory.MonoidalCategoryStruct.whiskerLeft X F = ((CategoryTheory.Functor.id ↑X).prod F.toFunctor).toCatHom
-- Mathlib.Analysis.Calculus.LocalExtr.Basic
/-- If `f` has a local max on `s` at `a`, `f'` is the derivative of `f` at `a` within `s`, and
`y` belongs to the positive tangent cone of `s` at `a`, then `f' y ≤ 0`.  -/
IsLocalMaxOn.hasFDerivWithinAt_nonpos : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {f' : StrongDual ℝ E} {s : Set E}
  {a y : E}, IsLocalMaxOn f s a → HasFDerivWithinAt f f' s a → y ∈ posTangentConeAt s a → f' y ≤ 0
-- Mathlib.CategoryTheory.GuitartExact.Opposite
CategoryTheory.TwoSquare.structuredArrowRightwardsOpEquivalence_inverse : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] {T : CategoryTheory.Functor C₁ C₂} {L : CategoryTheory.Functor C₁ C₃}
  {R : CategoryTheory.Functor C₂ C₄} {B : CategoryTheory.Functor C₃ C₄} (w : CategoryTheory.TwoSquare T L R B)
  {X₃ : C₃ᵒᵖ} {X₂ : C₂ᵒᵖ} (g : B.op.obj X₃ ⟶ R.op.obj X₂),
  (w.structuredArrowRightwardsOpEquivalence g).inverse =
    CategoryTheory.TwoSquare.structuredArrowRightwardsOpEquivalence.inverse w g
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.drop.aux.eq_2 : ∀ {α : Type u} (n : ℕ), Stream'.WSeq.drop.aux n.succ = fun a => Stream'.WSeq.tail.aux a >>= Stream'.WSeq.drop.aux n
-- Std.Data.Iterators.Combinators.Monadic.Zip
Std.Iterators.Types.Zip.instFinite₁ : ∀ {m : Type w → Type w'} {α₁ β₁ : Type w} [inst : Std.Iterator α₁ m β₁] {α₂ β₂ : Type w} [inst_1 : Std.Iterator α₂ m β₂]
  [inst_2 : Monad m] [Std.Iterators.Finite α₁ m] [Std.Iterators.Productive α₂ m],
  Std.Iterators.Finite (Std.Iterators.Types.Zip α₁ m α₂ β₂) m
-- Batteries.Control.AlternativeMonad
ReaderT.instAlternativeMonad : {m : Type u_1 → Type u_2} → {ρ : Type u_1} → [AlternativeMonad m] → AlternativeMonad (ReaderT ρ m)
-- Init.Data.Iterators.Basic
Std.IterStep.mapIterator_id' : ∀ {α : Type u} {β : Type w} {step : Std.IterStep α β}, Std.IterStep.mapIterator (fun x => x) step = step
-- Mathlib.Algebra.Group.Action.End
/-- **Alias** of `AddAut.vadd_def`. -/
AddAut.smul_def : ∀ {M : Type u_2} [inst : AddMonoid M] (f : AddAut M) (a : M), f +ᵥ a = f a
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.Array.unzip.eq_1 : ∀ {α : Type u} {β : Type u_1} (as : Array (α × β)),
  as.unzip =
    Array.foldl
      (fun x x_1 =>
        match x with
        | (as, bs) =>
          match x_1 with
          | (a, b) => (as.push a, bs.push b))
      (#[], #[]) as
-- Mathlib.Algebra.Order.Ring.Defs
IsOrderedRing.toPosMulMono : ∀ {R : Type u_1} {inst : Semiring R} {inst_1 : PartialOrder R} [self : IsOrderedRing R], PosMulMono R
-- Mathlib.Computability.TuringMachine.Tape
_private.Mathlib.Computability.TuringMachine.Tape.0.Turing.Tape.nth.match_1.eq_3 : ∀ (motive : ℤ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive (Int.ofNat n.succ))
  (h_3 : (n : ℕ) → motive (Int.negSucc n)),
  (match Int.negSucc n with
    | 0 => h_1 ()
    | Int.ofNat n.succ => h_2 n
    | Int.negSucc n => h_3 n) =
    h_3 n
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor
/-- Auxiliary definition for `homEquiv`. This is the universal property
of `PresheafOfModules.ModuleColimit`, as an abelian group.  -/
PresheafOfModules.ModuleColimit.homEquiv' : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {R : CategoryTheory.Functor Cᵒᵖ RingCat} →
      {cR : CategoryTheory.Limits.Cocone R} →
        (hcR : CategoryTheory.Limits.IsColimit cR) →
          {M : PresheafOfModules R} →
            {cM : CategoryTheory.Limits.Cocone M.presheaf} →
              (hcM : CategoryTheory.Limits.IsColimit cM) →
                {N : Type w} →
                  [inst_1 : AddCommGroup N] →
                    (PresheafOfModules.ModuleColimit hcR hcM →+ N) ≃+
                      (M.presheaf ⟶ (CategoryTheory.Functor.const Cᵒᵖ).obj (AddCommGrpCat.of N))
-- Mathlib.Algebra.Category.BialgCat.Basic
/-- The object in the category of `R`-bialgebras associated to an `R`-bialgebra.  -/
BialgCat.of : (R : Type u) → [inst : CommRing R] → (X : Type v) → [inst_1 : Ring X] → [Bialgebra R X] → BialgCat R
-- Mathlib.Analysis.Normed.Field.Basic
/-- A densely normed field is always a nontrivially normed field.
See note [lower instance priority].  -/
DenselyNormedField.toNontriviallyNormedField : {α : Type u_2} → [DenselyNormedField α] → NontriviallyNormedField α
-- Lean.Level
Lean.Level.toNat : Lean.Level → Option ℕ
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.aeval_natCast : ∀ {R : Type u} {A : Type z} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (x : A) (n : ℕ),
  (Polynomial.aeval x) ↑n = ↑n
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Option.isSome.match_1.eq_2 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (h_1 : (val : α) → motive (some val)) (h_2 : Unit → motive none),
  (match none with
    | some val => h_1 val
    | none => h_2 ()) =
    h_2 ()
-- Mathlib.Algebra.Group.Conj
ConjClasses.quotient_mk_eq_mk : ∀ {α : Type u} [inst : Monoid α] (a : α), ⟦a⟧ = ConjClasses.mk a
-- Init.Data.Array.Lemmas
Array.mem_or_eq_of_mem_setIfInBounds : ∀ {α : Type u_1} {xs : Array α} {i : ℕ} {a b : α}, a ∈ xs.setIfInBounds i b → a ∈ xs ∨ a = b
-- Mathlib.Geometry.Manifold.Diffeomorph
Diffeomorph.contMDiffWithinAt_diffeomorph_comp_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {F : Type u_4}
  [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜 F] {H : Type u_5} [inst_7 : TopologicalSpace H]
  {H' : Type u_6} [inst_8 : TopologicalSpace H'] {G : Type u_7} [inst_9 : TopologicalSpace G]
  {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {J : ModelWithCorners 𝕜 F G} {M : Type u_9}
  [inst_10 : TopologicalSpace M] [inst_11 : ChartedSpace H M] {M' : Type u_10} [inst_12 : TopologicalSpace M']
  [inst_13 : ChartedSpace H' M'] {N : Type u_11} [inst_14 : TopologicalSpace N] [inst_15 : ChartedSpace G N]
  {n m : WithTop ℕ∞} (h : Diffeomorph I J M N n) {f : M' → M},
  m ≤ n → ∀ {s : Set M'} {x : M'}, ContMDiffWithinAt I' J m (⇑h ∘ f) s x ↔ ContMDiffWithinAt I' I m f s x