mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.Coxeter.Matrix
CoxeterMatrix.mk.injEq : ∀ {B : Type u_1} (M : Matrix B B ℕ) (isSymm : autoParam M.IsSymm CoxeterMatrix.isSymm._autoParam)
  (diagonal : autoParam (∀ (i : B), M i i = 1) CoxeterMatrix.diagonal._autoParam)
  (off_diagonal : autoParam (∀ (i i' : B), i ≠ i' → M i i' ≠ 1) CoxeterMatrix.off_diagonal._autoParam)
  (M_1 : Matrix B B ℕ) (isSymm_1 : autoParam M_1.IsSymm CoxeterMatrix.isSymm._autoParam)
  (diagonal_1 : autoParam (∀ (i : B), M_1 i i = 1) CoxeterMatrix.diagonal._autoParam)
  (off_diagonal_1 : autoParam (∀ (i i' : B), i ≠ i' → M_1 i i' ≠ 1) CoxeterMatrix.off_diagonal._autoParam),
  ({ M := M, isSymm := isSymm, diagonal := diagonal, off_diagonal := off_diagonal } =
      { M := M_1, isSymm := isSymm_1, diagonal := diagonal_1, off_diagonal := off_diagonal_1 }) =
    (M = M_1)
-- Mathlib.Data.Analysis.Filter
CFilter.inf_le_right : ∀ {α : Type u_1} {σ : Type u_2} [inst : PartialOrder α] (self : CFilter α σ) (a b : σ), self.f (self.inf a b) ≤ self.f b
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.sin_add_two_pi : ∀ (x : ℝ), Real.sin (x + 2 * Real.pi) = Real.sin x
-- Mathlib.CategoryTheory.Limits.Types.Coproducts
CategoryTheory.Limits.CofanTypes.inj_apply_eq_iff_of_isColimit : ∀ {C : Type u} {F : C → Type v} {c : CategoryTheory.Limits.CofanTypes F},
  CategoryTheory.Functor.CoconeTypes.IsColimit c →
    ∀ {i₁ i₂ : C} (y₁ : F i₁) (y₂ : F i₂), c.inj i₁ y₁ = c.inj i₂ y₂ ↔ ∃ (h : i₁ = i₂), y₂ = cast ⋯ y₁
-- Mathlib.NumberTheory.Zsqrtd.GaussianInt
GaussianInt.normSq_le_normSq_of_re_le_of_im_le : ∀ {x y : ℂ}, |x.re| ≤ |y.re| → |x.im| ≤ |y.im| → Complex.normSq x ≤ Complex.normSq y
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
IsLinearSet.isSemilinearSet : ∀ {M : Type u_1} [inst : AddCommMonoid M] {s : Set M}, IsLinearSet s → IsSemilinearSet s
-- Mathlib.Algebra.Group.Subgroup.Defs
/-- Two `AddSubgroup`s are equal if they have the same elements.  -/
AddSubgroup.ext : ∀ {G : Type u_1} [inst : AddGroup G] {H K : AddSubgroup G}, (∀ (x : G), x ∈ H ↔ x ∈ K) → H = K
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
/-- **Alias** of `MeasureTheory.Integrable.fun_add`.

---

Eta-expanded form of `MeasureTheory.Integrable.add` -/
MeasureTheory.Integrable.add'' : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ε' : Type u_8} [inst : TopologicalSpace ε']
  [inst_1 : ESeminormedAddMonoid ε'] [ContinuousAdd ε'] {f g : α → ε'},
  MeasureTheory.Integrable f μ → MeasureTheory.Integrable g μ → MeasureTheory.Integrable (fun i => f i + g i) μ
-- Mathlib.Data.Fin.Basic
Fin.coe_neg_one : ∀ {n : ℕ}, ↑(-1) = n
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.biUnionIndex_mem : ∀ {ι : Type u_1} {I J : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I)
  {πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J}, J ∈ π.biUnion πi → π.biUnionIndex πi J ∈ π
-- Mathlib.Topology.Algebra.Order.Floor
tendsto_fract_left' : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] [inst_2 : FloorRing α] [inst_3 : TopologicalSpace α]
  [IsStrictOrderedRing α] [OrderClosedTopology α] [IsTopologicalAddGroup α] (n : ℤ),
  Filter.Tendsto Int.fract (nhdsWithin (↑n) (Set.Iio ↑n)) (nhds 1)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.cos_zero : Real.Angle.cos 0 = 1
-- Mathlib.Analysis.Normed.Algebra.Exponential
SemiconjBy.exp_neg_mul_mul_exp_eq_self : ∀ {𝔸 : Type u_1} [inst : NormedRing 𝔸] [NormedAlgebra ℚ 𝔸] [CompleteSpace 𝔸] {x a b : 𝔸},
  SemiconjBy x a b → NormedSpace.exp (-b) * x * NormedSpace.exp a = x
-- Mathlib.Order.Hom.WithTopBot
LatticeHom.withTopWithBot.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : Lattice α] [inst_1 : Lattice β] (f : LatticeHom α β),
  f.withTopWithBot = { toLatticeHom := f.withBot.withTop, map_top' := ⋯, map_bot' := ⋯ }
-- Mathlib.Analysis.Normed.Module.Basic
norm_zsmul : ∀ (𝕜 : Type u_1) {E : Type u_3} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup E] [NormedSpace 𝕜 E] (n : ℤ)
  (x : E), ‖n • x‖ = ‖↑n‖ * ‖x‖
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
/-- `rpow` version of `Multiset.prod_map_pow`.  -/
Real.multiset_prod_map_rpow : ∀ {ι : Type u_1} (s : Multiset ι) (f : ι → ℝ),
  (∀ i ∈ s, 0 ≤ f i) → ∀ (r : ℝ), (Multiset.map (fun x => f x ^ r) s).prod = (Multiset.map f s).prod ^ r
-- Init.Data.Int.DivMod.Lemmas
Int.ediv_sign : ∀ (a b : ℤ), a / b.sign = a * b.sign
-- Mathlib.Data.Nat.Cast.Basic
Nat.cast_dvd_cast : ∀ {α : Type u_1} [inst : Semiring α] {m n : ℕ}, m ∣ n → ↑m ∣ ↑n
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue_map : ∀ {α : Type u} [inst : BEq α] [EquivBEq α] {β : Type v} {γ : Type w} {f : α → β → γ} {l : List ((_ : α) × β)} {k : α},
  Std.Internal.List.DistinctKeys l →
    ∀ {h : Std.Internal.List.containsKey k (List.map (fun p => ⟨p.fst, f p.fst p.snd⟩) l) = true},
      Std.Internal.List.getValue k (List.map (fun p => ⟨p.fst, f p.fst p.snd⟩) l) h =
        f (Std.Internal.List.getKey k l ⋯) (Std.Internal.List.getValue k l ⋯)
-- Mathlib.Topology.UniformSpace.Defs
uniformContinuous_def : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] [inst_1 : UniformSpace β] {f : α → β},
  UniformContinuous f ↔ ∀ r ∈ uniformity β, {x | (f x.1, f x.2) ∈ r} ∈ uniformity α
-- Mathlib.Algebra.Group.Subsemigroup.Operations
/-- The `AddSemigroup` hom associated to an inclusion of subsemigroups.  -/
AddSubsemigroup.inclusion : {M : Type u_1} → [inst : Add M] → {S T : AddSubsemigroup M} → S ≤ T → ↥S →ₙ+ ↥T
-- Init.Data.Array.OfFn
Array.toList_ofFn : ∀ {n : ℕ} {α : Type u_1} {f : Fin n → α}, (Array.ofFn f).toList = List.ofFn f
-- Mathlib.RingTheory.Kaehler.Basic
KaehlerDifferential.kerTotal_mkQ_single_algebraMap : ∀ (R : Type u) (S : Type v) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (x : R) (y : S),
  ((KaehlerDifferential.kerTotal R S).mkQ fun₀ | (algebraMap R S) x => y) = 0
-- Init.Data.Nat.Basic
Nat.pos_iff_ne_zero : ∀ {n : ℕ}, 0 < n ↔ n ≠ 0
-- Mathlib.CategoryTheory.Limits.Cones
/-- The image of a cocone in C under a functor G : C ⥤ D is a cocone in D.  -/
CategoryTheory.Functor.mapCocone : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {D : Type u₄} →
          [inst_2 : CategoryTheory.Category.{v₄, u₄} D] →
            (H : CategoryTheory.Functor C D) →
              {F : CategoryTheory.Functor J C} →
                CategoryTheory.Limits.Cocone F → CategoryTheory.Limits.Cocone (F.comp H)
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.instPowInt : {R : Type u_1} →
  {Γ₀ : Type u_2} →
    [inst : LinearOrderedCommGroupWithZero Γ₀] → [inst_1 : DivisionRing R] → (v : Valuation R Γ₀) → Pow (WithVal v) ℤ
-- Init.Prelude
/-- Decides whether two 8-bit unsigned integers are equal. Usually accessed via the `DecidableEq UInt8`
instance.

This function is overridden at runtime with an efficient implementation.

Examples:
 * `UInt8.decEq 123 123 = .isTrue rfl`
 * `(if (6 : UInt8) = 7 then "yes" else "no") = "no"`
 * `show (7 : UInt8) = 7 by decide`
 -/
UInt8.decEq : (a b : UInt8) → Decidable (a = b)
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHom.sub_apply : ∀ {α : Type u_5} [inst : NonUnitalNonAssocRing α] (f g : CentroidHom α) (a : α), (f - g) a = f a - g a
-- ProofWidgets.Component.Basic
ProofWidgets.MarkdownDisplay.Props.mk.inj : ∀ {contents contents_1 : String}, { contents := contents } = { contents := contents_1 } → contents = contents_1
-- Mathlib.Analysis.LocallyConvex.AbsConvex
/-- In general, equality doesn't hold here - e.g. consider `s := {(-1, 1), (1, 1)}` in `ℝ²`.  -/
balancedHull_convexHull_subset_absConvexHull : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] {s : Set E}, balancedHull 𝕜 ((convexHull 𝕜) s) ⊆ (absConvexHull 𝕜) s
-- Mathlib.Algebra.Order.Ring.Ordering.Defs
RingPreordering.neg_one_notMem : ∀ {R : Type u_1} [inst : CommRing R] (P : RingPreordering R), -1 ∉ P
-- Init.Data.SInt.Basic
/-- Converts an 8-bit signed integer to a natural number, mapping all negative numbers to `0`.

Use `Int8.toBitVec` to obtain the two's complement representation.
 -/
Int8.toNatClampNeg : Int8 → ℕ
-- Mathlib.CategoryTheory.Localization.Predicate
CategoryTheory.Localization.essSurj : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [L.IsLocalization W], L.EssSurj
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.Word.mk.inj : ∀ {ι : Type u_1} {M : ι → Type u_2} {inst : (i : ι) → Monoid (M i)} {toList : List ((i : ι) × M i)}
  {ne_one : ∀ l ∈ toList, l.snd ≠ 1} {chain_ne : List.IsChain (fun l l' => l.fst ≠ l'.fst) toList}
  {toList_1 : List ((i : ι) × M i)} {ne_one_1 : ∀ l ∈ toList_1, l.snd ≠ 1}
  {chain_ne_1 : List.IsChain (fun l l' => l.fst ≠ l'.fst) toList_1},
  { toList := toList, ne_one := ne_one, chain_ne := chain_ne } =
      { toList := toList_1, ne_one := ne_one_1, chain_ne := chain_ne_1 } →
    toList = toList_1
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
Summable.tsum_finset_bUnion_disjoint : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α} [T2Space α]
  [ContinuousAdd α] {ι : Type u_4} {s : Finset ι} {t : ι → Set β},
  (↑s).Pairwise (Function.onFun Disjoint t) →
    (∀ i ∈ s, Summable (f ∘ Subtype.val)) → ∑' (x : ↑(⋃ i ∈ s, t i)), f ↑x = ∑ i ∈ s, ∑' (x : ↑(t i)), f ↑x
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
tangentMapWithin_id : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {s : Set M} {p : TangentBundle I M},
  UniqueMDiffAt[s] p.proj → tangentMapWithin I I id s p = p
-- Mathlib.Analysis.Analytic.Composition
Composition.length.eq_1 : ∀ {n : ℕ} (c : Composition n), c.length = c.blocks.length
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.mem_insertManyIfNewUnit_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α fun x => Unit} {ρ : Type w} [inst : ForIn Id ρ α]
  [EquivBEq α] [LawfulHashable α] {l : ρ} {k : α}, k ∈ m → k ∈ Std.DHashMap.Const.insertManyIfNewUnit m l
