mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.TwoSidedIdeal.Operations
TwoSidedIdeal.coe_mop_smul : ∀ {R : Type u_1} [inst : Ring R] (I : TwoSidedIdeal R) {r : Rᵐᵒᵖ} {x : ↥I}, r • ↑x = ↑x * MulOpposite.unop r
-- Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset
Finset.smul_neg : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] [inst_1 : Monoid α] [inst_2 : AddGroup β]
  [inst_3 : DistribMulAction α β] (s : Finset α) (t : Finset β), s • -t = -(s • t)
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.MethodSpecs
/-- This simproc reduces `_ == _` when both arguments are constructor applications and the `BEq` instance
in question has been annotated with `@[method_specs]`.
 -/
reduceBEq : Lean.Meta.Simp.Simproc
-- Mathlib.Order.Filter.Pointwise
Filter.vadd_le_vadd_left : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] {f : Filter α} {g₁ g₂ : Filter β}, g₁ ≤ g₂ → f +ᵥ g₁ ≤ f +ᵥ g₂
-- Mathlib.Algebra.BigOperators.Expect
Finset.expect_congr : ∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : Module ℚ≥0 M] {s : Finset ι} {f g : ι → M}
  {t : Finset ι}, s = t → (∀ i ∈ t, f i = g i) → (s.expect fun i => f i) = t.expect fun i => g i
-- Mathlib.NumberTheory.NumberField.Basic
NumberField.to_charZero : ∀ {K : Type u_1} {inst : Field K} [self : NumberField K], CharZero K
-- Mathlib.Analysis.InnerProductSpace.Orthonormal
/-- `if ... then ... else` characterization of an indexed set of vectors being orthonormal.  (Inner
product equals Kronecker delta.)  -/
orthonormal_iff_ite : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_4} [inst_3 : DecidableEq ι] {v : ι → E},
  Orthonormal 𝕜 v ↔ ∀ (i j : ι), inner 𝕜 (v i) (v j) = if i = j then 1 else 0
-- Mathlib.Topology.MetricSpace.CoveringNumbers
Metric.maximalSeparatedSet.eq_1 : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] (ε : NNReal) (A : Set X),
  Metric.maximalSeparatedSet ε A = if h : Metric.packingNumber ε A ≠ ⊤ then ⋯.choose else ∅
-- Mathlib.CategoryTheory.Groupoid.FreeGroupoid
Quiver.FreeGroupoid.redStep.step : ∀ {V : Type u} [inst : Quiver V] (X Z : Quiver.Symmetrify V) (f : X ⟶ Z),
  Quiver.FreeGroupoid.redStep (CategoryTheory.CategoryStruct.id ((CategoryTheory.Paths.of (Quiver.Symmetrify V)).obj X))
    (CategoryTheory.CategoryStruct.comp f.toPath (Quiver.reverse f).toPath)
-- Std.Time.Format.Modifier
Std.Time.ExtendedDayPeriod.noConfusionType : Sort v✝ → Std.Time.ExtendedDayPeriod → Std.Time.ExtendedDayPeriod → Sort v✝
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.PushoutObjObj.flip_pt : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)} {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} {X₂ Y₂ : C₂} {f₂ : X₂ ⟶ Y₂}
  (sq : F.PushoutObjObj f₁ f₂), sq.flip.pt = sq.pt
-- Init.Coe
/-- Coerces a value of type `α` to type `β`. Accessible by the notation `↑x`,
or by double type ascription `((x : α) : β)`.  -/
CoeOut.coe : {α : Sort u} → {β : semiOutParam (Sort v)} → [self : CoeOut α β] → α → β
-- Mathlib.Algebra.Polynomial.EraseLead
/-- If we erase the leading coefficient of a `Polynomial.coeffList` like [+,0,...], and then
multiply by a linear term, it's equivalent to erasing the first two coefficients of the product.  -/
Polynomial.eraseLead_mul_eq_mul_eraseLead_of_nextCoeff_zero : ∀ {R : Type u_2} [inst : Ring R] [NoZeroDivisors R] [Nontrivial R] {x : R} {P : Polynomial R},
  x ≠ 0 →
    P.nextCoeff = 0 →
      ((Polynomial.X - Polynomial.C x) * P).eraseLead.eraseLead = (Polynomial.X - Polynomial.C x) * P.eraseLead
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.RuleExpr.node.inj : ∀ {f : Aesop.Frontend.Feature} {children : Array Aesop.Frontend.RuleExpr} {f_1 : Aesop.Frontend.Feature}
  {children_1 : Array Aesop.Frontend.RuleExpr},
  Aesop.Frontend.RuleExpr.node f children = Aesop.Frontend.RuleExpr.node f_1 children_1 →
    f = f_1 ∧ children = children_1
