mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Lie.IdealOperations
LieSubmodule.lieIdeal_oper_eq_linear_span' : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] (N : LieSubmodule R L M) [inst_5 : LieAlgebra R L]
  (I : LieIdeal R L) [LieModule R L M], ↑⁅I, N⁆ = Submodule.span R {x | ∃ x_1 ∈ I, ∃ n ∈ N, ⁅x_1, n⁆ = x}
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.contains_of_contains_erase : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], (↑m).WF → ∀ {k a : α}, (m.erase k).contains a = true → m.contains a = true
-- Mathlib.LinearAlgebra.Dual.Lemmas
Subspace.instModuleDualFiniteDimensional : ∀ {K : Type u_1} {V : Type u_2} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [FiniteDimensional K V], FiniteDimensional K (Module.Dual K V)
-- Lean.ParserCompiler
Lean.ParserCompiler.Context.mk : {α : Type} →
  Lean.Name → Lean.KeyedDeclsAttribute α → Lean.ParserCompiler.CombinatorAttribute → Lean.ParserCompiler.Context α
-- Mathlib.MeasureTheory.Measure.AddContent
MeasureTheory.instInhabitedAddContent : {α : Type u_1} →
  {C : Set (Set α)} → {G : Type u_2} → [inst : AddCommMonoid G] → Inhabited (MeasureTheory.AddContent G C)
-- Init.Data.Random
/-- `next` operation returns a natural number that is uniformly distributed
 the range returned by `range` (including both end points),
and a new generator.  -/
RandomGen.next : {g : Type u} → [self : RandomGen g] → g → ℕ × g
-- Mathlib.MeasureTheory.Function.ConvergenceInMeasure
MeasureTheory.TendstoInMeasure.exists_seq_tendstoInMeasure_atTop : ∀ {α : Type u_1} {ι : Type u_2} {E : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : PseudoEMetricSpace E] {u : Filter ι} [u.NeBot] [u.IsCountablyGenerated] {f : ι → α → E} {g : α → E},
  MeasureTheory.TendstoInMeasure μ f u g →
    ∃ ns, Filter.Tendsto ns Filter.atTop u ∧ MeasureTheory.TendstoInMeasure μ (fun n => f (ns n)) Filter.atTop g
-- Lean.Meta.Match.Match
_private.Lean.Meta.Match.Match.0.Lean.Meta.Match.MatcherKey.isPrivate : Lean.Meta.Match.MatcherKey✝ → Bool
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.associator_naturality_left_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X X' : C}
  (f : X ⟶ X') (Y Z : C) {Z_1 : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X' (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z) ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Y) Z)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X' Y Z).hom h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight f (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)) h)
-- Mathlib.Algebra.MonoidAlgebra.Defs
/-- **Alias** of `MonoidAlgebra.coeff_mul_single_one`. -/
MonoidAlgebra.mul_single_one_apply : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : MulOneClass M] (x : MonoidAlgebra R M) (r : R) (m : M),
  (x * MonoidAlgebra.single 1 r).coeff m = x.coeff m * r
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
AlgEquiv.ofLeftInverse_symm_apply : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] {g : B → A} {f : A →ₐ[R] B} (h : Function.LeftInverse g ⇑f)
  (x : ↥f.range), (AlgEquiv.ofLeftInverse h).symm x = g ↑x
-- Mathlib.Order.WithBot
WithTop.untopD.eq_1 : ∀ {α : Type u_1} (d : α) (x : WithTop α), WithTop.untopD d x = WithTop.recTopCoe d id x
-- Mathlib.RingTheory.Algebraic.Integral
IsAlgebraic.add : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [NoZeroDivisors R]
  {a b : S}, IsAlgebraic R a → IsAlgebraic R b → IsAlgebraic R (a + b)
-- Mathlib.Algebra.Opposites
MulOpposite.instZero : {α : Type u_1} → [Zero α] → Zero αᵐᵒᵖ
-- Mathlib.Computability.TuringMachine.Tape
_private.Mathlib.Computability.TuringMachine.Tape.0.Turing.Tape.nth.match_1.splitter : (motive : ℤ → Sort u_1) →
  (x : ℤ) → (Unit → motive 0) → ((n : ℕ) → motive (Int.ofNat n.succ)) → ((n : ℕ) → motive (Int.negSucc n)) → motive x
