mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Expr
Lean.Expr.const.inj : ∀ {declName : Lean.Name} {us : List Lean.Level} {declName_1 : Lean.Name} {us_1 : List Lean.Level},
  Lean.Expr.const declName us = Lean.Expr.const declName_1 us_1 → declName = declName_1 ∧ us = us_1
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
SheafOfModules.ιFree_mapFreeIso_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : CategoryTheory.HasWeakSheafify J AddCommGrpCat]
  [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] {C' : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} C']
  {J' : CategoryTheory.GrothendieckTopology C'} {S : CategoryTheory.Sheaf J' RingCat}
  [inst_4 : CategoryTheory.HasSheafify J' AddCommGrpCat] [inst_5 : J'.WEqualsLocallyBijective AddCommGrpCat]
  (F : CategoryTheory.Functor (SheafOfModules R) (SheafOfModules S)) (I : Type u)
  [inst_6 : CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete I) F]
  (η : SheafOfModules.unit S ≅ F.obj (SheafOfModules.unit R)) (i : I),
  CategoryTheory.CategoryStruct.comp (SheafOfModules.ιFree i) (SheafOfModules.mapFreeIso F I η).hom =
    CategoryTheory.CategoryStruct.comp η.hom (F.map (SheafOfModules.ιFree i))
-- Mathlib.Data.Matrix.Block
Matrix.fromBlocks.eq_1 : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} (A : Matrix n l α) (B : Matrix n m α)
  (C : Matrix o l α) (D : Matrix o m α),
  Matrix.fromBlocks A B C D = Matrix.of (Sum.elim (fun i => Sum.elim (A i) (B i)) fun j => Sum.elim (C j) (D j))
-- Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
MvPolynomial.msymm.eq_1 : ∀ (σ : Type u_5) (R : Type u_6) [inst : CommSemiring R] [inst_1 : Fintype σ] [inst_2 : DecidableEq σ] {n : ℕ}
  (μ : n.Partition), MvPolynomial.msymm σ R μ = ∑ s, (Multiset.map MvPolynomial.X ↑↑s).prod
-- Mathlib.Data.Finset.Card
Finset.card_strictMono : ∀ {α : Type u_1}, StrictMono Finset.card
-- Mathlib.Analysis.Meromorphic.Basic
/-- Eta-expanded form of `MeromorphicOn.const_smul` -/
MeromorphicOn.fun_const_smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {R : Type u_4} [inst_3 : NormedRing R] [inst_4 : Module R E] [IsBoundedSMul R E]
  {f : 𝕜 → E} {U : Set 𝕜}, MeromorphicOn f U → ∀ [SMulCommClass 𝕜 R E] (c : R), MeromorphicOn (fun i => c • f i) U
-- Mathlib.Data.Real.Basic
Real.mul_add_one_le_add_one_pow : ∀ {a : ℝ}, 0 ≤ a → ∀ (b : ℕ), a * ↑b + 1 ≤ (a + 1) ^ b
-- Mathlib.Algebra.Lie.Weights.Basic
LieModule.map_posFittingComp_eq : ∀ {R : Type u_2} {L : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] {M₂ : Type u_5} [inst_8 : AddCommGroup M₂] [inst_9 : Module R M₂]
  [inst_10 : LieRingModule L M₂] [inst_11 : LieModule R L M₂] (e : M ≃ₗ⁅R,L⁆ M₂),
  LieSubmodule.map e.toLieModuleHom (LieModule.posFittingComp R L M) = LieModule.posFittingComp R L M₂
-- Mathlib.Data.Multiset.UnionInter
Multiset.instInter : {α : Type u_1} → [DecidableEq α] → Inter (Multiset α)
-- Lean.Compiler.LCNF.Basic
/-- We store the inline attribute at LCNF declarations to make sure we can set them for
auxiliary declarations created during compilation.
 -/
