mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Internal.Do.PredTrans
/-- A monotone predicate transformer from postconditions to preconditions.

Given a return type `α`, a lattice `Pred` for assertions, and an exception assertion type `EPred`,
`PredTrans Pred EPred α` wraps a function `(α → Pred) → EPred → Pred`.  -/
Std.Internal.Do.PredTrans : Type u → Type v → Type w → Type (max (max u v) w)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.Slice.skipSuffix?_prop_eq_some_iff : ∀ {P : Char → Prop} [inst : DecidablePred P] {s : String.Slice} {pos : s.Pos},
  s.skipSuffix? P = some pos ↔ ∃ (h : s.endPos ≠ s.startPos), pos = s.endPos.prev h ∧ P ((s.endPos.prev h).get ⋯)
-- Mathlib.RingTheory.Ideal.Maps
/-- `N.annihilator` is the ideal of all elements `r : R` such that `r • N = 0`.  -/
Submodule.annihilator : {R : Type u_1} →
  {M : Type u_2} → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → Submodule R M → Ideal R
-- Lean.Meta.Match.CaseArraySizes
Lean.Meta.instInhabitedCaseArraySizesSubgoal.default : Lean.Meta.CaseArraySizesSubgoal
-- Mathlib.Order.CompactlyGenerated.Basic
WellFoundedLT.finite_of_iSupIndep : ∀ {α : Type u_2} [inst : CompleteLattice α] [WellFoundedLT α] {ι : Type u_3} {t : ι → α},
  iSupIndep t → (∀ (i : ι), t i ≠ ⊥) → Finite ι
-- Std.Http.Data.Headers.Basic
/-- Parses an `Expect` header.

Succeeds only if the value is exactly `100-continue`
(case-insensitive, trimmed).
 -/
Std.Http.Header.Expect.parse : Std.Http.Header.Value → Option Std.Http.Header.Expect
-- Mathlib.Topology.Algebra.InfiniteSum.Constructions
summable_star_iff' : ∀ {α : Type u_1} {β : Type u_2} {L : SummationFilter β} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α]
  [inst_2 : StarAddMonoid α] [ContinuousStar α] {f : β → α}, Summable (star f) L ↔ Summable f L
-- Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct
CategoryTheory.Limits.SequentialProduct.functorObj_eq_neg : ∀ {C : Type u_1} {M N : ℕ → C} {n m : ℕ}, ¬m < n → (fun i => if x : i < n then M i else N i) m = N m
-- Mathlib.GroupTheory.GroupAction.FixedPoints
AddAction.vadd_mem_fixedBy_iff_mem_fixedBy : ∀ {α : Type u_1} {G : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] {a : α} {g : G},
  g +ᵥ a ∈ AddAction.fixedBy α g ↔ a ∈ AddAction.fixedBy α g
-- Lean.Meta.Tactic.Grind.Extension
/-- A constraint of the form `lhs =/= rhs`.
The `lhs` is one of the bound variables, and the `rhs` an abstract term that must not be definitionally
equal to a term `t` assigned to `lhs`.  -/
Lean.Meta.Grind.EMatchTheoremConstraint.notDefEq : ℕ → Lean.Meta.Grind.CnstrRHS → Lean.Meta.Grind.EMatchTheoremConstraint
-- Mathlib.Algebra.Lie.Weights.Basic
LieModule.Weight.mk : {R : Type u_2} →
  {L : Type u_3} →
    {M : Type u_4} →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : LieAlgebra R L] →
            [inst_3 : AddCommGroup M] →
              [inst_4 : Module R M] →
                [inst_5 : LieRingModule L M] →
                  [inst_6 : LieModule R L M] →
                    [inst_7 : LieRing.IsNilpotent L] →
                      (toFun : L → R) → LieModule.genWeightSpace M toFun ≠ ⊥ → LieModule.Weight R L M
-- Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
pinGroup.star_mul_self : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} (x : ↥(pinGroup Q)), star x * x = 1
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
IsCyclotomicExtension.Rat.p_mem_span_zeta_sub_one : ∀ (p k : ℕ) [hp : Fact (Nat.Prime p)] {K : Type u_1} [inst : Field K] [inst_1 : NumberField K]
  [hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K] {ζ : K} (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))),
  ↑p ∈ Ideal.span {hζ.toInteger - 1}
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.restrict_apply : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] (μ : MeasureTheory.FiniteMeasure Ω) (A : Set Ω) {s : Set Ω},
  MeasurableSet s → (μ.restrict A) s = μ (s ∩ A)
-- Mathlib.Topology.Connected.PathConnected
AddSubgroup.coe_pathComponentZero : ∀ (G : Type u_4) [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalAddGroup G],
  ↑(AddSubgroup.pathComponentZero G) = pathComponent 0
-- Mathlib.Analysis.Normed.Algebra.Spectrum
spectrum.spectralRadius_le_liminf_pow_nnnorm_pow_one_div : ∀ (𝕜 : Type u_1) {A : Type u_2} [inst : NormedField 𝕜] [inst_1 : NormedRing A] [inst_2 : NormedAlgebra 𝕜 A]
  [CompleteSpace A] (a : A), spectralRadius 𝕜 a ≤ Filter.liminf (fun n => ↑‖a ^ n‖₊ ^ (1 / ↑n)) Filter.atTop
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.negAt_apply_isComplex : ∀ {K : Type u_1} [inst : Field K] {s : Set { w // w.IsReal }} (x : NumberField.mixedEmbedding.mixedSpace K)
  (w : { w // w.IsComplex }), ((NumberField.mixedEmbedding.negAt s) x).2 w = x.2 w
-- Mathlib.Order.Hom.Lattice
/-- Natural projection homomorphism from `α × β` to `β`.  -/
LatticeHom.snd : {α : Type u_2} → {β : Type u_3} → [inst : Lattice α] → [inst_1 : Lattice β] → LatticeHom (α × β) β
-- Lean.Linter.MissingDocs
Lean.Linter.MissingDocs.mkHandler : Lean.Name → Lean.ImportM Lean.Linter.MissingDocs.Handler
-- Mathlib.Combinatorics.SimpleGraph.Sum
/-- Bijection between `(G ⊕g H).Coloring γ` and `G.Coloring γ × H.Coloring γ`  -/
SimpleGraph.Coloring.sumEquiv : {V : Type u_3} →
  {W : Type u_5} →
    {γ : Type u_7} → {G : SimpleGraph V} → {H : SimpleGraph W} → (G ⊕g H).Coloring γ ≃ G.Coloring γ × H.Coloring γ
-- Std.Net.Addr
Std.Net.AddressFamily.ipv4.sizeOf_spec : sizeOf Std.Net.AddressFamily.ipv4 = 1
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.toArray_filterMap : ∀ {α β γ : Type w} {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m] [inst_2 : Std.Iterator α m β]
  [Std.Iterators.Finite α m] {f : β → Option γ} (it : Std.IterM m β),
  (Std.IterM.filterMap f it).toArray = (fun x => Array.filterMap f x) <$> it.toArray
-- Lean.Data.Iterators.Producers.PersistentHashMap
_private.Lean.Data.Iterators.Producers.PersistentHashMap.0.Lean.PersistentHashMap.Node.measure.match_1.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (motive : Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β) → Sort u_3)
  (key : α) (val : β)
  (h_1 :
    Lean.PersistentHashMap.Entry.entry key val = Lean.PersistentHashMap.Entry.null →
      motive Lean.PersistentHashMap.Entry.null)
  (h_2 :
    (key_1 : α) →
      (val_1 : β) →
        Lean.PersistentHashMap.Entry.entry key val = Lean.PersistentHashMap.Entry.entry key_1 val_1 →
          motive (Lean.PersistentHashMap.Entry.entry key_1 val_1))
  (h_3 :
    (node : Lean.PersistentHashMap.Node α β) →
      Lean.PersistentHashMap.Entry.entry key val = Lean.PersistentHashMap.Entry.ref node →
        motive (Lean.PersistentHashMap.Entry.ref node)),
  (match h_eq : Lean.PersistentHashMap.Entry.entry key val with
    | Lean.PersistentHashMap.Entry.null => h_1 h_eq
    | Lean.PersistentHashMap.Entry.entry key_1 val_1 => h_2 key_1 val_1 h_eq
    | Lean.PersistentHashMap.Entry.ref node => h_3 node h_eq) =
    h_2 key val ⋯
-- Mathlib.LinearAlgebra.Projection
Submodule.projection_eq_id_sub_projection : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {p q : Submodule R E}
  (hpq : IsCompl p q), q.projection p ⋯ = LinearMap.id - p.projection q hpq
-- Mathlib.Order.Lattice.Nat
Nat.nonempty_of_pos_sInf : ∀ {s : Set ℕ}, 0 < sInf s → s.Nonempty
-- Mathlib.Data.Vector.Defs
/-- Vector of length `n` from a function on `Fin n`.  -/
List.Vector.ofFn : {α : Type u_1} → {n : ℕ} → (Fin n → α) → List.Vector α n
-- Mathlib.Order.BoundedOrder.Basic
Subtype.mk_eq_bot_iff : ∀ {α : Type u} {p : α → Prop} [inst : PartialOrder α] [inst_1 : OrderBot α] [inst_2 : OrderBot (Subtype p)],
  p ⊥ → ∀ {x : α} (hx : p x), ⟨x, hx⟩ = ⊥ ↔ x = ⊥
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Localization.mkHom_surjective : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M}, Function.Surjective ⇑Localization.mkHom
-- Mathlib.Geometry.RingedSpace.PresheafedSpace
AlgebraicGeometry.PresheafedSpace.restrict_presheaf : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {U : TopCat} (X : AlgebraicGeometry.PresheafedSpace C)
  {f : U ⟶ ↑X} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)),
  (X.restrict h).presheaf = h.functor.op.comp X.presheaf
