mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Fourier.Notation
/-- The inverse Fourier transform as a linear map.  -/
FourierTransform.fourierInvₗ : (R : Type u_2) →
  (E : Type u_3) →
    {F : Type u_4} →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid E] →
          [inst_2 : AddCommMonoid F] →
            [inst_3 : Module R E] →
              [inst_4 : Module R F] →
                [inst_5 : FourierTransformInv E F] → [FourierInvAdd E F] → [FourierInvSMul R E F] → E →ₗ[R] F
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roo.toArray_succ_succ_eq_map : ∀ {α : Type u} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [Std.PRange.LinearlyUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α]
  [inst_5 : Std.PRange.InfinitelyUpwardEnumerable α] [inst_6 : Std.Rxo.IsAlwaysFinite α]
  [inst_7 : Std.PRange.LawfulUpwardEnumerable α] {lo hi : α},
  ((Std.PRange.succ lo)<...Std.PRange.succ hi).toArray = Array.map Std.PRange.succ (lo<...hi).toArray
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.Limits.ReflexiveCofork.mk_π : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor CategoryTheory.Limits.WalkingReflexivePair C} {X : C}
  (π : F.obj CategoryTheory.Limits.WalkingReflexivePair.zero ⟶ X)
  (h :
    CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.left) π =
      CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.right) π),
  (CategoryTheory.Limits.ReflexiveCofork.mk π h).π = π
-- Mathlib.Analysis.Asymptotics.ExpGrowth
Monotone.expGrowthInf_comp_mul : ∀ {u : ℕ → ENNReal} {m : ℕ},
  Monotone u → m ≠ 0 → (ExpGrowth.expGrowthInf fun n => u (m * n)) = ↑m * ExpGrowth.expGrowthInf u
-- Mathlib.Topology.Filter
Filter.isOpen_iff : ∀ {α : Type u_2} {s : Set (Filter α)}, IsOpen s ↔ ∃ T, s = ⋃ t ∈ T, Set.Iic (Filter.principal t)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.ShrinkYoneda
/-- The type `(shrinkYonedaMon.obj M).obj Y` is equivalent to `Y.unop ⟶ M.X`.  -/
CategoryTheory.shrinkYonedaMonObjObjEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] →
      [inst_2 : CategoryTheory.CartesianMonoidalCategory C] →
        {M : CategoryTheory.Mon C} →
          {Y : Cᵒᵖ} → ↑((CategoryTheory.shrinkYonedaMon.{w, v, u}.obj M).obj Y) ≃* (Opposite.unop Y ⟶ M.X)
-- Mathlib.GroupTheory.Subgroup.Saturated
AddSubmonoid.nsmulSaturated_iff_nsmul : ∀ {G : Type u_1} [inst : AddMonoid G] {H : AddSubmonoid G},
  H.NSMulSaturated ↔ ∀ (n : ℕ) (g : G), n • g ∈ H → n = 0 ∨ g ∈ H
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.ImageFactorisation.copy_isImage : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y}
  (F : CategoryTheory.Limits.ImageFactorisation f) (m : F.F.I ⟶ Y) (e : X ⟶ F.F.I)
  (hm : autoParam (m = F.F.m) CategoryTheory.Limits.ImageFactorisation.copy._auto_1)
  (he : autoParam (e = F.F.e) CategoryTheory.Limits.ImageFactorisation.copy._auto_3),
  (F.copy m e hm he).isImage = F.isImage.copy m e ⋯ ⋯
-- Mathlib.Algebra.MvPolynomial.Basic
/-- `C a` is the constant polynomial with value `a`  -/
MvPolynomial.C : {R : Type u} → {σ : Type u_1} → [inst : CommSemiring R] → R →+* MvPolynomial σ R
-- Mathlib.Data.List.Fold
/-- **Second Bird–Wadler duality theorem**.  -/
List.foldl_flip_eq_foldr : ∀ {α : Type u_1} {β : Type u_2} {l : List α} {f : α → β → β} {b : β} [LeftCommutative f],
  List.foldl (flip f) b l = List.foldr f b l
