mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
/-- An element is in `spinGroup Q` if and only if it is in `pinGroup Q` and `even Q`.  -/
spinGroup.mem_iff : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} {x : CliffordAlgebra Q}, x ∈ spinGroup Q ↔ x ∈ pinGroup Q ∧ x ∈ CliffordAlgebra.even Q
-- Mathlib.Data.Multiset.UnionInter
Multiset.zero_inter : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Multiset α), 0 ∩ s = 0
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.instNonemptyMethodsRef : Nonempty Lean.Meta.Simp.MethodsRef
-- Batteries.Data.Fin.Lemmas
Fin.modNat_mkDivMod : ∀ {m n : ℕ} (i : Fin m) (j : Fin n), (i.mkDivMod j).modNat = j
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.whiskerRightIso_hom : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f g : a ⟶ b} (η : f ≅ g) (h : b ⟶ c),
  (CategoryTheory.Bicategory.whiskerRightIso η h).hom = CategoryTheory.Bicategory.whiskerRight η.hom h
-- Mathlib.Geometry.Convex.ConvexSpace.Prod
Finsupp.instConvexSpace : {R : Type u_2} →
  [inst : Semiring R] →
    [inst_1 : PartialOrder R] →
      [inst_2 : IsStrictOrderedRing R] →
        {ι : Type u_3} →
          {X : Type u_4} → [inst_3 : Zero X] → [Convexity.ConvexSpace R X] → Convexity.ConvexSpace R (ι →₀ X)
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.map_sup : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  (p p' : Submodule R M) [inst_6 : RingHomSurjective σ₁₂] (f : M →ₛₗ[σ₁₂] M₂),
  Submodule.map f (p ⊔ p') = Submodule.map f p ⊔ Submodule.map f p'
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
ENNReal.tsum_biUnion : ∀ {α : Type u_1} {ι : Type u_4} {f : α → ENNReal} {t : ι → Set α},
  Set.univ.PairwiseDisjoint t → ∑' (x : ↑(⋃ i, t i)), f ↑x = ∑' (i : ι) (x : ↑(t i)), f ↑x
-- Mathlib.CategoryTheory.Generator.Basic
/-- For a category `C` and an object `G : C`, `G` is a separator of `C` if
the functor `C(G, -)` is faithful.

While `IsSeparator G : Prop` is the proposition that `G` is a separator of `C`,
an `HasSeparator C : Prop` is the proposition that such a separator exists.
Note that `HasSeparator C` is a proposition. It does not designate a favored separator
and merely asserts the existence of one.
 -/
CategoryTheory.HasSeparator : (C : Type u₁) → [CategoryTheory.Category.{v₁, u₁} C] → Prop
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.Mor₂Iso.brecOn.go : {motive : Mathlib.Tactic.BicategoryLike.Mor₂Iso → Sort u} →
  (t : Mathlib.Tactic.BicategoryLike.Mor₂Iso) →
    ((t : Mathlib.Tactic.BicategoryLike.Mor₂Iso) → Mathlib.Tactic.BicategoryLike.Mor₂Iso.below t → motive t) →
      motive t ×' Mathlib.Tactic.BicategoryLike.Mor₂Iso.below t
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
/-- The lower integral of a function over `AddCircle T` is equal to the lower integral over an
interval $(t, t + T]$ in `ℝ` of its lift to `ℝ`.  -/
AddCircle.lintegral_preimage : ∀ (T : ℝ) [hT : Fact (0 < T)] (t : ℝ) (f : AddCircle T → ENNReal),
  ∫⁻ (a : ℝ) in Set.Ioc t (t + T), f ↑a = ∫⁻ (b : AddCircle T), f b
-- Mathlib.Combinatorics.SimpleGraph.Bipartite
SimpleGraph.IsBipartiteWith.mem_of_adj : ∀ {V : Type u_1} {G : SimpleGraph V} {s t : Set V},
  G.IsBipartiteWith s t → ∀ ⦃v w : V⦄, G.Adj v w → v ∈ s ∧ w ∈ t ∨ v ∈ t ∧ w ∈ s
-- Mathlib.CategoryTheory.Bicategory.Basic
/-- The left whiskering of a 2-isomorphism is a 2-isomorphism.  -/
CategoryTheory.Bicategory.«term_◁ᵢ_» : Lean.TrailingParserDescr
-- Mathlib.Tactic.FBinop
FBinopElab.SRec.mk : Lean.Name → Array Lean.Expr → FBinopElab.SRec
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic
SSet.anodyneExtensions.of_isIso : ∀ {X Y : SSet} (f : X ⟶ Y) [CategoryTheory.IsIso f], SSet.anodyneExtensions f
-- Lean.Meta.Tactic.Simp.Rewrite
_private.Lean.Meta.Tactic.Simp.Rewrite.0.Lean.Meta.Simp.isEqnThmHypothesis.go : Lean.Expr → Bool
-- Mathlib.Data.Finset.Card
Finset.card_le_three : ∀ {α : Type u_1} [inst : DecidableEq α] {a b c : α}, {a, b, c}.card ≤ 3
-- Mathlib.MeasureTheory.Function.L1Space.AEEqFun
MeasureTheory.L1.norm_def : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  (f : ↥(MeasureTheory.Lp β 1 μ)), ‖f‖ = (∫⁻ (a : α), ‖↑↑f a‖ₑ ∂μ).toReal
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- The source of every characteristic map of dimension `n` is
`(ball 0 1 : Set (Fin n → ℝ))`.  -/
Topology.RelCWComplex.source_eq : ∀ {X : Type u} {inst : TopologicalSpace X} {C : Set X} {D : outParam (Set X)} [self : Topology.RelCWComplex C D] (n : ℕ)
  (i : Topology.RelCWComplex.cell C n), (Topology.RelCWComplex.map n i).source = Metric.ball 0 1
-- Mathlib.CategoryTheory.Triangulated.TStructure.Basic
CategoryTheory.Triangulated.TStructure.isGE_shift : ∀ {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) (X : C) (n a n' : ℤ),
  autoParam (a + n' = n) CategoryTheory.Triangulated.TStructure.isGE_shift._auto_1 →
    ∀ [t.IsGE X n], t.IsGE ((CategoryTheory.shiftFunctor C a).obj X) n'
-- Mathlib.Condensed.Discrete.Module
LightCondMod.LocallyConstant.instFullModuleCatFunctor : ∀ (R : Type u) [inst : Ring R], (LightCondMod.LocallyConstant.functor R).Full
-- Init.Data.BitVec.Lemmas
BitVec.add_assoc : ∀ {n : ℕ} (x y z : BitVec n), x + y + z = x + (y + z)
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
/-- Given a `k`-module `A` with a compatible `DistribMulAction` of `G`, and a function
`f : G × G → A` satisfying the 2-cocycle condition, produces a 2-cocycle for the representation on
`A` induced by the `DistribMulAction`.  -/
groupCohomology.cocyclesOfIsCocycle₂ : {k G A : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      [inst_2 : AddCommGroup A] →
        [inst_3 : Module k A] →
          [inst_4 : DistribMulAction G A] →
            [inst_5 : SMulCommClass G k A] →
              {f : G × G → A} →
                groupCohomology.IsCocycle₂ f → ↥(groupCohomology.cocycles₂ (Rep.ofDistribMulAction k G A))
-- Init.Data.String.Iterate
String.Slice.RevByteIterator.mk.inj : ∀ {s : String.Slice} {offset : String.Pos.Raw} {hinv : offset ≤ s.rawEndPos} {s_1 : String.Slice}
  {offset_1 : String.Pos.Raw} {hinv_1 : offset_1 ≤ s_1.rawEndPos},
  { s := s, offset := offset, hinv := hinv } = { s := s_1, offset := offset_1, hinv := hinv_1 } →
    s = s_1 ∧ offset = offset_1
-- Mathlib.Algebra.Quandle
Rack.PreEnvelGroupRel.symm : ∀ {R : Type u} [inst : Rack R] {a b : Rack.PreEnvelGroup R}, Rack.PreEnvelGroupRel R a b → Rack.PreEnvelGroupRel R b a
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getElem!_toList_roo_eq_add : ∀ {m n : ℤ} {i : ℕ}, i < (n - (m + 1)).toNat → (m<...n).toList[i]! = m + 1 + ↑i
-- Mathlib.Algebra.Polynomial.EraseLead
Polynomial.eraseLead_natDegree_le_aux : ∀ {R : Type u_1} [inst : Semiring R] {f : Polynomial R}, f.eraseLead.natDegree ≤ f.natDegree
-- Mathlib.Algebra.Order.AddGroupWithTop
LinearOrderedAddCommMonoidWithTop.toOrderTop : {α : Type u_3} → [self : LinearOrderedAddCommMonoidWithTop α] → OrderTop α
-- Mathlib.Algebra.Order.BigOperators.Expect
Fintype.expect_eq_zero_iff_of_nonpos : ∀ {ι : Type u_1} {α : Type u_2} [inst : Fintype ι] [inst_1 : AddCommMonoid α] [inst_2 : PartialOrder α]
  [IsOrderedAddMonoid α] [inst_4 : Module ℚ≥0 α] {f : ι → α}, f ≤ 0 → ((Finset.univ.expect fun i => f i) = 0 ↔ f = 0)
-- Mathlib.LinearAlgebra.Finsupp.Defs
Finsupp.mapRange.linearEquiv_refl : ∀ {α : Type u_1} {M : Type u_2} {R : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  Finsupp.mapRange.linearEquiv (LinearEquiv.refl R M) = LinearEquiv.refl R (α →₀ M)
-- Mathlib.RingTheory.Kaehler.Polynomial
/-- The relative differential module of the univariate polynomial algebra `R[X]` is isomorphic to
`R[X]` as an `R[X]`-module.  -/
KaehlerDifferential.polynomialEquiv : (R : Type u) → [inst : CommRing R] → Ω[Polynomial R⁄R] ≃ₗ[Polynomial R] Polynomial R
-- Mathlib.Topology.Category.CompHausLike.Basic
/-- Any continuous function on compact Hausdorff spaces is a closed map.  -/
CompHausLike.isClosedMap : ∀ {P : TopCat → Prop} {X Y : CompHausLike P} (f : X ⟶ Y), IsClosedMap ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.SetTheory.ZFC.Class
/-- The power class of a class is the class of all subclasses that are ZFC sets  -/
Class.powerset : Class.{u_1} → Class.{u_1}
-- Mathlib.Data.W.Constructions
_private.Mathlib.Data.W.Constructions.0.WType.toList.match_1.eq_1 : ∀ (γ : Type u_1) (motive : WType (WType.Listβ γ) → Sort u_2) (f : WType.Listβ γ WType.Listα.nil → WType (WType.Listβ γ))
  (h_1 : (f : WType.Listβ γ WType.Listα.nil → WType (WType.Listβ γ)) → motive (WType.mk WType.Listα.nil f))
  (h_2 :
    (hd : γ) →
      (f : WType.Listβ γ (WType.Listα.cons hd) → WType (WType.Listβ γ)) → motive (WType.mk (WType.Listα.cons hd) f)),
  (match WType.mk WType.Listα.nil f with
    | WType.mk WType.Listα.nil f => h_1 f
    | WType.mk (WType.Listα.cons hd) f => h_2 hd f) =
    h_1 f
-- Mathlib.Topology.NhdsKer
subset_nhdsKer_iff : ∀ {X : Type u_2} [inst : TopologicalSpace X] {s t : Set X}, s ⊆ nhdsKer t ↔ ∀ (U : Set X), IsOpen U → t ⊆ U → s ⊆ U
-- Mathlib.Data.List.Defs
List.iterateTR.loop.eq_def : ∀ {α : Type u_1} (f : α → α) (a : α) (n : ℕ) (l : List α),
  List.iterateTR.loop f a n l =
    match n with
    | 0 => l.reverse
    | n.succ => List.iterateTR.loop f (f a) n (a :: l)
-- Batteries.Data.List.Lemmas
List.findIdxs_nil : ∀ {α : Type u_1} {p : α → Bool} {s : ℕ}, List.findIdxs p [] s = []
-- Std.Sat.AIG.Basic
/-- A `RefVec` bundled with constant distance to be shifted by.
 -/
Std.Sat.AIG.ShiftTarget : {α : Type} → [inst : Hashable α] → [inst_1 : DecidableEq α] → Std.Sat.AIG α → ℕ → Type
-- Batteries.Lean.PersistentHashMap
/-- Merge two `PersistentHashMap`s. The values of keys which appear in both maps are
combined using the monadic function `f`.
 -/
Lean.PersistentHashMap.mergeWithM : {α : Type u_1} →
  [inst : BEq α] →
    [inst_1 : Hashable α] →
      {m : Type (max u_2 u_1) → Type u_3} →
        {β : Type (max u_2 u_1)} →
          [Monad m] →
            Lean.PersistentHashMap α β → Lean.PersistentHashMap α β → (α → β → β → m β) → m (Lean.PersistentHashMap α β)
-- Mathlib.Data.ZMod.Basic
/-- Cast an integer modulo `n` to another semiring.
This function is a morphism if the characteristic of `R` divides `n`.
See `ZMod.castHom` for a bundled version.  -/
ZMod.cast : {R : Type u_1} → [AddGroupWithOne R] → {n : ℕ} → ZMod n → R
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.instHasCokernelInl : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y : C} [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y],
  CategoryTheory.Limits.HasCokernel CategoryTheory.Limits.biprod.inl
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- The minimal distance of a point to a set  -/
Metric.infDist : {α : Type u} → [PseudoMetricSpace α] → α → Set α → ℝ
-- Mathlib.Order.SuccPred.Limit
SuccOrder.limitRecOn_of_isSuccLimit : ∀ {α : Type u_1} {b : α} {motive : α → Sort u_2} [inst : PartialOrder α] [inst_1 : SuccOrder α]
  [inst_2 : WellFoundedLT α] (isMin : (a : α) → IsMin a → motive a)
  (succ : (a : α) → ¬IsMax a → motive a → motive (Order.succ a))
  (isSuccLimit : (a : α) → Order.IsSuccLimit a → ((b : α) → b < a → motive b) → motive a) (hb : Order.IsSuccLimit b),
  SuccOrder.limitRecOn b isMin succ isSuccLimit =
    isSuccLimit b hb fun x x_1 => SuccOrder.limitRecOn x isMin succ isSuccLimit
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
Summable.add : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f g : β → α}
  {L : SummationFilter β} [ContinuousAdd α], Summable f L → Summable g L → Summable (fun b => f b + g b) L
-- Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
AlgebraicGeometry.range_eq_univ : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.Surjective f], Set.range ⇑f = Set.univ
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Impl.Const.alter.match_1.splitter : {α : Type u_1} →
  {β : Type u_2} →
    (l' : Std.DTreeMap.Internal.Impl α fun x => β) →
      (motive : Std.DTreeMap.Internal.Impl.SizedBalancedTree α (fun x => β) (l'.size - 1) (l'.size + 1) → Sort u_3) →
        (x : Std.DTreeMap.Internal.Impl.SizedBalancedTree α (fun x => β) (l'.size - 1) (l'.size + 1)) →
          ((d : Std.DTreeMap.Internal.Impl α fun x => β) →
              (hd : d.Balanced) →
                (hd'₁ : l'.size - 1 ≤ d.size) →
                  (hd'₂ : d.size ≤ l'.size + 1) →
                    motive { impl := d, balanced_impl := hd, lb_le_size_impl := hd'₁, size_impl_le_ub := hd'₂ }) →
            motive x
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
SimpleGraph.IsEdgeConnected.connected : ∀ {V : Type u_1} {G : SimpleGraph V} {k : ℕ} [Nonempty V], k ≠ 0 → G.IsEdgeConnected k → G.Connected
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.size_ofArray_fold_fn : ∀ {n : ℕ} (assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment)
  (cOpt : Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n)),
  (Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.ofArray_fold_fn assignments cOpt).size = assignments.size
-- Mathlib.RingTheory.MvPowerSeries.Evaluation
MvPowerSeries.comp_eval₂ : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommRing R] [inst_1 : UniformSpace R] {S : Type u_3} [inst_2 : CommRing S]
  [inst_3 : UniformSpace S] {φ : R →+* S} {a : σ → S} [IsTopologicalSemiring R] [IsUniformAddGroup R]
  [IsUniformAddGroup S] [CompleteSpace S] [T2Space S] [IsTopologicalRing S] [IsLinearTopology S S],
  Continuous ⇑φ →
    MvPowerSeries.HasEval a →
      ∀ {T : Type u_4} [inst_11 : UniformSpace T] [CompleteSpace T] [T2Space T] [inst_14 : CommRing T]
        [IsTopologicalRing T] [IsLinearTopology T T] [IsUniformAddGroup T] {ε : S →+* T},
        Continuous ⇑ε → ⇑ε ∘ MvPowerSeries.eval₂ φ a = MvPowerSeries.eval₂ (ε.comp φ) (⇑ε ∘ a)
-- Lean.Parser.Do
Lean.Parser.Term.doTry : Lean.Parser.Parser
-- Mathlib.LinearAlgebra.BilinearMap
LinearMap.compr₂_id : ∀ {A : Type u_1} {R : Type u_2} [inst : Semiring A] [inst_1 : CommSemiring R] {M : Type u_5} {Nₗ : Type u_8}
  {Pₗ : Type u_9} [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid Nₗ] [inst_4 : AddCommMonoid Pₗ]
  [inst_5 : Module R Nₗ] [inst_6 : Module R Pₗ] [inst_7 : Module A Pₗ] [inst_8 : SMulCommClass R A Pₗ]
  [inst_9 : Module R A] [inst_10 : Module A M] [inst_11 : IsScalarTower R A Pₗ] (f : M →ₗ[A] Nₗ →ₗ[R] Pₗ),
  f.compr₂ LinearMap.id = f
-- Lean.Elab.InfoTree.Basic
Lean.Elab.CompletionInfo.stx : Lean.Elab.CompletionInfo → Lean.Syntax
-- Mathlib.Analysis.Calculus.ContDiff.Basic
contDiffWithinAt_singleton : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {x : E}
  {n : WithTop ℕ∞}, ContDiffWithinAt 𝕜 n f {x} x
-- Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
/-- The induced coverage by a Grothendieck topology as a precoverage.  -/
CategoryTheory.GrothendieckTopology.toPrecoverage : {C : Type u_2} →
  [inst : CategoryTheory.Category.{u_3, u_2} C] → CategoryTheory.GrothendieckTopology C → CategoryTheory.Precoverage C
-- Batteries.Control.LawfulMonadState
LawfulMonadStateOf.set_bind_getModify : ∀ {σ : Type u_2} {m : Type u_2 → Type u_1} [inst : Monad m] [inst_1 : MonadStateOf σ m] [LawfulMonadStateOf σ m] (s : σ)
  (f : σ → σ),
  (do
      set s
      getModify f) =
    do
    set (f s)
    pure s
-- Lean.Linter.MissingDocs
Lean.Linter.MissingDocs.hasInheritDoc : Lean.Syntax → Bool
-- Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
pinGroup.toUnits_injective : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M}, Function.Injective ⇑pinGroup.toUnits
-- Mathlib.Order.Filter.Map
Filter.image_coe_mem_of_mem_comap : ∀ {α : Type u_1} {f : Filter α} {U : Set α},
  U ∈ f → ∀ {W : Set ↑U}, W ∈ Filter.comap Subtype.val f → Subtype.val '' W ∈ f
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
/-- The top subalgebra is isomorphic to the algebra.

This is the algebra version of `Submodule.topEquiv`.  -/
Subalgebra.topEquiv : {R : Type u} → {A : Type v} → [inst : CommSemiring R] → [inst_1 : Semiring A] → [inst_2 : Algebra R A] → ↥⊤ ≃ₐ[R] A
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.truncGEδLT_comp_truncLTι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} 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) (n : ℤ),
  CategoryTheory.CategoryStruct.comp (t.truncGEδLT n)
      (CategoryTheory.Functor.whiskerRight (t.truncLTι n) (CategoryTheory.shiftFunctor C 1)) =
    0
