mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.BifunctorShift
CochainComplex.ι_mapBifunctorShift₁Iso_hom_f_assoc : ∀ {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]
  [inst_3 : CategoryTheory.Preadditive C₁] [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C₂]
  [inst_5 : CategoryTheory.Preadditive D] (K₁ : CochainComplex C₁ ℤ) (K₂ : CochainComplex C₂ ℤ)
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [inst_6 : F.Additive]
  [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (x : ℤ) [inst_8 : K₁.HasMapBifunctor K₂ F] (n₁ n₂ n : ℤ)
  (h : n₁ + n₂ = n) (m₁ m : ℤ) (hm₁ : m₁ = n₁ + x) (hm : m = n + x) {Z : D}
  (h_1 : ((CategoryTheory.shiftFunctor (CochainComplex D ℤ) x).obj (K₁.mapBifunctor K₂ F)).X n ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (((CategoryTheory.shiftFunctor (CochainComplex C₁ ℤ) x).obj K₁).ιMapBifunctor K₂ F n₁ n₂ n h)
      (CategoryTheory.CategoryStruct.comp ((K₁.mapBifunctorShift₁Iso K₂ F x).hom.f n) h_1) =
    CategoryTheory.CategoryStruct.comp ((F.map (K₁.shiftFunctorObjXIso x n₁ m₁ hm₁).hom).app (K₂.X n₂))
      (CategoryTheory.CategoryStruct.comp (K₁.ιMapBifunctor K₂ F m₁ n₂ m ⋯)
        (CategoryTheory.CategoryStruct.comp ((K₁.mapBifunctor K₂ F).shiftFunctorObjXIso x n m hm).inv h_1))
-- Std.Internal.Parsec.String
/-- Parses the given string.
 -/
Std.Internal.Parsec.String.pstring : String → Std.Internal.Parsec.String.Parser String
-- Init.Data.SInt.Lemmas
Int32.toInt_sub : ∀ (a b : Int32), (a - b).toInt = (a.toInt - b.toInt).bmod (2 ^ 32)
-- Mathlib.Algebra.Group.Units.Equiv
Units.mapEquiv_symm : ∀ {M : Type u_3} {N : Type u_4} [inst : Monoid M] [inst_1 : Monoid N] (h : M ≃* N),
  (Units.mapEquiv h).symm = Units.mapEquiv h.symm
-- Lean.ResolveName
/-- Finds an efficient name that unambiguously resolves to the given name `n₀`, if possible.
Considers suffixes of `n₀` and suffixes of aliases of `n₀` when "unresolving".
Aliases are considered first.

When `fullNames` is true, returns either `n₀` or `_root_.n₀`.

When `allowHorizAliases` is false, then "horizontal aliases" (ones that are not put into a parent namespace) are filtered out.
The assumption is that non-horizontal aliases are "API exports" (i.e., intentional exports that should be considered to be the new canonical name).
"Non-API exports" arise from (1) using `export` to add names to a namespace for dot notation or (2) projects that want names to be conveniently and permanently accessible in their own namespaces.

`filter` specifies a predicate that the unresolved name must additionally satisfy.

This function is meant to be used for pretty printing.
If `n₀` is an accessible name, then the result will be an accessible name.

The name `n₀` may be private.
 -/
Lean.unresolveNameGlobal? : {m : Type → Type} →
  [inst : Monad m] →
    [Lean.MonadResolveName m] →
      [Lean.MonadEnv m] →
        [Lean.MonadOptions m] →
          [Lean.MonadLog m] →
            [Lean.AddMessageContext m] →
              Lean.Name →
                optParam Bool false →
                  optParam Bool false → (optParam (Lean.Name → m Bool) fun x => pure true) → m (Option Lean.Name)
-- Lean.Server.Completion.EligibleHeaderDecls
/-- Iterate over all declarations that are allowed in completion results.  -/
Lean.Server.Completion.forEligibleDeclsM : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadEnv m] →
      [MonadLiftT Lean.MetaM m] → (Lean.Name → Lean.Server.Completion.EligibleDecl → m PUnit.{1}) → m PUnit.{1}
-- Mathlib.FieldTheory.RatFunc.AsPolynomial
RatFunc.C_injective : ∀ {K : Type u} [inst : CommRing K] [inst_1 : IsDomain K], Function.Injective ⇑RatFunc.C
-- Lean.Parser.Syntax
Lean.Parser.Command.elabTail.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.CategoryTheory.Localization.Triangulated
CategoryTheory.Triangulated.Localization.instIsTriangulatedLocalization : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Limits.HasZeroObject C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (W : CategoryTheory.MorphismProperty C) [inst_6 : W.HasLeftCalculusOfFractions]
  [inst_7 : W.IsCompatibleWithTriangulation] [CategoryTheory.IsTriangulated C],
  CategoryTheory.IsTriangulated W.Localization
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.natDegree_eq_of_natDegree_add_lt_right : ∀ {R : Type u} [inst : Semiring R] (p q : Polynomial R), (p + q).natDegree < q.natDegree → p.natDegree = q.natDegree
-- Mathlib.Geometry.Manifold.BumpFunction
SmoothBumpFunction.one_of_dist_le : ∀ {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] {c : M}
  (f : SmoothBumpFunction I c) {x : M} [inst_5 : FiniteDimensional ℝ E],
  x ∈ (chartAt H c).source → dist (↑(extChartAt I c) x) (↑(extChartAt I c) c) ≤ f.rIn → ↑f x = 1
-- Mathlib.Topology.ContinuousMap.LocallyConstant
LocallyConstant.toAddMonoidHom_toContinuousMapLinearMap : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (R : Type u_3)
  [inst_2 : Semiring R] [inst_3 : AddCommMonoid Y] [inst_4 : Module R Y] [inst_5 : ContinuousAdd Y]
  [inst_6 : ContinuousConstSMul R Y],
  (LocallyConstant.toContinuousMapLinearMap R).toAddMonoidHom = LocallyConstant.toContinuousMapAddMonoidHom
-- Mathlib.Topology.Sheaves.Module
/-- `sheafOfModulesEquivOver.inverse` takes `R |_ U` to `R.over U`.  -/
TopologicalSpace.Opens.sheafOfModulesEquivOverInverseUnit : {X : TopCat} →
  (U : TopologicalSpace.Opens ↑X) →
    (R : TopCat.Sheaf RingCat X) →
      (U.sheafOfModulesEquivOver R).inverse.obj (SheafOfModules.unit (U.sheafRestrict.obj R)) ≅
        SheafOfModules.unit (CategoryTheory.Sheaf.over R U)
-- Mathlib.NumberTheory.Real.GoldenRatio
/-- The golden ratio `φ := (1 + √5)/2`.  -/
goldenRatio.termφ : Lean.ParserDescr
-- Mathlib.Tactic.CategoryTheory.Bicategory.Datatypes
/-- The codomain of an isomorphism.  -/
Mathlib.Tactic.Bicategory.tgtExprOfIso : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Algebra.Group.Pi.Lemmas
Function.const_ne_zero : ∀ {ι : Type u_1} {α : Type u_2} [inst : Zero α] [Nonempty ι] {a : α}, Function.const ι a ≠ 0 ↔ a ≠ 0
-- Mathlib.Algebra.Order.Hom.MonoidWithZero
OrderMonoidWithZeroHom.coe_monoidWithZeroHom : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : MulZeroOneClass α]
  [inst_3 : MulZeroOneClass β] (f : α →*₀o β), ⇑(MonoidWithZeroHom.ofClass f) = ⇑f
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.isEmptyEquiv_symm_apply : ∀ (ι : Type u_1) {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)]
  [inst_2 : (i : ι) → Module R (s i)] [inst_3 : IsEmpty ι] (r : R),
  (PiTensorProduct.isEmptyEquiv ι).symm r = r • (PiTensorProduct.tprod R) isEmptyElim
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
/-- Given a `G`-representation `A` and a normal subgroup `S ≤ G`, the degree 1
corestriction-coinflation sequence `H₁(S, A) ⟶ H₁(G, A) ⟶ H₁(G ⧸ S, A_S)` is exact. `simp`s
squeezed for performance.  -/
groupHomology.H1CoresCoinf_exact : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) (S : Subgroup G) [inst_2 : S.Normal],
  (groupHomology.H1CoresCoinf A S).Exact
