mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.OrderOfElement
IsOfFinAddOrder.addOrderOf_nsmul : ∀ {G : Type u_1} [inst : AddMonoid G] (x : G) (n : ℕ),
  IsOfFinAddOrder x → addOrderOf (n • x) = addOrderOf x / (addOrderOf x).gcd n
-- Mathlib.Order.Filter.Map
Filter.compl_mem_kernMap : ∀ {α : Type u_1} {β : Type u_2} {m : α → β} {f : Filter α} {s : Set β},
  sᶜ ∈ Filter.kernMap m f ↔ ∃ t, tᶜ ∈ f ∧ m '' t = s
-- Init.Data.UInt.Lemmas
UInt64.mul_sub : ∀ {a b c : UInt64}, a * (b - c) = a * b - a * c
-- Mathlib.Order.Filter.Map
Filter.map_injective : ∀ {α : Type u_1} {β : Type u_2} {m : α → β}, Function.Injective m → Function.Injective (Filter.map m)
-- Mathlib.CategoryTheory.GuitartExact.HorizontalComposition
/-- A 2-square is Guitart exact iff it is so after replacing the top and bottom functors by
isomorphic functors.  -/
CategoryTheory.TwoSquare.GuitartExact.whiskerHorizontal_iff : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_4} {D₂ : Type u_5} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_4, u_4} D₁]
  [inst_3 : CategoryTheory.Category.{v_5, u_5} D₂] {T : CategoryTheory.Functor C₁ D₁} {L : CategoryTheory.Functor C₁ C₂}
  {R : CategoryTheory.Functor D₁ D₂} {B : CategoryTheory.Functor C₂ D₂} (w : CategoryTheory.TwoSquare T L R B)
  {T' : CategoryTheory.Functor C₁ D₁} {B' : CategoryTheory.Functor C₂ D₂} (α : T ≅ T') (β : B ≅ B'),
  (w.whiskerHorizontal α.inv β.hom).GuitartExact ↔ w.GuitartExact
-- Mathlib.Combinatorics.Additive.Dissociation
addDissociated_neg : ∀ {α : Type u_1} [inst : AddCommGroup α] {s : Set α}, AddDissociated (-s) ↔ AddDissociated s
-- Lean.Elab.Term.TermElabM
/-- Like `Meta.withRestoreOrSaveFull` for `TermElabM`, but also takes a `tacSnap?` that
* when running `act`, is set as `Context.tacSnap?`
* otherwise (i.e. on restore) is used to update the new snapshot promise to the old task's
  value.
This extra restore step is necessary because while `reusableResult?` can be used to replay any
effects on `State`, `Context.tacSnap?` is not part of it but changed via an `IO` side effect, so
it needs to be replayed separately.

We use an explicit parameter instead of accessing `Context.tacSnap?` directly because this prevents
`withRestoreOrSaveFull` and `withReader` from being used in the wrong order.
 -/
Lean.Elab.Term.withRestoreOrSaveFull : {α : Type} →
  Option (α × Lean.Elab.Term.SavedState) →
    Option (Lean.Language.SnapshotBundle Lean.Elab.Tactic.TacticParsedSnapshot) →
      Lean.Elab.TermElabM α → Lean.Elab.TermElabM (α × Lean.Elab.Term.SavedState)
-- Mathlib.Algebra.Order.Interval.Set.SuccPred
Set.Ioc_sub_one_left_eq_Icc_of_not_isMin : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : Sub α] [PredSubOrder α] {a : α},
  ¬IsMin a → ∀ (b : α), Set.Ioc (a - 1) b = Set.Icc a b
-- Mathlib.Combinatorics.Enumerative.DyckWord
instInhabitedDyckStep.default : DyckStep
-- Mathlib.NumberTheory.LocalField.Basic
IsNonarchimedeanLocalField.mk : ∀ {K : Type u_1} [inst : Field K] [inst_1 : ValuativeRel K] [inst_2 : TopologicalSpace K]
  [toIsValuativeTopology : IsValuativeTopology K] [toLocallyCompactSpace : LocallyCompactSpace K]
  [toIsNontrivial : ValuativeRel.IsNontrivial K], IsNonarchimedeanLocalField K
