mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.opcyclesIsoH_hom : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i₀ i₁ : ι} (f : i₀ ⟶ i₁) (n₀ n₁ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.opcyclesIsoH_hom._auto_1),
  (X.opcyclesIsoH f n₀ n₁ hn₁).hom = X.fromOpcycles f (CategoryTheory.CategoryStruct.id i₁) f ⋯ n₁
-- Mathlib.RingTheory.Nullstellensatz
MvPolynomial.IsPrime.vanishingIdeal_zeroLocus : ∀ {k : Type u_1} {K : Type u_2} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K] {σ : Type u_3}
  [IsAlgClosed K] [Finite σ] (P : Ideal (MvPolynomial σ k)) [h : P.IsPrime],
  MvPolynomial.vanishingIdeal k (MvPolynomial.zeroLocus K P) = P
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.instMembership : {α : Type u_1} → Membership α (FreeAddMonoid α)
-- Lean.Elab.PreDefinition.WF.Eqns
Lean.Elab.WF.EqnInfo.value : Lean.Elab.WF.EqnInfo → Lean.Expr
-- Init.Data.UInt.Bitwise
UInt16.ofBitVec_or : ∀ (a b : BitVec 16), { toBitVec := a ||| b } = { toBitVec := a } ||| { toBitVec := b }
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas
_private.Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas.0.Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.ofArray_fold_fn.match_1.eq_2 : ∀ {n : ℕ} (motive : Option (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) → Sort u_1)
  (l : Std.Tactic.BVDecide.LRAT.Internal.PosFin n) (h_1 : Unit → motive none)
  (h_2 : (l : Std.Tactic.BVDecide.LRAT.Internal.PosFin n) → motive (some (l, true)))
  (h_3 : (l : Std.Tactic.BVDecide.LRAT.Internal.PosFin n) → motive (some (l, false))),
  (match some (l, true) with
    | none => h_1 ()
    | some (l, true) => h_2 l
    | some (l, false) => h_3 l) =
    h_2 l
-- Mathlib.Order.BooleanAlgebra.Set
LE.le.sdiff_ssubset_of_nonempty : ∀ {α : Type u_1} {s t : Set α}, s ⊆ t → s.Nonempty → t \ s ⊂ t
-- Std.Internal.Do.PredTrans
/-- Push an `Except ε α` result into separate normal and exception postconditions:
`ok a` uses `post a`, and `error e` uses `epost.head e`.  -/
Std.Internal.Do.EPost.Cons.pushExcept : {α : Type u} →
  {ε : Type v} → {Pred : Type w} → {EPred : Type z} → (α → Pred) → EPost.Cons✝ (ε → Pred) EPred → Except ε α → Pred
