mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Discrete
CategoryTheory.Discrete.addMonoidal_associator : ∀ (M : Type u) [inst : AddMonoid M] (x x_1 x_2 : CategoryTheory.Discrete M),
  CategoryTheory.MonoidalCategoryStruct.associator x x_1 x_2 = CategoryTheory.Discrete.eqToIso ⋯
-- Mathlib.Algebra.Ring.ULift
ULift.nonUnitalCommRing : {R : Type u} → [NonUnitalCommRing R] → NonUnitalCommRing (ULift.{u_1, u} R)
-- Mathlib.Algebra.Notation.Indicator
Set.indicator_comp_right : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_3} [inst : Zero M] {s : Set α} (f : β → α) {g : α → M} {x : β},
  (f ⁻¹' s).indicator (g ∘ f) x = s.indicator g (f x)
-- Mathlib.SetTheory.ZFC.Class
Class.mem_univ : ∀ {A : Class.{u}}, A ∈ Class.univ ↔ ∃ x, ↑x = A
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientGroup.quotientKerEquivOfRightInverse_symm_apply : ∀ {G : Type u} [inst : Group G] {H : Type v} [inst_1 : Group H] (φ : G →* H) (ψ : H → G)
  (hφ : Function.RightInverse ψ ⇑φ) (a : H),
  (QuotientGroup.quotientKerEquivOfRightInverse φ ψ hφ).symm a = (QuotientGroup.mk ∘ ψ) a
-- Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov
MeasureTheory.MemLp.meas_ge_lt_top'_enorm : ∀ {α : Type u_1} {ε' : Type u_3} {m0 : MeasurableSpace α} [inst : TopologicalSpace ε'] [inst_1 : ContinuousENorm ε']
  {p : ENNReal} {μ : MeasureTheory.Measure α} {f : α → ε'},
  MeasureTheory.MemLp f p μ →
    p ≠ 0 → p ≠ ⊤ → ∀ {ε : ENNReal}, ε ≠ 0 → (ε = ⊤ → μ {x | ‖f x‖ₑ = ⊤} = 0) → μ {x | ε ≤ ‖f x‖ₑ} < ⊤
-- Lean.Elab.Tactic.Doc
Lean.Elab.Tactic.Doc.allTacticDocs : optParam Bool true → Lean.MetaM (Array Lean.Elab.Tactic.Doc.TacticDoc)
-- Mathlib.RingTheory.Valuation.Basic
Valuation.ne_zero_of_isUnit : ∀ {K : Type u_1} [inst : DivisionRing K] {Γ₀ : Type u_4} [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] [Nontrivial Γ₀]
  (v : Valuation K Γ₀) (x : K), IsUnit x → v x ≠ 0
-- Mathlib.CategoryTheory.Presentable.LocallyPresentable
CategoryTheory.IsCardinalLocallyPresentable.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {κ : Cardinal.{w}} [inst_1 : Fact κ.IsRegular]
  [toHasCardinalFilteredGenerator : CategoryTheory.HasCardinalFilteredGenerator C κ]
  [toHasColimitsOfSize : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v, u} C],
  CategoryTheory.IsCardinalLocallyPresentable C κ
