mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Prelude
Applicative.toSeqRight : {f : Type u → Type v} → [self : Applicative f] → SeqRight f
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get?_map_of_getKey?_eq_some : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.DTreeMap α (fun x => β) cmp}
  [Std.TransCmp cmp] {f : α → β → γ} {k k' : α},
  t.getKey? k = some k' →
    Std.DTreeMap.Const.get? (Std.DTreeMap.map f t) k = Option.map (f k') (Std.DTreeMap.Const.get? t k)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Maps
SimpleGraph.Walk.transfer.eq_def : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) (H : SimpleGraph V) (h : ∀ e ∈ p.edges, e ∈ H.edgeSet),
  p.transfer H h =
    match u, v, p, h with
    | u, .(u), SimpleGraph.Walk.nil, h => SimpleGraph.Walk.nil
    | u, w, SimpleGraph.Walk.cons h p, h_1 => SimpleGraph.Walk.cons ⋯ (p.transfer H ⋯)
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Functor.opInv_obj : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ), (CategoryTheory.Functor.opInv C D).obj F = Opposite.op F.unop
-- Mathlib.Data.Rel
SetRel.preimage_iUnion : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} (R : SetRel α β) (t : ι → Set β),
  R.preimage (⋃ i, t i) = ⋃ i, R.preimage (t i)
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.supp.eq_1 : ∀ (R : Type u_1) [inst : Semiring R] [inst_1 : ValuativeRel R],
  ValuativeRel.supp R = { carrier := {x | x ≤ᵥ 0}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
-- Mathlib.RingTheory.HahnSeries.Summable
/-- The summable family made of a single Hahn series.  -/
HahnSeries.SummableFamily.single : {Γ : Type u_1} →
  {R : Type u_3} →
    [inst : PartialOrder Γ] →
      [inst_1 : AddCommMonoid R] →
        {ι : Type u_7} → [DecidableEq ι] → ι → HahnSeries Γ R → HahnSeries.SummableFamily Γ R ι
-- Mathlib.MeasureTheory.Function.Jacobian
/-- The derivative of a function on a measurable set is almost everywhere measurable on this set
with respect to Lebesgue measure. Note that, in general, it is not genuinely measurable there,
as `f'` is not unique (but only on a set of measure `0`, as the argument shows).  -/
MeasureTheory.aemeasurable_fderivWithin : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E}
  {f : E → E} {f' : E → E →L[ℝ] E} [inst_3 : MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E)
  [μ.IsAddHaarMeasure], MeasurableSet s → (∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) → AEMeasurable f' (μ.restrict s)
-- Mathlib.Algebra.Category.Grp.Basic
CommGrpCat.hom_ofHom : ∀ {X Y : Type u} [inst : CommGroup X] [inst_1 : CommGroup Y] (f : X →* Y), CommGrpCat.Hom.hom (CommGrpCat.ofHom f) = f
-- Init.Data.Sum.Lemmas
Sum.isLeft_swap : ∀ {α : Type u_1} {β : Type u_2} (x : α ⊕ β), x.swap.isLeft = x.isRight
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.ext : ∀ {X : Type u_1} {R : Type u_3} [inst : Zero X] [inst_1 : Zero R] [inst_2 : TopologicalSpace X]
  [inst_3 : TopologicalSpace R] {f g : ContinuousMapZero X R}, (∀ (x : X), f x = g x) → f = g
-- Mathlib.Algebra.Order.Interval.Set.Group
Set.pairwise_disjoint_Ioc_zsmul : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] (b : α),
  Pairwise (Function.onFun Disjoint fun n => Set.Ioc (n • b) ((n + 1) • b))
