mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
/-- The one-edge walk associated to a pair of adjacent vertices.  -/
SimpleGraph.Adj.toWalk : {V : Type u} → {G : SimpleGraph V} → {u v : V} → G.Adj u v → G.Walk u v
-- Mathlib.LinearAlgebra.Matrix.SemiringInverse
Matrix.nonsingular_one : ∀ {n : Type u_1} {R : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommSemiring R],
  Matrix.Nonsingular 1
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
ZeroAtInftyContinuousMap.instNonUnitalNormedRing : {α : Type u} →
  {β : Type v} →
    [inst : TopologicalSpace α] → [inst_1 : NonUnitalNormedRing β] → NonUnitalNormedRing (ZeroAtInftyContinuousMap α β)
-- Init.Data.List.Sublist
List.nil_infix : ∀ {α : Type u_1} {l : List α}, [] <:+: l
-- Mathlib.LinearAlgebra.BilinearForm.Properties
LinearMap.BilinForm.Nondegenerate.ne_zero : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Nontrivial M]
  {B : LinearMap.BilinForm R M}, B.Nondegenerate → B ≠ 0
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.ext : ∀ {X : AlgebraicGeometry.Scheme} {I J : X.IdealSheafData}, I.ideal = J.ideal → I = J
-- Mathlib.Topology.Category.Profinite.Basic
FintypeCat.toProfinite_obj : ∀ (A : FintypeCat), FintypeCat.toProfinite.obj A = Profinite.of A.obj
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
uniformity_translate_add : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : AddGroup α] [IsUniformAddGroup α] (a : α),
  Filter.map (fun x => (x.1 + a, x.2 + a)) (uniformity α) = uniformity α
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
SheafOfModules.GeneratingSections.ofEpi_I : ∀ {C : Type u'} [inst : CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : CategoryTheory.HasWeakSheafify J AddCommGrpCat]
  [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] {M N : SheafOfModules R} (σ : M.GeneratingSections) (p : M ⟶ N)
  [inst_3 : CategoryTheory.Epi p], (σ.ofEpi p).I = σ.I
-- Mathlib.LinearAlgebra.Matrix.Echelon.Pivot
Matrix.IsLeadingEntry.eq_1 : ∀ {m : Type u_1} {n : Type u_2} {R : Type v} [inst : Zero R] [inst_1 : LT n] (A : Matrix m n R) (i : m) (c : n),
  A.IsLeadingEntry i c = ((∀ j < c, A i j = 0) ∧ A i c ≠ 0)
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Tactic.ComputeAsymptotics.Monomial.mk.injEq : ∀ (coef : ℝ) (unit : Tactic.ComputeAsymptotics.UnitMonomial) (coef_1 : ℝ)
  (unit_1 : Tactic.ComputeAsymptotics.UnitMonomial),
  ({ coef := coef, unit := unit } = { coef := coef_1, unit := unit_1 }) = (coef = coef_1 ∧ unit = unit_1)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.BinaryFan.braiding_inv_snd_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {s : CategoryTheory.Limits.BinaryFan X Y}
  (P : CategoryTheory.Limits.IsLimit s) {t : CategoryTheory.Limits.BinaryFan Y X} (Q : CategoryTheory.Limits.IsLimit t)
  {Z : C} (h : (CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.right } ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryFan.braiding P Q).inv
      (CategoryTheory.CategoryStruct.comp s.snd h) =
    CategoryTheory.CategoryStruct.comp t.fst h
-- Mathlib.CategoryTheory.Triangulated.Generators
CategoryTheory.ObjectProperty.triangEnvelopeIter_add' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (P : CategoryTheory.ObjectProperty C) [CategoryTheory.IsTriangulated C] {n m m' : ℕ},
  autoParam (m = m' + 1) CategoryTheory.ObjectProperty.triangEnvelopeIter_add'._auto_1 →
    P.triangEnvelopeIter (n + m) = ((P.triangEnvelopeIter n).extensionProduct (P.triangEnvelopeIter m')).retractClosure
-- Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
/-- The homotopy relation on the category of bifibrant objects.  -/
HomotopicalAlgebra.BifibrantObject.homRel : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : HomotopicalAlgebra.ModelCategory C] → HomRel (HomotopicalAlgebra.BifibrantObject C)
-- Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
AlgebraicGeometry.UniversallyClosed.mk : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y},
  (AlgebraicGeometry.topologically @IsClosedMap).universally f → AlgebraicGeometry.UniversallyClosed f
-- Mathlib.Algebra.Ring.MinimalAxioms
/-- Define a `Ring` structure on a Type by proving a minimized set of axioms.
Note that this uses the default definitions for `npow`, `nsmul`, `zsmul` and `sub`
See note [reducible non-instances].  -/
Ring.ofMinimalAxioms : {R : Type u} →
  [inst : Add R] →
    [inst_1 : Mul R] →
      [inst_2 : Neg R] →
        [inst_3 : Zero R] →
          [inst_4 : One R] →
            (∀ (a b c : R), a + b + c = a + (b + c)) →
              (∀ (a : R), 0 + a = a) →
                (∀ (a : R), -a + a = 0) →
                  (∀ (a b c : R), a * b * c = a * (b * c)) →
                    (∀ (a : R), 1 * a = a) →
                      (∀ (a : R), a * 1 = a) →
                        (∀ (a b c : R), a * (b + c) = a * b + a * c) →
                          (∀ (a b c : R), (a + b) * c = a * c + b * c) → Ring R
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.bsup_eq_zero_iff : ∀ {o : Ordinal.{u_3}} {f : (a : Ordinal.{u_3}) → a < o → Ordinal.{max u_4 u_3}},
  o.bsup f = 0 ↔ ∀ (i : Ordinal.{u_3}) (hi : i < o), f i hi = 0
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.union_smul_inter_subset_union : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : SMul α β] {s₁ s₂ : Finset α} {t₁ t₂ : Finset β}
  [inst_2 : DecidableEq α], (s₁ ∪ s₂) • (t₁ ∩ t₂) ⊆ s₁ • t₁ ∪ s₂ • t₂
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenAddSubgroup.mem_toAddSubgroup : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] {U : OpenAddSubgroup G} {g : G}, g ∈ ↑U ↔ g ∈ U
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.coe_toAffineMap_mk : ∀ {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [inst : Ring R] [inst_1 : AddCommGroup V]
  [inst_2 : Module R V] [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] [inst_5 : AddCommGroup W]
  [inst_6 : Module R W] [inst_7 : TopologicalSpace Q] [inst_8 : AddTorsor W Q] (f : P →ᵃ[R] Q) (h : Continuous f.toFun),
  ↑{ toAffineMap := f, cont := h } = f
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.Basic
SSet.ι_chainComplexMap_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [inst_2 : CategoryTheory.Preadditive C] (X Y : SSet) (f : X ⟶ Y) (R : C) {n : ℕ}
  (x : X.obj (Opposite.op { len := n })),
  CategoryTheory.CategoryStruct.comp (X.ιChainComplex x) ((SSet.chainComplexMap f R).f n) =
    Y.ιChainComplex ((CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op { len := n }))) x)