-- Mathlib.LinearAlgebra.AffineSpace.Independent
/-- Given an affinely independent family of points, suppose that an affine combination lies in
the span of one point of that family and a combination of another two points of that family given
by `lineMap` with coefficient between 0 and 1. Then the coefficients of those two points in the
combination lying in the span have the same sign.  -/
sign_eq_of_affineCombination_mem_affineSpan_single_lineMap : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : LinearOrder k] [IsStrictOrderedRing k]
  [inst_3 : AddCommGroup V] [inst_4 : Module k V] [inst_5 : AddTorsor V P] {ι : Type u_4} {p : ι → P},
  AffineIndependent k p →
    ∀ {w : ι → k} {s : Finset ι},
      ∑ i ∈ s, w i = 1 →
        ∀ {i₁ i₂ i₃ : ι},
          i₁ ∈ s →
            i₂ ∈ s →
              i₃ ∈ s →
                i₁ ≠ i₂ →
                  i₁ ≠ i₃ →
                    i₂ ≠ i₃ →
                      ∀ {c : k},
                        0 < c →
                          c < 1 →
                            (Finset.affineCombination k s p) w ∈ line[k, p i₁, (AffineMap.lineMap (p i₂) (p i₃)) c] →
                              SignType.sign (w i₂) = SignType.sign (w i₃)
-- Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
/-- In a Turán-maximal graph, non-adjacency is transitive.  -/
SimpleGraph.IsTuranMaximal.not_adj_trans : ∀ {V : Type u_1} [inst : Fintype V] {G : SimpleGraph V} [inst_1 : DecidableRel G.Adj] {r : ℕ} {s t u : V},
  G.IsTuranMaximal r → ¬G.Adj t s → ¬G.Adj s u → ¬G.Adj t u
-- Init.Data.String.Lemmas.Pattern.String.Basic
String.Slice.Pattern.Model.ForwardStringSearcher.strictPatternModel : ∀ {pat : String}, pat ≠ "" → String.Slice.Pattern.Model.StrictPatternModel pat
-- Mathlib.Analysis.Convex.Independent
/-- If an indexed family of points is convex independent, so is the corresponding set of points.  -/
ConvexIndependent.range : ∀ {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] {p : ι → E}, ConvexIndependent 𝕜 p → ConvexIndependent 𝕜 Subtype.val
-- Mathlib.CategoryTheory.Triangulated.SpectralObject
CategoryTheory.Triangulated.SpectralObject.Hom.comm_assoc : ∀ {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 Y : CategoryTheory.Triangulated.SpectralObject C ι} (self : X.Hom Y) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) {Z : C}
  (h : (CategoryTheory.shiftFunctor C 1).obj (Y.ω₁.obj (CategoryTheory.ComposableArrows.mk₁ f)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.δ f g)
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.shiftFunctor C 1).map (self.hom.app (CategoryTheory.ComposableArrows.mk₁ f))) h) =
    CategoryTheory.CategoryStruct.comp (self.hom.app (CategoryTheory.ComposableArrows.mk₁ g))
      (CategoryTheory.CategoryStruct.comp (Y.δ f g) h)
-- Mathlib.Analysis.Real.Cardinality
Cardinal.not_countable_real : ¬Set.univ.Countable
-- Lean.Meta.Match.Match
_private.Lean.Meta.Match.Match.0.Lean.Meta.Match.MatcherKey.compile : Lean.Meta.Match.MatcherKey✝ → Bool
-- Lean.Meta.Tactic.Grind.Util
/-- Beta-reduces the goal's target.
 -/
