mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKeyD_diff_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k fallback : α}, k ∉ t₁ → (t₁ \ t₂).getKeyD k fallback = fallback
-- Mathlib.Algebra.Algebra.Spectrum.Basic
/-- Given a commutative ring `R` and an `R`-algebra `A`, the *resolvent set* of `a : A`
is the `Set R` consisting of those `r : R` for which `r•1 - a` is a unit of the
algebra `A`.  -/
resolventSet : (R : Type u) → {A : Type v} → [inst : CommSemiring R] → [inst_1 : Ring A] → [Algebra R A] → A → Set R
-- Mathlib.Topology.Algebra.Module.ModuleTopology
/-- A semilinear surjection to a module with the module topology is open.  -/
IsModuleTopology.isOpenMap_of_surjectiveₛₗ : ∀ {R : Type u_1} {S : Type u_2} [τR : TopologicalSpace R] [τS : TopologicalSpace S] [inst : Ring R] [inst_1 : Ring S]
  {A : Type u_3} [inst_2 : AddCommGroup A] [inst_3 : Module R A] [inst_4 : TopologicalSpace A] {B' : Type u_5}
  [inst_5 : AddCommGroup B'] [inst_6 : Module S B'] [inst_7 : TopologicalSpace B'] [IsModuleTopology S B']
  [ContinuousAdd A] [ContinuousSMul R A] {σ : R →+* S},
  IsOpenQuotientMap ⇑σ → ∀ (φ : A →ₛₗ[σ] B'), Function.Surjective ⇑φ → IsOpenMap ⇑φ
-- Init.Data.String.Basic
String.Pos.ofToSlice_inj : ∀ {s : String} {p q : s.toSlice.Pos}, String.Pos.ofToSlice p = String.Pos.ofToSlice q ↔ p = q
-- Mathlib.Algebra.Ring.SumsOfSquares
IsSumSq.zero : ∀ {R : Type u_1} [inst : Mul R] [inst_1 : Add R] [inst_2 : Zero R], IsSumSq 0
-- Std.Data.HashMap.Lemmas
Std.HashMap.Equiv.insertIfNew : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  (k : α) (v : β), m₁.Equiv m₂ → (m₁.insertIfNew k v).Equiv (m₂.insertIfNew k v)
-- Std.Http.Data.Headers.Basic
Std.Http.Header.Connection.mk.injEq : ∀ (tokens : Array String) (valid : tokens.all Std.Http.Internal.isToken = true) (tokens_1 : Array String)
  (valid_1 : tokens_1.all Std.Http.Internal.isToken = true),
  ({ tokens := tokens, valid := valid } = { tokens := tokens_1, valid := valid_1 }) = (tokens = tokens_1)
-- Mathlib.Computability.Reduce
isTrans_manyOneReducible : ∀ {α : Type u_1} [inst : Primcodable α], IsTrans (α → Prop) ManyOneReducible
-- Mathlib.Algebra.Ring.Subring.Units
/-- The subgroup of positive units of a linear ordered semiring.  -/
Units.posSubgroup : (R : Type u_1) → [inst : Semiring R] → [inst_1 : LinearOrder R] → [IsStrictOrderedRing R] → Subgroup Rˣ
-- Lean.Server.References
Lean.Server.Reference.mk.injEq : ∀ (ident : Lean.Lsp.RefIdent) (aliases : Array Lean.Lsp.RefIdent) (range : Lean.Lsp.Range) (stx : Lean.Syntax)
  (ci : Lean.Elab.ContextInfo) (info : Lean.Elab.Info) (isBinder : Bool) (ident_1 : Lean.Lsp.RefIdent)
  (aliases_1 : Array Lean.Lsp.RefIdent) (range_1 : Lean.Lsp.Range) (stx_1 : Lean.Syntax) (ci_1 : Lean.Elab.ContextInfo)
  (info_1 : Lean.Elab.Info) (isBinder_1 : Bool),
  ({ ident := ident, aliases := aliases, range := range, stx := stx, ci := ci, info := info, isBinder := isBinder } =
      { ident := ident_1, aliases := aliases_1, range := range_1, stx := stx_1, ci := ci_1, info := info_1,
        isBinder := isBinder_1 }) =
    (ident = ident_1 ∧
      aliases = aliases_1 ∧ range = range_1 ∧ stx = stx_1 ∧ ci = ci_1 ∧ info = info_1 ∧ isBinder = isBinder_1)
-- Mathlib.CategoryTheory.Limits.Final
/-- A pointfree version of `colimitIso`, stating that whiskering by `F` followed by taking the
colimit is isomorphic to taking the colimit on the codomain of `F`.  -/
CategoryTheory.Functor.Final.colimIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) →
          [F.Final] →
            {E : Type u₃} →
              [inst_3 : CategoryTheory.Category.{v₃, u₃} E] →
                [inst_4 : CategoryTheory.Limits.HasColimitsOfShape D E] →
                  [inst_5 : CategoryTheory.Limits.HasColimitsOfShape C E] →
                    ((CategoryTheory.Functor.whiskeringLeft C D E).obj F).comp CategoryTheory.Limits.colim ≅
                      CategoryTheory.Limits.colim
-- Mathlib.GroupTheory.Congruence.Defs
/-- Congruence relations are transitive.  -/
Con.trans : ∀ {M : Type u_1} [inst : Mul M] (c : Con M) {x y z : M}, c x y → c y z → c x z
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.coreOfNat : Lean.Expr →
  ℕ →
    Lean.Meta.Grind.Arith.Linear.LinExpr →
      Lean.Meta.Grind.Arith.Linear.LinExpr → Lean.Meta.Grind.Arith.Linear.IneqCnstrProof
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidHomClass.toOrderAddMonoidHom.eq_1 : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : AddZeroClass α]
  [inst_3 : AddZeroClass β] [inst_4 : FunLike F α β] [inst_5 : OrderHomClass F α β] [inst_6 : AddMonoidHomClass F α β]
  (f : F), ↑f = { toAddMonoidHom := ↑f, monotone' := ⋯ }
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
dist_triangle_right : ∀ {α : Type u} [inst : PseudoMetricSpace α] (x y z : α), dist x y ≤ dist x z + dist y z
-- Mathlib.GroupTheory.GroupAction.Blocks
MulAction.isBlock_iff_smul_eq_smul_or_disjoint : ∀ {G : Type u_1} {X : Type u_2} [inst : SMul G X] {B : Set X},
  MulAction.IsBlock G B ↔ ∀ (g₁ g₂ : G), g₁ • B = g₂ • B ∨ Disjoint (g₁ • B) (g₂ • B)
-- Init.Data.Nat.Lemmas
/-- Dependent variant of `forall_lt_succ_right`.  -/
Nat.forall_lt_succ_right' : ∀ {n : ℕ} {p : (m : ℕ) → m < n + 1 → Prop}, (∀ (m : ℕ) (h : m < n + 1), p m h) ↔ (∀ (m : ℕ) (h : m < n), p m ⋯) ∧ p n ⋯
-- Mathlib.Algebra.Order.Group.PosPart
/-- **Alias** of the reverse direction of `negPart_eq_zero`. -/
negPart_of_nonneg : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddGroup α] {a : α} [AddLeftMono α], 0 ≤ a → a⁻ = 0
-- Mathlib.Algebra.DirectSum.Ring
/-- Multiplication by `one` on the left is the identity  -/
DirectSum.GSemiring.one_mul : ∀ {ι : Type u_1} {A : ι → Type u_2} {inst : AddMonoid ι} {inst_1 : (i : ι) → AddCommMonoid (A i)}
  [self : DirectSum.GSemiring A] (a : GradedMonoid A), 1 * a = a