-- Mathlib.Analysis.Calculus.Deriv.AffineMap
AffineMap.hasStrictDerivAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] (f : 𝕜 →ᵃ[𝕜] E) {x : 𝕜}, HasStrictDerivAt (⇑f) (f.linear 1) x
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.coeIdeal_injective' : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  [loc : IsLocalization S P], S ≤ nonZeroDivisors R → Function.Injective fun I => ↑I
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
CategoryTheory.Pseudofunctor.DescentData.Hom.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C}
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} {D₁ D₂ : F.DescentData f} {hom : (i : ι) → D₁.obj i ⟶ D₂.obj i}
  {comm :
    autoParam
      (∀ ⦃Y : C⦄ (q : Y ⟶ S) ⦃i₁ i₂ : ι⦄ (f₁ : Y ⟶ X i₁) (f₂ : Y ⟶ X i₂)
        (hf₁ : CategoryTheory.CategoryStruct.comp f₁ (f i₁) = q)
        (hf₂ : CategoryTheory.CategoryStruct.comp f₂ (f i₂) = q),
        CategoryTheory.CategoryStruct.comp ((F.map f₁.op.toLoc).toFunctor.map (hom i₁)) (D₂.hom q f₁ f₂ ⋯ ⋯) =
          CategoryTheory.CategoryStruct.comp (D₁.hom q f₁ f₂ ⋯ ⋯) ((F.map f₂.op.toLoc).toFunctor.map (hom i₂)))
      CategoryTheory.Pseudofunctor.DescentData.Hom.comm._autoParam}
  {hom_1 : (i : ι) → D₁.obj i ⟶ D₂.obj i}
  {comm_1 :
    autoParam
      (∀ ⦃Y : C⦄ (q : Y ⟶ S) ⦃i₁ i₂ : ι⦄ (f₁ : Y ⟶ X i₁) (f₂ : Y ⟶ X i₂)
        (hf₁ : CategoryTheory.CategoryStruct.comp f₁ (f i₁) = q)
        (hf₂ : CategoryTheory.CategoryStruct.comp f₂ (f i₂) = q),
        CategoryTheory.CategoryStruct.comp ((F.map f₁.op.toLoc).toFunctor.map (hom_1 i₁)) (D₂.hom q f₁ f₂ ⋯ ⋯) =
          CategoryTheory.CategoryStruct.comp (D₁.hom q f₁ f₂ ⋯ ⋯) ((F.map f₂.op.toLoc).toFunctor.map (hom_1 i₂)))
      CategoryTheory.Pseudofunctor.DescentData.Hom.comm._autoParam},
  { hom := hom, comm := comm } = { hom := hom_1, comm := comm_1 } → hom = hom_1
-- Mathlib.CategoryTheory.Monoidal.Bimon_
/-- A bimonoid object in a braided category `C` is an object that is simultaneously monoid and comonoid
objects, and structure morphisms of them satisfy appropriate consistency conditions.
 -/
CategoryTheory.BimonObj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → [CategoryTheory.BraidedCategory C] → C → Type v₁
-- Mathlib.Geometry.Manifold.VectorBundle.Basic
Bundle.contMDiff_section_of_subsingleton : ∀ {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} (E : B → Type u_6) [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F] [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_4 : (x : B) → TopologicalSpace (E x)] {EB : Type u_7} [inst_5 : NormedAddCommGroup EB]
  [inst_6 : NormedSpace 𝕜 EB] {HB : Type u_8} [inst_7 : TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB}
  [inst_8 : TopologicalSpace B] [inst_9 : ChartedSpace HB B] [inst_10 : FiberBundle F E] {s : (x : B) → E x}
  [Subsingleton F], ContMDiff IB (IB.prod (modelWithCornersSelf 𝕜 F)) n fun x => ⟨x, s x⟩
-- Init.Tactics
/-- A `dsimpArg` is similar to `simpArg`, but it does not have the `simpStar` form
because it does not make sense to use hypotheses in `dsimp`.
 -/
