mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Analytic.Constructions
/-- Analytic functions on products are analytic in the second coordinate  -/
AnalyticOnNhd.curry_right : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} {G : Type u_5}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E × F → G} {x : E} {s : Set (E × F)},
  AnalyticOnNhd 𝕜 f s → AnalyticOnNhd 𝕜 (fun y => f (x, y)) {y | (x, y) ∈ s}
-- Mathlib.Algebra.Polynomial.RuleOfSigns
/-- This lemma is really a specialization of `succ_signVariations_le_sub_mul` to monomials.  -/
Polynomial.succ_signVariations_X_sub_C_mul_monomial : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] {η : R} {d : ℕ} {c : R},
  c ≠ 0 →
    0 < η →
      ((Polynomial.monomial d) c).signVariations + 1 ≤
        ((Polynomial.X - Polynomial.C η) * (Polynomial.monomial d) c).signVariations
-- Mathlib.SetTheory.Ordinal.Rank
WellFoundedLT.rank_strictMono : ∀ {α : Type u} [inst : Preorder α] [inst_1 : WellFoundedLT α], StrictMono (IsWellFounded.rank fun x1 x2 => x1 < x2)
-- Mathlib.Data.Real.Sign
Real.sign_zero : Real.sign 0 = 0
-- Init.GrindInstances.ToInt
Lean.Grind.instMulUInt32UintOfNatNat : Lean.Grind.ToInt.Mul UInt32 (Lean.Grind.IntInterval.uint 32)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.isEmpty_filterMap_eq_false_iff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} {γ : α → Type w} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {f : (a : α) → β a → Option (γ a)},
  (Std.DTreeMap.filterMap f t).isEmpty = false ↔ ∃ k, ∃ (h : k ∈ t), (f k (t.get k h)).isSome = true
-- Mathlib.Algebra.Group.Equiv.TypeTags
MulEquiv.multiplicativeAdditive_apply : ∀ (H : Type u_3) [inst : MulOneClass H] (a : Multiplicative (Additive H)),
  (MulEquiv.multiplicativeAdditive H) a = Additive.toMul (Multiplicative.toAdd a)
-- Batteries.Tactic.Lint.Basic
_private.Batteries.Tactic.Lint.Basic.0.Batteries.Tactic.Lint.getLinter.unsafe_1 : Lean.Name → Lean.Name → Lean.CoreM Batteries.Tactic.Lint.NamedLinter
-- Mathlib.Order.Defs.LinearOrder
lt_iff_not_ge : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, a < b ↔ ¬b ≤ a
-- Mathlib.Algebra.BigOperators.Finprod
finsum_eq_sum_of_support_subset : ∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] (f : α → M) {s : Finset α},
  Function.support f ⊆ ↑s → ∑ᶠ (i : α), f i = ∑ i ∈ s, f i
-- Mathlib.Computability.Encoding
/-- A unary `Encoding` of `ℕ` in `Bool`.  -/
Computability.unaryEncodingNat : Computability.Encoding ℕ Bool
-- Mathlib.Order.SuccPred.Basic
Order.succ_lt_succ_of_not_isMax : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] {a b : α}, a < b → ¬IsMax b → Order.succ a < Order.succ b
-- Mathlib.Analysis.Complex.Trigonometric
Complex.exp_sub_sinh : ∀ (x : ℂ), Complex.exp x - Complex.sinh x = Complex.cosh x
-- Init.Data.UInt.Lemmas
UInt16.lt_iff_le_and_ne : ∀ {a b : UInt16}, a < b ↔ a ≤ b ∧ a ≠ b
-- Mathlib.CategoryTheory.Subobject.Limits
/-- Taking cokernels is an order-reversing map from the subobjects of `X` to the quotient objects
of `X`.  -/
CategoryTheory.Limits.cokernelOrderHom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      [CategoryTheory.Limits.HasCokernels C] →
        (X : C) → CategoryTheory.Subobject X →o (CategoryTheory.Subobject (Opposite.op X))ᵒᵈ
