mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.Cyclotomic.Basic
/-- Any two `S`-cyclotomic extensions are isomorphic.  -/
IsCyclotomicExtension.algEquiv : (S : Set ℕ) →
  (K : Type w) →
    (L : Type z) →
      [inst : Field K] →
        [inst_1 : Field L] →
          [inst_2 : Algebra K L] →
            [IsCyclotomicExtension S K L] →
              (L' : Type u_1) →
                [inst_4 : Field L'] → [inst_5 : Algebra K L'] → [IsCyclotomicExtension S K L'] → L ≃ₐ[K] L'
-- Mathlib.CategoryTheory.Monoidal.Internal.Types.Grp
/-- The category of group objects in `Type u` is equivalent to the category of groups.  -/
grpTypeEquivalenceGrp : CategoryTheory.Grp (Type u) ≌ GrpCat
-- Mathlib.Data.DFinsupp.Multiset
/-- A DFinsupp version of `Finsupp.toMultiset`.  -/
DFinsupp.toMultiset : {α : Type u_1} → [DecidableEq α] → (Π₀ (x : α), ℕ) →+ Multiset α
-- Mathlib.RingTheory.Multiplicity
Int.decidableMultiplicityFinite : DecidableRel fun a b => FiniteMultiplicity a b
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokenModifier.defaultLibrary.sizeOf_spec : sizeOf Lean.Lsp.SemanticTokenModifier.defaultLibrary = 1
-- Mathlib.CategoryTheory.FiberedCategory.HomLift
CategoryTheory.Functor.IsHomLift.map : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₂} 𝒳] [inst_1 : CategoryTheory.Category.{v₂, u₁} 𝒮]
  {p : CategoryTheory.Functor 𝒳 𝒮} {a b : 𝒳} (φ : a ⟶ b), p.IsHomLift (p.map φ) φ
-- Mathlib.LinearAlgebra.Matrix.Permanent
Matrix.permanent_isEmpty : ∀ {n : Type u_1} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type u_2} [inst_2 : CommSemiring R] [IsEmpty n]
  {A : Matrix n n R}, A.permanent = 1
-- Mathlib.AlgebraicGeometry.Morphisms.FiniteType
AlgebraicGeometry.instLocallyOfFiniteTypeResLE : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U : X.Opens) (V : Y.Opens)
  (e : U ≤ (TopologicalSpace.Opens.map f.base).obj V) [AlgebraicGeometry.LocallyOfFiniteType f],
  AlgebraicGeometry.LocallyOfFiniteType (AlgebraicGeometry.Scheme.Hom.resLE f V U e)
-- Std.Data.DTreeMap.Internal.Queries
_private.Std.Data.DTreeMap.Internal.Queries.0.Std.DTreeMap.Internal.Impl.maxEntryD.match_1.eq_2 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → (a : α) × β a → Sort u_3) (size : ℕ)
  (k : α) (v : β k) (l : Std.DTreeMap.Internal.Impl α β) (x : (a : α) × β a)
  (h_1 : (fallback : (a : α) × β a) → motive Std.DTreeMap.Internal.Impl.leaf fallback)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l : Std.DTreeMap.Internal.Impl α β) →
            (x : (a : α) × β a) →
              motive (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf) x)
  (h_3 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l r : Std.DTreeMap.Internal.Impl α β) →
            (size_1 : ℕ) →
              (k_1 : α) →
                (v_1 : β k_1) →
                  (l_1 r_1 : Std.DTreeMap.Internal.Impl α β) →
                    r = Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1 →
                      (fallback : (a : α) × β a) →
                        motive
                          (Std.DTreeMap.Internal.Impl.inner size k v l
                            (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1))
                          fallback),
  (match Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf, x with
    | Std.DTreeMap.Internal.Impl.leaf, fallback => h_1 fallback
    | Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf, x => h_2 size k v l x
    | Std.DTreeMap.Internal.Impl.inner size k v l r@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1),
      fallback => h_3 size k v l r size_1 k_1 v_1 l_1 r_1 h fallback) =
    h_2 size k v l x
