mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.balanceL!.match_5.congr_eq_2 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → Sort u_3)
  (l : Std.DTreeMap.Internal.Impl α β) (h_1 : Unit → motive Std.DTreeMap.Internal.Impl.leaf)
  (h_2 :
    (ls : ℕ) →
      (lk : α) →
        (lv : β lk) →
          (ll lr : Std.DTreeMap.Internal.Impl α β) → motive (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr))
  (ls : ℕ) (lk : α) (lv : β lk) (ll lr : Std.DTreeMap.Internal.Impl α β),
  l = Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr →
    (match l with
      | Std.DTreeMap.Internal.Impl.leaf => h_1 ()
      | Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr => h_2 ls lk lv ll lr) ≍
      h_2 ls lk lv ll lr
-- Mathlib.CategoryTheory.EssentiallySmall
CategoryTheory.smallCategorySmallModel : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.EssentiallySmall.{w, v, u} C] →
      CategoryTheory.SmallCategory (CategoryTheory.SmallModel.{w, v, u} C)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.dblXYZ_smul : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} (P : Fin 3 → R) (u : R),
  W'.dblXYZ (u • P) = u ^ 4 • W'.dblXYZ P
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
/-- **Triangle Removal Lemma**. If not all triangles can be removed by removing few edges (on the
order of `(card α)^2`), then there were many triangles to start with (on the order of
`(card α)^3`).  -/
SimpleGraph.FarFromTriangleFree.le_card_cliqueFinset : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {G : SimpleGraph α} [inst_2 : DecidableRel G.Adj] {ε : ℝ},
  G.FarFromTriangleFree ε → SimpleGraph.triangleRemovalBound ε * ↑(Fintype.card α) ^ 3 ≤ ↑(G.cliqueFinset 3).card
-- Lean.Meta.LazyDiscrTree
/-- This drops a specific key from the lazy discrimination tree so that
all the entries matching that key exactly are removed.
 -/
Lean.Meta.LazyDiscrTree.dropKey : {α : Type} → Lean.Meta.LazyDiscrTree α → List Lean.Meta.LazyDiscrTree.Key → Lean.MetaM (Lean.Meta.LazyDiscrTree α)
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
MeasurableSet.cond : ∀ {α : Type u_1} {m : MeasurableSpace α} {s₁ s₂ : Set α},
  MeasurableSet s₁ → MeasurableSet s₂ → ∀ {i : Bool}, MeasurableSet (bif i then s₁ else s₂)
-- Mathlib.Order.Category.BddLat
BddLat.hom_ext : ∀ {X Y : BddLat} {f g : X ⟶ Y}, BddLat.Hom.hom f = BddLat.Hom.hom g → f = g
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
/-- The `eqToHom` given by `ιInvApp_π`.  -/
AlgebraicGeometry.PresheafedSpace.GlueData.ιInvAppπEqMap : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (D : AlgebraicGeometry.PresheafedSpace.GlueData C) →
      [inst_1 : CategoryTheory.Limits.HasLimits C] →
        {i : D.J} →
          (U : TopologicalSpace.Opens ↑↑(D.U i)) →
            (D.U i).presheaf.obj
                (Opposite.op
                  ((TopologicalSpace.Opens.map
                        (CategoryTheory.Limits.colimit.ι D.diagram.multispan
                            (Opposite.unop (Opposite.op (CategoryTheory.Limits.WalkingMultispan.right i)))).base).obj
                    (⋯.functor.obj U))) ⟶
              (D.U i).presheaf.obj (Opposite.op U)
-- Mathlib.Data.Finset.PImage
Finset.mem_pimage : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] {f : α →. β} [inst_1 : (x : α) → Decidable (f x).Dom]
  {s : Finset α} {b : β}, b ∈ Finset.pimage f s ↔ ∃ a ∈ s, b ∈ f a
