mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Pred
Std.Tactic.BVDecide.Return.mk.injEq : ∀ {aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit} (result : aig.ExtendingEntrypoint)
  (cache : Std.Tactic.BVDecide.BVExpr.Cache (↑result).aig) (result_1 : aig.ExtendingEntrypoint)
  (cache_1 : Std.Tactic.BVDecide.BVExpr.Cache (↑result_1).aig),
  ({ result := result, cache := cache } = { result := result_1, cache := cache_1 }) =
    (result = result_1 ∧ cache ≍ cache_1)
-- Mathlib.AlgebraicGeometry.Sites.ElladicCohomology
/-- `ℓ`-adic cohomology of a scheme in degree `n`.  -/
AlgebraicGeometry.Scheme.EllAdicCohomology : AlgebraicGeometry.Scheme → (ℓ : ℕ) → [Fact (Nat.Prime ℓ)] → ℕ → Type (u + 1)
-- Mathlib.Algebra.Category.AlgCat.Basic
AlgCat.Hom.ext : ∀ {R : Type u} {inst : CommRing R} {A B : AlgCat R} {x y : A.Hom B}, x.hom' = y.hom' → x = y
-- Init.Data.BitVec.Lemmas
BitVec.twoPow_eq : ∀ (w i : ℕ), BitVec.twoPow w i = 1#w <<< i
-- Init.Data.List.MinMax
List.isSome_min?_iff : ∀ {α : Type u_1} [inst : Min α] {xs : List α}, xs.min?.isSome = true ↔ xs ≠ []
-- Std.Data.DTreeMap.Raw.Basic
Std.DTreeMap.Raw.instSDiff : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → SDiff (Std.DTreeMap.Raw α β cmp)
-- Mathlib.Topology.QuasiSeparated
IsQuasiSeparated.of_subset : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s t : Set α}, IsQuasiSeparated t → s ⊆ t → IsQuasiSeparated s
-- Lean.Meta.Tactic.NormCast
/-- squash lemma: LHS has ≥ 1 head coes and 0 internal coes, RHS has fewer head coes  -/
Lean.Meta.NormCast.Label.squash : Lean.Meta.NormCast.Label
-- Init.Data.BitVec.Lemmas
BitVec.toFin_udiv : ∀ {n : ℕ} {x y : BitVec n}, (x / y).toFin = x.toFin / y.toFin
-- Std.Data.DHashMap.Internal.Raw
_private.Std.Data.DHashMap.Internal.Raw.0.Std.DHashMap.Raw.getKeyD.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Raw α β) (a fallback : α),
  m.getKeyD a fallback =
    if h : 0 < m.buckets.size then Std.DHashMap.Internal.Raw₀.getKeyD ⟨m, h⟩ a fallback else fallback
-- Mathlib.Data.List.Nodup
List.nodup_append_comm : ∀ {α : Type u} {l₁ l₂ : List α}, (l₁ ++ l₂).Nodup ↔ (l₂ ++ l₁).Nodup
-- Mathlib.Logic.Function.Basic
/-- If `f : α → α → β` is surjective, then every endofunction on `β` has a fixed point.
This is an instance of Lawvere's fixed-point theorem applied to the category of types
and functions. It is the diagonal argument underlying `cantor_surjective` and
`cantor_injective`.  -/
Function.exists_fixed_point_of_surjective : ∀ {α : Type u_4} {β : Type u_5} (f : α → α → β), Function.Surjective f → ∀ (g : β → β), ∃ x, g x = x
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
MeasureTheory.SignedMeasure.toJordanDecomposition_spec : ∀ {α : Type u_1} [inst : MeasurableSpace α] (s : MeasureTheory.SignedMeasure α),
  ∃ i,
    ∃ (hi₁ : MeasurableSet i) (hi₂ :
      MeasureTheory.VectorMeasure.restrict 0 i ≤ MeasureTheory.VectorMeasure.restrict s i) (hi₃ :
      MeasureTheory.VectorMeasure.restrict s iᶜ ≤ MeasureTheory.VectorMeasure.restrict 0 iᶜ),
      s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂ ∧
        s.toJordanDecomposition.negPart = s.toMeasureOfLEZero iᶜ ⋯ hi₃
