mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.HasLimits
/-- We can transport colimits of shape `J` along an equivalence `J ≌ J'`.
 -/
CategoryTheory.Limits.hasColimitsOfShape_of_equivalence : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {J' : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} J'] (e : J ≌ J')
  [CategoryTheory.Limits.HasColimitsOfShape J C], CategoryTheory.Limits.HasColimitsOfShape J' C
-- Mathlib.LinearAlgebra.AffineSpace.Ordered
lineMap_mono_endpoints : ∀ {k : Type u_1} {E : Type u_2} [inst : Ring k] [inst_1 : PartialOrder k] [IsOrderedRing k] [inst_3 : AddCommGroup E]
  [inst_4 : PartialOrder E] [IsOrderedAddMonoid E] [inst_6 : Module k E] [IsStrictOrderedModule k E] {a a' b b' : E}
  {r : k}, a ≤ a' → b ≤ b' → 0 ≤ r → r ≤ 1 → (AffineMap.lineMap a b) r ≤ (AffineMap.lineMap a' b') r
-- Mathlib.Tactic.Linter.Style
/-- The `lambdaSyntax` linter flags uses of the symbol `λ` to define anonymous functions.
This is syntactically equivalent to the `fun` keyword; mathlib style prefers using the latter.
 -/
_private.Mathlib.Tactic.Linter.Style.0.Mathlib.Linter.Style.lambdaSyntax.lambdaSyntaxLinter : Lean.Linter
-- Mathlib.Data.List.Sigma
List.sublist_dlookup : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {l₁ l₂ : List (Sigma β)} {a : α} {b : β a},
  l₂.NodupKeys → l₁.Sublist l₂ → b ∈ List.dlookup a l₁ → b ∈ List.dlookup a l₂
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
/-- Graph homomorphisms induce a covariant function on subgraphs.  -/
SimpleGraph.Subgraph.map : {V : Type u} → {W : Type v} → {G : SimpleGraph V} → {G' : SimpleGraph W} → G →g G' → G.Subgraph → G'.Subgraph
-- Init.Meta.Defs
Lean.isSubScriptAlnum : Char → Bool
-- Mathlib.Geometry.Manifold.SmoothEmbedding
Manifold.IsSmoothEmbedding.id : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E₁ : Type u_2} [inst_1 : NormedAddCommGroup E₁]
  [inst_2 : NormedSpace 𝕜 E₁] {H : Type u_6} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E₁ H} {M : Type u_10}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {n : WithTop ℕ∞} [IsManifold I n M],
  Manifold.IsSmoothEmbedding I I n id
-- Lean.Elab.Term.TermElabM
Lean.Elab.Tactic.TacticParsedSnapshot.mk.sizeOf_spec : ∀
  (transformed :
    Lean.Language.TransformedSnap (Lean.Elab.Tactic.TacticParsedSnapshotInner Lean.Elab.Tactic.TacticParsedSnapshot))
  (next : Array (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot)),
  sizeOf { transformed := transformed, next := next } = 1 + sizeOf transformed + sizeOf next
-- Mathlib.LinearAlgebra.Isomorphisms
/-- Essentially the same equivalence as in the third isomorphism theorem,
except restated in terms of suprema/addition of submodules instead of `≤`.  -/
Submodule.quotientQuotientEquivQuotientSup : {R : Type u_1} →
  {M : Type u_2} →
    [inst : Ring R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] → (S T : Submodule R M) → ((M ⧸ S) ⧸ Submodule.map S.mkQ T) ≃ₗ[R] M ⧸ S ⊔ T
