mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Array.Lemmas
Array.replace_replicate_ne : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {n : ℕ} {a b c : α},
  (!b == a) = true → (Array.replicate n a).replace b c = Array.replicate n a
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toList_roc_eq_singleton : ∀ {m n : ℤ}, n = m + 1 → (m<...=n).toList = [m + 1]
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.fold_eq_foldl_toList : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} {δ : Type w}
  {f : δ → (a : α) → β a → δ} {init : δ},
  Std.DHashMap.fold f init m = List.foldl (fun a b => f a b.fst b.snd) init m.toList
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
Convexity.convexCombPair_convexCombPair_assoc_right : ∀ {R : Type u_1} {M : Type u_3} [inst : PartialOrder R] [inst_1 : Semiring R] [inst_2 : IsStrictOrderedRing R]
  [inst_3 : Convexity.ConvexSpace R M] {s t : R} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) {s' t' : R} (hs' : 0 ≤ s')
  (ht' : 0 ≤ t') (h' : s' + t' = 1) {s'' t'' : R} (hs'' : 0 ≤ s'') (ht'' : 0 ≤ t'') (h'' : s'' + t'' = 1),
  s * t'' = t * s' * s'' →
    ∀ (m₁ m₂ m₃ : M),
      Convexity.convexCombPair s t hs ht h m₁ (Convexity.convexCombPair s' t' hs' ht' h' m₂ m₃) =
        Convexity.convexCombPair (s + t * s') (t * t') ⋯ ⋯ ⋯ (Convexity.convexCombPair s'' t'' hs'' ht'' h'' m₁ m₂) m₃
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr.0.Std.Tactic.BVDecide.BVExpr.bitblast.go.match_15.eq_3 : ∀ (motive : Std.Tactic.BVDecide.BVUnOp → Sort u_1) (distance : ℕ) (h_1 : Unit → motive Std.Tactic.BVDecide.BVUnOp.not)
  (h_2 : (distance : ℕ) → motive (Std.Tactic.BVDecide.BVUnOp.rotateLeft distance))
  (h_3 : (distance : ℕ) → motive (Std.Tactic.BVDecide.BVUnOp.rotateRight distance))
  (h_4 : (distance : ℕ) → motive (Std.Tactic.BVDecide.BVUnOp.arithShiftRightConst distance))
  (h_5 : Unit → motive Std.Tactic.BVDecide.BVUnOp.reverse) (h_6 : Unit → motive Std.Tactic.BVDecide.BVUnOp.clz)
  (h_7 : Unit → motive Std.Tactic.BVDecide.BVUnOp.cpop),
  (match Std.Tactic.BVDecide.BVUnOp.rotateRight distance with
    | Std.Tactic.BVDecide.BVUnOp.not => h_1 ()
    | Std.Tactic.BVDecide.BVUnOp.rotateLeft distance => h_2 distance
    | Std.Tactic.BVDecide.BVUnOp.rotateRight distance => h_3 distance
    | Std.Tactic.BVDecide.BVUnOp.arithShiftRightConst distance => h_4 distance
    | Std.Tactic.BVDecide.BVUnOp.reverse => h_5 ()
    | Std.Tactic.BVDecide.BVUnOp.clz => h_6 ()
    | Std.Tactic.BVDecide.BVUnOp.cpop => h_7 ()) =
    h_3 distance
-- Init.Data.Nat.Basic
Nat.succ_ne_succ_iff : ∀ {a b : ℕ}, a.succ ≠ b.succ ↔ a ≠ b
-- Mathlib.Combinatorics.Enumerative.DyckWord
DyckStep.ofNat : ℕ → DyckStep
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.comm_comp_map_apply : ∀ {R : Type uR} {A : Type uA} {B : Type uB} {C : Type uC} {D : Type uD} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : Semiring B] [inst_4 : Algebra R B] [inst_5 : Semiring C] [inst_6 : Algebra R C]
  [inst_7 : Semiring D] [inst_8 : Algebra R D] (f : A →ₐ[R] C) (g : B →ₐ[R] D) (x : TensorProduct R A B),
  (Algebra.TensorProduct.comm R C D) ((Algebra.TensorProduct.map f g) x) =
    (Algebra.TensorProduct.map g f) ((Algebra.TensorProduct.comm R A B) x)
-- Init.Omega.LinearCombo
Lean.Omega.LinearCombo.add_eval : ∀ (l₁ l₂ : Lean.Omega.LinearCombo) (v : Lean.Omega.Coeffs), (l₁ + l₂).eval v = l₁.eval v + l₂.eval v
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
/-- A function from a model space `H` to itself is a local structomorphism, with respect to a
structure groupoid `G` for `H`, relative to a set `s` in `H`, if for all points `x` in the set, the
function agrees with a `G`-structomorphism on `s` in a neighbourhood of `x`.  -/
StructureGroupoid.IsLocalStructomorphWithinAt : {H : Type u_1} → [inst : TopologicalSpace H] → StructureGroupoid H → (H → H) → Set H → H → Prop
-- Mathlib.CategoryTheory.Limits.Fubini
CategoryTheory.Limits.coconeOfHasColimitCurryCompColim.eq_1 : ∀ {J : Type u_1} {K : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  (G : CategoryTheory.Functor (J × K) C) [inst_3 : CategoryTheory.Limits.HasColimitsOfShape K C]
  [inst_4 : CategoryTheory.Limits.HasColimit ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.colim)],
  CategoryTheory.Limits.coconeOfHasColimitCurryCompColim G =
    { pt := CategoryTheory.Limits.colimit ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.colim),
      ι :=
        {
          app := fun x =>
            CategoryTheory.CategoryStruct.comp
              (((CategoryTheory.Limits.DiagramOfCocones.mkOfHasColimits (CategoryTheory.Functor.curry.obj G)).obj
                      x.1).ι.app
                x.2)
              (CategoryTheory.Limits.colimit.ι ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.colim)
                x.1),
          naturality := ⋯ } }
