mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
/-- If `f : 𝕜 → 𝕜` is continuous on a compact set `s` and `f 0 = 0` and `a : X → A` tends to
`a₀ : A` along a filter `l` (such that eventually `a x` satisfies the predicate `p` associated to
`𝕜` and has quasispectrum contained in `s`, as does `a₀`), then `fun x ↦ cfcₙ f (a x)` tends to
`cfcₙ f a₀`.  -/
Filter.Tendsto.cfcₙ : ∀ {X : Type u_1} {𝕜 : Type u_2} {A : Type u_3} {p : A → Prop} [inst : RCLike 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : StarRing A] [inst_3 : NormedSpace 𝕜 A] [inst_4 : IsScalarTower 𝕜 A A] [inst_5 : SMulCommClass 𝕜 A A]
  [ContinuousStar A] [inst_7 : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p] {s : Set 𝕜},
  IsCompact s →
    ∀ (f : 𝕜 → 𝕜) {a : X → A} {a₀ : A} {l : Filter X},
      Filter.Tendsto a l (nhds a₀) →
        (∀ᶠ (x : X) in l, quasispectrum 𝕜 (a x) ⊆ s) →
          (∀ᶠ (x : X) in l, p (a x)) →
            quasispectrum 𝕜 a₀ ⊆ s →
              p a₀ →
                autoParam (ContinuousOn f s) Filter.Tendsto.cfcₙ._auto_1 →
                  autoParam (f 0 = 0) Filter.Tendsto.cfcₙ._auto_3 →
                    Filter.Tendsto (fun x => cfcₙ f (a x)) l (nhds (cfcₙ f a₀))
-- Init.Data.Format.Instances
instToFormatList : {α : Type u_1} → [Std.ToFormat α] → Std.ToFormat (List α)
-- Mathlib.Data.Seq.Computation
Computation.rmap.eq_1 : ∀ {α : Type u} {β : Type v} {γ : Type w} (f : β → γ) (a : α), Computation.rmap f (Sum.inl a) = Sum.inl a
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
HasProdUniformlyOn.tprod_eqOn : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : CommMonoid α] {f : ι → β → α} {g : β → α} {s : Set β}
  [inst_1 : UniformSpace α] [T2Space α], HasProdUniformlyOn f g s → Set.EqOn (fun x => ∏' (b : ι), f b x) g s
-- Mathlib.Combinatorics.SimpleGraph.Prod
SimpleGraph.edist_boxProd : ∀ {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {H : SimpleGraph β} (x y : α × β),
  (G □ H).edist x y = G.edist x.1 y.1 + H.edist x.2 y.2
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem!_insertIfNew : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  [inst : Inhabited β] {k a : α} {v : β}, (m.insertIfNew k v)[a]! = if (k == a) = true ∧ k ∉ m then v else m[a]!
-- Mathlib.NumberTheory.LSeries.ZMod
/-- The function `completedLFunction₀ Φ` is differentiable.  -/
ZMod.differentiable_completedLFunction₀ : ∀ {N : ℕ} [inst : NeZero N] (Φ : ZMod N → ℂ), Differentiable ℂ (ZMod.completedLFunction₀ Φ)
-- Mathlib.Algebra.Homology.HomotopyCategory.KInjective
CochainComplex.instIsKInjectiveObjIntShiftFunctor : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (L : CochainComplex C ℤ) [hL : L.IsKInjective] (n : ℤ),
  ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L).IsKInjective
-- Lean.Server.Completion.CompletionCollectors
_private.Lean.Server.Completion.CompletionCollectors.0.Lean.Server.Completion.completeNamespaces : Lean.Elab.ContextInfo → Lean.Name → Bool → Lean.Server.Completion.M✝ Unit
-- Std.Data.Iterators.Producers.Monadic.Vector
/-- Returns a finite monadic iterator for the given vector.
The iterator yields the elements of the vector in order and then terminates. There are no side
effects.

The pure version of this iterator is
`Vector.iter`.

**Termination properties:**

* `Finite` instance: always

* `Productive` instance: always
 -/
Vector.iterM : {α : Type u_1} → {n : ℕ} → Vector α n → (m : Type u_1 → Type u_2) → [Pure m] → Std.IterM m α
-- Mathlib.NumberTheory.PythagoreanTriples
PythagoreanTriple.eq : ∀ {x y z : ℤ}, PythagoreanTriple x y z → x * x + y * y = z * z
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.shortComplexH2.eq_1 : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u_1, u, u} k G),
  groupCohomology.shortComplexH2 A =
    { X₁ := ModuleCat.of k (G → ↑A), X₂ := ModuleCat.of k (G × G → ↑A), X₃ := ModuleCat.of k (G × G × G → ↑A),
      f := groupCohomology.d₁₂ A, g := groupCohomology.d₂₃ A, zero := ⋯ }
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
CategoryTheory.Bicategory.Adj.iso₂Mk.congr_simp : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : CategoryTheory.Bicategory.Adj B} {α β : a ⟶ b}
  (el el_1 : α.l ≅ β.l) (e_el : el = el_1) (er er_1 : β.r ≅ α.r) (e_er : er = er_1)
  (h : (CategoryTheory.Bicategory.conjugateEquiv β.adj α.adj) el.hom = er.hom),
  CategoryTheory.Bicategory.Adj.iso₂Mk el er h = CategoryTheory.Bicategory.Adj.iso₂Mk el_1 er_1 ⋯
