mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.LocallySurjective
CategoryTheory.Presheaf.isLocallyInjective_of_isLocallyInjective_of_isLocallySurjective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} A] {FA : A → A → Type u_1} {CA : A → Type w'}
  [inst_2 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] [inst_3 : CategoryTheory.ConcreteCategory A FA]
  {F₁ F₂ F₃ : CategoryTheory.Functor Cᵒᵖ A} (f₁ : F₁ ⟶ F₂) (f₂ : F₂ ⟶ F₃)
  [CategoryTheory.Presheaf.IsLocallyInjective J (CategoryTheory.CategoryStruct.comp f₁ f₂)]
  [CategoryTheory.Presheaf.IsLocallySurjective J f₁], CategoryTheory.Presheaf.IsLocallyInjective J f₂
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
/-- `ProfiniteAddGrp.limitCone` is a limit cone.  -/
ProfiniteAddGrp.limitConeIsLimit : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    (F : CategoryTheory.Functor J ProfiniteAddGrp.{max v u}) →
      CategoryTheory.Limits.IsLimit (ProfiniteAddGrp.limitCone F)
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyData.instEpiP : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.RightHomologyData), CategoryTheory.Epi h.p
-- Std.Do.WP.SimpLemmas
_private.Std.Do.WP.SimpLemmas.0.Std.Do.PredTrans.pushExcept.match_1.eq_1 : ∀ {α ε : Type u_1} (motive : Except ε α → Sort u_2) (a : α) (h_1 : (a : α) → motive (Except.ok a))
  (h_2 : (e : ε) → motive (Except.error e)),
  (match Except.ok a with
    | Except.ok a => h_1 a
    | Except.error e => h_2 e) =
    h_1 a
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.instIsMarkovKernelSectLOfProd : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel (α × β) γ) (b : β) [ProbabilityTheory.IsMarkovKernel κ],
  ProbabilityTheory.IsMarkovKernel (κ.sectL b)
