mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
SemilinearIsometryClass.nnnorm_map : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} {𝓕 : Type u_10} [inst : Semiring R]
  [inst_1 : Semiring R₂] {σ₁₂ : R →+* R₂} [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup E₂]
  [inst_4 : Module R E] [inst_5 : Module R₂ E₂] [inst_6 : FunLike 𝓕 E E₂] [SemilinearIsometryClass 𝓕 σ₁₂ E E₂] (f : 𝓕)
  (x : E), ‖f x‖₊ = ‖x‖₊
-- Mathlib.RingTheory.Algebraic.Cardinality
Algebra.IsAlgebraic.lift_cardinalMk_le_max : ∀ (R : Type u) [inst : CommRing R] [IsDomain R] (L : Type v) [inst_2 : CommRing L] [IsDomain L] [inst_4 : Algebra R L]
  [Module.IsTorsionFree R L] [Algebra.IsAlgebraic R L],
  Cardinal.lift.{u, v} (Cardinal.mk L) ≤ max (Cardinal.lift.{v, u} (Cardinal.mk R)) Cardinal.aleph0
-- Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
/-- The integral of the Gaussian function over the vertical edges of a rectangle
with vertices at `(±T, 0)` and `(±T, c)`.  -/
GaussianFourier.verticalIntegral : ℂ → ℝ → ℝ → ℂ
-- Init.Prelude
/-- Unpacks a `UInt16` into a `BitVec 16`. This function is overridden with a native implementation.
 -/
UInt16.toBitVec : UInt16 → BitVec 16
-- Lean.Elab.PreDefinition.PartialFixpoint.Induction
/-- Appends `_1` etc to `base` unless `n == 1`  -/
_private.Lean.Elab.PreDefinition.PartialFixpoint.Induction.0.Lean.Elab.PartialFixpoint.numberNames : ℕ → String → Array Lean.Name
-- Mathlib.FieldTheory.IsPerfectClosure
IsPRadical.mk : ∀ {K : Type u_1} {L : Type u_2} [inst : CommSemiring K] [inst_1 : CommSemiring L] {i : K →+* L} {p : ℕ},
  (∀ (x : L), ∃ n y, i y = x ^ p ^ n) → RingHom.ker i ≤ pNilradical K p → IsPRadical i p
-- Mathlib.CategoryTheory.Bicategory.Yoneda
/-- Middle component of the associator as a 2-isomorphism in `Cat`.  -/
CategoryTheory.Bicategory.associatorNatIsoMiddleCat : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c d : B} →
      (f : a ⟶ b) →
        (h : c ⟶ d) →
          CategoryTheory.CategoryStruct.comp ((CategoryTheory.Bicategory.precomposingCat a b c).obj f)
              ((CategoryTheory.Bicategory.postcomposingCat a c d).obj h) ≅
            CategoryTheory.CategoryStruct.comp ((CategoryTheory.Bicategory.postcomposingCat b c d).obj h)
              ((CategoryTheory.Bicategory.precomposingCat a b d).obj f)
-- Mathlib.FieldTheory.CardinalEmb
Field.Emb.cardinal_eq_two_pow_sepDegree : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] [Algebra.IsAlgebraic F E],
  Cardinal.aleph0 ≤ Field.sepDegree F E → Cardinal.mk (Field.Emb F E) = 2 ^ Field.sepDegree F E
-- Lean.Meta.DiscrTree.Basic
Lean.Meta.DiscrTree.empty : {α : Type} → Lean.Meta.DiscrTree α
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
lineDeriv_zero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type u_3} [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] {f : E → F} {x : E},
  lineDeriv 𝕜 f x 0 = 0
-- Mathlib.NumberTheory.FLT.Three
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution.x.congr_simp : ∀ {K : Type u_1} [inst : Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3}
  (S S_1 : FermatLastTheoremForThreeGen.Solution✝ hζ),
  S = S_1 →
    ∀ [inst_1 : NumberField K] [inst_2 : IsCyclotomicExtension {3} ℚ K],
      FermatLastTheoremForThreeGen.Solution.x✝ S = FermatLastTheoremForThreeGen.Solution.x✝ S_1
-- Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Asymptotics.SuperpolynomialDecay.inv_param_mul : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} {k f : α → β} [inst : TopologicalSpace β] [inst_1 : Field β]
  [inst_2 : LinearOrder β] [IsStrictOrderedRing β] [OrderTopology β],
  Filter.Tendsto k l Filter.atTop →
    Asymptotics.SuperpolynomialDecay l k f → Asymptotics.SuperpolynomialDecay l k (k⁻¹ * f)
-- Mathlib.Order.FixedPoints
OrderHom.lfp_le_fixed : ∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α) {a : α}, f a = a → OrderHom.lfp f ≤ a
-- Std.Data.ExtDHashMap.Lemmas
_private.Std.Data.ExtDHashMap.Lemmas.0.Std.ExtDHashMap.Const.insertManyIfNewUnit_list_mk : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {m : Std.DHashMap α fun x => Unit} {l : List α},
  Std.ExtDHashMap.Const.insertManyIfNewUnit (Std.ExtDHashMap.mk m) l =
    Std.ExtDHashMap.mk (Std.DHashMap.Const.insertManyIfNewUnit m l)
-- Mathlib.Logic.Function.Basic
Function.instIsTransSwapProp : ∀ {α : Sort u_1} (r : α → α → Prop) [IsTrans α r], IsTrans α (Function.swap r)
-- Mathlib.Order.Interval.Set.Disjoint
Set.Ioc_disjoint_Ioc : ∀ {α : Type v} [inst : LinearOrder α] {a₁ a₂ b₁ b₂ : α},
  Disjoint (Set.Ioc a₁ a₂) (Set.Ioc b₁ b₂) ↔ min a₂ b₂ ≤ max a₁ b₁
-- Mathlib.NumberTheory.ModularForms.QExpansion
ModularForm.cuspFunction_neg : ∀ {k : ℤ} {F : Type u_1} [inst : FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ},
  0 < h →
    h ∈ Γ.strictPeriods →
      ∀ (f : F) [ModularFormClass F Γ k], UpperHalfPlane.cuspFunction h (-⇑f) = -UpperHalfPlane.cuspFunction h ⇑f
