mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Galois.IsFundamentalgroup
_private.Mathlib.CategoryTheory.Galois.IsFundamentalgroup.0.CategoryTheory.PreGaloisCategory.isoOnObj_hom_hom_hom_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) {G : Type u_1}
  [inst_1 : Group G] [inst_2 : (X : C) → MulAction G (F.obj X).obj] (g : G) (X : C) (a : (F.obj X).obj),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.PreGaloisCategory.isoOnObj✝ F g X).hom.hom) a = g • a
-- Init.Grind.Util
Lean.Grind.matchCondUnexpander : Lean.PrettyPrinter.Unexpander
-- Lean.Meta.Tactic.Grind.AC.Seq
_private.Lean.Meta.Tactic.Grind.AC.Seq.0.Lean.Grind.AC.instReprStartsWithResult.repr : Lean.Grind.AC.StartsWithResult✝ → ℕ → Std.Format
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.mapShortComplexH2_id_comp : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A B C : Rep.{u, u, u} k G} (φ : A ⟶ B) (ψ : B ⟶ C),
  groupHomology.mapShortComplexH2 (MonoidHom.id G) (CategoryTheory.CategoryStruct.comp φ ψ) =
    CategoryTheory.CategoryStruct.comp (groupHomology.mapShortComplexH2 (MonoidHom.id G) φ)
      (groupHomology.mapShortComplexH2 (MonoidHom.id G) ψ)
-- Mathlib.Algebra.Group.Center
Set.center_prod : ∀ {M : Type u_1} [inst : Mul M] {N : Type u_2} [inst_1 : Mul N], Set.center (M × N) = Set.center M ×ˢ Set.center N
-- Mathlib.Algebra.Polynomial.Degree.Lemmas
Polynomial.nextCoeff_C_mul : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {a : R} [NoZeroDivisors R],
  (Polynomial.C a * p).nextCoeff = a * p.nextCoeff
-- Init.Data.String.Basic
String.startPos_toSlice : ∀ {s : String}, s.toSlice.startPos = s.startPos.toSlice
-- Mathlib.Topology.Order.LocalExtr
isLocalExtr_const : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder β] {a : α} {b : β},
  IsLocalExtr (fun x => b) a
-- Lean.Meta.Basic
_private.Lean.Meta.Basic.0.Lean.Meta.RealizeConstantResult.mk.sizeOf_spec : ∀ (snap? : Option Lean.Language.SnapshotTree) (error? : Option Lean.Exception),
  sizeOf { snap? := snap?, error? := error? } = 1 + sizeOf snap? + sizeOf error?
-- Std.Data.DTreeMap.Internal.WF.Defs
/-- `containsThenInsert` preserves well-formedness. Later shown to be subsumed by `.wf`.  -/
Std.DTreeMap.Internal.Impl.WF.containsThenInsert : ∀ {α : Type u} [inst : Ord α] {x : α → Type v} {t : Std.DTreeMap.Internal.Impl α x} {h : t.Balanced} {k : α} {v : x k},
  t.WF → (Std.DTreeMap.Internal.Impl.containsThenInsert k v t h).2.impl.WF
-- Init.Data.BitVec.Lemmas
BitVec.and_zero : ∀ {w : ℕ} {x : BitVec w}, x &&& 0#w = 0#w
-- Mathlib.Algebra.Homology.Embedding.TruncGE
HomologicalComplex.restrictionToTruncGE'_hasLift : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsTruncGE] [inst_3 : ∀ (i' : ι'), K.HasHomology i'],
  e.HasLift (K.restrictionToTruncGE' e)
-- Mathlib.Analysis.LocallyConvex.Bounded
Bornology.IsVonNBounded.of_subsingleton : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E] [inst_2 : Zero E]
  [inst_3 : TopologicalSpace E] [Subsingleton E] {s : Set E}, Bornology.IsVonNBounded 𝕜 s
-- Mathlib.Data.TwoPointing
/-- Swaps the two pointed elements.  -/
TwoPointing.swap : {α : Type u_1} → TwoPointing α → TwoPointing α
-- Batteries.Data.MLList.Basic
_private.Batteries.Data.MLList.Basic.0.MLList.instInhabitedForallForallForallForallForInStepOfMonad : {n : Type u_1 → Type u_2} →
  {δ : Type u_1} → {α : Sort u_3} → [Monad n] → Inhabited (δ → (α → δ → n (ForInStep δ)) → n δ)