-- Mathlib.CategoryTheory.Enriched.Basic
/-- Construct an honest category from a `Type v`-enriched category.
 -/
CategoryTheory.categoryOfEnrichedCategoryType : (C : Type u₁) → [𝒞 : CategoryTheory.EnrichedCategory (Type v) C] → CategoryTheory.Category.{v, u₁} C
-- Lean.Syntax
Lean.Syntax.rewriteBottomUpM : {m : Type → Type} → [Monad m] → (Lean.Syntax → m Lean.Syntax) → Lean.Syntax → m Lean.Syntax
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getEntry.congr_simp : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (t t_1 : Std.DTreeMap.Internal.Impl α β) (e_t : t = t_1) (k k_1 : α)
  (e_k : k = k_1) (hlk : k ∈ t), t.getEntry k hlk = t_1.getEntry k_1 ⋯
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
CategoryTheory.CountableAB4Star.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCountableProducts C],
  (∀ (α : Type) [inst_2 : Countable α], CategoryTheory.HasExactLimitsOfShape (CategoryTheory.Discrete α) C) →
    CategoryTheory.CountableAB4Star C
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
SSet.OneTruncation₂.ofNerve₂.natIso_inv_app_obj_obj : ∀ (X : CategoryTheory.Cat) (a : ↑X) (x : Fin 1), ((SSet.OneTruncation₂.ofNerve₂.natIso.inv.app X).obj a).obj x = a
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.keys_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.keys = t₂.keys
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKeyD_inter! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  m₁.WF →
    m₂.WF →
      ∀ {k fallback : α},
        (m₁.inter! m₂).getKeyD k fallback =
          if Std.DTreeMap.Internal.Impl.contains k m₂ = true then m₁.getKeyD k fallback else fallback
