mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
/-- Reinterpret a `NonUnitalStarSubalgebra` as a `NonUnitalSubalgebra`.  -/
NonUnitalStarSubalgebra.toNonUnitalSubalgebra : {R : Type u} →
  {A : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : NonUnitalNonAssocSemiring A] →
        [inst_2 : Module R A] → [inst_3 : Star A] → NonUnitalStarSubalgebra R A → NonUnitalSubalgebra R A
-- Mathlib.Order.Filter.Pointwise
Filter.mul_bot : ∀ {α : Type u_2} [inst : Mul α] {f : Filter α}, f * ⊥ = ⊥
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
/-- Coevaluation of an exact pairing.

Do not use directly. Use `ExactPairing.coevaluation` instead.  -/
CategoryTheory.ExactPairing.coevaluation' : {C : Type u₁} →
  {inst : CategoryTheory.Category.{v₁, u₁} C} →
    {inst_1 : CategoryTheory.MonoidalCategory C} →
      {X Y : C} →
        [self : CategoryTheory.ExactPairing X Y] →
          CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj X Y
-- Mathlib.Topology.ContinuousMap.ContinuousSqrt
instContinuousSqrtComplex : ContinuousSqrt ℂ
-- Mathlib.RingTheory.Extension.Basic
/-- The quotient map from the kernel of `P → S` onto the cotangent space.  -/
Algebra.Extension.Cotangent.mk : {R : Type u} →
  {S : Type v} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] → [inst_2 : Algebra R S] → {P : Algebra.Extension R S} → ↥P.ker →ₗ[P.Ring] P.Cotangent
-- Mathlib.Topology.Algebra.Valued.ValuedField
Valued.extension_eq_zero_iff : ∀ {K : Type u_1} [inst : Field K] {Γ₀ : Type u_2} [inst_1 : LinearOrderedCommGroupWithZero Γ₀] [hv : Valued K Γ₀]
  {x : UniformSpace.Completion K}, Valued.extension x = 0 ↔ x = 0
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.inhabited : Inhabited Ordinal.{u_1}
-- Init.Grind.ToIntLemmas
Lean.Grind.ToInt.mul_congr : ∀ {α : Type u_1} {i : Lean.Grind.IntInterval} [inst : Lean.Grind.ToInt α i] [inst_1 : Mul α] [Lean.Grind.ToInt.Mul α i]
  {a b : α} {a' b' : ℤ}, ↑a = a' → ↑b = b' → ↑(a * b) = i.wrap (a' * b')
-- Mathlib.Algebra.Homology.DerivedCategory.SingleTriangle
/-- The distinguished triangle in the derived category of `C` given by a
short exact short complex in `C`.  -/
CategoryTheory.ShortComplex.ShortExact.singleTriangle_distinguished : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact),
  hS.singleTriangle ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.instCommGroup : {α : Type u_1} → {β : Type u_2} → [inst : MeasurableSpace α] → [CommGroup β] → CommGroup (MeasureTheory.SimpleFunc α β)
-- Aesop.Forward.Match.Types
Aesop.instHashableForwardRuleMatch.hash : Aesop.ForwardRuleMatch → UInt64
-- Lean.Data.Json.Basic
Lean.Json.getObjValD : Lean.Json → String → Lean.Json
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.Const.getEntryLED : {α : Type u} → {β : Type v} → [Ord α] → α → (Std.DTreeMap.Internal.Impl α fun x => β) → α × β → α × β
-- Mathlib.LinearAlgebra.Matrix.Kronecker
Matrix.kroneckerMap_zero_right : ∀ {α : Type u_3} {β : Type u_5} {γ : Type u_7} {l : Type u_9} {m : Type u_10} {n : Type u_11} {p : Type u_12}
  [inst : Zero β] [inst_1 : Zero γ] (f : α → β → γ),
  (∀ (a : α), f a 0 = 0) → ∀ (A : Matrix l m α), Matrix.kroneckerMap f A 0 = 0