-- Mathlib.Topology.FiberBundle.Constructions
/-- The product of two fiber bundles is a fiber bundle.  -/
FiberBundle.prod : {B : Type u_1} →
  [inst : TopologicalSpace B] →
    (F₁ : Type u_2) →
      [inst_1 : TopologicalSpace F₁] →
        (E₁ : B → Type u_3) →
          [inst_2 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] →
            (F₂ : Type u_4) →
              [inst_3 : TopologicalSpace F₂] →
                (E₂ : B → Type u_5) →
                  [inst_4 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)] →
                    [(x : B) → Zero (E₁ x)] →
                      [(x : B) → Zero (E₂ x)] →
                        [inst_7 : (x : B) → TopologicalSpace (E₁ x)] →
                          [inst_8 : (x : B) → TopologicalSpace (E₂ x)] →
                            [FiberBundle F₁ E₁] → [FiberBundle F₂ E₂] → FiberBundle (F₁ × F₂) fun x => E₁ x × E₂ x
-- Mathlib.CategoryTheory.Monoidal.Preadditive
CategoryTheory.leftDistributor.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalPreadditive C]
  [inst_4 : CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [inst_5 : Finite J] (X : C) (f : J → C),
  CategoryTheory.leftDistributor X f = CategoryTheory.leftDistributor X f
-- Mathlib.FieldTheory.Extension
IntermediateField.inclusion.eq_1 : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {E F : IntermediateField K L}
  (hEF : E ≤ F), IntermediateField.inclusion hEF = Subalgebra.inclusion hEF
-- Std.Data.DTreeMap.Raw.Lemmas
/-- Simpler variant of `get?_filterMap` when `LawfulEqCmp` is available.  -/
Std.DTreeMap.Raw.Const.get?_filterMap' : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.DTreeMap.Raw α (fun x => β) cmp}
  [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] {f : α → β → Option γ} {k : α},
  t.WF → Std.DTreeMap.Raw.Const.get? (Std.DTreeMap.Raw.filterMap f t) k = (Std.DTreeMap.Raw.Const.get? t k).bind (f k)
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.sum_excenterWeightsUnnorm_singleton_pos : ∀ {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)), 0 < ∑ j, s.excenterWeightsUnnorm {i} j
-- Lean.Parser.Term.Basic
Lean.Parser.Term.typeSpec.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.GroupTheory.PushoutI
/-- The equivalence between normal forms and elements of the pushout  -/
Monoid.PushoutI.NormalWord.equiv : {ι : Type u_1} →
  {G : ι → Type u_2} →
    {H : Type u_3} →
      [inst : (i : ι) → Group (G i)] →
        [inst_1 : Group H] →
          {φ : (i : ι) → H →* G i} →
            {d : Monoid.PushoutI.NormalWord.Transversal φ} →
              [DecidableEq ι] → [(i : ι) → DecidableEq (G i)] → Monoid.PushoutI φ ≃ Monoid.PushoutI.NormalWord d
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.String.Legacy.revFindAux.eq_def : ∀ (s : String) (p : Char → Bool) (pos : String.Pos.Raw),
  String.Legacy.revFindAux s p pos =
    if h : pos = 0 then none
    else
      have this := ⋯;
      have pos := String.Pos.Raw.prev s pos;
      if p (String.Pos.Raw.get s pos) = true then some pos else String.Legacy.revFindAux s p pos
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Under.w_assoc : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {P Q : CategoryTheory.MorphismProperty T} {X : T}
  [inst_1 : Q.IsMultiplicative] {A B : P.Under Q X} (f : A ⟶ B) {Z : T} (h : B.right ⟶ Z),
  CategoryTheory.CategoryStruct.comp A.hom (CategoryTheory.CategoryStruct.comp f.right h) =
    CategoryTheory.CategoryStruct.comp B.hom h
