mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.Simps.Basic
/-- Add a lemma with `nm` stating that `lhs = rhs`. `type` is the type of both `lhs` and `rhs`,
`args` is the list of local constants occurring, and `univs` is the list of universe variables.  -/
Simps.addProjection : Lean.Syntax →
  List Lean.Name → Lean.Name → Lean.Expr → Lean.Expr → Lean.Expr → Array Lean.Expr → Simps.Config → Lean.MetaM Unit
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
/-- Lift a `MonoidHom` to `Finset` via `image`.  -/
Finset.imageMonoidHom : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : DecidableEq α] →
        [inst_1 : DecidableEq β] →
          [inst_2 : MulOneClass α] →
            [inst_3 : MulOneClass β] → [inst_4 : FunLike F α β] → [MonoidHomClass F α β] → F → Finset α →* Finset β
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem?_toList_rio : ∀ {n i : ℕ}, (*...n).toList[i]? = if i < n then some i else none
-- Lean.ResolveName
/-- Check surrounding namespaces  -/
_private.Lean.ResolveName.0.Lean.ResolveName.resolveUsingNamespace : Lean.Environment → Lean.Options → Lean.Name → Lean.Name → List Lean.Name
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
/-- Attempt to parse a `NatOffset` from an expression -/
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat.0.Nat.NatOffset.fromExprAux : Lean.Expr → ℕ → Lean.Meta.SimpM (Option (Lean.Expr × ℕ))
-- Mathlib.Topology.Instances.NNReal.Lemmas
/-- `x ↦ x ^ n` as an order isomorphism of `ℝ≥0`.  -/
NNReal.powOrderIso : (n : ℕ) → n ≠ 0 → NNReal ≃o NNReal
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated
SSet.Truncated.Edge.instSubsingleton : ∀ {X : SSet.Truncated 2}
  [Subsingleton (X.obj (Opposite.op { obj := { len := 1 }, property := SSet.Truncated.Edge._proof_2 }))]
  {x y : X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge._proof_1 })},
  Subsingleton (SSet.Truncated.Edge x y)
-- Mathlib.Tactic.FieldSimp
_private.Mathlib.Tactic.FieldSimp.0.Mathlib.Tactic.FieldSimp.qNF.mul.match_1.eq_3 : ∀ {v : Lean.Level} {M : Q(Type v)}
  (motive : Mathlib.Tactic.FieldSimp.qNF q(«$M») → Mathlib.Tactic.FieldSimp.qNF q(«$M») → Sort u_1) (a₁ : ℤ)
  (x₁ : Q(«$M»)) (k₁ : ℕ) (t₁ : List ((ℤ × Q(«$M»)) × ℕ)) (a₂ : ℤ) (x₂ : Q(«$M»)) (k₂ : ℕ)
  (t₂ : List ((ℤ × Q(«$M»)) × ℕ)) (h_1 : (l : Mathlib.Tactic.FieldSimp.qNF q(«$M»)) → motive [] l)
  (h_2 : (l : Mathlib.Tactic.FieldSimp.qNF q(«$M»)) → motive l [])
  (h_3 :
    (a₁ : ℤ) →
      (x₁ : Q(«$M»)) →
        (k₁ : ℕ) →
          (t₁ : List ((ℤ × Q(«$M»)) × ℕ)) →
            (a₂ : ℤ) →
              (x₂ : Q(«$M»)) →
                (k₂ : ℕ) → (t₂ : List ((ℤ × Q(«$M»)) × ℕ)) → motive (((a₁, x₁), k₁) :: t₁) (((a₂, x₂), k₂) :: t₂)),
  (match ((a₁, x₁), k₁) :: t₁, ((a₂, x₂), k₂) :: t₂ with
    | [], l => h_1 l
    | l, [] => h_2 l
    | ((a₁, x₁), k₁) :: t₁, ((a₂, x₂), k₂) :: t₂ => h_3 a₁ x₁ k₁ t₁ a₂ x₂ k₂ t₂) =
    h_3 a₁ x₁ k₁ t₁ a₂ x₂ k₂ t₂
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
HasDerivWithinAt.cpow : ∀ {f g : ℂ → ℂ} {s : Set ℂ} {f' g' x : ℂ},
  HasDerivWithinAt f f' s x →
    HasDerivWithinAt g g' s x →
      f x ∈ Complex.slitPlane →
        HasDerivWithinAt (fun x => f x ^ g x) (g x * f x ^ (g x - 1) * f' + f x ^ g x * Complex.log (f x) * g') s x
