mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey_insertListIfNewUnit_of_contains : ∀ {α : Type u} [inst : BEq α] [EquivBEq α] {l : List ((_ : α) × Unit)} {toInsert : List α} {k : α}
  (contains : Std.Internal.List.containsKey k l = true)
  {h : Std.Internal.List.containsKey k (Std.Internal.List.insertListIfNewUnit l toInsert) = true},
  Std.Internal.List.getKey k (Std.Internal.List.insertListIfNewUnit l toInsert) h =
    Std.Internal.List.getKey k l contains
-- Init.Prelude
/-- Gets the kind of a `Syntax.node` value, or the pseudo-kind of any other `Syntax` value.

“Pseudo-kinds” are kinds that are assigned by convention to non-`Syntax.node` values:
`identKind` for `Syntax.ident`, `` `missing `` for `Syntax.missing`, and the atom's string literal
for atoms.
 -/
Lean.Syntax.getKind : Lean.Syntax → Lean.SyntaxNodeKind
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
MeasureTheory.instSigmaFiniteRestrictUnionSet : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α}
  [MeasureTheory.SigmaFinite (μ.restrict s)] [MeasureTheory.SigmaFinite (μ.restrict t)],
  MeasureTheory.SigmaFinite (μ.restrict (s ∪ t))
-- Mathlib.ModelTheory.Algebra.Field.Basic
_private.Mathlib.ModelTheory.Algebra.Field.Basic.0.FirstOrder.Field.FieldAxiom.toSentence.match_1.eq_6 : ∀ (motive : FirstOrder.Field.FieldAxiom → Sort u_1) (h_1 : Unit → motive FirstOrder.Field.FieldAxiom.addAssoc)
  (h_2 : Unit → motive FirstOrder.Field.FieldAxiom.zeroAdd)
  (h_3 : Unit → motive FirstOrder.Field.FieldAxiom.negAddCancel)
  (h_4 : Unit → motive FirstOrder.Field.FieldAxiom.mulAssoc) (h_5 : Unit → motive FirstOrder.Field.FieldAxiom.mulComm)
  (h_6 : Unit → motive FirstOrder.Field.FieldAxiom.oneMul) (h_7 : Unit → motive FirstOrder.Field.FieldAxiom.existsInv)
  (h_8 : Unit → motive FirstOrder.Field.FieldAxiom.leftDistrib)
  (h_9 : Unit → motive FirstOrder.Field.FieldAxiom.existsPairNE),
  (match FirstOrder.Field.FieldAxiom.oneMul with
    | FirstOrder.Field.FieldAxiom.addAssoc => h_1 ()
    | FirstOrder.Field.FieldAxiom.zeroAdd => h_2 ()
    | FirstOrder.Field.FieldAxiom.negAddCancel => h_3 ()
    | FirstOrder.Field.FieldAxiom.mulAssoc => h_4 ()
    | FirstOrder.Field.FieldAxiom.mulComm => h_5 ()
    | FirstOrder.Field.FieldAxiom.oneMul => h_6 ()
    | FirstOrder.Field.FieldAxiom.existsInv => h_7 ()
    | FirstOrder.Field.FieldAxiom.leftDistrib => h_8 ()
    | FirstOrder.Field.FieldAxiom.existsPairNE => h_9 ()) =
    h_6 ()
-- Mathlib.CategoryTheory.Monoidal.Preadditive
CategoryTheory.instPreservesFiniteBiproductsTensorRight : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalPreadditive C] (X : C),
  CategoryTheory.Limits.PreservesFiniteBiproducts (CategoryTheory.MonoidalCategory.tensorRight X)
-- Lean.Meta.Offset
/-- Evaluate simple `Nat` expressions.
Remark: this method assumes the given expression has type `Nat`.  -/
Lean.Meta.evalNat : Lean.Expr → OptionT Lean.MetaM ℕ
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.pushforwardId_inv_app_app : ∀ {X : AlgebraicGeometry.Scheme} {M : X.Modules} {U : X.Opens},
  AlgebraicGeometry.Scheme.Modules.Hom.app ((AlgebraicGeometry.Scheme.Modules.pushforwardId X).inv.app M) U =
    CategoryTheory.CategoryStruct.id (((CategoryTheory.Functor.id X.Modules).obj M).presheaf.obj (Opposite.op U))
-- Mathlib.RingTheory.MvPowerSeries.Expand
MvPowerSeries.expand_substAlgHom : ∀ {σ : Type u_1} {τ : Type u_2} {S : Type u_4} [inst : CommRing S] (p : ℕ) (hp : p ≠ 0) {f : σ → MvPowerSeries τ S}
  (hf : MvPowerSeries.HasSubst f) {φ : MvPowerSeries σ S},
  (MvPowerSeries.expand p hp) ((MvPowerSeries.substAlgHom hf) φ) = (MvPowerSeries.substAlgHom ⋯) φ
-- Batteries.Data.List.Lemmas
List.getElem_idxOf_eq_idxOfNth : ∀ {α : Type u_1} {n : ℕ} {x : α} {xs : List α} [inst : BEq α] {h : n < (List.idxsOf x xs).length},
  (List.idxsOf x xs)[n] = List.idxOfNth x xs n
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
/-- If `M` is a monoid object, then `Hom(-, M)` is a presheaf of monoids.  -/
CategoryTheory.yonedaMonObj : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v, u_1} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      (M : C) → [CategoryTheory.MonObj M] → CategoryTheory.Functor Cᵒᵖ MonCat
-- Mathlib.Topology.Maps.Basic
IsClosedMap.isClosed_range : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  IsClosedMap f → IsClosed (Set.range f)
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
MDifferentiableWithinAt.fst : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {F : Type u_11}
  [inst_11 : NormedAddCommGroup F] [inst_12 : NormedSpace 𝕜 F] {G : Type u_12} [inst_13 : TopologicalSpace G]
  {J : ModelWithCorners 𝕜 F G} {N : Type u_13} [inst_14 : TopologicalSpace N] [inst_15 : ChartedSpace G N]
  {f : N → M × M'} {s : Set N} {x : N}, MDiffAt[s] f x → (MDiffAt[s] fun x => (f x).1) x
-- Mathlib.Topology.Algebra.InfiniteSum.Constructions
summable_op : ∀ {α : Type u_1} {β : Type u_2} {L : SummationFilter β} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α]
  {f : β → α}, Summable (fun a => MulOpposite.op (f a)) L ↔ Summable f L
-- Mathlib.CategoryTheory.FintypeCat
FintypeCat.uSwitchEquiv_symm_naturality : ∀ {X Y : FintypeCat} (f : X ⟶ Y) (x : X.obj),
  (CategoryTheory.ConcreteCategory.hom (FintypeCat.uSwitch.map f)) (X.uSwitchEquiv.symm x) =
    Y.uSwitchEquiv.symm ((CategoryTheory.ConcreteCategory.hom f) x)
-- Init.Data.BitVec.Bootstrap
BitVec.getLsbD_ofFin : ∀ {n : ℕ} (x : Fin (2 ^ n)) (i : ℕ), { toFin := x }.getLsbD i = (↑x).testBit i
-- Std.Sat.AIG.LawfulOperator
/-- `decls1` is a prefix of `decls2`
 -/
Std.Sat.AIG.IsPrefix : {α : Type} → Array (Std.Sat.AIG.Decl α) → Array (Std.Sat.AIG.Decl α) → Prop
-- Mathlib.RingTheory.Localization.InvSubmonoid
IsLocalization.mul_toInvSubmonoid : ∀ {R : Type u_1} [inst : CommRing R] (M : Submonoid R) (S : Type u_2) [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : IsLocalization M S] (m : ↥M), (algebraMap R S) ↑m * ↑((IsLocalization.toInvSubmonoid M S) m) = 1
-- Mathlib.Analysis.Normed.Operator.Fredholm.Basic
FredholmDecomposition.mk.sizeOf_spec : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [inst_4 : SizeOf 𝕜] [inst_5 : SizeOf E] (X₀ X₁ : Submodule 𝕜 E)
  (isTopCompl : Submodule.IsTopCompl X₁ X₀) (finite_X₀ : FiniteDimensional 𝕜 ↥X₀),
  sizeOf { X₀ := X₀, X₁ := X₁, isTopCompl := isTopCompl, finite_X₀ := finite_X₀ } =
    1 + sizeOf X₀ + sizeOf X₁ + sizeOf isTopCompl + sizeOf finite_X₀
-- Init.Data.Iterators.Combinators.Monadic.Append
Std.Iterators.Types.Append.PlausibleStep.fstDone : ∀ {m : Type w → Type w'} {β α₁ α₂ : Type w} [inst : Std.Iterator α₁ m β] [inst_1 : Std.Iterator α₂ m β]
  {it₁ : Std.IterM m β} {it₂ : Std.IterM m β},
  it₁.IsPlausibleStep Std.IterStep.done →
    Std.Iterators.Types.Append.PlausibleStep (it₁.append it₂)
      (Std.IterStep.skip (Std.IterM.Intermediate.appendSnd α₁ it₂))
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
ContinuousMul.measurableMul₂ : ∀ {γ : Type u_3} [inst : TopologicalSpace γ] [inst_1 : MeasurableSpace γ] [BorelSpace γ] [SecondCountableTopology γ]
  [inst_4 : Mul γ] [ContinuousMul γ], MeasurableMul₂ γ
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Matrix.toLinearMapₛₗ₂'_apply : ∀ {R : Type u_1} {R₁ : Type u_2} {S₁ : Type u_3} {R₂ : Type u_4} {S₂ : Type u_5} {N₂ : Type u_10} {n : Type u_11}
  {m : Type u_12} [inst : CommSemiring R] [inst_1 : AddCommMonoid N₂] [inst_2 : Module R N₂] [inst_3 : Semiring R₁]
  [inst_4 : Semiring R₂] [inst_5 : Semiring S₁] [inst_6 : Semiring S₂] [inst_7 : Module S₁ N₂] [inst_8 : Module S₂ N₂]
  [inst_9 : SMulCommClass S₁ R N₂] [inst_10 : SMulCommClass S₂ R N₂] [inst_11 : SMulCommClass S₂ S₁ N₂] (σ₁ : R₁ →+* S₁)
  (σ₂ : R₂ →+* S₂) [inst_12 : Fintype n] [inst_13 : Fintype m] [inst_14 : DecidableEq n] [inst_15 : DecidableEq m]
  (M : Matrix n m N₂) (x : n → R₁) (y : m → R₂),
  (((Matrix.toLinearMapₛₗ₂' R σ₁ σ₂) M) x) y = ∑ i, ∑ j, σ₁ (x i) • σ₂ (y j) • M i j
-- Mathlib.LinearAlgebra.Dimension.RankNullity
LinearMap.rank_quot_submodule_map_eq : ∀ {R : Type u_1} {M : Type u} {M' : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup M']
  [inst_3 : Module R M] [inst_4 : Module R M'] [HasRankNullity.{v, u_1} R] {f : M →ₗ[R] M'} (p : Submodule R M),
  Module.rank R (M' ⧸ Submodule.map f p) =
    Module.rank R (M' ⧸ f.range) + Module.rank R (↥f.range ⧸ Submodule.map f.rangeRestrict p)
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.degree_sub_eq_left_of_degree_lt : ∀ {R : Type u} [inst : Ring R] {p q : Polynomial R}, q.degree < p.degree → (p - q).degree = p.degree
-- Mathlib.Topology.Covering.Quotient
Topology.IsQuotientMap.isQuotientCoveringMap_of_properlyDiscontinuousSMul : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X} {G : Type u_3}
  [inst_2 : Group G] [inst_3 : MulAction G E],
  Topology.IsQuotientMap f →
    ∀ [ContinuousConstSMul G E],
      (∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂) →
        ∀ [ProperlyDiscontinuousSMul G E] [LocallyCompactSpace E] [T2Space E] [IsCancelSMul G E],
          IsQuotientCoveringMap f G
-- Init.Data.List.Sublist
_private.Init.Data.List.Sublist.0.List.isSublist.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → List α → Sort u_2) (x : List α) (h_1 : (x : List α) → motive [] x)
  (h_2 : (x : List α) → motive x [])
  (h_3 :
    (l₁ : List α) →
      (hd₁ : α) → (tl₁ : List α) → l₁ = hd₁ :: tl₁ → (hd₂ : α) → (tl₂ : List α) → motive (hd₁ :: tl₁) (hd₂ :: tl₂)),
  (x = [] → False) →
    (match x, [] with
      | [], x => h_1 x
      | x, [] => h_2 x
      | l₁@h:(hd₁ :: tl₁), hd₂ :: tl₂ => h_3 l₁ hd₁ tl₁ h hd₂ tl₂) =
      h_2 x
-- Init.Data.Option.Lemmas
Option.left_le_max : ∀ {α : Type u_1} [inst : LE α] [inst_1 : Max α],
  (∀ (x : α), x ≤ x) → (∀ (x y : α), x ≤ x ⊔ y) → ∀ {a b : Option α}, a ≤ a ⊔ b
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.eval₂_eq_eval_map : ∀ {R : Type u} {S : Type v} [inst : Semiring R] {p : Polynomial R} [inst_1 : Semiring S] (f : R →+* S) {x : S},
  Polynomial.eval₂ f x p = Polynomial.eval x (Polynomial.map f p)
-- Mathlib.Data.List.Induction
List.reverseRec.hcongr_5 : ∀ (α α' : Type u_1),
  α = α' →
    ∀ (motive : List α → Sort u_2) (motive' : List α' → Sort u_2),
      motive ≍ motive' →
        ∀ (nil : motive []) (nil' : motive' []),
          nil ≍ nil' →
            ∀ (append_singleton : (l : List α) → (a : α) → motive l → motive (l ++ [a]))
              (append_singleton' : (l : List α') → (a : α') → motive' l → motive' (l ++ [a])),
              append_singleton ≍ append_singleton' →
                ∀ (l : List α) (l' : List α'),
                  l ≍ l' → List.reverseRec nil append_singleton l ≍ List.reverseRec nil' append_singleton' l'
-- Mathlib.Algebra.Star.Basic
MulOpposite.unop_star : ∀ {R : Type u} [inst : Star R] (r : Rᵐᵒᵖ), MulOpposite.unop (star r) = star (MulOpposite.unop r)
-- Mathlib.Topology.Algebra.Module.Alternating.Topology
ContinuousAlternatingMap.instContinuousEvalConst : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : TopologicalSpace E] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] [inst_7 : IsTopologicalAddGroup F] [ContinuousSMul 𝕜 E],
  ContinuousEvalConst (E [⋀^ι]→L[𝕜] F) (ι → E) F
-- Mathlib.Probability.ProbabilityMassFunction.Basic
PMF.toMeasure_toPMF : ∀ {α : Type u_1} [inst : Countable α] [inst_1 : MeasurableSpace α] [inst_2 : MeasurableSingletonClass α] (p : PMF α),
  p.toMeasure.toPMF = p
-- Mathlib.Topology.Inseparable
SeparationQuotient.map_mk_nhdsSet : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X},
  Filter.map SeparationQuotient.mk (nhdsSet s) = nhdsSet (SeparationQuotient.mk '' s)
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
CategoryTheory.Abelian.Ext.mk₀_neg : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X Y : C} (f : X ⟶ Y),
  CategoryTheory.Abelian.Ext.mk₀ (-f) = -CategoryTheory.Abelian.Ext.mk₀ f
-- Mathlib.RingTheory.Flat.Equalizer
_private.Mathlib.RingTheory.Flat.Equalizer.0.AlgHom.coe_tensorEqualizerAux : ∀ {R : Type u_1} (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (T : Type u_3)
  [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [inst_6 : IsScalarTower R S T] {A : Type u_4}
  {B : Type u_5} [inst_7 : CommRing A] [inst_8 : CommRing B] [inst_9 : Algebra R A] [inst_10 : Algebra R B]
  (f g : A →ₐ[R] B) (x : TensorProduct R T ↥(f.equalizer g)),
  ↑((AlgHom.tensorEqualizerAux S T f g) x) = (Algebra.TensorProduct.map (AlgHom.id S T) (f.equalizer g).val) x
-- Mathlib.Topology.Category.Profinite.Nobeling.Successor
Profinite.NobelingProof.CC'₁.eq_1 : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] [inst_1 : WellFoundedLT I] {o : Ordinal.{u}}
  (hsC : Profinite.NobelingProof.contained C (Order.succ o)) (ho : o < Ordinal.type fun x1 x2 => x1 < x2)
  (g : ↑(Profinite.NobelingProof.C' C ho)),
  Profinite.NobelingProof.CC'₁ C hsC ho g = ⟨Profinite.NobelingProof.SwapTrue o ↑g, ⋯⟩
-- Mathlib.Algebra.Ring.GeomSum
mul_geom_sum : ∀ {R : Type u_1} [inst : Ring R] (x : R) (n : ℕ), (x - 1) * ∑ i ∈ Finset.range n, x ^ i = x ^ n - 1
-- Init.Data.Array.Lemmas
Array.push_append : ∀ {α : Type u_1} {a : α} {xs ys : Array α}, (xs ++ ys).push a = xs ++ ys.push a
-- Std.Data.HashMap.Basic
Std.HashMap.instMembership : {α : Type u} → {β : Type v} → [inst : BEq α] → [inst_1 : Hashable α] → Membership α (Std.HashMap α β)
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.ψ_neg : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve R) (n : ℤ), W.ψ (-n) = -W.ψ n
-- Init.Data.Vector.Lemmas
Vector.foldl_add_const : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {a b : ℕ}, Vector.foldl (fun x x_1 => x + a) b xs = b + a * n
-- Mathlib.Algebra.Order.Pi
Function.const_nonpos_of_nonpos : ∀ {α : Type u_2} (β : Type u_3) [inst : Zero α] [inst_1 : Preorder α] {a : α}, a ≤ 0 → Function.const β a ≤ 0
-- Lean.Meta.Tactic.NormCast
Lean.Meta.NormCast.Label.squash.sizeOf_spec : sizeOf Lean.Meta.NormCast.Label.squash = 1
-- Init.Data.BitVec.Lemmas
BitVec.ofNatLT_toNat : ∀ {w : ℕ} (x : BitVec w), x.toNat#'⋯ = x
-- Mathlib.Data.List.Range
List.isChain_cons_range_succ : ∀ (r : ℕ → ℕ → Prop) (n a : ℕ), List.IsChain r (a :: List.range n.succ) ↔ r a 0 ∧ ∀ m < n, r m m.succ
-- Mathlib.CategoryTheory.Bicategory.Opposites
Bicategory.Opposite.bicategory_homCategory_comp_unop2 : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] (a b : Bᵒᵖ) {X Y Z : a ⟶ b} (η : Bicategory.Opposite.Hom2 X Y)
  (θ : Bicategory.Opposite.Hom2 Y Z),
  (CategoryTheory.CategoryStruct.comp η θ).unop2 = CategoryTheory.CategoryStruct.comp η.unop2 θ.unop2
-- Init.ShareCommon
ShareCommon.StateFactoryBuilder : Type 1
-- Mathlib.MeasureTheory.Function.Egorov
/-- Given some `ε > 0`, `iUnionNotConvergentSeq` is the union of `notConvergentSeq` with
specific indices such that `iUnionNotConvergentSeq` has measure less equal than `ε`.

This definition is useful for Egorov's theorem.  -/
MeasureTheory.Egorov.iUnionNotConvergentSeq : {α : Type u_1} →
  {β : Type u_2} →
    {ι : Type u_3} →
      {m : MeasurableSpace α} →
        [inst : PseudoEMetricSpace β] →
          {μ : MeasureTheory.Measure α} →
            {s : Set α} →
              {ε : ℝ} →
                {f : ι → α → β} →
                  {g : α → β} →
                    [inst_1 : SemilatticeSup ι] →
                      [Nonempty ι] →
                        [Countable ι] →
                          0 < ε →
                            (∀ (n : ι), Measurable fun a => edist (f n a) (g a)) →
                              MeasurableSet s →
                                μ s ≠ ⊤ →
                                  (∀ᵐ (x : α) ∂μ, x ∈ s → Filter.Tendsto (fun n => f n x) Filter.atTop (nhds (g x))) →
                                    Set α
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.pushforwardComp_hom_app_app : ∀ {X Y Z : AlgebraicGeometry.Scheme} {M : X.Modules} (f : X ⟶ Y) (g : Y ⟶ Z) (U : Z.Opens),
  AlgebraicGeometry.Scheme.Modules.Hom.app ((AlgebraicGeometry.Scheme.Modules.pushforwardComp f g).hom.app M) U =
    CategoryTheory.CategoryStruct.id
      ((((AlgebraicGeometry.Scheme.Modules.pushforward f).comp (AlgebraicGeometry.Scheme.Modules.pushforward g)).obj
              M).presheaf.obj
        (Opposite.op U))
-- Mathlib.Algebra.Group.Basic
sub_add_eq_add_sub : ∀ {α : Type u_1} [inst : SubtractionCommMonoid α] (a b c : α), a - b + c = a + c - b
-- Mathlib.RingTheory.Polynomial.Bernstein
bernsteinPolynomial.eq_zero_of_lt : ∀ (R : Type u_1) [inst : CommRing R] {n ν : ℕ}, n < ν → bernsteinPolynomial R n ν = 0
-- Mathlib.CategoryTheory.Bicategory.Yoneda
CategoryTheory.Bicategory.yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_mapId_inv_toNatTrans_app : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] (x : B) (a : Bᵒᵖ) (X : Opposite.unop a ⟶ x),
  ((CategoryTheory.Bicategory.yoneda.obj x).mapId a).inv.toNatTrans.app X = (CategoryTheory.Bicategory.leftUnitor X).inv
-- Std.Data.DHashMap.Internal.Defs
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw.WFImp.distinct : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β},
  Std.DHashMap.Internal.Raw.WFImp m → Std.Internal.List.DistinctKeys (Std.DHashMap.Internal.toListModel m.buckets)
-- Mathlib.Data.Semiquot
Semiquot.bind_def : ∀ {α β : Type u_1}, (fun x1 x2 => x1 >>= x2) = Semiquot.bind
-- Mathlib.CategoryTheory.Monoidal.Action.End
CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionOfMonoidalFunctorToEndofunctorMop_actionHom : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  (F : CategoryTheory.Functor C (CategoryTheory.Functor D D)ᴹᵒᵖ) [inst_3 : F.Monoidal] {c c' : C} {d d' : D}
  (f : c ⟶ c') (g : d ⟶ d'),
  CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHom f g =
    CategoryTheory.CategoryStruct.comp ((F.map f).unmop.app d) ((F.obj c').unmop.map g)
-- Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Ideal.height_le_ringKrullDim_quotient_add_one : ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] {r : R} {p : Ideal R} [p.IsPrime],
  r ∈ p → ↑p.height ≤ ringKrullDim (R ⧸ Ideal.span {r}) + 1
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor
/-- A strict pseudofunctor between strict bicategories induces a functor on the underlying
categories.  -/
CategoryTheory.StrictPseudofunctor.toFunctor : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        [inst_2 : CategoryTheory.Bicategory.Strict B] →
          [inst_3 : CategoryTheory.Bicategory.Strict C] →
            CategoryTheory.StrictPseudofunctor B C → CategoryTheory.Functor B C
-- Init.Data.SInt.Lemmas
Int8.toInt32_ne_neg_one : ∀ (a : Int8), a ≠ -1 → a.toInt32 ≠ -1
-- Std.Data.HashMap.IteratorLemmas
_private.Std.Data.HashMap.IteratorLemmas.0.Std.HashMap.Raw.iter.eq_1 : ∀ {α : Type u} {β : Type v} (m : Std.HashMap.Raw α β), m.iter = Std.Iter.map (fun e => (e.fst, e.snd)) m.inner.iter
-- Lean.Parser.Do
Lean.Parser.Term.elseIf : Lean.Parser.Parser
-- Lean.DocString.Types
Lean.Doc.instReprMathMode : Repr Lean.Doc.MathMode
-- Mathlib.Algebra.Order.Monoid.Unbundled.Units
Units.mul_inv_le_one : ∀ {M : Type u_1} [inst : Monoid M] [inst_1 : LE M] [MulRightMono M] {a : M} (u : Mˣ), a * ↑u⁻¹ ≤ 1 ↔ a ≤ ↑u
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
UpperHalfPlane.neg_smul : ∀ (g : GL (Fin 2) ℝ) (z : UpperHalfPlane), -g • z = g • z
-- Mathlib.Algebra.Group.Units.Basic
AddUnits.add_eq_zero_iff_eq_neg : ∀ {α : Type u} [inst : AddMonoid α] {u : AddUnits α} {a : α}, a + ↑u = 0 ↔ a = ↑(-u)
-- Std.Http.Data.Headers.Basic
Std.Http.Header.Connection.mk.sizeOf_spec : ∀ (tokens : Array String) (valid : tokens.all Std.Http.Internal.isToken = true),
  sizeOf { tokens := tokens, valid := valid } = 1 + sizeOf tokens + sizeOf valid
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
_private.Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic.0.ProfiniteAddGrp.Hom.mk.sizeOf_spec : ∀ {A B : ProfiniteAddGrp.{u}} (hom' : ↑A.toProfinite.toTop →ₜ+ ↑B.toProfinite.toTop),
  sizeOf { hom' := hom' } = 1 + sizeOf hom'
-- Mathlib.CategoryTheory.Category.ULift
CategoryTheory.ULiftHom.category : {C : Type u₁} →
  [CategoryTheory.Category.{v₁, u₁} C] → CategoryTheory.Category.{max v₂ v₁, u₁} (CategoryTheory.ULiftHom C)
-- Mathlib.Topology.VectorBundle.Basic
VectorBundleCore.coe_coordChange : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField R] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace R F] [inst_3 : TopologicalSpace B] {ι : Type u_5} (Z : VectorBundleCore R B F ι) (b : B)
  (i j : ι), Z.toFiberBundleCore.coordChange i j b = ⇑(Z.coordChange i j b)
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.IsRankLeOne.of_valuativeExtension : ∀ {A : Type u_1} (B : Type u_2) [inst : CommRing A] [inst_1 : Ring B] [inst_2 : ValuativeRel A]
  [inst_3 : ValuativeRel B] [inst_4 : Algebra A B] [ValuativeExtension A B] [ValuativeRel.IsRankLeOne B],
  ValuativeRel.IsRankLeOne A
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
RingNorm.mk.sizeOf_spec : ∀ {R : Type u_2} [inst : NonUnitalNonAssocRing R] [inst_1 : SizeOf R] (toRingSeminorm : RingSeminorm R)
  (eq_zero_of_map_eq_zero' : ∀ (x : R), toRingSeminorm.toFun x = 0 → x = 0),
  sizeOf { toRingSeminorm := toRingSeminorm, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero' } =
    1 + sizeOf toRingSeminorm
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreZeroHypercover.toPreOneHypercover_Y : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S)
  [inst_1 : E.HasPullbacks] (i j : E.I₀) (x : PUnit.{u_2 + 1}),
  E.toPreOneHypercover.Y x = CategoryTheory.Limits.pullback (E.f i) (E.f j)
-- Mathlib.Order.Monotone.Basic
/-- **Alias** of the reverse direction of `strictAntiOn_dual_iff`. -/
StrictAntiOn.dual : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
  StrictAntiOn f s → StrictAntiOn (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual) s
-- Init.Data.String.Decode
/-- Decodes and returns the `Char` whose UTF-8 encoding begins at `i` in `bytes`.

Returns `none` if `i` is not the start of a valid UTF-8 encoding of a character.
 -/
ByteArray.utf8DecodeChar? : ByteArray → ℕ → Option Char
-- Mathlib.Order.Antichain
IsStrongAntichain.swap : ∀ {α : Type u_1} {r : α → α → Prop} {s : Set α} [Std.Symm r],
  IsStrongAntichain r s → IsStrongAntichain (Function.swap r) s
-- Mathlib.Algebra.Order.Sub.Unbundled.Basic
AddLECancellable.tsub_tsub_assoc : ∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α]
  [inst_4 : Sub α] [OrderedSub α] {a b c : α}, AddLECancellable (b - c) → b ≤ a → c ≤ b → a - (b - c) = a - b + c
-- Mathlib.Algebra.Ring.Divisibility.Basic
/-- An element `a` divides the difference `b - a` if and only if `a` divides `b`.  -/
dvd_sub_self_right : ∀ {α : Type u_1} [inst : Ring α] {a b : α}, a ∣ b - a ↔ a ∣ b
-- Mathlib.CategoryTheory.Monoidal.Internal.Types.CommGrp_
/-- The category of commutative group objects in `Type u` is equivalent to the category of
commutative groups.  -/
commGrpTypeEquivalenceCommGrp : CategoryTheory.CommGrp (Type u) ≌ CommGrpCat