mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Category.GrpWithZero
GrpWithZero.coe_id : ∀ {X : GrpWithZero}, ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) = id
-- Mathlib.RingTheory.HopfAlgebra.Convolution
/-- **Alias** of `HopfAlgebra.antipode_mul_antidistrib`. -/
HopfAlgebra.antipode_mul : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : HopfAlgebra R A] (a b : A),
  (HopfAlgebraStruct.antipode R) (a * b) = (HopfAlgebraStruct.antipode R) b * (HopfAlgebraStruct.antipode R) a
-- Mathlib.Order.UpperLower.Prod
LowerSet.prod_mono_right : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {s : LowerSet α} {t₁ t₂ : LowerSet β},
  t₁ ≤ t₂ → s ×ˢ t₁ ≤ s ×ˢ t₂
-- Init.Prelude
instHAdd : {α : Type u_1} → [Add α] → HAdd α α α
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.deleteVerts_empty : ∀ {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph}, G'.deleteVerts ∅ = G'
-- Init.Data.UInt.Lemmas
USize.toNat_inj : ∀ {a b : USize}, a.toNat = b.toNat ↔ a = b
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Exact.rightHomologyDataOfIsColimitCokernelCofork_ι : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S : CategoryTheory.ShortComplex C} (hS : S.Exact) [inst_2 : CategoryTheory.Limits.HasZeroObject C]
  (cc : CategoryTheory.Limits.CokernelCofork S.f) (hcc : CategoryTheory.Limits.IsColimit cc),
  (hS.rightHomologyDataOfIsColimitCokernelCofork cc hcc).ι = 0
-- ProofWidgets.Data.Html
ProofWidgets.Html.component.inj : ∀ {a : UInt64} {a_1 : String} {a_2 : ProofWidgets.LazyEncodable Lean.Json} {a_3 : Array ProofWidgets.Html}
  {a_4 : UInt64} {a_5 : String} {a_6 : ProofWidgets.LazyEncodable Lean.Json} {a_7 : Array ProofWidgets.Html},
  ProofWidgets.Html.component a a_1 a_2 a_3 = ProofWidgets.Html.component a_4 a_5 a_6 a_7 →
    a = a_4 ∧ a_1 = a_5 ∧ a_2 = a_6 ∧ a_3 = a_7
-- Aesop.RulePattern.Cache
Aesop.instEmptyCollectionRulePatternCache : EmptyCollection Aesop.RulePatternCache
-- Mathlib.Geometry.Convex.Cone.Basic
Convex.toCone_eq_sInf : ∀ {𝕜 : Type u_1} {M : Type u_4} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup M] [inst_4 : Module 𝕜 M] {s : Set M} (hs : Convex 𝕜 s), Convex.toCone s hs = sInf {t | s ⊆ ↑t}
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Finset.op_prod : ∀ {ι : Type u_1} {M : Type u_3} [inst : CommMonoid M] (s : Finset ι) (f : ι → M),
  AddOpposite.op (∏ i ∈ s, f i) = ∏ i ∈ s, AddOpposite.op (f i)
-- Mathlib.Dynamics.SymbolicDynamics.Basic
SymbolicDynamics.FullShift.Subshift.mk.injEq : ∀ {A : Type u_1} [inst : TopologicalSpace A] {G : Type u_2} [inst_1 : AddMonoid G] (carrier : Set (G → A))
  (isClosed : IsClosed carrier) (mapsTo : ∀ (g : G), Set.MapsTo (SymbolicDynamics.FullShift.shift g) carrier carrier)
  (carrier_1 : Set (G → A)) (isClosed_1 : IsClosed carrier_1)
  (mapsTo_1 : ∀ (g : G), Set.MapsTo (SymbolicDynamics.FullShift.shift g) carrier_1 carrier_1),
  ({ carrier := carrier, isClosed := isClosed, mapsTo := mapsTo } =
      { carrier := carrier_1, isClosed := isClosed_1, mapsTo := mapsTo_1 }) =
    (carrier = carrier_1)
