mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Convex.Segment
/-- A point is in an `Icc` iff it can be expressed as a convex combination of the endpoints.  -/
Convex.mem_Icc : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {x y z : 𝕜},
  x ≤ y → (z ∈ Set.Icc x y ↔ ∃ a b, 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ a * x + b * y = z)
-- Mathlib.MeasureTheory.Function.L2Space
MeasureTheory.MemLp.inner_const : ∀ {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {E : Type u_2} {𝕜 : Type u_3}
  [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {f : α → E},
  MeasureTheory.MemLp f p μ → ∀ (c : E), MeasureTheory.MemLp (fun a => inner 𝕜 (f a) c) p μ
-- Mathlib.Tactic.NormNum.Result
Mathlib.Meta.NormNum.Result'.isNNRat.sizeOf_spec : ∀ (inst : Lean.Expr) (q : ℚ) (n d proof : Lean.Expr),
  sizeOf (Mathlib.Meta.NormNum.Result'.isNNRat inst q n d proof) =
    1 + sizeOf inst + sizeOf q + sizeOf n + sizeOf d + sizeOf proof
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.minKey?_eq_none_iff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → (t.minKey? = none ↔ t.isEmpty = true)
-- Mathlib.NumberTheory.FLT.Four
/-- We can swap `a` and `b` in a minimal solution to `a ^ 4 + b ^ 4 = c ^ 2`.  -/
Fermat42.minimal_comm : ∀ {a b c : ℤ}, Fermat42.Minimal a b c → Fermat42.Minimal b a c
-- Mathlib.Topology.Clopen
IsClopen.himp : ∀ {X : Type u} [inst : TopologicalSpace X] {s t : Set X}, IsClopen s → IsClopen t → IsClopen (s ⇨ t)
-- Mathlib.RingTheory.Regular.RegularSequence
/-- A simplified version of `IsWeaklyRegular.recIterModByRegularWithRing` where
the motive is not allowed to depend on the proof of `IsWeaklyRegular`.  -/
RingTheory.Sequence.IsWeaklyRegular.ndrecWithRing : {motive :
    (R : Type u) → [inst : CommRing R] → (M : Type v) → [inst_1 : AddCommGroup M] → [Module R M] → List R → Sort u_7} →
  ((R : Type u) →
      [inst : CommRing R] → (M : Type v) → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → motive R M []) →
    ({R : Type u} →
        [inst : CommRing R] →
          {M : Type v} →
            [inst_1 : AddCommGroup M] →
              [inst_2 : Module R M] →
                (r : R) →
                  (rs : List R) →
                    IsSMulRegular M r →
                      RingTheory.Sequence.IsWeaklyRegular (QuotSMulTop r M)
                          (List.map (⇑(Ideal.Quotient.mk (Ideal.span {r}))) rs) →
                        motive (R ⧸ Ideal.span {r}) (QuotSMulTop r M)
                            (List.map (⇑(Ideal.Quotient.mk (Ideal.span {r}))) rs) →
                          motive R M (r :: rs)) →
      {R : Type u} →
        [inst : CommRing R] →
          {M : Type v} →
            [inst_1 : AddCommGroup M] →
              [inst_2 : Module R M] → {rs : List R} → RingTheory.Sequence.IsWeaklyRegular M rs → motive R M rs
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.canonicalEquiv_coeIdeal : ∀ {R : Type u_1} [inst : CommRing R] (S : Submonoid R) (P : Type u_2) [inst_1 : CommRing P] [inst_2 : Algebra R P]
  (P' : Type u_3) [inst_3 : CommRing P'] [inst_4 : Algebra R P'] [inst_5 : IsLocalization S P]
  [inst_6 : IsLocalization S P'] (I : Ideal R), (FractionalIdeal.canonicalEquiv S P P') ↑I = ↑I
-- Batteries.Data.Array.Basic
_private.Batteries.Data.Array.Basic.0.Array.SizeFitsUSize : {α : Type u_1} → Array α → Prop
-- Mathlib.Data.Complex.Basic
Complex.mul_conj : ∀ (z : ℂ), z * (starRingEnd ℂ) z = ↑(Complex.normSq z)
-- Init.Data.List.Lemmas
List.mem_of_ne_of_mem : ∀ {α : Type u_1} {a y : α} {l : List α}, a ≠ y → a ∈ y :: l → a ∈ l
-- Mathlib.RingTheory.PowerSeries.Expand
PowerSeries.expand_X : ∀ {R : Type u_2} [inst : CommRing R] (p : ℕ) (hp : p ≠ 0), (PowerSeries.expand p hp) PowerSeries.X = PowerSeries.X ^ p
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.getKey_alterKey : ∀ {α : Type u} [inst : BEq α] {β : Type v} [inst_1 : EquivBEq α] {k k' : α} {f : Option β → Option β}
  (l : List ((_ : α) × β)) (hl : Std.Internal.List.DistinctKeys l)
  (hc : Std.Internal.List.containsKey k' (Std.Internal.List.Const.alterKey k f l) = true),
  Std.Internal.List.getKey k' (Std.Internal.List.Const.alterKey k f l) hc =
    if heq : (k == k') = true then k else Std.Internal.List.getKey k' l ⋯
-- Mathlib.RingTheory.Ideal.Quotient.Operations
Ideal.quotientKerAlgEquivOfSurjective.congr_simp : ∀ {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R₁] [inst_1 : Ring A] [inst_2 : Algebra R₁ A]
  [inst_3 : Semiring B] [inst_4 : Algebra R₁ B] {f : A →ₐ[R₁] B} (hf : Function.Surjective ⇑f),
  Ideal.quotientKerAlgEquivOfSurjective hf = Ideal.quotientKerAlgEquivOfSurjective hf
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrpObj.ofIso_add : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {G' X : C} [inst_2 : CategoryTheory.AddGrpObj G'] (e : G' ≅ X),
  CategoryTheory.AddMonObj.add =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom e.inv e.inv)
      (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add e.hom)
-- Mathlib.GroupTheory.Nilpotent
/-- If two different elements of the `upperCentralSeries` of a group `G` are equal, then
they are all equal, starting from the smaller index.  -/
Subgroup.upperCentralSeries.eq_ge_of_eq_gt : ∀ {G : Type u_1} [inst : Group G] {a b c : ℕ},
  a ≠ b →
    a ≤ c →
      Subgroup.upperCentralSeries G a = Subgroup.upperCentralSeries G b →
        Subgroup.upperCentralSeries G a = Subgroup.upperCentralSeries G c
-- Mathlib.CategoryTheory.PathCategory.Basic
/-- Any prefunctor from `V` lifts to a functor from `paths V`  -/
CategoryTheory.Paths.lift : {V : Type u₁} →
  [inst : Quiver V] →
    {C : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} C] → V ⥤q C → CategoryTheory.Functor (CategoryTheory.Paths V) C
-- Mathlib.CategoryTheory.Filtered.Basic
PSigma.mk.hcongr_4 : ∀ (α α' : Sort u),
  α = α' →
    ∀ (β : α → Sort v) (β' : α' → Sort v),
      β ≍ β' →
        ∀ (fst : α) (fst' : α'), fst ≍ fst' → ∀ (snd : β fst) (snd' : β' fst'), snd ≍ snd' → ⟨fst, snd⟩ ≍ ⟨fst', snd'⟩
-- Mathlib.Order.Interval.Set.Defs
Set.Iio.eq_1 : ∀ {α : Type u_1} [inst : Preorder α] (b : α), Set.Iio b = {x | x < b}
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.size_alter_le_size : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {f : Option β → Option β}, (Std.DTreeMap.Raw.Const.alter t k f).size ≤ t.size + 1
-- Mathlib.Data.Nat.Bits
Nat.testBit_bit_succ : ∀ (m : ℕ) (b : Bool) (n : ℕ), (Nat.bit b n).testBit m.succ = n.testBit m
-- Mathlib.Order.ModularLattice
infIccOrderIsoIccSup_symm_apply_coe : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : IsModularLattice α] (a b : α) (x : ↑(Set.Icc b (a ⊔ b))),
  ↑((RelIso.symm (infIccOrderIsoIccSup a b)) x) = a ⊓ ↑x
-- Mathlib.RepresentationTheory.Action
Representation.LinearizeMonoidal.ε_toLinearMap : ∀ (k : Type u) (G : Type v) [inst : Monoid G] [inst_1 : Semiring k],
  (Representation.LinearizeMonoidal.ε k G).toLinearMap = ↑(MonoidAlgebra.uniqueLinearEquiv k PUnit.{w + 1}).symm
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey?_maxKey? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {km : α}, t.maxKey? = some km → t.getKey? km = some km
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.nndist_fst_le : ∀ {p : ENNReal} {α : Type u_2} {β : Type u_3} [hp : Fact (1 ≤ p)] [inst : PseudoMetricSpace α]
  [inst_1 : PseudoMetricSpace β] (x y : WithLp p (α × β)), nndist x.fst y.fst ≤ nndist x y
-- Mathlib.Algebra.BigOperators.Group.Finset.Sigma
Finset.prod_product_right : ∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : CommMonoid β] (s : Finset γ) (t : Finset α) (f : γ × α → β),
  ∏ x ∈ s ×ˢ t, f x = ∏ y ∈ t, ∏ x ∈ s, f (x, y)
-- Mathlib.Analysis.Convex.Join
convexJoin_subset_convexHull : ∀ {𝕜 : Type u_2} {E : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] (s t : Set E), convexJoin 𝕜 s t ⊆ (convexHull 𝕜) (s ∪ t)
-- Init.System.Promise
/-- `Promise α` allows you to create a `Task α` whose value is provided later by calling `resolve`.

Typical usage is as follows:
1. `let promise ← Promise.new` creates a promise
2. `promise.result? : Task (Option α)` can now be passed around
3. `promise.result?.get` blocks until the promise is resolved
4. `promise.resolve a` resolves the promise
5. `promise.result?.get` now returns `some a`

If the promise is dropped without ever being resolved, `promise.result?.get` will return `none`.
See `Promise.result!/resultD` for other ways to handle this case.
 -/
IO.Promise : Type → Type
-- Init.Data.Range.Polymorphic.RangeIterator
_private.Init.Data.Range.Polymorphic.RangeIterator.0.Std.Rxi.Iterator.instIteratorLoop.loop.wf : {α : Type u} →
  [inst : Std.PRange.UpwardEnumerable α] →
    [Std.PRange.LawfulUpwardEnumerable α] →
      {n : Type u → Type w} →
        [Monad n] →
          (γ : Type u) →
            (Pl : α → γ → ForInStep γ → Prop) →
              Std.IteratorLoop.WellFounded (Std.Rxi.Iterator α) Id Pl →
                (LargeEnough : α → Prop) →
                  (∀ (a b : α), Std.PRange.UpwardEnumerable.LE a b → LargeEnough a → LargeEnough b) →
                    γ →
                      (next : α) →
                        LargeEnough next → ((out : α) → LargeEnough out → (c : γ) → n { s // Pl out c s }) → n γ
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.faithful_map : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {A' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] {B' : Type u₅} [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  {T' : Type u₆} [inst_5 : CategoryTheory.Category.{v₆, u₆} T'] {L : CategoryTheory.Functor A T}
  {R : CategoryTheory.Functor B T} {L' : CategoryTheory.Functor A' T'} {R' : CategoryTheory.Functor B' T'}
  {F₁ : CategoryTheory.Functor A A'} {F₂ : CategoryTheory.Functor B B'} {F : CategoryTheory.Functor T T'}
  (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') [F₁.Faithful] [F₂.Faithful],
  (CategoryTheory.Comma.map α β).Faithful
-- Mathlib.Order.Cover
WCovBy.rfl : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, a ⩿ a
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Arrow.equivSigma_apply_snd_snd : ∀ (T : Type u) [inst : CategoryTheory.Category.{v, u} T] (f : CategoryTheory.Arrow T),
  ((CategoryTheory.Arrow.equivSigma T) f).snd.snd = f.hom
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionItem.kind? : Lean.Lsp.CompletionItem → Option Lean.Lsp.CompletionItemKind
-- Mathlib.Analysis.Convex.Intrinsic
/-- **Alias** of `AffineIsometry.intrinsicInterior_image`. -/
AffineIsometry.image_intrinsicInterior : ∀ {𝕜 : Type u_1} {V : Type u_2} {W : Type u_3} {Q : Type u_4} {P : Type u_5} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V] [inst_2 : SeminormedAddCommGroup W] [inst_3 : NormedSpace 𝕜 V]
  [inst_4 : NormedSpace 𝕜 W] [inst_5 : MetricSpace P] [inst_6 : PseudoMetricSpace Q] [inst_7 : NormedAddTorsor V P]
  [inst_8 : NormedAddTorsor W Q] (φ : P →ᵃⁱ[𝕜] Q) (s : Set P),
  intrinsicInterior 𝕜 (⇑φ '' s) = ⇑φ '' intrinsicInterior 𝕜 s
-- Mathlib.Algebra.Polynomial.Laurent
Polynomial.toLaurent_C_mul_X_pow : ∀ {R : Type u_1} [inst : Semiring R] (n : ℕ) (r : R),
  Polynomial.toLaurent (Polynomial.C r * Polynomial.X ^ n) = LaurentPolynomial.C r * LaurentPolynomial.T ↑n
-- Mathlib.GroupTheory.Congruence.Defs
Con.semigroup.eq_1 : ∀ {M : Type u_4} [inst : Semigroup M] (c : Con M), c.semigroup = { toMul := c.hasMul, mul_assoc := ⋯ }
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
/-- Let `f : E → F` be a function differentiable in a neighborhood of `a`.
If $Df(x) = O(‖x - a‖ ^ r)$ as `x → a`, where `r ≥ 0`, and `f a = 0`,
then $f(x) = O(‖x - a‖ ^ {r + 1})$ as `x → a`.  -/
isBigO_norm_rpow_add_one_of_fderiv_of_apply_eq_zero : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {f : E → F} {a : E} {r : ℝ},
  0 ≤ r →
    (∀ᶠ (x : E) in nhds a, DifferentiableAt ℝ f x) →
      (fderiv ℝ f =O[nhds a] fun x => ‖x - a‖ ^ r) → f a = 0 → f =O[nhds a] fun x => ‖x - a‖ ^ (r + 1)
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Rel.below.pentagon : ∀ {B : Type u} [inst : Quiver B]
  {motive :
    {a b : CategoryTheory.FreeBicategory B} →
      {f g : a ⟶ b} →
        (a_1 a_2 : CategoryTheory.FreeBicategory.Hom₂ f g) → CategoryTheory.FreeBicategory.Rel a_1 a_2 → Prop}
  {a b c d e : B} (f : CategoryTheory.FreeBicategory.Hom a b) (g : CategoryTheory.FreeBicategory.Hom b c)
  (h : CategoryTheory.FreeBicategory.Hom c d) (i : CategoryTheory.FreeBicategory.Hom d e),
  CategoryTheory.FreeBicategory.Rel.below ⋯
-- Mathlib.Data.ENat.Basic
/-- **Alias** of `ENat.natCast_lift`. -/
ENat.coe_lift : ∀ (x : ℕ∞) (h : x < ⊤), ↑(x.lift h) = x
-- Mathlib.ModelTheory.Order
FirstOrder.Language.instModelPartialOrderTheoryOfLinearOrderTheory : ∀ (L : FirstOrder.Language) {M : Type w'} [inst : L.IsOrdered] [inst_1 : L.Structure M] [h : M ⊨ L.linearOrderTheory],
  M ⊨ L.partialOrderTheory
-- Std.Data.Internal.List.Associative
Std.Internal.List.eraseKey_nil : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {k : α}, Std.Internal.List.eraseKey k [] = []
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.Nontrivial.add_right : ∀ {α : Type u_2} [inst : Add α] [IsRightCancelAdd α] [inst_2 : DecidableEq α] {s t : Finset α},
  s.Nontrivial → t.Nonempty → (s + t).Nontrivial
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.Scheme.Hom.liftQuotient_comp : ∀ {X : AlgebraicGeometry.Scheme} {A : CommRingCat} (f : X.Hom (AlgebraicGeometry.Spec A)) (I : Ideal ↑A)
  (hI :
    I ≤
      RingHom.ker
        (CommRingCat.Hom.hom (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ΓSpecIso A).inv f.appTop))),
  CategoryTheory.CategoryStruct.comp (f.liftQuotient I hI)
      (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I))) =
    f
-- Mathlib.AlgebraicGeometry.Spec
AlgebraicGeometry.StructureSheaf.toPushforwardStalk_comp : ∀ {R S : CommRingCat} (f : R ⟶ S) (p : PrimeSpectrum ↑R),
  CategoryTheory.CategoryStruct.comp f (AlgebraicGeometry.StructureSheaf.toPushforwardStalk f p) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.StructureSheaf.toStalk (↑R) p)
      ((TopCat.Presheaf.stalkFunctor CommRingCat p).map (AlgebraicGeometry.Spec.sheafedSpaceMap f).hom.c)
-- Mathlib.CategoryTheory.Triangulated.SpectralObject
CategoryTheory.Triangulated.SpectralObject.comp_hom : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Limits.HasZeroObject C]
  [inst_3 : CategoryTheory.HasShift C ℤ] [inst_4 : CategoryTheory.Preadditive C]
  [inst_5 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_6 : CategoryTheory.Pretriangulated C]
  {X Y Z : CategoryTheory.Triangulated.SpectralObject C ι} (α : X ⟶ Y) (β : Y ⟶ Z),
  (CategoryTheory.CategoryStruct.comp α β).hom = CategoryTheory.CategoryStruct.comp α.hom β.hom
-- Mathlib.NumberTheory.NumberField.Ideal.Basic
Ideal.torsionMapQuot_apply : ∀ {K : Type u_1} [inst : Field K] (I : Ideal (NumberField.RingOfIntegers K)) {x : (NumberField.RingOfIntegers K)ˣ}
  (hx : x ∈ NumberField.Units.torsion K), ↑(I.torsionMapQuot ⟨x, hx⟩) = (Ideal.Quotient.mk I) ↑x
-- Mathlib.Analysis.Normed.Ring.Basic
/-- `nnnorm` as a `MonoidWithZeroHom`.  -/
nnnormHom : {α : Type u_2} → [inst : SeminormedRing α] → [NormOneClass α] → [NormMulClass α] → α →*₀ NNReal
-- Mathlib.Topology.Constructible
Topology.IsConstructible.iUnion : ∀ {ι : Sort u_1} {X : Type u_2} [inst : TopologicalSpace X] [Finite ι] {f : ι → Set X},
  (∀ (i : ι), Topology.IsConstructible (f i)) → Topology.IsConstructible (⋃ i, f i)
-- Lean.Parser.Extra
/-- The parser `hexnum` parses a hexadecimal numeric literal not containing the `0x` prefix.

It produces a `hexnumKind` node containing an atom with the text of the
literal. This parser is mainly used for creating atoms such `#<hexnum>`. Recall that `hexnum`
is not a token and this parser must be prefixed by another parser.

For numerals such as `0xadef100a`, you should use `numLit`.
 -/
Lean.Parser.hexnum : Lean.Parser.Parser
-- Mathlib.CategoryTheory.Shift.CommShift
CategoryTheory.Functor.map_shiftFunctorComm : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {A : Type u_4} [inst_2 : AddCommMonoid A]
  [inst_3 : CategoryTheory.HasShift C A] [inst_4 : CategoryTheory.HasShift D A] (F : CategoryTheory.Functor C D)
  [inst_5 : F.CommShift A] (X : C) (a b : A),
  F.map ((CategoryTheory.shiftFunctorComm C a b).hom.app X) =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Functor.commShiftIso F b).hom.app ((CategoryTheory.shiftFunctor C a).obj X))
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.shiftFunctor D b).map ((CategoryTheory.Functor.commShiftIso F a).hom.app X))
        (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorComm D a b).hom.app (F.obj X))
          (CategoryTheory.CategoryStruct.comp
            ((CategoryTheory.shiftFunctor D a).map ((CategoryTheory.Functor.commShiftIso F b).inv.app X))
            ((CategoryTheory.Functor.commShiftIso F a).inv.app ((CategoryTheory.shiftFunctor C b).obj X)))))
