mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.Translate.Reorder
Mathlib.Tactic.Translate.Reorder.mk.inj : ∀ {univReorder : Mathlib.Tactic.Translate.Permutation} {reorder : Mathlib.Tactic.Translate.ArgReorder}
  {univReorder_1 : Mathlib.Tactic.Translate.Permutation} {reorder_1 : Mathlib.Tactic.Translate.ArgReorder},
  { univReorder := univReorder, reorder := reorder } = { univReorder := univReorder_1, reorder := reorder_1 } →
    univReorder = univReorder_1 ∧ reorder = reorder_1
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw.fold_induction : ∀ {α : Type u} {β : α → Type v} {δ : Type w} {f : δ → (a : α) → β a → δ} {init : δ} {b : Std.DHashMap.Raw α β}
  {P : δ → Prop}, P init → (∀ (acc : δ) (a : α) (b : β a), P acc → P (f acc a b)) → P (Std.DHashMap.Raw.fold f init b)
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.isSpanningSubgraph_iff : ∀ {α : Type u_1} {β : Type u_2} (H G : Graph α β), H ≤s G ↔ H.IsSubgraph G ∧ H.vertexSet = G.vertexSet
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.dist_map_zero_lt_of_semiconj : ∀ {f g₁ g₂ : CircleDeg1Lift}, Function.Semiconj ⇑f ⇑g₁ ⇑g₂ → dist (g₁ 0) (g₂ 0) < 2
-- Init.PropLemmas
forall₂_congr : ∀ {α : Sort u_1} {β : α → Sort u_2} {p q : (a : α) → β a → Prop},
  (∀ (a : α) (b : β a), p a b ↔ q a b) → ((∀ (a : α) (b : β a), p a b) ↔ ∀ (a : α) (b : β a), q a b)
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.lift.congr_simp : ∀ {R : Type u_1} [inst : CommSemiring R] (S S_1 : Submonoid R) (e_S : S = S_1) {M : Type u_2} {M' : Type u_3}
  {M'' : Type u_4} [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M'] [inst_3 : AddCommMonoid M'']
  [inst_4 : Module R M] [inst_5 : Module R M'] [inst_6 : Module R M''] (f f_1 : M →ₗ[R] M') (e_f : f = f_1)
  [inst_7 : IsLocalizedModule S f] (g g_1 : M →ₗ[R] M''),
  g = g_1 →
    ∀ (h : ∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M'')) ↑x)),
      IsLocalizedModule.lift S f g h = IsLocalizedModule.lift S_1 f_1 g_1 ⋯
-- Mathlib.Algebra.Star.Subalgebra
/-- The equalizer of two star `R`-algebra homomorphisms.  -/
StarAlgHom.equalizer : {F : Type u_1} →
  {R : Type u_2} →
    {A : Type u_3} →
      {B : Type u_4} →
        [inst : CommSemiring R] →
          [inst_1 : StarRing R] →
            [inst_2 : Semiring A] →
              [inst_3 : Algebra R A] →
                [inst_4 : StarRing A] →
                  [inst_5 : Semiring B] →
                    [inst_6 : Algebra R B] →
                      [inst_7 : StarRing B] →
                        [inst_8 : StarModule R A] →
                          [inst_9 : FunLike F A B] →
                            [AlgHomClass F R A B] → [StarHomClass F A B] → F → F → StarSubalgebra R A
-- Mathlib.AlgebraicGeometry.Modules.Tilde
AlgebraicGeometry.tilde.map_sub : ∀ {R : CommRingCat} {M N : ModuleCat ↑R} (f g : M ⟶ N),
  AlgebraicGeometry.tilde.map (f - g) = AlgebraicGeometry.tilde.map f - AlgebraicGeometry.tilde.map g
