mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Analytic.Basic
HasFPowerSeriesWithinOnBall.tendsto_partialSum : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ENNReal},
  HasFPowerSeriesWithinOnBall f p s x r →
    ∀ {y : E},
      y ∈ Metric.eball 0 r →
        x + y ∈ insert x s → Filter.Tendsto (fun n => p.partialSum n y) Filter.atTop (nhds (f (x + y)))
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.ins.match_3.splitter : {α : Type u_1} →
  (motive : RBTree.RBNode α → Sort u_2) →
    (x : RBTree.RBNode α) →
      (Unit → motive RBTree.RBNode.nil) →
        ((a : RBTree.RBNode α) →
            (y : α) → (b : RBTree.RBNode α) → motive (RBTree.RBNode.node RBTree.RBColor.red a y b)) →
          ((a : RBTree.RBNode α) →
              (y : α) → (b : RBTree.RBNode α) → motive (RBTree.RBNode.node RBTree.RBColor.black a y b)) →
            motive x
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Hom₂.left_unitor_inv.sizeOf_spec : ∀ {B : Type u} [inst : Quiver B] [inst_1 : SizeOf B] {a b : CategoryTheory.FreeBicategory B} (f : a ⟶ b),
  sizeOf (CategoryTheory.FreeBicategory.Hom₂.left_unitor_inv f) = 1 + sizeOf a + sizeOf b + sizeOf f
-- Mathlib.AlgebraicTopology.SingularHomology.Basic
AlgebraicTopology.instAdditiveFunctorTopCatChainComplexNatSingularChainComplexFunctor : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [inst_2 : CategoryTheory.Preadditive C], (AlgebraicTopology.singularChainComplexFunctor C).Additive
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.isMonHom_ofIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {M X : C}
  [inst_2 : CategoryTheory.MonObj M] (e : M ≅ X), CategoryTheory.IsMonHom e.hom
-- Init.Grind.Config
/-- If `trace` is `true`, `grind` records used E-matching theorems and case-splits.  -/
Lean.Grind.Config.trace : Lean.Grind.Config → Bool
-- Init.Data.Array.Lemmas
Array.mem_singleton_self : ∀ {α : Type u_1} (a : α), a ∈ #[a]
-- Mathlib.Analysis.Complex.UpperHalfPlane.Metric
UpperHalfPlane.image_coe_sphere : ∀ (z : UpperHalfPlane) (r : ℝ),
  UpperHalfPlane.coe '' Metric.sphere z r = Metric.sphere (↑(z.center r)) (z.im * Real.sinh r)
-- Mathlib.NumberTheory.Padics.Hensel
_private.Mathlib.NumberTheory.Padics.Hensel.0.a_is_soln : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : CommSemiring R] [inst_2 : Algebra R ℤ_[p]]
  {F : Polynomial R} {a : ℤ_[p]},
  ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2 →
    (Polynomial.aeval a) F = 0 →
      (Polynomial.aeval a) F = 0 ∧
        ‖a - a‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ∧
          ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ = ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ∧
            ∀ (z' : ℤ_[p]),
              (Polynomial.aeval z') F = 0 → ‖z' - a‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ → z' = a
-- Init.Data.UInt.Lemmas
UInt32.not_lt : ∀ {a b : UInt32}, ¬a < b ↔ b ≤ a
-- Mathlib.Data.EReal.Basic
EReal.coe_eq_coe_iff : ∀ {x y : ℝ}, ↑x = ↑y ↔ x = y
-- Mathlib.Analysis.Normed.Group.Int
Int.norm_cast_real : ∀ (m : ℤ), ‖↑m‖ = ‖m‖
-- Std.Data.HashMap.IteratorLemmas
Std.HashMap.Raw.toList_keysIter : ∀ {α β : Type u} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α],
  m.WF → m.keysIter.toList = m.keys
-- Mathlib.MeasureTheory.Measure.Prod
AEMeasurable.lintegral_prod_right' : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] {f : α × β → ENNReal},
  AEMeasurable f (μ.prod ν) → AEMeasurable (fun x => ∫⁻ (y : β), f (x, y) ∂ν) μ
-- Mathlib.Algebra.Group.Hom.Defs
/-- `M →ₙ+ N` denotes the type of addition-preserving maps from `M` to `N`.  -/
«term_→ₙ+_» : Lean.TrailingParserDescr
-- Aesop.Tree.Data
Aesop.NodeState.noConfusionType : Sort v✝ → Aesop.NodeState → Aesop.NodeState → Sort v✝
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.aeval_C : ∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] [inst_2 : Algebra R S₁]
  (f : σ → S₁) (r : R), (MvPolynomial.aeval f) (MvPolynomial.C r) = (algebraMap R S₁) r
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Iso.inv_hom_id_triangle_hom₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  {A B : CategoryTheory.Pretriangulated.Triangle C} (e : A ≅ B),
  CategoryTheory.CategoryStruct.comp e.inv.hom₂ e.hom.hom₂ = CategoryTheory.CategoryStruct.id B.obj₂
