mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Types.Yoneda
CategoryTheory.Limits.compCoyonedaSectionsEquiv_apply_app : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] (F : CategoryTheory.Functor J C) (X : C)
  (s : ↑(F.comp (CategoryTheory.coyoneda.obj (Opposite.op X))).sections) (j : J),
  ((CategoryTheory.Limits.compCoyonedaSectionsEquiv F X) s).app j = ↑s j
-- Mathlib.SetTheory.Ordinal.Notation
ONote.repr_sub : ∀ (o₁ o₂ : ONote) [o₁.NF] [o₂.NF], (o₁ - o₂).repr = o₁.repr - o₂.repr
-- Std.Time.Format.Basic
Std.Time.FormatType.eq_3 : ∀ (result : Type), Std.Time.FormatType result [] = result
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.Equiv.getLT?_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp] {k : α},
  t₁.Equiv t₂ → t₁.getLT? k = t₂.getLT? k
-- Mathlib.LinearAlgebra.Basis.MulOpposite
Module.Basis.repr_unop_eq_mulOpposite_repr : ∀ {R : Type u_1} {H : Type u_2} {ι : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid H] [inst_2 : Module R H]
  (b : Module.Basis ι R H) (x : Hᵐᵒᵖ), b.repr (MulOpposite.unop x) = b.mulOpposite.repr x
-- Mathlib.Analysis.Convex.Cone.Basic
_private.Mathlib.Analysis.Convex.Cone.Basic.0.«termR≥0» : Lean.ParserDescr
-- Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
/-- The underlying function of the cyclotomic character. See `cyclotomicCharacter`.  -/
cyclotomicCharacter.toFun : {L : Type u} → [inst : CommRing L] → [IsDomain L] → (p : ℕ) → [inst_2 : Fact (Nat.Prime p)] → L ≃+* L → ℤ_[p]
-- Init.Data.List.Lemmas
List.length_eq_one_iff : ∀ {α : Type u_1} {l : List α}, l.length = 1 ↔ ∃ a, l = [a]
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.splitAtPred.eq_2 : ∀ {α : Type u_1} (p : α → Bool) (a : α) (as : List α),
  Turing.PartrecToTM2.splitAtPred p (a :: as) =
    bif p a then ([], some a, as)
    else
      match Turing.PartrecToTM2.splitAtPred p as with
      | (l₁, o, l₂) => (a :: l₁, o, l₂)
-- Mathlib.Algebra.Group.ModEq
/-- **Alias** of the forward direction of `AddCommGroup.ModEq.sub_iff_right`. -/
AddCommGroup.ModEq.sub_right_cancel : ∀ {G : Type u_1} [inst : AddCommGroup G] {p a₁ a₂ b₁ b₂ : G},
  a₂ ≡ b₂ [PMOD p] → a₁ - a₂ ≡ b₁ - b₂ [PMOD p] → a₁ ≡ b₁ [PMOD p]
-- Mathlib.Topology.Algebra.Constructions.DomMulAct
DomMulAct.isEmbedding_mk_symm : ∀ {M : Type u_1} [inst : TopologicalSpace M], Topology.IsEmbedding ⇑DomMulAct.mk.symm
-- Mathlib.Geometry.Manifold.VectorBundle.Hom
/-- Consider a `C^n` map `v : M → E₁` to a vector bundle, over a base map `b : M → B`, and
linear maps `ϕ m : E₁ (b m) → E₂ (b m)` depending smoothly on `m`.
One can apply `ϕ m` to `v m`, and the resulting map is `C^n`.

