mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Triangulated.TStructure.Basic
CategoryTheory.Triangulated.TStructure.instIsStableUnderShiftPlusInt : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C), t.plus.IsStableUnderShift ℤ
-- Mathlib.Algebra.CharP.Two
CharTwo.intCast_eq_mod : ∀ {R : Type u_1} [inst : Ring R] [CharP R 2] (n : ℤ), ↑n = ↑(n % 2)
-- Lean.Data.JsonRpc
Lean.JsonRpc.MessageMetaData.responseError.injEq : ∀ (id : Lean.JsonRpc.RequestID) (code : Lean.JsonRpc.ErrorCode) (message : String) (data? : Option Lean.Json)
  (id_1 : Lean.JsonRpc.RequestID) (code_1 : Lean.JsonRpc.ErrorCode) (message_1 : String) (data?_1 : Option Lean.Json),
  (Lean.JsonRpc.MessageMetaData.responseError id code message data? =
      Lean.JsonRpc.MessageMetaData.responseError id_1 code_1 message_1 data?_1) =
    (id = id_1 ∧ code = code_1 ∧ message = message_1 ∧ data? = data?_1)
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.norm_def : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : SeminormedAddCommGroup β]
  (f : BoundedContinuousFunction α β), ‖f‖ = dist f 0
-- Mathlib.LinearAlgebra.TensorProduct.Tower
/-- Heterobasic version of `TensorProduct.lift`:

Constructing a linear map `M ⊗[R] N →[A] P` given a bilinear map `M →[A] N →[R] P` with the
property that its composition with the canonical bilinear map `M →[A] N →[R] M ⊗[R] N` is
the given bilinear map `M →[A] N →[R] P`.  -/
TensorProduct.AlgebraTensorModule.lift : {R : Type uR} →
  {A : Type uA} →
    {M : Type uM} →
      {N : Type uN} →
        {P : Type uP} →
          [inst : CommSemiring R] →
            [inst_1 : Semiring A] →
              [inst_2 : Algebra R A] →
                [inst_3 : AddCommMonoid M] →
                  [inst_4 : Module R M] →
                    [inst_5 : Module A M] →
                      [inst_6 : IsScalarTower R A M] →
                        [inst_7 : AddCommMonoid N] →
                          [inst_8 : Module R N] →
                            [inst_9 : AddCommMonoid P] →
                              [inst_10 : Module R P] →
                                [inst_11 : Module A P] →
                                  [inst_12 : IsScalarTower R A P] → (M →ₗ[A] N →ₗ[R] P) → TensorProduct R M N →ₗ[A] P
-- Init.Data.Array.Attach
Array.filterMap_unattach : ∀ {α : Type u_1} {β : Type u_2} {P : α → Prop} {xs : Array (Subtype P)} {f : α → Option β},
  Array.filterMap f xs.unattach =
    Array.filterMap
      (fun x =>
        match x with
        | ⟨x, h⟩ => binderNameHint x f (binderNameHint h () (f (wfParam x))))
      xs
-- Mathlib.NumberTheory.MulChar.Duality
MulChar.mem_subgroupOrderIsoSubgroupMulChar_iff : ∀ {M : Type u_1} {R : Type u_2} [inst : CommMonoid M] [inst_1 : CommRing R] [inst_2 : Finite M]
  [inst_3 : HasEnoughRootsOfUnity R (Monoid.exponent Mˣ)] {H : Subgroup Mˣ} {χ : MulChar M R},
  χ ∈ OrderDual.ofDual ((MulChar.subgroupOrderIsoSubgroupMulChar M R) H) ↔ ∀ m ∈ H, χ ↑m = 1
