mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
EulerSine.integral_cos_mul_cos_pow_aux : ∀ {z : ℂ} {n : ℕ},
  2 ≤ n →
    z ≠ 0 →
      ∫ (x : ℝ) in 0..Real.pi / 2, Complex.cos (2 * z * ↑x) * ↑(Real.cos x) ^ n =
        ↑n / (2 * z) * ∫ (x : ℝ) in 0..Real.pi / 2, Complex.sin (2 * z * ↑x) * ↑(Real.sin x) * ↑(Real.cos x) ^ (n - 1)
-- Batteries.Data.String.Lemmas
Substring.Raw.bsize.eq_1 : ∀ (str : String) (b e : String.Pos.Raw), { str := str, startPos := b, stopPos := e }.bsize = e.byteIdx.sub b.byteIdx
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.span_empty : ∀ (R : Type u) (L : Type v) (M : Type w) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M], LieSubmodule.lieSpan R L ∅ = ⊥
-- Mathlib.Analysis.Real.Sqrt
Real.lt_sqrt_self_iff : ∀ {x : ℝ}, x < √x ↔ x ≠ 0 ∧ x < 1
-- Mathlib.Algebra.GroupWithZero.Subgroup
AddSubgroup.pointwise_smul_le_iff₀ : ∀ {G₀ : Type u_1} {A : Type u_4} [inst : GroupWithZero G₀] [inst_1 : AddGroup A] [inst_2 : DistribMulAction G₀ A]
  {S T : AddSubgroup A} {a : G₀}, a ≠ 0 → (a • S ≤ T ↔ S ≤ a⁻¹ • T)
-- Mathlib.CategoryTheory.Core
CategoryTheory.Core.forgetFunctorToCore_obj_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {G : Type u₂} [inst_1 : CategoryTheory.Groupoid G]
  (F : CategoryTheory.Functor G (CategoryTheory.Core C)) (X : G),
  (CategoryTheory.Core.forgetFunctorToCore.obj F).obj X = (F.obj X).of
-- Mathlib.Order.Interval.Set.Basic
Set.Icc.eq_1 : ∀ {α : Type u_1} [inst : Preorder α] (a b : α), Set.Icc a b = {x | a ≤ x ∧ x ≤ b}
-- Std.Data.ExtDTreeMap.Basic
/-- Returns the key-value pair with the `n`-th smallest key.  -/
Std.ExtDTreeMap.Const.entryAtIdx : {α : Type u} →
  {cmp : α → α → Ordering} →
    {β : Type v} → [Std.TransCmp cmp] → (t : Std.ExtDTreeMap α (fun x => β) cmp) → (n : ℕ) → n < t.size → α × β
-- Mathlib.Data.Multiset.Powerset
Multiset.revzip_powersetAux' : ∀ {α : Type u_1} {l : List α} ⦃x : Multiset α × Multiset α⦄, x ∈ (Multiset.powersetAux' l).revzip → x.1 + x.2 = ↑l
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey_ofList_of_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List ((a : α) × β a)} {k k' : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a.fst b.fst = Ordering.eq) l →
      k ∈ List.map Sigma.fst l →
        ∀ {h' : k' ∈ Std.DTreeMap.Raw.ofList l cmp}, (Std.DTreeMap.Raw.ofList l cmp).getKey k' h' = k
-- Mathlib.Analysis.InnerProductSpace.Basic
inner_neg_neg : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (x y : E), inner 𝕜 (-x) (-y) = inner 𝕜 x y
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Adjunction
ModuleCat.extendScalars_δ_tmul : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (M₁ M₂ : ModuleCat R) (m₁ : ↑M₁) (m₂ : ↑M₂),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Functor.OplaxMonoidal.δ (ModuleCat.extendScalars f) M₁ M₂))
      (1 ⊗ₜ[R] (m₁ ⊗ₜ[R] m₂)) =
    1 ⊗ₜ[R] m₁ ⊗ₜ[S] (1 ⊗ₜ[R] m₂)
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.toContDiffMapSupportedInClass : (E : Type u_2) →
  (F : Type u_3) →
    [inst : NormedAddCommGroup E] →
      [inst_1 : NormedSpace ℝ E] →
        [inst_2 : NormedAddCommGroup F] →
          [inst_3 : NormedSpace ℝ F] →
            {n : ℕ∞} →
              {K : TopologicalSpace.Compacts E} → ContDiffMapSupportedInClass (ContDiffMapSupportedIn E F n K) E F n K
