mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_naturality_naturality_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.Pseudofunctor B C} (η : F ⟶ G) {a b : B} {a' : C} {f g : a ⟶ b} (β : f ⟶ g) (h : G.obj b ⟶ a')
  {Z : F.obj a ⟶ a'}
  (h_1 : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (η.app a) (G.map g)) h ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerRight (F.map₂ β) (η.app b)) h)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (η.naturality g).hom h) h_1) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (η.naturality f).hom h)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (η.app a) (G.map f) h).hom
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Bicategory.whiskerLeft (η.app a) (CategoryTheory.Bicategory.whiskerRight (G.map₂ β) h))
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (η.app a) (G.map g) h).inv h_1)))
-- Init.Data.UInt.Bitwise
UInt16.neg_one_shiftLeft_or_shiftLeft : ∀ {a b : UInt16}, (-1) <<< b ||| a <<< b = (-1) <<< b
-- Mathlib.AlgebraicGeometry.ResidueField
AlgebraicGeometry.Scheme.Spec.map_residueFieldIso_inv_eq_fromSpecResidueField_assoc : ∀ (R : CommRingCat) (x : ↥(AlgebraicGeometry.Spec R)) {Z : AlgebraicGeometry.Scheme}
  (h : AlgebraicGeometry.Spec (CommRingCat.of ↑R) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.Spec.residueFieldIso R x).inv)
      (CategoryTheory.CategoryStruct.comp
        (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap (↑R) x.asIdeal.ResidueField))) h) =
    CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Spec R).fromSpecResidueField x) h
