mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.IsManifold.Basic
ModelWithCorners.range_subset_closure_interior : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] (I : ModelWithCorners 𝕜 E H),
  Set.range ↑I ⊆ closure (interior (Set.range ↑I))
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
/-- The local context, which contains the introduced bound variables.  -/
Lean.Meta.RefinedDiscrTree.ExprInfo.lctx : Lean.Meta.RefinedDiscrTree.ExprInfo → Lean.LocalContext
-- Mathlib.CategoryTheory.Limits.Shapes.Terminal
CategoryTheory.Limits.hasTerminalChangeUniverse : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C]
  [h : CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete PEmpty.{w + 1}) C],
  CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete PEmpty.{w' + 1}) C
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Functions
Lean.Meta.Grind.Arith.CommRing.mkUnaryFn : {m : Type → Type} →
  [MonadLiftT Lean.MetaM m] →
    [Lean.MonadError m] →
      [Monad m] →
        [Lean.Meta.Sym.Arith.MonadCanon m] → Lean.Expr → Lean.Level → Lean.Name → Lean.Name → Lean.Expr → m Lean.Expr
-- Mathlib.Analysis.SpecialFunctions.Complex.CircleMap
eq_of_circleMap_eq : ∀ {a b R : ℝ} {c : ℂ}, R ≠ 0 → |a - b| < 2 * Real.pi → circleMap c R a = circleMap c R b → a = b
-- Lean.Meta.DiscrTree.Types
Lean.Meta.DiscrTree.Key.star.sizeOf_spec : sizeOf Lean.Meta.DiscrTree.Key.star = 1
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.coeff_C_mul_X_pow : ∀ {R : Type u_1} [inst : Semiring R] (x : R) (k n : ℕ),
  (PowerSeries.coeff n) (PowerSeries.C x * PowerSeries.X ^ k) = if n = k then x else 0
-- Mathlib.CategoryTheory.Triangulated.SpectralObject
CategoryTheory.Triangulated.SpectralObject.ω₂_obj_obj₂ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Limits.HasZeroObject C]
  [inst_3 : CategoryTheory.HasShift C ℤ] [inst_4 : CategoryTheory.Preadditive C]
  [inst_5 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_6 : CategoryTheory.Pretriangulated C]
  (X : CategoryTheory.Triangulated.SpectralObject C ι) (j : CategoryTheory.ComposableArrows ι 2),
  (X.ω₂.obj j).obj₂ = X.ω₁.obj (CategoryTheory.ComposableArrows.mk₁ (j.map (CategoryTheory.homOfLE ⋯)))
-- Mathlib.Algebra.Order.Module.Defs
Prod.instSMulPosMono : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  [inst_3 : SMul α β] [inst_4 : SMul α γ] [inst_5 : Zero β] [inst_6 : Zero γ] [SMulPosMono α β] [SMulPosMono α γ],
  SMulPosMono α (β × γ)
-- Mathlib.Probability.Kernel.CondDistrib
ProbabilityTheory.condDistrib_comp_map : ∀ {α : Type u_1} {β : Type u_2} {Ω : Type u_3} [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω]
  [inst_2 : Nonempty Ω] {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_3 : MeasureTheory.IsFiniteMeasure μ] {X : α → β} {Y : α → Ω} {mβ : MeasurableSpace β},
  AEMeasurable X μ →
    AEMeasurable Y μ →
      (MeasureTheory.Measure.map X μ).bind ⇑(ProbabilityTheory.condDistrib Y X μ) = MeasureTheory.Measure.map Y μ
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.stepNormal.is_ret : ∀ (c : Turing.ToPartrec.Code) (k : Turing.ToPartrec.Cont) (v : List ℕ),
  ∃ k' v', Turing.ToPartrec.stepNormal c k v = Turing.ToPartrec.Cfg.ret k' v'
-- Mathlib.Topology.PartialHomeomorph.Defs
PartialHomeomorph.bijOn : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : PartialHomeomorph X Y),
  Set.BijOn (↑e) e.source e.target
-- Mathlib.SetTheory.ZFC.VonNeumann
ZFSet.vonNeumann_mem_vonNeumann_iff : ∀ {a b : Ordinal.{u}}, ZFSet.vonNeumann a ∈ ZFSet.vonNeumann b ↔ a < b
-- Mathlib.Algebra.BigOperators.Pi
/-- This is used as the ext lemma instead of `MonoidHom.functions_ext` for reasons explained in
note [partially-applied ext lemmas].  -/
MonoidHom.functions_ext' : ∀ {I : Type u_7} [inst : DecidableEq I] {M : I → Type u_8} [inst_1 : (i : I) → CommMonoid (M i)] [Finite I]
  (N : Type u_9) [inst_3 : CommMonoid N] (g h : ((i : I) → M i) →* N),
  (∀ (i : I), g.comp (MonoidHom.mulSingle M i) = h.comp (MonoidHom.mulSingle M i)) → g = h
