mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Grind.Interactive
/-- The `!` modifier instructs `grind` to consider only minimal indexable subexpressions
when selecting patterns.
 -/
Lean.Parser.Tactic.grindLemmaMin : Lean.ParserDescr
-- Init.System.IO
/-- Converts an `EIO ε` action that might throw an exception of type `ε` into an exception-free `IO`
action that returns an `Except` value.
 -/
EIO.toIO' : {ε α : Type} → EIO ε α → IO (Except ε α)
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanClass.mem_ballAddSubgroup_iff : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] {a : M}
  {c : ArchimedeanClass M}, c ≠ ⊤ → (a ∈ c.ballAddSubgroup ↔ c < ArchimedeanClass.mk a)
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.log2_le_logb : ∀ (n : ℕ), ↑n.log2 ≤ Real.logb 2 ↑n
-- Mathlib.NumberTheory.Zsqrtd.Basic
instDecidableEqZsqrtd.decEq : {d : ℤ} → (x x_1 : ℤ√d) → Decidable (x = x_1)
-- Mathlib.Geometry.Manifold.ContMDiff.Constructions
ContMDiff.inl : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {M' : Type u_16} [inst_6 : TopologicalSpace M']
  [inst_7 : ChartedSpace H M'] {n : WithTop ℕ∞}, ContMDiff I I n Sum.inl
-- Mathlib.Data.NNReal.Defs
NNReal.instMulArchimedean : MulArchimedean NNReal
-- Std.Data.HashMap.Lemmas
Std.HashMap.get?_emptyWithCapacity : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {a : α} {c : ℕ},
  (Std.HashMap.emptyWithCapacity c).get? a = none
-- Lean.Elab.Term.TermElabM
_private.Lean.Elab.Term.TermElabM.0.Lean.Elab.Term.isExplicitApp : Lean.Syntax → Bool
-- Lean.Elab.BuiltinNotation
Lean.Elab.Term.elabDebugAssert : Lean.Elab.Term.TermElab
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
Finpartition.sparsePairs.congr_simp : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : DecidableEq α] {A : Finset α}
  (P P_1 : Finpartition A),
  P = P_1 →
    ∀ (G G_1 : SimpleGraph α),
      G = G_1 →
        ∀ {inst_3 : DecidableRel G.Adj} [inst_4 : DecidableRel G_1.Adj] (ε ε_1 : 𝕜),
          ε = ε_1 → P.sparsePairs G ε = P_1.sparsePairs G_1 ε_1
-- Mathlib.Data.Set.Image
Function.Surjective.nonempty_preimage : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, Function.Surjective f → ∀ {s : Set β}, (f ⁻¹' s).Nonempty ↔ s.Nonempty
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Hom₂.right_unitor : {B : Type u} →
  [inst : Quiver B] →
    {a b : CategoryTheory.FreeBicategory B} →
      (f : a ⟶ b) →
        CategoryTheory.FreeBicategory.Hom₂ (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.id b)) f
-- Mathlib.CategoryTheory.Action.Monoidal
/-- A lax monoidal functor induces a lax monoidal functor between
the categories of `G`-actions within those categories.  -/
CategoryTheory.Functor.instLaxMonoidalActionMapAction : {V : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    {G : Type u_2} →
      [inst_1 : Monoid G] →
        {W : Type u_3} →
          [inst_2 : CategoryTheory.Category.{v_2, u_3} W] →
            [inst_3 : CategoryTheory.MonoidalCategory V] →
              [inst_4 : CategoryTheory.MonoidalCategory W] →
                (F : CategoryTheory.Functor V W) → [F.LaxMonoidal] → (F.mapAction G).LaxMonoidal
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.mem_support_toFun : ∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → Zero (β i)]
  [inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] (f : Π₀ (i : ι), β i) (i : ι), i ∈ f.support ↔ f i ≠ 0
