mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.NormNum.Inv
/-- The result of inverting a `norm_num` result.  -/
Mathlib.Meta.NormNum.Result.inv : {u : Lean.Level} →
  {α : Q(Type u)} →
    {a : Q(«$α»)} →
      Mathlib.Meta.NormNum.Result a →
        (dsα : Q(DivisionSemiring «$α»)) → Option Q(CharZero «$α») → Lean.MetaM (Mathlib.Meta.NormNum.Result q(«$a»⁻¹))
-- Mathlib.RingTheory.RamificationInertia.Ramification
/-- Let `S/R` be an extension of rings, and let `q` be a prime ideal of `S` lying over a prime ideal
`p` of `R`. Let `Sq` be the localization of `S` and `q`, and let `pSq` be the image of `p` in `Sq`.
Then the ramification index of `q` over `R` is defined to be the length of the quotient `Sq/pSq` as
an `Sq`-module.

When `q` is not prime, we use a junk value of `0`.

This will eventually replace the existing definition of `Ideal.ramificationIdx'`.  -/
Ideal.ramificationIdx : {S : Type u_1} → [inst : CommRing S] → Ideal S → (R : Type u_2) → [inst_1 : CommRing R] → [Algebra R S] → ℕ
-- Mathlib.Probability.ProductMeasure
MeasureTheory.Measure.piContent_eq_infinitePiNat : ∀ {X : ℕ → Type u_1} {mX : (n : ℕ) → MeasurableSpace (X n)} (μ : (n : ℕ) → MeasureTheory.Measure (X n))
  [hμ : ∀ (n : ℕ), MeasureTheory.IsProbabilityMeasure (μ n)] {A : Set ((n : ℕ) → X n)},
  A ∈ MeasureTheory.measurableCylinders X → (MeasureTheory.piContent μ) A = (MeasureTheory.Measure.infinitePiNat μ) A
-- Mathlib.Logic.Equiv.Basic
Equiv.piCongrLeft_symm_apply : ∀ {α : Sort u_1} {β : Sort u_4} (P : β → Sort w) (e : α ≃ β) (g : (b : β) → P b) (a : α),
  (Equiv.piCongrLeft P e).symm g a = g (e a)
-- Mathlib.Order.Hom.Lattice
SupHom.subtypeVal_apply : ∀ {β : Type u_3} [inst : SemilatticeSup β] {P : β → Prop} (Psup : ∀ ⦃x y : β⦄, P x → P y → P (x ⊔ y))
  (x : { x // P x }), (SupHom.subtypeVal Psup) x = ↑x
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.val_sup : ∀ {α : Type u_2} [inst : BooleanAlgebra α] {L : BooleanSubalgebra α} (a b : ↥L), ↑(a ⊔ b) = ↑a ⊔ ↑b
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast?_cons_of_false : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k},
  (k == a) = false → Std.Internal.List.getValueCast? a (⟨k, v⟩ :: l) = Std.Internal.List.getValueCast? a l
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_id_app : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] {F G : CategoryTheory.OplaxFunctor B CategoryTheory.Cat}
  (η : CategoryTheory.Oplax.StrongTrans F G) {a : B} {a' : CategoryTheory.Cat} (f : G.obj a ⟶ a') (X : ↑(F.obj a)),
  CategoryTheory.CategoryStruct.comp
      (f.toFunctor.map ((η.naturality (CategoryTheory.CategoryStruct.id a)).hom.toNatTrans.app X))
      (f.toFunctor.map ((G.mapId a).toNatTrans.app ((η.app a).toFunctor.obj X))) =
    CategoryTheory.CategoryStruct.comp (f.toFunctor.map ((η.app a).toFunctor.map ((F.mapId a).toNatTrans.app X)))
      (CategoryTheory.CategoryStruct.comp
        (f.toFunctor.map
          (CategoryTheory.CategoryStruct.id
            ((η.app a).toFunctor.obj ((CategoryTheory.CategoryStruct.id (F.obj a)).toFunctor.obj X))))
        (f.toFunctor.map (CategoryTheory.CategoryStruct.id ((η.app a).toFunctor.obj X))))
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
/-- In this file, Lean often has a hard time working out the values of `n` and `R` for an expression
like `det ↑A`. Rather than writing `(A : Matrix n n R)` everywhere in this file which is annoyingly
verbose, or `A.val` which is not the simp-normal form for subtypes, we create a local notation
`↑ₘA`. This notation references the local `n` and `R` variables, so is not valid as a global
notation.  -/
_private.Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup.0.Matrix.SpecialLinearGroup.«term↑ₘ_» : Lean.ParserDescr
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.div.eq_1 : ∀ {α : Type u_2} [inst : Div α], Set.div = { div := Set.image2 fun x1 x2 => x1 / x2 }
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.instInhabited : Inhabited FirstOrder.Language
-- Lean.Meta.Basic
Lean.Meta.DefEqContext.mk.inj : ∀ {lhs rhs : Lean.Expr} {lctx : Lean.LocalContext} {localInstances : Lean.LocalInstances} {lhs_1 rhs_1 : Lean.Expr}
  {lctx_1 : Lean.LocalContext} {localInstances_1 : Lean.LocalInstances},
  { lhs := lhs, rhs := rhs, lctx := lctx, localInstances := localInstances } =
      { lhs := lhs_1, rhs := rhs_1, lctx := lctx_1, localInstances := localInstances_1 } →
    lhs = lhs_1 ∧ rhs = rhs_1 ∧ lctx = lctx_1 ∧ localInstances = localInstances_1
