mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
/-- **Alias** of `InnerProductSpace.gramSchmidtOrthonormalBasis_inv_isUpperTriangular`.

---

Given an indexed family `f : ι → E` of vectors in an inner product space `E`, for which the
size of the index set is the dimension of `E`, the matrix of coefficients of `f` with respect to the
orthonormal basis `gramSchmidtOrthonormalBasis` constructed from `f` is upper-triangular.  -/
InnerProductSpace.gramSchmidtOrthonormalBasis_inv_blockTriangular : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_3} [inst_3 : LinearOrder ι] [inst_4 : LocallyFiniteOrderBot ι] [inst_5 : WellFoundedLT ι]
  [inst_6 : Fintype ι] [inst_7 : FiniteDimensional 𝕜 E] (h : Module.finrank 𝕜 E = Fintype.card ι) (f : ι → E),
  ((InnerProductSpace.gramSchmidtOrthonormalBasis h f).toBasis.toMatrix f).IsUpperTriangular
-- Init.Data.Rat.Lemmas
Rat.pow_one : ∀ (q : ℚ), q ^ 1 = q
-- Mathlib.Data.Finset.Pi
/-- If a function `f` is restricted to a finite set `t`, and `s ⊆ t`,
this is the restriction to `s`.  -/
Finset.restrict₂ : {ι : Type u_2} → {π : ι → Type u_3} → {s t : Finset ι} → s ⊆ t → ((i : ↥t) → π ↑i) → (i : ↥s) → π ↑i
-- Mathlib.Data.Finsupp.Multiset
Multiset.toFinsupp_support : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Multiset α), (Multiset.toFinsupp s).support = s.toFinset
-- Mathlib.Data.Num.Bitwise
/-- Bitwise "and" for `PosNum`.  -/
PosNum.land : PosNum → PosNum → Num
-- Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
curveIntegral_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {a b : E} {γ : Path a b},
  curveIntegral 0 γ = 0
-- Mathlib.Algebra.Homology.TotalComplexShift
/-- The shift on bicomplexes obtained by shifting the first indices (and changing the
sign of differentials).  -/
HomologicalComplex₂.shiftFunctor₁ : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      ℤ →
        CategoryTheory.Functor (HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ))
          (HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ))
-- Init.System.IOError
instInhabitedError : Inhabited IO.Error
-- Lean.Parser.Term
Lean.Parser.Term.type.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.rootSet.congr_simp : ∀ {T : Type w} [inst : CommRing T] (p p_1 : Polynomial T),
  p = p_1 →
    ∀ (S : Type u_1) [inst_1 : CommRing S] [inst_2 : IsDomain S] [inst_3 : Algebra T S] (a a_1 : S),
      a = a_1 → p.rootSet S a = p_1.rootSet S a_1
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.coe_toSubring : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] (S : Subalgebra R A),
  ↑S.toSubring = ↑S
-- Mathlib.Analysis.InnerProductSpace.PiL2
/-- The change-of-basis matrix between two orthonormal bases `a`, `b` is an orthogonal matrix.  -/
OrthonormalBasis.toMatrix_orthonormalBasis_mem_orthogonal : ∀ {ι : Type u_1} {F : Type u_5} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] [inst_2 : Fintype ι]
  [inst_3 : DecidableEq ι] (a b : OrthonormalBasis ι ℝ F), a.toBasis.toMatrix ⇑b ∈ Matrix.orthogonalGroup ι ℝ
-- Mathlib.Data.Nat.Init
Nat.leRecOn_self : ∀ {C : ℕ → Sort u_1} {n : ℕ} {next : {k : ℕ} → C k → C (k + 1)} (x : C n), Nat.leRecOn ⋯ (fun {k} => next) x = x
-- Mathlib.Order.Basic
lt_self_iff_false : ∀ {α : Type u_2} [inst : Preorder α] (x : α), x < x ↔ False
-- Lean.PrettyPrinter.Delaborator.Options
Lean.pp.proofs.threshold : Lean.Option ℕ
-- Mathlib.Topology.Algebra.Group.Basic
Units.range_embedProduct : ∀ {α : Type u} [inst : Monoid α],
  Set.range ⇑(Units.embedProduct α) = {p | p.1 * MulOpposite.unop p.2 = 1 ∧ MulOpposite.unop p.2 * p.1 = 1}