-- Mathlib.Analysis.Polynomial.CauchyBound
Polynomial.cauchyBound_X : ∀ {K : Type u_1} [inst : NormedDivisionRing K], Polynomial.X.cauchyBound = 1
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.balanceL!.match_3.congr_eq_2 : ∀ {α : Type u_1} {β : α → Type u_2}
  (motive : Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl α β → Sort u_3)
  (ll lr : Std.DTreeMap.Internal.Impl α β)
  (h_1 :
    (lls : ℕ) →
      (k : α) →
        (v : β k) →
          (l r : Std.DTreeMap.Internal.Impl α β) →
            (lrs : ℕ) →
              (lrk : α) →
                (lrv : β lrk) →
                  (lrl lrr : Std.DTreeMap.Internal.Impl α β) →
                    motive (Std.DTreeMap.Internal.Impl.inner lls k v l r)
                      (Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr))
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l r : Std.DTreeMap.Internal.Impl α β) →
            motive (Std.DTreeMap.Internal.Impl.inner size k v l r) Std.DTreeMap.Internal.Impl.leaf)
  (h_3 : (x : Std.DTreeMap.Internal.Impl α β) → motive Std.DTreeMap.Internal.Impl.leaf x) (size : ℕ) (k : α) (v : β k)
  (l r : Std.DTreeMap.Internal.Impl α β),
  ll = Std.DTreeMap.Internal.Impl.inner size k v l r →
    lr = Std.DTreeMap.Internal.Impl.leaf →
      (match ll, lr with
        | Std.DTreeMap.Internal.Impl.inner lls k v l r, Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr =>
          h_1 lls k v l r lrs lrk lrv lrl lrr
        | Std.DTreeMap.Internal.Impl.inner size k v l r, Std.DTreeMap.Internal.Impl.leaf => h_2 size k v l r
        | Std.DTreeMap.Internal.Impl.leaf, x => h_3 x) ≍
        h_2 size k v l r
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get_union_of_contains_eq_false_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [inst_2 : LawfulBEq α] (h₁ : (↑m₁).WF) (h₂ : (↑m₂).WF) {k : α} (contains_eq_false : m₁.contains k = false)
  {h' : (m₁.union m₂).contains k = true}, (m₁.union m₂).get k h' = m₂.get k ⋯
-- Mathlib.CategoryTheory.Category.PartialFun
Pointed.Iso.mk.congr_simp : ∀ {α β : Pointed} (e e_1 : α.X ≃ β.X) (e_e : e = e_1) (he : e α.point = β.point),
  Pointed.Iso.mk e he = Pointed.Iso.mk e_1 ⋯
-- Mathlib.Data.Nat.Prime.Basic
Nat.not_prime_iff_exists_dvd_ne : ∀ {n : ℕ}, 2 ≤ n → (¬Nat.Prime n ↔ ∃ m, m ∣ n ∧ m ≠ 1 ∧ m ≠ n)
-- Mathlib.GroupTheory.Perm.Cycle.Factors
/-- Factors a permutation `f` into a list of disjoint cyclic permutations that multiply to `f`,
without a linear order.  -/
Equiv.Perm.truncCycleFactors : {α : Type u_2} →
  [DecidableEq α] →
    [Fintype α] →
      (f : Equiv.Perm α) → Trunc { l // l.prod = f ∧ (∀ g ∈ l, g.IsCycle) ∧ List.Pairwise Equiv.Perm.Disjoint l }
-- Mathlib.Order.Interval.Finset.Fin
Fin.map_castSuccEmb_Ioo : ∀ {n : ℕ} (i j : Fin n), Finset.map Fin.castSuccEmb (Finset.Ioo i j) = Finset.Ioo i.castSucc j.castSucc
-- Init.Data.BitVec.Lemmas
BitVec.toFin_allOnes : ∀ {w : ℕ}, (BitVec.allOnes w).toFin = Fin.ofNat (2 ^ w) (2 ^ w - 1)
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- **Alias** of `Metric.hausdorffEDist_def`. -/
EMetric.hausdorffEdist_def : ∀ {α : Type u_2} [inst : PseudoEMetricSpace α] (s t : Set α),
  Metric.hausdorffEDist s t = max (⨆ x ∈ s, Metric.infEDist x t) (⨆ y ∈ t, Metric.infEDist y s)
-- Mathlib.Order.LiminfLimsup
liminf_finset_inf' : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : ConditionallyCompleteLinearOrder β] {f : Filter α}
  {F : ι → α → β} {s : Finset ι} (hs : s.Nonempty),
  autoParam (∀ i ∈ s, Filter.IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) f (F i)) liminf_finset_inf'._auto_1 →
    autoParam (∀ i ∈ s, Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f (F i)) liminf_finset_inf'._auto_3 →
      Filter.liminf (fun a => s.inf' hs fun i => F i a) f = s.inf' hs fun i => Filter.liminf (F i) f
-- Lean.Meta.Sym.SymM
Lean.Meta.Sym.instInhabitedSymExtension.default : {σ : Type} → Lean.Meta.Sym.SymExtension σ
-- Init.Data.Array.Erase
Array.erase_eq_eraseP : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] (a : α) (xs : Array α), xs.erase a = xs.eraseP fun x => a == x
-- Mathlib.Algebra.Group.ConjFinite
instFintypeConjClassesOfDecidableRelIsConj : {α : Type u_1} → [inst : Monoid α] → [Fintype α] → [DecidableRel IsConj] → Fintype (ConjClasses α)
-- Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
/-- The **Riesz-Markov-Kakutani representation theorem**: given a positive linear functional `Λ`,
the integral of `f` with respect to the `rieszMeasure` associated to `Λ` is equal to `Λ f`.  -/
RealRMK.integral_rieszMeasure : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : T2Space X] [inst_2 : MeasurableSpace X] [inst_3 : BorelSpace X]
  (Λ : CompactlySupportedContinuousMap X ℝ →ₚ[ℝ] ℝ) [inst_4 : LocallyCompactSpace X]
  (f : CompactlySupportedContinuousMap X ℝ), ∫ (x : X), f x ∂ RealRMK.rieszMeasure Λ = Λ f
-- Mathlib.RingTheory.Extension.Presentation.Submersive
Algebra.PreSubmersivePresentation.jacobian_eq_jacobiMatrix_det : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.PreSubmersivePresentation R S ι σ) [inst_3 : Fintype σ] [inst_4 : DecidableEq σ],
  P.jacobian = (algebraMap P.Ring S) P.jacobiMatrix.det
