mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Filter.Bases.Basic
Filter.hasBasis_biInf_of_directed : ∀ {α : Type u_1} {ι : Type u_6} {ι' : Type u_7} {dom : Set ι},
  dom.Nonempty →
    ∀ {l : ι → Filter α} (s : ι → ι' → Set α) (p : ι → ι' → Prop),
      (∀ i ∈ dom, (l i).HasBasis (p i) (s i)) →
        DirectedOn (l ⁻¹'o GE.ge) dom →
          (⨅ i ∈ dom, l i).HasBasis (fun ii' => ii'.1 ∈ dom ∧ p ii'.1 ii'.2) fun ii' => s ii'.1 ii'.2
-- Lean.Meta.Sym.MaxFVar
/-- Returns the maximal free variable occurring in `e`.
This function assumes the current local context contains all free variables used in `e`.
 -/
Lean.Meta.Sym.getMaxFVar? : Lean.Expr → Lean.Meta.Sym.SymM (Option Lean.FVarId)
-- Mathlib.Analysis.Calculus.Deriv.Add
HasDerivAt.sub : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f g : 𝕜 → F} {f' g' : F} {x : 𝕜},
  HasDerivAt f f' x → HasDerivAt g g' x → HasDerivAt (f - g) (f' - g') x
-- Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
/-- `R` is integrally closed iff it is the integral closure of itself in its field of fractions.  -/
isIntegrallyClosed_iff_isIntegrallyClosedIn : ∀ {R : Type u_1} [inst : CommRing R] (K : Type u_4) [inst_1 : CommRing K] [inst_2 : Algebra R K] [IsFractionRing R K],
  IsIntegrallyClosed R ↔ IsIntegrallyClosedIn R K
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Affine.Simplex.closedInterior_eq_singleton : ∀ {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] [inst_4 : PartialOrder k] [ZeroLEOneClass k] (s : Affine.Simplex k P 0),
  s.closedInterior = {s.points 0}
-- Mathlib.Order.Filter.Bases.Finite
/-- The smallest filter basis containing a given collection of sets.  -/
Filter.FilterBasis.ofSets : {α : Type u_1} → Set (Set α) → FilterBasis α
-- Mathlib.Topology.Bornology.BoundedOperation
isBounded_add : ∀ {R : Type u_1} [inst : Bornology R] [inst_1 : Add R] [BoundedAdd R] {s t : Set R},
  Bornology.IsBounded s → Bornology.IsBounded t → Bornology.IsBounded (s + t)
-- Mathlib.Analysis.InnerProductSpace.Trace
LinearMap.IsSymmetric.trace_eq_sum_eigenvalues : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : FiniteDimensional 𝕜 E] {n : ℕ} (hn : Module.finrank 𝕜 E = n) {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric),
  (LinearMap.trace 𝕜 E) T = ↑(∑ i, hT.eigenvalues hn i)
-- Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
Multiplicative.toAdd_le : ∀ {α : Type u_1} [inst : Preorder α] {a b : Multiplicative α}, Multiplicative.toAdd a ≤ Multiplicative.toAdd b ↔ a ≤ b
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.WF.mergeWith! : ∀ {α : Type u} {β : α → Type v} {x : Ord α} [inst : Std.LawfulEqOrd α] {mergeFn : (a : α) → β a → β a → β a}
  {t₁ t₂ : Std.DTreeMap.Internal.Impl α β}, t₁.WF → (Std.DTreeMap.Internal.Impl.mergeWith! mergeFn t₁ t₂).WF
-- Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
NumberField.isTotallyReal_iSup : ∀ {K : Type u_2} [inst : Field K] [inst_1 : CharZero K] [Algebra.IsAlgebraic ℚ K] {ι : Type u_3} {k : ι → Subfield K}
  [∀ (i : ι), NumberField.IsTotallyReal ↥(k i)], NumberField.IsTotallyReal ↥(⨆ i, k i)
-- Mathlib.CategoryTheory.Limits.WeakLimits.WeakPullbacks
/-- If `t` is a weak limit pullback cone over `f` and `g` and `h : W ⟶ X` and `k : W ⟶ Y` are such
that `h ≫ f = k ≫ g`, then we have `l : W ⟶ t.pt` satisfying `l ≫ fst t = h` and `l ≫ snd t = k`.
 -/