-- Init.Data.Vector.Lemmas
Vector.toList_insertIdx! : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i : ℕ} {x : α}, i ≤ n → (xs.insertIdx! i x).toList = xs.toList.insertIdx i x
-- Mathlib.NumberTheory.Real.GoldenRatio
/-- The golden ratio `φ := (1 + √5)/2`.  -/
Real.goldenRatio : ℝ
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Arrow.mk_eq : ∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] (f : CategoryTheory.Arrow T), CategoryTheory.Arrow.mk f.hom = f
-- Mathlib.Data.List.Nodup
List.count_eq_one_of_mem : ∀ {α : Type u} [inst : BEq α] [LawfulBEq α] {a : α} {l : List α}, l.Nodup → a ∈ l → List.count a l = 1
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.hasColimit_leftOp_iff_hasLimit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  {F : CategoryTheory.Functor J Cᵒᵖ}, CategoryTheory.Limits.HasColimit F.leftOp ↔ CategoryTheory.Limits.HasLimit F
-- Mathlib.MeasureTheory.Measure.Typeclasses.Probability
MeasureTheory.isProbabilityMeasureSMul : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] [NeZero μ],
  MeasureTheory.IsProbabilityMeasure ((μ Set.univ)⁻¹ • μ)
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
LinearMap.withSeminorms_induced : ∀ {𝕜 : Type u_2} {𝕜₂ : Type u_3} {E : Type u_6} {F : Type u_7} {ι : Type u_9} [inst : NormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] [inst_3 : NormedField 𝕜₂] [inst_4 : AddCommGroup F]
  [inst_5 : Module 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_6 : RingHomIsometric σ₁₂] [inst_7 : TopologicalSpace F]
  {q : SeminormFamily 𝕜₂ F ι}, WithSeminorms q → ∀ (f : E →ₛₗ[σ₁₂] F), WithSeminorms (q.comp f)
-- Mathlib.Algebra.Category.AlgCat.Basic
AlgCat.restrictScalarsEquivalenceOfRingEquiv_counitIso : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S),
  (AlgCat.restrictScalarsEquivalenceOfRingEquiv e).counitIso =
    (AlgCat.restrictScalarsComp' e.toRingHom e.symm.toRingHom (RingHom.id R) ⋯).symm ≪≫
      AlgCat.restrictScalarsId' (RingHom.id R) ⋯
-- Mathlib.Data.Tree.Basic
BinaryTree.right.eq_1 : ∀ {α : Type u}, BinaryTree.nil.right = BinaryTree.nil
-- Mathlib.Data.Seq.Defs
Stream'.Seq.BisimO.eq_3 : ∀ {α : Type u} (R : Stream'.Seq α → Stream'.Seq α → Prop) (x x_1 : Option (Stream'.Seq1 α)),
  (x = none → x_1 = none → False) →
    (∀ (a : α) (s : Stream'.Seq α) (a' : α) (s' : Stream'.Seq α), x = some (a, s) → x_1 = some (a', s') → False) →
      Stream'.Seq.BisimO R x x_1 = False
