mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.FilterBasis
ModuleFilterBasis.toAddGroupFilterBasis : {R : Type u_1} →
  {M : Type u_2} →
    [inst : Semiring R] →
      [inst_1 : TopologicalSpace R] →
        [inst_2 : AddCommGroup M] → [inst_3 : Module R M] → ModuleFilterBasis R M → AddGroupFilterBasis M
-- Mathlib.GroupTheory.Goursat
Subgroup.goursatFst.eq_1 : ∀ {G : Type u_1} {H : Type u_2} [inst : Group G] [inst_1 : Group H] (I : Subgroup (G × H)),
  I.goursatFst = Subgroup.map ((MonoidHom.fst G H).comp I.subtype) ((MonoidHom.snd G H).comp I.subtype).ker
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get?_ofList_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [Std.TransCmp cmp] [inst : BEq α] [Std.LawfulBEqCmp cmp]
  {l : List (α × β)} {k : α},
  (List.map Prod.fst l).contains k = false → Std.DTreeMap.Const.get? (Std.DTreeMap.Const.ofList l cmp) k = none
-- Init.Data.Iterators.Basic
/-- Termination measure to be used in well-founded recursive functions recursing over a finite iterator
(see also `Finite`).
 -/
Std.IterM.finitelyManySteps : {α : Type w} →
  {m : Type w → Type w'} →
    {β : Type w} →
      [inst : Std.Iterator α m β] →
        [Std.Iterators.Finite α m] → Std.IterM m β → Std.IterM.TerminationMeasures.Finite α m
-- Mathlib.MeasureTheory.Measure.Stieltjes
StieltjesFunction.id_apply : ∀ (a : ℝ), ↑StieltjesFunction.id a = id a
-- Mathlib.Order.Lattice
le_inf : ∀ {α : Type u} [inst : SemilatticeInf α] {c a b : α}, c ≤ a → c ≤ b → c ≤ a ⊓ b
-- Mathlib.Data.List.Sym
List.length_sym2 : ∀ {α : Type u_1} {xs : List α}, xs.sym2.length = (xs.length + 1).choose 2
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_eq_add : ∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] {s : Finset ι} {f : ι → M} (a b : ι),
  a ≠ b → (∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 0) → (a ∉ s → f a = 0) → (b ∉ s → f b = 0) → ∑ x ∈ s, f x = f a + f b