-- Mathlib.CategoryTheory.Category.Pointed
/-- Turns a point into a pointed type.  -/
Pointed.of : {X : Type u_1} → X → Pointed
-- Mathlib.Topology.Algebra.Module.Equiv
/-- `Fin.cons` in the codomain of continuous linear maps.  -/
ContinuousLinearMap.finCons : {n : ℕ} →
  {R : Type u_4} →
    {M : Fin n.succ → Type u_5} →
      {N : Type u_6} →
        [inst : Semiring R] →
          [inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)] →
            [inst_2 : (i : Fin n.succ) → Module R (M i)] →
              [inst_3 : (i : Fin n.succ) → TopologicalSpace (M i)] →
                [inst_4 : AddCommMonoid N] →
                  [inst_5 : Module R N] →
                    [inst_6 : TopologicalSpace N] →
                      (N →L[R] M 0) → (N →L[R] (i : Fin n) → M i.succ) → N →L[R] (i : Fin n.succ) → M i
-- Mathlib.Algebra.MonoidAlgebra.Defs
/-- The multiplication in a monoid algebra.

We make it irreducible so that Lean doesn't unfold it when trying to unify two different things.  -/
MonoidAlgebra.mul' : {R : Type u_1} →
  {M : Type u_4} → [inst : Semiring R] → [Mul M] → MonoidAlgebra R M → MonoidAlgebra R M → MonoidAlgebra R M
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.EqCnstrProof.simp_middle.sizeOf_spec : ∀ (lhs : Bool) (s₁ s₂ : Lean.Grind.AC.Seq) (c₁ c₂ : Lean.Meta.Grind.AC.EqCnstr),
  sizeOf (Lean.Meta.Grind.AC.EqCnstrProof.simp_middle lhs s₁ s₂ c₁ c₂) =
    1 + sizeOf lhs + sizeOf s₁ + sizeOf s₂ + sizeOf c₁ + sizeOf c₂
-- Mathlib.RingTheory.Extension.Presentation.Core
/-- An arbitrarily chosen relation exhibiting the fact that `P.jacobian` is invertible,
provided `P.HasCoeffs R₀`.  -/
Algebra.SubmersivePresentation.jacobianRelationsOfHasCoeffs : {R : Type u_1} →
  {S : Type u_2} →
    {ι : Type u_3} →
      {σ : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : CommRing S] →
            [inst_2 : Algebra R S] →
              [inst_3 : Finite σ] →
                (P : Algebra.SubmersivePresentation R S ι σ) →
                  (R₀ : Type u_5) →
                    [inst_4 : CommRing R₀] →
                      [inst_5 : Algebra R₀ R] →
                        [inst_6 : Algebra R₀ S] →
                          [inst_7 : IsScalarTower R₀ R S] → [P.HasCoeffs R₀] → σ → MvPolynomial ι R₀
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Equiv.refl_toHom : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M],
  (FirstOrder.Language.Equiv.refl L M).toHom = FirstOrder.Language.Hom.id L M
-- Mathlib.Dynamics.Flow
IsInvariant.eq_1 : ∀ {τ : Type u_1} {α : Type u_2} (ϕ : τ → α → α) (s : Set α), IsInvariant ϕ s = ∀ (t : τ), Set.MapsTo (ϕ t) s s
-- Mathlib.GroupTheory.ArchimedeanDensely
/-- If an element of a linearly ordered mul-archimedean group is the least element greater than 1,
then the whole group is isomorphic (and order-isomorphic) to the multiplicative integers.  -/
LinearOrderedCommGroup.multiplicative_int_orderMonoidIso_of_isLeast_one_lt : {G : Type u_1} →
  [inst : CommGroup G] →
    [inst_1 : LinearOrder G] →
      [IsOrderedMonoid G] → [MulArchimedean G] → {x : G} → IsLeast {y | 1 < y} x → G ≃*o Multiplicative ℤ
