mathlib-initiative/mathlib-types huggingface dataset:
-- Batteries.Recycling.RBTree.Basic
/-- `modify cut f t` uses `cut` to find an element,
then modifies the element using `f` and reinserts it into the tree.

Because the tree structure is not modified,
`f` must not modify the ordering properties of the element.

The element in `t` is used linearly if `t` is unshared.
 -/
RBTree.RBNode.modify : {α : Type u_1} → (α → Ordering) → (α → α) → RBTree.RBNode α → RBTree.RBNode α
-- Mathlib.FieldTheory.Separable
Polynomial.nodup_of_separable_prod : ∀ {R : Type u} [inst : CommRing R] [Nontrivial R] {s : Multiset R},
  (Multiset.map (fun a => Polynomial.X - Polynomial.C a) s).prod.Separable → s.Nodup
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instAddCommGroup.eq_1 : ∀ {α : Type u_1} [inst : AddCommGroup α], Lex.instAddCommGroup = { toAddGroup := Lex.instAddGroup, add_comm := ⋯ }
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.preservesZeroMorphisms_π₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C],
  CategoryTheory.ShortComplex.π₁.PreservesZeroMorphisms
-- Mathlib.Geometry.Manifold.Sheaf.Smooth
/-- The presheaf of smooth functions from `M` to `A`, for `A` an abelian Lie group, as a
presheaf of abelian groups.  -/
smoothPresheafCommGroup : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {EM : Type u_2} →
      [inst_1 : NormedAddCommGroup EM] →
        [inst_2 : NormedSpace 𝕜 EM] →
          {HM : Type u_3} →
            [inst_3 : TopologicalSpace HM] →
              ModelWithCorners 𝕜 EM HM →
                {E : Type u_4} →
                  [inst_4 : NormedAddCommGroup E] →
                    [inst_5 : NormedSpace 𝕜 E] →
                      {H : Type u_5} →
                        [inst_6 : TopologicalSpace H] →
                          (I : ModelWithCorners 𝕜 E H) →
                            (M : Type u) →
                              [inst_7 : TopologicalSpace M] →
                                [ChartedSpace HM M] →
                                  (A : Type u) →
                                    [inst_9 : TopologicalSpace A] →
                                      [inst_10 : ChartedSpace H A] →
                                        [inst_11 : CommGroup A] →
                                          [LieGroup I (↑⊤) A] → TopCat.Presheaf CommGrpCat (TopCat.of M)
-- Mathlib.CategoryTheory.Pi.Basic
_private.Mathlib.CategoryTheory.Pi.Basic.0.CategoryTheory.Pi.optionEquivalence.match_1.eq_1 : ∀ {J : Type u_1} (motive : Option J → Sort u_2) (h_1 : Unit → motive none) (h_2 : (i : J) → motive (some i)),
  (match none with
    | none => h_1 ()
    | some i => h_2 i) =
    h_1 ()
-- Mathlib.SetTheory.Ordinal.Basic
/-- For `Ordinal`:

* less-equal is defined such that well orders `r` and `s` satisfy `type r ≤ type s` if there exists
  a function embedding `r` as an *initial* segment of `s`.
* less-than is defined such that well orders `r` and `s` satisfy `type r < type s` if there exists
  a function embedding `r` as a *principal* segment of `s`.

Note that most of the relevant results on initial and principal segments are proved in the
`Mathlib/Order/InitialSeg.lean` file.
 -/
