mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
/-- The composition in the opposite direction is equal to the identity if and only if `F` preserves
the biproduct, see `preservesBiproduct_of_monoBiproductComparison`.  -/
CategoryTheory.Functor.biproductComparison'_comp_biproductComparison : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {J : Type w₁}
  (F : CategoryTheory.Functor C D) (f : J → C) [inst_4 : CategoryTheory.Limits.HasBiproduct f]
  [inst_5 : CategoryTheory.Limits.HasBiproduct (F.obj ∘ f)] [F.PreservesZeroMorphisms],
  CategoryTheory.CategoryStruct.comp (F.biproductComparison' f) (F.biproductComparison f) =
    CategoryTheory.CategoryStruct.id (⨁ F.obj ∘ f)
-- Mathlib.Topology.Separation.GDelta
Set.Finite.isGδ : ∀ {X : Type u_1} [inst : TopologicalSpace X] [FirstCountableTopology X] {s : Set X} [T1Space X], s.Finite → IsGδ s
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
csSup_image2_eq_csSup_csInf : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : ConditionallyCompleteLattice α]
  [inst_1 : ConditionallyCompleteLattice β] [inst_2 : ConditionallyCompleteLattice γ] {s : Set α} {t : Set β}
  {l : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β},
  (∀ (b : β), GaloisConnection (Function.swap l b) (u₁ b)) →
    (∀ (a : α), GaloisConnection (l a ∘ ⇑OrderDual.ofDual) (⇑OrderDual.toDual ∘ u₂ a)) →
      s.Nonempty → BddAbove s → t.Nonempty → BddBelow t → sSup (Set.image2 l s t) = l (sSup s) (sInf t)
-- Mathlib.Analysis.Normed.Group.Pointwise
closedBall_zero_add_singleton : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] (δ : ℝ) (x : E), Metric.closedBall 0 δ + {x} = Metric.closedBall x δ
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokenModifier.async.sizeOf_spec : sizeOf Lean.Lsp.SemanticTokenModifier.async = 1
-- Init.Data.Int.DivMod.Lemmas
Int.ediv_lt_iff_of_dvd_of_neg : ∀ {a b c : ℤ}, b < 0 → b ∣ a → (a / b < c ↔ b * c < a)
-- Init.Data.Vector.Lemmas
Vector.any_replicate : ∀ {α : Type u_1} {f : α → Bool} {n : ℕ} {a : α}, (Vector.replicate n a).any f = if n = 0 then false else f a
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.AbelianImages
CategoryTheory.Abelian.PreservesImage.iso.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] {X Y : C} (f : X ⟶ Y)
  [inst_5 : CategoryTheory.Limits.HasCokernel f]
  [inst_6 : CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.π f)]
  [inst_7 : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) F]
  [inst_8 :
    CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.cokernel.π f) 0) F]
  [inst_9 : CategoryTheory.Limits.HasCokernel (F.map f)]
  [inst_10 : CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.π (F.map f))],
  CategoryTheory.Abelian.PreservesImage.iso F f =
    CategoryTheory.Limits.PreservesKernel.iso F (CategoryTheory.Limits.cokernel.π f) ≪≫
      CategoryTheory.Limits.kernel.mapIso (F.map (CategoryTheory.Limits.cokernel.π f))
        (CategoryTheory.Limits.cokernel.π (F.map f)) (CategoryTheory.Iso.refl (F.obj Y))
        (CategoryTheory.Limits.PreservesCokernel.iso F f) ⋯
-- Std.Data.ExtDTreeMap.Basic
/-- Given a proof that such a mapping exists, retrieves the smallest key that is
greater than the given key.
 -/
Std.ExtDTreeMap.getKeyGT : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} →
      [inst : Std.TransCmp cmp] → (t : Std.ExtDTreeMap α β cmp) → (k : α) → (∃ a ∈ t, cmp a k = Ordering.gt) → α