-- Mathlib.MeasureTheory.Function.AEMeasurableSequence
aeSeq.aeSeq_n_eq_fun_n_ae : ∀ {ι : Sort u_1} {α : Type u_2} {β : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {f : ι → α → β}
  {μ : MeasureTheory.Measure α} {p : α → (ι → β) → Prop} [Countable ι] (hf : ∀ (i : ι), AEMeasurable (f i) μ),
  (∀ᵐ (x : α) ∂μ, p x fun n => f n x) → ∀ (n : ι), aeSeq hf p n =ᵐ[μ] f n
-- Init.Prelude
/-- The homogeneous version of `HAnd`: `a &&& b : α` where `a b : α`.
(It is called `AndOp` because `And` is taken for the propositional connective.)
 -/
AndOp : Type u → Type u
-- Lean.Meta.Tactic.Grind.AC.Seq
/-- `s₁.startsWith s₂` checks whether `s₁` begins with `s₂`.
 -/
_private.Lean.Meta.Tactic.Grind.AC.Seq.0.Lean.Grind.AC.Seq.startsWith : Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Lean.Grind.AC.StartsWithResult✝
-- Init.Data.String.Lemmas.Splits
/-- Given a position that splits `s` into `t₁ ++ t₂` and `t₃` with witness `h`, construct a position
`h.rotateLeft` that splits `s` into `t₁` and `t₂ ++ t₃`. Use `h.splits_rotateLeft` for the witness
that `h.rotateLEft` splits `s` as required.
 -/
String.Slice.Pos.Splits.rotateLeft : {s : String.Slice} → {p : s.Pos} → {t₁ t₂ t₃ : String} → p.Splits (t₁ ++ t₂) t₃ → s.Pos
-- Mathlib.Analysis.InnerProductSpace.Spectrum
_private.Mathlib.Analysis.InnerProductSpace.Spectrum.0.LinearMap.IsSymmetric.hasEigenvalue_unsortedEigenvalues : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E →ₗ[𝕜] E} [inst_3 : FiniteDimensional 𝕜 E] {n : ℕ} (hT : T.IsSymmetric) (hn : Module.finrank 𝕜 E = n)
  (i : Fin n), Module.End.HasEigenvalue T ↑(LinearMap.IsSymmetric.unsortedEigenvalues✝ hT hn i)
-- Mathlib.CategoryTheory.Limits.MorphismProperty
/-- If `P` is stable under composition, base change and satisfies post-cancellation,
`P.Over ⊤ X` has pullbacks  -/
CategoryTheory.MorphismProperty.Over.hasPullbacks : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] (P : CategoryTheory.MorphismProperty T) (X : T)
  [CategoryTheory.Limits.HasPullbacks T] [P.IsStableUnderComposition] [P.IsStableUnderBaseChange]
  [P.HasOfPostcompProperty P], CategoryTheory.Limits.HasPullbacks (P.Over ⊤ X)
-- Init.Data.List.Sublist
List.IsPrefix.reverse : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <+: l₂ → l₁.reverse <:+ l₂.reverse
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.cooper₂.inj : ∀ {c c_1 : Lean.Meta.Grind.Arith.Cutsat.CooperSplit},
  Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.cooper₂ c = Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.cooper₂ c_1 →
    c = c_1
-- Mathlib.RingTheory.Extension.Generators
/-- If `S` is the localization of `R` away from `r`, we obtain a canonical generator mapping
to the inverse of `r`.  -/
Algebra.Generators.localizationAway : {R : Type u} →
  (S : Type v) →
    [inst : CommRing R] →
      [inst_1 : CommRing S] → [inst_2 : Algebra R S] → (r : R) → [IsLocalization.Away r S] → Algebra.Generators R S Unit
-- Mathlib.Algebra.Category.MonCat.Basic
/-- The underlying type.  -/
MonCat.carrier : MonCat → Type u
-- Mathlib.Tactic.ClickSuggestions.FindPremises
Mathlib.Tactic.ClickSuggestions.PreDiscrTrees.mk.sizeOf_spec : ∀ (rw : Lean.Meta.RefinedDiscrTree.PreDiscrTree Mathlib.Tactic.ClickSuggestions.RwLemma)
  (grw : Lean.Meta.RefinedDiscrTree.PreDiscrTree Mathlib.Tactic.ClickSuggestions.GrwLemma)
  (app : Lean.Meta.RefinedDiscrTree.PreDiscrTree Mathlib.Tactic.ClickSuggestions.ApplyLemma)
  (appAt : Lean.Meta.RefinedDiscrTree.PreDiscrTree Mathlib.Tactic.ClickSuggestions.ApplyAtLemma),
  sizeOf { rw := rw, grw := grw, app := app, appAt := appAt } = 1 + sizeOf rw + sizeOf grw + sizeOf app + sizeOf appAt