-- Init.Data.Iterators.Consumers.Monadic.Loop
Std.IterM.instForInOfIteratorLoop : {m : Type w → Type w'} →
  {n : Type w → Type w''} →
    {α β : Type w} →
      [inst : Std.Iterator α m β] → [Std.IteratorLoop α m n] → [MonadLiftT m n] → [Monad n] → ForIn n (Std.IterM m β) β
-- Mathlib.NumberTheory.Height.NumberField
/-- The logarithmic height of a rational number is the logarithm of the maximum of the absolute
value of its numerator and its denominator.  -/
Rat.logHeight₁_eq_log_max : ∀ (q : ℚ), Height.logHeight₁ q = Real.log ↑(max q.num.natAbs q.den)
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHom.toEnd_one : ∀ {α : Type u_5} [inst : NonUnitalNonAssocSemiring α], CentroidHom.toEnd 1 = 1
-- Mathlib.Tactic.DepRewrite
/-- Configures the behavior of the `rewrite!` and `rw!` tactics.  -/
Mathlib.Tactic.DepRewrite.Config : Type
-- Mathlib.Algebra.Lie.Killing
/-- We say a Lie algebra is Killing if its Killing form is non-singular.

NB: This is not standard terminology (the literature does not seem to name Lie algebras with this
property).  -/
LieAlgebra.IsKilling : (R : Type u_1) → (L : Type u_3) → [inst : CommRing R] → [inst_1 : LieRing L] → [LieAlgebra R L] → Prop
-- Std.Data.DHashMap.Internal.Raw
Std.DHashMap.Internal.Raw.getThenInsertIfNew?_snd_eq : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α] {m : Std.DHashMap.Raw α β}
  (h : m.WF) {a : α} {b : β a},
  (m.getThenInsertIfNew? a b).2 = ↑(Std.DHashMap.Internal.Raw₀.getThenInsertIfNew? ⟨m, ⋯⟩ a b).2
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKey!_le_minKey!_erase : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited α]
  {k : α}, (t.erase k).isEmpty = false → (cmp t.minKey! (t.erase k).minKey!).isLE = true
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
AugmentedSimplexCategory.inl_comp_inl_comp_associator_assoc : ∀ (x y z : AugmentedSimplexCategory) {Z : AugmentedSimplexCategory}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj x (CategoryTheory.MonoidalCategoryStruct.tensorObj y z) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (x.inl y)
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategoryStruct.tensorObj x y).inl z)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator x y z).hom h)) =
    CategoryTheory.CategoryStruct.comp (x.inl (CategoryTheory.MonoidalCategoryStruct.tensorObj y z)) h
-- Mathlib.GroupTheory.Congruence.Defs
/-- The infimum of two additive congruence relations equals the infimum of the underlying binary
operations.  -/
AddCon.coe_inf : ∀ {M : Type u_1} [inst : Add M] {c d : AddCon M}, ⇑(c ⊓ d) = ⇑c ⊓ ⇑d
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.size_le_size_erase : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF)
  {k : α}, t.size ≤ (Std.DTreeMap.Internal.Impl.erase k t ⋯).impl.size + 1
-- Mathlib.Algebra.GroupWithZero.Hom
MonoidWithZeroHom.map_one : ∀ {α : Type u_2} {β : Type u_3} [inst : MulZeroOneClass α] [inst_1 : MulZeroOneClass β] (f : α →*₀ β), f 1 = 1
-- Mathlib.CategoryTheory.Bicategory.Functor.Oplax
/-- Oplax associativity.  -/
CategoryTheory.OplaxFunctor.map₂_associator_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (self : CategoryTheory.OplaxFunctor B C) {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d)
  {Z : self.obj a ⟶ self.obj d}
  (h_1 :
    CategoryTheory.CategoryStruct.comp (self.map f) (CategoryTheory.CategoryStruct.comp (self.map g) (self.map h)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (self.map₂ (CategoryTheory.Bicategory.associator f g h).hom)
      (CategoryTheory.CategoryStruct.comp (self.mapComp f (CategoryTheory.CategoryStruct.comp g h))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (self.map f) (self.mapComp g h))
          h_1)) =
    CategoryTheory.CategoryStruct.comp (self.mapComp (CategoryTheory.CategoryStruct.comp f g) h)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (self.mapComp f g) (self.map h))
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Bicategory.associator (self.map f) (self.map g) (self.map h)).hom h_1))
-- Std.Data.Internal.List.Associative
Std.Internal.List.self_le_maxKey_insertEntryIfNew : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α} {v : β k}, (compare k (Std.Internal.List.maxKey (Std.Internal.List.insertEntryIfNew k v l) ⋯)).isLE = true
-- Mathlib.Combinatorics.SetFamily.Shadow
/-- `t` is in the upper shadow of `𝒜` iff `t` is exactly one element more than something from `𝒜`.