-- Mathlib.RingTheory.Ideal.Lattice
/-- All ideals in a division (semi)ring are trivial.  -/
Ideal.eq_bot_or_top : ∀ {K : Type u} [inst : DivisionSemiring K] (I : Ideal K), I = ⊥ ∨ I = ⊤
-- Mathlib.Geometry.Convex.Cone.Basic
ConvexCone.mk.injEq : ∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommMonoid M]
  [inst_3 : SMul R M] (carrier : Set M) (smul_mem' : ∀ ⦃c : R⦄, 0 < c → ∀ ⦃x : M⦄, x ∈ carrier → c • x ∈ carrier)
  (add_mem' : ∀ ⦃x : M⦄, x ∈ carrier → ∀ ⦃y : M⦄, y ∈ carrier → x + y ∈ carrier) (carrier_1 : Set M)
  (smul_mem'_1 : ∀ ⦃c : R⦄, 0 < c → ∀ ⦃x : M⦄, x ∈ carrier_1 → c • x ∈ carrier_1)
  (add_mem'_1 : ∀ ⦃x : M⦄, x ∈ carrier_1 → ∀ ⦃y : M⦄, y ∈ carrier_1 → x + y ∈ carrier_1),
  ({ carrier := carrier, smul_mem' := smul_mem', add_mem' := add_mem' } =
      { carrier := carrier_1, smul_mem' := smul_mem'_1, add_mem' := add_mem'_1 }) =
    (carrier = carrier_1)
-- Mathlib.Order.RelSeries
/-- If `f : α → β` is a strictly monotonic function and `α` is an infinite-dimensional type then so
is `β`.  -/
infiniteDimensionalOrder_of_strictMono : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (f : α → β),
  StrictMono f → ∀ [InfiniteDimensionalOrder α], InfiniteDimensionalOrder β
-- Mathlib.Tactic.FunProp.FunctionData
Mathlib.Meta.FunProp.instBEqMorApplication.beq : Mathlib.Meta.FunProp.MorApplication → Mathlib.Meta.FunProp.MorApplication → Bool
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
/-- The natural bijection between `α → β × γ` and `(α → β) × (α → γ)`, upgraded to a uniform
isomorphism between `α →ᵤ β × γ` and `(α →ᵤ β) × (α →ᵤ γ)`.  -/
UniformFun.uniformEquivProdArrow : {α : Type u_1} →
  {β : Type u_2} →
    {γ : Type u_3} →
      [inst : UniformSpace β] → [inst_1 : UniformSpace γ] → UniformFun α (β × γ) ≃ᵤ UniformFun α β × UniformFun α γ
-- Mathlib.Algebra.MonoidAlgebra.Basic
/-- **Alias** of `MonoidAlgebra.mapAlgEquiv_trans`. -/
MonoidAlgebra.mapRangeAlgEquiv_trans : ∀ {R : Type u_1} {A : Type u_4} {B : Type u_5} {C : Type u_6} {M : Type u_7} [inst : CommSemiring R]
  [inst_1 : Semiring A] [inst_2 : Semiring B] [inst_3 : Semiring C] [inst_4 : Algebra R A] [inst_5 : Algebra R B]
  [inst_6 : Algebra R C] [inst_7 : Monoid M] (e₁ : A ≃ₐ[R] B) (e₂ : B ≃ₐ[R] C),
  MonoidAlgebra.mapAlgEquiv R M (e₁.trans e₂) =
    (MonoidAlgebra.mapAlgEquiv R M e₁).trans (MonoidAlgebra.mapAlgEquiv R M e₂)
-- Init.Data.UInt.Basic
instSubUInt8 : Sub UInt8
-- Mathlib.AlgebraicGeometry.Morphisms.Basic
/-- `P` for `f` if `P` holds for `f` restricted to basic sets of a spanning set of the global
sections  -/
AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.of_basicOpenCover : ∀ {P : AlgebraicGeometry.AffineTargetMorphismProperty} [self : P.IsLocal] {X Y : AlgebraicGeometry.Scheme}
  [inst : AlgebraicGeometry.IsAffine Y] (f : X ⟶ Y) (s : Finset ↑(Y.presheaf.obj (Opposite.op ⊤))),
  Ideal.span ↑s = ⊤ → (∀ (r : ↥s), P (f ∣_ Y.basicOpen ↑r)) → P f
-- Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
AlgebraicGeometry.Scheme.IdealSheafData.map_mono : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y), Monotone fun x => x.map f
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.skeletonLT_top : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : T2Space X] [inst_1 : Topology.RelCWComplex C D],
  ↑(Topology.RelCWComplex.skeletonLT C ⊤) = C
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
PreQuasiregular.instMul : {R : Type u_1} → [NonUnitalSemiring R] → Mul (PreQuasiregular R)
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.neighborSet.eq_1 : ∀ {V : Type u} (G : SimpleGraph V) (v : V), G.neighborSet v = {w | G.Adj v w}
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.getKeyD_filterMap : ∀ {α : Type u} [inst : BEq α] [inst_1 : EquivBEq α] {β : Type v} {γ : Type w} {f : α → β → Option γ}
  {l : List ((_ : α) × β)} {k fallback : α},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.getKeyD k (List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) l)
        fallback =
      ((Std.Internal.List.getKey? k l).pfilter fun x h => (f x (Std.Internal.List.getValue x l ⋯)).isSome).getD fallback
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Power.beq'.eq_1 : ∀ (pw₁ pw₂ : Lean.Grind.CommRing.Power),
  pw₁.beq' pw₂ =
    Lean.Grind.CommRing.Power.rec
      (fun x₁ k₁ => Lean.Grind.CommRing.Power.rec (fun x₂ k₂ => Nat.beq x₁ x₂ && k₁.beq k₂) pw₂) pw₁
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.MonoidalCategory.rightUnitor_monoidal : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X₁ X₂ : C),
  CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.rightUnitor X₁).hom
      (CategoryTheory.MonoidalCategoryStruct.rightUnitor X₂).hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.tensorμ X₁ (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X₂
        (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ X₂)
          (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom)
        (CategoryTheory.MonoidalCategoryStruct.rightUnitor (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ X₂)).hom)