-- Batteries.Control.AlternativeMonad
Option.instAlternativeMonad : AlternativeMonad Option
-- Mathlib.Algebra.Module.Submodule.EqLocus
LinearMap.ext_on_codisjoint : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_3} {M₂ : Type u_4} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  {F : Type u_5} [inst_6 : FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] {f g : F} {S T : Submodule R M},
  Codisjoint S T → Set.EqOn ⇑f ⇑g ↑S → Set.EqOn ⇑f ⇑g ↑T → f = g
-- Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
SSet.ι₀_fst : ∀ (X : SSet),
  CategoryTheory.CategoryStruct.comp SSet.ι₀
      (CategoryTheory.SemiCartesianMonoidalCategory.fst X (SSet.stdSimplex.obj { len := 1 })) =
    CategoryTheory.CategoryStruct.id X
-- Mathlib.CategoryTheory.Comma.Arrow
/-- The natural transformation from `leftFunc` to `rightFunc`, given by the arrow itself.  -/
CategoryTheory.Arrow.leftToRight : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Arrow.leftFunc ⟶ CategoryTheory.Arrow.rightFunc
-- Mathlib.Tactic.Simps.Basic
/-- Suppose we are given a structure `str` and a projection `proj`, that could be multiple nested
projections (separated by `_`), where each projection could be a projection of a parent structure.
This function returns an expression that is the composition of these projections and a
list of natural numbers, that are the projection numbers of the applied projections.
Note that this function is similar to elaborating dot notation, but it can do a little more.

Example: if we do
```
structure gradedFun (A : ℕ → Type*) where
  toFun := ∀ i j, A i →+ A j →+ A (i + j)
initialize_simps_projections (toFun_toFun_toFun → myMul)
```
we will be able to generate the "projection"
  `fun {A} (f : gradedFun A) (x : A i) (y : A j) ↦ ↑(↑(f.toFun i j) x) y`,
which projection notation cannot do.  -/
Simps.getCompositeOfProjections : Lean.Name → String → Lean.MetaM (Lean.Expr × Array ℕ)
-- Mathlib.Analysis.Normed.Algebra.Unitization
/-- In a `RegularNormedAlgebra`, the map `Unitization.splitMul 𝕜 A` is injective.
We will use this to pull back the norm from `𝕜 × (A →L[𝕜] A)` to `Unitization 𝕜 A`.  -/
Unitization.splitMul_injective : ∀ (𝕜 : Type u_1) (A : Type u_2) [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : NormedSpace 𝕜 A] [inst_3 : IsScalarTower 𝕜 A A] [inst_4 : SMulCommClass 𝕜 A A] [RegularNormedAlgebra 𝕜 A],
  Function.Injective ⇑(Unitization.splitMul 𝕜 A)
