mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Convex.Cone.InnerDual
ProperCone.innerDual_insert : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : CompleteSpace E] (x : E)
  (s : Set E), ProperCone.innerDual (insert x s) = ProperCone.innerDual {x} ⊓ ProperCone.innerDual s
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.degree_sub_eq_right_of_degree_lt : ∀ {R : Type u} [inst : Ring R] {p q : Polynomial R}, p.degree < q.degree → (p - q).degree = q.degree
-- Mathlib.Algebra.IsPrimePow
/-- **Alias** of `IsPrimePow.not_isUnit`. -/
IsPrimePow.not_unit : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] {n : R}, IsPrimePow n → ¬IsUnit n
-- Mathlib.Algebra.Order.Interval.Basic
NonemptyInterval.one_mem_one : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : One α], 1 ∈ 1
-- Mathlib.Order.ModularLattice
OrderIso.setCongr.congr_simp : ∀ {α : Type u_1} [inst : Preorder α] (s t : Set α) (h : s = t), OrderIso.setCongr s t h = OrderIso.setCongr s t h
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
/-- `negAt` preserves the `norm`.  -/
NumberField.mixedEmbedding.norm_negAt : ∀ {K : Type u_1} [inst : Field K] {s : Set { w // w.IsReal }} [inst_1 : NumberField K]
  (x : NumberField.mixedEmbedding.mixedSpace K),
  NumberField.mixedEmbedding.norm ((NumberField.mixedEmbedding.negAt s) x) = NumberField.mixedEmbedding.norm x
-- Std.Data.DTreeMap.Internal.Def
/-- (Implementation detail) The actual inductive type for the size-balanced tree data structure.  -/
Std.DTreeMap.Internal.Impl : (α : Type u) → (α → Type v) → Type (max u v)
-- Mathlib.Algebra.Group.UniqueProds.Basic
TwoUniqueSums.instAddOpposite : ∀ {G : Type u} [inst : Add G] [h : TwoUniqueSums G], TwoUniqueSums Gᵃᵒᵖ
-- Mathlib.CategoryTheory.MorphismProperty.LocalClosure
CategoryTheory.MorphismProperty.sourceLocalClosure.of_presieve : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {K : CategoryTheory.Precoverage C}
  {P : CategoryTheory.MorphismProperty C} {X Y : C} (f : X ⟶ Y),
  ∀ R ∈ K.coverings X,
    (∀ (U : C) (g : U ⟶ X),
        R g → CategoryTheory.MorphismProperty.sourceLocalClosure K P (CategoryTheory.CategoryStruct.comp g f)) →
      CategoryTheory.MorphismProperty.sourceLocalClosure K P f
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.enorm_setToFun_le : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {T : Set α → E →L[ℝ] F} {C : ℝ} {f : α → E} (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) (hC : 0 ≤ C),
  ‖MeasureTheory.setToFun μ T hT f‖ₑ ≤ ↑(NNReal.mk C hC) * ∫⁻ (x : α), ‖f x‖ₑ ∂μ
-- Init.Data.List.Count
List.count_filterMap : ∀ {β : Type u_1} {α : Type u_2} [inst : BEq β] {b : β} {f : α → Option β} {l : List α},
  List.count b (List.filterMap f l) = List.countP (fun a => f a == some b) l
-- Mathlib.NumberTheory.HeckeRing.Defs
HeckeCosetModule.of_apply : ∀ {G : Type u_1} [inst : Group G] {Δ : Submonoid G} {H₁ H₂ : Subgroup G} {Z : Type u_3} [inst_1 : Zero Z]
  (f : HeckeCoset Δ H₁ H₂ →₀ Z) (D : HeckeCoset Δ H₁ H₂), (HeckeCosetModule.of f) D = f D
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.eraseList.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (l : List ((a : α) × β a)) (hd : α) (tl : List α),
  Std.Internal.List.eraseList l (hd :: tl) = Std.Internal.List.eraseList (Std.Internal.List.eraseKey hd l) tl
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- Evaluate `η ◫ (f ◁ θ)`  -/
Mathlib.Tactic.BicategoryLike.MkEvalHorizontalComp.mkEvalHorizontalCompAux'OfWhisker : {m : Type → Type} →
  [self : Mathlib.Tactic.BicategoryLike.MkEvalHorizontalComp m] →
    Mathlib.Tactic.BicategoryLike.Atom₁ →
      Mathlib.Tactic.BicategoryLike.HorizontalComp →
        Mathlib.Tactic.BicategoryLike.WhiskerLeft →
          Mathlib.Tactic.BicategoryLike.NormalExpr →
            Mathlib.Tactic.BicategoryLike.NormalExpr →
              Mathlib.Tactic.BicategoryLike.NormalExpr →
                Mathlib.Tactic.BicategoryLike.NormalExpr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → m Lean.Expr
-- Mathlib.RingTheory.AdjoinRoot
/-- **Alias** of `AdjoinRoot.quotMapOfEquivQuotMapCMapMk_mk`. -/
AdjoinRoot.quotMapOfEquivQuotMapCMapSpanMk_mk : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) (f : Polynomial R) (x : AdjoinRoot f),
  (AdjoinRoot.quotMapOfEquivQuotMapCMapMk I f) ((Ideal.Quotient.mk (Ideal.map (AdjoinRoot.of f) I)) x) =
    (Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk (Ideal.span {f})) (Ideal.map Polynomial.C I))) x
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.length_keys : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t.keys.length = t.size
-- Mathlib.CategoryTheory.Preadditive.CommGrp_
CategoryTheory.Preadditive.commGrpEquivalenceAux_inv_app_hom_hom_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.CartesianMonoidalCategory C] [inst_3 : CategoryTheory.BraidedCategory C]
  (X : CategoryTheory.CommGrp C),
  (CategoryTheory.Preadditive.commGrpEquivalenceAux.inv.app X).hom.hom.hom = CategoryTheory.CategoryStruct.id X.X