Ordinal.partialOrder : PartialOrder Ordinal.{u_1}
-- Mathlib.RingTheory.Coprime.Basic
IsCoprime.of_mul_add_right_left : ∀ {R : Type u} [inst : CommSemiring R] {x y z : R}, IsCoprime (z * y + x) y → IsCoprime x y
-- Lean.Elab.Calc
Lean.Elab.Term.CalcStepView.mk.injEq : ∀ (ref : Lean.Syntax) (term proof : Lean.Term) (ref_1 : Lean.Syntax) (term_1 proof_1 : Lean.Term),
  ({ ref := ref, term := term, proof := proof } = { ref := ref_1, term := term_1, proof := proof_1 }) =
    (ref = ref_1 ∧ term = term_1 ∧ proof = proof_1)
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.coe_prodMap : ∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} {V3 : Type u_6} {P3 : Type u_7}
  {V4 : Type u_8} {P4 : Type u_9} [inst : Ring k] [inst_1 : AddCommGroup V1] [inst_2 : Module k V1]
  [inst_3 : AddTorsor V1 P1] [inst_4 : AddCommGroup V2] [inst_5 : Module k V2] [inst_6 : AddTorsor V2 P2]
  [inst_7 : AddCommGroup V3] [inst_8 : Module k V3] [inst_9 : AddTorsor V3 P3] [inst_10 : AddCommGroup V4]
  [inst_11 : Module k V4] [inst_12 : AddTorsor V4 P4] (f : P1 →ᵃ[k] P2) (g : P3 →ᵃ[k] P4),
  ⇑(f.prodMap g) = Prod.map ⇑f ⇑g
-- Mathlib.Algebra.Category.GrpWithZero
GrpWithZero.instInhabited : Inhabited GrpWithZero
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Adjunction.Coalgebra.homEquiv_naturality_str_symm : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C C} (adj : F ⊣ G)
  (V₁ V₂ : CategoryTheory.Endofunctor.Coalgebra G) (f : V₁ ⟶ V₂),
  CategoryTheory.CategoryStruct.comp (F.map f.f) ((adj.homEquiv V₂.V V₂.V).symm V₂.str) =
    CategoryTheory.CategoryStruct.comp ((adj.homEquiv V₁.V V₁.V).symm V₁.str) f.f
-- Mathlib.RepresentationTheory.Action
Representation.LinearizeMonoidal.μ_rightUnitor : ∀ {G : Type v} [inst : Monoid G] (X : Action (Type w) G) {k : Type u} [inst_1 : CommSemiring k],
  ↑(Representation.TensorProduct.rid k (Representation.linearize k G X)) =
    ((Representation.linearizeMap (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom).comp
          (Representation.LinearizeMonoidal.μ X
            (CategoryTheory.MonoidalCategoryStruct.tensorUnit (Action (Type w) G)))).comp
      (Representation.IntertwiningMap.lTensor (Representation.linearize k G X) (Representation.LinearizeMonoidal.ε k G))
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
/-- The points of a face of a simplex are given by `mono_of_fin`.  -/
Affine.Simplex.face_points' : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_5} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {n : ℕ} (s : Affine.Simplex k P n) {fs : Finset (Fin (n + 1))} {m : ℕ} (h : fs.card = m + 1),
  (s.face h).points = s.points ∘ ⇑(fs.orderEmbOfFin h)
-- Mathlib.Algebra.GroupWithZero.Action.Defs
DistribSMul.ext : ∀ {M : Type u_12} {A : Type u_13} {inst : AddZeroClass A} {x y : DistribSMul M A}, SMul.smul = SMul.smul → x = y
-- Std.Async.Basic
/-- Creates an `EAsync` computation that awaits the completion of the given `ETask ε α`.
 -/
Std.Async.EAsync.await : {ε α : Type} → Std.Async.ETask ε α → Std.Async.EAsync ε α
-- Std.Data.HashSet.Basic
/-- Compares two hash sets using Boolean equality on keys.

Returns `true` if the sets contain the same keys, `false` otherwise.
 -/
Std.HashSet.beq : {α : Type u} → {x : Hashable α} → [inst : BEq α] → Std.HashSet α → Std.HashSet α → Bool
-- Mathlib.CategoryTheory.Triangulated.SpectralObject
CategoryTheory.Triangulated.SpectralObject.triangle_mor₁ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Limits.HasZeroObject C]
  [inst_3 : CategoryTheory.HasShift C ℤ] [inst_4 : CategoryTheory.Preadditive C]
  [inst_5 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_6 : CategoryTheory.Pretriangulated C]
  (X : CategoryTheory.Triangulated.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k),
  (X.triangle f g).mor₁ =
    X.ω₁.map (CategoryTheory.ComposableArrows.twoδ₂Toδ₁ f g (CategoryTheory.CategoryStruct.comp f g) ⋯)