-- Mathlib.Algebra.GroupWithZero.Hom
NeZero.of_injective : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Zero α] [inst_1 : Zero β] [inst_2 : FunLike F α β]
  [ZeroHomClass F α β] {a : α} {f : F}, Function.Injective ⇑f → ∀ [NeZero a], NeZero (f a)
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.op_id : ∀ {C : Type u₁} [inst : CategoryTheory.CategoryStruct.{v₁, u₁} C] {X : C},
  (CategoryTheory.CategoryStruct.id X).op = CategoryTheory.CategoryStruct.id (Opposite.op X)
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.Precoverage.RespectsIso.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C},
  (∀ {S : C} {E F : CategoryTheory.PreZeroHypercover S} (e : E ≅ F),
      E.presieve₀ ∈ J.coverings S → F.presieve₀ ∈ J.coverings S) →
    J.RespectsIso
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.Approx.instInhabitedCofixAOfA : (F : PFunctor.{uA, uB}) → [Inhabited F.A] → {n : ℕ} → Inhabited (PFunctor.Approx.CofixA F n)
-- Mathlib.Data.Matrix.Diagonal
Matrix.diagonal_eq_zero : ∀ {n : Type u_3} {α : Type v} [inst : DecidableEq n] [inst_1 : Zero α] {d : n → α}, Matrix.diagonal d = 0 ↔ d = 0
-- Aesop.Util.Basic
Aesop.runTacticMAsMetaM : {α : Type} → Lean.Elab.Tactic.TacticM α → List Lean.MVarId → Lean.MetaM (α × List Lean.MVarId)
-- Mathlib.GroupTheory.Exponent
AddMonoid.exponent_pi_eq_zero : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → AddMonoid (M i)] {j : ι},
  AddMonoid.exponent (M j) = 0 → AddMonoid.exponent ((i : ι) → M i) = 0
-- Mathlib.Probability.Martingale.Upcrossing
MeasureTheory.StronglyAdapted.measurable_upcrossings : ∀ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {a b : ℝ} {f : ℕ → Ω → ℝ} {ℱ : MeasureTheory.Filtration ℕ m0},
  MeasureTheory.StronglyAdapted ℱ f → a < b → Measurable (MeasureTheory.upcrossings a b f)
