mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.Padics.Measure.Basic
/-- The defining equivalence between measures and continuous linear maps on continuous functions.  -/
AbstractMeasure.toCLMEquiv : {X : Type u_1} →
  {R : Type u_3} →
    {E : Type u_4} →
      [inst : TopologicalSpace X] →
        [inst_1 : AddCommGroup E] →
          [inst_2 : TopologicalSpace E] →
            [inst_3 : IsTopologicalAddGroup E] →
              [inst_4 : CommRing R] →
                [inst_5 : TopologicalSpace R] →
                  [inst_6 : IsTopologicalRing R] →
                    [inst_7 : Module R E] → [inst_8 : ContinuousSMul R E] → AbstractMeasure X R E ≃ₗ[R] C(X, R) →L[R] E
-- Mathlib.Probability.Process.LocalProperty
/-- A stable property holding locally is idempotent.  -/
ProbabilityTheory.IsStable.locally_locally_iff : ∀ {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω}
  [inst : ConditionallyCompleteLinearOrderBot ι] [inst_1 : TopologicalSpace ι] [inst_2 : OrderTopology ι]
  {𝓕 : MeasureTheory.Filtration ι mΩ} {X : ι → Ω → E} {p : (ι → Ω → E) → Prop} [SecondCountableTopology ι]
  [MeasureTheory.IsFiniteMeasure P] [DenselyOrdered ι] [NoMaxOrder ι] [inst_7 : Zero E] [𝓕.IsRightContinuous],
  ProbabilityTheory.IsStable 𝓕 p →
    (ProbabilityTheory.Locally (fun Y => ProbabilityTheory.Locally p 𝓕 Y P) 𝓕 X P ↔ ProbabilityTheory.Locally p 𝓕 X P)
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.ExBase.sum.inj : ∀ {u : Lean.Level} {α : Q(Type u)} {BaseType : Q(«$α») → Type} {sα : Q(CommSemiring «$α»)} {e : Q(«$α»)}
  {x x_1 : Mathlib.Tactic.Ring.Common.ExSum BaseType sα e},
  Mathlib.Tactic.Ring.Common.ExBase.sum x = Mathlib.Tactic.Ring.Common.ExBase.sum x_1 → x = x_1
-- Init.Grind.ToInt
_private.Init.Grind.ToInt.0.Lean.Grind.IntInterval.lo?.match_1.eq_3 : ∀ (motive : Lean.Grind.IntInterval → Sort u_1) (hi : ℤ) (h_1 : (lo hi : ℤ) → motive (Lean.Grind.IntInterval.co lo hi))
  (h_2 : (lo : ℤ) → motive (Lean.Grind.IntInterval.ci lo)) (h_3 : (hi : ℤ) → motive (Lean.Grind.IntInterval.io hi))
  (h_4 : Unit → motive Lean.Grind.IntInterval.ii),
  (match Lean.Grind.IntInterval.io hi with
    | Lean.Grind.IntInterval.co lo hi => h_1 lo hi
    | Lean.Grind.IntInterval.ci lo => h_2 lo
    | Lean.Grind.IntInterval.io hi => h_3 hi
    | Lean.Grind.IntInterval.ii => h_4 ()) =
    h_3 hi
-- Mathlib.Algebra.Order.Field.Basic
IsLUB.mul_left : ∀ {α : Type u_2} [inst : Semifield α] [inst_1 : PartialOrder α] [PosMulReflectLT α] {a b : α} [IsStrictOrderedRing α]
  {s : Set α}, 0 ≤ a → IsLUB s b → IsLUB ((fun b => a * b) '' s) (a * b)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.forIn_eq_forIn_toList : ∀ {α : Type u} {β : α → Type v} {t : Std.DTreeMap.Internal.Impl α β} {δ : Type w} {m : Type w → Type w'}
  [inst : Monad m] [LawfulMonad m] {f : (a : α) × β a → δ → m (ForInStep δ)} {init : δ},
  Std.DTreeMap.Internal.Impl.forIn (fun k v => f ⟨k, v⟩) init t = forIn t.toList init f
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
/-- The functor which sends `A : X.Subcomplex` to `A.toSSet`.  -/
SSet.Subcomplex.toSSetFunctor : {X : SSet} → CategoryTheory.Functor X.Subcomplex SSet
-- Mathlib.Topology.Inseparable
/-- **Alias** of the forward direction of `specializes_iff_pure`. -/
Specializes.pure_le_nhds : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X}, x ⤳ y → pure x ≤ nhds y
-- Mathlib.Data.Matrix.Mul
Matrix.mulVec_diagonal : ∀ {m : Type u_2} {α : Type v} [inst : NonUnitalNonAssocSemiring α] [inst_1 : Fintype m] [inst_2 : DecidableEq m]
  (v w : m → α) (x : m), (Matrix.diagonal v).mulVec w x = v x * w x
