mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
/-- If `f` is a positive map, then it is bounded (and therefore continuous).
 -/
PositiveLinearMap.exists_norm_apply_le : ∀ {A₁ : Type u_1} {A₂ : Type u_2} [inst : NonUnitalCStarAlgebra A₁] [inst_1 : NonUnitalCStarAlgebra A₂]
  [inst_2 : PartialOrder A₁] [StarOrderedRing A₁] [inst_4 : PartialOrder A₂] [StarOrderedRing A₂] (f : A₁ →ₚ[ℂ] A₂),
  ∃ C, ∀ (a : A₁), ‖f a‖ ≤ ↑C * ‖a‖
-- Mathlib.RingTheory.FractionalIdeal.Basic
IsFractional.inf_right : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  {I : Submodule R P}, IsFractional S I → ∀ (J : Submodule R P), IsFractional S (I ⊓ J)
-- Aesop.RuleTac.RuleTerm
Aesop.instInhabitedElabRuleTerm.default : Aesop.ElabRuleTerm
-- Std.Sat.AIG.Basic
/-- Denotation of an `AIG` at a specific `Entrypoint`.
 -/
Std.Sat.AIG.«term⟦_,_⟧» : Lean.ParserDescr
-- Init.Data.String.Defs
/-- A region or slice of some underlying string.

A slice consists of a string together with the start and end byte positions of a region of
interest. Actually extracting a substring requires copying and memory allocation, while many
slices of the same underlying string may exist with very little overhead. While this could be
achieved by tracking the bounds by hand, the slice API is much more convenient.

`String.Slice` bundles proofs to ensure that the start and end positions always delineate a valid
string. For this reason, it should be preferred over `Substring.Raw`.
 -/
String.Slice : Type
-- Mathlib.RingTheory.Extension.Cotangent.BaseChange
/-- The cotangent space of an extension commutes with base change.  -/
Algebra.Extension.tensorCotangentSpace : {R : Type u_1} →
  {S : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          (P : Algebra.Extension R S) →
            (T : Type u_4) →
              [inst_3 : CommRing T] →
                [inst_4 : Algebra R T] → TensorProduct R T P.CotangentSpace ≃ₗ[T] P.baseChange.CotangentSpace
-- Mathlib.Data.Sym.Sym2
Sym2.instIsEmpty : ∀ {α : Type u_1} [IsEmpty α], IsEmpty (Sym2 α)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem?_erase : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k a : α},
  (t.erase k)[a]? = if cmp k a = Ordering.eq then none else t[a]?
