mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.Deriv.Shift
deriv_comp_sub_const : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] (f : 𝕜 → F) (a x : 𝕜), deriv (fun x => f (x - a)) x = deriv f (x - a)
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
SimpleGraph.triangleRemovalBound_le : ∀ {ε : ℝ},
  ε ≤ 1 →
    SimpleGraph.triangleRemovalBound ε ≤ (1 - ε / 4) * (ε / (16 * ↑(SzemerediRegularity.bound (ε / 8) ⌈4 / ε⌉₊))) ^ 3
-- Lean.Meta.Tactic.Cases
Lean.Meta.ByCasesSubgoal.fvarId : Lean.Meta.ByCasesSubgoal → Lean.FVarId
-- Mathlib.Analysis.Normed.Group.Quotient
Submodule.Quotient.completeSpace : ∀ {M : Type u_1} [inst : SeminormedAddCommGroup M] {R : Type u_3} [inst_1 : Ring R] [inst_2 : Module R M]
  (S : Submodule R M) [CompleteSpace M], CompleteSpace (M ⧸ S)
-- Mathlib.ModelTheory.Types
FirstOrder.Language.Theory.CompleteType.setOfPred_mem_eq_univ_iff : ∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type w} (φ : (L.withConstants α).Sentence),
  {p | φ ∈ p} = Set.univ ↔ (L.lhomWithConstants α).onTheory T ⊨ᵇ φ
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Zipper.cons : {α : Type u} →
  {β : α → Type v} →
    (k : α) → β k → Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Zipper α β → Std.DTreeMap.Internal.Zipper α β
-- Mathlib.Data.Nat.Totient
Nat.totient_zero : Nat.totient 0 = 0
-- Mathlib.LinearAlgebra.Matrix.Transvection
Matrix.TransvectionStruct.mk.injEq : ∀ {n : Type u_1} {R : Type u₂} (i j : n) (hij : i ≠ j) (c : R) (i_1 j_1 : n) (hij_1 : i_1 ≠ j_1) (c_1 : R),
  ({ i := i, j := j, hij := hij, c := c } = { i := i_1, j := j_1, hij := hij_1, c := c_1 }) =
    (i = i_1 ∧ j = j_1 ∧ c = c_1)
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- Characterization of the structured arrow category on the diagonal functor `T ⥤ T × T`.  -/
CategoryTheory.StructuredArrow.ofDiagEquivalence : {T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] →
    (X : T × T) →
      CategoryTheory.StructuredArrow X (CategoryTheory.Functor.diag T) ≌
        CategoryTheory.StructuredArrow X.2 (CategoryTheory.Under.forget X.1)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem_ofList_of_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List (α × β)} {k k' : α},
  cmp k k' = Ordering.eq →
    ∀ {v : β},
      List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l →
        (k, v) ∈ l → ∀ {h : k' ∈ Std.TreeMap.Raw.ofList l cmp}, (Std.TreeMap.Raw.ofList l cmp)[k'] = v
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKeyD_modify_self : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] [Inhabited α]
  {k fallback : α} {f : β k → β k}, (m.modify k f).getKeyD k fallback = if k ∈ m then k else fallback
-- Mathlib.Order.Interval.Basic
NonemptyInterval.pure_snd : ∀ {α : Type u_1} [inst : Preorder α] (a : α), (NonemptyInterval.pure a).toProd.2 = a
-- Init.Data.UInt.Lemmas
UInt16.toUInt8_lt : ∀ {a b : UInt16}, a.toUInt8 < b.toUInt8 ↔ a % 256 < b % 256
-- Mathlib.Tactic.FieldSimp.Lemmas
Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons : ∀ {M : Type u_1} [inst : CommGroupWithZero M] (n : ℤ) (e : M) {L l l' : Mathlib.Tactic.FieldSimp.NF M},
  L.eval * l.eval = l'.eval → L.eval * ((n, e) ::ᵣ l).eval = ((n, e) ::ᵣ l').eval
