mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeGroup.IsReduced.reduce_eq : ∀ {α : Type u_1} {L : List (α × Bool)} [inst : DecidableEq α], FreeGroup.IsReduced L → FreeGroup.reduce L = L
-- Mathlib.RingTheory.DividedPowers.SubDPIdeal
/-- The divided power structure on a sub-dp-ideal.  -/
DividedPowers.IsSubDPIdeal.dividedPowers : {A : Type u_1} →
  [inst : CommSemiring A] →
    {I : Ideal A} →
      (hI : DividedPowers I) → {J : Ideal A} → hI.IsSubDPIdeal J → [(x : A) → Decidable (x ∈ J)] → DividedPowers J
-- Std.Data.HashSet.Lemmas
Std.HashSet.get!_of_isEmpty : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [inst : Inhabited α] [EquivBEq α] [LawfulHashable α]
  {a : α}, m.isEmpty = true → m.get! a = default
-- Mathlib.Algebra.Algebra.Subalgebra.Unitization
NonUnitalStarSubalgebra.unitization_injective : ∀ {R : Type u_1} {S : Type u_2} {A : Type u_3} [inst : Field R] [inst_1 : StarRing R] [inst_2 : Ring A]
  [inst_3 : StarRing A] [inst_4 : Algebra R A] [inst_5 : StarModule R A] [inst_6 : SetLike S A]
  [hSA : NonUnitalSubringClass S A] [hSRA : SMulMemClass S R A] [inst_7 : StarMemClass S A] (s : S),
  1 ∉ s → Function.Injective ⇑(NonUnitalStarSubalgebra.unitization s)
-- Mathlib.NumberTheory.DirichletCharacter.Basic
DirichletCharacter.mem_annihilator_iff_mem_closure : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] {n : ℕ} {H : Set (ZMod n)ˣ} {χ : DirichletCharacter R n},
  χ ∈ DirichletCharacter.annihilator R H ↔ ∀ x ∈ Submonoid.closure H, χ ↑x = 1
-- Mathlib.RingTheory.LocalRing.ResidueField.Ideal
Ideal.algebraMap_quotient_residueField_mk : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) [inst_1 : I.IsPrime] (x : R),
  (algebraMap (R ⧸ I) I.ResidueField) ((Ideal.Quotient.mk I) x) = (algebraMap R I.ResidueField) x
-- Mathlib.Control.Fold
Traversable.foldr_map : ∀ {α β γ : Type u} {t : Type u → Type u} [inst : Traversable t] [LawfulTraversable t] (g : β → γ) (f : γ → α → α)
  (a : α) (l : t β), Traversable.foldr f a (g <$> l) = Traversable.foldr (f ∘ g) a l
-- Mathlib.RingTheory.Ideal.Height
/-- The height of a prime ideal is defined as the supremum of the lengths of strictly decreasing
chains of prime ideals below it.  -/
_private.Mathlib.RingTheory.Ideal.Height.0.Ideal.primeHeight : {R : Type u_1} → [inst : CommRing R] → (I : Ideal R) → [hI : I.IsPrime] → ℕ∞
-- Mathlib.Data.Int.Cast.Pi
Pi.intCast_apply : ∀ {ι : Type u_1} {π : ι → Type u_2} [inst : (i : ι) → IntCast (π i)] (n : ℤ) (i : ι), ↑n i = ↑n
-- Mathlib.Topology.VectorBundle.Basic
Bundle.Pretrivialization.linearMapAt_apply : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : Semiring R] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace B] [inst_3 : AddCommMonoid F] [inst_4 : Module R F]
  [inst_5 : (x : B) → AddCommMonoid (E x)] [inst_6 : (x : B) → Module R (E x)]
  (e : Bundle.Pretrivialization F Bundle.TotalSpace.proj) [inst_7 : Bundle.Pretrivialization.IsLinear R e] {b : B}
  (y : E b), (Bundle.Pretrivialization.linearMapAt R e b) y = if b ∈ e.baseSet then (↑e ⟨b, y⟩).2 else 0