-- Mathlib.SetTheory.Lists
/-- Recursion/induction principle for `Lists'.ofList`.  -/
Lists'.recOfList : {α : Type u_1} →
  {motive : Lists' α true → Sort u_2} →
    ((l : List (Lists α)) → motive (Lists'.ofList l)) → (l : Lists' α true) → motive l
-- Mathlib.Topology.Compactness.CountablyCompact
isSeqCompact_iff_isSeqCompact_univ : ∀ {E : Type u_2} [inst : TopologicalSpace E] {A : Set E}, IsSeqCompact A ↔ IsSeqCompact Set.univ
-- Mathlib.Condensed.Discrete.Colimit
/-- A finite set as a coproduct cocone in `Profinite` over itself.  -/
Condensed.fintypeCatAsCofan : (X : Profinite) → CategoryTheory.Limits.Cofan fun x => Profinite.of PUnit.{u + 1}
-- Aesop.Index.Basic
Aesop.IndexMatchLocation.hyp.sizeOf_spec : ∀ (ldecl : Lean.LocalDecl), sizeOf (Aesop.IndexMatchLocation.hyp ldecl) = 1 + sizeOf ldecl
-- Lean.Server.Rpc.Basic
/-- Version `1` is like `0`,
except that RPC references are serialized as `{"__rpcref": n}`.  -/
Lean.Lsp.RpcWireFormat.v1 : Lean.Lsp.RpcWireFormat
-- Std.Sat.CNF.Dimacs
_private.Std.Sat.CNF.Dimacs.0.Std.Sat.CNF.DimacsM.handleLit : Std.Sat.Literal ℕ → Std.Sat.CNF.DimacsM✝ Unit
-- Mathlib.ModelTheory.Syntax
/-- The `Finset` of variables used in a given term.  -/
FirstOrder.Language.Term.varFinset : {L : FirstOrder.Language} → {α : Type u'} → [DecidableEq α] → L.Term α → Finset α
-- Mathlib.LinearAlgebra.TensorProduct.Subalgebra
/-- If `A` is a subalgebra of `S/R`, there is the natural `R`-algebra isomorphism between
`A ⊗[R] i(R)` and `A` induced by multiplication in `S`, here `i : R → S` is the structure map.
This generalizes `Algebra.TensorProduct.rid` as `i(R)` is not necessarily isomorphic to `R`.

This is the `Subalgebra` version of `Submodule.rTensorOne`  -/
Subalgebra.rTensorBot : {R : Type u_1} →
  {S : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : Semiring S] → [inst_2 : Algebra R S] → (A : Subalgebra R S) → TensorProduct R ↥A ↥⊥ ≃ₐ[R] ↥A
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.sInf_compl_lt_lift_ord_succ : ∀ {ι : Type u} (f : ι → Ordinal.{max u v}), sInf (Set.range f)ᶜ < Ordinal.lift.{v, u} (Order.succ (Cardinal.mk ι)).ord
-- Init.Data.UInt.Bitwise
UInt16.or_eq_zero_iff : ∀ {a b : UInt16}, a ||| b = 0 ↔ a = 0 ∧ b = 0
-- Init.PropLemmas
Bool.ite_then_false_eq_false : ∀ {p : Prop} [inst : Decidable p] {x : Bool}, (if p then false else x) = false ↔ p ∨ x = false
-- Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
HurwitzKernelBounds.isBigO_exp_neg_mul_of_le : ∀ {c d : ℝ}, c ≤ d → (fun t => Real.exp (-d * t)) =O[Filter.atTop] fun t => Real.exp (-c * t)
-- Mathlib.Data.Real.ConjExponents
Real.HolderTriple.lt : ∀ {p q r : ℝ}, p.HolderTriple q r → r < p
-- Mathlib.Data.Multiset.Count
Multiset.ext : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Multiset α}, s = t ↔ ∀ (a : α), Multiset.count a s = Multiset.count a t
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.BitVec.Signed.rotate.eq_1 : ∀ {n : ℕ} (x : BitVec n), BitVec.Signed.rotate✝ x = x + BitVec.Signed.intMinSealed✝ n
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.eq_iff_unitGroup : ∀ {K : Type u} [inst : Field K] {A B : ValuationSubring K}, A = B ↔ A.unitGroup = B.unitGroup
-- Init.Data.String.Iterate
String.Slice.RevByteIterator.instIteratorUInt8OfPure : {m : Type → Type u_1} → [Pure m] → Std.Iterator String.Slice.RevByteIterator m UInt8
-- Mathlib.LinearAlgebra.AffineSpace.Combination
Finset.affineCombinationLineMapWeights_apply_of_ne : ∀ {k : Type u_1} [inst : Ring k] {ι : Type u_4} [inst_1 : DecidableEq ι] {i j t : ι},
  t ≠ i → t ≠ j → ∀ (c : k), Finset.affineCombinationLineMapWeights i j c t = 0
-- Mathlib.Tactic.Abel
_private.Mathlib.Tactic.Abel.0.Mathlib.Tactic.Abel.instEvalExprConfig.evalExpr : Lean.Expr → Lean.MetaM Mathlib.Tactic.AtomM.Recurse.Config
-- Mathlib.Topology.LocallyConstant.Basic
/-- If a composition of a function `f` followed by an injection `g` is locally
constant, then the locally constant property descends to `f`.  -/
IsLocallyConstant.desc : ∀ {X : Type u_1} [inst : TopologicalSpace X] {α : Type u_5} {β : Type u_6} (f : X → α) (g : α → β),
  IsLocallyConstant (g ∘ f) → Function.Injective g → IsLocallyConstant f
-- Mathlib.Order.Filter.CardinalInter
/-- A filter `l` has the cardinal `c` intersection property if for any collection
of less than `c` sets `s ∈ l`, their intersection belongs to `l` as well.  -/
CardinalInterFilter : {α : Type u} → Filter α → Cardinal.{u} → Prop
-- Init.Data.UInt.Bitwise
UInt32.toUSize_shiftLeft_of_lt : ∀ (a b : UInt32), b < 32 → (a <<< b).toUSize = a.toUSize <<< b.toUSize % 4294967296
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
_private.Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn.0.MeasureTheory.SignedMeasure.restrictNonposSeq_subset : ∀ {α : Type u_1} [inst : MeasurableSpace α] {s : MeasureTheory.SignedMeasure α} {i : Set α} (n : ℕ),
  MeasureTheory.SignedMeasure.restrictNonposSeq✝ s i n ⊆ i
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
/-- **Alias** of `Submodule.lipschitzWith_orthogonalProjectionOnto`.

---

The orthogonal projection onto a closed subspace is a `1`-Lipschitz map.  -/
Submodule.lipschitzWith_orthogonalProjection : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : Submodule 𝕜 E) [inst_3 : K.HasOrthogonalProjection], LipschitzWith 1 ⇑K.orthogonalProjectionOnto
-- Mathlib.Data.Int.GCD
Nat.gcdB_zero_right : ∀ {s : ℕ}, s ≠ 0 → s.gcdB 0 = 0
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.single_apply : ∀ {α : Type u_1} {β : Type u_2} (a : α) (b : β) (a_1 : α), ↑(PartialEquiv.single a b) a_1 = Function.const α b a_1
-- Mathlib.Algebra.GroupWithZero.Hom
MonoidWithZeroHom.one_apply_def : ∀ {M₀ : Type u_7} {N₀ : Type u_8} [inst : MulZeroOneClass M₀] [inst_1 : MulZeroOneClass N₀]
  [inst_2 : DecidablePred fun x => x = 0] [inst_3 : Nontrivial M₀] [inst_4 : NoZeroDivisors M₀] (x : M₀),
  1 x = if x = 0 then 0 else 1
-- Mathlib.Algebra.Algebra.Basic
Algebra.charZero_of_charZero : ∀ (R : Type u_1) (A : Type u_2) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] [FaithfulSMul R A]
  [CharZero R], CharZero A