-- Init.System.Uri
_private.Init.System.Uri.0.System.Uri.UriEscape.uriEscapeAsciiChar.uInt8ToHex : UInt8 → String
-- Mathlib.AlgebraicGeometry.RelativeGluing
AlgebraicGeometry.Scheme.Cover.RelativeGluingData.mk : {S : AlgebraicGeometry.Scheme} →
  {𝒰 : S.OpenCover} →
    [inst : CategoryTheory.Category.{u_2, u_1} 𝒰.I₀] →
      [inst_1 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰] →
        (functor : CategoryTheory.Functor 𝒰.I₀ AlgebraicGeometry.Scheme) →
          (natTrans : functor ⟶ AlgebraicGeometry.Scheme.Cover.functorOfLocallyDirected 𝒰) →
            CategoryTheory.NatTrans.Equifibered natTrans → AlgebraicGeometry.Scheme.Cover.RelativeGluingData 𝒰
-- Mathlib.Order.CompleteBooleanAlgebra
/-- The supremum of `x` and `xᶜ` is at least `⊤`  -/
CompleteBooleanAlgebra.top_le_sup_compl : ∀ {α : Type u_1} [self : CompleteBooleanAlgebra α] (x : α), ⊤ ≤ x ⊔ xᶜ
-- Init.Data.String.Defs
String.Slice.mk.sizeOf_spec : ∀ (str : String) (startInclusive endExclusive : str.Pos)
  (startInclusive_le_endExclusive : startInclusive ≤ endExclusive),
  sizeOf
      { str := str, startInclusive := startInclusive, endExclusive := endExclusive,
        startInclusive_le_endExclusive := startInclusive_le_endExclusive } =
    1 + sizeOf str + sizeOf startInclusive + sizeOf endExclusive + sizeOf startInclusive_le_endExclusive
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Ideal.isHomogeneous_iff_subset_iInter : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : Semiring A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubmonoidClass σ A] (𝒜 : ι → σ) [inst_3 : DecidableEq ι] [inst_4 : AddMonoid ι] [inst_5 : GradedRing 𝒜]
  (I : Ideal A), Ideal.IsHomogeneous 𝒜 I ↔ ↑I ⊆ ⋂ i, ⇑(GradedRing.proj 𝒜 i) ⁻¹' ↑I
