mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Int.Linear
Int.Internal.Linear.le_norm : ∀ (ctx : Int.Internal.Linear.Context) (p₁ p₂ : Int.Internal.Linear.Poly),
  p₁.norm.beq' p₂ = true → Int.Internal.Linear.Poly.denote' ctx p₁ ≤ 0 → Int.Internal.Linear.Poly.denote' ctx p₂ ≤ 0
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.instCommRingOfIsAbsoluteValue : {α : Type u_1} →
  [inst : Field α] →
    [inst_1 : LinearOrder α] →
      [inst_2 : IsStrictOrderedRing α] →
        {β : Type u_3} → [inst_3 : CommRing β] → {abv : β → α} → [IsAbsoluteValue abv] → CommRing (CauSeq β abv)
-- Lean.Declaration
Lean.Declaration.defnDecl.sizeOf_spec : ∀ (val : Lean.DefinitionVal), sizeOf (Lean.Declaration.defnDecl val) = 1 + sizeOf val
-- Mathlib.Combinatorics.Enumerative.InclusionExclusion
/-- **Inclusion-exclusion principle** for the sum of a function over an intersection of complements.

The sum of a function `f` over the intersection of the complements of the `S i` over `i ∈ s` is the
alternating sum of the sums of `f` over the intersections of the `S i`.  -/
Finset.inclusion_exclusion_sum_inf_compl : ∀ {ι : Type u_1} {α : Type u_2} {G : Type u_3} [inst : AddCommGroup G] [inst_1 : DecidableEq α] [inst_2 : Fintype α]
  (s : Finset ι) (S : ι → Finset α) (f : α → G),
  ∑ a ∈ s.inf fun i => (S i)ᶜ, f a = ∑ t ∈ s.powerset, (-1) ^ t.card • ∑ a ∈ t.inf S, f a
-- Lean.Parser.Do
Lean.Parser.Term.doNested.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.GroupTheory.GroupAction.Quotient
MulAction.injective_ofQuotientStabilizer : ∀ (G : Type u) {X : Type v} [inst : Group G] [inst_1 : MulAction G X] (x : X),
  Function.Injective (MulAction.ofQuotientStabilizer G x)
-- Mathlib.CategoryTheory.Adjunction.PartialAdjoint
/-- Given a functor `F : C ⥤ D`, this is a predicate on objects `X : D` corresponding
to the domain of definition of the (partial) right adjoint of `F`.  -/
CategoryTheory.Functor.rightAdjointObjIsDefined : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Functor C D → CategoryTheory.ObjectProperty D
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getD_eq_getD_get? : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {a : α}
  {fallback : β a}, m.getD a fallback = (m.get? a).getD fallback
-- Mathlib.CategoryTheory.Subobject.MonoOver
/-- The object property in `Over X` of the structure morphism being a monomorphism.  -/
CategoryTheory.Over.isMono : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] → (X : C) → CategoryTheory.ObjectProperty (CategoryTheory.Over X)
-- Mathlib.AlgebraicTopology.DoldKan.FunctorN
AlgebraicTopology.DoldKan.N₂_obj_X_X : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (P : CategoryTheory.Idempotents.Karoubi (CategoryTheory.SimplicialObject C)) (n : ℕ),
  (AlgebraicTopology.DoldKan.N₂.obj P).X.X n = P.X.obj (Opposite.op { len := n })
-- Mathlib.Data.Nat.Choose.Basic
_private.Mathlib.Data.Nat.Choose.Basic.0.Nat.choose.match_1.eq_3 : ∀ (motive : ℕ → ℕ → Sort u_1) (n k : ℕ) (h_1 : (x : ℕ) → motive x 0) (h_2 : (n : ℕ) → motive 0 n.succ)
  (h_3 : (n k : ℕ) → motive n.succ k.succ),
  (match n.succ, k.succ with
    | x, 0 => h_1 x
    | 0, n.succ => h_2 n
    | n.succ, k.succ => h_3 n k) =
    h_3 n k