-- Mathlib.RingTheory.PowerSeries.Inverse
PowerSeries.hasUnitMulPowIrreducibleFactorization : ∀ {k : Type u_2} [inst : Field k], IsDiscreteValuationRing.HasUnitMulPowIrreducibleFactorization (PowerSeries k)
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.Origin.stx.inj : ∀ {id : Lean.Name} {ref : Lean.Syntax} {id_1 : Lean.Name} {ref_1 : Lean.Syntax},
  Lean.Meta.Origin.stx id ref = Lean.Meta.Origin.stx id_1 ref_1 → id = id_1 ∧ ref = ref_1
-- Mathlib.Topology.Category.TopCat.Limits.Konig
TopCat.partialSections.directed : ∀ {J : Type u} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J TopCat),
  Directed GE.ge fun G => TopCat.partialSections F G.snd
-- Init.Data.SInt.Basic
/-- Decides whether one 16-bit signed integer is strictly less than another. Usually accessed via the
`DecidableLT Int16` instance.

This function is overridden at runtime with an efficient implementation.

Examples:
 * `(if ((-7) : Int16) < 7 then "yes" else "no") = "yes"`
 * `(if (5 : Int16) < 5 then "yes" else "no") = "no"`
 * `show ¬((7 : Int16) < 7) by decide`
 -/
Int16.decLt : (a b : Int16) → Decidable (a < b)
-- Mathlib.AlgebraicTopology.ModelCategory.BrownLemma
HomotopicalAlgebra.CofibrantBrownFactorization.instNonemptyOfIsCofibrant : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] {X Y : C}
  (f : X ⟶ Y) [HomotopicalAlgebra.IsCofibrant X] [HomotopicalAlgebra.IsCofibrant Y],
  Nonempty (HomotopicalAlgebra.CofibrantBrownFactorization f)
-- Mathlib.Analysis.Convex.BetweenList
List.SortedLT.sbtw : ∀ {R : Type u_1} [inst : Field R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] {l : List R},
  l.SortedLT → List.Sbtw R l
-- Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Datatypes
Mathlib.Tactic.Linarith.SimplexAlgorithm.SparseMatrix.mk.injEq : ∀ {n m : ℕ} (data data_1 : Array (Std.HashMap ℕ ℚ)), ({ data := data } = { data := data_1 }) = (data = data_1)
-- Mathlib.Algebra.MonoidAlgebra.Degree
AddMonoidAlgebra.monic_one : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_5} [inst : Semiring R] [inst_1 : LinearOrder B] [inst_2 : OrderBot B]
  {D : A → B} [inst_3 : AddZeroClass A], Function.Injective D → AddMonoidAlgebra.Monic D 1
-- Mathlib.Algebra.Group.Pi.Lemmas
Set.preimage_one : ∀ {α : Type u_5} {β : Type u_6} [inst : One β] (s : Set β) [inst_1 : Decidable (1 ∈ s)],
  1 ⁻¹' s = if 1 ∈ s then Set.univ else ∅
-- Mathlib.CategoryTheory.Adjunction.Quadruple
CategoryTheory.Adjunction.Quadruple.op_leftTriple : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor D C} {G : CategoryTheory.Functor C D}
  {R : CategoryTheory.Functor D C} (q : CategoryTheory.Adjunction.Quadruple L F G R), q.op.leftTriple = q.rightTriple.op
-- Mathlib.Order.Interval.Set.OrdConnected
Set.ordConnected_iff_uIcc_subset_left : ∀ {α : Type u_1} [inst : LinearOrder α] {s : Set α} {x : α},
  x ∈ s → (s.OrdConnected ↔ ∀ ⦃y : α⦄, y ∈ s → Set.uIcc x y ⊆ s)