-- Mathlib.Data.Set.Sups
/-- Notation typeclass for pointwise supremum `⊻`.  -/
HasSups : Type u_4 → Type u_4
-- Mathlib.Geometry.Manifold.IsManifold.Basic
Topology.IsOpenEmbedding.isManifold_singleton : ∀ {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : Nonempty M] {f : M → H} (h : Topology.IsOpenEmbedding f), IsManifold I n M
-- Mathlib.FieldTheory.PerfectClosure
PerfectClosure.instPerfectRing : ∀ (K : Type u) [inst : CommRing K] (p : ℕ) [inst_1 : Fact (Nat.Prime p)] [inst_2 : CharP K p],
  PerfectRing (PerfectClosure K p) p
-- Mathlib.Order.SupIndep
iSupIndep.of_coe_Iic_comp : ∀ {α : Type u_1} [inst : CompleteLattice α] {ι : Sort u_5} {a : α} {t : ι → ↑(Set.Iic a)},
  iSupIndep (Subtype.val ∘ t) → iSupIndep t
-- Mathlib.NumberTheory.ArithmeticFunction.Misc
/-- `ω n` is the number of distinct prime factors of `n`.  -/
ArithmeticFunction.omega.termω : Lean.ParserDescr
-- Lean.Data.Lsp.Basic
Lean.Lsp.instToJsonDocumentChange : Lean.ToJson Lean.Lsp.DocumentChange
-- Std.Data.HashMap.Raw
Std.HashMap.Raw.WF.erase : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} {a : α},
  m.WF → (m.erase a).WF