-- Mathlib.Analysis.SpecialFunctions.NonIntegrable
/-- **Alias** of `not_integrableOn_Ioi_inv`.

---

The function `fun x ↦ x⁻¹` is not integrable on any interval `(a, +∞)`.  -/
not_IntegrableOn_Ioi_inv : ∀ {a : ℝ}, ¬MeasureTheory.IntegrableOn (fun x => x⁻¹) (Set.Ioi a) MeasureTheory.volume
-- Mathlib.CategoryTheory.Limits.Types.ColimitType
CategoryTheory.Functor.CoconeTypes.IsColimit.mk : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {F : CategoryTheory.Functor J (Type w₀)} {c : F.CoconeTypes},
  Function.Bijective (F.descColimitType c) → c.IsColimit
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.WidePullback.lift_π : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {B : C} {objs : J → C}
  (arrows : (j : J) → objs j ⟶ B) [inst_1 : CategoryTheory.Limits.HasWidePullback B objs arrows] {X : C} (f : X ⟶ B)
  (fs : (j : J) → X ⟶ objs j) (w : ∀ (j : J), CategoryTheory.CategoryStruct.comp (fs j) (arrows j) = f) (j : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePullback.lift f fs w)
      (CategoryTheory.Limits.WidePullback.π arrows j) =
    fs j
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.coe_sInf : ∀ {G : Type u_1} [inst : AddGroup G] (H : Set (AddSubgroup G)), ↑(sInf H) = ⋂ s ∈ H, ↑s
-- Mathlib.Data.Int.Cast.Basic
Int.cast_four : ∀ {R : Type u} [inst : AddGroupWithOne R], ↑4 = 4
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.ofCLM_intCast : ∀ {𝕜₂ : Type u_2} [inst : NormedField 𝕜₂] {F : Type u_4} [inst_1 : AddCommGroup F] [inst_2 : TopologicalSpace F]
  [inst_3 : Module 𝕜₂ F] [inst_4 : IsTopologicalAddGroup F] (n : ℤ), ContinuousLinearMapWOT.ofCLM ↑n = ↑n
-- Lean.Data.Options
Lean.Option.mk.injEq : ∀ {α : Type} (name : Lean.Name) (defValue : α) (name_1 : Lean.Name) (defValue_1 : α),
  ({ name := name, defValue := defValue } = { name := name_1, defValue := defValue_1 }) =
    (name = name_1 ∧ defValue = defValue_1)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
CategoryTheory.Limits.ChosenPullback.LiftStruct.f_p : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S}
  {h : CategoryTheory.Limits.ChosenPullback f₁ f₂} {Y : C} {g₁ : Y ⟶ X₁} {g₂ : Y ⟶ X₂} {b : Y ⟶ S}
  (self : h.LiftStruct g₁ g₂ b), CategoryTheory.CategoryStruct.comp self.f h.p = b
-- Mathlib.LinearAlgebra.Matrix.Stochastic
/-- Right multiplication of a row stochastic matrix by a non-negative vector
gives a non-negative vector  -/
Matrix.nonneg_mulVec_of_mem_rowStochastic : ∀ {R : Type u_1} {n : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Semiring R]
  [inst_3 : PartialOrder R] [inst_4 : IsOrderedRing R] {M : Matrix n n R} {x : n → R},
  M ∈ Matrix.rowStochastic R n → (∀ (i : n), 0 ≤ x i) → ∀ (j : n), 0 ≤ M.mulVec x j
-- Mathlib.Data.Part
Part.get_some : ∀ {α : Type u_1} {a : α} (ha : (Part.some a).Dom), (Part.some a).get ha = a
-- Mathlib.Data.Ordmap.Invariants
_private.Mathlib.Data.Ordmap.Invariants.0.Ordnode.mem.match_1.eq_1 : ∀ (motive : Ordering → Sort u_1) (h_1 : Unit → motive Ordering.lt) (h_2 : Unit → motive Ordering.eq)
  (h_3 : Unit → motive Ordering.gt),
  (match Ordering.lt with
    | Ordering.lt => h_1 ()
    | Ordering.eq => h_2 ()
    | Ordering.gt => h_3 ()) =
    h_1 ()
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
/-- The submonoid of elements `x : R` whose valuation is positive.  -/
ValuativeRel.posSubmonoid : (R : Type u_1) → [inst : Semiring R] → [ValuativeRel R] → Submonoid R
-- Lean.Meta.Tactic.Simp.Simproc
Lean.Meta.Simp.registerSimprocAttr : Lean.Name →
  String →
    Option (IO.Ref Lean.Meta.Simprocs) →
      autoParam Lean.Name Lean.Meta.Simp.registerSimprocAttr._auto_1 → IO Lean.Meta.Simp.SimprocExtension
