mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.isUnit_comp : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] {P : Type u_3} [inst_3 : CommSemiring P] [IsLocalization M S] (j : S →+* P) (y : ↥M),
  IsUnit ((j.comp (algebraMap R S)) ↑y)
-- Lean.Meta.Tactic.Grind.AC.Seq
/-- `s₁ == s₂`  -/
Lean.Grind.AC.SubseqResult.exact : Lean.Grind.AC.SubseqResult
-- Lean.Util.Diff
Lean.Diff.instInhabitedAction : Inhabited Lean.Diff.Action
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey_filter : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : α → β → Bool} {k : α} {h' : k ∈ Std.HashMap.filter f m},
  (Std.HashMap.filter f m).getKey k h' = m.getKey k ⋯
-- Init.Data.Nat.Bitwise.Lemmas
Nat.or_two_pow_eq_add_of_lt : ∀ {a n : ℕ}, a < 2 ^ n → a ||| 2 ^ n = a + 2 ^ n
-- Mathlib.CategoryTheory.Triangulated.Opposite.Triangulated
CategoryTheory.Pretriangulated.Opposite.instIsTriangulatedOpposite : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C], CategoryTheory.IsTriangulated Cᵒᵖ
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
MulAction.fixingSubgroup_le_stabilizer : ∀ (G : Type u_1) [inst : Group G] {α : Type u_2} [inst_1 : MulAction G α] (s : Set α),
  fixingSubgroup G s ≤ MulAction.stabilizer G s
-- Mathlib.NumberTheory.Niven
/-- `2 cos(q * π)` for `q : ℚ` is integral over `ℤ`, using the complex `cos` function.  -/
Complex.isIntegral_two_mul_cos_rat_mul_pi : ∀ (q : ℚ), IsIntegral ℤ (2 * Complex.cos (↑q * ↑Real.pi))
-- Init.Data.Nat.Div.Basic
Nat.mod_self : ∀ (n : ℕ), n % n = 0
-- Mathlib.Analysis.InnerProductSpace.l2Space
lp.inner_single_right : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] {G : ι → Type u_4} [inst_1 : (i : ι) → NormedAddCommGroup (G i)]
  [inst_2 : (i : ι) → InnerProductSpace 𝕜 (G i)] [inst_3 : DecidableEq ι] (i : ι) (a : G i) (f : ↥(lp G 2)),
  inner 𝕜 f (lp.single 2 i a) = inner 𝕜 (↑f i) a
-- Mathlib.Data.Num.Basic
ZNum.neg.injEq : ∀ (a a_1 : PosNum), (ZNum.neg a = ZNum.neg a_1) = (a = a_1)
-- Batteries.Data.String.Legacy
_private.Batteries.Data.String.Legacy.0.String.Pos.Raw.utf8GetAux.match_1.splitter : (motive : List Char → String.Pos.Raw → String.Pos.Raw → Sort u_1) →
  (x : List Char) →
    (x_1 x_2 : String.Pos.Raw) →
      ((x x_3 : String.Pos.Raw) → motive [] x x_3) →
        ((c : Char) → (cs : List Char) → (i p : String.Pos.Raw) → motive (c :: cs) i p) → motive x x_1 x_2
-- Mathlib.CategoryTheory.Abelian.Subobject
/-- In an abelian category, the subobjects and quotient objects of an object `X` are
order-isomorphic via taking kernels and cokernels.
Implemented here using subobjects in the opposite category,
since mathlib does not have a notion of quotient objects at the time of writing.  -/
CategoryTheory.Abelian.subobjectIsoSubobjectOp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Abelian C] → (X : C) → CategoryTheory.Subobject X ≃o (CategoryTheory.Subobject (Opposite.op X))ᵒᵈ
-- Mathlib.CategoryTheory.Monoidal.Arrow
CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.leftUnitor_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPushouts C]
  [inst_2 : CategoryTheory.Limits.HasInitial C] [inst_3 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_4 : CategoryTheory.MonoidalClosed C] [inst_5 : CategoryTheory.BraidedCategory C] {X Y : CategoryTheory.Arrow C}
  (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft
        (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Arrow C)) f)
      (CategoryTheory.MonoidalCategoryStruct.leftUnitor Y).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom f
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.maxKey?_eq_some_iff_getKey?_eq_self_and_forall : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {km : α},
  t.maxKey? = some km ↔ t.getKey? km = some km ∧ ∀ k ∈ t, (cmp k km).isLE = true