-- Mathlib.Combinatorics.Hindman
/-- The weak form of **Hindman's theorem**: in any finite cover of a nonempty semigroup, one of the
parts contains an FP-set.  -/
Hindman.exists_FP_of_finite_cover : ∀ {M : Type u_1} [inst : Semigroup M] [Nonempty M] (s : Set (Set M)),
  s.Finite → ⊤ ⊆ ⋃₀ s → ∃ c ∈ s, ∃ a, Hindman.FP a ⊆ c
-- Init.Data.Int.Gcd
/-- Computes the least common multiple of two integers as a natural number. The LCM of two integers is
the smallest natural number that's evenly divisible by the absolute values of both.

Examples:
 * `Int.lcm 9 6 = 18`
 * `Int.lcm 9 (-6) = 18`
 * `Int.lcm 9 3 = 9`
 * `Int.lcm 9 (-3) = 9`
 * `Int.lcm 0 3 = 0`
 * `Int.lcm (-3) 0 = 0`
 -/
Int.lcm : ℤ → ℤ → ℕ
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.toENat_comp_ofENat : ⇑Cardinal.toENat ∘ Cardinal.ofENat = id
-- Mathlib.Data.Seq.Computation
Computation.get_thinkN : ∀ {α : Type u} (s : Computation α) [h : s.Terminates] (n : ℕ), (s.thinkN n).get = s.get
-- Mathlib.Algebra.Homology.Embedding.Connect
/-- the differential which connect `K` and `L`  -/
CochainComplex.ConnectData.d₀ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {K : ChainComplex C ℕ} → {L : CochainComplex C ℕ} → CochainComplex.ConnectData K L → (K.X 0 ⟶ L.X 0)
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Spec.map_comp : ∀ {R S T : CommRingCat} (f : R ⟶ S) (g : S ⟶ T),
  AlgebraicGeometry.Spec.map (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map g) (AlgebraicGeometry.Spec.map f)
-- Mathlib.Algebra.CharP.Frobenius
iterateFrobenius.congr_simp : ∀ (R : Type u_3) [inst : CommSemiring R] (p p_1 : ℕ) (e_p : p = p_1) (n n_1 : ℕ),
  n = n_1 → ∀ [inst_1 : ExpChar R p], iterateFrobenius R p n = iterateFrobenius R p_1 n_1
-- Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
UniformConvergenceCLM.instDistribMulAction : {𝕜₁ : Type u_1} →
  {𝕜₂ : Type u_2} →
    [inst : NormedField 𝕜₁] →
      [inst_1 : NormedField 𝕜₂] →
        (σ : 𝕜₁ →+* 𝕜₂) →
          {E : Type u_3} →
            (F : Type u_4) →
              [inst_2 : AddCommGroup E] →
                [inst_3 : Module 𝕜₁ E] →
                  [inst_4 : TopologicalSpace E] →
                    [inst_5 : AddCommGroup F] →
                      [inst_6 : Module 𝕜₂ F] →
                        (M : Type u_6) →
                          [inst_7 : Monoid M] →
                            [inst_8 : DistribMulAction M F] →
                              [SMulCommClass 𝕜₂ M F] →
                                [inst_10 : TopologicalSpace F] →
                                  [inst_11 : IsTopologicalAddGroup F] →
                                    [ContinuousConstSMul M F] →
                                      (𝔖 : Set (Set E)) → DistribMulAction M (UniformConvergenceCLM σ F 𝔖)
-- Mathlib.Probability.Kernel.RadonNikodym
ProbabilityTheory.Kernel.withDensity_one_sub_rnDerivAux : ∀ {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ}
  [hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ] (κ η : ProbabilityTheory.Kernel α γ)
  [inst : ProbabilityTheory.IsFiniteKernel κ] [inst_1 : ProbabilityTheory.IsFiniteKernel η],
  ((κ + η).withDensity fun a x => ↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal) = η
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr
Std.Tactic.BVDecide.BVExpr.Cache.insert.eq_1 : ∀ {aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit} {w : ℕ} (expr : Std.Tactic.BVDecide.BVExpr w) (refs : aig.RefVec w)
  (map : Std.DHashMap Std.Tactic.BVDecide.BVExpr.Cache.Key fun k => Vector Std.Sat.AIG.Fanin k.w)
  (hbound :
    ∀ {i : ℕ} (k : Std.Tactic.BVDecide.BVExpr.Cache.Key) (h1 : k ∈ map) (h2 : i < k.w),
      (map.get k h1)[i].gate < aig.decls.size),
  { map := map, hbound := hbound }.insert expr refs =
    { map := map.insert { w := w, expr := expr } refs.refs, hbound := ⋯ }
