mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.List.Forall2
List.forall₂_cons_right_iff : ∀ {α : Type u_1} {β : Type u_2} {R : α → β → Prop} {b : β} {l : List β} {u : List α},
  List.Forall₂ R u (b :: l) ↔ ∃ a u', R a b ∧ List.Forall₂ R u' l ∧ u = a :: u'
-- Init.Data.String.Lemmas.Pattern.String.ForwardSearcher
_private.Init.Data.String.Lemmas.Pattern.String.ForwardSearcher.0.String.Slice.Pattern.Model.ForwardSliceSearcher.Invariants.isEmpty_eq_false : ∀ {pat s : String.Slice} {needlePos stackPos : String.Pos.Raw},
  String.Slice.Pattern.Model.ForwardSliceSearcher.Invariants✝ pat s needlePos stackPos → pat.isEmpty = false
-- Mathlib.Algebra.Group.Pi.Units
Pi.isUnit_iff : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] {x : (i : ι) → M i},
  IsUnit x ↔ ∀ (i : ι), IsUnit (x i)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.isSome_maxKey?_modify_eq_isSome : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {f : β → β}, (Std.DTreeMap.Raw.Const.modify t k f).maxKey?.isSome = t.maxKey?.isSome
-- Lean.Meta.Tactic.Simp.SimpCongrTheorems
Lean.Meta.instInhabitedSimpCongrTheorems.default : Lean.Meta.SimpCongrTheorems
-- Init.Data.Vector.Attach
Vector.pmap_mk : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {xs : Array α} {h : xs.size = n} {P : α → Prop} {f : (a : α) → P a → β}
  {H : ∀ a ∈ Vector.mk xs h, P a}, Vector.pmap f (Vector.mk xs h) H = Vector.mk (Array.pmap f xs ⋯) ⋯
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
/-- The connecting homomorphism `(t.truncGE b).obj X ⟶ ((t.truncLE a).obj X)⟦1⟧`
when `a + 1 = b`, as a natural transformation.  -/
CategoryTheory.Triangulated.TStructure.truncGEδLE : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        [inst_3 : CategoryTheory.HasShift C ℤ] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [inst_5 : CategoryTheory.Pretriangulated C] →
              (t : CategoryTheory.Triangulated.TStructure C) →
                (a b : ℤ) → a + 1 = b → (t.truncGE b ⟶ (t.truncLE a).comp (CategoryTheory.shiftFunctor C 1))
-- Mathlib.Probability.Independence.ZeroOne
ProbabilityTheory.CondIndepSet.congr_simp : ∀ {Ω : Type u_1} (m' m'_1 : MeasurableSpace Ω) (e_m' : m' = m'_1) {mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω]
  (hm' : m' ≤ mΩ) (s s_1 : Set Ω),
  s = s_1 →
    ∀ (t t_1 : Set Ω),
      t = t_1 →
        ∀ (μ μ_1 : MeasureTheory.Measure Ω) (e_μ : μ = μ_1) [inst_1 : MeasureTheory.IsFiniteMeasure μ],
          ProbabilityTheory.CondIndepSet m' hm' s t μ = ProbabilityTheory.CondIndepSet m'_1 ⋯ s_1 t_1 μ_1
-- Mathlib.Topology.Category.Profinite.EffectiveEpi
Profinite.instPreservesEffectiveEpisCompHausProfiniteToCompHaus : profiniteToCompHaus.PreservesEffectiveEpis
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.getContext : Lean.Meta.SimpM Lean.Meta.Simp.Context
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Products
CategoryTheory.Limits.piObjIso_hom_comp_π_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} D]
  {α : Type w} [inst_2 : CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete α) C]
  (f : α → CategoryTheory.Functor D C) (d : D) (s : α) {Z : C} (h : (f s).obj d ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.piObjIso f d).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π (fun s => (f s).obj d) s) h) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.Pi.π f s).app d) h
