mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.ScottContinuity
/-- Eta-expanded form of `ScottContinuous.const` -/
ScottContinuous.fun_const : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (x : β), ScottContinuous fun x_1 => x
-- Mathlib.Data.Int.GCD
/-- **Bézout's lemma**  -/
Int.gcd_eq_gcd_ab : ∀ (x y : ℤ), ↑(x.gcd y) = x * x.gcdA y + y * x.gcdB y
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
CochainComplex.HomComplex.Cochain.shift_smul : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {R : Type u_1}
  [inst_2 : Ring R] [inst_3 : CategoryTheory.Linear R C] {K L : CochainComplex C ℤ} {n : ℤ}
  (γ : CochainComplex.HomComplex.Cochain K L n) (a : ℤ) (x : R), (x • γ).shift a = x • γ.shift a
-- Mathlib.GroupTheory.Congruence.Opposite
/-- If `c` is a multiplicative congruence on `M`, then `(a, b) ↦ c b.unop a.unop` is a
multiplicative congruence on `Mᵐᵒᵖ`.  -/
Con.op : {M : Type u_1} → [inst : Mul M] → Con M → Con Mᵐᵒᵖ
-- Mathlib.Order.Filter.Basic
Filter.mem_of_eq_bot : ∀ {α : Type u} {f : Filter α} {s : Set α}, f ⊓ Filter.principal sᶜ = ⊥ → s ∈ f
-- Init.Data.String.Lemmas.Order
String.Slice.Pos.ne_startPos_of_sliceFrom_ne_startPos : ∀ {s : String.Slice} {p p₀ : s.Pos} {h₀ : p₀ ≤ p}, p₀.sliceFrom p h₀ ≠ (s.sliceFrom p₀).startPos → p ≠ s.startPos
-- Mathlib.Data.List.Sort
RelIso.pairwise_swap_listMap : ∀ {α : Type u_1} {β : Type u_2} {ra : α → α → Prop} {rb : β → β → Prop} (e : ra ≃r rb) {l : List α},
  List.Pairwise (Function.swap rb) (List.map (⇑e) l) ↔ List.Pairwise (Function.swap ra) l
-- Mathlib.Data.Sym.Sym2
/-- `Sym2.diagElem` and `Sym2.diag` as an equivalence.  -/
Sym2.diagElemEquiv : {α : Type u_1} → { a // a.IsDiag } ≃ α
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
/-- A version of `exists_ne_zero_mem_ideal_lt` for the ring of integers of `K`.  -/
NumberField.mixedEmbedding.exists_ne_zero_mem_ringOfIntegers_lt : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] {f : NumberField.InfinitePlace K → NNReal},
  NumberField.mixedEmbedding.minkowskiBound K 1 < MeasureTheory.volume (NumberField.mixedEmbedding.convexBodyLT K f) →
    ∃ a, a ≠ 0 ∧ ∀ (w : NumberField.InfinitePlace K), w ↑a < ↑(f w)
-- Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd
/-- The product of two finite measures `μ` and `ν` is the only finite measure `ξ` such that
for all families of real bounded continuous functions `f` and `g` we have
`∫ p, (Π i, f i (p.1 i)) * (Π j, g j (p.2 j)) ∂ξ =
(∫ x, Π i, f i (x i) ∂μ) * (∫ y, Π j, g j (y j) ∂ν)`.  -/
Measure.eq_prod_of_integral_prod_mul_prod_boundedContinuousFunction : ∀ {ι : Type u_1} {κ : Type u_2} {X : ι → Type u_5} {Y : κ → Type u_6} {mX : (i : ι) → MeasurableSpace (X i)}
  [inst : (i : ι) → TopologicalSpace (X i)] [∀ (i : ι), BorelSpace (X i)] [∀ (i : ι), HasOuterApproxClosed (X i)]
  {mY : (j : κ) → MeasurableSpace (Y j)} [inst_3 : (j : κ) → TopologicalSpace (Y j)] [∀ (j : κ), BorelSpace (Y j)]
  [∀ (j : κ), HasOuterApproxClosed (Y j)] [inst_6 : Fintype ι] [inst_7 : Fintype κ]
  {μ : MeasureTheory.Measure ((i : ι) → X i)} {ν : MeasureTheory.Measure ((j : κ) → Y j)}
  {ξ : MeasureTheory.Measure (((i : ι) → X i) × ((j : κ) → Y j))} [MeasureTheory.IsFiniteMeasure μ]
  [MeasureTheory.IsFiniteMeasure ν] [MeasureTheory.IsFiniteMeasure ξ],
  (∀ (f : (i : ι) → BoundedContinuousFunction (X i) ℝ) (g : (j : κ) → BoundedContinuousFunction (Y j) ℝ),
      ∫ (p : ((i : ι) → X i) × ((j : κ) → Y j)), (∏ i, (f i) (p.1 i)) * ∏ j, (g j) (p.2 j) ∂ξ =
        (∫ (x : (i : ι) → X i), ∏ i, (f i) (x i) ∂μ) * ∫ (y : (j : κ) → Y j), ∏ j, (g j) (y j) ∂ν) →
    ξ = μ.prod ν