-- Mathlib.MeasureTheory.Measure.Regular
MeasureTheory.Measure.Regular.mk : ∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] {μ : MeasureTheory.Measure α}
  [toIsFiniteMeasureOnCompacts : MeasureTheory.IsFiniteMeasureOnCompacts μ] [toOuterRegular : μ.OuterRegular],
  μ.InnerRegularWRT IsCompact IsOpen → μ.Regular
-- Mathlib.Topology.Instances.AddCircle.Defs
AddCircle.liftIoc_eq_liftIco_of_ne : ∀ {𝕜 : Type u_1} {B : Type u_2} [inst : AddCommGroup 𝕜] {p : 𝕜} [inst_1 : LinearOrder 𝕜] [inst_2 : IsOrderedAddMonoid 𝕜]
  [hp : Fact (0 < p)] {a : 𝕜} [inst_3 : Archimedean 𝕜] {f : 𝕜 → B} {x : AddCircle p},
  x ≠ ↑a → AddCircle.liftIoc p a f x = AddCircle.liftIco p a f x
-- Mathlib.MeasureTheory.Integral.Prod
/-- The Bochner integral is measurable. This shows that the integrand of (the right-hand-side of)
Fubini's theorem is measurable.  -/
MeasureTheory.StronglyMeasurable.integral_prod_right' : ∀ {α : Type u_1} {β : Type u_2} {E : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  {ν : MeasureTheory.Measure β} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace ℝ E] [MeasureTheory.SFinite ν]
  ⦃f : α × β → E⦄, MeasureTheory.StronglyMeasurable f → MeasureTheory.StronglyMeasurable fun x => ∫ (y : β), f (x, y) ∂ν
-- Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Real.volume_pi_Ico : ∀ {ι : Type u_1} [inst : Fintype ι] {a b : ι → ℝ},
  MeasureTheory.volume (Set.univ.pi fun i => Set.Ico (a i) (b i)) = ∏ i, ENNReal.ofReal (b i - a i)
-- Mathlib.Algebra.Module.Presentation.Cokernel
Module.Presentation.ofExact_G : ∀ {A : Type u} [inst : Ring A] {M₁ : Type v₁} {M₂ : Type v₂} {M₃ : Type v₃} [inst_1 : AddCommGroup M₁]
  [inst_2 : Module A M₁] [inst_3 : AddCommGroup M₂] [inst_4 : Module A M₂] [inst_5 : AddCommGroup M₃]
  [inst_6 : Module A M₃] {f : M₁ →ₗ[A] M₂} {g : M₂ →ₗ[A] M₃} (pres₂ : Module.Presentation A M₂) {ι : Type w₁}
  {g₁ : ι → M₁} (data : pres₂.CokernelData f g₁) (hfg : Function.Exact ⇑f ⇑g) (hg : Function.Surjective ⇑g)
  (hg₁ : Submodule.span A (Set.range g₁) = ⊤), (pres₂.ofExact data hfg hg hg₁).G = pres₂.G
-- Mathlib.CategoryTheory.Abelian.Basic
CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.imageMonoFactorisation_e : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasKernels C] [inst_3 : CategoryTheory.Limits.HasCokernels C] {X Y : C} (f : X ⟶ Y),
  (CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.imageMonoFactorisation f).e =
    CategoryTheory.Limits.kernel.lift (CategoryTheory.Limits.cokernel.π f) f ⋯
-- Lean.Attributes
Lean.AttributeImplCore.applicationTime : Lean.AttributeImplCore → Lean.AttributeApplicationTime
-- Init.Data.UInt.Lemmas
UInt32.ofNatLT_toNat : ∀ (n : UInt32), UInt32.ofNatLT n.toNat ⋯ = n
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.denoteAsIntModule.eq_1 : ∀ {α : Type u_1} [inst : Lean.Grind.CommRing α] (ctx : Lean.Grind.CommRing.Context α),
  Lean.Grind.CommRing.Mon.denoteAsIntModule ctx Lean.Grind.CommRing.Mon.unit = One.one