CategoryTheory.Limits.PullbackCone.IsWeakLimit.lift' : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X Y Z : C} →
      {f : X ⟶ Z} →
        {g : Y ⟶ Z} →
          {t : CategoryTheory.Limits.PullbackCone f g} →
            CategoryTheory.Limits.IsWeakLimit t →
              {W : C} →
                (h : W ⟶ X) →
                  (k : W ⟶ Y) →
                    CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp k g →
                      { l //
                        CategoryTheory.CategoryStruct.comp l t.fst = h ∧
                          CategoryTheory.CategoryStruct.comp l t.snd = k }
-- Mathlib.Combinatorics.Tiling.Tile
DiscreteTiling.PlacedTile.mem_coe : ∀ {G : Type u_1} {X : Type u_2} {ιₚ : Type u_3} [inst : Group G] [inst_1 : MulAction G X]
  {ps : DiscreteTiling.Protoset G X ιₚ} {x : X} {pt : DiscreteTiling.PlacedTile ps}, x ∈ ↑pt ↔ x ∈ pt
-- Mathlib.Tactic.NormNum.Core
/-- Attempts to prove an expression is equal to some explicit number of the relevant type.  -/
Mathlib.Meta.NormNum.NormNumExt.eval : Mathlib.Meta.NormNum.NormNumExt →
  {u : Lean.Level} → {α : Q(Type u)} → (e : Q(«$α»)) → Lean.MetaM (Mathlib.Meta.NormNum.Result e)
-- Mathlib.Algebra.Algebra.Equiv
/-- Promotes a bijective algebra homomorphism to an algebra equivalence.  -/
AlgEquiv.ofBijective : {R : Type uR} →
  {A₁ : Type uA₁} →
    {A₂ : Type uA₂} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A₁] →
          [inst_2 : Semiring A₂] →
            [inst_3 : Algebra R A₁] → [inst_4 : Algebra R A₂] → (f : A₁ →ₐ[R] A₂) → Function.Bijective ⇑f → A₁ ≃ₐ[R] A₂
-- Mathlib.NumberTheory.LSeries.PrimesInAP
_private.Mathlib.NumberTheory.LSeries.PrimesInAP.0.ArithmeticFunction.vonMangoldt.F'' : Nat.Primes × ℕ → ℝ
-- Mathlib.FieldTheory.SeparableDegree
Polynomial.natSepDegree_pow_of_ne_zero : ∀ {F : Type u} [inst : Field F] (f : Polynomial F) {n : ℕ}, n ≠ 0 → (f ^ n).natSepDegree = f.natSepDegree
-- Lean.Meta.Tactic.Grind.EMatchTheorem
Lean.Meta.Grind.groundPattern? : Lean.Expr → Option Lean.Expr
-- Mathlib.NumberTheory.Padics.PadicVal.Defs
padicValNat.zero : ∀ {p : ℕ}, padicValNat p 0 = 0
-- Mathlib.Data.Num.Lemmas
/-- This tactic tries to turn an (in)equality about `PosNum`s to one about `Nat`s by rewriting.
```lean
example (n : PosNum) (m : PosNum) : n ≤ n + m := by
  transfer_rw
  exact Nat.le_add_right _ _
```
 -/
PosNum.transfer_rw : Lean.ParserDescr
-- Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
LiouvilleWith.mul_int_iff : ∀ {p x : ℝ} {m : ℤ}, m ≠ 0 → (LiouvilleWith p (x * ↑m) ↔ LiouvilleWith p x)
-- Mathlib.MeasureTheory.Measure.PreVariation
/-- `preVariationFun` is monotone in terms of the (measurable) set.  -/
MeasureTheory.preVariation.mono : ∀ {X : Type u_1} [inst : MeasurableSpace X] (f : Set X → ENNReal) {s₁ s₂ : Set X},
  MeasurableSet s₂ → s₁ ⊆ s₂ → MeasureTheory.preVariationFun f s₁ ≤ MeasureTheory.preVariationFun f s₂
