mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.InjSurj
Function.Injective.group.eq_1 : ∀ {M₁ : Type u_1} {M₂ : Type u_2} [inst : Mul M₁] [inst_1 : One M₁] [inst_2 : Pow M₁ ℕ] [inst_3 : Inv M₁]
  [inst_4 : Div M₁] [inst_5 : Pow M₁ ℤ] [inst_6 : Group M₂] (f : M₁ → M₂) (hf : Function.Injective f) (one : f 1 = 1)
  (mul : ∀ (x y : M₁), f (x * y) = f x * f y) (inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹)
  (div : ∀ (x y : M₁), f (x / y) = f x / f y) (npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n)
  (zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n),
  Function.Injective.group f hf one mul inv div npow zpow =
    { toDivInvMonoid := Function.Injective.divInvMonoid f hf one mul inv div npow zpow, inv_mul_cancel := ⋯ }
-- Mathlib.Algebra.Homology.Factorizations.CM5a
/-- The second morphism `π f n₀ : mid f n₀ ⟶ L` of the factorization lemma `cm5a_cof`.  -/
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.π : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {K L : CochainComplex C ℤ} →
        (f : K ⟶ L) →
          [inst_2 : CategoryTheory.EnoughInjectives C] →
            [inst_3 : CategoryTheory.Mono f] →
              (n₀ : ℤ) →
                [inst_4 : K.IsStrictlyGE (n₀ + 1)] →
                  [inst_5 : L.IsStrictlyGE (n₀ + 1)] → CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.mid✝ f n₀ ⟶ L
-- Mathlib.Order.Interval.Multiset
Multiset.right_mem_Icc : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] {a b : α}, b ∈ Multiset.Icc a b ↔ a ≤ b
-- Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
CongruenceSubgroup.instFiniteIndexGamma1 : ∀ (N : ℕ) [NeZero N], (CongruenceSubgroup.Gamma1 N).FiniteIndex
-- Mathlib.LinearAlgebra.AffineSpace.Midpoint
right_eq_midpoint_iff : ∀ (R : Type u_1) {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : Invertible 2] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] {x y : P}, y = midpoint R x y ↔ x = y
-- Mathlib.RingTheory.DedekindDomain.Different
FractionalIdeal.dual_mul_self : ∀ (A : Type u_1) (K : Type u_2) {L : Type u} {B : Type u_3} [inst : CommRing A] [inst_1 : Field K] [inst_2 : CommRing B]
  [inst_3 : Field L] [inst_4 : Algebra A K] [inst_5 : Algebra B L] [inst_6 : Algebra A B] [inst_7 : Algebra K L]
  [inst_8 : Algebra A L] [inst_9 : IsScalarTower A K L] [inst_10 : IsScalarTower A B L] [inst_11 : IsDomain A]
  [inst_12 : IsFractionRing A K] [inst_13 : FiniteDimensional K L] [inst_14 : Algebra.IsSeparable K L]
  [inst_15 : IsIntegralClosure B A L] [inst_16 : IsFractionRing B L] [inst_17 : IsIntegrallyClosed A]
  [inst_18 : IsDedekindDomain B] {I : FractionalIdeal (nonZeroDivisors B) L},
  I ≠ 0 → FractionalIdeal.dual A K I * I = FractionalIdeal.dual A K 1
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.AbsolutelyContinuous.trans : ∀ {α : Type u_1} {m : MeasurableSpace α} {L : Type u_3} {M : Type u_4} {N : Type u_5} [inst : AddCommMonoid L]
  [inst_1 : TopologicalSpace L] [inst_2 : AddCommMonoid M] [inst_3 : TopologicalSpace M] [inst_4 : AddCommMonoid N]
  [inst_5 : TopologicalSpace N] {u : MeasureTheory.VectorMeasure α L} {v : MeasureTheory.VectorMeasure α M}
  {w : MeasureTheory.VectorMeasure α N}, u.AbsolutelyContinuous v → v.AbsolutelyContinuous w → u.AbsolutelyContinuous w
-- Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence
Mathlib.Tactic.Monoidal.naturality_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {p f g h pf : C}
  {η : f ≅ g} {θ : g ≅ h} (η_f : CategoryTheory.MonoidalCategoryStruct.tensorObj p f ≅ pf)
  (η_g : CategoryTheory.MonoidalCategoryStruct.tensorObj p g ≅ pf)
  (η_h : CategoryTheory.MonoidalCategoryStruct.tensorObj p h ≅ pf),
  CategoryTheory.MonoidalCategory.whiskerLeftIso p η ≪≫ η_g = η_f →
    CategoryTheory.MonoidalCategory.whiskerLeftIso p θ ≪≫ η_h = η_g →
      CategoryTheory.MonoidalCategory.whiskerLeftIso p (η ≪≫ θ) ≪≫ η_h = η_f
-- Mathlib.GroupTheory.Finiteness
AddMonoid.fg_of_surjective : ∀ {M : Type u_1} [inst : AddMonoid M] {M' : Type u_3} [inst_1 : AddMonoid M'] [AddMonoid.FG M] (f : M →+ M'),
  Function.Surjective ⇑f → AddMonoid.FG M'
-- Mathlib.LinearAlgebra.Matrix.ToLin
Matrix.mulVecLin_apply : ∀ {R : Type u_1} [inst : CommSemiring R] {m : Type u_4} {n : Type u_5} [inst_1 : Fintype n] (M : Matrix m n R)
  (v : n → R), M.mulVecLin v = M.mulVec v
-- Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
/-- If x is in `lipschitzGroup Q`, then `(ι Q).range` is closed under twisted conjugation.
The reverse statement presumably is true only in finite dimensions.  -/
lipschitzGroup.conjAct_smul_range_ι : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} {x : (CliffordAlgebra Q)ˣ},
  x ∈ lipschitzGroup Q →
    ∀ [Invertible 2], ConjAct.toConjAct x • (CliffordAlgebra.ι Q).range = (CliffordAlgebra.ι Q).range
-- Mathlib.FieldTheory.Finite.Polynomial
MvPolynomial.rank_R : ∀ (σ K : Type u) [inst : Fintype K] [inst_1 : Field K] [inst_2 : Fintype σ],
  Module.rank K (MvPolynomial.R σ K) = ↑(Fintype.card (σ → K))