-- Mathlib.RepresentationTheory.Induced
/-- Given a group homomorphism `φ : G →* H`, this is the functor sending a `G`-representation `A`
to the induced `H`-representation `ind φ A`, with action on maps induced by left tensoring.  -/
Rep.indFunctor : (k : Type u) →
  {G : Type v} →
    {H : Type v'} →
      [inst : CommRing k] →
        [inst_1 : Group G] →
          [inst_2 : Group H] → (G →* H) → CategoryTheory.Functor (Rep.{w, u, v} k G) (Rep.{max (max u v') w, u, v'} k H)
-- Mathlib.Algebra.Polynomial.Div
Polynomial.finiteMultiplicity_of_degree_pos_of_monic : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R}, 0 < p.degree → p.Monic → q ≠ 0 → FiniteMultiplicity p q
-- Mathlib.Analysis.CStarAlgebra.ContinuousMap
BoundedContinuousFunction.instNonUnitalCommCStarAlgebra : {α : Type u_1} →
  {A : Type u_2} →
    [inst : TopologicalSpace α] →
      [inst_1 : NonUnitalCommCStarAlgebra A] → NonUnitalCommCStarAlgebra (BoundedContinuousFunction α A)
-- Init.Data.Ord.Array
List.compare_eq_compare_toArray : ∀ {α : Type u_1} [inst : Ord α] {l₁ l₂ : List α}, compare l₁ l₂ = compare l₁.toArray l₂.toArray
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
/-- The difference `f m₁ - f m₂` is controlled in terms of `‖f‖` and `‖m₁ - m₂‖`, less precise
version. For a more precise but less usable version, see `norm_image_sub_le'`.
The bound is `‖f m - f m'‖ ≤ ‖f‖ * card ι * ‖m - m'‖ * (max ‖m‖ ‖m'‖) ^ (card ι - 1)`.  -/
ContinuousMultilinearMap.norm_image_sub_le : ∀ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_3 : SeminormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] [inst_5 : Fintype ι]
  (f : ContinuousMultilinearMap 𝕜 E G) (m₁ m₂ : (i : ι) → E i),
  ‖f m₁ - f m₂‖ ≤ ‖f‖ * ↑(Fintype.card ι) * max ‖m₁‖ ‖m₂‖ ^ (Fintype.card ι - 1) * ‖m₁ - m₂‖
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.instInvolutiveInvOfMulOpposite.eq_1 : ∀ {M : Type u_1} [inst : InvolutiveInv Mᵐᵒᵖ], DomMulAct.instInvolutiveInvOfMulOpposite = inst
-- Mathlib.Algebra.Polynomial.Derivation
Polynomial.mkDerivation_one_eq_derivative' : ∀ (R : Type u_1) [inst : CommSemiring R], (Polynomial.mkDerivation R) 1 = Polynomial.derivative'
-- Mathlib.Topology.UnitInterval
unitInterval.coe_toNNReal : ∀ (x : ↑unitInterval), ↑(unitInterval.toNNReal x) = ↑x
-- Batteries.Recycling.RBTree.Basic
RBTree.RBNode.Stream.cons.inj : ∀ {α : Type u_1} {v : α} {r : RBTree.RBNode α} {tail : RBTree.RBNode.Stream α} {v_1 : α} {r_1 : RBTree.RBNode α}
  {tail_1 : RBTree.RBNode.Stream α},
  RBTree.RBNode.Stream.cons v r tail = RBTree.RBNode.Stream.cons v_1 r_1 tail_1 → v = v_1 ∧ r = r_1 ∧ tail = tail_1
-- Init.Data.Range.Polymorphic.UpwardEnumerable
Std.PRange.UpwardEnumerable.isSome_succMany? : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerable α]
  [Std.PRange.InfinitelyUpwardEnumerable α] {n : ℕ} {a : α}, (Std.PRange.succMany? n a).isSome = true