Lean.Parser.Tactic.dsimpArg : Lean.ParserDescr
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
ContinuousLinearMap.norm_compContinuousAlternatingMap_le : ∀ {𝕜 : Type u} {E : Type wE} {F : Type wF} {G : Type wG} {ι : Type v} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 F] [inst_5 : SeminormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] [inst_7 : Fintype ι]
  (g : F →L[𝕜] G) (f : E [⋀^ι]→L[𝕜] F), ‖g.compContinuousAlternatingMap f‖ ≤ ‖g‖ * ‖f‖
-- Mathlib.Data.Seq.Basic
Stream'.Seq.nil.eq_1 : ∀ {α : Type u}, Stream'.Seq.nil = ⟨Stream'.const none, ⋯⟩
-- Mathlib.Tactic.FunProp.Mor
/-- Morphism application  -/
Mathlib.Meta.FunProp.Mor.app : Lean.Expr → Mathlib.Meta.FunProp.Mor.Arg → Lean.Expr
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.Array.shrink.loop.eq_def : ∀ {α : Type u} (x : ℕ) (x_1 : Array α),
  Array.shrink.loop✝ x x_1 =
    match x, x_1 with
    | 0, xs => xs
    | n.succ, xs => Array.shrink.loop✝ n xs.pop
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem!_emptyc : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : Inhabited β] {a : α}, ∅[a]! = default
-- Batteries.Data.List.Lemmas
List.isPrefixOf?_eq_some_iff_append_eq : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {xs ys zs : List α}, xs.isPrefixOf? ys = some zs ↔ xs ++ zs = ys
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey!_eq_of_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [inst_2 : Inhabited α] {k : α}, k ∈ t → t.getKey! k = k
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.roots_eq_of_natDegree_le_card_of_ne_zero : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] {p : Polynomial R} {S : Finset R},
  (∀ x ∈ S, Polynomial.eval x p = 0) → p.natDegree ≤ S.card → p ≠ 0 → p.roots = S.val
-- Init.Data.Range.Basic
Membership.get_elem_helper : ∀ {i n : ℕ} {r : Std.Legacy.Range}, i ∈ r → r.stop = n → i < n
-- Mathlib.Algebra.Order.UpperLower
LowerSet.instAdd : {α : Type u_1} → [inst : AddCommGroup α] → [inst_1 : Preorder α] → [IsOrderedAddMonoid α] → Add (LowerSet α)
-- Mathlib.Algebra.Group.Submonoid.Defs
AddSubmonoid.mk : {M : Type u_3} →
  [inst : AddZeroClass M] → (toAddSubsemigroup : AddSubsemigroup M) → 0 ∈ toAddSubsemigroup.carrier → AddSubmonoid M
-- Mathlib.CategoryTheory.Category.Quiv
/-- An isomorphism of quivers defines an equivalence on carrier types.  -/
CategoryTheory.Quiv.equivOfIso : {V W : CategoryTheory.Quiv} → (V ≅ W) → ↑V ≃ ↑W
-- Mathlib.Algebra.Group.Subgroup.Pointwise
Subgroup.closure_singleton_inv : ∀ {G : Type u_2} [inst : Group G] (x : G), Subgroup.closure {x⁻¹} = Subgroup.closure {x}
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBSet.mem_of_mem_toList : ∀ {α : Type u_1} {cmp : α → α → Ordering} {x : α} [Std.OrientedCmp cmp] {t : RBTree.RBSet α cmp}, x ∈ t.toList → x ∈ t
-- Std.Internal.Parsec.ByteArray
/-- Skips while a predicate is satisfied, up to a given limit.
Fails with `.eof` if input ends before stopping or reaching the limit.
 -/