-- Mathlib.Algebra.Star.LinearMap
LinearMap.intrinsicStar_rTensor : ∀ {R : Type u_5} {E : Type u_6} {F : Type u_7} {G : Type u_8} [inst : CommSemiring R] [inst_1 : StarRing R]
  [inst_2 : AddCommMonoid E] [inst_3 : StarAddMonoid E] [inst_4 : Module R E] [inst_5 : StarModule R E]
  [inst_6 : AddCommMonoid F] [inst_7 : StarAddMonoid F] [inst_8 : Module R F] [inst_9 : StarModule R F]
  [inst_10 : AddCommMonoid G] [inst_11 : StarAddMonoid G] [inst_12 : Module R G] [inst_13 : StarModule R G]
  (f : WithConv (E →ₗ[R] F)),
  star (WithConv.toConv (LinearMap.rTensor G f.ofConv)) = WithConv.toConv (LinearMap.rTensor G (star f).ofConv)
-- Mathlib.RepresentationTheory.FinGroupCharZero
/-- If `G` is finite and its order is nonzero in an algebraically closed field `k`,
then an object of `FDRep k G` is simple if and only if its space of endomorphisms is
a `k`-vector space of dimension `1`.
 -/
FDRep.simple_iff_end_is_rank_one : ∀ {k : Type u} [inst : Field k] {G : Type u} [Finite G] [inst_2 : Group G] [IsAlgClosed k] [NeZero ↑(Nat.card G)]
  (V : FDRep k G), CategoryTheory.Simple V ↔ Module.finrank k (V ⟶ V) = 1
-- Mathlib.GroupTheory.GroupAction.Hom
/-- Composition of two equivariant additive ring homomorphisms.  -/
MulSemiringActionHom.comp : {M : Type u_1} →
  [inst : Monoid M] →
    {N : Type u_2} →
      [inst_1 : Monoid N] →
        {P : Type u_3} →
          [inst_2 : Monoid P] →
            {φ : M →* N} →
              {ψ : N →* P} →
                {χ : M →* P} →
                  {R : Type u_10} →
                    [inst_3 : Semiring R] →
                      [inst_4 : MulSemiringAction M R] →
                        {S : Type u_12} →
                          [inst_5 : Semiring S] →
                            [inst_6 : MulSemiringAction N S] →
                              {T : Type u_14} →
                                [inst_7 : Semiring T] →
                                  [inst_8 : MulSemiringAction P T] →
                                    (S →ₑ+*[ψ] T) → (R →ₑ+*[φ] S) → [κ : φ.CompTriple ψ χ] → R →ₑ+*[χ] T
-- Mathlib.AlgebraicGeometry.Gluing
/-- (Implementation detail)
The cocone associated to a locally directed diagram.

One usually does not want to use this directly, and instead use the generic `colimit` API.
 -/
AlgebraicGeometry.Scheme.IsLocallyDirected.cocone : {J : Type w} →
  [inst : CategoryTheory.Category.{v, w} J] →
    (F : CategoryTheory.Functor J AlgebraicGeometry.Scheme) →
      [∀ {i j : J} (f : i ⟶ j), AlgebraicGeometry.IsOpenImmersion (F.map f)] →
        [(F.comp AlgebraicGeometry.Scheme.forget).IsLocallyDirected] →
          [Quiver.IsThin J] → [Small.{u, w} J] → CategoryTheory.Limits.Cocone F
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getD.congr_simp : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.LawfulEqCmp cmp] (t t_1 : Std.DTreeMap α β cmp),
  t = t_1 → ∀ (a : α) (fallback fallback_1 : β a), fallback = fallback_1 → t.getD a fallback = t_1.getD a fallback_1
-- Mathlib.Order.OrderIsoNat
/-- If `f` is a strictly `r`-increasing sequence, then this returns `f` as an order embedding.  -/
RelEmbedding.natLT : {α : Type u_1} →
  {r : α → α → Prop} →
    [IsStrictOrder α r] → (f : ℕ → α) → (∀ (n : ℕ), r (f n) (f (n + 1))) → (fun x1 x2 => x1 < x2) ↪r r
