mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Projection
/-- **Alias** of `Submodule.projectionOnto_projection`. -/
Submodule.linearProjOfIsCompl_isCompl_projection : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {p q : Submodule R E}
  (h : IsCompl p q) (x : E), (p.projectionOnto q h) ((p.projection q h) x) = (p.projectionOnto q h) x
-- Mathlib.LinearAlgebra.Dual.BaseChange
/-- The linear map underlying `IsBaseChange.toDualBaseChangeLinearEquiv`.  -/
_private.Mathlib.LinearAlgebra.Dual.BaseChange.0.IsBaseChange.toDualBaseChangeAux : {R : Type u_1} →
  [inst : CommSemiring R] →
    {V : Type u_2} →
      [inst_1 : AddCommMonoid V] →
        [inst_2 : Module R V] →
          {W : Type u_3} →
            [inst_3 : AddCommMonoid W] →
              [inst_4 : Module R W] →
                {A : Type u_4} →
                  [inst_5 : CommSemiring A] →
                    [inst_6 : Algebra R A] →
                      [inst_7 : Module A W] →
                        [inst_8 : IsScalarTower R A W] →
                          {j : V →ₗ[R] W} → IsBaseChange A j → TensorProduct R A (Module.Dual R V) →ₗ[A] Module.Dual A W