-- Mathlib.LinearAlgebra.Span.Basic
/-- If a bilinear map takes values in a submodule along two sets, then the same is true along
the span of these sets.  -/
LinearMap.BilinMap.apply_apply_mem_of_mem_span : ∀ {R : Type u_9} {M : Type u_10} {N : Type u_11} {P : Type u_12} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Module R P] (P' : Submodule R P) (s : Set M) (t : Set N) (B : M →ₗ[R] N →ₗ[R] P),
  (∀ x ∈ s, ∀ y ∈ t, (B x) y ∈ P') → ∀ (x : M) (y : N), x ∈ Submodule.span R s → y ∈ Submodule.span R t → (B x) y ∈ P'
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue?_nil : ∀ {α : Type u} {β : Type v} [inst : BEq α] {a : α}, Std.Internal.List.getValue? a [] = none
-- Lean.Message
/-- Creates a tag (i.e., message kind) for an error message with (user-facing) name `errorName`.
 -/
Lean.kindOfErrorName : Lean.Name → Lean.Name
-- Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty
/-- When `j : J` is not maximal, this is the extension in `Φ.Iteration (Order.succ j)`
of any `iter : Φ.Iteration j`.  -/
CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfSucc : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {Φ : CategoryTheory.SmallObject.SuccStruct C} →
      {J : Type u} →
        [inst_1 : LinearOrder J] →
          [inst_2 : OrderBot J] →
            [inst_3 : SuccOrder J] →
              [inst_4 : WellFoundedLT J] →
                [inst_5 : CategoryTheory.Limits.HasIterationOfShape J C] →
                  {j : J} → ¬IsMax j → Φ.Iteration j → Φ.Iteration (Order.succ j)
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.Action.notApplicable : Lean.Meta.Grind.Action
-- Mathlib.Algebra.Category.ModuleCat.Adjunctions
CategoryTheory.Free.instPreadditive : (R : Type u_1) →
  [inst : CommRing R] →
    (C : Type u) → [inst_1 : CategoryTheory.Category.{v, u} C] → CategoryTheory.Preadditive (CategoryTheory.Free R C)
-- Mathlib.Topology.Order.NhdsSet
Ici_mem_nhdsSet_Ici : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderClosedTopology α] {a b : α},
  a < b → Set.Ici a ∈ nhdsSet (Set.Ici b)
-- Mathlib.RingTheory.Coalgebra.Equiv
CoalgEquiv.mk : {R : Type u_5} →
  [inst : CommSemiring R] →
    {A : Type u_6} →
      {B : Type u_7} →
        [inst_1 : AddCommMonoid A] →
          [inst_2 : AddCommMonoid B] →
            [inst_3 : Module R A] →
              [inst_4 : Module R B] →
                [inst_5 : CoalgebraStruct R A] →
                  [inst_6 : CoalgebraStruct R B] →
                    (toCoalgHom : A →ₗc[R] B) →
                      (invFun : B → A) →
                        autoParam (Function.LeftInverse invFun toCoalgHom.toFun) Equiv.left_inv._autoParam →
                          autoParam (Function.RightInverse invFun toCoalgHom.toFun) Equiv.right_inv._autoParam →
                            A ≃ₗc[R] B
-- Mathlib.Data.PFunctor.Multivariate.M
MvPFunctor.M.dest'_eq_dest' : ∀ {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u} n} {x : P.last.M} {a₁ : P.A} {f₁ : P.last.B a₁ → P.last.M}
  (h₁ : x.dest = ⟨a₁, f₁⟩) {a₂ : P.A} {f₂ : P.last.B a₂ → P.last.M} (h₂ : x.dest = ⟨a₂, f₂⟩)
  (f' : TypeVec.Arrow (MvPFunctor.M.Path P x) α), MvPFunctor.M.dest' P h₁ f' = MvPFunctor.M.dest' P h₂ f'
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.denote_mulPow : ∀ {α : Type u_1} [inst : Lean.Grind.CommSemiring α] (ctx : Lean.Grind.CommRing.Context α)
  (p : Lean.Grind.CommRing.Power) (m : Lean.Grind.CommRing.Mon),
  Lean.Grind.CommRing.Mon.denote ctx (Lean.Grind.CommRing.Mon.mulPow p m) =
    Lean.Grind.CommRing.Power.denote ctx p * Lean.Grind.CommRing.Mon.denote ctx m
-- Mathlib.Topology.MetricSpace.Infsep
Set.infsep_pos : ∀ {α : Type u_1} [inst : EDist α] {s : Set α}, 0 < s.infsep ↔ 0 < s.einfsep ∧ s.einfsep < ⊤
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.num_mul_dvd : ∀ {K : Type u} [inst : Field K] (x y : RatFunc K), (x * y).num ∣ x.num * y.num
-- Lean.Elab.Tactic.Conv.Pattern
Lean.Elab.Tactic.Conv.PatternMatchState.all.sizeOf_spec : ∀ (subgoals : Array Lean.MVarId), sizeOf (Lean.Elab.Tactic.Conv.PatternMatchState.all subgoals) = 1 + sizeOf subgoals
-- Std.Http.Data.Headers.Basic
/-- Serializes a `Host` header back to a name and a value.
 -/
Std.Http.Header.Host.serialize : Std.Http.Header.Host → Std.Http.Header.Name × Std.Http.Header.Value
-- Lean.Elab.Tactic.Conv.Basic
_private.Lean.Elab.Tactic.Conv.Basic.0.Lean.Elab.Tactic.Conv.convLocalDecl : Lean.Syntax → Lean.Name → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_hom_app_assoc : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] {F G : CategoryTheory.Pseudofunctor B CategoryTheory.Cat}
  (α : F ⟶ G) (a : B) (X : ↑(F.obj a)) {Z : ↑(G.obj a)}
  (h : (G.map (CategoryTheory.CategoryStruct.id a)).toFunctor.obj ((α.app a).toFunctor.obj X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((α.naturality (CategoryTheory.CategoryStruct.id a)).hom.toNatTrans.app X) h =
    CategoryTheory.CategoryStruct.comp ((α.app a).toFunctor.map ((F.mapId a).hom.toNatTrans.app X))
      (CategoryTheory.CategoryStruct.comp ((G.mapId a).inv.toNatTrans.app ((α.app a).toFunctor.obj X)) h)
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.mk.sizeOf_spec : ∀ {X : AlgebraicGeometry.Scheme} (ideal : (U : ↑X.affineOpens) → Ideal ↑(X.presheaf.obj (Opposite.op ↑U)))
  (map_ideal_basicOpen :
    ∀ (U : ↑X.affineOpens) (f : ↑(X.presheaf.obj (Opposite.op ↑U))),
      Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (CategoryTheory.homOfLE ⋯).op)) (ideal U) =
        ideal (X.affineBasicOpen f))
  (supportSet : Set ↥X)
  (supportSet_eq_iInter_zeroLocus :
    autoParam (supportSet = ⋂ U, X.zeroLocus ↑(ideal U))
      AlgebraicGeometry.Scheme.IdealSheafData.supportSet_eq_iInter_zeroLocus._autoParam),
  sizeOf
      { ideal := ideal, map_ideal_basicOpen := map_ideal_basicOpen, supportSet := supportSet,
        supportSet_eq_iInter_zeroLocus := supportSet_eq_iInter_zeroLocus } =
    1 + sizeOf supportSet_eq_iInter_zeroLocus