-- Mathlib.Geometry.Euclidean.Sphere.Tangent
EuclideanGeometry.Sphere.dist_orthogonalProjection_eq_radius_iff_isTangentAt : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {as : AffineSubspace ℝ P} [inst_4 : Nonempty ↥as]
  [inst_5 : as.direction.HasOrthogonalProjection],
  dist s.center ↑((EuclideanGeometry.orthogonalProjection as) s.center) = s.radius ↔
    s.IsTangentAt (↑((EuclideanGeometry.orthogonalProjection as) s.center)) as
-- Mathlib.Geometry.Manifold.IntegralCurve.Transform
isMIntegralCurve_comp_mul_ne_zero : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] {γ : ℝ → M}
  {v : (x : M) → TangentSpace I x} {a : ℝ},
  a ≠ 0 → (IsMIntegralCurve (γ ∘ fun x => x * a) (a • v) ↔ IsMIntegralCurve γ v)
-- Mathlib.Lean.Expr.Basic
/-- Given `f a b c`, return `#[f a, f a b, f a b c]`.
Each entry in the array is an `Expr.app`,
and this array has the same length as the one returned by `Lean.Expr.getAppArgs`.  -/
Lean.Expr.getAppApps : Lean.Expr → Array Lean.Expr
-- Mathlib.Order.DirSupClosed
dirSupClosed_compl : ∀ {α : Type u_1} {s : Set α} [inst : Preorder α], DirSupClosed sᶜ ↔ DirSupInacc s
-- Mathlib.Analysis.SpecialFunctions.Integrals.Basic
integral_cos_pow_aux : ∀ {a b : ℝ} (n : ℕ),
  ∫ (x : ℝ) in a..b, Real.cos x ^ (n + 2) =
    (Real.cos b ^ (n + 1) * Real.sin b - Real.cos a ^ (n + 1) * Real.sin a +
        (↑n + 1) * ∫ (x : ℝ) in a..b, Real.cos x ^ n) -
      (↑n + 1) * ∫ (x : ℝ) in a..b, Real.cos x ^ (n + 2)
-- Init.Data.List.Lemmas
List.foldr_eq_foldl : ∀ {α : Type u_1} {init : α} {xs : List α} {f : α → α → α} [Std.Associative f] [Std.LawfulIdentity f init],
  List.foldr f init xs = List.foldl f init xs
-- Mathlib.Topology.Algebra.Group.Extension
TopologicalAddGroup.IsSES.mk : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} [inst : AddGroup A] [inst_1 : AddGroup B] [inst_2 : AddGroup C]
  [inst_3 : TopologicalSpace A] [inst_4 : TopologicalSpace B] [inst_5 : TopologicalSpace C] {φ : A →+ B} {ψ : B →+ C},
  Topology.IsClosedEmbedding ⇑φ → IsOpenQuotientMap ⇑ψ → Function.Exact ⇑φ ⇑ψ → TopologicalAddGroup.IsSES φ ψ
-- Mathlib.RepresentationTheory.Intertwining
Representation.TensorProduct.assoc_symm_toLinearMap : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [inst : CommSemiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : AddCommMonoid U] [inst_5 : Module A V]
  [inst_6 : Module A W] [inst_7 : Module A U] (ρ : Representation A G V) (σ : Representation A G W)
  (τ : Representation A G U),
  (↑(Representation.TensorProduct.assoc ρ σ τ).symm).toLinearMap = ↑(TensorProduct.assoc A V W U).symm
