mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
WeierstrassCurve.natDegree_ΨSq_le : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) (n : ℤ), (W.ΨSq n).natDegree ≤ n.natAbs ^ 2 - 1
-- Mathlib.CategoryTheory.Triangulated.Opposite.Functor
/-- If `F` is triangulated, so is `F.op`.
 -/
CategoryTheory.Pretriangulated.Opposite.functor_isTriangulated_op : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.HasShift C ℤ]
  [inst_3 : CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [inst_4 : F.CommShift ℤ]
  [inst_5 : CategoryTheory.Limits.HasZeroObject C] [inst_6 : CategoryTheory.Preadditive C]
  [inst_7 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_8 : CategoryTheory.Pretriangulated C]
  [inst_9 : CategoryTheory.Limits.HasZeroObject D] [inst_10 : CategoryTheory.Preadditive D]
  [inst_11 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [inst_12 : CategoryTheory.Pretriangulated D]
  [F.IsTriangulated], F.op.IsTriangulated
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.ofCoeff_erase : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] (m : M) (x : M →₀ R),
  MonoidAlgebra.ofCoeff (Finsupp.erase m x) = MonoidAlgebra.erase m (MonoidAlgebra.ofCoeff x)
-- Mathlib.Data.Fintype.Powerset
Finset.fintype : {α : Type u_1} → [Fintype α] → Fintype (Finset α)
-- Mathlib.MeasureTheory.Covering.DensityTheorem
IsUnifLocDoublingMeasure.tendsto_closedBall_filterAt : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] [inst_1 : MeasurableSpace α] (μ : MeasureTheory.Measure α)
  [inst_2 : IsUnifLocDoublingMeasure μ] [inst_3 : SecondCountableTopology α] [inst_4 : BorelSpace α]
  [inst_5 : MeasureTheory.IsLocallyFiniteMeasure μ] {K : ℝ} {x : α} {ι : Type u_2} {l : Filter ι} (w : ι → α)
  (δ : ι → ℝ),
  Filter.Tendsto δ l (nhdsWithin 0 (Set.Ioi 0)) →
    (∀ᶠ (j : ι) in l, x ∈ Metric.closedBall (w j) (K * δ j)) →
      Filter.Tendsto (fun j => Metric.closedBall (w j) (δ j)) l ((IsUnifLocDoublingMeasure.vitaliFamily μ K).filterAt x)
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.Bicone.ofColimitCocone_ι : ∀ {J : Type w} {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {f : J → C}
  {t : CategoryTheory.Limits.Cocone (CategoryTheory.Discrete.functor f)} (ht : CategoryTheory.Limits.IsColimit t)
  (j : J), (CategoryTheory.Limits.Bicone.ofColimitCocone ht).ι j = t.ι.app { as := j }
-- Mathlib.Probability.Kernel.Composition.IntegralCompProd
ProbabilityTheory.Kernel.integral_fn_integral_add_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {E : Type u_4} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : NormedAddCommGroup E] {a : α} {κ : ProbabilityTheory.Kernel α β}
  {η : ProbabilityTheory.Kernel β γ} [inst_1 : NormedSpace ℝ E] {E' : Type u_5} [inst_2 : NormedAddCommGroup E']
  [inst_3 : NormedSpace ℝ E'] ⦃f g : γ → E⦄ (F : E → E'),
  MeasureTheory.Integrable f ((η.comp κ) a) →
    MeasureTheory.Integrable g ((η.comp κ) a) →
      ∫ (x : β), F (∫ (y : γ), f y + g y ∂η x) ∂κ a = ∫ (x : β), F (∫ (y : γ), f y ∂η x + ∫ (y : γ), g y ∂η x) ∂κ a