-- Lean.Parser.Command
Lean.Parser.Command.noncomputable : Lean.Parser.Parser
-- Mathlib.Computability.Partrec
Vector.mOfFn_part_some : ∀ {α : Type u_1} {n : ℕ} (f : Fin n → α), (List.Vector.mOfFn fun i => Part.some (f i)) = Part.some (List.Vector.ofFn f)
-- Mathlib.Algebra.Order.GroupWithZero.Action.Synonym
Lex.instMulActionWithZero' : {G₀ : Type u_1} →
  {M₀ : Type u_2} →
    [inst : MonoidWithZero G₀] → [inst_1 : AddMonoid M₀] → [MulActionWithZero G₀ M₀] → MulActionWithZero G₀ (Lex M₀)
-- Mathlib.Analysis.Calculus.LagrangeMultipliers
/-- Lagrange multipliers theorem, 1d version. Let `f : ι → E → ℝ` be a finite family of functions.
Suppose that `φ : E → ℝ` has a local extremum on the set `{x | ∀ i, f i x = f i x₀}` at `x₀`.
Suppose that all functions `f i` as well as `φ` are strictly differentiable at `x₀`.
Then the derivatives `f' i : E → L[ℝ] ℝ` and `φ' : StrongDual ℝ E` are linearly dependent:
there exist `Λ : ι → ℝ` and `Λ₀ : ℝ`, `(Λ, Λ₀) ≠ 0`, such that `∑ i, Λ i • f' i + Λ₀ • φ' = 0`.

