mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.BifunctorAssociator
/-- Given bifunctors `F : C₁ ⥤ C₂₃ ⥤ C₄`, `G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃`, homological complexes
`K₁ : HomologicalComplex C₁ c₁`, `K₂ : HomologicalComplex C₂ c₂` and
`K₃ : HomologicalComplex C₃ c₃`, and complexes shapes `c₁₂`, `c₂₃`, `c₄`
with `ComplexShape.Associative c₁ c₂ c₃ c₁₂ c₂₃ c₄`, this asserts that for
all `i₁ : ι₁` and `i₂₃ : ι₂₃`, the functor `F(K₁.X i₁, _)` commutes with
the coproducts of the `G₂₃(K₂.X i₂, K₃.X i₃)`
such that `π c₂ c₃ c₂₃ ⟨i₂, i₃⟩ = i₂₃`.  -/
HomologicalComplex.HasGoodTrifunctor₂₃Obj : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {C₂₃ : Type u_4} →
      {C₃ : Type u_5} →
        {C₄ : Type u_6} →
          [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
            [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
              [inst_2 : CategoryTheory.Category.{v_3, u_5} C₃] →
                [inst_3 : CategoryTheory.Category.{v_4, u_6} C₄] →
                  [inst_4 : CategoryTheory.Category.{v_6, u_4} C₂₃] →
                    [inst_5 : CategoryTheory.Limits.HasZeroMorphisms C₁] →
                      [inst_6 : CategoryTheory.Limits.HasZeroMorphisms C₂] →
                        [inst_7 : CategoryTheory.Limits.HasZeroMorphisms C₃] →
                          CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄) →
                            CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃) →
                              {ι₁ : Type u_7} →
                                {ι₂ : Type u_8} →
                                  {ι₃ : Type u_9} →
                                    {ι₁₂ : Type u_10} →
                                      {ι₂₃ : Type u_11} →
                                        {ι₄ : Type u_12} →
                                          {c₁ : ComplexShape ι₁} →
                                            {c₂ : ComplexShape ι₂} →
                                              {c₃ : ComplexShape ι₃} →
                                                HomologicalComplex C₁ c₁ →
                                                  HomologicalComplex C₂ c₂ →
                                                    HomologicalComplex C₃ c₃ →
                                                      (c₁₂ : ComplexShape ι₁₂) →
                                                        (c₂₃ : ComplexShape ι₂₃) →
                                                          (c₄ : ComplexShape ι₄) →
                                                            [inst : TotalComplexShape c₁ c₂ c₁₂] →
                                                              [inst_8 : TotalComplexShape c₁₂ c₃ c₄] →
                                                                [inst_9 : TotalComplexShape c₂ c₃ c₂₃] →
                                                                  [inst_10 : TotalComplexShape c₁ c₂₃ c₄] →
                                                                    [c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄] → Prop
-- Mathlib.RingTheory.Polynomial.GaussNorm
/-- If `v` is a nonarchimedean absolute value, then the Gauss norm is multiplicative.  -/
Polynomial.gaussNorm_mul : ∀ {c : ℝ} {R : Type u_3} [inst : Ring R] {v : AbsoluteValue R ℝ},
  IsNonarchimedean ⇑v →
    0 < c →
      ∀ (p q : Polynomial R), Polynomial.gaussNorm v c (p * q) = Polynomial.gaussNorm v c p * Polynomial.gaussNorm v c q
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.map_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (g : β → γ) (f : α → β),
  FreeMonoid.map (g ∘ f) = (FreeMonoid.map g).comp (FreeMonoid.map f)
-- Mathlib.Algebra.Order.IsBotOne
max_zero : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : Zero α] [IsBotZeroClass α] (a : α), max a 0 = a
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
hasProdUniformly_iff_tendstoUniformly : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : CommMonoid α] {f : ι → β → α} {g : β → α}
  [inst_1 : UniformSpace α], HasProdUniformly f g ↔ TendstoUniformly (fun x1 x2 => ∏ i ∈ x1, f i x2) g Filter.atTop