-- Mathlib.Combinatorics.SimpleGraph.Dart
SimpleGraph.Dart.mk : {V : Type u_1} → {G : SimpleGraph V} → (toProd : V × V) → G.Adj toProd.1 toProd.2 → G.Dart
-- Init.Data.List.Basic
List.filterTR.loop.eq_2 : ∀ {α : Type u} (p : α → Bool) (a : List α) (a_1 : α) (l : List α),
  List.filterTR.loop p (a_1 :: l) a =
    match p a_1 with
    | true => List.filterTR.loop p l (a_1 :: a)
    | false => List.filterTR.loop p l a
-- Mathlib.Order.WithBot
WithBot.forall_coe_le_iff_le : ∀ {α : Type u_1} [inst : Preorder α] {x y : WithBot α} [NoBotOrder α], (∀ (a : α), ↑a ≤ x → ↑a ≤ y) ↔ x ≤ y
-- Mathlib.CategoryTheory.WithTerminal.Basic
/-- Formally adjoin a terminal object to a category.  -/
CategoryTheory.WithTerminal : Type u → Type u
-- Mathlib.Data.Nat.GCD.Basic
Nat.coprime_one_left_iff : ∀ (n : ℕ), Nat.Coprime 1 n ↔ True
-- Mathlib.Algebra.Order.GroupWithZero.Basic
one_le_zpow_iff_right₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀} [ZeroLEOneClass G₀]
  {n : ℤ}, 1 < a → (1 ≤ a ^ n ↔ 0 ≤ n)
-- Mathlib.Data.Fin.VecNotation
/-- `mkVecLiteralQ ![x, y, z]` produces the term `q(![$x, $y, $z])`.  -/
PiFin.mkLiteralQ : {u : Lean.Level} → {α : Q(Type u)} → {n : ℕ} → (Fin n → Q(«$α»)) → Q(Fin «$n» → «$α»)
-- Mathlib.FieldTheory.Finite.GaloisField
instFieldGaloisField : (p : ℕ) → [inst : Fact (Nat.Prime p)] → (n : ℕ) → Field (GaloisField p n)
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
SSet.OneTruncation₂.nerveHomEquiv_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (X : SSet.OneTruncation₂ ((SSet.truncation 2).obj (CategoryTheory.nerve C))),
  SSet.OneTruncation₂.nerveHomEquiv (CategoryTheory.ReflQuiver.id X) =
    CategoryTheory.CategoryStruct.id (SSet.OneTruncation₂.nerveEquiv X)
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.coe_eq_one : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (S : Subalgebra R A)
  {x : ↥S}, ↑x = 1 ↔ x = 1
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.eval_sub : ∀ {R : Type u} [inst : Ring R] (p q : Polynomial R) (x : R),
  Polynomial.eval x (p - q) = Polynomial.eval x p - Polynomial.eval x q
-- Mathlib.Data.Nat.Log
Nat.clog_eq_one : ∀ {b n : ℕ}, 2 ≤ n → n ≤ b → Nat.clog b n = 1
-- Mathlib.GroupTheory.SemidirectProduct
SemidirectProduct.instMul : {N : Type u_1} → {G : Type u_2} → [inst : Group N] → [inst_1 : Group G] → {φ : G →* MulAut N} → Mul (N ⋊[φ] G)
-- Mathlib.CategoryTheory.Iso
CategoryTheory.IsIso.inv_comp_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {h : Y ⟶ Z}
  [inst_1 : CategoryTheory.IsIso f] [inst_2 : CategoryTheory.IsIso h] {Z_1 : C} (h_1 : X ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.CategoryStruct.comp f h)) h_1 =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.inv h)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.inv f) h_1)
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.AffineScheme.Spec_faithful : AlgebraicGeometry.AffineScheme.Spec.Faithful
-- Mathlib.CategoryTheory.Groupoid
/-- The inverse morphism  -/
CategoryTheory.Groupoid.inv : {obj : Type u} → [self : CategoryTheory.Groupoid obj] → {X Y : obj} → (X ⟶ Y) → (Y ⟶ X)
-- Std.Data.Iterators.Lemmas.Producers.Range
Std.Rci.count_iter : ∀ {α : Type u_1} [inst : Std.PRange.UpwardEnumerable α] [Std.Rxi.IsAlwaysFinite α]
  [inst_2 : Std.PRange.LawfulUpwardEnumerable α] [inst_3 : Std.Rxi.HasSize α] [Std.Rxi.LawfulHasSize α] {r : Std.Rci α},
  r.iter.length = r.size
