mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.Factorizations.CM5a
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.midπ_π_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {K L : CochainComplex C ℤ} (f : K ⟶ L) [inst_2 : CategoryTheory.EnoughInjectives C] [inst_3 : CategoryTheory.Mono f]
  (n₀ : ℤ) [inst_4 : K.IsStrictlyGE (n₀ + 1)] [inst_5 : L.IsStrictlyGE (n₀ + 1)] (q : ℕ) (i : ℤ),
  CategoryTheory.CategoryStruct.comp ((CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.midπ✝ f n₀ q).f i)
      (((CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.functor✝ f n₀).obj (Opposite.op q)).obj.π.f i) =
    (CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.π✝ f n₀).f i
-- Lean.Elab.Arg
/-- Add a new named argument to `namedArgs`, and throw an error if it already contains a named argument
with the same name.  -/
Lean.Elab.Term.addNamedArg : Array Lean.Elab.Term.NamedArg → Lean.Elab.Term.NamedArg → Lean.MetaM (Array Lean.Elab.Term.NamedArg)
-- Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Finset.sum_eq_add_sum_sdiff_singleton : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : DecidableEq ι] {s : Finset ι} (i : ι) (f : ι → M),
  (i ∉ s → f i = 0) → ∑ x ∈ s, f x = f i + ∑ x ∈ s \ {i}, f x
