mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Polynomial.Derivation
/-- `Polynomial.derivative` as a derivation.  -/
Polynomial.derivative' : {R : Type u_1} → [inst : CommSemiring R] → Derivation R (Polynomial R) (Polynomial R)
-- Mathlib.Topology.Convenient.ContinuousMapGeneratedBy
Topology.ContinuousGeneratedBy.comp : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)] {Y : Type v} [inst_1 : TopologicalSpace Y]
  {Z : Type v'} [inst_2 : TopologicalSpace Z] {g : Y → Z},
  Topology.ContinuousGeneratedBy X g →
    ∀ {T : Type u_1} [inst_3 : TopologicalSpace T] {f : T → Y},
      Topology.ContinuousGeneratedBy X f → Topology.ContinuousGeneratedBy X (g ∘ f)
-- Mathlib.GroupTheory.GroupAction.Hom
MulActionHom.instAddCommMonoid : {M : Type u_2} →
  {N : Type u_3} →
    {X : Type u_4} →
      {Y : Type u_5} →
        {σ : M → N} →
          [inst : SMul M X] → [inst_1 : AddCommMonoid Y] → [inst_2 : DistribSMul N Y] → AddCommMonoid (X →ₑ[σ] Y)
-- Mathlib.Probability.Kernel.Composition.MeasureCompProd
MeasureTheory.Measure.AbsolutelyContinuous.compProd : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ ν : MeasureTheory.Measure α}
  {κ η : ProbabilityTheory.Kernel α β} [MeasureTheory.SFinite ν] [ProbabilityTheory.IsSFiniteKernel η],
  μ.AbsolutelyContinuous ν →
    (∀ᵐ (a : α) ∂μ, (κ a).AbsolutelyContinuous (η a)) → (μ.compProd κ).AbsolutelyContinuous (ν.compProd η)
-- Mathlib.Data.Ordmap.Invariants
Ordnode.dual_node3L : ∀ {α : Type u_1} (l : Ordnode α) (x : α) (m : Ordnode α) (y : α) (r : Ordnode α),
  (l.node3L x m y r).dual = r.dual.node3R y m.dual x l.dual
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.naturality_naturality_hom_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.Pseudofunctor B C} (α : F ⟶ G) {a b : B} {f g : a ⟶ b} (η : f ≅ g) {Z : F.obj a ⟶ G.obj b}
  (h : CategoryTheory.CategoryStruct.comp (α.app a) (G.map g) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (α.naturality g).hom h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.map₂ η.inv) (α.app b))
      (CategoryTheory.CategoryStruct.comp (α.naturality f).hom
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (α.app a) (G.map₂ η.hom)) h))
-- Aesop.Tree.TreeM
Aesop.TreeM.State.mk.inj : ∀ {tree tree_1 : Aesop.Tree}, { tree := tree } = { tree := tree_1 } → tree = tree_1
-- Mathlib.LinearAlgebra.RootSystem.Base
RootPairing.Base.toWeightBasis_apply : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [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} (b : P.Base)
  [inst_5 : P.IsRootSystem] (i : ↥b.support), b.toWeightBasis i = P.root ↑i