-- Mathlib.Algebra.Order.Archimedean.Real.Basic
/-- As `⨆ i, f i = 0` when the real-valued function `f` is unbounded above,
it suffices to show that `f` takes a nonnegative value to show that `0 ≤ ⨆ i, f i`.  -/
Real.iSup_nonneg' : ∀ {ι : Sort u_1} {f : ι → ℝ}, (∃ i, 0 ≤ f i) → 0 ≤ ⨆ i, f i
-- Init.Prelude
MonadReaderOf.mk : {ρ : semiOutParam (Type u)} → {m : Type u → Type v} → m ρ → MonadReaderOf ρ m
-- Mathlib.Algebra.Order.UpperLower
UpperSet.instAdd : {α : Type u_1} → [inst : AddCommGroup α] → [inst_1 : Preorder α] → [IsOrderedAddMonoid α] → Add (UpperSet α)
-- Mathlib.Geometry.Manifold.ChartedSpace
isEmpty_of_chartedSpace : ∀ (H : Type u_5) {M : Type u_6} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M] [ChartedSpace H M]
  [IsEmpty H], IsEmpty M
-- Mathlib.Analysis.Real.Sqrt
Real.sqrt_mul' : ∀ (x : ℝ) {y : ℝ}, 0 ≤ y → √(x * y) = √x * √y
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rci.getElem?_toArray_eq : ∀ {α : Type u} {r : Std.Rci α} [inst : LT α] [DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α]
  [inst : Std.Rxi.IsAlwaysFinite α] {i : ℕ}, r.toArray[i]? = Std.PRange.succMany? i r.lower
-- Std.Sync.CancellationToken
Std.CancellationToken.Consumer.select.sizeOf_spec : ∀ (finished : Std.Async.Waiter Unit), sizeOf (Std.CancellationToken.Consumer.select finished) = 1 + sizeOf finished
-- Mathlib.CategoryTheory.GlueData
/-- This is a variant of `GlueData` that only requires conditions on `V (i, j)` when `i ≠ j`.
See `GlueData.ofGlueData'`
 -/
CategoryTheory.GlueData' : (C : Type u₁) → [CategoryTheory.Category.{v, u₁} C] → Type (max u₁ (v + 1))
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.size_le_size_insertManyIfNewUnit_list : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α (fun x => Unit) cmp} [Std.TransCmp cmp],
  t.WF → ∀ {l : List α}, t.size ≤ (Std.DTreeMap.Raw.Const.insertManyIfNewUnit t l).size
-- Std.Http.Data.URI.Basic
Std.Http.RequestTarget.authorityForm.sizeOf_spec : ∀ (authority : Std.Http.URI.Authority), sizeOf (Std.Http.RequestTarget.authorityForm authority) = 1 + sizeOf authority
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.mapNatIso_counitIso_inv_app_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : D} {S S' : CategoryTheory.Functor C D} (i : S ≅ S')
  (X : CategoryTheory.Comma S' (CategoryTheory.Functor.fromPUnit T)),
  ((CategoryTheory.CostructuredArrow.mapNatIso i).counitIso.inv.app X).left = CategoryTheory.CategoryStruct.id X.left
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
/-- **Alias** of `EisensteinSeries.eisensteinSeriesSIF`.

---

The `SlashInvariantForm` defined by an Eisenstein series of weight `k : ℤ`, level `Γ(N)`,
and congruence condition given by `a : Fin 2 → ZMod N`.  -/
EisensteinSeries.eisensteinSeries_SIF : {N : ℕ} →
  (Fin 2 → ZMod N) →
    (k : ℤ) → SlashInvariantForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma N)) k
-- Mathlib.CategoryTheory.Shift.Basic
CategoryTheory.shiftFunctorAdd'_zero_add : ∀ (C : Type u) {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddMonoid A]
  [inst_2 : CategoryTheory.HasShift C A] (a : A),
  CategoryTheory.shiftFunctorAdd' C 0 a a ⋯ =
    (CategoryTheory.shiftFunctor C a).leftUnitor.symm ≪≫
      CategoryTheory.Functor.isoWhiskerRight (CategoryTheory.shiftFunctorZero C A).symm
        (CategoryTheory.shiftFunctor C a)