-- Mathlib.Analysis.Complex.Exponential
/-- the exponential function as a monoid hom from `Multiplicative ℂ` to `ℂ`  -/
Complex.expMonoidHom : Multiplicative ℂ →* ℂ
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenSubgroup.instPartialOrderOpenSubgroup.eq_1 : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G],
  OpenSubgroup.instPartialOrderOpenSubgroup = inferInstance
-- Mathlib.RingTheory.Kaehler.JacobiZariski
Algebra.Generators.ker.eq_1 : ∀ {R : Type u} {S : Type v} {ι : Type w} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.Generators R S ι), P.ker = P.toExtension.ker
-- Mathlib.Topology.OpenPartialHomeomorph.Defs
OpenPartialHomeomorph.surjOn : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y), Set.SurjOn (↑e) e.source e.target
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.isRflProof : Lean.Expr → Lean.MetaM Bool
-- Mathlib.Topology.PartitionOfUnity
PartitionOfUnity.sum_eq_one : ∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] {s : Set X} (f : PartitionOfUnity ι X s) {x : X},
  x ∈ s → ∑ᶠ (i : ι), (f i) x = 1
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
Real.hasDerivAt_arctan' : ∀ (x : ℝ), HasDerivAt Real.arctan (1 + x ^ 2)⁻¹ x
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.toType_apply : ∀ (x : SimplexCategory), CategoryTheory.ToType x = Fin (x.len + 1)
-- Mathlib.Data.Finite.Defs
instInfiniteULift : ∀ {α : Type v} [Infinite α], Infinite (ULift.{u, v} α)
-- Mathlib.Algebra.BigOperators.Fin
Fin.prod_Ioc_castAdd : ∀ {M : Type u_2} [inst : CommMonoid M] {n : ℕ} (m : ℕ) (f : Fin (n + m) → M) (a b : Fin n),
  ∏ i ∈ Finset.Ioc (Fin.castAdd m a) (Fin.castAdd m b), f i = ∏ i ∈ Finset.Ioc a b, f (Fin.castAdd m i)
-- Mathlib.Algebra.Group.Center
Set.sub_mem_addCentralizer : ∀ {M : Type u_1} {S : Set M} [inst : AddGroup M] {a b : M},
  a ∈ S.addCentralizer → b ∈ S.addCentralizer → a - b ∈ S.addCentralizer
-- Batteries.Data.Char.Basic
Char.ofNat_toNat_eq_val : ∀ {c : Char}, UInt32.ofNat c.toNat = c.val
-- Mathlib.Algebra.MvPolynomial.Nilpotent
MvPolynomial.isUnit_iff_totalDegree_of_isReduced : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommRing R] {P : MvPolynomial σ R} [IsReduced R],
  IsUnit P ↔ IsUnit (MvPolynomial.coeff 0 P) ∧ P.totalDegree = 0
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.addX_smul : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} (P Q : Fin 3 → R) (u v : R),
  W'.addX (u • P) (v • Q) = ((u * v) ^ 2) ^ 2 * W'.addX P Q
-- Mathlib.Analysis.Real.Pi.Irrational
/-- Auxiliary for the proof that `π` is irrational.
The second of the two integer-coefficient polynomials that describe the behaviour of the
sequence of integrals `I`.
While not given in the informal proof, these are easy to deduce from the recursion formulae.
 -/
_private.Mathlib.Analysis.Real.Pi.Irrational.0.cosPoly : ℕ → Polynomial ℤ
-- Mathlib.LinearAlgebra.SymmetricAlgebra.Basis
/-- `SymmetricAlgebra.equivMvPolynomial` gives an algebra isomorphism between the symmetric algebra
over a free module and multivariate polynomials over a basis. This is analogous to
`TensorAlgebra.equivFreeAlgebra`.  -/
SymmetricAlgebra.equivMvPolynomial : {κ : Type uκ} →
  {R : Type uR} →
    {M : Type uM} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] → Module.Basis κ R M → SymmetricAlgebra R M ≃ₐ[R] MvPolynomial κ R
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.algebraMap_eq' : ∀ {R : Type u_1} (S : Type u_2) [inst : CommRing R] (f : Polynomial R) [inst_1 : CommSemiring S] [inst_2 : Algebra S R],
  algebraMap S (AdjoinRoot f) = (AdjoinRoot.of f).comp (algebraMap S R)
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.quotMapOfEquivQuotMapCMapMk_symm_mk : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) (f : Polynomial R) (x : AdjoinRoot f),
  (AdjoinRoot.quotMapOfEquivQuotMapCMapMk I f).symm
      ((Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk (Ideal.span {f})) (Ideal.map Polynomial.C I))) x) =
    (Ideal.Quotient.mk (Ideal.map (AdjoinRoot.of f) I)) x
