mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
/-- An equivalent expression of `IsProperLinearSet` in terms of `Finset` instead of `Set.Finite`.  -/
isProperLinearSet_iff : ∀ {M : Type u_1} [inst : AddCommMonoid M] {s : Set M},
  IsProperLinearSet s ↔ ∃ a t, LinearIndepOn ℕ id ↑t ∧ s = a +ᵥ ↑(AddSubmonoid.closure ↑t)
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.Hom.w₁₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S}
  {F : CategoryTheory.PreOneHypercover S} (self : E.Hom F) {i j : E.I₀} (k : E.I₁ i j),
  CategoryTheory.CategoryStruct.comp (self.h₁ k) (F.p₁ (self.s₁ k)) =
    CategoryTheory.CategoryStruct.comp (E.p₁ k) (self.h₀ i)
-- Mathlib.SetTheory.ZFC.PSet
PSet.brecOn.go : {motive : PSet.{u} → Sort u_1} → (t : PSet.{u}) → ((t : PSet.{u}) → PSet.below t → motive t) → motive t ×' PSet.below t
-- Init.Data.SInt.IntToBitVec
ISize.toBitVec32_toInt16 : ∀ (n : ISize) (h : System.Platform.numBits = 32), n.toInt16.toBitVec = BitVec.signExtend 16 (n.toBitVec32 h)
-- Mathlib.Topology.Hom.Open
ContinuousOpenMap.id_apply : ∀ {α : Type u_2} [inst : TopologicalSpace α] (a : α), (ContinuousOpenMap.id α) a = a
-- Mathlib.CategoryTheory.Triangulated.Opposite.Functor
/-- If `F : C ⥤ D` commutes with shifts, this expresses the compatibility of `F.mapTriangle`
with the equivalences `Pretriangulated.triangleOpEquivalence` on `C` and `D`.
 -/
CategoryTheory.Functor.opMapTriangleCompTriangleOpEquivalenceInverse : {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 ℤ] →
            (F : CategoryTheory.Functor C D) →
              [inst_4 : F.CommShift ℤ] →
                F.op.mapTriangle.comp (CategoryTheory.Pretriangulated.triangleOpEquivalence D).inverse ≅
                  (CategoryTheory.Pretriangulated.triangleOpEquivalence C).inverse.comp F.mapTriangle.op
-- Mathlib.MeasureTheory.PiSystem
measurableSet_iSup_of_mem_piiUnionInter : ∀ {α : Type u_3} {ι : Type u_4} (m : ι → MeasurableSpace α) (S : Set ι),
  ∀ t ∈ piiUnionInter (fun n => {s | MeasurableSet s}) S, MeasurableSet t
-- Mathlib.Analysis.Analytic.Constructions
analyticAt_pi_iff : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {ι : Type u_9} [inst_3 : Fintype ι] {e : E} {Fm : ι → Type u_10}
  [inst_4 : (i : ι) → NormedAddCommGroup (Fm i)] [inst_5 : (i : ι) → NormedSpace 𝕜 (Fm i)] {f : (i : ι) → E → Fm i},
  AnalyticAt 𝕜 (fun x x_1 => f x_1 x) e ↔ ∀ (i : ι), AnalyticAt 𝕜 (f i) e
-- Std.Data.DHashMap.Lemmas
/-- Simpler variant of `get?_filterMap` when `LawfulBEq` is available.  -/
Std.DHashMap.Const.get?_filterMap' : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {γ : Type w} {m : Std.DHashMap α fun x => β} [LawfulBEq α]
  {f : α → β → Option γ} {k : α},
  Std.DHashMap.Const.get? (Std.DHashMap.filterMap f m) k = (Std.DHashMap.Const.get? m k).bind fun x => f k x
-- Mathlib.Topology.Order.LowerUpperTopology
Topology.WithLower.instLinearOrder : {α : Type u_1} → [LinearOrder α] → LinearOrder (Topology.WithLower α)
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.isBasis_union_iff_indep_closure : ∀ {α : Type u_2} {M : Matroid α} {X I : Set α}, M.IsBasis I (I ∪ X) ↔ M.Indep I ∧ X ⊆ M.closure I
-- Mathlib.Data.Nat.Pairing
Nat.unpair_add_le : ∀ (n : ℕ), (Nat.unpair n).1 + (Nat.unpair n).2 ≤ n
-- Mathlib.CategoryTheory.Sums.Basic
CategoryTheory.Functor.isoSum_hom_app_inl : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor (A ⊕ B) C) (a : A),
  F.isoSum.hom.app (Sum.inl a) = CategoryTheory.CategoryStruct.id (F.obj (Sum.inl a))