-- Mathlib.Algebra.Module.Submodule.Equiv
LinearEquiv.range_comp : ∀ {R : Type u_1} {R₂ : Type u_3} {R₃ : Type u_4} {M : Type u_5} {M₂ : Type u_7} {M₃ : Type u_8} [inst : Semiring R]
  [inst_1 : Semiring R₂] [inst_2 : Semiring R₃] [inst_3 : AddCommMonoid M] [inst_4 : AddCommMonoid M₂]
  [inst_5 : AddCommMonoid M₃] {module_M : Module R M} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃}
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} [inst_6 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃]
  {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (e : M ≃ₛₗ[σ₁₂] M₂) (h : M₂ →ₛₗ[σ₂₃] M₃)
  [inst_7 : RingHomSurjective σ₂₃] [inst_8 : RingHomSurjective σ₁₃], (h ∘ₛₗ ↑e).range = h.range
-- Mathlib.Lean.Expr.Basic
/-- Given `(hNotEx : Not ex)` where `ex` is of the form `Exists x, p x`,
return a `forall x, Not (p x)` and a proof for it.

This function handles nested existentials.  -/
Lean.Expr.forallNot_of_notExists : Lean.Expr → Lean.Expr → Lean.MetaM (Lean.Expr × Lean.Expr)
-- Mathlib.Algebra.Category.ModuleCat.Localization
/-- `IsLocalizedModule.mapExtendScalars` as a morphism in `ModuleCat`.  -/
ModuleCat.localizedModuleMap : {R : Type u} →
  [inst : CommRing R] →
    [inst_1 : Small.{v, u} R] →
      {M N : ModuleCat R} → (S : Submonoid R) → (M ⟶ N) → (M.localizedModule S ⟶ N.localizedModule S)
-- Mathlib.Order.Monotone.Monovary
MonovaryOn.comp_right : ∀ {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α}
  {g : ι → β} {s : Set ι}, MonovaryOn f g s → ∀ (k : ι' → ι), MonovaryOn (f ∘ k) (g ∘ k) (k ⁻¹' s)
-- Mathlib.ModelTheory.Encoding
_private.Mathlib.ModelTheory.Encoding.0.FirstOrder.Language.BoundedFormula.listDecode.match_1.eq_5 : ∀ {L : FirstOrder.Language} {α : Type u_3}
  (motive : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ) → Sort u_4)
  (l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ))
  (h_1 :
    (n : ℕ) →
      (l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)) →
        motive (Sum.inr (Sum.inr n.succ.succ) :: l))
  (h_2 :
    (n₁ : ℕ) →
      (t₁ : L.Term (α ⊕ Fin n₁)) →
        (n₂ : ℕ) →
          (t₂ : L.Term (α ⊕ Fin n₂)) →
            (l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)) →
              motive (Sum.inl ⟨n₁, t₁⟩ :: Sum.inl ⟨n₂, t₂⟩ :: l))
  (h_3 :
    (n : ℕ) →
      (R : L.Relations n) →
        (k : ℕ) →
          (l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)) →
            motive (Sum.inr (Sum.inl ⟨n, R⟩) :: Sum.inr (Sum.inr k) :: l))
  (h_4 : (l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)) → motive (Sum.inr (Sum.inr 0) :: l))
  (h_5 : (l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)) → motive (Sum.inr (Sum.inr 1) :: l))
  (h_6 : (x : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)) → motive x),
  (match Sum.inr (Sum.inr 1) :: l with
    | Sum.inr (Sum.inr n.succ.succ) :: l => h_1 n l
    | Sum.inl ⟨n₁, t₁⟩ :: Sum.inl ⟨n₂, t₂⟩ :: l => h_2 n₁ t₁ n₂ t₂ l
    | Sum.inr (Sum.inl ⟨n, R⟩) :: Sum.inr (Sum.inr k) :: l => h_3 n R k l
    | Sum.inr (Sum.inr 0) :: l => h_4 l
    | Sum.inr (Sum.inr 1) :: l => h_5 l
    | x => h_6 x) =
    h_5 l
-- Mathlib.Probability.Kernel.Defs
ProbabilityTheory.Kernel.isSFiniteKernel_sum : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [inst : Countable ι]
  {κs : ι → ProbabilityTheory.Kernel α β} [hκs : ∀ (n : ι), ProbabilityTheory.IsSFiniteKernel (κs n)],
  ProbabilityTheory.IsSFiniteKernel (ProbabilityTheory.Kernel.sum κs)
-- Init.GetElem
/-- The syntax `arr[i]` gets the `i`'th element of the collection `arr`. If there
are proof side conditions to the application, they will be automatically
inferred by the `get_elem_tactic` tactic.


Conventions for notations in identifiers:

 * The recommended spelling of `xs[i]` in identifiers is `getElem`.

 * The recommended spelling of `xs[i]'h` in identifiers is `getElem`. -/
GetElem.getElem : {coll : Type u} →
  {idx : Type v} →
    {elem : outParam (Type w)} →
      {valid : outParam (coll → idx → Prop)} →
        [self : GetElem coll idx elem valid] → (xs : coll) → (i : idx) → valid xs i → elem
-- Std.Data.Iterators.Lemmas.Producers.Slice
Std.Slice.Internal.iter_eq_iter : ∀ {γ : Type u} {α β : Type v} [inst : Std.ToIterator (Std.Slice γ) Id α β] {s : Std.Slice γ},
  s.iter = Std.Slice.Internal.iter s