-- Mathlib.Analysis.Analytic.Constructions
analyticOnNhd_pi_iff : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {ι : Type u_9} [inst_3 : Fintype ι] {Fm : ι → Type u_10}
  [inst_4 : (i : ι) → NormedAddCommGroup (Fm i)] [inst_5 : (i : ι) → NormedSpace 𝕜 (Fm i)] {f : (i : ι) → E → Fm i}
  {s : Set E}, AnalyticOnNhd 𝕜 (fun x x_1 => f x_1 x) s ↔ ∀ (i : ι), AnalyticOnNhd 𝕜 (f i) s
-- Mathlib.RingTheory.Artinian.Module
IsArtinianRing.instIsSemiprimaryRing : ∀ {R : Type u_1} [inst : Ring R] [IsArtinianRing R], IsSemiprimaryRing R
-- Std.Time.Duration
/-- Adds a `Minute.Offset` to a `Duration`
 -/
Std.Time.Duration.addMinutes : Std.Time.Duration → Std.Time.Minute.Offset → Std.Time.Duration
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.Point.map_baseChange : ∀ {R : Type r} {F : Type u} {K : Type v} {L : Type w} [inst : CommRing R] [inst_1 : Field F] [inst_2 : Field K]
  [inst_3 : Field L] {W' : WeierstrassCurve.Affine R} [inst_4 : DecidableEq F] [inst_5 : DecidableEq K]
  [inst_6 : DecidableEq L] [inst_7 : Algebra R F] [inst_8 : Algebra R K] [inst_9 : Algebra R L] [inst_10 : Algebra F K]
  [inst_11 : IsScalarTower R F K] [inst_12 : Algebra F L] [inst_13 : IsScalarTower R F L] (f : K →ₐ[F] L)
  (P : (W'.baseChange F).Point),
  (WeierstrassCurve.Affine.Point.map f) ((WeierstrassCurve.Affine.Point.baseChange F K) P) =
    (WeierstrassCurve.Affine.Point.baseChange F L) P
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
/-- A variant of `Finset.mul_prod_erase` with the multiplication swapped.  -/
Finset.prod_erase_mul : ∀ {ι : Type u_1} {M : Type u_4} [inst : CommMonoid M] [inst_1 : DecidableEq ι] (s : Finset ι) (f : ι → M) {a : ι},
  a ∈ s → (∏ x ∈ s.erase a, f x) * f a = ∏ x ∈ s, f x
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.mk.sizeOf_spec : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {P : CategoryTheory.MorphismProperty T}
  {Q : CategoryTheory.MorphismProperty A} {W : CategoryTheory.MorphismProperty B} [inst_3 : SizeOf A]
  [inst_4 : SizeOf B] [inst_5 : SizeOf T] [inst_6 : ⦃X Y : T⦄ → (x : X ⟶ Y) → SizeOf (P x)]
  [inst_7 : ⦃X Y : A⦄ → (x : X ⟶ Y) → SizeOf (Q x)] [inst_8 : ⦃X Y : B⦄ → (x : X ⟶ Y) → SizeOf (W x)]
  (toComma : CategoryTheory.Comma L R) (prop : P toComma.hom),
  sizeOf { toComma := toComma, prop := prop } = 1 + sizeOf toComma + sizeOf prop
-- Init.Control.Lawful.Instances
ReaderT.instLawfulMonad : ∀ {m : Type u_1 → Type u_2} {ρ : Type u_1} [inst : Monad m] [LawfulMonad m], LawfulMonad (ReaderT ρ m)
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.hom_ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.SimplicialObject C} (f g : X ⟶ Y),
  (∀ (n : SimplexCategoryᵒᵖ), f.app n = g.app n) → f = g
-- Init.Data.Iterators.Internal.LawfulMonadLiftFunction
Std.Internal.LawfulMonadLiftFunction.lift_map : ∀ {m : Type u → Type v} {n : Type u → Type w} [inst : Monad m] [inst_1 : Monad n] {lift : ⦃α : Type u⦄ → m α → n α}
  {α β : Type u} [LawfulMonad m] [LawfulMonad n] [Std.Internal.LawfulMonadLiftFunction lift] (f : α → β) (ma : m α),
  lift (f <$> ma) = f <$> lift ma
-- Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
HomologicalComplex.homology.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) [inst_2 : K.HasHomology i],
  K.homology i = (K.sc i).homology
-- Mathlib.RingTheory.Derivation.MapCoeffs
/-- The `R`-derivation from `A[X]` to `M[X]` which applies the derivative to each
of the coefficients.
 -/
Derivation.mapCoeffs : {R : Type u_1} →
  {A : Type u_2} →
    {M : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : CommRing A] →
          [inst_2 : Algebra R A] →
            [inst_3 : AddCommGroup M] →
              [inst_4 : Module A M] →
                [inst_5 : Module R M] → Derivation R A M → Derivation R (Polynomial A) (PolynomialModule A M)
-- Batteries.Recycling.RBTree.Basic
RBTree.RBSet.ModifyWF.mk : ∀ {α : Type u_1} {cmp : α → α → Ordering} {t : RBTree.RBSet α cmp} {cut : α → Ordering} {f : α → α},
  RBTree.RBNode.WF cmp (RBTree.RBNode.modify cut f ↑t) → t.ModifyWF cut f
-- Mathlib.Data.Finite.Prod
Finite.prod_right : ∀ {β : Type u_2} (α : Type u_3) [Finite (α × β)] [Nonempty α], Finite β
-- Mathlib.Order.CountableSupClosed
countableInfClosed_countableInfClosure : ∀ {α : Type u_2} {s : Set α} [inst : Preorder α], CountableInfClosed (countableInfClosure s)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.maxKeyD.congr_simp : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] (t t_1 : Std.ExtTreeMap α β cmp),
  t = t_1 → ∀ (fallback fallback_1 : α), fallback = fallback_1 → t.maxKeyD fallback = t_1.maxKeyD fallback_1
