mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Range.Polymorphic.Map
Std.PRange.LawfulUpwardEnumerableLT.ofMap : ∀ {α : Type u_1} {β : Type u_2} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.UpwardEnumerable β]
  [inst_2 : LT α] [inst_3 : LT β] [Std.PRange.LawfulUpwardEnumerableLT β] (f : Std.PRange.UpwardEnumerable.Map α β)
  [f.PreservesLT], Std.PRange.LawfulUpwardEnumerableLT α
-- Mathlib.Algebra.Order.Group.Cyclic
LinearOrderedCommGroup.Subgroup.genLTOne_zpowers_eq_top : ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : LinearOrder G] [inst_2 : IsOrderedMonoid G] (H : Subgroup G)
  [inst_3 : Nontrivial ↥H] [hH : IsCyclic ↥H], Subgroup.zpowers (LinearOrderedCommGroup.Subgroup.genLTOne H) = H
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.mk'_cancel_right : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Submonoid R} {M : Type u_2} {M' : Type u_3} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M'] [inst_3 : Module R M] [inst_4 : Module R M'] (f : M →ₗ[R] M')
  [inst_5 : IsLocalizedModule S f] (m : M) (s₁ s₂ : ↥S),
  IsLocalizedModule.mk' f (s₂ • m) (s₁ * s₂) = IsLocalizedModule.mk' f m s₁
-- Init.Data.Option.Lemmas
Option.map_id_apply : ∀ {α : Type u} {x : Option α}, Option.map id x = x
-- Lean.Data.FuzzyMatching
Lean.FuzzyMatching.fuzzyMatchScoreWithThreshold? : String → String → optParam Float 0.1 → Option Float
-- Init.Data.UInt.Lemmas
UInt64.toBitVec_zero : UInt64.toBitVec 0 = 0#64
-- Mathlib.Data.Part
Part.eq_none_iff' : ∀ {α : Type u_1} {o : Part α}, o = Part.none ↔ ¬o.Dom
-- Mathlib.Algebra.Module.Torsion.Free
/-- An `R`-module `M` is torsion-free if scalar multiplication by an element `r : R` is injective if
multiplication (on `R`) by `r` is.

For domains, this is equivalent to the usual condition of `r • m = 0 → r = 0 ∨ m = 0`.
See `smul_eq_zero`.  -/
Module.IsTorsionFree : (R : Type u_1) → (M : Type u_3) → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [Module R M] → Prop
-- Init.Data.Vector.Lemmas
Vector.getElem_extract : ∀ {α : Type u_1} {n i : ℕ} {as : Vector α n} {start stop : ℕ} (h : i < min stop n - start),
  (as.extract start stop)[i] = as[start + i]
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.mapShortComplexH1_id_comp : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A B C : Rep.{u, u, u} k G} (φ : A ⟶ B) (ψ : B ⟶ C),
  groupHomology.mapShortComplexH1 (MonoidHom.id G) (CategoryTheory.CategoryStruct.comp φ ψ) =
    CategoryTheory.CategoryStruct.comp (groupHomology.mapShortComplexH1 (MonoidHom.id G) φ)
      (groupHomology.mapShortComplexH1 (MonoidHom.id G) ψ)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- Given a pair of maps between the summands of a pair of binary biproducts,
we obtain a map between the binary biproducts.  -/
CategoryTheory.Limits.biprod.map : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {W X Y Z : C} →
        [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct W X] →
          [inst_3 : CategoryTheory.Limits.HasBinaryBiproduct Y Z] → (W ⟶ Y) → (X ⟶ Z) → (W ⊞ X ⟶ Y ⊞ Z)