-- Mathlib.Algebra.Algebra.Tower
/-- Any `f : A →ₐ[R] B` is also an `S`-algebra homomorphism if the `R`-algebra structure on
`A` and `B` factors via a surjective ring homomorphism `R →+* S`.  -/
AlgHom.extendScalarsOfSurjective : {R : Type u} →
  {S : Type v} →
    {A : Type w} →
      {B : Type u₁} →
        [inst : CommSemiring R] →
          [inst_1 : CommSemiring S] →
            [inst_2 : Semiring A] →
              [inst_3 : Semiring B] →
                [inst_4 : Algebra R S] →
                  [inst_5 : Algebra S A] →
                    [inst_6 : Algebra S B] →
                      [inst_7 : Algebra R A] →
                        [inst_8 : Algebra R B] →
                          [IsScalarTower R S A] →
                            [IsScalarTower R S B] → Function.Surjective ⇑(algebraMap R S) → (A →ₐ[R] B) ≃ (A →ₐ[S] B)
-- Std.Data.ExtDTreeMap.Basic
/-- Returns the `n`-th smallest key, or `fallback` if `n` is at least `t.size`.  -/
Std.ExtDTreeMap.keyAtIdxD : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtDTreeMap α β cmp → ℕ → α → α
-- Mathlib.RingTheory.AlgebraicIndependent.AlgebraicClosure
Algebra.IsAlgebraic.algebraicIndependent_iff : ∀ {ι : Type u_1} (R : Type u_2) {A : Type u_4} {x : ι → A} (S : Type u_5) [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : CommRing A] [inst_3 : Algebra R S] [inst_4 : Algebra R A] [inst_5 : Algebra S A] [IsScalarTower R S A]
  [NoZeroDivisors S] [FaithfulSMul R S] [Algebra.IsAlgebraic R S], AlgebraicIndependent R x ↔ AlgebraicIndependent S x
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
mem_extChartAt_target : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  {I : ModelWithCorners 𝕜 E H} [inst_5 : ChartedSpace H M] (x : M), ↑(extChartAt I x) x ∈ (extChartAt I x).target
-- Init.Data.SInt.Lemmas
Int8.toISize_ne_minValue : ∀ (a : Int8), a.toISize ≠ ISize.minValue
-- Init.Prelude
instHShiftLeftOfShiftLeft : {α : Type u_1} → [ShiftLeft α] → HShiftLeft α α α
-- Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
HomotopicalAlgebra.FibrantObject.homMk_homMk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithFibrations C]
  [inst_2 : CategoryTheory.Limits.HasTerminal C] {X Y Z : C} [inst_3 : HomotopicalAlgebra.IsFibrant X]
  [inst_4 : HomotopicalAlgebra.IsFibrant Y] [inst_5 : HomotopicalAlgebra.IsFibrant Z] (f : X ⟶ Y) (g : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (HomotopicalAlgebra.FibrantObject.homMk f)
      (HomotopicalAlgebra.FibrantObject.homMk g) =
    HomotopicalAlgebra.FibrantObject.homMk (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.Algebra.Lie.Abelian
LieModule.le_max_triv_iff_bracket_eq_bot : ∀ (R : Type u) (L : Type v) (M : Type w) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  {N : LieSubmodule R L M}, N ≤ LieModule.maxTrivSubmodule R L M ↔ ⁅⊤, N⁆ = ⊥
-- Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
/-- The inclusion `BifibrantObject C ⥤ CofibrantObject C`, as a localizer morphism.  -/
HomotopicalAlgebra.BifibrantObject.ιCofibrantObjectLocalizerMorphism : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : HomotopicalAlgebra.ModelCategory C] →
      CategoryTheory.LocalizerMorphism (HomotopicalAlgebra.weakEquivalences (HomotopicalAlgebra.BifibrantObject C))
        (HomotopicalAlgebra.weakEquivalences (HomotopicalAlgebra.CofibrantObject C))
-- Init.Data.Slice.List.Lemmas
List.toArray_mkSlice_rio : ∀ {α : Type u_1} {xs : List α} {hi : ℕ},
  Std.Slice.toArray (Std.Rio.Sliceable.mkSlice xs *...hi) = (List.take hi xs).toArray
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.hasLimit_leftOp_of_hasColimit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  (F : CategoryTheory.Functor J Cᵒᵖ) [CategoryTheory.Limits.HasColimit F], CategoryTheory.Limits.HasLimit F.leftOp
-- Init.Data.UInt.Lemmas
USize.ofNat_uInt64ToNat : ∀ (n : UInt64), USize.ofNat n.toNat = n.toUSize
-- Mathlib.Order.Lex
Lex.forall : ∀ {α : Type u_1} {p : Lex α → Prop}, (∀ (a : Lex α), p a) ↔ ∀ (a : α), p (toLex a)
-- Mathlib.Order.Filter.Basic
Filter.not_neBot : ∀ {α : Type u} {f : Filter α}, ¬f.NeBot ↔ f = ⊥
-- Std.Data.DHashMap.Raw
Std.DHashMap.Raw.WF.union : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β},
  m₁.WF → m₂.WF → (m₁ ∪ m₂).WF