Lean.Compiler.LCNF.Decl.inlineAttr? : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.Decl pu → Option Lean.Compiler.InlineAttributeKind
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp.hom_inv_apply : ∀ {M N : SemiNormedGrp} (e : M ≅ N) (s : N.carrier),
  (CategoryTheory.ConcreteCategory.hom e.hom) ((CategoryTheory.ConcreteCategory.hom e.inv) s) = s
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
Complex.sinh_eq_tsum : ∀ (z : ℂ), Complex.sinh z = ∑' (n : ℕ), z ^ (2 * n + 1) / ↑(2 * n + 1).factorial
-- Plausible.Arbitrary
/-- A random generator for values of the given type.  -/
Plausible.Arbitrary.arbitrary : {α : Type u} → [self : Plausible.Arbitrary α] → Plausible.Gen α
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get?_diff_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k : α}, k ∉ t₁ → (t₁ \ t₂).get? k = none
-- Init.Data.Option.Basic
/-- Sequencing of `Option` computations.

From the perspective of `Option` as computations that might fail, this function sequences
potentially-failing computations, failing if either fails. From the perspective of `Option` as a
collection with at most one element, the function is applied to the element if present, and the
final result is empty if either the initial or the resulting collections are empty.

This function is often accessed via the `>>=` operator from the `Bind (Option α)` instance, or
implicitly via `do`-notation, but it is also idiomatic to call it using [generalized field
notation](https://lean-lang.org/doc/reference/4.33.0/find/?domain=Verso.Genre.Manual.section&name=generalized-field-notation).

Examples:
 * `none.bind (fun x => some x) = none`
 * `(some 4).bind (fun x => some x) = some 4`
 * `none.bind (Option.guard (· > 2)) = none`
 * `(some 2).bind (Option.guard (· > 2)) = none`
 * `(some 4).bind (Option.guard (· > 2)) = some 4`
 -/
Option.bind : {α : Type u_1} → {β : Type u_2} → Option α → (α → Option β) → Option β
-- Mathlib.Topology.LocallyClosed
isClosed_preimage_val_coborder : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, IsClosed (Subtype.val ⁻¹' s)
-- Init.Data.String.Basic
/-- Checks whether substrings of two strings are equal. Substrings are indicated by their starting
positions and a size in _UTF-8 bytes_. Returns `false` if the indicated substring does not exist in
either string.

This is a legacy function. The recommended alternative is to construct slices representing the
strings to be compared and use the `BEq` instance of `String.Slice`.
 -/
String.Pos.Raw.substrEq : String → String.Pos.Raw → String → String.Pos.Raw → ℕ → Bool
-- Mathlib.Algebra.Homology.ShortComplex.Basic
/-- the first (left) object of a `ShortComplex`  -/
CategoryTheory.ShortComplex.X₁ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] → CategoryTheory.ShortComplex C → C
-- Mathlib.Order.Filter.Pi
Filter.pi_comap : ∀ {ι : Type u_1} {α : ι → Type u_2} {β : ι → Type u_3} {f : (i : ι) → α i → β i} {l : (i : ι) → Filter (β i)},
  (Filter.pi fun i => Filter.comap (f i) (l i)) = Filter.comap (Pi.map f) (Filter.pi l)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.CooperSplitProof.dec.sizeOf_spec : ∀ (h : Lean.FVarId), sizeOf (Lean.Meta.Grind.Arith.Cutsat.CooperSplitProof.dec h) = 1 + sizeOf h
-- Mathlib.Analysis.Calculus.ContDiff.RCLike
/-- If `f` is `C¹` on a convex set `s`, it is locally Lipschitz on `s`.  -/
ContDiffOn.locallyLipschitzOn : ∀ {E : Type u_4} {F : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {f : E → F} {s : Set E}, Convex ℝ s → ContDiffOn ℝ 1 f s → LocallyLipschitzOn s f
-- Mathlib.Data.List.Sort
/-- **Alias** of the forward direction of `List.sortedGT_iff_pairwise`. -/
List.SortedGT.pairwise : ∀ {α : Type u_1} {l : List α} [inst : Preorder α], l.SortedGT → List.Pairwise (fun x1 x2 => x1 > x2) l
-- Mathlib.Analysis.InnerProductSpace.Reproducing
RKHS.norm_kernel_sq_le : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {X : Type u_2} {V : Type u_3} [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] (H : Type u_4) [inst_3 : NormedAddCommGroup H] [inst_4 : InnerProductSpace 𝕜 H]
  [inst_5 : RKHS 𝕜 H X V] [inst_6 : CompleteSpace H] [inst_7 : CompleteSpace V] (x y : X),
  ‖RKHS.kernel H x y‖ ^ 2 ≤ ‖RKHS.kernel H x x‖ * ‖RKHS.kernel H y y‖
-- Mathlib.CategoryTheory.Functor.Flat
CategoryTheory.final_of_representablyFlat : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [h : CategoryTheory.RepresentablyFlat F], F.Final
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKey?_insertManyIfNewUnit_empty_list_of_contains_eq_false : ∀ {α : Type u} {instOrd : Ord α} [Std.TransOrd α] [inst : BEq α] [Std.LawfulBEqOrd α] {l : List α} {k : α},
  l.contains k = false →
    (↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit Std.DTreeMap.Internal.Impl.empty l ⋯)).getKey? k = none
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.prodEquiv.eq_1 : ∀ {N : Type u_2} [inst : AddZeroClass N] {M : Type u_5} [inst_1 : AddZeroClass M] (s : AddSubmonoid M)
  (t : AddSubmonoid N), s.prodEquiv t = { toEquiv := Equiv.Set.prod ↑s ↑t, map_add' := ⋯ }
-- Mathlib.Data.EReal.Basic
EReal.rec_coe : ∀ {motive : EReal → Sort u_1} (bot : motive ⊥) (coe : (a : ℝ) → motive ↑a) (top : motive ⊤) (a : ℝ),
  EReal.rec bot coe top ↑a = coe a
-- Mathlib.CategoryTheory.Limits.Shapes.Diagonal
CategoryTheory.Limits.pullback.instIsSplitEpiFst : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} (f : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasPullback f f], CategoryTheory.IsSplitEpi (CategoryTheory.Limits.pullback.fst f f)
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.inhabitedCone : {C : Type u₃} →
  [inst : CategoryTheory.Category.{v₃, u₃} C] →
    (F : CategoryTheory.Functor (CategoryTheory.Discrete PUnit.{u_1 + 1}) C) → Inhabited (CategoryTheory.Limits.Cone F)
-- Mathlib.Order.Hom.CompleteLattice
/-- `id` as an `sInfHom`.  -/
sInfHom.id : (α : Type u_2) → [inst : InfSet α] → sInfHom α α
-- Mathlib.CategoryTheory.Localization.SmallHom
CategoryTheory.LocalizerMorphism.smallHomMap'_mk : ∀ {C₁ : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C₁] {W₁ : CategoryTheory.MorphismProperty C₁} {C₂ : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] {W₂ : CategoryTheory.MorphismProperty C₂}
  (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) {X Y : C₁}
  [inst_2 : CategoryTheory.Localization.HasSmallLocalizedHom W₁ X Y] {X' Y' : C₂}
  [inst_3 : CategoryTheory.Localization.HasSmallLocalizedHom W₂ X' X']
  [inst_4 : CategoryTheory.Localization.HasSmallLocalizedHom W₂ X' Y']
  [inst_5 : CategoryTheory.Localization.HasSmallLocalizedHom W₂ Y' Y'] (eX : Φ.functor.obj X ≅ X')
  (eY : Φ.functor.obj Y ≅ Y') (f : X ⟶ Y),
  Φ.smallHomMap' eX eY (CategoryTheory.Localization.SmallHom.mk W₁ f) =
    CategoryTheory.Localization.SmallHom.mk W₂
      (CategoryTheory.CategoryStruct.comp eX.inv (CategoryTheory.CategoryStruct.comp (Φ.functor.map f) eY.hom))
-- Mathlib.Data.List.SplitLengths
List.splitLengths_length_getElem : ∀ {α : Type u_2} (l : List α) (sz : List ℕ),
  sz.sum ≤ l.length → ∀ (i : ℕ) (hi : i < (sz.splitLengths l).length), (sz.splitLengths l)[i].length = sz[i]
-- Mathlib.Algebra.Homology.HomotopyCategory.KProjective
HomotopyEquiv.isKProjective : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {K₁ K₂ : CochainComplex C ℤ} (e : HomotopyEquiv K₁ K₂) [K₁.IsKProjective], K₂.IsKProjective
-- Mathlib.RingTheory.IsGaloisGroup.Defs
IsGaloisGroup.of_algEquiv : ∀ (G : Type u_1) (A : Type u_2) (B : Type u_4) [inst : Group G] [inst_1 : CommSemiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra A B] [inst_4 : MulSemiringAction G B] [hG : IsGaloisGroup G A B] (B' : Type u_5)
  [inst_5 : Semiring B'] [inst_6 : Algebra A B'] [inst_7 : MulSemiringAction G B'] (e : B ≃ₐ[A] B'),
  (∀ (g : G) (x : B), e (g • x) = g • e x) → IsGaloisGroup G A B'
-- Lean.DocString.Extension
Lean.ModuleDoc.mk.inj : ∀ {doc : String} {declarationRange : Lean.DeclarationRange} {doc_1 : String}
  {declarationRange_1 : Lean.DeclarationRange},
  { doc := doc, declarationRange := declarationRange } = { doc := doc_1, declarationRange := declarationRange_1 } →
    doc = doc_1 ∧ declarationRange = declarationRange_1
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.CodeDecl.sset : {pu : Lean.Compiler.LCNF.Purity} →
  Lean.FVarId →
    ℕ →
      ℕ →
        Lean.FVarId →
          Lean.Expr →
            autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.CodeDecl._auto_7 →
              Lean.Compiler.LCNF.CodeDecl pu
-- Mathlib.Analysis.Polynomial.CauchyBound
Polynomial.cauchyBound_zero : ∀ {K : Type u_1} [inst : NormedDivisionRing K], Polynomial.cauchyBound 0 = 1
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.Pattern.Model.CharPred.Decidable.matchesAt_iff_matchesAt_decide : ∀ {p : Char → Prop} [inst : DecidablePred p] {s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.Model.MatchesAt p pos ↔ String.Slice.Pattern.Model.MatchesAt (fun x => decide (p x)) pos
-- Init.Sym.Simp.SimprocDSL
/-- Try `a`, if no progress try `b`.  -/
Lean.Parser.Sym.Simp.orElse : Lean.TrailingParserDescr
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getD_insertIfNew : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {k a : α}
  {fallback : β a} {v : β k},
  (m.insertIfNew k v).getD a fallback = if h : (k == a) = true ∧ k ∉ m then cast ⋯ v else m.getD a fallback
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
/-- If the union of disjoint measurable sets has finite measure, then there are only
finitely many members of the union whose measure exceeds any given positive number.  -/
MeasureTheory.Measure.finite_const_le_meas_of_disjoint_iUnion : ∀ {α : Type u_1} {ι : Type u_4} [inst : MeasurableSpace α] (μ : MeasureTheory.Measure α) {ε : ENNReal},
  0 < ε →
    ∀ {As : ι → Set α},
      (∀ (i : ι), MeasurableSet (As i)) →
        Pairwise (Function.onFun Disjoint As) → μ (⋃ i, As i) ≠ ⊤ → {i | ε ≤ μ (As i)}.Finite
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.mapIso_functor_obj_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T T' : D} {S : CategoryTheory.Functor C D} (i : T ≅ T')
  (X : CategoryTheory.Comma S (CategoryTheory.Functor.fromPUnit T)),
  ((CategoryTheory.CostructuredArrow.mapIso i).functor.obj X).left = X.left
-- Lean.Parser.Term.Basic
Lean.Parser.Tactic.tacticSeq1Indented.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Data.Num.Lemmas
_private.Mathlib.Data.Num.Lemmas.0.PosNum.pred'.match_1.eq_2 : ∀ (motive : PosNum → Sort u_1) (n : PosNum) (h_1 : Unit → motive PosNum.one) (h_2 : (n : PosNum) → motive n.bit0)
  (h_3 : (n : PosNum) → motive n.bit1),
  (match n.bit0 with
    | PosNum.one => h_1 ()
    | n.bit0 => h_2 n
    | n.bit1 => h_3 n) =
    h_2 n
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.eq_C_of_degree_le_zero : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.degree ≤ 0 → p = Polynomial.C (p.coeff 0)
-- Mathlib.Algebra.Order.Monoid.Lex
AddMonoidHom.snd_mono : ∀ {α : Type u_1} {β : Type u_2} [inst : AddMonoid α] [inst_1 : Preorder α] [inst_2 : AddMonoid β] [inst_3 : Preorder β],
  Monotone ⇑(AddMonoidHom.snd α β)
-- Mathlib.CategoryTheory.Localization.Monoidal.Basic
CategoryTheory.Localization.Monoidal.associator_naturality : ∀ {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] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : W.IsMonoidal]
  [inst_4 : L.IsLocalization W] {unit : D} (ε : L.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ unit)
  {X₁ X₂ X₃ Y₁ Y₂ Y₃ : CategoryTheory.LocalizedMonoidal L W ε} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.tensorHom f₁ f₂) f₃)
      (CategoryTheory.MonoidalCategoryStruct.associator Y₁ Y₂ Y₃).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X₁ X₂ X₃).hom
      (CategoryTheory.MonoidalCategoryStruct.tensorHom f₁ (CategoryTheory.MonoidalCategoryStruct.tensorHom f₂ f₃))