-- Mathlib.Data.Seq.Computation
_private.Mathlib.Data.Seq.Computation.0.Computation.BisimO.match_1.eq_2 : ∀ {α : Type u_1} (motive : α ⊕ Computation α → α ⊕ Computation α → Sort u_2) (s s' : Computation α)
  (h_1 : (a a' : α) → motive (Sum.inl a) (Sum.inl a')) (h_2 : (s s' : Computation α) → motive (Sum.inr s) (Sum.inr s'))
  (h_3 : (x x_1 : α ⊕ Computation α) → motive x x_1),
  (match Sum.inr s, Sum.inr s' with
    | Sum.inl a, Sum.inl a' => h_1 a a'
    | Sum.inr s, Sum.inr s' => h_2 s s'
    | x, x_1 => h_3 x x_1) =
    h_2 s s'
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.braiding_leftUnitor_aux₁ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X : C),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
          (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
          (β_ X (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv)
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X
              (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv
          (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom
            (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)))) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight
        (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom X)
      (β_ X (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.coe_subtype : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : StarRing A] [inst_4 : Algebra R A] [inst_5 : StarModule R A] (S : StarSubalgebra R A),
  ⇑S.subtype = Subtype.val
-- Mathlib.Analysis.Complex.Conformal
/-- In cases where the **Cauchy-Riemann Equation** guarantees complex differentiability at `x`, the
complex derivative equals `ContinuousLinearMap.complexOfReal` of the real derivative.
 -/
HasFDerivAt.complexOfReal_hasFDerivAt : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : ℂ → E} {x : ℂ} {f' : ℂ →L[ℝ] E},
  HasFDerivAt f f' x → ∀ (h₂ : f' Complex.I = Complex.I • f' 1), HasFDerivAt f (f'.complexOfReal h₂) x
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.balanceR_eq_balanceRErase : ∀ {α : Type u} {β : α → Type v} {k : α} {v : β k} {l r : Std.DTreeMap.Internal.Impl α β} {hlb : l.Balanced}
  {hrb : r.Balanced} {hlr : Std.DTreeMap.Internal.Impl.BalanceLPrecond r.size l.size},
  Std.DTreeMap.Internal.Impl.balanceR k v l r hlb hrb hlr = Std.DTreeMap.Internal.Impl.balanceRErase k v l r hlb hrb ⋯
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.getD_union : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k fallback : α}, (m₁ ∪ m₂).getD k fallback = m₂.getD k (m₁.getD k fallback)
-- Mathlib.Order.Interval.Set.Basic
Set.Icc_subset_Ico : ∀ {α : Type u_1} [inst : Preorder α] {a₁ a₂ b₁ b₂ : α}, b₂ ≤ b₁ → a₁ < a₂ → Set.Icc b₁ a₁ ⊆ Set.Ico b₂ a₂
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.Scheme.Hom.instFullOpensOpensFunctor : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [H : AlgebraicGeometry.IsOpenImmersion f],
  (AlgebraicGeometry.Scheme.Hom.opensFunctor f).Full
-- Mathlib.Topology.Homotopy.HomotopyGroup
GenLoop.transAt_distrib : ∀ {N : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {x : X} [inst_1 : DecidableEq N] {i j : N},
  i ≠ j →
    ∀ (a b c d : ↑(GenLoop N X x)),
      GenLoop.transAt i (GenLoop.transAt j a b) (GenLoop.transAt j c d) =
        GenLoop.transAt j (GenLoop.transAt i a c) (GenLoop.transAt i b d)
-- Mathlib.MeasureTheory.Measure.MutuallySingular
MeasureTheory.Measure.MutuallySingular.comm : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α}, μ.MutuallySingular ν ↔ ν.MutuallySingular μ
-- Batteries.Recycling.RBTree.Basic
/-- Fold a function on the values from right to left (in decreasing order).  -/
RBTree.RBNode.foldr : {α : Type u_1} → {σ : Sort u_2} → (α → σ → σ) → RBTree.RBNode α → σ → σ
-- Mathlib.Order.Hom.Basic
OrderEmbedding.subtype_apply : ∀ {α : Type u_2} [inst : Preorder α] {p : α → Prop} (x : Subtype p), (OrderEmbedding.subtype p) x = ↑x
-- Mathlib.Data.Finset.Sum
Finset.toLeft_inter : ∀ {α : Type u_1} {β : Type u_2} {u v : Finset (α ⊕ β)} [inst : DecidableEq α] [inst_1 : DecidableEq β],
  (u ∩ v).toLeft = u.toLeft ∩ v.toLeft
