mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.roots_multiset_prod_X_sub_C : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] (s : Multiset R),
  (Multiset.map (fun a => Polynomial.X - Polynomial.C a) s).prod.roots = s
-- Init.Data.Iterators.Consumers.Monadic.Loop
/-- Iterates over the whole iterator, applying the monadic effects of each step, discarding all
emitted values.

This variant terminates after finitely many steps and requires a proof that the iterator is
finite. If such a proof is not available, consider using `IterM.drain`.
 -/
Std.IterM.Total.drain : {α : Type w} →
  {m : Type w → Type w'} →
    [Monad m] →
      {β : Type w} →
        [inst : Std.Iterator α m β] →
          [Std.Iterators.Finite α m] → Std.IterM.Total m β → [Std.IteratorLoop α m m] → m PUnit.{w + 1}
-- Batteries.Data.List.Lemmas
List.disjoint_comm : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Disjoint l₂ ↔ l₂.Disjoint l₁
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.IsCycle.eq_1 : ∀ {α : Type u_2} (f : Equiv.Perm α), f.IsCycle = ∃ x, f x ≠ x ∧ ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle x y
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.coe_aeval_mk_apply : ∀ {R : Type u} {A : Type z} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {p : Polynomial R}
  (x : A) {S : Subalgebra R A} (h : x ∈ S), ↑((Polynomial.aeval ⟨x, h⟩) p) = (Polynomial.aeval x) p
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
CategoryTheory.Oplax.LaxTrans.vComp_naturality_naturality : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G H : CategoryTheory.OplaxFunctor B C} (η : CategoryTheory.Oplax.LaxTrans F G)
  (θ : CategoryTheory.Oplax.LaxTrans G H) {a b : B} {f g : a ⟶ b} (β : f ⟶ g),
  CategoryTheory.CategoryStruct.comp (η.vCompNaturality θ f)
      (CategoryTheory.Bicategory.whiskerRight (F.map₂ β) (η.vCompApp θ b)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (η.vCompApp θ a) (H.map₂ β))
      (η.vCompNaturality θ g)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
/-- Extension for `Real.arctan`.  -/
Mathlib.Meta.Positivity.evalRealArctan : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Real.BohrMollerup.tendsto_log_gamma : ∀ {x : ℝ}, 0 < x → Filter.Tendsto (Real.BohrMollerup.logGammaSeq x) Filter.atTop (nhds (Real.log (Real.Gamma x)))
-- Mathlib.Computability.RegularExpressions
RegularExpression.matches'.eq_5 : ∀ {α : Type u_1} (P Q : RegularExpression α), (P.comp Q).matches' = P.matches' * Q.matches'
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
/-- All derivatives of a Schwartz function are rapidly decaying.  -/
SchwartzMap.decay : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] (f : SchwartzMap E F) (k n : ℕ),
  ∃ C, 0 < C ∧ ∀ (x : E), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