-- Lean.Elab.InfoTree.Types
Lean.Elab.TermInfo.mk.sizeOf_spec : ∀ (toElabInfo : Lean.Elab.ElabInfo) (lctx : Lean.LocalContext) (expectedType? : Option Lean.Expr) (expr : Lean.Expr)
  (isBinder isDisplayableTerm : Bool),
  sizeOf
      { toElabInfo := toElabInfo, lctx := lctx, expectedType? := expectedType?, expr := expr, isBinder := isBinder,
        isDisplayableTerm := isDisplayableTerm } =
    1 + sizeOf toElabInfo + sizeOf lctx + sizeOf expectedType? + sizeOf expr + sizeOf isBinder +
      sizeOf isDisplayableTerm
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.head_ofSeq : ∀ {α : Type u} (s : Stream'.Seq α), (↑s).head = Computation.pure s.head
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.le_total_ideal : ∀ {K : Type u} [inst : Field K] (A : ValuationSubring K), Std.Total fun x1 x2 => x1 ≤ x2
-- Mathlib.Algebra.MonoidAlgebra.ToDirectSum
AddMonoidAlgebra.toDirectSum_zero : ∀ {ι : Type u_1} {M : Type u_3} [inst : Semiring M], AddMonoidAlgebra.toDirectSum 0 = 0
-- Mathlib.Analysis.Complex.Trigonometric
Real.cosh_sq_sub_sinh_sq : ∀ (x : ℝ), Real.cosh x ^ 2 - Real.sinh x ^ 2 = 1
-- Std.Sync.Mutex
_private.Std.Sync.Mutex.0.Std.Mutex.ref : {α : Type} → Std.Mutex α → IO.Ref α
-- Aesop.RuleSet.Member
Aesop.LocalRuleSetMember.global.inj : ∀ {m m_1 : Aesop.GlobalRuleSetMember}, Aesop.LocalRuleSetMember.global m = Aesop.LocalRuleSetMember.global m_1 → m = m_1
-- Mathlib.Topology.Algebra.Module.Complement
/-- If two submodules are topological complements, then the linear equivalence
`Submodule.prodEquivOfIsCompl` is a homeomorphism, bundled as a continuous linear equivalence.  -/
Submodule.prodEquivOfIsTopCompl : {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) → [IsTopologicalAddGroup M] → Submodule.IsTopCompl p q → (↥p × ↥q) ≃L[R] M
-- Batteries.Data.List.Basic
/-- Tail-recursive version of `takeList`.  -/
List.takeListTR : {α : Type u_1} → List α → List ℕ → List (List α) × List α
-- Mathlib.Order.Bounds.Basic
subset_lowerBounds_upperBounds : ∀ {α : Type u_1} [inst : Preorder α] (s : Set α), s ⊆ lowerBounds (upperBounds s)
-- Lean.Elab.PreDefinition.Structural.Eqns
Lean.Elab.Structural.EqnInfo : Type
-- Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
AlgebraicIndependent.matroid_closure_of_subsingleton : ∀ {R : Type u_1} {A : Type w} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [inst_3 : FaithfulSMul R A] [inst_4 : Subsingleton A] (s : Set A), (AlgebraicIndependent.matroid R A).closure s = s
-- Lean.Elab.App
/-- Elaborate a `f`-application using `namedArgs` and `args` as the arguments.
- `expectedType?` the expected type if available. It is used to propagate typing information only. This method does **not** ensure the result has this type.
- `explicit = true` when notation `@` is used, and implicit arguments are assumed to be provided at `namedArgs` and `args`.
- `ellipsis = true` when notation `..` is used. That is, we add `_` for missing arguments.
- `resultIsOutParamSupport` is used to control whether special support is used when processing applications of functions that return
   output parameter of some local instance. Example:
   ```
   GetElem.getElem : {Cont : Type u_1} → {Idx : Type u_2} → {elem : Type u_3} → {dom : cont → idx → Prop} → [self : GetElem cont idx elem dom] → (xs : cont) → (i : idx) → dom xs i → elem
   ```
   The result type `elem` is the output parameter of the local instance `self`.
   When this parameter is set to `true`, we execute `synthesizeSyntheticMVarsUsingDefault`. For additional details, see comment at
   `ElabAppArgs.resultIsOutParam`.
 -/
Lean.Elab.Term.elabAppArgs : Lean.Expr →
  Array Lean.Elab.Term.NamedArg →
    Array Lean.Elab.Term.Arg → Option Lean.Expr → Bool → Bool → optParam Bool true → Lean.Elab.TermElabM Lean.Expr
-- Mathlib.Logic.Function.Basic
/-- `g` is a partial inverse to `f` (an injective but not necessarily
surjective function) if `g y = some x` implies `f x = y`, and `g y = none`
implies that `y` is not in the range of `f`.  -/
Function.IsPartialInv : {α : Type u_4} → {β : Sort u_5} → (α → β) → (β → Option α) → Prop
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.dvd_solve_elim_cert.match_1.eq_2 : ∀ (motive : Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → Sort u_1) (x x_1 : Int.Internal.Linear.Poly)
  (h_1 :
    (a₁ : ℤ) →
      (x₁ : Int.Internal.Linear.Var) →
        (p₁ : Int.Internal.Linear.Poly) →
          (a₂ : ℤ) →
            (x₂ : Int.Internal.Linear.Var) →
              (p₂ : Int.Internal.Linear.Poly) →
                motive (Int.Internal.Linear.Poly.add a₁ x₁ p₁) (Int.Internal.Linear.Poly.add a₂ x₂ p₂))
  (h_2 : (x x_2 : Int.Internal.Linear.Poly) → motive x x_2),
  (∀ (a₁ : ℤ) (x₁ : Int.Internal.Linear.Var) (p₁ : Int.Internal.Linear.Poly) (a₂ : ℤ) (x₂ : Int.Internal.Linear.Var)
      (p₂ : Int.Internal.Linear.Poly),
      x = Int.Internal.Linear.Poly.add a₁ x₁ p₁ → x_1 = Int.Internal.Linear.Poly.add a₂ x₂ p₂ → False) →
    (match x, x_1 with
      | Int.Internal.Linear.Poly.add a₁ x₁ p₁, Int.Internal.Linear.Poly.add a₂ x₂ p₂ => h_1 a₁ x₁ p₁ a₂ x₂ p₂
      | x, x_3 => h_2 x x_3) =
      h_2 x x_1
-- Lean.Data.Lsp.Basic
/-- An optional label of the workspace edit. This label is
presented in the user interface for example on an undo
stack to undo the workspace edit.  -/
Lean.Lsp.ApplyWorkspaceEditParams.label? : Lean.Lsp.ApplyWorkspaceEditParams → Option String
-- Mathlib.Order.CompleteSublattice
/-- The push forward of a complete sublattice under a complete lattice hom is a complete
sublattice.  -/
CompleteSublattice.map : {α : Type u_1} →
  {β : Type u_2} →
    [inst : CompleteLattice α] →
      [inst_1 : CompleteLattice β] → CompleteLatticeHom α β → CompleteSublattice α → CompleteSublattice β
-- Mathlib.Algebra.Order.Field.Basic
one_div_lt_one_div_of_neg_of_lt : ∀ {α : Type u_2} [inst : Field α] [inst_1 : PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b : α},
  b < 0 → a < b → 1 / b < 1 / a
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.num.eq_1 : ∀ {K : Type u} [inst : Field K] (x : RatFunc K), x.num = x.numDenom.1
-- Mathlib.Algebra.Algebra.Tower
AlgEquiv.extendScalarsOfSurjective_symm_apply : ∀ {R : Type u} {S : Type v} {A : Type w} {B : Type u₁} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : Semiring A] [inst_3 : Semiring B] [inst_4 : Algebra R S] [inst_5 : Algebra S A] [inst_6 : Algebra S B]
  [inst_7 : Algebra R A] [inst_8 : Algebra R B] [inst_9 : IsScalarTower R S A] [inst_10 : IsScalarTower R S B]
  (h : Function.Surjective ⇑(algebraMap R S)) (f : A ≃ₐ[S] B),
  (AlgEquiv.extendScalarsOfSurjective h).symm f = AlgEquiv.restrictScalars R f