-- Lean.Meta.Sym.Pattern
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.whenUndefDo : Lean.Meta.Sym.DefEqM✝ Lean.LBool → Lean.Meta.Sym.DefEqM✝ Bool → Lean.Meta.Sym.DefEqM✝ Bool
-- Mathlib.Condensed.Limits
instHasColimitsCondensedMod : ∀ (R : Type (u + 1)) [inst : Ring R], CategoryTheory.Limits.HasColimits (CondensedMod R)
-- Mathlib.Algebra.BigOperators.Pi
/-- An 'unapplied' analogue of `Finset.sum_apply`.  -/
Finset.sum_fn : ∀ {α : Type u_7} {M : α → Type u_8} {ι : Type u_9} [inst : (a : α) → AddCommMonoid (M a)] (s : Finset ι)
  (g : ι → (a : α) → M a), ∑ c ∈ s, g c = fun a => ∑ c ∈ s, g c a
-- Mathlib.Analysis.MellinTransform
/-- The Mellin transform of a function `f` (for a complex exponent `s`), defined as the integral of
`t ^ (s - 1) • f` over `Ioi 0`.  -/
mellin : {E : Type u_1} → [inst : NormedAddCommGroup E] → [NormedSpace ℂ E] → (ℝ → E) → ℂ → E
-- Init.Data.List.Lemmas
List.headD_eq_getD : ∀ {α : Type u_1} {l : List α} {fallback : α}, l.headD fallback = l.getD 0 fallback
-- Mathlib.Algebra.Group.Commute.Units
Units.ofPow.eq_1 : ∀ {M : Type u_1} [inst : Monoid M] (u : Mˣ) (x : M) {n : ℕ} (hn : n ≠ 0) (hu : x ^ n = ↑u),
  u.ofPow x hn hu = u.leftOfMul x (x ^ (n - 1)) ⋯ ⋯
