mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
CategoryTheory.instPreservesColimitsTensorLeft : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (A : C)
  [CategoryTheory.Closed A], CategoryTheory.Limits.PreservesColimits (CategoryTheory.MonoidalCategory.tensorLeft A)
-- Mathlib.NumberTheory.LSeries.ZMod
ZMod.completedLFunction_const_mul : ∀ {N : ℕ} [inst : NeZero N] (a : ℂ) (Φ : ZMod N → ℂ) (s : ℂ),
  ZMod.completedLFunction (fun j => a * Φ j) s = a * ZMod.completedLFunction Φ s
-- Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
PositiveLinearMap.leftMulMapPreGNS_mul_eq_comp : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] (f : A →ₚ[ℂ] ℂ) [inst_2 : StarOrderedRing A]
  (a b : A), f.leftMulMapPreGNS (a * b) = f.leftMulMapPreGNS a ∘SL f.leftMulMapPreGNS b
-- Mathlib.Algebra.Group.Pi.Lemmas
MulHom.pi_apply : ∀ {I : Type u} {f : I → Type v} [inst : (i : I) → Mul (f i)] {γ : Type w} [inst_1 : Mul γ] (g : (i : I) → γ →ₙ* f i)
  (x : γ) (i : I), (MulHom.pi g) x i = (g i) x
-- Mathlib.Algebra.Category.Ring.Basic
/-- Typecheck a `RingHom` as a morphism in `SemiRingCat`.  -/
SemiRingCat.ofHom : {R S : Type u} → [inst : Semiring R] → [inst_1 : Semiring S] → (R →+* S) → (SemiRingCat.of R ⟶ SemiRingCat.of S)
-- Std.Do.WP.SimpLemmas
Std.Do.WP.tryCatch_Except : ∀ {ε α : Type u_1} {x : Except ε α} {h : ε → Except ε α}
  {Q : Std.Do.PostCond α (Std.Do.PostShape.except ε Std.Do.PostShape.pure)},
  (Std.Do.wp (MonadExceptOf.tryCatch x h)).apply Q =
    (Std.Do.wp x).apply (Q.1, fun e => (Std.Do.wp (h e)).apply Q, Q.2.2)
-- Mathlib.Data.List.TakeDrop
List.dropLast_drop_eq_drop_dropLast : ∀ {α : Type u} (l : List α) (n : ℕ), (List.drop n l).dropLast = List.drop n l.dropLast
-- Mathlib.Data.Real.ConjExponents
NNReal.HolderConjugate.one_sub_inv_inv : ∀ {a : NNReal}, 0 < a → a < 1 → (1 - a)⁻¹.HolderConjugate a⁻¹
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Poly.denote_append : ∀ (ctx : Nat.Internal.Linear.Context) (p q : Nat.Internal.Linear.Poly),
  Nat.Internal.Linear.Poly.denote ctx (p ++ q) =
    Nat.Internal.Linear.Poly.denote ctx p + Nat.Internal.Linear.Poly.denote ctx q
-- Mathlib.RingTheory.Localization.NumDen
IsFractionRing.eq_zero_of_num_eq_zero : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : IsDomain A] [inst_2 : UniqueFactorizationMonoid A] {K : Type u_2}
  [inst_3 : Field K] [inst_4 : Algebra A K] [inst_5 : IsFractionRing A K] {x : K}, IsFractionRing.num A x = 0 → x = 0
-- Std.Time.Format.Modifier
Std.Time.instReprOffsetZ : Repr Std.Time.OffsetZ
-- Mathlib.Algebra.Order.Monoid.Unbundled.Pow
le_max_of_sq_le_mul : ∀ {M : Type u_3} [inst : Monoid M] [inst_1 : LinearOrder M] [MulLeftStrictMono M] [MulRightStrictMono M] {a b c : M},
  a ^ 2 ≤ b * c → a ≤ max b c
-- Mathlib.Topology.MetricSpace.Bounded
Bornology.IsBounded.subset_closedBall : ∀ {α : Type u} {s : Set α} [inst : PseudoMetricSpace α],
  Bornology.IsBounded s → ∀ (c : α), ∃ r, s ⊆ Metric.closedBall c r
