mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Polynomial.RuleOfSigns
/-- **Descartes' Rule of Signs**: the number of positive roots is at most the number of sign
variations.  -/
Polynomial.roots_countP_pos_le_signVariations : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : LinearOrder R] [inst_2 : IsStrictOrderedRing R] (P : Polynomial R),
  Multiset.countP (fun x => 0 < x) P.roots ≤ P.signVariations
-- Init.Data.Int.DivMod.Lemmas
Int.ediv_neg_of_neg_of_pos : ∀ {a b : ℤ}, a < 0 → 0 < b → a / b < 0
-- Aesop.Script.StructureDynamic
Aesop.Script.DynStructureM.Context.mk.sizeOf_spec : ∀ (steps : Lean.PHashMap Lean.MVarId (ℕ × Aesop.Script.Step)), sizeOf { steps := steps } = 1 + sizeOf steps
-- Mathlib.Analysis.Normed.Module.WeakDual
/-- By the Uniform Boundedness Principle, norm-boundedness (the default bornology)
and pointwise-boundedness (`IsVonNBounded`) coincide on the weak dual of a Banach space.  -/
WeakDual.isBounded_iff_isVonNBounded : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [CompleteSpace E] {s : Set (WeakDual 𝕜 E)},
  Bornology.IsBounded s ↔ Bornology.IsVonNBounded 𝕜 s
-- Mathlib.Topology.MetricSpace.UniformConvergence
/-- Let `f : γ → α →ᵤ[𝔖] β`. If for every `s ∈ 𝔖` and for every `c ∈ s`, the function
`fun x ↦ f x c` is Lipschitz (with Lipschitz constant depending on `s`), then `f` is continuous.  -/
UniformOnFun.continuous_of_forall_lipschitzWith : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : PseudoEMetricSpace γ] {𝔖 : Set (Set α)}
  [inst_1 : PseudoEMetricSpace β] {f : γ → UniformOnFun α β 𝔖} (K : Set α → NNReal),
  (∀ s ∈ 𝔖, ∀ c ∈ s, LipschitzWith (K s) fun x => (UniformOnFun.toFun 𝔖) (f x) c) → Continuous f
-- Mathlib.Order.InitialSeg
PrincipalSeg.surjOn : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : PrincipalSeg r s),
  Set.SurjOn (⇑f.toRelEmbedding) Set.univ {b | s b f.top}
