mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Lie.Abelian
lie_eq_self_of_isAtom_of_nonabelian : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (I : LieIdeal R L),
  IsAtom I → ¬IsLieAbelian ↥I → ⁅I, I⁆ = I
-- Mathlib.NumberTheory.ArithmeticFunction.Misc
Nat.card_divisors : ∀ {n : ℕ}, n ≠ 0 → n.divisors.card = ∏ x ∈ n.primeFactors, (n.factorization x + 1)
-- Mathlib.RingTheory.Multiplicity
FiniteMultiplicity.exists_eq_pow_mul_and_not_dvd : ∀ {α : Type u_1} [inst : Monoid α] {a b : α}, FiniteMultiplicity a b → ∃ c, b = a ^ multiplicity a b * c ∧ ¬a ∣ c
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.instAddGroup : {α : Type u_1} → {β : Type u_2} → [inst : MeasurableSpace α] → [AddGroup β] → AddGroup (MeasureTheory.SimpleFunc α β)
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Formula.realize_sup : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {φ ψ : L.Formula α} {v : α → M},
  (φ ⊔ ψ).Realize v ↔ φ.Realize v ∨ ψ.Realize v
-- Mathlib.Data.NNReal.Defs
NNReal.coe_sub : ∀ {r₁ r₂ : NNReal}, r₂ ≤ r₁ → ↑(r₁ - r₂) = ↑r₁ - ↑r₂
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.DeclValue.code.sizeOf_spec : ∀ {pu : Lean.Compiler.LCNF.Purity} (code : Lean.Compiler.LCNF.Code pu),
  sizeOf (Lean.Compiler.LCNF.DeclValue.code code) = 1 + sizeOf code
-- Lean.Parser.Term.Basic
Lean.Parser.Term.structInstArrayRef : Lean.Parser.Parser
-- Mathlib.Topology.Bases
TopologicalSpace.isSeparable_closure : ∀ {α : Type u} [t : TopologicalSpace α] {s : Set α},
  TopologicalSpace.IsSeparable (closure s) ↔ TopologicalSpace.IsSeparable s
-- Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
seminormFromConst_seq.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] (c : R) (f : RingSeminorm R) (x : R) (n : ℕ),
  seminormFromConst_seq c f x n = f (x * c ^ n) / f c ^ n
-- Aesop.Util.UnorderedArraySet
/-- O(n)  -/
Aesop.UnorderedArraySet.contains : {α : Type u_1} → [inst : BEq α] → α → Aesop.UnorderedArraySet α → Bool
-- Mathlib.RingTheory.MvPowerSeries.Substitution
/-- Rewrite `MvPowerSeries.substAlgHom` as `MvPowerSeries.aeval`.

Its use is discouraged because it introduces a topology and might lead
into awkward comparisons.  -/
MvPowerSeries.substAlgHom_eq_aeval : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] {τ : Type u_4} {S : Type u_5} [inst_1 : CommRing S]
  [inst_2 : Algebra R S] {a : σ → MvPowerSeries τ S} [inst_3 : UniformSpace R] [inst_4 : DiscreteUniformity R]
  [inst_5 : UniformSpace S] [inst_6 : DiscreteUniformity S] (ha : MvPowerSeries.HasSubst a),
  ⇑(MvPowerSeries.substAlgHom ha) = ⇑(MvPowerSeries.aeval ⋯)
