mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.MvPolynomial.Nilpotent
MvPolynomial.isUnit_iff_eq_C_of_isReduced : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommRing R] {P : MvPolynomial σ R} [IsReduced R],
  IsUnit P ↔ ∃ r, IsUnit r ∧ P = MvPolynomial.C r
-- Lean.Setup
Lean.instToJsonModuleSetup.toJson : Lean.ModuleSetup → Lean.Json
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.toList.eq_1 : ∀ {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n),
  f.toList =
    List.filterMap id f.clauses.toList ++
        List.map Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.unit f.rupUnits.toList ++
      List.map Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.unit f.ratUnits.toList
-- Mathlib.Topology.UniformSpace.Closeds
Filter.HasBasis.uniformity_nonemptyCompacts : ∀ {α : Type u_1} [inst : UniformSpace α] {ι : Sort u_4} {p : ι → Prop} {s : ι → Set (α × α)},
  (uniformity α).HasBasis p s →
    (uniformity (TopologicalSpace.NonemptyCompacts α)).HasBasis p fun i =>
      Prod.map SetLike.coe SetLike.coe ⁻¹' hausdorffEntourage (s i)
-- Mathlib.Order.ConditionallyCompleteLattice.Finset
sSup_ne_of_notMem : ∀ {α : Type u_5} [inst : CompleteLinearOrder α] {s : Set α}, s.Finite → ∀ {a : α}, a ≠ ⊥ → a ∉ s → sSup s ≠ a
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
/-- **Alias** of the reverse direction of `Subalgebra.toNonUnitalSubalgebra_le_toNonUnitalSubalgebra`. -/
Subalgebra.toNonUnitalSubalgebra_mono : ∀ {R : Type uR} {A : Type uA} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  {S T : Subalgebra R A}, S ≤ T → S.toNonUnitalSubalgebra ≤ T.toNonUnitalSubalgebra
-- Mathlib.Topology.JacobsonSpace
Topology.IsOpenEmbedding.preimage_closedPoints : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  Topology.IsOpenEmbedding f → ∀ [JacobsonSpace Y], f ⁻¹' closedPoints Y = closedPoints X
-- Mathlib.LinearAlgebra.Matrix.Kronecker
Matrix.diag.eq_1 : ∀ {n : Type u_3} {α : Type v} (A : Matrix n n α) (i : n), A.diag i = A i i
-- Mathlib.Topology.Algebra.Constructions.DomMulAct
DomAddAct.instRegularSpace : ∀ {M : Type u_1} [inst : TopologicalSpace M] [RegularSpace M], RegularSpace Mᵈᵃᵃ
-- Init.Data.BitVec.Lemmas
BitVec.toInt_ne : ∀ {n : ℕ} {x y : BitVec n}, x.toInt ≠ y.toInt ↔ x ≠ y
-- Mathlib.CategoryTheory.Limits.Types.Products
CategoryTheory.Limits.Types.binaryProductFunctor_map_app : ∀ {X₁ X₂ : Type u} (f : X₁ ⟶ X₂) (Y : Type u),
  (CategoryTheory.Limits.Types.binaryProductFunctor.map f).app Y =
    CategoryTheory.Limits.BinaryFan.IsLimit.lift (CategoryTheory.Limits.Types.binaryProductLimit X₂ Y)
      (CategoryTheory.CategoryStruct.comp (TypeCat.ofHom Prod.fst) f) (TypeCat.ofHom Prod.snd)
-- Mathlib.Topology.Category.TopCat.OpenNhds
TopologicalSpace.OpenNhds.instInhabited : {X : TopCat} → (x : ↑X) → Inhabited (TopologicalSpace.OpenNhds x)
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.comp_whiskerLeft_symm_assoc : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) {h h' : c ⟶ d} (η : h ⟶ h')
  {Z : a ⟶ d} (h_1 : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h') ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerLeft g η)) h_1 =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g h).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerLeft (CategoryTheory.CategoryStruct.comp f g) η)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g h').hom h_1))