-- Init.Data.List.Find
List.idxOf.eq_1 : ∀ {α : Type u} [inst : BEq α] (a : α), List.idxOf a = List.findIdx fun x => x == a
-- Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
FixedDetMatrices.reduce_mem_reps : ∀ {m : ℤ}, m ≠ 0 → ∀ (A : FixedDetMatrix (Fin 2) ℤ m), FixedDetMatrices.reduce A ∈ FixedDetMatrices.reps m
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Equiv.toHom_comp : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {ι₁ : Type u_8} {M₁ : Type u_9} {N₁ : Type u_10}
  {ι₂ : Type u_11} {M₂ : Type u_12} {N₂ : Type u_13} [inst_5 : AddCommGroup M₁] [inst_6 : Module R M₁]
  [inst_7 : AddCommGroup N₁] [inst_8 : Module R N₁] [inst_9 : AddCommGroup M₂] [inst_10 : Module R M₂]
  [inst_11 : AddCommGroup N₂] [inst_12 : Module R N₂] {P : RootPairing ι R M N} {P₁ : RootPairing ι₁ R M₁ N₁}
  {P₂ : RootPairing ι₂ R M₂ N₂} (g : P₁.Equiv P₂) (f : P.Equiv P₁), ↑(g.comp f) = (↑g).comp ↑f
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getKey_insertMany_list_of_mem : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α],
  (↑m).WF →
    ∀ {l : List (α × β)} {k k' : α},
      (k == k') = true →
        List.Pairwise (fun a b => (a.1 == b.1) = false) l →
          k ∈ List.map Prod.fst l →
            ∀ {h' : (↑(Std.DHashMap.Internal.Raw₀.Const.insertMany m l)).contains k' = true},
              (↑(Std.DHashMap.Internal.Raw₀.Const.insertMany m l)).getKey k' h' = k
-- Batteries.Data.String.Lemmas
String.get_of_valid : ∀ (cs cs' : List Char),
  String.Pos.Raw.get (String.ofList (cs ++ cs')) { byteIdx := String.utf8Len cs } = cs'.headD default
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalAlgebra.mem_adjoin_of_mem : ∀ (R : Type u) {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A] {s : Set A} {x : A},
  x ∈ s → x ∈ NonUnitalAlgebra.adjoin R s
-- Init.System.ST
EST.Out.error.inj : ∀ {ε σ α : Type} {a : ε} {a_1 : Void σ} {a_2 : ε} {a_3 : Void σ},
  EST.Out.error a a_1 = EST.Out.error a_2 a_3 → a = a_2 ∧ a_1 = a_3
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.bijective : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁}
  [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [inst_4 : TopologicalSpace M₁]
  [inst_5 : AddCommMonoid M₁] {M₂ : Type u_5} [inst_6 : TopologicalSpace M₂] [inst_7 : AddCommMonoid M₂]
  [inst_8 : Module R₁ M₁] [inst_9 : Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂), Function.Bijective ⇑e
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2to1.Λ'.ret.injEq : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} (a a_1 : Turing.TM2.Stmt Γ Λ σ),
  (Turing.TM2to1.Λ'.ret a = Turing.TM2to1.Λ'.ret a_1) = (a = a_1)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
/-- The `Y`-coordinate of a representative of `-(2 • P)` for a Jacobian point representative `P` on
a Weierstrass curve.  -/
WeierstrassCurve.Jacobian.negDblY : {R : Type r} → [CommRing R] → WeierstrassCurve.Jacobian R → (Fin 3 → R) → R
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.minKey!_alter_eq_self : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {k : α} {f : Option β → Option β},
  Std.ExtDTreeMap.Const.alter t k f ≠ ∅ →
    ((Std.ExtDTreeMap.Const.alter t k f).minKey! = k ↔
      (f (Std.ExtDTreeMap.Const.get? t k)).isSome = true ∧ ∀ k' ∈ t, (cmp k k').isLE = true)
-- Mathlib.RingTheory.Etale.Basic
Algebra.Etale.instProd_1 : ∀ {R : Type u} [inst : CommRing R] (S : Type u_2) [inst_1 : CommRing S], Algebra.Etale (R × S) R
-- Mathlib.Topology.Instances.Real.Lemmas
closure_ordConnected_inter_rat : ∀ {s : Set ℝ}, s.OrdConnected → s.Nontrivial → closure (s ∩ Set.range Rat.cast) = closure s
-- Mathlib.Data.Multiset.ZeroCons
Multiset.rel_of_forall : ∀ {α : Type u_1} {m1 m2 : Multiset α} {r : α → α → Prop},
  (∀ (a b : α), a ∈ m1 → b ∈ m2 → r a b) → m1.card = m2.card → Multiset.Rel r m1 m2
-- Mathlib.Tactic.FunProp.Theorems
/-- theorem name  -/
Mathlib.Meta.FunProp.FunctionTheorem.thmOrigin : Mathlib.Meta.FunProp.FunctionTheorem → Mathlib.Meta.FunProp.Origin
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.polar_smul : ∀ {S : Type u_1} {M : Type u_4} {N : Type u_5} [inst : AddCommGroup M] [inst_1 : AddCommGroup N] [inst_2 : Monoid S]
  [inst_3 : DistribMulAction S N] (f : M → N) (s : S) (x y : M),
  QuadraticMap.polar (s • f) x y = s • QuadraticMap.polar f x y
-- Init.Grind.Interactive
/-- `ac` associativity and commutativity procedure.  -/
Lean.Parser.Tactic.Grind.ac : Lean.ParserDescr
-- Init.Data.Dyadic.Basic
Dyadic.instDecidableLT : DecidableLT Dyadic
-- Mathlib.Combinatorics.Additive.SmallTripling
/-- If `A` is symmetric (`-A = A`) and has small tripling, then `A` has small powers,
in the sense that `|m • A|` is at most `|A|` times a constant exponential in `m`.

See also `Finset.small_alternating_nsmul_of_small_tripling` for a version with a weaker constant but
which encompasses non-symmetric sets.  -/
Finset.small_nsmul_of_small_tripling : ∀ {G : Type u_1} [inst : DecidableEq G] [inst_1 : AddGroup G] {A : Finset G} {K : ℝ} {m : ℕ},
  3 ≤ m → ↑(3 • A).card ≤ K * ↑A.card → -A = A → ↑(m • A).card ≤ K ^ (m - 2) * ↑A.card
-- Mathlib.Topology.MetricSpace.HausdorffDimension
/-- In an (extended) metric space with second countable topology, the Hausdorff dimension
of a set `s` is the supremum over `x ∈ s` of the limit superiors of `dimH t` along
`(𝓝[s] x).smallSets`.  -/
bsupr_limsup_dimH : ∀ {X : Type u_2} [inst : EMetricSpace X] [SecondCountableTopology X] (s : Set X),
  ⨆ x ∈ s, Filter.limsup dimH (nhdsWithin x s).smallSets = dimH s
-- Mathlib.Algebra.EuclideanDomain.Defs
EuclideanDomain.gcd_zero_left : ∀ {R : Type u} [inst : EuclideanDomain R] [inst_1 : DecidableEq R] (a : R), EuclideanDomain.gcd 0 a = a
-- Mathlib.RingTheory.TensorProduct.Pi
Algebra.TensorProduct.piRight_tmul : ∀ (R : Type u_1) (S : Type u_2) (A : Type u_3) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  [inst_3 : Semiring A] [inst_4 : Algebra R A] [inst_5 : Algebra S A] [inst_6 : IsScalarTower R S A] {ι : Type u_4}
  (B : ι → Type u_5) [inst_7 : (i : ι) → Semiring (B i)] [inst_8 : (i : ι) → Algebra R (B i)] [inst_9 : Fintype ι]
  [inst_10 : DecidableEq ι] (x : A) (f : (i : ι) → B i),
  (Algebra.TensorProduct.piRight R S A B) (x ⊗ₜ[R] f) = fun j => x ⊗ₜ[R] f j
-- Mathlib.Data.Int.Fib.Basic
Int.fib_two_mul_add_one_pos : ∀ {n : ℤ}, 0 < Int.fib (2 * n + 1)
-- Mathlib.Combinatorics.Matroid.Rank.Finite
Matroid.IsRkFinite.inter_left : ∀ {α : Type u_1} {M : Matroid α} {X Y : Set α}, M.IsRkFinite X → M.IsRkFinite (Y ∩ X)
-- Mathlib.Data.PNat.Prime
/-- The canonical map from `Nat.Primes` to `ℕ+`  -/
Nat.Primes.toPNat : Nat.Primes → ℕ+
-- Mathlib.Data.Set.Prod
Set.diag_image : ∀ {α : Type u_1} (s : Set α), Function.diag '' s = Set.diagonal α ∩ s ×ˢ s
-- Mathlib.Combinatorics.Additive.DoublingConst
Finset.addConst_empty_left : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : DecidableEq G] (B : Finset G), ∅.addConst B = 0
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.Relation.neg_1 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat}
  (x x' : RingCat.Colimits.Prequotient F), RingCat.Colimits.Relation F x x' → RingCat.Colimits.Relation F x.neg x'.neg
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.SInt
Int64.reduceLE : Lean.Meta.Simp.Simproc
-- Mathlib.Topology.Metrizable.Basic
TopologicalSpace.metrizableSpace_prod : ∀ {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [TopologicalSpace.MetrizableSpace X] [TopologicalSpace.MetrizableSpace Y], TopologicalSpace.MetrizableSpace (X × Y)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.isEmpty_alter_eq_isEmpty_erase : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α],
  (↑m).WF →
    ∀ {k : α} {f : Option (β k) → Option (β k)},
      (↑(m.alter k f)).isEmpty = ((↑(m.erase k)).isEmpty && (f (m.get? k)).isNone)
-- Lean.Elab.MutualInductive
Lean.Elab.Command.InductiveElabStep1.elabCtors : Lean.Elab.Command.InductiveElabStep1 →
  Array Lean.Elab.Command.ElabHeaderResult →
    Lean.Elab.Command.ElabHeaderResult → Array Lean.Expr → Lean.Elab.TermElabM Lean.Elab.Command.InductiveElabStep2
-- Mathlib.CategoryTheory.Limits.HasLimits
/-- The natural transformation induced by `colimit.ι`.  -/
CategoryTheory.Limits.colim.ι : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        [inst_2 : CategoryTheory.Limits.HasColimitsOfShape J C] →
          (j : J) → (CategoryTheory.evaluation J C).obj j ⟶ CategoryTheory.Limits.colim
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.Splits.roots_map_of_ne_zero : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] {S : Type u_4} [inst_2 : CommRing S] [inst_3 : IsDomain S]
  {f : Polynomial R},
  f.Splits → ∀ {φ : R →+* S}, Polynomial.map φ f ≠ 0 → (Polynomial.map φ f).roots = Multiset.map (⇑φ) f.roots
-- Init.Data.Array.Monadic
/-- Variant of `filterRevM_toArray` with a side condition for the start position.  -/
List.filterRevM_toArray' : ∀ {m : Type → Type u_1} {α : Type} {start : ℕ} [inst : Monad m] [LawfulMonad m] {l : List α} {p : α → m Bool},
  start = l.length → Array.filterRevM p l.toArray start = List.toArray <$> List.filterRevM p l
-- Mathlib.Analysis.Normed.Group.Ultra
/-- Given a function `f : ι → M` and a finite set `t ⊆ ι`, we can always find `i : ι`,
belonging to `t` if `t` is nonempty, such that `‖∑ j ∈ t, f j‖ ≤ ‖f i‖`.  -/
IsUltrametricDist.exists_norm_finsetSum_le : ∀ {M : Type u_1} {ι : Type u_2} [inst : SeminormedAddCommGroup M] [IsUltrametricDist M] (t : Finset ι) [Nonempty ι]
  (f : ι → M), ∃ i, (t.Nonempty → i ∈ t) ∧ ‖∑ j ∈ t, f j‖ ≤ ‖f i‖
-- Mathlib.CategoryTheory.GradedObject.Monoidal
CategoryTheory.GradedObject.Monoidal.rightUnitor_naturality : ∀ {I : Type u} [inst : AddMonoid I] {C : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : DecidableEq I] [inst_4 : CategoryTheory.Limits.HasInitial C]
  [inst_5 :
    ∀ (X₁ : C),
      CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C)
        ((CategoryTheory.MonoidalCategory.curriedTensor C).obj X₁)]
  {X X' : CategoryTheory.GradedObject I C} (φ : X ⟶ X'),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.GradedObject.Monoidal.tensorHom φ
        (CategoryTheory.CategoryStruct.id CategoryTheory.GradedObject.Monoidal.tensorUnit))
      (CategoryTheory.GradedObject.Monoidal.rightUnitor X').hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.rightUnitor X).hom φ
-- Lean.Meta.Basic
Lean.Meta.EtaStructMode.toUInt64 : Lean.Meta.EtaStructMode → UInt64
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- Notation for the `Ω` in an arbitrary choice of a subobject classifier  -/
CategoryTheory.HasSubobjectClassifier.Ω : (C : Type u) → [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.HasSubobjectClassifier C] → C
-- Mathlib.NumberTheory.RamificationInertia.Galois
Ideal.ramificationIdxIn.eq_1 : ∀ {A : Type u_1} [inst : CommRing A] (p : Ideal A) (B : Type u_2) [inst_1 : CommRing B] [inst_2 : Algebra A B],
  p.ramificationIdxIn B = if h : ∃ P, P.IsPrime ∧ P.LiesOver p then h.choose.ramificationIdx A else 0
-- Mathlib.Algebra.Category.Ring.Topology
CommRingCat.HomTopology.mvPolynomialHomeomorph_apply_snd : ∀ (σ : Type v) (R A : CommRingCat) [inst : TopologicalSpace ↑R] [inst_1 : IsTopologicalRing ↑R]
  (f : CommRingCat.of (MvPolynomial σ ↑A) ⟶ R) (i : σ),
  ((CommRingCat.HomTopology.mvPolynomialHomeomorph σ R A) f).2 i =
    (CategoryTheory.ConcreteCategory.hom f) (MvPolynomial.X i)
-- Mathlib.RingTheory.Polynomial.Selmer
Polynomial.X_pow_sub_X_sub_one_irreducible : ∀ {n : ℕ}, n ≠ 1 → Irreducible (Polynomial.X ^ n - Polynomial.X - 1)
-- Mathlib.Analysis.SpecialFunctions.Log.InvLog
Real.differentiableOn_log_log : DifferentiableOn ℝ (fun x => Real.log (Real.log x)) (Set.Ioi 1)
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.Parser.feature__2 : Lean.ParserDescr
-- Mathlib.RingTheory.Congruence.Defs
RingCon.coe_zero : ∀ {R : Type u_1} [inst : AddZeroClass R] [inst_1 : Mul R] (c : RingCon R), ↑0 = 0
-- Mathlib.Condensed.Epi
CondensedSet.epi_iff_locallySurjective_on_compHaus : ∀ {X Y : CondensedSet} (f : X ⟶ Y),
  CategoryTheory.Epi f ↔
    ∀ (S : CompHaus) (y : Y.obj.obj (Opposite.op S)),
      ∃ S' φ,
        ∃ (_ : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom φ)),
          ∃ x,
            (CategoryTheory.ConcreteCategory.hom (f.hom.app (Opposite.op S'))) x =
              (CategoryTheory.ConcreteCategory.hom (Y.obj.map (Opposite.op φ))) y
-- Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.hc : ∀ {ι : Type u_2} {κ : Type u_3} [inst : Preorder ι] {c : ℤ → ComplexShape κ} {r₀ : ℤ}
  (self : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀) (r : ℤ) (pq pq' : κ),
  (c r).Rel pq pq' →
    autoParam (r₀ ≤ r) CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore._auto_14 →
      self.deg pq + 1 = self.deg pq'
-- Init.Data.Int.Basic
/-- The negation of the successor of a natural number is an integer.

This constructor covers the negative integers (from `-1` to `-∞`).
 -/
Int.negSucc : ℕ → ℤ
-- Mathlib.CategoryTheory.Category.Quiv
CategoryTheory.Quiv.str' : (C : CategoryTheory.Quiv) → Quiver ↑C
-- Mathlib.MeasureTheory.Measure.Haar.Basic
/-- `haar` is some choice of a Haar measure, on a locally compact group.  -/
MeasureTheory.Measure.haar : {G : Type u_1} →
  [inst : Group G] →
    [inst_1 : TopologicalSpace G] →
      [IsTopologicalGroup G] →
        [inst : MeasurableSpace G] → [BorelSpace G] → [LocallyCompactSpace G] → MeasureTheory.Measure G
-- Mathlib.CategoryTheory.EquivalenceRelation
CategoryTheory.ReflexiveRelation.reflexivity₂_apply : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {R X : C} {p₁ p₂ : R ⟶ X}
  (self : CategoryTheory.ReflexiveRelation p₁ p₂) {F : C → C → Type uF} {carrier : C → Type w}
  {instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)} [inst_1 : CategoryTheory.ConcreteCategory C F]
  (x : carrier X), (CategoryTheory.ConcreteCategory.hom p₂) ((CategoryTheory.ConcreteCategory.hom self.r) x) = x
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.CodeDecl.inc.inj : ∀ {pu : Lean.Compiler.LCNF.Purity} {fvarId : Lean.FVarId} {n : ℕ} {check persistent : Bool}
  {h : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.CodeDecl._auto_11} {fvarId_1 : Lean.FVarId}
  {n_1 : ℕ} {check_1 persistent_1 : Bool}
  {h_1 : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.CodeDecl._auto_11},
  Lean.Compiler.LCNF.CodeDecl.inc fvarId n check persistent h =
      Lean.Compiler.LCNF.CodeDecl.inc fvarId_1 n_1 check_1 persistent_1 h_1 →
    fvarId = fvarId_1 ∧ n = n_1 ∧ check = check_1 ∧ persistent = persistent_1
-- Mathlib.Order.Basic
LE.le.not_lt_iff_eq : ∀ {α : Type u_2} [inst : PartialOrder α] {a b : α}, a ≤ b → (¬a < b ↔ a = b)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem!_insertManyIfNewUnit_list : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α Unit} {l : List α} {k : α},
  (m.insertManyIfNewUnit l)[k]! = ()
-- Mathlib.Logic.Embedding.Set
Function.Embedding.sigmaSet_range : ∀ {α : Type u_1} {ι : Type u_2} {s : ι → Set α} (h : Pairwise (Function.onFun Disjoint s)),
  Set.range ⇑(Function.Embedding.sigmaSet h) = ⋃ i, s i
-- Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
SummationFilter.conditional_filter : ∀ (β : Type u_2) [inst : Preorder β] [inst_1 : LocallyFiniteOrder β],
  (SummationFilter.conditional β).filter = Filter.map (fun p => Finset.Icc p.1 p.2) (Filter.atBot ×ˢ Filter.atTop)
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.supports_singleton : ∀ {S : Finset Turing.PartrecToTM2.Λ'} {q : Turing.PartrecToTM2.Λ'},
  Turing.PartrecToTM2.Supports {q} S ↔ Turing.TM2.SupportsStmt S (Turing.PartrecToTM2.tr q)
-- Mathlib.Data.Fintype.EquivFin
Multiset.pmap.congr_simp : ∀ {α : Type u_1} {β : Type v} {p : α → Prop} (f f_1 : (a : α) → p a → β),
  f = f_1 → ∀ (s s_1 : Multiset α) (e_s : s = s_1) (a : ∀ a ∈ s, p a), Multiset.pmap f s a = Multiset.pmap f_1 s_1 ⋯
-- Init.Data.Int.Order
Int.natAbs_sub_le : ∀ (a b : ℤ), (a - b).natAbs ≤ a.natAbs + b.natAbs
-- Mathlib.Algebra.Polynomial.Roots
/-- Given a polynomial `p` with coefficients in a ring `T` and a `T`-algebra `S`, `aroots p S` is
the multiset of roots of `p` regarded as a polynomial over `S`.  -/
Polynomial.aroots : {T : Type w} →
  [inst : CommRing T] →
    Polynomial T → (S : Type u_1) → [inst_1 : CommRing S] → [IsDomain S] → [Algebra T S] → Multiset S
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.instInhabited.eq_1 : ∀ {α : Type u_1}, FreeAddMonoid.instInhabited = { default := 0 }
-- Mathlib.RingTheory.Ideal.Span
Ideal.span_singleton_ne_top : ∀ {α : Type u_1} [inst : CommSemiring α] {x : α}, ¬IsUnit x → Ideal.span {x} ≠ ⊤
-- Mathlib.CategoryTheory.Limits.Types.Coproducts
CategoryTheory.Limits.CofanTypes.sigma_ι_fst : ∀ {C : Type u} (F : C → Type v) (x : CategoryTheory.Discrete C) (x_1 : (CategoryTheory.Discrete.functor F).obj x),
  ((CategoryTheory.Limits.CofanTypes.sigma F).ι x x_1).fst = x.as