-- Init.Data.Vector.Lemmas
Vector.reverse_flatMap : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {m : ℕ} {xs : Vector α n} {f : α → Vector β m},
  (xs.flatMap f).reverse = xs.reverse.flatMap (Vector.reverse ∘ f)
-- Mathlib.Tactic.CategoryTheory.Bicategory.Datatypes
Mathlib.Tactic.Bicategory.instMonadCoherehnceHomBicategoryM : Mathlib.Tactic.BicategoryLike.MonadCoherehnceHom Mathlib.Tactic.Bicategory.BicategoryM
-- Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
_private.Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities.0.MvPolynomial.NewtonIdentities.pairMap : (σ : Type u_1) → [DecidableEq σ] → Finset σ × σ → Finset σ × σ
-- Mathlib.GroupTheory.GroupAction.Defs
/-- The set of elements fixed under the whole action.  -/
MulAction.fixedPoints : (M : Type u_1) → (α : Type u_3) → [inst : Monoid M] → [MulAction M α] → Set α
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
/-- The homeomorphism induced from a two-sided continuous isomorphism additive groups.  -/
ContinuousAddEquiv.toHomeomorph : {G : Type u} →
  [inst : TopologicalSpace G] →
    {H : Type v} → [inst_1 : TopologicalSpace H] → [inst_2 : Add G] → [inst_3 : Add H] → G ≃ₜ+ H → G ≃ₜ H
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PushoutProduct
SSet.instFibrationAppPreOfMonoOfKanComplex : ∀ {A B : SSet} (i : A ⟶ B) [CategoryTheory.Mono i] (X : SSet) [X.KanComplex],
  HomotopicalAlgebra.Fibration ((CategoryTheory.MonoidalClosed.pre i).app X)
