mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
/-- Transfer preservation of a limit along a natural isomorphism in the functor.  -/
CategoryTheory.Limits.preservesLimit_of_natIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] (K : CategoryTheory.Functor J C)
  {F G : CategoryTheory.Functor C D} (h : F ≅ G) [CategoryTheory.Limits.PreservesLimit K F],
  CategoryTheory.Limits.PreservesLimit K G
-- Mathlib.CategoryTheory.Localization.Bousfield
CategoryTheory.ObjectProperty.le_isColocal_isColocal : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C),
  P ≤ P.isColocal.isColocal
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
CategoryTheory.Limits.limit.lift_π_app_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} J]
  {K : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} K]
  (H : CategoryTheory.Functor J (CategoryTheory.Functor K C)) [inst_3 : CategoryTheory.Limits.HasLimit H]
  (c : CategoryTheory.Limits.Cone H) (j : J) (k : K) {Z : C} (h : (H.obj j).obj k ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.limit.lift H c).app k)
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.limit.π H j).app k) h) =
    CategoryTheory.CategoryStruct.comp ((c.π.app j).app k) h
-- Mathlib.Algebra.LieRinehartAlgebra.Defs
instLieRinehartRingDerivation : ∀ {R : Type u_1} {A₁ : Type u_2} [inst : CommRing R] [inst_1 : CommRing A₁] [inst_2 : Algebra R A₁],
  LieRinehartRing A₁ (Derivation R A₁ A₁)
-- Mathlib.Algebra.Group.Equiv.Defs
AddEquiv.apply_eq_iff_symm_apply : ∀ {M : Type u_4} {N : Type u_5} [inst : Add M] [inst_1 : Add N] (e : M ≃+ N) {x : M} {y : N}, e x = y ↔ x = e.symm y
-- Mathlib.Data.Part
Part.none_toOption : ∀ {α : Type u_1} [inst : Decidable Part.none.Dom], Part.none.toOption = none
-- Init.Data.Fin.Lemmas
Fin.mul_zero : ∀ {n : ℕ} [inst : NeZero n] (k : Fin n), k * 0 = 0
-- Mathlib.Topology.LocallyFinsupp
/-- Assign a function with locally finite support within `U` to a function in the subgroup.
 -/
Function.locallyFinsuppWithin.mk_of_mem_addSubgroup : {X : Type u_1} →
  [inst : TopologicalSpace X] →
    {U : Set X} →
      {Y : Type u_2} →
        [inst_1 : AddGroup Y] →
          (f : X → Y) → f ∈ Function.locallyFinsuppWithin.addSubgroup U → Function.locallyFinsuppWithin U Y
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonSemanticTokenType.fromJson : Lean.Json → Except String Lean.Lsp.SemanticTokenType
-- Mathlib.Data.PFun
PFun.fn_apply : ∀ {α : Type u_1} {β : Type u_2} (f : α →. β) (a : α), f.fn a = (f a).get
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
eventually_forall_conj_nhds_one : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : Group α] [IsUniformGroup α] {p : α → Prop},
  (∀ᶠ (x : α) in nhds 1, p x) → ∀ᶠ (x : α) in nhds 1, ∀ (g : α), p (g * x * g⁻¹)
-- Mathlib.Topology.Order.MonotoneContinuity
/-- A monotone function with densely ordered codomain and a dense range is continuous.  -/
Monotone.continuous_of_denseRange : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  [inst_3 : LinearOrder β] [inst_4 : TopologicalSpace β] [OrderTopology β] [DenselyOrdered β] {f : α → β},
  Monotone f → DenseRange f → Continuous f
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
mul_le_mul_of_nonpos_of_nonpos : ∀ {R : Type u} [inst : Semiring R] [inst_1 : Preorder R] {a b c d : R} [ExistsAddOfLE R] [MulPosMono R] [PosMulMono R]
  [AddRightMono R] [AddRightReflectLE R], c ≤ a → d ≤ b → c ≤ 0 → b ≤ 0 → a * b ≤ c * d