-- Mathlib.Analysis.Calculus.ContDiff.Basic
contDiffAt_const : ∀ {𝕜 : 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] {x : E} {n : WithTop ℕ∞}
  {c : F}, ContDiffAt 𝕜 n (fun x => c) x
-- Mathlib.Data.Sigma.Basic
Sigma.fst_surjective_iff : ∀ {α : Type u_1} {β : α → Type u_4}, Function.Surjective Sigma.fst ↔ ∀ (a : α), Nonempty (β a)
-- Mathlib.CategoryTheory.Limits.Connected
CategoryTheory.Limits.constCone_π : ∀ (J : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} C]
  (X : C),
  (CategoryTheory.Limits.constCone J X).π = CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.const J).obj X)
-- Mathlib.Order.Interval.Finset.Basic
/-- `Finset.cons` version of `Finset.Ico_insert_right`.  -/
Finset.Icc_eq_cons_Ico : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : LocallyFiniteOrder α] {a b : α},
  a ≤ b → Finset.Icc a b = Finset.cons b (Finset.Ico a b) ⋯
-- Mathlib.GroupTheory.Complement
/-- **Alias** of `Subgroup.IsComplement.card_mul_card`. -/
Subgroup.IsComplement.card_mul : ∀ {G : Type u_1} [inst : Group G] {S T : Set G}, Subgroup.IsComplement S T → Nat.card ↑S * Nat.card ↑T = Nat.card G
-- Mathlib.Topology.Constructions
IsClosedMap.subtype_mk : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {p : X → Prop} {f : Y → X},
  IsClosedMap f → ∀ (hp : ∀ (x : Y), p (f x)), IsClosedMap fun x => ⟨f x, ⋯⟩
-- Aesop.Search.Expansion
Aesop.SafeRulesResult : Type
-- Mathlib.RingTheory.AdicCompletion.LocalRing
isLocalRing_of_isAdicComplete_maximal : ∀ {R : Type u_1} [inst : CommRing R] (m : Ideal R) [m.IsMaximal] [IsAdicComplete m R], IsLocalRing R
-- Mathlib.Topology.Maps.Proper.Basic
/-- By definition, a proper map is continuous.  -/
IsProperMap.continuous : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  IsProperMap f → Continuous f
-- Mathlib.Data.DFinsupp.Order
DFinsupp.single_mono : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Zero (α i)] [inst_1 : (i : ι) → Preorder (α i)] {i : ι}
  [inst_2 : DecidableEq ι], Monotone (DFinsupp.single i)
-- Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
/-- The **Bohr-Mollerup theorem**: the Gamma function is the *unique* log-convex, positive-valued
function on the positive reals which satisfies `f 1 = 1` and `f (x + 1) = x * f x` for all `x`.  -/
Real.eq_Gamma_of_log_convex : ∀ {f : ℝ → ℝ},
  ConvexOn ℝ (Set.Ioi 0) (Real.log ∘ f) →
    (∀ {y : ℝ}, 0 < y → f (y + 1) = y * f y) →
      (∀ {y : ℝ}, 0 < y → 0 < f y) → f 1 = 1 → Set.EqOn f Real.Gamma (Set.Ioi 0)
-- Mathlib.CategoryTheory.Monoidal.Mod
/-- The forgetful functor from additive module objects to the ambient category.  -/
CategoryTheory.AddMod.forget : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] →
            (A : C) → [inst_4 : CategoryTheory.AddMonObj A] → CategoryTheory.Functor (CategoryTheory.AddMod D A) D
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnSeries.orderTop_sub_pos : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : Zero Γ] [inst_2 : AddCommGroup R] [inst_3 : One R]
  {g : Γ}, 0 < g → ∀ (r : R), 0 < (1 + (HahnSeries.single g) r - 1).orderTop
-- Mathlib.MeasureTheory.Integral.CircleAverage
/-- If `f x` is smaller than `a` on for every point of the circle, then the circle average of `f` is
smaller than `a`.
 -/