Std.Internal.Parsec.ByteArray.skipWhileUpTo : (UInt8 → Bool) → ℕ → Std.Internal.Parsec.ByteArray.Parser Unit
-- Mathlib.Order.Hom.Lattice
Pi.coe_evalLatticeHom : ∀ {ι : Type u_6} {α : ι → Type u_7} [inst : (i : ι) → Lattice (α i)] (i : ι), ⇑(Pi.evalLatticeHom i) = Function.eval i
-- Mathlib.CategoryTheory.Limits.Comma
CategoryTheory.Comma.coconeOfPreserves_pt_hom : ∀ {J : Type w} [inst : CategoryTheory.Category.{w', w} J] {A : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} A]
  {B : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃}
  [inst_3 : CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T}
  (F : CategoryTheory.Functor J (CategoryTheory.Comma L R))
  [inst_4 : CategoryTheory.Limits.PreservesColimit (F.comp (CategoryTheory.Comma.fst L R)) L]
  {c₁ : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.Comma.fst L R))} (t₁ : CategoryTheory.Limits.IsColimit c₁)
  (c₂ : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.Comma.snd L R))),
  (CategoryTheory.Comma.coconeOfPreserves F t₁ c₂).pt.hom =
    (CategoryTheory.Limits.isColimitOfPreserves L t₁).desc (CategoryTheory.Comma.colimitAuxiliaryCocone F c₂)
-- Mathlib.Combinatorics.Matroid.Basic
/-- An `RankInfinite` matroid is one whose bases are infinite.  -/
Matroid.RankInfinite : {α : Type u_1} → Matroid α → Prop
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.uniqueRingEquiv_apply : ∀ {R : Type u_1} (M : Type u_4) [inst : Semiring R] [inst_1 : Monoid M] [inst_2 : Subsingleton M]
  (a : MonoidAlgebra R M), (MonoidAlgebra.uniqueRingEquiv M) a = a.coeff 1
-- Mathlib.RingTheory.WittVector.Identities
WittVector.mul_charP_coeff_succ : ∀ {p : ℕ} {R : Type u_1} [hp : Fact (Nat.Prime p)] [inst : CommRing R] [CharP R p] (x : WittVector p R) (i : ℕ),
  (x * ↑p).coeff (i + 1) = x.coeff i ^ p
-- Mathlib.Order.Filter.Extr
IsMaxOn.isLUB : ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {s : Set α} {a : α},
  a ∈ s → IsMaxOn f s a → IsLUB {x | ∃ x_1 ∈ s, f x_1 = x} (f a)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get!_filter_of_getKey?_eq_some : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : Inhabited β] {f : α → β → Bool} {k k' : α} (h : t.WF),
  t.getKey? k = some k' →
    Std.DTreeMap.Internal.Impl.Const.get! (Std.DTreeMap.Internal.Impl.filter f t ⋯).impl k =
      (Option.filter (fun x => f k' x) (Std.DTreeMap.Internal.Impl.Const.get? t k)).get!
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.Parser.transparency : Lean.ParserDescr
-- Lean.Meta.Sym.Simp.SimpM
Lean.Meta.Sym.Simp.instNonemptyMethodsRef : Nonempty Lean.Meta.Sym.Simp.MethodsRef
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.single_lt_sum : ∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : Preorder M] [IsOrderedCancelAddMonoid M] {f : ι → M}
  {s : Finset ι} [AddLeftStrictMono M] {i j : ι},
  j ≠ i → i ∈ s → j ∈ s → 0 < f j → (∀ k ∈ s, k ≠ i → 0 ≤ f k) → f i < ∑ k ∈ s, f k
-- Mathlib.Topology.Maps.Basic
Topology.isInducing_iff_nhds : ∀ {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))
-- Lean.LocalContext
Lean.instHashableLocalDeclKind.hash : Lean.LocalDeclKind → UInt64
-- Mathlib.Data.Stream.Defs
/-- Head of a stream: `Stream'.head s = Stream'.get s 0`.  -/
Stream'.head : {α : Type u} → Stream' α → α
-- Mathlib.Data.Nat.Prime.Int
Int.prime_three : Prime 3
-- Batteries.Util.ProofWanted
_private.Batteries.Util.ProofWanted.0.instanceWantedCmd : WantedCmdKind✝
-- Lean.Elab.ParseImportsFast
Lean.PrintImportsResult.mk.inj : ∀ {imports imports_1 : Array Lean.PrintImportResult},
  { imports := imports } = { imports := imports_1 } → imports = imports_1
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.isSome_minKey?_of_contains : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, t.contains k = true → t.minKey?.isSome = true
-- Mathlib.ModelTheory.Fraisse
/-- A countably generated structure is ultrahomogeneous if and only if any equivalence between
finitely generated substructures can be extended to any element in the domain.  -/
FirstOrder.Language.isUltrahomogeneous_iff_IsExtensionPair : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M],
  FirstOrder.Language.Structure.CG L M → (L.IsUltrahomogeneous M ↔ L.IsExtensionPair M M)