-- Mathlib.Order.Filter.ENNReal
Filter.IsCoboundedUnder.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (f : Filter β) (u : β → α),
  Filter.IsCoboundedUnder r f u = Filter.IsCobounded r (Filter.map u f)
-- Mathlib.LinearAlgebra.BilinearForm.IsometryEquiv
/-- An isometric equivalence between two bilinear spaces `M₁, B₁` and `M₂, B₂` over a ring `R`,
is a linear equivalence between `M₁` and `M₂` that commutes with the bilinear forms.  -/
LinearMap.BilinForm.IsometryEquiv : {R : Type u_1} →
  {M₁ : Type u_3} →
    {M₂ : Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M₁] →
          [inst_2 : AddCommMonoid M₂] →
            [inst_3 : Module R M₁] →
              [inst_4 : Module R M₂] → LinearMap.BilinForm R M₁ → LinearMap.BilinForm R M₂ → Type (max u_3 u_4)
-- Std.Sat.AIG.CachedGatesLemmas
Std.Sat.AIG.mkNotCached_le_size : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] (aig : Std.Sat.AIG α) (gate : aig.Ref),
  aig.decls.size ≤ (aig.mkNotCached gate).aig.decls.size
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
CategoryTheory.Limits.ChosenPullback.isPullback : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S}
  (h : CategoryTheory.Limits.ChosenPullback f₁ f₂), CategoryTheory.IsPullback h.p₁ h.p₂ f₁ f₂
-- Mathlib.Analysis.Calculus.Deriv.Basic
/-- `f` has the derivative `f'` along the filter `L`.

That is, `f x' = f x + (x' - x) • f' + o(x' - x)` where `(x', x)` converges along the filter `L`.
 -/
HasDerivAtFilter : {𝕜 : Type u} →
  [inst : NontriviallyNormedField 𝕜] →
    {F : Type v} →
      [inst_1 : AddCommGroup F] →
        [inst_2 : Module 𝕜 F] →
          [inst_3 : TopologicalSpace F] → [ContinuousSMul 𝕜 F] → (𝕜 → F) → F → Filter (𝕜 × 𝕜) → Prop
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
/-- Homotopy between morphisms of short complexes is compatible with composition.  -/
CategoryTheory.ShortComplex.Homotopy.comp : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {S₁ S₂ S₃ : CategoryTheory.ShortComplex C} →
        {φ₁ φ₂ : S₁ ⟶ S₂} →
          CategoryTheory.ShortComplex.Homotopy φ₁ φ₂ →
            {ψ₁ ψ₂ : S₂ ⟶ S₃} →
              CategoryTheory.ShortComplex.Homotopy ψ₁ ψ₂ →
                CategoryTheory.ShortComplex.Homotopy (CategoryTheory.CategoryStruct.comp φ₁ ψ₁)
                  (CategoryTheory.CategoryStruct.comp φ₂ ψ₂)
-- Mathlib.Data.List.Infix
List.infix_insert : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (l : List α), l <:+: List.insert a l
-- Mathlib.LinearAlgebra.Basis.Flag
Module.Basis.flag.eq_1 : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {n : ℕ}
  (b : Module.Basis (Fin n) R M) (k : Fin (n + 1)), b.flag k = Submodule.span R (⇑b '' {i | i.castSucc < k})
-- Lean.Meta.Sym.Pattern
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.UnifyM.Context.mk : Lean.Meta.Sym.Pattern → Bool → Bool → Lean.Meta.Sym.UnifyM.Context✝
-- Mathlib.Data.Stream.Defs
/-- Interleave two streams.  -/
Stream'.interleave : {α : Type u} → Stream' α → Stream' α → Stream' α
-- Init.Data.Nat.Internal.SOM
Nat.Internal.SOM.Mon.mul_denote : ∀ (ctx : Nat.Internal.Linear.Context) (m₁ m₂ : Nat.Internal.SOM.Mon),
  Nat.Internal.SOM.Mon.denote ctx (m₁.mul m₂) = Nat.Internal.SOM.Mon.denote ctx m₁ * Nat.Internal.SOM.Mon.denote ctx m₂
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
/-- The cosine of an angle in a right-angled triangle multiplied by the hypotenuse equals the
adjacent side, version subtracting vectors.  -/
InnerProductGeometry.cos_angle_sub_mul_norm_of_inner_eq_zero : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
  inner ℝ x y = 0 → Real.cos (InnerProductGeometry.angle x (x - y)) * ‖x - y‖ = ‖x‖