-- Mathlib.Topology.UniformSpace.Ascoli
/-- Let `X` be a topological space, `𝔖` a family of compact subsets of `X`,
`α` a uniform space, `F : ι → (X → α)` a family equicontinuous on each `K ∈ 𝔖`, and `ℱ` a filter
on `ι`. Then, `F` tends to `f : X → α` along `ℱ` *uniformly on each `K ∈ 𝔖`* iff it tends to `f`
*pointwise on `⋃₀ 𝔖`* along `ℱ`.  -/
EquicontinuousOn.tendsto_uniformOnFun_iff_pi' : ∀ {ι : Type u_1} {X : Type u_2} {α : Type u_3} [inst : TopologicalSpace X] [inst_1 : UniformSpace α] {F : ι → X → α}
  {𝔖 : Set (Set X)},
  (∀ K ∈ 𝔖, IsCompact K) →
    (∀ K ∈ 𝔖, EquicontinuousOn F K) →
      ∀ (ℱ : Filter ι) (f : X → α),
        Filter.Tendsto (⇑(UniformOnFun.ofFun 𝔖) ∘ F) ℱ (nhds ((UniformOnFun.ofFun 𝔖) f)) ↔
          Filter.Tendsto ((⋃₀ 𝔖).domRestrict ∘ F) ℱ (nhds ((⋃₀ 𝔖).domRestrict f))
-- Mathlib.Algebra.Homology.Embedding.CochainComplex
CochainComplex.isLE_of_le : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : CochainComplex C ℤ) (p q : ℤ), p ≤ q → ∀ [K.IsLE p], K.IsLE q
-- Mathlib.CategoryTheory.Monoidal.Mod
/-- **Alias** of `CategoryTheory.Mod.Hom.mk''`.

---

An alternative constructor for `Hom`,
taking a morphism without a `[IsModHom]` instance, between objects with
a `ModObj` instance (rather than bundled as `Mod`),
as well as the relevant equality to put such an instance.  -/
CategoryTheory.Mod_.Hom.mk'' : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] →
            {A : C} →
              [inst_4 : CategoryTheory.MonObj A] →
                {M N : D} →
                  [inst_5 : CategoryTheory.ModObj A M] →
                    [inst_6 : CategoryTheory.ModObj A N] →
                      (f : M ⟶ N) →
                        autoParam
                            (CategoryTheory.CategoryStruct.comp CategoryTheory.ModObj.smul f =
                              CategoryTheory.CategoryStruct.comp
                                (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight A f)
                                CategoryTheory.ModObj.smul)
                            CategoryTheory.Mod.Hom.mk''._auto_1 →
                          { X := M, mod := inst_5 }.Hom { X := N, mod := inst_6 }
-- Mathlib.LinearAlgebra.Eigenspace.Basic
/-- Generalized eigenspaces for exponents at least `finrank K V` are equal to each other.  -/
Module.End.genEigenspace_eq_genEigenspace_finrank_of_le : ∀ {K : Type v} {V : Type w} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] [FiniteDimensional K V]
  (f : Module.End K V) (μ : K) {k : ℕ},
  Module.finrank K V ≤ k → (f.genEigenspace μ) ↑k = (f.genEigenspace μ) ↑(Module.finrank K V)
-- Init.System.IO
/-- The permissions that all others have to access the file.  -/
IO.FileRight.other : IO.FileRight → IO.AccessRight
-- Std.Internal.Do.WP.Lemmas
Std.Internal.Do.WPMonad.wp_controlAt_apply_eq : ∀ {n : Type u_1 → Type u_2} {m : Type u_1 → Type u_3} {Pred : Type u_4} {EPred : Type u_5} {α : Type u_1}
  {post : α → Pred} {epost : EPred} [inst : Bind n] [Monad m] [Monad n] [inst_3 : Std.Internal.Do.Assertion Pred]
  [inst_4 : Std.Internal.Do.Assertion EPred] [inst_5 : (α : Type u_1) → Std.Internal.Do.WP (n α) α Pred EPred]
  [inst_6 : MonadControlT m n] (f : ({β : Type u_1} → n β → m (stM m n β)) → m (stM m n α)),
  Std.Internal.Do.wp (controlAt m f) post epost = Std.Internal.Do.wp (liftWith f >>= restoreM) post epost