-- Mathlib.Algebra.Category.Semigrp.Basic
MagmaCat.ofHom_hom : ∀ {M N : MagmaCat} (f : M ⟶ N), MagmaCat.ofHom (MagmaCat.Hom.hom f) = f
-- Init.Omega.LinearCombo
/-- Internal representation of a linear combination of atoms, and a constant term.  -/
Lean.Omega.LinearCombo : Type
-- Std.Http.Data.URI.Basic
Std.Http.URI.instInhabitedPath : Inhabited Std.Http.URI.Path
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.map.go.eq_2 : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} (f : (a : α) → β a → γ a) (acc : Std.DHashMap.Internal.AssocList α γ)
  (a : α) (b : β a) (es : Std.DHashMap.Internal.AssocList α β),
  Std.DHashMap.Internal.AssocList.map.go✝ f acc (Std.DHashMap.Internal.AssocList.cons a b es) =
    Std.DHashMap.Internal.AssocList.map.go✝ f (Std.DHashMap.Internal.AssocList.cons a (f a b) acc) es
-- Mathlib.Algebra.Order.Group.Synonym
toDual_div : ∀ {α : Type u_1} [inst : Div α] (a b : α), OrderDual.toDual (a / b) = OrderDual.toDual a / OrderDual.toDual b
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
CategoryTheory.Limits.FormalCoproduct.powerMap_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {U V W : CategoryTheory.Limits.FormalCoproduct C} (f : U ⟶ V)
  (g : V ⟶ W) (α : Type t) [inst_1 : CategoryTheory.Limits.HasProductsOfShape α C],
  CategoryTheory.Limits.FormalCoproduct.powerMap (CategoryTheory.CategoryStruct.comp f g) α =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.FormalCoproduct.powerMap f α)
      (CategoryTheory.Limits.FormalCoproduct.powerMap g α)
