mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Finiteness.Small
Submodule.instSemilatticeSupSubtypeSmallMem : {R : Type u_1} →
  {M : Type u_2} →
    [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → SemilatticeSup { P // Small.{u, u_2} ↥P }
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.find?_toArray_eq_some_iff_get?_eq_some : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α],
  (↑m).WF → ∀ {k : α} {v : β k}, Array.find? (fun x => x.fst == k) (↑m).toArray = some ⟨k, v⟩ ↔ m.get? k = some v
-- Mathlib.Topology.Maps.Basic
Topology.IsInducing.map_nhds_eq : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace Y] [inst_1 : TopologicalSpace X],
  Topology.IsInducing f → ∀ (x : X), Filter.map f (nhds x) = nhdsWithin (f x) (Set.range f)
-- Mathlib.RingTheory.Finiteness.Nilpotent
Matrix.isNilpotent_iff_forall_col : ∀ {R : Type u_1} [inst : CommSemiring R] {ι : Type u_3} [inst_1 : DecidableEq ι] [inst_2 : Fintype ι]
  {A : Matrix ι ι R}, IsNilpotent A ↔ ∀ (i : ι), ∃ n, (A ^ n).col i = 0
-- Mathlib.RingTheory.RootsOfUnity.Complex
Complex.isPrimitiveRoot_iff : ∀ (ζ : ℂ) (n : ℕ),
  n ≠ 0 → (IsPrimitiveRoot ζ n ↔ ∃ i < n, ∃ (_ : i.Coprime n), Complex.exp (2 * ↑Real.pi * Complex.I * (↑i / ↑n)) = ζ)
-- Mathlib.Algebra.Group.Hom.Defs
AddMonoidHom.mk'.eq_1 : ∀ {M : Type u_4} {G : Type u_7} [inst : AddGroup G] [inst_1 : AddZeroClass M] (f : M → G)
  (map_mul : ∀ (a b : M), f (a + b) = f a + f b),
  AddMonoidHom.mk' f map_mul = { toFun := f, map_zero' := ⋯, map_add' := map_mul }
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.addGroupWithOne : {d : ℤ} → AddGroupWithOne (ℤ√d)
-- Mathlib.Analysis.Convex.SimplicialComplex.Basic
Geometry.SimplicialComplex.ofErase_faces : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] (faces : Set (Finset E)) (indep : ∀ s ∈ faces, AffineIndependent 𝕜 Subtype.val)
  (down_closed : IsLowerSet faces)
  (inter_subset_convexHull :
    ∀ s ∈ faces, ∀ t ∈ faces, (convexHull 𝕜) ↑s ∩ (convexHull 𝕜) ↑t ⊆ (convexHull 𝕜) (↑s ∩ ↑t)),
  (Geometry.SimplicialComplex.ofErase faces indep down_closed inter_subset_convexHull).faces = faces \ {∅}
-- Mathlib.Topology.Order.MonotoneContinuity
OrderIso.coe_toHomeomorph_symm : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : TopologicalSpace α]
  [inst_3 : TopologicalSpace β] [inst_4 : OrderTopology α] [inst_5 : OrderTopology β] (e : α ≃o β),
  ⇑e.toHomeomorph.symm = ⇑e.symm
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.isMulCommutative_iSup : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A] {ι : Sort u_2} [Nonempty ι]
  {S : ι → NonUnitalSubalgebra R A} [hS : ∀ (i : ι), IsMulCommutative ↥(S i)],
  Directed (fun x1 x2 => x1 ≤ x2) S → IsMulCommutative ↥(⨆ i, S i)
