mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Array.Lemmas
Array.forall_mem_replicate : ∀ {α : Type u_1} {p : α → Prop} {a : α} {n : ℕ}, (∀ b ∈ Array.replicate n a, p b) ↔ n = 0 ∨ p a
-- Mathlib.Analysis.Normed.Field.UnitBall
Metric.unitSphere.coe_div : ∀ {𝕜 : Type u_1} [inst : NormedDivisionRing 𝕜] (x y : ↑(Metric.sphere 0 1)), ↑(x / y) = ↑x / ↑y
-- Init.Data.String.Basic
String.slice_eq_slice! : ∀ {s : String} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁}, s.slice p₀ p₁ h = s.slice! p₀ p₁
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_rco_eq_singleton_append_iff : ∀ {xs : Array ℕ} {m n a : ℕ}, (m...n).toArray = #[a] ++ xs ↔ m = a ∧ m < n ∧ ((m + 1)...n).toArray = xs
-- Mathlib.Order.Interval.Finset.Box
Finset.box.eq_1 : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : PartialOrder α] [inst_2 : LocallyFiniteOrder α] [inst_3 : DecidableEq α],
  Finset.box = disjointed fun n => Finset.Icc (-↑n) ↑n
-- Mathlib.CategoryTheory.Localization.HomEquiv
CategoryTheory.Localization.homEquiv_id : ∀ {C : Type u_1} {D₁ : Type u_5} {D₂ : Type u_6} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_5, u_5} D₁] [inst_2 : CategoryTheory.Category.{v_6, u_6} D₂]
  (W : CategoryTheory.MorphismProperty C) (L₁ : CategoryTheory.Functor C D₁) [inst_3 : L₁.IsLocalization W]
  (L₂ : CategoryTheory.Functor C D₂) [inst_4 : L₂.IsLocalization W] (X : C),
  (CategoryTheory.Localization.homEquiv W L₁ L₂) (CategoryTheory.CategoryStruct.id (L₁.obj X)) =
    CategoryTheory.CategoryStruct.id (L₂.obj X)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Pow
nsmul_nonpos_iff : ∀ {M : Type u_3} [inst : AddMonoid M] [inst_1 : LinearOrder M] [AddLeftMono M] {x : M} {n : ℕ},
  n ≠ 0 → (n • x ≤ 0 ↔ x ≤ 0)
-- Mathlib.Topology.UniformSpace.Separation
/-- If the uniformity has a linearly ordered basis, then the space is completely normal.
 -/
UniformSpace.completelyNormalSpace_of_hasAntitoneBasis : ∀ {α : Type u} [inst : UniformSpace α] {ι : Type u_1} [inst_1 : LinearOrder ι] {B : ι → SetRel α α},
  (uniformity α).HasAntitoneBasis B → CompletelyNormalSpace α
-- Init.Data.Array.Basic
/-- Low-level modification operator which is as fast as a C array write. The modification is performed
in-place when the reference to the array is unique.

This avoids overhead due to unboxing a `Nat` used as an index.
 -/