-- Mathlib.Topology.Category.TopCat.Opens
/-- `Opens.map f` gives the functor from open sets in Y to open set in X,
given by taking preimages under f.  -/
TopologicalSpace.Opens.map : {X Y : TopCat} → (X ⟶ Y) → CategoryTheory.Functor (TopologicalSpace.Opens ↑Y) (TopologicalSpace.Opens ↑X)
-- Mathlib.Analysis.Meromorphic.Basic
/-- Eta-expanded form of `MeromorphicOn.add` -/
MeromorphicOn.fun_add : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f g : 𝕜 → E} {U : Set 𝕜},
  MeromorphicOn f U → MeromorphicOn g U → MeromorphicOn (fun i => f i + g i) U
-- Mathlib.RingTheory.Congruence.Defs
RingCon.comap_nonUnitalRingHomComp : ∀ {R : Type u_5} {R' : Type u_6} {R'' : Type u_7} [inst : NonUnitalNonAssocSemiring R]
  [inst_1 : NonUnitalNonAssocSemiring R'] [inst_2 : NonUnitalNonAssocSemiring R''] (J : RingCon R) (g : R' →ₙ+* R)
  (f : R'' →ₙ+* R'), J.comap (g.comp f) = (J.comap g).comap f
-- Init.Data.SInt.Bitwise
Int32.ofBitVec_intMax : Int32.ofBitVec (BitVec.intMax 32) = Int32.maxValue
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
MonoidAlgebra.comapDomain_single_map : ∀ {R : Type u_3} {M : Type u_6} {N : Type u_7} [inst : Semiring R] (f : M → N) (hf : Function.Injective f) (m : M)
  (r : R), MonoidAlgebra.comapDomain f hf (MonoidAlgebra.single (f m) r) = MonoidAlgebra.single m r
-- Std.Data.DHashMap.Raw
Std.DHashMap.Raw.WF.below.containsThenInsert₀ : ∀ {α : Type u}
  {motive : {β : α → Type v} → [inst : BEq α] → [inst_1 : Hashable α] → (a : Std.DHashMap.Raw α β) → a.WF → Prop}
  {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} {h : 0 < m.buckets.size} {a : α}
  {b : β a} (a_1 : m.WF), Std.DHashMap.Raw.WF.below a_1 → motive m a_1 → Std.DHashMap.Raw.WF.below ⋯
-- Lean.Data.Lsp.Basic
Lean.Lsp.WorkDoneProgressBegin.mk.sizeOf_spec : ∀ (toWorkDoneProgressReport : Lean.Lsp.WorkDoneProgressReport) (title : String),
  sizeOf { toWorkDoneProgressReport := toWorkDoneProgressReport, title := title } =
    1 + sizeOf toWorkDoneProgressReport + sizeOf title
-- Mathlib.RepresentationTheory.Homological.Resolution
Rep.standardComplex.εToSingle₀_comp_eq : ∀ (k G : Type u) [inst : CommRing k] [inst_1 : Monoid G],
  CategoryTheory.CategoryStruct.comp
      (((CategoryTheory.forget₂ (Rep.{u, u, u} k G) (ModuleCat k)).mapHomologicalComplex (ComplexShape.down ℕ)).map
        (Rep.standardComplex.εToSingle₀ k G))
      ((HomologicalComplex.singleMapHomologicalComplex (CategoryTheory.forget₂ (Rep.{u, u, u} k G) (ModuleCat k))
              (ComplexShape.down ℕ) 0).hom.app
        (Rep.trivial k G k)) =
    (Rep.standardComplex.forget₂ToModuleCatHomotopyEquiv k G).hom
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
/-- The norm of an element in the `v`-adic completion of `K`. See `FinitePlace.norm_embedding`
for the equality involving `‖embedding v x‖` on the LHS.  -/
NumberField.FinitePlace.norm_def : ∀ {K : Type u_1} [inst : Field K] {R : Type u_2} [inst_1 : CommRing R] [inst_2 : Algebra R K]
  [inst_3 : IsDedekindDomain R] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R)
  [inst_5 : Module.Finite ℤ R] [inst_6 : Module.Free ℤ R] (x : IsDedekindDomain.HeightOneSpectrum.adicCompletion K v),
  ‖x‖ = ↑((WithZeroMulInt.toNNReal ⋯) (Valued.v x))
-- Lean.Parser.Term
Lean.Parser.Term.quotedName.formatter : Lean.PrettyPrinter.Formatter
-- Init.Data.List.Lemmas
List.set_cons_succ : ∀ {α : Type u_1} {x : α} {xs : List α} {i : ℕ} {a : α}, (x :: xs).set (i + 1) a = x :: xs.set i a
-- Mathlib.CategoryTheory.Limits.HasLimits
/-- The cone morphism from any cone to the arbitrary choice of limit cone.  -/
CategoryTheory.Limits.limit.coneMorphism : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {F : CategoryTheory.Functor J C} →
          [inst_2 : CategoryTheory.Limits.HasLimit F] →
            (c : CategoryTheory.Limits.Cone F) → c ⟶ CategoryTheory.Limits.limit.cone F
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
CategoryTheory.OverPresheafAux.YonedaCollection.mk_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)}
  {F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} {X : C}
  (s : CategoryTheory.yoneda.obj X ⟶ A) (x : F.obj (Opposite.op (CategoryTheory.CostructuredArrow.mk s))),
  (CategoryTheory.OverPresheafAux.YonedaCollection.mk s x).fst = s
-- Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
_private.Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic.0.CategoryTheory.Limits.compNatIso.match_1.eq_1 : ∀ (motive : CategoryTheory.Limits.WalkingParallelPair → Sort u_1)
  (h_1 : Unit → motive CategoryTheory.Limits.WalkingParallelPair.zero)
  (h_2 : Unit → motive CategoryTheory.Limits.WalkingParallelPair.one),
  (match CategoryTheory.Limits.WalkingParallelPair.zero with
    | CategoryTheory.Limits.WalkingParallelPair.zero => h_1 ()
    | CategoryTheory.Limits.WalkingParallelPair.one => h_2 ()) =
    h_1 ()
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get?_diff! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  m₁.WF →
    m₂.WF →
      ∀ {k : α}, (m₁.diff! m₂).get? k = if Std.DTreeMap.Internal.Impl.contains k m₂ = true then none else m₁.get? k
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.contains.match_1.splitter : (motive : Ordering → Sort u_1) →
  (x : Ordering) → (Unit → motive Ordering.lt) → (Unit → motive Ordering.gt) → (Unit → motive Ordering.eq) → motive x
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
/-- Monotone convergence theorem for real-valued functions and Bochner integrals  -/
MeasureTheory.integral_tendsto_of_tendsto_of_antitone : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : ℕ → α → ℝ} {F : α → ℝ},
  (∀ (n : ℕ), MeasureTheory.Integrable (f n) μ) →
    MeasureTheory.Integrable F μ →
      (∀ᵐ (x : α) ∂μ, Antitone fun n => f n x) →
        (∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) Filter.atTop (nhds (F x))) →
          Filter.Tendsto (fun n => ∫ (x : α), f n x ∂μ) Filter.atTop (nhds (∫ (x : α), F x ∂μ))
-- Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
/-- The algebra morphism `A →ₐ[R] A ⊗[R] B` sending `a` to `a ⊗ₜ 1`.  -/
GradedTensorProduct.includeLeft : {R : Type u_1} →
  {ι : Type u_2} →
    {A : Type u_3} →
      {B : Type u_4} →
        [inst : CommSemiring ι] →
          [inst_1 : DecidableEq ι] →
            [inst_2 : CommRing R] →
              [inst_3 : Ring A] →
                [inst_4 : Ring B] →
                  [inst_5 : Algebra R A] →
                    [inst_6 : Algebra R B] →
                      (𝒜 : ι → Submodule R A) →
                        (ℬ : ι → Submodule R B) →
                          [inst_7 : GradedAlgebra 𝒜] →
                            [inst_8 : GradedAlgebra ℬ] →
                              [inst_9 : Module ι (Additive ℤˣ)] → A →ₐ[R] GradedTensorProduct R 𝒜 ℬ
-- Mathlib.Data.Set.Restrict
Set.domRestrict_comp_codRestrict : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {f : ι → α} {g : α → β} {b : Set α} (h : ∀ (x : ι), f x ∈ b),
  b.domRestrict g ∘ Set.codRestrict f b h = g ∘ f