See also `Finset.mem_upShadow_iff_exists_mem_card_add_one`.  -/
Finset.mem_upShadow_iff_exists_sdiff : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {𝒜 : Finset (Finset α)} {t : Finset α},
  t ∈ 𝒜.upShadow ↔ ∃ s ∈ 𝒜, s ⊆ t ∧ (t \ s).card = 1
-- Mathlib.Algebra.BigOperators.Group.List.Basic
/-- A non-commutative variant of `List.sum_reverse`  -/
List.sum_reverse_noncomm : ∀ {G : Type u_7} [inst : AddGroup G] (L : List G), L.reverse.sum = -(List.map (fun x => -x) L).sum
-- Mathlib.Order.Category.HeytAlg
_private.Mathlib.Order.Category.HeytAlg.0.HeytAlg.Hom.mk : {X Y : HeytAlg} → HeytingHom ↑X ↑Y → X.Hom Y
-- Init.Data.Array.Lemmas
Array.getElem_modify : ∀ {α : Type u_1} {f : α → α} {xs : Array α} {j i : ℕ} (h : i < (xs.modify j f).size),
  (xs.modify j f)[i] = if j = i then f xs[i] else xs[i]
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- The top arrow in the pullback square  -/
CategoryTheory.Subobject.Classifier.χ₀ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → (self : CategoryTheory.Subobject.Classifier C) → (U : C) → U ⟶ self.Ω₀
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.insertManyIfNewUnit_list_equiv_foldl : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ : Std.TreeMap.Raw α Unit cmp} {l : List α},
  (t₁.insertManyIfNewUnit l).Equiv (List.foldl (fun acc a => acc.insertIfNew a ()) t₁ l)
-- Mathlib.Algebra.DirectSum.Ring
DirectSum.of_zero_pow : ∀ {ι : Type u_1} [inst : DecidableEq ι] (A : ι → Type u_2) [inst_1 : (i : ι) → AddCommMonoid (A i)]
  [inst_2 : AddMonoid ι] [inst_3 : DirectSum.GSemiring A] (a : A 0) (n : ℕ),
  (DirectSum.of A 0) (a ^ n) = (DirectSum.of A 0) a ^ n
-- Mathlib.Topology.Algebra.Group.Pointwise
closure_subset_of_mem_nhds_zero_of_neg_add_right_subset : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [SeparatelyContinuousAdd G] {s s' t : Set G},
  s' ∈ nhds 0 → (∀ x ∈ s', -x ∈ s') → s + s' ⊆ t → closure s ⊆ t
-- Mathlib.Order.Partition.Finpartition
Finpartition.ofExistsUnique_parts : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} (parts : Finset (Finset α)) (h : ∀ p ∈ parts, p ⊆ s)
  (h' : ∀ a ∈ s, ∃! t, t ∈ parts ∧ a ∈ t) (h'' : ∅ ∉ parts), (Finpartition.ofExistsUnique parts h h' h'').parts = parts
-- Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
_private.Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm.0.μ_bddBelow : ∀ {R : Type u_1} [inst : CommRing R] (μ : RingSeminorm R) (s : ℕ → ℕ) {x : R} (ψ : ℕ → ℕ),
  BddBelow {a | ∀ᶠ (n : ℝ) in Filter.map (fun n => μ x ^ (↑(s (ψ n)) * (1 / ↑(ψ n)))) Filter.atTop, n ≤ a}
