mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.DirichletCharacter.Basic
/-- Dirichlet character associated to multiplication of Dirichlet characters,
after changing both levels to the same  -/
DirichletCharacter.mul : {R : Type u_1} →
  [inst : CommMonoidWithZero R] →
    {n m : ℕ} → DirichletCharacter R n → DirichletCharacter R m → DirichletCharacter R (n.lcm m)
-- Mathlib.Combinatorics.Quiver.Path.Vertices
Quiver.Path.end_mem_vertices : ∀ {V : Type u_1} [inst : Quiver V] {a b : V} (p : Quiver.Path a b), b ∈ p.vertices
-- Mathlib.Analysis.InnerProductSpace.Defs
HilbertSpace.mk : {𝕜 : Type u_4} →
  {E : Type u_5} →
    [inst : RCLike 𝕜] →
      [inst_1 : NormedAddCommGroup E] → [inst_2 : InnerProductSpace 𝕜 E] → [inst_3 : CompleteSpace E] → HilbertSpace 𝕜 E
-- Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
/-- Characterization of differentiable functions into a vector bundle in terms
of any trivialization. Version at a point within a set.  -/
Bundle.Trivialization.mdifferentiableWithinAt_section_iff : ∀ {𝕜 : 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]
  [inst_11 : (x : B) → AddCommMonoid (E x)] [inst_12 : (x : B) → Module 𝕜 (E x)] [inst_13 : VectorBundle 𝕜 F E]
  [ContMDiffVectorBundle 1 F E IB] (e : Bundle.Trivialization F Bundle.TotalSpace.proj) [MemTrivializationAtlas e]
  (s : (b : B) → E b) {u : Set B} {b₀ : B},
  b₀ ∈ e.baseSet → (MDiffAt[u] (T% s) b₀ ↔ (MDiffAt[u] fun x => (↑e ⟨x, s x⟩).2) b₀)
-- Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
GaussianFourier.integrable_cexp_neg_mul_sq_add_real_mul_I : ∀ {b : ℂ},
  0 < b.re →
    ∀ (c : ℝ), MeasureTheory.Integrable (fun x => Complex.exp (-b * (↑x + ↑c * Complex.I) ^ 2)) MeasureTheory.volume
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict
ContinuousLinearMap.toLinearMap_rangeRestrict : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4}
  {M₂ : Type u_5} [inst_2 : TopologicalSpace M₁] [inst_3 : AddCommMonoid M₁] [inst_4 : Module R₁ M₁]
  [inst_5 : TopologicalSpace M₂] [inst_6 : AddCommMonoid M₂] [inst_7 : Module R₂ M₂] [inst_8 : RingHomSurjective σ₁₂]
  (f : M₁ →SL[σ₁₂] M₂), ↑f.rangeRestrict = (↑f).rangeRestrict
-- Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
UniformConvergenceCLM.instContinuousSemilinearMapClass : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3}
  (F : Type u_4) [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜₁ E] [inst_4 : TopologicalSpace E]
  [inst_5 : AddCommGroup F] [inst_6 : Module 𝕜₂ F] [inst_7 : TopologicalSpace F] (𝔖 : Set (Set E)),
  ContinuousSemilinearMapClass (UniformConvergenceCLM σ F 𝔖) σ E F
