mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Abelian.SerreClass.Localization
CategoryTheory.Abelian.coimage.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {P Q : C}
  (f f_1 : P ⟶ Q) (e_f : f = f_1) [inst_2 : CategoryTheory.Limits.HasKernel f]
  [inst_3 : CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι f)],
  CategoryTheory.Abelian.coimage f = CategoryTheory.Abelian.coimage f_1
-- Std.Data.HashSet.Basic
/-- Inserts the given element into the set. If the hash set already contains an element that is
equal (with regard to `==`) to the given element, then the hash set is returned unchanged.

Note: this non-replacement behavior is true for `HashSet` and `HashSet.Raw`.
The `insert` function on `HashMap`, `DHashMap`, `HashMap.Raw` and `DHashMap.Raw` behaves
differently: it will overwrite an existing mapping.
 -/
Std.HashSet.insert : {α : Type u} → {x : BEq α} → {x_1 : Hashable α} → Std.HashSet α → α → Std.HashSet α
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.FilterMap.0.Std.Iter.forIn_filterMapWithPostcondition.match_1.splitter : {β₂ : Type u_1} →
  (motive : Option β₂ → Sort u_2) →
    (__do_lift : Option β₂) → ((c : β₂) → motive (some c)) → (Unit → motive none) → motive __do_lift
-- Lean.DocString.Markdown
_private.Lean.DocString.Markdown.0.Lean.Doc.MarkdownM.State.mk.injEq : ∀ (footnotes footnotes_1 : Array (String × String)),
  ({ footnotes := footnotes } = { footnotes := footnotes_1 }) = (footnotes = footnotes_1)
-- Mathlib.Algebra.Torsor.Defs
Torsor.toMulAction : {G : outParam (Type u_1)} → {P : Type u_2} → {inst : Group G} → [self : Torsor G P] → MulAction G P
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.coeFn_negPart : ∀ {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} (f : ↥(MeasureTheory.Lp ℝ p μ)),
  ∀ᵐ (a : α) ∂μ, ↑↑(MeasureTheory.Lp.negPart f) a = -min (↑↑f a) 0
-- Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
mdifferentiableAt_add_section : ∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [inst : TopologicalSpace B]
  [inst_1 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_2 : (x : B) → TopologicalSpace (E x)]
  [inst_3 : NormedAddCommGroup F] [inst_4 : NontriviallyNormedField 𝕜] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : FiberBundle F E] [inst_7 : (x : B) → AddCommGroup (E x)] [inst_8 : (x : B) → Module 𝕜 (E x)]
  [VectorBundle 𝕜 F E] {HB : Type u_7} [inst_10 : TopologicalSpace HB] [inst_11 : ChartedSpace HB B] {EB : Type u_8}
  [inst_12 : NormedAddCommGroup EB] [inst_13 : NormedSpace 𝕜 EB] {I : ModelWithCorners 𝕜 EB HB} {s t : (x : B) → E x}
  {x₀ : B}, MDiffAt (T% s) x₀ → MDiffAt (T% t) x₀ → (MDiffAt fun x => ⟨x, (s + t) x⟩) x₀
-- Init.Data.List.Count
List.IsSuffix.count_le : ∀ {α : Type u_1} [inst : BEq α] {l₁ l₂ : List α} (a : α), l₁ <:+ l₂ → List.count a l₁ ≤ List.count a l₂
-- Init.SizeOf
_private.Init.Prelude.0.Lean.Macro.State.mk.sizeOf_spec : ∀ (macroScope : Lean.MacroScope) (traceMsgs : List (Lean.Name × String)) (expandedMacroDecls : List Lean.Name),
  sizeOf { macroScope := macroScope, traceMsgs := traceMsgs, expandedMacroDecls := expandedMacroDecls } =
    1 + sizeOf macroScope + sizeOf traceMsgs + sizeOf expandedMacroDecls