-- Mathlib.RingTheory.Ideal.Maps
Ideal.mem_image_of_mem_map_of_surjective : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : FunLike F R S] (f : F)
  [RingHomClass F R S], Function.Surjective ⇑f → ∀ {I : Ideal R} {y : S}, y ∈ Ideal.map f I → y ∈ ⇑f '' ↑I
-- Mathlib.CategoryTheory.Monoidal.Mon
/-- Natural isomorphisms between functors lift to monoid objects.  -/
CategoryTheory.Functor.mapMonNatIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            {F F' : CategoryTheory.Functor C D} →
              [inst_4 : F.LaxMonoidal] →
                [inst_5 : F'.LaxMonoidal] →
                  (e : F ≅ F') → [CategoryTheory.NatTrans.IsMonoidal e.hom] → F.mapMon ≅ F'.mapMon
-- Aesop.Script.UScriptToSScript
Aesop.Script.StepTree.node : Aesop.Script.Step → ℕ → Array Aesop.Script.StepTree → Aesop.Script.StepTree
-- Mathlib.SetTheory.Ordinal.Topology
Ordinal.instTopologicalSpace : TopologicalSpace Ordinal.{u}
-- Mathlib.Algebra.Order.Field.Basic
/-- **Alias** of `half_lt_self`.

---

**Alias** of the reverse direction of `half_lt_self_iff`. -/
div_two_lt_of_pos : ∀ {α : Type u_2} [inst : Semifield α] [inst_1 : PartialOrder α] [PosMulReflectLT α] {a : α} [IsStrictOrderedRing α],
  0 < a → a / 2 < a
-- Mathlib.RingTheory.FreeCommRing
/-- The restriction map from `FreeCommRing α` to `FreeCommRing s` where `s : Set α`, defined
by sending all variables not in `s` to zero.  -/
FreeCommRing.restriction : {α : Type u} → (s : Set α) → [DecidablePred fun x => x ∈ s] → FreeCommRing α →+* FreeCommRing ↑s
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Arrow.inv_hom_id_left : ∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] {f g : CategoryTheory.Arrow T} (e : f ≅ g),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.left e.inv) (CategoryTheory.Arrow.Hom.left e.hom) =
    CategoryTheory.CategoryStruct.id g.left
-- Mathlib.CategoryTheory.Sites.Continuous
CategoryTheory.Functor.sheafPushforwardContinuousId'_hom_app_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {F'' : CategoryTheory.Functor C C}
  (eF'' : F'' ≅ CategoryTheory.Functor.id C) (A : Type u) [inst_1 : CategoryTheory.Category.{t, u} A]
  (J : CategoryTheory.GrothendieckTopology C) [inst_2 : F''.IsContinuous J J] (X : CategoryTheory.Sheaf J A)
  (X_1 : Cᵒᵖ),
  ((CategoryTheory.Functor.sheafPushforwardContinuousId' eF'' A J).hom.app X).hom.app X_1 =
    X.obj.map (eF''.inv.app (Opposite.unop X_1)).op
-- Mathlib.Analysis.Analytic.ConvergenceRadius
_private.Mathlib.Analysis.Analytic.ConvergenceRadius.0.constFormalMultilinearSeries.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → ((x : ℕ) → (x = 0 → False) → motive x) → motive x
-- Mathlib.Order.Hom.Lattice
SupHom.toFun_eq_coe : ∀ {α : Type u_2} {β : Type u_3} [inst : Max α] [inst_1 : Max β] (f : SupHom α β), f.toFun = ⇑f
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceInverse_obj_base : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C CategoryTheory.Cat)
  (X : CategoryTheory.Grothendieck F),
  ((CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceInverse F).obj X).base = X.base
-- Mathlib.AlgebraicGeometry.Birational.Composition
AlgebraicGeometry.Scheme.PartialMap.comp.congr_simp : ∀ {X Y Z : AlgebraicGeometry.Scheme} [inst : PreirreducibleSpace ↥X] [inst_1 : Nonempty ↥Y] (f f_1 : X.PartialMap Y)
  (e_f : f = f_1) [inst_2 : AlgebraicGeometry.IsDominant f.hom] (g g_1 : Y.PartialMap Z),
  g = g_1 → f.comp g = f_1.comp g_1
-- Init.Data.Float.Model.Unpacked.Sign
/-- Apply the given sign to the given integer.
 -/
Float.Model.UnpackedFloat.Sign.apply : Float.Model.UnpackedFloat.Sign → ℤ → ℤ
-- Mathlib.NumberTheory.PythagoreanTriples
PythagoreanTriple.symm : ∀ {x y z : ℤ}, PythagoreanTriple x y z → PythagoreanTriple y x z
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
/-- This returns the multiset of irreducible factors as a `FactorSet`,
a multiset of irreducible associates `WithTop`.  -/
Associates.factors' : {α : Type u_1} → [inst : CommMonoidWithZero α] → [UniqueFactorizationMonoid α] → α → Multiset { a // Irreducible a }
-- Mathlib.Algebra.Polynomial.Div
/-- `divByMonic`, denoted as `p /ₘ q`, gives the quotient of `p` by a monic polynomial `q`.  -/
Polynomial.«term_/ₘ_» : Lean.TrailingParserDescr
-- Mathlib.Algebra.Free
FreeAddMagma.lift_comp_of : ∀ {α : Type u} {β : Type v} [inst : Add β] (f : α → β), ⇑(FreeAddMagma.lift f) ∘ FreeAddMagma.of = f
-- Mathlib.MeasureTheory.Group.Prod
/-- The shear mapping `(x, y) ↦ (x, x + y)` preserves the measure `μ × ν`.  -/
MeasureTheory.measurePreserving_prod_add : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [MeasurableAdd₂ G] (μ ν : MeasureTheory.Measure G)
  [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] [ν.IsAddLeftInvariant],
  MeasureTheory.MeasurePreserving (fun z => (z.1, z.1 + z.2)) (μ.prod ν) (μ.prod ν)
-- Init.Data.Array.Find
Array.findIdx?_eq_none_of_findIdx?_eq_none : ∀ {α : Type u_1} {xs : Array α} {p q : α → Bool},
  (∀ x ∈ xs, p x = true → q x = true) → Array.findIdx? q xs = none → Array.findIdx? p xs = none
-- Lean.Widget.TaggedText
_private.Lean.Widget.TaggedText.0.Lean.Widget.TaggedText.TaggedState.mk.injEq : ∀ (out : Lean.Widget.TaggedText (ℕ × ℕ)) (tagStack : List (ℕ × ℕ × Lean.Widget.TaggedText (ℕ × ℕ))) (column : ℕ)
  (out_1 : Lean.Widget.TaggedText (ℕ × ℕ)) (tagStack_1 : List (ℕ × ℕ × Lean.Widget.TaggedText (ℕ × ℕ))) (column_1 : ℕ),
  ({ out := out, tagStack := tagStack, column := column } =
      { out := out_1, tagStack := tagStack_1, column := column_1 }) =
    (out = out_1 ∧ tagStack = tagStack_1 ∧ column = column_1)
-- Mathlib.RingTheory.RootsOfUnity.Complex
/-- The complex `n`-th roots of unity are exactly the
complex numbers of the form `exp (2 * Real.pi * Complex.I * (i / n))` for some `i < n`.  -/
Complex.mem_rootsOfUnity : ∀ (n : ℕ) [NeZero n] (x : ℂˣ), x ∈ rootsOfUnity n ℂ ↔ ∃ i < n, Complex.exp (2 * ↑Real.pi * Complex.I * (↑i / ↑n)) = ↑x
-- Mathlib.CategoryTheory.Monoidal.Action.Opposites
CategoryTheory.MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionAssocIso : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] (x : D) (x_1 x_2 : Cᴹᵒᵖ),
  CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso x x_1 x_2 =
    CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso x_2.unmop x_1.unmop x
-- Mathlib.Algebra.MonoidAlgebra.Defs
/-- The monoid algebra over a semiring `R` generated by the monoid `M`.

It is the type of finite formal `R`-linear combinations of terms of `M`,
endowed with the convolution product.  -/
MonoidAlgebra : (R : Type u_8) → Type u_9 → [Semiring R] → Type (max u_8 u_9)
-- Mathlib.NumberTheory.ModularForms.Basic
/-- Given `ModularForm`'s `F i` of weight `k`, define the form which as a function is a product of
those indexed by `s : Finset ι` with weight `#s * k`.  -/
ModularForm.prodEqualWeights : {ι : Type} →
  {s : Finset ι} →
    {k : ℤ} →
      {Γ : Subgroup (GL (Fin 2) ℝ)} → [Γ.HasDetPlusMinusOne] → (ι → ModularForm Γ k) → ModularForm Γ (↑s.card * k)
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instInv.eq_1 : ∀ {α : Type u_1} [inst : Inv α], Colex.instInv = inst
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
WeierstrassCurve.Projective.Point.toAffineLift_add : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} [inst_1 : DecidableEq F] (P Q : W.Point),
  (P + Q).toAffineLift = P.toAffineLift + Q.toAffineLift