-- Mathlib.Order.Preorder.Finsupp
Finsupp.lt_def : ∀ {ι : Type u_1} {M : Type u_2} [inst : Zero M] [inst_1 : Preorder M] {f g : ι →₀ M}, f < g ↔ f ≤ g ∧ ∃ i, f i < g i
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.rpow_natCast_mul : ∀ (x : NNReal) (n : ℕ) (z : ℝ), x ^ (↑n * z) = (x ^ n) ^ z
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
CategoryTheory.Pseudofunctor.DescentData'.comp_pullHom''_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} {sq : (i j : ι) → CategoryTheory.Limits.ChosenPullback (f i) (f j)}
  {sq₃ : (i₁ i₂ i₃ : ι) → CategoryTheory.Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)}
  {obj : (i : ι) → ↑(F.obj { as := Opposite.op (X i) })}
  (hom :
    (i j : ι) →
      (F.map (sq i j).p₁.op.toLoc).toFunctor.obj (obj i) ⟶ (F.map (sq i j).p₂.op.toLoc).toFunctor.obj (obj j)),
  (∀ (i₁ i₂ i₃ : ι),
      CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Pseudofunctor.DescentData'.pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₂ ⋯
            ⋯)
          (CategoryTheory.Pseudofunctor.DescentData'.pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₂ (sq₃ i₁ i₂ i₃).p₃ ⋯
            ⋯) =
        CategoryTheory.Pseudofunctor.DescentData'.pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₃ ⋯
          ⋯) →
    ∀ ⦃Y : C⦄ (q : Y ⟶ S) ⦃i₁ i₂ i₃ : ι⦄ (f₁ : Y ⟶ X i₁) (f₂ : Y ⟶ X i₂) (f₃ : Y ⟶ X i₃)
      (hf₁ : CategoryTheory.CategoryStruct.comp f₁ (f i₁) = q) (hf₂ : CategoryTheory.CategoryStruct.comp f₂ (f i₂) = q)
      (hf₃ : CategoryTheory.CategoryStruct.comp f₃ (f i₃) = q) {Z : ↑(F.obj { as := Opposite.op Y })}
      (h : (F.map f₃.op.toLoc).toFunctor.obj (obj i₃) ⟶ Z),
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Pseudofunctor.DescentData'.pullHom' hom q f₁ f₂ ⋯ ⋯)
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Pseudofunctor.DescentData'.pullHom' hom q f₂ f₃ ⋯ ⋯) h) =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Pseudofunctor.DescentData'.pullHom' hom q f₁ f₃ ⋯ ⋯) h
-- Mathlib.SetTheory.ZFC.Ordinal
ZFSet.IsOrdinal.mem_of_subset_of_mem : ∀ {x y z : ZFSet.{u}}, x.IsOrdinal → z.IsOrdinal → x ⊆ y → y ∈ z → x ∈ z
-- Mathlib.RingTheory.Noetherian.Defs
isNoetherian_submodule' : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [IsNoetherian R M]
  (N : Submodule R M), IsNoetherian R ↥N
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.div_pf : ∀ {R : Type u_2} [inst : Semifield R] {a b c d : R}, b⁻¹ = c → a * c = d → a / b = d
-- Mathlib.RingTheory.Congruence.Basic
RingCon.nontrivial_quotient : ∀ {R : Type u_3} [inst : Add R] [inst_1 : Mul R] {c : RingCon R}, Nontrivial c.Quotient ↔ c ≠ ⊤
-- Mathlib.Topology.Instances.Discrete
OrderTopology.of_linearLocallyFinite : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [LocallyFiniteOrder α] [DiscreteTopology α],
  OrderTopology α
-- Init.Data.SInt.Lemmas
Int16.toInt_sub_of_le : ∀ (a b : Int16), 0 ≤ b → b ≤ a → (a - b).toInt = a.toInt - b.toInt
-- Mathlib.CategoryTheory.Subfunctor.Image
CategoryTheory.Subfunctor.preimage_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F F' F'' : CategoryTheory.Functor C (Type w)}
  (G : CategoryTheory.Subfunctor F) (f : F'' ⟶ F') (g : F' ⟶ F),
  G.preimage (CategoryTheory.CategoryStruct.comp f g) = (G.preimage g).preimage f
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem!_diff_of_not_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  [inst : Inhabited β], k ∉ t₂ → (t₁ \ t₂)[k]! = t₁[k]!
-- Init.System.IO
IO.FS.Metadata.mk.injEq : ∀ (accessed modified : IO.FS.SystemTime) (byteSize : UInt64) (type : IO.FS.FileType) (numLinks : UInt64)
  (accessed_1 modified_1 : IO.FS.SystemTime) (byteSize_1 : UInt64) (type_1 : IO.FS.FileType) (numLinks_1 : UInt64),
  ({ accessed := accessed, modified := modified, byteSize := byteSize, type := type, numLinks := numLinks } =
      { accessed := accessed_1, modified := modified_1, byteSize := byteSize_1, type := type_1,
        numLinks := numLinks_1 }) =
    (accessed = accessed_1 ∧ modified = modified_1 ∧ byteSize = byteSize_1 ∧ type = type_1 ∧ numLinks = numLinks_1)
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
CategoryTheory.Oplax.OplaxTrans.categoryStruct_id_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.OplaxFunctor B C) (a : B),
  (CategoryTheory.CategoryStruct.id F).app a = CategoryTheory.CategoryStruct.id (F.obj a)