-- Mathlib.Algebra.Module.Equiv.Basic
/-- An additive equivalence between commutative additive monoids is a linear equivalence between
ℕ-modules  -/
AddEquiv.toNatLinearEquiv : {M : Type u_5} → {M₂ : Type u_7} → [inst : AddCommMonoid M] → [inst_1 : AddCommMonoid M₂] → M ≃+ M₂ → M ≃ₗ[ℕ] M₂
-- Mathlib.Algebra.Ring.SumsOfSquares
AddSubmonoid.coe_sumSq : ∀ (T : Type u_2) [inst : AddMonoid T] [inst_1 : Mul T], ↑(AddSubmonoid.sumSq T) = {s | IsSumSq s}
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.completeTheory.eq_1 : ∀ (L : FirstOrder.Language) (M : Type w) [inst : L.Structure M], L.completeTheory M = {φ | M ⊨ φ}
-- Std.Data.ExtTreeMap.Basic
/-- Returns the number of mappings present in the map.  -/
Std.ExtTreeMap.size : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.ExtTreeMap α β cmp → ℕ
-- Mathlib.Data.Finsupp.Basic
/-- **Alias** of `Finsupp.mapRange_finsetSum`. -/
Finsupp.mapRange_finset_sum : ∀ {α : Type u_1} {ι : Type u_4} {M : Type u_5} {N : Type u_6} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N]
  {F : Type u_12} [inst_2 : FunLike F M N] [inst_3 : AddMonoidHomClass F M N] (f : F) (s : Finset ι) (g : ι → α →₀ M),
  Finsupp.mapRange ⇑f ⋯ (∑ x ∈ s, g x) = ∑ x ∈ s, Finsupp.mapRange ⇑f ⋯ (g x)
