mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.Module.PositiveLinearMap
PositiveLinearMap.nsmul_apply : ∀ {R : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid E₁]
  [inst_2 : PartialOrder E₁] [inst_3 : AddCommMonoid E₂] [inst_4 : PartialOrder E₂] [inst_5 : Module R E₁]
  [inst_6 : Module R E₂] [inst_7 : IsOrderedAddMonoid E₂] (f : E₁ →ₚ[R] E₂) (n : ℕ) (x : E₁), (n • f) x = n • f x
-- Mathlib.NumberTheory.Harmonic.ZetaAsymp
riemannZeta_eq_inv_sub_mul : ∀ {s : ℂ}, s ≠ 1 → riemannZeta s = (s - 1)⁻¹ * riemannZeta₁ s
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
/-- Radon-Nikodym derivative of the scalar multiple of a measure.
See also `rnDeriv_smul_left_of_ne_top'`, which requires sigma-finite `ν` and `μ`.  -/
MeasureTheory.Measure.rnDeriv_smul_left_of_ne_top : ∀ {α : Type u_1} {m : MeasurableSpace α} (ν μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure ν]
  [ν.HaveLebesgueDecomposition μ] {r : ENNReal}, r ≠ ⊤ → (r • ν).rnDeriv μ =ᵐ[μ] r • ν.rnDeriv μ
-- Mathlib.Analysis.Calculus.LineDeriv.Measurable
measurable_lineDeriv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [LocallyCompactSpace 𝕜] {E : Type u_2}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] [inst_4 : MeasurableSpace E] [OpensMeasurableSpace E]
  {F : Type u_3} [inst_6 : NormedAddCommGroup F] [inst_7 : NormedSpace 𝕜 F] [CompleteSpace F] {f : E → F} {v : E}
  [inst_9 : MeasurableSpace F] [BorelSpace F], Continuous f → Measurable fun x => lineDeriv 𝕜 f x v
-- Mathlib.CategoryTheory.Functor.FullyFaithful
CategoryTheory.Functor.map_injective : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {X Y : C} (F : CategoryTheory.Functor C D) [F.Faithful], Function.Injective F.map
-- Mathlib.Combinatorics.Young.YoungDiagram
YoungDiagram.cellsOfRowLens.eq_1 : YoungDiagram.cellsOfRowLens [] = ∅
-- Mathlib.CategoryTheory.Subterminal
CategoryTheory.subterminals_thin : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (X Y : CategoryTheory.Subterminals C), Subsingleton (X ⟶ Y)
-- Mathlib.Algebra.MvPolynomial.Basic
/-- Similar to `MvPolynomial.induction_on` but only a weak form of `h_add` is required.
In particular, this version only requires us to show
that `motive` is closed under addition of nontrivial monomials not present in the support.
 -/
MvPolynomial.monomial_add_induction_on : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {motive : MvPolynomial σ R → Prop} (p : MvPolynomial σ R),
  (∀ (a : R), motive (MvPolynomial.C a)) →
    (∀ (a : σ →₀ ℕ) (b : R) (f : MvPolynomial σ R),
        a ∉ f.coeff.support → b ≠ 0 → motive f → motive ((MvPolynomial.monomial a) b + f)) →
      motive p
-- Mathlib.Logic.Embedding.Basic
/-- Convert an `α ≃ β` to `α ↪ β`.

This is also available as a coercion `Equiv.coeEmbedding`.
The explicit `Equiv.toEmbedding` version is preferred though, since the coercion can have issues
inferring the type of the resulting embedding. For example:

```lean
-- Works:
example (s : Finset (Fin 3)) (f : Equiv.Perm (Fin 3)) : s.map f.toEmbedding = s.map f := by simp
-- Error, `f` has type `Fin 3 ≃ Fin 3` but is expected to have type `Fin 3 ↪ ?m_1 : Type ?`
example (s : Finset (Fin 3)) (f : Equiv.Perm (Fin 3)) : s.map f = s.map f.toEmbedding := by simp
```
 -/