Real.circleAverage_mono_on_of_le_circle : ∀ {c : ℂ} {R : ℝ} {f : ℂ → ℝ} {a : ℝ},
  CircleIntegrable f c R → (∀ x ∈ Metric.sphere c |R|, f x ≤ a) → Real.circleAverage f c R ≤ a
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.isEmpty_inter_iff : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ((m₁ ∩ m₂).isEmpty = true ↔ ∀ k ∈ m₁, k ∉ m₂)
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
/-- the auxiliary object of a left fraction  -/
CategoryTheory.MorphismProperty.LeftFraction.Y' : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W : CategoryTheory.MorphismProperty C} → {X Y : C} → W.LeftFraction X Y → C
-- Mathlib.Topology.Category.CompHausLike.Limits
CompHausLike.HasExplicitFiniteCoproducts.hasProp : ∀ {P : TopCat → Prop} [self : CompHausLike.HasExplicitFiniteCoproducts P] {α : Type w} [Finite α]
  (X : α → CompHausLike P), CompHausLike.HasExplicitFiniteCoproduct X
-- Mathlib.Data.Finset.Union
Finset.disjiUnion_eq_biUnion : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] (s : Finset α) (f : α → Finset β) (hf : (↑s).PairwiseDisjoint f),
  s.disjiUnion f hf = s.biUnion f
-- Mathlib.FieldTheory.Finite.Polynomial
/-- `MvPolynomial.eval` as a `K`-linear map.  -/
MvPolynomial.evalₗ : (K : Type u_1) → (σ : Type u_2) → [inst : CommSemiring K] → MvPolynomial σ K →ₗ[K] (σ → K) → K
-- Mathlib.CategoryTheory.GradedObject.Braiding
CategoryTheory.GradedObject.Monoidal.symmetry_assoc : ∀ {I : Type u_1} [inst : AddCommMonoid I] {C : Type u_2} [inst_1 : CategoryTheory.Category.{v_1, u_2} C]
  [inst_2 : CategoryTheory.MonoidalCategory C] (X Y : CategoryTheory.GradedObject I C)
  [inst_3 : CategoryTheory.SymmetricCategory C] [inst_4 : X.HasTensor Y] [inst_5 : Y.HasTensor X]
  {Z : CategoryTheory.GradedObject I C} (h : CategoryTheory.GradedObject.Monoidal.tensorObj X Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.braiding X Y).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.braiding Y X).hom h) =
    h
-- Lean.Parser.Term
Lean.Parser.Term.letEqnsDecl.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Analysis.Meromorphic.NormalForm
/-- If `f` is any function and `g` is analytic without zero in `U`, then `f` is
meromorphic in normal form on `U` iff `g * f` is meromorphic in normal form on
`U`.
 -/
meromorphicNFOn_mul_iff_right_of_analyticOnNhd : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {U : Set 𝕜} {f g : 𝕜 → 𝕜},
  AnalyticOnNhd 𝕜 g U → (∀ u ∈ U, g u ≠ 0) → (MeromorphicNFOn (g * f) U ↔ MeromorphicNFOn f U)
-- Std.Data.Internal.List.Associative
Std.Internal.List.maxKey!_insertEntry : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  [inst_4 : Inhabited α] {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α} {v : β k},
      Std.Internal.List.maxKey! (Std.Internal.List.insertEntry k v l) =
        (Std.Internal.List.maxKey? l).elim k fun k' => if (compare k' k).isLE = true then k else k'
-- Mathlib.RingTheory.Ideal.Prod
Ideal.isPrime_ideal_prod_top' : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] {I : Ideal S} [h : I.IsPrime], (⊤.prod I).IsPrime
-- Mathlib.MeasureTheory.Group.Action
MeasureTheory.measure_symmDiff_neg_vadd : ∀ {G : Type u} {α : Type w} {m : MeasurableSpace α} [inst : AddGroup G] [inst_1 : AddAction G α]
  (μ : MeasureTheory.Measure α) [MeasureTheory.VAddInvariantMeasure G α μ] (c : G) (s t : Set α),
  μ (symmDiff s (-c +ᵥ t)) = μ (symmDiff (c +ᵥ s) t)
