mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Convex.ConvexSpace.AffineSpace
/-- Any affine space is a convex space.

This is not an instance because its convex combination operation is defined through the choice of an
arbitrary basepoint, which makes it very diamond-prone.  -/
AddTorsor.toConvexSpace : {R : Type u_1} →
  {V : Type u_2} →
    {P : Type u_3} →
      [inst : Ring R] →
        [inst_1 : PartialOrder R] →
          [inst_2 : IsStrictOrderedRing R] →
            [inst_3 : AddCommGroup V] → [Module R V] → [AddTorsor V P] → Convexity.ConvexSpace R P
-- Std.Data.HashSet.Raw
Std.HashSet.Raw.instSingletonOfBEqOfHashable : {α : Type u} → [BEq α] → [Hashable α] → Singleton α (Std.HashSet.Raw α)
-- Lean.Elab.InfoTree.Types
Lean.Elab.PartialContextInfo.autoImplicitCtx.sizeOf_spec : ∀ (autoImplicits : Array Lean.Expr),
  sizeOf (Lean.Elab.PartialContextInfo.autoImplicitCtx autoImplicits) = 1 + sizeOf autoImplicits
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get_insertIfNew : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] (h : (↑m).WF) {k a : α} {v : β}
  {h₁ : (m.insertIfNew k v).contains a = true},
  Std.DHashMap.Internal.Raw₀.Const.get (m.insertIfNew k v) a h₁ =
    if h₂ : (k == a) = true ∧ m.contains k = false then v else Std.DHashMap.Internal.Raw₀.Const.get m a ⋯