-- Mathlib.Algebra.Category.Semigrp.Basic
MagmaCat.forgetReflectsIsos : (CategoryTheory.forget MagmaCat).ReflectsIsomorphisms
-- Mathlib.RingTheory.Spectrum.Prime.Defs
PrimeSpectrum.instCoeIdeal : {R : Type u_1} → [inst : CommSemiring R] → Coe (PrimeSpectrum R) (Ideal R)
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
NumberField.ComplexEmbedding.disjoint_unmixedEmbeddingsOver_mixedEmbeddingsOver : ∀ {K : Type u_3} (L : Type u_4) [inst : Field K] [inst_1 : Field L] (ψ : K →+* ℂ) [inst_2 : Algebra K L],
  Disjoint (NumberField.ComplexEmbedding.unmixedEmbeddingsOver L ψ)
    (NumberField.ComplexEmbedding.mixedEmbeddingsOver L ψ)
-- Lean.Data.Lsp.Capabilities
/-- Whether the client supports incremental `textDocument/publishDiagnostics` updates.
If `none` or `false`, the server will never set `PublishDiagnosticsParams.isIncremental?`
and always report full diagnostic updates that replace the previous one.
 -/
Lean.Lsp.LeanClientCapabilities.incrementalDiagnosticSupport? : Lean.Lsp.LeanClientCapabilities → Option Bool
-- Mathlib.LinearAlgebra.Ray
/-- Two scalar multiples of a common vector whose coefficients have nonnegative product
lie on a common ray.  -/
sameRay_smul_smul_of_mul_nonneg : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : LinearOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] {v : M} {c₁ c₂ : R}, 0 ≤ c₁ * c₂ → SameRay R (c₁ • v) (c₂ • v)
-- Mathlib.Probability.Distributions.SetBernoulli
ProbabilityTheory.setBernoulli_singleton : ∀ {ι : Type u_1} {s u : Set ι} (p : ↑unitInterval) [Countable ι],
  s ⊆ u →
    u.Finite →
      (ProbabilityTheory.setBernoulli u p) {s} =
        ↑(unitInterval.toNNReal p) ^ s.ncard * ↑(unitInterval.toNNReal (unitInterval.symm p)) ^ (u \ s).ncard
-- Mathlib.Topology.MetricSpace.UniformConvergence
UniformFun.isometry_ofFun_continuousMap : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace β] [inst_1 : TopologicalSpace α] [inst_2 : CompactSpace α],
  Isometry (⇑UniformFun.ofFun ∘ DFunLike.coe)
-- Init.Data.Int.DivMod.Lemmas
Int.add_mul_bmod_self_right : ∀ (a b : ℤ) (c : ℕ), (a + b * ↑c).bmod c = a.bmod c
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.cond.match_1.eq_1 : ∀ (motive : Bool → Sort u_1) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  (match true with
    | true => h_1 ()
    | false => h_2 ()) =
    h_1 ()
-- Mathlib.AlgebraicGeometry.Sites.Pretopology
/-- The pretopology on the category of schemes defined by jointly surjective families.  -/
AlgebraicGeometry.Scheme.jointlySurjectivePretopology : CategoryTheory.Pretopology AlgebraicGeometry.Scheme
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
SSet.Edge.CompStruct.mk_simplex : ∀ {X : SSet} {x₀ x₁ x₂ : X.obj (Opposite.op { len := 0 })} {e₀₁ : SSet.Edge x₀ x₁} {e₁₂ : SSet.Edge x₁ x₂}
  {e₀₂ : SSet.Edge x₀ x₂} (simplex : X.obj (Opposite.op { len := 2 }))
  (d₂ :
    autoParam ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X 2)) simplex = e₀₁.edge)
      _auto_99✝)
  (d₀ :
    autoParam ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X 0)) simplex = e₁₂.edge)
      _auto_101✝)
  (d₁ :
    autoParam ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X 1)) simplex = e₀₂.edge)
      _auto_103✝),
  (SSet.Edge.CompStruct.mk simplex ⋯ ⋯ ⋯).simplex = simplex
