mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.category_comp_τ₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : CategoryTheory.Square C} (f : X.Hom Y) (g : Y.Hom Z),
  (CategoryTheory.CategoryStruct.comp f g).τ₁ = CategoryTheory.CategoryStruct.comp f.τ₁ g.τ₁
-- Mathlib.Analysis.Meromorphic.FactorizedRational
_private.Mathlib.Analysis.Meromorphic.FactorizedRational.0.Function.FactorizedRational.mulSupport_update : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {d : 𝕜 → ℤ} {x : 𝕜} (h : (Function.support d).Finite),
  (Function.mulSupport fun u => (x - u) ^ Function.update d x 0 u) ⊆ ↑h.toFinset
-- Aesop.RuleTac.Descr
Aesop.RuleTacDescr.tacGen : Lean.Name → Aesop.RuleTacDescr
-- Mathlib.CategoryTheory.HomCongr
CategoryTheory.Functor.map_homCongr : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} D]
  (F : CategoryTheory.Functor C D) {X Y X₁ Y₁ : C} (α : X ≅ X₁) (β : Y ≅ Y₁) (f : X ⟶ Y),
  F.map ((α.homCongr β) f) = ((F.mapIso α).homCongr (F.mapIso β)) (F.map f)
-- Std.Time.DateTime
/-- Returns the weekday.
 -/
Std.Time.DateTime.weekday : Std.Time.DateTime → Std.Time.Weekday
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
continuousFunctionalCalculus_map_id : ∀ {A : Type u_1} [inst : CStarAlgebra A] (a : A) [inst_1 : IsStarNormal a],
  (continuousFunctionalCalculus a) (ContinuousMap.restrict (spectrum ℂ a) (ContinuousMap.id ℂ)) = ⟨a, ⋯⟩
-- Lean.Meta.Tactic.Cases
Lean.Meta.Cases.Context.majorDecl : Lean.Meta.Cases.Context → Lean.LocalDecl
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.GrpObj.mulRight.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {A : C} [inst_2 : CategoryTheory.GrpObj A] (f : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ A),
  CategoryTheory.GrpObj.mulRight f =
    {
      hom :=
        CategoryTheory.CategoryStruct.comp
          (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.id A)
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit A) f))
          CategoryTheory.MonObj.mul,
      inv :=
        CategoryTheory.CategoryStruct.comp
          (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.id A)
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit A)
              (CategoryTheory.CategoryStruct.comp f CategoryTheory.GrpObj.inv)))
          CategoryTheory.MonObj.mul,
      hom_inv_id := ⋯, inv_hom_id := ⋯ }
-- Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
SimplexCategory.σ₀Iter_coe_eq_of_le : ∀ (i : ℕ) {n m : ℕ} (j : Fin (m + 1)) (hi : autoParam (n + i = m) SimplexCategory.σ₀Iter_coe_eq_of_le._auto_1),
  autoParam (↑j ≤ i) SimplexCategory.σ₀Iter_coe_eq_of_le._auto_3 →
    ↑((CategoryTheory.ConcreteCategory.hom (SimplexCategory.σ₀Iter i hi)) j) = 0
-- Mathlib.Data.Multiset.Powerset
Multiset.powersetCardAux_cons : ∀ {α : Type u_1} (n : ℕ) (a : α) (l : List α),
  Multiset.powersetCardAux (n + 1) (a :: l) =
    Multiset.powersetCardAux (n + 1) l ++ List.map (Multiset.cons a) (Multiset.powersetCardAux n l)
-- Mathlib.RingTheory.Perfection
Perfection.coeffMonoidHom_mapMonoidHom : ∀ (p : ℕ) {M : Type u_2} {N : Type u_3} [inst : CommMonoid M] [inst_1 : CommMonoid N] (φ : M →* N) (f : Perfection M p)
  (n : ℕ), (Perfection.coeffMonoidHom N p n) ((Perfection.mapMonoidHom p φ) f) = φ ((Perfection.coeffMonoidHom M p n) f)