-- Init.Data.Ord.Basic
instOrdInt : Ord ℤ
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidHom.mk.inj : ∀ {α : Type u_6} {β : Type u_7} {inst : Preorder α} {inst_1 : Preorder β} {inst_2 : AddZeroClass α}
  {inst_3 : AddZeroClass β} {toAddMonoidHom : α →+ β} {monotone' : Monotone (↑toAddMonoidHom).toFun}
  {toAddMonoidHom_1 : α →+ β} {monotone'_1 : Monotone (↑toAddMonoidHom_1).toFun},
  { toAddMonoidHom := toAddMonoidHom, monotone' := monotone' } =
      { toAddMonoidHom := toAddMonoidHom_1, monotone' := monotone'_1 } →
    toAddMonoidHom = toAddMonoidHom_1
-- Mathlib.Combinatorics.SimpleGraph.CycleGraph
SimpleGraph.cycleGraph.eq_3 : ∀ (n : ℕ), SimpleGraph.cycleGraph n.succ.succ = { Adj := fun a b => a - b = 1 ∨ b - a = 1, symm := ⋯, loopless := ⋯ }
-- Mathlib.CategoryTheory.Action.Basic
Action.resEquiv_functor : ∀ (V : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_3} {H : Type u_4} [inst_1 : Monoid G]
  [inst_2 : Monoid H] (f : G ≃* H), (Action.resEquiv V f).functor = Action.res V ↑f
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
_private.Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion.0.eisensteinSeries_coeff_identity : ∀ {k : ℕ},
  Even k →
    k ≠ 0 → (riemannZeta ↑k)⁻¹ * (-2 * ↑Real.pi * Complex.I) ^ k / ↑(k - 1).factorial = -(2 * ↑k / ↑(bernoulli k))
-- Lean.Meta.Tactic.Assert
Lean.Meta.Hypothesis.mk.injEq : ∀ (userName : Lean.Name) (type value : Lean.Expr) (binderInfo : Lean.BinderInfo) (kind : Lean.LocalDeclKind)
  (userName_1 : Lean.Name) (type_1 value_1 : Lean.Expr) (binderInfo_1 : Lean.BinderInfo) (kind_1 : Lean.LocalDeclKind),
  ({ userName := userName, type := type, value := value, binderInfo := binderInfo, kind := kind } =
      { userName := userName_1, type := type_1, value := value_1, binderInfo := binderInfo_1, kind := kind_1 }) =
    (userName = userName_1 ∧ type = type_1 ∧ value = value_1 ∧ binderInfo = binderInfo_1 ∧ kind = kind_1)
-- Mathlib.Algebra.GradedMonoid
/-- The term `one` of grade 0  -/
GradedMonoid.GOne.one : {ι : Type u_1} → {A : ι → Type u_2} → {inst : Zero ι} → [self : GradedMonoid.GOne A] → A 0
-- Init.Data.Array.Find
Array.map_findSome? : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → Option β} {g : β → γ} {xs : Array α},
  Option.map g (Array.findSome? f xs) = Array.findSome? (Option.map g ∘ f) xs
-- Mathlib.Algebra.MonoidAlgebra.Division
/-- **Alias** of `AddMonoidAlgebra.coeff_divOf`. -/
AddMonoidAlgebra.divOf_apply : ∀ {k : Type u_1} {G : Type u_2} [inst : Semiring k] [inst_1 : AddCommMonoid G] [inst_2 : IsCancelAdd G] (g : G)
  (x : AddMonoidAlgebra k G) (g' : G), (x.divOf g).coeff g' = x.coeff (g + g')
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.WalkingPair.noConfusionType : Sort v✝ → CategoryTheory.Limits.WalkingPair → CategoryTheory.Limits.WalkingPair → Sort v✝
-- Mathlib.Topology.Separation.DisjointCover
/-- Any open cover of a profinite space can be refined to a finite cover by clopens.  -/
TopologicalSpace.IsOpenCover.exists_finite_clopen_cover : ∀ {ι : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] [TotallyDisconnectedSpace X] [T2Space X] [CompactSpace X]
  {U : ι → TopologicalSpace.Opens X},
  TopologicalSpace.IsOpenCover U → ∃ n V, (∀ (j : Fin n), ∃ i, ↑(V j) ⊆ ↑(U i)) ∧ Set.univ ⊆ ⋃ j, ↑(V j)
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.NonemptyCompacts.isCompact_biUnion_coe_of_isCompact : ∀ {α : Type u_1} [inst : TopologicalSpace α] {S : Set (TopologicalSpace.NonemptyCompacts α)},
  IsCompact S → IsCompact (⋃ K ∈ S, ↑K)
-- Mathlib.Combinatorics.SimpleGraph.Copy
/-- **Alias** of the forward direction of `SimpleGraph.compl_isIndContained_compl`. -/
SimpleGraph.IsIndContained.of_compl : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W}, Gᶜ.IsIndContained Hᶜ → G.IsIndContained H
-- Mathlib.Algebra.Group.Equiv.Defs
/-- An additive isomorphism preserves addition.  -/
AddEquiv.map_add : ∀ {M : Type u_4} {N : Type u_5} [inst : Add M] [inst_1 : Add N] (f : M ≃+ N) (x y : M), f (x + y) = f x + f y
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.colimit.ι_inv_pre_assoc : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u} [inst_2 : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor J C)
  [inst_3 : CategoryTheory.Limits.HasColimit F] (E : CategoryTheory.Functor K J)
  [inst_4 : CategoryTheory.Limits.HasColimit (E.comp F)]
  [inst_5 : CategoryTheory.IsIso (CategoryTheory.Limits.colimit.pre F E)] (k : K) {Z : C}
  (h : CategoryTheory.Limits.colimit (E.comp F) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F (E.obj k))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.Limits.colimit.pre F E)) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (E.comp F) k) h
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoMod.congr_simp : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p p_1 : α} (e_p : p = p_1) (hp : 0 < p) (a a_1 : α),
  a = a_1 → ∀ (b b_1 : α), b = b_1 → toIcoMod hp a b = toIcoMod ⋯ a_1 b_1