-- Mathlib.Computability.PartrecBasis
Nat.Partrec'.to_part : ∀ {n : ℕ} {f : List.Vector ℕ n →. ℕ}, Nat.Partrec' f → Partrec f
-- Lean.Elab.Tactic.Grind.Basic
/-- Non-backtracking `try`/`catch`.
 -/
Lean.Elab.Tactic.Grind.tryCatch : {α : Type} →
  Lean.Elab.Tactic.Grind.GrindTacticM α →
    (Lean.Exception → Lean.Elab.Tactic.Grind.GrindTacticM α) → Lean.Elab.Tactic.Grind.GrindTacticM α
-- Mathlib.Algebra.BigOperators.Fin
/-- A sum of a function `f : Fin (n + 1) → M` over all `Fin (n + 1)` is the sum of
`f 0` plus the remaining sum  -/
Fin.sum_univ_succ : ∀ {M : Type u_2} [inst : AddCommMonoid M] {n : ℕ} (f : Fin (n + 1) → M), ∑ i, f i = f 0 + ∑ i, f i.succ
-- Lean.Data.Json.Basic
_private.Lean.Data.Json.Basic.0.Lean.JsonNumber.countDigits : ℕ → ℕ
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
AlgebraicGeometry.Scheme.PartialMap.mk.injEq : ∀ {X Y : AlgebraicGeometry.Scheme} (domain : X.Opens) (dense_domain : Dense ↑domain) (hom : ↑domain ⟶ Y)
  (domain_1 : X.Opens) (dense_domain_1 : Dense ↑domain_1) (hom_1 : ↑domain_1 ⟶ Y),
  ({ domain := domain, dense_domain := dense_domain, hom := hom } =
      { domain := domain_1, dense_domain := dense_domain_1, hom := hom_1 }) =
    (domain = domain_1 ∧ hom ≍ hom_1)
-- Mathlib.Algebra.Ring.Subring.Defs
SubringClass.mk : ∀ {S : Type u_1} {R : outParam (Type u)} [inst : NonAssocRing R] [inst_1 : SetLike S R]
  [toSubsemiringClass : SubsemiringClass S R] [toNegMemClass : NegMemClass S R], SubringClass S R
-- Lean.Compiler.IR.Basic
Lean.IR.FnBody.jmp.sizeOf_spec : ∀ (j : Lean.IR.JoinPointId) (ys : Array Lean.IR.Arg), sizeOf (Lean.IR.FnBody.jmp j ys) = 1 + sizeOf j + sizeOf ys
-- Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
/-- **Alias** of the reverse direction of `Matrix.nondegenerate_iff_det_ne_zero`. -/
Matrix.Nondegenerate.of_det_ne_zero : ∀ {n : Type u_1} [inst : Fintype n] {A : Type u_4} [inst_1 : CommRing A] [IsDomain A] {M : Matrix n n A}
  [inst_3 : DecidableEq n], M.det ≠ 0 → M.Nondegenerate
