mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Data.Lsp.Extra
Lean.Lsp.LeanModule.mk.inj : ∀ {name : String} {uri : Lean.Lsp.DocumentUri} {data? : Option Lean.Json} {name_1 : String}
  {uri_1 : Lean.Lsp.DocumentUri} {data?_1 : Option Lean.Json},
  { name := name, uri := uri, data? := data? } = { name := name_1, uri := uri_1, data? := data?_1 } →
    name = name_1 ∧ uri = uri_1 ∧ data? = data?_1
-- Init.Data.String.Basic
String.toList_append : ∀ {s t : String}, (s ++ t).toList = s.toList ++ t.toList
-- Mathlib.Control.Functor.Multivariate
/-- Multivariate map, if `f : α ⟹ β` and `x : F α` then `f <$$> x : F β`  -/
MvFunctor.«term_<$$>_» : Lean.TrailingParserDescr
-- Lean.Elab.PreDefinition.Mutual
/-- Assign final attributes to the definitions. Assumes the EqnInfos to be already present.
 -/
Lean.Elab.Mutual.addPreDefAttributes : Array Lean.Elab.PreDefinition → Lean.Elab.TermElabM Unit
-- Lean.Util.MonadCache
Lean.MonadCacheT.instMonadFinally : {ω α β : Type} →
  {m : Type → Type} →
    [inst : STWorld ω m] →
      [inst_1 : BEq α] → [inst_2 : Hashable α] → [MonadFinally m] → MonadFinally (Lean.MonadCacheT α β m)
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.sum_X : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} (E : CategoryTheory.PreZeroHypercover X)
  (F : CategoryTheory.PreZeroHypercover X) (a : E.I₀ ⊕ F.I₀), (E.sum F).X a = Sum.elim E.X F.X a
-- Mathlib.Data.Nat.Prime.Defs
Nat.minFac_prime : ∀ {n : ℕ}, n ≠ 1 → Nat.Prime n.minFac
-- Mathlib.Algebra.Algebra.Hom
AlgHom.coe_id : ∀ (R : Type u) (A : Type v) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A], ⇑(AlgHom.id R A) = id
-- Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Multiset.sum_map_erase : ∀ {ι : Type u_2} {M : Type u_5} [inst : AddCommMonoid M] {m : Multiset ι} {f : ι → M} [inst_1 : DecidableEq ι] {a : ι},
  a ∈ m → f a + (Multiset.map f (m.erase a)).sum = (Multiset.map f m).sum
-- Init.Data.FloatArray.Basic
_private.Init.Data.FloatArray.Basic.0.FloatArray.forInUnsafe.loop : {β : Type v} → {m : Type v → Type w} → [Monad m] → FloatArray → (Float → β → m (ForInStep β)) → USize → USize → β → m β
-- Mathlib.Data.Subtype
Subtype.trans : ∀ {α : Sort u_1} {p : α → Prop} [inst : Setoid α] {s t u : Subtype p}, s ≈ t → t ≈ u → s ≈ u
-- Mathlib.Algebra.Ring.Semireal.Defs
instCharZeroOfIsSemireal : ∀ (R : Type u_1) [inst : NonAssocRing R] [IsSemireal R], CharZero R
-- Std.Sat.AIG.RefVec
Std.Sat.AIG.RefVec.get_append : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α} {lw rw : ℕ} (lhs : aig.RefVec lw)
  (rhs : aig.RefVec rw) (idx : ℕ) (hidx : idx < lw + rw),
  (lhs.append rhs).get idx hidx = if h : idx < lw then lhs.get idx h else rhs.get (idx - lw) ⋯