-- Mathlib.Algebra.Group.Subgroup.Defs
/-- Typeclass for substructures `s` such that `s ∪ -s = G`.  -/
HasMemOrNegMem : {S : Type u_3} → {G : Type u_4} → [Neg G] → [SetLike S G] → S → Prop
-- Mathlib.Order.Monotone.Basic
Nat.pow_self_strictMonoOn : StrictMonoOn (fun n => n ^ n) {n | n ≠ 0}
-- Mathlib.Data.ENat.Basic
/-- **Alias** of `ENat.natCast_lt_top`. -/
ENat.coe_lt_top : ∀ (n : ℕ), ↑n < ⊤
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.instHasOfPostcompPropertyTop : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C),
  ⊤.HasOfPostcompProperty W
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.edgeSet_monotone : ∀ {V : Type u} {G : SimpleGraph V}, Monotone SimpleGraph.Subgraph.edgeSet
-- Mathlib.RingTheory.Valuation.Basic
instCoeTCValuationOfValuationClass : (F : Type u_2) →
  (R : Type u_3) →
    (Γ₀ : Type u_4) →
      [inst : LinearOrderedCommMonoidWithZero Γ₀] →
        [inst_1 : Ring R] → [inst_2 : FunLike F R Γ₀] → [ValuationClass F R Γ₀] → CoeTC F (Valuation R Γ₀)
-- Mathlib.Order.Sublattice
Sublattice.map_id : ∀ {α : Type u_2} [inst : Lattice α] {L : Sublattice α}, Sublattice.map (LatticeHom.id α) L = L
-- Lean.Elab.PreDefinition.Structural.Main
Lean.Elab.Structural.reportTermMeasure : Lean.Elab.PreDefinition → ℕ → Lean.MetaM Unit
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.restrict_univ : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] {μ : MeasureTheory.FiniteMeasure Ω}, μ.restrict Set.univ = μ
-- Mathlib.Algebra.Group.Units.Equiv
Units.mulLeft_bijective : ∀ {M : Type u_3} [inst : Monoid M] (a : Mˣ), Function.Bijective fun x => ↑a * x
-- Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
MeasureTheory.lpNorm_zero : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} [inst : NormedAddCommGroup E] (p : ENNReal)
  (μ : MeasureTheory.Measure α), MeasureTheory.lpNorm 0 p μ = 0
-- Lean.Server.Requests
Lean.Server.RequestContext.doc : Lean.Server.RequestContext → Lean.Server.FileWorker.EditableDocument
-- Init.Data.List.Basic
/-- Returns `true` if every element of `bs` is the value `true`.

`O(|bs|)`. Short-circuits at the first `false` value.

* `[true, true, true].and = true`
* `[true, false, true].and = false`
* `[true, false, false].and = false`
* `[].and = true`
 -/