-- Init.Data.Ord.Basic
_private.Init.Data.Ord.Basic.0.List.compareLex.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → List α → Sort u_2) (x : List α) (h_1 : Unit → motive [] [])
  (h_2 : (x : List α) → motive [] x) (h_3 : (x : List α) → motive x [])
  (h_4 : (x : α) → (xs : List α) → (y : α) → (ys : List α) → motive (x :: xs) (y :: ys)),
  (x = [] → False) →
    (match [], x with
      | [], [] => h_1 ()
      | [], x => h_2 x
      | x, [] => h_3 x
      | x :: xs, y :: ys => h_4 x xs y ys) =
      h_2 x
-- Mathlib.Data.List.Forall2
List.SublistForall₂.is_refl : ∀ {α : Type u_1} {Rₐ : α → α → Prop} [Std.Refl Rₐ], Std.Refl (List.SublistForall₂ Rₐ)
-- Mathlib.AlgebraicGeometry.Sites.BigZariski
TopCat.precoverage.eq_1 : TopCat.precoverage =
  CategoryTheory.Precoverage.comap (CategoryTheory.forget TopCat) CategoryTheory.Types.jointlySurjectivePrecoverage ⊓
    TopCat.isOpenEmbedding.precoverage
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.Splits.prod : ∀ {R : Type u_1} [inst : CommSemiring R] {ι : Type u_2} {f : ι → Polynomial R} {s : Finset ι},
  (∀ i ∈ s, (f i).Splits) → (∏ i ∈ s, f i).Splits
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.contains_unitOfList : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α] {l : List α} {k : α},
  (Std.ExtDHashMap.Const.unitOfList l).contains k = l.contains k
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
WeierstrassCurve.Projective.smul_equiv_smul : ∀ {R : Type r} [inst : CommRing R] (P Q : Fin 3 → R) {u v : R}, IsUnit u → IsUnit v → (u • P ≈ v • Q ↔ P ≈ Q)
-- Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
/-- We prove that `seminormFromConst' c f x` is the limit of the sequence
`seminormFromConst_seq c f x` as `n` tends to infinity.  -/
tendsto_seminormFromConst_seq_atTop : ∀ {R : Type u_1} [inst : CommRing R] {c : R} {f : RingSeminorm R},
  f 1 ≤ 1 →
    f c ≠ 0 →
      IsPowMul ⇑f →
        ∀ (x : R), Filter.Tendsto (seminormFromConst_seq c f x) Filter.atTop (nhds (seminormFromConst' c f x))
-- Mathlib.Algebra.Torsor.Defs
smul_eq_smul_iff_inv_mul_eq_sdiv : ∀ {G : Type u_1} {P : Type u_2} [inst : Group G] [T : Torsor G P] {v₁ v₂ : G} {p₁ p₂ : P},
  v₁ • p₁ = v₂ • p₂ ↔ v₁⁻¹ * v₂ = p₁ /ₛ p₂
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.d₁₀_comp_coinvariantsMk_assoc : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) {Z : ModuleCat k}
  (h : (Rep.coinvariantsFunctor k G).obj A ⟶ Z),
  CategoryTheory.CategoryStruct.comp (groupHomology.d₁₀ A)
      (CategoryTheory.CategoryStruct.comp ((Rep.coinvariantsMk k G).app A) h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.getKeyLED_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t₁.WF →
    t₂.WF →
      t₁.Equiv t₂ →
        ∀ {k fallback : α},
          Std.DTreeMap.Internal.Impl.getKeyLED k t₁ fallback = Std.DTreeMap.Internal.Impl.getKeyLED k t₂ fallback
-- Mathlib.Tactic.Linarith.Oracle.FourierMotzkin
Mathlib.Tactic.Linarith.CompSource.scale.sizeOf_spec : ∀ (a : ℕ) (a_1 : Mathlib.Tactic.Linarith.CompSource),
  sizeOf (Mathlib.Tactic.Linarith.CompSource.scale a a_1) = 1 + sizeOf a + sizeOf a_1
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Term.restrictVarLeft.eq_2 : ∀ {L : FirstOrder.Language} {α : Type u'} {β : Type v'} [inst : DecidableEq α] {γ : Type u_2} (a : γ)
  (_f : ↥(FirstOrder.Language.var (Sum.inr a)).varFinsetLeft → β),
  (FirstOrder.Language.var (Sum.inr a)).restrictVarLeft _f = FirstOrder.Language.var (Sum.inr a)
-- Std.Data.Iterators.Lemmas.Combinators.Zip
Std.Iter.zip_eq_intermediateZip : ∀ {α₁ α₂ β₁ β₂ : Type w} [inst : Std.Iterator α₁ Id β₁] [inst_1 : Std.Iterator α₂ Id β₂] (it₁ : Std.Iter β₁)
  (it₂ : Std.Iter β₂), it₁.zip it₂ = Std.Iter.Intermediate.zip it₁ none it₂
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
Circle.bijOn_exp_Ioo_centeredArc : ∀ {r : ℝ}, r ≤ Real.pi → Set.BijOn (⇑Circle.exp) (Set.Ioo (-r) r) (Circle.centeredArc r)
-- Mathlib.Data.Finset.Max
Finset.max.eq_1 : ∀ {α : Type u_2} [inst : LinearOrder α] (s : Finset α), s.max = s.sup WithBot.some
-- Mathlib.LinearAlgebra.Span.Basic
Submodule.sup_inf_assoc_of_le_of_neg_le : ∀ {R : Type u_8} {M : Type u_9} [inst : Semiring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {s : Submodule R M}
  (t : Submodule R M) {p : Submodule R M}, s ≤ p → -s ≤ p → (s ⊔ t) ⊓ p = s ⊔ t ⊓ p
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.contains_filterMap_iff : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {γ : Type w} {t : Std.DTreeMap.Internal.Impl α fun x => β}
  [Std.TransOrd α] {f : α → β → Option γ} {k : α} (h : t.WF),
  Std.DTreeMap.Internal.Impl.contains k (Std.DTreeMap.Internal.Impl.filterMap f t ⋯).impl = true ↔
    ∃ (h' : Std.DTreeMap.Internal.Impl.contains k t = true),
      (f (t.getKey k h') (Std.DTreeMap.Internal.Impl.Const.get t k h')).isSome = true
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.skipSuffix?_congr : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.BackwardPattern pat] [String.Slice.Pattern.Model.LawfulBackwardPatternModel pat]
  {s t : String.Slice} (hst : s.copy = t.copy), s.skipSuffix? pat = Option.map (fun x => x.cast ⋯) (t.skipSuffix? pat)
-- Mathlib.Data.Set.Restrict
/-- **Alias** of `Set.domRestrict_extend_range`. -/
Set.restrict_extend_range : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β) (g : α → γ) (g' : β → γ),
  (Set.range f).domRestrict (Function.extend f g g') = fun x => g (Exists.choose ⋯)
-- Mathlib.Data.DFinsupp.Sigma
DFinsupp.sigmaUncurry_zero : ∀ {ι : Type u} {α : ι → Type u_2} {δ : (i : ι) → α i → Type v} [inst : DecidableEq ι]
  [inst_1 : (i : ι) → (j : α i) → Zero (δ i j)], DFinsupp.sigmaUncurry 0 = 0
-- Mathlib.NumberTheory.NumberField.Basic
NumberField.RingOfIntegers.instIsFractionRing : ∀ {K : Type u_1} [inst : Field K] [NumberField K], IsFractionRing (NumberField.RingOfIntegers K) K
-- Lean.Data.RArray
Lean.RArray.ofFn : {α : Type u_1} → {n : ℕ} → (Fin n → α) → 0 < n → Lean.RArray α
-- Std.Http.Data.Method
/-- Check in a checked-out version-controlled resource.
Source: https://www.rfc-editor.org/rfc/rfc3253#section-9.4
 -/
Std.Http.Method.checkin : Std.Http.Method
-- Mathlib.FieldTheory.Relrank
Subfield.relrank_dvd_rank_top_of_le : ∀ {E : Type v} [inst : Field E] {A B : Subfield E}, A ≤ B → A.relrank B ∣ Module.rank (↥A) E
-- Mathlib.RingTheory.Ideal.Norm.AbsNorm
Ideal.finite_setOfPred_absNorm_eq : ∀ {S : Type u_1} [inst : CommRing S] [inst_1 : IsDedekindDomain S] [inst_2 : Module.Free ℤ S] [Module.Finite ℤ S]
  [CharZero S] (n : ℕ), {I | Ideal.absNorm I = n}.Finite
-- Lean.Data.Lsp.Basic
Lean.Lsp.ApplyWorkspaceEditParams.mk : Option String → Lean.Lsp.WorkspaceEdit → Lean.Lsp.ApplyWorkspaceEditParams
-- Mathlib.Algebra.GroupWithZero.Associated
Associated.instRefl : ∀ {M : Type u_1} [inst : Monoid M], Std.Refl Associated
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Pretrivialization.source_eq : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  (self : Bundle.Pretrivialization F proj), self.source = proj ⁻¹' self.baseSet
-- Mathlib.GroupTheory.OrderOfElement
powCoprime_apply : ∀ {n : ℕ} {G : Type u_6} [inst : Group G] (h : (Nat.card G).Coprime n) (g : G), (powCoprime h) g = g ^ n
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousMapClass.toContinuousMapClass : ∀ {F : Type u_2} {α : outParam (Type u_3)} {β : outParam (Type u_4)} {inst : TopologicalSpace α}
  {inst_1 : PseudoMetricSpace β} {inst_2 : FunLike F α β} [self : BoundedContinuousMapClass F α β],
  ContinuousMapClass F α β
-- Mathlib.Topology.Category.Profinite.Nobeling.Basic
/-- If `l` is good w.r.t. `π C (ord I · < o₁)` and `o₁ ≤ o₂`, then it is good w.r.t.
`π C (ord I · < o₂)`
 -/
Profinite.NobelingProof.Products.isGood_mono : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] [inst_1 : WellFoundedLT I]
  {l : Profinite.NobelingProof.Products I} {o₁ o₂ : Ordinal.{u}},
  o₁ ≤ o₂ →
    Profinite.NobelingProof.Products.isGood (Profinite.NobelingProof.π C fun x => Profinite.NobelingProof.ord I x < o₁)
        l →
      Profinite.NobelingProof.Products.isGood
        (Profinite.NobelingProof.π C fun x => Profinite.NobelingProof.ord I x < o₂) l
-- Init.Control.Lawful.Instances
_private.Init.Control.Lawful.Instances.0.Option.getD.match_1.eq_1 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (x : α) (h_1 : (x : α) → motive (some x)) (h_2 : Unit → motive none),
  (match some x with
    | some x => h_1 x
    | none => h_2 ()) =
    h_1 x
-- Mathlib.Order.BooleanAlgebra.Basic
Prod.instGeneralizedBooleanAlgebra : {α : Type u} →
  {β : Type u_1} → [GeneralizedBooleanAlgebra α] → [GeneralizedBooleanAlgebra β] → GeneralizedBooleanAlgebra (α × β)
-- Mathlib.Combinatorics.Graph.Lattice
Graph.edgeSet_inf : ∀ {α : Type u_1} {β : Type u_2} (G H : Graph α β),
  (G ⊓ H).edgeSet = {e | e ∈ G.edgeSet ∩ H.edgeSet ∧ ∀ (x y : α), G.IsLink e x y ↔ H.IsLink e x y}
-- Mathlib.NumberTheory.Modular
_private.Mathlib.NumberTheory.Modular.0.ModularGroup.case_c_one_d_neg_one : ∀ {g : Matrix.SpecialLinearGroup (Fin 2) ℤ} {z : UpperHalfPlane},
  z ∈ ModularGroup.fd →
    g • z ∈ ModularGroup.fd →
      ‖UpperHalfPlane.denom (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) g))
              ↑z‖ ≤
          1 →
        ↑g 1 0 = 1 →
          ↑g 1 1 = -1 →
            (g = ModularGroup.S * ModularGroup.T⁻¹ ∨ g = ModularGroup.T⁻¹ * ModularGroup.S * ModularGroup.T⁻¹) ∧
              z = 1 +ᵥ UpperHalfPlane.ρ
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.nontrivial_iff_exists_ne_one : ∀ {M : Type u_1} [inst : MulOneClass M] (S : Submonoid M), Nontrivial ↥S ↔ ∃ x ∈ S, x ≠ 1
-- Lean.Environment
Lean.Kernel.Exception.excessiveMemory : Lean.Kernel.Exception
-- Mathlib.Topology.Algebra.FilterBasis
RingFilterBasis.toAddGroupFilterBasis : {R : Type u} → {inst : Ring R} → [self : RingFilterBasis R] → AddGroupFilterBasis R
-- Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf
PresheafOfModules.Derivation.postcomp_d_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : CategoryTheory.Functor Cᵒᵖ CommRingCat} {F : CategoryTheory.Functor C D}
  {R : CategoryTheory.Functor Dᵒᵖ CommRingCat}
  {M N : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} {φ : S ⟶ F.op.comp R}
  (d : M.Derivation φ) (f : M ⟶ N) {X : Dᵒᵖ} (x : ↑(R.obj X)),
  (d.postcomp f).d x = (ModuleCat.Hom.hom (f.app X)) (d.d x)