-- Mathlib.Algebra.Free
Magma.AssocRel.intro : ∀ {α : Type u} [inst : Mul α] (x y z : α), Magma.AssocRel α (x * y * z) (x * (y * z))
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.S_comp_two_mul_X : ∀ (R : Type u_1) [inst : CommRing R] (n : ℤ),
  (Polynomial.Chebyshev.S R n).comp (2 * Polynomial.X) = Polynomial.Chebyshev.U R n
-- Mathlib.Algebra.Order.Module.Defs
smul_lt_iff_lt_one_left : ∀ {α : Type u_1} {β : Type u_2} {a : α} {b : β} [inst : Monoid α] [inst_1 : Zero β] [inst_2 : MulAction α β]
  [inst_3 : Preorder α] [inst_4 : Preorder β] [SMulPosStrictMono α β] [SMulPosReflectLT α β],
  0 < b → (a • b < b ↔ a < 1)
-- Mathlib.CategoryTheory.Limits.Bicones
CategoryTheory.Bicone.right : {J : Type u₁} → CategoryTheory.Bicone J
-- Mathlib.Data.List.Palindrome
/-- `Palindrome l` asserts that `l` is a palindrome. This is defined inductively:

* The empty list is a palindrome;
* A list with one element is a palindrome;
* Adding the same element to both ends of a palindrome results in a bigger palindrome.
 -/