-- Mathlib.Analysis.Convolution
Continuous.convolution_integrand_fst : ∀ {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup E'] [inst_2 : NormedAddCommGroup F] {f : G → E} {g : G → E'}
  [inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 E'] [inst_6 : NormedSpace 𝕜 F]
  (L : E →L[𝕜] E' →L[𝕜] F) [inst_7 : AddGroup G] [inst_8 : TopologicalSpace G] [ContinuousSub G],
  Continuous g → ∀ (t : G), Continuous fun x => (L (f t)) (g (x - t))
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
/-- The coequalizer of a reflexive pair can be promoted to the colimit of a diagram out of the
walking reflexive pair  -/
CategoryTheory.Limits.colimitOfIsReflexivePairIsoCoequalizer : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A B : C} →
      {f g : A ⟶ B} →
        [inst_1 : CategoryTheory.IsReflexivePair f g] →
          [h : CategoryTheory.Limits.HasCoequalizer f g] →
            CategoryTheory.Limits.colimit (CategoryTheory.Limits.ofIsReflexivePair f g) ≅
              CategoryTheory.Limits.coequalizer f g
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.preAleph_le_of_strictMono : ∀ {f : Ordinal.{u_1} → Cardinal.{u_1}}, StrictMono f → ∀ (o : Ordinal.{u_1}), Cardinal.preAleph o ≤ f o
-- Init.Grind.Attr
/-- The `cases` modifier marks inductively-defined predicates as suitable for case splitting.
 -/
Lean.Parser.Attr.grindCases : Lean.ParserDescr
-- Lean.Meta.FunInfo
_private.Lean.Meta.FunInfo.0.Lean.Meta.getFunInfoAux : Lean.Expr → Option ℕ → Lean.MetaM Lean.Meta.FunInfo
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.coe_iSup_of_directed : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : StarRing A]
  [inst_3 : Module R A] {ι : Type u_1} [inst_4 : StarRing R] [inst_5 : IsScalarTower R A A]
  [inst_6 : SMulCommClass R A A] [inst_7 : StarModule R A] [Nonempty ι] {S : ι → NonUnitalStarSubalgebra R A},
  Directed (fun x1 x2 => x1 ≤ x2) S → ↑(iSup S) = ⋃ i, ↑(S i)
-- Mathlib.GroupTheory.DoubleCoset
DoubleCoset.mk_eq_of_doubleCoset_eq : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G} {a b : G},
  DoubleCoset.doubleCoset a ↑H ↑K = DoubleCoset.doubleCoset b ↑H ↑K → DoubleCoset.mk H K a = DoubleCoset.mk H K b
-- Mathlib.Analysis.Normed.Group.Subgroup
AddSubgroup.normedAddCommGroup.eq_1 : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {s : AddSubgroup E},
  AddSubgroup.normedAddCommGroup =
    { toNorm := AddSubgroup.seminormedAddCommGroup.toNorm, toAddCommGroup := s.toAddCommGroup,
      toMetricSpace := Subtype.metricSpace, dist_eq := ⋯ }
-- Mathlib.Data.Fintype.Prod
/-- The number of strictly ordered pairs `(a, b)` in `α` is `(Fintype.card α).choose 2`.  -/
Fintype.card_product_filter_lt : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : LinearOrder α], {x | x.1 < x.2}.card = (Fintype.card α).choose 2
-- Mathlib.Algebra.Lie.Weights.Killing
LieModule.Weight.ker.congr_simp : ∀ {R : Type u_2} {L : Type u_3} {M : Type u_4} [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] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] [inst_8 : LieModule.LinearWeights R L M] {χ χ_1 : LieModule.Weight R L M},
  χ = χ_1 → LieModule.Weight.ker = LieModule.Weight.ker
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.String.Legacy.Iterator.nextn.eq_1 : ∀ (x : String.Legacy.Iterator), x.nextn 0 = x
-- Mathlib.Combinatorics.SetFamily.Shadow
Finset.shadow_singleton : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α), {{a}}.shadow = {∅}
-- Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
SimpleGraph.Walk.getVert_lt_length_takeUntil_ne : ∀ {V : Type u} {G : SimpleGraph V} {v w u : V} [inst : DecidableEq V] {n : ℕ} {p : G.Walk v w} (h : u ∈ p.support),
  n < (p.takeUntil u h).length → p.getVert n ≠ u