-- Init.Data.Int.LemmasAux
Int.ofNat_mul_out : ∀ (m n : ℕ), ↑m * ↑n = ↑(m * n)
-- Lean.MetavarContext
Lean.MetavarContext.elimMVarDeps : Array Lean.Expr → Lean.Expr → Bool → Lean.MetavarContext.MkBindingM Lean.Expr
-- Mathlib.RingTheory.FormalGroup.Basic
/-- Additive formal group law `𝔾ₐ(X,Y) = X + Y`.  -/
FormalGroup.𝔾ₐ : {R : Type u_1} → [inst : CommRing R] → FormalGroup R
-- Mathlib.Data.Int.Order.Units
Int.units_pow_eq_pow_mod_two : ∀ (u : ℤˣ) (n : ℕ), u ^ n = u ^ (n % 2)
-- Aesop.Rule
Aesop.instOrdUnsafeRuleInfo : Ord Aesop.UnsafeRuleInfo
-- Mathlib.Analysis.Normed.Algebra.Spectrum
/-- Let `S` be a closed subalgebra of a Banach algebra `A`, and let `x : S`. If `z` is in the
spectrum of `x`, then the connected component of `z` in the complement of the spectrum of `↑x : A`
is bounded (or else `z` actually belongs to the spectrum of `↑x : A`).  -/
Subalgebra.spectrum_isBounded_connectedComponentIn : ∀ {𝕜 : Type u_3} {A : Type u_4} {SA : Type u_5} [inst : NormedRing A] [CompleteSpace A] [inst_2 : SetLike SA A]
  [inst_3 : SubringClass SA A] [inst_4 : NormedField 𝕜] [inst_5 : NormedAlgebra 𝕜 A] [instSMulMem : SMulMemClass SA 𝕜 A]
  (S : SA) [hS : IsClosed ↑S] (x : ↥S) {z : 𝕜},
  z ∈ spectrum 𝕜 x → Bornology.IsBounded (connectedComponentIn (spectrum 𝕜 ↑x)ᶜ z)
-- Lean.Meta.Tactic.Grind.Arith.Linear.Util
Lean.Meta.Grind.Arith.Linear.getOrderedRingInst : Lean.Meta.Grind.Arith.Linear.LinearM Lean.Expr
-- Mathlib.RingTheory.Ideal.Maps
Ideal.apply_coe_mem_map : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : FunLike F R S] (f : F)
  (I : Ideal R) (x : ↥I), f ↑x ∈ Ideal.map f I
-- Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
CategoryTheory.AdditiveFunctor.of_obj : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) [inst_4 : F.Additive],
  (CategoryTheory.AdditiveFunctor.of F).obj = F
-- Mathlib.CategoryTheory.Sites.ConstantSheaf
/-- The constant sheaf functor commutes up to isomorphism the equivalence of sheaf categories induced
by a dense subsite.
 -/