-- Mathlib.Topology.Closure
Finset.interior_iInter : ∀ {X : Type u} [inst : TopologicalSpace X] {ι : Type u_1} (s : Finset ι) (f : ι → Set X),
  interior (⋂ i ∈ s, f i) = ⋂ i ∈ s, interior (f i)
-- Mathlib.GroupTheory.Solvable
/-- **Alias** of `Equiv.Perm.not_isSolvable`. -/
Equiv.Perm.not_solvable : ∀ (X : Type u_3), 5 ≤ Cardinal.mk X → ¬Group.IsSolvable (Equiv.Perm X)
-- Mathlib.Topology.Inseparable
Inseparable.specializes : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X}, Inseparable x y → x ⤳ y
-- Lean.Syntax
Lean.Syntax.Range.contains : Lean.Syntax.Range → String.Pos.Raw → optParam Bool false → Bool
-- Mathlib.GroupTheory.IsSubnormal
_private.Mathlib.GroupTheory.IsSubnormal.0.AddSubgroup.IsSubnormal.isSubnormal_iff.match_1_1.congr_eq_1 : ∀ (motive : ℕ → Sort u_1) (x : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  x = 0 →
    (match x with
      | 0 => h_1 ()
      | n.succ => h_2 n) ≍
      h_1 ()
-- Mathlib.Algebra.Group.Submonoid.Membership
Submonoid.mem_sup_right : ∀ {M : Type u_1} [inst : MulOneClass M] {S T : Submonoid M} {x : M}, x ∈ T → x ∈ S ⊔ T
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.pullback₂.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S T : C} (f f_1 : S ⟶ T) (e_f : f = f_1)
  (E E_1 : CategoryTheory.PreZeroHypercover T) (e_E : E = E_1)
  [inst_1 : ∀ (i : E.I₀), CategoryTheory.Limits.HasPullback (E.f i) f],
  CategoryTheory.PreZeroHypercover.pullback₂ f E = CategoryTheory.PreZeroHypercover.pullback₂ f_1 E_1
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
/-- As `J` is nonempty, we can pick an arbitrary object `j₀ : J`. We use this object to
define the "zero" in the colimit as the equivalence class of `⟨j₀, 0 : F.obj j₀⟩`.  -/
AddMonCat.FilteredColimits.colimitZero : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    (F : CategoryTheory.Functor J AddMonCat) → [CategoryTheory.IsFiltered J] → Zero (AddMonCat.FilteredColimits.M F)
-- Mathlib.Algebra.DirectSum.Basic
DirectSum.IsInternal.addSubmonoid_iSup_eq_top : ∀ {ι : Type v} {M : Type u_1} [inst : DecidableEq ι] [inst_1 : AddCommMonoid M] (A : ι → AddSubmonoid M),
  DirectSum.IsInternal A → iSup A = ⊤
-- Batteries.Classes.Order
/-- `cmp x y = .lt` holds iff `x < y` is true.  -/
Std.LawfulLTCmp.eq_lt_iff_lt : ∀ {α : Type u_1} {inst : LT α} {cmp : α → α → Ordering} [self : Std.LawfulLTCmp cmp] {x y : α},
  cmp x y = Ordering.lt ↔ x < y
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
/-- The canonical map `(A_f)₀ ⟶ Γ(Proj A, D₊(f))`.
This is an isomorphism when `f` is homogeneous of positive degree. See `basicOpenIsoAway` below.  -/
AlgebraicGeometry.Proj.awayToSection : {σ : Type u_1} →
  {A : Type u} →
    [inst : CommRing A] →
      [inst_1 : SetLike σ A] →
        [inst_2 : AddSubgroupClass σ A] →
          (𝒜 : ℕ → σ) →
            [inst_3 : GradedRing 𝒜] →
              (f : A) →
                CommRingCat.of (HomogeneousLocalization.Away 𝒜 f) ⟶
                  (AlgebraicGeometry.Proj 𝒜).presheaf.obj (Opposite.op (AlgebraicGeometry.Proj.basicOpen 𝒜 f))
