mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Array.Lemmas
/-- Variant of `foldlM_reverse` with a side condition for the `stop` argument.  -/
Array.foldlM_reverse' : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] {xs : Array α} {f : β → α → m β} {b : β}
  {stop : ℕ}, stop = xs.size → Array.foldlM f b xs.reverse 0 stop = Array.foldrM (fun x y => f y x) b xs
-- Mathlib.Order.Filter.AtTopBot.Prod
Filter.prod_atBot_atBot_eq : ∀ {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β], Filter.atBot ×ˢ Filter.atBot = Filter.atBot
-- Mathlib.CategoryTheory.Comma.CardinalArrow
/-- The bijection `Arrow.{w} (ShrinkHoms C) ≃ Arrow C`.  -/
CategoryTheory.Arrow.shrinkHomsEquiv : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] →
      CategoryTheory.Arrow (CategoryTheory.ShrinkHoms.{u} C) ≃ CategoryTheory.Arrow C
-- Mathlib.Data.W.Constructions
/-- Lists are equivalent to their associated `WType`  -/
WType.equivList : (γ : Type u) → WType (WType.Listβ γ) ≃ List γ
-- Mathlib.LinearAlgebra.Lagrange
Lagrange.basis_eq_prod_sub_inv_mul_nodal_div : ∀ {F : Type u_1} [inst : Field F] {ι : Type u_2} [inst_1 : DecidableEq ι] {s : Finset ι} {v : ι → F} {i : ι},
  i ∈ s →
    Lagrange.basis s v i =
      Polynomial.C (Lagrange.nodalWeight s v i) * (Lagrange.nodal s v / (Polynomial.X - Polynomial.C (v i)))
-- Mathlib.Algebra.Polynomial.Homogenize
Polynomial.eval_eq_div_eval_toTupleMvPolynomial : ∀ {R : Type u_2} [inst : Field R] (p : Polynomial R) (x : R),
  Polynomial.eval x p =
    (MvPolynomial.eval ![x, 1]) (p.toTupleMvPolynomial 0) / (MvPolynomial.eval ![x, 1]) (p.toTupleMvPolynomial 1)
-- Init.Data.String.Pattern.Basic
String.Slice.Pattern.StrictForwardPattern.mk : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.ForwardPattern pat],
  (∀ {s : String.Slice} (h : s.isEmpty = false) (q : s.Pos),
      String.Slice.Pattern.ForwardPattern.skipPrefixOfNonempty? pat s h = some q → q ≠ s.startPos) →
    String.Slice.Pattern.StrictForwardPattern pat
-- Mathlib.Logic.Encodable.Basic
/-- A type with unique element is encodable. This is not an instance to avoid diamonds.  -/
Unique.encodable : {α : Type u_1} → [Unique α] → Encodable α
-- Mathlib.AlgebraicGeometry.StructureSheaf
/-- The functions satisfying `isLocallyFraction` form a submodule.  -/
AlgebraicGeometry.StructureSheaf.sectionsSubalgebraSubmodule : {R : Type u} →
  (M : Type u) →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) →
            Submodule (↥(AlgebraicGeometry.StructureSheaf.sectionsSubalgebra R U))
              ((x : ↥U) → AlgebraicGeometry.StructureSheaf.Localizations M ↑x)
-- Mathlib.Testing.Plausible.Functions
List.dlookup.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (a : α), List.dlookup a [] = none
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.coconeOfIsSplitEpi_pt : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] (f : X ⟶ Y) [inst_1 : CategoryTheory.IsSplitEpi f],
  (CategoryTheory.Limits.coconeOfIsSplitEpi f).pt = Y
-- Mathlib.Combinatorics.SimpleGraph.LapMatrix
SimpleGraph.linearIndependent_lapMatrix_ker_basis_aux : ∀ {V : Type u_1} [inst : Fintype V] (G : SimpleGraph V) [inst_1 : DecidableRel G.Adj] [inst_2 : DecidableEq V]
  [inst_3 : DecidableEq G.ConnectedComponent], LinearIndependent ℝ G.lapMatrix_ker_basis_aux