-- Mathlib.Data.List.Cycle
Cycle.instDecidableNontrivial : {α : Type u_1} → [DecidableEq α] → {s : Cycle α} → Decidable s.Nontrivial
-- Mathlib.CategoryTheory.Idempotents.Basic
/-- A category is idempotent complete iff all idempotent endomorphisms `p`
split as a composition `p = e ≫ i` with `i ≫ e = 𝟙 _`  -/
CategoryTheory.IsIdempotentComplete.idempotents_split : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} [self : CategoryTheory.IsIdempotentComplete C] (X : C)
  (p : X ⟶ X),
  CategoryTheory.CategoryStruct.comp p p = p →
    ∃ Y i e,
      CategoryTheory.CategoryStruct.comp i e = CategoryTheory.CategoryStruct.id Y ∧
        CategoryTheory.CategoryStruct.comp e i = p
-- Lean.Meta.Basic
/-- `withoutModifyingMCtx k` executes `k` and then restores the metavariable context.
 -/
Lean.Meta.withoutModifyingMCtx : {n : Type → Type u_1} → [MonadControlT Lean.MetaM n] → [Monad n] → {α : Type} → n α → n α
-- Mathlib.CategoryTheory.Linear.Basic
/-- Composition by a fixed right argument as an `R`-linear map.  -/
CategoryTheory.Linear.rightComp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      (R : Type w) →
        [inst_2 : Semiring R] →
          [inst_3 : CategoryTheory.Linear R C] → (X : C) → {Y Z : C} → (Y ⟶ Z) → (X ⟶ Y) →ₗ[R] X ⟶ Z
-- Mathlib.Algebra.Order.Ring.Synonym
OrderDual.instCommSemiring : {R : Type u_1} → [CommSemiring R] → CommSemiring Rᵒᵈ
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.isEmpty_filter_key_iff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {f : α → Bool},
  (Std.DTreeMap.filter (fun a x => f a) t).isEmpty = true ↔ ∀ (k : α) (h : k ∈ t), f (t.getKey k h) = false
-- Init.Data.Float.Float32
/-- Obtains a `Float32` whose value is near the given `UInt64`.

It will be exactly the value of the given `UInt64` if such a `Float32` exists. If no such `Float32`
exists, the returned value will either be the smallest `Float32` that is larger than the given
value, or the largest `Float32` that is smaller than the given value.

This function has a logical model in terms of `Float32.Model`, but is overridden at runtime with an
efficient implementation.
 -/
UInt64.toFloat32 : UInt64 → Float32
-- Mathlib.Analysis.Seminorm
Seminorm.continuousAt_zero : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : NontriviallyNormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [ContinuousConstSMul 𝕜 E] {p : Seminorm 𝕜 E} {r : ℝ},
  p.ball 0 r ∈ nhds 0 → ContinuousAt (⇑p) 0
-- Std.Http.Transport
/-- Gets the send channel for a server (server to client direction).
 -/
Std.Http.Internal.Mock.Server.getSendChan : Std.Http.Internal.Mock.Server → Std.CloseableChannel ByteArray
-- Mathlib.LinearAlgebra.Matrix.ToLin
LinearMap.toMatrix_symm : ∀ {R : Type u_1} [inst : CommSemiring R] {m : Type u_3} {n : Type u_4} [inst_1 : Fintype n] [inst_2 : Finite m]
  [inst_3 : DecidableEq n] {M₁ : Type u_5} {M₂ : Type u_6} [inst_4 : AddCommMonoid M₁] [inst_5 : AddCommMonoid M₂]
  [inst_6 : Module R M₁] [inst_7 : Module R M₂] (v₁ : Module.Basis n R M₁) (v₂ : Module.Basis m R M₂),
  (LinearMap.toMatrix v₁ v₂).symm = Matrix.toLin v₁ v₂
-- Mathlib.Data.Fin.Tuple.Basic
Fin.removeNth.eq_1 : ∀ {n : ℕ} {α : Fin (n + 1) → Sort u_1} (p : Fin (n + 1)) (f : (i : Fin (n + 1)) → α i) (i : Fin n),
  p.removeNth f i = f (p.succAbove i)