-- Mathlib.Tactic.Algebra.Basic
/-- Remove some nonstandard spellings of `algebraMap` such as `Nat.cast`  -/
Mathlib.Tactic.Algebra.preprocess : Lean.Expr → Lean.MetaM Lean.Meta.Simp.Result
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get_union_of_not_mem_left : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [inst : Std.TransCmp cmp] {k : α} (not_mem : k ∉ t₁)
  {h' : k ∈ t₁ ∪ t₂}, (t₁ ∪ t₂).get k h' = t₂.get k ⋯
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.instInhabited : {R : Type u_1} →
  {Γ₀ : Type u_2} →
    [inst : LinearOrderedCommGroupWithZero Γ₀] → [inst_1 : Ring R] → (v : Valuation R Γ₀) → Inhabited (WithVal v)
-- Mathlib.GroupTheory.GroupAction.Hom
AddActionHom.inverse'_inverse' : ∀ {M : Type u_2} {N : Type u_3} {φ : M → N} {X : Type u_5} [inst : VAdd M X] {Y : Type u_6} [inst_1 : VAdd N Y]
  {φ' : N → M} {f : X →ₑ[φ] Y} {g : Y → X} {k₁ : Function.LeftInverse φ' φ} {k₂ : Function.RightInverse φ' φ}
  {h₁ : Function.LeftInverse g ⇑f} {h₂ : Function.RightInverse g ⇑f}, (f.inverse' g k₂ h₁ h₂).inverse' (⇑f) k₁ h₂ h₁ = f
-- Batteries.Data.List.Lemmas
List.idxOfNth_eq_idxOfNth_iff_of_right_lt_count : ∀ {α : Type u_1} {m : ℕ} {x : α} {n : ℕ} [inst : BEq α] {xs : List α},
  m < List.count x xs → (List.idxOfNth x xs n = List.idxOfNth x xs m ↔ n = m)
-- Mathlib.CategoryTheory.ObjectProperty.Orthogonal
CategoryTheory.ObjectProperty.instContainsZeroLeftOrthogonalOfHasZeroObject : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (P : CategoryTheory.ObjectProperty C) [CategoryTheory.Limits.HasZeroObject C], P.leftOrthogonal.ContainsZero
-- Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Matrix.IsAdjMatrix.toGraph.eq_1 : ∀ {α : Type u_1} {V : Type u_2} {A : Matrix V V α} [inst : MulZeroOneClass α] [inst_1 : Nontrivial α]
  (h : A.IsAdjMatrix), h.toGraph = { Adj := fun i j => A i j = 1, symm := ⋯, loopless := ⋯ }
-- Mathlib.RingTheory.Flat.EquationalCriterion
/-- The proposition that the relation $\sum_i f_i x_i = 0$ in $M$ is trivial.
That is, there exist a finite index type $\kappa$ = `Fin k`, elements
$(y_j)_{j \in \kappa}$ of $M$, and elements $(a_{ij})_{i \in \iota, j \in \kappa}$ of $R$
such that for all $i$,
$$x_i = \sum_j a_{ij} y_j$$
and for all $j$,
$$\sum_i f_i a_{ij} = 0.$$
By `Module.sum_smul_eq_zero_of_isTrivialRelation`, this condition implies $\sum_i f_i x_i = 0$.  -/
Module.IsTrivialRelation : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] → [Module R M] → {ι : Type u_3} → [Fintype ι] → (ι → R) → (ι → M) → Prop
-- Mathlib.LinearAlgebra.FiniteDimensional.Defs
/-- A subspace of a finite-dimensional space is also finite-dimensional.

This is a shortcut instance to simplify inference in the presence of `[FiniteDimensional K V]`.
 -/
FiniteDimensional.finiteDimensional_submodule : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [FiniteDimensional K V] (S : Submodule K V), FiniteDimensional K ↥S
-- Mathlib.NumberTheory.MulChar.Basic
/-- A multiplicative character on a commutative monoid with finitely many units
has finite (= positive) order.  -/
MulChar.orderOf_pos : ∀ {M : Type u_1} [inst : CommMonoid M] {R : Type u_2} [inst_1 : CommMonoidWithZero R] [Finite Mˣ] (χ : MulChar M R),
  0 < orderOf χ
-- Mathlib.Algebra.Order.Field.Basic
inv_pow_anti : ∀ {α : Type u_2} [inst : Semifield α] [inst_1 : PartialOrder α] [PosMulReflectLT α] {a : α} [IsStrictOrderedRing α],
  1 ≤ a → Antitone fun n => (a ^ n)⁻¹
-- Mathlib.Geometry.Manifold.GroupLieAlgebra
/-- The tangent space at the identity of a Lie group is a Lie algebra, for the bracket
given by the Lie bracket of invariant vector fields.  -/
instLieAlgebraGroupLieAlgebra : {𝕜 : 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 : TopologicalSpace G] →
                    [inst_5 : ChartedSpace H G] →
                      [inst_6 : Group G] →
                        [inst_7 : LieGroup I (minSmoothness 𝕜 3) G] →
                          [inst_8 : CompleteSpace E] → LieAlgebra 𝕜 (GroupLieAlgebra I G)
-- Mathlib.LinearAlgebra.Lagrange
Lagrange.eval_interpolate_at_node : ∀ {F : Type u_1} [inst : Field F] {ι : Type u_2} [inst_1 : DecidableEq ι] {s : Finset ι} {i : ι} {v : ι → F}
  (r : ι → F), Set.InjOn v ↑s → i ∈ s → Polynomial.eval (v i) ((Lagrange.interpolate s v) r) = r i
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Functions
Lean.Meta.Grind.Arith.CommRing.getNegFn : {m : Type → Type} →
  [MonadLiftT Lean.MetaM m] →
    [Lean.MonadError m] →
      [Monad m] → [Lean.Meta.Sym.Arith.MonadCanon m] → [Lean.Meta.Grind.Arith.CommRing.MonadRing m] → m Lean.Expr
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- Any representation `Ω` of `Subobject.presheaf C` gives a subobject classifier with truth values
object `Ω`.  -/
CategoryTheory.SubobjectRepresentableBy.classifier : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasPullbacks C] →
      {Ω : C} →
        CategoryTheory.SubobjectRepresentableBy Ω →
          [CategoryTheory.Limits.HasTerminal C] → CategoryTheory.Subobject.Classifier C
-- Mathlib.Combinatorics.SimpleGraph.Paths
/-- **Alias** of `SimpleGraph.Walk.isCycle_mapLe`. -/
SimpleGraph.Walk.mapLe_isCycle : ∀ {V : Type u} {G G' : SimpleGraph V} (h : G ≤ G') {u : V} {p : G.Walk u u},
  (SimpleGraph.Walk.mapLe h p).IsCycle ↔ p.IsCycle
-- Mathlib.Algebra.Regular.Defs
/-- An add-regular element `c` is right-regular  -/
IsAddRegular.right : ∀ {R : Type u_2} [inst : Add R] {c : R}, IsAddRegular c → IsAddRightRegular c
-- Mathlib.RingTheory.PowerSeries.Binomial
PowerSeries.binomialSeries_zero : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : BinomialRing R] [inst_2 : Ring A] [inst_3 : Algebra R A],
  PowerSeries.binomialSeries A 0 = 1
