mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.Affine.AddTorsorBases
AffineBasis.centroid_mem_interior_convexHull : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] {ι : Type u_3} [inst_2 : Fintype ι]
  (b : AffineBasis ι ℝ V), Finset.centroid ℝ Finset.univ ⇑b ∈ interior ((convexHull ℝ) (Set.range ⇑b))
-- Lean.Elab.App
Lean.Elab.Term.ElabElim.Context.expectedType : Lean.Elab.Term.ElabElim.Context → Lean.Expr
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Pretrivialization.restrictPreimage'_baseSet : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  (e : Bundle.Pretrivialization F proj) (s : Set B) [inst_2 : Nonempty (↑s → F → ↑(proj ⁻¹' s))],
  (e.restrictPreimage' s).baseSet = Subtype.val ⁻¹' e.baseSet
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.support_induce_subset_coe_preimage : ∀ {V : Type u_1} (G : SimpleGraph V) (s : Set V), (SimpleGraph.induce s G).support ⊆ Subtype.val ⁻¹' s
-- Mathlib.Topology.Maps.Basic
Topology.IsInducing.nhds_eq_comap : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace Y] [inst_1 : TopologicalSpace X],
  Topology.IsInducing f → ∀ (x : X), nhds x = Filter.comap f (nhds (f x))
-- Init.Data.Vector.Lemmas
Vector.flatMap_replicate : ∀ {α : Type u_1} {β : Type u_2} {m n : ℕ} {a : α} {f : α → Vector β m},
  (Vector.replicate n a).flatMap f = (Vector.replicate n (f a)).flatten
-- Mathlib.Topology.Path
/-- Path composition commutes with products  -/
Path.trans_prod_eq_prod_trans : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {a₁ a₂ a₃ : X} {b₁ b₂ b₃ : Y}
  (γ₁ : Path a₁ a₂) (δ₁ : Path a₂ a₃) (γ₂ : Path b₁ b₂) (δ₂ : Path b₂ b₃),
  (γ₁.prod γ₂).trans (δ₁.prod δ₂) = (γ₁.trans δ₁).prod (γ₂.trans δ₂)
-- Mathlib.Algebra.FreeMonoid.Count
FreeAddMonoid.countP'_zero : ∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p], FreeAddMonoid.countP' p 0 = 0
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Finite
/-- `F` creates all finite limits.  -/
CategoryTheory.Limits.CreatesFiniteLimits.createsFiniteLimits : {C : Type u₁} →
  {inst : CategoryTheory.Category.{v₁, u₁} C} →
    {D : Type u₂} →
      {inst_1 : CategoryTheory.Category.{v₂, u₂} D} →
        {F : CategoryTheory.Functor C D} →
          [self : CategoryTheory.Limits.CreatesFiniteLimits F] →
            (J : Type) →
              [inst_2 : CategoryTheory.SmallCategory J] →
                [CategoryTheory.FinCategory J] → CategoryTheory.CreatesLimitsOfShape J F
-- Mathlib.Combinatorics.SimpleGraph.Hall
/-- This is the version of **Hall's marriage theorem** for bipartite graphs that finds a matching
for a single partition given that the neighborhood-condition only holds for elements of that
partition.  -/
SimpleGraph.exists_isMatching_of_forall_ncard_le : ∀ {V : Type u_1} {G : SimpleGraph V} [G.LocallyFinite] {p₁ p₂ : Set V},
  G.IsBipartiteWith p₁ p₂ → (∀ s ⊆ p₁, s.ncard ≤ (⋃ x ∈ s, G.neighborSet x).ncard) → ∃ M, p₁ ⊆ M.verts ∧ M.IsMatching
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.mkBreak : Lean.Syntax → Lean.Elab.Term.Do.CodeBlock
-- Init.Data.UInt.Bitwise
UInt16.ofNatLT_or : ∀ (a b : ℕ) (ha : a < 2 ^ 16) (hb : b < 2 ^ 16),
  UInt16.ofNatLT (a ||| b) ⋯ = UInt16.ofNatLT a ha ||| UInt16.ofNatLT b hb