-- Lean.Meta.DiscrTree.Main
_private.Lean.Meta.DiscrTree.Main.0.Lean.Meta.DiscrTree.isNatType : Lean.Expr → Lean.MetaM Bool
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue?_insertListConst_of_contains_eq_false : ∀ {α : Type u} {β : Type v} [inst : BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {toInsert : List (α × β)}
  {k : α},
  (List.map Prod.fst toInsert).contains k = false →
    Std.Internal.List.getValue? k (Std.Internal.List.insertListConst l toInsert) = Std.Internal.List.getValue? k l
-- Mathlib.CategoryTheory.Limits.Shapes.Products
/-- An iterated product is a product over a sigma type.  -/
CategoryTheory.Limits.piPiIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {ι : Type u_1} →
      (f : ι → Type u_2) →
        (g : (i : ι) → f i → C) →
          [inst_1 : ∀ (i : ι), CategoryTheory.Limits.HasProduct (g i)] →
            [inst_2 : CategoryTheory.Limits.HasProduct fun i => ∏ᶜ g i] →
              (∏ᶜ fun i => ∏ᶜ g i) ≅ ∏ᶜ fun p => g p.fst p.snd
-- Mathlib.CategoryTheory.ConcreteCategory.Basic
CategoryTheory.ConcreteCategory.id_apply : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {FC : outParam (C → C → Type u_1)} {CC : outParam (C → Type w)}
  {inst_1 : outParam ((X Y : C) → FunLike (FC X Y) (CC X) (CC Y))} [self : CategoryTheory.ConcreteCategory C FC] {X : C}
  (x : CC X), (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) x = x
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Poly.of_denote_eq_cancel : ∀ {ctx : Nat.Internal.Linear.Context} {m₁ m₂ : Nat.Internal.Linear.Poly},
  Nat.Internal.Linear.Poly.denote_eq ctx (m₁.cancel m₂) → Nat.Internal.Linear.Poly.denote_eq ctx (m₁, m₂)
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat.0.Nat.mkEqNat : Lean.Expr → Lean.Expr → Lean.Expr
-- Mathlib.Order.BooleanAlgebra.Set
Set.sdiff_self : ∀ {α : Type u_1} {s : Set α}, s \ s = ∅
-- Mathlib.Algebra.Order.UpperLower
UpperSet.instMul.eq_1 : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : Preorder α] [inst_2 : IsOrderedMonoid α],
  UpperSet.instMul = { mul := fun s t => { carrier := Set.image2 (fun x1 x2 => x1 * x2) ↑s ↑t, upper' := ⋯ } }
-- Mathlib.RingTheory.Coalgebra.Quotient
Submodule.isCoideal_iff : ∀ {R : Type u_1} {C : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup C] [inst_2 : Module R C]
  [inst_3 : CoalgebraStruct R C] (I : Submodule R C),
  I.IsCoideal ↔
    (∀ ⦃x : C⦄, x ∈ I → CoalgebraStruct.counit x = 0) ∧
      ∀ ⦃x : C⦄, x ∈ I → (TensorProduct.map I.mkQ I.mkQ) (CoalgebraStruct.comul x) = 0
-- Mathlib.RingTheory.MvPolynomial.Homogeneous
/-- A multivariate polynomial `φ` is homogeneous of degree `n`
if all monomials occurring in `φ` have degree `n`.  -/
MvPolynomial.IsHomogeneous : {σ : Type u_1} → {R : Type u_3} → [inst : CommSemiring R] → MvPolynomial σ R → ℕ → Prop
-- Mathlib.Algebra.Algebra.Defs
algebraMap.coe_one : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A], ↑1 = 1
-- Mathlib.Order.SuccPred.Archimedean
/-- Induction principle on a type with a `SuccOrder` for all elements above a given element `m`.  -/
Succ.rec : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] [IsSuccArchimedean α] {m : α} {P : (n : α) → m ≤ n → Prop},
  P m ⋯ → (∀ (n : α) (hmn : m ≤ n), P n hmn → P (Order.succ n) ⋯) → ∀ ⦃n : α⦄ (hmn : m ≤ n), P n hmn
