mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Logic.Relator
/-- A relation is "bi-unique" if it is both left unique and right unique.  -/
Relator.BiUnique : {α : Sort u₁} → {β : Sort u₂} → (α → β → Prop) → Prop
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get?_erase : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k a : α}, (t.erase k).get? a = if cmp k a = Ordering.eq then none else t.get? a
-- Lean.Meta.Tactic.Simp.Arith.Nat.Basic
Lean.Meta.Simp.Arith.Nat.ToLinear.State.varMap : Lean.Meta.Simp.Arith.Nat.ToLinear.State → Lean.Meta.KExprMap ℕ
-- Mathlib.Data.Int.ConditionallyCompleteOrder
Int.csSup_of_not_bddAbove : ∀ {s : Set ℤ}, ¬BddAbove s → sSup s = 0
-- Mathlib.FieldTheory.Finite.Basic
Int.ModEq.pow_eq_pow : ∀ {p x y : ℕ}, Nat.Prime p → p - 1 ∣ x - y → y ≤ x → 0 < y → ∀ (n : ℤ), n ^ x ≡ n ^ y [ZMOD ↑p]
-- Lean.Data.Lsp.InitShutdown
Lean.Lsp.ServerInfo : Type
-- Mathlib.Data.Finset.Image
Equiv.finsetCongr_toEmbedding : ∀ {α : Type u_1} {β : Type u_2} (e : α ≃ β), e.finsetCongr.toEmbedding = (Finset.mapEmbedding e.toEmbedding).toEmbedding
-- Mathlib.Analysis.Normed.Group.Basic
norm_toNNReal : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] {a : E}, ‖a‖.toNNReal = ‖a‖₊
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.Origin.stx.sizeOf_spec : ∀ (id : Lean.Name) (ref : Lean.Syntax), sizeOf (Lean.Meta.Origin.stx id ref) = 1 + sizeOf id + sizeOf ref
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
IsCyclic.exists_generator : ∀ {α : Type u_1} [inst : Group α] [IsCyclic α], ∃ g, ∀ (x : α), x ∈ Subgroup.zpowers g
-- Mathlib.Data.QPF.Multivariate.Constructions.Const
MvQPF.Const.inhabited : (n : ℕ) → {A : Type u_1} → {α : TypeVec.{u_2} n} → [Inhabited A] → Inhabited (MvQPF.Const n A α)
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get_ofList_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List α} {k k' : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l →
      k ∈ l → ∀ {h' : k' ∈ Std.TreeSet.Raw.ofList l cmp}, (Std.TreeSet.Raw.ofList l cmp).get k' h' = k
-- Mathlib.CategoryTheory.Monad.Kleisli
CategoryTheory.Kleisli.Hom.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {T : CategoryTheory.Monad C} {c c' : CategoryTheory.Kleisli T}
  (of of_1 : c.of ⟶ T.obj c'.of), ({ of := of } = { of := of_1 }) = (of = of_1)
-- Mathlib.Analysis.SpecificLimits.Basic
/-- The limit of `n / (n + x)` is 1, for any constant `x` (valid in `ℝ` or any topological division
algebra over `ℚ≥0`, e.g., `ℂ`).  -/
tendsto_natCast_div_add_atTop : ∀ {𝕜 : Type u_4} [inst : DivisionSemiring 𝕜] [inst_1 : TopologicalSpace 𝕜] [inst_2 : CharZero 𝕜] [ContinuousSMul ℚ≥0 𝕜]
  [IsTopologicalSemiring 𝕜] [ContinuousInv₀ 𝕜] (x : 𝕜), Filter.Tendsto (fun n => ↑n / (↑n + x)) Filter.atTop (nhds 1)
-- Mathlib.Data.Num.Lemmas
Num.ofNat'_bit : ∀ (b : Bool) (n : ℕ), Num.ofNat' (Nat.bit b n) = (bif b then Num.bit1 else Num.bit0) (Num.ofNat' n)
-- Mathlib.RingTheory.Polynomial.ContentIdeal
Polynomial.contentIdeal_C : ∀ {R : Type u_1} [inst : Semiring R] (r : R), (Polynomial.C r).contentIdeal = Ideal.span {r}
-- Lean.Elab.PreDefinition.Structural.IndPred
/-- Turns `fun a b => x` into `let funType := fun a b => α` (where `x : α`).
The continuation is the called with all `funType`s corresponding to the values.
 -/
Lean.Elab.Structural.withFunTypes : {α : Type} → Array Lean.Expr → (Array Lean.Expr → Lean.MetaM α) → Lean.MetaM α
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.contains_ofList : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α] {l : List (α × β)}
  {k : α}, (Std.HashMap.Raw.ofList l).contains k = (List.map Prod.fst l).contains k
-- Mathlib.Tactic.Widget.SelectPanelUtils
/-- Replace all meta-variable names by `"?_"`.  -/
String.renameMetaVar : String → String
-- Mathlib.Tactic.GCongr.Core
/-- Whether the lemma is suitable for use in `grw`. For most lemmas this is `true`,
but there are lemmas that aren't quite congruence lemmas, but can still be used in `gcongr`.  -/
Mathlib.Tactic.GCongr.GCongrLemma.forGrw : Mathlib.Tactic.GCongr.GCongrLemma → Bool
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.ι_comp_coproductIsoSelf_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Limits.FormalCoproduct C) (i : X.I),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι X.toFun i) X.coproductIsoSelf.hom =
    CategoryTheory.Limits.FormalCoproduct.Hom.fromIncl i (CategoryTheory.CategoryStruct.id (X.obj i))
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBSet.findP?_some_eq_eq : ∀ {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {y : α} {t : RBTree.RBSet α cmp},
  t.findP? cut = some y → cut y = Ordering.eq
-- Mathlib.ModelTheory.Syntax
/-- The graph of a function as a first-order formula.  -/
FirstOrder.Language.Formula.graph : {L : FirstOrder.Language} → {n : ℕ} → L.Functions n → L.Formula (Fin (n + 1))
-- Mathlib.MeasureTheory.Integral.Average
MeasureTheory.setAverage_eq' : ∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  (μ : MeasureTheory.Measure α) (f : α → E) (s : Set α), ⨍ (x : α) in s, f x ∂μ = ∫ (x : α), f x ∂(μ s)⁻¹ • μ.restrict s
-- Mathlib.Data.Nat.Choose.Central
Nat.centralBinom_le_four_pow : ∀ (n : ℕ), n.centralBinom ≤ 4 ^ n
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
_private.Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic.0.tacticMatrix_simp : Lean.ParserDescr
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.condIndepSet_iff : ∀ {Ω : Type u_1} (m' : MeasurableSpace Ω) {mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] (hm' : m' ≤ mΩ)
  (s t : Set Ω),
  MeasurableSet s →
    MeasurableSet t →
      ∀ (μ : MeasureTheory.Measure Ω) [inst_1 : MeasureTheory.IsFiniteMeasure μ],
        ProbabilityTheory.CondIndepSet m' hm' s t μ ↔
          μ[(s ∩ t).indicator fun ω => 1 | m'] =ᵐ[μ] μ[s.indicator fun ω => 1 | m'] * μ[t.indicator fun ω => 1 | m']
-- Init.Data.String.PosRaw
String.Pos.Raw.addChar_right_comm : ∀ (p : String.Pos.Raw) (c₁ c₂ : Char), p + c₁ + c₂ = p + c₂ + c₁
-- Mathlib.Order.Minimal
Minimal.eq_of_ge : ∀ {α : Type u_2} {P : α → Prop} {x y : α} [inst : PartialOrder α], Minimal P x → P y → y ≤ x → x = y
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.Option.dmap_some : ∀ {α : Type u} {β : Type v} (a : α) (f : (a' : α) → some a = some a' → β),
  Std.Internal.List.Option.dmap✝ (some a) f = some (f a ⋯)
-- Mathlib.Algebra.Order.Group.Pointwise.Bounds
IsLUB.add : ∀ {G : Type u_2} [inst : AddGroup G] [inst_1 : Preorder G] [AddLeftMono G] [AddRightMono G] {s t : Set G} {a b : G},
  IsLUB s a → IsLUB t b → IsLUB (s + t) (a + b)
-- Init.Data.Fin.Bitwise
Fin.or_val_of_two_pow : ∀ {w : ℕ} (a b : Fin (2 ^ w)), ↑(a ||| b) = ↑a ||| ↑b
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupSeminorm.apply_one : ∀ {E : Type u_3} [inst : Group E] [inst_1 : DecidableEq E] (x : E), 1 x = if x = 1 then 0 else 1
-- Mathlib.Algebra.Star.StarAlgHom
/-- Promote a bijective star algebra homomorphism to a star algebra equivalence.  -/
StarAlgEquiv.ofBijective : {F : Type u_1} →
  {R : Type u_3} →
    {A : Type u_4} →
      {B : Type u_5} →
        [inst : Monoid R] →
          [inst_1 : NonUnitalNonAssocSemiring A] →
            [inst_2 : DistribMulAction R A] →
              [inst_3 : Star A] →
                [inst_4 : NonUnitalNonAssocSemiring B] →
                  [inst_5 : DistribMulAction R B] →
                    [inst_6 : Star B] →
                      [inst_7 : FunLike F A B] →
                        [NonUnitalAlgHomClass F R A B] →
                          [StarHomClass F A B] → (f : F) → Function.Bijective ⇑f → A ≃⋆ₐ[R] B
-- Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
WeierstrassCurve.VariableChange.map_r : ∀ {R : Type u} [inst : CommRing R] (C : WeierstrassCurve.VariableChange R) {A : Type v} [inst_1 : CommRing A]
  (φ : R →+* A), (C.map φ).r = φ C.r
-- Mathlib.CategoryTheory.ConcreteCategory.Basic
CategoryTheory.ConcreteCategory.hom_ofHom : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {FC : outParam (C → C → Type u_1)} {CC : outParam (C → Type w)}
  {inst_1 : outParam ((X Y : C) → FunLike (FC X Y) (CC X) (CC Y))} [self : CategoryTheory.ConcreteCategory C FC]
  {X Y : C} (f : FC X Y), CategoryTheory.ConcreteCategory.hom (CategoryTheory.ConcreteCategory.ofHom f) = f
-- Mathlib.Order.Bounds.Image
isGLB_pi : ∀ {α : Type u} {π : α → Type u_1} [inst : (a : α) → Preorder (π a)] {s : Set ((a : α) → π a)} {f : (a : α) → π a},
  IsGLB s f ↔ ∀ (a : α), IsGLB (Function.eval a '' s) (f a)
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.mem_map : ∀ {F : Type w} {R : Type u} {S : Type v} [inst : NonUnitalNonAssocRing R] [inst_1 : NonUnitalNonAssocRing S]
  [inst_2 : FunLike F R S] [inst_3 : NonUnitalRingHomClass F R S] {f : F} {s : NonUnitalSubring R} {y : S},
  y ∈ NonUnitalSubring.map f s ↔ ∃ x ∈ s, f x = y
-- Mathlib.Topology.Maps.Basic
Topology.IsInducing.nontrivialTopology : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace Y] [inst_1 : TopologicalSpace X] [NontrivialTopology X]
  {f : X → Y}, Topology.IsInducing f → NontrivialTopology Y
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVUnOp.reverse.sizeOf_spec : sizeOf Std.Tactic.BVDecide.BVUnOp.reverse = 1
-- Batteries.Data.Array.Match
/-- Implementation datail for `Matcher.Iterator`.  -/
Array.Matcher.modifyStep : {α σ : Type u_1} →
  {n : Type u_1 → Type u_2} →
    [inst : BEq α] →
      (m : Array.Matcher α) →
        [inst_1 : Std.Iterator σ n α] →
          (it : Std.IterM n σ) → it.internalState.inner.Step → Std.IterStep (Std.IterM n σ) σ
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
LinearMap.separatingRight_congr_iff : ∀ {R : Type u_1} {M : Type u_5} {Mₗ₁ : Type u_9} {Mₗ₁' : Type u_10} {Mₗ₂ : Type u_11} {Mₗ₂' : Type u_12}
  [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : AddCommMonoid Mₗ₁]
  [inst_4 : AddCommMonoid Mₗ₂] [inst_5 : AddCommMonoid Mₗ₁'] [inst_6 : AddCommMonoid Mₗ₂'] [inst_7 : Module R Mₗ₁]
  [inst_8 : Module R Mₗ₂] [inst_9 : Module R Mₗ₁'] [inst_10 : Module R Mₗ₂'] {B : Mₗ₁ →ₗ[R] Mₗ₂ →ₗ[R] M}
  (e₁ : Mₗ₁ ≃ₗ[R] Mₗ₁') (e₂ : Mₗ₂ ≃ₗ[R] Mₗ₂'),
  ((e₁.arrowCongr (e₂.arrowCongr (LinearEquiv.refl R M))) B).SeparatingRight ↔ B.SeparatingRight
-- Mathlib.AlgebraicGeometry.StructureSheaf
AlgebraicGeometry.StructureSheaf.algebraMap_germ_apply : ∀ {R : Type u} [inst : CommRing R] (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R))
  (x : ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) (hxU : x ∈ U) (x_1 : R),
  (CategoryTheory.ConcreteCategory.hom ((AlgebraicGeometry.structurePresheafInCommRingCat R).germ U x hxU))
      ((algebraMap R ((AlgebraicGeometry.structureSheafInType R R).obj.obj (Opposite.op U))) x_1) =
    (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.StructureSheaf.toStalk R x)) x_1
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
/-- Eta-expanded form of `TendstoUniformlyOnFilter.add` -/
TendstoUniformlyOnFilter.fun_add : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : AddGroup α] [IsUniformAddGroup α] {ι : Type u_3}
  {l : Filter ι} {l' : Filter β} {f f' : ι → β → α} {g g' : β → α},
  TendstoUniformlyOnFilter f g l l' →
    TendstoUniformlyOnFilter f' g' l l' →
      TendstoUniformlyOnFilter (fun i i_1 => f i i_1 + f' i i_1) (fun i => g i + g' i) l l'
-- Mathlib.Order.Category.HeytAlg
HeytAlg.hom_ofHom : ∀ {X Y : Type u} [inst : HeytingAlgebra X] [inst_1 : HeytingAlgebra Y] (f : HeytingHom X Y),
  HeytAlg.Hom.hom (HeytAlg.ofHom f) = f
-- Mathlib.Geometry.Manifold.Immersion
/-- A linear equivalence `E × F ≃L[𝕜] E''` which belongs to the data of an immersion `f` at `x`:
the particular equivalence is arbitrary, but this choice matches the witnesses given by
`h.domChart` and `h.codChart`.  -/
Manifold.IsImmersionAt.equiv : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      {E'' : Type u} →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : NormedSpace 𝕜 E] →
            [inst_3 : NormedAddCommGroup E''] →
              [inst_4 : NormedSpace 𝕜 E''] →
                {H : Type u_7} →
                  [inst_5 : TopologicalSpace H] →
                    {G : Type u_9} →
                      [inst_6 : TopologicalSpace G] →
                        {I : ModelWithCorners 𝕜 E H} →
                          {J : ModelWithCorners 𝕜 E'' G} →
                            {M : Type u_11} →
                              [inst_7 : TopologicalSpace M] →
                                [inst_8 : ChartedSpace H M] →
                                  {N : Type u_13} →
                                    [inst_9 : TopologicalSpace N] →
                                      [inst_10 : ChartedSpace G N] →
                                        {n : WithTop ℕ∞} →
                                          {f : M → N} →
                                            {x : M} →
                                              (h : Manifold.IsImmersionAt I J n f x) → (E × h.complement) ≃L[𝕜] E''
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Product
/-- The projection map is precisely `Path.Homotopic.proj` interpreted as a functor  -/
FundamentalGroupoidFunctor.proj_map : ∀ {I : Type u} (X : I → TopCat) (i : I)
  (x₀ x₁ : ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj (TopCat.of ((i : I) → ↑(X i))))) (p : x₀ ⟶ x₁),
  (FundamentalGroupoidFunctor.proj X i).map p = Path.Homotopic.proj i p
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.instInhabitedTruncated : {n : ℕ} → Inhabited (SSet.Truncated n)
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.toList_emptyWithCapacity : ∀ {α : Type u} {c : ℕ}, (Std.HashSet.Raw.emptyWithCapacity c).toList = []
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBMap.findEntry?.eq_1 : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : RBTree.RBMap α β cmp) (k : α),
  t.findEntry? k = RBTree.RBSet.findP? t fun x => cmp k x.1