-- Batteries.Data.List.Lemmas
_private.Batteries.Data.List.Lemmas.0.List.countPBefore.go.match_1.splitter : {α : Type u_1} →
  (motive : List α → ℕ → ℕ → Sort u_2) →
    (x : List α) →
      (x_1 x_2 : ℕ) →
        ((head : α) → (tail : List α) → (s : ℕ) → motive (head :: tail) 0 s) →
          ((a : α) → (xs : List α) → (i s : ℕ) → motive (a :: xs) i.succ s) →
            ((x s : ℕ) → motive [] x s) → motive x x_1 x_2
-- Mathlib.Data.Set.Insert
Set.inter_singleton_of_mem : ∀ {α : Type u_1} {s : Set α} {a : α}, a ∈ s → s ∩ {a} = {a}
-- Lean.Meta.Tactic.Grind.CollectParams
_private.Lean.Meta.Tactic.Grind.CollectParams.0.Lean.Meta.Grind.Collector.State.anchors : Lean.Meta.Grind.Collector.State✝ → Array Lean.Meta.Grind.TAnchor✝
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getD_diff : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α],
  m₁.WF → m₂.WF → ∀ {k : α} {fallback : β}, (m₁ \ m₂).getD k fallback = if k ∈ m₂ then fallback else m₁.getD k fallback
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.EMatch.instInhabitedState.default : Lean.Meta.Grind.EMatch.State
-- Mathlib.Data.Set.Semiring
SetSemiring.instCompleteBooleanAlgebra : {α : Type u_1} → CompleteBooleanAlgebra (SetSemiring α)
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.Sorted.brecOn : ∀
  {motive :
    {basis : Tactic.ComputeAsymptotics.Basis} →
      (a : Tactic.ComputeAsymptotics.MultiseriesExpansion basis) → a.Sorted → Prop}
  {basis : Tactic.ComputeAsymptotics.Basis} {a : Tactic.ComputeAsymptotics.MultiseriesExpansion basis} (t : a.Sorted),
  (∀ {basis : Tactic.ComputeAsymptotics.Basis} (a : Tactic.ComputeAsymptotics.MultiseriesExpansion basis)
      (t : a.Sorted), Tactic.ComputeAsymptotics.MultiseriesExpansion.Sorted.below t → motive a t) →
    motive a t
-- Std.Time.Format.Modifier
Std.Time.Text.full.sizeOf_spec : sizeOf Std.Time.Text.full = 1
-- Mathlib.CategoryTheory.Yoneda
/-- A type-level equivalence between sections of a functor and morphisms from a terminal functor
to it. We use the constant functor on a given singleton type here as a specific choice of terminal
functor.  -/
CategoryTheory.Functor.sectionsEquivHom : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (F : CategoryTheory.Functor C (Type u₂)) →
      (X : Type u₂) → [Unique X] → ↑F.sections ≃ ((CategoryTheory.Functor.const C).obj X ⟶ F)