-- Mathlib.Geometry.Convex.Cone.Basic
ConvexCone.Salient.eq_1 : ∀ {R : Type u_2} {G : Type u_3} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup G]
  [inst_3 : SMul R G] (C : ConvexCone R G), C.Salient = ∀ x ∈ C, x ≠ 0 → -x ∉ C
-- Mathlib.Algebra.MonoidAlgebra.Basic
MonoidAlgebra.coeff_toAdditiveAlgEquiv_symm_apply : ∀ (R : Type u_1) (A : Type u_4) (M : Type u_7) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Monoid M] (x : AddMonoidAlgebra A (Additive M)),
  ((MonoidAlgebra.toAdditiveAlgEquiv R A M).symm x).coeff = Finsupp.mapDomain (⇑Additive.toMul) x.coeff
-- Lean.Syntax
/-- Remark: the State `String.Pos` is the `SourceInfo.trailing.stopPos` of the previous token,
or the beginning of the String.  -/
_private.Lean.Syntax.0.Lean.Syntax.updateLeadingAux : Lean.Syntax → StateM String.Pos.Raw (Option Lean.Syntax)
-- Mathlib.RingTheory.PowerSeries.Inverse
/-- The maximal ideal of `k⟦X⟧` is generated by `X`.  -/
PowerSeries.maximalIdeal_eq_span_X : ∀ {k : Type u_2} [inst : Field k], IsLocalRing.maximalIdeal (PowerSeries k) = Ideal.span {PowerSeries.X}
-- Mathlib.Algebra.Category.Grp.EpiMono
AddGrpCat.forget_grp_preserves_mono : (CategoryTheory.forget AddGrpCat).PreservesMonomorphisms
-- Mathlib.Topology.Order.LocalExtr
/-- `IsLocalMin f a` means that `f a ≤ f x` for all `x` in some neighborhood of `a`.  -/
IsLocalMin : {α : Type u} → {β : Type v} → [TopologicalSpace α] → [Preorder β] → (α → β) → α → Prop
-- Mathlib.Analysis.Calculus.FDeriv.Measurable
RightDerivMeasurableAux.norm_sub_le_of_mem_A : ∀ {F : Type u_1} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {f : ℝ → F} {r x : ℝ},
  0 < r →
    ∀ (ε : ℝ) {L₁ L₂ : F},
      x ∈ RightDerivMeasurableAux.A f L₁ r ε → x ∈ RightDerivMeasurableAux.A f L₂ r ε → ‖L₁ - L₂‖ ≤ 4 * ε
-- Std.Sat.AIG.CNF
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.Cache.mk.inj : ∀ {aig : Std.Sat.AIG ℕ} {cnf : Std.Sat.CNF ℕ} {marks : Array Bool} {hmarks : marks.size = aig.decls.size}
  {inv : Std.Sat.AIG.toCNF.Cache.Inv✝ aig cnf marks hmarks} {marks_1 : Array Bool}
  {hmarks_1 : marks_1.size = aig.decls.size} {inv_1 : Std.Sat.AIG.toCNF.Cache.Inv✝ aig cnf marks_1 hmarks_1},
  { marks := marks, hmarks := hmarks, inv := inv } = { marks := marks_1, hmarks := hmarks_1, inv := inv_1 } →
    marks = marks_1
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
/-- If `g : ℝ → ℝ` is periodic with period `T > 0` and `∀ x, 0 < g x`, then `t ↦ ∫ x in 0..t, g x`
tends to `-∞` as `t` tends to `-∞`.  -/
Function.Periodic.tendsto_atBot_intervalIntegral_of_pos' : ∀ {T : ℝ} {g : ℝ → ℝ},
  Function.Periodic g T →
    IntervalIntegrable g MeasureTheory.volume 0 T →
      (∀ (x : ℝ), 0 < g x) → 0 < T → Filter.Tendsto (fun t => ∫ (x : ℝ) in 0..t, g x) Filter.atBot Filter.atBot