-- Mathlib.Algebra.Ring.Subring.Defs
Subring.toSubsemiring_injective : ∀ {R : Type u} [inst : NonAssocRing R], Function.Injective Subring.toSubsemiring
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfc_predicate_one : ∀ (R : Type u_1) {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A] [inst_6 : Ring A]
  [inst_7 : StarRing A] [inst_8 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p], p 1
-- Mathlib.AlgebraicGeometry.Sites.QuasiCompact
AlgebraicGeometry.Scheme.propQCPrecoverage.eq_1 : ∀ (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme),
  AlgebraicGeometry.Scheme.propQCPrecoverage P =
    AlgebraicGeometry.Scheme.qcPrecoverage ⊓ AlgebraicGeometry.Scheme.precoverage P
-- Lean.Elab.ConfigEval.Commands
/-- `ensure_eval_term_instance t` ensures there is a `ConfigItem.EvalTerm t` instance by
deriving one or more instances if it needs to.
 -/
Lean.Elab.ConfigEval.ensureEvalTermInstance : Lean.ParserDescr
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
/-- For level `N = 1`, the gamma sets are all equal.  -/
EisensteinSeries.gammaSet_one_const : ∀ (r : ℕ) (a a' : Fin 2 → ZMod 1), EisensteinSeries.gammaSet 1 r a = EisensteinSeries.gammaSet 1 r a'
-- Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
AlgebraicClosure.instField : (k : Type u) → [inst : Field k] → Field (AlgebraicClosure k)
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.get!_erase_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : Inhabited α] [inst_1 : EquivBEq α]
  [inst_2 : LawfulHashable α] {k : α}, (m.erase k).get! k = default
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.mul_eq_one_iff : ∀ {α : Type u_2} [inst : DivisionMonoid α] {s t : Set α}, s * t = 1 ↔ ∃ a b, s = {a} ∧ t = {b} ∧ a * b = 1
-- Mathlib.Data.Finsupp.Single
Finsupp.single_eq_pi_single : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] [inst_1 : DecidableEq α] (a : α) (b : M),
  (⇑fun₀ | a => b) = Pi.single a b
-- Mathlib.CategoryTheory.Limits.Types.End
CategoryTheory.Limits.Types.coendRel.mk : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J]
  {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J (Type (max w u)))} {j j' : J} (f : j ⟶ j')
  (x : (F.obj (Opposite.op j')).obj j),
  CategoryTheory.Limits.Types.coendRel F ⟨j, (TypeCat.Hom.hom ((F.map f.op).app j)) x⟩
    ⟨j', (TypeCat.Hom.hom ((F.obj (Opposite.op j')).map f)) x⟩
