mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Shift.Adjunction
/-- Given an adjunction `adj : F ⊣ G`, `a` in `A` and commutation isomorphisms
`e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a` and
`e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a`, compatibility of `e₁` and `e₂` with the
unit of the adjunction `adj` implies compatibility with the counit of `adj`.
 -/
CategoryTheory.Adjunction.CommShift.compatibilityCounit_of_compatibilityUnit : ∀ {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] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  (adj : F ⊣ G) {A : Type u_3} [inst_2 : AddMonoid A] [inst_3 : CategoryTheory.HasShift C A]
  [inst_4 : CategoryTheory.HasShift D A] {a : A}
  (e₁ : (CategoryTheory.shiftFunctor C a).comp F ≅ F.comp (CategoryTheory.shiftFunctor D a))
  (e₂ : (CategoryTheory.shiftFunctor D a).comp G ≅ G.comp (CategoryTheory.shiftFunctor C a)),
  CategoryTheory.Adjunction.CommShift.CompatibilityUnit adj e₁ e₂ →
    CategoryTheory.Adjunction.CommShift.CompatibilityCounit adj e₁ e₂
-- Init.Core
Iff.rfl : ∀ {a : Prop}, a ↔ a
-- Mathlib.Order.Hom.Bounded
TopHom.instTopHomClass : ∀ {α : Type u_2} {β : Type u_3} [inst : Top α] [inst_1 : Top β], TopHomClass (TopHom α β) α β
-- Mathlib.Topology.Piecewise
continuousWithinAt_update_same : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s : Set α}
  {x : α} [inst_2 : DecidableEq α] {y : β},
  ContinuousWithinAt (Function.update f x y) s x ↔ Filter.Tendsto f (nhdsWithin x (s \ {x})) (nhds y)
-- Init.GetElem
Fin.getElem_fin : ∀ {Cont : Type u_1} {Elem : Type u_2} {Dom : Cont → ℕ → Prop} {n : ℕ} [inst : GetElem Cont ℕ Elem Dom] (a : Cont)
  (i : Fin n) (h : Dom a ↑i), a[i] = a[↑i]
-- Mathlib.AlgebraicTopology.SimplicialSet.Nerve
CategoryTheory.nerveMap_app_mk₀ : ∀ {C D : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Category.{v, u} D]
  (F : CategoryTheory.Functor C D) (x : C),
  (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.nerveMap F).app (Opposite.op { len := 0 })))
      (CategoryTheory.ComposableArrows.mk₀ x) =
    CategoryTheory.ComposableArrows.mk₀ (F.obj x)
-- Mathlib.Algebra.Group.Ext
AddCancelMonoid.ext : ∀ {M : Type u_1} ⦃m₁ m₂ : AddCancelMonoid M⦄, HAdd.hAdd = HAdd.hAdd → m₁ = m₂
-- Mathlib.Data.Matrix.Basic
AlgEquiv.mapMatrix_symm : ∀ {m : Type u_2} {R : Type u_7} {α : Type u_11} {β : Type u_12} [inst : Fintype m] [inst_1 : DecidableEq m]
  [inst_2 : CommSemiring R] [inst_3 : Semiring α] [inst_4 : Semiring β] [inst_5 : Algebra R α] [inst_6 : Algebra R β]
  (f : α ≃ₐ[R] β), f.mapMatrix.symm = f.symm.mapMatrix
-- Mathlib.CategoryTheory.Monoidal.Braided.Multifunctor
/-- The trifunctor `X₁ X₂ X₃ ↦ X₁ ⊗ (X₃ ⊗ X₂)`  -/
CategoryTheory.BraidedCategory.Hexagon.functor₁₃₂' : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [CategoryTheory.MonoidalCategory C] →
      CategoryTheory.Functor C (CategoryTheory.Functor C (CategoryTheory.Functor C C))