-- Init.Data.List.Lemmas
List.length_pos_iff : ∀ {α : Type u_1} {l : List α}, 0 < l.length ↔ l ≠ []
-- Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp'_inv_whiskerRight_mapComp'₀₂₃_inv_app_assoc : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] [inst_1 : CategoryTheory.Bicategory.Strict B]
  (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁) (f₁₂ : b₁ ⟶ b₂)
  (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃) (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂)
  (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃) (hf : CategoryTheory.CategoryStruct.comp f₀₂ f₂₃ = f)
  (X : ↑(F.obj b₀)) {Z : ↑(F.obj b₃)} (h : (F.map f).toFunctor.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((F.map f₂₃).toFunctor.map ((F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv.toNatTrans.app X))
      (CategoryTheory.CategoryStruct.comp ((F.mapComp' f₀₂ f₂₃ f ⋯).inv.toNatTrans.app X) h) =
    CategoryTheory.CategoryStruct.comp ((F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).inv.toNatTrans.app ((F.map f₀₁).toFunctor.obj X))
      (CategoryTheory.CategoryStruct.comp ((F.mapComp' f₀₁ f₁₃ f ⋯).inv.toNatTrans.app X) h)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.size_le_size_insertMany : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} {ρ : Type w}
  [inst : ForIn Id ρ ((a : α) × β a)] [inst_1 : EquivBEq α] [inst_2 : LawfulHashable α] {l : ρ},
  m.size ≤ (m.insertMany l).size
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Galois
/-- The bijection between the subgroups of `Gal(ℚ(ζₙ)/ℚ)` and the subgroups of the group
of Dirichlet characters of level `n`.
 -/
IsCyclotomicExtension.Rat.subgroupGalEquivSubgroupChar : (n : ℕ) →
  [NeZero n] →
    (K : Type u_1) →
      [inst : Field K] →
        [inst_1 : NumberField K] →
          [hK : IsCyclotomicExtension {n} ℚ K] →
            (R : Type u_2) →
              [inst_2 : CommRing R] →
                [HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)] →
                  Subgroup Gal(K/ℚ) ≃o (Subgroup (DirichletCharacter R n))ᵒᵈ
-- Aesop.Frontend.Tactic
Aesop.Frontend.TacticConfig : Type
-- Mathlib.Data.Finset.MulAntidiagonal
/-- **Alias** of `Finset.mem_antidiagonal`. -/
Finset.mem_addAntidiagonal : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedCancelAddMonoid α] {s t : Set α}
  {hs : s.IsPWO} {ht : t.IsPWO} {a : α} {x : α × α}, x ∈ Finset.antidiagonal hs ht a ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ x.1 + x.2 = a
-- Mathlib.RingTheory.Binomial
/-- The binomial coefficient `choose r n` generalizes the natural number `Nat.choose` function,
interpreted in terms of choosing without replacement.  -/
Ring.choose : {R : Type u_1} → [inst : AddCommGroupWithOne R] → [inst_1 : Pow R ℕ] → [BinomialRing R] → R → ℕ → R
-- Mathlib.CategoryTheory.Sites.Precoverage
CategoryTheory.Precoverage.HasIsos.mem_coverings_of_isIso : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {J : CategoryTheory.Precoverage C} [self : J.HasIsos] {S T : C}
  (f : S ⟶ T) [CategoryTheory.IsIso f], CategoryTheory.Presieve.singleton f ∈ J.coverings T
-- Mathlib.Analysis.Fourier.Notation
FourierTransform.fourier_zero : ∀ {E : Type u_3} {F : Type u_4} [inst : AddCommGroup E] [inst_1 : AddCommGroup F] [inst_2 : FourierTransform E F]
  [FourierAdd E F], FourierTransform.fourier 0 = 0
-- Init.Omega.Constraint
Lean.Omega.instBEqConstraint : BEq Lean.Omega.Constraint
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.comap_inf_map_of_injective : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective σ₁₂] {f : M →ₛₗ[σ₁₂] M₂},
  Function.Injective ⇑f → ∀ (p q : Submodule R M), Submodule.comap f (Submodule.map f p ⊓ Submodule.map f q) = p ⊓ q
-- Lean.Server.Requests
Lean.Language.SnapshotTree.foldSnaps.Control.done.sizeOf_spec : sizeOf Lean.Language.SnapshotTree.foldSnaps.Control.done = 1
-- Mathlib.Topology.Order.IsLUB
/-- The upper bounds of the image of a continuous function on a dense set are equal to the upper
bounds of the range of the universe.  -/
Dense.upperBounds_image : ∀ {γ : Type u_2} {α : Type u_3} [inst : TopologicalSpace α] [inst_1 : Preorder α] [ClosedIicTopology α] {f : γ → α}
  [inst_3 : TopologicalSpace γ] {S : Set γ}, Dense S → Continuous f → upperBounds (f '' S) = upperBounds (Set.range f)
-- Init.Data.Vector.Monadic
Vector.map_toArray_inj : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} {n : ℕ} [inst : Monad m] [LawfulMonad m] {xs ys : m (Vector α n)},
  Vector.toArray <$> xs = Vector.toArray <$> ys ↔ xs = ys
-- Mathlib.Geometry.Manifold.ContMDiff.NormedSpace
/-- Applying a linear map to a vector is smooth. Version in vector spaces. For
versions in nontrivial vector bundles, see `ContMDiffAt.clm_apply_of_inCoordinates` and
`ContMDiffAt.clm_bundle_apply`.  -/
ContMDiffAt.clm_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F₁ : Type u_8} [inst_6 : NormedAddCommGroup F₁]
  [inst_7 : NormedSpace 𝕜 F₁] {F₂ : Type u_9} [inst_8 : NormedAddCommGroup F₂] [inst_9 : NormedSpace 𝕜 F₂]
  {n : WithTop ℕ∞} {g : M → F₁ →L[𝕜] F₂} {f : M → F₁} {x : M},
  ContMDiffAt I (modelWithCornersSelf 𝕜 (F₁ →L[𝕜] F₂)) n g x →
    ContMDiffAt I (modelWithCornersSelf 𝕜 F₁) n f x →
      ContMDiffAt I (modelWithCornersSelf 𝕜 F₂) n (fun x => (g x) (f x)) x
-- Mathlib.Algebra.Algebra.Subalgebra.Operations
instSMulCommClassSubtypeMemSubalgebraSubalgebra : ∀ (A : Type u_1) (B' : Type u_3) [inst : CommSemiring A] [inst_1 : Semiring B'] [inst_2 : Algebra A B'] (G : Type u_4)
  [inst_3 : Monoid G] [inst_4 : MulSemiringAction G B'] [inst_5 : SMulCommClass G A B'],
  SMulCommClass G (↥(FixedPoints.subalgebra A B' G)) B'
-- Lean.Elab.InfoTree.InlayHints
Lean.Elab.InlayHintLabelPart : Type
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.continuousAt_of_dominated : ∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {X : Type u_6} [inst_2 : TopologicalSpace X] [FirstCountableTopology X] {F : X → α → G}
  {x₀ : X} {bound : α → ℝ},
  (∀ᶠ (x : X) in nhds x₀, MeasureTheory.AEStronglyMeasurable (F x) μ) →
    (∀ᶠ (x : X) in nhds x₀, ∀ᵐ (a : α) ∂μ, ‖F x a‖ ≤ bound a) →
      MeasureTheory.Integrable bound μ →
        (∀ᵐ (a : α) ∂μ, ContinuousAt (fun x => F x a) x₀) → ContinuousAt (fun x => ∫ (a : α), F x a ∂μ) x₀
-- Mathlib.Data.Fin.Tuple.Basic
Fin.insertNth_left_injective : ∀ {n : ℕ} {α : Fin (n + 1) → Sort u_1} {p : Fin (n + 1)} (x : (i : Fin n) → α (p.succAbove i)),
  Function.Injective fun x_1 => p.insertNth x_1 x
-- Mathlib.Algebra.Group.Defs
IsAddCommutative.is_comm : ∀ {M : Type u_2} {inst : Add M} [self : IsAddCommutative M], Std.Commutative fun x1 x2 => x1 + x2
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.snd_prodMkRight : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α (β × γ)) (δ : Type u_5) [inst : MeasurableSpace δ],
  (ProbabilityTheory.Kernel.prodMkRight δ κ).snd = ProbabilityTheory.Kernel.prodMkRight δ κ.snd
-- Lean.Widget.TaggedText
Lean.Widget.TaggedText.forM : {m : Type → Type u_1} →
  {α : Type u_2} → [Monad m] → (α → Lean.Widget.TaggedText α → m Unit) → Lean.Widget.TaggedText α → m Unit
-- Mathlib.CategoryTheory.Limits.Indization.Products
CategoryTheory.Limits.isIndObject_pi : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {α : Type v},
  (∀ (g : α → C), CategoryTheory.Limits.IsIndObject (∏ᶜ CategoryTheory.yoneda.obj ∘ g)) →
    ∀ (f : α → CategoryTheory.Functor Cᵒᵖ (Type v)),
      (∀ (a : α), CategoryTheory.Limits.IsIndObject (f a)) → CategoryTheory.Limits.IsIndObject (∏ᶜ f)
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.testAgainstNN_lipschitz_estimate : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [OpensMeasurableSpace Ω]
  (μ : MeasureTheory.FiniteMeasure Ω) (f g : BoundedContinuousFunction Ω NNReal),
  μ.testAgainstNN f ≤ μ.testAgainstNN g + nndist f g * μ.mass
-- Mathlib.Geometry.Convex.Cone.DualFinite
/-- A dually finitely generated cone is dually finitely generated w.r.t. the identity pairing.  -/
PointedCone.DualFG.id : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : AddCommGroup N] [inst_6 : Module R N]
  {p : M →ₗ[R] N →ₗ[R] R} {C : PointedCone R N}, PointedCone.DualFG p C → PointedCone.DualFG LinearMap.id C
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey_alter_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] [Inhabited α] {k : α} {f : Option (β k) → Option (β k)} {hc : k ∈ t.alter k f},
  (t.alter k f).getKey k hc = k
-- Init.Data.SInt.Lemmas
Int32.toNatClampNeg_ofInt_of_le : ∀ {n : ℤ}, -2 ^ 31 ≤ n → n < 2 ^ 31 → (Int32.ofInt n).toNatClampNeg = n.toNat
-- Mathlib.Topology.Homotopy.HomotopyGroup
Homeomorph.sumArrowHomeomorphProdArrow.eq_1 : ∀ {X : Type u_1} [inst : TopologicalSpace X] {ι : Type u_7} {ι' : Type u_8},
  Homeomorph.sumArrowHomeomorphProdArrow =
    { toEquiv := Equiv.sumArrowEquivProdArrow ι ι' X, continuous_toFun := ⋯, continuous_invFun := ⋯ }
-- Mathlib.AlgebraicTopology.SingularSet
instIsRightAdjointSSetTopCatToSSet : TopCat.toSSet.IsRightAdjoint
-- Mathlib.Algebra.Group.Commute.Basic
nsmul_neg_comm : ∀ {G : Type u_1} [inst : AddGroup G] (a : G) (m n : ℕ), m • -a + n • a = n • a + m • -a
-- Mathlib.Topology.UniformSpace.Equicontinuity
/-- A family `𝓕 : ι → X → α` is equicontinuous on `S` iff `range 𝓕` is equicontinuous on `S`,
i.e the family `(↑) : range F → X → α` is equicontinuous on `S`.  -/
equicontinuousOn_iff_range : ∀ {ι : Type u_1} {X : Type u_3} {α : Type u_6} [tX : TopologicalSpace X] [uα : UniformSpace α] {F : ι → X → α}
  {S : Set X}, EquicontinuousOn F S ↔ EquicontinuousOn Subtype.val S
-- Init.Prelude
USize.size_eq : USize.size = 4294967296 ∨ USize.size = 18446744073709551616
-- Mathlib.LinearAlgebra.Dimension.Constructions
rank_finsupp : ∀ (R : Type u) (M : Type v) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [StrongRankCondition R]
  [Module.Free R M] (ι : Type w),
  Module.rank R (ι →₀ M) = Cardinal.lift.{v, w} (Cardinal.mk ι) * Cardinal.lift.{w, v} (Module.rank R M)
-- Init.Data.List.Sublist
List.Sublist.filterMap : ∀ {α : Type u_1} {β : Type u_2} {l₁ l₂ : List α} (f : α → Option β),
  l₁.Sublist l₂ → (List.filterMap f l₁).Sublist (List.filterMap f l₂)
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Measurable.nnreal_tsum : ∀ {α : Type u_1} {mα : MeasurableSpace α} {ι : Type u_5} [Countable ι] {f : ι → α → NNReal},
  (∀ (i : ι), Measurable (f i)) → Measurable fun x => ∑' (i : ι), f i x
-- Mathlib.Order.Filter.Extr
isExtrOn_const : ∀ {α : Type u} {β : Type v} [inst : Preorder β] {s : Set α} {a : α} {b : β}, IsExtrOn (fun x => b) s a
-- Mathlib.Algebra.Notation.Lemmas
dite_neg : ∀ {α : Type u_1} [inst : Zero α] {p : Prop} [inst_1 : Decidable p] {a : p → α} {b : ¬p → α} [inst_2 : LT α],
  (∀ (h : p), a h < 0) → (∀ (h : ¬p), b h < 0) → dite p a b < 0
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.cyclesMap_i_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} [inst_2 : S₁.HasLeftHomology] [inst_3 : S₂.HasLeftHomology] (φ : S₁ ⟶ S₂)
  {Z : C} (h : S₂.X₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.cyclesMap φ)
      (CategoryTheory.CategoryStruct.comp S₂.iCycles h) =
    CategoryTheory.CategoryStruct.comp S₁.iCycles (CategoryTheory.CategoryStruct.comp φ.τ₂ h)
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
Std.DHashMap.Internal.AssocList.contains_eq : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l : Std.DHashMap.Internal.AssocList α β} {a : α},
  Std.DHashMap.Internal.AssocList.contains a l = Std.Internal.List.containsKey a l.toList
-- Mathlib.Topology.Compactness.CountablyCompact
/-- If `f : X → Y` is an embedding, the image `f '' s` of a set `s` is countably compact if and
only if `s` is countably compact.  -/
Topology.IsEmbedding.isCountablyCompact_iff : ∀ {E : Type u_2} {F : Type u_3} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace F] {A : Set E} {f : E → F},
  Topology.IsEmbedding f → (IsCountablyCompact A ↔ IsCountablyCompact (f '' A))
-- Mathlib.Algebra.Module.LinearMap.Polynomial
LinearMap.isNilRegular_def : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup L] [inst_2 : Module R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] (φ : L →ₗ[R] Module.End R M) [inst_5 : Module.Free R M]
  [inst_6 : Module.Finite R M] [inst_7 : Module.Finite R L] [inst_8 : Module.Free R L] (x : L),
  φ.IsNilRegular x ↔ (LinearMap.charpoly (φ x)).coeff φ.nilRank ≠ 0
-- Std.Data.TreeMap.Raw.Basic
/-- Tries to retrieve the largest key that is less than the given key,
panicking if no such key exists.
 -/
Std.TreeMap.Raw.getKeyLT! : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → [Inhabited α] → Std.TreeMap.Raw α β cmp → α → α
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.expMap_single_symm_apply : ∀ {K : Type u_1} [inst : Field K] (w : NumberField.InfinitePlace K) (x : ℝ),
  ↑(NumberField.mixedEmbedding.fundamentalCone.expMap_single w).symm x = ↑w.mult * Real.log x
-- Mathlib.Algebra.Polynomial.Degree.Lemmas
Polynomial.degree_map_eq_iff : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] {f : R →+* S} {p : Polynomial R},
  (Polynomial.map f p).degree = p.degree ↔ f p.leadingCoeff ≠ 0 ∨ p = 0