-- Lean.Meta.Tactic.Grind.Types
/-- Adds a new theorem instance produced using E-matching.  -/
Lean.Meta.Grind.addTheoremInstance : Lean.Meta.Grind.EMatchTheorem →
  Lean.Expr →
    Lean.Expr → ℕ → List Lean.Meta.Grind.TheoremGuard → List Lean.Meta.Grind.EMatchDiagNode → Lean.Meta.Grind.GoalM Unit
-- Mathlib.Algebra.Algebra.NonUnitalHom
/-- A morphism respecting addition, multiplication, and scalar multiplication
(denoted as `A →ₛₙₐ[φ] B`, or `A →ₙₐ[R] B` when `φ` is the identity on `R`).
When these arise from algebra structures, this is the same
as a not-necessarily-unital morphism of algebras.  -/
«term_→ₙₐ_» : Lean.TrailingParserDescr
-- Batteries.Lean.Meta.UnusedNames
/-- Auxiliary definition for `getUnusedUserNameIndex`.  -/
_private.Batteries.Lean.Meta.UnusedNames.0.Lean.LocalContext.getUnusedUserNameIndex.updateMinSuffix : Option ℕ → ℕ → Option ℕ
-- Lean.Meta.Instances
Lean.Meta.instInhabitedInstances : Inhabited Lean.Meta.Instances
-- Lean.Parser.Term
Lean.Parser.Term.showRhs.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Control.Applicative
instCommApplicativeId : CommApplicative Id
-- Mathlib.LinearAlgebra.Matrix.SemiringInverse
Matrix.detp_submatrix_equiv_self : ∀ {n : Type u_1} {m : Type u_2} {R : Type u_3} [inst : Fintype m] [inst_1 : Fintype n] [inst_2 : DecidableEq m]
  [inst_3 : DecidableEq n] [inst_4 : CommSemiring R] (s : ℤˣ) (A : Matrix n n R) (e : m ≃ n),
  Matrix.detp s (A.submatrix ⇑e ⇑e) = Matrix.detp s A
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
LinearIsometry.norm_compContinuousMultilinearMap : ∀ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} {G' : Type wG'} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_3 : SeminormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] [inst_5 : SeminormedAddCommGroup G']
  [inst_6 : NormedSpace 𝕜 G'] [inst_7 : Fintype ι] (g : G →ₗᵢ[𝕜] G') (f : ContinuousMultilinearMap 𝕜 E G),
  ‖g.toContinuousLinearMap.compContinuousMultilinearMap f‖ = ‖f‖
-- Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
MulAction.IsBlock.subsingleton_of_ssubset_compl_of_stabilizer_alternatingGroup_le : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {s B : Set α} {G : Subgroup ↥(alternatingGroup α)},
  s.Nontrivial → B ⊂ sᶜ → MulAction.stabilizer (↥(alternatingGroup α)) s ≤ G → MulAction.IsBlock (↥G) B → B.Subsingleton
-- Mathlib.NumberTheory.ArithmeticFunction.Moebius
ArithmeticFunction.moebius.eq_1 : ArithmeticFunction.moebius =
  { toFun := fun n => if Squarefree n then (-1) ^ ArithmeticFunction.cardFactors n else 0,
    map_zero' := ArithmeticFunction.moebius._proof_1 }
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.IsMonHom.one_hom_assoc : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} {M N : C}
  {inst_2 : CategoryTheory.MonObj M} {inst_3 : CategoryTheory.MonObj N} (f : M ⟶ N) [self : CategoryTheory.IsMonHom f]
  {Z : C} (h : N ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one (CategoryTheory.CategoryStruct.comp f h) =
    CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one h
-- Mathlib.Algebra.Pointwise.Stabilizer
AddAction.stabilizer_inf_stabilizer_le_stabilizer_apply₂ : ∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] {s t : Set α} {f : Set α → Set α → Set α},
  (∀ (a : G), a +ᵥ f s t = f (a +ᵥ s) (a +ᵥ t)) →
    AddAction.stabilizer G s ⊓ AddAction.stabilizer G t ≤ AddAction.stabilizer G (f s t)
-- Mathlib.Order.Filter.Pointwise
Filter.commMonoid.eq_1 : ∀ {α : Type u_2} [inst : CommMonoid α],
  Filter.commMonoid =
    { toMul := Filter.mulOneClass.toMul, mul_assoc := ⋯, toOne := Filter.mulOneClass.toOne, one_mul := ⋯, mul_one := ⋯,
      toNPow := Filter.monoid.toNPow, npow_zero := ⋯, npow_succ := ⋯, mul_comm := ⋯ }
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get_eq_get! : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {a : α}
  [inst_1 : Inhabited (β a)] {h : a ∈ m}, m.get a h = m.get! a
-- Mathlib.Data.Set.Constructions
/-- A structure encapsulating the fact that a set of sets is closed under finite intersection.  -/
FiniteInter : {α : Type u_1} → Set (Set α) → Prop
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- An `AffineSubspace k P` is a subset of an `AffineSpace V P` that, if not empty, has an affine
space structure induced by a corresponding subspace of the `Module k V`.  -/
AffineSubspace : (k : Type u_1) →
  {V : Type u_2} →
    (P : Type u_3) → [inst : Ring k] → [inst_1 : AddCommGroup V] → [Module k V] → [AddTorsor V P] → Type u_3
-- Mathlib.RingTheory.TensorProduct.IsBaseChangePi
/-- Localization of modules commutes with finite products.  -/
IsLocalizedModule.pi : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {ι : Type u_3} [Finite ι] {M : ι → Type u_4}
  {M' : ι → Type u_5} [inst_2 : (i : ι) → AddCommMonoid (M i)] [inst_3 : (i : ι) → AddCommMonoid (M' i)]
  [inst_4 : (i : ι) → Module R (M i)] [inst_5 : (i : ι) → Module R (M' i)] (f : (i : ι) → M i →ₗ[R] M' i)
  [∀ (i : ι), IsLocalizedModule S (f i)], IsLocalizedModule S (LinearMap.pi fun i => f i ∘ₗ LinearMap.proj i)
-- Mathlib.Analysis.CStarAlgebra.Unitary.Maps
Unitary.toLinearEquiv_mulLeft : ∀ {R : Type u_1} {A : Type u_2} [inst : NormedRing A] [inst_1 : StarRing A] [inst_2 : CStarRing A] [inst_3 : Ring R]
  [inst_4 : Module R A] [inst_5 : SMulCommClass R A A] (u : ↥(unitary A)),
  ((Unitary.mulLeft R A) u).toLinearEquiv = (Units.mulLeftLinearEquiv R A) (Unitary.toUnits u)
-- Mathlib.CategoryTheory.Preadditive.HomOrthogonal
CategoryTheory.HomOrthogonal.eq_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type u_1} {s : ι → C}
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C],
  CategoryTheory.HomOrthogonal s → ∀ {i j : ι}, i ≠ j → ∀ (f : s i ⟶ s j), f = 0