-- Mathlib.Data.Finsupp.Basic
Finsupp.comapDomain.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : Zero M] (f : α → β) (l : β →₀ M)
  (hf : Set.InjOn f (f ⁻¹' ↑l.support)),
  Finsupp.comapDomain f l hf = { support := l.support.preimage f hf, toFun := fun a => l (f a), mem_support_toFun := ⋯ }
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.getD_inter : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α],
  m₁.WF → m₂.WF → ∀ {k fallback : α}, (m₁ ∩ m₂).getD k fallback = if k ∈ m₂ then m₁.getD k fallback else fallback
-- Mathlib.Probability.ProbabilityMassFunction.Constructions
PMF.monad_map_eq_map : ∀ {α β : Type u} (f : α → β) (p : PMF α), f <$> p = PMF.map f p
-- Mathlib.RingTheory.MvPolynomial.Homogeneous
/-- The submodule of homogeneous `MvPolynomial`s of degree `n`.  -/
MvPolynomial.homogeneousSubmodule : (σ : Type u_1) → (R : Type u_3) → [inst : CommSemiring R] → ℕ → Submodule R (MvPolynomial σ R)
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.smulLeftCLM_add : ∀ {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NontriviallyNormedField 𝕜]
  [inst_5 : NormedAlgebra ℝ 𝕜] [inst_6 : NormedSpace 𝕜 F] {g₁ g₂ : E → 𝕜},
  Function.HasTemperateGrowth g₁ →
    Function.HasTemperateGrowth g₂ →
      SchwartzMap.smulLeftCLM F (g₁ + g₂) = SchwartzMap.smulLeftCLM F g₁ + SchwartzMap.smulLeftCLM F g₂
-- Init.Data.Array.Find
Array.findIdx_eq_getD_bind_find?_idxOf? : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {xs : Array α} {p : α → Bool},
  Array.findIdx p xs = ((Array.find? p xs).bind fun x => xs.idxOf? x).getD xs.size
-- Mathlib.MeasureTheory.Group.Prod
MeasureTheory.ae_measure_preimage_mul_right_lt_top : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [MeasurableMul₂ G] {s : Set G} [MeasurableInv G]
  (μ' ν' : MeasureTheory.Measure G) [MeasureTheory.SigmaFinite μ'] [MeasureTheory.SigmaFinite ν']
  [μ'.IsMulLeftInvariant] [ν'.IsMulLeftInvariant], μ' s ≠ ⊤ → ∀ᵐ (x : G) ∂μ', ν' ((fun x_1 => x_1 * x) ⁻¹' s) < ⊤
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
SSet.Subcomplex.PairingCore.AncestralRel.eq_1 : ∀ {X : SSet} {A : X.Subcomplex} (h : A.PairingCore) (s t : h.ι), h.AncestralRel s t = (s ≠ t ∧ h.type₂ s < h.type₁ t)
-- Mathlib.Data.Multiset.Count
/-- `countP p s` counts the number of elements of `s` (with multiplicity) that
satisfy `p`.  -/
Multiset.countP : {α : Type u_1} → (p : α → Prop) → [DecidablePred p] → Multiset α → ℕ
-- Mathlib.Topology.LocallyFinsupp
Function.locallyFinsuppWithin.restrictLatticeHom_apply : ∀ {X : Type u_1} [inst : TopologicalSpace X] {U : Set X} {Y : Type u_2} [inst_1 : AddCommGroup Y] [inst_2 : Lattice Y]
  {V : Set X} (D : Function.locallyFinsuppWithin U Y) (h : V ⊆ U),
  (Function.locallyFinsuppWithin.restrictLatticeHom h) D = D.restrict h
-- Mathlib.Data.Num.ZNum
ZNum.zneg_succ : ∀ (n : ZNum), -n.succ = (-n).pred
-- Mathlib.Topology.MetricSpace.PartitionOfUnity
/-- **Alias** of `Metric.exists_continuous_ennreal_forall_closedEBall_subset`.

---