Equiv.toEmbedding : {α : Sort u} → {β : Sort v} → α ≃ β → α ↪ β
-- Init.Data.UInt.Lemmas
UInt16.toUInt32_eq_mod_65536_iff : ∀ (a : UInt16) (b : UInt32), a.toUInt32 = b % 65536 ↔ a = b.toUInt16
-- Mathlib.Data.Set.Basic
Set.eq_empty_or_nonempty : ∀ {α : Type u} (s : Set α), s = ∅ ∨ s.Nonempty
-- Mathlib.Algebra.Group.End
Equiv.neg_addLeft : ∀ {α : Type u_4} [inst : AddGroup α] (a : α), (Equiv.addLeft a)⁻¹ = Equiv.addLeft (-a)
-- Init.Data.Array.Lemmas
Array.isEmpty_iff : ∀ {α : Type u_1} {xs : Array α}, xs.isEmpty = true ↔ xs = #[]
-- Mathlib.RingTheory.EssentialFiniteness
Algebra.EssFiniteType.comp_iff : ∀ (R : Type u_1) (S : Type u_2) (T : Type u_3) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [IsScalarTower R S T]
  [Algebra.EssFiniteType R S], Algebra.EssFiniteType R T ↔ Algebra.EssFiniteType S T
-- Mathlib.MeasureTheory.SetSemiring
/-- **Alias** of `MeasureTheory.IsSetSemiring.exists_disjoint_finset_sdiff_eq`.

---

In a semiring of sets `C`, for all set `s ∈ C` and finite set of sets `I ⊆ C`, there is a
finite set of sets in `C` whose union is `s \ ⋃₀ I`.
See `IsSetSemiring.disjointOfDiffUnion` for a definition that gives such a set.  -/
MeasureTheory.IsSetSemiring.exists_disjoint_finset_diff_eq : ∀ {α : Type u_1} {C : Set (Set α)} {s : Set α} {I : Finset (Set α)},
  MeasureTheory.IsSetSemiring C → s ∈ C → ↑I ⊆ C → ∃ J, ↑J ⊆ C ∧ (↑J).PairwiseDisjoint id ∧ s \ ⋃₀ ↑I = ⋃₀ ↑J
-- Mathlib.Order.Northcott
/-- A function `h : α → β` is Northcott if the sets `{a : α | h a ≤ b}` are all finite.  -/
Northcott : {α : Type u_1} → {β : Type u_2} → (α → β) → [LE β] → Prop
-- Mathlib.Data.Finset.Disjoint
Finset.disjoint_iff_ne : ∀ {α : Type u_2} {s t : Finset α}, Disjoint s t ↔ ∀ a ∈ s, ∀ b ∈ t, a ≠ b
-- Mathlib.RingTheory.Polynomial.Content
Polynomial.gcd_content_eq_of_dvd_sub : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : NormalizedGCDMonoid R] {a : R} {p q : Polynomial R},
  Polynomial.C a ∣ p - q → gcd a p.content = gcd a q.content
-- Mathlib.NumberTheory.LSeries.HurwitzZetaEven
/-- If `s` is not of the form `1 - n` for `n ∈ ℕ`, then `cosZeta a (1 - s)` is an explicit
multiple of `hurwitzZetaEven s`.  -/
HurwitzZeta.cosZeta_one_sub : ∀ (a : UnitAddCircle) {s : ℂ},
  (∀ (n : ℕ), s ≠ 1 - ↑n) →
    HurwitzZeta.cosZeta a (1 - s) =
      2 * (2 * ↑Real.pi) ^ (-s) * Complex.Gamma s * Complex.cos (↑Real.pi * s / 2) * HurwitzZeta.hurwitzZetaEven a s
-- Mathlib.Order.SuccPred.LinearLocallyFinite
toZ_of_ge : ∀ {ι : Type u_1} [inst : LinearOrder ι] [inst_1 : SuccOrder ι] [inst_2 : IsSuccArchimedean ι] [inst_3 : PredOrder ι]
  {i0 i : ι} (hi : i0 ≤ i), toZ i0 i = ↑(Nat.find ⋯)