-- Mathlib.Data.DFinsupp.BigOperators
DFinsupp.liftAddHom_apply : ∀ {ι : Type u} {γ : Type w} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → AddZeroClass (β i)]
  [inst_2 : AddCommMonoid γ] (φ : (i : ι) → β i →+ γ), DFinsupp.liftAddHom φ = DFinsupp.sumAddHom φ
-- Mathlib.CategoryTheory.GlueData
/-- The diagram of the image of a `GlueData` under a functor `F` is naturally isomorphic to the
original diagram of the `GlueData` via `F`.
 -/
CategoryTheory.GlueData.diagramIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v, u₁} C] →
    {C' : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v, u₂} C'] →
        (D : CategoryTheory.GlueData C) →
          (F : CategoryTheory.Functor C C') →
            [inst_2 :
                ∀ (i j k : D.J),
                  CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (D.f i j) (D.f i k)) F] →
              D.diagram.multispan.comp F ≅ (D.mapGlueData F).diagram.multispan
-- Mathlib.CategoryTheory.Join.Basic
CategoryTheory.Join.inclRightFaithful : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D],
  (CategoryTheory.Join.inclRight C D).Faithful
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
RootPairing.GeckConstruction.cartanSubalgebra.congr_simp : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N}
  [inst_5 : P.IsCrystallographic] (b : P.Base) [inst_6 : Fintype ι] [inst_7 : DecidableEq ι],
  RootPairing.GeckConstruction.cartanSubalgebra b = RootPairing.GeckConstruction.cartanSubalgebra b
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
MonoidAlgebra.map_neg : ∀ {R : Type u_3} {S : Type u_4} {M : Type u_6} [inst : Ring R] [inst_1 : Ring S] (f : R →+ S) (x : MonoidAlgebra R M),
  MonoidAlgebra.map f (-x) = -MonoidAlgebra.map f x
-- Mathlib.Order.Defs.PartialOrder
Preorder.mk : {α : Type u_2} →
  [toLE : LE α] →
    [toLT : LT α] →
      (∀ (a : α), a ≤ a) →
        (∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c) →
          autoParam (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) Preorder.lt_iff_le_not_ge._autoParam → Preorder α
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.map_add : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : Add β] [inst_2 : Add γ] {g : β → γ},
  (∀ (x y : β), g (x + y) = g x + g y) →
    ∀ (f₁ f₂ : MeasureTheory.SimpleFunc α β),
      MeasureTheory.SimpleFunc.map g (f₁ + f₂) = MeasureTheory.SimpleFunc.map g f₁ + MeasureTheory.SimpleFunc.map g f₂
-- Init.Data.String.Length
/-- Returns the length of a string in Unicode code points.

Examples:
* `"".length = 0`
* `"abc".length = 3`
* `"L∃∀N".length = 4`
 -/
String.length : String → ℕ
-- Mathlib.Algebra.FreeMonoid.Count
/-- `List.count` as a bundled additive monoid homomorphism.  -/
FreeAddMonoid.count : {α : Type u_1} → [DecidableEq α] → α → FreeAddMonoid α →+ ℕ
-- Mathlib.MeasureTheory.Group.MeasurableEquiv
MeasureTheory.Measure.instSMulCommClassNNRealDomMulAct : ∀ {G : Type u_1} {A : Type u_2} [inst : Group G] [inst_1 : MulAction G A] [inst_2 : MeasurableSpace A]
  [inst_3 : MeasurableConstSMul G A], SMulCommClass NNReal Gᵈᵐᵃ (MeasureTheory.Measure A)
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
/-- Extensionality lemma for morphisms from a module of the form `(M₁ ⊗ M₂) ⊗ M₃`.  -/
ModuleCat.MonoidalCategory.tensor_ext₃' : ∀ {R : Type u} [inst : CommRing R] {M₁ M₂ M₃ M₄ : ModuleCat R}
  {f g :
    CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj M₁ M₂) M₃ ⟶ M₄},
  (∀ (m₁ : ↑M₁) (m₂ : ↑M₂) (m₃ : ↑M₃),
      (CategoryTheory.ConcreteCategory.hom f) (m₁ ⊗ₜ[R] m₂ ⊗ₜ[R] m₃) =
        (CategoryTheory.ConcreteCategory.hom g) (m₁ ⊗ₜ[R] m₂ ⊗ₜ[R] m₃)) →
    f = g