-- Mathlib.Algebra.FiveLemma
/-- One four lemma in terms of modules. For a diagram explaining the variables,
see the module docstring.  -/
LinearMap.surjective_of_surjective_of_surjective_of_injective : ∀ {R : Type u_1} [inst : CommRing R] {M₁ : Type u_2} {M₂ : Type u_3} {M₃ : Type u_4} {M₄ : Type u_5} {N₁ : Type u_7}
  {N₂ : Type u_8} {N₃ : Type u_9} {N₄ : Type u_10} [inst_1 : AddCommGroup M₁] [inst_2 : AddCommGroup M₂]
  [inst_3 : AddCommGroup M₃] [inst_4 : AddCommGroup M₄] [inst_5 : Module R M₁] [inst_6 : Module R M₂]
  [inst_7 : Module R M₃] [inst_8 : Module R M₄] [inst_9 : AddCommGroup N₁] [inst_10 : AddCommGroup N₂]
  [inst_11 : AddCommGroup N₃] [inst_12 : AddCommGroup N₄] [inst_13 : Module R N₁] [inst_14 : Module R N₂]
  [inst_15 : Module R N₃] [inst_16 : Module R N₄] (f₁ : M₁ →ₗ[R] M₂) (f₂ : M₂ →ₗ[R] M₃) (f₃ : M₃ →ₗ[R] M₄)
  (g₁ : N₁ →ₗ[R] N₂) (g₂ : N₂ →ₗ[R] N₃) (g₃ : N₃ →ₗ[R] N₄) (i₁ : M₁ →ₗ[R] N₁) (i₂ : M₂ →ₗ[R] N₂) (i₃ : M₃ →ₗ[R] N₃)
  (i₄ : M₄ →ₗ[R] N₄),
  g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁ →
    g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂ →
      g₃ ∘ₗ i₃ = i₄ ∘ₗ f₃ →
        Function.Exact ⇑f₂ ⇑f₃ →
          Function.Exact ⇑g₁ ⇑g₂ →
            Function.Exact ⇑g₂ ⇑g₃ →
              Function.Surjective ⇑i₁ → Function.Surjective ⇑i₃ → Function.Injective ⇑i₄ → Function.Surjective ⇑i₂
-- Mathlib.RingTheory.Support
/-- If `M` is a finite module such that `Mₚ = 0` for some `p`,
then `M[1/f] = 0` for some `p ∈ D(f)`.  -/
LocalizedModule.exists_subsingleton_away : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Module.Finite R M]
  (p : Ideal R) [inst_4 : p.IsPrime] [Subsingleton (LocalizedModule p.primeCompl M)],
  ∃ f ∉ p, Subsingleton (LocalizedModule.Away f M)
-- Mathlib.Data.Finsupp.Single
Finsupp.single_zero : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] (a : α), (fun₀ | a => 0) = 0
-- Lean.Meta.Closure
_private.Lean.Meta.Closure.0.Lean.Meta.Closure.sortDecls.visit : Std.HashMap Lean.FVarId (Lean.LocalDecl × Lean.Expr) → Lean.FVarId → StateT Lean.Meta.Closure.TopoSort✝ Lean.CoreM Unit
-- Mathlib.GroupTheory.GroupAction.Jordan
Equiv.Perm.subgroup_eq_top_of_nontrivial : ∀ {α : Type u_1} {G : Subgroup (Equiv.Perm α)} [Finite α], Nat.card α ≤ 2 → Nontrivial ↥G → G = ⊤
-- Mathlib.NumberTheory.Real.Irrational
irrational_iff_ne_rational : ∀ (x : ℝ), Irrational x ↔ ∀ (a b : ℤ), b ≠ 0 → x ≠ ↑a / ↑b
-- Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
MeasureTheory.Measure.sigmaFiniteSetWRT'.congr_simp : ∀ {α : Type u_1} {mα : MeasurableSpace α} (μ μ_1 : MeasureTheory.Measure α),
  μ = μ_1 →
    ∀ (ν ν_1 : MeasureTheory.Measure α) (e_ν : ν = ν_1) [inst : MeasureTheory.IsFiniteMeasure ν] (a a_1 : α),
      a = a_1 → μ.sigmaFiniteSetWRT' ν a = μ_1.sigmaFiniteSetWRT' ν_1 a_1