-- Mathlib.CategoryTheory.Triangulated.Opposite.Triangle
CategoryTheory.Pretriangulated.TriangleOpEquivalence.inverse_obj : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  (T : CategoryTheory.Pretriangulated.Triangle Cᵒᵖ),
  (CategoryTheory.Pretriangulated.TriangleOpEquivalence.inverse C).obj T =
    Opposite.op
      (CategoryTheory.Pretriangulated.Triangle.mk T.mor₂.unop T.mor₁.unop
        (CategoryTheory.CategoryStruct.comp
          ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C 1).unitIso.inv.app T.obj₁).unop
          ((CategoryTheory.shiftFunctor C 1).map T.mor₃.unop)))
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Polynomial.Chebyshev.eval_T_real_node : ∀ {n i : ℕ}, i ∈ Finset.Iic n → Polynomial.eval (Polynomial.Chebyshev.node n i) (Polynomial.Chebyshev.T ℝ ↑n) = (-1) ^ i
-- Mathlib.Algebra.Algebra.Opposite
AlgEquiv.toOpposite_symm_apply : ∀ (R : Type u_1) (A : Type u_3) [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Algebra R A] (a : Aᵐᵒᵖ),
  (AlgEquiv.toOpposite R A).symm a = MulOpposite.unop a
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.continuousWithinAt_iff : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {f : α → β} {a : α} {s : Set α},
  ContinuousWithinAt f s a ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, x ∈ s → dist x a < δ → dist (f x) (f a) < ε
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonColor : Lean.FromJson Lean.Lsp.Color
-- Mathlib.Analysis.Asymptotics.ExpGrowth
ExpGrowth.le_expGrowthInf_mul : ∀ {u v : ℕ → ENNReal}, ExpGrowth.expGrowthInf u + ExpGrowth.expGrowthInf v ≤ ExpGrowth.expGrowthInf (u * v)
-- Mathlib.CategoryTheory.Equivalence.Symmetry
/-- The `inverse` functor that sends a functor to its inverse.  -/
CategoryTheory.Equivalence.inverseFunctor : (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] → CategoryTheory.Functor (C ≌ D) (CategoryTheory.Functor D C)ᵒᵖ
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.unitOfList_eq_insertManyIfNewUnit_empty : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {l : List α},
  Std.DHashMap.Raw.Const.unitOfList l = Std.DHashMap.Raw.Const.insertManyIfNewUnit ∅ l