-- Mathlib.Order.Interval.Set.Disjoint
Set.Ioi_disjoint_Iio_of_not_lt : ∀ {α : Type v} [inst : Preorder α] {a b : α}, ¬a < b → Disjoint (Set.Ioi a) (Set.Iio b)
-- Mathlib.GroupTheory.Congruence.Hom
/-- The natural homomorphism from a monoid to its quotient by a congruence relation.  -/
Con.mk' : {M : Type u_1} → [inst : MulOneClass M] → (c : Con M) → M →* c.Quotient
-- Mathlib.Algebra.Category.Grp.Basic
CommGrpCat.instCategory.eq_1 : CommGrpCat.instCategory =
  { Hom := fun X Y => X.Hom Y, id := fun X => { hom' := MonoidHom.id ↑X },
    comp := fun {X Y Z} f g => { hom' := g.hom'.comp f.hom' }, id_comp := @CommGrpCat.instCategory._proof_1,
    comp_id := @CommGrpCat.instCategory._proof_2, assoc := @CommGrpCat.instCategory._proof_3 }
-- Lean.Meta.Tactic.Grind.EMatchTheorem
/-- The parent pattern is the gadget `Grind.genPattern` and `Grind.genHEqPattern`.
These gadgets assume the arguments are variables (see: `isGenPattern?`).
Thus, during normalization we must not replace them with `dontCare`.
 -/
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.NormalizePattern.ParentKind.genPattern : Lean.Meta.Grind.NormalizePattern.ParentKind✝
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.homEquiv_naturality_right_square_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) {X' X : C} {Y Y' : D} (f : X' ⟶ X)
  (g : X ⟶ G.obj Y') (h : X' ⟶ G.obj Y) (k : Y ⟶ Y'),
  CategoryTheory.CategoryStruct.comp (F.map f) ((adj.homEquiv X Y').symm g) =
      CategoryTheory.CategoryStruct.comp ((adj.homEquiv X' Y).symm h) k ↔
    CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp h (G.map k)
-- Mathlib.RingTheory.WittVector.Defs
WittVector.wittZero.congr_simp : ∀ (p p_1 : ℕ) (e_p : p = p_1) [hp : Fact (Nat.Prime p)] (a a_1 : ℕ),
  a = a_1 → WittVector.wittZero p a = WittVector.wittZero p_1 a_1
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
_private.Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop.0.Std.IterM.findSomeM?.match_1.eq_1 : ∀ {γ : Type u_1} (motive : Option γ → Sort u_2) (h_1 : Unit → motive none) (h_2 : (fx : γ) → motive (some fx)),
  (match none with
    | none => h_1 ()
    | some fx => h_2 fx) =
    h_1 ()
-- Lean.Elab.Declaration
Lean.Elab.Command.elabInitialize : Lean.Elab.Command.CommandElab
-- Lean.DocString.Types
Lean.Doc.Part.brecOn_2.eq : ∀ {i : Type u} {b : Type v} {p : Type w} {motive_1 : Lean.Doc.Part i b p → Sort u_1}
  {motive_2 : Array (Lean.Doc.Part i b p) → Sort u_1} {motive_3 : List (Lean.Doc.Part i b p) → Sort u_1}
  (t : List (Lean.Doc.Part i b p)) (F_1 : (t : Lean.Doc.Part i b p) → t.below → motive_1 t)
  (F_2 : (t : Array (Lean.Doc.Part i b p)) → Lean.Doc.Part.below_1 t → motive_2 t)
  (F_3 : (t : List (Lean.Doc.Part i b p)) → Lean.Doc.Part.below_2 t → motive_3 t),
  Lean.Doc.Part.brecOn_2 t F_1 F_2 F_3 = F_3 t (Lean.Doc.Part.brecOn_2.go t F_1 F_2 F_3).2
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
_private.Mathlib.Tactic.CategoryTheory.Coherence.Normalize.0.Mathlib.Tactic.BicategoryLike.evalWhiskerLeft.match_1.eq_1 : ∀ (motive : Mathlib.Tactic.BicategoryLike.Mor₁ → Mathlib.Tactic.BicategoryLike.NormalExpr → Sort u_1)
  (f : Mathlib.Tactic.BicategoryLike.Mor₁) (e : Mathlib.Tactic.BicategoryLike.Mor₂)
  (α : Mathlib.Tactic.BicategoryLike.Structural)
  (h_1 :
    (f : Mathlib.Tactic.BicategoryLike.Mor₁) →
      (e : Mathlib.Tactic.BicategoryLike.Mor₂) →
        (α : Mathlib.Tactic.BicategoryLike.Structural) → motive f (Mathlib.Tactic.BicategoryLike.NormalExpr.nil e α))
  (h_2 :
    (f : Mathlib.Tactic.BicategoryLike.Atom₁) →
      (e : Mathlib.Tactic.BicategoryLike.Mor₂) →
        (α : Mathlib.Tactic.BicategoryLike.Structural) →
          (η : Mathlib.Tactic.BicategoryLike.WhiskerLeft) →
            (ηs : Mathlib.Tactic.BicategoryLike.NormalExpr) →
              motive (Mathlib.Tactic.BicategoryLike.Mor₁.of f) (Mathlib.Tactic.BicategoryLike.NormalExpr.cons e α η ηs))
  (h_3 :
    (e : Lean.Expr) →
      (f g : Mathlib.Tactic.BicategoryLike.Mor₁) →
        (η : Mathlib.Tactic.BicategoryLike.NormalExpr) → motive (Mathlib.Tactic.BicategoryLike.Mor₁.comp e f g) η)
  (h_4 :
    (e : Lean.Expr) →
      (a : Mathlib.Tactic.BicategoryLike.Obj) →
        (η : Mathlib.Tactic.BicategoryLike.NormalExpr) → motive (Mathlib.Tactic.BicategoryLike.Mor₁.id e a) η),
  (match f, Mathlib.Tactic.BicategoryLike.NormalExpr.nil e α with
    | f, Mathlib.Tactic.BicategoryLike.NormalExpr.nil e α => h_1 f e α
    | Mathlib.Tactic.BicategoryLike.Mor₁.of f, Mathlib.Tactic.BicategoryLike.NormalExpr.cons e α η ηs => h_2 f e α η ηs
    | Mathlib.Tactic.BicategoryLike.Mor₁.comp e f g, η => h_3 e f g η
    | Mathlib.Tactic.BicategoryLike.Mor₁.id e a, η => h_4 e a η) =
    h_1 f e α
-- Mathlib.Algebra.Homology.HomotopyFiber
HomologicalComplex.HasHomotopyFiber.hasBinaryBiproduct : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {inst_1 : CategoryTheory.Preadditive C} {α : Type u_2}
  {c : ComplexShape α} {F G : HomologicalComplex C c} (φ : F ⟶ G) [self : HomologicalComplex.HasHomotopyFiber φ]
  (i j : α), c.Rel i j → CategoryTheory.Limits.HasBinaryBiproduct (G.X i) (F.X j)
-- Mathlib.CategoryTheory.Preadditive.Mat
/-- Two additive functors `Mat_ C ⥤ D` are naturally isomorphic if
their precompositions with `embedding C` are naturally isomorphic as functors `C ⥤ D`.  -/
CategoryTheory.Mat_.ext : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {D : Type u₁} →
        [inst_2 : CategoryTheory.Category.{v₁, u₁} D] →
          [inst_3 : CategoryTheory.Preadditive D] →
            [CategoryTheory.Limits.HasFiniteBiproducts D] →
              {F G : CategoryTheory.Functor (CategoryTheory.Mat_ C) D} →
                [F.Additive] →
                  [G.Additive] →
                    ((CategoryTheory.Mat_.embedding C).comp F ≅ (CategoryTheory.Mat_.embedding C).comp G) → (F ≅ G)
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.C_eq_algebraMap : ∀ {R : Type u_1} [inst : CommSemiring R] {r : R}, PowerSeries.C r = (algebraMap R (PowerSeries R)) r
-- Mathlib.LinearAlgebra.Matrix.SemiringInverse
Matrix.IsDetpBalanced.congr_simp : ∀ {n : Type u_1} {R : Type u_3} [inst : Fintype n] {inst_1 : DecidableEq n} [inst_2 : DecidableEq n]
  [inst_3 : CommSemiring R] (A A_1 : Matrix n n R),
  A = A_1 → ∀ (a a_1 : R), a = a_1 → ∀ (b b_1 : R), b = b_1 → A.IsDetpBalanced a b = A_1.IsDetpBalanced a_1 b_1
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Pullbacks
/-- Evaluating a pullback amounts to taking the pullback of the evaluations.  -/
CategoryTheory.Limits.pullbackObjIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F G H : CategoryTheory.Functor D C} →
          [inst_2 : CategoryTheory.Limits.HasPullbacks C] →
            (f : F ⟶ H) →
              (g : G ⟶ H) →
                (d : D) →
                  (CategoryTheory.Limits.pullback f g).obj d ≅ CategoryTheory.Limits.pullback (f.app d) (g.app d)
-- Mathlib.Topology.Homotopy.Lifting
/-- Lifting two paths that are homotopic relative to `{0,1}`
starting from the same point also ends up in the same point.  -/
IsCoveringMap.liftPath_apply_one_eq_of_homotopicRel : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {p : E → X}
  (cov : IsCoveringMap p) {γ₀ γ₁ : C(↑unitInterval, X)},
  γ₀.HomotopicRel γ₁ {0, 1} →
    ∀ (e : E) (h₀ : γ₀ 0 = p e) (h₁ : γ₁ 0 = p e), (cov.liftPath γ₀ e h₀) 1 = (cov.liftPath γ₁ e h₁) 1
-- Mathlib.Analysis.Convex.Between
wbtw_smul_vadd_smul_vadd_of_nonpos_of_nonneg : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R]
  [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P] (x : P) (v : V) {r₁ r₂ : R},
  r₁ ≤ 0 → 0 ≤ r₂ → Wbtw R (r₁ • v +ᵥ x) x (r₂ • v +ᵥ x)
-- Mathlib.RingTheory.NonUnitalSubring.Basic
/-- The `NonUnitalSubring` generated by a set.  -/
NonUnitalSubring.closure : {R : Type u} → [inst : NonUnitalNonAssocRing R] → Set R → NonUnitalSubring R
-- Mathlib.Analysis.BoxIntegral.Partition.Tagged
BoxIntegral.Prepartition.iUnion_biUnionTagged : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I)
  (πi : (J : BoxIntegral.Box ι) → BoxIntegral.TaggedPrepartition J),
  (π.biUnionTagged πi).iUnion = ⋃ J ∈ π, (πi J).iUnion
-- Lean.Structure
Lean.instInhabitedStructureResolutionState : Inhabited Lean.StructureResolutionState
-- Mathlib.Computability.Ackermann
_private.Mathlib.Computability.Ackermann.0.sq_le_two_pow_add_one_minus_three : ∀ (n : ℕ), n ^ 2 ≤ 2 ^ (n + 1) - 3
-- Mathlib.LinearAlgebra.Matrix.ToLin
Matrix.toLinOfInv_symm_apply : ∀ {R : Type u_1} [inst : CommSemiring R] {m : Type u_3} {n : Type u_4} [inst_1 : Fintype n] [inst_2 : DecidableEq n]
  {M₁ : Type u_5} {M₂ : Type u_6} [inst_3 : AddCommMonoid M₁] [inst_4 : AddCommMonoid M₂] [inst_5 : Module R M₁]
  [inst_6 : Module R M₂] (v₁ : Module.Basis n R M₁) (v₂ : Module.Basis m R M₂) [inst_7 : Fintype m]
  [inst_8 : DecidableEq m] {M : Matrix m n R} {M' : Matrix n m R} (hMM' : M * M' = 1) (hM'M : M' * M = 1) (a : M₂),
  (Matrix.toLinOfInv v₁ v₂ hMM' hM'M).symm a = ((Matrix.toLin v₂ v₁) M') a
-- Mathlib.Order.WithBot
WithTop.instPreorder : {α : Type u_1} → [Preorder α] → Preorder (WithTop α)
-- Mathlib.Algebra.Order.CauSeq.Basic
/-- The constant Cauchy sequence.  -/
CauSeq.const : {α : Type u_1} →
  {β : Type u_2} →
    [inst : Field α] →
      [inst_1 : LinearOrder α] →
        [inst_2 : IsStrictOrderedRing α] → [inst_3 : Ring β] → (abv : β → α) → [IsAbsoluteValue abv] → β → CauSeq β abv
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.rightHomologyMap'_zero : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData),
  CategoryTheory.ShortComplex.rightHomologyMap' 0 h₁ h₂ = 0
-- Std.Data.ExtTreeMap.Basic
/-- Modifies in place the value associated with a given key,
allowing creating new values and deleting values via an `Option` valued replacement function.

This function ensures that the value is used linearly.
 -/
Std.ExtTreeMap.alter : {α : Type u} →
  {β : Type v} →
    {cmp : α → α → Ordering} →
      [Std.TransCmp cmp] → Std.ExtTreeMap α β cmp → α → (Option β → Option β) → Std.ExtTreeMap α β cmp
-- Mathlib.Algebra.Group.Subgroup.Pointwise
Set.mul_subgroupClosure : ∀ {G : Type u_2} [inst : Group G] {s : Set G}, s.Nonempty → s * ↑(Subgroup.closure s) = ↑(Subgroup.closure s)
-- Mathlib.Analysis.RCLike.Basic
LinearIsometryEquiv.symm_smul_apply : ∀ {𝕜 : Type u_3} {V : Type u_4} {W : Type u_5} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup V]
  [inst_2 : Module 𝕜 V] [inst_3 : SeminormedAddCommGroup W] [inst_4 : NormedSpace 𝕜 W] (e : V ≃ₗᵢ[𝕜] W)
  (α : ↥(unitary 𝕜)) (x : W), (α • e).symm x = ↑α⁻¹ • e.symm x
-- Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
ProbabilityTheory.IsMeasurableRatCDF.measurable : ∀ {α : Type u_1} [inst : MeasurableSpace α] {f : α → ℚ → ℝ}, ProbabilityTheory.IsMeasurableRatCDF f → Measurable f
-- Std.Data.DTreeMap.Basic
/-- Tries to retrieve the key-value pair with the largest key in the tree map, returning `none` if the
map is empty.
 -/
Std.DTreeMap.Const.maxEntry? : {α : Type u} → {cmp : α → α → Ordering} → {β : Type v} → Std.DTreeMap α (fun x => β) cmp → Option (α × β)
-- Lean.Message
Lean.instToMessageDataFormat : Lean.ToMessageData Std.Format
-- Mathlib.Data.DFinsupp.Submonoid
DFinsupp.filterAddMonoidHom.congr_simp : ∀ {ι : Type u} (β : ι → Type v) [inst : (i : ι) → AddZeroClass (β i)] (p p_1 : ι → Prop),
  p = p_1 →
    ∀ {inst_1 : DecidablePred p} [inst_2 : DecidablePred p_1],
      DFinsupp.filterAddMonoidHom β p = DFinsupp.filterAddMonoidHom β p_1
-- Std.Time.DateTime.PlainDateTime
/-- Getter for the `Second` inside of a `PlainDateTime`.
 -/
Std.Time.PlainDateTime.second : Std.Time.PlainDateTime → Std.Time.Second.Ordinal true
-- Mathlib.RingTheory.FiniteStability
Algebra.FiniteType.baseChangeAux_surj : ∀ {R : Type w₁} [inst : CommRing R] {A : Type w₂} [inst_1 : CommRing A] [inst_2 : Algebra R A] (B : Type w₃)
  [inst_3 : CommRing B] [inst_4 : Algebra R B] {σ : Type u_1} {f : MvPolynomial σ R →ₐ[R] A},
  Function.Surjective ⇑f → Function.Surjective ⇑(Algebra.TensorProduct.map (AlgHom.id B B) f)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.LaxMonoidalFunctor.isoOfComponents.congr_simp : ∀ {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 D]
  {F G : CategoryTheory.LaxMonoidalFunctor C D} (e e_1 : (X : C) → F.obj X ≅ G.obj X) (e_e : e = e_1)
  (naturality :
    ∀ {X Y : C} (f : X ⟶ Y),
      CategoryTheory.CategoryStruct.comp (F.map f) (e Y).hom = CategoryTheory.CategoryStruct.comp (e X).hom (G.map f))
  (unit :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε F.toFunctor)
        (e (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom =
      CategoryTheory.Functor.LaxMonoidal.ε G.toFunctor)
  (tensor :
    ∀ (X Y : C),
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F.toFunctor X Y)
          (e (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)).hom =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (e X).hom (e Y).hom)
          (CategoryTheory.Functor.LaxMonoidal.μ G.toFunctor X Y)),
  CategoryTheory.LaxMonoidalFunctor.isoOfComponents e naturality unit tensor =
    CategoryTheory.LaxMonoidalFunctor.isoOfComponents e_1 ⋯ ⋯ ⋯
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.instMonoidalMonForget₂Mon.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C],
  CategoryTheory.Grp.instMonoidalMonForget₂Mon =
    { ε := CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Mon C)),
      μ := fun G H =>
        CategoryTheory.CategoryStruct.id
          (CategoryTheory.MonoidalCategoryStruct.tensorObj ((CategoryTheory.Grp.forget₂Mon C).obj G)
            ((CategoryTheory.Grp.forget₂Mon C).obj H)),
      μ_natural_left := ⋯, μ_natural_right := ⋯, associativity := ⋯, left_unitality := ⋯, right_unitality := ⋯,
      η :=
        CategoryTheory.CategoryStruct.id
          ((CategoryTheory.Grp.forget₂Mon C).obj
            (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Grp C))),
      δ := fun G H =>
        CategoryTheory.CategoryStruct.id
          ((CategoryTheory.Grp.forget₂Mon C).obj (CategoryTheory.MonoidalCategoryStruct.tensorObj G H)),
      δ_natural_left := ⋯, δ_natural_right := ⋯, oplax_associativity := ⋯, oplax_left_unitality := ⋯,
      oplax_right_unitality := ⋯, ε_η := ⋯, η_ε := ⋯, μ_δ := ⋯, δ_μ := ⋯ }