-- Mathlib.RingTheory.MvPolynomial.Homogeneous
/-- The homogeneous submodules form a graded ring.
This instance is used by `DirectSum.commSemiring` and `DirectSum.algebra`.  -/
MvPolynomial.HomogeneousSubmodule.gradedMonoid : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R], SetLike.GradedMonoid (MvPolynomial.homogeneousSubmodule σ R)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.compare_maxKey?_modify_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [inst : Std.TransCmp cmp] (h : t.WF)
  {k : α} {f : β → β} {km kmm : α} (hkm : t.maxKey? = some km),
  (t.modify k f).maxKey?.get ⋯ = kmm → cmp kmm km = Ordering.eq
-- Mathlib.Topology.CantorBendixson
/-- The transfinite iteration of the relative derived-set operator on a set.  -/
CantorBendixson.«term_ᵈ[_]» : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.uliftYoneda_map_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) (X_1 : Cᵒᵖ),
  (CategoryTheory.uliftYoneda.{w, v₁, u₁}.map f).app X_1 =
    TypeCat.ofHom fun x => { down := CategoryTheory.CategoryStruct.comp x.down f }
-- Init.Data.Range.Polymorphic.Internal.SignedBitVec
_private.Init.Data.Range.Polymorphic.Internal.SignedBitVec.0.BitVec.Signed.ofNat_eq_rotate_ofInt_sub : ∀ {n k : ℕ}, BitVec.ofNat n k = BitVec.Signed.rotate✝ (BitVec.ofInt n (↑k - ↑(BitVec.Signed.intMinSealed✝ n).toNat))
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.Array.erase.match_1.eq_2 : ∀ {α : Type u_1} (as : Array α) (motive : Option (Fin as.size) → Sort u_2) (i : Fin as.size) (h_1 : Unit → motive none)
  (h_2 : (i : Fin as.size) → motive (some i)),
  (match some i with
    | none => h_1 ()
    | some i => h_2 i) =
    h_2 i