-- Lean.Parser.Basic
/-- The list of syntax nodes that can parse into this category.
This can be used to list all syntaxes in the category.  -/
Lean.Parser.ParserCategory.kinds : Lean.Parser.ParserCategory → Lean.Parser.SyntaxNodeKindSet
-- Mathlib.CategoryTheory.Functor.CurryingThree
CategoryTheory.Functor.flip₂₃_map_app_app : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {E : Type u_9} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_4} C₃]
  [inst_3 : CategoryTheory.Category.{v_9, u_9} E]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ E))) {X Y : C₁} (f : X ⟶ Y)
  (Y_1 : C₃) (X_1 : C₂), ((F.flip₂₃.map f).app Y_1).app X_1 = ((F.map f).app X_1).app Y_1
-- Mathlib.AlgebraicGeometry.ColimitsOver
AlgebraicGeometry.Scheme.Cover.ColimitGluingData.mk.sizeOf_spec : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [inst : P.IsStableUnderBaseChange]
  {S : AlgebraicGeometry.Scheme} {J : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} J]
  {D : CategoryTheory.Functor J (P.Over ⊤ S)} {𝒰 : S.OpenCover} [inst_2 : CategoryTheory.Category.{v_3, u_2} 𝒰.I₀]
  [inst_3 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰]
  [inst_4 : ⦃X Y : AlgebraicGeometry.Scheme⦄ → (x : X ⟶ Y) → SizeOf (P x)] [inst_5 : SizeOf J]
  (cocone :
    (i : 𝒰.I₀) → CategoryTheory.Limits.Cocone (D.comp (CategoryTheory.MorphismProperty.Over.pullback P ⊤ (𝒰.f i))))
  (isColimit : (i : 𝒰.I₀) → CategoryTheory.Limits.IsColimit (cocone i))
  (prop_trans : ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), P (AlgebraicGeometry.Scheme.Cover.trans 𝒰 hij)),
  sizeOf { cocone := cocone, isColimit := isColimit, prop_trans := prop_trans } = 1
-- Mathlib.Algebra.Lie.Nilpotent
LieModule.eventually_iInf_lowerCentralSeries_eq : ∀ (R : Type u) (L : Type v) (M : Type w) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [IsArtinian R M],
  ∀ᶠ (l : ℕ) in Filter.atTop, ⨅ k, LieModule.lowerCentralSeries R L M k = LieModule.lowerCentralSeries R L M l
-- Init.System.IO
/-- Replaces the standard output stream of the current thread and returns its previous value.

Use `IO.getStdout` to get the current standard output stream.
 -/
IO.setStdout : IO.FS.Stream → BaseIO IO.FS.Stream
-- Mathlib.Topology.Order.LocalExtr
IsLocalMinOn.isLocalMin : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder β] {f : α → β} {s : Set α} {a : α},
  IsLocalMinOn f s a → s ∈ nhds a → IsLocalMin f a
-- Mathlib.Algebra.Homology.DerivedCategory.HomologySequence
DerivedCategory.HomologySequence.comp_δ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C],
  ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles,
    ∀ (n₀ n₁ : ℤ) (h : autoParam (n₀ + 1 = n₁) DerivedCategory.HomologySequence.comp_δ._auto_1),
      CategoryTheory.CategoryStruct.comp ((DerivedCategory.homologyFunctor C n₀).map T.mor₂)
          (DerivedCategory.HomologySequence.δ T n₀ n₁ h) =
        0
-- Init.Grind.Ordered.Module
Lean.Grind.OrderedAdd.neg_pos_iff : ∀ {M : Type u} [inst : LE M] [inst_1 : Std.IsPreorder M] [inst_2 : Lean.Grind.AddCommGroup M] [Lean.Grind.OrderedAdd M]
  [inst_4 : LT M] [Std.LawfulOrderLT M] {a : M}, 0 < -a ↔ a < 0