-- Mathlib.Algebra.Group.Subgroup.Lattice
/-- Subgroups of a group form a complete lattice.  -/
Subgroup.instCompleteLattice : {G : Type u_1} → [inst : Group G] → CompleteLattice (Subgroup G)
-- Mathlib.LinearAlgebra.Matrix.Hadamard
Matrix.one_hadamard : ∀ {α : Type u_1} {n : Type u_3} [inst : DecidableEq n] [inst_1 : MulZeroOneClass α] (M : Matrix n n α),
  Matrix.hadamard 1 M = Matrix.diagonal M.diag
-- Mathlib.LinearAlgebra.AffineSpace.Combination
/-- The weighted sum is unaffected by changing the weights to the
corresponding indicator function and adding points to the set.  -/
Finset.weightedVSub_indicator_subset : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] {ι : Type u_4} (w : ι → k) (p : ι → P) {s₁ s₂ : Finset ι},
  s₁ ⊆ s₂ → (s₁.weightedVSub p) w = (s₂.weightedVSub p) ((↑s₁).indicator w)
-- Mathlib.GroupTheory.Complement
Subgroup.isComplement_subgroup_left_iff_bijective : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} {T : Set G},
  Subgroup.IsComplement (↑H) T ↔ Function.Bijective (T.domRestrict Quotient.mk'')
-- Mathlib.Algebra.Ring.Parity
IsSquare.zero : ∀ {α : Type u_2} [inst : MulZeroClass α], IsSquare 0
-- Mathlib.Topology.MetricSpace.GromovHausdorff
/-- This is indeed an equivalence relation  -/
_private.Mathlib.Topology.MetricSpace.GromovHausdorff.0.GromovHausdorff.equivalence_isometryRel : Equivalence GromovHausdorff.IsometryRel✝
-- Mathlib.Topology.Algebra.Module.Spaces.WeakDual
instFunLikeWeakDual : (𝕜 : Type u_1) →
  (E : Type u_2) →
    [inst : CommSemiring 𝕜] →
      [inst_1 : TopologicalSpace 𝕜] →
        [inst_2 : ContinuousAdd 𝕜] →
          [inst_3 : ContinuousConstSMul 𝕜 𝕜] →
            [inst_4 : AddCommMonoid E] →
              [inst_5 : Module 𝕜 E] → [inst_6 : TopologicalSpace E] → FunLike (WeakDual 𝕜 E) E 𝕜
-- Mathlib.Order.CompleteLattice.Basic
iSup_sigma : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {p : β → Type u_8} {f : Sigma p → α},
  ⨆ x, f x = ⨆ i, ⨆ j, f ⟨i, j⟩
-- Mathlib.Algebra.Homology.Homotopy
/-- `f` is homotopic to `g` iff `f - g` is homotopic to `0`.
 -/
Homotopy.equivSubZero : {ι : Type u_1} →
  {V : Type u} →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Preadditive V] →
        {c : ComplexShape ι} → {C D : HomologicalComplex V c} → {f g : C ⟶ D} → Homotopy f g ≃ Homotopy (f - g) 0
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem_erase : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k a : α} {h' : a ∈ m.erase k}, (m.erase k)[a] = m[a]
-- Batteries.Data.HashMap.Basic
/-- Performs an in-place edit of the value, ensuring that the value is used linearly.
The function `f` is passed the original key of the entry, along with the value in the map.
```
(ofList [("one", 1), ("two", 2)]).modify "one" (fun _ v => v + 1) = {"one" => 2, "two" => 2}
(ofList [("one", 1), ("two", 2)]).modify "three" (fun _ v => v + 1) = {"one" => 1, "two" => 2}
```
 -/
Batteries.HashMap.modify : {α : Type u_1} →
  {x : BEq α} → {x_1 : Hashable α} → {β : Type u_2} → Batteries.HashMap α β → α → (α → β → β) → Batteries.HashMap α β
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equifibered
CategoryTheory.NatTrans.Coequifibered.unop : ∀ {J : Type u_1} {C : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_3} C] {F G : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ} {α : F ⟶ G},
  CategoryTheory.NatTrans.Coequifibered α → CategoryTheory.NatTrans.Equifibered (CategoryTheory.NatTrans.unop α)