-- Mathlib.Data.Fin.Tuple.Basic
Fin.snoc_apply_zero : ∀ {n : ℕ} {α : Fin (n + 1) → Sort u_1} (x : α (Fin.last n)) (p : (i : Fin n) → α i.castSucc) [inst : NeZero n],
  Fin.snoc p x 0 = p 0
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
AlgebraicGeometry.Scheme.RationalMap.IsOver.exists_partialMap_over : ∀ {X Y S : AlgebraicGeometry.Scheme} {inst : X.Over S} {inst_1 : Y.Over S} {f : X.RationalMap Y}
  [self : AlgebraicGeometry.Scheme.RationalMap.IsOver S f],
  ∃ g, AlgebraicGeometry.Scheme.PartialMap.IsOver S g ∧ g.toRationalMap = f
-- Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Equiv.Perm.exists_mem_stabilizer_isThreeCycle : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (s : Set α),
  4 < Nat.card α → ∃ g ∈ MulAction.stabilizer (Equiv.Perm α) s, g.IsThreeCycle
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.inv_mul_cancel : ∀ {R : Type u} {M : Type v} [inst : DivisionSemiring R] [inst_1 : AddCommGroup M] [inst_2 : Module Rᵐᵒᵖ M]
  [inst_3 : Module R M] {x : TrivSqZeroExt R M}, x.fst ≠ 0 → x⁻¹ * x = 1
-- Mathlib.Data.Set.Basic
Set.mem_or_mem_of_mem_union : ∀ {α : Type u} {x : α} {a b : Set α}, x ∈ a ∪ b → x ∈ a ∨ x ∈ b
-- Mathlib.ModelTheory.Order
FirstOrder.Language.linearOrderTheory.eq_1 : ∀ (L : FirstOrder.Language) [inst : L.IsOrdered],
  L.linearOrderTheory = insert FirstOrder.Language.leSymb.total L.partialOrderTheory