-- Mathlib.RingTheory.TensorProduct.Pi
/-- Tensor product of rings commutes with binary products on the right.  -/
Algebra.TensorProduct.prodRight : (R : Type u_1) →
  (S : Type u_2) →
    (A : Type u_3) →
      [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] →
                    (B : Type u_6) →
                      (C : Type u_7) →
                        [inst_7 : Semiring B] →
                          [inst_8 : Semiring C] →
                            [inst_9 : Algebra R B] →
                              [inst_10 : Algebra R C] →
                                TensorProduct R A (B × C) ≃ₐ[S] TensorProduct R A B × TensorProduct R A C
-- Mathlib.Data.Subtype
Subtype.map_id : ∀ {α : Sort u_1} {p : α → Prop} {h : ∀ (a : α), p a → p (id a)}, Subtype.map id h = id
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.ExBase.atom.inj : ∀ {u : Lean.Level} {α : Q(Type u)} {BaseType : Q(«$α») → Type} {sα : Q(CommSemiring «$α»)} {e : Q(«$α»)} {id id_1 : ℕ},
  Mathlib.Tactic.Ring.Common.ExBase.atom id = Mathlib.Tactic.Ring.Common.ExBase.atom id_1 → id = id_1
-- Mathlib.Probability.Moments.Basic
ContinuousLinearMap.integral_comp_id_comm : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace ℝ E] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : NormedSpace ℝ F] [CompleteSpace E] [CompleteSpace F] [inst_9 : MeasurableSpace E]
  {μ : MeasureTheory.Measure E},
  MeasureTheory.Integrable id μ → ∀ (L : E →L[𝕜] F), ∫ (x : E), L x ∂μ = L (∫ (x : E), x ∂μ)