List.Palindrome : {α : Type u_1} → List α → Prop
-- Std.Data.DHashMap.Internal.AssocList.Basic
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.AssocList.forInStep : {α : Type u} →
  {β : α → Type v} →
    {δ : Type w} →
      {m : Type w → Type w'} →
        [Monad m] → Std.DHashMap.Internal.AssocList α β → δ → ((a : α) → β a → δ → m (ForInStep δ)) → m (ForInStep δ)
-- Mathlib.Algebra.EuclideanDomain.Basic
EuclideanDomain.gcd_zero_right : ∀ {R : Type u} [inst : EuclideanDomain R] [inst_1 : DecidableEq R] (a : R), EuclideanDomain.gcd a 0 = a
-- Mathlib.Algebra.SkewPolynomial.Basic
/-- See also `SkewPolynomial.sum_smul_index` for a version using multiplication on the RHS.  -/
SkewPolynomial.sum_smul_index' : ∀ {R : Type u_1} [inst : Semiring R] {S : Type u_5} [inst_1 : AddCommMonoid S] {T : Type u_6} [inst_2 : DistribSMul T R]
  (p : SkewPolynomial R) (b : T) (f : ℕ → R → S), (∀ (i : ℕ), f i 0 = 0) → (b • p).sum f = p.sum fun n a => f n (b • a)
-- Std.Async.Basic
/-- Creates a new `EAsync` out of a `RTask`.
 -/
Std.Async.EAsync.ofTask : {ε α : Type} → Std.Async.ETask ε α → Std.Async.EAsync ε α
-- Mathlib.RingTheory.HahnSeries.Lex
HahnSeries.abs_lt_abs_of_orderTop_ofLex : ∀ {Γ : Type u_1} {R : Type u_2} [inst : LinearOrder Γ] [inst_1 : LinearOrder R] [inst_2 : AddCommGroup R]
  [IsOrderedAddMonoid R] {x y : Lex (HahnSeries Γ R)}, (ofLex y).orderTop < (ofLex x).orderTop → |x| < |y|
-- Mathlib.Logic.Pairwise
Pairwise.mono : ∀ {α : Type u_1} {r p : α → α → Prop}, Pairwise r → (∀ ⦃i j : α⦄, r i j → p i j) → Pairwise p
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mod
CategoryTheory.IsModHom.mulActionHom_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] {M : C}
  [inst_2 : CategoryTheory.MonObj M] {X : C} [inst_3 : CategoryTheory.ModObj M X] {Y : C}
  [inst_4 : CategoryTheory.ModObj M Y] (f : X ⟶ Y) [inst_5 : CategoryTheory.IsModHom M f] (Z : C) (x : Z ⟶ X),
  (CategoryTheory.IsModHom.mulActionHom f Z) x = CategoryTheory.CategoryStruct.comp x f
-- Init.Data.Vector.Basic
/-- Converts an array to a vector. The resulting vector's size is the array's size.
 -/
Array.toVector : {α : Type u_1} → (xs : Array α) → Vector α xs.size
-- Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Multiset.sum_map_neg' : ∀ {G : Type u_4} [inst : SubtractionCommMonoid G] (m : Multiset G), (Multiset.map Neg.neg m).sum = -m.sum
-- Mathlib.RepresentationTheory.Homological.ContCohomology.Basic
TopRep.hom_d_succ : ∀ {k : Type u_1} {G : Type u_2} [inst : Ring k] [inst_1 : Group G] [inst_2 : TopologicalSpace k]
  [inst_3 : TopologicalSpace G] [inst_4 : IsTopologicalGroup G] (X : TopRep k G) (n : ℕ),
  TopRep.Hom.hom (X.d (n + 1)) =
    (X.resolutionX (n + 1)).ρ.coind₁ι - ContRepresentation.coind₁Map (TopRep.Hom.hom (X.d n))
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
/-- Angles are translation invariant.  -/
EuclideanGeometry.angle_vadd_const : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (v₁ v₂ v₃ : V) (p : P),
  EuclideanGeometry.angle (v₁ +ᵥ p) (v₂ +ᵥ p) (v₃ +ᵥ p) = EuclideanGeometry.angle v₁ v₂ v₃
-- Lean.MetavarContext
Lean.MonadMCtx.modifyMCtx : {m : Type → Type} → [self : Lean.MonadMCtx m] → (Lean.MetavarContext → Lean.MetavarContext) → m Unit
-- Init.Prelude
/-- An identifier.

In addition to source information, identifiers have the following fields:
* `rawVal` is the literal substring from the input file
* `val` is the parsed Lean name, potentially including macro scopes.
* `preresolved` is the list of possible declarations this could refer to, populated by
  [quotations](https://lean-lang.org/doc/reference/4.33.0/find/?domain=Verso.Genre.Manual.section&name=quasiquotation).
 -/
Lean.Syntax.ident : Lean.SourceInfo → Substring.Raw → Lean.Name → List Lean.Syntax.Preresolved → Lean.Syntax
-- Mathlib.Algebra.Group.Hom.Basic
MonoidHom.inv_apply : ∀ {M : Type u_2} {G : Type u_5} [inst : MulOneClass M] [inst_1 : CommGroup G] (f : M →* G) (x : M), f⁻¹ x = (f x)⁻¹
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Mul
Std.Tactic.BVDecide.BVExpr.bitblast.blastMul : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] → {w : ℕ} → (aig : Std.Sat.AIG α) → aig.BinaryRefVec w → Std.Sat.AIG.RefVecEntry α w
-- Mathlib.Tactic.LinearCombinationPrime
/-- The `(norm := $tac)` syntax says to use `tac` as a normalization postprocessor for
`linear_combination'`. The default normalizer is `ring1`, but you can override it with `ring_nf`
to get subgoals from `linear_combination'` or with `skip` to disable normalization.
 -/