Let `X` be an extended metric space. Let `K : ι → Set X` be a locally finite family of closed
sets, let `U : ι → Set X` be a family of open sets such that `K i ⊆ U i` for all `i`. Then there
exists a positive continuous function `δ : C(X, ℝ≥0∞)` such that for any `i` and `x ∈ K i`,
we have `Metric.closedEBall x (δ x) ⊆ U i`.  -/
EMetric.exists_continuous_eNNReal_forall_closedBall_subset : ∀ {ι : Type u_1} {X : Type u_2} [inst : EMetricSpace X] {K U : ι → Set X},
  (∀ (i : ι), IsClosed (K i)) →
    (∀ (i : ι), IsOpen (U i)) →
      (∀ (i : ι), K i ⊆ U i) →
        LocallyFinite K → ∃ δ, (∀ (x : X), 0 < δ x) ∧ ∀ (i : ι), ∀ x ∈ K i, Metric.closedEBall x (δ x) ⊆ U i
-- Mathlib.Algebra.Order.Module.Defs
PosSMulReflectLE.mk : ∀ {α : Type u_1} {β : Type u_2} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : Preorder β] [inst_3 : Zero α],
  (∀ ⦃a : α⦄, 0 < a → ∀ ⦃b₁ b₂ : β⦄, a • b₁ ≤ a • b₂ → b₁ ≤ b₂) → PosSMulReflectLE α β
-- Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits
CategoryTheory.ObjectProperty.preservesFiniteColimits_iff : ∀ {J : Type u_1} {C : Type u_3} [inst : CategoryTheory.Category.{v_3, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_5, u_3} C] (F : CategoryTheory.Functor J C),
  CategoryTheory.ObjectProperty.preservesFiniteColimits F ↔ CategoryTheory.Limits.PreservesFiniteColimits F
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.iUnion_cellFrontier_subset_skeleton : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : T2Space X] [inst_1 : Topology.RelCWComplex C D] (l : ℕ),
  ⋃ j, Topology.RelCWComplex.cellFrontier l j ⊆ ↑(Topology.RelCWComplex.skeleton C ↑l)
-- Mathlib.Algebra.Polynomial.Div
Polynomial.map_divByMonic : ∀ {R : Type u} {S : Type v} [inst : Ring R] {p q : Polynomial R} [inst_1 : Ring S] (f : R →+* S),
  q.Monic → Polynomial.map f (p /ₘ q) = Polynomial.map f p /ₘ Polynomial.map f q
-- Mathlib.Topology.Algebra.Monoid
AddMonoid.continuousSMul_nat : ∀ {A : Type u_6} [inst : AddMonoid A] [inst_1 : TopologicalSpace A] [ContinuousAdd A], ContinuousSMul ℕ A
-- Mathlib.Data.List.Lex
_private.Mathlib.Data.List.Lex.0.List.Lex.trichotomous.aux : ∀ {α : Type u} (r : α → α → Prop) [Std.Trichotomous r] (x x_1 : List α), ¬List.Lex r x x_1 → ¬List.Lex r x_1 x → x = x_1
-- Mathlib.CategoryTheory.Sites.Precoverage
CategoryTheory.Presieve.HasPairwisePullbacks.map_of_preservesPairwisePullbacks : ∀ {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) {X : C}
  (R : CategoryTheory.Presieve X) [F.PreservesPairwisePullbacks R] [R.HasPairwisePullbacks],
  (CategoryTheory.Presieve.map F R).HasPairwisePullbacks
