mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.Cofork.app_zero_eq_comp_π_right_assoc : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} (s : CategoryTheory.Limits.Cofork f g)
  {Z : C}
  (h :
    ((CategoryTheory.Functor.const CategoryTheory.Limits.WalkingParallelPair).obj s.pt).obj
        CategoryTheory.Limits.WalkingParallelPair.zero ⟶
      Z),
  CategoryTheory.CategoryStruct.comp (s.ι.app CategoryTheory.Limits.WalkingParallelPair.zero) h =
    CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.comp s.π h)
-- Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
EReal.expOrderIso_apply : ∀ (x : EReal), EReal.expOrderIso x = x.exp
-- Std.Net.Addr
Std.Net.instDecidableEqInterfaceAddress.decEq : (x x_1 : Std.Net.InterfaceAddress) → Decidable (x = x_1)
-- Init.Data.Array.Lemmas
Array.size_extract : ∀ {α : Type u_1} {xs : Array α} {start stop : ℕ}, (xs.extract start stop).size = min stop xs.size - start
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
/-- action on 2-morphisms  -/
CategoryTheory.StrictlyUnitaryLaxFunctorCore.map₂ : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        (self : CategoryTheory.StrictlyUnitaryLaxFunctorCore B C) →
          {a b : B} → {f g : a ⟶ b} → (f ⟶ g) → (self.map f ⟶ self.map g)
-- Mathlib.FieldTheory.SeparableDegree
/-- If `g` is a separable contraction of `f`, then the separable degree of `f` is equal to
the degree of `g`.  -/
Polynomial.IsSeparableContraction.natSepDegree_eq : ∀ {F : Type u} [inst : Field F] {f g : Polynomial F} {q : ℕ} [ExpChar F q],
  Polynomial.IsSeparableContraction q f g → f.natSepDegree = g.natDegree
-- Init.Data.Char.Ordinal
Char.ordinal_le_of_le : ∀ {c d : Char}, c ≤ d → c.ordinal ≤ d.ordinal
-- Init.Data.String.Termination
String.Slice.Pos.inner_down : ∀ {s : String.Slice} {p : s.Pos}, p.down.inner = p
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.maxKey!_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {k : α} {v : β},
  (t.insertIfNew k v).maxKey! = t.maxKey?.elim k fun k' => if cmp k' k = Ordering.lt then k else k'
-- Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
ContinuousLinearMap.isUniformAddGroup : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_4}
  {F : Type u_5} [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜₁ E] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜₂ F]
  [inst_6 : TopologicalSpace E] [inst_7 : UniformSpace F] [inst_8 : IsUniformAddGroup F], IsUniformAddGroup (E →SL[σ] F)
-- Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits
/-- **Alias** of `IsPrimitiveRoot.nthRootsFinset_pairwise_associated_sub_one_sub_of_prime`.

---

If `p` is prime and `ζ` is a `p`-th primitive root of unity, then `ζ - 1` and `η₁ - η₂` are
associated for all distinct `p`-th roots of unity `η₁` and `η₂`.  -/
IsPrimitiveRoot.ntRootsFinset_pairwise_associated_sub_one_sub_of_prime : ∀ {p : ℕ} {A : Type u_1} {ζ : A} [inst : CommRing A] [inst_1 : IsDomain A],
  IsPrimitiveRoot ζ p →
    Nat.Prime p → (↑(Polynomial.nthRootsFinset p 1)).Pairwise fun η₁ η₂ => Associated (ζ - 1) (η₁ - η₂)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Udiv
Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.BlastUdivOutput.mk.inj : ∀ {α : Type} {inst : Hashable α} {inst_1 : DecidableEq α} {old : Std.Sat.AIG α} {w : ℕ} {aig : Std.Sat.AIG α}
  {q r : aig.RefVec w} {hle : old.decls.size ≤ aig.decls.size} {aig_1 : Std.Sat.AIG α} {q_1 r_1 : aig_1.RefVec w}
  {hle_1 : old.decls.size ≤ aig_1.decls.size},
  { aig := aig, q := q, r := r, hle := hle } = { aig := aig_1, q := q_1, r := r_1, hle := hle_1 } →
    aig = aig_1 ∧ q ≍ q_1 ∧ r ≍ r_1