-- Mathlib.Algebra.Order.Interval.Basic
Interval.mul_bot : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : Mul α] [inst_2 : MulLeftMono α] [inst_3 : MulRightMono α]
  (s : Interval α), s * ⊥ = ⊥
-- Init.Grind.Ring.Basic
Lean.Grind.Semiring.natCast_succ : ∀ {α : Type u} [inst : Lean.Grind.Semiring α] (n : ℕ), ↑(n + 1) = ↑n + 1
-- Mathlib.RingTheory.Congruence.BigOperators
RingCon.coe_dfinsuppSum : ∀ {ι : Type u_1} {β : ι → Type u_2} {M : Type u_3} [inst : DecidableEq ι] [inst_1 : AddCommMonoid M] [inst_2 : Mul M]
  [inst_3 : (i : ι) → Zero (β i)] [inst_4 : (i : ι) → (y : β i) → Decidable (y ≠ 0)] (c : RingCon M)
  (h : (i : ι) → β i → M) (f : Π₀ (i : ι), β i), ↑(f.sum h) = f.sum fun i b => ↑(h i b)
-- Mathlib.LinearAlgebra.Multilinear.Curry
LinearMap.uncurryLeft_apply : ∀ {R : Type uR} {n : ℕ} {M : Fin n.succ → Type v} {M₂ : Type v₂} [inst : CommSemiring R]
  [inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)] [inst_2 : AddCommMonoid M₂]
  [inst_3 : (i : Fin n.succ) → Module R (M i)] [inst_4 : Module R M₂]
  (f : M 0 →ₗ[R] MultilinearMap R (fun i => M i.succ) M₂) (m : (i : Fin n.succ) → M i),
  f.uncurryLeft m = (f (m 0)) (Fin.tail m)
-- Mathlib.Order.Filter.Tendsto
Filter.tendsto_map'_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : β → γ} {g : α → β} {x : Filter α} {y : Filter γ},
  Filter.Tendsto f (Filter.map g x) y ↔ Filter.Tendsto (f ∘ g) x y
-- Init.Data.Int.DivMod.Lemmas
Int.mul_dvd_mul_right : ∀ {b c : ℤ} (a : ℤ), b ∣ c → b * a ∣ c * a
-- Mathlib.RingTheory.Jacobson.Ideal
Ideal.isLocal_iff : ∀ {R : Type u} [inst : CommRing R] {I : Ideal R}, I.IsLocal ↔ I.jacobson.IsMaximal
-- Init.Data.Nat.Coprime
Nat.Coprime.eq_1 : ∀ (m n : ℕ), m.Coprime n = (m.gcd n = 1)
-- Mathlib.Order.SuccPred.Basic
Order.lt_succ : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] [NoMaxOrder α] (a : α), a < Order.succ a
-- Mathlib.Analysis.InnerProductSpace.StandardSubspace
/-- A standard subspace `S` of a complex Hilbert space (or just an inner product space) `H` is a
closed real subspace `S` such that `S ⊓ i S = ⊥` and `S ⊔ i S = ⊤`.  -/
StandardSubspace : (H : Type u_1) → [inst : NormedAddCommGroup H] → [InnerProductSpace ℂ H] → Type u_1
-- Mathlib.Order.Interval.Set.OrdConnected
Set.not_ordConnected_inter_Icc_iff : ∀ {α : Type u_1} [inst : PartialOrder α] {s : Set α} {x y : α},
  x ∈ s → y ∈ s → (¬(s ∩ Set.Icc x y).OrdConnected ↔ ∃ z ∉ s, z ∈ Set.Ioo x y)
-- Mathlib.Data.Set.Insert
Set.singleton_subset_singleton : ∀ {α : Type u_1} {a b : α}, {a} ⊆ {b} ↔ a = b
-- Std.Data.TreeMap.Lemmas
_private.Std.Data.TreeMap.Lemmas.0.GetElem?.match_1.eq_2 : ∀ (elem : outParam (Type u_1)) (motive : Option elem → Sort u_2) (h_1 : (e : elem) → motive (some e))
  (h_2 : Unit → motive none),
  (match none with
    | some e => h_1 e
    | none => h_2 ()) =
    h_2 ()
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
AlgebraicGeometry.instLocallyQuasiFiniteOfIsPreimmersion : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsPreimmersion f],
  AlgebraicGeometry.LocallyQuasiFinite f
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey?_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp] [inst : BEq α]
  [Std.LawfulBEqCmp cmp],
  t.WF →
    ∀ {l : List (α × β)} {k : α}, (List.map Prod.fst l).contains k = false → (t.insertMany l).getKey? k = t.getKey? k