-- Std.Internal.Do.Order.Basic
Lean.Order.left_le_join : ∀ {α : Type u} [inst : Lean.Order.CompleteLattice α] (x y : α), Lean.Order.PartialOrder.rel x (Lean.Order.join x y)
-- Std.Time.Zoned.ZoneRules
Std.Time.TimeZone.instReprUTLocal : Repr Std.Time.TimeZone.UTLocal
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.whiskerLeft_obj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {n m : ℕ} (F : CategoryTheory.ComposableArrows C m)
  (Φ : CategoryTheory.Functor (Fin (n + 1)) (Fin (m + 1))) (X : Fin (n + 1)), (F.whiskerLeft Φ).obj X = F.obj (Φ.obj X)
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mapRightComp_hom_app_right : ∀ {B : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} B] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T)
  {R₁ R₂ L₃ : CategoryTheory.Functor B T} (r : R₂ ⟶ R₁) (r' : L₃ ⟶ R₂) (X : CategoryTheory.Comma L L₃),
  ((CategoryTheory.Comma.mapRightComp L r r').hom.app X).right = CategoryTheory.CategoryStruct.id X.right
-- Mathlib.Analysis.Fourier.FourierTransform
Real.instFourierTransform : {V : Type u_1} →
  {E : Type u_3} →
    [inst : NormedAddCommGroup E] →
      [NormedSpace ℂ E] →
        [inst : NormedAddCommGroup V] →
          [inst_1 : InnerProductSpace ℝ V] →
            [inst_2 : MeasurableSpace V] → [BorelSpace V] → [FiniteDimensional ℝ V] → FourierTransform (V → E) (V → E)
-- Mathlib.Analysis.Complex.Basic
Complex.continuous_normSq : Continuous ⇑Complex.normSq
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.checkColEq.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback
CategoryTheory.MonoidalCategory.Limits.pushout.associator_inv_naturality_right_condition_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasPushouts C] {A B X Y Z W : C} {f : A ⟶ B} {g : X ⟶ Y}
  {h : CategoryTheory.MonoidalCategoryStruct.tensorObj Z W ⟶ A} {Z_1 : C}
  (h_1 :
    CategoryTheory.Limits.pushout (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X)
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A g) ⟶
      Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z (CategoryTheory.MonoidalCategoryStruct.whiskerLeft W g))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Z W Y).inv
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight h Y)
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Limits.pushout.inr (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X)
              (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A g))
            h_1))) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Z W X).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp h f) X)
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Limits.pushout.inl (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X)
            (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A g))
          h_1))
-- Mathlib.Analysis.CStarAlgebra.Unitary.Maps
Unitary.mulRight.congr_simp : ∀ (R : Type u_1) {A : Type u_2} [inst : NormedRing A] [inst_1 : StarRing A] [inst_2 : CStarRing A] [inst_3 : Ring R]
  [inst_4 : Module R A] [inst_5 : IsScalarTower R A A] (u u_1 : ↥(unitary A)),
  u = u_1 → Unitary.mulRight R u = Unitary.mulRight R u_1
