mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Lie.Derivation.Basic
LieDerivation.instSMul : {R : Type u_1} →
  {L : Type u_2} →
    {M : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : LieAlgebra R L] →
            [inst_3 : AddCommGroup M] →
              [inst_4 : Module R M] →
                [inst_5 : LieRingModule L M] →
                  [inst_6 : LieModule R L M] →
                    {S : Type u_4} →
                      [inst_7 : Monoid S] →
                        [inst_8 : DistribMulAction S M] →
                          [SMulCommClass R S M] →
                            [LieDerivation.SMulBracketCommClass S L M] → SMul S (LieDerivation R L M)
-- Mathlib.CategoryTheory.Limits.Comma
CategoryTheory.Comma.hasFiniteColimits : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T}
  {R : CategoryTheory.Functor B T} [CategoryTheory.Limits.HasFiniteColimits A]
  [CategoryTheory.Limits.HasFiniteColimits B] [CategoryTheory.Limits.PreservesFiniteColimits L],
  CategoryTheory.Limits.HasFiniteColimits (CategoryTheory.Comma L R)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getKeyD_insertManyIfNewUnit_emptyWithCapacity_list_of_contains_eq_false : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α] {l : List α} {k fallback : α},
  l.contains k = false →
    (↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit Std.DHashMap.Internal.Raw₀.emptyWithCapacity l)).getKeyD k
        fallback =
      fallback
-- Mathlib.Algebra.Homology.HomologySequence
HomologicalComplex.HomologySequence.snakeInput_v₀₁ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {c : ComplexShape ι} {S : CategoryTheory.ShortComplex (HomologicalComplex C c)} (hS : S.ShortExact) (i j : ι)
  (hij : c.Rel i j),
  (HomologicalComplex.HomologySequence.snakeInput hS i j hij).v₀₁ =
    S.mapNatTrans (HomologicalComplex.natTransHomologyι C c i)
-- Mathlib.Algebra.BigOperators.Finprod
finprod_eq_prod_of_mulSupport_subset_of_finite : ∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] (f : α → M) {s : Set α},
  Function.mulSupport f ⊆ s → ∀ (hs : s.Finite), ∏ᶠ (i : α), f i = ∏ i ∈ hs.toFinset, f i
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.instOrdDiagnosticSeverity : Ord Lean.Lsp.DiagnosticSeverity
-- Mathlib.Combinatorics.Additive.AP.Three.Behrend
Behrend.box_zero : ∀ {n : ℕ}, Behrend.box (n + 1) 0 = ∅
-- Mathlib.NumberTheory.NumberField.House
NumberField.house_pow_le : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (α : K) (i : ℕ),
  NumberField.house (α ^ i) ≤ NumberField.house α ^ i