Array.uset : {α : Type u} → (xs : Array α) → (i : USize) → α → i.toNat < xs.size → Array α
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
/-- If `f` is monotone on `a..b`, then `f'` is interval integrable on `a..b` and the integral of
`f'` on `a..b` is in between `0` and `f b - f a`.  -/
MonotoneOn.intervalIntegral_deriv_mem_uIcc : ∀ {f : ℝ → ℝ} {a b : ℝ}, MonotoneOn f (Set.uIcc a b) → ∫ (x : ℝ) in a..b, deriv f x ∈ Set.uIcc 0 (f b - f a)
-- Mathlib.CategoryTheory.Sites.IsSheafFor
CategoryTheory.Presieve.isSheafFor_iff_bijective_shrinkFunctor_ι_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.LocallySmall.{w, v₁, u₁} C] {X : C}
  (S : CategoryTheory.Sieve X) (F : CategoryTheory.Functor Cᵒᵖ (Type w)),
  CategoryTheory.Presieve.IsSheafFor F S.arrows ↔
    Function.Bijective fun g =>
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Sieve.shrinkFunctor.{w, v₁, u₁} S).ι g
-- Mathlib.Algebra.Group.Subgroup.MulOpposite
AddSubgroup.equivOp_apply_coe : ∀ {G : Type u_2} [inst : AddGroup G] (H : AddSubgroup G) (a : ↥H), ↑(H.equivOp a) = AddOpposite.op ↑a
-- Init.Data.BitVec.Bitblast
/-- The current remainder.  -/
BitVec.DivModState.r : {w : ℕ} → BitVec.DivModState w → BitVec w
-- Mathlib.Algebra.Quaternion
Quaternion.coe_neg : ∀ {R : Type u_3} [inst : CommRing R] (x : R), ↑(-x) = -↑x
-- Mathlib.SetTheory.ZFC.Class
/-- Assert that `A` is a ZFC set satisfying `B`  -/
Class.ToSet : Class.{u} → Class.{u} → Prop
-- Init.Grind.Module.Basic
Lean.Grind.AddCommMonoid.mk : {M : Type u} →
  [toZero : Zero M] →
    [toAdd : Add M] →
      (∀ (a : M), a + 0 = a) →
        (∀ (a b : M), a + b = b + a) → (∀ (a b c : M), a + b + c = a + (b + c)) → Lean.Grind.AddCommMonoid M
-- Lean.Elab.App
/-- Main loop of the `elabAsElim` procedure.  -/
Lean.Elab.Term.ElabElim.main : Lean.Elab.Term.ElabElim.M Lean.Expr
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.minKeyD.match_1.eq_3 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → α → Sort u_3) (size : ℕ) (k : α)
  (v : β k) (size_1 : ℕ) (k_1 : α) (v_1 : β k_1) (l r r_1 : Std.DTreeMap.Internal.Impl α β) (fallback : α)
  (h_1 : (fallback : α) → motive Std.DTreeMap.Internal.Impl.leaf fallback)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (r : Std.DTreeMap.Internal.Impl α β) →
            (x : α) → motive (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r) x)
  (h_3 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l : Std.DTreeMap.Internal.Impl α β) →
            (size_2 : ℕ) →
              (k_2 : α) →
                (v_2 : β k_2) →
                  (l_1 r : Std.DTreeMap.Internal.Impl α β) →
                    l = Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_1 r →
                      (r_2 : Std.DTreeMap.Internal.Impl α β) →
                        (fallback : α) →
                          motive
                            (Std.DTreeMap.Internal.Impl.inner size k v
                              (Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_1 r) r_2)
                            fallback),
  (match Std.DTreeMap.Internal.Impl.inner size k v (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) r_1,
      fallback with
    | Std.DTreeMap.Internal.Impl.leaf, fallback => h_1 fallback
    | Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r, x => h_2 size k v r x
    | Std.DTreeMap.Internal.Impl.inner size k v (l@h:(Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_1 r)) r_2,
      fallback => h_3 size k v l size_2 k_2 v_2 l_1 r h r_2 fallback) =
    h_3 size k v (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) size_1 k_1 v_1 l r ⋯ r_1 fallback
-- Aesop.Rule.Name
Aesop.BuilderName.cases.sizeOf_spec : sizeOf Aesop.BuilderName.cases = 1
-- Mathlib.Tactic.FunProp.Types
/-- Get origin of the head function.  -/
Mathlib.Meta.FunProp.FunctionData.getFnOrigin : Mathlib.Meta.FunProp.FunctionData → Mathlib.Meta.FunProp.Origin
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.eTruncGE_obj_top : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C), t.eTruncGE.obj ⊤ = 0
-- Mathlib.Algebra.Polynomial.EraseLead
Polynomial.natDegree_eraseLead : ∀ {R : Type u_1} [inst : Semiring R] {f : Polynomial R}, f.nextCoeff ≠ 0 → f.eraseLead.natDegree = f.natDegree - 1
-- Std.Http.Internal.Char
_private.Std.Http.Internal.Char.0.Std.Http.Internal.Char.qdtext.match_1.splitter : (motive : Char → Sort u_1) →
  (c : Char) →
    (Unit → motive '\t') →
      (Unit → motive ' ') →
        (Unit → motive '!') →
          ((x : Char) → (x = '\t' → False) → (x = ' ' → False) → (x = '!' → False) → motive x) → motive c