-- Lean.Widget.InteractiveDiagnostic
_private.Lean.Widget.InteractiveDiagnostic.0.Lean.Widget.EmbedFmt.code.sizeOf_spec : ∀ (ctx : Lean.Elab.ContextInfo) (infos : Std.TreeMap ℕ Lean.Elab.Info compare),
  sizeOf (Lean.Widget.EmbedFmt.code✝ ctx infos) = 1 + sizeOf ctx + sizeOf infos
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
UpperHalfPlane.σ_conj : ∀ (g : GL (Fin 2) ℝ) (z : ℂ), (UpperHalfPlane.σ g) ((starRingEnd ℂ) z) = (starRingEnd ℂ) ((UpperHalfPlane.σ g) z)
-- Mathlib.Topology.Algebra.Module.FiniteDimensionBilinear
ContinuousLinearMap.evalL_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : CompleteSpace 𝕜] {E : Type u_2} [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] [inst_4 : TopologicalSpace E] [inst_5 : IsTopologicalAddGroup E] [inst_6 : ContinuousSMul 𝕜 E]
  [inst_7 : FiniteDimensional 𝕜 E] [inst_8 : T2Space E] {F : Type u_3} [inst_9 : AddCommGroup F] [inst_10 : Module 𝕜 F]
  [inst_11 : TopologicalSpace F] [inst_12 : IsTopologicalAddGroup F] [inst_13 : ContinuousSMul 𝕜 F]
  [inst_14 : FiniteDimensional 𝕜 F] [inst_15 : T2Space F] (x : E) (φ : E →L[𝕜] F),
  ((ContinuousLinearMap.evalL 𝕜 E F) x) φ = φ x
-- Init.Prelude
/-- Subtraction of natural numbers, truncated at `0`. Usually used via the `-` operator.

If a result would be less than zero, then the result is zero.

This definition is overridden in both the kernel and the compiler to efficiently evaluate using the
arbitrary-precision arithmetic library. The definition provided here is the logical model.

Examples:
* `5 - 3 = 2`
* `8 - 2 = 6`
* `8 - 8 = 0`
* `8 - 20 = 0`
 -/
Nat.sub : ℕ → ℕ → ℕ
-- Mathlib.Analysis.Calculus.Deriv.Mul
Differentiable.div_const : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {𝕜' : Type u_2} [inst_1 : NormedDivisionRing 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {c : 𝕜 → 𝕜'}, Differentiable 𝕜 c → ∀ (d : 𝕜'), Differentiable 𝕜 fun x => c x / d
-- Mathlib.RingTheory.Frobenius
/-- A Frobenius element at `Q` restricts to the Frobenius map on `S ⧸ Q`.  -/
AlgHom.IsArithFrobAt.restrict : {R : Type u_1} →
  {S : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          {φ : S →ₐ[R] S} → {Q : Ideal S} → φ.IsArithFrobAt Q → S ⧸ Q →ₐ[R ⧸ Ideal.under R Q] S ⧸ Q
-- Batteries.Data.List.Lemmas
List.replaceF_cons : ∀ {α : Type u_1} {p : α → Option α} (a : α) (l : List α),
  List.replaceF p (a :: l) =
    match p a with
    | none => a :: List.replaceF p l
    | some a' => a' :: l
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.le_pi_iff : ∀ {η : Type u_7} {f : η → Type u_8} [inst : (i : η) → AddGroup (f i)] {I : Set η} {H : (i : η) → AddSubgroup (f i)}
  {J : AddSubgroup ((i : η) → f i)},
  J ≤ AddSubgroup.pi I H ↔ ∀ i ∈ I, J ≤ AddSubgroup.comap (Pi.evalAddMonoidHom f i) (H i)
-- Mathlib.Topology.Algebra.ProperAction.Basic
/-- If `G` acts on `X` properly, then the map `G × T → X × T, (g, t) ↦ (g +ᵥ t, t)` is still
proper for *any* subset `T` of `X`.  -/
ProperVAdd.isProperMap_vadd_pair_set : ∀ {G : Type u_1} {X : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G X] [inst_2 : TopologicalSpace G]
  [inst_3 : TopologicalSpace X] [ProperVAdd G X] {t : Set X}, IsProperMap fun gx => (gx.1 +ᵥ ↑gx.2, gx.2)
-- Mathlib.GroupTheory.Congruence.Defs
/-- The inductively defined smallest congruence relation containing a binary relation `r` equals
the infimum of the set of congruence relations containing `r`.  -/
Con.conGen_eq : ∀ {M : Type u_1} [inst : Mul M] (r : M → M → Prop), conGen r = sInf {s | ∀ (x y : M), r x y → s x y}
-- Mathlib.AlgebraicGeometry.ResidueField
/-- See `AlgebraicGeometry.IsClosedImmersion.SpecMap_residue` for the stronger result that
`Spec.map (X.residue x)` is a closed immersion.  -/
AlgebraicGeometry.Scheme.instIsPreimmersionMapResidue : ∀ {X : AlgebraicGeometry.Scheme} (x : ↥X), AlgebraicGeometry.IsPreimmersion (AlgebraicGeometry.Spec.map (X.residue x))
-- Mathlib.Algebra.Quaternion
Quaternion.coe_ofScientific : ∀ {R : Type u_1} [inst : Field R] (m : ℕ) (s : Bool) (e : ℕ),
  ↑(OfScientific.ofScientific m s e) = OfScientific.ofScientific m s e
-- Mathlib.CategoryTheory.Sites.Precoverage.Generates
CategoryTheory.Precoverage.Generates.isSheaf_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} A]
  {K : CategoryTheory.Precoverage C} {J : CategoryTheory.GrothendieckTopology C},
  K.Generates J →
    ∀ {F : CategoryTheory.Functor Cᵒᵖ A},
      CategoryTheory.Presheaf.IsSheaf J F ↔
        ∀ ⦃X : C⦄,
          ∀ R ∈ K.coverings X,
            ∀ (M : A), CategoryTheory.Presieve.IsSheafFor (F.comp (CategoryTheory.coyoneda.obj (Opposite.op M))) R