-- Mathlib.Topology.OpenPartialHomeomorph.Continuity
/-- An open partial homeomorphism inverse is continuous at any point of its target  -/
OpenPartialHomeomorph.continuousAt_symm : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y) {x : Y}, x ∈ e.target → ContinuousAt (↑e.symm) x
-- Lean.Data.Json.FromToJson.Basic
Lean.instFromJsonBool : Lean.FromJson Bool
-- Mathlib.GroupTheory.Exponent
AddOpposite.exponent : ∀ {G : Type u} [inst : AddMonoid G], AddMonoid.exponent Gᵃᵒᵖ = AddMonoid.exponent G
-- Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Complete
CategoryTheory.Functor.instComonadicLeftAdjointDiscreteObjWhiskeringLeftIncl : (I : Type u₂) →
  [inst : CategoryTheory.Category.{v₂, u₂} I] →
    (C : Type u₁) →
      [inst_1 : CategoryTheory.Category.{v₁, u₁} C] →
        [∀ (F : CategoryTheory.Functor (CategoryTheory.Discrete I) C),
              (CategoryTheory.Discrete.functor id).HasRightKanExtension F] →
          [CategoryTheory.Limits.HasLimitsOfShape CategoryTheory.Limits.WalkingParallelPair C] →
            CategoryTheory.ComonadicLeftAdjoint
              ((CategoryTheory.Functor.whiskeringLeft (CategoryTheory.Discrete I) I C).obj
                (CategoryTheory.Functor.incl✝ I))
-- Mathlib.RingTheory.Bialgebra.Equiv
BialgEquiv.congr_fun : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B]
  {e e' : A ≃ₐc[R] B}, e = e' → ∀ (x : A), e x = e' x
-- Mathlib.Combinatorics.Enumerative.Composition
CompositionAsSet.mk : {n : ℕ} → (boundaries : Finset (Fin n.succ)) → 0 ∈ boundaries → Fin.last n ∈ boundaries → CompositionAsSet n
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKey?_insertEntry_of_isEmpty : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] {k : α} {v : β k}
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    l.isEmpty = true → Std.Internal.List.minKey? (Std.Internal.List.insertEntry k v l) = some k
-- Lean.Meta.Tactic.Grind.Types
_private.Lean.Meta.Tactic.Grind.Types.0.Lean.Meta.Grind.PendingSolverPropagationsData.eq.injEq : ∀ (solverId : ℕ) (lhs rhs : Lean.Expr) (rest : Lean.Meta.Grind.PendingSolverPropagationsData✝) (solverId_1 : ℕ)
  (lhs_1 rhs_1 : Lean.Expr) (rest_1 : Lean.Meta.Grind.PendingSolverPropagationsData✝),
  (Lean.Meta.Grind.PendingSolverPropagationsData.eq✝ solverId lhs rhs rest =
      Lean.Meta.Grind.PendingSolverPropagationsData.eq✝ solverId_1 lhs_1 rhs_1 rest_1) =
    (solverId = solverId_1 ∧ lhs = lhs_1 ∧ rhs = rhs_1 ∧ rest = rest_1)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonCompletionItemTag : Lean.FromJson Lean.Lsp.CompletionItemTag