-- Mathlib.Geometry.Manifold.MFDeriv.FDeriv
writtenInExtChartAt_model_space : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {f : E → E'}
  {x : E}, writtenInExtChartAt (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') x f = f
-- Mathlib.Data.Finset.Image
/-- A version of `Finset.map_disjUnion` for writing in the other direction.  -/
Finset.map_disjUnion' : ∀ {α : Type u_1} {β : Type u_2} {f : α ↪ β} (s₁ s₂ : Finset α) (h' : Disjoint (Finset.map f s₁) (Finset.map f s₂))
  (h : optParam (Disjoint s₁ s₂) ⋯), Finset.map f (s₁.disjUnion s₂ h) = (Finset.map f s₁).disjUnion (Finset.map f s₂) h'
-- Init.Data.UInt.Log2
/-- Base-two logarithm of 32-bit unsigned integers. Returns `⌊max 0 (log₂ a)⌋`.

This function is overridden at runtime with an efficient implementation. This definition is
the logical model.

Examples:
 * `UInt32.log2 0 = 0`
 * `UInt32.log2 1 = 0`
 * `UInt32.log2 2 = 1`
 * `UInt32.log2 4 = 2`
 * `UInt32.log2 7 = 2`
 * `UInt32.log2 8 = 3`
 -/
UInt32.log2 : UInt32 → UInt32
-- Mathlib.NumberTheory.Real.Irrational
Irrational.eq_1 : ∀ (x : ℝ), Irrational x = (x ∉ Set.range Rat.cast)
-- Mathlib.Logic.Basic
forall_apply_eq_imp_iff' : ∀ {α : Sort u_1} {β : Sort u_2} {f : α → β} {p : β → Prop}, (∀ (a : α) (b : β), f a = b → p b) ↔ ∀ (a : α), p (f a)
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.SimpCacheKey.mk.sizeOf_spec : ∀ (variant : Lean.Name) (extras : Array Lean.Elab.Tactic.Grind.ExtraTheorem),
  sizeOf { variant := variant, extras := extras } = 1 + sizeOf variant + sizeOf extras
-- Std.Data.HashSet.Lemmas
Std.HashSet.mem_union_of_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {k : α},
  k ∈ m₂ → k ∈ m₁ ∪ m₂
-- Mathlib.LinearAlgebra.Eigenspace.Pi
Module.End.mem_iInf_maxGenEigenspace_iff : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (f : ι → Module.End R M) (χ : ι → R) (m : M),
  m ∈ ⨅ i, (f i).maxGenEigenspace (χ i) ↔ ∀ (j : ι), ∃ k, ((f j - χ j • 1) ^ k) m = 0
-- Mathlib.CategoryTheory.MorphismProperty.Limits
/-- `P.HasPullbacksAlong f` states that for any morphism satisfying `P` with the same codomain
as `f`, the pullback of that morphism along `f` exists.  -/
CategoryTheory.MorphismProperty.HasPullbacksAlong : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.MorphismProperty C → {X Y : C} → (X ⟶ Y) → Prop
-- Mathlib.RingTheory.PolynomialLaw.Basic
PolynomialLaw.comp_toFun' : ∀ {R : Type u} [inst : CommSemiring R] {M : Type u_1} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_2}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {P : Type u_3} [inst_5 : AddCommMonoid P] [inst_6 : Module R P]
  (f : M →ₚₗ[R] N) (g : N →ₚₗ[R] P) (S : Type u) [inst_7 : CommSemiring S] [inst_8 : Algebra R S],
  (g.comp f).toFun' S = g.toFun' S ∘ f.toFun' S
-- Mathlib.Algebra.Algebra.Spectrum.Basic
/-- **Alias** of the reverse direction of `spectrum.zero_mem_iff`. -/
spectrum.zero_mem : ∀ (R : Type u) {A : Type v} [inst : CommSemiring R] [inst_1 : Ring A] [inst_2 : Algebra R A] {a : A},
  ¬IsUnit a → 0 ∈ spectrum R a
-- Std.Sync.Broadcast
_private.Std.Sync.Broadcast.0.Std.Bounded.trySend : {α : Type} → Std.Bounded✝ α → α → BaseIO (Option ℕ)
-- Mathlib.Geometry.Manifold.Submersion
Manifold.IsSubmersionAtOfComplement.mem_codChart_source : ∀ {𝕜 : Type u_1} {E'' : Type u_3} {F : Type u_5} {H : Type u_7} {G : Type u_9} {E : Type u}
  [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  [inst_3 : NormedAddCommGroup E''] [inst_4 : NormedSpace 𝕜 E''] [inst_5 : NormedAddCommGroup F]
  [inst_6 : NormedSpace 𝕜 F] [inst_7 : TopologicalSpace H] [inst_8 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} {N : Type u_13} [inst_9 : TopologicalSpace M]
  [inst_10 : ChartedSpace H M] [inst_11 : TopologicalSpace N] [inst_12 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N}
  {x : M} (h : Manifold.IsSubmersionAtOfComplement F I J n f x), f x ∈ h.codChart.source
-- Init.Data.List.Count
List.count_concat_self : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a : α} {l : List α}, List.count a (l.concat a) = List.count a l + 1
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Under.post_comp : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {X : T} {E : Type u_1} [inst_2 : CategoryTheory.Category.{v_1, u_1} E] (F : CategoryTheory.Functor T D)
  (G : CategoryTheory.Functor D E),
  CategoryTheory.Under.post (F.comp G) = (CategoryTheory.Under.post F).comp (CategoryTheory.Under.post G)
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.coeff_smul : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (f : MvPowerSeries σ R) (n : σ →₀ ℕ) (a : R),
  (MvPowerSeries.coeff n) (a • f) = a * (MvPowerSeries.coeff n) f
-- Mathlib.Algebra.Lie.Free
FreeLieAlgebra.universalEnvelopingEquivFreeAlgebra_symm_apply : ∀ (R : Type u) (X : Type v) [inst : CommRing R] (a : FreeAlgebra R X),
  (FreeLieAlgebra.universalEnvelopingEquivFreeAlgebra R X).symm a =
    ((FreeAlgebra.lift R) (⇑(UniversalEnvelopingAlgebra.ι R) ∘ FreeLieAlgebra.of R)) a
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.iSup_eq_zero_iff : ∀ {ι : Type u_3} {f : ι → Ordinal.{u}} [Small.{u, u_3} ι], iSup f = 0 ↔ ∀ (i : ι), f i = 0
-- Mathlib.Geometry.RingedSpace.SheafedSpace
AlgebraicGeometry.SheafedSpace.id_hom_base : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : AlgebraicGeometry.SheafedSpace C),
  (CategoryTheory.CategoryStruct.id X).hom.base = CategoryTheory.CategoryStruct.id ↑X.toPresheafedSpace
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Expr.denoteSAsRing.eq_9 : ∀ {α : Type u_1} [inst : Lean.Grind.Semiring α] (ctx : Lean.Grind.CommRing.Context α) (k : ℤ),
  Lean.Grind.CommRing.Expr.denoteSAsRing ctx (Lean.Grind.CommRing.Expr.intCast k) = 0
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.coe_two_pi : ↑(2 * Real.pi) = 0
-- Mathlib.Data.PFunctor.Univariate.Basic
PFunctor.fst_map : ∀ {P : PFunctor.{uA, uB}} {α : Type v₁} {β : Type v₂} (x : ↑P α) (f : α → β), (P.map f x).fst = x.fst
-- Mathlib.RingTheory.Filtration
Ideal.Filtration.submodule_span_single : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {I : Ideal R}
  (F : I.Filtration M), Submodule.span (↥(reesAlgebra I)) (⋃ i, PolynomialModule.single R i '' ↑(F.N i)) = F.submodule