-- Mathlib.NumberTheory.ModularForms.Basic
ModularForm.constℝ_apply : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} [inst : Γ.HasDetPlusMinusOne] (x : ℝ) (τ : UpperHalfPlane),
  (ModularForm.constℝ x) τ = ↑x
-- Mathlib.LinearAlgebra.Finsupp.Defs
Finsupp.instFaithfulSMulOfNonempty : ∀ {α : Type u_1} {M : Type u_2} {R : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [Nonempty α] [FaithfulSMul R M], FaithfulSMul R (α →₀ M)
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.PrettyPrinter.Delaborator.TopDownAnalyze.withKnowing : {α : Type} →
  Bool →
    Bool →
      Lean.PrettyPrinter.Delaborator.TopDownAnalyze.AnalyzeM α →
        Lean.PrettyPrinter.Delaborator.TopDownAnalyze.AnalyzeM α
-- Mathlib.CategoryTheory.Preadditive.Mat
/-- An object in `Mat_ C` is a finite tuple of objects in `C`.
 -/
CategoryTheory.Mat_ : Type u₁ → Type (max 1 u₁)
-- Lean.DocString.Markdown
/-- The current code is inside emphasis (`*…*`).  -/
Lean.Doc.MarkdownM.InlineCtx.inEmph : Lean.Doc.MarkdownM.InlineCtx → Bool
-- Mathlib.Data.Int.SuccPred
Int.succ_eq_succ : Order.succ = Int.succ
-- Mathlib.Topology.Algebra.Module.PerfectPairing
LinearMap.toLinearMap_toContPerfPair : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : TopologicalSpace R]
  [inst_2 : AddCommGroup M] [inst_3 : Module R M] [inst_4 : TopologicalSpace M] [inst_5 : AddCommGroup N]
  [inst_6 : Module R N] [inst_7 : TopologicalSpace N] (p : M →ₗ[R] N →ₗ[R] R) [inst_8 : p.IsContPerfPair]
  [inst_9 : IsTopologicalRing R] (x : M), ↑(p.toContPerfPair x) = p x
-- Mathlib.RingTheory.WittVector.Truncated
/-- A macro tactic used to prove that `truncateFun` respects ring operations.  -/
witt_truncateFun_tac : Lean.ParserDescr
-- Mathlib.Dynamics.SymbolicDynamics.Basic
/-- Shift invariance of `carrier`.  -/
SymbolicDynamics.FullShift.MulSubshift.mapsTo : ∀ {A : Type u_1} [inst : TopologicalSpace A] {G : Type u_2} [inst_1 : Monoid G]
  (self : SymbolicDynamics.FullShift.MulSubshift A G) (g : G),
  Set.MapsTo (SymbolicDynamics.FullShift.mulShift g) self.carrier self.carrier
-- ProofWidgets.Component.RefreshComponent
ProofWidgets.RefreshComponent.AwaitRefreshParams.mk.inj : ∀ {state : Lean.Server.WithRpcRef ProofWidgets.RefreshComponent.RefreshRef} {oldIdx : ℕ}
  {state_1 : Lean.Server.WithRpcRef ProofWidgets.RefreshComponent.RefreshRef} {oldIdx_1 : ℕ},
  { state := state, oldIdx := oldIdx } = { state := state_1, oldIdx := oldIdx_1 } → state = state_1 ∧ oldIdx = oldIdx_1
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Affine.Simplex.points_mem_affineSpan_face : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_5} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] [Nontrivial k] {n : ℕ} (s : Affine.Simplex k P n) {fs : Finset (Fin (n + 1))} {m : ℕ}
  (h : fs.card = m + 1) {i : Fin (n + 1)}, s.points i ∈ affineSpan k (Set.range (s.face h).points) ↔ i ∈ fs