-- Mathlib.RingTheory.FormalGroup.Basic
FormalGroup.mk.injEq : ∀ {R : Type u_1} [inst : CommRing R] (toPowerSeries : MvPowerSeries (Fin 2) R)
  (zero_constantCoeff : MvPowerSeries.constantCoeff toPowerSeries = 0)
  (lin_coeff_X : (MvPowerSeries.coeff fun₀ | 0 => 1) toPowerSeries = 1)
  (lin_coeff_Y : (MvPowerSeries.coeff fun₀ | 1 => 1) toPowerSeries = 1)
  (assoc :
    MvPowerSeries.subst ![MvPowerSeries.subst ![MvPowerSeries.X 0, MvPowerSeries.X 1] toPowerSeries, MvPowerSeries.X 2]
        toPowerSeries =
      MvPowerSeries.subst
        ![MvPowerSeries.X 0, MvPowerSeries.subst ![MvPowerSeries.X 1, MvPowerSeries.X 2] toPowerSeries] toPowerSeries)
  (toPowerSeries_1 : MvPowerSeries (Fin 2) R) (zero_constantCoeff_1 : MvPowerSeries.constantCoeff toPowerSeries_1 = 0)
  (lin_coeff_X_1 : (MvPowerSeries.coeff fun₀ | 0 => 1) toPowerSeries_1 = 1)
  (lin_coeff_Y_1 : (MvPowerSeries.coeff fun₀ | 1 => 1) toPowerSeries_1 = 1)
  (assoc_1 :
    MvPowerSeries.subst
        ![MvPowerSeries.subst ![MvPowerSeries.X 0, MvPowerSeries.X 1] toPowerSeries_1, MvPowerSeries.X 2]
        toPowerSeries_1 =
      MvPowerSeries.subst
        ![MvPowerSeries.X 0, MvPowerSeries.subst ![MvPowerSeries.X 1, MvPowerSeries.X 2] toPowerSeries_1]
        toPowerSeries_1),
  ({ toPowerSeries := toPowerSeries, zero_constantCoeff := zero_constantCoeff, lin_coeff_X := lin_coeff_X,
        lin_coeff_Y := lin_coeff_Y, assoc := assoc } =
      { toPowerSeries := toPowerSeries_1, zero_constantCoeff := zero_constantCoeff_1, lin_coeff_X := lin_coeff_X_1,
        lin_coeff_Y := lin_coeff_Y_1, assoc := assoc_1 }) =
    (toPowerSeries = toPowerSeries_1)
