mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Category.Profinite.Basic
/-- (Implementation) The bijection of homsets to establish the reflective adjunction of Profinite
spaces in compact Hausdorff spaces.
 -/
Profinite.toCompHausEquivalence : (X : CompHaus) → (Y : Profinite) → (X.toProfiniteObj ⟶ Y) ≃ (X ⟶ profiniteToCompHaus.obj Y)
-- Std.Data.DHashMap.Basic
/-- Checks if a mapping for the given key exists and returns the key-value pair if it does, otherwise `none`.
The key in the returned pair will be `BEq` to the input `a`.
 -/
Std.DHashMap.getEntry? : {α : Type u} → {β : α → Type v} → {x : BEq α} → {x_1 : Hashable α} → Std.DHashMap α β → α → Option ((a : α) × β a)
-- Mathlib.Data.PNat.Prime
PNat.Prime.one_lt : ∀ {p : ℕ+}, p.Prime → 1 < p
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
AlgebraicGeometry.quasiCompact_iff_forall_isAffineOpen : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y},
  AlgebraicGeometry.QuasiCompact f ↔
    ∀ (U : Y.Opens), AlgebraicGeometry.IsAffineOpen U → IsCompact ↑((TopologicalSpace.Opens.map f.base).obj U)
-- Mathlib.Tactic.Convert
/-- Close the goal `g` using `Eq.mp v e`,
where `v` is a metavariable asserting that the type of `g` and `e` are equal.
Then call `MVarId.congrN!` (also using local hypotheses and reflexivity) on `v`,
and return the resulting goals.

With `symm = true`, reverses the equality in `v`, and uses `Eq.mpr v e` instead.
With `depth = some n`, calls `MVarId.congrN! n` instead, with `n` as the max recursion depth.
 -/