-- Init.Data.List.Sort.Impl
_private.Init.Data.List.Sort.Impl.0.List.MergeSort.Internal.mergeTR.go.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → List α → List α → Sort u_2) (l₁ acc : List α)
  (h_1 : (l₂ acc : List α) → motive [] l₂ acc) (h_2 : (l₁ acc : List α) → motive l₁ [] acc)
  (h_3 : (x : α) → (xs : List α) → (y : α) → (ys acc : List α) → motive (x :: xs) (y :: ys) acc),
  (l₁ = [] → False) →
    (match l₁, [], acc with
      | [], l₂, acc => h_1 l₂ acc
      | l₁, [], acc => h_2 l₁ acc
      | x :: xs, y :: ys, acc => h_3 x xs y ys acc) =
      h_2 l₁ acc
-- Mathlib.Algebra.Algebra.Unitization
Unitization.instMulAction : {S : Type u_2} →
  {R : Type u_3} →
    {A : Type u_4} → [inst : Monoid S] → [MulAction S R] → [MulAction S A] → MulAction S (Unitization R A)
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.coroot_eq_coreflection_of_root_eq : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) {i j k : ι},
  P.root k = (P.reflection i) (P.root j) → P.coroot k = (P.coreflection i) (P.coroot j)
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.isColimitCoconeRightOpOfCone_desc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  (F : CategoryTheory.Functor Jᵒᵖ C) {c : CategoryTheory.Limits.Cone F} (hc : CategoryTheory.Limits.IsLimit c)
  (s : CategoryTheory.Limits.Cocone F.rightOp),
  (CategoryTheory.Limits.isColimitCoconeRightOpOfCone F hc).desc s =
    (hc.lift (CategoryTheory.Limits.coneOfCoconeRightOp s)).op
-- Mathlib.ModelTheory.Basic
/-- The type of constants in a given language.  -/
FirstOrder.Language.Constants : FirstOrder.Language → Type u
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
CStarAlgebra.nnnorm_le_natCast_iff_of_nonneg : ∀ {A : Type u_1} [inst : CStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A] (a : A) (n : ℕ),
  autoParam (0 ≤ a) CStarAlgebra.nnnorm_le_natCast_iff_of_nonneg._auto_1 → (‖a‖₊ ≤ ↑n ↔ a ≤ ↑n)
-- Mathlib.CategoryTheory.MorphismProperty.WeakFactorizationSystem
/-- Two classes of morphisms `W₁` and `W₂` in a category `C` form a weak
factorization system if `W₁` is exactly `W₂.llp`, `W₂` is exactly `W₁.rlp`,
and any morphism can be factored a `i ≫ p` with `W₁ i` and `W₂ p`.  -/
CategoryTheory.MorphismProperty.IsWeakFactorizationSystem : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.MorphismProperty C → CategoryTheory.MorphismProperty C → Prop
-- Mathlib.Logic.Godel.GodelBetaFunction
_private.Mathlib.Logic.Godel.GodelBetaFunction.0.Nat.coprimes.eq_1 : ∀ {m : ℕ} (a : Fin m → ℕ) (i : Fin m), Nat.coprimes✝ a i = (↑i + 1) * (Nat.supOfSeq✝ a).factorial + 1
-- Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
/-- Expand the definition of `proximity f a₀` in case where `a₀` is finite.  -/
ValueDistribution.proximity_coe : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {f : ℂ → E} {a₀ : E},
  ValueDistribution.proximity f ↑a₀ = Real.circleAverage (fun x => ‖f x - a₀‖⁻¹.posLog) 0
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.State.cache : Lean.Meta.Simp.State → Lean.Meta.Simp.Cache
-- Mathlib.Algebra.Order.CompleteField
/-- A field which is both linearly ordered and conditionally complete with respect to the order.
This axiomatizes the reals.  -/
ConditionallyCompleteLinearOrderedField : Type u_5 → Type u_5
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKey?_bind_getEntry? : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ((Std.Internal.List.minKey? l).bind fun k => Std.Internal.List.getEntry? k l) = Std.Internal.List.minEntry? l
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.ball_disjoint_closedBall : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x y : α} {δ ε : ℝ},
  δ + ε ≤ dist x y → Disjoint (Metric.ball x δ) (Metric.closedBall y ε)
