mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.Triangle.add_hom₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  {T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C} [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] (f g : T₁ ⟶ T₂), (f + g).hom₁ = f.hom₁ + g.hom₁
-- Mathlib.Topology.Algebra.Monoid
exists_nhds_one_split : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : MulOneClass M] [ContinuousMul M] {s : Set M},
  s ∈ nhds 1 → ∃ V ∈ nhds 1, ∀ v ∈ V, ∀ w ∈ V, v * w ∈ s
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
CategoryTheory.Limits.limitIsoSwapCompLim_inv_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} J]
  {K : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} K] [inst_3 : CategoryTheory.Limits.HasLimitsOfShape J C]
  (G : CategoryTheory.Functor J (CategoryTheory.Functor K C)) (X : K),
  (CategoryTheory.Limits.limitIsoSwapCompLim G).inv.app X =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limMap (G.flipIsoCurrySwapUncurry.inv.app X))
      (CategoryTheory.Limits.limitObjIsoLimitCompEvaluation G X).inv
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.ideal_sSup : ∀ {X : AlgebraicGeometry.Scheme} {I : Set X.IdealSheafData},
  (sSup I).ideal = sSup (AlgebraicGeometry.Scheme.IdealSheafData.ideal '' I)
-- Init.Data.List.Pairwise
List.pairwise_of_forall_sublist : ∀ {α : Type u_1} {l : List α} {R : α → α → Prop}, (∀ {a b : α}, [a, b].Sublist l → R a b) → List.Pairwise R l
-- Mathlib.Combinatorics.Enumerative.Catalan.Basic
catalan_one : catalan 1 = 1
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfc_predicate_algebraMap : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A] [inst_6 : Ring A]
  [inst_7 : StarRing A] [inst_8 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] (r : R),
  p ((algebraMap R A) r)
-- Std.Data.Internal.List.Associative
/-- Internal implementation detail of the hash map  -/
Std.Internal.List.getValueD : {α : Type u} → {β : Type v} → [BEq α] → α → List ((_ : α) × β) → β → β
-- Mathlib.Data.Finset.Lattice.Fold
Finset.toDual_sup' : ∀ {α : Type u_2} {ι : Type u_5} [inst : SemilatticeSup α] {s : Finset ι} (hs : s.Nonempty) (f : ι → α),
  OrderDual.toDual (s.sup' hs f) = s.inf' hs (⇑OrderDual.toDual ∘ f)
-- Mathlib.Tactic.Linter.Style
/-- The "show" linter emits a warning if the `show` tactic changed the goal. `show` should only be used
to indicate intermediate goal states for proof readability. When the goal is actually changed,
`change` should be preferred.
 -/
Mathlib.Linter.linter.style.show : Lean.Option Bool
-- Mathlib.Topology.NhdsWithin
eventuallyEq_nhdsWithin_of_eqOn : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {f g : α → β} {s : Set α} {a : α},
  Set.EqOn f g s → f =ᶠ[nhdsWithin a s] g
-- Mathlib.GroupTheory.Perm.Centralizer
/-- The canonical morphism from `Subgroup.centralizer {g}`
to the group of permutations of `g.cycleFactorsFinset`  -/
Equiv.Perm.OnCycleFactors.toPermHom : {α : Type u_1} →
  [inst : DecidableEq α] →
    [inst_1 : Fintype α] → (g : Equiv.Perm α) → ↥(Subgroup.centralizer {g}) →* Equiv.Perm ↥g.cycleFactorsFinset
-- Mathlib.RepresentationTheory.Rep.Res
/-- The restriction functor `Rep R G ⥤ Rep R H` for a subgroup `H` of `G`.  -/
Rep.resFunctor : {k : Type u} →
  [inst : Semiring k] →
    {G : Type v1} →
      {H : Type v2} →
        [inst_1 : Monoid G] →
          [inst_2 : Monoid H] → (H →* G) → CategoryTheory.Functor (Rep.{t, u, v1} k G) (Rep.{t, u, v2} k H)
-- Mathlib.Analysis.InnerProductSpace.OfNorm
/-- Auxiliary definition of the inner product derived from the norm.  -/
_private.Mathlib.Analysis.InnerProductSpace.OfNorm.0.inner_ : (𝕜 : Type u_1) → [inst : RCLike 𝕜] → {E : Type u_2} → [inst_1 : NormedAddCommGroup E] → [NormedSpace 𝕜 E] → E → E → 𝕜
-- Mathlib.GroupTheory.Coset.Basic
/-- If `H ≤ K`, then `G/H ≃ G/K × K/H` constructively, using the provided right inverse
of the quotient map `G → G/K`. The classical version is `Subgroup.quotientEquivProdOfLE`.  -/
Subgroup.quotientEquivProdOfLE' : {α : Type u_1} →
  [inst : Group α] →
    {s t : Subgroup α} →
      s ≤ t → (f : α ⧸ t → α) → Function.RightInverse f QuotientGroup.mk → α ⧸ s ≃ (α ⧸ t) × ↥t ⧸ s.subgroupOf t
-- Init.Data.List.MinMax
_private.Init.Data.List.MinMax.0.List.max?_attach : ∀ {α : Type u_1} [inst : Max α] [inst_1 : Std.MaxEqOr α] {xs : List α},
  xs.attach.max? = Option.pmap (fun m hm => ⟨m, ⋯⟩) xs.max? ⋯
-- Mathlib.Algebra.Group.Units.Defs
IsAddUnit.add_val_neg : ∀ {M : Type u_1} [inst : AddMonoid M] {a : M} (h : IsAddUnit a), a + ↑(-h.addUnit) = 0
-- Mathlib.Algebra.Group.Pointwise.Finset.Interval
Finset.Iic_mul_Iic_subset' : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Preorder α] [inst_2 : DecidableEq α] [MulLeftMono α] [MulRightMono α]
  [inst_5 : LocallyFiniteOrderBot α] (a b : α), Finset.Iic a * Finset.Iic b ⊆ Finset.Iic (a * b)
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.zero_le : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  (I : FractionalIdeal S P), 0 ≤ I
-- Init.Data.Vector.Attach
Vector.reverse_attach : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n},
  xs.attach.reverse =
    Vector.map
      (fun x =>
        match x with
        | ⟨x, h⟩ => ⟨x, ⋯⟩)
      xs.reverse.attach