-- Mathlib.LinearAlgebra.Matrix.Circulant
Matrix.Fin.circulant_inj : ∀ {α : Type u_1} {n : ℕ} {v w : Fin n → α}, Matrix.circulant v = Matrix.circulant w ↔ v = w
-- Mathlib.Analysis.InnerProductSpace.PiL2
EuclideanSpace.inner_basisFun_real : ∀ (ι : Type u_1) [inst : Fintype ι] (x : EuclideanSpace ℝ ι) (i : ι),
  inner ℝ x ((EuclideanSpace.basisFun ι ℝ) i) = x.ofLp i
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_roc_eq_toArray_rcc : ∀ {m n : ℕ}, (m<...=n).toArray = ((m + 1)...=n).toArray
-- Mathlib.CategoryTheory.Monoidal.Center
CategoryTheory.Center.Hom.mk.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {X Y : CategoryTheory.Center C} (f f_1 : X.fst ⟶ Y.fst) (e_f : f = f_1)
  (comm :
    ∀ (U : C),
      CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f U) (Y.snd.β U).hom =
        CategoryTheory.CategoryStruct.comp (X.snd.β U).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft U f)),
  { f := f, comm := comm } = { f := f_1, comm := ⋯ }
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
RCLike.nonUnitalContinuousFunctionalCalculus : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : RCLike 𝕜] [inst_1 : NonUnitalNormedRing A] [inst_2 : StarRing A]
  [inst_3 : NormedSpace 𝕜 A] [inst_4 : IsScalarTower 𝕜 A A] [inst_5 : SMulCommClass 𝕜 A A] [inst_6 : StarModule 𝕜 A]
  {p : A → Prop} {p₁ : Unitization 𝕜 A → Prop},
  (∀ {x : A}, p₁ ↑x ↔ p x) →
    ∀ [ClosedEmbeddingContinuousFunctionalCalculus 𝕜 (Unitization 𝕜 A) p₁] [CompleteSpace A] [CStarRing A],
      NonUnitalContinuousFunctionalCalculus 𝕜 A p
-- Lean.DeprecatedModule
Lean.Environment.setDeprecatedModule : Option Lean.DeprecatedModuleEntry → Lean.Environment → Lean.Environment
-- Init.Prelude
instHAndThenOfAndThen : {α : Type u_1} → [AndThen α] → HAndThen α α α
-- Mathlib.Probability.Kernel.Category.SFinKer
SFinKer.whiskerRight_hom : ∀ {X₁ X₂ : SFinKer} (κ : X₁ ⟶ X₂) (Y : SFinKer),
  (CategoryTheory.MonoidalCategoryStruct.whiskerRight κ Y).hom = κ.hom.parallelComp ProbabilityTheory.Kernel.id
-- Mathlib.Topology.Algebra.Group.ClosedSubgroup
ClosedSubgroup.isClosed' : ∀ {G : Type u} [inst : Group G] [inst_1 : TopologicalSpace G] (self : ClosedSubgroup G), IsClosed (↑self).carrier
-- Mathlib.ModelTheory.Substructures
/-- Turns any substructure containing a constant set `A` into a `L[[A]]`-substructure.  -/
FirstOrder.Language.Substructure.withConstants : {L : FirstOrder.Language} →
  {M : Type w} →
    [inst : L.Structure M] → (S : L.Substructure M) → {A : Set M} → A ⊆ ↑S → (L.withConstants ↑A).Substructure M
-- Init.Data.UInt.Lemmas
UInt8.sub_eq_add_mul : ∀ (a b : UInt8), a - b = a + 255 * b
-- Mathlib.Logic.Embedding.Basic
Function.Embedding.sectL_apply : ∀ (α : Type u_1) {β : Type u_2} (b : β) (a : α), (Function.Embedding.sectL α b) a = (a, b)
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.EqCnstrProof.refl.inj : ∀ {s s_1 : Lean.Grind.AC.Seq},
  Lean.Meta.Grind.AC.EqCnstrProof.refl s = Lean.Meta.Grind.AC.EqCnstrProof.refl s_1 → s = s_1