-- Mathlib.AlgebraicGeometry.Birational.Birational
AlgebraicGeometry.Scheme.PartialIso.symm_source : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X.PartialIso Y), f.symm.source = f.target
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.min'_zero : ∀ {α : Type u_2} [inst : Zero α] [inst_1 : LinearOrder α], Finset.min' 0 ⋯ = 0
-- Mathlib.CategoryTheory.Idempotents.Biproducts
/-- The `Bicone` used in order to obtain the existence of
the biproduct of a functor `J ⥤ Karoubi C` when the category `C` is additive.  -/
CategoryTheory.Idempotents.Karoubi.Biproducts.bicone : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [CategoryTheory.Limits.HasFiniteBiproducts C] →
        {J : Type} → [Finite J] → (F : J → CategoryTheory.Idempotents.Karoubi C) → CategoryTheory.Limits.Bicone F
-- Mathlib.RingTheory.MvPowerSeries.Evaluation
MvPowerSeries.continuous_aeval : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommRing R] [inst_1 : UniformSpace R] {S : Type u_3} [inst_2 : CommRing S]
  [inst_3 : UniformSpace S] {a : σ → S} [inst_4 : IsTopologicalSemiring R] [inst_5 : IsUniformAddGroup R]
  [inst_6 : IsUniformAddGroup S] [inst_7 : CompleteSpace S] [inst_8 : T2Space S] [inst_9 : IsTopologicalRing S]
  [inst_10 : IsLinearTopology S S] [inst_11 : Algebra R S] [inst_12 : ContinuousSMul R S]
  (ha : MvPowerSeries.HasEval a), Continuous ⇑(MvPowerSeries.aeval ha)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonFoldingRangeParams : Lean.ToJson Lean.Lsp.FoldingRangeParams
-- Mathlib.LinearAlgebra.CliffordAlgebra.Even
CliffordAlgebra.EvenHom.contract : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} {A : Type u_3} [inst_3 : Ring A] [inst_4 : Algebra R A] (self : CliffordAlgebra.EvenHom Q A)
  (m : M), (self.bilin m) m = (algebraMap R A) (Q m)
-- Mathlib.LinearAlgebra.Transvection.Basic
LinearEquiv.dilatransvection.apply : ∀ {R : Type u_1} {V : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : Module R V] {f : Module.Dual R V}
  {v : V} {h : IsUnit (1 + f v)} {x : V}, (LinearEquiv.dilatransvection h) x = x + f x • v
-- Mathlib.Algebra.Homology.CommSq
/-- The colimit cokernel cofork attached to a pushout square.  -/
CategoryTheory.IsPushout.isColimitCokernelCofork : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {X₁ X₂ X₃ X₄ : C} →
        [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X₂ X₃] →
          {f : X₁ ⟶ X₂} →
            {g : X₁ ⟶ X₃} →
              {inl : X₂ ⟶ X₄} →
                {inr : X₃ ⟶ X₄} →
                  (h : CategoryTheory.IsPushout f g inl inr) → CategoryTheory.Limits.IsColimit ⋯.cokernelCofork
-- Mathlib.Topology.Order.OrderClosed
instOrderClosedTopologyOrderDual : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : Preorder α] [t : OrderClosedTopology α], OrderClosedTopology αᵒᵈ
-- Init.Data.UInt.Lemmas
UInt16.mod_one : ∀ {a : UInt16}, a % 1 = 0
-- Lean.Parser.Extension
Lean.Parser.mkParserOfConstantUnsafe : Lean.Name → (Lean.ParserDescr → Lean.ImportM Lean.Parser.Parser) → Lean.ImportM (Bool × Lean.Parser.Parser)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.self_le_maxKey_insert : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  (h : t.WF) {k : α} {v : β k}, (compare k ((Std.DTreeMap.Internal.Impl.insert k v t ⋯).impl.maxKey ⋯)).isLE = true
-- Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
/-- **Alias** of `CategoryTheory.NatTrans.Coequifibered.of_isIso`. -/
AlgebraicGeometry.Scheme.preservesLocalization_toOpensFunctor : ∀ {J : Type u_1} {C : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_3} C] {F G : CategoryTheory.Functor J C} (α : F ⟶ G)
  [CategoryTheory.IsIso α], CategoryTheory.NatTrans.Coequifibered α