-- Mathlib.CategoryTheory.Monoidal.Action.End
CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionOfMonoidalFunctorToEndofunctorMop_actionAssocIso_hom : ∀ {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] (c c' : C) (d : D),
  (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso c c' d).hom =
    (CategoryTheory.Functor.OplaxMonoidal.δ F c c').unmop.app d
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.lift_iSup_le_iff : ∀ {ι : Type v} {f : ι → Cardinal.{w}},
  BddAbove (Set.range f) →
    ∀ {t : Cardinal.{max u w}}, Cardinal.lift.{u, w} (iSup f) ≤ t ↔ ∀ (i : ι), Cardinal.lift.{u, w} (f i) ≤ t
-- Init.Data.Array.Lemmas
Array.flatten_eq_empty_iff : ∀ {α : Type u_1} {xss : Array (Array α)}, xss.flatten = #[] ↔ ∀ xs ∈ xss, xs = #[]
-- Mathlib.Algebra.Module.Torsion.Basic
_private.Mathlib.Algebra.Module.Torsion.Basic.0.Submodule.sup_torsionBySet_ideal_eq_torsionBySet_inf.match_1_1.eq_1 : ∀ (motive : Fin 2 → Sort u_1) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1),
  (match 0 with
    | 0 => h_1 ()
    | 1 => h_2 ()) =
    h_1 ()
-- Init.Data.Vector.Basic
/-- Maps elements of a vector using the function `f`.  -/
Vector.map : {α : Type u_1} → {β : Type u_2} → {n : ℕ} → (α → β) → Vector α n → Vector β n
-- Mathlib.MeasureTheory.OuterMeasure.AE
MeasureTheory.union_ae_eq_univ_of_ae_eq_univ_right : ∀ {α : Type u_1} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [inst_1 : MeasureTheory.OuterMeasureClass F α]
  {μ : F} {s t : Set α}, t =ᵐ[μ] Set.univ → s ∪ t =ᵐ[μ] Set.univ
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
LinearMap.mkContinuous.congr_simp : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {F : Type u_4} [inst : Ring 𝕜] [inst_1 : Ring 𝕜₂]
  [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup F] [inst_4 : Module 𝕜 E] [inst_5 : Module 𝕜₂ F]
  {σ : 𝕜 →+* 𝕜₂} (f f_1 : E →ₛₗ[σ] F) (e_f : f = f_1) (C C_1 : ℝ) (e_C : C = C_1) (h : ∀ (x : E), ‖f x‖ ≤ C * ‖x‖),
  f.mkContinuous C h = f_1.mkContinuous C_1 ⋯
-- Mathlib.Combinatorics.Digraph.Basic
Digraph.emptyDigraph_eq_bot : ∀ (V : Type u_3), Digraph.emptyDigraph V = ⊥
-- Mathlib.Algebra.Free
FreeAddMagma.toFreeAddSemigroup_of : ∀ {α : Type u} (x : α), FreeAddMagma.toFreeAddSemigroup (FreeAddMagma.of x) = FreeAddSemigroup.of x
-- Mathlib.Topology.Algebra.UniformField
CompletableTopField.mk : ∀ {K : Type u_1} [inst : Field K] [inst_1 : UniformSpace K] [toT0Space : T0Space K],
  (∀ (F : Filter K), Cauchy F → nhds 0 ⊓ F = ⊥ → Cauchy (Filter.map (fun x => x⁻¹) F)) → CompletableTopField K
-- Mathlib.Algebra.Category.MonCat.Basic
AddEquiv.toAddMonCatIso_inv : ∀ {X Y : Type u} [inst : AddMonoid X] [inst_1 : AddMonoid Y] (e : X ≃+ Y),
  e.toAddMonCatIso.inv = AddMonCat.ofHom e.symm.toAddMonoidHom
-- Mathlib.Data.List.Sigma
List.NodupKeys.eq_of_fst_eq : ∀ {α : Type u} {β : α → Type v} {l : List (Sigma β)},
  l.NodupKeys → ∀ {s s' : Sigma β}, s ∈ l → s' ∈ l → s.fst = s'.fst → s = s'
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.DropWhile
Std.IterM.dropWhile_eq_intermediateDropWhile : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Monad m] [Std.Iterator α m β] {it : Std.IterM m β}
  {P : β → Bool}, Std.IterM.dropWhile P it = Std.IterM.Intermediate.dropWhile P true it
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.Expr.toPolyC.go.match_4.eq_2 : ∀ (motive : Lean.Grind.CommRing.Expr → Sort u_1) (k : ℕ) (h_1 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.num k))
  (h_2 : (k : ℕ) → motive (Lean.Grind.CommRing.Expr.natCast k))
  (h_3 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.intCast k))
  (h_4 : (x : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var x))
  (h_5 : (a b : Lean.Grind.CommRing.Expr) → motive (a.add b))
  (h_6 : (a b : Lean.Grind.CommRing.Expr) → motive (a.mul b)) (h_7 : (a : Lean.Grind.CommRing.Expr) → motive a.neg)
  (h_8 : (a b : Lean.Grind.CommRing.Expr) → motive (a.sub b))
  (h_9 : (a : Lean.Grind.CommRing.Expr) → (k : ℕ) → motive (a.pow k)),
  (match Lean.Grind.CommRing.Expr.natCast k with
    | Lean.Grind.CommRing.Expr.num k => h_1 k
    | Lean.Grind.CommRing.Expr.natCast k => h_2 k
    | Lean.Grind.CommRing.Expr.intCast k => h_3 k
    | Lean.Grind.CommRing.Expr.var x => h_4 x
    | a.add b => h_5 a b
    | a.mul b => h_6 a b
    | a.neg => h_7 a
    | a.sub b => h_8 a b
    | a.pow k => h_9 a k) =
    h_2 k