-- Mathlib.Data.Finset.Powerset
Finset.powersetCard_nonempty : ∀ {α : Type u_1} {n : ℕ} {s : Finset α}, (Finset.powersetCard n s).Nonempty ↔ n ≤ s.card
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.single_mem_pi : ∀ {η : Type u_7} {f : η → Type u_8} [inst : (i : η) → AddGroup (f i)] [inst_1 : DecidableEq η] {I : Set η}
  {H : (i : η) → AddSubgroup (f i)} (i : η) (x : f i), Pi.single i x ∈ AddSubgroup.pi I H ↔ i ∈ I → x ∈ H i
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
/-- The integral as a continuous linear map from Schwartz space to the codomain.  -/
SchwartzMap.integralCLM : (𝕜 : Type u_2) →
  {D : Type u_4} →
    {V : Type u_9} →
      [inst : RCLike 𝕜] →
        [inst_1 : NormedAddCommGroup D] →
          [inst_2 : NormedSpace ℝ D] →
            [inst_3 : NormedAddCommGroup V] →
              [inst_4 : NormedSpace ℝ V] →
                [inst_5 : NormedSpace 𝕜 V] →
                  [inst_6 : MeasurableSpace D] →
                    (μ : MeasureTheory.Measure D) →
                      [hμ : μ.HasTemperateGrowth] →
                        [BorelSpace D] → [SecondCountableTopology D] → SchwartzMap D V →L[𝕜] V
-- Mathlib.GroupTheory.Congruence.Defs
/-- The complete lattice of congruence relations on a given type with a multiplication.  -/
Con.instCompleteLattice : {M : Type u_1} → [inst : Mul M] → CompleteLattice (Con M)
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.instInhabitedSimpTheorem.default : Lean.Meta.SimpTheorem
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Coseparator
CategoryTheory.IsGrothendieckAbelian.instHasCoseparator : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [CategoryTheory.IsGrothendieckAbelian.{w, v, u} C], CategoryTheory.HasCoseparator C
-- Mathlib.GroupTheory.PushoutI
Monoid.PushoutI.NormalWord.mulAction : {ι : Type u_1} →
  {G : ι → Type u_2} →
    {H : Type u_3} →
      [inst : (i : ι) → Group (G i)] →
        [inst_1 : Group H] →
          {φ : (i : ι) → H →* G i} →
            {d : Monoid.PushoutI.NormalWord.Transversal φ} →
              [DecidableEq ι] →
                [(i : ι) → DecidableEq (G i)] → MulAction (Monoid.PushoutI φ) (Monoid.PushoutI.NormalWord d)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence
groupHomology.cyclesMk.congr_simp : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u, u, u} k G} (m n n_1 : ℕ) (e_n : n = n_1)
  (h : (ComplexShape.down ℕ).next m = n) (f f_1 : (Fin m → G) →₀ ↑A) (e_f : f = f_1)
  (hf : (CategoryTheory.ConcreteCategory.hom ((groupHomology.inhomogeneousChains A).d m n)) f = 0),
  groupHomology.cyclesMk m n h f hf = groupHomology.cyclesMk m n_1 ⋯ f_1 ⋯
-- Mathlib.RingTheory.WittVector.MulCoeff
WittVector.peval_polyOfInterest : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] {k : Type u_1} [inst : CommRing k] (n : ℕ) (x y : WittVector p k),
  WittVector.peval (WittVector.polyOfInterest p n) ![fun i => x.coeff i, fun i => y.coeff i] =
    (x * y).coeff (n + 1) + ↑p ^ (n + 1) * x.coeff (n + 1) * y.coeff (n + 1) -
        y.coeff (n + 1) * ∑ i ∈ Finset.range (n + 1 + 1), ↑p ^ i * x.coeff i ^ p ^ (n + 1 - i) -
      x.coeff (n + 1) * ∑ i ∈ Finset.range (n + 1 + 1), ↑p ^ i * y.coeff i ^ p ^ (n + 1 - i)