-- Mathlib.Computability.Reduce
OneOneEquiv.to_many_one : ∀ {α : Type u_1} {β : Type u_2} [inst : Primcodable α] [inst_1 : Primcodable β] {p : α → Prop} {q : β → Prop},
  OneOneEquiv p q → ManyOneEquiv p q
-- Mathlib.Tactic.NormNum.Prime
_private.Mathlib.Tactic.NormNum.Prime.0.Mathlib.Meta.NormNum.evalNatPrime.core : (n nn : Q(ℕ)) →
  Q(Mathlib.Meta.NormNum.IsNat «$n» «$nn») → ℕ → Lean.MetaM (Mathlib.Meta.NormNum.Result q(Nat.Prime «$n»))
-- Mathlib.AlgebraicTopology.SimplicialSet.Path
SSet.Truncated.spine_vertex : ∀ {n : ℕ} (X : SSet.Truncated (n + 1)) (m : ℕ) (hₘ : m ≤ n + 1)
  (Δ : X.obj (Opposite.op { obj := { len := m }, property := hₘ })) (i : Fin (m + 1)),
  (X.spine m hₘ Δ).vertex i =
    (CategoryTheory.ConcreteCategory.hom
        (X.map (SimplexCategory.Truncated.Hom.tr ({ len := 0 }.const { len := m } i) ⋯ hₘ).op))
      Δ
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
ContinuousMap.UniqueHom.eq_of_continuous_of_map_id : ∀ {R : Type u_1} {A : Type u_2} {inst : CommSemiring R} {inst_1 : StarRing R} {inst_2 : MetricSpace R}
  {inst_3 : IsTopologicalSemiring R} {inst_4 : ContinuousStar R} {inst_5 : Ring A} {inst_6 : StarRing A}
  {inst_7 : TopologicalSpace A} {inst_8 : Algebra R A} [self : ContinuousMap.UniqueHom R A] (s : Set R)
  [CompactSpace ↑s] (φ ψ : C(↑s, R) →⋆ₐ[R] A),
  Continuous ⇑φ →
    Continuous ⇑ψ →
      φ (ContinuousMap.restrict s (ContinuousMap.id R)) = ψ (ContinuousMap.restrict s (ContinuousMap.id R)) → φ = ψ
-- Mathlib.Topology.Separation.CompletelyRegular
Topology.IsInducing.completelyRegularSpace : ∀ {X : Type u} [inst : TopologicalSpace X] {Y : Type v} [inst_1 : TopologicalSpace Y] [CompletelyRegularSpace Y]
  {f : X → Y}, Topology.IsInducing f → CompletelyRegularSpace X
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
/-- When `C` and `D` have chosen finite products and `F : C ⥤ D` is any functor,
`terminalComparison F` is the unique map `F (𝟙_ C) ⟶ 𝟙_ D`.  -/
CategoryTheory.CartesianMonoidalCategory.terminalComparison : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      {D : Type u₁} →
        [inst_2 : CategoryTheory.Category.{v₁, u₁} D] →
          [inst_3 : CategoryTheory.CartesianMonoidalCategory D] →
            (F : CategoryTheory.Functor C D) →
              F.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ⟶
                CategoryTheory.MonoidalCategoryStruct.tensorUnit D
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
MeasureTheory.lintegral_iUnion₀ : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [Countable β] {s : β → Set α},
  (∀ (i : β), MeasureTheory.NullMeasurableSet (s i) μ) →
    Pairwise (Function.onFun (MeasureTheory.AEDisjoint μ) s) →
      ∀ (f : α → ENNReal), ∫⁻ (a : α) in ⋃ i, s i, f a ∂μ = ∑' (i : β), ∫⁻ (a : α) in s i, f a ∂μ