-- Mathlib.Order.Preorder.Finite
Set.infinite_of_forall_exists_lt : ∀ {α : Type u_2} [inst : Preorder α] {s : Set α} [Nonempty α], (∀ (a : α), ∃ b ∈ s, b < a) → s.Infinite
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
_private.Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt.0.Lean.Meta.Grind.Arith.Cutsat.mkBinOpThms : Lean.Name → Lean.Name → Lean.Meta.Grind.Arith.Cutsat.ToIntM Lean.Meta.Grind.Arith.Cutsat.ToIntThms
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.awayMap.congr_simp : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubgroupClass σ A] [inst_3 : AddCommMonoid ι] [inst_4 : DecidableEq ι] (𝒜 : ι → σ)
  [inst_5 : GradedRing 𝒜] {e e_1 : ι} (e_e : e = e_1) {f g g_1 : A} (e_g : g = g_1) (hg : g ∈ 𝒜 e) {x : A}
  (hx : x = f * g), HomogeneousLocalization.awayMap 𝒜 hg hx = HomogeneousLocalization.awayMap 𝒜 ⋯ ⋯
-- Mathlib.CategoryTheory.Discrete.Basic
CategoryTheory.instIsDiscreteOpposite : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.IsDiscrete C],
  CategoryTheory.IsDiscrete Cᵒᵖ
-- Mathlib.Algebra.Homology.DerivedCategory.Plus
DerivedCategory.Plus.instIsVerdierRightLocalizingHomotopyCategoryIntUpPlusSubcategoryAcyclic : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C],
  (HomotopyCategory.plus C).IsVerdierRightLocalizing (HomotopyCategory.subcategoryAcyclic C)
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- The diagram
```
      U ---------m----------> X
      |                       |
    χ₀ U                     χ m
      |                       |
      v                       v
      Ω₀ ------truth--------> Ω
```
is a pullback square.
 -/
CategoryTheory.HasSubobjectClassifier.isPullback_χ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasSubobjectClassifier C] {U X : C}
  (m : U ⟶ X) [inst_2 : CategoryTheory.Mono m],
  CategoryTheory.IsPullback m (⋯.some.χ₀ U) (CategoryTheory.HasSubobjectClassifier.χ m)
    (CategoryTheory.HasSubobjectClassifier.truth C)
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Poly.toExpr.go : Nat.Internal.Linear.Expr → Nat.Internal.Linear.Poly → Nat.Internal.Linear.Expr
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
/-- If an integral domain has a primitive `k`-th root of unity, then it has `φ k` of them.  -/
IsPrimitiveRoot.card_primitiveRoots : ∀ {R : Type u_4} [inst : CommRing R] [inst_1 : IsDomain R] {ζ : R} {k : ℕ},
  IsPrimitiveRoot ζ k → (primitiveRoots k R).card = k.totient
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
/-- The costructured arrow category `CostructuredArrow T d` depends on the chosen codomain `d : D`
in a functorial way, inducing a functor `D ⥤ Cat`.  -/
CategoryTheory.CostructuredArrow.functor : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        CategoryTheory.Functor C D → CategoryTheory.Functor D CategoryTheory.Cat
-- Init.Prelude
/-- Create syntax node with 5 children  -/
Lean.Syntax.node5 : Lean.SourceInfo →
  Lean.SyntaxNodeKind → Lean.Syntax → Lean.Syntax → Lean.Syntax → Lean.Syntax → Lean.Syntax → Lean.Syntax
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.infinitePos_abs_iff_infinite : ∀ {x : ℝ*}, |x|.InfinitePos ↔ x.Infinite
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Over
CategoryTheory.Over.tensorHom_left_fst_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  {X S U : C} {R T : CategoryTheory.Over X} (fS : S ⟶ X) (fU : U ⟶ X) (f : R ⟶ CategoryTheory.Over.mk fS)
  (g : T ⟶ CategoryTheory.Over.mk fU) {Z : C} (h : S ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.Hom.left (CategoryTheory.MonoidalCategoryStruct.tensorHom f g))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst fS fU) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst R.hom T.hom)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left f) h)
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.List.filterMap_replicate.match_1.splitter : {β : Type u_1} →
  (motive : Option β → Sort u_2) → (x : Option β) → (Unit → motive none) → ((b : β) → motive (some b)) → motive x
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey!_eq_of_contains : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [inst_2 : Inhabited α] {k : α}, t.contains k = true → t.getKey! k = k
-- Mathlib.RingTheory.SimpleRing.Basic
IsSimpleRing.one_mem_of_ne_bot : ∀ {A : Type u_2} [inst : NonAssocRing A] [IsSimpleRing A] (I : TwoSidedIdeal A), I ≠ ⊥ → 1 ∈ I
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
HomogeneousIdeal.toIdeal_sup : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : Semiring A] [inst_1 : DecidableEq ι] [inst_2 : AddMonoid ι]
  [inst_3 : SetLike σ A] [inst_4 : AddSubmonoidClass σ A] {𝒜 : ι → σ} [inst_5 : GradedRing 𝒜]
  (I J : HomogeneousIdeal 𝒜), (I ⊔ J).toIdeal = I.toIdeal ⊔ J.toIdeal
