mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
CategoryTheory.Limits.kernel_map_comp_preserves_kernel_iso_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (G : CategoryTheory.Functor C D) [inst_4 : G.PreservesZeroMorphisms] {X Y : C} (f : X ⟶ Y)
  [inst_5 : CategoryTheory.Limits.HasKernel f] [inst_6 : CategoryTheory.Limits.HasKernel (G.map f)]
  [inst_7 : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) G] {X' Y' : C} (g : X' ⟶ Y')
  [inst_8 : CategoryTheory.Limits.HasKernel g] [inst_9 : CategoryTheory.Limits.HasKernel (G.map g)]
  [inst_10 : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair g 0) G] (p : X ⟶ X') (q : Y ⟶ Y')
  (hpq : CategoryTheory.CategoryStruct.comp f q = CategoryTheory.CategoryStruct.comp p g),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯)
      (CategoryTheory.Limits.PreservesKernel.iso G g).inv =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesKernel.iso G f).inv
      (G.map (CategoryTheory.Limits.kernel.map f g p q hpq))
-- Mathlib.Topology.ContinuousMap.Compact
ContinuousMap.norm_coe_le_norm : ∀ {α : Type u_1} {E : Type u_3} [inst : TopologicalSpace α] [inst_1 : CompactSpace α]
  [inst_2 : SeminormedAddCommGroup E] (f : C(α, E)) (x : α), ‖f x‖ ≤ ‖f‖
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.comap_adj : ∀ {V : Type u} {W : Type v} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G →g G') (H : G'.Subgraph) (u v : V),
  (SimpleGraph.Subgraph.comap f H).Adj u v = (G.Adj u v ∧ H.Adj (f u) (f v))
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.toListModel_balanceL : ∀ {α : 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 l.size r.size},
  (Std.DTreeMap.Internal.Impl.balanceL k v l r hlb hrb hlr).toListModel = l.toListModel ++ ⟨k, v⟩ :: r.toListModel
-- Mathlib.Algebra.Quandle
UnitalShelf.act_idem : ∀ {S : Type u_1} [inst : UnitalShelf S] (x : S), Shelf.act x x = x
-- Init.Data.SInt.Lemmas
Int8.neg_eq_neg_one_mul : ∀ (a : Int8), -a = -1 * a
-- Mathlib.RingTheory.Smooth.Basic
Algebra.FormallySmooth.of_comp_surjective : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A],
  (∀ ⦃B : Type (max u v)⦄ [inst_3 : CommRing B] [inst_4 : Algebra R B] (I : Ideal B),
      I ^ 2 = ⊥ → Function.Surjective (Ideal.Quotient.mkₐ R I).comp) →
    Algebra.FormallySmooth R A
-- Mathlib.Order.ConditionallyCompleteLattice.Defs
conditionallyCompleteLatticeOfLatticeOfsSup.eq_1 : ∀ (α : Type u_5) [H1 : Lattice α] [inst : SupSet α]
  (isLUB_sSup : ∀ (s : Set α), BddAbove s → s.Nonempty → IsLUB s (sSup s)),
  conditionallyCompleteLatticeOfLatticeOfsSup α isLUB_sSup =
    { toLattice := H1, toSupSet := (conditionallyCompleteLatticeOfsSup α ⋯ ⋯ isLUB_sSup).toSupSet,
      toInfSet := (conditionallyCompleteLatticeOfsSup α ⋯ ⋯ isLUB_sSup).toInfSet, isLUB_csSup := ⋯, isGLB_csInf := ⋯ }
