mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Elab.Tactic.Conv.Basic
/-- Annotate `e` with the LHS annotation. The delaborator displays
expressions of the form `lhs = rhs` as `lhs` when they have this annotation.
This is used to implement the infoview for the `conv` mode.
 -/
Lean.Elab.Tactic.Conv.mkLHSGoal : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.leftHomologyMap_op : ∀ {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₂) [inst_2 : S₁.HasLeftHomology] [inst_3 : S₂.HasLeftHomology],
  (CategoryTheory.ShortComplex.leftHomologyMap φ).op =
    CategoryTheory.CategoryStruct.comp S₂.rightHomologyOpIso.inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.ShortComplex.rightHomologyMap (CategoryTheory.ShortComplex.opMap φ)) S₁.rightHomologyOpIso.hom)
-- Lean.Meta.Tactic.Backtrack
Lean.Meta.Tactic.Backtrack.BacktrackConfig.mk.inj : ∀ {maxDepth : ℕ} {proc : List Lean.MVarId → List Lean.MVarId → Lean.MetaM (Option (List Lean.MVarId))}
  {suspend : Lean.MVarId → Lean.MetaM Bool} {discharge : Lean.MVarId → Lean.MetaM (Option (List Lean.MVarId))}
  {commitIndependentGoals : Bool} {maxDepth_1 : ℕ}
  {proc_1 : List Lean.MVarId → List Lean.MVarId → Lean.MetaM (Option (List Lean.MVarId))}
  {suspend_1 : Lean.MVarId → Lean.MetaM Bool} {discharge_1 : Lean.MVarId → Lean.MetaM (Option (List Lean.MVarId))}
  {commitIndependentGoals_1 : Bool},
  { maxDepth := maxDepth, proc := proc, suspend := suspend, discharge := discharge,
        commitIndependentGoals := commitIndependentGoals } =
      { maxDepth := maxDepth_1, proc := proc_1, suspend := suspend_1, discharge := discharge_1,
        commitIndependentGoals := commitIndependentGoals_1 } →
    maxDepth = maxDepth_1 ∧
      proc = proc_1 ∧ suspend = suspend_1 ∧ discharge = discharge_1 ∧ commitIndependentGoals = commitIndependentGoals_1
-- Mathlib.CategoryTheory.Shift.SingleFunctors
/-- a family of natural transformations `F.functor a ⟶ G.functor a`  -/
CategoryTheory.SingleFunctors.Hom.hom : {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] →
        {A : Type u_5} →
          [inst_2 : AddMonoid A] →
            [inst_3 : CategoryTheory.HasShift D A] →
              {F G : CategoryTheory.SingleFunctors C D A} → F.Hom G → (a : A) → F.functor a ⟶ G.functor a
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.MonoidalOpposite.unmopFunctor_η : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C],
  CategoryTheory.Functor.OplaxMonoidal.η (CategoryTheory.unmopFunctor C) =
    CategoryTheory.CategoryStruct.id
      ((CategoryTheory.unmopFunctor C).obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit Cᴹᵒᵖ))
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.smul_mem_trW_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (P : CategoryTheory.ObjectProperty C) {X Y : C} (f : X ⟶ Y) (n : ℤˣ), P.trW (n • f) ↔ P.trW f
-- Mathlib.Order.RelClasses
instReflLe : ∀ {α : Type u} [inst : Preorder α], Std.Refl fun x1 x2 => x1 ≤ x2
-- Lean.Widget.Types
/-- Hash of the JS source of the widget module.  -/
Lean.Widget.WidgetInstance.javascriptHash : Lean.Widget.WidgetInstance → UInt64
-- Mathlib.Order.ModularLattice
/-- The diamond isomorphism between the open intervals `(a ⊓ b, b)` and `(a, a ⊔ b)`.  -/
infIooOrderIsoIooSup' : {α : Type u_1} → [inst : Lattice α] → [IsModularLattice α] → (a b : α) → ↑(Set.Ioo (a ⊓ b) b) ≃o ↑(Set.Ioo a (a ⊔ b))
-- Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
isIntegrallyClosed_of_isLocalization : ∀ {R : Type u_1} (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [IsIntegrallyClosed R]
  [IsDomain R], ∀ M ≤ nonZeroDivisors R, ∀ [IsLocalization M S], IsIntegrallyClosed S
-- Mathlib.RingTheory.Polynomial.Basic
MvPolynomial.isNoetherianRing_fin : ∀ {R : Type u} [inst : CommRing R] [IsNoetherianRing R] {n : ℕ}, IsNoetherianRing (MvPolynomial (Fin n) R)
-- Mathlib.Analysis.RCLike.Inner
RCLike.wInner_one_const_right : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : Fintype ι] [inst_1 : RCLike 𝕜] (f : ι → 𝕜) (a : 𝕜),
  ⟪f, Function.const ι a⟫_[𝕜] = a * ∑ i, (starRingEnd 𝕜) (f i)