-- Mathlib.RingTheory.Ideal.Cotangent
IsLocalRing.finrank_cotangentSpace_eq_zero_iff : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsLocalRing R] [IsNoetherianRing R],
  Module.finrank (IsLocalRing.ResidueField R) (IsLocalRing.CotangentSpace R) = 0 ↔ IsField R
-- Init.Data.String.Basic
String.Slice.Pos.offset_str_le_offset_endExclusive : ∀ {s : String.Slice} {pos : s.Pos}, pos.str.offset ≤ s.endExclusive.offset
-- Mathlib.Computability.RecursiveIn
Nat.RecursiveIn.left : ∀ {O : Set (ℕ →. ℕ)}, Nat.RecursiveIn O fun n => ↑(some (Nat.unpair n).1)
-- Mathlib.Analysis.Normed.Order.Hom.Ultra
AddGroupSeminormClass.toSeminormedAddGroup.congr_simp : ∀ {F : Type u_1} {α : Type u_2} [inst : FunLike F α ℝ] [inst_1 : AddGroup α] [inst_2 : AddGroupSeminormClass F α ℝ]
  (f f_1 : F), f = f_1 → AddGroupSeminormClass.toSeminormedAddGroup f = AddGroupSeminormClass.toSeminormedAddGroup f_1
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.RepeatInvariant.eq_1 : ∀ (α β Pred : Type u), Std.Internal.Do.RepeatInvariant α β Pred = (α ⊕ β → Pred)
-- Mathlib.Algebra.Module.FinitePresentation
instFinitePresentation : ∀ {R : Type u_1} [inst : Ring R], Module.FinitePresentation R R
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKey?_eq_some_minKey! : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.isEmpty = false → t.minKey? = some t.minKey!
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get?_eq_some_iff : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {k k' : α},
  t.get? k = some k' ↔ ∃ (h : k ∈ t), t.get k h = k'
-- Init.Data.String.Lemmas.Pattern.String.ForwardSearcher
/-- The start of the window, as a valid position in `s.`  -/
_private.Init.Data.String.Lemmas.Pattern.String.ForwardSearcher.0.String.Slice.Pattern.Model.ForwardSliceSearcher.Invariants.base : {pat s : String.Slice} →
  {needlePos stackPos : String.Pos.Raw} →
    String.Slice.Pattern.Model.ForwardSliceSearcher.Invariants✝ pat s needlePos stackPos → s.Pos
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
ENNReal.tsum_biUnion_le : ∀ {α : Type u_1} {ι : Type u_4} (f : α → ENNReal) (s : Finset ι) (t : ι → Set α),
  ∑' (x : ↑(⋃ i ∈ s, t i)), f ↑x ≤ ∑ i ∈ s, ∑' (x : ↑(t i)), f ↑x
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.LHom.realize_onBoundedFormula : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'}
  [inst_1 : L'.Structure M] (φ : L →ᴸ L') [φ.IsExpansionOn M] {n : ℕ} (ψ : L.BoundedFormula α n) {v : α → M}
  {xs : Fin n → M}, (φ.onBoundedFormula ψ).Realize v xs ↔ ψ.Realize v xs
-- Std.Internal.Do.WP.Lemmas
Std.Internal.Do.WPMonad.wp_modify_StateT_apply_eq : ∀ {Pred : Type u_1} {EPred : Type u_2} {m : Type u → Type v} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {σ : Type u}
  {post : PUnit.{u + 1} → σ → Pred} {epost : EPred} (f : σ → σ),
  Std.Internal.Do.wp (modify f) post epost =
    Std.Internal.Do.wp (MonadStateOf.modifyGet fun s => (PUnit.unit, f s)) post epost
-- Mathlib.Algebra.Algebra.Operations
Submodule.singleton_smul : ∀ {R : Type u} [inst : CommSemiring R] {A : Type v} [inst_1 : CommSemiring A] [inst_2 : Algebra R A] (a : A)
  (M : Submodule R A), Set.up {a} • M = Submodule.map (LinearMap.mulLeft R a) M
-- Mathlib.Algebra.Ring.Basic
/-- The right multiplication map: `(a, b) ↦ b * a`. See also `AddMonoidHom.mulRight`.  -/
AddMonoid.End.mulRight : {R : Type u_1} → [inst : NonUnitalNonAssocSemiring R] → R →+ AddMonoid.End R
-- Mathlib.LinearAlgebra.TensorProduct.Associator
TensorProduct.assoc_tensor' : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_5} {N : Type u_6} {Q : Type u_8} {S : Type u_9}
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid Q] [inst_4 : AddCommMonoid S]
  [inst_5 : Module R M] [inst_6 : Module R N] [inst_7 : Module R Q] [inst_8 : Module R S],
  TensorProduct.assoc R M (TensorProduct R N Q) S =
    LinearEquiv.rTensor S (TensorProduct.assoc R M N Q).symm ≪≫ₗ TensorProduct.assoc R (TensorProduct R M N) Q S ≪≫ₗ
        TensorProduct.assoc R M N (TensorProduct R Q S) ≪≫ₗ
      LinearEquiv.lTensor M (TensorProduct.assoc R N Q S).symm