-- Mathlib.Algebra.Group.Submonoid.MulAction
Submonoid.instMulActionSubtypeMem : {M' : Type u_1} →
  {α : Type u_2} →
    {S' : Type u_4} →
      [inst : SetLike S' M'] →
        (s : S') → [inst_1 : Monoid M'] → [inst_2 : SubmonoidClass S' M'] → [MulAction M' α] → MulAction (↥s) α
-- Mathlib.Analysis.Analytic.CPolynomialDef
HasFiniteFPowerSeriesAt.continuousAt : ∀ {𝕜 : 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} {x : E} {n : ℕ}, HasFiniteFPowerSeriesAt f p x n → ContinuousAt f x
-- Mathlib.MeasureTheory.Integral.Average
MeasureTheory.toReal_setLAverage : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {f : α → ENNReal},
  AEMeasurable f (μ.restrict s) →
    (∀ᵐ (x : α) ∂μ.restrict s, f x ≠ ⊤) → (⨍⁻ (x : α) in s, f x ∂μ).toReal = ⨍ (x : α) in s, (f x).toReal ∂μ
-- Mathlib.Algebra.Order.Antidiag.Prod
Finset.HasMulAntidiagonal.sigmaMulAntidiagonalEquivProd.eq_1 : ∀ {A : Type u_1} [inst : Monoid A] [inst_1 : Finset.HasMulAntidiagonal A],
  Finset.HasMulAntidiagonal.sigmaMulAntidiagonalEquivProd =
    { toFun := fun x => ↑x.snd, invFun := fun x => ⟨x.1 * x.2, ⟨x, ⋯⟩⟩, left_inv := ⋯, right_inv := ⋯ }
-- Init.Data.AC
_private.Init.Data.AC.0.Lean.Data.AC.removeNeutrals.loop.match_3.eq_1 : ∀ (motive : List ℕ → Sort u_1) (x : ℕ) (xs : List ℕ) (h_1 : (x : ℕ) → (xs : List ℕ) → motive (x :: xs))
  (h_2 : Unit → motive []),
  (match x :: xs with
    | x :: xs => h_1 x xs
    | [] => h_2 ()) =
    h_1 x xs
-- Mathlib.Data.Fintype.Quotient
Quotient.finLiftOn_empty : ∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] {α : ι → Sort u_2} {S : (i : ι) → Setoid (α i)}
  {β : Sort u_3} [e : IsEmpty ι] (q : (i : ι) → Quotient (S i)), Quotient.finLiftOn q = fun f x => f fun a => e.elim a
-- Mathlib.Algebra.Category.ModuleCat.Sheaf
/-- The forget functor `SheafOfModules R ⥤ Sheaf J AddCommGrpCat`.  -/
SheafOfModules.toSheaf : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      (R : CategoryTheory.Sheaf J RingCat) →
        CategoryTheory.Functor (SheafOfModules R) (CategoryTheory.Sheaf J AddCommGrpCat)
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.haar.prehaar_sup_le : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G]
  {K₀ : TopologicalSpace.PositiveCompacts G} {U : Set G} (K₁ K₂ : TopologicalSpace.Compacts G),
  (interior U).Nonempty →
    MeasureTheory.Measure.haar.prehaar (↑K₀) U (K₁ ⊔ K₂) ≤
      MeasureTheory.Measure.haar.prehaar (↑K₀) U K₁ + MeasureTheory.Measure.haar.prehaar (↑K₀) U K₂
-- Init.Data.BitVec.Lemmas
BitVec.ofNatLT_finVal : ∀ {w : ℕ} (n : Fin (2 ^ w)), (↑n)#'⋯ = { toFin := n }
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
/-- `Prod.fst` as an `AffineMap`.  -/
AffineMap.fst : {k : Type u_1} →
  {V1 : Type u_2} →
    {P1 : Type u_3} →
      {V2 : Type u_4} →
        {P2 : Type u_5} →
          [inst : Ring k] →
            [inst_1 : AddCommGroup V1] →
              [inst_2 : Module k V1] →
                [inst_3 : AddTorsor V1 P1] →
                  [inst_4 : AddCommGroup V2] → [inst_5 : Module k V2] → [inst_6 : AddTorsor V2 P2] → P1 × P2 →ᵃ[k] P1
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.Equiv.trans : ∀ {α : Type u} {m₁ m₂ m₃ : Std.HashSet.Raw α}, m₁.Equiv m₂ → m₂.Equiv m₃ → m₁.Equiv m₃
-- Mathlib.Order.Interval.Set.ProjIcc
Set.IccExtend_val : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] {a b : α} (h : a ≤ b) (f : ↑(Set.Icc a b) → β)
  (x : ↑(Set.Icc a b)), Set.IccExtend h f ↑x = f x
-- Mathlib.Algebra.Lie.Extension
LieAlgebra.Extension.bracket : ∀ {R : Type u_1} {L : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : LieRing M] [inst_4 : LieAlgebra R M] [inst_5 : IsLieAbelian M] [inst_6 : LieRingModule L M]
  [inst_7 : LieModule R L M] (c : ↥(LieModule.Cohomology.twoCocycle R L M))
  (x y : (LieAlgebra.Extension.ofTwoCocycle c).L),
  ⁅x, y⁆ = (LieAlgebra.Extension.ofAlg c) ⁅(LieAlgebra.Extension.ofAlg c).symm x, (LieAlgebra.Extension.ofAlg c).symm y⁆