-- Mathlib.Data.Nat.GCD.BigOperators
Nat.coprime_multiset_prod_left_iff : ∀ {m : Multiset ℕ} {k : ℕ}, m.prod.Coprime k ↔ ∀ n ∈ m, n.Coprime k
-- Mathlib.CategoryTheory.Bicategory.Functor.Cat.ObjectProperty
CategoryTheory.Pseudofunctor.ObjectProperty.mapComp_inv_app : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat}
  (P : F.ObjectProperty) [inst_1 : P.IsClosedUnderMapObj] {X Y Z : B} (f : X ⟶ Y) (g : Y ⟶ Z) (M : P.Obj X),
  (P.mapComp f g).inv.app M = CategoryTheory.ObjectProperty.homMk ((F.mapComp f g).inv.toNatTrans.app M.obj)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey?_diff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, (t₁ \ t₂).getKey? k = if k ∈ t₂ then none else t₁.getKey? k
-- Mathlib.CategoryTheory.Bicategory.Span.Basic
CategoryTheory.Span.comp_r : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {Wₗ Wᵣ : CategoryTheory.MorphismProperty C}
  [inst_1 : Wₗ.HasPullbacksAgainst Wᵣ] [inst_2 : Wₗ.IsStableUnderBaseChangeAgainst Wᵣ]
  [inst_3 : Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [inst_4 : Wₗ.IsStableUnderComposition]
  [inst_5 : Wᵣ.IsStableUnderComposition] {c c' c'' : C} (S₁ : CategoryTheory.Span Wₗ Wᵣ c c')
  (S₂ : CategoryTheory.Span Wₗ Wᵣ c' c''),
  (S₁.comp S₂).r = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd S₁.r S₂.l) S₂.r
-- Mathlib.Topology.Order.OrderClosed
isOpen_lt_prod' : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderClosedTopology α], IsOpen {p | p.2 < p.1}
-- Mathlib.RingTheory.IntegralClosure.Algebra.Basic
/-- **Alias** of `RingHom.Finite.to_isIntegral`.

---

[Stacks Tag 00GK](https://stacks.math.columbia.edu/tag/00GK) -/
RingHom.IsIntegral.of_finite : ∀ {R : Type u_1} {S : Type u_4} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S}, f.Finite → f.IsIntegral
-- Mathlib.Algebra.Group.Hom.Defs
/-- If `f` is an additive monoid homomorphism then `f (a + b) = f a + f b`.  -/
AddMonoidHom.map_add : ∀ {M : Type u_4} {N : Type u_5} [inst : AddZero M] [inst_1 : AddZero N] (f : M →+ N) (a b : M), f (a + b) = f a + f b
-- Mathlib.Order.Bounds.Basic
/-- In a codirected order, the union of two sets is bounded below if and only if both sets are.  -/
bddBelow_union : ∀ {α : Type u_1} [inst : Preorder α] [IsCodirectedOrder α] {s t : Set α}, BddBelow (s ∪ t) ↔ BddBelow s ∧ BddBelow t
-- Mathlib.RingTheory.Ideal.GoingUp
/-- **Alias** of `Ideal.IsIntegral.eq_bot_of_comap_eq_bot`. -/
Ideal.IntegralClosure.eq_bot_of_comap_eq_bot : ∀ (R : Type u_1) [inst : CommRing R] {A : Type u_3} [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [Algebra.IsIntegral R A] [IsDomain A] [Nontrivial R] {I : Ideal A}, Ideal.comap (algebraMap R A) I = ⊥ → I = ⊥
-- Mathlib.Combinatorics.SimpleGraph.Diam
SimpleGraph.ediam_le_two_mul_eccent : ∀ {α : Type u_1} {G : SimpleGraph α} (u : α), G.ediam ≤ 2 * G.eccent u
-- Mathlib.Algebra.Category.Grp.Basic
AddCommGrpCat.id_apply : ∀ (X : AddCommGrpCat) (x : ↑X), (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) x = x
-- Mathlib.Algebra.AffineMonoid.Embedding
_private.Mathlib.Algebra.AffineMonoid.Embedding.0.AffineAddMonoid.embedding.eq_1 : ∀ (M : Type u_1) [inst : AddCancelCommMonoid M] [inst_1 : AddMonoid.FG M] [inst_2 : IsAddTorsionFree M],
  AffineAddMonoid.embedding M =
    (FreeAbelianGroup.equivFinsupp (Fin (Module.finrank ℤ (AddLocalization ⊤)))).symm.toAddMonoidHom.comp
      ((↑(Module.finBasis ℤ (AddLocalization ⊤)).repr).toAddMonoidHom.comp
        (AddLocalization.addMonoidOf ⊤).toAddMonoidHom)
-- Mathlib.GroupTheory.Submonoid.Inverses
Submonoid.leftInvEquiv_apply : ∀ {M : Type u_1} [inst : CommMonoid M] (S : Submonoid M) (hS : S ≤ IsUnit.submonoid M) (a : ↥S.leftInv),
  (S.leftInvEquiv hS) a = (↑S.fromCommLeftInv).toFun a
-- Mathlib.Probability.Distributions.Gaussian.Multivariate
ProbabilityTheory.integral_id_multivariateGaussian : ∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] {μ : EuclideanSpace ℝ ι} {S : Matrix ι ι ℝ},
  ∫ (x : EuclideanSpace ℝ ι), x ∂ProbabilityTheory.multivariateGaussian μ S = μ
-- Mathlib.NumberTheory.NumberField.Discriminant.Defs
NumberField.discr_eq_discr : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] {ι : Type u_2} [inst_2 : Fintype ι] [inst_3 : DecidableEq ι]
  (b : Module.Basis ι ℤ (NumberField.RingOfIntegers K)), Algebra.discr ℤ ⇑b = NumberField.discr K