-- Mathlib.Algebra.Order.ToIntervalMod
toIocDiv_sub_ofNat_mul' : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedAddMonoid R]
  [inst_3 : Archimedean R] {p : R} (hp : 0 < p) (a b : R) (m : ℕ) [inst_4 : m.AtLeastTwo],
  toIocDiv hp (a - OfNat.ofNat m * p) b = toIocDiv hp a b + OfNat.ofNat m
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.Scheme.Opens.toSpecΓ_naturality : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U : Y.Opens),
  CategoryTheory.CategoryStruct.comp ((TopologicalSpace.Opens.map f.base).obj U).toSpecΓ
      (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.Hom.app f U)) =
    CategoryTheory.CategoryStruct.comp (f ∣_ U) U.toSpecΓ
-- Mathlib.Computability.TuringMachine.Tape
Turing.PointedMap.mk.inj : ∀ {Γ : Type u} {Γ' : Type v} {inst : Inhabited Γ} {inst_1 : Inhabited Γ'} {f : Γ → Γ'} {map_pt' : f default = default}
  {f_1 : Γ → Γ'} {map_pt'_1 : f_1 default = default},
  { f := f, map_pt' := map_pt' } = { f := f_1, map_pt' := map_pt'_1 } → f = f_1
-- Std.Http.Data.URI.Encoding
_private.Std.Http.Data.URI.Encoding.0.Std.Http.URI.EncodedString.mk.injEq : ∀ {r : UInt8 → Bool} (toByteArray : ByteArray) (valid : Std.Http.URI.IsAllowedEncodedChars r toByteArray)
  (toByteArray_1 : ByteArray) (valid_1 : Std.Http.URI.IsAllowedEncodedChars r toByteArray_1),
  ({ toByteArray := toByteArray, valid := valid } = { toByteArray := toByteArray_1, valid := valid_1 }) =
    (toByteArray = toByteArray_1)
-- Mathlib.LinearAlgebra.Transvection.Basic
LinearEquiv.dilatransvections.eq_1 : ∀ (R : Type u_1) (V : Type u_2) [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : Module R V],
  LinearEquiv.dilatransvections R V = {e | ∃ f v, ↑e = LinearMap.transvection f v}
-- Mathlib.Order.RelIso.Basic
RelEmbedding.isStrictTotalOrder : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (x : r ↪r s) [IsStrictTotalOrder β s],
  IsStrictTotalOrder α r