-- Mathlib.CategoryTheory.Monad.Monadicity
/-- The unit cofork is a colimit provided `G` preserves it.  -/
CategoryTheory.Monad.MonadicityInternal.unitColimitOfPreservesCoequalizer : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₁, u₂} D] →
        {G : CategoryTheory.Functor D C} →
          {F : CategoryTheory.Functor C D} →
            {adj : F ⊣ G} →
              (A : adj.toMonad.Algebra) →
                [inst_2 : CategoryTheory.Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))] →
                  [CategoryTheory.Limits.PreservesColimit
                        (CategoryTheory.Limits.parallelPair (F.map A.a) (adj.counit.app (F.obj A.A))) G] →
                    CategoryTheory.Limits.IsColimit (CategoryTheory.Monad.MonadicityInternal.unitCofork A)
-- Mathlib.Analysis.Calculus.BumpFunction.Basic
ContDiffBump.mk.inj : ∀ {E : Type u_1} {c : E} {rIn rOut : ℝ} {rIn_pos : 0 < rIn} {rIn_lt_rOut : rIn < rOut} {rIn_1 rOut_1 : ℝ}
  {rIn_pos_1 : 0 < rIn_1} {rIn_lt_rOut_1 : rIn_1 < rOut_1},
  { rIn := rIn, rOut := rOut, rIn_pos := rIn_pos, rIn_lt_rOut := rIn_lt_rOut } =
      { rIn := rIn_1, rOut := rOut_1, rIn_pos := rIn_pos_1, rIn_lt_rOut := rIn_lt_rOut_1 } →
    rIn = rIn_1 ∧ rOut = rOut_1
-- Mathlib.Algebra.Order.Group.Nat
Nat.instCanonicallyOrderedAdd : CanonicallyOrderedAdd ℕ
-- Init.Data.ByteArray.Bootstrap
/-- Appends two byte arrays.

In compiled code, calls to `ByteArray.append` are replaced with the much more efficient
`ByteArray.fastAppend`.
 -/
ByteArray.append : ByteArray → ByteArray → ByteArray
-- Init.Data.Order.Ord
Std.LawfulBEqCmp.not_compare_eq_iff_beq_eq_false : ∀ {α : Type u} [inst : BEq α] {cmp : α → α → Ordering} [Std.LawfulBEqCmp cmp] {a b : α},
  ¬cmp a b = Ordering.eq ↔ (a == b) = false
-- Mathlib.Topology.Order.OrderClosed
/-- If `s` is a closed set and two functions `f` and `g` are continuous on `s`,
then the set `{x ∈ s | f x ≤ g x}` is a closed set.  -/
IsClosed.isClosed_le : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder α] [t : OrderClosedTopology α]
  [inst_2 : TopologicalSpace β] {f g : β → α} {s : Set β},
  IsClosed s → ContinuousOn f s → ContinuousOn g s → IsClosed {x | x ∈ s ∧ f x ≤ g x}