-- Mathlib.Algebra.Polynomial.Degree.Lemmas
Polynomial.natDegree_sub : ∀ {R : Type u} [inst : Ring R] {p q : Polynomial R}, (p - q).natDegree = (q - p).natDegree
-- Lean.Elab.PreDefinition.Structural.Main
Lean.Elab.Structural.structuralRecursion : Lean.LocalContext × Lean.LocalInstances →
  Array Lean.Elab.PreDefinition → Array (Option Lean.Elab.TerminationMeasure) → Lean.Elab.TermElabM Unit
-- Mathlib.Tactic.CategoryTheory.Coherence.PureCoherence
Mathlib.Tactic.BicategoryLike.Normalize.Result.mk.inj : ∀ {normalizedHom : Mathlib.Tactic.BicategoryLike.NormalizedHom} {toNormalize : Mathlib.Tactic.BicategoryLike.Mor₂Iso}
  {normalizedHom_1 : Mathlib.Tactic.BicategoryLike.NormalizedHom}
  {toNormalize_1 : Mathlib.Tactic.BicategoryLike.Mor₂Iso},
  { normalizedHom := normalizedHom, toNormalize := toNormalize } =
      { normalizedHom := normalizedHom_1, toNormalize := toNormalize_1 } →
    normalizedHom = normalizedHom_1 ∧ toNormalize = toNormalize_1
-- Std.Data.DTreeMap.Internal.Queries
Std.DTreeMap.Internal.Impl.Const.minEntryD.eq_def : ∀ {α : Type u} {β : Type v} (x : Std.DTreeMap.Internal.Impl α fun x => β) (x_1 : α × β),
  Std.DTreeMap.Internal.Impl.Const.minEntryD x x_1 =
    match x, x_1 with
    | Std.DTreeMap.Internal.Impl.leaf, fallback => fallback
    | Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r, x => (k, v)
    | Std.DTreeMap.Internal.Impl.inner size k v (l@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r)) r_1,
      fallback => Std.DTreeMap.Internal.Impl.Const.minEntryD l fallback
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Minpoly
/-- The characteristic polynomial of the map `fun x => a * x` is the minimal polynomial of `a`.

In combination with `det_eq_sign_charpoly_coeff` or `trace_eq_neg_charpoly_coeff`
and a bit of rewriting, this will allow us to conclude the
field norm resp. trace of `x` is the product resp. sum of `x`'s conjugates.
 -/
charpoly_leftMulMatrix : ∀ {R : Type u} [inst : CommRing R] {S : Type u_1} [inst_1 : Ring S] [inst_2 : Algebra R S] (h : PowerBasis R S),
  ((Algebra.leftMulMatrix h.basis) h.gen).charpoly = minpoly R h.gen
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.instZero : {X : Type u_1} →
  {R : Type u_2} →
    [inst : Zero X] →
      [inst_1 : TopologicalSpace X] → [inst_2 : TopologicalSpace R] → [inst_3 : Zero R] → Zero (ContinuousMapZero X R)
-- Mathlib.Algebra.GroupWithZero.Invertible
/-- `a⁻¹` is an inverse of `a` if `a ≠ 0`  -/
invertibleOfNonzero : {α : Type u} → [inst : GroupWithZero α] → {a : α} → a ≠ 0 → Invertible a
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyMapData.instUnique : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        (φ : S₁ ⟶ S₂) →
          (h₁ : S₁.LeftHomologyData) →
            (h₂ : S₂.LeftHomologyData) → Unique (CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂)