-- Std.Data.TreeSet.Slice
Std.TreeSet.instSliceableRooSlice : {α : Type u} →
  (cmp : autoParam (α → α → Ordering) Std.TreeSet.instSliceableRooSlice._auto_1) →
    Std.Roo.Sliceable (Std.TreeSet α cmp) α (Std.DTreeMap.Internal.Unit.RooSlice α)
-- Mathlib.CategoryTheory.Category.Preorder
Preorder.subsingleton_hom : ∀ {α : Type u} [inst : Preorder α] (U V : α), Subsingleton (U ⟶ V)
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
/-- If the angle between three points is 0, they are collinear.  -/
EuclideanGeometry.collinear_of_angle_eq_zero : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {p₁ p₂ p₃ : P}, EuclideanGeometry.angle p₁ p₂ p₃ = 0 → Collinear ℝ {p₁, p₂, p₃}
-- Mathlib.RingTheory.LocalRing.ResidueField.Ideal
/-- The residue field at a prime ideal, defined to be the residue field of the local ring
`Localization.Prime I`.
We also provide an `IsFractionRing (R ⧸ I) I.ResidueField` instance.
 -/
Ideal.ResidueField : {R : Type u_1} → [inst : CommRing R] → (I : Ideal R) → [I.IsPrime] → Type u_1
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
mvfderiv_mul : ∀ {𝕜 : 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 g : M → 𝕜} {x : M},
  MDiffAt f x → MDiffAt g x → d% (f * g) x = f x • d% g x + g x • d% f x