-- Mathlib.SetTheory.Ordinal.Notation
ONote.NFBelow.zero : ∀ {b : Ordinal.{0}}, ONote.NFBelow 0 b
-- Lean.Meta.Tactic.Grind.AC.DenoteExpr
Lean.Grind.AC.Seq.denoteExpr : {M : Type → Type} → [Monad M] → [Lean.Meta.Grind.AC.MonadGetStruct M] → Lean.Grind.AC.Seq → M Lean.Expr
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
NumberField.mixedEmbedding.logMap_apply_of_norm_eq_one : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {x : NumberField.mixedEmbedding.mixedSpace K},
  NumberField.mixedEmbedding.norm x = 1 →
    ∀ (w : { w // w ≠ NumberField.Units.dirichletUnitTheorem.w₀ }),
      NumberField.mixedEmbedding.logMap x w = ↑(↑w).mult * Real.log ((NumberField.mixedEmbedding.normAtPlace ↑w) x)
-- Mathlib.Combinatorics.Matroid.Dual
Matroid.coindep_iff_exists' : ∀ {α : Type u_1} {M : Matroid α} {X : Set α}, M.Coindep X ↔ (∃ B, M.IsBase B ∧ B ⊆ M.E \ X) ∧ X ⊆ M.E
-- Mathlib.CategoryTheory.Action.Monoidal
Action.rightUnitor_inv_hom : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G]
  [inst_2 : CategoryTheory.MonoidalCategory V] (X : Action V G),
  (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv.hom =
    (CategoryTheory.MonoidalCategoryStruct.rightUnitor X.V).inv
-- Mathlib.Order.Interval.Set.InitialSeg
Set.initialSegIicIicOfLE_toFun_coe : ∀ {α : Type u_1} [inst : Preorder α] {i j : α} (h : i ≤ j) (k : ↑(Set.Iic i)), ↑((Set.initialSegIicIicOfLE h) k) = ↑k
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.tsupport_smulLeftCLM_subset : ∀ {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NontriviallyNormedField 𝕜]
  [inst_5 : NormedAlgebra ℝ 𝕜] [inst_6 : NormedSpace 𝕜 F] (g : E → 𝕜) (f : SchwartzMap E F),
  tsupport ⇑((SchwartzMap.smulLeftCLM F g) f) ⊆ tsupport ⇑f ∩ tsupport g
-- Mathlib.CategoryTheory.Core
CategoryTheory.Functor.coreComp_hom_app_iso_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D E) (X : CategoryTheory.Core C),
  ((F.coreComp G).hom.app X).iso.hom = CategoryTheory.CategoryStruct.id (G.obj (F.obj X.of))
-- Init.Core
iff_iff_implies_and_implies : ∀ {a b : Prop}, (a ↔ b) ↔ (a → b) ∧ (b → a)
-- Init.Data.Nat.Basic
Nat.add_one : ∀ (n : ℕ), n + 1 = n.succ
-- Lean.Elab.Level
_private.Lean.Elab.Level.0.Lean.Elab.Level.checkUniverseOffset : {m : Type → Type} → [Monad m] → [Lean.MonadError m] → [Lean.MonadOptions m] → ℕ → m Unit
-- Mathlib.Algebra.MvPolynomial.Monad
MvPolynomial.bind₁_bind₁ : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [inst : CommSemiring R] {υ : Type u_6} (f : σ → MvPolynomial τ R)
  (g : τ → MvPolynomial υ R) (φ : MvPolynomial σ R),
  (MvPolynomial.bind₁ g) ((MvPolynomial.bind₁ f) φ) = (MvPolynomial.bind₁ fun i => (MvPolynomial.bind₁ g) (f i)) φ
-- Mathlib.Order.Bounds.Image
Antitone.image_lowerBounds_subset_upperBounds_image : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  Antitone f → ∀ {s : Set α}, f '' lowerBounds s ⊆ upperBounds (f '' s)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.CooperSplitProof.dec.injEq : ∀ (h h_1 : Lean.FVarId),
  (Lean.Meta.Grind.Arith.Cutsat.CooperSplitProof.dec h = Lean.Meta.Grind.Arith.Cutsat.CooperSplitProof.dec h_1) =
    (h = h_1)
-- Mathlib.Algebra.Group.Action.Basic
smul_invOf_smul : ∀ {α : Type u_5} {β : Type u_6} [inst : Monoid α] [inst_1 : MulAction α β] (c : α) (x : β) [inst_2 : Invertible c],
  c • ⅟c • x = x
-- Mathlib.AlgebraicGeometry.Cover.QuasiCompact
AlgebraicGeometry.QuasiCompactCover.exists_hom : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {S : AlgebraicGeometry.Scheme}
  (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) S)
  [P.RespectsLeft AlgebraicGeometry.IsOpenImmersion] [CompactSpace ↥S]
  [AlgebraicGeometry.QuasiCompactCover 𝒰.toPreZeroHypercover],
  ∃ 𝒱 f, Finite 𝒱.I₀ ∧ ∀ (j : 𝒱.cover.I₀), AlgebraicGeometry.IsOpenImmersion (f.h₀ j)