Lean.MVarId.betaReduce : Lean.MVarId → Lean.MetaM Lean.MVarId
-- Init.System.ST
/-- Atomically swaps the value of a mutable reference cell with another value. The reference cell's
original value is returned.
 -/
ST.Ref.swap : {σ : Type} → {m : Type → Type} → [MonadLiftT (ST σ) m] → {α : Type} → ST.Ref σ α → α → m α
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.support_monomial_subset : ∀ {R : Type u} [inst : Semiring R] (n : ℕ) (a : R), ((Polynomial.monomial n) a).support ⊆ {n}
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_roo_eq_toList_rco : ∀ {m n : ℕ}, (m<...n).toList = ((m + 1)...n).toList
-- Mathlib.Analysis.Complex.Isometry
rotation_symm : ∀ (a : Circle), (rotation a).symm = rotation a⁻¹
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {s t : CategoryTheory.Limits.Cocone F} (P : CategoryTheory.Limits.IsColimit s)
  (Q : CategoryTheory.Limits.IsColimit t),
  P.coconePointUniqueUpToIso Q = (CategoryTheory.Limits.Cocone.forget F).mapIso (P.uniqueUpToIso Q)
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.eq_symm_apply : ∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) {x : α} {y : β},
  x ∈ e.source → y ∈ e.target → (x = ↑e.symm y ↔ ↑e x = y)
-- Mathlib.Order.Filter.Finite
Filter.frequently_exists_finset : ∀ {α : Type u} {ι : Type u_2} (I : Finset ι) {l : Filter α} {p : ι → α → Prop},
  (∃ᶠ (x : α) in l, ∃ i ∈ I, p i x) ↔ ∃ i ∈ I, ∃ᶠ (x : α) in l, p i x
-- Lean.Meta.Tactic.Simp.SimpAll
Lean.Meta.SimpAll.Entry.mk : Lean.FVarId → Lean.Name → Lean.Meta.Origin → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Meta.SimpAll.Entry
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.degree_mem_support : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] {p : MvPolynomial σ R},
  p ≠ 0 → m.degree p ∈ p.support
-- Mathlib.CategoryTheory.Skeletal
/-- The equivalence between the skeleton and the category itself.  -/
CategoryTheory.skeletonEquivalence : (C : Type u₁) → [inst : CategoryTheory.Category.{v₁, u₁} C] → CategoryTheory.Skeleton C ≌ C
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
/-- The monoid homomorphism from a given monoid in the diagram to the colimit monoid.  -/
MonCat.FilteredColimits.coconeMorphism : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    (F : CategoryTheory.Functor J MonCat) →
      [inst_1 : CategoryTheory.IsFiltered J] → (j : J) → F.obj j ⟶ MonCat.FilteredColimits.colimit F
-- Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
/-- A functor `F : J ⥤ C` from a cofiltered category is eventually constant if there
exists `j : J`, such that for any `f : i ⟶ j`, the induced map `F.map f` is an isomorphism.  -/
CategoryTheory.IsCofiltered.IsEventuallyConstant : {J : Type u_1} →
  {C : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} J] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} C] → CategoryTheory.Functor J C → Prop
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.Subcomplex.mk.injEq : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : Topology.RelCWComplex C D] (carrier : Set X)
  (I : (n : ℕ) → Set (Topology.RelCWComplex.cell C n)) (closed' : IsClosed carrier)
  (union' : D ∪ ⋃ n, ⋃ j, Topology.RelCWComplex.openCell n ↑j = carrier) (carrier_1 : Set X)
  (I_1 : (n : ℕ) → Set (Topology.RelCWComplex.cell C n)) (closed'_1 : IsClosed carrier_1)
  (union'_1 : D ∪ ⋃ n, ⋃ j, Topology.RelCWComplex.openCell n ↑j = carrier_1),
  ({ carrier := carrier, I := I, closed' := closed', union' := union' } =
      { carrier := carrier_1, I := I_1, closed' := closed'_1, union' := union'_1 }) =
    (carrier = carrier_1 ∧ I = I_1)
-- Mathlib.NumberTheory.Pell
/-- If a fundamental solution exists, then `d` must be a non-square.  -/
Pell.IsFundamental.d_nonsquare : ∀ {d : ℤ} {a : Pell.Solution₁ d}, Pell.IsFundamental a → ¬IsSquare d
-- Mathlib.RingTheory.SimpleRing.Basic
IsSimpleRing.instNontrivial : ∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R] [IsSimpleRing R], Nontrivial R
-- Mathlib.Order.Interval.Finset.Fin
Fin.map_valEmbedding_Ioc : ∀ {n : ℕ} (a b : Fin n), Finset.map Fin.valEmbedding (Finset.Ioc a b) = Finset.Ioc ↑a ↑b
-- Mathlib.RingTheory.FinitePresentation
RingHom.FinitePresentation.eq_1 : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] (f : A →+* B),
  f.FinitePresentation = Algebra.FinitePresentation A B
-- Mathlib.Order.Filter.Bases.Basic
Filter.HasBasis.le_iff : ∀ {α : Type u_1} {ι : Sort u_4} {l l' : Filter α} {p : ι → Prop} {s : ι → Set α},
  l.HasBasis p s → (l ≤ l' ↔ ∀ t ∈ l', ∃ i, p i ∧ s i ⊆ t)
-- Mathlib.RingTheory.AdicCompletion.RingHom
/-- `AlgHom` version of `IsAdicCompletion.liftRingHom`.  -/
IsAdicComplete.liftAlgHom : {R : Type u_3} →
  {S : Type u_4} →
    {A : Type u_5} →
      [inst : CommRing R] →
        [inst_1 : CommRing S] →
          [inst_2 : Algebra R S] →
            (I : Ideal S) →
              [IsAdicComplete I S] →
                [inst_4 : CommRing A] →
                  [inst_5 : Algebra R A] →
                    (f : (n : ℕ) → A →ₐ[R] S ⧸ I ^ n) →
                      (∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorₐ R ⋯).comp (f n) = f m) → A →ₐ[R] S
-- Mathlib.Combinatorics.SimpleGraph.Hamiltonian
/-- The support of a Hamiltonian walk is the entire vertex set.  -/
SimpleGraph.Walk.IsHamiltonian.toFinset_support : ∀ {α : Type u_1} [inst : DecidableEq α] {G : SimpleGraph α} {a b : α} {p : G.Walk a b} [inst_1 : Fintype α],
  p.IsHamiltonian → p.support.toFinset = Finset.univ
-- Mathlib.Algebra.Module.Equiv.Basic
LinearMap.piApply_apply : ∀ {R : Type u_1} {M : Type u_5} {V : M → Type u_9} [inst : CommSemiring R] [inst_1 : (x : M) → AddCommMonoid (V x)]
  [inst_2 : (x : M) → Module R (V x)] (e : (x : M) → V x →ₗ[R] R) (s : (x : M) → V x),
  (LinearMap.piApply e) s = fun x => (e x) (s x)
-- Init.Data.Option.Lemmas
Option.pmap.eq_2 : ∀ {α : Type u_1} {β : Type u_2} {p : α → Prop} (f : (a : α) → p a → β) (a : α)
  (H : ∀ (a_1 : α), some a = some a_1 → p a_1), Option.pmap f (some a) H = some (f a ⋯)
-- Mathlib.Algebra.Group.Submonoid.Membership
Submonoid.powLogEquiv_symm_apply : ∀ {M : Type u_1} [inst : Monoid M] [inst_1 : DecidableEq M] {n : M} (h : Function.Injective fun m => n ^ m)
  (m : ↥(Submonoid.powers n)), (Submonoid.powLogEquiv h).symm m = Multiplicative.ofAdd (Submonoid.log m)
-- Mathlib.CategoryTheory.EssentiallySmall
CategoryTheory.ShrinkHoms.instUnique : {T : Type u} → [Unique T] → Unique (CategoryTheory.ShrinkHoms.{u} T)
-- Lean.Meta.Sym.SymM
/-- Returns the internalized `0 : Nat` numeral.   -/
Lean.Meta.Sym.getNatZeroExpr : Lean.Meta.Sym.SymM Lean.Expr
-- Mathlib.Analysis.Convex.Mul
ConvexOn.mul_concaveOn : ∀ {𝕜 : Type u_1} {E : Type u_2} {G : Type u_4} [inst : CommRing 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : CommRing E] [inst_4 : LinearOrder E] [IsStrictOrderedRing E] [inst_6 : AddCommGroup G] [inst_7 : Module 𝕜 G]
  [inst_8 : Module 𝕜 E] {s : Set G} [IsOrderedModule 𝕜 E] [IsScalarTower 𝕜 E E] [SMulCommClass 𝕜 E E] {f g : G → E},
  ConvexOn 𝕜 s f →
    ConcaveOn 𝕜 s g →
      (∀ ⦃x : G⦄, x ∈ s → 0 ≤ f x) → (∀ ⦃x : G⦄, x ∈ s → g x ≤ 0) → AntivaryOn f g s → ConcaveOn 𝕜 s (f * g)
-- Mathlib.Order.GameAdd
/-- **Alias** of `Prod.GameAdd.recursion`.

---

Recursion on the well-founded `Prod.GameAdd` relation.
Note that it's strictly more general to recurse on the lexicographic order instead.  -/
Prod.GameAdd.fix : {α : Type u_1} →
  {β : Type u_2} →
    {rα : α → α → Prop} →
      {rβ : β → β → Prop} →
        {C : α → β → Sort u_3} →
          WellFounded rα →
            WellFounded rβ →
              ((a₁ : α) → (b₁ : β) → ((a₂ : α) → (b₂ : β) → Prod.GameAdd rα rβ (a₂, b₂) (a₁, b₁) → C a₂ b₂) → C a₁ b₁) →
                (a : α) → (b : β) → C a b
-- Mathlib.Topology.DenseEmbedding
DenseRange.induction_on₃ : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {e : α → β} {p : β → β → β → Prop},
  DenseRange e →
    IsClosed {q | p q.1 q.2.1 q.2.2} → (∀ (a₁ a₂ a₃ : α), p (e a₁) (e a₂) (e a₃)) → ∀ (b₁ b₂ b₃ : β), p b₁ b₂ b₃
-- Mathlib.CategoryTheory.Limits.Creates
CategoryTheory.LiftableCone.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : Type w} →
          [inst_2 : CategoryTheory.Category.{w', w} J] →
            {K : CategoryTheory.Functor J C} →
              {F : CategoryTheory.Functor C D} →
                {c : CategoryTheory.Limits.Cone (K.comp F)} →
                  (liftedCone : CategoryTheory.Limits.Cone K) →
                    (F.mapCone liftedCone ≅ c) → CategoryTheory.LiftableCone K F c
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.Monic.natDegree_pos : ∀ {R : Type u} [inst : CommSemiring R] {p : Polynomial R}, p.Monic → (0 < p.natDegree ↔ p ≠ 1)
-- Mathlib.Topology.CWComplex.Classical.Subcomplex
Topology.RelCWComplex.Subcomplex.map_def : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : T2Space X] [inst_1 : Topology.RelCWComplex C D]
  (E : Topology.RelCWComplex.Subcomplex C) (n : ℕ) (i : ↑(E.I n)),
  Topology.RelCWComplex.map n i = Topology.RelCWComplex.map n ↑i
-- Mathlib.Algebra.Group.Idempotent
IsIdempotentElem.pow : ∀ {M : Type u_1} [inst : Monoid M] {a : M} (n : ℕ), IsIdempotentElem a → IsIdempotentElem (a ^ n)
-- Mathlib.Algebra.Group.Prod
AddEquiv.prodCongr.eq_1 : ∀ {M : Type u_3} {N : Type u_4} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {M' : Type u_6} {N' : Type u_7}
  [inst_2 : AddZeroClass N'] [inst_3 : AddZeroClass M'] (f : M ≃+ M') (g : N ≃+ N'),
  f.prodCongr g = { toEquiv := f.prodCongr g.toEquiv, map_add' := ⋯ }
-- Mathlib.Data.TypeVec
/-- Extensionality for arrows  -/
TypeVec.Arrow.ext : ∀ {n : ℕ} {α : TypeVec.{u} n} {β : TypeVec.{v} n} (f g : α.Arrow β), (∀ (i : Fin2 n), f i = g i) → f = g
-- Std.Sync.StreamMap
Std.AnyAsyncStream.mk.injEq : ∀ {α t : Type} [inst : Std.Async.IO.AsyncStream t α] (a : t) (t_1 : Type) (inst_1 : Std.Async.IO.AsyncStream t_1 α)
  (a_1 : t_1), (Std.AnyAsyncStream.mk a = Std.AnyAsyncStream.mk a_1) = (t = t_1 ∧ inst ≍ inst_1 ∧ a ≍ a_1)
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.support_C_subset : ∀ {R : Type u} [inst : Semiring R] (a : R), (Polynomial.C a).support ⊆ {0}
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getD_eq_fallback : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α], t.WF → ∀ {a : α} {fallback : β a}, a ∉ t → t.getD a fallback = fallback
-- Mathlib.Probability.Decision.Risk.Defs
/-- The minimax risk, defined as the infimum over estimators of the maximal risk of
the estimator.  -/
ProbabilityTheory.minimaxRisk : {Θ : Type u_1} →
  {𝓧 : Type u_2} →
    {𝓨 : Type u_3} →
      {mΘ : MeasurableSpace Θ} →
        {m𝓧 : MeasurableSpace 𝓧} → [MeasurableSpace 𝓨] → (Θ → 𝓨 → ENNReal) → ProbabilityTheory.Kernel Θ 𝓧 → ENNReal
-- Lean.Elab.Tactic.LibrarySearch
Lean.Elab.LibrarySearch.evalApply : Lean.Elab.Tactic.Tactic
-- Mathlib.Analysis.Asymptotics.ExpGrowth
ExpGrowth.le_expGrowthInf_add : ∀ {u v : ℕ → ENNReal}, max (ExpGrowth.expGrowthInf u) (ExpGrowth.expGrowthInf v) ≤ ExpGrowth.expGrowthInf (u + v)
-- Mathlib.SetTheory.Ordinal.Basic
RelIso.ordinalType_congr : ∀ {α β : Type u_1} {r : α → α → Prop} {s : β → β → Prop} [inst : IsWellOrder α r] [inst_1 : IsWellOrder β s]
  (h : r ≃r s), Ordinal.type r = Ordinal.type s
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
/-- Vertical composition of lax transformations.  -/
CategoryTheory.Oplax.LaxTrans.vComp : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G H : CategoryTheory.OplaxFunctor B C} →
          CategoryTheory.Oplax.LaxTrans F G → CategoryTheory.Oplax.LaxTrans G H → CategoryTheory.Oplax.LaxTrans F H
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.restrictAppIso_inv_map_assoc : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.IsOpenImmersion f] (M : Y.Modules)
  {U V : X.Opens} (hUV : Opposite.op V ⟶ Opposite.op U) {Z : Ab} (h : (M.restrict f).presheaf.obj (Opposite.op U) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Modules.restrictAppIso f M V).inv
      (CategoryTheory.CategoryStruct.comp ((M.restrict f).presheaf.map hUV) h) =
    CategoryTheory.CategoryStruct.comp (M.presheaf.map (CategoryTheory.homOfLE ⋯).op)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Modules.restrictAppIso f M U).inv h)
