mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.GRewrite.Core
/-- Configures the behavior of the `rewrite` and `rw` tactics.  -/
Mathlib.Tactic.GRewrite.Config : Type
-- Init.Data.Vector.Lemmas
Vector.getElem_reverse : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i : ℕ} (hi : i < n), xs.reverse[i] = xs[n - 1 - i]
-- Mathlib.Data.Bool.AllAny
List.all_iff_forall_prop : ∀ {α : Type u_1} {p : α → Prop} [inst : DecidablePred p] {l : List α},
  (l.all fun a => decide (p a)) = true ↔ ∀ a ∈ l, p a
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.CWComplex.map_def : ∀ {X : Type u_1} [inst : TopologicalSpace X] (C : Set X) [inst_1 : Topology.CWComplex C] (n : ℕ)
  (i : Topology.CWComplex.cell C n), Topology.RelCWComplex.map n i = Topology.CWComplex.map n i
-- Mathlib.CategoryTheory.Bicategory.Monad.Basic
/-- The object in `B` associated with the comonad.  -/
CategoryTheory.Bicategory.OplaxTrans.ComonadBicat.obj : {B : Type u} → [inst : CategoryTheory.Bicategory B] → CategoryTheory.Bicategory.OplaxTrans.ComonadBicat B → B
-- Mathlib.SetTheory.Ordinal.Univ
Cardinal.lt_univ : ∀ {c : Cardinal.{u + 1}}, c < Cardinal.univ.{u, u + 1} ↔ ∃ c', c = Cardinal.lift.{u + 1, u} c'
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.nonUnitalNonAssocRing.eq_1 : ∀ {R : Type u_1} {M : Type u_4} [inst : Ring R] [inst_1 : Add M],
  AddMonoidAlgebra.nonUnitalNonAssocRing =
    { toAddCommGroup := AddMonoidAlgebra.addCommGroup, toMul := AddMonoidAlgebra.nonUnitalNonAssocSemiring.toMul,
      left_distrib := ⋯, right_distrib := ⋯, zero_mul := ⋯, mul_zero := ⋯ }
-- Std.Data.HashSet.Lemmas
Std.HashSet.ofList_singleton : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {k : α}, Std.HashSet.ofList [k] = ∅.insert k
-- Mathlib.Order.CompleteLattice.PiLex
_private.Mathlib.Order.CompleteLattice.PiLex.0.Pi.Lex.isGLB_sInf : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : LinearOrder ι] [inst_1 : (i : ι) → CompleteLinearOrder (α i)]
  [inst_2 : WellFoundedLT ι] {s : Set (Lex ((i : ι) → (fun i => α i) i))}, IsGLB s (sInf s)
-- Mathlib.Analysis.InnerProductSpace.ExteriorPower
exteriorPower.instInnerProductSpaceRealSubtypeExteriorAlgebraMemSubmoduleExteriorPower : {n : ℕ} →
  {E : Type u_1} →
    [inst : NormedAddCommGroup E] →
      [inst_1 : InnerProductSpace ℝ E] → [inst_2 : FiniteDimensional ℝ E] → InnerProductSpace ℝ ↥(⋀[ℝ]^n E)
-- Mathlib.Analysis.Normed.Lp.Matrix
Matrix.toLpLin_symm_pow : ∀ {n : Type u_2} {R : Type u_4} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing R] (p : ENNReal)
  (A : Module.End R (WithLp p (n → R))) (k : ℕ), (Matrix.toLpLin p p).symm (A ^ k) = (Matrix.toLpLin p p).symm A ^ k
-- Init.Data.String.Lemmas.Pattern.String.Basic
String.Slice.Pattern.Model.ForwardSliceSearcher.isLongestRevMatchAt_iff : ∀ {pat s : String.Slice} {pos₁ pos₂ : s.Pos},
  String.Slice.Pattern.Model.IsLongestRevMatchAt pat pos₁ pos₂ ↔
    ∃ (h : pos₁ ≤ pos₂), (s.slice pos₁ pos₂ h).copy = pat.copy