-- Init.Data.String.Basic
/-- Given a position in `s` that is at most `p₀`, obtain the corresponding position in `s.sliceTo p₀`.  -/
String.Pos.sliceTo : {s : String} → (p₀ pos : s.Pos) → pos ≤ p₀ → (s.sliceTo p₀).Pos
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.RcoSliceData.range : {α : Type u} → {β : Type v} → [inst : Ord α] → Std.DTreeMap.Internal.Const.RcoSliceData α β → Std.Rco α
-- Mathlib.Analysis.CStarAlgebra.Spectrum
/-- A non-unital star algebra homomorphism of complex C⋆-algebras is norm contractive.  -/
NonUnitalStarAlgHom.nnnorm_apply_le : ∀ {F : Type u_1} {A : Type u_2} {B : Type u_3} [inst : NonUnitalCStarAlgebra A] [inst_1 : NonUnitalCStarAlgebra B]
  [inst_2 : FunLike F A B] [NonUnitalAlgHomClass F ℂ A B] [StarHomClass F A B] (φ : F) (a : A), ‖φ a‖₊ ≤ ‖a‖₊
-- Lean.Meta.Sym.SymM
/-- Information about a function symbol. It stores which argument positions are proofs or instances,
enabling optimizations during pattern matching and structural definitional equality tests
such as skipping proof arguments or deferring instance synthesis.
 -/