Lean.MVarId.convert : Lean.Expr →
  Bool →
    optParam (Option ℕ) none →
      optParam Congr!.Config { } →
        optParam (List (Lean.TSyntax `rintroPat)) [] → Lean.MVarId → Lean.MetaM (List Lean.MVarId)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.tendsto_cos_pi_div_two : Filter.Tendsto Real.cos (nhdsWithin (Real.pi / 2) (Set.Iio (Real.pi / 2))) (nhdsWithin 0 (Set.Ioi 0))
-- Lean.Expr
Lean.Expr.brecOn.go : {motive : Lean.Expr → Sort u} →
  (t : Lean.Expr) → ((t : Lean.Expr) → Lean.Expr.below t → motive t) → motive t ×' Lean.Expr.below t
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.single_left_inj : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] {r : R} {m₁ m₂ : M},
  r ≠ 0 → (MonoidAlgebra.single m₁ r = MonoidAlgebra.single m₂ r ↔ m₁ = m₂)
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.support_zpow_le : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] (σ : Equiv.Perm α) (n : ℤ), (σ ^ n).support ⊆ σ.support
-- Mathlib.Algebra.Order.BigOperators.Group.List
List.sum_eq_zero_iff : ∀ {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : PartialOrder M] [IsOrderedAddMonoid M] [CanonicallyOrderedAdd M]
  {l : List M}, l.sum = 0 ↔ ∀ x ∈ l, x = 0
-- Mathlib.CategoryTheory.Countable
/-- The constructed category is indeed equivalent to `α`.  -/
CategoryTheory.CountableCategory.objAsTypeEquiv : (α : Type u) →
  [inst : CategoryTheory.Category.{v, u} α] →
    [inst_1 : CategoryTheory.CountableCategory α] → CategoryTheory.CountableCategory.ObjAsType α ≌ α
-- Mathlib.Analysis.SpecialFunctions.Exp
Real.coe_expOrderIso_apply : ∀ (x : ℝ), ↑(Real.expOrderIso x) = Real.exp x
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.infty_isScalarTower : ∀ {I : Type u_5} {B : I → Type u_6} [inst : (i : I) → NonUnitalNormedRing (B i)] {𝕜 : Type u_7} [inst_1 : NormedRing 𝕜]
  [inst_2 : (i : I) → Module 𝕜 (B i)] [inst_3 : ∀ (i : I), IsBoundedSMul 𝕜 (B i)]
  [∀ (i : I), IsScalarTower 𝕜 (B i) (B i)], IsScalarTower 𝕜 ↥(lp B ⊤) ↥(lp B ⊤)
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.hasOpNorm : {V₁ : Type u_2} →
  {V₂ : Type u_3} →
    [inst : SeminormedAddCommGroup V₁] → [inst_1 : SeminormedAddCommGroup V₂] → Norm (NormedAddGroupHom V₁ V₂)
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxi.Iterator.step_eq_step : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] {it : Std.Iter α}, it.step = ⟨Std.Rxi.Iterator.step it, ⋯⟩
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf
AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.commRingStructureSheafInTypeObj : {A : Type u_1} →
  {σ : Type u_2} →
    [inst : CommRing A] →
      [inst_1 : SetLike σ A] →
        [inst_2 : AddSubgroupClass σ A] →
          (𝒜 : ℕ → σ) →
            [inst_3 : GradedRing 𝒜] →
              (U : (TopologicalSpace.Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ) →
                CommRing ((AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.structureSheafInType 𝒜).obj.obj U)
-- Mathlib.GroupTheory.PushoutI
/-- All maps into the `PushoutI`, or amalgamated product of groups are injective,
provided all maps in the diagram are injective.

See also `base_injective`  -/
Monoid.PushoutI.of_injective : ∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [inst : (i : ι) → Group (G i)] [inst_1 : Group H]
  {φ : (i : ι) → H →* G i},
  (∀ (i : ι), Function.Injective ⇑(φ i)) → ∀ (i : ι), Function.Injective ⇑(Monoid.PushoutI.of i)
-- Mathlib.Combinatorics.SimpleGraph.Cayley
SimpleGraph.instDecidableRelAdjAddCayleyOfDecidableEqOfDecidablePredMemSet.eq_1 : ∀ {M : Type u_1} (s : Set M) [inst : AddGroup M] [inst_1 : DecidableEq M] [inst_2 : DecidablePred fun x => x ∈ s]
  (u v : M),
  SimpleGraph.instDecidableRelAdjAddCayleyOfDecidableEqOfDecidablePredMemSet s u v =
    decidable_of_iff (u ≠ v ∧ (-u + v ∈ s ∨ -v + u ∈ s)) ⋯
-- Mathlib.Analysis.Calculus.FDeriv.Mul
/-- Eta-expanded form of `HasFDerivWithinAt.mul'` -/
HasFDerivWithinAt.fun_mul' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {s : Set E} {𝔸 : Type u_5} [inst_3 : NormedRing 𝔸] [inst_4 : NormedAlgebra 𝕜 𝔸]
  {a b : E → 𝔸} {a' b' : E →L[𝕜] 𝔸},
  HasFDerivWithinAt a a' s x →
    HasFDerivWithinAt b b' s x → HasFDerivWithinAt (fun i => a i * b i) (a x • b' + MulOpposite.op (b x) • a') s x
-- Mathlib.CategoryTheory.Monoidal.Internal.Types.Grp
/-- Converting a group into a group object in `Type u`.  -/
GrpTypeEquivalenceGrp.inverse : CategoryTheory.Functor GrpCat (CategoryTheory.Grp (Type u))
-- Mathlib.LinearAlgebra.BilinearMap
/-- Restricting a bilinear map in both components  -/
LinearMap.domRestrict₁₂ : {R : Type u_1} →
  {R₂ : Type u_2} →
    {S : Type u_3} →
      {S₂ : Type u_4} →
        [inst : Semiring R] →
          [inst_1 : Semiring R₂] →
            [inst_2 : Semiring S] →
              [inst_3 : Semiring S₂] →
                {M : Type u_5} →
                  {N : Type u_7} →
                    {P : Type u_9} →
                      [inst_4 : AddCommMonoid M] →
                        [inst_5 : AddCommMonoid N] →
                          [inst_6 : AddCommMonoid P] →
                            [inst_7 : Module R M] →
                              [inst_8 : Module S N] →
                                [inst_9 : Module R₂ P] →
                                  [inst_10 : Module S₂ P] →
                                    [inst_11 : SMulCommClass S₂ R₂ P] →
                                      {ρ₁₂ : R →+* R₂} →
                                        {σ₁₂ : S →+* S₂} →
                                          (M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) →
                                            (p : Submodule R M) → (q : Submodule S N) → ↥p →ₛₗ[ρ₁₂] ↥q →ₛₗ[σ₁₂] P
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Iso.op_trans : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} (α : X ≅ Y) (β : Y ≅ Z),
  (α ≪≫ β).op = β.op ≪≫ α.op
-- Mathlib.Order.Closure
LowerAdjoint.closureOperator_apply : ∀ {α : Type u_1} {β : Type u_4} [inst : PartialOrder α] [inst_1 : Preorder β] {u : β → α} (l : LowerAdjoint u) (x : α),
  l.closureOperator x = u (l.toFun x)
-- Mathlib.LinearAlgebra.Matrix.PosDef
Matrix.posDef_conjTranspose_iff : ∀ {n : Type u_2} {R : Type u_3} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] {M : Matrix n n R},
  M.conjTranspose.PosDef ↔ M.PosDef
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.infinitePos_omega : Hyperreal.omega.InfinitePos
-- Mathlib.CategoryTheory.MorphismProperty.Limits
/-- **Alias** of `CategoryTheory.MorphismProperty.IsStableUnderBaseChange.of_isPullback`. -/
CategoryTheory.MorphismProperty.of_isPullback : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {P : CategoryTheory.MorphismProperty C}
  [self : P.IsStableUnderBaseChange] {X Y Y' S : C} {f : X ⟶ S} {g : Y ⟶ S} {f' : Y' ⟶ Y} {g' : Y' ⟶ X},
  CategoryTheory.IsPullback f' g' g f → P g → P g'
-- Mathlib.Combinatorics.Quiver.Path
/-- `Quiver.Path.toList` is a contravariant functor. The inversion comes from `Quiver.Path` and
`List` having different preferred directions for adding elements.  -/
Quiver.Path.toList_comp : ∀ {V : Type u} [inst : Quiver V] {a b : V} (p : Quiver.Path a b) {c : V} (q : Quiver.Path b c),
  (p.comp q).toList = q.toList ++ p.toList
-- Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells
/-- the top morphism of the pushout square  -/
HomotopicalAlgebra.AttachCells.g₁ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {α : Type t} →
      {A B : α → C} →
        {g : (a : α) → A a ⟶ B a} →
          {X₁ X₂ : C} → {f : X₁ ⟶ X₂} → (self : HomotopicalAlgebra.AttachCells g f) → self.cofan₁.pt ⟶ X₁
-- Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
integrable_inv_one_add_sq : MeasureTheory.Integrable (fun x => (1 + x ^ 2)⁻¹) MeasureTheory.volume
-- Init.Data.UInt.Bitwise
UInt8.or_not_self : ∀ {a : UInt8}, a ||| ~~~a = -1
-- Mathlib.RingTheory.Extension.Basic
Algebra.Extension.contangentEquiv_tmul : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {P : Algebra.Extension R S}
  (s : S) (x : ↥P.ker), P.cotangentEquiv (s ⊗ₜ[P.Ring] x) = s • Algebra.Extension.Cotangent.mk x
-- Mathlib.Order.Hom.WithTopBot
WithTop.subtypeOrderIso_symm_apply : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderTop α] [inst_2 : DecidablePred fun x => x = ⊤] {a : α}
  (h : a ≠ ⊤), WithTop.subtypeOrderIso.symm a = ↑⟨a, h⟩