-- Init.Data.Float.Float
instInhabitedFloat : Inhabited Float
-- Mathlib.SetTheory.Cardinal.Finite
/-- `Nat.card α` is the cardinality of `α` as a natural number.
If `α` is infinite, `Nat.card α = 0`.  -/
Nat.card : Type u_3 → ℕ
-- Mathlib.Control.Traversable.Basic
ApplicativeTransformation.preserves_seq : ∀ {F : Type u → Type v} [inst : Applicative F] {G : Type u → Type w} [inst_1 : Applicative G]
  (η : ApplicativeTransformation F G) {α β : Type u} (x : F (α → β)) (y : F α),
  (fun {α} => η.app α) (x <*> y) = (fun {α} => η.app α) x <*> (fun {α} => η.app α) y
-- Mathlib.LinearAlgebra.Matrix.Hadamard
Matrix.diagonal_hadamard : ∀ {α : Type u_1} {n : Type u_3} [inst : DecidableEq n] [inst_1 : MulZeroClass α] (M : Matrix n n α) (w : n → α),
  (Matrix.diagonal w).hadamard M = Matrix.diagonal (w * M.diag)
-- Mathlib.Data.Set.Image
Set.union_preimage_subset : ∀ {α : Type u_1} {β : Type u_2} (s : Set α) (t : Set β) (f : α → β), s ∪ f ⁻¹' t ⊆ f ⁻¹' (f '' s ∪ t)
-- Mathlib.GroupTheory.GroupAction.Hom
MulActionHom.coe_neg : ∀ {M : Type u_2} {N : Type u_3} {X : Type u_4} {Y : Type u_5} {σ : M → N} [inst : SMul M X] [inst_1 : AddGroup Y]
  [inst_2 : DistribSMul N Y] (f : X →ₑ[σ] Y), ⇑(-f) = -⇑f
-- Init.Data.SInt.Lemmas
ISize.neg_eq_neg_one_mul : ∀ (a : ISize), -a = -1 * a
-- Lean.Elab.InfoTree.Types
/-- Whether to use explicit mode when pretty printing the term on hover.  -/
Lean.Elab.DelabTermInfo.explicit : Lean.Elab.DelabTermInfo → Bool
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.mul_C_eq_smul : ∀ {R : Type u_1} {a b : R} [inst : CommSemiring R] (r : R) (x : QuadraticAlgebra R a b),
  x * QuadraticAlgebra.C r = r • x
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.containsThenInsertIfNew_fst : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {v : β}, (t.containsThenInsertIfNew k v).1 = t.contains k
-- Mathlib.Order.Zorn
/-- Every chain is contained in a maximal chain. This generalizes Hausdorff's maximality principle.
 -/
IsChain.exists_maxChain : ∀ {α : Type u_1} {r : α → α → Prop} {c : Set α}, IsChain r c → ∃ M, IsMaxChain r M ∧ c ⊆ M
-- Mathlib.CategoryTheory.Localization.SmallHom
CategoryTheory.Localization.hasSmallLocalizedHom_iff_of_isos : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (W : CategoryTheory.MorphismProperty C) {X Y X' Y' : C}
  (e : X ≅ X') (e' : Y ≅ Y'),
  CategoryTheory.Localization.HasSmallLocalizedHom W X Y ↔ CategoryTheory.Localization.HasSmallLocalizedHom W X' Y'
-- Lean.ToExpr
Lean.instToExprFilePath : Lean.ToExpr System.FilePath
-- Mathlib.MeasureTheory.Integral.Marginal
MeasureTheory.lmarginal_eq_of_subset : ∀ {δ : Type u_1} {X : δ → Type u_3} [inst : (i : δ) → MeasurableSpace (X i)] {μ : (i : δ) → MeasureTheory.Measure (X i)}
  [inst_1 : DecidableEq δ] {s t : Finset δ} [∀ (i : δ), MeasureTheory.SigmaFinite (μ i)]
  {f g : ((i : δ) → X i) → ENNReal},
  s ⊆ t → Measurable f → Measurable g → ∫⋯∫⁻_s, f ∂μ = ∫⋯∫⁻_s, g ∂μ → ∫⋯∫⁻_t, f ∂μ = ∫⋯∫⁻_t, g ∂μ
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.norm_le_one : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (z : ℤ_[p]), ‖z‖ ≤ 1
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.compl_adj : ∀ {V : Type u} (G : SimpleGraph V) (v w : V), Gᶜ.Adj v w ↔ v ≠ w ∧ ¬G.Adj v w
-- Std.Http.Server.Config
/-- Default buffer size for the connection
 -/
Std.Http.Config.defaultPayloadBytes : Std.Http.Config → ℕ
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.trans_apply : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} {A₃ : Type uA₃} [inst : CommSemiring R] [inst_1 : Semiring A₁]
  [inst_2 : Semiring A₂] [inst_3 : Semiring A₃] [inst_4 : Algebra R A₁] [inst_5 : Algebra R A₂] [inst_6 : Algebra R A₃]
  (e₁ : A₁ ≃ₐ[R] A₂) (e₂ : A₂ ≃ₐ[R] A₃) (x : A₁), (e₁.trans e₂) x = e₂ (e₁ x)