-- Mathlib.Tactic.FunProp.ToBatteries
_private.Mathlib.Tactic.FunProp.ToBatteries.0.Mathlib.Meta.FunProp.betaThroughLetAux.match_1.eq_2 : ∀ (motive : Lean.Expr → List Lean.Expr → Sort u_1) (binderName : Lean.Name) (binderType b : Lean.Expr)
  (binderInfo : Lean.BinderInfo) (a : Lean.Expr) (as : List Lean.Expr) (h_1 : (f : Lean.Expr) → motive f [])
  (h_2 :
    (binderName : Lean.Name) →
      (binderType b : Lean.Expr) →
        (binderInfo : Lean.BinderInfo) →
          (a : Lean.Expr) → (as : List Lean.Expr) → motive (Lean.Expr.lam binderName binderType b binderInfo) (a :: as))
  (h_3 :
    (n : Lean.Name) →
      (t v b : Lean.Expr) → (nondep : Bool) → (args : List Lean.Expr) → motive (Lean.Expr.letE n t v b nondep) args)
  (h_4 : (data : Lean.MData) → (b : Lean.Expr) → (args : List Lean.Expr) → motive (Lean.Expr.mdata data b) args)
  (h_5 : (f : Lean.Expr) → (args : List Lean.Expr) → motive f args),
  (match Lean.Expr.lam binderName binderType b binderInfo, a :: as with
    | f, [] => h_1 f
    | Lean.Expr.lam binderName binderType b binderInfo, a :: as => h_2 binderName binderType b binderInfo a as
    | Lean.Expr.letE n t v b nondep, args => h_3 n t v b nondep args
    | Lean.Expr.mdata data b, args => h_4 data b args
    | f, args => h_5 f args) =
    h_2 binderName binderType b binderInfo a as
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.algebraMap_right_apply : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] {S : Type u_3} [inst_1 : CommSemiring R]
  [inst_2 : Ring S] [inst_3 : Algebra R S] (v : Valuation S Γ₀) (r : R),
  (algebraMap R (WithVal v)) r = WithVal.toVal v ((algebraMap R S) r)