-- Mathlib.Order.BoundedOrder.Basic
ULift.instBoundedOrder : {α : Type u} → [inst : LE α] → [BoundedOrder α] → BoundedOrder (ULift.{v, u} α)
-- Init.Data.BitVec.Lemmas
/-- Signed multiplication overflow reassociation.
If `(x * y)` and `(y * z)` do not overflow, then `(x * y) * z` overflows iff `x * (y * z)` overflows.
 -/
BitVec.smulOverflow_assoc : ∀ {w : ℕ} {x y z : BitVec w},
  ¬x.smulOverflow y = true → ¬y.smulOverflow z = true → (x * y).smulOverflow z = x.smulOverflow (y * z)
-- Mathlib.FieldTheory.Relrank
Subfield.relfinrank_mul_relfinrank_eq_inf_relfinrank : ∀ {E : Type v} [inst : Field E] (A : Subfield E) {B C : Subfield E},
  B ≤ C → A.relfinrank B * B.relfinrank C = (A ⊓ B).relfinrank C
-- Init.Grind.Ring.Basic
Lean.Grind.IsCharP.mk : ∀ {α : Type u} [inst : Lean.Grind.Semiring α] {p : outParam ℕ},
  (∀ {x y : ℕ}, OfNat.ofNat x = OfNat.ofNat y ↔ x % p = y % p) → Lean.Grind.IsCharP α p
-- Mathlib.RepresentationTheory.Basic
Representation.leftRegular_norm_apply : ∀ {k : Type u_1} {G : Type u_2} [inst : CommSemiring k] [inst_1 : Group G] [inst_2 : Fintype G],
  (Representation.leftRegular k G).norm =
    (LinearMap.lsmul k (MonoidAlgebra k G)).flip ((Representation.leftRegular k G).norm (MonoidAlgebra.single 1 1)) ∘ₗ
      (Finsupp.linearCombination k fun x => 1) ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k)
-- Mathlib.CategoryTheory.Triangulated.TriangleShift
CategoryTheory.Pretriangulated.Triangle.shiftFunctor_eq : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] (n : ℤ),
  CategoryTheory.shiftFunctor (CategoryTheory.Pretriangulated.Triangle C) n =
    CategoryTheory.Pretriangulated.Triangle.shiftFunctor C n
-- Std.Do.SPred.SPred
Std.Do.SPred.or_nil : ∀ {P Q : Std.Do.SPred []}, spred(P ∨ Q) = { down := P.down ∨ Q.down }
-- Mathlib.Computability.RecursiveIn
ComputableIn.id : ∀ {α : Type u_1} [inst : Primcodable α] {O : Set (ℕ →. ℕ)}, ComputableIn O id
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.minKey!.induct_unfolding : ∀ {α : Type u} {β : α → Type v} [inst : Inhabited α] (motive : Std.DTreeMap.Internal.Impl α β → α → Prop),
  motive Std.DTreeMap.Internal.Impl.leaf
      (panicWithPosWithDecl "Std.Data.DTreeMap.Internal.Queries" "Std.DTreeMap.Internal.Impl.minKey!" 413 13
        "Map is empty") →
    (∀ (size : ℕ) (k : α) (v : β k) (r : Std.DTreeMap.Internal.Impl α β),
        motive (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r) k) →
      (∀ (size : ℕ) (k : α) (v : β k) (size_1 : ℕ) (k_1 : α) (v_1 : β k_1) (l r r_1 : Std.DTreeMap.Internal.Impl α β),
          motive (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r)
              (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r).minKey! →
            motive (Std.DTreeMap.Internal.Impl.inner size k v (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) r_1)
              (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r).minKey!) →
        ∀ (a : Std.DTreeMap.Internal.Impl α β), motive a a.minKey!
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.UInt
UInt16.reduceDiv : Lean.Meta.Simp.DSimproc
-- Mathlib.ModelTheory.Bundled
FirstOrder.Language.ElementarySubstructure.toModel.instSmall : ∀ {L : FirstOrder.Language} (T : L.Theory) {M : T.ModelType} (S : L.ElementarySubstructure ↑M) [h : Small.{w, x} ↥S],
  Small.{w, x} ↑(FirstOrder.Language.ElementarySubstructure.toModel T S)