List.and : List Bool → Bool
-- Mathlib.Topology.Constructible
/-- [Stacks Tag 005B](https://stacks.math.columbia.edu/tag/005B) -/
IsRetrocompact.image_of_isEmbedding : ∀ {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {s : Set X},
  IsRetrocompact s → Topology.IsEmbedding f → IsRetrocompact (Set.range f) → IsRetrocompact (f '' s)
-- Mathlib.Order.WellFoundedSet
Set.IsPWO.union : ∀ {α : Type u_2} [inst : Preorder α] {s t : Set α}, s.IsPWO → t.IsPWO → (s ∪ t).IsPWO
-- Mathlib.LinearAlgebra.LinearIndependent.Basic
linearIndependent_sum : ∀ {ι : Type u'} {ι' : Type u_1} {R : Type u_2} {M : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] {v : ι ⊕ ι' → M},
  LinearIndependent R v ↔
    LinearIndependent R (v ∘ Sum.inl) ∧
      LinearIndependent R (v ∘ Sum.inr) ∧
        Disjoint (Submodule.span R (Set.range (v ∘ Sum.inl))) (Submodule.span R (Set.range (v ∘ Sum.inr)))
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.curryAddEquiv_single : ∀ {R : Type u_1} {M : Type u_4} {N : Type u_5} [inst : Semiring R] [inst_1 : AddMonoid M] [inst_2 : AddMonoid N] (m : M)
  (n : N) (r : R),
  AddMonoidAlgebra.curryAddEquiv (AddMonoidAlgebra.single (m, n) r) =
    AddMonoidAlgebra.single m (AddMonoidAlgebra.single n r)
-- Init.Data.Range.Polymorphic.UInt
UInt8.upwardEnumerableLT_ofBitVec : ∀ {x y : BitVec 8},
  Std.PRange.UpwardEnumerable.LT { toBitVec := x } { toBitVec := y } ↔ Std.PRange.UpwardEnumerable.LT x y
-- Mathlib.LinearAlgebra.Matrix.Nondegenerate
/-- If `M` is nondegenerate and `w * M * v = 0` for all `w`, then `v = 0`.  -/
Matrix.Nondegenerate.eq_zero_of_ortho : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_3} [inst : CommSemiring R] {M : Matrix m n R} [inst_1 : Fintype m]
  [inst_2 : Fintype n], M.Nondegenerate → ∀ {v : m → R}, (∀ (w : n → R), v ⬝ᵥ M.mulVec w = 0) → v = 0
-- Mathlib.Logic.Equiv.Basic
/-- If `α ≃ β`, then for any predicate `p : β → Prop` the subtype `{a // p (e a)}` is equivalent
to the subtype `{b // p b}`.  -/
Equiv.subtypeEquivOfSubtype : {α : Sort u_1} → {β : Sort u_4} → {p : β → Prop} → (e : α ≃ β) → { a // p (e a) } ≃ { b // p b }
-- Mathlib.RingTheory.LaurentSeries
LaurentSeries.hasseDeriv_comp_coeff : ∀ {R : Type u_1} [inst : Semiring R] {V : Type u_2} [inst_1 : AddCommGroup V] [inst_2 : Module R V] (k l : ℕ)
  (f : LaurentSeries V) (n : ℤ),
  ((LaurentSeries.hasseDeriv R k) ((LaurentSeries.hasseDeriv R l) f)).coeff n =
    ((k + l).choose k • (LaurentSeries.hasseDeriv R (k + l)) f).coeff n
-- Lean.Meta.Tactic.Simp.Types
/-- `maxDischargeDepth` from `config` as an `UInt32`.  -/
Lean.Meta.Simp.Context.maxDischargeDepth : Lean.Meta.Simp.Context → UInt32
-- Mathlib.Data.Set.Card
Set.one_le_encard_iff_nonempty : ∀ {α : Type u_1} {s : Set α}, 1 ≤ s.encard ↔ s.Nonempty
-- Lean.Meta.Sym.SymM
Lean.Meta.Sym.State.mk.injEq : ∀ (share : Lean.Meta.Sym.AlphaShareCommon.State) (maxFVar : Lean.PHashMap Lean.Meta.Sym.ExprPtr (Option Lean.FVarId))
  (proofInstInfo : Lean.PHashMap Lean.Name (Option Lean.Meta.Sym.ProofInstInfo))
  (inferType : Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Expr)
  (getLevel : Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Level)
  (congrInfo : Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Meta.Sym.CongrInfo)
  (defEqI : Lean.PHashMap (Lean.Meta.Sym.ExprPtr × Lean.Meta.Sym.ExprPtr) Bool)
  (extensions : Array Lean.Meta.Sym.SymExtensionState) (issues : List Lean.MessageData)
  (canon : Lean.Meta.Sym.Canon.State) (instanceOverrides : Lean.PHashMap Lean.Expr Lean.Expr) (debug : Bool)
  (share_1 : Lean.Meta.Sym.AlphaShareCommon.State)
  (maxFVar_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr (Option Lean.FVarId))
  (proofInstInfo_1 : Lean.PHashMap Lean.Name (Option Lean.Meta.Sym.ProofInstInfo))
  (inferType_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Expr)
  (getLevel_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Level)
  (congrInfo_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Meta.Sym.CongrInfo)
  (defEqI_1 : Lean.PHashMap (Lean.Meta.Sym.ExprPtr × Lean.Meta.Sym.ExprPtr) Bool)
  (extensions_1 : Array Lean.Meta.Sym.SymExtensionState) (issues_1 : List Lean.MessageData)
  (canon_1 : Lean.Meta.Sym.Canon.State) (instanceOverrides_1 : Lean.PHashMap Lean.Expr Lean.Expr) (debug_1 : Bool),
  ({ share := share, maxFVar := maxFVar, proofInstInfo := proofInstInfo, inferType := inferType, getLevel := getLevel,
        congrInfo := congrInfo, defEqI := defEqI, extensions := extensions, issues := issues, canon := canon,
        instanceOverrides := instanceOverrides, debug := debug } =
      { share := share_1, maxFVar := maxFVar_1, proofInstInfo := proofInstInfo_1, inferType := inferType_1,
        getLevel := getLevel_1, congrInfo := congrInfo_1, defEqI := defEqI_1, extensions := extensions_1,
        issues := issues_1, canon := canon_1, instanceOverrides := instanceOverrides_1, debug := debug_1 }) =
    (share = share_1 ∧
      maxFVar = maxFVar_1 ∧
        proofInstInfo = proofInstInfo_1 ∧
          inferType = inferType_1 ∧
            getLevel = getLevel_1 ∧
              congrInfo = congrInfo_1 ∧
                defEqI = defEqI_1 ∧
                  extensions = extensions_1 ∧
                    issues = issues_1 ∧ canon = canon_1 ∧ instanceOverrides = instanceOverrides_1 ∧ debug = debug_1)
-- Mathlib.Geometry.Manifold.Bordism
SingularManifold.sum_M : ∀ {X : Type u_1} [inst : TopologicalSpace X] {k : WithTop ℕ∞} {E : Type u_4} {H : Type u_5}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] [inst_3 : FiniteDimensional ℝ E]
  [inst_4 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} (s : SingularManifold X k I) (t : SingularManifold X k I),
  (s.sum t).M = (s.M ⊕ t.M)
-- Mathlib.Data.Sym.Basic
Sym.erase.congr_simp : ∀ {α : Type u_1} {n : ℕ} [inst : DecidableEq α] (s s_1 : Sym α (n + 1)) (e_s : s = s_1) (a a_1 : α) (e_a : a = a_1)
  (h : a ∈ s), s.erase a h = s_1.erase a_1 ⋯
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.integral_comp_sub_left : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} (f : ℝ → E) (d : ℝ),
  ∫ (x : ℝ) in a..b, f (d - x) = ∫ (x : ℝ) in d - b..d - a, f x
-- Mathlib.ModelTheory.Algebra.Ring.Basic
/-- `RingFunc.mul`, but with the defeq type `Language.ring.Functions 2` instead
of `RingFunc 2`  -/
FirstOrder.Ring.mulFunc : FirstOrder.Language.ring.Functions 2
-- Mathlib.Analysis.InnerProductSpace.TwoDim
Orientation.rightAngleRotationAux₁_rightAngleRotationAux₁ : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : Fact (Module.finrank ℝ E = 2)]
  (o : Orientation ℝ E (Fin 2)) (x : E), o.rightAngleRotationAux₁ (o.rightAngleRotationAux₁ x) = -x