-- Mathlib.Data.Finset.Lattice.Fold
Finset.sup'_mem : ∀ {α : Type u_2} [inst : SemilatticeSup α] (s : Set α),
  (∀ x ∈ s, ∀ y ∈ s, x ⊔ y ∈ s) →
    ∀ {ι : Type u_7} (t : Finset ι) (H : t.Nonempty) (p : ι → α), (∀ i ∈ t, p i ∈ s) → t.sup' H p ∈ s
-- Mathlib.Probability.Decision.Risk.Basic
ProbabilityTheory.bayesRisk_const' : ∀ {Θ : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_4} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧}
  {m𝓨 : MeasurableSpace 𝓨} {ℓ : Θ → 𝓨 → ENNReal},
  Measurable (Function.uncurry ℓ) →
    ∀ (μ : MeasureTheory.Measure 𝓧) [MeasureTheory.SFinite μ] (π : MeasureTheory.Measure Θ) [MeasureTheory.SFinite π],
      (μ Set.univ = ⊤ → ⨅ y, ∫⁻ (θ : Θ), ℓ θ y ∂π = 0 → ∃ y, ∫⁻ (θ : Θ), ℓ θ y ∂π = 0) →
        (μ = 0 → Nonempty 𝓨) →
          ProbabilityTheory.bayesRisk ℓ (ProbabilityTheory.Kernel.const Θ μ) π = ⨅ y, ∫⁻ (θ : Θ), ℓ θ y * μ Set.univ ∂π
-- Init.Data.Array.Sort.Lemmas
Array.mem_mergeSort : ∀ {α : Type u_1} {le : α → α → Bool} {a : α} {xs : Array α}, a ∈ xs.mergeSort le ↔ a ∈ xs
-- Mathlib.Data.Int.Cast.Lemmas
SemiconjBy.intCast_mul_intCast_mul : ∀ {α : Type u_3} [inst : Ring α] {a x y : α}, SemiconjBy a x y → ∀ (m n : ℤ), SemiconjBy (↑m * a) (↑n * x) (↑n * y)
-- Mathlib.CategoryTheory.Comma.Over.OverClass
CategoryTheory.CanonicallyOverClass.instOverClass : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      (S : C) →
        [CategoryTheory.CanonicallyOverClass X Y] → [CategoryTheory.OverClass Y S] → CategoryTheory.OverClass X S
-- Mathlib.Algebra.Order.Positive.Ring
Positive.addRightReflectLT : ∀ {M : Type u_1} [inst : AddMonoid M] [inst_1 : Preorder M] [inst_2 : AddLeftStrictMono M] [AddRightReflectLT M],
  AddRightReflectLT { x // 0 < x }
-- Mathlib.CategoryTheory.Triangulated.HomologicalFunctor
CategoryTheory.Functor.homologySequenceδ.congr_simp : ∀ {C : Type u_1} {A : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} A] (F : CategoryTheory.Functor C A) [inst_3 : F.ShiftSequence ℤ]
  (T : CategoryTheory.Pretriangulated.Triangle C) (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁),
  F.homologySequenceδ T n₀ n₁ h = F.homologySequenceδ T n₀ n₁ h