-- Mathlib.Analysis.InnerProductSpace.Spectrum
/-- A self-adjoint operator preserves orthogonal complements of its eigenspaces.  -/
LinearMap.IsSymmetric.invariant_orthogonalComplement_eigenspace : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E →ₗ[𝕜] E}, T.IsSymmetric → ∀ (μ : 𝕜), ∀ v ∈ (Module.End.eigenspace T μ)ᗮ, T v ∈ (Module.End.eigenspace T μ)ᗮ
-- Mathlib.CategoryTheory.Functor.Flat
CategoryTheory.lan_preservesFiniteLimits_of_preservesFiniteLimits : ∀ {C D : Type u₁} [inst : CategoryTheory.SmallCategory C] [inst_1 : CategoryTheory.SmallCategory D] (E : Type u₂)
  [inst_2 : CategoryTheory.Category.{u₁, u₂} E] {FE : E → E → Type u_1} {CE : E → Type u₁}
  [inst_3 : (X Y : E) → FunLike (FE X Y) (CE X) (CE Y)] [inst_4 : CategoryTheory.ConcreteCategory E FE]
  [CategoryTheory.Limits.HasLimits E] [inst_6 : CategoryTheory.Limits.HasColimits E]
  [CategoryTheory.Limits.ReflectsLimits (CategoryTheory.forget E)]
  [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget E)]
  [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget E)] [CategoryTheory.Limits.HasFiniteLimits C]
  (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesFiniteLimits F],
  CategoryTheory.Limits.PreservesFiniteLimits F.op.lan