-- Mathlib.RingTheory.TensorProduct.Free
Algebra.TensorProduct.basis_apply : ∀ {R : Type u_1} {A : Type u_2} {M : Type uM} {ι : Type uι} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] (b : Module.Basis ι R M) (i : ι),
  (Algebra.TensorProduct.basis A b) i = 1 ⊗ₜ[R] b i
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.insertMany_cons : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} {l : List (α × β)} {k : α} {v : β},
  t.insertMany ((k, v) :: l) = (t.insert k v).insertMany l
-- Mathlib.Data.Finset.Card
/-- Given an injective map `f` from a finite set `s` to another finite set `t`, if `t` is no larger
than `s`, then `f` is surjective to `t` when restricted to `s`.
See `Finset.surj_on_of_inj_on_of_card_le` for the version where `f` is a dependent function.
 -/
Finset.surjOn_of_injOn_of_card_le : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} (f : α → β),
  Set.MapsTo f ↑s ↑t → Set.InjOn f ↑s → t.card ≤ s.card → Set.SurjOn f ↑s ↑t
-- Mathlib.Tactic.CancelDenoms.Core
_private.Mathlib.Tactic.CancelDenoms.Core.0.Mathlib.Tactic.cancelDenominatorsTarget : Lean.Elab.Tactic.TacticM Unit
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey!_erase_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {k : α}, (t.erase k).getKey! k = default
-- Mathlib.Data.QPF.Multivariate.Constructions.Fix
MvQPF.Fix.ind : ∀ {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} (p : MvQPF.Fix F α → Prop),
  (∀ (x : F (α ::: MvQPF.Fix F α)), MvFunctor.LiftP (α.PredLast p) x → p (MvQPF.Fix.mk x)) → ∀ (x : MvQPF.Fix F α), p x