-- Mathlib.RepresentationTheory.FiniteIndex
Rep.resIndAdjunction_homEquiv_symm_apply : ∀ {k : Type u} {G : Type v} [inst : CommRing k] [inst_1 : Group G] {S : Subgroup G}
  [inst_2 : DecidableRel ⇑(QuotientGroup.rightRel S)] [inst_3 : S.FiniteIndex] (A : Rep.{max w u v, u, v} k ↥S)
  {B : Rep.{max w u v, u, v} k G} (f : B ⟶ (Rep.indFunctor k S.subtype).obj A),
  ((Rep.resIndAdjunction k S).homEquiv B A).symm f =
    (Rep.resCoindHomEquiv.{max w u v, u, v, v} S.subtype B A).symm
      (CategoryTheory.CategoryStruct.comp f A.indCoindIso.hom)
-- Mathlib.NumberTheory.Padics.Hensel
_private.Mathlib.NumberTheory.Padics.Hensel.0.soln_deriv_norm : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : CommSemiring R] [inst_2 : Algebra R ℤ_[p]]
  {F : Polynomial R} {a : ℤ_[p]}
  (hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2),
  ‖(Polynomial.aeval (soln_gen✝ hnorm)) (Polynomial.derivative F)‖ = ‖(Polynomial.aeval a) (Polynomial.derivative F)‖
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.adj_inj : ∀ {V : Type u} {G H : SimpleGraph V}, G.Adj = H.Adj ↔ G = H
-- Std.Tactic.BVDecide.Bitblast.BoolExpr.Basic
Std.Tactic.BVDecide.BoolExpr.Unsat : {α : Type} → Std.Tactic.BVDecide.BoolExpr α → Prop
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get!_erase : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α]
  {k a : α}, (t.erase k).get! a = if cmp k a = Ordering.eq then default else t.get! a
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.Scheme.Hom.mem_opensRange : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [inst : AlgebraicGeometry.IsOpenImmersion f] {y : ↥Y},
  y ∈ AlgebraicGeometry.Scheme.Hom.opensRange f ↔ ∃ x, f x = y
-- Mathlib.MeasureTheory.Integral.CircleIntegral
CircleIntegrable.sub : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {f g : ℂ → E} {c : ℂ} {R : ℝ},
  CircleIntegrable f c R → CircleIntegrable g c R → CircleIntegrable (f - g) c R
-- Mathlib.Geometry.Manifold.StructureGroupoid
/-- The pregroupoid property is "local", in the sense that `f` has the pregroupoid property on `u`
iff its restriction to each open subset of `u` has it  -/
Pregroupoid.locality : ∀ {H : Type u_2} [inst : TopologicalSpace H] (self : Pregroupoid H) {f : H → H} {u : Set H},
  IsOpen u → (∀ x ∈ u, ∃ v, IsOpen v ∧ x ∈ v ∧ self.property f (u ∩ v)) → self.property f u
-- Mathlib.Analysis.Normed.Group.Basic
mem_closedBall_iff_norm'' : ∀ {E : Type u_5} [inst : SeminormedCommGroup E] {a b : E} {r : ℝ}, b ∈ Metric.closedBall a r ↔ ‖b / a‖ ≤ r
-- Mathlib.Data.Ordmap.Ordnode
Ordnode.toBinaryTree.eq_2 : ∀ {α : Type u_1} (sz : ℕ) (l : Ordnode α) (x_1 : α) (r : Ordnode α),
  (Ordnode.node sz l x_1 r).toBinaryTree = BinaryTree.node x_1 l.toBinaryTree r.toBinaryTree
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Submonoid.LocalizationMap.mk'_eq_of_eq : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N]
  (f : S.LocalizationMap N) {a₁ b₁ : M} {a₂ b₂ : ↥S}, ↑a₂ * b₁ = ↑b₂ * a₁ → f.mk' a₁ a₂ = f.mk' b₁ b₂
-- Mathlib.Algebra.MonoidAlgebra.Grading
AddMonoidAlgebra.single_mem_gradeBy : ∀ {M : Type u_1} {ι : Type u_2} {R : Type u_4} [inst : CommSemiring R] (f : M → ι) (m : M) (r : R),
  AddMonoidAlgebra.single m r ∈ AddMonoidAlgebra.gradeBy R f (f m)