-- Mathlib.Tactic.Peel
/-- Similar to `peelArgs` but peels arbitrarily many quantifiers. Returns whether or not
any quantifiers were peeled.  -/
Mathlib.Tactic.Peel.peelUnbounded : Lean.Expr → Option Lean.Name → optParam Bool false → Lean.Elab.Tactic.TacticM Bool
-- Mathlib.Algebra.GroupWithZero.Range
MonoidWithZeroHom.ValueGroup₀.embedding_apply : ∀ {A : Type u_1} {B : Type u_2} [inst : MonoidWithZero A] [inst_1 : GroupWithZero B] {f : A →*₀ B} (a : f.ValueGroup₀),
  MonoidWithZeroHom.ValueGroup₀.embedding a = WithZero.recZeroCoe 0 Units.val ((WithZero.map' f.valueGroup.subtype) a)
-- Mathlib.Algebra.Symmetrized
SymAlg.sym_injective : ∀ {α : Type u_1}, Function.Injective ⇑SymAlg.sym
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Dense.borel_eq_generateFrom_Ioc_mem : ∀ {α : Type u_5} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [SecondCountableTopology α]
  [DenselyOrdered α] [NoMaxOrder α] {s : Set α},
  Dense s → borel α = MeasurableSpace.generateFrom {S | ∃ l ∈ s, ∃ u ∈ s, l < u ∧ Set.Ioc l u = S}
-- Mathlib.Algebra.Order.Ring.Archimedean
ArchimedeanClass.instIsOrderedAddMonoid : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : CommRing R] [inst_2 : IsStrictOrderedRing R],
  IsOrderedAddMonoid (ArchimedeanClass R)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.maxKey!_erase_le_maxKey! : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {k : α}, t.erase k ≠ ∅ → (cmp (t.erase k).maxKey! t.maxKey!).isLE = true
-- Mathlib.Analysis.Seminorm
Seminorm.coe_lt_coe : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddGroup E] [inst_2 : SMul 𝕜 E]
  {p q : Seminorm 𝕜 E}, ⇑p < ⇑q ↔ p < q
-- Batteries.Util.ProofWanted
/-- Walk a syntax tree, throwing on the first `wantedRef` node found.  -/
_private.Batteries.Util.ProofWanted.0.rejectRefsIn : String → String → Lean.Syntax → Lean.Elab.Command.CommandElabM Unit
-- Mathlib.Tactic.MkIffOfInductiveProp
/-- Auxiliary data associated with a single constructor of an inductive declaration.
 -/
Mathlib.Tactic.MkIff.Shape : Type
-- Mathlib.Algebra.GroupWithZero.Defs
zero_eq_mul_self : ∀ {M₀ : Type u_1} [inst : MulZeroClass M₀] [NoZeroDivisors M₀] {a : M₀}, 0 = a * a ↔ a = 0
-- Std.Http.Data.URI.Basic
/-- Sets the host as an IPv4 address.
 -/
Std.Http.URI.Builder.setHostIPv4 : Std.Http.URI.Builder → Std.Net.IPv4Addr → Std.Http.URI.Builder
-- Lean.DocString.Types
/-- The math content is part of the text flow.  -/
Lean.Doc.MathMode.inline : Lean.Doc.MathMode
-- Mathlib.Algebra.Free
FreeAddMagma.recOnAdd.eq_1 : ∀ {α : Type u} {C : FreeAddMagma α → Sort l} (x : FreeAddMagma α) (ih1 : (x : α) → C (FreeAddMagma.of x))
  (ih2 : (x y : FreeAddMagma α) → C x → C y → C (x + y)), x.recOnAdd ih1 ih2 = FreeAddMagma.recOn x ih1 ih2
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.arrowEquiv_apply : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (F : CategoryTheory.ComposableArrows C 1),
  CategoryTheory.ComposableArrows.arrowEquiv F = CategoryTheory.Arrow.mk F.hom