We give here a version of this statement on a set.  -/
ContMDiffOn.clm_bundle_apply : ∀ {𝕜 : Type u_1} {B : Type u_2} {F₁ : Type u_3} {F₂ : Type u_4} {M : Type u_6} [inst : NontriviallyNormedField 𝕜]
  {n : WithTop ℕ∞} {E₁ : B → Type u_7} [inst_1 : (x : B) → AddCommGroup (E₁ x)] [inst_2 : (x : B) → Module 𝕜 (E₁ x)]
  [inst_3 : NormedAddCommGroup F₁] [inst_4 : NormedSpace 𝕜 F₁] [inst_5 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)]
  [inst_6 : (x : B) → TopologicalSpace (E₁ x)] {E₂ : B → Type u_8} [inst_7 : (x : B) → AddCommGroup (E₂ x)]
  [inst_8 : (x : B) → Module 𝕜 (E₂ x)] [inst_9 : NormedAddCommGroup F₂] [inst_10 : NormedSpace 𝕜 F₂]
  [inst_11 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [inst_12 : (x : B) → TopologicalSpace (E₂ x)] {EB : Type u_10}
  [inst_13 : NormedAddCommGroup EB] [inst_14 : NormedSpace 𝕜 EB] {HB : Type u_11} [inst_15 : TopologicalSpace HB]
  {IB : ModelWithCorners 𝕜 EB HB} [inst_16 : TopologicalSpace B] [inst_17 : ChartedSpace HB B] {EM : Type u_12}
  [inst_18 : NormedAddCommGroup EM] [inst_19 : NormedSpace 𝕜 EM] {HM : Type u_13} [inst_20 : TopologicalSpace HM]
  {IM : ModelWithCorners 𝕜 EM HM} [inst_21 : TopologicalSpace M] [inst_22 : ChartedSpace HM M]
  [inst_23 : FiberBundle F₁ E₁] [inst_24 : VectorBundle 𝕜 F₁ E₁] [inst_25 : FiberBundle F₂ E₂]
  [inst_26 : VectorBundle 𝕜 F₂ E₂] {b : M → B} {v : (x : M) → E₁ (b x)} {s : Set M}
  [inst_27 : ∀ (x : B), IsTopologicalAddGroup (E₂ x)] [inst_28 : ∀ (x : B), ContinuousSMul 𝕜 (E₂ x)]
  {ϕ : (x : M) → E₁ (b x) →L[𝕜] E₂ (b x)},
  ContMDiffOn IM (IB.prod (modelWithCornersSelf 𝕜 ⋯)) n (fun m => ⟨b m, ϕ m⟩) s →
    ContMDiffOn IM (IB.prod (modelWithCornersSelf 𝕜 F₁)) n (fun m => ⟨b m, v m⟩) s →
      ContMDiffOn IM (IB.prod (modelWithCornersSelf 𝕜 F₂)) n (fun m => ⋯) s
-- Init.Meta.Defs
_private.Init.Meta.Defs.0.Lean.Name.escape : String → String
-- Mathlib.Topology.Path
Path.inv_apply : ∀ {X : Type u_1} [inst : TopologicalSpace X] {a b : X} [inst_1 : Inv X] [inst_2 : ContinuousInv X] (γ : Path a b)
  (a_1 : ↑unitInterval), γ.inv a_1 = (γ a_1)⁻¹
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
Function.Surjective.tprod_eq_tprod_of_hasProd_iff_hasProd : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] [T2Space α]
  {α' : Type u_4} [inst_3 : CommMonoid α'] [inst_4 : TopologicalSpace α'] {e : α' → α},
  Function.Surjective e →
    e 1 = 1 →
      ∀ {f : β → α} {g : γ → α'}, (∀ {a : α'}, HasProd f (e a) ↔ HasProd g a) → ∏' (b : β), f b = e (∏' (c : γ), g c)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.powC : Lean.Grind.CommRing.Poly → ℕ → ℕ → Lean.Grind.CommRing.Poly
-- Mathlib.Algebra.Order.Interval.Set.Monoid
Set.Ioo_add_bij : ∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : PartialOrder M] [IsOrderedCancelAddMonoid M] [ExistsAddOfLE M]
  (a b d : M), Set.BijOn (fun x => x + d) (Set.Ioo a b) (Set.Ioo (a + d) (b + d))