-- Mathlib.Topology.Maps.Basic
IsOpenMap.map_nhdsSet_eq : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  IsOpenMap f → Continuous f → ∀ (s : Set X), Filter.map f (nhdsSet s) = nhdsSet (f '' s)
-- Mathlib.Data.PFun
PFun.fix.match_1.congr_eq_1 : ∀ {α : Type u_2} {β : Type u_1} (motive : β ⊕ α → Sort u_3) (x : β ⊕ α)
  (h_1 : (b : β) → x = Sum.inl b → motive (Sum.inl b)) (h_2 : (a' : α) → x = Sum.inr a' → motive (Sum.inr a')) (b : β)
  (heq_1 : x = Sum.inl b),
  (match e : x with
    | Sum.inl b => h_1 b e
    | Sum.inr a' => h_2 a' e) ≍
    h_1 b heq_1
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
/-- The distance function (given an ambient metric space on `α`), which returns
a nonnegative real number `dist x y` given `x y : α`.  -/
Dist : Type u_3 → Type u_3
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable
/-- A sequential limit of measurable functions valued in a (pseudo) metrizable space is
measurable.  -/
measurable_of_tendsto_metrizable : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace β]
  [TopologicalSpace.PseudoMetrizableSpace β] [inst_3 : MeasurableSpace β] [BorelSpace β] {f : ℕ → α → β} {g : α → β},
  (∀ (i : ℕ), Measurable (f i)) → Filter.Tendsto f Filter.atTop (nhds g) → Measurable g
-- Lean.Meta.Sym.Arith.Types
Lean.Meta.Sym.Arith.Ring.subFn? : Lean.Meta.Sym.Arith.Ring → Option Lean.Expr
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instMul.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Mul β]
  [inst_3 : ContinuousMul β], ContinuousMap.instMul = { mul := fun f g => { toFun := ⇑f * ⇑g, continuous_toFun := ⋯ } }
-- Mathlib.Topology.Algebra.Monoid
continuous_finsetSum : ∀ {ι : Type u_1} {M : Type u_3} {X : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace M]
  [inst_2 : AddCommMonoid M] [ContinuousAdd M] {f : ι → X → M} (s : Finset ι),
  (∀ i ∈ s, Continuous (f i)) → Continuous fun a => ∑ i ∈ s, f i a
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
/-- On square matrices, `mul_right_comm` applies under `det`.  -/
Matrix.det_mul_right_comm : ∀ {m : Type u_1} [inst : DecidableEq m] [inst_1 : Fintype m] {R : Type v} [inst_2 : CommRing R] (M N P : Matrix m m R),
  (M * N * P).det = (M * P * N).det
-- Mathlib.Data.ENNReal.Inv
ENNReal.lt_div_iff_mul_lt : ∀ {a b c : ENNReal}, b ≠ 0 ∨ c ≠ ⊤ → b ≠ ⊤ ∨ c ≠ 0 → (c < a / b ↔ c * b < a)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
Nonneg.instNonUnitalContinuousFunctionalCalculus : ∀ {A : Type u_1} [inst : NonUnitalRing A] [inst_1 : PartialOrder A] [inst_2 : StarRing A] [StarOrderedRing A]
  [inst_4 : TopologicalSpace A] [inst_5 : Module ℝ A] [inst_6 : IsScalarTower ℝ A A] [inst_7 : SMulCommClass ℝ A A]
  [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A],
  NonUnitalContinuousFunctionalCalculus NNReal A fun x => 0 ≤ x
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Mathlib.Meta.NormNum.IsNat.nnreal_rpow_isNNRat : ∀ {a : NNReal} {b : ℝ} {m n d r : ℕ},
  Mathlib.Meta.NormNum.IsNat a m →
    Mathlib.Meta.NormNum.IsNNRat b n d →
      ∀ (k : ℕ), r ^ d = k → ∀ (l : ℕ), m ^ n = l → k = l → Mathlib.Meta.NormNum.IsNat (a ^ b) r
-- Mathlib.Order.BooleanAlgebra.Set
Set.compl_subset_compl : ∀ {α : Type u_1} {s t : Set α}, sᶜ ⊆ tᶜ ↔ t ⊆ s
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.Rel.below.zero_add : ∀ {R : Type u_1} {X : Type u_2} [inst : CommSemiring R]
  {motive : (a a_1 : FreeAlgebra.Pre R X) → FreeAlgebra.Rel R X a a_1 → Prop} {a : FreeAlgebra.Pre R X},
  FreeAlgebra.Rel.below ⋯
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps
/-- Given a homotopy H : f ∼ g, we have an associated natural isomorphism between the induced
functors `map f` and `map g` on fundamental groupoids.  -/
FundamentalGroupoidFunctor.homotopicMapsNatIso : {X : Type u_1} →
  {Y : Type u_2} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] →
        {f g : C(X, Y)} → f.Homotopy g → (FundamentalGroupoid.map f ⟶ FundamentalGroupoid.map g)