-- Mathlib.Algebra.Module.LinearMap.Defs
SemilinearMapClass.toMulActionSemiHomClass : ∀ {F : Type u_14} {R : outParam (Type u_15)} {S : outParam (Type u_16)} {inst : Semiring R} {inst_1 : Semiring S}
  {σ : outParam (R →+* S)} {M : outParam (Type u_17)} {M₂ : outParam (Type u_18)} {inst_2 : AddCommMonoid M}
  {inst_3 : AddCommMonoid M₂} {inst_4 : Module R M} {inst_5 : Module S M₂} {inst_6 : FunLike F M M₂}
  [self : SemilinearMapClass F σ M M₂], MulActionSemiHomClass F (⇑σ) M M₂
-- Mathlib.Topology.Category.UniformSpace
/-- The mate of a morphism from a `UniformSpace` to a `CpltSepUniformSpace`.  -/
UniformSpaceCat.extensionHom : {X : UniformSpaceCat} →
  {Y : CpltSepUniformSpace} →
    (X ⟶ (CategoryTheory.forget₂ CpltSepUniformSpace UniformSpaceCat).obj Y) →
      (UniformSpaceCat.completionFunctor.obj X ⟶ Y)
-- Init.Data.Int.DivMod.Lemmas
Int.bmod_neg : ∀ (x : ℤ) (m : ℕ), x % ↑m ≥ (↑m + 1) / 2 → x.bmod m = x % ↑m - ↑m
-- Mathlib.Topology.LocallyConstant.Basic
LocallyConstant.indicator_apply : ∀ {X : Type u_1} [inst : TopologicalSpace X] {R : Type u_5} [inst_1 : Zero R] {U : Set X} (f : LocallyConstant X R)
  (hU : IsClopen U) (x : X), (f.indicator hU) x = U.indicator (⇑f) x
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.LaxBraidedFunctor.mk.injEq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {D : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_4 : CategoryTheory.MonoidalCategory D] [inst_5 : CategoryTheory.BraidedCategory D]
  (toFunctor : CategoryTheory.Functor C D)
  (laxBraided : autoParam toFunctor.LaxBraided CategoryTheory.LaxBraidedFunctor.laxBraided._autoParam)
  (toFunctor_1 : CategoryTheory.Functor C D)
  (laxBraided_1 : autoParam toFunctor_1.LaxBraided CategoryTheory.LaxBraidedFunctor.laxBraided._autoParam),
  ({ toFunctor := toFunctor, laxBraided := laxBraided } = { toFunctor := toFunctor_1, laxBraided := laxBraided_1 }) =
    (toFunctor = toFunctor_1 ∧ laxBraided ≍ laxBraided_1)
-- Lean.Meta.RecursorInfo
_private.Lean.Meta.RecursorInfo.0.Lean.Meta.getMajorPosDepElim : Lean.Name → Option ℕ → Array Lean.Expr → Array Lean.Expr → Lean.MetaM (Lean.Expr × ℕ × Bool)
-- Mathlib.Geometry.Convex.Cone.Face.Basic
/-- The product of two faces of two cones is a face of the product of the cones.  -/
PointedCone.IsFaceOf.prod : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : DivisionRing R] [inst_1 : LinearOrder R]
  [inst_2 : IsOrderedRing R] [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : AddCommGroup N]
  [inst_6 : Module R N] {C₁ F₁ : PointedCone R M} {C₂ F₂ : PointedCone R N},
  F₁.IsFaceOf C₁ → F₂.IsFaceOf C₂ → PointedCone.IsFaceOf (Submodule.prod F₁ F₂) (Submodule.prod C₁ C₂)
-- Mathlib.Algebra.Star.CHSH
IsCHSHTuple.A₀B₁_commutes : ∀ {R : Type u_1} [inst : Monoid R] [inst_1 : StarMul R] {A₀ A₁ B₀ B₁ : R}, IsCHSHTuple A₀ A₁ B₀ B₁ → A₀ * B₁ = B₁ * A₀
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.Hom.id_τ₄ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C),
  (CategoryTheory.Square.Hom.id sq).τ₄ = CategoryTheory.CategoryStruct.id sq.X₄