-- Mathlib.CategoryTheory.Limits.Opposites
/-- Turn a limit for `F : J ⥤ Cᵒᵖ` into a colimit for `F.leftOp : Jᵒᵖ ⥤ C`.  -/
CategoryTheory.Limits.isColimitOfConeOfCoconeLeftOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} J] →
        (F : CategoryTheory.Functor J Cᵒᵖ) →
          {c : CategoryTheory.Limits.Cocone F.leftOp} →
            CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.coneOfCoconeLeftOp c) →
              CategoryTheory.Limits.IsColimit c
-- Mathlib.Algebra.Homology.ShortComplex.FunctorEquivalence
CategoryTheory.ShortComplex.FunctorEquivalence.counitIso_hom_app_app_τ₂ : ∀ (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] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  (X : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)) (X_1 : J),
  (((CategoryTheory.ShortComplex.FunctorEquivalence.counitIso J C).hom.app X).app X_1).τ₂ =
    CategoryTheory.CategoryStruct.id (X.obj X_1).X₂
-- Lean.ScopedEnvExtension
Lean.activateScoped : {m : Type → Type} → [Monad m] → [Lean.MonadEnv m] → [MonadLiftT (ST IO.RealWorld) m] → Lean.Name → m Unit
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.zero.eq_1 : ∀ {α : Type u} [inst : Zero α], WithBot.zero = { zero := ↑0 }
-- Mathlib.Topology.Compactness.CompactSystem
/-- A set of sets is a compact system if, whenever a countable subfamily has empty intersection,
then finitely many of them already have empty intersection.  -/
IsCompactSystem : {α : Type u_1} → Set (Set α) → Prop
-- Mathlib.Util.Notation3
Mathlib.Notation3.DelabKey.other : Lean.Name → Mathlib.Notation3.DelabKey
-- Mathlib.CategoryTheory.Sites.Closed
/-- The presheaf sending each object to the set of `J`-closed sieves on it. This presheaf is a `J`-sheaf
(and will turn out to be a subobject classifier for the category of `J`-sheaves).
 -/