-- Init.Data.Fin.Lemmas
Fin.val_addNat : ∀ {n : ℕ} (m : ℕ) (i : Fin n), ↑(i.addNat m) = ↑i + m
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
CategoryTheory.Bicategory.Adj.Hom₂.mk.inj : ∀ {B : Type u} {inst : CategoryTheory.Bicategory B} {a b : CategoryTheory.Bicategory.Adj B} {α β : a ⟶ b}
  {τl : α.l ⟶ β.l} {τr : β.r ⟶ α.r}
  {conjugateEquiv_τl :
    autoParam ((CategoryTheory.Bicategory.conjugateEquiv β.adj α.adj) τl = τr)
      CategoryTheory.Bicategory.Adj.Hom₂.conjugateEquiv_τl._autoParam}
  {τl_1 : α.l ⟶ β.l} {τr_1 : β.r ⟶ α.r}
  {conjugateEquiv_τl_1 :
    autoParam ((CategoryTheory.Bicategory.conjugateEquiv β.adj α.adj) τl_1 = τr_1)
      CategoryTheory.Bicategory.Adj.Hom₂.conjugateEquiv_τl._autoParam},
  { τl := τl, τr := τr, conjugateEquiv_τl := conjugateEquiv_τl } =
      { τl := τl_1, τr := τr_1, conjugateEquiv_τl := conjugateEquiv_τl_1 } →
    τl = τl_1 ∧ τr = τr_1
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
HasProd.nat_mul_neg_add_one : ∀ {M : Type u_1} [inst : CommMonoid M] [inst_1 : TopologicalSpace M] {m : M} {f : ℤ → M},
  HasProd f m → HasProd (fun n => f ↑n * f (-(↑n + 1))) m
-- Mathlib.Topology.Constructions
IsOpenMap.domRestrict : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  IsOpenMap f → ∀ {s : Set X}, IsOpen s → IsOpenMap (s.domRestrict f)
-- Init.Data.List.Basic
List.foldl_nil : ∀ {α : Type u_1} {β : Type u_2} {f : α → β → α} {b : α}, List.foldl f b [] = b
-- Mathlib.MeasureTheory.Function.AEEqFun.DomAct
DomMulAct.smul_aeeqFun_const : ∀ {M : Type u_1} {α : Type u_2} {β : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
  [inst_1 : TopologicalSpace β] [inst_2 : SMul M α] [inst_3 : MeasurableConstSMul M α]
  [inst_4 : MeasureTheory.SMulInvariantMeasure M α μ] (c : Mᵈᵐᵃ) (b : β),
  c • MeasureTheory.AEEqFun.const α b = MeasureTheory.AEEqFun.const α b
-- Init.Data.Slice.List.Lemmas
ListSlice.toArray_toList : ∀ {α : Type u_1} {xs : ListSlice α}, (Std.Slice.toList xs).toArray = Std.Slice.toArray xs
-- Init.Data.Int.Linear
Int.Internal.Linear.norm_dvd_gcd_cert.eq_1 : ∀ (k₁ : ℤ) (e₁ : Int.Internal.Linear.Expr) (k₂ : ℤ) (p₂ : Int.Internal.Linear.Poly) (k : ℤ),
  Int.Internal.Linear.norm_dvd_gcd_cert k₁ e₁ k₂ p₂ k = Int.Internal.Linear.dvd_coeff_cert k₁ e₁.norm k₂ p₂ k
-- Mathlib.Algebra.Divisibility.Basic
/-- **Alias** of `Dvd.intro`. -/
dvd_of_mul_right_eq : ∀ {α : Type u_1} [inst : Semigroup α] {a b : α} (c : α), a * c = b → a ∣ b
-- Mathlib.Algebra.Polynomial.DenomsClearable
/-- Evaluating a polynomial with integer coefficients at a rational number and clearing
denominators, yields a number greater than or equal to one.  The target can be any
`LinearOrderedField K`.
The assumption on `K` could be weakened to `LinearOrderedCommRing` assuming that the
image of the denominator is invertible in `K`.  -/
one_le_pow_mul_abs_eval_div : ∀ {K : Type u_1} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] {f : Polynomial ℤ} {a b : ℤ},
  0 < b →
    Polynomial.eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) ≠ 0 →
      1 ≤ ↑b ^ f.natDegree * |Polynomial.eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f)|