-- Mathlib.SetTheory.Lists
Lists.mem.decidable : {α : Type u_1} → [DecidableEq α] → (a : Lists α) → (l : Lists' α true) → Decidable (a ∈ l)
-- Mathlib.Geometry.Manifold.Immersion
/-- If `f: M → N` and `g: M' × N'` are immersions at `x` and `x'`, respectively,
then `f × g: M × N → M' × N'` is an immersion at `(x, x')`.  -/
Manifold.IsImmersion.prodMap : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {E' : Type u_3} {E''' : Type u_4} {E'' : Type u}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E']
  [inst_4 : NormedSpace 𝕜 E'] [inst_5 : NormedAddCommGroup E''] [inst_6 : NormedSpace 𝕜 E'']
  [inst_7 : NormedAddCommGroup E'''] [inst_8 : NormedSpace 𝕜 E'''] {H : Type u_7} [inst_9 : TopologicalSpace H]
  {H' : Type u_8} [inst_10 : TopologicalSpace H'] {G : Type u_9} [inst_11 : TopologicalSpace G] {G' : Type u_10}
  [inst_12 : TopologicalSpace G'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'}
  {J : ModelWithCorners 𝕜 E'' G} {J' : ModelWithCorners 𝕜 E''' G'} {M : Type u_11} [inst_13 : TopologicalSpace M]
  [inst_14 : ChartedSpace H M] {M' : Type u_12} [inst_15 : TopologicalSpace M'] [inst_16 : ChartedSpace H' M']
  {N : Type u_13} [inst_17 : TopologicalSpace N] [inst_18 : ChartedSpace G N] {N' : Type u_14}
  [inst_19 : TopologicalSpace N'] [inst_20 : ChartedSpace G' N'] {n : WithTop ℕ∞} {f : M → N} {g : M' → N'}
  [IsManifold I n M] [IsManifold I' n M'] [IsManifold J n N] [IsManifold J' n N'],
  Manifold.IsImmersion I J n f →
    Manifold.IsImmersion I' J' n g → Manifold.IsImmersion (I.prod I') (J.prod J') n (Prod.map f g)
-- Qq.Simp
/-- For `pre` procedures, the resulting expression is passed to `pre` again.

For `post` procedures, the resulting expression is passed to `pre` again IF
`Simp.Config.singlePass := false` and resulting expression is not equal to initial expression.
 -/
Lean.Meta.Simp.StepQ.visit : {u : Lean.Level} → {α : Q(Sort u)} → {e : Q(«$α»)} → Lean.Meta.Simp.ResultQ e → Lean.Meta.Simp.StepQ e
-- Init.Data.Nat.Fold
_private.Init.Data.Nat.Fold.0.Nat.fold.match_1.splitter : {α : Type u_2} →
  (motive : (x : ℕ) → ((i : ℕ) → i < x → α → α) → α → Sort u_1) →
    (x : ℕ) →
      (x_1 : (i : ℕ) → i < x → α → α) →
        (x_2 : α) →
          ((f : (i : ℕ) → i < 0 → α → α) → (a : α) → motive 0 f a) →
            ((n : ℕ) → (f : (i : ℕ) → i < n.succ → α → α) → (a : α) → motive n.succ f a) → motive x x_1 x_2
-- Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries
PowerSeries.WithPiTopology.pentagonalSeries_eq_tsum : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : TopologicalSpace R] [T2Space R],
  PowerSeries.pentagonalSeries R = ∑' (k : ℤ), ↑↑k.negOnePow * PowerSeries.X ^ pentagonal k
-- Std.Time.Zoned.ZoneRules
/-- Represents a type of local time, including offset and daylight saving information.
 -/
Std.Time.TimeZone.LocalTimeType : Type
-- Init.GrindInstances.Ring.Fin
Nat.sub_sub_right : ∀ (a : ℕ) {b c : ℕ}, c ≤ b → a - (b - c) = a + c - b
-- Mathlib.Algebra.Group.UniqueProds.Basic
UniqueMul.iff_card_le_one : ∀ {G : Type u_1} [inst : Mul G] {A B : Finset G} {a0 b0 : G} [inst_1 : DecidableEq G],
  a0 ∈ A → b0 ∈ B → (UniqueMul A B a0 b0 ↔ {p ∈ A ×ˢ B | p.1 * p.2 = a0 * b0}.card ≤ 1)
-- Mathlib.CategoryTheory.Sites.CoverLifting
CategoryTheory.Functor.IsCocontinuous.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {G : CategoryTheory.Functor C D}
  {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D},
  (∀ {U : C} {S : CategoryTheory.Sieve (G.obj U)}, S ∈ K (G.obj U) → CategoryTheory.Sieve.functorPullback G S ∈ J U) →
    G.IsCocontinuous J K
-- Mathlib.Order.UpperLower.CompleteLattice
LowerSet.ext : ∀ {α : Type u_1} [inst : LE α] {s t : LowerSet α}, ↑s = ↑t → s = t
-- Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
RootPairing.polarizationEquiv_symm_apply_coroot : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Fintype ι] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : Field R] [inst_4 : Module R M] [inst_5 : Module R N] (P : RootPairing ι R M N)
  [inst_6 : P.IsAnisotropic] [inst_7 : P.IsRootSystem] {i : ι},
  P.PolarizationEquiv.symm (P.coroot i) = (2 / (P.RootForm (P.root i)) (P.root i)) • P.root i
-- Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
/-- If `A` is a triangulated subcategory of a pretriangulated category `C`,
and `B : ObjectProperty C`, this is the inclusion functor
`A.ι : A.FullSubcategory ⥤ C`, considered as a localizer morphism,
where `C` is equipped with the property of morphisms `B.trW`
and `A.FullSubcategory` with the property of morphisms `(B.inverseImage A.ι).trW`.  -/
CategoryTheory.ObjectProperty.triangulatedLocalizerMorphism : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (A B : CategoryTheory.ObjectProperty 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] →
              [inst_5 : CategoryTheory.Pretriangulated C] →
                [inst_6 : A.IsTriangulated] → CategoryTheory.LocalizerMorphism (B.inverseImage A.ι).trW B.trW
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.allM_map : ∀ {α β β' : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m β] [Std.Iterators.Finite α m] [inst_2 : Monad m]
  [inst_3 : Std.IteratorLoop α m m] [LawfulMonad m] [Std.LawfulIteratorLoop α m m] {it : Std.IterM m β} {f : β → β'}
  {p : β' → m (ULift.{w, 0} Bool)}, Std.IterM.allM p (Std.IterM.map f it) = Std.IterM.allM (fun x => p (f x)) it
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.one_eq_mk : ∀ {α : Type u}, 1 = FreeGroup.mk []
-- Mathlib.Algebra.Algebra.Operations
Submodule.smul_one_eq_span : ∀ {R : Type u} [inst : CommSemiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Algebra R A] (x : A), x • 1 = R ∙ x
-- Lean.Elab.Match
Lean.Elab.Term.Discr : Type
-- Mathlib.Algebra.Group.Submonoid.Basic
AddMonoidHom.coe_ofClosureMEqTopLeft : ∀ {M : Type u_1} {N : Type u_2} [inst : AddMonoid M] [inst_1 : AddMonoid N] {s : Set M} (f : M → N)
  (hs : AddSubmonoid.closure s = ⊤) (h1 : f 0 = 0) (hadd : ∀ x ∈ s, ∀ (y : M), f (x + y) = f x + f y),
  ⇑(AddMonoidHom.ofClosureMEqTopLeft f hs h1 hadd) = f
-- Mathlib.Probability.Moments.Basic
ProbabilityTheory.mgf_congr_of_identDistrib : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} (X : Ω → ℝ) {Ω' : Type u_3}
  {m' : MeasurableSpace Ω'} {μ' : MeasureTheory.Measure Ω'} (X' : Ω' → ℝ),
  ProbabilityTheory.IdentDistrib X X' μ μ' → ∀ (t : ℝ), ProbabilityTheory.mgf X μ t = ProbabilityTheory.mgf X' μ' t
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKey?_eq_some_iff_mem_and_forall : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] {km : α}, t.minKey? = some km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp km k).isLE = true
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
/-- If `f : 𝕜 → 𝕜` is continuous on a compact set `s` and `f 0 = 0` and `a : X → A` is continuous
at `x₀` within a set `t : Set X`, and eventually `a x` satisfies the predicate `p` associated to `𝕜`
and has quasispectrum contained in `s`, then `fun x ↦ cfcₙ f (a x)` is continuous at `x₀`
within `t`.  -/
ContinuousWithinAt.cfcₙ : ∀ {X : Type u_1} {𝕜 : Type u_2} {A : Type u_3} {p : A → Prop} [inst : RCLike 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : StarRing A] [inst_3 : NormedSpace 𝕜 A] [inst_4 : IsScalarTower 𝕜 A A] [inst_5 : SMulCommClass 𝕜 A A]
  [ContinuousStar A] [inst_7 : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p] [inst_8 : TopologicalSpace X]
  {s : Set 𝕜},
  IsCompact s →
    ∀ (f : 𝕜 → 𝕜) {a : X → A} {x₀ : X} {t : Set X},
      x₀ ∈ t →
        ContinuousWithinAt a t x₀ →
          (∀ᶠ (x : X) in nhdsWithin x₀ t, quasispectrum 𝕜 (a x) ⊆ s) →
            (∀ᶠ (x : X) in nhdsWithin x₀ t, p (a x)) →
              autoParam (ContinuousOn f s) ContinuousWithinAt.cfcₙ._auto_1 →
                autoParam (f 0 = 0) ContinuousWithinAt.cfcₙ._auto_3 → ContinuousWithinAt (fun x => cfcₙ f (a x)) t x₀
-- Mathlib.RingTheory.Congruence.Basic
RingCon.mkₐ_surjective : ∀ {α : Type u_1} {R : Type u_3} [inst : CommSemiring α] [inst_1 : Semiring R] [inst_2 : Algebra α R] (c : RingCon R),
  Function.Surjective ⇑(RingCon.mkₐ α c)
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.Bicone.mk.injEq : ∀ {J : Type w} {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} (pt : C) (π : (j : J) → pt ⟶ F j)
  (ι : (j : J) → F j ⟶ pt)
  (ι_π :
    autoParam
      (∀ (j j' : J),
        CategoryTheory.CategoryStruct.comp (ι j) (π j') = if h : j = j' then CategoryTheory.eqToHom ⋯ else 0)
      CategoryTheory.Limits.Bicone.ι_π._autoParam)
  (pt_1 : C) (π_1 : (j : J) → pt_1 ⟶ F j) (ι_1 : (j : J) → F j ⟶ pt_1)
  (ι_π_1 :
    autoParam
      (∀ (j j' : J),
        CategoryTheory.CategoryStruct.comp (ι_1 j) (π_1 j') = if h : j = j' then CategoryTheory.eqToHom ⋯ else 0)
      CategoryTheory.Limits.Bicone.ι_π._autoParam),
  ({ pt := pt, π := π, ι := ι, ι_π := ι_π } = { pt := pt_1, π := π_1, ι := ι_1, ι_π := ι_π_1 }) =
    (pt = pt_1 ∧ π ≍ π_1 ∧ ι ≍ ι_1)
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
/-- An isomorphism of short complexes `S₁ ≅ S₂` induces an isomorphism on the `H` fields
of left homology data of `S₁` and `S₂`.  -/
CategoryTheory.ShortComplex.leftHomologyMapIso' : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        (S₁ ≅ S₂) → (h₁ : S₁.LeftHomologyData) → (h₂ : S₂.LeftHomologyData) → h₁.H ≅ h₂.H
-- Mathlib.Algebra.Algebra.Unitization
Unitization.snd_zero : ∀ {R : Type u_3} {A : Type u_4} [inst : Zero R] [inst_1 : Zero A], (Unitization.toProd 0).2 = 0
-- Init.Data.UInt.Lemmas
USize.toBitVec_toUInt16 : ∀ (n : USize), n.toUInt16.toBitVec = BitVec.setWidth 16 n.toBitVec
-- Batteries.Data.Fin.Coding
_private.Batteries.Data.Fin.Coding.0.Fin.encodeSubtype.match_3.eq_1 : ∀ (motive : (n : ℕ) → (P : Fin n → Prop) → DecidablePred P → { i // P i } → Sort u_1) (n : ℕ) (P : Fin (n + 1) → Prop)
  (inst : DecidablePred P) (hp : P 0)
  (h_1 : (n : ℕ) → (P : Fin (n + 1) → Prop) → (inst : DecidablePred P) → (hp : P 0) → motive n.succ P inst ⟨⟨0, ⋯⟩, hp⟩)
  (h_2 :
    (n : ℕ) →
      (P : Fin (n + 1) → Prop) →
        (inst : DecidablePred P) →
          (i : ℕ) → (hi : i + 1 < n + 1) → (hp : P ⟨i + 1, hi⟩) → motive n.succ P inst ⟨⟨i.succ, hi⟩, hp⟩),
  (match n.succ, P, inst, ⟨⟨0, ⋯⟩, hp⟩ with
    | n.succ, P, inst, ⟨⟨0, ⋯⟩, hp⟩ => h_1 n P inst hp
    | n.succ, P, inst, ⟨⟨i.succ, hi⟩, hp⟩ => h_2 n P inst i hi hp) =
    h_1 n P inst hp
-- Mathlib.AlgebraicGeometry.Properties
AlgebraicGeometry.IsReduced.iff_of_openCover : ∀ (X : AlgebraicGeometry.Scheme) (𝒰 : X.OpenCover),
  AlgebraicGeometry.IsReduced X ↔ ∀ (i : 𝒰.I₀), AlgebraicGeometry.IsReduced (𝒰.X i)
-- Mathlib.CategoryTheory.Monoidal.ExternalProduct.Basic
/-- When both diagrams have the same source category, composing the external product with
the diagonal gives the pointwise functor tensor product.
Note that `(externalProductCompDiagIso _ _).app (F₁, F₂) : Functor.diag J₁ ⋙ F₁ ⊠ F₂ ≅ F₁ ⊗ F₂`
type checks.  -/
CategoryTheory.MonoidalCategory.externalProductCompDiagIso : (J₁ : Type u₁) →
  (C : Type u₃) →
    [inst : CategoryTheory.Category.{v₁, u₁} J₁] →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          (CategoryTheory.MonoidalCategory.externalProductBifunctor J₁ J₁ C).comp
              ((CategoryTheory.Functor.whiskeringLeft J₁ (J₁ × J₁) C).obj (CategoryTheory.Functor.diag J₁)) ≅
            CategoryTheory.MonoidalCategory.tensor (CategoryTheory.Functor J₁ C)
-- Mathlib.Data.ENNReal.Basic
ENNReal.coe_le_coe : ∀ {r q : NNReal}, ↑r ≤ ↑q ↔ r ≤ q
-- Mathlib.Topology.UniformSpace.Basic
entourageProd_mem_uniformity : ∀ {α : Type ua} {β : Type ub} [t₁ : UniformSpace α] [t₂ : UniformSpace β] {u : SetRel α α} {v : SetRel β β},
  u ∈ uniformity α → v ∈ uniformity β → entourageProd u v ∈ uniformity (α × β)
-- Mathlib.Topology.UniformSpace.Equiv
UniformEquiv.refl_apply : ∀ (α : Type u_4) [inst : UniformSpace α], ⇑(UniformEquiv.refl α) = id
-- Mathlib.Data.QPF.Univariate.Basic
/-- corecursor for type defined by `Cofix`  -/
QPF.Cofix.corec : {F : Type u → Type u} → [q : QPF F] → {α : Type u} → (α → F α) → α → QPF.Cofix F
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.coe_ofNat : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} [inst : CommRing R] {n : ℕ} [inst_1 : n.AtLeastTwo], ↑(OfNat.ofNat n) = OfNat.ofNat n
-- Lean.Elab.Tactic.Induction
/-- Applies `induction .. with $preTac | ..`, if any, to an alternative goal.  -/
_private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.ElimApp.evalAlts.applyPreTac : Lean.Syntax → Lean.MVarId → Lean.Elab.Tactic.TacticM (Option (List Lean.MVarId))
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
/-- A morphism `k : A ⟶ S.X₂` such that `k ≫ S.g = 0` lifts to a morphism `A ⟶ S.cycles`.  -/
CategoryTheory.ShortComplex.liftCycles : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (S : CategoryTheory.ShortComplex C) →
        {A : C} →
          (k : A ⟶ S.X₂) → CategoryTheory.CategoryStruct.comp k S.g = 0 → [inst_2 : S.HasLeftHomology] → A ⟶ S.cycles
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoMod_sub' : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α), toIcoMod hp (a - p) b = toIcoMod hp a b - p
-- Mathlib.Analysis.Calculus.Deriv.Mul
HasDerivAt.finsetProd : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {ι : Type u_2} [inst_1 : DecidableEq ι] {𝔸' : Type u_3}
  [inst_2 : NormedCommRing 𝔸'] [inst_3 : NormedAlgebra 𝕜 𝔸'] {u : Finset ι} {f : ι → 𝕜 → 𝔸'} {f' : ι → 𝔸'},
  (∀ i ∈ u, HasDerivAt (f i) (f' i) x) → HasDerivAt (∏ i ∈ u, f i) (∑ i ∈ u, (∏ j ∈ u.erase i, f j x) • f' i) x
-- Init.Data.String.Basic
String.lt_iff : ∀ {s t : String}, s < t ↔ s.toList < t.toList
-- Mathlib.Geometry.Diffeology.Basic
DiffeologicalSpace.generateFrom_union_toPlots : ∀ {X : Type u_1} (d₁ d₂ : DiffeologicalSpace X), DiffeologicalSpace.generateFrom (d₁.toPlots ∪ d₂.toPlots) = d₁ ⊔ d₂
-- Mathlib.Algebra.Order.Group.Opposite
AddOpposite.one_le_unop : ∀ {α : Type u_1} [inst : CommMonoid α] [inst_1 : PartialOrder α] {a : αᵃᵒᵖ}, 1 ≤ AddOpposite.unop a ↔ 1 ≤ a
-- Mathlib.AlgebraicGeometry.Morphisms.FiniteType
AlgebraicGeometry.LocallyOfFiniteType.stalkMap : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.LocallyOfFiniteType f] (x : ↥X),
  (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.stalkMap f x)).EssFiniteType
-- Mathlib.NumberTheory.PowModTotient
Nat.pow_totient_mod_eq_one : ∀ {x n : ℕ}, 1 < n → x.Coprime n → x ^ n.totient % n = 1
-- Lean.Parser.Command
Lean.Parser.Command.version.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.RingTheory.TensorProduct.MonoidAlgebra
AddMonoidAlgebra.rTensorEquiv_tmulAlgEquiv : ∀ {R : Type u_1} {M : Type u_2} {S : Type u_4} {A : Type u_5} {B : Type u_6} [inst : CommSemiring R]
  [inst_1 : CommSemiring S] [inst_2 : CommSemiring A] [inst_3 : CommSemiring B] [inst_4 : Algebra R S]
  [inst_5 : Algebra R A] [inst_6 : Algebra R B] [inst_7 : Algebra S A] [inst_8 : IsScalarTower R S A]
  [inst_9 : AddCommMonoid M] (a : A) (p : AddMonoidAlgebra B M),
  (AddMonoidAlgebra.rTensorEquivAlgEquiv R S A B) (a ⊗ₜ[R] p) =
    a • (AddMonoidAlgebra.mapAlgHom M Algebra.TensorProduct.includeRight) p
-- Mathlib.RepresentationTheory.Coinduced
Rep.resCoindToHom_hom_apply_coe : ∀ {k : Type u} {G : Type v} {H : Type w} [inst : CommRing k] [inst_1 : Monoid G] [inst_2 : Monoid H] (φ : G →* H)
  (B : Rep.{max w u_1, u, w} k H) (A : Rep.{max w u_1, u, v} k G) (f : Rep.res φ B ⟶ A) (c : ↑B) (i : H),
  ↑((Rep.Hom.hom (Rep.resCoindToHom φ B A f)) c) i = (Rep.Hom.hom f) ((B.ρ i) c)
-- Mathlib.GroupTheory.SpecificGroups.Alternating
alternatingGroup.mem_range_ofSubtype_iff : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (s : Finset α) (k : ↥(alternatingGroup α)),
  k ∈ (alternatingGroup.ofSubtype s).range ↔ (↑k).support ⊆ s
-- Mathlib.CategoryTheory.Subobject.Basic
/-- To show that two subobjects are equal, it suffices to exhibit an isomorphism commuting with
the arrows.  -/
CategoryTheory.Subobject.eq_mk_of_comm : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {B A : C} {X : CategoryTheory.Subobject B} (f : A ⟶ B)
  [inst_1 : CategoryTheory.Mono f] (i : CategoryTheory.Subobject.underlying.obj X ≅ A),
  CategoryTheory.CategoryStruct.comp i.hom f = X.arrow → X = CategoryTheory.Subobject.mk f
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.instModule : {S : Type u_1} →
  {R : Type u_3} →
    {c₁ c₂ c₃ : R} →
      [inst : Semiring S] → [inst_1 : AddCommGroup R] → [Module S R] → Module S (QuaternionAlgebra R c₁ c₂ c₃)
-- Mathlib.FieldTheory.IsAlgClosed.Spectrum
_private.Mathlib.FieldTheory.IsAlgClosed.Spectrum.0.spectrum.«term↑ₐ_1» : Lean.ParserDescr
-- Mathlib.RingTheory.IntegralClosure.IntegralRestrict
instFintypeAlgEquivOfIsDomainOfIsIntegrallyClosedOfFiniteOfIsTorsionFree : (A : Type u_1) →
  (B : Type u_6) →
    [inst : CommRing A] →
      [inst_1 : CommRing B] →
        [inst_2 : Algebra A B] →
          [IsDomain A] →
            [IsDomain B] →
              [IsIntegrallyClosed B] → [Module.Finite A B] → [Module.IsTorsionFree A B] → Fintype (B ≃ₐ[A] B)
-- Mathlib.CategoryTheory.Filtered.Final
/-- If `C` is filtered, then we can give an explicit condition for a functor `F : C ⥤ D` to
be final.  -/
CategoryTheory.Functor.final_iff_of_isFiltered : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.IsFilteredOrEmpty C],
  F.Final ↔
    (∀ (d : D), ∃ c, Nonempty (d ⟶ F.obj c)) ∧
      ∀ {d : D} {c : C} (s s' : d ⟶ F.obj c),
        ∃ c' t, CategoryTheory.CategoryStruct.comp s (F.map t) = CategoryTheory.CategoryStruct.comp s' (F.map t)
-- Mathlib.Probability.Kernel.Disintegration.Integral
ProbabilityTheory.setIntegral_condKernel_univ_left : ∀ {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω] [inst_2 : Nonempty Ω]
  [inst_3 : MeasurableSpace.CountableOrCountablyGenerated α β] {κ : ProbabilityTheory.Kernel α (β × Ω)}
  [inst_4 : ProbabilityTheory.IsFiniteKernel κ] {E : Type u_4} {f : β × Ω → E} [inst_5 : NormedAddCommGroup E]
  [inst_6 : NormedSpace ℝ E] (a : α) {t : Set Ω},
  MeasurableSet t →
    MeasureTheory.IntegrableOn f (Set.univ ×ˢ t) (κ a) →
      ∫ (b : β), ∫ (ω : Ω) in t, f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a = ∫ (x : β × Ω) in Set.univ ×ˢ t, f x ∂κ a
-- Mathlib.CategoryTheory.Monoidal.Types.Basic
CategoryTheory.whiskerRight_apply : ∀ {Y Z : Type u} (f : Y ⟶ Z) (X : Type u) (p : CategoryTheory.MonoidalCategoryStruct.tensorObj Y X),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X)) p =
    ((CategoryTheory.ConcreteCategory.hom f) p.1, p.2)