-- Mathlib.Analysis.Calculus.Gradient.Basic
HasGradientWithinAt.congr_mono : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F] [inst_2 : InnerProductSpace 𝕜 F]
  [inst_3 : CompleteSpace F] {f : F → 𝕜} {f' x : F} {s : Set F} {f₁ : F → 𝕜} {t : Set F},
  HasGradientWithinAt f f' s x → (∀ x ∈ t, f₁ x = f x) → f₁ x = f x → t ⊆ s → HasGradientWithinAt f₁ f' t x
-- Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1
/-- The cohomology in degree 1 of a presheaf of groups
`G : Cᵒᵖ ⥤ GrpCat` on a family of objects `U : I → C`.  -/
CategoryTheory.PresheafOfGroups.H1 : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.Functor Cᵒᵖ GrpCat → {I : Type w'} → (I → C) → Type (max (max (max u v) w) w')
-- Init.Data.SInt.Lemmas
Int16.add_assoc : ∀ (a b c : Int16), a + b + c = a + (b + c)
-- Mathlib.Algebra.GroupWithZero.NonZeroDivisors
mul_right_mem_nonZeroDivisorsRight_eq_zero_iff : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] {r x : M₀}, r ∈ nonZeroDivisorsRight M₀ → (x * r = 0 ↔ x = 0)
-- Init.Data.List.Zip
List.tail_zip_snd : ∀ {α : Type u_1} {β : Type u_2} {l : List (α × β)}, l.unzip.2.tail = l.tail.unzip.2
-- Mathlib.GroupTheory.Complement
AddSubgroup.IsComplement.add_eq : ∀ {G : Type u_1} [inst : AddGroup G] {S T : Set G}, AddSubgroup.IsComplement S T → S + T = Set.univ
-- Mathlib.Algebra.GroupWithZero.NonZeroDivisors
/-- Canonical isomorphism between the non-zero-divisors and units of a group with zero.  -/
nonZeroDivisorsEquivUnits : {G₀ : Type u_1} → [inst : GroupWithZero G₀] → ↥(nonZeroDivisors G₀) ≃* G₀ˣ
-- Mathlib.Algebra.Algebra.Unitization
Unitization.inl_mul_inl : ∀ {R : Type u_1} (A : Type u_2) [inst : Mul R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : SMulZeroClass R A]
  (r₁ r₂ : R), Unitization.inl r₁ * Unitization.inl r₂ = Unitization.inl (r₁ * r₂)
-- Lean.Meta.Match.MatcherInfo
Lean.Meta.Match.Overlaps.overlapping : Lean.Meta.Match.Overlaps → ℕ → Array ℕ
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.lift_lt_aleph_natCast : ∀ {c : Cardinal.{u}} {n : ℕ}, Cardinal.lift.{v, u} c < Cardinal.aleph ↑n ↔ c < Cardinal.aleph ↑n
-- Mathlib.CategoryTheory.Limits.Shapes.PiProd
/-- The projection maps of a product to the products indexed by a subset and its complement, as a
binary fan.
 -/