-- Mathlib.LinearAlgebra.Matrix.Rank
Matrix.rank.eq_1 : ∀ {m : Type um} {n : Type un} {R : Type uR} [inst : Fintype n] [inst_1 : CommSemiring R] (A : Matrix m n R),
  A.rank = Module.finrank R ↥A.mulVecLin.range
-- Init.Data.Format.Basic
/-- A directive indicating whether a given work group is able to be flattened.

- `allow` indicates that the group is allowed to be flattened; its argument is `true` if
  there is sufficient space for it to be flattened (and so it should be), or `false` if not.
- `disallow` means that this group should not be flattened irrespective of space concerns.
  This is used at levels of a `Format` outside of any flattening groups. It is necessary to track
  this so that, after a hard line break, we know whether to try to flatten the next line.
 -/
Std.Format.FlattenAllowability : Type
-- Mathlib.Data.Finset.Piecewise
Finset.piecewise_mem_Icc_of_mem_of_mem : ∀ {ι : Type u_1} (s : Finset ι) [inst : (j : ι) → Decidable (j ∈ s)] {π : ι → Type u_3} {f g f' g' : (i : ι) → π i}
  [inst_1 : (i : ι) → Preorder (π i)], f ∈ Set.Icc f' g' → g ∈ Set.Icc f' g' → s.piecewise f g ∈ Set.Icc f' g'
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.addFundamentalFrontier.eq_1 : ∀ (G : Type u_1) {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] (s : Set α),
  MeasureTheory.addFundamentalFrontier G s = s ∩ ⋃ g, ⋃ (_ : g ≠ 0), g +ᵥ s