-- Mathlib.LinearAlgebra.FreeModule.Basic
/-- **Alias** of `Module.Free.iff_of_equiv`. -/
Module.Free.iff_of_ringEquiv : ∀ {R : Type u_2} {R' : Type u_3} {M : Type u_4} {M' : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : Semiring R'] [inst_4 : AddCommMonoid M'] [inst_5 : Module R' M'] {σ : R →+* R'}
  {σ' : R' →+* R} [inst_6 : RingHomInvPair σ σ'] [inst_7 : RingHomInvPair σ' σ] (e₂ : M ≃ₛₗ[σ] M'),
  Module.Free R M ↔ Module.Free R' M'
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.ext_iff : ∀ {A : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} A} {B : Type u_2}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} B} {T : Type u_3} {inst_2 : CategoryTheory.Category.{v_3, u_3} T}
  {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {P : CategoryTheory.MorphismProperty T}
  {Q : CategoryTheory.MorphismProperty A} {W : CategoryTheory.MorphismProperty B}
  {x y : CategoryTheory.MorphismProperty.Comma L R P Q W}, x = y ↔ x.left = y.left ∧ x.right = y.right ∧ x.hom ≍ y.hom
-- Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
SchwartzMap.instLineDerivAdd : ∀ {E : Type u_5} {F : Type u_8} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace ℝ F]
  [inst_3 : NormedSpace ℝ E], LineDerivAdd E (SchwartzMap E F) (SchwartzMap E F)