-- Mathlib.Probability.Decision.BayesEstimator
/-- We say that a measurable function `f : 𝓧 → 𝓨` is an argmin estimator
with respect to the prior `π` if for `(P ∘ₘ π)`-almost every `x` it is of
the form `x ↦ argmin_y P†π(x)[θ ↦ ℓ θ y]`.  -/
ProbabilityTheory.IsArgminEstimator : {Θ : Type u_1} →
  {𝓧 : Type u_2} →
    {mΘ : MeasurableSpace Θ} →
      {m𝓧 : MeasurableSpace 𝓧} →
        [StandardBorelSpace Θ] →
          [Nonempty Θ] →
            {𝓨 : Type u_4} →
              [MeasurableSpace 𝓨] →
                (Θ → 𝓨 → ENNReal) →
                  (P : ProbabilityTheory.Kernel Θ 𝓧) →
                    [ProbabilityTheory.IsFiniteKernel P] →
                      (π : MeasureTheory.Measure Θ) → [MeasureTheory.IsFiniteMeasure π] → (𝓧 → 𝓨) → Prop
-- Mathlib.Order.Filter.Bases.Basic
FilterBasis.hasBasis : ∀ {α : Type u_1} (B : FilterBasis α), B.filter.HasBasis (fun s => s ∈ B) id
-- Mathlib.Algebra.Ring.BooleanRing
instZeroBool_mathlib : Zero Bool
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.ext_of_isTriangulatedClosed₃' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} 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]
  (P : CategoryTheory.ObjectProperty C) [P.IsTriangulatedClosed₃],
  ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles, P T.obj₁ → P T.obj₂ → P.isoClosure T.obj₃
-- Init.Data.Nat.Lemmas
Nat.mod_eq_sub_iff : ∀ {a b c : ℕ}, 0 < c → c ≤ b → (a % b = b - c ↔ b ∣ a + c)
-- Mathlib.Algebra.Regular.ULift
ULift.isSMulRegular_iff : ∀ {α : Type u_1} {R : Type v} [inst : SMul α R] {r : α}, IsSMulRegular (ULift.{u_2, v} R) r ↔ IsSMulRegular R r
-- Mathlib.FieldTheory.IsAlgClosed.Spectrum
IsIdempotentElem.spectrum_subset : ∀ (𝕜 : Type u_1) {A : Type u_2} [inst : Field 𝕜] [inst_1 : Ring A] [inst_2 : Algebra 𝕜 A] {p : A},
  IsIdempotentElem p → spectrum 𝕜 p ⊆ {0, 1}
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get!_erase_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k : α} [inst_1 : Inhabited (β k)], (t.erase k).get! k = default
-- Batteries.Data.String.Legacy
/-- Auxuliary definition for `String.Legacy.any`.

This is an old implementation, preserved here for users of the lemmas in
`Batteries.Data.String.Lemmas`.
 -/
String.Legacy.anyAux : String → String.Pos.Raw → (Char → Bool) → String.Pos.Raw → Bool
-- Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
RootPairing.posRootForm_posForm_apply_apply : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (S : Type u_5)
  [inst_5 : CommRing S] [inst_6 : LinearOrder S] [inst_7 : IsStrictOrderedRing S] [inst_8 : Algebra S R]
  [inst_9 : FaithfulSMul S R] [inst_10 : Module S M] [inst_11 : IsScalarTower S R M] [inst_12 : P.IsValuedIn S]
  [inst_13 : Fintype ι] (x y : ↥(P.rootSpan S)),
  ((P.posRootForm S).posForm x) y = ∑ i, (P.coroot'In S i) x * (P.coroot'In S i) y
-- Mathlib.CategoryTheory.Types.Basic
/-- The functor embedding `Type u` into `Type u` via `ULift` is isomorphic to the identity functor.
 -/
CategoryTheory.uliftFunctorTrivial : CategoryTheory.uliftFunctor.{u, u} ≅ CategoryTheory.Functor.id (Type u)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
CategoryTheory.Limits.preservesLimitsOfShape_walkingCospan_of_forall_isPullback : ∀ {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 Z : C⦄ (f : X ⟶ Z) (g : Y ⟶ Z) [CategoryTheory.Limits.HasPullback f g],
      ∃ P fst snd,
        CategoryTheory.IsPullback fst snd f g ∧ CategoryTheory.IsPullback (F.map fst) (F.map snd) (F.map f) (F.map g)) →
    CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan F