-- Mathlib.Combinatorics.Quiver.SingleObj
Quiver.SingleObj.pathEquivList_symm_nil : ∀ {α : Type u_1}, Quiver.SingleObj.pathEquivList.symm [] = Quiver.Path.nil
-- Mathlib.CategoryTheory.Bicategory.Opposites
Bicategory.Opposite.Hom2.op2' : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] → {a b : Bᵒᵖ} → {f g : a ⟶ b} → (f.unop ⟶ g.unop) → Bicategory.Opposite.Hom2 f g
-- Mathlib.CategoryTheory.Localization.Predicate
CategoryTheory.Localization.Lifting.compLeft_iso : ∀ {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] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) {E : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  (F : CategoryTheory.Functor D E),
  CategoryTheory.Localization.Lifting.iso L W (L.comp F) F = CategoryTheory.Iso.refl (L.comp F)
-- Mathlib.RingTheory.FinitePresentation
AlgHom.FinitePresentation.id : ∀ (R : Type u_1) (A : Type u_2) [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A],
  (AlgHom.id R A).FinitePresentation
-- Mathlib.Order.Filter.Pointwise
Filter.smulCommClass : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : SMul α γ] [inst_1 : SMul β γ] [SMulCommClass α β γ],
  SMulCommClass (Filter α) (Filter β) (Filter γ)
-- Lean.LocalContext
/-- Low level API for creating local declarations (`LocalDecl.cdecl`).
It is used to implement actions in the monads `Elab` and `Tactic`.
It should not be used directly since the argument `(fvarId : FVarId)` is
assumed to be unique. You can create a unique fvarId with `mkFreshFVarId`.  -/
Lean.LocalContext.mkLocalDecl : Lean.LocalContext →
  Lean.FVarId →
    Lean.Name →
      Lean.Expr →
        optParam Lean.BinderInfo Lean.BinderInfo.default →
          optParam Lean.LocalDeclKind Lean.LocalDeclKind.default → Lean.LocalContext
-- Mathlib.Algebra.FreeAbelianGroup.Finsupp
FreeAbelianGroup.coeff.eq_1 : ∀ {X : Type u_1} (x : X), FreeAbelianGroup.coeff x = (Finsupp.applyAddHom x).comp FreeAbelianGroup.toFinsupp
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.invRev_involutive : ∀ {α : Type u}, Function.Involutive FreeGroup.invRev
-- Mathlib.Topology.Covering.Quotient
Topology.IsQuotientMap.isQuotientCoveringMap_of_subgroup : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X},
  Topology.IsQuotientMap f →
    ∀ [inst_2 : Group E] [IsTopologicalGroup E] (G : Subgroup E),
      IsDiscrete ↑G → (∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₂ * e₁⁻¹ ∈ G) → IsQuotientCoveringMap f ↥G
-- Mathlib.LinearAlgebra.TensorProduct.Tower
/-- Heterobasic version of `TensorProduct.map_bilinear`  -/
TensorProduct.AlgebraTensorModule.mapBilinear : (R : Type uR) →
  (A : Type uA) →
    (B : Type uB) →
      (M : Type uM) →
        (N : Type uN) →
          (P : Type uP) →
            (Q : Type uQ) →
              [inst : CommSemiring R] →
                [inst_1 : Semiring A] →
                  [inst_2 : Semiring B] →
                    [inst_3 : Algebra R A] →
                      [inst_4 : Algebra R B] →
                        [inst_5 : AddCommMonoid M] →
                          [inst_6 : Module R M] →
                            [inst_7 : Module A M] →
                              [inst_8 : IsScalarTower R A M] →
                                [inst_9 : AddCommMonoid N] →
                                  [inst_10 : Module R N] →
                                    [inst_11 : AddCommMonoid P] →
                                      [inst_12 : Module R P] →
                                        [inst_13 : Module A P] →
                                          [inst_14 : IsScalarTower R A P] →
                                            [inst_15 : AddCommMonoid Q] →
                                              [inst_16 : Module R Q] →
                                                [inst_17 : Module B P] →
                                                  [inst_18 : IsScalarTower R B P] →
                                                    [inst_19 : SMulCommClass A B P] →
                                                      (M →ₗ[A] P) →ₗ[B]
                                                        (N →ₗ[R] Q) →ₗ[R] TensorProduct R M N →ₗ[A] TensorProduct R P Q