-- Mathlib.MeasureTheory.Function.LpSpace.Indicator
/-- A family of `indicatorConstLp` functions is continuous in the parameter,
if `μ (s y ∆ s x)` tends to zero as `y` tends to `x` for all `x`.  -/
MeasureTheory.continuous_indicatorConstLp_set : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] {c : E} [inst_1 : Fact (1 ≤ p)] {X : Type u_3} [inst_2 : TopologicalSpace X]
  {s : X → Set α} {hs : ∀ (x : X), MeasurableSet (s x)} {hμs : ∀ (x : X), μ (s x) ≠ ⊤},
  p ≠ ⊤ →
    (∀ (x : X), Filter.Tendsto (fun y => μ (symmDiff (s y) (s x))) (nhds x) (nhds 0)) →
      Continuous fun x => MeasureTheory.indicatorConstLp p ⋯ ⋯ c
-- Lean.Elab.Tactic.Basic
Lean.Elab.Tactic.instOrElseTacticM : {α : Type} → OrElse (Lean.Elab.Tactic.TacticM α)
-- Mathlib.Order.SuccPred.Archimedean
monotoneOn_of_le_succ : ∀ {α : Type u_3} {β : Type u_4} [inst : PartialOrder α] [inst_1 : Preorder β] [inst_2 : SuccOrder α]
  [IsSuccArchimedean α] {s : Set α} {f : α → β},
  s.OrdConnected → (∀ (a : α), ¬IsMax a → a ∈ s → Order.succ a ∈ s → f a ≤ f (Order.succ a)) → MonotoneOn f s
-- Mathlib.Order.Filter.Basic
Filter.eventually_false_iff_eq_bot : ∀ {α : Type u} {f : Filter α}, (∀ᶠ (x : α) in f, False) ↔ f = ⊥
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.foldl_eq_foldl_keys : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} {δ : Type w}
  [inst : Std.TransCmp cmp] {f : δ → α → δ} {init : δ},
  Std.ExtDTreeMap.foldl (fun d a x => f d a) init t = List.foldl f init t.keys
-- Mathlib.CategoryTheory.ComposableArrows.Basic
/-- Constructor for isomorphisms in `ComposableArrows C 1`.  -/
CategoryTheory.ComposableArrows.isoMk₁ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {F G : CategoryTheory.ComposableArrows C 1} →
      (left :
          F.obj' 0 CategoryTheory.ComposableArrows.homMk₁._proof_4 ≅
            G.obj' 0 CategoryTheory.ComposableArrows.homMk₁._proof_4) →
        (right :
            F.obj' 1 CategoryTheory.ComposableArrows.homMk₁._proof_5 ≅
              G.obj' 1 CategoryTheory.ComposableArrows.homMk₁._proof_5) →
          autoParam
              (CategoryTheory.CategoryStruct.comp
                  (F.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4
                    CategoryTheory.ComposableArrows.homMk₁._proof_5)
                  right.hom =
                CategoryTheory.CategoryStruct.comp left.hom
                  (G.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4
                    CategoryTheory.ComposableArrows.homMk₁._proof_5))
              CategoryTheory.ComposableArrows.isoMk₁._auto_1 →
            (F ≅ G)
-- Lean.Compiler.IR.Basic
Lean.IR.instInhabitedFnBody : Inhabited Lean.IR.FnBody
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.instIsOrderedRing : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P],
  IsOrderedRing (FractionalIdeal S P)
-- Mathlib.Data.Fintype.Card
Fintype.card_fin : ∀ (n : ℕ), Fintype.card (Fin n) = n
-- Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
/-- The mapping cone of the identity is contractible.  -/
CochainComplex.mappingCone.homotopyToZeroOfId : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] →
        (K : CochainComplex C ℤ) →
          Homotopy (CategoryTheory.CategoryStruct.id (CochainComplex.mappingCone (CategoryTheory.CategoryStruct.id K)))
            0
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.congrLeftₗ_symm_apply : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : AddCommGroup V₂] [inst_3 : Module k V₁] [inst_4 : Module k V₂]
  [inst_5 : AddTorsor V₁ P₁] [inst_6 : AddTorsor V₂ P₂] (R : Type u_10) (W : Type u_11) [inst_7 : Ring R]
  [inst_8 : AddCommGroup W] [inst_9 : Module k W] [inst_10 : Module R W] [inst_11 : SMulCommClass k R W]
  (e : P₁ ≃ᵃ[k] P₂) (f : P₂ →ᵃ[k] W) (x : P₁), ((AffineEquiv.congrLeftₗ R W e).symm f) x = f (e x)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.isEmpty_inter_iff : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ((m₁ ∩ m₂).isEmpty = true ↔ ∀ k ∈ m₁, k ∉ m₂)
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Map
CategoryTheory.Functor.mapExtAddHom_coe : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {D : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} D] [inst_3 : CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D)
  [inst_4 : F.Additive] [inst_5 : CategoryTheory.Limits.PreservesFiniteLimits F]
  [inst_6 : CategoryTheory.Limits.PreservesFiniteColimits F] [inst_7 : CategoryTheory.HasExt C]
  [inst_8 : CategoryTheory.HasExt D] (X Y : C) (n : ℕ),
  ⇑(F.mapExtAddHom X Y n) = CategoryTheory.Abelian.Ext.mapExactFunctor F