-- Mathlib.CategoryTheory.Bicategory.Functor.Lax
CategoryTheory.LaxFunctor.map₂_leftUnitor_hom_app_assoc : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] (F : CategoryTheory.LaxFunctor B CategoryTheory.Cat) {a b : B}
  (f : a ⟶ b) (X : ↑(F.obj a)) {Z : ↑(F.obj b)}
  (h : (F.map f).toFunctor.obj ((CategoryTheory.CategoryStruct.id (F.obj a)).toFunctor.obj X) ⟶ Z),
  h =
    CategoryTheory.CategoryStruct.comp ((F.map f).toFunctor.map ((F.mapId a).toNatTrans.app X))
      (CategoryTheory.CategoryStruct.comp ((F.mapComp (CategoryTheory.CategoryStruct.id a) f).toNatTrans.app X)
        (CategoryTheory.CategoryStruct.comp ((F.map₂ (CategoryTheory.Bicategory.leftUnitor f).hom).toNatTrans.app X) h))
-- Mathlib.Topology.MetricSpace.Dilation
/-- The underlying function.

Do NOT use directly. Use the coercion instead.  -/
Dilation.toFun : {α : Type u_1} → {β : Type u_2} → [inst : PseudoEMetricSpace α] → [inst_1 : PseudoEMetricSpace β] → α →ᵈ β → α → β
-- Mathlib.CategoryTheory.ObjectProperty.Opposite
CategoryTheory.ObjectProperty.opEquivalence_inverse : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C),
  P.opEquivalence.inverse = P.op.lift P.ι.op ⋯