-- Mathlib.Order.BooleanAlgebra.Basic
sdiff_eq_symm : ∀ {α : Type u} {x y z : α} [inst : GeneralizedBooleanAlgebra α], y ≤ x → x \ y = z → x \ z = y
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.isEmpty_filter_key_eq_false_iff : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] {f : α → Bool}
  (h : t.WF),
  (Std.DTreeMap.Internal.Impl.filter (fun a x => f a) t ⋯).impl.isEmpty = false ↔
    ∃ k, ∃ (h : Std.DTreeMap.Internal.Impl.contains k t = true), f (t.getKey k h) = true
-- Lean.Elab.Binders
Lean.Elab.Term.precheckFun : Lean.Elab.Term.Quotation.Precheck
-- Mathlib.Data.Quot
Trunc.instLawfulMonad : LawfulMonad Trunc
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.Opens.ι_apply : ∀ {X : AlgebraicGeometry.Scheme} (U : X.Opens) (x : ↥U), U.ι x = ↑x
-- Mathlib.Topology.Algebra.Module.Complement
Submodule.projectionL_apply : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {p q : Submodule R M} (h : Submodule.IsTopCompl p q) (x : M),
  (p.projectionL q h) x = ↑((p.projectionOntoL q h) x)
-- Lean.Elab.ConfigEval.DeriveEvalExpr
_private.Lean.Elab.ConfigEval.DeriveEvalExpr.0.Lean.Elab.ConfigEval.ensureEvalExpr.extraDeps : Lean.Syntax → Lean.Expr → Lean.Elab.TermElabM (Array Lean.Expr)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.contains_keys : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k : α}, m.keys.contains k = m.contains k
-- Mathlib.RingTheory.Spectrum.Prime.Chevalley
/-- [Stacks Tag 00I1](https://stacks.math.columbia.edu/tag/00I1) -/
PrimeSpectrum.isOpenMap_comap_of_hasGoingDown_of_finitePresentation : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.HasGoingDown R S] [Algebra.FinitePresentation R S], IsOpenMap (PrimeSpectrum.comap (algebraMap R S))
-- Mathlib.Topology.MetricSpace.PiNat
PiNat.dist_le_one : ∀ {E : ℕ → Type u_1} (x y : (n : ℕ) → E n), dist x y ≤ 1
-- Std.Do.WP.Sound
_private.Std.Do.WP.Sound.0.Std.Do.instWPSoundOptionTExceptPUnitPureOfLawfulMonad.match_5.splitter : {α : Type u_1} →
  {P : α → Prop} →
    (motive :
        (r : Option α) →
          (match r with
            | some a => P a
            | none => True) →
            Sort u_2) →
      (r : Option α) →
        (h :
            match r with
            | some a => P a
            | none => True) →
          ((a : α) →
              (hp :
                  match some a with
                  | some a => P a
                  | none => True) →
                motive (some a) hp) →
            ((x :
                  match none with
                  | some a => P a
                  | none => True) →
                motive none x) →
              motive r h