-- Mathlib.Data.Finset.Option
/-- Construct an empty or singleton finset from an `Option`  -/
Option.toFinset : {α : Type u_1} → Option α → Finset α
-- Mathlib.RingTheory.PolynomialLaw.Basic
PolynomialLaw.exists_range_φ_eq_of_fg : ∀ {R : Type u} [inst : CommSemiring R] {S : Type v} [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  {B : Subalgebra R S}, B.FG → ∃ s, (PolynomialLaw.φ R s).range = B
-- Mathlib.Algebra.Module.Presentation.Cokernel
Module.Presentation.CokernelData.mk.inj : ∀ {A : Type u} {inst : Ring A} {M₁ : Type v₁} {M₂ : Type v₂} {inst_1 : AddCommGroup M₁} {inst_2 : Module A M₁}
  {inst_3 : AddCommGroup M₂} {inst_4 : Module A M₂} {pres₂ : Module.Presentation A M₂} {f : M₁ →ₗ[A] M₂} {ι : Type w₁}
  {g₁ : ι → M₁} {lift : ι → pres₂.G →₀ A} {π_lift : ∀ (i : ι), pres₂.π (lift i) = f (g₁ i)} {lift_1 : ι → pres₂.G →₀ A}
  {π_lift_1 : ∀ (i : ι), pres₂.π (lift_1 i) = f (g₁ i)},
  { lift := lift, π_lift := π_lift } = { lift := lift_1, π_lift := π_lift_1 } → lift = lift_1
-- Mathlib.RingTheory.WittVector.Teichmuller
WittVector.teichmuller_zero : ∀ (p : ℕ) {R : Type u_1} [hp : Fact (Nat.Prime p)] [inst : CommRing R], (WittVector.teichmuller p) 0 = 0
-- Mathlib.Topology.Order
WithTopology.topology_eq_induced : ∀ {X : Type u_4} (t : TopologicalSpace X),
  WithTopology.instTopologicalSpace X t = TopologicalSpace.induced WithTopology.ofTopology t
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.Red.refl : ∀ {α : Type u} {L : List (α × Bool)}, FreeAddGroup.Red L L
-- Mathlib.Topology.Hom.ContinuousEvalConst
continuous_coeFun : ∀ {F : Type u_1} {α : Type u_2} {X : Type u_3} [inst : FunLike F α X] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace X] [ContinuousEvalConst F α X], Continuous DFunLike.coe
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.minEntry?.match_1.congr_eq_2 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → Sort u_3)
  (x : Std.DTreeMap.Internal.Impl α β) (h_1 : Unit → motive Std.DTreeMap.Internal.Impl.leaf)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (r : Std.DTreeMap.Internal.Impl α β) →
            motive (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r))
  (h_3 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l : Std.DTreeMap.Internal.Impl α β) →
            (size_1 : ℕ) →
              (k_1 : α) →
                (v_1 : β k_1) →
                  (l_1 r : Std.DTreeMap.Internal.Impl α β) →
                    l = Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r →
                      (r_1 : Std.DTreeMap.Internal.Impl α β) →
                        motive
                          (Std.DTreeMap.Internal.Impl.inner size k v
                            (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r) r_1))
  (size : ℕ) (k : α) (v : β k) (r : Std.DTreeMap.Internal.Impl α β),
  x = Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r →
    (match x with
      | Std.DTreeMap.Internal.Impl.leaf => h_1 ()
      | Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r => h_2 size k v r
      | Std.DTreeMap.Internal.Impl.inner size k v (l@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r)) r_1 =>
        h_3 size k v l size_1 k_1 v_1 l_1 r h r_1) ≍
      h_2 size k v r
-- Mathlib.CategoryTheory.Limits.Shapes.Images
/-- `HasImages` asserts that every morphism has an image.  -/
CategoryTheory.Limits.HasImages.has_image : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.Limits.HasImages C] {X Y : C}
  (f : X ⟶ Y), CategoryTheory.Limits.HasImage f
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.Y_sub_Y_add_Y_sub_negY : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} {P Q : Fin 3 → R},
  P 0 * Q 2 = Q 0 * P 2 → P 1 * Q 2 - Q 1 * P 2 + (P 1 * Q 2 - W'.negY Q * P 2) = (P 1 - W'.negY P) * Q 2