-- Mathlib.RingTheory.TwoSidedIdeal.Basic
TwoSidedIdeal.instAddSubgroupClass : ∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R], AddSubgroupClass (TwoSidedIdeal R) R
-- LeanSearchClient.Syntax
LeanSearchClient.SearchResult.toTacticSuggestions : LeanSearchClient.SearchResult → Array Lean.Meta.Tactic.TryThis.Suggestion
-- Mathlib.CategoryTheory.Skeletal
/-- Construct the skeleton category by taking the quotient of objects. This construction gives a
preorder with nice definitional properties, but is only really appropriate for thin categories.
If your original category is not thin, you probably want to be using `Skeleton` instead of this.
 -/
CategoryTheory.ThinSkeleton : (C : Type u₁) → [CategoryTheory.Category.{v₁, u₁} C] → Type u₁
-- Mathlib.Order.Category.Preord
Preord.hom_inv_apply : ∀ {X Y : Preord} (e : X ≅ Y) (s : ↑Y),
  (CategoryTheory.ConcreteCategory.hom e.hom) ((CategoryTheory.ConcreteCategory.hom e.inv) s) = s
-- Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Real.smul_map_volume_mul_left : ∀ {a : ℝ},
  a ≠ 0 → ENNReal.ofReal |a| • MeasureTheory.Measure.map (fun x => a * x) MeasureTheory.volume = MeasureTheory.volume
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.gamma_zero_eq_nfp : Ordinal.gamma 0 = Ordinal.nfp (fun x => Ordinal.veblen x 0) 0
-- Init.Data.BitVec.Lemmas
BitVec.toNat_shiftConcat : ∀ {w : ℕ} {x : BitVec w} {b : Bool}, (x.shiftConcat b).toNat = (x.toNat <<< 1 + b.toNat) % 2 ^ w
-- Mathlib.RingTheory.Valuation.Integers
Valuation.Integers.coe_span_singleton_eq_setOfPred_le_v_algebraMap : ∀ {F : Type u} {Γ₀ : Type v} [inst : Field F] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] {v : Valuation F Γ₀}
  {O : Type w} [inst_2 : CommRing O] [inst_3 : Algebra O F],
  v.Integers O → ∀ (x : O), ↑(Ideal.span {x}) = {y | v ((algebraMap O F) y) ≤ v ((algebraMap O F) x)}
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.pullback.lift_snd_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z}
  [inst_1 : CategoryTheory.Limits.HasPullback f g] (h : W ⟶ X) (k : W ⟶ Y)
  (w : CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp k g) {Z_1 : C} (h_1 : Y ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.lift h k w)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f g) h_1) =
    CategoryTheory.CategoryStruct.comp k h_1
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- A functor from the structured arrow category on the projection functor for any structured
arrow category.  -/
CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.functor : {T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor D T) →
          (Y : T) →
            (X : D) →
              CategoryTheory.Functor (CategoryTheory.StructuredArrow X (CategoryTheory.StructuredArrow.proj Y F))
                (CategoryTheory.StructuredArrow Y ((CategoryTheory.Under.forget X).comp F))
-- Init.Meta.Defs
Lean.Syntax.isScientificLit? : Lean.Syntax → Option (ℕ × Bool × ℕ)
-- Mathlib.RingTheory.TwoSidedIdeal.BigOperators
TwoSidedIdeal.multiSetProd_mem : ∀ {R : Type u_1} [inst : CommRing R] (I : TwoSidedIdeal R) {ι : Type u_2} (s : Multiset ι) (f : ι → R),
  (∃ x ∈ s, f x ∈ I) → (Multiset.map f s).prod ∈ I
-- Mathlib.LinearAlgebra.Finsupp.LSum
LinearMap.leftInverse_splittingOfFinsuppSurjective : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {α : Type u_4}
  (f : M →ₗ[R] α →₀ R) (s : Function.Surjective ⇑f), Function.LeftInverse ⇑f ⇑(f.splittingOfFinsuppSurjective s)
-- Mathlib.Algebra.Module.SpanRank
Submodule.spanFinrank_map_le_of_fg : ∀ {R : Type u_1} {S : Type u_2} {M : Type u} [inst : Semiring R] [inst_1 : Semiring S] {σ : R →+* S}
  [inst_2 : AddCommMonoid M] [inst_3 : Module R M] {L : Type v} [inst_4 : AddCommMonoid L] [inst_5 : Module S L]
  [inst_6 : RingHomSurjective σ] (f : M →ₛₗ[σ] L) {p : Submodule R M},
  p.FG → (Submodule.map f p).spanFinrank ≤ p.spanFinrank