-- Mathlib.Probability.Process.Stopping
MeasureTheory.IsStoppingTime.measurableSet_min_const_iff : ∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : LinearOrder ι] {f : MeasureTheory.Filtration ι m}
  {τ : Ω → WithTop ι} (hτ : MeasureTheory.IsStoppingTime f τ) (s : Set Ω) {i : ι},
  MeasurableSet s ↔ MeasurableSet s ∧ MeasurableSet s
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.instAdd : {R : Type u_1} →
  {V : Type u_2} →
    {W : Type u_3} →
      {P : Type u_4} →
        [inst : Ring R] →
          [inst_1 : AddCommGroup V] →
            [inst_2 : Module R V] →
              [inst_3 : TopologicalSpace P] →
                [inst_4 : AddTorsor V P] →
                  [inst_5 : AddCommGroup W] →
                    [inst_6 : Module R W] → [inst_7 : TopologicalSpace W] → [IsTopologicalAddGroup W] → Add (P →ᴬ[R] W)
-- Mathlib.CategoryTheory.DinatTrans
/-- Post-composition with a natural transformation.  -/
CategoryTheory.DinatTrans.compNatTrans : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F G H : CategoryTheory.Functor Cᵒᵖ (CategoryTheory.Functor C D)} →
          CategoryTheory.DinatTrans F G → (G ⟶ H) → CategoryTheory.DinatTrans F H
-- Mathlib.SetTheory.Cardinal.NatCard
Finite.card_eq_zero_iff : ∀ {α : Type u_1} [Finite α], Nat.card α = 0 ↔ IsEmpty α
-- Mathlib.CategoryTheory.Limits.WeakLimits.WeakPullbacks
CategoryTheory.Limits.weakLimit.pullbackConeSnd_cone_cospan : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst_1 : CategoryTheory.Limits.HasWeakLimit (CategoryTheory.Limits.cospan f g)],
  CategoryTheory.Limits.PullbackCone.snd (CategoryTheory.Limits.weakLimit.cone (CategoryTheory.Limits.cospan f g)) =
    CategoryTheory.Limits.weakPullback.snd f g