-- Mathlib.RingTheory.Extension.Cotangent.BaseChange
Ideal.tensorCotangentEquiv.congr_simp : ∀ (R : Type u_1) {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (T : Type u_3)
  [inst_3 : CommRing T] [inst_4 : Algebra R T] (I : Ideal S) [inst_5 : Module.Flat R T],
  Ideal.tensorCotangentEquiv R T I = Ideal.tensorCotangentEquiv R T I
-- Lean.Data.Lsp.Extra
Lean.Lsp.RpcReleaseParams.sessionId : Lean.Lsp.RpcReleaseParams → UInt64
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Iso.unop_hom_inv_id_app_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] {F G : CategoryTheory.Functor C Dᵒᵖ} (e : F ≅ G) (X : C) {Z : D}
  (h : Opposite.unop (G.obj X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (e.hom.app X).unop (CategoryTheory.CategoryStruct.comp (e.inv.app X).unop h) = h
-- Mathlib.Algebra.Opposites
MulOpposite.op_unop : ∀ {α : Type u_1} (x : αᵐᵒᵖ), MulOpposite.op (MulOpposite.unop x) = x
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.fold_filterWithPostcondition : ∀ {α β δ : Type w} {n : Type w → Type w''} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] [inst_2 : Monad n]
  [LawfulMonad n] [inst_4 : Std.IteratorLoop α Id n] [Std.LawfulIteratorLoop α Id n]
  {f : β → Std.Iterators.PostconditionT n (ULift.{w, 0} Bool)} {g : δ → β → δ} {init : δ} {it : Std.Iter β},
  Std.IterM.fold g init (Std.Iter.filterWithPostcondition f it) =
    Std.Iter.foldM
      (fun d b => do
        let __do_lift ← (f b).run
        pure (if __do_lift.down = true then g d b else d))
      init it
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenNormalAddSubgroup.mk : {G : Type u} →
  [inst : AddGroup G] →
    [inst_1 : TopologicalSpace G] →
      (toOpenAddSubgroup : OpenAddSubgroup G) →
        autoParam (↑toOpenAddSubgroup).Normal OpenNormalAddSubgroup.isNormal'._autoParam → OpenNormalAddSubgroup G
-- Init.Data.List.Sort.Lemmas
List.MergeSort.Internal.splitInTwo_cons_cons_zipIdx_fst : ∀ {α : Type u_1} {a b : α} (i : ℕ) (l : List α),
  ↑(List.MergeSort.Internal.splitInTwo ⟨(a, i) :: (b, i + 1) :: l.zipIdx (i + 2), ⋯⟩).1 =
    (↑(List.MergeSort.Internal.splitInTwo ⟨a :: b :: l, ⋯⟩).1).zipIdx i
-- Mathlib.Analysis.Convex.Integral
/-- If `E` is a strictly convex normed space and `f : α → E` is a function such that `‖f x‖ ≤ C`
a.e., then either this function is a.e. equal to its average value, or the norm of its average value
is strictly less than `C`.  -/
ae_eq_const_or_norm_average_lt_of_norm_le_const : ∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [CompleteSpace E] {μ : MeasureTheory.Measure α} {f : α → E} {C : ℝ} [StrictConvexSpace ℝ E],
  (∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C) → f =ᵐ[μ] Function.const α (⨍ (x : α), f x ∂μ) ∨ ‖⨍ (x : α), f x ∂μ‖ < C
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
Convexity.StdSimplex.instConvexSpace : {R : Type u_1} →
  {I : Type u_6} →
    [inst : PartialOrder R] →
      [inst_1 : Semiring R] → [inst_2 : IsStrictOrderedRing R] → Convexity.ConvexSpace R (Convexity.StdSimplex R I)
-- Mathlib.Order.Atoms
IsAtomic.mk : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : OrderBot α], (∀ (b : α), b = ⊥ ∨ ∃ a, IsAtom a ∧ a ≤ b) → IsAtomic α
-- Mathlib.Analysis.Distribution.TestFunction
TestFunction.monoCLM_eq_of_scalars : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] {Ω₁ Ω₂ : TopologicalSpace.Opens E} {F : Type u_4} [inst_3 : NormedAddCommGroup F]
  [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace 𝕜 F] {n₁ n₂ : ℕ∞} [inst_6 : Algebra ℝ 𝕜]
  [inst_7 : IsScalarTower ℝ 𝕜 F] (𝕜' : Type u_6) [inst_8 : NontriviallyNormedField 𝕜'] [inst_9 : NormedSpace 𝕜' F]
  [inst_10 : Algebra ℝ 𝕜'] [inst_11 : IsScalarTower ℝ 𝕜' F], ⇑(TestFunction.monoCLM 𝕜) = ⇑(TestFunction.monoCLM 𝕜')
-- Mathlib.Data.Nat.Factorial.SuperFactorial
Nat.prod_range_factorial_succ : ∀ (n : ℕ), ∏ x ∈ Finset.range n, (x + 1).factorial = n.superFactorial
-- Init.Data.BitVec.Lemmas
/-- Iterated `setWidth` agrees with the second `setWidth`
except in the case the first `setWidth` is a non-trivial truncation,
and the second `setWidth` is a non-trivial extension.
 -/
BitVec.setWidth_setWidth : ∀ {u : ℕ} {x : BitVec u} {w v : ℕ}, ¬(v < u ∧ v < w) → BitVec.setWidth w (BitVec.setWidth v x) = BitVec.setWidth w x
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
PowerSeries.isWeierstrassFactorization_weierstrassDistinguished_weierstrassUnit : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : IsLocalRing A] [inst_2 : IsAdicComplete (IsLocalRing.maximalIdeal A) A]
  {g : PowerSeries A} (hg : (PowerSeries.map (IsLocalRing.residue A)) g ≠ 0),
  g.IsWeierstrassFactorization (g.weierstrassDistinguished hg) (g.weierstrassUnit hg)
-- Lean.Setup
Lean.ModuleHeader.mk.inj : ∀ {imports : Array Lean.Import} {isModule : Bool} {imports_1 : Array Lean.Import} {isModule_1 : Bool},
  { imports := imports, isModule := isModule } = { imports := imports_1, isModule := isModule_1 } →
    imports = imports_1 ∧ isModule = isModule_1
-- Mathlib.Data.WSeq.Relation
Stream'.WSeq.exists_of_liftRel_left : ∀ {α : Type u} {β : Type v} {R : α → β → Prop} {s : Stream'.WSeq α} {t : Stream'.WSeq β},
  Stream'.WSeq.LiftRel R s t → ∀ {a : α}, a ∈ s → ∃ b ∈ t, R a b
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
ContinuousMapZero.toContinuousMapHom_toNNReal : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : Zero X] (f : ContinuousMapZero X ℝ),
  (ContinuousMapZero.toContinuousMapHom f).toNNReal = ContinuousMapZero.toContinuousMapHom f.toNNReal
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.final_of_final_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D E) [hF : F.Final] [hFG : (F.comp G).Final], G.Final
-- Mathlib.Data.Set.Function
Set.bijOn_comm : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} {g : β → α},
  Set.InvOn f g t s → (Set.BijOn f s t ↔ Set.BijOn g t s)