-- Mathlib.RingTheory.Multiplicity
emultiplicity_pow_self_of_prime : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [IsCancelMulZero α] {p : α},
  Prime p → ∀ (n : ℕ), emultiplicity p (p ^ n) = ↑n
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.not_isSuccLimit_natCast : ∀ (n : ℕ), ¬Order.IsSuccLimit ↑n
-- Mathlib.Analysis.Real.Cardinality
Cardinal.Real.Ico_countable_iff : ∀ {x y : ℝ}, (Set.Ico x y).Countable ↔ y ≤ x
-- Mathlib.Order.SuccPred.Basic
Order.le_succ_iterate : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] (k : ℕ) (x : α), x ≤ Order.succ^[k] x
-- Init.WF
acc_transGen_iff : ∀ {α : Sort u_1} {r : α → α → Prop} {a : α}, Acc (Relation.TransGen r) a ↔ Acc r a
-- Init.Data.List.Lemmas
List.flatMap_id' : ∀ {α : Type u_1} {L : List (List α)}, List.flatMap (fun as => as) L = L.flatten
-- Mathlib.Combinatorics.Additive.VerySmallDoubling
_private.Mathlib.Combinatorics.Additive.VerySmallDoubling.0.Finset.weaken_doubling : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {A : Finset G},
  ↑(A * A).card < 3 / 2 * ↑A.card → (A * A).card < 2 * A.card
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic
/-- The `n`-th Chebyshev polynomial of the first kind evaluates on `cosh θ` to the
value `cosh (n * θ)`.  -/
Polynomial.Chebyshev.T_complex_cosh : ∀ (θ : ℂ) (n : ℤ), Polynomial.eval (Complex.cosh θ) (Polynomial.Chebyshev.T ℂ n) = Complex.cosh (↑n * θ)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.yonedaAddGrp_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (G : CategoryTheory.AddGrp C), CategoryTheory.yonedaAddGrp.obj G = CategoryTheory.yonedaAddGrpObj G.X
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.edgeSet_top : ∀ {V : Type u}, ⊤.edgeSet = Sym2.diagSetᶜ
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Associates.bcount.congr_simp : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] {inst_1 : DecidableEq (Associates α)}
  [inst_2 : DecidableEq (Associates α)] (p p_1 : { a // Irreducible a }),
  p = p_1 → ∀ (a a_1 : Associates.FactorSet α), a = a_1 → Associates.bcount p a = Associates.bcount p_1 a_1
-- Mathlib.Topology.Semicontinuity.Basic
IsClosed.lowerSemicontinuousWithinAt_indicator : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {s t : Set α} {x : α} {y : β} [inst_1 : Zero β]
  [inst_2 : Preorder β], IsClosed s → y ≤ 0 → LowerSemicontinuousWithinAt (s.indicator fun _x => y) t x
-- Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
tendsto_rpow_atBot_of_base_gt_one : ∀ (b : ℝ), 1 < b → Filter.Tendsto (fun x => b ^ x) Filter.atBot (nhds 0)
-- Mathlib.MeasureTheory.Integral.PeakFunction
/-- Consider a nonnegative function `φ` with integral one, decaying quickly enough at infinity.
Then suitable renormalizations of `φ` form a sequence of peak functions around the origin:
`∫ (c ^ d * φ (c • x)) • g x` converges to `g 0` as `c → ∞` if `g` is continuous at `0`
and integrable.  -/
tendsto_integral_comp_smul_smul_of_integrable : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {F : Type u_4}
  [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [FiniteDimensional ℝ F] [inst_6 : MeasurableSpace F]
  [BorelSpace F] {μ : MeasureTheory.Measure F} [μ.IsAddHaarMeasure] {φ : F → ℝ},
  (∀ (x : F), 0 ≤ φ x) →
    ∫ (x : F), φ x ∂μ = 1 →
      Filter.Tendsto (fun x => ‖x‖ ^ Module.finrank ℝ F * φ x) (Bornology.cobounded F) (nhds 0) →
        ∀ {g : F → E},
          MeasureTheory.Integrable g μ →
            ContinuousAt g 0 →
              Filter.Tendsto (fun c => ∫ (x : F), (c ^ Module.finrank ℝ F * φ (c • x)) • g x ∂μ) Filter.atTop
                (nhds (g 0))
-- Mathlib.Algebra.Exact.Basic
Function.MulExact.comp_injective : ∀ {M : Type u_2} {N : Type u_4} {P : Type u_6} {P' : Type u_7} {f : M → N} {g : N → P} (g' : P → P') [inst : One P]
  [inst_1 : One P'], Function.MulExact f g → Function.Injective g' → g' 1 = 1 → Function.MulExact f (g' ∘ g)
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.hasCodetector_op_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C],
  CategoryTheory.HasCodetector Cᵒᵖ ↔ CategoryTheory.HasDetector C
-- Mathlib.Computability.Partrec
Computable.vector_ofFn : ∀ {α : Type u_1} {σ : Type u_4} [inst : Primcodable α] [inst_1 : Primcodable σ] {n : ℕ} {f : Fin n → α → σ},
  (∀ (i : Fin n), Computable (f i)) → Computable fun a => List.Vector.ofFn fun i => f i a
-- Mathlib.RingTheory.NonUnitalSubring.Defs
/-- Copy of a non-unital subring with a new `carrier` equal to the old one. Useful to fix
definitional equalities.  -/
NonUnitalSubring.copy : {R : Type u} → [inst : NonUnitalNonAssocRing R] → (S : NonUnitalSubring R) → (s : Set R) → s = ↑S → NonUnitalSubring R
-- Lean.Data.SMap
Lean.SMap.iter : {α : Type u} → {β : Type v} → [inst : BEq α] → [inst_1 : Hashable α] → Lean.SMap α β → Std.Iter (α × β)
-- Std.Time.Format.Modifier
/-- `classify` classifies the number of pattern letters into an `OffsetZ` format.
 -/
Std.Time.OffsetZ.classify : ℕ → Option Std.Time.OffsetZ
-- Mathlib.Topology.MetricSpace.Pseudo.Basic
Metric.isUniformInducing_iff : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {f : α → β},
  IsUniformInducing f ↔ UniformContinuous f ∧ ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, dist (f a) (f b) < ε → dist a b < δ
-- Mathlib.Order.Cover
exists_covBy_of_wellFoundedGT : ∀ {α : Type u_1} [inst : Preorder α] [wf : WellFoundedGT α] ⦃a : α⦄, ¬IsMin a → ∃ a', a' ⋖ a
-- Lean.Meta.Sym.Pattern
/-- If `zetaDelta` is `true`, then zeta-delta reduction is allowed.
That is, `isDefEqS` can unfold `x` if the local context contains `(x : t := v)`.
 -/
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.DefEqM.Context.zetaDelta : Lean.Meta.Sym.DefEqM.Context✝ → Bool
-- Init.Data.Vector.Find
Vector.find?_singleton : ∀ {α : Type} {a : α} {p : α → Bool}, Vector.find? p #v[a] = if p a = true then some a else none
-- Mathlib.Algebra.Lie.SerreConstruction
/-- The exceptional split Lie algebra of type e₇.  -/
LieAlgebra.e₇ : (R : Type u) → [CommRing R] → Type u
-- Mathlib.Algebra.Group.Subsemigroup.Operations
Subsemigroup.gc_map_comap : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] (f : M →ₙ* N),
  GaloisConnection (Subsemigroup.map f) (Subsemigroup.comap f)
-- Mathlib.Order.UpperLower.Basic
isLowerSet_empty : ∀ {α : Type u_1} [inst : LE α], IsLowerSet ∅
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.getKeyLT?_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp] {k : α},
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.getKeyLT? k = t₂.getKeyLT? k
-- Mathlib.MeasureTheory.Measure.EverywherePos
/-- In a space with an inner regular measure, any measurable set coincides almost everywhere with
its everywhere positive subset.  -/
MeasureTheory.Measure.everywherePosSubset_ae_eq : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α}
  [OpensMeasurableSpace α] [μ.InnerRegular], MeasurableSet s → μ.everywherePosSubset s =ᵐ[μ] s