-- Mathlib.Order.Category.DistLat
/-- Turn a morphism in `DistLat` back into a `LatticeHom`.  -/
DistLat.Hom.hom : {X Y : DistLat} → X.Hom Y → LatticeHom ↑X ↑Y
-- Mathlib.Analysis.Calculus.FormalMultilinearSeries
/-- Product of formal multilinear series (with the same field `𝕜` and the same source
space, but possibly different target spaces).  -/
FormalMultilinearSeries.pi : {𝕜 : Type u} →
  {E : Type v} →
    [inst : Semiring 𝕜] →
      [inst_1 : AddCommMonoid E] →
        [inst_2 : Module 𝕜 E] →
          [inst_3 : TopologicalSpace E] →
            [inst_4 : ContinuousAdd E] →
              [inst_5 : ContinuousConstSMul 𝕜 E] →
                {ι : Type u_1} →
                  {F : ι → Type u_2} →
                    [inst_6 : (i : ι) → AddCommGroup (F i)] →
                      [inst_7 : (i : ι) → Module 𝕜 (F i)] →
                        [inst_8 : (i : ι) → TopologicalSpace (F i)] →
                          [inst_9 : ∀ (i : ι), IsTopologicalAddGroup (F i)] →
                            [inst_10 : ∀ (i : ι), ContinuousConstSMul 𝕜 (F i)] →
                              ((i : ι) → FormalMultilinearSeries 𝕜 E (F i)) →
                                FormalMultilinearSeries 𝕜 E ((i : ι) → F i)
-- Mathlib.CategoryTheory.Monoidal.Action.Opposites
CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftActionOfMonoidalOppositeRightAction_actionUnitIso : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction Cᴹᵒᵖ D] (x : D),
  CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso x =
    CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso x
-- Mathlib.Analysis.Normed.Field.Ultra
IsUltrametricDist.isUltrametricDist_of_forall_norm_add_one_of_norm_le_one : ∀ {R : Type u_1} [inst : NormedDivisionRing R], (∀ (x : R), ‖x‖ ≤ 1 → ‖x + 1‖ ≤ 1) → IsUltrametricDist R
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.instToJsonWorkspaceClientCapabilities.toJson : Lean.Lsp.WorkspaceClientCapabilities → Lean.Json
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
/-- The images of `plusPart` by `negAt` are pairwise disjoint.  -/
NumberField.mixedEmbedding.disjoint_negAt_plusPart : ∀ {K : Type u_1} [inst : Field K] (A : Set (NumberField.mixedEmbedding.mixedSpace K)),
  Pairwise
    (Function.onFun Disjoint fun s => ⇑(NumberField.mixedEmbedding.negAt s) '' NumberField.mixedEmbedding.plusPart A)
-- Mathlib.Data.Num.Lemmas
Num.size_eq_natSize : ∀ (n : Num), ↑n.size = n.natSize
-- Mathlib.Data.Fin.Embedding
Fin.nonempty_embedding_iff : ∀ {n m : ℕ}, Nonempty (Fin n ↪ Fin m) ↔ n ≤ m
-- Std.Http.Protocol.H1
/-- Takes and clears accumulated output bytes, returning them as a buffer.
 -/
Std.Http.Protocol.H1.Machine.takeOutput : {dir : Std.Http.Protocol.H1.Direction} →
  Std.Http.Protocol.H1.Machine dir → Std.Http.Protocol.H1.Machine dir × Std.Http.Internal.ChunkedBuffer
-- Mathlib.Topology.EMetricSpace.Diam
/-- **Alias** of `Metric.ediam_le`.

---

If the distance between any two points in a set is bounded by some constant, this constant
bounds the diameter.  -/
EMetric.diam_le : ∀ {X : Type u_2} {s : Set X} [inst : PseudoEMetricSpace X] {d : ENNReal},
  (∀ x ∈ s, ∀ y ∈ s, edist x y ≤ d) → Metric.ediam s ≤ d