-- Mathlib.RingTheory.NonUnitalSubring.Defs
NonUnitalSubring.instNonUnitalSubringClass : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R], NonUnitalSubringClass (NonUnitalSubring R) R
-- Mathlib.Logic.Equiv.Sum
Equiv.sumCompl_symm_apply_pos : ∀ {α : Type u_9} {p : α → Prop} [inst : DecidablePred p] (x : { x // p x }), (Equiv.sumCompl p).symm ↑x = Sum.inl x
-- Mathlib.RingTheory.QuotSMulTop
QuotSMulTop.equivTensorQuot_naturality_mk : ∀ {R : Type u_2} [inst : CommRing R] (r : R) {M : Type u_1} {M' : Type u_3} [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup M'] [inst_4 : Module R M'] (f : M →ₗ[R] M') (x : M),
  (QuotSMulTop.equivTensorQuot r M') (((QuotSMulTop.map r) f) (Submodule.Quotient.mk x)) =
    (LinearMap.rTensor (R ⧸ Ideal.span {r}) f) ((QuotSMulTop.equivTensorQuot r M) (Submodule.Quotient.mk x))
-- Mathlib.Data.List.Sigma
List.NodupKeys.map₁ : ∀ {α : Type u} {α' : Type u'} {β : Type v} (f : α → α'),
  Function.Injective f → ∀ {l : List ((_ : α) × β)}, l.NodupKeys → (List.map (Sigma.map f fun x => id) l).NodupKeys
-- Init.Data.Order.Lemmas
Std.instTrichotomousOfTotal : ∀ {α : Sort u_1} (r : α → α → Prop) [Std.Total r], Std.Trichotomous r
-- Mathlib.Algebra.Group.Action.Defs
SMulCommClass.op_left : ∀ {M : Type u_1} {N : Type u_2} {α : Type u_5} [inst : SMul M α] [inst_1 : SMul Mᵐᵒᵖ α] [IsCentralScalar M α]
  [inst_3 : SMul N α] [SMulCommClass M N α], SMulCommClass Mᵐᵒᵖ N α
-- Mathlib.Algebra.Order.Floor.Ring
Int.fract_eq_iff : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] [IsOrderedRing R] {a b : R},
  Int.fract a = b ↔ 0 ≤ b ∧ b < 1 ∧ ∃ z, a - b = ↑z
-- Mathlib.Analysis.Calculus.FDeriv.Prod
differentiableOn_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {ι : Type u_6} {F' : ι → Type u_7}
  [inst_1 : (i : ι) → NormedAddCommGroup (F' i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (F' i)] (i : ι)
  (s' : Set ((i : ι) → F' i)), DifferentiableOn 𝕜 (fun f => f i) s'
-- Mathlib.NumberTheory.ModularForms.Basic
/-- The `SlashInvariantForm` associated to a `ModularForm`.  -/
ModularForm.toSlashInvariantForm : {Γ : Subgroup (GL (Fin 2) ℝ)} → {k : ℤ} → ModularForm Γ k → SlashInvariantForm Γ k
-- Init.Core
/-- `x ≈ y` says that `x` and `y` are equivalent. Because this is a typeclass,
the notion of equivalence is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `≈` in identifiers is `equiv`. -/
«term_≈_» : Lean.TrailingParserDescr
-- Init.Data.SInt.Lemmas
Int8.le_of_eq : ∀ {a b : Int8}, a = b → a ≤ b
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
/-- Replace the indexing type of a pre-`0`-hypercover.  -/
CategoryTheory.PreZeroHypercover.reindex : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {T : C} → (E : CategoryTheory.PreZeroHypercover T) → {ι : Type w'} → ι ≃ E.I₀ → CategoryTheory.PreZeroHypercover T
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms_le_monomorphisms : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (G : C),
  CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms G ≤ CategoryTheory.MorphismProperty.monomorphisms C
-- Mathlib.CategoryTheory.Triangulated.Opposite.Basic
CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_counitIso_inv_naturality_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ] (n : ℤ)
  {X Y : Cᵒᵖ} (f : X ⟶ Y) {Z : Cᵒᵖ}
  (h :
    (CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).functor.obj
        ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).inverse.obj Y) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp f
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).counitIso.inv.app Y) h) =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).counitIso.inv.app X)
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.shiftFunctor Cᵒᵖ n).map ((CategoryTheory.shiftFunctor C n).map f.unop).op) h)
-- Mathlib.Analysis.Calculus.Deriv.Shift
derivWithin_comp_const_sub : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] (f : 𝕜 → F) (a : 𝕜) (s : Set 𝕜) (x : 𝕜),
  derivWithin (fun x => f (a - x)) s x = -derivWithin f (a +ᵥ -s) (a - x)