-- Mathlib.CategoryTheory.Functor.Currying
CategoryTheory.Functor.curryObjCompIso_inv_app_app : ∀ {B : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} B] {C : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} C]
  {D : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} E] (F : CategoryTheory.Functor (C × B) D) (G : CategoryTheory.Functor D E)
  (X : B) (X_1 : C),
  ((F.curryObjCompIso G).inv.app X).app X_1 = CategoryTheory.CategoryStruct.id (G.obj (F.obj (X_1, X)))
-- Mathlib.Order.Filter.Map
Filter.map_mono : ∀ {α : Type u_1} {β : Type u_2} {m : α → β}, Monotone (Filter.map m)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.MonObj.mul_rightUnitor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {M : C} [inst_3 : CategoryTheory.MonObj M],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.tensorμ M (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) M
          (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
        (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.mul
          (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom))
      (CategoryTheory.MonoidalCategoryStruct.rightUnitor M).hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.rightUnitor M).hom
        (CategoryTheory.MonoidalCategoryStruct.rightUnitor M).hom)
      CategoryTheory.MonObj.mul
-- Mathlib.RingTheory.Ideal.Prime
Ideal.IsPrime.one_notMem : ∀ {α : Type u} [inst : Semiring α] {I : Ideal α}, I.IsPrime → 1 ∉ I
-- Mathlib.LinearAlgebra.Span.Defs
/-- `span` forms a Galois insertion with the coercion from submodule to set.  -/
Submodule.gi : (R : Type u_1) →
  (M : Type u_4) →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → GaloisInsertion (Submodule.span R) SetLike.coe
-- Mathlib.RepresentationTheory.Continuous.TopRep
/-- The morphism between invariant submodules induced by a morphism `res φ X ⟶ Y` of
topological `H`-representations, where `φ : H →* G` is a group homomorphism.  -/
TopRep.invariantsResMap : {k : Type u} →
  [inst : TopologicalSpace k] →
    [inst_1 : Ring k] →
      {G : Type u_1} →
        {H : Type u_2} →
          [inst_2 : Group G] →
            [inst_3 : Group H] →
              (φ : H →* G) → {X : TopRep k G} → {Y : TopRep k H} → (TopRep.res φ X ⟶ Y) → (X.invariants ⟶ Y.invariants)
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidHom.mk.injEq : ∀ {α : Type u_6} {β : Type u_7} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : AddZeroClass α]
  [inst_3 : AddZeroClass β] (toAddMonoidHom : α →+ β) (monotone' : Monotone (↑toAddMonoidHom).toFun)
  (toAddMonoidHom_1 : α →+ β) (monotone'_1 : Monotone (↑toAddMonoidHom_1).toFun),
  ({ toAddMonoidHom := toAddMonoidHom, monotone' := monotone' } =
      { toAddMonoidHom := toAddMonoidHom_1, monotone' := monotone'_1 }) =
    (toAddMonoidHom = toAddMonoidHom_1)
-- Batteries.Linter.UnnecessarySeqFocus
/-- Enables the 'unnecessary `<;>`' linter. This will warn whenever the `<;>` tactic combinator
is used when `;` would work.

```
example : True := by apply id <;> trivial
```
The `<;>` is unnecessary here because `apply id` only makes one subgoal.
Prefer `apply id; trivial` instead.

In some cases, the `<;>` is syntactically necessary because a single tactic is expected:
```
example : True := by
  cases () with apply id <;> apply id
  | unit => trivial
```
In this case, you should use parentheses, as in `(apply id; apply id)`:
```
example : True := by
  cases () with (apply id; apply id)
  | unit => trivial
```
 -/
Batteries.Linter.UnnecessarySeqFocus.unnecessarySeqFocusLinter : Lean.Linter
-- Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
cyclotomic_prime_pow_comp_X_add_one_isEisensteinAt : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ),
  ((Polynomial.cyclotomic (p ^ (n + 1)) ℤ).comp (Polynomial.X + 1)).IsEisensteinAt (ℤ ∙ ↑p)
-- Std.Time.Zoned.Database.TzIf
/-- The array of local time type indices corresponding to each transition time.
 -/
Std.Time.TimeZone.TZif.TZifV1.transitionIndices : Std.Time.TimeZone.TZif.TZifV1 → Array UInt8
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.mem_iff_contains : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α},
  k ∈ t ↔ t.contains k = true
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.revMatchAt?_eq_some_iff : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice}
  {startPos endPos : s.Pos},
  String.Slice.Pattern.Model.revMatchAt? pat endPos = some startPos ↔
    String.Slice.Pattern.Model.IsLongestRevMatchAt pat startPos endPos