-- Mathlib.Order.Cover
CovBy.lt : ∀ {α : Type u_1} [inst : LT α] {a b : α}, a ⋖ b → a < b
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instSMul : {α : Type u_1} → {l : Filter α} → {M : Type u_5} → {G : Type u_6} → [SMul M G] → SMul M (l.Germ G)
-- Init.Grind.Lemmas
Lean.Grind.of_decide_eq_false : ∀ {p : Prop} {x : Decidable p}, decide p = false → p = False
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.AddAndFinalizeContext.mk.injEq : ∀ (views : Array Lean.Elab.Command.InductiveView) (elabs' : Array Lean.Elab.Command.InductiveElabStep2)
  (indFVars vars : Array Lean.Expr) (levelParams : List Lean.Name) (numVars numParams : ℕ)
  (indTypes : List Lean.InductiveType) (isUnsafe : Bool) (rs : Array Lean.Elab.Command.ElabHeaderResult)
  (params : Array Lean.Expr) (isCoinductive : Bool) (views_1 : Array Lean.Elab.Command.InductiveView)
  (elabs'_1 : Array Lean.Elab.Command.InductiveElabStep2) (indFVars_1 vars_1 : Array Lean.Expr)
  (levelParams_1 : List Lean.Name) (numVars_1 numParams_1 : ℕ) (indTypes_1 : List Lean.InductiveType)
  (isUnsafe_1 : Bool) (rs_1 : Array Lean.Elab.Command.ElabHeaderResult) (params_1 : Array Lean.Expr)
  (isCoinductive_1 : Bool),
  ({ views := views, elabs' := elabs', indFVars := indFVars, vars := vars, levelParams := levelParams,
        numVars := numVars, numParams := numParams, indTypes := indTypes, isUnsafe := isUnsafe, rs := rs,
        params := params, isCoinductive := isCoinductive } =
      { views := views_1, elabs' := elabs'_1, indFVars := indFVars_1, vars := vars_1, levelParams := levelParams_1,
        numVars := numVars_1, numParams := numParams_1, indTypes := indTypes_1, isUnsafe := isUnsafe_1, rs := rs_1,
        params := params_1, isCoinductive := isCoinductive_1 }) =
    (views = views_1 ∧
      elabs' = elabs'_1 ∧
        indFVars = indFVars_1 ∧
          vars = vars_1 ∧
            levelParams = levelParams_1 ∧
              numVars = numVars_1 ∧
                numParams = numParams_1 ∧
                  indTypes = indTypes_1 ∧
                    isUnsafe = isUnsafe_1 ∧ rs = rs_1 ∧ params = params_1 ∧ isCoinductive = isCoinductive_1)
-- Mathlib.Algebra.Lie.Sl2
IsSl2Triple.e_ne_zero : ∀ {L : Type u_2} [inst : LieRing L] {h e f : L}, IsSl2Triple h e f → e ≠ 0
-- Mathlib.CategoryTheory.Sites.Point.Monoidal
CategoryTheory.GrothendieckTopology.Point.instIsMonoidalFunctorOppositeHomPresheafToSheafCompSheafFiberIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point)
  {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A] [inst_2 : CategoryTheory.MonoidalCategory A]
  [inst_3 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] [inst_4 : CategoryTheory.LocallySmall.{w, v, u} C]
  [inst_5 :
    ∀ (X : A),
      CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'}
        (CategoryTheory.MonoidalCategory.tensorLeft X)]
  [inst_6 :
    ∀ (X : A),
      CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'}
        (CategoryTheory.MonoidalCategory.tensorRight X)]
  [inst_7 : J.W.IsMonoidal] [inst_8 : CategoryTheory.HasWeakSheafify J A]
  [inst_9 : CategoryTheory.Limits.HasProducts A],
  CategoryTheory.NatTrans.IsMonoidal (Φ.presheafToSheafCompSheafFiberIso A).hom
-- Mathlib.Algebra.Group.Equiv.Basic
AddEquiv.addMonoidHomCongrLeftEquiv.eq_1 : ∀ {M₁ : Type u_5} {M₂ : Type u_6} {N : Type u_8} [inst : AddZeroClass M₁] [inst_1 : AddZeroClass M₂]
  [inst_2 : AddMonoid N] (e : M₁ ≃+ M₂),
  e.addMonoidHomCongrLeftEquiv =
    { toFun := fun f => f.comp e.symm.toAddMonoidHom, invFun := fun f => f.comp e.toAddMonoidHom, left_inv := ⋯,
      right_inv := ⋯ }
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.Code.reassign.injEq : ∀ (xs : Array Lean.Elab.Term.Do.Var) (doElem : Lean.Syntax) (k : Lean.Elab.Term.Do.Code)
  (xs_1 : Array Lean.Elab.Term.Do.Var) (doElem_1 : Lean.Syntax) (k_1 : Lean.Elab.Term.Do.Code),
  (Lean.Elab.Term.Do.Code.reassign xs doElem k = Lean.Elab.Term.Do.Code.reassign xs_1 doElem_1 k_1) =
    (xs = xs_1 ∧ doElem = doElem_1 ∧ k = k_1)
-- Mathlib.Control.Traversable.Basic
/-- A traversable functor is lawful if its `traverse` satisfies a
number of additional properties.  It must send `pure : α → Id α` to `pure`,
send the composition of applicative functors to the composition of the
`traverse` of each, send each function `f` to `fun x ↦ f <$> x`, and
satisfy a naturality condition with respect to applicative
transformations.  -/
LawfulTraversable : (t : Type u → Type u) → [Traversable t] → Prop
-- Mathlib.MeasureTheory.PiSystem
isPiSystem_image_Ioi : ∀ {α : Type u_1} [inst : LinearOrder α] (s : Set α), IsPiSystem (Set.Ioi '' s)
-- Init.Data.Int.Order
Int.neg_lt_of_neg_lt : ∀ {a b : ℤ}, -a < b → -b < a
-- Mathlib.Algebra.Group.Hom.Defs
AddHom.coe_coe : ∀ {M : Type u_4} {N : Type u_5} {F : Type u_9} [inst : Add M] [inst_1 : Add N] [inst_2 : FunLike F M N]
  [inst_3 : AddHomClass F M N] (f : F), ⇑↑f = ⇑f
-- Mathlib.RingTheory.Etale.Finite
CommAlgCat.FiniteEtale.baseChange_map_hom : ∀ (R : Type u) [inst : CommRing R] (S : Type w) [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {A B : CommAlgCat.FiniteEtale R} (f : A ⟶ B),
  ((CommAlgCat.FiniteEtale.baseChange R S).map f).hom =
    CommAlgCat.ofHom (Algebra.TensorProduct.map (AlgHom.id S S) (CommAlgCat.Hom.hom f.hom))
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.XIsoOfEq_rfl : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (K : HomologicalComplex V c) (p : ι),
  K.XIsoOfEq ⋯ = CategoryTheory.Iso.refl (K.X p)
-- Mathlib.Analysis.Complex.Exponential
Real.exp_bound : ∀ {x : ℝ},
  |x| ≤ 1 →
    ∀ {n : ℕ},
      0 < n → |Real.exp x - ∑ m ∈ Finset.range n, x ^ m / ↑m.factorial| ≤ |x| ^ n * (↑n.succ / (↑n.factorial * ↑n))
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
SemiNormedGrp.explicitCokernelπ_apply_dom_eq_zero : ∀ {X Y : SemiNormedGrp} {f : X ⟶ Y} (x : X.carrier),
  (CategoryTheory.ConcreteCategory.hom (SemiNormedGrp.explicitCokernelπ f))
      ((CategoryTheory.ConcreteCategory.hom f) x) =
    0
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
CategoryTheory.Bicategory.Equivalence.mk : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {a b : B} →
      (hom : a ⟶ b) →
        (inv : b ⟶ a) →
          (unit : CategoryTheory.CategoryStruct.id a ≅ CategoryTheory.CategoryStruct.comp hom inv) →
            (counit : CategoryTheory.CategoryStruct.comp inv hom ≅ CategoryTheory.CategoryStruct.id b) →
              autoParam
                  (CategoryTheory.Bicategory.leftZigzagIso unit counit =
                    CategoryTheory.Bicategory.leftUnitor hom ≪≫ (CategoryTheory.Bicategory.rightUnitor hom).symm)
                  CategoryTheory.Bicategory.Equivalence.left_triangle._autoParam →
                CategoryTheory.Bicategory.Equivalence a b
-- Init.Data.Int.Order
Int.sign_mul : ∀ (a b : ℤ), (a * b).sign = a.sign * b.sign
-- Mathlib.CategoryTheory.Discrete.Basic
CategoryTheory.Discrete.natIso_inv_app : ∀ {C : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} C] {I : Type u₁}
  {F G : CategoryTheory.Functor (CategoryTheory.Discrete I) C} (f : (i : CategoryTheory.Discrete I) → F.obj i ≅ G.obj i)
  (X : CategoryTheory.Discrete I), (CategoryTheory.Discrete.natIso f).inv.app X = (f X).inv
-- Mathlib.Topology.Algebra.Group.Torsor
Homeomorph.vaddConst.eq_1 : ∀ {V : Type u_1} {P : Type u_2} [inst : AddGroup V] [inst_1 : TopologicalSpace V] [inst_2 : AddTorsor V P]
  [inst_3 : TopologicalSpace P] [inst_4 : IsTopologicalAddTorsor P] (p : P),
  Homeomorph.vaddConst p = { toEquiv := Equiv.vaddConst p, continuous_toFun := ⋯, continuous_invFun := ⋯ }
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalSubsemiring.map_bot : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocSemiring R] [inst_1 : NonUnitalNonAssocSemiring S] {F : Type u_1}
  [inst_2 : FunLike F R S] [inst_3 : NonUnitalRingHomClass F R S] (f : F), NonUnitalSubsemiring.map f ⊥ = ⊥
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
/-- Change of variables for monotone functions.
If `f` is continuous on `[a, b]` and has a nonnegative derivative `f'` in `(a, b)`,
then we can substitute `u = f x` to get `∫ x in a..b, (g ∘ f) x * f' x = ∫ u in f a..f b, g u`.  -/
intervalIntegral.integral_comp_mul_deriv_of_deriv_nonneg : ∀ {a b : ℝ} {f f' g : ℝ → ℝ},
  ContinuousOn f (Set.uIcc a b) →
    (∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivAt f (f' x) x) →
      (∀ x ∈ Set.Ioo (min a b) (max a b), 0 ≤ f' x) → ∫ (x : ℝ) in a..b, (g ∘ f) x * f' x = ∫ (u : ℝ) in f a..f b, g u
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddSubsemigroup.coe_equivMapOfInjective_apply : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (S : AddSubsemigroup M) (f : M →ₙ+ N)
  (hf : Function.Injective ⇑f) (x : ↥S), ↑((S.equivMapOfInjective f hf) x) = f ↑x
-- Mathlib.Combinatorics.Additive.Energy
Finset.mulEnergy_mono_left : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Mul α] {s₁ s₂ t : Finset α}, s₁ ⊆ s₂ → s₁.mulEnergy t ≤ s₂.mulEnergy t
-- Mathlib.Order.JordanHolder
JordanHolderLattice.isMaximal_inf_left_of_isMaximal_sup : ∀ {X : Type u} {inst : Lattice X} [self : JordanHolderLattice X] {x y : X},
  JordanHolderLattice.IsMaximal x (x ⊔ y) →
    JordanHolderLattice.IsMaximal y (x ⊔ y) → JordanHolderLattice.IsMaximal (x ⊓ y) x
-- Mathlib.Algebra.Ring.Semiconj
SemiconjBy.sub_left : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] {a b x y : R},
  SemiconjBy a x y → SemiconjBy b x y → SemiconjBy (a - b) x y
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.hom_ext : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {A B : CategoryTheory.Grp C} (f g : A ⟶ B), f.hom.hom = g.hom.hom → f = g
-- Mathlib.LinearAlgebra.Dimension.Constructions
subalgebra_top_rank_eq_submodule_top_rank : ∀ {F : Type u_2} {E : Type u_3} [inst : CommSemiring F] [inst_1 : Semiring E] [inst_2 : Algebra F E],
  Module.rank F ↥⊤ = Module.rank F ↥⊤
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.intervalIntegral_im : ∀ {𝕜 : Type u_8} [inst : RCLike 𝕜] {f : ℝ → 𝕜} {a b : ℝ} {μ : MeasureTheory.Measure ℝ},
  IntervalIntegrable f μ a b → ∫ (x : ℝ) in a..b, RCLike.im (f x) ∂μ = RCLike.im (∫ (x : ℝ) in a..b, f x ∂μ)
-- Mathlib.Topology.Algebra.Group.Units
/-- Any `ContinuousMulEquiv` induces a `ContinuousMulEquiv` on units.  -/
Units.mapContinuousMulEquiv : {M : Type u_1} →
  {N : Type u_2} →
    [inst : TopologicalSpace M] →
      [inst_1 : TopologicalSpace N] → [inst_2 : Monoid M] → [inst_3 : Monoid N] → M ≃ₜ* N → Mˣ ≃ₜ* Nˣ
-- Mathlib.Combinatorics.SimpleGraph.Hamiltonian
/-- The length of a Hamiltonian path is one less than the number of vertices of the graph.  -/
SimpleGraph.Walk.IsHamiltonian.length_eq : ∀ {α : Type u_1} [inst : DecidableEq α] {G : SimpleGraph α} {a b : α} {p : G.Walk a b} [inst_1 : Fintype α],
  p.IsHamiltonian → p.length = Fintype.card α - 1
-- Mathlib.CategoryTheory.Quotient.LocallySmall
CategoryTheory.Quotient.instLocallySmall : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (r : HomRel C) [CategoryTheory.LocallySmall.{w, v, u} C],
  CategoryTheory.LocallySmall.{w, v, u} (CategoryTheory.Quotient r)
-- Std.Data.HashMap.Raw
/-- Modifies in place the value associated with a given key.

This function ensures that the value is used linearly.
 -/
Std.HashMap.Raw.modify : {α : Type u} →
  {β : Type v} → [inst : BEq α] → [EquivBEq α] → [Hashable α] → Std.HashMap.Raw α β → α → (β → β) → Std.HashMap.Raw α β
-- Init.Data.Int.DivMod.Lemmas
Int.fmod.eq_5 : ∀ (m n : ℕ), (Int.negSucc m).fmod (Int.negSucc n) = -Int.ofNat (m.succ % n.succ)
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.SInt
Int16.reduceOfInt : Lean.Meta.Simp.DSimproc
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
/-- The inverse `LinearIsometryEquiv`.  -/
LinearIsometryEquiv.symm : {R : Type u_1} →
  {R₂ : Type u_2} →
    {E : Type u_5} →
      {E₂ : Type u_6} →
        [inst : Semiring R] →
          [inst_1 : Semiring R₂] →
            {σ₁₂ : R →+* R₂} →
              {σ₂₁ : R₂ →+* R} →
                [inst_2 : RingHomInvPair σ₁₂ σ₂₁] →
                  [inst_3 : RingHomInvPair σ₂₁ σ₁₂] →
                    [inst_4 : SeminormedAddCommGroup E] →
                      [inst_5 : SeminormedAddCommGroup E₂] →
                        [inst_6 : Module R E] → [inst_7 : Module R₂ E₂] → (E ≃ₛₗᵢ[σ₁₂] E₂) → E₂ ≃ₛₗᵢ[σ₂₁] E
-- Mathlib.Analysis.Complex.HalfPlane
/-- An open left half-plane (with boundary real part given by an `EReal`) is an open set
in the complex plane.  -/
Complex.isOpen_re_lt_EReal : ∀ (x : EReal), IsOpen {z | ↑z.re < x}
-- Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
exists_isTranscendenceBasis_subset : ∀ {R : Type u_1} {A : Type w} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] [NoZeroDivisors A]
  [FaithfulSMul R A] (s : Set A) [Algebra.IsAlgebraic (↥(Algebra.adjoin R s)) A],
  ∃ t ⊆ s, IsTranscendenceBasis R Subtype.val
-- Mathlib.CategoryTheory.Triangulated.TStructure.Basic
CategoryTheory.Triangulated.TStructure.isGE_of_shift : ∀ {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]
  (t : CategoryTheory.Triangulated.TStructure C) (X : C) (n a n' : ℤ),
  autoParam (a + n' = n) CategoryTheory.Triangulated.TStructure.isGE_of_shift._auto_1 →
    ∀ [t.IsGE ((CategoryTheory.shiftFunctor C a).obj X) n'], t.IsGE X n
-- Mathlib.CategoryTheory.PUnit
/-- Functors from `Discrete PUnit` are equivalent to the category itself.  -/
CategoryTheory.Functor.equiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Functor (CategoryTheory.Discrete PUnit.{w + 1}) C ≌ C
-- Mathlib.AlgebraicTopology.SimplicialSet.Basic
SSet.δ_comp_δ_apply : ∀ {S : SSet} {n : ℕ} {i j : Fin (n + 2)},
  i ≤ j →
    ∀ (x : S.obj (Opposite.op { len := n + 2 })),
      (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ S i))
          ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ S j.succ)) x) =
        (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ S j))
          ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ S i.castSucc)) x)
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MulticospanIndex.sndPiMap_π_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape}
  (I : CategoryTheory.Limits.MulticospanIndex J C) [inst_1 : CategoryTheory.Limits.HasProduct I.left]
  [inst_2 : CategoryTheory.Limits.HasProduct I.right] (b : J.R) {Z : C} (h : I.right b ⟶ Z),
  CategoryTheory.CategoryStruct.comp I.sndPiMap
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π I.right b) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π I.left (J.snd b))
      (CategoryTheory.CategoryStruct.comp (I.snd b) h)