CategoryTheory.Functor.closedSieves : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.GrothendieckTopology C → CategoryTheory.Subfunctor (CategoryTheory.Functor.sieves C)
-- Mathlib.Data.WSeq.Defs
/-- A weak sequence is finite if `toList s` terminates. Equivalently,
it is a finite number of `think` and `cons` applied to `nil`.  -/
Stream'.WSeq.IsFinite : {α : Type u} → Stream'.WSeq α → Prop
-- Mathlib.Algebra.Quandle
/-- The function under the Shelf Homomorphism  -/
ShelfHom.toFun : {S₁ : Type u_1} → {S₂ : Type u_2} → [inst : Shelf S₁] → [inst_1 : Shelf S₂] → ShelfHom S₁ S₂ → S₁ → S₂
-- Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
CategoryTheory.Limits.asEmptyCocone_ι_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (X : C) (X_1 : CategoryTheory.Discrete PEmpty.{1}),
  (CategoryTheory.Limits.asEmptyCocone X).ι.app X_1 = id (CategoryTheory.Discrete.casesOn X_1 fun as => ⋯.elim)
-- Mathlib.Data.Nat.Size
Nat.size_pow : ∀ {n : ℕ}, (2 ^ n).size = n + 1
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.logb_one_left : ∀ {x : ℝ}, Real.logb 1 x = 0
-- Lean.Declaration
/-- Number of parameters in inductive datatype.  -/
Lean.ConstructorVal.numParams : Lean.ConstructorVal → ℕ
-- Mathlib.Geometry.Diffeology.Basic
DiffeologicalSpace.isPlot_inf_iff : ∀ {X : Type u_1} {d₁ d₂ : DiffeologicalSpace X} {n : ℕ} {p : EuclideanSpace ℝ (Fin n) → X},
  Diffeology.IsPlot p ↔ Diffeology.IsPlot p ∧ Diffeology.IsPlot p
