mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.IsSheafFor
/-- The extension of `f` to `yoneda.obj X` is unique.  -/
CategoryTheory.Presieve.IsSheafFor.unique_extend : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {S : CategoryTheory.Sieve X}
  {P : CategoryTheory.Functor Cᵒᵖ (Type v₁)} (h : CategoryTheory.Presieve.IsSheafFor P S.arrows) {f : S.functor ⟶ P}
  (t : CategoryTheory.yoneda.obj X ⟶ P), CategoryTheory.CategoryStruct.comp S.functorInclusion t = f → t = h.extend f
-- Mathlib.Topology.Continuous
/-- If a function `f` tends to somewhere other than `𝓝 (f x)` at `x`,
then `f` is not continuous at `x`
 -/
not_continuousAt_of_tendsto : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {l₁ : Filter X}
  {l₂ : Filter Y} {x : X},
  Filter.Tendsto f l₁ l₂ → ∀ [l₁.NeBot], l₁ ≤ nhds x → Disjoint (nhds (f x)) l₂ → ¬ContinuousAt f x
-- Mathlib.Topology.Specialization
topToPreord_map : ∀ {X Y : TopCat} (f : X ⟶ Y), topToPreord.map f = Preord.ofHom (Specialization.map (TopCat.Hom.hom f))
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.List.zipWithAll_go_toArray : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (as : List α) (bs : List β) (f : Option α → Option β → γ) (i : ℕ)
  (xs : Array γ),
  Array.zipWithAll.go✝ f as.toArray bs.toArray i xs =
    xs ++ (List.zipWithAll f (List.drop i as) (List.drop i bs)).toArray
-- Init.Data.Array.Lemmas
Array.flatten_eq_flatMap : ∀ {α : Type u_1} {xss : Array (Array α)}, xss.flatten = Array.flatMap id xss
-- Lean.CoreM
Lean.catchInternalIds : {m : Type u_1 → Type u_2} →
  {α : Type u_1} →
    [Monad m] → [MonadExcept Lean.Exception m] → List Lean.InternalExceptionId → m α → (Lean.Exception → m α) → m α
-- Lean.Elab.Tactic.Conv.Basic
Lean.Elab.Tactic.Conv.evalConvTactic : Lean.Elab.Tactic.Tactic
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.copy_apply : ∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) (f : α → β) (hf : ↑e = f) (g : β → α) (hg : ↑e.symm = g)
  (s : Set α) (hs : e.source = s) (t : Set β) (ht : e.target = t), ↑(e.copy f hf g hg s hs t ht) = f
-- Mathlib.Data.Sum.Order
_private.Mathlib.Data.Sum.Order.0.Option.elim.match_1.eq_1 : ∀ {α : Type u_1} {β : Sort u_3} (motive : Option α → β → (α → β) → Sort u_2) (x : α) (x_1 : β) (f : α → β)
  (h_1 : (x : α) → (x_2 : β) → (f : α → β) → motive (some x) x_2 f) (h_2 : (y : β) → (x : α → β) → motive none y x),
  (match some x, x_1, f with
    | some x, x_2, f => h_1 x x_2 f
    | none, y, x => h_2 y x) =
    h_1 x x_1 f
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.starIsoInitial_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  CategoryTheory.WithInitial.starIsoInitial.hom =
    CategoryTheory.WithInitial.starInitial.to (⊥_ CategoryTheory.WithInitial C)
-- Mathlib.MeasureTheory.Measure.Portmanteau
MeasureTheory.tendsto_of_forall_isOpen_le_liminf_nat' : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [inst_2 : OpensMeasurableSpace Ω]
  {μ : MeasureTheory.ProbabilityMeasure Ω} {μs : ℕ → MeasureTheory.ProbabilityMeasure Ω},
  (∀ (G : Set Ω), IsOpen G → ↑μ G ≤ Filter.liminf (fun i => ↑(μs i) G) Filter.atTop) →
    Filter.Tendsto (fun i => μs i) Filter.atTop (nhds μ)
