mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.map₂_obj_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : D} {S : CategoryTheory.Functor C D} {A : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} A] {B : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} B] {U : CategoryTheory.Functor A B} {V : B}
  {F : CategoryTheory.Functor C A} {G : CategoryTheory.Functor D B} (α : F.comp U ⟶ S.comp G) (β : G.obj T ⟶ V)
  (X : CategoryTheory.Comma S (CategoryTheory.Functor.fromPUnit T)),
  ((CategoryTheory.CostructuredArrow.map₂ α β).obj X).right = X.right
-- Mathlib.Algebra.Algebra.Subalgebra.Unitization
NonUnitalStarSubalgebra.unitization.congr_simp : ∀ {R : Type u_1} {S : 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] [inst_6 : SetLike S A]
  [hSA : NonUnitalSubsemiringClass S A] [hSRA : SMulMemClass S R A] [inst_7 : StarMemClass S A] (s : S),
  NonUnitalStarSubalgebra.unitization s = NonUnitalStarSubalgebra.unitization s
-- Mathlib.CategoryTheory.Limits.Shapes.Terminal
/-- We can more explicitly show that a category has a terminal object by specifying the object,
and showing there is a unique morphism to it from any other object.  -/
CategoryTheory.Limits.hasTerminal_of_unique : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (X : C) [∀ (Y : C), Nonempty (Y ⟶ X)]
  [∀ (Y : C), Subsingleton (Y ⟶ X)], CategoryTheory.Limits.HasTerminal C
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.MonoidalOpposite.mopMopEquivalence_functor_map : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : Cᴹᵒᵖᴹᵒᵖ} (f : X ⟶ Y),
  (CategoryTheory.MonoidalOpposite.mopMopEquivalence C).functor.map f = f.unmop.unmop
-- Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
AddSubgroup.op_eq_bot : ∀ {G : Type u_2} [inst : AddGroup G] {S : AddSubgroup G}, S.op = ⊥ ↔ S = ⊥
-- Mathlib.Analysis.Complex.Basic
/-- The natural `ContinuousLinearEquiv` from `ℂ` to `ℝ × ℝ`.  -/
Complex.equivRealProdCLM : ℂ ≃L[ℝ] ℝ × ℝ
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.WorkspaceSymbolParams : Type
-- Init.Data.Array.Lemmas
/-- Variant of `any_map` with a side condition for the `stop` argument.  -/
Array.any_map' : ∀ {α : Type u_1} {β : Type u_2} {stop : ℕ} {f : α → β} {xs : Array α} {p : β → Bool},
  stop = xs.size → (Array.map f xs).any p 0 stop = xs.any (p ∘ f)
-- Mathlib.Data.Num.Lemmas
Num.bit0_of_bit0 : ∀ (n : Num), n + n = n.bit0
-- Mathlib.Topology.Order.OrderClosed
Icc_mem_nhdsGT : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [ClosedIciTopology α] {a b : α},
  b < a → Set.Icc b a ∈ nhdsWithin b (Set.Ioi b)
-- Mathlib.CategoryTheory.Sites.Coherent.Equivalence
CategoryTheory.Equivalence.sheafCongrPrecoherent_inverse_map_hom_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Precoherent C] (A : Type u_3)
  [inst_3 : CategoryTheory.Category.{v_3, u_3} A] (e : C ≌ D)
  {X Y : CategoryTheory.Sheaf (CategoryTheory.coherentTopology D) A} (f : X ⟶ Y) (X_1 : Cᵒᵖ),
  ((CategoryTheory.Equivalence.sheafCongrPrecoherent A e).inverse.map f).hom.app X_1 =
    f.hom.app (Opposite.op (e.functor.obj (Opposite.unop X_1)))
-- Mathlib.Tactic.TacticAnalysis
/-- Environment extensions for `tacticAnalysis` declarations  -/
Mathlib.TacticAnalysis.tacticAnalysisExt : Lean.PersistentEnvExtension Mathlib.TacticAnalysis.Entry (Mathlib.TacticAnalysis.Entry × Mathlib.TacticAnalysis.Pass)
  (List Mathlib.TacticAnalysis.Entry × Array Mathlib.TacticAnalysis.Pass)