-- Mathlib.GroupTheory.RegularWreathProduct
/-- The regular wreath product of groups `Q` and `D`. It is the product `(Q → D) × Q` with the group
operation `⟨a₁, a₂⟩ * ⟨b₁, b₂⟩ = ⟨a₁ * (fun x ↦ b₁ (a₂⁻¹ * x)), a₂ * b₂⟩`.  -/
«term_≀ᵣ_» : Lean.TrailingParserDescr
-- Mathlib.Tactic.Linter.DocString
/-- The `docStringVerso` linter warns on docstrings that cannot be parsed by Verso.
Since this linter only checks syntax, not semantics, it is no assurance that complying docstrings
are actually accepted by Verso.
 -/
Mathlib.Linter.linter.style.docStringVerso : Lean.Option Bool
-- Mathlib.Data.Seq.Basic
Stream'.Seq.Pairwise.eq_1 : ∀ {α : Type u} (R : α → α → Prop) (s : Stream'.Seq α),
  Stream'.Seq.Pairwise R s = ∀ (i j : ℕ), i < j → ∀ x ∈ s.get? i, ∀ y ∈ s.get? j, R x y
-- Init.Data.String.Lemmas.Pattern.Find.Pred
String.Pos.find?_prop_eq_some_iff_splits : ∀ {p : Char → Prop} [inst : DecidablePred p] {s : String} {pos : s.Pos} {t u : String},
  pos.Splits t u →
    ∀ {pos' : s.Pos},
      pos.find? p = some pos' ↔ ∃ v c w, pos'.Splits (t ++ v) (String.singleton c ++ w) ∧ p c ∧ ∀ d ∈ v.toList, ¬p d
-- Mathlib.Data.List.Lemmas
_private.Mathlib.Data.List.Lemmas.0.List.mapAccumr₂.match_1.splitter : {α : Type u_1} →
  {β : Type u_2} →
    {γ : Type u_4} →
      (motive : List α → List β → γ → Sort u_3) →
        (x : List α) →
          (x_1 : List β) →
            (x_2 : γ) →
              ((x : List β) → (c : γ) → motive [] x c) →
                ((x : List α) → (c : γ) → (x = [] → False) → motive x [] c) →
                  ((x : α) → (xr : List α) → (y : β) → (yr : List β) → (c : γ) → motive (x :: xr) (y :: yr) c) →
                    motive x x_1 x_2
-- Mathlib.Logic.Equiv.Set
Equiv.Set.insert_symm_apply_inl : ∀ {α : Type u} {s : Set α} [inst : DecidablePred fun x => x ∈ s] {a : α} (H : a ∉ s) (b : ↑s),
  (Equiv.Set.insert H).symm (Sum.inl b) = ⟨↑b, ⋯⟩
-- Mathlib.Analysis.LocallyConvex.Separation
RCLike.geometric_hahn_banach_point_point : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : TopologicalSpace E] [inst_1 : AddCommGroup E] [inst_2 : Module ℝ E] {x y : E}
  [inst_3 : RCLike 𝕜] [inst_4 : Module 𝕜 E] [IsScalarTower ℝ 𝕜 E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E]
  [LocallyConvexSpace ℝ E] [T1Space E], x ≠ y → ∃ f, RCLike.re (f x) < RCLike.re (f y)
-- Lean.EnvExtension
Lean.MapDeclarationExtension.contains : {α : Type} → [Inhabited α] → Lean.MapDeclarationExtension α → Lean.Environment → Lean.Name → Bool
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.smul_eq_empty : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] {s : Set α} {t : Set β}, s • t = ∅ ↔ s = ∅ ∨ t = ∅
-- Mathlib.Order.Filter.Partial
/-- Generic "limit of a relation" predicate. `RTendsto r l₁ l₂` asserts that for every
`l₂`-neighborhood `a`, the `r`-core of `a` is an `l₁`-neighborhood. One generalization of
`Filter.Tendsto` to relations.  -/
Filter.RTendsto : {α : Type u} → {β : Type v} → SetRel α β → Filter α → Filter β → Prop
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.card_lt_card_of_right_finite : ∀ {α : Type u} {A B : Set α}, B.Finite → A ⊂ B → Cardinal.mk ↑A < Cardinal.mk ↑B
-- Mathlib.Data.Real.ConjExponents
Real.HolderTriple.mk : ∀ {p q r : ℝ}, p⁻¹ + q⁻¹ = r⁻¹ → 0 < p → 0 < q → p.HolderTriple q r
-- Std.Sat.AIG.Basic
/-- The denotation of the `Entrypoint` is false for all assignments.
 -/