-- Mathlib.RingTheory.Extension.Basic
Algebra.Extension.ker_infinitesimal : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.Extension R S), P.infinitesimal.ker = P.ker.cotangentIdeal
-- Mathlib.Algebra.Group.Defs
_private.Mathlib.Algebra.Group.Defs.0.npowRec.match_1.eq_2 : ∀ {M : Type u_2} (motive : ℕ → M → Sort u_1) (n : ℕ) (a : M) (h_1 : (x : M) → motive 0 x)
  (h_2 : (n : ℕ) → (a : M) → motive n.succ a),
  (match n.succ, a with
    | 0, x => h_1 x
    | n.succ, a => h_2 n a) =
    h_2 n a
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.coeff_sub : ∀ {R : Type u_1} [inst : Ring R] (p q : SkewPolynomial R) (n : ℕ), (p - q).coeff n = p.coeff n - q.coeff n
-- Mathlib.RingTheory.Localization.BaseChange
/-- If `A` is a localization of `R`, tensoring two `A`-algebras over `A` is the same as
tensoring them over `R`.  -/
IsLocalization.algebraTensorEquiv : {R : Type u_1} →
  [inst : CommSemiring R] →
    (S : Submonoid R) →
      (A : Type u_2) →
        [inst_1 : CommSemiring A] →
          [inst_2 : Algebra R A] →
            [IsLocalization S A] →
              (B : Type u_5) →
                (C : Type u_6) →
                  [inst_4 : Semiring B] →
                    [inst_5 : Algebra R B] →
                      [inst_6 : Algebra A B] →
                        [inst_7 : IsScalarTower R A B] →
                          [inst_8 : Semiring C] →
                            [inst_9 : Algebra R C] →
                              [inst_10 : Algebra A C] →
                                [IsScalarTower R A C] → TensorProduct A B C ≃ₐ[A] TensorProduct R B C
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.instGroup : {α : Type u_1} →
  {γ : Type u_3} →
    [inst : MeasurableSpace α] →
      {μ : MeasureTheory.Measure α} →
        [inst_1 : TopologicalSpace γ] → [inst_2 : Group γ] → [IsTopologicalGroup γ] → Group (α →ₘ[μ] γ)
-- Batteries.Data.String.Legacy
_private.Batteries.Data.String.Legacy.0.String.utf8ByteSize'.go.match_1.splitter : (motive : List Char → Sort u_1) →
  (x : List Char) → (Unit → motive []) → ((c : Char) → (cs : List Char) → motive (c :: cs)) → motive x
-- Mathlib.LinearAlgebra.RootSystem.Base
RootPairing.Base.height_reflectionPerm_self : ∀ {ι : 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] {P : RootPairing ι R M N} (b : P.Base)
  [inst_5 : CharZero R] (i : ι), b.height (-i) = -b.height i