-- Init.Meta.Defs
/-- Configures the behaviour of the `apply` tactic.  -/
Lean.Meta.ApplyConfig : Type
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.Functor.RepresentableBy.coyoneda_homEquiv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (X Y : C),
  (CategoryTheory.Functor.RepresentableBy.yoneda X).homEquiv = Equiv.refl (Y ⟶ X)
-- Mathlib.LinearAlgebra.FreeModule.Finite.CardQuotient
AddSubgroup.relIndex_eq_natAbs_det : ∀ {E : Type u_1} [inst : AddCommGroup E] (L₁ L₂ : AddSubgroup E) (H : L₁ ≤ L₂) {ι : Type u_2} [inst_1 : DecidableEq ι]
  [inst_2 : Fintype ι] (b₁ : Module.Basis ι ℤ ↥(AddSubgroup.toIntSubmodule L₁))
  (b₂ : Module.Basis ι ℤ ↥(AddSubgroup.toIntSubmodule L₂)), L₁.relIndex L₂ = (b₂.det fun i => ⟨↑(b₁ i), ⋯⟩).natAbs
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- The contravariant categorical equivalence between augmented simplicial
objects and augmented cosimplicial objects in the opposite category.  -/
CategoryTheory.simplicialCosimplicialAugmentedEquiv : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    (CategoryTheory.SimplicialObject.Augmented C)ᵒᵖ ≌ CategoryTheory.CosimplicialObject.Augmented Cᵒᵖ
-- Mathlib.Algebra.Lie.Weights.RootSystem
LieAlgebra.IsKilling.chainTopCoeff_of_eq_zsmul_add : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : CharZero K] [inst_2 : LieRing L] [inst_3 : LieAlgebra K L]
  [LieAlgebra.IsKilling K L] [inst_5 : FiniteDimensional K L] {H : LieSubalgebra K L} [inst_6 : H.IsCartanSubalgebra]
  [LieModule.IsTriangularizable K (↥H) L] (α β : LieModule.Weight K (↥H) L),
  α.IsNonZero →
    ∀ (β' : LieModule.Weight K (↥H) L) (n : ℤ),
      ⇑β' = n • ⇑α + ⇑β → ↑(LieModule.chainTopCoeff (⇑α) β') = ↑(LieModule.chainTopCoeff (⇑α) β) - n
-- Mathlib.RepresentationTheory.Equiv
Representation.leftRegularTensorTrivialIsoFree_apply_single_tmul_single : ∀ {G : Type v} [inst : Monoid G] {k : Type u} [inst_1 : CommSemiring k] {α : Type w'} (g : G) (i : α) (r s : k),
  (Representation.leftRegularTensorTrivialIsoFree α) (MonoidAlgebra.single g r ⊗ₜ[k] MonoidAlgebra.single i s) =
    fun₀ | i => MonoidAlgebra.single g (r * s)
-- Mathlib.RingTheory.LinearDisjoint
Subalgebra.LinearDisjoint.of_subsingleton : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] {A B : Subalgebra R S}
  [Subsingleton R], A.LinearDisjoint B
-- Mathlib.AlgebraicTopology.SimplicialComplex.Basic
PreAbstractSimplicialComplex.instCompleteSemilatticeInf : (ι : Type u_1) → CompleteSemilatticeInf (PreAbstractSimplicialComplex ι)
-- Mathlib.Order.Partition.Finpartition
Finpartition.ofErase.eq_1 : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : OrderBot α] [inst_2 : DecidableEq α] {a : α} (parts : Finset α)
  (sup_indep : parts.SupIndep id) (sup_parts : parts.sup id = a),
  Finpartition.ofErase parts sup_indep sup_parts =
    { parts := parts.erase ⊥, supIndep := ⋯, sup_parts := ⋯, bot_notMem := ⋯ }