-- Mathlib.Analysis.Calculus.Implicit
HasStrictFDerivAt.implicitToOpenPartialHomeomorphOfComplemented_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : CompleteSpace E] {F : Type u_3} [inst_4 : NormedAddCommGroup F]
  [inst_5 : NormedSpace 𝕜 F] [inst_6 : CompleteSpace F] {f : E → F} {f' : E →L[𝕜] F} {a : E}
  (hf : HasStrictFDerivAt f f' a) (hf' : (↑f').range = ⊤) (hker : (↑f').ker.ClosedComplemented) (y : E),
  ↑(HasStrictFDerivAt.implicitToOpenPartialHomeomorphOfComplemented f f' hf hf' hker) y =
    (f y, (Classical.choose hker) (y - a))
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.addXYZ_self : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} (P : Fin 3 → R), W'.addXYZ P P = ![0, 0, 0]
-- Mathlib.Order.Filter.Map
Filter.comap_iSup : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_6} {f : ι → Filter β} {m : α → β},
  Filter.comap m (iSup f) = ⨆ i, Filter.comap m (f i)
-- Std.Data.ExtDHashMap.Lemmas
/-- Variant of `getD_map` that holds with `EquivBEq` (i.e. without `LawfulBEq`).  -/
Std.ExtDHashMap.Const.getD_map' : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {γ : Type w} {m : Std.ExtDHashMap α fun x => β}
  [inst : EquivBEq α] [inst_1 : LawfulHashable α] {f : α → β → γ} {k : α} {fallback : γ},
  Std.ExtDHashMap.Const.getD (Std.ExtDHashMap.map f m) k fallback =
    (Option.pmap (fun v h => f (m.getKey k h) v) (Std.ExtDHashMap.Const.get? m k) ⋯).getD fallback
-- Mathlib.Analysis.PSeries
Real.summable_nat_rpow : ∀ {p : ℝ}, (Summable fun n => ↑n ^ p) ↔ p < -1
-- Std.Data.HashSet.Lemmas
Std.HashSet.getD_of_isEmpty : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {a fallback : α},
  m.isEmpty = true → m.getD a fallback = fallback
-- Mathlib.Algebra.Polynomial.Homogenize
Polynomial.coeff_homogenize : ∀ {R : Type u_1} [inst : CommSemiring R] (p : Polynomial R) (n : ℕ) (m : Fin 2 →₀ ℕ),
  MvPolynomial.coeff m (p.homogenize n) = if m 0 + m 1 = n then p.coeff (m 0) else 0
-- Std.Internal.Do.WP.Basic
/-- `Id` is a WPMonad with `Prop` assertions and no exceptions.  -/
Std.Internal.Do.Id.instWPMonad : Std.Internal.Do.WPMonad Id Prop EPost⟨⟩
-- Init.Data.Range.Polymorphic.PRange
Std.Rii.instMembership : {α : Type u} → Membership α (Std.Rii α)
-- Mathlib.Data.List.TFAE
List.tfae_cons_self : ∀ {a : Prop} {l : List Prop}, (a :: a :: l).TFAE ↔ (a :: l).TFAE
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.maxKeyD_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k : α} {v : β} {fallback : α},
      (t.insertIfNew k v).maxKeyD fallback = t.maxKey?.elim k fun k' => if cmp k' k = Ordering.lt then k else k'
