mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.ModularForms.Basic
/-- **Alias** of `FunLike.coe_sub`. -/
ModularForm.coe_sub : ∀ {F : Type u_3} {α : Type u_5} {β : Type u_6} [inst : FunLike F α β] [inst_1 : Sub F] [inst_2 : Sub β]
  [IsSubApply F α β] (f g : F), ⇑(f - g) = ⇑f - ⇑g
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
/-- A point is in the affine span of a single point if and only if they are equal.  -/
AffineSubspace.mem_affineSpan_singleton : ∀ (k : Type u_1) (V : Type u_2) {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] {p₁ p₂ : P}, p₁ ∈ affineSpan k {p₂} ↔ p₁ = p₂
-- Mathlib.CategoryTheory.Sites.Point.Monoidal
CategoryTheory.GrothendieckTopology.Point.instPreservesColimitsOfShapeOppositeElementsFiberObjFunctorCurriedTensor : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point)
  {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A] [inst_2 : CategoryTheory.MonoidalCategory A]
  [CategoryTheory.LocallySmall.{w, v, u} C]
  [∀ (X : A),
      CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'}
        (CategoryTheory.MonoidalCategory.tensorLeft X)]
  (M : A),
  CategoryTheory.Limits.PreservesColimitsOfShape Φ.fiber.Elementsᵒᵖ
    ((CategoryTheory.MonoidalCategory.curriedTensor A).obj M)
-- Mathlib.Order.SymmDiff
symmDiff_triangle : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] (a b c : α), symmDiff a c ≤ symmDiff a b ⊔ symmDiff b c
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
/-- All supported binary operations on `BVExpr`.
 -/
Std.Tactic.BVDecide.BVBinOp : Type
-- Mathlib.Topology.MetricSpace.Lipschitz
LipschitzWith.nndist_le : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {K : NNReal} {f : α → β},
  LipschitzWith K f → ∀ (x y : α), nndist (f x) (f y) ≤ K * nndist x y
-- Init.Data.SInt.Lemmas
Int16.toInt_ofIntTruncate : ∀ {x : ℤ}, Int16.minValue.toInt ≤ x → x ≤ Int16.maxValue.toInt → (Int16.ofIntClamp x).toInt = x
-- Mathlib.Data.Real.ConjExponents
NNReal.HolderTriple.inv_lt_inv : ∀ {p q r : NNReal}, p.HolderTriple q r → p⁻¹ < r⁻¹
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
exists_of_linearIndepOn_of_finite_span : ∀ {K : Type u_3} {V : Type u} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {s : Set V}
  {t : Finset V}, LinearIndepOn K id s → s ⊆ ↑(Submodule.span K ↑t) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ t'.card = t.card
