mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Module.Submodule.Lattice
Submodule.coe_eq_univ : ∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {p : Submodule R M}, ↑p = Set.univ ↔ p = ⊤
-- Mathlib.Topology.Path
Path.prod_coe : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {a₁ a₂ : X} {b₁ b₂ : Y}
  (γ₁ : Path a₁ a₂) (γ₂ : Path b₁ b₂), ⇑(γ₁.prod γ₂) = fun t => (γ₁ t, γ₂ t)
-- Mathlib.CategoryTheory.Monad.Adjunction
CategoryTheory.Adjunction.adjToMonadIso_inv_toNatTrans_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) (X : C),
  (CategoryTheory.Adjunction.adjToMonadIso T).inv.app X = CategoryTheory.CategoryStruct.id (T.obj X)
-- Mathlib.LinearAlgebra.Finsupp.Pi
Finsupp.lcoeFun_comp_lsingle : ∀ {α : Type u_1} {M : Type u_2} {R : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : DecidableEq α] (x : α), Finsupp.lcoeFun ∘ₗ Finsupp.lsingle x = LinearMap.single R (fun x => M) x
-- Mathlib.FieldTheory.IsAlgClosed.Basic
Algebra.IsAlgebraic.algHomEquivAlgHomOfSplits_apply_apply : ∀ {F : Type u_1} {K : Type u_2} (A : Type u_3) [inst : Field F] [inst_1 : Field K] [inst_2 : Field A]
  [inst_3 : Algebra F K] [inst_4 : Algebra F A] [inst_5 : Algebra.IsAlgebraic F K] (L : Type u_4) [inst_6 : Field L]
  [inst_7 : Algebra F L] [inst_8 : Algebra L A] [inst_9 : IsScalarTower F L A]
  (hL : ∀ (x : K), (Polynomial.map (algebraMap F L) (minpoly F x)).Splits) (f : K →ₐ[F] L) (x : K),
  ((Algebra.IsAlgebraic.algHomEquivAlgHomOfSplits A L hL) f) x = (algebraMap L A) (f x)
-- Mathlib.Topology.Constructions
Continuous.subtype_map : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {p : X → Prop} {f : X → Y},
  Continuous f → ∀ {q : Y → Prop} (hpq : ∀ (x : X), p x → q (f x)), Continuous (Subtype.map f hpq)