-- Init.Data.String.Pattern.Basic
String.Slice.Pattern.ToForwardSearcher.DefaultForwardSearcher.mk.inj : ∀ {ρ : Type} {pat : ρ} {s : String.Slice} {currPos currPos_1 : s.Pos},
  { currPos := currPos } = { currPos := currPos_1 } → currPos = currPos_1
-- Mathlib.Topology.Order.Category.AlexDisc
AlexDisc.mk.injEq : ∀ (toTopCat : TopCat) [is_alexandrovDiscrete : AlexandrovDiscrete ↑toTopCat] (toTopCat_1 : TopCat)
  (is_alexandrovDiscrete_1 : AlexandrovDiscrete ↑toTopCat_1),
  ({ toTopCat := toTopCat, is_alexandrovDiscrete := is_alexandrovDiscrete } =
      { toTopCat := toTopCat_1, is_alexandrovDiscrete := is_alexandrovDiscrete_1 }) =
    (toTopCat = toTopCat_1)
-- Lean.Meta.Tactic.Grind.Arith.Linear.StructId
_private.Lean.Meta.Tactic.Grind.Arith.Linear.StructId.0.Lean.Meta.Grind.Arith.Linear.mkRingInst? : Lean.Level → Lean.Expr → Option Lean.Expr → Lean.Meta.Grind.GoalM (Option Lean.Expr)
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
ContinuousLinearMap.smul_compLp : ∀ {α : Type u_1} {E : Type u_4} {F : Type u_5} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F] {𝕜 : Type u_6} {𝕜' : Type u_7}
  [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜'] [inst_4 : NormedSpace 𝕜 E]
  [inst_5 : NormedSpace 𝕜' F] {σ : 𝕜 →+* 𝕜'} [inst_6 : RingHomIsometric σ] {𝕜'' : Type u_8} [inst_7 : NormedRing 𝕜'']
  [inst_8 : Module 𝕜'' F] [inst_9 : IsBoundedSMul 𝕜'' F] [inst_10 : SMulCommClass 𝕜' 𝕜'' F] (c : 𝕜'') (L : E →SL[σ] F)
  (f : ↥(MeasureTheory.Lp E p μ)), (c • L).compLp f = c • L.compLp f
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
IntermediateField.adjoin_root_eq_top : ∀ {K : Type u} [inst : Field K] (p : Polynomial K) [inst_1 : Fact (Irreducible p)], K⟮AdjoinRoot.root p⟯ = ⊤
-- Mathlib.Analysis.Normed.Group.Defs
NormedCommGroup.toNormedGroup : {E : Type u_5} → [NormedCommGroup E] → NormedGroup E
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.shortComplexFunctor_obj_X₃ : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} (c : ComplexShape ι) (i : ι) (K : HomologicalComplex C c),
  ((HomologicalComplex.shortComplexFunctor C c i).obj K).X₃ = K.X (c.next i)
-- Mathlib.CategoryTheory.Preadditive.Mat
CategoryTheory.Mat_.Embedding.instAdditiveEmbedding : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C],
  (CategoryTheory.Mat_.embedding C).Additive
-- Mathlib.Algebra.Module.Submodule.Ker
LinearMap.le_ker_iff_map : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective τ₁₂] {f : M →ₛₗ[τ₁₂] M₂} {p : Submodule R M}, p ≤ f.ker ↔ Submodule.map f p = ⊥
-- Mathlib.Order.Filter.Tendsto
Filter.tendsto_top : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {l : Filter α}, Filter.Tendsto f l ⊤
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.Term.relabel_comp_relabel : ∀ {L : FirstOrder.Language} {α : Type u'} {β : Type v'} {γ : Type u_1} (f : α → β) (g : β → γ),
  FirstOrder.Language.Term.relabel g ∘ FirstOrder.Language.Term.relabel f = FirstOrder.Language.Term.relabel (g ∘ f)
-- Mathlib.Data.Nat.PrimeFin
Nat.le_of_mem_primeFactors : ∀ {n p : ℕ}, p ∈ n.primeFactors → p ≤ n
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.get?_eq_some_getD_of_contains : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α],
  m.WF → ∀ {a fallback : α}, m.contains a = true → m.get? a = some (m.getD a fallback)