-- Mathlib.Data.UInt
UInt8.toFin_injective : Function.Injective UInt8.toFin
-- Mathlib.MeasureTheory.Measure.Regular
MeasureTheory.Measure.InnerRegular.mk : ∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] {μ : MeasureTheory.Measure α},
  μ.InnerRegularWRT IsCompact MeasurableSet → μ.InnerRegular
-- Mathlib.GroupTheory.Commutator.Basic
/-- If `g` is conjugate to `g ^ 2`, then `g` is a commutator  -/
mem_commutatorSet_of_isConj_sq : ∀ (G : Type u_1) [inst : Group G] {g : G}, IsConj g (g ^ 2) → g ∈ commutatorSet G
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey!_modify_self : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α],
  (↑m).WF →
    ∀ [inst_3 : Inhabited α] {k : α} {f : β k → β k},
      (m.modify k f).getKey! k = if m.contains k = true then k else default
-- Mathlib.Algebra.Module.LinearMap.Polynomial
LinearMap.nilRank.congr_simp : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup L] [inst_2 : Module R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : Module.Free R M] [inst_6 : Module.Finite R M]
  [inst_7 : Module.Finite R L] [inst_8 : Module.Free R L] (φ φ_1 : L →ₗ[R] Module.End R M),
  φ = φ_1 → φ.nilRank = φ_1.nilRank