-- Mathlib.Algebra.Module.Defs
instDistribSMul : {R : Type u_1} → [inst : NonUnitalNonAssocSemiring R] → DistribSMul R R
-- Mathlib.Data.Stream.Defs
/-- Prepend an element to a stream.  -/
Stream'.cons : {α : Type u} → α → Stream' α → Stream' α
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instIsTopologicalGroup : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : IsTopologicalGroup G],
  IsTopologicalGroup (SeparationQuotient G)
-- Init.Data.Int.Linear
Int.Internal.Linear.norm_dvd_gcd : ∀ (ctx : Int.Internal.Linear.Context) (k₁ : ℤ) (e₁ : Int.Internal.Linear.Expr) (k₂ : ℤ) (p₂ : Int.Internal.Linear.Poly)
  (g : ℤ),
  Int.Internal.Linear.norm_dvd_gcd_cert k₁ e₁ k₂ p₂ g = true →
    (k₁ ∣ Int.Internal.Linear.Expr.denote ctx e₁) = (k₂ ∣ Int.Internal.Linear.Poly.denote' ctx p₂)
-- Mathlib.Order.ConditionallyCompletePartialOrder.Basic
OrderDual.instConditionallyCompletePartialOrderInfOfConditionallyCompletePartialOrderSup : {α : Type u_1} → [ConditionallyCompletePartialOrderSup α] → ConditionallyCompletePartialOrderInf αᵒᵈ
-- Init.Data.Fin.Lemmas
Fin.ite_val : ∀ {n : ℕ} {c : Prop} [inst : Decidable c] {x : c → Fin n} (y : ¬c → Fin n),
  ↑(if h : c then x h else y h) = if h : c then ↑(x h) else ↑(y h)
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- This is a structure encapsulating the data necessary to define a `Multispan`.  -/
CategoryTheory.Limits.MultispanIndex : CategoryTheory.Limits.MultispanShape →
  (C : Type u) → [CategoryTheory.Category.{v, u} C] → Type (max (max (max u v) w) w')
-- Mathlib.Algebra.Group.Submonoid.Defs
AddSubmonoid.mem_inf : ∀ {M : Type u_1} [inst : AddZeroClass M] {p p' : AddSubmonoid M} {x : M}, x ∈ p ⊓ p' ↔ x ∈ p ∧ x ∈ p'
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get!_insertManyIfNewUnit_list : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α fun x => Unit} {l : List α} {k : α},
  Std.DHashMap.Raw.Const.get! (Std.DHashMap.Raw.Const.insertManyIfNewUnit m l) k = ()
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get?_eq_some_get!_of_contains : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : Inhabited β],
  t.WF →
    ∀ {a : α},
      Std.DTreeMap.Internal.Impl.contains a t = true →
        Std.DTreeMap.Internal.Impl.Const.get? t a = some (Std.DTreeMap.Internal.Impl.Const.get! t a)
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
_private.Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms.0.SimplexCategoryGenRel.standardσ.match_1.splitter : {m₁ m₂ : ℕ} →
  (motive : (L : List ℕ) → m₂ + L.length = m₁ → Sort u_1) →
    (L : List ℕ) →
      (h : m₂ + L.length = m₁) →
        ((h : m₂ + [].length = m₁) → motive [] h) →
          ((a : ℕ) → (t : List ℕ) → (h : m₂ + (a :: t).length = m₁) → motive (a :: t) h) → motive L h
-- Lean.Data.Lsp.Extra
Lean.Lsp.instFromJsonWaitForILeansParams : Lean.FromJson Lean.Lsp.WaitForILeansParams
-- Mathlib.Algebra.DualQuaternion
Quaternion.fst_imJ_dualNumberEquiv_symm : ∀ {R : Type u_1} [inst : CommRing R] (d : DualNumber (Quaternion R)),
  TrivSqZeroExt.fst (Quaternion.dualNumberEquiv.symm d).imJ = (TrivSqZeroExt.fst d).imJ
-- Lean.Data.OpenDecl
Lean.OpenDecl.simple.inj : ∀ {ns : Lean.Name} {except : List Lean.Name} {ns_1 : Lean.Name} {except_1 : List Lean.Name},
  Lean.OpenDecl.simple ns except = Lean.OpenDecl.simple ns_1 except_1 → ns = ns_1 ∧ except = except_1
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
/-- The class of morphisms that are of the form `toSucc X : X ⟶ succ X`.  -/
CategoryTheory.SmallObject.SuccStruct.prop : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.SmallObject.SuccStruct C → CategoryTheory.MorphismProperty C
-- Mathlib.SetTheory.Ordinal.Basic
Cardinal.ord_card_le : ∀ (o : Ordinal.{u_1}), o.card.ord ≤ o
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.IsBasis.exists_isBasis_inter_eq_of_superset : ∀ {α : Type u_1} {M : Matroid α} {I X Y : Set α},
  M.IsBasis I X →
    X ⊆ Y →
      autoParam (Y ⊆ M.E) Matroid.IsBasis.exists_isBasis_inter_eq_of_superset._auto_1 → ∃ J, M.IsBasis J Y ∧ J ∩ X = I
-- Mathlib.Analysis.Calculus.FDeriv.Add
DifferentiableAt.const_sub : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {x : E}, DifferentiableAt 𝕜 f x → ∀ (c : F), DifferentiableAt 𝕜 (fun y => c - f y) x
-- Mathlib.CategoryTheory.Subfunctor.Image
CategoryTheory.Subfunctor.range_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)}
  (G : CategoryTheory.Subfunctor F), CategoryTheory.Subfunctor.range G.ι = G
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.homOfLE_apply : ∀ {X : AlgebraicGeometry.Scheme} {U V : X.Opens} (e : U ≤ V) (x : ↥U), ↑((X.homOfLE e) x) = ↑x
-- Mathlib.Order.Filter.Basic
Filter.EventuallyLE.inf_le_of_right_le : ∀ {α : Type u} {β : Type v} [inst : SemilatticeInf β] {l : Filter α} {f g h : α → β}, g ≤ᶠ[l] h → f ⊓ g ≤ᶠ[l] h
-- Mathlib.Topology.VectorBundle.Basic
VectorBundle.continuousLinearEquivAt_symm_apply : ∀ (R : Type u_1) {B : Type u_2} (F : Type u_3) (E : B → Type u_4) [inst : NontriviallyNormedField R]
  [inst_1 : (x : B) → AddCommMonoid (E x)] [inst_2 : (x : B) → Module R (E x)] [inst_3 : NormedAddCommGroup F]
  [inst_4 : NormedSpace R F] [inst_5 : TopologicalSpace B] [inst_6 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_7 : (x : B) → TopologicalSpace (E x)] [inst_8 : FiberBundle F E] [inst_9 : VectorBundle R F E] (b : B) (y : F),
  (VectorBundle.continuousLinearEquivAt R F E b).symm y = (trivializationAt F E b).symm b y