-- Mathlib.CategoryTheory.Sites.LocallyBijective
CategoryTheory.GrothendieckTopology.W.isLocallyInjective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} A] {FA : A → A → Type u_1} {CA : A → Type w'}
  [inst_2 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] [inst_3 : CategoryTheory.ConcreteCategory A FA]
  [J.WEqualsLocallyBijective A] {X Y : CategoryTheory.Functor Cᵒᵖ A} {f : X ⟶ Y},
  J.W f → CategoryTheory.Presheaf.IsLocallyInjective J f
-- Mathlib.Algebra.Category.MonCat.Basic
AddCommMonCat.equivalence_inverse_obj_coe : ∀ (X : CommMonCat), ↑(AddCommMonCat.equivalence.inverse.obj X) = Additive ↑X
-- Mathlib.LinearAlgebra.BilinearForm.Isometry
/-- The identity isometry from a bilinear form to itself.  -/
LinearMap.BilinForm.Isometry.id : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → (B : LinearMap.BilinForm R M) → B →bᵢ B
-- Mathlib.Algebra.Group.Conj
AddConjClasses.mk_injective : ∀ {α : Type u} [inst : AddCommMonoid α], Function.Injective AddConjClasses.mk
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
_private.Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting.0.CategoryTheory.Limits.termF₂ : Lean.ParserDescr
-- Mathlib.Combinatorics.Pigeonhole
/-- The pigeonhole principle for finitely many pigeons of different weights, non-strict inequality
version: there is a pigeonhole with the total weight of pigeons in it greater than or equal to `b`
provided that the total number of pigeonholes times `b` is less than or equal to the total weight of
all pigeons.  -/
Fintype.exists_le_sum_fiber_of_nsmul_le_sum : ∀ {α : Type u} {β : Type v} {M : Type w} [inst : DecidableEq β] [inst_1 : Fintype α] [inst_2 : Fintype β] (f : α → β)
  {w : α → M} {b : M} [inst_3 : AddCommMonoid M] [inst_4 : LinearOrder M] [IsOrderedCancelAddMonoid M] [Nonempty β],
  Fintype.card β • b ≤ ∑ x, w x → ∃ y, b ≤ ∑ x with f x = y, w x
-- Mathlib.Topology.Connected.Clopen
IsClopen.not_isPreconnected_iff : ∀ {α : Type u} [inst : TopologicalSpace α] {s : Set α},
  IsClopen s → (¬IsPreconnected s ↔ ∃ a b, IsClopen a ∧ IsClopen b ∧ a.Nonempty ∧ b.Nonempty ∧ Disjoint a b ∧ s = a ∪ b)
-- Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
/-- [Stacks Tag 04XU](https://stacks.math.columbia.edu/tag/04XU) -/
AlgebraicGeometry.Scheme.Hom.isProperMap : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.UniversallyClosed f], IsProperMap ⇑f
-- Mathlib.RingTheory.MvPowerSeries.Trunc
/-- A coefficient of a product of truncated power series equals the coefficient of the untruncated
product. Both factors are truncated at the same level `n`.  -/
MvPowerSeries.coeff_trunc_mul_trunc_eq_coeff_mul : ∀ {σ : Type u_1} {R : Type u_2} [inst : DecidableEq σ] [inst_1 : CommSemiring R] (n : σ →₀ ℕ) (f g : MvPowerSeries σ R)
  {m : σ →₀ ℕ},
  m < n →
    MvPolynomial.coeff m ((MvPowerSeries.trunc R n) f * (MvPowerSeries.trunc R n) g) = (MvPowerSeries.coeff m) (f * g)
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.smul_mem_smul : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : SMul α β] {s : Finset α} {t : Finset β} {a : α}
  {b : β}, a ∈ s → b ∈ t → a • b ∈ s • t
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.applyPartition.go.congr_simp : ∀ {α : Type u} {β : α → Type v} {δ : Type w} [inst : Ord α] (k : α → Ordering) (l : Std.DTreeMap.Internal.Impl α β)
  (f f_1 :
    List ((a : α) × β a) →
      (c : Std.DTreeMap.Internal.Cell α β k) →
        (Std.DTreeMap.Internal.Impl.contains' k l = true → c.contains = true) → List ((a : α) × β a) → δ),
  f = f_1 →
    ∀ (ll ll_1 : List ((a : α) × β a)),
      ll = ll_1 →
        ∀ (m m_1 : Std.DTreeMap.Internal.Impl α β) (e_m : m = m_1)
          (hm : Std.DTreeMap.Internal.Impl.contains' k l = true → Std.DTreeMap.Internal.Impl.contains' k m = true)
          (rr rr_1 : List ((a : α) × β a)),
          rr = rr_1 →
            Std.DTreeMap.Internal.Impl.applyPartition.go k l f ll m hm rr =
              Std.DTreeMap.Internal.Impl.applyPartition.go k l f_1 ll_1 m_1 ⋯ rr_1
-- Mathlib.RingTheory.PolynomialLaw.Basic
/-- The opposite of a polynomial law  -/
PolynomialLaw.neg : {R : Type u} →
  [inst : CommRing R] →
    {M : Type u_1} →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          {N : Type u_2} → [inst_3 : AddCommGroup N] → [inst_4 : Module R N] → (M →ₚₗ[R] N) → M →ₚₗ[R] N
-- Mathlib.Analysis.SumIntegralComparisons
/-- The partial sums of a nonnegative function are bounded by the integral over `(0, ∞)`.  -/
AntitoneOn.sum_range_le_integral : ∀ {f : ℝ → ℝ} {N : ℕ},
  AntitoneOn f (Set.Icc 0 ↑N) →
    MeasureTheory.IntegrableOn f (Set.Ioi 0) MeasureTheory.volume →
      (∀ t ∈ Set.Ioi 0, 0 ≤ f t) → ∑ n ∈ Finset.range N, f ↑(n + 1) ≤ ∫ (x : ℝ) in Set.Ioi 0, f x
-- Mathlib.Analysis.Calculus.FDeriv.Comp
/-- The chain rule for derivatives in the sense of strict differentiability.  -/
HasStrictFDerivAt.comp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E → F} {f' : E →L[𝕜] F} (x : E) {g : F → G}
  {g' : F →L[𝕜] G},
  HasStrictFDerivAt g g' (f x) → HasStrictFDerivAt f f' x → HasStrictFDerivAt (fun x => g (f x)) (g' ∘SL f') x
-- Mathlib.CategoryTheory.Shift.CommShift
CategoryTheory.NatTrans.CommShift.of_iso_inv : ∀ {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] {F₁ F₂ : CategoryTheory.Functor C D} (e : F₁ ≅ F₂) (A : Type u_5)
  [inst_2 : AddMonoid A] [inst_3 : CategoryTheory.HasShift C A] [inst_4 : CategoryTheory.HasShift D A]
  [inst_5 : F₁.CommShift A] [inst_6 : F₂.CommShift A] [CategoryTheory.NatTrans.CommShift e.hom A],
  CategoryTheory.NatTrans.CommShift e.inv A
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.le_one_iff_exists_coeIdeal : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  {J : FractionalIdeal S P}, J ≤ 1 ↔ ∃ I, ↑I = J
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
/-- In a unital `ℝ`-algebra `A` with a continuous functional calculus, an element `a : A` is larger
than some `algebraMap ℝ A r` if and only if every element of the `ℝ`-spectrum is nonnegative.  -/
CFC.exists_pos_algebraMap_le_iff : ∀ {A : Type u_1} [inst : TopologicalSpace A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : PartialOrder A]
  [StarOrderedRing A] [inst_5 : Algebra ℝ A] [NonnegSpectrumClass ℝ A] [Nontrivial A]
  [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] {a : A},
  autoParam (IsSelfAdjoint a) CFC.exists_pos_algebraMap_le_iff._auto_1 →
    ((∃ r > 0, (algebraMap ℝ A) r ≤ a) ↔ ∀ x ∈ spectrum ℝ a, 0 < x)
-- Mathlib.Data.List.Intervals
List.Ico.append_consecutive : ∀ {n m l : ℕ}, n ≤ m → m ≤ l → List.Ico n m ++ List.Ico m l = List.Ico n l
-- Mathlib.Data.Real.Embedding
Archimedean.ratLt'_add : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [IsOrderedAddMonoid M] [inst_3 : One M]
  [ZeroLEOneClass M] [NeZero 1] [Archimedean M] (x y : M),
  Archimedean.ratLt' (x + y) = Archimedean.ratLt' x + Archimedean.ratLt' y
-- Mathlib.Algebra.Order.Ring.Archimedean
ArchimedeanClass.isAddRegular_mk : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : CommRing R] [inst_2 : IsStrictOrderedRing R] {x : R},
  x ≠ 0 → IsAddRegular (ArchimedeanClass.mk x)
-- Init.Data.Array.Range
_private.Init.Data.Array.Range.0.Array.range.eq_1 : ∀ (n : ℕ), Array.range n = Array.ofFn fun i => ↑i
-- Mathlib.Combinatorics.SimpleGraph.Copy
/-- **Alias** of `SimpleGraph.Copy.maxDegree_mono`. -/
SimpleGraph.Copy.max_degree_le : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} [inst : Fintype V] [inst_1 : Fintype W]
  [inst_2 : DecidableRel G.Adj] [inst_3 : DecidableRel H.Adj] (f : G.Copy H), G.maxDegree ≤ H.maxDegree
-- Init.Data.String.Basic
List.utf8Decode?_utf8Encode : ∀ {l : List Char}, l.utf8Encode.utf8Decode? = some l.toArray
-- Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
CategoryTheory.FreeGroupoid.liftNatIso_inv_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {G : Type u₁} [inst_1 : CategoryTheory.Groupoid G]
  (F₁ F₂ : CategoryTheory.Functor (CategoryTheory.FreeGroupoid C) G)
  (τ : (CategoryTheory.FreeGroupoid.of C).comp F₁ ≅ (CategoryTheory.FreeGroupoid.of C).comp F₂) (X : C),
  (CategoryTheory.FreeGroupoid.liftNatIso F₁ F₂ τ).inv.app (CategoryTheory.FreeGroupoid.mk X) = τ.inv.app X
-- Mathlib.CategoryTheory.Abelian.Basic
CategoryTheory.Abelian.monoLift_comp_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y)
  [inst_2 : CategoryTheory.Mono f] {T : C} (g : T ⟶ Y)
  (hg : CategoryTheory.CategoryStruct.comp g (CategoryTheory.Limits.cokernel.π f) = 0) {Z : C} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.monoLift f g hg) (CategoryTheory.CategoryStruct.comp f h) =
    CategoryTheory.CategoryStruct.comp g h