-- Mathlib.CategoryTheory.Sums.Associator
CategoryTheory.sum.inrCompInverseAssociator_hom_app : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (E : Type u₃) [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (X : D ⊕ E),
  (CategoryTheory.sum.inrCompInverseAssociator C D E).hom.app X =
    CategoryTheory.CategoryStruct.id
      ((((CategoryTheory.Sum.inr_ C D).comp (CategoryTheory.Sum.inl_ (C ⊕ D) E)).sum'
            (CategoryTheory.Sum.inr_ (C ⊕ D) E)).obj
        X)
-- Mathlib.Topology.DiscreteQuotient
DiscreteQuotient.ofLE_proj : ∀ {X : Type u_2} [inst : TopologicalSpace X] {A B : DiscreteQuotient X} (h : A ≤ B) (x : X),
  DiscreteQuotient.ofLE h (A.proj x) = B.proj x
-- Mathlib.Algebra.Algebra.Hom
/-- `AlgHomClass F R A B` asserts `F` is a type of bundled algebra homomorphisms
from `A` to `B`.  -/
AlgHomClass : (F : Type u_1) →
  (R : outParam (Type u_2)) →
    (A : outParam (Type u_3)) →
      (B : outParam (Type u_4)) →
        [inst : CommSemiring R] →
          [inst_1 : Semiring A] → [inst_2 : Semiring B] → [Algebra R A] → [Algebra R B] → [FunLike F A B] → Prop
-- Mathlib.Topology.Homotopy.Basic
/-- Let `F` be a homotopy between `f₀ : C(X, Y)` and `f₁ : C(X, Y)`. Let `G` be a homotopy between
`g₀ : C(X, Z)` and `g₁ : C(X, Z)`. Then `F.prodMk G` is the homotopy between `f₀.prodMk g₀` and
`f₁.prodMk g₁` that sends `p` to `(F p, G p)`.  -/
ContinuousMap.Homotopy.prodMk : {X : Type u} →
  {Y : Type v} →
    {Z : Type w} →
      [inst : TopologicalSpace X] →
        [inst_1 : TopologicalSpace Y] →
          [inst_2 : TopologicalSpace Z] →
            {f₀ f₁ : C(X, Y)} →
              {g₀ g₁ : C(X, Z)} → f₀.Homotopy f₁ → g₀.Homotopy g₁ → (f₀.prodMk g₀).Homotopy (f₁.prodMk g₁)
-- Mathlib.GroupTheory.Perm.Fin
Fin.cycleIcc.trans : ∀ {n : ℕ} {i j k : Fin n} [NeZero n], i ≤ j → j ≤ k → ⇑(i.cycleIcc j) ∘ ⇑(j.cycleIcc k) = ⇑(i.cycleIcc k)
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed
CategoryTheory.MonoidalCategory.dayConvolutionInternalHomDiagramFunctor_obj_map_app_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  [inst_4 : CategoryTheory.MonoidalClosed V] (F G : CategoryTheory.Functor C V) {c c' : C} (f : c ⟶ c') (X : Cᵒᵖ)
  (c_1 : C),
  ((((CategoryTheory.MonoidalCategory.dayConvolutionInternalHomDiagramFunctor F).obj G).map f).app X).app c_1 =
    (CategoryTheory.ihom (F.obj (Opposite.unop X))).map
      (G.map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft c_1 f))
-- Lean.Meta.Tactic.Grind.Types
/-- Result type for a `grind` Action  -/
Lean.Meta.Grind.ActionResult : Type
-- Init.Data.String.Basic
String.Slice.slice_eq_slice! : ∀ {s : String.Slice} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁}, s.slice p₀ p₁ h = s.slice! p₀ p₁
-- Mathlib.Order.SymmDiff
inf_le_bihimp : ∀ {α : Type u_2} [inst : GeneralizedHeytingAlgebra α] {a b : α}, a ⊓ b ≤ bihimp a b
-- Mathlib.RingTheory.DedekindDomain.Different
Submodule.one_le_traceDual_one : ∀ {A : Type u_1} {K : Type u_2} {L : Type u} {B : Type u_3} [inst : CommRing A] [inst_1 : Field K] [inst_2 : CommRing B]
  [inst_3 : Field L] [inst_4 : Algebra A K] [inst_5 : Algebra B L] [inst_6 : Algebra A B] [inst_7 : Algebra K L]
  [inst_8 : Algebra A L] [inst_9 : IsScalarTower A K L] [inst_10 : IsScalarTower A B L] [IsFractionRing A K]
  [IsIntegrallyClosed A] [FiniteDimensional K L] [IsIntegralClosure B A L], 1 ≤ Submodule.traceDual A K 1