-- Mathlib.Algebra.Order.Kleene
Prod.snd_kstar : ∀ {α : Type u_1} {β : Type u_2} [inst : KleeneAlgebra α] [inst_1 : KleeneAlgebra β] (a : α × β),
  (KStar.kstar a).2 = KStar.kstar a.2
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.IsAddMonHom.zero_hom : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} {M' N' : C}
  {inst_2 : CategoryTheory.AddMonObj M'} {inst_3 : CategoryTheory.AddMonObj N'} (f : M' ⟶ N')
  [self : CategoryTheory.IsAddMonHom f],
  CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.zero f = CategoryTheory.AddMonObj.zero
-- Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
IsLocalFrameOn.contMDiffOn : ∀ {𝕜 : 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} {n : WithTop ℕ∞}
  {s : ι → (x : M) → V x} {u : Set M},
  IsLocalFrameOn I F n s u → ∀ (i : ι), ContMDiffOn I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun x => ⟨x, s i x⟩) u
-- Init.Sym.Lemmas
Lean.Sym.Nat.lt_eq_false : ∀ (a b : ℕ), decide (a < b) = false → (a < b) = False
-- Mathlib.FieldTheory.Relrank
Subfield.inf_relrank_left : ∀ {E : Type v} [inst : Field E] (A B : Subfield E), (A ⊓ B).relrank A = B.relrank A
-- Mathlib.RingTheory.Ideal.Maps
LinearMap.annihilator_le_of_surjective : ∀ {R : Type u_1} {M : Type u_2} {M' : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] (f : M →ₗ[R] M'),
  Function.Surjective ⇑f → Module.annihilator R M ≤ Module.annihilator R M'
-- Init.Data.Vector.Monadic
Vector.forIn_map : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {n : ℕ} {β : Type u_4} {γ : Type u_1} {init : γ} [inst : Monad m]
  [LawfulMonad m] {xs : Vector α n} (g : α → β) (f : β → γ → m (ForInStep γ)),
  forIn (Vector.map g xs) init f = forIn xs init fun a y => f (g a) y
-- Mathlib.Combinatorics.Additive.ApproximateSubgroup
IsApproximateAddSubgroup.nonempty : ∀ {G : Type u_1} [inst : AddGroup G] {A : Set G} {K : ℝ}, IsApproximateAddSubgroup K A → A.Nonempty
-- Mathlib.Algebra.Group.Pi.Lemmas
Pi.mulSingle_sup : ∀ {I : Type u} {f : I → Type v} [inst : DecidableEq I] [inst_1 : (i : I) → SemilatticeSup (f i)]
  [inst_2 : (i : I) → One (f i)] (i : I) (x y : f i), Pi.mulSingle i (x ⊔ y) = Pi.mulSingle i x ⊔ Pi.mulSingle i y
-- Mathlib.ModelTheory.Satisfiability
/-- The **Compactness Theorem of first-order logic**: A theory is satisfiable if and only if it is
finitely satisfiable.  -/
FirstOrder.Language.Theory.isSatisfiable_iff_isFinitelySatisfiable : ∀ {L : FirstOrder.Language} {T : L.Theory}, T.IsSatisfiable ↔ T.IsFinitelySatisfiable
-- Mathlib.Algebra.Regular.Basic
/-- If a product is regular, so is its right factor.  -/
IsRegular.of_mul_right : ∀ {R : Type u_1} [inst : CommSemigroup R] {a b : R}, IsRegular (a * b) → IsRegular b
-- Mathlib.Algebra.Homology.HomologicalComplex
CochainComplex.next : ∀ (α : Type u_2) [inst : AddRightCancelSemigroup α] [inst_1 : One α] (i : α), (ComplexShape.up α).next i = i + 1
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.isoMk_hom_left : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {L₁ : CategoryTheory.Functor A T}
  {R₁ : CategoryTheory.Functor B T} {X Y : CategoryTheory.Comma L₁ R₁} (l : X.left ≅ Y.left) (r : X.right ≅ Y.right)
  (h :
    autoParam
      (CategoryTheory.CategoryStruct.comp (L₁.map l.hom) Y.hom =
        CategoryTheory.CategoryStruct.comp X.hom (R₁.map r.hom))
      CategoryTheory.Comma.isoMk._auto_1),
  (CategoryTheory.Comma.isoMk l r h).hom.left = l.hom
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.PolyDerivation.brecOn.eq : ∀ {motive : Lean.Meta.Grind.Arith.CommRing.PolyDerivation → Sort u} (t : Lean.Meta.Grind.Arith.CommRing.PolyDerivation)
  (F_1 :
    (t : Lean.Meta.Grind.Arith.CommRing.PolyDerivation) →
      Lean.Meta.Grind.Arith.CommRing.PolyDerivation.below t → motive t),
  Lean.Meta.Grind.Arith.CommRing.PolyDerivation.brecOn t F_1 =
    F_1 t (Lean.Meta.Grind.Arith.CommRing.PolyDerivation.brecOn.go t F_1).2