-- Mathlib.SetTheory.Ordinal.CantorNormalForm
_private.Mathlib.SetTheory.Ordinal.CantorNormalForm.0.Ordinal.CNF.nodupKeys : ∀ (b o : Ordinal.{u_1}), (List.map Prod.toSigma (Ordinal.CNF b o)).NodupKeys
-- Mathlib.Lean.Meta.RefinedDiscrTree.Initialize
/-- Information about a failed import.  -/
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Initialize.0.Lean.Meta.RefinedDiscrTree.ImportFailure : Type
-- Mathlib.Analysis.Complex.Hadamard
/-- Rewrite for `InterpStrip` when `0 = sSupNormIm f 0` or `0 = sSupNormIm f 1`.  -/
Complex.HadamardThreeLines.interpStrip_eq_of_zero : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] (f : ℂ → E) (z : ℂ),
  Complex.HadamardThreeLines.sSupNormIm f 0 = 0 ∨ Complex.HadamardThreeLines.sSupNormIm f 1 = 0 →
    Complex.HadamardThreeLines.interpStrip f z = 0
-- Mathlib.GroupTheory.Subsemigroup.Center
AddSubsemigroup.center.eq_1 : ∀ (M : Type u_1) [inst : Add M], AddSubsemigroup.center M = { carrier := Set.addCenter M, add_mem' := ⋯ }
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.cokernel.desc_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasCokernel f] {W : C} {h : CategoryTheory.CategoryStruct.comp f 0 = 0},
  CategoryTheory.Limits.cokernel.desc f 0 h = 0
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
HomotopicalAlgebra.PathObject.ofFactorizationData_p₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] {A : C}
  (h :
    (HomotopicalAlgebra.trivialCofibrations C).MapFactorizationData (HomotopicalAlgebra.fibrations C)
      (CategoryTheory.Limits.diag A)),
  (HomotopicalAlgebra.PathObject.ofFactorizationData h).p₀ =
    CategoryTheory.CategoryStruct.comp h.p CategoryTheory.Limits.prod.fst
-- Lean.Util.NumObjs
Lean.Expr.NumObjs.State : Type
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.edgeFinset_subset_sym2_of_support_subset : ∀ {V : Type u_1} {s : Set V} [inst : DecidablePred fun x => x ∈ s] [inst_1 : Fintype V] {G : SimpleGraph V}
  [inst_2 : DecidableRel G.Adj], G.support ⊆ s → G.edgeFinset ⊆ s.toFinset.sym2
-- Mathlib.Topology.Sheaves.Stalks
TopCat.Presheaf.stalkSpecializes_stalkPushforward_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X Y : TopCat}
  (f : X ⟶ Y) (F : TopCat.Presheaf C X) {x y : ↑X} (h : x ⤳ y) {Z : C} (h_1 : F.stalk x ⟶ Z),
  CategoryTheory.CategoryStruct.comp (((TopCat.Presheaf.pushforward C f).obj F).stalkSpecializes ⋯)
      (CategoryTheory.CategoryStruct.comp (TopCat.Presheaf.stalkPushforward C f F x) h_1) =
    CategoryTheory.CategoryStruct.comp (TopCat.Presheaf.stalkPushforward C f F y)
      (CategoryTheory.CategoryStruct.comp (F.stalkSpecializes h) h_1)