CategoryTheory.Limits.Pi.binaryFanOfProp : {C : Type u_1} →
  {I : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      (X : I → C) →
        (P : I → Prop) →
          [CategoryTheory.Limits.HasProduct X] →
            [inst_2 : CategoryTheory.Limits.HasProduct fun i => X ↑i] →
              [inst_3 : CategoryTheory.Limits.HasProduct fun i => X ↑i] →
                CategoryTheory.Limits.BinaryFan (∏ᶜ fun i => X ↑i) (∏ᶜ fun i => X ↑i)
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.instInitialOppositeLeftOpOfFinal : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor C Dᵒᵖ) [F.Final], F.leftOp.Initial
-- Mathlib.Order.Category.PartOrdEmb
_private.Mathlib.Order.Category.PartOrdEmb.0.PartOrdEmb.Hom.mk.sizeOf_spec : ∀ {X Y : PartOrdEmb} (hom' : ↑X ↪o ↑Y), sizeOf { hom' := hom' } = 1 + sizeOf hom'
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Meromorphic
/-- The function `tan` is meromorphic at any `z`.  -/
Complex.meromorphicAt_tan : ∀ (z : ℂ), MeromorphicAt Complex.tan z
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.instNonAssocSemiring : {n : Type u_2} →
  {A : Type u_5} → [Fintype n] → [DecidableEq n] → [NonAssocSemiring A] → NonAssocSemiring (CStarMatrix n n A)
-- Init.Data.Bool
Bool.and_xor_distrib_left : ∀ (x y z : Bool), (x && (y ^^ z)) = (x && y ^^ x && z)
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.FunctorCategory
CategoryTheory.instHasExactColimitsOfShapeFunctorOfHasFiniteLimits : ∀ {A : Type u_1} {C : Type u_2} {J : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] [inst_2 : CategoryTheory.Category.{v_3, u_3} J]
  [inst_3 : CategoryTheory.Limits.HasColimitsOfShape J A] [CategoryTheory.HasExactColimitsOfShape J A]
  [CategoryTheory.Limits.HasFiniteLimits A], CategoryTheory.HasExactColimitsOfShape J (CategoryTheory.Functor C A)
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.SimprocOLeanEntry.post : Lean.Meta.Simp.SimprocOLeanEntry → Bool
-- Mathlib.Algebra.GroupWithZero.WithZero
WithZero.div : {α : Type u_1} → [Div α] → Div (WithZero α)
-- Lean.Elab.Term.TermElabM
/-- Try to log errors for unassigned level metavariables `pendingLevelMVarIds`.

Returns `true` if there are any relevant `LevelMVarErrorInfo`s and we should "abort" the declaration.

Remark: we only log unassigned level metavariables as new errors if no error has been logged so far.
 -/
Lean.Elab.Term.logUnassignedLevelMVarsUsingErrorInfos : Array Lean.LMVarId → Lean.Elab.TermElabM Bool
-- Mathlib.LinearAlgebra.Matrix.Notation
Matrix.replicateCol_cons : ∀ {α : Type u} {m : ℕ} {ι : Type u_1} (x : α) (u : Fin m → α),
  Matrix.replicateCol ι (Matrix.vecCons x u) = Matrix.of (Matrix.vecCons (fun x_1 => x) (Matrix.replicateCol ι u))
-- Mathlib.Combinatorics.SimpleGraph.Walk.Maps
_private.Mathlib.Combinatorics.SimpleGraph.Walk.Maps.0.SimpleGraph.Walk.transfer.match_1.eq_1 : ∀ {V : Type u_1} {G : SimpleGraph V} (H : SimpleGraph V)
  (motive : (u v : V) → (p : G.Walk u v) → (∀ e ∈ p.edges, e ∈ H.edgeSet) → Sort u_2) (u : V)
  (h : ∀ e ∈ SimpleGraph.Walk.nil.edges, e ∈ H.edgeSet)
  (h_1 : (u : V) → (h : ∀ e ∈ SimpleGraph.Walk.nil.edges, e ∈ H.edgeSet) → motive u u SimpleGraph.Walk.nil h)
  (h_2 :
    (u w v : V) →
      (h : G.Adj u v) →
        (p : G.Walk v w) →
          (h_2 : ∀ e ∈ (SimpleGraph.Walk.cons' u v w h p).edges, e ∈ H.edgeSet) →
            motive u w (SimpleGraph.Walk.cons h p) h_2),
  (match u, u, SimpleGraph.Walk.nil, h with
    | u, .(u), SimpleGraph.Walk.nil, h => h_1 u h
    | u, w, SimpleGraph.Walk.cons h p, h_3 => h_2 u w v h p h_3) =
    h_1 u h
-- Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
CategoryTheory.ObjectProperty.isVerdierRightLocalizing_op_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (A B : CategoryTheory.ObjectProperty C),
  A.op.IsVerdierRightLocalizing B.op ↔ A.IsVerdierLeftLocalizing B
-- Mathlib.CategoryTheory.Sites.Sheaf
CategoryTheory.Sheaf.hom_ext : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} A] {F G : CategoryTheory.Sheaf J A} {f g : F ⟶ G}, f.hom = g.hom → f = g
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
ModularGroup.SL_to_GL_tower : IsScalarTower (Matrix.SpecialLinearGroup (Fin 2) ℤ) (↥(Matrix.GLPos (Fin 2) ℝ)) UpperHalfPlane
-- Mathlib.Order.WithBotTop
/-- The type obtained by adding both `⊤` and `⊥` to a type.  -/
WithTopBot : Type u_1 → Type u_1
-- Std.Data.HashMap.Lemmas
Std.HashMap.mem_of_mem_union_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α}, k ∈ m₁ ∪ m₂ → k ∉ m₁ → k ∈ m₂
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey!_eq_of_contains : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [LawfulBEq α] [inst : Inhabited α]
  {k : α}, m.contains k = true → m.getKey! k = k
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.ofList_eq_insertMany_empty : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {l : List ((a : α) × β a)},
  Std.DHashMap.Raw.ofList l = ∅.insertMany l