-- Mathlib.CategoryTheory.Limits.Types.Products
CategoryTheory.Limits.Types.binaryProductFunctor_obj_obj : ∀ (X Y : Type u), (CategoryTheory.Limits.Types.binaryProductFunctor.obj X).obj Y = (X × Y)
-- Lean.Elab.PreDefinition.PartialFixpoint.Induction
_private.Lean.Elab.PreDefinition.PartialFixpoint.Induction.0.Lean.Elab.PartialFixpoint.isInductName : Lean.Environment → Lean.Name → Bool
-- Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
/-- In a finite-dimensional inner product space, the dimension of the orthogonal complement of the
span of a nonzero vector is one less than the dimension of the space.  -/
Submodule.finrank_orthogonal_span_singleton : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {n : ℕ} [_i : Fact (Module.finrank 𝕜 E = n + 1)] {v : E}, v ≠ 0 → Module.finrank 𝕜 ↥(𝕜 ∙ v)ᗮ = n
-- Mathlib.Algebra.Order.Monovary
AntivaryOn.pow_left₀ : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semiring α] [inst_1 : PartialOrder α] [IsOrderedRing α]
  [inst_3 : PartialOrder β] {s : Set ι} {f : ι → α} {g : ι → β},
  (∀ i ∈ s, 0 ≤ f i) → AntivaryOn f g s → ∀ (n : ℕ), AntivaryOn (f ^ n) g s
-- Mathlib.CategoryTheory.Limits.FunctorCategory.BinaryBiproducts
/-- The bicone associated with `F` and `G` is a bilimit bicone.  -/
CategoryTheory.Limits.pointwiseBinaryBicone.isBilimit : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] →
        {D : Type u_2} →
          [inst_3 : CategoryTheory.Category.{v_2, u_2} D] →
            (F G : CategoryTheory.Functor D C) → (CategoryTheory.Limits.pointwiseBinaryBicone F G).IsBilimit
-- Mathlib.CategoryTheory.Shift.Adjunction
CategoryTheory.Adjunction.shift_counit_app : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  (adj : F ⊣ G) {A : Type u_3} [inst_2 : AddMonoid A] [inst_3 : CategoryTheory.HasShift C A]
  [inst_4 : CategoryTheory.HasShift D A] [inst_5 : F.CommShift A] [inst_6 : G.CommShift A] [adj.CommShift A] (a : A)
  (Y : D),
  (CategoryTheory.shiftFunctor D a).map (adj.counit.app Y) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso F a).inv.app (G.obj Y))
      (CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.Functor.commShiftIso G a).inv.app Y))
        (adj.counit.app ((CategoryTheory.shiftFunctor D a).obj Y)))
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.Slice.endsWith_prop_iff_get : ∀ {P : Char → Prop} [inst : DecidablePred P] {s : String.Slice},
  s.endsWith P = true ↔ ∃ (h : s.endPos ≠ s.startPos), P ((s.endPos.prev h).get ⋯)
-- Lean.MetavarContext
/-- The metavariable context is a set of metavariable declarations and their assignments.

For more information on specifics see the comment in the file that `MetavarContext` is defined in.
 -/
Lean.MetavarContext : Type
-- Mathlib.Topology.Basic
TopologicalSpace.ext : ∀ {X : Type u} {f g : TopologicalSpace X}, IsOpen = IsOpen → f = g
-- Mathlib.LinearAlgebra.Span.Defs
Disjoint.of_span₀ : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {s t : Set M},
  Disjoint (Submodule.span R s) (Submodule.span R t) → 0 ∉ s → Disjoint s t
-- Mathlib.CategoryTheory.Limits.WeakLimits.WeakKernels
CategoryTheory.Limits.weakKernel.lift_ι_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y : C} (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasWeakKernel f] {W : C} (k : W ⟶ X)
  (h : CategoryTheory.CategoryStruct.comp k f = 0) {Z : C} (h_1 : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.weakKernel.lift f k h)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.weakKernel.ι f) h_1) =
    CategoryTheory.CategoryStruct.comp k h_1