-- Mathlib.Topology.Category.TopPair
/-- Given a `Homotopy f₀ f₁`, we can define a `Homotopy f₁ f₀` by `TopCat.Homotopy.symm` on
the first and second components.
 -/
TopPair.Homotopy.symm : {X Y : TopPair} → {f₀ f₁ : X ⟶ Y} → TopPair.Homotopy f₀ f₁ → TopPair.Homotopy f₁ f₀
-- Mathlib.Topology.Homotopy.HomotopyGroup
LoopSpace.inhabited : (X : Type u_2) → [inst : TopologicalSpace X] → (x : X) → Inhabited (Path x x)
-- Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
GradedTensorProduct.auxEquiv_one : ∀ {R : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring ι] [inst_1 : DecidableEq ι]
  [inst_2 : CommRing R] [inst_3 : Ring A] [inst_4 : Ring B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  (𝒜 : ι → Submodule R A) (ℬ : ι → Submodule R B) [inst_7 : GradedAlgebra 𝒜] [inst_8 : GradedAlgebra ℬ],
  (GradedTensorProduct.auxEquiv R 𝒜 ℬ) 1 = 1
-- Batteries.Recycling.RBTree.Basic
/-- `O(n)`. Convert the stream to a list in ascending order.  -/
RBTree.RBNode.Stream.toList : {α : Type u_1} → RBTree.RBNode.Stream α → List α
-- Mathlib.Algebra.Category.CommBialgCat
/-- Commutative bialgebras over a commutative ring `R` are the same thing as comonoid
`R`-algebras.  -/
commBialgCatEquivComonCommAlgCat : (R : Type u) → [inst : CommRing R] → CommBialgCat R ≌ (CategoryTheory.Mon (CommAlgCat R)ᵒᵖ)ᵒᵖ
-- Mathlib.FieldTheory.IsAlgClosed.Basic
IsAlgClosed.nonempty_algEquiv_or_of_finrank_eq_two : ∀ {F : Type u_1} {F' : Type u_2} (E : Type u_3) [inst : Field F] [inst_1 : Field F'] [inst_2 : Field E]
  [inst_3 : Algebra F F'] [inst_4 : Algebra F E] [Algebra.IsAlgebraic F E] [IsAlgClosed F'],
  Module.finrank F F' = 2 → Nonempty (E ≃ₐ[F] F) ∨ Nonempty (E ≃ₐ[F] F')
-- Batteries.Lean.EStateM
EStateM.ext_iff : ∀ {ε σ α : Type u_1} {x y : EStateM ε σ α}, x = y ↔ ∀ (s : σ), x.run s = y.run s
-- Mathlib.LinearAlgebra.BilinearForm.Properties
LinearMap.BilinForm.dualBasis_flip_dualBasis : ∀ {V : Type u_5} {K : Type u_6} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {ι : Type u_9}
  [inst_3 : DecidableEq ι] [inst_4 : Finite ι] {B : LinearMap.BilinForm K V} (hB : B.Nondegenerate)
  (b : Module.Basis ι K V), B.flip.dualBasis ⋯ (B.dualBasis hB b) = b