-- Mathlib.Algebra.Order.Nonneg.Ring
Nonneg.nontrivial : ∀ {α : Type u_1} [inst : Semiring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α], Nontrivial { x // 0 ≤ x }
-- Mathlib.Data.Nat.Bitwise
Nat.bitwise_swap : ∀ {f : Bool → Bool → Bool}, Nat.bitwise (Function.swap f) = Function.swap (Nat.bitwise f)
-- Mathlib.Data.Matrix.Mul
dotProduct_sub : ∀ {m : Type u_2} {α : Type v} [inst : Fintype m] [inst_1 : NonUnitalNonAssocRing α] (u v w : m → α),
  u ⬝ᵥ (v - w) = u ⬝ᵥ v - u ⬝ᵥ w
-- Mathlib.NumberTheory.Harmonic.ZetaAsymp
/-- The function `ζ s - 1 / (s - 1)` tends to `γ` as `s → 1`.  -/
tendsto_riemannZeta_sub_one_div : Filter.Tendsto (fun s => riemannZeta s - 1 / (s - 1)) (nhdsWithin 1 {1}ᶜ) (nhds ↑Real.eulerMascheroniConstant)
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
HasProd.congr_fun : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {f g : β → α} {a : α}
  {L : SummationFilter β}, HasProd f a L → (∀ (x : β), g x = f x) → HasProd g a L
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric
CFC.IsSelfAdjoint.norm_mul_mul_self_of_nonneg : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : NonUnitalNormedRing A] [inst_2 : StarRing A] [CStarRing A]
  [inst_4 : NormedSpace ℝ A] [inst_5 : SMulCommClass ℝ A A] [inst_6 : IsScalarTower ℝ A A] [inst_7 : StarOrderedRing A]
  [inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_9 : NonnegSpectrumClass ℝ A] {a : A} (b : A),
  autoParam (IsSelfAdjoint b) CFC.IsSelfAdjoint.norm_mul_mul_self_of_nonneg._auto_1 →
    autoParam (0 ≤ a) CFC.IsSelfAdjoint.norm_mul_mul_self_of_nonneg._auto_3 → ‖b * a * b‖ = ‖CFC.sqrt a * b‖ ^ 2
-- Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
NumberField.IsTotallyComplex.mult_eq : ∀ {K : Type u_2} [inst : Field K] [NumberField.IsTotallyComplex K] (w : NumberField.InfinitePlace K), w.mult = 2
-- Mathlib.Data.Nat.Pairing
Nat.pair.eq_1 : ∀ (a b : ℕ), Nat.pair a b = if a < b then b * b + a else a * a + a + b
-- Lean.Compiler.ExternAttr
_private.Lean.Compiler.ExternAttr.0.Lean.expandExternPatternAux.match_1.splitter : (pattern : String) →
  (it₁ : pattern.Pos) →
    (motive : (pattern.sliceFrom it₁).Pos × ℕ → Sort u_1) →
      (x : (pattern.sliceFrom it₁).Pos × ℕ) →
        ((it₂ : (pattern.sliceFrom it₁).Pos) → (j : ℕ) → motive (it₂, j)) → motive x
-- Mathlib.Data.Complex.Basic
Complex.instIntCast : IntCast ℂ
-- Mathlib.Algebra.GroupWithZero.Defs
/-- A type `M` is a commutative “monoid with zero” if it is a commutative monoid with zero
element, and `0` is left and right absorbing.  -/
CommMonoidWithZero : Type u_2 → Type u_2
-- Lean.Data.Json.Parser
Lean.Json.Parser.strCore : String → Std.Internal.Parsec.String.Parser String
-- Mathlib.Analysis.Normed.Group.Defs
/-- The distance function is induced by the norm.  -/
NormedCommGroup.dist_eq : ∀ {E : Type u_8} [self : NormedCommGroup E] (x y : E), dist x y = ‖x⁻¹ * y‖
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- The fourth cosimplicial identity  -/
CategoryTheory.CosimplicialObject.δ_comp_σ_of_gt_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) {n : ℕ}
  {i : Fin (n + 2)} {j : Fin (n + 1)},
  j.castSucc < i →
    ∀ {Z : C} (h : X.obj { len := n + 1 } ⟶ Z),
      CategoryTheory.CategoryStruct.comp (X.δ i.succ) (CategoryTheory.CategoryStruct.comp (X.σ j.castSucc) h) =
        CategoryTheory.CategoryStruct.comp (X.σ j) (CategoryTheory.CategoryStruct.comp (X.δ i) h)
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.coe_inj : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7} {f g : M [⋀^ι]→ₗ[R] N}, ⇑f = ⇑g ↔ f = g
-- Mathlib.Analysis.Calculus.FDeriv.Symmetric
/-- Definition recording that a function has a symmetric second derivative within a set at
a point. This is automatic in most cases of interest (open sets over real or complex vector fields,
or general case for analytic functions), but we can express theorems of calculus using this
as a general assumption, and then specialize to these situations.  -/
IsSymmSndFDerivWithinAt : (𝕜 : Type u_1) →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      {F : Type u_3} →
        [inst_1 : NormedAddCommGroup E] →
          [NormedSpace 𝕜 E] → [inst_3 : NormedAddCommGroup F] → [NormedSpace 𝕜 F] → (E → F) → Set E → E → Prop
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
Submonoid.unop_le_unop_iff : ∀ {M : Type u_2} [inst : MulOneClass M] {S₁ S₂ : Submonoid Mᵐᵒᵖ}, S₁.unop ≤ S₂.unop ↔ S₁ ≤ S₂
-- Lean.DocString.Types
/-- A string approximation of the part's title, for use in contexts where formatted text is invalid.
 -/