-- Mathlib.Data.Sum.Basic
/-- The map from the third summand into a ternary sum.  -/
Sum3.in₂ : {α : Type u} → {β : Type v} → {γ : Type u_1} → γ → α ⊕ β ⊕ γ
-- Mathlib.RingTheory.TensorProduct.IsBaseChangeHom
IsBaseChange.det_endHom : ∀ {R : Type u_6} [inst : CommRing R] (S : Type u_7) [inst_1 : CommRing S] [inst_2 : Algebra R S] (M : Type u_8)
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] {P : Type u_9} [inst_5 : AddCommGroup P] [inst_6 : Module R P]
  [inst_7 : Module S P] [inst_8 : IsScalarTower R S P] [Module.Free R M] [Module.Finite R M] {α : M →ₗ[R] P}
  (j : IsBaseChange S α) (f : M →ₗ[R] M), LinearMap.det (j.endHom f) = (algebraMap R S) (LinearMap.det f)
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.coconeOfIsLeftKanExtension_ι : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  (F' : CategoryTheory.Functor D H) {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H}
  (α : F ⟶ L.comp F') [inst_3 : F'.IsLeftKanExtension α] (c : CategoryTheory.Limits.Cocone F),
  (F'.coconeOfIsLeftKanExtension α c).ι = F'.descOfIsLeftKanExtension α ((CategoryTheory.Functor.const D).obj c.pt) c.ι
-- Mathlib.Algebra.AddConstMap.Equiv
/-- Projection from `G ≃+c[a, a] G` to permutations `G ≃ G`, as a monoid homomorphism.  -/
AddConstEquiv.toPerm : {G : Type u_1} → [inst : Add G] → {a : G} → AddConstEquiv G G a a →* Equiv.Perm G
-- Std.Data.HashSet.Lemmas
Std.HashSet.get!_inter_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α]
  [inst : Inhabited α] {k : α}, k ∉ m₁ → (m₁ ∩ m₂).get! k = default
-- Init.Data.List.ToArray
List.foldl_toArray : ∀ {β : Type u_1} {α : Type u_2} (f : β → α → β) (init : β) (l : List α),
  Array.foldl f init l.toArray = List.foldl f init l
-- Lean.ReducibilityAttrs
Lean.ReducibilityStatus.implicitReducible : Lean.ReducibilityStatus
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
/-- More flexible variant of `mapId`. (See the file `Bicategory.Functor.Strict`
for applications to strict bicategories.)  -/
CategoryTheory.Pseudofunctor.mapId' : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        (F : CategoryTheory.Pseudofunctor B C) →
          {b : B} →
            (f : b ⟶ b) →
              autoParam (f = CategoryTheory.CategoryStruct.id b) CategoryTheory.Pseudofunctor.mapId'._auto_1 →
                (F.map f ≅ CategoryTheory.CategoryStruct.id (F.obj b))
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKey_eq_maxKeyD : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {he : t.isEmpty = false} {fallback : α}, t.maxKey he = t.maxKeyD fallback
-- Mathlib.Analysis.Calculus.FormalMultilinearSeries
FormalMultilinearSeries.apply_eq_prod_smul_coeff : ∀ {𝕜 : Type u} {E : Type v} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {p : FormalMultilinearSeries 𝕜 𝕜 E} {n : ℕ} {y : Fin n → 𝕜},
  (p n) y = (∏ i, y i) • p.coeff n
-- Mathlib.CategoryTheory.Sites.Sheafification
CategoryTheory.sheafifyMap_sheafifyLift : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] [inst_2 : CategoryTheory.HasWeakSheafify J D]
  {P Q R : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) (γ : Q ⟶ R) (hR : CategoryTheory.Presheaf.IsSheaf J R),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.sheafifyMap J η) (CategoryTheory.sheafifyLift J γ hR) =
    CategoryTheory.sheafifyLift J (CategoryTheory.CategoryStruct.comp η γ) hR
-- Mathlib.NumberTheory.Height.Basic
/-- The logarithmic height of the pointwise negative of a tuple
equals its logarithmic height.  -/
Height.logHeight_neg : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] {ι : Type u_2} (x : ι → K),
  Height.logHeight (-x) = Height.logHeight x
-- Mathlib.CategoryTheory.Comma.LocallySmall
CategoryTheory.CostructuredArrow.locallySmall : ∀ {A : Type u₁} {T : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₃, u₃} T]
  (S : CategoryTheory.Functor A T) (X : T) [CategoryTheory.LocallySmall.{w, v₁, u₁} A],
  CategoryTheory.LocallySmall.{w, v₁, max u₁ v₃} (CategoryTheory.CostructuredArrow S X)