-- Lean.Meta.Tactic.Grind.EMatch
Lean.Meta.Grind.EMatch.Cnstr.offset.inj : ∀ {gen? : Option Lean.Meta.Grind.GenPatternInfo} {pat : Lean.Expr} {k : ℕ} {e : Lean.Expr}
  {gen?_1 : Option Lean.Meta.Grind.GenPatternInfo} {pat_1 : Lean.Expr} {k_1 : ℕ} {e_1 : Lean.Expr},
  Lean.Meta.Grind.EMatch.Cnstr.offset gen? pat k e = Lean.Meta.Grind.EMatch.Cnstr.offset gen?_1 pat_1 k_1 e_1 →
    gen? = gen?_1 ∧ pat = pat_1 ∧ k = k_1 ∧ e = e_1
-- Mathlib.CategoryTheory.Sites.LocalSite
/-- Every category with a terminal object becomes a local site with the trivial topology.  -/
CategoryTheory.GrothendieckTopology.IsLocalSite.instTrivialOfHasTerminal : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C],
  (CategoryTheory.GrothendieckTopology.trivial C).IsLocalSite
-- Mathlib.Algebra.Algebra.Unitization
Unitization.instStarRing : {R : Type u_1} →
  {A : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : StarRing R] →
        [inst_2 : NonUnitalNonAssocSemiring A] →
          [inst_3 : StarRing A] → [inst_4 : Module R A] → [StarModule R A] → StarRing (Unitization R A)
-- Init.Data.Range.Polymorphic.Lemmas
Std.Ric.mem_succ_iff : ∀ {α : Type u} [inst : LE α] [DecidableLE α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [Std.PRange.LinearlyUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α]
  [inst_5 : Std.PRange.InfinitelyUpwardEnumerable α] [Std.Rxc.IsAlwaysFinite α] [Std.PRange.LawfulUpwardEnumerable α]
  {hi a : α}, (a ∈ *...=Std.PRange.succ hi) ↔ (a ∈ *...=hi) ∨ a = Std.PRange.succ hi
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.le_beth_ord : ∀ (c : Cardinal.{u_1}), c ≤ Cardinal.beth c.ord
-- Mathlib.Data.List.Indexes
_private.Mathlib.Data.List.Indexes.0.List.mapIdxMAux'.match_1.eq_2 : ∀ {α : Type u_1} (motive : ℕ → List α → Sort u_2) (i : ℕ) (a : α) (as : List α) (h_1 : (x : ℕ) → motive x [])
  (h_2 : (i : ℕ) → (a : α) → (as : List α) → motive i (a :: as)),
  (match i, a :: as with
    | x, [] => h_1 x
    | i, a :: as => h_2 i a as) =
    h_2 i a as
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1.Stmt.load.injEq : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} (a : Γ → σ → σ) (a_1 : Turing.TM1.Stmt Γ Λ σ) (a_2 : Γ → σ → σ)
  (a_3 : Turing.TM1.Stmt Γ Λ σ), (Turing.TM1.Stmt.load a a_1 = Turing.TM1.Stmt.load a_2 a_3) = (a = a_2 ∧ a_1 = a_3)
-- Mathlib.Data.Set.Finite.Basic
/-- If `(Set.univ : Set α)` is finite then `α` is a finite type.  -/
Set.fintypeOfFiniteUniv : {α : Type u} → Set.univ.Finite → Fintype α
-- Mathlib.Combinatorics.SimpleGraph.Hamiltonian
SimpleGraph.Walk.not_isHamiltonian_of_infinite : ∀ {α : Type u_1} [inst : DecidableEq α] {G : SimpleGraph α} {a b : α} {p : G.Walk a b} [h : Infinite α],
  ¬p.IsHamiltonian