Lean.Meta.Sym.ProofInstInfo : Type
-- Mathlib.RingTheory.FractionalIdeal.Inverse
FractionalIdeal.spanSingleton_inv_mul : ∀ (K : Type u_3) [inst : Field K] {R₁ : Type u_4} [inst_1 : CommRing R₁] [inst_2 : IsDomain R₁] [inst_3 : Algebra R₁ K]
  [inst_4 : IsFractionRing R₁ K] {x : K},
  x ≠ 0 →
    (FractionalIdeal.spanSingleton (nonZeroDivisors R₁) x)⁻¹ * FractionalIdeal.spanSingleton (nonZeroDivisors R₁) x = 1
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy
/-- `f` is left homotopic to `g` iff `g` is left homotopic to `f`.  -/
CategoryTheory.Arrow.LeftHomotopy.symm : {V : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    [inst_1 : CategoryTheory.Preadditive V] →
      {u v : CategoryTheory.Arrow V} →
        {f g : u ⟶ v} → CategoryTheory.Arrow.LeftHomotopy f g → CategoryTheory.Arrow.LeftHomotopy g f
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.decidableNonnegg : (c d : ℕ) → DecidableRel (Zsqrtd.Nonnegg c d)
-- Mathlib.ModelTheory.Complexity
_private.Mathlib.ModelTheory.Complexity.0.FirstOrder.Language.BoundedFormula.toPrenex.match_1.eq_3 : ∀ {L : FirstOrder.Language} {α : Type u_3} (motive : (x : ℕ) → L.BoundedFormula α x → Sort u_4) (x l : ℕ)
  (R : L.Relations l) (ts : Fin l → L.Term (α ⊕ Fin x))
  (h_1 : (x : ℕ) → motive x FirstOrder.Language.BoundedFormula.falsum)
  (h_2 : (x : ℕ) → (t₁ t₂ : L.Term (α ⊕ Fin x)) → motive x (FirstOrder.Language.BoundedFormula.equal t₁ t₂))
  (h_3 :
    (x l : ℕ) →
      (R : L.Relations l) → (ts : Fin l → L.Term (α ⊕ Fin x)) → motive x (FirstOrder.Language.BoundedFormula.rel R ts))
  (h_4 : (x : ℕ) → (f₁ f₂ : L.BoundedFormula α x) → motive x (f₁.imp f₂))
  (h_5 : (x : ℕ) → (f : L.BoundedFormula α (x + 1)) → motive x f.all),
  (match x, FirstOrder.Language.BoundedFormula.rel R ts with
    | x, FirstOrder.Language.BoundedFormula.falsum => h_1 x
    | x, FirstOrder.Language.BoundedFormula.equal t₁ t₂ => h_2 x t₁ t₂
    | x, FirstOrder.Language.BoundedFormula.rel R ts => h_3 x l R ts
    | x, f₁.imp f₂ => h_4 x f₁ f₂
    | x, f.all => h_5 x f) =
    h_3 x l R ts
-- Mathlib.Algebra.Group.Basic
zsmul_neg' : ∀ {α : Type u_1} [inst : SubtractionMonoid α] (a : α) (n : ℤ), n • -a = -n • a
-- Mathlib.Order.UpperLower.Hom
/-- `UpperSet.Ici` as a `SupHom`.  -/
UpperSet.iciSupHom : {α : Type u_1} → [inst : SemilatticeSup α] → SupHom α (UpperSet α)
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
MeasureTheory.AECover.biInter_Ici_aecover : ∀ {α : Type u_1} {ι : Type u_2} [Countable ι] [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
  [inst_1 : Preorder ι] {φ : ι → Set α},
  MeasureTheory.AECover μ Filter.atTop φ → MeasureTheory.AECover μ Filter.atTop fun n => ⋂ k ∈ Set.Ici n, φ k
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.negAddY_of_X_eq' : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} {P Q : Fin 3 → R},
  W'.Equation P →
    W'.Equation Q →
      P 0 * Q 2 ^ 2 = Q 0 * P 2 ^ 2 → W'.negAddY P Q * (P 2 * Q 2) ^ 3 = (P 1 * Q 2 ^ 3 - Q 1 * P 2 ^ 3) ^ 3
-- Mathlib.Topology.Semicontinuity.Basic
lowerSemicontinuous_iff_isClosed_epigraph : ∀ {α : Type u_1} [inst : TopologicalSpace α] {γ : Type u_4} [inst_1 : LinearOrder γ] [inst_2 : TopologicalSpace γ]
  [ClosedIciTopology γ] {f : α → γ}, LowerSemicontinuous f ↔ IsClosed {p | f p.1 ≤ p.2}
-- Lean.Parser.Types
/-- Modifies the ending position of a parser context.
 -/
Lean.Parser.ParserContext.setEndPos : (c : Lean.Parser.ParserContext) →
  (endPos : String.Pos.Raw) → endPos ≤ c.inputString.rawEndPos → Lean.Parser.ParserContext
-- Mathlib.Analysis.Asymptotics.Theta
Asymptotics.isTheta_norm_left : ∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E'] {g : α → F}
  {f' : α → E'} {l : Filter α}, (fun x => ‖f' x‖) =Θ[l] g ↔ f' =Θ[l] g
-- Mathlib.Algebra.Group.UniqueProds.Basic
UniqueProds.of_injective_mulHom : ∀ {G : Type u} {H : Type v} [inst : Mul G] [inst_1 : Mul H] (f : H →ₙ* G),
  Function.Injective ⇑f → UniqueProds G → UniqueProds H
-- Mathlib.CategoryTheory.Triangulated.Rotate
CategoryTheory.Pretriangulated.invRotCompRot_hom_app_hom₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  (X : CategoryTheory.Pretriangulated.Triangle C),
  (CategoryTheory.Pretriangulated.invRotCompRot.hom.app X).hom₂ = CategoryTheory.CategoryStruct.id X.obj₂
-- Lean.Parser.Command
Lean.Parser.Command.classInductive.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.rescale_zero_apply : ∀ {R : Type u_1} [inst : CommSemiring R] (f : PowerSeries R),
  (PowerSeries.rescale 0) f = PowerSeries.C (PowerSeries.constantCoeff f)
-- Mathlib.Topology.Algebra.Module.Complement
ContinuousLinearMap.isIdempotentElem_iff_eq_projectionL_range_ker : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {f : M →L[R] M},
  IsIdempotentElem f ↔ ∃ (h : Submodule.IsTopCompl (↑f).range (↑f).ker), f = (↑f).range.projectionL (↑f).ker h
-- Mathlib.Algebra.Ring.Parity
Even.neg_zpow : ∀ {α : Type u_2} [inst : DivisionMonoid α] [inst_1 : HasDistribNeg α] {n : ℤ}, Even n → ∀ (a : α), (-a) ^ n = a ^ n
-- Mathlib.Algebra.Ring.Associated
Associated.neg_left_iff : ∀ {M : Type u_1} [inst : Monoid M] [inst_1 : HasDistribNeg M] {a b : M}, Associated (-a) b ↔ Associated a b
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.mem_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {k a : α},
  a ∈ t.insert k ↔ cmp k a = Ordering.eq ∨ a ∈ t
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
IntermediateField.fg_top : ∀ (F : Type u_1) [inst : Field F] (E : Type u_2) [inst_1 : Field E] [inst_2 : Algebra F E] [Algebra.EssFiniteType F E],
  ⊤.FG
-- Mathlib.Analysis.Normed.Affine.Isometry
/-- The underlying linear equiv of an affine isometry equiv is in fact a linear isometry equiv.  -/
AffineIsometryEquiv.linearIsometryEquiv : {𝕜 : Type u_1} →
  {V : Type u_2} →
    {V₂ : Type u_5} →
      {P : Type u_10} →
        {P₂ : Type u_11} →
          [inst : NormedField 𝕜] →
            [inst_1 : SeminormedAddCommGroup V] →
              [inst_2 : NormedSpace 𝕜 V] →
                [inst_3 : PseudoMetricSpace P] →
                  [inst_4 : NormedAddTorsor V P] →
                    [inst_5 : SeminormedAddCommGroup V₂] →
                      [inst_6 : NormedSpace 𝕜 V₂] →
                        [inst_7 : PseudoMetricSpace P₂] → [inst_8 : NormedAddTorsor V₂ P₂] → (P ≃ᵃⁱ[𝕜] P₂) → V ≃ₗᵢ[𝕜] V₂
-- Mathlib.RingTheory.Polynomial.ScaleRoots
/-- `scaleRoots p s` is a polynomial with root `r * s` for each root `r` of `p`.  -/
Polynomial.scaleRoots : {R : Type u_1} → [inst : Semiring R] → Polynomial R → R → Polynomial R
-- Init.Data.Iterators.Consumers.Loop
/-- Returns `true` if the monadic predicate `p` returns `true` for
any element emitted by the iterator `it`.

`O(|xs|)`. Short-circuits upon encountering the first match. The elements in `it` are
examined in order of iteration.
 -/
Std.Iter.anyM : {α β : Type w} →
  {m : Type → Type w'} →
    [Monad m] → [inst : Std.Iterator α Id β] → [Std.IteratorLoop α Id m] → (β → m Bool) → Std.Iter β → m Bool
-- Mathlib.NumberTheory.PellMatiyasevic
Pell.xz_succ_succ : ∀ {a : ℕ} (a1 : 1 < a) (n : ℕ), Pell.xz a1 (n + 2) = ↑(2 * a) * Pell.xz a1 (n + 1) - Pell.xz a1 n
-- Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
/-- A sum taken over a conditional whose condition is an equality
test on the index and whose alternative is `0` has value either the term at that index or `0`.

The difference with `Finset.sum_ite_eq` is that the arguments to `Eq` are swapped.  -/
Finset.sum_ite_eq' : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : DecidableEq ι] (s : Finset ι) (a : ι) (b : ι → M),
  (∑ x ∈ s, if x = a then b x else 0) = if a ∈ s then b a else 0
-- Mathlib.Data.List.Infix
List.dropSlice_sublist : ∀ {α : Type u_1} (n m : ℕ) (l : List α), (List.dropSlice n m l).Sublist l
-- Mathlib.Order.RelClasses
Set.Unbounded.eq_1 : ∀ {α : Type u} (r : α → α → Prop) (s : Set α), Set.Unbounded r s = ∀ (a : α), ∃ b ∈ s, ¬r b a
-- Mathlib.Algebra.RingQuot
RingQuot.Rel.brecOn : ∀ {R : Type uR} [inst : Semiring R] {r : R → R → Prop} {motive : (a a_1 : R) → RingQuot.Rel r a a_1 → Prop} {a a_1 : R}
  (t : RingQuot.Rel r a a_1),
  (∀ (a a_2 : R) (t : RingQuot.Rel r a a_2), RingQuot.Rel.below t → motive a a_2 t) → motive a a_1 t
-- Mathlib.Analysis.Convex.Topology
Convex.combo_self_interior_mem_interior : ∀ {𝕜 : Type u_2} {E : Type u_3} [inst : Field 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] [inst_4 : TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] {s : Set E},
  Convex 𝕜 s → ∀ {x y : E}, x ∈ s → y ∈ interior s → ∀ {a b : 𝕜}, 0 ≤ a → 0 < b → a + b = 1 → a • x + b • y ∈ interior s
-- Mathlib.Algebra.Field.Defs
DivisionRing.toNNRatCast : {K : Type u_2} → [self : DivisionRing K] → NNRatCast K
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- Given `c : Classifier C`, `c.Ω₀` is a terminal object.
Prefer `c.χ₀` over `c.isTerminalΩ₀.from`.  -/
CategoryTheory.Subobject.Classifier.isTerminalΩ₀ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {c : CategoryTheory.Subobject.Classifier C} → CategoryTheory.Limits.IsTerminal c.Ω₀
-- Mathlib.Data.Set.Restrict
Set.eq_domRestrict_iff : ∀ {α : Type u_1} {π : α → Type u_6} {s : Set α} {f : (a : ↑s) → π ↑a} {g : (a : α) → π a},
  f = s.domRestrict g ↔ ∀ (a : α) (ha : a ∈ s), f ⟨a, ha⟩ = g a
-- Lean.Meta.Tactic.Grind.Parser
Lean.Parser.Command.GrindCnstr.notValue : Lean.Parser.Parser
-- Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
/-- The maximal real subfield of `K`. It is totally real,
see `NumberField.isTotallyReal_maximalRealSubfield`, and contains all the other totally real
subfields of `K`, see `NumberField.IsTotallyReal.le_maximalRealSubfield`.
 -/
NumberField.maximalRealSubfield : (K : Type u_2) → [inst : Field K] → Subfield K
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- If `F.cones` is represented by `X`, each morphism `f : Y ⟶ X` gives a cone with cone point
`Y`.  -/
CategoryTheory.Limits.IsLimit.OfNatIso.coneOfHom : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          {X : C} → F.cones.RepresentableBy X → {Y : C} → (Y ⟶ X) → CategoryTheory.Limits.Cone F
-- Init.Data.Option.Lemmas
_private.Init.Data.Option.Lemmas.0.Option.choice.eq_1 : ∀ (α : Type u_1), Option.choice α = if h : Nonempty α then some (Classical.choice h) else none
-- Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
CategoryTheory.Limits.zeroProdIso_inv_snd : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (X : C),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.zeroProdIso X).inv CategoryTheory.Limits.prod.snd =
    CategoryTheory.CategoryStruct.id X
-- Mathlib.Topology.ClusterPt
AccPt.clusterPt : ∀ {X : Type u} [inst : TopologicalSpace X] {x : X} {F : Filter X}, AccPt x F → ClusterPt x F
-- Mathlib.Order.Defs.LinearOrder
eq_or_lt_of_not_gt : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, ¬b < a → a = b ∨ a < b
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Real.logDeriv_sin : logDeriv Real.sin = Real.cot
-- Mathlib.Algebra.Order.Group.OrderIso
/-- `x ↦ x⁻¹` as an order-reversing equivalence.  -/
OrderIso.inv : (α : Type u) → [inst : Group α] → [inst_1 : LE α] → [MulLeftMono α] → [MulRightMono α] → α ≃o αᵒᵈ
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
SheafOfModules.relationsOfIsCokernelFree_s : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : CategoryTheory.HasSheafify J AddCommGrpCat]
  [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] {ι σ : Type u} {M : SheafOfModules R}
  (f : SheafOfModules.free ι ⟶ SheafOfModules.free σ) (g : SheafOfModules.free σ ⟶ M)
  (H : CategoryTheory.CategoryStruct.comp f g = 0)
  (H' : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ g H)) (a : ι),
  (SheafOfModules.relationsOfIsCokernelFree f g H H').s a =
    (CategoryTheory.Limits.kernel (SheafOfModules.generatorsOfIsCokernelFree f g H H').π).freeHomEquiv
      (CategoryTheory.Limits.kernel.lift (SheafOfModules.generatorsOfIsCokernelFree f g H H').π f ⋯) a
-- Mathlib.Data.List.TakeDrop
List.span.loop.eq_1 : ∀ {α : Type u} (p : α → Bool) (a : List α), List.span.loop p [] a = (a.reverse, [])
-- Mathlib.Algebra.Order.Floor.Ring
Int.fract_div_mul_self_add_zsmul_eq : ∀ {k : Type u_4} [inst : Field k] [inst_1 : LinearOrder k] [inst_2 : FloorRing k] (a b : k),
  a ≠ 0 → Int.fract (b / a) * a + ⌊b / a⌋ • a = b
-- Lean.Parser.Command
Lean.Parser.Command.openHiding.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.GroupWithZero.Defs
MonoidWithZero.mk : {M₀ : Type u} →
  [toMonoid : Monoid M₀] → [toZero : Zero M₀] → (∀ (a : M₀), 0 * a = 0) → (∀ (a : M₀), a * 0 = 0) → MonoidWithZero M₀
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get_union_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} (not_mem : k ∉ t₁) {h' : k ∈ t₁ ∪ t₂},
  (t₁ ∪ t₂).get k h' = t₂.get k ⋯
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.one_rpow : ∀ (x : ℝ), 1 ^ x = 1
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Formula.realize_iSup : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {β : Type v'} [inst_1 : Finite β]
  {f : β → L.Formula α} {v : α → M}, (FirstOrder.Language.Formula.iSup f).Realize v ↔ ∃ b, (f b).Realize v
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
/-- Pushing an additive free group basis through a group isomorphism.  -/
FreeAddGroupBasis.map : {ι : Type u_1} →
  {G : Type u_3} →
    {H : Type u_4} →
      [inst : AddGroup G] → [inst_1 : AddGroup H] → FreeAddGroupBasis ι G → G ≃+ H → FreeAddGroupBasis ι H
-- Mathlib.Data.Finset.Insert
Finset.eq_singleton_iff_nonempty_unique_mem : ∀ {α : Type u_1} {s : Finset α} {a : α}, s = {a} ↔ s.Nonempty ∧ ∀ x ∈ s, x = a
-- Mathlib.LinearAlgebra.Matrix.SemiringInverse
Matrix.detp_smul : ∀ {n : Type u_1} {R : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommSemiring R] (s : ℤˣ)
  (A : Matrix n n R) (c : R), Matrix.detp s (c • A) = c ^ Fintype.card n * Matrix.detp s A
-- Mathlib.Algebra.Module.StablyFree.FreeOfInvertible
_private.Mathlib.Algebra.Module.StablyFree.FreeOfInvertible.0.exteriorPower.cofactorToLeft_ιMulti_cons : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} {N : Type u_3} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] {n : ℕ} (bN : Module.Basis (Fin n) R N) (m : M),
  (exteriorPower.cofactorToLeft✝ bN) ((exteriorPower.ιMulti R (n + 1)) (Fin.cons (m, 0) fun i => (0, bN i))) = m