-- Mathlib.GroupTheory.Exponent
/-- If `f : M₁ →⋆ M₂` is surjective, then the exponent of `M₂` divides the exponent of `M₁`.  -/
MonoidHom.exponent_dvd : ∀ {F : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} [inst : Monoid M₁] [inst_1 : Monoid M₂] [inst_2 : FunLike F M₁ M₂]
  [MonoidHomClass F M₁ M₂] {f : F}, Function.Surjective ⇑f → Monoid.exponent M₂ ∣ Monoid.exponent M₁
-- Mathlib.CategoryTheory.Functor.FullyFaithful
/-- The unique isomorphism `X ≅ Y` which induces an isomorphism `F.obj X ≅ F.obj Y`
when `hF : F.FullyFaithful`.  -/
CategoryTheory.Functor.FullyFaithful.preimageIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C D} → F.FullyFaithful → {X Y : C} → (F.obj X ≅ F.obj Y) → (X ≅ Y)
-- Init.Data.UInt.Lemmas
UInt32.toUSize_ofNat' : ∀ {n : ℕ}, n < UInt32.size → (UInt32.ofNat n).toUSize = USize.ofNat n
-- Mathlib.RingTheory.Ideal.Quotient.Operations
DoubleQuot.quotQuotEquivQuotSup_quotQuotMk : ∀ {R : Type u} [inst : CommRing R] (I J : Ideal R) (x : R),
  (DoubleQuot.quotQuotEquivQuotSup I J) ((DoubleQuot.quotQuotMk I J) x) = (Ideal.Quotient.mk (I ⊔ J)) x
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getD.congr_simp : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] [inst_1 : Std.LawfulEqCmp cmp]
  (t t_1 : Std.ExtDTreeMap α β cmp),
  t = t_1 → ∀ (a : α) (fallback fallback_1 : β a), fallback = fallback_1 → t.getD a fallback = t_1.getD a fallback_1
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Param.mk.sizeOf_spec : ∀ {pu : Lean.Compiler.LCNF.Purity} (fvarId : Lean.FVarId) (binderName : Lean.Name) (type : Lean.Expr) (borrow : Bool),
  sizeOf { fvarId := fvarId, binderName := binderName, type := type, borrow := borrow } =
    1 + sizeOf fvarId + sizeOf binderName + sizeOf type + sizeOf borrow
-- Mathlib.Data.Finset.Filter
Finset.monotone_filter_right : ∀ {α : Type u_1} (s : Finset α) ⦃p q : α → Prop⦄ [inst : DecidablePred p] [inst_1 : DecidablePred q],
  (∀ a ∈ s, p a → q a) → Finset.filter p s ⊆ Finset.filter q s
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.constEntryAtIdx_eq : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t₁ t₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) {i : ℕ} {h' : i < t₁.size},
  Std.DTreeMap.Internal.Impl.Const.entryAtIdx t₁ ⋯ i h' = Std.DTreeMap.Internal.Impl.Const.entryAtIdx t₂ ⋯ i ⋯
-- Mathlib.Algebra.Group.Basic
sub_eq_neg_self : ∀ {G : Type u_3} [inst : AddGroup G] {a b : G}, a - b = -b ↔ a = 0
-- Mathlib.NumberTheory.EulerProduct.Basic
tsum_eq_tsum_primes_add_tsum_primes_of_support_subset_prime_powers : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : UniformSpace α] [IsUniformAddGroup α] [CompleteSpace α] [T0Space α]
  {f : ℕ → α},
  Summable f →
    Function.support f ⊆ {n | IsPrimePow n} →
      ∑' (n : ℕ), f n = ∑' (p : Nat.Primes), f ↑p + ∑' (p : Nat.Primes) (k : ℕ), f (↑p ^ (k + 2))
-- Mathlib.Data.Nat.BinaryRec
Nat.binaryRec_eq : ∀ {motive : ℕ → Sort u} {zero : motive 0} {bit : (b : Bool) → (n : ℕ) → motive n → motive (Nat.bit b n)} (b : Bool)
  (n : ℕ),
  bit false 0 zero = zero ∨ (n = 0 → b = true) →
    Nat.binaryRec zero bit (Nat.bit b n) = bit b n (Nat.binaryRec zero bit n)
