mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.TotalComplexShift
/-- The shift functors `shiftFunctor₁ C x` and `shiftFunctor₂ C y` on bicomplexes
with respect to both variables commute.  -/
HomologicalComplex₂.shiftFunctor₁₂CommIso : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      (x y : ℤ) →
        (HomologicalComplex₂.shiftFunctor₂ C y).comp (HomologicalComplex₂.shiftFunctor₁ C x) ≅
          (HomologicalComplex₂.shiftFunctor₁ C x).comp (HomologicalComplex₂.shiftFunctor₂ C y)
-- Init.Data.String.Substring
/-- Checks whether two substrings represent equal strings. Usually accessed via the `==` operator.

Two substrings do not need to have the same underlying string or the same start and end positions;
instead, they are equal if they contain the same sequence of characters.
 -/
Substring.Raw.beq : Substring.Raw → Substring.Raw → Bool
-- Mathlib.Tactic.NormNum.Result
/-- Constructs an `ofNat` application `a'` with the canonical instance, together with a proof that
the instance is equal to the result of `Nat.cast` on the given `AddMonoidWithOne` instance.

This function is performance-critical, as many higher level tactics have to construct numerals.
So rather than using typeclass search we hardcode the (relatively small) set of solutions
to the typeclass problem.
 -/
Mathlib.Meta.NormNum.mkOfNat : {u : Lean.Level} →
  (α : Q(Type u)) → (_sα : Q(AddMonoidWithOne «$α»)) → (lit : Q(ℕ)) → Lean.MetaM ((a' : Q(«$α»)) × Q(↑«$lit» = «$a'»))
-- Mathlib.Computability.TuringMachine.Computable
/-- type of states of the machine  -/
Turing.FinTM2.σ : Turing.FinTM2 → Type
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
/-- **Alias** of `SkewMonoidAlgebra.ofCoeff_one`. -/
SkewMonoidAlgebra.ofFinsupp_one : ∀ {k : Type u_1} {G : Type u_2} [inst : One G] [inst_1 : AddMonoidWithOne k], { coeff := fun₀ | 1 => 1 } = 1
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.Term.relabelEquiv_symm_apply : ∀ {L : FirstOrder.Language} {α : Type u'} {β : Type v'} (g : α ≃ β) (a : L.Term β),
  (FirstOrder.Language.Term.relabelEquiv g).symm a = FirstOrder.Language.Term.relabel (⇑g.symm) a
-- Mathlib.Algebra.Module.LocalizedModule.IsLocalization
instIsLocalizedModuleLinearMapOfIsLocalization : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) (A : Type u_2) [inst_1 : CommSemiring A]
  [inst_2 : Algebra R A] [IsLocalization S A], IsLocalizedModule S (Algebra.linearMap R A)
-- Mathlib.Probability.Kernel.IonescuTulcea.Traj
/-- This function takes as input a tuple `(x_₀, ..., x_ₐ)` and `ind` a function which
given `(y_₀, ...,y_ₙ)` outputs `x_{n+1} : X (n + 1)`, and it builds an element of `Π n, X n`
by starting with `(x_₀, ..., x_ₐ)` and then iterating `ind`.  -/
iterateInduction : {X : ℕ → Type u_1} →
  {a : ℕ} → ((i : ↥(Finset.Iic a)) → X ↑i) → ((n : ℕ) → ((i : ↥(Finset.Iic n)) → X ↑i) → X (n + 1)) → (n : ℕ) → X n
-- Mathlib.Data.Sym.Sym2
Sym2.toRel_prop : ∀ {α : Type u_1} (s : Set (Sym2 α)) (x y : α), Sym2.ToRel s x y ↔ s(x, y) ∈ s
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.sInf_toSubmodule : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] (S : Set (LieSubmodule R L M)),
  ↑(sInf S) = sInf {x | ∃ s ∈ S, ↑s = x}
-- Mathlib.FieldTheory.IsSepClosed
/-- Typeclass for separably closed fields.

To show `Polynomial.Splits p f` for an arbitrary ring homomorphism `f`,
see `IsSepClosed.splits_codomain` and `IsSepClosed.splits_domain`.
 -/