-- Mathlib.Tactic.Lift
/-- Enable automatic handling of product types in `CanLift`.  -/
Prod.instCanLift : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {coeβα : β → α} {condβα : α → Prop} {coeδγ : δ → γ}
  {condδγ : γ → Prop} [CanLift α β coeβα condβα] [CanLift γ δ coeδγ condδγ],
  CanLift (α × γ) (β × δ) (Prod.map coeβα coeδγ) fun x => condβα x.1 ∧ condδγ x.2
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.hom_ext_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {A B : CategoryTheory.Grp C} {f g : A ⟶ B}, f = g ↔ f.hom.hom = g.hom.hom
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
IsPrimitiveRoot.isRoot_of_dvd : ∀ {R : Type u_4} [inst : CommRing R] {n n' : ℕ} {ζ : R}, IsPrimitiveRoot ζ n → n ∣ n' → (Polynomial.X ^ n' - 1).IsRoot ζ
-- Aesop.Index
Aesop.Index : Type → Type
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.LeanDiagnosticTag.noConfusionType : Sort v✝ → Lean.Lsp.LeanDiagnosticTag → Lean.Lsp.LeanDiagnosticTag → Sort v✝
-- Mathlib.Algebra.Homology.Embedding.AreComplementary
ComplexShape.Embedding.AreComplementary.exists_i₂ : ∀ {ι : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} {c : ComplexShape ι} {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  {e₁ : c₁.Embedding c} {e₂ : c₂.Embedding c},
  e₁.AreComplementary e₂ → ∀ (i : ι), (∀ (i₁ : ι₁), e₁.f i₁ ≠ i) → ∃ i₂, i = e₂.f i₂
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.mk.injEq : ∀ {α : Type u} [inst : MeasurableSpace α] {β : Type v} (toFun : α → β)
  (measurableSet_fiber' : ∀ (x : β), MeasurableSet (toFun ⁻¹' {x})) (finite_range' : (Set.range toFun).Finite)
  (toFun_1 : α → β) (measurableSet_fiber'_1 : ∀ (x : β), MeasurableSet (toFun_1 ⁻¹' {x}))
  (finite_range'_1 : (Set.range toFun_1).Finite),
  ({ toFun := toFun, measurableSet_fiber' := measurableSet_fiber', finite_range' := finite_range' } =
      { toFun := toFun_1, measurableSet_fiber' := measurableSet_fiber'_1, finite_range' := finite_range'_1 }) =
    (toFun = toFun_1)
-- Mathlib.Tactic.Polynomial.Core
/-- `polynomial_infer_base` marks a procedure used by the `polynomial` tactic to infer
the base ring of polynomial-like types.  -/
Mathlib.Tactic.Polynomial.PolyInferBaseAttr : Lean.ParserDescr
-- Mathlib.RingTheory.DedekindDomain.PID
/-- An invertible fractional ideal of a commutative ring with finitely many maximal ideals is principal.

https://math.stackexchange.com/a/95857  -/
FractionalIdeal.isPrincipal.of_finite_maximals_of_inv : ∀ {R : Type u_1} [inst : CommRing R] {A : Type u_2} [inst_1 : CommRing A] [inst_2 : Algebra R A] {S : Submonoid R}
  [IsLocalization S A],
  S ≤ nonZeroDivisors R → {I | I.IsMaximal}.Finite → ∀ (I I' : FractionalIdeal S A), I * I' = 1 → (↑I).IsPrincipal
-- Mathlib.Algebra.Homology.BifunctorShift
CategoryTheory.Functor.commShiftIso_map₂CochainComplex_flip_hom_app : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [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} D]
  [inst_3 : CategoryTheory.Preadditive C₁] [inst_4 : CategoryTheory.Preadditive C₂]
  [inst_5 : CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
  [inst_6 : F.Additive] [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).Additive]
  [inst_8 : ∀ (K₁ : CochainComplex C₁ ℤ) (K₂ : CochainComplex C₂ ℤ), K₁.HasMapBifunctor K₂ F] (K₁ : CochainComplex C₁ ℤ)
  (K₂ : CochainComplex C₂ ℤ) (n : ℤ),
  (CategoryTheory.Functor.commShiftIso (F.map₂CochainComplex.flip.obj K₂) n).hom.app K₁ =
    (K₁.mapBifunctorShift₁Iso K₂ F n).hom
-- Mathlib.CategoryTheory.Shift.CommShiftTwo
/-- A bifunctor `G : C₁ ⥤ C₂ ⥤ D` commutes with the shifts by `ℤ` if all functors
`G.obj X₁` and `G.flip X₂` are equipped with `Functor.CommShift` structures, in a way
that is natural in `X₁` and `X₂`, and that these isomorphisms for the shift by `p`
on the first variable and the shift by `q` on the second variable commute up
to the sign `(-1) ^ (p * q)`.  -/
CategoryTheory.Functor.CommShift₂Int : {C₁ : Type u_1} →
  {C₂ : Type u_3} →
    {D : Type u_5} →
      [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
        [inst_1 : CategoryTheory.Category.{v_3, u_3} C₂] →
          [inst_2 : CategoryTheory.Category.{v_5, u_5} D] →
            [CategoryTheory.HasShift C₁ ℤ] →
              [CategoryTheory.HasShift C₂ ℤ] →
                [inst_5 : CategoryTheory.HasShift D ℤ] →
                  [inst_6 : CategoryTheory.Preadditive D] →
                    [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] →
                      CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D) → Type (max (max u_1 u_3) v_5)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.isSome_minKey?_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β}, (t.insertIfNew k v).minKey?.isSome = true
-- Lean.Elab.InfoTree.Types
Lean.Elab.UserWidgetInfo.toWidgetInstance : Lean.Elab.UserWidgetInfo → Lean.Widget.WidgetInstance
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.instModule : {R : Type u_1} →
  {S : Type u_2} →
    {a b : R} → [inst : Semiring S] → [inst_1 : AddCommMonoid R] → [Module S R] → Module S (QuadraticAlgebra R a b)
-- Mathlib.Logic.Equiv.Defs
/-- The `Sort` of proofs of a false proposition is equivalent to `PEmpty`.  -/
Equiv.propEquivPEmpty : {p : Prop} → ¬p → p ≃ PEmpty.{u_1}
-- Init.Data.Int.DivMod.Lemmas
Int.toNat_emod : ∀ {x y : ℤ}, 0 ≤ x → 0 ≤ y → (x % y).toNat = x.toNat % y.toNat
-- Mathlib.Analysis.Normed.Group.Continuity
ContinuousAt.nnnorm : ∀ {α : Type u_1} {E : Type u_4} [inst : SeminormedAddGroup E] [inst_1 : TopologicalSpace α] {f : α → E} {a : α},
  ContinuousAt f a → ContinuousAt (fun x => ‖f x‖₊) a
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
/-- The tensor product over an empty index type `ι` is isomorphic to the base ring.  -/
PiTensorProduct.isEmptyEquiv : (ι : Type u_1) →
  {R : Type u_4} →
    [inst : CommSemiring R] →
      {s : ι → Type u_7} →
        [inst_1 : (i : ι) → AddCommMonoid (s i)] →
          [inst_2 : (i : ι) → Module R (s i)] → [IsEmpty ι] → (PiTensorProduct R fun i => s i) ≃ₗ[R] R
-- Mathlib.GroupTheory.FreeGroup.Basic
/-- The isomorphism between the free additive group on a unique type and the integers.  -/
FreeAddGroup.addEquivIntOfUnique : {α : Type u} → [Unique α] → FreeAddGroup α ≃+ ℤ
-- Mathlib.GroupTheory.OrderOfElement
IsOfFinOrder.eq_one : ∀ {G : Type u_1} [inst : Semiring G] [inst_1 : LinearOrder G] [IsStrictOrderedRing G] {a : G},
  0 ≤ a → IsOfFinOrder a → a = 1
-- Mathlib.Topology.Algebra.Group.Basic
Inseparable.neg : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Neg G] [ContinuousNeg G] {x y : G},
  Inseparable x y → Inseparable (-x) (-y)
-- Mathlib.RepresentationTheory.Continuous.Basic
ContIntertwiningMap.mk.injEq : ∀ {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Monoid G] [inst_1 : Ring R]
  [inst_2 : AddCommGroup V] [inst_3 : TopologicalSpace V] [inst_4 : IsTopologicalAddGroup V] [inst_5 : Module R V]
  [inst_6 : AddCommGroup W] [inst_7 : TopologicalSpace W] [inst_8 : IsTopologicalAddGroup W] [inst_9 : Module R W]
  {π₁ : ContRepresentation R G V} {π₂ : ContRepresentation R G W} (toContinuousLinearMap : V →L[R] W)
  (isIntertwining' : ∀ (g : G), toContinuousLinearMap ∘SL π₁ g = π₂ g ∘SL toContinuousLinearMap)
  (toContinuousLinearMap_1 : V →L[R] W)
  (isIntertwining'_1 : ∀ (g : G), toContinuousLinearMap_1 ∘SL π₁ g = π₂ g ∘SL toContinuousLinearMap_1),
  ({ toContinuousLinearMap := toContinuousLinearMap, isIntertwining' := isIntertwining' } =
      { toContinuousLinearMap := toContinuousLinearMap_1, isIntertwining' := isIntertwining'_1 }) =
    (toContinuousLinearMap = toContinuousLinearMap_1)
-- Mathlib.Topology.Order.LeftRightNhds
/-- A set is a neighborhood of `a` within `(a, +∞)` if and only if it contains an interval `(a, u)`
with `a < u < u'`, provided `a` is not a top element.  -/
mem_nhdsGT_iff_exists_Ioo_subset' : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] {a u' : α} {s : Set α},
  a < u' → (s ∈ nhdsWithin a (Set.Ioi a) ↔ ∃ u ∈ Set.Ioi a, Set.Ioo a u ⊆ s)
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.image_sub_const_Icc : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] (a b c : α),
  (fun x => x - a) '' Set.Icc b c = Set.Icc (b - a) (c - a)
-- Mathlib.Order.Bounds.Basic
isGLB_Icc : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, b ≤ a → IsGLB (Set.Icc b a) b
-- Lean.Data.FuzzyMatching
Lean.FuzzyMatching.CharRole.noConfusionType : Sort v✝ → Lean.FuzzyMatching.CharRole → Lean.FuzzyMatching.CharRole → Sort v✝
-- Mathlib.Order.Bounds.Basic
/-- If `s` has a least upper bound, then it is bounded above.  -/
IsLUB.bddAbove : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α} {a : α}, IsLUB s a → BddAbove s
-- Init.Data.Range.Polymorphic.Iterators
Std.Rci.Internal.iter.eq_1 : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] (r : Std.Rci α),
  Std.Rci.Internal.iter r = { internalState := { next := some r.lower } }
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
UniformFun.eq_1 : ∀ (α : Type u_1) (β : Type u_2), UniformFun α β = (α → β)
-- Lean.PrettyPrinter.Delaborator.Builtins
Lean.PrettyPrinter.Delaborator.delabMData : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.comp_h₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {X Y Z : CategoryTheory.PreZeroHypercover S}
  (f : X.Hom Y) (g : Y.Hom Z) (i : X.I₀),
  (CategoryTheory.CategoryStruct.comp f g).h₀ i = CategoryTheory.CategoryStruct.comp (f.h₀ i) (g.h₀ (f.s₀ i))