-- Qq.ForLean.ToExpr
instToExprLevelMVarId_qq : Lean.ToExpr Lean.LevelMVarId
-- Mathlib.CategoryTheory.Limits.Shapes.SplitEqualizer
/-- `rightRetraction` splits `g`  -/
CategoryTheory.IsSplitEqualizer.bottom_rightRetraction_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {W : C} {ι : W ⟶ X}
  (self : CategoryTheory.IsSplitEqualizer f g ι) {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.comp self.rightRetraction h) = h
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubMulAction.copy_eq : ∀ {R : Type u} {M : Type v} [inst : SMul R M] (p : SubMulAction R M) (s : Set M) (hs : s = ↑p), p.copy s hs = p
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
SubMulAction.of_fixingSubgroupEmpty_mapScalars_surjective : ∀ {M : Type u_1} {α : Type u_2} [inst : Group M] [inst_1 : MulAction M α],
  Function.Surjective ⇑(fixingSubgroup M ∅).subtype
-- Init.Data.SInt.Lemmas
ISize.zero_le_ofNat_of_lt : ∀ {a : ℕ}, a < 2 ^ (System.Platform.numBits - 1) → 0 ≤ ISize.ofNat a
-- Mathlib.GroupTheory.Exponent
AddMonoid.exponent_eq_zero_addOrder_zero : ∀ {G : Type u} [inst : AddMonoid G] {g : G}, addOrderOf g = 0 → AddMonoid.exponent G = 0
-- Mathlib.Analysis.Convex.Basic
convex_Ici : ∀ {𝕜 : Type u_1} {β : Type u_4} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid β]
  [inst_3 : PartialOrder β] [IsOrderedAddMonoid β] [inst_5 : Module 𝕜 β] [PosSMulMono 𝕜 β] (r : β), Convex 𝕜 (Set.Ici r)
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.map_map : ∀ {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁]
  (f : R →+* S₁) [inst_2 : CommSemiring S₂] (g : S₁ →+* S₂) (p : MvPolynomial σ R),
  (MvPolynomial.map g) ((MvPolynomial.map f) p) = (MvPolynomial.map (g.comp f)) p
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurable_unit : ∀ {α : Type u_1} [inst : MeasurableSpace α] (f : Unit → α), Measurable f
-- Mathlib.Data.Finset.Basic
Finset.erase_eq : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Finset α) (a : α), s.erase a = s \ {a}
-- Mathlib.Order.ModularLattice
/-- **Alias** of `covBy_sup_of_inf_covBy_of_inf_covBy_left`. -/
CovBy.sup_of_inf_of_inf_left : ∀ {α : Type u_1} [inst : Lattice α] [IsWeakUpperModularLattice α] {a b : α}, a ⊓ b ⋖ a → a ⊓ b ⋖ b → a ⋖ a ⊔ b
-- Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
MeasureTheory.hasFiniteIntegral_zero : ∀ (α : Type u_1) {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) {ε : Type u_7} [inst : TopologicalSpace ε]
  [inst_1 : ESeminormedAddMonoid ε], MeasureTheory.HasFiniteIntegral 0 μ
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.IsCharTwoJEqZeroNF.mk : ∀ {R : Type u_1} [inst : CommRing R] {W : WeierstrassCurve R}, W.a₁ = 0 → W.a₂ = 0 → W.IsCharTwoJEqZeroNF
-- Lean.Meta.Sym.SymM
/-- Returns the internalized `Bool.false`.   -/
Lean.Meta.Sym.getBoolFalseExpr : Lean.Meta.Sym.SymM Lean.Expr
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.coe_mkₐ : ∀ {R : Type u_1} [inst : CommRing R] (f : Polynomial R), ⇑(AdjoinRoot.mkₐ f) = ⇑(AdjoinRoot.mk f)
-- Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject
CategoryTheory.Triangulated.TStructure.spectralObjectFunctor_obj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) [inst_6 : CategoryTheory.IsTriangulated C] (X : C),
  t.spectralObjectFunctor.obj X = t.spectralObject X
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.succ_aleph : ∀ (o : Ordinal.{u_1}), Order.succ (Cardinal.aleph o) = Cardinal.aleph (o + 1)
-- Mathlib.Geometry.Convex.Set
/-- A set `s` in a convex space is convex if all convex combinations of points in `s` lie themselves
in `s`.