-- Mathlib.Tactic.Ring.Common
/-- A product `x ^ e * b` is a monomial if `b` is a monomial. Here `x` is an `ExBase`
and `e` is an `ExProdNat` representing a monomial expression in `ℕ` (it is a monomial instead of
a polynomial because we eagerly normalize `x ^ (a + b) = x ^ a * x ^ b`.)
 -/
Mathlib.Tactic.Ring.Common.ExProd.mul : {u : Lean.Level} →
  {α : Q(Type u)} →
    {BaseType : Q(«$α») → Type} →
      {sα : Q(CommSemiring «$α»)} →
        {x : Q(«$α»)} →
          {e : Q(ℕ)} →
            {b : Q(«$α»)} →
              Mathlib.Tactic.Ring.Common.ExBase BaseType sα x →
                Mathlib.Tactic.Ring.Common.ExProdNat e →
                  Mathlib.Tactic.Ring.Common.ExProd BaseType sα b →
                    Mathlib.Tactic.Ring.Common.ExProd BaseType sα q(«$x» ^ «$e» * «$b»)
-- Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
RootPairing.Polarization.eq_1 : ∀ {ι : 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] (P : RootPairing ι R M N) [inst_5 : Fintype ι],
  P.Polarization = ∑ i, LinearMap.toSpanSingleton R N (P.coroot i) ∘ₗ P.coroot' i
-- Mathlib.Algebra.Order.Monoid.Submonoid
/-- A submonoid of an ordered monoid is an ordered monoid.  -/
SubmonoidClass.toIsOrderedMonoid : ∀ {M : Type u_1} {S : Type u_2} [inst : SetLike S M] [inst_1 : CommMonoid M] [inst_2 : Preorder M] [IsOrderedMonoid M]
  [inst_4 : SubmonoidClass S M] (s : S), IsOrderedMonoid ↥s
-- Mathlib.Algebra.Module.Hom
/-- The tautological action by `AddMonoid.End α` on `α`.

This generalizes `AddMonoid.End.applyDistribMulAction`.  -/
AddMonoid.End.applyModule : {A : Type u_4} → [inst : AddCommMonoid A] → Module (AddMonoid.End A) A
-- Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
AlgebraicGeometry.Scheme.AffineZariskiSite.toOpens_injective : ∀ {X : AlgebraicGeometry.Scheme}, Function.Injective AlgebraicGeometry.Scheme.AffineZariskiSite.toOpens
-- Mathlib.LinearAlgebra.Matrix.Hermitian
/-- A diagonal matrix is Hermitian if each diagonal entry is self-adjoint  -/
Matrix.isHermitian_diagonal_iff : ∀ {α : Type u_1} {n : Type u_4} [inst : AddMonoid α] [inst_1 : StarAddMonoid α] [inst_2 : DecidableEq n] {d : n → α},
  (Matrix.diagonal d).IsHermitian ↔ ∀ (i : n), IsSelfAdjoint (d i)
-- Lean.Meta.Tactic.Grind.EMatchTheorem
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.NormalizePattern.ParentKind.noConfusionType : Sort v✝ → Lean.Meta.Grind.NormalizePattern.ParentKind✝ → Lean.Meta.Grind.NormalizePattern.ParentKind✝ → Sort v✝
-- Init.Data.Range.Polymorphic.Char
Char.instLawfulUpwardEnumerableLT : Std.PRange.LawfulUpwardEnumerableLT Char
-- Init.Data.Nat.Lemmas
Nat.add_left_min_self : ∀ {a b : ℕ}, min (b + a) a = a
-- Mathlib.LinearAlgebra.Dual.Basis
Module.Basis.toDual_inj : ∀ {R : Type uR} {M : Type uM} {ι : Type uι} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : DecidableEq ι] (b : Module.Basis ι R M) (m : M), b.toDual m = 0 → m = 0
-- Mathlib.CategoryTheory.Bicategory.Extension
CategoryTheory.Bicategory.LeftLift.whiskerOfIdCompIsoSelf_inv_right : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a}
  (t : CategoryTheory.Bicategory.LeftLift f g),
  t.whiskerOfIdCompIsoSelf.inv.right = (CategoryTheory.Bicategory.leftUnitor t.lift).inv