Std.Sat.AIG.Entrypoint.Unsat : {α : Type} → [inst : Hashable α] → [inst_1 : DecidableEq α] → Std.Sat.AIG.Entrypoint α → Prop
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.add_le_add_iff_right : ∀ {α : Type u} [inst : Add α] {x y z : WithTop α} [inst_1 : LE α] [AddRightMono α] [AddRightReflectLE α],
  z ≠ ⊤ → (x + z ≤ y + z ↔ x ≤ y)
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.sub_apply : ∀ {V₁ : Type u_2} {V₂ : Type u_3} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂]
  (f g : NormedAddGroupHom V₁ V₂) (v : V₁), (f - g) v = f v - g v
-- Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
CategoryTheory.Pseudofunctor.isoMapOfCommSq.eq_1 : ∀ {B : Type u₁} {C : Type u₂} [inst : CategoryTheory.Bicategory B] [inst_1 : CategoryTheory.Bicategory.Strict B]
  [inst_2 : CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {X₁ X₂ Y₁ Y₂ : B} {t : X₁ ⟶ Y₁}
  {l : X₁ ⟶ X₂} {r : Y₁ ⟶ Y₂} {b : X₂ ⟶ Y₂} (sq : CategoryTheory.CommSq t l r b),
  F.isoMapOfCommSq sq = (F.mapComp t r).symm ≪≫ F.mapComp' l b (CategoryTheory.CategoryStruct.comp t r) ⋯
-- Mathlib.SetTheory.Ordinal.FixedPoint
Ordinal.nfp_le_iff : ∀ {f : Ordinal.{u} → Ordinal.{u}} {a b : Ordinal.{u}}, Ordinal.nfp f a ≤ b ↔ ∀ (n : ℕ), f^[n] a ≤ b
-- Mathlib.CategoryTheory.EquivalenceRelation
CategoryTheory.EffectiveEquivalenceRelation.mk.sizeOf_spec : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {R A : C} {p₁ p₂ : R ⟶ A} [inst_1 : SizeOf C]
  (toEquivalenceRelation : CategoryTheory.EquivalenceRelation p₁ p₂) (B : C) (π : A ⟶ B)
  (isKernelPair : CategoryTheory.IsKernelPair π p₁ p₂) (isPushout : CategoryTheory.IsPushout p₁ p₂ π π),
  sizeOf
      { toEquivalenceRelation := toEquivalenceRelation, B := B, π := π, isKernelPair := isKernelPair,
        isPushout := isPushout } =
    1 + sizeOf toEquivalenceRelation + sizeOf B + sizeOf π + sizeOf isKernelPair + sizeOf isPushout
-- Mathlib.Algebra.Algebra.Unitization
Unitization.fst_neg : ∀ {R : Type u_3} {A : Type u_4} [inst : Neg R] [inst_1 : Neg A] (x : Unitization R A), (-x).toProd.1 = -x.toProd.1
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.productTriangle.lift_hom₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ] {J : Type u_1}
  (T : J → CategoryTheory.Pretriangulated.Triangle C) [inst_2 : CategoryTheory.Limits.HasProduct fun j => (T j).obj₁]
  [inst_3 : CategoryTheory.Limits.HasProduct fun j => (T j).obj₂]
  [inst_4 : CategoryTheory.Limits.HasProduct fun j => (T j).obj₃]
  [inst_5 : CategoryTheory.Limits.HasProduct fun j => (CategoryTheory.shiftFunctor C 1).obj (T j).obj₁]
  {T' : CategoryTheory.Pretriangulated.Triangle C} (φ : (j : J) → T' ⟶ T j),
  (CategoryTheory.Pretriangulated.productTriangle.lift T φ).hom₃ = CategoryTheory.Limits.Pi.lift fun j => (φ j).hom₃
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.isEmpty_inter_iff : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ((t₁ ∩ t₂).isEmpty = true ↔ ∀ k ∈ t₁, k ∉ t₂)
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.instIsStableUnderShiftExtensionProductIterInt : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (P : CategoryTheory.ObjectProperty C) [P.IsStableUnderShift ℤ] (n : ℕ),
  (P.extensionProductIter n).IsStableUnderShift ℤ
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.mem_of_mem_union_of_not_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α},
  k ∈ t₁ ∪ t₂ → k ∉ t₂ → k ∈ t₁