-- Mathlib.Analysis.RCLike.Basic
RCLike.I_im : ∀ {K : Type u_1} [inst : RCLike K] (z : K), RCLike.im z * RCLike.im RCLike.I = RCLike.im z
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Closeds.coe_preimage : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  (s : TopologicalSpace.Closeds β) {f : α → β} (hf : Continuous f), ↑(s.preimage hf) = f ⁻¹' ↑s
-- Mathlib.Algebra.Module.LocalizedModule.Basic
/-- The natural map `Mₛ →ₗ[R] Mₜ` if `s ≤ t` (in `Submonoid R`).  -/
LocalizedModule.liftOfLE : {R : Type u_1} →
  [inst : CommSemiring R] →
    {M : Type u_2} →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] → (S₁ S₂ : Submonoid R) → S₁ ≤ S₂ → LocalizedModule S₁ M →ₗ[R] LocalizedModule S₂ M
-- Mathlib.Computability.Primrec.Basic
Primcodable.prim : ∀ (α : Type u_1) [self : Primcodable α], Nat.Primrec fun n => Encodable.encode (Encodable.decode n)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.foldM_eq_foldlM_keys : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} {δ : Type w}
  {m' : Type w → Type w'} [inst_2 : Monad m'] [LawfulMonad m'],
  m.WF → ∀ {f : δ → α → m' δ} {init : δ}, Std.DHashMap.Raw.foldM (fun d a x => f d a) init m = List.foldlM f init m.keys
-- Lean.Data.Lsp.Basic
Lean.Lsp.LocationLink.mk.injEq : ∀ (originSelectionRange? : Option Lean.Lsp.Range) (targetUri : Lean.Lsp.DocumentUri)
  (targetRange targetSelectionRange : Lean.Lsp.Range) (originSelectionRange?_1 : Option Lean.Lsp.Range)
  (targetUri_1 : Lean.Lsp.DocumentUri) (targetRange_1 targetSelectionRange_1 : Lean.Lsp.Range),
  ({ originSelectionRange? := originSelectionRange?, targetUri := targetUri, targetRange := targetRange,
        targetSelectionRange := targetSelectionRange } =
      { originSelectionRange? := originSelectionRange?_1, targetUri := targetUri_1, targetRange := targetRange_1,
        targetSelectionRange := targetSelectionRange_1 }) =
    (originSelectionRange? = originSelectionRange?_1 ∧
      targetUri = targetUri_1 ∧ targetRange = targetRange_1 ∧ targetSelectionRange = targetSelectionRange_1)
-- Mathlib.Probability.Martingale.Upcrossing
MeasureTheory.lowerCrossingTime_lt_upperCrossingTime : ∀ {Ω : Type u_1} {a b : ℝ} {f : ℕ → Ω → ℝ} {N n : ℕ} {ω : Ω},
  a < b →
    MeasureTheory.upperCrossingTime a b f N (n + 1) ω ≠ N →
      MeasureTheory.lowerCrossingTime a b f N n ω < MeasureTheory.upperCrossingTime a b f N (n + 1) ω
-- Init.Data.Vector.Lemmas
Vector.toList_eraseIdx : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i : ℕ} (h : i < n), (xs.eraseIdx i h).toList = xs.toList.eraseIdx i
-- Mathlib.Order.Category.NonemptyFinLinOrd
/-- The equivalence between `NonemptyFinLinOrd` and itself induced by `OrderDual` both ways.  -/
NonemptyFinLinOrd.dualEquiv : NonemptyFinLinOrd ≌ NonemptyFinLinOrd
-- Mathlib.Order.Types.Arithmetic
/-- The order type of the rational numbers. 

Conventions for notations in identifiers:

 * The recommended spelling of `η` in identifiers is `eta`. -/