-- Mathlib.GroupTheory.Subgroup.Centralizer
Subgroup.normal_subgroupOf_centralizer_normalizer : ∀ {G : Type u_1} [inst : Group G] (s : Set G), ((Subgroup.centralizer s).subgroupOf (Subgroup.normalizer s)).Normal
-- Mathlib.Topology.Order.Hom.Esakia
EsakiaHom.ext : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : Preorder α] [inst_2 : TopologicalSpace β]
  [inst_3 : Preorder β] {f g : EsakiaHom α β}, (∀ (a : α), f a = g a) → f = g
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.Term.instDecidableEq : {L : FirstOrder.Language} →
  {α : Type u'} → [DecidableEq α] → [(n : ℕ) → DecidableEq (L.Functions n)] → DecidableEq (L.Term α)
-- Mathlib.MeasureTheory.Constructions.Pi
IsUnifLocDoublingMeasure.pi : ∀ {ι : Type u_4} [inst : Fintype ι] {X : ι → Type u_5} [inst_1 : (i : ι) → PseudoMetricSpace (X i)]
  [inst_2 : (i : ι) → MeasurableSpace (X i)] (μ : (i : ι) → MeasureTheory.Measure (X i))
  [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)] [∀ (i : ι), IsUnifLocDoublingMeasure (μ i)],
  IsUnifLocDoublingMeasure (MeasureTheory.Measure.pi μ)
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.isOrderedRing : IsOrderedRing Cardinal.{u}
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey_filter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [inst : Std.TransCmp cmp]
  {f : α → β → Bool} {k : α} (h : t.WF) {h' : k ∈ Std.TreeMap.Raw.filter f t},
  (Std.TreeMap.Raw.filter f t).getKey k h' = t.getKey k ⋯
-- Mathlib.Algebra.Order.Group.Lattice
inf_mul_sup : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : CommGroup α] [MulLeftMono α] (a b : α), (a ⊓ b) * (a ⊔ b) = a * b
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Functor.IsCoverDense.sheafHom.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {K : CategoryTheory.GrothendieckTopology D} {A : Type u_4}
  [inst_2 : CategoryTheory.Category.{v_4, u_4} A] {G : CategoryTheory.Functor C D} [inst_3 : G.IsCoverDense K]
  [inst_4 : G.IsLocallyFull K] {ℱ : CategoryTheory.Functor Dᵒᵖ A} {ℱ' : CategoryTheory.Sheaf K A}
  (α : G.op.comp ℱ ⟶ G.op.comp ℱ'.obj),
  CategoryTheory.Functor.IsCoverDense.sheafHom α =
    { app := fun X => CategoryTheory.yoneda.preimage ((CategoryTheory.Functor.IsCoverDense.sheafYonedaHom α).app X),
      naturality := ⋯ }
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.compAddMonoidHom'.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {γ : Type u_3}
  [inst_2 : TopologicalSpace γ] [inst_3 : AddZeroClass γ] [inst_4 : ContinuousAdd γ] (g : C(α, β)),
  g.compAddMonoidHom' = { toFun := fun f => f.comp g, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.Algebra.Category.Ring.Constructions
/-- In the category of `CommRingCat`, the pullback of `f : A ⟶ C` and `g : B ⟶ C` is the `eqLocus`
of the two maps `A × B ⟶ C`. This is the constructed pullback cone.
 -/
CommRingCat.pullbackCone : {A B C : CommRingCat} → (f : A ⟶ C) → (g : B ⟶ C) → CategoryTheory.Limits.PullbackCone f g
-- Mathlib.Algebra.Group.TypeTags.Basic
Additive.ofMul_symm_eq : ∀ {α : Type u}, Additive.ofMul.symm = Additive.toMul
-- Mathlib.RingTheory.FreeRing
FreeRing.lift_of : ∀ {α : Type u} {R : Type v} [inst : Ring R] (f : α → R) (x : α), (FreeRing.lift f) (FreeRing.of x) = f x
-- Mathlib.AlgebraicGeometry.Limits
AlgebraicGeometry.instIsOverTerminalScheme : ∀ {X Y : AlgebraicGeometry.Scheme} [inst : X.Over (⊤_ AlgebraicGeometry.Scheme)]
  [inst_1 : Y.Over (⊤_ AlgebraicGeometry.Scheme)] (f : X ⟶ Y),
  AlgebraicGeometry.Scheme.Hom.IsOver f (⊤_ AlgebraicGeometry.Scheme)
-- Mathlib.Algebra.Order.Field.Basic
one_lt_one_div : ∀ {α : Type u_2} [inst : Semifield α] [inst_1 : PartialOrder α] [PosMulReflectLT α] {a : α} [IsStrictOrderedRing α],
  0 < a → a < 1 → 1 < 1 / a
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric
ModuleCat.MonoidalCategory.instBraidedCategory : {R : Type u} → [inst : CommRing R] → CategoryTheory.BraidedCategory (ModuleCat R)
-- Mathlib.Algebra.Module.ZMod
Submodule.toAddSubgroup_toZModSubmodule : ∀ (n : ℕ) {M : Type u_1} [inst : AddCommGroup M] [inst_1 : Module (ZMod n) M] (S : Submodule (ZMod n) M),
  (AddSubgroup.toZModSubmodule n) S.toAddSubgroup = S
-- Std.Http.Data.Extensions
/-- Removes the value of type `α` from the extensions.
 -/
Std.Http.Extensions.remove : Std.Http.Extensions → (α : Type) → [TypeName α] → Std.Http.Extensions
-- Mathlib.Analysis.Normed.Module.MStructure
IsLprojection.compl_mul : ∀ {X : Type u_1} [inst : NormedAddCommGroup X] {M : Type u_2} [inst_1 : Ring M] [inst_2 : Module M X]
  {P : { P // IsLprojection X P }} {Q : M}, ↑Pᶜ * Q = Q - ↑P * Q
-- Lean.Parser.Do
Lean.Parser.Term.doMatchExprAlts.formatter : Lean.PrettyPrinter.Formatter
-- Std.Do.PostCond
Std.Do.PostShape.except.inj : ∀ {ε : Type u} {a : Std.Do.PostShape} {ε_1 : Type u} {a_1 : Std.Do.PostShape},
  Std.Do.PostShape.except ε a = Std.Do.PostShape.except ε_1 a_1 → ε = ε_1 ∧ a = a_1
-- Std.Http.Data.URI.Encoding
/-- Converts a byte to its percent-encoded hexadecimal representation (%XX). For example, a space
character (0x20) becomes "%20".
 -/
_private.Std.Http.Data.URI.Encoding.0.Std.Http.URI.EncodedString.byteToHex : {r : UInt8 → Bool} → UInt8 → Std.Http.URI.EncodedString r → Std.Http.URI.EncodedString r
-- Mathlib.Algebra.Category.Ring.Topology
/-- `Hom(B ⊗[A] C, R)` has the subspace topology from `Hom(B, R) × Hom(C, R)`.  -/
CommRingCat.HomTopology.isEmbedding_pushout : ∀ {R A B C : CommRingCat} [inst : TopologicalSpace ↑R] [IsTopologicalRing ↑R] (φ : A ⟶ B) (ψ : A ⟶ C),
  Topology.IsEmbedding fun f =>
    (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl φ ψ) f,
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr φ ψ) f)
-- Mathlib.LinearAlgebra.Basis.Flag
Module.Basis.flag_mono : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {n : ℕ}
  (b : Module.Basis (Fin n) R M), Monotone b.flag
-- Std.Data.TreeMap.Raw.Basic
/-- Tries to retrieve the smallest key that is greater than the given key,
returning `fallback` if no such key exists.
 -/
Std.TreeMap.Raw.getKeyGTD : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap.Raw α β cmp → α → α → α
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.getEntryGE?_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp] {k : α},
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.getEntryGE? k = t₂.getEntryGE? k
-- Std.Tactic.BVDecide.Normalize.Bool
Std.Tactic.BVDecide.Normalize.BitVec.zero_beq_eq_ite' : ∀ {b : Bool} {a : BitVec 1}, (b == (0#1 == a)) = (a == bif b then 0#1 else 1#1)
-- Init.Data.Iterators.PostconditionMonad
Std.Iterators.PostconditionT.bind_assoc : ∀ {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m] {α β γ : Type w} {x : Std.Iterators.PostconditionT m α}
  {f : α → Std.Iterators.PostconditionT m β} {g : β → Std.Iterators.PostconditionT m γ},
  (x.bind f).bind g = x.bind fun a => (f a).bind g
-- Mathlib.Algebra.Group.Submonoid.Units
AddSubmonoid.val_neg_addUnitsEquivAddUnitsType_symm_apply_coe : ∀ {M : Type u_1} [inst : AddMonoid M] (S : AddSubmonoid M) (x : AddUnits ↥S),
  ↑(-↑(S.addUnitsEquivAddUnitsType.symm x)) = ↑↑(-x)
-- Mathlib.Algebra.Category.FGModuleCat.Basic
FGModuleCat.exactPairing : (K : Type u) → [inst : Field K] → (V : FGModuleCat K) → CategoryTheory.ExactPairing V (FGModuleCat.FGModuleCatDual K V)
-- Init.Data.BitVec.Bitblast
_private.Init.Data.BitVec.Bitblast.0.BitVec.extractLsb'_addRecAux_of_le : ∀ {len w r k : ℕ} {x : BitVec (len * w)},
  r ≤ k → BitVec.addRecAux✝ (BitVec.extractLsb' 0 (k * w) x) r 0#w = BitVec.addRecAux✝ x r 0#w
-- Mathlib.Analysis.Meromorphic.Divisor
/-- If `f` is meromorphic, then the divisor of `f ^ n` is `n` times the divisor of `f`.
 -/
MeromorphicOn.divisor_fun_pow : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {U : Set 𝕜} {f : 𝕜 → 𝕜},
  MeromorphicOn f U → ∀ (n : ℕ), MeromorphicOn.divisor (fun z => f z ^ n) U = n • MeromorphicOn.divisor f U
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Polynomial.sub_one_pow_totient_le_cyclotomic_eval : ∀ {q : ℝ}, 1 < q → ∀ (n : ℕ), (q - 1) ^ n.totient ≤ Polynomial.eval q (Polynomial.cyclotomic n ℝ)
-- Mathlib.Algebra.Homology.Opposite
/-- Auxiliary definition for `opEquivalence`.  -/
HomologicalComplex.opUnitIso : {ι : Type u_1} →
  (V : Type u_2) →
    [inst : CategoryTheory.Category.{v_1, u_2} V] →
      (c : ComplexShape ι) →
        [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
          CategoryTheory.Functor.id (HomologicalComplex V c)ᵒᵖ ≅
            (HomologicalComplex.opFunctor V c).comp (HomologicalComplex.opInverse V c)
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.hasColimitsOfSize : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} [CategoryTheory.Limits.HasCoproducts C]
  [CategoryTheory.Limits.HasStrongEpiMonoFactorisations C],
  CategoryTheory.Limits.HasColimitsOfSize.{w, w', max u₁ v₁, max u₁ v₁} (CategoryTheory.Subobject X)
-- Mathlib.Algebra.Ring.GeomSum
RingHom.map_geom_sum₂ : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : Semiring S] (x y : R) (n : ℕ) (f : R →+* S),
  f (∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i)) = ∑ i ∈ Finset.range n, f x ^ i * f y ^ (n - 1 - i)
-- Mathlib.GroupTheory.Descent
/-- If `G` is a commutative additive group and `n : ℕ`, `h : G → ℝ` satisfy
* `G / 2 • G` is finite,
* `0 ≤ h x` for all `x : G`,
* there is `C : ℝ` such that for all `x y : G`, `|h (x + y) + h(x - y) - 2 * (h x + h y)| ≤ C`,
* for all `B : ℝ`, there are only finitely many `x : G` such that `h x ≤ B`,

then `G` is finitely generated.  -/
AddCommGroup.fg_of_descent' : ∀ {G : Type u_1} [inst : AddCommGroup G] {h : G → ℝ} {C : ℝ},
  (nsmulAddMonoidHom 2).range.FiniteIndex →
    (∀ (x : G), 0 ≤ h x) → (∀ (x y : G), |h (x + y) + h (x - y) - 2 * (h x + h y)| ≤ C) → ∀ [Northcott h], AddGroup.FG G
-- Lean.Meta.IntInstTesters
Lean.Meta.DefEq.isInstHMulInt : Lean.Expr → Lean.MetaM Bool
-- Mathlib.Topology.UniformSpace.Closeds
/-- When `Set` is equipped with the Hausdorff uniformity, taking the image under a uniform
inducing map is uniform inducing.  -/
IsUniformInducing.image_hausdorff : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : UniformSpace β] {f : α → β},
  IsUniformInducing f → IsUniformInducing fun x => f '' x
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.insertMany_nil : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β}, m.insertMany [] = m
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKeyD_filter_not_contains_map_fst : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)} {k fallback : α},
  Std.Internal.List.DistinctKeys l₁ →
    Std.Internal.List.getKeyD k (List.filter (fun p => !(List.map Sigma.fst l₂).contains p.fst) l₁) fallback =
      if Std.Internal.List.containsKey k l₂ = true then fallback else Std.Internal.List.getKeyD k l₁ fallback