-- Mathlib.Topology.Homotopy.HomotopyGroup
GenLoop.loopHomeo_symm_apply : ∀ {N : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {x : X} [inst_1 : DecidableEq N] (i : N)
  (p : LoopSpace (↑(GenLoop { j // j ≠ i } X x)) GenLoop.const), (GenLoop.loopHomeo i).symm p = GenLoop.fromLoop i p
-- Mathlib.Analysis.Normed.Group.Defs
SeminormedCommGroup.toSeminormedGroup.eq_1 : ∀ {E : Type u_5} [inst : SeminormedCommGroup E],
  SeminormedCommGroup.toSeminormedGroup =
    { toNorm := inst.toNorm, toGroup := inst.toGroup, toPseudoMetricSpace := inst.toPseudoMetricSpace, dist_eq := ⋯ }
-- Mathlib.Data.List.Defs
List.iterate_eq_iterateTR : @List.iterate = @List.iterateTR
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
_private.Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle.0.Real.Angle.abs_toReal_add_eq_two_pi_sub_abs_toReal_add_abs_toReal_aux : ∀ {θ ψ : Real.Angle},
  θ.sign = 1 → ψ.sign = 1 → (θ + ψ).sign ≠ 1 → |(θ + ψ).toReal| = 2 * Real.pi - (|θ.toReal| + |ψ.toReal|)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
WeierstrassCurve.instIsMinimalMinimal : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsDiscreteValuationRing R] {K : Type u_2}
  [inst_3 : Field K] [inst_4 : Algebra R K] [inst_5 : IsFractionRing R K] {W : WeierstrassCurve K},
  WeierstrassCurve.IsMinimal R (WeierstrassCurve.minimal R W)
-- Mathlib.Data.TypeVec
/-- given a predicate vector `p` over vector `α`, `Subtype_ p` is the type of vectors
that contain an `α` that satisfies `p`  -/
TypeVec.Subtype_ : {n : ℕ} → {α : TypeVec.{u} n} → α.Arrow (TypeVec.repeat n Prop) → TypeVec.{u} n
-- Mathlib.CategoryTheory.Monoidal.Action.Opposites
CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftActionOfMonoidalOppositeRightAction_actionHomLeft : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction Cᴹᵒᵖ D] {c c' : C} (f : c ⟶ c') (d : D),
  CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f d =
    CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight d f.mop
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.sub.eq_1 : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Sub α], Finset.sub = { sub := Finset.image₂ fun x1 x2 => x1 - x2 }
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Images
/-- The image of a natural transformation between type-valued functors is a `MonoFactorisation`  -/
CategoryTheory.FunctorToTypes.monoFactorisation : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {F G : CategoryTheory.Functor C (Type u)} → (f : F ⟶ G) → CategoryTheory.Limits.MonoFactorisation f
-- Mathlib.CategoryTheory.Preadditive.Basic
CategoryTheory.Preadditive.neg_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {P Q R : C} (f : P ⟶ Q)
  (g : Q ⟶ R), CategoryTheory.CategoryStruct.comp (-f) g = -CategoryTheory.CategoryStruct.comp f g
-- Mathlib.Algebra.CharP.Lemmas
list_sum_pow_char_pow : ∀ {R : Type u_3} [inst : CommSemiring R] (p n : ℕ) [ExpChar R p] (l : List R),
  l.sum ^ p ^ n = (List.map (fun x => x ^ p ^ n) l).sum
-- Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
ENNReal.exp_log : ∀ (x : ENNReal), x.log.exp = x
-- Mathlib.CategoryTheory.ObjectProperty.Retract
CategoryTheory.ObjectProperty.IsStableUnderRetracts.of_bicone : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) [P.IsStableUnderRetracts]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {J : Type u_1} (F : J → C) (c : CategoryTheory.Limits.Bicone F),
  P c.pt → ∀ (j : J), P (F j)
-- Mathlib.Algebra.EuclideanDomain.Basic
EuclideanDomain.zero_div : ∀ {R : Type u} [inst : EuclideanDomain R] {a : R}, 0 / a = 0
-- Mathlib.Order.UpperLower.Prod
LowerSet.top_prod_top : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β], ⊤ ×ˢ ⊤ = ⊤
-- Mathlib.Tactic.Basic
/-- Runs a tactic, returning any new messages and info trees rather than adding them to the state.
 -/
Mathlib.Tactic.withResetServerInfo : {α : Type} → Lean.Elab.Tactic.TacticM α → Lean.Elab.Tactic.TacticM (Mathlib.Tactic.withResetServerInfo.Result α)
-- Mathlib.Topology.Algebra.InfiniteSum.Constructions
HasSum.unop : ∀ {α : Type u_1} {β : Type u_2} {L : SummationFilter β} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α]
  {f : β → αᵐᵒᵖ} {a : αᵐᵒᵖ}, HasSum f a L → HasSum (fun a => MulOpposite.unop (f a)) (MulOpposite.unop a) L