IsSepClosed : (k : Type u) → [Field k] → Prop
-- Mathlib.Order.BoundedOrder.Basic
Ne.lt_top' : ∀ {α : Type u} [inst : PartialOrder α] [inst_1 : OrderTop α] {a : α}, ⊤ ≠ a → a < ⊤
-- Mathlib.Algebra.Ring.Basic
IsDomain.to_noZeroDivisors : ∀ (α : Type u_3) [inst : Semiring α] [IsDomain α], NoZeroDivisors α
-- Mathlib.Order.Part
/-- `Part.bind` as a monotone function  -/
OrderHom.partBind : {α : Type u_1} → {β : Type u_2} → {γ : Type u_3} → [inst : Preorder α] → (α →o Part β) → (α →o β → Part γ) → α →o Part γ
-- Mathlib.RingTheory.Coalgebra.GroupLike
isGroupLikeElem_iff : ∀ (R : Type u_2) {A : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : Coalgebra R A] (a : A),
  IsGroupLikeElem R a ↔ CoalgebraStruct.counit a = 1 ∧ CoalgebraStruct.comul a = a ⊗ₜ[R] a
-- Mathlib.Order.Filter.AtTopBot.Field
Filter.map_div_atTop_eq : ∀ {α : Type u_1} [inst : Semifield α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] (k : α),
  0 < k → Filter.map (fun a => a / k) Filter.atTop = Filter.atTop
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.instSliceableImplRooSlice : {α : Type u} →
  {β : Type v} →
    [inst : Ord α] →
      Std.Roo.Sliceable (Std.DTreeMap.Internal.Impl α fun x => β) α (Std.DTreeMap.Internal.Const.RooSlice α β)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.getKey_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [inst : Std.TransCmp cmp]
  {k : α} {hk : k ∈ t₁} (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂), t₁.getKey k hk = t₂.getKey k ⋯
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.min_insert_le_self : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α},
  (cmp ((t.insert k).min ⋯) k).isLE = true
-- Lean.Meta.Tactic.Grind.Arith.CommRing.PP
_private.Lean.Meta.Tactic.Grind.Arith.CommRing.PP.0.Lean.Meta.Grind.Arith.CommRing.push : Array Lean.MessageData → Option Lean.MessageData → Array Lean.MessageData
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.sInter_singleton : ∀ {x : ZFSet.{u}}, {x}.sInter = x
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalSubsemiring.mem_centralizer_iff : ∀ {R : Type u_1} [inst : NonUnitalSemiring R] {s : Set R} {z : R},
  z ∈ NonUnitalSubsemiring.centralizer s ↔ ∀ g ∈ s, g * z = z * g
-- Mathlib.AlgebraicTopology.DoldKan.Projections
AlgebraicTopology.DoldKan.HigherFacesVanish.comp_P_eq_self_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {X : CategoryTheory.SimplicialObject C} {Y : C} {n q : ℕ} {φ : Y ⟶ X.obj (Opposite.op { len := n + 1 })},
  AlgebraicTopology.DoldKan.HigherFacesVanish q φ →
    ∀ {Z : C} (h : (AlgebraicTopology.AlternatingFaceMapComplex.obj X).X (n + 1) ⟶ Z),
      CategoryTheory.CategoryStruct.comp φ
          (CategoryTheory.CategoryStruct.comp ((AlgebraicTopology.DoldKan.P q).f (n + 1)) h) =
        CategoryTheory.CategoryStruct.comp φ h