-- Lean.Attributes
Lean.instInhabitedAttributeApplicationTime.default : Lean.AttributeApplicationTime
-- Mathlib.Analysis.Calculus.Implicit
HasStrictFDerivAt.implicitFunctionOfComplemented.congr_simp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : CompleteSpace E] {F : Type u_3} [inst_4 : NormedAddCommGroup F]
  [inst_5 : NormedSpace 𝕜 F] [inst_6 : CompleteSpace F] (f f_1 : E → F) (e_f : f = f_1) (f' : E →L[𝕜] F) {a a_1 : E}
  (e_a : a = a_1) (hf : HasStrictFDerivAt f f' a) (hf' : (↑f').range = ⊤) (hker : (↑f').ker.ClosedComplemented)
  (a_2 a_3 : F),
  a_2 = a_3 →
    ∀ (a_4 a_5 : ↥(↑f').ker),
      a_4 = a_5 →
        HasStrictFDerivAt.implicitFunctionOfComplemented f f' hf hf' hker a_2 a_4 =
          HasStrictFDerivAt.implicitFunctionOfComplemented f_1 f' ⋯ hf' hker a_3 a_5
-- Mathlib.Data.Seq.Computation
Computation.liftRel_rec : ∀ {α : Type u} {β : Type v} {R : α → β → Prop} (C : Computation α → Computation β → Prop),
  (∀ {ca : Computation α} {cb : Computation β}, C ca cb → Computation.LiftRelAux R C ca.destruct cb.destruct) →
    ∀ (ca : Computation α) (cb : Computation β), C ca cb → Computation.LiftRel R ca cb
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.coeff_zero_of_isScalarTower : ∀ {A : Type u_3} (B : Type u_4) (C : Type u_5) [inst : CommSemiring A] [inst_1 : CommSemiring B] [inst_2 : Semiring C]
  [inst_3 : Algebra A B] [inst_4 : Algebra A C] [inst_5 : Algebra B C] [IsScalarTower A B C] (p : Polynomial A),
  (algebraMap B C) ((algebraMap A B) (p.coeff 0)) = ((Polynomial.mapAlg A C) p).coeff 0
-- Mathlib.Algebra.Symmetrized
SymAlg.addMonoid : {α : Type u_1} → [AddMonoid α] → AddMonoid αˢʸᵐ
-- Mathlib.CategoryTheory.Triangulated.HomologicalFunctor
CategoryTheory.Functor.homologySequenceδ_naturality : ∀ {C : Type u_1} {A : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} A] (F : CategoryTheory.Functor C A) [inst_3 : F.ShiftSequence ℤ]
  (T T' : CategoryTheory.Pretriangulated.Triangle C) (φ : T ⟶ T') (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁),
  CategoryTheory.CategoryStruct.comp ((F.shift n₀).map φ.hom₃) (F.homologySequenceδ T' n₀ n₁ h) =
    CategoryTheory.CategoryStruct.comp (F.homologySequenceδ T n₀ n₁ h) ((F.shift n₁).map φ.hom₁)
-- Mathlib.RingTheory.Polynomial.Basic
Polynomial.degreeLE_mono : ∀ {R : Type u} [inst : Semiring R] {m n : WithBot ℕ}, m ≤ n → Polynomial.degreeLE R m ≤ Polynomial.degreeLE R n
-- Mathlib.Algebra.Polynomial.Module.AEval
Module.AEval'_def : ∀ {R : Type u_2} {M : Type u_1} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (φ : M →ₗ[R] M), Module.AEval' φ = Module.AEval R M φ
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.sum_blocksFun : ∀ {n : ℕ} (c : Composition n), ∑ i, c.blocksFun i = n
-- Lean.Util.FindExpr
/-- Search subterms  -/
Lean.Expr.FindStep.visit : Lean.Expr.FindStep
-- Aesop.Search.Expansion
Aesop.RuleResult.failed.sizeOf_spec : sizeOf Aesop.RuleResult.failed = 1
-- Mathlib.CategoryTheory.WithTerminal.Cone
CategoryTheory.WithInitial.commaFromUnder_map_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type w} [inst_1 : CategoryTheory.Category.{w', w} J]
  {X : C} {X_1 Y : CategoryTheory.Functor J (CategoryTheory.Under X)} (f : X_1 ⟶ Y),
  (CategoryTheory.WithInitial.commaFromUnder.map f).left = CategoryTheory.CategoryStruct.id X
-- Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
/-- The first factor of `p` in the universal factorization ring of `p`.  -/
Polynomial.UniversalFactorizationRing.factor₁ : {R : Type u_1} →
  [inst : CommRing R] →
    {n : ℕ} →
      (m k : ℕ) →
        (hn : n = m + k) →
          (p : Polynomial.MonicDegreeEq R n) →
            Polynomial.MonicDegreeEq (Polynomial.UniversalFactorizationRing m k hn p) m
-- Init.Data.Slice.Notation
Std.Rcc.Sliceable.mk : {α : Type u} → {β : outParam (Type v)} → {γ : outParam (Type w)} → (α → Std.Rcc β → γ) → Std.Rcc.Sliceable α β γ
-- Std.Data.ExtTreeSet.Basic
/-- Returns the `n`-th smallest element, or panics if `n` is at least `t.size`.  -/
Std.ExtTreeSet.atIdx! : {α : Type u} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → [Inhabited α] → Std.ExtTreeSet α cmp → ℕ → α
-- Mathlib.Algebra.Homology.ShortComplex.Homology
/-- Computation of the `f'` field of `LeftHomologyData.canonical`.  -/
CategoryTheory.ShortComplex.LeftHomologyData.canonical_f' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasHomology],
  (CategoryTheory.ShortComplex.LeftHomologyData.canonical S).f' = S.toCycles
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
/-- The right point of the walking cospan.  -/
CategoryTheory.Limits.WalkingCospan.right : CategoryTheory.Limits.WalkingCospan
-- Mathlib.RingTheory.Spectrum.Prime.Chevalley
/-- **Chevalley's theorem**: If `f` is of finite presentation,
then the image of a constructible set under `Spec(f)` is constructible.  -/
PrimeSpectrum.isConstructible_comap_image : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S},
  f.FinitePresentation →
    ∀ {s : Set (PrimeSpectrum S)}, Topology.IsConstructible s → Topology.IsConstructible (PrimeSpectrum.comap f '' s)
-- Init.Data.SInt.Lemmas
Int32.toBitVec_ofInt : ∀ (i : ℤ), (Int32.ofInt i).toBitVec = BitVec.ofInt 32 i
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxc.instIteratorIteratorIdOfUpwardEnumerableOfDecidableLE : {α : Type u} →
  [Std.PRange.UpwardEnumerable α] → [inst : LE α] → [DecidableLE α] → Std.Iterator (Std.Rxc.Iterator α) Id α
-- Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
HomotopicalAlgebra.mem_cofibrations : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y)
  [inst_1 : HomotopicalAlgebra.CategoryWithCofibrations C] [HomotopicalAlgebra.Cofibration f],
  HomotopicalAlgebra.cofibrations C f
-- Init.Grind.AC
Lean.Grind.AC.eq_norm_ac_cert : Lean.Grind.AC.Expr → Lean.Grind.AC.Expr → Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Bool
-- Mathlib.Order.Filter.AtTopBot.Basic
/-- A function `f` maps upwards closed sets (atTop sets) to upwards closed sets when it is a
Galois insertion. The Galois "insertion" and "connection" is weakened to only require it to be an
insertion and a connection above `b`.  -/
Filter.map_atTop_eq_of_gc_preorder : ∀ {α : Type u_3} {β : Type u_4} [inst : Preorder α] [IsDirectedOrder α] [inst_2 : Preorder β] [IsDirectedOrder β]
  {f : α → β},
  Monotone f →
    ∀ (b : β), (∀ (c : β), b ≤ c → ∃ x, f x = c ∧ ∀ (a : α), f a ≤ c ↔ a ≤ x) → Filter.map f Filter.atTop = Filter.atTop
-- Mathlib.Analysis.Seminorm
/-- **Alias** of `FunLike.coeAddMonoidHom`. -/
Seminorm.coeFnAddMonoidHom : (F : Type u_1) →
  (α : Type u_2) →
    (β : Type u_3) →
      [inst : FunLike F α β] →
        [inst_1 : AddZero F] → [inst_2 : AddZeroClass β] → [IsZeroApply F α β] → [IsAddApply F α β] → F →+ α → β
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Filter.Tendsto.log : ∀ {α : Type u_1} {f : α → ℝ} {l : Filter α} {x : ℝ},
  Filter.Tendsto f l (nhds x) → x ≠ 0 → Filter.Tendsto (fun x => Real.log (f x)) l (nhds (Real.log x))
-- Mathlib.Topology.ContinuousMap.Ideals
/-- The Galois insertion `ContinuousMap.opensOfIdeal : Ideal C(X, 𝕜) → Opens X` and
`fun s ↦ ContinuousMap.idealOfSet ↑s`.  -/
ContinuousMap.idealOpensGI : (X : Type u_1) →
  (𝕜 : Type u_2) →
    [inst : RCLike 𝕜] →
      [inst_1 : TopologicalSpace X] →
        [CompactSpace X] →
          [T2Space X] → GaloisInsertion ContinuousMap.opensOfIdeal fun s => ContinuousMap.idealOfSet 𝕜 ↑s
-- Mathlib.NumberTheory.Padics.PadicIntegers
/-- The `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`.  -/
PadicInt : (p : ℕ) → [hp : Fact (Nat.Prime p)] → Type
-- Mathlib.CategoryTheory.Limits.HasLimits
/-- An arbitrary choice of colimit object of a functor.  -/
CategoryTheory.Limits.colimit : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        (F : CategoryTheory.Functor J C) → [CategoryTheory.Limits.HasColimit F] → C
-- Mathlib.RingTheory.Conductor
quotAdjoinEquivQuotMap_apply_mk : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {x : S} {I : Ideal R}
  (hx : Ideal.comap (algebraMap R S) (conductor R x) ⊔ I = ⊤) (h_alg : Function.Injective ⇑(algebraMap (↥R[x]) S))
  (a : ↥R[x]),
  (quotAdjoinEquivQuotMap hx h_alg) ((Ideal.Quotient.mk (Ideal.map (algebraMap R ↥R[x]) I)) a) =
    (Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) ↑a
-- Lean.DocString.Types
Lean.Doc.Block.blockquote.sizeOf_spec : ∀ {i : Type u} {b : Type v} [inst : SizeOf i] [inst_1 : SizeOf b] (items : Array (Lean.Doc.Block i b)),
  sizeOf (Lean.Doc.Block.blockquote items) = 1 + sizeOf items
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getD_inter!_of_contains_eq_false_left : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {m₁ m₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  m₁.WF →
    m₂.WF →
      ∀ {k : α} {fallback : β},
        Std.DTreeMap.Internal.Impl.contains k m₁ = false →
          Std.DTreeMap.Internal.Impl.Const.getD (m₁.inter! m₂) k fallback = fallback
-- Mathlib.CategoryTheory.Idempotents.HomologicalComplex
CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.counitIso_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι},
  CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.counitIso.hom = CategoryTheory.eqToHom ⋯
-- Mathlib.Order.LatticeIntervals
Set.Ico.coe_bot : ∀ {α : Type u_1} [inst : PartialOrder α] (a b : α) [inst_1 : Fact (a < b)], ↑⊥ = a
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey?_ofList_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {l : List ((a : α) × β a)} {k : α},
  (List.map Sigma.fst l).contains k = false → (Std.ExtDHashMap.ofList l).getKey? k = none
-- Mathlib.Algebra.Group.Units.Defs
IsAddUnit.neg : ∀ {α : Type u} [inst : SubtractionMonoid α] {a : α}, IsAddUnit a → IsAddUnit (-a)
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify
PresheafOfModules.Sheafify.instSubsingletonSMulCandidate : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R₀ : CategoryTheory.Functor Cᵒᵖ RingCat} {R : CategoryTheory.Sheaf J RingCat} (α : R₀ ⟶ R.obj)
  [CategoryTheory.Presheaf.IsLocallySurjective J α] {M₀ : PresheafOfModules R₀}
  {A : CategoryTheory.Sheaf J AddCommGrpCat} (φ : M₀.presheaf ⟶ A.obj) [CategoryTheory.Presheaf.IsLocallySurjective J φ]
  {X : Cᵒᵖ} (r : ↑(R.obj.obj X)) (m : ↑(A.obj.obj X)), Subsingleton (PresheafOfModules.Sheafify.SMulCandidate α φ r m)
-- Mathlib.Tactic.Ring.RingNF
/-- `ring_nf` simplifies expressions in the language of commutative (semi)rings,
which rewrites all ring expressions into a normal form, allowing variables in the exponents.

`ring_nf` works as both a tactic and a conv tactic.

See also the `ring` tactic for solving a goal which is an equation in the language
of commutative (semi)rings.

* `ring_nf!` will use a more aggressive reducibility setting to identify atoms.
* `ring_nf (config := cfg)` allows for additional configuration (see `RingNF.Config`):
  * `red`: the reducibility setting (overridden by `!`)
  * `zetaDelta`: if true, local let variables can be unfolded (overridden by `!`)
  * `recursive`: if true, `ring_nf` will also recurse into atoms
* `ring_nf at l1 l2 ...` can be used to rewrite at the given locations.

Examples:
This can be used non-terminally to normalize ring expressions in the goal such as
`⊢ P (x + x + x)` ~> `⊢ P (x * 3)`, as well as being able to prove some equations that
`ring` cannot because they involve ring reasoning inside a subterm, such as
`sin (x + y) + sin (y + x) = 2 * sin (x + y)`.
 -/
Mathlib.Tactic.RingNF.convRing_nf!_ : Lean.ParserDescr
-- Std.Http.Data.Body.Full
/-- Closes the body, discarding any unconsumed data.
 -/
Std.Http.Body.Full.close : Std.Http.Body.Full → Std.Async.Async Unit
-- Mathlib.Analysis.InnerProductSpace.Calculus
contDiffAt_euclidean : ∀ {𝕜 : Type u_1} {ι : Type u_2} {H : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup H]
  [inst_2 : NormedSpace 𝕜 H] {f : H → EuclideanSpace 𝕜 ι} {y : H} [inst_3 : Fintype ι] {n : WithTop ℕ∞},
  ContDiffAt 𝕜 n f y ↔ ∀ (i : ι), ContDiffAt 𝕜 n (fun x => (f x).ofLp i) y
-- Mathlib.CategoryTheory.Limits.IsConnected
CategoryTheory.Limits.Types.pUnitCocone_pt : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C], (CategoryTheory.Limits.Types.pUnitCocone C).pt = PUnit.{w + 1}
-- Mathlib.Algebra.GradedMonoid
/-- The monoid `A 0` inherited from `R` in the presence of `SetLike.GradedMonoid A`.  -/
SetLike.GradeZero.instMonoid : {ι : Type u_1} →
  {R : Type u_2} →
    {S : Type u_3} →
      [inst : SetLike S R] →
        [inst_1 : Monoid R] → [inst_2 : AddMonoid ι] → {A : ι → S} → [SetLike.GradedMonoid A] → Monoid ↥(A 0)
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.antilipschitzWith_toLp : ∀ (p : ENNReal) {ι : Type u_2} (β : ι → Type u_4) [hp : Fact (1 ≤ p)] [inst : Fintype ι]
  [inst_1 : (i : ι) → PseudoEMetricSpace (β i)], AntilipschitzWith 1 (WithLp.toLp p)