When the scalars form a field, this is equivalent to the definition in terms of binary combinations.
See `IsConvexSet.of_convexCombPair_mem`.  -/
Convexity.IsConvexSet : (R : Type u_3) →
  {X : Type u_5} →
    [inst : Semiring R] →
      [inst_1 : PartialOrder R] → [inst_2 : IsStrictOrderedRing R] → [Convexity.ConvexSpace R X] → Set X → Prop
-- Std.Http.Data.Method
Std.Http.Method.copy.sizeOf_spec : sizeOf Std.Http.Method.copy = 1
-- Mathlib.Order.Interval.Set.UnorderedInterval
MonotoneOn.image_uIcc_subset : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : Lattice β] {f : α → β} {a b : α},
  MonotoneOn f (Set.uIcc a b) → f '' Set.uIcc a b ⊆ Set.uIcc (f a) (f b)
-- Mathlib.CategoryTheory.Join.Basic
CategoryTheory.Join.mkFunctorLeft_hom_app : ∀ {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 E)
  (G : CategoryTheory.Functor D E) (α : (CategoryTheory.Prod.fst C D).comp F ⟶ (CategoryTheory.Prod.snd C D).comp G)
  (X : C), (CategoryTheory.Join.mkFunctorLeft F G α).hom.app X = CategoryTheory.CategoryStruct.id (F.obj X)
-- Mathlib.GroupTheory.Nilpotent
/-- The nilpotency class of a nilpotent `G` is equal to the smallest `n` for which an ascending
central series reaches `G` in its `n`-th term.  -/
Subgroup.least_ascending_central_series_length_eq_nilpotencyClass : ∀ {G : Type u_1} [inst : Group G] [hG : Group.IsNilpotent G], Nat.find ⋯ = Group.nilpotencyClass G
-- Mathlib.MeasureTheory.Integral.CircleIntegral
/-- **Alias** of `CircleIntegrable.continuousOn_mul`.

---

If `g` is continuous on the circle `sphere c |R|` and `f` is circle integrable, then `g * f` is
circle integrable.
 -/
CircleIntegrable.mul_of_continuousOn : ∀ {c : ℂ} {R : ℝ} {𝕜 : Type u_3} [inst : NormedRing 𝕜] {f g : ℂ → 𝕜},
  CircleIntegrable f c R → ContinuousOn g (Metric.sphere c |R|) → CircleIntegrable (g * f) c R
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.smul_def : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {α : Type u_1}
  [inst_3 : SMul A α] {S : Subalgebra R A} (g : ↥S) (m : α), g • m = ↑g • m