-- Init.Data.Vector.Range
Vector.fst_mem_of_mem_zipIdx : ∀ {α : Type u_1} {n : ℕ} {x : α × ℕ} {xs : Vector α n} {k : ℕ}, x ∈ xs.zipIdx k → x.1 ∈ xs
-- Mathlib.CategoryTheory.Limits.Indization.FilteredColimits
CategoryTheory.Limits.IndizationClosedUnderFilteredColimitsAux.exists_nonempty_limit_obj_of_colimit : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I : Type v} [inst_1 : CategoryTheory.SmallCategory I]
  (F : CategoryTheory.Functor I (CategoryTheory.Functor Cᵒᵖ (Type v))) {J : Type v}
  [inst_2 : CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J]
  (G :
    CategoryTheory.Functor J (CategoryTheory.CostructuredArrow CategoryTheory.yoneda (CategoryTheory.Limits.colimit F)))
  {K : Type v} [inst_4 : CategoryTheory.SmallCategory K]
  (H : CategoryTheory.Functor K (CategoryTheory.Over (CategoryTheory.Limits.colimit F))) [CategoryTheory.IsFiltered K],
  Nonempty
      (CategoryTheory.Limits.limit
        ((G.op.comp
              (CategoryTheory.CostructuredArrow.toOver CategoryTheory.yoneda (CategoryTheory.Limits.colimit F)).op).comp
          (CategoryTheory.yoneda.obj (CategoryTheory.Limits.colimit H)))) →
    ∃ k,
      Nonempty
        (CategoryTheory.Limits.limit
          ((G.op.comp
                (CategoryTheory.CostructuredArrow.toOver CategoryTheory.yoneda
                    (CategoryTheory.Limits.colimit F)).op).comp
            (CategoryTheory.yoneda.obj (H.obj k))))
-- Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
CategoryTheory.ObjectProperty.isVerdierRightLocalizing_iff : ∀ {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] [A.IsTriangulated] [B.IsTriangulated] [B.IsClosedUnderIsomorphisms],
  A.IsVerdierRightLocalizing B ↔
    ∀ ⦃X Y : C⦄ (s : X ⟶ Y),
      A X → B.trW s → ∃ Z s' b, A Z ∧ (A ⊓ B).trW s' ∧ CategoryTheory.CategoryStruct.comp s b = s'
-- Mathlib.Algebra.Homology.HomologicalComplex
ChainComplex.mk_X_1 : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  (X₀ X₁ X₂ : V) (d₀ : X₁ ⟶ X₀) (d₁ : X₂ ⟶ X₁) (s : CategoryTheory.CategoryStruct.comp d₁ d₀ = 0)
  (succ :
    (S : CategoryTheory.ShortComplex V) →
      (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' CategoryTheory.CategoryStruct.comp d₂ S.f = 0),
  (ChainComplex.mk X₀ X₁ X₂ d₀ d₁ s succ).X 1 = X₁
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.toSubfield_inj : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  {F E : IntermediateField K L}, F.toSubfield = E.toSubfield ↔ F = E
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.iInter_neg : ∀ {α : Type u_2} {ι : Sort u_5} [inst : Neg α] (s : ι → Set α), -⋂ i, s i = ⋂ i, -s i
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.coeffEquiv_symm_apply : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] (coeff : M →₀ R),
  MonoidAlgebra.coeffEquiv.symm coeff = MonoidAlgebra.ofCoeff coeff
-- Mathlib.Analysis.LocallyConvex.Bounded
/-- The von Neumann bornology defined by the von Neumann bounded sets.

Note that this is not registered as an instance, in order to avoid diamonds with the
metric bornology.  -/
Bornology.vonNBornology : (𝕜 : Type u_1) →
  (E : Type u_3) →
    [inst : NormedField 𝕜] →
      [inst_1 : AddCommGroup E] →
        [inst_2 : Module 𝕜 E] → [inst_3 : TopologicalSpace E] → [ContinuousSMul 𝕜 E] → Bornology E
-- Lean.Elab.BuiltinNotation
Lean.Elab.Term.elabSubst : Lean.Elab.Term.TermElab
-- Std.Data.DTreeMap.Raw.Iterator
_private.Std.Data.DTreeMap.Raw.Iterator.0.Std.DTreeMap.Raw.keysIter.eq_1 : ∀ {α : Type u} {β : α → Type u} {cmp : α → α → Ordering} (m : Std.DTreeMap.Raw α β cmp),
  m.keysIter = Std.Iter.map (fun e => e.fst) m.iter
-- Mathlib.Order.Interval.Set.Image
Set.image_subtype_val_Ioo_subset : ∀ {α : Type u_1} [inst : Preorder α] {p : α → Prop} (a b : { x // p x }), Subtype.val '' Set.Ioo a b ⊆ Set.Ioo ↑a ↑b
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.isBasis_self_iff_indep : ∀ {α : Type u_1} {M : Matroid α} {I : Set α}, M.IsBasis I I ↔ M.Indep I
-- Init.Data.Fin.Fold
Fin.foldl_rev : ∀ {n : ℕ} {α : Sort u_1} (f : Fin n → α → α) (x : α), Fin.foldl n (fun x i => f i.rev x) x = Fin.foldr n f x
-- Mathlib.Topology.Homeomorph.Lemmas
/-- A map from a compact space to a T2 space is a homeomorphism iff it is continuous and
bijective.  -/
isHomeomorph_iff_continuous_bijective : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} [CompactSpace X]
  [T2Space Y], IsHomeomorph f ↔ Continuous f ∧ Function.Bijective f
-- Mathlib.Algebra.Polynomial.Monic
/-- The image of a monic polynomial of degree `n` under a ring homomorphism.  -/
Polynomial.MonicDegreeEq.map : {R : Type u} →
  {S : Type v} →
    {n : ℕ} →
      [inst : Semiring R] →
        [inst_1 : Semiring S] → Polynomial.MonicDegreeEq R n → (R →+* S) → Polynomial.MonicDegreeEq S n
-- Mathlib.NumberTheory.Harmonic.EulerMascheroni
Real.eulerMascheroniConstant.eq_1 : Real.eulerMascheroniConstant = Filter.atTop.limUnder Real.eulerMascheroniSeq
-- Mathlib.Order.RelIso.Basic
RelIso.coe_copy : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (e : r ≃r s) (f : α → β) (g : β → α) (hf : f = ⇑e)
  (hg : g = ⇑e.symm), ⇑(e.copy f g hf hg) = f
-- Mathlib.CategoryTheory.LiftingProperties.Basic
/-- Given a morphism `φ : f ⟶ g` in the category `Arrow C`, this is an
abbreviation for the `CommSq.LiftStruct` structure for
the square corresponding to `φ`.  -/
CategoryTheory.Arrow.LiftStruct : {C : Type u_1} → [inst : CategoryTheory.Category.{v_1, u_1} C] → {f g : CategoryTheory.Arrow C} → (f ⟶ g) → Type v_1
-- Mathlib.GroupTheory.Coprod.Basic
AddEquiv.coprodPUnit_symm_apply : ∀ (M : Type u_1) [inst : AddMonoid M], ⇑(AddEquiv.coprodPUnit M).symm = ⇑AddMonoid.Coprod.inl