-- LeanSearchClient.Syntax
LeanSearchClient.leanSearchCache : IO.Ref (Std.HashMap (String × ℕ) (Array Lean.Json))
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.coe_add : ∀ {Γ : Type u_1} {R : Type u_3} {α : Type u_5} [inst : PartialOrder Γ] [inst_1 : AddCommMonoid R]
  (s t : HahnSeries.SummableFamily Γ R α), ⇑(s + t) = ⇑s + ⇑t
-- Lean.Parser.Extension
Lean.Parser.ParserExtension.State.tokens : Lean.Parser.ParserExtension.State → Lean.Parser.TokenTable
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw.keysArray_eq_toArray_keys_toListModel : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β},
  m.keysArray = (Std.Internal.List.keys (Std.DHashMap.Internal.toListModel m.buckets)).toArray
-- Mathlib.Data.Finset.Card
/-- If `a ∈ s` is known, see also `Finset.card_insert_of_mem` and `Finset.card_insert_of_notMem`.
 -/
Finset.card_insert_eq_ite : ∀ {α : Type u_1} {s : Finset α} {a : α} [inst : DecidableEq α], (insert a s).card = if a ∈ s then s.card else s.card + 1
-- Mathlib.AlgebraicGeometry.Cover.MorphismProperty
AlgebraicGeometry.Scheme.coverOfIsIso_X : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [inst : P.ContainsIdentities] [inst_1 : P.RespectsIso]
  {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst_2 : CategoryTheory.IsIso f] (x : PUnit.{v + 1}),
  (AlgebraicGeometry.Scheme.coverOfIsIso f).X x = X