-- Init.Data.List.Find
List.findIdx.go.eq_def : ∀ {α : Type u} (p : α → Bool) (a : List α) (a_1 : ℕ),
  List.findIdx.go p a a_1 =
    match a, a_1 with
    | [], n => n
    | a :: l, n => bif p a then n else List.findIdx.go p l (n + 1)
-- Mathlib.RingTheory.Bialgebra.Basic
Bialgebra.counitAlgHom_self : ∀ {R : Type u_1} [inst : CommSemiring R], Bialgebra.counitAlgHom R R = AlgHom.id R R
-- Mathlib.Tactic.NormNum.Core
/-- `#norm_num e`, where `e` is an expression, will print the `norm_num` form of `e`.
Unlike `norm_num`, this command does not fail when no simplifications are made.
`#norm_num` understands local variables, so you can use them to introduce parameters.

(In the variants below, the `:` is optional but helpful for the parser.)

* `#norm_num [h1, ...] : e` adds the arguments `h1, ...` to the `simp` set in addition to the
  default `simp` set. All options for `simp` arguments are supported, in particular `←`, `↑`
  and `↓`.
* `#norm_num only : e` and `#norm_num only [h1, ...] : e` do not use the default `simp` set for
  simplification.
* `#norm_num (config := cfg) : e` uses `cfg` as configuration for `simp` calls (see the `simp`
  tactic for further details).
 -/
Mathlib.Tactic.normNumCmd : Lean.ParserDescr
-- Lean.Elab.Do.Basic
/-- The name of the monadic result variable.  -/
Lean.Elab.Do.DoElemCont.resultName : Lean.Elab.Do.DoElemCont → Lean.Name
-- Mathlib.Algebra.Homology.HomologicalBicomplex
HomologicalComplex₂.toGradedObjectMap_apply : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {I₁ : Type u_2} {I₂ : Type u_3} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {K L : HomologicalComplex₂ C c₁ c₂}
  (φ : K ⟶ L) (i₁ : I₁) (i₂ : I₂), HomologicalComplex₂.toGradedObjectMap φ (i₁, i₂) = (φ.f i₁).f i₂
-- Mathlib.Algebra.Lie.Weights.Basic
LieModule.map_genWeightSpace_eq_of_injective : ∀ {R : Type u_2} {L : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] {M₂ : Type u_5} [inst_8 : AddCommGroup M₂] [inst_9 : Module R M₂]
  [inst_10 : LieRingModule L M₂] [inst_11 : LieModule R L M₂] {χ : L → R} {f : M →ₗ⁅R,L⁆ M₂},
  Function.Injective ⇑f → LieSubmodule.map f (LieModule.genWeightSpace M χ) = LieModule.genWeightSpace M₂ χ ⊓ f.range
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
/-- This is the natural linear isometric equivalence induced by `f : F ≃ₗᵢ G`.  -/
LinearIsometryEquiv.lTensor : {𝕜 : Type u_1} →
  (E : Type u_2) →
    {F : Type u_3} →
      {G : Type u_4} →
        [inst : RCLike 𝕜] →
          [inst_1 : NormedAddCommGroup E] →
            [inst_2 : InnerProductSpace 𝕜 E] →
              [inst_3 : NormedAddCommGroup F] →
                [inst_4 : InnerProductSpace 𝕜 F] →
                  [inst_5 : NormedAddCommGroup G] →
                    [inst_6 : InnerProductSpace 𝕜 G] → (F ≃ₗᵢ[𝕜] G) → TensorProduct 𝕜 E F ≃ₗᵢ[𝕜] TensorProduct 𝕜 E G