-- Mathlib.CategoryTheory.MorphismProperty.Limits
/-- A morphism property is `IsStableUnderBaseChange` if the base change of such a morphism
still falls in the class.  -/
CategoryTheory.MorphismProperty.IsStableUnderBaseChange : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.MorphismProperty C → Prop
-- Mathlib.MeasureTheory.Function.ConvergenceInMeasure
/-- `TendstoInMeasure` is equivalent to every subsequence having another subsequence
which converges almost surely.  -/
MeasureTheory.exists_seq_tendstoInMeasure_atTop_iff : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : PseudoEMetricSpace E]
  [MeasureTheory.IsFiniteMeasure μ] {f : ℕ → α → E},
  (∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (f n) μ) →
    ∀ {g : α → E},
      MeasureTheory.TendstoInMeasure μ f Filter.atTop g ↔
        ∀ (ns : ℕ → ℕ),
          StrictMono ns →
            ∃ ns', StrictMono ns' ∧ ∀ᵐ (ω : α) ∂μ, Filter.Tendsto (fun i => f (ns (ns' i)) ω) Filter.atTop (nhds (g ω))
-- Mathlib.NumberTheory.EulerProduct.DirichletLSeries
/-- A variant of the Euler product for the L-series of `ζ`.  -/
ArithmeticFunction.LSeries_zeta_eulerProduct_exp_log : ∀ {s : ℂ}, 1 < s.re → Complex.exp (∑' (p : Nat.Primes), -Complex.log (1 - ↑↑p ^ (-s))) = LSeries 1 s
-- Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
HomotopicalAlgebra.PathObject.IsVeryGood.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C}
  [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C] (P P_1 : HomotopicalAlgebra.PathObject A),
  P = P_1 →
    ∀ [inst_2 : CategoryTheory.Limits.HasBinaryProduct A A] [inst_3 : HomotopicalAlgebra.CategoryWithFibrations C]
      [inst_4 : HomotopicalAlgebra.CategoryWithCofibrations C], P.IsVeryGood = P_1.IsVeryGood
-- Aesop.Rule
Aesop.UnfoldRule.instBEq : BEq Aesop.UnfoldRule
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
_private.Std.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap.0.Std.IterM.stepAsHetT_filterMapWithPostcondition.match_1.eq_2 : ∀ {γ : Type u_1} (motive : Option γ → Sort u_2) (h_1 : (out' : γ) → motive (some out')) (h_2 : Unit → motive none),
  (match none with
    | some out' => h_1 out'
    | none => h_2 ()) =
    h_2 ()
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.getEntryLTD_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t₁.WF →
    t₂.WF →
      t₁.Equiv t₂ →
        ∀ {k : α} {fallback : (a : α) × β a},
          Std.DTreeMap.Internal.Impl.getEntryLTD k t₁ fallback = Std.DTreeMap.Internal.Impl.getEntryLTD k t₂ fallback
-- Mathlib.Tactic.CategoryTheory.Elementwise
/-- Gives a name based on `baseName` that's not already in the list.  -/
_private.Mathlib.Tactic.CategoryTheory.Elementwise.0.Mathlib.Tactic.Elementwise.mkUnusedName : List Lean.Name → Lean.Name → Lean.Name
-- Mathlib.Data.List.ToFinsupp
List.toFinsupp_apply_fin : ∀ {M : Type u_1} [inst : Zero M] (l : List M) [inst_1 : DecidablePred fun x => l.getD x 0 ≠ 0] (n : Fin l.length),
  l.toFinsupp ↑n = l[n]
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get?_eq_some_get : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {a : α} (h' : a ∈ t),
  t.get? a = some (t.get a h')
-- Mathlib.FieldTheory.IntermediateField.Basic
/-- The embedding from an intermediate field of `L / K` to `L`.  -/
IntermediateField.val : {K : Type u_1} →
  {L : Type u_2} →
    [inst : Field K] → [inst_1 : Field L] → [inst_2 : Algebra K L] → (S : IntermediateField K L) → ↥S →ₐ[K] L
-- Mathlib.Order.GaloisConnection.Basic
/-- **Alias** of `giSSupIic`.

---

`sSup` and `Iic` form a Galois insertion.  -/
gi_sSup_Iic : {α : Type u} → [inst : CompleteSemilatticeSup α] → GaloisInsertion sSup Set.Iic
-- Mathlib.RingTheory.Localization.Away.Basic
/-- The localization away from a unit is isomorphic to the ring.  -/
IsLocalization.atUnit : (R : Type u_1) →
  [inst : CommSemiring R] →
    (S : Type u_2) →
      [inst_1 : CommSemiring S] → [inst_2 : Algebra R S] → (x : R) → IsUnit x → [IsLocalization.Away x S] → R ≃ₐ[R] S
-- Aesop.RuleSet.Name
Aesop.defaultRuleSetName : Aesop.RuleSetName
-- Mathlib.Topology.LocallyConstant.Basic
IsLocallyConstant.exists_open : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] {f : X → Y},
  IsLocallyConstant f → ∀ (x : X), ∃ U, IsOpen U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x
-- Mathlib.Algebra.Module.Projective
Module.instProjectiveShrink : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_3} [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Small.{w, u_3} M] [Module.Projective R M], Module.Projective R (Shrink.{w, u_3} M)
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
instConcreteCategoryProfiniteGrpContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfinite : CategoryTheory.ConcreteCategory ProfiniteGrp.{u_1} fun X Y => ↑X.toProfinite.toTop →ₜ* ↑Y.toProfinite.toTop
-- Lean.Server.Completion.CompletionItemCompression
_private.Lean.Server.Completion.CompletionItemCompression.0.Lean.Lsp.ResolvableCompletionList.compressCompletionTagsFast.eq_def : ∀ (acc : String) (tags : Array Lean.Lsp.CompletionItemTag) (i : ℕ),
  Lean.Lsp.ResolvableCompletionList.compressCompletionTagsFast✝ acc tags i =
    if h : i < tags.size then
      have acc := acc ++ (tags[i].ctorIdx + 1).repr;
      have acc := if i < tags.size - 1 then acc ++ "," else acc;
      Lean.Lsp.ResolvableCompletionList.compressCompletionTagsFast✝ acc tags (i + 1)
    else acc
-- Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_map_mkHom_id_homMk : ∀ {X Y : SSet.Truncated 2}
  (x : X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge.tensor._proof_1 }))
  {y₀ y₁ : Y.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge.tensor._proof_1 })}
  (e : SSet.Truncated.Edge y₀ y₁),
  (SSet.Truncated.HomotopyCategory.BinaryProduct.inverse X Y).map
      (CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id (SSet.Truncated.HomotopyCategory.mk x))
        (SSet.Truncated.HomotopyCategory.homMk e)) =
    SSet.Truncated.HomotopyCategory.homMk ((SSet.Truncated.Edge.id x).tensor e)