-- Mathlib.LinearAlgebra.RootSystem.IsValuedIn
RootPairing.rootSpanMem_reflectionPerm_self : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (S : Type u_6)
  [inst_5 : CommRing S] [inst_6 : Module S M] (i : ι), P.rootSpanMem S ((P.reflectionPerm i) i) = -P.rootSpanMem S i
-- Std.Time.Format.Modifier
/-- `S`: Fraction of second (e.g., 978).
 -/
Std.Time.Modifier.S : Std.Time.Fraction → Std.Time.Modifier
-- Mathlib.Algebra.Algebra.Defs
Algebra.algebraMap_eq_smul_one : ∀ {R : Type u} {A : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (r : R),
  (algebraMap R A) r = r • 1
-- Mathlib.Data.Real.Basic
Real.instIsDomain : IsDomain ℝ
-- Std.Time.Time.PlainTime
/-- Converts a `PlainTime` value to the total number of seconds.
 -/
Std.Time.PlainTime.toSeconds : Std.Time.PlainTime → Std.Time.Second.Offset
-- Mathlib.Algebra.Lie.Weights.Cartan
LieAlgebra.rootSpace_zero_eq : ∀ (R : Type u_1) (L : Type u_2) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  (H : LieSubalgebra R L) [inst_3 : H.IsCartanSubalgebra] [IsNoetherian R L],
  LieAlgebra.rootSpace H 0 = H.toLieSubmodule
-- Init.Data.List.Nat.InsertIdx
List.getElem?_insertIdx_self : ∀ {α : Type u} {l : List α} {x : α} {i : ℕ}, (l.insertIdx i x)[i]? = if i ≤ l.length then some x else none
-- Mathlib.Order.Interval.Set.Basic
Set.nonempty_Ioo : ∀ {α : Type u_1} [inst : Preorder α] {a b : α} [DenselyOrdered α], (Set.Ioo a b).Nonempty ↔ a < b
-- Mathlib.FieldTheory.Extension
IntermediateField.Lifts.mk : {F : Type u_1} →
  {E : Type u_2} →
    {K : Type u_3} →
      [inst : Field F] →
        [inst_1 : Field E] →
          [inst_2 : Field K] →
            [inst_3 : Algebra F E] →
              [inst_4 : Algebra F K] →
                (carrier : IntermediateField F E) → (↥carrier →ₐ[F] K) → IntermediateField.Lifts F E K
-- Mathlib.AlgebraicGeometry.AffineTransitionLimit
/-- (Implementation)
The map sending `x` to `(a x, b x)`, which should fall in the diagonal component.
See the section docstring.  -/
AlgebraicGeometry.ExistsHomHomCompEqCompAux.g : {I : Type u} →
  [inst : CategoryTheory.Category.{u, u} I] →
    {S X : AlgebraicGeometry.Scheme} →
      {D : CategoryTheory.Functor I AlgebraicGeometry.Scheme} →
        {t : D ⟶ (CategoryTheory.Functor.const I).obj S} →
          {f : X ⟶ S} →
            [inst_1 : ∀ (i : I), CompactSpace ↥(D.obj i)] →
              [inst_2 : CategoryTheory.IsCofiltered I] →
                [inst_3 : ∀ {i j : I} (f : i ⟶ j), AlgebraicGeometry.IsAffineHom (D.map f)] →
                  (A : AlgebraicGeometry.ExistsHomHomCompEqCompAux D t f) →
                    D.obj A.i' ⟶ CategoryTheory.Limits.pullback f f
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.FullyFaithful.ofFullyFaithful.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [inst_2 : F.Full] [inst_3 : F.Faithful],
  CategoryTheory.Functor.FullyFaithful.ofFullyFaithful F = CategoryTheory.Functor.FullyFaithful.ofFullyFaithful F
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.id_apply : ∀ {R : Type u_1} {M : Type u_8} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (x : M),
  LinearMap.id x = x
-- Mathlib.RingTheory.MvPolynomial.Homogeneous
MvPolynomial.IsHomogeneous.prod : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R] {ι : Type u_5} (s : Finset ι) (φ : ι → MvPolynomial σ R)
  (n : ι → ℕ), (∀ i ∈ s, (φ i).IsHomogeneous (n i)) → (∏ i ∈ s, φ i).IsHomogeneous (∑ i ∈ s, n i)