-- Mathlib.Algebra.Algebra.Equiv
LinearEquiv.conjAlgEquiv_apply_apply : ∀ (R : Type u_1) {S : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : Module R M₁] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M₂] [inst_5 : Semiring S] [inst_6 : Module S M₁]
  [inst_7 : Module S M₂] [inst_8 : SMulCommClass S R M₁] [inst_9 : SMulCommClass S R M₂] [inst_10 : SMul R S]
  [inst_11 : IsScalarTower R S M₁] [inst_12 : IsScalarTower R S M₂] (e : M₁ ≃ₗ[S] M₂) (f : M₁ →ₗ[S] M₁) (x : M₂),
  ((LinearEquiv.conjAlgEquiv R e) f) x = e (f (e.symm x))
-- Mathlib.Analysis.Distribution.TestFunction
TestFunctionClass.map_contDiff : ∀ {B : Type u_6} {E : outParam (Type u_7)} {inst : NormedAddCommGroup E} {inst_1 : NormedSpace ℝ E}
  {Ω : outParam (TopologicalSpace.Opens E)} {F : outParam (Type u_8)} {inst_2 : NormedAddCommGroup F}
  {inst_3 : NormedSpace ℝ F} {n : outParam ℕ∞} [self : TestFunctionClass B Ω F n] (f : B), ContDiff ℝ ↑n ⇑f