-- Mathlib.SetTheory.ZFC.Basic
/-- The intersection operator, the collection of elements in all of the elements of a ZFC set. We
define `⋂₀ ∅ = ∅`. Uses `⋂₀` notation, scoped under the `ZFSet` namespace.  -/
ZFSet.«term⋂₀_» : Lean.ParserDescr
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
Matrix.star_vecMul : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : NonUnitalSemiring α] [inst_1 : Fintype m] [inst_2 : StarRing α]
  (M : Matrix m n α) (v : m → α), star (Matrix.vecMul v M) = M.conjTranspose.mulVec (star v)
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.XIsoOfEq_inv_naturality_assoc : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {K L : HomologicalComplex V c} (φ : K ⟶ L)
  {n n' : ι} (h : n = n') {Z : V} (h_1 : L.X n ⟶ Z),
  CategoryTheory.CategoryStruct.comp (φ.f n') (CategoryTheory.CategoryStruct.comp (L.XIsoOfEq h).inv h_1) =
    CategoryTheory.CategoryStruct.comp (K.XIsoOfEq h).inv (CategoryTheory.CategoryStruct.comp (φ.f n) h_1)
-- Mathlib.LinearAlgebra.Projectivization.Basic
Projectivization.mk_rep : ∀ {K : Type u_1} {V : Type u_2} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  (v : Projectivization K V), Projectivization.mk K v.rep ⋯ = v
-- Init.Grind.Ring.Basic
/-- The canonical map from the integers is consistent with negation.  -/
Lean.Grind.Ring.intCast_neg : ∀ {α : Type u} [self : Lean.Grind.Ring α] (i : ℤ), ↑(-i) = -↑i
-- Mathlib.Combinatorics.Quiver.Path
_private.Mathlib.Combinatorics.Quiver.Path.0.Quiver.Path.length.match_1.eq_1 : ∀ {V : Type u_2} [inst : Quiver V] {a : V} (motive : (x : V) → Quiver.Path a x → Sort u_3)
  (h_1 : Unit → motive a Quiver.Path.nil)
  (h_2 : (x b : V) → (p : Quiver.Path a b) → (a_1 : b ⟶ x) → motive x (p.cons a_1)),
  (match a, Quiver.Path.nil with
    | .(a), Quiver.Path.nil => h_1 ()
    | x, p.cons a => h_2 x b p a) =
    h_1 ()
-- Mathlib.Algebra.Quandle
Quandle.toRack : {α : Type u_1} → [self : Quandle α] → Rack α
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.BinaryBicone.ofIso_inl : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {P P' Q Q' : C} (b : CategoryTheory.Limits.BinaryBicone P Q) (eP : P ≅ P') (eQ : Q ≅ Q'),
  (b.ofIso eP eQ).inl = CategoryTheory.CategoryStruct.comp eP.inv b.inl
-- Mathlib.Data.Nat.Count
/-- **Alias** of the reverse direction of `Nat.count_iff_forall_not`. -/
Nat.count_of_forall_not : ∀ {p : ℕ → Prop} [inst : DecidablePred p] {n : ℕ}, (∀ m < n, ¬p m) → Nat.count p n = 0
-- Lean.Data.JsonRpc
Lean.JsonRpc.instBEqNotification : {α : Type u_1} → [BEq α] → BEq (Lean.JsonRpc.Notification α)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.DefinitionParams.mk : Lean.Lsp.TextDocumentPositionParams → Lean.Lsp.DefinitionParams
-- Lean.Parser.Extra
/-- No-op parser combinator that prints a line break.
The line break is soft if the combinator is followed
by an ungrouped parser (see ppAllowUngrouped), otherwise hard.  -/
Lean.Parser.ppHardLineUnlessUngrouped : Lean.Parser.Parser
-- Mathlib.Topology.Algebra.Support
isClosed_tsupport : ∀ {X : Type u_1} {α : Type u_2} [inst : Zero α] [inst_1 : TopologicalSpace X] (f : X → α), IsClosed (tsupport f)
-- Mathlib.Algebra.Group.Subgroup.MulOpposite
Subgroup.mem_op : ∀ {G : Type u_2} [inst : Group G] {x : Gᵐᵒᵖ} {S : Subgroup G}, x ∈ S.op ↔ MulOpposite.unop x ∈ S
-- Mathlib.Algebra.Group.Equiv.Defs
AddEquivClass.apply_coe_symm_apply : ∀ {α : Type u_9} {β : Type u_10} [inst : Add α] [inst_1 : Add β] {F : Type u_11} [inst_2 : EquivLike F α β]
  [inst_3 : AddEquivClass F α β] (e : F) (x : β), e ((↑e).symm x) = x
-- Std.Data.DTreeMap.Internal.Lemmas
_private.Std.Data.DTreeMap.Internal.Lemmas.0.Std.DTreeMap.Internal.Impl.Const.get_insertMany_list.match_1.splitter : {β : Type u_1} →
  (motive : Option β → Sort u_2) →
    (x : Option β) → ((v : β) → x = some v → motive (some v)) → (x = none → motive none) → motive x
-- Mathlib.Topology.MetricSpace.CoveringNumbers
Metric.exists_set_encard_eq_packingNumber : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] {A : Set X} {ε : NNReal},
  Metric.packingNumber ε A ≠ ⊤ → ∃ C ⊆ A, C.Finite ∧ Metric.IsSeparated (↑ε) C ∧ C.encard = Metric.packingNumber ε A