-- Mathlib.Algebra.Homology.ModelCategory.Lifting
CochainComplex.Lifting.comp_coe_cocyle₁'_v_eq_zero_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {A B X Y : CochainComplex C ℤ} {t : A ⟶ X} {i : A ⟶ B} {p : X ⟶ Y} {b : B ⟶ Y} (sq : CategoryTheory.CommSq t i p b)
  (hsq : (n : ℤ) → ⋯.LiftStruct) (n m : ℤ)
  (hnm : autoParam (n + 1 = m) CochainComplex.Lifting.comp_coe_cocyle₁'_v_eq_zero._auto_1) {Z : C} (h : X.X m ⟶ Z),
  CategoryTheory.CategoryStruct.comp (i.f n)
      (CategoryTheory.CategoryStruct.comp ((↑(CochainComplex.Lifting.cocycle₁' sq hsq)).v n m hnm) h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.RingTheory.NormalClosure
Ring.instIsGaloisFractionRingNormalClosure : ∀ (R : Type u_1) (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : IsDomain R] [inst_3 : IsDomain S]
  [inst_4 : Algebra R S] [inst_5 : Module.IsTorsionFree R S] [Module.Finite R S] [PerfectField (FractionRing R)],
  IsGalois (FractionRing R) (FractionRing (Ring.NormalClosure R S))
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Products
/-- (Impl) A preliminary definition to avoid timeouts.  -/
CategoryTheory.Over.ConstructProducts.conesEquivUnitIso : {J : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      (B : C) →
        (F : CategoryTheory.Functor (CategoryTheory.Discrete J) (CategoryTheory.Over B)) →
          CategoryTheory.Functor.id
              (CategoryTheory.Limits.Cone
                (CategoryTheory.Over.ConstructProducts.widePullbackDiagramOfDiagramOver B F)) ≅
            (CategoryTheory.Over.ConstructProducts.conesEquivFunctor B F).comp
              (CategoryTheory.Over.ConstructProducts.conesEquivInverse B F)
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
CategoryTheory.Bicategory.Adj.Bicategory.whiskerRight_τr : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : CategoryTheory.Bicategory.Adj B} {α α' : a ⟶ b}
  (x : α ⟶ α') (β : b ⟶ c),
  (CategoryTheory.Bicategory.Adj.Bicategory.whiskerRight x β).τr = CategoryTheory.Bicategory.whiskerLeft β.r x.τr
-- Mathlib.CategoryTheory.ObjectProperty.Small
CategoryTheory.ObjectProperty.instSmallISupOfSmall : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {α : Type u_1} (P : α → CategoryTheory.ObjectProperty C)
  [∀ (a : α), CategoryTheory.ObjectProperty.Small.{w, v, u} (P a)] [Small.{w, u_1} α],
  CategoryTheory.ObjectProperty.Small.{w, v, u} (⨆ a, P a)
-- Mathlib.Probability.ConditionalProbability
ProbabilityTheory.ae_cond_mem₀ : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {s : Set Ω},
  MeasureTheory.NullMeasurableSet s μ → ∀ᵐ (x : Ω) ∂μ[|s], x ∈ s
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.Equiv.of_forall_get?_eq : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α],
  m₁.WF → m₂.WF → (∀ (k : α), m₁.get? k = m₂.get? k) → m₁.Equiv m₂
-- Mathlib.CategoryTheory.Subobject.MonoOver
CategoryTheory.MonoOver.map_obj_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [inst_1 : CategoryTheory.Mono f]
  (g : CategoryTheory.MonoOver X), ((CategoryTheory.MonoOver.map f).obj g).obj.left = g.obj.left
-- Mathlib.Algebra.Group.Units.Basic
Units.mul_eq_one_iff_eq_inv : ∀ {α : Type u} [inst : Monoid α] {u : αˣ} {a : α}, a * ↑u = 1 ↔ a = ↑u⁻¹
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.map_smul : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (Q : QuadraticMap R M N) (a : R) (x : M), Q (a • x) = (a * a) • Q x
-- Lean.Meta.Tactic.Grind.Arith.Insts
Lean.Meta.Grind.Arith.getPowIdentityInst? : Lean.Level → Lean.Expr → Lean.Meta.Grind.GoalM (Option (Lean.Expr × Lean.Expr × ℕ))
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.isEmpty_filterMap_iff : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {γ : Type w} {t : Std.DTreeMap.Internal.Impl α fun x => β}
  [Std.TransOrd α] {f : α → β → Option γ} (h : t.WF),
  (Std.DTreeMap.Internal.Impl.filterMap f t ⋯).impl.isEmpty = true ↔
    ∀ (k : α) (h : Std.DTreeMap.Internal.Impl.contains k t = true),
      f (t.getKey k h) (Std.DTreeMap.Internal.Impl.Const.get t k h) = none
-- Mathlib.Order.Filter.IsBounded
Monotone.isBoundedUnder_le_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {l : Filter γ} {u : γ → α}
  {v : α → β},
  Monotone v → Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l u → Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l (v ∘ u)
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroup.Normal.mk : ∀ {A : Type u_2} [inst : AddGroup A] {H : AddSubgroup A}, (∀ n ∈ H, ∀ (g : A), g + n + -g ∈ H) → H.Normal
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getD_filterMap_of_getKey?_eq_some : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {γ : Type w} {m : Std.ExtDHashMap α fun x => β}
  [inst : EquivBEq α] [inst_1 : LawfulHashable α] {f : α → β → Option γ} {k k' : α} {fallback : γ},
  m.getKey? k = some k' →
    Std.ExtDHashMap.Const.getD (Std.ExtDHashMap.filterMap f m) k fallback =
      ((Std.ExtDHashMap.Const.get? m k).bind (f k')).getD fallback
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
SSet.N.dim_le_of_le : ∀ {X : SSet} {x y : X.N}, x ≤ y → x.dim ≤ y.dim
-- Mathlib.ModelTheory.PartialEquiv
FirstOrder.Language.PartialEquiv.mk.sizeOf_spec : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
  [inst_2 : SizeOf M] [inst_3 : SizeOf N] (dom : L.Substructure M) (cod : L.Substructure N)
  (toEquiv : L.Equiv ↥dom ↥cod),
  sizeOf { dom := dom, cod := cod, toEquiv := toEquiv } = 1 + sizeOf dom + sizeOf cod + sizeOf toEquiv
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Poly.denote_le.eq_1 : ∀ (ctx : Nat.Internal.Linear.Context) (mp : Nat.Internal.Linear.Poly × Nat.Internal.Linear.Poly),
  Nat.Internal.Linear.Poly.denote_le ctx mp =
    (Nat.Internal.Linear.Poly.denote ctx mp.1 ≤ Nat.Internal.Linear.Poly.denote ctx mp.2)
-- Lean.Elab.MutualInductive
Lean.Elab.Command.ElabHeaderResult.mk : Lean.Elab.Command.PreElabHeaderResult → Lean.Expr → Lean.Elab.Command.ElabHeaderResult
-- Mathlib.Algebra.Group.Units.Defs
/-- Additive units of an additive monoid have an induced addition.  -/
AddUnits.instAdd : {α : Type u} → [inst : AddMonoid α] → Add (AddUnits α)
-- Mathlib.RingTheory.WittVector.Identities
WittVector.mul_pow_charP_coeff_succ : ∀ {p : ℕ} {R : Type u_1} [hp : Fact (Nat.Prime p)] [inst : CommRing R] [CharP R p] (x : WittVector p R) {m n : ℕ},
  (x * ↑p ^ n).coeff (m + n) = x.coeff m ^ p ^ n
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCastD_modifyKey : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {k k' : α} {fallback : β k'} {f : β k → β k}
  (l : List ((a : α) × β a)),
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.getValueCastD k' (Std.Internal.List.modifyKey k f l) fallback =
      if heq : (k == k') = true then
        (Option.map (cast ⋯) (Option.map f (Std.Internal.List.getValueCast? k l))).getD fallback
      else Std.Internal.List.getValueCastD k' l fallback
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.natCast_image_Iio : ∀ (n : ℕ), Nat.cast '' Set.Iio n = Set.Iio ↑n
-- Mathlib.CategoryTheory.Preadditive.Biproducts
/-- In a preadditive category, we can construct a biproduct for `f : J → C` from
any bicone `b` for `f` satisfying `total : ∑ j : J, b.π j ≫ b.ι j = 𝟙 b.X`.

(That is, such a bicone is a limit cone and a colimit cocone.)
 -/
CategoryTheory.Limits.hasBiproduct_of_total : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {J : Type u_1}
  [inst_2 : Fintype J] {f : J → C} (b : CategoryTheory.Limits.Bicone f),
  ∑ j, CategoryTheory.CategoryStruct.comp (b.π j) (b.ι j) = CategoryTheory.CategoryStruct.id b.pt →
    CategoryTheory.Limits.HasBiproduct f
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteAddGrp.ContinuousMulEquiv.toProfiniteAddGrpIso.eq_1 : ∀ {X Y : ProfiniteAddGrp.{u_1}} (e : ↑X.toProfinite.toTop ≃ₜ+ ↑Y.toProfinite.toTop),
  ProfiniteAddGrp.ContinuousMulEquiv.toProfiniteAddGrpIso e =
    { hom := ProfiniteAddGrp.ofHom ↑e, inv := ProfiniteAddGrp.ofHom ↑e.symm, hom_inv_id := ⋯, inv_hom_id := ⋯ }
-- Mathlib.CategoryTheory.Core
CategoryTheory.coreCategory_inv_iso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {x x_1 : CategoryTheory.Core C}
  (f : CategoryTheory.CoreHom x x_1), (CategoryTheory.Groupoid.inv f).iso = f.iso.symm
-- Mathlib.Analysis.Normed.Ring.WithAbs
WithAbs.toAbs_injective : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring S] [inst_1 : PartialOrder S] [inst_2 : Semiring R]
  (v : AbsoluteValue R S), Function.Injective (WithAbs.toAbs v)
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHom.coe_zero : ∀ {α : Type u_5} [inst : NonUnitalNonAssocSemiring α], ⇑0 = 0
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.constGetD_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  {k : α} {fallback : β}, t₁.Equiv t₂ → Std.DTreeMap.Const.getD t₁ k fallback = Std.DTreeMap.Const.getD t₂ k fallback
-- Mathlib.Order.Partition.Finpartition
Finpartition.avoid.eq_1 : ∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] [inst_1 : DecidableEq α] {a : α} (P : Finpartition a) (b : α),
  P.avoid b = Finpartition.ofErase (Finset.image (fun x => x \ b) P.parts) ⋯ ⋯
-- Init.Omega.IntList
Lean.Omega.IntList.dot_of_left_zero : ∀ {xs ys : Lean.Omega.IntList}, (∀ x ∈ xs, x = 0) → xs.dot ys = 0
-- Init.Data.List.Control
List.foldlM.eq_def : ∀ {m : Type u → Type v} [inst : Monad m] {s : Type u} {α : Type w} (x : s → α → m s) (x_1 : s) (x_2 : List α),
  List.foldlM x x_1 x_2 =
    match x, x_1, x_2 with
    | x, s_1, [] => pure s_1
    | f, s_1, a :: as => do
      let s' ← f s_1 a
      List.foldlM f s' as
-- Lean.Linter.UnusedVariables
/-- The list of builtin `IgnoreFunction`s.  -/
Lean.Linter.builtinUnusedVariablesIgnoreFnsRef : IO.Ref (Array Lean.Linter.IgnoreFunction)
-- Mathlib.Topology.MetricSpace.ThickenedIndicator
thickenedIndicatorAux_le_one : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α] (δ : ℝ) (E : Set α) (x : α), thickenedIndicatorAux δ E x ≤ 1
-- Mathlib.Topology.Order.Basic
/-- The order topology on an ordered type is the topology generated by open intervals. We register
it on a preorder, but it is mostly interesting in linear orders, where it is also order-closed.
We define it as a mixin. If you want to introduce the order topology on a preorder, use
`Preorder.topology`.  -/
OrderTopology : (α : Type u_1) → [t : TopologicalSpace α] → [Preorder α] → Prop
-- Mathlib.Analysis.Distribution.DerivNotation
/-- `∂_{v} f` is the line derivative of `f` in direction `v`. The meaning of this notation is
type-dependent.  -/
LineDeriv.lineDerivOp : {V : Type u} → {E : Type v} → {F : outParam (Type w)} → [self : LineDeriv V E F] → V → E → F
-- Mathlib.Topology.Order
TopologicalSpace.generateFrom_setOfPred_isOpen : ∀ {α : Type u} (t : TopologicalSpace α), TopologicalSpace.generateFrom {s | IsOpen s} = t
-- Mathlib.Algebra.Group.Units.Hom
AddUnits.map_injective : ∀ {M : Type u} {N : Type v} [inst : AddMonoid M] [inst_1 : AddMonoid N] {f : M →+ N},
  Function.Injective ⇑f → Function.Injective ⇑(AddUnits.map f)
-- Mathlib.LinearAlgebra.Eigenspace.Zero
/-- The geometric multiplicity of an eigenvalue is at most the algebraic multiplicity.  -/
LinearMap.finrank_eigenspace_le : ∀ {K : Type u_2} {M : Type u_3} [inst : Field K] [inst_1 : AddCommGroup M] [inst_2 : Module K M]
  [inst_3 : Module.Finite K M] (φ : Module.End K M) (μ : K),
  Module.finrank K ↥(φ.eigenspace μ) ≤ Polynomial.rootMultiplicity μ (LinearMap.charpoly φ)
-- Std.Time.Time.Unit.Basic
/-- Converts a `Millisecond.Offset` to a `Second.Offset`.
 -/
Std.Time.Millisecond.Offset.toSeconds : Std.Time.Millisecond.Offset → Std.Time.Second.Offset
-- Mathlib.CategoryTheory.Limits.Presheaf
/-- The cocone with point `P` given by `coconeOfRepresentable` is a colimit:
that is, we have exhibited an arbitrary presheaf `P` as a colimit of representables.

The result of [MM92], Chapter I, Section 5, Corollary 3.
 -/
CategoryTheory.Presheaf.colimitOfRepresentable : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (P : CategoryTheory.Functor Cᵒᵖ (Type (max w v₁))) →
      CategoryTheory.Limits.IsColimit (CategoryTheory.Presheaf.coconeOfRepresentable P)
-- Mathlib.Computability.TuringMachine.Tape
/-- A pointed map of `Inhabited` types is a map that sends one default value to the other.  -/
Turing.PointedMap : (Γ : Type u) → (Γ' : Type v) → [Inhabited Γ] → [Inhabited Γ'] → Type (max u v)
-- Mathlib.Algebra.Star.StarAlgHom
NonUnitalStarAlgHom.id_comp : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : Monoid R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : DistribMulAction R A] [inst_3 : Star A] [inst_4 : NonUnitalNonAssocSemiring B]
  [inst_5 : DistribMulAction R B] [inst_6 : Star B] (f : A →⋆ₙₐ[R] B), (NonUnitalStarAlgHom.id R B).comp f = f
-- Mathlib.Data.List.Basic
List.monotone_filter_right : ∀ {α : Type u} (l : List α) ⦃p q : α → Bool⦄,
  (∀ (a : α), p a = true → q a = true) → (List.filter p l).Sublist (List.filter q l)
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.instDivNonZeroDivisors : {R₁ : Type u_3} →
  [inst : CommRing R₁] →
    {K : Type u_4} →
      [inst_1 : Field K] →
        [inst_2 : Algebra R₁ K] → [IsFractionRing R₁ K] → [IsDomain R₁] → Div (FractionalIdeal (nonZeroDivisors R₁) K)
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.eRk_eq_eRk_union_eRk_le_zero : ∀ {α : Type u_1} {M : Matroid α} {Y : Set α} (X : Set α), M.eRk Y ≤ 0 → M.eRk (X ∪ Y) = M.eRk X
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.toList_toArray : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp},
  (Std.DTreeMap.Raw.Const.toArray t).toList = Std.DTreeMap.Raw.Const.toList t
-- Batteries.Data.List.Pairwise
List.pwFilter_map : ∀ {α : Type u_1} {R : α → α → Prop} {β : Type u_2} [inst : DecidableRel R] (f : β → α) (l : List β),
  List.pwFilter R (List.map f l) = List.map f (List.pwFilter (fun x y => R (f x) (f y)) l)
-- Mathlib.Data.Finset.BooleanAlgebra
Finset.univ_map_subtype : ∀ {α : Type u_1} [inst : Fintype α] (p : α → Prop) [inst_1 : DecidablePred p] [inst_2 : Fintype { a // p a }],
  Finset.map (Function.Embedding.subtype p) Finset.univ = Finset.filter p Finset.univ
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.mul_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : Ring β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] (f g : CauSeq β abv) (i : ℕ), ↑(f * g) i = ↑f i * ↑g i
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.AffineScheme.mk_obj : ∀ (X : AlgebraicGeometry.Scheme) (x : AlgebraicGeometry.IsAffine X), (AlgebraicGeometry.AffineScheme.mk X x).obj = X
-- Mathlib.Analysis.Calculus.Gradient.Basic
gradient.eq_1 : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F] [inst_2 : InnerProductSpace 𝕜 F]
  [inst_3 : CompleteSpace F] (f : F → 𝕜) (x : F), gradient f x = (InnerProductSpace.toDual 𝕜 F).symm (fderiv 𝕜 f x)
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.comap_evalRingHom_basicOpen : ∀ {ι : Type u_1} {R : ι → Type u_2} [inst : (i : ι) → CommRing (R i)] [inst_1 : DecidableEq ι] (i : ι) (f : R i),
  PrimeSpectrum.comap (Pi.evalRingHom R i) '' ↑(PrimeSpectrum.basicOpen f) = ↑(PrimeSpectrum.basicOpen (Pi.single i f))
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
/-- Let `𝒜` be a graded ring, finitely generated (as an algebra) over `𝒜₀` by `{ vᵢ }`,
where `vᵢ` has degree `dvᵢ`.
If `f : A` has degree `d`, then `𝒜_(f)` is generated (as a module) over `𝒜₀` by
elements of the form `(∏ i, vᵢ ^ aᵢ) / fᵃ` such that `∑ aᵢ • dvᵢ = a • d`.
 -/
HomogeneousLocalization.Away.span_mk_prod_pow_eq_top : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubgroupClass σ A] [inst_3 : AddCommMonoid ι] [inst_4 : DecidableEq ι] {𝒜 : ι → σ}
  [inst_5 : GradedRing 𝒜] {f : A} {d : ι} (hf : f ∈ 𝒜 d) {ι' : Type u_4} [inst_6 : Fintype ι'] (v : ι' → A),
  Algebra.adjoin (↥(𝒜 0)) (Set.range v) = ⊤ →
    ∀ (dv : ι' → ι) (hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)),
      Submodule.span ↥(𝒜 0)
          {x |
            ∃ a ai,
              ∃ (hai : ∑ i, ai i • dv i = a • d), HomogeneousLocalization.Away.mk 𝒜 hf a (∏ i, v i ^ ai i) ⋯ = x} =
        ⊤
-- Mathlib.Algebra.Category.MonCat.Limits
MonCat.limitπMonoidHom.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J MonCat)
  [inst_1 : Small.{u, max u v} ↑(F.comp (CategoryTheory.forget MonCat)).sections] (j : J),
  MonCat.limitπMonoidHom F j =
    {
      toFun :=
        ⇑(CategoryTheory.ConcreteCategory.hom
            ((CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget MonCat))).π.app j)),
      map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
IsGreatest.nnnorm_cfc : ∀ {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [inst : RCLike 𝕜] [inst_1 : NormedRing A]
  [inst_2 : StarRing A] [inst_3 : NormedAlgebra 𝕜 A] [inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p]
  [Nontrivial A] (f : 𝕜 → 𝕜) (a : A),
  autoParam (ContinuousOn f (spectrum 𝕜 a)) IsGreatest.nnnorm_cfc._auto_1 →
    autoParam (p a) IsGreatest.nnnorm_cfc._auto_3 → IsGreatest ((fun x => ‖f x‖₊) '' spectrum 𝕜 a) ‖cfc f a‖₊
-- Mathlib.Topology.MetricSpace.HolderNorm
HolderWith.eHolderNorm_le : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] {r : NNReal} {f : X → Y}
  {C : NNReal}, HolderWith C r f → eHolderNorm r f ≤ ↑C
-- Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
/-- `Submodule.baseChange` as an order embedding.  -/
Submodule.baseChangeOrderEmbedding : (R : Type u_1) →
  (M : Type u_2) →
    (A : Type u_3) →
      [inst : CommRing R] →
        [inst_1 : Ring A] →
          [inst_2 : Algebra R A] →
            [Module.FaithfullyFlat R A] →
              [inst_4 : AddCommGroup M] → [inst_5 : Module R M] → Submodule R M ↪o Submodule A (TensorProduct R A M)
-- Batteries.Data.ByteSlice
ByteSlice.instCoeByteArray_batteries : Coe ByteArray ByteSlice
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeAddGroup.norm_of_nsmul : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (n : ℕ), (n • FreeAddGroup.of a).norm = n
-- Mathlib.Order.Lattice
/-- A type endowed with `⊔` and `⊓` is a `Lattice`, if it admits an injective map that
preserves `⊔` and `⊓` to a `Lattice`.
See note [reducible non-instances].  -/
Function.Injective.lattice : {α : Type u} →
  {β : Type v} →
    [inst : Max α] →
      [inst_1 : Min α] →
        [inst_2 : LE α] →
          [inst_3 : LT α] →
            [inst_4 : Lattice β] →
              (f : α → β) →
                Function.Injective f →
                  (∀ {x y : α}, f x ≤ f y ↔ x ≤ y) →
                    (∀ {x y : α}, f x < f y ↔ x < y) →
                      (∀ (a b : α), f (a ⊔ b) = f a ⊔ f b) → (∀ (a b : α), f (a ⊓ b) = f a ⊓ f b) → Lattice α
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
/-- Turn a uniform isomorphism `γ ≃ᵤ β` into a uniform isomorphism `(α →ᵤ[𝔖] γ) ≃ᵤ (α →ᵤ[𝔖] β)`
by post-composing.  -/
UniformOnFun.congrRight : {α : Type u_1} →
  {β : Type u_2} →
    {γ : Type u_3} →
      [inst : UniformSpace β] →
        {𝔖 : Set (Set α)} → [inst_1 : UniformSpace γ] → γ ≃ᵤ β → UniformOnFun α γ 𝔖 ≃ᵤ UniformOnFun α β 𝔖
-- Mathlib.Topology.Instances.Matrix
Summable.matrix_diag : ∀ {X : Type u_1} {n : Type u_5} {R : Type u_8} [inst : AddCommMonoid R] [inst_1 : TopologicalSpace R]
  {L : SummationFilter X} {f : X → Matrix n n R}, Summable f L → Summable (fun x => (f x).diag) L
-- Mathlib.Data.Multiset.UnionInter
Multiset.le_union_right : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Multiset α}, t ≤ s ∪ t
-- Init.Data.Nat.Gcd
Nat.gcd_mul_right : ∀ (m n k : ℕ), (m * n).gcd (k * n) = m.gcd k * n
-- Init.Prelude
instInhabitedRaw : Inhabited String.Pos.Raw
-- Mathlib.Topology.Algebra.Group.Basic
OrderDual.instContinuousInv : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Inv G] [ContinuousInv G], ContinuousInv Gᵒᵈ
-- Mathlib.Tactic.Module
_private.Mathlib.Tactic.Module.0.Mathlib.Tactic.Module.qNF.add.match_1.splitter : {u v : Lean.Level} →
  {M : Q(Type v)} →
    {R : Q(Type u)} →
      (motive : Mathlib.Tactic.Module.qNF R M → Mathlib.Tactic.Module.qNF R M → Sort u_1) →
        (x x_1 : Mathlib.Tactic.Module.qNF R M) →
          ((l : Mathlib.Tactic.Module.qNF R M) → motive [] l) →
            ((l : Mathlib.Tactic.Module.qNF R M) → (l = [] → False) → motive l []) →
              ((a₁ : Q(«$R»)) →
                  (x₁ : Q(«$M»)) →
                    (k₁ : ℕ) →
                      (t₁ : Mathlib.Tactic.Module.NF (Q(«$R») × Q(«$M»)) ℕ) →
                        (a₂ : Q(«$R»)) →
                          (x₂ : Q(«$M»)) →
                            (k₂ : ℕ) →
                              (t₂ : Mathlib.Tactic.Module.NF (Q(«$R») × Q(«$M»)) ℕ) →
                                motive (((a₁, x₁), k₁) :: t₁) (((a₂, x₂), k₂) :: t₂)) →
                motive x x_1
-- Init.Data.Dyadic.Basic
Dyadic.toRat_ofOdd_eq_mkRat : ∀ {n k : ℤ} {hn : n % 2 = 1}, (Dyadic.ofOdd n k hn).toRat = mkRat (n <<< (-k).toNat) (1 <<< k.toNat)
-- Mathlib.RingTheory.Support
Module.notMem_support_iff' : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {p : PrimeSpectrum R}, p ∉ Module.support R M ↔ ∀ (m : M), ∃ r ∉ p.asIdeal, r • m = 0
-- Mathlib.Data.Fintype.Quotient
/-- Choice-free induction principle for quotients indexed by a `List`.  -/
Quotient.list_ind : ∀ {ι : Type u_1} [DecidableEq ι] {α : ι → Sort u_2} {S : (i : ι) → Setoid (α i)} {l : List ι}
  {C : ((i : ι) → i ∈ l → Quotient (S i)) → Prop},
  (∀ (a : (i : ι) → i ∈ l → α i), C fun x1 x2 => ⟦a x1 x2⟧) → ∀ (q : (i : ι) → i ∈ l → Quotient (S i)), C q