-- Lean.Elab.Tactic.Try
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.getEvalFns : Lean.SyntaxNodeKind → Lean.CoreM (List (Lean.KeyedDeclsAttribute.AttributeEntry Lean.Elab.Tactic.Try.TryTactic))
-- Mathlib.Combinatorics.Enumerative.Composition
compositionAsSet_card : ∀ (n : ℕ), Fintype.card (CompositionAsSet n) = 2 ^ (n - 1)
-- Mathlib.Analysis.Normed.Module.Basic
/-- A normed algebra `𝕜'` over `𝕜` is normed module that is also an algebra.

See the implementation notes for `Algebra` for a discussion about non-unital algebras. Following
the strategy there, a non-unital *normed* algebra can be written as:
```lean
variable [NormedField 𝕜] [NonUnitalSeminormedRing 𝕜']
variable [NormedSpace 𝕜 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜']
```
 -/
NormedAlgebra : (𝕜 : Type u_6) → (𝕜' : Type u_7) → [NormedField 𝕜] → [SeminormedRing 𝕜'] → Type (max u_6 u_7)
-- Mathlib.Data.Ordmap.Ordset
Ordnode.delta.eq_1 : Ordnode.delta = 3
-- Mathlib.Combinatorics.Additive.ETransform
/-- An **e-transform**.
Turns `(s, t)` into `(s ∪ s +ᵥ e, t ∩ -e +ᵥ t)`. This reduces the sum of the two sets.  -/
Finset.addETransformRight : {α : Type u_1} → [DecidableEq α] → [AddGroup α] → α → Finset α × Finset α → Finset α × Finset α
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
NumberField.mixedEmbedding.fundamentalCone.integerSetEquivNorm_apply_fst : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {n : ℕ}
  (a : { a // NumberField.mixedEmbedding.norm ↑a = ↑n }),
  ↑↑((NumberField.mixedEmbedding.fundamentalCone.integerSetEquivNorm K n) a).1 =
    Ideal.span {↑(NumberField.mixedEmbedding.fundamentalCone.preimageOfMemIntegerSet ↑a)}
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.toSubmodule_inj : ∀ {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 N' : LieSubmodule R L M), ↑N = ↑N' ↔ N = N'
-- Mathlib.Algebra.Group.Submonoid.Units
AddSubmonoid.addUnitsEquivIsAddUnitAddSubmonoid.eq_1 : ∀ {M : Type u_1} [inst : AddMonoid M] (S : AddSubmonoid M),
  S.addUnitsEquivIsAddUnitAddSubmonoid =
    S.addUnitsEquivAddUnitsType.trans AddSubmonoid.addUnitsTypeEquivIsAddUnitAddSubmonoid
-- Mathlib.Computability.AkraBazzi.GrowsPolynomially
AkraBazziRecurrence.GrowsPolynomially.eventually_zero_of_frequently_zero : ∀ {f : ℝ → ℝ},
  AkraBazziRecurrence.GrowsPolynomially f → (∃ᶠ (x : ℝ) in Filter.atTop, f x = 0) → ∀ᶠ (x : ℝ) in Filter.atTop, f x = 0
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
AffineMap.map_top_of_surjective : ∀ {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁] [inst_4 : AddCommGroup V₂]
  [inst_5 : Module k V₂] [inst_6 : AddTorsor V₂ P₂] (f : P₁ →ᵃ[k] P₂),
  Function.Surjective ⇑f → AffineSubspace.map f ⊤ = ⊤
-- Mathlib.Algebra.NeZero
eq_zero_or_neZero : ∀ {R : Type u_1} [inst : Zero R] (a : R), a = 0 ∨ NeZero a
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
_private.Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable.0.MeasureTheory.«term_→ₛ_» : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.isoWhiskerRight_left : ∀ {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] {B : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} B] (F : CategoryTheory.Functor B C) {G H : CategoryTheory.Functor C D}
  (α : G ≅ H) (K : CategoryTheory.Functor D E),
  CategoryTheory.Functor.isoWhiskerRight (F.isoWhiskerLeft α) K =
    F.associator G K ≪≫ F.isoWhiskerLeft (CategoryTheory.Functor.isoWhiskerRight α K) ≪≫ (F.associator H K).symm
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.equiv_iff_keys_unit_perm : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α Unit cmp}, t₁.Equiv t₂ ↔ t₁.keys.Perm t₂.keys
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.monomialRpow.eq_2 : ∀ (basis_hd : ℝ → ℝ) (basis_tl : Tactic.ComputeAsymptotics.Basis) (r : ℝ) (m : ℕ),
  Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.monomialRpow basis_hd basis_tl m.succ r =
    Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.cons 0
      (Tactic.ComputeAsymptotics.MultiseriesExpansion.monomialRpow basis_tl m r)
      Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.nil
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- The canonical map `S.opcycles ⟶ X₃`.  -/
CategoryTheory.ShortComplex.fromOpcycles : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (S : CategoryTheory.ShortComplex C) → [inst_2 : S.HasRightHomology] → S.opcycles ⟶ S.X₃
-- Init.Data.Int.Linear
Int.Internal.Linear.dvd_neg_le_tight_cert : ℤ → Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → Bool
-- Mathlib.Topology.Semicontinuity.Basic
/-- **Alias** of the forward direction of `lowerSemicontinuousAt_iff_le_liminf`. -/
LowerSemicontinuousAt.le_liminf : ∀ {α : Type u_1} [inst : TopologicalSpace α] {x : α} {γ : Type u_4} [inst_1 : CompleteLinearOrder γ] {f : α → γ},
  LowerSemicontinuousAt f x → f x ≤ Filter.liminf f (nhds x)
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- Restrict a cone to the diagram over `j`. This preserves being limiting if the forgetful functor
`Over j ⥤ J` is initial (see `CategoryTheory.Limits.IsLimit.overPost`).
 -/
CategoryTheory.Limits.Cone.overPost : {J : Type u_1} →
  {C : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} J] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} C] →
        {D : CategoryTheory.Functor J C} →
          CategoryTheory.Limits.Cone D → (j : J) → CategoryTheory.Limits.Cone (CategoryTheory.Over.post D)