-- Mathlib.Topology.LocalAtTarget
TopologicalSpace.IsOpenCover.isClosed_iff_coe_preimage : ∀ {β : Type u_2} [inst : TopologicalSpace β] {ι : Type u_3} {U : ι → TopologicalSpace.Opens β},
  TopologicalSpace.IsOpenCover U → ∀ {s : Set β}, IsClosed s ↔ ∀ (i : ι), IsClosed (Subtype.val ⁻¹' s)
-- Init.Grind.Module.Envelope
Lean.Grind.IntModule.OfNatModule.zsmul : {α : Type u} →
  [inst : Lean.Grind.NatModule α] → ℤ → Lean.Grind.IntModule.OfNatModule.Q α → Lean.Grind.IntModule.OfNatModule.Q α
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
/-- Let `x` be a nondegenerate `d`-simplex of `Δ[m + 1] ⊗ Δ[n]` which
does not belong to `Λ[m + 1, k.castSucc].unionProd ∂Δ[n]`. In particular,
`x` induces a strictly monotone map from `Fin (d + 1)` to
`{0, ..., m + 1} × {0, ..., n}`. We introduce a predicate on elements in
`Fin (d + 1)` which shall be satisfied for `l.succ` (`l : Fin d`)
if `x l.castSucc = (k.castSucc, t)` and `x l.succ = (k.succ, t)`
for some `t`. The nondegenerate simplices `x` such that there exists
such a `l` shall be the type (I) simplices of a pairing, and the
corresponding type (II) simplex shall be obtained by deleting `x l.castSucc`.  -/
SSet.prodStdSimplex.pairingCore.IsIndex : {m : ℕ} →
  {k : Fin (m + 1)} →
    {n : ℕ} →
      (x : ((SSet.horn (m + 1) k.castSucc).unionProd (SSet.boundary n)).N) → {d : ℕ} → x.dim = d → Fin (d + 1) → Prop
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
CategoryTheory.CostructuredArrow.toOverCompYoneda.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (A : CategoryTheory.Functor Cᵒᵖ (Type v))
  (T : CategoryTheory.Over A),
  CategoryTheory.CostructuredArrow.toOverCompYoneda A T =
    CategoryTheory.NatIso.ofComponents
      (fun X =>
        (CategoryTheory.overEquivPresheafCostructuredArrow A).fullyFaithfulFunctor.homEquiv.toIso ≪≫
          (((CategoryTheory.CostructuredArrow.toOverCompOverEquivPresheafCostructuredArrow A).app
                  (Opposite.unop X)).homCongr
              (CategoryTheory.Iso.refl ((CategoryTheory.overEquivPresheafCostructuredArrow A).functor.obj T))).toIso)
      ⋯
-- Mathlib.Algebra.Group.Units.Basic
/-- A subsingleton `AddMonoid` has a unique additive unit.  -/
instUniqueAddUnitsOfSubsingleton : {M : Type u_1} → [inst : AddMonoid M] → [Subsingleton M] → Unique (AddUnits M)
-- Mathlib.CategoryTheory.Sites.Coverage
CategoryTheory.Coverage.Saturate.transitive : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {K : CategoryTheory.Coverage C} (X : C)
  (R S : CategoryTheory.Sieve X),
  K.Saturate X R →
    (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → K.Saturate Y (CategoryTheory.Sieve.pullback f S)) → K.Saturate X S
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.ofNNReal_liminf : ∀ {ι : Type u_4} {f : Filter ι} {u : ι → NNReal},
  Filter.IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) f u → ↑(Filter.liminf u f) = Filter.liminf (fun i => ↑(u i)) f
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.volume_preserving_finTwoArrow : ∀ (α : Type u) [inst : MeasureTheory.MeasureSpace α] [MeasureTheory.SigmaFinite MeasureTheory.volume],
  MeasureTheory.MeasurePreserving (⇑MeasurableEquiv.finTwoArrow) MeasureTheory.volume MeasureTheory.volume
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_rco_eq_if : ∀ {m n : ℕ}, (m...n).toArray = if m < n then #[m] ++ ((m + 1)...n).toArray else #[]
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.Splits.degree_eq_card_roots : ∀ {R : Type u_1} [inst : CommRing R] {f : Polynomial R} [inst_1 : IsDomain R],
  f.Splits → f ≠ 0 → f.degree = ↑f.roots.card