-- Init.Dynamic
_private.Init.Dynamic.0.TypeName.typeNameImpl : (α : Type u_1) → [TypeName α] → Lean.Name
-- Mathlib.Analysis.Convex.Strict
/-- A set in a linear ordered field is strictly convex if and only if it is convex.  -/
strictConvex_iff_convex : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [inst_3 : TopologicalSpace 𝕜]
  [OrderTopology 𝕜] {s : Set 𝕜}, StrictConvex 𝕜 s ↔ Convex 𝕜 s
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
_private.Lean.PrettyPrinter.Delaborator.TopDownAnalyze.0.Lean.PrettyPrinter.Delaborator.TopDownAnalyze.analyze.analyzeApp : Lean.PrettyPrinter.Delaborator.TopDownAnalyze.AnalyzeM Unit
-- Mathlib.Tactic.Widget.LibraryRewrite
_private.Mathlib.Tactic.Widget.LibraryRewrite.0.Mathlib.Tactic.LibraryRewrite.importedRewriteLemmasExt : Lean.EnvExtension Mathlib.Tactic.LibraryRewrite.ExtState✝
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.map_neg : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] (Q : QuadraticMap R M N) (x : M), Q (-x) = Q x
-- Mathlib.Data.Finset.Finsupp
/-- When `t` is supported on `s`, `f ∈ s.finsupp t` precisely means that `f` is pointwise in `t`.  -/
Finset.mem_finsupp_iff_of_support_subset : ∀ {ι : Type u_1} {α : Type u_2} [inst : Zero α] {s : Finset ι} {f : ι →₀ α} {t : ι →₀ Finset α},
  t.support ⊆ s → (f ∈ s.finsupp ⇑t ↔ ∀ (i : ι), f i ∈ t i)
-- Mathlib.Control.Fix
Part.fix_def' : ∀ {α : Type u_1} {β : α → Type u_2} (f : ((a : α) → Part (β a)) → (a : α) → Part (β a)) {x : α},
  (¬∃ i, (Part.Fix.approx f i x).Dom) → Part.fix f x = Part.none
-- Mathlib.Algebra.Group.ModEq
/-- `a ≡ b [PMOD p]` means that `b` is congruent to `a` modulo `p`.

If `a`, `b` are elements of an additive group,
then `a ≡ b [PMOD p]` iff `m • p = b - a` for some `m : ℤ`, see `modEq_iff_zsmul` below.
For additive commutative monoid, the definition is given by `modEq_iff_nsmul`.

Equivalently (as shown in `Algebra.Order.ToIntervalMod`), `b` does not lie in the open interval
`(a, a + p)` modulo `p`, or `toIcoMod hp a` disagrees with `toIocMod hp a` at `b`, or
`toIcoDiv hp a` disagrees with `toIocDiv hp a` at `b`.  -/
AddCommGroup.«term_≡_[PMOD_]» : Lean.TrailingParserDescr
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.coe_range : ∀ {α : Type u_1} [inst : Small.{u, u_1} α] (f : α → ZFSet.{u}), ↑(ZFSet.range f) = Set.range f
-- Batteries.Recycling.RBTree.WF
/-- The `map` function preserves the balance invariants.  -/
RBTree.RBNode.Balanced.map : ∀ {α : Type u_1} {c : RBTree.RBColor} {n : ℕ} {α_1 : Type u_2} {f : α → α_1} {t : RBTree.RBNode α},
  t.Balanced c n → (RBTree.RBNode.map f t).Balanced c n
-- Mathlib.Algebra.Group.Action.Defs
IsCancelSMul.left_cancel : ∀ {G : Type u_11} {P : Type u_12} [inst : SMul G P] [IsCancelSMul G P] (a : G) (b c : P), a • b = a • c → b = c
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward
/-- Implementation of `pushforward₀`.  -/
PresheafOfModules.pushforward₀Obj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) →
          (R : CategoryTheory.Functor Dᵒᵖ RingCat) → PresheafOfModules R → PresheafOfModules (F.op.comp R)
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.instInhabitedCommSemiring.default : Lean.Meta.Grind.Arith.CommRing.CommSemiring
-- Mathlib.Algebra.Group.Basic
mul_div_mul_right_eq_div : ∀ {G : Type u_3} [inst : Group G] (a b c : G), a * c / (b * c) = a / b
-- Mathlib.Topology.Order.Monotone
/-- An antitone function sending `bot` to `top` is continuous at the indexed supremum over
a `Sort`, then it sends this indexed supremum to the indexed supremum of the composition.  -/
Antitone.map_iSup_of_continuousAt : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  [inst_3 : CompleteLinearOrder β] [inst_4 : TopologicalSpace β] [OrderClosedTopology β] {ι : Sort u_3} {f : α → β}
  {g : ι → α}, ContinuousAt f (iSup g) → Antitone f → f ⊥ = ⊤ → f (⨆ i, g i) = ⨅ i, f (g i)