CategoryTheory.equivCommuteConstant : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      (D : Type u_2) →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_2 : CategoryTheory.HasWeakSheafify J D] →
            {C' : Type u_3} →
              [inst_3 : CategoryTheory.Category.{v_3, u_3} C'] →
                (K : CategoryTheory.GrothendieckTopology C') →
                  [inst_4 : CategoryTheory.HasWeakSheafify K D] →
                    (G : CategoryTheory.Functor C C') →
                      [inst_5 :
                          ∀ (X : C'ᵒᵖ),
                            CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X G.op) D] →
                        [inst_6 : CategoryTheory.Functor.IsDenseSubsite J K G] →
                          {T : C} →
                            CategoryTheory.Limits.IsTerminal T →
                              CategoryTheory.Limits.IsTerminal (G.obj T) →
                                ((CategoryTheory.constantSheaf J D).comp
                                    (CategoryTheory.Functor.IsDenseSubsite.sheafEquiv J K G D).functor ≅
                                  CategoryTheory.constantSheaf K D)
-- Mathlib.Data.Nat.Nth
Nat.le_nth : ∀ {p : ℕ → Prop} {n : ℕ}, (∀ (hf : (Set.ofPred p).Finite), n < hf.toFinset.card) → n ≤ Nat.nth p n
-- Mathlib.Algebra.Lie.Loop
LieAlgebra.LoopAlgebra.instGradedLieAlgebraTensorProductAddMonoidAlgebraDecomposeTensorGrade : (R : Type u_1) →
  (A : Type u_2) →
    (L : Type u_3) →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : LieAlgebra R L] →
            [inst_3 : DecidableEq A] →
              [inst_4 : AddCommMonoid A] →
                GradedLieAlgebra fun a => DirectSum.decomposeTensor (AddMonoidAlgebra.grade R) L a
-- Mathlib.Data.ENat.Lattice
ENat.sSup_mem_of_nonempty_of_lt_top : ∀ {s : Set ℕ∞} [Nonempty ↑s], sSup s < ⊤ → sSup s ∈ s
-- Mathlib.Order.Filter.Map
Filter.NeBot.comap_of_surj : ∀ {α : Type u_1} {β : Type u_2} {f : Filter β} {m : α → β}, f.NeBot → Function.Surjective m → (Filter.comap m f).NeBot
-- Mathlib.MeasureTheory.Measure.Count
MeasureTheory.Measure.ae_count_iff : ∀ {α : Type u_1} [inst : MeasurableSpace α] {p : α → Prop},
  (∀ᵐ (x : α) ∂MeasureTheory.Measure.count, p x) ↔ ∀ (x : α), p x
-- Mathlib.Topology.UniformSpace.Cauchy
Ultrafilter.cauchy_of_totallyBounded : ∀ {α : Type u} [uniformSpace : UniformSpace α] {s : Set α} (f : Ultrafilter α),
  TotallyBounded s → ↑f ≤ Filter.principal s → Cauchy ↑f
-- Std.Data.HashMap.Lemmas
Std.HashMap.Equiv.diff_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ m₃ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α],
  m₁.Equiv m₂ → (m₁ \ m₃).Equiv (m₂ \ m₃)
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Trimming
Tactic.ComputeAsymptotics.MultiseriesExpansion.Trimmed.below.const : ∀
  {motive :
    {basis : Tactic.ComputeAsymptotics.Basis} →
      (a : Tactic.ComputeAsymptotics.MultiseriesExpansion basis) → a.Trimmed → Prop}
  {c : ℝ}, Tactic.ComputeAsymptotics.MultiseriesExpansion.Trimmed.below ⋯
-- Mathlib.Analysis.Analytic.Basic
HasFPowerSeriesWithinOnBall.comp_sub : ∀ {𝕜 : 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), HasFPowerSeriesWithinOnBall (fun z => f (z - y)) p (s + {y}) (x + y) r
-- Mathlib.CategoryTheory.Sites.Hypercover.Saturate
CategoryTheory.PreZeroHypercover.toSaturateOfHasPullbacks_fromSaturateOfHasPullbacks : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {S : C} (E : CategoryTheory.PreZeroHypercover S)
  [inst_1 : E.HasPullbacks],
  CategoryTheory.PreOneHypercover.Hom.comp E.toSaturateOfHasPullbacks E.fromSaturateOfHasPullbacks =
    CategoryTheory.PreOneHypercover.Hom.id E.toPreOneHypercover
-- Mathlib.Algebra.Homology.DerivedCategory.Plus
DerivedCategory.Plus.instEssSurjPlusQh : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C], DerivedCategory.Plus.Qh.EssSurj
-- Lean.Parser.Tactic.Doc
/-- If `tac` is registered as the alternative form of another tactic, then return the canonical name for
it.
 -/
Lean.Parser.Tactic.Doc.alternativeOfTactic : Lean.Environment → Lean.Name → Option Lean.Name
-- Mathlib.CategoryTheory.Preadditive.Basic
/-- A category is called preadditive if `P ⟶ Q` is an abelian group such that composition is
linear in both variables.  -/
CategoryTheory.Preadditive.add_comp_assoc : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.Preadditive C] (P Q R : C)
  (f f' : P ⟶ Q) (g : Q ⟶ R) {Z : C} (h : R ⟶ Z),
  CategoryTheory.CategoryStruct.comp (f + f') (CategoryTheory.CategoryStruct.comp g h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp f g + CategoryTheory.CategoryStruct.comp f' g) h
-- Init.Data.SInt.Lemmas
Int16.le_toInt : ∀ (x : Int16), -2 ^ 15 ≤ x.toInt
-- Mathlib.Probability.Martingale.Upcrossing
MeasureTheory.Submartingale.sum_upcrossingStrat_mul : ∀ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {f : ℕ → Ω → ℝ}
  {ℱ : MeasureTheory.Filtration ℕ m0} [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.Submartingale f ℱ μ →
    ∀ (a b : ℝ) (N : ℕ),
      MeasureTheory.Submartingale
        (fun n => ∑ k ∈ Finset.range n, MeasureTheory.upcrossingStrat a b f N k * (f (k + 1) - f k)) ℱ μ
-- Mathlib.Combinatorics.SimpleGraph.Copy
SimpleGraph.copyCount.eq_1 : ∀ {V : Type u_1} {W : Type u_2} [inst : Fintype V] (G : SimpleGraph V) (H : SimpleGraph W),
  G.copyCount H = {G' | Nonempty (H ≃g G'.coe)}.card
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
/-- The tail morphism of a reflexive cofork.  -/
CategoryTheory.Limits.ReflexiveCofork.π : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor CategoryTheory.Limits.WalkingReflexivePair C} →
      (G : CategoryTheory.Limits.ReflexiveCofork F) → F.obj CategoryTheory.Limits.WalkingReflexivePair.zero ⟶ G.pt