-- Mathlib.Order.SuccPred.Limit
Order.IsPredPrelimit.pred_le_iff : ∀ {α : Type u_1} {a b : α} [inst : LinearOrder α] [inst_1 : PredOrder α],
  Order.IsPredPrelimit b → (Order.pred a ≤ b ↔ a ≤ b)
-- Mathlib.Order.Basic
Prod.mk_lt_mk_iff_right : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {a : α} {b₁ b₂ : β},
  (a, b₁) < (a, b₂) ↔ b₁ < b₂
-- Mathlib.Topology.Separation.Hausdorff
/-- A T₂ space, also known as a Hausdorff space, is one in which for every
`x ≠ y` there exists disjoint open sets around `x` and `y`. This is
the most widely used of the separation axioms.  -/
T2Space : (X : Type u) → [TopologicalSpace X] → Prop
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor
AlgebraicGeometry.Proj.mapAffineOpenCover_f : ∀ {A B σ τ : Type u} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] [inst_3 : CommRing B]
  [inst_4 : SetLike τ B] [inst_5 : AddSubgroupClass τ B] {𝒜 : ℕ → σ} {ℬ : ℕ → τ} [inst_6 : GradedRing 𝒜]
  [inst_7 : GradedRing ℬ] (f : 𝒜 →+*ᵍ ℬ)
  (hf : HomogeneousIdeal.irrelevant ℬ ≤ HomogeneousIdeal.map f (HomogeneousIdeal.irrelevant 𝒜))
  (i : (AlgebraicGeometry.Proj.affineOpenCover 𝒜).I₀),
  (AlgebraicGeometry.Proj.mapAffineOpenCover f hf).f i = AlgebraicGeometry.Proj.awayι ℬ (f ↑i.snd) ⋯ ⋯