-- Mathlib.Order.SuccPred.CompleteLinearOrder
exists_eq_ciSup_of_not_isSuccLimit : ∀ {ι : Sort u_1} {α : Type u_2} [inst : ConditionallyCompleteLinearOrder α] [Nonempty ι] {f : ι → α},
  BddAbove (Set.range f) → ¬Order.IsSuccLimit (⨆ i, f i) → ∃ i, f i = ⨆ i, f i
-- Mathlib.Probability.Moments.Variance
ProbabilityTheory.evariance_ne_top : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.MemLp X 2 μ → ProbabilityTheory.evariance X μ ≠ ⊤
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
IsUniformAddGroup.isRightUniformAddGroup : ∀ (α : Type u_1) [inst : UniformSpace α] [inst_1 : AddGroup α] [IsUniformAddGroup α], IsRightUniformAddGroup α
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
addRightReflectLT_of_addRightMono : ∀ (N : Type u_2) [inst : Add N] [inst_1 : LinearOrder N] [AddRightMono N], AddRightReflectLT N
-- Lean.Expr
Lean.mkIntLit : ℤ → Lean.Expr
-- Mathlib.Analysis.CStarAlgebra.Module.Constructions
_private.Mathlib.Analysis.CStarAlgebra.Module.Constructions.0.WithCStarModule.isBounded_pi_iff_aux : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] {ι : Type u_2} {E : ι → Type u_3}
  [inst_2 : Fintype ι] [inst_3 : (i : ι) → NormedAddCommGroup (E i)] [inst_4 : (i : ι) → Module ℂ (E i)]
  [inst_5 : (i : ι) → SMul A (E i)] [inst_6 : (i : ι) → CStarModule A (E i)] [inst_7 : StarOrderedRing A]
  (s : Set (WithCStarModule A ((i : ι) → E i))), Bornology.IsBounded s ↔ Bornology.IsBounded s
-- Lean.Elab.Tactic.Grind.Basic
_private.Lean.Elab.Tactic.Grind.Basic.0.Lean.Elab.Tactic.Grind.evalGrindTactic.expandEval : Lean.Syntax →
  Lean.Elab.Tactic.Grind.SavedState →
    List (Lean.KeyedDeclsAttribute.AttributeEntry Lean.Macro) →
      List (Lean.KeyedDeclsAttribute.AttributeEntry Lean.Elab.Tactic.Grind.GrindTactic) →
        Array Lean.Elab.Tactic.Grind.EvalTacticFailure → Lean.Elab.Tactic.Grind.GrindTacticM Unit
-- Mathlib.CategoryTheory.Limits.Sifted
/-- If `C` is sifted, the `colimit` functor `(C ⥤ Type) ⥤ Type` preserves terminal objects  -/
CategoryTheory.IsSifted.colim_preservesTerminal_of_isSifted : ∀ {C : Type u} [inst : CategoryTheory.SmallCategory C] [CategoryTheory.IsSifted C],
  CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty (CategoryTheory.Functor C (Type u)))
    CategoryTheory.Limits.colim
-- Aesop.Forward.State
Aesop.PatSubstSource.target.sizeOf_spec : sizeOf Aesop.PatSubstSource.target = 1
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax
CategoryTheory.Lax.LaxTrans.LaxFunctor.bicategory_leftUnitor_hom_as_app : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C]
  {x x_1 : CategoryTheory.LaxFunctor B C} (η : x ⟶ x_1) (a : B),
  (CategoryTheory.Bicategory.leftUnitor η).hom.as.app a = (CategoryTheory.Bicategory.leftUnitor (η.app a)).hom