-- Mathlib.Tactic.GRewrite.Core
Mathlib.Tactic.GRewrite.GRewriteResult.mk.injEq : ∀ (eNew impProof : Lean.Expr) (mvarIds : List Lean.MVarId) (lctx? : Option Lean.LocalContext)
  (eNew_1 impProof_1 : Lean.Expr) (mvarIds_1 : List Lean.MVarId) (lctx?_1 : Option Lean.LocalContext),
  ({ eNew := eNew, impProof := impProof, mvarIds := mvarIds, lctx? := lctx? } =
      { eNew := eNew_1, impProof := impProof_1, mvarIds := mvarIds_1, lctx? := lctx?_1 }) =
    (eNew = eNew_1 ∧ impProof = impProof_1 ∧ mvarIds = mvarIds_1 ∧ lctx? = lctx?_1)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonFoldingRangeParams.fromJson : Lean.Json → Except String Lean.Lsp.FoldingRangeParams
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.StructuredArrow.ofCommaSndEquivalenceFunctor_obj_left : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T)
  (G : CategoryTheory.Functor D T) (c : C) (X : CategoryTheory.StructuredArrow c (CategoryTheory.Comma.fst F G)),
  ((CategoryTheory.StructuredArrow.ofCommaSndEquivalenceFunctor F G c).obj X).left = CategoryTheory.Under.mk X.hom