-- Init.Data.String.Lemmas.Pattern.TakeDrop.String
String.startsWith_string_iff : ∀ {pat s : String}, s.startsWith pat = true ↔ pat.toList <+: s.toList
-- Mathlib.Algebra.BigOperators.ModEq
Nat.prod_modEq_ite : ∀ {α : Type u_1} {n : ℕ} {f : α → ℕ} [inst : DecidableEq α] {s : Finset α} {a : α},
  (∀ x ∈ s, x ≠ a → f x ≡ 1 [MOD n]) → ∏ x ∈ s, f x ≡ if a ∈ s then f a else 1 [MOD n]
-- Mathlib.CategoryTheory.Pi.Monoidal
CategoryTheory.Pi.δ_def : ∀ {I : Type w₁} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)]
  [inst_1 : (i : I) → CategoryTheory.MonoidalCategory (C i)] (i : I) (X Y : (i : I) → C i),
  CategoryTheory.Functor.OplaxMonoidal.δ (CategoryTheory.Pi.eval C i) X Y =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj (X i) (Y i))
-- Mathlib.NumberTheory.LSeries.Dirichlet
/-- The abscissa of absolute convergence of the L-series of a Dirichlet character mod `N > 0`
is `1`.  -/
DirichletCharacter.absicssaOfAbsConv_eq_one : ∀ {N : ℕ}, N ≠ 0 → ∀ (χ : DirichletCharacter ℂ N), (LSeries.abscissaOfAbsConv fun n => χ ↑n) = 1
-- Mathlib.Analysis.Convex.Between
sbtw_sub_const_iff : ∀ {R : Type u_1} {V : Type u_2} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] {x y z : V} (v : V), Sbtw R (x - v) (y - v) (z - v) ↔ Sbtw R x y z
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
/-- Shorthand for the 0th group homology of a `k`-linear `G`-representation `A`, `H₀(G, A)`,
defined as the 0th homology of the complex of inhomogeneous chains of `A`.  -/
groupHomology.H0 : {k G : Type u} → [inst : CommRing k] → [inst_1 : Group G] → Rep.{u, u, u} k G → ModuleCat k
-- Mathlib.Algebra.Algebra.Tower
AlgEquiv.coe_restrictScalars_symm : ∀ (R : Type u) {S : Type v} {A : Type w} {B : Type u₁} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : Semiring A] [inst_3 : Semiring B] [inst_4 : Algebra R S] [inst_5 : Algebra S A] [inst_6 : Algebra S B]
  [inst_7 : Algebra R A] [inst_8 : Algebra R B] [inst_9 : IsScalarTower R S A] [inst_10 : IsScalarTower R S B]
  (f : A ≃ₐ[S] B), (AlgEquiv.restrictScalars R f).symm.toRingEquiv = f.symm.toRingEquiv
-- Lean.Widget.Diff
_private.Lean.Widget.Diff.0.Lean.Widget.ExprDiffTag.noConfusionType : Sort v✝ → Lean.Widget.ExprDiffTag✝ → Lean.Widget.ExprDiffTag✝ → Sort v✝
-- Mathlib.Dynamics.BirkhoffSum.NormedSpace
/-- If a function `g` is bounded along the positive orbit of `x` under `f`,
then the difference between Birkhoff averages of `g`
along the orbit of `f x` and along the orbit of `x`
tends to zero.