-- Mathlib.CategoryTheory.Bicategory.CatEnriched
CategoryTheory.CatEnrichedOrdinary.hComp_id_heq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.EnrichedOrdinaryCategory CategoryTheory.Cat C] {a b : CategoryTheory.CatEnrichedOrdinary C}
  {f f' : a ⟶ b} (η : f ⟶ f'),
  CategoryTheory.CatEnrichedOrdinary.hComp η (CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.id b)) ≍ η
-- Init.Internal.Order.Lemmas
Lean.Order.List.monotone_forIn' : ∀ {m : Type u → Type v} [inst : Monad m] [inst_1 : (α : Type u) → Lean.Order.PartialOrder (m α)] [Lean.Order.MonoBind m]
  {β : Type u} {γ : Type w} [inst_3 : Lean.Order.PartialOrder γ] {α : Type uu} (as : List α) (init : β)
  (f : γ → (a : α) → a ∈ as → β → m (ForInStep β)),
  Lean.Order.monotone f → Lean.Order.monotone fun x => forIn' as init (f x)
-- Mathlib.Topology.MetricSpace.PartitionOfUnity
/-- **Alias** of `Metric.exists_continuous_real_forall_closedEBall_subset`.

---

Let `X` be an extended metric space. Let `K : ι → Set X` be a locally finite family of closed
sets, let `U : ι → Set X` be a family of open sets such that `K i ⊆ U i` for all `i`. Then there
exists a positive continuous function `δ : C(X, ℝ)` such that for any `i` and `x ∈ K i`,
we have `Metric.closedEBall x (ENNReal.ofReal (δ x)) ⊆ U i`.  -/
EMetric.exists_continuous_real_forall_closedBall_subset : ∀ {ι : Type u_1} {X : Type u_2} [inst : EMetricSpace X] {K U : ι → Set X},
  (∀ (i : ι), IsClosed (K i)) →
    (∀ (i : ι), IsOpen (U i)) →
      (∀ (i : ι), K i ⊆ U i) →
        LocallyFinite K →
          ∃ δ, (∀ (x : X), 0 < δ x) ∧ ∀ (i : ι), ∀ x ∈ K i, Metric.closedEBall x (ENNReal.ofReal (δ x)) ⊆ U i
-- Mathlib.Algebra.Order.Ring.Unbundled.Rat
NNRatCast.toOfScientific : {K : Type u_1} → [NNRatCast K] → OfScientific K
-- Mathlib.Analysis.AperiodicOrder.Delone.Basic
Delone.DeloneSet.instMembership : {X : Type u_1} → [inst : MetricSpace X] → Membership X (Delone.DeloneSet X)
-- Mathlib.Computability.AkraBazzi.SumTransform
/-- `g` grows polynomially  -/
AkraBazziRecurrence.g_grows_poly : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : Nonempty α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ}
  (self : AkraBazziRecurrence T g a b r), AkraBazziRecurrence.GrowsPolynomially g