-- Mathlib.GroupTheory.Congruence.Hom
/-- The definition of the additive congruence relation defined by an
`AddMonoid` homomorphism's kernel.  -/
AddCon.ker_rel : ∀ {M : Type u_1} {N : Type u_2} {F : Type u_4} [inst : Add M] [inst_1 : Add N] [inst_2 : FunLike F M N]
  [inst_3 : AddHomClass F M N] (f : F) {x y : M}, (AddCon.ker f) x y ↔ f x = f y
-- Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
/-- In light of the fact that `MonicDegreeEq · n` is representable by `R[X₁,...,Xₙ]`,
this is the map `R[X₁,...,Xₘ₊ₖ] → R[X₁,...,Xₘ] ⊗ R[X₁,...,Xₖ]` corresponding to the multiplication
`MonicDegreeEq · m × MonicDegreeEq · k → MonicDegreeEq · (m + k)`.  -/
MvPolynomial.universalFactorizationMap : (R : Type u_1) →
  [inst : CommRing R] →
    (n m k : ℕ) →
      n = m + k → MvPolynomial (Fin n) R →ₐ[R] TensorProduct R (MvPolynomial (Fin m) R) (MvPolynomial (Fin k) R)
-- Mathlib.Geometry.Manifold.IsManifold.Basic
IsManifold.instOfNatWithTopENat_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] [IsManifold I 2 M], IsManifold I 1 M
-- Mathlib.Analysis.Complex.Exponential
Real.expNear_zero : ∀ (x r : ℝ), Real.expNear 0 x r = r
-- Init.Data.BitVec.Lemmas
BitVec.zero_and : ∀ {w : ℕ} {x : BitVec w}, 0#w &&& x = 0#w
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.aleph0_lt_aleph : ∀ {o : Ordinal.{u_1}}, Cardinal.aleph0 < Cardinal.aleph o ↔ 0 < o
-- Mathlib.Dynamics.Ergodic.Conservative
/-- If `f` is a conservative map and `s` is a measurable set of nonzero measure, then
for infinitely many values of `m` a positive measure of points `x ∈ s` returns back to `s`
after `m` iterations of `f`.  -/
MeasureTheory.Conservative.frequently_measure_inter_ne_zero : ∀ {α : Type u_1} [inst : MeasurableSpace α] {f : α → α} {s : Set α} {μ : MeasureTheory.Measure α},
  MeasureTheory.Conservative f μ →
    MeasureTheory.NullMeasurableSet s μ → μ s ≠ 0 → ∃ᶠ (m : ℕ) in Filter.atTop, μ (s ∩ f^[m] ⁻¹' s) ≠ 0
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
/-- `f : α → ℝ` and `ENNReal.ofReal ∘ f : α → ℝ≥0∞` have the same `eLpNorm`.
Usually, you should not use this lemma (but use enorms everywhere.)  -/
MeasureTheory.eLpNorm_ofReal : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} (f : α → ℝ),
  (∀ᵐ (x : α) ∂μ, 0 ≤ f x) → MeasureTheory.eLpNorm (ENNReal.ofReal ∘ f) p μ = MeasureTheory.eLpNorm f p μ
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.BinaryCofan.IsColimit.desc'_coe : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y : C} {s : CategoryTheory.Limits.BinaryCofan X Y}
  (h : CategoryTheory.Limits.IsColimit s) (f : X ⟶ W) (g : Y ⟶ W),
  ↑(CategoryTheory.Limits.BinaryCofan.IsColimit.desc' h f g) = h.desc (CategoryTheory.Limits.BinaryCofan.mk f g)
-- Std.Http.Data.Response
/-- Creates a new HTTP Response builder with the 400 status code.
 -/
Std.Http.Response.badRequest : Std.Http.Response.Builder
-- Mathlib.Order.RelIso.Basic
RelIso.emptySumLex_symm_apply : ∀ {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) [inst : IsEmpty α] (a : β),
  (RelIso.emptySumLex r s).symm a = Sum.inr a
-- Mathlib.Data.Finsupp.Basic
Finsupp.snd_sumFinsuppEquivProdFinsupp : ∀ {α : Type u_12} {β : Type u_13} {γ : Type u_14} [inst : Zero γ] (f : α ⊕ β →₀ γ) (y : β),
  (Finsupp.sumFinsuppEquivProdFinsupp f).2 y = f (Sum.inr y)
-- Mathlib.Topology.ContinuousMap.Basic
/-- Abbreviation for product of continuous maps, which is continuous  -/
ContinuousMap.pi : {I : Type u_5} →
  {A : Type u_6} →
    {X : I → Type u_7} →
      [inst : TopologicalSpace A] →
        [inst_1 : (i : I) → TopologicalSpace (X i)] → ((i : I) → C(A, X i)) → C(A, (i : I) → X i)
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField
AlgebraicGeometry.LocallyRingedSpace.residue_comp_residueFieldMap_eq_stalkMap_comp_residue : ∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Y) (x : ↑X.toTopCat),
  CategoryTheory.CategoryStruct.comp (Y.residue ((CategoryTheory.ConcreteCategory.hom f.base) x))
      (AlgebraicGeometry.LocallyRingedSpace.residueFieldMap f x) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap f x) (X.residue x)