-- Mathlib.Topology.Sheaves.CommRingCat
TopCat.instSubHomObjTopCommRingCatForget₂SubtypeRingHomαContinuousCoeContinuousMapCarrier : (X : TopCat) → (R : TopCommRingCat) → Sub (X ⟶ (CategoryTheory.forget₂ TopCommRingCat TopCat).obj R)
-- Mathlib.RingTheory.PowerSeries.Basic
Polynomial.coe_mul : ∀ {R : Type u_1} [inst : Semiring R] (φ ψ : Polynomial R), ↑(φ * ψ) = ↑φ * ↑ψ
-- Init.Data.SInt.Lemmas
ISize.ofNat_add : ∀ (a b : ℕ), ISize.ofNat (a + b) = ISize.ofNat a + ISize.ofNat b
-- Mathlib.Algebra.Group.NatPowAssoc
/-- Multiplication is power-associative.  -/
NatPowAssoc.npow_add : ∀ {M : Type u_2} {inst : MulOneClass M} {inst_1 : Pow M ℕ} [self : NatPowAssoc M] (k n : ℕ) (x : M),
  x ^ (k + n) = x ^ k * x ^ n
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instLawfulUpwardEnumerableLeast? : Std.PRange.LawfulUpwardEnumerableLeast? Int64
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
/-- The function `Real.cos` is real analytic.  -/
Real.analyticWithinAt_cos : ∀ {x : ℝ} {s : Set ℝ}, AnalyticWithinAt ℝ Real.cos s x
-- Lean.PrettyPrinter.Delaborator.Basic
Lean.PrettyPrinter.Delaborator.instOrElseDelabM : {α : Type} → OrElse (Lean.PrettyPrinter.Delaborator.DelabM α)
-- Mathlib.CategoryTheory.Limits.Shapes.End
CategoryTheory.Limits.multispanIndexCoend_left : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  (F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)) (f : (CategoryTheory.Limits.multispanShapeCoend J).L),
  (CategoryTheory.Limits.multispanIndexCoend F).left f =
    (F.obj (Opposite.op (CategoryTheory.Arrow.right f))).obj (CategoryTheory.Arrow.left f)
-- Init.Data.Array.Lemmas
Array.toList_filterMap : ∀ {α : Type u_1} {β : Type u_2} {f : α → Option β} {xs : Array α},
  (Array.filterMap f xs).toList = List.filterMap f xs.toList
-- Mathlib.Combinatorics.Matroid.Circuit
Matroid.exists_isCircuit_of_mem_closure : ∀ {α : Type u_1} {M : Matroid α} {X : Set α} {e : α}, e ∈ M.closure X → e ∉ X → ∃ C ⊆ insert e X, M.IsCircuit C ∧ e ∈ C
-- Mathlib.Combinatorics.SimpleGraph.Clique
/-- **Alias** of `SimpleGraph.IsContained.not_cliqueFree_card`. -/
SimpleGraph.not_cliqueFree_card_of_top_embedding : ∀ {α : Type u_1} {G : SimpleGraph α} [inst : Fintype α],
  (SimpleGraph.completeGraph α).IsContained G → ¬G.CliqueFree (Fintype.card α)
-- Mathlib.Topology.Algebra.Module.FiniteDimension
LinearEquiv.coe_toContinuousLinearEquiv' : ∀ {𝕜 : Type u} [hnorm : NontriviallyNormedField 𝕜] {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E]
  [inst_2 : TopologicalSpace E] [inst_3 : IsTopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E] {F : Type w}
  [inst_5 : AddCommGroup F] [inst_6 : Module 𝕜 F] [inst_7 : TopologicalSpace F] [inst_8 : IsTopologicalAddGroup F]
  [inst_9 : ContinuousSMul 𝕜 F] [inst_10 : CompleteSpace 𝕜] [inst_11 : T2Space E] [inst_12 : T2Space F]
  [inst_13 : FiniteDimensional 𝕜 E] (e : E ≃ₗ[𝕜] F), ⇑e.toContinuousLinearEquiv = ⇑e
-- Mathlib.Analysis.Calculus.ContDiff.Defs
ContDiffWithinAt.analyticWithinAt : ∀ {𝕜 : 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}, ContDiffWithinAt 𝕜 ⊤ f s x → AnalyticWithinAt 𝕜 f s x
-- Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
/-- A family of sections `s i` of `V → M` is called a **C^k local frame** on a set `U ⊆ M` iff
- the section values `s i x` form a basis for each `x ∈ U`,
- each section `s i` is `C^k` on `U`.
 -/