OrderType.termη : Lean.ParserDescr
-- Aesop.Saturate
Aesop.SaturateM.instInhabitedContext.default : Aesop.SaturateM.Context
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
_private.Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono.0.SimplexCategoryGenRel.factor_δ_σ : ∀ {n : ℕ} (i : Fin (n + 1)) (i' : Fin (n + 2)),
  ∃ z e m,
    ∃ (_ : SimplexCategoryGenRel.P_σ e) (_ : SimplexCategoryGenRel.P_δ m),
      CategoryTheory.CategoryStruct.comp (SimplexCategoryGenRel.δ i') (SimplexCategoryGenRel.σ i) =
        CategoryTheory.CategoryStruct.comp e m
-- Mathlib.Topology.UniformSpace.Equicontinuity
/-- If `𝓕 : ι → β → α` tends to `f : β → α` *pointwise on `S : Set β`* along some nontrivial
filter, and if the family `𝓕` is uniformly equicontinuous on `S`, then the limit is uniformly
continuous on `S`.  -/
Filter.Tendsto.uniformContinuousOn_of_uniformEquicontinuousOn : ∀ {ι : Type u_1} {α : Type u_6} {β : Type u_8} [uα : UniformSpace α] [uβ : UniformSpace β] {l : Filter ι} [l.NeBot]
  {F : ι → β → α} {f : β → α} {S : Set β},
  (∀ x ∈ S, Filter.Tendsto (fun x_1 => F x_1 x) l (nhds (f x))) → UniformEquicontinuousOn F S → UniformContinuousOn f S
-- Mathlib.Analysis.RCLike.Basic
RCLike.normSq_to_real : ∀ {x : ℝ}, RCLike.normSq x = x * x
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.coproductUniqueIso_inv : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : Unique β] (f : β → C),
  (CategoryTheory.Limits.coproductUniqueIso f).inv = CategoryTheory.Limits.Sigma.ι f default
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.vadd_set_pi_of_isAddUnit : ∀ {M : Type u_5} {ι : Type u_6} {α : ι → Type u_7} [inst : AddMonoid M] [inst_1 : (i : ι) → AddAction M (α i)] {c : M},
  IsAddUnit c → ∀ (I : Set ι) (s : (i : ι) → Set (α i)), c +ᵥ I.pi s = I.pi (c +ᵥ s)
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2to1.tr_respects_aux₁ : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} [inst : DecidableEq K] (M : Λ → Turing.TM2.Stmt Γ Λ σ)
  {k : K} (o : Turing.TM2to1.StAct K Γ σ k) (q : Turing.TM2.Stmt Γ Λ σ) (v : σ) {S : List (Γ k)}
  {L : Turing.ListBlank ((k : K) → Option (Γ k))},
  Turing.ListBlank.map (Turing.proj k) L = Turing.ListBlank.mk (List.map some S).reverse →
    ∀ n ≤ S.length,
      StateTransition.Reaches₀ (Turing.TM1.step (Turing.TM2to1.tr M))
        { l := some (Turing.TM2to1.Λ'.go k o q), var := v, Tape := Turing.Tape.mk' ∅ (Turing.TM2to1.addBottom L) }
        { l := some (Turing.TM2to1.Λ'.go k o q), var := v,
          Tape := (Turing.Tape.move Turing.Dir.right)^[n] (Turing.Tape.mk' ∅ (Turing.TM2to1.addBottom L)) }
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
SSet.Truncated.HomotopyCategory.ext : ∀ {V : SSet.Truncated 2} {x y : V.HomotopyCategory}, x.as.as = y.as.as → x = y
-- Mathlib.Algebra.Polynomial.UnitTrinomial
Polynomial.IsUnitTrinomial.not_isUnit : ∀ {p : Polynomial ℤ}, p.IsUnitTrinomial → ¬IsUnit p
-- Std.Http.Server.Config
/-- Maximum length of chunk extension name (default: 256 bytes)
 -/
Std.Http.Config.maxChunkExtNameLength : Std.Http.Config → ℕ
-- Mathlib.Topology.MetricSpace.Infsep
Set.infsep_nonneg : ∀ {α : Type u_1} [inst : EDist α] {s : Set α}, 0 ≤ s.infsep
-- Mathlib.CategoryTheory.Monad.Limits
/-- If `C` has colimits then any reflective subcategory has colimits.  -/
CategoryTheory.hasColimits_of_reflective : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (R : CategoryTheory.Functor D C) [CategoryTheory.Reflective R]
  [CategoryTheory.Limits.HasColimitsOfSize.{v, u, v₁, u₁} C], CategoryTheory.Limits.HasColimitsOfSize.{v, u, v₂, u₂} D
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getD_diff_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α} {fallback : β k}, k ∉ t₁ → (t₁ \ t₂).getD k fallback = fallback
-- Mathlib.CategoryTheory.Sites.GlobalSections
/-- The natural transformation from the global sections functor to the sections functor on any
object `U`.  -/
CategoryTheory.Sheaf.natTransΓRes : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      (A : Type u₂) →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} A] →
          [inst_2 : CategoryTheory.HasWeakSheafify J A] →
            [inst_3 : CategoryTheory.HasGlobalSectionsFunctor J A] →
              (U : Cᵒᵖ) → CategoryTheory.Sheaf.Γ J A ⟶ (CategoryTheory.sheafSections J A).obj U
-- Mathlib.Data.Part
/-- `assert p f` is a bind-like operation which appends an additional condition
`p` to the domain and uses `f` to produce the value.  -/
Part.assert : {α : Type u_1} → (p : Prop) → (p → Part α) → Part α
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Functor.mapCoconeMorphism.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] (H : CategoryTheory.Functor C D)
  {F : CategoryTheory.Functor J C} {c c' : CategoryTheory.Limits.Cocone F} (f : c' ⟶ c),
  H.mapCoconeMorphism f = (CategoryTheory.Limits.Cocone.functoriality F H).map f
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Impl.Const.alter.match_3.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (motive : (t : Std.DTreeMap.Internal.Impl α fun x => β) → t.Balanced → Sort u_3)
  (sz : ℕ) (k' : α) (v' : β) (l' r' : Std.DTreeMap.Internal.Impl α fun x => β)
  (hl : (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r').Balanced)
  (h_1 : (hl : Std.DTreeMap.Internal.Impl.leaf.Balanced) → motive Std.DTreeMap.Internal.Impl.leaf hl)
  (h_2 :
    (sz : ℕ) →
      (k' : α) →
        (v' : β) →
          (l' r' : Std.DTreeMap.Internal.Impl α fun x => β) →
            (hl : (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r').Balanced) →
              motive (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r') hl),
  (match Std.DTreeMap.Internal.Impl.inner sz k' v' l' r', hl with
    | Std.DTreeMap.Internal.Impl.leaf, hl => h_1 hl
    | Std.DTreeMap.Internal.Impl.inner sz k' v' l' r', hl => h_2 sz k' v' l' r' hl) =
    h_2 sz k' v' l' r' hl
-- Mathlib.Analysis.BoxIntegral.Partition.Tagged
BoxIntegral.Prepartition.IsPartition.biUnionTagged : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} {π : BoxIntegral.Prepartition I},
  π.IsPartition →
    ∀ {πi : (J : BoxIntegral.Box ι) → BoxIntegral.TaggedPrepartition J},
      (∀ J ∈ π, (πi J).IsPartition) → (π.biUnionTagged πi).IsPartition
-- Mathlib.CategoryTheory.Limits.IndYoneda
CategoryTheory.Limits.colimitYonedaHomIsoLimitOp_π_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] {I : Type v₁} [inst_1 : CategoryTheory.Category.{v₂, v₁} I]
  (D : CategoryTheory.Functor I C) (F : CategoryTheory.Functor Cᵒᵖ (Type u₂))
  [inst_2 : CategoryTheory.Limits.HasColimit (D.comp CategoryTheory.yoneda)]
  [inst_3 : CategoryTheory.Limits.HasLimitsOfShape Iᵒᵖ (Type (max u₁ u₂))]
  (f : CategoryTheory.Limits.colimit (D.comp CategoryTheory.yoneda) ⟶ F) (i : Iᵒᵖ),
  (CategoryTheory.ConcreteCategory.hom
        (CategoryTheory.Limits.limit.π (D.op.comp (F.comp CategoryTheory.uliftFunctor.{u₁, u₂})) i))
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimitYonedaHomIsoLimitOp D F).hom) f) =
    {
      down :=
        (CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op (D.obj (Opposite.unop i)))))
          ((CategoryTheory.ConcreteCategory.hom
              ((CategoryTheory.Limits.colimit.ι (D.comp CategoryTheory.yoneda) (Opposite.unop i)).app
                (Opposite.op (D.obj (Opposite.unop i)))))
            (CategoryTheory.CategoryStruct.id (D.obj (Opposite.unop i)))) }
-- Mathlib.CategoryTheory.Limits.WeakLimits.WeakKernels
/-- A morphism `f` has a weak kernel if the functor `ParallelPair f 0` has a weak limit.  -/
CategoryTheory.Limits.HasWeakKernel : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [CategoryTheory.Limits.HasZeroMorphisms C] → {X Y : C} → (X ⟶ Y) → Prop
-- Mathlib.Algebra.Group.Submonoid.Operations
MonoidHom.mker_inl : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N], MonoidHom.mker (MonoidHom.inl M N) = ⊥
-- Lean.Environment
/-- The module data that should be used for accessing IR for interpretation (lean) or compilation
(leanir; loadIRSig = true).  -/
_private.Lean.Environment.0.Lean.ImportedModule.irData? : Lean.ImportedModule✝ → optParam Bool false → Option Lean.ModuleData
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.leftUnitor_inv_comp_tensorHom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y Z : C}
  (f : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ Y) (g : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv
      (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) =
    CategoryTheory.CategoryStruct.comp g
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor Z).inv
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z))
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Sigma.map_epi : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f g : β → C}
  [inst_1 : CategoryTheory.Limits.HasCoproduct f] [inst_2 : CategoryTheory.Limits.HasCoproduct g]
  (p : (b : β) → f b ⟶ g b) [∀ (i : β), CategoryTheory.Epi (p i)],
  CategoryTheory.Epi (CategoryTheory.Limits.Sigma.map p)