-- Lean.Meta.Tactic.Simp.SimpCongrTheorems
Lean.Meta.SimpCongrTheorems.get : Lean.Meta.SimpCongrTheorems → Lean.Name → List Lean.Meta.SimpCongrTheorem
-- Mathlib.Algebra.Polynomial.FieldDivision
/-- **Alias** of the reverse direction of `Polynomial.mul_div_eq_iff_isRoot`. -/
Polynomial.IsRoot.mul_div_eq : ∀ {R : Type u} {a : R} [inst : Field R] {p : Polynomial R},
  p.IsRoot a → (Polynomial.X - Polynomial.C a) * (p / (Polynomial.X - Polynomial.C a)) = p
-- Init.Data.String.Lemmas.Basic
String.Slice.Pos.cast_toSlice_copy : ∀ {s : String.Slice} {pos : s.Pos}, pos.copy.toSlice.cast ⋯ = pos
-- Std.Http.Test.Helpers
Std.Http.Internal.Test.instHandlerTestHandler : Std.Http.Server.Handler Std.Http.Internal.Test.TestHandler
-- Mathlib.CategoryTheory.Sites.Sheaf
CategoryTheory.Presheaf.IsSheaf.hom_ext_ofArrows : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {J : CategoryTheory.GrothendieckTopology C} {P : CategoryTheory.Functor Cᵒᵖ A},
  CategoryTheory.Presheaf.IsSheaf J P →
    ∀ {I : Type u_1} {S : C} {X : I → C} (f : (i : I) → X i ⟶ S),
      CategoryTheory.Sieve.ofArrows X f ∈ J S →
        ∀ {E : A} {x y : E ⟶ P.obj (Opposite.op S)},
          (∀ (i : I),
              CategoryTheory.CategoryStruct.comp x (P.map (f i).op) =
                CategoryTheory.CategoryStruct.comp y (P.map (f i).op)) →
            x = y
-- Mathlib.NumberTheory.LSeries.HurwitzZetaEven
/-- The function `cosKernel a - 1` has exponential decay at `+∞`, for any `a`.  -/
HurwitzZeta.isBigO_atTop_cosKernel_sub : ∀ (a : UnitAddCircle), ∃ p, 0 < p ∧ (fun x => HurwitzZeta.cosKernel a x - 1) =O[Filter.atTop] fun x => Real.exp (-p * x)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equifibered
CategoryTheory.NatTrans.Coequifibered.of_isIso : ∀ {J : Type u_1} {C : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_3} C] {F G : CategoryTheory.Functor J C} (α : F ⟶ G)
  [CategoryTheory.IsIso α], CategoryTheory.NatTrans.Coequifibered α
-- Mathlib.Data.Int.Fib.Basic
Int.fib_two : Int.fib 2 = 1
-- Mathlib.Algebra.Order.Monoid.Canonical.Defs
CanonicallyOrderedMul.toExistsMulOfLE : ∀ {α : Type u_1} {inst : Mul α} {inst_1 : LE α} [self : CanonicallyOrderedMul α], ExistsMulOfLE α
-- Mathlib.Algebra.Group.Units.Defs
/-- The element of the group of units, corresponding to an element of a monoid which is a unit. As
opposed to `IsUnit.unit`, the inverse is computable and comes from the inversion on `α`. This is
useful to transfer properties of inversion in `Units α` to `α`. See also `toUnits`.  -/
IsUnit.unit' : {α : Type u} → [inst : DivisionMonoid α] → {a : α} → IsUnit a → αˣ
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
Mathlib.Tactic.BicategoryLike.HorizontalComp.cons.inj : ∀ {e : Mathlib.Tactic.BicategoryLike.Mor₂} {η : Mathlib.Tactic.BicategoryLike.WhiskerRight}
  {ηs : Mathlib.Tactic.BicategoryLike.HorizontalComp} {e_1 : Mathlib.Tactic.BicategoryLike.Mor₂}
  {η_1 : Mathlib.Tactic.BicategoryLike.WhiskerRight} {ηs_1 : Mathlib.Tactic.BicategoryLike.HorizontalComp},
  Mathlib.Tactic.BicategoryLike.HorizontalComp.cons e η ηs =
      Mathlib.Tactic.BicategoryLike.HorizontalComp.cons e_1 η_1 ηs_1 →
    e = e_1 ∧ η = η_1 ∧ ηs = ηs_1