-- Mathlib.Analysis.Normed.Algebra.Spectrum
/-- The map `a ↦ spectrum ℝ≥0 a` is upper hemicontinuous.  -/
upperHemicontinuous_spectrum_nnreal : ∀ (A : Type u_2) [inst : NormedRing A] [inst_1 : NormedAlgebra ℝ A] [CompleteSpace A],
  UpperHemicontinuous (spectrum NNReal)
-- Mathlib.Algebra.Polynomial.Reverse
Polynomial.coeff_one_reverse : ∀ {R : Type u_1} [inst : Semiring R] (f : Polynomial R), f.reverse.coeff 1 = f.nextCoeff
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
CategoryTheory.ihom.ev_coev : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (A B : C)
  [inst_2 : CategoryTheory.Closed A],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A ((CategoryTheory.ihom.coev A).app B))
      ((CategoryTheory.ihom.ev A).app (CategoryTheory.MonoidalCategoryStruct.tensorObj A B)) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj A B)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.self_le_maxKey?_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β} {kmi : α}, (t.insert k v).maxKey?.get ⋯ = kmi → (cmp k kmi).isLE = true
-- Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic
_private.Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic.0.ProbabilityTheory.HasIndepIncrements.indepFun_sub_sub.match_1_1.eq_3 : ∀ (motive : ℕ → Sort u_1) (x : ℕ) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1) (h_3 : (x : ℕ) → motive x),
  (x = 0 → False) →
    (x = 1 → False) →
      (match x with
        | 0 => h_1 ()
        | 1 => h_2 ()
        | x => h_3 x) =
        h_3 x