-- Mathlib.Order.Interval.Set.Basic
Set.Iic_toDual : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, Set.Iic (OrderDual.toDual a) = ⇑OrderDual.ofDual ⁻¹' Set.Ici a
-- Mathlib.Order.CompleteBooleanAlgebra
OrderDual.instFrame : {α : Type u} → [Order.Coframe α] → Order.Frame αᵒᵈ
-- Mathlib.CategoryTheory.EpiMono
/-- A split mono which is epi is an iso.  -/
CategoryTheory.isIso_of_epi_of_isSplitMono : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : Y ⟶ X) [CategoryTheory.Epi f]
  [CategoryTheory.IsSplitMono f], CategoryTheory.IsIso f
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- An alternative formula for the braiding isomorphism which swaps a binary biproduct,
using the fact that the biproduct is a coproduct.  -/
CategoryTheory.Limits.biprod.braiding' : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] → (P Q : C) → P ⊞ Q ≅ Q ⊞ P
-- Lean.Meta.Tactic.FunIndCollect
Lean.Meta.FunInd.SeenCalls.mk : Array Lean.Expr → Std.HashSet (Lean.Name × Array Lean.Expr) → Lean.Meta.FunInd.SeenCalls
-- Std.Do.WP.SimpLemmas
Std.Do.WP.set_EStateM : ∀ {σ ε : Type u_1}
  {Q : Std.Do.PostCond PUnit.{u_1 + 1} (Std.Do.PostShape.except ε (Std.Do.PostShape.arg σ Std.Do.PostShape.pure))}
  (x : σ), (Std.Do.wp (set x)).apply Q = fun x_1 => Q.1 PUnit.unit x
-- Mathlib.Algebra.Group.End
AddAut.neg_apply : ∀ (M : Type u_2) [inst : Add M] (e : AddAut M) (m : M), (-e) m = (AddEquiv.symm e) m
-- Mathlib.Topology.Homotopy.Contractible
ContractibleSpace.instPathConnectedSpace : ∀ {X : Type u_1} [inst : TopologicalSpace X] [ContractibleSpace X], PathConnectedSpace X
-- Mathlib.Algebra.Lie.Nilpotent
/-- A Lie module is nilpotent if its lower central series reaches 0 (in a finite number of
steps).  -/
LieModule.IsNilpotent : (L : Type v) → (M : Type w) → [inst : LieRing L] → [inst_1 : AddCommGroup M] → [LieRingModule L M] → Prop
-- Mathlib.MeasureTheory.Integral.Lebesgue.Add
_private.Mathlib.MeasureTheory.Integral.Lebesgue.Add.0.MeasureTheory.«term_→ₛ_» : Lean.TrailingParserDescr
-- Mathlib.Data.EReal.Operations
EReal.add_lt_of_lt_sub : ∀ {a b c : EReal}, a < b - c → a + c < b
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
IsPrimitiveRoot.zmodEquivZPowers_apply_coe_nat : ∀ {R : Type u_4} {k : ℕ} [inst : CommRing R] {ζ : Rˣ} (h : IsPrimitiveRoot ζ k) (i : ℕ),
  h.zmodEquivZPowers ↑i = Additive.ofMul ⟨ζ ^ i, ⋯⟩