-- Mathlib.CategoryTheory.MorphismProperty.Composition
/-- for all `X : C`, the identity of `X` satisfies the morphism property  -/
CategoryTheory.MorphismProperty.ContainsIdentities.id_mem : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {W : CategoryTheory.MorphismProperty C}
  [self : W.ContainsIdentities] (X : C), W (CategoryTheory.CategoryStruct.id X)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equifibered
CategoryTheory.NatTrans.equifibered_unop_iff : ∀ {J : Type u_1} {C : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_3} C] {F G : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ} {α : F ⟶ G},
  CategoryTheory.NatTrans.Equifibered (CategoryTheory.NatTrans.unop α) ↔ CategoryTheory.NatTrans.Coequifibered α
-- Lean.Server.Utils
Lean.Server.DocumentMeta.mk : Lean.Lsp.DocumentUri → Lean.Name → ℕ → Lean.FileMap → Lean.Lsp.DependencyBuildMode → Lean.Server.DocumentMeta
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
MeasureTheory.Measure.MutuallySingular.haveLebesgueDecomposition : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α},
  μ.MutuallySingular ν → μ.HaveLebesgueDecomposition ν
-- Mathlib.CategoryTheory.Action.Basic
Action.instIsEquivalenceFunctorSingleObjInverse : ∀ (V : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} V] (G : Type u_2) [inst_1 : Monoid G],
  Action.FunctorCategoryEquivalence.inverse.IsEquivalence
-- Mathlib.Algebra.Category.Ring.Basic
/-- **Alias** of `CategoryTheory.forget_obj`. -/
RingCat.forget_obj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {FC : outParam (C → C → Type u_2)}
  {CC : outParam (C → Type w)} [inst_1 : outParam ((X Y : C) → FunLike (FC X Y) (CC X) (CC Y))]
  [inst_2 : CategoryTheory.ConcreteCategory C FC] (X : C), (CategoryTheory.forget C).obj X = CategoryTheory.ToType X
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousAlternatingMap.smulRight_apply : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {ι : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] [inst_5 : TopologicalSpace R]
  [inst_6 : TopologicalSpace M] [inst_7 : TopologicalSpace N] [inst_8 : ContinuousSMul R N] (f : M [⋀^ι]→L[R] R) (z : N)
  (a : (i : ι) → (fun x => M) i), (f.smulRight z) a = f a • z
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.toArray_keys : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp}, t.keys.toArray = t.keysArray
-- Mathlib.LinearAlgebra.QuadraticForm.TensorProduct
LinearMap.BilinForm.tensorDistrib.eq_1 : ∀ (R : Type uR) (A : Type uA) {M₁ : Type uM₁} {M₂ : Type uM₂} [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : AddCommMonoid M₁] [inst_3 : AddCommMonoid M₂] [inst_4 : Algebra R A] [inst_5 : Module R M₁]
  [inst_6 : Module A M₁] [inst_7 : SMulCommClass R A M₁] [inst_8 : IsScalarTower R A M₁] [inst_9 : Module R M₂],
  LinearMap.BilinForm.tensorDistrib R A =
    ↑(TensorProduct.AlgebraTensorModule.rid R A A).congrRight₂ ∘ₗ LinearMap.BilinMap.tensorDistrib R A
-- Mathlib.Data.Set.SMulAntidiagonal
Set.VAddAntidiagonal.finite_of_isPWO : ∀ {G : Type u_1} {P : Type u_2} {s : Set G} {t : Set P} [inst : PartialOrder G] [inst_1 : PartialOrder P]
  [inst_2 : VAdd G P] [IsOrderedCancelVAdd G P], s.IsPWO → t.IsPWO → ∀ (a : P), (s.vaddAntidiagonal t a).Finite