-- Init.Data.Rat.Basic
Rat.mk'.sizeOf_spec : ∀ (num : ℤ) (den : ℕ) (den_nz : autoParam (den ≠ 0) Rat.den_nz._autoParam)
  (reduced : autoParam (num.natAbs.Coprime den) Rat.reduced._autoParam),
  sizeOf { num := num, den := den, den_nz := den_nz, reduced := reduced } = 1 + sizeOf num + sizeOf den + sizeOf reduced
-- Init.Meta.Defs
Lean.version.major : ℕ
-- Mathlib.RingTheory.Ideal.Cotangent
AlgHom.ker_kerSquareLift : ∀ {R : Type u} [inst : CommRing R] {A : Type u_1} {B : Type u_2} [inst_1 : CommRing A] [inst_2 : CommRing B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (f : A →ₐ[R] B),
  RingHom.ker f.kerSquareLift.toRingHom = (RingHom.ker f.toRingHom).cotangentIdeal
-- Mathlib.GroupTheory.Nilpotent
Subgroup.mem_lowerCentralSeries_succ_iff : ∀ {G : Type u_1} [inst : Group G] (S : Subgroup G) (n : ℕ) (q : G),
  q ∈ S.lowerCentralSeries (n + 1) ↔ q ∈ Subgroup.closure {x | ∃ p ∈ S.lowerCentralSeries n, ∃ q ∈ S, ⁅p, q⁆ = x}
-- Mathlib.Geometry.Convex.Cone.Pointed
PointedCone.ofSubmodule_lineal : ∀ {R : Type u_1} {E : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommGroup E] [inst_4 : Module R E] (C : PointedCone R E), ↑C.lineal = C ⊓ -C
-- Mathlib.Data.W.Basic
_private.Mathlib.Data.W.Basic.0.WType.finv : {α : Type u_1} →
  {β : α → Type u_2} →
    [inst : (a : α) → Fintype (β a)] → (n : ℕ) → (a : α) × (β a → WType.WType'✝ β n) → WType.WType'✝ β (n + 1)
-- Mathlib.CategoryTheory.Dialectica.Monoidal
CategoryTheory.Dial.instMonoidalCategoryStruct : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasFiniteProducts C] →
      [inst_2 : CategoryTheory.Limits.HasPullbacks C] → CategoryTheory.MonoidalCategoryStruct (CategoryTheory.Dial C)
-- Mathlib.Algebra.BigOperators.Group.Multiset.Defs
/-- Product of a multiset given a commutative monoid structure on `M`.
`prod {a, b, c} = a * b * c`  -/
Multiset.prod : {M : Type u_3} → [CommMonoid M] → Multiset M → M
-- Lean.Meta.LazyDiscrTree
/-- Structure for quickly initializing a lazy discrimination tree with a large number
of elements using concurrent functions for generating entries.
 -/
Lean.Meta.LazyDiscrTree.PreDiscrTree : Type → Type
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
/-- The measurable sets are exactly the Borel-measurable sets.  -/
BorelSpace.measurable_eq : ∀ {α : Type u_6} {inst : TopologicalSpace α} {inst_1 : MeasurableSpace α} [self : BorelSpace α], inst_1 = borel α
-- Mathlib.Tactic.LinearCombination.Lemmas
/-- Given two (in)equalities `P` and `Q`, look up the lemma to deduce `Q` from `P`, and the relation
appearing in the side condition produced by this lemma.  -/
Mathlib.Ineq.relImpRelData : Mathlib.Ineq → Mathlib.Ineq → Option (Lean.Name × Mathlib.Ineq)
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.homologyι_comp_asIsoHomologyι_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) (hg : S.g = 0) [inst_2 : S.HasHomology],
  CategoryTheory.CategoryStruct.comp S.homologyι (S.asIsoHomologyι hg).inv = CategoryTheory.CategoryStruct.id S.homology
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.min_insert_of_isEmpty : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α},
  t.isEmpty = true → (t.insert k).min ⋯ = k