IsLocalFrameOn : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {H : Type u_3} →
            [inst_3 : TopologicalSpace H] →
              ModelWithCorners 𝕜 E H →
                {M : Type u_4} →
                  [inst_4 : TopologicalSpace M] →
                    [ChartedSpace H M] →
                      (F : Type u_5) →
                        [inst_6 : NormedAddCommGroup F] →
                          [NormedSpace 𝕜 F] →
                            {V : M → Type u_6} →
                              [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)] →
                                [inst_9 : (x : M) → AddCommGroup (V x)] →
                                  [(x : M) → Module 𝕜 (V x)] →
                                    [inst : (x : M) → TopologicalSpace (V x)] →
                                      [FiberBundle F V] →
                                        {ι : Type u_7} → WithTop ℕ∞ → (ι → (x : M) → V x) → Set M → Prop
-- Mathlib.Data.Finset.Max
Finset.min'_eq_iff : ∀ {α : Type u_2} [inst : LinearOrder α] (s : Finset α) (H : s.Nonempty) (a : α), s.min' H = a ↔ a ∈ s ∧ ∀ b ∈ s, a ≤ b
-- Mathlib.RingTheory.IntegralClosure.IntegralRestrict
galRestrictHom_apply : ∀ (A : Type u_1) (K : Type u_2) (L : Type u_3) (B : Type u_6) [inst : CommRing A] [inst_1 : CommRing B]
  [inst_2 : Algebra A B] [inst_3 : Field K] [inst_4 : Field L] [inst_5 : Algebra A K] [inst_6 : IsFractionRing A K]
  [inst_7 : Algebra K L] [inst_8 : Algebra A L] [inst_9 : IsScalarTower A K L] [inst_10 : Algebra B L]
  [inst_11 : IsScalarTower A B L] [inst_12 : IsIntegralClosure B A L] [inst_13 : Algebra.IsAlgebraic K L]
  (f : L →ₐ[K] L), (galRestrictHom A K L B) f = galRestrict' A B B f
-- Std.Data.DTreeMap.Raw.Basic
/-- Modifies in place the value associated with a given key,
allowing creating new values and deleting values via an `Option` valued replacement function.

This function ensures that the value is used linearly.
 -/
Std.DTreeMap.Raw.Const.alter : {α : Type u} →
  {cmp : α → α → Ordering} →
    {β : Type v} → Std.DTreeMap.Raw α (fun x => β) cmp → α → (Option β → Option β) → Std.DTreeMap.Raw α (fun x => β) cmp
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- If the angle between three points is `-π / 2`, the last two points are not equal.  -/
EuclideanGeometry.right_ne_of_oangle_eq_neg_pi_div_two : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ : P}, EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(-Real.pi / 2) → p₃ ≠ p₂
-- Init.Data.Int.DivMod.Lemmas
Int.bmod_mul_bmod : ∀ {x : ℤ} {n : ℕ} {y : ℤ}, (x.bmod n * y).bmod n = (x * y).bmod n
-- Mathlib.RingTheory.AdicCompletion.Algebra
AdicCompletion.val_mul : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) (n : ℕ) (x y : AdicCompletion I R), ↑(x * y) n = ↑x n * ↑y n
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMonObj.instIsAddMonHomHomAssociator : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {X Y Z : C} [inst_3 : CategoryTheory.AddMonObj X]
  [inst_4 : CategoryTheory.AddMonObj Y] [inst_5 : CategoryTheory.AddMonObj Z],
  CategoryTheory.IsAddMonHom (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.IsAffineOpen.fromSpec_image_zeroLocus : ∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U)
  (s : Set ↑(X.presheaf.obj (Opposite.op U))), ⇑hU.fromSpec '' PrimeSpectrum.zeroLocus s = X.zeroLocus s ∩ ↑U