-- Mathlib.Topology.Category.Profinite.Nobeling.Basic
Profinite.NobelingProof.ProjRestrict_coe : ∀ {I : Type u} (C : Set (I → Bool)) (J : I → Prop) [inst : (i : I) → Decidable (J i)] (a : ↑C) (a_1 : I),
  ↑(Profinite.NobelingProof.ProjRestrict C J a) a_1 = Profinite.NobelingProof.Proj J (↑a) a_1
-- Mathlib.CategoryTheory.Triangulated.TStructure.Basic
CategoryTheory.Triangulated.TStructure.ge_iff_isGE : ∀ {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]
  (t : CategoryTheory.Triangulated.TStructure C) (X : C) (n : ℤ), t.ge n X ↔ t.IsGE X n
-- Mathlib.Algebra.Polynomial.Monic
Polynomial.Monic.sub_of_right : ∀ {R : Type u} [inst : Ring R] {p q : Polynomial R}, q.leadingCoeff = -1 → p.degree < q.degree → (p - q).Monic
-- Mathlib.CategoryTheory.Bicategory.Yoneda
CategoryTheory.Bicategory.leftUnitorNatIsoCat_hom_toNatTrans_app : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] (a b : B) (X : a ⟶ b),
  (CategoryTheory.Bicategory.leftUnitorNatIsoCat a b).hom.toNatTrans.app X =
    (CategoryTheory.Bicategory.leftUnitor X).hom
-- Mathlib.Algebra.Star.Subsemiring
StarSubsemiring.subsemiringClass : ∀ {R : Type v} [inst : NonAssocSemiring R] [inst_1 : StarRing R], SubsemiringClass (StarSubsemiring R) R
-- Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber
Matrix.square_of_invertible : ∀ {n : Type u_1} {m : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Fintype m]
  [inst_3 : DecidableEq m] {R : Type u_3} [inst_4 : Semiring R] [InvariantBasisNumber R] (M : Matrix n m R)
  (N : Matrix m n R), M * N = 1 → N * M = 1 → Fintype.card n = Fintype.card m
-- Mathlib.CategoryTheory.Limits.Shapes.SplitEqualizer
/-- Composition of `ι` with `f` and with `g` agree  -/
CategoryTheory.IsSplitEqualizer.condition_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {W : C} {ι : W ⟶ X}
  (self : CategoryTheory.IsSplitEqualizer f g ι) {Z : C} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp ι (CategoryTheory.CategoryStruct.comp f h) =
    CategoryTheory.CategoryStruct.comp ι (CategoryTheory.CategoryStruct.comp g h)
-- Mathlib.Algebra.Group.Prod
MonoidHom.prod_apply : ∀ {M : Type u_3} {N : Type u_4} {P : Type u_5} [inst : MulOneClass M] [inst_1 : MulOneClass N] [inst_2 : MulOneClass P]
  (f : M →* N) (g : M →* P) (x : M), (f.prod g) x = (f x, g x)
-- Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
iteratedDeriv_const_mul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {𝔸 : Type u_5} [inst_1 : NormedRing 𝔸]
  [inst_2 : NormedAlgebra 𝕜 𝔸] {n : ℕ} {f : 𝕜 → 𝔸} (c : 𝔸),
  ContDiffAt 𝕜 (↑n) f x → iteratedDeriv n (fun x => c * f x) x = c * iteratedDeriv n f x
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- The morphism to the zero object is a cokernel of an epimorphism  -/
CategoryTheory.Limits.cokernel.isColimitCoconeZeroCocone : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} →
        (f : X ⟶ Y) →
          [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
            [CategoryTheory.Epi f] →
              CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.cokernel.zeroCokernelCofork f)
