mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.ModelTheory.Semantics
_private.Mathlib.ModelTheory.Semantics.0.FirstOrder.Language.Term.restrictVarLeft.match_1.splitter : {L : FirstOrder.Language} →
  {α : Type u_4} →
    {β : Type u_6} →
      [inst : DecidableEq α] →
        {γ : Type u_3} →
          (motive : (x : L.Term (α ⊕ γ)) → (↥x.varFinsetLeft → β) → Sort u_5) →
            (x : L.Term (α ⊕ γ)) →
              (x_1 : ↥x.varFinsetLeft → β) →
                ((a : α) →
                    (f : ↥(FirstOrder.Language.var (Sum.inl a)).varFinsetLeft → β) →
                      motive (FirstOrder.Language.var (Sum.inl a)) f) →
                  ((a : γ) →
                      (_f : ↥(FirstOrder.Language.var (Sum.inr a)).varFinsetLeft → β) →
                        motive (FirstOrder.Language.var (Sum.inr a)) _f) →
                    ((l : ℕ) →
                        (F : L.Functions l) →
                          (ts : Fin l → L.Term (α ⊕ γ)) →
                            (f : ↥(FirstOrder.Language.func F ts).varFinsetLeft → β) →
                              motive (FirstOrder.Language.func F ts) f) →
                      motive x x_1
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.closure_iUnion : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] {ι : Sort u_1} (s : ι → Set R),
  NonUnitalSubring.closure (⋃ i, s i) = ⨆ i, NonUnitalSubring.closure (s i)
-- Mathlib.Combinatorics.Additive.SubsetSum
Finset.nonneg_of_mem_subsetSum : ∀ {M : Type u_1} [inst : DecidableEq M] [inst_1 : AddCommMonoid M] {A : Finset M} [inst_2 : LinearOrder M]
  [IsOrderedCancelAddMonoid M], (∀ x ∈ A, 0 ≤ x) → ∀ x ∈ A.subsetSum, 0 ≤ x