-- Mathlib.Data.WSeq.Relation
Stream'.WSeq.Equiv.equivalence : ∀ {α : Type u}, Equivalence Stream'.WSeq.Equiv
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.getKeyLED : {α : Type u} → {β : α → Type v} → [Ord α] → α → Std.DTreeMap.Internal.Impl α β → α → α
-- Mathlib.Analysis.Normed.Group.Bounded
tendsto_norm_cocompact_atTop' : ∀ {E : Type u_2} [inst : SeminormedGroup E] [ProperSpace E], Filter.Tendsto norm (Filter.cocompact E) Filter.atTop
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionItemKind : Type
-- Mathlib.Algebra.Group.Submonoid.Operations
AddMonoidHom.comap_mker : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : AddZeroClass M] [inst_1 : AddZeroClass N]
  [inst_2 : AddZeroClass P] (g : N →+ P) (f : M →+ N),
  AddSubmonoid.comap f (AddMonoidHom.mker g) = AddMonoidHom.mker (g.comp f)
-- Mathlib.Analysis.Convex.Between
wbtw_midpoint : ∀ (R : Type u_1) {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P] (x y : P),
  Wbtw R x (midpoint R x y) y
-- Lean.Parser.Attr
Lean.Parser.Attr.tactic_name.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
ContinuousMultilinearMap.instPseudoMetricSpace : {𝕜 : Type u} →
  {ι : Type v} →
    {E : ι → Type wE} →
      {G : Type wG} →
        [inst : NontriviallyNormedField 𝕜] →
          [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] →
            [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)] →
              [inst_3 : SeminormedAddCommGroup G] →
                [inst_4 : NormedSpace 𝕜 G] → [Fintype ι] → PseudoMetricSpace (ContinuousMultilinearMap 𝕜 E G)
-- Init.Grind.AC
_private.Init.Grind.AC.0.Lean.Grind.AC.Seq.erase0.match_1.eq_2 : ∀ (motive : Lean.Grind.AC.Seq → Sort u_1) (x : Lean.Grind.AC.Var) (s : Lean.Grind.AC.Seq)
  (h_1 : (x : Lean.Grind.AC.Var) → motive (Lean.Grind.AC.Seq.var x))
  (h_2 : (x : Lean.Grind.AC.Var) → (s : Lean.Grind.AC.Seq) → motive (Lean.Grind.AC.Seq.cons x s)),
  (match Lean.Grind.AC.Seq.cons x s with
    | Lean.Grind.AC.Seq.var x => h_1 x
    | Lean.Grind.AC.Seq.cons x s => h_2 x s) =
    h_2 x s
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instVAdd' : {β : Type u_2} → {α : Type u_1} → [VAdd β α] → VAdd (Lex β) α
-- Mathlib.Data.Set.Function
Function.Surjective.surjOn_preimage : ∀ {α : Type u_1} {β : Type u_2} {t : Set β} {f : α → β}, Function.Surjective f → Set.SurjOn f (f ⁻¹' t) t
-- Mathlib.Algebra.GroupWithZero.Defs
mul_self_ne_zero : ∀ {M₀ : Type u_1} [inst : MulZeroClass M₀] [NoZeroDivisors M₀] {a : M₀}, a * a ≠ 0 ↔ a ≠ 0
-- Mathlib.LinearAlgebra.RootSystem.Hom
/-- For finite roots systems in characteristic zero, a linear equivalence preserving roots, also
preserves coroots, and is thus an equivalence of root systems.  -/
RootPairing.Equiv.mk' : {ι : 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] →
                  {ι₂ : Type u_5} →
                    {M₂ : Type u_6} →
                      {N₂ : Type u_7} →
                        [inst_5 : AddCommGroup M₂] →
                          [inst_6 : Module R M₂] →
                            [inst_7 : AddCommGroup N₂] →
                              [inst_8 : Module R N₂] →
                                [IsDomain R] →
                                  [CharZero R] →
                                    [Module.IsTorsionFree R M₂] →
                                      [Finite ι₂] →
                                        (P : RootPairing ι R M N) →
                                          [P.IsRootSystem] →
                                            (Q : RootPairing ι₂ R M₂ N₂) →
                                              [Q.IsRootSystem] →
                                                (f : M ≃ₗ[R] M₂) →
                                                  (e : ι ≃ ι₂) → (∀ (i : ι), f (P.root i) = Q.root (e i)) → P.Equiv Q
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.darts_cons : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} (h : G.Adj u v) (p : G.Walk v w),
  (SimpleGraph.Walk.cons h p).darts = { fst := u, snd := v, adj := h } :: p.darts