-- Aesop.Tree.Traversal
Aesop.TreeRef.rapp.inj : ∀ {rref rref_1 : Aesop.RappRef}, Aesop.TreeRef.rapp rref = Aesop.TreeRef.rapp rref_1 → rref = rref_1
-- Init.Data.Int.Lemmas
Int.subNatNat_add_add : ∀ (m n k : ℕ), Int.subNatNat (m + k) (n + k) = Int.subNatNat m n
-- Mathlib.Data.Set.Basic
Set.union_subset_iff : ∀ {α : Type u} {s t u : Set α}, s ∪ t ⊆ u ↔ s ⊆ u ∧ t ⊆ u
-- Mathlib.Algebra.Group.Subsemigroup.Defs
/-- The actual `Subsemigroup` obtained from an element of a `MulMemClass`.  -/
Subsemigroup.ofClass : {S : Type u_3} → {M : Type u_4} → [inst : Mul M] → [inst_1 : SetLike S M] → [MulMemClass S M] → S → Subsemigroup M
-- Mathlib.Tactic.CrossRefAttribute
/-- A cross-reference from a Mathlib declaration to an entry in an external database.  -/
Mathlib.CrossRef.Tag : Type
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.imJ_sub : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} [inst : AddGroup R] (a b : QuaternionAlgebra R c₁ c₂ c₃), (a - b).imJ = a.imJ - b.imJ
-- Lean.Data.Lsp.Extra
Lean.Lsp.instToJsonLineRange.toJson : Lean.Lsp.LineRange → Lean.Json
-- Mathlib.RingTheory.OrderOfVanishing.Noetherian
Ring.ordFrac_of_isUnit : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsNoetherianRing R] [inst_3 : Ring.KrullDimLE 1 R]
  {K : Type u_2} [inst_4 : Field K] [inst_5 : Algebra R K] [inst_6 : IsFractionRing R K] {x : R},
  IsUnit x → (Ring.ordFrac R) ((algebraMap R K) x) = 1
-- Mathlib.Data.Complex.Basic
Complex.neg_im : ∀ (z : ℂ), (-z).im = -z.im
-- Init.Data.Vector.Lemmas
/-- Variant of `any_beq` with `==` reversed.  -/
Vector.any_beq' : ∀ {α : Type u_1} {n : ℕ} {a : α} [inst : BEq α] [PartialEquivBEq α] {xs : Vector α n},
  (xs.any fun x => x == a) = xs.contains a
-- Mathlib.Analysis.InnerProductSpace.Defs
/-- The inner product is positive definite.  -/
InnerProductSpace.Core.definite : ∀ {𝕜 : Type u_4} {F : Type u_5} [inst : RCLike 𝕜] [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F]
  (self : InnerProductSpace.Core 𝕜 F) (x : F), inner 𝕜 x x = 0 → x = 0
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.singleton_eq_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {p : α × β}, {p} = ∅.insert p.1 p.2
-- Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Set.powersetCard.isPretransitive : ∀ {α : Type u_2} {n : ℕ} [inst : DecidableEq α], MulAction.IsPretransitive (Equiv.Perm α) ↑(Set.powersetCard α n)
-- Mathlib.Algebra.Pointwise.Stabilizer
AddAction.mem_stabilizer_finset : ∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] {a : G} [inst_2 : DecidableEq α]
  {s : Finset α}, a ∈ AddAction.stabilizer G s ↔ ∀ (b : α), a +ᵥ b ∈ s ↔ b ∈ s
-- Lean.Elab.App
/-- Returns `fType` with loose bvars instantiated.
Like `State.getFType` but caches the result.
 -/
_private.Lean.Elab.App.0.Lean.Elab.Term.ElabAppArgs.getFType : Lean.Elab.Term.ElabAppArgs.M Lean.Expr
-- Mathlib.Analysis.Calculus.Deriv.Abs
DifferentiableAt.abs : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {x : E},
  DifferentiableAt ℝ f x → f x ≠ 0 → DifferentiableAt ℝ (fun x => |f x|) x
-- Mathlib.Analysis.Normed.Lp.ProdLp
/-- The distance from one point to itself is always zero.

This holds independent of `p` and does not require `[Fact (1 ≤ p)]`. We keep it separate
from `WithLp.instProdPseudoEMetricSpace` so it can be used also for `p < 1`.  -/
WithLp.prod_edist_self : ∀ (p : ENNReal) {α : Type u_2} {β : Type u_3} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β]
  (f : WithLp p (α × β)), edist f f = 0