-- Mathlib.Topology.Order.WithTop
TopologicalSpace.instWithTopOfOrderTopology.congr_simp : ∀ {ι : Type u_1} [inst : Preorder ι] [inst_1 : TopologicalSpace ι] [inst_2 : OrderTopology ι],
  TopologicalSpace.instWithTopOfOrderTopology = TopologicalSpace.instWithTopOfOrderTopology
-- Init.Data.Nat.Fold
Nat.dfold_succ : ∀ {n : ℕ} {α : (i : ℕ) → autoParam (i ≤ n + 1) Nat.dfold_succ._auto_3 → Type u}
  (f : (i : ℕ) → (h : i < n + 1) → α i ⋯ → α (i + 1) ⋯) (init : α 0 ⋯),
  (n + 1).dfold f init = f n ⋯ (n.dfold (fun i h => f i ⋯) init)
-- Mathlib.Data.Set.Restrict
Set.domRestrict_eq_iff : ∀ {α : Type u_1} {π : α → Type u_6} {f : (a : α) → π a} {s : Set α} {g : (a : ↑s) → π ↑a},
  s.domRestrict f = g ↔ ∀ (a : α) (ha : a ∈ s), f a = g ⟨a, ha⟩
-- Mathlib.AlgebraicGeometry.Morphisms.FlatRank
AlgebraicGeometry.Scheme.Hom.finrank_pullback_snd : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [AlgebraicGeometry.Flat f] [AlgebraicGeometry.IsFinite f]
  (y : ↥Y),
  AlgebraicGeometry.Scheme.Hom.finrank (CategoryTheory.Limits.pullback.snd f g) y =
    AlgebraicGeometry.Scheme.Hom.finrank f (g y)
-- Mathlib.Data.Nat.Factorization.Defs
Nat.factorization_one : Nat.factorization 1 = 0
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get!_insertMany_list : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : BEq α] [Std.LawfulBEqOrd α] [inst : Inhabited β] (h : t.WF) {l : List (α × β)} {k : α},
  Std.DTreeMap.Internal.Impl.Const.get! (↑(Std.DTreeMap.Internal.Impl.Const.insertMany t l ⋯)) k =
    (List.findSomeRev?
          (fun x =>
            match x with
            | (a, b) => if compare a k = Ordering.eq then some b else none)
          l).getD
      (Std.DTreeMap.Internal.Impl.Const.get! t k)
-- Mathlib.Analysis.Distribution.TemperedDistribution
/-- Coercion of the product of two `Lp` functions to a tempered distribution is equal to the left
multiplication if the left factor is a function of temperate growth.  -/
MeasureTheory.Lp.toTemperedDistribution_smul_eq : ∀ {E : Type u_3} {F : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℂ F] [inst_4 : CompleteSpace F] [inst_5 : MeasurableSpace E] [inst_6 : BorelSpace E]
  {μ : MeasureTheory.Measure E} [hμ : μ.HasTemperateGrowth] {p q r : ENNReal} [inst_7 : p.HolderTriple q r]
  [inst_8 : Fact (1 ≤ q)] [inst_9 : Fact (1 ≤ r)] {g : E → ℂ},
  Function.HasTemperateGrowth g →
    ∀ (hg₂ : MeasureTheory.MemLp g p μ) (f : ↥(MeasureTheory.Lp F q μ)),
      MeasureTheory.Lp.toTemperedDistribution (MeasureTheory.MemLp.toLp g hg₂ • f) =
        (TemperedDistribution.smulLeftCLM F g) (MeasureTheory.Lp.toTemperedDistribution f)
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
ZeroAtInftyContinuousMap.neg_apply : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (x : α) [inst_2 : AddGroup β]
  [inst_3 : IsTopologicalAddGroup β] (f : ZeroAtInftyContinuousMap α β), (-f) x = -f x
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
CategoryTheory.Pretriangulated.instSplitMonoCategory : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C],
  CategoryTheory.SplitMonoCategory C