-- Mathlib.Algebra.Category.ModuleCat.Ulift
ModuleCat.instPreservesFiniteLimitsUliftFunctor : ∀ (R : Type u) [inst : Ring R], CategoryTheory.Limits.PreservesFiniteLimits (ModuleCat.uliftFunctor.{v', v, u} R)
-- Mathlib.Dynamics.Flow
Flow.IsSemiconjugacy.isFactorOf : ∀ {τ : Type u_1} {α : Type u_2} [inst : TopologicalSpace τ] [inst_1 : TopologicalSpace α] [inst_2 : AddMonoid τ]
  (ϕ : Flow τ α) {β : Type u_3} [inst_3 : TopologicalSpace β] (ψ : Flow τ β) {π : α → β},
  Flow.IsSemiconjugacy π ϕ ψ → ψ.IsFactorOf ϕ
-- Aesop.Tree.Data
Aesop.RappId.dummy : Aesop.RappId
-- Lean.Language.Basic
/-- Transforms a task's output without changing the processed syntax.  -/
Lean.Language.SnapshotTask.map : {α β : Type} →
  (t : Lean.Language.SnapshotTask α) →
    (α → β) →
      optParam (Option Lean.Syntax) t.stx? →
        optParam Lean.Language.SnapshotTask.ReportingRange t.reportingRange →
          optParam Bool false → Lean.Language.SnapshotTask β
-- Mathlib.Analysis.Distribution.TemperedDistribution
/-- **Alias** of `TemperedDistribution.fourier_toTemperedDistributionCLM_eq`.

---

The distributional Fourier transform and the classical Fourier transform coincide on
`𝓢(E, F)`.  -/
TemperedDistribution.fourierTransform_toTemperedDistributionCLM_eq : ∀ {E : Type u_3} {F : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E]
  [inst_2 : FiniteDimensional ℝ E] [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] [inst_5 : NormedAddCommGroup F]
  [inst_6 : NormedSpace ℂ F] [CompleteSpace F] (f : SchwartzMap E F),
  FourierTransform.fourier ((SchwartzMap.toTemperedDistributionCLM E F MeasureTheory.volume) f) =
    (SchwartzMap.toTemperedDistributionCLM E F MeasureTheory.volume) (FourierTransform.fourier f)
-- Mathlib.Data.Matrix.Mul
Matrix.vecMul_intCast : ∀ {m : Type u_2} {α : Type v} [inst : NonAssocRing α] [inst_1 : Fintype m] [inst_2 : DecidableEq m] (x : ℤ) (v : m → α),
  Matrix.vecMul v ↑x = MulOpposite.op ↑x • v
-- Mathlib.Data.List.NodupEquivFin
List.SortedLT.coe_getIso_symm_apply : ∀ {α : Type u_1} [inst : Preorder α] {l : List α} [inst_1 : DecidableEq α] (H : l.SortedLT) {x : { x // x ∈ l }},
  ↑((List.SortedLT.getIso l H).symm x) = List.idxOf (↑x) l
-- Mathlib.Algebra.Group.Defs
add_zero : ∀ {M : Type u} [inst : AddZeroClass M] (a : M), a + 0 = a
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.Lift.aux.eq_1 : ∀ {α : Type u} {β : Type v} [inst : AddGroup β] (f : α → β) (L : List (α × Bool)),
  FreeAddGroup.Lift.aux f L = (List.map (fun x => bif x.2 then f x.1 else -f x.1) L).sum
-- Mathlib.Topology.Order.Hom.Esakia
PseudoEpimorphism.toFun_eq_coe : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {f : PseudoEpimorphism α β}, f.toFun = ⇑f
-- Mathlib.Algebra.Polynomial.Div
Polynomial.associated_of_dvd_of_degree_eq : ∀ {K : Type u_1} [inst : Field K] {p q : Polynomial K}, p ∣ q → p.degree = q.degree → Associated p q
-- Std.Http.Protocol.H1.Config
/-- Maximum length of header field value (default: 8192 bytes).
 -/
Std.Http.Protocol.H1.Config.maxHeaderValueLength : Std.Http.Protocol.H1.Config → ℕ
-- Init.Data.List.Lemmas
List.getLast!.eq_2 : ∀ {α : Type u_1} [inst : Inhabited α] (a : α) (as : List α), (a :: as).getLast! = (a :: as).getLast ⋯
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- Naturality of the `prodComparison` morphism in both arguments.  -/
CategoryTheory.Limits.prodComparison_natural : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{w, u₂} D]
  (F : CategoryTheory.Functor C D) {A A' B B' : C} [inst_2 : CategoryTheory.Limits.HasBinaryProduct A B]
  [inst_3 : CategoryTheory.Limits.HasBinaryProduct A' B']
  [inst_4 : CategoryTheory.Limits.HasBinaryProduct (F.obj A) (F.obj B)]
  [inst_5 : CategoryTheory.Limits.HasBinaryProduct (F.obj A') (F.obj B')] (f : A ⟶ A') (g : B ⟶ B'),
  CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Limits.prod.map f g))
      (CategoryTheory.Limits.prodComparison F A' B') =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prodComparison F A B)
      (CategoryTheory.Limits.prod.map (F.map f) (F.map g))