-- Mathlib.RingTheory.MatrixAlgebra
/-- Note this can't be stated for rectangular matrices because there is no
`HMul (TensorProduct R _ _) (TensorProduct R _ _) (TensorProduct R _ _)` instance.  -/
kroneckerTMulLinearEquiv_mul : ∀ (m : Type u_2) (n : Type u_3) (R : Type u_5) (S : Type u_6) (A : Type u_7) {B : Type u_8} [inst : CommSemiring R]
  [inst_1 : Semiring S] [inst_2 : Semiring A] [inst_3 : Semiring B] [inst_4 : Algebra R S] [inst_5 : Algebra R A]
  [inst_6 : Algebra R B] [inst_7 : Fintype m] [inst_8 : Fintype n] [inst_9 : DecidableEq m] [inst_10 : DecidableEq n]
  [inst_11 : Module S A] [inst_12 : IsScalarTower R S A] (x y : TensorProduct R (Matrix m m A) (Matrix n n B)),
  (kroneckerTMulLinearEquiv m m n n R S A B) (x * y) =
    (kroneckerTMulLinearEquiv m m n n R S A B) x * (kroneckerTMulLinearEquiv m m n n R S A B) y
-- Mathlib.Analysis.Normed.Algebra.Spectrum
spectrum.subset_closedBall_norm_mul : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NormedField 𝕜] [inst_1 : NormedRing A] [inst_2 : NormedAlgebra 𝕜 A]
  [CompleteSpace A] (a : A), spectrum 𝕜 a ⊆ Metric.closedBall 0 (‖a‖ * ‖1‖)
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
AlgebraicGeometry.QuasiSeparated.mk : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y},
  autoParam (AlgebraicGeometry.QuasiCompact (CategoryTheory.Limits.pullback.diagonal f))
      AlgebraicGeometry.QuasiSeparated.quasiCompact_diagonal._autoParam →
    AlgebraicGeometry.QuasiSeparated f
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get_alter : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k k' : α} {f : Option β → Option β} {hc : k' ∈ Std.DTreeMap.Const.alter t k f},
  Std.DTreeMap.Const.get (Std.DTreeMap.Const.alter t k f) k' hc =
    if heq : cmp k k' = Ordering.eq then (f (Std.DTreeMap.Const.get? t k)).get ⋯ else Std.DTreeMap.Const.get t k' ⋯