-- Mathlib.SetTheory.Cardinal.Cofinality.Enum
Order.ord_cof_eq_type_lt : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : WellFoundedLT α] [IsRegularCardinalOrder α],
  (Order.cof α).ord = Ordinal.type fun x1 x2 => x1 < x2
-- Mathlib.Combinatorics.SimpleGraph.Diam
SimpleGraph.diam_bot : ∀ {α : Type u_1}, ⊥.diam = 0
-- Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
/-- If `w` is a nontorsion weight function, then the finitely supported function `m : σ →₀ ℕ`
has weighted degree zero if and only if `∀ x : σ, m x = 0`.  -/
MvPolynomial.weightedDegree_eq_zero_iff : ∀ {M : Type u_2} {σ : Type u_3} [inst : AddCommMonoid M] [inst_1 : PartialOrder M] {w : σ → M}
  [CanonicallyOrderedAdd M],
  MvPolynomial.NonTorsionWeight w → ∀ {m : σ →₀ ℕ}, (Finsupp.weight w) m = 0 ↔ ∀ (x : σ), m x = 0
-- Mathlib.Tactic.FunProp.Theorems
Mathlib.Meta.FunProp.instBEqFunctionTheorem : BEq Mathlib.Meta.FunProp.FunctionTheorem
-- Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Asymptotics.superpolynomialDecay_iff_abs_tendsto_zero : ∀ {α : Type u_1} {β : Type u_2} (l : Filter α) (k f : α → β) [inst : TopologicalSpace β] [inst_1 : CommRing β]
  [inst_2 : LinearOrder β] [IsStrictOrderedRing β] [OrderTopology β],
  Asymptotics.SuperpolynomialDecay l k f ↔ ∀ (n : ℕ), Filter.Tendsto (fun a => |k a ^ n * f a|) l (nhds 0)
-- Mathlib.MeasureTheory.Measure.AEMeasurable
aemeasurable_union_iff : ∀ {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] {f : α → β}
  {μ : MeasureTheory.Measure α} {s t : Set α},
  AEMeasurable f (μ.restrict (s ∪ t)) ↔ AEMeasurable f (μ.restrict s) ∧ AEMeasurable f (μ.restrict t)
-- Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
MeasureTheory.rnDeriv_mconv' : ∀ {G : Type u_3} [inst : Group G] {mG : MeasurableSpace G} [MeasurableMul₂ G] [MeasurableInv G]
  {μ : MeasureTheory.Measure G} [μ.IsMulLeftInvariant] [MeasureTheory.SigmaFinite μ] {ν₁ ν₂ : MeasureTheory.Measure G}
  [MeasureTheory.SigmaFinite ν₁] [MeasureTheory.SigmaFinite ν₂],
  ν₁.AbsolutelyContinuous μ →
    ν₂.AbsolutelyContinuous μ →
      (ν₁.mconv ν₂).rnDeriv μ =ᵐ[μ] MeasureTheory.mlconvolution (ν₁.rnDeriv μ) (ν₂.rnDeriv μ) μ
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roc.size.eq_1 : ∀ {α : Type u} [inst : Std.Rxc.HasSize α] [inst_1 : Std.PRange.UpwardEnumerable α] (r : Std.Roc α),
  r.size =
    match Std.PRange.succ? r.lower with
    | none => 0
    | some lower => Std.Rxc.HasSize.size lower r.upper
-- Mathlib.GroupTheory.Perm.List
/-- A list `l : List α` can be interpreted as an `Equiv.Perm α` where each element in the list
is permuted to the next one, defined as `formPerm`. When we have that `Nodup l`,
we prove that `Equiv.Perm.support (formPerm l) = l.toFinset`, and that
`formPerm l` is rotationally invariant, in `formPerm_rotate`.
 -/