-- Mathlib.Analysis.Calculus.Deriv.Abs
Differentiable.abs : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ},
  Differentiable ℝ f → (∀ (x : E), f x ≠ 0) → Differentiable ℝ fun x => |f x|
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoMod_sub_ofNat_mul : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedAddMonoid R]
  [inst_3 : Archimedean R] {p : R} (hp : 0 < p) (a b : R) (m : ℕ) [inst_4 : m.AtLeastTwo],
  toIcoMod hp a (b - OfNat.ofNat m * p) = toIcoMod hp a b
-- Batteries.Recycling.RBTree.Alter
RBTree.RBNode.Path.Ordered.eq_2 : ∀ {α : Type u_1} (cmp : α → α → Ordering) (c : RBTree.RBColor) (parent : RBTree.RBNode.Path α) (x_1 : α)
  (r : RBTree.RBNode α),
  RBTree.RBNode.Path.Ordered cmp (RBTree.RBNode.Path.left c parent x_1 r) =
    (RBTree.RBNode.Path.Ordered cmp parent ∧
      RBTree.RBNode.All (fun x => RBTree.RBNode.cmpLT cmp x_1 x) r ∧
        RBTree.RBNode.Path.RootOrdered cmp parent x_1 ∧
          RBTree.RBNode.All (RBTree.RBNode.Path.RootOrdered cmp parent) r ∧ RBTree.RBNode.Ordered cmp r)
-- Mathlib.Combinatorics.SimpleGraph.Ends.Defs
/-- The components outside a given set of vertices `K`  -/
SimpleGraph.ComponentCompl : {V : Type u} → SimpleGraph V → Set V → Type u
-- Mathlib.Algebra.Category.MonCat.Colimits
/-- The relation on `Prequotient` saying when two expressions are equal
because of the monoid laws, or
because one element is mapped to another by a morphism in the diagram.
 -/
MonCat.Colimits.Relation : {J : Type v} →
  [inst : CategoryTheory.Category.{u, v} J] →
    (F : CategoryTheory.Functor J MonCat) → MonCat.Colimits.Prequotient F → MonCat.Colimits.Prequotient F → Prop
-- Mathlib.AlgebraicGeometry.Morphisms.LocalFlatDescent
AlgebraicGeometry.instDescendsAlongSchemeLocallyOfFiniteTypeMinMorphismPropertySurjectiveFlatQuasiCompact : CategoryTheory.MorphismProperty.DescendsAlong (@AlgebraicGeometry.LocallyOfFiniteType)
  (@AlgebraicGeometry.Surjective ⊓ @AlgebraicGeometry.Flat ⊓ @AlgebraicGeometry.QuasiCompact)
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.Raw₀.Const.modify_eq_modifyₘ : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  (m : Std.DHashMap.Internal.Raw₀ α fun x => β) (a : α) (f : β → β),
  Std.DHashMap.Internal.Raw₀.Const.modify m a f = Std.DHashMap.Internal.Raw₀.Const.modifyₘ m a f
-- Mathlib.Data.Finset.Insert
Finset.insert_ne_empty : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (s : Finset α), insert a s ≠ ∅
-- Mathlib.CategoryTheory.HomCongr
CategoryTheory.Iso.isoCongr_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ Y₁ X₂ Y₂ : C} (f : X₁ ≅ X₂) (g : Y₁ ≅ Y₂) (h : X₁ ≅ Y₁),
  (f.isoCongr g) h = f.symm ≪≫ h ≪≫ g