-- Mathlib.Algebra.Algebra.Equiv
/-- If an `R`-algebra `A` is isomorphic to `R` as `R`-module, then the canonical map `R → A` is an
equivalence of `R`-algebras.

Note that if `e : R ≃ₗ[R] A` is the linear equivalence, then this is not the same as the equivalence
of algebras provided here unless `e 1 = 1`.  -/
LinearEquiv.algEquivOfRing : {R : Type u_1} →
  {A : Type u_2} →
    [inst : CommSemiring R] → [inst_1 : CommSemiring A] → [inst_2 : Algebra R A] → (R ≃ₗ[R] A) → R ≃ₐ[R] A
-- Mathlib.Algebra.Star.Unitary
commute_unitary_iff_star_right_conjugate : ∀ {R : Type u_1} [inst : Monoid R] [inst_1 : StarMul R] {x u : R}, u ∈ unitary R → (Commute u x ↔ u * x * star u = x)
-- Mathlib.Data.Seq.Defs
Stream'.Seq.le_stable : ∀ {α : Type u} (s : Stream'.Seq α) {m n : ℕ}, m ≤ n → s.get? m = none → s.get? n = none
-- Mathlib.Probability.Kernel.Composition.Comp
ProbabilityTheory.Kernel.IsFiniteKernel.comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (η : ProbabilityTheory.Kernel β γ) [ProbabilityTheory.IsFiniteKernel η]
  (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsFiniteKernel κ], ProbabilityTheory.IsFiniteKernel (η.comp κ)