-- Mathlib.MeasureTheory.Group.Prod
/-- The map `(x, y) ↦ (xy, y)` preserves the measure `μ × ν`.  -/
MeasureTheory.measurePreserving_mul_prod : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [MeasurableMul₂ G] (μ ν : MeasureTheory.Measure G)
  [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] [μ.IsMulRightInvariant],
  MeasureTheory.MeasurePreserving (fun z => (z.1 * z.2, z.2)) (μ.prod ν) (μ.prod ν)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
CategoryTheory.CostructuredArrow.grothendieckProj_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (L : CategoryTheory.Functor C D) (X : CategoryTheory.Grothendieck (CategoryTheory.CostructuredArrow.functor L)),
  (CategoryTheory.CostructuredArrow.grothendieckProj L).obj X = CategoryTheory.CostructuredArrow.left X.fiber
-- Init.Data.Order.FactoriesExtra
/-- The `LT α` instance obtained from an `Ord α` instance is compatible with the `LE α` instance
instance if `Ord α` is compatible with it.
 -/
Std.instLawfulOrderLT_ofOrd : ∀ {α : Type u} [inst : Ord α] [inst_1 : LE α] [Std.LawfulOrderOrd α], Std.LawfulOrderLT α
-- Mathlib.Topology.Category.TopCat.Limits.Pullbacks
TopCat.pullback_topology : ∀ {X Y Z : TopCat} (f : X ⟶ Z) (g : Y ⟶ Z),
  (CategoryTheory.Limits.pullback f g).str =
    TopologicalSpace.induced (⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.fst f g))) X.str ⊓
      TopologicalSpace.induced (⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.snd f g))) Y.str
-- Mathlib.GroupTheory.OrderOfElement
finEquivZMultiples_symm_apply : ∀ {G : Type u_1} [inst : AddGroup G] {x : G} (hx : IsOfFinAddOrder x) (n : ℕ),
  (finEquivZMultiples hx).symm ⟨n • x, ⋯⟩ = ⟨n % addOrderOf x, ⋯⟩
-- Mathlib.Data.List.Cycle
Cycle.Subsingleton.eq_1 : ∀ {α : Type u_1} (s : Cycle α), s.Subsingleton = (s.length ≤ 1)
-- Mathlib.Topology.UnitInterval
/-- Helper definition for `convexComb_assoc'`, giving one of the coefficients appearing
when we reassociate a convex combination in the reverse direction.
 -/
Set.Icc.convexComb_assoc_coeff₂' : ↑unitInterval → ↑unitInterval → ↑unitInterval
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Closeds.instSProdProd : {α : Type u_2} →
  {β : Type u_3} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        SProd (TopologicalSpace.Closeds α) (TopologicalSpace.Closeds β) (TopologicalSpace.Closeds (α × β))