-- Mathlib.Order.PFilter
Order.PFilter.mem_of_le : ∀ {P : Type u_1} [inst : Preorder P] {x y : P} {F : Order.PFilter P}, x ≤ y → x ∈ F → y ∈ F
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.instInv : {ι : Type u_1} → (G : ι → Type u_4) → [inst : (i : ι) → Group (G i)] → Inv (Monoid.CoprodI G)
-- Mathlib.Order.Closure
ClosureOperator.mk : {α : Type u_1} →
  [inst : Preorder α] →
    (toOrderHom : α →o α) →
      (∀ (x : α), x ≤ toOrderHom.toFun x) →
        (∀ (x : α), toOrderHom.toFun (toOrderHom.toFun x) = toOrderHom.toFun x) →
          (IsClosed : α → Prop) →
            autoParam (∀ {x : α}, IsClosed x ↔ toOrderHom.toFun x = x) ClosureOperator.isClosed_iff._autoParam →
              ClosureOperator α
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
/-- If `cons (exp, coef) tl` is `Sorted`, then `coef` and `tl` are `Sorted`, and the
leading exponent of `tl` is less than `exp`.  -/
Tactic.ComputeAsymptotics.MultiseriesExpansion.Sorted.elim_cons : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis} {exp : ℝ}
  {coef : Tactic.ComputeAsymptotics.MultiseriesExpansion basis_tl}
  {tl : Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl} {f : ℝ → ℝ},
  (Tactic.ComputeAsymptotics.MultiseriesExpansion.mk
        (Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.cons exp coef tl) f).Sorted →
    coef.Sorted ∧ tl.leadingExp < ↑exp ∧ tl.Sorted
-- Lean.LocalContext
/-- Auxiliary local declaration for recursive calls.
The behavior is similar to `implDetail`.

For example: `def foo (n : Nat) : Nat := _` adds the local declaration
`foo : Nat → Nat` to allow recursive calls.
This declaration has the `auxDecl` kind.
 -/
Lean.LocalDeclKind.auxDecl : Lean.LocalDeclKind
-- Mathlib.GroupTheory.Congruence.Defs
AddCon.instMembershipProd.eq_1 : ∀ {M : Type u_1} [inst : Add M], AddCon.instMembershipProd = { mem := fun c x => c x.1 x.2 }
-- Mathlib.RepresentationTheory.Intertwining
LinearMap.toIntertwiningMap : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Semiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : Module A V] [inst_5 : Module A W]
  (ρ : Representation A G V) (σ : Representation A G W) (f : V →ₗ[A] W)
  (hf : ∀ (g : G) (v : V), f ((ρ g) v) = (σ g) (f v)) (v : V),
  (LinearMap.intertwiningMap_of_isIntertwiningMap ρ σ f hf) v = f v
-- Mathlib.Tactic.Algebra.Lemmas
Mathlib.Tactic.Algebra.rat_rawCast_neg : ∀ {n d : ℕ} {R : Type u_3} [inst : DivisionRing R],
  Rat.rawCast (Int.negOfNat n) d = (Int.negOfNat n).rawCast / d.rawCast