See also `IsLocalExtrOn.linear_dependent_of_hasStrictFDerivAt` for a version that
states `¬LinearIndependent ℝ _` instead of existence of `Λ` and `Λ₀`.  -/
IsLocalExtrOn.exists_multipliers_of_hasStrictFDerivAt : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {φ : E → ℝ} {x₀ : E}
  {φ' : StrongDual ℝ E} {ι : Type u_3} [inst_3 : Fintype ι] {f : ι → E → ℝ} {f' : ι → StrongDual ℝ E},
  IsLocalExtrOn φ {x | ∀ (i : ι), f i x = f i x₀} x₀ →
    (∀ (i : ι), HasStrictFDerivAt (f i) (f' i) x₀) →
      HasStrictFDerivAt φ φ' x₀ → ∃ Λ Λ₀, (Λ, Λ₀) ≠ 0 ∧ ∑ i, Λ i • f' i + Λ₀ • φ' = 0
-- Lean.Server.Requests
Lean.Server.LspResponse.mk : {α : Type} → α → Bool → Lean.Server.LspResponse α
-- Mathlib.FieldTheory.Galois.Basic
IntermediateField.fixingSubgroup_top : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E], ⊤.fixingSubgroup = ⊥
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupNorm.coe_lt_coe : ∀ {E : Type u_3} [inst : Group E] {p q : GroupNorm E}, ⇑p < ⇑q ↔ p < q
-- Init.System.IO
/-- Given a non-empty list of tasks, wait for the first to complete.
Return the value and the list of remaining tasks.
 -/
IO.waitAny' : {α : Type} → (tasks : List (Task α)) → autoParam (0 < tasks.length) IO.waitAny'._auto_1 → BaseIO (α × List (Task α))
-- Mathlib.RingTheory.Polynomial.GaussNorm
Polynomial.exists_eq_gaussNorm : ∀ {R : Type u_1} {F : Type u_2} [inst : Semiring R] [inst_1 : FunLike F R ℝ] (v : F) (c : ℝ) (p : Polynomial R)
  [ZeroHomClass F R ℝ], ∃ i, Polynomial.gaussNorm v c p = v (p.coeff i) * c ^ i
-- Mathlib.Tactic.ClickSuggestions.ApplyAt
Mathlib.Tactic.ClickSuggestions.ApplyAtLemma.mk.inj : ∀ {name name_1 : Mathlib.Tactic.ClickSuggestions.Premise}, { name := name } = { name := name_1 } → name = name_1
-- Mathlib.Logic.Nontrivial.Defs
Bool.instNontrivial : Nontrivial Bool
-- Init.Data.BitVec.Lemmas
BitVec.not_not : ∀ {w : ℕ} {b : BitVec w}, ~~~~~~b = b
-- Mathlib.Algebra.Notation.Indicator
/-- See `Set.eqOn_indicator` for the version with `s`.  -/
Set.eqOn_indicator' : ∀ {α : Type u_1} {M : Type u_3} [inst : Zero M] {s : Set α} {f : α → M}, Set.EqOn (s.indicator f) 0 sᶜ
-- Mathlib.LinearAlgebra.Matrix.Irreducible.Defs
/-- A matrix `A` is irreducible if it is entrywise nonnegative and
its quiver of positive entries (`toQuiver A`) is strongly connected.  -/
Matrix.IsIrreducible : {n : Type u_1} → {R : Type u_2} → [Ring R] → [LinearOrder R] → Matrix n n R → Prop
-- Batteries.Data.String.Matcher
/-- Accumulator loop for `String.Matcher.findAll`  -/
String.Matcher.findAll.loop : String.Matcher → Substring.Raw → Array.Matcher Char → Array Substring.Raw → Array Substring.Raw
-- Aesop.Stats.Basic
Aesop.instInhabitedForwardInstantiationStats : Inhabited Aesop.ForwardInstantiationStats
-- Aesop.Script.Step
Aesop.Script.LazyStep.mk.sizeOf_spec : ∀ (preState : Lean.Meta.SavedState) (preGoal : Lean.MVarId) (tacticBuilders : Array Aesop.Script.TacticBuilder)
  (tacticBuilders_ne : autoParam (0 < tacticBuilders.size) Aesop.Script.LazyStep.tacticBuilders_ne._autoParam)
  (postState : Lean.Meta.SavedState) (postGoals : Array Lean.MVarId),
  sizeOf
      { preState := preState, preGoal := preGoal, tacticBuilders := tacticBuilders,
        tacticBuilders_ne := tacticBuilders_ne, postState := postState, postGoals := postGoals } =
    1 + sizeOf preState + sizeOf preGoal + sizeOf tacticBuilders + sizeOf tacticBuilders_ne + sizeOf postState +
      sizeOf postGoals
-- Mathlib.Data.Nat.Prime.Factorial
Nat.Prime.coprime_descFactorial_of_lt_of_le : ∀ {p n k : ℕ}, Nat.Prime p → n < p → k ≤ n → p.Coprime (n.descFactorial k)
-- Init.Data.Iterators.Basic
/-- `IterStep.yield it out` describes the situation that an iterator emits `out` and provides `it`
as the succeeding iterator.
 -/
Std.IterStep.yield : {α : Sort u_1} → {β : Sort u_2} → α → β → Std.IterStep α β
-- Mathlib.RingTheory.Multiplicity
le_emultiplicity_of_pow_dvd : ∀ {α : Type u_1} [inst : Monoid α] {a b : α} {k : ℕ}, a ^ k ∣ b → ↑k ≤ emultiplicity a b
-- Mathlib.Data.List.Sort
/-- **Alias** of the reverse direction of `List.sortedGT_map_toDual`. -/
List.SortedLT.of_map_toDual : ∀ {α : Type u_1} [inst : Preorder α] {l : List αᵒᵈ}, l.SortedLT → (List.map (⇑OrderDual.toDual) l).SortedGT
-- Mathlib.LinearAlgebra.Determinant
/-- If the determinant of a map vanishes, then the map is not onto.  -/
LinearMap.range_lt_top_of_det_eq_zero : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsDomain R]
  [Module.Free R M] {f : M →ₗ[R] M}, LinearMap.det f = 0 → f.range < ⊤