-- Mathlib.Computability.Partrec
Partrec.to₂ : ∀ {α : Type u_1} {β : Type u_2} {σ : Type u_3} [inst : Primcodable α] [inst_1 : Primcodable β] [inst_2 : Primcodable σ]
  {f : α × β →. σ}, Partrec f → Partrec₂ fun a b => f (a, b)
-- Mathlib.CategoryTheory.Adjunction.CompositionIso
CategoryTheory.Adjunction.leftAdjointCompNatTrans_app : ∀ {C₀ : Type u_1} {C₁ : Type u_2} {C₂ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₀]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₁] [inst_2 : CategoryTheory.Category.{v_3, u_3} C₂]
  {F₀₁ : CategoryTheory.Functor C₀ C₁} {F₁₂ : CategoryTheory.Functor C₁ C₂} {F₀₂ : CategoryTheory.Functor C₀ C₂}
  {G₁₀ : CategoryTheory.Functor C₁ C₀} {G₂₁ : CategoryTheory.Functor C₂ C₁} {G₂₀ : CategoryTheory.Functor C₂ C₀}
  (adj₀₁ : F₀₁ ⊣ G₁₀) (adj₁₂ : F₁₂ ⊣ G₂₁) (adj₀₂ : F₀₂ ⊣ G₂₀) (τ₀₁₂ : G₂₀ ⟶ G₂₁.comp G₁₀) (X : C₀),
  (adj₀₁.leftAdjointCompNatTrans adj₁₂ adj₀₂ τ₀₁₂).app X =
    CategoryTheory.CategoryStruct.comp (F₁₂.map (F₀₁.map (adj₀₂.unit.app X)))
      (CategoryTheory.CategoryStruct.comp (F₁₂.map (F₀₁.map (τ₀₁₂.app (F₀₂.obj X))))
        (CategoryTheory.CategoryStruct.comp (F₁₂.map (adj₀₁.counit.app (G₂₁.obj (F₀₂.obj X))))
          (adj₁₂.counit.app (F₀₂.obj X))))
-- Mathlib.Order.LatticeIntervals
Set.Iic.isCompl_iff : ∀ {α : Type u_1} {a : α} [inst : Lattice α] [inst_1 : OrderBot α] {x y : ↑(Set.Iic a)},
  IsCompl x y ↔ Disjoint ↑x ↑y ∧ ↑x ⊔ ↑y = a
-- Std.Internal.Parsec.Basic
Std.Internal.Parsec.Input.pos : {ι : Type} →
  {elem idx : outParam Type} →
    {inst : DecidableEq idx} → {inst_1 : DecidableEq elem} → [self : Std.Internal.Parsec.Input ι elem idx] → ι → idx
-- Mathlib.MeasureTheory.Measure.EverywherePos
MeasureTheory.Measure.everywherePosSubset_subset : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] (μ : MeasureTheory.Measure α) (s : Set α),
  μ.everywherePosSubset s ⊆ s