-- Init.Data.List.Lemmas
List.some_eq_getElem?_iff : ∀ {α : Type u_1} {a : α} {i : ℕ} {l : List α}, some a = l[i]? ↔ ∃ (h : i < l.length), l[i] = a
-- Mathlib.RingTheory.Lasker
/-- The second uniqueness theorem for primary decomposition, Theorem 4.10 in Atiyah-Macdonald.  -/
Submodule.IsMinimalPrimaryDecomposition.comap_localized₀_eq_iInf : ∀ {R : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Submodule R M}
  {t : Finset (Submodule R M)},
  N.IsMinimalPrimaryDecomposition t →
    ∀ (s₀ : Finset ↑N.associatedPrimes),
      IsLowerSet ↑s₀ →
        ∀ s ⊆ t,
          Finset.image (fun q => (q.colon Set.univ).radical) s = Finset.image Subtype.val s₀ →
            Submodule.comap (LocalizedModule.mkLinearMap (⨅ q ∈ s₀, (↑q).primeCompl) M)
                (Submodule.localized₀ (⨅ q ∈ s₀, (↑q).primeCompl)
                  (LocalizedModule.mkLinearMap (⨅ q ∈ s₀, (↑q).primeCompl) M) N) =
              ⨅ q ∈ s, q
-- Mathlib.Algebra.Group.Shrink
Shrink.instCommGroup : {α : Type u_2} → [inst : Small.{v, u_2} α] → [CommGroup α] → CommGroup (Shrink.{v, u_2} α)
-- Mathlib.CategoryTheory.Category.Cat.Adjunction
_private.Mathlib.CategoryTheory.Category.Cat.Adjunction.0.CategoryTheory.Cat.typeToCatObjectsAdjCounitApp : (C : CategoryTheory.Cat) → CategoryTheory.Functor ↑((CategoryTheory.Cat.objects.comp CategoryTheory.typeToCat).obj C) ↑C
-- Mathlib.Algebra.Homology.Localization
/-- The localization functor `HomologicalComplex C c ⥤ HomologicalComplexUpToQuasiIso C c`.  -/
HomologicalComplexUpToQuasiIso.Q : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {ι : Type u_2} →
      {c : ComplexShape ι} →
        [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
          [inst_2 : CategoryTheory.CategoryWithHomology C] →
            [inst_3 : (HomologicalComplex.quasiIso C c).HasLocalization] →
              CategoryTheory.Functor (HomologicalComplex C c) (HomologicalComplexUpToQuasiIso C c)
-- Mathlib.Algebra.Ring.BooleanRing
ofBoolAlg_inf : ∀ {α : Type u_1} [inst : BooleanRing α] (a b : AsBoolAlg α), ofBoolAlg (a ⊓ b) = ofBoolAlg a * ofBoolAlg b
-- Init.Data.String.Basic
ByteArray.utf8Decode?.go.match_1.congr_eq_1 : ∀ (motive : Option Char → Sort u_1) (x : Option Char) (h_1 : x = none → motive none)
  (h_2 : (c : Char) → x = some c → motive (some c)) (heq_1 : x = none),
  (match h : x with
    | none => h_1 h
    | some c => h_2 c h) ≍
    h_1 heq_1
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.length_eq_match_step : ∀ {α β : Type w} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] [inst_2 : Std.IteratorLoop α Id Id]
  [Std.LawfulIteratorLoop α Id Id] {it : Std.Iter β},
  it.length =
    match ↑it.step with
    | Std.IterStep.yield it' out => it'.length + 1
    | Std.IterStep.skip it' => it'.length
    | Std.IterStep.done => 0