-- Mathlib.Logic.Embedding.Basic
subtypeOrLeftEmbedding_apply_right : ∀ {α : Type u_1} {p q : α → Prop} [inst : DecidablePred p] (x : { x // p x ∨ q x }) (hx : ¬p ↑x),
  (subtypeOrLeftEmbedding p q) x = Sum.inr ⟨↑x, ⋯⟩
-- Mathlib.CategoryTheory.Limits.Creates
/-- Transfer creation of limits along a natural isomorphism in the diagram.  -/
CategoryTheory.createsLimitOfIsoDiagram : {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] →
            {K₁ K₂ : CategoryTheory.Functor J C} →
              (F : CategoryTheory.Functor C D) →
                (K₁ ≅ K₂) → [CategoryTheory.CreatesLimit K₁ F] → CategoryTheory.CreatesLimit K₂ F
-- Mathlib.Analysis.Matrix.Order
/-- The isometric continuous functional calculus on `Matrix n n 𝕜` arising from the operator norm
given by the identification with (continuous) linear endomorphisms of `EuclideanSpace 𝕜 n`.  -/
Matrix.instIsometricContinuousFunctionalCalculus : ∀ {𝕜 : Type u_1} {n : Type u_2} [inst : RCLike 𝕜] [inst_1 : Fintype n] [inst_2 : DecidableEq n],
  IsometricContinuousFunctionalCalculus ℝ (Matrix n n 𝕜) IsSelfAdjoint
-- Lean.Elab.Match
/-- Auxiliary structure for storing an type mismatch exception when processing the
pattern #`idx` of some alternative.  -/
Lean.Elab.Term.PatternElabException : Type
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.skipPrefix?_bool_eq_some_iff : ∀ {p : Char → Bool} {s : String} {pos : s.Pos},
  s.skipPrefix? p = some pos ↔ ∃ (h : s.startPos ≠ s.endPos), pos = s.startPos.next h ∧ p (s.startPos.get h) = true
-- Lean.Meta.Constructions.CtorElim
_private.Lean.Meta.Constructions.CtorElim.0.Lean.asPrivateAs : Lean.Name → Lean.Name → Lean.Name
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.Splits.eval_derivative_div_eval_of_ne_zero : ∀ {R : Type u_1} [inst : Field R] {f : Polynomial R},
  f.Splits →
    ∀ {x : R},
      Polynomial.eval x f ≠ 0 →
        Polynomial.eval x (Polynomial.derivative f) / Polynomial.eval x f =
          (Multiset.map (fun z => 1 / (x - z)) f.roots).sum
-- Mathlib.Combinatorics.SetFamily.FourFunctions
/-- The **Four Functions Theorem**, aka **Ahlswede-Daykin Inequality**.  -/
four_functions_theorem : ∀ {α : Type u_1} {β : Type u_2} [inst : DistribLattice α] [inst_1 : CommSemiring β] [inst_2 : LinearOrder β]
  [IsStrictOrderedRing β] [ExistsAddOfLE β] (f₁ f₂ f₃ f₄ : α → β) [inst_5 : DecidableEq α],
  0 ≤ f₁ →
    0 ≤ f₂ →
      0 ≤ f₃ →
        0 ≤ f₄ →
          (∀ (a b : α), f₁ a * f₂ b ≤ f₃ (a ⊓ b) * f₄ (a ⊔ b)) →
            ∀ (s t : Finset α), (∑ a ∈ s, f₁ a) * ∑ a ∈ t, f₂ a ≤ (∑ a ∈ s ⊼ t, f₃ a) * ∑ a ∈ s ⊻ t, f₄ a
-- Mathlib.CategoryTheory.Linear.Yoneda
CategoryTheory.linearCoyoneda_obj_obj_carrier : ∀ (R : Type w) [inst : Ring R] (C : Type u) [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Linear R C] (Y : Cᵒᵖ) (X : C),
  ↑(((CategoryTheory.linearCoyoneda R C).obj Y).obj X) = (Opposite.unop Y ⟶ X)
-- Mathlib.LinearAlgebra.Quotient.Pi
Submodule.quotientPiLift.congr_simp : ∀ {ι : Type u_1} {R : Type u_2} [inst : CommRing R] {Ms : ι → Type u_3} [inst_1 : (i : ι) → AddCommGroup (Ms i)]
  [inst_2 : (i : ι) → Module R (Ms i)] {Ns : ι → Type u_5} [inst_3 : (i : ι) → AddCommGroup (Ns i)]
  [inst_4 : (i : ι) → Module R (Ns i)] (p : (i : ι) → Submodule R (Ms i)) (f f_1 : (i : ι) → Ms i →ₗ[R] Ns i)
  (e_f : f = f_1) (hf : ∀ (i : ι), p i ≤ (f i).ker), Submodule.quotientPiLift p f hf = Submodule.quotientPiLift p f_1 ⋯
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.untop_zero : ∀ {α : Type u} [inst : Zero α], WithTop.untop 0 ⋯ = 0
-- Mathlib.Tactic.TFAE
/-- Convert an expression representing an explicit list into a list of expressions.  -/
_private.Mathlib.Tactic.TFAE.0.Mathlib.Tactic.TFAE.getTFAEList.getExplicitList : Q(List Prop) → Lean.MetaM (List Q(Prop))
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
/-- If three points are not collinear, the sine of the angle between them is positive.  -/
EuclideanGeometry.sin_pos_of_not_collinear : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {p₁ p₂ p₃ : P},
  ¬Collinear ℝ {p₁, p₂, p₃} → 0 < Real.sin (EuclideanGeometry.angle p₁ p₂ p₃)
-- Mathlib.LinearAlgebra.TensorProduct.Map
LinearMap.map_comp_rTensor : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} {Q : Type u_10} {S : Type u_11}
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : AddCommMonoid Q]
  [inst_5 : AddCommMonoid S] [inst_6 : Module R M] [inst_7 : Module R N] [inst_8 : Module R S] [inst_9 : Module R P]
  [inst_10 : Module R Q] (f : M →ₗ[R] P) (g : N →ₗ[R] Q) (f' : S →ₗ[R] M),
  TensorProduct.map f g ∘ₗ LinearMap.rTensor N f' = TensorProduct.map (f ∘ₗ f') g