-- Init.Data.List.Lemmas
List.exists_cons_of_length_eq_add_one : ∀ {α : Type u_1} {n : ℕ} {l : List α}, l.length = n + 1 → ∃ h t, l = h :: t
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.instDecidableEqCont'.decEq : (x x_1 : Turing.PartrecToTM2.Cont') → Decidable (x = x_1)
-- Init.Data.Nat.Gcd
Nat.gcd_eq_one_iff : ∀ {m n : ℕ}, m.gcd n = 1 ↔ ∀ (c : ℕ), c ∣ m → c ∣ n → c = 1
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgEquiv.symm_arrowCongr' : ∀ {R : Type u_1} {A₁ : Type u_2} {A₂ : Type u_3} {A₁' : Type u_5} {A₂' : Type u_6} [inst : Monoid R]
  [inst_1 : NonUnitalNonAssocSemiring A₁] [inst_2 : DistribMulAction R A₁] [inst_3 : Star A₁]
  [inst_4 : NonUnitalNonAssocSemiring A₂] [inst_5 : DistribMulAction R A₂] [inst_6 : Star A₂]
  [inst_7 : NonUnitalNonAssocSemiring A₁'] [inst_8 : DistribMulAction R A₁'] [inst_9 : Star A₁']
  [inst_10 : NonUnitalNonAssocSemiring A₂'] [inst_11 : DistribMulAction R A₂'] [inst_12 : Star A₂'] (e₁ : A₁ ≃⋆ₐ[R] A₁')
  (e₂ : A₂ ≃⋆ₐ[R] A₂'), (e₁.arrowCongr' e₂).symm = e₁.symm.arrowCongr' e₂.symm
-- Mathlib.RingTheory.Polynomial.Quotient
Ideal.polynomialQuotientEquivQuotientPolynomial.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R),
  I.polynomialQuotientEquivQuotientPolynomial =
    {
      toFun :=
        ⇑(Polynomial.eval₂RingHom
            (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map Polynomial.C I)).comp Polynomial.C) ⋯)
            ((Ideal.Quotient.mk (Ideal.map Polynomial.C I)) Polynomial.X)),
      invFun :=
        ⇑(Ideal.Quotient.lift (Ideal.map Polynomial.C I)
            (Polynomial.eval₂RingHom (Polynomial.C.comp (Ideal.Quotient.mk I)) Polynomial.X) ⋯),
      left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯ }
-- Mathlib.Analysis.Convex.Combination
/-- A weak version of Carathéodory's theorem.  -/
convexHull_eq_union_convexHull_finite_subsets : ∀ {R : Type u_1} {E : Type u_3} [inst : Field R] [inst_1 : AddCommGroup E] [inst_2 : Module R E]
  [inst_3 : LinearOrder R] [IsStrictOrderedRing R] (s : Set E),
  (convexHull R) s = ⋃ t, ⋃ (_ : ↑t ⊆ s), (convexHull R) ↑t
-- Mathlib.Algebra.Lie.OfAssociative
AlgHom.coe_toLieHom : ∀ {A : Type v} [inst : Ring A] {R : Type u} [inst_1 : CommRing R] [inst_2 : Algebra R A] {B : Type w} [inst_3 : Ring B]
  [inst_4 : Algebra R B] (f : A →ₐ[R] B), ⇑f.toLieHom = ⇑f
-- Mathlib.CategoryTheory.Bicategory.InducedBicategory
CategoryTheory.Bicategory.InducedBicategory.bicategory_id_hom : ∀ {B : Type u_1} {C : Type u_2} [inst : CategoryTheory.Bicategory C] {F : B → C}
  (X : CategoryTheory.Bicategory.InducedBicategory C F),
  (CategoryTheory.CategoryStruct.id X).hom = CategoryTheory.CategoryStruct.id (F X)
-- Mathlib.Topology.MetricSpace.UniformConvergence
UniformOnFun.edist_def' : ∀ {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [inst : PseudoEMetricSpace β] [inst_1 : Finite ↑𝔖]
  (f g : UniformOnFun α β 𝔖),
  edist f g = ⨆ s ∈ 𝔖, ⨆ x ∈ s, edist ((UniformOnFun.toFun 𝔖) f x) ((UniformOnFun.toFun 𝔖) g x)
-- Mathlib.Order.Fin.Tuple
Fin.strictMono_cons_zero_succ : ∀ {n : ℕ} {f : Fin n → Fin (n + 1)}, StrictMono (Fin.cons 0 f) ↔ f = Fin.succ
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.FunDecl.brecOn.eq : ∀ {pu : Lean.Compiler.LCNF.Purity} {motive_1 : Lean.Compiler.LCNF.Alt pu → Sort u}
  {motive_2 : Lean.Compiler.LCNF.FunDecl pu → Sort u} {motive_3 : Lean.Compiler.LCNF.Cases pu → Sort u}
  {motive_4 : Lean.Compiler.LCNF.Code pu → Sort u} {motive_5 : Array (Lean.Compiler.LCNF.Alt pu) → Sort u}
  {motive_6 : List (Lean.Compiler.LCNF.Alt pu) → Sort u} (t : Lean.Compiler.LCNF.FunDecl pu)
  (F_1 : (t : Lean.Compiler.LCNF.Alt pu) → t.below → motive_1 t)
  (F_2 : (t : Lean.Compiler.LCNF.FunDecl pu) → t.below → motive_2 t)
  (F_3 : (t : Lean.Compiler.LCNF.Cases pu) → t.below → motive_3 t)
  (F_4 : (t : Lean.Compiler.LCNF.Code pu) → t.below → motive_4 t)
  (F_5 : (t : Array (Lean.Compiler.LCNF.Alt pu)) → Lean.Compiler.LCNF.Alt.below_1 t → motive_5 t)
  (F_6 : (t : List (Lean.Compiler.LCNF.Alt pu)) → Lean.Compiler.LCNF.Alt.below_2 t → motive_6 t),
  t.brecOn F_1 F_2 F_3 F_4 F_5 F_6 = F_2 t (Lean.Compiler.LCNF.FunDecl.brecOn.go t F_1 F_2 F_3 F_4 F_5 F_6).2