-- Mathlib.GroupTheory.Perm.Fin
sign_finRotate : ∀ (n : ℕ), Equiv.Perm.sign (finRotate n) = (-1) ^ (n - 1)
-- Mathlib.Data.Nat.Factorization.PrimePow
Nat.exists_base_eq_prime_pow_of_prime_pow_eq_base_pow : ∀ {p a m n : ℕ}, Nat.Prime p → n ≠ 0 → p ^ m = a ^ n → ∃ k, a = p ^ k
-- Lean.Meta.Tactic.Try.Collect
Lean.Meta.Try.Collector.checkInductive : Lean.LocalDecl → Lean.Meta.Try.Collector.M Unit
-- Mathlib.Data.List.Sort
/-- **Alias** of the forward direction of `List.sortedGT_iff_isChain`. -/
List.SortedGT.isChain : ∀ {α : Type u_1} {l : List α} [inst : Preorder α], l.SortedGT → List.IsChain (fun x1 x2 => x1 > x2) l
-- Mathlib.FieldTheory.Cardinality
/-- A `Fintype` can be given a field structure iff its cardinality is a prime power.  -/
Fintype.nonempty_field_iff : ∀ {α : Type u_1} [inst : Fintype α], Nonempty (Field α) ↔ IsPrimePow (Fintype.card α)
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.isSome_min?_of_contains : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α},
  t.contains k = true → t.min?.isSome = true
-- Mathlib.Topology.MetricSpace.UniformConvergence
/-- If `f : α → γ → β` is a family of a functions, all of which are Lipschitz on `s` with the
same constant, then the family is uniformly equicontinuous on `s`.  -/
LipschitzOnWith.uniformEquicontinuousOn : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : PseudoEMetricSpace γ] [inst_1 : PseudoEMetricSpace β]
  (f : α → γ → β) (K : NNReal) {s : Set γ}, (∀ (c : α), LipschitzOnWith K (f c) s) → UniformEquicontinuousOn f s
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitDisc.instIsScalarTower_circle_circle : IsScalarTower Circle Circle Complex.UnitDisc
-- Mathlib.RingTheory.TwoSidedIdeal.BigOperators
TwoSidedIdeal.listProd_mem : ∀ {R : Type u_1} [inst : Ring R] (I : TwoSidedIdeal R) {ι : Type u_2} (l : List ι) (f : ι → R),
  (∃ x ∈ l, f x ∈ I) → (List.map f l).prod ∈ I
-- Mathlib.CategoryTheory.Sites.Point.Presheaf
/-- If `X` is an object of `C`, this is the point of the site `(C, ⊥)` (whose
sheaves are presheaves, see `sheafBotEquivalence`) corresponding to `X`.  -/
CategoryTheory.GrothendieckTopology.pointBot : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.LocallySmall.{w, v, u} C] → C → ⊥.Point
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
RootPairing.EmbeddedG2.pairingIn_shortAddLong_left : ∀ {ι : 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] (P : RootPairing ι R M N)
  [inst_5 : P.EmbeddedG2] [Finite ι] [CharZero R] [IsDomain R] (i : ι),
  P.pairingIn ℤ (RootPairing.EmbeddedG2.shortAddLong P) i =
    P.pairingIn ℤ (RootPairing.EmbeddedG2.short P) i + P.pairingIn ℤ (RootPairing.EmbeddedG2.long P) i