-- Mathlib.RingTheory.TensorProduct.MonoidAlgebra
/-- The base change of `B[M]` to an `R`-algebra `A` is isomorphic to `(A ⊗[R] B)[M]`
as an `A`-algebra.  -/
MonoidAlgebra.lTensorAlgEquiv : (R : Type u_1) →
  {M : Type u_2} →
    (A : Type u_5) →
      (B : Type u_6) →
        [inst : CommSemiring R] →
          [inst_1 : CommSemiring A] →
            [inst_2 : CommSemiring B] →
              [inst_3 : Algebra R A] →
                [inst_4 : Algebra R B] →
                  [inst_5 : CommMonoid M] →
                    TensorProduct R (MonoidAlgebra A M) B ≃ₐ[R] MonoidAlgebra (TensorProduct R A B) M
-- Mathlib.Topology.Order.UpperLowerSetTopology
Topology.isLowerSet_iff_nhds : ∀ {α : Type u_4} [inst : TopologicalSpace α] [inst_1 : Preorder α],
  Topology.IsLowerSet α ↔ ∀ (a : α), nhds a = Filter.principal (Set.Iic a)
-- Mathlib.Dynamics.Ergodic.Conservative
/-- Poincaré recurrence theorem. Let `f : α → α` be a conservative dynamical system on a topological
space with second countable topology and measurable open sets. Then almost every point `x : α`
is recurrent: it visits every neighborhood `s ∈ 𝓝 x` infinitely many times.  -/
MeasureTheory.Conservative.ae_frequently_mem_of_mem_nhds : ∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] [SecondCountableTopology α]
  [OpensMeasurableSpace α] {f : α → α} {μ : MeasureTheory.Measure α},
  MeasureTheory.Conservative f μ → ∀ᵐ (x : α) ∂μ, ∀ s ∈ nhds x, ∃ᶠ (n : ℕ) in Filter.atTop, f^[n] x ∈ s
-- Mathlib.Analysis.InnerProductSpace.LinearMap
_private.Mathlib.Analysis.InnerProductSpace.LinearMap.0.«term⟪_,_⟫» : Lean.ParserDescr
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.aeval_subalgebra_coe : ∀ {R : Type u} [inst : CommSemiring R] (g : Polynomial R) {A : Type u_3} [inst_1 : Semiring A] [inst_2 : Algebra R A]
  (s : Subalgebra R A) (f : ↥s), ↑((Polynomial.aeval f) g) = (Polynomial.aeval ↑f) g
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Var.denote : Nat.Internal.Linear.Context → Nat.Internal.Linear.Var → ℕ
-- Mathlib.Algebra.Group.Hom.Defs
/-- Additive group homomorphisms preserve negation.  -/
AddMonoidHom.map_neg : ∀ {α : Type u_2} {β : Type u_3} [inst : AddGroup α] [inst_1 : SubtractionMonoid β] (f : α →+ β) (a : α), f (-a) = -f a
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.val_algHomUnitsEquiv_symm_apply : ∀ (R : Type u_1) (S : Type u_2) [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] (f : S ≃ₐ[R] S),
  ↑((AlgEquiv.algHomUnitsEquiv R S).symm f) = ↑f
-- Init.Data.ByteArray.Basic
/-- Returns `true` when `s` contains zero bytes.
 -/