-- Init.Data.List.Find
List.finIdxOf?_eq_some_iff : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {l : List α} {a : α} {i : Fin l.length},
  List.finIdxOf? a l = some i ↔ l[i] = a ∧ ∀ j < i, ¬l[j] = a
-- Mathlib.FieldTheory.Minpoly.ConjRootClass
ConjRootClass.instFintypeElemCarrierOfNormalOfDecidableEqOfAlgEquiv : {K : Type u_1} →
  {L : Type u_2} →
    [inst : Field K] →
      [inst_1 : Field L] →
        [inst_2 : Algebra K L] →
          [Normal K L] → [DecidableEq L] → [Fintype Gal(L/K)] → (c : ConjRootClass K L) → Fintype ↑c.carrier
-- Mathlib.CategoryTheory.Bicategory.End
CategoryTheory.rightUnitor_def : ∀ {C : Type u} [inst : CategoryTheory.Bicategory C] (X : C) (f : X ⟶ X),
  CategoryTheory.MonoidalCategoryStruct.rightUnitor f = CategoryTheory.Bicategory.rightUnitor f
-- Mathlib.RingTheory.Ideal.Operations
Ideal.IsPrime.mul_le : ∀ {R : Type u} [inst : CommSemiring R] {I J P : Ideal R}, P.IsPrime → (I * J ≤ P ↔ I ≤ P ∨ J ≤ P)
-- Mathlib.Data.Matrix.Composition
Matrix.compAddEquiv_symm_apply : ∀ (I : Type u_1) (J : Type u_2) (K : Type u_3) (L : Type u_4) (R : Type u_5) [inst : Add R]
  (M : Matrix (I × K) (J × L) R), (Matrix.compAddEquiv I J K L R).symm M = (Matrix.comp I J K L R).symm M
-- Mathlib.Algebra.Star.StarRingHom
NonUnitalStarRingHom.coe_coe : ∀ {A : Type u_1} {B : Type u_2} [inst : NonUnitalNonAssocSemiring A] [inst_1 : Star A]
  [inst_2 : NonUnitalNonAssocSemiring B] [inst_3 : Star B] {F : Type u_5} [inst_4 : FunLike F A B]
  [inst_5 : NonUnitalRingHomClass F A B] [inst_6 : NonUnitalStarRingHomClass F A B] (f : F), ⇑↑f = ⇑f
-- Mathlib.LinearAlgebra.TensorProduct.Graded.External
TensorProduct.tmul_of_gradedMul_of_tmul : ∀ (R : Type u_1) {ι : Type u_2} [inst : CommSemiring ι] [inst_1 : Module ι (Additive ℤˣ)] [inst_2 : DecidableEq ι]
  (𝒜 : ι → Type u_3) (ℬ : ι → Type u_4) [inst_3 : CommRing R] [inst_4 : (i : ι) → AddCommGroup (𝒜 i)]
  [inst_5 : (i : ι) → AddCommGroup (ℬ i)] [inst_6 : (i : ι) → Module R (𝒜 i)] [inst_7 : (i : ι) → Module R (ℬ i)]
  [inst_8 : DirectSum.GRing 𝒜] [inst_9 : DirectSum.GRing ℬ] [inst_10 : DirectSum.GAlgebra R 𝒜]
  [inst_11 : DirectSum.GAlgebra R ℬ] (j₁ i₂ : ι) (a₁ : DirectSum ι fun i => 𝒜 i) (b₁ : ℬ j₁) (a₂ : 𝒜 i₂)
  (b₂ : DirectSum ι fun i => ℬ i),
  ((TensorProduct.gradedMul R 𝒜 ℬ) (a₁ ⊗ₜ[R] (DirectSum.lof R ι ℬ j₁) b₁)) ((DirectSum.lof R ι 𝒜 i₂) a₂ ⊗ₜ[R] b₂) =
    (-1) ^ (j₁ * i₂) • (a₁ * (DirectSum.lof R ι 𝒜 i₂) a₂) ⊗ₜ[R] ((DirectSum.lof R ι ℬ j₁) b₁ * b₂)
-- Lean.Elab.Term.TermElabM
/-- Gives all resolutions of the name `n`.

- `explicitLevels` provides a prefix of level parameters to the constant. For resolutions with a projection
component, the levels are not used, since they must apply to the last projection, not the constant.
In that case, the third component of the tuple is `explicitLevels`.
 -/