-- Mathlib.Algebra.Group.Units.Defs
IsUnit.mul_div_mul_right : ∀ {α : Type u} [inst : DivisionMonoid α] {c : α}, IsUnit c → ∀ (a b : α), a * c / (b * c) = a / b
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
MeasureTheory.Measure.LebesgueDecomposition.iSup_succ_eq_sup : ∀ {α : Sort u_2} (f : ℕ → α → ENNReal) (m : ℕ) (a : α),
  ⨆ k, ⨆ (_ : k ≤ m + 1), f k a = max (f m.succ a) (⨆ k, ⨆ (_ : k ≤ m), f k a)
-- Init.Data.List.Monadic
/-- We can express a for loop over a list which always yields as a fold.  -/
List.forIn_yield_eq_foldlM : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β γ : Type u_1} [inst : Monad m] [LawfulMonad m] {l : List α}
  (f : α → β → m γ) (g : α → β → γ → β) (init : β),
  (forIn l init fun a b => (fun c => ForInStep.yield (g a b c)) <$> f a b) =
    List.foldlM (fun b a => g a b <$> f a b) init l
-- Mathlib.Analysis.Complex.Hadamard
/-- A technical lemma relating the bounds given by the three lines lemma on a general strip
to the bounds for its scaled version on the strip `re ⁻¹' [0, 1]`.  -/
Complex.HadamardThreeLines.interpStrip_scale : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] (f : ℂ → E) {l u : ℝ},
  l < u →
    ∀ (z : ℂ),
      Complex.HadamardThreeLines.interpStrip (Complex.HadamardThreeLines.scale f l u) ((z - ↑l) / (↑u - ↑l)) =
        Complex.HadamardThreeLines.interpStrip' f l u z
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.isoWhiskerRight_symm : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {G H : CategoryTheory.Functor C D} (α : G ≅ H)
  (F : CategoryTheory.Functor D E),
  (CategoryTheory.Functor.isoWhiskerRight α F).symm = CategoryTheory.Functor.isoWhiskerRight α.symm F
-- Init.Data.Vector.Lemmas
Vector.eq_replicate_iff : ∀ {α : Type u_1} {a : α} {n : ℕ} {xs : Vector α n}, xs = Vector.replicate n a ↔ ∀ b ∈ xs, b = a
-- Mathlib.GroupTheory.CommutingProbability
commProb_eq_zero_of_infinite : ∀ (M : Type u_1) [inst : Mul M] [Infinite M], commProb M = 0
-- Mathlib.CategoryTheory.Category.Bipointed
Bipointed.mk.injEq : ∀ (X : Type u) (toProd : X × X) (X_1 : Type u) (toProd_1 : X_1 × X_1),
  ({ X := X, toProd := toProd } = { X := X_1, toProd := toProd_1 }) = (X = X_1 ∧ toProd ≍ toProd_1)
-- Mathlib.Tactic.Linarith.Datatypes
/-- `produceCertificate hyps max_var` tries to derive a contradiction from the comparisons in
`hyps` by eliminating all variables ≤ `max_var`.
If successful, it returns a map `coeff : Nat → Nat` as a certificate.
This map represents that we can find a contradiction by taking the sum `∑ (coeff i) * hyps[i]`.  -/
Mathlib.Tactic.Linarith.CertificateOracle.produceCertificate : Mathlib.Tactic.Linarith.CertificateOracle → List Mathlib.Tactic.Linarith.Comp → ℕ → Lean.MetaM (Std.HashMap ℕ ℕ)
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.Append
Std.IterM.toListRev_append : ∀ {α₁ α₂ β : Type w} {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m] [inst_2 : Std.Iterator α₁ m β]
  [inst_3 : Std.Iterator α₂ m β] [Std.Iterators.Finite α₁ m] [Std.Iterators.Finite α₂ m] {it₁ : Std.IterM m β}
  {it₂ : Std.IterM m β},
  (it₁.append it₂).toListRev = do
    let l₁ ← it₁.toListRev
    let l₂ ← it₂.toListRev
    pure (l₂ ++ l₁)
-- Mathlib.Dynamics.PeriodicPts.Defs
AddAction.zsmul_vadd_mod_minimalPeriod : ∀ {α : Type v} {G : Type u} [inst : AddGroup G] [inst_1 : AddAction G α] (a : G) (b : α) (n : ℤ),
  (n % ↑(Function.minimalPeriod (fun x => a +ᵥ x) b)) • a +ᵥ b = n • a +ᵥ b