-- Std.Tactic.BVDecide.Normalize.Bool
Std.Tactic.BVDecide.Normalize.BitVec.beq_zero_eq_ite : ∀ {b : Bool} {a : BitVec 1}, ((a == 0#1) == b) = (a == bif b then 0#1 else 1#1)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getKeyD_insertManyIfNewUnit_list_of_not_mem_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtDHashMap α fun x => Unit} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List α} {k k' fallback : α},
  (k == k') = true →
    k ∉ m →
      List.Pairwise (fun a b => (a == b) = false) l →
        k ∈ l → (Std.ExtDHashMap.Const.insertManyIfNewUnit m l).getKeyD k' fallback = k
-- Mathlib.Algebra.Algebra.Unitization
Unitization.mk_surjective : ∀ {R : Type u_1} {A : Type u_2}, Function.Surjective Unitization.mk
-- Lean.Server.Completion.CompletionCollectors
/-- All completion items and their fuzzy match scores so far.  -/
_private.Lean.Server.Completion.CompletionCollectors.0.Lean.Server.Completion.State.items : Lean.Server.Completion.State✝ → Array Lean.Lsp.ResolvableCompletionItem
-- Mathlib.Algebra.Polynomial.Coeff
Polynomial.coeff_mul_X_pow' : ∀ {R : Type u} [inst : Semiring R] (p : Polynomial R) (n d : ℕ),
  (p * Polynomial.X ^ n).coeff d = if n ≤ d then p.coeff (d - n) else 0
-- Lean.Data.JsonRpc
Lean.JsonRpc.RequestID.lt : Lean.JsonRpc.RequestID → Lean.JsonRpc.RequestID → Bool
-- Mathlib.Data.Finset.MulAntidiagonal
Set.IsPWO.add : ∀ {α : Type u_1} {s t : Set α} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [IsOrderedCancelAddMonoid α],
  s.IsPWO → t.IsPWO → (s + t).IsPWO
-- Mathlib.Combinatorics.SimpleGraph.Cayley
SimpleGraph.instDecidableRelAdjMulCayleyOfDecidableEqOfDecidablePredMemSet : {M : Type u_1} →
  (s : Set M) →
    [inst : Group M] → [DecidableEq M] → [DecidablePred fun x => x ∈ s] → DecidableRel (SimpleGraph.mulCayley s).Adj
-- Mathlib.Topology.Defs.Induced
Topology.isClosedEmbedding_iff : ∀ {X : Type u_1} {Y : Type u_2} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] (f : X → Y),
  Topology.IsClosedEmbedding f ↔ Topology.IsEmbedding f ∧ IsClosed (Set.range f)
-- Mathlib.Algebra.Homology.Embedding.Basic
ComplexShape.embeddingUpIntGE_f : ∀ (p : ℤ) (n : ℕ), (ComplexShape.embeddingUpIntGE p).f n = p + ↑n
-- Mathlib.GroupTheory.OrderOfElement
IsOfFinAddOrder.multiples_eq_zmultiples : ∀ {G : Type u_1} [inst : AddGroup G] {x : G},
  IsOfFinAddOrder x → ↑(AddSubmonoid.multiples x) = ↑(AddSubgroup.zmultiples x)
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
/-- The inflation map `H¹(G ⧸ S, A^S) ⟶ H¹(G, A)` is a monomorphism.  -/
groupCohomology.instMonoModuleCatFH1InfRes : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) (S : Subgroup G) [inst_2 : S.Normal],
  CategoryTheory.Mono (groupCohomology.H1InfRes A S).f
-- Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne
SimplexCategory.σ_comp_toMk₁_of_le : ∀ {n : ℕ} (i : Fin (n + 2)) (j : Fin (n + 1)),
  i ≤ j.castSucc →
    CategoryTheory.CategoryStruct.comp (SimplexCategory.σ j) (SimplexCategory.toMk₁ i) =
      SimplexCategory.toMk₁ i.castSucc
-- Mathlib.MeasureTheory.Group.Arithmetic
AddOpposite.instMeasurableSpace.eq_1 : ∀ {α : Type u_2} [h : MeasurableSpace α], AddOpposite.instMeasurableSpace = MeasurableSpace.map AddOpposite.op h
-- Mathlib.Analysis.AbsoluteValue.Equivalence
/-- If `v : ι → AbsoluteValue R S` is a finite collection of non-trivial and pairwise inequivalent
absolute values, then for any `i` there is some `a : R` such that `1 < v i a` and
`v j a < 1` for all `j ≠ i`.
 -/
AbsoluteValue.exists_one_lt_lt_one_pi_of_not_isEquiv : ∀ {R : Type u_1} {S : Type u_2} [inst : Field R] [inst_1 : Field S] [inst_2 : LinearOrder S]
  [inst_3 : TopologicalSpace S] [IsStrictOrderedRing S] [Archimedean S] [OrderTopology S] {ι : Type u_3} [Finite ι]
  {v : ι → AbsoluteValue R S},
  (∀ (i : ι), (v i).IsNontrivial) →
    (Pairwise fun i j => ¬(v i).IsEquiv (v j)) → ∀ (i : ι), ∃ a, 1 < (v i) a ∧ ∀ (j : ι), j ≠ i → (v j) a < 1
-- Mathlib.Probability.Distributions.Uniform
PMF.uniformOfFinset_apply : ∀ {α : Type u_1} {s : Finset α} (hs : s.Nonempty) (a : α),
  (PMF.uniformOfFinset s hs) a = if a ∈ s then (↑s.card)⁻¹ else 0
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanClass.mk_sub_eq_mk_right : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] {a b : M},
  ArchimedeanClass.mk b < ArchimedeanClass.mk a → ArchimedeanClass.mk (a - b) = ArchimedeanClass.mk b