-- Mathlib.Topology.Algebra.Module.Equiv
/-- The inverse of `equivOfInverse'` is obtained by swapping the order of its parameters.  -/
ContinuousLinearEquiv.symm_equivOfInverse' : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁}
  [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [inst_4 : TopologicalSpace M₁]
  [inst_5 : AddCommMonoid M₁] {M₂ : Type u_5} [inst_6 : TopologicalSpace M₂] [inst_7 : AddCommMonoid M₂]
  [inst_8 : Module R₁ M₁] [inst_9 : Module R₂ M₂] (f₁ : M₁ →SL[σ₁₂] M₂) (f₂ : M₂ →SL[σ₂₁] M₁)
  (h₁ : f₁ ∘SL f₂ = ContinuousLinearMap.id R₂ M₂) (h₂ : f₂ ∘SL f₁ = ContinuousLinearMap.id R₁ M₁),
  (ContinuousLinearEquiv.equivOfInverse' f₁ f₂ h₁ h₂).symm = ContinuousLinearEquiv.equivOfInverse' f₂ f₁ h₂ h₁
-- Mathlib.RingTheory.Localization.FractionRing
IsFractionRing.algEquivOfAlgEquiv_symm : ∀ {R : Type u_8} {A : Type u_9} {K : Type u_10} {B : Type u_11} {L : Type u_12} [inst : CommSemiring R]
  [inst_1 : CommRing A] [inst_2 : CommRing B] [inst_3 : CommRing K] [inst_4 : CommRing L] [inst_5 : Algebra R A]
  [inst_6 : Algebra R K] [inst_7 : Algebra A K] [inst_8 : IsFractionRing A K] [inst_9 : IsScalarTower R A K]
  [inst_10 : Algebra R B] [inst_11 : Algebra R L] [inst_12 : Algebra B L] [inst_13 : IsFractionRing B L]
  [inst_14 : IsScalarTower R B L] (h : A ≃ₐ[R] B),
  (IsFractionRing.algEquivOfAlgEquiv h).symm = IsFractionRing.algEquivOfAlgEquiv h.symm
-- Mathlib.Computability.TuringDegree
/-- A partial function `f` is partial recursive if and only if it is recursive in
every partial function `g`.  -/
partrec_iff_forall_turingReducible : ∀ {f : ℕ →. ℕ}, Partrec f ↔ ∀ (g : ℕ →. ℕ), TuringReducible f g
-- Mathlib.Analysis.Polynomial.Basic
/-- **Alias** of `Polynomial.eventually_atTop_not_isRoot`. -/
Polynomial.eventually_no_roots : ∀ {𝕜 : Type u_1} [inst : NormedField 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (P : Polynomial 𝕜),
  P ≠ 0 → ∀ᶠ (x : 𝕜) in Filter.atTop, ¬P.IsRoot x
-- Batteries.Tactic.GeneralizeProofs
/-- (Debugging) When `true`, enables consistency checks.  -/
Batteries.Tactic.GeneralizeProofs.Config.debug : Batteries.Tactic.GeneralizeProofs.Config → Bool
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
CategoryTheory.Bicategory.Adj.forget₁_toPrelaxFunctor_toPrelaxFunctorStruct_map₂ : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : CategoryTheory.Bicategory.Adj B} {f g : a ⟶ b} (α : f ⟶ g),
  CategoryTheory.Bicategory.Adj.forget₁.map₂ α = α.τl
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.Precoverage.instSmallOfSmall : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.Precoverage C) [J.Small] {S : C}
  (E : J.ZeroHypercover S), E.Small
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.haar.mul_left_index_le : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G] {K : Set G},
  IsCompact K →
    ∀ {V : Set G},
      (interior V).Nonempty →
        ∀ (g : G), MeasureTheory.Measure.haar.index ((fun h => g * h) '' K) V ≤ MeasureTheory.Measure.haar.index K V
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.liftOnWellOrder_type : ∀ {δ : Sort v} (f : (α : Type u_1) → [inst : LinearOrder α] → [WellFoundedLT α] → δ)
  (c :
    ∀ (α : Type u_1) [inst : LinearOrder α] [inst_1 : WellFoundedLT α] (β : Type u_1) [inst_2 : LinearOrder β]
      [inst_3 : WellFoundedLT β], ((Ordinal.type fun x1 x2 => x1 < x2) = Ordinal.type fun x1 x2 => x1 < x2) → f α = f β)
  {γ : Type u_1} [inst : LinearOrder γ] [inst_1 : WellFoundedLT γ],
  (Ordinal.type fun x1 x2 => x1 < x2).liftOnWellOrder f c = f γ
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
hasMFDerivAt_unique : ∀ {𝕜 : 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} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {x : M}
  {f₀' f₁' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)}, HasMFDerivAt% f x f₀' → HasMFDerivAt% f x f₁' → f₀' = f₁'
-- Mathlib.Algebra.Group.Pi.Lemmas
/-- The injection into an additive pi group at different indices commutes.

For injections of commuting elements at the same index, see `AddCommute.map`  -/
Pi.single_addCommute : ∀ {I : Type u} {f : I → Type v} [inst : DecidableEq I] [inst_1 : (i : I) → AddZeroClass (f i)],
  Pairwise fun i j => ∀ (x : f i) (y : f j), AddCommute (Pi.single i x) (Pi.single j y)
-- Init.Data.SInt.Lemmas
Int16.toISize_div_of_ne_left : ∀ (a b : Int16), a ≠ Int16.minValue → (a / b).toISize = a.toISize / b.toISize
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.ExBaseNat.sum.injEq : ∀ {e : Q(ℕ)} (x x_1 : Mathlib.Tactic.Ring.Common.ExSumNat e),
  (Mathlib.Tactic.Ring.Common.ExBaseNat.sum x = Mathlib.Tactic.Ring.Common.ExBaseNat.sum x_1) = (x = x_1)
-- Mathlib.Order.Filter.IsBounded
/-- For nontrivial filters in linear orders, coboundedness for `≤` implies frequent boundedness
from below.  -/
Filter.IsCobounded.frequently_ge : ∀ {α : Type u_1} {f : Filter α} [inst : LinearOrder α] [f.NeBot],
  Filter.IsCobounded (fun x1 x2 => x1 ≤ x2) f → ∃ l, ∃ᶠ (x : α) in f, l ≤ x