-- Init.Grind.Ring.OfScientific
/-- A type class that ensures that `OfScientific.ofScientific` is properly defined with respect to
the field structure.
 -/
Lean.Grind.LawfulOfScientific : (α : Type u) → [Lean.Grind.Field α] → [OfScientific α] → Prop
-- Lean.Meta.WHNF
/-- If `major` is not a constructor application, and its type is a non-recursive structure `C ...`, then return `C.mk major.1 ... major.n`

\pre `inductName` is `C`.

If `Meta.Config.etaStruct` is `false` or the condition above does not hold, this method just returns `major`.  -/
_private.Lean.Meta.WHNF.0.Lean.Meta.toCtorWhenStructure : Lean.Name → Lean.Expr → Lean.MetaM Lean.Expr
-- Init.Data.Option.Lemmas
Option.bind_fun_none : ∀ {α : Type u_1} {β : Type u_2} (x : Option α), (x.bind fun x => none) = none
-- Mathlib.CategoryTheory.Triangulated.TStructure.Induced
CategoryTheory.ObjectProperty.HasInducedTStructure.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} 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]
  (P P_1 : CategoryTheory.ObjectProperty C) (e_P : P = P_1) (t t_1 : CategoryTheory.Triangulated.TStructure C),
  t = t_1 → ∀ [inst_6 : P.IsTriangulated], P.HasInducedTStructure t = P_1.HasInducedTStructure t_1
-- Mathlib.Combinatorics.Additive.ApproximateSubgroup
IsApproximateSubgroup.pow_inter_pow_covBySMul_sq_inter_sq : ∀ {G : Type u_1} [inst : Group G] {A B : Set G} {K L : ℝ} {m n : ℕ},
  IsApproximateSubgroup K A →
    IsApproximateSubgroup L B → 2 ≤ m → 2 ≤ n → CovBySMul G (K ^ (m - 1) * L ^ (n - 1)) (A ^ m ∩ B ^ n) (A ^ 2 ∩ B ^ 2)
-- Mathlib.Computability.Reduce
/-- Lifts a binary function on sets of natural numbers to many-one degrees.  -/
ManyOneDegree.liftOn₂ : {φ : Sort u_1} →
  ManyOneDegree →
    ManyOneDegree →
      (f : Set ℕ → Set ℕ → φ) →
        (∀ (p₁ p₂ q₁ q₂ : ℕ → Prop), ManyOneEquiv p₁ p₂ → ManyOneEquiv q₁ q₂ → f p₁ q₁ = f p₂ q₂) → φ
-- Lean.Parser.Basic
Lean.Parser.lookaheadFn : Lean.Parser.ParserFn → Lean.Parser.ParserFn
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
AlgebraicGeometry.Scheme.Hom.quasiFiniteAt_comp_iff : ∀ {X Y Z : AlgebraicGeometry.Scheme} {f : X ⟶ Y} {g : Y ⟶ Z} {x : ↥X} [AlgebraicGeometry.LocallyQuasiFinite g],
  AlgebraicGeometry.Scheme.Hom.QuasiFiniteAt (CategoryTheory.CategoryStruct.comp f g) x ↔
    AlgebraicGeometry.Scheme.Hom.QuasiFiniteAt f x