-- Mathlib.Algebra.Star.Rat
star_ratCast : ∀ {R : Type u_1} [inst : DivisionRing R] [inst_1 : StarRing R] (r : ℚ), star ↑r = ↑r
-- Mathlib.CategoryTheory.Limits.Over
CategoryTheory.Over.liftCocone_pt : ∀ {J : Type w} [inst : CategoryTheory.Category.{w', w} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone F) {X : C} (f : c.pt ⟶ X),
  (CategoryTheory.Over.liftCocone c f).pt = CategoryTheory.Over.mk f
-- Mathlib.NumberTheory.NumberField.Units.Basic
IsPrimitiveRoot.coe_coe_iff : ∀ {K : Type u_1} [inst : Field K] {ν : (NumberField.RingOfIntegers K)ˣ} {n : ℕ},
  IsPrimitiveRoot ((algebraMap (NumberField.RingOfIntegers K) K) ↑ν) n ↔ IsPrimitiveRoot ν n
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
mul_nonneg_iff_of_pos_right : ∀ {R : Type u} [inst : Semiring R] [inst_1 : LinearOrder R] {b c : R} [MulPosStrictMono R], 0 < c → (0 ≤ b * c ↔ 0 ≤ b)
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
/-- Adjunction between identities.  -/
CategoryTheory.Bicategory.Adjunction.id : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    (a : B) →
      CategoryTheory.Bicategory.Adjunction (CategoryTheory.CategoryStruct.id a) (CategoryTheory.CategoryStruct.id a)
-- Std.Time.DateTime
/-- Subtract `Month.Offset` from a `DateTime`, rolling over excess days.
 -/
Std.Time.DateTime.subMonthsRollOver : Std.Time.DateTime → Std.Time.Month.Offset → Std.Time.DateTime
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
WeierstrassCurve.Jacobian.smul_fin3_ext : ∀ {R : Type r} [inst : CommRing R] (P : Fin 3 → R) (u : R),
  (u • P) 0 = u ^ 2 * P 0 ∧ (u • P) 1 = u ^ 3 * P 1 ∧ (u • P) 2 = u * P 2
-- Init.Core
/-- An antisymmetric relation `r` satisfies `r a b → r b a → a = b`.  -/
Std.Antisymm.antisymm : ∀ {α : Sort u} {r : α → α → Prop} [self : Std.Antisymm r] (a b : α), r a b → r b a → a = b
-- Std.Async.Basic
/-- Represents monads that can launch computations asynchronously of type `t` in a monad `m`.
 -/
Std.Async.MonadAsync : (Type → Type) → (Type → Type) → Type 1
-- Mathlib.Algebra.Group.Subgroup.Actions
AddSubgroup.instVAddAssocClassSubtypeMem : ∀ {G : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddGroup G] [inst_1 : VAdd α β] [inst_2 : AddAction G α]
  [inst_3 : AddAction G β] [VAddAssocClass G α β] (S : AddSubgroup G), VAddAssocClass (↥S) α β
-- Mathlib.Data.Multiset.Fold
Multiset.fold_cons'_left : ∀ {α : Type u_1} (op : α → α → α) [hc : Std.Commutative op] [ha : Std.Associative op] (b a : α) (s : Multiset α),
  Multiset.fold op b (a ::ₘ s) = Multiset.fold op (op a b) s
-- Mathlib.Data.Subtype
exists_subtype_mk_eq_iff : ∀ {α : Sort u_1} {p : α → Prop} {a : Subtype p} {b : α}, (∃ (h : p b), ⟨b, h⟩ = a) ↔ b = ↑a
-- Init.Data.Array.Find
Array.find?_pmap : ∀ {α : Type u_1} {β : Type u_2} {P : α → Prop} {f : (a : α) → P a → β} {xs : Array α} (H : ∀ a ∈ xs, P a)
  {p : β → Bool},
  Array.find? p (Array.pmap f xs H) =
    Option.map
      (fun x =>
        match x with
        | ⟨a, m⟩ => f a ⋯)
      (Array.find?
        (fun x =>
          match x with
          | ⟨a, m⟩ => p (f a ⋯))
        xs.attach)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
SimpleGraph.Walk.getVert_cons : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} {n : ℕ} (p : G.Walk v w) (h : G.Adj u v),
  n ≠ 0 → (SimpleGraph.Walk.cons h p).getVert n = p.getVert (n - 1)
-- Mathlib.Algebra.Group.Hom.Defs
/-- The proposition that the function preserves 1  -/
OneHomClass.map_one : ∀ {F : Type u_10} {M : outParam (Type u_11)} {N : outParam (Type u_12)} {inst : One M} {inst_1 : One N}
  {inst_2 : FunLike F M N} [self : OneHomClass F M N] (f : F), f 1 = 1
-- Batteries.Data.Vector.Basic
_private.Batteries.Data.Vector.Basic.0.Vector.scanlMFast.loop : {m : Type u_1 → Type u_2} →
  {β : Type u_1} →
    {α : Type u_3} →
      {n : ℕ} →
        [Monad m] →
          (β → α → m β) →
            Vector α n →
              n < USize.size →
                β → (i n_usize : USize) → n_usize.toNat = n → i.toNat ≤ n → Vector β i.toNat → m (Vector β (n + 1))
-- Lean.ParserCompiler
/-- Takes an expression of type `Parser`, and determines the syntax kind of the root node it produces.  -/
Lean.ParserCompiler.parserNodeKind? : Lean.Expr → Lean.MetaM (Option Lean.Name)
-- Mathlib.Order.SuccPred.Basic
Order.lt_succ_iff_eq_or_lt : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : SuccOrder α] {a b : α} [NoMaxOrder α],
  a < Order.succ b ↔ a = b ∨ a < b