-- Init.Data.String.Lemmas.Basic
String.sliceFrom_sliceTo : ∀ {s : String} {pos : s.Pos} {pos' : (s.sliceTo pos).Pos},
  (s.sliceTo pos).sliceFrom pos' = s.slice (String.Pos.ofSliceTo pos') pos ⋯
-- Mathlib.Dynamics.Minimal
IsOpen.exists_vadd_mem : ∀ (M : Type u_1) {α : Type u_3} [inst : AddMonoid M] [inst_1 : TopologicalSpace α] [inst_2 : AddAction M α]
  [AddAction.IsMinimal M α] (x : α) {U : Set α}, IsOpen U → U.Nonempty → ∃ c, c +ᵥ x ∈ U
-- Mathlib.CategoryTheory.Triangulated.TStructure.Basic
/-- The full subcategory consisting of `t`-bounded objects.  -/
CategoryTheory.Triangulated.TStructure.bounded : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        [inst_3 : CategoryTheory.HasShift C ℤ] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [inst_5 : CategoryTheory.Pretriangulated C] →
              CategoryTheory.Triangulated.TStructure C → CategoryTheory.ObjectProperty C
-- Mathlib.Algebra.Star.Module
starLinearEquiv_symm_apply : ∀ (R : Type u_1) {A : Type u_2} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : AddCommMonoid A]
  [inst_3 : StarAddMonoid A] [inst_4 : Module R A] [inst_5 : StarModule R A] (x : A),
  (starLinearEquiv R).symm x = starAddEquiv.invFun x
-- Mathlib.Data.Finset.PiInduction
/-- Given a predicate on functions `∀ i, Finset (α i)` defined on a finite type, it is true on all
maps provided that it is true on `fun _ ↦ ∅` and for any function `g : ∀ i, Finset (α i)`, an index
`i : ι`, and an element `x : α i` that is strictly greater than all elements of `g i`, `p g` implies
`p (update g i (insert x (g i)))`.

This lemma requires `LinearOrder` instances on all `α i`. See also `Finset.induction_on_pi` for a
version that needs `x ∉ g i` and does not need `∀ i, LinearOrder (α i)`.  -/
Finset.induction_on_pi_max : ∀ {ι : Type u_1} {α : ι → Type u_2} [Finite ι] [inst : DecidableEq ι] [inst_1 : (i : ι) → DecidableEq (α i)]
  [inst_2 : (i : ι) → LinearOrder (α i)] {p : ((i : ι) → Finset (α i)) → Prop} (f : (i : ι) → Finset (α i)),
  (p fun x => ∅) →
    (∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i),
        (∀ y ∈ g i, y < x) → p g → p (Function.update g i (insert x (g i)))) →
      p f
-- Mathlib.Geometry.Convex.Cone.Basic
ConvexCone.Blunt.eq_1 : ∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommMonoid M]
  [inst_3 : SMul R M] (C : ConvexCone R M), C.Blunt = (0 ∉ C)
-- Mathlib.Topology.Maps.Basic
Topology.IsQuotientMap.of_inverse : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {g : Y → X},
  Continuous f → Continuous g → Function.LeftInverse g f → Topology.IsQuotientMap g
-- Mathlib.Analysis.SpecialFunctions.Gamma.Beta
/-- Relation between Beta integral and Gamma function.  -/
Complex.Gamma_mul_Gamma_eq_betaIntegral : ∀ {s t : ℂ}, 0 < s.re → 0 < t.re → Complex.Gamma s * Complex.Gamma t = Complex.Gamma (s + t) * s.betaIntegral t
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey_alter_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] [Inhabited α],
  t.WF → ∀ {k : α} {f : Option (β k) → Option (β k)} {hc : k ∈ t.alter k f}, (t.alter k f).getKey k hc = k
-- Lean.Data.Lsp.Ipc
_private.Lean.Data.Lsp.Ipc.0.Lean.Lsp.Ipc.expandIncomingCallHierarchy.go : ℕ →
  Lean.Lsp.CallHierarchyItem →
    Array Lean.Lsp.Range → Std.TreeSet String compare → Lean.Lsp.Ipc.IpcM (Lean.Lsp.Ipc.CallHierarchy × ℕ)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Cpop