-- Mathlib.Algebra.Group.Equiv.Basic
AddEquiv.ofUnique.eq_1 : ∀ {M : Type u_16} {N : Type u_17} [inst : Unique M] [inst_1 : Unique N] [inst_2 : Add M] [inst_3 : Add N],
  AddEquiv.ofUnique = { toEquiv := Equiv.ofUnique M N, map_add' := ⋯ }
-- Mathlib.Algebra.Algebra.NonUnitalHom
NonUnitalAlgHom.coe_inverse' : ∀ {R : Type u} {S : Type u₁} [inst : Monoid R] [inst_1 : Monoid S] {φ : R →* S} {A : Type v} {B : Type w}
  [inst_2 : NonUnitalNonAssocSemiring A] [inst_3 : DistribMulAction R A] [inst_4 : NonUnitalNonAssocSemiring B]
  [inst_5 : DistribMulAction S B] {φ' : S →* R} (f : A →ₛₙₐ[φ] B) (g : B → A) (k : Function.RightInverse ⇑φ' ⇑φ)
  (h₁ : Function.LeftInverse g ⇑f) (h₂ : Function.RightInverse g ⇑f), ⇑(f.inverse' g k h₁ h₂) = g
-- Mathlib.RingTheory.Valuation.ValuationSubring
/-- The action on a valuation subring corresponding to applying the action to every element.

This is available as an instance in the `Pointwise` locale.

This is a stronger version of `ValuationSubring.pointwiseSMul`.  -/
ValuationSubring.pointwiseMulAction : {K : Type u} →
  [inst : Field K] → {G : Type u_1} → [inst_1 : Group G] → [MulSemiringAction G K] → MulAction G (ValuationSubring K)
-- Aesop.Index.Forward
Aesop.ForwardIndex.mk : Lean.Meta.DiscrTree (Aesop.ForwardRule × Aesop.PremiseIndex) →
  Lean.PHashMap Aesop.RuleName Aesop.ForwardRule → Lean.PHashSet Aesop.ForwardRule → Aesop.ForwardIndex
-- Std.Internal.Do.Order.Heyting
/-- Heyting implication: the upper adjoint of the lattice meet. For `Prop` it is `→`.  -/
Lean.Order.«term_⇨_» : Lean.TrailingParserDescr
-- Init.Data.Option.Lemmas
/-- See `Option.apply_get` for a version that can be rewritten in the reverse direction.  -/
Option.get_map : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {o : Option α} {h : (Option.map f o).isSome = true},
  (Option.map f o).get h = f (o.get ⋯)
-- Lean.Data.Json.Parser
Lean.Json.parse : String → Except String Lean.Json
-- Init.Data.Fin.Lemmas
Fin.coe_sub : ∀ {n : ℕ} (a b : Fin n), ↑(a - b) = (n - ↑b + ↑a) % n
-- Mathlib.SetTheory.Cardinal.Ordinal
/-- **Alias** of `Ordinal.isPrincipal_mul_omega`. -/
Ordinal.principal_mul_omega : ∀ (o : Ordinal.{u_1}), Ordinal.IsPrincipal (fun x1 x2 => x1 * x2) (Ordinal.omega o)
-- Mathlib.CategoryTheory.CommSq
CategoryTheory.CommSq.HasLift.iff_unop : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A B X Y : Cᵒᵖ} {f : A ⟶ X} {i : A ⟶ B} {p : X ⟶ Y}
  {g : B ⟶ Y} (sq : CategoryTheory.CommSq f i p g), sq.HasLift ↔ ⋯.HasLift
-- Mathlib.Algebra.CubicDiscriminant
Cubic.map_roots : ∀ {R : Type u_1} {S : Type u_2} {P : Cubic R} [inst : CommRing R] [inst_1 : CommRing S] {φ : R →+* S}
  [inst_2 : IsDomain S], (Cubic.map φ P).roots = (Polynomial.map φ P.toPoly).roots
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.ofLE_refl : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {B : C} (X : CategoryTheory.Subobject B),
  X.ofLE X ⋯ = CategoryTheory.CategoryStruct.id (CategoryTheory.Subobject.underlying.obj X)
-- Lean.Data.JsonRpc
Lean.JsonRpc.Message.responseError.sizeOf_spec : ∀ (id : Lean.JsonRpc.RequestID) (code : Lean.JsonRpc.ErrorCode) (message : String) (data? : Option Lean.Json),
  sizeOf (Lean.JsonRpc.Message.responseError id code message data?) =
    1 + sizeOf id + sizeOf code + sizeOf message + sizeOf data?
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Real.differentiableWithinAt_arcsin_Iic : ∀ {x : ℝ}, DifferentiableWithinAt ℝ Real.arcsin (Set.Iic x) x ↔ x ≠ 1
-- Mathlib.Control.Bitraversable.Instances
instBitraversableProd : Bitraversable Prod
-- Mathlib.Data.Rat.Floor
/-- This variant of `floor_def` uses the `Int.floor` (for any `FloorRing`) rather than `Rat.floor`.
 -/
Rat.floor_def' : ∀ {q : ℚ}, ⌊q⌋ = q.num / ↑q.den
-- Mathlib.RingTheory.Polynomial.Wronskian
Polynomial.isAlt_wronskianBilin : ∀ {R : Type u_1} [inst : CommRing R], (Polynomial.wronskianBilin R).IsAlt
-- Mathlib.Algebra.Group.Defs
npowBinRec_succ : ∀ {M : Type u_2} [inst : Semigroup M] [inst_1 : One M] (n : ℕ) (m : M), npowBinRec (n + 1) m = npowBinRec n m * m
-- Mathlib.Topology.MetricSpace.Closeds
Metric.uniformContinuous_infDist_Hausdorff_dist : ∀ {α : Type u_1} [inst : MetricSpace α], UniformContinuous fun p => Metric.infDist p.1 ↑p.2
-- Init.Data.Array.Lemmas
Array.mem_replicate : ∀ {α : Type u_1} {a b : α} {n : ℕ}, b ∈ Array.replicate n a ↔ n ≠ 0 ∧ b = a
-- Mathlib.Geometry.Euclidean.Triangle
/-- Converse of pons asinorum, oriented angle-at-point form (given equality of angles mod `π`).  -/
EuclideanGeometry.dist_eq_of_two_zsmul_oangle_eq : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [inst_4 : Module.Oriented ℝ V (Fin 2)] [inst_5 : Fact (Module.finrank ℝ V = 2)]
  {p₁ p₂ p₃ : P},
  2 • EuclideanGeometry.oangle p₁ p₂ p₃ = 2 • EuclideanGeometry.oangle p₂ p₃ p₁ →
    EuclideanGeometry.oangle p₃ p₁ p₂ ≠ 0 → EuclideanGeometry.oangle p₃ p₁ p₂ ≠ ↑Real.pi → dist p₁ p₂ = dist p₁ p₃
-- Mathlib.RingTheory.HahnSeries.Summable
/-- A summable family induced by an equivalence of the parametrizing type.  -/
HahnSeries.SummableFamily.Equiv : {Γ : Type u_1} →
  {R : Type u_3} →
    {α : Type u_5} →
      {β : Type u_6} →
        [inst : PartialOrder Γ] →
          [inst_1 : AddCommMonoid R] → α ≃ β → HahnSeries.SummableFamily Γ R α → HahnSeries.SummableFamily Γ R β
-- Mathlib.Algebra.Category.Ring.Basic
CommSemiRingCat.of.inj : ∀ {carrier : Type u} {commSemiring : CommSemiring carrier} {carrier_1 : Type u}
  {commSemiring_1 : CommSemiring carrier_1},
  CommSemiRingCat.of carrier = CommSemiRingCat.of carrier_1 → carrier = carrier_1 ∧ commSemiring ≍ commSemiring_1
-- Mathlib.Order.Category.PartOrd
/-- The type of morphisms in `PartOrd R`.  -/
PartOrd.Hom : PartOrd → PartOrd → Type u
-- Batteries.Util.ProofWanted
/-- Prefix for the generated parameter binder name.  -/
_private.Batteries.Util.ProofWanted.0.WantedRefKind.hypPrefix : WantedRefKind✝ → String
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.lt_logb_iff_rpow_lt_of_base_lt_one : ∀ {b x y : ℝ}, 0 < b → b < 1 → 0 < y → (x < Real.logb b y ↔ y < b ^ x)
-- Mathlib.Geometry.Euclidean.PerpBisector
AffineSubspace.perpBisector_self : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (p : P), AffineSubspace.perpBisector p p = ⊤
-- Init.Data.Slice.List.Basic
instSliceableListSliceNat_6 : {α : Type u} → Std.Ric.Sliceable (ListSlice α) ℕ (ListSlice α)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.isEmpty_inter_right : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α], m₂.isEmpty = true → (m₁ ∩ m₂).isEmpty = true
-- Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
CategoryTheory.MorphismProperty.Over.mapCongr_inv_app_left : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {P : CategoryTheory.MorphismProperty T}
  (Q : CategoryTheory.MorphismProperty T) [inst_1 : Q.IsMultiplicative] [inst_2 : P.IsStableUnderComposition]
  [inst_3 : Q.RespectsIso] {X Y : T} {f g : X ⟶ Y} (hfg : f = g) (hf : P f) (X_1 : P.Over Q X),
  ((CategoryTheory.MorphismProperty.Over.mapCongr Q hfg hf).inv.app X_1).left =
    CategoryTheory.CategoryStruct.id X_1.left