-- Init.Data.OfScientific
Float.ofScientific : ℕ → Bool → ℕ → Float
-- Lean.Meta.Basic
/-- Realizes and caches a value for a given key with all environment objects derived from calling
`enableRealizationsForConst forConst` (fails if not called yet). If
this is the first environment branch passing the specific `key`, `realize` is called with the
environment and options at the time of calling `enableRealizationsForConst` if `forConst` is from
the current module and the state just after importing  otherwise, thus helping achieve deterministic
results despite the non-deterministic choice of which thread is tasked with realization. In other
words, the result of `realizeValue` is *as if* `realize` had been called immediately after
`enableRealizationsForConst forConst`, with most effects but the return value discarded (see below).
Whether two calls of `realizeValue` with different `forConst`s but the same `key` share the result
is undefined; in practice, the key should usually uniquely determine `forConst` by e.g. including it
as a field.

`realizeValue` cannot check what other data is captured in the `realize` closure,
so it is best practice to extract it into a separate function and pass only arguments uniquely
determined by `key`. Traces, diagnostics, and raw std stream
output of `realize` are reported at all callers via `Core.logSnapshotTask` (so that the location of
generated diagnostics is deterministic). Note that, as `realize` is run using the options at
declaration time of `forConst`, trace options must be set prior to that (or, for imported constants,
on the cmdline) in order to be active. If `realize` throws an exception, it is rethrown at all
callers.

CAVEAT: `realize` MUST NOT reference the current environment (the result of `getEnv`) in its result
to avoid creating an un-collectable promise cycle.
 -/
Lean.Meta.realizeValue : {α : Type u_1} →
  {β : Type} → [BEq α] → [Hashable α] → [TypeName α] → [TypeName β] → Lean.Name → α → Lean.MetaM β → Lean.MetaM β
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.one_lt_aleph0 : 1 < Cardinal.aleph0
-- Mathlib.Topology.EMetricSpace.BoundedVariation
/-- If a function is continuous on the left at a point `a`, then its variations on `Iio a` and
on `Iic a` coincide. We give a version relative to a set `s`.  -/
eVariationOn.eVariationOn_inter_Iio_eq_inter_Iic_of_continuousWithinAt : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] [inst_2 : TopologicalSpace α]
  [OrderTopology α] {f : α → E} {s : Set α} {a : α},
  (nhdsWithin a (s ∩ Set.Iio a)).NeBot →
    ContinuousWithinAt f (s ∩ Set.Iic a) a → eVariationOn f (s ∩ Set.Iio a) = eVariationOn f (s ∩ Set.Iic a)
-- Mathlib.RingTheory.Ideal.Maps
Submodule.annihilator_top : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  ⊤.annihilator = Module.annihilator R M
-- Mathlib.Data.DFinsupp.Interval
DFinsupp.pi.eq_1 : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Zero (α i)] [inst_1 : DecidableEq ι]
  [inst_2 : (i : ι) → DecidableEq (α i)] (f : Π₀ (i : ι), Finset (α i)), f.pi = f.support.dfinsupp ⇑f