-- Mathlib.Geometry.Euclidean.Sphere.Power
/-- The power of a point is nonnegative if and only if the point lies outside or on the sphere.  -/
EuclideanGeometry.Sphere.power_nonneg_iff_radius_le_dist_center : ∀ {P : Type u_2} [inst : MetricSpace P] {s : EuclideanGeometry.Sphere P} {p : P},
  0 ≤ s.radius → (0 ≤ s.power p ↔ s.radius ≤ dist p s.center)
-- Aesop.Tree.TreeM
Aesop.TreeM.State : Type
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.support_nonempty : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {p : MvPolynomial σ R}, p.support.Nonempty ↔ p ≠ 0
-- Mathlib.CategoryTheory.GradedObject.Trifunctor
CategoryTheory.GradedObject.ι_mapBifunctor₁₂BifunctorDesc_assoc : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₁₂ : Type u_5}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} C₁₂] {F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)}
  {G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)} {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9}
  {J : Type u_10} {r : I₁ × I₂ × I₃ → J} {ρ₁₂ : CategoryTheory.GradedObject.BifunctorComp₁₂IndexData r}
  {X₁ : CategoryTheory.GradedObject I₁ C₁} {X₂ : CategoryTheory.GradedObject I₂ C₂}
  {X₃ : CategoryTheory.GradedObject I₃ C₃}
  [inst_5 : (((CategoryTheory.GradedObject.mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p]
  [inst_6 :
    (((CategoryTheory.GradedObject.mapBifunctor G ρ₁₂.I₁₂ I₃).obj
              (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj
          X₃).HasMap
      ρ₁₂.q]
  [H : CategoryTheory.GradedObject.HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃] {j : J} {A : C₄}
  (f :
    (i₁ : I₁) → (i₂ : I₂) → (i₃ : I₃) → r (i₁, i₂, i₃) = j → ((G.obj ((F₁₂.obj (X₁ i₁)).obj (X₂ i₂))).obj (X₃ i₃) ⟶ A))
  (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (h : r (i₁, i₂, i₃) = j) {Z : C₄} (h_1 : A ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.GradedObject.ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapBifunctor₁₂BifunctorDesc f) h_1) =
    CategoryTheory.CategoryStruct.comp (f i₁ i₂ i₃ h) h_1
-- Std.Time.Date.Basic
Std.Time.instHSubOffset_4 : HSub Std.Time.Hour.Offset Std.Time.Hour.Offset Std.Time.Hour.Offset
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Real.integral_rpowIntegrand₀₁_eq_rpow_mul_const : ∀ {p x : ℝ},
  p ∈ Set.Ioo 0 1 →
    0 ≤ x → ∫ (t : ℝ) in Set.Ioi 0, p.rpowIntegrand₀₁ t x = x ^ p * ∫ (t : ℝ) in Set.Ioi 0, p.rpowIntegrand₀₁ t 1
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.IsCharTwoJNeZeroNF.a₄ : ∀ {R : Type u_1} {inst : CommRing R} {W : WeierstrassCurve R} [self : W.IsCharTwoJNeZeroNF], W.a₄ = 0
-- Mathlib.Order.Interval.Basic
NonemptyInterval.coe_top_interval : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : BoundedOrder α], ↑⊤ = ⊤
-- Mathlib.Algebra.GCDMonoid.Multiset
Multiset.lcm_cons : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] (a : α) (s : Multiset α),
  (a ::ₘ s).lcm = lcm a s.lcm
-- Init.Data.SInt.Lemmas
Int16.minValue_le : ∀ (a : Int16), Int16.minValue ≤ a
-- Init.Data.List.Monadic
_private.Init.Data.List.Monadic.0.List.filterMap.match_1.eq_1 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (h_1 : Unit → motive none) (h_2 : (b : β) → motive (some b)),
  (match none with
    | none => h_1 ()
    | some b => h_2 b) =
    h_1 ()
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupSeminorm.sup_apply : ∀ {E : Type u_3} [inst : Group E] (p q : GroupSeminorm E) (x : E), (p ⊔ q) x = max (p x) (q x)
-- Mathlib.Algebra.GroupWithZero.Indicator
Set.indicator_mul : ∀ {ι : Type u_1} {M₀ : Type u_4} [inst : MulZeroClass M₀] (s : Set ι) (f g : ι → M₀),
  (s.indicator fun i => f i * g i) = fun i => s.indicator f i * s.indicator g i
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.congrRightₐ_apply_apply : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] {Z : Type u_6} (R : Type u_7) [inst_1 : CommSemiring R]
  [inst_2 : Semiring Y] [inst_3 : Algebra R Y] [inst_4 : Semiring Z] [inst_5 : Algebra R Z] (e : Y ≃ₐ[R] Z)
  (g : LocallyConstant X Y) (a : X), ((LocallyConstant.congrRightₐ R e) g) a = e (g a)
-- Batteries.Data.String.Lemmas
String.Pos.Raw.extract.go₁.eq_1 : ∀ (a a_1 a_2 : String.Pos.Raw), String.Pos.Raw.extract.go₁ [] a a_1 a_2 = []
-- Init.Data.Slice.List.Lemmas
List.toArray_mkSlice_roi_eq_toArray_mkSlice_rco : ∀ {α : Type u_1} {xs : List α} {lo : ℕ},
  Std.Slice.toArray (Std.Roi.Sliceable.mkSlice xs lo<...*) =
    Std.Slice.toArray (Std.Rco.Sliceable.mkSlice xs (lo + 1)...xs.length)
-- Mathlib.CategoryTheory.Core
CategoryTheory.Functor.core_comp_inclusion : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D),
  F.core.comp (CategoryTheory.Core.inclusion D) = (CategoryTheory.Core.inclusion C).comp F
-- Mathlib.GroupTheory.GroupAction.ConjAct
ConjAct.ofConjAct_toConjAct : ∀ {G : Type u_3} [inst : DivInvMonoid G] (x : G), ConjAct.ofConjAct (ConjAct.toConjAct x) = x
-- Lean.Parser.Basic
Lean.Parser.OrElseOnAntiquotBehavior.acceptLhs : Lean.Parser.OrElseOnAntiquotBehavior
-- Init.Data.List.Nat.TakeDrop
List.getElem?_take_eq_none : ∀ {α : Type u_1} {l : List α} {i j : ℕ}, i ≤ j → (List.take i l)[j]? = none
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.equiv_iff_toList_perm : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α],
  m₁.Equiv m₂ ↔ m₁.toList.Perm m₂.toList
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed
/-- If we have a map `G ⟶ G'` and a `DayConvolutionInternalHom F G' H'`, then
there is a unique map `H ⟶ H'` induced by functoriality of ends and functoriality
of `internalHomDiagramFunctor F`.  -/
CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.map : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {V : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} V] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          [inst_3 : CategoryTheory.MonoidalCategory V] →
            [inst_4 : CategoryTheory.MonoidalClosed V] →
              {F G H : CategoryTheory.Functor C V} →
                CategoryTheory.MonoidalCategory.DayConvolutionInternalHom F G H →
                  {G' H' : CategoryTheory.Functor C V} →
                    (G ⟶ G') → CategoryTheory.MonoidalCategory.DayConvolutionInternalHom F G' H' → (H ⟶ H')
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
Submodule.starProjection_mem_subspace_eq_self : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {K : Submodule 𝕜 E} [inst_3 : K.HasOrthogonalProjection] (v : ↥K), K.starProjection ↑v = ↑v
-- Mathlib.Data.Fin.Tuple.Take
Fin.take_eq_self : ∀ {n : ℕ} {α : Fin n → Sort u_1} (v : (i : Fin n) → α i), Fin.take n ⋯ v = v
-- Mathlib.GroupTheory.OreLocalization.Basic
/-- The subtraction in the Ore localization,
as a difference of an element of `X` and `S`.  -/
OreLocalization.«term_-ₒ_» : Lean.TrailingParserDescr
-- Mathlib.Algebra.Homology.HomologicalComplexBiprod
HomologicalComplex.instPreservesBinaryBiproductEval : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {c : ComplexShape ι} (K L : HomologicalComplex C c)
  [∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)] (i : ι),
  CategoryTheory.Limits.PreservesBinaryBiproduct K L (HomologicalComplex.eval C c i)
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.cancel_counitInv_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D) {X Y : D} (f f' : e.functor.obj (e.inverse.obj Y) ⟶ X),
  CategoryTheory.CategoryStruct.comp (e.counitInv.app Y) f = CategoryTheory.CategoryStruct.comp (e.counitInv.app Y) f' ↔
    f = f'
-- Mathlib.Algebra.Ring.Subring.Defs
Subring.coe_one : ∀ {R : Type u} [inst : NonAssocRing R] (s : Subring R), ↑1 = 1
-- Mathlib.Algebra.Group.Units.Basic
IsUnit.isUnit_iff_mulRight_bijective : ∀ {M : Type u_1} [inst : Monoid M] {a : M}, IsUnit a ↔ Function.Bijective fun x => x * a
-- Mathlib.Order.Nucleus
Nucleus.instPartialOrder : {X : Type u_1} → [inst : SemilatticeInf X] → PartialOrder (Nucleus X)
-- Mathlib.Algebra.Order.CompleteField
/-- There is a unique ordered ring homomorphism from an archimedean linear ordered field to a
conditionally complete linear ordered field.  -/
ConditionallyCompleteLinearOrderedField.uniqueOrderRingHom : (α : Type u_2) →
  (β : Type u_3) →
    [inst : Field α] →
      [inst_1 : LinearOrder α] →
        [IsStrictOrderedRing α] →
          [inst_3 : Field β] →
            [inst_4 : ConditionallyCompleteLinearOrder β] →
              [IsStrictOrderedRing β] → [Archimedean α] → Unique (α →+*o β)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- The left unitor isomorphism for binary coproducts with the initial object.  -/
CategoryTheory.Limits.coprod.leftUnitor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasBinaryCoproducts C] →
      [inst_2 : CategoryTheory.Limits.HasInitial C] → (P : C) → (⊥_ C) ⨿ P ≅ P