-- Mathlib.Analysis.Normed.Group.AddCircle
AddCircle.instNormedAddCommGroupReal : (p : ℝ) → NormedAddCommGroup (AddCircle p)
-- Mathlib.RingTheory.Coalgebra.CoassocSimps
CoassocSimps.coassoc_left : ∀ {R : Type u_1} {M : Type u_3} {M' : Type u_6} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] [inst_5 : Coalgebra R M] (f : M →ₗ[R] M'),
  ↑(TensorProduct.assoc R M M M') ∘ₗ TensorProduct.map CoalgebraStruct.comul f ∘ₗ CoalgebraStruct.comul =
    TensorProduct.map LinearMap.id (TensorProduct.map LinearMap.id f) ∘ₗ
      TensorProduct.map LinearMap.id CoalgebraStruct.comul ∘ₗ CoalgebraStruct.comul
-- Mathlib.Topology.UniformSpace.Cauchy
totallyBounded_sSup : ∀ {α : Type u} [uniformSpace : UniformSpace α] {S : Set (Filter α)},
  S.Finite → ((sSup S).TotallyBounded ↔ ∀ f ∈ S, f.TotallyBounded)
-- Mathlib.RingTheory.PrincipalIdealDomain
/-- If a `RingHom` maps all units and all factors of an element `a` into a submonoid `s`, then it
also maps `a` into that submonoid.  -/
PrincipalIdealRing.ringHom_mem_submonoid_of_factors_subset_of_units_subset : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsPrincipalIdealRing R]
  [inst_3 : NonAssocSemiring S] (f : R →+* S) (s : Submonoid S) (a : R),
  a ≠ 0 → (∀ b ∈ PrincipalIdealRing.factors a, f b ∈ s) → (∀ (c : Rˣ), f ↑c ∈ s) → f a ∈ s
-- Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
UniformConvergenceCLM.hasBasis_nhds_zero_of_basis : ∀ {𝕜₁ : 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] [inst_7 : TopologicalSpace F] [inst_8 : IsTopologicalAddGroup F]
  {ι : Type u_6} (𝔖 : Set (Set E)),
  𝔖.Nonempty →
    DirectedOn (fun x1 x2 => x1 ⊆ x2) 𝔖 →
      ∀ {p : ι → Prop} {b : ι → Set F},
        (nhds 0).HasBasis p b → (nhds 0).HasBasis (fun Si => Si.1 ∈ 𝔖 ∧ p Si.2) fun Si => {f | ∀ x ∈ Si.1, f x ∈ b Si.2}
-- Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise
ContDiffPointwiseHolderAt.snd : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {k : ℕ} {α : ↑unitInterval} {a : E × F}, ContDiffPointwiseHolderAt k α Prod.snd a
-- Mathlib.LinearAlgebra.Matrix.Nonsingular
/-- A nontrivial commutative semiring satisfies the strong rank condition.  -/
CommSemiring.strongRankCondition_of_nontrivial : ∀ {R : Type u_1} [inst : CommSemiring R] [Nontrivial R], StrongRankCondition R
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.degree_sum_fin_lt : ∀ {R : Type u} [inst : Semiring R] {n : ℕ} (f : Fin n → R), (∑ i, Polynomial.C (f i) * Polynomial.X ^ ↑i).degree < ↑n
-- Mathlib.Algebra.Homology.HomologicalComplexLimits
HomologicalComplex.instPreservesColimitsOfShapeSingle : ∀ {C : Type u_1} {ι : Type u_2} {J : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_3} J] {c : ComplexShape ι}
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasZeroObject C]
  [inst_4 : DecidableEq ι] (i : ι), CategoryTheory.Limits.PreservesColimitsOfShape J (HomologicalComplex.single C c i)
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.IsCoreflexivePair.common_retraction' : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {A B : C} {f g : A ⟶ B}
  [self : CategoryTheory.IsCoreflexivePair f g],
  ∃ s,
    CategoryTheory.CategoryStruct.comp f s = CategoryTheory.CategoryStruct.id A ∧
      CategoryTheory.CategoryStruct.comp g s = CategoryTheory.CategoryStruct.id A