-- Mathlib.Geometry.Manifold.StructureGroupoid
StructureGroupoid.mk : {H : Type u_2} →
  [inst : TopologicalSpace H] →
    (members : Set (OpenPartialHomeomorph H H)) →
      (∀ (e e' : OpenPartialHomeomorph H H), e ∈ members → e' ∈ members → e.trans e' ∈ members) →
        (∀ e ∈ members, e.symm ∈ members) →
          OpenPartialHomeomorph.refl H ∈ members →
            (∀ (e : OpenPartialHomeomorph H H),
                (∀ x ∈ e.source, ∃ s, IsOpen s ∧ x ∈ s ∧ e.restr s ∈ members) → e ∈ members) →
              (∀ (e e' : OpenPartialHomeomorph H H), e ∈ members → e' ≈ e → e' ∈ members) → StructureGroupoid H
-- Mathlib.RingTheory.MvPolynomial.Basic
_private.Mathlib.RingTheory.MvPolynomial.Basic.0.MvPolynomial.finite_setOfPred_bounded : ∀ (α : Type u_1) [Finite α] (n : ℕ), Finite ↑{f | ∀ (a : α), f a ≤ n}
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.toFinsuppIsoLinear_symm_apply_toFinsupp : ∀ (R : Type u) [inst : Semiring R] (a : AddMonoidAlgebra R ℕ), ((Polynomial.toFinsuppIsoLinear R).symm a).toFinsupp = a
-- Mathlib.Tactic.NormNum.Result
/-- Convert a `Result` to a `Simp.Result`.  -/
Mathlib.Meta.NormNum.Result.toSimpResult : {u : Lean.Level} → {α : Q(Type u)} → {e : Q(«$α»)} → Mathlib.Meta.NormNum.Result e → Lean.MetaM Lean.Meta.Simp.Result
-- Mathlib.Data.Nat.Choose.Lucas
/-- For primes `p`, `choose (p * a) (p * b)` is congruent to `choose a b` modulo `p`.
Also see `choose_mul_mul_modEq_choose_nat` for the version with `MOD`.  -/
Choose.choose_mul_mul_modEq_choose : ∀ {a b p : ℕ} [Fact (Nat.Prime p)], ↑((p * a).choose (p * b)) ≡ ↑(a.choose b) [ZMOD ↑p]
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey!_ofList_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : BEq α] [Std.LawfulBEqCmp cmp]
  [inst_2 : Inhabited α] {l : List (α × β)} {k : α},
  (List.map Prod.fst l).contains k = false → (Std.TreeMap.ofList l cmp).getKey! k = default
-- Mathlib.MeasureTheory.Order.Lattice
MeasurableSup.mk : ∀ {M : Type u_1} [inst : MeasurableSpace M] [inst_1 : Max M],
  autoParam (∀ (c : M), Measurable fun x => c ⊔ x) MeasurableSup.measurable_const_sup._autoParam →
    autoParam (∀ (c : M), Measurable fun x => x ⊔ c) MeasurableSup.measurable_sup_const._autoParam → MeasurableSup M
-- Mathlib.Order.Bounds.Basic
DirectedOn.maximal_iff_isGreatest : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α} {a : α},
  DirectedOn (fun x y => x ≤ y) s → (Maximal (fun x => x ∈ s) a ↔ IsGreatest s a)
-- Mathlib.Data.ENat.Basic
ENat.le_one_iff_eq_zero_or_eq_one : ∀ {n : ℕ∞}, n ≤ 1 ↔ n = 0 ∨ n = 1
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.sign_antiperiodic : Function.Antiperiodic Real.Angle.sign ↑Real.pi
-- Mathlib.ModelTheory.Equivalence
FirstOrder.Language.Formula.iff_not_not : ∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type w} (φ : L.Formula α), T.Iff φ φ.not.not
-- Mathlib.Order.Category.BoolAlg
BoolAlg.dualEquiv_functor : BoolAlg.dualEquiv.functor = BoolAlg.dual
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.Disjoint.zpow_disjoint_zpow : ∀ {α : Type u_1} {σ τ : Equiv.Perm α}, σ.Disjoint τ → ∀ (m n : ℤ), (σ ^ m).Disjoint (τ ^ n)
-- Mathlib.RingTheory.MvPowerSeries.Rename
MvPowerSeries.coeff_embDomain_rename : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [inst : CommSemiring R] (e : σ ↪ τ) (p : MvPowerSeries σ R) (x : σ →₀ ℕ),
  (MvPowerSeries.coeff (Finsupp.embDomain e x)) ((MvPowerSeries.rename ⇑e) p) = (MvPowerSeries.coeff x) p
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonInlayHintTooltip : Lean.ToJson Lean.Lsp.InlayHintTooltip
-- Mathlib.CategoryTheory.Preadditive.Mat
CategoryTheory.Mat_.embedding_obj_fintype : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C] (X : C),
  ((CategoryTheory.Mat_.embedding C).obj X).fintype = PUnit.fintype