-- Mathlib.CategoryTheory.Category.Cat
/-- Construct a bundled `Cat` from the underlying type and the typeclass.  -/
CategoryTheory.Cat.of : (C : Type u) → [CategoryTheory.Category.{v, u} C] → CategoryTheory.Cat
-- Mathlib.CategoryTheory.Bicategory.CatEnriched
CategoryTheory.CatEnriched.eqToHom_hComp_eqToHom : ∀ {C : Type u_1} [inst : CategoryTheory.EnrichedCategory CategoryTheory.Cat C] {a b c : CategoryTheory.CatEnriched C}
  {f f' : a ⟶ b} (α : f = f') {g g' : b ⟶ c} (β : g = g'),
  CategoryTheory.CatEnriched.hComp (CategoryTheory.eqToHom α) (CategoryTheory.eqToHom β) = CategoryTheory.eqToHom ⋯
-- Mathlib.CategoryTheory.Sites.Over
CategoryTheory.Sieve.overEquiv_pullback : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {Y₁ Y₂ : CategoryTheory.Over X} (f : Y₁ ⟶ Y₂)
  (S : CategoryTheory.Sieve Y₂),
  (CategoryTheory.Sieve.overEquiv Y₁) (CategoryTheory.Sieve.pullback f S) =
    CategoryTheory.Sieve.pullback (CategoryTheory.Over.Hom.left f) ((CategoryTheory.Sieve.overEquiv Y₂) S)
-- Mathlib.RingTheory.WittVector.WittPolynomial
aeval_wittPolynomial : ∀ (p : ℕ) (R : Type u_1) [inst : CommRing R] {A : Type u_3} [inst_1 : CommRing A] [inst_2 : Algebra R A] (f : ℕ → A)
  (n : ℕ), (MvPolynomial.aeval f) (wittPolynomial p R n) = ∑ i ∈ Finset.range (n + 1), ↑p ^ i * f i ^ p ^ (n - i)
-- Mathlib.Algebra.Order.Group.PosPart
add_abs_eq_two_nsmul_posPart : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddCommGroup α] [AddLeftMono α] (a : α), a + |a| = 2 • a⁺
-- Mathlib.LinearAlgebra.LinearIndependent.Algebra
LinearIndependent.algebraMap_comp_iff : ∀ {R : Type u_1} {S : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Semiring A]
  [inst_3 : Algebra R S] [inst_4 : Algebra S A] [inst_5 : Algebra R A] [IsScalarTower R S A] [FaithfulSMul S A]
  {ι : Type u_4} {v : ι → S}, LinearIndependent R (⇑(algebraMap S A) ∘ v) ↔ LinearIndependent R v
-- Lean.Data.Lsp.Basic
Lean.Lsp.instToJsonStaticRegistrationOptions : Lean.ToJson Lean.Lsp.StaticRegistrationOptions
-- Mathlib.LinearAlgebra.Matrix.Invertible
/-- A matrix is invertible if the conjugate transpose is invertible.  -/
Matrix.invertibleOfInvertibleConjTranspose : {n : Type u_2} →
  {α : Type u_3} →
    [inst : Fintype n] →
      [inst_1 : DecidableEq n] →
        [inst_2 : Semiring α] → [inst_3 : StarRing α] → (A : Matrix n n α) → [Invertible A.conjTranspose] → Invertible A
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
comap_inv_leftUniformSpace : ∀ (G : Type u_1) [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalGroup G],
  UniformSpace.comap (⇑(Equiv.inv G)) (IsTopologicalGroup.leftUniformSpace G) = IsTopologicalGroup.rightUniformSpace G
-- Lean.Parser.Basic
Lean.Parser.unicodeSymbolNoAntiquot : String → String → Bool → Lean.Parser.Parser
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.top_prod : ∀ {N : Type u_2} [inst : MulOneClass N] {M : Type u_5} [inst_1 : MulOneClass M] (s : Submonoid N),
  ⊤.prod s = Submonoid.comap (MonoidHom.snd M N) s
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
/-- This is a helper construction that can be useful when verifying that a category has all
pushout. Given `F : WalkingSpan ⥤ C`, which is really the same as
`span (F.map fst) (F.map snd)`, and a pushout cocone on `F.map fst` and `F.map snd`,
we get a cocone on `F`.