-- Init.Core
/-- `singleton x` is a collection with the single element `x` (notation: `{x}`). 

Conventions for notations in identifiers:

 * The recommended spelling of `{x}` in identifiers is `singleton`. -/
Singleton.singleton : {α : outParam (Type u)} → {β : Type v} → [self : Singleton α β] → α → β
-- Mathlib.Order.SymmDiff
bihimp_triangle : ∀ {α : Type u_2} [inst : GeneralizedHeytingAlgebra α] (a b c : α), bihimp a b ⊓ bihimp b c ≤ bihimp a c
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.LetRecToLift.mvarId : Lean.Elab.Term.LetRecToLift → Lean.MVarId
-- Mathlib.Logic.Unique
/-- `Option α` is a `Subsingleton` if and only if `α` is empty.  -/
Option.subsingleton_iff_isEmpty : ∀ {α : Type u}, Subsingleton (Option α) ↔ IsEmpty α
-- Mathlib.Analysis.Polynomial.MahlerMeasure
Polynomial.logMahlerMeasure_X_add_C : ∀ (z : ℂ), (Polynomial.X + Polynomial.C z).logMahlerMeasure = ‖z‖.posLog
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
PreQuasiregular.inv_add_add_mul_eq_zero : ∀ {R : Type u_1} [inst : NonUnitalSemiring R] (u : (PreQuasiregular R)ˣ),
  (↑u⁻¹).val + (↑u).val + (↑u).val * (↑u⁻¹).val = 0
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.topologicalSpace : {E : Type u_2} →
  {F : Type u_3} →
    [inst : NormedAddCommGroup E] →
      [inst_1 : NormedSpace ℝ E] →
        [inst_2 : NormedAddCommGroup F] →
          [inst_3 : NormedSpace ℝ F] →
            {n : ℕ∞} → {K : TopologicalSpace.Compacts E} → TopologicalSpace (ContDiffMapSupportedIn E F n K)
-- Mathlib.GroupTheory.CoprodI
/-- The empty reduced word.  -/
Monoid.CoprodI.Word.empty : {ι : Type u_1} → {M : ι → Type u_2} → [inst : (i : ι) → Monoid (M i)] → Monoid.CoprodI.Word M
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.map_comp_map : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  (f : R →+* S) (g : S →+* T) (p : Polynomial R) (q : Polynomial S) (r : Polynomial T) (hf : q ∣ Polynomial.map f p)
  (hg : r ∣ Polynomial.map g q),
  (AdjoinRoot.map g q r hg).comp (AdjoinRoot.map f p q hf) = AdjoinRoot.map (g.comp f) p r ⋯
-- Mathlib.Algebra.Group.Irreducible.Indecomposable
AddSubmonoid.mem_closure_image_pos_iff : ∀ {ι : Type u_1} {M : Type u_2} {S : Type u_4} [inst : AddMonoid M] [inst_1 : LinearOrder S] [inst_2 : AddCommMonoid S]
  [IsOrderedCancelAddMonoid S] (v : ι → M) (f : M →+ S) (i : ι),
  v i ≠ 0 → (v i ∈ AddSubmonoid.closure (v '' {i | 0 < f (v i)}) ↔ 0 < f (v i))
-- Mathlib.Order.Bounds.Basic
isLUB_lt_iff : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α} {a b : α}, IsLUB s a → (a < b ↔ ∃ c ∈ upperBounds s, c < b)
-- Mathlib.CategoryTheory.Monoidal.Action.End
CategoryTheory.MonoidalCategory.MonoidalRightAction.actionOfMonoidalFunctorToEndofunctor_actionUnitIso_inv : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  (F : CategoryTheory.Functor C (CategoryTheory.Functor D D)) [inst_3 : F.Monoidal] (d : D),
  (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso d).inv =
    (CategoryTheory.Functor.LaxMonoidal.ε F).app d