-- Std.Data.DHashMap.Internal.AssocList.Basic
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.AssocList.map : {α : Type u} →
  {β : α → Type v} →
    {γ : α → Type w} → ((a : α) → β a → γ a) → Std.DHashMap.Internal.AssocList α β → Std.DHashMap.Internal.AssocList α γ
-- Mathlib.Combinatorics.Matroid.Circuit
/-- `M.IsCircuit C` means that `C` is a minimal dependent set in `M`.  -/
Matroid.IsCircuit : {α : Type u_1} → Matroid α → Set α → Prop
-- Mathlib.RingTheory.Lasker
Submodule.IsMinimalPrimaryDecomposition.mem_associatedPrimes : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {N : Submodule R M} {t : Finset (Submodule R M)},
  N.IsMinimalPrimaryDecomposition t → ∀ {q : Submodule R M}, q ∈ t → (q.colon Set.univ).radical ∈ N.associatedPrimes
-- Mathlib.CategoryTheory.SingleObj
/-- The endomorphisms monoid of the only object in `SingleObj M` is equivalent to the original
monoid `M`.  -/
CategoryTheory.SingleObj.toEnd : (M : Type u) → [inst : Monoid M] → M ≃* CategoryTheory.End (CategoryTheory.SingleObj.star M)
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Cat
CategoryTheory.Bicategory.toNatTrans_conjugateEquiv : ∀ {C D : CategoryTheory.Cat} {L₁ L₂ : C ⟶ D} {R₁ R₂ : D ⟶ C} (adj₁ : CategoryTheory.Bicategory.Adjunction L₁ R₁)
  (adj₂ : CategoryTheory.Bicategory.Adjunction L₂ R₂) (f : L₂ ⟶ L₁),
  ((CategoryTheory.Bicategory.conjugateEquiv adj₁ adj₂) f).toNatTrans =
    (CategoryTheory.conjugateEquiv (CategoryTheory.Adjunction.ofCat adj₁) (CategoryTheory.Adjunction.ofCat adj₂))
      f.toNatTrans
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey?_minKeyD : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    l.isEmpty = false →
      ∀ {fallback : α},
        Std.Internal.List.getKey? (Std.Internal.List.minKeyD l fallback) l = some (Std.Internal.List.minKeyD l fallback)