-- Mathlib.Topology.Algebra.Module.Complement
Submodule.projectionL_eq_self_sub_projectionL : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {p q : Submodule R M} [inst_4 : ContinuousSub M] (h : Submodule.IsTopCompl p q) (x : M),
  (q.projectionL p ⋯) x = x - (p.projectionL q h) x
-- Mathlib.RingTheory.Finiteness.Cofinite
/-- **Alias** of `Submodule.CoFG.of_le`.

---

A submodule that contains a CoFG submodule is CoFG.  -/
Submodule.CoFG.cofg_of_le : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {S T : Submodule R M},
  S ≤ T → S.CoFG → T.CoFG
-- Mathlib.CategoryTheory.Localization.Resolution
CategoryTheory.LocalizerMorphism.RightResolution.unopFunctor_obj : ∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) (X₂ : C₂ᵒᵖ)
  (R : (Φ.op.RightResolution X₂)ᵒᵖ),
  (CategoryTheory.LocalizerMorphism.RightResolution.unopFunctor Φ X₂).obj R = (Opposite.unop R).unop
-- Std.Http.Transport
/-- Mock server endpoint for testing.
 -/
Std.Http.Internal.Mock.Server : Type
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.haar.addCHaar_sup_eq : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalAddGroup G]
  {K₀ : TopologicalSpace.PositiveCompacts G} {K₁ K₂ : TopologicalSpace.Compacts G},
  Disjoint K₁.carrier K₂.carrier →
    IsClosed K₂.carrier →
      MeasureTheory.Measure.haar.addCHaar K₀ (K₁ ⊔ K₂) =
        MeasureTheory.Measure.haar.addCHaar K₀ K₁ + MeasureTheory.Measure.haar.addCHaar K₀ K₂