-- Mathlib.RingTheory.TotallySplit
Algebra.IsFiniteSplit.inst : ∀ {R : Type u_2} [inst : CommRing R], Algebra.IsFiniteSplit R R
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.weierstrassP.eq_1 : ∀ (L : PeriodPair) (z : ℂ), L.weierstrassP z = ∑' (l : ↥L.lattice), (1 / (z - ↑l) ^ 2 - 1 / ↑l ^ 2)
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
AddSubmonoid.op_closure : ∀ {M : Type u_2} [inst : AddZeroClass M] (s : Set M),
  (AddSubmonoid.closure s).op = AddSubmonoid.closure (AddOpposite.unop ⁻¹' s)
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
/-- Auxiliary definition for the lemma `OneHypercoverDenseData.isSheaf_iff`.  -/
_private.Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense.0.CategoryTheory.Functor.OneHypercoverDenseData.isSheaf_iff.lift : {C₀ : Type u₀} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v₀, u₀} C₀] →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {F : CategoryTheory.Functor C₀ C} →
          {J₀ : CategoryTheory.GrothendieckTopology C₀} →
            {J : CategoryTheory.GrothendieckTopology C} →
              {A : Type u'} →
                [inst_2 : CategoryTheory.Category.{v', u'} A] →
                  [inst_3 : CategoryTheory.Functor.IsDenseSubsite J₀ J F] →
                    {data : (X : C) → F.OneHypercoverDenseData J₀ J X} →
                      {G : CategoryTheory.Functor Cᵒᵖ A} →
                        CategoryTheory.Presheaf.IsSheaf J₀ (F.op.comp G) →
                          ((X : C) → CategoryTheory.Limits.IsLimit ((data X).toOneHypercover.multifork G)) →
                            {X : C} →
                              {S : J.Cover X} →
                                (s : CategoryTheory.Limits.Multifork (S.index G)) → s.pt ⟶ G.obj (Opposite.op X)
-- Mathlib.Algebra.Group.Submonoid.Membership
FreeMonoid.closure_range_of : ∀ {α : Type u_4}, Submonoid.closure (Set.range FreeMonoid.of) = ⊤
-- Mathlib.Data.Fin.Tuple.Reflection
/-- This can be used to prove
```lean
example (P : (Fin 2 → α) → Prop) : (∀ f, P f) ↔ ∀ a₀ a₁, P ![a₀, a₁] :=
  (forall_iff _).symm
```
 -/
FinVec.forall_iff : ∀ {α : Type u_1} {m : ℕ} (P : (Fin m → α) → Prop), FinVec.Forall P ↔ ∀ (x : Fin m → α), P x
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.adj_and_reachable_delete_edges_iff_exists_cycle : ∀ {V : Type u} {G : SimpleGraph V} {v w : V},
  G.Adj v w ∧ (G.deleteEdges {s(v, w)}).Reachable v w ↔ ∃ u p, p.IsCycle ∧ s(v, w) ∈ p.edges
-- ImportGraph.Imports.RequiredModules
/-- Return the names of the constants used in the specified declaration,
and the constants they use transitively.
 -/
Lean.Name.transitivelyUsedConstants : Lean.Name → Lean.CoreM Lean.NameSet
-- Mathlib.Analysis.Normed.Operator.Mul
ContinuousLinearMap.opENorm_mul : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] (R : Type u_3) [inst_1 : NonUnitalNormedRing R]
  [inst_2 : NormedSpace 𝕜 R] [inst_3 : IsScalarTower 𝕜 R R] [inst_4 : SMulCommClass 𝕜 R R] [RegularNormedAlgebra 𝕜 R]
  [Nontrivial R], ‖ContinuousLinearMap.mul 𝕜 R‖ₑ = 1