-- Mathlib.Data.Set.Image
Set.InjOn.image_nontrivial_iff : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β}, Set.InjOn f s → ((f '' s).Nontrivial ↔ s.Nontrivial)
-- Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction
/-- For `1 ≤ r`, the characteristic function of a sum `∑ a, f a` at `⊤` is less than or equal to the sum
of the characteristic functions of `f ·`, plus `log s.card`.
 -/
ValueDistribution.characteristic_sum_top_le : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {α : Type u_2} (s : Finset α) (f : α → ℂ → E)
  {r : ℝ},
  (∀ a ∈ s, Meromorphic (f a)) →
    1 ≤ r →
      ValueDistribution.characteristic (∑ a ∈ s, f a) ⊤ r ≤
        (∑ a ∈ s, ValueDistribution.characteristic (f a) ⊤) r + Real.log ↑s.card
-- Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
CliffordAlgebra.contractLeft_ι : ∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q : QuadraticForm R M) (d : Module.Dual R M) (x : M),
  (CliffordAlgebra.contractLeft d) ((CliffordAlgebra.ι Q) x) = (algebraMap R (CliffordAlgebra Q)) (d x)
-- Mathlib.Analysis.Complex.Norm
Complex.norm_div : ∀ (z w : ℂ), ‖z / w‖ = ‖z‖ / ‖w‖
-- Mathlib.CategoryTheory.MorphismProperty.Retract
CategoryTheory.MorphismProperty.retracts_le : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C)
  [P.IsStableUnderRetracts], P.retracts ≤ P
-- Mathlib.MeasureTheory.Integral.IntervalAverage
interval_average_symm : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (f : ℝ → E) (a b : ℝ),
  ⨍ (x : ℝ) in a..b, f x = ⨍ (x : ℝ) in b..a, f x
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.not_lt_norm' : ∀ {α : Type u_1} [inst : Lean.Grind.IntModule α] [inst_1 : LE α] [inst_2 : LT α] [Std.LawfulOrderLT α]
  [inst_4 : Std.IsPreorder α] [Lean.Grind.OrderedAdd α] (ctx : Lean.Grind.Linarith.Context α)
  (lhs rhs : Lean.Grind.Linarith.Expr) (p : Lean.Grind.Linarith.Poly),
  Lean.Grind.Linarith.norm_cert lhs rhs p = true →
    ¬Lean.Grind.Linarith.Expr.denote ctx lhs < Lean.Grind.Linarith.Expr.denote ctx rhs →
      ¬Lean.Grind.Linarith.Poly.denote' ctx p < 0
-- Mathlib.AlgebraicGeometry.Sites.Small
/-- The pretopology defined on the subcategory of `S`-schemes satisfying `Q` where coverings
are given by `P`-coverings in `S`-schemes satisfying `Q`.
The most common case is `P = Q`. In this case, this is simply surjective families
in `S`-schemes with `P`.  -/
AlgebraicGeometry.Scheme.smallPretopology : (P Q : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) →
  {S : AlgebraicGeometry.Scheme} →
    [P.IsStableUnderBaseChange] →
      [P.IsMultiplicative] →
        [P.RespectsIso] →
          [inst : Q.IsStableUnderComposition] →
            [inst_1 : Q.IsStableUnderBaseChange] →
              [inst_2 : Q.HasOfPostcompProperty Q] → CategoryTheory.Pretopology (Q.Over ⊤ S)