-- Mathlib.Algebra.Polynomial.Smeval
/-- Scalar multiplication together with taking a natural number power.  -/
Polynomial.smul_pow : {R : Type u_1} →
  [inst : Semiring R] →
    {S : Type u_2} → [inst_1 : AddCommMonoid S] → [Pow S ℕ] → [MulActionWithZero R S] → S → ℕ → R → S
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.archimedeanClassMk_neg_of_tendsto_atTop : ∀ {x : ℝ*}, Filter.Germ.Tendsto x Filter.atTop → ArchimedeanClass.mk x < 0
-- Mathlib.Topology.MetricSpace.Dilation
/-- A dilation maps closed balls to closed balls and scales the radius by `ratio f`.  -/
Dilation.mapsTo_closedEBall : ∀ {α : Type u_1} {β : Type u_2} {F : Type u_4} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β]
  [inst_2 : FunLike F α β] [inst_3 : DilationClass F α β] (f : F) (x : α) (r' : ENNReal),
  Set.MapsTo (⇑f) (Metric.closedEBall x r') (Metric.closedEBall (f x) (↑(Dilation.ratio f) * r'))
-- Mathlib.Order.Filter.Map
Filter.sup_bind : ∀ {α : Type u_1} {β : Type u_2} {f g : Filter α} {h : α → Filter β}, (f ⊔ g).bind h = f.bind h ⊔ g.bind h
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
CategoryTheory.Limits.PushoutCocone.IsColimit.desc.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z}
  {t : CategoryTheory.Limits.PushoutCocone f g} (ht ht_1 : CategoryTheory.Limits.IsColimit t),
  ht = ht_1 →
    ∀ {W : C} (h h_1 : Y ⟶ W) (e_h : h = h_1) (k k_1 : Z ⟶ W) (e_k : k = k_1)
      (w : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g k),
      CategoryTheory.Limits.PushoutCocone.IsColimit.desc ht h k w =
        CategoryTheory.Limits.PushoutCocone.IsColimit.desc ht_1 h_1 k_1 ⋯
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
CategoryTheory.Limits.PullbackCone.isIso_fst_of_mono_of_isLimit : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} [CategoryTheory.Mono f]
  {t : CategoryTheory.Limits.PullbackCone f f} (ht : CategoryTheory.Limits.IsLimit t), CategoryTheory.IsIso t.fst
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometry.injective : ∀ {𝕜 : Type u_1} {V₁' : Type u_4} {V₂ : Type u_5} {P₁' : Type u_9} {P₂ : Type u_11} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V₁'] [inst_2 : NormedSpace 𝕜 V₁'] [inst_3 : MetricSpace P₁']
  [inst_4 : NormedAddTorsor V₁' P₁'] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂] (f₁ : P₁' →ᵃⁱ[𝕜] P₂), Function.Injective ⇑f₁
-- Lean.Elab.Do.InferControlInfo
/-- The `ControlInfo` of branches `a | b`: effect flags are unioned, the regular exits are summed, and
the alternative falls through iff at least one branch falls through.
 -/
Lean.Elab.Do.ControlInfo.alternative : Lean.Elab.Do.ControlInfo → Lean.Elab.Do.ControlInfo → Lean.Elab.Do.ControlInfo
-- Mathlib.Tactic.NormNum.Result
/-- Returns the rational number that is the result of `norm_num` evaluation, along with a proof
that the denominator is nonzero in the `isRat` case.  -/
Mathlib.Meta.NormNum.Result.toRatNZ : {u : Lean.Level} → {α : Q(Type u)} → {e : Q(«$α»)} → Mathlib.Meta.NormNum.Result e → Option (ℚ × Option Lean.Expr)