-- Mathlib.MeasureTheory.Measure.GiryMonad
/-- Measurability structure on `Measure`: Measures are measurable w.r.t. all projections  -/
MeasureTheory.Measure.instMeasurableSpace : {α : Type u_1} → {mα : MeasurableSpace α} → MeasurableSpace (MeasureTheory.Measure α)
-- Mathlib.AlgebraicGeometry.Cover.Directed
AlgebraicGeometry.Scheme.Cover.instIsLocallyDirectedI₀CompFunctorOfLocallyDirectedForget : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {X : AlgebraicGeometry.Scheme}
  (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X)
  [inst : CategoryTheory.Category.{v_1, u_1} 𝒰.I₀] [inst_1 : 𝒰.LocallyDirected],
  (𝒰.functorOfLocallyDirected.comp AlgebraicGeometry.Scheme.forget).IsLocallyDirected
-- Lean.Meta.Basic
_private.Lean.Meta.Basic.0.Lean.Meta.withNewMCtxDepthImp : {α : Type} → Bool → Lean.MetaM α → Lean.MetaM α
-- Mathlib.Data.Nat.ModEq
Nat.add_modulus_modEq_iff : ∀ {n a b : ℕ}, a + n ≡ b [MOD n] ↔ a ≡ b [MOD n]
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SignatureInformation.mk : String →
  Option Lean.Lsp.MarkupContent →
    Option (Array Lean.Lsp.ParameterInformation) → Option ℕ → Lean.Lsp.SignatureInformation
-- Mathlib.SetTheory.Cardinal.Finite
Nat.card_fun : ∀ {α : Type u_1} {β : Type u_2} [Finite α], Nat.card (α → β) = Nat.card β ^ Nat.card α
-- Mathlib.RingTheory.Ideal.Operations
Ideal.isCoprime_iff_sup_eq : ∀ {R : Type u} [inst : CommSemiring R] {I J : Ideal R}, IsCoprime I J ↔ I ⊔ J = ⊤
-- Std.Async.System
_private.Std.Async.System.0.Std.Async.System.Environment.mk : Std.HashMap String String → Std.Async.System.Environment
-- Mathlib.NumberTheory.ModularForms.Basic
CuspForm.instIsScalarTowerComplex : ∀ {α : Type u_2} [inst : SMul α ℝ] [inst_1 : SMul α ℂ] [IsScalarTower α ℝ ℂ], IsScalarTower α ℂ ℂ
-- Mathlib.Algebra.Group.TypeTags.Basic
Additive.subtractionCommMonoid : {α : Type u} → [DivisionCommMonoid α] → SubtractionCommMonoid (Additive α)
-- Init.Data.Range.Polymorphic.Internal.SignedBitVec
_private.Init.Data.Range.Polymorphic.Internal.SignedBitVec.0.BitVec.Signed.instRxoLawfulHasSize : ∀ {n : ℕ}, Std.Rxo.LawfulHasSize (BitVec n)
-- Mathlib.Combinatorics.Matroid.Minor.Contract
/-- Contraction and deletion commute for disjoint sets.  -/
Matroid.contract_delete_comm : ∀ {α : Type u_1} {D C : Set α} (M : Matroid α), Disjoint C D → (M.contract C).delete D = (M.delete D).contract C
-- Init.Data.List.Zip
List.zipWith_eq_cons_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {g : γ} {l : List γ} {f : α → β → γ} {l₁ : List α} {l₂ : List β},
  List.zipWith f l₁ l₂ = g :: l ↔ ∃ a l₁' b l₂', l₁ = a :: l₁' ∧ l₂ = b :: l₂' ∧ g = f a b ∧ l = List.zipWith f l₁' l₂'
-- Init.Data.List.MinMaxIdx
/-- Returns the index of an element of `xs` that minimizes `f`. If `x`, `y`
are such that `f x = f y`, it returns the index of whichever comes first in the list.
Returns `none` if the list is empty.