-- Mathlib.RingTheory.Jacobson.Ring
/-- If `K` is a Jacobson Noetherian ring, `A` a nontrivial `K`-algebra of finite type,
then any `K`-subfield of `A` is finite over `K`.  -/
finite_of_algHom_finiteType_of_isJacobsonRing : ∀ {K : Type u_1} {L : Type u_2} {A : Type u_3} [inst : CommRing K] [inst_1 : DivisionRing L] [inst_2 : CommRing A]
  [IsJacobsonRing K] [IsNoetherianRing K] [Nontrivial A] [inst_6 : Algebra K L] [inst_7 : Algebra K A]
  [Algebra.FiniteType K A] (f : L →ₐ[K] A), Module.Finite K L
-- Mathlib.Control.Monad.Cont
ContT.map : {r : Type u} → {m : Type u → Type v} → {α : Type w} → (m r → m r) → ContT r m α → ContT r m α
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.keysArray_insertIfNew_perm : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [inst : BEq α] [Std.TransCmp cmp]
  [Std.LawfulBEqCmp cmp] {k : α} {v : β k},
  (t.insertIfNew k v).keysArray.Perm (if k ∈ t then t.keysArray else t.keysArray.push k)
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Hom.eqToHom_app : ∀ {X Y : AlgebraicGeometry.Scheme} (e : X = Y) (U : Y.Opens),
  AlgebraicGeometry.Scheme.Hom.app (CategoryTheory.eqToHom e) U = CategoryTheory.eqToHom ⋯
-- Lean.Elab.InfoTree.Main
/-- Saves the current list of trees `t₀`, runs `x` to produce a new tree list `t₁` and
runs `mkInfoTree t₁` to get `n : InfoTree` and then restores the trees to be `t₀ ++ [n]`. -/
Lean.Elab.withInfoTreeContext : {m : Type → Type} →
  [Monad m] →
    [Lean.Elab.MonadInfoTree m] →
      {α : Type} → [MonadFinally m] → m α → (Lean.PersistentArray Lean.Elab.InfoTree → m Lean.Elab.InfoTree) → m α
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.mem_iff_isSome_getKey? : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {a : α}, a ∈ t ↔ (t.getKey? a).isSome = true
-- Mathlib.AlgebraicGeometry.Morphisms.Flat
/-- **Alias** of `AlgebraicGeometry.Scheme.Hom.flat_appLE`.

---

**Alias** of `AlgebraicGeometry.Flat.flat_appLE`. -/
AlgebraicGeometry.Flat.flat_of_affine_subset : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [self : AlgebraicGeometry.Flat f] {U : Y.Opens},
  AlgebraicGeometry.IsAffineOpen U →
    ∀ {V : X.Opens},
      AlgebraicGeometry.IsAffineOpen V →
        ∀ (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U),
          (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appLE f U V e)).Flat
-- Mathlib.Topology.FiberBundle.Constructions
Pullback.continuous_totalSpaceMk : ∀ {B : Type u} (F : Type v) (E : B → Type w₁) {B' : Type w₂} [inst : TopologicalSpace B']
  [inst_1 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_2 : TopologicalSpace F] [inst_3 : TopologicalSpace B]
  [inst_4 : (x : B) → TopologicalSpace (E x)] [FiberBundle F E] {f : B' → B} {x : B'},
  Continuous (Bundle.TotalSpace.mk x)
-- Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
HomotopicalAlgebra.CofibrantObject.instFullHoCatHoCatιCofibrantObject : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C],
  HomotopicalAlgebra.BifibrantObject.HoCat.ιCofibrantObject.Full
-- Mathlib.Order.OmegaCompletePartialOrder
/-- A chain is a monotone sequence.

This is made a one-field structure around order homomorphisms `ℕ →o α` because we want to endow
chains with the domination order rather than the pointwise order. See `Chain.instLE`.

See the definition on page 114 of [gunter1992].  -/
OmegaCompletePartialOrder.Chain : (α : Type u) → [Preorder α] → Type u
-- Mathlib.Analysis.Normed.Ring.Finite
AddChar.norm_apply : ∀ {α : Type u_1} [inst : NormedRing α] [NormMulClass α] [NormOneClass α] {G : Type u_3} [inst_3 : AddLeftCancelMonoid G]
  [Finite G] (ψ : AddChar G α) (x : G), ‖ψ x‖ = 1
-- Mathlib.NumberTheory.ModularForms.Cusps
CongruenceSubgroup.strictPeriods_Gamma0 : ∀ (N : ℕ),
  (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma0 N)).strictPeriods =
    AddSubgroup.zmultiples 1