-- Mathlib.CategoryTheory.Subobject.Limits
CategoryTheory.Limits.imageSubobjectMap.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} {f : W ⟶ X}
  [inst_1 : CategoryTheory.Limits.HasImage f] {g : Y ⟶ Z} [inst_2 : CategoryTheory.Limits.HasImage g]
  (sq : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk g) [inst_3 : CategoryTheory.Limits.HasImageMap sq],
  CategoryTheory.Limits.imageSubobjectMap sq =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobjectIso f).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.map sq)
        (CategoryTheory.Limits.imageSubobjectIso g).inv)
-- Std.Data.DHashMap.Raw
Std.DHashMap.Raw.WF.emptyWithCapacity : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {c : ℕ}, (Std.DHashMap.Raw.emptyWithCapacity c).WF
-- Mathlib.Data.Matrix.Reflection
Matrix.Exists.eq_1 : ∀ {α : Type u_1} (x : ℕ) (x_1 : Matrix (Fin 0) (Fin x) α → Prop), Matrix.Exists x_1 = x_1 (Matrix.of ![])
-- Mathlib.Algebra.Algebra.Unitization
Unitization.instNonAssocRing : {R : Type u_1} →
  {A : Type u_2} →
    [inst : CommRing R] → [inst_1 : NonUnitalNonAssocRing A] → [Module R A] → NonAssocRing (Unitization R A)
-- Mathlib.Analysis.Fourier.ZMod
ZMod.stdAddChar.congr_simp : ∀ {N : ℕ} [inst : NeZero N], ZMod.stdAddChar = ZMod.stdAddChar
-- Mathlib.Algebra.Homology.HomologicalComplexLimits
/-- A functor `D ⥤ HomologicalComplex C c` preserves colimits of shape `J`
if for any `i`, `G ⋙ eval C c i` does.  -/
HomologicalComplex.preservesColimitsOfShape_of_eval : ∀ {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] {D : Type u_4} [inst_3 : CategoryTheory.Category.{v_3, u_4} D]
  (G : CategoryTheory.Functor D (HomologicalComplex C c)),
  (∀ (i : ι), CategoryTheory.Limits.PreservesColimitsOfShape J (G.comp (HomologicalComplex.eval C c i))) →
    CategoryTheory.Limits.PreservesColimitsOfShape J G
-- Init.Data.UInt.Bitwise
USize.xor_self : ∀ {a : USize}, a ^^^ a = 0
-- Init.Data.Array.Lex.Lemmas
Array.not_lt_empty : ∀ {α : Type u_1} [inst : LT α] (xs : Array α), ¬xs < #[]
-- Init.Grind.AC
Lean.Grind.AC.Seq.denote_insert : ∀ {α : Sort u_1} (ctx : Lean.Grind.AC.Context α) {inst₁ : Std.Associative ctx.op} {inst₂ : Std.Commutative ctx.op}
  (x : Lean.Grind.AC.Var) (s : Lean.Grind.AC.Seq),
  Lean.Grind.AC.Seq.denote ctx (Lean.Grind.AC.Seq.insert x s) =
    ctx.op (Lean.Grind.AC.Var.denote ctx x) (Lean.Grind.AC.Seq.denote ctx s)
-- Mathlib.Analysis.BoxIntegral.Box.Basic
BoxIntegral.Box.mk.congr_simp : ∀ {ι : Type u_2} (lower lower_1 : ι → ℝ) (e_lower : lower = lower_1) (upper upper_1 : ι → ℝ) (e_upper : upper = upper_1)
  (lower_lt_upper : ∀ (i : ι), lower i < upper i),
  { lower := lower, upper := upper, lower_lt_upper := lower_lt_upper } =
    { lower := lower_1, upper := upper_1, lower_lt_upper := ⋯ }