-- Mathlib.NumberTheory.PrimeCounting
Nat.primesBelow_eq_filter_Ico_one : ∀ (n : ℕ), n.primesBelow = Finset.filter Nat.Prime (Finset.Ico 1 n)
-- Init.Data.SInt.Lemmas
Int8.toInt16_ofIntLE : ∀ {n : ℤ} (h₁ : Int8.minValue.toInt ≤ n) (h₂ : n ≤ Int8.maxValue.toInt),
  (Int8.ofIntLE n h₁ h₂).toInt16 = Int16.ofIntLE n ⋯ ⋯
-- Init.Data.SInt.Basic
/-- The power operation, raising a 64-bit signed integer to a natural number power,
wrapping around on overflow. Usually accessed via the `^` operator.

This function is currently *not* overridden at runtime with an efficient implementation,
and should be used with caution. See https://github.com/leanprover/lean4/issues/7887.
 -/
Int64.pow : Int64 → ℕ → Int64
-- Mathlib.Analysis.Convex.Topology
convexHull_subset_closedConvexHull : ∀ {𝕜 : Type u_2} {E : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] [inst_4 : TopologicalSpace E] {s : Set E}, (convexHull 𝕜) s ⊆ (closedConvexHull 𝕜) s
-- Lean.Declaration
Lean.Declaration.thmDecl.sizeOf_spec : ∀ (val : Lean.TheoremVal), sizeOf (Lean.Declaration.thmDecl val) = 1 + sizeOf val
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.toCharThreeNF_spec_of_b₂_eq_zero : ∀ {F : Type u_2} [inst : Field F] [inst_1 : CharP F 3] (W : WeierstrassCurve F),
  W.b₂ = 0 → (W.toCharThreeNF • W).IsShortNF
-- Mathlib.Combinatorics.Colex
Finset.Colex.lt_iff_exists_forall_lt : ∀ {α : Type u_1} [inst : LinearOrder α] {s t : Colex (Finset α)},
  s < t ↔ ∃ a ∈ ofColex t, a ∉ ofColex s ∧ ∀ b ∈ ofColex s, b ∉ ofColex t → b < a
-- Mathlib.AlgebraicGeometry.AlgClosed.Basic
AlgebraicGeometry.pointOfClosedPoint_apply : ∀ {X : AlgebraicGeometry.Scheme} {K : Type u} [inst : Field K] [inst_1 : IsAlgClosed K]
  (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) [inst_2 : AlgebraicGeometry.LocallyOfFiniteType f] (x : ↥X)
  (hx : IsClosed {x}) (a : ↥(AlgebraicGeometry.Spec (CommRingCat.of K))),
  (AlgebraicGeometry.pointOfClosedPoint f x hx) a = x
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.Bicone.toBinaryBiconeFunctor_map_hom : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y : C} {X_1 Y_1 : CategoryTheory.Limits.Bicone (CategoryTheory.Limits.pairFunction X Y)} (f : X_1 ⟶ Y_1),
  (CategoryTheory.Limits.Bicone.toBinaryBiconeFunctor.map f).hom = f.hom
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
/-- A finite group of prime order is cyclic.  -/
isAddCyclic_of_prime_card : ∀ {α : Type u_1} [inst : AddGroup α] {p : ℕ} [hp : Fact (Nat.Prime p)], Nat.card α = p → IsAddCyclic α
-- Mathlib.CategoryTheory.GlueData
CategoryTheory.GlueData.ι_gluedIso_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] {C' : Type u₂} [inst_1 : CategoryTheory.Category.{v, u₂} C']
  (D : CategoryTheory.GlueData C) (F : CategoryTheory.Functor C C')
  [inst_2 : CategoryTheory.Limits.HasMulticoequalizer D.diagram]
  [inst_3 : CategoryTheory.Limits.PreservesColimit D.diagram.multispan F]
  [inst_4 : ∀ (i j k : D.J), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (D.f i j) (D.f i k)) F]
  (i : D.J), CategoryTheory.CategoryStruct.comp ((D.mapGlueData F).ι i) (D.gluedIso F).inv = F.map (D.ι i)