-- Mathlib.RingTheory.Coprime.Basic
IsCoprime.neg_left_iff : ∀ {R : Type u} [inst : CommRing R] (x y : R), IsCoprime (-x) y ↔ IsCoprime x y
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.cyclesIsoX₂_hom_inv_id_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasLeftHomology] (hg : S.g = 0) {Z : C} (h : S.cycles ⟶ Z),
  CategoryTheory.CategoryStruct.comp S.iCycles (CategoryTheory.CategoryStruct.comp (S.cyclesIsoX₂ hg).inv h) = h
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits
ProfiniteAddGrp.cone_π_app : ∀ (P : ProfiniteAddGrp.{u}) (U : OpenNormalAddSubgroup ↑P.toProfinite.toTop), P.cone.π.app U = ProfiniteAddGrp.proj U
-- Lean.Util.CollectLevelParams
Lean.CollectLevelParams.State.visitedExpr : Lean.CollectLevelParams.State → Lean.ExprSet
-- Mathlib.Tactic.FunProp.FunctionData
/-- The decomposition failed for some other reason.  -/
Mathlib.Meta.FunProp.DecompositionResult.failed : Mathlib.Meta.FunProp.DecompositionResult
-- Mathlib.Dynamics.PeriodicPts.Defs
Function.IsPeriodicPt.sub : ∀ {α : Type u_1} {f : α → α} {x : α} {m n : ℕ},
  Function.IsPeriodicPt f m x → Function.IsPeriodicPt f n x → Function.IsPeriodicPt f (m - n) x