-- Mathlib.Order.Filter.EventuallyConst
Filter.HasBasis.eventuallyConst_iff' : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} {f : α → β} {ι : Sort u_5} {p : ι → Prop} {s : ι → Set α} {x : ι → α},
  l.HasBasis p s → (∀ (i : ι), p i → x i ∈ s i) → (Filter.EventuallyConst f l ↔ ∃ i, p i ∧ ∀ y ∈ s i, f y = f (x i))
-- Mathlib.Topology.MetricSpace.Dilation
Dilation.ratio.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {F : Type u_4} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β]
  [inst_2 : FunLike F α β] [inst_3 : DilationClass F α β] (f : F),
  Dilation.ratio f = if ∀ (x y : α), edist x y = 0 ∨ edist x y = ⊤ then 1 else ⋯.choose
-- Lean.Declaration
Lean.ConstantInfo.isCtor : Lean.ConstantInfo → Bool
-- Mathlib.FieldTheory.RatFunc.Valuation
RatFunc.instIsTrivialOnWithZeroMultiplicativeIntInftyValuation : ∀ (F : Type u_1) [inst : Field F] [inst_1 : DecidableEq (RatFunc F)], Valuation.IsTrivialOn F (RatFunc.inftyValuation F)
-- Mathlib.FieldTheory.KummerExtension
adjoinRootXPowSubCEquiv.congr_simp : ∀ {K : Type u} [inst : Field K] {n : ℕ} {a : K} {L : Type u_1} [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : Polynomial.IsSplittingField K L (Polynomial.X ^ n - Polynomial.C a)] {α α_1 : L} (e_α : α = α_1)
  (hζ : (primitiveRoots n K).Nonempty) (H : Irreducible (Polynomial.X ^ n - Polynomial.C a))
  (hα : α ^ n = (algebraMap K L) a), adjoinRootXPowSubCEquiv hζ H hα = adjoinRootXPowSubCEquiv hζ H ⋯
-- Mathlib.Order.Irreducible
supIrred_toDual : ∀ {α : Type u_2} [inst : SemilatticeInf α] {a : α}, SupIrred (OrderDual.toDual a) ↔ InfIrred a
-- Mathlib.Logic.Equiv.Defs
Equiv.trans_eq_refl_iff_symm_eq : ∀ {α : Sort u} {β : Sort v} {f : α ≃ β} {g : β ≃ α}, f.trans g = Equiv.refl α ↔ f.symm = g
-- Lean.Elab.Do.Basic
Lean.Elab.Do.getBreakCont : Lean.Elab.Do.DoElabM (Option (Lean.Elab.Do.DoElabM Lean.Expr))
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.coyonedaEquiv_naturality : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {F : CategoryTheory.Functor C (Type v₁)}
  (f : CategoryTheory.coyoneda.obj (Opposite.op X) ⟶ F) (g : X ⟶ Y),
  (CategoryTheory.ConcreteCategory.hom (F.map g)) (CategoryTheory.coyonedaEquiv f) =
    CategoryTheory.coyonedaEquiv (CategoryTheory.CategoryStruct.comp (CategoryTheory.coyoneda.map g.op) f)
-- Lean.Syntax
Lean.Syntax.TopDown.mk.inj : ∀ {firstChoiceOnly : Bool} {stx : Lean.Syntax} {firstChoiceOnly_1 : Bool} {stx_1 : Lean.Syntax},
  { firstChoiceOnly := firstChoiceOnly, stx := stx } = { firstChoiceOnly := firstChoiceOnly_1, stx := stx_1 } →
    firstChoiceOnly = firstChoiceOnly_1 ∧ stx = stx_1