-- Mathlib.Analysis.Normed.Group.Continuity
tendsto_norm_neg_add_self_nhdsNE : ∀ {E : Type u_4} [inst : NormedAddGroup E] (a : E),
  Filter.Tendsto (fun x => ‖-x + a‖) (nhdsWithin a {a}ᶜ) (nhdsWithin 0 (Set.Ioi 0))
-- Lean.Util.PPExt
Lean.instInhabitedPPFns.default : Lean.PPFns
-- Mathlib.Data.Setoid.Partition
Setoid.finite_classes_ker : ∀ {α : Type u_2} {β : Type u_3} [Finite β] (f : α → β), (Setoid.ker f).classes.Finite
-- Mathlib.Data.Nat.Init
Nat.decreasingInduction_succ_left : ∀ {m n : ℕ} {motive : (m : ℕ) → m ≤ n → Sort u_1} (of_succ : (k : ℕ) → (h : k < n) → motive (k + 1) h → motive k ⋯)
  (self : motive n ⋯) (smn : m + 1 ≤ n) (mn : m ≤ n),
  Nat.decreasingInduction of_succ self mn = of_succ m smn (Nat.decreasingInduction of_succ self smn)
-- Lean.PrivateName
Lean.isPrivateName : Lean.Name → Bool
-- Mathlib.Data.Set.BoolIndicator
Set.preimage_boolIndicator_eq_union : ∀ {α : Type u_1} (s : Set α) (t : Set Bool),
  s.boolIndicator ⁻¹' t = (if true ∈ t then s else ∅) ∪ if false ∈ t then sᶜ else ∅
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.singleton_eq_insert : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {p : α}, {p} = ∅.insert p
-- Init.Data.Iterators.Consumers.Monadic.Loop
_private.Init.Data.Iterators.Consumers.Monadic.Loop.0.Std.IterM.DefaultConsumers.forIn'.match_1.splitter : {β : Type u_3} →
  (γ : Type u_1) →
    (PlausibleForInStep : β → γ → ForInStep γ → Prop) →
      (acc : γ) →
        (out : β) →
          (motive : Subtype (PlausibleForInStep out acc) → Sort u_2) →
            (__do_lift : Subtype (PlausibleForInStep out acc)) →
              ((c : γ) → (h' : PlausibleForInStep out acc (ForInStep.yield c)) → motive ⟨ForInStep.yield c, h'⟩) →
                ((c : γ) → (h : PlausibleForInStep out acc (ForInStep.done c)) → motive ⟨ForInStep.done c, h⟩) →
                  motive __do_lift
-- Lean.Data.Lsp.TextSync
Lean.Lsp.TextDocumentSyncKind.incremental : Lean.Lsp.TextDocumentSyncKind
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHom.toEnd_sub : ∀ {α : Type u_5} [inst : NonUnitalNonAssocRing α] (x y : CentroidHom α), (x - y).toEnd = x.toEnd - y.toEnd
-- Init.Data.Int.Order
Int.le_of_not_gt : ∀ {a b : ℤ}, ¬a > b → a ≤ b
-- Mathlib.Geometry.Manifold.Instances.Sphere
/-- Stereographic projection, forward direction. This is a map from an inner product space `E` to
the orthogonal complement of an element `v` of `E`. It is smooth away from the affine hyperplane
through `v` parallel to the orthogonal complement.  It restricts on the sphere to the stereographic
projection.  -/
stereoToFun : {E : Type u_1} → [inst : NormedAddCommGroup E] → [inst_1 : InnerProductSpace ℝ E] → (v : E) → E → ↥(ℝ ∙ v)ᗮ
-- Mathlib.Data.Finsupp.Order
/-- The support of a sum is the union of the supports, when the coefficients satisfy
`CanonicallyOrderedAdd`.

In the case where the supports are disjoint, there is also `Finsupp.support_add_eq`,
which holds in any `AddZeroClass`.  -/
Finsupp.support_add_eq_union : ∀ {ι : Type u_1} {α : Type u_3} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [CanonicallyOrderedAdd α]
  [inst_3 : Sub α] [OrderedSub α] {f1 f2 : ι →₀ α} [inst_5 : DecidableEq ι], (f1 + f2).support = f1.support ∪ f2.support
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnModule.instAddCommGroup : {Γ : Type u_1} →
  {R : Type u_3} →
    {V : Type u_5} →
      [inst : PartialOrder Γ] → [inst_1 : SMul R V] → [inst_2 : AddCommGroup V] → AddCommGroup (HahnModule Γ R V)
-- Std.Data.TreeMap.Basic
/-- Returns the key-value pair with the `n`-th smallest key, or `none` if `n` is at least `t.size`.  -/
Std.TreeMap.entryAtIdx? : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap α β cmp → ℕ → Option (α × β)
-- Mathlib.AlgebraicGeometry.Morphisms.Smooth
AlgebraicGeometry.instFlatOfSmooth : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.Smooth f], AlgebraicGeometry.Flat f
-- Init.Data.List.TakeDrop
List.takeWhile.eq_2 : ∀ {α : Type u} (p : α → Bool) (a : α) (as : List α),
  List.takeWhile p (a :: as) =
    match p a with
    | true => a :: List.takeWhile p as
    | false => []
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.all_eq_false_iff_exists_mem_get : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α]
  {p : (a : α) → β a → Bool}, m.all p = false ↔ ∃ a, ∃ (h : a ∈ m), p a (m.get a h) = false