-- Mathlib.Data.List.Sublists
List.sublists_concat : ∀ {α : Type u} (l : List α) (a : α), (l ++ [a]).sublists = l.sublists ++ List.map (fun x => x ++ [a]) l.sublists
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equifibered
/-- **Alias** of `CategoryTheory.NatTrans.Equifibered.of_discrete`. -/
CategoryTheory.mapPair_equifibered : ∀ {C : Type u_3} {ι : Type u_5} [inst : CategoryTheory.Category.{v_2, u_3} C]
  {F G : CategoryTheory.Functor (CategoryTheory.Discrete ι) C} (α : F ⟶ G), CategoryTheory.NatTrans.Equifibered α
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
IsQuasiregular.map : ∀ {F : Type u_1} {R : Type u_2} {S : Type u_3} [inst : NonUnitalSemiring R] [inst_1 : NonUnitalSemiring S]
  [inst_2 : FunLike F R S] [NonUnitalRingHomClass F R S] (f : F) {x : R}, IsQuasiregular x → IsQuasiregular (f x)
-- Mathlib.CategoryTheory.Triangulated.TStructure.Heart
CategoryTheory.Triangulated.TStructure.mem_heart_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (X : C), t.heart X ↔ t.IsLE X 0 ∧ t.IsGE X 0
-- Mathlib.Order.Bounds.Basic
isGreatest_Iic : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, IsGreatest (Set.Iic a) a
-- Mathlib.Order.OmegaCompletePartialOrder
/-- The map from continuous functions to monotone functions is itself a monotone function.  -/
OmegaCompletePartialOrder.ContinuousHom.toMono : {α : Type u_2} →
  {β : Type u_3} → [inst : OmegaCompletePartialOrder α] → [inst_1 : OmegaCompletePartialOrder β] → (α →𝒄 β) →o α →o β
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
CategoryTheory.Bicategory.conjugateIsoEquiv_apply_hom : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {c d : B} {l₁ l₂ : c ⟶ d} {r₁ r₂ : d ⟶ c}
  (adj₁ : CategoryTheory.Bicategory.Adjunction l₁ r₁) (adj₂ : CategoryTheory.Bicategory.Adjunction l₂ r₂) (α : l₂ ≅ l₁),
  ((CategoryTheory.Bicategory.conjugateIsoEquiv adj₁ adj₂) α).hom =
    (CategoryTheory.Bicategory.conjugateEquiv adj₁ adj₂) α.hom
-- Mathlib.NumberTheory.Padics.Complex
PadicComplex.coe_natCast : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ), ↑↑n = ↑n
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.negAddY.eq_1 : ∀ {R : Type r} [inst : CommRing R] (W' : WeierstrassCurve.Projective R) (P Q : Fin 3 → R),
  W'.negAddY P Q =
    -3 * P 0 ^ 2 * Q 0 * Q 1 + 3 * P 0 * Q 0 ^ 2 * P 1 - P 1 ^ 2 * Q 1 * Q 2 + P 1 * Q 1 ^ 2 * P 2 +
                                W'.a₁ * P 0 * Q 1 ^ 2 * P 2 -
                              W'.a₁ * Q 0 * P 1 ^ 2 * Q 2 -
                            W'.a₂ * P 0 ^ 2 * Q 1 * Q 2 +
                          W'.a₂ * Q 0 ^ 2 * P 1 * P 2 +
                        2 * W'.a₂ * P 0 * Q 0 * P 1 * Q 2 -
                      2 * W'.a₂ * P 0 * Q 0 * Q 1 * P 2 -
                    W'.a₃ * P 1 ^ 2 * Q 2 ^ 2 +
                  W'.a₃ * Q 1 ^ 2 * P 2 ^ 2 +
                W'.a₄ * P 0 * P 1 * Q 2 ^ 2 -
              2 * W'.a₄ * P 0 * Q 1 * P 2 * Q 2 +
            2 * W'.a₄ * Q 0 * P 1 * P 2 * Q 2 -
          W'.a₄ * Q 0 * Q 1 * P 2 ^ 2 +
        3 * W'.a₆ * P 1 * P 2 * Q 2 ^ 2 -
      3 * W'.a₆ * Q 1 * P 2 ^ 2 * Q 2
-- Mathlib.Analysis.Analytic.Constructions
HasFPowerSeriesOnBall.compContinuousLinearMap : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} {G : Type u_5}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {u : E →L[𝕜] F} {f : F → G}
  {pf : FormalMultilinearSeries 𝕜 F G} {x : E} {r : ENNReal},
  HasFPowerSeriesOnBall f pf (u x) r → HasFPowerSeriesOnBall (f ∘ ⇑u) (pf.compContinuousLinearMap u) x (r / ‖u‖ₑ)