-- Mathlib.Algebra.Group.Submonoid.Defs
SubmonoidClass.mk : ∀ {S : Type u_3} {M : outParam (Type u_4)} [inst : MulOneClass M] [inst_1 : SetLike S M]
  [toMulMemClass : MulMemClass S M] [toOneMemClass : OneMemClass S M], SubmonoidClass S M
-- Mathlib.Algebra.Order.GroupWithZero.Basic
one_le_div₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [MulPosReflectLT G₀] {a b : G₀},
  0 < b → (1 ≤ a / b ↔ b ≤ a)
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
contMDiffAt_iff_of_mem_maximalAtlas : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {e : OpenPartialHomeomorph M H}
  {e' : OpenPartialHomeomorph M' H'} {f : M → M'} {n : WithTop ℕ∞} {x : M},
  e ∈ IsManifold.maximalAtlas I n M →
    e' ∈ IsManifold.maximalAtlas I' n M' →
      x ∈ e.source →
        f x ∈ e'.source →
          (ContMDiffAt I I' n f x ↔
            ContinuousAt f x ∧
              ContDiffWithinAt 𝕜 n (↑(e'.extend I') ∘ f ∘ ↑(e.extend I).symm) (Set.range ↑I) (↑(e.extend I) x))
-- Mathlib.Analysis.Normed.Lp.WithLp
/-- `WithLp.equiv` as a linear equivalence.  -/
WithLp.linearEquiv : (p : ENNReal) →
  (K : Type u_1) →
    (V : Type u_4) → [inst : Semiring K] → [inst_1 : AddCommGroup V] → [inst_2 : Module K V] → WithLp p V ≃ₗ[K] V
-- Mathlib.RingTheory.AdicCompletion.Basic
/-- Lift a compatible family of linear maps `M →ₗ[R] N ⧸ (I ^ n • ⊤ : Submodule R N)` to
the `I`-adic completion of `M`.  -/
AdicCompletion.lift : {R : Type u_1} →
  [inst : CommRing R] →
    (I : Ideal R) →
      {M : Type u_4} →
        [inst_1 : AddCommGroup M] →
          [inst_2 : Module R M] →
            {N : Type u_5} →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R N] →
                  (f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ n • ⊤) →
                    (∀ {m n : ℕ} (hle : m ≤ n), AdicCompletion.transitionMap I N hle ∘ₗ f n = f m) →
                      M →ₗ[R] AdicCompletion I N
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.get!_diff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  [inst : Inhabited β], (t₁ \ t₂).get! k = if k ∈ t₂ then default else t₁.get! k
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get?_ofList_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {l : List α} {k k' : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l → k ∈ l → (Std.ExtTreeSet.ofList l cmp).get? k' = some k
-- Mathlib.MeasureTheory.Function.LpSeminorm.SMul
MeasureTheory.eLpNorm_nsmul : ∀ {α : Type u_1} {F : Type u_2} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup F] [NormedSpace ℝ F] (n : ℕ) (f : α → F),
  MeasureTheory.eLpNorm (n • f) p μ = ↑n * MeasureTheory.eLpNorm f p μ
-- Init.System.FilePath
/-- Appends two paths, taking absolute paths into account. This operation is also accessible via the `/`
operator.

If `sub` is an absolute path, then `p` is discarded and `sub` is returned. If `sub` is a relative
path, then it is attached to `p` with the platform-specific path separator.
 -/
System.FilePath.join : System.FilePath → System.FilePath → System.FilePath
-- Mathlib.Analysis.InnerProductSpace.Calculus
ContDiffWithinAt.norm : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
  [inst : NormedSpace ℝ E] {G : Type u_4} [inst_2 : NormedAddCommGroup G] [inst_3 : NormedSpace ℝ G] {f : G → E}
  {s : Set G} {x : G} {n : WithTop ℕ∞}, ContDiffWithinAt ℝ n f s x → f x ≠ 0 → ContDiffWithinAt ℝ n (fun y => ‖f y‖) s x