-- Mathlib.LinearAlgebra.Multilinear.Basic
/-- This calculates the differences between the values of a multilinear map at
two arguments that differ on a finset `s` of `ι`. It requires a
linear order on `ι` in order to express the result.  -/
MultilinearMap.map_piecewise_sub_map_piecewise : ∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommGroup (M₁ i)] [inst_2 : AddCommGroup M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] (f : MultilinearMap R M₁ M₂) [inst_5 : LinearOrder ι] (a b v : (i : ι) → M₁ i) (s : Finset ι),
  f (s.piecewise a v) - f (s.piecewise b v) =
    ∑ i ∈ s, f fun j => if j ∈ s then if j < i then a j else if j = i then a j - b j else b j else v j
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.Limits.WalkingReflexivePair.reflexion_comp_right_assoc : ∀ {Z : CategoryTheory.Limits.WalkingReflexivePair} (h : CategoryTheory.Limits.WalkingReflexivePair.zero ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.WalkingReflexivePair.Hom.reflexion
      (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.WalkingReflexivePair.Hom.right h) =
    h
-- Init.Data.UInt.Lemmas
USize.toBitVec_ne_of_ne : ∀ {a b : USize}, a ≠ b → a.toBitVec ≠ b.toBitVec
-- Mathlib.Data.Stream.Init
Stream'.map_const : ∀ {α : Type u} {β : Type v} (f : α → β) (a : α), Stream'.map f (Stream'.const a) = Stream'.const (f a)
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.toProd_comp_inr : ∀ {M : Type u_1} {N : Type u_2} [inst : AddMonoid M] [inst_1 : AddMonoid N],
  AddMonoid.Coprod.toProd.comp AddMonoid.Coprod.inr = AddMonoidHom.inr M N
-- Batteries.Util.LibraryNote
/-- Encode a name to be safe for the Lean export format.

The current export format (used by `lean4export` and consumed by external type checkers like
`nanoda_lib`) does not support whitespace in declaration names. Library notes often have
human-readable names with spaces like `«my library note»`, which would produce declarations
like `LibraryNote.«my library note»` that cannot be exported.

This function replaces spaces with underscores to produce export-safe names like
`LibraryNote.my_library_note`.
 -/
Batteries.Util.LibraryNote.encodeNameForExport : Lean.Name → Lean.Name
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.Y_ne_negY_of_Y_ne : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} [NoZeroDivisors R] {P Q : Fin 3 → R},
  W'.Equation P → W'.Equation Q → P 0 * Q 2 ^ 2 = Q 0 * P 2 ^ 2 → P 1 * Q 2 ^ 3 ≠ Q 1 * P 2 ^ 3 → P 1 ≠ W'.negY P
-- Mathlib.Algebra.Homology.ExactSequence
CategoryTheory.ComposableArrows.Exact.δlast : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {n : ℕ} {S : CategoryTheory.ComposableArrows C (n + 2)}, S.Exact → S.δlast.Exact
-- Mathlib.Order.Interval.Finset.Defs
Finset.uIcc_product_uIcc : ∀ {α : Type u_1} {β : Type u_2} [inst : Lattice α] [inst_1 : Lattice β] [inst_2 : LocallyFiniteOrder α]
  [inst_3 : LocallyFiniteOrder β] [inst_4 : DecidableLE (α × β)] (a₁ a₂ : α) (b₁ b₂ : β),
  Finset.uIcc a₁ a₂ ×ˢ Finset.uIcc b₁ b₂ = Finset.uIcc (a₁, b₁) (a₂, b₂)
-- Mathlib.Algebra.Order.Positive.Ring
Positive.instOneSubtypeLtOfNat_mathlib : {R : Type u_2} → [inst : Semiring R] → [inst_1 : PartialOrder R] → [IsStrictOrderedRing R] → One { x // 0 < x }
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the reverse direction of `antivaryOn_inv`. -/
AntivaryOn.inv : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α]
  [inst_3 : CommGroup β] [inst_4 : PartialOrder β] [IsOrderedMonoid β] {s : Set ι} {f : ι → α} {g : ι → β},
  AntivaryOn f g s → AntivaryOn f⁻¹ g⁻¹ s
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.coeff_X_zero : ∀ {R : Type u} [inst : Semiring R], Polynomial.X.coeff 0 = 0
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.map_add_toArray_rio : ∀ {n k : ℕ}, Array.map (fun x => x + k) (*...n).toArray = (k...n + k).toArray
-- Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc
CategoryTheory.SmallObject.SuccStruct.extendToSuccObjIso_hom_naturality : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {J : Type u} [inst_1 : LinearOrder J]
  [inst_2 : SuccOrder J] {j : J} (hj : ¬IsMax j) (F : CategoryTheory.Functor (↑(Set.Iic j)) C) {X : C}
  (τ : F.obj ⟨j, ⋯⟩ ⟶ X) (i₁ i₂ : J) (hi : i₁ ≤ i₂) (hi₂ : i₂ ≤ j),
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.SmallObject.SuccStruct.extendToSucc hj F τ).map (CategoryTheory.homOfLE hi))
      (CategoryTheory.SmallObject.SuccStruct.extendToSuccObjIso hj F τ i₂ hi₂).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.SuccStruct.extendToSuccObjIso hj F τ i₁ ⋯).hom
      (F.map (CategoryTheory.homOfLE hi))