-- Mathlib.Analysis.Normed.Module.Ball.Homeomorph
Homeomorph.coe_unitBall_apply_zero : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E], ↑(Homeomorph.unitBall 0) = 0
-- Batteries.Util.ProofWanted
/-- If `true`, the wanted declaration is an `instance_wanted`: the recorded payload must
be a typeclass, the `Try this:` fallback is `instance`, and the declared name is registered
in `wantedInstancesExt` so subsequent wanted decls auto-include it.  -/
_private.Batteries.Util.ProofWanted.0.WantedCmdKind.isInstance : WantedCmdKind✝ → Bool
-- Mathlib.Topology.Compactification.OnePoint.Basic
/-- Extend a map `f : X → Y` to a map `OnePoint X → OnePoint Y`
by sending infinity to infinity.  -/
OnePoint.map : {X : Type u_1} → {Y : Type u_2} → (X → Y) → OnePoint X → OnePoint Y
-- Mathlib.Algebra.Homology.DerivedCategory.Plus
DerivedCategory.Plus.instShiftSequenceHomologyFunctorOfNatInt : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [inst_2 : HasDerivedCategory C] → (DerivedCategory.Plus.homologyFunctor C 0).ShiftSequence ℤ
-- Mathlib.Topology.EMetricSpace.Diam
/-- **Alias** of `Metric.ediam_image_le_iff`. -/
EMetric.diam_image_le_iff : ∀ {α : Type u_1} {X : Type u_2} [inst : PseudoEMetricSpace X] {d : ENNReal} {f : α → X} {s : Set α},
  Metric.ediam (f '' s) ≤ d ↔ ∀ x ∈ s, ∀ y ∈ s, edist (f x) (f y) ≤ d
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Unitization.val_inv_unitsFstOne_mulEquiv_quasiregular_apply : ∀ (R : Type u_1) {A : Type u_2} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A] (x : ↥(Unitization.unitsFstOne R A)),
  ↑((Unitization.unitsFstOne_mulEquiv_quasiregular R) x)⁻¹ = PreQuasiregular.equiv (↑↑x⁻¹).toProd.2
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.mem_cons_iff : ∀ {α : Type u} (s : Stream'.WSeq α) (b : α) {a : α}, a ∈ Stream'.WSeq.cons b s ↔ a = b ∨ a ∈ s
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
CategoryTheory.RegularMono.mk.injEq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f : X ⟶ Y} (Z : C) (left right : Y ⟶ Z)
  (w :
    autoParam (CategoryTheory.CategoryStruct.comp f left = CategoryTheory.CategoryStruct.comp f right)
      CategoryTheory.RegularMono.w._autoParam)
  (isLimit : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fork.ofι f w)) (Z_1 : C) (left_1 right_1 : Y ⟶ Z_1)
  (w_1 :
    autoParam (CategoryTheory.CategoryStruct.comp f left_1 = CategoryTheory.CategoryStruct.comp f right_1)
      CategoryTheory.RegularMono.w._autoParam)
  (isLimit_1 : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fork.ofι f w_1)),
  ({ Z := Z, left := left, right := right, w := w, isLimit := isLimit } =
      { Z := Z_1, left := left_1, right := right_1, w := w_1, isLimit := isLimit_1 }) =
    (Z = Z_1 ∧ left ≍ left_1 ∧ right ≍ right_1 ∧ isLimit ≍ isLimit_1)
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
MonoidAlgebra.mapDomainRingHom_apply : ∀ (R : Type u_3) {M : Type u_6} {N : Type u_7} [inst : Semiring R] [inst_1 : Monoid M] [inst_2 : Monoid N] (f : M →* N)
  (x : MonoidAlgebra R M), (MonoidAlgebra.mapDomainRingHom R f) x = MonoidAlgebra.mapDomain (⇑f) x
-- Mathlib.FieldTheory.Extension
IntermediateField.Lifts.carrier_union : ∀ {F : Type u_1} {E : Type u_2} {K : Type u_3} [inst : Field F] [inst_1 : Field E] [inst_2 : Field K]
  [inst_3 : Algebra F E] [inst_4 : Algebra F K] (c : Set (IntermediateField.Lifts F E K))
  (hc : IsChain (fun x1 x2 => x1 ≤ x2) c), (IntermediateField.Lifts.union c hc).carrier = ⨆ i, (↑i).carrier
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem?_unitOfList : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List α} {k : α},
  (Std.HashMap.unitOfList l)[k]? = if l.contains k = true then some () else none