-- Mathlib.Data.Rat.Cast.Order
Rat.cast_nonpos : ∀ {q : ℚ} {K : Type u_5} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K], ↑q ≤ 0 ↔ q ≤ 0
-- Lean.Parser.Extra
Lean.Parser.sepBy1Indent.parenthesizer : Lean.PrettyPrinter.Parenthesizer →
  String → Lean.PrettyPrinter.Parenthesizer → optParam Bool false → Lean.PrettyPrinter.Parenthesizer
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.Point.xRep_ne_zero : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Affine R} [Nontrivial R] (P : W'.Point), P.xRep ≠ 0
-- Std.Data.DTreeMap.Lemmas
/-- Variant of `get_map` that holds without `LawfulEqCmp`.  -/
Std.DTreeMap.Const.get_map' : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.DTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] {f : α → β → γ} {k : α} {h' : k ∈ Std.DTreeMap.map f t},
  Std.DTreeMap.Const.get (Std.DTreeMap.map f t) k h' = f (t.getKey k ⋯) (Std.DTreeMap.Const.get t k ⋯)
-- Mathlib.Algebra.Category.BialgCat.Basic
/-- Turn a morphism in `BialgCat` back into a `BialgHom`.  -/
BialgCat.Hom.toBialgHom : {R : Type u} → [inst : CommRing R] → {X Y : BialgCat R} → X.Hom Y → X.carrier →ₐc[R] Y.carrier
-- Mathlib.CategoryTheory.SingleObj
/-- Groupoid structure on `SingleObj M`.  -/
CategoryTheory.SingleObj.groupoid : (G : Type u) → [Group G] → CategoryTheory.Groupoid (CategoryTheory.SingleObj G)
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.UInt64.toBitVec_ite : ∀ {c : Prop} {t e : UInt64} [inst : Decidable c], (if c then t else e).toBitVec = if c then t.toBitVec else e.toBitVec
-- Mathlib.Algebra.Homology.ModelCategory.Lifting
/-- The `1`-cochain from `Q` to `K` which refines `cocycle₁'`.  -/
CochainComplex.Lifting.cochain₁ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {A B X Y : CochainComplex C ℤ} →
        {t : A ⟶ X} →
          {i : A ⟶ B} →
            {p : X ⟶ Y} →
              {b : B ⟶ Y} →
                (sq : CategoryTheory.CommSq t i p b) →
                  ((n : ℤ) → ⋯.LiftStruct) →
                    {Q : CochainComplex C ℤ} →
                      {π : B ⟶ Q} →
                        {hπ : CategoryTheory.CategoryStruct.comp i π = 0} →
                          CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ π hπ) →
                            {K : CochainComplex C ℤ} →
                              {ι : K ⟶ X} →
                                {hι : CategoryTheory.CategoryStruct.comp ι p = 0} →
                                  CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι ι hι) →
                                    CochainComplex.HomComplex.Cochain Q K 1
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.SInt
Int8.reduceOfInt : Lean.Meta.Simp.DSimproc
-- Mathlib.Tactic.Ring.Common
/-- Multiplies two polynomials `va, vb` together to get a normalized result polynomial.

* `0 * b = 0`
* `(a₁ + a₂) * b = (a₁ * b) + (a₂ * b)`
 -/
Mathlib.Tactic.Ring.Common.evalMul : {u : Lean.Level} →
  {α : Q(Type u)} →
    {bt : Q(«$α») → Type} →
      {sα : Q(CommSemiring «$α»)} →
        Mathlib.Tactic.Ring.Common.RingCompute bt sα →
          Mathlib.Tactic.Ring.Common.RingCompute Mathlib.Tactic.Ring.Common.btℕ Mathlib.Tactic.Ring.Common.sℕ →
            {a b : Q(«$α»)} →
              Mathlib.Tactic.Ring.Common.ExSum bt sα a →
                Mathlib.Tactic.Ring.Common.ExSum bt sα b →
                  Lean.MetaM (Mathlib.Tactic.Ring.Common.Result (Mathlib.Tactic.Ring.Common.ExSum bt sα) q(«$a» * «$b»))
-- Init.Data.String.Basic
String.eq_singleton_append : ∀ {s : String} (h : s.startPos ≠ s.endPos), ∃ t, s = String.singleton (s.startPos.get h) ++ t
-- Lean.Meta.Tactic.Simp.Types
/-- Save current cache, reset it, execute `x`, and then restore original cache.
 -/