-- Mathlib.Combinatorics.SetFamily.AhlswedeZhang
/-- Weighted sum of the size of the truncated suprema of a set family. Relevant to the
Ahlswede-Zhang identity.  -/
AhlswedeZhang.supSum : {α : Type u_1} → [Fintype α] → [DecidableEq α] → Finset (Finset α) → ℚ
-- Mathlib.RingTheory.Valuation.Basic
Valuation.IsEquiv.orderMonoidIso_spec : ∀ {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [inst : LinearOrderedCommGroupWithZero Γ₀]
  [inst_1 : LinearOrderedCommGroupWithZero Γ'₀] [inst_2 : Ring R] {v : Valuation R Γ₀} {w : Valuation R Γ'₀}
  (h : v.IsEquiv w) (a : R), h.orderMonoidIso (v.restrict a) = w.restrict a
-- Std.Data.DHashMap.Internal.RawLemmas
_private.Std.Data.DHashMap.Internal.RawLemmas.0.Std.DHashMap.Internal.Raw₀.insertMany.eq_1 : ∀ {α : Type u} {β : α → Type v} {ρ : Type w} [inst : ForIn Id ρ ((a : α) × β a)] [inst_1 : BEq α] [inst_2 : Hashable α]
  (m : Std.DHashMap.Internal.Raw₀ α β) (l : ρ),
  m.insertMany l =
    (have r := ⟨m, ⋯⟩;
      do
      let __s ←
        forIn l r fun x __s =>
            let r := __s;
            match x with
            | ⟨a, b⟩ =>
              have r := ⟨(↑r).insert a b, ⋯⟩;
              pure (ForInStep.yield r)
      have r :
        { m' //
          ∀ (P : Std.DHashMap.Internal.Raw₀ α β → Prop),
            (∀ {m'' : Std.DHashMap.Internal.Raw₀ α β} {a : α} {b : β a}, P m'' → P (m''.insert a b)) → P m → P m' } :=
        __s
      pure r).run
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.instIsGEObjEIntFunctorETruncGE : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (X : C) (n : ℤ) [t.IsGE X n] (i : EInt),
  t.IsGE ((t.eTruncGE.obj i).obj X) n
-- Std.Data.HashSet.Lemmas
Std.HashSet.Equiv.trans : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ m₃ : Std.HashSet α}, m₁.Equiv m₂ → m₂.Equiv m₃ → m₁.Equiv m₃
-- Mathlib.Algebra.Category.Grp.Limits
AddGrpCat.sectionsπAddMonoidHom.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddGrpCat) (j : J),
  AddGrpCat.sectionsπAddMonoidHom F j = { toFun := fun x => ↑x j, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.LHom.funext : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} {F G : L →ᴸ L'},
  F.onFunction = G.onFunction → F.onRelation = G.onRelation → F = G
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.WalkingPair.equivBool_apply_left : CategoryTheory.Limits.WalkingPair.equivBool CategoryTheory.Limits.WalkingPair.left = true
-- Mathlib.Data.Nat.Log
Nat.log_of_left_le_one : ∀ {b : ℕ}, b ≤ 1 → ∀ (n : ℕ), Nat.log b n = 0
-- Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace
ChartedSpace.locallyRingedSpace_id : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {EM : Type u_1} [inst_1 : NormedAddCommGroup EM]
  [inst_2 : NormedSpace 𝕜 EM] {HM : Type u_2} [inst_3 : TopologicalSpace HM] (IM : ModelWithCorners 𝕜 EM HM)
  (M : Type u) [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace HM M],
  ChartedSpace.locallyRingedSpaceMap id ⋯ = CategoryTheory.CategoryStruct.id (ChartedSpace.locallyRingedSpace IM M)
-- Mathlib.RingTheory.Idempotents
OrthogonalIdempotents.lift_of_isNilpotent_ker_aux : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] (f : R →+* S),
  (∀ x ∈ RingHom.ker f, IsNilpotent x) →
    ∀ {n : ℕ} {e : Fin n → S},
      OrthogonalIdempotents e → (∀ (i : Fin n), e i ∈ f.range) → ∃ e', OrthogonalIdempotents e' ∧ ⇑f ∘ e' = e
-- Init.Data.Float.Float
/-- Computes the absolute value of a floating-point number.

This function has a logical model in terms of `Float.Model`. It is implemented in compiled code by the
C function `fabs`.
 -/
Float.abs : Float → Float
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.restrict_closure_eq : ∀ {α : Type u_2} {X R : Set α} (M : Matroid α),
  X ⊆ R → autoParam (R ⊆ M.E) Matroid.restrict_closure_eq._auto_1 → (M.restrict R).closure X = M.closure X ∩ R