The correctness of this function assumes `β` to be linearly pre-ordered.
 -/
List.minIdxOn? : {β : Type u_1} → {α : Type u_2} → [inst : LE β] → [DecidableLE β] → (α → β) → List α → Option ℕ
-- Mathlib.Algebra.Order.Chebyshev
/-- **Chebyshev's Sum Inequality**: When `f` and `g` monovary together (e.g. they are both
monotone/antitone), the product of their sum is less than the size of the set times their scalar
product.  -/
Monovary.sum_mul_sum_le_card_mul_sum : ∀ {ι : Type u_1} {α : Type u_2} [inst : Semiring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α]
  {f g : ι → α} [inst_4 : Fintype ι], Monovary f g → (∑ i, f i) * ∑ i, g i ≤ ↑(Fintype.card ι) * ∑ i, f i * g i
-- Mathlib.Combinatorics.Quiver.Schreier
Quiver.SchreierGraph.ofVertex.injEq : ∀ {V : Type u_1} {M : Type u_2} [inst : SMul M V] {S : Type u_3} {_ι : S → M} (toVertex toVertex_1 : V),
  ({ toVertex := toVertex } = { toVertex := toVertex_1 }) = (toVertex = toVertex_1)
-- Mathlib.Order.WellFounded
/-- Given a function `f : α → β` where `β` carries a well-founded `<`, this is an element of `α`
whose image under `f` is minimal in the sense of `Function.not_lt_argmin`.

See also `Set.Finite.exists_minimalFor` and related lemmas for the case when `α` is finite.  -/
Function.argmin : {α : Type u_1} → {β : Type u_2} → (α → β) → [inst : LT β] → [WellFoundedLT β] → [Nonempty α] → α
-- Mathlib.Analysis.Normed.Algebra.Exponential
NormedSpace.expSeries_summable' : ∀ {𝕂 : Type u_1} {𝔸 : Type u_2} [inst : NontriviallyNormedField 𝕂] [inst_1 : CharZero 𝕂] [ContinuousSMul ℚ 𝕂]
  [inst_3 : NormedRing 𝔸] [inst_4 : NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] (x : 𝔸),
  Summable fun n => (↑n.factorial)⁻¹ • x ^ n
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.GrothendieckTopology.OneHypercover.instCategory : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {S : C} → CategoryTheory.Category.{max v u_2, max (max u v) (u_2 + 1)} (J.OneHypercover S)
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
Summable.nat_add_neg_add_one : ∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M] {f : ℤ → M},
  Summable f → Summable fun n => f ↑n + f (-(↑n + 1))
-- Mathlib.Combinatorics.SimpleGraph.Diam
SimpleGraph.dist_le_diam : ∀ {α : Type u_1} {G : SimpleGraph α}, G.ediam ≠ ⊤ → ∀ {u v : α}, G.dist u v ≤ G.diam
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
GaloisConnection.u_csInf : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLattice α] [inst_1 : ConditionallyCompleteLattice β]
  {l : α → β} {u : β → α}, GaloisConnection l u → ∀ {s : Set β}, s.Nonempty → BddBelow s → u (sInf s) = ⨅ x, u ↑x
-- Mathlib.Algebra.BigOperators.Expect
Finset.expect_const_zero : ∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : Module ℚ≥0 M] (s : Finset ι),
  (s.expect fun _i => 0) = 0