-- Mathlib.RingTheory.Smooth.Locus
Algebra.smoothLocus_eq_compl_support_inter : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [Algebra.EssFiniteType R A],
  Algebra.smoothLocus R A = (Module.support A (Algebra.H1Cotangent R A))ᶜ ∩ Module.freeLocus A Ω[A⁄R]
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.Functor.CorepresentableBy.ext : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C (Type v)} {X : C}
  {e e' : F.CorepresentableBy X},
  e.homEquiv (CategoryTheory.CategoryStruct.id X) = e'.homEquiv (CategoryTheory.CategoryStruct.id X) → e = e'
-- Lean.Data.Lsp.Extra
Lean.Lsp.instFromJsonLeanImportKind.fromJson : Lean.Json → Except String Lean.Lsp.LeanImportKind
-- Mathlib.NumberTheory.ZetaValues
/-- The multiplication theorem. Proof follows https://math.stackexchange.com/a/1721099/38218.  -/
bernoulliFun_mul : ∀ (k : ℕ) {m : ℕ},
  m ≠ 0 → ∀ (x : ℝ), bernoulliFun k (↑m * x) = ↑m ^ k / ↑m * ∑ i ∈ Finset.range m, bernoulliFun k (x + ↑i / ↑m)
-- Mathlib.Data.Finsupp.MonomialOrder.DegLex
Finsupp.DegLex.lt_def : ∀ {α : Type u_1} [inst : LT α] {a b : DegLex (α →₀ ℕ)},
  a < b ↔
    toLex (Finsupp.degree (ofDegLex a), toLex (ofDegLex a)) < toLex (Finsupp.degree (ofDegLex b), toLex (ofDegLex b))
-- Mathlib.Data.Seq.Defs
Stream'.Seq.cons_eq_cons : ∀ {α : Type u} {x x' : α} {s s' : Stream'.Seq α}, Stream'.Seq.cons x s = Stream'.Seq.cons x' s' ↔ x = x' ∧ s = s'
-- Mathlib.LinearAlgebra.Projection
/-- Projection to the image of an injection along a complement.

This has an advantage over `Submodule.projectionOnto` in that it allows the user better
definitional control over the type.  -/
LinearMap.linearProjOfIsCompl : {R : Type u_1} →
  [inst : Ring R] →
    {E : Type u_2} →
      [inst_1 : AddCommGroup E] →
        [inst_2 : Module R E] →
          (q : Submodule R E) →
            {F : Type u_7} →
              [inst_3 : AddCommGroup F] →
                [inst_4 : Module R F] → (i : F →ₗ[R] E) → Function.Injective ⇑i → IsCompl i.range q → E →ₗ[R] F
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
MultipliableUniformly.exists : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : CommMonoid α] {f : ι → β → α} [inst_1 : UniformSpace α],
  MultipliableUniformly f → ∃ g, HasProdUniformly f g
-- Init.Prelude
/-- A string is a sequence of Unicode scalar values.