-- Mathlib.Data.Finset.Functor
Finset.seq_def : ∀ {α β : Type u} [inst : (P : Prop) → Decidable P] (s : Finset α) (t : Finset (α → β)),
  t <*> s = t.sup fun f => Finset.image f s
-- Mathlib.Analysis.InnerProductSpace.EuclideanDist
Euclidean.closedBall_mem_nhds : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : TopologicalSpace E] [inst_2 : IsTopologicalAddGroup E]
  [inst_3 : T2Space E] [inst_4 : Module ℝ E] [inst_5 : ContinuousSMul ℝ E] [inst_6 : FiniteDimensional ℝ E] {x : E}
  {r : ℝ}, 0 < r → Euclidean.closedBall x r ∈ nhds x
-- Mathlib.Probability.Kernel.RadonNikodym
ProbabilityTheory.Kernel.setLIntegral_rnDeriv : ∀ {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ}
  [hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ] {κ η : ProbabilityTheory.Kernel α γ}
  [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η] {a : α},
  (κ a).AbsolutelyContinuous (η a) → ∀ {s : Set γ}, MeasurableSet s → ∫⁻ (c : γ) in s, κ.rnDeriv η a c ∂η a = (κ a) s
-- Mathlib.LinearAlgebra.RootSystem.CartanMatrix
RootPairing.Base.cartanMatrixIn_def : ∀ {ι : 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] (S : Type u_5) [inst_5 : CommRing S]
  [inst_6 : Algebra S R] {P : RootPairing ι R M N} [inst_7 : P.IsValuedIn S] (b : P.Base) (i j : ↥b.support),
  RootPairing.Base.cartanMatrixIn S b i j = P.pairingIn S ↑i ↑j
-- Mathlib.MeasureTheory.OuterMeasure.Caratheodory
MeasureTheory.OuterMeasure.measure_inter_union : ∀ {α : Type u} (m : MeasureTheory.OuterMeasure α) {s₁ s₂ : Set α},
  s₁ ∩ s₂ ⊆ ∅ → m.IsCaratheodory s₁ → ∀ {t : Set α}, m (t ∩ (s₁ ∪ s₂)) = m (t ∩ s₁) + m (t ∩ s₂)
-- Mathlib.LinearAlgebra.Matrix.Integer
Matrix.map_mul_ratCast : ∀ {n : Type u_2} [inst : Fintype n] {α : Type u_3} [inst_1 : DivisionRing α] [CharZero α] (A B : Matrix n n ℚ),
  (A * B).map Rat.cast = A.map Rat.cast * B.map Rat.cast