-- Mathlib.Algebra.Module.LinearMap.FiniteRange
LinearMap.HasNoetherianRange.smul : ∀ {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} [inst : CommRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [inst_3 : AddCommGroup V₂] [inst_4 : Module K V₂] {f : V →ₗ[K] V₂},
  f.HasNoetherianRange → ∀ (c : K), (c • f).HasNoetherianRange
-- Init.Data.List.Perm
List.Perm.pmap : ∀ {α : Type u_1} {β : Type u_2} {p : α → Prop} (f : (a : α) → p a → β) {l₁ l₂ : List α},
  l₁.Perm l₂ → ∀ {H₁ : ∀ a ∈ l₁, p a} {H₂ : ∀ a ∈ l₂, p a}, (List.pmap f l₁ H₁).Perm (List.pmap f l₂ H₂)
-- Init.Data.AC
Lean.Data.AC.Variable : {α : Sort u} → (α → α → α) → Type u
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.of.eq_1 : ∀ {α : Type u} (x : α), FreeAddGroup.of x = FreeAddGroup.mk [(x, true)]
-- Mathlib.Tactic.Linarith.Datatypes
Mathlib.Tactic.Linarith.CertificateOracle.mk.inj : ∀ {produceCertificate produceCertificate_1 : List Mathlib.Tactic.Linarith.Comp → ℕ → Lean.MetaM (Std.HashMap ℕ ℕ)},
  { produceCertificate := produceCertificate } = { produceCertificate := produceCertificate_1 } →
    produceCertificate = produceCertificate_1
-- Mathlib.LinearAlgebra.DirectSum.Finsupp
finsuppTensorFinsuppRid_apply_apply : ∀ (R : Type u_1) (M : Type u_3) (ι : Type u_5) (κ : Type u_6) [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] (f : ι →₀ M) (g : κ →₀ R) (a : ι) (b : κ),
  ((finsuppTensorFinsuppRid R M ι κ) (f ⊗ₜ[R] g)) (a, b) = g b • f a
-- Mathlib.Combinatorics.Enumerative.DoubleCounting
Fintype.card_le_card_of_rightTotal_unique : ∀ {α : Type u_2} {β : Type u_3} [inst : Fintype α] [inst_1 : Fintype β] {r : α → β → Prop},
  Relator.RightTotal r → Relator.RightUnique r → Fintype.card β ≤ Fintype.card α
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
CategoryTheory.CostructuredArrow.commaToGrothendieckPrecompFunctor_map_fiber : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (L : CategoryTheory.Functor C D)
  (R : CategoryTheory.Functor E D) {X Y : CategoryTheory.Comma L R} (f : X ⟶ Y),
  ((CategoryTheory.CostructuredArrow.commaToGrothendieckPrecompFunctor L R).map f).fiber =
    CategoryTheory.CostructuredArrow.homMk f.left ⋯
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.zoom.eq_2 : ∀ {α : Type u_1} (cut : α → Ordering) (x : RBTree.RBNode.Path α) (c : RBTree.RBColor) (a : RBTree.RBNode α) (y : α)
  (b : RBTree.RBNode α),
  RBTree.RBNode.zoom cut (RBTree.RBNode.node c a y b) x =
    match cut y with
    | Ordering.lt => RBTree.RBNode.zoom cut a (RBTree.RBNode.Path.left c x y b)
    | Ordering.gt => RBTree.RBNode.zoom cut b (RBTree.RBNode.Path.right c a y x)
    | Ordering.eq => (RBTree.RBNode.node c a y b, x)
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
aestronglyMeasurable_congr : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f g : α → β}, f =ᵐ[μ] g → (MeasureTheory.AEStronglyMeasurable f μ ↔ MeasureTheory.AEStronglyMeasurable g μ)
-- Std.Do.SPred.SVal
Std.Do.SVal.uncurry.eq_1 : ∀ {α : Type u} (f_2 : Std.Do.SVal [] α), f_2.uncurry = fun x => f_2
-- Init.Data.Range.Lemmas
_private.Init.Data.Range.Lemmas.0.List.forIn'_cons.match_1.splitter : {β : Type u_1} →
  (motive : ForInStep β → Sort u_2) →
    (x : ForInStep β) → ((b : β) → motive (ForInStep.done b)) → ((b : β) → motive (ForInStep.yield b)) → motive x