-- Aesop.RuleSet.Member
Aesop.GlobalRuleSetMember.name : Aesop.GlobalRuleSetMember → Aesop.RuleName
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getKey_alter : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  [Inhabited α] {k k' : α} {f : Option β → Option β} {hc : k' ∈ Std.DTreeMap.Const.alter t k f},
  (Std.DTreeMap.Const.alter t k f).getKey k' hc = if heq : cmp k k' = Ordering.eq then k else t.getKey k' ⋯
-- Mathlib.AlgebraicGeometry.Sites.AffineEtale
AlgebraicGeometry.Scheme.isGrothendieckAbelian_sheaf_smallEtaleTopology : ∀ (S : AlgebraicGeometry.Scheme) (A : Type u') [inst : CategoryTheory.Category.{u, u'} A] {FA : A → A → Type u_1}
  {CD : A → Type u} [inst_1 : (X Y : A) → FunLike (FA X Y) (CD X) (CD Y)]
  [inst_2 : CategoryTheory.ConcreteCategory A FA]
  [inst_3 : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget A)]
  [inst_4 : CategoryTheory.Limits.HasColimits A] [inst_5 : CategoryTheory.Limits.HasLimits A]
  [inst_6 : (CategoryTheory.forget A).ReflectsIsomorphisms]
  [inst_7 : CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{u, u, u, u, u', u + 1} (CategoryTheory.forget A)]
  [inst_8 : CategoryTheory.Abelian A] [CategoryTheory.IsGrothendieckAbelian.{u, u, u'} A],
  CategoryTheory.IsGrothendieckAbelian.{u, u + 1, max (max u' (u + 1)) u} (CategoryTheory.Sheaf S.smallEtaleTopology A)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_roc_append_toList_roc : ∀ {l m n : ℕ}, l ≤ m → m ≤ n → (l<...=m).toList ++ (m<...=n).toList = (l<...=n).toList
-- Mathlib.Analysis.InnerProductSpace.Projection.Reflection
/-- Reflection in a complete subspace of an inner product space.  The word "reflection" is
sometimes understood to mean specifically reflection in a codimension-one subspace, and sometimes
more generally to cover operations such as reflection in a point.  The definition here, of
reflection in a subspace, is a more general sense of the word that includes both those common
cases.  -/
Submodule.reflection : {𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : RCLike 𝕜] →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : InnerProductSpace 𝕜 E] → (K : Submodule 𝕜 E) → [K.HasOrthogonalProjection] → E ≃ₗᵢ[𝕜] E
-- Mathlib.Algebra.Homology.Opposite
HomologicalComplex.fromOpcycles_op_cyclesOpIso_inv : ∀ {ι : Type u_1} {V : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} V] {c : ComplexShape ι}
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] (K : HomologicalComplex V c) (i : ι) [inst_2 : K.HasHomology i]
  (j : ι), CategoryTheory.CategoryStruct.comp (K.fromOpcycles i j).op (K.cyclesOpIso i).inv = K.op.toCycles j i
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKey?_erase!_eq_iff_not_compare_eq_maxKey? : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF →
    ∀ {k : α},
      (Std.DTreeMap.Internal.Impl.erase! k t).maxKey? = t.maxKey? ↔
        ∀ {km : α}, t.maxKey? = some km → ¬compare k km = Ordering.eq
-- Std.Data.TreeSet.AdditionalOperations
/-- Given a proof that such an element exists, retrieves the smallest element that is
greater than the given element.
 -/
Std.TreeSet.getGT : {α : Type u} →
  {cmp : α → α → Ordering} →
    [Std.TransCmp cmp] → (t : Std.TreeSet α cmp) → (k : α) → (∃ a ∈ t, cmp a k = Ordering.gt) → α
-- Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
UniformConvergenceCLM.smulCommClass : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3}
  (F : Type u_4) [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜₁ E] [inst_4 : TopologicalSpace E]
  [inst_5 : AddCommGroup F] [inst_6 : Module 𝕜₂ F] {S : Type u_6} {T : Type u_7} [inst_7 : TopologicalSpace F]
  [inst_8 : Monoid S] [inst_9 : DistribMulAction S F] [inst_10 : SMulCommClass 𝕜₂ S F]
  [inst_11 : ContinuousConstSMul S F] [inst_12 : Monoid T] [inst_13 : DistribMulAction T F]
  [inst_14 : SMulCommClass 𝕜₂ T F] [inst_15 : ContinuousConstSMul T F] [SMulCommClass S T F] (𝔖 : Set (Set E)),
  SMulCommClass S T (UniformConvergenceCLM σ F 𝔖)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_ric_eq_toList_rio_append : ∀ {n : ℕ}, (*...=n).toList = (*...n).toList ++ [n]
-- Mathlib.Algebra.Lie.Semisimple.Defs
LieAlgebra.HasCentralRadical.radical_eq_center : ∀ {R : Type u_1} {L : Type u_2} {inst : CommRing R} {inst_1 : LieRing L} {inst_2 : LieAlgebra R L}
  [self : LieAlgebra.HasCentralRadical R L], LieAlgebra.radical R L = LieAlgebra.center R L
-- Std.Internal.Parsec.Basic
/-- The result of parsing some string.
 -/
Std.Internal.Parsec.ParseResult : Type → Type → Type
-- Init.Data.Option.Monadic
Option.filterM_none : ∀ {m : Type → Type u_1} {α : Type} [inst : Applicative m] (p : α → m Bool), Option.filterM p none = pure none
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Tactic.ComputeAsymptotics.Seq.FriendlyOperationClass.comp : ∀ {α : Type u_1} {γ : Type u_3} {γ' : Type u_4} (F : γ → Stream'.Seq α → Stream'.Seq α) (g : γ' → γ)
  [h : Tactic.ComputeAsymptotics.Seq.FriendlyOperationClass F],
  Tactic.ComputeAsymptotics.Seq.FriendlyOperationClass fun c => F (g c)
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.homology_π_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasHomology],
  CategoryTheory.CategoryStruct.comp S.homologyπ S.homologyι = CategoryTheory.CategoryStruct.comp S.iCycles S.pOpcycles
-- Std.Data.DTreeMap.Raw.Basic
/-- Inserts multiple mappings into the tree map by iterating over the given collection and calling
`insert`. If the same key appears multiple times, the last occurrence takes precedence.

Note: this precedence behavior is true for `TreeMap`, `DTreeMap`, `TreeMap.Raw` and `DTreeMap.Raw`.
The `insertMany` function on `TreeSet` and `TreeSet.Raw` behaves differently: it will prefer the first
appearance.
 -/
Std.DTreeMap.Raw.insertMany : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} →
      {ρ : Type u_1} → [ForIn Id ρ ((a : α) × β a)] → Std.DTreeMap.Raw α β cmp → ρ → Std.DTreeMap.Raw α β cmp