-- Mathlib.Order.Disjoint
IsCompl.inf_left_le_of_le_sup_right : ∀ {α : Type u_1} [inst : DistribLattice α] [inst_1 : BoundedOrder α] {a b x y : α}, IsCompl x y → a ≤ b ⊔ y → a ⊓ x ≤ b
-- Mathlib.Order.Hom.CompleteLattice
sInfHom.instTop.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : InfSet α] {x : CompleteLattice β},
  sInfHom.instTop = { top := { toFun := fun x_1 => ⊤, map_sInf' := ⋯ } }
-- Mathlib.Geometry.Manifold.Sheaf.Smooth
/-- Canonical ring homomorphism from the stalk of `smoothSheafCommRing IM I M R` at `x` to `R`,
given by evaluating sections at `x`.  -/
smoothSheafCommRing.eval : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {EM : Type u_2} →
      [inst_1 : NormedAddCommGroup EM] →
        [inst_2 : NormedSpace 𝕜 EM] →
          {HM : Type u_3} →
            [inst_3 : TopologicalSpace HM] →
              (IM : ModelWithCorners 𝕜 EM HM) →
                {E : Type u_4} →
                  [inst_4 : NormedAddCommGroup E] →
                    [inst_5 : NormedSpace 𝕜 E] →
                      {H : Type u_5} →
                        [inst_6 : TopologicalSpace H] →
                          (I : ModelWithCorners 𝕜 E H) →
                            (M : Type u) →
                              [inst_7 : TopologicalSpace M] →
                                [inst_8 : ChartedSpace HM M] →
                                  (R : Type u) →
                                    [inst_9 : TopologicalSpace R] →
                                      [inst_10 : ChartedSpace H R] →
                                        [inst_11 : CommRing R] →
                                          [inst_12 : ContMDiffRing I (↑⊤) R] →
                                            (x : M) → ↑((smoothSheafCommRing IM I M R).presheaf.stalk x) →+* R
-- Init.Data.Int.DivMod.Lemmas
Int.fdiv_one : ∀ (a : ℤ), a.fdiv 1 = a
-- Mathlib.Data.NNRat.Defs
NNRat.instCharZero : CharZero ℚ≥0
-- Init.Data.Vector.Lex
Vector.le_trans : ∀ {α : Type u_1} {n : ℕ} [inst : LT α] [inst_1 : LE α] [Std.LawfulOrderLT α] [Std.IsLinearOrder α]
  {xs ys zs : Vector α n}, xs ≤ ys → ys ≤ zs → xs ≤ zs
-- Mathlib.Analysis.SpecificLimits.Normed
instHasSummableGeomSeries : ∀ {K : Type u_4} [inst : NormedDivisionRing K], HasSummableGeomSeries K
-- Aesop.Tree.Check
_private.Aesop.Tree.Check.0.Aesop.MVarClusterRef.checkMVars.checkAssignedMVars : Aesop.Rapp → Lean.MetaM Unit
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.getEntryLE.match_1.splitter : (motive : Ordering → Sort u_1) →
  (x : Ordering) →
    (x = Ordering.gt → motive Ordering.gt) →
      (x = Ordering.eq → motive Ordering.eq) → (x = Ordering.lt → motive Ordering.lt) → motive x
-- Mathlib.Order.Sublocale
/-- See `Sublocale.giRestrict` for the public-facing version.  -/
_private.Mathlib.Order.Sublocale.0.Sublocale.giAux : {X : Type u_1} → [inst : Order.Frame X] → (S : Sublocale X) → GaloisInsertion (Sublocale.restrictAux✝ S) Subtype.val
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.setToFun_add_left : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {T T' : Set α → E →L[ℝ] F} {C C' : ℝ} (hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
  (hT' : MeasureTheory.DominatedFinMeasAdditive μ T' C') (f : α → E),
  MeasureTheory.setToFun μ (T + T') ⋯ f = MeasureTheory.setToFun μ T hT f + MeasureTheory.setToFun μ T' hT' f
-- Mathlib.Data.Real.Basic
Real.cauchy_inv : ∀ (f : ℝ), f⁻¹.cauchy = f.cauchy⁻¹
-- Mathlib.SetTheory.ZFC.PSet
/-- A nonempty set is one that contains some element.  -/
PSet.Nonempty : PSet.{u_1} → Prop
-- Lean.Elab.BuiltinTerm
Lean.Elab.Term.elabClear : Lean.Elab.Term.TermElab
-- Mathlib.Combinatorics.Colex
/-- `s < {a}` in colex iff all elements of `s` are strictly less than `a`.  -/
Finset.Colex.toColex_lt_singleton : ∀ {α : Type u_1} [inst : PartialOrder α] {s : Finset α} {a : α}, toColex s < toColex {a} ↔ ∀ b ∈ s, b < a
-- Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Measurable.cexp : ∀ {α : Type u_1} {m : MeasurableSpace α} {f : α → ℂ}, Measurable f → Measurable fun x => Complex.exp (f x)
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.rightUnitor_inv_braiding_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X : C) {Z : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv
      (CategoryTheory.CategoryStruct.comp (β_ X (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv h
-- Mathlib.LinearAlgebra.Dual.Defs
Submodule.le_dualAnnihilator_dualCoannihilator : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (U : Submodule R M), U ≤ U.dualAnnihilator.dualCoannihilator
-- Mathlib.RingTheory.PicardGroup
Module.Invertible.instDual : ∀ (R : Type u) (M : Type v) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [Module.Invertible R M], Module.Invertible R (Module.Dual R M)
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.hom_ext_iff : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C D : HomologicalComplex V c} {f g : C ⟶ D},
  f = g ↔ ∀ (i : ι), f.f i = g.f i
-- Mathlib.Topology.MetricSpace.Lipschitz
/-- For functions to `ℝ`, it suffices to prove `f x ≤ f y + K * dist x y`; this version
doesn't assume `0≤K`.  -/
LipschitzOnWith.of_le_add_mul' : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α} {f : α → ℝ} (K : ℝ),
  (∀ x ∈ s, ∀ y ∈ s, f x ≤ f y + K * dist x y) → LipschitzOnWith K.toNNReal f s
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.ofLe_eq_comap_incl : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  {K K' : LieSubalgebra R L} (h : K ≤ K'), LieSubalgebra.ofLe h = LieSubalgebra.comap K'.incl K
-- Mathlib.FieldTheory.Finite.GaloisField
FiniteField.isSplittingField_of_nat_card_eq : ∀ (p : ℕ) [h_prime : Fact (Nat.Prime p)] (n : ℕ) {K : Type u_1} [inst : Field K] [inst_1 : Algebra (ZMod p) K],
  Nat.card K = p ^ n → Polynomial.IsSplittingField (ZMod p) K (Polynomial.X ^ p ^ n - Polynomial.X)
-- Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
/-- The middle object of the fork diagram given in Equation (3) of [MM92], as well as the fork diagram
of the Stacks entry.
 -/
CategoryTheory.Equalizer.FirstObj : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.Functor Cᵒᵖ (Type (max v u)) → {X : C} → CategoryTheory.Presieve X → Type (max v u)
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.colimit.desc_cocone : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasColimit F],
  CategoryTheory.Limits.colimit.desc F (CategoryTheory.Limits.colimit.cocone F) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.colimit F)
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
Matrix.charmatrix_zero : ∀ {R : Type u_1} [inst : CommRing R] {n : Type u_4} [inst_1 : DecidableEq n] [inst_2 : Fintype n],
  Matrix.charmatrix 0 = (Matrix.scalar n) Polynomial.X
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.snd_comp_inl : ∀ {M : Type u_1} {N : Type u_2} [inst : AddMonoid M] [inst_1 : AddMonoid N],
  AddMonoid.Coprod.snd.comp AddMonoid.Coprod.inl = 0
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.isSome_get?_iff_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {a : α},
  (m.get? a).isSome = true ↔ a ∈ m
-- Mathlib.Algebra.CharP.MixedCharZero
/-- `ℚ`-algebra implies equal characteristic.  -/
_private.Mathlib.Algebra.CharP.MixedCharZero.0.EqualCharZero.of_algebraRat : ∀ (R : Type u_1) [inst : CommRing R] [Algebra ℚ R] (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)
-- Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
GaussianFourier.integral_cexp_neg_mul_sq_norm_add_of_euclideanSpace : ∀ {b : ℂ} {ι : Type u_2} [inst : Fintype ι],
  0 < b.re →
    ∀ (c : ℂ) (w : EuclideanSpace ℝ ι),
      ∫ (v : EuclideanSpace ℝ ι), Complex.exp (-b * ↑‖v‖ ^ 2 + c * ↑(inner ℝ w v)) =
        (↑Real.pi / b) ^ (↑(Fintype.card ι) / 2) * Complex.exp (c ^ 2 * ↑‖w‖ ^ 2 / (4 * b))
-- Mathlib.Topology.Instances.AddCircle.Real
/-- Explicit formula for `toCircle j`. Note that this is "evil" because it uses `ZMod.val`. Where
possible, it is recommended to lift `j` to `ℤ` and use `toAddCircle_intCast` instead.
 -/
ZMod.toAddCircle_apply : ∀ {N : ℕ} [inst : NeZero N] (j : ZMod N), ZMod.toAddCircle j = ↑(↑j.val / ↑N)
-- Mathlib.Data.PNat.Basic
PNat.mul_coe : ∀ (m n : ℕ+), ↑(m * n) = ↑m * ↑n
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.maxKeyD_eq_getD_maxKey? : ∀ {α : Type u} {β : α → Type v} {l : Std.DTreeMap.Internal.Impl α β} {fallback : α},
  l.maxKeyD fallback = l.maxKey?.getD fallback
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_le_self_of_le_one : ∀ {x y : ℝ}, 0 ≤ x → x ≤ 1 → 1 ≤ y → x ^ y ≤ x
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey!_minKeyD : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  [inst_4 : Inhabited α] {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    l.isEmpty = false →
      ∀ {fallback : α},
        Std.Internal.List.getKey! (Std.Internal.List.minKeyD l fallback) l = Std.Internal.List.minKeyD l fallback
-- Mathlib.Algebra.Order.Ring.Abs
sq_le_sq : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {a b : α}, a ^ 2 ≤ b ^ 2 ↔ |a| ≤ |b|
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_roo_eq_singleton_iff : ∀ {k m n : ℕ}, (m<...n).toArray = #[k] ↔ n = m + 2 ∧ m + 1 = k
-- Mathlib.Algebra.Module.LinearMap.Defs
DistribMulActionHom.coe_toLinearMap : ∀ {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₂ : Type u_10} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid M₂]
  [inst_2 : Semiring R] [inst_3 : Module R M] [inst_4 : Semiring S] [inst_5 : Module S M₂] {σ : R →+* S}
  (f : M →ₑ+[↑σ] M₂), ⇑↑f = ⇑f
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.rpow_zero : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : TopologicalSpace A]
  [inst_4 : StarOrderedRing A] [inst_5 : Algebra ℝ A] [inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
  [inst_7 : NonnegSpectrumClass ℝ A] (a : A), autoParam (0 ≤ a) CFC.rpow_zero._auto_1 → a ^ 0 = 1
-- Mathlib.Analysis.Normed.Lp.lpHolder
lp.norm_holderL_le : ∀ {ι : Type u_1} {𝕜 : Type u_2} {E : ι → Type u_3} {F : ι → Type u_4} {G : ι → Type u_5} [inst : RCLike 𝕜]
  [inst_1 : (i : ι) → NormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_3 : (i : ι) → NormedAddCommGroup (F i)] [inst_4 : (i : ι) → NormedSpace 𝕜 (F i)]
  [inst_5 : (i : ι) → NormedAddCommGroup (G i)] [inst_6 : (i : ι) → NormedSpace 𝕜 (G i)] {p q : ENNReal} (r : ENNReal)
  [hpqr : p.HolderTriple q r] [inst_7 : Fact (1 ≤ p)] [inst_8 : Fact (1 ≤ q)] [inst_9 : Fact (1 ≤ r)]
  (B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i) {K : NNReal} (hBK : ∀ (i : ι), ‖B i‖ ≤ ↑K), ‖lp.holderL r B hBK‖ ≤ ↑K
-- Lean.Meta.Tactic.SplitIf
Lean.Meta.FindSplitImpl.FindM : Type → Type
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionItemKind.snippet : Lean.Lsp.CompletionItemKind
-- Mathlib.Order.Category.OmegaCompletePartialOrder
ωCPO.omegaCompletePartialOrderEqualizer : {α : Type u_1} →
  {β : Type u_2} →
    [inst : OmegaCompletePartialOrder α] →
      [inst_1 : OmegaCompletePartialOrder β] → (f g : α →𝒄 β) → OmegaCompletePartialOrder { a // f a = g a }
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.ringEq.injEq : ∀ (c : Lean.Meta.Grind.Arith.Linear.RingEqCnstr) (lhs : Lean.Meta.Grind.Arith.Linear.LinExpr)
  (c_1 : Lean.Meta.Grind.Arith.Linear.RingEqCnstr) (lhs_1 : Lean.Meta.Grind.Arith.Linear.LinExpr),
  (Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.ringEq c lhs =
      Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.ringEq c_1 lhs_1) =
    (c = c_1 ∧ lhs = lhs_1)
-- Mathlib.CategoryTheory.Functor.Currying
/-- The equivalence of types of bifunctors given by currying.  -/
CategoryTheory.Functor.curryingEquiv : {C : Type u₂} →
  [inst : CategoryTheory.Category.{v₂, u₂} C] →
    {D : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} D] →
        {E : Type u₄} →
          [inst_2 : CategoryTheory.Category.{v₄, u₄} E] →
            CategoryTheory.Functor C (CategoryTheory.Functor D E) ≃ CategoryTheory.Functor (C × D) E
-- Mathlib.Algebra.GroupWithZero.Associated
associated_unit_mul_left_iff : ∀ {N : Type u_2} [inst : CommMonoid N] {a b : N} {u : Nˣ}, Associated (↑u * a) b ↔ Associated a b
-- Std.Async.System
Std.Async.System.SystemUser.mk.inj : ∀ {username : String} {userId : Option Std.Async.System.UserId} {groupId : Option Std.Async.System.GroupId}
  {shell : Option String} {homeDir : Option System.FilePath} {username_1 : String}
  {userId_1 : Option Std.Async.System.UserId} {groupId_1 : Option Std.Async.System.GroupId} {shell_1 : Option String}
  {homeDir_1 : Option System.FilePath},
  { username := username, userId := userId, groupId := groupId, shell := shell, homeDir := homeDir } =
      { username := username_1, userId := userId_1, groupId := groupId_1, shell := shell_1, homeDir := homeDir_1 } →
    username = username_1 ∧ userId = userId_1 ∧ groupId = groupId_1 ∧ shell = shell_1 ∧ homeDir = homeDir_1
-- Mathlib.Data.Fintype.Sets
Finset.attach_eq_univ : ∀ {α : Type u_1} {s : Finset α}, s.attach = Finset.univ
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.ext_iff : ∀ {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₂]
  {f f' : ContinuousMultilinearMap R M₁ M₂}, f = f' ↔ ∀ (x : (i : ι) → M₁ i), f x = f' x
-- Mathlib.Geometry.Manifold.Diffeomorph
ContinuousLinearEquiv.contMDiffOn_transContinuousLinearEquiv_left : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {F : Type u_4}
  [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜 F] {H : Type u_5} [inst_7 : TopologicalSpace H]
  {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'}
  {M : Type u_9} [inst_9 : TopologicalSpace M] [inst_10 : ChartedSpace H M] {M' : Type u_10}
  [inst_11 : TopologicalSpace M'] [inst_12 : ChartedSpace H' M'] {n : WithTop ℕ∞} (e : E ≃L[𝕜] F) {f : M → M'}
  {s : Set M}, ContMDiffOn (I.transContinuousLinearEquiv e) I' n f s ↔ ContMDiffOn I I' n f s
-- Mathlib.Topology.UniformSpace.CompactConvergence
ContinuousMap.isUniformEmbedding_toUniformOnFunIsCompact : ∀ {α : Type u₁} {β : Type u₂} [inst : TopologicalSpace α] [inst_1 : UniformSpace β],
  IsUniformEmbedding ContinuousMap.toUniformOnFunIsCompact
-- Mathlib.Analysis.Calculus.ContDiff.Comp
/-- Application of a `ContinuousLinearMap` to a constant commutes with `iteratedFDeriv`.  -/
iteratedFDeriv_clm_apply_const_apply : ∀ {𝕜 : 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] {n : WithTop ℕ∞} {c : E → F →L[𝕜] G},
  ContDiff 𝕜 n c →
    ∀ {i : ℕ},
      ↑i ≤ n →
        ∀ {x : E} {u : F} {m : Fin i → E}, (iteratedFDeriv 𝕜 i (fun y => (c y) u) x) m = ((iteratedFDeriv 𝕜 i c x) m) u
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.homMk''.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {A B : CategoryTheory.Grp C} (f f_1 : A.X ⟶ B.X) (e_f : f = f_1)
  (one_f : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one f = CategoryTheory.MonObj.one)
  (mul_f :
    CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul f =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f f)
        CategoryTheory.MonObj.mul),
  CategoryTheory.Grp.homMk'' f one_f mul_f = CategoryTheory.Grp.homMk'' f_1 ⋯ ⋯
-- Init.Data.UInt.Bitwise
UInt16.or_comm : ∀ (a b : UInt16), a ||| b = b ||| a
-- Mathlib.Algebra.Order.SuccPred
strictMonoOn_of_sub_one_lt : ∀ {α : Type u_2} {β : Type u_3} [inst : PartialOrder α] [inst_1 : Preorder β] [inst_2 : Sub α] [inst_3 : One α]
  [inst_4 : PredSubOrder α] [IsPredArchimedean α] {s : Set α} {f : α → β},
  s.OrdConnected → (∀ (a : α), ¬IsMin a → a ∈ s → a - 1 ∈ s → f (a - 1) < f a) → StrictMonoOn f s
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get_eq_get : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp], t.WF → ∀ {a : α} {h' : a ∈ t}, Std.DTreeMap.Raw.Const.get t a h' = t.get a h'
-- Batteries.Data.Vector.Lemmas
Vector.toArray_scanl : ∀ {β : Type u_1} {α : Type u_2} {n : ℕ} {init : β} {f : β → α → β} {as : Vector α n},
  (Vector.scanl f init as).toArray = Array.scanl f init as.toArray
-- Lean.Data.PersistentArray
Lean.PersistentArray.isEmpty : {α : Type u} → Lean.PersistentArray α → Bool