-- Aesop.Tree.UnsafeQueue
Aesop.UnsafeQueueEntry.postponedSafeRule : Aesop.PostponedSafeRule → Aesop.UnsafeQueueEntry
-- Std.Internal.Do.WP.Lemmas
Std.Internal.Do.WPMonad.le_wp_read_ReaderT_apply : ∀ {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),
  Lean.Order.PartialOrder.rel (fun r => post r r) (Std.Internal.Do.wp MonadReaderOf.read post epost)
-- Mathlib.SetTheory.ZFC.Ordinal
/-- An ordinal is a transitive set, trichotomous under membership.  -/
ZFSet.isOrdinal_iff_trichotomous : ∀ {x : ZFSet.{u}}, x.IsOrdinal ↔ x.IsTransitive ∧ Std.Trichotomous (Subrel (fun x1 x2 => x1 ∈ x2) fun x_1 => x_1 ∈ x)
-- Mathlib.ModelTheory.FinitelyGenerated
FirstOrder.Language.Structure.FG.finite : ∀ {L : FirstOrder.Language} {M : Type u_1} [inst : L.Structure M] [L.IsRelational],
  FirstOrder.Language.Structure.FG L M → Finite M
-- Batteries.Data.List.Lemmas
List.singleton_disjoint : ∀ {α : Type u_1} {a : α} {l : List α}, [a].Disjoint l ↔ a ∉ l
-- Lean.Meta.Tactic.Simp.SimpAll
_private.Lean.Meta.Tactic.Simp.SimpAll.0.Lean.Meta.SimpAll.getSimpTheorems : Lean.Meta.SimpAll.M Lean.Meta.SimpTheoremsArray
-- Mathlib.Order.LiminfLimsup
Filter.blimsup_congr' : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {f : Filter β} {p q : β → Prop} {u : β → α},
  (∀ᶠ (x : β) in f, u x ≠ ⊥ → (p x ↔ q x)) → Filter.blimsup u f p = Filter.blimsup u f q
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
/-- The addition-preserving equivalence between the type of nonsingular Jacobian points on a
Weierstrass curve `W` and the type of nonsingular points in affine coordinates.  -/
WeierstrassCurve.Jacobian.Point.toAffineAddEquiv : {F : Type u} →
  [inst : Field F] → (W : WeierstrassCurve.Jacobian F) → [inst_1 : DecidableEq F] → W.Point ≃+ W.toAffine.Point
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Stepwise.d_step1 : ∀ {α : Type u_1} [inst : Lean.Grind.CommRing α] (ctx : Lean.Grind.CommRing.Context α) (k : ℤ)
  (init p₁ : Lean.Grind.CommRing.Poly) (k₂ : ℤ) (m₂ : Lean.Grind.CommRing.Mon) (p₂ p : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Stepwise.d_step1_cert p₁ k₂ m₂ p₂ p = true →
    ↑k * Lean.Grind.CommRing.Poly.denote ctx init = Lean.Grind.CommRing.Poly.denote ctx p₁ →
      Lean.Grind.CommRing.Poly.denote ctx p₂ = 0 →
        ↑k * Lean.Grind.CommRing.Poly.denote ctx init = Lean.Grind.CommRing.Poly.denote ctx p
-- Mathlib.Analysis.Normed.Field.Basic
NormedField.toNormedDivisionRing : {α : Type u_2} → [NormedField α] → NormedDivisionRing α
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
ContinuousLinearMap.sum_comp_single : ∀ (R : Type u_1) [inst : Semiring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] {ι : Type u_4} (φ : ι → Type u_5) [inst_4 : (i : ι) → TopologicalSpace (φ i)]
  [inst_5 : (i : ι) → AddCommMonoid (φ i)] [inst_6 : (i : ι) → Module R (φ i)] [inst_7 : Fintype ι]
  [inst_8 : DecidableEq ι] (L : ((i : ι) → φ i) →L[R] M) (v : (i : ι) → φ i),
  ∑ i, (L ∘SL ContinuousLinearMap.single R φ i) (v i) = L v
-- Std.Data.ExtDTreeMap.Basic
Std.ExtDTreeMap.instLawfulSingletonSigma : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp],
  LawfulSingleton ((a : α) × β a) (Std.ExtDTreeMap α β cmp)