-- Init.Data.Float.Float
Float.ofModel.inj : ∀ {toModel toModel_1 : Float.Model}, { toModel := toModel } = { toModel := toModel_1 } → toModel = toModel_1
-- Init.Data.UInt.Bitwise
UInt16.or_not_self : ∀ {a : UInt16}, a ||| ~~~a = -1
-- Mathlib.Algebra.Homology.TotalComplexShift
HomologicalComplex₂.totalShift₁Iso_hom_naturality_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)} (f : K ⟶ L) (x : ℤ)
  [inst_2 : K.HasTotal (ComplexShape.up ℤ)] [inst_3 : L.HasTotal (ComplexShape.up ℤ)]
  {Z : HomologicalComplex C (ComplexShape.up ℤ)}
  (h :
    (CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) x).obj (L.total (ComplexShape.up ℤ)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (HomologicalComplex₂.total.map ((HomologicalComplex₂.shiftFunctor₁ C x).map f) (ComplexShape.up ℤ))
      (CategoryTheory.CategoryStruct.comp (L.totalShift₁Iso x).hom h) =
    CategoryTheory.CategoryStruct.comp (K.totalShift₁Iso x).hom
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) x).map
          (HomologicalComplex₂.total.map f (ComplexShape.up ℤ)))
        h)
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
/-- A variant of `tendsto_atTop` that
uses `∃ N, ∀ n > N, ...` rather than `∃ N, ∀ n ≥ N, ...`
 -/