-- Mathlib.Data.NNRat.Defs
Rat.instPosMulMono : PosMulMono ℚ
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.mem_lp_const_smul : ∀ {𝕜 : Type u_1} {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)]
  [inst_1 : NormedRing 𝕜] [inst_2 : (i : α) → Module 𝕜 (E i)] [∀ (i : α), IsBoundedSMul 𝕜 (E i)] (c : 𝕜)
  (f : ↥(lp E p)), c • ↑f ∈ lp E p
-- Std.Data.Internal.List.Associative
Std.Internal.List.getEntry_cons : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k}
  (h : Std.Internal.List.containsKey a (⟨k, v⟩ :: l) = true),
  Std.Internal.List.getEntry a (⟨k, v⟩ :: l) h =
    if h' : (k == a) = true then ⟨k, v⟩ else Std.Internal.List.getEntry a l ⋯
-- Mathlib.CategoryTheory.Shift.Twist
/-- Given `t : TwistShiftData C A`, the shift functors on `t.Category`
identify to the shift functors on `C`.  -/
CategoryTheory.TwistShiftData.shiftIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : Type w} →
      [inst_1 : AddMonoid A] →
        [inst_2 : CategoryTheory.HasShift C A] →
          (t : CategoryTheory.TwistShiftData C A) →
            (m : A) → CategoryTheory.shiftFunctor t.Category m ≅ CategoryTheory.shiftFunctor C m
-- Mathlib.ModelTheory.Order
FirstOrder.Language.order.instIsEmptyRelationsOfNatNat : IsEmpty (FirstOrder.Language.order.Relations 0)
-- Mathlib.Analysis.RCLike.Inner
RCLike.wInner_cWeight_const_left : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : Fintype ι] [inst_1 : RCLike 𝕜] (a : 𝕜) (f : ι → 𝕜),
  ⟪Function.const ι a, f⟫ₙ_[𝕜] = Finset.univ.expect fun i => f i * (starRingEnd 𝕜) a
-- Mathlib.Algebra.TrivSqZeroExt.Basic
/-- The canonical inclusion of rings `R → TrivSqZeroExt R M`.  -/
TrivSqZeroExt.inlHom : (R : Type u) →
  (M : Type v) →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → [inst_3 : Module Rᵐᵒᵖ M] → R →+* TrivSqZeroExt R M
-- Mathlib.CategoryTheory.Filtered.Basic
/-- `minToRight j j'` is an arbitrary choice of morphism from `min j j'` to `j'`,
whose existence is ensured by `IsCofiltered`.
 -/