-- Mathlib.NumberTheory.MulChar.Basic
MulChar.mk.inj : ∀ {R : Type u_1} {inst : CommMonoid R} {R' : Type u_2} {inst_1 : CommMonoidWithZero R'} {toMonoidHom : R →* R'}
  {map_nonunit' : ∀ (a : R), ¬IsUnit a → (↑toMonoidHom).toFun a = 0} {toMonoidHom_1 : R →* R'}
  {map_nonunit'_1 : ∀ (a : R), ¬IsUnit a → (↑toMonoidHom_1).toFun a = 0},
  { toMonoidHom := toMonoidHom, map_nonunit' := map_nonunit' } =
      { toMonoidHom := toMonoidHom_1, map_nonunit' := map_nonunit'_1 } →
    toMonoidHom = toMonoidHom_1
-- Mathlib.GroupTheory.Nilpotent
/-- The nilpotency class of a nilpotent `G` is equal to the smallest `n` for which the descending
central series reaches `⊥` in its `n`-th term.  -/
Subgroup.least_descending_central_series_length_eq_nilpotencyClass : ∀ {G : Type u_1} [inst : Group G] [hG : Group.IsNilpotent G], Nat.find ⋯ = Group.nilpotencyClass G
-- Mathlib.GroupTheory.Subgroup.Center
AddSubgroup.centerToAddOpposite_symm_apply_coe : ∀ (G : Type u_1) [inst : AddGroup G] (r : ↥(AddSubsemigroup.center Gᵃᵒᵖ)),
  ↑((AddSubgroup.centerToAddOpposite G).symm r) = AddOpposite.unop ↑r
-- Mathlib.Order.Hom.Basic
OrderHom.fst_comp_prod : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  (f : α →o β) (g : α →o γ), OrderHom.fst.comp (f.prod g) = f
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
CategoryTheory.Pseudofunctor.DescentData'.pullHom'_hom_self : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} {sq : (i j : ι) → CategoryTheory.Limits.ChosenPullback (f i) (f j)}
  {sq₃ : (i₁ i₂ i₃ : ι) → CategoryTheory.Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)}
  (self : F.DescentData' sq sq₃) (i : ι),
  CategoryTheory.Pseudofunctor.DescentData'.pullHom' self.hom (f i) (CategoryTheory.CategoryStruct.id (X i))
      (CategoryTheory.CategoryStruct.id (X i)) ⋯ ⋯ =
    CategoryTheory.CategoryStruct.id
      ((F.map (CategoryTheory.CategoryStruct.id (X i)).op.toLoc).toFunctor.obj (self.obj i))
-- Mathlib.Data.Finset.Max
Finset.max_eq_sup_coe : ∀ {α : Type u_2} [inst : LinearOrder α] {s : Finset α}, s.max = s.sup WithBot.some
-- Mathlib.LinearAlgebra.RootSystem.RootPairingCat
RootPairingCat.coweightIsModule : {R : Type u} → [inst : CommRing R] → (self : RootPairingCat R) → Module R self.coweight
-- Mathlib.Data.PFunctor.Univariate.M
/-- Bisimulation is the standard proof technique for equality between
infinite tree-like structures  -/
PFunctor.M.IsBisimulation : {F : PFunctor.{uA, uB}} → (F.M → F.M → Prop) → Prop
-- Init.Data.Array.Lemmas
/-- Variant of `all_toArray` with a side condition on `stop`.  -/
List.all_toArray' : ∀ {α : Type u_1} {p : α → Bool} {l : List α} {stop : ℕ}, stop = l.toArray.size → l.toArray.all p 0 stop = l.all p
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.basicOpen_eq_zeroLocus_of_mul_add : ∀ {R : Type u} [inst : CommSemiring R] (e f : R),
  e * f = 0 → e + f = 1 → ↑(PrimeSpectrum.basicOpen e) = PrimeSpectrum.zeroLocus {f}
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roc.isSome_succMany?_of_lt_length_toList : ∀ {α : Type u} {r : Std.Roc α} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α]
  [inst_5 : Std.Rxc.IsAlwaysFinite α] {i : ℕ},
  i < r.toList.length → (Std.PRange.succMany? (i + 1) r.lower).isSome = true