-- Mathlib.LinearAlgebra.AffineSpace.Independent
AffineIndependent.indicator_eq_of_affineCombination_eq : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {ι : Type u_4} {p : ι → P},
  AffineIndependent k p →
    ∀ (s₁ s₂ : Finset ι) (w₁ w₂ : ι → k),
      ∑ i ∈ s₁, w₁ i = 1 →
        ∑ i ∈ s₂, w₂ i = 1 →
          (Finset.affineCombination k s₁ p) w₁ = (Finset.affineCombination k s₂ p) w₂ →
            (↑s₁).indicator w₁ = (↑s₂).indicator w₂
-- Init.Core
not_not_intro : ∀ {p : Prop}, p → ¬¬p
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransform.comp_whiskerLeft : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} {A'' : Type u₇} {B'' : Type u₈}
  {C'' : Type u₉} [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  [inst_6 : CategoryTheory.Category.{v₇, u₇} A''] [inst_7 : CategoryTheory.Category.{v₈, u₈} B'']
  [inst_8 : CategoryTheory.Category.{v₉, u₉} C''] {F'' : CategoryTheory.Functor A'' B''}
  {G'' : CategoryTheory.Functor C'' B''} {A''' : Type u₁₀} {B''' : Type u₁₁} {C''' : Type u₁₂}
  [inst_9 : CategoryTheory.Category.{v₁₀, u₁₀} A'''] [inst_10 : CategoryTheory.Category.{v₁₁, u₁₁} B''']
  [inst_11 : CategoryTheory.Category.{v₁₂, u₁₂} C'''] {F''' : CategoryTheory.Functor A''' B'''}
  {G''' : CategoryTheory.Functor C''' B'''} {ψ : CategoryTheory.Limits.CatCospanTransform F G F' G'}
  {φ : CategoryTheory.Limits.CatCospanTransform F' G' F'' G''}
  {τ τ' : CategoryTheory.Limits.CatCospanTransform F'' G'' F''' G'''} (γ : τ ⟶ τ'),
  CategoryTheory.Limits.CatCospanTransformMorphism.whiskerLeft (ψ.comp φ) γ =
    CategoryTheory.CategoryStruct.comp (ψ.associator φ τ).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerLeft ψ
          (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerLeft φ γ))
        (ψ.associator φ τ').inv)
-- Init.Data.Float.Model.Unpacked.Pack.Lemmas
_private.Init.Data.Float.Model.Unpacked.Pack.Lemmas.0.Float.Model.UnpackedFloat.pack.match_1.eq_4 : ∀ (motive : Float.Model.UnpackedFloat → Sort u_1) (s : Float.Model.UnpackedFloat.Sign) (m : ℕ) (e : ℤ)
  (mantissa_pos : 0 < m) (h_1 : Unit → motive Float.Model.UnpackedFloat.notANumber)
  (h_2 : (s : Float.Model.UnpackedFloat.Sign) → motive (Float.Model.UnpackedFloat.infinity s))
  (h_3 : (s : Float.Model.UnpackedFloat.Sign) → motive (Float.Model.UnpackedFloat.zero s))
  (h_4 :
    (s : Float.Model.UnpackedFloat.Sign) →
      (m : ℕ) → (e : ℤ) → (mantissa_pos : 0 < m) → motive (Float.Model.UnpackedFloat.finite s m e mantissa_pos)),
  (match Float.Model.UnpackedFloat.finite s m e mantissa_pos with
    | Float.Model.UnpackedFloat.notANumber => h_1 ()
    | Float.Model.UnpackedFloat.infinity s => h_2 s
    | Float.Model.UnpackedFloat.zero s => h_3 s
    | Float.Model.UnpackedFloat.finite s m e mantissa_pos => h_4 s m e mantissa_pos) =
    h_4 s m e mantissa_pos
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.instSDiff : SDiff ZFSet.{u_1}
-- Mathlib.CategoryTheory.Bicategory.Functor.Prelax
CategoryTheory.PrelaxFunctor.mkOfHomFunctors_mapFunctor : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C] (F : B → C)
  (F' : (a b : B) → CategoryTheory.Functor (a ⟶ b) (F a ⟶ F b)) (a b : B),
  (CategoryTheory.PrelaxFunctor.mkOfHomFunctors F F').mapFunctor a b = F' a b
-- Std.Http.Data.Status
Std.Http.Status.multiStatus.sizeOf_spec : sizeOf Std.Http.Status.multiStatus = 1
-- Mathlib.Topology.UniformSpace.Defs
mem_nhds_uniformity_iff_right : ∀ {α : Type ua} [inst : UniformSpace α] {x : α} {s : Set α}, s ∈ nhds x ↔ {p | p.1 = x → p.2 ∈ s} ∈ uniformity α
-- Std.Http.Data.URI.Basic
/-- Partially normalizes a URI by removing dot-segments from the path (`.` and `..`)
according to RFC 3986 Section 5.2.4.

This does not apply the full normalization set from RFC 3986 Section 6 — for example,
case normalization, percent-encoding normalization, and default-port normalization are
not performed.
 -/
Std.Http.URI.normalize : Std.Http.URI → Std.Http.URI
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
AbsoluteValue.map_zero : ∀ {R : Type u_5} {S : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : PartialOrder S]
  (abv : AbsoluteValue R S), abv 0 = 0
-- Mathlib.Data.Finset.Union
Finset.sUnion_disjiUnion : ∀ {α : Type u_1} {β : Type u_2} {f : α → Finset (Set β)} (I : Finset α) (hf : (↑I).PairwiseDisjoint f),
  ⋃₀ ↑(I.disjiUnion f hf) = ⋃ a ∈ I, ⋃₀ ↑(f a)
-- Mathlib.Geometry.Manifold.Instances.Icc
instOneTangentSpaceRealEuclideanSpaceFinOfNatNatEuclideanHalfSpaceModelWithCornersEuclideanHalfSpaceElemIcc : {x y : ℝ} → [h : Fact (x < y)] → (z : ↑(Set.Icc x y)) → One (TangentSpace (modelWithCornersEuclideanHalfSpace 1) z)
-- Mathlib.Algebra.Field.Defs
DivisionSemiring.toNNRatCast : {K : Type u_2} → [self : DivisionSemiring K] → NNRatCast K
-- Mathlib.GroupTheory.MonoidLocalization.GrothendieckGroup
Algebra.GrothendieckGroup.lift_symm_apply : ∀ {M : Type u_1} {G : Type u_2} [inst : CommMonoid M] [inst_1 : CommGroup G] (f : Algebra.GrothendieckGroup M →* G),
  Algebra.GrothendieckGroup.lift.symm f = f.comp Algebra.GrothendieckGroup.of
-- Aesop.RuleTac.Forward
Aesop.RuleTac.forwardTerm : Lean.Term → Aesop.UnorderedArraySet Aesop.PremiseIndex → Bool → Aesop.RuleTac
-- Init.Data.Order.Opposite
Std.OppositeOrderInstances.instLESymmOpposite : ∀ {α : Type u_1} {i : LE α} [Std.Symm fun x1 x2 => x1 ≤ x2], Std.Symm fun x1 x2 => x1 ≤ x2
-- Mathlib.Order.Category.Preord
/-- Turn a morphism in `Preord` back into a `OrderHom`.  -/
Preord.Hom.hom : {X Y : Preord} → X.Hom Y → ↑X →o ↑Y
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.symm_apply_eq : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁}
  [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [inst_4 : TopologicalSpace M₁]
  [inst_5 : AddCommMonoid M₁] {M₂ : Type u_5} [inst_6 : TopologicalSpace M₂] [inst_7 : AddCommMonoid M₂]
  [inst_8 : Module R₁ M₁] [inst_9 : Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) {x : M₂} {y : M₁}, e.symm x = y ↔ x = e y
-- Mathlib.Tactic.Algebra.Lemmas
Mathlib.Tactic.Algebra.add_eq_of_add_zero : ∀ {A : Type u_2} [sA : CommSemiring A] {a₁ a₂ b₁ b₂ : A}, b₁ = 0 → a₁ + a₂ = b₂ → a₁ + a₂ = b₁ + b₂
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.Mod.Hom.ext : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} {D : Type u₂}
  {inst_2 : CategoryTheory.Category.{v₂, u₂} D} {inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D}
  {A : C} {inst_4 : CategoryTheory.MonObj A} {M N : CategoryTheory.Mod D A} {x y : M.Hom N}, x.hom = y.hom → x = y
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.fg_iSup : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {ι : Sort u_3} [Finite ι]
  {S : ι → IntermediateField F E}, (∀ (i : ι), (S i).FG) → (⨆ i, S i).FG
-- Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Multiset.sum_add : ∀ {M : Type u_5} [inst : AddCommMonoid M] (s t : Multiset M), (s + t).sum = s.sum + t.sum
-- Mathlib.CategoryTheory.Idempotents.FunctorCategories
/-- Tautological action on maps of the functor `Karoubi (J ⥤ C) ⥤ (J ⥤ Karoubi C)`.  -/
CategoryTheory.Idempotents.KaroubiFunctorCategoryEmbedding.map : {J : Type u_1} →
  {C : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} J] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} C] →
        {P Q : CategoryTheory.Idempotents.Karoubi (CategoryTheory.Functor J C)} →
          (P ⟶ Q) →
            (CategoryTheory.Idempotents.KaroubiFunctorCategoryEmbedding.obj P ⟶
              CategoryTheory.Idempotents.KaroubiFunctorCategoryEmbedding.obj Q)
-- Std.Sat.AIG.Basic
Std.Sat.AIG.toGraphviz.toGraphvizString : {α : Type} →
  [DecidableEq α] → [ToString α] → [Hashable α] → (decls : Array (Std.Sat.AIG.Decl α)) → Fin decls.size → String
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- The expression for an atomic non-structural 2-morphism.  -/
Mathlib.Tactic.BicategoryLike.Mor₂.of : Mathlib.Tactic.BicategoryLike.Atom → Mathlib.Tactic.BicategoryLike.Mor₂
-- Mathlib.Combinatorics.Enumerative.Schroder
Nat.even_largeSchroder : ∀ {n : ℕ}, n ≠ 0 → Even n.largeSchroder
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.L1.SimpleFunc.setToL1S_smul_real : ∀ {α : 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 : Set α → E →L[ℝ] F),
  (∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0) →
    MeasureTheory.FinMeasAdditive μ T →
      ∀ (c : ℝ) (f : ↥(α →₁ₛ[μ] E)),
        MeasureTheory.L1.SimpleFunc.setToL1S T (c • f) = c • MeasureTheory.L1.SimpleFunc.setToL1S T f
-- Mathlib.Topology.Algebra.Ring.Basic
Pi.instIsTopologicalRing : ∀ {ι : Type u_2} {R : ι → Type u_3} [inst : (i : ι) → TopologicalSpace (R i)]
  [inst_1 : (i : ι) → NonUnitalNonAssocRing (R i)] [∀ (i : ι), IsTopologicalRing (R i)],
  IsTopologicalRing ((i : ι) → R i)
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion
ProfiniteAddGrp.ProfiniteCompletion.etaFn.eq_1 : ∀ (G : AddGrpCat) (x : ↑G), ProfiniteAddGrp.ProfiniteCompletion.etaFn G x = ⟨fun x_1 => ↑x, ⋯⟩
-- Mathlib.NumberTheory.LSeries.Basic
/-- If `f = O(n^(x-1))` and `re s > x`, then the `LSeries` of `f` is summable at `s`.  -/
LSeriesSummable_of_isBigO_rpow : ∀ {f : ℕ → ℂ} {x : ℝ} {s : ℂ}, x < s.re → (f =O[Filter.atTop] fun n => ↑n ^ (x - 1)) → LSeriesSummable f s
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.dblXYZ.eq_1 : ∀ {R : Type r} [inst : CommRing R] (W' : WeierstrassCurve.Projective R) (P : Fin 3 → R),
  W'.dblXYZ P = ![W'.dblX P, W'.dblY P, W'.dblZ P]
-- Mathlib.SetTheory.Lists
Lists.Subset.decidable : {α : Type u_1} → [DecidableEq α] → (l₁ l₂ : Lists' α true) → Decidable (l₁ ⊆ l₂)
-- Mathlib.CategoryTheory.Enriched.Basic
CategoryTheory.enrichedNatTransYoneda_obj : ∀ {V : Type v} [inst : CategoryTheory.Category.{w, v} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u₁}
  [inst_2 : CategoryTheory.EnrichedCategory V C] {D : Type u₂} [inst_3 : CategoryTheory.EnrichedCategory V D]
  [inst_4 : CategoryTheory.BraidedCategory V] (F G : CategoryTheory.EnrichedFunctor V C D) (A : Vᵒᵖ),
  (CategoryTheory.enrichedNatTransYoneda F G).obj A =
    CategoryTheory.GradedNatTrans ((CategoryTheory.Center.ofBraided V).obj (Opposite.unop A)) F G
-- Std.Http.Data.Response
/-- Creates a new HTTP Response builder with default head (status: 200 OK, version: HTTP/1.1).
 -/
Std.Http.Response.new : Std.Http.Response.Builder
-- Init.System.IO
/-- Converts `s` to a string using its `ToString α` instance, and prints it to the current standard
output (as determined by `IO.getStdout`).
 -/
IO.print : {α : Type u_1} → [ToString α] → α → IO Unit
-- Mathlib.Analysis.Normed.Lp.ProdLp
/-- This definition allows to endow `α × β` with the Lp norm with the uniformity and bornology
being defeq to the product ones. It is useful to endow a type synonym of `α × β` with the
Lp norm.  -/
WithLp.normedAddCommGroupToProd : (p : ENNReal) →
  [hp : Fact (1 ≤ p)] →
    (α : Type u_4) → (β : Type u_5) → [NormedAddCommGroup α] → [NormedAddCommGroup β] → NormedAddCommGroup (α × β)
-- Lean.Compiler.LCNF.Types
/-- Convert a Lean type into a LCNF type used by the code generator.
 -/
Lean.Compiler.LCNF.toLCNFType : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.CategoryTheory.Limits.ExactFunctor
CategoryTheory.RightExactFunctor.whiskeringLeft_map_app : ∀ (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] {F G : C ⥤ᵣ D} (η : F ⟶ G) (H : D ⥤ᵣ E),
  ((CategoryTheory.RightExactFunctor.whiskeringLeft C D E).map η).app H =
    CategoryTheory.ObjectProperty.homMk (((CategoryTheory.Functor.whiskeringLeft C D E).map η.hom).app H.obj)
-- Mathlib.Topology.CWComplex.Classical.Subcomplex
Topology.RelCWComplex.Subcomplex.closedCell_eq : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : T2Space X] [inst_1 : Topology.RelCWComplex C D]
  (E : Topology.RelCWComplex.Subcomplex C) (n : ℕ) (i : ↑(E.I n)),
  Topology.RelCWComplex.closedCell n i = Topology.RelCWComplex.closedCell n ↑i
-- Mathlib.Tactic.Linter.FlexibleLinter
/-- `Stained.toFMVarId mv lctx st` takes a metavariable `mv`, a local context `lctx` and
a `Stained` `st` and returns the array of pairs `(FVarId, mv)`s that `lctx` assigns to `st`
(the second component is always `mv`):
* if `st` "is" a `Name`, returns the singleton of the `FVarId` with the name carried by `st`;
* if `st` is `.goal`, returns the singleton `#[default]`;
* if `st` is `.wildcard`, returns the array of all the `FVarId`s in `lctx` with also `default`
  (to keep track of the `goal`).
 -/
_private.Mathlib.Tactic.Linter.FlexibleLinter.0.Mathlib.Linter.Flexible.Stained.toFMVarId : Lean.MVarId → Lean.LocalContext → Mathlib.Linter.Flexible.Stained✝ → Array (Lean.FVarId × Lean.MVarId)
-- Mathlib.NumberTheory.Padics.Hensel
_private.Mathlib.NumberTheory.Padics.Hensel.0.T_pow' : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : CommSemiring R] [inst_2 : Algebra R ℤ_[p]]
  {F : Polynomial R} {a : ℤ_[p]},
  ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2 → ∀ (n : ℕ), T_gen✝ p F a ^ 2 ^ n < 1
-- Lean.Elab.MutualInductive
/-- The declaration docstring.  -/
Lean.Elab.Command.InductiveView.docString? : Lean.Elab.Command.InductiveView → Option (Lean.TSyntax `Lean.Parser.Command.docComment)
-- Mathlib.Topology.Sheaves.LocalPredicate
/-- For a binary operation (e.g. `x ↦ y ↦ x + y`) defined at each stalk, if a prelocal predicate is
closed under the operation on each open set (possibly by refinement), then the sheafified predicate
is also closed under the operation. See `sheafify_inductionOn₂'` for the version without
refinement.  -/
TopCat.PrelocalPredicate.sheafify_inductionOn₂ : ∀ {X : TopCat} {T₁ : ↑X → Type u_2} {T₂ : ↑X → Type u_3} {T₃ : ↑X → Type u_4} (P₁ : TopCat.PrelocalPredicate T₁)
  (P₂ : TopCat.PrelocalPredicate T₂) (P₃ : TopCat.PrelocalPredicate T₃) (op : {x : ↑X} → T₁ x → T₂ x → T₃ x),
  (∀ {U V : TopologicalSpace.Opens ↑X} {a : (x : ↥U) → T₁ ↑x} {b : (x : ↥V) → T₂ ↑x},
      P₁.pred a → P₂.pred b → ∀ (p : ↥(U ⊓ V)), ∃ W ia ib, ↑p ∈ W ∧ P₃.pred fun x => op (a (ia x)) (b (ib x))) →
    ∀ {U : TopologicalSpace.Opens ↑X} {a : (x : ↥U) → T₁ ↑x} {b : (x : ↥U) → T₂ ↑x},
      P₁.sheafify.pred a → P₂.sheafify.pred b → P₃.sheafify.pred fun x => op (a x) (b x)
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.mem_toSubring : ∀ {K : Type u} [inst : Field K] (A : ValuationSubring K) (x : K), x ∈ A.toSubring ↔ x ∈ A
-- Mathlib.CategoryTheory.Monoidal.Internal.Types.CommGrp_
CommGrpTypeEquivalenceCommGrp.inverse_obj_one : ∀ {A : CommGrpCat} {x : (fun X => X) (CategoryTheory.MonoidalCategoryStruct.tensorUnit (Type u))},
  (CategoryTheory.ConcreteCategory.hom CategoryTheory.MonObj.one) x = 1
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
CategoryTheory.Limits.pointwiseCocone_pt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} J]
  {K : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} K] [inst_3 : CategoryTheory.Limits.HasColimitsOfShape J C]
  (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)),
  (CategoryTheory.Limits.pointwiseCocone F).pt = F.flip.comp CategoryTheory.Limits.colim
-- Mathlib.CategoryTheory.Triangulated.TStructure.Basic
CategoryTheory.Triangulated.TStructure.shift_ge : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (a n n' : ℤ), a + n = n' → (t.ge n).shift a = t.ge n'
-- Init.Data.Dyadic.Basic
Int.trailingZeros.aux : (k : ℕ) → (i : ℤ) → i ≠ 0 → i.natAbs ≤ k → ℕ → ℕ
-- Mathlib.Order.MinMax
max_eq_iff : ∀ {α : Type u} [inst : LinearOrder α] {a b c : α}, max a b = c ↔ a = c ∧ b ≤ a ∨ b = c ∧ a ≤ b
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.instSub : {R : Type uR} →
  {ι : Type uι} →
    {M₁ : ι → Type v₁} →
      {M₂ : Type v₂} →
        [inst : Semiring R] →
          [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] →
            [inst_2 : AddCommGroup M₂] →
              [inst_3 : (i : ι) → Module R (M₁ i)] → [inst_4 : Module R M₂] → Sub (MultilinearMap R M₁ M₂)
-- Mathlib.Tactic.ClickSuggestions.Rewrite
/-- The nae of the used lemma.  -/
Mathlib.Tactic.ClickSuggestions.RwKey.name : Mathlib.Tactic.ClickSuggestions.RwKey → String
-- Std.Data.DTreeMap.Internal.Operations
/-- Slower version of `union` which can be used in absence of balance information but still assumes the preconditions of `union`, otherwise might panic.
 -/
Std.DTreeMap.Internal.Impl.union! : {α : Type u} →
  {β : α → Type v} →
    [Ord α] → Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl α β
-- Mathlib.Order.Hom.WithTopBot
/-- A version of `Equiv.optionCongr` for `WithTop`.  -/
OrderIso.withTopCongr : {α : Type u_1} → {β : Type u_2} → [inst : PartialOrder α] → [inst_1 : PartialOrder β] → α ≃o β → WithTop α ≃o WithTop β
-- Mathlib.LinearAlgebra.Multilinear.Basic
/-- **Alias** of `FunLike.coe_smul`. -/
MultilinearMap.coe_smul : ∀ {M : Type u_1} {F : Type u_3} {α : Type u_5} {β : Type u_6} [inst : FunLike F α β] [inst_1 : SMul M F]
  [inst_2 : SMul M β] [IsSMulApply M F α β] (n : M) (f : F), ⇑(n • f) = n • ⇑f
-- Mathlib.Order.Heyting.Boundary
Coheyting.boundary_le_boundary_sup_sup_boundary_inf_right : ∀ {α : Type u_1} [inst : CoheytingAlgebra α] {a b : α},
  Coheyting.boundary b ≤ Coheyting.boundary (a ⊔ b) ⊔ Coheyting.boundary (a ⊓ b)
-- Mathlib.CategoryTheory.Quotient
CategoryTheory.instInhabitedQuotient : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] → (r : HomRel C) → [Inhabited C] → Inhabited (CategoryTheory.Quotient r)
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
/-- If `H : C ⥤ D` is an additive functor and `φ` is a morphism of cochain complexes
in `C`, this is the comparison isomorphism (in each degree) between the image
by `H` of `mappingCone φ` and the mapping cone of the image by `H` of `φ`.  -/
CochainComplex.mappingCone.mapHomologicalComplexXIso : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v', u_2} D] →
        [inst_2 : CategoryTheory.Preadditive C] →
          [inst_3 : CategoryTheory.Preadditive D] →
            {F G : CochainComplex C ℤ} →
              (φ : F ⟶ G) →
                [inst_4 : HomologicalComplex.HasHomotopyCofiber φ] →
                  (H : CategoryTheory.Functor C D) →
                    [inst_5 : H.Additive] →
                      [inst_6 :
                          HomologicalComplex.HasHomotopyCofiber ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)] →
                        (n : ℤ) →
                          ((H.mapHomologicalComplex (ComplexShape.up ℤ)).obj (CochainComplex.mappingCone φ)).X n ≅
                            (CochainComplex.mappingCone ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).X n
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.degree_map : ∀ {R : Type u} {S : Type v} [inst : Ring R] [IsSimpleRing R] [inst_2 : Semiring S] [Nontrivial S] (p : Polynomial R)
  (f : R →+* S), (Polynomial.map f p).degree = p.degree
-- Mathlib.Topology.MetricSpace.Bounded
Bornology.IsBounded.subset_ball_lt : ∀ {α : Type u} {s : Set α} [inst : PseudoMetricSpace α],
  Bornology.IsBounded s → ∀ (a : ℝ) (c : α), ∃ r, a < r ∧ s ⊆ Metric.ball c r
-- Lean.MetavarContext
Lean.instReprMetavarKind : Repr Lean.MetavarKind
-- Mathlib.RingTheory.RootsOfUnity.Basic
mem_rootsOfUnity_prime_pow_mul_iff : ∀ (R : Type u_4) [inst : CommRing R] [IsReduced R] (p k m : ℕ) [ExpChar R p] {ζ : Rˣ},
  ζ ∈ rootsOfUnity (p ^ k * m) R ↔ ζ ∈ rootsOfUnity m R