-- Mathlib.LinearAlgebra.DFinsupp
/-- `DFinsupp.mapRange.linearMap` as a `LinearEquiv`.  -/
DFinsupp.mapRange.linearEquiv : {ι : Type u_1} →
  {R : Type u_3} →
    [inst : Semiring R] →
      {β₁ : ι → Type u_8} →
        {β₂ : ι → Type u_9} →
          [inst_1 : (i : ι) → AddCommMonoid (β₁ i)] →
            [inst_2 : (i : ι) → AddCommMonoid (β₂ i)] →
              [inst_3 : (i : ι) → Module R (β₁ i)] →
                [inst_4 : (i : ι) → Module R (β₂ i)] →
                  ((i : ι) → β₁ i ≃ₗ[R] β₂ i) → (Π₀ (i : ι), β₁ i) ≃ₗ[R] Π₀ (i : ι), β₂ i
-- Mathlib.Order.Fin.Basic
Fin.strictMono_succAbove : ∀ {n : ℕ} (p : Fin (n + 1)), StrictMono p.succAbove
-- Init.Data.Array.Lemmas
Array.foldr_append_eq_append : ∀ {α : Type u_1} {β : Type u_2} {xs : Array α} {f : α → Array β} {ys : Array β},
  Array.foldr (fun x1 x2 => f x1 ++ x2) ys xs = (Array.map f xs).flatten ++ ys
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
/-- Through the equivalence `(AugmentedSimplexCategory ⥤ C) ≌ CosimplicialObject.Augmented C`,
taking the point of the augmentation corresponds to evaluation at the initial object.  -/
AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompPointIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    AugmentedSimplexCategory.equivAugmentedCosimplicialObject.functor.comp
        CategoryTheory.CosimplicialObject.Augmented.point ≅
      (CategoryTheory.evaluation AugmentedSimplexCategory C).obj CategoryTheory.WithInitial.star
-- Init.Data.Array.Lemmas
Array.filter_eq_empty_iff : ∀ {α : Type u_1} {p : α → Bool} {xs : Array α}, Array.filter p xs = #[] ↔ ∀ a ∈ xs, ¬p a = true
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- The function on the walking pair, sending the two points to `X` and `Y`.  -/
CategoryTheory.Limits.pairFunction : {C : Type u} → C → C → CategoryTheory.Limits.WalkingPair → C
-- Mathlib.Topology.Order.DenselyOrdered
frontier_Iio : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [DenselyOrdered α]
  [NoMinOrder α] {a : α}, frontier (Set.Iio a) = {a}
-- Mathlib.Data.Set.Prod
Set.mem_graphOn : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} {x : α × β}, x ∈ Set.graphOn f s ↔ x.1 ∈ s ∧ f x.1 = x.2
-- Mathlib.Analysis.Normed.Group.Seminorm
/-- **Alias** of `FunLike.coe_smul`. -/
NonarchAddGroupSeminorm.coe_smul : ∀ {M : Type u_1} {F : Type u_3} {α : Type u_5} {β : Type u_6} [inst : FunLike F α β] [inst_1 : SMul M F]
  [inst_2 : SMul M β] [IsSMulApply M F α β] (n : M) (f : F), ⇑(n • f) = n • ⇑f
-- Mathlib.Topology.UniformSpace.Cauchy
isComplete_iff_ultrafilter' : ∀ {α : Type u} [uniformSpace : UniformSpace α] {s : Set α},
  IsComplete s ↔ ∀ (l : Ultrafilter α), Cauchy ↑l → s ∈ l → ∃ x ∈ s, ↑l ≤ nhds x