CategoryTheory.IsCofiltered.minToRight : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.IsCofilteredOrEmpty C] → (j j' : C) → CategoryTheory.IsCofiltered.min j j' ⟶ j'
-- Mathlib.Probability.Kernel.Proper
ProbabilityTheory.Kernel.IsProper.restrict_eq_indicator_smul' : ∀ {X : Type u_1} {𝓑 𝓧 : MeasurableSpace X} {π : ProbabilityTheory.Kernel X X},
  π.IsProper → ∀ ⦃B : Set X⦄ (hB : MeasurableSet B) (x : X), (π.restrict ⋯) x = B.indicator (fun x => 1) x • π x
-- Init.SimpLemmas
or_true : ∀ (p : Prop), (p ∨ True) = True
-- ProofWidgets.Presentation.Expr
ProofWidgets.ExprPresentationProps.mk : Lean.Server.WithRpcRef ProofWidgets.ExprWithCtx → ProofWidgets.ExprPresentationProps
-- Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
/-- Consider a point `x` at which a set `s` has density one, with respect to closed balls (i.e.,
a Lebesgue density point of `s`). Then `s` has also density one at `x` with respect to any
measurable set `t`: the proportion of points in `s` belonging to a rescaled copy `{x} + r • t`
of `t` tends to one as `r` tends to zero.  -/
MeasureTheory.Measure.tendsto_addHaar_inter_smul_one_of_density_one : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  [FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (s : Set E) (x : E),
  Filter.Tendsto (fun r => μ (s ∩ Metric.closedBall x r) / μ (Metric.closedBall x r)) (nhdsWithin 0 (Set.Ioi 0))
      (nhds 1) →
    ∀ (t : Set E),
      MeasurableSet t →
        μ t ≠ 0 →
          μ t ≠ ⊤ →
            Filter.Tendsto (fun r => μ (s ∩ ({x} + r • t)) / μ ({x} + r • t)) (nhdsWithin 0 (Set.Ioi 0)) (nhds 1)
-- Mathlib.Order.Hom.CompleteLattice
sInfHom.id_apply : ∀ {α : Type u_2} [inst : InfSet α] (a : α), (sInfHom.id α) a = a
-- Mathlib.FieldTheory.Galois.Basic
Algebra.IsQuadraticExtension.isMulCommutative_galoisGroup : ∀ (F : Type u_1) (K : Type u_2) [inst : Field F] [inst_1 : Field K] [inst_2 : Algebra F K]
  [Algebra.IsQuadraticExtension F K], IsMulCommutative Gal(K/F)
-- Mathlib.Analysis.InnerProductSpace.Harmonic.Basic
/-- **Alias** of `InnerProductSpace.isOpen_setOfPred_harmonicAt`.

---

Harmonicity is an open property.
 -/
InnerProductSpace.isOpen_setOf_harmonicAt : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {F : Type u_2} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] (f : E → F),
  IsOpen {x | InnerProductSpace.HarmonicAt f x}
-- Mathlib.AlgebraicGeometry.Morphisms.Finite
AlgebraicGeometry.IsClosedImmersion.eq_isFinite_inf_mono : @AlgebraicGeometry.IsClosedImmersion =
  @AlgebraicGeometry.IsFinite ⊓ CategoryTheory.MorphismProperty.monomorphisms AlgebraicGeometry.Scheme
-- Mathlib.Tactic.LinearCombination.Lemmas
Mathlib.Tactic.LinearCombination.add_le_eq : ∀ {α : Type u_1} {a₁ a₂ b₁ b₂ : α} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α],
  a₁ ≤ b₁ → a₂ = b₂ → a₁ + a₂ ≤ b₁ + b₂
-- Lean.Meta.Canonicalizer
/-- Auxiliary structure for creating a pointer-equality.
 -/
Lean.Meta.Canonicalizer.ExprVisited : Type
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.revlex_k : Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Mon → Ordering
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getKey_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  [inst_1 : BEq α] [inst_2 : Std.LawfulBEqCmp cmp] (h : t.WF) {l : List (α × β)} {k : α}
  (contains_eq_false : (List.map Prod.fst l).contains k = false) {h' : k ∈ Std.DTreeMap.Raw.Const.insertMany t l},
  (Std.DTreeMap.Raw.Const.insertMany t l).getKey k h' = t.getKey k ⋯
-- Mathlib.RingTheory.Spectrum.Prime.FreeLocus
/-- See `rankAtStalk_tensorProduct_of_isScalarTower` for a hetero-basic version.  -/
Module.rankAtStalk_tensorProduct : ∀ {R : Type uR} {M : Type uM} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Module.Flat R M]
  [Module.Finite R M] (N : Type u_1) [inst_5 : AddCommGroup N] [inst_6 : Module R N] [Module.Finite R N]
  [Module.Flat R N], Module.rankAtStalk (TensorProduct R M N) = Module.rankAtStalk M * Module.rankAtStalk N
-- Mathlib.Algebra.Ring.Hom.Defs
RingHom.coe_monoidHom_mk : ∀ {α : Type u_2} {β : Type u_3} {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →* β) (h₁ : (↑f).toFun 0 = 0)
  (h₂ : ∀ (x_2 y : α), (↑f).toFun (x_2 + y) = (↑f).toFun x_2 + (↑f).toFun y),
  ↑{ toMonoidHom := f, map_zero' := h₁, map_add' := h₂ } = f