-- Mathlib.RingTheory.Coalgebra.Hom
CoalgHomClass.mk : ∀ {F : Type u_1} {R : outParam (Type u_2)} {A : outParam (Type u_3)} {B : outParam (Type u_4)} [inst : CommSemiring R]
  [inst_1 : AddCommMonoid A] [inst_2 : Module R A] [inst_3 : AddCommMonoid B] [inst_4 : Module R B]
  [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B] [inst_7 : FunLike F A B]
  [toSemilinearMapClass : SemilinearMapClass F (RingHom.id R) A B],
  (∀ (f : F), CoalgebraStruct.counit ∘ₗ ↑f = CoalgebraStruct.counit) →
    (∀ (f : F), TensorProduct.map ↑f ↑f ∘ₗ CoalgebraStruct.comul = CoalgebraStruct.comul ∘ₗ ↑f) → CoalgHomClass F R A B
-- Mathlib.Topology.UniformSpace.Equiv
UniformEquiv.ext : ∀ {α : Type u} {β : Type u_1} [inst : UniformSpace α] [inst_1 : UniformSpace β] {h h' : α ≃ᵤ β},
  (∀ (x : α), h x = h' x) → h = h'
-- Init.Data.List.Sort.Lemmas
_private.Init.Data.List.Sort.Lemmas.0.List.mergeSort.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → (α → α → Bool) → Sort u_2) (x : α → α → Bool)
  (h_1 : (x : α → α → Bool) → motive [] x) (h_2 : (a : α) → (x : α → α → Bool) → motive [a] x)
  (h_3 : (a b : α) → (xs : List α) → (le : α → α → Bool) → motive (a :: b :: xs) le),
  (match [], x with
    | [], x => h_1 x
    | [a], x => h_2 a x
    | a :: b :: xs, le => h_3 a b xs le) =
    h_1 x
-- Mathlib.Data.Num.Lemmas
Num.add_zero : ∀ (n : Num), n + 0 = n
-- Mathlib.Algebra.Lie.EngelSubalgebra
LieSubalgebra.engel_carrier : ∀ (R : Type u_1) {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (x : L),
  ↑(LieSubalgebra.engel R x) = ⋂ s, ⋂ (_ : ∀ (a : ℕ), ((LieAlgebra.ad R L) x ^ a).ker ≤ s), ↑s
-- Mathlib.Algebra.Ring.Subring.Defs
Subring.zsmul_mem : ∀ {R : Type u} [inst : NonAssocRing R] (s : Subring R) {x : R}, x ∈ s → ∀ (n : ℤ), n • x ∈ s
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.L1.setToL1_zero_left : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_4 : CompleteSpace F] {C : ℝ} (hT : MeasureTheory.DominatedFinMeasAdditive μ 0 C)
  (f : ↥(MeasureTheory.Lp E 1 μ)), (MeasureTheory.L1.setToL1 hT) f = 0
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.Measure.pi.isLocallyFiniteMeasure : ∀ {ι : Type u_1} {α : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → MeasurableSpace (α i)]
  {μ : (i : ι) → MeasureTheory.Measure (α i)} [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)]
  [inst_3 : (i : ι) → TopologicalSpace (α i)] [∀ (i : ι), MeasureTheory.IsLocallyFiniteMeasure (μ i)],
  MeasureTheory.IsLocallyFiniteMeasure (MeasureTheory.Measure.pi μ)
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.return.inj : ∀ {pu : Lean.Compiler.LCNF.Purity} {fvarId fvarId_1 : Lean.FVarId},
  Lean.Compiler.LCNF.Code.return fvarId = Lean.Compiler.LCNF.Code.return fvarId_1 → fvarId = fvarId_1
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.mk_one : ∀ {K : Type u} [inst : CommRing K] [inst_1 : IsDomain K] (x : Polynomial K),
  RatFunc.mk x 1 = (algebraMap (Polynomial K) (RatFunc K)) x
-- Init.Data.List.Sublist
List.suffix_append_of_suffix : ∀ {α : Type u_1} {l₁ l₃ l₂ : List α}, l₁ <:+ l₃ → l₁ <:+ l₂ ++ l₃
-- Mathlib.AlgebraicGeometry.Morphisms.Affine
AlgebraicGeometry.isAffine_of_isAffineHom : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsAffineHom f] [AlgebraicGeometry.IsAffine Y],
  AlgebraicGeometry.IsAffine X