-- Batteries.Data.List.Perm
List.Perm.insertP : ∀ {α : Type u_1} {l₁ l₂ : List α} (p : α → Bool) (a : α), l₁.Perm l₂ → (List.insertP p a l₁).Perm (List.insertP p a l₂)
-- Mathlib.Topology.Separation.GDelta
IsGδ.singleton : ∀ {X : Type u_1} [inst : TopologicalSpace X] [FirstCountableTopology X] [T1Space X] (x : X), IsGδ {x}
-- Mathlib.Data.Vector.MapLemmas
List.Vector.map₂_flip : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : ℕ} (xs : List.Vector α n) (ys : List.Vector β n) (f : α → β → γ),
  List.Vector.map₂ f xs ys = List.Vector.map₂ (flip f) ys xs
-- Mathlib.Algebra.Homology.Opposite
/-- If `K` is a homological complex in the opposite category,
then the homology of `K.unop` identifies to the opposite of the homology of `K`.  -/
HomologicalComplex.homologyUnop : {ι : Type u_1} →
  {V : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_2} V] →
      {c : ComplexShape ι} →
        [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
          (K : HomologicalComplex Vᵒᵖ c) →
            (i : ι) → [inst_2 : K.HasHomology i] → K.unop.homology i ≅ Opposite.unop (K.homology i)
-- Mathlib.Analysis.SpecialFunctions.Log.Deriv
Real.differentiableOn_log : DifferentiableOn ℝ Real.log {0}ᶜ
-- Mathlib.Analysis.Meromorphic.Order
/-- Eta-expanded form of `meromorphicOrderAt_div`

---

The order of a quotient is the difference of the orders.
 -/
fun_meromorphicOrderAt_div : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {𝕜' : Type u_4} [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {x : 𝕜} {f g : 𝕜 → 𝕜'},
  MeromorphicAt f x →
    MeromorphicAt g x → meromorphicOrderAt (fun i => f i / g i) x = meromorphicOrderAt f x - meromorphicOrderAt g x
-- Mathlib.Data.PNat.Basic
PNat.ofNat_lt_ofNat : ∀ {m n : ℕ} [inst : NeZero m] [inst_1 : NeZero n], OfNat.ofNat m < OfNat.ofNat n ↔ OfNat.ofNat m < OfNat.ofNat n
-- Mathlib.MeasureTheory.VectorMeasure.Variation.Basic
MeasureTheory.VectorMeasure.variation_eq_zero : ∀ {X : Type u_1} {V : Type u_2} {mX : MeasurableSpace X} [inst : TopologicalSpace V] [inst_1 : ENormedAddCommMonoid V]
  [inst_2 : T2Space V] {μ : MeasureTheory.VectorMeasure X V}, μ.variation = 0 ↔ μ = 0
-- Mathlib.CategoryTheory.Iso
CategoryTheory.Iso.inv_eq_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (α : X ≅ Y) (β : Y ≅ X),
  α.inv = β.hom ↔ β.inv = α.hom
-- Mathlib.RingTheory.SimpleModule.Basic
/-- The isomorphism relation for composition series of modules implies isomorphism of quotients.  -/
JordanHolderLattice.Iso.linearEquiv : {R : Type u_2} →
  [inst : Ring R] →
    {M : Type u_4} →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          {X Y : Submodule R M × Submodule R M} →
            JordanHolderLattice.Iso X Y →
              (↥X.2 ⧸ Submodule.comap X.2.subtype X.1) ≃ₗ[R] ↥Y.2 ⧸ Submodule.comap Y.2.subtype Y.1
-- Mathlib.Topology.Category.Compactum
Profinite.forgetCreatesLimits : CategoryTheory.CreatesLimits (CategoryTheory.forget Profinite)
-- Mathlib.Analysis.Analytic.Uniqueness
/-- A one-dimensional formal multilinear series representing a locally zero function is zero.  -/
HasFPowerSeriesAt.eq_zero_of_eventually : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {p : FormalMultilinearSeries 𝕜 𝕜 E} {f : 𝕜 → E} {x : 𝕜},
  HasFPowerSeriesAt f p x → f =ᶠ[nhds x] 0 → p = 0
-- Mathlib.Algebra.Category.Ring.Basic
SemiRingCat.coe_of : ∀ (R : Type u) [inst : Semiring R], ↑(SemiRingCat.of R) = R
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidIso.toOrderIso_injective : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Mul α] [inst_3 : Mul β],
  Function.Injective OrderMonoidIso.toOrderIso