-- Mathlib.NumberTheory.Height.Basic
/-- The multiplicative height of the inverse of a field element `x`
is the same as the multiplicative height of `x`.  -/
Height.mulHeight₁_inv : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] (x : K),
  Height.mulHeight₁ x⁻¹ = Height.mulHeight₁ x
-- Mathlib.Analysis.InnerProductSpace.Basic
/-- If the inner product of two vectors is equal to the product of their norms (i.e.,
`⟪x, y⟫ = ‖x‖ * ‖y‖`), then the two vectors are nonnegative real multiples of each other. One form
of the equality case for Cauchy-Schwarz.
Compare `norm_inner_eq_norm_iff`, which takes the weaker hypothesis `abs ⟪x, y⟫ = ‖x‖ * ‖y‖`.  -/
inner_eq_norm_mul_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {x y : E}, inner 𝕜 x y = ↑‖x‖ * ↑‖y‖ ↔ ↑‖y‖ • x = ↑‖x‖ • y
-- Mathlib.SetTheory.Lists
Lists.atom.eq_1 : ∀ {α : Type u_1} (a : α), Lists.atom a = ⟨false, Lists'.atom a⟩
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.free_ext : ∀ (k : Type u) (G : Type v) [inst : CommRing k] [inst_1 : Monoid G] {α : Type u'} (A : Rep.{max (max u u') v, u, v} k G)
  (f g : Rep.free k G α ⟶ A),
  (∀ (i : α),
      ((Rep.Hom.hom f) fun₀ | i => MonoidAlgebra.single 1 1) = (Rep.Hom.hom g) fun₀ | i => MonoidAlgebra.single 1 1) →
    f = g
-- Std.Data.DHashMap.Internal.Raw
Std.DHashMap.Internal.Raw.filter_eq : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} (h : m.WF)
  {f : (a : α) → β a → Bool}, Std.DHashMap.Raw.filter f m = ↑(Std.DHashMap.Internal.Raw₀.filter f ⟨m, ⋯⟩)
-- Mathlib.Analysis.LocallyConvex.StrongTopology
ContinuousLinearMap.instLocallyConvexSpace : ∀ {R : Type u_1} {𝕜₁ : Type u_2} {𝕜₂ : Type u_3} {E : Type u_4} {F : Type u_5} [inst : AddCommGroup E]
  [inst_1 : TopologicalSpace E] [inst_2 : AddCommGroup F] [inst_3 : TopologicalSpace F]
  [inst_4 : IsTopologicalAddGroup F] [inst_5 : Semiring R] [inst_6 : PartialOrder R] [inst_7 : NormedField 𝕜₁]
  [inst_8 : NormedField 𝕜₂] [inst_9 : Module 𝕜₁ E] [inst_10 : Module 𝕜₂ F] {σ : 𝕜₁ →+* 𝕜₂} [inst_11 : Module R F]
  [inst_12 : ContinuousConstSMul R F] [LocallyConvexSpace R F] [inst_14 : SMulCommClass 𝕜₂ R F],
  LocallyConvexSpace R (E →SL[σ] F)
-- Aesop.Util.EqualUpToIds
Aesop.instMonadEqualUpToIdsM : Monad Aesop.EqualUpToIdsM
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
CategoryTheory.IsPushout.inr_isoPushout_inv_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P}
  {inr : Y ⟶ P} (h : CategoryTheory.IsPushout f g inl inr) [inst_1 : CategoryTheory.Limits.HasPushout f g] {Z_1 : C}
  (h_1 : P ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr f g)
      (CategoryTheory.CategoryStruct.comp h.isoPushout.inv h_1) =
    CategoryTheory.CategoryStruct.comp inr h_1