-- Mathlib.LinearAlgebra.Matrix.ToLin
LinearMap.single.eq_1 : ∀ (R : Type u) {ι : Type x} [inst : Semiring R] (φ : ι → Type i) [inst_1 : (i : ι) → AddCommMonoid (φ i)]
  [inst_2 : (i : ι) → Module R (φ i)] [inst_3 : DecidableEq ι] (i : ι),
  LinearMap.single R φ i = { toFun := Pi.single i, map_add' := ⋯, map_smul' := ⋯ }
-- Mathlib.Data.Multiset.Lattice
Multiset.inf.eq_1 : ∀ {α : Type u_1} [inst : SemilatticeInf α] [inst_1 : OrderTop α] (s : Multiset α),
  s.inf = Multiset.fold (fun x1 x2 => x1 ⊓ x2) ⊤ s
-- Mathlib.Analysis.Normed.Ring.Units
/-- The `Ideal.closure` of a maximal ideal in a normed ring with summable
geometric series is the ideal itself.  -/
Ideal.IsMaximal.closure_eq : ∀ {R : Type u_1} [inst : NormedRing R] [HasSummableGeomSeries R] {I : Ideal R}, I.IsMaximal → I.closure = I
-- Mathlib.Order.Bounds.Basic
NoBotOrder.lowerBounds_univ : ∀ {α : Type u_1} [inst : Preorder α] [NoBotOrder α], lowerBounds Set.univ = ∅
-- Mathlib.LinearAlgebra.Ray
exists_pos_left_iff_sameRay : ∀ {R : Type u_1} [inst : Field R] [inst_1 : LinearOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] {x y : M}, x ≠ 0 → y ≠ 0 → ((∃ r, 0 < r ∧ r • x = y) ↔ SameRay R x y)
-- Mathlib.AlgebraicGeometry.Cover.QuasiCompact
AlgebraicGeometry.QuasiCompactCover.instSumScheme_1 : ∀ {S : AlgebraicGeometry.Scheme} {𝒰 : CategoryTheory.PreZeroHypercover S} {𝒱 : CategoryTheory.PreZeroHypercover S}
  [AlgebraicGeometry.QuasiCompactCover 𝒱], AlgebraicGeometry.QuasiCompactCover (𝒰.sum 𝒱)
-- Init.Data.Nat.Basic
Nat.beq_eq : ∀ {x y : ℕ}, (x.beq y = true) = (x = y)
-- Mathlib.Algebra.Group.WithOne.Defs
WithOne.instMonad.eq_1 : WithOne.instMonad =
  { map := @WithOne.instMonad._aux_1, mapConst := @WithOne.instMonad._aux_3, pure := @WithOne.instMonad._aux_5,
    seq := @WithOne.instMonad._aux_7, seqLeft := @WithOne.instMonad._aux_9, seqRight := @WithOne.instMonad._aux_11,
    bind := @WithOne.instMonad._aux_13 }
-- Mathlib.RepresentationTheory.Subrepresentation
Subrepresentation.toSubmodule_inf : ∀ {A : Type u_1} {G : Type u_2} {W : Type u_3} [inst : Semiring A] [inst_1 : Monoid G] [inst_2 : AddCommMonoid W]
  [inst_3 : Module A W] {ρ : Representation A G W} (ρ₁ ρ₂ : Subrepresentation ρ),
  (ρ₁ ⊓ ρ₂).toSubmodule = ρ₁.toSubmodule ⊓ ρ₂.toSubmodule
-- Init.Data.Array.Attach
Array.attachWith.congr_simp : ∀ {α : Type u_1} (xs xs_1 : Array α) (e_xs : xs = xs_1) (P : α → Prop) (H : ∀ x ∈ xs, P x),
  xs.attachWith P H = xs_1.attachWith P ⋯