-- Mathlib.LinearAlgebra.Matrix.ZPow
Matrix.zpow_mul : ∀ {n' : Type u_1} [inst : DecidableEq n'] [inst_1 : Fintype n'] {R : Type u_2} [inst_2 : CommRing R]
  (A : Matrix n' n' R), IsUnit A.det → ∀ (m n : ℤ), A ^ (m * n) = (A ^ m) ^ n
-- Mathlib.CategoryTheory.Monoidal.Ring
CategoryTheory.CommRingObjCat.forget_map : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {X Y : CategoryTheory.CommRingObjCat C} (f : X ⟶ Y),
  (CategoryTheory.CommRingObjCat.forget C).map f = f.hom
-- Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
/-- `spinGroup Q` is defined as the infimum of `pinGroup Q` and `CliffordAlgebra.even Q`.
See `mem_iff`.  -/
spinGroup : {R : Type u_1} →
  [inst : CommRing R] →
    {M : Type u_2} →
      [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → (Q : QuadraticForm R M) → Submonoid (CliffordAlgebra Q)
-- Init.Data.Fin.Lemmas
Fin.reverseInduction_last : ∀ {n : ℕ} {motive : Fin (n + 1) → Sort u_1} {zero : motive (Fin.last n)}
  {succ : (i : Fin n) → motive i.succ → motive i.castSucc}, Fin.reverseInduction zero succ (Fin.last n) = zero
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  {k : α} (h' : k ∈ t), t.get k h' = k
-- Mathlib.Order.Filter.ENNReal
ENNReal.limsup_mul_const : ∀ {α : Type u_1} {f : Filter α} [CountableInterFilter f] {u : α → ENNReal} {a : ENNReal},
  Filter.limsup (fun x => u x * a) f = a * Filter.limsup u f
-- Mathlib.LinearAlgebra.DFinsupp
DFinsupp.mapRange.linearMap_comp : ∀ {ι : Type u_1} {R : Type u_3} [inst : Semiring R] {β : ι → Type u_7} {β₁ : ι → Type u_8} {β₂ : ι → Type u_9}
  [inst_1 : (i : ι) → AddCommMonoid (β i)] [inst_2 : (i : ι) → AddCommMonoid (β₁ i)]
  [inst_3 : (i : ι) → AddCommMonoid (β₂ i)] [inst_4 : (i : ι) → Module R (β i)] [inst_5 : (i : ι) → Module R (β₁ i)]
  [inst_6 : (i : ι) → Module R (β₂ i)] (f : (i : ι) → β₁ i →ₗ[R] β₂ i) (f₂ : (i : ι) → β i →ₗ[R] β₁ i),
  (DFinsupp.mapRange.linearMap fun i => f i ∘ₗ f₂ i) = DFinsupp.mapRange.linearMap f ∘ₗ DFinsupp.mapRange.linearMap f₂
-- Mathlib.SetTheory.Lists
_private.Mathlib.SetTheory.Lists.0.Lists.Subset.decidable.match_1.eq_1 : ∀ {α : Type u_1} (motive : Lists' α true → Lists' α true → Sort u_2) (x : Lists' α true)
  (h_1 : (x : Lists' α true) → motive Lists'.nil x)
  (h_2 : (b : Bool) → (a : Lists' α b) → (l₁ l₂ : Lists' α true) → motive (a.cons' l₁) l₂),
  (match Lists'.nil, x with
    | Lists'.nil, x => h_1 x
    | a.cons' l₁, l₂ => h_2 b a l₁ l₂) =
    h_1 x
-- Lean.Data.Lsp.Workspace
Lean.Lsp.FileEvent.mk.inj : ∀ {uri : Lean.Lsp.DocumentUri} {type : Lean.Lsp.FileChangeType} {uri_1 : Lean.Lsp.DocumentUri}
  {type_1 : Lean.Lsp.FileChangeType},
  { uri := uri, type := type } = { uri := uri_1, type := type_1 } → uri = uri_1 ∧ type = type_1
-- Mathlib.Topology.EMetricSpace.BoundedVariation
LipschitzOnWith.comp_eVariationOn_le : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] {F : Type u_3}
  [inst_2 : PseudoEMetricSpace F] {f : E → F} {C : NNReal} {t : Set E},
  LipschitzOnWith C f t → ∀ {g : α → E} {s : Set α}, Set.MapsTo g s t → eVariationOn (f ∘ g) s ≤ ↑C * eVariationOn g s
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupNorm.coe_sup : ∀ {E : Type u_3} [inst : Group E] (p q : GroupNorm E), ⇑(p ⊔ q) = ⇑p ⊔ ⇑q
-- Lean.PrettyPrinter.Delaborator.Options
Lean.getPPDeepTerms : Lean.Options → Bool
-- Mathlib.Algebra.Star.StarAlgHom
NonUnitalStarAlgHom.coe_mk' : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : Monoid R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : DistribMulAction R A] [inst_3 : Star A] [inst_4 : NonUnitalNonAssocSemiring B]
  [inst_5 : DistribMulAction R B] [inst_6 : Star B] (f : A →ₙₐ[R] B)
  (h : ∀ (a : A), f.toFun (star a) = star (f.toFun a)), ⇑{ toNonUnitalAlgHom := f, map_star' := h } = ⇑f
-- Init.Data.Order.Lemmas
Std.lt_trans : ∀ {α : Type u} [inst : LT α] [Trans (fun x1 x2 => x1 < x2) (fun x1 x2 => x1 < x2) fun x1 x2 => x1 < x2] {a b c : α},
  a < b → b < c → a < c
-- Std.Tactic.BVDecide.LRAT.Internal.LRATChecker
Std.Tactic.BVDecide.LRAT.Internal.instInhabitedResult.default : Std.Tactic.BVDecide.LRAT.Internal.Result
-- Init.WFExtrinsicFix
_private.Init.WFExtrinsicFix.0.WellFounded.partialExtrinsicFix.eq_1 : ∀ {α : Sort u_1} {C : α → Sort u_2} [inst : ∀ (a : α), Nonempty (C a)] (R : α → α → Prop)
  (F : (a : α) → ((a' : α) → R a' a → C a') → C a) (a : α),
  WellFounded.partialExtrinsicFix R F a =
    WellFounded.extrinsicFix (fun p q => R ↑p ↑q) (fun a_1 recur => F ↑a_1 fun a' hR => recur ⟨a', ⋯⟩ hR) ⟨a, ⋯⟩
-- Mathlib.RingTheory.Teichmuller
Perfection.exists_teichmullerFun : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : CommRing R] {I : Ideal R} [inst_2 : CharP (R ⧸ I) p]
  [IsPrecomplete I R] (x : Perfection (R ⧸ I) p), ∃ y, ∀ (n : ℕ), x.teichmullerAux n ≡ y [SMOD I ^ n • ⊤]
-- Mathlib.Algebra.Order.GroupWithZero.Defs
mulPosReflectLT_iff : ∀ (α : Type u_1) [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α],
  MulPosReflectLT α ↔ ContravariantClass { x // 0 ≤ x } α (fun x y => y * ↑x) fun x1 x2 => x1 < x2
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
AddMonoidAlgebra.mapDomainBialgHom_id : ∀ {R : Type u_1} {M : Type u_8} [inst : CommSemiring R] [inst_1 : AddMonoid M],
  AddMonoidAlgebra.mapDomainBialgHom R (AddMonoidHom.id M) = BialgHom.id R (AddMonoidAlgebra R M)
-- Mathlib.Data.Finset.Basic
Finset.filter_erase : ∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] [inst_1 : DecidableEq α] (a : α) (s : Finset α),
  Finset.filter p (s.erase a) = (Finset.filter p s).erase a
-- Mathlib.Logic.Equiv.Set
/-- **Alias** of `Equiv.strictMono_setCongr`. -/
Equiv.Set.Equiv.strictMono_setCongr : ∀ {α : Type u_3} [inst : Preorder α] {S T : Set α} (h : S = T), StrictMono ⇑(Equiv.setCongr h)
-- Aesop.Util.OrderedHashSet
Aesop.OrderedHashSet.foldrM : {α : Type u_1} →
  [inst : BEq α] →
    [inst_1 : Hashable α] →
      {m : Type u_2 → Type u_3} → {β : Type u_2} → [Monad m] → (α → β → m β) → β → Aesop.OrderedHashSet α → m β
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
IsPrimitiveRoot.zmodEquivZPowers_apply_coe_int : ∀ {R : Type u_4} {k : ℕ} [inst : CommRing R] {ζ : Rˣ} (h : IsPrimitiveRoot ζ k) (i : ℤ),
  h.zmodEquivZPowers ↑i = Additive.ofMul ⟨ζ ^ i, ⋯⟩
-- Lean.MetavarContext
Lean.instMonadMCtxStateRefT'MetavarContextST : {ω : Type} → Lean.MonadMCtx (StateRefT' ω Lean.MetavarContext (ST ω))
-- Mathlib.Order.Hom.BoundedLattice
BoundedLatticeHom.coe_comp_inf_hom' : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Lattice α] [inst_1 : Lattice β] [inst_2 : Lattice γ]
  [inst_3 : BoundedOrder α] [inst_4 : BoundedOrder β] [inst_5 : BoundedOrder γ] (f : BoundedLatticeHom β γ)
  (g : BoundedLatticeHom α β),
  { toFun := ⇑f ∘ ⇑g, map_inf' := ⋯ } = { toFun := ⇑f, map_inf' := ⋯ }.comp { toFun := ⇑g, map_inf' := ⋯ }