-- Mathlib.RepresentationTheory.Equiv
/-- Equiv between representations induced by linear equiv between `V ⊗[k] (α →₀ W)` and
`α →₀ (V ⊗[k] W)`.  -/
Representation.finsuppTensorRight : {G : Type v} →
  [inst : Monoid G] →
    {V : Type v'} →
      [inst_1 : AddCommMonoid V] →
        {W : Type w'} →
          [inst_2 : AddCommMonoid W] →
            {k : Type u} →
              [inst_3 : CommSemiring k] →
                [inst_4 : Module k V] →
                  [inst_5 : Module k W] →
                    (σ : Representation k G V) →
                      (ρ : Representation k G W) →
                        (α : Type w') → [DecidableEq α] → (σ.tprod (ρ.finsupp α)).Equiv ((σ.tprod ρ).finsupp α)
-- Mathlib.RingTheory.Bialgebra.Equiv
BialgEquiv.mk : {R : Type u} →
  [inst : CommSemiring R] →
    {A : Type v} →
      {B : Type w} →
        [inst_1 : Semiring A] →
          [inst_2 : Semiring B] →
            [inst_3 : Algebra R A] →
              [inst_4 : Algebra R B] →
                [inst_5 : CoalgebraStruct R A] →
                  [inst_6 : CoalgebraStruct R B] →
                    (toCoalgEquiv : A ≃ₗc[R] B) →
                      (∀ (x y : A), toCoalgEquiv.toFun (x * y) = toCoalgEquiv.toFun x * toCoalgEquiv.toFun y) →
                        A ≃ₐc[R] B
-- Mathlib.AlgebraicGeometry.Cover.Directed
AlgebraicGeometry.Scheme.Cover.LocallyDirected.w : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {X : AlgebraicGeometry.Scheme}
  {𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X}
  {inst : CategoryTheory.Category.{v_1, u_1} 𝒰.I₀} [self : 𝒰.LocallyDirected] {i j : 𝒰.I₀} (hij : i ⟶ j),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Cover.LocallyDirected.trans hij) (𝒰.f j) = 𝒰.f i
-- Mathlib.MeasureTheory.OuterMeasure.OfFunction
MeasureTheory.OuterMeasure.map_ofFunction : ∀ {α : Type u_1} {m : Set α → ENNReal} {m_empty : m ∅ = 0} {β : Type u_2} {f : α → β},
  Function.Injective f →
    (MeasureTheory.OuterMeasure.map f) (MeasureTheory.OuterMeasure.ofFunction m m_empty) =
      MeasureTheory.OuterMeasure.ofFunction (fun s => m (f ⁻¹' s)) m_empty
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
/-- Convergence in the metric on `C₀(α, β)` is uniform convergence.  -/
ZeroAtInftyContinuousMap.tendsto_iff_tendstoUniformly : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β] [inst_2 : Zero β] {ι : Type u_2}
  {F : ι → ZeroAtInftyContinuousMap α β} {f : ZeroAtInftyContinuousMap α β} {l : Filter ι},
  Filter.Tendsto F l (nhds f) ↔ TendstoUniformly (fun i => ⇑(F i)) (⇑f) l
-- Std.Tactic.BVDecide.Reflect
Std.Tactic.BVDecide.Reflect.BitVec.udiv_congr : ∀ {w : ℕ} (lhs rhs lhs' rhs' : BitVec w), lhs' = lhs → rhs' = rhs → lhs' / rhs' = lhs / rhs
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.ServerCapabilities.colorProvider? : Lean.Lsp.ServerCapabilities → Option Lean.Lsp.DocumentColorOptions
-- Mathlib.Algebra.Homology.Embedding.TruncLE
ComplexShape.Embedding.truncLEFunctor_obj : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') [inst : e.IsTruncLE]
  (C : Type u_4) [inst_1 : CategoryTheory.Category.{v_2, u_4} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroObject C] [inst_4 : CategoryTheory.CategoryWithHomology C]
  (K : HomologicalComplex C c'), (e.truncLEFunctor C).obj K = K.truncLE e
-- Mathlib.Data.PNat.Xgcd
PNat.XgcdType.reduce_isSpecial' : ∀ (u : PNat.XgcdType), u.IsSpecial → u.reduce.IsSpecial'
-- Mathlib.RingTheory.TensorProduct.Finite
Module.exists_isPrincipal_quotient_of_finite : ∀ (R : Type u_1) (M : Type u_2) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Module.Finite R M]
  [Nontrivial M], ∃ N, N ≠ ⊤ ∧ ⊤.IsPrincipal
-- Mathlib.Algebra.Order.Algebra
algebraMap_le_algebraMap : ∀ {α : Type u_1} {β : Type u_2} [inst : CommSemiring α] [inst_1 : PartialOrder α] [inst_2 : Semiring β]
  [inst_3 : PartialOrder β] [inst_4 : Algebra α β] [ZeroLEOneClass β] [Nontrivial β] [SMulPosMono α β]
  [SMulPosReflectLE α β] {a₁ a₂ : α}, (algebraMap α β) a₁ ≤ (algebraMap α β) a₂ ↔ a₁ ≤ a₂
-- Mathlib.SetTheory.Descriptive.Tree
Descriptive.Tree.pullSub_subAt : ∀ {A : Type u_1} (T : ↥(Descriptive.tree A)) (x : List A), Descriptive.Tree.pullSub (Descriptive.Tree.subAt T x) x ≤ T
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
LinearMap.BilinForm.apply_smul_sub_smul_sub_eq : ∀ {R : Type u_1} {M : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (B : LinearMap.BilinForm R M) (x y : M),
  (B ((B x) y • x - (B x) x • y)) ((B x) y • x - (B x) x • y) = (B x) x * ((B x) x * (B y) y - (B x) y * (B y) x)
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.IsCycleOn.extendDomain : ∀ {α : Type u_2} {β : Type u_3} {g : Equiv.Perm α} {s : Set α} {p : β → Prop} [inst : DecidablePred p]
  (f : α ≃ Subtype p), g.IsCycleOn s → (g.extendDomain f).IsCycleOn (Subtype.val ∘ ⇑f '' s)
-- Mathlib.Algebra.Category.Grp.Basic
AddGrpCat.instCoeMonCat : Coe AddGrpCat AddMonCat
-- Mathlib.Topology.Homotopy.Contractible
ContractibleSpace.mk : ∀ {X : Type u_1} [inst : TopologicalSpace X], Nonempty (ContinuousMap.HomotopyEquiv X Unit) → ContractibleSpace X
-- Mathlib.MeasureTheory.Group.FoelnerFilter
amenable_of_maxFoelner_neBot : ∀ {G : Type u_1} {X : Type u_2} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} [inst_1 : Group G]
  [inst_2 : MulAction G X] [MeasureTheory.SMulInvariantMeasure G X μ] [(maxFoelner G μ).NeBot],
  ∃ m,
    m Set.univ = 1 ∧
      (∀ (s t : Set X), MeasurableSet t → Disjoint s t → m (s ∪ t) = m s + m t) ∧ ∀ (g : G) (s : Set X), m (g • s) = m s
-- Batteries.Linter.UnreachableTactic
/-- Search for tactic executions in the info tree and remove executed tactic syntaxes.  -/
Batteries.Linter.UnreachableTactic.eraseUsedTactics : Lean.Elab.InfoTree → Batteries.Linter.UnreachableTactic.M Unit
-- Mathlib.Topology.Spectral.Hom
IsProperMap.isSpectralMap : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β},
  IsProperMap f → IsSpectralMap f
-- Batteries.Data.UnionFind.Basic
Batteries.UnionFind.rank'_lt : ∀ (self : Batteries.UnionFind) (i : ℕ) (h : i < self.arr.size),
  self.arr[i].parent ≠ i → self.rank i < self.rank self.arr[i].parent
-- Std.Sync.SharedMutex
/-- An exclusion primitive that allows a number of readers or at most one writer.

If you want to guard shared state, use `SharedMutex α` instead.
 -/
Std.BaseSharedMutex : Type
-- Mathlib.CategoryTheory.Category.RelCat
/-- The underlying relation between `X` and `Y` of a morphism `X ⟶ Y` for `X Y : RelCat`.  -/
CategoryTheory.RelCat.Hom.rel : {X Y : CategoryTheory.RelCat} → X.Hom Y → SetRel X Y
-- Mathlib.Topology.Algebra.Module.Equiv
/-- Continuous linear equivalences between modules. We only put the type classes that are necessary
for the definition, although in applications `M` and `M₂` will be topological modules over the
topological semiring `R`.  -/
ContinuousLinearEquiv.continuous_toFun : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : Semiring S] {σ : R →+* S} {σ' : S →+* R}
  [inst_2 : RingHomInvPair σ σ'] [inst_3 : RingHomInvPair σ' σ] {M : Type u_3} [inst_4 : TopologicalSpace M]
  [inst_5 : AddCommMonoid M] {M₂ : Type u_4} [inst_6 : TopologicalSpace M₂] [inst_7 : AddCommMonoid M₂]
  [inst_8 : Module R M] [inst_9 : Module S M₂] (self : M ≃SL[σ] M₂), Continuous (↑↑self).toFun
-- Mathlib.CategoryTheory.Monoidal.CommMon_
CategoryTheory.CommMon.mk.injEq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X : C) [mon : CategoryTheory.MonObj X]
  [comm : CategoryTheory.IsCommMonObj X] (X_1 : C) (mon_1 : CategoryTheory.MonObj X_1)
  (comm_1 : CategoryTheory.IsCommMonObj X_1),
  ({ X := X, mon := mon, comm := comm } = { X := X_1, mon := mon_1, comm := comm_1 }) = (X = X_1 ∧ mon ≍ mon_1)
-- Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
ciSup_subsingleton : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompletePartialOrderSup α] [Subsingleton ι] (i : ι) (s : ι → α),
  ⨆ i, s i = s i