-- Mathlib.Algebra.Ring.Subring.MulOpposite
Subring.op_unop : ∀ {R : Type u_2} [inst : NonAssocRing R] (S : Subring Rᵐᵒᵖ), S.unop.op = S
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem!_diff_of_not_mem_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited β], m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₁ → (m₁ \ m₂)[k]! = default
-- Mathlib.Order.CompleteLattice.Chain
ChainClosure.brecOn : ∀ {α : Type u_1} {r : α → α → Prop} {motive : (a : Set α) → ChainClosure r a → Prop} {a : Set α} (t : ChainClosure r a),
  (∀ (a : Set α) (t : ChainClosure r a), ChainClosure.below t → motive a t) → motive a t
-- Mathlib.RingTheory.Ideal.Height
/-- Use `RingEquiv.height_comap` instead, which does not assume `IsPrime`.  -/
_private.Mathlib.RingTheory.Ideal.Height.0.RingEquiv.height_comap_of_isPrime : ∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] (e : R ≃+* S) (p : Ideal S) [p.IsPrime],
  (Ideal.comap e p).height = p.height
-- Mathlib.Topology.UnitInterval
Set.Icc.continuous_convexComb : ∀ {a b : ℝ} (x y : ↑(Set.Icc a b)), Continuous (Set.Icc.convexComb x y)
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Functor.mapGrpNatTrans.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  {F F' : CategoryTheory.Functor C D} [inst_4 : F.Monoidal] [inst_5 : F'.Monoidal] (f : F ⟶ F'),
  CategoryTheory.Functor.mapGrpNatTrans f =
    { app := fun X => CategoryTheory.Grp.homMk' ((CategoryTheory.Functor.mapMonNatTrans f).app X.toMon),
      naturality := ⋯ }
-- Init.Data.Slice.Array.Lemmas
Array.toList_mkSlice_ric : ∀ {α : Type u_1} {xs : Array α} {hi : ℕ},
  Std.Slice.toList (Std.Ric.Sliceable.mkSlice xs *...=hi) = List.take (hi + 1) xs.toList
-- Mathlib.LinearAlgebra.Matrix.SemiringInverse
Matrix.detp_one_one : ∀ {n : Type u_1} {R : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommSemiring R],
  Matrix.detp 1 1 = 1
-- Lean.Elab.Binders
Lean.Elab.Term.LetIdDeclView.type : Lean.Elab.Term.LetIdDeclView → Lean.Syntax
-- Mathlib.Analysis.Distribution.TestFunction
TestFunction.instIsUniformAddGroup : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4}
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {n : ℕ∞}, IsUniformAddGroup (TestFunction Ω F n)
-- Mathlib.Analysis.Calculus.ContDiff.Comp
ContDiffAt.comp_contDiffWithinAt : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {s : Set E} {f : E → F} {g : F → G} {n : WithTop ℕ∞}
  (x : E), ContDiffAt 𝕜 n g (f x) → ContDiffWithinAt 𝕜 n f s x → ContDiffWithinAt 𝕜 n (g ∘ f) s x
-- Mathlib.Algebra.Category.AlgCat.Basic
AlgCat.intEquivalence_counitIso : AlgCat.intEquivalence.counitIso =
  CategoryTheory.Iso.refl
    ({ obj := fun A => AlgCat.of ℤ ↑A, map := fun {X Y} f => AlgCat.ofHom (RingCat.Hom.hom f).toIntAlgHom,
          map_id := AlgCat.intEquivalence._proof_1, map_comp := @AlgCat.intEquivalence._proof_2 }.comp
      (CategoryTheory.forget₂ (AlgCat ℤ) RingCat))
-- Aesop.Nanos
Aesop.Nanos.instAdd : Add Aesop.Nanos
-- Aesop.Forward.State
/-- Erase a hypothesis from the rule state.  -/
Aesop.RuleState.eraseHyp : Lean.FVarId → Aesop.PremiseIndex → Aesop.RuleState → Aesop.RuleState
-- Mathlib.LinearAlgebra.Projectivization.Subspace
/-- The infimum of two subspaces exists.  -/
Projectivization.Subspace.instInf : {K : Type u_1} →
  {V : Type u_2} →
    [inst : DivisionRing K] → [inst_1 : AddCommGroup V] → [inst_2 : Module K V] → Min (Projectivization.Subspace K V)