-- Lean.Parser.StrInterpolation
Lean.Parser.isQuotableCharForStrInterpolant : Char → Bool
-- Lean.Server.Completion.EligibleHeaderDecls
Lean.Server.Completion.EligibleDecl.kind : Lean.Server.Completion.EligibleDecl → Lean.MetaM Lean.Lsp.CompletionItemKind
-- Mathlib.Probability.Kernel.Condexp
MeasureTheory.AEStronglyMeasurable.comp_snd_map_prod_id : ∀ {Ω : Type u_1} {F : Type u_2} {m mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {f : Ω → F}
  [inst : TopologicalSpace F],
  MeasureTheory.AEStronglyMeasurable f μ →
    MeasureTheory.AEStronglyMeasurable (fun x => f x.2) (MeasureTheory.Measure.map Function.diag μ)
-- Init.Data.List.Basic
/-- Creates a list that contains `n` copies of `a`.

This is a tail-recursive version of `List.replicate`.

* `List.replicateTR 5 "five" = ["five", "five", "five", "five", "five"]`
* `List.replicateTR 0 "zero" = []`
* `List.replicateTR 2 ' ' = [' ', ' ']`
 -/
List.replicateTR : {α : Type u} → ℕ → α → List α
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.Context.reportMVarIssue : Lean.Meta.Grind.Context → Bool
-- Mathlib.Data.FinEnum
FinEnum.sum : {α : Type u} → {β : Type u_1} → [FinEnum α] → [FinEnum β] → FinEnum (α ⊕ β)
-- Mathlib.Combinatorics.Matroid.Dual
Matroid.Coindep.eq_1 : ∀ {α : Type u_1} (M : Matroid α) (I : Set α), M.Coindep I = M✶.Indep I
-- Mathlib.Topology.Algebra.Algebra.Equiv
ContinuousAlgEquiv.self_comp_symm : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : TopologicalSpace A] [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A]
  [inst_6 : Algebra R B] (e : A ≃A[R] B), ⇑e ∘ ⇑e.symm = id
-- Mathlib.Data.Set.Function
Set.eqOn_empty : ∀ {α : Type u_1} {β : Type u_2} (f₁ f₂ : α → β), Set.EqOn f₁ f₂ ∅
-- Init.Data.List.Attach
_private.Init.Data.List.Attach.0.List.pmap.match_1.splitter : {α : Type u_1} →
  {P : α → Prop} →
    (motive : (x : List α) → (∀ a ∈ x, P a) → Sort u_2) →
      (x : List α) →
        (x_1 : ∀ a ∈ x, P a) →
          ((x : ∀ a ∈ [], P a) → motive [] x) →
            ((a : α) → (l : List α) → (H : ∀ a_1 ∈ a :: l, P a_1) → motive (a :: l) H) → motive x x_1
-- Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
/-- Explicit formula for `toCircle j`. Note that this is "evil" because it uses `ZMod.val`. Where
possible, it is recommended to lift `j` to `ℤ` and use `toCircle_intCast` instead.
 -/
