mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
continuousOn_cfcₙ_nnreal_setProd_nhdsSet : ∀ {A : Type u_2} [inst : NonUnitalNormedRing A] [inst_1 : StarRing A] [inst_2 : NormedSpace ℝ A]
  [inst_3 : IsScalarTower ℝ A A] [inst_4 : SMulCommClass ℝ A A] [ContinuousStar A]
  [inst_6 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_7 : PartialOrder A]
  [inst_8 : StarOrderedRing A] [inst_9 : NonnegSpectrumClass ℝ A] [T2Space A] [IsSemitopologicalRing A]
  [CompleteSpace A] {s : Set NNReal},
  ContinuousOn (fun fa => cfcₙ ((UniformOnFun.toFun {s}) fa.1) fa.2)
    ({f | ContinuousOn ((UniformOnFun.toFun {t | IsCompact t ∧ t ⊆ s}) f) s ∧ f 0 = 0} ×ˢ
      {a | 0 ≤ a ∧ s ∈ nhdsSet (quasispectrum NNReal a)})
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.instModule : {X : Type u_1} →
  {R : Type u_2} →
    [inst : Zero X] →
      [inst_1 : TopologicalSpace X] →
        [inst_2 : TopologicalSpace R] →
          [inst_3 : AddCommMonoid R] →
            [inst_4 : ContinuousAdd R] →
              {M : Type u_3} →
                [inst_5 : Semiring M] →
                  [inst_6 : Module M R] → [ContinuousConstSMul M R] → Module M (ContinuousMapZero X R)
-- Mathlib.RingTheory.SimpleModule.Isotypic
/-- The fully invariant submodules of a module form a complete sublattice in the lattice of
submodules.  -/
fullyInvariantSubmodule : (R : Type u_5) →
  (M : Type u_6) →
    [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → CompleteSublattice (Submodule R M)
-- Mathlib.RingTheory.Kaehler.Basic
/-- The universal derivation into `Ω[S⁄R]`.  -/
KaehlerDifferential.D : (R : Type u) →
  (S : Type v) → [inst : CommRing R] → [inst_1 : CommRing S] → [inst_2 : Algebra R S] → Derivation R S Ω[S⁄R]
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.map₂_coe : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {l : Filter α} (op : β → γ → δ) (f : α → β) (g : α → γ),
  Filter.Germ.map₂ op ↑f ↑g = ↑fun x => op (f x) (g x)
-- Init.Internal.Order.Basic
Lean.Order.instMonoBindReaderT : ∀ {m : Type u_1 → Type u_2} {ρ : Type u_1} [inst : Monad m] [inst_1 : (α : Type u_1) → Lean.Order.PartialOrder (m α)]
  [Lean.Order.MonoBind m], Lean.Order.MonoBind (ReaderT ρ m)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.diff_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp}, t₁.diff t₂ = t₁ \ t₂
-- Mathlib.RingTheory.DividedPowerAlgebra.Init
DividedPowerAlgebra.induction_on' : ∀ {R : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {P : DividedPowerAlgebra R M → Prop} (f : DividedPowerAlgebra R M),
  (∀ (a : R), P ↑(MvPolynomial.C a)) →
    (∀ (f g : DividedPowerAlgebra R M), P f → P g → P (f + g)) →
      (∀ (f : DividedPowerAlgebra R M) (n : ℕ) (m : M), P f → P (f * DividedPowerAlgebra.dp R n m)) → P f
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.MemLp.integrable_enorm_rpow : ∀ {α : Type u_1} {ε : Type u_5} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace ε]
  [inst_1 : ContinuousENorm ε] {f : α → ε} {p : ENNReal},
  MeasureTheory.MemLp f p μ → p ≠ 0 → p ≠ ⊤ → MeasureTheory.Integrable (fun x => ‖f x‖ₑ ^ p.toReal) μ