-- Mathlib.MeasureTheory.Integral.CircleIntegral
/-- For any circle integrable function `f`, the power series `cauchyPowerSeries f c R`, `R > 0`,
converges to the Cauchy integral `(2 * π * I : ℂ)⁻¹ • ∮ z in C(c, R), (z - w)⁻¹ • f z` on the open
disc `Metric.ball c R`.  -/
hasSum_cauchyPowerSeries_integral : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : ℂ → E} {c : ℂ} {R : ℝ} {w : ℂ},
  CircleIntegrable f c R →
    ‖w‖ < R →
      HasSum (fun n => (cauchyPowerSeries f c R n) fun x => w)
        ((2 * ↑Real.pi * Complex.I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - (c + w))⁻¹ • f z)
-- Mathlib.Order.BooleanAlgebra.Set
/-- **Alias** of `Set.insert_sdiff_insert`. -/
Set.insert_diff_insert : ∀ {α : Type u_1} {s t : Set α} {a : α}, insert a (s \ insert a t) = insert a (s \ t)
-- Mathlib.Algebra.Category.MonCat.Colimits
/-- The function from a given monoid in the diagram to the colimit monoid.  -/
MonCat.Colimits.coconeFun : {J : Type v} →
  [inst : CategoryTheory.Category.{u, v} J] →
    (F : CategoryTheory.Functor J MonCat) → (j : J) → ↑(F.obj j) → MonCat.Colimits.ColimitType F