List.formPerm : {α : Type u_1} → [DecidableEq α] → List α → Equiv.Perm α
-- Mathlib.CategoryTheory.Functor.Category
CategoryTheory.NatTrans.naturality_app_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {E' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} E']
  {F G : CategoryTheory.Functor C (CategoryTheory.Functor D (CategoryTheory.Functor E E'))} (α : F ⟶ G) {X₁ Y₁ : C}
  (f : X₁ ⟶ Y₁) (X₂ : D) (X₃ : E),
  CategoryTheory.CategoryStruct.comp (((F.map f).app X₂).app X₃) (((α.app Y₁).app X₂).app X₃) =
    CategoryTheory.CategoryStruct.comp (((α.app X₁).app X₂).app X₃) (((G.map f).app X₂).app X₃)
-- Mathlib.Topology.Algebra.Group.Defs
ContinuousWithinAt.inv : ∀ {G : Type u_1} {X : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace G] [inst_2 : Inv G]
  [ContinuousInv G] {f : X → G} {s : Set X} {x : X}, ContinuousWithinAt f s x → ContinuousWithinAt f⁻¹ s x
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.isCompact_basicOpen : ∀ {R : Type u} [inst : CommSemiring R] (f : R), IsCompact ↑(PrimeSpectrum.basicOpen f)
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.omega0_le : ∀ {o : Ordinal.{u_4}}, Ordinal.omega0 ≤ o ↔ ∀ (n : ℕ), ↑n ≤ o
-- Mathlib.Order.PFilter
/-- A specific witness of `pfilter.nonempty` when `P` has a top element.  -/
Order.PFilter.top_mem : ∀ {P : Type u_1} [inst : Preorder P] [inst_1 : OrderTop P] {F : Order.PFilter P}, ⊤ ∈ F
-- Mathlib.Algebra.BigOperators.Finprod
Nat.cast_finsum_mem : ∀ {ι : Type u_3} {s : Set ι},
  s.Finite →
    ∀ {M : Type u_7} [inst : AddCommMonoidWithOne M] (f : ι → ℕ),
      ↑(∑ᶠ (x : ι) (_ : x ∈ s), f x) = ∑ᶠ (x : ι) (_ : x ∈ s), ↑(f x)
-- Lean.Elab.Declaration
/-- Return `true` if `stx` is a `Command.declaration`, and it is a declaration that always has a name.  -/
_private.Lean.Elab.Declaration.0.Lean.Elab.Command.isNamedDecl : Lean.Syntax → Bool
-- Mathlib.Topology.Order.LeftRight
nhdsWithin_Ici_neBot : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : Preorder α] {a b : α}, a ≤ b → (nhdsWithin b (Set.Ici a)).NeBot
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddSubsemigroup.map_sup_comap_of_surjective : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] {f : M →ₙ+ N},
  Function.Surjective ⇑f →
    ∀ (S T : AddSubsemigroup N), AddSubsemigroup.map f (AddSubsemigroup.comap f S ⊔ AddSubsemigroup.comap f T) = S ⊔ T
-- Mathlib.RingTheory.LocalRing.ResidueField.Fiber
/-- The `OrderIso` between the set of primes lying over a prime ideal `p : Ideal R`,
and the prime spectrum of `κ(p) ⊗[R] S`.  -/
PrimeSpectrum.primesOverOrderIsoFiber : (R : Type u_3) →
  (S : Type u_4) →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] → (p : Ideal R) → [inst_3 : p.IsPrime] → ↑(p.primesOver S) ≃o PrimeSpectrum (p.Fiber S)
-- Mathlib.SetTheory.Cardinal.Aleph
Ordinal.omega0_le_preOmega_iff : ∀ {x : Ordinal.{u_1}}, Ordinal.omega0 ≤ Ordinal.preOmega x ↔ Ordinal.omega0 ≤ x
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.tendsto_translationNumber_aux : ∀ (f : CircleDeg1Lift), Filter.Tendsto f.transnumAuxSeq Filter.atTop (nhds f.translationNumber)
-- Mathlib.CategoryTheory.Triangulated.Opposite.Subcategory
CategoryTheory.ObjectProperty.instIsTriangulatedClosed₂OppositeOp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (P : CategoryTheory.ObjectProperty C) [P.IsTriangulatedClosed₂], P.op.IsTriangulatedClosed₂