-- Lean.Widget.InteractiveDiagnostic
_private.Lean.Widget.InteractiveDiagnostic.0.Lean.Widget.InteractiveDiagnostic.toDiagnostic.prettyTt : Lean.Widget.InteractiveMessage → String
-- Mathlib.CategoryTheory.Sites.Sheaf
CategoryTheory.Presheaf.isSheaf_comp_of_isSheaf : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {B : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} B] (J : CategoryTheory.GrothendieckTopology C)
  (P : CategoryTheory.Functor Cᵒᵖ A) (s : CategoryTheory.Functor A B)
  [CategoryTheory.Limits.PreservesLimitsOfSize.{v₁, max v₁ u₁, v₂, v₃, u₂, u₃} s],
  CategoryTheory.Presheaf.IsSheaf J P → CategoryTheory.Presheaf.IsSheaf J (P.comp s)
-- Mathlib.RingTheory.DedekindDomain.Factorization
/-- If `p` is a maximal ideal, then the lift of `p` in an extension is the product of the primes
over `p` to the power the ramification index.
 -/
Ideal.map_algebraMap_eq_finsetProd_pow : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {S : Type u_3} [inst_2 : CommRing S]
  [inst_3 : Algebra S R] [inst_4 : Algebra.IsIntegral S R] [inst_5 : IsDomain S] [inst_6 : Module.IsTorsionFree S R]
  {p : Ideal S} [inst_7 : p.IsMaximal],
  p ≠ 0 → Ideal.map (algebraMap S R) p = ∏ P ∈ (p.primesOver R).toFinset, P ^ P.ramificationIdx S
-- Mathlib.Data.Multiset.Interval
Multiset.card_Ico : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Multiset α),
  (Finset.Ico s t).card = ∏ i ∈ s.toFinset ∪ t.toFinset, (Multiset.count i t + 1 - Multiset.count i s) - 1
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.mk' : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (functor : CategoryTheory.Functor C D) →
          (inverse : CategoryTheory.Functor D C) →
            (unitIso : CategoryTheory.Functor.id C ≅ functor.comp inverse) →
              (counitIso : inverse.comp functor ≅ CategoryTheory.Functor.id D) →
                autoParam
                    (∀ (X : C),
                      CategoryTheory.CategoryStruct.comp (functor.map (unitIso.hom.app X))
                          (counitIso.hom.app (functor.obj X)) =
                        CategoryTheory.CategoryStruct.id (functor.obj X))
                    CategoryTheory.Equivalence.functor_unitIso_comp._autoParam →
                  (C ≌ D)
-- Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
integrable_cexp_quadratic : ∀ {b : ℂ},
  0 < b.re →
    ∀ (c d : ℂ), MeasureTheory.Integrable (fun x => Complex.exp (-b * ↑x ^ 2 + c * ↑x + d)) MeasureTheory.volume
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientAddGroup.subsingleton_quotient_top : ∀ {G : Type u} [inst : AddGroup G], Subsingleton (G ⧸ ⊤)
-- Lean.Widget.Types
/-- A widget module is a unit of source code that can execute in the infoview.

Every module definition must either be annotated with `@[widget_module]`,
or use a value of `javascript` identical to that of another definition
annotated with `@[widget_module]`.
This makes it possible for the infoview to load the module.

