mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Star.StarAlgHom
NonUnitalStarAlgHom.coe_restrictScalars : ∀ (R : Type u_1) {S : Type u_2} {A : Type u_3} {B : Type u_4} [inst : Monoid R] [inst_1 : Monoid S] [inst_2 : Star A]
  [inst_3 : Star B] [inst_4 : NonUnitalNonAssocSemiring A] [inst_5 : NonUnitalNonAssocSemiring B]
  [inst_6 : MulAction R S] [inst_7 : DistribMulAction S A] [inst_8 : DistribMulAction S B]
  [inst_9 : DistribMulAction R A] [inst_10 : DistribMulAction R B] [inst_11 : IsScalarTower R S A]
  [inst_12 : IsScalarTower R S B] (f : A →⋆ₙₐ[S] B), ↑(NonUnitalStarAlgHom.restrictScalars R f) = ↑f
-- Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset
CategoryTheory.CardinalDirectedPoset.instIsFilteredSubtypeSetCarrierObjPartOrdEmbIsCardinalFilteredWithTopPropSetWithTop : ∀ {κ : Cardinal.{u}} [inst : Fact κ.IsRegular] (J : CategoryTheory.CardinalDirectedPoset κ) (κ' : Cardinal.{u})
  [inst_1 : Fact κ'.IsRegular], CategoryTheory.IsFiltered (Subtype (J.PropSetWithTop κ'))
-- Mathlib.CategoryTheory.Monoidal.PushoutProduct
/-- The Leibniz functor associated to the tensor product on a monoidal category. This is the
bifunctor of arrow categories that sends `f : A ⟶ B` and `g : X ⟶ Y` to the canonical map from the
pushout of `f ◁ X` and `A ▷ g` to `B ⊗ Y`, induced by the following diagram:
```
  A ⊗ X --> B ⊗ X
     |          |
     v          v
  A ⊗ Y --> B ⊗ Y
```
 -/
CategoryTheory.MonoidalCategory.Arrow.pushoutProduct : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Limits.HasPushouts C] →
      [CategoryTheory.MonoidalCategory C] →
        CategoryTheory.Functor (CategoryTheory.Arrow C)
          (CategoryTheory.Functor (CategoryTheory.Arrow C) (CategoryTheory.Arrow C))
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.HasAddFundamentalDomain.mk : ∀ {G : Type u_6} {α : Type u_7} [inst : Zero G] [inst_1 : VAdd G α] [inst_2 : MeasurableSpace α]
  {ν : autoParam (MeasureTheory.Measure α) MeasureTheory.HasAddFundamentalDomain._auto_1},
  (∃ s, MeasureTheory.IsAddFundamentalDomain G s ν) → MeasureTheory.HasAddFundamentalDomain G α ν
-- Std.Data.TreeMap.Raw.Basic
/-- Tries to retrieve the key-value pair with the largest key in the tree map, returning `none` if the
map is empty.
 -/
Std.TreeMap.Raw.maxEntry? : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap.Raw α β cmp → Option (α × β)
-- Mathlib.MeasureTheory.Group.Action
MeasureTheory.measure_inter_neg_vadd : ∀ {G : Type u} {α : Type w} {m : MeasurableSpace α} [inst : AddGroup G] [inst_1 : AddAction G α]
  (μ : MeasureTheory.Measure α) [MeasureTheory.VAddInvariantMeasure G α μ] (c : G) (s t : Set α),
  μ (s ∩ (-c +ᵥ t)) = μ ((c +ᵥ s) ∩ t)
-- Mathlib.MeasureTheory.Group.Arithmetic
AddOpposite.instMeasurableAdd : ∀ {M : Type u_2} [inst : Add M] [inst_1 : MeasurableSpace M] [MeasurableAdd M], MeasurableAdd Mᵃᵒᵖ
-- Mathlib.Order.Monotone.Monovary
Antivary.dual : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β},
  Antivary f g → Antivary (⇑OrderDual.toDual ∘ f) (⇑OrderDual.toDual ∘ g)
-- Mathlib.GroupTheory.Nilpotent
/-- **Alias** of `Subgroup.nilpotent_iff_finite_descending_central_series`.