-- Mathlib.GroupTheory.MonoidLocalization.GrothendieckGroup
Algebra.GrothendieckAddGroup.neg_mk : ∀ {M : Type u_1} [inst : AddCommMonoid M] (m : M) (s : ↥⊤), -AddLocalization.mk m s = AddLocalization.mk ↑s ⟨m, ⋯⟩
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Ioc_union_Ioo_eq_Ioo : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c : α}, a ≤ b → b < c → Set.Ioc a b ∪ Set.Ioo b c = Set.Ioo a c
-- Mathlib.Order.Atoms
IsCoatom.Ici_eq : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : OrderTop α] {a : α}, IsCoatom a → Set.Ici a = {⊤, a}
-- Lean.Data.Lsp.Communication
Lean.IO.FS.Stream.readLspResponseAs : IO.FS.Stream → Lean.JsonRpc.RequestID → (α : Type) → [Lean.FromJson α] → IO (Lean.JsonRpc.Response α)
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
/-- If `g : ℝ → ℝ` is periodic with period `T > 0` and `0 < ∫ x in 0..T, 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 →
    0 < ∫ (x : ℝ) in 0..T, g x → 0 < T → Filter.Tendsto (fun t => ∫ (x : ℝ) in 0..t, g x) Filter.atBot Filter.atBot
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
SemilinearIsometryClass.diam_range : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} {𝓕 : Type u_10} [inst : Semiring R]
  [inst_1 : Semiring R₂] {σ₁₂ : R →+* R₂} [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup E₂]
  [inst_4 : Module R E] [inst_5 : Module R₂ E₂] [inst_6 : FunLike 𝓕 E E₂] [SemilinearIsometryClass 𝓕 σ₁₂ E E₂] (f : 𝓕),
  Metric.diam (Set.range ⇑f) = Metric.diam Set.univ
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
fderiv_sin : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {x : E},
  DifferentiableAt ℝ f x → fderiv ℝ (fun x => Real.sin (f x)) x = Real.cos (f x) • fderiv ℝ f x
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.rTensor_apply : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [inst : CommSemiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : AddCommMonoid U] [inst_5 : Module A V]
  [inst_6 : Module A W] [inst_7 : Module A U] {ρ : Representation A G V} {σ : Representation A G W}
  {τ : Representation A G U} (f : σ.IntertwiningMap τ) (v : V) (w : W),
  (Representation.IntertwiningMap.rTensor ρ f) (w ⊗ₜ[A] v) = f w ⊗ₜ[A] v
-- Mathlib.Data.Multiset.Filter
Multiset.count_filter_of_neg : ∀ {α : Type u_1} [inst : DecidableEq α] {p : α → Prop} [inst_1 : DecidablePred p] {a : α} {s : Multiset α},
  ¬p a → Multiset.count a (Multiset.filter p s) = 0
-- Lean.Meta.TryThis
/-- A raw string to be used as suggested replacement text in the infoview.  -/
Lean.Meta.Tactic.TryThis.SuggestionText.string : String → Lean.Meta.Tactic.TryThis.SuggestionText
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.IsAffineOpen.fromSpec_top : ∀ {X : AlgebraicGeometry.Scheme} [inst : AlgebraicGeometry.IsAffine X], ⋯.fromSpec = X.isoSpec.inv
-- Mathlib.Algebra.Group.Conj
mem_addConjugatesOf_self : ∀ {α : Type u} [inst : AddMonoid α] {a : α}, a ∈ addConjugatesOf a
-- Mathlib.Algebra.Group.Subgroup.Actions
MonoidWithZeroHom.comap_mker : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : MulZeroOneClass M] [inst_1 : MulZeroOneClass N]
  [inst_2 : MulZeroOneClass P] (g : N →*₀ P) (f : M →*₀ N),
  Submonoid.comap f (MonoidHom.mker g) = MonoidHom.mker (g.comp f)
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
/-- Reindexing both indices along the same equivalence preserves the determinant.

For the `simp` version of this lemma, see `det_submatrix_equiv_self`; this one is unsuitable because
`Matrix.reindex_apply` unfolds `reindex` first.
 -/
Matrix.det_reindex_self : ∀ {m : Type u_1} {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : DecidableEq m]
  [inst_3 : Fintype m] {R : Type v} [inst_4 : CommRing R] (e : m ≃ n) (A : Matrix m m R),
  ((Matrix.reindex e e) A).det = A.det
-- Mathlib.Tactic.ReduceModChar
Tactic.ReduceModChar.TypeToCharPResult.intLike.injEq : ∀ {u : Lean.Level} {α : Q(Type u)} (n : Q(ℕ)) (instRing : Q(Ring «$α»)) (instCharP : Q(CharP «$α» «$n»)) (n_1 : Q(ℕ))
  (instRing_1 : Q(Ring «$α»)) (instCharP_1 : Q(CharP «$α» «$n_1»)),
  (Tactic.ReduceModChar.TypeToCharPResult.intLike n instRing instCharP =
      Tactic.ReduceModChar.TypeToCharPResult.intLike n_1 instRing_1 instCharP_1) =
    (n = n_1 ∧ instRing = instRing_1 ∧ instCharP = instCharP_1)
-- Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexEvaluation
SSet.Subcomplex.instPreservesColimitsOfShapeToSSetFunctorOfIsFilteredOrEmpty : ∀ {J : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} J] {X : SSet} [CategoryTheory.IsFilteredOrEmpty J],
  CategoryTheory.Limits.PreservesColimitsOfShape J SSet.Subcomplex.toSSetFunctor
-- Mathlib.Data.Set.Lattice
Set.mem_iInter_of_mem : ∀ {α : Type u_1} {ι : Sort u_5} {s : ι → Set α} {a : α}, (∀ (i : ι), a ∈ s i) → a ∈ ⋂ i, s i
-- Mathlib.Algebra.Order.Monoid.WithTop
WithTop.canonicallyOrderedAdd : ∀ {α : Type u} [inst : Add α] [inst_1 : Preorder α] [CanonicallyOrderedAdd α], CanonicallyOrderedAdd (WithTop α)
-- Mathlib.RingTheory.Localization.Basic
Localization.mk_intCast : ∀ {R : Type u_1} [inst : CommRing R] {M : Submonoid R} (m : ℤ), Localization.mk (↑m) 1 = ↑m
-- Mathlib.LinearAlgebra.Quotient.Basic
Submodule.map_liftQ : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (p : Submodule R M)
  {R₂ : Type u_3} {M₂ : Type u_4} [inst_3 : Ring R₂] [inst_4 : AddCommGroup M₂] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂) (h : p ≤ f.ker) (q : Submodule R (M ⧸ p)),
  Submodule.map (p.liftQ f h) q = Submodule.map f (Submodule.comap p.mkQ q)
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
/-- A rational map is an `S`-map if some partial map in the equivalence class is an `S`-map.  -/
AlgebraicGeometry.Scheme.RationalMap.IsOver : {X Y : AlgebraicGeometry.Scheme} → (S : AlgebraicGeometry.Scheme) → [X.Over S] → [Y.Over S] → X.RationalMap Y → Prop
-- Std.Do.SPred.SPred
/-- A predicate over states, where each state is defined by a list of component state types.

Example:
```lean example
SPred [Nat, Bool] = (Nat → Bool → ULift Prop)
```
 -/
Std.Do.SPred : List (Type u) → Type u
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.setToFun.congr_simp : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} (μ μ_1 : MeasureTheory.Measure α)
  (e_μ : μ = μ_1) (T T_1 : Set α → E →L[ℝ] F) (e_T : T = T_1) {C C_1 : ℝ} (e_C : C = C_1)
  (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) (f f_1 : α → E),
  f = f_1 → MeasureTheory.setToFun μ T hT f = MeasureTheory.setToFun μ_1 T_1 ⋯ f_1
-- Mathlib.Data.List.Basic
List.foldr_fixed' : ∀ {α : Type u} {β : Type v} {f : α → β → β} {b : β}, (∀ (a : α), f a b = b) → ∀ (l : List α), List.foldr f b l = b
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddSubmonoid.LocalizationMap.mk'_add_cancel_left : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
  (f : S.LocalizationMap N) (x : M) (y : ↥S), f.mk' (↑y + x) y = f x
-- Mathlib.Order.Heyting.Basic
PUnit.himp_eq : ∀ (a b : PUnit.{u + 1}), a ⇨ b = PUnit.unit
-- Mathlib.RingTheory.RootsOfUnity.Basic
Units.val_set_image_rootsOfUnity : ∀ {R : Type u_4} {k : ℕ} [inst : CommMonoid R] [NeZero k], Units.val '' ↑(rootsOfUnity k R) = {z | z ^ k = 1}
-- Mathlib.CategoryTheory.GradedObject.Trifunctor
/-- Given bifunctors `F : C₁ ⥤ C₂₃ ⥤ C₄`, `G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃`, graded objects
`X₁ : GradedObject I₁ C₁`, `X₂ : GradedObject I₂ C₂`, `X₃ : GradedObject I₃ C₃` and
`ρ₂₃ : BifunctorComp₂₃IndexData r`, this asserts that for all `i₁ : I₁` and `i₂₃ : ρ₂₃.I₂₃`,
the functor `F(X₁ i₁, _)` commutes with the coproducts of the `G₂₃(X₂ i₂, X₃ i₃)`
such that `ρ₂₃.p ⟨i₂, i₃⟩ = i₂₃`.  -/
CategoryTheory.GradedObject.HasGoodTrifunctor₂₃Obj : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {C₃ : Type u_3} →
      {C₄ : Type u_4} →
        {C₂₃ : Type u_6} →
          [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
            [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
              [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] →
                [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄] →
                  [inst_4 : CategoryTheory.Category.{v_6, u_6} C₂₃] →
                    CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄) →
                      CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃) →
                        {I₁ : Type u_7} →
                          {I₂ : Type u_8} →
                            {I₃ : Type u_9} →
                              {J : Type u_10} →
                                {r : I₁ × I₂ × I₃ → J} →
                                  CategoryTheory.GradedObject.BifunctorComp₂₃IndexData r →
                                    CategoryTheory.GradedObject I₁ C₁ →
                                      CategoryTheory.GradedObject I₂ C₂ → CategoryTheory.GradedObject I₃ C₃ → Prop
-- Mathlib.Algebra.Lie.CartanSubalgebra
LieSubalgebra.normalizer_eq_self_of_isCartanSubalgebra : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (H : LieSubalgebra R L)
  [H.IsCartanSubalgebra], H.toLieSubmodule.normalizer = H.toLieSubmodule
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey!_eq_of_mem : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [LawfulBEq α] [inst : Inhabited α]
  {k : α}, k ∈ m → m.getKey! k = k
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.mulC_nc.go.induct_unfolding : ∀ (p₂ : Lean.Grind.CommRing.Poly) (c : ℕ)
  (motive : Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly → Prop),
  (∀ (acc : Lean.Grind.CommRing.Poly) (k : ℤ),
      motive (Lean.Grind.CommRing.Poly.num k) acc (acc.combineC (Lean.Grind.CommRing.Poly.mulConstC k p₂ c) c)) →
    (∀ (acc : Lean.Grind.CommRing.Poly) (k : ℤ) (m : Lean.Grind.CommRing.Mon) (p : Lean.Grind.CommRing.Poly),
        motive p (acc.combineC (Lean.Grind.CommRing.Poly.mulMonC_nc k m p₂ c) c)
            (Lean.Grind.CommRing.Poly.mulC_nc.go p₂ c p
              (acc.combineC (Lean.Grind.CommRing.Poly.mulMonC_nc k m p₂ c) c)) →
          motive (Lean.Grind.CommRing.Poly.add k m p) acc
            (Lean.Grind.CommRing.Poly.mulC_nc.go p₂ c p
              (acc.combineC (Lean.Grind.CommRing.Poly.mulMonC_nc k m p₂ c) c))) →
      ∀ (p₁ acc : Lean.Grind.CommRing.Poly), motive p₁ acc (Lean.Grind.CommRing.Poly.mulC_nc.go p₂ c p₁ acc)
-- Mathlib.Data.Seq.Computation
Computation.liftRel_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {δ : Type u_1} (R : α → β → Prop) (S : γ → δ → Prop) {s1 : Computation α}
  {s2 : Computation β} {f1 : α → γ} {f2 : β → δ},
  Computation.LiftRel R s1 s2 →
    (∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)) → Computation.LiftRel S (Computation.map f1 s1) (Computation.map f2 s2)
-- Mathlib.Tactic.DepRewrite
/-- `rw!` is like `rewrite!`, but also cleans up introduced refl-casts after every substitution.
It is available as an ordinary tactic and a `conv` tactic.
 -/
Mathlib.Tactic.DepRewrite.evalDepRwSeq : Lean.Elab.Tactic.Tactic
-- Mathlib.AlgebraicTopology.SimplicialSet.Horn
SSet.horn.edge_coe : ∀ (n : ℕ) (i a b : Fin (n + 1)) (hab : a ≤ b) (H : {i, a, b}.card ≤ n),
  ↑(SSet.horn.edge n i a b hab H) = SSet.stdSimplex.edge n a b hab
-- Mathlib.CategoryTheory.Presentable.Directed
/-- The functor which sends a `κ`-bounded diagram with a unique terminal object to
its terminal object.  -/
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.functor : (J : Type w) →
  [inst : CategoryTheory.SmallCategory J] →
    (κ : Cardinal.{w}) →
      CategoryTheory.Functor (CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.DiagramWithUniqueTerminal J κ)
        J
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
CategoryTheory.Limits.Fork.unop.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : Cᵒᵖ} {f g : X ⟶ Y}
  (c : CategoryTheory.Limits.Fork f g),
  c.unop =
    ((CategoryTheory.Limits.Cone.postcompose (CategoryTheory.Limits.opParallelPairIso f.unop g.unop).symm.hom).obj
        (CategoryTheory.Limits.Cone.whisker CategoryTheory.Limits.walkingParallelPairOpEquiv.inverse c)).unop
-- Mathlib.Tactic.Linarith.Parsing
/-- A single variable `n` is represented by a sum with coefficient `1` and monomial `n`.  -/
Mathlib.Tactic.Linarith.var : ℕ → Mathlib.Tactic.Linarith.Sum
-- Mathlib.Computability.Partrec
Nat.Partrec.below.pair : ∀ {motive : (a : ℕ →. ℕ) → Nat.Partrec a → Prop} {f g : ℕ →. ℕ} (a : Nat.Partrec f) (a_1 : Nat.Partrec g),
  Nat.Partrec.below a → motive f a → Nat.Partrec.below a_1 → motive g a_1 → Nat.Partrec.below ⋯
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.sin_neg : ∀ (θ : Real.Angle), (-θ).sin = -θ.sin
-- Lean.Data.Lsp.CodeActions
/-- The kind of a code action.

Kinds are a hierarchical list of identifiers separated by `.`,
e.g. `"refactor.extract.function"`.

The set of kinds is open and client needs to announce the kinds it supports
to the server during initialization.
You can make your own code action kinds, the ones supported by LSP are:
- `quickfix`
- `refactor`
  - `refactor.extract`
  - `refactor.inline`
  - `refactor.rewrite`
- `source` Source code actions apply to the entire file. Eg fixing all issues or organising imports.
  - `source.organizeImports`
  - `source.fixAll`
 -/
Lean.Lsp.CodeActionKind : Type
-- Lean.Expr
Lean.Literal.natVal.injEq : ∀ (val val_1 : ℕ), (Lean.Literal.natVal val = Lean.Literal.natVal val_1) = (val = val_1)
-- Lean.Meta.Sym.ReplaceS
_private.Lean.Meta.Sym.ReplaceS.0.Lean.Meta.Sym.visitChild.match_4.splitter : (motive : Option Lean.Expr → Sort u_1) →
  (__do_lift : Option Lean.Expr) →
    ((r : Lean.Expr) → motive (some r)) →
      ((x : Option Lean.Expr) → (∀ (r : Lean.Expr), x = some r → False) → motive x) → motive __do_lift
-- Mathlib.Algebra.Order.GroupWithZero.Basic
/-- See `lt_mul_inv_iff₀` for a version with multiplication on the other side.  -/
lt_mul_inv_iff₀' : ∀ {G₀ : Type u_3} [inst : CommGroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a b c : G₀},
  0 < c → (a < b * c⁻¹ ↔ c * a < b)