-- Std.Sat.AIG.LawfulOperator
Std.Sat.AIG.LawfulOperator.denote_cast_entry : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {β : Std.Sat.AIG α → Type}
  {f : (aig : Std.Sat.AIG α) → β aig → Std.Sat.AIG.Entrypoint α} [Std.Sat.AIG.LawfulOperator α β f] {assign : α → Bool}
  (entry : Std.Sat.AIG.Entrypoint α) {input : β entry.aig}
  {h : entry.aig.decls.size ≤ (f entry.aig input).aig.decls.size},
  ⟦assign, { aig := (f entry.aig input).aig, ref := entry.ref.cast h }⟧ = ⟦assign, entry⟧
-- Init.Data.Range.Polymorphic.Stream
Std.PRange.instToStreamRcoIterIteratorOfUpwardEnumerable : {α : Type u_1} → [Std.PRange.UpwardEnumerable α] → Std.ToStream (Std.Rco α) (Std.Iter α)
-- Mathlib.Algebra.Prime.Defs
Prime.dvd_pow_iff_dvd : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] {p : M}, Prime p → ∀ {a : M} {n : ℕ}, n ≠ 0 → (p ∣ a ^ n ↔ p ∣ a)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- The product of two antitone functions is antitone.  -/
Antitone.mul' : ∀ {α : Type u_1} {β : Type u_2} [inst : Mul α] [inst_1 : Preorder α] [inst_2 : Preorder β] {f g : β → α} [MulLeftMono α]
  [MulRightMono α], Antitone f → Antitone g → Antitone fun x => f x * g x