-- Mathlib.CategoryTheory.Sites.Over
CategoryTheory.GrothendieckTopology.over_map_compatiblePreserving : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {X Y : C}
  (f : X ⟶ Y), CategoryTheory.CompatiblePreserving (J.over Y) (CategoryTheory.Over.map f)
-- Mathlib.CategoryTheory.Triangulated.TriangleShift
/-- The shift functor `Triangle C ⥤ Triangle C` by `n : ℤ` sends a triangle
to the triangle obtained by shifting the objects by `n` in `C` and by
multiplying the three morphisms by `(-1)^n`.  -/
CategoryTheory.Pretriangulated.Triangle.shiftFunctor : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.HasShift C ℤ] →
        ℤ →
          CategoryTheory.Functor (CategoryTheory.Pretriangulated.Triangle C) (CategoryTheory.Pretriangulated.Triangle C)
-- Lean.Meta.Sym.Canon
_private.Lean.Meta.Sym.Canon.0.Lean.Meta.Sym.Canon.Context.mk.injEq : ∀ (insideType insideType_1 : Bool),
  ({ insideType := insideType } = { insideType := insideType_1 }) = (insideType = insideType_1)
-- Mathlib.Analysis.InnerProductSpace.Positive
LinearMap.IsPositive.eq_1 : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (T : E →ₗ[𝕜] E), T.IsPositive = (T.IsSymmetric ∧ ∀ (x : E), 0 ≤ RCLike.re (inner 𝕜 (T x) x))
-- Mathlib.Topology.Spectral.Basic
SpectralSpace.toPrespectralSpace : ∀ {X : Type u_3} {inst : TopologicalSpace X} [self : SpectralSpace X], PrespectralSpace X
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.colimMap.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F G : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasColimit F]
  [inst_3 : CategoryTheory.Limits.HasColimit G] (α : G ⟶ F),
  CategoryTheory.Limits.colimMap α =
    (CategoryTheory.Limits.colimit.isColimit G).map (CategoryTheory.Limits.colimit.cocone F) α
-- Mathlib.LinearAlgebra.Dimension.Basic
rank_range_le : ∀ {R : Type u} {M M₁ : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid M₁] [inst_4 : Module R M₁] (f : M →ₗ[R] M₁), Module.rank R ↥f.range ≤ Module.rank R M
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.Prod.sectR_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (Z : C) (D : Type u₂)
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (X : D), (CategoryTheory.Prod.sectR Z D).obj X = (Z, X)
-- Mathlib.RingTheory.Valuation.RankOne
ValuativeRel.IsRankLeOne.of_compatible_mulArchimedean : ∀ {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] {R : Type u_3} [inst_1 : Ring R] [inst_2 : ValuativeRel R]
  [MulArchimedean Γ₀] (v : Valuation R Γ₀) [v.Compatible], ValuativeRel.IsRankLeOne R
-- Mathlib.Topology.Algebra.Monoid.Defs
ContinuousWithinAt.mul_const : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : Mul M] [SeparatelyContinuousMul M] {X : Type u_2}
  [inst_3 : TopologicalSpace X] {f : X → M} {s : Set X} {x : X},
  ContinuousWithinAt f s x → ∀ (b : M), ContinuousWithinAt (fun x => f x * b) s x
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax
CategoryTheory.Lax.OplaxTrans.rightUnitor_hom_as_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.LaxFunctor B C} (η : F ⟶ G) (a : B),
  (CategoryTheory.Lax.OplaxTrans.rightUnitor η).hom.as.app a = (CategoryTheory.Bicategory.rightUnitor (η.app a)).hom