-- Mathlib.Data.Finsupp.Interval
Finsupp.card_Icc : ∀ {ι : Type u_1} {α : Type u_2} [inst : PartialOrder α] [inst_1 : Zero α] [inst_2 : LocallyFiniteOrder α]
  [inst_3 : DecidableEq ι] [inst_4 : DecidableEq α] (f g : ι →₀ α),
  (Finset.Icc f g).card = ∏ i ∈ f.support ∪ g.support, (Finset.Icc (f i) (g i)).card
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
/-- The additive equivalence `(K⟦n⟧) ⟶ L ≃+ Cocycle K L m` when `m + n = 0`.  -/
CochainComplex.HomComplex.Cocycle.equivHomShift' : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {K L : CochainComplex C ℤ} →
        (n m : ℤ) →
          m + n = 0 →
            ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K ⟶ L) ≃+ CochainComplex.HomComplex.Cocycle K L m
-- Mathlib.Data.Nat.MaxPowDiv
/-- **Alias** of `padicValNat`.

---

For `p ≠ 1`, the `p`-adic valuation of a natural `n ≠ 0` is the largest natural number `k` such
that `p^k` divides `n`. If `n = 0` or `p = 1`, then `padicValNat p n` defaults to `0`.  -/
Nat.maxPowDiv : ℕ → ℕ → ℕ
-- Mathlib.Topology.MetricSpace.ProperSpace.Real
NNReal.instProperSpace : ProperSpace NNReal
-- Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily
/-- The induced condition on presieves in `C`, given by a pre-`0`-hypercover family.  -/
CategoryTheory.PreZeroHypercoverFamily.presieve : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.PreZeroHypercoverFamily C → {X : C} → CategoryTheory.Presieve X → Prop
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
/-- If `A.det` has a constructive inverse, produce one for `A`.  -/
Matrix.invertibleOfDetInvertible : {n : Type u'} →
  {α : Type v} →
    [inst : Fintype n] →
      [inst_1 : DecidableEq n] → [inst_2 : CommRing α] → (A : Matrix n n α) → [Invertible A.det] → Invertible A
-- Mathlib.Tactic.Abel
/-- Apply the function `n : ∀ {α} [AddComm{Monoid,Group} α]` to the given list of arguments.

Will use the `AddComm{Monoid,Group}` instance that has been cached in the context.
 -/
Mathlib.Tactic.Abel.iapp : Lean.Name → Array Lean.Expr → Mathlib.Tactic.Abel.M Lean.Expr
-- Mathlib.Algebra.Order.Group.Synonym
toDual_neg : ∀ {α : Type u_1} [inst : Neg α] (a : α), OrderDual.toDual (-a) = -OrderDual.toDual a
-- Init.Internal.Order.Basic
/-- A “less-or-equal-to” or “approximates” relation.

This is intended to be used in the construction of `partial_fixpoint`, and not meant to be used otherwise.
 -/
Lean.Order.«term_⊑_» : Lean.TrailingParserDescr
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.rename_toMvPolynomial : ∀ {R : Type u_1} {σ : Type u_3} {τ : Type u_4} [inst : CommSemiring R] (f : σ → τ) (a : σ) (p : Polynomial R),
  (MvPolynomial.rename f) ((Polynomial.toMvPolynomial a) p) = (Polynomial.toMvPolynomial (f a)) p
-- Mathlib.Topology.Sheaves.Stalks
TopCat.Presheaf.pullbackPushforwardAdjunction_unit_app_app_germToPullbackStalk : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X Y : TopCat}
  (f : X ⟶ Y) (F : TopCat.Presheaf C Y) (V : (TopologicalSpace.Opens ↑Y)ᵒᵖ) (x : ↑X)
  (hx : (CategoryTheory.ConcreteCategory.hom f) x ∈ Opposite.unop V),
  CategoryTheory.CategoryStruct.comp (((TopCat.Presheaf.pullbackPushforwardAdjunction C f).unit.app F).app V)
      (TopCat.Presheaf.germToPullbackStalk C f F ((TopologicalSpace.Opens.map f).obj (Opposite.unop V)) x hx) =
    F.germ (Opposite.unop V) ((CategoryTheory.ConcreteCategory.hom f) x) hx