-- Lean.Data.Lsp.Internal
Lean.Lsp.instFromJsonLeanStaleDependencyParams.fromJson : Lean.Json → Except String Lean.Lsp.LeanStaleDependencyParams
-- Std.Tactic.BVDecide.LRAT.Internal.LRATCheckerSound
Std.Tactic.BVDecide.LRAT.Internal.lratChecker.match_3.congr_eq_1 : ∀ {α : Type u_1} {β : Type u_2} (motive : List (Std.Tactic.BVDecide.LRAT.Action β α) → Sort u_3)
  (prf : List (Std.Tactic.BVDecide.LRAT.Action β α)) (h_1 : Unit → motive [])
  (h_2 :
    (id : ℕ) →
      (rupHints : Array ℕ) →
        (tail : List (Std.Tactic.BVDecide.LRAT.Action β α)) →
          motive (Std.Tactic.BVDecide.LRAT.Action.addEmpty id rupHints :: tail))
  (h_3 :
    (id : ℕ) →
      (c : β) →
        (rupHints : Array ℕ) →
          (restPrf : List (Std.Tactic.BVDecide.LRAT.Action β α)) →
            motive (Std.Tactic.BVDecide.LRAT.Action.addRup id c rupHints :: restPrf))
  (h_4 :
    (id : ℕ) →
      (c : β) →
        (pivot : Std.Sat.Literal α) →
          (rupHints : Array ℕ) →
            (ratHints : Array (ℕ × Array ℕ)) →
              (restPrf : List (Std.Tactic.BVDecide.LRAT.Action β α)) →
                motive (Std.Tactic.BVDecide.LRAT.Action.addRat id c pivot rupHints ratHints :: restPrf))
  (h_5 :
    (ids : Array ℕ) →
      (restPrf : List (Std.Tactic.BVDecide.LRAT.Action β α)) →
        motive (Std.Tactic.BVDecide.LRAT.Action.del ids :: restPrf)),
  prf = [] →
    (match prf with
      | [] => h_1 ()
      | Std.Tactic.BVDecide.LRAT.Action.addEmpty id rupHints :: tail => h_2 id rupHints tail
      | Std.Tactic.BVDecide.LRAT.Action.addRup id c rupHints :: restPrf => h_3 id c rupHints restPrf
      | Std.Tactic.BVDecide.LRAT.Action.addRat id c pivot rupHints ratHints :: restPrf =>
        h_4 id c pivot rupHints ratHints restPrf
      | Std.Tactic.BVDecide.LRAT.Action.del ids :: restPrf => h_5 ids restPrf) ≍
      h_1 ()