-- Batteries.Tactic.Lint.Frontend
Batteries.Tactic.Lint.LintVerbosity.ofNat_ctorIdx : ∀ (x : Batteries.Tactic.Lint.LintVerbosity), Batteries.Tactic.Lint.LintVerbosity.ofNat x.ctorIdx = x
-- Mathlib.GroupTheory.FiniteAbelian.Duality
_private.Mathlib.GroupTheory.FiniteAbelian.Duality.0.CommGroup.dvd_exponent : ∀ {ι : Type u_1} {G : Type u_2} [inst : Monoid G] {n : ι → ℕ} (e : G ≃* ((i : ι) → Multiplicative (ZMod (n i))))
  (i : ι), n i ∣ Monoid.exponent G
-- Mathlib.Order.Category.Preord
/-- The embedding of `Preord` into `Cat`.
 -/
preordToCat : CategoryTheory.Functor Preord CategoryTheory.Cat
-- Mathlib.Analysis.InnerProductSpace.PiL2
OrthonormalBasis.reindex_toBasis : ∀ {ι : Type u_1} {ι' : Type u_2} {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι] [inst_4 : Fintype ι'] (b : OrthonormalBasis ι 𝕜 E) (e : ι ≃ ι'),
  (b.reindex e).toBasis = b.toBasis.reindex e
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.NonUnitalStarRing.of_f : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι]
  [inst_4 : (i : ι) → NonUnitalNonAssocSemiring (G i)]
  [inst_5 : ∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)] [inst_6 : (i : ι) → StarRing (G i)]
  [inst_7 : ∀ (i j : ι) (h : i ≤ j), StarHomClass (T h) (G i) (G j)] [inst_8 : Nonempty ι] {i j : ι} (hij : i ≤ j)
  (x : G i), (DirectLimit.NonUnitalStarRing.of G f j) ((f i j hij) x) = (DirectLimit.NonUnitalStarRing.of G f i) x
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.Proof.hyp.inj : ∀ {n n_1 : Lean.Name}, Mathlib.Tactic.ITauto.Proof.hyp n = Mathlib.Tactic.ITauto.Proof.hyp n_1 → n = n_1
-- Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_δ₀' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (K : ChainComplex C ℕ) {Δ Δ' : SimplexCategory} (i : Δ' ⟶ Δ) [inst_2 : CategoryTheory.Mono i],
  AlgebraicTopology.DoldKan.Isδ₀ i → AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono K i = K.d Δ.len Δ'.len
-- Mathlib.SetTheory.ZFC.Class
/-- Function value  -/
Class.«term_′_» : Lean.TrailingParserDescr
-- Init.Data.SInt.Lemmas
Int8.two_mul : ∀ {a : Int8}, 2 * a = a + a
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey!_insertManyIfNewUnit_list_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α Unit} [EquivBEq α] [LawfulHashable α]
  [inst : Inhabited α] {l : List α} {k : α}, k ∈ m → (m.insertManyIfNewUnit l).getKey! k = m.getKey! k
-- Std.Internal.Do.Order.Lemmas
Std.Internal.Do.CompleteLattice.meet_le_meet_of_le_himp : ∀ {l : Type u} [inst : Lean.Order.CompleteLattice l] {P P' Q Q' : l}
  [∀ (a : l), Lean.Order.PreservesSup (Lean.Order.meet a)],
  Lean.Order.PartialOrder.rel P P' →
    Lean.Order.PartialOrder.rel Q (Lean.Order.himp P' Q') →
      Lean.Order.PartialOrder.rel (Lean.Order.meet P Q) (Lean.Order.meet P' Q')