-- Mathlib.RingTheory.Polynomial.IsIntegral
MvPolynomial.isIntegral_iff_isIntegral_coeff : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {σ : Type w}
  {f : MvPolynomial σ S}, IsIntegral (MvPolynomial σ R) f ↔ ∀ (n : σ →₀ ℕ), IsIntegral R (MvPolynomial.coeff n f)
-- Mathlib.CategoryTheory.Monad.Kleisli
CategoryTheory.Kleisli.of_mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {T : CategoryTheory.Monad C} (c : C), { of := c }.of = c
-- Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
/-- This is the affine target morphism property where the source is affine and
the induced map of rings on global sections satisfies `P`.  -/
AlgebraicGeometry.affineAnd : ({R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) →
  AlgebraicGeometry.AffineTargetMorphismProperty
-- ProofWidgets.Data.Html
ProofWidgets.instInhabitedHtml : Inhabited ProofWidgets.Html
-- Init.Data.Iterators.Basic
Std.Iterators.Finite.wf_of_id : ∀ {α β : Type w} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id], WellFounded Std.Iter.IsPlausibleSuccessorOf
-- Mathlib.Data.Finset.Defs
Finset.FinsetCoe.canLift : ∀ {α : Type u_1} (s : Finset α), CanLift α (↥s) Subtype.val fun a => a ∈ s
-- Init.Data.Option.Instances
Option.decidableExistsMem : {α : Type u_1} → {p : α → Prop} → [DecidablePred p] → (o : Option α) → Decidable (∃ a ∈ o, p a)
-- Lean.Meta.Sym.Simp.SimpM
Lean.Meta.Sym.Simp.Context.mk.inj : ∀ {config : Lean.Meta.Sym.Simp.Config} {initialLCtxSize dischargeDepth : ℕ} {config_1 : Lean.Meta.Sym.Simp.Config}
  {initialLCtxSize_1 dischargeDepth_1 : ℕ},
  { config := config, initialLCtxSize := initialLCtxSize, dischargeDepth := dischargeDepth } =
      { config := config_1, initialLCtxSize := initialLCtxSize_1, dischargeDepth := dischargeDepth_1 } →
    config = config_1 ∧ initialLCtxSize = initialLCtxSize_1 ∧ dischargeDepth = dischargeDepth_1
-- Std.Tactic.BVDecide.LRAT.Internal.Convert
_private.Std.Tactic.BVDecide.LRAT.Internal.Convert.0.Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.ofArray.folder.match_6.eq_2 : ∀ {n : ℕ} (motive : Option (Std.HashMap (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) Bool) → Sort u_1)
  (map : Std.HashMap (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) Bool) (h_1 : Unit → motive none)
  (h_2 : (map : Std.HashMap (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) Bool) → motive (some map)),
  (match some map with
    | none => h_1 ()
    | some map => h_2 map) =
    h_2 map
-- Mathlib.CategoryTheory.Bicategory.Coherence
/-- The discrete category on the paths includes into the category of 1-morphisms in the free
bicategory.
 -/
CategoryTheory.FreeBicategory.inclusionPath : {B : Type u} →
  [inst : Quiver B] →
    (a b : B) →
      CategoryTheory.Functor (CategoryTheory.Discrete (Quiver.Path a b)) (CategoryTheory.FreeBicategory.Hom a b)
-- Mathlib.Algebra.Ring.Defs
mul_boole : ∀ {α : Type u_1} [inst : MulZeroOneClass α] (P : Prop) [inst_1 : Decidable P] (a : α),
  (a * if P then 1 else 0) = if P then a else 0