Std.Tactic.BVDecide.BVExpr.bitblast.blastCpopLayer.go_decl_eq : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {len w outWidth : ℕ} (aig : Std.Sat.AIG α) (iterNum : ℕ)
  (oldLayer : aig.RefVec (len * w)) (newLayer : aig.RefVec (iterNum * w)) (hold : 2 * (iterNum - 1) < len)
  (hout : outWidth = (len + 1) / 2 * w) (idx : ℕ)
  (h1 :
    idx < (Std.Tactic.BVDecide.BVExpr.bitblast.blastCpopLayer.go iterNum oldLayer newLayer hold hout).aig.decls.size)
  (h2 : idx < aig.decls.size),
  (Std.Tactic.BVDecide.BVExpr.bitblast.blastCpopLayer.go iterNum oldLayer newLayer hold hout).aig.decls[idx] =
    aig.decls[idx]
-- Mathlib.Order.Hom.Bounded
TopHom.instFunLike : {α : Type u_2} → {β : Type u_3} → [inst : Top α] → [inst_1 : Top β] → FunLike (TopHom α β) α β
-- Std.Data.ExtDTreeMap.Basic
/-- Modifies in place the value associated with a given key.

This function ensures that the value is used linearly.
 -/
Std.ExtDTreeMap.Const.modify : {α : Type u} →
  {cmp : α → α → Ordering} →
    {β : Type v} →
      [Std.TransCmp cmp] → Std.ExtDTreeMap α (fun x => β) cmp → α → (β → β) → Std.ExtDTreeMap α (fun x => β) cmp
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.snd_apply_inr : ∀ {M : Type u_1} {N : Type u_2} [inst : AddMonoid M] [inst_1 : AddMonoid N] (x : N),
  AddMonoid.Coprod.snd (AddMonoid.Coprod.inr x) = x
-- Mathlib.RingTheory.Coalgebra.CoassocSimps
/-- Simproc version of `rid_comp_map` that only fires when `g ≠ id`.  -/
CoassocSimps.rid_comp_map_simproc : Lean.Meta.Simp.Simproc
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- The multicoequalizer of `I : MultispanIndex J C`.  -/
CategoryTheory.Limits.multicoequalizer : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.Limits.MultispanShape} →
      (I : CategoryTheory.Limits.MultispanIndex J C) → [CategoryTheory.Limits.HasMulticoequalizer I] → C
-- Std.Data.TreeMap.Raw.WF
Std.TreeMap.Raw.WF.unitOfList : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List α}, (Std.TreeMap.Raw.unitOfList l cmp).WF
-- Lean.Data.PersistentArray
Lean.PersistentArray.map : {α β : Type u} → (α → β) → Lean.PersistentArray α → Lean.PersistentArray β
-- Mathlib.Algebra.Lie.Matrix
Matrix.lieConj_symm_apply : ∀ {R : Type u} [inst : CommRing R] {n : Type w} [inst_1 : DecidableEq n] [inst_2 : Fintype n] (P A : Matrix n n R)
  (h : Invertible P), (P.lieConj h).symm A = P⁻¹ * A * P
-- Mathlib.Data.Semiquot
Semiquot.instSemilatticeSup : {α : Type u_1} → SemilatticeSup (Semiquot α)
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
UniformContinuous.div_const : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : Group α] [IsUniformGroup α] [inst_3 : UniformSpace β]
  {f : β → α}, UniformContinuous f → ∀ (a : α), UniformContinuous fun x => f x / a
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2to1.trStmts₁.eq_2 : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} (k : K) (f : σ → Option (Γ k) → σ)
  (q : Turing.TM2.Stmt Γ Λ σ),
  Turing.TM2to1.trStmts₁ (Turing.TM2.Stmt.peek k f q) =
    {Turing.TM2to1.Λ'.go k (Turing.TM2to1.StAct.peek f) q, Turing.TM2to1.Λ'.ret q} ∪ Turing.TM2to1.trStmts₁ q