-- Mathlib.Dynamics.OmegaLimit
omegaLimit_preimage_subset : ∀ {τ : Type u_1} {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace β] {α' : Type u_5} (ϕ : τ → α' → β) (s : Set α')
  (f : Filter τ) (g : α → α'), omegaLimit f (fun t x => ϕ t (g x)) (g ⁻¹' s) ⊆ omegaLimit f ϕ s
-- Mathlib.Algebra.Group.Defs
CommSemigroup.mk : {G : Type u} → [toSemigroup : Semigroup G] → (∀ (a b : G), a * b = b * a) → CommSemigroup G
-- Std.Data.HashSet.Lemmas
Std.HashSet.get?_eq_some : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [LawfulBEq α] {k : α}, k ∈ m → m.get? k = some k
-- Mathlib.Order.SuccPred.Limit
Order.IsSuccLimit.mk : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, ¬IsMin a → Order.IsSuccPrelimit a → Order.IsSuccLimit a
-- Init.Grind.Ordered.Ring
Lean.Grind.OrderedRing.natCast_nonneg : ∀ {R : Type u} [inst : Lean.Grind.Ring R] [inst_1 : LE R] [inst_2 : LT R] [Std.LawfulOrderLT R]
  [inst_4 : Std.IsPreorder R] [Lean.Grind.OrderedRing R] {a : ℕ}, 0 ≤ ↑a
-- Init.System.IO
IO.FS.instReprFileType.repr : IO.FS.FileType → ℕ → Std.Format
-- Init.Data.Char.Basic
/-- Returns `true` if the character is an ASCII letter or digit.

The ASCII letters are the following: `ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz`.
The ASCII digits are the following: `0123456789`.
 -/
Char.isAlphanum : Char → Bool
-- Mathlib.Algebra.Group.Units.Defs
AddUnits.neg_eq_val_neg : ∀ {α : Type u} [inst : AddMonoid α] (a : AddUnits α), a.neg = ↑(-a)
-- Mathlib.CategoryTheory.Monoidal.Action.End
CategoryTheory.MonoidalCategory.MonoidalRightAction.curriedActionMonoidal_δ_app : ∀ {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]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] (x x_1 : C) (x_2 : D),
  (CategoryTheory.Functor.OplaxMonoidal.δ (CategoryTheory.MonoidalCategory.MonoidalRightAction.curriedAction C D) x
          x_1).app
      x_2 =
    (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso x_2 x x_1).hom
-- Init.Data.List.MinMaxIdx
_private.Init.Data.List.MinMaxIdx.0.List.minIdxOn.eq_def : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] (f : α → β) (xs : List α) (h : xs ≠ []),
  List.minIdxOn f xs h =
    match xs, h with
    | y :: ys, h => List.minIdxOn.go✝ f y 0 1 ys
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.mul_sum : ∀ {α : Type u_1} {R : Type u_14} {S : Type u_15} [inst : NonUnitalNonAssocSemiring R]
  [inst_1 : NonUnitalNonAssocSemiring S] (b : S) (s : α →₀ R) {f : α → R → S}, b * s.sum f = s.sum fun a c => b * f a c
-- Mathlib.CategoryTheory.Skeletal
/-- If `C` is thin and skeletal, `D ⥤ C` is skeletal.
`CategoryTheory.functor_thin` shows it is thin also.
 -/
CategoryTheory.functor_skeletal : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [Quiver.IsThin C], CategoryTheory.Skeletal C → CategoryTheory.Skeletal (CategoryTheory.Functor D C)
-- Mathlib.Algebra.Category.MonCat.Colimits
MonCat.Colimits.monoidColimitType : {J : Type v} →
  [inst : CategoryTheory.Category.{u, v} J] →
    (F : CategoryTheory.Functor J MonCat) → Monoid (MonCat.Colimits.ColimitType F)