-- Mathlib.LinearAlgebra.RootSystem.RootPositive
RootPairing.RootPositiveForm.rootLength.congr_simp : ∀ {ι : Type u_1} {R : Type u_2} {S : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing S]
  [inst_1 : LinearOrder S] [inst_2 : CommRing R] [inst_3 : Algebra S R] [inst_4 : AddCommGroup M] [inst_5 : Module R M]
  [inst_6 : AddCommGroup N] [inst_7 : Module R N] {P : RootPairing ι R M N} [inst_8 : P.IsValuedIn S]
  (B B_1 : RootPairing.RootPositiveForm S P),
  B = B_1 →
    ∀ [inst_9 : FaithfulSMul S R] [inst_10 : Module S M] [inst_11 : IsScalarTower S R M] (i i_1 : ι),
      i = i_1 → B.rootLength i = B_1.rootLength i_1
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getEntry_eq_getEntryₘ : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (l : Std.DTreeMap.Internal.Impl α β) {h : k ∈ l}
  (h' : (l.getEntry?ₘ k).isSome = true), l.getEntry k h = l.getEntryₘ k h'
-- Mathlib.Combinatorics.SimpleGraph.Sum
SimpleGraph.neighborSet_sum_inl : ∀ {V : Type u_3} {W : Type u_5} {G : SimpleGraph V} {H : SimpleGraph W} (v : V),
  (G ⊕g H).neighborSet (Sum.inl v) = Sum.inl '' G.neighborSet v
-- Mathlib.RingTheory.Regular.RegularSequence
LinearEquiv.isWeaklyRegular_congr : ∀ {R : Type u_1} {M : Type u_3} {M₂ : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂] (e : M ≃ₗ[R] M₂) (rs : List R),
  RingTheory.Sequence.IsWeaklyRegular M rs ↔ RingTheory.Sequence.IsWeaklyRegular M₂ rs
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.ExcenterExists.excenter_notMem_affineSpan_face : ∀ {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} {signs : Finset (Fin (n + 1))},
  s.ExcenterExists signs →
    ∀ {fs : Finset (Fin (n + 1))} {m : ℕ} (hfs : fs.card = m + 1),
      m ≠ n → s.excenter signs ∉ affineSpan ℝ (Set.range (s.face hfs).points)
-- Mathlib.Order.Category.Frm
Frm.instInhabited : Inhabited Frm
-- Mathlib.Analysis.Calculus.FDeriv.Const
/-- If `f : E → F` has injective differential at `x`, it is differentiable at `x`.  -/
differentiableAt_of_fderiv_injective : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {x : E}, Function.Injective ⇑(fderiv 𝕜 f x) → DifferentiableAt 𝕜 f x
-- Aesop.Script.CtorNames
Aesop.CtorNames.mk : Lean.Name → Array Lean.Name → Bool → Aesop.CtorNames
-- Lean.Elab.Quotation.Precheck
Lean.Elab.Term.Quotation.runPrecheck : Lean.Syntax → Lean.Elab.TermElabM Unit
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
/-- The complement sequence `Wᶜ : ℤ × ℤ → R` for a normalised EDS `W : ℤ → R` that witnesses
`W(k) ∣ W(n * k)`. In other words, `W(k) * Wᶜ(k, n) = W(n * k)` for all `k, n ∈ ℤ`.

This extends `complEDS'` by defining its values at negative integers.  -/
complEDS : {R : Type u_1} → [CommRing R] → R → R → R → ℤ → ℤ → R
-- Mathlib.Analysis.Analytic.Basic
/-- If a function admits a power series expansion, then it is exponentially close to the partial
sums of this power series on strict subdisks of the disk of convergence.  -/
HasFPowerSeriesOnBall.uniform_geometric_approx : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} {r' : NNReal},
  HasFPowerSeriesOnBall f p x r →
    ↑r' < r → ∃ a ∈ Set.Ioo 0 1, ∃ C > 0, ∀ y ∈ Metric.ball 0 ↑r', ∀ (n : ℕ), ‖f (x + y) - p.partialSum n y‖ ≤ C * a ^ n
-- Mathlib.CategoryTheory.Category.Basic
CategoryTheory.comp_dite : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : Prop} [inst_1 : Decidable P] {X Y Z : C} (f : X ⟶ Y)
  (g : P → (Y ⟶ Z)) (g' : ¬P → (Y ⟶ Z)),
  CategoryTheory.CategoryStruct.comp f (if h : P then g h else g' h) =
    if h : P then CategoryTheory.CategoryStruct.comp f (g h) else CategoryTheory.CategoryStruct.comp f (g' h)
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Submonoid.IsLocalizationMap.map_one : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {F : Type u_4}
  [inst_2 : FunLike F M N] [MulHomClass F M N] {f : F}, S.IsLocalizationMap ⇑f → f 1 = 1
-- Init.Data.SInt.Basic
/-- Converts a natural number to a 16-bit signed integer, wrapping around on overflow.

This function is overridden at runtime with an efficient implementation.

Examples:
* `Int16.ofNat 127 = 127`
* `Int16.ofNat 32767 = 32767`
* `Int16.ofNat 32768 = -32768`
* `Int16.ofNat 32770 = -32766`
 -/
Int16.ofNat : ℕ → Int16
-- Mathlib.Analysis.LocallyConvex.WeakDual
LinearMap.hasBasis_weakBilin : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : AddCommGroup F] [inst_4 : Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜),
  (nhds 0).HasBasis (fun x => x ∈ B.toSeminormFamily.basisSets) id
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.MonoidalCategory.tensorδ_tensorμ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X₁ X₂ Y₁ Y₂ : C),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorδ X₁ X₂ Y₁ Y₂)
      (CategoryTheory.MonoidalCategory.tensorμ X₁ X₂ Y₁ Y₂) =
    CategoryTheory.CategoryStruct.id
      (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ Y₁)
        (CategoryTheory.MonoidalCategoryStruct.tensorObj X₂ Y₂))