ByteArray.isEmpty : ByteArray → Bool
-- Mathlib.RingTheory.HopfAlgebra.Quotient
HopfAlgebra.Quotient.instQuotientIdeal : {R : Type u_1} →
  {A : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : Ring A] →
        [inst_2 : HopfAlgebra R A] →
          (I : Ideal A) → [inst_3 : I.IsTwoSided] → [Ideal.IsHopfIdeal R I] → HopfAlgebra R (A ⧸ I)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.InlayHintKind : Type
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Add
Std.Tactic.BVDecide.BVExpr.bitblast.FullAdderOutput.hle : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {old : Std.Sat.AIG α}
  (self : Std.Tactic.BVDecide.BVExpr.bitblast.FullAdderOutput old), old.decls.size ≤ self.aig.decls.size
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientAddGroup.rangeKerLift_surjective : ∀ {G : Type u} [inst : AddGroup G] {H : Type v} [inst_1 : AddGroup H] (φ : G →+ H),
  Function.Surjective ⇑(QuotientAddGroup.rangeKerLift φ)
-- Init.Data.String.Pattern.Pred
String.Slice.Pattern.CharPred.Decidable.instForwardPatternForallCharPropOfDecidablePred : {p : Char → Prop} → [DecidablePred p] → String.Slice.Pattern.ForwardPattern p
-- Mathlib.Algebra.Polynomial.Degree.CardPowDegree
/-- `cardPowDegree` is the absolute value on `𝔽_q[t]` sending `f` to `q ^ degree f`.

`cardPowDegree 0` is defined to be `0`.  -/
Polynomial.cardPowDegree : {Fq : Type u_1} → [inst : Field Fq] → [Fintype Fq] → AbsoluteValue (Polynomial Fq) ℤ
-- Mathlib.Data.Finset.Lattice.Basic
Finset.inter_eq_left : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α}, s ∩ t = s ↔ s ⊆ t
-- Mathlib.Topology.UniformSpace.Separation
SeparationQuotient.uniformContinuous_dom₂ : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : UniformSpace α] [inst_1 : UniformSpace β] [inst_2 : UniformSpace γ]
  {f : SeparationQuotient α × SeparationQuotient β → γ},
  UniformContinuous f ↔ UniformContinuous fun p => f (SeparationQuotient.mk p.1, SeparationQuotient.mk p.2)
-- Mathlib.RingTheory.IdealFilter.Basic
/-- Module-level `F`-torsion: every element is `F`-torsion.  -/
IdealFilter.IsTorsion : {A : Type u_1} → [inst : Ring A] → IdealFilter A → (M : Type u_2) → [inst_1 : AddCommMonoid M] → [Module A M] → Prop
-- Mathlib.Analysis.InnerProductSpace.Reproducing
RKHS.coe_zero : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {X : Type u_2} {V : Type u_3} [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] {H : Type u_4} [inst_3 : NormedAddCommGroup H] [inst_4 : InnerProductSpace 𝕜 H]
  [inst_5 : RKHS 𝕜 H X V], ⇑0 = 0
-- Mathlib.Data.Matrix.Mul
Matrix.pow_row_eq_zero_of_le : ∀ {n : Type u_3} {R : Type u_7} [inst : Semiring R] [inst_1 : Fintype n] [inst_2 : DecidableEq n] {M : Matrix n n R}
  {k l : ℕ} {i : n}, (M ^ k).row i = 0 → k ≤ l → (M ^ l).row i = 0
-- Mathlib.Order.Grade
grade_ne_grade_iff : ∀ {𝕆 : Type u_1} {α : Type u_3} [inst : Preorder 𝕆] [inst_1 : LinearOrder α] [inst_2 : GradeOrder 𝕆 α] {a b : α},
  grade 𝕆 a ≠ grade 𝕆 b ↔ a ≠ b
-- Mathlib.Probability.Moments.Basic
ProbabilityTheory.centralMoment_one' : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.Integrable X μ → ProbabilityTheory.centralMoment X 1 μ = (1 - μ.real Set.univ) * ∫ (x : Ω), X x ∂μ
-- Mathlib.Algebra.BigOperators.Fin
Fin.prod_uIcc_castAdd : ∀ {M : Type u_2} [inst : CommMonoid M] {n : ℕ} (m : ℕ) (f : Fin (n + m) → M) (a b : Fin n),
  ∏ i ∈ Finset.uIcc (Fin.castAdd m a) (Fin.castAdd m b), f i = ∏ i ∈ Finset.uIcc a b, f (Fin.castAdd m i)