-- Std.Data.Internal.List.Associative
Std.Internal.List.getEntryD_append_of_containsKey_eq_false : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l l' : List ((a : α) × β a)} {a : α} {fallback : (a : α) × β a},
  Std.Internal.List.containsKey a l' = false →
    Std.Internal.List.getEntryD a fallback (l ++ l') = Std.Internal.List.getEntryD a fallback l
-- Init.Data.String.Defs
/-- The byte position of the end of the string slice.  -/
String.Slice.endExclusive : (self : String.Slice) → self.str.Pos
-- Lean.Parser.Term
/-- `.(e)` marks an "inaccessible pattern", which does not influence evaluation of the pattern match, but may be necessary for type-checking.
In contrast to regular patterns, `e` may be an arbitrary term of the appropriate type.
 -/
Lean.Parser.Term.inaccessible : Lean.Parser.Parser
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.infinitePos_iff_infinite_of_pos : ∀ {x : ℝ*}, 0 < x → (x.InfinitePos ↔ x.Infinite)
-- Mathlib.CategoryTheory.Sites.Precoverage
CategoryTheory.Precoverage.HasPullbacks.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C},
  (∀ {X Y : C} {R : CategoryTheory.Presieve Y} (f : X ⟶ Y), R ∈ J.coverings Y → R.HasPullbacks f) → J.HasPullbacks
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Functor.mapAddGrp.instMonoidal.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  [inst_4 : CategoryTheory.BraidedCategory C] [inst_5 : CategoryTheory.BraidedCategory D]
  (F : CategoryTheory.Functor C D) [inst_6 : F.Braided],
  CategoryTheory.Functor.mapAddGrp.instMonoidal F =
    {
        εIso :=
          (CategoryTheory.AddGrp.fullyFaithfulForget₂Mon D).preimageIso
            (CategoryTheory.Functor.Monoidal.εIso F.mapAddMon),
        μIso := fun X Y =>
          (CategoryTheory.AddGrp.fullyFaithfulForget₂Mon D).preimageIso
            (CategoryTheory.Functor.Monoidal.μIso F.mapAddMon X.toAddMon Y.toAddMon),
        μIso_hom_natural_left := ⋯, μIso_hom_natural_right := ⋯, associativity := ⋯, left_unitality := ⋯,
        right_unitality := ⋯ }.toMonoidal
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.prod_antilipschitzWith_toLp : ∀ (p : ENNReal) (α : Type u_2) (β : Type u_3) [hp : Fact (1 ≤ p)] [inst : PseudoEMetricSpace α]
  [inst_1 : PseudoEMetricSpace β], AntilipschitzWith 1 (WithLp.toLp p)
-- Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv
QuadraticMap.IsometryEquiv.mk.sizeOf_spec : ∀ {R : Type u_2} {M₁ : Type u_5} {M₂ : Type u_6} {N : Type u_9} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid N] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R N] {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₂ N} [inst_7 : SizeOf R] [inst_8 : SizeOf M₁]
  [inst_9 : SizeOf M₂] [inst_10 : SizeOf N] (toLinearEquiv : M₁ ≃ₗ[R] M₂)
  (map_app' : ∀ (m : M₁), Q₂ ((↑toLinearEquiv).toFun m) = Q₁ m),
  sizeOf { toLinearEquiv := toLinearEquiv, map_app' := map_app' } = 1 + sizeOf toLinearEquiv
-- Mathlib.GroupTheory.SemidirectProduct
SemidirectProduct.mulEquivProd_symm_apply_right : ∀ {N : Type u_1} {G : Type u_2} [inst : Group N] [inst_1 : Group G] (x : N × G),
  (SemidirectProduct.mulEquivProd.symm x).right = x.2
-- Mathlib.Data.Matrix.ColumnRowPartitioned
Matrix.vecMul_fromRows : ∀ {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} [inst : Semiring R] [inst_1 : Fintype m₁]
  [inst_2 : Fintype m₂] (B₁ : Matrix m₁ n R) (B₂ : Matrix m₂ n R) (v : m₁ ⊕ m₂ → R),
  Matrix.vecMul v (B₁.fromRows B₂) = Matrix.vecMul (v ∘ Sum.inl) B₁ + Matrix.vecMul (v ∘ Sum.inr) B₂
-- Mathlib.Algebra.Order.GroupWithZero.Basic
/-- **Alias** of the reverse direction of `inv_pos`. -/
inv_pos_of_pos : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀}, 0 < a → 0 < a⁻¹
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Submonoid.LocalizationMap.mul_mk'_eq_mk'_of_mul : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N]
  (f : S.LocalizationMap N) (x₁ x₂ : M) (y : ↥S), f x₁ * f.mk' x₂ y = f.mk' (x₁ * x₂) y