-- Mathlib.Topology.Algebra.UniformRing
/-- The completion map as a ring morphism.  -/
UniformSpace.Completion.mapRingHom : {α : Type u_1} →
  [inst : Ring α] →
    [inst_1 : UniformSpace α] →
      [inst_2 : IsTopologicalRing α] →
        [inst_3 : IsUniformAddGroup α] →
          {β : Type u} →
            [inst_4 : UniformSpace β] →
              [inst_5 : Ring β] →
                [inst_6 : IsUniformAddGroup β] →
                  [inst_7 : IsTopologicalRing β] →
                    (f : α →+* β) → Continuous ⇑f → UniformSpace.Completion α →+* UniformSpace.Completion β
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.Equiv.beq_congr : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α]
  {m₃ m₄ : Std.HashSet.Raw α}, m₁.WF → m₂.WF → m₃.WF → m₄.WF → m₁.Equiv m₃ → m₂.Equiv m₄ → (m₁ == m₂) = (m₃ == m₄)
-- Mathlib.RingTheory.PowerBasis
PowerBasis.liftEquiv'_apply_coe : ∀ {S : Type u_2} [inst : Ring S] {A : Type u_4} {B : Type u_5} [inst_1 : CommRing A] [inst_2 : CommRing B]
  [inst_3 : Algebra A B] [inst_4 : Algebra A S] [inst_5 : IsDomain B] (pb : PowerBasis A S) (a : S →ₐ[A] B),
  ↑(pb.liftEquiv' a) = a pb.gen
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.ratUnits_performRupCheck : ∀ {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (rupHints : Array ℕ),
  (f.performRupCheck rupHints).1.ratUnits = f.ratUnits
-- Mathlib.Algebra.Order.Hom.Basic
RingSeminormClass.toSubmultiplicativeHomClass : ∀ {F : Type u_7} {α : outParam (Type u_8)} {β : outParam (Type u_9)} {inst : NonUnitalNonAssocRing α}
  {inst_1 : Semiring β} {inst_2 : PartialOrder β} {inst_3 : FunLike F α β} [self : RingSeminormClass F α β],
  SubmultiplicativeHomClass F α β
-- Mathlib.Analysis.Complex.TaylorSeries
/-- **Alias** of `Complex.taylorSeries_eq_on_eball`.

---

A function that is complex differentiable on the open ball of radius `r ≤ ∞` around `c`
is given by evaluating its Taylor series at `c` on this open ball.  -/
Complex.taylorSeries_eq_on_emetric_ball : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [CompleteSpace E] ⦃f : ℂ → E⦄ ⦃c : ℂ⦄
  ⦃r : ENNReal⦄,
  DifferentiableOn ℂ f (Metric.eball c r) →
    ∀ ⦃z : ℂ⦄, z ∈ Metric.eball c r → ∑' (n : ℕ), (↑n.factorial)⁻¹ • (z - c) ^ n • iteratedDeriv n f c = f z
-- Lean.Meta.Tactic.Grind.Arith.CommRing.RingM
Lean.Meta.Grind.Arith.CommRing.isField : Lean.Meta.Grind.Arith.CommRing.RingM Bool
-- Mathlib.Topology.LocallyConstant.Basic
IsLocallyConstant.iff_isOpen_fiber_apply : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] {f : X → Y},
  IsLocallyConstant f ↔ ∀ (x : X), IsOpen (f ⁻¹' {f x})
-- Mathlib.RingTheory.Smooth.StandardSmooth
Algebra.instIsStandardSmoothOfSubsingleton : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [Subsingleton S],
  Algebra.IsStandardSmooth R S
-- Mathlib.Topology.MetricSpace.Snowflaking
Metric.Snowflaking.mk : {X : Type u_1} → {α : ℝ} → {hα₀ : 0 < α} → {hα₁ : α ≤ 1} → X → Metric.Snowflaking X α hα₀ hα₁
-- Mathlib.Analysis.Normed.Group.Pointwise
sphere_one_div_singleton : ∀ {E : Type u_1} [inst : SeminormedCommGroup E] (δ : ℝ) (x : E), Metric.sphere 1 δ / {x} = Metric.sphere x⁻¹ δ
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
WeierstrassCurve.Jacobian.eval_polynomialY_of_Z_ne_zero : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Jacobian F} {P : Fin 3 → F},
  P 2 ≠ 0 →
    (MvPolynomial.eval P) W.polynomialY / P 2 ^ 3 =
      Polynomial.evalEval (P 0 / P 2 ^ 2) (P 1 / P 2 ^ 3) W.toAffine.polynomialY
-- Mathlib.Algebra.Module.ZLattice.Basic
ZSpan.map : ∀ {E : Type u_1} {ι : Type u_2} {K : Type u_3} [inst : NormedField K] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace K E] (b : Module.Basis ι K E) {F : Type u_4} [inst_3 : AddCommGroup F] [inst_4 : Module K F]
  (f : E ≃ₗ[K] F),
  Submodule.map (↑(LinearEquiv.restrictScalars ℤ f)) (Submodule.span ℤ (Set.range ⇑b)) =
    Submodule.span ℤ (Set.range ⇑(b.map f))