-- Mathlib.Order.FixedPoints
OrderHom.gfp_const_inf_le : ∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α) (x : α), OrderHom.gfp ((OrderHom.const α) x ⊓ f) ≤ x
-- Init.Data.Range.Polymorphic.RangeIterator
_private.Init.Data.Range.Polymorphic.RangeIterator.0.Std.Rxo.Iterator.instIteratorLoop.loopWf_eq : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LT α] [inst_2 : DecidableLT α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerableLT α] {n : Type u → Type w}
  [inst_5 : Monad n] [LawfulMonad n] (γ : Type u) {lift : (γ δ : Type u) → (γ → n δ) → Id γ → n δ}
  [instLawfulMonadLiftFunction : Std.Internal.LawfulMonadLiftBindFunction lift] (Pl : α → γ → ForInStep γ → Prop)
  (wf : Std.IteratorLoop.WellFounded (Std.Rxo.Iterator α) Id Pl) (LargeEnough : α → Prop)
  (hl : ∀ (a b : α), Std.PRange.UpwardEnumerable.LE a b → LargeEnough a → LargeEnough b) (upperBound : α) (acc : γ)
  (next : α) (h : LargeEnough next)
  (f : (out : α) → LargeEnough out → out < upperBound → (c : γ) → n { s // Pl out c s }),
  Std.Rxo.Iterator.instIteratorLoop.loop.wf✝ γ Pl wf LargeEnough hl upperBound acc next h f =
    if hu : next < upperBound then do
      let __do_lift ← f next h hu acc
      match __do_lift with
        | ⟨ForInStep.yield acc', property⟩ =>
          Std.IterM.DefaultConsumers.forIn' lift γ Pl
            { internalState := { next := Std.PRange.succ? next, upperBound := upperBound } } acc'
            { internalState := { next := Std.PRange.succ? next, upperBound := upperBound } }.IsPlausibleIndirectOutput ⋯
            fun next' h_1 acc' => f next' ⋯ ⋯ acc'
        | ⟨ForInStep.done acc', property⟩ => pure acc'
    else pure acc
-- Mathlib.AlgebraicGeometry.Morphisms.Preimmersion
AlgebraicGeometry.IsPreimmersion.of_isLocalization : ∀ {R S : Type u} [inst : CommRing R] (M : Submonoid R) [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [IsLocalization M S],
  AlgebraicGeometry.IsPreimmersion (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R S)))
-- Mathlib.Analysis.ODE.Gronwall
hasDerivAt_gronwallBound_shift : ∀ (δ K ε x a : ℝ), HasDerivAt (fun y => gronwallBound δ K ε (y - a)) (K * gronwallBound δ K ε (x - a) + ε) x
-- Mathlib.CategoryTheory.Action.Limits
Action.instHasZeroMorphisms : {V : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    {G : Type u_2} →
      [inst_1 : Monoid G] →
        [CategoryTheory.Limits.HasZeroMorphisms V] → CategoryTheory.Limits.HasZeroMorphisms (Action V G)
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
ExteriorAlgebra.map_id : ∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  ExteriorAlgebra.map LinearMap.id = AlgHom.id R (ExteriorAlgebra R M)
-- Mathlib.Analysis.BoxIntegral.Box.Basic
BoxIntegral.Box.isBounded_Icc : ∀ {ι : Type u_1} [Finite ι] (I : BoxIntegral.Box ι), Bornology.IsBounded (BoxIntegral.Box.Icc I)
-- Mathlib.Topology.MetricSpace.Gluing
_private.Mathlib.Topology.MetricSpace.Gluing.0.Metric.Sigma.dist.match_1.splitter : {ι : Type u_1} →
  {E : ι → Type u_2} →
    (motive : (i : ι) × E i → (i : ι) × E i → Sort u_3) →
      (x x_1 : (i : ι) × E i) → ((i : ι) → (x : E i) → (j : ι) → (y : E j) → motive ⟨i, x⟩ ⟨j, y⟩) → motive x x_1
-- Mathlib.Analysis.LocallyConvex.Polar
/-- Given a subset `s` in a monoid `M` (over a field `𝕜`) closed under scalar multiplication,
the polar `polarSubmodule 𝕜 s` is the submodule of `StrongDual 𝕜 M` consisting of those functionals
which evaluate to zero at all points `z ∈ s`.  -/
StrongDual.polarSubmodule : (𝕜 : Type u_4) →
  [inst : NontriviallyNormedField 𝕜] →
    {M : Type u_5} →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : TopologicalSpace M] →
          [inst_3 : Module 𝕜 M] →
            {S : Type u_6} → [inst_4 : SetLike S M] → [SMulMemClass S 𝕜 M] → S → Submodule 𝕜 (StrongDual 𝕜 M)
-- Mathlib.AlgebraicGeometry.Modules.Tilde
/-- The tilde functor is fully faithful. We will later show that the essential image is
exactly quasi-coherent modules.  -/
AlgebraicGeometry.tilde.fullyFaithfulFunctor : {R : CommRingCat} → (AlgebraicGeometry.tilde.functor R).FullyFaithful
-- Mathlib.GroupTheory.Perm.MaximalSubgroups
Equiv.Perm.exists_mem_stabilizer_smul_eq : ∀ {α : Type u_2} {s : Set α}, ∀ a ∈ s, ∀ b ∈ s, ∃ g ∈ MulAction.stabilizer (Equiv.Perm α) s, g • a = b
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
LinearMap.compQuadraticMap_apply : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} {P : Type u_6} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : AddCommMonoid N] [inst_4 : Module R N] [inst_5 : AddCommMonoid P]
  [inst_6 : Module R P] (f : N →ₗ[R] P) (Q : QuadraticMap R M N) (x : M), (f.compQuadraticMap Q) x = f (Q x)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CallHierarchyIncomingCall : Type
