mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.Module.Complement
Submodule.projectionOntoL_surjective : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {p q : Submodule R M} (h : Submodule.IsTopCompl p q),
  Function.Surjective ⇑(p.projectionOntoL q h)
-- Mathlib.CategoryTheory.Monoidal.CommComon_
/-- A commutative comonoid object internal to a monoidal category.  -/
CategoryTheory.CommComon : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → [CategoryTheory.BraidedCategory C] → Type (max u₁ v₁)
-- Mathlib.Analysis.CStarAlgebra.Unitary.Maps
Unitary.mulLeft.congr_simp : ∀ (R : Type u_1) (A : Type u_2) [inst : NormedRing A] [inst_1 : StarRing A] [inst_2 : CStarRing A] [inst_3 : Ring R]
  [inst_4 : Module R A] [inst_5 : SMulCommClass R A A], Unitary.mulLeft R A = Unitary.mulLeft R A
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
/-- (Implementation)
The projection from the limit of `diagram_over_open` to a component of `D.U j`.  -/
AlgebraicGeometry.PresheafedSpace.GlueData.diagramOverOpenπ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (D : AlgebraicGeometry.PresheafedSpace.GlueData C) →
      [inst_1 : CategoryTheory.Limits.HasLimits C] →
        {i : D.J} →
          (U : TopologicalSpace.Opens ↑↑(D.U i)) →
            (j : D.J) →
              CategoryTheory.Limits.limit (D.diagramOverOpen U) ⟶
                (D.diagramOverOpen U).obj (Opposite.op (CategoryTheory.Limits.WalkingMultispan.right j))
-- Mathlib.RingTheory.Coalgebra.Hom
Coalgebra.counitCoalgHom_toLinearMap : ∀ (R : Type u) (A : Type v) [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : Coalgebra R A], ↑(Coalgebra.counitCoalgHom R A) = CoalgebraStruct.counit
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
SSet.prodStdSimplex.pairingCore.finset.congr_simp : ∀ {m : ℕ} {k : Fin (m + 1)} {n : ℕ} (x x_1 : ((SSet.horn (m + 1) k.castSucc).unionProd (SSet.boundary n)).N)
  (e_x : x = x_1) {d : ℕ} (hd : x.dim = d),
  SSet.prodStdSimplex.pairingCore.finset x hd = SSet.prodStdSimplex.pairingCore.finset x_1 ⋯
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.isPartition_single_iff : ∀ {ι : Type u_1} {I J : BoxIntegral.Box ι} (h : J ≤ I), (BoxIntegral.Prepartition.single I J h).IsPartition ↔ J = I
-- Mathlib.Algebra.Torsor.Basic
Equiv.right_vsub_pointReflection : ∀ {G : Type u_3} {P : Type u_4} [inst : AddGroup G] [T : AddTorsor G P] (x y : P),
  y -ᵥ (Equiv.pointReflection x) y = 2 • (y -ᵥ x)
-- Mathlib.GroupTheory.Congruence.Hom
AddCon.ker.eq_1 : ∀ {M : Type u_1} {N : Type u_2} {F : Type u_4} [inst : Add M] [inst_1 : Add N] [inst_2 : FunLike F M N]
  [inst_3 : AddHomClass F M N] (f : F), AddCon.ker f = { toSetoid := Setoid.ker ⇑f, add' := ⋯ }
-- Init.Data.String.Basic
String.Pos.cast_cast : ∀ {s t u : String} {hst : s = t} {htu : t = u} {pos : s.Pos}, (pos.cast hst).cast htu = pos.cast ⋯
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.zero_of_num_eq_bot : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  [IsDomain R] [Module.IsTorsionFree R P], 0 ∉ S → ∀ {I : FractionalIdeal S P}, I.num = ⊥ → I = 0
-- Mathlib.NumberTheory.RamificationInertia.Ramification
Ideal.ramificationIdx'_bot' : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] {p : Ideal R},
  p ≠ ⊥ → Function.Injective ⇑(algebraMap R S) → p.ramificationIdx' ⊥ = 0
-- Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
/-- Functor translating a functor into the category of comonoid objects
to a comonoid object in the functor category
 -/
_private.Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory.0.CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.inverse : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        [inst_2 : CategoryTheory.MonoidalCategory D] →
          CategoryTheory.Functor (CategoryTheory.Functor C (CategoryTheory.Comon D))
            (CategoryTheory.Comon (CategoryTheory.Functor C D))
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_inv_app : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] {F G : CategoryTheory.Pseudofunctor B CategoryTheory.Cat}
  (α : F ⟶ G) (a : B) (X : ↑(F.obj a)),
  (α.naturality (CategoryTheory.CategoryStruct.id a)).inv.toNatTrans.app X =
    CategoryTheory.CategoryStruct.comp ((G.mapId a).hom.toNatTrans.app ((α.app a).toFunctor.obj X))
      ((α.app a).toFunctor.map ((F.mapId a).inv.toNatTrans.app X))
-- Mathlib.GroupTheory.Perm.Sign
Equiv.Perm.signAux3_symm_trans_trans : ∀ {α : Type u} [inst : DecidableEq α] {β : Type v} [inst_1 : Finite α] [inst_2 : DecidableEq β] [inst_3 : Finite β]
  (f : Equiv.Perm α) (e : α ≃ β) {s : Multiset α} {t : Multiset β} (hs : ∀ (x : α), x ∈ s) (ht : ∀ (x : β), x ∈ t),
  Equiv.Perm.signAux3 ((e.symm.trans f).trans e) ht = f.signAux3 hs
-- Mathlib.Order.CompleteLattice.Lemmas
PUnit.instCompleteLinearOrder : CompleteLinearOrder PUnit.{u_8 + 1}
-- Std.Http.Data.Status
/-- Checks if the type of the status code is redirection, meaning that further action needs to be taken
to complete the request.

Reference: https://httpwg.org/specs/rfc9110.html#status.codes
 -/
Std.Http.Status.isRedirection : Std.Http.Status → Bool
-- Mathlib.RingTheory.MvPowerSeries.Substitution
MvPowerSeries.subst_pow : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] {τ : Type u_4} {S : Type u_5} [inst_1 : CommRing S]
  [inst_2 : Algebra R S] {a : σ → MvPowerSeries τ S},
  MvPowerSeries.HasSubst a →
    ∀ (f : MvPowerSeries σ R) (n : ℕ), MvPowerSeries.subst a (f ^ n) = MvPowerSeries.subst a f ^ n