-- Init.Control.Lawful.Instances
ExceptT.bind.eq_1 : ∀ {ε : Type u} {m : Type u → Type v} [inst : Monad m] {α β : Type u} (ma : ExceptT ε m α) (f : α → ExceptT ε m β),
  ma.bind f = ExceptT.mk (ma >>= ExceptT.bindCont f)
-- Mathlib.Topology.Algebra.Group.Basic
Homeomorph.divRight.eq_1 : ∀ {G : Type w} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalGroup G] (x : G),
  Homeomorph.divRight x = { toEquiv := Equiv.divRight x, continuous_toFun := ⋯, continuous_invFun := ⋯ }
-- Mathlib.RingTheory.Spectrum.Maximal.Localization
MaximalSpectrum.mapPiLocalization_naturality : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] (f : R →+* S)
  (hf : Function.Bijective ⇑f),
  (MaximalSpectrum.mapPiLocalization f hf).comp ↑(MaximalSpectrum.toPiLocalization R) =
    (MaximalSpectrum.toPiLocalization S).comp f
-- Mathlib.Order.KrullDimension
/-- The coheight of an element in a series is larger or equal to its reverse index in the series.
 -/
Order.rev_index_le_coheight : ∀ {α : Type u_1} [inst : Preorder α] (p : LTSeries α) (i : Fin (p.length + 1)), ↑↑i.rev ≤ Order.coheight (p.toFun i)
-- Mathlib.CategoryTheory.Monoidal.Braided.Multifunctor
/-- The trifunctor `X₁ X₂ X₃ ↦ (X₁ ⊗ X₂) ⊗ X₃`  -/
CategoryTheory.BraidedCategory.Hexagon.functor₁₂₃ : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [CategoryTheory.MonoidalCategory C] →
      CategoryTheory.Functor C (CategoryTheory.Functor C (CategoryTheory.Functor C C))
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.memLp_const_iff : ∀ {α : Type u_1} {E : Type u_4} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup E]
  {p : ENNReal} {c : E}, p ≠ 0 → p ≠ ⊤ → (MeasureTheory.MemLp (fun x => c) p μ ↔ c = 0 ∨ μ Set.univ < ⊤)
-- Init.Data.List.Lemmas
_private.Init.Data.List.Lemmas.0.List.filter.match_1.splitter : (motive : Bool → Sort u_1) → (x : Bool) → (Unit → motive true) → (Unit → motive false) → motive x
-- Mathlib.RingTheory.DividedPowers.SubDPIdeal
/-- A `SubDPIdeal` of `I` is a sub-ideal `J` of `I` such that for all `n > 0` `x ∈ J`,
`hI.dpow n j ∈ J`. The unbundled version of this definition is called `IsSubDPIdeal`.  -/
DividedPowers.SubDPIdeal : {A : Type u_1} → [inst : CommSemiring A] → {I : Ideal A} → DividedPowers I → Type u_1
-- Std.Sat.AIG.Relabel
Std.Sat.AIG.Entrypoint.relabel_unsat_iff : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {β : Type} [inst_2 : Hashable β] [inst_3 : DecidableEq β]
  [Nonempty α] {entry : Std.Sat.AIG.Entrypoint α} {r : α → β},
  (∀ (x y : α), x ∈ entry.aig → y ∈ entry.aig → r x = r y → x = y) →
    ((Std.Sat.AIG.Entrypoint.relabel r entry).Unsat ↔ entry.Unsat)