-- Lean.Level
Lean.Level.find? : Lean.Level → (Lean.Level → Bool) → Option Lean.Level
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
CategoryTheory.Limits.Cotrident.condition_assoc : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)} (j₁ j₂ : J)
  (t : CategoryTheory.Limits.Cotrident f) {Z : C}
  (h :
    ((CategoryTheory.Functor.const (CategoryTheory.Limits.WalkingParallelFamily J)).obj t.pt).obj
        CategoryTheory.Limits.WalkingParallelFamily.one ⟶
      Z),
  CategoryTheory.CategoryStruct.comp (f j₁) (CategoryTheory.CategoryStruct.comp t.π h) =
    CategoryTheory.CategoryStruct.comp (f j₂) (CategoryTheory.CategoryStruct.comp t.π h)
-- Mathlib.Topology.Constructible
IsRetrocompact.isLocallyConstructible : ∀ {X : Type u_2} [inst : TopologicalSpace X] {U : Set X},
  IsOpen U → IsRetrocompact U → Topology.IsLocallyConstructible U
-- Mathlib.Algebra.Group.Basic
SubtractionMonoid.toSubNegZeroMonoid.eq_1 : ∀ {α : Type u_1} [inst : SubtractionMonoid α],
  SubtractionMonoid.toSubNegZeroMonoid = { toSubNegMonoid := inst.toSubNegMonoid, neg_zero := ⋯ }
-- Mathlib.Algebra.Group.Subsemigroup.Defs
/-- The actual `AddSubsemigroup` obtained from an element of a
`AddMemClass`  -/
AddSubsemigroup.ofClass : {S : Type u_3} → {M : Type u_4} → [inst : Add M] → [inst_1 : SetLike S M] → [AddMemClass S M] → S → AddSubsemigroup M
-- Init.Data.Int.DivMod.Lemmas
Int.neg_add_emod_self : ∀ (a b : ℤ), (-a + b) % a = b % a
-- Mathlib.Order.Filter.IsBounded
Filter.IsBounded.mono : ∀ {α : Type u_1} {r : α → α → Prop} {f g : Filter α}, f ≤ g → Filter.IsBounded r g → Filter.IsBounded r f
-- Mathlib.CategoryTheory.Limits.Creates
CategoryTheory.LiftsToColimit.mk.sizeOf_spec : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] {K : CategoryTheory.Functor J C}
  {F : CategoryTheory.Functor C D} {c : CategoryTheory.Limits.Cocone (K.comp F)} {t : CategoryTheory.Limits.IsColimit c}
  [inst_3 : SizeOf C] [inst_4 : SizeOf D] [inst_5 : SizeOf J] (toLiftableCocone : CategoryTheory.LiftableCocone K F c)
  (makesColimit : CategoryTheory.Limits.IsColimit toLiftableCocone.liftedCocone),
  sizeOf { toLiftableCocone := toLiftableCocone, makesColimit := makesColimit } =
    1 + sizeOf toLiftableCocone + sizeOf makesColimit
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
MeasureTheory.ProbabilityMeasure.continuous_lintegral_continuousMap : ∀ {X : Type u_2} [inst : TopologicalSpace X] [CompactSpace X] [inst_2 : MeasurableSpace X]
  [inst_3 : OpensMeasurableSpace X] {F : Type u_3} [inst_4 : FunLike F X NNReal] [ContinuousMapClass F X NNReal]
  (f : F), Continuous fun μ => ∫⁻ (x : X), ↑(f x) ∂↑μ
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getD_erase_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α} {fallback : β k}, (t.erase k).getD k fallback = fallback
-- Lean.Parser.Term
Lean.Parser.Termination.suffix.formatter : Lean.PrettyPrinter.Formatter
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKey?_insertEntry : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] {k : α} {v : β k}
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.minKey? (Std.Internal.List.insertEntry k v l) =
      some ((Std.Internal.List.minKey? l).elim k fun k' => if (compare k k').isLE = true then k else k')
-- Mathlib.Algebra.Ring.Idempotent
/-- If idempotent `a` and element `b` anti-commute, then their product is zero.  -/
IsIdempotentElem.mul_eq_zero_of_anticommute : ∀ {R : Type u_1} {a b : R} [inst : NonUnitalSemiring R] [IsAddTorsionFree R],
  IsIdempotentElem a → a * b + b * a = 0 → a * b = 0