If you're thinking about using this, have a look at `hasPushouts_of_hasColimit_span`, which
you may find to be an easier way of achieving your goal.  -/
CategoryTheory.Limits.Cocone.ofPushoutCocone : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor CategoryTheory.Limits.WalkingSpan C} →
      CategoryTheory.Limits.PushoutCocone (F.map CategoryTheory.Limits.WalkingSpan.Hom.fst)
          (F.map CategoryTheory.Limits.WalkingSpan.Hom.snd) →
        CategoryTheory.Limits.Cocone F
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
_private.Mathlib.CategoryTheory.Sites.Hypercover.Zero.0.CategoryTheory.PreZeroHypercover.sumLift.match_1.eq_2 : ∀ {C : Type u_4} [inst : CategoryTheory.Category.{u_3, u_4} C] {S : C} {E : CategoryTheory.PreZeroHypercover S}
  {F : CategoryTheory.PreZeroHypercover S} (motive : (E.sum F).I₀ → Sort u_5) (i : F.I₀)
  (h_1 : (i : E.I₀) → motive (Sum.inl i)) (h_2 : (i : F.I₀) → motive (Sum.inr i)),
  (match Sum.inr i with
    | Sum.inl i => h_1 i
    | Sum.inr i => h_2 i) =
    h_2 i
-- Lean.Meta.Tactic.Grind.CollectParams
_private.Lean.Meta.Tactic.Grind.CollectParams.0.Lean.Meta.Grind.Collector.State.params : Lean.Meta.Grind.Collector.State✝ → Array Lean.Meta.Grind.TParam
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.Red.Step.diamond : ∀ {α : Type u} {L₁ L₂ L₃ L₄ : List (α × Bool)},
  FreeGroup.Red.Step L₁ L₃ →
    FreeGroup.Red.Step L₂ L₄ → L₁ = L₂ → L₃ = L₄ ∨ ∃ L₅, FreeGroup.Red.Step L₃ L₅ ∧ FreeGroup.Red.Step L₄ L₅
-- Mathlib.Topology.Algebra.Group.Defs
ContinuousAt.div' : ∀ {G : Type u_1} {X : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace G] [inst_2 : Div G]
  [ContinuousDiv G] {f g : X → G} {x : X}, ContinuousAt f x → ContinuousAt g x → ContinuousAt (f / g) x
-- Mathlib.Algebra.Group.Prod
AddMonoidHom.comp_coprod : ∀ {M : Type u_3} {N : Type u_4} {P : Type u_5} [inst : AddZeroClass M] [inst_1 : AddZeroClass N]
  [inst_2 : AddCommMonoid P] {Q : Type u_6} [inst_3 : AddCommMonoid Q] (h : P →+ Q) (f : M →+ P) (g : N →+ P),
  h.comp (f.coprod g) = (h.comp f).coprod (h.comp g)
-- Aesop.Tree.UnsafeQueue
Aesop.PostponedSafeRule.mk : Aesop.SafeRule → Aesop.RuleTacOutput → Aesop.PostponedSafeRule
-- Mathlib.Order.Category.Preord
/-- Typecheck a `OrderHom` as a morphism in `Preord`.  -/
Preord.ofHom : {X Y : Type u} →
  [inst : Preorder X] →
    [inst_1 : Preorder Y] → (X →o Y) → ({ carrier := X, str := inst } ⟶ { carrier := Y, str := inst_1 })
-- Mathlib.Order.Filter.Pointwise
Filter.vaddAssocClass' : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : VAdd α β] [inst_1 : VAdd α γ] [inst_2 : VAdd β γ]
  [VAddAssocClass α β γ], VAddAssocClass α (Filter β) (Filter γ)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVExpr.arithShiftRight.injEq : ∀ {m n : ℕ} (lhs : Std.Tactic.BVDecide.BVExpr m) (rhs : Std.Tactic.BVDecide.BVExpr n) (n_1 : ℕ)
  (lhs_1 : Std.Tactic.BVDecide.BVExpr m) (rhs_1 : Std.Tactic.BVDecide.BVExpr n_1),
  (lhs.arithShiftRight rhs = lhs_1.arithShiftRight rhs_1) = (n = n_1 ∧ lhs = lhs_1 ∧ rhs ≍ rhs_1)
-- Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
NumberField.InfinitePlace.Completion.algebraMap_coe : ∀ {K : Type u_1} [inst : Field K] {v : NumberField.InfinitePlace K} {L : Type u_2} [inst_1 : Field L]
  [inst_2 : Algebra K L] (w : NumberField.InfinitePlace L) [inst_3 : Algebra v.Completion w.Completion]
  [IsScalarTower K v.Completion w.Completion] (x : WithAbs ↑v),
  (algebraMap v.Completion w.Completion) { toCompletion := ↑x } =
    { toCompletion := ↑((algebraMap (WithAbs ↑v) (WithAbs ↑w)) x) }
-- Mathlib.CategoryTheory.Shift.SingleFunctors
CategoryTheory.SingleFunctors.hom_inv_id_hom_app : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {A : Type u_5} [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift D A] {F G : CategoryTheory.SingleFunctors C D A} (e : F ≅ G) (n : A) (X : C),
  CategoryTheory.CategoryStruct.comp ((e.hom.hom n).app X) ((e.inv.hom n).app X) =
    CategoryTheory.CategoryStruct.id ((F.functor n).obj X)
-- Mathlib.MeasureTheory.Group.Action
MeasureTheory.vadd_mem_ae : ∀ {G : Type u} {α : Type w} {m : MeasurableSpace α} [inst : AddGroup G] [inst_1 : AddAction G α]
  {μ : MeasureTheory.Measure α} [MeasureTheory.VAddInvariantMeasure G α μ] (c : G) {s : Set α},
  c +ᵥ s ∈ MeasureTheory.ae μ ↔ s ∈ MeasureTheory.ae μ
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteAddGrp.instHasForget₂FiniteAddGrpAddMonoidHomCarrierToAddGrpContinuousAddMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfinite : CategoryTheory.HasForget₂ FiniteAddGrp.{u_1} ProfiniteAddGrp.{u_1}
-- Std.Data.DHashMap.Internal.Defs
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.getKey! : {α : Type u} → {β : α → Type v} → [BEq α] → [Hashable α] → [Inhabited α] → Std.DHashMap.Internal.Raw₀ α β → α → α
-- Init.Data.String.Pattern.Basic
String.Slice.Pattern.ToBackwardSearcher.DefaultBackwardSearcher.currPos : {ρ : Type} →
  {pat : ρ} → {s : String.Slice} → String.Slice.Pattern.ToBackwardSearcher.DefaultBackwardSearcher pat s → s.Pos
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.excenter_univ : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n),
  s.excenter Finset.univ = s.incenter
-- Lean.Data.PPContext
Lean.PPContext.mctx : Lean.PPContext → Lean.MetavarContext
-- Init.Data.UInt.Bitwise
UInt8.toFin_or : ∀ (a b : UInt8), (a ||| b).toFin = a.toFin ||| b.toFin
-- Lean.Expr
/-- Annotate `e` with `pp.explicit := flag`
The delaborator uses `pp` options.
 -/
Lean.Expr.setPPExplicit : Lean.Expr → Bool → Lean.Expr
-- Mathlib.Data.List.Sort
List.sortedGE_iff_pairwise : ∀ {α : Type u_1} {l : List α} [inst : Preorder α], l.SortedGE ↔ List.Pairwise (fun x1 x2 => x1 ≥ x2) l
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.Δ_of_isCharThreeJNeZeroNF : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [W.IsCharThreeJNeZeroNF],
  W.Δ = -64 * W.a₂ ^ 3 * W.a₆ - 432 * W.a₆ ^ 2
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.instMulActionElemRootSetOfSMulCommClass : {R : Type u} →
  {S : Type v} →
    [inst : CommRing R] →
      [inst_1 : IsDomain R] →
        [inst_2 : CommRing S] →
          [inst_3 : Algebra S R] →
            (G : Type u_1) →
              [inst_4 : Monoid G] →
                [inst_5 : MulSemiringAction G R] →
                  [SMulCommClass G S R] → (f : Polynomial S) → MulAction G ↑(f.rootSet R)