-- Mathlib.Order.Filter.Pointwise
Filter.coe_pureAddHom : ∀ {α : Type u_2} [inst : Add α], ⇑Filter.pureAddHom = pure
-- Mathlib.Order.GaloisConnection.Basic
/-- Lift the top along a Galois insertion  -/
GaloisInsertion.liftOrderTop : {α : Type u} →
  {β : Type v} →
    {l : α → β} →
      {u : β → α} → [inst : PartialOrder β] → [inst_1 : Preorder α] → [OrderTop α] → GaloisInsertion l u → OrderTop β
-- Mathlib.CategoryTheory.Limits.VanKampen
CategoryTheory.IsVanKampenColimit.of_mapCocone : ∀ {J : Type v'} [inst : CategoryTheory.Category.{u', v'} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {D : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} D] (G : CategoryTheory.Functor C D)
  {F : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone F}
  [∀ (i j : J) (X : C) (f : X ⟶ F.obj j) (g : i ⟶ j),
      CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f (F.map g)) G]
  [∀ (i : J) (X : C) (f : X ⟶ c.pt),
      CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f (c.ι.app i)) G]
  [CategoryTheory.Limits.ReflectsLimitsOfShape CategoryTheory.Limits.WalkingCospan G]
  [CategoryTheory.Limits.PreservesColimitsOfShape J G] [CategoryTheory.Limits.ReflectsColimitsOfShape J G],
  CategoryTheory.IsVanKampenColimit (G.mapCocone c) → CategoryTheory.IsVanKampenColimit c
-- Mathlib.RingTheory.DedekindDomain.Ideal.Basic
FractionalIdeal.not_inv_le_one_of_ne_bot : ∀ {A : Type u_2} {K : Type u_3} [inst : CommRing A] [inst_1 : Field K] [inst_2 : Algebra A K]
  [inst_3 : IsFractionRing A K] [inst_4 : IsDedekindDomain A] {I : Ideal A}, I ≠ ⊥ → I ≠ ⊤ → ¬(↑I)⁻¹ ≤ 1
-- Lean.Server.Completion.CompletionCollectors
Lean.Server.Completion.fieldIdCompletion : Lean.Lsp.DocumentUri →
  Lean.Lsp.Position →
    ℕ →
      Lean.Elab.ContextInfo →
        Lean.LocalContext →
          Option Lean.Name → Lean.Name → Lean.Server.CancellableM (Array Lean.Lsp.ResolvableCompletionItem)
-- Init.Data.UInt.Lemmas
UInt32.le_antisymm : ∀ {a b : UInt32}, a ≤ b → b ≤ a → a = b
-- Mathlib.Data.Sum.Basic
Sum.isSome_getLeft?_iff_isLeft : ∀ {α : Type u} {β : Type v} {x : α ⊕ β}, x.getLeft?.isSome = true ↔ x.isLeft = true
-- Mathlib.Tactic.Linter.FlexibleLinter
/-- The main implementation of the flexible linter.  -/
_private.Mathlib.Tactic.Linter.FlexibleLinter.0.Mathlib.Linter.Flexible.flexibleLinter : Lean.Linter
-- Mathlib.Topology.Category.TopCat.Limits.Products
/-- The constructed binary coproduct cofan in `TopCat` is the coproduct.  -/
TopCat.binaryCofanIsColimit : (X Y : TopCat) → CategoryTheory.Limits.IsColimit (X.binaryCofan Y)
-- Mathlib.Algebra.Order.Antidiag.Prod
/-- The class of (multiplicative) monoids with a mulAntidiagonal.  -/
Finset.HasMulAntidiagonal : (A : Type u_1) → [Monoid A] → Type u_1
-- Lean.Environment
/-- Result of `Lean.Environment.addConstAsync` which is necessary to complete the asynchronous addition.
 -/
Lean.Environment.AddConstAsyncResult : Type
-- Mathlib.Algebra.Module.Submodule.Lattice
Submodule.bot_coe : ∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M], ↑⊥ = {0}
-- Lean.Server.Rpc.Basic
_private.Lean.Server.Rpc.Basic.0.Lean.Server.WithRpcRef.mk' : {α : Type u} → α → USize → Lean.Server.WithRpcRef α
-- Mathlib.CategoryTheory.Localization.Resolution
CategoryTheory.LocalizerMorphism.LeftResolution.hom_ext_iff : ∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂}
  {L L' : Φ.LeftResolution X₂} {φ₁ φ₂ : L ⟶ L'}, φ₁ = φ₂ ↔ φ₁.f = φ₂.f