-- Init.Core
Quot.indBeta : ∀ {α : Sort u} {r : α → α → Prop} {motive : Quot r → Prop} (p : ∀ (a : α), motive (Quot.mk r a)) (a : α), ⋯ = ⋯
-- Lean.Expr
/-- Return `true` if the given expression is a lambda abstraction aka anonymous function.  -/
Lean.Expr.isLambda : Lean.Expr → Bool
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.ordered_keys_toList : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp],
  List.Pairwise (fun a b => cmp a.fst b.fst = Ordering.lt) t.toList
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
IsTopologicalAddGroup.tendstoUniformlyOn_iff : ∀ {ι : Type u_1} {α : Type u_2} {G : Type u_3} [inst : AddGroup G] [u : UniformSpace G]
  [inst_1 : IsTopologicalAddGroup G] (F : ι → α → G) (f : α → G) (p : Filter ι) (s : Set α),
  IsTopologicalAddGroup.rightUniformSpace G = u →
    (TendstoUniformlyOn F f p s ↔ ∀ u_1 ∈ nhds 0, ∀ᶠ (i : ι) in p, ∀ a ∈ s, F i a - f a ∈ u_1)
-- Mathlib.Logic.Embedding.Basic
Function.Embedding.setValue_eq_of_ne : ∀ {α : Sort u_1} {β : Sort u_2} {f : α ↪ β} {a : α} {b : β} {c : α} [inst : (a' : α) → Decidable (a' = a)]
  [inst_1 : (a' : α) → Decidable (f a' = b)], c ≠ a → f c ≠ b → (f.setValue a b) c = f c
-- Mathlib.Topology.Maps.Basic
Topology.IsInducing.id : ∀ {X : Type u_1} [inst : TopologicalSpace X], Topology.IsInducing id
-- Mathlib.Geometry.Euclidean.Sphere.Tangent
EuclideanGeometry.Sphere.IsIntTangent.eq_1 : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (s₁ s₂ : EuclideanGeometry.Sphere P), s₁.IsIntTangent s₂ = ∃ p, s₁.IsIntTangentAt s₂ p
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.Hom.mk'.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {M N : CategoryTheory.Mon C} (f : M.X ⟶ N.X)
  (one_f : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one f = CategoryTheory.MonObj.one)
  (mul_f :
    CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul f =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f f)
        CategoryTheory.MonObj.mul),
  CategoryTheory.Mon.Hom.mk' f one_f mul_f = { hom := f, isMonHom_hom := ⋯ }
-- Mathlib.Algebra.Group.Action.Units
Units.smul_def : ∀ {M : Type u_3} {α : Type u_5} [inst : Monoid M] [inst_1 : SMul M α] (m : Mˣ) (a : α), m • a = ↑m • a
-- Mathlib.Analysis.Distribution.TemperedDistribution
/-- **Alias** of `TemperedDistribution.fourierInv_apply`. -/
TemperedDistribution.fourierTransformInv_apply : ∀ {E : Type u_3} {F : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E]
  [inst_2 : FiniteDimensional ℝ E] [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] [inst_5 : AddCommGroup F]
  [inst_6 : Module ℂ F] [inst_7 : TopologicalSpace F] [inst_8 : IsTopologicalAddGroup F]
  [inst_9 : ContinuousConstSMul ℂ F] (f : TemperedDistribution E F) (g : SchwartzMap E ℂ),
  (FourierTransformInv.fourierInv f) g = f (FourierTransformInv.fourierInv g)
-- Init.Data.Iterators.Consumers.Monadic.Loop
Std.IteratorLoop.ext_iff : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} {inst : Std.Iterator α m β} {n : Type x → Type x'}
  {x y : Std.IteratorLoop α m n}, x = y ↔ Std.IteratorLoop.forIn = Std.IteratorLoop.forIn
-- Mathlib.Combinatorics.Additive.Convolution
Finset.card_inter_vadd : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : DecidableEq G] (A B : Finset G) (x : G),
  (A ∩ (x +ᵥ B)).card = A.addConvolution (-B) x
-- Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
HomotopicalAlgebra.BifibrantObject.instIsLocalizationCompCofibrantObjectιCofibrantObjectWeakEquivalences : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] {D : Type u_1}
  [inst_2 : CategoryTheory.Category.{u_2, u_1} D] (L : CategoryTheory.Functor (HomotopicalAlgebra.CofibrantObject C) D)
  [L.IsLocalization (HomotopicalAlgebra.weakEquivalences (HomotopicalAlgebra.CofibrantObject C))],
  (HomotopicalAlgebra.BifibrantObject.ιCofibrantObject.comp L).IsLocalization
    (HomotopicalAlgebra.weakEquivalences (HomotopicalAlgebra.BifibrantObject C))