-- Mathlib.Topology.PartialHomeomorph.Defs
PartialHomeomorph.continuousOn_invFun : ∀ {X : Type u_7} {Y : Type u_8} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (self : PartialHomeomorph X Y), ContinuousOn self.invFun self.target
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.ring : Lean.Meta.Grind.Arith.Linear.RingIneqCnstr →
  Lean.Meta.Grind.Arith.Linear.LinExpr → Lean.Meta.Grind.Arith.Linear.IneqCnstrProof
-- Mathlib.RingTheory.Localization.Integral
/-- Taking integral closure commutes with localizations.  -/
IsLocalization.integralClosure : ∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] [inst_2 : Algebra R S] {Rf : Type u_5}
  {Sf : Type u_6} [inst_3 : CommRing Rf] [inst_4 : CommRing Sf] [inst_5 : Algebra R Rf] [inst_6 : Algebra S Sf]
  [inst_7 : Algebra Rf Sf] [inst_8 : Algebra R Sf] [IsScalarTower R S Sf] [inst_10 : IsScalarTower R Rf Sf]
  (M : Submonoid R) [IsLocalization M Rf] [IsLocalization (Algebra.algebraMapSubmonoid S M) Sf]
  [inst_13 : Algebra ↥(integralClosure R S) ↥(integralClosure Rf Sf)]
  [IsScalarTower (↥(integralClosure R S)) (↥(integralClosure Rf Sf)) Sf]
  [IsScalarTower R ↥(integralClosure R S) ↥(integralClosure Rf Sf)],
  IsLocalization (Algebra.algebraMapSubmonoid (↥(integralClosure R S)) M) ↥(integralClosure Rf Sf)
-- Mathlib.Algebra.Group.ModEq
AddCommGroup.ModEq.add_right_cancel' : ∀ {M : Type u_1} [inst : AddCancelCommMonoid M] {a b p : M} (c : M), a + c ≡ b + c [PMOD p] → a ≡ b [PMOD p]
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.mk.eq_1 : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {β : Type u_5} [inst_1 : TopologicalSpace β]
  (f : α → β) (hf : MeasureTheory.AEStronglyMeasurable f μ), MeasureTheory.AEEqFun.mk f hf = Quotient.mk'' ⟨f, hf⟩
-- Mathlib.Data.List.AList
AList.insert_insert_of_ne : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a a' : α} {b : β a} {b' : β a'} (s : AList β),
  a ≠ a' → (AList.insert a' b' (AList.insert a b s)).entries.Perm (AList.insert a b (AList.insert a' b' s)).entries
-- Mathlib.Algebra.Algebra.RestrictScalars
/-- When `M` is a right-module over a ring `S`, and `S` is an algebra over `R`, then `M` inherits a
right-module structure over `R`.
The preferred way of setting this up is
`[Module Rᵐᵒᵖ M] [Module Sᵐᵒᵖ M] [IsScalarTower Rᵐᵒᵖ Sᵐᵒᵖ M]`.
 -/
RestrictScalars.opModule : (R : Type u_1) →
  (S : Type u_2) →
    (M : Type u_3) →
      [inst : Semiring S] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : CommSemiring R] → [Algebra R S] → [Module Sᵐᵒᵖ M] → Module Rᵐᵒᵖ (RestrictScalars R S M)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.any_toList : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} {p : (a : α) → β a → Bool},
  (m.toList.any fun x => p x.fst x.snd) = m.any p
-- Mathlib.GroupTheory.MonoidLocalization.Basic
/-- Given a localization map `f : M →* N`, and `z w : N`, there exist `z' w' : M` and `d : S`
such that `f z' / f d = z` and `f w' / f d = w`.  -/
Submonoid.LocalizationMap.surj₂ : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N]
  (f : S.LocalizationMap N) (z w : N), ∃ z' w' d, z * f ↑d = f z' ∧ w * f ↑d = f w'
-- Mathlib.MeasureTheory.Function.EssSup
essInf_eq_ciInf : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : ConditionallyCompleteLattice β] {f : α → β} [Nonempty α],
  (∀ (a : α), μ {a} ≠ 0) → BddBelow (Set.range f) → essInf f μ = ⨅ a, f a