-- Mathlib.Analysis.Normed.Ring.Lemmas
/-- Normed ring structure on the product of finitely many non-unital normed rings, using the sup
norm.  -/
Pi.nonUnitalNormedRing : {ι : Type u_3} →
  {R : ι → Type u_4} → [Fintype ι] → [(i : ι) → NonUnitalNormedRing (R i)] → NonUnitalNormedRing ((i : ι) → R i)
-- Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
SSet.horn.IsCompatible.δ_pred_comp_assoc : ∀ {n : ℕ} {X : SSet} {i : Fin (n + 3)} {f : (j : Fin (n + 3)) → j ≠ i → (SSet.stdSimplex.obj { len := n + 1 } ⟶ X)},
  SSet.horn.IsCompatible f →
    ∀ (j k : Fin (n + 3)) (hj : autoParam (j ≠ i) SSet.horn.IsCompatible.δ_pred_comp._auto_1)
      (hk : autoParam (k ≠ i) SSet.horn.IsCompatible.δ_pred_comp._auto_3)
      (hjk : autoParam (j < k) SSet.horn.IsCompatible.δ_pred_comp._auto_5) {Z : SSet} (h : X ⟶ Z),
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ (k.pred ⋯))
          (CategoryTheory.CategoryStruct.comp (f j hj) h) =
        CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ (j.castPred ⋯))
          (CategoryTheory.CategoryStruct.comp (f k hk) h)
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.disjoint_smul_set_left : ∀ {α : Type u_2} {β : Type u_3} [inst : Group α] [inst_1 : MulAction α β] {s t : Set β} {a : α},
  Disjoint (a • s) t ↔ Disjoint s (a⁻¹ • t)
-- Lean.Server.GoTo
Lean.Server.GoToKind.type.sizeOf_spec : sizeOf Lean.Server.GoToKind.type = 1
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.negAddY_eq : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} {P Q : Fin 3 → F},
  W.Equation P →
    W.Equation Q →
      P 2 ≠ 0 →
        Q 2 ≠ 0 →
          W.negAddY P Q =
            ((P 1 * Q 2 - Q 1 * P 2) *
                  ((P 1 * Q 2 - Q 1 * P 2) ^ 2 * P 2 * Q 2 +
                            W.a₁ * (P 1 * Q 2 - Q 1 * P 2) * P 2 * Q 2 * (P 0 * Q 2 - Q 0 * P 2) -
                          W.a₂ * P 2 * Q 2 * (P 0 * Q 2 - Q 0 * P 2) ^ 2 -
                        P 0 * Q 2 * (P 0 * Q 2 - Q 0 * P 2) ^ 2 -
                      Q 0 * P 2 * (P 0 * Q 2 - Q 0 * P 2) ^ 2 -
                    P 0 * Q 2 * (P 0 * Q 2 - Q 0 * P 2) ^ 2) +
                P 1 * Q 2 * (P 0 * Q 2 - Q 0 * P 2) ^ 3) /
              (P 2 * Q 2) ^ 2