-- Mathlib.Topology.MetricSpace.Isometry
IsometryEquiv.range_eq_univ : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] (h : α ≃ᵢ β),
  Set.range ⇑h = Set.univ
-- Mathlib.Computability.Partrec
/-- `Nat.Partrec f` means that the partial function `f : ℕ →. ℕ` is partially recursive.  -/
Nat.Partrec : (ℕ →. ℕ) → Prop
-- Mathlib.Data.W.Cardinal
/-- `#(WType β)` is the least cardinal `κ` such that `sum (fun a : α ↦ κ ^ #(β a)) ≤ κ`  -/
WType.cardinalMk_le_of_le : ∀ {α : Type u} {β : α → Type u} {κ : Cardinal.{u}},
  (Cardinal.sum fun a => κ ^ Cardinal.mk (β a)) ≤ κ → Cardinal.mk (WType β) ≤ κ
-- Mathlib.Order.Interval.Set.InitialSeg
/-- `Iio j` is a principal segment.  -/
Set.principalSegIio : {α : Type u_1} → [inst : Preorder α] → (j : α) → ↑(Set.Iio j) <i α
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.preimage_interior : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y) (s : Set Y),
  ⇑h ⁻¹' interior s = interior (⇑h ⁻¹' s)
-- Mathlib.Topology.Category.Profinite.Nobeling.Successor
/-- Given `l : MaxProducts C ho`, its `Tail` is a `GoodProducts (C' C ho)`.  -/
Profinite.NobelingProof.GoodProducts.MaxToGood : {I : Type u} →
  (C : Set (I → Bool)) →
    [inst : LinearOrder I] →
      [inst_1 : WellFoundedLT I] →
        {o : Ordinal.{u}} →
          IsClosed C →
            Profinite.NobelingProof.contained C (Order.succ o) →
              (ho : o < Ordinal.type fun x1 x2 => x1 < x2) →
                ⊤ ≤
                    Submodule.span ℤ
                      (Set.range
                        (Profinite.NobelingProof.GoodProducts.eval
                          (Profinite.NobelingProof.π C fun x => Profinite.NobelingProof.ord I x < o))) →
                  ↑(Profinite.NobelingProof.GoodProducts.MaxProducts C ho) →
                    ↑(Profinite.NobelingProof.GoodProducts (Profinite.NobelingProof.C' C ho))
-- Mathlib.GroupTheory.Index
AddSubgroup.relIndex_dvd_card : ∀ {G : Type u_1} [inst : AddGroup G] (H K : AddSubgroup G), H.relIndex K ∣ Nat.card ↥K
-- Mathlib.NumberTheory.PrimeCounting
Nat.surjective_primeCounting : Function.Surjective Nat.primeCounting
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.CoordinateRing.basis_apply : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Affine R} (n : Fin 2),
  (WeierstrassCurve.Affine.CoordinateRing.basis W') n = (AdjoinRoot.powerBasis' ⋯).gen ^ ↑n
-- Std.Data.HashSet.Basic
/-- Internal implementation detail of the hash set.  -/
Std.HashSet.inner : {α : Type u} → [inst : BEq α] → [inst_1 : Hashable α] → Std.HashSet α → Std.HashMap α Unit
-- Mathlib.Algebra.Group.Equiv.Defs
MulEquivClass.instMonoidHomClass : ∀ (F : Type u_1) {M : Type u_4} {N : Type u_5} [inst : EquivLike F M N] [inst_1 : MulOneClass M]
  [inst_2 : MulOneClass N] [MulEquivClass F M N], MonoidHomClass F M N
-- Mathlib.Algebra.Ring.Submonoid.Pointwise
AddSubmonoid.smul_le_smul_right : ∀ {R : Type u_2} {A : Type u_3} [inst : AddMonoid R] [inst_1 : AddMonoid A] [inst_2 : DistribSMul R A]
  {M : AddSubmonoid R} {N P : AddSubmonoid A}, N ≤ P → M • N ≤ M • P
-- Mathlib.Geometry.Convex.Cone.Basic
/-- A flat cone is always pointed (contains `0`).  -/
ConvexCone.Flat.pointed : ∀ {R : Type u_2} {G : Type u_3} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup G]
  [inst_3 : SMul R G] {C : ConvexCone R G}, C.Flat → C.Pointed