-- Lean.Elab.Coinductive
Lean.Elab.Command.CoinductiveElabData.mk.inj : ∀ {declId : Lean.Syntax} {declName : Lean.Name} {ref : Lean.Syntax} {modifiers : Lean.Elab.Modifiers}
  {ctorSyntax : Array Lean.Syntax} {isGreatest : Bool} {declId_1 : Lean.Syntax} {declName_1 : Lean.Name}
  {ref_1 : Lean.Syntax} {modifiers_1 : Lean.Elab.Modifiers} {ctorSyntax_1 : Array Lean.Syntax} {isGreatest_1 : Bool},
  { declId := declId, declName := declName, ref := ref, modifiers := modifiers, ctorSyntax := ctorSyntax,
        isGreatest := isGreatest } =
      { declId := declId_1, declName := declName_1, ref := ref_1, modifiers := modifiers_1, ctorSyntax := ctorSyntax_1,
        isGreatest := isGreatest_1 } →
    declId = declId_1 ∧
      declName = declName_1 ∧
        ref = ref_1 ∧ modifiers = modifiers_1 ∧ ctorSyntax = ctorSyntax_1 ∧ isGreatest = isGreatest_1
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- The type of objects for the diagram indexing a binary (co)product.  -/
CategoryTheory.Limits.WalkingPair : Type
-- Mathlib.Algebra.Category.FGModuleCat.Colimits
FGModuleCat.instHasFiniteColimits : ∀ {k : Type u} [inst : Ring k], CategoryTheory.Limits.HasFiniteColimits (FGModuleCat k)
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Matrix.SpecialLinearGroup.diagonal_neZero : ∀ {F : Type u_1} [inst : Field F] {ι : Type u_2} [inst_1 : Fintype ι] [inst_2 : DecidableEq ι] (D : ι → F),
  (Matrix.diagonal D).det = 1 → ∀ (j : ι), D j ≠ 0
-- Lean.Parser.Command
Lean.Parser.Command.print.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Combinatorics.SimpleGraph.Clique
/-- If `s` is an independent set, its complement meets every edge of `G`.  -/
SimpleGraph.IsIndepSet.nonempty_mem_compl_mem_edge : ∀ {α : Type u_1} (G : SimpleGraph α) {s : Set α},
  G.IsIndepSet s → ∀ {e : Sym2 α}, e ∈ G.edgeSet → {b | b ∈ sᶜ ∧ b ∈ e}.Nonempty
-- Lean.Util.SCC
Lean.SCC.Data.mk.inj : ∀ {index? lowlink? : Option ℕ} {onStack : Bool} {index?_1 lowlink?_1 : Option ℕ} {onStack_1 : Bool},
  { index? := index?, lowlink? := lowlink?, onStack := onStack } =
      { index? := index?_1, lowlink? := lowlink?_1, onStack := onStack_1 } →
    index? = index?_1 ∧ lowlink? = lowlink?_1 ∧ onStack = onStack_1