-- Mathlib.Algebra.EuclideanDomain.Field
Field.gcd_eq_of_ne : ∀ {K : Type u_1} [inst : Field K] [inst_1 : DecidableEq K] {a : K}, a ≠ 0 → ∀ (b : K), EuclideanDomain.gcd a b = a
-- Mathlib.Lean.Expr.Basic
/-- `isPrefixOf? pre nm` returns `some post` if `nm = pre ++ post`.
Note that this includes the case where `nm` has multiple more namespaces.
If `pre` is not a prefix of `nm`, it returns `none`.  -/
Lean.Name.isPrefixOf? : Lean.Name → Lean.Name → Option Lean.Name
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue!_insertEntryIfNew : ∀ {α : Type u} {β : Type v} [inst : BEq α] [PartialEquivBEq α] [inst_2 : Inhabited β] {l : List ((_ : α) × β)} {k a : α}
  {v : β},
  Std.Internal.List.getValue! a (Std.Internal.List.insertEntryIfNew k v l) =
    if (k == a) = true ∧ Std.Internal.List.containsKey k l = false then v else Std.Internal.List.getValue! a l
-- Lean.Meta.Tactic.Grind.Types
/-- Returns the root element in the equivalence class of `e` IF `e` has been internalized.  -/
Lean.Meta.Grind.Goal.getRoot? : Lean.Meta.Grind.Goal → Lean.Expr → Option Lean.Expr
-- Std.Sat.AIG.If
Std.Sat.AIG.RefVec.IfInput.lhs : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] → {aig : Std.Sat.AIG α} → {w : ℕ} → Std.Sat.AIG.RefVec.IfInput aig w → aig.RefVec w
-- Mathlib.Data.Rel
SetRel.comp_univ : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (R : SetRel α β), R.comp Set.univ = {(a, _c) | a ∈ R.dom}
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.ConsumerNode : Type
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.HasModel.instHasSizeInt8 : Std.Rxc.HasSize Int8
-- Mathlib.Analysis.Calculus.ContDiff.Defs
contDiff_infty_iff_fderiv : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F},
  ContDiff 𝕜 (↑⊤) f ↔ Differentiable 𝕜 f ∧ ContDiff 𝕜 (↑⊤) (fderiv 𝕜 f)
-- Lean.Data.Lsp.Internal
/-- Query in the `$/lean/queryModule` watchdog <- worker request.  -/
Lean.Lsp.LeanModuleQuery : Type
-- Mathlib.Algebra.Homology.ImageToKernel
CategoryTheory.Subobject.isoOfEq.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {B : C} (X Y : CategoryTheory.Subobject B) (h : X = Y),
  X.isoOfEq Y h = X.isoOfEq Y h
-- Mathlib.Order.ConditionallyCompleteLattice.Finset
Set.Finite.map_sSup_of_monotone : ∀ {α : Type u_2} {β : Type u_3} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : ConditionallyCompleteLattice β]
  {f : α → β}, Monotone f → ∀ {s : Set α}, s.Nonempty → s.Finite → f (sSup s) = sSup (f '' s)
-- Mathlib.Algebra.Homology.ShortComplex.Exact
/-- A splitting for a short complex `S` consists of the data of a retraction `r : X₂ ⟶ X₁`
of `S.f` and section `s : X₃ ⟶ X₂` of `S.g` which satisfy `r ≫ S.f + S.g ≫ s = 𝟙 _`  -/
CategoryTheory.ShortComplex.Splitting : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] → CategoryTheory.ShortComplex C → Type v_1
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.Measure.set_prod_ae_eq : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} {s s' : Set α} {t t' : Set β}, s =ᵐ[μ] s' → t =ᵐ[ν] t' → s ×ˢ t =ᵐ[μ.prod ν] s' ×ˢ t'
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Functor.opInv_map : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {X Y : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ} (α : X ⟶ Y),
  (CategoryTheory.Functor.opInv C D).map α =
    Quiver.Hom.op { app := fun X_1 => (α.app (Opposite.op X_1)).unop, naturality := ⋯ }
-- Mathlib.Topology.Algebra.Order.Field
comap_mulLeft_nhdsGT_zero : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [inst_3 : TopologicalSpace 𝕜]
  [OrderTopology 𝕜] {x : 𝕜},
  0 < x → Filter.comap (fun x_1 => x * x_1) (nhdsWithin 0 (Set.Ioi 0)) = nhdsWithin 0 (Set.Ioi 0)