-- Mathlib.Order.Interval.Finset.Fin
Fin.finsetImage_castLE_Ioc : ∀ {n m : ℕ} (a b : Fin n) (h : n ≤ m),
  Finset.image (Fin.castLE h) (Finset.Ioc a b) = Finset.Ioc (Fin.castLE h a) (Fin.castLE h b)
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
/-- Given `U : FormalCoproduct C`, this is the simplicial object
in `FormalCoproduct C` which sends `⦋n⦌` to `U.power (Fin (n + 1))`.  -/
CategoryTheory.Limits.FormalCoproduct.cech : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Limits.HasFiniteProducts C] →
      CategoryTheory.Limits.FormalCoproduct C →
        CategoryTheory.SimplicialObject (CategoryTheory.Limits.FormalCoproduct C)
-- Mathlib.Order.Category.FinBddDistLat
FinBddDistLat.instInhabited : Inhabited FinBddDistLat
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokenType.macro.sizeOf_spec : sizeOf Lean.Lsp.SemanticTokenType.macro = 1
-- Mathlib.Topology.MetricSpace.Pseudo.Constructions
sphere_prod : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] (x : α × β) (r : ℝ),
  Metric.sphere x r = Metric.sphere x.1 r ×ˢ Metric.closedBall x.2 r ∪ Metric.closedBall x.1 r ×ˢ Metric.sphere x.2 r
-- Mathlib.Order.Defs.PartialOrder
Decidable.lt_or_eq_of_le' : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α} [DecidableLE α], b ≤ a → b < a ∨ a = b
-- Mathlib.Order.Hom.Basic
ULift.orderIso_symm_apply_down : ∀ {α : Type u} [inst : Preorder α] (down : α), ((RelIso.symm ULift.orderIso.{v, u}) down).down = down
-- Mathlib.Order.Interval.Set.Pi
Set.piecewise_mem_Icc' : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Preorder (α i)] {s : Set ι} [inst_1 : (j : ι) → Decidable (j ∈ s)]
  {f₁ f₂ g₁ g₂ : (i : ι) → α i}, f₁ ∈ Set.Icc g₁ g₂ → f₂ ∈ Set.Icc g₁ g₂ → s.piecewise f₁ f₂ ∈ Set.Icc g₁ g₂
-- Mathlib.CategoryTheory.Types.Basic
CategoryTheory.Functor.map_id_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (self : CategoryTheory.Functor C D) (X : C) {F : D → D → Type uF} {carrier : D → Type w}
  {instFunLike : (X Y : D) → FunLike (F X Y) (carrier X) (carrier Y)} [inst_2 : CategoryTheory.ConcreteCategory D F]
  (x : carrier (self.obj X)),
  (CategoryTheory.ConcreteCategory.hom (self.map (CategoryTheory.CategoryStruct.id X))) x = x
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.GrpObj.lift_comp_inv_left_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {A B : C} [inst_2 : CategoryTheory.GrpObj B] (f : A ⟶ B) {Z : C} (h : B ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.comp f CategoryTheory.GrpObj.inv) f)
      (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit A)
      (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one h)
-- Mathlib.Logic.Function.Basic
Function.Injective2.eq_iff : ∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β → γ},
  Function.Injective2 f → ∀ {a₁ a₂ : α} {b₁ b₂ : β}, f a₁ b₁ = f a₂ b₂ ↔ a₁ = a₂ ∧ b₁ = b₂
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- **Alias** of the forward direction of `sub_lt_iff_lt_add'`. -/
lt_add_of_sub_left_lt : ∀ {α : Type u} [inst : AddCommGroup α] [inst_1 : LT α] [AddLeftStrictMono α] {a b c : α}, a - b < c → a < b + c
-- Mathlib.CategoryTheory.Bicategory.Kan.IsKan
CategoryTheory.Bicategory.RightLift.IsKan.uniqueUpToIso_inv_left : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a}
  {s t : CategoryTheory.Bicategory.RightLift f g} (P : s.IsKan) (Q : t.IsKan), (P.uniqueUpToIso Q).inv.left = P.desc t
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
CategoryTheory.Bicategory.rightZigzagIso_inv : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {a b : B} {f : a ⟶ b} {g : b ⟶ a}
  (η : CategoryTheory.CategoryStruct.id a ≅ CategoryTheory.CategoryStruct.comp f g)
  (ε : CategoryTheory.CategoryStruct.comp g f ≅ CategoryTheory.CategoryStruct.id b),
  (CategoryTheory.Bicategory.rightZigzagIso η ε).inv = CategoryTheory.Bicategory.leftZigzag ε.inv η.inv