-- Mathlib.Data.Num.Basic
ZNum.instLT : LT ZNum
-- Mathlib.Data.ENNReal.Basic
ENNReal.instCoeNNReal : Coe NNReal ENNReal
-- Batteries.Data.BitVec.Lemmas
BitVec.getMsbD_ofFnBE : ∀ {n : ℕ} (f : Fin n → Bool) (i : ℕ), (BitVec.ofFnBE f).getMsbD i = if h : i < n then f ⟨i, h⟩ else false
-- Mathlib.Algebra.Group.Ext
AddCancelCommMonoid.toAddCommMonoid_injective : ∀ {M : Type u}, Function.Injective (@AddCancelCommMonoid.toAddCommMonoid M)
-- Mathlib.Algebra.Star.NonUnitalSubsemiring
/-- The actual `NonUnitalStarSubsemiring` obtained from an element of a type satisfying
`NonUnitalSubsemiringClass` and `StarMemClass`.  -/
NonUnitalStarSubsemiring.ofClass : {S : Type u_1} →
  {R : Type u_2} →
    [inst : NonUnitalNonAssocSemiring R] →
      [inst_1 : StarRing R] →
        [inst_2 : SetLike S R] → [NonUnitalSubsemiringClass S R] → [StarMemClass S R] → S → NonUnitalStarSubsemiring R
-- Init.Data.UInt.Bitwise
UInt32.shiftLeft_and : ∀ {a b c : UInt32}, (a &&& b) <<< c = a <<< c &&& b <<< c
-- Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
SimpleGraph.Walk.support.eq_1 : ∀ {V : Type u} {G : SimpleGraph V} {u : V}, SimpleGraph.Walk.nil.support = [u]
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.Relation.below.mul_2 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat}
  {motive : (a a_1 : RingCat.Colimits.Prequotient F) → RingCat.Colimits.Relation F a a_1 → Prop}
  (x y y' : RingCat.Colimits.Prequotient F) (x_1 : RingCat.Colimits.Relation F y y'),
  RingCat.Colimits.Relation.below x_1 → motive y y' x_1 → RingCat.Colimits.Relation.below ⋯
-- Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv
/-- Given an orthogonal basis, a quadratic form is isometrically equivalent with a weighted sum of
squares.  -/
QuadraticForm.isometryEquivWeightedSumSquares : {K : Type u_3} →
  {V : Type u_8} →
    [inst : Field K] →
      [inst_1 : Invertible 2] →
        [inst_2 : AddCommGroup V] →
          [inst_3 : Module K V] →
            (Q : QuadraticForm K V) →
              (v : Module.Basis (Fin (Module.finrank K V)) K V) →
                LinearMap.IsOrthoᵢ (QuadraticMap.associated Q) ⇑v →
                  QuadraticMap.IsometryEquiv Q (QuadraticMap.weightedSumSquares K fun i => Q (v i))
-- Init.Data.Bool
Bool.instDecidableForallOfDecidablePred : (p : Bool → Prop) → [inst : DecidablePred p] → Decidable (∀ (x : Bool), p x)
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.monadLift_StateT : ∀ {m : Type u → Type v} {Pred EPred : Type u} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {α σ : Type u}
  {epost : EPred} (x : m α) (post : α → σ → Pred),
  ⦃ fun s => Std.Internal.Do.wp x (fun a => post a s) epost ⦄ MonadLift.monadLift x ⦃ post; epost ⦄
-- Init.Data.Int.Order
Int.le_of_sub_one_lt : ∀ {a b : ℤ}, a - 1 < b → a ≤ b
-- Mathlib.Logic.Equiv.Multiset
_private.Mathlib.Logic.Equiv.Multiset.0.enle.isLinearOrder : ∀ {α : Type u_1} [inst : Encodable α], IsLinearOrder α enle✝
-- Mathlib.Logic.Equiv.Array
/-- The natural equivalence between arrays and lists.  -/
Equiv.arrayEquivList : (α : Type u_1) → Array α ≃ List α
-- Mathlib.Topology.MetricSpace.Gluing
Metric.toGlueR_isometry : ∀ {X : Type u} {Y : Type v} {Z : Type w} [inst : Nonempty Z] [inst_1 : MetricSpace Z] [inst_2 : MetricSpace X]
  [inst_3 : MetricSpace Y] {Φ : Z → X} {Ψ : Z → Y} (hΦ : Isometry Φ) (hΨ : Isometry Ψ), Isometry (Metric.toGlueR hΦ hΨ)
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
/-- Obvious triangles `X ⟶ 0 ⟶ X⟦1⟧ ⟶ X⟦1⟧` are distinguished  -/
CategoryTheory.Pretriangulated.contractible_distinguished₂ : ∀ {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] (X : C),
  CategoryTheory.Pretriangulated.Triangle.mk 0 0
      (CategoryTheory.CategoryStruct.id ((CategoryTheory.shiftFunctor C 1).obj X)) ∈
    CategoryTheory.Pretriangulated.distinguishedTriangles
-- Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.le₀₁ : ∀ {ι : Type u_2} {κ : Type u_3} [inst : Preorder ι] {c : ℤ → ComplexShape κ} {r₀ : ℤ}
  (self : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀) (r : ℤ) (pq : κ)
  (hr : autoParam (r₀ ≤ r) CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore._auto_5),
  self.i₀ r pq ⋯ ≤ self.i₁ pq
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Fin
Fin.reduceLT : Lean.Meta.Simp.Simproc
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Submodule
PresheafOfModules.Submodule.toPresheafOfModules_map_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  {M : PresheafOfModules R} (N : M.Submodule) {X Y : Cᵒᵖ} (f : X ⟶ Y) (m : ↥(N.obj X)),
  ↑((CategoryTheory.ConcreteCategory.hom (N.toPresheafOfModules.map f)) m) =
    (CategoryTheory.ConcreteCategory.hom (M.map f)) ↑m
-- Init.Data.Nat.Control
/-- Checks whether there is some number less that the given bound for which the monadic predicate `p`
returns `true`. Numbers are checked in increasing order until `p` returns true, after which
no further are checked.
 -/
Nat.anyM : {m : Type → Type u_1} → [Monad m] → (n : ℕ) → ((i : ℕ) → i < n → m Bool) → m Bool