-- Qq.MetaM
Qq.withLocalDeclDQ : {n : Type → Type u_1} →
  {u : Lean.Level} →
    {α : Type} → [Monad n] → [MonadControlT Lean.MetaM n] → Lean.Name → (β : Q(Sort u)) → (Q(«$β») → n α) → n α
-- Init.NotationExtra
unexpandUnit : Lean.PrettyPrinter.Unexpander
-- Mathlib.Order.UpperLower.Principal
LowerSet.Iic_ne_Iic : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, LowerSet.Iic a ≠ LowerSet.Iic b ↔ a ≠ b
-- Mathlib.Order.Filter.Bases.Basic
Filter.IsBasis.filterBasis.eq_1 : ∀ {α : Type u_1} {ι : Sort u_4} {p : ι → Prop} {s : ι → Set α} (h : Filter.IsBasis p s),
  h.filterBasis = { sets := {t | ∃ i, p i ∧ s i = t}, nonempty := ⋯, inter_sets := ⋯ }
-- Init.Data.SInt.Lemmas
Int64.neg_nonpos_iff : ∀ (n : Int64), -n ≤ 0 ↔ n = Int64.minValue ∨ 0 ≤ n
-- Init.Data.Dyadic.Basic
/-- Subtract two dyadic numbers.  -/
Dyadic.sub : Dyadic → Dyadic → Dyadic
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
_private.Mathlib.Analysis.LocallyConvex.WeakOperatorTopology.0.ContinuousLinearMapWOT.«term_⋆» : Lean.TrailingParserDescr
-- Std.Http.Data.URI.Basic
/-- Formats a query parameter as a string in the format "key" or "key=value". The key and value are
already percent-encoded as `EncodedQueryParam`.
 -/