-- Mathlib.Analysis.Normed.Module.Bases
SchauderBasis.RankOneDecomposition.mk.inj : ∀ {𝕜 : Type u_1} {inst : NontriviallyNormedField 𝕜} {X : Type u_2} {inst_1 : NormedAddCommGroup X}
  {inst_2 : NormedSpace 𝕜 X} {P : ℕ → X →L[𝕜] X} {e : ℕ → X} {proj_zero : P 0 = 0}
  {finrank_range : ∀ (n : ℕ), Module.finrank 𝕜 ↥(↑(P n)).range = n}
  {proj_comp : ∀ (n m : ℕ) (x : X), (P n) ((P m) x) = (P (min n m)) x}
  {proj_tendsto : ∀ (x : X), Filter.Tendsto (fun n => (P n) x) Filter.atTop (nhds x)}
  {e_mem_range : ∀ (n : ℕ), e n ∈ (↑(SchauderBasis.succSub P n)).range} {e_ne_zero : ∀ (n : ℕ), e n ≠ 0}
  {P_1 : ℕ → X →L[𝕜] X} {e_1 : ℕ → X} {proj_zero_1 : P_1 0 = 0}
  {finrank_range_1 : ∀ (n : ℕ), Module.finrank 𝕜 ↥(↑(P_1 n)).range = n}
  {proj_comp_1 : ∀ (n m : ℕ) (x : X), (P_1 n) ((P_1 m) x) = (P_1 (min n m)) x}
  {proj_tendsto_1 : ∀ (x : X), Filter.Tendsto (fun n => (P_1 n) x) Filter.atTop (nhds x)}
  {e_mem_range_1 : ∀ (n : ℕ), e_1 n ∈ (↑(SchauderBasis.succSub P_1 n)).range} {e_ne_zero_1 : ∀ (n : ℕ), e_1 n ≠ 0},
  { P := P, e := e, proj_zero := proj_zero, finrank_range := finrank_range, proj_comp := proj_comp,
        proj_tendsto := proj_tendsto, e_mem_range := e_mem_range, e_ne_zero := e_ne_zero } =
      { P := P_1, e := e_1, proj_zero := proj_zero_1, finrank_range := finrank_range_1, proj_comp := proj_comp_1,
        proj_tendsto := proj_tendsto_1, e_mem_range := e_mem_range_1, e_ne_zero := e_ne_zero_1 } →
    P = P_1 ∧ e = e_1
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Zipper.toList_iterOfTree : ∀ {α : Type u} {β : α → Type v} (t : Std.DTreeMap.Internal.Impl α β),
  (Std.DTreeMap.Internal.Zipper.iterOfTree t).toList = t.toList
-- Mathlib.Algebra.Ring.Subsemiring.Defs
/-- Reinterpret a `Subsemiring` as an `AddSubmonoid`.  -/
Subsemiring.toAddSubmonoid : {R : Type u} → [inst : NonAssocSemiring R] → Subsemiring R → AddSubmonoid R
-- Mathlib.AlgebraicTopology.DoldKan.GammaCompN
AlgebraicTopology.DoldKan.N₁Γ₀.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasFiniteCoproducts C],
  AlgebraicTopology.DoldKan.N₁Γ₀ =
    Trans.trans
      (Trans.trans
        (Trans.trans
          (Trans.trans
            (AlgebraicTopology.DoldKan.Γ₀'.associator (CategoryTheory.SimplicialObject.Split.forget C)
              AlgebraicTopology.DoldKan.N₁)
            (AlgebraicTopology.DoldKan.Γ₀'.isoWhiskerLeft
              CategoryTheory.SimplicialObject.Split.toKaroubiNondegComplexFunctorIsoN₁.symm))
          (AlgebraicTopology.DoldKan.Γ₀'.associator CategoryTheory.SimplicialObject.Split.nondegComplexFunctor
              (CategoryTheory.Idempotents.toKaroubi (ChainComplex C ℕ))).symm)
        (CategoryTheory.Functor.isoWhiskerRight AlgebraicTopology.DoldKan.Γ₀'CompNondegComplexFunctor
          (CategoryTheory.Idempotents.toKaroubi (ChainComplex C ℕ))))
      (CategoryTheory.Idempotents.toKaroubi (ChainComplex C ℕ)).leftUnitor