-- Mathlib.Combinatorics.SimpleGraph.Density
/-- Density of edges of a graph between two finsets of vertices.  -/
SimpleGraph.edgeDensity : {α : Type u_4} → (G : SimpleGraph α) → [DecidableRel G.Adj] → Finset α → Finset α → ℚ
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.insertMany_list_eq_foldl : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {l : List α},
  t.insertMany l = List.foldl (fun acc a => acc.insert a) t l
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
/-- Auxiliary definition for `HasCokernels SemiNormedGrp`.  -/
SemiNormedGrp.cokernelLift : {X Y : SemiNormedGrp} →
  (f : X ⟶ Y) → (s : CategoryTheory.Limits.CokernelCofork f) → (SemiNormedGrp.cokernelCocone f).pt ⟶ s.pt
-- Init.Data.List.Nat.TakeDrop
List.take_set_of_le : ∀ {α : Type u_1} {a : α} {i j : ℕ} {l : List α}, j ≤ i → List.take j (l.set i a) = List.take j l
-- Mathlib.Algebra.BigOperators.RingEquiv
RingEquiv.map_multiset_sum : ∀ {R : Type u_2} {S : Type u_3} [inst : NonUnitalNonAssocSemiring R] [inst_1 : NonUnitalNonAssocSemiring S]
  (f : R ≃+* S) (s : Multiset R), f s.sum = (Multiset.map (⇑f) s).sum
-- Mathlib.Order.TransfiniteIteration
transfiniteIterate_limit : ∀ {I : Type u} [inst : SupSet I] (φ : I → I) {J : Type w} [inst_1 : LinearOrder J] [inst_2 : SuccOrder J]
  [inst_3 : WellFoundedLT J] (i₀ : I) (j : J),
  Order.IsSuccLimit j → transfiniteIterate φ j i₀ = ⨆ x, transfiniteIterate φ (↑x) i₀