-- Mathlib.Analysis.CStarAlgebra.Matrix
/-- This is the same as `Matrix.l2_opNorm_def`, but with a more bundled RHS for square matrices.  -/
Matrix.cstar_norm_def : ∀ {𝕜 : Type u_1} {n : Type u_3} [inst : RCLike 𝕜] [inst_1 : Fintype n] [inst_2 : DecidableEq n] (A : Matrix n n 𝕜),
  ‖A‖ = ‖Matrix.toEuclideanCLM A‖
-- Mathlib.Order.SymmDiff
bihimp_left_inj : ∀ {α : Type u_2} [inst : BooleanAlgebra α] {a b c : α}, bihimp a b = bihimp c b ↔ a = c
-- Mathlib.GroupTheory.Commutator.Basic
AddSubgroup.addCommutator_center_right : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G), ⁅H, AddSubgroup.center G⁆ = ⊥
-- Mathlib.LinearAlgebra.Projectivization.Collinear
Projectivization.IsCollinear_iff_rank : ∀ {K : Type u_1} {V : Type u_2} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  (S : Set (Projectivization K V)),
  Projectivization.IsCollinear S ↔ ∃ M, Module.rank K ↥(Projectivization.Subspace.submodule M) ≤ 2 ∧ S ⊆ ↑M
-- Mathlib.Analysis.Complex.Isometry
LinearIsometry.re_apply_eq_re : ∀ {f : ℂ →ₗᵢ[ℝ] ℂ}, f 1 = 1 → ∀ (z : ℂ), (f z).re = z.re
-- Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
CategoryTheory.ObjectProperty.instCommShiftFullSubcategoryFunctorTrWInverseImageιTriangulatedLocalizerMorphismInt : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (A B : CategoryTheory.ObjectProperty C) →
      [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
        [inst_2 : CategoryTheory.HasShift C ℤ] →
          [inst_3 : CategoryTheory.Preadditive C] →
            [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
              [inst_5 : CategoryTheory.Pretriangulated C] →
                [inst_6 : A.IsTriangulated] → (A.triangulatedLocalizerMorphism B).functor.CommShift ℤ
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Matrix.nondegenerate_toLinearMap₂'_iff_nondegenerate_toLinearMap₂ : ∀ {R : Type u_1} {M₁ : Type u_6} {M₂ : Type u_7} {n : Type u_11} {m : Type u_12} [inst : CommRing R]
  [inst_1 : DecidableEq m] [inst_2 : Fintype m] [inst_3 : DecidableEq n] [inst_4 : Fintype n] {M : Matrix m n R}
  [inst_5 : AddCommMonoid M₁] [inst_6 : Module R M₁] [inst_7 : AddCommMonoid M₂] [inst_8 : Module R M₂]
  (b₁ : Module.Basis m R M₁) (b₂ : Module.Basis n R M₂),
  ((Matrix.toLinearMap₂' R) M).Nondegenerate ↔ ((Matrix.toLinearMap₂ b₁ b₂) M).Nondegenerate
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
cfcₙAux.congr_simp : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : RCLike 𝕜] [inst_1 : NonUnitalNormedRing A] [inst_2 : StarRing A]
  [inst_3 : NormedSpace 𝕜 A] [inst_4 : IsScalarTower 𝕜 A A] [inst_5 : SMulCommClass 𝕜 A A] [inst_6 : StarModule 𝕜 A]
  {p p_1 : A → Prop} (e_p : p = p_1) {p₁ p₁_1 : Unitization 𝕜 A → Prop} (e_p₁ : p₁ = p₁_1)
  (hp₁ : ∀ {x : A}, p₁ ↑x ↔ p x) (a : A) (ha : p a)
  [inst_7 : ClosedEmbeddingContinuousFunctionalCalculus 𝕜 (Unitization 𝕜 A) p₁], cfcₙAux hp₁ a ha = cfcₙAux ⋯ a ⋯
-- Mathlib.Analysis.Calculus.ContDiff.Defs
/-- In a complete space, a function which is analytic within a set at a point is also `C^ω` there.
Note that the same statement for `AnalyticOn` does not require completeness, see
`AnalyticOn.contDiffOn`.  -/
AnalyticWithinAt.contDiffWithinAt : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {x : E} {n : WithTop ℕ∞} [CompleteSpace F], AnalyticWithinAt 𝕜 f s x → ContDiffWithinAt 𝕜 n f s x
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
/-- The second left fraction.  -/
CategoryTheory.MorphismProperty.LeftFraction₂.snd : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W : CategoryTheory.MorphismProperty C} → {X Y : C} → W.LeftFraction₂ X Y → W.LeftFraction X Y
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.map_iInf : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_4}
  [inst_2 : FunLike F M N] [mc : AddMonoidHomClass F M N] {ι : Sort u_5} [Nonempty ι] (f : F),
  Function.Injective ⇑f → ∀ (s : ι → AddSubmonoid M), AddSubmonoid.map f (iInf s) = ⨅ i, AddSubmonoid.map f (s i)
-- Batteries.Recycling.MonadSatisfying.Basic
/-- The value of the lifted monadic value is equal to the original monadic value.  -/
MonadSatisfying.val_eq : ∀ {m : Type u → Type v} {inst : Functor m} {inst_1 : LawfulFunctor m} [self : MonadSatisfying m] {α : Type u}
  {p : α → Prop} {x : m α} (h : SatisfiesM p x), Subtype.val <$> satisfying h = x
-- Init.Data.SInt.Lemmas
Int32.ofBitVec_add : ∀ (a b : BitVec 32), Int32.ofBitVec (a + b) = Int32.ofBitVec a + Int32.ofBitVec b
-- Mathlib.Algebra.Homology.Homotopy
Homotopy.refl_hom : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D : HomologicalComplex V c} (f : C ⟶ D) (i j : ι), (Homotopy.refl f).hom i j = 0
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
WeierstrassCurve.Jacobian.eval_polynomialX : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} (P : Fin 3 → R),
  (MvPolynomial.eval P) W'.polynomialX = W'.a₁ * P 1 * P 2 - (3 * P 0 ^ 2 + 2 * W'.a₂ * P 0 * P 2 ^ 2 + W'.a₄ * P 2 ^ 4)