-- Mathlib.Geometry.Convex.Cone.Basic
ConvexCone.pointed_iff_not_blunt : ∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommMonoid M]
  [inst_3 : SMul R M] {C : ConvexCone R M}, C.Pointed ↔ ¬C.Blunt
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.summable_mul : ∀ {α : Type u_3} {E : α → Type u_4} [inst : (i : α) → NormedAddCommGroup (E i)] {p q : ENNReal},
  p.toReal.HolderConjugate q.toReal → ∀ (f : ↥(lp E p)) (g : ↥(lp E q)), Summable fun i => ‖↑f i‖ * ‖↑g i‖
-- Mathlib.Tactic.Translate.TagUnfoldBoundary
_private.Mathlib.Tactic.Translate.TagUnfoldBoundary.0.Mathlib.Tactic.Translate.CastKind.refoldFun.sizeOf_spec : sizeOf Mathlib.Tactic.Translate.CastKind.refoldFun✝ = 1
-- Mathlib.Topology.Category.TopCommRingCat
TopCommRingCat.forgetToCommRingCatTopologicalSpace : (R : TopCommRingCat) → TopologicalSpace ↑((CategoryTheory.forget₂ TopCommRingCat CommRingCat).obj R)
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Hom.toLRSHom' : {X Y : AlgebraicGeometry.Scheme} → X.Hom Y → X.Hom Y.toLocallyRingedSpace
-- Mathlib.RingTheory.AlgebraicIndependent.Basic
algebraicIndependent_iff_ker_eq_bot : ∀ {ι : Type u} {R : Type u_2} {A : Type v} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A],
  AlgebraicIndependent R x ↔ RingHom.ker (MvPolynomial.aeval x).toRingHom = ⊥
-- Mathlib.Algebra.Field.Subfield.Basic
Subfield.smulCommClass_right : ∀ {K : Type u} [inst : DivisionRing K] {X : Type u_1} {Y : Type u_2} [inst_1 : SMul X Y] [inst_2 : SMul K Y]
  [SMulCommClass X K Y] (F : Subfield K), SMulCommClass X (↥F) Y
-- Std.Sat.AIG.CNF
/-- The `Cache` invariant always holds for an empty CNF when all nodes are unmarked.
 -/
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.Cache.Inv_init : ∀ {aig : Std.Sat.AIG ℕ}, Std.Sat.AIG.toCNF.Cache.Inv✝ aig Std.Sat.CNF.empty (Array.replicate aig.decls.size false) ⋯
-- Mathlib.SetTheory.Cardinal.Divisibility
Cardinal.is_prime_iff : ∀ {a : Cardinal.{u_1}}, Prime a ↔ Cardinal.aleph0 ≤ a ∨ ∃ p, a = ↑p ∧ Nat.Prime p
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- Structure expressing a symmetry of `I : MultispanIndex (.prod ι) C` which
allows to compare the corresponding multicoequalizer to the multicoequalizer
of `I.toLinearOrder`.  -/
CategoryTheory.Limits.MultispanIndex.SymmStruct : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {ι : Type w} → CategoryTheory.Limits.MultispanIndex (CategoryTheory.Limits.MultispanShape.prod ι) C → Type (max v w)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.preimage_mul_left_one : ∀ {α : Type u_2} [inst : Group α] {a : α}, Finset.preimage 1 (fun x => a * x) ⋯ = {a⁻¹}
-- Mathlib.Data.Stream.Init
Stream'.tail_drop' : ∀ {α : Type u} {i : ℕ} {s : Stream' α}, (Stream'.drop i s).tail = Stream'.drop (i + 1) s
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.IsSFiniteKernel.fst : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α (β × γ)) [ProbabilityTheory.IsSFiniteKernel κ],
  ProbabilityTheory.IsSFiniteKernel κ.fst
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.not_mem_of_isEmpty : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {a : α}, m.isEmpty = true → a ∉ m
-- Mathlib.RingTheory.LocalProperties.Basic
IsLocalization.Away.tensorRightEquiv.congr_simp : ∀ {R : Type u_7} (S : Type u_8) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (r : R)
  (A : Type u_9) [inst_3 : CommSemiring A] [inst_4 : Algebra R A] [inst_5 : IsLocalization.Away r A],
  IsLocalization.Away.tensorRightEquiv S r A = IsLocalization.Away.tensorRightEquiv S r A
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
/-- The cofan for `summand N Δ` induced by morphisms `N n ⟶ X _⦋n⦌` for all `n : ℕ`.  -/
CategoryTheory.SimplicialObject.Splitting.cofan' : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (N : ℕ → C) →
      (X : CategoryTheory.SimplicialObject C) →
        ((n : ℕ) → N n ⟶ X.obj (Opposite.op { len := n })) →
          (Δ : SimplexCategoryᵒᵖ) → CategoryTheory.Limits.Cofan (CategoryTheory.SimplicialObject.Splitting.summand N Δ)