-- Mathlib.CategoryTheory.Sites.Closed
/-- A sieve is closed for the Grothendieck topology if it contains every arrow it covers.
In the case of the usual topology on a topological space, this means that the open cover contains
every open set which it covers.

Note this has no relation to a closed subset of a topological space.
 -/
CategoryTheory.GrothendieckTopology.IsClosed : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.GrothendieckTopology C → {X : C} → CategoryTheory.Sieve X → Prop
-- Mathlib.RingTheory.DividedPowers.RatAlgebra
DividedPowers.OfInvertibleFactorial.dpow_mem : ∀ {A : Type u_1} [inst : CommSemiring A] {I : Ideal A} [inst_1 : DecidablePred fun x => x ∈ I] {m : ℕ},
  m ≠ 0 → ∀ {x : A}, x ∈ I → DividedPowers.OfInvertibleFactorial.dpow I m x ∈ I
-- Mathlib.Topology.Algebra.LinearMapCompletion
ContinuousLinearMap.coe_fromCompletion : ∀ {α : Type u_1} {β : Type u_2} {R₁ : Type u_3} {R₂ : Type u_4} [inst : UniformSpace α] [inst_1 : AddCommGroup α]
  [inst_2 : IsUniformAddGroup α] [inst_3 : Semiring R₁] [inst_4 : Module R₁ α]
  [inst_5 : UniformContinuousConstSMul R₁ α] [inst_6 : Semiring R₂] [inst_7 : UniformSpace β] [inst_8 : AddCommGroup β]
  [inst_9 : IsUniformAddGroup β] [inst_10 : Module R₂ β] [inst_11 : UniformContinuousConstSMul R₂ β] {σ : R₁ →+* R₂}
  [inst_12 : T0Space β] [inst_13 : CompleteSpace β] (f : α →SL[σ] β),
  ⇑f.fromCompletion = UniformSpace.Completion.extension ⇑f