-- Mathlib.Data.Prod.TProd
Set.mk_preimage_tprod : ∀ {ι : Type u} {α : ι → Type v} (l : List ι) (t : (i : ι) → Set (α i)),
  List.TProd.mk l ⁻¹' Set.tprod l t = {i | i ∈ l}.pi t
-- Mathlib.RingTheory.RingHom.Bijective
RingHom.Bijective.containsIdentities : RingHom.ContainsIdentities fun {R S} [CommRing R] [CommRing S] f => Function.Bijective ⇑f
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.coe_pow : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  (I : FractionalIdeal S P) (n : ℕ), ↑(I ^ n) = ↑I ^ n
-- Init.Conv
/-- `change t'` replaces the target `t` with `t'`,
assuming `t` and `t'` are definitionally equal.  -/
Lean.Parser.Tactic.Conv.change : Lean.ParserDescr
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.instInhabitedSyntheticMVarDecl.default : Lean.Elab.Term.SyntheticMVarDecl
-- Mathlib.CategoryTheory.Join.Pseudofunctor
_private.Mathlib.CategoryTheory.Join.Pseudofunctor.0.CategoryTheory.Join.id.match_1.eq_1 : ∀ {C : Type u_3} [inst : CategoryTheory.Category.{u_1, u_3} C] {D : Type u_4}
  [inst_1 : CategoryTheory.Category.{u_2, u_4} D] (motive : CategoryTheory.Join C D → Sort u_5) (x : C)
  (h_1 : (x : C) → motive (CategoryTheory.Join.left x)) (h_2 : (x : D) → motive (CategoryTheory.Join.right x)),
  (match CategoryTheory.Join.left x with
    | CategoryTheory.Join.left x => h_1 x
    | CategoryTheory.Join.right x => h_2 x) =
    h_1 x
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.Approx.CofixA.intro.injEq : ∀ {F : PFunctor.{uA, uB}} {n : ℕ} (a : F.A) (a_1 : F.B a → PFunctor.Approx.CofixA F n) (a_2 : F.A)
  (a_3 : F.B a_2 → PFunctor.Approx.CofixA F n),
  (PFunctor.Approx.CofixA.intro a a_1 = PFunctor.Approx.CofixA.intro a_2 a_3) = (a = a_2 ∧ a_1 ≍ a_3)