-- Mathlib.AlgebraicTopology.SimplexCategory.SemiSimplexCategory
/-- The object of `SemiSimplexCategory` corresponding to `n : ℕ` is denoted `⦋n⦌ₛ`.  -/
Simplicial.«term⦋_⦌ₛ» : Lean.ParserDescr
-- Init.Data.List.Zip
List.tail_zip_fst : ∀ {α : Type u_1} {β : Type u_2} {l : List (α × β)}, l.unzip.1.tail = l.tail.unzip.1
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas
_private.Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas.0.RootPairing.chainBotCoeff_mul_chainTopCoeff.aux_0 : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : CharZero R]
  [inst_2 : IsDomain R] [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : AddCommGroup N] [inst_6 : Module R N]
  {P : RootPairing ι R M N} [inst_7 : Finite ι] [inst_8 : P.IsCrystallographic] {i k : ι} [P.IsNotG2],
  P.root k + P.root i ∈ Set.range ⇑P.root →
    P.pairingIn ℤ k i = 0 ∨ P.pairingIn ℤ k i < 0 ∧ RootPairing.chainBotCoeff i k = 0
-- Init.Data.Vector.Zip
Vector.zip_append : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {m : ℕ} {as : Vector α n} {bs : Vector β n} {as' : Vector α m}
  {bs' : Vector β m}, (as ++ as').zip (bs ++ bs') = as.zip bs ++ as'.zip bs'
-- Mathlib.Analysis.InnerProductSpace.Adjoint
_private.Mathlib.Analysis.InnerProductSpace.Adjoint.0.ContinuousLinearMap.adjointAux_inner_right : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : InnerProductSpace 𝕜 E] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : CompleteSpace E] (A : E →L[𝕜] F) (x : E) (y : F),
  inner 𝕜 x ((ContinuousLinearMap.adjointAux✝ A) y) = inner 𝕜 (A x) y