-- Mathlib.Algebra.Module.LinearMap.FiniteRange
LinearMap.FiniteRangeSetoid.projection_equiv_id : ∀ {K : Type u_1} {V : Type u_2} [inst : CommRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  {S T : Submodule K V} [IsNoetherian K ↥T] (hST : IsCompl S T), S.projection T hST ≈ LinearMap.id
-- Mathlib.RingTheory.TensorProduct.Pi
Algebra.TensorProduct.prodRight_tmul_snd : ∀ (R : Type u_1) (S : Type u_2) (A : Type u_3) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  [inst_3 : Semiring A] [inst_4 : Algebra R A] [inst_5 : Algebra S A] [inst_6 : IsScalarTower R S A] (B : Type u_6)
  (C : Type u_7) [inst_7 : Semiring B] [inst_8 : Semiring C] [inst_9 : Algebra R B] [inst_10 : Algebra R C] (a : A)
  (x : B × C), ((Algebra.TensorProduct.prodRight R S A B C) (a ⊗ₜ[R] x)).2 = a ⊗ₜ[R] x.2
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey_erase : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k a : α} {h' : a ∈ m.erase k}, (m.erase k).getKey a h' = m.getKey a ⋯
-- Mathlib.RingTheory.ClassGroup.Basic
FractionalIdeal.map_canonicalEquiv_mk0 : ∀ {R : Type u_1} (K : Type u_2) [inst : CommRing R] [inst_1 : Field K] [inst_2 : Algebra R K]
  [inst_3 : IsFractionRing R K] [inst_4 : IsDomain R] [inst_5 : IsDedekindDomain R] (K' : Type u_3) [inst_6 : Field K']
  [inst_7 : Algebra R K'] [inst_8 : IsFractionRing R K'] (I : ↥(nonZeroDivisors (Ideal R))),
  (Units.map ↑(FractionalIdeal.canonicalEquiv (nonZeroDivisors R) K K')) ((FractionalIdeal.mk0 K) I) =
    (FractionalIdeal.mk0 K') I
-- Mathlib.Data.Finset.SDiff
/-- `· \ s` is injective on finsets containing `s`.  -/
Finset.superset_injOn_sdiff : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Finset α), Set.InjOn (fun x => x \ s) {t | s ⊆ t}
-- Mathlib.MeasureTheory.Integral.Average
/-- **First moment method**. The maximum of an integrable function is greater than its integral.  -/
MeasureTheory.exists_integral_le : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ}
  [MeasureTheory.IsProbabilityMeasure μ], MeasureTheory.Integrable f μ → ∃ x, ∫ (a : α), f a ∂μ ≤ f x
-- Mathlib.CategoryTheory.Enriched.Ordinary.Basic
/-- The functor that makes up `TransportEnrichment.forgetEnrichmentEquiv`.  -/
CategoryTheory.TransportEnrichment.forgetEnrichmentEquivFunctor : {V : Type u'} →
  [inst : CategoryTheory.Category.{v', u'} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      {W : Type u''} →
        [inst_2 : CategoryTheory.Category.{v'', u''} W] →
          [inst_3 : CategoryTheory.MonoidalCategory W] →
            (F : CategoryTheory.Functor V W) →
              [inst_4 : F.LaxMonoidal] →
                (D : Type u) →
                  [inst_5 : CategoryTheory.EnrichedCategory V D] →
                    (e :
                        (v : V) →
                          (CategoryTheory.MonoidalCategoryStruct.tensorUnit V ⟶ v) ≃
                            (CategoryTheory.MonoidalCategoryStruct.tensorUnit W ⟶ F.obj v)) →
                      (∀ (v : V) (f : CategoryTheory.MonoidalCategoryStruct.tensorUnit V ⟶ v),
                          (e v) f =
                            CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε F) (F.map f)) →
                        CategoryTheory.Functor
                          (CategoryTheory.TransportEnrichment F (CategoryTheory.ForgetEnrichment V D))
                          (CategoryTheory.ForgetEnrichment W (CategoryTheory.TransportEnrichment F D))
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.mem_pi : ∀ {ι : Type u_4} {M : ι → Type u_5} [inst : (i : ι) → MulOneClass (M i)] (I : Set ι) {S : (i : ι) → Submonoid (M i)}
  {p : (i : ι) → M i}, p ∈ Submonoid.pi I S ↔ ∀ i ∈ I, p i ∈ S i
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Pi
cfcₙ_map_pi : ∀ {ι : Type u_1} {R : Type u_2} {S : Type u_3} {A : ι → Type u_4} [inst : CommSemiring R] [inst_1 : Nontrivial R]
  [inst_2 : StarRing R] [inst_3 : MetricSpace R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R]
  [inst_6 : CommRing S] [inst_7 : Algebra R S] [inst_8 : (i : ι) → NonUnitalRing (A i)]
  [inst_9 : (i : ι) → Module S (A i)] [inst_10 : (i : ι) → Module R (A i)] [∀ (i : ι), IsScalarTower R S (A i)]
  [inst_12 : ∀ (i : ι), SMulCommClass R (A i) (A i)] [inst_13 : ∀ (i : ι), IsScalarTower R (A i) (A i)]
  [inst_14 : (i : ι) → StarRing (A i)] [inst_15 : (i : ι) → TopologicalSpace (A i)] {p : ((i : ι) → A i) → Prop}
  {q : (i : ι) → A i → Prop} [inst_16 : NonUnitalContinuousFunctionalCalculus R ((i : ι) → A i) p]
  [inst_17 : ∀ (i : ι), NonUnitalContinuousFunctionalCalculus R (A i) (q i)]
  [∀ (i : ι), ContinuousMapZero.UniqueHom R (A i)] (f : R → R) (a : (i : ι) → A i),
  autoParam (ContinuousOn f (⋃ i, quasispectrum R (a i))) cfcₙ_map_pi._auto_1 →
    autoParam (p a) cfcₙ_map_pi._auto_3 →
      autoParam (∀ (i : ι), q i (a i)) cfcₙ_map_pi._auto_5 → cfcₙ f a = fun i => cfcₙ f (a i)
-- Mathlib.Algebra.Category.CommHopfAlgCat
CommHopfAlgCat.isoEquivBialgEquiv_symm_apply : ∀ {R : Type u} [inst : CommRing R] {X Y : Type v} [inst_1 : CommRing X] [inst_2 : HopfAlgebra R X] [inst_3 : CommRing Y]
  [inst_4 : HopfAlgebra R Y] (e : X ≃ₐc[R] Y), CommHopfAlgCat.isoEquivBialgEquiv.symm e = CommHopfAlgCat.isoMk e
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
hasProdUniformlyOn_iff_tendstoUniformlyOn : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : CommMonoid α] {f : ι → β → α} {g : β → α} {s : Set β}
  [inst_1 : UniformSpace α],
  HasProdUniformlyOn f g s ↔ TendstoUniformlyOn (fun x1 x2 => ∏ i ∈ x1, f i x2) g Filter.atTop s
-- Mathlib.RingTheory.Etale.Locus
Algebra.etaleLocus_eq_compl_support : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A],
  Algebra.etaleLocus R A = (Module.support A Ω[A⁄R])ᶜ ∩ (Module.support A (Algebra.H1Cotangent R A))ᶜ
-- Mathlib.AlgebraicGeometry.StructureSheaf
AlgebraicGeometry.StructureSheaf.const_self : ∀ {R : Type u} [inst : CommRing R] (f : R) (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R))
  (hu : U ≤ PrimeSpectrum.basicOpen f), AlgebraicGeometry.StructureSheaf.const f f U hu = 1
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.projectMapAux.eq_2 : ∀ {C : Type u} {D : Type u'} [inst : CategoryTheory.Category.{v', u'} D] [inst_1 : CategoryTheory.MonoidalCategory D]
  (f : C → D) (X Y Z : CategoryTheory.FreeMonoidalCategory C),
  CategoryTheory.FreeMonoidalCategory.projectMapAux f (CategoryTheory.FreeMonoidalCategory.Hom.α_hom X Y Z) =
    (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.FreeMonoidalCategory.projectObj f X)
        (CategoryTheory.FreeMonoidalCategory.projectObj f Y) (CategoryTheory.FreeMonoidalCategory.projectObj f Z)).hom
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.instAdd.eq_1 : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : Add Y],
  LocallyConstant.instAdd = { add := fun f g => { toFun := ⇑f + ⇑g, isLocallyConstant := ⋯ } }