-- Mathlib.Data.Sign.Defs
sign_eq_zero_iff : ∀ {α : Type u_1} [inst : Zero α] [inst_1 : LinearOrder α] {a : α}, SignType.sign a = 0 ↔ a = 0
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Ordinal.lift_iSup_add_one_lt_of_lt_cof : ∀ {β : Type v} {f : β → Ordinal.{u}} {a : Ordinal.{u}},
  Cardinal.lift.{u, v} (Cardinal.mk β) < (Ordinal.lift.{v, u} a).cof → (∀ (i : β), f i < a) → ⨆ i, f i + 1 < a
-- Lean.Meta.Tactic.Grind.AC.Seq
_private.Lean.Meta.Tactic.Grind.AC.Seq.0.Lean.Grind.AC.«term_::_» : Lean.TrailingParserDescr
-- Mathlib.RingTheory.TensorProduct.Basic
Algebra.TensorProduct.ext_iff : ∀ {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} {C : Type uC} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : Semiring B] [inst_4 : Algebra R B] [inst_5 : Semiring C] [inst_6 : Algebra R C]
  [inst_7 : CommSemiring S] [inst_8 : Algebra S A] [inst_9 : Algebra R S] [inst_10 : Algebra S C]
  [inst_11 : IsScalarTower R S A] [inst_12 : IsScalarTower R S C] {f g : TensorProduct R A B →ₐ[S] C},
  f = g ↔
    f.comp Algebra.TensorProduct.includeLeft = g.comp Algebra.TensorProduct.includeLeft ∧
      (AlgHom.restrictScalars R f).comp Algebra.TensorProduct.includeRight =
        (AlgHom.restrictScalars R g).comp Algebra.TensorProduct.includeRight
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Sigma.map'_eq : ∀ {β : Type w} {α : Type w₂} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f : α → C} {g : β → C}
  [inst_1 : CategoryTheory.Limits.HasCoproduct f] [inst_2 : CategoryTheory.Limits.HasCoproduct g] {p p' : α → β}
  {q : (a : α) → f a ⟶ g (p a)} {q' : (a : α) → f a ⟶ g (p' a)} (hp : p = p'),
  (∀ (a : α), CategoryTheory.CategoryStruct.comp (q a) (CategoryTheory.eqToHom ⋯) = q' a) →
    CategoryTheory.Limits.Sigma.map' p q = CategoryTheory.Limits.Sigma.map' p' q'
-- Batteries.Data.MLList.Basic
_private.Batteries.Data.MLList.Basic.0.MLList.instNonemptySpec : ∀ {m : Type u_1 → Type u_1}, Nonempty (MLList.Spec✝ m)
-- Init.Data.List.Erase
List.erase_append_right : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a : α} {l₁ : List α} (l₂ : List α),
  a ∉ l₁ → (l₁ ++ l₂).erase a = l₁ ++ l₂.erase a
-- Mathlib.Analysis.Normed.Order.Hom.Basic
/-- Constructs a `NormedCommGroup` structure from a `GroupNormClass` on a `CommGroup`.  -/
GroupNormClass.toNormedCommGroup : {F : Type u_1} →
  {α : Type u_2} → [inst : FunLike F α ℝ] → [inst_1 : CommGroup α] → [GroupNormClass F α ℝ] → F → NormedCommGroup α
-- Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
RootPairing.coroot'In.congr_simp : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (S : Type u_6)
  [inst_5 : CommRing S] [inst_6 : Algebra S R] [inst_7 : Module S M] [inst_8 : IsScalarTower S R M]
  [inst_9 : FaithfulSMul S R] [inst_10 : P.IsValuedIn S] (i i_1 : ι), i = i_1 → P.coroot'In S i = P.coroot'In S i_1
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.size_erase_le : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k : α}, (m.erase k).size ≤ m.size
-- Mathlib.Algebra.Group.InjSurj
Function.Injective.addLeftCancelSemigroup.eq_1 : ∀ {M₁ : Type u_1} {M₂ : Type u_2} [inst : Add M₁] [inst_1 : AddLeftCancelSemigroup M₂] (f : M₁ → M₂)
  (hf : Function.Injective f) (mul : ∀ (x y : M₁), f (x + y) = f x + f y),
  Function.Injective.addLeftCancelSemigroup f hf mul =
    { toAddSemigroup := Function.Injective.addSemigroup f hf mul, toIsLeftCancelAdd := ⋯ }