-- Mathlib.Data.Num.ZNum
PosNum.sub'.eq_6 : ∀ (a b : PosNum), a.bit1.sub' b.bit1 = (a.sub' b).bit0
-- Mathlib.CategoryTheory.Idempotents.Karoubi
/-- a morphism between the underlying objects  -/
CategoryTheory.Idempotents.Karoubi.Hom.f : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] → {P Q : CategoryTheory.Idempotents.Karoubi C} → P.Hom Q → (P.X ⟶ Q.X)
-- Mathlib.Geometry.Convex.Set
Convexity.IsConvexSet.iConvexComb_mem : ∀ {ι : Type u_1} {R : Type u_3} {X : Type u_5} [inst : Semiring R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : Convexity.ConvexSpace R X] {s : Set X},
  Convexity.IsConvexSet R s →
    ∀ {w : Convexity.StdSimplex R ι} {f : ι → X}, (∀ (i : ι), w.weights i ≠ 0 → f i ∈ s) → Convexity.iConvexComb w f ∈ s
-- Mathlib.Tactic.Widget.Conv
/-- Display a widget panel allowing to generate a `conv` call zooming to the subexpression selected
in the goal or in the type of a local hypothesis or let-decl.  -/
Mathlib.Tactic.Conv.tacticConv? : Lean.ParserDescr
-- Mathlib.Topology.Order.LocalExtr
IsLocalMax.on : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder β] {f : α → β} {a : α},
  IsLocalMax f a → ∀ (s : Set α), IsLocalMaxOn f s a