-- Init.Data.Nat.Basic
Nat.sub_eq_iff_eq_add : ∀ {b a c : ℕ}, b ≤ a → (a - b = c ↔ a = c + b)
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.instInhabitedCode.default : Turing.ToPartrec.Code
-- Mathlib.Algebra.Order.Archimedean.Defs
exists_nat_ge : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : PartialOrder R] [IsOrderedRing R] [Archimedean R] (x : R), ∃ n, x ≤ ↑n
-- Lean.Elab.MutualDef
Lean.Elab.DefViewElabHeader.mk.sizeOf_spec : ∀ (toDefView : Lean.Elab.DefView) (toDefViewElabHeaderData : Lean.Elab.DefViewElabHeaderData)
  (tacSnap? : Option (Lean.Language.SnapshotBundle Lean.Elab.Tactic.TacticParsedSnapshot))
  (bodySnap? : Option (Lean.Language.SnapshotBundle (Option Lean.Elab.BodyProcessedSnapshot))),
  sizeOf
      { toDefView := toDefView, toDefViewElabHeaderData := toDefViewElabHeaderData, tacSnap? := tacSnap?,
        bodySnap? := bodySnap? } =
    1 + sizeOf toDefView + sizeOf toDefViewElabHeaderData + sizeOf tacSnap? + sizeOf bodySnap?