-- Mathlib.Algebra.Homology.Bifunctor
HomologicalComplex.ιMapBifunctorOrZero_eq_zero : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} D] {I₁ : Type u_4}
  {I₂ : Type u_5} {J : Type u_6} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂}
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C₁] [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C₂]
  [inst_5 : CategoryTheory.Preadditive D] (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂)
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [inst_6 : F.PreservesZeroMorphisms]
  [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (c : ComplexShape J) [inst_8 : TotalComplexShape c₁ c₂ c]
  [inst_9 : K₁.HasMapBifunctor K₂ F c] [inst_10 : DecidableEq J] (i₁ : I₁) (i₂ : I₂) (j : J),
  c₁.π c₂ c (i₁, i₂) ≠ j → K₁.ιMapBifunctorOrZero K₂ F c i₁ i₂ j = 0
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.IntegrableAtFilter.inf_of_left : ∀ {α : Type u_1} {ε : Type u_3} {mα : MeasurableSpace α} {f : α → ε} {μ : MeasureTheory.Measure α}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε] {l l' : Filter α},
  MeasureTheory.IntegrableAtFilter f l μ → MeasureTheory.IntegrableAtFilter f (l ⊓ l') μ
-- Mathlib.Data.ENNReal.Basic
Set.OrdConnected.preimage_ennreal_ofReal : ∀ {u : Set ENNReal}, u.OrdConnected → (ENNReal.ofReal ⁻¹' u).OrdConnected
-- Mathlib.Algebra.MonoidAlgebra.Module
MonoidAlgebra.basis_apply : ∀ {R : Type u_1} (k : Type u_7) [inst : Semiring k] (r : R), (MonoidAlgebra.basis R k) r = MonoidAlgebra.single r 1
-- Mathlib.LinearAlgebra.Span.Basic
/-- If two linear maps are equal on a set `s`, then they are equal on `Submodule.span s`.

See also `LinearMap.eqOn_span'` for a version using `Set.EqOn`.  -/
LinearMap.eqOn_span : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : Semiring R₂] [inst_4 : AddCommMonoid M₂] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  {s : Set M} {f g : M →ₛₗ[σ₁₂] M₂}, Set.EqOn (⇑f) (⇑g) s → ∀ ⦃x : M⦄, x ∈ Submodule.span R s → f x = g x
-- Mathlib.Algebra.Category.Ring.Basic
/-- The underlying ring hom.  -/
CommRingCat.Hom.hom : {R S : CommRingCat} → R.Hom S → ↑R →+* ↑S
-- Init.Data.UInt.Lemmas
UInt64.toUInt16_mod : ∀ (a b : UInt64), a < 65536 → b < 65536 → (a % b).toUInt16 = a.toUInt16 % b.toUInt16
-- Mathlib.Data.Ordmap.Invariants
Ordnode.splitMin'.eq_2 : ∀ {α : Type u_1} (x : α) (x_1 : Ordnode α) (size : ℕ) (ll : Ordnode α) (lx : α) (lr : Ordnode α),
  (Ordnode.node size ll lx lr).splitMin' x x_1 =
    match ll.splitMin' lx lr with
    | (xm, l') => (xm, l'.balanceR x x_1)
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
CategoryTheory.Pretriangulated.Triangle.yoneda_exact₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C],
  ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles,
    ∀ {X : C} (f : T.obj₂ ⟶ X),
      CategoryTheory.CategoryStruct.comp T.mor₁ f = 0 → ∃ g, f = CategoryTheory.CategoryStruct.comp T.mor₂ g
-- Mathlib.Topology.UniformSpace.CompactConvergence
/-- A family `f : X → α → β`, each of which is continuous on a compact set `s : Set α` is
continuous in the topology `X → α →ᵤ[{s}] β` if and only if the family of continuous restrictions
`X → C(s, β)` is continuous.  -/
ContinuousOn.continuous_domRestrict_iff_continuous_uniformOnFun : ∀ {α : Type u₁} {β : Type u₂} [inst : TopologicalSpace α] [inst_1 : UniformSpace β] {X : Type u_1}
  [inst_2 : TopologicalSpace X] {f : X → α → β} {s : Set α} (hf : ∀ (x : X), ContinuousOn (f x) s) [CompactSpace ↑s],
  (Continuous fun x => { toFun := s.domRestrict (f x), continuous_toFun := ⋯ }) ↔
    Continuous fun x => (UniformOnFun.ofFun {s}) (f x)
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.braiding_rightUnitor_aux₁ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X : C),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator X (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
          (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight
          (β_ (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X).inv
          (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X
              (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom
          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
            (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom))) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X
        (CategoryTheory.MonoidalCategoryStruct.rightUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom)
      (β_ (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X).inv