-- Mathlib.Lean.Meta.RefinedDiscrTree.Lookup
Lean.Meta.RefinedDiscrTree.MatchResult.mk.injEq : ∀ {α : Type} (elts elts_1 : Std.TreeMap ℕ (Array (Array α)) compare),
  ({ elts := elts } = { elts := elts_1 }) = (elts = elts_1)
-- Mathlib.Combinatorics.Additive.DoublingConst
/-- If `A` has small difference, then it has small doubling, with the constant squared.

This is a consequence of the Ruzsa triangle inequality.  -/
Finset.mulConst_le_divConst_sq : ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : DecidableEq G] {A : Finset G}, A.mulConst A ≤ A.divConst A ^ 2
-- Mathlib.Algebra.Category.Grp.Basic
/-- Additive equivalences between `AddGroup`s are the same
as (isomorphic to) isomorphisms in `AddGrpCat`.  -/
addEquivIsoAddGroupIso : {X Y : AddGrpCat} → ↑X ≃+ ↑Y ≅ X ≅ Y
-- Mathlib.RingTheory.PrincipalIdealDomain
IsBezout.gcd.congr_simp : ∀ {R : Type u} [inst : Ring R] (x x_1 : R) (e_x : x = x_1) (y y_1 : R) (e_y : y = y_1)
  [inst_1 : Submodule.IsPrincipal (Ideal.span {x, y})], IsBezout.gcd x y = IsBezout.gcd x_1 y_1