-- Mathlib.Analysis.Fourier.FourierTransform
VectorFourier.fourierIntegral_const_smul : ∀ {𝕜 : Type u_1} [inst : CommRing 𝕜] {V : Type u_2} [inst_1 : AddCommGroup V] [inst_2 : Module 𝕜 V]
  [inst_3 : MeasurableSpace V] {W : Type u_3} [inst_4 : AddCommGroup W] [inst_5 : Module 𝕜 W] {E : Type u_4}
  [inst_6 : NormedAddCommGroup E] [inst_7 : NormedSpace ℂ E] (e : AddChar 𝕜 Circle) (μ : MeasureTheory.Measure V)
  (L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜) (f : V → E) (r : ℂ),
  VectorFourier.fourierIntegral e μ L (r • f) = r • VectorFourier.fourierIntegral e μ L f
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
/-- The degree of `cyclotomic' n R` is `totient n` if there is a primitive root of unity in `R`.  -/
Polynomial.degree_cyclotomic' : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] {ζ : R} {n : ℕ},
  IsPrimitiveRoot ζ n → (Polynomial.cyclotomic' n R).degree = ↑n.totient
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.withoutAutoBoundImplicit : {α : Type} → Lean.Elab.TermElabM α → Lean.Elab.TermElabM α
-- Mathlib.LinearAlgebra.Matrix.Vec
Matrix.vec_hadamard : ∀ {m : Type u_2} {n : Type u_3} {R : Type u_1} [inst : Mul R] (A B : Matrix m n R), (A.hadamard B).vec = A.vec * B.vec
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.Pi.ι_π_eq_id_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {β : Type w} [inst_2 : DecidableEq β] (f : β → C) [inst_3 : CategoryTheory.Limits.HasProduct f] (b : β) {Z : C}
  (h : f b ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.ι f b)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π f b) h) =
    h
-- Mathlib.Algebra.Module.Submodule.RestrictScalars
Submodule.disjoint_restrictScalars_iff : ∀ (S : Type u_1) {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Semiring S]
  [inst_3 : Module S M] [inst_4 : Module R M] [inst_5 : SMul S R] [inst_6 : IsScalarTower S R M] {s t : Submodule R M},
  Disjoint (Submodule.restrictScalars S s) (Submodule.restrictScalars S t) ↔ Disjoint s t