-- Mathlib.Algebra.Lie.Weights.IsSimple
/-- The submodule spanned by roots of a Lie ideal is invariant under all root reflections.  -/
LieIdeal.rootSpan_mem_invtRootSubmodule : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : LieRing L] [inst_2 : LieAlgebra K L]
  [inst_3 : FiniteDimensional K L] {H : LieSubalgebra K L} [inst_4 : H.IsCartanSubalgebra] [inst_5 : CharZero K]
  [inst_6 : LieAlgebra.IsKilling K L] [inst_7 : LieModule.IsTriangularizable K (↥H) L] (I : LieIdeal K L),
  I.rootSpan ∈ (LieAlgebra.IsKilling.rootSystem H).invtRootSubmodule
-- Mathlib.RingTheory.Bialgebra.Equiv
/-- See Note [custom simps projection]  -/
BialgEquiv.Simps.apply : {R : Type u} →
  [inst : CommSemiring R] →
    {α : Type v} →
      {β : Type w} →
        [inst_1 : Semiring α] →
          [inst_2 : Semiring β] →
            [inst_3 : Algebra R α] →
              [inst_4 : Algebra R β] →
                [inst_5 : CoalgebraStruct R α] → [inst_6 : CoalgebraStruct R β] → (α ≃ₐc[R] β) → α → β
-- Init.Data.String.Defs
String.push.eq_1 : ∀ (x : Char) (b : ByteArray) (h : b.IsValidUTF8),
  { toByteArray := b, isValidUTF8 := h }.push x = { toByteArray := b.append [x].utf8Encode, isValidUTF8 := ⋯ }
-- Mathlib.Combinatorics.SimpleGraph.Diam
SimpleGraph.ediam_eq_top_iff_radius_eq_top : ∀ {α : Type u_1} {G : SimpleGraph α} [Nonempty α], G.ediam = ⊤ ↔ G.radius = ⊤
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.HomotopyEquiv.symm_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (e : S₁.HomotopyEquiv S₂), e.symm.inv = e.hom