-- Std.Time.Date.PlainDate
/-- Creates a new `PlainDate` by adjusting the day of the month to the given `days` value, with any
out-of-range days rolled over to the next month or year as needed.
 -/
Std.Time.PlainDate.withDaysRollOver : Std.Time.PlainDate → Std.Time.Day.Ordinal → Std.Time.PlainDate
-- Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
HomotopicalAlgebra.mem_trivialCofibrations : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y)
  [inst_1 : HomotopicalAlgebra.CategoryWithCofibrations C] [inst_2 : HomotopicalAlgebra.CategoryWithWeakEquivalences C]
  [HomotopicalAlgebra.Cofibration f] [HomotopicalAlgebra.WeakEquivalence f], HomotopicalAlgebra.trivialCofibrations C f
-- Mathlib.CategoryTheory.Abelian.Basic
/-- A preadditive category with kernels, cokernels, and finite products,
in which the coimage-image comparison morphism is always an isomorphism,
is an abelian category.  -/
CategoryTheory.Abelian.ofCoimageImageComparisonIsIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasKernels C] →
        [inst_3 : CategoryTheory.Limits.HasCokernels C] →
          [∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.IsIso (CategoryTheory.Abelian.coimageImageComparison f)] →
            [CategoryTheory.Limits.HasFiniteProducts C] → CategoryTheory.Abelian C
-- Mathlib.LinearAlgebra.Matrix.SemiringInverse
Matrix.IsDetpBalanced.eq_1 : ∀ {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 * Matrix.detp 1 A + b * Matrix.detp (-1) A = b * Matrix.detp 1 A + a * Matrix.detp (-1) A)
-- Mathlib.Probability.Process.HittingTime
MeasureTheory.hittingAfter.eq_1 : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : Preorder ι] [inst_1 : InfSet ι] (u : ι → Ω → β) (s : Set β)
  (n : ι) (x : Ω),
  MeasureTheory.hittingAfter u s n x = if ∃ j, n ≤ j ∧ u j x ∈ s then ↑(sInf {i | n ≤ i ∧ u i x ∈ s}) else ⊤
-- Lean.MetavarContext
Lean.MetavarContext.LevelMVarToParam.Context.mk.inj : ∀ {paramNamePrefix : Lean.Name} {alreadyUsedPred : Lean.Name → Bool} {except : Lean.LMVarId → Bool}
  {paramNamePrefix_1 : Lean.Name} {alreadyUsedPred_1 : Lean.Name → Bool} {except_1 : Lean.LMVarId → Bool},
  { paramNamePrefix := paramNamePrefix, alreadyUsedPred := alreadyUsedPred, except := except } =
      { paramNamePrefix := paramNamePrefix_1, alreadyUsedPred := alreadyUsedPred_1, except := except_1 } →
    paramNamePrefix = paramNamePrefix_1 ∧ alreadyUsedPred = alreadyUsedPred_1 ∧ except = except_1
-- Mathlib.Topology.UniformSpace.DiscreteUniformity
/-- The bot uniformity is the discrete uniformity.  -/
DiscreteUniformity.inst : ∀ (X : Type u_1), DiscreteUniformity X
-- Lean.Compiler.Old
/-- Return the name of new definitions in the a given declaration.
Here we consider only declarations we generate code for.
We use this definition to implement `add_and_compile`.  -/
Lean.Compiler.getDeclNamesForCodeGen : Lean.Declaration → Array Lean.Name
-- Mathlib.Order.Hom.Bounded
TopHom.coe_top : ∀ {α : Type u_2} {β : Type u_3} [inst : Top α] [inst_1 : LE β] [inst_2 : OrderTop β], ⇑⊤ = ⊤
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.instMonadBacktrackSavedStateTermElabM : Lean.MonadBacktrack Lean.Elab.Term.SavedState Lean.Elab.TermElabM
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.Measure.restrictₗ.eq_1 : ∀ {α : Type u_2} {m0 : MeasurableSpace α} (s : Set α),
  MeasureTheory.Measure.restrictₗ s = MeasureTheory.Measure.liftLinear (MeasureTheory.OuterMeasure.restrict s) ⋯
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.mem_support_iff : ∀ {X : AlgebraicGeometry.Scheme} {I : X.IdealSheafData} {x : ↥X},
  x ∈ I.support ↔ ∀ (U : ↑X.affineOpens), x ∈ X.zeroLocus ↑(I.ideal U)