-- Mathlib.Combinatorics.Young.YoungDiagram
YoungDiagram.rowLens_sorted : ∀ (μ : YoungDiagram), μ.rowLens.SortedGE
-- Batteries.Recycling.RBTree.WF
RBTree.RBNode.Ordered.setBlack : ∀ {α : Type u_1} {cmp : α → α → Ordering} {t : RBTree.RBNode α},
  RBTree.RBNode.Ordered cmp t.setBlack ↔ RBTree.RBNode.Ordered cmp t
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.orderTop_le_of_coeff_ne_zero : ∀ {R : Type u_3} [inst : Zero R] {Γ : Type u_5} [inst_1 : LinearOrder Γ] {x : HahnSeries Γ R} {g : Γ},
  x.coeff g ≠ 0 → x.orderTop ≤ ↑g
-- Mathlib.RingTheory.OrderOfVanishing.Basic
Ring.ordFrac.congr_simp : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsNoetherianRing R] [inst_2 : Ring.KrullDimLE 1 R] {K : Type u_3}
  [inst_3 : Field K] [inst_4 : Algebra R K] [inst_5 : IsFractionRing R K] [inst_6 : Nontrivial R],
  Ring.ordFrac R = Ring.ordFrac R
-- Mathlib.AlgebraicTopology.CechNerve
CategoryTheory.SimplicialObject.equivalenceRightToLeft_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 :
    ∀ (n : ℕ) (f : CategoryTheory.Arrow C),
      CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom]
  (X : CategoryTheory.SimplicialObject.Augmented C) (F : CategoryTheory.Arrow C) (G : X ⟶ F.augmentedCechNerve),
  (CategoryTheory.SimplicialObject.equivalenceRightToLeft X F G).left =
    CategoryTheory.CategoryStruct.comp (G.left.app (Opposite.op { len := 0 }))
      (CategoryTheory.Limits.WidePullback.π (fun x => F.hom) 0)
-- Mathlib.Algebra.Order.Interval.Basic
Interval.zero_ne_bot : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : Zero α], 0 ≠ ⊥
-- Mathlib.Order.Bounds.Image
/-- A monotone map sends a greatest element of a set to a greatest element of its
image.  -/
MonotoneOn.map_isGreatest : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {t : Set α} {a : α},
  MonotoneOn f t → IsGreatest t a → IsGreatest (f '' t) (f a)
-- Mathlib.Algebra.Homology.ShortComplex.Homology
/-- A homology map data for a morphism of short complexes in the opposite category
induces a homology map data in the original category.  -/
CategoryTheory.ShortComplex.HomologyMapData.unop : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S₁ S₂ : CategoryTheory.ShortComplex Cᵒᵖ} →
        {φ : S₁ ⟶ S₂} →
          {h₁ : S₁.HomologyData} →
            {h₂ : S₂.HomologyData} →
              CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂ →
                CategoryTheory.ShortComplex.HomologyMapData (CategoryTheory.ShortComplex.unopMap φ) h₂.unop h₁.unop