Metric.tendsto_atTop' : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [Nonempty β] [inst_2 : SemilatticeSup β] [NoMaxOrder β]
  {u : β → α} {a : α}, Filter.Tendsto u Filter.atTop (nhds a) ↔ ∀ ε > 0, ∃ N, ∀ n > N, dist (u n) a < ε
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- The bijection of `Fork.IsLimit.homIso` is natural in `Z`.  -/
CategoryTheory.Limits.Fork.IsLimit.homIso_natural : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {t : CategoryTheory.Limits.Fork f g}
  (ht : CategoryTheory.Limits.IsLimit t) {Z Z' : C} (q : Z' ⟶ Z) (k : Z ⟶ t.pt),
  ↑((CategoryTheory.Limits.Fork.IsLimit.homIso ht Z') (CategoryTheory.CategoryStruct.comp q k)) =
    CategoryTheory.CategoryStruct.comp q ↑((CategoryTheory.Limits.Fork.IsLimit.homIso ht Z) k)
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
/-- The opposite of `Δ[n]` is isomorphic to `Δ[n]`.  -/
SSet.stdSimplex.opIso : (n : SimplexCategory) → (SSet.stdSimplex.obj n).op ≅ SSet.stdSimplex.obj n
-- Mathlib.CategoryTheory.Sites.Types
CategoryTheory.equivYoneda'_hom_hom : ∀ (S : CategoryTheory.Sheaf CategoryTheory.typesGrothendieckTopology (Type u)),
  (CategoryTheory.equivYoneda' S).hom.hom = (CategoryTheory.equivYoneda S.obj ⋯).hom
-- Lean.Structure
Lean.StructureResolutionState.mk.injEq : ∀ (resolutions resolutions_1 : Lean.PHashMap Lean.Name (Array Lean.Name)),
  ({ resolutions := resolutions } = { resolutions := resolutions_1 }) = (resolutions = resolutions_1)
-- Lean.Setup
Lean.Plugin.mk.injEq : ∀ (path : System.FilePath) (initFn? : Option String) (path_1 : System.FilePath) (initFn?_1 : Option String),
  ({ path := path, initFn? := initFn? } = { path := path_1, initFn? := initFn?_1 }) =
    (path = path_1 ∧ initFn? = initFn?_1)
-- Mathlib.Order.Category.Lat
Lat.Iso.mk_hom : ∀ {α β : Lat} (e : ↑α ≃o ↑β), (Lat.Iso.mk e).hom = Lat.ofHom { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯ }
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_add_intCast' : ∀ {x y : ℝ}, 0 ≤ x → ∀ {n : ℤ}, y + ↑n ≠ 0 → x ^ (y + ↑n) = x ^ y * x ^ n
-- Mathlib.Algebra.Order.Interval.Set.Instances
Set.Icc.coe_ne_zero : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R] {x : ↑(Set.Icc 0 1)},
  ↑x ≠ 0 ↔ x ≠ 0
-- Mathlib.Algebra.Group.Equiv.Defs
MulEquiv.instInhabited : {M : Type u_4} → [inst : Mul M] → Inhabited (M ≃* M)
-- Std.Http.Data.URI.Config
/-- Maximum length of the fragment component, in bytes.
 -/
Std.Http.URI.Config.maxFragmentLength : Std.Http.URI.Config → ℕ
-- Std.Async.Process
Std.IO.Process.ResourceUsageStats.mk : Std.Time.Millisecond.Offset →
  Std.Time.Millisecond.Offset →
    UInt64 →
      UInt64 →
        UInt64 →
          UInt64 →
            UInt64 →
              UInt64 →
                UInt64 →
                  UInt64 → UInt64 → UInt64 → UInt64 → UInt64 → UInt64 → UInt64 → Std.IO.Process.ResourceUsageStats
-- Mathlib.RingTheory.Polynomial.ScaleRoots
Polynomial.map_scaleRoots : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : Semiring S] (p : Polynomial R) (x : R) (f : R →+* S),
  f p.leadingCoeff ≠ 0 → Polynomial.map f (p.scaleRoots x) = (Polynomial.map f p).scaleRoots (f x)
-- Mathlib.Computability.AkraBazzi.SumTransform
AkraBazziRecurrence.eventually_atTop_sumTransform_ge : ∀ {α : Type u_1} [inst : Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ} [inst_1 : Nonempty α]
  (R : AkraBazziRecurrence T g a b r),
  ∃ c > 0,
    ∀ᶠ (n : ℕ) in Filter.atTop,
      ∀ (i : α), c * g ↑n ≤ AkraBazziRecurrence.sumTransform (AkraBazziRecurrence.p a b) g (r i n) n
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.equiv_iff_toArray_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp],
  t₁.Equiv t₂ ↔ t₁.toArray = t₂.toArray
-- Mathlib.NumberTheory.EulerProduct.DirichletLSeries
/-- When `s.re > 1`, the map `n ↦ n^(-s)` is norm-summable.  -/
summable_riemannZetaSummand : ∀ {s : ℂ} (hs : 1 < s.re), Summable fun n => ‖(riemannZetaSummandHom ⋯) n‖
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.coe_mulSingle_apply : ∀ {ι : Type u_1} {S : ι → Type u_3} {G : ι → Type u_4} [inst : (i : ι) → SetLike (S i) (G i)] (A : (i : ι) → S i)
  [inst_1 : DecidableEq ι] [inst_2 : (i : ι) → One (G i)] [inst_3 : ∀ (i : ι), OneMemClass (S i) (G i)] (i : ι)
  (x : G i) (j : ι), (RestrictedProduct.mulSingle A i x) j = Pi.mulSingle i x j