---

A group `G` is nilpotent iff there exists a descending central series which reaches the
trivial group in a finite time.  -/
nilpotent_iff_finite_descending_central_series : ∀ (G : Type u_1) [inst : Group G], Group.IsNilpotent G ↔ ∃ n H, Subgroup.IsDescendingCentralSeries H ∧ H n = ⊥
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.size_unitOfList_le : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α] {l : List α},
  (Std.DHashMap.Raw.Const.unitOfList l).size ≤ l.length
-- Mathlib.LinearAlgebra.AffineSpace.Independent
/-- An affinely independent set of points can be extended to such a
set that spans the whole space.  -/
exists_subset_affineIndependent_affineSpan_eq_top : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {s : Set P},
  (AffineIndependent k fun p => ↑p) → ∃ t, s ⊆ t ∧ (AffineIndependent k fun p => ↑p) ∧ affineSpan k t = ⊤
-- Mathlib.Algebra.Homology.AlternatingConst
/-- The `j`th homology of the alternating constant complex on `φ, ψ : A ⟶ A` is the homology of
`A --ψ--> A --φ--> A` when `prev(j) ~ j, j ~ next(j)` and `j` is even.  -/
HomologicalComplex.alternatingConstHomologyIsoEven : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (A : C) →
        {φ ψ : A ⟶ A} →
          (hOdd : CategoryTheory.CategoryStruct.comp φ ψ = 0) →
            (hEven : CategoryTheory.CategoryStruct.comp ψ φ = 0) →
              {c : ComplexShape ℕ} →
                [inst_2 : DecidableRel c.Rel] →
                  (hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)) →
                    [inst_3 : CategoryTheory.CategoryWithHomology C] →
                      {j : ℕ} →
                        c.Rel (c.prev j) j →
                          c.Rel j (c.next j) →
                            Even j →
                              ((HomologicalComplex.alternatingConst A hOdd hEven hc).homology j ≅
                                { X₁ := A, X₂ := A, X₃ := A, f := ψ, g := φ, zero := hEven }.homology)
-- Mathlib.Topology.FiberBundle.Basic
/-- Extend a vector `v ∈ V x` to a section of the bundle `V`, whose value at `x` is `v`.
The details of the extension are mostly unspecified: for covariant derivatives, the value of
`s` at points other than `x` will not matter (except for shorter proofs).
 -/