-- LeanSearchClient.LoogleSyntax
LeanSearchClient.instReprLoogleResult : Repr LeanSearchClient.LoogleResult
-- Mathlib.Algebra.Order.Module.Defs
smulPosMono_iff_smulPosStrictMono : ∀ {α : Type u_1} {β : Type u_2} [inst : Ring α] [inst_1 : AddCommGroup β] [inst_2 : Module α β]
  [inst_3 : PartialOrder α] [inst_4 : PartialOrder β] [IsDomain α] [Module.IsTorsionFree α β],
  SMulPosMono α β ↔ SMulPosStrictMono α β
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof.core0.injEq : ∀ (a zero a_1 zero_1 : Lean.Expr),
  (Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof.core0 a zero =
      Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof.core0 a_1 zero_1) =
    (a = a_1 ∧ zero = zero_1)
-- Mathlib.Topology.VectorBundle.Basic
Bundle.Pretrivialization.coe_linearMapAt : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : Semiring R] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace B] [inst_3 : AddCommMonoid F] [inst_4 : Module R F]
  [inst_5 : (x : B) → AddCommMonoid (E x)] [inst_6 : (x : B) → Module R (E x)]
  (e : Bundle.Pretrivialization F Bundle.TotalSpace.proj) [inst_7 : Bundle.Pretrivialization.IsLinear R e] (b : B),
  ⇑(Bundle.Pretrivialization.linearMapAt R e b) = fun y => if b ∈ e.baseSet then (↑e ⟨b, y⟩).2 else 0
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.hom_inv_whiskerRight_assoc : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f g : a ⟶ b} (η : f ≅ g) (h : b ⟶ c) {Z : a ⟶ c}
  (h_1 : CategoryTheory.CategoryStruct.comp f h ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight η.hom h)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight η.inv h) h_1) =
    h_1
-- Lean.Elab.BuiltinTerm
Lean.Elab.Term.elabWithDeclName : Lean.Elab.Term.TermElab
-- Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
OnePoint.smul_infty_eq_self_iff : ∀ {K : Type u_1} [inst : Field K] [inst_1 : DecidableEq K] {g : GL (Fin 2) K},
  g • OnePoint.infty = OnePoint.infty ↔ ↑g 1 0 = 0
-- Mathlib.Algebra.MonoidAlgebra.Module
AddMonoidAlgebra.coeff_mapDomainLinearMap : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : Module R S] (f : M → N) (x : AddMonoidAlgebra S M),
  ((AddMonoidAlgebra.mapDomainLinearMap R S f) x).coeff = Finsupp.mapDomain f x.coeff
-- Mathlib.Order.ModularLattice
IsModularLattice.to_isUpperModularLattice : ∀ {α : Type u_1} [inst : Lattice α] [IsModularLattice α], IsUpperModularLattice α
-- Mathlib.GroupTheory.FiniteAbelian.Duality
/-- **Alias** of `MonoidHom.domRestrict_surjective`.

---

Let `G` be a finite commutative group and let `H` be a subgroup. If `M` is a commutative monoid
such that `G →* Mˣ` and `H →* Mˣ` are both finite (this is the case for example if `M` is a
commutative domain) and with enough `n`th roots of unity, where `n` is the exponent
of `G`, then any homomorphism `H →* Mˣ` can be extended to an homomorphism `G →* Mˣ`.
 -/
MonoidHom.restrict_surjective : ∀ {G : Type u_1} (M : Type u_2) [inst : CommGroup G] [Finite G] [inst_2 : CommMonoid M]
  [hM : HasEnoughRootsOfUnity M (Monoid.exponent G)] (H : Subgroup G),
  Function.Surjective ⇑(MonoidHom.domRestrictHom H Mˣ)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.maxEntryD_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  {fallback : (a : α) × β a}, t₁.Equiv t₂ → t₁.maxEntryD fallback = t₂.maxEntryD fallback