-- Mathlib.LinearAlgebra.UnitaryGroup
Matrix.kroneckerTMul_mem_unitary : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type u_1} {A : Type u_2} {B : Type u_3}
  [inst_2 : CommSemiring R] [inst_3 : Semiring A] [inst_4 : Semiring B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  [inst_7 : StarRing A] [inst_8 : StarRing B] [inst_9 : StarRing R] [inst_10 : StarModule R A]
  [inst_11 : StarModule R B] {m : Type u_4} [inst_12 : Fintype m] [inst_13 : DecidableEq m] {U : Matrix m m A}
  {V : Matrix n n B},
  U ∈ unitary (Matrix m m A) →
    V ∈ unitary (Matrix n n B) →
      Matrix.kroneckerMap (TensorProduct.tmul R) U V ∈ unitary (Matrix (m × n) (m × n) (TensorProduct R A B))
-- Init.Data.Int.Linear
Int.Internal.Linear.cooper_left_split_dvd_cert.eq_1 : ∀ (p₁ p' : Int.Internal.Linear.Poly) (a k : ℤ),
  Int.Internal.Linear.cooper_left_split_dvd_cert p₁ p' a k = (a.beq' p₁.leadCoeff).and' (p'.beq' (p₁.tail.addConst_k k))
-- Mathlib.SetTheory.ZFC.Rank
PSet.rank_le_iff : ∀ {o : Ordinal.{u_1}} {x : PSet.{u_1}}, x.rank ≤ o ↔ ∀ ⦃y : PSet.{u_1}⦄, y ∈ x → y.rank < o
-- Mathlib.Analysis.Hofer
_private.Mathlib.Analysis.Hofer.0.termD : Lean.ParserDescr
-- Mathlib.Analysis.Complex.UpperHalfPlane.Measure
UpperHalfPlane.instBorelSpace : BorelSpace UpperHalfPlane
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
ciInf_subtype_fun : ∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {ι : Type u_5} {s : Set ι} {f : ι → α},
  BddBelow (Set.range fun i => f ↑i) → ⨅ i, f ↑i ≤ sInf ∅ → ⨅ i, f ↑i = ⨅ t ∈ s, f t
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey!_inter_of_contains_eq_false_right : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [inst : Inhabited α]
  [Std.TransOrd α] (h₁ : m₁.WF),
  m₂.WF → ∀ {k : α}, Std.DTreeMap.Internal.Impl.contains k m₂ = false → (m₁.inter m₂ ⋯).getKey! k = default
-- Mathlib.Algebra.Order.Archimedean.Class
FiniteArchimedeanClass.congrOrderIso.eq_1 : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] {N : Type u_2}
  [inst_3 : AddCommGroup N] [inst_4 : LinearOrder N] [inst_5 : IsOrderedAddMonoid N]
  (e : ArchimedeanClass M ≃o ArchimedeanClass N),
  FiniteArchimedeanClass.congrOrderIso e = { toEquiv := (↑e).subtypeEquiv ⋯, map_rel_iff' := ⋯ }
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instReprCompletionItemKind : Repr Lean.Lsp.CompletionItemKind
-- Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
SSet.PtSimplex.MulStruct.δ_succ_castSucc_map : ∀ {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} {f g fg : X.PtSimplex n x} {i : Fin n}
  (self : f.MulStruct g fg i), CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ i.castSucc.succ) self.map = fg.map
-- Std.Data.Internal.List.Associative
Std.Internal.List.DistinctKeys.filterMap : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} [inst : BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)}
  {f : (a : α) → β a → Option (γ a)},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.DistinctKeys (List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) l)
-- Mathlib.RingTheory.DividedPowers.SubDPIdeal
DividedPowers.SubDPIdeal.mk : {A : Type u_1} →
  [inst : CommSemiring A] →
    {I : Ideal A} →
      {hI : DividedPowers I} →
        (carrier : Ideal A) → carrier ≤ I → (∀ (n : ℕ), n ≠ 0 → ∀ j ∈ carrier, hI.dpow n j ∈ carrier) → hI.SubDPIdeal