-- Mathlib.Algebra.EuclideanDomain.Defs
EuclideanDomain.xgcdAux.eq_def : ∀ {R : Type u} [inst : EuclideanDomain R] [inst_1 : DecidableEq R] (r s t r' s' t' : R),
  EuclideanDomain.xgcdAux r s t r' s' t' =
    if _hr : r = 0 then (r', s', t')
    else
      have q := r' / r;
      have x := ⋯;
      EuclideanDomain.xgcdAux (r' % r) (s' - q * s) (t' - q * t) r s t
-- Mathlib.Algebra.Order.Interval.Basic
NonemptyInterval.fst_div : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : CommGroup α] [inst_2 : MulLeftMono α] (s t : NonemptyInterval α),
  (s / t).toProd.1 = s.toProd.1 / t.toProd.2
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get!_eq_get!_get? : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α], (↑m).WF → ∀ {a : α} [inst_3 : Inhabited (β a)], m.get! a = (m.get? a).get!
-- Mathlib.AlgebraicGeometry.Birational.Birational
AlgebraicGeometry.Scheme.Opens.partialIsoOfDense_target : ∀ {X : AlgebraicGeometry.Scheme} (U : X.Opens) (hU : Dense ↑U), (U.partialIsoOfDense hU).target = U
-- Mathlib.Topology.Order.LowerUpperTopology
/-- A function `f : β → α` with upper topology in the codomain is continuous
if and only if the preimage of every interval `Set.Iic a` is a closed set.  -/
Topology.IsUpper.continuous_iff_Iic : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : TopologicalSpace α] [Topology.IsUpper α]
  [inst_3 : TopologicalSpace β] {f : β → α}, Continuous f ↔ ∀ (a : α), IsClosed (f ⁻¹' Set.Iic a)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Real.cos_eq_cos_iff : ∀ {x y : ℝ}, Real.cos x = Real.cos y ↔ ∃ k, y = 2 * ↑k * Real.pi + x ∨ y = 2 * ↑k * Real.pi - x
-- Mathlib.Algebra.Group.Opposite
MulOpposite.instDivInvMonoid.eq_1 : ∀ {α : Type u_1} [inst : DivInvMonoid α],
  MulOpposite.instDivInvMonoid =
    { toMonoid := MulOpposite.instMonoid, toInv := MulOpposite.instInv, div := DivInvMonoid.div',
      zpow := fun n a => MulOpposite.op (MulOpposite.unop a ^ n), div_eq_mul_inv := ⋯, zpow_zero' := ⋯, zpow_succ' := ⋯,
      zpow_neg' := ⋯ }
-- Mathlib.Order.KrullDimension
Order.height_pos_of_bot_lt : ∀ {α : Type u_1} [inst : Preorder α] {x : α} [inst_1 : OrderBot α], ⊥ < x → 0 < Order.height x
-- Mathlib.ModelTheory.Order
FirstOrder.Language.realize_noTopOrder_iff : ∀ {L : FirstOrder.Language} {M : Type w'} [inst : L.IsOrdered] [inst_1 : L.Structure M] [inst_2 : LE M]
  [L.OrderedStructure M], M ⊨ L.noTopOrderSentence ↔ NoTopOrder M
-- Mathlib.CategoryTheory.Bicategory.Modification.Lax
CategoryTheory.Lax.LaxTrans.Hom.of.inj : ∀ {B : Type u₁} {inst : CategoryTheory.Bicategory B} {C : Type u₂} {inst_1 : CategoryTheory.Bicategory C}
  {F G : CategoryTheory.LaxFunctor B C} {η θ : F ⟶ G} {as as_1 : CategoryTheory.Lax.LaxTrans.Modification η θ},
  { as := as } = { as := as_1 } → as = as_1
-- Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.repr_symm_apply : ∀ {ι : Type u_1} {R : Type u_3} {M : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (b : Module.Basis ι R M) (v : ι →₀ R), b.repr.symm v = (Finsupp.linearCombination R ⇑b) v
-- Mathlib.LinearAlgebra.QuadraticForm.Real
/-- The isometry between a weighted sum of squares with weights `u` on the
(non-zero) real numbers and the weighted sum of squares with weights `sign ∘ u`.  -/
QuadraticForm.isometryEquivSignWeightedSumSquares : {ι : Type u_1} →
  [inst : Fintype ι] →
    (w : ι → ℝ) →
      (QuadraticMap.weightedSumSquares ℝ w).IsometryEquiv
        (QuadraticMap.weightedSumSquares ℝ fun i => ↑(SignType.sign (w i)))
-- Mathlib.Data.Set.Lattice
Set.iInter_inter_distrib : ∀ {β : Type u_2} {ι : Sort u_5} (s t : ι → Set β), ⋂ i, s i ∩ t i = (⋂ i, s i) ∩ ⋂ i, t i
-- Mathlib.Topology.Order.UpperLowerSetTopology
Topology.WithUpperSet.ofUpperSet_inj : ∀ {α : Type u_1} {a b : Topology.WithUpperSet α},
  Topology.WithUpperSet.ofUpperSet a = Topology.WithUpperSet.ofUpperSet b ↔ a = b
-- Mathlib.Algebra.MvPolynomial.CommRing
MvPolynomial.coeff_sub : ∀ {R : Type u} (σ : Type u_1) [inst : CommRing R] (m : σ →₀ ℕ) (p q : MvPolynomial σ R),
  MvPolynomial.coeff m (p - q) = MvPolynomial.coeff m p - MvPolynomial.coeff m q
-- Init.Data.SInt.Bitwise
ISize.shiftLeft_and : ∀ {a b c : ISize}, (a &&& b) <<< c = a <<< c &&& b <<< c
-- Lean.Meta.RecursorInfo
Lean.Meta.RecursorInfo.typeName : Lean.Meta.RecursorInfo → Lean.Name
-- Init.Data.Nat.Div.Lemmas
Nat.mod_add_mod_eq : ∀ {a b c : ℕ}, a % c + b % c = (a + b) % c + if a % c + b % c < c then 0 else c
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.updateCell.match_5.eq_2 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : (l : Std.DTreeMap.Internal.Impl α β) → l.Balanced → Sort u_3) (sz : ℕ)
  (ky : α) (y : β ky) (l r : Std.DTreeMap.Internal.Impl α β)
  (hl : (Std.DTreeMap.Internal.Impl.inner sz ky y l r).Balanced)
  (h_1 : (hl : Std.DTreeMap.Internal.Impl.leaf.Balanced) → motive Std.DTreeMap.Internal.Impl.leaf hl)
  (h_2 :
    (sz : ℕ) →
      (ky : α) →
        (y : β ky) →
          (l r : Std.DTreeMap.Internal.Impl α β) →
            (hl : (Std.DTreeMap.Internal.Impl.inner sz ky y l r).Balanced) →
              motive (Std.DTreeMap.Internal.Impl.inner sz ky y l r) hl),
  (match Std.DTreeMap.Internal.Impl.inner sz ky y l r, hl with
    | Std.DTreeMap.Internal.Impl.leaf, hl => h_1 hl
    | Std.DTreeMap.Internal.Impl.inner sz ky y l r, hl => h_2 sz ky y l r hl) =
    h_2 sz ky y l r hl
-- Mathlib.Dynamics.Minimal
/-- An action of a monoid `M` on a topological space is called *minimal* if the `M`-orbit of every
point `x : α` is dense.  -/
MulAction.IsMinimal : (M : Type u_1) → (α : Type u_2) → [inst : Monoid M] → [TopologicalSpace α] → [MulAction M α] → Prop
-- Mathlib.Topology.Category.UniformSpace
/-- The category instance on `CpltSepUniformSpace`.  -/
CpltSepUniformSpace.category : CategoryTheory.LargeCategory CpltSepUniformSpace
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ioo_subset_Ioo : ∀ {α : Type u_2} {a₁ a₂ b₁ b₂ : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α],
  a₂ ≤ a₁ → b₁ ≤ b₂ → Finset.Ioo a₁ b₁ ⊆ Finset.Ioo a₂ b₂
-- Mathlib.Topology.MetricSpace.Algebra
TendstoLocallyUniformlyOn.smul₀ : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] [inst_2 : Zero α]
  [inst_3 : Zero β] [inst_4 : SMul α β] [IsBoundedSMul α β] {X : Type u_3} {ι : Type u_4} [inst_6 : TopologicalSpace X]
  {s : Set X} {F : ι → X → α} {G : ι → X → β} {f : X → α} {g : X → β} {l : Filter ι},
  TendstoLocallyUniformlyOn F f l s →
    TendstoLocallyUniformlyOn G g l s →
      ContinuousOn f s → ContinuousOn g s → TendstoLocallyUniformlyOn (F • G) (f • g) l s
-- Lean.Server.Requests
/-- `handle` with explicit state management for chaining request handlers.
This function is pure w.r.t. `lastTaskMutex` and `stateRef`, but not `RequestM`.
 -/
Lean.Server.StatefulRequestHandler.pureHandle : Lean.Server.StatefulRequestHandler →
  Lean.Json → Dynamic → Lean.Server.RequestM (Lean.Server.SerializedLspResponse × Dynamic)