-- Mathlib.Algebra.Group.Basic
hom_coe_nsmul : ∀ {M : Type u_4} {F : Type u_5} [inst : AddMonoid F] (c : F → M → M),
  c 0 = id → (∀ (f g : F), c (f + g) = c f ∘ c g) → ∀ (f : F) (n : ℕ), c (n • f) = (c f)^[n]
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.symm_apply : ∀ {B : Type u_1} {F : Type u_2} {E : B → Type u_3} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_3 : ∀ (x : B), Nonempty (E x)]
  (e : Bundle.Trivialization F Bundle.TotalSpace.proj) {b : B} (hb : b ∈ e.baseSet) (y : F),
  e.symm b y = cast ⋯ (↑e.symm (b, y)).snd
-- Mathlib.GroupTheory.GroupAction.Blocks
MulAction.IsInvariantBlock.eq_1 : ∀ (G : Type u_1) {X : Type u_2} [inst : SMul G X] (B : Set X), MulAction.IsInvariantBlock G B = ∀ (g : G), g • B ⊆ B
-- Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity
HasEnoughRootsOfUnity.cyc : ∀ {M : Type u_1} {inst : CommMonoid M} {n : ℕ} [self : HasEnoughRootsOfUnity M n], IsCyclic ↥(rootsOfUnity n M)
-- Std.Sync.Broadcast
/-- Try to send a value to the broadcast channel, if this can be completed right away without blocking return
`true`, otherwise don't send the value and return `false`.
 -/
Std.Broadcast.Sync.trySend : {α : Type} → Std.Broadcast.Sync α → α → BaseIO (Option ℕ)
-- Mathlib.Combinatorics.Additive.DoublingConst
Finset.card_mul_divConst : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] (A B : Finset G), ↑A.card * A.divConst B = ↑(A / B).card
-- Mathlib.NumberTheory.LSeries.Nonvanishing
_private.Mathlib.NumberTheory.LSeries.Nonvanishing.0.DirichletCharacter.BadChar.mk.inj : ∀ {N : ℕ} {inst : NeZero N} {χ : DirichletCharacter ℂ N} {χ_ne : χ ≠ 1} {χ_sq : χ ^ 2 = 1}
  {hχ : DirichletCharacter.LFunction χ 1 = 0} {χ_1 : DirichletCharacter ℂ N} {χ_ne_1 : χ_1 ≠ 1} {χ_sq_1 : χ_1 ^ 2 = 1}
  {hχ_1 : DirichletCharacter.LFunction χ_1 1 = 0},
  { χ := χ, χ_ne := χ_ne, χ_sq := χ_sq, hχ := hχ } = { χ := χ_1, χ_ne := χ_ne_1, χ_sq := χ_sq_1, hχ := hχ_1 } → χ = χ_1
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKey?_insertManyIfNewUnit!_list_of_not_mem_of_contains_eq_false : ∀ {α : Type u} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α fun x => Unit} [Std.TransOrd α] [inst : BEq α]
  [Std.LawfulBEqOrd α],
  t.WF →
    ∀ {l : List α} {k : α},
      k ∉ t → l.contains k = false → (↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit! t l)).getKey? k = none
-- Mathlib.Algebra.Order.Monoid.Lex
AddMonoidHom.inr_strictMono : ∀ {α : Type u_1} {β : Type u_2} [inst : AddMonoid α] [inst_1 : Preorder α] [inst_2 : AddMonoid β] [inst_3 : Preorder β],
  StrictMono ⇑(AddMonoidHom.inr α β)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.insertMany.congr_simp : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {ρ : Type u_1}
  [inst_1 : ForIn Id ρ (α × β)] (t t_1 : Std.ExtTreeMap α β cmp),
  t = t_1 → ∀ (l l_1 : ρ), l = l_1 → t.insertMany l = t_1.insertMany l_1
-- Mathlib.Topology.Homeomorph.Lemmas
/-- Homeomorphism given an embedding.  -/
Topology.IsEmbedding.toHomeomorph : {X : Type u_1} →
  {Y : Type u_2} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] → {f : X → Y} → Topology.IsEmbedding f → X ≃ₜ ↑(Set.range f)