-- Mathlib.Algebra.Group.Units.Equiv
Equiv.addLeft_symm : ∀ {G : Type u_5} [inst : AddGroup G] (a : G), Equiv.symm (Equiv.addLeft a) = Equiv.addLeft (-a)
-- Mathlib.Analysis.Calculus.FDeriv.Const
fderivWithin_intCast : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {s : Set E} [inst_7 : IntCast F] (z : ℤ), fderivWithin 𝕜 (↑z) s = 0
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
HasDerivWithinAt.rpow : ∀ {f g : ℝ → ℝ} {f' g' x : ℝ} {s : Set ℝ},
  HasDerivWithinAt f f' s x →
    HasDerivWithinAt g g' s x →
      0 < f x → HasDerivWithinAt (fun x => f x ^ g x) (f' * g x * f x ^ (g x - 1) + g' * f x ^ g x * Real.log (f x)) s x
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.aeval_val_σ : ∀ {R : Type u} {S : Type v} {ι : Type w} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.Generators R S ι) (s : S), (MvPolynomial.aeval P.val) (P.σ s) = s
-- Lean.Meta.TryThis
/-- How to construct the text that appears in the lightbulb menu from the suggestion text. If
`none`, we use `fun ppSuggestionText => "Try this: " ++ ppSuggestionText`. Only the pretty-printed
`suggestion : SuggestionText` is used here.  -/
Lean.Meta.Tactic.TryThis.Suggestion.toCodeActionTitle? : Lean.Meta.Tactic.TryThis.Suggestion → Option (String → String)
-- Mathlib.CategoryTheory.Shift.ShiftSequence
CategoryTheory.Functor.shiftIso_add_hom_app : ∀ {C : Type u_1} {A : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} A] (F : CategoryTheory.Functor C A) {M : Type u_4} [inst_2 : AddMonoid M]
  [inst_3 : CategoryTheory.HasShift C M] [inst_4 : F.ShiftSequence M] (n m a a' a'' : M) (ha' : n + a = a')
  (ha'' : m + a' = a'') (X : C),
  (F.shiftIso (m + n) a a'' ⋯).hom.app X =
    CategoryTheory.CategoryStruct.comp ((F.shift a).map ((CategoryTheory.shiftFunctorAdd C m n).hom.app X))
      (CategoryTheory.CategoryStruct.comp ((F.shiftIso n a a' ha').hom.app ((CategoryTheory.shiftFunctor C m).obj X))
        ((F.shiftIso m a' a'' ha'').hom.app X))
-- Mathlib.AlgebraicTopology.SimplicialSet.Basic
SSet.Truncated.comp_app : ∀ {n : ℕ} {X Y Z : SSet.Truncated n} (f : X ⟶ Y) (g : Y ⟶ Z) (d : (SimplexCategory.Truncated n)ᵒᵖ),
  (CategoryTheory.CategoryStruct.comp f g).app d = CategoryTheory.CategoryStruct.comp (f.app d) (g.app d)
-- Mathlib.Order.Hom.WithTopBot
/-- Adjoins a `⊥` to the domain and codomain of an `InfHom`.  -/
InfHom.withBot : {α : Type u_1} →
  {β : Type u_2} → [inst : SemilatticeInf α] → [inst_1 : SemilatticeInf β] → InfHom α β → InfHom (WithBot α) (WithBot β)
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.eq_neg_cert.eq_1 : ∀ (p₁ p₂ : Lean.Grind.Linarith.Poly), Lean.Grind.Linarith.eq_neg_cert p₁ p₂ = (p₂ == p₁.mul (-1))
-- Mathlib.Data.Rat.Lemmas
/-- Denominator as `ℕ+`.  -/
Rat.pnatDen : ℚ → ℕ+
-- Mathlib.Data.Setoid.Partition
/-- Two equivalence relations are equal iff all their equivalence classes are equal.  -/
Setoid.eq_iff_classes_eq : ∀ {α : Type u_1} {r₁ r₂ : Setoid α}, r₁ = r₂ ↔ ∀ (x : α), {y | r₁ x y} = {y | r₂ x y}
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.isoZeroBiprod_hom : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y : C} [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y] (hY : CategoryTheory.Limits.IsZero X),
  (CategoryTheory.Limits.isoZeroBiprod hY).hom = CategoryTheory.Limits.biprod.inr
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.cont : ∀ {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [inst : Ring R] [inst_1 : AddCommGroup V]
  [inst_2 : Module R V] [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] [inst_5 : AddCommGroup W]
  [inst_6 : Module R W] [inst_7 : TopologicalSpace Q] [inst_8 : AddTorsor W Q] (self : P →ᴬ[R] Q),
  Continuous (↑self).toFun
-- Mathlib.Algebra.Polynomial.AlgebraMap
/-- Polynomial evaluation on an indexed tuple is the indexed tuple of the evaluations
on the components.
Generalizes `Polynomial.aeval_prod_apply` to indexed products.  -/
Polynomial.aeval_pi_apply : ∀ {R : Type u} [inst : CommSemiring R] {I : Type u_3} {A : I → Type u_4} [inst_1 : (i : I) → Semiring (A i)]
  [inst_2 : (i : I) → Algebra R (A i)] (x : (i : I) → A i) (p : Polynomial R),
  (Polynomial.aeval x) p = fun j => (Polynomial.aeval (x j)) p
-- Lean.Compiler.IR.Format
Lean.IR.instToStringFnBody : ToString Lean.IR.FnBody
-- Mathlib.LinearAlgebra.BilinearMap
/-- Bundled statement of bilinearity for a function.

The bundled type `E →ₗ[R] F →ₗ[R] G` should be preferred in cases where that can be used.
`IsBilinearMap` can be useful to have `IsBilinearMap (myFunction ..)` as a hypothesis to a
declaration.  -/
IsBilinearMap : (R : Type u_1) →
  [inst : CommSemiring R] →
    {E : Type u_2} →
      [inst_1 : AddCommMonoid E] →
        [Module R E] →
          {F : Type u_3} →
            [inst_3 : AddCommMonoid F] →
              [Module R F] → {G : Type u_4} → [inst_5 : AddCommMonoid G] → [Module R G] → (E → F → G) → Prop
-- Lean.Meta.DecLevel
Lean.Meta.DecLevelContext.mk.inj : ∀ {canAssignMVars canAssignMVars_1 : Bool},
  { canAssignMVars := canAssignMVars } = { canAssignMVars := canAssignMVars_1 } → canAssignMVars = canAssignMVars_1
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.RioSliceData.mk.sizeOf_spec : ∀ {α : Type u} [inst : Ord α] [inst_1 : SizeOf α] (treeMap : Std.DTreeMap.Internal.Impl α fun x => Unit)
  (range : Std.Rio α), sizeOf { treeMap := treeMap, range := range } = 1 + sizeOf treeMap + sizeOf range
-- Init.Data.String.Lemmas.Pattern.Char
String.Slice.Pattern.Model.Char.isLongestRevMatchAtChain_startPos_endPos_iff_toList : ∀ {c : Char} {s : String.Slice},
  String.Slice.Pattern.Model.IsLongestRevMatchAtChain c s.startPos s.endPos ↔
    s.copy.toList = List.replicate s.copy.toList.length c
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey?_minKeyD : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t ≠ ∅ → ∀ {fallback : α}, t.getKey? (t.minKeyD fallback) = some (t.minKeyD fallback)
-- Mathlib.Topology.OpenPartialHomeomorph.Constructions
OpenPartialHomeomorph.transHomeomorph_eq_trans : ∀ {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) (f' : Y ≃ₜ Z),
  e.transHomeomorph f' = e.trans f'.toOpenPartialHomeomorph
-- Std.Internal.Do.Order.Lemmas
Std.Internal.Do.CompleteLattice.join_self : ∀ {l : Type u} [inst : Lean.Order.CompleteLattice l] {P : l}, Lean.Order.join P P = P
-- Init.Data.List.Basic
/-- Compares lists lexicographically with respect to a comparison on their elements.

The lexicographic order with respect to `lt` is:
* `[].lex (b :: bs)` is `true`
* `as.lex [] = false` is `false`
* `(a :: as).lex (b :: bs)` is true if `lt a b` or `a == b` and `lex lt as bs` is true.
 -/
List.lex : {α : Type u} → [BEq α] → List α → List α → autoParam (α → α → Bool) List.lex._auto_1 → Bool
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.Pattern.Model.Pos.revSkipWhile_eq_self_iff : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [String.Slice.Pattern.Model.StrictPatternModel pat] [inst_2 : String.Slice.Pattern.BackwardPattern pat]
  [String.Slice.Pattern.Model.LawfulBackwardPatternModel pat] {s : String.Slice} {pos : s.Pos},
  pos.revSkipWhile pat = pos ↔ ¬String.Slice.Pattern.Model.RevMatchesAt pat pos
-- Mathlib.AlgebraicTopology.DoldKan.PInfty
AlgebraicTopology.DoldKan.PInfty_f_add_QInfty_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {X : CategoryTheory.SimplicialObject C} (n : ℕ),
  AlgebraicTopology.DoldKan.PInfty.f n + AlgebraicTopology.DoldKan.QInfty.f n =
    CategoryTheory.CategoryStruct.id ((AlgebraicTopology.AlternatingFaceMapComplex.obj X).X n)
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
ZeroAtInftyContinuousMap.toBCF_apply : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β] [inst_2 : Zero β]
  (f : ZeroAtInftyContinuousMap α β) (a : α), f.toBCF a = f a
-- Mathlib.CategoryTheory.Limits.Cones
/-- Change a cone on `F : Jᵒᵖ ⥤ C` to a cocone on `F.rightOp : Jᵒᵖ ⥤ C`.  -/
CategoryTheory.Limits.coconeRightOpOfCone : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor Jᵒᵖ C} → CategoryTheory.Limits.Cone F → CategoryTheory.Limits.Cocone F.rightOp
-- Lean.Environment
_private.Lean.Environment.0.Lean.importModulesCore.loadData : Lean.OLeanLevel →
  Lean.NameMap Lean.ImportArtifacts → Lean.Import → Lean.ImportStateM (Array (Lean.ModuleData × Lean.CompactedRegion))
-- Mathlib.MeasureTheory.Constructions.Polish.Basic
/-- Two sets `u` and `v` in a measurable space are measurably separable if there
exists a measurable set containing `u` and disjoint from `v`.
This is mostly interesting for Borel-separable sets.  -/
MeasureTheory.MeasurablySeparable : {α : Type u_3} → [MeasurableSpace α] → Set α → Set α → Prop
-- Init.Data.Array.Lemmas
Array.reverse.eq_1 : ∀ {α : Type u} (as : Array α), as.reverse = if h : as.size ≤ 1 then as else Array.reverse.loop as 0 ⟨as.size - 1, ⋯⟩
-- Init.Core
/-- The empty relation is the relation on `α` which is always `False`.  -/
emptyRelation : {α : Sort u} → α → α → Prop
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.ConjSqrt
CFC.ringInverse_conjSqrt : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : TopologicalSpace A]
  [inst_4 : StarOrderedRing A] [inst_5 : Algebra ℝ A] [inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
  [inst_7 : NonnegSpectrumClass ℝ A] [inst_8 : SeparatelyContinuousMul A] [IsSemitopologicalRing A] [T2Space A]
  (c a : A),
  autoParam (IsStrictlyPositive c) CFC.ringInverse_conjSqrt._auto_1 →
    Ring.inverse ((CFC.conjSqrt c) a) = (CFC.conjSqrt (Ring.inverse c)) (Ring.inverse a)
-- Mathlib.LinearAlgebra.TensorProduct.Opposite
Algebra.TensorProduct.opAlgEquiv_symm_apply : ∀ (R : Type u_1) (S : Type u_2) (A : Type u_3) (B : Type u_4) [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : Semiring A] [inst_3 : Semiring B] [inst_4 : Algebra R S] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  [inst_7 : Algebra S A] [inst_8 : IsScalarTower R S A] (x : (TensorProduct R A B)ᵐᵒᵖ),
  (Algebra.TensorProduct.opAlgEquiv R S A B).symm x =
    (TensorProduct.map ↑(MulOpposite.opLinearEquiv R) ↑(MulOpposite.opLinearEquiv R)) (MulOpposite.unop x)
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
HomotopicalAlgebra.PathObject.exists_very_good : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] (A : C),
  ∃ P, P.IsVeryGood
-- Lean.Meta.Tactic.Backtrack
_private.Lean.Meta.Tactic.Backtrack.0.Lean.Meta.Tactic.Backtrack.Backtrack.run.match_5.eq_2 : ∀ (motive : Option (List Lean.MVarId) → Sort u_1) (h_1 : (curr' : List Lean.MVarId) → motive (some curr'))
  (h_2 : Unit → motive none),
  (match none with
    | some curr' => h_1 curr'
    | none => h_2 ()) =
    h_2 ()
-- Mathlib.RingTheory.ChainOfDivisors
Associates.isAtom_iff : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [IsCancelMulZero M] {p : Associates M},
  p ≠ 0 → (IsAtom p ↔ Irreducible p)
-- Mathlib.Data.Tree.Basic
instReprBinaryTree.repr : {α : Type u_1} → [Repr α] → BinaryTree α → ℕ → Std.Format