Mathlib.Tactic.LinearCombinationPrime.normStx : Lean.ParserDescr
-- Mathlib.Topology.Covering.Quotient
/-- A function from a topological space `E` with an action by a discrete group to another
topological space `X` is a quotient covering map if it is a quotient map, the action is
continuous and transitive on fibers, and every point of `E` has a neighborhood whose translates
by the group elements are pairwise disjoint.  -/
IsQuotientCoveringMap : {E : Type u_1} →
  {X : Type u_2} →
    [TopologicalSpace E] → [TopologicalSpace X] → (E → X) → (G : Type u_3) → [inst : Group G] → [MulAction G E] → Prop
-- Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
ProbabilityTheory.IsMeasurableRatCDF.mk : ∀ {α : Type u_1} [inst : MeasurableSpace α] {f : α → ℚ → ℝ},
  (∀ (a : α), ProbabilityTheory.IsRatStieltjesPoint f a) → Measurable f → ProbabilityTheory.IsMeasurableRatCDF f
-- Mathlib.Data.Multiset.Sym
Multiset.sym2_coe : ∀ {α : Type u_1} (xs : List α), (↑xs).sym2 = ↑xs.sym2
-- Mathlib.GroupTheory.OrderOfElement
isOfFinOrder_ofAdd_iff : ∀ {α : Type u_6} [inst : AddMonoid α] {x : α}, IsOfFinOrder (Multiplicative.ofAdd x) ↔ IsOfFinAddOrder x
-- Init.Data.SInt.Lemmas
Int32.ofIntClamp_bitVecToInt : ∀ (n : BitVec 32), Int32.ofIntClamp n.toInt = Int32.ofBitVec n
-- Mathlib.Order.Interval.Finset.Basic
Finset.uIcc_comm : ∀ {α : Type u_2} [inst : Lattice α] [inst_1 : LocallyFiniteOrder α] (a b : α), Finset.uIcc a b = Finset.uIcc b a
-- Mathlib.RingTheory.Morita.Matrix
/-- The functor from `Mod-R` to `Mod-Mₙ(R)` induced by `LinearMap.mapModule` and
`Matrix.matrixModule`.  -/
ModuleCat.toMatrixModCat : (R : Type u) →
  (ι : Type v) →
    [inst : Ring R] →
      [inst_1 : Fintype ι] → [inst_2 : DecidableEq ι] → CategoryTheory.Functor (ModuleCat R) (ModuleCat (Matrix ι ι R))
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.deleteVerts_adj : ∀ {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} {s : Set V} {u v : V},
  (G'.deleteVerts s).Adj u v ↔ u ∈ G'.verts ∧ u ∉ s ∧ v ∈ G'.verts ∧ v ∉ s ∧ G'.Adj u v
-- Init.Data.Array.Count
Array.count_toList : ∀ {α : Type u_1} [inst : BEq α] {xs : Array α} {a : α}, List.count a xs.toList = Array.count a xs
-- Lean.Widget.Types
Lean.Widget.Module.mk : (javascript : String) → { x // x = hash javascript } → Lean.Widget.Module
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.WalkingMultispan.left.inj : ∀ {J : CategoryTheory.Limits.MultispanShape} {a a_1 : J.L},
  CategoryTheory.Limits.WalkingMultispan.left a = CategoryTheory.Limits.WalkingMultispan.left a_1 → a = a_1
-- Mathlib.Algebra.Group.Hom.Instances
/-- The expression `fun g m ↦ g (f m)` as an `AddMonoidHom`.
Equivalently, `(fun g ↦ AddMonoidHom.comp g f)` as an `AddMonoidHom`.

This also exists in a `LinearMap` version, `LinearMap.lcomp`.  -/
AddMonoidHom.compHom' : {M : Type uM} →
  {N : Type uN} →
    {P : Type uP} →
      [inst : AddZeroClass M] → [inst_1 : AddZeroClass N] → [inst_2 : AddCommMonoid P] → (M →+ N) → (N →+ P) →+ M →+ P
-- Mathlib.Data.Matrix.Basis
Matrix.ext_linearMap_iff : ∀ {m : Type u_2} {n : Type u_3} {R : Type u_5} {α : Type u_7} {β : Type u_8} [inst : DecidableEq m]
  [inst_1 : DecidableEq n] [Finite m] [Finite n] [inst_4 : Semiring R] [inst_5 : AddCommMonoid α]
  [inst_6 : AddCommMonoid β] [inst_7 : Module R α] [inst_8 : Module R β] {f g : Matrix m n α →ₗ[R] β},
  f = g ↔ ∀ (i : m) (j : n), f ∘ₗ Matrix.singleLinearMap R i j = g ∘ₗ Matrix.singleLinearMap R i j
-- Mathlib.CategoryTheory.Adjunction.Basic
/-- If `adj : F ⊣ G`, and `X : C`, then `F.obj X` corepresents `Y ↦ (X ⟶ G.obj Y)`.  -/
CategoryTheory.Adjunction.corepresentableBy : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          {G : CategoryTheory.Functor D C} →
            (F ⊣ G) → (X : C) → (G.comp (CategoryTheory.coyoneda.obj (Opposite.op X))).CorepresentableBy (F.obj X)
-- Lean.Meta.Tactic.LibrarySearch
/-- Called to abort speculative execution in library search.
 -/
Lean.Meta.LibrarySearch.abortSpeculation : {m : Type u_1 → Type u_2} → {α : Type u_1} → [MonadExcept Lean.Exception m] → m α
-- Mathlib.Algebra.Algebra.Spectrum.Basic
spectrum.notMem_iff : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Ring A] [inst_2 : Algebra R A] {r : R} {a : A},
  r ∉ spectrum R a ↔ IsUnit ((algebraMap R A) r - a)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.String
String.Slice.dropSuffix?_string_empty : ∀ {s : String.Slice}, s.dropSuffix? "" = some s
-- Mathlib.Logic.Unique
Unique.forall_iff : ∀ {α : Sort u_1} [inst : Unique α] {p : α → Prop}, (∀ (a : α), p a) ↔ p default
-- Mathlib.Order.Filter.Interval
Filter.tendstoIxxClass_of_subset : ∀ {α : Type u_1} {l₁ l₂ : Filter α} {Ixx Ixx' : α → α → Set α},
  (∀ (a b : α), Ixx a b ⊆ Ixx' a b) → ∀ [h' : Filter.TendstoIxxClass Ixx' l₁ l₂], Filter.TendstoIxxClass Ixx l₁ l₂
-- Mathlib.Algebra.Group.WithOne.Map
WithZero.map₂_eq_bot_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {a : WithZero α} {b : WithZero β},
  WithZero.map₂ f a b = 0 ↔ a = 0 ∨ b = 0
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.forIn_eq_forIn : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} {δ : Type w}
  {m' : Type w → Type w'} [inst : Monad m'] [LawfulMonad m'] {f : (a : α) → β a → δ → m' (ForInStep δ)} {init : δ},
  Std.DHashMap.forIn f init m = forIn m init fun a b => f a.fst a.snd b
-- Mathlib.Order.RelSeries
RelSeries.toList_ne_nil : ∀ {α : Type u_1} {r : SetRel α α} (x : RelSeries r), x.toList ≠ []
-- Init.Grind.ToInt
/-- The embedding into the integers is monotone.
 -/
Lean.Grind.ToInt.LE : (α : Type u) → [LE α] → (I : outParam Lean.Grind.IntInterval) → [Lean.Grind.ToInt α I] → Prop
-- Mathlib.Data.Quot
/-- `Quotient.mk` is a surjective function.  -/
Quotient.mk_surjective : ∀ {α : Sort u_1} {s : Setoid α}, Function.Surjective (Quotient.mk s)
-- Mathlib.CategoryTheory.Sites.Subsheaf
CategoryTheory.Sheaf.imageι_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  {F F' : CategoryTheory.Sheaf J (Type w)} (f : F ⟶ F'),
  (CategoryTheory.Sheaf.imageι f).hom = (CategoryTheory.Subfunctor.sheafify J (CategoryTheory.Subfunctor.range f.hom)).ι
-- Mathlib.SetTheory.Ordinal.Notation
_private.Mathlib.SetTheory.Ordinal.Notation.0.ONote.opowAux2.match_1.eq_1 : ∀ (motive : ONote × ℕ → Sort u_1) (b : ONote) (h_1 : (b : ONote) → motive (b, 0))
  (h_2 : (b : ONote) → (k : ℕ) → motive (b, k.succ)),
  (match (b, 0) with
    | (b, 0) => h_1 b
    | (b, k.succ) => h_2 b k) =
    h_1 b
-- Mathlib.NumberTheory.ModularForms.Basic
ModularForm.instGAlgebra : (Γ : Subgroup (GL (Fin 2) ℝ)) → [inst : Γ.HasDetOne] → DirectSum.GAlgebra ℂ (ModularForm Γ)
-- Mathlib.Data.Nat.Cast.NeZero
NeZero.pos_of_neZero_natCast : ∀ (R : Type u_1) [inst : AddMonoidWithOne R] {n : ℕ} [NeZero ↑n], 0 < n
-- Mathlib.Algebra.Order.GroupWithZero.Basic
/-- See `div_self` for the version with equality when `a ≠ 0`.  -/
div_self_le_one : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : Preorder G₀] [ZeroLEOneClass G₀] (a : G₀), a / a ≤ 1
-- Lean.Environment
_private.Lean.Environment.0.Lean.Environment.RealizeConstResult.mk.inj : ∀ {newConsts : Lean.VisibilityMap✝ (List Lean.AsyncConst✝)}
  {replayKernel : Lean.Kernel.Environment → Task (Except Lean.Kernel.Exception Lean.Kernel.Environment)} {dyn : Dynamic}
  {newConsts_1 : Lean.VisibilityMap✝ (List Lean.AsyncConst✝)}
  {replayKernel_1 : Lean.Kernel.Environment → Task (Except Lean.Kernel.Exception Lean.Kernel.Environment)}
  {dyn_1 : Dynamic},
  { newConsts := newConsts, replayKernel := replayKernel, dyn := dyn } =
      { newConsts := newConsts_1, replayKernel := replayKernel_1, dyn := dyn_1 } →
    newConsts = newConsts_1 ∧ replayKernel = replayKernel_1 ∧ dyn = dyn_1
-- Mathlib.Algebra.Lie.Weights.IsSimple
/-- The invariant root submodule corresponding to a Lie ideal.

Given a Lie ideal `I`, this produces an invariant root submodule by taking the span of all
roots whose root spaces are contained in `I`.  -/
LieIdeal.toInvtRootSubmodule : {K : Type u_1} →
  {L : Type u_2} →
    [inst : Field K] →
      [inst_1 : LieRing L] →
        [inst_2 : LieAlgebra K L] →
          [inst_3 : FiniteDimensional K L] →
            {H : LieSubalgebra K L} →
              [inst_4 : H.IsCartanSubalgebra] →
                [inst_5 : CharZero K] →
                  [inst_6 : LieAlgebra.IsKilling K L] →
                    [inst_7 : LieModule.IsTriangularizable K (↥H) L] →
                      LieIdeal K L → ↥(LieAlgebra.IsKilling.rootSystem H).invtRootSubmodule
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
CategoryTheory.Bicategory.Adj.id_l : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] (a : CategoryTheory.Bicategory.Adj B),
  (CategoryTheory.CategoryStruct.id a).l = CategoryTheory.CategoryStruct.id a.obj
-- Mathlib.NumberTheory.RamificationInertia.HilbertTheory
/-- Let `L/K` be a Galois extension of fields and let `P` be a prime ideal of `B`. The predicate that
says that `E` is the inertia field of `P` in `L/K`, that is the subfield fixed by the inertia
subgroup of `P` in `Gal(L/K)`.
 -/
IsInertiaField : (K : Type u_2) →
  (L : Type u_3) →
    {B : Type u_4} →
      [inst : Field K] →
        [inst_1 : Field L] →
          [inst_2 : Algebra K L] →
            [inst_3 : CommRing B] →
              Ideal B → (E : Type u_6) → [inst_4 : Field E] → [Algebra E L] → [MulSemiringAction Gal(L/K) B] → Prop
-- Mathlib.Algebra.Order.CauSeq.Completion
CauSeq.Completion.ofRat_nnratCast : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] {β : Type u_2}
  [inst_3 : DivisionRing β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] (q : ℚ≥0), CauSeq.Completion.ofRat ↑q = ↑q