-- Mathlib.CategoryTheory.MorphismProperty.Representable
CategoryTheory.Functor.relativelyRepresentable.pullback₃.snd_snd_eq_p₃ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} [inst_2 : F.Full] {A₁ A₂ A₃ : C} {X : D} {f₁ : F.obj A₁ ⟶ X}
  (hf₁ : F.relativelyRepresentable f₁) (f₂ : F.obj A₂ ⟶ X) (f₃ : F.obj A₃ ⟶ X)
  [inst_3 : CategoryTheory.Limits.HasPullback (hf₁.fst' f₂) (hf₁.fst' f₃)],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (hf₁.fst' f₂) (hf₁.fst' f₃)) (hf₁.snd f₃) =
    CategoryTheory.Functor.relativelyRepresentable.pullback₃.p₃ hf₁ f₂ f₃
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.mulConst_k_eq_mulConst : ∀ (k : ℤ) (p : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Poly.mulConst_k k p = Lean.Grind.CommRing.Poly.mulConst k p
-- Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Asymptotics.IsEquivalent.trans_eventuallyEq : ∀ {α : Type u_1} {β : Type u_2} [inst : NormedAddCommGroup β] {l : Filter α} {f g₁ g₂ : α → β},
  Asymptotics.IsEquivalent l f g₁ → g₁ =ᶠ[l] g₂ → Asymptotics.IsEquivalent l f g₂
-- Mathlib.Order.Category.BddDistLat
BddDistLat.coe_toBddLat : ∀ (X : BddDistLat), ↑X.toBddLat.toLat = ↑X.toDistLat
-- Mathlib.Probability.Kernel.Defs
ProbabilityTheory.Kernel.apply_congr_of_mem_measurableAtom : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ProbabilityTheory.Kernel α β)
  {y' y : α}, y' ∈ measurableAtom y → κ y' = κ y
-- Mathlib.LinearAlgebra.Dimension.RankNullity
nontrivial_of_hasRankNullity : ∀ (R : Type u_1) [inst : Ring R] [HasRankNullity.{u, u_1} R], Nontrivial R
-- Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
_private.Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr.0.Lean.Grind.CommRing.Poly.denoteExpr.go : {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.Grind.CommRing.Poly → Lean.Expr → M Lean.Expr
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.tensor_isIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {W X Y Z : C}
  (f : W ⟶ X) [CategoryTheory.IsIso f] (g : Y ⟶ Z) [CategoryTheory.IsIso g],
  CategoryTheory.IsIso (CategoryTheory.MonoidalCategoryStruct.tensorHom f g)
-- Mathlib.Algebra.Group.Prod
MonoidHom.fst_comp_inl : ∀ {M : Type u_3} {N : Type u_4} [inst : MulOneClass M] [inst_1 : MulOneClass N],
  (MonoidHom.fst M N).comp (MonoidHom.inl M N) = MonoidHom.id M
-- Mathlib.AlgebraicGeometry.Cover.MorphismProperty
/-- A morphism between covers `𝒰 ⟶ 𝒱` indicates that `𝒰` is a refinement of `𝒱`.
Since covers of schemes are indexed, the definition also involves a map on the
indexing types.
This is implemented as an `abbrev` for `CategoryTheory.Precoverage.ZeroHypercover.Hom`.
 -/
AlgebraicGeometry.Scheme.Cover.Hom : {K : CategoryTheory.Precoverage AlgebraicGeometry.Scheme} →
  {X : AlgebraicGeometry.Scheme} →
    AlgebraicGeometry.Scheme.Cover K X → AlgebraicGeometry.Scheme.Cover K X → Type (max u v)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey!_modify : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited α] {k k' : α} {f : β → β},
  (m.modify k f).getKey! k' = if (k == k') = true then if k ∈ m then k else default else m.getKey! k'
-- Init.Data.Vector.Lemmas
Vector.findFinIdx?_mk : ∀ {α : Type u_1} {n : ℕ} {xs : Array α} (h : xs.size = n) (f : α → Bool),
  Vector.findFinIdx? f (Vector.mk xs h) = Option.map (Fin.cast h) (Array.findFinIdx? f xs)
-- Lean.Message
Lean.instInhabitedTraceResult.default : Lean.TraceResult
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- `post (F ⋙ G)` is isomorphic (actually equal) to `post F ⋙ post G`.  -/
CategoryTheory.Over.postComp : {T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {X : T} →
          {E : Type u_1} →
            [inst_2 : CategoryTheory.Category.{v_1, u_1} E] →
              (F : CategoryTheory.Functor T D) →
                (G : CategoryTheory.Functor D E) →
                  CategoryTheory.Over.post (F.comp G) ≅ (CategoryTheory.Over.post F).comp (CategoryTheory.Over.post G)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.containsThenInsertIfNew!_snd : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF →
    ∀ {k : α} {v : β k},
      (Std.DTreeMap.Internal.Impl.containsThenInsertIfNew! k v t).2 = Std.DTreeMap.Internal.Impl.insertIfNew! k v t
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.instIteratorZipperIdSigma : {α : Type u} → {β : α → Type v} → Std.Iterator (Std.DTreeMap.Internal.Zipper α β) Id ((a : α) × β a)
-- Mathlib.RingTheory.Ideal.Quotient.Defs
Ideal.Quotient.mk_surjective : ∀ {R : Type u} [inst : Ring R] {I : Ideal R} [inst_1 : I.IsTwoSided], Function.Surjective ⇑(Ideal.Quotient.mk I)