-- Lean.Elab.InfoTree.Types
Lean.Elab.Info.ofDelabTermInfo.inj : ∀ {i i_1 : Lean.Elab.DelabTermInfo}, Lean.Elab.Info.ofDelabTermInfo i = Lean.Elab.Info.ofDelabTermInfo i_1 → i = i_1
-- Init.Data.Range.Polymorphic.SInt
Int8.instRxoHasSize : Std.Rxo.HasSize Int8
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalLeftAction.tensor_actionHomRight : ∀ {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.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] (x y : C) {z z' : D} (f : z ⟶ z'),
  CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight
      (CategoryTheory.MonoidalCategoryStruct.tensorObj x y) f =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso x y z).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight x
          (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight y f))
        (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso x y z').inv)
-- Mathlib.Algebra.Category.ModuleCat.Adjunctions
ModuleCat.free_map_apply : ∀ {R : Type u} [inst : Ring R] {X Y : Type u} (f : X ⟶ Y) (x : X),
  (CategoryTheory.ConcreteCategory.hom ((ModuleCat.free R).map f)) (ModuleCat.freeMk x) =
    ModuleCat.freeMk ((CategoryTheory.ConcreteCategory.hom f) x)
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
CategoryTheory.Oplax.LaxTrans.Modification.ext_iff : ∀ {B : Type u₁} {inst : CategoryTheory.Bicategory B} {C : Type u₂} {inst_1 : CategoryTheory.Bicategory C}
  {F G : CategoryTheory.OplaxFunctor B C} {η θ : F ⟶ G} {x y : CategoryTheory.Oplax.LaxTrans.Modification η θ},
  x = y ↔ x.app = y.app
-- Lean.Level
Lean.LevelMVarId.name : Lean.LevelMVarId → Lean.Name
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
StarAlgebra.elemental.characterSpaceToSpectrum.eq_1 : ∀ {A : Type u_1} [inst : CStarAlgebra A] (x : A) (φ : ↑(WeakDual.characterSpace ℂ ↥(StarAlgebra.elemental ℂ x))),
  StarAlgebra.elemental.characterSpaceToSpectrum x φ = ⟨φ ⟨x, ⋯⟩, ⋯⟩
-- Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
/-- A transfinite composition of shape `J` of morphisms in `W` induces a transfinite
composition of shape `Set.Iic j` (for any `j : J`).  -/
CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.iic : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {W : CategoryTheory.MorphismProperty C} →
      {J : Type w} →
        [inst_1 : LinearOrder J] →
          [inst_2 : SuccOrder J] →
            [inst_3 : OrderBot J] →
              [inst_4 : WellFoundedLT J] →
                {X Y : C} →
                  {f : X ⟶ Y} →
                    (h : W.TransfiniteCompositionOfShape J f) →
                      (j : J) → W.TransfiniteCompositionOfShape (↑(Set.Iic j)) (h.F.map (CategoryTheory.homOfLE ⋯))
-- Init.Data.Int.Order
Int.ge_of_eq : ∀ {a b : ℤ}, a = b → b ≤ a
-- Plausible.Gen
Plausible.instBEqGenError : BEq Plausible.GenError
-- Mathlib.Data.Fin.Basic
Fin.pos_of_ne_zero : ∀ {n : ℕ} {a : Fin (n + 1)}, a ≠ 0 → 0 < a
-- Mathlib.Util.Export
Lean.Export.State.mk.inj : ∀ {names : Lean.Export.Alloc Lean.Name} {levels : Lean.Export.Alloc Lean.Level} {exprs : Lean.Export.Alloc Lean.Expr}
  {defs : Std.HashSet Lean.Name} {stk : Array (Bool × Lean.Export.Entry)} {names_1 : Lean.Export.Alloc Lean.Name}
  {levels_1 : Lean.Export.Alloc Lean.Level} {exprs_1 : Lean.Export.Alloc Lean.Expr} {defs_1 : Std.HashSet Lean.Name}
  {stk_1 : Array (Bool × Lean.Export.Entry)},
  { names := names, levels := levels, exprs := exprs, defs := defs, stk := stk } =
      { names := names_1, levels := levels_1, exprs := exprs_1, defs := defs_1, stk := stk_1 } →
    names = names_1 ∧ levels = levels_1 ∧ exprs = exprs_1 ∧ defs = defs_1 ∧ stk = stk_1
-- Mathlib.Order.Hom.CompleteLattice
sSupHom.setImage_toFun : ∀ {α : Type u_2} {β : Type u_3} (f : α → β) (s : Set α), (sSupHom.setImage f) s = f '' s
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Finite
Set.infinite_smul_set : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] {a : G} {s : Set α},
  (a • s).Infinite ↔ s.Infinite
-- Mathlib.MeasureTheory.MeasurableSpace.Basic
Measurable.iSup' : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort uι} {mα : ι → MeasurableSpace α} {x : MeasurableSpace β} {f : α → β} (i₀ : ι),
  Measurable f → Measurable f