-- Mathlib.Data.Finset.Pi
/-- Given a function `f` defined on a finset `s`, define a new function on the finset `s ∪ {a}`,
equal to `f` on `s` and sending `a` to a given value `b`. This function is denoted
`s.Pi.cons a b f`. If `a` already belongs to `s`, the new function takes the value `b` at `a`
anyway.  -/
Finset.Pi.cons : {α : Type u_1} →
  {δ : α → Sort v} →
    [inst : DecidableEq α] →
      (s : Finset α) → (a : α) → δ a → ((a : α) → a ∈ s → δ a) → (a' : α) → a' ∈ insert a s → δ a'
-- Mathlib.Algebra.Divisibility.Basic
instIsPreorderRightDvd : ∀ {α : Type u_1} [inst : Monoid α], IsPreorder α RightDvd
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
AbsoluteValue.mk.injEq : ∀ {R : Type u_5} {S : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : PartialOrder S] (toMulHom : R →ₙ* S)
  (nonneg' : ∀ (x : R), 0 ≤ toMulHom.toFun x) (eq_zero' : ∀ (x : R), toMulHom.toFun x = 0 ↔ x = 0)
  (add_le' : ∀ (x y : R), toMulHom.toFun (x + y) ≤ toMulHom.toFun x + toMulHom.toFun y) (toMulHom_1 : R →ₙ* S)
  (nonneg'_1 : ∀ (x : R), 0 ≤ toMulHom_1.toFun x) (eq_zero'_1 : ∀ (x : R), toMulHom_1.toFun x = 0 ↔ x = 0)
  (add_le'_1 : ∀ (x y : R), toMulHom_1.toFun (x + y) ≤ toMulHom_1.toFun x + toMulHom_1.toFun y),
  ({ toMulHom := toMulHom, nonneg' := nonneg', eq_zero' := eq_zero', add_le' := add_le' } =
      { toMulHom := toMulHom_1, nonneg' := nonneg'_1, eq_zero' := eq_zero'_1, add_le' := add_le'_1 }) =
    (toMulHom = toMulHom_1)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
/-- Resets the assignment of any variable bigger or equal to `x`.  -/
Lean.Meta.Grind.Arith.Cutsat.resetAssignmentFrom : Int.Internal.Linear.Var → Lean.Meta.Grind.GoalM Unit
-- Mathlib.RingTheory.Ideal.MinimalPrime.Localization
IsLocalization.minimalPrimes_comap : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) (A : Type u_2) [inst_1 : CommSemiring A]
  [inst_2 : Algebra R A] [IsLocalization S A] (J : Ideal A),
  (Ideal.comap (algebraMap R A) J).minimalPrimes = Ideal.comap (algebraMap R A) '' J.minimalPrimes
-- Mathlib.CategoryTheory.Sites.Coherent.Equivalence
CategoryTheory.Equivalence.sheafCongrPrecoherent_unitIso_inv_app_hom_app : ∀ {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] [inst_2 : CategoryTheory.Precoherent C] (A : Type u_3)
  [inst_3 : CategoryTheory.Category.{v_3, u_3} A] (e : C ≌ D)
  (X : CategoryTheory.Sheaf (CategoryTheory.coherentTopology C) A) (X_1 : Cᵒᵖ),
  ((CategoryTheory.Equivalence.sheafCongrPrecoherent A e).unitIso.inv.app X).hom.app X_1 =
    X.obj.map (e.unitIso.hom.app (Opposite.unop X_1)).op
-- Mathlib.Order.BooleanAlgebra.Basic
inf_sdiff_eq_bot_iff : ∀ {α : Type u} {x y z : α} [inst : GeneralizedBooleanAlgebra α], z ≤ y → x ≤ y → (z ⊓ y \ x = ⊥ ↔ z ≤ x)
-- Mathlib.GroupTheory.GroupExtension.Defs
/-- The inclusion homomorphism `N →* E`  -/
GroupExtension.inl : {N : Type u_1} →
  {E : Type u_2} →
    {G : Type u_3} → [inst : Group N] → [inst_1 : Group E] → [inst_2 : Group G] → GroupExtension N E G → N →* E
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
CategoryTheory.IsPullback.isoIsPullback_hom_snd_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : C} (X Y : C) {Z : C} {fst : P ⟶ X} {snd : P ⟶ Y}
  {f : X ⟶ Z} {g : Y ⟶ Z} {P' : C} {fst' : P' ⟶ X} {snd' : P' ⟶ Y} (h : CategoryTheory.IsPullback fst snd f g)
  (h' : CategoryTheory.IsPullback fst' snd' f g) {Z_1 : C} (h_1 : Y ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.IsPullback.isoIsPullback X Y h h').hom
      (CategoryTheory.CategoryStruct.comp snd' h_1) =
    CategoryTheory.CategoryStruct.comp snd h_1
-- Mathlib.Analysis.Convex.SimplicialComplex.Basic
Geometry.SimplicialComplex.vertices_subset_space : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] {K : Geometry.SimplicialComplex 𝕜 E}, K.vertices ⊆ K.space
-- Mathlib.GroupTheory.Congruence.Defs
/-- The supremum of a set of additive congruence relations is the same as the smallest
additive congruence relation containing the supremum of the set's image under the map to the
underlying binary relation.  -/
AddCon.sSup_def : ∀ {M : Type u_1} [inst : Add M] (S : Set (AddCon M)), sSup S = addConGen (sSup (DFunLike.coe '' S))
-- Mathlib.Algebra.Star.Subalgebra
/-- Preimage of a star subalgebra under a star algebra homomorphism.  -/
StarSubalgebra.comap : {R : Type u_2} →
  {A : Type u_3} →
    {B : Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : StarRing R] →
          [inst_2 : Semiring A] →
            [inst_3 : StarRing A] →
              [inst_4 : Algebra R A] →
                [inst_5 : StarModule R A] →
                  [inst_6 : Semiring B] →
                    [inst_7 : StarRing B] →
                      [inst_8 : Algebra R B] →
                        [inst_9 : StarModule R B] → (A →⋆ₐ[R] B) → StarSubalgebra R B → StarSubalgebra R A
-- Mathlib.Order.InitialSeg
PrincipalSeg.mk.injEq : ∀ {α : Type u_4} {β : Type u_5} {r : α → α → Prop} {s : β → β → Prop} (toRelEmbedding : r ↪r s) (top : β)
  (mem_range_iff_rel' : ∀ (b : β), b ∈ Set.range ⇑toRelEmbedding ↔ s b top) (toRelEmbedding_1 : r ↪r s) (top_1 : β)
  (mem_range_iff_rel'_1 : ∀ (b : β), b ∈ Set.range ⇑toRelEmbedding_1 ↔ s b top_1),
  ({ toRelEmbedding := toRelEmbedding, top := top, mem_range_iff_rel' := mem_range_iff_rel' } =
      { toRelEmbedding := toRelEmbedding_1, top := top_1, mem_range_iff_rel' := mem_range_iff_rel'_1 }) =
    (toRelEmbedding = toRelEmbedding_1 ∧ top = top_1)
-- Mathlib.Data.Set.Lattice
Set.sInter_eq_empty_iff : ∀ {α : Type u_1} {c : Set (Set α)}, ⋂₀ c = ∅ ↔ ∀ (a : α), ∃ b ∈ c, a ∉ b
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.Prequotient.mul.injEq : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat}
  (a a_1 a_2 a_3 : CommRingCat.Colimits.Prequotient F), (a.mul a_1 = a_2.mul a_3) = (a = a_2 ∧ a_1 = a_3)
-- Init.Data.UInt.Lemmas
UInt16.toUInt32_mod : ∀ (a b : UInt16), (a % b).toUInt32 = a.toUInt32 % b.toUInt32
-- Lean.Elab.PreDefinition.Structural.IndGroupInfo
Lean.Elab.Structural.instInhabitedIndGroupInfo : Inhabited Lean.Elab.Structural.IndGroupInfo
-- Mathlib.Geometry.Diffeology.Basic
Diffeology.dSmooth_iff_contDiff : ∀ {X : Type u_1} [inst : DiffeologicalSpace X] {Y : Type u_2} [inst_1 : NormedAddCommGroup X] [inst_2 : NormedSpace ℝ X]
  [Diffeology.IsContDiffCompatible X] [inst_4 : NormedAddCommGroup Y] [inst_5 : NormedSpace ℝ Y]
  [inst_6 : DiffeologicalSpace Y] [Diffeology.IsContDiffCompatible Y] [FiniteDimensional ℝ X] {f : X → Y},
  Diffeology.DSmooth f ↔ ContDiff ℝ (↑⊤) f
-- Mathlib.Algebra.Homology.SpectralSequence.Basic
CategoryTheory.SpectralSequence.pageFunctor.congr_simp : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{u_3, u_1} C] [inst_1 : CategoryTheory.Abelian C] {κ : Type u_2}
  (c : ℤ → ComplexShape κ) (r₀ r : ℤ) (hr : r₀ ≤ r),
  CategoryTheory.SpectralSequence.pageFunctor C c r₀ r hr = CategoryTheory.SpectralSequence.pageFunctor C c r₀ r hr
-- Mathlib.FieldTheory.PerfectClosure
PerfectClosure.instField : (K : Type u) →
  [inst : Field K] → (p : ℕ) → [inst_1 : Fact (Nat.Prime p)] → [inst_2 : CharP K p] → Field (PerfectClosure K p)
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.eTruncGEπ_naturality_assoc : ∀ {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) (i : EInt) {X Y : C} (f : X ⟶ Y) {Z : C}
  (h : (t.eTruncGE.obj i).obj Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((t.eTruncGEπ i).app X)
      (CategoryTheory.CategoryStruct.comp ((t.eTruncGE.obj i).map f) h) =
    CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp ((t.eTruncGEπ i).app Y) h)
-- Mathlib.Probability.Process.Stopping
MeasureTheory.IsStoppingTime.measurableSet_inter_le : ∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : LinearOrder ι] {f : MeasureTheory.Filtration ι m}
  {τ π : Ω → WithTop ι} [inst_1 : TopologicalSpace ι] [SecondCountableTopology ι] [OrderTopology ι]
  (hτ : MeasureTheory.IsStoppingTime f τ) (hπ : MeasureTheory.IsStoppingTime f π) (s : Set Ω),
  MeasurableSet s → MeasurableSet (s ∩ {ω | τ ω ≤ π ω})
-- Mathlib.Algebra.Group.Subgroup.Defs
/-- Construct a subgroup from a nonempty set that is closed under division.  -/
Subgroup.ofDiv : {G : Type u_1} → [inst : Group G] → (s : Set G) → s.Nonempty → (∀ x ∈ s, ∀ y ∈ s, x * y⁻¹ ∈ s) → Subgroup G
-- Mathlib.Topology.Order.OrderClosed
nhdsWithin_Icc_eq_nhdsGE : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [ClosedIciTopology α] {a b : α},
  b < a → nhdsWithin b (Set.Icc b a) = nhdsWithin b (Set.Ici b)
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SetLike.addUnits_vadd : ∀ {S : Type u_1} {R : Type u_2} {M : Type u_3} [inst : SetLike S M] [inst_1 : AddMonoid R] [inst_2 : AddAction R M]
  [VAddMemClass S R M] (s : S) (r : AddUnits R), r +ᵥ ↑s = ↑s
-- Mathlib.Tactic.ReduceModChar
/-- Determine the characteristic of a ring from the type.
This should be fast, so this pattern-matches on the type, rather than searching for a
`CharP` instance.
Use `typeToCharP (expensive := true)` to do more work in finding the characteristic,
in particular it will search for a `CharP` instance in the context.  -/
Tactic.ReduceModChar.typeToCharP : {u : Lean.Level} → optParam Bool false → (t : Q(Type u)) → Lean.MetaM (Tactic.ReduceModChar.TypeToCharPResult t)
-- Mathlib.Algebra.Lie.IdealOperations
LieIdeal.comap_bracket_eq : ∀ {R : Type u} {L : Type v} {L' : Type w₂} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : LieRing L'] [inst_4 : LieAlgebra R L'] {f : L →ₗ⁅R⁆ L'} {J₁ J₂ : LieIdeal R L'},
  f.IsIdealMorphism →
    LieIdeal.comap f ⁅f.idealRange ⊓ J₁, f.idealRange ⊓ J₂⁆ = ⁅LieIdeal.comap f J₁, LieIdeal.comap f J₂⁆ ⊔ f.ker
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.BinaryBiconeMorphism.mk : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {P Q : C} →
        {A B : CategoryTheory.Limits.BinaryBicone P Q} →
          (hom : A.pt ⟶ B.pt) →
            autoParam (CategoryTheory.CategoryStruct.comp hom B.fst = A.fst)
                CategoryTheory.Limits.BinaryBiconeMorphism.wfst._autoParam →
              autoParam (CategoryTheory.CategoryStruct.comp hom B.snd = A.snd)
                  CategoryTheory.Limits.BinaryBiconeMorphism.wsnd._autoParam →
                autoParam (CategoryTheory.CategoryStruct.comp A.inl hom = B.inl)
                    CategoryTheory.Limits.BinaryBiconeMorphism.winl._autoParam →
                  autoParam (CategoryTheory.CategoryStruct.comp A.inr hom = B.inr)
                      CategoryTheory.Limits.BinaryBiconeMorphism.winr._autoParam →
                    CategoryTheory.Limits.BinaryBiconeMorphism A B
-- Mathlib.LinearAlgebra.Alternating.Basic
/-- Given an alternating `R`-multilinear map `f` taking values in `R`, `f.smul_right z` is the map
sending `m` to `f m • z`.  -/
AlternatingMap.smulRight : {R : Type u_10} →
  {M₁ : Type u_11} →
    {M₂ : Type u_12} →
      {ι : Type u_13} →
        [inst : CommSemiring R] →
          [inst_1 : AddCommMonoid M₁] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : Module R M₁] → [inst_4 : Module R M₂] → M₁ [⋀^ι]→ₗ[R] R → M₂ → M₁ [⋀^ι]→ₗ[R] M₂
-- Mathlib.ModelTheory.Satisfiability
FirstOrder.Language.Theory.exists_model_card_eq : ∀ {L : FirstOrder.Language} {T : L.Theory},
  (∃ M, Infinite ↑M) →
    ∀ (κ : Cardinal.{w}),
      Cardinal.aleph0 ≤ κ → Cardinal.lift.{w, max u v} L.card ≤ Cardinal.lift.{max u v, w} κ → ∃ N, Cardinal.mk ↑N = κ
-- Mathlib.Algebra.Group.Submonoid.Support
/-- **Alias** of the reverse direction of `isMulPointed_iff_mulSupport_eq_bot`. -/
Submonoid.IsMulPointed.of_mulSupport_eq_bot : ∀ {G : Type u_1} [inst : Group G] {M : Submonoid G}, M.mulSupport = ⊥ → M.IsMulPointed
-- Mathlib.Analysis.Normed.Field.UnitBall
/-- Unit sphere in a seminormed ring (with strictly multiplicative norm) as a bundled
`Submonoid`.  -/
Submonoid.unitSphere : (𝕜 : Type u_2) → [inst : SeminormedRing 𝕜] → [NormMulClass 𝕜] → [NormOneClass 𝕜] → Submonoid 𝕜
-- Mathlib.Algebra.Group.Hom.Defs
instInhabitedAddHom.eq_1 : ∀ {M : Type u_4} {N : Type u_5} [inst : Add M] [inst_1 : AddZeroClass N], instInhabitedAddHom = { default := 0 }
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get_eq_get : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  t.WF →
    ∀ {a : α} {h : Std.DTreeMap.Internal.Impl.contains a t = true},
      Std.DTreeMap.Internal.Impl.Const.get t a h = t.get a h
-- Mathlib.CategoryTheory.Monoidal.OfHasFiniteProducts
CategoryTheory.monoidalOfHasFiniteCoproducts.rightUnitor_inv : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasInitial C]
  [inst_2 : CategoryTheory.Limits.HasBinaryCoproducts C] (X : C),
  (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv = CategoryTheory.Limits.coprod.inl
-- Mathlib.Lean.Environment
/-- Like `findConstVal?`, but only finds the `ConstantVal` for `decl` in `env` if it is a theorem.

Blocks on everything but the constant's body (if any), which is not accessible through the result.
 -/
Lean.Environment.findTheoremConstVal? : Lean.Environment → Lean.Name → optParam Bool false → Option Lean.ConstantVal
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRootMonic.powerBasis_dim : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
  (h : IsAdjoinRootMonic S f), h.powerBasis.dim = f.natDegree
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKeyD_modify : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k k' fallback : α} {f : β → β},
      (t.modify k f).getKeyD k' fallback =
        if cmp k k' = Ordering.eq then if k ∈ t then k else fallback else t.getKeyD k' fallback
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.vietoris.eq_1 : ∀ (α : Type u_1) [inst : TopologicalSpace α],
  TopologicalSpace.vietoris α =
    TopologicalSpace.generateFrom (Set.powerset '' {U | IsOpen U} ∪ (fun V => {s | (s ∩ V).Nonempty}) '' {V | IsOpen V})