-- Mathlib.CategoryTheory.Adjunction.Mates
/-- A component of a transposed version of the inverse mates correspondence.  -/
CategoryTheory.unit_mateEquiv_symm : ∀ {C : Type u₁} {D : Type u₂} {E : Type u₃} {F : Type u₄} [inst : CategoryTheory.Category.{v₁, u₁} C]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] [inst_2 : CategoryTheory.Category.{v₃, u₃} E]
  [inst_3 : CategoryTheory.Category.{v₄, u₄} F] {G : CategoryTheory.Functor C E} {H : CategoryTheory.Functor D F}
  {L₁ : CategoryTheory.Functor C D} {R₁ : CategoryTheory.Functor D C} {L₂ : CategoryTheory.Functor E F}
  {R₂ : CategoryTheory.Functor F E} (adj₁ : L₁ ⊣ R₁) (adj₂ : L₂ ⊣ R₂) (α : CategoryTheory.TwoSquare R₁ H G R₂) (c : C),
  CategoryTheory.CategoryStruct.comp (G.map (adj₁.unit.app c)) (α.app (L₁.obj c)) =
    CategoryTheory.CategoryStruct.comp (adj₂.unit.app (G.obj ((CategoryTheory.Functor.id C).obj c)))
      (R₂.map (((CategoryTheory.mateEquiv adj₁ adj₂).symm α).app ((CategoryTheory.Functor.id C).obj c)))
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.map₂_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  {F G : CategoryTheory.Functor C D} (η : F ⟶ G) (X : CategoryTheory.WithInitial C),
  (CategoryTheory.WithInitial.map₂ η).app X =
    match X with
    | CategoryTheory.WithInitial.of x => η.app x
    | CategoryTheory.WithInitial.star => CategoryTheory.CategoryStruct.id CategoryTheory.WithInitial.star
-- Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter
CategoryTheory.SimplicialObject.σ₀Iter_δ' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ}
  (i : Fin (n + 2)) (j : ℕ) {m : ℕ} (i' : Fin (m + 2))
  (h : autoParam (m + j = n) CategoryTheory.SimplicialObject.σ₀Iter_δ'._auto_1),
  autoParam (j < ↑i) CategoryTheory.SimplicialObject.σ₀Iter_δ'._auto_3 →
    autoParam (↑i = ↑i' + j) CategoryTheory.SimplicialObject.σ₀Iter_δ'._auto_5 →
      CategoryTheory.CategoryStruct.comp (X.σ₀Iter j ⋯) (X.δ i) =
        CategoryTheory.CategoryStruct.comp (X.δ i') (X.σ₀Iter j ⋯)
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.weekdayPairs : Vector String 7 → Array (String × Std.Time.Weekday)
-- Mathlib.Analysis.InnerProductSpace.PiL2
Complex.orthonormalBasisOneI.eq_1 : Complex.orthonormalBasisOneI = Complex.basisOneI.toOrthonormalBasis Complex.orthonormalBasisOneI._proof_1
-- Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
CochainComplex.triangleOfDegreewiseSplit_mor₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (S : CategoryTheory.ShortComplex (CochainComplex C ℤ))
  (σ : (n : ℤ) → (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n)).Splitting),
  (CochainComplex.triangleOfDegreewiseSplit S σ).mor₃ = CochainComplex.homOfDegreewiseSplit S σ
-- Mathlib.Algebra.Order.Ring.Opposite
MulOpposite.instIsOrderedRing : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : PartialOrder R] [IsOrderedRing R], IsOrderedRing Rᵐᵒᵖ
-- Mathlib.RingTheory.AlgebraTower
Module.Basis.isScalarTower_finsupp : ∀ (R : Type u_1) {S : Type u_2} {A : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : AddCommMonoid A]
  [inst_3 : Module R S] [inst_4 : Module S A] [inst_5 : Module R A] [IsScalarTower R S A] {ι : Type u_5}
  (b : Module.Basis ι S A), IsScalarTower R S (ι →₀ S)
-- Mathlib.Analysis.Normed.Group.Constructions
OrderDual.normedAddGroup.eq_1 : ∀ {E : Type u_2} [inst : NormedAddGroup E],
  OrderDual.normedAddGroup =
    { toNorm := OrderDual.toNorm, toAddGroup := OrderDual.instAddGroup, toMetricSpace := instMetricSpaceOrderDual,
      dist_eq := ⋯ }
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.ofArrows.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {ι : Type u_1} {Y : ι → C} {f : (i : ι) → Y i ⟶ X}
  (i : ι), CategoryTheory.Presieve.ofArrows Y f (f i)
-- Init.Prelude
Lean.instMonadQuotationOfMonadFunctorOfMonadLift : {m n : Type → Type} → [MonadFunctor m n] → [MonadLift m n] → [Lean.MonadQuotation m] → Lean.MonadQuotation n
-- Mathlib.CategoryTheory.LocallyDirected
CategoryTheory.Functor.IsLocallyDirected.cond : ∀ {J : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} J} (F : CategoryTheory.Functor J (Type u_2))
  [self : F.IsLocallyDirected] {i j k : J} (fi : i ⟶ k) (fj : j ⟶ k) (xi : F.obj i) (xj : F.obj j),
  (CategoryTheory.ConcreteCategory.hom (F.map fi)) xi = (CategoryTheory.ConcreteCategory.hom (F.map fj)) xj →
    ∃ l fli flj x,
      (CategoryTheory.ConcreteCategory.hom (F.map fli)) x = xi ∧
        (CategoryTheory.ConcreteCategory.hom (F.map flj)) x = xj
-- Lean.Meta.Tactic.Try.Collect
Lean.Meta.Try.Collector.saveUnfoldCandidate : Lean.Name → Lean.Meta.Try.Collector.M Unit
-- Lean.Elab.Do.Basic
_private.Lean.Elab.Do.Basic.0.Lean.Elab.Do.bindMutVarsFromTuple.go : Lean.Elab.Do.DoElabM Lean.Expr →
  List Lean.Name → Lean.FVarId → Lean.Expr → Array Lean.Expr → Lean.Elab.Do.DoElabM Lean.Expr
-- Mathlib.Order.Interval.Set.UnorderedInterval
Set.uIoc_eq_union : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, Set.uIoc a b = Set.Ioc a b ∪ Set.Ioc b a
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
Lean.Meta.Grind.Arith.Cutsat.ToIntM : Type → Type
-- Mathlib.RingTheory.TensorProduct.Maps
/-- `rTensor B f : A ⊗ B →ₐ C ⊗ B` is the natural algebra morphism induced by `f : A →ₐ C`.  -/
Algebra.TensorProduct.rTensor : {R : Type uR} →
  {S : Type uS} →
    {A : Type uA} →
      (B : Type uB) →
        {C : Type uC} →
          [inst : CommSemiring R] →
            [inst_1 : CommSemiring S] →
              [inst_2 : Algebra R S] →
                [inst_3 : Semiring A] →
                  [inst_4 : Algebra R A] →
                    [inst_5 : Algebra S A] →
                      [inst_6 : IsScalarTower R S A] →
                        [inst_7 : Semiring B] →
                          [inst_8 : Algebra R B] →
                            [inst_9 : Semiring C] →
                              [inst_10 : Algebra R C] →
                                [inst_11 : Algebra S C] →
                                  [inst_12 : IsScalarTower R S C] →
                                    (A →ₐ[S] C) → TensorProduct R A B →ₐ[S] TensorProduct R C B
-- Mathlib.AlgebraicGeometry.Morphisms.Constructors
AlgebraicGeometry.HasAffineProperty.diagonal_of_diagonal_of_isPullback : ∀ (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) {Q : AlgebraicGeometry.AffineTargetMorphismProperty}
  [AlgebraicGeometry.HasAffineProperty P Q] {X Y U V : AlgebraicGeometry.Scheme} {f : X ⟶ Y} {g : U ⟶ Y}
  [inst : AlgebraicGeometry.IsAffine U] [AlgebraicGeometry.IsOpenImmersion g] {iV : V ⟶ X} {f' : V ⟶ U},
  CategoryTheory.IsPullback iV f' f g → P.diagonal f → Q.diagonal f'
-- Mathlib.Tactic.Translate.Reorder
Mathlib.Tactic.Translate.ArgReorder.instBEq : BEq Mathlib.Tactic.Translate.ArgReorder
-- Mathlib.Topology.UrysohnsLemma
exists_continuous_nonneg_pos : ∀ {X : Type u_1} [inst : TopologicalSpace X] [RegularSpace X] [LocallyCompactSpace X] (x : X),
  ∃ f, HasCompactSupport ⇑f ∧ 0 ≤ ⇑f ∧ f x ≠ 0
-- Mathlib.LinearAlgebra.TensorProduct.Defs
IsAddUnit.tmul_left : ∀ (R : Type u_1) [inst : CommSemiring R] {M : Type u_7} {N : Type u_8} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] {n : N},
  IsAddUnit n → ∀ (m : M), IsAddUnit (m ⊗ₜ[R] n)
-- Mathlib.CategoryTheory.Bicategory.SingleObj
CategoryTheory.MonoidalSingleObj.endMonoidalStarFunctor_isEquivalence : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C],
  (CategoryTheory.MonoidalSingleObj.endMonoidalStarFunctor C).IsEquivalence