-- Init.Data.Ord.Basic
Ordering.isEq_iff_eq_eq : ∀ {o : Ordering}, o.isEq = true ↔ o = Ordering.eq
-- Mathlib.Topology.Algebra.Constructions.DomMulAct
DomAddAct.instR1Space : ∀ {M : Type u_1} [inst : TopologicalSpace M] [R1Space M], R1Space Mᵈᵃᵃ
-- Mathlib.CategoryTheory.Functor.EpiMono
/-- **Alias** of `CategoryTheory.Functor.ReflectsMonomorphisms.iso_iff`. -/
CategoryTheory.Functor.reflectsMonomorphisms.iso_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} (α : F ≅ G), F.ReflectsMonomorphisms ↔ G.ReflectsMonomorphisms
-- Mathlib.RepresentationTheory.Invariants
/-- Given a normal subgroup `S ≤ G`, a `G`-representation `ρ` restricts to a `G`-representation on
the invariants of `ρ|_S`.  -/
Representation.toInvariants : {k : Type u_1} →
  {G : Type u_2} →
    [inst : CommRing k] →
      [inst_1 : Group G] →
        {V : Type u_5} →
          [inst_2 : AddCommGroup V] →
            [inst_3 : Module k V] →
              (ρ : Representation k G V) →
                (S : Subgroup G) →
                  [S.Normal] → Representation k G ↥(Representation.invariants (MonoidHom.comp ρ S.subtype))