-- Mathlib.Geometry.Euclidean.Inversion.Basic
Continuous.inversion : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {X : Type u_3} [inst_4 : TopologicalSpace X] {c x : X → P} {R : X → ℝ},
  Continuous c →
    Continuous R →
      Continuous x → (∀ (a : X), x a ≠ c a) → Continuous fun a => EuclideanGeometry.inversion (c a) (R a) (x a)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get!_diff_of_mem_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β}
  [inst_2 : LawfulBEq α], m₁.WF → m₂.WF → ∀ {k : α} [inst_3 : Inhabited (β k)], k ∈ m₂ → (m₁ \ m₂).get! k = default
-- Mathlib.CategoryTheory.Sites.CompatiblePlus
/-- The isomorphism between `P⁺ ⋙ F` and `(P ⋙ F)⁺`, functorially in `P`.  -/
CategoryTheory.GrothendieckTopology.plusFunctorWhiskerRightIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      {D : Type u_1} →
        [inst_1 : CategoryTheory.Category.{v_1, u_1} D] →
          {E : Type u_2} →
            [inst_2 : CategoryTheory.Category.{v_2, u_2} E] →
              (F : CategoryTheory.Functor D E) →
                [inst_3 :
                    ∀ (J : CategoryTheory.Limits.MulticospanShape),
                      CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) D] →
                  [inst_4 :
                      ∀ (J : CategoryTheory.Limits.MulticospanShape),
                        CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) E] →
                    [∀ (X : C) (W : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D),
                          CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F] →
                      [inst_6 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] →
                        [inst_7 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E] →
                          [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F] →
                            (J.plusFunctor D).comp ((CategoryTheory.Functor.whiskeringRight Cᵒᵖ D E).obj F) ≅
                              ((CategoryTheory.Functor.whiskeringRight Cᵒᵖ D E).obj F).comp (J.plusFunctor E)