At runtime, strings are represented by [dynamic arrays](https://en.wikipedia.org/wiki/Dynamic_array)
of bytes using the UTF-8 encoding. Both the size in bytes (`String.utf8ByteSize`) and in characters
(`String.length`) are cached and take constant time. Many operations on strings perform in-place
modifications when the reference to the string is unique.
 -/
String : Type
-- Mathlib.Data.Real.ConjExponents
NNReal.HolderConjugate.mul_eq_add : ∀ {p q : NNReal}, p.HolderConjugate q → p * q = p + q
-- Mathlib.Logic.Embedding.Basic
/-- Fixing an element `a : α` gives an embedding `β ↪ α × β`.  -/
Function.Embedding.sectR : {α : Type u_1} → α → (β : Type u_2) → β ↪ α × β
-- Mathlib.Data.Matrix.Diagonal
Matrix.diagonal_one' : ∀ {n : Type u_3} {α : Type v} [inst : DecidableEq n] [inst_1 : Zero α] [inst_2 : One α], Matrix.diagonal 1 = 1
-- Std.Time.DateTime.WallTime
Std.Time.WallTime.instHAddOffset_2 : HAdd Std.Time.WallTime Std.Time.Hour.Offset Std.Time.WallTime
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
AffineSubspace.map_direction : ∀ {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁] [inst_4 : AddCommGroup V₂]
  [inst_5 : Module k V₂] [inst_6 : AddTorsor V₂ P₂] (f : P₁ →ᵃ[k] P₂) (s : AffineSubspace k P₁),
  (AffineSubspace.map f s).direction = Submodule.map f.linear s.direction
-- Init.Data.Hashable
instHashablePUnit : Hashable PUnit.{u}
-- Batteries.Data.MLList.Basic
/-- Constructs a `MLList` from head and tail.
 -/
MLList.cons : {α : Type u_1} → {m : Type u_1 → Type u_1} → α → MLList m α → MLList m α
-- Mathlib.Analysis.Complex.AbelLimit
/-- Auxiliary lemma for Abel's limit theorem. The difference between the sum `l` at 1 and the
power series's value at a point `z` away from 1 can be rewritten as `1 - z` times a power series
whose coefficients are tail sums of `l`.  -/
Complex.abel_aux : ∀ {f : ℕ → ℂ} {l : ℂ},
  Filter.Tendsto (fun n => ∑ i ∈ Finset.range n, f i) Filter.atTop (nhds l) →
    ∀ {z : ℂ},
      ‖z‖ < 1 →
        Filter.Tendsto (fun n => (1 - z) * ∑ i ∈ Finset.range n, (l - ∑ j ∈ Finset.range (i + 1), f j) * z ^ i)
          Filter.atTop (nhds (l - ∑' (n : ℕ), f n * z ^ n))
-- Mathlib.Data.List.Lookmap
_private.Mathlib.Data.List.Lookmap.0.List.replaceFTR.go.match_1.splitter : {α : Type u_1} →
  (motive : List α → Array α → Sort u_2) →
    (x : List α) →
      (x_1 : Array α) →
        ((acc : Array α) → motive [] acc) →
          ((x : α) → (xs : List α) → (acc : Array α) → motive (x :: xs) acc) → motive x x_1
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.kernelSequenceCycles_g : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n₀ n₁ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.kernelSequenceCycles._auto_1),
  (X.kernelSequenceCycles f g n₀ n₁ hn₁).g = X.δ f g n₀ n₁ hn₁
-- Mathlib.Data.Fin.Tuple.Basic
/-- A weak version of `Fin.find_congr`, requiring `p = q` everywhere.  -/
Fin.find_congr' : ∀ {n : ℕ} {p q : Fin n → Prop} [inst : DecidablePred p] [inst_1 : DecidablePred q] {hp : ∃ i, p i} {hq : ∃ i, q i},
  (∀ {i : Fin n}, p i ↔ q i) → Fin.find p hp = Fin.find q hq
-- Init.Data.BitVec.Lemmas
BitVec.not_and : ∀ {w : ℕ} {x y : BitVec w}, ~~~(x &&& y) = ~~~x ||| ~~~y
-- Lean.Data.Lsp.Basic
Lean.Lsp.instFromJsonDocumentChange : Lean.FromJson Lean.Lsp.DocumentChange
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
Convexity.iConvexComb.eq_def : ∀ {R : Type u_1} {M : Type u_3} {I : Type u_6} [inst : PartialOrder R] [inst_1 : Semiring R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : Convexity.ConvexSpace R M] (s : Convexity.StdSimplex R I) (f : I → M),
  Convexity.iConvexComb s f = Convexity.sConvexComb (Convexity.StdSimplex.map f s)
-- Mathlib.RepresentationTheory.Continuous.TopRep
/-- The constant function `rep ⟶ C(G, rep)` as a natural transformation.  -/
TopRep.coind₁ι : {k : Type u} →
  [inst : TopologicalSpace k] →
    [inst_1 : Ring k] →
      {G : Type v} →
        [inst_2 : Group G] →
          [inst_3 : TopologicalSpace G] →
            [inst_4 : IsTopologicalGroup G] → CategoryTheory.Functor.id (TopRep k G) ⟶ TopRep.coind₁Functor k G
-- Mathlib.Algebra.Group.Basic
sub_sub_cancel_left : ∀ {G : Type u_3} [inst : AddCommGroup G] (a b : G), a - b - a = -b
-- Mathlib.CategoryTheory.Bicategory.SingleObj
CategoryTheory.MonoidalSingleObj.endMonoidalStarFunctor_map : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {X Y : CategoryTheory.EndMonoidal (CategoryTheory.MonoidalSingleObj.star C)} (f : X ⟶ Y),
  (CategoryTheory.MonoidalSingleObj.endMonoidalStarFunctor C).map f = f
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
/-- Mapping from terms to variables representing nonlinear terms.
For example, suppose the denotation of variable `x` is the nonlinear term `a*b*c`,
and `y` is the nonlinear term `a / d`. Then the mapping contains the entries
- `a ↦ [x, y]`
- `b ↦ [x]`
- `c ↦ [x]`
- `d ↦ [y]`
 -/
Lean.Meta.Grind.Arith.Cutsat.State.nonlinearOccs : Lean.Meta.Grind.Arith.Cutsat.State → Lean.PHashMap Int.Internal.Linear.Var (List Int.Internal.Linear.Var)
-- Mathlib.RingTheory.Polynomial.Pochhammer
/-- `descPochhammer R n` is `0` for `0, 1, …, n-1`.  -/
descPochhammer_eval_coe_nat_of_lt : ∀ {R : Type u} [inst : Ring R] {k n : ℕ}, k < n → Polynomial.eval (↑k) (descPochhammer R n) = 0
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.cyclesOpIso_inv_op_iCycles : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasRightHomology],
  CategoryTheory.CategoryStruct.comp S.cyclesOpIso.inv S.op.iCycles = S.pOpcycles.op
-- Lean.Meta.Tactic.Grind.Theorems
/-- A proof term provided directly to a call to `grind` where `ref`
is the provided grind argument. The `id` is a unique identifier for the call.
 -/
Lean.Meta.Grind.Origin.stx : Lean.Name → Lean.Syntax → Lean.Meta.Grind.Origin
-- Mathlib.RingTheory.PowerSeries.Substitution
PowerSeries.C.eq_1 : ∀ {R : Type u_1} [inst : Semiring R], PowerSeries.C = MvPowerSeries.C
-- Mathlib.Algebra.Group.Opposite
SemiconjBy.unop : ∀ {α : Type u_1} [inst : Mul α] {a x y : αᵐᵒᵖ},
  SemiconjBy a x y → SemiconjBy (MulOpposite.unop a) (MulOpposite.unop y) (MulOpposite.unop x)
-- Mathlib.Data.Nat.Totient
Nat.prime_pow_pow_totient_ediv_prod : ∀ {p k : ℕ},
  Nat.Prime p →
    0 < k →
      (p ^ k) ^ (p ^ k).totient / ∏ q ∈ (p ^ k).primeFactors, q ^ ((p ^ k).totient / (q - 1)) =
        p ^ (p ^ (k - 1) * ((p - 1) * k - 1))
-- Mathlib.MeasureTheory.Constructions.ProjectiveFamilyContent
MeasureTheory.projectiveFamilyContent.congr_simp : ∀ {ι : Type u_1} {α : ι → Type u_2} {mα : (i : ι) → MeasurableSpace (α i)}
  {P P_1 : (J : Finset ι) → MeasureTheory.Measure ((j : ↥J) → α ↑j)} (e_P : P = P_1)
  (hP : MeasureTheory.IsProjectiveMeasureFamily P),
  MeasureTheory.projectiveFamilyContent hP = MeasureTheory.projectiveFamilyContent ⋯
-- Init.SimpLemmas
bne_eq_false_iff_eq : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a b : α}, (a != b) = false ↔ a = b
-- Mathlib.Algebra.Group.Subsemigroup.Basic
/-- Additive closure of an additive subsemigroup `S` equals `S`  -/
AddSubsemigroup.closure_eq : ∀ {M : Type u_1} [inst : Add M] (S : AddSubsemigroup M), AddSubsemigroup.closure ↑S = S
-- Mathlib.Probability.Distributions.Binomial
ProbabilityTheory.binomial.eq_1 : ∀ (n : ℕ) (p : ↑unitInterval),
  ProbabilityTheory.binomial n p = MeasureTheory.Measure.map Set.ncard (ProbabilityTheory.setBernoulli (Set.Iio n) p)
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.coproducts_eq_self : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C)
  [CategoryTheory.MorphismProperty.IsStableUnderCoproducts.{w, v, u} W],
  CategoryTheory.MorphismProperty.coproducts.{w, v, u} W = W
