mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Metric
TensorialAt.mkHom₂.congr_simp : ∀ {𝕜 : 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 I_1 : ModelWithCorners 𝕜 E H}
  (e_I : I = I_1) {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]
  {F' : Type u_7} [inst_13 : NormedAddCommGroup F'] [inst_14 : NormedSpace 𝕜 F'] {V' : M → Type u_8}
  [inst_15 : TopologicalSpace (Bundle.TotalSpace F' V')] [inst_16 : (x : M) → AddCommGroup (V' x)]
  [inst_17 : (x : M) → Module 𝕜 (V' x)] [inst_18 : (x : M) → TopologicalSpace (V' x)] [inst_19 : FiberBundle F' V']
  {A : Type u_9} [inst_20 : AddCommGroup A] [inst_21 : Module 𝕜 A] [inst_22 : VectorBundle 𝕜 F V]
  [inst_23 : VectorBundle 𝕜 F' V'] [inst_24 : CompleteSpace 𝕜] [inst_25 : FiniteDimensional 𝕜 F]
  [inst_26 : FiniteDimensional 𝕜 F'] [inst_27 : ContMDiffVectorBundle 1 F V I]
  [inst_28 : ContMDiffVectorBundle 1 F' V' I] [inst_29 : TopologicalSpace A] [inst_30 : IsTopologicalAddGroup A]
  [inst_31 : ContinuousSMul 𝕜 A] (Φ Φ_1 : ((x : M) → V x) → ((x : M) → V' x) → A) (e_Φ : Φ = Φ_1) (x : M)
  (hΦ₁ : ∀ (τ : (x : M) → V' x), MDiffAt (T% τ) x → TensorialAt I F (fun x => Φ x τ) x)
  (hΦ₂ : ∀ (σ : (x : M) → V x), MDiffAt (T% σ) x → TensorialAt I F' (Φ σ) x),
  TensorialAt.mkHom₂ Φ x hΦ₁ hΦ₂ = TensorialAt.mkHom₂ Φ_1 x ⋯ ⋯
-- Mathlib.Logic.Equiv.List
/-- If `α` is equivalent to `ℕ`, then `List α` is equivalent to `α`.  -/
Equiv.listEquivSelfOfEquivNat : {α : Type u_1} → α ≃ ℕ → List α ≃ α
-- Mathlib.Logic.Equiv.Sum
Equiv.Perm.sumCongr_symm : ∀ {α : Type u_9} {β : Type u_10} (e : Equiv.Perm α) (f : Equiv.Perm β),
  Equiv.symm (e.sumCongr f) = Equiv.Perm.sumCongr (Equiv.symm e) (Equiv.symm f)
-- Mathlib.RingTheory.DividedPowerAlgebra.Init
DividedPowerAlgebra.LinearMap.dp_add : ∀ {R : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {S : Type u_4}
  [inst_3 : CommSemiring S] {N : Type u_5} [inst_4 : AddCommMonoid N] [inst_5 : Module R N] [inst_6 : Module S N]
  (f : M →ₗ[R] N) {n : ℕ} {a b : M},
  DividedPowerAlgebra.dp S n (f (a + b)) =
    ∑ k ∈ Finset.HasAntidiagonal.antidiagonal n, DividedPowerAlgebra.dp S k.1 (f a) * DividedPowerAlgebra.dp S k.2 (f b)
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.erase.congr_simp : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  (m m_1 : Std.ExtHashSet α), m = m_1 → ∀ (a a_1 : α), a = a_1 → m.erase a = m_1.erase a_1
-- Lean.Elab.Quotation.Util
Lean.Elab.Term.Quotation.getAntiquotationIds : Lean.Syntax → Lean.Elab.TermElabM (Array Lean.Ident)
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
/-- The point in a simplex constructed with `mkOfPoint`.  -/
Affine.Simplex.mkOfPoint_points : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_5} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] (p : P) (i : Fin 1), (Affine.Simplex.mkOfPoint k p).points i = p
-- Mathlib.CategoryTheory.Monoidal.Multifunctor
CategoryTheory.Functor.LaxMonoidal.ofBifunctor.firstMap₃_app_app_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {D : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor C D) (X X_1 X_2 : C),
  (((CategoryTheory.Functor.LaxMonoidal.ofBifunctor.firstMap₃ F).app X).app X_1).app X_2 =
    F.map (CategoryTheory.MonoidalCategoryStruct.associator X X_1 X_2).hom
-- Lean.Meta.Sym.Arith.Poly
/-- Given `m₁` and `m₂` such that `m₂.divides m₁`, then
`m₁.div m₂` returns the result.
Example `w.x^3.y^2.z` div `x^2.z` returns `w.x.y^2`
 -/
Lean.Grind.CommRing.Mon.div : Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Mon
-- Mathlib.FieldTheory.Separable
IsSeparable.of_equiv_equiv : ∀ {A₁ : Type u_1} {B₁ : Type u_2} {A₂ : Type u_3} {B₂ : Type u_4} [inst : Field A₁] [inst_1 : Ring B₁]
  [inst_2 : Field A₂] [inst_3 : Ring B₂] [inst_4 : Algebra A₁ B₁] [inst_5 : Algebra A₂ B₂] (e₁ : A₁ ≃+* A₂)
  (e₂ : B₁ ≃+* B₂),
  (algebraMap A₂ B₂).comp ↑e₁ = (↑e₂).comp (algebraMap A₁ B₁) → ∀ {x : B₁}, IsSeparable A₁ x → IsSeparable A₂ (e₂ x)
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra
CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence_unitIso_inv_app_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F :
    CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ)
      (CategoryTheory.Bicategory.Adj CategoryTheory.Cat))
  (ι : Type u_1) [inst_1 : Unique ι] {X S : C} (f : X ⟶ S) (X_1 : F.DescentDataAsCoalgebra fun x => f) (i : ι),
  ((CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence F ι f).unitIso.inv.app X_1).hom i =
    CategoryTheory.eqToHom ⋯
-- Mathlib.CategoryTheory.Monoidal.CommMon_
/-- Construct an isomorphism of commutative monoid objects by giving a monoid isomorphism between
the underlying objects.  -/
CategoryTheory.CommMon.mkIso' : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        {M N : C} →
          (e : M ≅ N) →
            [inst_3 : CategoryTheory.MonObj M] →
              [inst_4 : CategoryTheory.IsCommMonObj M] →
                [inst_5 : CategoryTheory.MonObj N] →
                  [inst_6 : CategoryTheory.IsCommMonObj N] →
                    [CategoryTheory.IsMonHom e.hom] →
                      { X := M, mon := inst_3, comm := inst_4 } ≅ { X := N, mon := inst_5, comm := inst_6 }
-- Lean.Environment
Lean.PersistentEnvExtensionDescr.mk.inj : ∀ {α β σ : Type} {toPersistentEnvExtensionDescrCore : Lean.PersistentEnvExtensionDescrCore α β σ}
  {exportEntriesFn : σ → Array α} {toPersistentEnvExtensionDescrCore_1 : Lean.PersistentEnvExtensionDescrCore α β σ}
  {exportEntriesFn_1 : σ → Array α},
  { toPersistentEnvExtensionDescrCore := toPersistentEnvExtensionDescrCore, exportEntriesFn := exportEntriesFn } =
      { toPersistentEnvExtensionDescrCore := toPersistentEnvExtensionDescrCore_1,
        exportEntriesFn := exportEntriesFn_1 } →
    toPersistentEnvExtensionDescrCore = toPersistentEnvExtensionDescrCore_1 ∧ exportEntriesFn = exportEntriesFn_1
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
/-- Additively isomorphic rings have additively isomorphic monoid algebras.

`MonoidAlgebra.map` as an `AddEquiv`.  -/
MonoidAlgebra.mapAddEquiv : {R : Type u_3} →
  {S : Type u_4} →
    (M : Type u_6) →
      [inst : Semiring R] → [inst_1 : Semiring S] → [inst_2 : Mul M] → R ≃+ S → MonoidAlgebra R M ≃+ MonoidAlgebra S M
-- Mathlib.Algebra.Lie.Weights.Chain
LieModule.genWeightSpace_chainBotCoeff_sub_one_zsmul_sub : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {M : Type u_3}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] [inst_8 : IsAddTorsionFree R] [inst_9 : IsDomain R]
  [inst_10 : Module.IsTorsionFree R M] [inst_11 : IsNoetherian R M] (α : L → R) (β : LieModule.Weight R L M),
  α ≠ 0 → LieModule.genWeightSpace M ((-↑(LieModule.chainBotCoeff α β) - 1) • α + ⇑β) = ⊥
-- Mathlib.Analysis.InnerProductSpace.Projection.Reflection
_private.Mathlib.Analysis.InnerProductSpace.Projection.Reflection.0.Submodule.«term⟪_,_⟫» : Lean.ParserDescr
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
/-- A ring homomorphism ``f : R →+* S`` induces a homomorphism ``GLₙ(f) : GLₙ(R) →* GLₙ(S)``.  -/
Matrix.GeneralLinearGroup.map : {n : Type u} →
  [inst : DecidableEq n] →
    [inst_1 : Fintype n] →
      {R : Type v} → [inst_2 : CommRing R] → {S : Type u_1} → [inst_3 : CommRing S] → (R →+* S) → GL n R →* GL n S
-- Mathlib.Data.Finset.NAry
Finset.image₂_image_left : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} [inst : DecidableEq γ] {s : Finset α} {t : Finset β}
  [inst_1 : DecidableEq δ] (f : γ → β → δ) (g : α → γ),
  Finset.image₂ f (Finset.image g s) t = Finset.image₂ (fun a b => f (g a) b) s t
-- Mathlib.Order.ModularLattice
sup_strictMonoOn_Icc_inf : ∀ {α : Type u_1} [inst : Lattice α] [IsModularLattice α] {a b : α}, StrictMonoOn (fun c => c ⊔ b) (Set.Icc (a ⊓ b) a)
-- Mathlib.Data.Set.Basic
Set.lt_eq_ssubset : ∀ {α : Type u}, (fun x1 x2 => x1 ⊂ x2) = fun x1 x2 => x1 ⊂ x2
-- Mathlib.Data.Tree.Basic
BinaryTree.traverse.eq_def : ∀ {m : Type u_1 → Type u_2} [inst : Applicative m] {α : Type u_3} {β : Type u_1} (f : α → m β) (x : BinaryTree α),
  BinaryTree.traverse f x =
    match x with
    | BinaryTree.nil => pure BinaryTree.nil
    | BinaryTree.node a l r => BinaryTree.node <$> f a <*> BinaryTree.traverse f l <*> BinaryTree.traverse f r
-- Init.Data.Nat.Bitwise.Lemmas
Nat.testBit_of_two_pow_le_and_two_pow_add_one_gt : ∀ {n i : ℕ}, 2 ^ i ≤ n → n < 2 ^ (i + 1) → n.testBit i = true
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof : Type
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.length_toList : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → m.toList.length = m.size
-- Mathlib.RingTheory.Ideal.Operations
/-- A product of ideals in an integral domain is zero if and only if one of the terms is zero.  -/
Ideal.multiset_prod_eq_bot : ∀ {R : Type u_2} [inst : CommSemiring R] [IsDomain R] {s : Multiset (Ideal R)}, s.prod = ⊥ ↔ ⊥ ∈ s
-- Mathlib.Topology.Category.UniformSpace
UniformSpaceCat.of.inj : ∀ {carrier : Type u} {str : UniformSpace carrier} {carrier_1 : Type u} {str_1 : UniformSpace carrier_1},
  { carrier := carrier, str := str } = { carrier := carrier_1, str := str_1 } → carrier = carrier_1 ∧ str ≍ str_1
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.homotopyCofiber.mapArrowHom_comp_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {F G : HomologicalComplex C c} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ]
  [inst_3 : DecidableRel c.Rel] {F' F'' G' G'' : HomologicalComplex C c} (φ' : F' ⟶ G') (φ'' : F'' ⟶ G'')
  [inst_4 : HomologicalComplex.HasHomotopyCofiber φ'] [inst_5 : HomologicalComplex.HasHomotopyCofiber φ'']
  (H : ∀ (j : ι), ∃ i, c.Rel i j) (α : CategoryTheory.Arrow.mk φ ⟶ CategoryTheory.Arrow.mk φ')
  (β : CategoryTheory.Arrow.mk φ' ⟶ CategoryTheory.Arrow.mk φ'') {Z : HomologicalComplex C c}
  (h : HomologicalComplex.homotopyCofiber φ'' ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (HomologicalComplex.homotopyCofiber.mapArrowHom φ φ'' H (CategoryTheory.CategoryStruct.comp α β)) h =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.mapArrowHom φ φ' H α)
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.mapArrowHom φ' φ'' H β) h)
-- Mathlib.Algebra.Group.Basic
sub_eq_iff_comm : ∀ {G : Type u_3} [inst : AddCommGroup G] {a b c : G}, a - b = c ↔ a - c = b
-- Mathlib.Order.ScottContinuity.Prod
ScottContinuous.fromProd : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  {f : α × β → γ},
  (∀ (a : α), ScottContinuous fun b => f (a, b)) → (∀ (b : β), ScottContinuous fun a => f (a, b)) → ScottContinuous f
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.Equiv.diff_left : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] {t₃ : Std.TreeSet.Raw α cmp},
  t₁.WF → t₂.WF → t₃.WF → t₁.Equiv t₂ → (t₁ \ t₃).Equiv (t₂ \ t₃)
-- Mathlib.CategoryTheory.SmallObject.Construction
/-- the bottom morphism in the square  -/
CategoryTheory.SmallObject.FunctorObjIndex.b : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {I : Type w} →
      {A B : I → C} →
        {f : (i : I) → A i ⟶ B i} →
          {S X : C} → {πX : X ⟶ S} → (self : CategoryTheory.SmallObject.FunctorObjIndex f πX) → B self.i ⟶ S
-- Mathlib.NumberTheory.LSeries.Deriv
/-- If the L-series of `f` is summable at `s` and `re s < re s'`, then the L-series of the
point-wise product of `log` with `f` is summable at `s'`.  -/
LSeriesSummable_logMul_of_lt_re : ∀ {f : ℕ → ℂ} {s : ℂ}, LSeries.abscissaOfAbsConv f < ↑s.re → LSeriesSummable (LSeries.logMul f) s
-- Mathlib.Data.Set.Image
Set.eq_preimage_subtype_val_iff : ∀ {α : Type u_1} {p : α → Prop} {s : Set (Subtype p)} {t : Set α},
  s = Subtype.val ⁻¹' t ↔ ∀ (x : α) (h : p x), ⟨x, h⟩ ∈ s ↔ x ∈ t
-- Mathlib.Data.Nat.Cast.Order.Basic
Nat.one_le_cast : ∀ {α : Type u_1} [inst : AddMonoidWithOne α] [inst_1 : PartialOrder α] [AddLeftMono α] [ZeroLEOneClass α] [CharZero α]
  {n : ℕ}, 1 ≤ ↑n ↔ 1 ≤ n
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKeyD_inter_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k fallback : α}, k ∉ t₁ → (t₁ ∩ t₂).getKeyD k fallback = fallback
-- Mathlib.CategoryTheory.Subobject.Lattice
CategoryTheory.Subobject.map_bot : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasInitial C]
  [inst_2 : CategoryTheory.Limits.InitialMonoClass C] (f : X ⟶ Y) [inst_3 : CategoryTheory.Mono f],
  (CategoryTheory.Subobject.map f).obj ⊥ = ⊥
-- Aesop.Saturate
Aesop.Stateful.saturateCore : Aesop.LocalRuleSet → Lean.MVarId → Aesop.SaturateM Lean.MVarId
-- Init.Data.Option.Basic
Option.orElse_none : ∀ {α : Type u_1} {b : Unit → Option α}, none.orElse b = b ()
-- Lean.Parser.Basic
/-- `withForbidden tk p` runs `p` with `tk` as a "forbidden token". This means that if the token
appears anywhere in `p` (unless it is nested in `withoutForbidden`), parsing will immediately
stop there, making `tk` effectively a lowest-precedence operator. This is used for parsers like
`for x in arr do ...`: `arr` is parsed as `withForbidden "do" term` because otherwise `arr do ...`
would be treated as an application.

This parser has the same arity as `p` - it just forwards the results of `p`.  -/
Lean.Parser.withForbidden : Lean.Parser.Token → Lean.Parser.Parser → Lean.Parser.Parser
-- Lean.Meta.SynthInstance
Lean.Meta.throwFailedToSynthesize : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- A colimit cocone extended by an isomorphism is a colimit cocone.  -/
CategoryTheory.Limits.IsColimit.extendIso : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          {s : CategoryTheory.Limits.Cocone F} →
            {X : C} →
              (i : s.pt ⟶ X) →
                [CategoryTheory.IsIso i] →
                  CategoryTheory.Limits.IsColimit s → CategoryTheory.Limits.IsColimit (s.extend i)
-- Mathlib.Data.Finset.Image
Finset.empty_eq_map : ∀ {α : Type u_1} {β : Type u_2} {f : α ↪ β} {s : Finset α}, ∅ = Finset.map f s ↔ s = ∅
-- Mathlib.FieldTheory.PolynomialGaloisGroup
Polynomial.Gal.instAlgebraSplittingFieldOfFactSplitsMapAlgebraMap : {F : Type u_1} →
  [inst : Field F] →
    (p : Polynomial F) →
      (E : Type u_2) →
        [inst_1 : Field E] →
          [inst_2 : Algebra F E] → [h : Fact (Polynomial.map (algebraMap F E) p).Splits] → Algebra p.SplittingField E
-- Mathlib.GroupTheory.SemidirectProduct
SemidirectProduct.inr_inj : ∀ {N : Type u_1} {G : Type u_2} [inst : Group N] [inst_1 : Group G] {φ : G →* MulAut N} {g₁ g₂ : G},
  SemidirectProduct.inr g₁ = SemidirectProduct.inr g₂ ↔ g₁ = g₂
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
HasDerivAt.const_cpow : ∀ {f : ℂ → ℂ} {f' x c : ℂ},
  HasDerivAt f f' x → c ≠ 0 ∨ f x ≠ 0 → HasDerivAt (fun x => c ^ f x) (c ^ f x * Complex.log c * f') x
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Fintype.sum_fiberwise : ∀ {M : Type u_4} {κ : Type u_6} {ι : Type u_7} [inst : Fintype ι] [inst_1 : Fintype κ] [inst_2 : AddCommMonoid M]
  [inst_3 : DecidableEq κ] (g : ι → κ) (f : ι → M), ∑ j, ∑ i, f ↑i = ∑ i, f i
-- Mathlib.Order.InitialSeg
InitialSeg.eq_relIso : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder β s] (f : InitialSeg r s)
  (g : r ≃r s) (a : α), g a = f a
-- Mathlib.Topology.Algebra.Group.SubmonoidClosure
mapClusterPt_atTop_zpow_iff_pow : ∀ {G : Type u_1} [inst : DivInvMonoid G] [inst_1 : TopologicalSpace G] {x y : G},
  (MapClusterPt x Filter.atTop fun x => y ^ x) ↔ MapClusterPt x Filter.atTop fun x => y ^ x
-- Init.Data.List.Impl
List.zipWith_eq_zipWithTR : @List.zipWith = @List.zipWithTR
-- Mathlib.Data.Finset.Image
Finset.map_injective : ∀ {α : Type u_1} {β : Type u_2} (f : α ↪ β), Function.Injective (Finset.map f)
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor
PresheafOfModules.ModuleColimit.homEquiv_naturality_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C]
  [inst_2 : CategoryTheory.IsCofiltered C] [inst_3 : CategoryTheory.InitiallySmall C]
  {R : CategoryTheory.Functor Cᵒᵖ RingCat} {cR : CategoryTheory.Limits.Cocone R}
  (hcR : CategoryTheory.Limits.IsColimit cR) {M : PresheafOfModules R} {cM : CategoryTheory.Limits.Cocone M.presheaf}
  (hcM : CategoryTheory.Limits.IsColimit cM) {N N' : ModuleCat ↑cR.pt}
  (φ : ModuleCat.of (↑cR.pt) (PresheafOfModules.ModuleColimit hcR hcM) ⟶ N) (g : N ⟶ N'),
  (PresheafOfModules.ModuleColimit.homEquiv hcR hcM) (CategoryTheory.CategoryStruct.comp φ g) =
    CategoryTheory.CategoryStruct.comp ((PresheafOfModules.ModuleColimit.homEquiv hcR hcM) φ)
      ((PresheafOfModules.constFunctor cR).map g)
-- Std.Data.DHashMap.Raw
/-- Internal implementation detail of the hash map.

Folds the given function over the mappings in the hash map in the reverse order used
by `foldM`.  -/
Std.DHashMap.Raw.Internal.foldRev : {α : Type u} → {β : α → Type v} → {δ : Type w} → (δ → (a : α) → β a → δ) → δ → Std.DHashMap.Raw α β → δ
-- Lean.Data.NameMap.Basic
Lean.NameSet.empty : Lean.NameSet
-- Mathlib.RingTheory.Nilpotent.Exp
IsNilpotent.exp_smul : ∀ {A : Type u_1} [inst : Ring A] [inst_1 : Module ℚ A] {G : Type u_2} [inst_2 : Monoid G]
  [inst_3 : MulSemiringAction G A] (g : G) {a : A}, IsNilpotent a → IsNilpotent.exp (g • a) = g • IsNilpotent.exp a
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Real.iteratedDeriv_even_sin : ∀ (n : ℕ), iteratedDeriv (2 * n) Real.sin = (-1) ^ n * Real.sin
-- Init.Data.List.Lemmas
/-- Variant of `append_inj_left` instead requiring equality of the lengths of the second lists.  -/
List.append_inj_left' : ∀ {α : Type u_1} {s₁ t₁ s₂ t₂ : List α}, s₁ ++ t₁ = s₂ ++ t₂ → t₁.length = t₂.length → s₁ = s₂
-- Lean.Meta.Tactic.Grind.MatchDiscrOnly
/-- Erases `Grind.simpMatchDiscrsOnly` annotations.  -/
Lean.Meta.Grind.eraseSimpMatchDiscrsOnly : Lean.Expr → Lean.MetaM Lean.Meta.Simp.Result
-- Lean.Log
/-- Log a new information message using the given message data. The position is provided by `ref`.  -/
Lean.logInfoAt : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadLog m] → [Lean.AddMessageContext m] → [Lean.MonadOptions m] → Lean.Syntax → Lean.MessageData → m Unit
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.SavedState.mk : Lean.Meta.SavedState → Lean.Meta.Grind.State → Lean.Meta.Grind.SavedState
-- Mathlib.RingTheory.Extension.Presentation.Core
/-- (Implementation detail): The underlying `AlgHom` of `tensorModelOfHasCoeffsEquiv`.  -/
Algebra.Presentation.tensorModelOfHasCoeffsHom : {R : Type u_1} →
  {S : Type u_2} →
    {ι : Type u_3} →
      {σ : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : CommRing S] →
            [inst_2 : Algebra R S] →
              (P : Algebra.Presentation R S ι σ) →
                (R₀ : Type u_5) →
                  [inst_3 : CommRing R₀] →
                    [inst_4 : Algebra R₀ R] →
                      [inst_5 : Algebra R₀ S] →
                        [inst_6 : IsScalarTower R₀ R S] →
                          [inst_7 : P.HasCoeffs R₀] →
                            TensorProduct R₀ R (Algebra.Presentation.ModelOfHasCoeffs R₀) →ₐ[R] S
-- Mathlib.Analysis.Convolution
/-- The convolution of two functions with respect to a bilinear operation `L` and a measure `μ`.  -/
Convolution.«term_⋆[_,_]_» : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.leftUnitor_inv_braiding : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X : C),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv
      (β_ (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X).hom =
    (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv
-- Mathlib.CategoryTheory.Enriched.Ordinary.Basic
/-- Whiskering commutes with the enriched composition.  -/
CategoryTheory.eComp_eHomWhiskerLeft_assoc : ∀ (V : Type u') [inst : CategoryTheory.Category.{v', u'} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u}
  [inst_2 : CategoryTheory.Category.{v, u} C] [inst_3 : CategoryTheory.EnrichedOrdinaryCategory V C] (X Y : C)
  {Z Z' : C} (g : Z ⟶ Z') {Z_1 : V} (h : (X ⟶[V] Z') ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V X Y Z)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.eHomWhiskerLeft V X g) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (X ⟶[V] Y) (CategoryTheory.eHomWhiskerLeft V Y g))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V X Y Z') h)
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
QuasispectrumRestricts.mk : ∀ {R : Type u_3} {S : Type u_4} {A : Type u_5} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : NonUnitalRing A] [inst_3 : Module R A] [inst_4 : Module S A] [inst_5 : Algebra R S] {a : A} {f : S → R},
  Set.RightInvOn f (⇑(algebraMap R S)) (quasispectrum S a) →
    Function.LeftInverse f ⇑(algebraMap R S) → QuasispectrumRestricts a f
-- Mathlib.Order.KrullDimension
Order.coheight_coe_enat : ∀ (n : ℕ), Order.coheight ↑n = ⊤
-- Mathlib.Order.SymmDiff
bihimp_right_injective : ∀ {α : Type u_2} [inst : BooleanAlgebra α] (a : α), Function.Injective fun x => bihimp a x
-- Mathlib.Algebra.Algebra.Opposite
AlgEquiv.opComm_apply_symm_apply : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (a : A ≃ₐ[R] Bᵐᵒᵖ) (a_1 : B),
  (AlgEquiv.opComm a).symm a_1 = MulOpposite.op (a.symm (MulOpposite.op a_1))
-- Mathlib.CategoryTheory.Shift.Basic
CategoryTheory.instMonoidalDiscreteFunctorShiftMonoidalFunctor : (C : Type u) →
  (A : Type u_1) →
    [inst : CategoryTheory.Category.{v, u} C] →
      [inst_1 : AddMonoid A] →
        [inst_2 : CategoryTheory.HasShift C A] → (CategoryTheory.shiftMonoidalFunctor C A).Monoidal
-- Mathlib.CategoryTheory.Types.Basic
TypeCat.instFunLikeFun : {X : Type u_1} → {Y : Type u_2} → FunLike (TypeCat.Fun X Y) X Y
-- Mathlib.CategoryTheory.Limits.Creates
/-- Define the lift of a cone: For a cone `c` for `K ⋙ F`, give a cone for `K`
which is a lift of `c`, i.e. the image of it under `F` is (iso) to `c`.

We will then use this as part of the definition of creation of limits:
every limit cone has a lift.

Note this definition is really only useful when `c` is a limit already.
 -/
CategoryTheory.LiftableCone : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : Type w} →
          [inst_2 : CategoryTheory.Category.{w', w} J] →
            (K : CategoryTheory.Functor J C) →
              (F : CategoryTheory.Functor C D) →
                CategoryTheory.Limits.Cone (K.comp F) → Type (max (max (max u₁ v₁) v₂) w)
-- Mathlib.RingTheory.PowerSeries.Trunc
PowerSeries.trunc_apply : ∀ {R : Type u_1} [inst : Semiring R] (n : ℕ) (φ : PowerSeries R),
  (PowerSeries.trunc n) φ = ∑ m ∈ Finset.Ico 0 n, (Polynomial.monomial m) ((PowerSeries.coeff m) φ)