-- Batteries.Data.List.Basic
/-- Auxiliary for `splitAtD`: `splitAtD.go dflt n l acc = (acc.reverse ++ left, right)`
if `splitAtD n l dflt = (left, right)`.  -/
List.splitAtD.go : {α : Type u_1} → α → ℕ → List α → List α → List α × List α
-- Init.Data.Fin.Fold
/-- Folds a monadic function over all the values in `Fin n` from left to right, starting with `0`.

It is the sequence of steps:
```
Fin.foldlM n f x₀ = do
  let x₁ ← f x₀ 0
  let x₂ ← f x₁ 1
  ...
  let xₙ ← f xₙ₋₁ (n-1)
  pure xₙ
```
 -/
Fin.foldlM : {m : Type u_1 → Type u_2} → {α : Type u_1} → [Monad m] → (n : ℕ) → (α → Fin n → m α) → α → m α
-- Mathlib.CategoryTheory.Functor.Category
/-- The left unitor, a natural isomorphism `((𝟭 _) ⋙ F) ≅ F`.
 -/
CategoryTheory.Functor.leftUnitor : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) → (CategoryTheory.Functor.id C).comp F ≅ F
-- Mathlib.Algebra.GCDMonoid.Basic
/-- `0` is left-absorbing.  -/
GCDMonoid.lcm_zero_left : ∀ {α : Type u_2} {inst : CommMonoidWithZero α} [self : GCDMonoid α] (a : α), lcm 0 a = 0
-- Std.Sat.AIG.Basic
Std.Sat.AIG.ArbitraryShiftTarget.mk.sizeOf_spec : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α} {m : ℕ} [inst_2 : SizeOf α] (n : ℕ)
  (target : aig.RefVec m) (distance : aig.RefVec n),
  sizeOf { n := n, target := target, distance := distance } = 1 + sizeOf n + sizeOf target + sizeOf distance
-- Mathlib.LinearAlgebra.Matrix.Transvection
Matrix.mul_transvection_apply_of_ne : ∀ {n : Type u_1} {R : Type u₂} [inst : DecidableEq n] [inst_1 : CommRing R] (i j : n) [inst_2 : Fintype n]
  {m : Type u_4} (a : m) (b : n), b ≠ j → ∀ (c : R) (M : Matrix m n R), (M * Matrix.transvection i j c) a b = M a b
-- Mathlib.Algebra.Lie.IdealOperations
LieSubmodule.bot_lie : ∀ {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] (N : LieSubmodule R L M) [inst_5 : LieAlgebra R L], ⁅⊥, N⁆ = ⊥
-- Mathlib.Analysis.Fourier.Inversion
/-- **Fourier inversion formula**: If a function `f` on a finite-dimensional real inner product
space is continuous, integrable, and its Fourier transform `𝓕 f` is also integrable,
then `𝓕 (𝓕⁻ f) = f`.  -/
Continuous.fourier_fourierInv_eq : ∀ {V : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
  [inst_2 : MeasurableSpace V] [inst_3 : BorelSpace V] [inst_4 : FiniteDimensional ℝ V] [inst_5 : NormedAddCommGroup E]
  [inst_6 : NormedSpace ℂ E] {f : V → E} [CompleteSpace E],
  Continuous f →
    MeasureTheory.Integrable f MeasureTheory.volume →
      MeasureTheory.Integrable (FourierTransform.fourier f) MeasureTheory.volume →
        FourierTransform.fourier (FourierTransformInv.fourierInv f) = f
-- Mathlib.CategoryTheory.FiberedCategory.Grothendieck
/-- The domain of the Cartesian lift of `f`.  -/
CategoryTheory.Pseudofunctor.CoGrothendieck.domainCartesianLift : {𝒮 : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} 𝒮] →
    {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} →
      {R S : 𝒮} → ↑(F.obj { as := Opposite.op S }) → (R ⟶ S) → F.CoGrothendieck