-- Mathlib.NumberTheory.LSeries.AbstractFuncEq
/-- As `x → 0`, `f x` decays faster than any power of `x`.  -/
IsStrongFEPair.hf_zero : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {P : WeakFEPair E},
  IsStrongFEPair P → ∀ (r : ℝ), P.f =O[nhdsWithin 0 (Set.Ioi 0)] fun x => x ^ r
-- Init.Data.Vector.Lemmas
Vector.finIdxOf?_toList : ∀ {α : Type u_1} {n : ℕ} [inst : BEq α] {a : α} {xs : Vector α n},
  List.finIdxOf? a xs.toList = Option.map (Fin.cast ⋯) (xs.finIdxOf? a)
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
PreQuasiregular.mk.inj : ∀ {R : Type u_1} {val val_1 : R}, { val := val } = { val := val_1 } → val = val_1
-- Init.Data.SInt.Lemmas
Int16.sub_add_cancel : ∀ (a b : Int16), a - b + b = a
-- Mathlib.CategoryTheory.EpiMono
/-- A category where every morphism has a `Trunc` retraction is computably a groupoid.  -/
CategoryTheory.Groupoid.ofTruncSplitMono : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (∀ {X Y : C} (f : X ⟶ Y), Trunc (CategoryTheory.IsSplitMono f)) → CategoryTheory.Groupoid C
-- Mathlib.Order.Partition.Basic
Partition.coe_copy : ∀ {α : Type u_1} {s t : α} [inst : CompleteLattice α] (P : Partition s) (hst : s = t), ↑(P.copy hst) = ↑P
-- Mathlib.Order.Filter.Bases.Basic
Filter.hasBasis_principal : ∀ {α : Type u_1} (t : Set α), (Filter.principal t).HasBasis (fun x => True) fun x => t
-- Init.Data.Int.Basic
Int.negSucc.sizeOf_spec : ∀ (a : ℕ), sizeOf (Int.negSucc a) = 1 + sizeOf a
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.toWithBotSyn_withBotDegree_mul_le : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] (f g : MvPolynomial σ R),
  m.toWithBotSyn (m.withBotDegree (f * g)) ≤ m.toWithBotSyn (m.withBotDegree f) + m.toWithBotSyn (m.withBotDegree g)
-- Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
AlgebraicGeometry.UniversallyOpen.mk : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y},
  (AlgebraicGeometry.topologically @IsOpenMap).universally f → AlgebraicGeometry.UniversallyOpen f
-- Init.Data.Array.Bootstrap
Array.foldrM.eq_1 : ∀ {α : Type u} {β : Type v} {m : Type v → Type w} [inst : Monad m] (f : α → β → m β) (init : β) (as : Array α)
  (start stop : ℕ),
  Array.foldrM f init as start stop =
    if h : start ≤ as.size then if stop < start then Array.foldrM.fold f as stop start h init else pure init
    else if stop < as.size then Array.foldrM.fold f as stop as.size ⋯ init else pure init
-- Lean.DocString.Types
/-- Rewrites using a proof that two inline element types are equal.  -/
Lean.Doc.Inline.cast : {i i' : Type u_1} → i = i' → Lean.Doc.Inline i → Lean.Doc.Inline i'
-- Mathlib.Logic.IsEmpty.Basic
leftTotal_empty : ∀ {α : Type u_4} {β : Type u_5} (R : α → β → Prop) [IsEmpty α], Relator.LeftTotal R
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.inf_toSubalgebra : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E]
  (S T : IntermediateField F E), (S ⊓ T).toSubalgebra = S.toSubalgebra ⊓ T.toSubalgebra
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.RightExtension.postcompose₂ObjMkIso_hom_left_app : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  [inst_3 : CategoryTheory.Category.{v_5, u_5} D'] {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H}
  (G : CategoryTheory.Functor H D') {F' : CategoryTheory.Functor D H} (α : L.comp F' ⟶ F) (X : D),
  (CategoryTheory.Functor.RightExtension.postcompose₂ObjMkIso G α).hom.left.app X =
    CategoryTheory.CategoryStruct.id (G.obj (F'.obj X))