-- Lean.Linter.Init
Lean.Linter.LinterOptions.mk.injEq : ∀ (toOptions : Lean.Options) (linterSets : Lean.Linter.LinterSets) (toOptions_1 : Lean.Options)
  (linterSets_1 : Lean.Linter.LinterSets),
  ({ toOptions := toOptions, linterSets := linterSets } = { toOptions := toOptions_1, linterSets := linterSets_1 }) =
    (toOptions = toOptions_1 ∧ linterSets = linterSets_1)
-- Mathlib.Algebra.Category.Semigrp.Basic
Semigrp.hom_ofHom : ∀ {X Y : Type u} [inst : Semigroup X] [inst_1 : Semigroup Y] (f : X →ₙ* Y), Semigrp.Hom.hom (Semigrp.ofHom f) = f
-- Init.Data.List.Lex
List.not_le : ∀ {α : Type u_1} [inst : LT α] {l₁ l₂ : List α}, ¬l₁ ≤ l₂ ↔ l₂ < l₁
-- Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
/-- The two-variable Jacobi theta function is quasi-periodic in `z` with period `τ`.  -/
jacobiTheta₂_add_left' : ∀ (z τ : ℂ), jacobiTheta₂ (z + τ) τ = Complex.exp (-↑Real.pi * Complex.I * (τ + 2 * z)) * jacobiTheta₂ z τ
-- Mathlib.Analysis.Convex.Basic
convex_halfSpace_lt : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] [inst_4 : AddCommMonoid β] [inst_5 : PartialOrder β] [IsOrderedCancelAddMonoid β]
  [inst_7 : Module 𝕜 β] [PosSMulStrictMono 𝕜 β] {f : E → β}, IsLinearMap 𝕜 f → ∀ (r : β), Convex 𝕜 {w | f w < r}
-- Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
/-- Two sections `s` and `t` are equal at `x` if and only if their coefficients w.r.t. some local
frame at `x` agree.  -/
IsLocalFrameOn.eq_iff_coeff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → AddCommGroup (V x)] [inst_10 : (x : M) → Module 𝕜 (V x)]
  [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : FiberBundle F V] {ι : Type u_7} {s : ι → (x : M) → V x}
  {u : Set M} {n : WithTop ℕ∞} {x : M} {t t' : (x : M) → V x} [VectorBundle 𝕜 F V] [FiniteDimensional 𝕜 F]
  (hs : IsLocalFrameOn I F n s u), x ∈ u → (t x = t' x ↔ ∀ (i : ι), (hs.coeff i x) (t x) = (hs.coeff i x) (t' x))