-- Mathlib.CategoryTheory.Shift.Opposite
/-- The functor `F.op`, seen as a functor from `OppositeShift C A` to `OppositeShift D A`.
(We will use this to carry a `CommShift` instance for the naive shifts on the opposite category.
Then, in the pretriangulated case, we will be able to put a `CommShift` instance on `F.op`
for the modified shifts and not deal with instance clashes.)
 -/
CategoryTheory.OppositeShift.functor : {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_3) →
          [inst_2 : AddMonoid A] →
            [inst_3 : CategoryTheory.HasShift C A] →
              [inst_4 : CategoryTheory.HasShift D A] →
                CategoryTheory.Functor C D →
                  CategoryTheory.Functor (CategoryTheory.OppositeShift C A) (CategoryTheory.OppositeShift D A)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Polynomial.Chebyshev.eval_iterate_derivative_le_of_forall_abs_le_one : ∀ {n : ℕ} {P : Polynomial ℝ} {k : ℕ} {x : ℝ},
  1 ≤ x →
    P.degree ≤ ↑n →
      (∀ x ∈ Set.Icc (-1) 1, |Polynomial.eval x P| ≤ 1) →
        Polynomial.eval x ((⇑Polynomial.derivative)^[k] P) ≤
          Polynomial.eval x ((⇑Polynomial.derivative)^[k] (Polynomial.Chebyshev.T ℝ ↑n))