-- Mathlib.GroupTheory.Index
/-- **Alias** of `AddSubgroup.isFiniteRelIndex_of_le_left`. -/
AddSubgroup.isFiniteRelIndex_of_le : ∀ {G : Type u_1} [inst : AddGroup G] {H K : AddSubgroup G} (L : AddSubgroup G) [H.IsFiniteRelIndex L],
  H ≤ K → K.IsFiniteRelIndex L
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.AddMod.Hom.mk''_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D]
  {A : C} [inst_4 : CategoryTheory.AddMonObj A] {M N : D} [inst_5 : CategoryTheory.AddModObj A M]
  [inst_6 : CategoryTheory.AddModObj A N] (f : M ⟶ N)
  (vadd_hom :
    autoParam
      (CategoryTheory.CategoryStruct.comp CategoryTheory.AddModObj.vadd f =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight A f)
          CategoryTheory.AddModObj.vadd)
      CategoryTheory.AddMod.Hom.mk''._auto_1),
  (CategoryTheory.AddMod.Hom.mk'' f vadd_hom).hom = f
-- Lean.Environment
Lean.MonadEnv.getEnv : {m : Type → Type} → [self : Lean.MonadEnv m] → m Lean.Environment
-- Mathlib.Order.LatticeIntervals
Set.Ici.isCompl_iff : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : OrderTop α] {a : α} {x y : ↑(Set.Ici a)},
  IsCompl x y ↔ ↑x ⊓ ↑y = a ∧ Codisjoint ↑x ↑y
-- Mathlib.Geometry.Manifold.StructureGroupoid
groupoid_of_pregroupoid_le : ∀ {H : Type u_1} [inst : TopologicalSpace H] (PG₁ PG₂ : Pregroupoid H),
  (∀ (f : H → H) (s : Set H), PG₁.property f s → PG₂.property f s) → PG₁.groupoid ≤ PG₂.groupoid
-- Mathlib.Topology.UniformSpace.UniformConvergence
TendstoUniformlyOnFilter.mono_left : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι}
  {p' : Filter α} {p'' : Filter ι}, TendstoUniformlyOnFilter F f p p' → p'' ≤ p → TendstoUniformlyOnFilter F f p'' p'
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
CategoryTheory.Bicategory.Adj.Bicategory.leftUnitor_inv_τr : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : CategoryTheory.Bicategory.Adj B} (α : a ⟶ b),
  (CategoryTheory.Bicategory.Adj.Bicategory.leftUnitor α).inv.τr = (CategoryTheory.Bicategory.rightUnitor α.r).hom
-- Mathlib.Topology.Category.TopCat.Limits.Konig
/-- Partial sections of a cofiltered limit are sections when restricted to
a finite subset of objects and morphisms of `J`.
 -/
TopCat.partialSections : {J : Type u} →
  [inst : CategoryTheory.SmallCategory J] →
    (F : CategoryTheory.Functor J TopCat) →
      {G : Finset J} → Finset (TopCat.FiniteDiagramArrow✝ G) → Set ((j : J) → ↑(F.obj j))
-- Mathlib.Algebra.MvPolynomial.Degrees
MvPolynomial.degreesLE_nsmul : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (s : Multiset σ) (n : ℕ),
  MvPolynomial.degreesLE R σ (n • s) = MvPolynomial.degreesLE R σ s ^ n