-- Mathlib.NumberTheory.DirichletCharacter.Basic
DirichletCharacter.primitiveCharacter_isPrimitive : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter R n), χ.primitiveCharacter.IsPrimitive
-- Mathlib.CategoryTheory.Countable
CategoryTheory.CountableCategory.instObjAsType : ∀ (α : Type u) [inst : CategoryTheory.Category.{v, u} α] [inst_1 : CategoryTheory.CountableCategory α],
  CategoryTheory.CountableCategory (CategoryTheory.CountableCategory.ObjAsType α)
-- Mathlib.Analysis.Analytic.Constructions
HasFPowerSeriesWithinOnBall.prod : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} {G : Type u_5}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {e : E} {f : E → F} {g : E → G} {r s : ENNReal} {t : Set E}
  {p : FormalMultilinearSeries 𝕜 E F} {q : FormalMultilinearSeries 𝕜 E G},
  HasFPowerSeriesWithinOnBall f p t e r →
    HasFPowerSeriesWithinOnBall g q t e s → HasFPowerSeriesWithinOnBall (fun x => (f x, g x)) (p.prod q) t e (min r s)
-- Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
SummationFilter.unconditional_filter : ∀ (β : Type u_2), (SummationFilter.unconditional β).filter = Filter.atTop
-- Mathlib.RingTheory.TensorProduct.Maps
/-- Build an algebra equivalence from a linear equivalence out of a tensor product, and evidence
that on pure tensors, it preserves multiplication and the identity.

Note that we state `h_one` using `1 ⊗ₜ[R] 1` instead of `1` so that lemmas about `f` applied to pure
tensors can be directly applied by the caller (without needing `TensorProduct.one_def`).
 -/
Algebra.TensorProduct.algEquivOfLinearEquivTensorProduct : {R : Type uR} →
  {S : Type uS} →
    {A : Type uA} →
      {B : Type uB} →
        {C : Type uC} →
          [inst : CommSemiring R] →
            [inst_1 : CommSemiring S] →
              [inst_2 : Algebra R S] →
                [inst_3 : Semiring A] →
                  [inst_4 : Algebra R A] →
                    [inst_5 : Algebra S A] →
                      [inst_6 : IsScalarTower R S A] →
                        [inst_7 : Semiring B] →
                          [inst_8 : Algebra R B] →
                            [inst_9 : Semiring C] →
                              [inst_10 : Algebra S C] →
                                (f : TensorProduct R A B ≃ₗ[S] C) →
                                  (∀ (a₁ a₂ : A) (b₁ b₂ : B),
                                      f ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) = f (a₁ ⊗ₜ[R] b₁) * f (a₂ ⊗ₜ[R] b₂)) →
                                    f (1 ⊗ₜ[R] 1) = 1 → TensorProduct R A B ≃ₐ[S] C
-- Batteries.Linter.UnnecessarySeqFocus
Batteries.Linter.UnnecessarySeqFocus.Entry.mk.sizeOf_spec : ∀ (stx : Lean.Syntax) (used : Bool), sizeOf { stx := stx, used := used } = 1 + sizeOf stx + sizeOf used
-- Lean.Meta.Basic
/-- Value of `synthPendingDepth` when instance was synthesized or failed to be synthesized.
See issue #2522.
 -/
Lean.Meta.SynthInstanceCacheKey.synthPendingDepth : Lean.Meta.SynthInstanceCacheKey → ℕ
-- Init.Data.SInt.Lemmas
ISize.toNat_toInt : ∀ (x : ISize), x.toInt.toNat = x.toNatClampNeg
-- Init.Data.Nat.MinMax
Nat.max_le : ∀ {a b c : ℕ}, max a b ≤ c ↔ a ≤ c ∧ b ≤ c
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
/-- `Real.sin` as an `OpenPartialHomeomorph` between `(-π / 2, π / 2)` and `(-1, 1)`.  -/
Real.sinPartialHomeomorph : OpenPartialHomeomorph ℝ ℝ
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.HasZeroObject.zeroIsoIsInitial_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {X : C} (t : CategoryTheory.Limits.IsInitial X),
  (CategoryTheory.Limits.HasZeroObject.zeroIsoIsInitial t).hom = 0