-- Lean.Meta.Tactic.Grind.EMatchAction
_private.Lean.Meta.Tactic.Grind.EMatchAction.0.Lean.Meta.Grind.Action.CollectState.thms : Lean.Meta.Grind.Action.CollectState✝ → Array Lean.Meta.Grind.EMatchTheorem
-- Mathlib.Algebra.Category.Ring.Limits
/-- A choice of limit cone for a functor into `CommRingCat`.
(Generally, you'll just want to use `limit F`.)
 -/
CommRingCat.limitCone : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J CommRingCat) →
      [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget CommRingCat)).sections] → CategoryTheory.Limits.Cone F
-- Mathlib.AlgebraicGeometry.ValuativeCriterion
/-- A morphism `f : X ⟶ Y` satisfies the uniqueness part of the valuative criterion if
every valuative commutative square over `f` has at most one lift.  -/
AlgebraicGeometry.ValuativeCriterion.Uniqueness : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme
-- Mathlib.MeasureTheory.Measure.Dirac
MeasureTheory.ae_eq_dirac : ∀ {α : Type u_1} {δ : Type u_3} [inst : MeasurableSpace α] [MeasurableSingletonClass α] {a : α} (f : α → δ),
  f =ᵐ[MeasureTheory.Measure.dirac a] Function.const α (f a)
-- Mathlib.NumberTheory.EulerProduct.DirichletLSeries
/-- When `χ` is a Dirichlet character and `s ≠ 0`, the map `n ↦ χ n * n^(-s)` is completely
multiplicative and vanishes at zero.  -/
dirichletSummandHom : {s : ℂ} → {n : ℕ} → DirichletCharacter ℂ n → s ≠ 0 → ℕ →*₀ ℂ
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
/-- Automorphism of `ℂ`: the identity if `0 < det g` and conjugation otherwise.  -/
UpperHalfPlane.σ : GL (Fin 2) ℝ → ℂ ≃A[ℝ] ℂ
-- Mathlib.RingTheory.MvPolynomial.Basic
MvPolynomial.instSmall : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] [Small.{u, u_2} R] [Small.{u, u_1} σ],
  Small.{u, max u_2 u_1} (MvPolynomial σ R)