-- Batteries.Data.List.Basic
List.forall₂_cons : ∀ {α : Type u_1} {β : Type u_2} {R : α → β → Prop} {a : α} {b : β} {l₁ : List α} {l₂ : List β},
  List.Forall₂ R (a :: l₁) (b :: l₂) ↔ R a b ∧ List.Forall₂ R l₁ l₂
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.Zipper.val_run_step_toIterM_iter : ∀ {α : Type u} {β : α → Type v} {z : Std.DTreeMap.Internal.Zipper α β}, ↑z.iter.toIterM.step.run.inflate = z.step
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
/-- A set is semilinear if it is a finite union of linear sets.  -/
IsSemilinearSet : {M : Type u_1} → [AddCommMonoid M] → Set M → Prop
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue?_eq_getValueCast? : ∀ {α : Type u} [inst : BEq α] [inst_1 : LawfulBEq α] {β : Type v} {l : List ((_ : α) × β)} {a : α},
  Std.Internal.List.getValue? a l = Std.Internal.List.getValueCast? a l
-- Aesop.Options.Internal
Aesop.instInhabitedOptions'.default : Aesop.Options'
-- Mathlib.Data.ENNReal.Operations
ENNReal.le_sub_of_add_le_right : ∀ {a b c : ENNReal}, b ≠ ⊤ → a + b ≤ c → a ≤ c - b
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
AlgebraicGeometry.Scheme.RationalMap.compHom_toRationalMap : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X.PartialMap Y) (g : Y ⟶ Z),
  (f.compHom g).toRationalMap = f.toRationalMap.compHom g
-- Mathlib.Data.Finsupp.Option
Finsupp.embDomain_some_some : ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] (f : α →₀ M) (x : α),
  (Finsupp.embDomain Function.Embedding.some f) (some x) = f x
-- Lean.Meta.Tactic.Grind.EMatchTheorem
Lean.Meta.Grind.GenPatternInfo.xIdx : Lean.Meta.Grind.GenPatternInfo → ℕ
-- Mathlib.AlgebraicTopology.SimplicialSet.Nerve
PartOrd.nerveFunctor_map : ∀ {X Y : PartOrd} (f : X ⟶ Y), PartOrd.nerveFunctor.map f = CategoryTheory.nerveMap ⋯.functor
-- Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Groupoid
/-- Auxiliary definition for `CategoryTheory.Functor.closed`.
The counit for the adjunction `(tensorLeft F) ⊣ (ihom F)`.  -/
CategoryTheory.Functor.closedCounit : {D : Type u} →
  {C : Type u_1} →
    [inst : CategoryTheory.Groupoid D] →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          [inst_3 : CategoryTheory.MonoidalClosed C] →
            (F : CategoryTheory.Functor D C) →
              F.closedIhom.comp (CategoryTheory.MonoidalCategory.tensorLeft F) ⟶
                CategoryTheory.Functor.id (CategoryTheory.Functor D C)
-- Mathlib.Order.WellFoundedSet
Set.WellFoundedOn.mono : ∀ {α : Type u_2} {r r' : α → α → Prop} {s t : Set α}, t.WellFoundedOn r' → r ≤ r' → s ⊆ t → s.WellFoundedOn r
-- Mathlib.Algebra.Category.Grp.EquivalenceGroupAddGroup
GrpCat.toAddGrp_obj_coe : ∀ (X : GrpCat), ↑(GrpCat.toAddGrp.obj X) = Additive ↑X
-- Mathlib.NumberTheory.ModularForms.NormTrace
/-- The trace of a slash-invariant form, as a slash-invariant form.  -/
SlashInvariantForm.trace : {𝒢 : Subgroup (GL (Fin 2) ℝ)} →
  (ℋ : Subgroup (GL (Fin 2) ℝ)) →
    {F : Type u_1} →
      F →
        [inst : FunLike F UpperHalfPlane ℂ] →
          {k : ℤ} → [SlashInvariantFormClass F 𝒢 k] → [𝒢.IsFiniteRelIndex ℋ] → SlashInvariantForm ℋ k
-- Mathlib.RingTheory.Localization.FractionRing
FractionRing.field : (A : Type u_4) → [inst : CommRing A] → [IsDomain A] → Field (FractionRing A)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.PushoutObjObj.ofNatIso_inl : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)} {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} {X₂ Y₂ : C₂} {f₂ : X₂ ⟶ Y₂}
  (sq : F.PushoutObjObj f₁ f₂) {F' : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)} (e : F ≅ F'),
  (sq.ofNatIso e).inl = CategoryTheory.CategoryStruct.comp ((e.inv.app Y₁).app X₂) sq.inl