-- Mathlib.Algebra.Group.Hom.Defs
instZeroAddMonoidHom.eq_1 : ∀ {M : Type u_4} {N : Type u_5} [inst : AddZero M] [inst_1 : AddZeroClass N],
  instZeroAddMonoidHom = { zero := { toFun := fun x => 0, map_zero' := ⋯, map_add' := ⋯ } }
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
/-- A seminorm on a ring `R` is a function `f : R → ℝ` that preserves zero, takes nonnegative
values, is subadditive and submultiplicative and such that `f (-x) = f x` for all `x ∈ R`.  -/
RingSeminorm : (R : Type u_2) → [NonUnitalNonAssocRing R] → Type u_2
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.toCompositionAsSet.eq_1 : ∀ {n : ℕ} (c : Composition n), c.toCompositionAsSet = { boundaries := c.boundaries, zero_mem := ⋯, getLast_mem := ⋯ }
-- Mathlib.Algebra.Order.Archimedean.Real.Basic
Real.exists_floor : ∀ (x : ℝ), ∃ ub, ↑ub ≤ x ∧ ∀ (z : ℤ), ↑z ≤ x → z ≤ ub
-- Mathlib.Topology.Category.TopCat.Basic
TopCat.isIso_of_bijective_of_isOpenMap : ∀ {X Y : TopCat} (f : X ⟶ Y),
  Function.Bijective ⇑(CategoryTheory.ConcreteCategory.hom f) →
    IsOpenMap ⇑(CategoryTheory.ConcreteCategory.hom f) → CategoryTheory.IsIso f
-- Mathlib.CategoryTheory.NatIso
CategoryTheory.NatIso.ofComponents_inv_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} (app : (X : C) → F.obj X ≅ G.obj X)
  (naturality :
    autoParam
      (∀ {X Y : C} (f : X ⟶ Y),
        CategoryTheory.CategoryStruct.comp (F.map f) (app Y).hom =
          CategoryTheory.CategoryStruct.comp (app X).hom (G.map f))
      CategoryTheory.NatIso.ofComponents._auto_1)
  (X : C), (CategoryTheory.NatIso.ofComponents app naturality).inv.app X = (app X).inv
-- Std.Sync.Broadcast
/-- Send a value through the broadcast channel, returning a task that will resolve once the transmission
could be completed.
 -/
Std.Broadcast.send : {α : Type} → Std.Broadcast α → α → BaseIO (Task (Except IO.Error ℕ))
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.Tactic.instIsPureOrPureOr : ∀ {φ ψ : Prop} (σs : List (Type u_1)), Std.Do.SPred.Tactic.IsPure spred(⌜φ⌝ ∨ ⌜ψ⌝) (φ ∨ ψ)
-- Mathlib.Analysis.Asymptotics.ExpGrowth
ExpGrowth.frequently_exp_le : ∀ {u : ℕ → ENNReal} {a : EReal}, a < ExpGrowth.expGrowthSup u → ∃ᶠ (n : ℕ) in Filter.atTop, (a * ↑n).exp ≤ u n
-- Batteries.Recycling.RBTree.WF
/-- The invariant of the `del` function.
* If the input tree is black, then the result of deletion is a red-red tree with
  black-height lowered by 1.
* If the input tree is red or nil, then the result of deletion is a balanced tree with
  some color and the same black-height.
 -/
RBTree.RBNode.DelProp : {α : Type u_1} → RBTree.RBColor → RBTree.RBNode α → ℕ → Prop
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_iSup : ∀ {X : AlgebraicGeometry.Scheme} {ι : Sort u_1} (Z : ι → TopologicalSpace.Closeds ↥X),
  AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (iSup Z) =
    ⨅ i, AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (Z i)