-- Mathlib.Order.Concept
/-- The `intentClosure` of a set is the smallest intent containing it. See
`IsIntent.upperPolar_lowerPolar_subset` for this proof.  -/
intentClosure : {α : Type u_2} → {β : Type u_3} → (α → β → Prop) → ClosureOperator (Set β)
-- Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone
/-- Auxiliary definition for `ofCocone`.  -/
CategoryTheory.SmallObject.SuccStruct.ofCocone.objIsoPt : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {J : Type u} →
      [inst_1 : LinearOrder J] →
        {j : J} →
          {F : CategoryTheory.Functor (↑(Set.Iio j)) C} →
            (c : CategoryTheory.Limits.Cocone F) → CategoryTheory.SmallObject.SuccStruct.ofCocone.obj c j ≅ c.pt
-- Mathlib.Topology.UniformSpace.ProdApproximation
_private.Mathlib.Topology.UniformSpace.ProdApproximation.0.ContinuousMap.tensorHom.eq_1 : ∀ {X : Type u_5} {Y : Type u_6} {R : Type u_7} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : CommRing R] [inst_3 : TopologicalSpace R] [inst_4 : IsTopologicalRing R],
  ContinuousMap.tensorHom = TensorProduct.lift ContinuousMap.prodMul
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.toReal_inj : ∀ {θ ψ : Real.Angle}, θ.toReal = ψ.toReal ↔ θ = ψ
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.isUnsatDiseq : Int.Internal.Linear.Poly → Bool
-- Mathlib.Algebra.RingQuot
/-- The `intCast` function for `RingQuot`.  -/
RingQuot.intCast : {R : Type uR} → [inst : Ring R] → (r : R → R → Prop) → ℤ → RingQuot r
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.dropPrefix_prop_eq_dropPrefix_decide : ∀ {p : Char → Prop} [inst : DecidablePred p] {s : String.Slice}, s.dropPrefix p = s.dropPrefix fun x => decide (p x)
-- Mathlib.Topology.Algebra.Module.Spaces.WeakDual
instTopologicalSpaceWeakSpace : (𝕜 : Type u_2) →
  (E : Type u_1) →
    [inst : CommSemiring 𝕜] →
      [inst_1 : TopologicalSpace 𝕜] →
        [inst_2 : ContinuousAdd 𝕜] →
          [inst_3 : ContinuousConstSMul 𝕜 𝕜] →
            [inst_4 : AddCommMonoid E] →
              [inst_5 : Module 𝕜 E] → [inst_6 : TopologicalSpace E] → TopologicalSpace (WeakSpace 𝕜 E)