-- Mathlib.LinearAlgebra.Matrix.ToLin
Matrix.toLinAlgEquiv_one : ∀ {R : Type u_1} [inst : CommSemiring R] {n : Type u_4} [inst_1 : Fintype n] [inst_2 : DecidableEq n] {M₁ : Type u_5}
  [inst_3 : AddCommMonoid M₁] [inst_4 : Module R M₁] (v₁ : Module.Basis n R M₁),
  (Matrix.toLinAlgEquiv v₁) 1 = LinearMap.id
-- Std.Sync.CancellationToken
Std.instBEqCancellationReason.beq : Std.CancellationReason → Std.CancellationReason → Bool
-- Mathlib.Analysis.LocallyConvex.Basic
/-- A balanced set absorbs itself.  -/
Balanced.absorbs_self : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : NormedDivisionRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  {s : Set E}, Balanced 𝕜 s → Absorbs 𝕜 s s
-- Mathlib.CategoryTheory.Limits.Final
/-- If `Over j ⥤ J` is initial, restricting a limit cone to the diagram above `j`,
preserves the limit.  -/
CategoryTheory.Limits.IsLimit.overPost : {J : Type u_1} →
  {C : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} J] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} C] →
        {D : CategoryTheory.Functor J C} →
          {c : CategoryTheory.Limits.Cone D} →
            CategoryTheory.Limits.IsLimit c →
              (j : J) → [(CategoryTheory.Over.forget j).Initial] → CategoryTheory.Limits.IsLimit (c.overPost j)
-- Std.Data.HashSet.Basic
/-- Check if any element satisfies the predicate, short-circuiting if a predicate succeeds.  -/
Std.HashSet.any : {α : Type u} → {x : BEq α} → {x_1 : Hashable α} → Std.HashSet α → (α → Bool) → Bool
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.d₂₁_single_one_snd : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u, u, u} k G} (g : G) (a : ↑A),
  ((CategoryTheory.ConcreteCategory.hom (groupHomology.d₂₁ A)) fun₀ | (g, 1) => a) = fun₀ | 1 => (A.ρ g⁻¹) a
-- Mathlib.RingTheory.PowerSeries.Substitution
_private.Mathlib.RingTheory.PowerSeries.Substitution.0.PowerSeries.termX₀ : Lean.ParserDescr
-- Mathlib.Data.Real.ConjExponents
ENNReal.coe_conjExponent : ∀ {p : NNReal}, 1 < p → ↑p.conjExponent = (↑p).conjExponent
-- Mathlib.Algebra.GroupWithZero.Range
/-- The inclusion of the subgroup with zero generated by the range of a monoid with zero
hom `f : A →*₀ B` into the codomain `B`.  -/
MonoidWithZeroHom.ValueGroup₀.embedding : {A : Type u_1} →
  {B : Type u_2} → [inst : MonoidWithZero A] → [inst_1 : GroupWithZero B] → {f : A →*₀ B} → f.ValueGroup₀ →*₀ B
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.toOpposite_symm_apply : ∀ (R : Type u_4) [inst : NonUnitalCommSemiring R] (r : Rᵐᵒᵖ), (RingEquiv.toOpposite R).symm r = MulOpposite.unop r
-- Init.System.IO
IO.FS.Metadata.mk.inj : ∀ {accessed modified : IO.FS.SystemTime} {byteSize : UInt64} {type : IO.FS.FileType} {numLinks : UInt64}
  {accessed_1 modified_1 : IO.FS.SystemTime} {byteSize_1 : UInt64} {type_1 : IO.FS.FileType} {numLinks_1 : UInt64},
  { accessed := accessed, modified := modified, byteSize := byteSize, type := type, numLinks := numLinks } =
      { accessed := accessed_1, modified := modified_1, byteSize := byteSize_1, type := type_1,
        numLinks := numLinks_1 } →
    accessed = accessed_1 ∧ modified = modified_1 ∧ byteSize = byteSize_1 ∧ type = type_1 ∧ numLinks = numLinks_1