-- Mathlib.Data.Set.Insert
Set.insert_subset : ∀ {α : Type u_1} {s t : Set α} {a : α}, a ∈ t → s ⊆ t → insert a s ⊆ t
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
/-- The type of functions from `α` to `β` equipped with the uniform structure and topology of
uniform convergence on some family `𝔖` of subsets of `α`. We denote it `α →ᵤ[𝔖] β`.  -/
UniformOnFun : (α : Type u_1) → Type u_2 → Set (Set α) → Type (max u_1 u_2)
-- Mathlib.Algebra.Polynomial.Degree.Operations
/-- `degree` as a monoid homomorphism between `R[X]` and `Multiplicative (WithBot ℕ)`.
This is useful to prove results about multiplication and degree.  -/
Polynomial.degreeMonoidHom : {R : Type u} → [inst : Semiring R] → [NoZeroDivisors R] → [Nontrivial R] → Polynomial R →* Multiplicative (WithBot ℕ)
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.sumPiLpEquivProdLpPiLp_apply_ofLp : ∀ {𝕜 : Type u_1} [inst : Semiring 𝕜] {ι : Type u_5} {κ : Type u_6} (p : ENNReal) (α : ι ⊕ κ → Type u_7)
  [inst_1 : Fintype ι] [inst_2 : Fintype κ] [inst_3 : Fact (1 ≤ p)]
  [inst_4 : (i : ι ⊕ κ) → SeminormedAddCommGroup (α i)] [inst_5 : (i : ι ⊕ κ) → Module 𝕜 (α i)]
  (x : WithLp p ((i : ι ⊕ κ) → α i)),
  ((PiLp.sumPiLpEquivProdLpPiLp p α) x).ofLp =
    (WithLp.toLp p fun i => x.ofLp (Sum.inl i), WithLp.toLp p fun i' => x.ofLp (Sum.inr i'))
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Cpop
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Cpop.0.Std.Tactic.BVDecide.BVExpr.bitblast.blastExtractAndExtendBit.match_1.eq_1 : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α)
  (motive : Std.Tactic.BVDecide.BVExpr.bitblast.ExtractAndExtendBitTarget aig w → Sort u_1) (start : ℕ)
  (x : aig.RefVec w) (h_1 : (start : ℕ) → (x : aig.RefVec w) → motive { start := start, x := x }),
  (match { start := start, x := x } with
    | { start := start, x := x } => h_1 start x) =
    h_1 start x
-- Mathlib.CategoryTheory.Bicategory.Modification.Lax
CategoryTheory.Lax.LaxTrans.Hom.of.injEq : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.LaxFunctor B C} {η θ : F ⟶ G} (as as_1 : CategoryTheory.Lax.LaxTrans.Modification η θ),
  ({ as := as } = { as := as_1 }) = (as = as_1)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.self_le_maxKeyD_insertIfNew! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF →
    ∀ {k : α} {v : β k} {fallback : α},
      (compare k ((Std.DTreeMap.Internal.Impl.insertIfNew! k v t).maxKeyD fallback)).isLE = true
-- Mathlib.Tactic.Positivity.Core
_private.Mathlib.Tactic.Positivity.Core.0.Mathlib.Meta.Positivity.OrderRel : Type
-- Mathlib.Analysis.Analytic.CPolynomialDef
/-- If a function `f` has a finite power series `p` on a ball and `g` is a continuous linear map,
then `g ∘ f` has the finite power series `g ∘ p` on the same ball.  -/
ContinuousLinearMap.comp_hasFiniteFPowerSeriesOnBall : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {x : E}
  {r : ENNReal} {n : ℕ} (g : F →L[𝕜] G),
  HasFiniteFPowerSeriesOnBall f p x n r → HasFiniteFPowerSeriesOnBall (⇑g ∘ f) (g.compFormalMultilinearSeries p) x n r
-- Mathlib.Combinatorics.SimpleGraph.Prod
/-- The embedding of `H` into `G □ H` given by `a`.  -/
SimpleGraph.boxProdRight : {α : Type u_1} → {β : Type u_2} → (G : SimpleGraph α) → (H : SimpleGraph β) → α → H ↪g G □ H
-- Init.Prelude
Char.mk : (val : UInt32) → val.isValidChar → Char