-- Mathlib.Analysis.Calculus.FDeriv.Equiv
fderivWithin_continuousLinearEquiv_comp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {G' : Type u_5} [inst_7 : NormedAddCommGroup G']
  [inst_8 : NormedSpace 𝕜 G'] {x : E} {s : Set E} (L : G ≃L[𝕜] G') (f : E → F →L[𝕜] G),
  UniqueDiffWithinAt 𝕜 s x →
    fderivWithin 𝕜 (fun x => ↑L ∘SL f x) s x = ↑((ContinuousLinearEquiv.refl 𝕜 F).arrowCongr L) ∘SL fderivWithin 𝕜 f s x
-- Mathlib.Algebra.Order.Interval.Basic
NonemptyInterval.pure_one : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : One α], NonemptyInterval.pure 1 = 1
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.ringEquivOfRingEquiv_symm_eq : ∀ {R : Type u_5} {S : Type u_6} (K : Type u_7) (L : Type u_8) [inst : CommRing R] [inst_1 : IsDomain R]
  [inst_2 : CommRing S] [inst_3 : IsDomain S] [inst_4 : CommRing K] [inst_5 : CommRing L] [inst_6 : Algebra R K]
  [inst_7 : Algebra S L] [inst_8 : IsFractionRing R K] [inst_9 : IsFractionRing S L] (f : R ≃+* S),
  (FractionalIdeal.ringEquivOfRingEquiv K L f).symm = FractionalIdeal.ringEquivOfRingEquiv L K f.symm
-- Mathlib.Topology.Compactness.CountablyCompact
Subtype.isCountablyCompact_iff : ∀ {E : Type u_2} [inst : TopologicalSpace E] {p : E → Prop} {A : Set { x // p x }},
  IsCountablyCompact A ↔ IsCountablyCompact (Subtype.val '' A)
-- Mathlib.LinearAlgebra.FreeModule.PID
Ideal.smithCoeffs_ne_zero : ∀ {ι : Type u_1} {R : Type u_2} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsPrincipalIdealRing R]
  {S : Type u_4} [inst_3 : CommRing S] [inst_4 : IsDomain S] [inst_5 : Algebra R S] [inst_6 : Finite ι]
  (b : Module.Basis ι R S) (I : Ideal S) (hI : I ≠ ⊥) (i : ι), Ideal.smithCoeffs b I hI i ≠ 0
-- Mathlib.MeasureTheory.MeasurableSpace.Basic
measurable_zero : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] [inst_2 : Zero α], Measurable 0
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.homologyMapIso_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} {K L : HomologicalComplex C c} (iso : K ≅ L) (i : ι) [inst_2 : K.HasHomology i]
  [inst_3 : L.HasHomology i], (HomologicalComplex.homologyMapIso iso i).inv = HomologicalComplex.homologyMap iso.inv i
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.splitAtPred_eq : ∀ {α : Type u_1} (p : α → Bool) (L l₁ : List α) (o : Option α) (l₂ : List α),
  (∀ x ∈ l₁, p x = false) →
    Option.elim' (L = l₁ ∧ l₂ = []) (fun a => p a = true ∧ L = l₁ ++ a :: l₂) o →
      Turing.PartrecToTM2.splitAtPred p L = (l₁, o, l₂)