-- Mathlib.Algebra.Group.Action.Pointwise.Finset
Nat.decidablePred_mem_vadd_set : {s : Set ℕ} → [DecidablePred fun x => x ∈ s] → (a : ℕ) → DecidablePred fun x => x ∈ a +ᵥ s
-- Mathlib.Geometry.Euclidean.Sphere.Tangent
EuclideanGeometry.Sphere.IsTangentAt.eq_orthogonalProjection : ∀ {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 : EuclideanGeometry.Sphere P} {p : P} {as : AffineSubspace ℝ P}
  [inst_4 : Nonempty ↥as] [inst_5 : as.direction.HasOrthogonalProjection],
  s.IsTangentAt p as → p = ↑((EuclideanGeometry.orthogonalProjection as) s.center)
-- Init.Data.List.Nat.Range
List.nodup_range : ∀ {n : ℕ}, (List.range n).Nodup
-- Mathlib.Data.Multiset.ZeroCons
Multiset.cons_swap : ∀ {α : Type u_1} (a b : α) (s : Multiset α), a ::ₘ b ::ₘ s = b ::ₘ a ::ₘ s
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.invFun_eq_symm : ∀ {R : Type u_4} {S : Type u_5} [inst : Mul R] [inst_1 : Mul S] [inst_2 : Add R] [inst_3 : Add S] (f : R ≃+* S),
  EquivLike.inv f = ⇑f.symm
-- Mathlib.Data.Nat.Size
Nat.shiftLeft'_true_eq_mul_pow : ∀ (m n : ℕ), Nat.shiftLeft' true m n + 1 = (m + 1) * 2 ^ n
-- Batteries.Data.MLList.Basic
/-- Gives the monadic lazy list consisting all of folds of a function on a given initial element.
Thus `[a₀, a₁, ...].foldsM f b` will give `[b, f b a₀, f (f b a₀) a₁, ...]`.  -/
MLList.folds : {m : Type u_1 → Type u_1} → {β α : Type u_1} → [Monad m] → (β → α → β) → β → MLList m α → MLList m β
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.instInhabitedCnstrRHS : Inhabited Lean.Meta.Grind.CnstrRHS
-- Mathlib.Order.Filter.Ultrafilter.Defs
/-- Ultrafilter extending the inf of a comapped ultrafilter and a principal ultrafilter.  -/
Ultrafilter.ofComapInfPrincipal : {α : Type u} → {β : Type v} → {m : α → β} → {s : Set α} → {g : Ultrafilter β} → m '' s ∈ g → Ultrafilter α
-- Init.GrindInstances.ToInt
Lean.Grind.instMulInt64SintOfNatNat : Lean.Grind.ToInt.Mul Int64 (Lean.Grind.IntInterval.sint 64)
-- Mathlib.Data.Part
Part.instDiv : {α : Type u_1} → [Div α] → Div (Part α)
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic
SSet.anodyneExtensions_eq_llp_rlp : SSet.anodyneExtensions = SSet.modelCategoryQuillen.J.rlp.llp
-- Mathlib.Tactic.Widget.StringDiagram
/-- Construct a string diagram from a Penrose `sub`stance program and expressions `embeds` to
display as labels in the diagram.  -/
Mathlib.Tactic.Widget.StringDiagram.mkStringDiagram : List (List Mathlib.Tactic.Widget.StringDiagram.Node) →
  List (List Mathlib.Tactic.Widget.StringDiagram.Strand) → ProofWidgets.Penrose.DiagramBuilderM PUnit.{1}
-- Mathlib.Algebra.Polynomial.Basic
/-- `erase p n` is the polynomial `p` in which the `X^n` term has been erased.  -/
Polynomial.erase : {R : Type u_1} → [inst : Semiring R] → ℕ → Polynomial R → Polynomial R
-- Mathlib.Analysis.LocallyConvex.AbsConvex
absConvexHull_mono : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E] [inst_2 : AddCommMonoid E]
  [inst_3 : PartialOrder 𝕜] {s t : Set E}, s ⊆ t → (absConvexHull 𝕜) s ⊆ (absConvexHull 𝕜) t