-- Batteries.Control.AlternativeMonad
StateRefT'.instLawfulAlternative : ∀ {m : Type → Type} {ω σ : Type} [inst : AlternativeMonad m] [LawfulAlternative m], LawfulAlternative (StateRefT' ω σ m)
-- Mathlib.GroupTheory.Rank
Group.rank_spec : ∀ (G : Type u_1) [inst : Group G] [h : Group.FG G], ∃ S, S.card = Group.rank G ∧ Subgroup.closure ↑S = ⊤
-- Mathlib.CategoryTheory.Monoidal.Rigid.Braided
/-- If `C` is a braided and left rigid category, then it is a rigid category.
Not registered as an instance as this is not canonical enough.  -/
CategoryTheory.BraidedCategory.rigidCategoryOfLeftRigidCategory : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [CategoryTheory.BraidedCategory C] → [CategoryTheory.LeftRigidCategory C] → CategoryTheory.RigidCategory C
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMonObj.add_braiding : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.SymmetricCategory C] (X Y : C) [inst_3 : CategoryTheory.AddMonObj X]
  [inst_4 : CategoryTheory.AddMonObj Y],
  CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add (β_ X Y).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (β_ X Y).hom (β_ X Y).hom)
      CategoryTheory.AddMonObj.add
-- Mathlib.Data.Set.Basic
Set.inter_nonempty_iff_exists_right : ∀ {α : Type u} {s t : Set α}, (s ∩ t).Nonempty ↔ ∃ x ∈ t, x ∈ s
-- Mathlib.GroupTheory.HNNExtension
HNNExtension.inv_t_mul_of : ∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} {φ : ↥A ≃* ↥B} (b : ↥B),
  HNNExtension.t⁻¹ * HNNExtension.of ↑b = HNNExtension.of ↑(φ.symm b) * HNNExtension.t⁻¹
-- Mathlib.Order.BoundedOrder.Basic
OrderDual.ofDual_top : ∀ (α : Type u) [inst : Bot α], OrderDual.ofDual ⊤ = ⊥
-- Mathlib.Tactic.NormNum.PowMod
/-- Represents and proves equalities of the form `a^b % m = c` for natural numbers.  -/
Mathlib.Meta.NormNum.IsNatPowModT : Prop → ℕ → ℕ → ℕ → ℕ → Prop
-- Mathlib.GroupTheory.Complement
Subgroup.instMulActionLeftTransversal.eq_1 : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} {F : Type u_2} [inst_1 : Group F] [inst_2 : MulAction F G]
  [inst_3 : MulAction.QuotientAction F H],
  Subgroup.instMulActionLeftTransversal = { smul := fun f T => ⟨f • ↑T, ⋯⟩, mul_smul := ⋯, one_smul := ⋯ }
-- Mathlib.Topology.Category.CompHausLike.Basic
/-- Any continuous bijection of compact Hausdorff spaces induces an isomorphism.  -/
CompHausLike.isoOfBijective : {P : TopCat → Prop} →
  {X Y : CompHausLike P} → (f : X ⟶ Y) → Function.Bijective ⇑(CategoryTheory.ConcreteCategory.hom f) → (X ≅ Y)
-- Init.Omega.LinearCombo
Lean.Omega.LinearCombo.mk.injEq : ∀ (const : ℤ) (coeffs : Lean.Omega.Coeffs) (const_1 : ℤ) (coeffs_1 : Lean.Omega.Coeffs),
  ({ const := const, coeffs := coeffs } = { const := const_1, coeffs := coeffs_1 }) =
    (const = const_1 ∧ coeffs = coeffs_1)
-- Mathlib.Topology.ContinuousOn
ContinuousWithinAt.preimage_mem_nhdsWithin' : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s : Set α}
  {x : α} {t : Set β}, ContinuousWithinAt f s x → t ∈ nhdsWithin (f x) (f '' s) → f ⁻¹' t ∈ nhdsWithin x s
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
/-- `IsStrictRestriction N M` means that `N = M ↾ R` for some strict subset `R` of `M.E`  -/
Matroid.IsStrictRestriction : {α : Type u_1} → Matroid α → Matroid α → Prop
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.ofList_eq_insertMany_empty : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {l : List (α × β)},
  Std.DHashMap.Const.ofList l = Std.DHashMap.Const.insertMany ∅ l