-- Mathlib.Data.Multiset.FinsetOps
Multiset.Nodup.inter : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Multiset α} (t : Multiset α), s.Nodup → (s ∩ t).Nodup
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.union_eq : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashSet α} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α], m₁.union m₂ = m₁ ∪ m₂
-- Mathlib.Order.Filter.Pointwise
Filter.bot_sub : ∀ {α : Type u_2} [inst : Sub α] {g : Filter α}, ⊥ - g = ⊥
-- Mathlib.Analysis.Calculus.ContDiff.Defs
ContDiffOn.differentiableOn_iteratedFDerivWithin : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {n : WithTop ℕ∞} {m : ℕ},
  ContDiffOn 𝕜 n f s → ↑m < n → UniqueDiffOn 𝕜 s → DifferentiableOn 𝕜 (iteratedFDerivWithin 𝕜 m f s) s
-- Mathlib.Combinatorics.SimpleGraph.Star
SimpleGraph.isTree_starGraph : ∀ {V : Type u_1} (r : V), (SimpleGraph.starGraph r).IsTree
-- Mathlib.CategoryTheory.Sums.Products
CategoryTheory.Sum.associativityFunctorEquivNaturalityFunctorIso_hom_app_fst : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {A' : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} A'] {B : Type u} [inst_2 : CategoryTheory.Category.{v, u} B]
  (T : Type u_3) [inst_3 : CategoryTheory.Category.{v_3, u_3} T] (X : CategoryTheory.Functor ((A ⊕ A') ⊕ T) B),
  ((CategoryTheory.Sum.associativityFunctorEquivNaturalityFunctorIso T).hom.app X).1 =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Sum.inl_ A (A' ⊕ T)).associator (CategoryTheory.sum.inverseAssociator A A' T) X).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.whiskerRight (CategoryTheory.sum.inlCompInverseAssociator A A' T).hom X)
        ((CategoryTheory.Sum.inl_ A A').associator (CategoryTheory.Sum.inl_ (A ⊕ A') T) X).hom)
-- Mathlib.GroupTheory.RegularWreathProduct
RegularWreathProduct.one_left : ∀ {D : Type u_1} {Q : Type u_2} [inst : Group D] [inst_1 : Group Q], RegularWreathProduct.left 1 = 1
-- Mathlib.Algebra.Regular.SMul
IsLeftRegular.isSMulRegular : ∀ {R : Type u_1} [inst : Mul R] {c : R}, IsLeftRegular c → IsSMulRegular R c
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanClass.mk_surjective : ∀ (M : Type u_1) [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M],
  Function.Surjective MulArchimedeanClass.mk
-- Mathlib.CategoryTheory.Triangulated.Triangulated
CategoryTheory.Triangulated.Octahedron.triangleMorphism₁_hom₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃}
  {comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃} {v₁₂ : X₂ ⟶ Z₁₂}
  {w₁₂ : Z₁₂ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁}
  {h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  {v₂₃ : X₃ ⟶ Z₂₃} {w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₂}
  {h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  {v₁₃ : X₃ ⟶ Z₁₃} {w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁}
  {h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  (h : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃), h.triangleMorphism₁.hom₂ = u₂₃
-- Mathlib.Algebra.Group.Center
Set.subset_center_units : ∀ {M : Type u_1} [inst : Monoid M], Units.val ⁻¹' Set.center M ⊆ Set.center Mˣ
-- Mathlib.Topology.Semicontinuity.Hemicontinuity
/-- A net of lower hemicontinuous set-valued functions converging uniformly on `s` (along a
filter `l`) in the Hausdorff uniformity has a lower hemicontinuous limit on `s`  -/
TendstoUniformlyOn.lowerHemicontinuousOn : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {f : α → Set β} {s : Set α} {ι : Type u_3}
  {F : ι → α → Set β} {l : Filter ι} [l.NeBot] [inst_2 : UniformSpace β],
  TendstoUniformlyOn F f l s → (∀ (n : ι), LowerHemicontinuousOn (F n) s) → LowerHemicontinuousOn f s
-- Std.Http.Data.Request
/-- Creates a new HTTP POST Request builder with the specified URI.
 -/
Std.Http.Request.post : Std.Http.RequestTarget → Std.Http.Request.Builder
-- Mathlib.Analysis.SpecialFunctions.Complex.Analytic
AnalyticOnNhd.im_ofReal : ∀ {f : ℂ → ℂ} {s : Set ℝ}, AnalyticOnNhd ℂ f (Complex.ofReal '' s) → AnalyticOnNhd ℝ (fun x => (f ↑x).im) s
-- Mathlib.CategoryTheory.Monoidal.Limits.Colimits
/-- The tensor product of colimit cocones for functors `F₁ : J ⥤ C`
and `F₂ : J ⥤ C` is a colimit cocone when `PreservesColimit₂ F₁ F₂ (curriedTensor C)`
holds and `J` is sifted.  -/
CategoryTheory.Limits.IsColimit.tensor : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {J : Type u_2} →
        [inst_2 : CategoryTheory.Category.{v_2, u_2} J] →
          {F₁ F₂ : CategoryTheory.Functor J C} →
            {c₁ : CategoryTheory.Limits.Cocone F₁} →
              {c₂ : CategoryTheory.Limits.Cocone F₂} →
                [CategoryTheory.Limits.PreservesColimit₂ F₁ F₂ (CategoryTheory.MonoidalCategory.curriedTensor C)] →
                  [CategoryTheory.IsSifted J] →
                    CategoryTheory.Limits.IsColimit c₁ →
                      CategoryTheory.Limits.IsColimit c₂ → CategoryTheory.Limits.IsColimit (c₁.tensor c₂)
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.Red.Step.cons_cons_iff : ∀ {α : Type u} {L₁ L₂ : List (α × Bool)} {p : α × Bool},
  FreeGroup.Red.Step (p :: L₁) (p :: L₂) ↔ FreeGroup.Red.Step L₁ L₂
-- Lean.Elab.ConfigEval.Instances
Lean.Elab.ConfigEval.EvalTerm.evalOptionStx : {α : Type} →
  Lean.Expr → (Lean.Term → Lean.Elab.TermElabM (α × Lean.Expr)) → Lean.Term → Lean.Elab.TermElabM (Option α × Lean.Expr)
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.SignedMeasure.toMeasureOfLEZero_apply : ∀ {α : Type u_1} {m : MeasurableSpace α} (s : MeasureTheory.SignedMeasure α) {i j : Set α}
  (hi : MeasureTheory.VectorMeasure.restrict s i ≤ MeasureTheory.VectorMeasure.restrict 0 i) (hi₁ : MeasurableSet i),
  MeasurableSet j → (s.toMeasureOfLEZero i hi₁ hi) j = ↑(NNReal.mk (-s (i ∩ j)) ⋯)
-- Mathlib.Topology.FiberBundle.Basic
/-- Topological structure on the total space of a fiber bundle created from core, designed so
that all the local trivialization are continuous.  -/
FiberBundleCore.toTopologicalSpace : {ι : Type u_1} →
  {B : Type u_2} →
    {F : Type u_3} →
      [inst : TopologicalSpace B] →
        [inst_1 : TopologicalSpace F] → (Z : FiberBundleCore ι B F) → TopologicalSpace (Bundle.TotalSpace F Z.Fiber)
-- Mathlib.Algebra.MvPolynomial.Counit
/-- `MvPolynomial.ACounit A B` is the natural surjective algebra homomorphism
`MvPolynomial B A →ₐ[A] B` obtained by `X a ↦ a`.

See `MvPolynomial.counit` for the “absolute” variant with `A = ℤ`,
and `MvPolynomial.counitNat` for the “absolute” variant with `A = ℕ`.  -/
MvPolynomial.ACounit : (A : Type u_1) →
  (B : Type u_2) →
    [inst : CommSemiring A] → [inst_1 : CommSemiring B] → [inst_2 : Algebra A B] → MvPolynomial B A →ₐ[A] B
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.isNormal_map : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] (S : CategoryTheory.Subgroupoid C) {D : Type u_1}
  [inst_1 : CategoryTheory.Groupoid D] (φ : CategoryTheory.Functor C D) (hφ : Function.Injective φ.obj),
  CategoryTheory.Subgroupoid.im φ hφ = ⊤ → S.IsNormal → (CategoryTheory.Subgroupoid.map φ hφ S).IsNormal
-- Mathlib.CategoryTheory.FiberedCategory.Grothendieck
CategoryTheory.Pseudofunctor.CoGrothendieck.instIsEquivalenceαCategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor : ∀ {𝒮 : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} 𝒮]
  (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat) (S : 𝒮),
  (CategoryTheory.Functor.Fiber.inducedFunctor ⋯).IsEquivalence
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.η_def : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C],
  CategoryTheory.Functor.OplaxMonoidal.η (CategoryTheory.AddGrp.forget₂Mon C) =
    CategoryTheory.CategoryStruct.id
      ((CategoryTheory.AddGrp.forget₂Mon C).obj
        (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.AddGrp C)))