See also `tendsto_birkhoffAverage_apply_sub_birkhoffAverage'`.  -/
tendsto_birkhoffAverage_apply_sub_birkhoffAverage : ∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] (𝕜 : Type u_3) [inst_1 : RCLike 𝕜]
  [inst_2 : NormedSpace 𝕜 E] {f : α → α} {g : α → E} {x : α},
  Bornology.IsBounded (Set.range fun x_1 => g (f^[x_1] x)) →
    Filter.Tendsto (fun n => birkhoffAverage 𝕜 f g n (f x) - birkhoffAverage 𝕜 f g n x) Filter.atTop (nhds 0)
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.any_map : ∀ {α β β' : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m β] [Std.Iterators.Finite α m] [inst_2 : Monad m]
  [inst_3 : Std.IteratorLoop α m m] [LawfulMonad m] [Std.LawfulIteratorLoop α m m] {it : Std.IterM m β} {f : β → β'}
  {p : β' → Bool}, Std.IterM.any p (Std.IterM.map f it) = Std.IterM.any (fun x => p (f x)) it
-- Init.Data.SInt.Basic
/-- Subtracts one 32-bit signed integer from another, wrapping around on over- or underflow. Usually
accessed via the `-` operator.

This function is overridden at runtime with an efficient implementation.
 -/
Int32.sub : Int32 → Int32 → Int32
-- Mathlib.CategoryTheory.MorphismProperty.IsSmall
CategoryTheory.MorphismProperty.isSmall_iSup : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {α : Type u_1} (W : α → CategoryTheory.MorphismProperty C)
  [Small.{w, u_1} α] [∀ (a : α), CategoryTheory.MorphismProperty.IsSmall.{w, v, u} (W a)],
  CategoryTheory.MorphismProperty.IsSmall.{w, v, u} (iSup W)
-- Mathlib.Condensed.TopCatAdjunction
/-- The map part of the functor `CondensedSet ⥤ TopCat`  -/
CondensedSet.toTopCatMap : {X Y : CondensedSet} → (X ⟶ Y) → (X.toTopCat ⟶ Y.toTopCat)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Equiv.getKeyD_eq : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] {k fallback : α}, m₁.WF → m₂.WF → m₁.Equiv m₂ → m₁.getKeyD k fallback = m₂.getKeyD k fallback
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.isCharThreeJNeZeroNF_iff : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R), W.IsCharThreeJNeZeroNF ↔ W.a₁ = 0 ∧ W.a₃ = 0 ∧ W.a₄ = 0
-- Mathlib.Geometry.Euclidean.Sphere.Basic
EuclideanGeometry.Sphere.nonempty_iff : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [NormedSpace ℝ V] [inst_2 : MetricSpace P]
  [NormedAddTorsor V P] [Nontrivial V] {s : EuclideanGeometry.Sphere P},
  (Metric.sphere s.center s.radius).Nonempty ↔ 0 ≤ s.radius
-- Mathlib.Algebra.Group.Opposite
AddOpposite.instAddCommGroup : {α : Type u_1} → [AddCommGroup α] → AddCommGroup αᵃᵒᵖ
-- Mathlib.GroupTheory.Coprod.Basic
/-- An additive equivalence between `AddMonoid.Coprod (AddMonoid.Coprod M N) P` and
`AddMonoid.Coprod M (AddMonoid.Coprod N P)`.  -/
AddEquiv.coprodAssoc : (M : Type u_1) →
  (N : Type u_2) →
    (P : Type u_3) →
      [inst : AddMonoid M] →
        [inst_1 : AddMonoid N] →
          [inst_2 : AddMonoid P] →
            AddMonoid.Coprod (AddMonoid.Coprod M N) P ≃+ AddMonoid.Coprod M (AddMonoid.Coprod N P)
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.ExcenterExists.excenter_mem_affineSpan_range : ∀ {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} {signs : Finset (Fin (n + 1))},
  s.ExcenterExists signs → s.excenter signs ∈ affineSpan ℝ (Set.range s.points)
-- Mathlib.CategoryTheory.Triangulated.TStructure.Basic
CategoryTheory.Triangulated.TStructure.le_isClosedUnderIsomorphisms : ∀ {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]
  (self : CategoryTheory.Triangulated.TStructure C) (n : ℤ), (self.le n).IsClosedUnderIsomorphisms
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get_insertMany!_list_of_contains_eq_false : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [inst : Std.TransOrd α]
  [inst_1 : BEq α] [inst_2 : Std.LawfulBEqOrd α] (h : t.WF) {l : List (α × β)} {k : α}
  (h₁ : (List.map Prod.fst l).contains k = false)
  {h' : Std.DTreeMap.Internal.Impl.contains k ↑(Std.DTreeMap.Internal.Impl.Const.insertMany! t l) = true},
  Std.DTreeMap.Internal.Impl.Const.get (↑(Std.DTreeMap.Internal.Impl.Const.insertMany! t l)) k h' =
    Std.DTreeMap.Internal.Impl.Const.get t k ⋯
-- Mathlib.Data.Seq.Computation
/-- `runFor c n` evaluates `c` for `n` steps and returns the result, or `none`
if it did not terminate after `n` steps.  -/
Computation.runFor : {α : Type u} → Computation α → ℕ → Option α
-- Mathlib.Algebra.Group.Subgroup.Pointwise
Subgroup.conj_smul_subgroupOf : ∀ {G : Type u_2} [inst : Group G] {P H : Subgroup G},
  P ≤ H → ∀ (h : ↥H), MulAut.conj h • P.subgroupOf H = (MulAut.conj ↑h • P).subgroupOf H
-- Mathlib.Data.Nat.BinaryRec
Nat.shiftRight_one : ∀ (n : ℕ), n >>> 1 = n / 2
-- Mathlib.RingTheory.Bialgebra.Convolution
BialgHom.toAlgHom_convMul : ∀ {R : Type u_1} {A : Type u_2} {C : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Semiring C]
  [inst_3 : Bialgebra R A] [inst_4 : Bialgebra R C] [inst_5 : Coalgebra.IsCocomm R C] (f g : WithConv (C →ₐc[R] A)),
  WithConv.toConv ↑(f * g).ofConv = WithConv.toConv ↑f.ofConv * WithConv.toConv ↑g.ofConv
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.EqCnstrProof.mul.sizeOf_spec : ∀ (k : ℤ) (e : Lean.Meta.Grind.Arith.CommRing.EqCnstr),
  sizeOf (Lean.Meta.Grind.Arith.CommRing.EqCnstrProof.mul k e) = 1 + sizeOf k + sizeOf e
-- Mathlib.Algebra.Module.ULift
ULift.mulAction' : {R : Type u} → {M : Type v} → [inst : Monoid R] → [MulAction R M] → MulAction R (ULift.{u_1, v} M)
-- Mathlib.Topology.Compactness.Lindelof
Filter.ofCountableUnion.congr_simp : ∀ {α : Type u_2} (l l_1 : Set (Set α)) (e_l : l = l_1)
  (hUnion : ∀ (S : Set (Set α)), S.Countable → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l) (hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l),
  Filter.ofCountableUnion l hUnion hmono = Filter.ofCountableUnion l_1 ⋯ ⋯
-- Mathlib.Algebra.Module.Submodule.Lattice
Submodule.toAddSubgroup_eq_top : ∀ {R : Type u_4} {M : Type u_5} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {p : Submodule R M},
  p.toAddSubgroup = ⊤ ↔ p = ⊤
-- Mathlib.LinearAlgebra.Matrix.Nonsingular
/-- If a matrix over a commutative semiring with cancellative addition is nonsingular, then its
columns are linearly independent. Generalizes `Matrix.linearIndependent_cols_of_det_ne_zero`.  -/
Matrix.Nonsingular.linearIndependent_col : ∀ {R : Type u_1} {n : Type u_3} [inst : CommSemiring R] [inst_1 : Fintype n] [inst_2 : DecidableEq n] {A : Matrix n n R}
  [IsCancelAdd R], A.Nonsingular → LinearIndependent R A.col
-- Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
/-- A trivial fibration is a morphism that is both a fibration and a weak equivalence.  -/
HomotopicalAlgebra.trivialFibrations : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [HomotopicalAlgebra.CategoryWithFibrations C] →
      [HomotopicalAlgebra.CategoryWithWeakEquivalences C] → CategoryTheory.MorphismProperty C
-- Mathlib.Algebra.Group.Action.Hom
AddAction.isPretransitive_compHom : ∀ {E : Type u_4} {F : Type u_5} {G : Type u_6} [inst : AddMonoid E] [inst_1 : AddMonoid F] [inst_2 : AddAction F G]
  [AddAction.IsPretransitive F G] {f : E →+ F}, Function.Surjective ⇑f → AddAction.IsPretransitive E G
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
IsAddCyclic.card_addOrderOf_eq_totient : ∀ {α : Type u_1} [inst : AddGroup α] [IsAddCyclic α] [inst_2 : Fintype α] {d : ℕ},
  d ∣ Fintype.card α → {a | addOrderOf a = d}.card = d.totient
-- Std.Time.Format.Modifier
Std.Time.Modifier.k.injEq : ∀ (presentation presentation_1 : Std.Time.Number),
  (Std.Time.Modifier.k presentation = Std.Time.Modifier.k presentation_1) = (presentation = presentation_1)
-- Mathlib.CategoryTheory.Preadditive.Yoneda.Basic
CategoryTheory.preadditiveYoneda_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] (Y : C),
  CategoryTheory.preadditiveYoneda.obj Y =
    (CategoryTheory.preadditiveYonedaObj Y).comp
      (CategoryTheory.forget₂ (ModuleCat (CategoryTheory.End Y)) AddCommGrpCat)
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instAddCommMonoid : {α : Type u_1} → [AddCommMonoid α] → AddCommMonoid αᵒᵈ
-- Lean.Expr
Lean.instInhabitedFVarIdSet : Inhabited Lean.FVarIdSet
-- Init.Data.Vector.Perm
Vector.Perm.extract : ∀ {α : Type u_1} {n : ℕ} {xs ys : Vector α n},
  xs.Perm ys →
    ∀ {lo hi : ℕ},
      (∀ i < lo, xs[i]? = ys[i]?) → (∀ (i : ℕ), hi ≤ i → xs[i]? = ys[i]?) → (xs.extract lo hi).Perm (ys.extract lo hi)
-- Mathlib.Algebra.Group.Conj
AddConjClasses.mk.eq_1 : ∀ {α : Type u_1} [inst : AddMonoid α] (a : α), AddConjClasses.mk a = ⟦a⟧
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
uniformity_eq_comap_nhds_zero_swapped : ∀ (Gᵣ : Type u_3) [inst : UniformSpace Gᵣ] [inst_1 : AddGroup Gᵣ] [IsRightUniformAddGroup Gᵣ],
  uniformity Gᵣ = Filter.comap (fun x => x.1 - x.2) (nhds 0)
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
/-- Every nonzero element of a group with zero is invertible.  -/
LinearOrderedCommGroupWithZero.mul_inv_cancel : ∀ {α : Type u_3} [self : LinearOrderedCommGroupWithZero α] (a : α), a ≠ 0 → a * a⁻¹ = 1
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get?_diff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : LawfulBEq α]
  {k : α}, (m₁ \ m₂).get? k = if k ∈ m₂ then none else m₁.get? k
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.forM_eq_forM : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} {m' : Type w → Type w'} [inst : Monad m'] [LawfulMonad m']
  {f : (a : α) → β a → m' PUnit.{w + 1}}, Std.DHashMap.Raw.forM f m = forM m fun a => f a.fst a.snd
-- Mathlib.MeasureTheory.VectorMeasure.SetIntegral
MeasureTheory.VectorMeasure.setIntegral_eq_zero_of_ae_eq_zero : ∀ {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedAddCommGroup G] {μ : MeasureTheory.VectorMeasure X F} {f : X → E}
  {t : Set X} [inst_3 : NormedSpace ℝ E] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G},
  (∀ᵐ (x : X) ∂μ.variation, x ∈ t → f x = 0) → ∫ᵛ (x : X) in t, f x ∂[B; μ] = 0