-- Mathlib.CategoryTheory.Triangulated.Functor
CategoryTheory.Functor.instCommShiftTriangleMapTriangleInt : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        [inst_2 : CategoryTheory.HasShift C ℤ] →
          [inst_3 : CategoryTheory.HasShift D ℤ] →
            (F : CategoryTheory.Functor C D) →
              [inst_4 : F.CommShift ℤ] →
                [inst_5 : CategoryTheory.Preadditive C] →
                  [inst_6 : CategoryTheory.Preadditive D] →
                    [F.Additive] →
                      [inst_8 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
                        [inst_9 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] → F.mapTriangle.CommShift ℤ
-- Lean.Util.ParamMinimizer
/-- Result type for the parameter minimizer.
 -/
Lean.Util.ParamMinimizer.Result : Type
-- Mathlib.Topology.Order
/-- Construct a topology on α given the filter of neighborhoods of each point of α.  -/
TopologicalSpace.mkOfNhds : {α : Type u} → (α → Filter α) → TopologicalSpace α
-- Mathlib.Data.Nat.Init
_private.Mathlib.Data.Nat.Init.0.Nat.leRec.match_1.splitter : {n : ℕ} →
  (motive : (x : ℕ) → n ≤ x → Sort u_1) →
    (x : ℕ) → (x_1 : n ≤ x) → ((H : n ≤ 0) → motive 0 H) → ((m : ℕ) → (H : n ≤ m + 1) → motive m.succ H) → motive x x_1
-- Mathlib.NumberTheory.NumberField.Basic
NumberField.of_subfield : ∀ {K : Type u_1} [inst : Field K] [NumberField K] (E : Subfield K), NumberField ↥E
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
/-- A `LazyEntry` represents a snapshot of the computation of encoding an `Expr` as `Array Key`.
This is used for computing the keys one by one.  -/
Lean.Meta.RefinedDiscrTree.LazyEntry : Type
-- Mathlib.Algebra.Module.Submodule.LinearMap
LinearMap.restrict_apply : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  {f : M →ₛₗ[σ₁₂] M₂} {p : Submodule R M} {q : Submodule R₂ M₂} (hf : ∀ x ∈ p, f x ∈ q) (x : ↥p),
  (f.restrict hf) x = ⟨f ↑x, ⋯⟩
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.instVAdd : {α : Type u_1} →
  {β : Type u_2} → [inst : MeasurableSpace α] → {K : Type u_5} → [VAdd K β] → VAdd K (MeasureTheory.SimpleFunc α β)
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.IsRankLeOne.nonempty : ∀ {R : Type u_1} {inst : Semiring R} {inst_1 : ValuativeRel R} [self : ValuativeRel.IsRankLeOne R],
  Nonempty (ValuativeRel.RankLeOneStruct R)
-- Mathlib.Algebra.Order.Ring.Archimedean
_private.Mathlib.Algebra.Order.Ring.Archimedean.0.ArchimedeanClass.add_assoc' : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : CommRing R] [inst_2 : IsStrictOrderedRing R]
  (x y z : ArchimedeanClass R), x + y + z = x + (y + z)
-- Lean.Data.Lsp.Internal
Lean.Lsp.instForInModuleRefsProdRefIdentRefInfoOfMonad : {m : Type u_1 → Type u_2} → [Monad m] → ForIn m Lean.Lsp.ModuleRefs (Lean.Lsp.RefIdent × Lean.Lsp.RefInfo)
-- Init.Prelude
Lean.Macro.MethodsRef : Type
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.contains_congr : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k k' : α}, cmp k k' = Ordering.eq → t.contains k = t.contains k'
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.maxKey?_eq_some_maxKeyD : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t ≠ ∅ → ∀ {fallback : α}, t.maxKey? = some (t.maxKeyD fallback)
-- Mathlib.Combinatorics.Matroid.Minor.Delete
Matroid.IsRestriction.isRestriction_deleteElem : ∀ {α : Type u_1} {M N : Matroid α} {e : α}, N.IsRestriction M → e ∉ N.E → N.IsRestriction (M.delete {e})
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometry.coe_pow : ∀ {R : Type u_1} {E : Type u_5} [inst : Semiring R] [inst_1 : SeminormedAddCommGroup E] [inst_2 : Module R E]
  (f : E →ₗᵢ[R] E) (n : ℕ), ⇑(f ^ n) = (⇑f)^[n]
-- Mathlib.RingTheory.Valuation.Basic
Valuation.isEquiv_tfae : ∀ {K : Type u_1} [inst : DivisionRing K] {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [inst_1 : LinearOrderedCommGroupWithZero Γ₀]
  [inst_2 : LinearOrderedCommGroupWithZero Γ'₀] (v : Valuation K Γ₀) (v' : Valuation K Γ'₀),
  [v.IsEquiv v', ∀ {x y : K}, v x < v y ↔ v' x < v' y, ∀ {x : K}, v x ≤ 1 ↔ v' x ≤ 1, ∀ {x : K}, v x = 1 ↔ v' x = 1,
      ∀ {x : K}, v x < 1 ↔ v' x < 1, ∀ {x : K}, v (x - 1) < 1 ↔ v' (x - 1) < 1].TFAE
-- Mathlib.FieldTheory.RatFunc.Valuation
RatFunc.CompletionAtInfty.instInhabited : (F : Type u_1) → [inst : Field F] → [inst_1 : DecidableEq (RatFunc F)] → Inhabited (RatFunc.CompletionAtInfty F)
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
/-- The category structure on `∫ F`.  -/
CategoryTheory.Pseudofunctor.Grothendieck.category : {𝒮 : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
    {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮) CategoryTheory.Cat} →
      CategoryTheory.Category.{max v₁ v₂, max u₂ u₁} F.Grothendieck
-- Init.Control.Lawful.Instances
OptionT.lift_pure : ∀ {m : Type u → Type u_1} [inst : Monad m] [LawfulMonad m] {α : Type u} (a : α), OptionT.lift (pure a) = pure a
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get_filter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {f : (a : α) → β a → Bool} {k : α} {h' : k ∈ Std.DTreeMap.filter f t},
  (Std.DTreeMap.filter f t).get k h' = t.get k ⋯
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.map_zero : ∀ {Γ : Type u_1} {R : Type u_3} {S : Type u_4} [inst : PartialOrder Γ] [inst_1 : Zero R] [inst_2 : Zero S]
  (f : ZeroHom R S), HahnSeries.map 0 f = 0
-- Lean.Meta.CoeAttr
/-- The type of coercion  -/
Lean.Meta.CoeFnInfo.type : Lean.Meta.CoeFnInfo → Lean.Meta.CoeFnType
-- Mathlib.Algebra.Group.Commute.Basic
AddCommute.function_commute_add_right : ∀ {G : Type u_1} [inst : AddSemigroup G] {a b : G}, AddCommute a b → Function.Commute (fun x => x + a) fun x => x + b
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem?_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : BEq α]
  [Std.LawfulBEqCmp cmp] {l : List (α × β)} {k : α},
  (List.map Prod.fst l).contains k = false → (t.insertMany l)[k]? = t[k]?
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.CoordinateRing.smul : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Affine R} (x : Polynomial R) (y : W'.CoordinateRing),
  x • y = (WeierstrassCurve.Affine.CoordinateRing.mk W') (Polynomial.C x) * y
-- Mathlib.Analysis.Calculus.FDeriv.Star
HasStrictFDerivAt.star : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : StarRing 𝕜] {E : Type u_2} [inst_2 : NormedAddCommGroup E]
  [inst_3 : NormedSpace 𝕜 E] {F : Type u_3} [inst_4 : NormedAddCommGroup F] [inst_5 : StarAddMonoid F]
  [inst_6 : NormedSpace 𝕜 F] [inst_7 : StarModule 𝕜 F] [inst_8 : ContinuousStar F] {f : E → F} {f' : E →L[𝕜] F} {x : E}
  [inst_9 : TrivialStar 𝕜], HasStrictFDerivAt f f' x → HasStrictFDerivAt (fun x => star (f x)) (↑(starL' 𝕜) ∘SL f') x
-- Lean.Elab.Quotation
Lean.Elab.Term.Quotation.stxQuot.expand : Lean.Syntax → Lean.Elab.TermElabM Lean.Syntax
-- Std.Internal.Do.Triple.SpecLemmas
/-- The type of loop invariants used by the specifications of `for ... in ...` loops over string slices.
A loop invariant is a function mapping the current position and state to a lattice element.
 -/
Std.Internal.Do.StringSliceInvariant : String.Slice → Type u → Type u → Type u
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
/-- the underlying morphism induces a local ring homomorphism on stalks  -/
AlgebraicGeometry.LocallyRingedSpace.Hom.prop : ∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (self : X.Hom Y) (x : ↑↑X.toPresheafedSpace),
  IsLocalHom (CommRingCat.Hom.hom (self.stalkMap x))
-- Mathlib.MeasureTheory.Integral.SetToL1
/-- Extend `Set α → (E →L[ℝ] F)` to `(α →₁[μ] E) →L[𝕜] F`.  -/
MeasureTheory.L1.setToL1' : {α : Type u_1} →
  {E : Type u_2} →
    {F : Type u_3} →
      (𝕜 : Type u_6) →
        [inst : NormedAddCommGroup E] →
          [inst_1 : NormedSpace ℝ E] →
            [inst_2 : NormedAddCommGroup F] →
              [inst_3 : NormedSpace ℝ F] →
                {m : MeasurableSpace α} →
                  {μ : MeasureTheory.Measure α} →
                    [inst_4 : NormedRing 𝕜] →
                      [inst_5 : Module 𝕜 E] →
                        [inst_6 : Module 𝕜 F] →
                          [inst_7 : IsBoundedSMul 𝕜 E] →
                            [IsBoundedSMul 𝕜 F] →
                              [CompleteSpace F] →
                                {T : Set α → E →L[ℝ] F} →
                                  {C : ℝ} →
                                    MeasureTheory.DominatedFinMeasAdditive μ T C →
                                      (∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x) →
                                        ↥(MeasureTheory.Lp E 1 μ) →L[𝕜] F
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.BinaryCofan.ext_hom_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A B : C} {c c' : CategoryTheory.Limits.BinaryCofan A B}
  (e : c.pt ≅ c'.pt) (h₁ : CategoryTheory.CategoryStruct.comp c.inl e.hom = c'.inl)
  (h₂ : CategoryTheory.CategoryStruct.comp c.inr e.hom = c'.inr),
  (CategoryTheory.Limits.BinaryCofan.ext e h₁ h₂).hom.hom = e.hom
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.setToFun_mono_left : ∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {G'' : Type u_8} [inst_2 : NormedAddCommGroup G''] [inst_3 : PartialOrder G'']
  [IsOrderedAddMonoid G''] [inst_5 : NormedSpace ℝ G''] [OrderClosedTopology G''] {T T' : Set α → E →L[ℝ] G''}
  {C C' : ℝ} (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) (hT' : MeasureTheory.DominatedFinMeasAdditive μ T' C'),
  (∀ (s : Set α) (x : E), (T s) x ≤ (T' s) x) →
    ∀ (f : ↥(MeasureTheory.Lp E 1 μ)), MeasureTheory.setToFun μ T hT ↑↑f ≤ MeasureTheory.setToFun μ T' hT' ↑↑f
-- Mathlib.Order.DirectedInverseSystem
InverseSystem.piLTProj_intro : ∀ {ι : Type u_1} [inst : Preorder ι] {X : ι → Type u_5} ⦃i j : ι⦄ (h : i ≤ j) {l : ↑(Set.Iio j)}
  {f : InverseSystem.piLT X j} (hl : ↑l < i), f l = InverseSystem.piLTProj h f ⟨↑l, hl⟩
-- Mathlib.Analysis.Normed.Group.Defs
/-- Construct a seminormed group from a multiplication-invariant distance.  -/
SeminormedGroup.ofMulDist : {E : Type u_5} →
  [inst : Norm E] →
    [inst_1 : Group E] →
      [inst_2 : PseudoMetricSpace E] →
        (∀ (x : E), ‖x‖ = dist 1 x) → (∀ (x y z : E), dist x y ≤ dist (z * x) (z * y)) → SeminormedGroup E