-- Mathlib.Computability.RegularExpressions
RegularExpression.rmatch.congr_simp : ∀ {α : Type u_1} {inst : DecidableEq α} [inst_1 : DecidableEq α] (a a_1 : RegularExpression α),
  a = a_1 → ∀ (a_2 a_3 : List α), a_2 = a_3 → a.rmatch a_2 = a_1.rmatch a_3
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.GrpObj.instIsIsoInv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (A : C) [inst_2 : CategoryTheory.GrpObj A], CategoryTheory.IsIso CategoryTheory.GrpObj.inv
-- Mathlib.FieldTheory.SeparableClosure
IntermediateField.finInsepDegree_bot : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E], Field.finInsepDegree F ↥⊥ = 1
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.IsLongestRevMatchAtChain.le : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice}
  {startPos endPos : s.Pos}, String.Slice.Pattern.Model.IsLongestRevMatchAtChain pat startPos endPos → startPos ≤ endPos
-- Mathlib.Order.Interval.Set.Monotone
AntitoneOn.Icc : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f g : α → β} {s : Set α},
  AntitoneOn f s → MonotoneOn g s → MonotoneOn (fun x => Set.Icc (f x) (g x)) s
-- Mathlib.Combinatorics.Quiver.SingleObj
Quiver.SingleObj.toPrefunctor_symm_apply : ∀ {α : Type u_1} {β : Type u_2} (f : Quiver.SingleObj α ⥤q Quiver.SingleObj β) (a : α),
  Quiver.SingleObj.toPrefunctor.symm f a = f.map (Quiver.SingleObj.toHom a)