-- Mathlib.AlgebraicGeometry.Properties
AlgebraicGeometry.isReduced_stalk_of_isReduced : ∀ (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsReduced X] (x : ↥X), IsReduced ↑(X.presheaf.stalk x)
-- Mathlib.Tactic.Linter.TextBased
_private.Mathlib.Tactic.Linter.TextBased.0.Mathlib.Linter.TextBased.ErrorContext.mk.inj : ∀ {error : Mathlib.Linter.TextBased.StyleError✝} {lineNumber : ℕ} {path : System.FilePath}
  {error_1 : Mathlib.Linter.TextBased.StyleError✝} {lineNumber_1 : ℕ} {path_1 : System.FilePath},
  { error := error, lineNumber := lineNumber, path := path } =
      { error := error_1, lineNumber := lineNumber_1, path := path_1 } →
    error = error_1 ∧ lineNumber = lineNumber_1 ∧ path = path_1
-- Mathlib.CategoryTheory.Subobject.MonoOver
/-- The category of monomorphisms over X is a thin category,
which makes defining its skeleton easy.  -/
CategoryTheory.MonoOver.isThin : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C}, Quiver.IsThin (CategoryTheory.MonoOver X)
-- Mathlib.RingTheory.Flat.Tensor
/-- `CharacterModule M` is Baer iff `M` is flat.  -/
Module.Flat.iff_characterModule_baer : ∀ {R : Type u} {M : Type v} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  Module.Flat R M ↔ Module.Baer R (CharacterModule M)
-- Mathlib.Topology.Neighborhoods
/-- If `U` is a neighborhood of each point of a set `s` then it is a neighborhood of `s`:
it contains an open set containing `s`.  -/
exists_open_set_nhds : ∀ {X : Type u} [inst : TopologicalSpace X] {s U : Set X}, (∀ x ∈ s, U ∈ nhds x) → ∃ V, s ⊆ V ∧ IsOpen V ∧ V ⊆ U
-- Mathlib.CategoryTheory.Types.Basic
CategoryTheory.FunctorToTypes.comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F G H : CategoryTheory.Functor C (Type w)) {X : C} (σ : F ⟶ G)
  (τ : G ⟶ H) (x : F.obj X),
  (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.CategoryStruct.comp σ τ).app X)) x =
    (CategoryTheory.ConcreteCategory.hom (τ.app X)) ((CategoryTheory.ConcreteCategory.hom (σ.app X)) x)
-- Mathlib.Topology.EMetricSpace.Pi
edist_pi_def : ∀ {β : Type v} {X : β → Type u_2} [inst : Fintype β] [inst_1 : (b : β) → EDist (X b)] (f g : (b : β) → X b),
  edist f g = Finset.univ.sup fun b => edist (f b) (g b)
-- Lean.Meta.Sym.SymM
/-- Returns `true` if `e` is the internalized `True` expression.   -/
Lean.Meta.Sym.isTrueExpr : Lean.Expr → Lean.Meta.Sym.SymM Bool