-- Mathlib.Algebra.Order.GroupWithZero.Basic
/-- See also `lt_inv_of_lt_inv₀` for a one-sided implication with one fewer assumption.  -/
lt_inv_comm₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] [MulPosReflectLT G₀]
  {a b : G₀}, 0 < a → 0 < b → (a < b⁻¹ ↔ b < a⁻¹)
-- Init.Data.Int.DivMod.Bootstrap
Int.add_emod_eq_add_emod_right : ∀ {m n k : ℤ} (i : ℤ), m % n = k % n → (m + i) % n = (k + i) % n
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
IsEllipticNet.atomRel.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] (W : ℤ → R) (a b c d : ℤ),
  IsEllipticNet.atomRel W a b c d =
    IsEllipticNet.atom W a b * IsEllipticNet.atom W c d - IsEllipticNet.atom W a c * IsEllipticNet.atom W b d +
      IsEllipticNet.atom W a d * IsEllipticNet.atom W b c
-- Mathlib.MeasureTheory.MeasurableSpace.Instances
ENat.instMeasurableSingletonClass : MeasurableSingletonClass ℕ∞
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getKey_alter : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] [Inhabited α] {k k' : α} {f : Option β → Option β} (h : m.WF)
  {hc : k' ∈ Std.DHashMap.Raw.Const.alter m k f},
  (Std.DHashMap.Raw.Const.alter m k f).getKey k' hc = if heq : (k == k') = true then k else m.getKey k' ⋯
-- Std.Async.Basic
Std.Async.instMonadAwaitStateTOfMonad : {m t : Type → Type} → {n : Type} → [Monad m] → [Std.Async.MonadAwait t m] → Std.Async.MonadAwait t (StateT n m)
-- Mathlib.Order.Atoms
isCoatom_iff_ge_of_le : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : OrderTop α] {a : α},
  IsCoatom a ↔ a ≠ ⊤ ∧ ∀ (b : α), b ≠ ⊤ → a ≤ b → b ≤ a
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.Tactic.Specialize.imp_pure : ∀ {σs : List (Type u)} {φ : Prop} {P Q R : Std.Do.SPred σs} [Std.Do.SPred.Tactic.PropAsSPredTautology φ Q],
  φ → P ∧ (Q → R) ⊢ₛ P ∧ R
-- Init.Data.Array.Zip
_private.Init.Data.Array.Zip.0.Array.getElem?_zipWithAll.match_1.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (motive : Option α → Option β → Sort u_3) (a? : Option α) (b? : Option β)
  (h_1 : Unit → motive none none) (h_2 : (a? : Option α) → (b? : Option β) → motive a? b?),
  (a? = none → b? = none → False) →
    (match a?, b? with
      | none, none => h_1 ()
      | a?, b? => h_2 a? b?) =
      h_2 a? b?
-- Mathlib.SetTheory.ZFC.Ordinal
/-- **Alias** of `ZFSet.IsOrdinal.trichotomous`. -/
ZFSet.IsOrdinal.isTrichotomous : ∀ {x : ZFSet.{u}}, x.IsOrdinal → Std.Trichotomous (Subrel (fun x1 x2 => x1 ∈ x2) fun x_1 => x_1 ∈ x)
-- Mathlib.CategoryTheory.Monad.Equalizer
/-- The Beck fork is a split equalizer.  -/
CategoryTheory.Comonad.beckSplitEqualizer : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {T : CategoryTheory.Comonad C} → (X : T.Coalgebra) → CategoryTheory.IsSplitEqualizer (T.map X.a) (T.δ.app X.A) X.a
-- Init.Data.SInt.Lemmas
Int16.mul_two : ∀ {a : Int16}, a * 2 = a + a
-- Mathlib.Data.Fintype.BigOperators
Fintype.prod_extend_by_one : ∀ {α : Type u_1} {ι : Type u_4} [inst : DecidableEq ι] [inst_1 : Fintype ι] [inst_2 : CommMonoid α] (s : Finset ι)
  (f : ι → α), (∏ i, if i ∈ s then f i else 1) = ∏ i ∈ s, f i