-- Mathlib.Analysis.Normed.Module.FiniteDimension
/-- If `K` is a compact set in a nontrivial real normed space and `x ∈ K`, then there exists a point
`y` of the boundary of `K` at distance `Metric.infDist x Kᶜ` from `x`. See also
`exists_mem_frontier_infDist_compl_eq_dist`.  -/
IsCompact.exists_mem_frontier_infDist_compl_eq_dist : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [NormedSpace ℝ E] [Nontrivial E] {x : E} {K : Set E},
  IsCompact K → x ∈ K → ∃ y ∈ frontier K, Metric.infDist x Kᶜ = dist x y
-- Mathlib.Analysis.SpecificLimits.Normed
not_summable_of_ratio_norm_eventually_ge : ∀ {α : Type u_4} [inst : SeminormedAddCommGroup α] {f : ℕ → α} {r : ℝ},
  1 < r → (∃ᶠ (n : ℕ) in Filter.atTop, ‖f n‖ ≠ 0) → (∀ᶠ (n : ℕ) in Filter.atTop, r * ‖f n‖ ≤ ‖f (n + 1)‖) → ¬Summable f
-- Mathlib.Algebra.Free
FreeSemigroup.ext : ∀ {α : Type u} {x y : FreeSemigroup α}, x.head = y.head → x.tail = y.tail → x = y
-- Init.Data.Int.Linear
Int.Internal.Linear.cooper_left_split_ineq_cert : Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → ℤ → ℤ → Int.Internal.Linear.Poly → Bool
-- Init.Omega.Constraint
Lean.Omega.normalize.eq_1 : ∀ (p : Lean.Omega.Constraint × Lean.Omega.Coeffs), Lean.Omega.normalize p = (Lean.Omega.normalize? p).getD p
-- Mathlib.CategoryTheory.Abelian.Preradical.Colon
CategoryTheory.Abelian.Preradical.shortComplex_X₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (Φ : CategoryTheory.Abelian.Preradical C), Φ.shortComplex.X₁ = Φ.r
-- Lean.Meta.SynthInstance
_private.Lean.Meta.SynthInstance.0.Lean.Meta.PreprocessResult.mk : Lean.Expr → Lean.Expr → Lean.Meta.PreprocessKind✝ → Lean.Meta.PreprocessResult✝
-- Lean.Data.Json.FromToJson.Basic
Lean.instFromJsonJsonNumber : Lean.FromJson Lean.JsonNumber
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F : C ⥤ Dᵒᵖ` creates colimits of `K.leftOp : Jᵒᵖ ⥤ C`, then `F.leftOp : Cᵒᵖ ⥤ D`
creates limits of `K : J ⥤ Cᵒᵖ`.  -/
CategoryTheory.Limits.createsLimitLeftOp : {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 : CategoryTheory.Functor J Cᵒᵖ) →
              (F : CategoryTheory.Functor C Dᵒᵖ) →
                [CategoryTheory.CreatesColimit K.leftOp F] → CategoryTheory.CreatesLimit K F.leftOp
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.isCoseparator_unop_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (G : Cᵒᵖ),
  CategoryTheory.IsCoseparator (Opposite.unop G) ↔ CategoryTheory.IsSeparator G
-- Mathlib.LinearAlgebra.UnitaryGroup
/-- `Matrix.unitaryGroup n` is the group of `n` by `n` matrices where the star-transpose is the
inverse.
 -/
Matrix.unitaryGroup : (n : Type u) →
  [inst : DecidableEq n] →
    [inst_1 : Fintype n] → (α : Type v) → [inst_2 : CommRing α] → [StarRing α] → Submonoid (Matrix n n α)
-- Mathlib.Order.SuccPred.Basic
Order.Icc_pred_left : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : PredOrder α] {a b : α},
  Order.pred b ≤ a → Set.Icc (Order.pred b) a = insert (Order.pred b) (Set.Icc b a)
-- Lean.Meta.Basic
Lean.Meta.instInhabitedConfig : Inhabited Lean.Meta.Config
-- Mathlib.Analysis.Normed.Module.RCLike.Basic
/-- Lemma to normalize a vector in a normed space `E` over either `ℂ` or `ℝ` to length `r`.  -/
norm_smul_inv_norm' : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {r : ℝ},
  0 ≤ r → ∀ {x : E}, x ≠ 0 → ‖(↑r * (↑‖x‖)⁻¹) • x‖ = r
-- Mathlib.Data.Ordmap.Ordnode
/-- Convert to an `OrdNode` by pre-computing the sizes.  -/
BinaryTree.toOrdNode : {α : Type u_1} → BinaryTree α → Ordnode α
-- Mathlib.Analysis.Calculus.ContDiff.Defs
ContDiffOn.differentiableOn_one : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F}, ContDiffOn 𝕜 1 f s → DifferentiableOn 𝕜 f s
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.mapAddMon_obj_X : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.LaxMonoidal] (A : CategoryTheory.AddMon C),
  (F.mapAddMon.obj A).X = F.obj A.X
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
le_add_iff_nonneg_right : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : LE α] [AddLeftMono α] [AddLeftReflectLE α] (a : α) {b : α},
  a ≤ a + b ↔ 0 ≤ b
-- Mathlib.Topology.Algebra.Group.Basic
map_add_left_nhds : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [IsTopologicalAddGroup G] (x y : G),
  Filter.map (fun x_1 => x + x_1) (nhds y) = nhds (x + y)
-- Mathlib.Data.EReal.Inv
EReal.div_nonpos_of_nonpos_of_nonneg : ∀ {a b : EReal}, a ≤ 0 → 0 ≤ b → a / b ≤ 0
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.coe_mul : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : Mul Y] (f g : LocallyConstant X Y),
  ⇑(f * g) = ⇑f * ⇑g
-- Mathlib.Algebra.Homology.BifunctorAssociator
HomologicalComplex.mapBifunctor₁₂.D₂.congr_simp : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₃ : Type u_5} {C₄ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_5} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_6} C₄]
  [inst_4 : CategoryTheory.Category.{v_5, u_3} C₁₂] [inst_5 : CategoryTheory.Limits.HasZeroMorphisms C₁]
  [inst_6 : CategoryTheory.Limits.HasZeroMorphisms C₂] [inst_7 : CategoryTheory.Limits.HasZeroMorphisms C₃]
  [inst_8 : CategoryTheory.Preadditive C₁₂] [inst_9 : CategoryTheory.Preadditive C₄]
  (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂))
  (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) [inst_10 : F₁₂.PreservesZeroMorphisms]
  [inst_11 : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [inst_12 : G.Additive]
  [inst_13 : ∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9}
  {ι₁₂ : Type u_10} {ι₄ : Type u_12} [inst_14 : DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃)
  (c₁₂ : ComplexShape ι₁₂) (c₄ : ComplexShape ι₄) [inst_15 : TotalComplexShape c₁ c₂ c₁₂]
  [inst_16 : TotalComplexShape c₁₂ c₃ c₄] [inst_17 : K₁.HasMapBifunctor K₂ F₁₂ c₁₂] [inst_18 : DecidableEq ι₁₂]
  [inst_19 : (K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄]
  [inst_20 : HomologicalComplex.HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄] (j j' : ι₄),
  HomologicalComplex.mapBifunctor₁₂.D₂ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ j j' =
    HomologicalComplex.mapBifunctor₁₂.D₂ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ j j'
-- Mathlib.Algebra.MonoidAlgebra.Degree
AddMonoidAlgebra.supDegree_single : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_5} [inst : Semiring R] [inst_1 : SemilatticeSup B] [inst_2 : OrderBot B]
  {D : A → B} (a : A) (r : R), AddMonoidAlgebra.supDegree D (AddMonoidAlgebra.single a r) = if r = 0 then ⊥ else D a
-- Mathlib.Topology.Semicontinuity.Defs
/-- **Alias** of the reverse direction of `lowerHemicontinuousAt_iff_frequently`. -/
LowerHemicontinuousAt.of_frequently : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → Set β} {x : α},
  (∀ (t : Set β), IsClosed t → (∃ᶠ (x' : α) in nhds x, f x' ⊆ t) → f x ⊆ t) → LowerHemicontinuousAt f x
-- Mathlib.Algebra.FreeMonoid.FreeSemigroup
FreeAddMonoid.equivWithZeroFreeAddSemigroup_symm_apply : ∀ {α : Type u_1} (a : WithZero (FreeAddSemigroup α)),
  FreeAddMonoid.equivWithZeroFreeAddSemigroup.symm a = (WithZero.lift FreeAddSemigroup.toFreeAddMonoid) a
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
/-- Lower bound on the edge densities between non-uniform parts of `SzemerediRegularity.star`.  -/
_private.Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk.0.SzemerediRegularity.edgeDensity_star_not_uniform : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {P : Finpartition Finset.univ} {hP : P.IsEquipartition}
  {G : SimpleGraph α} [inst_2 : DecidableRel G.Adj] {ε : ℝ} {U V : Finset α} [Nonempty α],
  P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α →
    100 ≤ 4 ^ P.parts.card * ε ^ 5 →
      ε ≤ 1 →
        ∀ {hU : U ∈ P.parts} {hV : V ∈ P.parts},
          U ≠ V →
            ¬G.IsUniform ε U V →
              3 / 4 * ε ≤
                |(∑ ab ∈ (SzemerediRegularity.star hP G ε hU V).product (SzemerediRegularity.star hP G ε hV U),
                        ↑(G.edgeDensity ab.1 ab.2)) /
                      (↑(SzemerediRegularity.star hP G ε hU V).card * ↑(SzemerediRegularity.star hP G ε hV U).card) -
                    (∑
                        ab ∈
                          (SzemerediRegularity.chunk hP G ε hU).parts.product
                            (SzemerediRegularity.chunk hP G ε hV).parts,
                        ↑(G.edgeDensity ab.1 ab.2)) /
                      16 ^ P.parts.card|
-- Std.Data.DHashMap.Internal.AssocList.Iterator
_private.Std.Data.DHashMap.Internal.AssocList.Iterator.0.Std.DHashMap.Internal.AssocList.instIteratorAssocListIteratorIdSigma.match_3.eq_1 : ∀ {α : Type u_2} {β : α → Type u_1} (motive : Std.IterM Id ((a : α) × β a) → Sort u_3)
  (h_1 : Unit → motive { internalState := { l := Std.DHashMap.Internal.AssocList.nil } })
  (h_2 :
    (k : α) →
      (v : β k) →
        (l : Std.DHashMap.Internal.AssocList α β) →
          motive { internalState := { l := Std.DHashMap.Internal.AssocList.cons k v l } }),
  (match { internalState := { l := Std.DHashMap.Internal.AssocList.nil } } with
    | { internalState := { l := Std.DHashMap.Internal.AssocList.nil } } => h_1 ()
    | { internalState := { l := Std.DHashMap.Internal.AssocList.cons k v l } } => h_2 k v l) =
    h_1 ()
-- Lean.Parser.Types
Lean.Parser.InputContext.inputString : Lean.Parser.InputContext → String
-- Mathlib.Algebra.CubicDiscriminant
Cubic.natDegree_of_b_eq_zero' : ∀ {R : Type u_1} {c d : R} [inst : Semiring R], { a := 0, b := 0, c := c, d := d }.toPoly.natDegree ≤ 1
-- Mathlib.Topology.LocallyConstant.Basic
IsLocallyConstant.add : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : Add Y] ⦃f g : X → Y⦄,
  IsLocallyConstant f → IsLocallyConstant g → IsLocallyConstant (f + g)
-- Mathlib.LinearAlgebra.BilinearForm.Properties
LinearMap.BilinForm.apply_toDual_symm_apply : ∀ {V : Type u_5} {K : Type u_6} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [inst_3 : FiniteDimensional K V] {B : LinearMap.BilinForm K V} {hB : B.Nondegenerate} (f : Module.Dual K V) (v : V),
  (B ((B.toDual hB).symm f)) v = f v
-- Mathlib.CategoryTheory.Monoidal.Grp
/-- The image of a group object under a monoidal functor is a group object.  -/
CategoryTheory.Functor.grpObjObj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.CartesianMonoidalCategory D] →
            {F : CategoryTheory.Functor C D} →
              [F.Monoidal] → {G : C} → [CategoryTheory.GrpObj G] → CategoryTheory.GrpObj (F.obj G)
-- Mathlib.RingTheory.HopfAlgebra.MonoidAlgebra
LaurentPolynomial.instHopfAlgebra : (R : Type u_1) →
  (A : Type u_2) →
    [inst : CommSemiring R] → [inst_1 : Semiring A] → [HopfAlgebra R A] → HopfAlgebra R (LaurentPolynomial A)
-- Mathlib.Algebra.Group.Prod
Units.embedProduct_apply : ∀ (α : Type u_6) [inst : Monoid α] (x : αˣ), (Units.embedProduct α) x = (↑x, MulOpposite.op ↑x⁻¹)
-- Mathlib.AlgebraicGeometry.Morphisms.Proper
AlgebraicGeometry.IsProper.instIsMultiplicativeScheme : CategoryTheory.MorphismProperty.IsMultiplicative @AlgebraicGeometry.IsProper
-- Mathlib.Topology.EMetricSpace.PairReduction
PairReduction.card_finset_logSizeBallSeq_add_one_lt : ∀ {T : Type u_1} [inst : PseudoEMetricSpace T] {a c : ENNReal} {J : Finset T} [inst_1 : DecidableEq T] (hJ : J.Nonempty)
  (i : ℕ),
  (PairReduction.logSizeBallSeq J hJ a c i).finset.Nonempty →
    (PairReduction.logSizeBallSeq J hJ a c (i + 1)).finset.card < (PairReduction.logSizeBallSeq J hJ a c i).finset.card
-- Mathlib.Data.Set.Prod
Set.Disjoint.set_prod_left : ∀ {α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α}, Disjoint s₁ s₂ → ∀ (t₁ t₂ : Set β), Disjoint (s₁ ×ˢ t₁) (s₂ ×ˢ t₂)
-- Mathlib.Analysis.Normed.Field.Lemmas
Rat.instDenselyNormedField : DenselyNormedField ℚ
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
WeierstrassCurve.Projective.map_polynomialZ : ∀ {R : Type r} [inst : CommRing R] (W' : WeierstrassCurve.Projective R) {S : Type s} [inst_1 : CommRing S]
  (f : R →+* S), (W'.map f).polynomialZ = (MvPolynomial.map f) W'.polynomialZ
-- Mathlib.Topology.Compactness.SigmaCompact
Topology.IsClosedEmbedding.sigmaCompactSpace : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [SigmaCompactSpace X]
  {e : Y → X}, Topology.IsClosedEmbedding e → SigmaCompactSpace Y
-- Mathlib.Data.Num.Bitwise
/-- Add an active bit at the end of a `SNum`. This mimics `ZNum.bit1`.  -/
SNum.bit1 : SNum → SNum
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Poly.denote_eq_cancel : ∀ {ctx : Nat.Internal.Linear.Context} {m₁ m₂ : Nat.Internal.Linear.Poly},
  Nat.Internal.Linear.Poly.denote_eq ctx (m₁, m₂) → Nat.Internal.Linear.Poly.denote_eq ctx (m₁.cancel m₂)
-- Mathlib.Topology.Bases
/-- If `α` is a separable space and `f : α → β` is a continuous map with dense range, then `β` is
a separable space as well. E.g., the completion of a separable uniform space is separable.  -/
DenseRange.separableSpace : ∀ {α : Type u} {β : Type u_1} [t : TopologicalSpace α] [TopologicalSpace.SeparableSpace α] [inst : TopologicalSpace β]
  {f : α → β}, DenseRange f → Continuous f → TopologicalSpace.SeparableSpace β
-- Mathlib.Data.Nat.Choose.Basic
Nat.choose.eq_def : ∀ (x x_1 : ℕ),
  x.choose x_1 =
    match x, x_1 with
    | x, 0 => 1
    | 0, n.succ => 0
    | n.succ, k.succ => n.choose k + n.choose (k + 1)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.addX_eq' : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} {P Q : Fin 3 → R},
  W'.Equation P →
    W'.Equation Q →
      W'.addX P Q * (P 2 * Q 2) ^ 2 =
        ((P 1 * Q 2 - Q 1 * P 2) ^ 2 * P 2 * Q 2 +
                  W'.a₁ * (P 1 * Q 2 - Q 1 * P 2) * P 2 * Q 2 * (P 0 * Q 2 - Q 0 * P 2) -
                W'.a₂ * P 2 * Q 2 * (P 0 * Q 2 - Q 0 * P 2) ^ 2 -
              P 0 * Q 2 * (P 0 * Q 2 - Q 0 * P 2) ^ 2 -
            Q 0 * P 2 * (P 0 * Q 2 - Q 0 * P 2) ^ 2) *
          (P 0 * Q 2 - Q 0 * P 2)
-- Mathlib.Order.Closure
ClosureOperator.instInhabited : (α : Type u_1) → [inst : Preorder α] → Inhabited (ClosureOperator α)
-- Mathlib.LinearAlgebra.Matrix.ToLin
/-- `dotProduct` as a bilinear map.

When `A` is noncommutative, `R` and `S` can be instantiated as `dotProductBilin A Aᵐᵒᵖ`.  -/
dotProductBilin : {m : Type u_2} →
  (R : Type u_4) →
    (S : Type u_5) →
      {A : Type u_6} →
        [inst : Semiring R] →
          [inst_1 : Semiring S] →
            [inst_2 : NonUnitalNonAssocSemiring A] →
              [inst_3 : Module R A] →
                [inst_4 : Module S A] →
                  [inst_5 : SMulCommClass S R A] →
                    [SMulCommClass S A A] → [IsScalarTower R A A] → [Fintype m] → (m → A) →ₗ[R] (m → A) →ₗ[S] A
-- Mathlib.NumberTheory.KummerDedekind
KummerDedekind.quotMapEquivQuotQuotMap.eq_1 : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {x : S} {I : Ideal R}
  [inst_3 : IsDomain R] [inst_4 : IsIntegrallyClosed R] [inst_5 : IsDedekindDomain S]
  [inst_6 : Module.IsTorsionFree R S] (hx : Ideal.comap (algebraMap R S) (conductor R x) ⊔ I = ⊤)
  (hx' : IsIntegral R x),
  KummerDedekind.quotMapEquivQuotQuotMap hx hx' =
    (quotAdjoinEquivQuotMap hx ⋯).symm.trans
      (((Algebra.adjoin.powerBasis' hx').quotientEquivQuotientMinpolyMap I).toRingEquiv.trans (Ideal.quotEquivOfEq ⋯))
-- Mathlib.Analysis.Calculus.ContDiff.Convolution
/-- The convolution `f * g` is `C^n` when `f` is locally integrable and `g` is `C^n` and compactly
supported. Version where `g` depends on an additional parameter in an open subset `s` of a
parameter space `P` (and the compact support `k` is independent of the parameter in `s`),
given in terms of composition with an additional `C^n` function.  -/
MeasureTheory.contDiffOn_convolution_right_with_param_comp : ∀ {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {P : Type uP} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup E'] [inst_2 : NormedAddCommGroup F] [inst_3 : RCLike 𝕜] [inst_4 : NormedSpace 𝕜 E]
  [inst_5 : NormedSpace 𝕜 E'] [inst_6 : NormedSpace ℝ F] [inst_7 : NormedSpace 𝕜 F] [inst_8 : MeasurableSpace G]
  [inst_9 : NormedAddCommGroup G] [BorelSpace G] [inst_11 : NormedSpace 𝕜 G] [inst_12 : NormedAddCommGroup P]
  [inst_13 : NormedSpace 𝕜 P] {μ : MeasureTheory.Measure G} {n : ℕ∞} (L : E →L[𝕜] E' →L[𝕜] F) {s : Set P} {v : P → G},
  ContDiffOn 𝕜 (↑n) v s →
    ∀ {f : G → E} {g : P → G → E'} {k : Set G},
      IsOpen s →
        IsCompact k →
          (∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0) →
            MeasureTheory.LocallyIntegrable f μ →
              ContDiffOn 𝕜 (↑n) (↿g) (s ×ˢ Set.univ) →
                ContDiffOn 𝕜 (↑n) (fun x => MeasureTheory.convolution f (g x) L μ (v x)) s
-- Mathlib.LinearAlgebra.Dual.Lemmas
Module.instIsReflexiveOfFiniteOfProjective : ∀ (R : Type u_1) (N : Type u_3) [inst : CommSemiring R] [inst_1 : AddCommMonoid N] [inst_2 : Module R N]
  [Module.Finite R N] [Module.Projective R N], Module.IsReflexive R N
-- Lean.PrettyPrinter.Delaborator.Basic
Lean.PrettyPrinter.Delaborator.OmissionReason.proof.sizeOf_spec : sizeOf Lean.PrettyPrinter.Delaborator.OmissionReason.proof = 1
-- Mathlib.Analysis.Matrix.Normed
Matrix.linfty_opNorm_replicateRow : ∀ {n : Type u_4} {α : Type u_5} {ι : Type u_7} [inst : Fintype n] [inst_1 : Unique ι]
  [inst_2 : SeminormedAddCommGroup α] (v : n → α), ‖Matrix.replicateRow ι v‖ = ∑ i, ‖v i‖
-- Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
HurwitzKernelBounds.F_int.eq_1 : ∀ (k : ℕ) (a : UnitAddCircle) (t : ℝ), HurwitzKernelBounds.F_int k a t = ⋯.lift a
-- Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
integrable_mul_exp_neg_mul_sq : ∀ {b : ℝ}, 0 < b → MeasureTheory.Integrable (fun x => x * Real.exp (-b * x ^ 2)) MeasureTheory.volume
-- Mathlib.Order.Filter.Extr
IsExtrOn.neg : ∀ {α : Type u} {β : Type v} [inst : AddCommGroup β] [inst_1 : PartialOrder β] [IsOrderedAddMonoid β] {f : α → β} {a : α}
  {s : Set α}, IsExtrOn f s a → IsExtrOn (fun x => -f x) s a