-- Mathlib.Algebra.Order.Floor.Defs
Int.lt_ceil : ∀ {α : Type u_2} [inst : Ring α] [inst_1 : LinearOrder α] [inst_2 : FloorRing α] {z : ℤ} {a : α}, z < ⌈a⌉ ↔ ↑z < a
-- Mathlib.AlgebraicGeometry.ColimitsOver
CategoryTheory.MorphismProperty.Over.mapId.congr_simp : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {P : CategoryTheory.MorphismProperty T}
  (Q : CategoryTheory.MorphismProperty T) [inst_1 : Q.IsMultiplicative] [inst_2 : P.IsStableUnderComposition]
  [inst_3 : P.IsMultiplicative] [inst_4 : Q.RespectsIso] (X : T) (f : X ⟶ X)
  (hf : f = CategoryTheory.CategoryStruct.id X),
  CategoryTheory.MorphismProperty.Over.mapId Q X f hf = CategoryTheory.MorphismProperty.Over.mapId Q X f hf
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
HasFTaylorSeriesUpToOn.shift_of_succ : ∀ {𝕜 : 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} {p : E → FormalMultilinearSeries 𝕜 E F} {n : ℕ},
  HasFTaylorSeriesUpToOn (↑(n + 1)) f p s →
    HasFTaylorSeriesUpToOn (↑n) (fun x => (continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) (fun x => (p x).shift) s
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf
AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.add_mem' : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] {𝒜 : ℕ → σ}
  [inst_3 : GradedRing 𝒜] (U : (TopologicalSpace.Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ)
  (a b : (x : ↥(Opposite.unop U)) → HomogeneousLocalization.AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal),
  (AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.isLocallyFraction 𝒜).pred a →
    (AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.isLocallyFraction 𝒜).pred b →
      (AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.isLocallyFraction 𝒜).pred (a + b)
-- Mathlib.NumberTheory.PellMatiyasevic
Pell.xy_modEq_yn : ∀ {a : ℕ} (a1 : 1 < a) (n k : ℕ),
  Pell.xn a1 (n * k) ≡ Pell.xn a1 n ^ k [MOD Pell.yn a1 n ^ 2] ∧
    Pell.yn a1 (n * k) ≡ k * Pell.xn a1 n ^ (k - 1) * Pell.yn a1 n [MOD Pell.yn a1 n ^ 3]
-- Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
MeasureTheory.eLpNorm_le_eLpNorm_top_mul_eLpNorm : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {m : MeasurableSpace α} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedAddCommGroup G] {μ : MeasureTheory.Measure α} (p : ENNReal)
  (f : α → E) {g : α → F},
  MeasureTheory.AEStronglyMeasurable g μ →
    ∀ (b : E → F → G) (c : NNReal),
      (∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊) →
        MeasureTheory.eLpNorm (fun x => b (f x) (g x)) p μ ≤
          ↑c * MeasureTheory.eLpNorm f ⊤ μ * MeasureTheory.eLpNorm g p μ
-- Mathlib.CategoryTheory.Category.PartialFun
partialFunEquivPointed_unitIso_inv_app : ∀ (X : PartialFun),
  partialFunEquivPointed.unitIso.inv.app X =
    (PartialFun.Iso.mk
        { toFun := fun a => ⟨some a, ⋯⟩, invFun := fun a => (↑a).get ⋯, left_inv := ⋯, right_inv := ⋯ }).inv
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.ne_zero_of_degree_ne_zero : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] {f : MvPolynomial σ R},
  m.degree f ≠ 0 → f ≠ 0
-- Init.Data.Vector.Lemmas
Vector.not_mem_push_of_ne_of_not_mem : ∀ {α : Type u_1} {n : ℕ} {a y : α} {xs : Vector α n}, a ≠ y → a ∉ xs → a ∉ xs.push y
-- Mathlib.Algebra.Vertex.HVertexOperator
/-- The composite of two heterogeneous vertex operators, as a heterogeneous vertex operator.  -/
HVertexOperator.comp : {Γ : Type u_5} →
  {Γ' : Type u_6} →
    [inst : PartialOrder Γ] →
      [inst_1 : PartialOrder Γ'] →
        {R : Type u_7} →
          [inst_2 : CommRing R] →
            {U : Type u_8} →
              {V : Type u_9} →
                {W : Type u_10} →
                  [inst_3 : AddCommGroup U] →
                    [inst_4 : Module R U] →
                      [inst_5 : AddCommGroup V] →
                        [inst_6 : Module R V] →
                          [inst_7 : AddCommGroup W] →
                            [inst_8 : Module R W] →
                              HVertexOperator Γ R V W → HVertexOperator Γ' R U V → HVertexOperator (Lex (Γ' × Γ)) R U W
-- Mathlib.Topology.LocalAtTarget
IsOpenMap.restrictPreimage : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β},
  IsOpenMap f → ∀ (s : Set β), IsOpenMap (s.restrictPreimage f)
-- Mathlib.LinearAlgebra.Matrix.Vec
Matrix.vec_mul_eq_mulVec : ∀ {l : Type u_2} {m : Type u_3} {n : Type u_1} {R : Type u_4} [inst : Semiring R] [inst_1 : Fintype m]
  [inst_2 : Fintype n] [inst_3 : DecidableEq n] (A : Matrix l m R) (B : Matrix m n R),
  (A * B).vec = (Matrix.kroneckerMap (fun x1 x2 => x1 * x2) 1 A).mulVec B.vec