-- Mathlib.Algebra.GCDMonoid.Multiset
Multiset.gcd_add : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] (s₁ s₂ : Multiset α),
  (s₁ + s₂).gcd = gcd s₁.gcd s₂.gcd
-- Mathlib.Data.SProd
/-- The Cartesian product `s ×ˢ t` is the set of `(a, b)` such that `a ∈ s` and `b ∈ t`.  -/
SProd.sprod : {α : Type u} → {β : Type v} → {γ : outParam (Type w)} → [self : SProd α β γ] → α → β → γ
-- Mathlib.AlgebraicGeometry.Scheme
/-- The forgetful functor from `Scheme` to `TopCat`.  -/
AlgebraicGeometry.Scheme.forgetToTop : CategoryTheory.Functor AlgebraicGeometry.Scheme TopCat
-- Mathlib.Topology.UniformSpace.AbstractCompletion
_private.Mathlib.Topology.UniformSpace.AbstractCompletion.0.AbstractCompletion.termHatβ_2 : Lean.ParserDescr
-- Mathlib.Combinatorics.SimpleGraph.Basic
/-- A vertex in a graph is isolated if it's adjacent to no other vertex.  -/
SimpleGraph.IsIsolated : {V : Type u} → SimpleGraph V → V → Prop
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.get.congr_simp : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  (m m_1 : Std.ExtHashMap α β) (e_m : m = m_1) (a a_1 : α) (e_a : a = a_1) (h : a ∈ m), m.get a h = m_1.get a_1 ⋯
-- Lean.Parser.Syntax
Lean.Parser.Syntax.sepBy.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity
/-- Simple graphs on `n` vertices having at least `(turanDensity H + o(1)) * n ^ 2` edges contain
`H`, for sufficiently large `n`.  -/
SimpleGraph.eventually_isContained_of_card_edgeFinset : ∀ {W : Type u_1} (H : SimpleGraph W) {ε : ℝ},
  0 < ε →
    ∀ᶠ (n : ℕ) in Filter.atTop,
      ∀ {G : SimpleGraph (Fin n)} [inst : DecidableRel G.Adj],
        ↑G.edgeFinset.card ≥ (H.turanDensity + ε) * ↑(n.choose 2) → H.IsContained G
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
/-- **Alias** of `ciSup_eq_top_of_top_mem`. -/
ciInf_eq_top_of_top_mem : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : OrderTop α] {f : ι → α},
  ⊤ ∈ Set.range f → iSup f = ⊤
-- Mathlib.Analysis.Normed.Group.Uniform
dist_add_self_right : ∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] (a b : E), dist a (b + a) = ‖b‖
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification
PresheafOfModules.sheafification_map : ∀ {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)
  [inst_1 : CategoryTheory.Presheaf.IsLocallyInjective J α] [inst_2 : CategoryTheory.Presheaf.IsLocallySurjective J α]
  [inst_3 : J.WEqualsLocallyBijective AddCommGrpCat] [inst_4 : CategoryTheory.HasWeakSheafify J AddCommGrpCat]
  {X Y : PresheafOfModules R₀} (f : X ⟶ Y),
  (PresheafOfModules.sheafification α).map f =
    PresheafOfModules.sheafifyMap α (CategoryTheory.toSheafify J X.presheaf) (CategoryTheory.toSheafify J Y.presheaf) f
      ((CategoryTheory.presheafToSheaf J AddCommGrpCat).map ((PresheafOfModules.toPresheaf R₀).map f)) ⋯