-- Mathlib.Algebra.Category.MonCat.Colimits
MonCat.Colimits.descFunLift.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.Category.{u, v} J] (F : CategoryTheory.Functor J MonCat)
  (s : CategoryTheory.Limits.Cocone F) (j : J) (x_1 : ↑(F.obj j)),
  MonCat.Colimits.descFunLift F s (MonCat.Colimits.Prequotient.of j x_1) =
    (CategoryTheory.ConcreteCategory.hom (s.ι.app j)) x_1
-- Mathlib.Order.InitialSeg
InitialSeg.eq : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder β s] (f g : InitialSeg r s) (a : α),
  f a = g a
-- Aesop.Tree.Data
Aesop.Goal : Type
-- Mathlib.Order.Filter.Lift
Filter.lift'_top : ∀ {α : Type u_1} {β : Type u_2} (h : Set α → Set β), ⊤.lift' h = Filter.principal (h Set.univ)
-- Lean.Meta.Match.Basic
Lean.Meta.Match.instantiatePatternMVars : Lean.Meta.Match.Pattern → Lean.MetaM Lean.Meta.Match.Pattern
-- Mathlib.MeasureTheory.PiSystem
/-- **Alias** of `MeasurableSpace.DynkinSystem.has_sdiff`. -/
MeasurableSpace.DynkinSystem.has_diff : ∀ {α : Type u_3} (d : MeasurableSpace.DynkinSystem α) {s₁ s₂ : Set α}, d.Has s₁ → d.Has s₂ → s₂ ⊆ s₁ → d.Has (s₁ \ s₂)
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.map_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C CategoryTheory.Cat} {α : F ⟶ G}
  {X Y : CategoryTheory.Grothendieck F} {f : X ⟶ Y},
  (CategoryTheory.Grothendieck.map α).map f =
    { base := f.base,
      fiber :=
        CategoryTheory.CategoryStruct.comp ((CategoryTheory.eqToHom ⋯).toNatTrans.app X.fiber)
          ((α.app Y.base).toFunctor.map f.fiber) }