-- Mathlib.Order.Max
noMinOrder_iff : ∀ {α : Type u_1} [inst : Preorder α], NoMinOrder α ↔ ∀ (x : α), ¬IsMin x
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.map_add_toArray_ric' : ∀ {n k : ℕ}, Array.map (fun x => k + x) (*...=n).toArray = (k...=k + n).toArray
-- Mathlib.Algebra.Category.Semigrp.Basic
AddSemigrp.coe_comp : ∀ {X Y Z : AddSemigrp} {f : X ⟶ Y} {g : Y ⟶ Z},
  ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) =
    ⇑(CategoryTheory.ConcreteCategory.hom g) ∘ ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.Algebra.GCDMonoid.Multiset
/-- Greatest common divisor of a multiset  -/
Multiset.gcd : {α : Type u_1} → [inst : CommMonoidWithZero α] → [NormalizedGCDMonoid α] → Multiset α → α
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.DiagnosticCode.string.sizeOf_spec : ∀ (s : String), sizeOf (Lean.Lsp.DiagnosticCode.string s) = 1 + sizeOf s
-- Mathlib.Algebra.Ring.Subring.MulOpposite
Subring.unop_toSubsemiring : ∀ {R : Type u_2} [inst : NonAssocRing R] (S : Subring Rᵐᵒᵖ), S.unop.toSubsemiring = S.unop
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.defnNat.sizeOf_spec : ∀ (h : Lean.Expr) (x : Int.Internal.Linear.Var) (e' : Int.Internal.Linear.Expr),
  sizeOf (Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.defnNat h x e') = 1 + sizeOf h + sizeOf x + sizeOf e'
-- Mathlib.CategoryTheory.Sites.CartesianClosed
instMonoidalClosedSheafOfHasSheafifyOfFunctorOpposite : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      (A : Type u_2) →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} A] →
          [CategoryTheory.HasSheafify J A] →
            [inst_3 : CategoryTheory.CartesianMonoidalCategory A] →
              [CategoryTheory.MonoidalClosed (CategoryTheory.Functor Cᵒᵖ A)] →
                CategoryTheory.MonoidalClosed (CategoryTheory.Sheaf J A)
-- Lean.Meta.PPGoal
Lean.Meta.ppGoal : Lean.MVarId → Lean.MetaM Std.Format
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.PUnit
FundamentalGroupoid.punitEquivDiscretePUnit_functor : FundamentalGroupoid.punitEquivDiscretePUnit.functor = CategoryTheory.Functor.star (FundamentalGroupoid PUnit.{u + 1})
-- Mathlib.CategoryTheory.Monoidal.Preadditive
CategoryTheory.MonoidalPreadditive.zero_whiskerRight : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {inst_1 : CategoryTheory.Preadditive C}
  {inst_2 : CategoryTheory.MonoidalCategory C} [self : CategoryTheory.MonoidalPreadditive C] {X Y Z : C},
  CategoryTheory.MonoidalCategoryStruct.whiskerRight 0 X = 0