-- Mathlib.RingTheory.Spectrum.Prime.Basic
PrimeSpectrum.nilradical_eq_iInf : ∀ {R : Type u} [inst : CommSemiring R], nilradical R = iInf PrimeSpectrum.asIdeal
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomAddAct.instAddSemigroupOfAddOpposite : {M : Type u_1} → [AddSemigroup Mᵃᵒᵖ] → AddSemigroup Mᵈᵃᵃ
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.postcompose₂_obj_obj_obj_map : ∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] {E : Type u_7} [inst_2 : CategoryTheory.Category.{v_7, u_7} E]
  {E' : Type u_8} [inst_3 : CategoryTheory.Category.{v_8, u_8} E'] (X : CategoryTheory.Functor E E')
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ E)) (X_1 : C₁) {X_2 Y : C₂} (f : X_2 ⟶ Y),
  (((CategoryTheory.Functor.postcompose₂.obj X).obj F).obj X_1).map f = X.map ((F.obj X_1).map f)
-- Init.Data.BitVec.Lemmas
BitVec.not_xor_left : ∀ {w : ℕ} {x y : BitVec w}, ~~~(x ^^^ y) = ~~~x ^^^ y
-- Mathlib.Algebra.Order.Floor.Ring
Int.ceil_lt_add_one : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] [IsOrderedRing R] (a : R), ↑⌈a⌉ < a + 1
-- Mathlib.Topology.ContinuousMap.StarOrdered
ContinuousSqrt.mk : {R : Type u_1} →
  [inst : LE R] →
    [inst_1 : NonUnitalSemiring R] →
      [inst_2 : TopologicalSpace R] →
        (sqrt : R × R → R) →
          ContinuousOn sqrt {x | x.1 ≤ x.2} →
            (∀ (x : R × R), x.1 ≤ x.2 → 0 ≤ sqrt x) →
              (∀ (x : R × R), x.1 ≤ x.2 → x.2 = x.1 + sqrt x * sqrt x) → ContinuousSqrt R
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getThenInsertIfNew?_snd : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α],
  m.WF → ∀ {k : α} {v : β}, (m.getThenInsertIfNew? k v).2 = m.insertIfNew k v
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKeyD_empty : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {a fallback : α},
  ∅.getKeyD a fallback = fallback
-- Mathlib.Data.NNReal.Defs
NNReal.iSup_empty : ∀ {ι : Sort u_1} [IsEmpty ι] (f : ι → NNReal), ⨆ i, f i = 0
-- Mathlib.GroupTheory.SpecificGroups.Dihedral
DihedralGroup.exponent : ∀ {n : ℕ}, Monoid.exponent (DihedralGroup n) = lcm n 2
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.equiv_apply : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] [inst_1 : Ring R] (v : Valuation R Γ₀)
  (self : WithVal v), (WithVal.equiv v) self = self.ofVal