-- Init.Data.List.Range
List.range'_eq_nil_iff : ∀ {s n step : ℕ}, List.range' s n step = [] ↔ n = 0
-- Std.Sat.AIG.If
Std.Sat.AIG.RefVec.IfInput.mk.sizeOf_spec : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α} {w : ℕ} [inst_2 : SizeOf α]
  (discr : aig.Ref) (lhs rhs : aig.RefVec w),
  sizeOf { discr := discr, lhs := lhs, rhs := rhs } = 1 + sizeOf discr + sizeOf lhs + sizeOf rhs
-- Mathlib.Analysis.RCLike.Basic
LinearIsometryEquiv.trans.congr_simp : ∀ {R : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} {E : Type u_5} {E₂ : Type u_6} {E₃ : Type u_7} [inst : Semiring R]
  [inst_1 : Semiring R₂] [inst_2 : Semiring R₃] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {σ₁₃ : R →+* R₃} {σ₃₁ : R₃ →+* R}
  {σ₂₃ : R₂ →+* R₃} {σ₃₂ : R₃ →+* R₂} [inst_3 : RingHomInvPair σ₁₂ σ₂₁] [inst_4 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_5 : RingHomInvPair σ₁₃ σ₃₁] [inst_6 : RingHomInvPair σ₃₁ σ₁₃] [inst_7 : RingHomInvPair σ₂₃ σ₃₂]
  [inst_8 : RingHomInvPair σ₃₂ σ₂₃] [inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [inst_10 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁]
  [inst_11 : SeminormedAddCommGroup E] [inst_12 : SeminormedAddCommGroup E₂] [inst_13 : SeminormedAddCommGroup E₃]
  [inst_14 : Module R E] [inst_15 : Module R₂ E₂] [inst_16 : Module R₃ E₃] (e e_1 : E ≃ₛₗᵢ[σ₁₂] E₂),
  e = e_1 → ∀ (e' e'_1 : E₂ ≃ₛₗᵢ[σ₂₃] E₃), e' = e'_1 → e.trans e' = e_1.trans e'_1
-- Mathlib.GroupTheory.CosetCover
AddSubgroup.pairwiseDisjoint_leftCoset_cover_of_sum_neg_index_eq_zero : ∀ {G : Type u_1} [inst : AddGroup G] {ι : Type u_2} {H : ι → AddSubgroup G} {g : ι → G} {s : Finset ι},
  ⋃ i ∈ s, g i +ᵥ ↑(H i) = Set.univ →
    ∀ [inst_1 : DecidablePred AddSubgroup.FiniteIndex],
      ∑ i ∈ s, (↑(H i).index)⁻¹ = 1 → (↑({i ∈ s | (H i).FiniteIndex})).PairwiseDisjoint fun i => g i +ᵥ ↑(H i)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.max!_eq_default : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.isEmpty = true → t.max! = default
-- Aesop.Tree.Data
Aesop.Goal.id : Aesop.Goal → Aesop.GoalId
-- Mathlib.Analysis.Normed.Operator.Banach
ContinuousLinearMap.isQuotientMap : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜'] {σ : 𝕜 →+* 𝕜'}
  {E : Type u_3} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {F : Type u_4}
  [inst_4 : NormedAddCommGroup F] [inst_5 : NormedSpace 𝕜' F] (f : E →SL[σ] F) {σ' : 𝕜' →+* 𝕜} [RingHomInvPair σ σ']
  [RingHomIsometric σ] [RingHomIsometric σ'] [CompleteSpace F] [CompleteSpace E],
  Function.Surjective ⇑f → Topology.IsQuotientMap ⇑f
-- Mathlib.RingTheory.WittVector.Compare
TruncatedWittVector.commutes' : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ) {m : ℕ} (hm : n ≤ m) (x : ZMod (p ^ m)),
  (TruncatedWittVector.truncate hm) ((TruncatedWittVector.zmodEquivTrunc p m) x) =
    (TruncatedWittVector.zmodEquivTrunc p n) ((ZMod.castHom ⋯ (ZMod (p ^ n))) x)
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
_private.Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE.0.CategoryTheory.Triangulated.TStructure.TruncAux.triangle_obj₂ : ∀ {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 : ℤ) (X : C),
  (CategoryTheory.Triangulated.TStructure.TruncAux.triangle✝ t n X).obj₂ = X
-- Init.While
/-- The body of `repeatM`: run `f a`, recurse via `recur` on `.inl`, return on `.inr`.  -/
repeatM.body : {α : Type u} → {m : Type u → Type v} → [Monad m] → {β : Type u} → (α → m (α ⊕ β)) → (α → m β) → α → m β
-- Init.PropLemmas
forall_or_imp_or_self_right_right : ∀ {α : Sort u_1} {P Q R : α → Prop}, (∀ (a : α), P a ∨ Q a → R a ∨ Q a) ↔ ∀ (a : α), P a → R a ∨ Q a
-- Init.Data.Nat.Basic
Nat.not_gt_eq : ∀ (a b : ℕ), (¬a > b) = (a ≤ b)
-- Mathlib.Data.Set.Prod
Set.offDiag_nonempty : ∀ {α : Type u_1} {s : Set α}, s.offDiag.Nonempty ↔ s.Nontrivial
-- Mathlib.RingTheory.FreeCommRing
FreeCommRing.induction_on : ∀ {α : Type u} {motive : FreeCommRing α → Prop} (z : FreeCommRing α),
  motive (-1) →
    (∀ (b : α), motive (FreeCommRing.of b)) →
      (∀ (x y : FreeCommRing α), motive x → motive y → motive (x + y)) →
        (∀ (x y : FreeCommRing α), motive x → motive y → motive (x * y)) → motive z
-- Mathlib.Order.Hom.Bounded
BotHom.symm_dual_comp : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : LE α] [inst_1 : OrderBot α] [inst_2 : LE β] [inst_3 : OrderBot β]
  [inst_4 : LE γ] [inst_5 : OrderBot γ] (g : TopHom βᵒᵈ γᵒᵈ) (f : TopHom αᵒᵈ βᵒᵈ),
  BotHom.dual.symm (g.comp f) = (BotHom.dual.symm g).comp (BotHom.dual.symm f)