-- Mathlib.Topology.UniformSpace.Defs
SetRel.mem_filter_prod_comm : ∀ {α : Type ua} (R : SetRel α α) {f g : Filter α} [R.IsSymm], R ∈ f ×ˢ g ↔ R ∈ g ×ˢ f
-- Mathlib.RingTheory.MvPolynomial.Homogeneous
MvPolynomial.homogeneousSubmodule_one_eq_span_X : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R],
  MvPolynomial.homogeneousSubmodule σ R 1 = Submodule.span R (Set.range MvPolynomial.X)
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.divByMonic_add_X_sub_C_mul_derivative_divByMonic_eq_derivative : ∀ {K : Type u_1} [inst : CommRing K] (f : Polynomial K) (a : K),
  f /ₘ (Polynomial.X - Polynomial.C a) +
      (Polynomial.X - Polynomial.C a) * Polynomial.derivative (f /ₘ (Polynomial.X - Polynomial.C a)) =
    Polynomial.derivative f
-- Mathlib.Geometry.Euclidean.Triangle
/-- The **sum of the angles of a triangle** (possibly degenerate, where two
given vertices are distinct), angle-at-point.  -/
EuclideanGeometry.angle_add_angle_add_angle_eq_pi : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {p₁ p₂ : P} (p₃ : P),
  p₂ ≠ p₁ →
    EuclideanGeometry.angle p₁ p₂ p₃ + EuclideanGeometry.angle p₂ p₃ p₁ + EuclideanGeometry.angle p₃ p₁ p₂ = Real.pi
-- Mathlib.LinearAlgebra.Span.TensorProduct
Submodule.surjective_tensorToSpan : ∀ {R : Type u_1} (A : Type u_2) {M : Type u_3} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Algebra R A]
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module A M] [inst_6 : IsScalarTower R A M]
  (p : Submodule R M), Function.Surjective ⇑(Submodule.tensorToSpan A p)
-- Mathlib.Order.Monotone.Basic
StrictMono.le_iff_le : ∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : Preorder β] {f : α → β},
  StrictMono f → ∀ {a b : α}, f a ≤ f b ↔ a ≤ b
-- Mathlib.CategoryTheory.Shift.Quotient
CategoryTheory.Quotient.LiftCommShift.iso_inv_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  (F : CategoryTheory.Functor C D) (r : HomRel C) {A : Type w} [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift C A] [inst_4 : CategoryTheory.HasShift D A] [inst_5 : r.IsCompatibleWithShift A]
  [inst_6 : F.CommShift A] (hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂) (a : A) (X : C),
  (CategoryTheory.Quotient.LiftCommShift.iso F r hF a).inv.app ((CategoryTheory.Quotient.functor r).obj X) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso F a).inv.app X)
      ((CategoryTheory.Quotient.lift r F hF).map
        ((CategoryTheory.Functor.commShiftIso (CategoryTheory.Quotient.functor r) a).hom.app X))
-- Mathlib.Topology.ClusterPt
MapClusterPt.mono : ∀ {X : Type u} [inst : TopologicalSpace X] {α : Type u_1} {F : Filter α} {u : α → X} {x : X} {G : Filter α},
  MapClusterPt x F u → F ≤ G → MapClusterPt x G u
-- Mathlib.CategoryTheory.Limits.Bicones
CategoryTheory.Bicone.left : {J : Type u₁} → CategoryTheory.Bicone J