-- Lean.Meta.Sym.DSimp.DSimpM
Lean.Meta.Sym.DSimp.instNonemptyMethodsRef : Nonempty Lean.Meta.Sym.DSimp.MethodsRef
-- Mathlib.LinearAlgebra.AffineSpace.Midpoint
midpoint_pointReflection_right : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : Invertible 2] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] (x y : P), midpoint R y ((Equiv.pointReflection x) y) = x
-- Mathlib.Logic.Function.Conjugate
/-- If `f` semiconjugates `ga` to `gb` and `ga'` to `gb'`,
then it semiconjugates `ga ∘ ga'` to `gb ∘ gb'`.  -/
Function.Semiconj.comp_right : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {ga ga' : α → α} {gb gb' : β → β},
  Function.Semiconj f ga gb → Function.Semiconj f ga' gb' → Function.Semiconj f (ga ∘ ga') (gb ∘ gb')
-- Mathlib.Topology.Constructions
IsClosed.isClosedMap_subtype_val : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, IsClosed s → IsClosedMap Subtype.val
-- Lean.Meta.Tactic.Grind.EMatchTheorem
/-- `checkCoverage` succeeded  -/
Lean.Meta.Grind.CheckCoverageResult.ok : Lean.Meta.Grind.CheckCoverageResult
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
AlgebraicGeometry.Proj.basicOpenIsoSpec_inv_ι : ∀ {σ : Type u_1} {A : Type u} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] (f : A) {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.basicOpenIsoSpec 𝒜 f f_deg hm).inv
      (AlgebraicGeometry.Proj.basicOpen 𝒜 f).ι =
    AlgebraicGeometry.Proj.awayι 𝒜 f f_deg hm
-- Init.Data.Ord.Basic
/-- Compare two elements in `α` using the comparator contained in an `[Ord α]` instance.  -/
Ord.compare : {α : Type u} → [self : Ord α] → α → α → Ordering
-- Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
LiouvilleWith.add_nat_iff : ∀ {p x : ℝ} {n : ℕ}, LiouvilleWith p (x + ↑n) ↔ LiouvilleWith p x
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
SSet.Subcomplex.PairingCore.injective_type₁ : ∀ {X : SSet} {A : X.Subcomplex} (h : A.PairingCore), Function.Injective h.type₁
-- Mathlib.LinearAlgebra.Matrix.DotProduct
/-- Note that this applies to `ℂ` via `RCLike.toStarOrderedRing`.  -/
Matrix.dotProduct_self_star_pos_iff : ∀ {n : Type u_2} {R : Type u_4} [inst : Fintype n] [inst_1 : PartialOrder R] [inst_2 : NonUnitalRing R]
  [inst_3 : StarRing R] [StarOrderedRing R] [NoZeroDivisors R] {v : n → R}, 0 < v ⬝ᵥ star v ↔ v ≠ 0