-- Mathlib.Order.Antichain
/-- A weak antichain in `Π i, α i` is a set such that no two distinct elements are strongly less
than each other.  -/
IsWeakAntichain : {ι : Type u_1} → {α : ι → Type u_2} → [(i : ι) → Preorder (α i)] → Set ((i : ι) → α i) → Prop
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.invRev_surjective : ∀ {α : Type u}, Function.Surjective FreeGroup.invRev
-- Mathlib.CategoryTheory.Limits.Creates
/-- `F` creates colimits if it creates colimits of shape `J` for any small `J`.  -/
CategoryTheory.CreatesColimitsOfSize : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        CategoryTheory.Functor C D → Type (max (max (max (max (max u₁ u₂) v₁) v₂) (w + 1)) (w' + 1))
-- Mathlib.Dynamics.BirkhoffSum.Basic
birkhoffSum_sub : ∀ {α : Type u_1} {G : Type u_2} [inst : AddCommGroup G] (f : α → α) (g g' : α → G) (n : ℕ) (x : α),
  birkhoffSum f (g - g') n x = birkhoffSum f g n x - birkhoffSum f g' n x
-- Mathlib.Algebra.Group.Units.Defs
IsUnit.val_inv_mul : ∀ {M : Type u_1} [inst : Monoid M] {a : M} (h : IsUnit a), ↑h.unit⁻¹ * a = 1
-- Mathlib.LinearAlgebra.Matrix.SemiringInverse
Matrix.IsDetpBalanced.eq_of_nonsingular : ∀ {n : Type u_1} {R : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommSemiring R] {A : Matrix n n R}
  {a b : R}, A.IsDetpBalanced a b → A.Nonsingular → a = b
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
SubMulAction.ofStabilizer.conjMap_apply : ∀ {G : Type u_1} [inst : Group G] {α : Type u_2} [inst_1 : MulAction G α] {g : G} {a b : α} (hg : b = g • a)
  (x : ↥(SubMulAction.ofStabilizer G a)), ↑((SubMulAction.ofStabilizer.conjMap hg) x) = g • ↑x
-- Init.Data.List.Count
List.count_eq_zero : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a : α} {l : List α}, List.count a l = 0 ↔ a ∉ l
-- Mathlib.Algebra.BigOperators.Fin
/-- **Alias** of `List.alternatingSum_eq_finsetSum`. -/
List.alternatingSum_eq_finset_sum : ∀ {G : Type u_3} [inst : SubtractionCommMonoid G] (L : List G), L.alternatingSum = ∑ i, (-1) ^ ↑i • L[i]
-- Mathlib.Algebra.Algebra.Unitization
Unitization.starMap_inl : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R]
  [inst_2 : NonUnitalSemiring A] [inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : SMulCommClass R A A]
  [inst_6 : IsScalarTower R A A] [inst_7 : NonUnitalSemiring B] [inst_8 : StarRing B] [inst_9 : Module R B]
  [inst_10 : SMulCommClass R B B] [inst_11 : IsScalarTower R B B] [inst_12 : StarModule R B] (φ : A →⋆ₙₐ[R] B) (r : R),
  (Unitization.starMap φ) (Unitization.inl r) = (algebraMap R (Unitization R B)) r
-- Init.Data.BitVec.Lemmas
BitVec.finMk_toNat : ∀ {w : ℕ} (x : BitVec w), ⟨x.toNat, ⋯⟩ = x.toFin
-- Init.Data.Array.Lemmas
Array.any_beq : ∀ {α : Type u_1} [inst : BEq α] {xs : Array α} {a : α}, (xs.any fun x => a == x) = xs.contains a
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
HasSum.of_add_one_of_neg_add_one : ∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M] {m m' : M} [ContinuousAdd M] {f : ℤ → M},
  HasSum (fun n => f (↑n + 1)) m → HasSum (fun n => f (-(↑n + 1))) m' → HasSum f (m + f 0 + m')
-- Mathlib.CategoryTheory.Triangulated.Functor
CategoryTheory.IsTriangulated.of_fully_faithful_triangulated_functor : ∀ {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] [inst_2 : CategoryTheory.HasShift C ℤ]
  [inst_3 : CategoryTheory.HasShift D ℤ] [inst_4 : CategoryTheory.Limits.HasZeroObject C]
  [inst_5 : CategoryTheory.Limits.HasZeroObject D] [inst_6 : CategoryTheory.Preadditive C]
  [inst_7 : CategoryTheory.Preadditive D] [inst_8 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [inst_9 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [inst_10 : CategoryTheory.Pretriangulated C]
  [inst_11 : CategoryTheory.Pretriangulated D] (F : CategoryTheory.Functor C D) [inst_12 : F.CommShift ℤ]
  [F.IsTriangulated] [F.Full] [F.Faithful] [CategoryTheory.IsTriangulated D], CategoryTheory.IsTriangulated C
-- Mathlib.Tactic.TacticAnalysis.Declarations
/-- Verify that replacing `grind` with `grind?` produces a valid `grind only` suggestion.  -/
verifyGrindOnly : Mathlib.TacticAnalysis.Config
-- Mathlib.CategoryTheory.Limits.Preserves.Finite
CategoryTheory.Limits.ReflectsFiniteCoproducts.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D},
  (∀ (n : ℕ), CategoryTheory.Limits.ReflectsColimitsOfShape (CategoryTheory.Discrete (Fin n)) F) →
    CategoryTheory.Limits.ReflectsFiniteCoproducts F
-- Mathlib.Data.Finset.Preimage
/-- Preimage of `s : Finset β` under a map `f` injective on `f ⁻¹' s` as a `Finset`.  -/
Finset.preimage : {α : Type u} → {β : Type v} → (s : Finset β) → (f : α → β) → Set.InjOn f (f ⁻¹' ↑s) → Finset α
-- Mathlib.Order.Preorder.Finsupp
Finsupp.coe_strictMono : ∀ {ι : Type u_1} {M : Type u_2} [inst : Zero M] [inst_1 : Preorder M], Monotone Finsupp.toFun
-- Mathlib.Geometry.Manifold.Sheaf.Smooth
/-- The sheaf of smooth functions from `M` to `N`, as a sheaf of types.  -/
smoothSheaf : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {EM : Type u_2} →
      [inst_1 : NormedAddCommGroup EM] →
        [inst_2 : NormedSpace 𝕜 EM] →
          {HM : Type u_3} →
            [inst_3 : TopologicalSpace HM] →
              ModelWithCorners 𝕜 EM HM →
                {E : Type u_4} →
                  [inst_4 : NormedAddCommGroup E] →
                    [inst_5 : NormedSpace 𝕜 E] →
                      {H : Type u_5} →
                        [inst_6 : TopologicalSpace H] →
                          ModelWithCorners 𝕜 E H →
                            (M : Type u) →
                              [inst : TopologicalSpace M] →
                                [ChartedSpace HM M] →
                                  (N : Type u) →
                                    [inst_8 : TopologicalSpace N] →
                                      [ChartedSpace H N] → TopCat.Sheaf (Type u) (TopCat.of M)
-- Mathlib.CategoryTheory.Bicategory.Modification.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.Modification.hasCoeToOplax : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.Pseudofunctor B C} →
          {η θ : F ⟶ G} →
            Coe (CategoryTheory.Pseudofunctor.StrongTrans.Modification η θ)
              ((CategoryTheory.Pseudofunctor.StrongTrans.toOplax η).Modification
                (CategoryTheory.Pseudofunctor.StrongTrans.toOplax θ))
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : Cᵒᵖ ⥤ D` preserves colimits, then `F.rightOp : C ⥤ Dᵒᵖ` preserves limits.  -/
CategoryTheory.Limits.preservesLimits_rightOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor Cᵒᵖ D) [CategoryTheory.Limits.PreservesColimits F],
  CategoryTheory.Limits.PreservesLimits F.rightOp
-- Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
/-- If `f : X ⟶ Y` and `g : Y ⟶ Z` satisfy `W f` and `W g`, then `f ≫ g` is a
transfinite composition of shape `Fin 3` of morphisms in `W`.  -/
CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {W : CategoryTheory.MorphismProperty C} →
      {X Y Z : C} →
        (f : X ⟶ Y) →
          (g : Y ⟶ Z) → W f → W g → W.TransfiniteCompositionOfShape (Fin 3) (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.Algebra.Polynomial.Eval.Coeff
Polynomial.support_map_of_injective : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] (p : Polynomial R) {f : R →+* S},
  Function.Injective ⇑f → (Polynomial.map f p).support = p.support
-- Init.Data.BitVec.Lemmas
BitVec.not_or : ∀ {w : ℕ} {x y : BitVec w}, ~~~(x ||| y) = ~~~x &&& ~~~y
-- Mathlib.Algebra.Lie.Abelian
TrivialLieModule.instLieRingModule : (R : Type u_1) →
  (L : Type u_2) →
    (M : Type u_3) → [inst : LieRing L] → [inst_1 : AddCommGroup M] → LieRingModule L (TrivialLieModule R L M)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get?_emptyc : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : Std.LawfulEqCmp cmp] {a : α},
  ∅.get? a = none
-- Mathlib.RingTheory.Algebraic.Integral
Transcendental.integralClosure : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [NoZeroDivisors S]
  {a : S}, Transcendental R a → Transcendental (↥(integralClosure R S)) a
-- Mathlib.Algebra.Group.TypeTags.Hom
AddMonoidHom.coe_toMultiplicativeRight : ∀ {α : Type u_3} {β : Type u_4} [inst : MulOneClass α] [inst_1 : AddZeroClass β] (f : Additive α →+ β),
  ⇑(AddMonoidHom.toMultiplicativeRight f) = ⇑Multiplicative.ofAdd ∘ ⇑f ∘ ⇑Additive.ofMul
-- Mathlib.Order.Interval.Set.Image
MonotoneOn.mapsTo_Icc : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : Preorder α] [inst_1 : Preorder β] {a b : α},
  MonotoneOn f (Set.Icc a b) → Set.MapsTo f (Set.Icc a b) (Set.Icc (f a) (f b))
-- Mathlib.LinearAlgebra.Finsupp.Defs
Finsupp.curryLinearEquiv_symm_apply_apply : ∀ {α : Type u_9} {β : Type u_10} {R : Type u_11} {M : Type u_12} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] (f : α →₀ β →₀ M) (xy : α × β), ((Finsupp.curryLinearEquiv R).symm f) xy = (f xy.1) xy.2
-- Mathlib.Data.QPF.Multivariate.Constructions.Comp
/-- Destructor for functor composition  -/
MvQPF.Comp.get : {n m : ℕ} →
  {F : TypeVec.{u} n → Type u_1} →
    {G : Fin2 n → TypeVec.{u} m → Type u} → {α : TypeVec.{u} m} → MvQPF.Comp F G α → F fun i => G i α
-- Lean.Environment
_private.Lean.Environment.0.Lean.AsyncConst.aconsts : Lean.AsyncConst✝ → Task Lean.AsyncConsts✝
-- Mathlib.AlgebraicGeometry.Morphisms.Separated
AlgebraicGeometry.Scheme.instIsClosedImmersionLiftIdOfIsSeparated : ∀ {X : AlgebraicGeometry.Scheme} [X.IsSeparated],
  AlgebraicGeometry.IsClosedImmersion
    (CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id X))
-- Mathlib.CategoryTheory.FiberedCategory.Fiber
/-- `Fiber p S` is the type of elements of `𝒳` mapping to `S` via `p`.  -/
CategoryTheory.Functor.Fiber : {𝒮 : Type u₁} →
  {𝒳 : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳] → CategoryTheory.Functor 𝒳 𝒮 → 𝒮 → Type (max 0 u₂)
-- Mathlib.Algebra.Order.BigOperators.Group.List
/-- If `l₁` is a sublist of `l₂` and all elements of `l₂` are greater than or equal to one, then
`l₁.prod ≤ l₂.prod`. One can prove a stronger version assuming `∀ a ∈ l₂.diff l₁, 1 ≤ a` instead
of `∀ a ∈ l₂, 1 ≤ a` but this lemma is not yet in `mathlib`.  -/
List.Sublist.prod_le_prod' : ∀ {M : Type u_3} [inst : Monoid M] [inst_1 : Preorder M] [MulRightMono M] [MulLeftMono M] {l₁ l₂ : List M},
  l₁.Sublist l₂ → (∀ a ∈ l₂, 1 ≤ a) → l₁.prod ≤ l₂.prod
-- Lean.Meta.Tactic.Grind.Types
/-- Mapping from binary functions `f` to a theorem `thm : ∀ a b, f a b = .eq → a = b`
if it implements the `LawfulEqCmp` type class.
 -/
Lean.Meta.Grind.State.lawfulEqCmpMap : Lean.Meta.Grind.State → Lean.PHashMap Lean.Meta.Sym.ExprPtr (Option Lean.Expr)
-- Mathlib.AlgebraicTopology.SimplexCategory.Rev
SimplexCategory.revCompRevIso_hom_app : ∀ (X : SimplexCategory), SimplexCategory.revCompRevIso.hom.app X = CategoryTheory.CategoryStruct.id X
-- Mathlib.Data.Finsupp.Basic
Finsupp.sumFinsuppAddEquivProdFinsupp_symm_inl : ∀ {M : Type u_5} [inst : AddMonoid M] {α : Type u_12} {β : Type u_13} (fg : (α →₀ M) × (β →₀ M)) (x : α),
  (Finsupp.sumFinsuppAddEquivProdFinsupp.symm fg) (Sum.inl x) = fg.1 x
-- Mathlib.RingTheory.Etale.StandardEtale
/-- The polynomial to be localized away from in a standard etale algebra.  -/
StandardEtalePair.g : {R : Type u_1} → [inst : CommRing R] → StandardEtalePair R → Polynomial R
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.associator_hom_snd_fst_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (X Y Z : C) {Z_1 : C} (h : Y ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.SemiCartesianMonoidalCategory.snd X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.fst Y Z) h)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.SemiCartesianMonoidalCategory.fst (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.snd X Y) h)
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
/-- `Lp.simpleFunc` is a subspace of Lp consisting of equivalence classes of an integrable simple
function.  -/
MeasureTheory.«term_→₁ₛ[_]_» : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.associator_hom_snd_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (X Y Z : C),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.SemiCartesianMonoidalCategory.snd X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z))
        (CategoryTheory.SemiCartesianMonoidalCategory.snd Y Z)) =
    CategoryTheory.SemiCartesianMonoidalCategory.snd (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z
-- Mathlib.CategoryTheory.Functor.Functorial
CategoryTheory.functorial_id : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → CategoryTheory.Functorial id
-- Mathlib.Data.Nat.Init
Nat.leRec_self : ∀ {n : ℕ} {motive : (m : ℕ) → n ≤ m → Sort u_1} (refl : motive n ⋯)
  (le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯), Nat.leRec refl le_succ_of_le ⋯ = refl
-- Mathlib.Analysis.Complex.Trigonometric
Complex.cos_mul_I : ∀ (x : ℂ), Complex.cos (x * Complex.I) = Complex.cosh x
-- Mathlib.Order.Closure
ClosureOperator.sInf_isClosed : ∀ {α : Type u_1} [inst : CompleteLattice α] {c : ClosureOperator α} {S : Set α},
  (∀ x ∈ S, c.IsClosed x) → c.IsClosed (sInf S)
-- Mathlib.SetTheory.ZFC.PSet
PSet.instMembership : Membership PSet.{u_1} PSet.{u_1}
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get_diff : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k : α} {h_mem : k ∈ t₁ \ t₂}, Std.DTreeMap.Const.get (t₁ \ t₂) k h_mem = Std.DTreeMap.Const.get t₁ k ⋯
-- Std.Http.Server.Connection
Std.Http.Server.RemoteAddr.mk.injEq : ∀ (addr addr_1 : Std.Net.SocketAddress), ({ addr := addr } = { addr := addr_1 }) = (addr = addr_1)
-- Mathlib.Computability.TuringMachine.PostTuringMachine
/-- The statement (if any) which is currently evaluated  -/
Turing.TM1.Cfg.l : {Γ : Type u_1} → {Λ : Type u_2} → {σ : Type u_3} → [inst : Inhabited Γ] → Turing.TM1.Cfg Γ Λ σ → Option Λ
-- Init.Data.Ord.Basic
compareOfLessAndEq_eq_swap_of_lt_iff_not_gt_and_ne : ∀ {α : Type u} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : DecidableEq α],
  (∀ (x y : α), x < y ↔ ¬y < x ∧ x ≠ y) → ∀ {x y : α}, compareOfLessAndEq x y = (compareOfLessAndEq y x).swap
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List (α × β)} {k : α} (contains_eq_false : (List.map Prod.fst l).contains k = false)
  {h : k ∈ m.insertMany l}, (m.insertMany l)[k] = m[k]
-- Mathlib.Geometry.Euclidean.Incenter
/-- The distance between the excenter and its projection in the plane of each face is the
exradius.  -/
Affine.Simplex.ExcenterExists.dist_excenter : ∀ {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 → ∀ (i : Fin (n + 1)), dist (s.excenter signs) (s.touchpoint signs i) = s.exradius signs
-- Mathlib.LinearAlgebra.CliffordAlgebra.Even
CliffordAlgebra.even.lift_symm_apply_bilin : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q : QuadraticForm R M) {A : Type u_3} [inst_3 : Ring A] [inst_4 : Algebra R A]
  (F : ↥(CliffordAlgebra.even Q) →ₐ[R] A),
  ((CliffordAlgebra.even.lift Q).symm F).bilin = (CliffordAlgebra.even.ι Q).bilin.compr₂ F.toLinearMap
-- Init.Data.Slice.Array.Iterator
_private.Init.Data.Slice.Array.Iterator.0.SubarrayIterator.step.match_1.splitter : {α : Type u_1} →
  (motive : Std.IterM Id α → Sort u_2) →
    (x : Std.IterM Id α) → ((xs : Subarray α) → motive { internalState := { xs := xs } }) → motive x
-- Mathlib.Order.Filter.ENNReal
Real.limsup_of_not_isCoboundedUnder : ∀ {ι : Type u_1} {f : Filter ι} {u : ι → ℝ}, ¬Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f u → Filter.limsup u f = 0
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Localization.mk_eq_mk_iff : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {a c : M} {b d : ↥S},
  Localization.mk a b = Localization.mk c d ↔ (Localization.r S) (a, b) (c, d)
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
_private.Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing.0.AlgebraicGeometry.PresheafedSpace.GlueData.«termπ₁⁻¹_,_,_» : Lean.ParserDescr
-- Mathlib.Analysis.Calculus.ContDiff.Basic
iteratedFDerivWithin_zero : ∀ {𝕜 : 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] {s : Set E} {i : ℕ},
  iteratedFDerivWithin 𝕜 i 0 s = 0
-- Mathlib.Analysis.Asymptotics.Lemmas
/-- **Alias** of the forward direction of `Asymptotics.isLittleO_iff_exists_eq_mul`. -/
Asymptotics.IsLittleO.exists_eq_mul : ∀ {α : Type u_1} {𝕜 : Type u_15} [inst : NormedDivisionRing 𝕜] {l : Filter α} {u v : α → 𝕜},
  u =o[l] v → ∃ φ, Filter.Tendsto φ l (nhds 0) ∧ u =ᶠ[l] φ * v
-- Mathlib.Order.Lattice
toDual_max : ∀ {α : Type u} [inst : LinearOrder α] (a b : α),
  OrderDual.toDual (max a b) = min (OrderDual.toDual a) (OrderDual.toDual b)
-- Mathlib.Topology.Algebra.Constructions
Units.isInducing_embedProduct : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : Monoid M], Topology.IsInducing ⇑(Units.embedProduct M)
-- Mathlib.CategoryTheory.Adjunction.FullyFaithful
CategoryTheory.Adjunction.instIsIsoFunctorCounitOfIsEquivalence_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) [R.IsEquivalence],
  CategoryTheory.IsIso h.counit
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
/-- If `η` is also `yoneda`-costructured, then `OverArrows η s` is just morphisms of costructured
arrows.  -/
CategoryTheory.OverPresheafAux.OverArrows.costructuredArrowIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : CategoryTheory.Functor Cᵒᵖ (Type v)} →
      (s t : CategoryTheory.CostructuredArrow CategoryTheory.yoneda A) →
        CategoryTheory.OverPresheafAux.OverArrows s.hom t.hom ≅ t ⟶ s
-- Mathlib.CategoryTheory.Limits.Connected
CategoryTheory.Limits.hasLimit_const_of_isConnected : ∀ (J : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} C]
  (X : C) [CategoryTheory.IsConnected J], CategoryTheory.Limits.HasLimit ((CategoryTheory.Functor.const J).obj X)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get!_inter_of_not_mem_left : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.ExtDTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] [inst_1 : Inhabited β] {k : α}, k ∉ t₁ → Std.ExtDTreeMap.Const.get! (t₁ ∩ t₂) k = default
-- Init.Core
/-- Superset relation: `a ⊇ b`  

Conventions for notations in identifiers:

 * The recommended spelling of `⊇` in identifiers is `superset` (prefer `⊆` over `⊇`). -/
«term_⊇_» : Lean.TrailingParserDescr
-- Mathlib.Data.Nat.Choose.Factorization
/-- The factorization of `p` in `(p * n)!` is `n` more than that of `n!`.  -/
Nat.factorization_factorial_mul : ∀ {n p : ℕ}, Nat.Prime p → (p * n).factorial.factorization p = n.factorial.factorization p + n
-- Mathlib.CategoryTheory.Preadditive.FunctorCategory
CategoryTheory.instNegHomFunctor : {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] →
        [CategoryTheory.Preadditive D] → {F G : CategoryTheory.Functor C D} → Neg (F ⟶ G)
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.mem_insert_iff : ∀ {x y z : ZFSet.{u}}, x ∈ insert y z ↔ x = y ∨ x ∈ z
-- Init.Data.Int.Linear
Int.Internal.Linear.Expr.denote.eq_def : ∀ (ctx : Int.Internal.Linear.Context) (x : Int.Internal.Linear.Expr),
  Int.Internal.Linear.Expr.denote ctx x =
    match x with
    | a.add b => Int.Internal.Linear.Expr.denote ctx a + Int.Internal.Linear.Expr.denote ctx b
    | a.sub b => Int.Internal.Linear.Expr.denote ctx a - Int.Internal.Linear.Expr.denote ctx b
    | a.neg => -Int.Internal.Linear.Expr.denote ctx a
    | Int.Internal.Linear.Expr.num k => k
    | Int.Internal.Linear.Expr.var v => Int.Internal.Linear.Var.denote ctx v
    | Int.Internal.Linear.Expr.mulL k e => k * Int.Internal.Linear.Expr.denote ctx e
    | e.mulR k => Int.Internal.Linear.Expr.denote ctx e * k
-- Mathlib.Combinatorics.Additive.PluenneckeRuzsa
/-- **Ruzsa's triangle inequality**. Negadd-add-add version.  -/
Finset.ruzsa_triangle_inequality_negAdd_add_add : ∀ {G : Type u_1} [inst : DecidableEq G] [inst_1 : AddGroup G] (A B C : Finset G),
  B.card * (-A + C).card ≤ (B + A).card * (B + C).card
-- Mathlib.Analysis.Calculus.FDeriv.Basic
/-- **Alias** of `fderivWithin_fun_id`.

---

Eta-expanded form of `fderivWithin_id` -/
fderivWithin_id' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {x : E} {s : Set E} [ContinuousAdd E] [ContinuousSMul 𝕜 E] [T2Space E],
  UniqueDiffWithinAt 𝕜 s x → fderivWithin 𝕜 (fun x => x) s x = ContinuousLinearMap.id 𝕜 E