-- Lean.Parser.Level
Lean.Parser.Level.paren : Lean.Parser.Parser
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.forget_faithful : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T}, (CategoryTheory.Over.forget X).Faithful
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.hasCompactSupport : ∀ {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {n : ℕ∞} {K : TopologicalSpace.Compacts E} (f : ContDiffMapSupportedIn E F n K),
  HasCompactSupport ⇑f
-- Mathlib.Order.Antisymmetrization
instIsTransAntisymmRel : ∀ {α : Type u_1} {r : α → α → Prop} [IsTrans α r], IsTrans α (AntisymmRel r)
-- Mathlib.Algebra.Group.Basic
neg_nsmul : ∀ {α : Type u_1} [inst : SubtractionMonoid α] (a : α) (n : ℕ), n • -a = -(n • a)
-- Lean.Meta.Tactic.Grind.Intro
Lean.Meta.Grind.Goal.lastDecl? : Lean.Meta.Grind.Goal → Lean.MetaM (Option Lean.LocalDecl)
-- Init.Prelude
/-- Version of `Array.get!Internal` that does not increment the reference count of its result.

This is only intended for direct use by the compiler.
 -/
Array.get!InternalBorrowed : {α : Type u} → [Inhabited α] → Array α → ℕ → α
-- Mathlib.RingTheory.Regular.Category
/-- **Alias** of `LinearMap.exact_lsmul_mkQ_smul_top`. -/
LinearMap.exact_smul_id_smul_top_mkQ : ∀ {R : Type u} [inst : CommRing R] (M : Type v) [inst_1 : AddCommGroup M] [inst_2 : Module R M] (r : R),
  Function.Exact ⇑((LinearMap.lsmul R M) r) ⇑(r • ⊤).mkQ
-- Init.Data.Range.Basic
Std.Legacy.Range.size.eq_1 : ∀ (r : Std.Legacy.Range), r.size = (r.stop - r.start + r.step - 1) / r.step
-- Mathlib.Data.DFinsupp.Module
/-- `DFinsupp.filter` as a `LinearMap`.  -/
DFinsupp.filterLinearMap : {ι : Type u} →
  (γ : Type w) →
    (β : ι → Type v) →
      [inst : Semiring γ] →
        [inst_1 : (i : ι) → AddCommMonoid (β i)] →
          [inst_2 : (i : ι) → Module γ (β i)] →
            (p : ι → Prop) → [DecidablePred p] → (Π₀ (i : ι), β i) →ₗ[γ] Π₀ (i : ι), β i
-- Mathlib.Topology.Constructions.SumProd
Continuous.sumMap : ∀ {X : Type u} {Y : Type v} {W : Type u_1} {Z : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace W] [inst_3 : TopologicalSpace Z] {f : X → Y} {g : Z → W},
  Continuous f → Continuous g → Continuous (Sum.map f g)
-- Mathlib.Combinatorics.SimpleGraph.Diam
SimpleGraph.radius_eq_iInf_iSup_edist : ∀ {α : Type u_1} {G : SimpleGraph α}, G.radius = ⨅ u, ⨆ v, G.edist u v
-- Lean.MonadEnv
Lean.getConstInfo : {m : Type → Type} → [Monad m] → [Lean.MonadEnv m] → [Lean.MonadError m] → Lean.Name → m Lean.ConstantInfo
-- Mathlib.CategoryTheory.ObjectProperty.Local
CategoryTheory.MorphismProperty.instIsClosedUnderColimitsOfShapeIsColocal : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) (J : Type u')
  [inst_1 : CategoryTheory.Category.{v', u'} J], W.isColocal.IsClosedUnderColimitsOfShape J
-- Mathlib.Computability.Partrec
Computable.snd : ∀ {α : Type u_1} {β : Type u_2} [inst : Primcodable α] [inst_1 : Primcodable β], Computable Prod.snd
-- Init.Data.Int.DivMod.Lemmas
Int.tmod_eq_zero_of_dvd : ∀ {a b : ℤ}, a ∣ b → b.tmod a = 0
-- Mathlib.Algebra.Ring.Subring.IntPolynomial
Polynomial.int_monic_iff : ∀ {K : Type u_1} [inst : Field K] (R : Subring K) (P : Polynomial K) (hP : ∀ (n : ℕ), P.coeff n ∈ R),
  (Polynomial.int R P hP).Monic ↔ P.Monic
-- Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
Additive.ofMul_lt : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, Additive.ofMul a < Additive.ofMul b ↔ a < b
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.map_tensor_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.Monoidal] {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y') {Z : D}
  (h : F.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Y') ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategoryStruct.tensorHom f g)) h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.δ F X X')
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (F.map f) (F.map g))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F Y Y') h))
-- Mathlib.RingTheory.MvPowerSeries.Equiv
MvPowerSeries.toAdicCompletionAlgEquiv_symm_apply : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommRing R] [inst_1 : Finite σ]
  (x : AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)),
  (MvPowerSeries.toAdicCompletionAlgEquiv σ R).symm x = MvPowerSeries.toAdicCompletionInv σ R x