FiberBundle.extend : {B : Type u_2} →
  (F : Type u_3) →
    {E : B → Type u_5} →
      [inst : TopologicalSpace B] →
        [inst_1 : TopologicalSpace F] →
          [inst_2 : (x : B) → TopologicalSpace (E x)] →
            [(x : B) → Zero (E x)] →
              [inst_4 : TopologicalSpace (Bundle.TotalSpace F E)] → [FiberBundle F E] → {x : B} → E x → (x' : B) → E x'
-- Mathlib.Geometry.Euclidean.Sphere.Power
/-- **Intersecting Chords Theorem**.  -/
EuclideanGeometry.mul_dist_eq_mul_dist_of_cospherical_of_angle_eq_pi : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {P : Type u_2} [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {a b c d p : P},
  EuclideanGeometry.Cospherical {a, b, c, d} →
    EuclideanGeometry.angle a p b = Real.pi →
      EuclideanGeometry.angle c p d = Real.pi → dist a p * dist b p = dist c p * dist d p
-- Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
MvPolynomial.esymmPart_indiscrete : ∀ (σ : Type u_5) (R : Type u_6) [inst : CommSemiring R] [inst_1 : Fintype σ] (n : ℕ),
  MvPolynomial.esymmPart σ R (Nat.Partition.indiscrete n) = MvPolynomial.esymm σ R n
-- Mathlib.Algebra.Group.TypeTags.Finite
instInfiniteMultiplicative : ∀ {α : Type u} [h : Infinite α], Infinite (Multiplicative α)
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.parenthesizeCategoryCore : Lean.Name → ℕ → Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.Compacts.isCompact_subsets_of_isCompact : ∀ {α : Type u_1} [inst : TopologicalSpace α] {K : Set α}, IsCompact K → IsCompact {L | ↑L ⊆ K}
-- Lean.Meta.Tactic.Grind.Theorems
Lean.Meta.Grind.instReprOrigin.repr : Lean.Meta.Grind.Origin → ℕ → Std.Format
-- Lean.Server.FileWorker.SemanticHighlighting
/-- The current interval's token, with its start position suitably adjusted. The current interval's
token always has a priority that's at least as high as all tokens in `surrounding` (they may be
equal if overlapping tokens had the same priority, and a tiebreaker such as length was used).

When a token is replaced by a higher-priority token in part of its interval, its start position is
set to the end position of the overriding token when it is resumed.
 -/
_private.Lean.Server.FileWorker.SemanticHighlighting.0.Lean.Server.FileWorker.HandleOverlapState.current? : Lean.Server.FileWorker.HandleOverlapState✝ → Option Lean.Server.FileWorker.AbsoluteLspSemanticToken
-- Mathlib.Logic.Equiv.List
Equiv.listUniqueEquiv_apply : ∀ (α : Type u_1) [inst : Unique α] (a : List α), (Equiv.listUniqueEquiv α) a = a.length
-- Mathlib.Algebra.Star.LinearMap
/-- Intrinsic star operation for `(End R E)ˣ`.  -/
Module.End.Units.intrinsicStar : {R : Type u_1} →
  {E : Type u_2} →
    [inst : Semiring R] →
      [inst_1 : InvolutiveStar R] →
        [inst_2 : AddCommMonoid E] →
          [inst_3 : Module R E] → [inst_4 : StarAddMonoid E] → [StarModule R E] → Star (WithConv (Module.End R E)ˣ)
-- Mathlib.AlgebraicGeometry.Gluing
AlgebraicGeometry.Scheme.Cover.glued_cover_cocycle : ∀ {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (x y z : 𝒰.I₀),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Cover.gluedCoverT' 𝒰 x y z)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Cover.gluedCoverT' 𝒰 y z x)
        (AlgebraicGeometry.Scheme.Cover.gluedCoverT' 𝒰 z x y)) =
    CategoryTheory.CategoryStruct.id
      (CategoryTheory.Limits.pullback (CategoryTheory.Limits.pullback.fst (𝒰.f x) (𝒰.f y))
        (CategoryTheory.Limits.pullback.fst (𝒰.f x) (𝒰.f z)))
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.lift_inf : ∀ (F : Type u_1) [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (K : IntermediateField F E)
  (L L' : IntermediateField F ↥K),
  IntermediateField.lift (L ⊓ L') = IntermediateField.lift L ⊓ IntermediateField.lift L'
-- Mathlib.RingTheory.AlgebraicIndependent.Adjoin
AlgebraicIndependent.aevalEquivField.congr_simp : ∀ {ι : Type u_1} {F : Type u_2} {E : Type u_3} {x : ι → E} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E]
  (hx : AlgebraicIndependent F x), hx.aevalEquivField = hx.aevalEquivField
-- Init.Data.String.Basic
String.Slice.Pos.cast_rfl : ∀ {s : String.Slice} {pos : s.Pos}, pos.cast ⋯ = pos
-- Mathlib.Algebra.Category.Grp.Shrink
instSmallCompGrpCatForgetMonoidHomCarrierOfSmallObj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C GrpCat)
  [∀ (X : C), Small.{w, w'} ↑(F.obj X)],
  CategoryTheory.FunctorToTypes.Small.{w, w', v, u} (F.comp (CategoryTheory.forget GrpCat))
-- Mathlib.AlgebraicGeometry.Morphisms.Smooth
/-- If `f` is smooth of any relative dimension, it is smooth.  -/
AlgebraicGeometry.SmoothOfRelativeDimension.smooth : ∀ (n : ℕ) {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.SmoothOfRelativeDimension n f],
  AlgebraicGeometry.Smooth f
-- Mathlib.Logic.Basic
forall_prop_congr' : ∀ {p p' : Prop} {q q' : p → Prop}, (∀ (h : p), q h ↔ q' h) → ∀ (hp : p ↔ p'), (∀ (h : p), q h) = ∀ (h : p'), q' ⋯
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
Finpartition.nonUniforms.congr_simp : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : DecidableEq α] {A : Finset α}
  (P P_1 : Finpartition A),
  P = P_1 →
    ∀ (G G_1 : SimpleGraph α),
      G = G_1 →
        ∀ {inst_3 : DecidableRel G.Adj} [inst_4 : DecidableRel G_1.Adj] (ε ε_1 : 𝕜),
          ε = ε_1 → P.nonUniforms G ε = P_1.nonUniforms G_1 ε_1
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.Homotopy.unop_h₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex Cᵒᵖ} {φ₁ φ₂ : S₁ ⟶ S₂} (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂),
  h.unop.h₁ = h.h₂.unop
-- Mathlib.Tactic.Algebraize
_private.Mathlib.Tactic.Algebraize.0.Mathlib.Tactic.Algebraize.instEvalExprConfig.evalExpr : Lean.Expr → Lean.MetaM Mathlib.Tactic.Algebraize.Config
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.isSome_getKey?_eq_contains : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {a : α},
  (t.getKey? a).isSome = t.contains a
-- Mathlib.Algebra.Free
FreeAddSemigroup.instMonad : Monad FreeAddSemigroup
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor
/-- The "inclusion" maps to the colimit ring.  -/
PresheafOfModules.ModuleColimit.ιR : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {R : CategoryTheory.Functor Cᵒᵖ RingCat} → (cR : CategoryTheory.Limits.Cocone R) → {U : Cᵒᵖ} → ↑(R.obj U) →+* ↑cR.pt
-- Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_comp_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (K : ChainComplex C ℕ) {Δ Δ' Δ'' : SimplexCategory} (i' : Δ'' ⟶ Δ') (i : Δ' ⟶ Δ) [inst_2 : CategoryTheory.Mono i']
  [inst_3 : CategoryTheory.Mono i] {Z : C} (h : K.X Δ''.len ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono K i)
      (CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono K i') h) =
    CategoryTheory.CategoryStruct.comp
      (AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono K (CategoryTheory.CategoryStruct.comp i' i)) h
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.support_sum : ∀ {α : Type u_1} {β : Type u_7} {M : Type u_8} {N : Type u_10} [inst : DecidableEq β] [inst_1 : Zero M]
  [inst_2 : AddCommMonoid N] {f : α →₀ M} {g : α → M → β →₀ N},
  (f.sum g).support ⊆ f.support.biUnion fun a => (g a (f a)).support
-- Mathlib.Tactic.ClickSuggestions.Util
/-- Try to combine the suggested tactic with the preceding tactic in the tactic sequence.
In particular, we merge sequences of `rw`, `simp_rw` and `grw`.  -/
Mathlib.Tactic.ClickSuggestions.mergeTactics? : {m : Type → Type} →
  [Monad m] → [Lean.MonadQuotation m] → Lean.TSyntax `tactic → Lean.TSyntax `tactic → m (Option (Lean.TSyntax `tactic))
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.mk.sizeOf_spec : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : SizeOf R] [inst_4 : SizeOf A] (toNonUnitalSubsemiring : NonUnitalSubsemiring A)
  (smul_mem' : ∀ (c : R) {x : A}, x ∈ toNonUnitalSubsemiring.carrier → c • x ∈ toNonUnitalSubsemiring.carrier),
  sizeOf { toNonUnitalSubsemiring := toNonUnitalSubsemiring, smul_mem' := smul_mem' } =
    1 + sizeOf toNonUnitalSubsemiring
-- Mathlib.Analysis.Normed.Group.Defs
ESeminormedCommMonoid.toCommMonoid : {E : Type u_8} → [inst : TopologicalSpace E] → [self : ESeminormedCommMonoid E] → CommMonoid E
-- Mathlib.Algebra.GroupWithZero.Idempotent
IsIdempotentElem.instZeroSubtype : {M₀ : Type u_1} → [inst : MulZeroClass M₀] → Zero { p // IsIdempotentElem p }
-- Mathlib.AlgebraicGeometry.Morphisms.Etale
/-- **Alias** of `AlgebraicGeometry.Etale.etale_appLE`. -/
AlgebraicGeometry.Scheme.Hom.etale_appLE : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [self : AlgebraicGeometry.Etale f] {U : Y.Opens},
  AlgebraicGeometry.IsAffineOpen U →
    ∀ {V : X.Opens},
      AlgebraicGeometry.IsAffineOpen V →
        ∀ (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U),
          (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appLE f U V e)).Etale
-- Mathlib.AlgebraicGeometry.Artinian
AlgebraicGeometry.IsLocallyArtinian.iff_isLocallyNoetherian_and_discreteTopology : ∀ {X : AlgebraicGeometry.Scheme},
  AlgebraicGeometry.IsLocallyArtinian X ↔ AlgebraicGeometry.IsLocallyNoetherian X ∧ DiscreteTopology ↥X
-- Mathlib.Geometry.Euclidean.Sphere.Basic
EuclideanGeometry.Sphere.IsDiameter.left_ne_right_iff_radius_ne_zero : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {p₁ p₂ : P},
  s.IsDiameter p₁ p₂ → (p₁ ≠ p₂ ↔ s.radius ≠ 0)
-- Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity
/-- The Law of Quadratic Reciprocity: if `p` and `q` are odd primes and `p % 4 = 1`,
then `(q / p) = (p / q)`.  -/
legendreSym.quadratic_reciprocity_one_mod_four : ∀ {p q : ℕ} [inst : Fact (Nat.Prime p)] [inst_1 : Fact (Nat.Prime q)],
  p % 4 = 1 → q ≠ 2 → legendreSym q ↑p = legendreSym p ↑q
-- Mathlib.AlgebraicGeometry.Group.Affine
AlgebraicGeometry.one_spec_asOver_spec_left : ∀ {R A : CommRingCat} [inst : Bialgebra ↑R ↑A],
  CategoryTheory.Over.Hom.left CategoryTheory.MonObj.one =
    AlgebraicGeometry.Spec.map (CommRingCat.ofHom ↑(Bialgebra.counitAlgHom ↑R ↑A))
-- Mathlib.Combinatorics.Configuration
/-- If a nondegenerate configuration has at least as many points as lines, then there exists
an injective function `f` from lines to points, such that `f l` does not lie on `l`.  -/
Configuration.Nondegenerate.exists_injective_of_card_le : ∀ {P : Type u_1} {L : Type u_2} [inst : Membership P L] [Configuration.Nondegenerate P L] [inst_2 : Fintype P]
  [inst_3 : Fintype L], Fintype.card L ≤ Fintype.card P → ∃ f, Function.Injective f ∧ ∀ (l : L), f l ∉ l
-- Mathlib.Data.Set.PowersetCard
/-- The equivalence sending `a : α` to the singleton `{a}`.  -/
Set.powersetCard.ofSingleton : {α : Type u_1} → α ≃ ↑(Set.powersetCard α 1)
-- Lean.Meta.KExprMap
Lean.Meta.KExprMap.mk : {α : Type} → Lean.PHashMap Lean.HeadIndex (Lean.AssocList Lean.Expr α) → Lean.Meta.KExprMap α
-- Init.Data.Array.Lemmas
Array.ext_getElem? : ∀ {α : Type u_1} {xs ys : Array α}, (∀ (i : ℕ), xs[i]? = ys[i]?) → xs = ys
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.contains_filterMap : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β}
  [inst_2 : LawfulBEq α] {f : (a : α) → β a → Option (γ a)} {k : α},
  m.WF → (Std.DHashMap.Raw.filterMap f m).contains k = Option.any (fun x => (f k x).isSome) (m.get? k)
-- Mathlib.Analysis.Normed.Order.Hom.Basic
GroupNormClass.toNormedCommGroup.eq_1 : ∀ {F : Type u_1} {α : Type u_2} [inst : FunLike F α ℝ] [inst_1 : CommGroup α] [inst_2 : GroupNormClass F α ℝ] (f : F),
  GroupNormClass.toNormedCommGroup f =
    { toNorm := (GroupNormClass.toNormedGroup f).toNorm, toGroup := (GroupNormClass.toNormedGroup f).toGroup,
      mul_comm := ⋯, toMetricSpace := (GroupNormClass.toNormedGroup f).toMetricSpace, dist_eq := ⋯ }
-- Mathlib.Topology.Order
gc_nhds : ∀ {α : Type u} (a : α), GaloisConnection (nhdsAdjoint a) fun t => nhds a
-- Mathlib.Topology.NhdsSet
eventually_nhdsSet_iUnion₂ : ∀ {X : Type u_2} [inst : TopologicalSpace X] {ι : Sort u_4} {p : ι → Prop} {s : ι → Set X} {P : X → Prop},
  (∀ᶠ (x : X) in nhdsSet (⋃ i, ⋃ (_ : p i), s i), P x) ↔ ∀ (i : ι), p i → ∀ᶠ (x : X) in nhdsSet (s i), P x
-- Mathlib.RingTheory.DividedPowers.SubDPIdeal
DividedPowers.SubDPIdeal.ext_iff : ∀ {A : Type u_1} {inst : CommSemiring A} {I : Ideal A} {hI : DividedPowers I} {x y : hI.SubDPIdeal},
  x = y ↔ x.carrier = y.carrier
-- Mathlib.CategoryTheory.Functor.EpiMono
/-- If `F` is a fully faithful functor, split monomorphisms are preserved and reflected by `F`.  -/
CategoryTheory.Functor.splitMonoEquiv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) →
          {X Y : C} →
            (f : Y ⟶ X) → [F.Full] → [F.Faithful] → CategoryTheory.SplitMono f ≃ CategoryTheory.SplitMono (F.map f)
-- Mathlib.Order.Ideal
/-- The ideal is nonempty.  -/
Order.Ideal.nonempty' : ∀ {P : Type u_2} [inst : LE P] (self : Order.Ideal P), self.carrier.Nonempty
-- Aesop.Tracing
Aesop.TraceOption.proof : Aesop.TraceOption
-- Mathlib.Algebra.Order.Group.Action.Synonym
OrderDual.instAddAction.eq_1 : ∀ {M : Type u_1} {α : Type u_3} [inst : AddMonoid M] [inst_1 : AddAction M α],
  OrderDual.instAddAction = { toVAdd := OrderDual.instVAdd', add_vadd := ⋯, zero_vadd := ⋯ }
-- Mathlib.RingTheory.FractionalIdeal.Inverse
FractionalIdeal.mul_inv_cancel_iff_isUnit : ∀ (K : Type u_3) [inst : Field K] {R₁ : Type u_4} [inst_1 : CommRing R₁] [inst_2 : IsDomain R₁] [inst_3 : Algebra R₁ K]
  [inst_4 : IsFractionRing R₁ K] {I : FractionalIdeal (nonZeroDivisors R₁) K}, I * I⁻¹ = 1 ↔ IsUnit I
-- Mathlib.LinearAlgebra.Matrix.RowCol
Matrix.mulVec_replicateCol_eq_const : ∀ {m : Type u_2} {α : Type v} {ι : Type u_6} [inst : Fintype m] [inst_1 : NonUnitalNonAssocSemiring α] (v w : m → α),
  Matrix.vecMul v (Matrix.replicateCol ι w) = Function.const ι (v ⬝ᵥ w)
-- Mathlib.Analysis.InnerProductSpace.Orthonormal
Orthonormal.nnnorm_eq_one : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_4} {v : ι → E}, Orthonormal 𝕜 v → ∀ (i : ι), ‖v i‖₊ = 1
-- Mathlib.Logic.Unique
Fin.instUnique : Unique (Fin 1)
-- Mathlib.LinearAlgebra.Matrix.Hadamard
Matrix.hadamard_one : ∀ {α : Type u_1} {n : Type u_3} [inst : DecidableEq n] [inst_1 : MulZeroOneClass α] (M : Matrix n n α),
  M.hadamard 1 = Matrix.diagonal M.diag
-- Mathlib.CategoryTheory.InducedCategory
CategoryTheory.InducedCategory.Hom.mk.sizeOf_spec : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v, u₂} D] {F : C → D}
  {X Y : CategoryTheory.InducedCategory D F} [inst_1 : SizeOf C] [inst_2 : SizeOf D] (hom : F X ⟶ F Y),
  sizeOf { hom := hom } = 1 + sizeOf hom
-- Mathlib.Order.Booleanisation
Booleanisation.lift_le_lift : ∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] {a b : α}, Booleanisation.lift a ≤ Booleanisation.lift b ↔ a ≤ b
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- Uses `left` co(ntra)variant.  -/
Left.neg_neg_iff : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α] [AddLeftStrictMono α] {a : α}, -a < 0 ↔ 0 < a
-- Init.Data.SInt.Bitwise
Int8.zero_or : ∀ {a : Int8}, 0 ||| a = a
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.AdjoinSimple.algebraMap_gen : ∀ (F : Type u_1) [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (α : E),
  (algebraMap (↥F⟮α⟯) E) (IntermediateField.AdjoinSimple.gen F α) = α
-- Mathlib.Algebra.Group.Subgroup.Pointwise
Subgroup.normalizer_le_normalizer_sup_of_normalizer_le_left : ∀ {G : Type u_2} [inst : Group G] {H K : Subgroup G},
  Subgroup.normalizer ↑H ≤ Subgroup.normalizer ↑K → Subgroup.normalizer ↑H ≤ Subgroup.normalizer ↑(H ⊔ K)
-- Mathlib.Data.Set.Subset
Set.image_val_compl : ∀ {α : Type u_2} {A : Set α} {D : Set ↑A}, Subtype.val '' Dᶜ = A \ Subtype.val '' D
-- Mathlib.RingTheory.ChainOfDivisors
coe_factor_orderIso_map_eq_one_iff : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [IsCancelMulZero M] {N : Type u_2} [inst_2 : CommMonoidWithZero N]
  [IsCancelMulZero N] {m u : Associates M} {n : Associates N} (hu' : u ≤ m) (d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)),
  ↑(d ⟨u, hu'⟩) = 1 ↔ u = 1
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.end_mem_tail_support : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v}, ¬p.Nil → v ∈ p.support.tail
-- Std.Time.Time.HourMarker
Std.Time.HourMarker.ofNat : ℕ → Std.Time.HourMarker
-- Mathlib.Algebra.Homology.SingleHomology
HomologicalComplex.singleObjOpcyclesSelfIso.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {ι : Type u_1} [inst_3 : DecidableEq ι] (c : ComplexShape ι) (j : ι)
  (A : C),
  HomologicalComplex.singleObjOpcyclesSelfIso c j A =
    (HomologicalComplex.singleObjXSelf c j A).symm ≪≫
      ((HomologicalComplex.single C c j).obj A).pOpcyclesIso (c.prev j) j ⋯ ⋯
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
cfcHom_mem_elemental : ∀ {𝕜 : Type u_1} {A : Type u_2} {p : A → Prop} [inst : RCLike 𝕜] [inst_1 : Ring A] [inst_2 : StarRing A]
  [inst_3 : Algebra 𝕜 A] [inst_4 : TopologicalSpace A] [inst_5 : StarModule 𝕜 A]
  [inst_6 : ContinuousFunctionalCalculus 𝕜 A p] [inst_7 : IsTopologicalRing A] [inst_8 : ContinuousStar A] {a : A}
  (ha : p a) (f : C(↑(spectrum 𝕜 a), 𝕜)), (cfcHom ha) f ∈ StarAlgebra.elemental 𝕜 a
-- Mathlib.Analysis.Convex.Integral
/-- If `E` is a strictly convex normed space and `f : α → E` is a function such that `‖f x‖ ≤ C`
a.e., then either this function is a.e. equal to its average value, or the norm of its integral is
strictly less than `μ.real univ * C`.  -/
ae_eq_const_or_norm_integral_lt_of_norm_le_const : ∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [CompleteSpace E] {μ : MeasureTheory.Measure α} {f : α → E} {C : ℝ} [StrictConvexSpace ℝ E]
  [MeasureTheory.IsFiniteMeasure μ],
  (∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C) → f =ᵐ[μ] Function.const α (⨍ (x : α), f x ∂μ) ∨ ‖∫ (x : α), f x ∂μ‖ < μ.real Set.univ * C