-- Mathlib.Data.ENat.Pow
ENat.top_epow : ∀ {y : ℕ∞}, y ≠ 0 → ⊤ ^ y = ⊤
-- Mathlib.AlgebraicGeometry.Morphisms.Smooth
/-- Open immersions are smooth of relative dimension `0`.  -/
AlgebraicGeometry.instSmoothOfRelativeDimensionOfNatNatOfIsOpenImmersion : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsOpenImmersion f],
  AlgebraicGeometry.SmoothOfRelativeDimension 0 f
-- Mathlib.Combinatorics.SimpleGraph.Basic
/-- **Alias** of the forward direction of `SimpleGraph.neighborSet_eq_compl_singleton`. -/
SimpleGraph.IsUniversal.of_neighborSet_eq : ∀ {V : Type u} {G : SimpleGraph V} {v : V}, G.neighborSet v = {v}ᶜ → G.IsUniversal v
-- Mathlib.Geometry.Euclidean.SignedDist
signedDist_vadd_vadd : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (v w : V) (p q : P), ((signedDist v) (w +ᵥ p)) (w +ᵥ q) = ((signedDist v) p) q
-- Mathlib.Order.Filter.Ultrafilter.Defs
Ultrafilter.lawfulMonad : LawfulMonad Ultrafilter
-- Mathlib.Tactic.Order
/-- Necessary for tracing below.  -/
Mathlib.Tactic.Order.instOrdProdNatExpr_mathlib : Ord (ℕ × Lean.Expr)