-- Mathlib.Data.Multiset.Defs
Multiset.card_pmap : ∀ {α : Type u_1} {β : Type v} {p : α → Prop} (f : (a : α) → p a → β) (s : Multiset α) (H : ∀ a ∈ s, p a),
  (Multiset.pmap f s H).card = s.card
-- Mathlib.Analysis.Normed.Module.Basic
/-- Warning: This declaration should be used judiciously.
Please consider using `IsScalarTower` instead.

This definition allows the `RestrictScalars.normedSpace` instance to be put directly on `E`
rather on `RestrictScalars 𝕜 𝕜' E`. This would be a very bad instance; both because `𝕜'` cannot be
inferred, and because it is likely to create instance diamonds.

See Note [reducible non-instances].
 -/
NormedSpace.restrictScalars : (𝕜 : Type u_1) →
  (𝕜' : Type u_2) →
    (E : Type u_3) →
      [inst : NormedField 𝕜] →
        [inst_1 : NormedField 𝕜'] →
          [NormedAlgebra 𝕜 𝕜'] → [inst_3 : SeminormedAddCommGroup E] → [NormedSpace 𝕜' E] → NormedSpace 𝕜 E
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.contains_congr : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {k k' : α},
  cmp k k' = Ordering.eq → t.contains k = t.contains k'
-- Mathlib.Algebra.Order.Ring.Unbundled.Rat
Rat.num_nonpos : ∀ {a : ℚ}, a.num ≤ 0 ↔ a ≤ 0