See the [manual entry](https://lean-lang.org/examples/1900-1-1-widgets/)
for more information on how to use the widgets system.  -/
Lean.Widget.Module : Type
-- Mathlib.Logic.Relation
refl_iff_eq_le : ∀ {α : Type u_1} {r : α → α → Prop}, Std.Refl r ↔ Eq ≤ r
-- Init.Data.Int.DivMod.Bootstrap
Int.emod_lt_of_pos : ∀ (a : ℤ) {b : ℤ}, 0 < b → a % b < b
-- Init.Data.String.Bootstrap
String.Internal.isPrefixOf : String → String → Bool
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.think_append : ∀ {α : Type u} (s t : Stream'.WSeq α), s.think.append t = (s.append t).think
-- Mathlib.Util.AtomM.Recurse
Mathlib.Tactic.AtomM.Recurse.Context.mk : Lean.Meta.Simp.Context →
  (Lean.Meta.Simp.Result → Lean.MetaM Lean.Meta.Simp.Result) → Mathlib.Tactic.AtomM.Recurse.Context
-- Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Dense.eq_zero_of_mem_orthogonal : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {K : Submodule 𝕜 E} {x : E}, Dense ↑K → x ∈ Kᗮ → x = 0
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.map_update_neg : ∀ {R : Type u_1} [inst : Semiring R] {M' : Type u_5} [inst_1 : AddCommGroup M'] [inst_2 : Module R M'] {N' : Type u_6}
  [inst_3 : AddCommGroup N'] [inst_4 : Module R N'] {ι : Type u_7} (g' : M' [⋀^ι]→ₗ[R] N') (v' : ι → M')
  [inst_5 : DecidableEq ι] (i : ι) (x : M'), g' (Function.update v' i (-x)) = -g' (Function.update v' i x)
-- Mathlib.Analysis.Calculus.Deriv.Add
/-- Eta-expanded form of `HasDerivAtFilter.sub` -/
HasDerivAtFilter.fun_sub : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f g : 𝕜 → F} {f' g' : F} {L : Filter (𝕜 × 𝕜)},
  HasDerivAtFilter f f' L → HasDerivAtFilter g g' L → HasDerivAtFilter (fun i => f i - g i) (f' - g') L
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.snd_mem_support_of_mem_edges : ∀ {V : Type u} {G : SimpleGraph V} {t u v w : V} (p : G.Walk v w), s(t, u) ∈ p.edges → u ∈ p.support
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.balanceL!.match_3.congr_eq_3 : ∀ {α : Type u_1} {β : α → Type u_2}
  (motive : Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl α β → Sort u_3)
  (ll lr : Std.DTreeMap.Internal.Impl α β)
  (h_1 :
    (lls : ℕ) →
      (k : α) →
        (v : β k) →
          (l r : Std.DTreeMap.Internal.Impl α β) →
            (lrs : ℕ) →
              (lrk : α) →
                (lrv : β lrk) →
                  (lrl lrr : Std.DTreeMap.Internal.Impl α β) →
                    motive (Std.DTreeMap.Internal.Impl.inner lls k v l r)
                      (Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr))
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l r : Std.DTreeMap.Internal.Impl α β) →
            motive (Std.DTreeMap.Internal.Impl.inner size k v l r) Std.DTreeMap.Internal.Impl.leaf)
  (h_3 : (x : Std.DTreeMap.Internal.Impl α β) → motive Std.DTreeMap.Internal.Impl.leaf x)
  (x : Std.DTreeMap.Internal.Impl α β),
  ll = Std.DTreeMap.Internal.Impl.leaf →
    lr = x →
      (match ll, lr with
        | Std.DTreeMap.Internal.Impl.inner lls k v l r, Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr =>
          h_1 lls k v l r lrs lrk lrv lrl lrr
        | Std.DTreeMap.Internal.Impl.inner size k v l r, Std.DTreeMap.Internal.Impl.leaf => h_2 size k v l r
        | Std.DTreeMap.Internal.Impl.leaf, x => h_3 x) ≍
        h_3 x
-- Mathlib.Analysis.InnerProductSpace.Positive
LinearMap.IsPositive.adjoint_eq : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E}, T.IsPositive → LinearMap.adjoint T = T
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.takeTR.go.eq_2 : ∀ {α : Type u_1} (l : List α) (a : Array α) (head : α) (xs : List α), List.takeTR.go✝ l (head :: xs) 0 a = a.toList
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
_private.Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop.0.Std.IterM.length_eq_match_step.match_1.eq_1 : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} (motive : Std.IterStep (Std.IterM m β) β → Sort u_3) (it' : Std.IterM m β)
  (out : β) (h_1 : (it' : Std.IterM m β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.IterM m β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.yield it' out with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_1 it' out
-- Mathlib.Analysis.Normed.Group.Basic
preimage_add_closedBall : ∀ {E : Type u_5} [inst : SeminormedAddCommGroup E] (a b : E) (r : ℝ),
  (fun x => b + x) ⁻¹' Metric.closedBall a r = Metric.closedBall (a - b) r
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq
/-- The square with `0 : 0 ⟶ 0` on the right and `𝟙 X` on the left is a pushout square.  -/
CategoryTheory.IsPushout.zero_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (X : C),
  CategoryTheory.IsPushout 0 (CategoryTheory.CategoryStruct.id X) 0 0
-- Mathlib.Data.Finset.Image
Finset.mem_subtype : ∀ {α : Type u_1} {p : α → Prop} [inst : DecidablePred p] {s : Finset α} {a : Subtype p}, a ∈ Finset.subtype p s ↔ ↑a ∈ s
-- Lean.Meta.Tactic.Grind.Extension
/-- Stores whether patterns were inferred using the minimal indexable subexpression condition.  -/
Lean.Meta.Grind.EMatchTheorem.minIndexable : Lean.Meta.Grind.EMatchTheorem → Bool
-- Mathlib.Algebra.Polynomial.BigOperators
Polynomial.coeff_prod_of_natDegree_le : ∀ {R : Type u} {ι : Type w} (s : Finset ι) [inst : CommSemiring R] (f : ι → Polynomial R) (n : ℕ),
  (∀ p ∈ s, (f p).natDegree ≤ n) → (∏ i ∈ s, f i).coeff (s.card * n) = ∏ i ∈ s, (f i).coeff n
-- Mathlib.Data.Finset.Insert
/-- **Alias** of the forward direction of `Finset.nontrivial_coe`. -/
Finset.Nontrivial.of_coe : ∀ {α : Type u_1} {s : Finset α}, (↑s).Nontrivial → s.Nontrivial
-- Mathlib.Algebra.Module.Equiv.Basic
addMonoidEndRingEquivInt_symm_apply : ∀ (A : Type u_9) [inst : AddCommGroup A] (a : A →ₗ[ℤ] A),
  (addMonoidEndRingEquivInt A).symm a = (addMonoidHomLequivInt ℤ).invFun a
-- Mathlib.Tactic.Ring.Common
/-- Evaluate the negation of a coefficient.  -/
Mathlib.Tactic.Ring.Common.RingCompute.neg : {u : Lean.Level} →
  {α : Q(Type u)} →
    {BaseType : Q(«$α») → Type} →
      {sα : Q(CommSemiring «$α»)} →
        Mathlib.Tactic.Ring.Common.RingCompute BaseType sα →
          {x : Q(«$α»)} →
            (rα : Q(CommRing «$α»)) → BaseType x → Lean.MetaM (Mathlib.Tactic.Ring.Common.Result BaseType q(-«$x»))
-- Mathlib.Analysis.InnerProductSpace.Symmetric
LinearMap.IsSymmetric.isSymmetric_smul_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {f : E →ₗ[𝕜] E}, f.IsSymmetric → f ≠ 0 → ∀ {α : 𝕜}, (α • f).IsSymmetric ↔ IsSelfAdjoint α
-- Mathlib.Data.List.MinMax
List.le_maximum_of_mem : ∀ {α : Type u_1} [inst : LinearOrder α] {l : List α} {a m : α}, a ∈ l → l.maximum = ↑m → a ≤ m
-- Std.Data.DTreeMap.Internal.WF.Defs
/-- `mergeWith` preserves well-formedness. Later shown to be subsumed by `.wf`.  -/
Std.DTreeMap.Internal.Impl.WF.constMergeWith : ∀ {α : Type u} [inst : Ord α] {x : Type v} {t₁ t₂ : Std.DTreeMap.Internal.Impl α fun x_1 => x} {f : α → x → x → x}
  {h : t₁.Balanced}, t₁.WF → (Std.DTreeMap.Internal.Impl.Const.mergeWith f t₁ t₂ h).impl.WF
-- Init.Data.Int.DivMod.Lemmas
Int.mul_sub_fdiv_left : ∀ (b : ℤ) {a : ℤ} (c : ℤ), a ≠ 0 → (a * b - c).fdiv a = b + (-c).fdiv a
-- Mathlib.RingTheory.ChainOfDivisors
DivisorChain.exists_chain_of_prime_pow : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [IsCancelMulZero M] {p : Associates M} {n : ℕ},
  n ≠ 0 → Prime p → ∃ c, c 1 = p ∧ StrictMono c ∧ ∀ {r : Associates M}, r ≤ p ^ n ↔ ∃ i, r = c i
-- Mathlib.Logic.Encodable.Basic
Encodable.encode_nat : ∀ (n : ℕ), Encodable.encode n = n
-- Mathlib.Data.Set.Lattice
/-- A specialization of `mem_iInter₂`.  -/
Set.mem_biInter : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : α → Set β} {y : β}, (∀ x ∈ s, y ∈ t x) → y ∈ ⋂ x ∈ s, t x
-- Mathlib.RingTheory.RingHom.Locally
/-- If `P` is preserved by localizations, then so is `Locally P`.  -/
RingHom.locally_localizationPreserves : ∀ {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  (RingHom.LocalizationPreserves fun {R S} [CommRing R] [CommRing S] => P) →
    RingHom.LocalizationPreserves fun {R S} [CommRing R] [CommRing S] =>
      RingHom.Locally fun {R S} [CommRing R] [CommRing S] => P
-- Mathlib.Logic.Equiv.Fin.Rotate
finRotate_succ : ∀ (n : ℕ), finRotate (n + 1) = finAddFlip.trans (finCongr ⋯)
-- Lean.Server.FileWorker.SemanticHighlighting
Lean.Server.FileWorker.instFromJsonAbsoluteLspSemanticToken : Lean.FromJson Lean.Server.FileWorker.AbsoluteLspSemanticToken
-- Mathlib.Algebra.Tropical.Basic
Tropical.trop_monotone : ∀ {R : Type u} [inst : Preorder R], Monotone Tropical.trop
-- Aesop.Tree.Data.ForwardRuleMatches
Aesop.ForwardRuleMatches.instEmptyCollection : EmptyCollection Aesop.ForwardRuleMatches
-- Mathlib.Algebra.Group.Basic
/-- **Alias** of the reverse direction of `sub_eq_zero`. -/
sub_eq_zero_of_eq : ∀ {G : Type u_3} [inst : AddGroup G] {a b : G}, a = b → a - b = 0
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.map_add_nat : ∀ (f : CircleDeg1Lift) (x : ℝ) (n : ℕ), f (x + ↑n) = f x + ↑n
-- Mathlib.Combinatorics.SimpleGraph.CycleGraph
_private.Mathlib.Combinatorics.SimpleGraph.CycleGraph.0.SimpleGraph.cycleGraph.match_1.eq_3 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1) (h_3 : (n : ℕ) → motive n.succ.succ),
  (match n.succ.succ with
    | 0 => h_1 ()
    | 1 => h_2 ()
    | n.succ.succ => h_3 n) =
    h_3 n
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.isSome_maxKey?_of_contains : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  t.contains k = true → t.maxKey?.isSome = true