-- Lean.Meta.Sym.Eta
_private.Lean.Meta.Sym.Eta.0.Lean.Meta.Sym.hasLooseBVarsInRange.go : Lean.Expr → ℕ → Bool
-- Mathlib.Combinatorics.Tiling.Tile
DiscreteTiling.PlacedTile.coe_mk_mk : ∀ {G : Type u_1} {X : Type u_2} {ιₚ : Type u_3} [inst : Group G] [inst_1 : MulAction G X]
  {ps : DiscreteTiling.Protoset G X ιₚ} (i : ιₚ) (g : G), ↑{ index := i, groupElts := ⟦g⟧ } = g • ↑(↑ps i)
-- Mathlib.Analysis.Analytic.ChangeOrigin
/-- Summing the series `p.changeOrigin x` at a point `y` gives back `p (x + y)`.  -/
FormalMultilinearSeries.changeOrigin_eval : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [CompleteSpace F]
  (p : FormalMultilinearSeries 𝕜 E F) {x y : E}, ↑‖x‖₊ + ↑‖y‖₊ < p.radius → (p.changeOrigin x).sum y = p.sum (x + y)
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.RightFreyd
CategoryTheory.Preadditive.RightFreyd.rightFunctor_map : ∀ (V : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} V] [inst_1 : CategoryTheory.Preadditive V]
  [inst_2 : CategoryTheory.Limits.HasZeroObject V] {X Y : V} (f : X ⟶ Y),
  (CategoryTheory.Preadditive.RightFreyd.rightFunctor V).map f = CategoryTheory.Arrow.homMk 0 f ⋯