-- Mathlib.Order.BourbakiWitt
/-- A chain complete partial order (CCPO) is a nonempty partial order such that every
nonempty chain has a supremum (which we call `cSup`)  -/
ChainCompletePartialOrder : Type u_4 → Type u_4
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.hasCoequalizer_epi_comp : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y}
  [CategoryTheory.Limits.HasCoequalizer f g] {W : C} (h : W ⟶ X) [CategoryTheory.Epi h],
  CategoryTheory.Limits.HasCoequalizer (CategoryTheory.CategoryStruct.comp h f) (CategoryTheory.CategoryStruct.comp h g)
-- Init.Data.UInt.Basic
/-- The modulo operator for 64-bit unsigned integers, which computes the remainder when dividing one
integer by another. Usually accessed via the `%` operator.

When the divisor is `0`, the result is the dividend rather than an error.

This function is overridden at runtime with an efficient implementation.

Examples:
* `UInt64.mod 5 2 = 1`
* `UInt64.mod 4 2 = 0`
* `UInt64.mod 4 0 = 4`
 -/
UInt64.mod : UInt64 → UInt64 → UInt64
-- Lean.Data.DeclarationRange
Lean.DeclarationRanges.mk : Lean.DeclarationRange → Lean.DeclarationRange → Lean.DeclarationRanges
-- Lean.Data.Lsp.Internal
/-- Range of this location.  -/
Lean.Lsp.RefInfo.Location.range : Lean.Lsp.RefInfo.Location → Lean.Lsp.Range
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
LinearMap.BilinForm.toMatrix_mul_basis_toMatrix : ∀ {R₁ : Type u_1} {M₁ : Type u_2} [inst : CommSemiring R₁] [inst_1 : AddCommMonoid M₁] [inst_2 : Module R₁ M₁]
  {n : Type u_5} {o : Type u_6} [inst_3 : Fintype n] [inst_4 : Fintype o] [inst_5 : DecidableEq n]
  (b : Module.Basis n R₁ M₁) [inst_6 : DecidableEq o] (c : Module.Basis o R₁ M₁) (B : LinearMap.BilinForm R₁ M₁),
  (b.toMatrix ⇑c).transpose * (LinearMap.BilinForm.toMatrix b) B * b.toMatrix ⇑c = (LinearMap.BilinForm.toMatrix c) B
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get?.congr_simp : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [inst : Std.TransCmp cmp]
  (t t_1 : Std.ExtDTreeMap α (fun x => β) cmp),
  t = t_1 → ∀ (a a_1 : α), a = a_1 → Std.ExtDTreeMap.Const.get? t a = Std.ExtDTreeMap.Const.get? t_1 a_1
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
/-- For `f : SkewMonoidAlgebra k G`, `f.support` is the set of all `a ∈ G` such that
`f.coeff a ≠ 0`.  -/
SkewMonoidAlgebra.support : {k : Type u_1} → {G : Type u_2} → [inst : AddMonoid k] → SkewMonoidAlgebra k G → Finset G
-- Qq.Match
_private.Qq.Match.0.Qq.floatLevelAntiquot : Lean.Syntax.Level → StateT (Array Qq.Lift✝) Lean.MacroM Lean.Syntax.Level
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.InfinitePlace.embedding_of_isReal.congr_simp : ∀ {K : Type u_1} [inst : Field K] {w w_1 : NumberField.InfinitePlace K} (e_w : w = w_1) (hw : w.IsReal),
  NumberField.InfinitePlace.embedding_of_isReal hw = NumberField.InfinitePlace.embedding_of_isReal ⋯
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.continuousSemilinearMapClass : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4}
  [inst_2 : TopologicalSpace M₁] [inst_3 : AddCommMonoid M₁] {M₂ : Type u_6} [inst_4 : TopologicalSpace M₂]
  [inst_5 : AddCommMonoid M₂] [inst_6 : Module R₁ M₁] [inst_7 : Module R₂ M₂],
  ContinuousSemilinearMapClass (M₁ →SL[σ₁₂] M₂) σ₁₂ M₁ M₂