-- Mathlib.CategoryTheory.Bicategory.LocallyGroupoid
CategoryTheory.Bicategory.Pith.instInhabited : (B : Type u₁) → [Inhabited B] → Inhabited (CategoryTheory.Bicategory.Pith B)
-- Mathlib.GroupTheory.GroupExtension.Defs
/-- `GroupExtension N E G` is a short exact sequence of groups `1 → N → E → G → 1`.  -/
GroupExtension : (N : Type u_1) → (E : Type u_2) → (G : Type u_3) → [Group N] → [Group E] → [Group G] → Type (max (max u_1 u_2) u_3)
-- Init.Core
/-- A dependent recursion principle for `Quotient`. It is analogous to the
[recursor](https://lean-lang.org/doc/reference/4.33.0/find/?domain=Verso.Genre.Manual.section&name=recursors) for a structure, and can be used when the resulting type
is not necessarily a proposition.

While it is very general, this recursor can be tricky to use. The following simpler alternatives may
be easier to use:

 * `Quotient.lift` is useful for defining non-dependent functions.
 * `Quotient.ind` is useful for proving theorems about quotients.
 * `Quotient.recOnSubsingleton` can be used whenever the target type is a `Subsingleton`.
 * `Quotient.hrecOn` uses heterogeneous equality instead of rewriting with `Quotient.sound`.

`Quotient.recOn` is a version of this recursor that takes the quotient parameter first.
 -/
Quotient.rec : {α : Sort u} →
  {s : Setoid α} →
    {motive : Quotient s → Sort v} →
      (f : (a : α) → motive ⟦a⟧) → (∀ (a b : α) (p : a ≈ b), ⋯ ▸ f a = f b) → (q : Quotient s) → motive q
-- Mathlib.Data.Fintype.EquivFin
Infinite.sigma_of_right : ∀ {α : Type u_1} {β : α → Type u_4} {a : α} [Infinite (β a)], Infinite ((a : α) × β a)
-- Lean.Parser.Extra
Lean.Parser.rawIdent.formatter : Lean.PrettyPrinter.Formatter
-- Init.Internal.Order.Lemmas
Lean.Order.List.monotone_filterAuxM : ∀ {γ : Type w} [inst : Lean.Order.PartialOrder γ] {m : Type → Type v} [inst_1 : Monad m]
  [inst_2 : (α : Type) → Lean.Order.PartialOrder (m α)] [Lean.Order.MonoBind m] {α : Type} (f : γ → α → m Bool)
  (xs acc : List α), Lean.Order.monotone f → Lean.Order.monotone fun x => List.filterAuxM (f x) xs acc
-- Mathlib.LinearAlgebra.Basis.Defs
/-- A `Basis ι R M` for a module `M` is the type of `ι`-indexed `R`-bases of `M`.

The basis vectors are available as `DFunLike.coe (b : Basis ι R M) : ι → M`.
To turn a linear independent family of vectors spanning `M` into a basis, use `Basis.mk`.
They are internally represented as linear equivs `M ≃ₗ[R] (ι →₀ R)`,
available as `Basis.repr`.
 -/
Module.Basis : Type u_1 →
  (R : Type u_3) →
    (M : Type u_6) → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [Module R M] → Type (max (max u_1 u_3) u_6)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SymbolKind.field : Lean.Lsp.SymbolKind
-- Mathlib.LinearAlgebra.FiniteDimensional.Defs
/-- Finite dimensionality is preserved under linear equivalence.  -/
LinearEquiv.finiteDimensional : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {V₂ : Type v'}
  [inst_3 : AddCommGroup V₂] [inst_4 : Module K V₂] (f : V ≃ₗ[K] V₂) [FiniteDimensional K V], FiniteDimensional K V₂
-- Std.Data.ExtDTreeMap.Basic
/-- Tries to retrieve the key-value pair with the smallest key that is greater than or equal to the
given key, panicking if no such pair exists.
 -/
Std.ExtDTreeMap.getEntryGE! : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} → [Std.TransCmp cmp] → [Inhabited (Sigma β)] → Std.ExtDTreeMap α β cmp → α → (a : α) × β a
-- Mathlib.RingTheory.Localization.Away.Basic
selfZPow_natCast : ∀ {R : Type u_1} [inst : CommSemiring R] (x : R) (B : Type u_2) [inst_1 : CommSemiring B] [inst_2 : Algebra R B]
  [inst_3 : IsLocalization.Away x B] (d : ℕ), selfZPow x B ↑d = (algebraMap R B) x ^ d
-- Mathlib.RingTheory.RamificationInertia.Ramification
Ideal.ramificationIdx_above_le : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [IsScalarTower R S T] (q : Ideal S) (r : Ideal T)
  [r.IsPrime] [r.LiesOver q] [Module.Finite R T] [Module.Flat S T], r.ramificationIdx S ≤ r.ramificationIdx R
-- Init.Data.Int.DivMod.Lemmas
Int.add_one_tdiv : ∀ {a b : ℤ}, (a + 1).tdiv b = a.tdiv b + if 0 < a + 1 ∧ b ∣ a + 1 ∨ a < 0 ∧ b ∣ a then b.sign else 0
-- Init.Data.Array.Attach
Array.attachWith_map_subtype_val : ∀ {α : Type u_1} {p : α → Prop} {xs : Array α} (H : ∀ a ∈ xs, p a), Array.map Subtype.val (xs.attachWith p H) = xs
-- Mathlib.Algebra.BigOperators.Pi
prod_indicator_const : ∀ {ι : Type u_1} {κ : Type u_2} {R : Type u_5} [inst : CommSemiring R] (s : Finset ι) (f : ι → Set κ) (g : κ → R),
  ∏ i ∈ s, (f i).indicator g = (⋂ x ∈ s, f x).indicator (g ^ s.card)
-- Mathlib.Geometry.Manifold.Algebra.Structures
/-- A `C^n` (semi)ring is a (semi)ring `R` where addition and multiplication are `C^n`.
If `R` is a ring, then negation is automatically `C^n`, as it is multiplication with `-1`.  -/
ContMDiffRing : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {H : Type u_2} →
      [inst_1 : TopologicalSpace H] →
        {E : Type u_3} →
          [inst_2 : NormedAddCommGroup E] →
            [inst_3 : NormedSpace 𝕜 E] →
              ModelWithCorners 𝕜 E H →
                WithTop ℕ∞ → (R : Type u_4) → [Semiring R] → [inst : TopologicalSpace R] → [ChartedSpace H R] → Prop
-- Mathlib.Order.Filter.Pointwise
Filter.map_zero : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Zero α] [inst_1 : Zero β] [inst_2 : FunLike F α β]
  [ZeroHomClass F α β] (φ : F), Filter.map (⇑φ) 0 = 0
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.Minpoly.coe_toAdjoin_mk_X : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {x : S},
  ↑((AdjoinRoot.Minpoly.toAdjoin R x) ((AdjoinRoot.mk (minpoly R x)) Polynomial.X)) = x