-- Mathlib.GroupTheory.Torsion
/-- **Alias** of `isAddTorsion_of_finite`.

---

Finite additive groups are torsion additive groups.  -/
is_add_torsion_of_finite : ∀ {G : Type u_1} [inst : AddGroup G] [Finite G], IsAddTorsion G
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.mem_alter_of_not_compare_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k k' : α} {f : Option β → Option β}, ¬cmp k k' = Ordering.eq → (k' ∈ Std.DTreeMap.Raw.Const.alter t k f ↔ k' ∈ t)
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
/-- Constructor to show a wide pullback cone is limiting.  -/
CategoryTheory.Limits.WidePullbackCone.IsLimit.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {ι : Type u_1} →
      {X : C} →
        {Y : ι → C} →
          {f : (i : ι) → Y i ⟶ X} →
            (s : CategoryTheory.Limits.WidePullbackCone f) →
              (lift : (t : CategoryTheory.Limits.WidePullbackCone f) → t.pt ⟶ s.pt) →
                (∀ (t : CategoryTheory.Limits.WidePullbackCone f),
                    CategoryTheory.CategoryStruct.comp (lift t) s.base = t.base) →
                  (∀ (t : CategoryTheory.Limits.WidePullbackCone f) (i : ι),
                      CategoryTheory.CategoryStruct.comp (lift t) (s.π i) = t.π i) →
                    (∀ (t : CategoryTheory.Limits.WidePullbackCone f) (m : t.pt ⟶ s.pt),
                        CategoryTheory.CategoryStruct.comp m s.base = t.base →
                          (∀ (i : ι), CategoryTheory.CategoryStruct.comp m (s.π i) = t.π i) → m = lift t) →
                      CategoryTheory.Limits.IsLimit s