-- Mathlib.Algebra.Group.Submonoid.Defs
Submonoid.toMulOneClass.eq_1 : ∀ {M : Type u_5} [inst : MulOneClass M] (S : Submonoid M), S.toMulOneClass = SubmonoidClass.toMulOneClass S
-- Init.Data.Int.Order
Int.mul_le_mul : ∀ {a b c d : ℤ}, a ≤ c → b ≤ d → 0 ≤ b → 0 ≤ c → a * b ≤ c * d
-- Mathlib.LinearAlgebra.Dual.Defs
Submodule.dualCoannihilator_sup_eq : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (U V : Submodule R (Module.Dual R M)), (U ⊔ V).dualCoannihilator = U.dualCoannihilator ⊓ V.dualCoannihilator
-- Std.Http.Data.Chunk
Std.Http.Chunk.instInhabitedExtensionName : Inhabited Std.Http.Chunk.ExtensionName
-- Mathlib.Algebra.Group.Hom.Defs
/-- Additive group homomorphisms preserve negation.  -/
map_neg : ∀ {G : Type u_7} {H : Type u_8} {F : Type u_9} [inst : FunLike F G H] [inst_1 : AddGroup G]
  [inst_2 : SubtractionMonoid H] [AddMonoidHomClass F G H] (f : F) (a : G), f (-a) = -f a
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.reachable_comm : ∀ {V : Type u} {G : SimpleGraph V} {u v : V}, G.Reachable u v ↔ G.Reachable v u
-- Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
SSet.unique_nonDegenerate_dim : ∀ (X : SSet) {n : ℕ} (x : X.obj (Opposite.op { len := n })) {m₁ m₂ : ℕ} (f₁ : { len := n } ⟶ { len := m₁ })
  [CategoryTheory.Epi f₁] (y₁ : ↑(X.nonDegenerate m₁)),
  x = (CategoryTheory.ConcreteCategory.hom (X.map f₁.op)) ↑y₁ →
    ∀ (f₂ : { len := n } ⟶ { len := m₂ }) [CategoryTheory.Epi f₂] (y₂ : ↑(X.nonDegenerate m₂)),
      x = (CategoryTheory.ConcreteCategory.hom (X.map f₂.op)) ↑y₂ → m₁ = m₂
-- Mathlib.Algebra.Module.GradedModule
DirectSum.Gmodule.toGdistribMulAction : {ιA : Type u_1} →
  {ιB : Type u_2} →
    {A : ιA → Type u_3} →
      {M : ιB → Type u_4} →
        {inst : AddMonoid ιA} →
          {inst_1 : VAdd ιA ιB} →
            {inst_2 : (i : ιA) → AddMonoid (A i)} →
              {inst_3 : (i : ιB) → AddMonoid (M i)} →
                {inst_4 : GradedMonoid.GMonoid A} → [self : DirectSum.Gmodule A M] → DirectSum.GdistribMulAction A M
-- Std.Data.HashSet.Lemmas
Std.HashSet.Equiv.get?_eq : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {k : α},
  m₁.Equiv m₂ → m₁.get? k = m₂.get? k
-- Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
/-- **Alias** of `FourierTransform.fourierCLE_apply`. -/
SchwartzMap.fourierTransformCLE_apply : ∀ {R : Type u_5} {E : Type u_6} {F : Type u_7} [inst : Semiring R] [inst_1 : AddCommMonoid E] [inst_2 : AddCommMonoid F]
  [inst_3 : Module R E] [inst_4 : Module R F] [inst_5 : FourierTransform E F] [inst_6 : FourierAdd E F]
  [inst_7 : FourierSMul R E F] [inst_8 : FourierTransformInv F E] [inst_9 : FourierPair E F]
  [inst_10 : FourierInvPair F E] [inst_11 : TopologicalSpace E] [inst_12 : TopologicalSpace F]
  [inst_13 : ContinuousFourier E F] [inst_14 : ContinuousFourierInv F E] (f : E),
  (FourierTransform.fourierCLE R E) f = FourierTransform.fourier f