-- Mathlib.Analysis.Analytic.Order
le_analyticOrderAt_sub : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f g : 𝕜 → E} {z₀ : 𝕜},
  min (analyticOrderAt f z₀) (analyticOrderAt g z₀) ≤ analyticOrderAt (f - g) z₀
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.prod.braiding_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P Q : C) [inst_1 : CategoryTheory.Limits.HasBinaryProduct P Q]
  [inst_2 : CategoryTheory.Limits.HasBinaryProduct Q P],
  (CategoryTheory.Limits.prod.braiding P Q).hom =
    CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst
-- Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells
HomotopicalAlgebra.AttachCells.ofArrowIso_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {α : Type t} {A B : α → C} {g : (a : α) → A a ⟶ B a}
  {X₁ X₂ : C} {f : X₁ ⟶ X₂} (c : HomotopicalAlgebra.AttachCells g f) {Y₁ Y₂ : C} {f' : Y₁ ⟶ Y₂}
  (e : CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk f'), (c.ofArrowIso e).ι = c.ι
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.constGetEntryGT?_eq : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t₁ t₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t₁.WF →
    t₂.WF →
      t₁.Equiv t₂ →
        ∀ {k : α}, Std.DTreeMap.Internal.Impl.Const.getEntryGT? k t₁ = Std.DTreeMap.Internal.Impl.Const.getEntryGT? k t₂
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.tr_push : ∀ (k : Turing.PartrecToTM2.K') (f : Option Turing.PartrecToTM2.Γ' → Option Turing.PartrecToTM2.Γ')
  (q : Turing.PartrecToTM2.Λ'),
  Turing.PartrecToTM2.tr (Turing.PartrecToTM2.Λ'.push k f q) =
    Turing.TM2.Stmt.branch (fun s => (f s).isSome)
      (Turing.TM2.Stmt.push k (fun s => (f s).getD default) (Turing.TM2.Stmt.goto fun x => q))
      (Turing.TM2.Stmt.goto fun x => q)
-- Init.Data.String.Defs
/-- The past-the-end position of `s`, as an `s.Pos`.  -/
String.endPos : (s : String) → s.Pos
-- Mathlib.Data.Vector.Basic
List.Vector.eq_cons_iff : ∀ {α : Type u_1} {n : ℕ} (a : α) (v : List.Vector α n.succ) (v' : List.Vector α n),
  v = a ::ᵥ v' ↔ v.head = a ∧ v.tail = v'