-- Mathlib.Algebra.Category.CommHopfAlgCat
CommHopfAlgCat.of.injEq : ∀ (R : Type u) [inst : CommRing R] (X : Type v) [commRing : CommRing X] [hopfAlgebra : HopfAlgebra R X] (X_1 : Type v)
  (commRing_1 : CommRing X_1) (hopfAlgebra_1 : HopfAlgebra R X_1),
  ({ X := X, commRing := commRing, hopfAlgebra := hopfAlgebra } =
      { X := X_1, commRing := commRing_1, hopfAlgebra := hopfAlgebra_1 }) =
    (X = X_1 ∧ commRing ≍ commRing_1 ∧ hopfAlgebra ≍ hopfAlgebra_1)
-- Init.Data.SInt.Lemmas
instLawfulIdentityInt16HAddOfNat : Std.LawfulIdentity (fun x1 x2 => x1 + x2) 0
-- Mathlib.Order.SupIndep
Finset.supIndep_pair : ∀ {α : Type u_1} {ι : Type u_3} [inst : Lattice α] [inst_1 : OrderBot α] {f : ι → α} [inst_2 : DecidableEq ι] {i j : ι},
  i ≠ j → ({i, j}.SupIndep f ↔ Disjoint (f i) (f j))
-- Mathlib.Algebra.Order.Monoid.Unbundled.Pow
lt_of_nsmul_lt_nsmul_right : ∀ {M : Type u_3} [inst : AddMonoid M] [inst_1 : LinearOrder M] [AddLeftMono M] [AddRightMono M] {a b : M} (n : ℕ),
  n • a < n • b → a < b
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
_private.Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass.0.PeriodPair.relation_sub_coe : ∀ (L : PeriodPair) (x : ℂ) (l : ↥L.lattice), PeriodPair.relation✝ L (x - ↑l) = PeriodPair.relation✝ L x
-- Mathlib.Order.SymmDiff
symmDiff_of_ge : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, b ≤ a → symmDiff a b = a \ b
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
LinearMap.BilinMap.toQuadraticMap_list_sum : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (B : List (LinearMap.BilinMap R M N)),
  B.sum.toQuadraticMap = (List.map LinearMap.BilinMap.toQuadraticMap B).sum
-- Mathlib.Algebra.Order.Field.Basic
Mathlib.Meta.Positivity.div_nonneg_of_nonneg_of_pos : ∀ {α : Type u_4} [inst : GroupWithZero α] [inst_1 : PartialOrder α] {a b : α} [PosMulReflectLT α],
  0 ≤ a → 0 < b → 0 ≤ a / b
-- Mathlib.Data.Rat.Cast.Order
Rat.preimage_cast_uIoc : ∀ {K : Type u_5} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] (p q : ℚ),
  Rat.cast ⁻¹' Set.uIoc ↑p ↑q = Set.uIoc p q
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionParams.mk.injEq : ∀ (toTextDocumentPositionParams toTextDocumentPositionParams_1 : Lean.Lsp.TextDocumentPositionParams),
  ({ toTextDocumentPositionParams := toTextDocumentPositionParams } =
      { toTextDocumentPositionParams := toTextDocumentPositionParams_1 }) =
    (toTextDocumentPositionParams = toTextDocumentPositionParams_1)
-- Mathlib.Analysis.Normed.Module.Ball.Pointwise
closure_thickening : ∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] [NormedSpace ℝ E] {δ : ℝ},
  0 < δ → ∀ (s : Set E), closure (Metric.thickening δ s) = Metric.cthickening δ s