-- Mathlib.Algebra.Category.FGModuleCat.Basic
FGModuleCat.instIsMonoidalModuleCatIsFG : ∀ (R : Type u) [inst : CommRing R], (ModuleCat.isFG R).IsMonoidal
-- Mathlib.Algebra.Quaternion
Quaternion.imJ_one : ∀ {R : Type u_3} [inst : CommRing R], QuaternionAlgebra.imJ 1 = 0
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.IterM.foldM_filterM : ∀ {α β δ : Type w} {ps : Std.Do.PostShape} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''}
  [inst : Std.Iterator α m β] [Std.Iterators.Finite α m] [inst_2 : Monad m] [LawfulMonad m] [inst_4 : Monad n]
  [inst_5 : MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [inst_8 : Monad o] [LawfulMonad o]
  [inst_10 : Std.Do.WPMonad o ps] [inst_11 : Std.IteratorLoop α m n] [inst_12 : Std.IteratorLoop α m o]
  [Std.LawfulIteratorLoop α m n] [Std.LawfulIteratorLoop α m o] [inst_15 : MonadLiftT m n] [inst_16 : MonadLiftT n o]
  [LawfulMonadLiftT m n] [LawfulMonadLiftT n o] {f : β → n (ULift.{w, 0} Bool)} {g : δ → β → o δ} {init : δ}
  {it : Std.IterM m β} {P : Std.Do.Assertion ps} {Q : Std.Do.PostCond δ ps},
  ⦃P⦄
      Std.IterM.foldM
        (fun d b => do
          let __do_lift ← liftM (f b)
          if __do_lift.down = true then g d b else pure d)
        init it ⦃Q⦄ →
    ⦃P⦄ Std.IterM.foldM g init (Std.IterM.filterM f it) ⦃Q⦄
-- Init.Data.Range.Polymorphic.RangeIterator
_private.Init.Data.Range.Polymorphic.RangeIterator.0.Std.Rxc.Iterator.instIteratorLoop.loop.wf.match_1.splitter : {α : Type u_1} →
  (γ : Type u_1) →
    (Pl : α → γ → ForInStep γ → Prop) →
      (acc : γ) →
        (next : α) →
          (motive : { s // Pl next acc s } → Sort u_2) →
            (__do_lift : { s // Pl next acc s }) →
              ((acc' : γ) → (property : Pl next acc (ForInStep.yield acc')) → motive ⟨ForInStep.yield acc', property⟩) →
                ((acc' : γ) → (property : Pl next acc (ForInStep.done acc')) → motive ⟨ForInStep.done acc', property⟩) →
                  motive __do_lift
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
/-- `orthogonal.orthogonal` preserves the `≤` ordering of two
subspaces.  -/
Submodule.orthogonal_orthogonal_monotone : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {K₁ K₂ : Submodule 𝕜 E}, K₁ ≤ K₂ → K₁ᗮᗮ ≤ K₂ᗮᗮ
-- Mathlib.Data.Prod.Basic
Prod.swap_rightInverse : ∀ {α : Type u_1} {β : Type u_2}, Function.RightInverse Prod.swap Prod.swap
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.prod_le_prod_of_subset' : ∀ {ι : Type u_1} {M : Type u_4} [inst : CommMonoid M] [inst_1 : Preorder M] [CanonicallyOrderedMul M] {f : ι → M}
  {s t : Finset ι}, s ⊆ t → ∏ x ∈ s, f x ≤ ∏ x ∈ t, f x
-- Mathlib.RingTheory.AlgebraicIndependent.Basic
AlgebraicIndependent.of_ringHom_of_comp_eq : ∀ {ι : Type u} {R : Type u_2} {A : Type v} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  {S : Type u_3} {B : Type u_4} {FRS : Type u_5} {FAB : Type u_6} [inst_3 : CommRing S] [inst_4 : CommRing B]
  [inst_5 : Algebra S B] [inst_6 : FunLike FRS R S] [inst_7 : RingHomClass FRS R S] [inst_8 : FunLike FAB A B]
  [inst_9 : RingHomClass FAB A B] (f : FRS) (g : FAB),
  AlgebraicIndependent S (⇑g ∘ x) →
    Function.Injective ⇑f → (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A) → AlgebraicIndependent R x
-- Mathlib.GroupTheory.Commutator.Basic
Subgroup.commutator_comm_le : ∀ {G : Type u_1} [inst : Group G] (H₁ H₂ : Subgroup G), ⁅H₁, H₂⁆ ≤ ⁅H₂, H₁⁆
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.ofFractionRing_mul : ∀ {K : Type u} [inst : CommRing K] (p q : FractionRing (Polynomial K)),
  { toFractionRing := p * q } = { toFractionRing := p } * { toFractionRing := q }
-- Init.Prelude
/-- The byte position of the start of the string slice.  -/
Substring.Raw.startPos : Substring.Raw → String.Pos.Raw
-- Mathlib.RingTheory.FractionalIdeal.Operations
IsFractional.div_of_nonzero : ∀ {R₁ : Type u_3} [inst : CommRing R₁] {K : Type u_4} [inst_1 : Field K] [inst_2 : Algebra R₁ K] [IsFractionRing R₁ K]
  [IsDomain R₁] {I J : Submodule R₁ K},
  IsFractional (nonZeroDivisors R₁) I →
    IsFractional (nonZeroDivisors R₁) J → J ≠ 0 → IsFractional (nonZeroDivisors R₁) (I / J)
-- Mathlib.LinearAlgebra.Projection
LinearMap.IsProj.codRestrict_apply_cod : ∀ {S : Type u_5} [inst : Semiring S] {M : Type u_6} [inst_1 : AddCommMonoid M] [inst_2 : Module S M] {m : Submodule S M}
  {f : M →ₗ[S] M} (h : LinearMap.IsProj m f) (x : ↥m), h.codRestrict ↑x = x
-- Mathlib.Geometry.Convex.Cone.Basic
ConvexCone.mem_top : ∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommMonoid M]
  [inst_3 : SMul R M] {x : M}, x ∈ ⊤
-- Mathlib.GroupTheory.Nilpotent
/-- If two different elements of the `upperCentralSeries` of an additive group `G`
are equal, then they are all equal, starting from the smaller index.  -/
AddSubgroup.upperCentralSeries.eq_ge_of_eq_gt : ∀ {G : Type u_1} [inst : AddGroup G] {a b c : ℕ},
  a ≠ b →
    a ≤ c →
      AddSubgroup.upperCentralSeries G a = AddSubgroup.upperCentralSeries G b →
        AddSubgroup.upperCentralSeries G a = AddSubgroup.upperCentralSeries G c
-- Aesop.Tree.Data
Aesop.GoalState.isUnknown : Aesop.GoalState → Bool
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.degree_pos_iff_exists_adj : ∀ {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} {v : V} [inst : Fintype ↑(G'.neighborSet v)],
  0 < G'.degree v ↔ ∃ w, G'.Adj v w
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
_private.Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop.0.Std.IterM.toArray_eq_match_step.match_1.eq_1 : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} (motive : Std.IterStep (Std.IterM m β) β → Sort u_3) (it' : Std.IterM m β)
  (out : β) (h_1 : (it' : Std.IterM m β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.IterM m β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.yield it' out with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_1 it' out
-- Mathlib.AlgebraicGeometry.Limits
AlgebraicGeometry.ι_right_coprodIsoSigma_inv : ∀ (X Y : AlgebraicGeometry.Scheme),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.Sigma.ι (fun i => CategoryTheory.Limits.WalkingPair.casesOn i.down X Y)
        { down := CategoryTheory.Limits.WalkingPair.right })
      (AlgebraicGeometry.coprodIsoSigma X Y).inv =
    CategoryTheory.Limits.coprod.inr
-- Mathlib.Analysis.SpecialFunctions.Sigmoid
AnalyticOnNhd.sigmoid : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {s : Set E},
  AnalyticOnNhd ℝ f s → AnalyticOnNhd ℝ (Real.sigmoid ∘ f) s
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
FormalMultilinearSeries.hasFDerivAt_sum : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type v} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  {p : FormalMultilinearSeries 𝕜 E F} {x : E} [CompleteSpace F],
  ‖x‖ₑ < p.radius → HasFDerivAt p.sum (p.derivSeries.sum x) x
-- Mathlib.Analysis.Convex.Gauge
Convex.lipschitzWith_gauge : ∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {s : Set E} {r : NNReal},
  Convex ℝ s → 0 < r → Metric.ball 0 ↑r ⊆ s → LipschitzWith r⁻¹ (gauge s)
-- Mathlib.Analysis.CStarAlgebra.Multiplier
/-- For `a : 𝓜(𝕜, A)`, the norms of `a.fst` and `a.snd` coincide, and hence these
also coincide with `‖a‖` which is `max (‖a.fst‖) (‖a.snd‖)`.  -/
DoubleCentralizer.norm_fst_eq_snd : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : NormedSpace 𝕜 A] [inst_3 : SMulCommClass 𝕜 A A] [inst_4 : IsScalarTower 𝕜 A A] [inst_5 : StarRing A]
  [CStarRing A] (a : DoubleCentralizer 𝕜 A), ‖a.toProd.1‖ = ‖a.toProd.2‖
-- Init.Data.Slice.Basic
Std.Slice.Self.mk : ∀ {α : Type u} {β : outParam (Type u)}, autoParam (α = β) Std.Slice.Self.eq._autoParam → Std.Slice.Self α β
-- Mathlib.CategoryTheory.EpiMono
/-- Every iso is a split mono.  -/
CategoryTheory.IsSplitMono.of_iso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : Y ⟶ X) [CategoryTheory.IsIso f],
  CategoryTheory.IsSplitMono f
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem_alter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k k' : α}
  {f : Option β → Option β} {hc : k' ∈ t.alter k f},
  (t.alter k f)[k'] = if heq : cmp k k' = Ordering.eq then (f t[k]?).get ⋯ else t[k']
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.extendScalars_comp_id : ∀ {R₁ R₂ : Type u₁} [inst : CommRing R₁] [inst_1 : CommRing R₂] (f₁₂ : R₁ →+* R₂),
  CategoryTheory.CategoryStruct.comp (ModuleCat.extendScalarsComp f₁₂ (RingHom.id R₂)).hom
      (CategoryTheory.CategoryStruct.comp ((ModuleCat.extendScalars f₁₂).whiskerLeft (ModuleCat.extendScalarsId R₂).hom)
        (ModuleCat.extendScalars f₁₂).rightUnitor.hom) =
    CategoryTheory.CategoryStruct.id (ModuleCat.extendScalars ((RingHom.id R₂).comp f₁₂))
-- Mathlib.Data.Sym.Sym2
Sym2.fromRel_bot : ∀ {α : Type u_1}, Sym2.fromRel ⋯ = ∅
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.leadingTerm_eq_leadingTerm_iff : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] {p q : MvPolynomial σ R},
  m.leadingTerm p = m.leadingTerm q ↔ m.leadingCoeff p = m.leadingCoeff q ∧ m.degree p = m.degree q
-- Mathlib.CategoryTheory.Generator.Indization
CategoryTheory.Ind.isSeparating_range_yoneda : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  (CategoryTheory.ObjectProperty.ofObj CategoryTheory.Ind.yoneda.obj).IsSeparating
-- Mathlib.Topology.Constructions
Continuous.finSnoc : ∀ {X : Type u} [inst : TopologicalSpace X] {n : ℕ} {A : Fin (n + 1) → Type u_9}
  [inst_1 : (i : Fin (n + 1)) → TopologicalSpace (A i)] {f : X → (j : Fin n) → A j.castSucc} {g : X → A (Fin.last n)},
  Continuous f → Continuous g → Continuous fun a => Fin.snoc (f a) (g a)
-- Mathlib.Geometry.Manifold.Algebra.Monoid
instOneContMDiffMonoidMorphism : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {n : WithTop ℕ∞} →
      {H : Type u_2} →
        [inst_1 : TopologicalSpace H] →
          {E : Type u_3} →
            [inst_2 : NormedAddCommGroup E] →
              [inst_3 : NormedSpace 𝕜 E] →
                {I : ModelWithCorners 𝕜 E H} →
                  {G : Type u_4} →
                    [inst_4 : Monoid G] →
                      [inst_5 : TopologicalSpace G] →
                        [inst_6 : ChartedSpace H G] →
                          {H' : Type u_5} →
                            [inst_7 : TopologicalSpace H'] →
                              {E' : Type u_6} →
                                [inst_8 : NormedAddCommGroup E'] →
                                  [inst_9 : NormedSpace 𝕜 E'] →
                                    {I' : ModelWithCorners 𝕜 E' H'} →
                                      {G' : Type u_7} →
                                        [inst_10 : Monoid G'] →
                                          [inst_11 : TopologicalSpace G'] →
                                            [inst_12 : ChartedSpace H' G'] → One (ContMDiffMonoidMorphism I I' n G G')
-- Mathlib.RingTheory.LocalRing.RingHom.Basic
IsLocalRing.map_maximalIdeal_of_surjective : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : IsLocalRing R]
  [inst_3 : IsLocalRing S] (f : R →+* S),
  Function.Surjective ⇑f → Ideal.map f (IsLocalRing.maximalIdeal R) = IsLocalRing.maximalIdeal S
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
OpenPartialHomeomorph.pi.congr_simp : ∀ {ι : Type u_7} [inst : Finite ι] {X : ι → Type u_8} {Y : ι → Type u_9} [inst_1 : (i : ι) → TopologicalSpace (X i)]
  [inst_2 : (i : ι) → TopologicalSpace (Y i)] (ei ei_1 : (i : ι) → OpenPartialHomeomorph (X i) (Y i)),
  ei = ei_1 → OpenPartialHomeomorph.pi ei = OpenPartialHomeomorph.pi ei_1
-- Lean.Server.Requests
Lean.Server.instInhabitedServerRequestResponse.default : {α : Type} → Lean.Server.ServerRequestResponse α
-- Init.Data.NeZero
instNeZeroNatHAdd_1 : ∀ {n m : ℕ} [h : NeZero m], NeZero (n + m)
-- Mathlib.CategoryTheory.EffectiveEpi.Preserves
CategoryTheory.Functor.ReflectsEffectiveEpiFamilies.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D},
  (∀ {α : Type u} {B : C} (X : α → C) (π : (a : α) → X a ⟶ B),
      (CategoryTheory.EffectiveEpiFamily (fun a => F.obj (X a)) fun a => F.map (π a)) →
        CategoryTheory.EffectiveEpiFamily X π) →
    F.ReflectsEffectiveEpiFamilies
-- Mathlib.RingTheory.Valuation.ValuationRing
PreValuationRing.cond' : ∀ {A : Type u} {inst : Mul A} [self : PreValuationRing A] (a b : A), ∃ c, a * c = b ∨ b * c = a
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts
CategoryTheory.Limits.PreservesLimitPair.iso_inv_snd_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) (X Y : C) [inst_2 : CategoryTheory.Limits.HasBinaryProduct X Y]
  [inst_3 : CategoryTheory.Limits.HasBinaryProduct (G.obj X) (G.obj Y)]
  [inst_4 : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.pair X Y) G] {Z : D} (h : G.obj Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesLimitPair.iso G X Y).inv
      (CategoryTheory.CategoryStruct.comp (G.map CategoryTheory.Limits.prod.snd) h) =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd h
-- Mathlib.Logic.Equiv.Basic
Equiv.piCongrLeft'_refl : ∀ {α : Sort u_1} (P : α → Sort u_9), Equiv.piCongrLeft' P (Equiv.refl α) = Equiv.refl ((a : α) → P a)
-- Init.Data.UInt.Lemmas
UInt32.neg_mul_neg : ∀ (a b : UInt32), -a * -b = a * b