-- Std.Tactic.Do.Syntax
/-- If set to `some n`, `mvcgen` will only do 42 steps of the VC generation procedure.
This is helpful for bisecting bugs in `mvcgen` and tracing its execution.
 -/
Lean.Elab.Tactic.Do.VCGen.Config.stepLimit : Lean.Elab.Tactic.Do.VCGen.Config → Option ℕ
-- Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated
CategoryTheory.Pretriangulated.Opposite.contractibleTriangleIso_hom_hom₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] (X : Cᵒᵖ),
  (CategoryTheory.Pretriangulated.Opposite.contractibleTriangleIso X).hom.hom₃ = (⋯.iso ⋯).hom
-- Mathlib.Topology.Instances.EReal.Lemmas
EReal.nhds_bot : nhds ⊥ = ⨅ a, ⨅ (_ : a ≠ ⊥), Filter.principal (Set.Iio a)
-- Mathlib.Analysis.Complex.Norm
Complex.dist_eq : ∀ (z w : ℂ), dist z w = ‖z - w‖
-- Init.Data.Slice.Array.Lemmas
Array.toArray_mkSlice_rci : ∀ {α : Type u_1} {xs : Array α} {lo : ℕ}, Std.Slice.toArray (Std.Rci.Sliceable.mkSlice xs lo...*) = xs.extract lo
-- Mathlib.CategoryTheory.Triangulated.Triangulated
CategoryTheory.Triangulated.Octahedron'.triangle_obj₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃}
  (comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃) {v₁₂ : Z₁₂ ⟶ X₁}
  {w₁₂ : X₂ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₁₂}
  (h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk v₁₂ u₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
  {v₂₃ : Z₂₃ ⟶ X₂} {w₂₃ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₂₃}
  (h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk v₂₃ u₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
  {v₁₃ : Z₁₃ ⟶ X₁} {w₁₃ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₁₃}
  (h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk v₁₃ u₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
  (h : CategoryTheory.Triangulated.Octahedron' comm h₁₂ h₂₃ h₁₃),
  (CategoryTheory.Triangulated.Octahedron'.triangle comm h₁₂ h₂₃ h₁₃ h).obj₁ = Z₁₂
-- Mathlib.Algebra.Polynomial.Div
/-- See `Polynomial.mul_self_modByMonic` for the other multiplication order. That version, unlike
this one, requires commutativity.  -/
Polynomial.self_mul_modByMonic : ∀ {R : Type u} [inst : Ring R] {p q : Polynomial R}, q.Monic → q * p %ₘ q = 0
-- Mathlib.Algebra.Order.Ring.WithTop
WithTop.eq_top_of_pow : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : MonoidWithZero α] [inst_2 : NoZeroDivisors α] [inst_3 : Nontrivial α]
  {x : WithTop α} (n : ℕ), x ^ n = ⊤ → x = ⊤
-- Mathlib.Topology.UniformSpace.Basic
UniformSpace.toTopologicalSpace_iInf : ∀ {α : Type ua} {ι : Sort u_2} {u : ι → UniformSpace α}, (iInf u).toTopologicalSpace = ⨅ i, (u i).toTopologicalSpace
-- Mathlib.Algebra.Algebra.Subalgebra.Tower
Subalgebra.disjoint_one_iff : ∀ (R : Type u) (A : Type w) [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Algebra R A]
  (S : Subalgebra R A) (I : Ideal A),
  Disjoint 1 (Submodule.restrictScalars (↥S) I) ↔ Disjoint (Subalgebra.toSubmodule S) (Submodule.restrictScalars R I)
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Ideal.prime_of_isPrime : ∀ {A : Type u_2} [inst : CommRing A] [IsDedekindDomain A] {P : Ideal A}, P ≠ ⊥ → P.IsPrime → Prime P
-- Batteries.Data.Nat.Lemmas
Nat.casesDiagOn_zero_succ : ∀ {motive : ℕ → ℕ → Sort u_1} (zero_zero : motive 0 0) (zero_succ : (n : ℕ) → motive 0 (n + 1))
  (succ_zero : (m : ℕ) → motive (m + 1) 0) (succ_succ : (m n : ℕ) → motive (m + 1) (n + 1)) (n : ℕ),
  Nat.casesDiagOn 0 (n + 1) zero_zero zero_succ succ_zero succ_succ = zero_succ n
-- Mathlib.RingTheory.FormalGroup.Basic
FormalGroup.map_toPowerSeries : ∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] (F : FormalGroup R) (f : R →+* S),
  (F.map f).toPowerSeries = (MvPowerSeries.map f) F.toPowerSeries
-- Mathlib.Data.String.Basic
String.toList_nonempty : ∀ {s : String}, s ≠ "" → s.toList = String.Legacy.front s :: (String.Legacy.drop s 1).toList
-- Mathlib.Algebra.Polynomial.DenomsClearable
/-- `denomsClearable` formalizes the property that `b ^ N * f (a / b)`
does not have denominators, if the inequality `f.natDegree ≤ N` holds.

The definition asserts the existence of an element `D` of `R` and an
element `bi = 1 / i b` of `K` such that clearing the denominators of
the fraction equals `i D`.
 -/
DenomsClearable : {R : Type u_1} →
  {K : Type u_2} → [inst : Semiring R] → [inst_1 : CommSemiring K] → R → R → ℕ → Polynomial R → (R →+* K) → Prop
-- Mathlib.Data.Nat.Init
Nat.case_strong_induction_on : ∀ {p : ℕ → Prop} (a : ℕ), p 0 → (∀ (n : ℕ), (∀ m ≤ n, p m) → p (n + 1)) → p a
-- Mathlib.FieldTheory.Perfect
frobeniusEquiv.congr_simp : ∀ (R : Type u_1) (p p_1 : ℕ) (e_p : p = p_1) [inst : CommSemiring R] [inst_1 : ExpChar R p] [inst_2 : PerfectRing R p],
  frobeniusEquiv R p = frobeniusEquiv R p_1
-- Mathlib.CategoryTheory.EffectiveEpi.Preserves
CategoryTheory.Functor.PreservesEffectiveEpiFamilies.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D},
  (∀ {α : Type u} {B : C} (X : α → C) (π : (a : α) → X a ⟶ B) [CategoryTheory.EffectiveEpiFamily X π],
      CategoryTheory.EffectiveEpiFamily (fun a => F.obj (X a)) fun a => F.map (π a)) →
    F.PreservesEffectiveEpiFamilies
-- Mathlib.Analysis.Convex.Combination
/-- A refinement of `Finset.centerMass_mem_convexHull` when the indexed family is a `Finset` of
the space.  -/
Finset.centerMass_id_mem_convexHull : ∀ {R : Type u_1} {E : Type u_3} [inst : Field R] [inst_1 : AddCommGroup E] [inst_2 : Module R E]
  [inst_3 : LinearOrder R] [IsStrictOrderedRing R] (t : Finset E) {w : E → R},
  (∀ i ∈ t, 0 ≤ w i) → 0 < ∑ i ∈ t, w i → t.centerMass w id ∈ (convexHull R) ↑t
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.refl_symm : ∀ {R : Type uR} {A₁ : Type uA₁} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Algebra R A₁],
  AlgEquiv.refl.symm = AlgEquiv.refl
-- Init.Data.Ord.Basic
_private.Init.Data.Ord.Basic.0.Ordering.then.match_1.eq_1 : ∀ (motive : Ordering → Sort u_1) (h_1 : Unit → motive Ordering.eq) (h_2 : (a : Ordering) → motive a),
  (match Ordering.eq with
    | Ordering.eq => h_1 ()
    | a => h_2 a) =
    h_1 ()
-- Mathlib.CategoryTheory.Comma.Basic
/-- A morphism from `L.obj left` to `R.obj right`  -/
CategoryTheory.Comma.hom : {A : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} A] →
    {B : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
        {T : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} T] →
            {L : CategoryTheory.Functor A T} →
              {R : CategoryTheory.Functor B T} → (self : CategoryTheory.Comma L R) → L.obj self.left ⟶ R.obj self.right