-- Init.Data.Range.Polymorphic.Lemmas
_private.Init.Data.Range.Polymorphic.Lemmas.0.Std.Rii.Internal.toArray_eq_toArray_iter : ∀ {α : Type u} [inst : Std.PRange.Least? α] [inst_1 : Std.PRange.UpwardEnumerable α] [inst_2 : Std.Rxi.IsAlwaysFinite α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] {r : Std.Rii α}, r.toArray = (Std.Rii.Internal.iter r).toArray
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.ShortComplex.HomologyMapData.map_right : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {S₁ S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂}
  {h₁ : S₁.HomologyData} {h₂ : S₂.HomologyData} (ψ : CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂)
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] [inst_5 : h₁.left.IsPreservedBy F]
  [inst_6 : h₁.right.IsPreservedBy F] [inst_7 : h₂.left.IsPreservedBy F] [inst_8 : h₂.right.IsPreservedBy F],
  (ψ.map F).right = ψ.right.map F
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
/-- **Alias** of the forward direction of `ValuativeRel.veq_comm`. -/
ValuativeRel.veq.symm : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] {x y : R}, x =ᵥ y → y =ᵥ x
-- Mathlib.Geometry.Manifold.Algebra.SMul
ContMDiffSMul.contMDiff_const_smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {H' : Type u_4}
  [inst_4 : TopologicalSpace H'] {E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  {I' : ModelWithCorners 𝕜 E' H'} {G : Type u_8} [inst_7 : TopologicalSpace G] [inst_8 : ChartedSpace H G]
  {M : Type u_9} [inst_9 : TopologicalSpace M] [inst_10 : ChartedSpace H' M] [inst_11 : SMul G M] {n : WithTop ℕ∞}
  [ContMDiffSMul I I' n G M] (g : G), ContMDiff I' I' n fun x => g • x
-- Std.Data.Internal.List.Associative
Std.Internal.List.DistinctKeys.modifyKey : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {a : α} {f : β a → β a}
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l → Std.Internal.List.DistinctKeys (Std.Internal.List.modifyKey a f l)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
/-- Coefficients use to reproduce the leading coefficient of a polynomial given its values on the
Chebyshev nodes.  -/
_private.Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal.0.Polynomial.Chebyshev.leadingCoeffC : ℕ → ℕ → ℝ
-- Mathlib.Data.Finsupp.Basic
Finsupp.support_extendDomain_subset : ∀ {α : Type u_1} {M : Type u_12} [inst : Zero M] {P : α → Prop} [inst_1 : DecidablePred P] (f : Subtype P →₀ M),
  ↑f.extendDomain.support ⊆ {x | P x}
-- Mathlib.NumberTheory.ModularForms.Petersson
UpperHalfPlane.petersson_slash : ∀ (k : ℤ) (f f' : UpperHalfPlane → ℂ) (g : GL (Fin 2) ℝ) (τ : UpperHalfPlane),
  UpperHalfPlane.petersson k (SlashAction.map k g f) (SlashAction.map k g f') τ =
    ↑|↑(Matrix.GeneralLinearGroup.det g)| ^ (k - 2) * (UpperHalfPlane.σ g) (UpperHalfPlane.petersson k f f' (g • τ))
-- Lean.Util.FindExpr
Lean.Expr.find? : (Lean.Expr → Bool) → Lean.Expr → Option Lean.Expr
-- Mathlib.Data.Nat.Prime.Basic
Nat.coprime_of_lt_prime : ∀ {n p : ℕ}, n ≠ 0 → n < p → Nat.Prime p → p.Coprime n
-- Init.Data.BitVec.Lemmas
BitVec.toNat_one : ∀ {w : ℕ}, 0 < w → (1#w).toNat = 1
-- Lean.PrettyPrinter.Delaborator.Options
Lean.getPPFieldNotation : Lean.Options → Bool
-- Lean.Elab.App
Lean.Elab.Term.ElabAppArgs.M : Type → Type
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
/-- The generic case of the first simplicial identity  -/
SimplexCategory.δ_comp_δ : ∀ {n : ℕ} {i j : Fin (n + 2)},
  i ≤ j →
    CategoryTheory.CategoryStruct.comp (SimplexCategory.δ i) (SimplexCategory.δ j.succ) =
      CategoryTheory.CategoryStruct.comp (SimplexCategory.δ j) (SimplexCategory.δ i.castSucc)
-- Lean.Expr
/-- Return true if the given expression is the function of an expression that is target for (head) beta reduction.
If `useZeta = true`, then `let`-expressions are visited. That is, it assumes
that zeta-reduction (aka let-expansion) is going to be used.

See `isHeadBetaTarget`.
 -/
Lean.Expr.isHeadBetaTargetFn : Bool → Lean.Expr → Bool
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.zeroLocus_ideal_mem_irreducibleComponents : ∀ {R : Type u} [inst : CommSemiring R] {I : Ideal R},
  PrimeSpectrum.zeroLocus ↑I ∈ irreducibleComponents (PrimeSpectrum R) ↔ I.radical ∈ minimalPrimes R
-- Std.Data.Iterators.Combinators.Monadic.Zip
Std.Iterators.Types.Zip.PlausibleStep.doneLeft : ∀ {m : Type w → Type w'} {α₁ β₁ : Type w} [inst : Std.Iterator α₁ m β₁] {α₂ β₂ : Type w} [inst_1 : Std.Iterator α₂ m β₂]
  {it : Std.IterM m (β₁ × β₂)},
  it.internalState.memoizedLeft = none →
    it.internalState.left.IsPlausibleStep Std.IterStep.done → Std.Iterators.Types.Zip.PlausibleStep it Std.IterStep.done
-- Mathlib.Data.ENNReal.Real
ENNReal.trichotomy₂ : ∀ {p q : ENNReal},
  p ≤ q →
    p = 0 ∧ q = 0 ∨
      p = 0 ∧ q = ⊤ ∨
        p = 0 ∧ 0 < q.toReal ∨ p = ⊤ ∧ q = ⊤ ∨ 0 < p.toReal ∧ q = ⊤ ∨ 0 < p.toReal ∧ 0 < q.toReal ∧ p.toReal ≤ q.toReal
-- Mathlib.Algebra.Ring.Subsemiring.Basic
RingHom.coe_restrict_apply : ∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] {σR : Type u_1} {σS : Type u_2}
  [inst_2 : SetLike σR R] [inst_3 : SetLike σS S] [inst_4 : SubsemiringClass σR R] [inst_5 : SubsemiringClass σS S]
  (f : R →+* S) (s' : σR) (s : σS) (h : ∀ x ∈ s', f x ∈ s) (x : ↥s'), ↑((f.restrict s' s h) x) = f ↑x
-- Batteries.Data.String.Lemmas
/-- The UTF-8 byte length of a list of characters. (This is intended for specification purposes.)  -/
String.utf8Len : List Char → ℕ
-- Init.Grind.Ring.Field
Lean.Grind.Field.natCast_div_of_dvd : ∀ {α : Type u_1} [inst : Lean.Grind.Field α] {x y : ℕ}, y ∣ x → ↑y ≠ 0 → ↑(x / y) = ↑x / ↑y
-- Mathlib.Logic.Equiv.Prod
Equiv.sumProdDistrib_symm_apply_right : ∀ {α : Type u_9} {β : Type u_10} {γ : Type u_11} (b : β × γ),
  (Equiv.sumProdDistrib α β γ).symm (Sum.inr b) = (Sum.inr b.1, b.2)
-- Mathlib.Algebra.Group.TypeTags.Hom
AddMonoidHom.toMultiplicativeLeft_apply_apply : ∀ {α : Type u_3} {β : Type u_4} [inst : AddZeroClass α] [inst_1 : MulOneClass β] (f : α →+ Additive β)
  (a : Multiplicative α), (AddMonoidHom.toMultiplicativeLeft f) a = Additive.toMul (f (Multiplicative.toAdd a))
-- Mathlib.Data.Fintype.Card
Fintype.card_lt_of_injective_not_surjective : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : Fintype β] (f : α → β),
  Function.Injective f → ¬Function.Surjective f → Fintype.card α < Fintype.card β
-- Mathlib.CategoryTheory.Limits.Shapes.Preorder.TransfiniteCompositionOfShape
CategoryTheory.TransfiniteCompositionOfShape.iic_isoBot : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : LinearOrder J] [inst_2 : OrderBot J]
  {X Y : C} {f : X ⟶ Y} [inst_3 : SuccOrder J] [inst_4 : WellFoundedLT J]
  (c : CategoryTheory.TransfiniteCompositionOfShape J f) (j : J),
  (c.iic j).isoBot = CategoryTheory.Iso.refl ((⋯.functor.comp c.F).obj ⊥)
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_id : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] {d d' : D} (f : d ⟶ d') (c : C),
  CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom f (CategoryTheory.CategoryStruct.id c) =
    CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft f c
-- Mathlib.Analysis.Convex.Star
StarConvex.prod : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid F] [inst_4 : SMul 𝕜 E] [inst_5 : SMul 𝕜 F] {x : E} {y : F} {s : Set E} {t : Set F},
  StarConvex 𝕜 x s → StarConvex 𝕜 y t → StarConvex 𝕜 (x, y) (s ×ˢ t)
-- Init.Data.Slice.Array.Lemmas
Subarray.size_take : ∀ {α : Type u_1} {i : ℕ} {xs : Subarray α}, Std.Slice.size (xs.take i) = min i (Std.Slice.size xs)
-- Mathlib.Data.ENNReal.Basic
ENNReal.max_eq_zero_iff : ∀ {a b : ENNReal}, max a b = 0 ↔ a = 0 ∧ b = 0
-- Mathlib.GroupTheory.GroupAction.Blocks
AddAction.IsFixedBlock.eq_1 : ∀ (G : Type u_1) {X : Type u_2} [inst : VAdd G X] (B : Set X), AddAction.IsFixedBlock G B = ∀ (g : G), g +ᵥ B = B
-- Mathlib.Analysis.Normed.MulAction
Metric.smul_image_sphere : ∀ {α : Type u_1} {β : Type u_2} [inst : NormedDivisionRing α] [inst_1 : SeminormedAddCommGroup β] [inst_2 : Module α β]
  [NormSMulClass α β] {s : α},
  s ≠ 0 → ∀ (x : β) (ε : ℝ), (fun x => s • x) '' Metric.sphere x ε = Metric.sphere (s • x) (‖s‖ * ε)
-- Mathlib.LinearAlgebra.Dimension.RankNullity
HasRankNullity.mk : ∀ {R : Type v} [inst : Ring R],
  (∀ (M : Type u) [inst_1 : AddCommGroup M] [inst_2 : Module R M],
      ∃ s, Cardinal.mk ↑s = Module.rank R M ∧ LinearIndepOn R id s) →
    (∀ {M : Type u} [inst_1 : AddCommGroup M] [inst_2 : Module R M] (N : Submodule R M),
        Module.rank R (M ⧸ N) + Module.rank R ↥N = Module.rank R M) →
      HasRankNullity.{u, v} R
-- Mathlib.Algebra.Homology.Augment
CochainComplex.truncate_obj_X : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  (C : CochainComplex V ℕ) (i : ℕ), (CochainComplex.truncate.obj C).X i = C.X (i + 1)
-- Mathlib.Combinatorics.Additive.Convolution
Finset.convolution_ne_zero : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {A B : Finset G} {x : G}, A.convolution B x ≠ 0 ↔ x ∈ A * B
-- Mathlib.RingTheory.TensorProduct.MvPolynomial
MvPolynomial.tensorEquivSum_one_tmul_C : ∀ {R : Type u} [inst : CommSemiring R] {σ : Type u_1} {ι : Type u_2} {S : Type u_3} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] (r : R),
  (MvPolynomial.tensorEquivSum R σ ι S) (1 ⊗ₜ[R] MvPolynomial.C r) = MvPolynomial.C ((algebraMap R S) r)
-- Mathlib.Data.Num.Basic
/-- The negation of a `ZNum`.  -/
ZNum.zNeg : ZNum → ZNum
-- Mathlib.CategoryTheory.Adjunction.Mates
/-- If `α` is a natural transformation between right adjoints whose conjugate natural transformation is
an isomorphism, then `α` is an isomorphism. The converse is given in `conjugateEquiv_symm_iso`.
 -/
CategoryTheory.conjugateEquiv_symm_of_iso : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L₁ L₂ : CategoryTheory.Functor C D} {R₁ R₂ : CategoryTheory.Functor D C} (adj₁ : L₁ ⊣ R₁) (adj₂ : L₂ ⊣ R₂)
  (α : R₁ ⟶ R₂) [CategoryTheory.IsIso ((CategoryTheory.conjugateEquiv adj₁ adj₂).symm α)], CategoryTheory.IsIso α