-- Mathlib.NumberTheory.EulerProduct.DirichletLSeries
riemannZeta_eq_exp_LSeries : ∀ {s : ℂ},
  1 < s.re → Complex.exp (LSeries (fun n => ↑(ArithmeticFunction.vonMangoldt n) / ↑(Real.log ↑n)) s) = riemannZeta s
-- Mathlib.Data.Fintype.Order
Finite.map_iInf_of_monotoneOn : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : ConditionallyCompleteLinearOrder α]
  [inst_1 : ConditionallyCompleteLattice β] [Finite ι] [Nonempty ι] {s : Set α} {f : ι → α} {g : α → β},
  MonotoneOn g s → (∀ (i : ι), f i ∈ s) → g (⨅ i, f i) = ⨅ i, g (f i)
-- Mathlib.Data.Finset.Piecewise
Finset.piecewise_compl : ∀ {ι : Type u_1} {π : ι → Sort u_2} [inst : Fintype ι] [inst_1 : DecidableEq ι] (s : Finset ι)
  [inst_2 : (i : ι) → Decidable (i ∈ s)] [inst_3 : (i : ι) → Decidable (i ∈ sᶜ)] (f g : (i : ι) → π i),
  sᶜ.piecewise f g = s.piecewise g f
-- Mathlib.Data.Fin.Tuple.Basic
Fin.castLT.eq_1 : ∀ {n m : ℕ} (i : Fin m) (h : ↑i < n), i.castLT h = ⟨↑i, h⟩
-- Mathlib.Dynamics.FixedPoints.Defs
Function.fixedPoints_subset_range : ∀ {α : Type u_1} {f : α → α}, Function.fixedPoints f ⊆ Set.range f
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.RotateRight
Std.Tactic.BVDecide.BVExpr.bitblast.blastRotateRight.go_get : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (distance : ℕ)
  (input : aig.RefVec w) (curr : ℕ) (hcurr : curr ≤ w) (s : aig.RefVec curr) (idx : ℕ) (hidx1 : idx < w),
  curr ≤ idx →
    (Std.Tactic.BVDecide.BVExpr.bitblast.blastRotateRight.go input distance curr hcurr s).get idx hidx1 =
      if hidx3 : idx < w - distance % w then input.get (distance % w + idx) ⋯
      else input.get (idx - (w - distance % w)) ⋯