-- Lean.Server.Completion.EligibleHeaderDecls
Lean.Server.Completion.EligibleDecl.info : Lean.Server.Completion.EligibleDecl → Lean.ConstantInfo
-- Mathlib.Data.Nat.Prime.Defs
Nat.not_prime_one : ¬Nat.Prime 1
-- Init.Data.String.Lemmas.Modify
String.map_eq_empty : ∀ {f : Char → Char} {s : String}, String.map f s = "" ↔ s = ""
-- Mathlib.Analysis.Complex.Circle
Circle.smul_def : ∀ {α : Type u_1} [inst : SMul ℂ α] (z : Circle) (a : α), z • a = ↑z • a
-- Mathlib.Data.List.Basic
Function.Bijective.list_map : ∀ {α : Type u} {β : Type v} {f : α → β}, Function.Bijective f → Function.Bijective (List.map f)
-- Qq.MatchImpl
Qq.Impl.PatVarDecl.userName : Qq.Impl.PatVarDecl → Lean.Name
-- Mathlib.Algebra.Ring.CompTypeclasses
/-- Class that expresses the fact that two ring homomorphisms are inverses of each other. This is
used to handle `symm` for semilinear equivalences.  -/
RingHomInvPair : {R₁ : Type u_1} →
  {R₂ : Type u_2} → [inst : Semiring R₁] → [inst_1 : Semiring R₂] → (R₁ →+* R₂) → outParam (R₂ →+* R₁) → Prop
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.dual_loops : ∀ {α : Type u_1} {M : Matroid α}, M✶.loops = M.coloops
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
CategoryTheory.Pseudofunctor.DescentData.hom_self : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} (self : F.DescentData f) ⦃Y : C⦄ (q : Y ⟶ S) ⦃i : ι⦄ (g : Y ⟶ X i)
  (x : CategoryTheory.CategoryStruct.comp g (f i) = q),
  self.hom q g g ⋯ ⋯ = CategoryTheory.CategoryStruct.id ((F.map g.op.toLoc).toFunctor.obj (self.obj i))
-- Std.Http.Data.Body.Full
/-- Creates a `Full` body from a `String`.
 -/
Std.Http.Body.Full.ofString : String → Std.Async.Async Std.Http.Body.Full
-- Mathlib.Algebra.Lie.UniversalEnveloping
UniversalEnvelopingAlgebra.lift_ι_apply : ∀ (R : Type u₁) {L : Type u₂} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {A : Type u₃}
  [inst_3 : Ring A] [inst_4 : Algebra R A] (f : L →ₗ⁅R⁆ A) (x : L),
  ((UniversalEnvelopingAlgebra.lift R) f) ((UniversalEnvelopingAlgebra.ι R) x) = f x
-- Mathlib.Tactic.NormNum.Pow
Mathlib.Meta.NormNum.isInt_zpow_pos : ∀ {α : Type u_1} [inst : DivisionRing α] {a : α} {b : ℤ} {nb ne : ℕ},
  Mathlib.Meta.NormNum.IsNat b nb →
    Mathlib.Meta.NormNum.IsInt (a ^ nb) (Int.negOfNat ne) → Mathlib.Meta.NormNum.IsInt (a ^ b) (Int.negOfNat ne)
-- Mathlib.Algebra.Order.Floor.Defs
/-- `Int.fract a` the fractional part of `a`, is `a` minus its floor.  -/
Int.fract : {α : Type u_2} → [inst : Ring α] → [inst_1 : LinearOrder α] → [FloorRing α] → α → α
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
/-- When `α` is a \*-additive monoid, `Matrix.star` is also a \*-additive monoid.  -/
Matrix.instStarAddMonoid : {n : Type u_3} → {α : Type v} → [inst : AddMonoid α] → [StarAddMonoid α] → StarAddMonoid (Matrix n n α)
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.ofReal_setIntegral_one_of_measure_ne_top : ∀ {X : Type u_5} {m : MeasurableSpace X} {μ : MeasureTheory.Measure X} {s : Set X},
  autoParam (μ s ≠ ⊤) MeasureTheory.ofReal_setIntegral_one_of_measure_ne_top._auto_1 →
    ENNReal.ofReal (∫ (x : X) in s, 1 ∂μ) = μ s