-- Mathlib.Analysis.SpecialFunctions.Gamma.Basic
_private.Mathlib.Analysis.SpecialFunctions.Gamma.Basic.0.Complex.GammaAux.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive n.succ) → motive x
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- A multifork is a cone over a multicospan.  -/
CategoryTheory.Limits.Multifork : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.Limits.MulticospanShape} →
      CategoryTheory.Limits.MulticospanIndex J C → Type (max (max (max w w') u) v)
-- Std.Tactic.BVDecide.LRAT.Internal.CompactLRATCheckerSound
_private.Std.Tactic.BVDecide.LRAT.Internal.CompactLRATCheckerSound.0.Std.Tactic.BVDecide.LRAT.Internal.compactLratChecker.go.match_1.eq_1 : ∀ {n : ℕ} (motive : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n × Bool → Sort u_1)
  (fst : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (checkSuccess : Bool)
  (h_1 :
    (fst : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) → (checkSuccess : Bool) → motive (fst, checkSuccess)),
  (match (fst, checkSuccess) with
    | (fst, checkSuccess) => h_1 fst checkSuccess) =
    h_1 fst checkSuccess
-- Init.Data.List.Lemmas
List.mem_of_mem_cons_of_mem : ∀ {α : Type u_1} {a b : α} {l : List α}, a ∈ b :: l → b ∈ l → a ∈ l
-- Lean.Expr
/-- Given `a b : Nat`, returns `a ^ b`  -/
Lean.mkNatPow : Lean.Expr → Lean.Expr → Lean.Expr
-- Lean.Meta.Sym.Arith.Types
Lean.Meta.Sym.Arith.instInhabitedRing.default : Lean.Meta.Sym.Arith.Ring
-- Std.Data.HashSet.Basic
Std.HashSet.mk.sizeOf_spec : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : SizeOf α] (inner : Std.HashMap α Unit),
  sizeOf { inner := inner } = 1 + sizeOf inner
-- Std.Data.ExtHashMap.Basic
/-- Inserts multiple keys with the value `()` into the hash map by iterating over the given collection
and calling `insertIfNew`. If the same key appears multiple times, the first occurrence takes
precedence.

This is mainly useful to implement `HashSet.insertMany`, so if you are considering using this,
`HashSet` or `HashSet.Raw` might be a better fit for you.
 -/
Std.ExtHashMap.insertManyIfNewUnit : {α : Type u} →
  {x : BEq α} →
    {x_1 : Hashable α} →
      [EquivBEq α] →
        [LawfulHashable α] → {ρ : Type w} → [ForIn Id ρ α] → Std.ExtHashMap α Unit → ρ → Std.ExtHashMap α Unit
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
/-- If `C` has coproducts indexed by `X`, then `Cᵒᵖ` has products indexed by `X`.
 -/
CategoryTheory.Limits.hasProductsOfShape_opposite : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (X : Type v₂)
  [CategoryTheory.Limits.HasCoproductsOfShape X C], CategoryTheory.Limits.HasProductsOfShape X Cᵒᵖ
-- Mathlib.Topology.FiberBundle.Constructions
FiberBundle.prod_trivializationAtlas' : ∀ {B : Type u_1} [inst : TopologicalSpace B] (F₁ : Type u_2) [inst_1 : TopologicalSpace F₁] (E₁ : B → Type u_3)
  [inst_2 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] (F₂ : Type u_4) [inst_3 : TopologicalSpace F₂]
  (E₂ : B → Type u_5) [inst_4 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [inst_5 : (x : B) → Zero (E₁ x)]
  [inst_6 : (x : B) → Zero (E₂ x)] [inst_7 : (x : B) → TopologicalSpace (E₁ x)]
  [inst_8 : (x : B) → TopologicalSpace (E₂ x)] [inst_9 : FiberBundle F₁ E₁] [inst_10 : FiberBundle F₂ E₂],
  FiberBundle.trivializationAtlas' =
    {e | ∃ e₁ e₂, ∃ (_ : MemTrivializationAtlas e₁) (_ : MemTrivializationAtlas e₂), e = e₁.prod e₂}
-- Mathlib.Algebra.Algebra.Equiv
RingEquiv.equivIntAlgEquiv_apply : ∀ (R : Type u_1) (S : Type u_2) [inst : Ring R] [inst_1 : Ring S] (f : R ≃+* S),
  (RingEquiv.equivIntAlgEquiv R S) f = f.toIntAlgEquiv
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.image_op_add : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Add α] (s t : Finset α),
  Finset.image AddOpposite.op (s + t) = Finset.image AddOpposite.op t + Finset.image AddOpposite.op s
-- Lean.Elab.Term.TermElabM
/-- Helper function for "embedding" an `Expr` in `Syntax`.
It creates a named hole `?m` and immediately assigns `e` to it.
Examples:
```lean
let e := mkConst ``Nat.zero
`(Nat.succ $(← exprToSyntax e))
```
 -/
Lean.Elab.Term.exprToSyntax : Lean.Expr → Lean.Elab.TermElabM Lean.Term
-- Mathlib.Topology.Algebra.Group.Basic
/-- Every weakly locally compact separable topological group is σ-compact.
Note: this is not true if we drop the topological group hypothesis.  -/
SeparableWeaklyLocallyCompactGroup.sigmaCompactSpace : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G] [TopologicalSpace.SeparableSpace G]
  [WeaklyLocallyCompactSpace G], SigmaCompactSpace G
-- Mathlib.CategoryTheory.SmallObject.Construction
CategoryTheory.SmallObject.ρFunctorObj_π_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C}
  (πX : X ⟶ S)
  [inst_1 :
    CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX))
      C]
  [inst_2 :
    CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πX)
      (CategoryTheory.SmallObject.functorObjLeft f πX)]
  {Z : C} (h : S ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.ρFunctorObj f πX)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.πFunctorObj f πX) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.π'FunctorObj f πX) h
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
NonUnitalIsometricContinuousFunctionalCalculus.isGreatest_nnnorm_quasispectrum : ∀ {𝕜 : Type u_1} {A : Type u_2} {p : outParam (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]
  [NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p] (a : A),
  autoParam (p a) NonUnitalIsometricContinuousFunctionalCalculus.isGreatest_nnnorm_quasispectrum._auto_1 →
    IsGreatest ((fun x => ‖x‖₊) '' quasispectrum 𝕜 a) ‖a‖₊
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
CategoryTheory.SimplicialObject.Splitting.IndexSet.eqId_iff_len_eq : ∀ {Δ : SimplexCategoryᵒᵖ} (A : CategoryTheory.SimplicialObject.Splitting.IndexSet Δ),
  A.EqId ↔ (Opposite.unop A.fst).len = (Opposite.unop Δ).len
-- Mathlib.Algebra.Star.StarProjection
IsStarProjection.pow_succ_eq : ∀ {R : Type u_1} {p : R} [inst : Monoid R] [inst_1 : Star R], IsStarProjection p → ∀ (n : ℕ), p ^ (n + 1) = p
-- Mathlib.Analysis.Calculus.FDeriv.CompCLM
HasFDerivAt.clm_comp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {x : E} {H : Type u_5} [inst_7 : NormedAddCommGroup H]
  [inst_8 : NormedSpace 𝕜 H] {c : E → G →L[𝕜] H} {c' : E →L[𝕜] G →L[𝕜] H} {d : E → F →L[𝕜] G} {d' : E →L[𝕜] F →L[𝕜] G},
  HasFDerivAt c c' x →
    HasFDerivAt d d' x →
      HasFDerivAt (fun y => c y ∘SL d y)
        ((ContinuousLinearMap.compL 𝕜 F G H) (c x) ∘SL d' + (ContinuousLinearMap.compL 𝕜 F G H).flip (d x) ∘SL c') x
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.prodOpEquiv_inverse_map : ∀ (C : Type u₃) [inst : CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [inst_1 : CategoryTheory.Category.{v₄, u₄} D]
  {X Y : Cᵒᵖ × Dᵒᵖ} (x : X ⟶ Y),
  (CategoryTheory.prodOpEquiv C).inverse.map x =
    match x with
    | (f, g) => Opposite.op (CategoryTheory.Prod.mkHom f.unop g.unop)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.all_eq_true_iff_forall_mem_get : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α]
  {p : (a : α) → β a → Bool}, m.all p = true ↔ ∀ (a : α) (h : a ∈ m), p a (m.get a h) = true
-- Lean.Data.Format
Lean.formatKVMap : Lean.KVMap → Std.Format
-- Mathlib.CategoryTheory.Sites.Continuous
CategoryTheory.Functor.sheafPushforwardContinuousCompSheafToPresheafIso_hom_app_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) (A : Type u) [inst_2 : CategoryTheory.Category.{t, u} A]
  (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) [inst_3 : F.IsContinuous J K]
  (X : CategoryTheory.Sheaf K A) (X_1 : Cᵒᵖ),
  ((F.sheafPushforwardContinuousCompSheafToPresheafIso A J K).hom.app X).app X_1 =
    CategoryTheory.CategoryStruct.id (X.obj.obj (Opposite.op (F.obj (Opposite.unop X_1))))
-- Batteries.Data.List.Lemmas
List.countPBefore_mono : ∀ {α : Type u_1} {i j : ℕ} {p : α → Bool} {xs : List α}, i ≤ j → List.countPBefore p xs i ≤ List.countPBefore p xs j
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
/-- If ∠BCD = π, then ∠ACB + ∠ACD = π.  -/
EuclideanGeometry.angle_add_angle_eq_pi_of_angle_eq_pi : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (p₁ : P) {p₂ p₃ p₄ : P},
  EuclideanGeometry.angle p₂ p₃ p₄ = Real.pi →
    EuclideanGeometry.angle p₁ p₃ p₂ + EuclideanGeometry.angle p₁ p₃ p₄ = Real.pi
-- Mathlib.Topology.UrysohnsLemma
Urysohns.CU.left_U_subset : ∀ {X : Type u_1} [inst : TopologicalSpace X] {P : Set X → Set X → Prop} (c : Urysohns.CU P), c.left.U ⊆ c.U
-- Init.Data.Range.Polymorphic.IntLemmas
Int.map_add_toArray_roc' : ∀ {m n k : ℤ}, Array.map (fun x => k + x) (m<...=n).toArray = ((k + m)<...=k + n).toArray
-- Mathlib.Data.PNat.Defs
Nat.natPred_succPNat : ∀ (n : ℕ), n.succPNat.natPred = n
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart
cfc_comp_im : ∀ {A : Type u_1} [inst : TopologicalSpace A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : Algebra ℂ A]
  [inst_4 : StarModule ℂ A] [inst_5 : ContinuousFunctionalCalculus ℂ A IsStarNormal] [ContinuousMap.UniqueHom ℂ A]
  [T2Space A] (f : ℝ → ℝ) (a : A),
  ContinuousOn f (spectrum ℝ ↑(imaginaryPart a)) →
    autoParam (IsStarNormal a) cfc_comp_im._auto_1 → cfc (fun x => ↑(f x.im)) a = cfc f ↑(imaginaryPart a)
-- Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
CategoryTheory.Precoverage.toGrothendieck_monotone : ∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_3, u_2} C], Monotone CategoryTheory.Precoverage.toGrothendieck
-- Mathlib.RingTheory.Spectrum.Prime.Basic
PrimeSpectrum.zeroLocus_singleton_zero : ∀ {R : Type u} [inst : CommSemiring R], PrimeSpectrum.zeroLocus {0} = Set.univ
-- Mathlib.Data.Set.Operations
/-- `diagonal α` is the set of `α × α` consisting of all pairs of the form `(a, a)`.  -/
Set.diagonal : (α : Type u_1) → Set (α × α)
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.Prequotient.mul.injEq : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat}
  (a a_1 a_2 a_3 : RingCat.Colimits.Prequotient F), (a.mul a_1 = a_2.mul a_3) = (a = a_2 ∧ a_1 = a_3)
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.IsCircuit.isNonloop_of_mem_of_one_lt_card : ∀ {α : Type u_1} {M : Matroid α} {e : α} {C : Set α}, M.IsCircuit C → 1 < C.encard → e ∈ C → M.IsNonloop e
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueD_eq_getValue? : ∀ {α : Type u} {β : Type v} [inst : BEq α] {l : List ((_ : α) × β)} {a : α} {fallback : β},
  Std.Internal.List.getValueD a l fallback = (Std.Internal.List.getValue? a l).getD fallback
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrpObj.tensorHom_neg_neg_add : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (A : C) [inst_3 : CategoryTheory.AddGrpObj A],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddGrpObj.neg CategoryTheory.AddGrpObj.neg)
      CategoryTheory.AddMonObj.add =
    CategoryTheory.CategoryStruct.comp (β_ A A).hom
      (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add CategoryTheory.AddGrpObj.neg)
-- Mathlib.Data.Analysis.Filter
/-- The filter represented by a `CFilter` is the collection of supersets of
elements of the filter base.  -/
CFilter.toFilter : {α : Type u_1} → {σ : Type u_3} → CFilter (Set α) σ → Filter α
-- Mathlib.RingTheory.MvPowerSeries.Equiv
/-- Given a power series `p : R⟦X⟧` and an index `i`, we may view it as a
multivariate power series `toMvPowerSeries i p : MvPowerSeries σ R`.  -/
PowerSeries.toMvPowerSeries : {R : Type u_1} → {σ : Type u_2} → [inst : CommSemiring R] → σ → PowerSeries R →ₐ[R] MvPowerSeries σ R
-- Mathlib.CategoryTheory.Triangulated.TStructure.Heart
CategoryTheory.Triangulated.TStructure.Heart.faithful_ι : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} 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} {H : Type u'} {inst_6 : CategoryTheory.Category.{v', u'} H}
  {inst_7 : CategoryTheory.Preadditive H} [self : t.Heart H],
  (CategoryTheory.Triangulated.TStructure.Heart.ι t).Faithful
-- Mathlib.MeasureTheory.Order.Lattice
OrderDual.instMeasurableSup : ∀ {M : Type u_1} [inst : MeasurableSpace M] [inst_1 : Min M] [MeasurableInf M], MeasurableSup Mᵒᵈ
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous
/-- The pushforward of sheaves of modules that is induced by a continuous functor `F`
and a morphism of sheaves of rings `φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R`.  -/
SheafOfModules.pushforward : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : CategoryTheory.GrothendieckTopology C} →
          {K : CategoryTheory.GrothendieckTopology D} →
            {F : CategoryTheory.Functor C D} →
              {S : CategoryTheory.Sheaf J RingCat} →
                {R : CategoryTheory.Sheaf K RingCat} →
                  [inst_2 : F.IsContinuous J K] →
                    (S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R) →
                      CategoryTheory.Functor (SheafOfModules R) (SheafOfModules S)
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.instAdd : {k : Type u_1} →
  {V1 : Type u_2} →
    {P1 : Type u_3} →
      {V2 : Type u_4} →
        [inst : Ring k] →
          [inst_1 : AddCommGroup V1] →
            [inst_2 : Module k V1] →
              [inst_3 : AddTorsor V1 P1] → [inst_4 : AddCommGroup V2] → [inst_5 : Module k V2] → Add (P1 →ᵃ[k] V2)
-- Lean.Util.SortExprs
/-- Sorts the given expressions using `Expr.lt`, and creates a "permutation map" storing the new position of each expression.
If `lt := false`, then sorts expressions in decreasing order.
 -/
Lean.sortExprs : Array Lean.Expr → optParam Bool true → Array Lean.Expr × Lean.Perm
-- Mathlib.GroupTheory.Index
AddSubgroup.fintypeQuotientOfFiniteIndex.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} [inst_1 : H.FiniteIndex],
  AddSubgroup.fintypeQuotientOfFiniteIndex = AddSubgroup.fintypeOfIndexNeZero ⋯
-- Mathlib.Algebra.Lie.IdealOperations
LieSubmodule.lie_le_left : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (I J : LieIdeal R L),
  ⁅I, J⁆ ≤ I
-- Mathlib.NumberTheory.RamificationInertia.Galois
Ideal.instMulActionElemPrimesOver : {A : Type u_1} →
  {B : Type u_2} →
    [inst : CommRing A] →
      [inst_1 : CommRing B] →
        [inst_2 : Algebra A B] →
          {p : Ideal A} →
            {G : Type u_3} →
              [inst_3 : Group G] →
                [inst_4 : MulSemiringAction G B] → [SMulCommClass G A B] → MulAction G ↑(p.primesOver B)
-- Mathlib.Data.Semiquot
Semiquot.isPure_of_subsingleton : ∀ {α : Type u_1} [Subsingleton α] (q : Semiquot α), q.IsPure
-- Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
/-- The clifford algebra is commutative since it is isomorphic to the complex numbers.

TODO: prove this is true for all `CliffordAlgebra`s over a 1-dimensional vector space.  -/
CliffordAlgebraComplex.instCommRingCliffordAlgebraRealQ : CommRing (CliffordAlgebra CliffordAlgebraComplex.Q)
-- Mathlib.Order.Hom.CompleteLattice
/-- The type of `⨅`-preserving functions from `α` to `β`.  -/
sInfHom : (α : Type u_8) → (β : Type u_9) → [InfSet α] → [InfSet β] → Type (max u_8 u_9)
-- Std.Data.Internal.List.Associative
Std.Internal.List.maxKey!_eraseKey_eq_iff_beq_maxKey!_eq_false : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  [inst_4 : Inhabited α] {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α},
      (Std.Internal.List.eraseKey k l).isEmpty = false →
        (Std.Internal.List.maxKey! (Std.Internal.List.eraseKey k l) = Std.Internal.List.maxKey! l ↔
          (k == Std.Internal.List.maxKey! l) = false)
-- Lean.Server.FileWorker.Utils
Lean.Server.FileWorker.EditableDocument.mk.inj : ∀ {toEditableDocumentCore : Lean.Server.FileWorker.EditableDocumentCore} {reporter : Lean.Server.ServerTask Unit}
  {toEditableDocumentCore_1 : Lean.Server.FileWorker.EditableDocumentCore} {reporter_1 : Lean.Server.ServerTask Unit},
  { toEditableDocumentCore := toEditableDocumentCore, reporter := reporter } =
      { toEditableDocumentCore := toEditableDocumentCore_1, reporter := reporter_1 } →
    toEditableDocumentCore = toEditableDocumentCore_1 ∧ reporter = reporter_1
-- Mathlib.Data.Finite.Sum
Finite.psum_left : ∀ {α : Sort u_3} {β : Sort u_4} [Finite (α ⊕' β)], Finite α
-- Mathlib.Topology.MetricSpace.DilationEquiv
DilationEquiv.edist_eq' : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] (self : X ≃ᵈ Y),
  ∃ r, r ≠ 0 ∧ ∀ (x y : X), edist (self.toFun x) (self.toFun y) = ↑r * edist x y
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
writtenInExtChartAt_chartAt_symm : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  {I : ModelWithCorners 𝕜 E H} [inst_5 : ChartedSpace H M] {x : M} {y : E},
  y ∈ (extChartAt I x).target → writtenInExtChartAt I I (↑(chartAt H x) x) (↑(chartAt H x).symm) y = y
-- Mathlib.Tactic.NormNum.Basic
/-- The `norm_num` extension which identifies expressions of the form `a * b`,
such that `norm_num` successfully recognises both `a` and `b`.  -/
Mathlib.Meta.NormNum.evalMul : Mathlib.Meta.NormNum.NormNumExt
-- Mathlib.Analysis.Convex.Basic
convex_Iic : ∀ {𝕜 : Type u_1} {β : Type u_4} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid β]
  [inst_3 : PartialOrder β] [IsOrderedAddMonoid β] [inst_5 : Module 𝕜 β] [PosSMulMono 𝕜 β] (r : β), Convex 𝕜 (Set.Iic r)
-- Mathlib.Algebra.Group.Hom.Defs
OneHom.one_comp : ∀ {M : Type u_4} {N : Type u_5} {P : Type u_6} [inst : One M] [inst_1 : One N] [inst_2 : One P] (f : OneHom M N),
  OneHom.comp 1 f = 1
-- Mathlib.Data.List.Sort
_private.Mathlib.Data.List.Sort.0.List.orderedInsert.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (h_1 : Unit → motive []) (h_2 : (b : α) → (l : List α) → motive (b :: l)),
  (match [] with
    | [] => h_1 ()
    | b :: l => h_2 b l) =
    h_1 ()
-- Mathlib.Analysis.BoxIntegral.UnitPartition
/-- The tag of (the index of) a `unitPartition.box`.  -/
BoxIntegral.unitPartition.tag : {ι : Type u_1} → ℕ → (ι → ℤ) → ι → ℝ
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
/-- Slightly less general but more convenient version of `SkewMonoidAlgebra.induction_on`.  -/
SkewMonoidAlgebra.induction_on' : ∀ {k : Type u_1} {G : Type u_2} [inst : AddCommMonoid k] [instNonempty : Nonempty G] {p : SkewMonoidAlgebra k G → Prop}
  (f : SkewMonoidAlgebra k G),
  (∀ (g : G) (a : k), p (SkewMonoidAlgebra.single g a)) → (∀ (f g : SkewMonoidAlgebra k G), p f → p g → p (f + g)) → p f
-- Mathlib.Algebra.Group.Center
Set.div_mem_center : ∀ {M : Type u_1} [inst : DivisionMonoid M] {a b : M}, a ∈ Set.center M → b ∈ Set.center M → a / b ∈ Set.center M
-- Mathlib.RingTheory.Radical.Basic
UniqueFactorizationMonoid.mem_primeFactors : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [inst_1 : NormalizationMonoid M] [inst_2 : UniqueFactorizationMonoid M]
  {a b : M}, a ∈ UniqueFactorizationMonoid.primeFactors b ↔ a ∈ UniqueFactorizationMonoid.normalizedFactors b
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof.reorder.sizeOf_spec : ∀ (c : Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr),
  sizeOf (Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof.reorder c) = 1 + sizeOf c
-- Mathlib.Data.Real.ConjExponents
ENNReal.holderTriple_coe_iff : ∀ {p q r : NNReal}, r ≠ 0 → ((↑p).HolderTriple ↑q ↑r ↔ p.HolderTriple q r)