-- Mathlib.Data.Matrix.Mul
Matrix.mulVec_single_one : ∀ {m : Type u_2} {n : Type u_3} {R : Type u_7} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : NonAssocSemiring R]
  (M : Matrix m n R) (j : n), M.mulVec (Pi.single j 1) = M.col j
-- Mathlib.NumberTheory.HeckeRing.Defs
/-- The right subgroup is contained in `Δ`.  -/
IsHeckeTriple.right_le : ∀ {G : Type u_1} {inst : Group G} {Δ : Submonoid G} (H₁ : Subgroup G) {H₂ : Subgroup G} [self : IsHeckeTriple Δ H₁ H₂],
  H₂.toSubmonoid ≤ Δ
-- Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
CuspForm.ofMulDiscriminant_apply : ∀ {k : ℤ} (f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range (k - 12)) (z : UpperHalfPlane),
  (CuspForm.ofMulDiscriminant f) z = ModularForm.discriminant z * f z
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.isRightKanExtension_iff_isIso : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  {F' F'' : CategoryTheory.Functor D H} (φ : F'' ⟶ F') {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H}
  (α : L.comp F' ⟶ F) (α' : L.comp F'' ⟶ F),
  CategoryTheory.CategoryStruct.comp (L.whiskerLeft φ) α = α' →
    ∀ [F'.IsRightKanExtension α], F''.IsRightKanExtension α' ↔ CategoryTheory.IsIso φ
-- Mathlib.Data.Fintype.Order
/-- Constructs the `⊤` of a finite nonempty `SemilatticeSup`  -/
Fintype.toOrderTop : (α : Type u_2) → [Fintype α] → [Nonempty α] → [inst : SemilatticeSup α] → OrderTop α
-- Lean.Linter.MissingDocs
Lean.Linter.MissingDocs.checkElab : Lean.Linter.MissingDocs.SimpleHandler
-- Mathlib.NumberTheory.DirichletCharacter.Basic
DirichletCharacter.changeLevel_eq_one_iff : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] {n m : ℕ} [NeZero m] {χ : DirichletCharacter R n} (hm : n ∣ m),
  (DirichletCharacter.changeLevel hm) χ = 1 ↔ χ = 1
-- Mathlib.CategoryTheory.Preadditive.Projective.Basic
CategoryTheory.EnoughProjectives.presentation : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.EnoughProjectives C] (X : C),
  Nonempty (CategoryTheory.ProjectivePresentation X)
-- Init.Data.String.Lemmas.Iterate
String.Model.positionsFrom_endPos : ∀ {s : String}, String.Model.positionsFrom s.endPos = []
-- Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
CategoryTheory.MorphismProperty.transfiniteCompositions.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C),
  CategoryTheory.MorphismProperty.transfiniteCompositions.{w, v, u} W =
    ⨆ J, ⨆ x, ⨆ x_1, ⨆ x_2, ⨆ (x_3 : WellFoundedLT J), W.transfiniteCompositionsOfShape J
-- Mathlib.SetTheory.Cardinal.Defs
Cardinal.mk_pi_congrRight_prop : ∀ {ι : Prop} {f g : ι → Type v},
  (∀ (i : ι), Cardinal.mk (f i) = Cardinal.mk (g i)) → Cardinal.mk ((i : ι) → f i) = Cardinal.mk ((i : ι) → g i)