-- Mathlib.Analysis.Analytic.ConvergenceRadius
_private.Mathlib.Analysis.Analytic.ConvergenceRadius.0.constFormalMultilinearSeries.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (x : ℕ) → motive x),
  (match 0 with
    | 0 => h_1 ()
    | x => h_2 x) =
    h_1 ()
-- Init.Grind.Config
Lean.Grind.OrderConfig.toNoopConfig : Lean.Grind.OrderConfig → Lean.Grind.NoopConfig
-- Mathlib.MeasureTheory.OuterMeasure.OfFunction
/-- The value of the Infimum of a family of outer measures on a nonempty set is not simply
the minimum value of a measure on that set: it is the infimum sum of measures of countable set of
sets that covers that set, where a different measure can be used for each set in the cover.  -/
MeasureTheory.OuterMeasure.iInf_apply' : ∀ {α : Type u_1} {ι : Sort u_2} (m : ι → MeasureTheory.OuterMeasure α) {s : Set α},
  s.Nonempty → (⨅ i, m i) s = ⨅ t, ⨅ (_ : s ⊆ Set.iUnion t), ∑' (n : ℕ), ⨅ i, (m i) (t n)
-- Mathlib.Order.PFilter
/-- There is a top filter when `P` has a bottom element.  -/
Order.PFilter.instOrderTopOfOrderBot : {P : Type u_2} → [inst : Preorder P] → [OrderBot P] → OrderTop (Order.PFilter P)
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.monObjAsOverPullback : {M S T : AlgebraicGeometry.Scheme} →
  [inst : M.Over S] →
    {f : T ⟶ S} →
      [CategoryTheory.MonObj (M.asOver S)] → CategoryTheory.MonObj ((CategoryTheory.Limits.pullback (M ↘ S) f).asOver T)
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.star_eq_neg : ∀ {R : Type u_3} {c₃ : R} [inst : CommRing R] [NoZeroDivisors R] [CharZero R] {c₁ : R}
  {a : QuaternionAlgebra R c₁ 0 c₃}, star a = -a ↔ a.re = 0
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.IterM.forIn_filter : ∀ {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {Pred EPred : Type w} [inst : Monad m] [LawfulMonad m]
  [inst_2 : Monad n] [inst_3 : Std.Internal.Do.Assertion Pred] [inst_4 : Std.Internal.Do.Assertion EPred]
  [inst_5 : Std.Internal.Do.WPMonad n Pred EPred] [inst_6 : MonadLiftT m n] [LawfulMonadLiftT m n]
  [inst_8 : Std.Iterator α m β] [Std.Iterators.Finite α m] [inst_10 : Std.IteratorLoop α m n]
  [Std.LawfulIteratorLoop α m n] {it : Std.IterM m β} {f : β → Bool} {init : γ} {g : β → γ → n (ForInStep γ)} {P : Pred}
  {Q : γ → Pred} {eQ : EPred},
  ⦃ P ⦄ forIn it init fun out acc => if f out = true then g out acc else pure (ForInStep.yield acc) ⦃ Q; eQ ⦄ →
    ⦃ P ⦄ forIn (Std.IterM.filter f it) init g ⦃ Q; eQ ⦄
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.alterKey_of_perm : ∀ {α : Type u} [inst : BEq α] {β : Type v} [EquivBEq α] {a : α} {f : Option β → Option β} {l l' : List ((_ : α) × β)},
  Std.Internal.List.DistinctKeys l →
    l.Perm l' → (Std.Internal.List.Const.alterKey a f l).Perm (Std.Internal.List.Const.alterKey a f l')
-- Mathlib.Topology.Instances.Matrix
Continuous.matrix_transpose : ∀ {X : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_8} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace R]
  {A : X → Matrix m n R}, Continuous A → Continuous fun x => (A x).transpose
-- Std.Async.Basic
/-- Converts a `BaseAsync` to a `EIO ETask`.
 -/
Std.Async.EAsync.toEIO : {ε α : Type} → Std.Async.EAsync ε α → EIO ε (Std.Async.ETask ε α)
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanClass.mk_sub_comm : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] (a b : M),
  ArchimedeanClass.mk (a - b) = ArchimedeanClass.mk (b - a)