-- Mathlib.CategoryTheory.Shift.Basic
CategoryTheory.shiftFunctorCompIsoId_naturality_1_assoc : ∀ {C : Type u} {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddGroup A]
  [inst_2 : CategoryTheory.HasShift C A] {X Y : C} (f : X ⟶ Y) (i j : A) (hij : i + j = 0) {Z : C} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorCompIsoId C i j hij).inv.app X)
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.shiftFunctor C j).map ((CategoryTheory.shiftFunctor C i).map f))
        (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorCompIsoId C i j hij).hom.app Y) h)) =
    CategoryTheory.CategoryStruct.comp f h
-- Mathlib.Algebra.Category.ModuleCat.Ulift
/-- Universe lift functor for `R`-module.  -/
ModuleCat.uliftFunctor : (R : Type u) → [inst : Ring R] → CategoryTheory.Functor (ModuleCat R) (ModuleCat R)
-- Mathlib.NumberTheory.Real.Irrational
irrational_sub_intCast_iff : ∀ {m : ℤ} {x : ℝ}, Irrational (x - ↑m) ↔ Irrational x
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem_union_of_not_mem_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [inst_2 : EquivBEq α]
  [inst_3 : LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} (not_mem : k ∉ m₁) {h' : k ∈ m₁ ∪ m₂},
  (m₁ ∪ m₂)[k] = m₂[k]
-- Mathlib.Algebra.Group.UniqueProds.Basic
TwoUniqueProds.of_mulHom : ∀ {G : Type u} {H : Type v} [inst : Mul G] [inst_1 : Mul H] (f : H →ₙ* G),
  (∀ ⦃a b c d : H⦄, a * b = c * d → f a = f c ∧ f b = f d → a = c ∧ b = d) → ∀ [TwoUniqueProds G], TwoUniqueProds H
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientAddGroup.liftEquiv.eq_1 : ∀ {G : Type u_1} {H : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup H] (N : AddSubgroup G) [nN : N.Normal]
  {φ : G →+ H} (hφ : Function.Surjective ⇑φ) (HN : N = φ.ker),
  QuotientAddGroup.liftEquiv N hφ HN = AddEquiv.ofBijective (QuotientAddGroup.lift N φ ⋯) ⋯
-- Mathlib.Algebra.Category.ModuleCat.Pseudofunctor
/-- The pseudofunctor from `LocallyDiscrete RingCatᵒᵖ` to `Cat` which sends a ring `R`
to its category of modules. The functoriality is given by the restriction of scalars.  -/
RingCat.moduleCatRestrictScalarsPseudofunctor : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete RingCatᵒᵖ) CategoryTheory.Cat
-- Mathlib.Topology.UniformSpace.Basic
uniformity_prod_eq_comap_prod : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] [inst_1 : UniformSpace β],
  uniformity (α × β) = Filter.comap (fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) (uniformity α ×ˢ uniformity β)
-- Init.Data.List.Perm
List.perm_cons : ∀ {α : Type u_1} (a : α) {l₁ l₂ : List α}, (a :: l₁).Perm (a :: l₂) ↔ l₁.Perm l₂
-- Mathlib.CategoryTheory.Shift.CommShiftTwo
CategoryTheory.CommShift₂Setup.toTwistShiftData : {D : Type u_5} →
  [inst : CategoryTheory.Category.{v_5, u_5} D] →
    {M : Type u_6} →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : CategoryTheory.HasShift D M] →
          CategoryTheory.CommShift₂Setup D M →
            CategoryTheory.TwistShiftData (CategoryTheory.PullbackShift D (AddMonoidHom.fst M M + AddMonoidHom.snd M M))
              (M × M)
-- Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Asymptotics.IsLittleO.add_isEquivalent : ∀ {α : Type u_1} {β : Type u_2} [inst : NormedAddCommGroup β] {u v w : α → β} {l : Filter α},
  u =o[l] w → Asymptotics.IsEquivalent l v w → Asymptotics.IsEquivalent l (u + v) w
-- Init.Omega.IntList
Lean.Omega.IntList.dot_cons₂ : ∀ {x : ℤ} {xs : List ℤ} {y : ℤ} {ys : List ℤ},
  Lean.Omega.IntList.dot (x :: xs) (y :: ys) = x * y + Lean.Omega.IntList.dot xs ys