-- Batteries.Data.Array.Scan
Subarray.scanrM.eq_1 : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] (f : α → β → m β) (init : β)
  (as : Subarray α), Subarray.scanrM f init as = Array.scanrM f init as.array as.start as.stop
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.map_eq_ofNat_iff : ∀ {α : Type u} {β : Type v} [inst : AddMonoidWithOne α] {f : β → α} {n : ℕ} [inst_1 : n.AtLeastTwo] {a : WithTop β},
  WithTop.map f a = OfNat.ofNat n ↔ ∃ x, a = ↑x ∧ f x = ↑n
-- Mathlib.CategoryTheory.FiberedCategory.Fibered
/-- In a category which admits strongly Cartesian pullbacks, any Cartesian morphism is
strongly Cartesian. This is a helper-lemma for the fact that admitting strongly Cartesian pullbacks
implies being fibered.  -/
CategoryTheory.Functor.IsFibered.isStronglyCartesian_of_exists_isCartesian : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  (p : CategoryTheory.Functor 𝒳 𝒮),
  (∀ (a : 𝒳) (R : 𝒮) (f : R ⟶ p.obj a), ∃ b φ, p.IsStronglyCartesian f φ) →
    ∀ {R S : 𝒮} (f : R ⟶ S) {a b : 𝒳} (φ : a ⟶ b) [p.IsCartesian f φ], p.IsStronglyCartesian f φ
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.mvPolynomial_σ : ∀ (R : Type u) (ι : Type w) [inst : CommRing R] (f : MvPolynomial ι R), (Algebra.Generators.mvPolynomial R ι).σ f = f
-- Init.Data.Dyadic.Basic
_private.Init.Data.Dyadic.Basic.0.Dyadic.add.match_1.splitter : (motive : ℤ → Sort u_1) →
  (x : ℤ) → (Unit → motive 0) → ((d' : ℕ) → motive (Int.ofNat d'.succ)) → ((d : ℕ) → motive (Int.negSucc d)) → motive x
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
/-- Given a group homomorphism `f : G →* H` and a representation morphism `φ : A ⟶ Res(f)(B)`,
this is the induced map sending `∑ aᵢ·(gᵢ₁, gᵢ₂) : G × G →₀ A` to
`∑ φ(aᵢ)·(f(gᵢ₁), f(gᵢ₂)) : H × H →₀ B`.  -/
groupHomology.chainsMap₂ : {k G H : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      [inst_2 : Group H] →
        {A : Rep.{u_1, u, u} k G} →
          {B : Rep.{u_1, u, u} k H} →
            (f : G →* H) → (A ⟶ Rep.res f B) → (ModuleCat.of k (G × G →₀ ↑A) ⟶ ModuleCat.of k (H × H →₀ ↑B))
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
MulRingNorm.mulRingNormEquivAbsoluteValue_apply : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : Nontrivial R] (N : MulRingNorm R) (x : R),
  (MulRingNorm.mulRingNormEquivAbsoluteValue N) x = N x
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax
CategoryTheory.Lax.OplaxTrans.rightUnitor_inv_as_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.LaxFunctor B C} (η : F ⟶ G) (a : B),
  (CategoryTheory.Lax.OplaxTrans.rightUnitor η).inv.as.app a = (CategoryTheory.Bicategory.rightUnitor (η.app a)).inv
-- Mathlib.Algebra.Group.Hom.Defs
/-- Any type satisfying `MonoidHomClass` can be cast into `MonoidHom` via
`MonoidHomClass.toMonoidHom`.  -/
instCoeTCMonoidHomOfMonoidHomClass : {M : Type u_4} →
  {N : Type u_5} →
    {F : Type u_9} →
      [inst : MulOne M] → [inst_1 : MulOne N] → [inst_2 : FunLike F M N] → [MonoidHomClass F M N] → CoeTC F (M →* N)