-- Mathlib.Combinatorics.Matroid.Closure
/-- **Alias** of `Matroid.Indep.insert_sdiff_indep_iff`.

---

This can be used for rewriting if the LHS is inside a binder and it is unknown
whether `f = e`.  -/
Matroid.Indep.insert_diff_indep_iff : ∀ {α : Type u_2} {M : Matroid α} {e f : α} {I : Set α},
  M.Indep (I \ {e}) → e ∈ I → (M.Indep (insert f I \ {e}) ↔ f ∈ M.E \ M.closure (I \ {e}) ∨ f ∈ I)
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated
SSet.Truncated.Edge.CompStruct.mk.injEq : ∀ {X : SSet.Truncated 2}
  {x₀ x₁ x₂ : X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge._proof_1 })}
  {e₀₁ : SSet.Truncated.Edge x₀ x₁} {e₁₂ : SSet.Truncated.Edge x₁ x₂} {e₀₂ : SSet.Truncated.Edge x₀ x₂}
  (simplex : X.obj (Opposite.op { obj := { len := 2 }, property := SSet.Truncated.Edge.CompStruct._proof_1 }))
  (d₂ :
    autoParam
      ((CategoryTheory.ConcreteCategory.hom
            (X.map
              (SimplexCategory.Truncated.δ₂ 2 SSet.Truncated.Edge._proof_2 SSet.Truncated.Edge.CompStruct._proof_2).op))
          simplex =
        e₀₁.edge)
      SSet.Truncated.Edge.CompStruct.d₂._autoParam)
  (d₀ :
    autoParam
      ((CategoryTheory.ConcreteCategory.hom
            (X.map
              (SimplexCategory.Truncated.δ₂ 0 SSet.Truncated.Edge._proof_2 SSet.Truncated.Edge.CompStruct._proof_2).op))
          simplex =
        e₁₂.edge)
      SSet.Truncated.Edge.CompStruct.d₀._autoParam)
  (d₁ :
    autoParam
      ((CategoryTheory.ConcreteCategory.hom
            (X.map
              (SimplexCategory.Truncated.δ₂ 1 SSet.Truncated.Edge._proof_2 SSet.Truncated.Edge.CompStruct._proof_2).op))
          simplex =
        e₀₂.edge)
      SSet.Truncated.Edge.CompStruct.d₁._autoParam)
  (simplex_1 : X.obj (Opposite.op { obj := { len := 2 }, property := SSet.Truncated.Edge.CompStruct._proof_1 }))
  (d₂_1 :
    autoParam
      ((CategoryTheory.ConcreteCategory.hom
            (X.map
              (SimplexCategory.Truncated.δ₂ 2 SSet.Truncated.Edge._proof_2 SSet.Truncated.Edge.CompStruct._proof_2).op))
          simplex_1 =
        e₀₁.edge)
      SSet.Truncated.Edge.CompStruct.d₂._autoParam)
  (d₀_1 :
    autoParam
      ((CategoryTheory.ConcreteCategory.hom
            (X.map
              (SimplexCategory.Truncated.δ₂ 0 SSet.Truncated.Edge._proof_2 SSet.Truncated.Edge.CompStruct._proof_2).op))
          simplex_1 =
        e₁₂.edge)
      SSet.Truncated.Edge.CompStruct.d₀._autoParam)
  (d₁_1 :
    autoParam
      ((CategoryTheory.ConcreteCategory.hom
            (X.map
              (SimplexCategory.Truncated.δ₂ 1 SSet.Truncated.Edge._proof_2 SSet.Truncated.Edge.CompStruct._proof_2).op))
          simplex_1 =
        e₀₂.edge)
      SSet.Truncated.Edge.CompStruct.d₁._autoParam),
  ({ simplex := simplex, d₂ := d₂, d₀ := d₀, d₁ := d₁ } =
      { simplex := simplex_1, d₂ := d₂_1, d₀ := d₀_1, d₁ := d₁_1 }) =
    (simplex = simplex_1)