-- Mathlib.Algebra.Homology.ExactSequenceFour
/-- If `S` is a complex, this is the morphism from a cokernel of `S.map' k (k + 1)`
to a kernel of `S.map' (k + 2) (k + 3)`.  -/
CategoryTheory.ComposableArrows.IsComplex.cokerToKer' : {C : Type u_1} →
  [inst : CategoryTheory.Category.{u_2, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {n : ℕ} →
        {S : CategoryTheory.ComposableArrows C (n + 3)} →
          S.IsComplex →
            (k : ℕ) →
              (hk : k ≤ n) →
                (cc : CategoryTheory.Limits.CokernelCofork (S.map' k (k + 1) ⋯ ⋯)) →
                  (kf : CategoryTheory.Limits.KernelFork (S.map' (k + 2) (k + 3) ⋯ ⋯)) →
                    CategoryTheory.Limits.IsColimit cc → CategoryTheory.Limits.IsLimit kf → (cc.pt ⟶ kf.pt)
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.ofCoeff_sum : ∀ {R : Type u_1} {M : Type u_4} {ι : Type u_7} [inst : Semiring R] (s : Finset ι) (f : ι → M →₀ R),
  AddMonoidAlgebra.ofCoeff (∑ i ∈ s, f i) = ∑ i ∈ s, AddMonoidAlgebra.ofCoeff (f i)
-- Mathlib.NumberTheory.LucasLehmer
/-- If `1 < p`, then `q p`, the smallest prime factor of `mersenne p`, is more than 2.  -/
LucasLehmer.two_lt_q : ∀ (p' : ℕ), 2 < LucasLehmer.q (p' + 2)
-- Mathlib.Probability.Process.Stopping
MeasureTheory.stoppedValue_stoppedProcess_ae_eq : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : Nonempty ι] {u : ι → Ω → β}
  {τ σ : Ω → WithTop ι} [inst_1 : LinearOrder ι] {μ : MeasureTheory.Measure Ω},
  (∀ᵐ (ω : Ω) ∂μ, σ ω ≠ ⊤) →
    MeasureTheory.stoppedValue (MeasureTheory.stoppedProcess u τ) σ =ᵐ[μ]
      MeasureTheory.stoppedValue u fun ω => min (σ ω) (τ ω)
-- Lean.Compiler.IR.Format
Lean.IR.instToFormatFnBody : Std.ToFormat Lean.IR.FnBody
-- Mathlib.Analysis.Convex.Strict
strictConvex_empty : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : TopologicalSpace E]
  [inst_3 : AddCommMonoid E] [inst_4 : SMul 𝕜 E], StrictConvex 𝕜 ∅
-- Mathlib.Algebra.Lie.TensorProduct
TensorProduct.LieModule.coe_liftLie_eq_lift_coe : ∀ (R : Type u) [inst : CommRing R] (L : Type v) (M : Type w) (N : Type w₁) (P : Type w₂) [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] [inst_7 : AddCommGroup N] [inst_8 : Module R N] [inst_9 : LieRingModule L N]
  [inst_10 : LieModule R L N] [inst_11 : AddCommGroup P] [inst_12 : Module R P] [inst_13 : LieRingModule L P]
  [inst_14 : LieModule R L P] (f : M →ₗ⁅R,L⁆ N →ₗ[R] P),
  ⇑((TensorProduct.LieModule.liftLie R L M N P) f) = ⇑((TensorProduct.LieModule.lift R L M N P) ↑f)
-- Mathlib.RingTheory.SimpleRing.Basic
IsSimpleRing.of_eq_bot_or_eq_top : ∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R] [Nontrivial R],
  (∀ (I : TwoSidedIdeal R), I = ⊥ ∨ I = ⊤) → IsSimpleRing R
-- Std.Http.Data.Chunk
Std.Http.Chunk.instBEqExtensionValue : BEq Std.Http.Chunk.ExtensionValue
-- Mathlib.Data.Nat.GCD.Basic
Nat.pow_sub_one_gcd_pow_sub_one : ∀ (a b c : ℕ), (a ^ b - 1).gcd (a ^ c - 1) = a ^ b.gcd c - 1
-- Lean.Meta.Tactic.Grind.MatchDiscrOnly
Lean.Meta.Grind.reduceSimpMatchDiscrsOnly : Lean.Meta.Simp.Simproc
-- Mathlib.Algebra.Order.Nonneg.Field
Nonneg.inv_mk : ∀ {α : Type u_1} [inst : Semifield α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] {x : α} (hx : 0 ≤ x),
  ⟨x, hx⟩⁻¹ = ⟨x⁻¹, ⋯⟩
-- Mathlib.GroupTheory.GroupAction.Hom
/-- The identity map as an equivariant map.  -/
MulActionHom.id : (M : Type u_2) → {X : Type u_5} → [inst : SMul M X] → X →ₑ[id] X
-- Mathlib.SetTheory.Cardinal.CountableCover
/-- If a space is eventually covered by a countable family of sets, all with cardinality at
most `a`, then the cardinality of the space is also bounded by `a`.  -/
Cardinal.mk_le_of_countable_eventually_mem : ∀ {α : Type u} {ι : Type v} {a : Cardinal.{u}} [Countable ι] {f : ι → Set α} {l : Filter ι} [l.NeBot],
  (∀ (x : α), ∀ᶠ (i : ι) in l, x ∈ f i) → (∀ (i : ι), Cardinal.mk ↑(f i) ≤ a) → Cardinal.mk α ≤ a
-- Mathlib.Algebra.FreeMonoid.Basic
/-- If `α` is a type, then `FreeAddMonoid α` is the free additive monoid generated by `α`.
This is a monoid equipped with a function `FreeAddMonoid.of : α → FreeAddMonoid α` which has
the following universal property: if `M` is any monoid, and `f : α → M` is any function,
then this function is the composite of `FreeAddMonoid.of` and a unique monoid homomorphism
`FreeAddMonoid.lift f : FreeAddMonoid α →+ M`.

A typical element of `FreeAddMonoid α` is a formal sum of elements of `α`.
For example if `x` and `y` are terms of type `α` then `x + y + y + x` is a
"typical" element of `FreeAddMonoid α`. In particular if `α` is empty
then `FreeAddMonoid α` is isomorphic to the trivial monoid, and if `α` has one term
then `FreeAddMonoid α` is isomorphic to `ℕ`.
If `α` has two or more terms then `FreeAddMonoid α` is not commutative.
One can think of `FreeAddMonoid α` as the type of lists of `α`, with addition
given by concatenation.  -/
FreeAddMonoid : Type u_6 → Type u_6
-- Std.Data.Internal.List.Associative
Std.Internal.List.maxKey!_eq_maxKeyD_default : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  [inst_4 : Inhabited α] {l : List ((a : α) × β a)}, Std.Internal.List.maxKey! l = Std.Internal.List.maxKeyD l default
-- Mathlib.Data.Matrix.Block
Matrix.toBlock_diagonal_self : ∀ {m : Type u_2} {α : Type u_12} [inst : DecidableEq m] [inst_1 : Zero α] (d : m → α) (p : m → Prop),
  (Matrix.diagonal d).toBlock p p = Matrix.diagonal fun i => d ↑i
-- Mathlib.Probability.Kernel.Basic
ProbabilityTheory.Kernel.comapRight.congr_simp : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
  {mγ : MeasurableSpace γ} {f f_1 : γ → β} (e_f : f = f_1) (κ κ_1 : ProbabilityTheory.Kernel α β),
  κ = κ_1 → ∀ (hf : MeasurableEmbedding f), κ.comapRight hf = κ_1.comapRight ⋯
-- Init.Data.List.MinMaxIdx
List.maxIdxOn_eq_get_maxIdxOn? : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] {f : α → β} {xs : List α} (h : xs ≠ []),
  List.maxIdxOn f xs h = (List.maxIdxOn? f xs).get ⋯
-- Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
IsIntegral.map : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {B : Type u_6}
  {C : Type u_7} {F : Type u_8} [inst_3 : Ring B] [inst_4 : Ring C] [inst_5 : Algebra R B] [inst_6 : Algebra A B]
  [inst_7 : Algebra R C] [IsScalarTower R A B] [inst_9 : Algebra A C] [IsScalarTower R A C] {b : B}
  [inst_11 : FunLike F B C] [AlgHomClass F A B C] (f : F), IsIntegral R b → IsIntegral R (f b)
-- Mathlib.Analysis.CStarAlgebra.Multiplier
DoubleCentralizer.norm_snd : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : NormedSpace 𝕜 A] [inst_3 : SMulCommClass 𝕜 A A] [inst_4 : IsScalarTower 𝕜 A A] [inst_5 : StarRing A]
  [CStarRing A] (a : DoubleCentralizer 𝕜 A), ‖a.toProd.2‖ = ‖a‖