-- Aesop.Forward.State
Aesop.instToMessageDataRawHyp : Lean.ToMessageData Aesop.RawHyp
-- Std.Time.DateTime
Std.Time.DateTime.instHAddOffset : HAdd Std.Time.DateTime Std.Time.Day.Offset Std.Time.DateTime
-- Mathlib.Analysis.Calculus.FDeriv.Mul
DifferentiableOn.inv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {R : Type u_5} [inst_3 : NormedDivisionRing R] [inst_4 : NormedAlgebra 𝕜 R] {h : E → R}
  {S : Set E}, DifferentiableOn 𝕜 h S → (∀ x ∈ S, h x ≠ 0) → DifferentiableOn 𝕜 h⁻¹ S
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Pullback
PresheafOfModules.pullbackObjIsDefined_free_yoneda : ∀ {C D : Type u} [inst : CategoryTheory.SmallCategory C] [inst_1 : CategoryTheory.SmallCategory D]
  {F : CategoryTheory.Functor C D} {R : CategoryTheory.Functor Dᵒᵖ RingCat} {S : CategoryTheory.Functor Cᵒᵖ RingCat}
  (φ : S ⟶ F.op.comp R) (X : C),
  PresheafOfModules.pullbackObjIsDefined φ ((PresheafOfModules.free S).obj (CategoryTheory.yoneda.obj X))