-- Std.Data.ExtTreeMap.Lemmas
_private.Std.Data.ExtTreeMap.Lemmas.0.GetElem?.match_1.splitter : (elem : outParam (Type u_1)) →
  (motive : Option elem → Sort u_2) →
    (x : Option elem) → ((e : elem) → motive (some e)) → (Unit → motive none) → motive x
-- Mathlib.Geometry.Euclidean.NinePointCircle
Affine.Simplex.midpoint_faceOppositeCentroid_eulerPoint : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [hn : NeZero n] (s : Affine.Simplex ℝ P n) (i : Fin (n + 1)),
  midpoint ℝ (s.faceOppositeCentroid i) (s.eulerPoint i) = s.ninePointCircle.center
-- Mathlib.Order.Interval.Finset.Defs
instLocallyFiniteOrderBotSubtypeLtOfDecidableLTOfLocallyFiniteOrder : {α : Type u_1} →
  [inst : Preorder α] → {y : α} → [DecidableLT α] → [LocallyFiniteOrder α] → LocallyFiniteOrderBot { x // y < x }
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
CategoryTheory.StrictlyUnitaryLaxFunctor.id_obj : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (X : B), (CategoryTheory.StrictlyUnitaryLaxFunctor.id B).obj X = X
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.toCLM_apply : ∀ {m : Type u_1} {n : Type u_2} {A : Type u_5} [inst : Fintype m] [inst_1 : NonUnitalCStarAlgebra A]
  {M : CStarMatrix m n A} {v : WithCStarModule A (m → A)},
  (CStarMatrix.toCLM M) v = (WithCStarModule.equiv A (n → A)).symm (Matrix.vecMul v M)