-- Std.Tactic.BVDecide.Bitblast.BoolExpr.Basic
Std.Tactic.BVDecide.BoolExpr.toString : {α : Type} → [ToString α] → Std.Tactic.BVDecide.BoolExpr α → String
-- Mathlib.Algebra.Algebra.Subalgebra.Rank
Subalgebra.rank_sup_eq_rank_left_mul_rank_of_free : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (A B : Subalgebra R S)
  [Module.Free R ↥A] [Module.Free ↥A ↥(Algebra.adjoin ↥A ↑B)],
  Module.rank R ↥(A ⊔ B) = Module.rank R ↥A * Module.rank ↥A ↥(Algebra.adjoin ↥A ↑B)
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
ENNReal.tsum_mul_right : ∀ {α : Type u_1} {a : ENNReal} {f : α → ENNReal}, ∑' (i : α), f i * a = (∑' (i : α), f i) * a
-- Lean.Elab.Tactic.RCases
/-- Runs `rintroContinue` on `pats[i...*]`  -/
_private.Lean.Elab.Tactic.RCases.0.Lean.Elab.Tactic.RCases.rintroContinue.loop : {α : Type} →
  Lean.Syntax →
    Lean.TSyntaxArray `rintroPat →
      Option Lean.Term →
        (Lean.MVarId → Lean.Meta.FVarSubst → Array Lean.FVarId → α → Lean.Elab.TermElabM α) →
          ℕ → Lean.MVarId → Lean.Meta.FVarSubst → Array Lean.FVarId → α → Lean.Elab.TermElabM α
-- Mathlib.Algebra.Module.Equiv.Basic
LinearMap.ringLmapEquivSelf_symm_apply : ∀ (R : Type u_1) (S : Type u_4) (M : Type u_5) [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] [inst_4 : Module S M] [inst_5 : SMulCommClass R S M] (x : M),
  (LinearMap.ringLmapEquivSelf R S M).symm x = LinearMap.smulRight 1 x
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
/-- The subgroupoid generated by the set of arrows `X`  -/
CategoryTheory.Subgroupoid.generated : {C : Type u} → [inst : CategoryTheory.Groupoid C] → ((c d : C) → Set (c ⟶ d)) → CategoryTheory.Subgroupoid C
-- Mathlib.RingTheory.LocalRing.ResidueField.Polynomial
Localization.AtPrime.IsLiesOverAlgebra.congr_simp : ∀ {A : Type u_4} {B : Type u_5} [inst : CommSemiring A] [inst_1 : CommSemiring B] [inst_2 : Algebra A B] (p : Ideal A)
  [inst_3 : p.IsPrime] (P : Ideal B) [inst_4 : P.IsPrime] [inst_5 : P.LiesOver p]
  [inst_6 : Algebra (Localization.AtPrime p) (Localization.AtPrime P)],
  Localization.AtPrime.IsLiesOverAlgebra p P = Localization.AtPrime.IsLiesOverAlgebra p P
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
OrderedFinpartition.default_eq : ∀ {n : ℕ}, default = OrderedFinpartition.atomic n
-- Mathlib.CategoryTheory.Idempotents.Karoubi
CategoryTheory.Idempotents.zero_def : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {P Q : CategoryTheory.Idempotents.Karoubi C}, 0 = { f := 0, comm := ⋯ }
-- Init.Data.SInt.Bitwise
Int16.xor_not : ∀ {a b : Int16}, a ^^^ ~~~b = ~~~(a ^^^ b)
-- Mathlib.Order.CompactlyGenerated.Basic
/-- An element `k` is compact if and only if any directed set with `sSup` above
`k` already got above `k` at some point in the set.  -/
CompleteLattice.isCompactElement_iff_le_of_directed_sSup_le : ∀ (α : Type u_2) [inst : CompleteLattice α] (k : α),
  IsCompactElement k ↔ ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 => x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgEquiv.ofAlgEquiv_apply : ∀ {R : Type u_6} {A : Type u_7} {B : Type u_8} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : Star A] [inst_6 : Star B] (f : A ≃ₐ[R] B)
  (map_star : ∀ (x : A), f (star x) = star (f x)) (x : A), (StarAlgEquiv.ofAlgEquiv f map_star) x = f x
-- Lean.Meta.Sym.Pattern
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.isMillerPatternArgs.isUniqueArgUpTo : Lean.Expr → Lean.Expr → Lean.FVarId → Bool
-- Mathlib.CategoryTheory.Limits.Shapes.End
CategoryTheory.Limits.coend.map_id : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} [inst_2 : CategoryTheory.Limits.HasCoend F],
  CategoryTheory.Limits.coend.map (CategoryTheory.CategoryStruct.id F) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.coend F)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.inter_mul_singleton : ∀ {α : Type u_2} [inst : Mul α] [IsRightCancelMul α] [inst_2 : DecidableEq α] (s t : Finset α) (a : α),
  s ∩ t * {a} = s * {a} ∩ (t * {a})
-- Mathlib.Tactic.IntervalCases
Mathlib.Tactic.IntervalCases.Bound.lt.sizeOf_spec : ∀ (n : ℤ), sizeOf (Mathlib.Tactic.IntervalCases.Bound.lt n) = 1 + sizeOf n
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.iterate_derivative_U_eval_one_dvd : ∀ {𝔽 : Type u_3} [inst : Field 𝔽] (n : ℤ) (k : ℕ),
  ↑(∏ l ∈ Finset.range k, (2 * l + 3)) ∣ ↑(∏ l ∈ Finset.range k, ((n + 1) ^ 2 - (↑l + 1) ^ 2)) * (↑n + 1)
-- Mathlib.Topology.Constructions.SumProd
/-- A product of induced topologies is induced by the product map  -/
prod_induced_induced : ∀ {Y : Type v} {W : Type u_1} [inst : TopologicalSpace Y] [inst_1 : TopologicalSpace W] {X : Type u_5} {Z : Type u_6}
  (f : X → Y) (g : Z → W),
  instTopologicalSpaceProd = TopologicalSpace.induced (fun p => (f p.1, g p.2)) instTopologicalSpaceProd
-- Mathlib.Order.CompleteLattice.Basic
iSup₂_eq_bot : ∀ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_6} [inst : CompleteLattice α] {f : (i : ι) → κ i → α},
  ⨆ i, ⨆ j, f i j = ⊥ ↔ ∀ (i : ι) (j : κ i), f i j = ⊥
-- Mathlib.GroupTheory.Coprod.Basic
/-- Isomorphism between `AddMonoid.Coprod PUnit M` and `M`.  -/
AddEquiv.punitCoprod : (M : Type u_1) → [inst : AddMonoid M] → AddMonoid.Coprod PUnit.{u_4 + 1} M ≃+ M
-- Init.Data.Nat.Basic
/-- Applies a function to a starting value the specified number of times.

In other words, `f` is iterated `n` times on `a`.

Examples:
* `Nat.repeat f 3 a = f <| f <| f <| a`
* `Nat.repeat (· ++ "!") 4 "Hello" = "Hello!!!!"`
 -/
Nat.repeat : {α : Type u} → (α → α) → ℕ → α → α
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.size_le_size_alter : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {f : Option β → Option β}, t.size - 1 ≤ (Std.DTreeMap.Raw.Const.alter t k f).size
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.ofLp_fst : ∀ {p : ENNReal} {α : Type u_2} {β : Type u_3} (x : WithLp p (α × β)), x.ofLp.1 = x.fst
-- Lean.Meta.Basic
/-- Ensures that the user names of all local declarations after index `idx` have a macro scope.
 -/
_private.Lean.Meta.Basic.0.Lean.Meta.freshenUserNamesSinceIdx : {n : Type → Type u_1} → [Monad n] → [MonadLiftT Lean.MetaM n] → Lean.LocalContext → ℕ → n Lean.LocalContext