-- Mathlib.Order.Std
/-- ≤ forms a preorder.  -/
Preorder.OfStdArgs.isPreorder : ∀ {α : Type u_1} (self : Preorder.OfStdArgs α),
  let this := self.le;
  Std.IsPreorder α
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs
EisensteinSeries.D2_mul : ∀ (A B : Matrix.SpecialLinearGroup (Fin 2) ℤ),
  EisensteinSeries.D2 (A * B) = SlashAction.map 2 B (EisensteinSeries.D2 A) + EisensteinSeries.D2 B
-- Mathlib.AlgebraicGeometry.AffineTransitionLimit
/-- A variant of `exists_mem_of_isClosed_of_nonempty` where the closed sets are only defined
for the objects over a given `j : I`.
 -/
AlgebraicGeometry.exists_mem_of_isClosed_of_nonempty' : ∀ {I : Type u} [inst : CategoryTheory.Category.{u, u} I] (D : CategoryTheory.Functor I AlgebraicGeometry.Scheme)
  (c : CategoryTheory.Limits.Cone D) (hc : CategoryTheory.Limits.IsLimit c) [CategoryTheory.IsCofilteredOrEmpty I]
  [∀ {i j : I} (f : i ⟶ j), AlgebraicGeometry.IsAffineHom (D.map f)] {j : I} (Z : (i : I) → (i ⟶ j) → Set ↥(D.obj i)),
  (∀ (i : I) (hij : i ⟶ j), IsClosed (Z i hij)) →
    (∀ (i : I) (hij : i ⟶ j), (Z i hij).Nonempty) →
      (∀ (i : I) (hij : i ⟶ j), IsCompact (Z i hij)) →
        (∀ (i i' : I) (hi'i : i' ⟶ i) (hij : i ⟶ j),
            Set.MapsTo (⇑(D.map hi'i)) (Z i' (CategoryTheory.CategoryStruct.comp hi'i hij)) (Z i hij)) →
          ∃ s, ∀ (i : I) (hij : i ⟶ j), (c.π.app i) s ∈ Z i hij
-- Mathlib.Analysis.InnerProductSpace.LinearMap
LinearMap.coe_isometryOfInner : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {E' : Type u_7} [inst_3 : SeminormedAddCommGroup E'] [inst_4 : InnerProductSpace 𝕜 E'] (f : E →ₗ[𝕜] E')
  (h : ∀ (x y : E), inner 𝕜 (f x) (f y) = inner 𝕜 x y), ⇑(f.isometryOfInner h) = ⇑f
-- Std.Http.Data.URI.Basic
Std.Http.RequestTarget.authorityForm.injEq : ∀ (authority authority_1 : Std.Http.URI.Authority),
  (Std.Http.RequestTarget.authorityForm authority = Std.Http.RequestTarget.authorityForm authority_1) =
    (authority = authority_1)
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
ClosedSubmodule.mk.sizeOf_spec : ∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : TopologicalSpace M]
  [inst_3 : Module R M] [inst_4 : SizeOf R] [inst_5 : SizeOf M] (toSubmodule : Submodule R M)
  (isClosed' : IsClosed toSubmodule.carrier),
  sizeOf { toSubmodule := toSubmodule, isClosed' := isClosed' } = 1 + sizeOf toSubmodule + sizeOf isClosed'
-- Mathlib.Algebra.Group.Action.Units
IsUnit.smul : ∀ {G : Type u_1} {M : Type u_3} [inst : Group G] [inst_1 : Monoid M] [inst_2 : MulAction G M] [SMulCommClass G M M]
  [IsScalarTower G M M] {m : M} (g : G), IsUnit m → IsUnit (g • m)
-- Mathlib.LinearAlgebra.Matrix.Rank
Matrix.rank_of_isUnit : ∀ {n : Type un} {R : Type uR} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommSemiring R]
  [StrongRankCondition R] (A : Matrix n n R), IsUnit A → A.rank = Fintype.card n