-- Mathlib.Computability.Partrec
Computable.list_reverse : ∀ {α : Type u_1} [inst : Primcodable α], Computable List.reverse
-- Mathlib.Algebra.GroupWithZero.Units.Lemmas
/-- We define the inverse as a `MonoidWithZeroHom` by extending the inverse map by zero
on non-units.  -/
MonoidWithZero.inverse : {M : Type u_8} → [inst : CommMonoidWithZero M] → M →*₀ M
-- Mathlib.Order.Interval.Finset.Fin
Fin.finsetImage_cast_Icc : ∀ {n m : ℕ} (h : n = m) (i j : Fin n),
  Finset.image (Fin.cast h) (Finset.Icc i j) = Finset.Icc (Fin.cast h i) (Fin.cast h j)
-- Mathlib.Analysis.Calculus.FDeriv.CompCLM
/-- Application of a `ContinuousMultilinearMap` to a constant commutes with `fderiv`.  -/
fderiv_continuousMultilinear_apply_const_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {ι : Type u_5} {M : ι → Type u_6} [inst_3 : (i : ι) → NormedAddCommGroup (M i)]
  [inst_4 : (i : ι) → NormedSpace 𝕜 (M i)] {H : Type u_7} [inst_5 : NormedAddCommGroup H] [inst_6 : NormedSpace 𝕜 H]
  {c : E → ContinuousMultilinearMap 𝕜 M H} [Finite ι],
  DifferentiableAt 𝕜 c x → ∀ (u : (i : ι) → M i) (m : E), (fderiv 𝕜 (fun y => (c y) u) x) m = ((fderiv 𝕜 c x) m) u