-- Init.Data.Float.Model.Float32
/-- Determine whether `a` is less than `b` according to IEEE rules.

This is not a total ordering.
 -/
Float32.Model.lt : Float32.Model → Float32.Model → Bool
-- Mathlib.Algebra.Star.LinearMap
LinearMap.intrinsicStar_comp' : ∀ {R : Type u_1} {E : Type u_2} {F : Type u_3} [inst : Semiring R] [inst_1 : InvolutiveStar R]
  [inst_2 : AddCommMonoid E] [inst_3 : Module R E] [inst_4 : StarAddMonoid E] [inst_5 : StarModule R E]
  [inst_6 : AddCommMonoid F] [inst_7 : Module R F] [inst_8 : StarAddMonoid F] [inst_9 : StarModule R F] {G : Type u_4}
  [inst_10 : AddCommMonoid G] [inst_11 : Module R G] [inst_12 : StarAddMonoid G] [inst_13 : StarModule R G]
  (f : E →ₗ[R] F) (g : G →ₗ[R] E),
  star (WithConv.toConv (f ∘ₗ g)) =
    WithConv.toConv ((star (WithConv.toConv f)).ofConv ∘ₗ (star (WithConv.toConv g)).ofConv)
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.getD_insertMany_list_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {l : List α} {k fallback : α}, k ∈ t → (t.insertMany l).getD k fallback = t.getD k fallback
-- Mathlib.LinearAlgebra.Matrix.ToLin
Matrix.toLin_pow : ∀ {R : Type u_1} [inst : CommSemiring R] {n : Type u_4} [inst_1 : Fintype n] [inst_2 : DecidableEq n] {M₁ : Type u_5}
  [inst_3 : AddCommMonoid M₁] [inst_4 : Module R M₁] (v₁ : Module.Basis n R M₁) (A : Matrix n n R) (k : ℕ),
  (Matrix.toLin v₁ v₁) (A ^ k) = (Matrix.toLin v₁ v₁) A ^ k
-- Lean.Meta.Tactic.Grind.Attr
Lean.Meta.Grind.AttrKind.symbol.sizeOf_spec : ∀ (prio : ℕ), sizeOf (Lean.Meta.Grind.AttrKind.symbol prio) = 1 + sizeOf prio
-- Mathlib.GroupTheory.SpecificGroups.Quaternion
instDecidableEqQuaternionGroup.decEq : {n : ℕ} → (x x_1 : QuaternionGroup n) → Decidable (x = x_1)
-- Mathlib.Analysis.CStarAlgebra.Projection
IsStarProjection.le_iff_mul_eq_right : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A] {p q : A},
  IsStarProjection p → IsStarProjection q → (p ≤ q ↔ q * p = p)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.mem_filter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {f : α → β → Bool}
  {k : α}, k ∈ Std.TreeMap.filter f t ↔ ∃ (h' : k ∈ t), f (t.getKey k h') t[k] = true
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.strictMonoOn_logb : ∀ {b : ℝ}, 1 < b → StrictMonoOn (Real.logb b) (Set.Ioi 0)
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
MeasureTheory.JordanDecomposition.toSignedMeasure_zero : ∀ {α : Type u_1} [inst : MeasurableSpace α], MeasureTheory.JordanDecomposition.toSignedMeasure 0 = 0
-- Mathlib.NumberTheory.FLT.Four
/-- We can assume that a minimal solution to `a ^ 4 + b ^ 4 = c ^ 2` has `a` odd.  -/
Fermat42.exists_odd_minimal : ∀ {a b c : ℤ}, Fermat42 a b c → ∃ a0 b0 c0, Fermat42.Minimal a0 b0 c0 ∧ a0 % 2 = 1
-- Mathlib.Algebra.Field.Opposite
MulOpposite.op_ratCast : ∀ {α : Type u_1} [inst : RatCast α] (q : ℚ), MulOpposite.op ↑q = ↑q
-- Mathlib.Data.Fintype.Card
Finite.to_wellFoundedLT : ∀ {α : Type u_1} [Finite α] [inst : Preorder α], WellFoundedLT α
-- Mathlib.RingTheory.DividedPowers.Padic
/-- The family `ℕ → ℚ_[p] → ℚ_[p]` given by `dpow n x = x ^ n / n!`.  -/
_private.Mathlib.RingTheory.DividedPowers.Padic.0.PadicInt.dpow' : (p : ℕ) → [hp : Fact (Nat.Prime p)] → ℕ → ℚ_[p] → ℚ_[p]
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey!_eq_default_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited α] {a : α}, m.contains a = false → m.getKey! a = default
-- Mathlib.Algebra.Module.ZLattice.Basic
Module.Basis.ofZLatticeBasis_repr_apply : ∀ (K : Type u_1) [inst : NormedField K] [inst_1 : LinearOrder K] [inst_2 : IsStrictOrderedRing K]
  [inst_3 : HasSolidNorm K] [inst_4 : FloorRing K] {E : Type u_2} [inst_5 : NormedAddCommGroup E]
  [inst_6 : NormedSpace K E] [inst_7 : FiniteDimensional K E] [inst_8 : ProperSpace E] (L : Submodule ℤ E)
  [inst_9 : DiscreteTopology ↥L] {ι : Type u_3} [hs : IsZLattice K L] (b : Module.Basis ι ℤ ↥L) (x : ↥L) (i : ι),
  ((Module.Basis.ofZLatticeBasis K L b).repr ↑x) i = ↑((b.repr x) i)
-- Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential
UniqueMDiffOn.uniqueDiffWithinAt_range_inter : ∀ {𝕜 : 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] {s : Set M} [IsManifold I 1 M],
  UniqueMDiff[s] →
    ∀ (x : M),
      ∀ y ∈ (extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s,
        UniqueDiffWithinAt 𝕜 (Set.range ↑I ∩ ↑(extChartAt I x).symm ⁻¹' s) y
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
/-- Eta-expanded form of `TendstoLocallyUniformlyOn.add` -/
TendstoLocallyUniformlyOn.fun_add : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : AddGroup α] [IsUniformAddGroup α] {ι : Type u_3} {X : Type u_4}
  [inst_3 : TopologicalSpace X] {F G : ι → X → α} {f g : X → α} {s : Set X} {l : Filter ι},
  TendstoLocallyUniformlyOn F f l s →
    TendstoLocallyUniformlyOn G g l s →
      TendstoLocallyUniformlyOn (fun i i_1 => F i i_1 + G i i_1) (fun i => f i + g i) l s
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.Measure.pi_pi : ∀ {ι : Type u_1} {α : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → MeasurableSpace (α i)]
  (μ : (i : ι) → MeasureTheory.Measure (α i)) [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)] (s : (i : ι) → Set (α i)),
  (MeasureTheory.Measure.pi μ) (Set.univ.pi s) = ∏ i, (μ i) (s i)
-- Lean.Data.Lsp.TextSync
Lean.Lsp.instToJsonDidChangeTextDocumentParams : Lean.ToJson Lean.Lsp.DidChangeTextDocumentParams
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.contains_inter!_eq_false_of_contains_eq_false_left : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  m₁.WF →
    m₂.WF →
      ∀ {k : α},
        Std.DTreeMap.Internal.Impl.contains k m₁ = false → Std.DTreeMap.Internal.Impl.contains k (m₁.inter! m₂) = false
-- Mathlib.GroupTheory.OrderOfElement
/-- If each prime factor of `orderOf x` has higher multiplicity in `orderOf y`, and `x` commutes
with `y`, then `x * y` has the same order as `y`.  -/
Commute.orderOf_mul_eq_right_of_forall_prime_mul_dvd : ∀ {G : Type u_1} [inst : Monoid G] {x y : G},
  Commute x y →
    IsOfFinOrder y → (∀ (p : ℕ), Nat.Prime p → p ∣ orderOf x → p * orderOf x ∣ orderOf y) → orderOf (x * y) = orderOf y