-- Mathlib.CategoryTheory.RegularCategory.Basic
/-- Given a morphism `f : A ⟶ B` and subobjects `A' ⟶ A` and `B' ⟶ B`, we have a canonical morphism
`(A' ⊓ (Subobject.pullback f).obj B') ⟶ ((«exists» f).obj A' ⊓ B')`.
This morphism is part of a `StrongEpiMonoFactorisation` of
`(A' ⊓ (Subobject.pullback f).obj B').arrow ≫ f`, see `frobeniusStrongEpiMonoFactorisation`.
 -/
CategoryTheory.Regular.frobeniusMorphism : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Regular C] →
      {A B : C} →
        (f : A ⟶ B) →
          (A' : CategoryTheory.Subobject A) →
            (B' : CategoryTheory.Subobject B) →
              CategoryTheory.Subobject.underlying.obj (A' ⊓ (CategoryTheory.Subobject.pullback f).obj B') ⟶
                CategoryTheory.Subobject.underlying.obj ((CategoryTheory.Subobject.exists f).obj A' ⊓ B')
-- Mathlib.Probability.Moments.IntegrableExpMul
ProbabilityTheory.integrable_pow_abs_mul_cexp_of_re_mem_interior_integrableExpSet : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {z : ℂ},
  z.re ∈ interior (ProbabilityTheory.integrableExpSet X μ) →
    ∀ (n : ℕ), MeasureTheory.Integrable (fun ω => ↑|X ω| ^ n * Complex.exp (z * ↑(X ω))) μ
-- Mathlib.Analysis.Calculus.ContDiff.Operations
/-- The negative of a `C^n` function at a point is `C^n` at this point.  -/
ContDiffAt.neg : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {x : E}
  {n : WithTop ℕ∞} {f : E → F}, ContDiffAt 𝕜 n f x → ContDiffAt 𝕜 n (fun x => -f x) x
-- Std.Data.ExtDHashMap.Lemmas
/-- Simpler variant of `get?_filter` when `LawfulBEq` is available.  -/
Std.ExtDHashMap.Const.get?_filter' : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : LawfulBEq α]
  {f : α → β → Bool} {k : α},
  Std.ExtDHashMap.Const.get? (Std.ExtDHashMap.filter f m) k = Option.filter (f k) (Std.ExtDHashMap.Const.get? m k)
-- Mathlib.Algebra.Order.Rearrangement
/-- **Strict inequality case of the Rearrangement Inequality**: Pointwise scalar multiplication of
`f` and `g`, which antivary together on `s`, is strictly decreased by a permutation if and only if
`f` and `g ∘ σ` do not antivary together on `s`. Stated by permuting the entries of `g`.  -/
AntivaryOn.sum_smul_lt_sum_smul_comp_perm_iff : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semiring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [ExistsAddOfLE α] [inst_4 : AddCommMonoid β] [inst_5 : LinearOrder β] [IsOrderedCancelAddMonoid β]
  [inst_7 : Module α β] [PosSMulStrictMono α β] {s : Finset ι} {σ : Equiv.Perm ι} {f : ι → α} {g : ι → β},
  AntivaryOn f g ↑s → {x | σ x ≠ x} ⊆ ↑s → (∑ i ∈ s, f i • g i < ∑ i ∈ s, f i • g (σ i) ↔ ¬AntivaryOn f (g ∘ ⇑σ) ↑s)
-- Mathlib.RingTheory.MvPolynomial.Basic
MvPolynomial.instCharP : ∀ (σ : Type u) (R : Type v) [inst : CommSemiring R] (p : ℕ) [CharP R p], CharP (MvPolynomial σ R) p
-- Mathlib.LinearAlgebra.Finsupp.Pi
Finsupp.submodule_top : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {α : Type u_5},
  (Finsupp.submodule fun x => ⊤) = ⊤
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.size_inter_le_size_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → (t₁ ∩ t₂).size ≤ t₂.size
-- Mathlib.Algebra.Ring.Divisibility.Lemmas
associated_abs_right_iff : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : LinearOrder R] {x y : R}, Associated x |y| ↔ Associated x y
-- Mathlib.Data.QPF.Univariate.Basic
QPF.Wequiv.brecOn : ∀ {F : Type u → Type v} [q : QPF F] {motive : (a a_1 : (QPF.P F).W) → QPF.Wequiv a a_1 → Prop} {a a_1 : (QPF.P F).W}
  (t : QPF.Wequiv a a_1),
  (∀ (a a_2 : (QPF.P F).W) (t : QPF.Wequiv a a_2), QPF.Wequiv.below t → motive a a_2 t) → motive a a_1 t
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.eraseManyEntries_impl_eq_foldl : ∀ {α : Type u} {β : α → Type v} {x : Ord α} {t₁ : Std.DTreeMap.Internal.Impl α β} (h₁ : t₁.Balanced)
  {t₂ : Std.DTreeMap.Internal.Impl α β},
  ↑(t₁.eraseManyEntries t₂ h₁) =
    Std.DTreeMap.Internal.Impl.foldl (fun acc k x_1 => Std.DTreeMap.Internal.Impl.erase! k acc) t₁ t₂
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
mvfderivWithin_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] [inst_5 : ChartedSpace H M] {F : Type u_8} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {x : M} {s : Set M}, UniqueMDiffAt[s] x → d[s] 0 x = 0