-- Mathlib.Analysis.Normed.Group.Basic
/-- **Alias** of the reverse direction of `hasCompactSupport_norm_iff`. -/
HasCompactSupport.norm : ∀ {α : Type u_2} {E : Type u_5} [inst : NormedAddGroup E] [inst_1 : TopologicalSpace α] {f : α → E},
  HasCompactSupport f → HasCompactSupport fun x => ‖f x‖
-- Std.Sync.Channel
/-- How many slots in `buf` are currently used. This is used to disambiguate between an empty and a
full buffer without sacrificing a slot for indicating that.
 -/
_private.Std.Sync.Channel.0.Std.CloseableChannel.Bounded.State.bufCount : {α : Type} → Std.CloseableChannel.Bounded.State✝ α → ℕ
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.Supports.eq_1 : ∀ (K S : Finset Turing.PartrecToTM2.Λ'),
  Turing.PartrecToTM2.Supports K S = ∀ q ∈ K, Turing.TM2.SupportsStmt S (Turing.PartrecToTM2.tr q)
-- Mathlib.GroupTheory.Torsion
CommGroup.freeRank_eq_zero : ∀ {G : Type u_1} [inst : CommGroup G], IsMulTorsion G → ∀ [inst_1 : Group.FG G], CommGroup.freeRank G = 0
-- Mathlib.CategoryTheory.Adjunction.Lifting.Left
/-- The adjoint triangle theorem: Suppose `U : B ⥤ C` has a left adjoint `F` such that each counit
`ε_X : FUX ⟶ X` is a regular epimorphism. Then if a category `A` has coequalizers of reflexive
pairs, then a functor `R : A ⥤ B` has a left adjoint if the composite `R ⋙ U` does.

Note the converse is true (with weaker assumptions), by `Adjunction.comp`.
See https://ncatlab.org/nlab/show/adjoint+triangle+theorem
 -/
CategoryTheory.isRightAdjoint_triangle_lift : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {U : CategoryTheory.Functor B C} {F : CategoryTheory.Functor C B} (R : CategoryTheory.Functor A B) (adj₁ : F ⊣ U)
  (h : (X : B) → CategoryTheory.RegularEpi (adj₁.counit.app X)) [CategoryTheory.Limits.HasReflexiveCoequalizers A]
  [(R.comp U).IsRightAdjoint], R.IsRightAdjoint
-- Mathlib.AlgebraicGeometry.AffineScheme
/-- Let `P` be a predicate on the affine open sets of `X` satisfying
1. If `P` holds on `U`, then `P` holds on the basic open set of every section on `U`.
2. If `P` holds for a family of basic open sets covering `U`, then `P` holds for `U`.
3. There exists an affine open cover of `X` each satisfying `P`.

Then `P` holds for every affine open of `X`.

This is also known as the **Affine communication lemma** in [*The rising sea*][RisingSea].  -/
AlgebraicGeometry.of_affine_open_cover : ∀ {X : AlgebraicGeometry.Scheme} {P : ↑X.affineOpens → Prop} {ι : Sort u_2} (U : ι → ↑X.affineOpens),
  ⨆ i, ↑(U i) = ⊤ →
    ∀ (V : ↑X.affineOpens),
      (∀ (U : ↑X.affineOpens) (f : ↑(X.presheaf.obj (Opposite.op ↑U))), P U → P (X.affineBasicOpen f)) →
        (∀ (U : ↑X.affineOpens) (s : Finset ↑(X.presheaf.obj (Opposite.op ↑U))),
            Ideal.span ↑s = ⊤ → (∀ (f : ↥s), P (X.affineBasicOpen ↑f)) → P U) →
          (∀ (i : ι), P (U i)) → P V
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.dist_eq_eLpNorm_neg_add : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] (f g : ↥(MeasureTheory.Lp E p μ)),
  dist f g = (MeasureTheory.eLpNorm (-↑↑f + ↑↑g) p μ).toReal