-- Mathlib.Algebra.Polynomial.UnitTrinomial
Polynomial.IsUnitTrinomial.irreducible_aux3 : ∀ {p q : Polynomial ℤ} {k m m' n : ℕ},
  k < m →
    m < n →
      k < m' →
        m' < n →
          ∀ (u v w x z : ℤˣ),
            p = Polynomial.trinomial k m n ↑u ↑v ↑w →
              q = Polynomial.trinomial k m' n ↑x ↑v ↑z → p * p.mirror = q * q.mirror → q = p ∨ q = p.mirror
-- Mathlib.Algebra.Field.Periodic
Function.Antiperiodic.sub_nat_mul_eq : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c x : α} [inst : NonAssocRing α] [inst_1 : Ring β],
  Function.Antiperiodic f c → ∀ (n : ℕ), f (x - ↑n * c) = (-1) ^ n * f x
-- Mathlib.Topology.Algebra.Group.GroupTopology
AddGroupTopology.toTopologicalSpace : {α : Type u} → [inst : AddGroup α] → AddGroupTopology α → TopologicalSpace α
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instAddCommMagmaOfAddHomClass : {ι : Type u_2} →
  [inst : Preorder ι] →
    {G : ι → Type u_3} →
      {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} →
        {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} →
          [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] →
            [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] →
              [inst_3 : IsDirectedOrder ι] →
                [inst_4 : (i : ι) → AddCommMagma (G i)] →
                  [∀ (i j : ι) (h : i ≤ j), AddHomClass (T h) (G i) (G j)] → AddCommMagma (DirectLimit G f)
-- Mathlib.Tactic.Positivity.Basic
/-- Extension for `Nat.lcm`.  -/
Mathlib.Meta.Positivity.evalNatLCM : Mathlib.Meta.Positivity.PositivityExt