Lean.Elab.Term.resolveName : Lean.Syntax →
  Lean.Name →
    List Lean.Syntax.Preresolved →
      List Lean.Level →
        optParam (Option Lean.Expr) none → Lean.Elab.TermElabM (List (Lean.Expr × List String × List Lean.Level))
-- Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
/-- The inclusion `Δ[2] ⟶ Λ[3, 1]` which avoids `0`.  -/
SSet.horn₃₁.ι₀ : SSet.stdSimplex.obj { len := 2 } ⟶ (SSet.horn 3 1).toSSet
-- Mathlib.Algebra.Order.UpperLower
UpperSet.instDiv : {α : Type u_1} → [inst : CommGroup α] → [inst_1 : Preorder α] → [IsOrderedMonoid α] → Div (UpperSet α)
-- Mathlib.Algebra.Order.Interval.Finset.Basic
Finset.map_add_right_Icc : ∀ {α : Type u_2} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedCancelAddMonoid α]
  [ExistsAddOfLE α] [inst_4 : LocallyFiniteOrder α] (a b c : α),
  Finset.map (addRightEmbedding c) (Finset.Icc a b) = Finset.Icc (a + c) (b + c)
-- Mathlib.GroupTheory.Sylow
Sylow.mk.inj : ∀ {p : ℕ} {G : Type u_1} {inst : Group G} {toSubgroup : Subgroup G} {isPGroup' : IsPGroup p ↥toSubgroup}
  {is_maximal' : ∀ {Q : Subgroup G}, IsPGroup p ↥Q → toSubgroup ≤ Q → Q = toSubgroup} {toSubgroup_1 : Subgroup G}
  {isPGroup'_1 : IsPGroup p ↥toSubgroup_1}
  {is_maximal'_1 : ∀ {Q : Subgroup G}, IsPGroup p ↥Q → toSubgroup_1 ≤ Q → Q = toSubgroup_1},
  { toSubgroup := toSubgroup, isPGroup' := isPGroup', is_maximal' := is_maximal' } =
      { toSubgroup := toSubgroup_1, isPGroup' := isPGroup'_1, is_maximal' := is_maximal'_1 } →
    toSubgroup = toSubgroup_1
-- Mathlib.Data.Vector.Mem
List.Vector.mem_cons_of_mem : ∀ {α : Type u_1} {n : ℕ} (a a' : α) (v : List.Vector α n), a' ∈ v.toList → a' ∈ (a ::ᵥ v).toList
-- Mathlib.Topology.Order.LowerUpperTopology
/-- The lower topology is homeomorphic to the upper topology on the dual order
 -/
Topology.WithLower.toDualHomeomorph : {α : Type u_1} → [inst : Preorder α] → Topology.WithLower α ≃ₜ Topology.WithUpper αᵒᵈ
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roi.size_eq_match_rci : ∀ {α : Type u} {r : Std.Roi α} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.Rxi.HasSize α]
  [Std.PRange.LawfulUpwardEnumerable α] [Std.Rxi.IsAlwaysFinite α] [Std.Rxi.LawfulHasSize α],
  r.size =
    match Std.PRange.succ? r.lower with
    | none => 0
    | some next => next...*.size
-- Mathlib.Combinatorics.SimpleGraph.Density
/-- Edge density of a relation between two finsets of vertices.  -/
Rel.edgeDensity : {α : Type u_4} → {β : Type u_5} → (r : α → β → Prop) → [(a : α) → DecidablePred (r a)] → Finset α → Finset β → ℚ
-- Mathlib.FieldTheory.AlgebraicClosure
/-- If `i` is an `F`-algebra homomorphism from `E` to `K`, then the image of `algebraicClosure F E`
under the map `i` is contained in `algebraicClosure F K`.  -/
algebraicClosure.map_le_of_algHom : ∀ {F : Type u_1} {E : Type u_2} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {K : Type u_3}
  [inst_3 : Field K] [inst_4 : Algebra F K] (i : E →ₐ[F] K),
  IntermediateField.map i (algebraicClosure F E) ≤ algebraicClosure F K
-- Std.Http.Data.Headers
/-- Inserts a new key-value pair into the headers.
 -/
Std.Http.Headers.insert : Std.Http.Headers → Std.Http.Header.Name → Std.Http.Header.Value → Std.Http.Headers
-- Init.Data.SInt.Lemmas
Int32.mul_two : ∀ {a : Int32}, a * 2 = a + a
-- Lean.Elab.Tactic.Omega.Frontend
_private.Lean.Elab.Tactic.Omega.Frontend.0.Lean.Elab.Tactic.Omega.instEvalExprOmegaConfig : Lean.Elab.ConfigEval.EvalExpr Lean.Meta.Omega.OmegaConfig
-- Mathlib.Analysis.Complex.Harmonic.Analytic
/-- If a function `f : ℂ → ℝ` is harmonic, then `f` is the real part of a holomorphic function.
 -/
InnerProductSpace.HarmonicOnNhd.exists_analyticOnNhd_univ_re_eq : ∀ {f : ℂ → ℝ}, InnerProductSpace.HarmonicOnNhd f Set.univ → ∃ F, AnalyticOnNhd ℂ F Set.univ ∧ (fun z => (F z).re) = f
-- Mathlib.Order.Lex
instNonemptyColex : ∀ (α : Type u_2) [Nonempty α], Nonempty (Colex α)
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.glue!.match_1.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → Sort u_3)
  (h_1 : Unit → motive Std.DTreeMap.Internal.Impl.leaf)
  (h_2 :
    (r : Std.DTreeMap.Internal.Impl α β) →
      (sz' : ℕ) →
        (k' : α) →
          (v' : β k') →
            (l'' r'' : Std.DTreeMap.Internal.Impl α β) →
              r = Std.DTreeMap.Internal.Impl.inner sz' k' v' l'' r'' →
                motive (Std.DTreeMap.Internal.Impl.inner sz' k' v' l'' r'')),
  (match Std.DTreeMap.Internal.Impl.leaf with
    | Std.DTreeMap.Internal.Impl.leaf => h_1 ()
    | r@h:(Std.DTreeMap.Internal.Impl.inner sz' k' v' l'' r'') => h_2 r sz' k' v' l'' r'' h) =
    h_1 ()
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
lt_sub_comm : ∀ {α : Type u} [inst : AddCommGroup α] [inst_1 : LT α] [AddLeftStrictMono α] {a b c : α}, a < b - c ↔ c < b - a
-- Mathlib.Algebra.BigOperators.Finprod
/-- See also `finsum_smul` for a version that works even when the support of `f` is not finite,
but with slightly stronger typeclass requirements.  -/
finsum_smul' : ∀ {ι : Type u_3} {R : Type u_7} {M : Type u_8} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {f : ι → R}, Function.HasFiniteSupport f → ∀ (x : M), (∑ᶠ (i : ι), f i) • x = ∑ᶠ (i : ι), f i • x
-- Mathlib.Algebra.Group.Pointwise.Set.Small
small_sub : ∀ {α : Type u_1} (s t : Set α) [inst : Sub α] [Small.{u, u_1} ↑s] [Small.{u, u_1} ↑t], Small.{u, u_1} ↑(s - t)
-- Mathlib.Combinatorics.Matroid.Dual
Matroid.dualIndepMatroid_Indep : ∀ {α : Type u_1} (M : Matroid α) (I : Set α), M.dualIndepMatroid.Indep I = (I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B)
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.isIsolated_compl_iff_isUniversal : ∀ {V : Type u} {G : SimpleGraph V} {v : V}, Gᶜ.IsIsolated v ↔ G.IsUniversal v
-- Mathlib.Tactic.Positivity.Basic
Mathlib.Meta.Positivity.int_natAbs_pos : ∀ {n : ℤ}, 0 < n → 0 < n.natAbs
-- Mathlib.Data.Set.Function
Set.LeftInvOn.mapsTo : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} {f' : β → α},
  Set.LeftInvOn f' f s → Set.SurjOn f s t → Set.MapsTo f' t s
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem_eq_get_getElem? : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {a : α} {h : a ∈ m}, m[a] = m[a]?.get ⋯
-- Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset
CategoryTheory.CardinalDirectedPoset.Hom.injective : ∀ {κ : Cardinal.{u}} [inst : Fact κ.IsRegular] {J₁ J₂ : CategoryTheory.CardinalDirectedPoset κ} (f : J₁ ⟶ J₂),
  Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Init.Data.String.OrderInstances
String.Slice.Pos.instTransLe : {s : String.Slice} → Trans (fun x1 x2 => x1 ≤ x2) (fun x1 x2 => x1 ≤ x2) fun x1 x2 => x1 ≤ x2
-- Mathlib.Data.Complex.Basic
Complex.im_ofReal_mul : ∀ (r : ℝ) (z : ℂ), (↑r * z).im = r * z.im
-- Mathlib.Topology.Algebra.Module.Equiv
/-- Continuous linear equivalence between two equal submodules:
this is `LinearEquiv.ofEq` as a continuous linear equivalence  -/
ContinuousLinearEquiv.ofEq : {R : Type u_1} →
  {M : Type u_3} →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : TopologicalSpace M] → {module_M : Module R M} → (p q : Submodule R M) → p = q → ↥p ≃L[R] ↥q
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
/-- This function is used to give an upper bound on the summands in Eisenstein series; it is
defined by `z ↦ min z.im √(z.im ^ 2 / (z.re ^ 2 + z.im ^ 2))`.  -/
EisensteinSeries.r : UpperHalfPlane → ℝ
-- ProofWidgets.Presentation.Expr
ProofWidgets.ExprPresentations : Type
-- Mathlib.LinearAlgebra.Prod
LinearMap.range_prod_le : ∀ {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M] [inst_5 : Module R M₂]
  [inst_6 : Module R M₃] (f : M →ₗ[R] M₂) (g : M →ₗ[R] M₃), (f.prod g).range ≤ f.range.prod g.range
-- Mathlib.Order.Irreducible
InfIrred.ne_top : ∀ {α : Type u_2} [inst : SemilatticeInf α] {a : α} [inst_1 : OrderTop α], InfIrred a → a ≠ ⊤
-- Mathlib.Data.Finset.Insert
Finset.ssubset_iff_exists_cons_subset : ∀ {α : Type u_1} {s t : Finset α}, s ⊂ t ↔ ∃ a, ∃ (h : a ∉ s), Finset.cons a s h ⊆ t
-- Mathlib.Algebra.Star.SelfAdjoint
IsSelfAdjoint.intCast : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : StarRing R] (z : ℤ), IsSelfAdjoint ↑z
-- Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
CategoryTheory.IsFiltered.IsEventuallyConstant.exists_isEventuallyConstantFrom : ∀ {J : Type u_1} {C : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} J}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} C} {F : CategoryTheory.Functor J C}
  [self : CategoryTheory.IsFiltered.IsEventuallyConstant F], ∃ i, F.IsEventuallyConstantFrom i
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Oplax
/-- Associator for the vertical composition of oplax natural transformations.  -/
CategoryTheory.Oplax.OplaxTrans.associator : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G H I : CategoryTheory.OplaxFunctor B C} →
          (η : F ⟶ G) →
            (θ : G ⟶ H) →
              (ι : H ⟶ I) →
                CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp η θ) ι ≅
                  CategoryTheory.CategoryStruct.comp η (CategoryTheory.CategoryStruct.comp θ ι)
-- Init.Data.Vector.Monadic
_private.Init.Data.Vector.Monadic.0.Array.forIn'_eq_foldlM.match_1.eq_1 : ∀ {β : Type u_1} (motive : ForInStep β → Sort u_2) (b : β) (h_1 : (b : β) → motive (ForInStep.yield b))
  (h_2 : (b : β) → motive (ForInStep.done b)),
  (match ForInStep.yield b with
    | ForInStep.yield b => h_1 b
    | ForInStep.done b => h_2 b) =
    h_1 b
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.find?_toList_eq_none_iff_not_mem : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k : α}, List.find? (fun x => x.fst == k) m.toList = none ↔ k ∉ m
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.surjOn_logb' : ∀ {b : ℝ}, 0 < b → b ≠ 1 → Set.SurjOn (Real.logb b) (Set.Iio 0) Set.univ
-- Mathlib.CategoryTheory.Sites.LocallySurjective
CategoryTheory.Presheaf.isLocallySurjective_toSheafify' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_1, u_2} D] {FD : D → D → Type u_3} {CD : D → Type (max u v)}
  [inst_2 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [inst_3 : CategoryTheory.ConcreteCategory D FD]
  (P : CategoryTheory.Functor Cᵒᵖ D) [inst_4 : CategoryTheory.HasWeakSheafify J D]
  [J.HasSheafCompose (CategoryTheory.forget D)] [J.PreservesSheafification (CategoryTheory.forget D)],
  CategoryTheory.Presheaf.IsLocallySurjective J (CategoryTheory.toSheafify J P)
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
SSet.Edge.CompStruct.ext_iff : ∀ {X : SSet} {x₀ x₁ x₂ : X.obj (Opposite.op { len := 0 })} {e₀₁ : SSet.Edge x₀ x₁} {e₁₂ : SSet.Edge x₁ x₂}
  {e₀₂ : SSet.Edge x₀ x₂} {h h' : e₀₁.CompStruct e₁₂ e₀₂}, h = h' ↔ h.simplex = h'.simplex
-- Mathlib.Data.Finset.Lattice.Fold
Finset.isLUB_sup_id : ∀ {α : Type u_2} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s : Finset α}, IsLUB (↑s) (s.sup id)
-- Mathlib.SetTheory.Ordinal.Principal
Ordinal.isPrincipal_add_of_isPrincipal_mul : ∀ {o : Ordinal.{u}}, Ordinal.IsPrincipal (fun x1 x2 => x1 * x2) o → o ≠ 2 → Ordinal.IsPrincipal (fun x1 x2 => x1 + x2) o
-- Init.Data.UInt.Lemmas
UInt16.ofNat_mul : ∀ (a b : ℕ), UInt16.ofNat (a * b) = UInt16.ofNat a * UInt16.ofNat b
-- Batteries.Data.List.Count
/-- `idxToSigmaCount` is essentially a `Fin`-to-`Fin` wrapper for `countBefore` that also
includes the corresponding element.

For example:
```
idxToSigmaCount [5, 1, 3, 2, 4, 0, 1, 4] 5 = ⟨0, 0⟩
```
 -/
List.idxToSigmaCount : {α : Type u_1} → [inst : BEq α] → [ReflBEq α] → (xs : List α) → Fin xs.length → (x : α) × Fin (List.count x xs)
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupSeminorm.add_comp : ∀ {E : Type u_3} {F : Type u_4} [inst : AddGroup E] [inst_1 : AddGroup F] (p q : AddGroupSeminorm E) (f : F →+ E),
  (p + q).comp f = p.comp f + q.comp f
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- Twice the angle between a vector and a multiple of that vector is 0.  -/
Orientation.two_zsmul_oangle_smul_right_self : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) (x : V) {r : ℝ}, 2 • o.oangle x (r • x) = 0
-- Mathlib.RingTheory.Noetherian.Basic
IsNoetherianRing.of_finite : ∀ (R : Type u_1) (S : Type u_2) [inst : Ring R] [inst_1 : Ring S] [inst_2 : Module R S] [IsScalarTower R S S]
  [IsNoetherianRing R] [Module.Finite R S], IsNoetherianRing S
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.instCommutativeHAdd : ∀ {α : Type u_1} [inst : Lean.Grind.IntModule α], Std.Commutative fun x1 x2 => x1 + x2
-- Mathlib.RingTheory.Ideal.GoingUp
/-- **Alias** of `Ideal.IsIntegral.eq_bot_of_comap_eq_bot`. -/
Ideal.IsIntegralClosure.eq_bot_of_comap_eq_bot : ∀ (R : Type u_1) [inst : CommRing R] {A : Type u_3} [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [Algebra.IsIntegral R A] [IsDomain A] [Nontrivial R] {I : Ideal A}, Ideal.comap (algebraMap R A) I = ⊥ → I = ⊥
-- Mathlib.Algebra.Order.Monoid.Unbundled.Pow
/-- This lemma is useful in non-cancellative monoids, like sets under pointwise operations.  -/
pow_le_pow_mul_of_sq_le_mul : ∀ {M : Type u_3} [inst : Monoid M] [inst_1 : Preorder M] [MulRightMono M] [MulLeftMono M] {a b : M},
  a ^ 2 ≤ b * a → ∀ {n : ℕ}, n ≠ 0 → a ^ n ≤ b ^ (n - 1) * a
-- Init.Grind.Attr
/-- The `unfold` modifier instructs `grind` to unfold the given definition during the preprocessing step.
Example:
```
@[grind unfold] def h (x : Nat) := 2 * x
example : 6 ∣ 3*h x := by grind
```
 -/
Lean.Parser.Attr.grindUnfold : Lean.ParserDescr
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
CategoryTheory.Functor.hasPointwiseRightKanExtensionAt_iff_of_equivalence : ∀ {C : Type u_1} {D : Type u_2} {D' : Type u_3} {H : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} D']
  [inst_3 : CategoryTheory.Category.{v_4, u_4} H] (L : CategoryTheory.Functor C D) (L' : CategoryTheory.Functor C D')
  (F : CategoryTheory.Functor C H) (E : D ≌ D') (eL : L.comp E.functor ≅ L') (Y : D) (Y' : D')
  (e : E.functor.obj Y ≅ Y'), L.HasPointwiseRightKanExtensionAt F Y ↔ L'.HasPointwiseRightKanExtensionAt F Y'
-- Mathlib.Algebra.Azumaya.Defs
AlgHom.mulLeftRight_apply : ∀ (R : Type u_1) (A : Type u_2) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (a : A) (b : Aᵐᵒᵖ)
  (x : A), ((AlgHom.mulLeftRight R A) (a ⊗ₜ[R] b)) x = a * x * MulOpposite.unop b
-- Std.Data.HashSet.Lemmas
Std.HashSet.size_add_size_eq_size_union_add_size_inter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α],
  m₁.size + m₂.size = (m₁ ∪ m₂).size + (m₁ ∩ m₂).size
-- Init.Data.Option.Basic
Option.min_none_right : ∀ {α : Type u_1} [inst : Min α] {o : Option α}, o ⊓ none = none
-- Mathlib.Data.List.Chain
List.IsChain.suffix : ∀ {α : Type u_1} {R : α → α → Prop} {l l₁ : List α}, List.IsChain R l → l₁ <:+ l → List.IsChain R l₁
-- Mathlib.Order.Filter.Map
/-- If functions `m₁` and `m₂` are eventually equal at a filter `f`, then
they map this filter to the same filter.  -/
Filter.map_congr : ∀ {α : Type u_1} {β : Type u_2} {m₁ m₂ : α → β} {f : Filter α}, m₁ =ᶠ[f] m₂ → Filter.map m₁ f = Filter.map m₂ f
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.IsAddFundamentalDomain.lintegral_eq_tsum : ∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α] {s : Set α}
  {μ : MeasureTheory.Measure α} [MeasurableConstVAdd G α] [MeasureTheory.VAddInvariantMeasure G α μ] [Countable G],
  MeasureTheory.IsAddFundamentalDomain G s μ →
    ∀ (f : α → ENNReal), ∫⁻ (x : α), f x ∂μ = ∑' (g : G), ∫⁻ (x : α) in g +ᵥ s, f x ∂μ