-- Mathlib.CategoryTheory.Galois.Equivalence
CategoryTheory.PreGaloisCategory.instEssSurjContActionFintypeCatFunObjFiniteAutFunctorFunctorToContActionOfFiberFunctor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.GaloisCategory C]
  {F : CategoryTheory.Functor C FintypeCat} [CategoryTheory.PreGaloisCategory.FiberFunctor F],
  (CategoryTheory.PreGaloisCategory.functorToContAction F).EssSurj
-- Mathlib.MeasureTheory.Function.SpecialFunctions.Sinc
Real.measurable_sinc : Measurable Real.sinc
-- Init.Data.FloatArray.Basic
FloatArray.ext_iff : ∀ {x y : FloatArray}, x = y ↔ x.data = y.data
-- Mathlib.Combinatorics.SimpleGraph.Finsubgraph
/-- The finite subgraph of G generated by a single vertex.  -/
SimpleGraph.singletonFinsubgraph : {V : Type u} → {G : SimpleGraph V} → V → G.Finsubgraph
-- Mathlib.Geometry.Manifold.Algebra.Monoid
instContMDiffMulOfSomeENatTopOfLEInfty : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : Mul G] [inst_5 : TopologicalSpace G] [inst_6 : ChartedSpace H G] {a : WithTop ℕ∞} [ContMDiffMul I (↑⊤) G]
  [h : ENat.LEInfty a], ContMDiffMul I a G
-- Mathlib.Algebra.Ring.Defs
CommRing.mk : {α : Type u} → [toRing : Ring α] → (∀ (a b : α), a * b = b * a) → CommRing α
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.Multifork.ext_hom_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape}
  {I : CategoryTheory.Limits.MulticospanIndex J C} {t s : CategoryTheory.Limits.Multifork I} (e : t.pt ≅ s.pt)
  (h :
    autoParam (∀ (i : J.L), CategoryTheory.CategoryStruct.comp e.hom (s.ι i) = t.ι i)
      CategoryTheory.Limits.Multifork.ext._auto_1),
  (CategoryTheory.Limits.Multifork.ext e h).hom.hom = e.hom
-- Batteries.Control.LawfulMonadState
LawfulMonadStateOf.modifyThe_eq : ∀ {σ : Type u_2} {m : Type u_2 → Type u_1} [inst : Monad m] [inst_1 : MonadStateOf σ m] [LawfulMonadStateOf σ m]
  (f : σ → σ),
  modifyThe σ f = do
    let __do_lift ← get
    set (f __do_lift)