-- Mathlib.Analysis.Distribution.TemperateGrowth
ContinuousLinearEquiv.hasTemperateGrowth : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] (f : E ≃L[ℝ] F), Function.HasTemperateGrowth ⇑f
-- Init.Data.UInt.Bitwise
UInt8.or_eq_zero_iff : ∀ {a b : UInt8}, a ||| b = 0 ↔ a = 0 ∧ b = 0
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
List.aestronglyMeasurable_fun_prod : ∀ {α : Type u_1} {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {M : Type u_5} [inst : Monoid M]
  [inst_1 : TopologicalSpace M] [ContinuousMul M] (l : List (α → M)),
  (∀ f ∈ l, MeasureTheory.AEStronglyMeasurable f μ) →
    MeasureTheory.AEStronglyMeasurable (fun x => (List.map (fun f => f x) l).prod) μ
-- Lean.ScopedEnvExtension
Lean.registerScopedEnvExtension : {α β σ : Type} → Lean.ScopedEnvExtension.Descr α β σ → IO (Lean.ScopedEnvExtension α β σ)
-- Mathlib.MeasureTheory.OuterMeasure.Operations
MeasureTheory.OuterMeasure.comap_apply : ∀ {α : Type u_1} {β : Type u_3} (f : α → β) (m : MeasureTheory.OuterMeasure β) (s : Set α),
  ((MeasureTheory.OuterMeasure.comap f) m) s = m (f '' s)
-- Lean.Meta.Match.MVarRenaming
Lean.Meta.MVarRenaming.find! : Lean.Meta.MVarRenaming → Lean.MVarId → Lean.MVarId
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.sin_antiperiodic : Function.Antiperiodic Complex.sin ↑Real.pi
-- Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {W : CategoryTheory.MorphismProperty C} →
      {J : Type w} →
        [inst_1 : LinearOrder J] →
          [inst_2 : SuccOrder J] →
            [inst_3 : OrderBot J] →
              [inst_4 : WellFoundedLT J] →
                {X Y : C} →
                  {f : X ⟶ Y} →
                    (toTransfiniteCompositionOfShape : CategoryTheory.TransfiniteCompositionOfShape J f) →
                      (∀ (j : J), ¬IsMax j → W (toTransfiniteCompositionOfShape.F.map (CategoryTheory.homOfLE ⋯))) →
                        W.TransfiniteCompositionOfShape J f
-- Mathlib.Topology.Algebra.Module.Spaces.PointwiseConvergenceCLM
PointwiseConvergenceCLM.hasBasis_nhds_zero_of_basis : ∀ {𝕜₁ : Type u_4} {𝕜₂ : Type u_5} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_7}
  {F : Type u_8} [inst_2 : AddCommGroup E] [inst_3 : TopologicalSpace E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : IsTopologicalAddGroup F] [inst_7 : Module 𝕜₁ E] [inst_8 : Module 𝕜₂ F]
  {ι : Type u_11} {p : ι → Prop} {b : ι → Set F},
  (nhds 0).HasBasis p b → (nhds 0).HasBasis (fun Si => Finite ↑Si.1 ∧ p Si.2) fun Si => {f | ∀ x ∈ Si.1, f x ∈ b Si.2}
-- Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
_private.Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr.0.Lean.Meta.Grind.Arith.CommRing.denoteExprCore : {M : Type → Type} →
  [Monad M] →
    [Lean.MonadError M] →
      [MonadLiftT Lean.MetaM M] →
        [Lean.Meta.Sym.Arith.MonadCanon M] →
          [Lean.Meta.Grind.Arith.CommRing.MonadRing M] →
            (ℕ → Lean.Expr) → Lean.Meta.Grind.Arith.CommRing.RingExpr → M Lean.Expr
-- Init.Data.List.Scan.Basic
/-- Tail-recursive helper function for `scanlM` and `scanrM`  -/
_private.Init.Data.List.Scan.Basic.0.List.scanAuxM : {m : Type u_1 → Type u_2} → {β : Type u_1} → {α : Type u_3} → [Monad m] → (β → α → m β) → β → List α → m (List β)
-- Mathlib.GroupTheory.Nilpotent
/-- **Alias** of `Subgroup.upperCentralSeriesAux`.

---

An auxiliary type-theoretic definition defining both the upper central series of
a group, and a proof that it is characteristic, all in one go.  -/
upperCentralSeriesAux : (G : Type u_1) → [inst : Group G] → ℕ → (H : Subgroup G) ×' H.Characteristic
-- Mathlib.Topology.Constructible
Equiv.toHomeomorphOfIsInducing.eq_1 : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X ≃ Y)
  (hf : Topology.IsInducing ⇑f),
  f.toHomeomorphOfIsInducing hf = { toEquiv := f, continuous_toFun := ⋯, continuous_invFun := ⋯ }
-- Mathlib.Logic.Equiv.PartialEquiv
/-- **Alias** of `PartialEquiv.mapsTo_symm`. -/
PartialEquiv.symm_mapsTo : ∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β), Set.MapsTo (↑e.symm) e.target e.source