mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
/-- If there is a primitive `n`th root of unity in `K`, then `X ^ n - 1 = ∏ (X - μ)`, where `μ`
varies over the `n`-th roots of unity.  -/
Polynomial.X_pow_sub_one_eq_prod : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] {ζ : R} {n : ℕ},
  0 < n →
    IsPrimitiveRoot ζ n → Polynomial.X ^ n - 1 = ∏ ζ ∈ Polynomial.nthRootsFinset n 1, (Polynomial.X - Polynomial.C ζ)
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.mk'_sub_mk' : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Submonoid R} {M : Type u_6} {M' : Type u_7} [inst_1 : AddCommGroup M]
  [inst_2 : SubtractionCommMonoid M'] [inst_3 : Module R M] [inst_4 : Module R M'] (f : M →ₗ[R] M')
  [inst_5 : IsLocalizedModule S f] (m₁ m₂ : M) (s₁ s₂ : ↥S),
  IsLocalizedModule.mk' f m₁ s₁ - IsLocalizedModule.mk' f m₂ s₂ = IsLocalizedModule.mk' f (s₂ • m₁ - s₁ • m₂) (s₁ * s₂)
-- Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives
HomotopyCategory.Plus.inverseImage_quasiIso_mapCochainComplexPlus_injectiveObjectι : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C],
  (CochainComplex.Plus.quasiIso C).inverseImage (CategoryTheory.InjectiveObject.ι C).mapCochainComplexPlus =
    (HomologicalComplex.homotopyEquivalences (CategoryTheory.InjectiveObject C) (ComplexShape.up ℤ)).inverseImage
      (CochainComplex.Plus.ι (CategoryTheory.InjectiveObject C))
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.ext_iff : ∀ {K : Type u} [inst : Field K] {A B : ValuationSubring K}, A = B ↔ ∀ (x : K), x ∈ A ↔ x ∈ B
-- Mathlib.RingTheory.MvPowerSeries.Substitution
MvPowerSeries.rescale_one : ∀ {σ : Type u_1} {R : Type u_9} [inst : CommSemiring R], MvPowerSeries.rescale 1 = RingHom.id (MvPowerSeries σ R)
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.SavedState : Type
-- Mathlib.Data.Rel.Cover
SetRel.isCover_id : ∀ {X : Type u_1} {s N : Set X}, SetRel.id.IsCover s N ↔ s ⊆ N
-- Mathlib.Algebra.Homology.Embedding.TruncGE
HomologicalComplex.truncGE'.XIso.congr_simp : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : ∀ (i' : ι'), K.HasHomology i'] {i : ι}
  (hi : ¬e.BoundaryGE i), HomologicalComplex.truncGE'.XIso K e hi = HomologicalComplex.truncGE'.XIso K e hi
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
ContinuousLinearMap.lTensor_comp_commIsometry : ∀ {𝕜 : 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 : E →L[𝕜] F),
  ContinuousLinearMap.lTensor G f ∘SL ↑↑(TensorProduct.commIsometry 𝕜 E G) =
    ↑↑(TensorProduct.commIsometry 𝕜 F G) ∘SL ContinuousLinearMap.rTensor G f
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.sndₗ_apply : ∀ (p : ENNReal) (𝕜 : Type u_1) (α : Type u_2) (β : Type u_3) [inst : Semiring 𝕜] [inst_1 : AddCommGroup α]
  [inst_2 : AddCommGroup β] [inst_3 : Module 𝕜 α] [inst_4 : Module 𝕜 β] (x : WithLp p (α × β)),
  (WithLp.sndₗ p 𝕜 α β) x = x.snd
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.mul_single_apply_of_not_exists_mul : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : Mul M] (r : R) {g g' : M} (x : MonoidAlgebra R M),
  (¬∃ d, g' = d * g) → (x * MonoidAlgebra.single g r).coeff g' = 0
-- Init.System.IOError
/-- A required resource does not exist.

This corresponds to the POSIX errors `ENXIO`, `EHOSTUNREACH`, `ENETUNREACH`, `ECHILD`,
`ECONNREFUSED`, `ENODATA`, `ENOMSG`, and `ESRCH`.
 -/
IO.Error.noSuchThing : Option String → UInt32 → String → IO.Error
-- Mathlib.CategoryTheory.Monoidal.Action.Opposites
CategoryTheory.MonoidalCategory.MonoidalLeftAction.oppositeLeftAction_actionAssocIso_op : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] (c c' : C) (d : D),
  CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso (Opposite.op c) (Opposite.op c')
      (Opposite.op d) =
    (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso c c' d).symm.op
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.HomEquiv.tensor : ∀ {C : Type u} {W X Y Z : CategoryTheory.FreeMonoidalCategory C} {f f' : W.Hom X} {g g' : Y.Hom Z},
  CategoryTheory.FreeMonoidalCategory.HomEquiv f f' →
    CategoryTheory.FreeMonoidalCategory.HomEquiv g g' →
      CategoryTheory.FreeMonoidalCategory.HomEquiv (f.tensor g) (f'.tensor g')
-- Mathlib.Lean.Meta.RefinedDiscrTree.Encode
/-- Sometimes, we need to not index lambda binders, in particular when the body is the application of
a metavariable.

In the case where we do index the lambda binders,
`withLams` efficiently adds the lambdas and `key` to the result.
 -/
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Encode.0.Lean.Meta.RefinedDiscrTree.withLams : List Lean.FVarId →
  Lean.Meta.RefinedDiscrTree.Key → StateT Lean.Meta.RefinedDiscrTree.LazyEntry Lean.MetaM Lean.Meta.RefinedDiscrTree.Key
-- Lean.Meta.DiscrTree.Basic
Lean.Meta.DiscrTree.Key.format : Lean.Meta.DiscrTree.Key → Std.Format
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Ordinal.cof_iSup_le_lift : ∀ {ι : Type u} {f : ι → Ordinal.{max u v}},
  (∀ (i : ι), f i < iSup f) → (iSup f).cof ≤ Cardinal.lift.{v, u} (Cardinal.mk ι)
-- Init.Data.Iterators.Consumers.Monadic.Loop
/-- Returns the first output of the iterator for which the predicate `p` returns `true`, or `none` if
no such output is found.

`O(|it|)`. Short-circuits upon encountering the first match. The elements in `it` are examined in
order of iteration.

This function is deprecated. Instead of `it.allowNontermination.find?`, use `it.find?`.

Examples:
* `([7, 6, 5, 8, 1, 2, 6].iterM Id).allowNontermination.find? (· < 5) = pure (some 1)`
* `([7, 6, 5, 8, 1, 2, 6].iterM Id).allowNontermination.find? (· < 1) = pure none`
 -/
Std.IterM.Partial.find? : {α β : Type w} →
  {m : Type w → Type w'} →
    [Monad m] →
      [inst : Std.Iterator α m β] → [Std.IteratorLoop α m m] → Std.IterM.Partial m β → (β → Bool) → m (Option β)
-- Mathlib.Algebra.Homology.CommSq
CategoryTheory.CommSq.shortComplex'_X₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {X₁ X₂ X₃ X₄ : C}
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X₂ X₃] {fst : X₁ ⟶ X₂} {snd : X₁ ⟶ X₃} {f : X₂ ⟶ X₄} {g : X₃ ⟶ X₄}
  (sq : CategoryTheory.CommSq fst snd f g), sq.shortComplex'.X₁ = X₁
-- Mathlib.Algebra.Group.Equiv.Defs
MulEquiv.toFun_eq_coe : ∀ {M : Type u_4} {N : Type u_5} [inst : Mul M] [inst_1 : Mul N] (f : M ≃* N), f.toFun = ⇑f
-- Lean.Meta.Sym.SymM
/-- Information about each argument position.  -/
Lean.Meta.Sym.ProofInstInfo.argsInfo : Lean.Meta.Sym.ProofInstInfo → Array Lean.Meta.Sym.ProofInstArgInfo
-- Init.Data.UInt.Bitwise
USize.ofFin_or : ∀ (a b : Fin USize.size), USize.ofFin (a ||| b) = USize.ofFin a ||| USize.ofFin b
-- Init.Internal.Order.Basic
/-- The bottom element is the least upper bound of the empty chain.

This is intended to be used in the construction of `partial_fixpoint`, and not meant to be used otherwise.
 -/
Lean.Order.bot : {α : Sort u} → [Lean.Order.CCPO α] → α
-- Lean.Elab.Command
Lean.Elab.Command.instMonadEvalTermElabMCommandElabM : MonadEval Lean.Elab.TermElabM Lean.Elab.Command.CommandElabM
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Iso.hom_inv_id_triangle_hom₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  {A B : CategoryTheory.Pretriangulated.Triangle C} (e : A ≅ B),
  CategoryTheory.CategoryStruct.comp e.hom.hom₂ e.inv.hom₂ = CategoryTheory.CategoryStruct.id A.obj₂
-- Mathlib.Order.Atoms
/-- A simple `BoundedOrder` is also a `CompleteBooleanAlgebra`.  -/
IsSimpleOrder.completeBooleanAlgebra : {α : Type u_2} → [inst : Lattice α] → [inst_1 : BoundedOrder α] → [IsSimpleOrder α] → CompleteBooleanAlgebra α
-- Mathlib.CategoryTheory.Sites.Sheafification
/-- A proposition saying that the inclusion functor from sheaves to presheaves admits a left adjoint.
 -/
CategoryTheory.HasWeakSheafify : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    CategoryTheory.GrothendieckTopology C → (A : Type u₂) → [CategoryTheory.Category.{v₂, u₂} A] → Prop
-- Mathlib.Algebra.Module.Equiv.Basic
LinearEquiv.congrLeft_symm_apply : ∀ (M : Type u_5) {M₂ : Type u_7} {M₃ : Type u_8} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid M₂]
  [inst_2 : AddCommMonoid M₃] {R : Type u_9} (S : Type u_10) [inst_3 : Semiring R] [inst_4 : Semiring S]
  [inst_5 : Module R M₂] [inst_6 : Module R M₃] [inst_7 : Module R M] [inst_8 : Module S M]
  [inst_9 : SMulCommClass R S M] (e : M₂ ≃ₗ[R] M₃) (a : M₃ →ₗ[R] M),
  (LinearEquiv.congrLeft M S e).symm a = (e.arrowCongrAddEquiv (LinearEquiv.refl R M)).invFun a
-- Mathlib.Logic.Equiv.Fin.Basic
Equiv.embeddingFinSucc_snd : ∀ {n : ℕ} {ι : Type u_1} (e : Fin (n + 1) ↪ ι), ↑((Equiv.embeddingFinSucc n ι) e).snd = e 0
-- Mathlib.CategoryTheory.EffectiveEpi.Preserves
CategoryTheory.Functor.instPreservesEffectiveEpiFamiliesOfIsEquivalence : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor C D) [F.IsEquivalence],
  F.PreservesEffectiveEpiFamilies
-- Mathlib.NumberTheory.Padics.RingHoms
/-- `toZModHom` is an auxiliary constructor for creating ring homs from `ℤ_[p]` to `ZMod v`.
 -/
PadicInt.toZModHom : {p : ℕ} →
  [hp_prime : Fact (Nat.Prime p)] →
    (v : ℕ) →
      (f : ℤ_[p] → ℕ) →
        (∀ (x : ℤ_[p]), x - ↑(f x) ∈ Ideal.span {↑v}) →
          (∀ (x : ℤ_[p]) (a b : ℕ), x - ↑a ∈ Ideal.span {↑v} → x - ↑b ∈ Ideal.span {↑v} → ↑a = ↑b) → ℤ_[p] →+* ZMod v
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
MultipliableLocallyUniformly.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : CommMonoid α] (f : ι → β → α) [inst_1 : UniformSpace α]
  [inst_2 : TopologicalSpace β], MultipliableLocallyUniformly f = ∃ g, HasProdLocallyUniformly f g
-- Mathlib.CategoryTheory.Limits.Cones
/-- There is a morphism from an extended cone to the original cone.  -/
CategoryTheory.Limits.Cone.extendHom : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          (s : CategoryTheory.Limits.Cone F) → {X : C} → (f : X ⟶ s.pt) → s.extend f ⟶ s
-- Mathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived
/-- A left derived functor is a pointwise left derived functor when
there exists a pointwise left derived functor.  -/
CategoryTheory.Functor.isPointwiseRightKanExtensionOfHasPointwiseLeftDerivedFunctor : {C : Type u₁} →
  {D : Type u₂} →
    {H : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} C] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} H] →
            (F' : CategoryTheory.Functor D H) →
              {F : CategoryTheory.Functor C H} →
                {L : CategoryTheory.Functor C D} →
                  (α : L.comp F' ⟶ F) →
                    (W : CategoryTheory.MorphismProperty C) →
                      [F.HasPointwiseLeftDerivedFunctor W] →
                        [inst_4 : L.IsLocalization W] →
                          [F'.IsLeftDerivedFunctor α W] →
                            (CategoryTheory.Functor.RightExtension.mk F' α).IsPointwiseRightKanExtension
-- Mathlib.Data.Rel
/-- Domain of a relation.  -/
SetRel.dom : {α : Type u_1} → {β : Type u_2} → SetRel α β → Set α
-- Mathlib.Data.List.OfFn
/-- `Fin.sigma_eq_iff_eq_comp_cast` may be useful to work with the RHS of this expression.  -/
List.ofFn_inj' : ∀ {α : Type u} {m n : ℕ} {f : Fin m → α} {g : Fin n → α}, List.ofFn f = List.ofFn g ↔ ⟨m, f⟩ = ⟨n, g⟩
-- Batteries.Tactic.GeneralizeProofs
/-- `generalize_proofs ids* [at locs]?` generalizes proofs in the current goal,
turning them into new local hypotheses.

- `generalize_proofs` generalizes proofs in the target.
- `generalize_proofs at h₁ h₂` generalized proofs in hypotheses `h₁` and `h₂`.
- `generalize_proofs at *` generalizes proofs in the entire local context.
- `generalize_proofs pf₁ pf₂ pf₃` uses names `pf₁`, `pf₂`, and `pf₃` for the generalized proofs.
  These can be `_` to not name proofs.

If a proof is already present in the local context, it will use that rather than create a new
local hypothesis.

When doing `generalize_proofs at h`, if `h` is a let binding, its value is cleared,
and furthermore if `h` duplicates a preceding local hypothesis then it is eliminated.

The tactic is able to abstract proofs from under binders, creating universally quantified
proofs in the local context.
To disable this, use `generalize_proofs -abstract`.
The tactic is also set to recursively abstract proofs from the types of the generalized proofs.
This can be controlled with the `maxDepth` configuration option,
with `generalize_proofs (config := { maxDepth := 0 })` turning this feature off.

For example:
```lean
def List.nthLe {α} (l : List α) (n : ℕ) (_h : n < l.length) : α := sorry
example : List.nthLe [1, 2] 1 (by simp) = 2 := by
  -- ⊢ [1, 2].nthLe 1 ⋯ = 2
  generalize_proofs h
  -- h : 1 < [1, 2].length
  -- ⊢ [1, 2].nthLe 1 h = 2
```
 -/
Batteries.Tactic.generalizeProofsElab : Lean.ParserDescr
-- Mathlib.Data.Nat.Cast.Basic
Pi.ofNat_def : ∀ {α : Type u_1} {π : α → Type u_3} (n : ℕ) [inst : (i : α) → OfNat (π i) n], OfNat.ofNat n = fun x => OfNat.ofNat n
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.Raw₀.reinsertAux_eq : ∀ {α : Type u} {β : α → Type v} [inst : Hashable α] (data : { d // 0 < d.size }) (a : α) (b : β a),
  ↑(Std.DHashMap.Internal.Raw₀.reinsertAux hash data a b) =
    Std.DHashMap.Internal.updateBucket ↑data ⋯ a fun l => Std.DHashMap.Internal.AssocList.cons a b l
-- Lean.Meta.Tactic.Grind.Split
Lean.Meta.Grind.SplitCandidateWithAnchor.mk : Lean.Meta.Grind.SplitInfo → ℕ → Bool → Lean.Expr → UInt64 → Lean.Meta.Grind.SplitCandidateWithAnchor
-- Mathlib.Analysis.Matrix.Normed
Matrix.linfty_opNorm_replicateCol : ∀ {m : Type u_3} {α : Type u_5} {ι : Type u_7} [inst : Fintype m] [inst_1 : Unique ι]
  [inst_2 : SeminormedAddCommGroup α] (v : m → α), ‖Matrix.replicateCol ι v‖ = ‖v‖
-- Mathlib.Data.ENNReal.Basic
ENNReal.canLift : CanLift ENNReal NNReal ENNReal.ofNNReal fun x => x ≠ ⊤
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.faithful_inverse : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {E : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} E]
  (e : C ≌ E), e.inverse.Faithful
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
CategoryTheory.Pseudofunctor.Grothendieck.Hom.mk : {𝒮 : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
    {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮) CategoryTheory.Cat} →
      {X Y : F.Grothendieck} → (base : X.base ⟶ Y.base) → ((F.map base.toLoc).toFunctor.obj X.fiber ⟶ Y.fiber) → X.Hom Y
-- Mathlib.Order.Interval.Set.Basic
Set.Ico_eq_Ioc_same_iff : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, Set.Ico b a = Set.Ioc b a ↔ ¬b < a
-- Mathlib.CategoryTheory.Sites.Coverage
CategoryTheory.Precoverage.Saturate.hcongr_5 : ∀ (C C' : Type u_1),
  C = C' →
    ∀ (inst : CategoryTheory.Category.{u_2, u_1} C) (inst' : CategoryTheory.Category.{u_2, u_1} C'),
      inst ≍ inst' →
        ∀ (J : CategoryTheory.Precoverage C) (J' : CategoryTheory.Precoverage C'),
          J ≍ J' →
            ∀ (X : C) (X' : C'),
              X ≍ X' →
                ∀ (a : CategoryTheory.Sieve X) (a' : CategoryTheory.Sieve X'),
                  a ≍ a' → J.Saturate X a ≍ J'.Saturate X' a'
-- Mathlib.Combinatorics.Matroid.Constructions
Matroid.uniqueBaseOn_inter_isBasis : ∀ {α : Type u_1} {E I X : Set α}, X ⊆ E → (Matroid.uniqueBaseOn I E).IsBasis (X ∩ I) X
-- Init.ShareCommon
ShareCommon.Object.ptrEq : ShareCommon.Object → ShareCommon.Object → Bool
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.comap_map_eq_of_injective : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_4}
  [inst_2 : FunLike F M N] [mc : AddMonoidHomClass F M N] {f : F},
  Function.Injective ⇑f → ∀ (S : AddSubmonoid M), AddSubmonoid.comap f (AddSubmonoid.map f S) = S
-- Mathlib.Algebra.Group.Subgroup.Map
Subgroup.map_map : ∀ {G : Type u_1} [inst : Group G] (K : Subgroup G) {N : Type u_5} [inst_1 : Group N] {P : Type u_6} [inst_2 : Group P]
  (g : N →* P) (f : G →* N), Subgroup.map g (Subgroup.map f K) = Subgroup.map (g.comp f) K
-- Mathlib.Algebra.Group.Submonoid.Support
AddSubmonoid.IsSpanning.of_le : ∀ {G : Type u_1} [inst : AddGroup G] {M N : AddSubmonoid G}, M.IsSpanning → M ≤ N → N.IsSpanning
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.whiskerLeft_rightUnitor : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y : C),
  CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.MonoidalCategoryStruct.rightUnitor Y).hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator X Y (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv
      (CategoryTheory.MonoidalCategoryStruct.rightUnitor (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)).hom
-- Init.Data.Nat.ToString
_private.Init.Data.Nat.ToString.0.Nat.toDigitsCore_of_lt_base : ∀ {b n fuel : ℕ} {cs : List Char}, n < b → n < fuel → b.toDigitsCore fuel n cs = n.digitChar :: cs
-- Mathlib.Algebra.Group.Commute.Defs
AddCommute.on_refl : ∀ {G : Type u_1} {S : Type u_3} [inst : Add S] {f : G → S}, Std.Refl fun a b => AddCommute (f a) (f b)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.isEmpty_filter!_key_iff : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] {f : α → Bool},
  t.WF →
    ((Std.DTreeMap.Internal.Impl.filter! (fun a x => f a) t).isEmpty = true ↔
      ∀ (k : α) (h : Std.DTreeMap.Internal.Impl.contains k t = true), f (t.getKey k h) = false)
-- Mathlib.Analysis.Distribution.FourierMultiplier
TemperedDistribution.fourierMultiplierCLM.congr_simp : ∀ {E : Type u_3} (F : Type u_4) [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F]
  [inst_2 : InnerProductSpace ℝ E] [inst_3 : NormedSpace ℂ F] [inst_4 : FiniteDimensional ℝ E]
  [inst_5 : MeasurableSpace E] [inst_6 : BorelSpace E] (g g_1 : E → ℂ),
  g = g_1 → TemperedDistribution.fourierMultiplierCLM F g = TemperedDistribution.fourierMultiplierCLM F g_1
-- Mathlib.Analysis.Calculus.Deriv.Basic
derivWithin_congr : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f f₁ : 𝕜 → F} {x : 𝕜} {s : Set 𝕜},
  Set.EqOn f₁ f s → f₁ x = f x → derivWithin f₁ s x = derivWithin f s x
-- Mathlib.Analysis.Normed.Ring.Basic
NNReal.enorm_eq : ∀ (x : NNReal), ‖↑x‖ₑ = ↑x
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Power.denote_eq : ∀ {α : Type u_1} [inst : Lean.Grind.Semiring α] (ctx : Lean.Grind.CommRing.Context α) (p : Lean.Grind.CommRing.Power),
  Lean.Grind.CommRing.Power.denote ctx p = Lean.Grind.CommRing.Var.denote ctx p.x ^ p.k
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.prodMkLeft_apply' : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) (ca : γ × α) (s : Set β),
  ((ProbabilityTheory.Kernel.prodMkLeft γ κ) ca) s = (κ ca.2) s
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometry.one_def : ∀ {R : Type u_1} {E : Type u_5} [inst : Semiring R] [inst_1 : SeminormedAddCommGroup E] [inst_2 : Module R E],
  1 = LinearIsometry.id
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
BitVec.reduceShiftLeftShiftLeft : Lean.Meta.Simp.Simproc
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Submonoid.unitClosedBall.congr_simp : ∀ (𝕜 : Type u_2) [inst : SeminormedRing 𝕜] [inst_1 : NormOneClass 𝕜],
  Submonoid.unitClosedBall 𝕜 = Submonoid.unitClosedBall 𝕜
-- Lean.Meta.Basic
Lean.Meta.DefEqContext.localInstances : Lean.Meta.DefEqContext → Lean.LocalInstances
-- Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
AlgebraicGeometry.instLocallyOfFinitePresentationFstScheme : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [AlgebraicGeometry.LocallyOfFinitePresentation g],
  AlgebraicGeometry.LocallyOfFinitePresentation (CategoryTheory.Limits.pullback.fst f g)
-- Mathlib.Algebra.Homology.Embedding.Extend
HomologicalComplex.extend.X.eq_2 : ∀ {ι : Type u_1} {c : ComplexShape ι} {C : Type u_3} [inst : CategoryTheory.Category.{v_1, u_3} C]
  [inst_1 : CategoryTheory.Limits.HasZeroObject C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c), HomologicalComplex.extend.X K none = 0
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getD_eq_getD : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : LawfulBEq α], m.WF → ∀ {a : α} {fallback : β}, Std.DHashMap.Raw.Const.getD m a fallback = m.getD a fallback
-- Lean.Meta.Basic
/-- Given `e` of the form `let x₁ := v₁; ...; let xₙ := vₙ; A`, executes `k xs A`,
where `xs` is an array of free variables for the binders.
The `let`s can also be `have`s.

- If `cleanupAnnotations` is `true`, applies `Expr.cleanupAnnotations` to each type in the telescope.
- If `preserveNondep` is `false`, all `have`s are converted to `let`s.
- If `nondepLetOnly` is `true`, then only `have`s are consumed (it stops at the first dependent `let`).

See also `mapLetTelescope` for entering and rebuilding the telescope.
 -/
Lean.Meta.letTelescope : {n : Type → Type u_1} →
  [MonadControlT Lean.MetaM n] →
    [Monad n] →
      {α : Type} →
        Lean.Expr →
          (Array Lean.Expr → Lean.Expr → n α) → optParam Bool false → optParam Bool true → optParam Bool false → n α
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.contains_congr : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {a b : α}, (a == b) = true → m.contains a = m.contains b
-- Mathlib.AlgebraicGeometry.Properties
AlgebraicGeometry.IsReduced.component_reduced : ∀ {X : AlgebraicGeometry.Scheme} [self : AlgebraicGeometry.IsReduced X] (U : X.Opens),
  IsReduced ↑(X.presheaf.obj (Opposite.op U))
-- Mathlib.Algebra.Lie.Quotient
LieHom.quotKerEquivRange_invFun : ∀ {R : Type u_1} {L : Type u_2} {L' : Type u_3} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : LieRing L'] [inst_4 : LieAlgebra R L'] (f : L →ₗ⁅R⁆ L') (a : ↥(↑f).range),
  f.quotKerEquivRange.invFun a = (↑f).quotKerEquivRange.invFun a
-- Mathlib.Dynamics.Ergodic.Ergodic
/-- A map `f : α → α` is said to be ergodic with respect to a measure `μ` if it is measure
preserving and pre-ergodic.  -/
Ergodic : {α : Type u_1} → {m : MeasurableSpace α} → (α → α) → autoParam (MeasureTheory.Measure α) Ergodic._auto_1 → Prop
-- Mathlib.Topology.Compactness.Compact
Filter.Tendsto.isCompact_insert_range_of_cocompact : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {y : Y},
  Filter.Tendsto f (Filter.cocompact X) (nhds y) → Continuous f → IsCompact (insert y (Set.range f))
-- Batteries.Tactic.Lint.Simp
/-- Constructs a message from all the simp theorems encoded in the given type.  -/
Batteries.Tactic.Lint.checkAllSimpTheoremInfos : Lean.Expr →
  (Batteries.Tactic.Lint.SimpTheoremInfo → Lean.MetaM (Option Lean.MessageData)) → Lean.MetaM (Option Lean.MessageData)
-- Init.Data.Range.Polymorphic.Fin
Fin.rxiHasSize_eq : ∀ {n : ℕ}, Std.Rxi.HasSize.size = fun lo => n - ↑lo