-- Mathlib.NumberTheory.ModularForms.Basic
CuspForm.mk.sizeOf_spec : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} (toSlashInvariantForm : SlashInvariantForm Γ k)
  (holo' : MDiff ⇑toSlashInvariantForm)
  (zero_at_cusps' : ∀ {c : OnePoint ℝ}, IsCusp c Γ → c.IsZeroAt toSlashInvariantForm.toFun k),
  sizeOf { toSlashInvariantForm := toSlashInvariantForm, holo' := holo', zero_at_cusps' := zero_at_cusps' } =
    1 + sizeOf toSlashInvariantForm
-- Mathlib.Data.Multiset.Filter
/-- `filterMap f s` is a combination filter/map operation on `s`.
The function `f : α → Option β` is applied to each element of `s`;
if `f a` is `some b` then `b` is added to the result, otherwise
`a` is removed from the resulting multiset.  -/
Multiset.filterMap : {α : Type u_1} → {β : Type v} → (α → Option β) → Multiset α → Multiset β
-- Mathlib.Data.NNReal.Defs
NNReal.zero_le_coe : ∀ {q : NNReal}, 0 ≤ ↑q
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.Scheme.isoSpec_inv_naturality : ∀ {X Y : AlgebraicGeometry.Scheme} [inst : AlgebraicGeometry.IsAffine X] [inst_1 : AlgebraicGeometry.IsAffine Y]
  (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.Hom.appTop f))
      Y.isoSpec.inv =
    CategoryTheory.CategoryStruct.comp X.isoSpec.inv f
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Matrix.SpecialLinearGroup.diag2_mul_inv : ∀ {F : Type u_1} [inst : Field F] (a : F) (ha : a ≠ 0),
  Matrix.SpecialLinearGroup.diag2 a ha * Matrix.SpecialLinearGroup.diag2 a⁻¹ ⋯ = 1
-- Mathlib.MeasureTheory.Integral.Average
/-- **First moment method**. The maximum of a measurable function is greater than its mean.  -/
MeasureTheory.exists_laverage_le : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal},
  μ ≠ 0 → ∫⁻ (a : α), f a ∂μ ≠ ⊤ → ∃ x, ⨍⁻ (a : α), f a ∂μ ≤ f x
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVUnOp.eval_arithShiftRightConst : ∀ {n w : ℕ}, (Std.Tactic.BVDecide.BVUnOp.arithShiftRightConst n).eval = fun x => x.sshiftRight n
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.Triangle.functorHomMk'_app_hom₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ] {J : Type u_1}
  [inst_2 : CategoryTheory.Category.{v_1, u_1} J] {obj₁ obj₂ obj₃ : CategoryTheory.Functor J C} {mor₁ : obj₁ ⟶ obj₂}
  {mor₂ : obj₂ ⟶ obj₃} {mor₃ : obj₃ ⟶ obj₁.comp (CategoryTheory.shiftFunctor C 1)}
  {obj₁' obj₂' obj₃' : CategoryTheory.Functor J C} {mor₁' : obj₁' ⟶ obj₂'} {mor₂' : obj₂' ⟶ obj₃'}
  {mor₃' : obj₃' ⟶ obj₁'.comp (CategoryTheory.shiftFunctor C 1)} (hom₁ : obj₁ ⟶ obj₁') (hom₂ : obj₂ ⟶ obj₂')
  (hom₃ : obj₃ ⟶ obj₃')
  (comm₁ : CategoryTheory.CategoryStruct.comp mor₁ hom₂ = CategoryTheory.CategoryStruct.comp hom₁ mor₁')
  (comm₂ : CategoryTheory.CategoryStruct.comp mor₂ hom₃ = CategoryTheory.CategoryStruct.comp hom₂ mor₂')
  (comm₃ :
    CategoryTheory.CategoryStruct.comp mor₃
        (CategoryTheory.Functor.whiskerRight hom₁ (CategoryTheory.shiftFunctor C 1)) =
      CategoryTheory.CategoryStruct.comp hom₃ mor₃')
  (j : J),
  ((CategoryTheory.Pretriangulated.Triangle.functorHomMk' hom₁ hom₂ hom₃ comm₁ comm₂ comm₃).app j).hom₂ = hom₂.app j
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
/-- The `v`-adic absolute value on `R` defined as `b` raised to negative `v`-adic
valuation, for some `b` in `ℝ≥0`  -/
IsDedekindDomain.HeightOneSpectrum.intAdicAbv : {R : Type u_1} →
  [inst : CommRing R] →
    [IsDedekindDomain R] → IsDedekindDomain.HeightOneSpectrum R → {b : NNReal} → 1 < b → AbsoluteValue R ℝ
-- Mathlib.Topology.UniformSpace.UniformConvergence
/-- Uniform convergence implies pointwise convergence.  -/
TendstoUniformlyOn.tendsto_at : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α} {x : α}
  {p : Filter ι}, TendstoUniformlyOn F f p s → x ∈ s → Filter.Tendsto (fun n => F n x) p (nhds (f x))
-- Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.SimplexAlgorithm
Mathlib.Tactic.Linarith.SimplexAlgorithm.SimplexAlgorithmException.noConfusionType : Sort v✝ →
  Mathlib.Tactic.Linarith.SimplexAlgorithm.SimplexAlgorithmException →
    Mathlib.Tactic.Linarith.SimplexAlgorithm.SimplexAlgorithmException → Sort v✝
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.cos_periodic : Function.Periodic Real.cos (2 * Real.pi)
-- Mathlib.Data.Sum.Order
OrderIso.sumCongr_apply : ∀ {α₁ : Type u_4} {α₂ : Type u_5} {β₁ : Type u_6} {β₂ : Type u_7} [inst : LE α₁] [inst_1 : LE α₂] [inst_2 : LE β₁]
  [inst_3 : LE β₂] (ea : α₁ ≃o α₂) (eb : β₁ ≃o β₂) (a : α₁ ⊕ β₁), (ea.sumCongr eb) a = Sum.map (⇑ea) (⇑eb) a
-- Mathlib.Algebra.Polynomial.Expand
/-- The opposite of `expand`: sends `∑ aₙ xⁿᵖ` to `∑ aₙ xⁿ`.  -/
Polynomial.contract : {R : Type u} → [inst : CommSemiring R] → ℕ → Polynomial R → Polynomial R
-- Mathlib.Topology.Order
inhabitedTopologicalSpace : {α : Type u} → Inhabited (TopologicalSpace α)
-- Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
IsSymmetricAlgebra.equiv_symm_comp : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {A : Type u_3}
  [inst_3 : CommSemiring A] [inst_4 : Algebra R A] {f : M →ₗ[R] A} (h : IsSymmetricAlgebra f),
  ↑(↑h.equiv).symm ∘ₗ f = SymmetricAlgebra.ι R M
-- Mathlib.LinearAlgebra.Matrix.Vec
Matrix.hadamard_kronecker_hadamard : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_4} {p : Type u_5} {R : Type u_3} [inst : CommSemigroup R]
  (A B : Matrix l m R) (C D : Matrix n p R),
  Matrix.kroneckerMap (fun x1 x2 => x1 * x2) (A.hadamard B) (C.hadamard D) =
    (Matrix.kroneckerMap (fun x1 x2 => x1 * x2) A C).hadamard (Matrix.kroneckerMap (fun x1 x2 => x1 * x2) B D)
-- Mathlib.Data.PFun
PFun.id_apply : ∀ {α : Type u_1} (a : α), PFun.id α a = Part.some a
-- Mathlib.Geometry.Manifold.Diffeomorph
Diffeomorph.apply_symm_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_4} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {H : Type u_5}
  [inst_5 : TopologicalSpace H] {G : Type u_7} [inst_6 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 F G} {M : Type u_9} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M] {N : Type u_11}
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} (h : Diffeomorph I J M N n) (x : N),
  h (h.symm x) = x
-- Mathlib.RingTheory.Derivation.MapCoeffs
Derivation.apply_aeval_eq' : ∀ {R : Type u_1} {A : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [inst_3 : AddCommGroup M] [inst_4 : Module A M] [inst_5 : Module R M] (d : Derivation R A M) {B : Type u_4}
  {M' : Type u_5} [inst_6 : CommRing B] [inst_7 : Algebra R B] [inst_8 : Algebra A B] [inst_9 : AddCommGroup M']
  [inst_10 : Module B M'] [inst_11 : Module R M'] [inst_12 : Module A M'] (d' : Derivation R B M') (f : M →ₗ[A] M'),
  (∀ (a : A), f (d a) = d' ((algebraMap A B) a)) →
    ∀ (x : B) (p : Polynomial A),
      d' ((Polynomial.aeval x) p) =
        (PolynomialModule.eval x) ((PolynomialModule.map B f) (d.mapCoeffs p)) +
          (Polynomial.aeval x) (Polynomial.derivative p) • d' x
-- Mathlib.Analysis.Normed.Group.Seminorm
NonarchAddGroupNorm.instPartialOrder : {E : Type u_3} → [inst : AddGroup E] → PartialOrder (NonarchAddGroupNorm E)