-- Mathlib.Algebra.Colimit.DirectLimit
/-- The universal property of the direct limit: maps from the components to another R-algebra
that respect the directed system structure (i.e. make some diagram commute) give rise
to a unique map out of the direct limit.
 -/
DirectLimit.Algebra.lift : {R : Type u_1} →
  {ι : Type u_2} →
    [inst : Preorder ι] →
      (G : ι → Type u_3) →
        {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} →
          (f : (x x_1 : ι) → (h : x ≤ x_1) → T h) →
            [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] →
              [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] →
                [inst_3 : IsDirectedOrder ι] →
                  [inst_4 : CommSemiring R] →
                    [inst_5 : (i : ι) → Semiring (G i)] →
                      [inst_6 : (i : ι) → Algebra R (G i)] →
                        [inst_7 : ∀ (i j : ι) (h : i ≤ j), AlgHomClass (T h) R (G i) (G j)] →
                          [inst_8 : Nonempty ι] →
                            (P : Type u_7) →
                              [inst_9 : Semiring P] →
                                [inst_10 : Algebra R P] →
                                  (g : (i : ι) → G i →ₐ[R] P) →
                                    (∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x) →
                                      DirectLimit G f →ₐ[R] P
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHomRight_hom_inv : ∀ {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] [inst_2 : CategoryTheory.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] (x : D) {y z : C} (f : y ≅ z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight x f.hom)
      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight x f.inv) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj x y)
-- Mathlib.Tactic.Linter.HashCommandLinter
/-- Exactly like `withSetOptionIn`, but recursively discards nested uses of `in`.
Intended to be used in the `hashCommand` linter, where we want to enter `set_option` `in` commands.
 -/
_private.Mathlib.Tactic.Linter.HashCommandLinter.0.Mathlib.Linter.HashCommandLinter.withSetOptionIn' : Lean.Elab.Command.CommandElab → Lean.Elab.Command.CommandElab
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.embedding_comp_inv : ∀ {n : ℕ} (c : Composition n) (j : Fin n), (c.embedding (c.index j)) (c.invEmbedding j) = j
-- Mathlib.CategoryTheory.Monoidal.Ring
CategoryTheory.CommRingObjCat.Hom.mk.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {R₁ R₂ : CategoryTheory.CommRingObjCat C} (hom hom_1 : R₁.X ⟶ R₂.X)
  (e_hom : hom = hom_1) [isRingHom : CategoryTheory.IsRingHom hom],
  { hom := hom, isRingHom := isRingHom } = { hom := hom_1, isRingHom := ⋯ }
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.ext_iff : ∀ {R : Type u} {M : Type v} {x y : TrivSqZeroExt R M}, x = y ↔ x.fst = y.fst ∧ x.snd = y.snd
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.ParentSet.insert : Lean.Meta.Grind.ParentSet → Lean.Expr → Lean.Meta.Grind.ParentSet
-- Lean.Parser.Types
Lean.Parser.ParserCacheEntry.mk.injEq : ∀ (stx : Lean.Syntax) (lhsPrec : ℕ) (newPos : String.Pos.Raw) (errorMsg : Option Lean.Parser.Error)
  (stx_1 : Lean.Syntax) (lhsPrec_1 : ℕ) (newPos_1 : String.Pos.Raw) (errorMsg_1 : Option Lean.Parser.Error),
  ({ stx := stx, lhsPrec := lhsPrec, newPos := newPos, errorMsg := errorMsg } =
      { stx := stx_1, lhsPrec := lhsPrec_1, newPos := newPos_1, errorMsg := errorMsg_1 }) =
    (stx = stx_1 ∧ lhsPrec = lhsPrec_1 ∧ newPos = newPos_1 ∧ errorMsg = errorMsg_1)