-- Mathlib.CategoryTheory.Sites.InducedTopology
/-- The induced topology by a topology on `D` along a functor `F : C ⥤ D` is the finest
topology on `C` making `F` continuous.
[SGA4, III, 3.1][sga-4-tome-1]
 -/
CategoryTheory.Functor.inducedTopology : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        CategoryTheory.Functor C D → CategoryTheory.GrothendieckTopology D → CategoryTheory.GrothendieckTopology C
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
AddSubmonoid.opEquiv.eq_1 : ∀ {M : Type u_2} [inst : AddZeroClass M],
  AddSubmonoid.opEquiv =
    { toFun := AddSubmonoid.op, invFun := AddSubmonoid.unop, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }
-- Mathlib.Data.Multiset.OrderedMonoid
Multiset.instCanonicallyOrderedAdd : ∀ {α : Type u_1}, CanonicallyOrderedAdd (Multiset α)
-- Init.Data.Int.Linear
Int.Internal.Linear.eq_eq_subst_cert : Int.Internal.Linear.Var → Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → Bool
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get!_union_of_not_mem_left : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.ExtDTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] [inst_1 : Inhabited β] {k : α},
  k ∉ t₁ → Std.ExtDTreeMap.Const.get! (t₁.union t₂) k = Std.ExtDTreeMap.Const.get! t₂ k
-- Batteries.Data.String.Lemmas
String.get_cons_addChar : ∀ (c : Char) (cs : List Char) (i : String.Pos.Raw),
  String.Pos.Raw.get (String.ofList (c :: cs)) (i + c) = String.Pos.Raw.get (String.ofList cs) i