Std.Http.URI.Query.formatQueryParam : Std.Http.URI.EncodedQueryParam → Option Std.Http.URI.EncodedQueryParam → String
-- Mathlib.Data.Finset.Lattice.Prod
/-- See also `Finset.sup'_prodMap`.  -/
Finset.prodMk_sup'_sup' : ∀ {ι : Type u_7} {κ : Type u_8} {α : Type u_9} {β : Type u_10} [inst : SemilatticeSup α] [inst_1 : SemilatticeSup β]
  {s : Finset ι} {t : Finset κ} (hs : s.Nonempty) (ht : t.Nonempty) (f : ι → α) (g : κ → β),
  (s.sup' hs f, t.sup' ht g) = (s ×ˢ t).sup' ⋯ (Prod.map f g)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get?_modify_self : ∀ {α : Type u} {instOrd : Ord α} [Std.TransOrd α] {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β},
  t.WF →
    ∀ {k : α} {f : β → β},
      Std.DTreeMap.Internal.Impl.Const.get? (Std.DTreeMap.Internal.Impl.Const.modify k f t) k =
        Option.map f (Std.DTreeMap.Internal.Impl.Const.get? t k)
-- Mathlib.Analysis.Normed.Order.Hom.Basic
/-- Constructs a `NormedGroup` structure from a `GroupNormClass` on a `Group`.  -/
GroupNormClass.toNormedGroup : {F : Type u_1} →
  {α : Type u_2} → [inst : FunLike F α ℝ] → [inst_1 : Group α] → [GroupNormClass F α ℝ] → F → NormedGroup α
-- Init.Grind.Interactive
/-- Shorthand for `instantiate only`  -/
Lean.Parser.Tactic.Grind.use : Lean.ParserDescr
-- Mathlib.Data.Finsupp.Single
Finsupp.uniqueEquiv_symm_apply : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] (a : α) [inst_1 : Subsingleton α] (b : M),
  (Finsupp.uniqueEquiv a).symm b = fun₀ | a => b
-- Mathlib.Algebra.Group.Opposite
AddOpposite.instIsLeftCancelAdd : ∀ {α : Type u_1} [inst : Add α] [IsRightCancelAdd α], IsLeftCancelAdd αᵃᵒᵖ
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupNorm.addGroupNormClass : ∀ {E : Type u_3} [inst : AddGroup E], AddGroupNormClass (AddGroupNorm E) E ℝ