-- Mathlib.Dynamics.PeriodicPts.Defs
MulAction.period.eq_1 : ∀ {α : Type v} {M : Type u} [inst : Monoid M] [inst_1 : MulAction M α] (m : M) (a : α),
  MulAction.period m a = Function.minimalPeriod (fun x => m • x) a
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.lid_symm_apply : ∀ (R : Type uR) {A : Type uA} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (a : A),
  (Algebra.TensorProduct.lid R A).symm a = 1 ⊗ₜ[R] a
-- Init.Data.String.Iterate
/-- Creates an iterator over all valid positions within `s` that are strictly smaller than
`p`, starting from the position before `p` and iterating towards the first one.
 -/
String.Slice.revPositionsFrom : (s : String.Slice) → s.Pos → Std.Iter { p // p ≠ s.endPos }
-- Mathlib.LinearAlgebra.Span.Basic
Submodule.iSup_toAddSubmonoid : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Sort u_8}
  (p : ι → Submodule R M), (⨆ i, p i).toAddSubmonoid = ⨆ i, (p i).toAddSubmonoid
-- Mathlib.Order.RelSeries
RelSeries.length_withLength : ∀ {α : Type u_1} (r : SetRel α α) [inst : r.InfiniteDimensional] (n : ℕ), (RelSeries.withLength r n).length = n
-- Mathlib.Computability.RE
computablePred_iff_computable_decide : ∀ {α : Type u_1} [inst : Primcodable α] {p : α → Prop} [inst_1 : DecidablePred p],
  ComputablePred p ↔ Computable fun a => decide (p a)
-- Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
CategoryTheory.Abelian.SpectralObject.coreE₂CohomologicalNat_i₂ : ∀ (pq : ℕ × ℕ), CategoryTheory.Abelian.SpectralObject.coreE₂CohomologicalNat.i₂ pq = WithBotTop.coe (↑pq.2 + 1)
-- Mathlib.Algebra.GroupWithZero.Associated
associated_unit_mul_left : ∀ {N : Type u_2} [inst : CommMonoid N] (a u : N), IsUnit u → Associated (u * a) a
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.size_alter_le_size : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k : α} {f : Option (β k) → Option (β k)}, (t.alter k f).size ≤ t.size + 1
-- Init.Data.Array.Lemmas
Array.pop_empty : ∀ {α : Type u_1}, #[].pop = #[]
-- Mathlib.Combinatorics.Additive.DoublingConst
/-- The difference constant `σ[A, B]` of two finsets `A` and `B` in a group is `|A - B| / |A|`.