-- Mathlib.Order.BoundedOrder.Basic
not_isMax_iff_ne_top : ∀ {α : Type u} [inst : PartialOrder α] [inst_1 : OrderTop α] {a : α}, ¬IsMax a ↔ a ≠ ⊤
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toList_roo_eq_if : ∀ {m n : ℤ}, (m<...n).toList = if m + 1 < n then (m + 1) :: ((m + 1)<...n).toList else []
-- Mathlib.RingTheory.FilteredAlgebra.Basic
IsModuleFiltration.toIsFiltration : ∀ {ι : Type u_1} {ιM : Type u_2} (R : Type u_3) (M : Type u_4) {σ : Type u_5} {σM : Type u_6} {inst : AddMonoid ι}
  {inst_1 : PartialOrder ι} {inst_2 : PartialOrder ιM} {inst_3 : VAdd ι ιM} {inst_4 : Preorder σ} {inst_5 : Semiring R}
  {inst_6 : SetLike σ R} {inst_7 : Preorder σM} {inst_8 : AddCommMonoid M} {inst_9 : Module R M}
  {inst_10 : SetLike σM M} (F : ι → σ) {F_lt : outParam (ι → σ)} {inst_11 : IsRingFiltration F F_lt} {F' : ιM → σM}
  {F'_lt : outParam (ιM → σM)} [self : IsModuleFiltration F F_lt F' F'_lt], IsFiltration F' F'_lt