-- Mathlib.Algebra.GCDMonoid.Basic
lcm_dvd_mul : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : GCDMonoid α] (m n : α), lcm m n ∣ m * n
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
/-- The natural degree of `cyclotomic n` is `totient n`.  -/
Polynomial.natDegree_cyclotomic : ∀ (n : ℕ) (R : Type u_1) [inst : Ring R] [Nontrivial R], (Polynomial.cyclotomic n R).natDegree = n.totient
-- Mathlib.Combinatorics.SimpleGraph.Finsubgraph
SimpleGraph.Finsubgraph.instInfSet : {V : Type u} → {G : SimpleGraph V} → [Finite V] → InfSet G.Finsubgraph
-- Mathlib.Order.Category.Semilat
SemilatSupCat.coe_of : ∀ (α : Type u_1) [inst : SemilatticeSup α] [inst_1 : OrderBot α],
  { X := α, isSemilatticeSup := inst, isOrderBot := inst_1 }.X = α
-- Mathlib.CategoryTheory.Abelian.Images
/-- The coimage-image comparison morphism is functorial.  -/
CategoryTheory.Abelian.coimageImageComparisonFunctor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      [CategoryTheory.Limits.HasKernels C] →
        [CategoryTheory.Limits.HasCokernels C] →
          CategoryTheory.Functor (CategoryTheory.Arrow C) (CategoryTheory.Arrow C)