-- Mathlib.Order.Filter.Prod
Filter.Eventually.trans_prod : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Filter α} {g : Filter β} {h : Filter γ} [g.NeBot] {p : α → β → Prop}
  {q : β → γ → Prop} {r : α → γ → Prop},
  (∀ᶠ (xy : α × β) in f ×ˢ g, p xy.1 xy.2) →
    (∀ᶠ (yz : β × γ) in g ×ˢ h, q yz.1 yz.2) →
      (∀ (x : α) (y : β) (z : γ), p x y → q y z → r x z) → ∀ᶠ (xz : α × γ) in f ×ˢ h, r xz.1 xz.2
-- Plausible.Testable
/-- Allow elaboration of `Configuration` arguments to tactics.
 -/
Plausible.elabConfig : Lean.Syntax →
  optParam Plausible.Configuration { } → optParam Bool true → Lean.Elab.Tactic.TacticM Plausible.Configuration
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.toZeroAtInfty_apply : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] [inst_4 : ProperSpace E] (f : SchwartzMap E F) (x : E), f.toZeroAtInfty x = f x
-- Init.Data.SInt.Lemmas
Int8.toInt_toBitVec : ∀ (x : Int8), x.toBitVec.toInt = x.toInt
-- Mathlib.Analysis.Calculus.Deriv.Basic
hasDerivAtFilter_zero : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] (L : Filter (𝕜 × 𝕜)), HasDerivAtFilter 0 0 L
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
/-- the cokernel condition for `π`  -/
CategoryTheory.ShortComplex.LeftHomologyData.wπ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (self : S.LeftHomologyData),
  CategoryTheory.CategoryStruct.comp (self.hi.lift (CategoryTheory.Limits.KernelFork.ofι S.f ⋯)) self.π = 0
-- Mathlib.Data.Num.ZNum
ZNum.of_nat_toZNum : ∀ (n : ℕ), (↑n).toZNum = ↑n
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.instSMulCommClassPreLp : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} {α : Type u_3} {E : α → Type u_4} [inst : (i : α) → NormedAddCommGroup (E i)]
  [inst_1 : NormedRing 𝕜] [inst_2 : NormedRing 𝕜'] [inst_3 : (i : α) → Module 𝕜 (E i)]
  [inst_4 : (i : α) → Module 𝕜' (E i)] [∀ (i : α), SMulCommClass 𝕜' 𝕜 (E i)], SMulCommClass 𝕜' 𝕜 (PreLp E)
-- Mathlib.LinearAlgebra.BilinearForm.TensorProduct
/-- The base change of a bilinear form.  -/
LinearMap.BilinForm.baseChange : {R : Type uR} →
  (A : Type uA) →
    {M₂ : Type uM₂} →
      [inst : CommSemiring R] →
        [inst_1 : CommSemiring A] →
          [inst_2 : AddCommMonoid M₂] →
            [inst_3 : Algebra R A] →
              [inst_4 : Module R M₂] → LinearMap.BilinForm R M₂ → LinearMap.BilinForm A (TensorProduct R A M₂)
-- Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
CategoryTheory.ObjectProperty.instIsStableUnderBaseChangeMonoModSerre : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (P : CategoryTheory.ObjectProperty C) [inst_2 : P.IsSerreClass], P.monoModSerre.IsStableUnderBaseChange
-- Mathlib.Geometry.Manifold.ContMDiff.Basic
contMDiffWithinAt_zero : ∀ {𝕜 : 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] {E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  {H' : Type u_6} [inst_7 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7}
  [inst_8 : TopologicalSpace M'] [inst_9 : ChartedSpace H M] [inst_10 : ChartedSpace H' M'] {s : Set M} {x : M}
  {n : WithTop ℕ∞} [inst_11 : Zero M'], ContMDiffWithinAt I I' n 0 s x