-- Init.Data.Vector.Attach
/-- `O(1)`. "Attach" the proof that the elements of `xs` are in `xs` to produce a new vector
with the same elements but in the type `{x // x ∈ xs}`.  -/
Vector.attach : {α : Type u_1} → {n : ℕ} → (xs : Vector α n) → Vector { x // x ∈ xs } n
-- Mathlib.Algebra.Homology.HomotopyCategory.KInjective
/-- A choice of homotopy to zero for a morphism from an acyclic
cochain complex to a K-injective cochain complex.  -/
CochainComplex.IsKInjective.homotopyZero : {C : Type u_2} →
  [inst : CategoryTheory.Category.{u_3, u_2} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {K L : CochainComplex C ℤ} → (f : K ⟶ L) → HomologicalComplex.Acyclic K → [L.IsKInjective] → Homotopy f 0
-- Mathlib.MeasureTheory.Group.Defs
/-- A measure `μ : Measure α` is invariant under an additive action of `M` on `α` if for any
measurable set `s : Set α` and `c : M`, the measure of its preimage under `fun x => c +ᵥ x` is equal
to the measure of `s`.  -/
MeasureTheory.VAddInvariantMeasure : (M : Type u_1) → (α : Type u_2) → [VAdd M α] → {x : MeasurableSpace α} → MeasureTheory.Measure α → Prop
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
ContDiffAt.arctan : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {x : E} {n : ℕ∞},
  ContDiffAt ℝ (↑n) f x → ContDiffAt ℝ (↑n) (fun x => Real.arctan (f x)) x
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.coproductIsoSelf.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Limits.FormalCoproduct C),
  X.coproductIsoSelf = CategoryTheory.Limits.FormalCoproduct.coproductIsoCofanPt X.I X.toFun ≪≫ X.cofanPtIsoSelf
-- Mathlib.Algebra.Homology.Embedding.TruncLEHomology
HomologicalComplex.instEpiGShortComplexTruncLE : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Abelian C] (K : HomologicalComplex C c')
  (e : c.Embedding c') [inst_2 : e.IsTruncLE], CategoryTheory.Epi (K.shortComplexTruncLE e).g
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
AlgebraicGeometry.LocallyRingedSpace.GlueData.ι_isoSheafedSpace_inv_assoc : ∀ (D : AlgebraicGeometry.LocallyRingedSpace.GlueData) (i : D.J) {Z : AlgebraicGeometry.SheafedSpace CommRingCat}
  (h : D.glued.toSheafedSpace ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((D.mapGlueData AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace).ι i)
      (CategoryTheory.CategoryStruct.comp D.isoSheafedSpace.inv h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.LocallyRingedSpace.Hom.toShHom (D.ι i)) h
-- Init.Data.UInt.Lemmas
UInt32.toUInt16_ofNatTruncate_of_lt : ∀ {n : ℕ}, n < UInt32.size → (UInt32.ofNatClamp n).toUInt16 = UInt16.ofNat n
-- Mathlib.Probability.ProductMeasure
/-- Let `μ : (i : Ioc a c) → Measure (X i)` be a family of measures. Up to an equivalence,
`(⨂ i : Ioc a b, μ i) ⊗ (⨂ i : Ioc b c, μ i) = ⨂ i : Ioc a c, μ i`, where `⊗` denotes the
product of measures.  -/
MeasureTheory.Measure.pi_prod_map_IocProdIoc : ∀ {X : ℕ → Type u_1} {mX : (n : ℕ) → MeasurableSpace (X n)} (μ : (n : ℕ) → MeasureTheory.Measure (X n))
  [hμ : ∀ (n : ℕ), MeasureTheory.IsProbabilityMeasure (μ n)] {a b c : ℕ},
  a ≤ b →
    b ≤ c →
      MeasureTheory.Measure.map (IocProdIoc a b c)
          ((MeasureTheory.Measure.pi fun i => μ ↑i).prod (MeasureTheory.Measure.pi fun i => μ ↑i)) =
        MeasureTheory.Measure.pi fun i => μ ↑i
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
_private.Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat.0.SSet.map_map_of_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (V : CategoryTheory.Functor Cᵒᵖ (Type w)) {X Y Z : C}
  {α : X ⟶ Y} {β : Y ⟶ Z} {γ : X ⟶ Z} {φ : (fun X => X) (V.obj (Opposite.op Z))},
  CategoryTheory.CategoryStruct.comp α β = γ →
    (CategoryTheory.ConcreteCategory.hom (V.map α.op)) ((CategoryTheory.ConcreteCategory.hom (V.map β.op)) φ) =
      (CategoryTheory.ConcreteCategory.hom (V.map γ.op)) φ
-- Mathlib.Algebra.Group.End
AddAut.instInhabited : (M : Type u_2) → [inst : Add M] → Inhabited (AddAut M)
-- Mathlib.SetTheory.ZFC.Class
/-- The intersection of a class is the class of all members of ZFC sets in the class .
Uses `⋂₀` notation, scoped under the `Class` namespace.  -/
Class.«term⋂₀_» : Lean.ParserDescr
-- Mathlib.GroupTheory.QuotientGroup.Defs
Subgroup.orderIsoCon_apply : ∀ {G : Type u_1} [inst : Group G] (N : { N // N.Normal }), Subgroup.orderIsoCon N = QuotientGroup.con ↑N
-- Lean.Elab.Tactic.Grind.Annotated
/-- Extension to track modules that have been marked as "grind-annotated".
These modules contain theorems that have been manually reviewed/annotated for grind,
so they should be excluded from premise selection when the caller is "grind".
 -/
_private.Lean.Elab.Tactic.Grind.Annotated.0.Lean.Elab.Tactic.Grind.grindAnnotatedExt : Lean.SimplePersistentEnvExtension Lean.Name Lean.NameSet
-- Mathlib.AlgebraicGeometry.StructureSheaf
AlgebraicGeometry.structureSheafInType.add_apply : ∀ {R M : Type u} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)}
  (s t : (AlgebraicGeometry.structureSheafInType R M).obj.obj (Opposite.op U)) (x : ↥U), ↑(s + t) x = ↑s x + ↑t x
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.M.children_mk : ∀ {F : PFunctor.{uA, uB}} {a : F.A} (x : F.B a → F.M) (i : F.B (PFunctor.M.mk ⟨a, x⟩).head),
  (PFunctor.M.mk ⟨a, x⟩).children i = x (cast ⋯ i)
-- Init.Data.ToString.Name
_private.Init.Data.ToString.Name.0.Lean.Name.toStringWithSep.maybeEscape : Bool → String → Bool → String
-- Mathlib.Order.Hom.CompleteLattice
FrameHomClass.toBoundedLatticeHomClass : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : CompleteLattice α]
  [inst_2 : CompleteLattice β] [FrameHomClass F α β], BoundedLatticeHomClass F α β
-- Mathlib.GroupTheory.DivisibleHull
DivisibleHull.mk_zero : ∀ {M : Type u_1} [inst : AddCommMonoid M] (s : ℕ+), DivisibleHull.mk 0 s = 0
-- Mathlib.Data.Set.Lattice
Set.iInter_option : ∀ {α : Type u_1} {ι : Type u_12} (s : Option ι → Set α), ⋂ o, s o = s none ∩ ⋂ i, s (some i)
-- Mathlib.Logic.Relation
Relation.ReflTransGen.head_induction_on : ∀ {α : Type u_1} {r : α → α → Prop} {b : α} {motive : (a : α) → Relation.ReflTransGen r a b → Prop} {a : α}
  (h : Relation.ReflTransGen r a b),
  motive b ⋯ → (∀ {a c : α} (h' : r a c) (h : Relation.ReflTransGen r c b), motive c h → motive a ⋯) → motive a h
-- Mathlib.Algebra.Polynomial.Expand
Polynomial.rootMultiplicity_expand : ∀ {R : Type u} [inst : CommRing R] {p : ℕ} [ExpChar R p] {f : Polynomial R} {r : R},
  Polynomial.rootMultiplicity r ((Polynomial.expand R p) f) = p * Polynomial.rootMultiplicity (r ^ p) f
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
List.stronglyMeasurable_sum : ∀ {α : Type u_1} {M : Type u_5} [inst : AddMonoid M] [inst_1 : TopologicalSpace M] [ContinuousAdd M]
  {m : MeasurableSpace α} (l : List (α → M)),
  (∀ f ∈ l, MeasureTheory.StronglyMeasurable f) → MeasureTheory.StronglyMeasurable l.sum