-- Mathlib.Algebra.GroupWithZero.Associated
Irreducible.associated_of_dvd : ∀ {M : Type u_1} [inst : Monoid M] {p q : M}, Irreducible p → Irreducible q → p ∣ q → Associated p q
-- Batteries.Data.MLList.Basic
_private.Batteries.Data.MLList.Basic.0.MLList.Spec.mk.inj : ∀ {m listM : Type u → Type u} {nil : {α : Type u} → listM α} {cons : {α : Type u} → α → listM α → listM α}
  {thunk : {α : Type u} → (Unit → listM α) → listM α} {squash : {α : Type u} → (Unit → m (listM α)) → listM α}
  {uncons : {α : Type u} → [Monad m] → listM α → m (Option (α × listM α))}
  {uncons? : {α : Type u} → listM α → Option (Option (α × listM α))} {listM_1 : Type u → Type u}
  {nil_1 : {α : Type u} → listM_1 α} {cons_1 : {α : Type u} → α → listM_1 α → listM_1 α}
  {thunk_1 : {α : Type u} → (Unit → listM_1 α) → listM_1 α}
  {squash_1 : {α : Type u} → (Unit → m (listM_1 α)) → listM_1 α}
  {uncons_1 : {α : Type u} → [Monad m] → listM_1 α → m (Option (α × listM_1 α))}
  {uncons?_1 : {α : Type u} → listM_1 α → Option (Option (α × listM_1 α))},
  { listM := listM, nil := nil, cons := cons, thunk := thunk, squash := squash, uncons := uncons, uncons? := uncons? } =
      { listM := listM_1, nil := nil_1, cons := cons_1, thunk := thunk_1, squash := squash_1, uncons := uncons_1,
        uncons? := uncons?_1 } →
    listM = listM_1 ∧
      nil ≍ nil_1 ∧ cons ≍ cons_1 ∧ thunk ≍ thunk_1 ∧ squash ≍ squash_1 ∧ uncons ≍ uncons_1 ∧ uncons? ≍ uncons?_1
-- Init.Data.BitVec.Lemmas
BitVec.toFin_smod : ∀ {w : ℕ} {x y : BitVec w},
  (x.smod y).toFin =
    match x.msb, y.msb with
    | false, false => x.toFin % y.toFin
    | false, true => if x % -y = 0#w then 0 else (x % -y + y).toFin
    | true, false => if -x % y = 0#w then 0 else (y - -x % y).toFin
    | true, true => (-(-x % -y)).toFin
-- Init.Data.UInt.Lemmas
UInt64.toUInt8_le : ∀ {a b : UInt64}, a.toUInt8 ≤ b.toUInt8 ↔ a % 256 ≤ b % 256