-- Init.Data.String.Iterator
String.Iterator : Type
-- Init.Data.List.Basic
/-- The first list is a non-contiguous sub-list of the second list. Typically written with the `<+`
operator.

In other words, `l₁ <+ l₂` means that `l₁` can be transformed into `l₂` by repeatedly inserting new
elements.
 -/
List.Sublist : {α : Type u_1} → List α → List α → Prop
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.kernelFactorThruImage_inv_comp_ι_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasKernel f] [inst_3 : CategoryTheory.Limits.HasImage f]
  [inst_4 : CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.factorThruImage f)] {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelFactorThruImage f).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι (CategoryTheory.Limits.factorThruImage f))
        h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι f) h
-- Mathlib.Combinatorics.SimpleGraph.Density
SimpleGraph.edgeDensity_empty_left : ∀ {α : Type u_4} (G : SimpleGraph α) [inst : DecidableRel G.Adj] (t : Finset α), G.edgeDensity ∅ t = 0
-- Mathlib.Combinatorics.Young.YoungDiagram
YoungDiagram.decidableMem : (μ : YoungDiagram) → DecidablePred fun x => x ∈ μ
-- Mathlib.Topology.LocallyFinite
LocallyFinite.continuous : ∀ {ι : Type u_1} {X : Type u_4} {Y : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : ι → Set X}
  {g : X → Y},
  LocallyFinite f → ⋃ i, f i = Set.univ → (∀ (i : ι), IsClosed (f i)) → (∀ (i : ι), ContinuousOn g (f i)) → Continuous g
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toList_rco_ne_nil_iff : ∀ {m n : ℤ}, (m...n).toList ≠ [] ↔ m < n
-- Init.Meta.Defs
Lean.Meta.ApplyNewGoals.nonDependentOnly.sizeOf_spec : sizeOf Lean.Meta.ApplyNewGoals.nonDependentOnly = 1
-- Mathlib.Analysis.Calculus.DSlope
dslope_sub_smul_of_ne : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {a b : 𝕜} (f : 𝕜 → E), b ≠ a → dslope (fun x => (x - a) • f x) a b = f b
-- Mathlib.CategoryTheory.ObjectProperty.Kernels
CategoryTheory.ObjectProperty.isClosedUnderKernels_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (P : CategoryTheory.ObjectProperty C),
  P.IsClosedUnderKernels ↔ (CategoryTheory.MorphismProperty.ofObjectProperty P P).kernels ≤ P
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
AddSubmonoid.inclusion.congr_simp : ∀ {M : Type u_1} [inst : AddZeroClass M] {S T : AddSubmonoid M} (h : S ≤ T),
  AddSubmonoid.inclusion h = AddSubmonoid.inclusion h
-- Batteries.Data.Char.Basic
_private.Batteries.Data.Char.Basic.0.Char.of_all_eq_true_aux : ∀ {p : Char → Bool}, Char.all p = true → ∀ (n : ℕ) (hn : n.isValidChar), p (Char.ofNatAux n hn) = true
-- Mathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit
CategoryTheory.Limits.WeightedCone.mk_π : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  {W : CategoryTheory.Functor J (Type w)} {F : CategoryTheory.Functor J C} (pt : C)
  (π : ⦃j : J⦄ → W.obj j → (pt ⟶ F.obj j))
  (hπ :
    ∀ ⦃j₁ j₂ : J⦄ (x : W.obj j₁) (f : j₁ ⟶ j₂),
      CategoryTheory.CategoryStruct.comp (π x) (F.map f) = π ((CategoryTheory.ConcreteCategory.hom (W.map f)) x))
  {j : J} (x : W.obj j), (CategoryTheory.Limits.WeightedCone.mk pt π hπ).π x = π x