-- Mathlib.CategoryTheory.Monoidal.Closed.Ideal
/-- The subcategory of subterminal objects is an exponential ideal.  -/
CategoryTheory.instExponentialIdealSubterminalsSubterminalInclusion : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.MonoidalClosed C], CategoryTheory.ExponentialIdeal (CategoryTheory.subterminalInclusion C)
-- Mathlib.Algebra.Group.TypeTags.Basic
Multiplicative.instCancelCommMonoid : {α : Type u} → [AddCancelCommMonoid α] → CancelCommMonoid (Multiplicative α)
-- Mathlib.Topology.Homeomorph.Defs
HomeomorphClass.inv_continuous : ∀ {F : Type u_5} {A : outParam (Type u_6)} {B : outParam (Type u_7)} {inst : TopologicalSpace A}
  {inst_1 : TopologicalSpace B} {h : EquivLike F A B} [self : HomeomorphClass F A B] (f : F),
  Continuous (EquivLike.inv f)
-- Mathlib.Util.TermReduce
/-- `reduceProj% t` apply `Expr.reduceProjStruct?` to all subexpressions of `t`.  -/
Mathlib.Util.TermReduce.reduceProjStx : Lean.ParserDescr
-- Init.Tactics
/-- The arguments to `simpa ... using! e` — like `simpaArgsRest`, but with a
mandatory `using!` clause selecting the permissive default-transparency close.  -/
Lean.Parser.Tactic.simpaUsingBangArgsRest : Lean.ParserDescr
-- Mathlib.MeasureTheory.Integral.CircleIntegral
circleIntegral.integral_radius_zero : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (f : ℂ → E) (c : ℂ),
  ∮ (z : ℂ) in C(c, 0), f z = 0
-- Init.Data.UInt.Lemmas
UInt32.toBitVec_ofNat' : ∀ (n : ℕ), (UInt32.ofNat n).toBitVec = BitVec.ofNat 32 n
-- Mathlib.Order.Bounds.Basic
isLeast_univ : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : OrderBot α], IsLeast Set.univ ⊥
-- Mathlib.RingTheory.Coalgebra.CoassocSimps
CoassocSimps.map_counit_comp_comul_left : ∀ {R : Type u_1} {M : Type u_3} {M' : Type u_6} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] [inst_5 : Coalgebra R M] (f : M →ₗ[R] M'),
  TensorProduct.map CoalgebraStruct.counit f ∘ₗ CoalgebraStruct.comul =
    TensorProduct.map LinearMap.id f ∘ₗ ↑(TensorProduct.lid R M).symm