-- Init.Data.Array.Lemmas
/-- Use this as `induction ass using array₃_induction` on a hypothesis of the form `ass : Array (Array (Array α))`.
The hypothesis `ass` will be replaced with a hypothesis `ass : List (List (List α))`,
and former appearances of `ass` in the goal will be replaced with
`((ass.map (fun xs => xs.map List.toArray)).map List.toArray).toArray`.
 -/
Array.array₃_induction : ∀ {α : Type u_1} (P : Array (Array (Array α)) → Prop),
  (∀ (xss : List (List (List α))),
      P (List.map List.toArray (List.map (fun xs => List.map List.toArray xs) xss)).toArray) →
    ∀ (xss : Array (Array (Array α))), P xss
-- Mathlib.Data.Real.ENatENNReal
ENat.toENNReal_ne_top : ∀ {n : ℕ∞}, ↑n ≠ ⊤ ↔ n ≠ ⊤
-- Mathlib.CategoryTheory.Limits.MorphismProperty
CategoryTheory.MorphismProperty.Under.instCreatesColimitsOfShapeTopUnderDiscretePEmptyForgetOfContainsIdentitiesOfRespectsIso : {T : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} T] →
    (P : CategoryTheory.MorphismProperty T) →
      (X : T) →
        [P.ContainsIdentities] →
          [P.RespectsIso] →
            CategoryTheory.CreatesColimitsOfShape (CategoryTheory.Discrete PEmpty.{1})
              (CategoryTheory.MorphismProperty.Under.forget P ⊤ X)
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.tr_move : ∀ (p : Turing.PartrecToTM2.Γ' → Bool) (k₁ k₂ : Turing.PartrecToTM2.K') (q : Turing.PartrecToTM2.Λ'),
  Turing.PartrecToTM2.tr (Turing.PartrecToTM2.Λ'.move p k₁ k₂ q) =
    Turing.PartrecToTM2.pop' k₁
      (Turing.TM2.Stmt.branch (fun s => s.elim true p) (Turing.TM2.Stmt.goto fun x => q)
        (Turing.PartrecToTM2.push' k₂ (Turing.TM2.Stmt.goto fun x => Turing.PartrecToTM2.Λ'.move p k₁ k₂ q)))
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.instHasZeroMorphisms : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      CategoryTheory.Limits.HasZeroMorphisms (CategoryTheory.Grp C)
-- Mathlib.Algebra.Algebra.Defs
/-- Creating an algebra from a morphism to the center of a semiring.
See note [reducible non-instances].

*Warning:* In general this should not be used if `S` already has a `SMul R S`
instance, since this creates another `SMul R S` instance from the supplied `RingHom` and
this will likely create a diamond.  -/
RingHom.toAlgebra' : {R : Type u_1} →
  {S : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : Semiring S] → (i : R →+* S) → (∀ (c : R) (x : S), i c * x = x * i c) → Algebra R S
-- Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
MvPolynomial.coeff_sumSMulX : ∀ {n : Type u_1} {R : Type u_2} [inst : CommRing R] (c : n →₀ R) (i : n),
  MvPolynomial.coeff (fun₀ | i => 1) (MvPolynomial.sumSMulX c) = c i
-- Mathlib.Algebra.GroupWithZero.Pointwise.Finset
Finset.div_zero_subset : ∀ {α : Type u_1} [inst : GroupWithZero α] [inst_1 : DecidableEq α] (s : Finset α), s / 0 ⊆ 0
-- Mathlib.Analysis.CStarAlgebra.Module.Constructions
WithCStarModule.instNormedAddCommGroupForall : {A : Type u_1} →
  [inst : NonUnitalCStarAlgebra A] →
    [inst_1 : PartialOrder A] →
      {ι : Type u_2} →
        {E : ι → Type u_3} →
          [Fintype ι] →
            [inst_3 : (i : ι) → NormedAddCommGroup (E i)] →
              [inst_4 : (i : ι) → Module ℂ (E i)] →
                [inst_5 : (i : ι) → SMul A (E i)] →
                  [(i : ι) → CStarModule A (E i)] →
                    [StarOrderedRing A] → NormedAddCommGroup (WithCStarModule A ((i : ι) → E i))
-- Init.Data.List.Sublist
List.instTransSubset : {α : Type u_1} → Trans Subset Subset Subset
-- Mathlib.Algebra.Regular.Opposite
/-- **Alias** of the reverse direction of `isAddRegular_op`. -/
IsAddRegular.op : ∀ {R : Type u_1} [inst : Add R] {a : R}, IsAddRegular a → IsAddRegular (AddOpposite.op a)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
HasFDerivAt.sin : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {f' : StrongDual ℝ E} {x : E},
  HasFDerivAt f f' x → HasFDerivAt (fun x => Real.sin (f x)) (Real.cos (f x) • f') x
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.id_whiskerLeft : ∀ {B : Type u} [self : CategoryTheory.Bicategory B] {a b : B} {f g : a ⟶ b} (η : f ⟶ g),
  CategoryTheory.Bicategory.whiskerLeft (CategoryTheory.CategoryStruct.id a) η =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor f).hom
      (CategoryTheory.CategoryStruct.comp η (CategoryTheory.Bicategory.leftUnitor g).inv)
-- Mathlib.Algebra.CharP.Invertible
not_ringChar_dvd_of_invertible : ∀ {R : Type u_1} [inst : Ring R] {t : ℕ} [Invertible ↑t] [Nontrivial R], ¬ringChar R ∣ t
-- Mathlib.Geometry.Manifold.Algebra.Monoid
mdifferentiable_add_right : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {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 : Add G] [inst_5 : TopologicalSpace G] [inst_6 : ChartedSpace H G] [ContMDiffAdd I 1 G] {a : G},
  MDiff fun x => x + a