-- Init.Data.String.Lemmas.TakeDrop
String.Slice.toList_copy_drop : ∀ {s : String.Slice} {n : ℕ}, (s.drop n).copy.toList = List.drop n s.copy.toList
-- Mathlib.Analysis.Normed.Group.Defs
ESeminormedAddCommMonoid.toAddCommMonoid : {E : Type u_8} → [inst : TopologicalSpace E] → [self : ESeminormedAddCommMonoid E] → AddCommMonoid E
-- Mathlib.RingTheory.MvPolynomial.Homogeneous
MvPolynomial.IsHomogeneous.C_mul : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R] {φ : MvPolynomial σ R} {m : ℕ},
  φ.IsHomogeneous m → ∀ (r : R), (MvPolynomial.C r * φ).IsHomogeneous m
-- Mathlib.RingTheory.Localization.Finiteness
/-- To check that the kernel of a ring homomorphism is finitely generated,
it suffices to check this after localizing at a spanning set of the source.
 -/
RingHom.ker_fg_of_localizationSpan : ∀ {R : Type u} [inst : CommSemiring R] {S : Type v} [inst_1 : CommSemiring S] {f : R →+* S} (t : Set R),
  Ideal.span t = ⊤ → (∀ (g : ↑t), (RingHom.ker (Localization.awayMap f ↑g)).FG) → (RingHom.ker f).FG
-- Mathlib.Geometry.Euclidean.Incenter
/-- The barycentric coordinates of the incenter are less than `2⁻¹` (thus, it lies closer on an
angle bisector to the opposite side than to the vertex, or equivalently the image of the incenter
under a homothety with scale factor 2 about a vertex lies outside the simplex).  -/
Affine.Simplex.excenterWeights_empty_lt_inv_two : ∀ {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 : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) [n.AtLeastTwo]
  (i : Fin (n + 1)), s.excenterWeights ∅ i < 2⁻¹
-- Lean.Elab.ConfigEval.Types
Lean.Elab.ConfigEval.ConfigItem.mk : Lean.Syntax →
  Lean.Ident →
    Lean.Syntax → Option Bool → Lean.Name → List Lean.Syntax → List Lean.Syntax → Lean.Elab.ConfigEval.ConfigItem
-- Mathlib.AlgebraicTopology.CechNerve
/-- The augmented Čech conerve construction is left adjoint to the `toArrow` functor.  -/
CategoryTheory.CosimplicialObject.cechConerveAdjunction : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 :
        ∀ (n : ℕ) (f : CategoryTheory.Arrow C),
          CategoryTheory.Limits.HasWidePushout f.left (fun x => f.right) fun x => f.hom] →
      CategoryTheory.CosimplicialObject.augmentedCechConerve ⊣ CategoryTheory.CosimplicialObject.Augmented.toArrow
-- Mathlib.Algebra.Homology.DerivedCategory.HomologySequence
DerivedCategory.HomologySequence.mono_homologyMap_mor₂_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C],
  ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles,
    ∀ (n₀ : ℤ),
      CategoryTheory.Mono ((DerivedCategory.homologyFunctor C n₀).map T.mor₂) ↔
        (DerivedCategory.homologyFunctor C n₀).map T.mor₁ = 0
-- Mathlib.GroupTheory.Congruence.Defs
/-- Additive congruence relations are symmetric.  -/
AddCon.symm : ∀ {M : Type u_1} [inst : Add M] (c : AddCon M) {x y : M}, c x y → c y x
-- Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
integral_gaussian : ∀ (b : ℝ), ∫ (x : ℝ), Real.exp (-b * x ^ 2) = √(Real.pi / b)
-- Mathlib.Data.Ordmap.Invariants
Ordnode.Emem.eq_1 : ∀ {α : Type u_1} (x : α), Ordnode.Emem x = Ordnode.Any (Eq x)