-- Mathlib.RingTheory.Extension.Cotangent.Basic
/-- The sequence `H¹(L_{S/R}) → P.Cotangent → P.CotangentSpace` is exact.  -/
Algebra.Extension.exact_hCotangentι_cotangentComplex : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {P : Algebra.Extension R S}, Function.Exact ⇑Algebra.Extension.h1Cotangentι ⇑P.cotangentComplex
-- Mathlib.Analysis.SpecialFunctions.Arsinh
Filter.Tendsto.arsinh : ∀ {α : Type u_1} {l : Filter α} {f : α → ℝ} {a : ℝ},
  Filter.Tendsto f l (nhds a) → Filter.Tendsto (fun x => Real.arsinh (f x)) l (nhds (Real.arsinh a))
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Udiv
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Udiv.0.Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.eq_1 : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (lhs rhs : aig.RefVec w),
  Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv aig { lhs := lhs, rhs := rhs } =
    Std.Sat.AIG.RefVec.ite
      (Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.go
          (Std.Tactic.BVDecide.BVPred.mkEq aig
              { lhs := rhs, rhs := Std.Tactic.BVDecide.BVExpr.bitblast.blastConst aig 0#w }).aig
          w (lhs.cast ⋯) (rhs.cast ⋯) w 0 ((Std.Tactic.BVDecide.BVExpr.bitblast.blastConst aig 0#w).cast ⋯)
          ((Std.Tactic.BVDecide.BVExpr.bitblast.blastConst aig 0#w).cast ⋯)).aig
      {
        discr :=
          (Std.Tactic.BVDecide.BVPred.mkEq aig
                  { lhs := rhs, rhs := Std.Tactic.BVDecide.BVExpr.bitblast.blastConst aig 0#w }).ref.cast
            ⋯,
        lhs := ((Std.Tactic.BVDecide.BVExpr.bitblast.blastConst aig 0#w).cast ⋯).cast ⋯,
        rhs :=
          (Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.go
              (Std.Tactic.BVDecide.BVPred.mkEq aig
                  { lhs := rhs, rhs := Std.Tactic.BVDecide.BVExpr.bitblast.blastConst aig 0#w }).aig
              w (lhs.cast ⋯) (rhs.cast ⋯) w 0 ((Std.Tactic.BVDecide.BVExpr.bitblast.blastConst aig 0#w).cast ⋯)
              ((Std.Tactic.BVDecide.BVExpr.bitblast.blastConst aig 0#w).cast ⋯)).q }
-- Mathlib.Probability.Process.HittingTime
/-- `hittingAfter` is nonincreasing with respect to the set.  -/
MeasureTheory.hittingAfter_anti : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : ConditionallyCompleteLinearOrder ι] (u : ι → Ω → β) (n : ι),
  Antitone fun x => MeasureTheory.hittingAfter u x n
-- Mathlib.Order.ScottContinuity
ScottContinuousOn.prodMk : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  {D : Set (Set α)} {f : α → β} {g : α → γ},
  (∀ (a b : α), a ≤ b → {a, b} ∈ D) →
    ScottContinuousOn D f → ScottContinuousOn D g → ScottContinuousOn D fun x => (f x, g x)
-- Mathlib.Order.Filter.Pi
Filter.coprodᵢ_bot' : ∀ {ι : Type u_1} {α : ι → Type u_2}, Filter.coprodᵢ ⊥ = ⊥
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.equivWithVal_apply : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] [inst_1 : Ring R] {Γ'₀ : Type u_3}
  [inst_2 : LinearOrderedCommGroupWithZero Γ'₀] (v : Valuation R Γ₀) (w : Valuation R Γ'₀) {x : WithVal v},
  (WithVal.congr v w (RingEquiv.refl R)) x = (WithVal.equiv w).symm ((WithVal.equiv v) x)
-- Mathlib.Algebra.Category.MonCat.Basic
AddMonCat.instCoeSortType.eq_1 : AddMonCat.instCoeSortType = { coe := AddMonCat.carrier }
-- Mathlib.Algebra.Group.Finsupp
Finsupp.update_eq_add_single : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddZeroClass M] {f : ι →₀ M} {a : ι},
  f a = 0 → ∀ (b : M), f.update a b = f + fun₀ | a => b
-- Mathlib.Control.Monad.Cont
OptionT.mkLabel : {m : Type u → Type v} → [Monad m] → {α β : Type u} → MonadCont.Label (Option α) m β → MonadCont.Label α (OptionT m) β