-- Init.Data.UInt.Lemmas
UInt64.toNat_toUSize : ∀ (x : UInt64), x.toUSize.toNat = x.toNat % 2 ^ System.Platform.numBits
-- Mathlib.Algebra.Homology.Homotopy
/-- Compatibility of `nullHomotopicMap` with the postcomposition by a morphism
of complexes.  -/
Homotopy.nullHomotopicMap_comp : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D E : HomologicalComplex V c} (hom : (i j : ι) → C.X i ⟶ D.X j) (g : D ⟶ E),
  CategoryTheory.CategoryStruct.comp (Homotopy.nullHomotopicMap hom) g =
    Homotopy.nullHomotopicMap fun i j => CategoryTheory.CategoryStruct.comp (hom i j) (g.f j)
-- Std.Data.HashSet.Lemmas
Std.HashSet.contains_of_isEmpty : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {a : α},
  m.isEmpty = true → m.contains a = false
-- Mathlib.Data.ENNReal.Action
/-- A `DistribMulAction` over `ℝ≥0∞` restricts to a `DistribMulAction` over `ℝ≥0`.  -/
ENNReal.instDistribMulActionNNReal : {M : Type u_1} → [inst : AddMonoid M] → [DistribMulAction ENNReal M] → DistribMulAction NNReal M
-- Mathlib.Data.Finset.Disjoint
Finset.not_disjoint_iff : ∀ {α : Type u_2} {s t : Finset α}, ¬Disjoint s t ↔ ∃ a ∈ s, a ∈ t
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
CategoryTheory.Limits.PushoutCocone.flip_pt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z}
  (t : CategoryTheory.Limits.PushoutCocone f g), t.flip.pt = t.pt
-- Batteries.Data.Float.Basic
/-- Calculates the number of trailing bits in a `UInt32`. Requires `v ≠ 0`.  -/
Float32.toRatParts'.trailingZeros : UInt32 → UInt8 → UInt8
-- Mathlib.Order.Partition.Finpartition
/-- The partition is supremum-independent  -/
Finpartition.supIndep : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : OrderBot α] {a : α} (self : Finpartition a), self.parts.SupIndep id
-- Init.Data.UInt.Lemmas
UInt8.ofNatLT_uInt64ToNat : ∀ (n : UInt64) (h : n.toNat < UInt8.size), UInt8.ofNatLT n.toNat h = n.toUInt8
-- Std.Data.Iterators.Producers.Range
/-- Returns an iterator over the given range. This iterator will emit the elements of the range
in increasing order.
 -/
Std.Rcc.iter : {α : Type u_1} → Std.Rcc α → Std.Iter α
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.swap.match_1.eq_3 : ∀ {α : Type u_1} (motive : List α → ℕ → ℕ → Sort u_2) (a : α) (xs : List α) (i : ℕ)
  (h_1 : (x x_1 : ℕ) → motive [] x x_1) (h_2 : (a : α) → (xs : List α) → motive (a :: xs) 0 0)
  (h_3 : (a : α) → (xs : List α) → (i : ℕ) → motive (a :: xs) 0 i.succ)
  (h_4 : (a : α) → (xs : List α) → (i : ℕ) → motive (a :: xs) i.succ 0)
  (h_5 : (a : α) → (xs : List α) → (i j : ℕ) → motive (a :: xs) i.succ j.succ),
  (match a :: xs, 0, i.succ with
    | [], x, x_1 => h_1 x x_1
    | a :: xs, 0, 0 => h_2 a xs
    | a :: xs, 0, i.succ => h_3 a xs i
    | a :: xs, i.succ, 0 => h_4 a xs i
    | a :: xs, i.succ, j.succ => h_5 a xs i j) =
    h_3 a xs i
-- Mathlib.Data.ENNReal.BigOperators
/-- **Alias** of `ENNReal.ofNNReal_finsetProd`. -/
ENNReal.coe_finsetProd : ∀ {ι : Type u_1} (s : Finset ι) (f : ι → NNReal), ↑(∏ i ∈ s, f i) = ∏ i ∈ s, ↑(f i)
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_add_of_nonneg : ∀ {x y z : ℝ}, 0 ≤ x → 0 ≤ y → 0 ≤ z → x ^ (y + z) = x ^ y * x ^ z