-- Mathlib.Algebra.Polynomial.EraseLead
/-- An induction lemma for polynomials. It takes a natural number `N` as a parameter, that is
required to be at least as big as the `natDegree` of the polynomial.  This is useful to prove
results where you want to change each term in a polynomial to something else depending on the
`natDegree` of the polynomial itself and not on the specific `natDegree` of each term.  -/
Polynomial.induction_with_natDegree_le : ∀ {R : Type u_1} [inst : Semiring R] (motive : Polynomial R → Prop) (N : ℕ),
  motive 0 →
    (∀ (n : ℕ) (r : R), r ≠ 0 → n ≤ N → motive (Polynomial.C r * Polynomial.X ^ n)) →
      (∀ (f g : Polynomial R), f.natDegree < g.natDegree → g.natDegree ≤ N → motive f → motive g → motive (f + g)) →
        ∀ (f : Polynomial R), f.natDegree ≤ N → motive f
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.characteristic_iInf : ∀ {G : Type u_1} [inst : Group G] {ι : Sort u_5} {H : ι → Subgroup G} [∀ (i : ι), (H i).Characteristic],
  (⨅ i, H i).Characteristic
-- Mathlib.AlgebraicGeometry.Spec
AlgebraicGeometry.Spec.sheafedSpaceMap_hom_base : ∀ {R S : CommRingCat} (f : R ⟶ S), (AlgebraicGeometry.Spec.sheafedSpaceMap f).hom.base = AlgebraicGeometry.Spec.topMap f
-- Mathlib.Order.UpperLower.Principal
LowerSet.coe_Iio : ∀ {α : Type u_1} [inst : Preorder α] (a : α), ↑(LowerSet.Iio a) = Set.Iio a
-- Mathlib.MeasureTheory.OuterMeasure.AE
MeasureTheory.sdiff_null_ae_eq_self : ∀ {α : Type u_1} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [inst_1 : MeasureTheory.OuterMeasureClass F α]
  {μ : F} {s t : Set α}, μ t = 0 → s \ t =ᵐ[μ] s
-- Batteries.Control.LawfulMonadState
LawfulMonadStateOf.modify_comm_of_comp_comm : ∀ {σ : Type u_1} {m : Type u_1 → Type u_2} [inst : Monad m] [inst_1 : MonadStateOf σ m] [LawfulMonadStateOf σ m]
  {f g : σ → σ},
  f ∘ g = g ∘ f →
    (do
        modify f
        modify g) =
      do
      modify g
      modify f
-- Mathlib.GroupTheory.Submonoid.Inverses
Submonoid.fromCommLeftInv_apply : ∀ {M : Type u_1} [inst : CommMonoid M] (S : Submonoid M) (a : ↥S.leftInv), S.fromCommLeftInv a = S.fromLeftInv a
-- Init.Data.Vector.Lemmas
Vector.foldrM_toList : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {n : ℕ} [inst : Monad m] {f : α → β → m β} {init : β}
  {xs : Vector α n}, List.foldrM f init xs.toList = Vector.foldrM f init xs