The notation `δ[A, B]` is available in scope `Combinatorics.Additive`.  -/
Finset.subConst : {G : Type u_1} → [AddGroup G] → [DecidableEq G] → Finset G → Finset G → ℚ≥0
-- Mathlib.Algebra.Category.MonCat.Limits
AddCommMonCat.forget_createsLimitsOfShape : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] → CategoryTheory.CreatesLimitsOfShape J (CategoryTheory.forget AddMonCat)
-- Lean.Expr
Lean.BinderInfo.implicit.sizeOf_spec : sizeOf Lean.BinderInfo.implicit = 1
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.natIsoSc'_hom_app_τ₁ : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} (c : ComplexShape ι) (i j k : ι) (hi : c.prev j = i) (hk : c.next j = k) (X : HomologicalComplex C c),
  ((HomologicalComplex.natIsoSc' C c i j k hi hk).hom.app X).τ₁ = (X.XIsoOfEq hi).hom
-- Init.Data.String.Basic
/-- Advances a valid position on a string to the next valid position, or returns `none` if the
given position is the past-the-end position.  -/
String.Pos.next? : {s : String} → s.Pos → Option s.Pos
-- Mathlib.Data.Finset.Insert
Finset.ne_insert_of_notMem : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Finset α) {a : α}, a ∉ s → s ≠ insert a t
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.AddGrp.Hom.hom_nsmul : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {G H : CategoryTheory.AddGrp C}
  [inst_3 : CategoryTheory.IsCommAddMonObj H.X] (f : G ⟶ H) (n : ℕ), (n • f).hom = n • f.hom
-- Mathlib.Order.Types.Defs
/-- `Quotient.inductionOn₃` specialized to `OrderType`.  -/
OrderType.inductionOn₃ : ∀ {C : OrderType.{u_1} → OrderType.{u_2} → OrderType.{u_3} → Prop} (o₁ : OrderType.{u_1}) (o₂ : OrderType.{u_2})
  (o₃ : OrderType.{u_3}),
  (∀ (α : Type u_1) [inst : LinearOrder α] (β : Type u_2) [inst_1 : LinearOrder β] (γ : Type u_3)
      [inst_2 : LinearOrder γ], C (OrderType.type α) (OrderType.type β) (OrderType.type γ)) →
    C o₁ o₂ o₃
-- Mathlib.Order.Directed
/-- If `f` is monotone and antitone on a directed set `s`, then `f` is constant on `s`.  -/
constant_of_monotoneOn_antitoneOn : ∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder β] [inst_1 : Preorder α] {f : α → β} {s : Set α},
  MonotoneOn f s →
    AntitoneOn f s → DirectedOn (fun x1 x2 => x1 ≤ x2) s → ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → f a = f b
-- Lean.Message
/-- If the provided name is labeled as a diagnostic name, removes the label and returns the
corresponding diagnostic name.

Note: we use this labeling mechanism so that we can have error kinds that are not intended to be
shown to the user, without having to validate the presence of an error explanation at runtime.
 -/
Lean.errorNameOfKind? : Lean.Name → Option Lean.Name
-- Mathlib.Order.Quotient
Quotient.le_def : ∀ {α : Type u_1} {s : Setoid α} [inst : LE α] {x y : α}, ⟦x⟧ ≤ ⟦y⟧ ↔ Relation.TransGen (fun x y => x ≤ y ∨ x ≈ y) x y
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isBigOWith_abs_abs : ∀ {α : Type u_1} {c : ℝ} {l : Filter α} {u v : α → ℝ},
  (Asymptotics.IsBigOWith c l (fun x => |u x|) fun x => |v x|) ↔ Asymptotics.IsBigOWith c l u v