-- Mathlib.CategoryTheory.Triangulated.Triangulated
/-- The triangle `Z₁₂ ⟶ Z₁₃ ⟶ Z₂₃ ⟶ Z₁₂⟦1⟧` given by an octahedron.  -/
CategoryTheory.Triangulated.Octahedron.triangle : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        [inst_3 : CategoryTheory.HasShift C ℤ] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [inst_5 : CategoryTheory.Pretriangulated C] →
              {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} →
                {u₁₂ : X₁ ⟶ X₂} →
                  {u₂₃ : X₂ ⟶ X₃} →
                    {u₁₃ : X₁ ⟶ X₃} →
                      {comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃} →
                        {v₁₂ : X₂ ⟶ Z₁₂} →
                          {w₁₂ : Z₁₂ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁} →
                            {h₁₂ :
                                CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈
                                  CategoryTheory.Pretriangulated.distinguishedTriangles} →
                              {v₂₃ : X₃ ⟶ Z₂₃} →
                                {w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₂} →
                                  {h₂₃ :
                                      CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈
                                        CategoryTheory.Pretriangulated.distinguishedTriangles} →
                                    {v₁₃ : X₃ ⟶ Z₁₃} →
                                      {w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁} →
                                        {h₁₃ :
                                            CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈
                                              CategoryTheory.Pretriangulated.distinguishedTriangles} →
                                          CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃ →
                                            CategoryTheory.Pretriangulated.Triangle C
-- Mathlib.RingTheory.AlgebraicIndependent.Basic
IsTranscendenceBasis.to_subtype_range' : ∀ {ι : Type u} {R : Type u_2} {A : Type v} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A],
  IsTranscendenceBasis R x → ∀ {t : Set A}, Set.range x = t → IsTranscendenceBasis R Subtype.val
-- Mathlib.Combinatorics.Digraph.Basic
Digraph.Bot.adjDecidable : (V : Type u_2) → DecidableRel ⊥.Adj
-- Mathlib.Tactic.Attr.Register
/-- Simplification procedure  -/
Parser.Attr.coassoc_simps_proc : Lean.ParserDescr
-- Mathlib.Order.OrdContinuous
/-- **Alias** of `RightOrdContinuous.dual`. -/
RightOrdContinuous.orderDual : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  RightOrdContinuous f → LeftOrdContinuous (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual)
-- Mathlib.Algebra.Homology.Single
/-- The functor `V ⥤ HomologicalComplex V c` creating a chain complex supported in a single degree.
 -/
HomologicalComplex.single : (V : Type u) →
  [inst : CategoryTheory.Category.{v, u} V] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
      [CategoryTheory.Limits.HasZeroObject V] →
        {ι : Type u_1} → [DecidableEq ι] → (c : ComplexShape ι) → ι → CategoryTheory.Functor V (HomologicalComplex V c)
-- Mathlib.FieldTheory.Minpoly.ConjRootClass
ConjRootClass.mk_eq_zero_iff : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (x : L),
  ConjRootClass.mk K x = 0 ↔ x = 0
-- Mathlib.CategoryTheory.Monoidal.Braided.PushoutObjObj
CategoryTheory.Functor.PushoutObjObj.flipTensor_inr : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {X₁ Y₁ X₂ Y₂ : C} {f₁ : X₁ ⟶ Y₁} {f₂ : X₂ ⟶ Y₂}
  (sq : (CategoryTheory.MonoidalCategory.curriedTensor C).PushoutObjObj f₁ f₂),
  sq.flipTensor.inr = CategoryTheory.CategoryStruct.comp (β_ X₂ Y₁).hom sq.inl
-- Std.Data.TreeMap.Raw.Basic
Std.TreeMap.Raw.instInter : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Inter (Std.TreeMap.Raw α β cmp)
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.inj_comp_cofanPtIsoSelf_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Limits.FormalCoproduct C) (i : X.I),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.FormalCoproduct.cofan X.I X.toFun).inj i)
      X.cofanPtIsoSelf.hom =
    CategoryTheory.Limits.FormalCoproduct.Hom.fromIncl i (CategoryTheory.CategoryStruct.id (X.obj i))
-- Mathlib.CategoryTheory.Sites.Precoverage
CategoryTheory.Precoverage.instHasIsosMin : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J K : CategoryTheory.Precoverage C) [J.HasIsos] [K.HasIsos],
  (J ⊓ K).HasIsos