-- Mathlib.Geometry.Manifold.LocalDiffeomorph
PartialDiffeomorph.contMDiffOn_toFun : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {H₁ : Type u_5}
  [inst_5 : TopologicalSpace H₁] {H₂ : Type u_6} [inst_6 : TopologicalSpace H₂] {I : ModelWithCorners 𝕜 E H₁}
  {J : ModelWithCorners 𝕜 F H₂} {M : Type u_8} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H₁ M] {N : Type u_9}
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace H₂ N] {n : WithTop ℕ∞} (self : PartialDiffeomorph I J M N n),
  ContMDiffOn I J n (↑self.toPartialEquiv) self.source
-- Mathlib.GroupTheory.MonoidLocalization.GrothendieckGroup
IsUnit.liftRight.congr_simp : ∀ {M : Type u_3} {N : Type u_4} [inst : Monoid M] [inst_1 : Monoid N] (f f_1 : M →* N) (e_f : f = f_1)
  (hf : ∀ (x : M), IsUnit (f x)), IsUnit.liftRight f hf = IsUnit.liftRight f_1 ⋯
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
extChartAt_coe_symm : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  {I : ModelWithCorners 𝕜 E H} [inst_5 : ChartedSpace H M] (x : M),
  ↑(extChartAt I x).symm = ↑(chartAt H x).symm ∘ ↑I.symm
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
/-- **Alias** of `FunLike.coe_coeAddMonoidHom`. -/
SchwartzMap.coe_coeHom : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : AddZero F] [inst_2 : AddZeroClass β]
  [inst_3 : IsZeroApply F α β] [inst_4 : IsAddApply F α β], ⇑(FunLike.coeAddMonoidHom F α β) = DFunLike.coe
-- Mathlib.Util.AtLocation
Mathlib.Tactic.BehaviorIfUnchanged.noConfusionType : Sort v✝ → Mathlib.Tactic.BehaviorIfUnchanged → Mathlib.Tactic.BehaviorIfUnchanged → Sort v✝
-- Mathlib.Topology.Category.Locale
instLargeCategoryLocale : CategoryTheory.LargeCategory Locale
-- Mathlib.Algebra.Module.Submodule.Bilinear
Submodule.apply_mem_map₂ : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Module R P] (f : M →ₗ[R] N →ₗ[R] P) {m : M} {n : N} {p : Submodule R M} {q : Submodule R N},
  m ∈ p → n ∈ q → (f m) n ∈ Submodule.map₂ f p q
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
ContMDiffAt.mdifferentiableAt : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {x : M} {n : WithTop ℕ∞},
  ContMDiffAt I I' n f x → n ≠ 0 → MDiffAt f x
-- Mathlib.Algebra.Lie.Basis.Basic
LieAlgebra.Basis.ext_iff : ∀ {ι : Type u_1} {R : Type u_2} {L : Type u_3} {inst : Finite ι} {inst_1 : CommRing R} {inst_2 : LieRing L}
  {inst_3 : LieAlgebra R L} {H : LieSubalgebra R L} {x y : LieAlgebra.Basis ι H},
  x = y ↔ x.A = y.A ∧ x.h = y.h ∧ x.e = y.e ∧ x.f = y.f
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem!_eq_default : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited β], t.WF → ∀ {a : α}, a ∉ t → t[a]! = default
-- Mathlib.Topology.Algebra.Nonarchimedean.Basic
/-- An open neighborhood of the identity in
the Cartesian square of a nonarchimedean group contains the Cartesian square of
an open neighborhood in the group.  -/
NonarchimedeanAddGroup.prod_self_subset : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [NonarchimedeanAddGroup G] {U : Set (G × G)},
  U ∈ nhds 0 → ∃ V, ↑V ×ˢ ↑V ⊆ U
-- Std.Http.Data.URI.Encoding
/-- Decodes an encoded fragment component back to a UTF-8 string.
 -/
Std.Http.URI.EncodedFragment.decode : Std.Http.URI.EncodedFragment → Option String