-- Mathlib.MeasureTheory.OuterMeasure.OfFunction
/-- Given any function `m` assigning measures to sets, there is a unique maximal outer measure `μ`
satisfying `μ s ≤ m s` for all `s : Set α`. This is the same as `OuterMeasure.ofFunction`,
except that it doesn't require `m ∅ = 0`.  -/
MeasureTheory.OuterMeasure.boundedBy : {α : Type u_1} → (Set α → ENNReal) → MeasureTheory.OuterMeasure α
-- Mathlib.Data.PNat.Factors
/-- The product of the factors is the original number  -/
PNat.prod_factorMultiset : ∀ (n : ℕ+), n.factorMultiset.prod = n
-- Mathlib.Analysis.Matrix.Normed
/-- Normed space instance (using sup norm of L1 norm) for matrices over a normed space.  Not
declared as an instance because there are several natural choices for defining the norm of a
matrix.  -/
Matrix.linftyOpNormedSpace : {R : Type u_1} →
  {m : Type u_3} →
    {n : Type u_4} →
      {α : Type u_5} →
        [inst : Fintype m] →
          [inst_1 : Fintype n] →
            [inst_2 : NormedField R] →
              [inst_3 : SeminormedAddCommGroup α] → [NormedSpace R α] → NormedSpace R (Matrix m n α)