-- Mathlib.Algebra.Group.Units.Equiv
/-- Left multiplication by a unit of a monoid is a permutation of the underlying type.  -/
Units.mulLeft : {M : Type u_3} → [inst : Monoid M] → Mˣ → Equiv.Perm M
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Relations.Quotient.linearMap_ext : ∀ {A : Type u} [inst : Ring A] {relations : Module.Relations A} {M : Type v} [inst_1 : AddCommGroup M]
  [inst_2 : Module A M] {f f' : relations.Quotient →ₗ[A] M},
  (∀ (g : relations.G), f (relations.toQuotient fun₀ | g => 1) = f' (relations.toQuotient fun₀ | g => 1)) → f = f'
-- Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct
CategoryTheory.Limits.SequentialProduct.functorMap_epi : ∀ {C : Type u_1} {M N : ℕ → C} [inst : CategoryTheory.Category.{v_1, u_1} C] (f : (n : ℕ) → M n ⟶ N n)
  [inst_1 : CategoryTheory.Limits.HasCountableProducts C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [CategoryTheory.Limits.HasFiniteBiproducts C] [∀ (n : ℕ), CategoryTheory.Epi (f n)] (n : ℕ),
  CategoryTheory.Epi (CategoryTheory.Limits.SequentialProduct.functorMap f n)
-- Mathlib.Topology.Algebra.InfiniteSum.Constructions
tsum_star : ∀ {α : Type u_1} {β : Type u_2} {L : SummationFilter β} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α]
  [inst_2 : StarAddMonoid α] [ContinuousStar α] {f : β → α} [T2Space α],
  star (∑'[L] (b : β), f b) = ∑'[L] (b : β), star (f b)
-- Mathlib.RingTheory.Invariant.Galois
/-- For any domain `k` containing `B ⧸ Q`,
any endomorphism of `k` can be restricted to an endomorphism of `B ⧸ Q`.  -/
Ideal.Quotient.normal : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] (G : Type u_3)
  [Finite G] [inst_4 : Group G] [inst_5 : MulSemiringAction G B] [Algebra.IsInvariant A B G] (P : Ideal A) (Q : Ideal B)
  [inst_7 : Q.LiesOver P] [inst_8 : P.IsMaximal] [inst_9 : Q.IsMaximal], Normal (A ⧸ P) (B ⧸ Q)
-- Lean.Parser.Term
Lean.Parser.Term.attributes.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubMulAction.image_inclusion : ∀ {M : Type u_1} {α : Type u_2} [inst : Monoid M] [inst_1 : MulAction M α] (s : SubMulAction M α),
  Set.range ⇑s.inclusion = s.carrier
-- Mathlib.LinearAlgebra.TensorAlgebra.Basis
Module.Basis.tensorAlgebra_repr_apply : ∀ {κ : Type uκ} {R : Type uR} {M : Type uM} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (b : Module.Basis κ R M) (x : TensorAlgebra R M),
  b.tensorAlgebra.repr x = (FreeAlgebra.basisFreeMonoid R κ).repr ((TensorAlgebra.equivFreeAlgebra b) x)
-- Init.Data.List.Find
List.findFinIdx?.go.congr_simp : ∀ {α : Type u} (p p_1 : α → Bool),
  p = p_1 →
    ∀ (l l' l'_1 : List α) (e_l' : l' = l'_1) (i i_1 : ℕ) (e_i : i = i_1) (h : l'.length + i = l.length),
      List.findFinIdx?.go p l l' i h = List.findFinIdx?.go p_1 l l'_1 i_1 ⋯
-- Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
LiouvilleWith.nat_add : ∀ {p x : ℝ}, LiouvilleWith p x → ∀ (n : ℕ), LiouvilleWith p (↑n + x)
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
/-- A lax braided functor between braided monoidal categories is a lax monoidal functor
which preserves the braiding.
 -/
CategoryTheory.Functor.LaxBraided : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [CategoryTheory.BraidedCategory C] →
        {D : Type u₂} →
          [inst_3 : CategoryTheory.Category.{v₂, u₂} D] →
            [inst_4 : CategoryTheory.MonoidalCategory D] →
              [CategoryTheory.BraidedCategory D] → CategoryTheory.Functor C D → Type (max u₁ v₂)
-- Mathlib.Topology.Constructions.SumProd
/-- Precomposing `f` with `Prod.fst` is continuous at `x : X × Y`  -/
ContinuousAt.fst'' : ∀ {X : Type u} {Y : Type v} {Z : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {f : X → Z} {x : X × Y}, ContinuousAt f x.1 → ContinuousAt (fun x => f x.1) x
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafMap_restriction : ∀ {C₀ : Type u₀} {C : Type u} [inst : CategoryTheory.Category.{v₀, u₀} C₀] [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor C₀ C} {J₀ : CategoryTheory.GrothendieckTopology C₀}
  {J : CategoryTheory.GrothendieckTopology C} {A : Type u'} [inst_2 : CategoryTheory.Category.{v', u'} A]
  [inst_3 : CategoryTheory.Functor.IsDenseSubsite J₀ J F] (data : (X : C) → F.OneHypercoverDenseData J₀ J X)
  [inst_4 : CategoryTheory.Limits.HasLimitsOfSize.{w, w, v', u'} A] (G₀ : CategoryTheory.Sheaf J₀ A) {X Y : C} {X₀ : C₀}
  (f : F.obj X₀ ⟶ X) (g : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafMap data G₀ g)
      (CategoryTheory.Functor.OneHypercoverDenseData.essSurj.restriction data G₀ f) =
    CategoryTheory.Functor.OneHypercoverDenseData.essSurj.restriction data G₀ (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.Order.Filter.AtTopBot.Ring
Filter.Tendsto.atTop_of_mul_const₀ : ∀ {α : Type u_1} {β : Type u_2} [inst : Semiring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {l : Filter β}
  {f : β → α} {c : α}, 0 < c → Filter.Tendsto (fun x => f x * c) l Filter.atTop → Filter.Tendsto f l Filter.atTop
-- Mathlib.Order.Interval.Finset.Fin
Fin.attachFin_Ico_eq_Ici : ∀ {n : ℕ} (a : Fin n), (Finset.Ico (↑a) n).attachFin ⋯ = Finset.Ici a
-- Mathlib.RingTheory.Etale.StandardEtale
Algebra.instEtaleOfIsStandardEtale : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.IsStandardEtale R S], Algebra.Etale R S