-- Batteries.Util.ProofWanted
/-- The surfaced binder's type (Π over the dependency's own binders, ending in its accessor).  -/
_private.Batteries.Util.ProofWanted.0.WantedDep.binderType : WantedDep✝ → Lean.TSyntax `term
-- Mathlib.Algebra.Group.Pointwise.Set.Finite
Set.Finite.div : ∀ {α : Type u_2} [inst : Div α] {s t : Set α}, s.Finite → t.Finite → (s / t).Finite
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.uniformContinuous : ∀ {V₁ : Type u_2} {V₂ : Type u_3} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂]
  (f : NormedAddGroupHom V₁ V₂), UniformContinuous ⇑f
-- Lean.Meta.Tactic.Intro
/-- Calculate the number of new hypotheses that would be created by `intros`,
i.e. the number of binders which can be introduced without unfolding definitions.
 -/
Lean.Meta.getIntrosSize : Lean.Expr → ℕ
-- Init.Data.Array.Nat
Array.prod_eq_zero_iff_exists_zero_nat : ∀ {xs : Array ℕ}, xs.prod = 0 ↔ ∃ x ∈ xs, x = 0
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.valuation_eq_iff : ∀ {K : Type u} [inst : Field K] (A : ValuationSubring K) (x y : K), A.valuation x = A.valuation y ↔ ∃ a, ↑↑a * y = x
-- Mathlib.Probability.CDF
/-- The cdf tends to 1 at +∞.  -/
ProbabilityTheory.tendsto_cdf_atTop : ∀ (μ : MeasureTheory.Measure ℝ), Filter.Tendsto (↑(ProbabilityTheory.cdf μ)) Filter.atTop (nhds 1)
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.Context.mk : Lean.Elab.Tactic.Context →
  Lean.Meta.Grind.Context →
    Lean.Meta.Sym.Context → Lean.Meta.Grind.Methods → Lean.Meta.Grind.Params → Bool → Lean.Elab.Tactic.Grind.Context
-- Init.System.IO
IO.Process.SpawnArgs.mk.injEq : ∀ (toStdioConfig : IO.Process.StdioConfig) (cmd : String) (args : Array String) (cwd : Option System.FilePath)
  (env : Array (String × Option String)) (inheritEnv setsid : Bool) (toStdioConfig_1 : IO.Process.StdioConfig)
  (cmd_1 : String) (args_1 : Array String) (cwd_1 : Option System.FilePath) (env_1 : Array (String × Option String))
  (inheritEnv_1 setsid_1 : Bool),
  ({ toStdioConfig := toStdioConfig, cmd := cmd, args := args, cwd := cwd, env := env, inheritEnv := inheritEnv,
        setsid := setsid } =
      { toStdioConfig := toStdioConfig_1, cmd := cmd_1, args := args_1, cwd := cwd_1, env := env_1,
        inheritEnv := inheritEnv_1, setsid := setsid_1 }) =
    (toStdioConfig = toStdioConfig_1 ∧
      cmd = cmd_1 ∧ args = args_1 ∧ cwd = cwd_1 ∧ env = env_1 ∧ inheritEnv = inheritEnv_1 ∧ setsid = setsid_1)
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.zeroLocus_span : ∀ (X : AlgebraicGeometry.Scheme) {U : X.Opens} (s : Set ↑(X.presheaf.obj (Opposite.op U))),
  X.zeroLocus ↑(Ideal.span s) = X.zeroLocus s
-- Mathlib.Data.Finsupp.Defs
Finsupp.instFunLike : {α : Type u_1} → {M : Type u_4} → [inst : Zero M] → FunLike (α →₀ M) α M
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.coprod.map_desc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S T U V W : C}
  [inst_1 : CategoryTheory.Limits.HasBinaryCoproduct U W] [inst_2 : CategoryTheory.Limits.HasBinaryCoproduct T V]
  (f : U ⟶ S) (g : W ⟶ S) (h : T ⟶ U) (k : V ⟶ W),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map h k) (CategoryTheory.Limits.coprod.desc f g) =
    CategoryTheory.Limits.coprod.desc (CategoryTheory.CategoryStruct.comp h f) (CategoryTheory.CategoryStruct.comp k g)
-- Lean.Meta.Basic
_private.Lean.Meta.Basic.0.Lean.Meta.withLocalContextImp : {α : Type} → Lean.LocalContext → Lean.LocalInstances → Lean.MetaM α → Lean.MetaM α
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.addCommMonoid : {R : Type u} →
  {ι : Type v} →
    {M₁ : ι → Type w₁} →
      {M₂ : Type w₂} →
        [inst : Semiring R] →
          [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : (i : ι) → Module R (M₁ i)] →
                [inst_4 : Module R M₂] →
                  [inst_5 : (i : ι) → TopologicalSpace (M₁ i)] →
                    [inst_6 : TopologicalSpace M₂] →
                      [ContinuousAdd M₂] → AddCommMonoid (ContinuousMultilinearMap R M₁ M₂)
-- Mathlib.Topology.VectorBundle.Basic
VectorBundleCore.baseSet_at : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField R] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace R F] [inst_3 : TopologicalSpace B] {ι : Type u_5} (Z : VectorBundleCore R B F ι) (i : ι),
  Z.baseSet i = (Z.localTriv i).baseSet
-- Lean.Elab.Do.Basic
_private.Lean.Elab.Do.Basic.0.Lean.Elab.Do.ContInfoRefPointed : NonemptyType
-- Batteries.Util.Cache
Batteries.Tactic.DeclCache.mk'.inj : ∀ {α : Type} {cache : Batteries.Tactic.Cache α}
  {addDecl addLibraryDecl : Lean.Name → Lean.ConstantInfo → α → Lean.MetaM α} {cache_1 : Batteries.Tactic.Cache α}
  {addDecl_1 addLibraryDecl_1 : Lean.Name → Lean.ConstantInfo → α → Lean.MetaM α},
  { cache := cache, addDecl := addDecl, addLibraryDecl := addLibraryDecl } =
      { cache := cache_1, addDecl := addDecl_1, addLibraryDecl := addLibraryDecl_1 } →
    cache = cache_1 ∧ addDecl = addDecl_1 ∧ addLibraryDecl = addLibraryDecl_1
-- Mathlib.Analysis.Normed.Group.Basic
norm_add_eq_norm_right : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] {x : E} (y : E), ‖x‖ = 0 → ‖x + y‖ = ‖y‖
-- Mathlib.Analysis.Normed.Group.Subgroup
Subgroup.seminormedCommGroup : {E : Type u_1} → [inst : SeminormedCommGroup E] → {s : Subgroup E} → SeminormedCommGroup ↥s
-- Mathlib.Data.ENNReal.Basic
ENNReal.ofReal_toReal_eq_iff : ∀ {a : ENNReal}, ENNReal.ofReal a.toReal = a ↔ a ≠ ⊤
-- Mathlib.Order.CompleteBooleanAlgebra
CompleteAtomicBooleanAlgebra.mk : {α : Type u} →
  [toCompleteBooleanAlgebra : CompleteBooleanAlgebra α] →
    (∀ {ι : Type u} {κ : ι → Type u} (f : (a : ι) → κ a → α), ⨅ a, ⨆ b, f a b = ⨆ g, ⨅ a, f a (g a)) →
      CompleteAtomicBooleanAlgebra α
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
Convexity.StdSimplex.weights_restrict : ∀ {X : Type u_2} {K : Type u_8} [inst : Semifield K] [inst_1 : LinearOrder K] [inst_2 : IsStrictOrderedRing K]
  (w : Convexity.StdSimplex K X) (s : Set X) (hs : ∃ x ∈ s, w.weights x ≠ 0) [inst_3 : DecidablePred fun x => x ∈ s],
  (w.restrict s hs).weights =
    ((Finsupp.filter (fun x => x ∈ s) w.weights).sum fun _x k => k)⁻¹ • Finsupp.filter (fun x => x ∈ s) w.weights
-- Mathlib.Computability.Partrec
Partrec.comp : ∀ {α : Type u_1} {β : Type u_2} {σ : Type u_3} [inst : Primcodable α] [inst_1 : Primcodable β] [inst_2 : Primcodable σ]
  {f : β →. σ} {g : α → β}, Partrec f → Computable g → Partrec fun a => f (g a)
-- Mathlib.Order.WithBot
WithBot.lt_iff_exists : ∀ {α : Type u_1} [inst : LT α] {x y : WithBot α}, x < y ↔ ∃ b, y = ↑b ∧ ∀ (a : α), x = ↑a → a < b