-- Mathlib.Algebra.Group.Units.Basic
AddUnits.eq_neg_add_iff_add_eq : ∀ {α : Type u} [inst : AddMonoid α] (b : AddUnits α) {a c : α}, a = ↑(-b) + c ↔ ↑b + a = c
-- Mathlib.RepresentationTheory.Intertwining
Representation.TensorProduct.comm_comp_rTensor : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [inst : CommSemiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : AddCommMonoid U] [inst_5 : Module A V]
  [inst_6 : Module A W] [inst_7 : Module A U] (ρ : Representation A G V) (σ : Representation A G W)
  (τ : Representation A G U) (f : σ.IntertwiningMap τ),
  (↑(Representation.TensorProduct.comm τ ρ)).comp (Representation.IntertwiningMap.rTensor ρ f) =
    (Representation.IntertwiningMap.lTensor ρ f).comp ↑(Representation.TensorProduct.comm σ ρ)
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanClass.addSubgroup.eq_1 : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M]
  (s : UpperSet (ArchimedeanClass M)),
  ArchimedeanClass.addSubgroup s =
    if hs : s = ⊤ then ⊥
    else
      let __src := ArchimedeanClass.subsemigroup s;
      { toAddSubsemigroup := __src, zero_mem' := ⋯, neg_mem' := ⋯ }
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Products
/-- (Impl) A preliminary definition to avoid timeouts.  -/
CategoryTheory.Over.ConstructProducts.conesEquivInverseObj : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (B : C) →
      {J : Type w} →
        (F : CategoryTheory.Functor (CategoryTheory.Discrete J) (CategoryTheory.Over B)) →
          CategoryTheory.Limits.Cone F →
            CategoryTheory.Limits.Cone (CategoryTheory.Over.ConstructProducts.widePullbackDiagramOfDiagramOver B F)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransformMorphism.whiskerLeft_left : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} {A'' : Type u₇} {B'' : Type u₈}
  {C'' : Type u₉} [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  [inst_6 : CategoryTheory.Category.{v₇, u₇} A''] [inst_7 : CategoryTheory.Category.{v₈, u₈} B'']
  [inst_8 : CategoryTheory.Category.{v₉, u₉} C''] {F'' : CategoryTheory.Functor A'' B''}
  {G'' : CategoryTheory.Functor C'' B''} (φ : CategoryTheory.Limits.CatCospanTransform F G F' G')
  {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F' G' F'' G''} (α : ψ ⟶ ψ'),
  (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerLeft φ α).left = φ.left.whiskerLeft α.left
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.filterMap.eq_1 : ∀ {α β γ : Type w} [inst : Std.Iterator α Id β] (f : β → Option γ) (it : Std.Iter β),
  Std.Iter.filterMap f it = (Std.IterM.filterMap f it.toIterM).toIter
-- Lean.Meta.Sym.ReplaceS
_private.Lean.Meta.Sym.ReplaceS.0.Lean.Meta.Sym.visitChild.match_4.eq_2 : ∀ (motive : Option Lean.Expr → Sort u_1) (x : Option Lean.Expr) (h_1 : (r : Lean.Expr) → motive (some r))
  (h_2 : (x : Option Lean.Expr) → motive x),
  (∀ (r : Lean.Expr), x = some r → False) →
    (match x with
      | some r => h_1 r
      | x => h_2 x) =
      h_2 x
-- Mathlib.LinearAlgebra.FixedSubmodule
LinearEquiv.reduce_mk : ∀ {R : Type u_4} {V : Type u_5} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : Module R V] (W : Submodule R V)
  (u : ↥(MulAction.stabilizer (V ≃ₗ[R] V) W)) (x : V),
  ((LinearEquiv.reduce W) u) (Submodule.Quotient.mk x) = Submodule.Quotient.mk (↑u x)
-- Mathlib.Topology.ContinuousMap.CompactlySupported
/-- `C_c(α, β)` is the type of continuous functions `α → β` with compact support from a topological
space to a topological space with a zero element.

When possible, instead of parametrizing results over `f : C_c(α, β)`,
you should parametrize over `{F : Type*} [CompactlySupportedContinuousMapClass F α β] (f : F)`.

When you extend this structure, make sure to extend `CompactlySupportedContinuousMapClass`.  -/
CompactlySupported.«termC_c(_,_)» : Lean.ParserDescr
-- Mathlib.Algebra.Group.Submonoid.Pointwise
Submonoid.coe_invOrderIso_apply : ∀ {G : Type u_2} [inst : Group G] (a : Submonoid G), ↑(Submonoid.invOrderIso a) = (↑a)⁻¹
-- Mathlib.Analysis.Asymptotics.Defs
/-- **Alias** of the forward direction of `Asymptotics.isLittleO_abs_left`. -/
Asymptotics.IsLittleO.of_abs_left : ∀ {α : Type u_1} {F : Type u_4} [inst : Norm F] {g : α → F} {l : Filter α} {u : α → ℝ},
  (fun x => |u x|) =o[l] g → u =o[l] g
-- Lean.Meta.Tactic.Grind.Proof
_private.Lean.Meta.Tactic.Grind.Proof.0.Lean.Meta.Grind.isCongrDefaultProofTarget.loop : Array Lean.Meta.ParamInfo → Lean.Expr → Lean.Expr → ℕ → Lean.Meta.Grind.GoalM Bool
-- Mathlib.Algebra.Category.AlgCat.Monoidal
/-- Auxiliary definition used to fight a timeout when building
`AlgCat.instMonoidalCategory`.  -/
AlgCat.instMonoidalCategory.tensorHom : {R : Type u} →
  [inst : CommRing R] →
    {W X Y Z : AlgCat R} →
      (W ⟶ X) → (Y ⟶ Z) → (AlgCat.instMonoidalCategory.tensorObj W Y ⟶ AlgCat.instMonoidalCategory.tensorObj X Z)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
/-- For each term `e` of type `α` which implements the `ToInt α i` class,
we store its corresponding `Int` term `eToInt`, a proof `he : toInt e = eToInt`,
and the type `α`.
 -/
Lean.Meta.Grind.Arith.Cutsat.ToIntTermInfo : Type
-- Mathlib.Data.Num.Basic
ZNum.instAdd : Add ZNum
-- Mathlib.Analysis.Analytic.Constructions
Units.ofNearby.eq_1 : ∀ {R : Type u_1} [inst : NormedRing R] [inst_1 : HasSummableGeomSeries R] (x : Rˣ) (y : R) (h : ‖y - ↑x‖ < ‖↑x⁻¹‖⁻¹),
  x.ofNearby y h = (x.add (y - ↑x) h).copy y ⋯ ↑(x.add (y - ↑x) h)⁻¹ ⋯