-- Mathlib.Algebra.Colimit.Module
Module.DirectLimit.hom_ext : ∀ {R : Type u_1} [inst : Semiring R] {ι : Type u_2} [inst_1 : Preorder ι] {G : ι → Type u_3}
  [inst_2 : (i : ι) → AddCommMonoid (G i)] [inst_3 : (i : ι) → Module R (G i)] {f : (i j : ι) → i ≤ j → G i →ₗ[R] G j}
  [inst_4 : DecidableEq ι] {P : Type u_4} [inst_5 : AddCommMonoid P] [inst_6 : Module R P]
  {g₁ g₂ : Module.DirectLimit G f →ₗ[R] P},
  (∀ (i : ι), g₁ ∘ₗ Module.DirectLimit.of R ι G f i = g₂ ∘ₗ Module.DirectLimit.of R ι G f i) → g₁ = g₂
-- Mathlib.GroupTheory.GroupAction.FixedPoints
/-- `MulActionHom` maps `fixedPoints` to `fixedPoints`.  -/
MulActionHom.map_mem_fixedPoints : ∀ {G : Type u_1} {A : Type u_2} {B : Type u_3} [inst : Monoid G] [inst_1 : MulAction G A] [inst_2 : MulAction G B]
  (f : A →ₑ[id] B) {H : Submonoid G} {a : A}, a ∈ MulAction.fixedPoints (↥H) A → f a ∈ MulAction.fixedPoints (↥H) B
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.instNonAssocSemiringOfMulOpposite : {M : Type u_1} → [NonAssocSemiring Mᵐᵒᵖ] → NonAssocSemiring Mᵈᵐᵃ
-- Mathlib.Analysis.CStarAlgebra.GelfandDuality
IsSelfAdjoint.nnnorm_sub_eq_max : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] {a b : A},
  IsSelfAdjoint a → IsSelfAdjoint b → a * b = 0 → ‖a - b‖₊ = max ‖a‖₊ ‖b‖₊
-- Mathlib.RingTheory.Kaehler.Basic
/-- (Implementation) The underlying linear map of the derivation into `Ω[S⁄R]`.  -/
KaehlerDifferential.DLinearMap : (R : Type u) → (S : Type v) → [inst : CommRing R] → [inst_1 : CommRing S] → [inst_2 : Algebra R S] → S →ₗ[R] Ω[S⁄R]
-- Init.Data.Int.DivMod.Lemmas
Int.bmod_sub_cancel_left : ∀ {x : ℤ} {n : ℕ} {y : ℤ} (i : ℤ), (i - x).bmod n = (i - y).bmod n ↔ x.bmod n = y.bmod n
-- Mathlib.Geometry.Manifold.VectorBundle.Basic
Bundle.contMDiffWithinAt_section_of_subsingleton : ∀ {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} (E : B → Type u_6) [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F] [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_4 : (x : B) → TopologicalSpace (E x)] {EB : Type u_7} [inst_5 : NormedAddCommGroup EB]
  [inst_6 : NormedSpace 𝕜 EB] {HB : Type u_8} [inst_7 : TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB}
  [inst_8 : TopologicalSpace B] [inst_9 : ChartedSpace HB B] [inst_10 : FiberBundle F E] {s : (x : B) → E x} {u : Set B}
  {x : B} [Subsingleton F], ContMDiffWithinAt IB (IB.prod (modelWithCornersSelf 𝕜 F)) n (fun x => ⟨x, s x⟩) u x