-- Mathlib.Order.Filter.IsBounded
Filter.not_isBoundedUnder_of_tendsto_atBot : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder β] [NoMinOrder β] {f : α → β} {l : Filter α} [l.NeBot],
  Filter.Tendsto f l Filter.atBot → ¬Filter.IsBoundedUnder (fun x1 x2 => x2 ≤ x1) l f
-- Lean.Elab.Tactic.Simp
_private.Lean.Elab.Tactic.Simp.0.Lean.Elab.Tactic.instEvalExprConfigCtx : Lean.Elab.ConfigEval.EvalExpr Lean.Meta.Simp.ConfigCtx
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.CoconeMorphism.map_w_assoc : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] {F : CategoryTheory.Functor J C}
  {c c' : CategoryTheory.Limits.Cocone F} (f : c' ⟶ c) (G : CategoryTheory.Functor C D) (j : J) {Z : D}
  (h : G.obj c.pt ⟶ Z),
  CategoryTheory.CategoryStruct.comp (G.map (c'.ι.app j)) (CategoryTheory.CategoryStruct.comp (G.map f.hom) h) =
    CategoryTheory.CategoryStruct.comp (G.map (c.ι.app j)) h
-- Mathlib.Dynamics.Ergodic.AddCircle
AddCircle.ergodic_nsmul : ∀ {T : ℝ} [hT : Fact (0 < T)] {n : ℕ}, 1 < n → Ergodic (fun y => n • y) MeasureTheory.volume
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.EqCnstrProof.superpose_tail_idempotent : Lean.Grind.AC.Var → Lean.Meta.Grind.AC.EqCnstr → Lean.Meta.Grind.AC.EqCnstrProof
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.prod_norm_sq_eq_of_L2 : ∀ {α : Type u_2} {β : Type u_3} [inst : SeminormedAddCommGroup α] [inst_1 : SeminormedAddCommGroup β]
  (x : WithLp 2 (α × β)), ‖x‖ ^ 2 = ‖x.fst‖ ^ 2 + ‖x.snd‖ ^ 2
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.LHom.comp_onBoundedFormula : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} {α : Type u'} {n : ℕ} {L'' : FirstOrder.Language} (φ : L' →ᴸ L'')
  (ψ : L →ᴸ L'), (φ.comp ψ).onBoundedFormula = φ.onBoundedFormula ∘ ψ.onBoundedFormula
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
SSet.prodStdSimplex.pairingCore.IsType₂.simplex_snd_apply : ∀ {m : ℕ} {k : Fin (m + 1)} {n : ℕ} {x : ((SSet.horn (m + 1) k.castSucc).unionProd (SSet.boundary n)).N}
  (hx : SSet.prodStdSimplex.pairingCore.IsType₂ x) {d : ℕ} (hd : x.dim = d) (i : Fin (d + 2)),
  (hx.simplex hd).2 i = (SSet.prodStdSimplex.pairingCore.IsType₂.φ x hd i).2
-- Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
SimpleGraph.Walk.isSubwalk_iff_darts_isInfix : ∀ {V : Type u_1} {G : SimpleGraph V} {u v u' v' : V} {p₁ : G.Walk u v} {p₂ : G.Walk u' v'},
  ¬p₁.Nil → (p₁.IsSubwalk p₂ ↔ p₁.darts <:+: p₂.darts)
-- Mathlib.RingTheory.Etale.Kaehler
Algebra.Extension.tensorCotangent.congr_simp : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] [inst_5 : Algebra S T] {P : Algebra.Extension R S}
  {Q : Algebra.Extension R T} (f f_1 : P.Hom Q) (e_f : f = f_1) [alg : Algebra P.Ring Q.Ring]
  (halg : algebraMap P.Ring Q.Ring = f.toRingHom)
  (H : Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg))),
  Algebra.Extension.tensorCotangent f halg H = Algebra.Extension.tensorCotangent f_1 ⋯ ⋯
-- Mathlib.CategoryTheory.Functor.KanExtension.Dense
_private.Mathlib.CategoryTheory.Functor.KanExtension.Dense.0.CategoryTheory.Functor.IsDense.of_fullyFaithful_restrictedULiftYoneda.match_1_1.splitter : {C : Type u_4} →
  {D : Type u_5} →
    [inst : CategoryTheory.Category.{u_1, u_4} C] →
      [inst_1 : CategoryTheory.Category.{u_2, u_5} D] →
        {F : CategoryTheory.Functor C D} →
          (Y : D) →
            (X : C) →
              (motive : ((CategoryTheory.Presheaf.restrictedULiftYoneda F).obj Y).obj (Opposite.op X) → Sort u_6) →
                (x : ((CategoryTheory.Presheaf.restrictedULiftYoneda F).obj Y).obj (Opposite.op X)) →
                  ((x : (CategoryTheory.yoneda.obj Y).obj (F.op.obj (Opposite.op X))) → motive { down := x }) → motive x