ZMod.toCircle_apply : ∀ {N : ℕ} [inst : NeZero N] (j : ZMod N), ↑(ZMod.toCircle j) = Complex.exp (2 * ↑Real.pi * Complex.I * ↑j.val / ↑N)
-- Mathlib.Algebra.Order.Monoid.Canonical.Defs
lt_iff_exists_add : ∀ {α : Type u} [inst : AddZeroClass α] [inst_1 : PartialOrder α] [CanonicallyOrderedAdd α] {a b : α}
  [AddLeftStrictMono α], a < b ↔ ∃ c > 0, b = a + c
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.notMem_support_iff_isIsolated : ∀ {V : Type u} (G : SimpleGraph V) {v : V}, v ∉ G.support ↔ G.IsIsolated v
-- Mathlib.Data.Set.Function
Set.imageFactorization_injective_iff : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β}, Function.Injective (Set.imageFactorization f s) ↔ Set.InjOn f s
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas
aestronglyMeasurable_smul_const_iff : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {𝕜 : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [CompleteSpace 𝕜] {E : Type u_5} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {f : α → 𝕜} {c : E},
  c ≠ 0 → (MeasureTheory.AEStronglyMeasurable (fun x => f x • c) μ ↔ MeasureTheory.AEStronglyMeasurable f μ)
-- Mathlib.Combinatorics.SimpleGraph.Trails
SimpleGraph.Walk.IsTrail.edgesFinset.congr_simp : ∀ {V : Type u_1} {G : SimpleGraph V} {u v : V} {p p_1 : G.Walk u v} (e_p : p = p_1) (h : p.IsTrail),
  h.edgesFinset = ⋯.edgesFinset
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.typein_le_typein' : ∀ (o : Ordinal.{u_1}) {x y : o.ToType},
  (Ordinal.typein fun x1 x2 => x1 < x2).toRelEmbedding x ≤ (Ordinal.typein fun x1 x2 => x1 < x2).toRelEmbedding y ↔
    x ≤ y
-- Mathlib.RingTheory.Ideal.Norm.RelNorm
Ideal.relNorm_relNorm : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDomain R] {S : Type u_3} [inst_2 : CommRing S] [inst_3 : IsDomain S]
  [inst_4 : IsIntegrallyClosed R] [inst_5 : IsIntegrallyClosed S] [inst_6 : Algebra R S] [inst_7 : Module.Finite R S]
  [inst_8 : Module.IsTorsionFree R S] [inst_9 : IsDedekindDomain R] [inst_10 : IsDedekindDomain S] (T : Type u_4)
  [inst_11 : CommRing T] [inst_12 : IsDedekindDomain T] [inst_13 : IsIntegrallyClosed T] [inst_14 : Algebra R T]
  [inst_15 : Algebra T S] [IsScalarTower R T S] [inst_17 : Module.Finite R T] [inst_18 : Module.Finite T S]
  [inst_19 : Module.IsTorsionFree R T] [inst_20 : Module.IsTorsionFree T S] (I : Ideal S),
  (Ideal.relNorm R) ((Ideal.relNorm T) I) = (Ideal.relNorm R) I
-- Mathlib.RingTheory.Ideal.Norm.RelNorm
Ideal.spanNorm_mono : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDomain R] {S : Type u_3} [inst_2 : CommRing S] [inst_3 : IsDomain S]
  [inst_4 : IsIntegrallyClosed R] [inst_5 : IsIntegrallyClosed S] [inst_6 : Algebra R S] [inst_7 : Module.Finite R S]
  [inst_8 : Module.IsTorsionFree R S] {I J : Ideal S}, I ≤ J → Ideal.spanNorm R I ≤ Ideal.spanNorm R J
-- Init.Data.BitVec.Basic
BitVec.instXorOp : {w : ℕ} → XorOp (BitVec w)
-- Init.Data.ByteArray.Basic
/-- Copies the bytes with indices `b` \(inclusive\) to `e` \(exclusive\) to a new
`ByteArray`.
 -/
ByteArray.extract : ByteArray → ℕ → ℕ → ByteArray
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
/-- A generalization of `HetT.map` that provides the postcondition property to the mapping function.
 -/
Std.Iterators.HetT.pmap : {m : Type w → Type w'} →
  [Functor m] →
    {α : Type u} → {β : Type v} → (x : Std.Iterators.HetT m α) → ((a : α) → x.Property a → β) → Std.Iterators.HetT m β
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.algebraMap_apply'' : ∀ {σ : Type u_1} {R : Type u_2} (A : Type u_3) [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Algebra R A]
  (f : MvPowerSeries σ R),
  (algebraMap (MvPowerSeries σ R) (MvPowerSeries σ A)) f = (MvPowerSeries.map (algebraMap R A)) f
-- Std.Data.TreeMap.Iterator
Std.TreeMap.toList_iter : ∀ {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} (m : Std.TreeMap α β cmp), m.iter.toList = m.toList
-- Lean.Meta.Tactic.Grind.Types
/-- Symbol priorities for inferring E-matching patterns  -/
Lean.Meta.Grind.Context.symPrios : Lean.Meta.Grind.Context → Lean.Meta.Grind.SymbolPriorities