-- Mathlib.Analysis.BoxIntegral.Partition.Measure
BoxIntegral.BoxAdditiveMap.volume.eq_1 : ∀ {ι : Type u_1} [inst : Fintype ι] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E],
  BoxIntegral.BoxAdditiveMap.volume = MeasureTheory.volume.toBoxAdditive.toSMul
-- Mathlib.Order.BooleanAlgebra.Set
Set.union_inter_compl_right_subset : ∀ {α : Type u_1} (s t : Set α), (s ∪ t) ∩ tᶜ ⊆ s
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
/-- The `v`-adic absolute value on `K` defined as the norm of `v` raised to negative `v`-adic
valuation  -/
NumberField.HeightOneSpectrum.adicAbv : (K : Type u_1) →
  [inst : Field K] →
    {R : Type u_2} →
      [inst_1 : CommRing R] →
        [inst_2 : Algebra R K] →
          [IsDedekindDomain R] →
            [IsFractionRing R K] →
              IsDedekindDomain.HeightOneSpectrum R → [Module.Finite ℤ R] → [Module.Free ℤ R] → AbsoluteValue K ℝ
-- Mathlib.Analysis.CStarAlgebra.Multiplier
DoubleCentralizer.one_snd : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : NormedSpace 𝕜 A] [inst_3 : SMulCommClass 𝕜 A A] [inst_4 : IsScalarTower 𝕜 A A],
  (DoubleCentralizer.toProd 1).2 = 1
-- Mathlib.RingTheory.Invariant.Basic
/-- A technical lemma for `fixed_of_fixed1`.  -/
_private.Mathlib.RingTheory.Invariant.Basic.0.fixed_of_fixed1_aux2 : ∀ {B : Type u_2} [inst : CommRing B] (G : Type u_3) [inst_1 : Group G] [Finite G] [inst_3 : MulSemiringAction G B]
  (Q : Ideal B) [Q.IsPrime] (b₀ : B),
  (∀ (g : G), g • Q = Q → (algebraMap B (B ⧸ Q)) (g • b₀) = (algebraMap B (B ⧸ Q)) b₀) →
    ∃ a b,
      (∀ (g : G), g • a = a) ∧
        a ∉ Q ∧ ∀ (g : G), (algebraMap B (B ⧸ Q)) (g • b) = (algebraMap B (B ⧸ Q)) (if g • Q = Q then a * b₀ else 0)
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.liftCycles_i : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁)
  {A : C} (x : A ⟶ (X.H n₀).obj (CategoryTheory.ComposableArrows.mk₁ g))
  (hx : CategoryTheory.CategoryStruct.comp x (X.δ f g n₀ n₁ hn₁) = 0),
  CategoryTheory.CategoryStruct.comp (X.liftCycles f g n₀ n₁ hn₁ x hx) (X.iCycles f g n₀) = x
-- Mathlib.Data.Nat.Factorial.Basic
Nat.ascFactorialBinary.eq_def : ∀ (n k : ℕ),
  n.ascFactorialBinary k =
    match k with
    | 0 => 1
    | 1 => n
    | k@h:n_1.succ.succ => n.ascFactorialBinary (k / 2) * (n + k / 2).ascFactorialBinary ((k + 1) / 2)
-- Mathlib.Topology.Constructions.SumProd
Homeomorph.coe_sumComm : ∀ (X : Type u) (Y : Type v) [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  ⇑(Homeomorph.sumComm X Y) = Sum.swap