-- Init.Data.Option.Attach
Option.unattach_pfilter : ∀ {α : Type u_1} {p : α → Prop} {o : Option { x // p x }} {f : (a : { x // p x }) → o = some a → Bool}
  {g : (a : α) → o.unattach = some a → Bool},
  (∀ (x : α) (h : p x) (h' : o = some ⟨x, h⟩), f ⟨x, h⟩ h' = g x ⋯) → (o.pfilter f).unattach = o.unattach.pfilter g
-- Mathlib.Analysis.Convex.Exposed
IsExposed.isClosed : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : TopologicalSpace 𝕜] [inst_1 : Ring 𝕜] [inst_2 : PartialOrder 𝕜]
  [inst_3 : AddCommMonoid E] [inst_4 : TopologicalSpace E] [inst_5 : Module 𝕜 E] [OrderClosedTopology 𝕜] {A B : Set E},
  IsExposed 𝕜 A B → IsClosed A → IsClosed B
-- Mathlib.Combinatorics.Young.YoungDiagram
/-- Transposing Young diagrams is an `OrderIso`.  -/
YoungDiagram.transposeOrderIso : YoungDiagram ≃o YoungDiagram
-- Batteries.Control.LawfulMonadState
LawfulMonadStateOf.set_bind_map_set : ∀ {σ : Type u_1} {m : Type u_1 → Type u_2} [inst : Monad m] [inst_1 : MonadStateOf σ m] [LawfulMonadStateOf σ m]
  {α : Type u_1} (s s' : σ) (f : PUnit.{u_1 + 1} → α),
  (do
      set s
      f <$> set s') =
    f <$> set s'
-- Mathlib.Order.UpperLower.Hom
UpperSet.icisSupHom_apply : ∀ {α : Type u_1} [inst : CompleteLattice α] (a : α), UpperSet.icisSupHom a = UpperSet.Ici a
-- Init.Data.String.Basic
String.Pos.cast_endPos : ∀ {s t : String} {hst : s = t}, s.endPos.cast hst = t.endPos
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.EMatchTheoremKind.eqBwd : Lean.Meta.Grind.EMatchTheoremKind
-- Init.Data.Range.Polymorphic.RangeIterator
_private.Init.Data.Range.Polymorphic.RangeIterator.0.Std.Rxo.Iterator.instIteratorLoop.loop.wf.induct_unfolding : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LT α] [inst_2 : DecidableLT α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerableLT α] {n : Type u → Type w}
  [inst_5 : Monad n] (γ : Type u) (Pl : α → γ → ForInStep γ → Prop)
  (wf : Std.IteratorLoop.WellFounded (Std.Rxo.Iterator α) Id Pl) (LargeEnough : α → Prop)
  (hl : ∀ (a b : α), Std.PRange.UpwardEnumerable.LE a b → LargeEnough a → LargeEnough b) (upperBound : α)
  (f : (out : α) → LargeEnough out → out < upperBound → (c : γ) → n { s // Pl out c s })
  (motive : γ → (next : α) → LargeEnough next → n γ → Prop),
  (∀ (acc : γ) (next : α) (h : LargeEnough next) (h_1 : next < upperBound),
      (∀ (acc' : γ),
          Pl next acc (ForInStep.yield acc') →
            ∀ (next' : α) (hs : Std.PRange.succ? next = some next'),
              motive acc' next' ⋯
                (Std.Rxo.Iterator.instIteratorLoop.loop.wf✝ γ Pl wf LargeEnough hl upperBound acc' next' ⋯ f)) →
        motive acc next h do
          let __do_lift ← f next h h_1 acc
          match __do_lift with
            | ⟨ForInStep.yield acc', property⟩ =>
              match hs : Std.PRange.succ? next with
              | some next' =>
                Std.Rxo.Iterator.instIteratorLoop.loop.wf✝ γ Pl wf LargeEnough hl upperBound acc' next' ⋯ f
              | none => pure acc'
            | ⟨ForInStep.done acc', property⟩ => pure acc') →
    (∀ (acc : γ) (next : α) (h : LargeEnough next), ¬next < upperBound → motive acc next h (pure acc)) →
      ∀ (acc : γ) (next : α) (h : LargeEnough next),
        motive acc next h (Std.Rxo.Iterator.instIteratorLoop.loop.wf✝ γ Pl wf LargeEnough hl upperBound acc next h f)
-- Init.Data.Nat.Bitwise.Lemmas
Nat.exists_testBit_ne_of_ne : ∀ {x y : ℕ}, x ≠ y → ∃ i, x.testBit i ≠ y.testBit i
-- Mathlib.RingTheory.AdicCompletion.Basic
IsAdicComplete.StrictMono.extend.congr_simp : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal R} {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {N : Type u_5} [inst_3 : AddCommGroup N] [inst_4 : Module R N] {a : ℕ → ℕ} (ha : StrictMono a)
  (f f_1 : (n : ℕ) → M →ₗ[R] N ⧸ I ^ a n • ⊤),
  f = f_1 → ∀ (n : ℕ), IsAdicComplete.StrictMono.extend ha f n = IsAdicComplete.StrictMono.extend ha f_1 n
-- Mathlib.Analysis.Calculus.FDeriv.Mul
DifferentiableAt.inv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {R : Type u_5} [inst_3 : NormedDivisionRing R] [inst_4 : NormedAlgebra 𝕜 R] {h : E → R}
  {z : E}, DifferentiableAt 𝕜 h z → h z ≠ 0 → DifferentiableAt 𝕜 h⁻¹ z
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKeyD_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α],
  (↑m).WF →
    ∀ {l : List ((a : α) × β a)} {k fallback : α},
      (List.map Sigma.fst l).contains k = false → (↑(m.insertMany l)).getKeyD k fallback = m.getKeyD k fallback
-- Mathlib.Data.Finset.SDiff
Finset.union_sdiff_cancel_left : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α}, Disjoint s t → (s ∪ t) \ s = t
-- Mathlib.Analysis.PSeries
/-- Summability of the `p`-series over `ℤ`.  -/
Real.summable_one_div_int_pow : ∀ {p : ℕ}, (Summable fun n => 1 / ↑n ^ p) ↔ 1 < p
-- Mathlib.Analysis.Normed.Module.RCLike.Real
norm_smul_of_nonneg : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {t : ℝ},
  0 ≤ t → ∀ (x : E), ‖t • x‖ = t * ‖x‖
-- Plausible.Testable
/-- Format the counter-examples found in a test failure.
 -/
Plausible.Testable.formatFailure : String → List String → ℕ → String
-- Mathlib.Topology.FiberBundle.Basic
FiberBundleCore.mem_localTrivAt_baseSet : ∀ {ι : Type u_1} {B : Type u_2} {F : Type u_3} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  (Z : FiberBundleCore ι B F) (b : B), b ∈ (Z.localTrivAt b).baseSet