-- Mathlib.GroupTheory.Complement
Subgroup.instMulActionLeftTransversal : {G : Type u_1} →
  [inst : Group G] →
    {H : Subgroup G} →
      {F : Type u_2} →
        [inst_1 : Group F] → [inst_2 : MulAction F G] → [MulAction.QuotientAction F H] → MulAction F H.LeftTransversal
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F : C ⥤ Dᵒᵖ` creates finite limits, then `F.leftOp : Cᵒᵖ ⥤ D` creates finite
colimits.  -/
CategoryTheory.Limits.createsFiniteColimitsLeftOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C Dᵒᵖ) →
          [CategoryTheory.Limits.CreatesFiniteLimits F] → CategoryTheory.Limits.CreatesFiniteColimits F.leftOp
-- Init.Data.UInt.Lemmas
UInt32.ofBitVec_ofFin : ∀ (n : Fin (2 ^ 32)), { toBitVec := { toFin := n } } = UInt32.ofFin n
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddHom.srangeRestrict.eq_1 : ∀ {M : Type u_1} [inst : Add M] {N : Type u_5} [inst_1 : Add N] (f : M →ₙ+ N),
  f.srangeRestrict = f.codRestrict f.srange ⋯
-- Init.PropLemmas
Decidable.and_iff_not_not_or_not : ∀ {a b : Prop} [Decidable a] [Decidable b], a ∧ b ↔ ¬(¬a ∨ ¬b)
-- Mathlib.Logic.Function.Basic
/-- `s.piecewise f g` is the function equal to `f` on the set `s`, and to `g` on its complement.  -/
Set.piecewise : {α : Type u} →
  {β : α → Sort v} → (s : Set α) → ((i : α) → β i) → ((i : α) → β i) → [(j : α) → Decidable (j ∈ s)] → (i : α) → β i
-- Mathlib.Algebra.Homology.HomologicalBicomplex
/-- Constructor for bicomplexes taking as inputs a graded object, horizontal differentials
and vertical differentials satisfying suitable relations.  -/
HomologicalComplex₂.ofGradedObject : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {I₁ : Type u_2} →
        {I₂ : Type u_3} →
          (c₁ : ComplexShape I₁) →
            (c₂ : ComplexShape I₂) →
              (X : CategoryTheory.GradedObject (I₁ × I₂) C) →
                (d₁ : (i₁ i₁' : I₁) → (i₂ : I₂) → X (i₁, i₂) ⟶ X (i₁', i₂)) →
                  (d₂ : (i₁ : I₁) → (i₂ i₂' : I₂) → X (i₁, i₂) ⟶ X (i₁, i₂')) →
                    (∀ (i₁ i₁' : I₁), ¬c₁.Rel i₁ i₁' → ∀ (i₂ : I₂), d₁ i₁ i₁' i₂ = 0) →
                      (∀ (i₁ : I₁) (i₂ i₂' : I₂), ¬c₂.Rel i₂ i₂' → d₂ i₁ i₂ i₂' = 0) →
                        (∀ (i₁ i₁' i₁'' : I₁) (i₂ : I₂),
                            CategoryTheory.CategoryStruct.comp (d₁ i₁ i₁' i₂) (d₁ i₁' i₁'' i₂) = 0) →
                          (∀ (i₁ : I₁) (i₂ i₂' i₂'' : I₂),
                              CategoryTheory.CategoryStruct.comp (d₂ i₁ i₂ i₂') (d₂ i₁ i₂' i₂'') = 0) →
                            (∀ (i₁ i₁' : I₁) (i₂ i₂' : I₂),
                                CategoryTheory.CategoryStruct.comp (d₁ i₁ i₁' i₂) (d₂ i₁' i₂ i₂') =
                                  CategoryTheory.CategoryStruct.comp (d₂ i₁ i₂ i₂') (d₁ i₁ i₁' i₂')) →
                              HomologicalComplex₂ C c₁ c₂
-- Std.Async.Select
Std.Async.Selectable.case.injEq : ∀ {α β : Type} (selector : Std.Async.Selector β) (cont : β → Std.Async.Async α) (β_1 : Type)
  (selector_1 : Std.Async.Selector β_1) (cont_1 : β_1 → Std.Async.Async α),
  ({ β := β, selector := selector, cont := cont } = { β := β_1, selector := selector_1, cont := cont_1 }) =
    (β = β_1 ∧ selector ≍ selector_1 ∧ cont ≍ cont_1)
-- Mathlib.Topology.ClusterPt
/-- `x` is an accumulation point of a set `C` iff
there are points near `x` in `C` and different from `x`.  -/
accPt_iff_frequently : ∀ {X : Type u} [inst : TopologicalSpace X] {x : X} {C : Set X},
  AccPt x (Filter.principal C) ↔ ∃ᶠ (y : X) in nhds x, y ≠ x ∧ y ∈ C
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.mem_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : α → β → γ} {k : α}, k ∈ Std.ExtHashMap.map f m ↔ k ∈ m
-- Mathlib.Tactic.CrossRefAttribute
Mathlib.CrossRef.Tag.mk.sizeOf_spec : ∀ (declName : Lean.Name) (database : Mathlib.CrossRef.Database) (tag comment : String),
  sizeOf { declName := declName, database := database, tag := tag, comment := comment } =
    1 + sizeOf declName + sizeOf database + sizeOf tag + sizeOf comment
-- Mathlib.CategoryTheory.Functor.EpiMono
/-- A functor reflects monomorphisms if morphisms that are mapped to monomorphisms are themselves
monomorphisms.  -/
CategoryTheory.Functor.ReflectsMonomorphisms : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} → [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Functor C D → Prop