-- Mathlib.Combinatorics.Enumerative.Catalan.Basic
_private.Mathlib.Combinatorics.Enumerative.Catalan.Basic.0.catalan.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match n.succ with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_2 n
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.isSome_maxKey?_of_contains : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, t.contains k = true → t.maxKey?.isSome = true
-- Mathlib.Algebra.Order.IsBotOne
one_min : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : One α] [IsBotOneClass α] (a : α), min 1 a = 1
-- Mathlib.MeasureTheory.Measure.Lebesgue.Basic
/-- **Alias** of `Real.volume_closedEBall`. -/
Real.volume_emetric_closedBall : ∀ (a : ℝ) (r : ENNReal), MeasureTheory.volume (Metric.closedEBall a r) = 2 * r
-- Mathlib.Order.UpperLower.Basic
IsLowerSet.preimage : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {s : Set α},
  IsLowerSet s → ∀ {f : β → α}, Monotone f → IsLowerSet (f ⁻¹' s)
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.instSliceableImplUnitRcoSlice : {α : Type u} →
  [inst : Ord α] →
    Std.Rco.Sliceable (Std.DTreeMap.Internal.Impl α fun x => Unit) α (Std.DTreeMap.Internal.Unit.RcoSlice α)
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.maxView.match_1.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (l : Std.DTreeMap.Internal.Impl α β)
  (motive :
    (r : Std.DTreeMap.Internal.Impl α β) →
      r.Balanced → Std.DTreeMap.Internal.Impl.BalancedAtRoot l.size r.size → Sort u_3)
  (hr : Std.DTreeMap.Internal.Impl.leaf.Balanced)
  (hlr : Std.DTreeMap.Internal.Impl.BalancedAtRoot l.size Std.DTreeMap.Internal.Impl.leaf.size)
  (h_1 :
    (hr : Std.DTreeMap.Internal.Impl.leaf.Balanced) →
      (hlr : Std.DTreeMap.Internal.Impl.BalancedAtRoot l.size Std.DTreeMap.Internal.Impl.leaf.size) →
        motive Std.DTreeMap.Internal.Impl.leaf hr hlr)
  (h_2 :
    (size : ℕ) →
      (k' : α) →
        (v' : β k') →
          (l' r' : Std.DTreeMap.Internal.Impl α β) →
            (hr : (Std.DTreeMap.Internal.Impl.inner size k' v' l' r').Balanced) →
              (hlr :
                  Std.DTreeMap.Internal.Impl.BalancedAtRoot l.size
                    (Std.DTreeMap.Internal.Impl.inner size k' v' l' r').size) →
                motive (Std.DTreeMap.Internal.Impl.inner size k' v' l' r') hr hlr),
  (match Std.DTreeMap.Internal.Impl.leaf, hr, hlr with
    | Std.DTreeMap.Internal.Impl.leaf, hr, hlr => h_1 hr hlr
    | Std.DTreeMap.Internal.Impl.inner size k' v' l' r', hr, hlr => h_2 size k' v' l' r' hr hlr) =
    h_1 hr hlr
-- Init.Data.Ord.Basic
Ordering.isNe_then : ∀ {o₁ o₂ : Ordering}, (o₁.then o₂).isNe = (o₁.isNe || o₂.isNe)
-- Mathlib.Tactic.Linarith.Oracle.FourierMotzkin
/-- A `PComp` represents a contradiction if its `Comp` field represents a contradiction.
 -/
Mathlib.Tactic.Linarith.PComp.isContr : Mathlib.Tactic.Linarith.PComp → Bool
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.unitOfList_nil : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [EquivBEq α] [LawfulHashable α], Std.ExtHashMap.unitOfList [] = ∅
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
/-- Finitely summable non-negative functions have countable support  -/
Summable.countable_support_ennreal : ∀ {α : Type u_1} {f : α → ENNReal}, ∑' (i : α), f i ≠ ⊤ → (Function.support f).Countable
-- Mathlib.CategoryTheory.Limits.VanKampen
/-- Pullbacks distribute over universal coproducts in both arguments: This is the isomorphism
`∐ (Xᵢ ×[S] Xⱼ) ≅ (∐ Xᵢ) ×[S] (∐ Xⱼ)`.  -/
CategoryTheory.IsUniversalColimit.nonempty_isColimit_prod_of_pullbackCone : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type u_3} {ι' : Type u_4} {S : C} {X : ι → C}
  {a : CategoryTheory.Limits.Cofan X},
  CategoryTheory.IsUniversalColimit a →
    ∀ {Y : ι' → C} {b : CategoryTheory.Limits.Cofan Y},
      CategoryTheory.IsUniversalColimit b →
        ∀ (f : (i : ι) → X i ⟶ S) (g : (i : ι') → Y i ⟶ S) (u : a.pt ⟶ S) (v : b.pt ⟶ S)
          [∀ (i : ι), CategoryTheory.Limits.HasPullback (f i) v]
          (s : (i : ι) → (j : ι') → CategoryTheory.Limits.PullbackCone (f i) (g j))
          (hs : (i : ι) → (j : ι') → CategoryTheory.Limits.IsLimit (s i j)) (t : CategoryTheory.Limits.PullbackCone u v)
          (ht : CategoryTheory.Limits.IsLimit t) {d : CategoryTheory.Limits.Cofan fun p => (s p.1 p.2).pt}
          (e : d.pt ≅ t.pt),
          autoParam (∀ (i : ι), CategoryTheory.CategoryStruct.comp (a.inj i) u = f i)
              CategoryTheory.IsUniversalColimit.nonempty_isColimit_prod_of_pullbackCone._auto_1 →
            autoParam (∀ (i : ι'), CategoryTheory.CategoryStruct.comp (b.inj i) v = g i)
                CategoryTheory.IsUniversalColimit.nonempty_isColimit_prod_of_pullbackCone._auto_3 →
              autoParam
                  (∀ (i : ι) (j : ι'),
                    CategoryTheory.CategoryStruct.comp (d.inj (i, j)) (CategoryTheory.CategoryStruct.comp e.hom t.fst) =
                      CategoryTheory.CategoryStruct.comp (s (i, j).1 (i, j).2).fst (a.inj (i, j).1))
                  CategoryTheory.IsUniversalColimit.nonempty_isColimit_prod_of_pullbackCone._auto_5 →
                autoParam
                    (∀ (i : ι) (j : ι'),
                      CategoryTheory.CategoryStruct.comp (d.inj (i, j))
                          (CategoryTheory.CategoryStruct.comp e.hom t.snd) =
                        CategoryTheory.CategoryStruct.comp (s (i, j).1 (i, j).2).snd (b.inj (i, j).2))
                    CategoryTheory.IsUniversalColimit.nonempty_isColimit_prod_of_pullbackCone._auto_7 →
                  Nonempty (CategoryTheory.Limits.IsColimit d)
-- Mathlib.RingTheory.WittVector.Basic
WittVector.mapFun.surjective : ∀ {p : ℕ} {α : Type u_3} {β : Type u_4} (f : α → β), Function.Surjective f → Function.Surjective (WittVector.mapFun f)
-- Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
jacobiTheta₂_conj : ∀ (z τ : ℂ), (starRingEnd ℂ) (jacobiTheta₂ z τ) = jacobiTheta₂ ((starRingEnd ℂ) z) (-(starRingEnd ℂ) τ)
-- Init.Data.BitVec.Lemmas
BitVec.two_pow_le_toNat_of_getElem_eq_true : ∀ {w i : ℕ} {x : BitVec w} (hi : i < w), x[i] = true → 2 ^ i ≤ x.toNat
-- Std.Data.DTreeMap.Iterator
/-- Returns a finite iterator over the keys of a dependent tree map.
The iterator yields the keys in order and then terminates.

The key and value types must live in the same universe.

**Termination properties:**

* `Finite` instance: always
* `Productive` instance: always
 -/
Std.DTreeMap.keysIter : {α : Type u} → {β : α → Type u} → {cmp : α → α → Ordering} → Std.DTreeMap α β cmp → Std.Iter α
-- Mathlib.Algebra.Order.GroupWithZero.Defs
/-- Typeclass for strict monotonicity of multiplication by positive elements on the left,
namely `a₁ < a₂ → b * a₁ < b * a₂` if `0 < b`.

You should usually not use this very granular typeclass directly, but rather a typeclass like
`IsStrictOrderedRing`.  -/
PosMulStrictMono : (α : Type u_1) → [Mul α] → [Zero α] → [Preorder α] → Prop
-- Lean.Elab.Term.TermElabM
/-- State of the `TermElabM` monad.
 -/
Lean.Elab.Term.State : Type
-- Mathlib.CategoryTheory.Galois.Action
CategoryTheory.PreGaloisCategory.instPreservesFiniteCoproductsActionFintypeCatAutFunctorFunctorToAction : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (F : CategoryTheory.Functor C FintypeCat)
  [inst_1 : CategoryTheory.GaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F],
  CategoryTheory.Limits.PreservesFiniteCoproducts (CategoryTheory.PreGaloisCategory.functorToAction F)
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.mem_map_submodule : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {L₂ : Type w}
  [inst_3 : LieRing L₂] [inst_4 : LieAlgebra R L₂] (K : LieSubalgebra R L) (e : L ≃ₗ⁅R⁆ L₂) (x : L₂),
  x ∈ LieSubalgebra.map e.toLieHom K ↔ x ∈ Submodule.map (↑e.toLinearEquiv) K.toSubmodule
-- Mathlib.GroupTheory.GroupAction.Hom
DistribMulActionHom.id_comp : ∀ {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] {φ : M →* N} {A : Type u_4} [inst_2 : AddMonoid A]
  [inst_3 : DistribMulAction M A] {B : Type u_5} [inst_4 : AddMonoid B] [inst_5 : DistribMulAction N B]
  (f : A →ₑ+[φ] B), (DistribMulActionHom.id N).comp f = f
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.mk_eq_two_iff' : ∀ {α : Type u} (x : α), Cardinal.mk α = 2 ↔ ∃! y, y ≠ x
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
HomogeneousIdeal.mem_iff : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : Semiring A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubmonoidClass σ A] {𝒜 : ι → σ} [inst_3 : DecidableEq ι] [inst_4 : AddMonoid ι] [inst_5 : GradedRing 𝒜]
  {I : HomogeneousIdeal 𝒜} {x : A}, x ∈ I.toIdeal ↔ x ∈ I
-- Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology
CategoryTheory.Precoverage.toGrothendieck_comap_eq_restrictedTopology : ∀ {C : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_3, u_3} C]
  [inst_1 : CategoryTheory.Category.{v_4, u_4} D] (F : CategoryTheory.Functor C D) (K : CategoryTheory.Precoverage D)
  [K.HasIsos] [K.IsStableUnderBaseChange] [K.IsStableUnderComposition] [K.HasPullbacks] [F.Faithful] [F.Full],
  (∀ {S : C} {R : CategoryTheory.Presieve (F.obj S)},
      R ∈ K.coverings (F.obj S) →
        CategoryTheory.Presieve.map F (CategoryTheory.Presieve.functorPullback F R) ∈ K.coverings (F.obj S)) →
    (CategoryTheory.Precoverage.comap F K).toGrothendieck = F.restrictedTopology K.toGrothendieck
-- Std.Data.DTreeMap.Internal.WF.Defs
/-- `mergeWith` preserves well-formedness. Later shown to be subsumed by `.wf`.  -/
Std.DTreeMap.Internal.Impl.WF.mergeWith : ∀ {α : Type u} [inst : Ord α] {x : α → Type v} {t₁ t₂ : Std.DTreeMap.Internal.Impl α x} {f : (a : α) → x a → x a → x a}
  {h : t₁.Balanced} [inst_1 : Std.LawfulEqOrd α], t₁.WF → (Std.DTreeMap.Internal.Impl.mergeWith f t₁ t₂ h).impl.WF
-- Mathlib.GroupTheory.Submonoid.Inverses
Submonoid.fromLeftInv_mul : ∀ {M : Type u_1} [inst : CommMonoid M] (S : Submonoid M) (x : ↥S.leftInv), ↑(S.fromLeftInv x) * ↑x = 1
-- Mathlib.Order.Grade
/-- Maximal elements have maximal grades.  -/
GradeMaxOrder.isMax_grade : ∀ {𝕆 : Type u_5} {α : Type u_6} {inst : Preorder 𝕆} {inst_1 : Preorder α} [self : GradeMaxOrder 𝕆 α] ⦃a : α⦄,
  IsMax a → IsMax (GradeOrder.grade a)
-- Mathlib.Tactic.NormNum.Inv
Mathlib.Meta.NormNum.isRat_mkRat : ∀ {a na n : ℤ} {b nb d : ℕ},
  Mathlib.Meta.NormNum.IsInt a na →
    Mathlib.Meta.NormNum.IsNat b nb →
      Mathlib.Meta.NormNum.IsRat (↑na / ↑nb) n d → Mathlib.Meta.NormNum.IsRat (mkRat a b) n d
-- Mathlib.Tactic.LinearCombination.Lemmas
Mathlib.Ineq.WithStrictness.le : Mathlib.Ineq.WithStrictness
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKeyD_modify_eq_minKeyD : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] {k : α} {f : β → β} {fallback : α}, (t.modify k f).minKeyD fallback = t.minKeyD fallback
-- Std.Internal.Do.WP.Lemmas
Std.Internal.Do.WPMonad.wp_restoreM_ReaderT_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 : α → ρ → Pred} {epost : EPred} (x : m α),
  Std.Internal.Do.wp (MonadControl.restoreM x) post epost = fun r => Std.Internal.Do.wp x (fun a => post a r) epost
-- Mathlib.Order.UpperLower.Basic
isUpperSet_iInter : ∀ {α : Type u_1} {ι : Sort u_3} [inst : LE α] {f : ι → Set α}, (∀ (i : ι), IsUpperSet (f i)) → IsUpperSet (⋂ i, f i)
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.lift_mk : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] {f : Polynomial R} [inst_1 : CommRing S] {i : R →+* S} {a : S}
  (h : Polynomial.eval₂ i a f = 0) (g : Polynomial R),
  (AdjoinRoot.lift i a h) ((AdjoinRoot.mk f) g) = Polynomial.eval₂ i a g
-- Mathlib.Computability.TuringMachine.Computable
/-- A proof of tm outputting l' when given l.  -/
Turing.TM2Outputs : (tm : Turing.FinTM2) → List (tm.Γ tm.k₀) → Option (List (tm.Γ tm.k₁)) → Type
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed
CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.right_triangle_components : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  [inst_4 : CategoryTheory.MonoidalClosed V] {F H : CategoryTheory.Functor C V} (G : CategoryTheory.Functor C V)
  [inst_5 : CategoryTheory.MonoidalCategory.DayConvolution F H]
  (ℌ : CategoryTheory.MonoidalCategory.DayConvolutionInternalHom F G H) {H' : CategoryTheory.Functor C V}
  (ℌ' :
    CategoryTheory.MonoidalCategory.DayConvolutionInternalHom F
      (CategoryTheory.MonoidalCategory.DayConvolution.convolution F H) H'),
  CategoryTheory.CategoryStruct.comp ℌ'.coev_app (ℌ'.map ℌ.ev_app ℌ) = CategoryTheory.CategoryStruct.id H
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.secondCountableTopology : ∀ (p : ENNReal) (α : Type u_2) (β : Type u_3) [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [SecondCountableTopology α] [SecondCountableTopology β], SecondCountableTopology (WithLp p (α × β))
-- Std.Do.Triple.SpecLemmas
List.eq_of_range'_eq_append_cons : ∀ {s n step : ℕ} {xs : List ℕ} {cur : ℕ} {ys : List ℕ},
  List.range' s n step = xs ++ cur :: ys → cur = s + step * xs.length
-- Mathlib.Data.Set.Image
Set.image_eq_empty : ∀ {α : Type u_5} {β : Type u_6} {f : α → β} {s : Set α}, f '' s = ∅ ↔ s = ∅
-- Mathlib.Computability.DFA
/-- Starting state.  -/
DFA.start : {α : Type u} → {σ : Type v} → DFA α σ → σ