Lean.Doc.Part.titleString : {i : Type u} → {b : Type v} → {p : Type w} → Lean.Doc.Part i b p → String
-- Mathlib.Analysis.Normed.Group.FunctionSeries
/-- An infinite sum of functions with eventually summable sup norm is the uniform limit of its
partial sums. Version relative to a set, with general index set.  -/
tendstoUniformlyOn_tsum_of_cofinite_eventually : ∀ {β : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup F] [CompleteSpace F] {ι : Type u_4} {f : ι → β → F}
  {u : ι → ℝ},
  Summable u →
    ∀ {s : Set β},
      (∀ᶠ (n : ι) in Filter.cofinite, ∀ x ∈ s, ‖f n x‖ ≤ u n) →
        TendstoUniformlyOn (fun t x => ∑ n ∈ t, f n x) (fun x => ∑' (n : ι), f n x) Filter.atTop s
-- Mathlib.CategoryTheory.Sites.Localization
CategoryTheory.GrothendieckTopology.instIsLocalizationFunctorOppositeSheafPresheafToSheafW : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (J : CategoryTheory.GrothendieckTopology C)
  {A : Type u_2} [inst_1 : CategoryTheory.Category.{v_2, u_2} A] [inst_2 : CategoryTheory.HasWeakSheafify J A],
  (CategoryTheory.presheafToSheaf J A).IsLocalization J.W
-- Mathlib.Tactic.NormNum.Result
Mathlib.Meta.NormNum.Result'.isNegNat.inj : ∀ {inst lit proof inst_1 lit_1 proof_1 : Lean.Expr},
  Mathlib.Meta.NormNum.Result'.isNegNat inst lit proof = Mathlib.Meta.NormNum.Result'.isNegNat inst_1 lit_1 proof_1 →
    inst = inst_1 ∧ lit = lit_1 ∧ proof = proof_1
-- Mathlib.Analysis.InnerProductSpace.Calculus
differentiableAt_euclidean : ∀ {𝕜 : Type u_1} {ι : Type u_2} {H : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup H]
  [inst_2 : NormedSpace 𝕜 H] {f : H → EuclideanSpace 𝕜 ι} {y : H} [Finite ι],
  DifferentiableAt 𝕜 f y ↔ ∀ (i : ι), DifferentiableAt 𝕜 (fun x => (f x).ofLp i) y
-- Mathlib.Algebra.Regular.Pi
Pi.isSMulRegular_iff : ∀ {ι : Type u_1} {α : Type u_2} {R : ι → Type u_3} [inst : (i : ι) → SMul α (R i)] {r : α} [∀ (i : ι), Nonempty (R i)],
  IsSMulRegular ((i : ι) → R i) r ↔ ∀ (i : ι), IsSMulRegular (R i) r
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.ElabSimpArgResult.addLetToUnfold.injEq : ∀ (fvarId fvarId_1 : Lean.FVarId),
  (Lean.Elab.Tactic.ElabSimpArgResult.addLetToUnfold fvarId =
      Lean.Elab.Tactic.ElabSimpArgResult.addLetToUnfold fvarId_1) =
    (fvarId = fvarId_1)
-- Mathlib.Topology.Sion
/-- A minimax theorem in inf-sup form, for complete linear orders.  -/
Sion.minimax' : ∀ {E : Type u_1} {F : Type u_2} {β : Type u_3} [inst : CompleteLinearOrder β] [DenselyOrdered β] {X : Set E} {Y : Set F}
  {f : E → F → β} [inst_2 : TopologicalSpace E] [inst_3 : AddCommGroup E] [inst_4 : Module ℝ E]
  [IsTopologicalAddGroup E] [ContinuousSMul ℝ E],
  X.Nonempty →
    Convex ℝ X →
      IsCompact X →
        (∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X) →
          (∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y) →
            ∀ [inst_7 : TopologicalSpace F] [inst_8 : AddCommGroup F] [inst_9 : Module ℝ F] [IsTopologicalAddGroup F]
              [ContinuousSMul ℝ F],
              Convex ℝ Y →
                (∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y) →
                  (∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y) → ⨅ x ∈ X, ⨆ y ∈ Y, f x y = ⨆ y ∈ Y, ⨅ x ∈ X, f x y
-- Mathlib.Analysis.InnerProductSpace.ProdL2
Submodule.toLinearEquiv_orthogonalDecomposition : ∀ {𝕜 : Type u_1} {E : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : Submodule 𝕜 E) [inst_3 : K.HasOrthogonalProjection],
  K.orthogonalDecomposition.toLinearEquiv =
    (K.prodEquivOfIsCompl Kᗮ ⋯).symm ≪≫ₗ (WithLp.linearEquiv 2 𝕜 (↥K × ↥Kᗮ)).symm
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.cos_nonneg_iff_abs_toReal_le_pi_div_two : ∀ {θ : Real.Angle}, 0 ≤ θ.cos ↔ |θ.toReal| ≤ Real.pi / 2
-- Mathlib.Order.Types.Arithmetic
OrderType.type_lex_sum : ∀ (α : Type u) (β : Type v) [inst : LinearOrder α] [inst_1 : LinearOrder β],
  OrderType.type (α ⊕ₗ β) = OrderType.type α + OrderType.type β
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
/-- A uniform group is a group in which multiplication and inversion are uniformly continuous.

`IsUniformGroup G` is equivalent to the fact that `G` is a topological group, and the uniformity
coincides with **both** the associated left and right uniformities
(see `IsUniformGroup.isRightUniformGroup`, `IsUniformGroup.isLeftUniformGroup` and
`IsUniformGroup.of_left_right`).

Since there are topological groups where these two uniformities do **not** coincide,
not all topological groups admit a uniform group structure in this sense. This is however the
case for commutative groups, which are the main motivation for the existence of this
typeclass.  -/
IsUniformGroup : (α : Type u_3) → [UniformSpace α] → [Group α] → Prop
-- Mathlib.Algebra.Category.Grp.Yoneda
AddCommGrpCat.coyonedaType_map_app : ∀ {X Y : Type uᵒᵖ} (f : X ⟶ Y) (G : AddCommGrpCat),
  (AddCommGrpCat.coyonedaType.map f).app G =
    AddCommGrpCat.ofHom
      (AddMonoidHom.pi fun i => Pi.evalAddMonoidHom (fun a => ↑G) ((CategoryTheory.ConcreteCategory.hom f.unop) i))
-- Lean.Data.Lsp.Workspace
Lean.Lsp.instFromJsonDidChangeWatchedFilesRegistrationOptions : Lean.FromJson Lean.Lsp.DidChangeWatchedFilesRegistrationOptions
-- Mathlib.Analysis.Convex.Deriv
/-- If `f : ℝ → ℝ` is strictly convex on `S` and right-differentiable at `x ∈ S`, then the slope of
any secant line with left endpoint at `x` is strictly greater than the right derivative of `f` at
`x`.  -/
StrictConvexOn.lt_slope_of_hasDerivWithinAt_Ioi : ∀ {S : Set ℝ} {f : ℝ → ℝ} {x y f' : ℝ},
  StrictConvexOn ℝ S f → x ∈ S → y ∈ S → x < y → HasDerivWithinAt f f' (Set.Ioi x) x → f' < slope f x y
-- Mathlib.Order.Interval.Set.Basic
Set.Icc_subset_Ioc_left : ∀ {α : Type u_1} [inst : Preorder α] {a₁ a₂ b : α}, a₁ < a₂ → Set.Icc a₂ b ⊆ Set.Ioc a₁ b
-- Std.Time.Format.Basic
/-- Builds a `GenericFormat` from the input string. If parsing fails, it will panic
 -/
Std.Time.GenericFormat.spec! : {tz : Std.Time.Awareness} → String → optParam Std.Time.FormatConfig { } → Std.Time.GenericFormat tz
-- Mathlib.Tactic.Linarith.Parsing
/-- `findDefeq red m e` looks for a key in `m` that is defeq to `e` (up to transparency `red`),
and returns the value associated with this key if it exists.
Otherwise, it fails.
 -/
List.findDefeq : {v : Type} → Lean.Meta.TransparencyMode → List (Lean.Expr × v) → Lean.Expr → Lean.MetaM v
-- Mathlib.Analysis.Calculus.TangentCone.Basic
uniqueDiffWithinAt_inter' : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Semiring 𝕜] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [ContinuousAdd E] {s t : Set E} {x : E},
  t ∈ nhdsWithin x s → (UniqueDiffWithinAt 𝕜 (s ∩ t) x ↔ UniqueDiffWithinAt 𝕜 s x)
-- Lean.Meta.Tactic.Grind.Proof
/-- Given `acc : lhs₀ = lhs`, returns a proof of `lhs₀ = common`.  -/
_private.Lean.Meta.Tactic.Grind.Proof.0.Lean.Meta.Grind.mkProofTo : Lean.Expr → Lean.Expr → Option Lean.Expr → Bool → Lean.Meta.Grind.GoalM (Option Lean.Expr)
-- Mathlib.Analysis.SpecialFunctions.Integrals.Basic
/-- Simplification of the integral of `sin x ^ m * cos x ^ n`, case `n` is odd.  -/
integral_sin_pow_mul_cos_pow_odd : ∀ {a b : ℝ} (m n : ℕ),
  ∫ (x : ℝ) in a..b, Real.sin x ^ m * Real.cos x ^ (2 * n + 1) =
    ∫ (u : ℝ) in Real.sin a..Real.sin b, u ^ m * (1 - u ^ 2) ^ n
-- Mathlib.Analysis.Real.Cardinality
/-- `cantorFunction c` is injective if `0 < c < 1/2`.  -/
Cardinal.cantorFunction_injective : ∀ {c : ℝ}, 0 < c → c < 1 / 2 → Function.Injective (Cardinal.cantorFunction c)
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.ElabSimpArgResult.erase.inj : ∀ {toErase toErase_1 : Lean.Meta.Origin},
  Lean.Elab.Tactic.ElabSimpArgResult.erase toErase = Lean.Elab.Tactic.ElabSimpArgResult.erase toErase_1 →
    toErase = toErase_1
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
SimplexCategoryGenRel.standardσ.eq_def : ∀ (L : List ℕ) {m₁ m₂ : ℕ} (h : m₂ + L.length = m₁),
  SimplexCategoryGenRel.standardσ L h =
    match L, h with
    | [], h => CategoryTheory.eqToHom ⋯
    | a :: t, h =>
      CategoryTheory.CategoryStruct.comp (SimplexCategoryGenRel.standardσ t ⋯)
        (SimplexCategoryGenRel.σ (Fin.ofNat (m₂ + 1) a))
-- Mathlib.Analysis.Analytic.IsolatedZeros
/-- Preimages of codiscrete sets, filter version: if `f` is analytic on a neighbourhood of `U` and
not locally constant, then the push-forward of the filter of sets codiscrete within `U` is less
than or equal to the filter of sets codiscrete within `f '' U`.

Applications might want to use the theorem `Filter.codiscreteWithin_mono`.
 -/
AnalyticOnNhd.map_codiscreteWithin : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {U : Set 𝕜} {f : 𝕜 → E},
  AnalyticOnNhd 𝕜 f U →
    (∀ x ∈ U, ¬Filter.EventuallyConst f (nhds x)) →
      Filter.map f (Filter.codiscreteWithin U) ≤ Filter.codiscreteWithin (f '' U)