-- Mathlib.Topology.MetricSpace.IsometricSMul
edist_add_left : ∀ {M : Type u} [inst : Add M] [inst_1 : PseudoEMetricSpace M] [IsIsometricVAdd M M] (a b c : M),
  edist (a + b) (a + c) = edist b c
-- Mathlib.LinearAlgebra.ExteriorPower.Basis
exteriorPower.basis_repr_self : ∀ (R : Type u_1) {M : Type u_3} (n : ℕ) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {I : Type u_5} [inst_3 : LinearOrder I] (b : Module.Basis I R M) (s : ↑(Set.powersetCard I n)),
  ((Module.Basis.exteriorPower n b).repr (exteriorPower.ιMulti_family R n (⇑b) s)) s = 1
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.schwartzSeminormFamily_apply : ∀ (𝕜 : Type u_2) (E : Type u_5) (F : Type u_6) [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedField 𝕜] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : SMulCommClass ℝ 𝕜 F] (n k : ℕ), schwartzSeminormFamily 𝕜 E F (n, k) = SchwartzMap.seminorm 𝕜 n k
-- Mathlib.Topology.TietzeExtension
/-- This theorem is not intended to be used directly because it is rare for a set alone to
satisfy `[TietzeExtension t]`. For example, `Metric.ball` in `ℝ` only satisfies it when
the radius is strictly positive, so finding this as an instance will fail.

Instead, it is intended to be used as a constructor for theorems about sets which *do* satisfy
`[TietzeExtension t]` under some hypotheses.  -/
ContinuousMap.exists_forall_mem_restrict_eq : ∀ {X : Type u} [inst : TopologicalSpace X] [NormalSpace X] {s : Set X},
  IsClosed s →
    ∀ {Y : Type v} [inst_2 : TopologicalSpace Y] (f : C(↑s, Y)) {t : Set Y},
      (∀ (x : ↑s), f x ∈ t) → ∀ [ht : TietzeExtension ↑t], ∃ g, (∀ (x : X), g x ∈ t) ∧ ContinuousMap.restrict s g = f
-- Mathlib.CategoryTheory.Limits.Preorder
/-- If `C` is a preorder with bot, then `⊥` is an initial object.  -/
Preorder.isInitialBot : (C : Type u) → [inst : Preorder C] → [inst_1 : OrderBot C] → CategoryTheory.Limits.IsInitial ⊥
-- Mathlib.Logic.Equiv.Prod
Equiv.prodCongr_refl_right : ∀ {α₁ : Type u_9} {β₁ : Type u_11} {β₂ : Type u_12} (e : β₁ ≃ β₂),
  e.prodCongr (Equiv.refl α₁) = Equiv.prodCongrLeft fun x => e
-- Init.System.IO
/-- The owner's permissions to access the file.  -/
IO.FileRight.user : IO.FileRight → IO.AccessRight
-- Mathlib.Algebra.Homology.ShortComplex.ModuleCat
CategoryTheory.ShortComplex.ShortExact.moduleCat_surjective_g : ∀ {R : Type u} [inst : Ring R] {S : CategoryTheory.ShortComplex (ModuleCat R)},
  S.ShortExact → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom S.g)
-- Lean.Environment
Lean.Kernel.setDiagnostics : Lean.Environment → Lean.Kernel.Diagnostics → Lean.Environment
-- Mathlib.Algebra.Free
/-- The universal property of the free additive magma expressing its adjointness.  -/
FreeAddMagma.lift : {α : Type u} → {β : Type v} → [inst : Add β] → (α → β) ≃ (FreeAddMagma α →ₙ+ β)
-- Mathlib.Tactic.NormNum.ModEq
/-- `norm_num` extension for `Nat.ModEq`.  -/
Mathlib.Meta.NormNum.evalNatModEq : Mathlib.Meta.NormNum.NormNumExt
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.NumDenSameDeg.num_mul : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubmonoidClass σ A] {𝒜 : ι → σ} (x : Submonoid A) [inst_3 : AddCommMonoid ι] [inst_4 : DecidableEq ι]
  [inst_5 : GradedRing 𝒜] (c1 c2 : HomogeneousLocalization.NumDenSameDeg 𝒜 x), ↑(c1 * c2).num = ↑c1.num * ↑c2.num