-- Mathlib.AlgebraicGeometry.Cover.Open
AlgebraicGeometry.Scheme.affineBasisCover_obj : ∀ (X : AlgebraicGeometry.Scheme) (i : X.affineBasisCover.I₀),
  X.affineBasisCover.X i = AlgebraicGeometry.Spec (X.affineBasisCoverRing i)
-- Mathlib.Topology.FiberBundle.Basic
FiberBundle.mem_trivializationAt_proj_source : ∀ {B : Type u_2} {F : Type u_3} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {E : B → Type u_5}
  [inst_2 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_3 : (b : B) → TopologicalSpace (E b)]
  [inst_4 : FiberBundle F E] {x : Bundle.TotalSpace F E}, x ∈ (trivializationAt F E x.proj).source
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.biproduct.ι_π_self : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [inst_2 : CategoryTheory.Limits.HasBiproduct f]
  (j : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι f j) (CategoryTheory.Limits.biproduct.π f j) =
    CategoryTheory.CategoryStruct.id (f j)
-- Mathlib.Control.Fold
Traversable.mapFold : {α β : Type u} →
  [inst : Monoid α] → [inst_1 : Monoid β] → (α →* β) → ApplicativeTransformation (Functor.Const α) (Functor.Const β)
-- Mathlib.Logic.Equiv.Basic
Equiv.Perm.subtypeCongr.eq_1 : ∀ {ε : Type u_9} {p : ε → Prop} [inst : DecidablePred p] (ep : Equiv.Perm { a // p a }) (en : Equiv.Perm { a // ¬p a }),
  ep.subtypeCongr en = (Equiv.sumCompl p).permCongr (ep.sumCongr en)
-- Mathlib.LinearAlgebra.Matrix.ToLin
Matrix.toLinOfInv_apply : ∀ {R : Type u_1} [inst : CommSemiring R] {m : Type u_3} {n : Type u_4} [inst_1 : Fintype n] [inst_2 : DecidableEq n]
  {M₁ : Type u_5} {M₂ : Type u_6} [inst_3 : AddCommMonoid M₁] [inst_4 : AddCommMonoid M₂] [inst_5 : Module R M₁]
  [inst_6 : Module R M₂] (v₁ : Module.Basis n R M₁) (v₂ : Module.Basis m R M₂) [inst_7 : Fintype m]
  [inst_8 : DecidableEq m] {M : Matrix m n R} {M' : Matrix n m R} (hMM' : M * M' = 1) (hM'M : M' * M = 1) (a : M₁),
  (Matrix.toLinOfInv v₁ v₂ hMM' hM'M) a = ((Matrix.toLin v₁ v₂) M) a
-- Mathlib.Computability.Primrec.Basic
Primrec.subtype_mk : ∀ {α : Type u_1} {β : Type u_2} [inst : Primcodable α] [inst_1 : Primcodable β] {p : β → Prop}
  [inst_2 : DecidablePred p] {hp : PrimrecPred p} {f : α → β} {h : ∀ (a : α), p (f a)},
  Primrec f → Primrec fun a => ⟨f a, ⋯⟩
-- Mathlib.Analysis.Normed.Field.Basic
/-- A real absolute value on a field determines a `NormedField` structure.  -/
AbsoluteValue.toNormedField : {K : Type u_5} → [inst : Field K] → AbsoluteValue K ℝ → NormedField K