-- Lean.Parser.Do
Lean.Parser.Term.doLetExpr.formatter : Lean.PrettyPrinter.Formatter
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getD_diff_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α} {fallback : β k}, k ∉ t₂ → (t₁ \ t₂).getD k fallback = t₁.getD k fallback
-- Mathlib.RingTheory.ZMod.UnitsCyclic
ZMod.isCyclic_units_one : IsCyclic (ZMod 1)ˣ
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.toList_filterMap! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} {γ : α → Type w}
  {f : (a : α) → β a → Option (γ a)},
  t.WF →
    (Std.DTreeMap.Internal.Impl.filterMap! f t).toList =
      List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) t.toList
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.isReduced_cons_cons : ∀ {α : Type u} {L : List (α × Bool)} {a b : α × Bool},
  FreeGroup.IsReduced (a :: b :: L) ↔ (a.1 = b.1 → a.2 = b.2) ∧ FreeGroup.IsReduced (b :: L)
-- Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
/-- Variant of `IsFiltered.span` for `κ`-filtered categories.  -/
CategoryTheory.IsCardinalFiltered.wideSpan : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {κ : Cardinal.{w}} [hκ : Fact κ.IsRegular]
  [CategoryTheory.IsCardinalFiltered J κ] {ι : Type v'} {j : J} {k : ι → J} (f : (i : ι) → j ⟶ k i),
  HasCardinalLT ι κ → ∃ m a b, ∀ (i : ι), CategoryTheory.CategoryStruct.comp (f i) (a i) = b
-- Lean.Expr
Lean.instBEqBinderInfo : BEq Lean.BinderInfo