-- Mathlib.Order.Category.FinBddDistLat
FinBddDistLat.coe_id : ∀ {X : FinBddDistLat}, ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) = id
-- Mathlib.Analysis.Distribution.TestFunction
TestFunction.instAdd : {E : Type u_3} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : NormedSpace ℝ E] →
      {Ω : TopologicalSpace.Opens E} →
        {F : Type u_4} →
          [inst_2 : NormedAddCommGroup F] → [inst_3 : NormedSpace ℝ F] → {n : ℕ∞} → Add (TestFunction Ω F n)
-- Init.Data.UInt.Basic
/-- Non-strict inequality of 64-bit unsigned integers, defined as inequality of the corresponding
natural numbers. Usually accessed via the `≤` operator.
 -/
UInt64.le : UInt64 → UInt64 → Prop
-- Lean.Elab.Do.Basic
Lean.Elab.Do.DoElemCont.mk.injEq : ∀ (resultName : Lean.Name) (resultType : Lean.Expr) (k : Lean.Elab.Do.DoElabM Lean.Expr)
  (kind : Lean.Elab.Do.DoElemContKind) (resultName_1 : Lean.Name) (resultType_1 : Lean.Expr)
  (k_1 : Lean.Elab.Do.DoElabM Lean.Expr) (kind_1 : Lean.Elab.Do.DoElemContKind),
  ({ resultName := resultName, resultType := resultType, k := k, kind := kind } =
      { resultName := resultName_1, resultType := resultType_1, k := k_1, kind := kind_1 }) =
    (resultName = resultName_1 ∧ resultType = resultType_1 ∧ k = k_1 ∧ kind = kind_1)
-- Mathlib.Order.ModularLattice
/-- **Alias** of `inf_covBy_of_covBy_sup_right`. -/
CovBy.inf_of_sup_right : ∀ {α : Type u_1} [inst : Lattice α] [IsLowerModularLattice α] {a b : α}, b ⋖ a ⊔ b → a ⊓ b ⋖ a
-- Mathlib.RingTheory.DedekindDomain.Ideal.Basic
FractionalIdeal.instPosMulStrictMonoNonZeroDivisors : ∀ {A : Type u_2} (K : Type u_3) [inst : CommRing A] [inst_1 : Field K] [IsDedekindDomain A] [inst_3 : Algebra A K]
  [IsFractionRing A K], PosMulStrictMono (FractionalIdeal (nonZeroDivisors A) K)
-- Mathlib.Algebra.Field.Subfield.Basic
RingHom.coe_rangeRestrictField : ∀ {K : Type u} {L : Type v} [inst : DivisionRing K] [inst_1 : DivisionRing L] (f : K →+* L) (x : K),
  ↑(f.rangeRestrictField x) = f x
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKey_insertMany_empty_list_of_mem : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} [Std.TransOrd α] {l : List (α × β)} {k k' : α},
  compare k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬compare a.1 b.1 = Ordering.eq) l →
      k ∈ List.map Prod.fst l →
        ∀
          {h' :
            Std.DTreeMap.Internal.Impl.contains k'
                ↑(Std.DTreeMap.Internal.Impl.Const.insertMany Std.DTreeMap.Internal.Impl.empty l ⋯) =
              true},
          (↑(Std.DTreeMap.Internal.Impl.Const.insertMany Std.DTreeMap.Internal.Impl.empty l ⋯)).getKey k' h' = k