-- Mathlib.Data.Set.NAry
Set.image_image2_distrib : ∀ {α : Type u_1} {α' : Type u_2} {β : Type u_3} {β' : Type u_4} {γ : Type u_5} {δ : Type u_7} {f : α → β → γ}
  {s : Set α} {t : Set β} {g : γ → δ} {f' : α' → β' → δ} {g₁ : α → α'} {g₂ : β → β'},
  (∀ (a : α) (b : β), g (f a b) = f' (g₁ a) (g₂ b)) → g '' Set.image2 f s t = Set.image2 f' (g₁ '' s) (g₂ '' t)
-- Mathlib.Algebra.Group.WithOne.Map
WithZero.map₂_bot_right : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (a : WithZero α), WithZero.map₂ f a 0 = 0
-- Mathlib.Algebra.Star.StarAlgHom
/-- Copy of a `NonUnitalStarAlgHom` with a new `toFun` equal to the old one. Useful
to fix definitional equalities.  -/
NonUnitalStarAlgHom.copy : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      [inst : Monoid R] →
        [inst_1 : NonUnitalNonAssocSemiring A] →
          [inst_2 : DistribMulAction R A] →
            [inst_3 : Star A] →
              [inst_4 : NonUnitalNonAssocSemiring B] →
                [inst_5 : DistribMulAction R B] →
                  [inst_6 : Star B] → (f : A →⋆ₙₐ[R] B) → (f' : A → B) → f' = ⇑f → A →⋆ₙₐ[R] B
-- Mathlib.CategoryTheory.SingleObj
MulEquiv.toSingleObjEquiv_inverse_obj : ∀ {M : Type u} {N : Type v} [inst : Monoid M] [inst_1 : Monoid N] (e : M ≃* N) (a : CategoryTheory.SingleObj N),
  e.toSingleObjEquiv.inverse.obj a = a
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mapLeftEq_hom_app_left : ∀ {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] (R : CategoryTheory.Functor B T)
  {L₁ L₂ : CategoryTheory.Functor A T} (l l' : L₁ ⟶ L₂) (h : l = l') (X : CategoryTheory.Comma L₂ R),
  ((CategoryTheory.Comma.mapLeftEq R l l' h).hom.app X).left = CategoryTheory.CategoryStruct.id X.left
-- Mathlib.Algebra.Group.Action.Faithful
/-- `instVAddOfAdd` is faithful when addition is right cancellative.  -/
instFaithfulVAddOfIsRightCancelAdd : ∀ (R : Type u_4) [inst : Add R] [IsRightCancelAdd R], FaithfulVAdd R R
-- Mathlib.Analysis.Normed.Lp.lpHolder
lp.mapCLM_apply_coe : ∀ {α : Type u_1} {𝕜 : Type u_2} {E : α → Type u_3} {F : α → Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : α) → NormedAddCommGroup (E i)] [inst_2 : (i : α) → NormedSpace 𝕜 (E i)]
  [inst_3 : (i : α) → NormedAddCommGroup (F i)] [inst_4 : (i : α) → NormedSpace 𝕜 (F i)] (p : ENNReal)
  [inst_5 : Fact (1 ≤ p)] (T : (i : α) → E i →L[𝕜] F i) {K : ℝ} (hK : 0 ≤ K) (hTK : ∀ (i : α), ‖T i‖ ≤ K)
  (x : ↥(lp E p)) (i : α), ↑((lp.mapCLM p T hK hTK) x) i = (T i) (↑x i)
-- Mathlib.CategoryTheory.Sites.Hypercover.One
/-- The trivial `1`-hypercover of `S` where a single component `S`.  -/
CategoryTheory.GrothendieckTopology.OneHypercover.trivial : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → (J : CategoryTheory.GrothendieckTopology C) → (S : C) → J.OneHypercover S
-- Mathlib.Algebra.Group.Ideal
AddSemigroupIdeal.closure_le : ∀ {M : Type u_1} [inst : Add M] {s : Set M} {I : AddSemigroupIdeal M}, AddSemigroupIdeal.closure s ≤ I ↔ s ⊆ ↑I
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.eLpNorm_one_le_of_le' : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ} {r : ℝ},
  MeasureTheory.Integrable f μ →
    0 ≤ ∫ (x : α), f x ∂μ → (∀ᵐ (ω : α) ∂μ, f ω ≤ r) → MeasureTheory.eLpNorm f 1 μ ≤ 2 * μ Set.univ * ENNReal.ofReal r
-- Mathlib.MeasureTheory.Measure.MutuallySingular
MeasureTheory.Measure.MutuallySingular.self_iff : ∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α), μ.MutuallySingular μ ↔ μ = 0
-- Mathlib.RingTheory.Ideal.Pointwise
Ideal.pointwise_central_scalar : ∀ {M : Type u_1} {R : Type u_3} [inst : Monoid M] [inst_1 : Semiring R] [inst_2 : MulSemiringAction M R]
  [inst_3 : MulSemiringAction Mᵐᵒᵖ R] [IsCentralScalar M R], IsCentralScalar M (Ideal R)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey?_diff_of_not_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  k ∉ t₂ → (t₁ \ t₂).getKey? k = t₁.getKey? k
-- Lean.Server.Rpc.Basic
Lean.Server.instInhabitedWithRpcRef.default : {α : Type u} → [Inhabited α] → Lean.Server.WithRpcRef α
-- Init.PropLemmas
exists_prop_decidable : {p : Prop} → (P : p → Prop) → [Decidable p] → [(h : p) → Decidable (P h)] → Decidable (∃ (h : p), P h)