-- Mathlib.Data.Finset.Lattice.Lemmas
Finset.inter_singleton_of_notMem : ∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {s : Finset α}, a ∉ s → s ∩ {a} = ∅
-- Mathlib.Geometry.Manifold.ChartedSpace
/-- A chart on the discrete space is the constant chart.  -/
chartedSpace_of_discreteTopology_chartAt : ∀ {H : Type u} {M : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace H] [inst_2 : DiscreteTopology M]
  [h : Unique H] {x : M}, chartAt H x = OpenPartialHomeomorph.const ⋯ ⋯
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.iSup_eq_lsub_iff_lt_iSup : ∀ {ι : Type u_3} (f : ι → Ordinal.{max u_4 u_3}), iSup f = Ordinal.lsub f ↔ ∀ (i : ι), f i < iSup f
-- Mathlib.Order.Cover
WCovBy.ge_of_gt : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c : α}, b ⩿ a → b < c → a ≤ c
-- Init.Data.List.Sort.Impl
List.MergeSort.Internal.splitRevInTwo'_snd : ∀ {α : Type u_1} {n : ℕ} (l : { l // l.length = n }),
  (List.MergeSort.Internal.splitRevInTwo' l).2 =
    ⟨(↑(List.MergeSort.Internal.splitInTwo ⟨(↑l).reverse, ⋯⟩).1).reverse, ⋯⟩
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
ContMDiffWithinAt.congr : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f f₁ : M → M'} {s : Set M} {x : M}
  {n : WithTop ℕ∞},
  ContMDiffWithinAt I I' n f s x → (∀ y ∈ s, f₁ y = f y) → f₁ x = f x → ContMDiffWithinAt I I' n f₁ s x
-- Mathlib.Analysis.BoxIntegral.Basic
_private.Mathlib.Analysis.BoxIntegral.Basic.0.BoxIntegral.«termℝⁿ» : Lean.ParserDescr
-- Mathlib.Topology.Connected.LocallyPathConnected
/-- **Alias** of `LocallyPathConnectedSpace.coinduced`.

---

Any topology coinduced by a locally path-connected topology is locally path-connected.  -/
LocPathConnectedSpace.coinduced : ∀ {X : Type u_1} [inst : TopologicalSpace X] [LocallyPathConnectedSpace X] {Y : Type u_4} (f : X → Y),
  LocallyPathConnectedSpace Y
-- Mathlib.LinearAlgebra.Pi
LinearEquiv.piCurry_symm_apply : ∀ (R : Type u) [inst : Semiring R] {ι : Type u_4} {κ : ι → Type u_5} (α : (i : ι) → κ i → Type u_6)
  [inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (α i k)] [inst_2 : (i : ι) → (k : κ i) → Module R (α i k)]
  (f : (a : ι) → (b : κ a) → α a b), (LinearEquiv.piCurry R α).symm f = Sigma.uncurry f
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.instInhabitedResultOfSigmaQuoted : {u : Lean.Level} →
  {α : Q(Type u)} →
    {E : Q(«$α») → Type} →
      {e : Q(«$α»)} → [Inhabited ((e : Q(«$α»)) × E e)] → Inhabited (Mathlib.Tactic.Ring.Common.Result E e)
-- Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf
/-- The presheaf of relative differentials of a morphism of presheaves of
commutative rings.  -/
PresheafOfModules.DifferentialsConstruction.relativeDifferentials' : {D : Type u₂} →
  [inst : CategoryTheory.Category.{v₂, u₂} D] →
    {S' R : CategoryTheory.Functor Dᵒᵖ CommRingCat} →
      (S' ⟶ R) → PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))
-- Init.Data.Vector.MapIdx
Vector.getElem_zipIdx : ∀ {α : Type u_1} {n k : ℕ} {xs : Vector α n} {i : ℕ} {h : i < n}, (xs.zipIdx k)[i] = (xs[i], k + i)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.toList_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {f : α → β → γ}, (Std.ExtTreeMap.map f t).toList = List.map (fun p => (p.1, f p.1 p.2)) t.toList
-- Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
CategoryTheory.ObjectProperty.instIsClosedUnderLimitsOfShapeDiscreteOfIsClosedUnderFiniteProductsOfFinite : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C)
  [P.IsClosedUnderFiniteProducts] (J : Type u_2) [Finite J], P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete J)
-- Init.Data.Int.DivMod.Lemmas
Int.emod_one : ∀ (a : ℤ), a % 1 = 0
-- Lean.Environment
Lean.EnvExtension.AsyncMode.async.inj : ∀ {branch branch_1 : Lean.AsyncBranch},
  Lean.EnvExtension.AsyncMode.async branch = Lean.EnvExtension.AsyncMode.async branch_1 → branch = branch_1
-- Batteries.Data.Fin.Coding
/-- Encode `(i : Fin n) × Fin (f i)` into `Fin (Fin.sum f)`.  -/
Fin.encodeSigma : {n : ℕ} → (f : Fin n → ℕ) → (i : Fin n) × Fin (f i) → Fin (Fin.sum f)
-- Lean.LocalContext
/-- Low-level function for updating the local context.
Assumptions about `f`, the resulting nested expressions must be definitionally equal to their original values,
and neither the `index` nor `fvarId` are modified.
 -/
Lean.LocalContext.modifyLocalDecl : Lean.LocalContext → Lean.FVarId → (Lean.LocalDecl → Lean.LocalDecl) → Lean.LocalContext
-- ProofWidgets.Component.Basic
/-- Which export of the module to use as the component function.  -/
ProofWidgets.Component.export : {Props : Type} → ProofWidgets.Component Props → String
-- Mathlib.Logic.Pairwise
/-- The relation `r` holds pairwise on the set `s` if `r x y` for all *distinct* `x y ∈ s`.  -/
Set.Pairwise : {α : Type u_1} → Set α → (α → α → Prop) → Prop
-- Mathlib.Topology.UniformSpace.HeineCantor
Continuous.uniformContinuous_of_tendsto_cocompact : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : UniformSpace β] {f : α → β} {x : β},
  Continuous f → Filter.Tendsto f (Filter.cocompact α) (nhds x) → UniformContinuous f
-- Mathlib.Topology.UnitInterval
unitInterval.symm_le_comm : ∀ {i j : ↑unitInterval}, unitInterval.symm i ≤ j ↔ unitInterval.symm j ≤ i
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
CategoryTheory.Bicategory.conjugateIsoEquiv_symm_apply_hom : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {c d : B} {l₁ l₂ : c ⟶ d} {r₁ r₂ : d ⟶ c}
  (adj₁ : CategoryTheory.Bicategory.Adjunction l₁ r₁) (adj₂ : CategoryTheory.Bicategory.Adjunction l₂ r₂) (β : r₁ ≅ r₂),
  ((CategoryTheory.Bicategory.conjugateIsoEquiv adj₁ adj₂).symm β).hom =
    (CategoryTheory.Bicategory.conjugateEquiv adj₁ adj₂).symm β.hom