-- Mathlib.Combinatorics.SimpleGraph.Prod
SimpleGraph.Walk.ofBoxProdRight.eq_2 : ∀ {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {H : SimpleGraph β} [inst : DecidableEq α]
  [inst_1 : DecidableRel H.Adj] {x y : α × β} (v : α × β) (h : (G □ H).Adj x v) (w : (G □ H).Walk v y),
  (SimpleGraph.Walk.cons h w).ofBoxProdRight =
    ⋯.by_cases (fun hH => SimpleGraph.Walk.cons ⋯ w.ofBoxProdRight) fun hG => ⋯ ▸ w.ofBoxProdRight
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.abs_rpow_le_abs_rpow : ∀ (x y : ℝ), |x ^ y| ≤ |x| ^ y
-- Mathlib.Topology.MetricSpace.Basic
/-- If `f : β → α` sends any two distinct points to points at distance at least `ε > 0`, then
`f` is a uniform embedding with respect to the discrete uniformity on `β`.  -/
Metric.isUniformEmbedding_bot_of_pairwise_le_dist : ∀ {α : Type u} [inst : PseudoMetricSpace α] {β : Type u_2} {ε : ℝ},
  0 < ε → ∀ {f : β → α}, (Pairwise fun x y => ε ≤ dist (f x) (f y)) → IsUniformEmbedding f
-- Mathlib.Data.Finset.Powerset
Finset.image_injOn_powerset_of_injOn : ∀ {α : Type u_1} {s : Finset α} {β : Type u_2} [inst : DecidableEq β] {f : α → β},
  Set.InjOn f ↑s → Set.InjOn (fun x => Finset.image f x) ↑s.powerset
-- Mathlib.CategoryTheory.Limits.FullSubcategory
/-- The essential image of a functor is closed under the colimits it preserves.  -/
CategoryTheory.Limits.instIsClosedUnderColimitsOfShapeEssImageOfHasColimitsOfShapeOfPreservesColimitsOfShapeOfFullOfFaithful : ∀ {J : Type w} [inst : CategoryTheory.Category.{w', w} J] {C : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D)
  [CategoryTheory.Limits.HasColimitsOfShape J C] [CategoryTheory.Limits.PreservesColimitsOfShape J F] [F.Full]
  [F.Faithful], F.essImage.IsClosedUnderColimitsOfShape J
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Add
Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorBinaryRefVecBlastAdd : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α],
  Std.Sat.AIG.LawfulVecOperator α Std.Sat.AIG.BinaryRefVec fun {len} => Std.Tactic.BVDecide.BVExpr.bitblast.blastAdd
-- Mathlib.ModelTheory.Basic
Function.emptyHom_toFun : ∀ {M : Type w} {N : Type w'} [inst : FirstOrder.Language.empty.Structure M]
  [inst_1 : FirstOrder.Language.empty.Structure N] (f : M → N) (a : M), (Function.emptyHom f) a = f a
-- Mathlib.Analysis.Meromorphic.Basic
AnalyticAt.meromorphicAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜}, AnalyticAt 𝕜 f x → MeromorphicAt f x
-- Mathlib.Data.TypeVec
TypeVec.const_nil : ∀ {β : Type u_1} (x : β) (α : TypeVec.{u_2} 0), TypeVec.const x α = TypeVec.nilFun
-- Mathlib.FieldTheory.AbelRuffini
IsSolvableByRad.below.inv : ∀ {F : Type u_1} {E : Type u_2} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E]
  {motive : (a : E) → IsSolvableByRad F a → Prop} (α : E) (a : IsSolvableByRad F α),
  IsSolvableByRad.below a → motive α a → IsSolvableByRad.below ⋯
-- Mathlib.FieldTheory.PurelyInseparable.Basic
IsPurelyInseparable.minpoly_eq_X_sub_C_pow : ∀ (F : Type u) {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (q : ℕ) [ExpChar F q]
  [IsPurelyInseparable F E] (x : E),
  ∃ n, Polynomial.map (algebraMap F E) (minpoly F x) = (Polynomial.X - Polynomial.C x) ^ q ^ n
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
/-- The following diagram is a pullback
```
X --f--> Z
|        |
id       id
v        v
X --f--> Z
```
 -/
CategoryTheory.IsPushout.id_vert : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Z X : C} (f : X ⟶ Z),
  CategoryTheory.IsPushout f (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id Z) f
-- Init.MetaTypes
Lean.Meta.instInhabitedOccurrences : Inhabited Lean.Meta.Occurrences
-- Mathlib.MeasureTheory.Function.SimpleFuncDense
_private.Mathlib.MeasureTheory.Function.SimpleFuncDense.0.MeasureTheory.SimpleFunc.nearestPtInd.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (N : ℕ) (h_1 : Unit → motive 0) (h_2 : (N : ℕ) → motive N.succ),
  (match N.succ with
    | 0 => h_1 ()
    | N.succ => h_2 N) =
    h_2 N
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F : C ⥤ Dᵒᵖ` creates limits of shape `Jᵒᵖ`, then `F.leftOp : Cᵒᵖ ⥤ D` creates colimits
of shape `J`.  -/
CategoryTheory.Limits.createsColimitsOfShapeLeftOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (J : Type w) →
          [inst_2 : CategoryTheory.Category.{w', w} J] →
            (F : CategoryTheory.Functor C Dᵒᵖ) →
              [CategoryTheory.CreatesLimitsOfShape Jᵒᵖ F] → CategoryTheory.CreatesColimitsOfShape J F.leftOp
-- Mathlib.Order.Category.NonemptyFinLinOrd
NonemptyFinLinOrd.Iso.mk_hom : ∀ {α β : NonemptyFinLinOrd} (e : ↑α.toLinOrd ≃o ↑β.toLinOrd),
  (NonemptyFinLinOrd.Iso.mk e).hom = NonemptyFinLinOrd.ofHom ↑e
-- Mathlib.Data.Sign.Basic
SignType.univ_eq : Finset.univ = {0, -1, 1}
-- Init.Data.UInt.Basic
/-- The power operation, raising a word-sized unsigned integer to a natural number power,
wrapping around on overflow. Usually accessed via the `^` operator.

This function is currently *not* overridden at runtime with an efficient implementation,
and should be used with caution. See https://github.com/leanprover/lean4/issues/7887.
 -/
USize.pow : USize → ℕ → USize
-- Mathlib.LinearAlgebra.Matrix.Circulant
Matrix.circulant_zero : ∀ (α : Type u_5) (n : Type u_6) [inst : Zero α] [inst_1 : Sub n], Matrix.circulant 0 = 0
-- Mathlib.Logic.Encodable.Basic
ULower.up_down : ∀ {α : Type u_1} [inst : Encodable α] {a : α}, (ULower.down a).up = a
-- Mathlib.Algebra.Order.Interval.Finset.SuccPred
Finset.Ioo_add_one_right_eq_Ioc_of_not_isMax : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : LocallyFiniteOrder α] [inst_3 : Add α]
  [SuccAddOrder α] {b : α}, ¬IsMax b → ∀ (a : α), Finset.Ioo a (b + 1) = Finset.Ioc a b
-- Mathlib.CategoryTheory.Subfunctor.Basic
/-- If `G` is a subfunctor of `F` and `i : U ⟶ V`, then for each `G`-sections on `U` `x`,
`F i x` is in `F(V)`.  -/
CategoryTheory.Subfunctor.map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)}
  (self : CategoryTheory.Subfunctor F) {U V : C} (i : U ⟶ V),
  self.obj U ⊆ ⇑(CategoryTheory.ConcreteCategory.hom (F.map i)) ⁻¹' self.obj V
-- Mathlib.Algebra.Algebra.Operations
/-- R-submodules of the R-algebra A are a module over `Set A`.  -/
Submodule.moduleSet : (R : Type u) →
  [inst : CommSemiring R] →
    (A : Type v) → [inst_1 : CommSemiring A] → [inst_2 : Algebra R A] → Module (SetSemiring A) (Submodule R A)
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
/-- The error bound for trapezoidal integration in the slightly weaker, but very common, case where
`f` is `C^2`.  -/
trapezoidal_error_le_of_c2 : ∀ {f : ℝ → ℝ} {a b : ℝ},
  ContDiffOn ℝ 2 f (Set.uIcc a b) →
    ∀ {ζ : ℝ},
      (∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.uIcc a b) x| ≤ ζ) →
        ∀ {N : ℕ}, 0 < N → |trapezoidal_error f N a b| ≤ |b - a| ^ 3 * ζ / (12 * ↑N ^ 2)
-- Mathlib.Order.Filter.AtTopBot.Monoid
Filter.Tendsto.atBot_of_add_const_le : ∀ {α : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] [inst_1 : Preorder M] [IsOrderedCancelAddMonoid M]
  {l : Filter α} {f g : α → M},
  (∃ C, ∀ (x : α), C ≤ g x) → Filter.Tendsto (fun x => f x + g x) l Filter.atBot → Filter.Tendsto f l Filter.atBot
-- Mathlib.LinearAlgebra.Matrix.Rank
Matrix.ker_mulVecLin_conjTranspose_mul_self : ∀ {m : Type um} {n : Type un} {R : Type uR} [inst : Fintype n] [inst_1 : Fintype m] [inst_2 : Field R]
  [inst_3 : PartialOrder R] [inst_4 : StarRing R] [StarOrderedRing R] (A : Matrix m n R),
  (A.conjTranspose * A).mulVecLin.ker = A.mulVecLin.ker
-- Lean.ReducibilityAttrs
/-- Reducibility status for a definition. Controls when `isDefEq` and `whnf` are allowed to unfold it.
See `TransparencyMode` for the full design rationale.

- **`reducible`**: Unfolded at `TransparencyMode.reducible` or above. Reducible definitions still
  appear in user-facing terms, but are eagerly unfolded when indexing terms into discrimination
  trees (`simp`, type class resolution) and in `grind`. Think of it as `[inline]` for indexing.
  Suitable for abbreviations and definitions that should be transparent to proof automation.
- **`instanceReducible`**: Unfolded at `TransparencyMode.instances` or above. Auto-applied by the
  `instance` command and to subobject projections of class parents. The attribute
  `[instance_reducible]` marks a definition with this status; users typically do not need to
  apply it manually.
- **`implicitReducible`**: Unfolded at `TransparencyMode.implicit` or above (strictly above
  `.instances`). Used for definitions that should unfold when checking implicit and
  instance-implicit arguments for definitional equality, including for resolving instance diamonds,
  but must stay opaque to type class *search*.
  The attribute `[implicit_reducible]` marks a definition with this status.
  (Note: core arithmetic such as `Nat.add` and `Array.size` is deliberately `instanceReducible`,
  not `implicitReducible`, because type class synthesis depends on it unfolding.)
- **`semireducible`**: The default. Unfolded at `TransparencyMode.default` or above. Used for
  ordinary definitions. Suitable for user-written code where `isDefEq` should try hard during
  type checking, but not during speculative proof automation.
- **`irreducible`**: Only unfolded at `TransparencyMode.all`. The definition body is effectively
  hidden from `isDefEq` in normal usage.
 -/
Lean.ReducibilityStatus : Type
-- Mathlib.Analysis.InnerProductSpace.Orthonormal
LinearMap.coe_isometryOfOrthonormal : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_4} {E' : Type u_7} [inst_3 : SeminormedAddCommGroup E'] [inst_4 : InnerProductSpace 𝕜 E'] (f : E →ₗ[𝕜] E')
  {v : Module.Basis ι 𝕜 E} (hv : Orthonormal 𝕜 ⇑v) (hf : Orthonormal 𝕜 (⇑f ∘ ⇑v)), ⇑(f.isometryOfOrthonormal hv hf) = ⇑f
-- Lean.PrettyPrinter.Delaborator.Builtins
Lean.PrettyPrinter.Delaborator.delabPProdMkCore : Lean.Name → Lean.PrettyPrinter.Delaborator.Delab