-- Mathlib.AlgebraicGeometry.Group.Affine
AlgebraicGeometry.preservesLimitsOfSize_algSpec : ∀ {R : CommRingCat},
  CategoryTheory.Limits.PreservesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (AlgebraicGeometry.algSpec R)
-- Mathlib.Algebra.Group.Ideal
/-- A (left) semigroup ideal in a semigroup `M` is a set `s` such that `a * b ∈ s` whenever
`b ∈ s`.  -/
SemigroupIdeal : (M : Type u_1) → [Mul M] → Type u_1
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.Subcomplex.coe_mk'' : ∀ {X : Type u_1} [t : TopologicalSpace X] [inst : T2Space X] (C : Set X) {D : Set X}
  [inst_1 : Topology.RelCWComplex C D] (E : Set X) (I : (n : ℕ) → Set (Topology.RelCWComplex.cell C n))
  [inst_2 : Topology.RelCWComplex E D] (union : D ∪ ⋃ n, ⋃ j, Topology.RelCWComplex.openCell n ↑j = E),
  ↑(Topology.RelCWComplex.Subcomplex.mk'' C E I union) = E
-- Mathlib.Data.Num.Lemmas
PosNum.size.eq_3 : ∀ (n : PosNum), n.bit1.size = n.size.succ
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Stepwise.unsat_eq : ∀ {α : Type u_1} [inst : Lean.Grind.CommRing α] (ctx : Lean.Grind.CommRing.Context α) [Lean.Grind.IsCharP α 0]
  (p : Lean.Grind.CommRing.Poly) (k : ℤ),
  Lean.Grind.CommRing.Stepwise.unsat_eq_cert p k = true → Lean.Grind.CommRing.Poly.denote ctx p = 0 → False
-- Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
/-- If `s` is a von Neumann bounded set and `U` is a neighbourhood of zero,
then sufficiently small continuous linear maps map `s` to `U`.  -/
ContinuousLinearMap.eventually_nhds_zero_mapsTo : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_4}
  {F : Type u_5} [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜₁ E] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜₂ F]
  [inst_6 : TopologicalSpace E] [inst_7 : TopologicalSpace F] [inst_8 : IsTopologicalAddGroup F] {s : Set E},
  Bornology.IsVonNBounded 𝕜₁ s → ∀ {U : Set F}, U ∈ nhds 0 → ∀ᶠ (f : E →SL[σ] F) in nhds 0, Set.MapsTo (⇑f) s U
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.zpow_lt_iff_lt_log : ∀ {x y : ℝ} {n : ℤ}, 0 < x → 0 < y → (x ^ n < y ↔ ↑n * Real.log x < Real.log y)
-- Mathlib.Data.Ordmap.Invariants
Ordnode.Sized.eq_node' : ∀ {α : Type u_1} {s : ℕ} {l : Ordnode α} {x : α} {r : Ordnode α},
  (Ordnode.node s l x r).Sized → Ordnode.node s l x r = l.node' x r
-- Lean.Widget.Diff
_private.Lean.Widget.Diff.0.Lean.Widget.ExprDiffTag.change.sizeOf_spec : sizeOf Lean.Widget.ExprDiffTag.change✝ = 1
-- Mathlib.Algebra.Group.Action.Defs
SMulCommClass.of_mul_smul_one : ∀ {M : Type u_9} {N : Type u_10} [inst : Monoid N] [inst_1 : SMul M N],
  (∀ (x : M) (y : N), y * x • 1 = x • y) → SMulCommClass M N N
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidIso.eq_symm_comp : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Add α] [inst_3 : Add β]
  (e : α ≃+o β) (f : α → α) (g : α → β), f = ⇑e.symm ∘ g ↔ ⇑e ∘ f = g
-- Mathlib.Geometry.Manifold.MFDeriv.FDeriv
/-- For maps between vector spaces, `mfderivWithin` and `fderivWithin` coincide  -/
mfderivWithin_eq_fderivWithin : ∀ {𝕜 : 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'}
  {s : Set E} {x : E}, mfderiv[s] f x = fderivWithin 𝕜 f s x
-- Mathlib.Analysis.Calculus.DerivativeTest
/-- The First Derivative test with a hypothesis on the sign of the derivative, maximum version.  -/
isLocalMax_of_sign_deriv : ∀ {f : ℝ → ℝ} {x₀ : ℝ},
  ContinuousAt f x₀ →
    (∀ᶠ (x : ℝ) in nhdsWithin x₀ {x₀}ᶜ, SignType.sign (deriv f x) = SignType.sign (x₀ - x)) → IsLocalMax f x₀
-- Mathlib.Data.Sigma.Order
Sigma.Lex.denselyOrdered_of_noMinOrder : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : Preorder ι] [inst_1 : (i : ι) → Preorder (α i)]
  [∀ (i : ι), DenselyOrdered (α i)] [∀ (i : ι), NoMinOrder (α i)], DenselyOrdered (Σₗ (i : ι), α i)
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNorm_exponent_zero : ∀ {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : ENorm ε] {f : α → ε},
  MeasureTheory.eLpNorm f 0 μ = 0