Lean.Meta.Simp.withFreshCache : {α : Type} → Lean.Meta.SimpM α → Lean.Meta.SimpM α
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.toProd_pf : ∀ {R : Type u_1} [inst : CommSemiring R] {a a' : R}, a = a' → ∀ {e : ℕ}, Nat.rawCast 1 = e → a = a' ^ e * Nat.rawCast 1
-- Batteries.Data.Nat.Bitwise.Lemmas
Nat.or_self_left : ∀ (a b : ℕ), a ||| (a ||| b) = a ||| b
-- Mathlib.Algebra.Order.Module.Defs
IsOrderedModule.mk : ∀ {α : Type u_1} {β : Type u_2} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : Preorder β] [inst_3 : Zero α]
  [inst_4 : Zero β] [toPosSMulMono : PosSMulMono α β] [toSMulPosMono : SMulPosMono α β], IsOrderedModule α β
-- Lean.Expr
/-- Uses `binderNames?` to update the binder names of the corresponding lambda and forall expressions.
 -/
Lean.Expr.updateBinderNames : Lean.Expr → List (Option Lean.Name) → Lean.Expr
-- Mathlib.Order.LiminfLimsup
/-- Same as `limsup_const` applied to `⊤` but without the `NeBot f` assumption  -/
Filter.liminf_const_top : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {f : Filter β}, Filter.liminf (fun x => ⊤) f = ⊤
-- Mathlib.RingTheory.Localization.Submodule
IsLocalization.instIsNoetherianRingLocalization : ∀ {R : Type u_3} [inst : CommRing R] [IsNoetherianRing R] (S : Submonoid R), IsNoetherianRing (Localization S)
-- Mathlib.Order.ConditionallyCompletePartialOrder.Defs
ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf : {α : Type u_3} → [self : ConditionallyCompletePartialOrder α] → ConditionallyCompletePartialOrderInf α
-- Mathlib.RingTheory.WittVector.Isocrystal
WittVector.IsocrystalHom.mk.injEq : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {k : Type u_1} [inst_1 : CommRing k] [inst_2 : CharP k p]
  [inst_3 : PerfectRing k p] {V : Type u_2} [inst_4 : AddCommGroup V] [inst_5 : WittVector.Isocrystal p k V]
  {V₂ : Type u_3} [inst_6 : AddCommGroup V₂] [inst_7 : WittVector.Isocrystal p k V₂]
  (toLinearMap : V →ₗ[FractionRing (WittVector p k)] V₂)
  (frob_equivariant :
    ∀ (x : V),
      (WittVector.Isocrystal.frobenius p k) (toLinearMap x) = toLinearMap ((WittVector.Isocrystal.frobenius p k) x))
  (toLinearMap_1 : V →ₗ[FractionRing (WittVector p k)] V₂)
  (frob_equivariant_1 :
    ∀ (x : V),
      (WittVector.Isocrystal.frobenius p k) (toLinearMap_1 x) =
        toLinearMap_1 ((WittVector.Isocrystal.frobenius p k) x)),
  ({ toLinearMap := toLinearMap, frob_equivariant := frob_equivariant } =
      { toLinearMap := toLinearMap_1, frob_equivariant := frob_equivariant_1 }) =
    (toLinearMap = toLinearMap_1)
-- Init.Data.SInt.Bitwise
Bool.toInt16.eq_1 : ∀ (b : Bool), b.toInt16 = if b = true then 1 else 0
-- Mathlib.Lean.Expr.Basic
/-- Given a proposition `ty` that is an `Eq`, `Iff`, or `HEq`, returns `(tyLhs, lhs, tyRhs, rhs)`,
where `lhs : tyLhs` and `rhs : tyRhs`,
and where `lhs` is related to `rhs` by the respective relation.

See also `Lean.Expr.iff?`, `Lean.Expr.eq?`, and `Lean.Expr.heq?`.  -/
Lean.Expr.sides? : Lean.Expr → Option (Lean.Expr × Lean.Expr × Lean.Expr × Lean.Expr)